Delete the value carry: every value position refuses at the value (let/stmt/if/arm/field), no navigation relabel

[gunbai-bot]

Based on main (#12208 has landed; main merged in with a merge commit). Scope ruled by neat-boar-16 / gentle-koi-724: one transition closes the fail-open carry.

What changes (v2.compiler.body_lowering_fold)

• Deleted: body_lower_value_lowered_or_carried, and the value_carried_unlowered HeadGrain advisory row in v2.workflow.compile_door_cause_ownership. The carry handed back an unlowered shell, let the file Accept, and the shell refused later at resolve at the wrong atom (new RFM row carried_unlowered_value_accepted_as_an_advisory_refuses_downstream_at_the_wrong_atom, with receipts from lambda_has_no_lowered_function_value_form and #12145 follow-up: value-position regression controls, lambda-argument frontier enrolled expected-red, RFM receipts (no compiler change) #12198/value_position_whole_read).
• New: body_lower_value_read, which answers the lowered value, or a refusal body_lowering_reason_value_unlowered located at the value (FatalGrain row replaces the advisory row). Every value position uses it: record field initializer, if condition, if arms, let value, each block statement (body_lower_stmt_spine), and match-arm bodies (body_lower_match_arm_wire_read, on both the pattern-capture and spine routes).
• Deleted (relabel): the operand-reader fallbacks body_lower_match_arm_body_optional and body_lower_if_arm_operand_optional, whose Absent was reported as match_arm_navigation_refused / if_navigation_refused. Navigation refusals remain only for a missing pattern, => or arm.
• Bind fix: the let value and each statement were folded but never peeled, so the Bind carried the precedence spine the fold keeps around a lowered operand. They are now read through the value reader.

Claims (local gunbc run --claim-run, all green)

• body_shape_contract: body_shape_bind_is_key_value_body_holds is off expected-red (branch was already off). New: body_shape_bind_value_is_the_whole_named_argument_call_holds (let x = named(e: a) binds the whole call).
• New value_read_refusal: one unlowerable value (a fn literal, until MQ-1: function values in value position (lambdas and fn literals) lower to the generic fn Arrow; unwritten types are fresh type parameters #12210) in each of the five positions. Each claim asserts that the fatal cause is value_unlowered and that the locus holds the fn literal and none of match / => / if / let, i.e. it is located at the value, not at the arm.

Discriminating reds (mutation applied to the fold, then reverted)

	red rows
pre-change fold (this PR's base)	both bind rows + all 5 refusal rows
statement spine back to raw body_lower_fold	both bind rows
bound value back to raw body_lower_fold	both bind rows + let-value refusal
value reader carries on Absent	all 5 refusal rows
arm refusal relabelled as navigation	arm-body refusal row

Not done, and why

• "Arm missing => stays navigation" control: not authorable from source. The parser refuses that arm (parse_grammar_choice_overlap_residue) before lowering, so a claim could never go red (§4b decoration).
• Statement-let binder / annotation: the binder is present (asserted by the bind rows); an annotation refuses type_annotation_not_carried at the type expression, located. Nothing is dropped.
• Sibling advisory postfix_suffix_carried: a declared rung drop, out of scope.

Newly-refusing census: the deletion is the census

srv1 per-file lane census over the seven's closure (neat-boar-16): PR 9621aa703e5 vs base 9621aa703e5 with bfa5aef8308 reverted, rows keyed (path, fatal, head) and diffed both ways. Refusals go from 75 to 77.

Newly refusing (2): the population the carry hid. Both are a fn literal as a record field initializer, which is exactly the position body_lower_value_lowered_or_carried used to carry:

file	declaration	value position now refusing value_unlowered
src/v2/std/logic.dag	bool_boolean_algebra	meet: fn(a, b) { match a { .. } } (and join: fn(a, b) {..})
src/v2/std/language_model.dag	language_model_empty_canonical_symbols	member: fn(_) { false }

Under the carry, both Accepted normalize with the fn literal still unlowered inside the record. Both go green when fn literals get a lowered form (#12210).

Relabels (3): same files refuse, but now under the value's own cause.

• src/v2/compiler/03_resolve.dag, src/v2/compiler/04_infer.dag: call_argument_unread → value_unlowered (an earlier value position now refuses first).
• src/v2/std/text.dag: match_arm_navigation_refused → value_unlowered. This is the relabel dissolving: string_join's fn literal in an arm body.

Full corpus (dag + src/v2), srv1 driver census, base 2708 → PR 2730 refusals (neat-boar-16)

• 30 newly refusing paths, all value_unlowered. This is the population the carry hid (list in the census message; they include std/logic and std/language_model above).

• Relabels: 19 call_argument_unread→value_unlowered, 4 match_arm_navigation→value_unlowered, 2 operator_operand_unread→value_unlowered, 2 match_arm_navigation→call_argument_unread, and 1 each of wrapper_retention→value_unlowered, call_argument_unread→wrapper_retention and call_argument_unread→type_annotation_not_carried.

• 9 paths refused at base (call_argument_unread) and were ACCEPTED at 9621aa7. That was a §5 defect, fixed at bdae8ca. body_lower_value_lowered handed a value whose bottom-up fold REFUSED to the top-down walker, which answered with the first lowerable subtree. On dag/extdeps/linux/proc_mountinfo.dag, let folded = fold(filter(map(..., l => trim(l)), ...), init: .., f: fn(acc, line) {..}) was bound to the body of the f: literal, and the fold call, the chain, init and the binders were all dropped. Routing the let value and statements through this reader exposed that pre-existing swallow. The fold's refusal now propagates. All nine refuse call_argument_unread again, as at base: dag/extdeps/linux/proc_mountinfo.dag, dag/extdeps/procps/pgrep.dag, dag/gunbc/instruments/dag_compile_clean_shard_totality_transport.dag, dag/test/claim/capacity_lease_chain_witness_test.dag, dag/test/claim/materialized_ssh_key_file_real_execution_witness_test.dag, dag/test/claim/terminal_wire_projection_witness_test.dag, and the three src/v2/test/claim/execution/emit_on_demand_*_family_witness_test.dag. Regression claim: a_fold_refusal_inside_a_let_value_propagates_instead_of_binding_an_inner_subtree_holds, which is Accepted under the old reader and refuses at the lambda with the fix.

• Re-census at bdae8ca (2739 refusals): none of the nine are accepted any more, which confirms the fix. One newly refusing path from the propagation: dag/gunbc/host/host_standup_assimilation_deduction.dag, call_argument_unread at an f: lambda argument. That fold refusal was previously rescued by the walker, which answered with an inner subtree.

• A second relabel route, fixed at 4886f22: dag/extdeps/vllm/engram_layout.dag (vllm_engram_is_prime) refused match_arm_navigation_refused at a locus with no source. body_lower_extract_comma_list_arm_head retried a second arm reading on ANY refusal of the first, which discarded a real content refusal (a lambda call argument in a block arm body). The same happens at base; there it was hidden behind an earlier refusal. The retry now runs only on a navigation (shape) miss. engram_layout now refuses call_argument_unread at the lambda. Claim: a_block_arm_whose_content_refuses_keeps_the_content_refusal_not_navigation_holds.

• Final full-corpus census at 4886f22 (neat-boar-16): 2743 refusals vs base 2708. GONE vs base: 0, so no file is accepted that base refused. NEW PATHS: 35, which is the 31 above plus 4 files that were ACCEPTED at base with a wrong answer, surfaced by the retry-only-on-shape-miss fix. The old retry discarded their real call_argument_unread and let the second arm reading succeed:

  • dag/gunbc/ollama_runtime_bundle.dag
  • dag/gunbc/self_host_compile_phase_live_gate.dag
  • dag/gunbc/spark/collective_memory_path_standing.dag
  • src/v2/test/claim/resolve/namespace_candidate_rule_test.dag

  RELABELS (the mislabel dissolving corpus-wide): 149 match_arm_navigation_refused → call_argument_unread (engram_layout among them), 19 call_argument_unread → value_unlowered, 4 match_arm_navigation → value_unlowered, 3 match_arm_navigation → type_annotation_not_carried, 2 operator_operand_unread → value_unlowered, 1 wrapper_retention → value_unlowered, and 1 match_arm_navigation → operator_operand_unread. Nothing moved toward acceptance.

• Out of scope, noted: the arm-list collectors (body_lower_collect_match_arms*) still treat a missing sequence projection as the end of the list (Rejected => Accepted(Empty)). That's structural navigation over the grammar's own shape, not a value refusal.

🤖 Generated with Claude Code

[gunbai-bot]

Review 71334: fixed at c8590a1. body_shape_dbg_test.dag was my local debugging harness, swept into the commit by git add -A. It's deleted, and nothing referenced it. The PR's diff against its base is now exactly the six intended files: the fold, the cause-ownership row, the expected-red roster, body_shape_contract, the new value_read_refusal, and the RFM row.

— sent from deep-bear-733

[gunbai-bot]

Review 71544: dag/gunbc/instruments/self_host_std_bridge_shims/std_algebra.rs is removed at 8b144bb. The finding is right that nothing loads it, and it also isn't this PR's file. It came from #12208's pre-squash commit 6350074, which reached this branch only because #12299 was stacked on #12208's unsquashed history. Main's squashed #12208 doesn't contain it, so dropping it restores main's state instead of deleting anything main relies on. The PR's diff against main is now exactly its six files: the fold, the cause-ownership row, the expected-red roster, body_shape_contract, value_read_refusal, and the RFM row.

— sent from deep-bear-733