Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
49 commits
Select commit Hold shift + click to select a range
776206c
Total fold-step lowering: an arrow-lambda step reaches the same seam …
Sep 13, 2026
42e5937
Row receipts: the arrow half closes, the row narrows to by-name, and …
Sep 13, 2026
dc6e7ab
Merge remote-tracking branch 'origin/session/still-bee-353' into sess…
Sep 13, 2026
f15871a
By-name fold steps: the DFS finds the site erased before any lens run…
Sep 13, 2026
a5f5585
Read the step form at the step ARGUMENT, not across the whole fold-ca…
Sep 13, 2026
6dc1930
Row: the search grain is this class's worse half, and the first cut a…
Sep 13, 2026
bac8d5f
Preserve call callee and argument edges through v2 body lowering.
Sep 13, 2026
f48cbec
Count imported-callee call sites after normalize, not declaration names.
Sep 13, 2026
a7db456
Make the named-edge census a call-site delta; add same-module decl co…
Sep 13, 2026
76fb593
Admit call-forward standing without a one-arm coproduct; pass NonEmpt…
Sep 13, 2026
03b0a21
The nested positive control is a plain fn: a newly enrolled ingest-re…
Sep 13, 2026
fbe971b
One named-argument decoder, at the layer that owns the production (re…
Sep 13, 2026
2706c84
Do not treat brace or comma tokens as call callee or argument values.
Sep 13, 2026
fcd4e6d
Merge remote-tracking branch 'origin/main' into session/deep-newt-301
Sep 13, 2026
bb54b46
Stop treating comma as infix and stop taking the right of a comma-pai…
Sep 13, 2026
879bcaf
Merge remote-tracking branch 'origin/session/still-bee-353' into sess…
Sep 13, 2026
07f58a0
Restore call_args_include_punct after inserting call_arg_identity_at.
Sep 13, 2026
8ca512b
Controls for the step-slot read in the other direction: a lambda in a…
Sep 13, 2026
b2e3d36
Delete the dangling call-forward DeclarationRef roster.
Sep 14, 2026
975101f
State where the positive evidence executes: claim_batch and no lane, …
Sep 14, 2026
c12e5fe
Keep the callee when the body is a primary_expr wrapper, and keep the…
Sep 14, 2026
021ca90
Declare the drop: the accumulator-copy lens's positive controls execu…
Sep 14, 2026
935abba
Do not treat a nested init literal or a closing brace as the body call.
Sep 14, 2026
7995aea
Close the producer call-shape table before any T freeze.
Sep 14, 2026
51907f5
fold_family_head derives from the step-slot roster instead of restati…
Sep 14, 2026
66b67bf
Keep the trailing named fold step and Loop-first on let remainders.
Sep 14, 2026
dd2ce73
Propagate fold-loop Rejected on the primary/postfix producer path.
Sep 14, 2026
012911a
Walk the full comma-list Repeat when collecting call arguments.
Sep 14, 2026
04251a9
Lower infix operands as expressions so a piped call keeps its arguments.
Sep 14, 2026
936473b
Delete the commentary String row; pin the must-refuse on the executin…
Sep 14, 2026
a32f4b1
Record the interpreter partial climb; leave native as the class rung.
Sep 14, 2026
b3ecc4f
One call-spine walker; close the shape table by identity not a count.
Sep 14, 2026
6ecb16d
Close the producer-shape table against reflected coproduct arms.
Sep 14, 2026
43edca7
Propagate nested body-lowering Rejected through call args and match a…
Sep 14, 2026
e184d7b
Match Outcome on infix lowering at its consumers.
Sep 14, 2026
0bf6754
Unify search_call_named's Optional arms.
Sep 14, 2026
f143176
Classify call-structure delimiters from the dag lex roster.
Sep 14, 2026
5ca4a43
Drop the new call-preservation witness file off the enrolment gate.
Sep 14, 2026
e099b99
Re-enroll filing call shapes on existing projection-call identities.
Sep 14, 2026
b6aa5ca
Split filing-shape call preservation onto named identities.
Sep 14, 2026
9b38e76
Retarget sequence-operand citations after the named-arg accessor rewr…
Sep 14, 2026
b561123
Drop the deleted operand-peel identifier from remaining prose.
Sep 14, 2026
9fa8f61
Fold filing-shape call checks into the existing projection-normalize …
Sep 14, 2026
a447c47
Merge remote-tracking branch 'origin/main' into session/deep-newt-301
Sep 14, 2026
c9c02cb
Merge remote-tracking branch 'origin/session/zesty-fox-514' into sess…
Sep 14, 2026
b8e47f2
The by-name fold site is visible to the complexity lens: counted and …
Sep 14, 2026
876fbe2
Drop a body-grain annotation: §4c admits leading module-item blocks only
Sep 14, 2026
9d0a7d0
Merge remote-tracking branch 'origin/main' into session/deep-newt-301…
Sep 14, 2026
bce7eb8
The four greened witnesses are plain fns in the drop's population: ne…
Sep 14, 2026
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
14 changes: 3 additions & 11 deletions dag/gunbc/explicit_witness_admission.dag
Original file line number Diff line number Diff line change
Expand Up @@ -403,19 +403,11 @@ data explicit_witness_admissions: List<ExplicitWitnessAdmission> = [
),
known_red_probe(
entry: "src/v2/test/claim/long/accumulator_copy_fold_analysis_test.dag",
f: "named_step_fold_refuses_accumulator_unread",
f: "declared_named_step_fold_copy_is_caught",
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")
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: "the first of the two capabilities this row named has fired (gunbc#11322: the by-name call reaches the normalized tree as Transform [ fold, xs, 0, step ]) and the lens now counts the site and refuses ^fold_accumulator_unread at it, which retired its two weaker sibling rows. What remains is a NEW sub-capability the site exposed: the lowered call envelope carries its named actuals positionally with the labels erased, so which operand fills the callee's step slot is not a fact the tree carries -- named actuals visible to v2.std.node_query's call envelope is its own admission (zesty-fox-514, 2026-09-14), and then 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",
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -9,21 +9,25 @@ data call_expression_erased_at_v2_body_lowering: RecurringFailureMode = Recurrin
receipts: [
"**a call expression is erased by v2 normalize before resolve runs, so every reference it carries -- callee and arguments -- is invisible to name resolution and the refusal a missing declaration should raise has nothing to fire on** (INVALID STATE: v2.compiler.normalize, via v2.compiler.body_lowering_fold, lowers a function body that is a call into a Transform node whose only child is the `dag_token_lbrace` atom. The callee identity and every argument subtree are dropped. The module then passes normalize and resolve Accepted, with no diagnostic of any severity).",

"HARM. v2 name resolution fails OPEN for the whole call-expression population, declared and undeclared alike. A call to a name no declaration provides is Accepted. The namespace cut's census rests on a delete-first premise, that removing an authority makes every real dependent REFUSE LOUDLY, and that premise is void for every dependent reached through a call. For the observed call shapes, erasure prevents the missing-callee resolution refusal from firing. Consequently a refusal roster cannot establish completeness of affected call dependents from absence of refusals. The affected population has not been established by these receipts. Native census mode separately performs no resolution and therefore cannot establish binding-refusal completeness. A native run with no passing call-bearing identities does not by itself identify lowering as the cause of every refused identity.",
"HARM. v2 name resolution failed OPEN for the whole call-expression population while lowering dropped the call: a name no declaration provides was Accepted. The namespace cut's census rests on a delete-first premise, that removing an authority makes every real dependent REFUSE LOUDLY, and that premise is void for every dependent reached through an erased call. Interpreter prepared/unprepared now refuse the enrolled undeclared-callee specimen at resolve; native census mode still performs no resolution and cannot establish binding-refusal completeness. A native run with no passing call-bearing identities does not by itself identify lowering as the cause of every refused identity.",

"DISTINGUISHING FACTS, because two neighbouring rows look like this one and are not. `unresolved_callee_conflated_with_dispatched_elsewhere` is the v1 ExprCall-tail class: there the callee reaches the classifier and the miss is absorbed later. Here the callee never reaches resolve at all. And the earlier dated measurements (v2.test.claim.staged_front_end unbound_symbol_reason_note, v2.test.claim.dag_acceptance frontier_arm_note) attributed the silence to resolve. That was the wrong stage: resolve is correct over the tree it receives, and the tree has already lost the call. A wall authored in resolve would therefore be a decoration (DESIGN section 4b), because the undeclared-callee RED and the declared-callee positive control arrive as identical trees.",
"DISTINGUISHING FACTS, because two neighbouring rows look like this one and are not. `unresolved_callee_conflated_with_dispatched_elsewhere` is the v1 ExprCall-tail class: there the callee reaches the classifier and the miss is absorbed later. AT FILING (2026-09-12 interpreter dumps), the v2 callee never reached resolve at all: the earlier dated measurements (v2.test.claim.dag_acceptance frontier_arm_note, and a since-deleted staged_front_end commentary row) attributed the silence to resolve, which was the wrong stage — resolve is correct over the tree it receives, and that tree had already lost the call, so a resolve-side wall would have been a decoration because the undeclared-callee RED and the declared-callee positive control arrived as identical trees. THAT IDENTITY IS NO LONGER THE INTERPRETER FACT: those two trees now differ, and the resolve-side assertion is executing evidence rather than a decoration. Native remains unshown.",

"RECEIPT (2026-09-12, still-eagle-447, NAMESPACE XL-2 scoping). The normalized tree was dumped for five bodies via prepare_grammar, parse_module_prepared and normalize -- the calls v2.compiler.program_assembly program_assembly_read_to_normalized_root_prepared makes, and so the census route's own hand-off (v2.compiler.compile native_test_context_from_ingest). `{ k }` keeps `Atom:k`. `{ x }` over a parameter keeps `Atom:x`. `{ g(x: 1) }` with g declared, `{ zzz(x: 1) }` and `{ zzz(1) }` with zzz undeclared all become `Transform [ Atom:dag_token_lbrace ]`. The unprepared parse_module route (v2.compiler.staged_front_end run_front_end) dumps identically, so this is not a second lossy route beside a faithful one.",

"EVIDENCE LEVEL, stated so the receipt is not read one rung high. The dumps ran the v2 .dag through the gunbc interpreter at main f9d37e43a1, and a structural node-count fold (not a printer) agrees: the parse tree grows with a call's arguments and nesting, while the normalized body of { g(x: 1) } is exactly one node larger than { k } -- the Transform and its lbrace atom -- and { g(x: h(y: 5)) } is no larger than that. A second named argument adds one node, so the lowering keeps something per extra argument, but none of the callee or argument content. That the natively emitted normalize behaves identically is not executed. The native route gives no contrary evidence: its receipt on the #10940 head (eager-raven-113, 2026-09-12) holds exactly one Passed identity, a literal-bodied smoke test, and every richer body refuses before or at eval (v2.compiler.infer node_grounding_frontier_note). So no route has been observed to lower a call faithfully.",

"RUNG FOUND AT: outside the ladder -- silent wrongness. The compiler Accepts a program with an undeclared callee and reports nothing.",
"RUNG FOUND AT: the minimum across in-scope paths (DESIGN section 4b). Interpreter prepared and unprepared: mechanically preventable — undeclared callee refuses at resolve with resolve_reason_unbound_symbol, and enrolled argument-subtree controls RED if erasure is restored. Native realization of a declared argument-dependent call is not executed here, so the class rung remains that path: outside the ladder until arm (i) lands.",

"CEILING: structurally guaranteed. Whether a name is bound in the containment index is decidable, and v2 resolve already refuses an unbound VALUE name with `resolve_reason_unbound_symbol`. The missing piece is not an authority but the lowering preserving what resolve needs.",

"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.",
"PARTIAL CLIMB (2026-09-14, #11322). Interpreter prepared and unprepared now preserve enrolled call shapes. Arm (ii): undeclared callee refuses at resolve with resolve_reason_unbound_symbol (v2.test.claim.staged_front_end staged_front_end_unbound_value_name_refuses_with_its_own_reason, including undefined_callee_zzz). Arm (iii): v2.test.manual.body_lowering_projection_call body_lowering_normalize_accepts_projection_module — postfix helper.step(a, b) keeps callee step at arity 2; the same identity also normalizes `{ g(x: 1) }` and `{ g(x: h(y: 5)) }` in one extra module (two calls named g, inner h under outer g). Dedicated filing test fns were enrolment-censored at the 500ms ceiling (b561123). Restoring erasure reds that identity. Arm (i) is not delivered: a declared callee through the native route returning an argument-dependent result is unexecuted on this head.",

"NEXT-RUNG TRIGGER, naming the residual capability: a call with a DECLARED callee executes through the NATIVE route and returns the expected ARGUMENT-DEPENDENT result, so the argument subtree is carried and consumed rather than merely present on that path. Interpreter prepared/unprepared arms (ii) and (iii) do not stand in for native. A census count or a migration of known call sites does not fire this trigger.",

"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