Skip to content

Total fold-step lowering: an arrow-lambda step reaches the same seam Loop the fn literal does - #11314

Merged
briansrls merged 5 commits into
mainfrom
session/still-bee-353
Sep 14, 2026
Merged

briansrls merged 5 commits into
mainfrom
session/still-bee-353

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Sep 13, 2026 •

Copy link
Copy Markdown
Contributor

v2.compiler.fold_lowering read ONE step production. The grammar declares two function-value productions reachable in argument position — dag_production_fn_literal (emitted ^dag_surface_fn_literal) and dag_production_arrow_lambda (emitted ^dag_surface_arrow_lambda) — and fold_call_step_fn searched for the first only. A step spelled f: (acc, x) => ... was read as "no step form present", sharing one state with a step passed BY NAME. Those are different facts: the arrow lambda's binder and body are in hand at this stage; a named step's binder is a callee-resolution fact it does not have.

Measured, one binary, both directions

Fixtures differ only in lambda spelling. Numbers came from a scratch entry point calling count_fold_sites / accumulator_copy_findings directly; the enrolled instrument that re-derives them is the committed pair planted_copy_arrow.dag + clean_linear_arrow.dag read through corpus_rows_for_paths in v2.test.claim.complexity.accumulator_copy_corpus_path_test.

reading baseline repaired
arrow_seen 0 1
arrow_bound 0 1
arrow_suspect 0 1
fn_seen / fn_bound / fn_suspect 1/1/1 1/1/1

The arrow site was invisible to the traversal, not merely unbound — a planted quadratic identical to one the gate catches was admitted in silence. Population: ~2198 arrow-form step sites across ~538 files.

The prediction that failed is part of the record. I predicted from structure that the arrow site would be SEEN-but-unbound, since recognition reads the callee head and not the lambda. It is invisible outright. Recognition is spelling-independent and the site still vanishes — that is the fact the next reader needs, and it is on the row.

The shape of the repair

A closed FoldStepForm = StepFnLiteral | StepArrowLambda | StepByName, both inline forms projecting onto the same two seam inputs through one shared fold_call_seam_from_step into the existing, already spelling-agnostic fold_call_seam_loop. No per-spelling arm at any consumer; no "unknown lambda shape is zero-cost" arm anywhere.

StepByName is a real named arm over the residue, not a fall-through — it keeps yielding the FoldCallStepFormUnresolved the seam produced before. (deep-cat-655's review condition, adopted.)

The bare acc => e form is a refusal by construction, not an omission: a fold step takes (accumulator, item), the grammar admits the one-binder form for ordinary lambdas, so reading its sole binder as an accumulator would fabricate a carrier the source never declared. The reading refuses rather than falling through to a DFS for the first plausible ident.

What this does NOT discharge

gunbc.recurring_failure_mode fold_shape_visible_to_no_lens does not retire. The row narrows: its remaining population is the by-name step alone, ~18 sites / 14 files (a floor — re-derive before quoting), bounded by the named_seen reading of count_fold_sites over named_step_snippet, which is 0 both before and after this PR.

Its trigger is stated as the capability — a by-name fold step's accumulator flow is visible to the complexity lens — not as "a Loop". Filed as its own item (node://adhoc-d517fc46-052) under eager-raven with two candidate constructions, the lens-side callee read DFS-first by ruling, since a lens is a pure reader and lowering is not changed to suit it.

A second specimen, filed on the row

No surface fold call survives normalize for any spelling:

surface fold call survives lowered Loop
fn-form no yes
arrow (baseline) no no → invisible
arrow (repaired) no yes → visible
by-name (both) no no → invisible

So the SURFACE arm of count_fold_sites is reachable on no ingest route — a permanently-green check in the §4b sense, reading as a second independent way to see a fold when it is not one. Not fixed here; filed on the row with the lens authority named as owner.

Witness placement

The A/B predicates land as plain fns, not test fns, on this file's own recorded standing: each reaches the interpreted ingest, which measures several times required_floor_claim_cpu_safety_limit_ms and would report interrupted_before_verdict. They pass by execution under claim_batch, same as their fn-form siblings. I am not calling that enrollment.

Rung honesty

Source→interpretation is what the A/B above establishes. Source→native emission is not claimed here — that is measured by the srv2 closure receipt fold, which is owed anyway since fold_lowering is a closure member. The class sits at the minimum across its paths.

🤖 Generated with Claude Code

https://claude.ai/code/session_014tbjacTtGDpN2UHpBUrfoG

gunbc-ci-auto-heal and others added 2 commits September 13, 2026 21:26
…Loop the fn literal does

v2.compiler.fold_lowering read ONE step production. The grammar declares two
function-value productions reachable in argument position -- dag_production_fn_literal
(emitted ^dag_surface_fn_literal) and dag_production_arrow_lambda (emitted
^dag_surface_arrow_lambda) -- and fold_call_step_fn searched for the first only. A step
spelled `f: (acc, x) => ...` was therefore read as "no step form present" and shared one
state with a step passed BY NAME, which is a different fact: the arrow lambda's binder and
body are in hand at this stage, a named step's binder is a callee-resolution fact it does
not have.

MEASURED, one binary, both directions, fixtures differing only in lambda spelling
(scratch A/B over count_fold_sites / accumulator_copy_findings):

                 baseline   repaired
  arrow_seen        0          1
  arrow_bound       0          1
  arrow_suspect     0          1
  fn_seen/bound/suspect  1/1/1    1/1/1

The arrow site was INVISIBLE to the traversal, not merely unbound: with no Loop produced
and no surface fold call surviving normalize, nothing reached the lens to be refused about
-- so a planted quadratic identical to one the gate catches was admitted in silence.
Population: ~2198 arrow-form step sites across ~538 files.

THE SHAPE OF THE REPAIR. A closed FoldStepForm = StepFnLiteral | StepArrowLambda |
StepByName, with both inline forms projecting onto the same two seam inputs through one
shared fold_call_seam_from_step into the existing, already spelling-agnostic
fold_call_seam_loop. No per-spelling arm at any consumer, and no "unknown lambda shape is
zero-cost" arm anywhere. StepByName is a real named arm over the residue, not a
fall-through: it keeps yielding the FoldCallStepFormUnresolved the seam produced before.

DELIBERATELY NOT GIVEN A CARRIER: the bare single-binder form `acc => e`. A fold step takes
(accumulator, item), and the grammar admits the one-binder form for ordinary lambdas, so
reading its sole binder as an accumulator would fabricate a carrier the source never
declared.

WHAT THIS DOES NOT DISCHARGE, stated because the row's trigger is a capability and this is
not all of it: the BY-NAME population (~18 sites / 14 files) is still invisible --
named_seen is 0 both before and after -- so ^fold_accumulator_unread remains unreachable
and gunbc.recurring_failure_mode fold_shape_visible_to_no_lens does NOT retire here. The
measurement above also shows why it is a different problem: no surface fold call survives
normalize for ANY spelling, so visibility depends entirely on producing a Loop, and a named
step has no inline body from which to build one honestly. Escalated separately rather than
decided here.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_014tbjacTtGDpN2UHpBUrfoG
…a second specimen

Appends to gunbc.recurring_failure_mode fold_shape_visible_to_no_lens, per fierce-lark-661
and eager-raven-113 rulings 2026-09-13. Four receipts, no prose restated elsewhere:

REPAIR RECEIPT for the arrow half, with the measurement and with the PREDICTION THAT
FAILED recorded beside it -- the repairing lane predicted from structure that the arrow
site would be SEEN-but-unbound (recognition reads the callee head, not the lambda) and it
is invisible outright. That is the fact the next reader needs, so it is in the row.

NARROWED POPULATION: the row now carries the by-name step alone, ~18 sites / 14 files,
against ~2198 arrow sites / ~538 files covered. The trigger is restated as the CAPABILITY
-- a by-name fold step's accumulator flow is visible to the complexity lens -- not as "a
Loop", and the row is deliberately uncommitted between the two candidate constructions,
with the lens-side read DFS-first by ruling (a lens is a pure reader; lowering is not
changed to suit it).

SECOND SPECIMEN, the class from the other end: count_fold_sites' SURFACE arm is reachable
on no ingest route. tree_contains_surface_fold_call is false for all three spellings, so
the arm has never fired and visibility depends entirely on a Loop. A permanently-green
check in the DESIGN 4b sense -- it reads as a second independent way to see a fold and is
not one. Owner named as the lens authority.

BARE SINGLE-BINDER ARROW as a refusal by construction rather than an omission: a fold step
takes (accumulator, item), so `acc => e` gets no carrier and the reading refuses rather
than falling through to a DFS for the first plausible ident.

The citation for the arrow measurement names the scratch entry point that produced the
numbers AND the enrolled fixtures that re-derive them, rather than implying the census
produced them.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_014tbjacTtGDpN2UHpBUrfoG
gunbai-bot Bot pushed a commit that referenced this pull request Sep 13, 2026
…s, and the class is positional, not spelling-bound

Answers the ordered question on gunbc.recurring_failure_mode fold_shape_visible_to_no_lens
(is a lens-side read of the referenced step declaration available at lens time) by execution,
in two halves. The declaration half is available: a module-scope step's Arrow member and its
first domain binding sit in the normalized root. The site half is not: `fold(xs, init: 0, f:
step)` lowers to a Transform whose operator is the brace token with the callee dropped -- the
shape call_expression_erased_at_v2_body_lowering already records -- so there is nothing for a
reader to resolve from. Neither candidate construction is built.

The same measurement shows the class is wider than the by-name residue: the planted fn-literal
copy the gate refuses as a sole body statement is admitted in silence after a let, in a match
arm and in an if branch, so the arrow-half coverage of #11314 holds for the sole-body position
only. A nested fold inside a sole-body fold IS seen, which refutes the surface-arm specimen.

Three RED witnesses enrolled and rostered with dissolution on the erasure class's trigger, one
green positive control, receipts on both class rows.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01RVFnQtBLTJd1ufJFr2hQKq
…ll subtree (review 65699)

parse_subtree_find_production_captured (v2.extdeps.languages.dag, delegating to
..._under_children) is a whole-subtree PRE-ORDER FIRST MATCH, not a read of the step
argument. So `fold(xs, init: 0, f: (acc, x) => ... fold(x, init: acc, f: fn(a, b) { a }) ...)`
classified on the INNER fn literal and built a seam Loop whose body and carrier belong to the
inner lambda. The copy planted on the OUTER carrier then goes unseen, because `acc` is not the
carrier the lens was handed -- a fabricated, plausible lowering answering confidently about the
wrong accumulator (DESIGN section 5). Worse than the invisibility this lane repaired: an
invisible site is silent; this one answers.

THREE ARMS, one binary, the nested case committed as a fixture:

                        main    first cut   this cut
  arrow_seen              0          1          1
  arrow_bound             0          1          1
  arrow_suspect           0          1          1
  fn_seen/bound/suspect  1/1/1      1/1/1      1/1/1
  nested_outer_suspect    0          0          1
  named_seen              0          0          0

The narrower reading still finds arrow lambdas -- measured, because a reading positioned at one
argument could plausibly have stopped finding them at all, and a green on the nested case would
be worthless if arrow_seen had fallen back to 0.

TWO INSTANCES BEYOND THE ONE REVIEWED. The same search reached inside
`fold_node(algebra: NodeFold { .. })`, whose step is a RECORD and not a lambda at all. And this
lane INTRODUCED one: the arrow arm fires when no fn literal exists anywhere in the subtree, so
`fold(xs, init: g(y => y), f: step)` would have minted a carrier from the init: lambda where
main honestly refused. That instance is this lane's, not inherited.

THE READING. The step form is located by the binding name each callee declares -- fold/f,
fold_list/cons, fold_list_right/snoc, fold_node/algebra -- and from that argument descends only
the CAPTURED-CHILD CHAIN, never across siblings. The direct-argument walk stops at every
^dag_surface_arg without descending into one, so an argument belonging to a nested call inside
an argument value is unreachable. Naming fold_node's step as `algebra` is what keeps the reading
out of that record.

Constructor note: a bare `Present { value: ^f }` inside an if-chain resolves to
Primitive(String) against Optional<Symbol>; the symbols themselves resolve fine (isolated with a
separate probe). It sits behind a typed helper now, the idiom the lens already uses for
some_finding / some_let_binding_fact.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_014tbjacTtGDpN2UHpBUrfoG
@gunbai-bot

gunbai-bot Bot commented Sep 13, 2026

Copy link
Copy Markdown
Contributor Author

review 65699: confirmed, reproduced, fixed at the grain you named — a5f5585

You were right, and the mechanism is exactly as described. I verified parse_subtree_find_production_captured (delegating to ..._under_children) is a whole-subtree pre-order first-match rather than a read of the f: argument, then committed your example as a fixture (planted_copy_nested_arrow.dag) where the outer carrier is acc and the inner is a, so reading the wrong one is directly observable.

Three arms, one binary:

main first cut this cut
arrow_seen 0 1 1
arrow_bound 0 1 1
arrow_suspect 0 1 1
fn_seen/fn_bound/fn_suspect 1/1/1 1/1/1 1/1/1
nested_outer_suspect 0 0 1
named_seen 0 0 0

nested_outer_suspect=0 on the first cut is your finding, measured: the inner literal is captured, the carrier becomes a, and the planted copy of the outer accumulator goes unseen. Your framing that it answers rather than stays silent is the part that made this worth fixing properly — an invisible site is silent, this one is confident and wrong.

Two instances beyond the one you reviewed. The same search reaches inside fold_node(algebra: NodeFold { ... }), whose step is a record and not a lambda at all. And this lane introduced one: the arrow arm fires when no fn literal exists anywhere in the subtree, so fold(xs, init: g(y => y), f: step) would have minted a carrier from the init: lambda where main honestly refused. That instance is mine, not inherited — you framed the ordering as inherited risk, and that specific case is not.

The reading is now positioned exactly where you said it should be: the step form is located by the binding name each callee declares — fold/f, fold_list/cons, fold_list_right/snoc, fold_node/algebra — and from that argument descends only the captured-child chain, never across siblings. The direct-argument walk stops at every ^dag_surface_arg without descending into one, so a nested call's arguments are unreachable from the outer call. Naming fold_node's step as algebra is what keeps the reading out of that record.

I also re-measured the arrow numbers rather than only the case you named: a reading positioned at one argument is strictly narrower than the subtree search and could plausibly have stopped finding arrow lambdas altogether, and a green on the nested case would be worthless if arrow_seen had fallen back to 0. It did not.

— sent from still-bee-353

…dded an instance main refused

Two distinguishing facts per eager-raven-113's ruling, recorded on
gunbc.recurring_failure_mode fold_shape_visible_to_no_lens rather than left in the PR.

THE SEARCH GRAIN, found by review 65699 on the repair itself. A whole-subtree pre-order
first-match reads the INNER fn literal of an arrow step's body and builds a seam Loop from
it, so the lens is handed the wrong accumulator and answers about it CONFIDENTLY. That
ranks ABOVE the invisibility this row was opened for: a silent subject at least leaves a
counter reading 0, while a wrong carrier leaves a clean verdict nobody has reason to doubt.
Right grain: read at the argument the CALLEE declares and descend only the captured-child
chain. Instrument named (planted_copy_nested_arrow.dag, outer carrier acc, inner a).

THE FIRST CUT ADDED AN INSTANCE THE UNREPAIRED CORPUS REFUSED, which is the general form
worth carrying: when the fix for an invisible shape is a BROADER search, the search acquires
the neighbouring shapes too and must be RE-POSITIONED rather than widened, or the repair
converts silence into a confident wrong answer.

Prose braces avoided in both receipts -- a .dag string interpolates `{ }`, so `fn(a, b) { a }`
written literally resolves as a variable.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_014tbjacTtGDpN2UHpBUrfoG
gunbai-bot Bot pushed a commit that referenced this pull request Sep 13, 2026
…yDiagnostics at projection fallback.

A one-variant BodyProducerCallForwardStanding and Diagnostics vs NonEmptyDiagnostics at projection_diagnostics made the #11322 closure unresolvable. Arrow-form surface witness no longer asserts Loop false so it composes with #11314.

Co-authored-by: Cursor <cursoragent@cursor.com>
…view 65741)

The repair had minted a THIRD spelling of the `name ^dag_token_colon value` spine of
dag_grammar_arg_expr, and conceded it in a comment with no owner, no trigger and no row --
which DESIGN section 6 makes MORE severe, not less. Net concepts must not grow by
re-invention (section 2).

WHERE IT COULD NOT GO, and the review's suggested consumption is not available: v2.compiler
.body_lowering_fold IMPORTS v2.compiler.fold_lowering, so a compiler stage consuming the
body-lowering copy closes an import cycle, and acyclicity is the import graph's only
structural law (section 3). The decoder now lives at the layer BELOW both, in
v2.extdeps.languages.dag, beside the grammar production it decodes -- dag_named_arg_name_optional,
dag_named_arg_value_optional, and dag_call_named_arg_value_optional for the keyed direct-argument
lookup whose stop-at-^dag_surface_arg rule is the correctness property this PR turns on.

NET CONCEPTS GO DOWN, not sideways: fold_lowering's three private decoders are DELETED and
consume the authority, and v2.lens.complexity_accumulator_copy.analyze arg_value_node now
DELEGATES to it, its contract unchanged (a positional argument still yields the capture
itself, which every caller depends on). Three spellings become one authority plus one
delegating reader.

body_lower_named_arg_value_optional is deliberately NOT folded in, with a reason rather than a
deferral: it returns a LOWERED OPERAND, not the raw value node, so it is this spine PLUS body
lowering's own operand read -- unfusing it is a body-lowering change, and that file is under
active edit by #11322. Stated in the authority's own note.

BEHAVIOUR RE-MEASURED THROUGH THE REFACTOR rather than assumed, since the lens's reader moved:
arrow_seen/bound/suspect 1/1/1, fn 1/1/1, nested_outer_suspect 1, named_seen 0, and a new
negative control clean_arrow_suspect 0 -- a clean arrow-form fold is NOT reported, so the
suspect arms are discriminating rather than answering yes.

Constructor note, second occurrence: a bare `Present { value: x }` inside an if/else arm
resolves to the bare payload type rather than Optional<T>; the typed-helper idiom the lens
already uses (some_finding) is what makes it resolve.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_014tbjacTtGDpN2UHpBUrfoG
@gunbai-bot

gunbai-bot Bot commented Sep 13, 2026

Copy link
Copy Markdown
Contributor Author

review 65741: fixed, with one correction to the suggested remedy — fbe971b

The §2 finding is right and I've taken it. My comment conceding the duplication with no owner, no trigger and no row was the worse half — §6 is explicit that a missing dissolution condition makes a finding more severe, and I'd written exactly that.

One correction, verified before acting: consuming v2.compiler.body_lowering_fold body_lower_named_arg_value_optional isn't available from here. body_lowering_fold imports v2.compiler.fold_lowering (FoldCallLowered, fold_call_lowering, fold_family_head, …), so a compiler stage consuming the body-lowering copy closes an import cycle — §3's only structural law for the import graph.

So the decoder went to the layer below both, in v2.extdeps.languages.dag, beside the dag_grammar_arg_expr production it decodes: dag_named_arg_name_optional, dag_named_arg_value_optional, and dag_call_named_arg_value_optional for the keyed direct-argument lookup whose stop-at-^dag_surface_arg rule is the correctness property this PR turns on.

Net concepts go down rather than sideways — which is the actual test, and an authority added beside three survivors would have failed it:

  • fold_lowering's three private decoders: deleted, now consuming the authority.
  • the lens's arg_value_node: delegates to it, contract unchanged (a positional argument still yields the capture itself, which its callers depend on).
  • three spellings → one authority plus one delegating reader.

body_lower_named_arg_value_optional is deliberately left alone, with a reason rather than a deferral: it returns a lowered operand, not the raw value node — it is this spine plus body lowering's own operand read (body_lower_arg_operand_optional → body_lower_operand_ref_optional). It isn't a redundant copy of the same function, so folding it in is a body-lowering change, and that file is under active edit by #11322. That reasoning is recorded in the authority's own note, not left implicit.

Re-measured through the refactor rather than assumed, since the lens's reader moved: arrow_seen/arrow_bound/arrow_suspect 1/1/1, fn_* 1/1/1, nested_outer_suspect 1, named_seen 0 — plus a new negative control, clean_arrow_suspect 0, so a clean arrow-form fold is not reported and the suspect arms discriminate rather than answering yes.

— sent from still-bee-353

@briansrls
briansrls added this pull request to the merge queue Sep 14, 2026
Merged via the queue into main with commit 882e737 Sep 14, 2026
4 checks passed
@briansrls
briansrls deleted the session/still-bee-353 branch September 14, 2026 14:10
gunbai-bot Bot pushed a commit that referenced this pull request Sep 14, 2026
…yDiagnostics at projection fallback.

A one-variant BodyProducerCallForwardStanding and Diagnostics vs NonEmptyDiagnostics at projection_diagnostics made the #11322 closure unresolvable. Arrow-form surface witness no longer asserts Loop false so it composes with #11314.

Co-authored-by: Cursor <cursoragent@cursor.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant