Skip to content

Bazel-compatible target model: label subset, target identity, //:required aggregate, typed Build/TestStanding in .dag - #9227

Merged
briansrls merged 6 commits into
mainfrom
session/bold-hawk-65
Aug 26, 2026
Merged

briansrls merged 6 commits into
mainfrom
session/bold-hawk-65

Conversation

@briansrls

@briansrls briansrls commented Aug 25, 2026 •

Copy link
Copy Markdown
Contributor

What was missing

The repository decides its required set with run-level counters in the seed (RequiredFloorOutcome's planned / executed / passed / known_red_held / route_gap) and with per-identity ClaimDisposition rows in v2.workflow.floor_terminal_ledger. What does not exist anywhere is a target-grain carrier: a thing that says this identity, these edges, this standing, over which an aggregate can be folded. This lands one, on Bazel's own vocabulary rather than a name string.

The four cited surfaces (dag/extdeps/bazel/)

One ExternalModelScope per module, one shared subject symbol (bazel.dag bazel_product_name), per DESIGN §3 external upstream decomposition. All four enrolled in scope_carrier_paths.

  • label.dag — the label grammar as a declared subset. Four families the cited authority admits and this module does not — @repo//, package-relative :t / t, target patterns (..., :all, :*), and target names containing / — each refuse with their own named cause, not one MalformedLabel { text }. The repository axis has no field on Label at all, so an @repo// string cannot become a value later readers must remember to check (structural impossibility rather than a validator over a writable state). The cited shorthand (//my/app/lib ≡ //my/app/lib:lib) is folded at parse time, so the two spellings reach one value and label_eq is a usable identity.
  • test_status.dag — BlazeTestStatus at upstream arity (9) and upstream wire numbers, decoded fail-closed: an unknown wire number is BlazeTestStatusUnknownWireNumber, not NO_STATUS. Those are ⊥-as-answer and ⊥-as-ignorance, and their remedies are opposite (schedule the test / update this module).
  • build_event_stream.dag — Aborted.AbortReason, whole. Upstream's numbering is non-contiguous (NO_ANALYZE = 8, NO_BUILD = 9, after SKIPPED = 7); it is reproduced as declared, and a witness asserts exactly that, because a renumbered mirror of a wire vocabulary is a decode that silently lies.

Arms carry TestStatus / Abort prefixes deliberately: Passed and Failed collide with ClaimDisposition, and DESIGN §4b records that an ambiguous type name in this compiler resolves by silent last-import-wins rather than refusing. The upstream spelling is not lost — blaze_test_status_proto_name / abort_reason_proto_name carry it verbatim, which is what a wire comparison joins on.

The target model (dag/gunbc/build_target.dag)

  • Identity is the label and there is no second key. No id, no slug. target_identity renders it on every call, so it cannot drift from it.
  • //:required is an ordinary root-package target, not a distinguished constant of some AggregateId type — modelling the most important node in the graph outside the target vocabulary would put it outside every operation the graph supports.
  • BuildStanding is the pair upstream actually emits: TargetCompleted { success } or TargetAborted { reason }. A single built: Bool reports an analysis failure and a compile failure identically, and they have different owners.
  • TestStanding carries ClaimDisposition; it does not copy its arms. The floor owns that vocabulary one module away, and a parallel eleven-arm coproduct here would be §3 nicknaming. What this layer adds is the policy over it — a downstream fact by the same section — stated once in claim_disposition_satisfies, arm by arm with no wildcard, so a twelfth disposition added upstream fails to compile here instead of inheriting whichever verdict a _ happened to name.

Two states the obvious implementation gets wrong, refused in their own arms:

  • AggregateNoDependencies — a conjunction folded over an empty list is true, so the natural implementation reports a //:required that requires nothing as fully satisfied: the strongest green from the weakest evidence, and exactly what a mis-wired discovery pass produces.
  • DependencyStandingAbsent — a dependency nobody observed is not silence. Otherwise a standings list that lost rows reports the survivors as the whole answer (the empty-observation narrow, guarded at the join).

The aggregate reports every unsatisfied dependency, not the first: short-circuiting would make it a bisection tool where the number of runs needed equals the number of broken things.

Evidence — green by execution, with discriminating controls

20 witnesses in dag/test/claim/bazel_target_model_witness_test.dag, each run through gunbc run on the real compile path (--source-root dag --source-root src/v2). The file declares SubstrateInputsOnly, without which the floor's fail-closed default declines it — discovered, counted, never run.

The controls are what make them discriminating rather than green by construction:

  • the excluded label families are asserted against their own causes, so merging two arms goes red;
  • build_standing_dominates_test_standing uses a fixture whose test standing is a PASS, so consulting the test first or merging the two would make it satisfied;
  • aggregate_over_zero_dependencies_refuses carries a one-dependency positive control beside it, so it cannot pass by refusing everything;
  • abort_reason_preserves_upstream_numbering asserts the non-contiguous values, so tidying them into declaration order goes red;
  • export_reports_the_observation_not_the_policy asserts both halves: a held known-red satisfies //:required and exports as FAILED. Exporting it as PASSED would fabricate an observation nobody made; this is what keeps the policy and the observation from being merged in either direction.

What is deliberately out of scope

Nothing populates //:required from the live floor roster. That is wiring — the parent lane's move off claim_executor — and doing it here would have meant landing a discovery pass under a model-landing brief. The model is the prerequisite, and it is consumed by the floor's own ClaimDisposition today, so it is not an artifact with no final consumer.

Rung honesty

The label subset's excluded families sit at structurally impossible for the repository axis (no field exists) and structurally guaranteed for the rest (parse refuses on the acceptance path, measured). claim_disposition_satisfies' totality is structurally guaranteed — the wildcard-free match is the wall, not a lens over it. The aggregate's two refusal arms are mechanically preventable: the states are representable and the fold refuses them, rather than being unwritable. Their next-rung trigger is a non-empty-list carrier for the dependency roster and a standings map keyed by identity, neither of which exists in std today.

… not a name string

The repository's required set is decided by run-level counters in the seed and by
nothing at target grain: there is no carrier that says "this identity, these edges,
this standing". This lands one.

Four cited Bazel surfaces under dag/extdeps/bazel (one ExternalModelScope each, one
shared subject symbol): the label grammar as a declared SUBSET whose four excluded
families each refuse with their own cause; BlazeTestStatus and Aborted.AbortReason
at their upstream names, arities and wire numbers, decoded fail-closed so an unknown
number is not read as NO_STATUS.

gunbc.build_target joins them: identity IS the label and there is no second key,
//:required is an ordinary root-package target rather than a distinguished constant,
and TestStanding CARRIES v2.workflow.floor_terminal_ledger's ClaimDisposition rather
than copying its arms - the floor owns that vocabulary, this layer owns only the
policy over it (stated once, arm by arm, no wildcard, so a twelfth disposition fails
to compile here instead of inheriting a verdict).

Two states the obvious implementation gets wrong and this one refuses: an aggregate
over zero dependencies is its own arm, because a conjunction folded over nothing is
TRUE and would report a //:required that requires nothing as fully satisfied; and a
dependency with no standing is DependencyStandingAbsent, not silence, so a standings
list that lost rows cannot report the survivors as the whole answer.

Twenty witnesses, each with a discriminating control - the excluded label families
asserted against their own causes, the abort numbering asserted at the upstream
non-contiguous values, build-dominates-test asserted over a fixture whose test PASSES,
and the export asserted to report FAILED for a held known-red rather than fabricating
the pass its policy grants.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review August 25, 2026 19:57
Brian Searls and others added 2 commits August 25, 2026 20:40
…and `gunbc run` does not

The required parse sweep refused five lines in `extdeps.bazel.label` — two `//`
blocks written INSIDE function bodies, which DESIGN §4c admits only at module-item
grain. Both are moved above the declaration they describe; no code changed.

WHY IT REACHED CI: `gunbc run --entry ... --function ...` accepted the file and every
witness returned true, so the model was verified green on a path that cannot see this
class at all. The sweep is a separate phase over whole files, and its refusal then
took the v2-emission and floor phases down with it — three failed phases, one cause.
That is the execution-provenance gap DESIGN already records: a witness verdict and a
parse refusal are answers to different questions, and a green from the first is not
evidence about the second. Re-verified here against the instrument that owns the
question — `v1_src_dag_parse` over src/v1, dag and src/v2 — not against `gunbc run`.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…unrelated claims

The floor fold reported `failed=232` against main's `failed=0` on the same roster,
every one of them `call contract mismatch calling 'label_of': missing required
argument 'target'` in modules this change never touched.

The cause is this diff's. `test.claim.bazel_target_model_witness` declared a
module-level `fn label_of(package_segments, target)`, and `v2.std.node` takes
`label_of` as a FUNCTION-TYPED PARAMETER that its callers pass by bare name. Bare-name
resolution then bound those call sites to the two-argument global that had just
appeared in the corpus, so `test.claim.node_hash_protocol_witness` and its neighbours
called a Bazel label constructor with an edge-label argument.

The helpers are renamed to names that cannot be reached by accident
(`bazel_label_of`, `label_round_trips`, `target_standing_of`, and the rest). No
behaviour changed and every witness still holds.

WHAT THIS IS AN INSTANCE OF: the same silent last-import-wins hazard DESIGN §4b
records for census-ambiguous TYPE names, reached through FUNCTION names instead. Both
modules' Bazel enums already carried arm prefixes for exactly this reason — the
carrier was defended and the test helper beside it was not, which is where a generic
name is cheapest to write and most expensive to resolve.

Verified against the instruments that own each question: `v1_src_dag_parse` over
src/v1, dag and src/v2 for §4c, and the witnesses through `gunbc run`.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…is a parallel surface

Review 55919 (REQUEST_CHANGES) is right on all three counts, and the first one caught
this diff contradicting its own comment.

`blaze_test_status_is_pass` is DELETED, not relocated. It was a nine-arm Bool in the
UPSTREAM interface module, directly beneath a comment saying that a consumer treating
FLAKY as a pass has decided a policy question this vocabulary does not own -- which
that function then decided, there, for every consumer. The judgment now lives at the
layer that holds the policy, as `gunbc.build_target` `blaze_test_status_verdict`,
arm by arm and wildcard-free.

`claim_disposition_satisfies` and `aggregate_standing_blocks` return typed verdicts
instead of Bool: `claim_disposition_verdict -> StandingVerdict` and
`required_gate_decision -> RequiredGateDecision`. Neither is deleted, because the
grouping each expresses is a real single authority -- that KnownRedHeld satisfies and
that an aggregate requiring nothing stops the line are policies every consumer must
agree on, and pushing the match to each call site would let them drift. What changed
is that the return type now carries the reason.

WHAT THE BOOLS WERE COSTING, which is the part worth keeping: exhaustiveness at every
call site. A tenth BlazeTestStatus or a twelfth ClaimDisposition would have been
absorbed into `false` with nobody asked to decide -- the same silent-absorption shape
this model refuses elsewhere, committed by the functions guarding it. `w_refused_
verdict_names_the_disposition_it_refused` is new and asserts the recovered fact: the
refused arm names WHICH disposition it refused, where the Bool said only `false`.

Witnesses match the coproducts directly now rather than through a predicate, per the
`codex_preflight_ok` precedent. 21 witnesses green, 3998 files parse-clean.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Aug 26, 2026

Copy link
Copy Markdown
Contributor

Addressed in 6b81731 — all three findings in review 55919 accepted and fixed. Thank you for the first one in particular; it caught this diff contradicting its own comment.

blaze_test_status_is_pass — deleted, not relocated. You were right that it placed consumer policy in the upstream interface module, and the sharpest evidence was the comment sitting directly above it: it said a consumer treating FLAKY as a pass has decided a policy question this vocabulary does not own, and then the function decided exactly that, there, on every consumer's behalf. The arm-by-arm judgment now lives at the policy layer as gunbc.build_target blaze_test_status_verdict, returning StandingVerdict, wildcard-free. extdeps.bazel.test_status now carries a note above BlazeTestStatus recording why it holds no green/not-green predicate.

claim_disposition_satisfies → claim_disposition_verdict -> StandingVerdict and aggregate_standing_blocks → required_gate_decision -> RequiredGateDecision. I kept both as functions rather than pushing the match to every call site, and want to be explicit about that choice: the grouping each expresses is a genuine single authority — that KnownRedHeld satisfies the required set, and that an aggregate requiring nothing stops the line, are policies every consumer must agree on, and inlining them would let gates drift apart. What was wrong was the Bool return, not the existence of one decision point. Both now carry the reason in the type.

What the Bools were actually costing, which is the argument I should have made myself: exhaustiveness at every call site. A tenth BlazeTestStatus or a twelfth ClaimDisposition would have been absorbed into false with no call site asked to decide — the same silent-absorption shape the rest of this model refuses, committed by the three functions guarding it. I added w_refused_verdict_names_the_disposition_it_refused to assert the recovered fact: the refused arm names which disposition it refused, where the Bool said only false.

Witnesses now match the coproducts directly rather than through a predicate, following the codex_preflight_ok precedent in roadmap_belt_actuate_witness_test — which makes the same point, that matching in place recovers what the Bool discarded.

Verified: 21 witnesses green through gunbc run on the real compile path, and 3998 files parse-clean via v1_src_dag_parse over src/v1, dag, src/v2.

— sent from bold-hawk-65

briansrls and others added 2 commits August 25, 2026 21:10
…quiredFloorDisposition, with //:required derived from the Planned subset (#9246)

* The discovery census: one row per site, //:required derived from the Planned subset

`gunbc.build_target` landed the target-grain carrier and the `//:required`
aggregate, and deliberately left it unpopulated: nothing derived its
dependencies from the roster the floor actually discovers. `v2.workflow.required_floor`
owned the disposition VOCABULARY but not the DECISION -- the order in which a
site is declined lived only in the host loop that walks the corpus
(`v1_compiler.cli_run` `run_required_floor`), so a second walker would have had
to re-author it and could have re-authored it differently.

This lands both halves.

`required_floor_site_disposition` moves the admission order into the module
that owns the type: long home, then fixture home, then live tree, then
planned. It takes the declared `LiveTreeDisposition` rather than the boolean
the host computes one level up, so a third live-tree state fails to compile
here instead of being folded into whichever side of a Bool it was coerced to.
`required_floor_disposition_is_planned` is the wildcard-free predicate a
consumer reads.

`gunbc.discovery_census` is the join. One row per DISCOVERED site -- declined
rows included, because a census that dropped them derives the same
`//:required` and would pass every assertion about it. The row carries a
`Label` and no second identity field, for the reason `BuildTarget` carries
none. `//:required` is DERIVED from the Planned subset by one fold, so a
discovered site is either a dependency of it or carries the named disposition
saying why it is not; a hand-authored dependency list would be a second
population that disagrees the first time a witness is added, silently, in the
direction that under-runs.

Three states refuse rather than shrinking the census: a site whose module path
is empty, a site whose label the cited grammar refuses (this module mints no
second package grammar -- it renders the text and hands it to `parse_label`),
and two rows with one identity. A refused census yields
`RequiredAggregateUnderivable` carrying the cause, never an empty aggregate:
that would surface downstream as "requires nothing" when the real cause was a
site that could not be labelled.

14 witnesses, with the controls that make them discriminating: the fixture-home
fixture also reads the live tree, so reordering the two declines changes its
arm; a module whose name merely contains the long-home spelling is planned, so
the decline cannot pass under a `contains` test; the leading-empty-segment
control fails the obvious accumulator, which silently repairs `.a.b` into a
valid package; the duplicate is two DECLINED sites, which the host loop's own
uniqueness wall does not reach; and the all-declined census derives an
aggregate that BLOCKS, against a positive control where the derived aggregate
is satisfied over per-dependency standings.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01U7UX1cnZC3Cqf4Wh7qyrTi

* Fix two quadratic shapes in the census fold before they meet a five-figure roster

DESIGN's bare-minimum-cost rule names both by name and admits no "n is small
here" exception: rows were appended with concat(rows, [row]), copying the
accumulator once per site, and duplicate detection scanned the rows already
collected, comparing once per pair. Rows are now prepended and reversed once;
membership is a Map keyed on the rendered label, which is not a second identity
beside label_eq but the same relation that function is defined as, evaluated
once per row instead of once per pair.

Also: the header transcribed a run's offered-site count. DESIGN rules that a
measurement is cited by naming the producer that re-derives it, never by
copying its numbers into prose, so it names the instrument instead.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01U7UX1cnZC3Cqf4Wh7qyrTi

---------

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
… finish the same cleanup there

The census witness merged in from #9246 imports and calls `aggregate_standing_blocks`,
which does not exist. The obvious reading -- a witness referencing a function nobody
wrote -- is wrong, and the history says so:

  c57b3db:dag/gunbc/build_target.dag  aggregate_standing_blocks -> 1
  e887a2a:dag/gunbc/build_target.dag  aggregate_standing_blocks -> 1
  6b81731:dag/gunbc/build_target.dag  aggregate_standing_blocks -> 0

It existed. #9246 branched from e887a2a and wrote a correct witness against the API
as it stood; 6b81731 dissolved that predicate under review 55919 and took the symbol
out from under a stacked branch whose author had already closed. The break is mine.

The predicate does NOT come back -- restoring it to unbreak a downstream caller would
revert a review finding to avoid an edit. The witness arm is REWRITTEN rather than
deleted: it now matches `required_gate_decision` and asserts `RequiredGateStops`
CARRYING `AggregateNoDependencies`, so it still proves an all-declined census derives an
aggregate that stops the line, and additionally proves WHICH standing stopped it -- a
fact the Bool could not express.

WHY THIS REFUSED THE WHOLE FLOOR RATHER THAN ONE ROW: name resolution runs at strict
preparation, upstream of every witness, so nothing executed at all. Measured both ways
here -- 16 of 16 NOVALUE before, 16 of 16 true after.

Also takes review 55984's non-blocking observation, which is the same class one module
over: `required_floor_disposition_is_planned` was a Bool over the closed
`RequiredFloorDisposition`, and its only consumer filtered a roster with it -- keeping
the routed side and DISCARDING the declined one, which is precisely the fact the census
exists to carry. Replaced by `census_partition`: one pass, both sides, wildcard-free
descent, with a witness asserting planned + declined == all and that the declined side
is non-empty on the fixture.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@briansrls
briansrls merged commit cd7cf33 into main Aug 26, 2026
3 checks passed
@briansrls
briansrls deleted the session/bold-hawk-65 branch August 26, 2026 05:10
briansrls pushed a commit that referenced this pull request Aug 26, 2026
…sposition

#9227 landed a .dag authority for the floor's admission order whose middle arm
was the fixture home this branch deletes. #9227's construction is kept whole --
ModulePrefixMatch, first_module_prefix_match, and the typed LiveTreeDisposition
input -- and only the fixture arm is cut, which is the wildcard-free wall doing
its job: three consumers failed to compile rather than inheriting an arm.

required_floor.dag: fixture_home_prefixes, DeclinedFixtureMember and the arm are
gone. #9227's header argued the ordering was load-bearing BECAUSE a fixture
member that also read the live tree had to report the permanent ownership fact
over the staged prediction. That argument dies with the arm, so it is rewritten
rather than left standing: the surviving long-home-over-live-tree precedence has
no executing discriminator, since no site can be both, and the header now says
so and says not to cite it as covered.

discovery_census.dag: the arm is removed from census_partition_step and
census_counts_add and the declined_fixture_member counter field with it.

discovery_census_witness_test.dag: w_fixture_home_dominates_live_tree is deleted
-- its subject is gone, and repointing it at a live fixture home is the borrowed
-home move this cut already refused once. The mixed population stays at five
sites, the fixture site becoming a second live-tree read, so every assertion
denominated in the population size is unchanged and only the arm it lands in
moved.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot pushed a commit that referenced this pull request Aug 26, 2026
This branch is cut from the plan/walk residue branch, so it carries that
branch's required_floor deletion and hit main's #9227 conflict identically.
Merging the parent branch inherits the resolution made there rather than
re-deriving it, which is the point: one resolution, not two.

DESIGN.md was reported unmerged by the generated-artifact merge driver, which
refuses BY POLICY whenever both sides touch a generated path -- it does not mean
the content collides. It does not here: a three-way merge of the two sides is
clean, and DESIGN.md and its authority dag/gunbc/design_document.dag each move
by exactly the same one row, so the projection and its source stay in agreement.
The drift gate is the check on that, not this message.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot pushed a commit that referenced this pull request Aug 26, 2026
…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>
briansrls pushed a commit that referenced this pull request Aug 26, 2026
…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>
briansrls added a commit that referenced this pull request Aug 28, 2026
* 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>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant