Repository navigation
A panic in witness evaluation had no terminal: capture it, publish the ledger, stop the line - #9263
Conversation
…e ledger, stop the line
MEASURED FIRST, and both hypotheses the investigation started from are refuted by execution.
Baseline: `test.claim.qualified_pattern_head_witness_test` green through `claim_batch`, exit 0.
ARM A — a panic injected INSIDE `compile_dag_diagnostic_census`'s `catch_unwind`: caught,
returned `NotRunnable`, mapped to `-1` by its `.dag` consumer, witness FAIL, exit 1.
ARM B — a panic injected in witness evaluation OUTSIDE that catch: the process ABORTED with
exit 101 and the identity produced no PASS/FAIL line at all.
So NotRunnable is never counted as pass — verified at three independent grains: all 25 authored
`(Census|Binding)NotRunnable` arms in the corpus map to `false` / `-1` / `none`; the floor derives
`passed` solely from rows whose `claim_disposition` is `Passed`; and `readback_disposition` refuses
an unrecognised tag rather than defaulting. And a panic DOES reach the exit status — but only by
killing the process, which is the defect this lands.
WHAT WAS WRONG. `ClaimOutcome` carries a typed arm for every non-verdict a claim can reach —
runtime error, not-Bool, budget interruption, unresolved host tool, route gap — and had none for
an unwind. So a panicking claim was named nowhere: no terminal row, and the terminal ledger, the
expected-red roster join and the disposition TSV are all written AFTER the fold, so none of the
three was written. Every remaining planned claim went unmeasured, and the ledger that would have
said so did not exist.
WHAT LANDS.
- `ClaimAttemptTerminal` gains `Panicked { payload }` and `NotAttempted { halted_by }`;
`ClaimDisposition` gains `PanickedBeforeVerdict` and `NotAttemptedAfterAbort`; the wire gains
the `panicked` / `not-attempted` tags and their readback arms. Substrate first: the `.dag`
carrier is the authority and the seed mirrors it, and the production per-row comparator
already requires the two mappings to agree.
- `run_claim` captures the unwind at the one seam that already classifies terminals.
- The fold STOPS on a panic (operator ruling, 2026-08-26). Not caution: every other non-verdict
is a state the producer DECIDED to return, so invariants held; a panic is an invariant
violated at an unknown place, and a later row would carry an unstated precondition no row can
express — a green row after the unwind and one before it would render identically.
- THE LEDGER IS PUBLISHED OVER THE PLANNED POPULATION, NEVER THE PREFIX THAT RAN. Every planned
identity behind the unwind gets a `NotAttempted` row naming what halted the line, so
"stopped at claim 400 of 10439" and "10039 rows quietly missing" stop being the same artifact.
These rows are not executions and are not counted as any; the identity check now reads
`planned == executed + not_attempted`.
- `ClaimTerminality` gains `Unwound`, and its `_ => VerdictReached` wildcard is DELETED. That
wildcard would have reported a panicked claim as having reached a verdict — the same
wrong-fact defect `BudgetRefusedBeforeVerdict` was split to repair, one type over.
Evidence: three `.dag` witnesses on the executing round-trip module, plus the new arms enrolled in
`the_disposition_survives_the_round_trip_for_every_terminal_shape` (12 shapes -> 15).
DECLARED, NOT HIDDEN: an ENROLLED identity that panics is left as the roster join's
`NotEvaluated { reason: "not_observed" }` — disposition exactly right, reason generic — because
naming the cause there needs an arm on `WitnessEvalVerdict`, a GENERATED carrier. It lands with
that module's regeneration. The cause is not lost meanwhile: the terminal ledger carries it.
…end staleness over a truncated denominator, and enumerate the seed growth
Review 56032 (codex/gpt-5.6-sol) found the central promise defeated on exactly the runs it was
written for, and it is confirmed by reading the ordering: the fold breaks before
`expected_red_seen` is updated, so every expected-red identity in the UNRUN SUFFIX is missing
from the observed set; the reverse join then `return Err(ExpectedRedIdentityDidNotExecute)`
ahead of ledger publication. A halted run therefore refused by naming rows that are FINE, and
published NO ledger -- which is precisely the artifact the halt exists to produce.
THE DEFECT IS THE EMPTY-OBSERVATION NARROW, not an ordering accident, and naming it that way is
what decides the repair. A reverse join answers "is every enrolled identity still executing" by
subtracting what was OBSERVED from the roster. That subtraction is sound only when the
observation ran over the whole routed roster. After a halt it ran over a PREFIX, so an unrun
enrolled identity is not stale -- it is NOT-ATTEMPTED, and this run already mints exactly one row
for it saying so. Rendering "nothing observed it" as "nothing exercises it" inverts the remedy:
the join says DELETE THE ROSTER ROW.
WHAT LANDS. One predicate, `reverse_joins_answerable = halted_by.is_none()`, gating every reverse
join and nothing else:
- the expected-red staleness refusal and the expected-red partition sum (the latter's own
comment states its premise -- "every enrolled identity was observed exactly once" -- which a
halt falsifies by construction, so it would refuse over an inexactness the halt guarantees);
- `stale_route_gap` and the non-verdict roster's `repaid` arm.
`admission.added` STAYS ARMED, and that asymmetry is the whole content of the predicate: `added`
is a FORWARD observation -- this identity RAN and produced no verdict -- decidable over the
prefix, and suppressing it would hide an observed failure.
IT DOES NOT FAIL OPEN. The panic is already in `outcome.failures`, and
`required_floor_outcome_is_clean` is false whenever that is non-empty, so the run refuses either
way; what changes is which refusal it carries and whether the ledger is reached. The suspension
is announced as a counted `[floor-halt]` line naming the halting identity and all three roster
sizes, so it is a typed, located, countable diagnostic rather than a silent skip.
FINDING 2 -- the hand-Rust receipt -- IS ANSWERED WHERE THE REPOSITORY ACTUALLY REQUIRES IT.
DESIGN carries no "Pure Bootstrap" clause, but `gunbc.seed_growth_admission`
`seed_growth_forward_freeze_policy_note` does make unenumerated hand src/v1 growth a stop-line,
and this change adds two citable items. `gunbc.claim_unwind_seed_growth` enumerates both --
`run_claim_evaluation` and `panic_payload_text` -- with the .dag authority they mirror, why the
seam cannot leave the seed (catch_unwind and Any-downcast are host capabilities the substrate
has no representation of), the owning lane, the deletion trigger, the current boundary, and the
measured item/LOC deltas. It is enrolled in the roster and the roster's well-formedness gate
passes with it (4/4 green through claim_batch, including the duplicate-key check).
This is not a scaffold and carries no dissolution condition of its own: it is the final
construction for a terminal arm, in the same relation to its .dag carrier as every other arm,
under the per-row comparator floor_terminal_ledger.dag already requires to agree.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Both sides append one SeedGrowthJustification row to gunbc.seed_growth_admission -- claim_unwind (this branch) and declaration_index (main). The roster is a UNION, not a choice: taking either side would silently drop the other lane's forward-freeze receipt, which is the one artifact the roster exists to hold.
…, so it printed fourteen spaces mid-sentence Review 56060 (claude/claude-opus-4-7), non-blocking. The string was wrapped across source lines without a `\` continuation, so the indentation became part of the message: "were never attempted and are published". Repaired with the continuation every neighbouring eprintln in this fold already uses, which is also why the defect is worth the commit rather than being left as cosmetic -- the line is the halt's own console announcement, and it is read at exactly the moment a reader is deciding whether the run stopped or narrowed. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
|
Both findings from review 56032 (codex/gpt-5.6-sol) addressed; the first is confirmed and fixed, the second is answered against a different authority than the one it cites. Finding 1 — CONFIRMED, fixed in
|
…ore exhaustiveness over the two abort-side dispositions MAIN IS RED, and the finding is HOW rather than what. This is a SEMANTIC MERGE CONFLICT between two PRs that were each correct and each green, and NEITHER IS AT FAULT: #9227 cd7cf33 adds dag/gunbc/build_target.dag, which MATCHES over ClaimDisposition #9263 a968415 adds PanickedBeforeVerdict and NotAttemptedAfterAbort TO ClaimDisposition Neither PR touches the other's file. There is no textual conflict, no merge-tree signal, and both merged cleanly. One grows a coproduct, the other adds a match over it, and main refuses at strict preparation the moment they meet: dag/gunbc/build_target.dag:177:3: error: non-exhaustive match: missing variant(s) PanickedBeforeVerdict, NotAttemptedAfterAbort dag/gunbc/build_target.dag:378:3: error: non-exhaustive match: missing variant(s) PanickedBeforeVerdict, NotAttemptedAfterAbort #9263 was genuinely green on its own head (witnesses/build/floor all success, 03:38-04:56Z) and merged at 15:16Z against a main that had meanwhile acquired the match. So this is not a PR that merged on a missing check. NO PER-PR GATE CAN CATCH THIS CLASS BY CONSTRUCTION, because each PR is green against the base it was tested on; the combination is what is untested. That is worth recording separately from this repair, because the repair will look routine in six hours and the gap will not have moved. The compiler catching it the instant the two met is fail-closed working correctly. It is the only thing that did catch it. THE MAPPING IS DECIDED BY THE PARTITION THESE MATCHES ALREADY DRAW, not by severity. blaze_test_status_of_claim_disposition already sorts on DID THE CLAIM RUN -- RuntimeErrored is FAILED because it ran and blew up, while RouteGap, HostToolUnresolved and ObservationUnreadable are all INCOMPLETE because they never ran. So: PanickedBeforeVerdict -> TestStatusFailed it executed and died NotAttemptedAfterAbort -> TestStatusIncomplete it never executed INCOMPLETE is the honest arm here rather than the soft one. Rendering a claim that never ran as FAILED asserts that an assertion failed when no assertion ever executed -- the execution-provenance loss DESIGN forbids, where a stage refused before it ran must not inhabit the same carrier as a stage that ran and found a defect. In claim_disposition_verdict both are StandingUnsatisfied, for the same reason read the other way: neither is a claim that satisfied its standing, and admitting an unattempted claim as satisfied would let an aborted run report a standing it never tested. Verified by compiling dag/gunbc/build_target.dag as an entry. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ore exhaustiveness over the two abort-side dispositions (#9343) * Two independently-green PRs met on main and the corpus went red: restore exhaustiveness over the two abort-side dispositions MAIN IS RED, and the finding is HOW rather than what. This is a SEMANTIC MERGE CONFLICT between two PRs that were each correct and each green, and NEITHER IS AT FAULT: #9227 cd7cf33 adds dag/gunbc/build_target.dag, which MATCHES over ClaimDisposition #9263 a968415 adds PanickedBeforeVerdict and NotAttemptedAfterAbort TO ClaimDisposition Neither PR touches the other's file. There is no textual conflict, no merge-tree signal, and both merged cleanly. One grows a coproduct, the other adds a match over it, and main refuses at strict preparation the moment they meet: dag/gunbc/build_target.dag:177:3: error: non-exhaustive match: missing variant(s) PanickedBeforeVerdict, NotAttemptedAfterAbort dag/gunbc/build_target.dag:378:3: error: non-exhaustive match: missing variant(s) PanickedBeforeVerdict, NotAttemptedAfterAbort #9263 was genuinely green on its own head (witnesses/build/floor all success, 03:38-04:56Z) and merged at 15:16Z against a main that had meanwhile acquired the match. So this is not a PR that merged on a missing check. NO PER-PR GATE CAN CATCH THIS CLASS BY CONSTRUCTION, because each PR is green against the base it was tested on; the combination is what is untested. That is worth recording separately from this repair, because the repair will look routine in six hours and the gap will not have moved. The compiler catching it the instant the two met is fail-closed working correctly. It is the only thing that did catch it. THE MAPPING IS DECIDED BY THE PARTITION THESE MATCHES ALREADY DRAW, not by severity. blaze_test_status_of_claim_disposition already sorts on DID THE CLAIM RUN -- RuntimeErrored is FAILED because it ran and blew up, while RouteGap, HostToolUnresolved and ObservationUnreadable are all INCOMPLETE because they never ran. So: PanickedBeforeVerdict -> TestStatusFailed it executed and died NotAttemptedAfterAbort -> TestStatusIncomplete it never executed INCOMPLETE is the honest arm here rather than the soft one. Rendering a claim that never ran as FAILED asserts that an assertion failed when no assertion ever executed -- the execution-provenance loss DESIGN forbids, where a stage refused before it ran must not inhabit the same carrier as a stage that ran and found a defect. In claim_disposition_verdict both are StandingUnsatisfied, for the same reason read the other way: neither is a claim that satisfied its standing, and admitting an unattempted claim as satisfied would let an aborted run report a standing it never tested. Verified by compiling dag/gunbc/build_target.dag as an entry. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * witness: make the ran/never-ran split executable for the two new dispositions The arm-by-arm policy roster enumerated every ClaimDisposition BY HAND, so the two arms this PR adds would have landed with no executing evidence -- the exact specification-without-execution gap DESIGN names, one rung up from the non-exhaustive match that caused the outage. Both dispositions join the roster, and a dedicated witness pins the split that decides them: PanickedBeforeVerdict exports FAILED beside RuntimeErrored (the claim ran and died), NotAttemptedAfterAbort exports INCOMPLETE beside RouteGap (the claim never ran). The INCOMPLETE half is the assertion that earns its keep -- it goes red on precisely the collapse that is tempting to make, where a claim that never executed is reported as one whose assertion failed. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * ci: re-push to trigger a dispatch that never arrived The 16:20 push and the 16:27 ready-flip should each have fired a witnesses run -- witnesses.yml lists both synchronize and ready_for_review, and carries no draft guard -- and neither produced a run of any kind. Not queued, not failed, not startup_failure: absent. The fleet was dispatching normally throughout that window, so this is specific to this ref rather than the outage pattern seen earlier today. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Two independently-green PRs met on main and the corpus went red: restore exhaustiveness over the two abort-side dispositions MAIN IS RED, and the finding is HOW rather than what. This is a SEMANTIC MERGE CONFLICT between two PRs that were each correct and each green, and NEITHER IS AT FAULT: #9227 cd7cf33 adds dag/gunbc/build_target.dag, which MATCHES over ClaimDisposition #9263 a968415 adds PanickedBeforeVerdict and NotAttemptedAfterAbort TO ClaimDisposition Neither PR touches the other's file. There is no textual conflict, no merge-tree signal, and both merged cleanly. One grows a coproduct, the other adds a match over it, and main refuses at strict preparation the moment they meet: dag/gunbc/build_target.dag:177:3: error: non-exhaustive match: missing variant(s) PanickedBeforeVerdict, NotAttemptedAfterAbort dag/gunbc/build_target.dag:378:3: error: non-exhaustive match: missing variant(s) PanickedBeforeVerdict, NotAttemptedAfterAbort #9263 was genuinely green on its own head (witnesses/build/floor all success, 03:38-04:56Z) and merged at 15:16Z against a main that had meanwhile acquired the match. So this is not a PR that merged on a missing check. NO PER-PR GATE CAN CATCH THIS CLASS BY CONSTRUCTION, because each PR is green against the base it was tested on; the combination is what is untested. That is worth recording separately from this repair, because the repair will look routine in six hours and the gap will not have moved. The compiler catching it the instant the two met is fail-closed working correctly. It is the only thing that did catch it. THE MAPPING IS DECIDED BY THE PARTITION THESE MATCHES ALREADY DRAW, not by severity. blaze_test_status_of_claim_disposition already sorts on DID THE CLAIM RUN -- RuntimeErrored is FAILED because it ran and blew up, while RouteGap, HostToolUnresolved and ObservationUnreadable are all INCOMPLETE because they never ran. So: PanickedBeforeVerdict -> TestStatusFailed it executed and died NotAttemptedAfterAbort -> TestStatusIncomplete it never executed INCOMPLETE is the honest arm here rather than the soft one. Rendering a claim that never ran as FAILED asserts that an assertion failed when no assertion ever executed -- the execution-provenance loss DESIGN forbids, where a stage refused before it ran must not inhabit the same carrier as a stage that ran and found a defect. In claim_disposition_verdict both are StandingUnsatisfied, for the same reason read the other way: neither is a claim that satisfied its standing, and admitting an unattempted claim as satisfied would let an aborted run report a standing it never tested. Verified by compiling dag/gunbc/build_target.dag as an entry. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Prove required record fields cannot be omitted * witness: make the ran/never-ran split executable for the two new dispositions The arm-by-arm policy roster enumerated every ClaimDisposition BY HAND, so the two arms this PR adds would have landed with no executing evidence -- the exact specification-without-execution gap DESIGN names, one rung up from the non-exhaustive match that caused the outage. Both dispositions join the roster, and a dedicated witness pins the split that decides them: PanickedBeforeVerdict exports FAILED beside RuntimeErrored (the claim ran and died), NotAttemptedAfterAbort exports INCOMPLETE beside RouteGap (the claim never ran). The INCOMPLETE half is the assertion that earns its keep -- it goes red on precisely the collapse that is tempting to make, where a claim that never executed is reported as one whose assertion failed. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * ci: re-push to trigger a dispatch that never arrived The 16:20 push and the 16:27 ready-flip should each have fired a witnesses run -- witnesses.yml lists both synchronize and ready_for_review, and carries no draft guard -- and neither produced a run of any kind. Not queued, not failed, not startup_failure: absent. The fleet was dispatching normally throughout that window, so this is specific to this ref rather than the outage pattern seen earlier today. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Pin the existing successful-tree stamp order * Name the required-field refusal in the carrier control * Enroll required-field refusal hermetically * Revert "Merge remote-tracking branch 'origin/session/cool-swift-307-exhaustive' into HEAD" This reverts commit 9f56a4e, reversing changes made to 1bc049d. * Carry occurrence identity through v1 Node construction * Regenerate identity-bearing v1 seed * Traverse nested nodes in identity control * Account for shared nodes in identity control * Index shared authored occurrences once * Canonicalize occurrence transport projections * Revert "Canonicalize occurrence transport projections" This reverts commit 43f5c0c. * Complete remaining identity test constructions * Control OCI parser identity uniqueness * Advance allocator beyond published occurrences * Control annotation subject identity coverage * Publish allocator state from accepted node trees * Control occurrence allocation across real modules * Publish occurrence allocation across parser lists * Floor function identities over accepted children * Publish condition identities through if parsing * Make parser occurrence allocation mandatory * Avoid duplicate node declaration occurrence * Record parser context publication rung * Use durable parser repair citation * Publish list slice operand identities * Clarify slice publication repair population --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Brian Searls <searlsbrian@gmail.com>
A panic in witness evaluation had no terminal: capture it, publish the ledger, stop the line
MEASURED FIRST, and both hypotheses the investigation started from are refuted by execution.
Baseline:
test.claim.qualified_pattern_head_witness_testgreen throughclaim_batch, exit 0.ARM A — a panic injected INSIDE
compile_dag_diagnostic_census'scatch_unwind: caught,returned
NotRunnable, mapped to-1by its.dagconsumer, witness FAIL, exit 1.ARM B — a panic injected in witness evaluation OUTSIDE that catch: the process ABORTED with
exit 101 and the identity produced no PASS/FAIL line at all.
So NotRunnable is never counted as pass — verified at three independent grains: all 25 authored
(Census|Binding)NotRunnablearms in the corpus map tofalse/-1/none; the floor derivespassedsolely from rows whoseclaim_dispositionisPassed; andreadback_dispositionrefusesan unrecognised tag rather than defaulting. And a panic DOES reach the exit status — but only by
killing the process, which is the defect this lands.
WHAT WAS WRONG.
ClaimOutcomecarries a typed arm for every non-verdict a claim can reach —runtime error, not-Bool, budget interruption, unresolved host tool, route gap — and had none for
an unwind. So a panicking claim was named nowhere: no terminal row, and the terminal ledger, the
expected-red roster join and the disposition TSV are all written AFTER the fold, so none of the
three was written. Every remaining planned claim went unmeasured, and the ledger that would have
said so did not exist.
WHAT LANDS.
ClaimAttemptTerminalgainsPanicked { payload }andNotAttempted { halted_by };ClaimDispositiongainsPanickedBeforeVerdictandNotAttemptedAfterAbort; the wire gainsthe
panicked/not-attemptedtags and their readback arms. Substrate first: the.dagcarrier is the authority and the seed mirrors it, and the production per-row comparator
already requires the two mappings to agree.
run_claimcaptures the unwind at the one seam that already classifies terminals.is a state the producer DECIDED to return, so invariants held; a panic is an invariant
violated at an unknown place, and a later row would carry an unstated precondition no row can
express — a green row after the unwind and one before it would render identically.
identity behind the unwind gets a
NotAttemptedrow naming what halted the line, so"stopped at claim 400 of 10439" and "10039 rows quietly missing" stop being the same artifact.
These rows are not executions and are not counted as any; the identity check now reads
planned == executed + not_attempted.ClaimTerminalitygainsUnwound, and its_ => VerdictReachedwildcard is DELETED. Thatwildcard would have reported a panicked claim as having reached a verdict — the same
wrong-fact defect
BudgetRefusedBeforeVerdictwas split to repair, one type over.Evidence: three
.dagwitnesses on the executing round-trip module, plus the new arms enrolled inthe_disposition_survives_the_round_trip_for_every_terminal_shape(12 shapes -> 15).DECLARED, NOT HIDDEN: an ENROLLED identity that panics is left as the roster join's
NotEvaluated { reason: "not_observed" }— disposition exactly right, reason generic — becausenaming the cause there needs an arm on
WitnessEvalVerdict, a GENERATED carrier. It lands withthat module's regeneration. The cause is not lost meanwhile: the terminal ledger carries it.
Post-merge with origin/main at 381137c:
cargo check --release -p v1-compiler --binsgreen (remote).🤖 Generated with Claude Code