XL-2: a match arm keeps its own refusal cause in every arm position; the value reader carries the fold's refusal

[gunbai-bot]

What

v2 body lowering now keeps a match arm's own refusal cause in every arm position. It no longer re-reads a refused arm under the wrong shape and reports body_lowering_reason_match_arm_navigation_refused, which carried the arm as its only locus.

XL-2 fold cleanup, item (1) (the fall-back reader). Owner: quiet-seal-543.

The chain, and where it first went wrong

I bisected dag/gunbc/accelerator_demo/accelerator_demo_eval.dag down to its smallest refusing shape. The refusal is not specific to lists, nesting or if: a refusable value in any match arm after the first (or in a comma-separated arm) refuses as navigation. The same value in the first arm refuses located. I tagged each of the 14 body_lower_match_arm_navigation_reject callers to find the one that fires. The earliest unjustified link was one step above the arm wiring:

• body_lower_extract_comma_list_arm_head, the earliest wrong link. It wired the node as an arm and, on any Rejected, discarded the diagnostics and retried the same node as a comma-repeat element. An arm that refused for its own located cause was re-read under the wrong shape, and the retry answered navigation. Repair: decide the shape first, then wire once, and let Rejected stand. A repeat element is Seq(optional-comma, arm), so its left side is a separator, as body_lower_match_arm_repeat_elem_is_separator already decides; an arm's left side is its pattern, which never is. body_lower_match_arm_from_comma_repeat_elem is deleted: it had no other caller.
• body_lower_value_lowered, the brief's link. When the bottom-up fold refused, it handed the raw value to the top-down walker, discarding the fold's cause. It now carries the fold's Rejected.
• One arm-body reader. The sequence arm path read bodies through body_lower_value_lowered, but the two spine arm paths used the operand reader alone. All three now go through body_lower_match_arm_wired (value reader first, its Rejected carried; the operand reader only when it answers Absent). This is §3: one question, one authority.

Witness

v2.test.claim.namespace_xl0.match_arm_refusal_carried covers five inline modules through the native front end. Each is judged by the fatal cause of its file refusal.

claim	origin/main	head
a_second_arm_refuses_under_the_cause_the_first_arm_reaches	FAIL	PASS
a_comma_separated_arm_refuses_under_the_cause_the_first_arm_reaches	FAIL	PASS
a_first_arm_specimen_still_refuses_located (control)	PASS	PASS
a_second_arm_with_no_refusable_value_is_not_refused (control)	PASS	PASS
a_comma_separated_arm_with_no_refusable_value_is_not_refused (control)	PASS	PASS

Both sides were run with local claim_batch, same binary, with only the fold file swapped. Each claim costs about 1.48M eval steps, almost all of it the shared front end, so marc_outcomes is enrolled WARM in v2.workflow.floor_pure_producer_share, as iasl_outcomes is.

Why the claims are relational. The specimen is a list literal, the shape the corpus specimen refused on. The claims do not name body_lowering_reason_list_literal_unlowered, because #12208 deletes that cause when it lowers lists. They assert instead that arm position does not change the cause. If a later change lowers the specimen, a_first_arm_specimen_still_refuses_located goes red by name and the specimen value is replaced, rather than three accepts greening the relational claims.

Identity census (main 69e0bb7566e vs head 7692619dc7a, the fold change alone)

Instrument: native_test_context_from_ingest file_refusals, one ingest per path, head_reason and fatal_reason. It ran remotely in batches of 25, same binary on both sides, with only the checkout differing. Coverage so far is PARTIAL: 1,000 of 6,778 .dag files under dag/ and src/v2/ are paired. The rest is running in waves against BuildBuddy's 1-hour cap, and the full table will be posted as a PR comment. Hand-off to the parent waits on the full census; the PR is marked ready now only so CI and the floor can plan the witness in parallel.

27 of the 1,000 paired files change. No file goes from refused on main to accepted on head.

main	head	files	disposition
match_arm_navigation_refused	list_literal_unlowered	16	Intended. The arm's own located cause, previously discarded.
match_arm_navigation_refused	call_argument_unread	7	Intended. Same, with a different own cause.
call_argument_unread / list_literal_unlowered	the other one	2	Neutral. Two located causes in one file; the first fatal cause now comes from a different site. Both are real and both are located.
(accepted)	list_literal_unlowered	2	Intended: silent drop becomes a loud refusal. On main, dag/gunbc/bmc/bmc_converge.dag is accepted with 436 of 1,193 authored atoms dropped and 0 refused, and dag/gunbc/fleet/fleet_desired_observe.dag is accepted with 74 of 280 dropped (reference_conservation_census_for_paths on main). The fold refused, the walker accepted by dropping, and DESIGN §4b forbids that silent state outright.

Not in this PR (so this PR is not read as closing them)

• Arms 3+ of a match are dropped silently (gentle-crane-869, about 457 atoms). This is the next PR in this lane, in the same reader. v2.test.claim.body_lowering.single_arm_match pins that drop today.
• body_lower_find_control_form_optional (a record, call or binary expression containing a block lowers to the block alone) is not touched here. It is a separate queue item.
• An as-cast operand is accepted in every arm position on both sides, which means it is carried, not refused. That is item (4)'s evidence, recorded here.

Carrier wording (for compiler_frontend_program_status, not edited here)

v2 body lowering keeps a refused match arm's own cause and locus in every arm position (body_lower_extract_comma_list_arm_head decides the arm shape before wiring and never discards an arm's Rejected), and body_lower_value_lowered carries a fold refusal instead of re-reading the value through the walker. Witness: v2.test.claim.namespace_xl0.match_arm_refusal_carried.

Stage0

No generated stage0 file derives from the changed functions, so none is installed.

Other

The census ran with a per-batch child cgroup memory.max bound after the build, not GUNBC_MEMORY_BUDGET_BYTES. The parent agreed: the budget variable is the refusal-bypass DESIGN §5 forbids. No catch-all binder arm over an Rc-held coproduct was added, so the known read.clone() E0308 emitter defect is not exercised.

🤖 Generated with Claude Code

[briansrls]

REQUEST_CHANGES at exact head 8af19cb. Do not enqueue this head yet.

The production direction is sound: decide comma-repeat versus arm shape before wiring, wire once, retain Rejected diagnostics, and use one arm-body reader. I am not alleging that these changes themselves produce an incorrect locus. Two acceptance-evidence gaps remain:

1. The located-refusal property is not tested. In src/v2/test/claim/namespace_xl0/match_arm_refusal_carried_test.dag, MarcFileRefused retains only fatal_reason. marc_verdict_in throws away any ability to check the diagnostic's actual locus, and marc_same_located_cause checks only equal non-navigation reasons. a_first_arm_specimen_still_refuses_located compares the first verdict with itself. These checks can all remain green if the right reason is reported at the whole arm, the wrong node, or no usable locus. That is precisely the distinction XL-2 needs.

Keep the relational reason checks and the accepting controls; add a discriminating production-boundary witness that inspects the actual diagnostic occurrence/location and resolves it against each specimen's own offending body/source-span evidence, rather than accepting the enclosing arm. A small lower-level witness alongside the current integration suite is sufficient; no broad context-carrier rewrite is requested. The three source strings have different layouts, so do not compare their raw numeric offsets to one another. A deliberate wrong/enclosing-arm locus must make this witness red. This need not pin the retiring list_literal_unlowered reason.

2. Complete or supply the promised census handback. The PR explicitly says hand-off waits for the full census, but the only posted receipt still covers 1,000 / 6,778 files, comparing main 69e0bb7 against intermediate 7692619. There is no completion comment as of this review. Please append the completed paired population, terminal completeness, source/binary identities, and dispositions for changed rows. Bind it to the reviewed production changes, or document production-code equivalence if the completed run used an earlier head. The broader body_lower_value_lowered rejection change warrants honoring the already-declared handback condition. A green workflow is not that receipt.

Arms 3+ and the enclosing-control-expression silent drop correctly remain separate work. Do not expand this repair to solve those before returning; close the two bounded evidence gaps above, then request exact-head re-review. I reviewed source and posted CI/author evidence, not a fresh local execution.

[gunbai-bot]

Closing as superseded by #12299 (merged e4bdd90), which landed all three of this PR's fixes: value-reader refusal propagation, the arm body read through the value reader with the operand fallback deleted, and comma-arm heads keeping non-navigation refusals. #12299's value_read_refusal witness asserts the refusal locus is the value itself (not match/=>/if/let), including a second arm, which covers the locus-discrimination gap review 5326092139 raised here. The remaining fold work (match arms 3+) continues in #12327.

— sent from quiet-seal-543