Model the purpose standing, the non-execution consequence, and the admission wall

[briansrls]

The ranking key made executable. Stacked on #10161 (the taxonomy refinement), which it merges; review that first.

What this adds

Three types and three total folds in a new v2.workflow.floor_purpose_standing:

WitnessPurposeStanding   PurposeDeclared | PurposeUndeclaredGrandfathered | PurposeUndeclared
WitnessChangeStanding    WitnessChanged | WitnessUnchanged
NonExecutionConsequence  SilencedWall { refuser } | OpenQuestion | ConsequenceUndeclared

The consequence is the key. Only a BehavioralDiscriminator requiring a refusal silences a wall; every other purpose leaves a question open when it does not run. The SilencedWall arm carries the decision that stopped being checked — the difference between a count and a lead.

The two properties that carry the safety weight

ConsequenceUndeclared is not OpenQuestion. Collapsing them is the single change that would make this model fail open: unknown reported as the benign arm would let the entire grandfather roster read as carrying no walls on day one. Unknown is its own arm, counted, and never summed into either other.

The grandfather roster is debt, not an exemption — and purpose_admission_refuses enforces that rather than asserting it. A grandfathered identity that changed must declare before it is admitted again. So the roster can only lose members, and it loses them exactly when someone is already editing the row; the cost lands on whoever is there anyway. An untouched row is admitted — it carries yesterday's debt at no new risk. That is the shrink mechanism; without one the arm would be a permanent exemption wearing a debt contract's clothes.

Evidence — executed, with the degradations run as REDs

Seven controls green. The two that matter were mutated and confirmed red:

mutation	control that fires
report unknown as the benign arm	an_undeclared_row_is_unknown_rather_than_benign → false
drop the change standing from admission (roster stops shrinking)	a_grandfathered_row_must_declare_once_it_changes → false

Positive controls are included so that an admission refusing everything would not satisfy the wall tests, and a sibling control asserts a declared non-discriminator purpose silences no wall — so the key cannot be read as "anything that declared a purpose is load-bearing".

One substrate trap worth recording

v2.std.logic Bool is realized natively as a machine scalar, so a function returning the True/False variants produces a value the interpreter's match_pattern has no arm for. My first run of the key control came back false for exactly that reason. This module returns native true/false literals and reserves variant matching for its own coproducts, which are genuine variants. Noted on the import — required_floor records the same straddle from the pattern side, where an earlier revision matching True {} / False {} errored 11 of 19 witnesses.

Scope

Nothing wires this into the floor yet, so nothing gates on it and no admission behavior changes. The 500ms ceiling does not move, no budget widens, and a non-verdict on a required claim still blocks exactly as before.

Inert-roster state verified against main's baseline rather than against zero, using the same live entry point the gate calls: origin/main stale=0/unrostered=2, this branch stale=0/unrostered=2. The unrostered=2 is pre-existing on main and deliberately untouched — it reproduces with this diff absent, so absorbing it would claim a repair this change did not make.

🤖 Generated with Claude Code

https://claude.ai/code/session_0198WYhRXB3scqq262mtHqSx

[gunbai-bot]

On the inert-roster finding (review 59085) — I checked it against the gate rather than by inspection, and the omission is correct: those units are not inert by the lens's own definition, so a roster row for them would be a false entry rather than a missing one.

What inert actually means, read from the producer (compute_inert_carrier_data) rather than from the roster's prose: a carrier is inert when it is declared exactly once outside tests, referenced by some test, and its non-test occurrences minus its own type block's self-references come to ≤ 0. The subtraction is per block, so a reference from another block in the same non-test file counts as consumption.

WitnessPurposeStanding, WitnessChangeStanding and NonExecutionConsequence are each read by floor_purpose_standing.dag itself — in the signatures and bodies of non_execution_consequence, purpose_admission_refuses and the folds — which are blocks other than their own type declarations. So their consumption is positive and the lens does not class them as inert.

Measured against the live entry point the gate calls (inert_carrier_live_stale_roster_count / ..._unrostered_count), rather than asserted:

tree	stale	unrostered
origin/main	0	2
this branch, before my roster fix	2	2
this branch, now	0	2

If these three units were inert-but-unrostered, unrostered would read 5 here and 2 on main. It reads 2 on both, and those 2 reproduce on origin/main with this diff entirely absent — so they are pre-existing drift I have deliberately not absorbed, because doing so would claim a repair this change did not make and hide whose drift it is.

The review is right that inert_carrier.dag changed in this stack, and right about why — but the change was the opposite direction: I removed two rows (WitnessPurpose, DiscriminatedOutcome) that my own diff made untrue. DiscriminatedOutcome is consumed by the WitnessPurpose block itself, since the refined arm reads it, so the row I originally added for it was never true. WitnessPurpose is a pre-existing row that WitnessPurposeBinding made stale via its purpose: WitnessPurpose field. WitnessPurposeBinding stays rostered because nothing outside its own block reads it yet.

One genuine oddity I recorded in that commit rather than acted on, since it is the lens owner's call: the lens counts a sibling inert type as a consumer, so adding an inert carrier that references another inert carrier silently un-inerts the referent even though no production code reads either. That means the roster tracks reference topology rather than production consumption — two different facts under one name.

No change pushed for this item. Separately I did push a real fix to this stack: a CITED-MODULE-ABSENT failure where my fixture_refuser_ref cited dag.test.claim.witness_purpose_taxonomy_witness, a path no module declares.

— sent from crisp-crane-370

[gunbai-bot]

Both findings from review 59106 addressed, one by a fix and one by a measurement. Also amended the model itself after approval — details below, because it removes an arm.

Unused True, False import — fixed, and it was a good catch. They were imported and never used, in a file whose sibling documents why those variants must not be constructed. Removed, and replaced with a note saying why they are deliberately absent: leaving them importable puts the wrong spelling within easy reach of whoever edits these controls next.

The inert-roster finding — checked against the gate, and it does not hold. This is the second review to raise it, so here is the falsifiable form rather than a restatement.

inert is not "referenced only by a _test file". Read from the producer (compute_inert_carrier_data): a carrier is inert when it is declared once outside tests, referenced by some test, and its non-test occurrences minus its own type block's self-references come to ≤ 0 — the subtraction being per block.

WitnessPurposeStanding, WitnessChangeStanding and NonExecutionConsequence are each read by floor_purpose_standing.dag itself, in the signatures and bodies of non_execution_consequence and purpose_admission_refuses — blocks other than their own declarations. Their consumption is positive, so the lens does not class them as inert, and a roster row for them would be a false entry, not a missing one.

The check, run against the same live entry point the gate calls:

tree	stale	unrostered
origin/main	0	2
this branch	0	2

If these three were inert-but-unrostered, unrostered would read 5 here against 2 on main. It reads 2 on both. The 2 reproduce on origin/main with this diff absent — pre-existing drift I have deliberately not absorbed, since doing so would claim a repair this change did not make.

Amended after approval: the standing collapses to two arms

Scoping the wiring showed the grandfather roster should not exist. Enumerating the identities that predate the requirement means ~3500 entries — a second copy of the discovery output, and the kind of redundancy that rots against every witness rename (§2).

The change standing already carries the whole distinction: refuse undeclared and changed. An untouched old row is admitted with no entry; an edited row must declare; a new row is changed by construction, so the mandatory-at-admission wall falls out without enumerating anything.

That made PurposeUndeclaredGrandfathered unreachable by construction — nothing can distinguish "new" from "predating" without a roster. §4b calls an arm no producer can reach a decoration: permanently unconstructed and worse than absent once cited as covering the new-row case. Removed here rather than in the follow-up, so the approved artifact never advertises coverage it does not have.

The shrink guard is now satisfied by dissolution: there is no roster that could sit unshrinking, because there is no roster.

Controls re-verified, since collapsing an arm is where one gets eaten. Eight green, and every degradation still discriminates — including the direction a one-sided test would miss:

mutation	control that fires
report undeclared as the benign arm	..._unknown_rather_than_benign → false
admission constant false (never refuse)	..._must_declare_once_it_changes, a_new_row_..._is_refused → false
admission constant true (always refuse)	..._must_declare_once_it_changes, ..._is_admitted_which_is_the_implicit_debt → false

One assertion was deleted on purpose and is not a lost control: a_new_row_without_a_declared_purpose_is_refused previously required refusal on both change standings — the behaviour of the removed always-refuse arm. An untouched undeclared row is now admitted, so keeping that half would have contradicted the design rather than guarded it. It is replaced by an explicit test for the implicit debt, so both halves of the contract are asserted: refuse on contact, admit while untouched.

— sent from crisp-crane-370

[gunbai-bot]

review 59131 asks me to migrate five bare BehavioralDiscriminator => false patterns, or to "verify the pattern grammar admits the bare form for payload variants and drop this if so". I verified it. The grammar admits it and the bare form matches correctly, so I have not changed those arms — but the review was right to ask, because the five arms are in a position where being wrong would have been invisible.

Why the existing tests could not settle it. All five stale-looking arms sit in matches whose scrutinee is a different variant — e.g. a_declared_non_discriminator_purpose_silences_no_wall matches a PopulationTotality. Those arms never execute, so a pattern that silently matched nothing would leave every test green. Green tests were not evidence here, which is exactly the reviewer's concern.

The decisive probe. I built the case the corpus does not contain: a scrutinee that is a payload-carrying BehavioralDiscriminator, matched with the bare form.

match BehavioralDiscriminator { discriminates: RefusalRequired { refuser: r() } } {
  BehavioralDiscriminator => true
  BoundaryCrossing { modeled_boundary: _, chosen_input: _ } => false
  PopulationTotality { population: _ } => false
  ExternalFidelity { effect: _ } => false
  ResourceContract { bound: _ } => false
}

Result: returned true. The bare pattern binds a payload-carrying variant. Had the grammar rejected it, the module would have failed to resolve — resolve errors here are loud, and I hit one earlier in this same stack for an unrelated import. Had it parsed but matched nothing, the fall-through would have produced a runtime pattern-match-failure, which is how the sibling required_floor documents the native-Bool straddle behaving.

So this is not the "closed variants eliminate exhaustively" case: the arms do eliminate the variant, they simply do not destructure a payload they have no use for. The probe was temporary and is not in the diff.

One thing the review gets right that is worth keeping. The file is inconsistent in style — every other payload-carrying variant is matched with braces. I have left the bare arms because changing five patterns that provably work is churn on an approved diff, and because the inconsistency is now documented here rather than being a silent oddity. If you would prefer uniformity for readability, say so and I will migrate them; that is a style call, not a correctness one, and I would rather it be made explicitly than have me pre-empt it.

For completeness on this PR's other moving part: I amended the model after approval to collapse WitnessPurposeStanding to two arms, since the grandfather roster turned out to be derivable from the change standing and the third arm was therefore unreachable by construction. Details and the re-verified mutation table are in the comment above.

— sent from crisp-crane-370

[briansrls]

LANDING HOLD on exact head 08831e2. The latest cited-declaration repair is correct: watched_decision now names live_tree_frontier_verdict in its declaring module gunbc.self_host_compile_phase_live_gate, and exact-head run 33723236503 is terminal success. Two blockers remain. First, this stacked head is one commit BEHIND #10161's accepted annotation repair: compare 5270a0a...08831e2 is diverged with merge-base b1bbe32 and behind_by=1, and this head still contains the superseded claim that same-module authoring makes the population independently defined. Incorporate #10161's 5270a0a correction; do not reintroduce that claim. Second, current main is 2bba578 with #10166, a parser/occurrence-binding + stage0 change landed after this run, so fresh composition/CI is required under the standing materiality rule. Recommended sequence: land corrected #10161 first, then merge current main into #10174, resolve witness_purpose.dag to the corrected prerequisite text, and rerun exact-head CI.