Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
16 commits
Select commit Hold shift + click to select a range
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 24 additions & 0 deletions dag/gunbc/explicit_witness_admission.dag
Original file line number Diff line number Diff line change
Expand Up @@ -417,6 +417,30 @@ data explicit_witness_admissions: List<ExplicitWitnessAdmission> = [
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/accumulator_copy_fold_analysis_test.dag",
f: "let_prefixed_fold_copy_is_caught",
kind: CorpusWitnessKind,
budget: SubstrateLongLaneEvalBudget,
reason: "A SILENT FAIL-OPEN ONE POSITION OVER FROM THE SPECIMEN THE GATE CATCHES, AND IT IS SPELLING-INDEPENDENT. The specimen is quadratic_snippet's planted fold / list_append copy -- an fn-literal step, the very shape gate_red_quadratic_rejects refuses -- preceded by one `let seed = 0`. Measured on the tokenize / parse_module / normalize route (2026-09-13, deep-newt-301): the let lowers to a Bind whose body is a bare sequence spine with `fold` as its leftmost atom and every right projection an EMPTY Conj -- the fn literal, the arguments and the production shells are gone -- so there is no seam Loop, no surface fold call, count_fold_sites reads 0 and accumulator_copy_findings is empty. The same planted copy as the sole body statement is caught (quadratic_fold_has_suspect PASSES in the same run). So the arrow half of gunbc.recurring_failure_mode fold_shape_visible_to_no_lens closed by gunbc#11314 covers fold sites in ONE position, the sole expression of a brace body; every other position is this class. The erasure is gunbc.recurring_failure_mode call_expression_erased_at_v2_body_lowering seen from the lens's side: a lens is a pure reader, and nothing it reads carries the site. NOT FIXED HERE: the repair is that class's trigger, in v2.compiler.body_lowering_fold, a load-bearing pipeline file outside this lane's brief. Owner: the lane that fires that trigger.",
dissolution: unbound_dissolution(description: "the capability is gunbc.recurring_failure_mode call_expression_erased_at_v2_body_lowering's own trigger applied to this position -- v2 body lowering preserves a fold-family call's callee and argument subtrees when the call follows a let-binding, so the fold reaches v2.lens.complexity_accumulator_copy.analyze as a seam Loop or a surface fold call and the planted copy mints a Poly2Suspect. When it lands this assertion greens with no edit to the specimen and this row deletes in the same change. A lens-side reading of the erased spine, a diagnostic on the erasure, or a census that counts the site without classifying it retires nothing")
),
known_red_probe(
entry: "src/v2/test/claim/long/accumulator_copy_fold_analysis_test.dag",
f: "match_arm_fold_copy_is_caught",
kind: CorpusWitnessKind,
budget: SubstrateLongLaneEvalBudget,
reason: "THE SAME FAIL-OPEN AS ITS let_prefixed_fold_copy_is_caught SIBLING AT A SECOND POSITION, rostered separately because it is a separate executing assertion over a separately lowered body form. The planted fold / list_append copy sits in the `true` arm of a `match`; measured 2026-09-13 on the same route, count_fold_sites reads 0 and no finding is minted, while the identical fold as the sole body statement is caught. An `if` branch measured the same way in the same session (probe, not enrolled -- one position per row is enough to bound the class and the if-form dissolves on the same trigger). Class: gunbc.recurring_failure_mode call_expression_erased_at_v2_body_lowering, consumer-side receipt on gunbc.recurring_failure_mode fold_shape_visible_to_no_lens.",
dissolution: unbound_dissolution(description: "the same capability its let_prefixed sibling names, at the match-arm position: the fold-family call inside a match arm reaches the lens with its callee and arguments intact and the planted copy mints a Poly2Suspect. This row deletes together with the let_prefixed_fold_copy_is_caught row when the position it names is covered; neither retires on the other")
),
known_red_probe(
entry: "src/v2/test/claim/long/accumulator_copy_fold_analysis_test.dag",
f: "declared_named_step_fold_copy_is_caught",
kind: CorpusWitnessKind,
budget: SubstrateLongLaneEvalBudget,
reason: "THE CAPABILITY WITNESS FOR THE BY-NAME HALF OF gunbc.recurring_failure_mode fold_shape_visible_to_no_lens, and the answer to the DFS the row's dispatch ordered (eager-raven-113, 2026-09-13: establish whether a lens-side read of the referenced step declaration is available before proposing a Loop). The specimen declares `fn step(acc: Int, x: Int)` carrying the planted list_append copy in its own body and calls `fold(xs, init: 0, f: step)`. Measured 2026-09-13: the DECLARATION half of the read IS available at lens time -- the normalized root carries step's Arrow member with `acc` as the first named domain binding, readable by v2.std.node_query arrow_domain_named_param_bindings, and its body is a lowered Transform the lens's own lowered-call arm walks. The SITE half is not: `fold(xs, init: 0, f: step)` as the sole body statement lowers to a Transform whose operator is the dag_token_lbrace atom with `xs` and the callee dropped -- the exact shape gunbc.recurring_failure_mode call_expression_erased_at_v2_body_lowering records for `{ g(x: 1) }` -- and after a let it lowers to the argument-less spine its let_prefixed sibling records. No spelling-specific residue survives that a reader could resolve FROM; recognising the site by the shape of the erasure would be reading a defect as a fact. So candidate (B), the lens-side callee read, is BLOCKED ON THE ERASURE CLASS and not on any missing resolution primitive, and candidate (A), the seam Loop over a step reference, is fierce-lark-661's ruling to revisit and would in any case not reach the let / match / if positions. This witness asserts the capability the row names -- the by-name step's accumulator flow is visible, so the planted copy mints a suspect -- rather than the weaker ^fold_accumulator_unread refusal its named_step_fold_refuses_accumulator_unread sibling asserts, because a resolvable step with a planted copy that only REFUSES would be the lens declining a proof it has in hand.",
dissolution: unbound_dissolution(description: "two capabilities in sequence, both named: first, gunbc.recurring_failure_mode call_expression_erased_at_v2_body_lowering's trigger fires so the by-name fold-family call reaches the normalized tree with its callee and its `f: step` argument intact; second, v2.lens.complexity_accumulator_copy.analyze resolves the step reference to its Arrow member in the same root, takes the first domain binding as the carrier, and analyzes the step body under iteration -- or, where the step is not declared in the root, refuses ^fold_accumulator_unread with the site COUNTED. When both land this assertion greens with no edit to the specimen and this row deletes in the same change, together with the named_step_fold_refuses_accumulator_unread and report_counters_state_the_domain rows whose weaker assertions it subsumes. Treating an unresolved step as zero-cost, or an allow-list of step names, retires nothing")
),
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",
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,8 @@ data call_expression_erased_at_v2_body_lowering: RecurringFailureMode = Recurrin
"NEXT-RUNG TRIGGER, naming the capability: v2 body lowering PRESERVES every call expression's callee and argument subtrees into the normalized tree on every v2 route that feeds resolve, so that resolve receives the callee as a reference. The climb's evidence is executed, and resolution alone does not discharge it. The repair that fires this trigger must show, by execution: (i) a call with a DECLARED callee executes through the native route and returns the expected ARGUMENT-DEPENDENT result, so that the argument subtree is demonstrably carried and consumed rather than merely present; (ii) a call with an UNDECLARED callee refuses at RESOLVE with a typed, located missing-binding cause -- at resolve, not later at grounding, emission or eval, since a refusal arriving downstream is consistent with the callee never having reached resolve at all; (iii) controls that discriminate ARGUMENT-subtree loss specifically, over the additional-argument and nested-call shapes named above, such that restoring the erasure makes those regression assertions FAIL rather than leaving them green. An invalid specimen that is Accepted is a FAILING must-refuse assertion, not evidence of anything. The prepared and unprepared routes and the native realization are distinct evidence paths and one passing route does not stand in for the others. A resolve-side check, a census count, or a migration of known call sites does not fire this trigger, because none of them makes the call reach resolve. These are requirements on the repair's evidence, not executions owed before this row lands.",

"CENSUS CONSEQUENCE, recorded because the cut consumes it: the whole-tree native census (the emitted closure binary's census mode) runs only tokenize, parse and normalize per file and never calls resolve, so its roster carries front-end refusals only. Restoring call lowering does not by itself add resolve refusals to that census. That needs the census mode to resolve per module as well.",

"CONSUMER-SIDE RECEIPT AND A SECOND SHAPE, 2026-09-13 (deep-newt-301, dispatched on `fold_shape_visible_to_no_lens`). The same route (tokenize, parse_module, normalize) was dumped for fold-family calls, which this class also erases, and for a body that is a `let` followed by a call. `{ fold(xs, init: 0, f: step) }` and `{ g(xs, init: 0, f: step) }` both become `Transform [ Atom dag_token_lbrace, Atom dag_token_int_literal, Atom step ]`: the named-argument VALUES survive as positional operands with their labels and the callee and positional `xs` dropped, which refines the earlier receipt's `a second named argument adds one node` -- what is kept is the value atom of each named argument, not the argument. The let form is a DIFFERENT erasure shape under the same class: `{ let seed = 0 \n fold(xs, init: seed, f: fn(acc, x) { .. }) }` lowers to a Bind whose body is a bare left/right sequence spine with `fold` as its leftmost atom and every right projection an empty Conj -- here the callee SURVIVES and the arguments, including an fn literal, do not, with the production shells stripped. So the two shapes lose complementary halves and neither carries a call. THE CONSUMER THIS SILENCES beyond resolve: `v2.lens.complexity_accumulator_copy.analyze`, a required root lens at the compile door, enumerates fold sites by seam Loop or by surface fold call, and both are produced only where fold_lowering runs BEFORE this erasure -- the sole-body position. A planted quadratic after a let, in a match arm or in an if branch is Accepted with no finding, in every step spelling; enrolled RED at `gunbc.explicit_witness_admission` as `let_prefixed_fold_copy_is_caught`, `match_arm_fold_copy_is_caught` and `declared_named_step_fold_copy_is_caught` in `src/v2/test/claim/long/accumulator_copy_fold_analysis_test.dag`, each dissolving on this row's trigger. The trigger's clause (iii) gains a shape: the controls must cover the let-prefixed body, whose loss is the argument half rather than the callee half.",
],

evidence: [],
Expand Down
Loading
Loading