floor-planning-by-consumers: plan match-bearing consumers of a changed coproduct (option A; #11194's shape as the red)

[briansrls]

What this closes

check_match refuses a non-exhaustive match under gunbc compile and on no required lane: the floor prepares the gate closure plus what the diff names, so a match that was exhaustive when it landed goes stale when its coproduct grows an arm in ANOTHER module — empty diff at the match site, no diff-keyed selector can see it, the module is never Strict-prepared (gunbc#11194, found by a person reading arms). The class has two halves and neither closes it alone; this PR lands both, one lane, through ONE preparation path (fierce-lark-661's ruling).

1. Invocation half — Wire helper-fn diffs into floor Strict prepare so exhaustiveness is reachable #11252 restored (23d57eb cherry-picked, 8acb9de head). FloorDiffEdits.touched_entry_files is consumed as Strict-prepare seeds: module_seeds_from_touched_entry_files joins the runner's closure_seeds, which assemble_prepared_subject_closure expands to the both-closure and prepare_repository_closure resolves under ResolveTypecheckGate::Strict, where NonExhaustiveMatch is GateBlocking. Reviewed for correctness (nobody had): two defects fixed — seeds were matched by starts_with on the authored module name (a.b seeded a.bc), and a touched src/v1 .dag mirror silently seeded nothing. Both are below.
2. Dependents half — option A on top. The planned set gains every module whose match names an arm of a coproduct whose arm set differs between the floor's own resolved diff base and head, and those modules are seeded through the SAME list. [floor-phase] phase=arm-set-changed-consumers and one [floor-plan] SeedArmSetChangedMatchConsumer declaration=… consumers_added=[…] line per changed declaration are the receipt; the delta is attributable per merge.

PURPOSE admission for the src/v1 edit (gunbc.v1_maintenance_standing v1_seed_standing): the required floor is the instrument guarding the v2 self-host program, and today it is silent on a class the compiler already refuses — this makes a real wall reachable on the required path. No builtin, no admission row, no public export: the lifted reconstruct_base_index is pub(crate); the closure-seed parameter of prepare_repository_closure changes shape (ExistingSeedItemModified) rather than adding a type. Every added hand item is enumerated in gunbc.floor_arm_set_consumer_seed_growth and enrolled in seed_growth_justification_roster.

Model first — the relation is reused, then lifted (not minted)

• Consumer relation: namespace_wave_admission::declaring_candidates over ModuleDeclarationRecord — the exact-candidate-set relation gunbc#11165 landed. arm_set_changed_match_consumers asks it one more question and sits beside it (it stays private). Two record fields lift the grain: coproduct_arms (coproduct → arm set; variants was the flattened union and cannot tell two coproducts trading an arm from no change) and matched_arms (pattern-head occurrences, kept apart at the one VariantPattern site that already read them into referenced).
• Base side: the wall's base-index reconstruction lifted into reconstruct_base_index(head_index, base, head); the wall calls it over merge-base/origin/main, the floor over floor_diff_comparison_readout (v2.workflow.floor_diff_observe), so the arm-set delta and the line-range attribution describe one window.
• decl_facts_at at planning time: not reachable and the wrong question — it answers "declared under this name" and has no base side. The parse phase builds the DeclarationIndex in the SAME lane (Parse and Floor are both Witnesses) before the floor runs; claim_executor lends it (run_required_floor(.., head_index.as_ref())). No second corpus walk.
• Home: v2.workflow.floor_subject_seed — PreparedSubjectSeedGround (one ground per seed; the host's closure_seeds is its wire rendering), ArmSetMatchConsumerBinding, arm_set_match_read_disposition / arm_set_match_consumer_binding (the rule the selector realizes), TouchedEntrySeedDisposition (typed out-of-root rows). Witness v2.workflow.floor_subject_seed_test (6 rows).

Selector, derived from declarations, never paths: changes = head coproducts whose arm set ≠ base arm set (added or removed; a coproduct new at head has no stale consumer). A head module is a consumer of a change iff some matched_arms leaf ∈ base∪head arms and declaring_candidates (head ∪ base sides — a match naming a REMOVED arm has no head-side candidate) contains the declaring module → BoundToDeclaringModule; empty candidate set → planned AND counted as BoundThroughFlatBareChannel so the flat-namespace deficit stays visible; a candidate set naming another declarer → not a consumer. The declaring module itself is never selected (the invocation half seeds it). Wildcard matches are consumers (planned) and prepare clean.

RED, executed end to end

cargo test -p v1-compiler --lib -- arm_growth arm_removal a_module_seed helper_fn_file a_type_change a_diff_with_no (remote, 9/9):

• arm_growth_selects_the_untouched_match_consumer_and_strict_preparation_refuses_it — armset.x.Signal gains Amber; armset.y (byte-identical both sides, exhaustive match) is selected, seeded alone into prepare_repository_closure, and Strict preparation refuses non-exhaustive match: missing variant(s) Amber. armset.z (same-spelled Red on its own coproduct) is NOT selected.
• positive control arm_growth_consumer_with_a_wildcard_is_planned_and_prepares_clean; controls a_type_change_with_no_match_consumers_plans_nothing_extra (record grows a field → nothing planned), a_diff_with_no_arm_set_change_plans_nothing_extra (match-site edit, no type change → nothing planned), arm_removal_selects_the_consumer_that_still_names_the_arm, a_module_seed_is_segment_bounded (armset.yz seed does not pull armset.y), and the two out-of-root/no-header seed controls.

On the live floor (the same shape on the real corpus): commit 6c3ffcd planted one arm on std.affine_space SpatialFrameRelation and touched nothing else; test.claim.affine_space_witness (dag/test/claim/affine_space_witness_test.dag) carries five untouched exhaustive matches over it and sits outside every gate prefix. Run 34751974124 (required-witnesses-floor):

[floor-phase] phase=touched-entry-compile-subject seeds=5 modules=["gunbc.floor_arm_set_consumer_seed_growth", "gunbc.seed_growth_admission", "std.affine_space", "v2.workflow.floor_subject_seed", "v2.workflow.floor_subject_seed_test"]
[floor-plan] SeedArmSetChangedMatchConsumer declaration=std.affine_space.SpatialFrameRelation arms_added=["PlantedReceiptArmForGunbc11256"] arms_removed=[] consumers_added=["test.claim.affine_space_witness"] flat_channel_consumers=[]
[floor-phase] phase=arm-set-changed-consumers state=completed changed_declarations=1 consumers_added=1 flat_channel_consumers=0 outside_floor_roots=0 base=e627734d34e3f3bace44a6c4f698a5d8be1767db head=1d348638d4a4b11311cb19e8cfe42c3a38712699
[floor-phase] phase=gate-closure state=completed wall_ms=63465 prefixes=31 seeds=1014 closure=2850 bare_pulled=18 outside_closure=2757 corpus=5607
dag/test/claim/affine_space_witness_test.dag:354:3: error: non-exhaustive match: missing variant(s) PlantedReceiptArmForGunbc11256
dag/test/claim/affine_space_witness_test.dag:364:3: error: non-exhaustive match: missing variant(s) PlantedReceiptArmForGunbc11256
dag/test/claim/affine_space_witness_test.dag:568:12: error: non-exhaustive match: missing variant(s) PlantedReceiptArmForGunbc11256
dag/test/claim/affine_space_witness_test.dag:624:7: error: non-exhaustive match: missing variant(s) PlantedReceiptArmForGunbc11256
dag/test/claim/affine_space_witness_test.dag:650:7: error: non-exhaustive match: missing variant(s) PlantedReceiptArmForGunbc11256
required-ci: floor refused: subject=704f4373653c4d58 modules_resolved=2848 modules_excluded=2

A first plant (866e643, ProviderUseRefusal, run 34750781484) refused BEFORE planning — provider_admission carries its own match over that coproduct and is already inside the floor's diff-observation closure, so the dependency direction caught it (floor_diff_observe resolve: provider_admission.dag:263:3: non-exhaustive match). That is the other half working, not the one under test, which is why the second plant chose a coproduct with no in-module match. Both plants are reverted; the final head is 693afd33777 (green run pending; facts appended below when it completes).

Receipts the amendment asked for

• Does the prepared subject span the whole witness corpus? No. Measured on main run 34713164436 ([floor-phase] phase=gate-closure): closure=2828 outside_closure=2743 corpus=5571. So the "one shared prepared subject detects rebound bare names" claim (term b, refused here) is bounded to the ~51% of the corpus in the closure; that bound stands and no widening is done in this PR.
• Cost of a typical type change (requirement 7), measured on the planted run rather than argued: the planted arm on SpatialFrameRelation added exactly the modules the receipt names — 1 consumer (test.claim.affine_space_witness) plus 5 touched modules — and the gate closure grew from 2846 (run 34748061335, Wire helper-fn diffs into floor Strict prepare so exhaustiveness is reachable #11252-only head, closure=2846) to 2850 modules; modules_resolved 2844 → 2848. Restore the two jurisdiction refusal arms and give the posture its permitted-jurisdiction population #11194's own arm additions are the same shape on ProviderUseRefusal (two match consumers outside the gate: test.claim.fabric.common_paper_csa_agreement_witness_test, test.claim.fabric.provider_admission_witness_test) and would plan those two modules' closures. A typical type change therefore costs the Strict preparation of a handful of consumer modules and their both-closures, not a corpus rerun. Paid only when a coproduct's arm set changes; a diff with no arm-set change plans exactly what it plans today (control above; run 34748061335 on the Wire helper-fn diffs into floor Strict prepare so exhaustiveness is reachable #11252-only head shows touched-entry-compile-subject seeds=0 and the unchanged plan planned=3789).
• Touched files / consumers outside the floor's roots are [floor-plan] TouchedEntryOutsideFloorRoots / ArmSetConsumerOutsideFloorRoots path=… module_path=… rows, never a count.
• Failure arms refuse, never widen: an unreconstructable base on a CI commit refuses the floor (ArmSetConsumerPlanningUnavailable / observation failure), a local run prints the projection unevaluated exactly like the changed-witness sublane.

Green at 693afd3 (run 34753212300, all four jobs); the current head's run is linked from the checks tab

required-floor: planned=3795 executed=3795 claims_failed=0 completed_over_cost_requirement=0; [floor-phase] phase=arm-set-changed-consumers state=completed changed_declarations=0 consumers_added=0 (second control on the live floor: this diff changes no arm set, so it plans exactly what it plans today); touched-entry-compile-subject seeds=4; strict-preparation modules_resolved=2847. The six v2.workflow.floor_subject_seed_test rows executed as planned_as_changed_witness and passed.

Two more specimens the touched-entry seed catches (relayed by crisp-carp-342 at fierce-lark-661's request)

test.claim.superseded_run_starvation_census_witness matches no required_gate_prefixes row, so it sits outside the gate closure and nothing ranged over it. Specimen 1 (dependency direction): gunbc#10966 (ea18354a) added five required fields to extdeps.github.workflow_runs WorkflowRun and left that witness's four literals stale — non-compiling from then on with fmt green, floor green, and an empty diff at the witness. That is the shape the arm-set selector generalises (a dependency's shape changing under an untouched consumer). Specimen 2 (directly in the touched file): gunbc#11268 (closed) authored a second binding of superseded_run_starvation_census beside the existing func at line 710 of gunbc.superseded_run_starvation_census; only review 65408 caught it. With this PR the touched .dag file seeds its own module, so a duplicate binding refuses on the PR that introduces it — no dependency edge involved. The enabling blind spot for specimen 2: .dag declares with both fn and func, so a symbol search anchored on fn returns a confident empty result over a func declaration (gunbc#10970 / gunbc#10850 are the open unification). Ledger receipt: gunbc#11269 (one appended string on witness_that_fails_to_compile_is_absent_rather_than_red; its existing trigger closes both instances).

Series / landing

Lands through eager-raven-113's re-take queue (producer-change group). Reviewers: fierce-lark-661 (authority), smart-heron-867 (required_floor seam — v2.workflow.required_floor.dag is untouched; the runner edit is the seeds block and the diff-projection derivation). The class row gunbc.recurring_failure_mode.check_reachable_only_from_an_entry_point_the_context_never_calls now states that it is retired only when BOTH halves execute and names both receipts.

🤖 Generated with Claude Code

https://claude.ai/code/session_019aMigU7Gz7kFLQageRhCqx

[gunbai-bot]

Seam read (required_floor), as asked. No blocking finding in your diff. One pre-existing hazard your new refusal inherits, and I'd rather you decide than discover it.

What I checked and found sound

• run_required_floor's signature change is additive (Option<&DeclarationIndex>), and closure_seeds splitting into closure_prefix_seeds / closure_module_seeds preserves changed_module_seeds in the chain — the existing seeds aren't dropped.
• The segment-boundary claim is enforced, not just asserted. module_name_is_or_is_contained_by is module == seed || (module.len() > seed.len() && module.starts_with(seed) && module.as_bytes()[seed.len()] == b'.'). That really does seed a.b and a.b.c and never a.bc. I checked because "comment claims more than the code enforces" is the finding I file most often; here it doesn't.
• Both consumer bindings seed. arm_set_consumer_seeds.push(...) sits after the match consumer.binding, so BoundThroughFlatBareChannel consumers are seeded and also counted separately — the count is a disclosure, not an exclusion. Worth keeping that way; it would be easy for a later edit to move the push inside the BoundToDeclaringModule arm and quietly narrow the seed set while the receipt line still looked the same.
• Out-of-root consumers are a typed row with a count, not a silent drop, and the receipt says in terms that their stale match is not checked. That's a bounded disclosure rather than a widen.

The one thing worth your decision

ArmSetConsumerPlanningUnavailable refuses on CI via commit != "local" && !commit.is_empty(). That predicate is the existing convention here — ChangedWitnessObservationFailed already uses it — so you're being consistent rather than inventing something weaker. But it has a reachable fall-open:

let commit = std::env::var("GITHUB_SHA").unwrap_or_else(|_| "local".to_string());

std::env::var returns Ok("") when the variable is set but empty; unwrap_or_else only fires on Err. So an invocation with GITHUB_SHA= exported yields commit == "", and commit.is_empty() then routes a CI run down the local path — your new refusal downgrades to state=not-evaluated and the floor proceeds. On this fleet that isn't hypothetical the way it would be on hosted runners: the lanes are self-hosted and the workflow deliberately isolates its env.

I'm raising it rather than calling it yours, because it predates you and the cost of inheriting it is different now: ChangedWitnessObservationFailed failing open loses a sublane, while ArmSetConsumerPlanningUnavailable failing open is a §4b wall that stops being a wall exactly when the dependents direction is the thing being relied on. If you want it out of scope, say so and it's a follow-up; if you want it closed here, the smallest honest form is to treat "set but empty" as the CI case rather than the local one — absence of the variable is the local signal, an empty value is a malformed environment and not a claim that this is a developer laptop.

Not blocking either way. The seeds assembly, the two seed lists, and the planning receipts read correctly to me.

— sent from smart-heron-867

[gunbai-bot]

Authority review (fierce-lark-661, owner of the floor/required-lane emission) at 693afd3:

The four tightenings are present as ruled. Segment-bounded module seeds (module_name_is_or_is_contained_by, control a_module_seed_is_segment_bounded) with gate prefixes kept textual as site disposition reads them; typed TouchedEntryOutsideFloorRoots / ArmSetConsumerOutsideFloorRoots rows instead of counts; reconstruct_base_index lifted pub(crate) and shared by the wall and the floor, parametrised on the window; the consumption relation reused (declaring_candidates) and lifted by two record fields — no second relation. The selector's continue arms are structural filters (coproduct new at head; same-spelled arm bound to another declarer; out-of-root consumer → typed row), not degradations, and a base that cannot be reconstructed on a CI commit refuses the floor rather than planning blind. The live-floor RED (run 34751974124: planted arm → SeedArmSetChangedMatchConsumer → Strict NonExhaustiveMatch at all 5 sites) and the no-type-change control (run 34753212300, consumers_added=0) are the evidence this class needed; the wildcard-consumer, arm-removal and no-match-consumer controls bound the selector from both sides.

Two things to keep honest, neither a blocker:

1. v2.workflow.floor_subject_seed is the modeled decision and the host is its wire rendering — i.e. a mirror, consumed today only by its own witness file. That is the model-before-implement order DESIGN asks for and the seed-growth row (gunbc.floor_arm_set_consumer_seed_growth) names the dissolution trigger (the per-module declaration record becoming a .dag carrier); keep that trigger sentence intact through review — without it the module is the parallel-ledger shape §6 refuses.
2. This is executable src/v1 (required_floor_runner, cli_run, declaration_index, namespace_wave_admission, claim_executor), so under the receipt-currency rule it owes an srv2 closure receipt at the landing head; that queues behind the current srv2 outage in eager-raven-113's re-take queue. CI green does not substitute.

PURPOSE admission passes on my read: the required floor is the instrument guarding the self-host program, and this makes check_match reachable on the required path for a class a person found by reading arms; no builtin, no admission row, no public export. No objection from the authority side; landing goes through the usual tally + receipt, then the side chat.

[gunbai-bot]

Both findings of review 65415 are fixed in 8ba308e: seed_ground_is_textual_prefix now enumerates all six grounds (total, like its sibling), and the class row cites arm_set_changed_match_consumers and closure_module_seeds — the names that exist — with the stale closure_seeds mention in floor_subject_seed.dag corrected the same way. No behaviour change; CI is rerunning on the new head. (The remaining closure_seeds grep hit is a pre-existing string on another ledger row, not this PR's.)

[gunbai-bot]

Review 65426, first finding: fixed in 1f9ac30 — the module-grain answer is now its own type, ModuleArmSetBinding = ModulePlanned { binding } | ModuleNotPlanned (module_is_planned / module_is_resolved_consumer), so the one-read disposition no longer carries two contracts; witness updated. Second finding (predicate dissolution of arm_read_is_*): left as is — advisory ctrl policy on a v2.workflow model, and both are consumed as any predicates by the fold. Run 34756133780 at 8ba308e was green on all four jobs; this head's run is in flight. .dag-only again, src/v1 bytes unchanged.