From 0ace730306e6ac62b46745fd01ebf2461004026f Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 29 Sep 2026 19:48:46 +0000 Subject: [PATCH] DO NOT MERGE: spine depths 24/48/96 on #12640's pre-change base 476baf1 (old list gather) Co-Authored-By: Claude Opus 5.5 (1M context) --- .../execution/infer_gather_cost_test.dag | 104 ++++++++++++++++++ 1 file changed, 104 insertions(+) create mode 100644 src/v2/test/claim/execution/infer_gather_cost_test.dag diff --git a/src/v2/test/claim/execution/infer_gather_cost_test.dag b/src/v2/test/claim/execution/infer_gather_cost_test.dag new file mode 100644 index 00000000000..2939f15a3f2 --- /dev/null +++ b/src/v2/test/claim/execution/infer_gather_cost_test.dag @@ -0,0 +1,104 @@ +module v2.test.execution.infer_gather_cost + +import std.occurrence_identity { OccurrenceSynthetic } +import v2.compiler.resolve { ResolvedTree } +import v2.std.symbol_index { empty_symbol_index } +import v2.compiler.infer { DerivedGrounding, GroundingNotDerived, infer } +import v2.extdeps.languages.dag { dag_int_literal_fixture_one } +import v2.std.diagnostic { Accepted, Rejected } +import v2.std.integer { Int } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import v2.std.logic { Bool } +import v2.std.node { Conj, Edge, Named, Node, TypeNode } +import v2.std.optional { Absent, Present } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// SUBJECT: the v2.compiler.infer gather fold's cost in the depth of the tree it folds. The +// gather used to carry each subtree's facts as an entries LIST: every parent joined its children's +// lists and answered each lookup by scanning, so a spine of depth n paid a superlinear term in n. +// It now threads one facts Map through fold_node (infer_gather_step_run), so each node enters its +// facts once and each lookup is a map lookup. +// +// THE INSTRUMENT IS THE FLOOR'S EVAL-STEP COUNT FOR THIS CLAIM: the per-claim cost TSV the required +// floor writes (GUNBC_REQUIRED_FLOOR_CLAIM_COST, uploaded as required_floor_claim_cost.tsv, column +// eval_steps) and the new-witness ceiling it is admitted under +// (v2.workflow.required_floor required_floor_new_witness_eval_step_budget). A claim cannot read its +// own eval steps, so the claim cannot state the growth law as a ratio of two depths; it states it +// as ADMISSION: the depth is chosen so the threaded gather fits the ceiling and the list gather it +// replaced does not. The PR that landed this records both runs. +// +// THE SPECIMEN IS SUPPLIED, NOT PRODUCED (DESIGN section 3, a witness discriminates at one +// interface): a right-nested product spine, each level a Conj of an int literal and the rest, so +// every level awaits and takes the product row. Its pairing inhabitance claim -- that the real +// front end emits Conj products the same row derives -- is +// v2.test.execution.infer_product_introduction product_introduction_derives_fully_evidenced_products_holds, which runs the +// real ingest and asserts every Conj in it derives. + +data infer_gather_cost_spine_depth: Int = 96 + +fn infer_gather_cost_spine(depth: Int) -> Node { + if depth == 0 { + dag_int_literal_fixture_one() + } else { + Node { + kind: TypeNode { connective: Conj }, + children: [ + Edge { label: Named { name: ^infer_gather_cost_head }, target: dag_int_literal_fixture_one() }, + Edge { label: Named { name: ^infer_gather_cost_rest }, target: infer_gather_cost_spine(depth: depth - 1) } + ], + occurrence_id: OccurrenceSynthetic + } + } +} + +// The spine's root derives: every level took the product row over derived children, so the fold +// reached the root with the facts of every level entered. A gather that dropped or failed to thread +// a level leaves the root on the frontier. +test fn infer_gather_deep_product_spine_derives_its_root_holds() -> Bool { + let spine = infer_gather_cost_spine(depth: infer_gather_cost_spine_depth) + match infer(tree: ResolvedTree { root: spine, symbol_index: empty_symbol_index() }) { + Rejected { diagnostics: _ } => false + Accepted { value: t, diagnostics: _ } => + match t.facts.lookup(spine) { + Absent => false + Present { value: facts } => + match facts.grounding { + GroundingNotDerived { node: _ } => false + DerivedGrounding { grounding: _ } => true + } + } + } +} + +test fn dnm_spine_depth_24_derives_its_root_holds() -> Bool { + let spine = infer_gather_cost_spine(depth: 24) + match infer(tree: ResolvedTree { root: spine, symbol_index: empty_symbol_index() }) { + Rejected { diagnostics: _ } => false + Accepted { value: t, diagnostics: _ } => + match t.facts.lookup(spine) { + Absent => false + Present { value: facts } => + match facts.grounding { + GroundingNotDerived { node: _ } => false + DerivedGrounding { grounding: _ } => true + } + } + } +} + +test fn dnm_spine_depth_48_derives_its_root_holds() -> Bool { + let spine = infer_gather_cost_spine(depth: 48) + match infer(tree: ResolvedTree { root: spine, symbol_index: empty_symbol_index() }) { + Rejected { diagnostics: _ } => false + Accepted { value: t, diagnostics: _ } => + match t.facts.lookup(spine) { + Absent => false + Present { value: facts } => + match facts.grounding { + GroundingNotDerived { node: _ } => false + DerivedGrounding { grounding: _ } => true + } + } + } +}