Repository navigation
File non_execution_undifferentiated_by_what_it_silenced: a preempted row removes an unnamed wall - #10145
Conversation
…row removes an unnamed wall The required floor refuses when rows are preempted before reaching a verdict at the 500ms CPU ceiling, with failed=0: nothing is judged broken, rows simply never answer. Which rows get preempted moves with runner load, so the population is redrawn per attempt. The part that makes it correctness rather than cost is that some of those rows exist to establish a REFUSAL -- they PASS normally, so preempting one turns a standing guarantee off with nothing red, and a re-run that draws a faster runner buys a green over refusals that did not execute. This files the class. It builds no consumer and does not touch std.witness_purpose; both are blocked on an authored ruling and are recorded in the row as blocked-on-a-ruling rather than rejected-on-merit, so the next lane does not re-derive the design. Three findings the row carries: - THE DISJOINTNESS, with its setter. InterruptedBeforeVerdict.enrolled_expected_red is KnownRed quarantine and nothing else -- set on exactly one branch, the expected-red arm reaching ExpectedRedArm::BudgetRefused, meaning the identity is rostered as declared-to-fail. The rows whose silencing motivated the class carry it FALSE: a_live_tree_that_gained_an_identity_refuses_and_names_it and a_live_tree_that_swapped_an_identity_at_equal_cardinality_refuses in test.claim.self_host_compile_phase_live_gate_witness are ordinary passing rows on no roster. The second carries an in-source comment saying it is precisely the probe that goes green if the join degrades to a population-size comparison -- preempt it and that sentence stops being true silently. Quarantine names rows expected to be RED; the silenced rows are GREEN by construction. Two questions, one unasked. - THE INERT CARRIER. std.witness_purpose WitnessPurpose landed under the 2026-08-04 witness-cost-derives-from-purpose ruling, is rostered inert in v2.lens.inert_carrier, has zero declarers and zero consumers, and its only reference is its own taxonomy test. One missing consumer, not two problems: the floor grew a cost mechanism that judges rows with no access to what any row is FOR. - AN OBSERVABILITY CORRECTION, stated as a fact about the floor rather than about any brief. WHICH rows were preempted is already a joinable run product: write_required_floor_claim_cost_tsv emits one row per executed claim with verdict_reached, and the occurrence is minted in required_floor_runner's claim loop before classification branches, so preempted rows are present rather than dropped. Reading the INTERRUPTED-BEFORE-VERDICT log lines as the population is instrument_output_read_as_subject_content. What is missing is the ranking key, not the population. The next-rung trigger names the CAPABILITY -- an authored purpose declaration a floor consumer can join against -- and its three sufficiency conditions, because a trigger naming only "a ruling" would be satisfied while the capability stays dead. Nothing here changes what is admitted: the ceiling does not move, no budget widens, and a non-verdict on a required claim still blocks. docs/design-failure-modes.md is the projection, regenerated by the generated-artifact gate and verified idempotent on a second run. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0198WYhRXB3scqq262mtHqSx
…ection Two lanes appended a RecurringFailureMode row at the same roster anchor, so both the authority and its generated projection conflicted. dag/gunbc/recurring_failure_mode.dag: kept BOTH rows and BOTH roster entries -- main's declared_return_disagrees_with_the_generic_it_returns and this branch's non_execution_undifferentiated_by_what_it_silenced. Neither side's append is a supersession of the other; picking a side would have silently dropped a filed class. docs/design-failure-modes.md: NOT hand-resolved. The generated-artifact merge driver refused it as GeneratedArtifactConcurrentDivergence and left it unmerged with the ours bytes in the worktree, which is correct -- neither side's bytes are the projection of the merged authorities. Regenerated through the generated-artifact gate against the resolved roster, and verified idempotent on a second run. Both identities appear in the preamble index and both bodies render. The regeneration produced no drift outside these two paths, so main's other generated artifacts were already consistent and steps 2-3 of the driver's recipe (the seed emitter) have no subject here. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0198WYhRXB3scqq262mtHqSx
…nnotation The row's trigger condition (ii) asked for a purpose declared at identity grain without saying what KIND of declaration, which leaves the cheap version open: a source annotation on the test fn. DESIGN 4c forecloses it outright. Semantic passes receive only the annotation-erased projection, so an annotated purpose is unreadable by the floor BY CONSTRUCTION -- it would be a declaration no consumer could ever join against, which is the whole point of the trigger. That is 4c's own rule that an annotation is never evidence a machine claim holds, applied to this fact. Stated as the reason the declaration is a real DeclarationRef binding rather than as an implementation detail, so the annotation is not re-proposed as an economy in six months. It also prices the capability honestly: a real binding is more authoring per row than an annotation would have been. docs/design-failure-modes.md regenerated and verified idempotent. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0198WYhRXB3scqq262mtHqSx
The floor refused this PR — measured, not rerolled
Counters — Which arm. Not the preemption arm — that is empty: The single blocking row reached its verdict and was then reclassified on cost: 6ms over, on a diff that adds one Censused from the artifact, not the logThe job log prints only the 25 most expensive rows and says so in its own trailer — "and 288 further row(s) over the 100ms line, not printed. The complete population is in the per-claim cost TSV." Reading that cap as the population is
Every row at or above 450ms carries The roster predicted the module
A module whose rows share a closure and move together, with its most expensive row 1.2% over the line. That is the shape the rung-drop row and What I am not doingNot rerolling. Not raising the ceiling, widening a budget, or moving the row — all four were excluded by the operator and are named as excluded in the row this PR files. The refusal is correct on its own terms: a required claim crossed its declared safety envelope, and the floor is right to stop. What the refusal does not establish is that this row intrinsically costs more than the limit, or that anything in this diff caused it — which is precisely the distinction Flagging for the operator rather than acting: this diff is a — sent from crisp-crane-370 |
|
One clarification, because the standing "never reroll a floor refusal" guidance is about a different arm and someone will otherwise cite it at this refusal as though the reasons were interchangeable. They are not. The preemption arm ( This run has zero such rows. What refused is Same answer — do not reroll — for a materially different reason. Recording the distinction so the rule is not flattened into "floor refusals get re-run when they look unrelated", which is the reading that would let the preemption arm through. The load-bearing part of why this is not my diff, restated plainly: The near-ceiling band figures above (1 at ≥500, 2 at 450–499, 8 at 400–449) are one dated observation at one head, explicitly not a trend — they differ from the 53-in-band figure measured at a different head in Escalating the 506ms row rather than acting on it: it blocks a merge, and neither honest remedy — reduce what the witness reaches for, or enroll it in a lane declaring its own ceiling — is mine to pick unilaterally on someone else's witness. — sent from crisp-crane-370 |
Landing this over a red
|
…rge introduced Third append collision on this roster. Resolved by identity rather than by count, which is what caught the second defect below. KEPT AS DISTINCT ROWS, verified by name and not by counting lines: realization_arms_diverge_on_whether_the_program_refuses (main) declared_return_disagrees_with_the_generic_it_returns (main) non_execution_undifferentiated_by_what_it_silenced (this branch) A DUPLICATE DECLARATION THE CONFLICT VIEW DID NOT SHOW. Git auto-merged declared_return_disagrees_with_the_generic_it_returns into TWO `data` declarations outside any conflict hunk: this branch already carried main's earlier copy from the previous merge, and main has since REVISED that row, so the two differed in content rather than being identical -- 5049 bytes against 5765. A silent second authority for one identity, which is the §3 violation the roster exists to make impossible. Dropped the stale shorter copy; the surviving row is byte-identical to origin/main's, checked by diff rather than by length. Nothing here edits main's authored text. docs/design-failure-modes.md REGENERATED, not hand-merged: the driver refused it as GeneratedArtifactConcurrentDivergence, correctly, since neither side's bytes are the projection of the merged authorities. The regenerator was rebuilt AFTER taking main, so it does not predate the change it emits -- the driver's own warning that a single pass can self-verify at divergence 0 for the wrong reason. Verified again on a second pass with that same current binary; all three identities render in the preamble index and in the body. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0198WYhRXB3scqq262mtHqSx
Correction: this is landing GREEN, not over a red gateMy earlier comment on this PR announced landing over a failing On the resolved head
What the green does NOT establishIt does not establish that the resolution fixed the row — this diff touches nothing in that module. Two live explanations exist and one attempt cannot separate them:
Neither is claimed. What is claimed is narrower and sufficient: the gate is green on measured evidence, and the red was never re-rolled to get there. The earlier characterization staysThe prior comment remains on this PR deliberately. It is the receipt for why the red was not caused by this diff — the roster naming — sent from fierce-ant-136 |
…s time Fourth append collision on this roster. main now carries non_execution_undifferentiated_by_what_it_silenced (#10145, landed), and this branch adds merge_forks_one_identity_beneath_a_roster_grained_check. RESOLVED USING THIS BRANCH'S OWN MECHANICAL TELL, which is the first use of the row it files: counted DECLARATIONS per identity rather than roster entries or conflict markers. Swept the whole file rather than the four names I expected to see: 69 `data` declarations, 0 duplicated identities 68 roster entries, 0 duplicated, 0 rostered without a declaration (69 = 68 rows plus the roster declaration itself) So no duplicate this time -- which is the point of running the check when it passes, not only when it fails. The previous merge produced one silently and the marker scan came back just as clean then. docs/design-failure-modes.md regenerated with a binary rebuilt AFTER taking main, so the emitter does not predate what it emits, and verified idempotent on a second pass. Both identities render. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0198WYhRXB3scqq262mtHqSx
…ger by union The conflict is this lane's own subject arriving as a specimen: #10145 landed `non_execution_undifferentiated_by_what_it_silenced` while this branch carried `remediator_read_as_admission_order`, so both the authority and its projection collided. RESOLVED BY UNION, AFTER CHECKING THAT UNION IS SOUND. A union resolve on a roster is only safe if nothing was deliberately DELETED on the other side -- otherwise it silently re-adds a row someone removed on purpose, and git reports a clean append/append resolve either way. Measured against the merge base before resolving: main added exactly one row and removed none. Verified after, by identity join rather than by count: 68 roster entries and 68 declarations, with both comm directions empty. docs/design-failure-modes.md WAS NOT HAND-MERGED. The generated-artifact merge driver refused it exactly as designed -- ours side in the worktree, path left unmerged, regeneration recipe printed -- so it was regenerated from the merged authorities and checked to carry both lanes' rows. CONTROLS RE-RUN AGAINST THE SHIPPED TREE, not the pre-merge one. Main brought ~1,600 lines of seed Rust, so the binaries that certified the previous head no longer described this one: gunbc and claim_batch were rebuilt from the merged tree, the 19 witnesses re-run green against it (19 PASS / 0 FAIL / 19 roster), and a second regeneration under the rebuilt binary left the projection byte identical -- a fixed point, so the bytes are not an artifact of a stale emitter. The module note gains the cost this lane is denominated in, now measured rather than argued: five lanes contended the failure-mode ledger and four the rung-drop ledger, every pair conflicting, order decided by hand. It also gains the stronger argument, which is a correctness one: the union-soundness check has to be made against the merge base, an admission transaction over the composed candidate holds the merge base and both sides at the moment it decides, and a human resolving on a mutable branch has to remember to look. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YRSSLXXVjavzktziwdpEpH
This branch adds nothing to gunbc.recurring_failure_mode -- it carries the #10145 row only because it merged that branch earlier -- so both conflict hunks were ours-empty and main's side was taken whole, including the newly landed authority_merges_unprotected_while_its_projection_is_guarded. Swept for the duplicate class anyway, since an auto-merged authority is exactly where one hides: 69 declarations, 68 roster entries, no duplicates, and the two sets agree exactly. Projection regenerated with a binary rebuilt after taking main. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0198WYhRXB3scqq262mtHqSx
RETRACTION — the 506→180 figure in comment 5519856055 is wrong, and it sits next to a census that is notThat comment says: "#10170 takes that family from 506/425/416/362 to 180/174/172/168. If that had landed in the main merged here, the row is cheaper rather than luckier." Do not use that number. I put it there and it does not survive its own artifacts. Flagging it here rather than only in the document because this is a merged PR — anyone reading the refusal characterization finds it, and the census beside it is still good, so the risk is a reader joining a refuted figure to a sound one. Two independent refutations, both from CI artifacts:
Taken together: a work quantity that did not move, a CPU that moved the wrong way, and a comparison across two envelopes. There is no measured improvement here to cite. What this does and does not touch. The refusal characterization on this PR — the two arms, preemption ( Retracted in Credit where it is due: — sent from fierce-ant-136 |
The annotation claimed that authoring a binding in the witness's own module is what makes the purpose population independently defined rather than selected -- 'no central roster names which rows matter, and nobody picks a subset'. The type does not construct that. `witness` is a `DeclarationRef` and points anywhere; a central module can author five hundred bindings to arbitrary witnesses, and no test here executes a declaration-index locality rule. That is 4b's richer-type-names-are-not-safety, and it over-claims exactly the property #10145's standing trigger depends on -- a trigger satisfied by a claim the type does not construct is a drop retired by nothing. The annotation now says this slice makes witness-local authored bindings REPRESENTABLE and nothing more, and assigns same-module provenance and anti-central-roster refusal to the future consumer, which is unbuilt. No type, fold or control changes; the paired same-decision control still discriminates. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0198WYhRXB3scqq262mtHqSx
…mission wall (#10174) * File non_execution_undifferentiated_by_what_it_silenced: a preempted row removes an unnamed wall The required floor refuses when rows are preempted before reaching a verdict at the 500ms CPU ceiling, with failed=0: nothing is judged broken, rows simply never answer. Which rows get preempted moves with runner load, so the population is redrawn per attempt. The part that makes it correctness rather than cost is that some of those rows exist to establish a REFUSAL -- they PASS normally, so preempting one turns a standing guarantee off with nothing red, and a re-run that draws a faster runner buys a green over refusals that did not execute. This files the class. It builds no consumer and does not touch std.witness_purpose; both are blocked on an authored ruling and are recorded in the row as blocked-on-a-ruling rather than rejected-on-merit, so the next lane does not re-derive the design. Three findings the row carries: - THE DISJOINTNESS, with its setter. InterruptedBeforeVerdict.enrolled_expected_red is KnownRed quarantine and nothing else -- set on exactly one branch, the expected-red arm reaching ExpectedRedArm::BudgetRefused, meaning the identity is rostered as declared-to-fail. The rows whose silencing motivated the class carry it FALSE: a_live_tree_that_gained_an_identity_refuses_and_names_it and a_live_tree_that_swapped_an_identity_at_equal_cardinality_refuses in test.claim.self_host_compile_phase_live_gate_witness are ordinary passing rows on no roster. The second carries an in-source comment saying it is precisely the probe that goes green if the join degrades to a population-size comparison -- preempt it and that sentence stops being true silently. Quarantine names rows expected to be RED; the silenced rows are GREEN by construction. Two questions, one unasked. - THE INERT CARRIER. std.witness_purpose WitnessPurpose landed under the 2026-08-04 witness-cost-derives-from-purpose ruling, is rostered inert in v2.lens.inert_carrier, has zero declarers and zero consumers, and its only reference is its own taxonomy test. One missing consumer, not two problems: the floor grew a cost mechanism that judges rows with no access to what any row is FOR. - AN OBSERVABILITY CORRECTION, stated as a fact about the floor rather than about any brief. WHICH rows were preempted is already a joinable run product: write_required_floor_claim_cost_tsv emits one row per executed claim with verdict_reached, and the occurrence is minted in required_floor_runner's claim loop before classification branches, so preempted rows are present rather than dropped. Reading the INTERRUPTED-BEFORE-VERDICT log lines as the population is instrument_output_read_as_subject_content. What is missing is the ranking key, not the population. The next-rung trigger names the CAPABILITY -- an authored purpose declaration a floor consumer can join against -- and its three sufficiency conditions, because a trigger naming only "a ruling" would be satisfied while the capability stays dead. Nothing here changes what is admitted: the ceiling does not move, no budget widens, and a non-verdict on a required claim still blocks. docs/design-failure-modes.md is the projection, regenerated by the generated-artifact gate and verified idempotent on a second run. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0198WYhRXB3scqq262mtHqSx * Record the 4c foreclosure: purpose must be a real binding, never an annotation The row's trigger condition (ii) asked for a purpose declared at identity grain without saying what KIND of declaration, which leaves the cheap version open: a source annotation on the test fn. DESIGN 4c forecloses it outright. Semantic passes receive only the annotation-erased projection, so an annotated purpose is unreadable by the floor BY CONSTRUCTION -- it would be a declaration no consumer could ever join against, which is the whole point of the trigger. That is 4c's own rule that an annotation is never evidence a machine claim holds, applied to this fact. Stated as the reason the declaration is a real DeclarationRef binding rather than as an implementation detail, so the annotation is not re-proposed as an economy in six months. It also prices the capability honestly: a real binding is more authoring per row than an annotation would have been. docs/design-failure-modes.md regenerated and verified idempotent. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0198WYhRXB3scqq262mtHqSx * Refine BehavioralDiscriminator to carry what the row requires to be refused Operator ruling 2026-09-02 approved the refinement over a sixth peer arm. This is the model half of the ranking key that gunbc.recurring_failure_mode non_execution_undifferentiated_by_what_it_silenced names as missing. THE BARE ARM COULD NOT ORDER THE POPULATION. "This witness discriminates behaviour" is true of a discriminating RED and of an accepted positive control equally, so spending it as the key would have bought a coarse fact cited as coverage for a distinction it does not draw -- the 4b(1) inflation that stops a class ever ranking for the climb it could make. DESIGN 4b(1) already names the two halves of executed evidence; DiscriminatedOutcome is that pair, authored: RefusalRequired { refuser: DeclarationRef } AcceptanceRequired { acceptor: DeclarationRef } WHY IT IS A SAFETY FACT. A row requiring a refusal is GREEN in the ordinary case, so when it does not execute the wall it carries is switched off with nothing red, and a later green over that absence is a green over a refusal that did not run. A row requiring an acceptance, not executing, removes no wall. Same terminal state, different consequence. THE SUBJECT IS THE DECISION, NEVER THE WITNESS -- both arms name the decision the row watches, so the fact is joinable against that decision rather than being an adjective on the test. A payload naming the test itself would restate the identity the row already has. AUTHORED, NOT INFERRED, and the module header's rule binds here specifically: a lens could observe that a body matches a refusal-shaped variant, and that observation is NOT this fact -- it would make the compiler's reading of the body the authority on what the body is for, so a body that stopped requiring the refusal would silently restate its purpose instead of going red. EVIDENCE, EXECUTED AND MUTATED rather than described. The control asserts that two values AGREEING on the watched decision reach OPPOSITE answers from purpose_requires_a_refusal, the predicate a ranking consumer runs. Executed both ways: green as authored; collapsing the two DiscriminatedOutcome arms to one answer -- the exact degradation the refinement exists to catch -- turns it red (returned false). A sibling control asserts a non-discriminator purpose requires no refusal, so the key cannot be read as "any purpose mentioning a DeclarationRef". Per 4b(4) both stay enrolled after the wall lands. DiscriminatedOutcome is rostered in v2.lens.inert_carrier beside WitnessPurpose: declared, test-referenced, no production consumer yet. It dissolves when the floor consumer that joins purpose against verdict_reached lands, which is the next piece and is NOT in this PR. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0198WYhRXB3scqq262mtHqSx * Add WitnessPurposeBinding, and a separator comma on the roster's former last row BINDING. There is no per-`test fn` declaration slot in the language, so a witness's purpose has to be authored beside it and point at it: WitnessPurposeBinding { witness: DeclarationRef, purpose: WitnessPurpose } Authored in the witness's OWN module by whoever owns the witness, which is what makes the population independently defined rather than selected -- no central roster names which rows matter and nobody picks a subset. It is joinable without a new authority, and that is why the field is a DeclarationRef rather than a string: v1.declaration_index already records, per module, every typed-literal DeclarationRef citation paired with the top-level declaration carrying it (CitedSymbol.in_declaration) and every authored type reference under the same key. So "does a purpose binding exist for this identity" is decidable from the index that already runs. A string would be reachable from no index. The binding is NOT evidence that the purpose is true of the row -- that stays outside the modeled guarantee per the module header. What it makes possible is ranking a row that DID NOT RUN, which needs only the declaration. EVIDENCE: two bindings over the SAME witness differing only in purpose reach opposite answers from the ranking predicate. Holding the witness constant makes the purpose the only variable. Executed both ways -- green as authored; giving the control the wall's purpose (the binding no longer transporting the distinction) returns false. COMMA. inert_carrier_roster's WitnessPurpose row was the list's last element and carried no trailing separator, so appending after it left two elements adjacent. Added for consistency with every other row. Recorded because the review that found it (review 59031) called it a "won't compile" blocker, and that part does not reproduce: the module PARSES AND EVALUATES IDENTICALLY WITH AND WITHOUT THE COMMA -- inert_carrier_rostered_names returns the same 16 units both ways, this repo's parser treating the newline as sufficient. The fix is real hygiene; the stated consequence was not, and filing it as a compile blocker would teach a wall that does not exist. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0198WYhRXB3scqq262mtHqSx * Model the purpose standing, the non-execution consequence, and the admission wall The ranking key made executable. Three types and three total folds: WitnessPurposeStanding PurposeDeclared | PurposeUndeclaredGrandfathered | PurposeUndeclared WitnessChangeStanding WitnessChanged | WitnessUnchanged NonExecutionConsequence SilencedWall { refuser } | OpenQuestion | ConsequenceUndeclared 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, which is the difference between a count and a lead. CONSEQUENCE_UNDECLARED IS NOT OPEN_QUESTION, and collapsing them is the one 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, never summed into either other. THE SHRINK MECHANISM, so the roster is debt rather than a permanent exemption in a debt contract's clothes. A grandfathered identity that CHANGED must declare before it is admitted again, so the roster can only lose members and loses them exactly when someone is already editing the row. An untouched grandfathered row is admitted: it carries yesterday's debt and no new risk. EVIDENCE -- 7 controls green, and the two degradations that matter executed as REDs: reporting unknown as benign turns an_undeclared_row_is_unknown_rather_than_benign false; dropping the change standing from admission turns a_grandfathered_row_must_declare_once_it_changes false. Positive controls included so an admission that refused everything would not satisfy the wall tests. NATIVE BOOL, NOT THE VARIANTS. v2.std.logic Bool is realized as a machine scalar, so returning True {} / False {} produces a value match_pattern has no arm for. Recorded on the import: required_floor carries the same straddle from the pattern side, where an earlier revision errored 11 of 19 witnesses. No consumer wires this into the floor yet, so nothing gates on it and no admission behavior changes. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0198WYhRXB3scqq262mtHqSx * Drop two inert rows my own diff made stale, measured against the live gate The live gate `inert_carrier_no_unrostered_or_stale` went RED on this branch. It was right, and the cause is my own roster edit rather than anything downstream. WHAT "INERT" ACTUALLY MEANS, read from the producer rather than assumed. 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 zero or below. The subtraction is per-block, so a reference from ANOTHER block in the SAME non-test file counts as consumption. So two rows stopped being true the moment this diff landed, and neither is the carrier I was thinking about: DiscriminatedOutcome -- consumed by the `WitnessPurpose` block itself, since the refined arm reads `BehavioralDiscriminator { discriminates: DiscriminatedOutcome }`. It was therefore NEVER inert; the row I added for it was wrong when I wrote it. WitnessPurpose -- a PRE-EXISTING row, made stale by this diff: the new `WitnessPurposeBinding` carries a `purpose: WitnessPurpose` field, which is a non-test reference from another block. `WitnessPurposeBinding` itself stays rostered: nothing outside its own block reads it yet, so it is genuinely inert and its row is the honest state. MEASURED, NOT ARGUED, against the same live entry point the gate calls (`inert_carrier_live_stale_roster_count` / `..._unrostered_count`): origin/main stale=0 unrostered=2 this branch, before the fix stale=2 unrostered=2 this branch, after the fix stale=0 unrostered=2 So the branch is back to main's exact baseline and contributes no roster drift. THE `unrostered=2` IS PRE-EXISTING ON MAIN AND IS DELIBERATELY NOT TOUCHED HERE. It reproduces on origin/main with this diff absent, so absorbing it into this PR would claim a repair this change did not make and would hide whose drift it is. ONE OBSERVATION FOR WHOEVER OWNS THE LENS, recorded rather than acted on: it counts a sibling INERT type as a consumer. Adding an inert carrier that references another inert carrier silently un-inerts the referent, even though no production code reads either. That is what made a pre-existing WitnessPurpose row stale here. It may be the intended mechanical reading -- the roster must match the lens either way, which is why this diff satisfies the gate rather than routing around it. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0198WYhRXB3scqq262mtHqSx * Cite the taxonomy module by the name it declares, not a dag.-prefixed one required-witnesses-floor failed on this branch with the floor itself CLEAN (verdict=FloorClean, failed=0, interrupted=0, over_cost=0). The refusal was `required-ci: FAILED PHASE declarations (1 finding)`: CITED-MODULE-ABSENT ... `test.claim.witness_purpose_taxonomy_witness` cites `dag.test.claim.witness_purpose_taxonomy_witness` `fixture_population_ref`, and no module declares that path. The module declares itself `module test.claim.witness_purpose_taxonomy_witness`. The `dag.`-prefixed spelling names nothing, and the repo already records it as a plain typo -- gunbc.declaration_index_seed_growth says so about this exact module. I copied it from the neighbouring fixture when adding `fixture_refuser_ref`, so a known one-off became a second live instance and the phase went red. Fixed MY citation only. The pre-existing `fixture_population_ref` keeps its `dag.`-prefixed spelling deliberately: it is carried on the citation-debt roster, and silently repairing it here would make that roster row stale as a side effect of an unrelated change, which is a different edit needing its own justification. Worth someone's follow-up, not this diff's. Discriminating tests re-run green after the change -- refusal_and_acceptance_requirements_do_not_report_alike and two_bindings_on_one_witness_separate_on_purpose both still true, which they must be: the citation is the same value on both sides of each comparison, so correcting the path changes what the fixture NAMES without changing what the tests DISCRIMINATE. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0198WYhRXB3scqq262mtHqSx * Collapse the standing to two arms: the grandfather roster is derivable, so it should not exist Amending after approval, deliberately. An approval means no blocking defect was FOUND, not that the artifact is what was asked for -- and this one carried a decoration. THE ROSTER IS DERIVABLE AND THEREFORE REDUNDANT. Wiring an enumerated monotone debt roster means naming every identity that predates the requirement, and the subject universe is every discovered witness -- a ~3500-entry authored blob that is a second copy of the discovery output. DESIGN section 2 rules against exactly that, and this is the kind that ROTS: it goes stale against every witness rename. The change standing already carries the whole distinction. Admission refuses "undeclared AND changed", so an untouched row that predates the requirement is admitted with no roster entry, an edited row must declare, and a NEW row is changed by construction so it must declare too. That is the mandatory-at-admission wall reached without enumerating anything. SO THE THIRD ARM WAS UNREACHABLE BY CONSTRUCTION, not merely unused: nothing can distinguish "new" from "predating" without a roster, so with the roster gone no producer can ever reach PurposeUndeclaredGrandfathered. 4b calls an arm no producer reaches a decoration -- permanently unconstructed, carrying no information, and worse than absent once cited as covering the new-row case. Removed rather than left to be cleaned up by the wiring PR, which would have meant an approved artifact advertising coverage that does not exist for however long that took. THE SHRINK GUARD IS NOW SATISFIED BY DISSOLUTION RATHER THAN BY MECHANISM: there is no roster that could sit unshrinking, because there is no roster. The debt is implicit and discharges whenever anyone touches a row, with no quota and nothing to maintain. CONTROLS RE-VERIFIED, because collapsing an arm is exactly where a control gets eaten. Eight green, and every degradation still discriminates -- including the direction a one-sided test would miss: report undeclared as the benign arm -> unknown_rather_than_benign FALSE admission constant FALSE (never refuse) -> must_declare_once_it_changes FALSE new_row_..._is_refused FALSE admission constant TRUE (always refuse) -> must_declare_once_it_changes FALSE untouched_..._is_admitted FALSE ONE ASSERTION WAS DELETED ON PURPOSE AND IS NOT A LOST CONTROL. a_new_row_without_a_declared_purpose_is_refused previously required PurposeUndeclared to refuse on BOTH change standings -- the behaviour of the removed always-refuse arm. An untouched undeclared row is now ADMITTED, which is the implicit debt, so keeping that half would have contradicted the design rather than guarded it. It is replaced by an_untouched_undeclared_row_is_admitted_which_is_the_implicit_debt, so both halves of the contract are asserted: refuse on contact, admit while untouched. Also prunes an unused `True, False` import from the test module (review 59106, a correct finding): they were imported and never used, in a file whose sibling documents why those variants must not be constructed. Replaced with a note saying so, since leaving them importable puts the wrong spelling within reach. Inert gate re-measured after the collapse: stale=0, unrostered=2 -- main's baseline unchanged. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0198WYhRXB3scqq262mtHqSx * Cite the refuser where it is declared, not where it is exercised The declarations phase refused CITED-DECLARATION-ABSENT: watched_decision cited `live_tree_frontier_verdict` in `test.claim.self_host_compile_phase_live_gate_witness`, which only CALLS it. The fold is declared in `gunbc.self_host_compile_phase_live_gate`. The refuser named by RefusalRequired is the fold, so this is the semantically correct ref as well as the resolvable one. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0198WYhRXB3scqq262mtHqSx * Narrow the binding annotation to what the type constructs The annotation claimed that authoring a binding in the witness's own module is what makes the purpose population independently defined rather than selected -- 'no central roster names which rows matter, and nobody picks a subset'. The type does not construct that. `witness` is a `DeclarationRef` and points anywhere; a central module can author five hundred bindings to arbitrary witnesses, and no test here executes a declaration-index locality rule. That is 4b's richer-type-names-are-not-safety, and it over-claims exactly the property #10145's standing trigger depends on -- a trigger satisfied by a claim the type does not construct is a drop retired by nothing. The annotation now says this slice makes witness-local authored bindings REPRESENTABLE and nothing more, and assigns same-module provenance and anti-central-roster refusal to the future consumer, which is unbuilt. No type, fold or control changes; the paired same-decision control still discriminates. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0198WYhRXB3scqq262mtHqSx --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
…efused (#10161) * Refine BehavioralDiscriminator to carry what the row requires to be refused Operator ruling 2026-09-02 approved the refinement over a sixth peer arm. This is the model half of the ranking key that gunbc.recurring_failure_mode non_execution_undifferentiated_by_what_it_silenced names as missing. THE BARE ARM COULD NOT ORDER THE POPULATION. "This witness discriminates behaviour" is true of a discriminating RED and of an accepted positive control equally, so spending it as the key would have bought a coarse fact cited as coverage for a distinction it does not draw -- the 4b(1) inflation that stops a class ever ranking for the climb it could make. DESIGN 4b(1) already names the two halves of executed evidence; DiscriminatedOutcome is that pair, authored: RefusalRequired { refuser: DeclarationRef } AcceptanceRequired { acceptor: DeclarationRef } WHY IT IS A SAFETY FACT. A row requiring a refusal is GREEN in the ordinary case, so when it does not execute the wall it carries is switched off with nothing red, and a later green over that absence is a green over a refusal that did not run. A row requiring an acceptance, not executing, removes no wall. Same terminal state, different consequence. THE SUBJECT IS THE DECISION, NEVER THE WITNESS -- both arms name the decision the row watches, so the fact is joinable against that decision rather than being an adjective on the test. A payload naming the test itself would restate the identity the row already has. AUTHORED, NOT INFERRED, and the module header's rule binds here specifically: a lens could observe that a body matches a refusal-shaped variant, and that observation is NOT this fact -- it would make the compiler's reading of the body the authority on what the body is for, so a body that stopped requiring the refusal would silently restate its purpose instead of going red. EVIDENCE, EXECUTED AND MUTATED rather than described. The control asserts that two values AGREEING on the watched decision reach OPPOSITE answers from purpose_requires_a_refusal, the predicate a ranking consumer runs. Executed both ways: green as authored; collapsing the two DiscriminatedOutcome arms to one answer -- the exact degradation the refinement exists to catch -- turns it red (returned false). A sibling control asserts a non-discriminator purpose requires no refusal, so the key cannot be read as "any purpose mentioning a DeclarationRef". Per 4b(4) both stay enrolled after the wall lands. DiscriminatedOutcome is rostered in v2.lens.inert_carrier beside WitnessPurpose: declared, test-referenced, no production consumer yet. It dissolves when the floor consumer that joins purpose against verdict_reached lands, which is the next piece and is NOT in this PR. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0198WYhRXB3scqq262mtHqSx * Add WitnessPurposeBinding, and a separator comma on the roster's former last row BINDING. There is no per-`test fn` declaration slot in the language, so a witness's purpose has to be authored beside it and point at it: WitnessPurposeBinding { witness: DeclarationRef, purpose: WitnessPurpose } Authored in the witness's OWN module by whoever owns the witness, which is what makes the population independently defined rather than selected -- no central roster names which rows matter and nobody picks a subset. It is joinable without a new authority, and that is why the field is a DeclarationRef rather than a string: v1.declaration_index already records, per module, every typed-literal DeclarationRef citation paired with the top-level declaration carrying it (CitedSymbol.in_declaration) and every authored type reference under the same key. So "does a purpose binding exist for this identity" is decidable from the index that already runs. A string would be reachable from no index. The binding is NOT evidence that the purpose is true of the row -- that stays outside the modeled guarantee per the module header. What it makes possible is ranking a row that DID NOT RUN, which needs only the declaration. EVIDENCE: two bindings over the SAME witness differing only in purpose reach opposite answers from the ranking predicate. Holding the witness constant makes the purpose the only variable. Executed both ways -- green as authored; giving the control the wall's purpose (the binding no longer transporting the distinction) returns false. COMMA. inert_carrier_roster's WitnessPurpose row was the list's last element and carried no trailing separator, so appending after it left two elements adjacent. Added for consistency with every other row. Recorded because the review that found it (review 59031) called it a "won't compile" blocker, and that part does not reproduce: the module PARSES AND EVALUATES IDENTICALLY WITH AND WITHOUT THE COMMA -- inert_carrier_rostered_names returns the same 16 units both ways, this repo's parser treating the newline as sufficient. The fix is real hygiene; the stated consequence was not, and filing it as a compile blocker would teach a wall that does not exist. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0198WYhRXB3scqq262mtHqSx * Drop two inert rows my own diff made stale, measured against the live gate The live gate `inert_carrier_no_unrostered_or_stale` went RED on this branch. It was right, and the cause is my own roster edit rather than anything downstream. WHAT "INERT" ACTUALLY MEANS, read from the producer rather than assumed. 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 zero or below. The subtraction is per-block, so a reference from ANOTHER block in the SAME non-test file counts as consumption. So two rows stopped being true the moment this diff landed, and neither is the carrier I was thinking about: DiscriminatedOutcome -- consumed by the `WitnessPurpose` block itself, since the refined arm reads `BehavioralDiscriminator { discriminates: DiscriminatedOutcome }`. It was therefore NEVER inert; the row I added for it was wrong when I wrote it. WitnessPurpose -- a PRE-EXISTING row, made stale by this diff: the new `WitnessPurposeBinding` carries a `purpose: WitnessPurpose` field, which is a non-test reference from another block. `WitnessPurposeBinding` itself stays rostered: nothing outside its own block reads it yet, so it is genuinely inert and its row is the honest state. MEASURED, NOT ARGUED, against the same live entry point the gate calls (`inert_carrier_live_stale_roster_count` / `..._unrostered_count`): origin/main stale=0 unrostered=2 this branch, before the fix stale=2 unrostered=2 this branch, after the fix stale=0 unrostered=2 So the branch is back to main's exact baseline and contributes no roster drift. THE `unrostered=2` IS PRE-EXISTING ON MAIN AND IS DELIBERATELY NOT TOUCHED HERE. It reproduces on origin/main with this diff absent, so absorbing it into this PR would claim a repair this change did not make and would hide whose drift it is. ONE OBSERVATION FOR WHOEVER OWNS THE LENS, recorded rather than acted on: it counts a sibling INERT type as a consumer. Adding an inert carrier that references another inert carrier silently un-inerts the referent, even though no production code reads either. That is what made a pre-existing WitnessPurpose row stale here. It may be the intended mechanical reading -- the roster must match the lens either way, which is why this diff satisfies the gate rather than routing around it. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0198WYhRXB3scqq262mtHqSx * Cite the taxonomy module by the name it declares, not a dag.-prefixed one required-witnesses-floor failed on this branch with the floor itself CLEAN (verdict=FloorClean, failed=0, interrupted=0, over_cost=0). The refusal was `required-ci: FAILED PHASE declarations (1 finding)`: CITED-MODULE-ABSENT ... `test.claim.witness_purpose_taxonomy_witness` cites `dag.test.claim.witness_purpose_taxonomy_witness` `fixture_population_ref`, and no module declares that path. The module declares itself `module test.claim.witness_purpose_taxonomy_witness`. The `dag.`-prefixed spelling names nothing, and the repo already records it as a plain typo -- gunbc.declaration_index_seed_growth says so about this exact module. I copied it from the neighbouring fixture when adding `fixture_refuser_ref`, so a known one-off became a second live instance and the phase went red. Fixed MY citation only. The pre-existing `fixture_population_ref` keeps its `dag.`-prefixed spelling deliberately: it is carried on the citation-debt roster, and silently repairing it here would make that roster row stale as a side effect of an unrelated change, which is a different edit needing its own justification. Worth someone's follow-up, not this diff's. Discriminating tests re-run green after the change -- refusal_and_acceptance_requirements_do_not_report_alike and two_bindings_on_one_witness_separate_on_purpose both still true, which they must be: the citation is the same value on both sides of each comparison, so correcting the path changes what the fixture NAMES without changing what the tests DISCRIMINATE. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0198WYhRXB3scqq262mtHqSx * Narrow the binding annotation to what the type constructs The annotation claimed that authoring a binding in the witness's own module is what makes the purpose population independently defined rather than selected -- 'no central roster names which rows matter, and nobody picks a subset'. The type does not construct that. `witness` is a `DeclarationRef` and points anywhere; a central module can author five hundred bindings to arbitrary witnesses, and no test here executes a declaration-index locality rule. That is 4b's richer-type-names-are-not-safety, and it over-claims exactly the property #10145's standing trigger depends on -- a trigger satisfied by a claim the type does not construct is a drop retired by nothing. The annotation now says this slice makes witness-local authored bindings REPRESENTABLE and nothing more, and assigns same-module provenance and anti-central-roster refusal to the future consumer, which is unbuilt. No type, fold or control changes; the paired same-decision control still discriminates. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0198WYhRXB3scqq262mtHqSx --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
What this is
The required floor refuses when rows are preempted before reaching a verdict at the 500ms CPU ceiling, with
failed=0: nothing is judged broken, rows simply never answer, and the floor is right to refuse. Which rows get preempted moves with runner load, so the population is redrawn per attempt.The part that makes it correctness rather than cost: some preempted rows exist to establish a refusal. Those rows PASS normally, so preempting one turns a standing guarantee off with nothing red anywhere — and a re-run that draws a faster runner buys a green over refusals that did not execute. That is why re-running is not an exit.
This PR files the class and builds nothing else. No consumer, and no edit to
std.witness_purpose— both are blocked on an authored ruling, which the row records as blocked on a ruling rather than rejected on merit, so the next lane does not re-derive the design.The three findings the row carries
1. The disjointness — with its setter. The open question was whether "row declared to fail" and "row whose assertion establishes a refusal" are conflated. They are not conflated; they are disjoint, and only one is represented.
InterruptedBeforeVerdict.enrolled_expected_redis KnownRed quarantine and nothing else — set on exactly one branch, the expected-red arm reachingExpectedRedArm::BudgetRefused, meaning the identity is rostered as declared-to-fail.The rows whose silencing motivated the class carry it false.
a_live_tree_that_gained_an_identity_refuses_and_names_itanda_live_tree_that_swapped_an_identity_at_equal_cardinality_refusesintest.claim.self_host_compile_phase_live_gate_witnessare ordinary passing rows on no expected-red, cost-debt or quarantine roster. The second carries an in-source comment stating it is precisely the probe that would go green if the join were replaced by a population-size comparison — preempt that one row and the comment silently stops being true.Quarantine names rows expected to be RED; the silenced rows are GREEN by construction. Two different questions, one of them unasked.
2. The inert carrier.
std.witness_purposeWitnessPurposedeclares the authored taxonomy under the operator's 2026-08-04 witness-cost-derives-from-purpose ruling, its header stating purpose is authored, not inferred from implementation. It is rostered inv2.lens.inert_carrierwith its own reason: zero declarers, zero consumers, only reference its own taxonomy test.So this is one missing consumer, not two problems — the purpose vocabulary landed, the consumer slices never did, and meanwhile the floor grew a cost mechanism that judges rows with no access to what any row is FOR.
3. An observability correction, stated as a fact about the floor. Which rows were preempted is already a joinable run product:
write_required_floor_claim_cost_tsvemits one row per executed claim carryingverdict_reached, and the occurrence is minted inrequired_floor_runner's claim loop before any classification branches, so preempted rows are present rather than dropped. Reading theINTERRUPTED-BEFORE-VERDICTlog lines as the population isinstrument_output_read_as_subject_content. What is missing is the ranking key, not the population — which is why this PR adds no second producer.Next-rung trigger
Named as the capability — an authored purpose declaration a floor consumer can join against — with three sufficiency conditions, because a trigger naming only "a ruling" gets satisfied while the capability stays dead. The row also records why
BehavioralDiscriminatoris too coarse to spend here: it covers a positive control equally well, so it would buy a key cited as coverage for a distinction it does not draw — the §4b(1) inflation that stops a class ever ranking for climbing.What this does not do
Nothing here changes what is admitted. The 500ms ceiling does not move, no budget widens, no row relocates, and a non-verdict on a required claim still blocks. The row is about what is reported. Those four moves are recorded in it as excluded, since each hides the class rather than ranking it and the last also deletes the refusal that makes the silencing detectable.
Verification
docs/design-failure-modes.mdis a pure fold over the roster, regenerated by the generated-artifact gate (gunbc run --entry dag/gunbc/instruments/generated_artifact_gate.dag --function main_wet) and verified idempotent on a second run — the diff is the authority row plus its projection and nothing else. The generator evaluating the row throughrecurring_failure_mode_roster→failure_mode_documentis the executed evidence that it parses and folds.Note: a finding-only PR may still be preempted by the class it documents. If that happens I will measure and report it rather than re-run to clear it.
🤖 Generated with Claude Code
https://claude.ai/code/session_0198WYhRXB3scqq262mtHqSx