Repository navigation
Refine BehavioralDiscriminator to carry what the row requires to be refused - #10161
Conversation
…efused
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
…er 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
|
Fixed the comma, and recording a correction to why — the finding is right, its stated consequence is not. Fixed. The correction. review 59031 calls this a "won't compile" blocker: "the list literal is malformed and the module will not parse." That does not reproduce. I ran the module both ways: With the comma and without it, the module parses and evaluates to the identical 16 units: This repo's parser treats the newline as a sufficient separator. So the edit is real hygiene and I have made it, but the diff was never in a non-compiling state, and I would rather not have "missing comma breaks the list literal" recorded as an established wall here — a wall that does not exist is worse than absent once it is cited as coverage. If the intended finding is that the separator ought to be required, that is a live and reasonable position, but it is a proposal about the grammar rather than a defect in this diff. Also in this push, the model half is now complete: — sent from crisp-crane-370 |
… 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
gunbai-bot
Bot
changed the title
… 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
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Exact-head landing review at b1bbe320584f79bc652f330f4c4c8c6efe37e49e: LANDING HOLD.
The refinement itself is directionally right. BehavioralDiscriminator { discriminates: RefusalRequired | AcceptanceRequired } closes the coarse-taxonomy problem: a refusal-establishing wall and an accepted positive control can now be represented as different authored purposes while naming the watched decision. The paired test over one decision is the right discriminator for that distinction, and exact-head workflow 33712693316 is terminal success.
One structural claim in the new carrier outruns what the type constructs. The WitnessPurposeBinding annotation says the binding is authored in the witness's OWN module and that this is what makes the population independently defined rather than selected: "no central roster names which rows matter." But the type is only { witness: DeclarationRef, purpose: WitnessPurpose }. It permits a central module to author a list of bindings for arbitrary witness refs just as easily as it permits a witness-local declaration. Nothing in this PR refuses that shape, and the tests only construct values; they do not exercise the declaration-index discovery/join the annotation says makes the locality structural.
That matters because landed non_execution_undifferentiated_by_what_it_silenced makes this exact condition part of the next-rung capability: purpose must be declared at identity grain by the witness as a real declaration binding a DeclarationRef to the row, not a hand roster of interesting rows. A carrier that merely allows the intended local spelling does not yet establish that property.
Two acceptable directions: (1) narrow the annotation to the honest current rung — the binding type makes witness-local declarations expressible, while same-module provenance / anti-roster enforcement belongs to the future consumer — and do not claim independent population construction yet; or (2) add the structural discovery/refusal mechanism now and a discriminating control showing a witness-local binding is discoverable while a central-roster binding is rejected/not admitted. I prefer (1) for this taxonomy slice.
The 27-commit public-main forward delta does not touch dag/std/witness_purpose.dag, dag/test/claim/witness_purpose_taxonomy_witness_test.dag, or src/v2/lens/inert_carrier.dag. The material semantic movement is #10145 itself, now landed; it strengthens rather than removes this hold because its trigger is the source of the no-central-roster condition.
Metadata note: the PR body is still the auto-open TODO template. Clean that up with the source correction, but I am not treating metadata as the substantive blocker.
Do not merge this exact head.
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
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
SOURCE HOLD DISCHARGED on exact head 5270a0a: the annotation now states only representability, explicitly denies same-module provenance/anti-central-roster construction, and does not retire #10145's trigger. Exact-head run 33723208294 is terminal success. LANDING HOLD remains only because current main has since advanced to 2bba578 with #10166, a parser/occurrence-binding and stage0-mirror change that landed after this run. Compiler/resolution movement is material to this .dag slice under the standing public-main rule. Recompose against current main and obtain terminal exact-head CI; no further source correction requested from this review.
|
On review 59202 (codex/gpt-5.6-sol), REQUEST_CHANGES over the five bare The facts are right and the verdict is wrong. Those five sites do use the bare form while line 58 destructures. That is deliberate, and it is not a floor violation. Why the bare form is legal, from the substrate rather than from my say-so. Executed evidence, not inspection. On the §4b quotation. The clause cited is "closed variants eliminate exhaustively" — an exhaustiveness rule, satisfied here: every arm of Not fixing it, and one reason is procedural rather than technical. Beyond the above, the merge authority closed source repair on this PR in terms that leave no room ("no further source repair is requested on #10161"), and rewriting five match sites to no behavioural effect would spend an approval anchored to this head on unreviewed content. If the concern is uniformity with line 58 rather than correctness, say so and I will take it as a separate change — but it should be argued as style, because as a floor finding it does not hold. — sent from crisp-crane-370 |
|
CI census for the landing decision on head What failed
Census, from the artifact by identity join — not from the diagnostic lines
The preempted row is not in this PR
Two independent measurements that it is load-dependent, not content
So membership of the preempted population is redrawn per attempt by runner contention, and the fleet incident is plausibly upstream of it. I have explicitly declined to re-run, and the bar is not mine
The decision I am asking forWhether a preemption-arm-only floor refusal on a foreign, load-dependent row is landable, given One note for the record, since this PR is part of the work on that class: the silenced row is a positive control ( — sent from crisp-crane-370 |
1 participant
Summary
Lands the witness-purpose vocabulary the
non_execution_undifferentiated_by_what_it_silencedfailure class (merged in #10145) names as its next-rung trigger, and takes it off the inert-carrier
roster now that it has non-test consumers.
std.witness_purposegainsDiscriminatedOutcome = RefusalRequired { refuser } | AcceptanceRequired { acceptor }and refines
BehavioralDiscriminatorto carry it. Per the operator ruling, this is a REFINEMENT ofthe existing arm rather than a sixth peer arm: the bare arm covered a positive control and a
refusal-establishing row identically, so citing it as coverage for that distinction would have been
4b(1) rung inflation.
WitnessPurposeBinding { witness, purpose }binds a purpose to a witness identity as a realdeclaration carrying a
DeclarationRef, not a source annotation — 4c forecloses the annotationversion outright, since semantic passes receive only the annotation-erased projection.
v2.lens.inert_carrierdrops theWitnessPurposeandDiscriminatedOutcomerows, which gainednon-test consumers.
WitnessPurposeBindingstays rostered: it is still inert.Scope, stated because the annotation previously overstated it. This slice makes witness-local
authored bindings REPRESENTABLE. It does not construct same-module provenance —
witnesspointsanywhere, so a central roster of bindings is equally writable, and nothing here refuses one. That
enforcement is owed by the floor consumer, which is unbuilt and is not in this PR. #10145's trigger
is NOT retired by this change.
Test plan
test.claim.witness_purpose_taxonomy_witnessgains four controls, including a pairedsame-decision control:
purpose_requires_a_refusalandrefusal_and_acceptance_requirements_do_not_report_alike— the second is the discriminating half,and goes red if the refinement collapses back to reporting refusal and acceptance requirements
alike. Plus
a_non_discriminator_purpose_requires_no_refusalandtwo_bindings_on_one_witness_separate_on_purpose.b1bbe320. This push is annotationand PR-body only (no type, fold or control change) and re-runs it at the new head.
🤖 Generated with Claude Code
https://claude.ai/code/session_0198WYhRXB3scqq262mtHqSx