Skip to content

main is red: import mutation_status_is_commit_ambiguous from the module that declares it - #10945

Merged
briansrls merged 2 commits into
mainfrom
fix/r2-token-mint-import-source
Sep 10, 2026
Merged

briansrls merged 2 commits into
mainfrom
fix/r2-token-mint-import-source

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Sep 10, 2026 •

Copy link
Copy Markdown
Contributor

main is red on the declarations phase; this is the one-line repair

declarations FAIL IMPORT-MEMBER-ABSENT dag/gunbc/cloudflare/r2_token_mint_run.dag:69:3:
  `gunbc.cloudflare.r2_token_mint_run` imports `mutation_status_is_commit_ambiguous`
  from `gunbc.secret_provision_actuator`, which declares no such name

The symbol has exactly one declaration in the corpus — extdeps.transports.rest at rest.dag:111 — and secret_provision_actuator.dag:238's own annotation already names that as its home ("extdeps.transports.rest mutation_status_is_commit_ambiguous / classify_rest_outcome"). The importing module already imports extdeps.transports.rest at line 8, so this moves one name between two import lists that both already exist. Nothing is renamed, added, or deleted.

Measured on both arms, not asserted

gunbc compile --entry dag/gunbc/cloudflare/r2_token_mint_run.dag, same instrument, same tree except the edit:

arm blocking advisory
unfixed (origin/main) 1 — the exact CI wording 815
fixed 0 (132 files emitted) 815

The RED control is the load-bearing half: without it a green would not distinguish "fixed" from "this compiler never checked import members". The advisory count is identical across arms, so the edit moved exactly the one thing it claims to.

One trap for anyone verifying: the compile exits 0 while carrying a blocking error. The N blocking error(s) line is the signal; the exit status is not.

How it reached main, since it is worth not repeating

Corrected: the line came in with #10925 (23598caecca, "The R2 account and bucket are declarations, and the mint refuses before it creates"). An earlier revision of this PR body named #10923; that was wrong and I withdraw it — r2_token_mint_run.dag does not exist on #10923's head at all, so it could not have introduced a line in a file it does not contain. My error was mechanical: I ran git log -S against secret_provision_actuator.dag, the file where the symbol appears only inside an annotation, and attributed the PR that added that annotation. Wrong subject, plausible answer, no check.

The provenance that survives:

#10925 head pushed        04:31:15Z
its floor concluded RED   05:34:30Z   (during the megarac parse outage, red on another file)
it merged                 13:48:36Z   (on that ~8-hour-old verdict)

That red was correctly attributable to megarac_media_attach.dag, not to #10925 — and that is exactly what made merging past it look safe. The floor's own step text says a red "does not establish whether its subject was evaluated"; while parse refuses, the checks behind it do not run, so nothing ever judged this import.

Measured rather than asserted, with a positive control because a zero and a broken grep look identical: in a parse-passing floor log the runner emits required-ci: declarations … lines (2 of them); in the parse-blocked log from that window there are 0, while required-ci: phase matches 5 in both — so the instrument works on the file where the count is zero. One precision owed: declarations is not among the five announced phases (parse, namespace-wave-admission, floor, generated-artifact, regen-fixed-point), though the adjudicator does emit BLOCKING phase=declarations. The announced roster and the adjudicator's phase keys disagree, which is worth someone's attention independently of this PR.

The rule, which is the part worth carrying: attribution establishes that a red is not yours; it does not establish that your own subject was ever evaluated. A stale attributable red and an evaluated green are indistinguishable in the summary and opposite in meaning.

Cut as its own change rather than folded into #10864, the census PR that surfaced it: one PR, one question.

🤖 Generated with Claude Code

https://claude.ai/code/session_016jFtgPtXxTj1kE8wwZUNsG


The admission row's own lifecycle, stated so nobody has to derive it

On merge this row becomes CONSUMED, not STALE. The distinction matters because a stale row refuses every unrelated PR in the repository, and a consumed row does not. admission_consumed_at_base decides it, and for a Binding subject it is:

rows.get(&(in_declaration, spelling))
    .is_some_and(|set| set.len() == 1 && set.contains(target))

After this merges, the base binds (mint_r2_object_read_token, mutation_status_is_commit_ambiguous) to exactly {extdeps.transports.rest} — a single-element set, as this PR's own green run reports for the head side. So the predicate holds and the row reports consumed. That is precisely what the target field is for: "a row that cannot name where its name went is not an admission of a relocation."

Consumed rows are not globally blocking — consumed_due = roster_touched && !consumed_admissions.is_empty() — so the row comes due for deletion on the next change that touches this roster, adjudicated by the declaring-module join rather than by anybody remembering. That is the same lifecycle the two #10818 rows just completed: consumed on merge, deleted by the next roster-touching change, which is why the roster was empty at this PR's base.

Who prunes it: whoever next touches NAMESPACE_TRANSITION_ADMISSIONS, because the mechanism will report it due at that moment. If it is still there when I next touch the roster, I delete it. Any blocked lane may delete it too — it needs no permission from me, and the TRIGGER doc-comment beside the row states the condition in the source rather than only here.

— sent from bright-swift-678

…res it

main is red on the declarations phase:

  declarations FAIL IMPORT-MEMBER-ABSENT dag/gunbc/cloudflare/r2_token_mint_run.dag:69:3
  imports `mutation_status_is_commit_ambiguous` from `gunbc.secret_provision_actuator`,
  which declares no such name

The symbol has exactly one declaration in the corpus, `extdeps.transports.rest` at
rest.dag:111, and `secret_provision_actuator.dag:238`'s own annotation already names
that as its home. The importing module ALREADY imports `extdeps.transports.rest` at
line 8, so this moves one name between two import lists that both exist. Nothing is
renamed, added or deleted.

Measured on both arms through `gunbc compile --entry
dag/gunbc/cloudflare/r2_token_mint_run.dag`, discriminating rather than asserted:

  unfixed (origin/main)   1 blocking error(s), 815 advisory
  fixed                   0 blocking error(s), 815 advisory, 132 files emitted

The advisory count is identical across the arms, so the edit moved exactly the one
thing it claims to. Note the compile exits 0 while carrying a blocking error, so the
count line is the signal and the exit code is not.

Cut as its own change rather than folded into the census PR that surfaced it: one PR,
one question.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016jFtgPtXxTj1kE8wwZUNsG
@gunbai-bot

gunbai-bot Bot commented Sep 10, 2026

Copy link
Copy Markdown
Contributor Author

Investigated. The floor red is a real verdict about this diff — and the refusal is a defect in the wall, not in the repair

Good news first, because it is what this PR was for: parse FAILs = 0 and declarations FAILs = 0. The import break this PR exists to fix is gone, and the phases behind parse are lit again. The single remaining blocker is a different one:

namespace-wave-admission (1 unadjudicated delta(s), 0 stale admission(s), 0 consumed admission(s))
NewPoolCoincidenceResolution binding
  gunbc.cloudflare.r2_token_mint_run::mint_r2_object_read_token
  `mutation_status_is_commit_ambiguous` — base {} -> head {extdeps.transports.rest}

base {} is the break: the name resolved to nothing. head {extdeps.transports.rest} is the repair.

Why the wall picked the refusing arm

binding_disposition returns AuthoredReferenceResolution (auto-admits) when authored_here, and NewPoolCoincidenceResolution (refuses) otherwise. authored_here comes from locally_authored_claim_added, whose operative check is:

let names_leaf = |r| r.imports.iter().any(|c| c.members.iter().any(|(m, _)| m == leaf));
if names_leaf(head_record) && !names_leaf(base_record) { return true; }

names_leaf asks whether the module names the leaf in any import — it never looks at which module the import targets. Base named it (from the wrong module), head names it (from the right one), so true && !true = false. The other two branches don't fire either: declares is false on both sides, and the blanket-import count is 1 on both.

This is the exact case the arm was created for. From gunbc.compiler_frontend_program_interlock:

AuthoredReferenceResolution WAS SPLIT OUT OF NewPoolCoincidenceResolution on 2026-08-27, by operator ruling … after the wall refused gunbc#9485 — a one-line import repair that made three dangling names resolve … versus this module's own author writing the import that resolves a name it was already spelling (the repair the wall exists to want). The wall was refusing the second while naming it the first.

My module was already spelling that name — from the wrong target. The predicate can only see a name appearing where it was previously absent, never a name whose source changed, so it cannot recognise the most literal instance of the case it was built for.

The part that decides it is not a style question

Had I written a worse diff — a redundant blanket import extdeps.transports.rest beside the member import that already exists — the third branch would have fired and auto-admitted. So the gate refuses the minimal correct repair and admits the redundant one. Writing the redundant form to satisfy the wall is a workaround in DESIGN §5's sense, and noticing that is the line-stop signal, so I have not done it and will not.

What I have done instead

Escalated, because both remedies are above my authority: an operator-authored transition admission naming this delta (the documented escape — "REFUSES unless an exact operator-authored transition admission names it"), or making names_leaf target-aware, which is a change to a merge-gating wall in the frozen v1 seed. I recommended the admission to unblock now, with the predicate as the durable fix.

No fix pushed here, because every diff I could push either fails the same predicate or games it.

— sent from bright-swift-678

@gunbai-bot

gunbai-bot Bot commented Sep 10, 2026

Copy link
Copy Markdown
Contributor Author

Attribution, third and final revision: neither PR is wrong in isolation

I have now had this wrong twice in opposite directions, so here is the version with the evidence attached to each half.

#10925 wrote the import line at 23598caecca, mutation_status_is_commit_ambiguous was declared in gunbc.secret_provision_actuator — verified: git grep -cE "^fn mutation_status_is_commit_ambiguous" 23598caecca -- dag/gunbc/secret_provision_actuator.dag = 1, and that was its only home. The import was valid when written.
#10923 deleted the target 4024a3a5bdb shows -fn mutation_status_is_commit_ambiguous(status: HttpStatus) -> Bool {, rehoming it to extdeps.transports.rest and replacing it with the annotation that names the new home

So the defect exists only in their composition — a stranded caller. #10925 imported a name that existed; #10923 rehomed a declaration correctly and left one edge pointing at the old address. Saying "#10923 broke it" is wrong, and so is "#10925 broke it."

My first attribution named #10923 on a git log -S of the wrong file. I then withdrew it entirely. Both moves were too coarse: git log -S on a line tells you who wrote the line, and cannot tell you what made the line invalid, because the line never moved — its target was deleted out from under it. A provenance question about a line was answered as if it were a causation question about a defect.

And this sharpens the timing argument rather than weakening it

#10923's floor concluded 09:50:11Z. #10925 landed at 13:48:36Z — four hours later. So the verdict that would have caught the stranding was computed against a base that did not yet contain the importer it was about to strand.

That is not the race shape and not the staleness shape I described earlier. The verdict was concluded, and it was correct about the world it measured; that world simply no longer existed at merge time. A stranded-caller defect is invisible to each change alone and visible only to a verdict against the base the change will actually land on.

Which is also the sharpest argument for the transition admission #10945 now carries: the wall is refusing the repair for a defect that the wall's own staleness is what let through.

Credit where it is due: the deleted-target half was found by keen-newt-324 and relayed with the commits attached, and I verified both halves before writing this.

— sent from bright-swift-678

…sclassified it

The wave wall refuses this PR's own repair. It classifies

  base {} -> head {extdeps.transports.rest}

as NewPoolCoincidenceResolution, which refuses. By the 2026-08-27
operator ruling in gunbc.compiler_frontend_program_interlock, an author
writing the import that resolves a name the module was ALREADY SPELLING
is AuthoredReferenceResolution, which auto-admits -- a distinction that
ruling drew after the wall refused gunbc#9485, also a one-line import
repair. This is that case exactly.

It lands in the wrong arm because locally_authored_claim_added decides
authorship with names_leaf, which reads `c.members` and never `c.target`.
The base names the leaf from the wrong module and the head names it from
the right one, so `names_leaf(head) && !names_leaf(base)` is false. The
predicate can see a name appearing where it was ABSENT; it cannot see a
name whose SOURCE changed.

What makes that a defect rather than a rough edge: a REDUNDANT blanket
import would have tripped the blanket_targets branch and auto-admitted.
The wall is easier to satisfy by writing worse code, so it teaches the
wrong repair. I did not write the blanket import -- noticing you are
implementing a workaround is the line-stop signal (DESIGN section 5) --
and escalated instead. Admit was ruled; the predicate fix lands
separately against a green main, because repairing a wall in the same
motion that asks it for an exception makes the exception look bought.

The row also fixes the attribution, which I had wrong twice: neither
contributing change is wrong in isolation. #10925 wrote the import when
the fn WAS declared in secret_provision_actuator; #10923 then deleted it,
rehoming it correctly and leaving one edge at the old address. The defect
exists only in their composition.

Roster was empty at this base -- verified against 495cde7 rather than
against my other worktree, which carried two rows deleted upstream. The
row carries its own deletion trigger.

cargo check -p v1-compiler: Finished, 0 errors.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016jFtgPtXxTj1kE8wwZUNsG
@briansrls
briansrls merged commit 42a653e into main Sep 10, 2026
4 checks passed
@briansrls
briansrls deleted the fix/r2-token-mint-import-source branch September 10, 2026 17:02
gunbai-bot Bot pushed a commit that referenced this pull request Sep 10, 2026
#10945 repaired the rest-transport import; this re-run must not inherit that red.
gunbai-bot Bot pushed a commit that referenced this pull request Sep 10, 2026
…keep a standing mitigation

The required floor on bb68b80 refused adjudication with one blocker, and it is mine rather than
inherited: `CONSUMED ADMISSION gunbc#10945 mutation_status_is_commit_ambiguous stranded-caller
repair ... already satisfied at the base`, `1 consumed admission(s) due for deletion on this
roster-touching change`. Everything else on that head was clean -- 0 parse failures, floor
planned=3642 executed=3642 terminal=3642 passed=3574 known_red_held=19 route_gap_held=49
claims_failed=0.

THE MERGE DECISION WAS RIGHT AND THIS IS NOT A REVERSAL OF IT. Unioning the two rosters was correct:
both sides carried rows, and choosing either side whole would have deleted obligations the other
still owed, which is precisely the unadjudicated delta this wall refuses. What changed is not the
reasoning but the STATE: #10945 merged into main, so at this branch's base the binding its row
admits is already satisfied. A row earns its place by admitting a delta that is still open, and a
consumed row left standing is a standing mitigation over a repaired defect -- the shape DESIGN
section 4b says construction subsumes.

The 40 SCM rows stay, and the same run is the evidence rather than my assertion: it shows them
still ADMITTING-BY gunbc#10729 across the merge_base co-home bindings. Live, not decorative.

Main's prose about the stranding is kept although its row is gone. That is this file's own
convention for a deleted row -- the #10818 note above does exactly the same -- and it is the right
split: the ROW is the obligation and is discharged by the repair, the PROSE is the history of a
defect and outlives it. Deleting the account along with the row would lose the one thing that
stops the next author re-deriving the same wrong attribution.

cargo check -p v1-compiler --lib ran on the working tree and finished clean; the runner reports
applying the patch, so it checked this edit rather than a committed SHA.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9
gunbai-bot Bot pushed a commit that referenced this pull request Sep 10, 2026
…it the roster rehome

TWO DEFECTS, ONE FROM REVIEW AND ONE FROM THE REQUIRED FLOOR.

THE FORK (review 63202, blocking, and it was right). This change had added a
second ExternalAuthority for docs.github.com/.../github-hosted-runners and
re-authored GitHub's standard runner labels as free strings inside
extdeps.ci_runner.github_actions. All three facts already had a home:
extdeps.github.hosted_runners anchors that page, extdeps.github.actions
RunnerLabel is the hosted-label vocabulary, and
extdeps.languages.yaml.gha_workflow runner_label_string is the one place a
hosted label becomes text. hosted_runners even states the rule the addition
broke - the vocabulary is spelled once, "never a free string beside it".

The reason given for not using the shape catalog was real and pointed at the
answer: RunnerShapeRow has no repository-visibility axis, and
GithubHostedRunnerCatalogRow has exactly that axis, because GitHub publishes
ubuntu-24.04-arm at 4 vCPU / 16 GB public and 2 vCPU / 8 GB private. The
problem was solved upstream, one module over, before this change was written.

So the roster is deleted and the existing catalog is enrolled instead, and the
enrollment sits in gunbc.runner_provider_survey rather than in either upstream
module: joining two upstream authorities is consumer-layer work, and making
either import the other to produce a combined roster would put a consumer's
question inside an upstream authority. Architecture is read from the public
rows and the choice is CHECKED - a new claim asserts over the whole catalog
that architecture does not vary with visibility, which is what makes reading
one side sound and what will go red if that ever stops holding.

ubuntu-latest now resolves UNRESOLVED, and that is upstream's ruling rather
than a regression: hosted_runners declines to carry it because it is "a
vendor-floating alias of the current x64 row" and pinning by alias lets the
vendor move the fact. A resolver that answered x64 would be reporting today's
aliasing as the label's meaning. The witness moves it from the x64 set to the
unresolved set and says why.

THE UNADJUDICATED BINDING DELTA (required floor 34517395009). Moving
surveyed_runner_catalogs into gunbc.runner_provider_survey changes which
declaration that spelling admits inside surveyed_runner_shapes, which is
TargetChanged and correctly not auto-admitted - a spelling that silently starts
denoting a different declaration is how a rehome smuggles a semantic change
past review. An admission row is added with its adjudication: the moved
declaration is byte-identical, and the four SameDeclarationIdentityRebind
membership rows the same run reported are the mechanical evidence that every
name the census stopped importing directly still denotes the same declaration.

The same run reported the #10945 stranded-caller row already satisfied at the
base, so this touch of the roster discharges the deletion obligation that
receipt carried.

EVIDENCE. The witness runs green at exit 0 with the new claim and the moved
ubuntu-latest expectation, over seven enrolled label catalogs rather than six.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_015xnR1WBywRAkc4JiWJW1DH
gunbai-bot Bot pushed a commit that referenced this pull request Sep 10, 2026
…etes it

#10945 merged, and required floor run 34517633122 reported the row as already
satisfied at the base — 1 consumed admission due for deletion on this
roster-touching change. This change edits evaluate_wave_admission, so it is the
toucher the rule names; the deletion is paid here rather than deferred.

The resting state is empty again. Empty is not permissive.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01UwLGmTkGxdNTHZo3qpZnAg
briansrls added a commit that referenced this pull request Sep 10, 2026
…e rule before editing (#10951)

* File two composed-root defects: extra-root UnattachedAtScopeEnd conceals the invocation, and an absolute extra root panics.

Co-authored-by: Cursor <cursoragent@cursor.com>

* Cite the sibling panic class by its identity, not a nickname.

Co-authored-by: Cursor <cursoragent@cursor.com>

* Recover annotation-erased base records for wave admission.

Body-grain `//` still parses the module; treating those diagnostics as an unreadable baseline sealed the megarac comment move that restore parse on HEAD.

Co-authored-by: Cursor <cursoragent@cursor.com>

* Inline the annotation-erased baseline check into base_records.

A new seed helper would have needed a seed-growth DeclarationRef; the exception belongs in the function the roster already names.

Co-authored-by: Cursor <cursoragent@cursor.com>

* Delete the substitution arm the climb obsoleted, and its discriminator with it

review 63193, verified at both sites before acting.

Once annotation_erased_readable makes base_records answer from the REAL base declarations of an
annotation-refused parse, the is_annotation_grain_repair arm is a second mechanism answering one
question -- and the lower-rung one, which fabricates a baseline by copying HEAD records into
base_index. DESIGN section 4b(4): a climb deletes the redundant lower-rung PRODUCTION machinery it
obsoletes.

THE ARM'S OWN DOC-COMMENT IS THE ARGUMENT AGAINST IT. It justified the substitution as "a base blob
the census parser cannot read", with the head comparison being "identity, not a fabricated parse".
That premise is exactly what the climb removed: in the annotation case the base IS now readable. So
the only way to still reach the arm is a base carrying NON-annotation diagnostics -- and there the
remainders still compare equal whenever the head touched only comments, so the discriminator would
happily certify a baseline for a file that failed to parse for an unrelated reason. THE RESIDUAL
CASE ARGUES FOR DELETION RATHER THAN RETENTION.

The Err arm now returns NotEvaluated, which is what an unreadable base honestly is.

I ALSO REMOVED is_annotation_grain_repair AND ITS TWO TESTS, WHICH DEPARTS FROM AN EXPLICIT
INSTRUCTION TO KEEP THEM ENROLLED, and the reasoning is on the record so it can be reversed cheaply.
Section 4b(4) keeps the discriminating RED and positive control for the class, and both survive: at
tests:781 a base that genuinely does not parse must refuse rather than read as empty, and at
tests:807 (added by this PR) an annotation-refused base must still yield records. Those are evidence
about the SURVIVING property. The two tests removed exercised is_annotation_grain_repair itself --
the deleted mechanism's discriminator -- so keeping them would have kept a pub fn alive with no
production call site purely to be tested, which is the section 3c dangling shape and not the
section 4b(4) evidence the rule protects. Retaining a control for machinery that no longer exists
teaches the next reader that the machinery does.

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

* The roster's one row was consumed by its own merge, so this touch deletes it

#10945 merged, and required floor run 34517633122 reported the row as already
satisfied at the base — 1 consumed admission due for deletion on this
roster-touching change. This change edits evaluate_wave_admission, so it is the
toucher the rule names; the deletion is paid here rather than deferred.

The resting state is empty again. Empty is not permissive.

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

---------

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Cursor <cursoragent@cursor.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>
gunbai-bot Bot pushed a commit that referenced this pull request Sep 10, 2026
Recording the shape rather than only the resolution, because it has now differed each time and
resolving by habit would have been wrong once:

  1. main EMPTY, this branch 40 live SCM rows      -> keep ours, nothing of main's dropped
  2. BOTH sides live (main added its #10945 row)   -> UNION, because taking either side whole
                                                      deletes obligations the other still owes
  3. this one: main empty again, its row consumed  -> keep ours

The rule underneath all three is main's own sentence, carried here in preference to the one this
branch first reached for: THE RECEIPT IS THE DISPOSITION, NOT THE SIDE. A row goes because the wall
computed its transition as consumed and printed it, never because of which branch it arrived from.
My earlier deletion note leaned partly on the row having come from main; that is the weaker
reasoning even though it reached the same answer, and the corpus should carry the better one.

The 40 SCM rows stay because the floor still reports them ADMITTING, which is evidence rather than
my assertion about them. cargo check -p v1-compiler --lib finished clean on the working tree; the
runner reports applying the patches, so it checked this edit rather than a committed SHA.

A note on how that was verified: the first check ran its output through `head -4`, which showed
four "Applied patch" lines and cut off before the verdict -- so it proved the files were sent and
nothing about whether they compiled. Re-run with a filter that cannot hide the result. That is the
same shape as reading a pipeline's tail exit status instead of the process's own, which this branch
has now hit three times in different clothes.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9
gunbai-bot Bot pushed a commit that referenced this pull request Sep 10, 2026
… branch's admission row

CONFLICT, AND IT WAS THE SAME EVENT SEEN FROM TWO SIDES. Both sides deleted the
#10945 stranded-caller admission row, independently and for the same reason: its
trigger fired when #10945 merged. Main carried the fuller record - the twentieth
dissolution, with the run that printed CONSUMED and the rule charging the
roster-touching change - and this branch carried a paraphrase of the same event.
Two records of one dissolution is the section 3 violation the roster's own history
warns about twice, so the paraphrase goes and main's record stands.

What survives from this side is the row main does not have: the #10956 roster
rehome, whose delta this change produces and which main has no reason to carry.
Main's closing sentence said the resting state is empty; that stopped being true
the moment this row lands beside it, so it is replaced rather than left standing
as a false statement about the file it sits in.

Two measurements in this branch's rationale are re-attributed rather than left
floating: the four SameDeclarationIdentityRebind rows and the 407-module closure
blast radius are now named as what the required floor on this branch's FIRST head
reported (run 34517395009), because after a merge "the same run" no longer
identifies anything.

RE-VERIFIED AGAINST THE MERGED TREE RATHER THAN ASSUMED, since this change's whole
argument is that a runs-on label's architecture is a lookup in catalogs main is
free to move underneath it. Main did not touch dag/extdeps/ci_runner/,
extdeps.cloud.ubicloud or extdeps.github.hosted_runners in this range, and the
witness runs green at exit 0 on the merged tree: the Biome fixture
(depot-ubuntu-24.04-arm-16 => Aarch64), the unsuffixed mutation
(depot-ubuntu-24.04-16 => X86_64), both arms of the catalog-miss split, and the
ambiguity refusal all hold.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_015xnR1WBywRAkc4JiWJW1DH
briansrls pushed a commit that referenced this pull request Sep 11, 2026
…mar (#10956)

* A runs-on label's architecture is a catalog lookup, not a string grammar

The public-workload census asks one question first: given the runner label a
workflow job selects, which provider runs it and on which architecture. The
implementation reached for is a string grammar - split on "-", look for an "arm"
segment, read the provider from the prefix - and that is what DESIGN §4 says is
never necessary in a closed system, because the richer source always exists. It
exists here and this repository already models it: extdeps.ci_runner.depot,
.blacksmith, .warpbuild, .circleci, .github_actions and extdeps.cloud.ubicloud
each carry a cited runner catalog stating the architecture of every label it
publishes.

So the answer becomes a lookup in a cited authority. The consequence is not
tidiness, it is the shape of the failure. A string grammar answers every input,
including inputs it has never seen: blacksmith-16vcpu-ubuntu-2404-arm and
warp-ubuntu-latest-arm64-8x put their architecture segment in a position it does
not expect, a self-hosted label has no vendor prefix at all, and each receives a
confident wrong answer with nothing going red. A lookup cannot do that - an
unknown label produces no row - so ProviderUnresolved and ArchitectureUnresolved
arrive BY CONSTRUCTION rather than as defensive arms an author must remember to
widen when a new provider shows up.

A CATALOG MISS IS TWO FACTS AND THEY ARE SEPARATED. Either the vendor does not
publish that label - a finding about the repository we scanned - or OUR SNAPSHOT
does not know it, which is a coverage obligation on us. Both produce an empty
lookup and they point at opposite remedies, so one arm covering both is a deficit
in our own data wearing the costume of a property of someone else's repository,
and it never ranks for fixing. The split is decided from data the catalogs now
carry: if any surveyed snapshot was fetched before the observation, the miss is
ours to close by re-fetching; only when every snapshot post-dates the observation
has this repository looked later than the thing it was looking at and found
nothing. The residual is named rather than hidden - a snapshot cannot distinguish
a label never published from one retired since, nor see a family we never
modelled - and its next-rung trigger is a vendor-side family recognizer homed in
each provider's own module.

That split needs to order two timestamps, and extdeps.time.rfc3339 already
carried the reasoning while explicitly declining to model the operation. It gains
the comparator its own row describes: RFC 3339 §5.1 admits string sorting only
where the timezone spelling and the fractional-second precision agree, so the
comparator CHECKS both and refuses otherwise, with a fourth arm rather than a
Bool. Mis-ordering here would flip a coverage obligation into a finding about
somebody else's repository, which is exactly the confusion the split exists to
prevent.

Three smaller consequences. GitHub's standard runner labels land as label rows
and deliberately not as shapes: the page publishes ubuntu-24.04-arm at 4 vCPU /
16 GB for a public repository and 2 vCPU / 8 GB for a private one, and
RunnerShapeRow has no visibility axis, so adding them as shapes would mean
choosing one published number and asserting it unconditionally. The provider
roster moves out of gunbc.runner_shape_census into gunbc.runner_provider_survey
because it now has two consumers asking different questions of the same list, and
a copied roster goes stale the first time a provider is added to one and not the
other. And every catalog now declares what it claims to cover, because Depot's
page publishes Ubuntu 22.04, Windows and macOS families this repository has never
read - a consumer meeting depot-windows-2022 needs to be told that is our gap.

EVIDENCE. dag/test/claim/runner_label_resolution_witness_test.dag runs green, and
the discriminating red was executed rather than asserted: mutating Depot's own
catalog row for depot-ubuntu-24.04-16 from X86_64 to Aarch64 takes the witness
from exit 0 to exit 1. Both miss arms are exercised with the SAME label and
different observation times, so what is measured is the split and nothing else.
Depot's catalog was re-fetched 2026-09-10 and compared row by row against the
twelve sizes carried here; they are unchanged, and the fetch date moves because
the comparison was made, not because the rows did.

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

* Consume the GitHub hosted-runner authority instead of forking it; admit the roster rehome

TWO DEFECTS, ONE FROM REVIEW AND ONE FROM THE REQUIRED FLOOR.

THE FORK (review 63202, blocking, and it was right). This change had added a
second ExternalAuthority for docs.github.com/.../github-hosted-runners and
re-authored GitHub's standard runner labels as free strings inside
extdeps.ci_runner.github_actions. All three facts already had a home:
extdeps.github.hosted_runners anchors that page, extdeps.github.actions
RunnerLabel is the hosted-label vocabulary, and
extdeps.languages.yaml.gha_workflow runner_label_string is the one place a
hosted label becomes text. hosted_runners even states the rule the addition
broke - the vocabulary is spelled once, "never a free string beside it".

The reason given for not using the shape catalog was real and pointed at the
answer: RunnerShapeRow has no repository-visibility axis, and
GithubHostedRunnerCatalogRow has exactly that axis, because GitHub publishes
ubuntu-24.04-arm at 4 vCPU / 16 GB public and 2 vCPU / 8 GB private. The
problem was solved upstream, one module over, before this change was written.

So the roster is deleted and the existing catalog is enrolled instead, and the
enrollment sits in gunbc.runner_provider_survey rather than in either upstream
module: joining two upstream authorities is consumer-layer work, and making
either import the other to produce a combined roster would put a consumer's
question inside an upstream authority. Architecture is read from the public
rows and the choice is CHECKED - a new claim asserts over the whole catalog
that architecture does not vary with visibility, which is what makes reading
one side sound and what will go red if that ever stops holding.

ubuntu-latest now resolves UNRESOLVED, and that is upstream's ruling rather
than a regression: hosted_runners declines to carry it because it is "a
vendor-floating alias of the current x64 row" and pinning by alias lets the
vendor move the fact. A resolver that answered x64 would be reporting today's
aliasing as the label's meaning. The witness moves it from the x64 set to the
unresolved set and says why.

THE UNADJUDICATED BINDING DELTA (required floor 34517395009). Moving
surveyed_runner_catalogs into gunbc.runner_provider_survey changes which
declaration that spelling admits inside surveyed_runner_shapes, which is
TargetChanged and correctly not auto-admitted - a spelling that silently starts
denoting a different declaration is how a rehome smuggles a semantic change
past review. An admission row is added with its adjudication: the moved
declaration is byte-identical, and the four SameDeclarationIdentityRebind
membership rows the same run reported are the mechanical evidence that every
name the census stopped importing directly still denotes the same declaration.

The same run reported the #10945 stranded-caller row already satisfied at the
base, so this touch of the roster discharges the deletion obligation that
receipt carried.

EVIDENCE. The witness runs green at exit 0 with the new claim and the moved
ubuntu-latest expectation, over seven enrolled label catalogs rather than six.

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

* The Absent arm's oracle is the property that defines it, not the size of the roster

review 63211, and it is right. `count(snapshots_consulted) == 7` compared a live
repository population to a numeral copied from the same tree.
`snapshots_consulted` is always `surveyed_snapshots()`, so the assertion measured
how many catalogs happen to be enrolled today against a number written down while
looking at that same list - DESIGN §5's change detector, green by construction and
"repaired" by editing the numeral the day a provider is added. Automating the
literal's update would collapse it to measure() == measure(), which the same
paragraph names as the tell.

What actually distinguishes this arm from its neighbour is a property of the
SNAPSHOTS rather than a count of them. The Absent arm claims every consulted
snapshot post-dates the observation; the Stale arm claims every snapshot it
reports pre-dates it. Both are now asserted against the same comparator the
resolver used to make the split, so a stale snapshot appearing in the Absent
arm - or a fresh one in the Stale arm - goes red at any roster size. The
complementary claim on the Stale arm is added in the same motion, because a
soundness claim on one side of a split says little without the other.

EVIDENCE. Witness green at exit 0 with the literal gone and both properties
asserted.

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

* Two catalogs answering for one label refuse rather than race

review 63221, and it is right. `first(matches)` silently took the head of the
match list, so a label two surveyed catalogs carried got whichever answer was
enrolled first. That is the same fail-open this module's own header argues
against, relocated from the label's spelling to the SURVEY'S ORDER: a genuine
disagreement about provider or architecture resolved silently in favour of a
line's position in a list nobody thinks of as ordered.

It is a live growth surface rather than a hypothetical, and the review names why:
gunbc.runner_provider_survey says in so many words that adding a provider is one
line in each list, and two already-enrolled catalogs - the larger-runner families
and the standard hosted labels - share one provider identity and one label
namespace. They are disjoint today and nothing structural keeps them so.

THE ARM REFUSES ON MULTIPLICITY, NOT ON DISAGREEMENT, and that is the deliberate
part. Refusing only when the rows contradict each other would widen on the
agreeing case, which is the same absorbing fallback one step quieter: two
authorities claiming one label is a single-authority defect whether or not they
agree this week, and tolerating agreeing duplicates would hide the fork until one
of them changed.

THE SPLIT IS OVER A MATCH LIST, NOT OVER THE LIVE SURVEY, so the wall has an
authorable red. resolve_from_matches takes the matches as an argument and
resolve_runner_label supplies them from the survey; a claim can hand the first
function two competing rows directly. A wall reachable only by corrupting the
enrolled catalogs would be a wall nothing could exercise.

FOUR DIRECTIONS ARE CLAIMED, not one: a disagreeing pair refuses, an AGREEING pair
refuses, reversing the pair's order refuses identically (which is the property
that says order stopped deciding), and a single match still resolves. Beside them
is a control over the LIVE survey asserting that no label in use today is carried
by two catalogs - so the refusal is a wall over a real corpus rather than one that
has already swallowed the ordinary case.

TWO EXECUTED REDS, and the second is the more useful finding. Relaxing the arm's
threshold takes the witness from exit 0 to exit 1. It did NOT the first time I ran
it, and the reason was a defect in my own roster: the two new claims had been
added to all_claims_hold as a separate statement rather than a conjunct, so their
value was computed and discarded and only the last expression was returned. A
claim enrolled in a roster that does not gate is precisely the inert-lens failure,
and it was invisible until the mutation refused to go red. Both claims are now
conjuncts and the red reproduces.

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

* A label is a value in one CI system's key: catalogs declare their selection surface

SOUNDNESS DEFECT, FOUND BY THE SIDE CHAT AND CONFIRMED BY EXECUTION, on a head that
already carried two approvals and nine review rounds.

THE RESOLVER SEARCHED EVERY ENROLLED CATALOG, and one of them is CircleCI — whose
rows are `resource_class` values written in .circleci/config.yml, not GitHub
Actions `runs-on` labels. Two ecosystems, two keys, and namespaces that overlap on
ordinary words. Measured on the previous head:

  resolve_runner_label("small")      -> NotArmConfirmed x86_64, from CircleCI
  resolve_runner_label("large")      -> NotArmConfirmed x86_64, from CircleCI
  resolve_runner_label("arm.medium") -> ArmConfirmed,           from CircleCI

The third is promotion 1 — an x64 label may not become Arm evidence — running in
REVERSE through the resolver written to prevent it: a GitHub Actions job on a
self-hosted runner named arm.medium reported as confirmed Arm, with full
provenance and a snapshot date attached. The first two are worse in practice,
because small and large are what an ordinary fleet actually calls its runners.

WHY NOTHING CAUGHT IT, WHICH IS THE PART WORTH KEEPING. Every unresolved arm in
this module answers a MISS. This is a HIT from the wrong ecosystem, so no
miss-shaped wall can see it. The ambiguity arm cannot fire either: exactly one
catalog carries "small", so there is no multiplicity to refuse. The guard and the
defect were disjoint — the same shape as a hermetic witness that cannot see a wet
decode, and the same shape as a claim green against a copy of the classifier it
tests. Two approvals did not catch it because no reviewer ran the resolver against
an ordinary word.

THE FIX IS CONSTRUCTION, NOT REMOVAL. RunnerLabelCatalog gains a SELECTION SURFACE
— the declaration defining the key its labels are written in — and the resolver
answers only for catalogs on the GitHub Actions runs-on surface. Dropping CircleCI
from the roster would have fixed this instance and left the class open for the next
non-GitHub system anyone enrolls, with nothing recording why it had to go. A
catalog that does not name the runs-on surface now cannot answer a runs-on
question, whoever adds it and whenever.

IT IS A DeclarationRef AND NOT A VARIANT, for the reason RunnerShapeRow.provider
already is: a central enum of surfaces would need widening by every CI system ever
enrolled, which is the concrete-product enumeration section 3 forbids a generic
hub. And the surface is declared ONCE, in extdeps.github.actions beside the
RunnerSpec that `runs-on` IS — my first cut of this fix declared it in five
provider modules, which was a fork introduced while repairing a fork.

CircleCI STAYS IN surveyed_label_catalogs, because this repository HAS read its
resource classes and a survey of what we surveyed should say so. It is excluded by
a FILTER on the question asked, not by deletion from the record.

EVIDENCE. witness_another_ci_systems_label_namespace_is_not_consulted asserts all
seven CircleCI spellings resolve undetermined in all three directions — not Arm,
not x64, undetermined. The red was executed: putting CircleCI back on the runs-on
surface takes the witness from exit 0 to exit 1, and restoring the surface returns
it to 0.

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

* Fold the real population, and tell a duplicated catalog from a duplicated roster

THREE FINDINGS FROM REVIEW, all confirmed. Two are the same defect wearing
different clothes: a claim whose denominator was chosen by a person rather than
computed from the corpus.

THE COLLISION WITNESS FOLDED TEN HAND-TYPED LABELS. That is the copied-population
defect: the sample was written while looking at the catalogs, so it passed by
construction, and it would have gone on passing when a provider was enrolled the
sample never named. It now folds runs_on_label_rows() — every row on the runs-on
surface — so the denominator is the corpus. A positive control lands beside it,
because a resolver that refused everything would satisfy "no collisions"
trivially: every surveyed row's own label must come back Resolved.

THE RED IS EXECUTED AND IT IS A REAL COLLISION, not a constructed pair: adding
depot-ubuntu-24.04-arm-16 to blacksmith's catalog takes BOTH claims from true to
false — the label is carried twice, so it stops resolving and starts refusing. The
old ten-label version would not have noticed, because blacksmith's rows were never
in its list.

THE AGREEING-AMBIGUITY RED NEVER TESTED TWO CATALOGS. Both competing matches were
built from one snapshot with no catalog identity, so the pair was indistinguishable
from ONE catalog listing a label twice. LabelMatch now carries catalog_provider,
and the multiplicity arm says WHICH defect it found: a label appearing twice in one
catalog is a defect in that provider's own projection and the repair belongs to
that module; a label claimed by two different catalogs is a defect in the roster
and the repair belongs to gunbc.runner_provider_survey. Different owners, different
repairs, and previously one undifferentiated cause.

AND THE CircleCI SURFACE WAS THE PROVIDER IDENTITY. circleci_resource_class_surface
pointed at circleci_catalog_authority, which is byte-for-byte the ref
circleci_provider_identity already uses — so "which key are these labels written
in" and "who publishes them" were one declaration, and a provider identity passed
where a surface was expected would have compared equal. That is the
interface/realization conflation section 3 names, one level above the defect this
axis was added to fix, introduced while fixing it.

GitHub's side names the declaration that IS the key (extdeps.github.actions
RunnerSpec). There is no CircleCI analogue in this repository — resource_class is
not modelled here at all — so the row now names ITSELF and says so, rather than
borrowing a neighbour and implying a modelled key exists. When resource_class is
modelled the ref moves to it. Not reachable today, since the filter only ever
compares against the GitHub surface; fixed because a knowingly-wrong ref that is
merely unreachable is still wrong.

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

* An unorderable snapshot is not an old one, and a type used must be a type imported

review 63545, two findings, both confirmed.

A SPELLING BOUND TO NOTHING, IN THE PR THAT DELETES A ROSTER ROW ABOUT EXACTLY
THAT. The witness used DeclarationRef while importing only declaration_ref_eq.
Every other real use in the corpus imports the type; the one grep hit that does
not is inside a comment. It is the class the floor has failed this branch for twice
tonight from main's side — grain_admits_single_cabinet, DurableOriginRead — and I
wrote one.

WHAT MAKES IT WORTH MORE THAN A ONE-LINE FIX: MY LOCAL RUNS CANNOT SEE IT. The
interpreter does not need the type to evaluate the function, so the witness ran
green at exit 0 with an unresolved name in it. Every "verified locally" I have
reported on this branch was verified by a path that structurally cannot catch this
class, and the declarations phase is the only thing that can. That is a gap in my
verification loop rather than a typo, and it is the third time this session that a
green has been green for a reason adjacent to the thing it claimed.

AND A FABRICATED CAUSE ON A FAILURE PATH. snapshot_is_stale_for mapped
Rfc3339OrderUndecidable to true, and the refusal then reported that the snapshot
was "fetched BEFORE the observation" — a fact that was never established, because
under that arm rfc3339_compare had explicitly REFUSED to order the two timestamps.
Routing undecidable toward re-fetch is the right policy and it is unchanged: when
the instrument cannot say, the arm that costs US effort is the honest one. What was
wrong was reporting a reason that is not true. Right destination, invented
justification.

The standing is now three-valued — SnapshotPredatesObservation,
SnapshotOrderUndecidable carrying rfc3339_compare's own cause, and
SnapshotPostdatesObservation — and the refusal COUNTS the two separately: how many
snapshots were fetched before the observation, and how many could not be ordered
against it at all. Both still route to re-fetch, so the policy the split preserves
is asserted in the claim rather than left to be inferred.

EVIDENCE. The claim drives the exact pair the RFC's section 5.1 preconditions
exclude — a fractional-second stamp against a whole-second one — and asserts four
things: the undecidable one is named undecidable, the plainly older one is named
older, BOTH still route to re-fetch, and only one of them is undecidable. The red
was executed: mapping the undecidable arm back to SnapshotPredatesObservation takes
it from true to false.

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

* Carry the standing on the arm and compute it once; I fixed the sentence and left the carrier fused

review 63580, both findings confirmed, and both are mine from the commit that was
supposed to fix this exact thing.

I SPLIT THE TYPE AND THEN THREW THE SPLIT AWAY. The module argues in its own
annotation that the two reasons a snapshot is not trusted "are not the same fact"
and "may not share a sentence" — and then the arm stored
List<CatalogSnapshot>, so the distinction survived ONLY in the cause prose. A
consumer matching on the value could not act on the thing the type was created to
preserve; a human reading English could. That is section 4c read backwards: a count
living in a String. I repaired the sentence, declared the carrier three-valued, and
left the carrier fused — a fix that addressed the symptom I had just written about
while reproducing its cause one field over.

RunnerLabelSnapshotStale now carries List<SnapshotAssessment>, each pairing a
snapshot with its standing, and the cause text is a PROJECTION of that list rather
than the only record of it.

AND THE STANDING WAS RE-DERIVED THREE TIMES PER SNAPSHOT. stale_snapshots_for
computed it to filter, then the two count(filter(...)) calls in the message
computed it again for every snapshot in the survey — so rfc3339_compare ran three
times per row where once was needed, with unmatched_resolution as the least common
ancestor of all three demands. Section 2: when several demands share an ancestor,
the repetition is authored duplication, and the remedy is to carry the first value
rather than to cache the recomputation. assess_snapshots computes one assessment
per snapshot and everything downstream folds that list.

The two Bool predicates over the coproduct are gone with it: assessment_is_untrusted
and assessment_is_undecidable read a standing already computed instead of
collapsing a three-arm type back to a Bool by recomputing it.

EVIDENCE. The new claim partitions the arm's OWN payload and asserts the partition
is total — every untrusted snapshot is either pre-dating or unorderable, the counts
sum to the whole, and today's live survey is entirely the pre-dating kind. That
last conjunct is the reading a consumer actually wants, because it says the remedy
is "re-fetch four stale catalogs" rather than "our timestamps are unreadable", and
it is derived from the value rather than parsed out of a sentence. Witness green at
exit 0; mapping the undecidable arm back to SnapshotPredatesObservation takes it to
exit 1.

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

* Key a match on the catalog it came from, not on who published its rows

review 63609, and it clears the soundness bar I set in this PR's freeze notice, so
the head moves and the approvals reset. It is a confident wrong answer on a failure
path: the refusal would have stated a false fact and sent the reader to the wrong
module to repair it.

WHAT WAS WRONG. LabelMatch carried catalog_provider and matches_share_one_catalog
compared providers, so "one catalog lists this label twice" and "two catalogs both
claim it" were decided by who PUBLISHED the rows rather than by which catalog
matched. Those are different defects with different owners: the first belongs to
the module that projected the rows, the second to the roster that enrolled them.

IT IS NOT HYPOTHETICAL AND THE MODULE ITSELF NAMES THE PAIR. GitHub's sized
larger-runner catalog and its standard-runner catalog BOTH carry
github_actions_provider_identity - they are two readings of two different published
references by one vendor, and the module's own annotation calls them the live
growth surface. An overlap between them would still have refused, but the cause
would have read "this label appears twice in ONE catalog's rows... the repair
belongs to that module" when the duplication was in the survey. Right refusal,
false explanation, wrong module.

RunnerLabelCatalog now carries its own identity - a DeclarationRef naming the
catalog declaration - distinct from the provider naming who published it. A
provider can have several catalogs in one survey and now that is representable.
LabelMatch keys on the catalog, and RunnerLabelAmbiguousAcrossCatalogs carries
List<LabelMatch> rather than List<RunnerLabelRow>, because bare rows cannot recover
which catalog matched and a consumer reading the arm needs exactly that.

WHY MY EXISTING CLAIM COULD NOT SEE IT: both competing matches went through
control_match, which set the same provider, so the pair never exercised two
catalogs at all - let alone two that share a provider. Guard and defect disjoint,
again, and this is the third time in this module that the carrier was keyed on a
neighbouring fact while the annotation argued for the distinction.

EVIDENCE, in both directions so the two causes are not interchangeable. Two
catalogs sharing GitHub as provider now read as two catalogs and the cause names
the ROSTER; one catalog listing a label twice names THAT CATALOG and its module.
The red was executed: keying matches_share_one_catalog back on row.provider takes
the shared-provider claim from true to false.

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

* The seam checks its own inputs, and a lowercase separator reverses chronology

Two more soundness findings from the side chat, both unfreezing the head.

THE PUBLIC SEAM WAS A DOOR BESIDE THE WALL. resolve_from_matches is split out
precisely so a claim can hand it constructed matches - which means ANY caller can,
and the surface filter lived only in surveyed_matches. So the path that was already
safe was guarded and the path a caller reaches was not: a bare CircleCI row handed
straight to the seam resolved happily as a runs-on label. LabelMatch now carries
its selection surface and the seam refuses a match from any other one, so the wall
holds for a constructed call exactly as it does for the survey.

AND RFC 3339 PERMITS LOWERCASE, WHICH REVERSES LEXICAL ORDER. The grammar's own
note allows "t" and "z" in place of "T" and "Z", so 2026-09-04t16:04:06Z and
2026-09-04T16:04:06Z are the same instant spelled two admissible ways - and 't' is
code point 0x74 against 'T' at 0x54, so lexical comparison puts the lowercase one
AFTER every uppercase one whatever its date. An OLDER stamp compares as NEWER.

That is not imprecision, it is a reversal, and it lands exactly where this branch
cares: a snapshot that pre-dates an observation would read as post-dating it, which
flips our own coverage obligation into a finding about somebody else's repository -
the confusion the three-valued standing was built to prevent, reintroduced
underneath it by the comparator that standing is derived from.

Section 5.1's precondition is "expressed using the same string", and case is part
of the string. The comparator now requires the canonical uppercase spelling of both
designators and refuses anything else, including an internally-consistent lowercase
pair, because admitting that would mean admitting the mixed pair.

EVIDENCE. A lowercase separator against an uppercase one refuses as undecidable;
the same two instants in canonical spelling still order correctly, so the refusal
is not blanket. A CircleCI row handed to the seam is refused naming the surface it
came from.

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

* A caller category error is not a roster defect: give the wrong surface its own arm

review 63694, and it is the FOURTH time in this module that a carrier fused two
facts while an annotation argued for the distinction. I added the surface check one
commit ago and reported the refusal through RunnerLabelAmbiguousAcrossCatalogs,
whose declared meaning is "two surveyed catalogs both carry this label".

THEY ARE DIFFERENT FACTS WITH DIFFERENT OWNERS. A wrong-surface match means a
caller asked a resource_class value as a runs-on question - the repair is at the
CALL SITE. Ambiguity means the roster enrolled one label twice - the repair is in
gunbc.runner_provider_survey. Reported through one arm, nothing on the value
separated them and the English cause was the only discriminator.

MY OWN WITNESS PROVED IT, which is the part worth keeping. The claim I wrote to
check the seam had to assert string_contains(cause, "does not answer for") to tell
the two refusals apart - a claim reaching into prose because the value would not
answer. I wrote that claim, ran it, watched it pass, and did not notice that its
SHAPE was the evidence of the defect. The same module says three declarations
later, about the snapshot standing, that "the distinction survived in the English
and nowhere a consumer could match on it."

RunnerLabelWrongSelectionSurface is now its own arm. The seam claim matches on it
by variant and the ambiguity claim matches on the other, so the two are separated
by value and neither reads a sentence.

WHAT I WOULD FLAG ABOUT THE PATTERN: four instances, one module, all mine, and each
introduced while repairing the previous one. Snapshot standing split three ways and
stored as bare snapshots. Selection surface pointed at the provider anchor. Match
keyed on provider rather than catalog. Now a new refusal reusing an existing arm. I
said last round I would grep my own diffs for "the annotation argues for a
distinction the type does not carry" and then did not, because I was adding a check
rather than a type and did not think the rule applied. It applies to the REFUSAL as
much as to the carrier: a new way to fail is a new fact, and reaching for an
existing arm is the same reach as reusing a neighbouring key.

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

* Three ways to refuse a multiplicity have three owners: give each its own name

review 63714, the FIFTH instance of this shape in this module, and this time the
arm was the one I wrote the criterion about. Two commits ago I split
RunnerLabelWrongSelectionSurface off ambiguity BECAUSE the two had different owners
and different repairs. RunnerLabelAmbiguousAcrossCatalogs was already fusing two
facts by the same test, one line away, and I did not look.

THE THREE FACTS AND THEIR THREE OWNERS. A label appearing twice in ONE catalog is a
defect in that provider module's projection of its own published surface. A label
claimed by TWO catalogs is a defect in gunbc.runner_provider_survey's roster. A
match on another CI system's surface is neither - a caller asked a resource_class
value as a runs-on question and the repair is at the call site. The name
AcrossCatalogs was simply FALSE for the same-catalog case.

RunnerLabelDuplicatedWithinCatalog and RunnerLabelClaimedByTwoCatalogs now carry
their own names, and every witness matches on the VARIANT. The file has zero
string_contains on a cause left in it - the claims had been reading English to tell
two refusals apart, which is the tell, and which I had described in my own commit
message one commit earlier while leaving four instances of it in the same file.

EVIDENCE, AND THE RED IS PRECISE RATHER THAN MERELY PRESENT: collapsing the split
so both multiplicities report as cross-catalog takes the same-catalog claim from
true to false and leaves the cross-catalog claim GREEN. A pair of claims that both
went red would not have shown they test different things.

FIVE INSTANCES, ONE MODULE, ALL MINE, EACH INTRODUCED WHILE REPAIRING THE LAST.
Snapshot standing split three ways and stored as bare snapshots; selection surface
pointed at the provider anchor; match keyed on provider not catalog; a new refusal
reusing an existing arm; and now the arm that refusal was split off FROM. The
mechanical check I keep failing to run is cheap and I am stating it so the next
reader can hold me to it: after any change to a coproduct, grep the witnesses for
string_contains on a cause. Every hit is a place the value does not carry what the
prose claims.

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

---------

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot pushed a commit that referenced this pull request Sep 11, 2026
… from its own blob

The freeze is lifted by the trigger review named for it -- a CONCRETE CONFLICT, not elapsed commits.
This branch sat at 265a92d through 9, 13 and 28 commits of drift without merging, because
absorbing main on a schedule buys nothing while nobody can execute the missing acceptance receipt
and every absorption moves the subject SHA. GitHub reported the branch unmergeable at 55 behind, so
the condition is met and the merge happens now.

FIFTH CONFLICT IN THIS FILE, AND THE FIRST QUALITATIVELY DIFFERENT ONE. Both sides appended rows, so
git interleaved the two arrays and produced THREE hunks across one list: 40 SCM rows here, 3 for
gunbc#11071 from main. Patching interleaved hunks is exactly how a row gets silently dropped in the
middle of a list nobody re-counts, and a dropped row here is an unadjudicated delta the wall exists
to refuse. So the resolution does not touch the hunks at all: each side's array is reconstructed
from its OWN staged blob (`git show :2:` and `git show :3:`) and the two are concatenated.

UNION, for the reason that decided the second and fourth conflicts: taking either side whole deletes
obligations the other still owes. 43 rows, verified by label census -- 31 SCM_MERGE_BASE_COHOME, 9
SCM_SOURCE_RECOVERY_REHOME, 3 gunbc#11071 -- rather than by trusting the patch applied cleanly.

Main's #11071 TRIGGER paragraph is kept verbatim. It records when those rows come due and this
branch is not the authority that retires them; the same receipt rule that deleted #10945 and #10956
from this roster will delete these when the wall says so, and not before.

cargo check -p v1-compiler --lib finished clean on the working tree.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9
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