Repository navigation
Split the budget outcome into two arms: an interruption and a completed overrun are not one state - #9073
Merged
Conversation
added 4 commits
August 24, 2026 00:41
…ed overrun are not one state
The floor's ledger described one row three inconsistent ways -- BUDGET-REFUSED
on the per-row line, outcome=timed_out on the over-cost line, and "cost exactly
57193ms" on the gating line. Those cannot all be true of one claim.
They came from one habit. `ClaimOutcome::TimedOut` carried the discriminator as
a field (`completion: Interrupted | CompletedOverBudget`), and five projections
over it wrote `TimedOut { .. }`, giving the interrupted row's label to a claim
that had reached its verdict. Four were in the seed; the fifth was the .dag
AUTHORITY -- `v2.workflow.floor_terminal_ledger` `claim_disposition`
wildcarding `ClaimSafetyOutcome` and answering `BudgetRefusedBeforeVerdict`, on
a type whose own model already separates `SafetyInterrupted` from
`CompletedPastSafetyLimit`. THE MODEL HAD THE DISTINCTION; EVERY PROJECTION
OVER IT DROPPED IT. Its wire renderer dropped it a sixth time.
The axis is now the arm: `BudgetInterrupted { elapsed_at_least_ms, .. }` and
`CompletedOverBudget { elapsed_ms, .. }`. A labelling consumer must name both
or fail to compile, and the field names carry the reading so a bound cannot be
spelled as a cost. `BudgetCompletion` is deliberately NOT deleted -- it is the
axis as data where a value has to travel (`BudgetRefusal`, the wire verdict,
the `budget_event` projection), and deleting it there would force a second
spelling of the same two states beside it.
This is the seed comment's own declared next-rung trigger firing: it kept the
field, called the wildcard hazard "paid for by review", and named THE NEXT
CONSUMING SITE ADDED THAT DROPS THE AXIS as the evidence that review is not the
mechanism. Five sites did. The prior decision is not overruled -- it argued
against splitting on RAISE MECHANISM, which no consumer should act on; this
splits on PASSED-VERSUS-INTERRUPTED, which that same comment calls a real
distinction because it determines the remedy.
Evidence, enrolled permanently rather than as scaffolding (DESIGN 4b(4)):
`the_two_budget_arms_project_apart_in_every_consumer` asserts all four seed
projections disagree across the two arms -- each pair was EQUAL before the
split -- and the wire round-trip's every-shape population grows 9 -> 12 with
the three shapes a wildcarded `safety` could not tell apart.
This fixes the INSTRUMENT, not the cost. The 57s row is #9044's, already
merged; keeping them separate is what lets a reader tell which change moved
which number.
…side a green one
Operator ruling, 2026-08-24, on the one call I flagged as mine alone.
KEEP THE NAME. Folding `BudgetRefused { safety: CompletedWithinSafetyLimits }`
into either real arm publishes a refusal or a completion that nothing observed
-- the fabricated plausible output, committed by the function whose purpose is
to stop committing it.
DO NOT MAKE IT UNCONSTRUCTIBLE EITHER, and the reason is not cost.
`ClaimSafetyOutcome` is owned by `v2.workflow.required_floor` and reused here
deliberately; a narrowed two-arm twin declared beside it is one concept forked
by rigor -- §3 nicknaming -- and a fork gets consolidated later at someone
else's cost. So the class sits at MITIGATABLE with its next-rung trigger
written on the carrier (§4b(2), no untracked stall): the safety axis declared
as a family in its OWNING module, at which point this arm, its refusal and
their evidence dissolve together.
WHAT WAS ACTUALLY BROKEN: nothing happened when the arm fired. It appeared
twice -- declaration and produce site -- and no consumer read it, so
`ledger_green_admission` judged publication, reconciliation and footer count
and admitted a ledger carrying it as GREEN. That is a name that describes a
contradiction and permits it: the deficit's frequency is unobservable by
construction, which is the absorbing fallback's quiet half.
It now REFUSES, and the refusal is LOCATED rather than merely typed --
`EvidenceCarriesIncoherentRow` carries the offending identities, so a reader
gets rows to look at instead of a count to hunt with. Checked ahead of
completeness and the footer, because those ask whether the right rows are
present and this asks whether a row says anything at all; calling a population
complete while a member carries no readable outcome answers a question the
count cannot reach. The check folds over the SAME `claim_disposition` every
other consumer reads, so it cannot become a second authority over the fact the
disposition already answers.
Evidence: `a_row_carrying_a_contradictory_budget_terminal_refuses_the_ledger`,
with the positive control beside it -- the identical ledger with a coherent row
IS complete, without which an admission that refused everything would also
pass. All 20 tests across both ledger modules return true by execution.
…in is modeled
CI refused the floor at `phase=strict-preparation` with 78 diagnostics, one per
line, all of them mine:
source annotation sits inside a declaration body. Only module-item grain is
modeled; move it above the declaration it describes.
DESIGN §4c admits only STANDALONE LEADING `//` blocks attached to MODULE-SCOPE
declarations. I put prose where it read best -- inside `type` coproduct arms,
inside `fn` bodies, inside `match` arms -- rather than where the grammar admits
it. Every block is hoisted above the `type`/`fn` it describes and re-worded to
NAME its subject ("the `BudgetRefused` arm below", "two of the arms below"),
because a hoisted annotation is no longer adjacent to the thing it explains and
a reader cannot rely on position to tell them what it is about.
Nothing is dropped: the §4b rung and next-rung trigger, the §3 argument for why
narrowing `BudgetRefused`'s carrier is refused rather than deferred, the
wire-tag finding, and the refuse-rather-than-count reasoning all survive at
module scope.
WHY THIS REACHED CI AT ALL, which is the part worth recording. `gunbc run` does
NOT enforce annotation grain, and neither does `gunbc compile`: the check lives
on the MODULE-INDEX path (`via_index_source_annotation_diagnostics`), so a tree
full of body-grain annotations evaluates witness-by-witness perfectly green --
I reported 20/20 true and a mutation receipt on exactly this tree -- and then
refuses the whole floor before a single witness runs. Green by execution on the
lenient path was not evidence about the strict one, and I presented it as
though it were.
The first verification of this fix was thrown away because it failed its own
control: `gunbc compile` over a fixture carrying a deliberate in-body
annotation reported ZERO refusals, so its zero over the real tree measured
nothing. An absence claim whose known-positive is dead is not evidence.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The defect
The floor's ledger described one row three inconsistent ways:
Those cannot all be true. Reading the producers rather than the strings settles it: the row completed.
claim_terminalitymaps onlyTimedOut { completion: Interrupted }toSafetyInterrupted; everything else,CompletedOverBudgetincluded, becomesVerdictReachedcarrying exact costs. Three independent confirmations — the over-cost fold filters onverdict_reached, the same run reportsinterrupted_before_verdict=0, and PREEMPTION-1 documents this exactcompile_dag_rust_emit_checkclass as uninterruptible. So the gating line was the true one and BUDGET-REFUSED /timed_outwere the false labels.One habit, not five slips
ClaimOutcome::TimedOutcarried the discriminator as a FIELD, and five projections wroteTimedOut { .. }:CiWitnessVerdict::from_outcomeBudgetRefusedfor a row that was refused nothingclaim_dispositionBudgetRefusedBeforeVerdict— a wrong fact, not a labelclaim_terminal_tag"budget-refused"witness_execution_outcome_label"timed_out"v2.workflow.floor_terminal_ledgerclaim_dispositionsafety: _→BudgetRefusedBeforeVerdictfloor_terminal_ledger_wirerender_terminal_tag"budget-refused"tag for both armsSix, not five. The count in the brief was five; the sixth was found while descending the
.dagauthority and it is the one that lasts, because the wire tag is what a reader of the PUBLISHED LEDGER FILE joins on. The other five erased the axis in a log line; this one erased it in the artifact.The fifth is the finding. The model had the distinction; every projection over it dropped it.
ClaimSafetyOutcomealready separatesSafetyInterruptedfromCompletedPastSafetyLimitone import away, and the.dagauthority threw it away exactly as its seed mirror did — plus a sixth inrender_terminal_tag. That is DESIGN's total at the level examined, blind one level down: every one of these matches is exhaustive over its type, which is why review saw nothing incomplete.The fix, and why it is a split rather than a descent
Descending at each consumer fixes today and leaves the invalid state writable, so the next consumer reopens it — which is what happened five times under a comment that predicted it. The axis is now the arm:
A labelling consumer must name both or fail to compile, and the field names carry the reading so a bound cannot be spelled as a cost.
The prior decision is not overruled. The seed comment argued against splitting on RAISE MECHANISM — an axis no consumer should act on. This splits on PASSED-VERSUS-INTERRUPTED, which that same comment calls a real distinction because it determines the remedy. It also declared its own falsifiable next-rung trigger — the next consuming site added that drops the axis — and five sites did.
BudgetCompletionis deliberately NOT deleted, and that is not tidiness lost. It is the axis as data where a value must travel (BudgetRefusal, the wire verdict, the newbudget_eventprojection). Deleting it there would force a second spelling of the same two states beside it, and a dissolution that spawns a duplicate has dissolved nothing.Evidence (§4b(4): enrolled permanently, not scaffolding)
the_two_budget_arms_project_apart_in_every_consumer— asserts all four seed projections disagree across the two arms. The pairing is the assertion: either row alone would pass against a mapping merely re-pointed. On the strength of its red, stated exactly rather than left to be assumed: each pair was equal before the split, and that is established BY READING the fourTimedOut { .. }wildcards, not by execution — the test's two fixtures have no constructors under the old enum, so it cannot be run there at all. What executes is the post-split control; the pre-split claim is a source reading.BudgetRefused { CompletedWithinSafetyLimits }pairing, which gets its own typed disposition rather than being folded into either real arm.cargo check -p v1-compiler --bins --lib --tests: 0 errors, 0 warnings (remote).the_disposition_survives_the_round_trip_for_every_terminal_shapeanda_budget_refusal_is_a_pre_verdict_disposition_not_a_failureboth returntrueunder a freshly builtgunbc(remote; theProcessExitwrapper complaint is the harness, after the value).Not claimed
This fixes the instrument, not the cost. The 57s row is #9044's, already merged. Keeping them apart is what lets a reader tell which change moved which number.
Second commit: the ruling on the contradictory pairing (operator, 2026-08-24)
BudgetRefused { safety: CompletedWithinSafetyLimits }— a budget terminal whose safety outcome says the claim stayed inside its limits — keeps its own disposition rather than being folded into either real arm, and is not made unconstructible. NarrowingBudgetRefused's carrier to the two coherent arms would declare a two-arm twin ofClaimSafetyOutcomebeside the onev2.workflow.required_flooralready owns: one concept forked by rigor, §3 nicknaming, consolidated later at someone else's cost. So the class sits at mitigatable, with its next-rung trigger written on the carrier per §4b(2) — the safety axis declared as a family in its owning module, at which point the arm, its refusal and their evidence dissolve together.What was actually broken: nothing happened when the arm fired. It appeared exactly twice — declaration and produce site — and no consumer read it, so
ledger_green_admissionjudged publication, reconciliation and footer count and admitted a ledger carrying it as GREEN. A name that describes a contradiction and permits it has a deficit frequency of zero by construction; that is the absorbing fallback's quiet half.It now refuses through
EvidenceCarriesIncoherentRow { rows }, located rather than merely typed — the offending identities travel with the refusal, so a reader gets rows to look at instead of a count to hunt with. It is checked ahead of completeness and the footer: those ask whether the right rows are present, this asks whether a row says anything at all, and calling a population complete while a member carries no readable outcome answers a question the count cannot reach.Mutation receipt — the refusal is shown to fire, not asserted
The test comment claims deleting the arm returns
EvidenceComplete. Rather than leave that as a source reading, it was executed (remote, same binary, one guard flipped):So the check has an authorable red and is not permanently green by construction. Its positive control is in the same test — the identical ledger with a coherent row is still
EvidenceComplete— without which an admission that refused everything would also pass.Full sweep, post-change, by execution
20/20 tests in
floor_terminal_ledger_testandfloor_terminal_ledger_wire_testreturntrue, plus 8/8 seedbudget_completion_testsincludingthe_two_budget_arms_project_apart_in_every_consumer.