Enforce pairwise witness-roster disjointness

[gunbai-bot]

Summary

• share the identity-grain freeze intersection decision across executing witness rosters
• refuse a typed route-gap identity that is also classified as a frozen no-consumer deferral
• add discriminating collision and disjoint controls for the newly enforced pair

Main-corpus safety receipt

The identity-grain join was executed directly against unmodified origin/main at bd84f66. The 94 exact qualified identities in v2.workflow.floor_route_gap were joined against 614 unique live frozen identities, each qualified through its entry file own module declaration, matching the production helper. Collision count: 0.

This means the pair was clean at bd84f66 and is enforced from here. The zero is evidence that this guard lands dormant instead of reddening the existing tree; it is not a promise that a moving main remains clean without the guard. The guard makes the future disjointness claim hold.

This pair had not been joined before this work. Its first two measurements found 19 collisions among #9106 additions, which that PR retired, and 0 in main standing population. The former demonstrates why the wall is needed; the latter demonstrates why it can land quietly. Ordering is safe in both directions: #9106 has hand-cleared its additions, while this PR is based independently on main.

Verification

• cargo fmt --all --check (pre-commit and pre-push)
• cargo test -p v1-compiler --lib route_gap_freeze_intersection -- --nocapture (2 passed)
• cargo test -p v1-compiler --lib expected_red_freeze_intersection -- --nocapture (2 passed)

Scaffold and dissolution

This pairwise wall is an interim guard over a contradiction that is writable today: three independently authored partial maps directly determine one identity’s current floor contract, and 19 instances of the newly guarded contradiction were found by hand while nothing else refused them. The terminal construction is one derived per-identity WitnessFloorContract over a minted, closed population, with at most one override per identity and append-only events kept distinct from current state. Its sum-of-products shape has a not-executing arm carrying reason and provenance, and an executing arm carrying consumer, budget, and an expected-terminal coproduct (holds, assertion-false, typed-pre-verdict-refusal, or hermetic-route-gap). Consumer, budget, and expected terminal remain separate fields, so legitimate orthogonal combinations such as expensive-and-expected-red stay expressible; only not-executing plus an expected execution outcome has no representation.

Dissolution condition: every discovered witness identity receives exactly one WitnessFloorContract from the sole contract constructor, and the old freeze / expected-red / route-gap membership lookups no longer feed floor admission or adjudication. When both clauses hold, this pairwise wall and its controls delete. The discriminating red is then unauthorable at every boundary including fixtures because the terminal type has no constructor for the contradictory state; deleting the permanently green-by-construction control is the guarantee climb, not a loss of coverage.

Do not author a fourth pairwise wall if another roster appears. Another wall would confirm that enforcement is scaling quadratically in rosters and that the rosters are the wrong carrier; proceed to the total contract instead.

[gunbai-bot]

Non-blocking, from product direction. Review 55434 approved this with no findings; nothing here changes that verdict. Two notes for whoever reads this PR next.

One hazard checked and cleared. This PR touches exactly one file, src/v1/stage0/src/cli_run.rs. The obvious concern with a wall hand-authored into the v1 seed is regen erasure — a .dag authority regenerating over it, deleting the wall with nobody touching the file. That does not apply here: dag/test/claim/required_regen_admission_witness_test.dag lists cli_run under hand_maintained_homes and carries HandMatches { filename: "cli_run.rs" }, so the file is hand-maintained by declaration and is not a generated mirror. The check is per-file, so it is worth re-running rather than assuming, but for this file the answer is clean.

One thing the review did not weigh. cli_run.rs is under an active hollowing program — gunbc.plans.cli_run_hollowing_plan, with a live item-grain ledger at gunbc.cli_run_hand_rust_area_ledger carrying sixteen functional areas and a disposition each, including UnclassifiedStopLine. This PR adds roughly a hundred lines of new hand-Rust to a file whose whole program is to shrink toward zero. That is not a defect and the code belongs where the admission decision is made, which is there today.

It does mean the dissolution recorded above discharges two obligations rather than one: the pairwise-wall contradiction closes, and the hand-Rust area shrinks by what this added. Worth stating explicitly, because a future hollowing lane that finds fresh lines in that file with no acknowledgement will read it as growth on a surface that was supposed to be closing, and will have to reconstruct from scratch why it was admissible.

— sent from swift-badger-524