Floor: observe-only execution-grain reach selection (claims whose verdict a body change can move; #12361 near-miss)

[gunbai-bot]

Work item adhoc-be476b8f-943. Design ruled by neat-boar-16 (2026-09-26). Scope: selector + model + RFM row, observe-only. Operator ruling 2026-09-27: the per-PR v2 claim comparison is merge-blocking over this reach selection ∩ the v2 claim set (never the whole set). That enabling step is a separate follow-up PR stacked on this one; the execution-cost receipt (condition b) and the main-sha baseline belong to it.

What "affected" meant (read from #12361's floor run 36256059426 @ e659b86)

• Executed claims are the static gate selectors (required_gate_prefixes and required_gate_authored_modules, whose one v2 member is v2.test.claim.body_lowering.statement_let_bind) plus changed witnesses (test fns whose own lines the diff edits). That run had planned=537 and changed_witnesses=7.
• Compiled modules add the touched modules and the readers of interface-changed declarations (interface_changed_consumers, 8 changes, 1 consumer added).
• The 10 regressed claims (vivid-ram-65's base-vs-head list) are in v2.test.claim.* / v2.test.execution.*, outside the executed population. One of them sits in a touched file, so this is not a file-grain gap.

Earliest unjustified boundary

The only dependents walk is compile-grain, and it correctly stops at interfaces: a body-only edit can't make a caller's caller fail to typecheck. Nothing relates a body change to a claim verdict. #12361 changed only bodies (arrow_signature_edges_conform, eval_bind_arrow_params, infer_application_formals / _argument_inhabitance).

This PR

• namespace_baseline body_reach_from_changed_declarations does reverse reach over every read channel of the parse-phase DeclarationIndex. It uses the same read_binding rule as the interface walk and propagates through bodies. Readers are inverted once into a leaf map, so cost is linear in the reads touched.
• Seeds are FloorDiffEdits.touched_declarations (the declaration grain of the floor's own line attribution; an import-region edit seeds every declaration in its file) plus every interface change (the only seed a removed declaration has).
• Observe-only. The floor prints [floor-plan] BodyReachWitness identity=… through=… and a [floor-phase] phase=body-reach-selection summary, and plans nothing from it.
• Model: v2.workflow.floor_subject_seed ReachConsumer / reach_propagates, where a body read propagates for ClaimExecution and not for StrictPreparation. It is one rule keyed on its consumer, not a second relation.
• RFM row green_floor_executes_no_claim_whose_verdict_a_body_change_can_move.
• The seed-growth admission record (floor_arm_set_consumer_seed_growth) enumerates the new hand items.

Import-closure selection was rejected: v2's resolver ignores imports, and the namespace cut deletes them.

Evidence

• Rust fixture RED: a_body_only_change_reaches_the_witness_two_calls_away. The interface walk plans nothing; the reach walk selects the witness two calls away, and neither the idle importer nor the unrelated witness. Control: no_changed_declaration_reaches_nothing. Both pass (remote cargo test).
• .dag claim a_body_read_propagates_for_claim_execution_and_not_for_strict_preparation passes under claim_batch, and so does its neighbour only_an_interface_read_propagates_a_change.
• Not yet shown: the DECLARATIONS phase (DeclarationRef citations in the RFM row and the admission record) runs only on the required lane, not locally.
• Replay (srv1, see the evidence comment): MQ-1 PR-A: declared parameter order on the Arrow; positional binding reads it (infer + eval), never label order #12361 selects all 10 base-pass/head-fail claims (3655 witness decls); unrelated control V4.1 runtime image distribution by config digest (spark_v41_runtime_image_distribute) #12353 selects 522, scoped to readers of what it changed; 1-decl node.dag body edit 3286; selection ~1.8 s wall. Round 1 failed its control (13147) through two defects fixed in c4bbb44.
• process_cwd_mutation_reachability_gate (2 tests) fails identically on clean main 980761c; pre-existing.

Condition (a): the base-verdict cache, for the enabling step

The base verdict is a materialization (std.materialization_ladder). Its key must be complete over everything the verdict depends on:

• the claim identity;
• a digest of the base tree over every declaration in the claim's reach (the same reach relation, evaluated at base, over declaration source text);
• the seed binary identity;
• the interpreter identity.

The reach digest is the load-bearing part. A key over the claim's own file alone is exactly this row's failure again, one layer down. Because reach is computed at the grain of the reference index, the key inherits that bound: a dependency only through an inferred type, which no declaration on the path spells, escapes it. That bound belongs on the cache's refusal list, not silently in its key.

🤖 Generated with Claude Code

[gunbai-bot]

Replay evidence (srv1, via neat-boar-16; planning receipts only, each run stopped after planning)

Round 1 FAILED its control:

run	seeds	reached decls	witness decls
#12361 replay	812	21,850	13,474
#12353 unrelated control	684	21,613	13,147
1-decl node.dag body edit	1	6,710	4,802

An unrelated diff selected as much as the replay, so the selection discriminated nothing. Two defects were located from the fan-out (through= counts):

1. Field accesses and ambiguous names bound as reads. The flat bare channel admitted dotted field accesses (cfg.root has no module prefix, so its candidate set is empty) and ambiguous bare names. The fan-out ran through test-local helpers named root, subject, observed and standing. The execution walk now admits a flat read only for a bare spelling whose leaf has exactly one declarer, which is the compiler's own global-bare rule.
2. Seed inflation from import edits. An import-region edit seeded every declaration in its file (ci_spec has 244, fleet_converge_workflow 213). import_rebound_declarations now seeds only the reads whose import binding changed.

Round 2, after the fixes (commit c4bbb44):

run	seeds	reached decls	witness decls	flat-bound	selection wall
#12361 replay (7493f52 / 575fc48)	80	5,229	3,655	212	1,777 ms
#12353 control (bc51daa / bbe7f5b)	77	1,535	522	53	1,847 ms
node.dag body edit (7252753 / c4bbb44)	1	4,494	3,286	200	1,755 ms

• All 10 of vivid-ram-65's base-pass/head-fail claims are among the replay's BodyReachWitness identities (each grep count = 1).
• The control's top fan-outs are host_effect_apply, the spark serving/grant witnesses, posix_sh_program_command and the fleet workflow. Those are readers of what V4.1 runtime image distribution by config digest (spark_v41_runtime_image_distribute) #12353 changed (extdeps.exec.command, extdeps.docker.cli), so the selection is scoped to the change.
• "Witness decls" counts declarations in fixture-carrier modules, helpers included, not claims.
• Selection cost is ~1.8 s wall over an index already in memory.

Pending, condition (b): the cost of EXECUTING the selection at base and at head (one claim_batch per side over the selected test fns). That run is with neat-boar-16. For the node.dag case, the edit is semantics-preserving, so its differential should be ~0, which also makes it a false-positive control.

Pre-existing, not this PR: process_cwd_mutation_reachability_gate (2 tests) fails identically on clean main 980761c.

Separate finding (compile walk, not changed here): interface_changed_consumers has the same dotted-flat admission. It is bounded there by interface-only propagation, so it over-plans compile seeds modestly rather than saturating.