XL-2: a return lowers only as a function body's tail; everywhere else it refuses located

[gunbai-bot]

XL-2, the return floor fix (option A as ruled by quiet-seal-543): return is recognised, lowers only as a function body's tail, and refuses located everywhere else.

The defect: silent wrongness on main

No reader in v2.compiler.body_lowering_fold named dag_token_kw_return. A deep first-match search answered the statement seq(return, e) with e, so the keyword was silently dropped. Measured on main 88436e5 through module_roots_from_source_root_ingest:

fn f(c: Bool, j: Int, k: Int) -> Int { let x = if c { return j } else { k }
  x }

This was accepted as x = Branch(c, j, k): the function continues where it should have exited. A return in an arm of a tail-position if, and a return before another statement in a fn value, were accepted the same way.

The change

• body_lower_return_statement_expr_optional recognises a return statement.
• body_lower_return_outside_tail_optional is the wall. It collects every return under a fn declaration, a fn value's block body or a data initializer, stopping at nested fn values, which own their own returns. It refuses the first one that is not the body's tail statement as body_lowering_reason_return_not_in_tail_position, located at it, before any reader can search past it. It sits beside the existing else-less wall in body_lower_fn_decl_to_arrow.
• In the statement spine, the tail statement is read by body_lower_tail_statement_read: a return lowers to its operand, explicitly. body_lower_try_statement_spine routes a sole return head into the spine rather than the expression walkers.
• The else-less guard keeps refusing else_less_if_unlowered.
• No reader signature changes. bright-boar-848 was told of the fold edits before the push.

A consequence, stated plainly: fn f(..) { if c { return a } else { b } } was accepted on main (correct only by luck) and now refuses as return_not_in_tail_position. Admitting it needs the tail position carried through the value readers. That is the next-rung trigger, sequenced after first-match PR-2. The census counts these cases.

Evidence (local gunbc run, same binary; the only variable is main's body_lowering_fold.dag versus head's)

Witness v2.test.claim.namespace_xl0.return_tail_position: one front end over 9 inline modules, enrolled warm.

claim	main fold	head
a_return_inside_a_let_bound_if_refuses_rather_than_binding_its_operand (the bug)	FAIL (accepted)	PASS
a_return_followed_by_a_statement_refuses_as_not_in_tail_position	FAIL (generic statement_precedes_without_binding)	PASS
a_return_in_an_if_arm_refuses_as_not_in_tail_position	FAIL (accepted)	PASS
a_return_before_another_statement_in_a_fn_value_refuses	FAIL	PASS
an_else_less_guard_still_refuses_as_unlowered	PASS	PASS
a_tail_return_of_a_fn_body_is_accepted (control)	PASS	PASS
a_tail_return_after_a_let_is_accepted (control)	PASS	PASS
a_tail_return_of_a_fn_value_block_body_is_accepted (control)	PASS	PASS
a_tail_return_operand_is_read_and_refuses_unbound_at_its_atom (discriminator: the operand is read, not dropped)	PASS	PASS

Census

Population: the 316-path pinned reference_conservation_stratified_sample_paths, plus every file containing return (451 paths). Base 88436e5, head 6326413. Results follow in a comment when the completed waves pair: modules that newly refuse, each with a disposition.

Carriers

• New RFM row return_lowered_as_its_operand_outside_the_function_tail. Rung: below the floor → mitigated. Its ceiling is structured early exit, and its trigger is the tail position through the value readers. The else_less_if_statement_has_no_lowered_form row points to it.
• New cause row body_lowering_reason_return_not_in_tail_position in compile_door_cause_ownership.
• For compiler_frontend_program_status (not edited here): return is recognised, lowers only at a function body's tail, and refuses located elsewhere. Structured tail return and the guard wait on the tail position through the value readers, after XL-2 PR-2.

🤖 Generated with Claude Code

[gunbai-bot]

Census, from completed waves only (4 waves). Population: the 316-path reference_conservation_stratified_sample_paths plus every file containing return, 451 paths in all. Base 88436e5, head 6326413. One gunbc process per path, with a child cgroup memory.max per batch.

Paired: 450 of 451. The unpaired path is this PR's new RFM row, which has no main side.

Changed verdicts: 5 modules, each with a disposition.

module	main	head	disposition
dag/test/claim/diverging_match_arm_join_witness_test.dag	accepted	refuses return_not_in_tail_position	Silent wrongness removed. let cell = match .. { Absent => return ProbeUnknown {..} Present { value } => value } is the exact bug class: main bound cell to the ProbeUnknown and continued.
dag/gunbc/machine_intake/mtcollins1_fan_observe.dag	accepted	refuses return_not_in_tail_position	Correct on main by luck, now loud. return sits in the arms of a match that is mtcollins1_fan_observe_wet's tail, so main's lowering matched the meaning. It returns when the RFM trigger (tail position through the value readers) lands.
dag/gunbc/bmc/bmc_fan_converge.dag	refused statement_precedes_without_binding	refuses return_not_in_tail_position	Refused on both sides; the cause is now named precisely.
dag/gunbc/fleet/fleet_health.dag	refused else_less_if_unlowered	refuses return_not_in_tail_position	Refused on both sides; the return wall is reached first.
dag/test/claim/doc_reachability_witness_test.dag	refused operator_operand_unread	accepted	Recovery. Its fns are { return <expr> }, which main's walker misread as an unreadable operand. They now lower explicitly: conserved goes from 0 to 175. Its 26 absent atoms are let binders and named-argument labels (b, dup, rows, description, binds, key_eq, ..), with role_not_yet_read = 26 on both sides. That is the instrument's baseline class for these roles, seen on main in accepted modules (e.g. dag/examples/weather/weather.dag let binders), not a drop this change introduces.

Newly refusing modules: 2, one silent-wrong and one correct-by-luck.
Atoms: 321 recovered, and 26 newly absent, all of them the doc_reachability baseline-class atoms above.
Totals (main → head): authored 94440 → 94440, conserved 19779 → 19674, dropped 64217 → 64293. Both moves come from the two newly refusing modules dropping whole, net of the doc_reachability recovery.

— sent from sharp-carp-336

[gunbai-bot]

Correction to the census comment above: its last line put the conserved and dropped totals down to the two newly refusing modules and the doc_reachability recovery. That is incomplete. I re-derived the per-module deltas (head minus main) from the same completed waves.

module	conserved	dropped	verdict
diverging_match_arm_join_witness_test	-261	+344	newly refuses (silent-wrong removed)
mtcollins1_fan_observe	-191	+235	newly refuses (correct by luck, now loud)
doc_reachability_witness_test	+175	-276	newly accepted (recovery)
boot_image_fetch	+122	-161	accepted on both sides
extdeps/accounting/budget	+26	-34	accepted on both sides
product/budget_tree	+16	-20	accepted on both sides
extdeps_external_authority_gate, json_emit_corpus_witness, roadmap_site_healthz_json_parse_witness, cheap_claim_pool_gate	+2 each	-2 each	accepted on both sides
reference_instrument_witness_test	0	-1	accepted on both sides
bmc_fan_converge	0	+5	refused on both sides
fleet_health	0	-8	refused on both sides

The seven modules accepted on both sides all move toward conserved. Their tail return operands are now read explicitly, where main's first-match search lost part of the operand. No module accepted on both sides lost a conserved atom. The two newly refusing modules account for the whole net loss in conserved (-452). Every other module gains (+347).

— sent from sharp-carp-336

[briansrls]

APPROVE-MERGE at exact head 6326413, through the merge queue only.

This closes a real below-floor path rather than merely renaming a refusal. return is now recognized before the first-match walkers can search past its keyword. A function declaration or block-bodied function value admits only its own direct tail statement; data initializers admit none; nested function values are pruned from the outer scan and own their returns. The admitted tail is lowered explicitly through the value reader, while every other site refuses with the located return_not_in_tail_position cause. The witnesses distinguish the original silent-wrong let/if case, a non-tail sequence, an arm return, a nested function-value return, the retained else-less-if refusal, lawful direct-tail cases, and an unbound tail operand that proves the operand is read.

The narrower current floor is stated honestly: a return in a tail-position if or match arm remains loud until tail position is carried through the value readers. The RFM and cause roster name that trigger instead of claiming structured early exit is already delivered.

I also checked the corrected census disposition. The two newly refusing modules are the silent-wrong specimen and one correct-by-luck structured-return case; every module accepted on both sides either improves conservation or is unchanged, and the recovered tail-return modules are accounted for. That supports the wall rather than hiding an unexplained accepted-program regression.

Current exact-head witnesses run 36542641708 completed successfully, and there are no unresolved review threads. No local tests or census were run by me. Require the actual merge_group candidate to pass against then-current main; no direct merge or check bypass.

[briansrls]

APPROVE-MERGE / REBIND at exact head b4307d7, through the merge queue only.

This renews my approval from 6326413. The only branch commit since that reviewed head is the merge of main (second parent 6571276). Its sole conflict was src/v2/workflow/floor_pure_producer_share.dag. The resolved PR diff retains the return-tail-position warm producer and its nine-specimen rationale while taking main's other roster additions; the PR's behavior files are unchanged from the approved head.

The original verdict therefore carries: return is recognized before first-match search can discard its keyword; only a function body's direct tail return lowers explicitly through the value reader; every other return refuses at its own site; nested function values own their returns; and the structured-tail-return limitation remains honestly open. The nine exact claims remain the discriminating floor evidence.

Exact-head witnesses run 36604560732 completed successfully, and GitHub reports the PR mergeable. No local tests or census were run by me. Require the actual merge_group candidate to pass against then-current main; no direct merge or check bypass.