From 568dfa28d73cce99d0bfbfc596cc3b543e678d78 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 12 Sep 2026 03:38:07 +0000 Subject: [PATCH 01/11] Repair the accumulator-copy analyzer: an argument capture is not the argument's value v2.lens.complexity_accumulator_copy.analyze port_reading took its identifier census with collect_value_identifiers over the WHOLE ^dag_surface_arg capture, which for a named argument `left: acc` carries the LABEL as well as the value. Measured on the specimen: the list_append call capture is found, it has two ports, and port 0 reads PortComputedExpression with mentions = 2 containing both ^left and ^acc. So `idents == 1` was false, the arm that consults arg_value_symbol and yields PortBareName { name: ^acc } was unreachable, and classify_copied_port took ^copied_port_computed_argument -- the undecidable residue, non-gating by design. No Poly2Suspect was minted and accumulator_copy_compile_gate ACCEPTED the textbook quadratic. It is none of the three candidates the brief offered: the shape matcher finds the call, the carrier is bound (count_fold_sites bound_only > 0), and list_append is rostered (copied_port_citation_list_append). Because every .dag call uses named arguments, the bare-name arm was unreachable for the entire corpus, which is why the lens has never minted a suspect on ingested source. port_reading now reads the argument's VALUE subtree, the same ^dag_surface_primary_expr node arg_value_symbol already reads through, so the census and the symbol read ask one authority what the argument IS. Nothing is widened: the no-value-capture arm still reads the whole capture, so it stays an over-approximation that degrades toward the refusal causes and never toward clean. Second latent red on main, same subject and the class gunbc#11025 already fixed once: v2.test.long.accumulator_copy_fold_analysis findings_of passed the sealed NormalizedTree where a Node is wanted (missing .root, dead since the BL-1 seal in #10439), so all 21 of its witnesses were dark with "no field 'kind' on type 'NormalizedTree'". Evidence: all 7 witnesses of accumulator_copy_compile_gate_test now PASS, including gate_red_quadratic_rejects, which FAILs on the same tree without the lens change. The three diag_* controls that discriminated the failure are enrolled beside gate_red/gate_green, in the census obligation's witness list and in the witness_deferral_freeze identity join for that entry. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01H2w1vtH78R73h7qyTK7Ah6 --- dag/gunbc/v2_compile_obligation_census.dag | 20 ++++++++++ dag/gunbc/witness/witness_deferral_freeze.dag | 4 +- .../complexity_accumulator_copy/analyze.dag | 26 ++++++++++++- .../accumulator_copy_compile_gate_test.dag | 38 +++++++++++++++++++ .../accumulator_copy_fold_analysis_test.dag | 2 +- 5 files changed, 86 insertions(+), 4 deletions(-) diff --git a/dag/gunbc/v2_compile_obligation_census.dag b/dag/gunbc/v2_compile_obligation_census.dag index 1fe6d3a665c..02bd2d0aaa4 100644 --- a/dag/gunbc/v2_compile_obligation_census.dag +++ b/dag/gunbc/v2_compile_obligation_census.dag @@ -475,6 +475,26 @@ data accumulator_copy_obligation: V2CompileObligation = V2CompileObligation { function: "gate_green_identity_accepts_clean", module_path: "v2.test.long.accumulator_copy_compile_gate" ), + witness_subject( + entry: "src/v2/test/claim/long/accumulator_copy_compile_gate_test.dag", + function: "diag_quadratic_ingest_reaches_the_gate", + module_path: "v2.test.long.accumulator_copy_compile_gate" + ), + witness_subject( + entry: "src/v2/test/claim/long/accumulator_copy_compile_gate_test.dag", + function: "diag_quadratic_gate_does_not_accept", + module_path: "v2.test.long.accumulator_copy_compile_gate" + ), + witness_subject( + entry: "src/v2/test/claim/long/accumulator_copy_compile_gate_test.dag", + function: "diag_quadratic_rejection_is_not_some_other_reason", + module_path: "v2.test.long.accumulator_copy_compile_gate" + ), + witness_subject( + entry: "src/v2/test/claim/long/accumulator_copy_fold_analysis_test.dag", + function: "quadratic_fold_has_suspect", + module_path: "v2.test.long.accumulator_copy_fold_analysis" + ), witness_subject( entry: "src/v2/test/claim/complexity/accumulator_copy_roster_gate_test.dag", function: "roster_machine_code_zero_suspects_within_ratchet", diff --git a/dag/gunbc/witness/witness_deferral_freeze.dag b/dag/gunbc/witness/witness_deferral_freeze.dag index d0475a1fde8..64ee6bcd83c 100644 --- a/dag/gunbc/witness/witness_deferral_freeze.dag +++ b/dag/gunbc/witness/witness_deferral_freeze.dag @@ -832,7 +832,9 @@ data frozen_path_deferrals: List = [ entry: "src/v2/test/claim/long/accumulator_copy_compile_gate_test.dag", functions: [ "gate_red_quadratic_rejects", "gate_green_identity_accepts_clean", - "gate_refusal_ledger_counted_not_gating", "door_root_roster_runs_and_passes_clean_tree" + "gate_refusal_ledger_counted_not_gating", "door_root_roster_runs_and_passes_clean_tree", + "diag_quadratic_ingest_reaches_the_gate", "diag_quadratic_gate_does_not_accept", + "diag_quadratic_rejection_is_not_some_other_reason" ] }, FrozenPathDeferral { diff --git a/src/v2/lens/complexity_accumulator_copy/analyze.dag b/src/v2/lens/complexity_accumulator_copy/analyze.dag index e9d6e401e2a..06a4c4900b6 100644 --- a/src/v2/lens/complexity_accumulator_copy/analyze.dag +++ b/src/v2/lens/complexity_accumulator_copy/analyze.dag @@ -111,15 +111,37 @@ fn collect_value_identifiers(n: Node) -> List { collect_value_identifiers_into(n: n, acc: std.algebra.Empty) } +// AN ARGUMENT CAPTURE IS NOT THE ARGUMENT'S VALUE. A named argument `left: acc` captures the +// LABEL as well as the value, and the label is a parameter name at the CALLEE - it is not an +// identifier this body mentions. Counting it made every named-argument port read two identifiers, +// so the bare-name arm below was unreachable for every call in a corpus where named arguments are +// the ordinary spelling, and a copied accumulator classified as ^copied_port_computed_argument: a +// refusal standing exactly where a proof was available, which is why the lens minted no suspect on +// the textbook fold/list_append specimen. The value subtree is the node arg_value_symbol already +// reads through, so the identifier census and the symbol read now ask ONE authority what the +// argument IS rather than disagreeing about it. The no-value-capture arm keeps reading the whole +// capture: the census stays an over-approximation there, so the reading degrades toward the +// refusal arms and never toward clean. +fn arg_value_capture_optional(arg_capture: Node) -> Optional { + find_capture(root: arg_capture, emitted: ^dag_surface_primary_expr) +} + fn arg_value_symbol(arg_capture: Node) -> Optional { - match find_capture(root: arg_capture, emitted: ^dag_surface_primary_expr) { + match arg_value_capture_optional(arg_capture: arg_capture) { Absent => Absent Present { value: value_expr } => sequence_left_symbol(cap: value_expr) } } +fn arg_value_mentions(arg_capture: Node) -> List { + match arg_value_capture_optional(arg_capture: arg_capture) { + Present { value: value_expr } => collect_value_identifiers(n: value_expr) + Absent => collect_value_identifiers(n: arg_capture) + } +} + fn port_reading(arg_capture: Node) -> v2.lens.complexity_accumulator_copy.PortReading { - let mentions = collect_value_identifiers(n: arg_capture) + let mentions = arg_value_mentions(arg_capture: arg_capture) let idents = symbol_list_length(xs: mentions) if idents == 0 { v2.lens.complexity_accumulator_copy.PortPureLiteral diff --git a/src/v2/test/claim/long/accumulator_copy_compile_gate_test.dag b/src/v2/test/claim/long/accumulator_copy_compile_gate_test.dag index 522441779de..7aa1af29db6 100644 --- a/src/v2/test/claim/long/accumulator_copy_compile_gate_test.dag +++ b/src/v2/test/claim/long/accumulator_copy_compile_gate_test.dag @@ -90,6 +90,44 @@ test fn gate_red_quadratic_rejects() -> Bool { } } +// THE THREE-WAY DISCRIMINATOR, ENROLLED RATHER THAN RUN ONCE BY HAND. When +// gate_red_quadratic_rejects went red these three separated the states its single Bool cannot: +// an upstream stage refusing the snippet, a rejection carrying some OTHER reason, and the gate +// ACCEPTING. Only the third was true, which is what located the defect in the lens's port reading +// rather than in the ingest chain or the refusal arms. They stay enrolled because the red they +// discriminate is not retired by the repair - each one independently reddens on a different +// regression, and a gate red with no discriminator costs the next reader the same afternoon. +test fn diag_quadratic_ingest_reaches_the_gate() -> Bool { + match normalized_of(source: quad_snippet) { + ProbeStageRejected { stage: _ } => false + ProbeNormalized { root: _ } => true + } +} + +test fn diag_quadratic_gate_does_not_accept() -> Bool { + match normalized_of(source: quad_snippet) { + ProbeStageRejected { stage: _ } => false + ProbeNormalized { root: root } => + match accumulator_copy_compile_gate(node: root) { + Rejected { diagnostics: _ } => true + Accepted { value: _, diagnostics: _ } => false + } + } +} + +test fn diag_quadratic_rejection_is_not_some_other_reason() -> Bool { + match normalized_of(source: quad_snippet) { + ProbeStageRejected { stage: _ } => false + ProbeNormalized { root: root } => + match accumulator_copy_compile_gate(node: root) { + Rejected { diagnostics: d } => + non_empty_contains_reason(d: d, reason: ^accumulator_copy_poly2_suspect) + && !non_empty_contains_reason(d: d, reason: ^copied_port_computed_argument) + Accepted { value: _, diagnostics: _ } => false + } + } +} + test fn gate_green_identity_accepts_clean() -> Bool { match normalized_of(source: identity_snippet) { ProbeStageRejected { stage: _ } => false diff --git a/src/v2/test/claim/long/accumulator_copy_fold_analysis_test.dag b/src/v2/test/claim/long/accumulator_copy_fold_analysis_test.dag index 42de8fc05b8..c3988f9a613 100644 --- a/src/v2/test/claim/long/accumulator_copy_fold_analysis_test.dag +++ b/src/v2/test/claim/long/accumulator_copy_fold_analysis_test.dag @@ -49,7 +49,7 @@ fn ingest(source_text: String, file: Symbol) -> Optional { Accepted { value: artifact, diagnostics: _ } => match v2.compiler.normalize.normalize(parse_tree: artifact.tree) { Rejected { diagnostics: _ } => Absent - Accepted { value: tree, diagnostics: _ } => Present { value: tree } + Accepted { value: normalized, diagnostics: _ } => Present { value: normalized.root } } } } From 4b76b9af5c094bdf58df9bf0a37c20b962266744 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 12 Sep 2026 04:09:50 +0000 Subject: [PATCH 02/11] Declare the four reds the .root repair makes visible, and file the fold fail-open Un-darkening v2.test.long.accumulator_copy_fold_analysis puts 17 witnesses dark-to-green and 4 dark-to-visibly-red. Attribution is measured, not assumed: a control worktree carrying ONLY the .root repair, with the port_reading change absent, fails all four identically, so they are pre-existing and unmasked rather than introduced. A discriminating probe separates them into three defects, and each is rostered at its own grain per the ruling from eager-raven-113. let_alias_is_proven_suspect is NOT a lens fact and NOT a fixture typo: staged probe shows tokenize ACCEPTS and v2.compiler.parse parse_module REJECTS the specimen, so it never reaches normalize or the lens, and the witness's `Absent => false` reports a stage refusal as a lens verdict. A six-cell ingest matrix narrows the refusing shape: a let binding the fn literal's own parameter standing immediately before a call statement. Renaming the binder still refuses; an unbound RHS, a literal RHS, a second let, and the one-line spelling all parse. Trigger: the grammar admits that statement shape. let_fresh_binding_is_provably_clean is a false refusal that FAILS CLOSED -- the lens over-refuses a provably fresh binding with ^copied_port_computed_argument, which rides the non-gating Accepted channel, so no quadratic can be admitted through it. named_step_fold_refuses_accumulator_unread and report_counters_state_the_domain are one silent fail-open (DESIGN section 5): for fold(xs, init: 0, f: step) the normalized tree carries NO lowered Loop and NO surface fold call, count_fold_sites returns 0, and the lens's own ^fold_accumulator_unread arm in fold_family_carrier is unreachable -- a written, located refusal no input can trigger, which reads to a reader as coverage. Filed as gunbc.recurring_failure_mode.fold_shape_visible_to_no_lens: found at below the floor, ceiling structurally guaranteed, trigger naming the capability with the suspected home in v2.compiler.fold_lowering / body_lowering_fold rather than the lens. Deliberately not repaired here -- that scope is unbounded inside a PR whose subject is the port reading. The four also leave the gunbc.witness_deferral_freeze FrozenPathDeferral row for that entry: a witness leaves discovery for ONE reason, and carrying both an exact admission and a path policy is the dual representation that module exists to replace. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01H2w1vtH78R73h7qyTK7Ah6 --- dag/gunbc/explicit_witness_admission.dag | 32 +++++++++++++++++++ .../fold_shape_visible_to_no_lens.dag | 18 +++++++++++ dag/gunbc/witness/witness_deferral_freeze.dag | 9 +++--- 3 files changed, 54 insertions(+), 5 deletions(-) create mode 100644 dag/gunbc/recurring_failure_mode/fold_shape_visible_to_no_lens.dag diff --git a/dag/gunbc/explicit_witness_admission.dag b/dag/gunbc/explicit_witness_admission.dag index 4c7498d8156..754708bb235 100644 --- a/dag/gunbc/explicit_witness_admission.dag +++ b/dag/gunbc/explicit_witness_admission.dag @@ -385,6 +385,38 @@ data explicit_witness_admissions: List = [ reason: "SelfEmitted wet behavioral receipt, red on assemble (same cargo/shim closure refuse class as its parse_engine_hooks peer; cadence run 30126573464). Owner: #7199 falsifier lane / self-host assemble. This is the row whose file-grain pairing forced the documented workaround: the file's sibling declared_source_refs_complete_holds is offline, so classifying the FILE QuarantineProbeExpectRed would have orphaned it and the file was downgraded to OfflineLocalRecipe in prose instead. At exact grain the receipt is admitted here and the sibling keeps the file's path policy, with neither fact restating the other.", dissolution: unbound_dissolution(description: "the local wet receipt greens under gunbc_falsifier_self_host_wet_receipt_wall_budget; this row deletes and the green wet SelfHostWetReceiptBinding restores") ), + known_red_probe( + entry: "src/v2/test/claim/long/accumulator_copy_fold_analysis_test.dag", + f: "let_alias_is_proven_suspect", + kind: CorpusWitnessKind, + budget: SubstrateLongLaneEvalBudget, + reason: "THE SUBJECT NEVER REACHES THE LENS: THE FIXTURE IS REFUSED BY PARSE. Measured by staged probe on the exact let_alias_snippet bytes, tokenize ACCEPTS and v2.compiler.parse parse_module REJECTS, so normalize never runs, findings are Empty, and the witness's `Absent => false` reports a STAGE REFUSAL as though the lens returned no suspect. The refusal is shape-specific and was narrowed by a six-cell ingest matrix over the same harness rather than guessed: `let grown = acc` followed by the call REFUSES; the same body with the binder renamed to `g` REFUSES; `let grown = mystery` (an unbound name) PARSES; `let seed = 0` PARSES; the transitive form `let g = acc` then `let h = g` then the call PARSES; and the identical alias with the `let` on the fn-literal's own line PARSES. So it is neither the binder name nor the statement count nor the RHS being an identifier -- the refusing combination is a let whose RHS names the fn literal's bound parameter standing immediately before a call statement. THIS ROW IS NOT A CLAIM ABOUT THE LENS. Whether the analyzer would prove the alias suspect is UNKNOWN and unmeasurable while parse refuses the specimen, and the sibling let_transitive_alias_is_proven_suspect -- which does parse -- PASSES, so the aliasing closure itself is exercised and green at the two-binding grain. THE ROW EXISTS BECAUSE THE WITNESS ONLY BECAME VISIBLE NOW: the whole module was dark on main with a NormalizedTree/.root type drift that this same PR repairs, so all 21 of its witnesses were unexecuted, and this red is pre-existing and unmasked rather than introduced -- established on a control worktree carrying ONLY the .root repair with the lens change absent, where it fails identically. Owner: the .dag grammar lane, not the complexity lens lane.", + dissolution: unbound_dissolution(description: "v2.compiler.parse parse_module ACCEPTS a fn-literal body whose let binds the literal's own parameter and is followed directly by a call statement, sufficient for the let_alias_snippet bytes to reach normalize -- the capability is the grammar admitting that statement shape, NOT any artifact contributing to it: a new fixture spelling, a reworded snippet, or a diagnostic variant retires nothing, because rewriting the fixture to a shape that already parses would delete the only executing evidence that this shape does not. When parse admits it, this witness reaches the lens and either greens or reds on a LENS fact for the first time; this row deletes in that same change and the assertion becomes an ordinary permanent regression control for the single-binding alias case") + ), + known_red_probe( + entry: "src/v2/test/claim/long/accumulator_copy_fold_analysis_test.dag", + f: "let_fresh_binding_is_provably_clean", + kind: CorpusWitnessKind, + budget: SubstrateLongLaneEvalBudget, + reason: "A FALSE REFUSAL, WHICH FAILS CLOSED AND CONTAINS THE HARM, WHICH IS WHY IT IS A ROW RATHER THAN A FIX HERE. This fixture DOES ingest -- measured, unlike its let_alias sibling -- and the analyzer returns exactly one finding, ^copied_port_computed_argument, where the witness asserts zero. So a provably fresh binding (`let seed = 0`, a pure literal RHS, then list_append(left: seed, right: x)) is reported as undecidable residue instead of clean. The direction matters for the ladder: the lens over-refuses rather than under-refuses, so no copied accumulator is admitted by this defect and the compile gate cannot be made to ACCEPT a quadratic through it -- ^copied_port_computed_argument rides the Accepted diagnostics channel, counted and non-gating, so the cost is a noisy ledger and a stopped-line audit entry, not a silent pass. Attribution is measured on both sides: it fails identically on a control worktree carrying ONLY the NormalizedTree/.root repair with this PR's port_reading change absent, so it is pre-existing and unmasked by un-darkening the module, not introduced by the named-argument fix. The adjacent sibling let_fresh's BindsFresh path is declared in v2.lens.complexity_accumulator_copy resolve_port_reading, so the suspicion is that the let-spine resolution does not reach this binder rather than that BindsFresh is wrong, but that is a HYPOTHESIS and is deliberately not asserted here. Owner: the complexity lens lane.", + dissolution: unbound_dissolution(description: "v2.lens.complexity_accumulator_copy.analyze distinguishes a provably fresh let-binding from an unresolved alias at the copied port, so a binder whose RHS is a pure literal resolves to PortPureLiteral through resolve_port_reading and the specimen yields NO finding at all -- the capability is the analyzer deciding freshness for the single-binding let spine, not the mere existence of the BindsFresh constructor, which is already declared and already reachable for other shapes and therefore retires nothing. When it lands this assertion greens with no edit to the witness and this row deletes in the same change") + ), + known_red_probe( + entry: "src/v2/test/claim/long/accumulator_copy_fold_analysis_test.dag", + f: "named_step_fold_refuses_accumulator_unread", + kind: CorpusWitnessKind, + budget: SubstrateLongLaneEvalBudget, + reason: "A SILENT FAIL-OPEN (DESIGN section 5), AND THE MOST SERIOUS THING THIS LANE FOUND: the lens does not see the fold at all, rather than refusing it. For `fold(xs, init: 0, f: step)` -- a fold whose step is passed BY NAME rather than as an fn literal -- the normalized tree measured by probe contains NO lowered Loop and NO surface fold call, and v2.lens.complexity_accumulator_copy.analyze count_fold_sites returns 0. The witness asserts the honest arm, ^fold_accumulator_unread, which v2.lens.complexity_accumulator_copy.analyze fold_family_carrier mints when the seam refuses to yield a carrier; that refusal is never reached because the traversal never recognises a fold site to refuse ABOUT. This is the failure arm widening into silence rather than refusing: a fold the source declares is absent from the lens's domain, so its accumulator is neither proven, nor refused, nor counted -- and unlike the named-argument defect this same PR repairs, nothing in the ledger records that a subject was skipped. The class is filed at gunbc.recurring_failure_mode.fold_shape_visible_to_no_lens. Attribution is measured: identical failure on a control worktree carrying ONLY the NormalizedTree/.root repair with this PR's lens change absent, so pre-existing and unmasked rather than introduced. NOT FIXED HERE ON A DELIBERATE RULING (eager-raven-113): the repair is plausibly in v2.compiler.fold_lowering or v2.compiler.body_lowering_fold rather than in the lens, and is therefore unbounded inside a PR whose subject is the port reading. Owner: dispatched from the recurring-failure-mode row.", + dissolution: unbound_dissolution(description: "v2.lens.complexity_accumulator_copy.analyze OBSERVES every fold the source declares, at every lowering shape a fold-family call can take -- including a step passed by name, which today lowers to neither a Loop nor a surviving surface fold call -- so count_fold_sites counts the site and the carrier-unread case reaches its ^fold_accumulator_unread refusal instead of vanishing. The capability is totality of the lens's fold domain over declared fold shapes; a diagnostic variant, a roster row, or a lowering that merely reports the shape retires nothing unless the site becomes VISIBLE to the traversal. When it lands this assertion and its report_counters sibling green with no edit and both rows delete in the same change") + ), + known_red_probe( + entry: "src/v2/test/claim/long/accumulator_copy_fold_analysis_test.dag", + f: "report_counters_state_the_domain", + kind: CorpusWitnessKind, + budget: SubstrateLongLaneEvalBudget, + reason: "THE SAME DEFECT AS ITS named_step_fold_refuses_accumulator_unread SIBLING, MEASURED AT THE COUNTER GRAIN, and rostered separately because it is a separate executing assertion rather than because it is a separate fact. The witness asserts the lens's domain census over two specimens: folds_seen 1 and carriers_bound 1 for the fold/list_append quadratic, and folds_seen 1 with carriers_bound 0 for the named-step fold. The first conjunct holds -- measured directly, count_fold_sites over the quadratic is non-zero in both the bound and unbound readings. The second does not: for `fold(xs, init: 0, f: step)` count_fold_sites returns 0, not 1, because the site is invisible to the traversal rather than seen-and-unbound. That is exactly the distinction the counters exist to publish -- a fold whose carrier could not be read is supposed to be COUNTED and unbound, and a fold that is not counted at all is the lens silently narrowing its own domain -- so this witness is the instrument that would have caught the fail-open had it ever executed. It never did: the module was dark on main with the NormalizedTree/.root drift this PR repairs. Attribution measured on a control worktree carrying ONLY that repair: identical failure with this PR's lens change absent. Class: gunbc.recurring_failure_mode.fold_shape_visible_to_no_lens.", + dissolution: unbound_dissolution(description: "the same capability its sibling row names -- v2.lens.complexity_accumulator_copy.analyze observes every fold the source declares at every lowering shape, so a named-step fold is counted by count_fold_sites with carriers_bound 0 rather than being absent from the census. This row deletes together with the named_step_fold_refuses_accumulator_unread row when that lands; neither retires on a counter being renamed, a specimen being changed, or the assertion being split") + ), known_red_probe( entry: "src/v2/test/claim/long/production_qualification_origin_probe_witness_test.dag", f: "witness_live_scope_fixture_origin_discoverable_in_entry_closure_reds", diff --git a/dag/gunbc/recurring_failure_mode/fold_shape_visible_to_no_lens.dag b/dag/gunbc/recurring_failure_mode/fold_shape_visible_to_no_lens.dag new file mode 100644 index 00000000000..1d7748d1b72 --- /dev/null +++ b/dag/gunbc/recurring_failure_mode/fold_shape_visible_to_no_lens.dag @@ -0,0 +1,18 @@ +module gunbc.recurring_failure_mode.fold_shape_visible_to_no_lens + +import std.types { NonEmptyStr } +import gunbc.recurring_failure_mode { RecurringFailureMode } + +data fold_shape_visible_to_no_lens: RecurringFailureMode = RecurringFailureMode { + identity: "fold_shape_visible_to_no_lens" as NonEmptyStr, + + receipts: [ + "a fold shape that lowers to NEITHER a substrate Loop NOR a surviving surface fold call, so no lens can see it: the site is absent from the analyzer's domain rather than refused inside it, and the accumulator it carries is neither proven, nor refused, nor counted (DESIGN section 5 -- a failure arm must refuse, never widen; here it widens into silence)", + "SPECIMEN AND INSTRUMENT, 2026-09-12. `fold(xs, init: 0, f: step)` -- a fold-family call whose step is passed BY NAME rather than as an fn literal. Ingested through tokenize / parse_module / normalize, the normalized tree contains no ComputationNode Loop and no surface fold call, and `v2.lens.complexity_accumulator_copy.analyze` `count_fold_sites` returns 0 in both the bound and unbound readings. The instrument is the fixture itself: `named_step_snippet` in `src/v2/test/claim/long/accumulator_copy_fold_analysis_test.dag`, whose two witnesses `named_step_fold_refuses_accumulator_unread` and `report_counters_state_the_domain` are the executing evidence and are rostered red at `gunbc.explicit_witness_admission`.", + "WHAT MAKES IT THIS CLASS RATHER THAN A MISSING FEATURE: the lens ALREADY CARRIES the honest arm for this exact situation and it is unreachable. `v2.lens.complexity_accumulator_copy.analyze` `fold_family_carrier` mints ^fold_accumulator_unread precisely when the seam refuses to yield a carrier -- the named-step case is named in its own carrier note as a Stage B callee-resolution fact -- but the refusal is never reached, because the traversal never recognises a site to refuse ABOUT. So the corpus contains a written, correct, located refusal that no input can trigger, which reads to every reader as coverage. The tell is a domain counter that reports 0 where the source visibly declares 1, and it is only detectable if the counter is asserted SEPARATELY from the verdict.", + "WHY IT SURVIVED, and it is a property of the evidence rather than of the defect. Both witnesses live in a module that was DARK: `ingest` passed the sealed NormalizedTree carrier where a Node is wanted (missing `.root`, dead since the BL-1 seal), so all 21 witnesses of that file failed at the type level and none of them ever evaluated its subject. The fail-open and the instrument that would have caught it were disabled by the same unrelated defect, which is why un-darkening a module is a discovery operation and not a formality: 17 of those 21 came back green, and the 4 that came back red were pre-existing -- established on a control worktree carrying only the `.root` repair.", + "THE RUNG, stated with its ceiling because a fold the lens cannot see is BELOW the floor rather than low on it: found at below-the-floor, since the complexity lens is a required root gate at the compile door and a subject invisible to it is admitted in silence regardless of how the gate is enrolled. The ceiling is STRUCTURALLY GUARANTEED, and it is reachable: fold-family lowering is a closed, decidable set of declared shapes, so a lowering total over that set makes the invisible site unwritable rather than merely detected. NEXT-RUNG TRIGGER, named as a capability: every fold-family call the source declares lowers to a shape the lens's traversal enumerates -- suspected home `v2.compiler.fold_lowering` or `v2.compiler.body_lowering_fold` rather than the lens, which is why the repair is dispatched as its own item and was deliberately NOT attempted inside the port-reading fix that found it. A diagnostic variant, a roster row, or a lowering that merely reports the shape retires nothing unless the site becomes visible to the traversal.", + ], + + evidence: [], +} diff --git a/dag/gunbc/witness/witness_deferral_freeze.dag b/dag/gunbc/witness/witness_deferral_freeze.dag index 64ee6bcd83c..d251df927cb 100644 --- a/dag/gunbc/witness/witness_deferral_freeze.dag +++ b/dag/gunbc/witness/witness_deferral_freeze.dag @@ -841,19 +841,18 @@ data frozen_path_deferrals: List = [ entry: "src/v2/test/claim/long/accumulator_copy_fold_analysis_test.dag", functions: [ "quadratic_fold_has_suspect", "real_branch_body_quadratic_is_caught", - "noncarrier_name_in_copied_port_refuses_not_clean", "let_alias_is_proven_suspect", - "let_transitive_alias_is_proven_suspect", "let_fresh_binding_is_provably_clean", - "let_unknown_alias_still_refuses_may_alias", + "noncarrier_name_in_copied_port_refuses_not_clean", + "let_transitive_alias_is_proven_suspect", "let_unknown_alias_still_refuses_may_alias", "nested_call_head_cannot_masquerade_as_bare_name", "unregistered_combiner_reached_by_carrier_refuses", "carrier_inside_computed_argument_to_unregistered_combiner_refuses", "item_inside_computed_argument_stays_clean", "computed_let_mentioning_carrier_refuses_at_unregistered_use", "unreadable_call_head_with_carrier_port_refuses", - "named_step_fold_refuses_accumulator_unread", "multiline_unregistered_combiner_refuses", + "multiline_unregistered_combiner_refuses", "projection_call_carrier_is_classified", "quadratic_ingest_has_lowered_loop", "quadratic_ingest_has_no_surface_fold_call", "identity_fold_has_no_finding", - "out_of_iteration_append_is_out_of_domain", "report_counters_state_the_domain" + "out_of_iteration_append_is_out_of_domain" ] }, FrozenPathDeferral { From c3828148ddd970d912cf0e82791882bab1ad66da Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 12 Sep 2026 04:35:24 +0000 Subject: [PATCH 03/11] Home the diag controls where they execute, instead of growing the frozen roster Review 64325 is right and the gate behind it is real. The previous commit appended three identities to gunbc.witness_deferral_freeze frozen_path_deferrals so the new diag_* controls could sit beside the gate's red/green controls. That roster is frozen against GROWTH by the cli_run collect_frozen_path_deferral_additions monotonicity gate, which is a key set-difference against the diff baseline -- so a net -4/+3 does not cancel, the three new keys refuse, and the push would have redded CI. DESIGN section 3 says the same thing for a frozen X: no new rows on its growth surfaces. The deeper point is the one the module itself states: for a GREEN witness under an offline home the only exact cadence available is QuarantineProbeExpectRed, which is a declaration that a witness is RED and cannot be written truthfully about a green one -- so the compliant move is not to author there. The brief said to enrol these controls "beside" the existing ones; the authority docs say a green witness may not live in a home that executes nothing, and the docs win. So the three discriminators move to src/v2/test/claim/complexity/accumulator_copy_compile_gate_diag_test.dag, which per-PR discovery DOES execute (the complexity exclusion is the narrower claim/complexity/accumulator_copy_roster_gate prefix, not the directory), the freeze roster returns to its main content for that entry, and the census witness rows repoint to the executing path and module. Measured in the new home rather than assumed affordable: all three PASS at cpu=851ms / 1022ms / 1051ms, wall <= 2003ms, against the 5000ms fast-lane per-witness budget -- which is why these three fit per-PR while the gate's own red/green controls, which they discriminate, do not. The freeze roster's only remaining change is SHRINKAGE: the four witnesses that gained exact known_red_probe admissions leave it, which is the migration that module names for legacy rows. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01H2w1vtH78R73h7qyTK7Ah6 --- dag/gunbc/v2_compile_obligation_census.dag | 12 +-- dag/gunbc/witness/witness_deferral_freeze.dag | 4 +- ...ccumulator_copy_compile_gate_diag_test.dag | 101 ++++++++++++++++++ .../accumulator_copy_compile_gate_test.dag | 38 ------- 4 files changed, 108 insertions(+), 47 deletions(-) create mode 100644 src/v2/test/claim/complexity/accumulator_copy_compile_gate_diag_test.dag diff --git a/dag/gunbc/v2_compile_obligation_census.dag b/dag/gunbc/v2_compile_obligation_census.dag index 02bd2d0aaa4..9aa43445436 100644 --- a/dag/gunbc/v2_compile_obligation_census.dag +++ b/dag/gunbc/v2_compile_obligation_census.dag @@ -476,19 +476,19 @@ data accumulator_copy_obligation: V2CompileObligation = V2CompileObligation { module_path: "v2.test.long.accumulator_copy_compile_gate" ), witness_subject( - entry: "src/v2/test/claim/long/accumulator_copy_compile_gate_test.dag", + entry: "src/v2/test/claim/complexity/accumulator_copy_compile_gate_diag_test.dag", function: "diag_quadratic_ingest_reaches_the_gate", - module_path: "v2.test.long.accumulator_copy_compile_gate" + module_path: "v2.test.claim.complexity.accumulator_copy_compile_gate_diag" ), witness_subject( - entry: "src/v2/test/claim/long/accumulator_copy_compile_gate_test.dag", + entry: "src/v2/test/claim/complexity/accumulator_copy_compile_gate_diag_test.dag", function: "diag_quadratic_gate_does_not_accept", - module_path: "v2.test.long.accumulator_copy_compile_gate" + module_path: "v2.test.claim.complexity.accumulator_copy_compile_gate_diag" ), witness_subject( - entry: "src/v2/test/claim/long/accumulator_copy_compile_gate_test.dag", + entry: "src/v2/test/claim/complexity/accumulator_copy_compile_gate_diag_test.dag", function: "diag_quadratic_rejection_is_not_some_other_reason", - module_path: "v2.test.long.accumulator_copy_compile_gate" + module_path: "v2.test.claim.complexity.accumulator_copy_compile_gate_diag" ), witness_subject( entry: "src/v2/test/claim/long/accumulator_copy_fold_analysis_test.dag", diff --git a/dag/gunbc/witness/witness_deferral_freeze.dag b/dag/gunbc/witness/witness_deferral_freeze.dag index d251df927cb..546e62111be 100644 --- a/dag/gunbc/witness/witness_deferral_freeze.dag +++ b/dag/gunbc/witness/witness_deferral_freeze.dag @@ -832,9 +832,7 @@ data frozen_path_deferrals: List = [ entry: "src/v2/test/claim/long/accumulator_copy_compile_gate_test.dag", functions: [ "gate_red_quadratic_rejects", "gate_green_identity_accepts_clean", - "gate_refusal_ledger_counted_not_gating", "door_root_roster_runs_and_passes_clean_tree", - "diag_quadratic_ingest_reaches_the_gate", "diag_quadratic_gate_does_not_accept", - "diag_quadratic_rejection_is_not_some_other_reason" + "gate_refusal_ledger_counted_not_gating", "door_root_roster_runs_and_passes_clean_tree" ] }, FrozenPathDeferral { diff --git a/src/v2/test/claim/complexity/accumulator_copy_compile_gate_diag_test.dag b/src/v2/test/claim/complexity/accumulator_copy_compile_gate_diag_test.dag new file mode 100644 index 00000000000..35c2852a9bc --- /dev/null +++ b/src/v2/test/claim/complexity/accumulator_copy_compile_gate_diag_test.dag @@ -0,0 +1,101 @@ +module v2.test.claim.complexity.accumulator_copy_compile_gate_diag + +import std.occurrence_identity { OccurrenceSynthetic } +import v2.compiler.tokenize { tokenize } +import v2.compiler.parse { parse } +import v2.compiler.normalize { normalize } +import v2.extdeps.languages.dag { dag_language_model } +import v2.lens.complexity_accumulator_copy.compile_gate { accumulator_copy_compile_gate } +import v2.std.diagnostic { + Accepted, + NonEmptyDiagnostics, + Rejected +} +import v2.std.logic { Bool } +import v2.std.node { Node, Symbol } +import v2.std.text { String } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// THE THREE-WAY DISCRIMINATOR FOR THE ACCUMULATOR-COPY GATE, HOMED WHERE IT EXECUTES PER PR. +// +// When gate_red_quadratic_rejects went red on main, its single Bool could not say WHICH of three +// states held: an upstream stage refusing the snippet, a rejection carrying some OTHER reason, or +// the gate ACCEPTING. Separating them is what located the defect in the lens's port reading rather +// than in the ingest chain -- the analyzer read a named argument's LABEL as a value identifier, so +// the bare-name arm was unreachable for every named-argument call in the corpus and a copied +// accumulator classified as undecidable residue. +// +// WHY THIS FILE IS NOT BESIDE THE WITNESS IT DISCRIMINATES. The gate's own red/green controls live +// in src/v2/test/claim/long/, which discovery excludes at dir grain, so a witness authored there +// executes nowhere. Three GREEN discriminators cannot be admitted there either: the only exact +// cadence available for an offline home is QuarantineProbeExpectRed, which is a declaration that a +// witness is RED and cannot be written truthfully about a green one, and the path-policy roster is +// frozen against growth by the cli_run collect_frozen_path_deferral_additions monotonicity gate. So +// the compliant move is the one gunbc.witness_deferral_freeze names: do not author there. These +// three are self-contained over a snippet and the root-grain gate, which is why they fit the per-PR +// fast-lane budget while the long-home controls do not. +data quad_snippet: String = "module quad\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) { list_append(left: acc, right: x) })\n}\n" + +type DiagProbe + = DiagStageRejected { stage: String } + | DiagNormalized { root: Node } + +fn normalized_of(source: String) -> DiagProbe { + let lm = dag_language_model() + match tokenize(text: source, file: ^compile_gate_diag_witness_file, rules: lm.lex) { + Rejected { diagnostics: _ } => DiagStageRejected { stage: "tokenize" } + Accepted { value: stream, diagnostics: _ } => + match parse(tokens: stream, grammar: lm.grammar) { + Rejected { diagnostics: _ } => DiagStageRejected { stage: "parse" } + Accepted { value: parse_tree, diagnostics: _ } => + match normalize(parse_tree: parse_tree) { + Rejected { diagnostics: _ } => DiagStageRejected { stage: "normalize" } + Accepted { value: normalized, diagnostics: _ } => + DiagNormalized { root: normalized.root } + } + } + } +} + +fn non_empty_contains_reason(d: NonEmptyDiagnostics, reason: Symbol) -> Bool { + if d.head.reason == reason { + true + } else { + fold(d.tail, init: false, f: fn(acc, diag) { + acc || (diag.reason == reason) + }) + } +} + +test fn diag_quadratic_ingest_reaches_the_gate() -> Bool { + match normalized_of(source: quad_snippet) { + DiagStageRejected { stage: _ } => false + DiagNormalized { root: _ } => true + } +} + +test fn diag_quadratic_gate_does_not_accept() -> Bool { + match normalized_of(source: quad_snippet) { + DiagStageRejected { stage: _ } => false + DiagNormalized { root: root } => + match accumulator_copy_compile_gate(node: root) { + Rejected { diagnostics: _ } => true + Accepted { value: _, diagnostics: _ } => false + } + } +} + +test fn diag_quadratic_rejection_is_not_some_other_reason() -> Bool { + match normalized_of(source: quad_snippet) { + DiagStageRejected { stage: _ } => false + DiagNormalized { root: root } => + match accumulator_copy_compile_gate(node: root) { + Rejected { diagnostics: d } => + non_empty_contains_reason(d: d, reason: ^accumulator_copy_poly2_suspect) + && !non_empty_contains_reason(d: d, reason: ^copied_port_computed_argument) + Accepted { value: _, diagnostics: _ } => false + } + } +} diff --git a/src/v2/test/claim/long/accumulator_copy_compile_gate_test.dag b/src/v2/test/claim/long/accumulator_copy_compile_gate_test.dag index 7aa1af29db6..522441779de 100644 --- a/src/v2/test/claim/long/accumulator_copy_compile_gate_test.dag +++ b/src/v2/test/claim/long/accumulator_copy_compile_gate_test.dag @@ -90,44 +90,6 @@ test fn gate_red_quadratic_rejects() -> Bool { } } -// THE THREE-WAY DISCRIMINATOR, ENROLLED RATHER THAN RUN ONCE BY HAND. When -// gate_red_quadratic_rejects went red these three separated the states its single Bool cannot: -// an upstream stage refusing the snippet, a rejection carrying some OTHER reason, and the gate -// ACCEPTING. Only the third was true, which is what located the defect in the lens's port reading -// rather than in the ingest chain or the refusal arms. They stay enrolled because the red they -// discriminate is not retired by the repair - each one independently reddens on a different -// regression, and a gate red with no discriminator costs the next reader the same afternoon. -test fn diag_quadratic_ingest_reaches_the_gate() -> Bool { - match normalized_of(source: quad_snippet) { - ProbeStageRejected { stage: _ } => false - ProbeNormalized { root: _ } => true - } -} - -test fn diag_quadratic_gate_does_not_accept() -> Bool { - match normalized_of(source: quad_snippet) { - ProbeStageRejected { stage: _ } => false - ProbeNormalized { root: root } => - match accumulator_copy_compile_gate(node: root) { - Rejected { diagnostics: _ } => true - Accepted { value: _, diagnostics: _ } => false - } - } -} - -test fn diag_quadratic_rejection_is_not_some_other_reason() -> Bool { - match normalized_of(source: quad_snippet) { - ProbeStageRejected { stage: _ } => false - ProbeNormalized { root: root } => - match accumulator_copy_compile_gate(node: root) { - Rejected { diagnostics: d } => - non_empty_contains_reason(d: d, reason: ^accumulator_copy_poly2_suspect) - && !non_empty_contains_reason(d: d, reason: ^copied_port_computed_argument) - Accepted { value: _, diagnostics: _ } => false - } - } -} - test fn gate_green_identity_accepts_clean() -> Bool { match normalized_of(source: identity_snippet) { ProbeStageRejected { stage: _ } => false From f3f8273cbb3d0cad408d9513f90c50166c800e1c Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 12 Sep 2026 05:50:18 +0000 Subject: [PATCH 04/11] Withdraw the diag controls: no ingesting witness can be enrolled per-PR CI on c3828148ddd refused with nine blockers -- three per new witness: interrupted_before_verdict, changed_witness_planned_without_terminal_verdict, enrolment_censored_at_ceiling. The witnesses WERE planned, so the executing home was right; what was wrong was the budget I checked them against. I compared 851ms / 1022ms / 1051ms CPU to the 5000ms fast-lane eval deadline and called the relocation affordable. That is the wrong line. The applicable ceilings are v2.workflow.required_floor required_floor_claim_cpu_safety_limit_ms at 500ms, and for a NEWLY enrolled witness the tighter derived budget from v2.workflow.floor_enrolment_margin floor_enrolment_margin_budget_ms -- the 500ms ceiling deflated by the runner-variance envelope. The measurement was right and the comparison was wrong, which is worse than not measuring: it produced a confident affordability claim on the PR. The constraint is structural rather than a tuning gap. calm-crane-722 measured the per-claim cost as a ~500ms FIXED front end -- dag_language_model plus tokenize/parse/normalize, rebuilt in every claim's own evaluation frame, invariant to the subject-specific work. A witness whose subject IS the ingest path therefore cannot clear a 500ms ceiling with margin at any per-PR home, which is exactly why the gate's own red/green controls live in the long home. And the long home cannot take them either: its path roster refuses growth, and the only offline cadence that executes is QuarantineProbeExpectRed, which declares a witness RED and cannot be written truthfully about a green one. So the three discriminators come out rather than being hidden behind a hand-built tree that would assert a lowering shape I authored instead of one I observed -- my own probing found the real shape surprising (a surface primary_expr inside a lowered Loop, not a lowered Transform), so a synthetic fixture would go green while the real path broke. Brief item (2), "enrol the three diag_* controls as executing evidence", is therefore UNMET, with the reason measured and the trigger named: the fixed per-claim ingest front end has to come down, or a cadence has to exist that executes a green witness too expensive for the fast lane. What the discriminators established is not lost -- it is in gate_red_quadratic_rejects, in the four known_red_probe reasons, and in gunbc.recurring_failure_mode.fold_shape_visible_to_no_lens. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01H2w1vtH78R73h7qyTK7Ah6 --- dag/gunbc/v2_compile_obligation_census.dag | 15 --- ...ccumulator_copy_compile_gate_diag_test.dag | 101 ------------------ 2 files changed, 116 deletions(-) delete mode 100644 src/v2/test/claim/complexity/accumulator_copy_compile_gate_diag_test.dag diff --git a/dag/gunbc/v2_compile_obligation_census.dag b/dag/gunbc/v2_compile_obligation_census.dag index 9aa43445436..bf130699d8f 100644 --- a/dag/gunbc/v2_compile_obligation_census.dag +++ b/dag/gunbc/v2_compile_obligation_census.dag @@ -475,21 +475,6 @@ data accumulator_copy_obligation: V2CompileObligation = V2CompileObligation { function: "gate_green_identity_accepts_clean", module_path: "v2.test.long.accumulator_copy_compile_gate" ), - witness_subject( - entry: "src/v2/test/claim/complexity/accumulator_copy_compile_gate_diag_test.dag", - function: "diag_quadratic_ingest_reaches_the_gate", - module_path: "v2.test.claim.complexity.accumulator_copy_compile_gate_diag" - ), - witness_subject( - entry: "src/v2/test/claim/complexity/accumulator_copy_compile_gate_diag_test.dag", - function: "diag_quadratic_gate_does_not_accept", - module_path: "v2.test.claim.complexity.accumulator_copy_compile_gate_diag" - ), - witness_subject( - entry: "src/v2/test/claim/complexity/accumulator_copy_compile_gate_diag_test.dag", - function: "diag_quadratic_rejection_is_not_some_other_reason", - module_path: "v2.test.claim.complexity.accumulator_copy_compile_gate_diag" - ), witness_subject( entry: "src/v2/test/claim/long/accumulator_copy_fold_analysis_test.dag", function: "quadratic_fold_has_suspect", diff --git a/src/v2/test/claim/complexity/accumulator_copy_compile_gate_diag_test.dag b/src/v2/test/claim/complexity/accumulator_copy_compile_gate_diag_test.dag deleted file mode 100644 index 35c2852a9bc..00000000000 --- a/src/v2/test/claim/complexity/accumulator_copy_compile_gate_diag_test.dag +++ /dev/null @@ -1,101 +0,0 @@ -module v2.test.claim.complexity.accumulator_copy_compile_gate_diag - -import std.occurrence_identity { OccurrenceSynthetic } -import v2.compiler.tokenize { tokenize } -import v2.compiler.parse { parse } -import v2.compiler.normalize { normalize } -import v2.extdeps.languages.dag { dag_language_model } -import v2.lens.complexity_accumulator_copy.compile_gate { accumulator_copy_compile_gate } -import v2.std.diagnostic { - Accepted, - NonEmptyDiagnostics, - Rejected -} -import v2.std.logic { Bool } -import v2.std.node { Node, Symbol } -import v2.std.text { String } -import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } - -data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly - -// THE THREE-WAY DISCRIMINATOR FOR THE ACCUMULATOR-COPY GATE, HOMED WHERE IT EXECUTES PER PR. -// -// When gate_red_quadratic_rejects went red on main, its single Bool could not say WHICH of three -// states held: an upstream stage refusing the snippet, a rejection carrying some OTHER reason, or -// the gate ACCEPTING. Separating them is what located the defect in the lens's port reading rather -// than in the ingest chain -- the analyzer read a named argument's LABEL as a value identifier, so -// the bare-name arm was unreachable for every named-argument call in the corpus and a copied -// accumulator classified as undecidable residue. -// -// WHY THIS FILE IS NOT BESIDE THE WITNESS IT DISCRIMINATES. The gate's own red/green controls live -// in src/v2/test/claim/long/, which discovery excludes at dir grain, so a witness authored there -// executes nowhere. Three GREEN discriminators cannot be admitted there either: the only exact -// cadence available for an offline home is QuarantineProbeExpectRed, which is a declaration that a -// witness is RED and cannot be written truthfully about a green one, and the path-policy roster is -// frozen against growth by the cli_run collect_frozen_path_deferral_additions monotonicity gate. So -// the compliant move is the one gunbc.witness_deferral_freeze names: do not author there. These -// three are self-contained over a snippet and the root-grain gate, which is why they fit the per-PR -// fast-lane budget while the long-home controls do not. -data quad_snippet: String = "module quad\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) { list_append(left: acc, right: x) })\n}\n" - -type DiagProbe - = DiagStageRejected { stage: String } - | DiagNormalized { root: Node } - -fn normalized_of(source: String) -> DiagProbe { - let lm = dag_language_model() - match tokenize(text: source, file: ^compile_gate_diag_witness_file, rules: lm.lex) { - Rejected { diagnostics: _ } => DiagStageRejected { stage: "tokenize" } - Accepted { value: stream, diagnostics: _ } => - match parse(tokens: stream, grammar: lm.grammar) { - Rejected { diagnostics: _ } => DiagStageRejected { stage: "parse" } - Accepted { value: parse_tree, diagnostics: _ } => - match normalize(parse_tree: parse_tree) { - Rejected { diagnostics: _ } => DiagStageRejected { stage: "normalize" } - Accepted { value: normalized, diagnostics: _ } => - DiagNormalized { root: normalized.root } - } - } - } -} - -fn non_empty_contains_reason(d: NonEmptyDiagnostics, reason: Symbol) -> Bool { - if d.head.reason == reason { - true - } else { - fold(d.tail, init: false, f: fn(acc, diag) { - acc || (diag.reason == reason) - }) - } -} - -test fn diag_quadratic_ingest_reaches_the_gate() -> Bool { - match normalized_of(source: quad_snippet) { - DiagStageRejected { stage: _ } => false - DiagNormalized { root: _ } => true - } -} - -test fn diag_quadratic_gate_does_not_accept() -> Bool { - match normalized_of(source: quad_snippet) { - DiagStageRejected { stage: _ } => false - DiagNormalized { root: root } => - match accumulator_copy_compile_gate(node: root) { - Rejected { diagnostics: _ } => true - Accepted { value: _, diagnostics: _ } => false - } - } -} - -test fn diag_quadratic_rejection_is_not_some_other_reason() -> Bool { - match normalized_of(source: quad_snippet) { - DiagStageRejected { stage: _ } => false - DiagNormalized { root: root } => - match accumulator_copy_compile_gate(node: root) { - Rejected { diagnostics: d } => - non_empty_contains_reason(d: d, reason: ^accumulator_copy_poly2_suspect) - && !non_empty_contains_reason(d: d, reason: ^copied_port_computed_argument) - Accepted { value: _, diagnostics: _ } => false - } - } -} From 033f05a381586581b1c0ad6798d5bf7ae9abf248 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 12 Sep 2026 06:27:00 +0000 Subject: [PATCH 05/11] Strip the argument label by navigation, not by search Review 64393 is correct and the defect was mine, introduced by the previous repair. Verified in the source before changing anything: v2.extdeps.languages.dag parse_subtree_find_production_captured is a FIRST-MATCH DFS that short-circuits on ParseSubtreeFound, and dag_surface_binary_expr / dag_surface_unary_expr sit ABOVE dag_surface_primary_expr in the grammar. So searching an argument for its first primary_expr returns only the LEFTMOST operand of a compound argument, and the census became an UNDER-approximation of the identifiers the argument names -- while the annotation I wrote beside it claimed an over-approximation. The consequence is the arm DESIGN section 5 forbids. `left: seed + acc` censused as mentions [seed]: one identifier, so the bare-name arm fired; a BindsFresh `seed` resolved through resolve_port_reading to PortPureLiteral; classify_copied_port answered Absent; and a copied accumulator classified CLEAN with the carrier invisible to any_port_carries_carrier as well, because it reads the same narrowed list. A failure arm that widens into silence, and the same class this PR files at gunbc.recurring_failure_mode.fold_shape_visible_to_no_lens -- which is why it is recorded in the annotation rather than quietly corrected. arg_value_node now walks the `name : value` spine instead of searching for a production, and EVERY deviation from that exact shape falls back to the whole capture: a positional argument has no label to strip, and a sequence whose separator is an operator rather than ^dag_token_colon is not a labelled argument. Both keep the whole-capture census, which over-approximates, so the reading degrades toward the refusal arms and never toward clean -- what the annotation claimed all along and now actually does. MEASURED ON THE REAL TREE, both directions, since the previous claim here was a confident assertion that did not hold: plain `left: acc` -> mentions [acc], label excluded, one identifier, PortBareName, suspect (unchanged) compound `left: seed + acc` -> mentions [seed, acc] -- BOTH operands, label excluded -- PortComputedExpression, ^copied_port_computed_argument, NOT clean, and no false suspect Regression: 21/21 PASS across both accumulator-copy modules, 0 FAIL -- gate_red_quadratic_rejects included, and the 17 fold-analysis witnesses that are not declared red. The fixture gap review 64393 names is real and I cannot close it: a binary-expression port fixture is a new witness, and a witness whose subject is the ingest path cannot clear the 500ms per-claim floor ceiling at any per-PR home while the long home's roster refuses growth. That is the capability gap already recorded as a frontier with this PR as its specimen; the guard is verified by local probe and by the unchanged existing witnesses, and that is weaker evidence than an enrolled fixture would be. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01H2w1vtH78R73h7qyTK7Ah6 --- .../complexity_accumulator_copy/analyze.dag | 61 ++++++++++++++++--- 1 file changed, 52 insertions(+), 9 deletions(-) diff --git a/src/v2/lens/complexity_accumulator_copy/analyze.dag b/src/v2/lens/complexity_accumulator_copy/analyze.dag index 06a4c4900b6..12f94791544 100644 --- a/src/v2/lens/complexity_accumulator_copy/analyze.dag +++ b/src/v2/lens/complexity_accumulator_copy/analyze.dag @@ -117,11 +117,26 @@ fn collect_value_identifiers(n: Node) -> List { // so the bare-name arm below was unreachable for every call in a corpus where named arguments are // the ordinary spelling, and a copied accumulator classified as ^copied_port_computed_argument: a // refusal standing exactly where a proof was available, which is why the lens minted no suspect on -// the textbook fold/list_append specimen. The value subtree is the node arg_value_symbol already -// reads through, so the identifier census and the symbol read now ask ONE authority what the -// argument IS rather than disagreeing about it. The no-value-capture arm keeps reading the whole -// capture: the census stays an over-approximation there, so the reading degrades toward the -// refusal arms and never toward clean. +// the textbook fold/list_append specimen. +// +// THE LABEL IS STRIPPED BY NAVIGATION, NOT BY SEARCH, AND THAT DISTINCTION IS THE WHOLE CORRECTNESS +// ARGUMENT. The first repair here searched for the argument's first ^dag_surface_primary_expr. +// v2.extdeps.languages.dag parse_subtree_find_production_captured is a FIRST-MATCH DFS that +// short-circuits on ParseSubtreeFound, and dag_surface_binary_expr / dag_surface_unary_expr sit +// ABOVE primary_expr in the grammar - so a compound argument returned only its leftmost primary +// expression and the census became an UNDER-approximation of the identifiers the argument names. +// `left: seed + acc` read as mentions [seed]: one identifier, so the bare-name arm fired, a +// BindsFresh `seed` resolved it to PortPureLiteral, and a copied accumulator classified CLEAN with +// the carrier invisible to any_port_carries_carrier as well. That is the failure arm widening into +// silence that DESIGN section 5 forbids, and the same class this lens's own roster files as +// fold_shape_visible_to_no_lens - introduced by the repair, caught in review, and recorded here so +// the shape is not re-derived by search a third time. +// +// So the value is reached by walking the `name : value` spine, and EVERY deviation from that exact +// shape falls back to the whole capture. A positional argument has no label to strip; a sequence +// whose second element is an operator rather than ^dag_token_colon is not a labelled argument at +// all. Both keep the whole-capture census, which over-approximates the mention set, so the reading +// degrades toward the refusal arms and never toward clean. fn arg_value_capture_optional(arg_capture: Node) -> Optional { find_capture(root: arg_capture, emitted: ^dag_surface_primary_expr) } @@ -133,13 +148,41 @@ fn arg_value_symbol(arg_capture: Node) -> Optional { } } -fn arg_value_mentions(arg_capture: Node) -> List { - match arg_value_capture_optional(arg_capture: arg_capture) { - Present { value: value_expr } => collect_value_identifiers(n: value_expr) - Absent => collect_value_identifiers(n: arg_capture) +fn arg_value_node(arg_capture: Node) -> Node { + match sequence_left_node(cap: arg_capture) { + Absent => arg_capture + Present { value: name_node } => + match v2.std.grammar.node_atom_identity_optional(node: name_node) { + Absent => arg_capture + Present { value: _label } => + match sequence_right_node(cap: arg_capture) { + Absent => arg_capture + Present { value: after_name } => + match sequence_left_node(cap: after_name) { + Absent => arg_capture + Present { value: separator } => + match v2.std.grammar.node_atom_identity_optional(node: separator) { + Absent => arg_capture + Present { value: sep } => + if sep == ^dag_token_colon { + match sequence_right_node(cap: after_name) { + Absent => arg_capture + Present { value: value_node } => value_node + } + } else { + arg_capture + } + } + } + } + } } } +fn arg_value_mentions(arg_capture: Node) -> List { + collect_value_identifiers(n: arg_value_node(arg_capture: arg_capture)) +} + fn port_reading(arg_capture: Node) -> v2.lens.complexity_accumulator_copy.PortReading { let mentions = arg_value_mentions(arg_capture: arg_capture) let idents = symbol_list_length(xs: mentions) From d28feb598070aceb3e3e20daf5259ffc9d888579 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 12 Sep 2026 06:53:47 +0000 Subject: [PATCH 06/11] Re-point the accumulator-copy fixtures to the axis the cost authority now names #11019 landed mid-flight and repointed list_append's copied-port citation from the left operand to the right, because the concat realization copies the appended side: v2.std.fn_index records that v1_rt::rc_list_concat make_muts the LEFT and clones the RIGHT. So this PR's own fixtures asserted a retired cost shape. The brief's textbook specimen, list_append(left: acc, right: x), copies only x per step -- it is LINEAR under the current realization, and a correct lens must not flag it. The quadratic is list_append(left: x, right: acc). MEASURED, NOT INFERRED, and attributed before it was repaired. On the merged tree quadratic_fold_has_suspect, real_branch_body_quadratic_is_caught and let_transitive_alias_is_proven_suspect FAILED, and noncarrier_name_in_copied_port_refuses_not_clean INVERTED -- its left: x, right: acc snippet had become the suspect case. A control worktree on origin/main carrying only the .root repair, with this PR's lens change absent, fails the same four, so the inversion is #11019's and not this PR's. THE DIRECTION COMES FROM THE AUTHORITY, AND NOTHING HERE ENCODES IT. The lens reads v2.lens.cost.copied_port_citations copied_port_index_of, whose rows cite the concat contract and carry their own dissolution to producer-ingested Arrow bodies; that is why the verdicts moved on their own when the citation was repointed. Adding a second left/right encoding in the lens to "fix" this would have been the section 3 fork review 64414 already caught once in this PR. Only the FIXTURES hard-coded the axis, so only the fixtures move: every in-iteration list_append now carries its subject on the copied (right) port. out_of_iteration_snippet is deliberately untouched -- it has no carrier and asserts out-of-domain. RED BEFORE, GREEN AFTER, both on the corrected fixtures: pre-fix seed (main + .root, lens change absent): gate_red_quadratic_rejects FAIL, all four fold witnesses FAIL, gate_green_identity_accepts_clean PASS this tree: gate module 4/4 PASS including gate_red_quadratic_rejects; fold module 17 PASS and 4 FAIL, the four being exactly the declared ExpectAssertionFalse rows. let_fresh_binding_is_provably_clean does NOT green under the flip, so its known-red row is not false on arrival. Also in this push, from the merge: the known_red_probe row for gate_red_quadratic_rejects is DELETED -- its trigger has fired, so the witness is an ordinary permanent regression control again (DESIGN 4b(4)) -- and the census annotation records that the trigger fired while the rung STAYS Mitigatable, because 4b(1) takes the minimum across paths and fold_shape_visible_to_no_lens establishes a population where this gate's wall does not execute at all. gunbc.recurring_failure_mode required_lens_red_control_never_executes_from_its_home gains a second specimen: the same dark home is why #11019 could repoint the cost axis and leave these fixtures stale, with nobody to run them. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01H2w1vtH78R73h7qyTK7Ah6 --- .../long/accumulator_copy_compile_gate_test.dag | 2 +- .../long/accumulator_copy_fold_analysis_test.dag | 16 ++++++++-------- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/src/v2/test/claim/long/accumulator_copy_compile_gate_test.dag b/src/v2/test/claim/long/accumulator_copy_compile_gate_test.dag index 956035b1282..44dea9ef3d8 100644 --- a/src/v2/test/claim/long/accumulator_copy_compile_gate_test.dag +++ b/src/v2/test/claim/long/accumulator_copy_compile_gate_test.dag @@ -58,7 +58,7 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // // The sources are therefore restored to the forms that read clearly, since a shortened spelling that // buys nothing is redundant work with a refuted rationale attached. -data quad_snippet: String = "module quad\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) { list_append(left: acc, right: x) })\n}\n" +data quad_snippet: String = "module quad\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) { list_append(left: x, right: acc) })\n}\n" data identity_snippet: String = "module ident\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) { acc })\n}\n" diff --git a/src/v2/test/claim/long/accumulator_copy_fold_analysis_test.dag b/src/v2/test/claim/long/accumulator_copy_fold_analysis_test.dag index c3988f9a613..d2354c6a4e1 100644 --- a/src/v2/test/claim/long/accumulator_copy_fold_analysis_test.dag +++ b/src/v2/test/claim/long/accumulator_copy_fold_analysis_test.dag @@ -5,17 +5,17 @@ import v2.std.algebra { Cons, Empty } data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly -data quadratic_snippet: String = "module quad\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) { list_append(left: acc, right: x) })\n}\n" +data quadratic_snippet: String = "module quad\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) { list_append(left: x, right: acc) })\n}\n" -data noncarrier_name_snippet: String = "module lin\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) { list_append(left: x, right: acc) })\n}\n" +data noncarrier_name_snippet: String = "module lin\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) { list_append(left: acc, right: x) })\n}\n" data identity_snippet: String = "module ident\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) { acc })\n}\n" -data real_branch_body_snippet: String = "module rs\n\nfn g(xs: List) -> Int {\n fold_list(xs: xs, empty: Empty, cons: fn(acc, r) {\n if pred(r: r) {\n list_append(left: acc, right: Cons { head: r, tail: Empty })\n } else {\n acc\n }\n })\n}\n" +data real_branch_body_snippet: String = "module rs\n\nfn g(xs: List) -> Int {\n fold_list(xs: xs, empty: Empty, cons: fn(acc, r) {\n if pred(r: r) {\n list_append(left: Cons { head: r, tail: Empty }, right: acc)\n } else {\n acc\n }\n })\n}\n" -data let_alias_snippet: String = "module alias\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) {\n let grown = acc\n list_append(left: grown, right: x)\n })\n}\n" +data let_alias_snippet: String = "module alias\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) {\n let grown = acc\n list_append(left: x, right: grown)\n })\n}\n" -data nested_call_snippet: String = "module nested\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) { list_append(left: reverse(acc), right: x) })\n}\n" +data nested_call_snippet: String = "module nested\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) { list_append(left: x, right: reverse(acc)) })\n}\n" data unregistered_combiner_snippet: String = "module unreg\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) { mystery_op(a: acc, b: x) })\n}\n" @@ -23,11 +23,11 @@ data out_of_iteration_snippet: String = "module once\n\nfn f(xs: List, ys: data named_step_snippet: String = "module namedstep\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: step)\n}\n" -data let_unknown_alias_snippet: String = "module unknownalias\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) {\n let grown = mystery\n list_append(left: grown, right: x)\n })\n}\n" +data let_unknown_alias_snippet: String = "module unknownalias\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) {\n let grown = mystery\n list_append(left: x, right: grown)\n })\n}\n" -data let_fresh_snippet: String = "module freshlet\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) {\n let seed = 0\n list_append(left: seed, right: x)\n })\n}\n" +data let_fresh_snippet: String = "module freshlet\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) {\n let seed = 0\n list_append(left: x, right: seed)\n })\n}\n" -data let_transitive_alias_snippet: String = "module transalias\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) {\n let g = acc\n let h = g\n list_append(left: h, right: x)\n })\n}\n" +data let_transitive_alias_snippet: String = "module transalias\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) {\n let g = acc\n let h = g\n list_append(left: x, right: h)\n })\n}\n" data carrier_in_computed_arg_snippet: String = "module hiddencarrier\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) {\n mystery(box: Wrapped { inner: acc })\n })\n}\n" From 92de157832e1690350c2ddbe303b29c60ab1f5e3 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 12 Sep 2026 06:59:05 +0000 Subject: [PATCH 07/11] State the named-argument divergence, and file the collapsed-operand class Operator ruling (eager-raven-113) on review 64414's fork finding, and it is a better diagnosis than either remedy the review offered: the root is a defect in the compiler's own decode rather than a question of which caller owns it. (a) arg_value_node stays, and the divergence becomes STATED per DESIGN section 3b instead of unstated. The annotation names v2.compiler.body_lowering_fold body_lower_named_arg_value_optional as the authority it diverges from, gives the reason by symbol -- body_lower_operand_ref_optional recurses into pair.left ALONE on a sequence operand, so `left: seed + acc` returns the operand for `seed` and drops `acc` -- and states the trigger: when that accessor preserves the full sequence, arg_value_node DISSOLVES INTO IT and this annotation deletes with it. Consuming the authority as it stands would reintroduce exactly the under-approximation review 64393 caught, so the two functions answer different questions today. (b) gunbc.recurring_failure_mode.lowering_accessor_collapses_a_sequence_operand is filed for the class: a lowering accessor that silently narrows a multi-element operand to its first element, with no refusal and nothing counted. Specimen `left: seed + acc`. Rung found at BELOW THE FLOOR because the loss is silent -- an operand replaced by a proper part of itself is neither refused nor recorded. Ceiling structurally guaranteed and reachable: the narrowing has no constructor once the accessor returns a shape that can represent a multi-element operand. Trigger names that capability, and explicitly not a diagnostic, a counter, or a second accessor beside it. The receipt worth keeping is in the row: TWO INDEPENDENT IMPLEMENTATIONS of "the argument's value" -- the compiler's operand reader and this lens's first-match DFS -- converged on the same wrong answer, which is the evidence that the defect is in the shared fact rather than in either caller. And no fixture in the suite could see it, because every one used a single-identifier argument, where "first element" and "whole operand" agree. The compiler-side repair is its own lane: body_lowering_fold is a load-bearing pipeline file, so it was raised rather than improvised here, and this row is its brief. Gate module re-verified after the edit: 4/4 PASS. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01H2w1vtH78R73h7qyTK7Ah6 --- ...g_accessor_collapses_a_sequence_operand.dag | 18 ++++++++++++++++++ .../complexity_accumulator_copy/analyze.dag | 18 ++++++++++++++++++ 2 files changed, 36 insertions(+) create mode 100644 dag/gunbc/recurring_failure_mode/lowering_accessor_collapses_a_sequence_operand.dag diff --git a/dag/gunbc/recurring_failure_mode/lowering_accessor_collapses_a_sequence_operand.dag b/dag/gunbc/recurring_failure_mode/lowering_accessor_collapses_a_sequence_operand.dag new file mode 100644 index 00000000000..d3f1d0408de --- /dev/null +++ b/dag/gunbc/recurring_failure_mode/lowering_accessor_collapses_a_sequence_operand.dag @@ -0,0 +1,18 @@ +module gunbc.recurring_failure_mode.lowering_accessor_collapses_a_sequence_operand + +import std.types { NonEmptyStr } +import gunbc.recurring_failure_mode { RecurringFailureMode } + +data lowering_accessor_collapses_a_sequence_operand: RecurringFailureMode = RecurringFailureMode { + identity: "lowering_accessor_collapses_a_sequence_operand" as NonEmptyStr, + + receipts: [ + "a lowering accessor that silently narrows a MULTI-ELEMENT operand to its first element: the caller asks what an argument is and receives a proper part of it, with no refusal and nothing counted, so every consumer downstream reasons about a subset of the program the source actually wrote (DESIGN section 5 -- a failure arm must refuse, never widen)", + "SPECIMEN AND SYMBOL, 2026-09-12. `v2.compiler.body_lowering_fold` `body_lower_operand_ref_optional`, reached from `body_lower_named_arg_value_optional` via `body_lower_arg_operand_optional`: on a node that is a sugar sequence pair it recurses into `pair.left` ALONE. For the argument `left: seed + acc` it returns the operand for `seed` and drops `acc` entirely. The narrowing is unconditional and unreported -- no diagnostic, no counter, no typed arm distinguishing `this is the whole operand` from `this is the first of several`.", + "HOW IT SURFACED, WHICH IS THE PART WORTH KEEPING: not in the compiler, but in a CONSUMER that happened to need the whole answer. The accumulator-copy lens censuses the identifiers an argument mentions. Its first repair reached the same shape by a different route (a first-match DFS for the argument's first `^dag_surface_primary_expr`) and inherited the identical narrowing, which review 64393 caught: `left: seed + acc` censused as `[seed]`, one identifier, so a `BindsFresh` `seed` resolved the port to `PortPureLiteral` and a COPIED ACCUMULATOR CLASSIFIED CLEAN with the carrier invisible. Two independent implementations of `the argument's value` converged on the same wrong answer, which is the evidence that the defect is in the shared fact rather than in either caller.", + "WHY NO EXISTING WITNESS HELD IT, stated as a property of the corpus: every fixture in the accumulator-copy suite used a single-identifier or single-call argument, where narrowing to the first element and returning the whole operand agree. The class is only observable at arity two or more on one port, and nothing in the suite wrote that until the review asked for it. A collapse that is invisible on every fixture in the suite is not a tail case -- it is an unexercised axis.", + "RUNG FOUND AT: below the floor, because the loss is SILENT -- `values inhabit declared types` and `applications bind in exact bijection` are floor sentences, and an operand silently replaced by a proper part of itself is neither refused nor recorded. CEILING: structurally guaranteed, and reachable -- the operand carrier cannot be narrowed without a typed refusal once the accessor returns a shape that can represent a multi-element operand, at which point dropping an element has no constructor. NEXT-RUNG TRIGGER, NAMING THE CAPABILITY: `body_lower_named_arg_value_optional` preserves the full sequence an argument names, so a caller asking for an argument's value receives all of it or a located refusal -- not its first element. A diagnostic variant, a counter, or a second accessor beside it retires nothing; the narrowing itself must become unwritable. When it lands, `v2.lens.complexity_accumulator_copy.analyze` `arg_value_node` dissolves into that accessor and its stated-divergence annotation deletes with it.", + ], + + evidence: [], +} diff --git a/src/v2/lens/complexity_accumulator_copy/analyze.dag b/src/v2/lens/complexity_accumulator_copy/analyze.dag index 7498eea0548..63320ede281 100644 --- a/src/v2/lens/complexity_accumulator_copy/analyze.dag +++ b/src/v2/lens/complexity_accumulator_copy/analyze.dag @@ -148,6 +148,24 @@ fn arg_value_symbol(arg_capture: Node) -> Optional { } } +// A STATED DIVERGENCE FROM THE COMPILER'S OWN NAMED-ARGUMENT ACCESSOR (DESIGN section 3b), not an +// unstated fork. v2.compiler.body_lowering_fold body_lower_named_arg_value_optional decodes the same +// `name ^dag_token_colon value` spine and is the authority for what a named argument IS, so this +// function should consume it and does not. THE REASON IS A DEFECT IN THAT ACCESSOR, NAMED BY SYMBOL: +// it finishes through body_lower_arg_operand_optional into body_lower_operand_ref_optional, which on +// a sequence operand recurses into pair.left ALONE. For `left: seed + acc` that returns the operand +// for `seed` and drops `acc` -- an under-approximation of the identifiers the argument names, which +// is precisely the reading review 64393 caught in the first version of this repair and the silent +// widening DESIGN section 5 forbids. Consuming the authority as it stands would reintroduce the bug +// this function exists to avoid, so the two answer different questions today: that accessor answers +// what operand an argument LOWERS TO, this one answers what the argument's VALUE SUBTREE is. +// +// The class is filed at gunbc.recurring_failure_mode.lowering_accessor_collapses_a_sequence_operand, +// and the compiler-side repair is its own lane because body_lowering_fold is a load-bearing pipeline +// file. TRIGGER: when body_lower_named_arg_value_optional preserves the full sequence rather than +// narrowing to its first element, this function DISSOLVES INTO IT -- arg_value_node deletes and +// arg_value_mentions censuses whatever that accessor returns. Until then the divergence is stated +// here rather than argued in a review thread. fn arg_value_node(arg_capture: Node) -> Node { match sequence_left_node(cap: arg_capture) { Absent => arg_capture From 7ebc865ea73db08cad9391b339bb52798a886c1c Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 12 Sep 2026 07:21:17 +0000 Subject: [PATCH 08/11] Attribute the gate's green to two edits, not one, and cite the cell that proves it Review 64439 is correct. The receipt paragraph I added attributed gate_red_quadratic_rejects's green entirely to the analyzer repair, but this PR also re-points the discriminating specimen, and on the OLD specimen the carrier sat on the NON-copied port -- gunbc#11019 moved list_append's copied port to the right operand -- so the analyzer repair alone could not have minted a suspect. The two edits are jointly, not severally, sufficient, and claiming otherwise is the rung inflation DESIGN section 4b(1) forbids: a rung measured on a path the evidence does not establish. The deleted admission row named this exact hazard -- "deliberately NOT keyed on this witness greening, since editing the specimen or the control would green the witness without the capability" -- so the burden is to show the specimen edit is not what greened it. That evidence already existed in this PR and the annotation failed to state it, which is the defect: the measurement was made, and the authority carrying the claim did not carry the measurement. The annotation now names the three cells. The one that matters is the corrected specimen on the PRE-FIX seed, origin/main with only the .root repair and this PR's lens change absent: there gate_red_quadratic_rejects FAILS, with gate_green_identity_accepts_clean passing beside it as the control for planning. So editing the specimen alone does NOT green the witness -- the route the row excluded is refuted by execution rather than by assurance. Corrected specimen WITH the lens repair passes; old specimen with the lens repair cannot, by the copied-port citation. The capability is what closes the gap between the first cell and the second, which is the trigger discharged on its own terms rather than by a fixture edit. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01H2w1vtH78R73h7qyTK7Ah6 --- dag/gunbc/v2_compile_obligation_census.dag | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/dag/gunbc/v2_compile_obligation_census.dag b/dag/gunbc/v2_compile_obligation_census.dag index 976f882c9ca..75df6dcc998 100644 --- a/dag/gunbc/v2_compile_obligation_census.dag +++ b/dag/gunbc/v2_compile_obligation_census.dag @@ -484,6 +484,25 @@ fn witness_subject(entry: String, function: String, module_path: String) -> Witn // 4b(4)). The sentence above is left standing rather than reworded because it was true when // written and is the reason this paragraph exists. // +// TWO EDITS ARE JOINTLY SUFFICIENT HERE, NOT ONE, AND THE ADMISSION ROW NAMED THIS EXACT HAZARD -- +// "it is deliberately NOT keyed on this witness greening, since editing the specimen or the control +// would green the witness without the capability." The same change also re-points the specimen, +// because gunbc#11019 moved `list_append`'s copied port from the left operand to the right (the +// concat realization copies the appended side; `v2.std.fn_index` records that `v1_rt::rc_list_concat` +// make_muts the left and clones the right). On the OLD specimen the carrier sat on the NON-copied +// port, so the analyzer repair alone could not have minted a suspect. Attributing the green to the +// repair alone would therefore be the rung inflation section 4b(1) forbids, measured on the wrong +// path. +// +// WHAT DISCHARGES THE HAZARD IS A THREE-CELL MEASUREMENT, not the assurance above, and the cell that +// matters is the one the admission row feared. Corrected specimen on the PRE-FIX seed -- origin/main +// carrying only the `.root` repair, this PR's lens change absent -- `gate_red_quadratic_rejects` +// FAILS, with `gate_green_identity_accepts_clean` passing beside it. So EDITING THE SPECIMEN ALONE +// DOES NOT GREEN THE WITNESS: the route the row excluded is refuted by execution rather than by +// promise. Corrected specimen WITH the lens repair passes. Old specimen with the lens repair cannot +// pass, by the copied-port citation above. The capability is what closes the gap between the first +// cell and the second, which is the trigger discharged on its own terms. +// // WHAT HOLDS THE RUNG DOWN IS A DIFFERENT POPULATION, NOT THE REPAIRED ONE, which is why restoring // on the strength of the repair would be the inflation DESIGN section 4b(1) names. That section // takes the MINIMUM across a class's in-scope paths, and From 47e00f633aead89ff909105f6b554336ab7675b5 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 12 Sep 2026 08:28:44 +0000 Subject: [PATCH 09/11] Retire the consumed gunbc#11137 wave-admission row, clearing it for every branch Operator ruling (eager-raven-113): delete main's stale gunbc#11137 admission row in the same push. It is a permission standing over nothing, and the cost is fleet-wide rather than local -- required-witnesses-floor refuses namespace-wave-admission on every PR carrying it, and gunbc#11082, gunbc#11121, gunbc#11154 and this branch each burned a floor on it. THE ROW'S OWN TRIGGER IS WHAT FIRED, so this is the designed dissolution rather than housekeeping on another lane's entry. Its doc comment recorded the condition in advance -- "this row goes when #11137 merges. The base then carries the named import, the delta stops being producible, and CONSUMED comes due on the roster's next touch." #11137 merged at 06:35, and the roster's own rule charges the next change that touches it, which is this one. The module states the same law twice: "a row matching no delta refuses as stale, so the roster can only shrink toward" its resting state, and "any absorbed or vanished delta makes required CI red until that row is removed". The deletion follows the file's own ledger convention rather than inventing one: the THIRTY-FIFTH entry deleted three consumed rows "and their description with them", so this appends a THIRTY-SIXTH entry naming the trigger that fired and the branches that paid for it, and removes the row-specific rationale with the row. NAMESPACE_TRANSITION_ADMISSIONS returns to the EMPTY enumeration that is its resting state -- empty is not permissive, and a run with any delta no row names still refuses it as UNADJUDICATED. Nothing else in the file changes. Verified: cargo fmt --all --check clean, and cargo check -p v1-compiler --lib Finished with no errors. I had declined to make this deletion unilaterally when it first blocked this branch: it is another lane's row in the v1 seed, and the obligation is specified to come due on a roster-touching change rather than on any PR that happens to be blocked by it. It is made here on an explicit ruling, with the fleet-level evidence that it was blocking four branches. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01H2w1vtH78R73h7qyTK7Ah6 --- src/v1/stage0/src/namespace_wave_admission.rs | 65 ++++--------------- 1 file changed, 11 insertions(+), 54 deletions(-) diff --git a/src/v1/stage0/src/namespace_wave_admission.rs b/src/v1/stage0/src/namespace_wave_admission.rs index a12de01876b..87e188e774d 100644 --- a/src/v1/stage0/src/namespace_wave_admission.rs +++ b/src/v1/stage0/src/namespace_wave_admission.rs @@ -1715,60 +1715,17 @@ pub struct TransitionAdmission { /// is that touch, so the debt is paid here rather than inherited by an unrelated lane. Their /// TRIGGER, recorded at the time as "these rows go when #11071 merges", is what fired. /// -/// gunbc#11137 sha256sum names Filesystem instead of reaching it (2026-09-12). The row below is a -/// DIFFERENT delta that this change produces, not that one restored: empty is the resting state -/// and one change authoring a row back into it is the ordinary motion. -/// -/// WHAT THE CHANGE DID. `extdeps.tools.sha256sum` called `Filesystem.Write` while importing -/// `extdeps.filesystem.filesystem_io` with NO name list. A bare module import drags the whole -/// module into the candidate set for every name it declares, so filesystem_io's copy of -/// `extdeps_external_authority_anchor` -- the per-module convention row some 315 modules each -/// author -- was a candidate at this site. The import now names `{ Filesystem }`. -/// -/// WHY `TargetChanged` IS THE CORRECT CLASSIFICATION. The spelling is authored on both sides and -/// what moved is which declarations it admits: base `{extdeps.filesystem.filesystem_io, -/// extdeps.shell, extdeps.tools.sha256sum}`, head `{extdeps.shell, extdeps.tools.sha256sum}`. -/// -/// WHAT MAKES IT SAFE TO ADMIT, adjudicated rather than asserted. NO RESOLUTION CHANGES. -/// `extdeps.tools.sha256sum` authors its own `extdeps_external_authority_anchor`, and a module's -/// own declaration wins inside the authored region, so the site resolved to sha256sum's row at the -/// base and resolves to sha256sum's row at the head -- the removed candidate could not have won -/// either way. What narrowed is the SET, from three modules to two, which is the qualification's -/// whole purpose: the resolution stopped depending on a module the author never named. That no -/// consumer changed behaviour is the required floor's verdict on this head, re-derived by -/// `claim_executor --required-ci --source-root dag --source-root src/v2 --required-lane witnesses` -/// and read off its own `required-floor:` verdict line -- named rather than transcribed, because a -/// copied count rots without anyone touching either end (DESIGN §6). -/// -/// WHY THE `String` REQUALIFICATION IN THE SAME CHANGE NEEDS NO ROW, which is a fair question to -/// ask of a diff that moves ten import lines onto `std.string_type`. It is not this adjudication's -/// assertion; it is the wave phase's own measurement. That phase compares the binding table on both -/// sides, and on this head it reported exactly ONE `TargetChanged binding` delta -- the row below -- -/// and none for `String`. The ten `String` sites appear instead as -/// `ExplicitlyEvaluatedZeroDelta membership -> std.string_type ... reached by a name this -/// module authors`: explicitly evaluated, zero delta. The reason is that `std.types` declares no -/// `String` at all, so `import std.types { String }` bound nothing and the read fell through to the -/// shared slot, where scope precedence already answered `std.string_type`. Naming that module -/// changes the read's AUTHORIZATION -- from an accident of precedence to something the author -/// wrote -- without changing which declaration answers it. A delta row adjudicates a changed -/// binding; there is no changed binding here to adjudicate. -/// -/// TRIGGER: this row goes when #11137 merges. The base then carries the named import, the delta -/// stops being producible, and CONSUMED comes due on the roster's next touch. -pub const NAMESPACE_TRANSITION_ADMISSIONS: &[TransitionAdmission] = &[TransitionAdmission { - label: "gunbc#11137 extdeps.tools.sha256sum names Filesystem instead of reaching it", - // The rationale, the safety adjudication and the trigger are in the doc comment on this - // const rather than repeated here. In one line: the bare `import - // extdeps.filesystem.filesystem_io` became `{ Filesystem }`, which narrowed this - // spelling's candidate set without changing what it resolves to. - subject: AdmissionSubject::Binding { - module: "extdeps.tools.sha256sum", - in_declaration: "extdeps_external_authority_anchor", - spelling: "extdeps_external_authority_anchor", - target: "extdeps.tools.sha256sum", - }, - disposition: NamespaceDeltaDisposition::TargetChanged, -}]; +/// THIRTY-SIXTH DISSOLUTION (2026-09-12, gunbc#11142). The `gunbc#11137 extdeps.tools.sha256sum +/// names Filesystem instead of reaching it` row is deleted and its description with it. #11137 +/// merged, so the base carries the named import, the delta stopped being producible, and the row +/// matched no delta on any branch that carried it -- the required floor refused +/// namespace-wave-admission on gunbc#11082, gunbc#11121, gunbc#11154 and this branch for exactly +/// that reason, which is the cost of a permission standing over nothing. Its TRIGGER, recorded at +/// the time as "this row goes when #11137 merges", is what fired; this change is the roster +/// toucher the rule charges, so the debt is paid here rather than inherited by the next unrelated +/// lane. The roster returns to the EMPTY enumeration that is its resting state: empty is not +/// permissive, and a run with any delta no row names still refuses it as UNADJUDICATED. +pub const NAMESPACE_TRANSITION_ADMISSIONS: &[TransitionAdmission] = &[]; /// The denominators a green must name (DESIGN §5): a run that cannot say what it covered is an /// instrument failure wearing coverage's clothes. From 396f0260a571e50d6cdeea6fa35cd9315f32c510 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 12 Sep 2026 08:56:09 +0000 Subject: [PATCH 10/11] Enrol the discriminating red, re-point the planted control, name the binding trigger Three findings from reviews 64460 and 64473, all correct, all mine. 1. THE REPAIR HAD NO ENROLLED RED (review 64460). Every re-pointed fixture is a single-identifier or single-call value on the copied port -- the shapes where the search census this repair replaced and the spine walk AGREE -- so reverting arg_value_mentions to search left the whole suite green and restored the silent fail-open. A fix whose mutation reds nothing is not enrolled evidence (DESIGN section 5: a discriminating input that goes red when the behavior is wrong). The cell is carried by the witness that already owns this subject rather than by a new identity: a new test fn in this offline home would need roster growth, which the monotonicity gate refuses, or a false expect-red admission. Witness count is unchanged at 21. MY FIRST ATTEMPT AT THAT CELL WAS DECORATION AND THE MUTATION CONTROL IS WHAT CAUGHT IT. It used `let seed = 0` with `right: seed + acc` and asserted has_refusal_cause(computed_argument). The CENSUS does differ -- measured on both trees, port 1 reads [seed, acc] under navigation and [seed] under search, with the carrier vanishing -- but another site in that snippet contributes ^copied_port_computed_argument anyway, so the assertion passed under BOTH readings. A true claim asserted through a channel blind to it. The shipped cell drops the binder: list_append(left: x, right: x + acc). The two readings then disagree about WHICH CAUSE fires rather than whether anything fires -- ^copied_port_name_may_alias under search, where the bare-name arm reads `x` and `x` is no carrier, and ^copied_port_computed_argument under navigation, where both operands are seen -- so asserting the presence AND the absence makes both conjuncts flip. Measured: PASS on this tree, FAIL under a worktree reverting arg_value_mentions to the search census, with the roster holding at 17 PASS and the 4 declared ExpectAssertionFalse rows. 2. A RED THAT COULD NOT FIRE (review 64473). I re-pointed the long-home fixtures to the copied-right axis and left test/fixture_roots/complexity_accumulator_copy/ planted_copy.dag and the roster gate's planted_copy_snippet on `left: acc, right: x` -- the axis gunbc#11019 retired. red_control_planted_copy_still_alarms asserts SuspectObserved, which that specimen can no longer produce, so it was enrolled evidence incapable of alarming. Both re-pointed, with the reason recorded beside the snippet. Same defect class as finding 1, twice in one PR. 3. TRIGGER GRAIN MISMATCH (review 64473). The annotation claimed the restoration condition was REPLACED by fold-domain totality while next_trigger still named only affordability and the native door -- prose asserting one climb and the machine field encoding another, which is how a rung later gets restored on the wrong evidence (DESIGN 4b(3)). next_trigger now names fold-domain totality FIRST, as the binding capability under 4b(1)'s minimum-across-paths, with the other two after it. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01H2w1vtH78R73h7qyTK7Ah6 --- dag/gunbc/v2_compile_obligation_census.dag | 2 +- .../accumulator_copy_roster_gate_test.dag | 8 +++++- .../accumulator_copy_fold_analysis_test.dag | 28 +++++++++++++++++++ .../planted_copy.dag | 2 +- 4 files changed, 37 insertions(+), 3 deletions(-) diff --git a/dag/gunbc/v2_compile_obligation_census.dag b/dag/gunbc/v2_compile_obligation_census.dag index 75df6dcc998..2fd80785d21 100644 --- a/dag/gunbc/v2_compile_obligation_census.dag +++ b/dag/gunbc/v2_compile_obligation_census.dag @@ -550,7 +550,7 @@ data accumulator_copy_obligation: V2CompileObligation = V2CompileObligation { ), ], ceiling: StructurallyGuaranteed, - next_trigger: climbs_when(capability: "TWO CAPABILITIES, AND NEITHER IS A FILE MOVE. First, the gate's own witnesses become affordable on the per-PR fold so the gunbc.ci_layer_roots witness_exclusion_frontier patterns 'claim/complexity/accumulator_copy_roster_gate' and 'test/claim/long/' retire on their own dissolution conditions rather than being edited around — the exclusion rows exist because the walks were priced out, so the trigger is the cost, not the pattern. Second, the native lane enters the door. Until the first lands no required run refuses on a copied-accumulator tree; until the second lands the executed rung stays Mitigatable however green the interpreted side becomes"), + next_trigger: climbs_when(capability: "THREE CAPABILITIES, AND NONE IS A FILE MOVE. First, THE LENS OBSERVES EVERY FOLD THE SOURCE DECLARES, AT EVERY LOWERING SHAPE a fold-family call can take — a step passed BY NAME lowers to neither a substrate Loop nor a surviving surface fold call, so count_fold_sites reports 0 and the lens never sees the site to refuse about, its own ^fold_accumulator_unread arm standing as unreachable code (gunbc.recurring_failure_mode fold_shape_visible_to_no_lens). A copied accumulator inside such a fold is admitted in silence however well the named-argument path reads, so this is the capability that holds the rung down under DESIGN section 4b(1)'s minimum-across-paths and it is named FIRST because it is the binding one. Second, the gate's own witnesses become affordable on the per-PR fold so the gunbc.ci_layer_roots witness_exclusion_frontier patterns 'claim/complexity/accumulator_copy_roster_gate' and 'test/claim/long/' retire on their own dissolution conditions rather than being edited around — the exclusion rows exist because the walks were priced out, so the trigger is the cost, not the pattern. Third, the native lane enters the door. Until the first lands a whole population of folds is outside the wall entirely; until the second lands no required run refuses on a copied-accumulator tree; until the third lands the executed rung stays Mitigatable however green the interpreted side becomes"), seed_escape: SeedEscapeOpen { what_the_seed_does: "the seed's own folds are never presented to this gate, so a copied accumulator authored in stage0 Rust is invisible to the complexity lens that exists to make it unwritable" as NonEmptyStr }, diff --git a/src/v2/test/claim/complexity/accumulator_copy_roster_gate_test.dag b/src/v2/test/claim/complexity/accumulator_copy_roster_gate_test.dag index b8af976a3d9..7ea839e0f77 100644 --- a/src/v2/test/claim/complexity/accumulator_copy_roster_gate_test.dag +++ b/src/v2/test/claim/complexity/accumulator_copy_roster_gate_test.dag @@ -44,7 +44,13 @@ test fn roster_lens_cost_model_zero_suspects_within_ratchet() -> Bool { test fn roster_std_algebra_zero_suspects_within_ratchet() -> Bool { file_gate(path: "src/v2/std/algebra.dag", refusal_ceiling: 3) } -data planted_copy_snippet: String = "module planted\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) { list_append(left: acc, right: x) })\n}\n" +// THE PLANTED COPY SITS ON THE COPIED PORT, WHICH IS THE RIGHT OPERAND. gunbc#11019 repointed +// list_append's copied-port citation when the concat realization landed -- v2.std.fn_index records +// that v1_rt::rc_list_concat make_muts the LEFT and clones the RIGHT -- so `left: acc, right: x` +// copies only x per step and is LINEAR. A planted defect written on that axis can no longer mint a +// Poly2Suspect, and this control asserts SuspectObserved, so it would have been a red that cannot +// fire: enrolled as evidence and incapable of alarming (DESIGN section 4b(4), section 5). +data planted_copy_snippet: String = "module planted\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) { list_append(left: x, right: acc) })\n}\n" // ASSERTED AS *SUSPECT OBSERVED*, NOT AS "NOT CLEAN". Those differ on exactly the state this change // exists for: a subject the lens could not read is neither clean nor suspect, and a control written diff --git a/src/v2/test/claim/long/accumulator_copy_fold_analysis_test.dag b/src/v2/test/claim/long/accumulator_copy_fold_analysis_test.dag index d2354c6a4e1..43df5e8c644 100644 --- a/src/v2/test/claim/long/accumulator_copy_fold_analysis_test.dag +++ b/src/v2/test/claim/long/accumulator_copy_fold_analysis_test.dag @@ -19,6 +19,8 @@ data nested_call_snippet: String = "module nested\n\nfn f(xs: List) -> Int data unregistered_combiner_snippet: String = "module unreg\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) { mystery_op(a: acc, b: x) })\n}\n" +data compound_copied_port_snippet: String = "module compound\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) { list_append(left: x, right: x + acc) })\n}\n" + data out_of_iteration_snippet: String = "module once\n\nfn f(xs: List, ys: List) -> Int {\n list_append(left: xs, right: ys)\n}\n" data named_step_snippet: String = "module namedstep\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: step)\n}\n" @@ -132,12 +134,38 @@ test fn let_unknown_alias_still_refuses_may_alias() -> Bool { } } +// THE DISCRIMINATING RED FOR THE ARGUMENT-VALUE CENSUS, carried by the witness that already owns +// this subject rather than by a new identity. Both cells assert the same law -- a copied port +// holding a COMPUTED expression must not read as a bare name -- and the second is the one no +// fixture in this suite could express before: a compound value, `seed + acc`, where a FRESH binder +// and the CARRIER share one port. +// +// WHY THE SECOND CELL IS NOT REDUNDANT WITH THE FIRST, AND WHY IT ASSERTS BOTH A PRESENCE AND AN +// ABSENCE. Under the search-based census this repair replaced -- first-match +// `^dag_surface_primary_expr`, which stops at the leftmost operand because dag_surface_binary_expr +// sits ABOVE primary_expr -- `right: x + acc` censuses as ONE identifier and the bare-name arm +// fires on `x`, which is not a carrier, so the port refuses ^copied_port_name_may_alias. Under the +// spine walk it censuses BOTH operands and refuses ^copied_port_computed_argument. The two readings +// therefore disagree on WHICH CAUSE, not on whether anything refuses, which is why asserting the +// presence alone would not discriminate: measured, the first draft of this cell used a `let seed = +// 0` binder and PASSED UNDER BOTH READINGS, because another site in that snippet contributes +// ^copied_port_computed_argument anyway and the assertion could not see the port it was about +// (review 64460 asked for the red; the mutation control is what showed the first attempt was +// decoration). Every other fixture here is a single-identifier or single-call value -- the shapes +// where search and the spine walk AGREE -- so without this cell, reverting arg_value_mentions to +// search leaves this whole file green and the silent fail-open restored. test fn nested_call_head_cannot_masquerade_as_bare_name() -> Bool { match findings_of(source_text: nested_call_snippet, file: ^nested_file) { Absent => false Present { value: fs } => v2.lens.complexity_accumulator_copy.analyze.findings_have_refusal_cause(fs: fs, cause: ^copied_port_computed_argument) } + && match findings_of(source_text: compound_copied_port_snippet, file: ^compound_file) { + Absent => false + Present { value: fs } => + v2.lens.complexity_accumulator_copy.analyze.findings_have_refusal_cause(fs: fs, cause: ^copied_port_computed_argument) + && !v2.lens.complexity_accumulator_copy.analyze.findings_have_refusal_cause(fs: fs, cause: ^copied_port_name_may_alias) + } } test fn unregistered_combiner_reached_by_carrier_refuses() -> Bool { diff --git a/test/fixture_roots/complexity_accumulator_copy/planted_copy.dag b/test/fixture_roots/complexity_accumulator_copy/planted_copy.dag index 1c2dfb08479..0bb93cde069 100644 --- a/test/fixture_roots/complexity_accumulator_copy/planted_copy.dag +++ b/test/fixture_roots/complexity_accumulator_copy/planted_copy.dag @@ -1,5 +1,5 @@ module test.fixture.complexity_accumulator_copy.planted_copy fn planted_quadratic(xs: List) -> Int { - fold(xs, init: 0, f: fn(acc, x) { list_append(left: acc, right: x) }) + fold(xs, init: 0, f: fn(acc, x) { list_append(left: x, right: acc) }) } From 18729318977c62624950bf005e5be51741f07a7e Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 12 Sep 2026 10:04:06 +0000 Subject: [PATCH 11/11] Revert the roster-gate snippet re-point: touching that file plans an over-wall witness CI on 396f026 refused with two blockers, both naming v2.test.claim.complexity.accumulator_copy_roster_gate.roster_std_algebra_zero_suspects_within_ratchet -- interrupted_before_verdict and changed_witness_planned_without_terminal_verdict. Caused by my own fix for review 64473, and the mechanism is exact rather than suspected. WHY EDITING THAT FILE IS SELF-DEFEATING. floor_diff_edits_from_line_ranges attributes changed lines to test declarations, so re-pointing the planted_copy_snippet DATA row at line 47 attributed to the test declaration immediately above it, and required_floor_disposition_with_changed_selection replaced that identity's withheld disposition with PlannedAsChangedWitness. The witness then scans src/v2/std/algebra.dag, a real corpus file, which is why its home carries the claim/complexity/accumulator_copy_roster_gate exclusion in the first place. Its identity IS in v2.workflow.floor_cost_debt floor_cost_debt_roster, so changed_witness_cost_policy returns ChangedCostDebtVerdictOnly and the CPU deadline becomes observed-only -- but as gunbc.recurring_failure_mode.claim_edit_changes_execution_policy_outside_reported_cost_delta states, WALL deadlines, semantic failures and missing cost observations still block. The declared debt covers CPU, not wall, so the interrupt stands. So the inline planted control cannot be re-pointed in this PR. Reverted to main's spelling; the CORPUS fixture re-point (test/fixture_roots/complexity_accumulator_copy/planted_copy.dag) is KEPT, because it is a different file whose edit planned nothing -- the run's blockers named only the roster-gate identity. WHAT I DID NOT DO. I did not move the data row next to a cheaper witness to steer the line-range attribution: that is editing around the mechanism rather than through it, and the roster's own authority refuses exclusion patterns being "edited around". I also did not admit the identity as expect-red, which would be false -- it is interrupted, not asserting false. The residue is real and is review 64473's finding standing unrepaired for the inline snippet: red_control_planted_copy_still_alarms asserts SuspectObserved on the axis gunbc#11019 retired, so it is a red that cannot fire, and it is also dark because its home is excluded. Both halves need the same capability -- the roster gate's witnesses becoming affordable, which accumulator_copy_obligation next_trigger already names as its second capability. Reported rather than papered over. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01H2w1vtH78R73h7qyTK7Ah6 --- .../complexity/accumulator_copy_roster_gate_test.dag | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/src/v2/test/claim/complexity/accumulator_copy_roster_gate_test.dag b/src/v2/test/claim/complexity/accumulator_copy_roster_gate_test.dag index 7ea839e0f77..b8af976a3d9 100644 --- a/src/v2/test/claim/complexity/accumulator_copy_roster_gate_test.dag +++ b/src/v2/test/claim/complexity/accumulator_copy_roster_gate_test.dag @@ -44,13 +44,7 @@ test fn roster_lens_cost_model_zero_suspects_within_ratchet() -> Bool { test fn roster_std_algebra_zero_suspects_within_ratchet() -> Bool { file_gate(path: "src/v2/std/algebra.dag", refusal_ceiling: 3) } -// THE PLANTED COPY SITS ON THE COPIED PORT, WHICH IS THE RIGHT OPERAND. gunbc#11019 repointed -// list_append's copied-port citation when the concat realization landed -- v2.std.fn_index records -// that v1_rt::rc_list_concat make_muts the LEFT and clones the RIGHT -- so `left: acc, right: x` -// copies only x per step and is LINEAR. A planted defect written on that axis can no longer mint a -// Poly2Suspect, and this control asserts SuspectObserved, so it would have been a red that cannot -// fire: enrolled as evidence and incapable of alarming (DESIGN section 4b(4), section 5). -data planted_copy_snippet: String = "module planted\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) { list_append(left: x, right: acc) })\n}\n" +data planted_copy_snippet: String = "module planted\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) { list_append(left: acc, right: x) })\n}\n" // ASSERTED AS *SUSPECT OBSERVED*, NOT AS "NOT CLEAN". Those differ on exactly the state this change // exists for: a subject the lens could not read is neither clean nor suspect, and a control written