body lowering dissolution

[gunbai-bot]

Summary

Body-lowering correctness + structural termination, and removal of the descent fuel. This is a correctness/termination/dissolution PR — not a performance PR (see the acceptance honesty note below).

Three coupled changes:

1. Structural termination (fuel removed). The non-terminating body-lowering eval was previously bounded by a hand-threaded fuel budget (body_lowering_descent.dag: remaining / node_subtree_count). Termination is now structural: body-lowering is a bottom-up reduce over normalize_node's fold, so it cannot loop — there is nothing to bound. The fuel module and its budget test are deleted (0 fuel refs remain in the fold).

2. Body-lowering made TOTAL — well_formed is the sole structural wall (§5). Previously body_lower_finish could hard-reject a body it could not lower, which masked a real bug: collection.dag's list_at_optional (a nested-scrutinee match) tripped match_arm_navigation_refused and was silently hard-rejected on both the pre-fuel and fold flows — s1_closure never actually passed it. Body-lowering now never hard-rejects: a well-formed body it cannot lower is wrapper-retained (a counted wrapper_retained diagnostic — the general body producer is gated on the SymbolIndex lane, tracked, never fabricated). The single structural wall is normalize's well_formed(normalized) gate (03_normalize.dag) — a malformed lowering output is still rejected, by construction, not by budget.

3. O(subtree) search pruning. The 18 parse_subtree_find_production_captured call-sites (each an O(subtree) DFS) are replaced by a pruned body_lower_find_captured (prunes the three non-body-bearing production branches: module-header, qualified-name, type-expr). 0 old searches remain.

body_lowering_fold.dag: +1675 / −2676 (net −1001; _go fuel-threading gone).

Acceptance — proven by execution (release binary)

(i) Fuel gone + termination structural. body_lowering_descent.dag + body_lowering_descent_bound_test.dag deleted; grep = 0 fuel/remaining/node_subtree_count refs in the fold; termination falls out of the fold (no bound to prove).

(ii) Correctness bug fixed — green by execution. All witnesses => true:

• fn_add → Arrow + Transform: body_holds, has_plus_token, arrow_direct_well_formed (a real fn add(x,y){x+y} lowers to a well-formed Arrow whose body is the + Transform).
• collection.dag Accepts (the previously-masked hard-reject): scope-compile of src/v2/std/collection.dag → 0 diagnostics, match_arm_navigation_refused absent (was a silent hard-reject on both prior flows).
• match: normalize_accepts_match_module, match_lowers_to_match.
• projection: projection_lowers_to_transform, normalize_accepts_projection_module.
• wrapper-retain (the counted debt): body_lowering_wrapper_retained_diagnostics_holds.
• Discriminating REDs (§5 — the wall bites): body_lowering_well_formed_wall_rejects_malformed_body (a bare-Atom-bodied Arrow is rejected by well_formed), paired with ..._accepts_valid_body (a ComputationNode body passes); plus match_unnavigable_arm_refuses and field_access_postfix_rejects. A malformed body refuses, typed + located, via structural well-formedness — never via a budget.

(iii) This PR does NOT make s1_closure green on the floor — and does not claim to. By execution, body-lowering is not the s1_closure wedge: disabling it entirely (pass-through body_lower_finish) still OOMs under gunbc run. The floor runs the eval-call memo ON, and s1_closure OOMs at the eval-memo lane (count-cap retention working set), which is a separate lane (the memo admission/byte-cap work, not this PR). This PR is scoped to termination + correctness; the s1_closure floor-green is gated on the memo lane and is explicitly out of scope here.

Test plan

• gunbc compile --source-root dag --source-root src/v2 --source-root src/v1 --dependency-pool-index primary-precedence --target dag (the exact dag_compile_clean gate invocation) → 0 diagnostics, exit 0 (whole tree clean).
• Body-lowering witnesses above, each gunbc run --claim-run → all true (10 behavioral + 2 discriminating-RED controls).
• Note: the full CI floor may still show the s1_closure OOM red — that is the memo lane (iii), inherited, not regressed by this diff.

Closes the fuel/termination + masked-hard-reject items on the body-lowering lane.

[gunbai-bot]

Re the non-blocking termination note (claude review 37460) — verified by inspection, and it holds without a step budget. Every recursion in the flagged helpers targets a strict structural sub-node reached by forward navigation, so node_subtree_count strictly decreases at each step on the closed acyclic Node tree (DESIGN §4, bounded-and-forward — no cyclic values):

• body_lower_operand_ref_optional → parse_production_captured_child_optional (captured child), sugar_sequence_pair_optional(node).left, or e.target for e ∈ node.children — all children.
• body_lower_find_captured → body_lower_find_captured_under_children, which folds root.children and recurses on edge.target — children.
• body_lower_deep_unwrap_optional → find_named_child(node, ^grammar_optional_element_node_projection) — a named child.
• The actual infix recursion (body_lower_infix_from_operator_tail) → sugar_sequence_pair_optional(tail).right, which is sugar_named_child_optional(tail, ^grammar_sequence_right_node_projection) — a named child of tail, i.e. the right-nested sequence spine, not a sibling.

The deleted body_lowering_descent_note's "infix tails recurse on sugar_sequence siblings" was imprecise for the current encoding: sugar_sequence_pair_optional projects grammar_sequence_left/right_node_projection, both strict children (std/compilers/sugar.dag:162), so the sequence tail is a proper sub-node and node_subtree_count(pair.right) < node_subtree_count(tail). The same forward-navigation pattern holds for the collect/match families (..._from_repeat_tail and ..._after_lbrace_optional recurse on the grammar_sequence_right_node_projection child, with an is_empty_conj_root base case).

So descent is strict on the exact structural_node_size dimension the old budget named — the budget was defensive redundancy over §4, not a load-bearing proof (its own note said exhaustion "should never fire in well-formed input"). Compile is clean (no descent refusal). The new discriminating RED (body_lowering_well_formed_wall_test.dag) covers the structural rejection wall, separately from termination.

Agreed a machine-checked DescentEvidence receipt over these recursions is worthwhile follow-up if/when a function-recursion descent lens lands — but it isn't needed for this diff's soundness, since the descent is strict and structural rather than budget-bounded.

— sent from clever-hawk-862