One accepted fleet revision from two exact positive facts by briansrls · Pull Request #8725 · gunb-ai/gunbc

briansrls · 2026-08-21T04:39:24Z

Stacked on #8720 → #8701 (base is fleet/admission-consumes-expectation, so this diff is one commit). Retarget as the stack lands.

Two propositions, two producers

The desired ref must never move onto a revision whose floor did not run — and the failure that matters is not a red floor. A red floor is loud and refuses. It is a green floor belonging to something else: a PR's merge-subject run, a fork's branch, a different workflow in the same repo, a run that was cancelled rather than concluded. Each produces a perfectly truthful "a workflow run succeeded", and none proves what the fleet needs proved.

proposition	producer	proved by
`RequiredCiSucceeded` — the Required CI contract completed successfully for revision R	`accept_required_ci_workflow_run`	workflow path, repository, head repository, activity, conclusion, head SHA decodes
`DefaultBranchRevisionObserved` — revision R entered the default branch	`observe_default_branch_revision`	repository, head repository, originating event, head branch, head SHA decodes

Neither implies the other, so folding them into one predicate would let either stand in for the pair.

A PR's merge-subject run can produce the first and cannot produce the second. The floor genuinely ran and genuinely passed on that tree — refusing it as a CI failure would be a lie about a real result. What it cannot prove is that the revision entered the default branch. That asymmetry is what stops the fleet following a revision main never had, and it is only expressible because the two are apart.

The SCM fact is named for what the event can prove

A workflow_run envelope carries the head branch and the originating event. It does not distinguish a PR merge from a direct fast-forward push, an authorized emergency push, or any other mechanism that moved the branch. So the carrier is DefaultBranchRevisionObserved, not MergedMainRevisionObserved — naming it for merges because merges are the ordinary producer would assert provenance nothing observed. A policy that genuinely requires merge origin needs a separate merge authority, and will find this carrier honestly insufficient rather than quietly sufficient-looking.

Three smaller walls

The revision is decoded once. GitHub says head_sha is a SHA; nothing on the wire establishes it. Both producers decode through git_object_id_from_untagged_hex and refuse an undecodable value before any positive carrier exists. One canonical GitObjectId is carried — not an authored CommitSha beside it, which would be two writable names for one fact that could disagree.

Evidence is a type parameter, not a variant. GitHub is the first provider of both propositions and will not be the last; an accepted fabric receipt proves the same Required CI proposition through a different channel. GitHub | Fabric inside the positive carrier would make every consumer branch on a provenance it has no business branching on, and make adding a provider an edit to the admission carrier.

No phase roster. RequiredCiSucceeded carries RequiredCiContractIdentity, derived from the artifact authority that emits the workflow. The fleet asks whether the exact contract succeeded for the exact revision; it does not own the contract's internal phase roster. A phases_run == 6 field would make every phase added to the floor a breaking change to fleet admission.

The join

The sole join takes the two positive carriers, not the two admissions — so a refused producer cannot reach it at all; the caller must have matched out a success on both sides before it can even ask. Downstream only AcceptedFleetRevision.revision exists: no candidate remains beside it to compare against or accidentally substitute.

The mismatch arm is load-bearing. Required CI proving revision A while the branch carries revision B is not a contradiction in the data — both facts can be perfectly true, about different revisions, and they arrive together whenever a push lands while a run is in flight. What is false is the conjunction anyone would infer from holding both. It refuses carrying both revisions, because "which two" is the entire content of the finding.

Evidence

9/9 witnesses green. Two mutation controls, each discriminating exactly one row:

MUT-1 — the default-branch producer stops checking the originating event:

an_eligible_trunk_push_satisfies_both_propositions_and_the_join_accepts   true
a_pull_request_run_proves_required_ci_but_not_the_default_branch         FALSE
a_push_to_a_topic_branch_is_refused_by_the_branch_fact                    true
required_ci_for_one_revision_and_a_branch_at_another_refuses_naming_both  true

MUT-2 — the join stops comparing the two revisions:

an_eligible_trunk_push_satisfies_both_propositions_and_the_join_accepts   true
a_pull_request_run_proves_required_ci_but_not_the_default_branch          true
required_ci_for_one_revision_and_a_branch_at_another_refuses_naming_both FALSE
an_undecodable_head_sha_refuses_on_both_producers                         true

Restored byte-identical after each arm. The positive control is deliberate and load-bearing: almost every other row asserts a refusal, and a pair of producers that refused unconditionally would satisfy all of them. It is the only row that fails when a wall is too strict — which is the failure mode a wall-shaped change actually has, and it is silent in production, because a too-strict wall just stops the fleet advancing with nothing red anywhere.

Not in this cut

Forward-only motion, and it is not implied by anything already landed. A CAS makes the write atomic, not monotone: a valid lease against a correctly observed prior will move the ref backwards to an older revision without complaint. Ancestry, the superseded-result no-op, and unverifiable-ancestry refusal come next, over the existing gunbc.live_deploy.revision DeployRevisionRelation authority — which already distinguishes the five relations and already treats a late superseded result as terminal success rather than operational failure.

No actuator consumes AcceptedFleetRevision yet, so nothing can advance on it in the meantime. The transport binder (push_remote_ref_compare_and_swap) stays out until it lands with its first real consumer, per the boundary #8697 declared — adding it here just to census its callers would be another unconsumed capability.

— sent from silent-bear-842

The desired ref must never move onto a revision whose floor did not run, and the failure that matters is not a red floor -- a red floor is loud and refuses. It is a GREEN floor belonging to SOMETHING ELSE: a PR's merge-subject run, a fork's branch, a different workflow in the same repository, a run that was cancelled rather than concluded. Each produces a truthful "a workflow run succeeded", and none proves what the fleet needs proved. TWO PROPOSITIONS, TWO PRODUCERS, and the split is the point: RequiredCiSucceeded the Required CI contract completed successfully for revision R DefaultBranchRevisionObserved revision R entered the default branch Neither implies the other and they are proved by different facts, so folding them into one predicate would let either stand in for the pair. A PR's merge-subject run CAN produce the first -- the floor genuinely ran and genuinely passed on that tree, and refusing it as a CI failure would be a lie about a real result -- and it CANNOT produce the second. That asymmetry is what stops the fleet following a revision main never had, and it is only expressible because the two are apart. THE SCM FACT IS NAMED FOR WHAT THE EVENT CAN PROVE. A workflow_run envelope carries the head branch and the originating event; it does not distinguish a PR merge from a direct fast-forward push, an authorized emergency push, or any other mechanism that moved the branch. So the carrier is DefaultBranchRevisionObserved, not MergedMainRevisionObserved: naming it for merges because merges are the ordinary producer would assert provenance nothing observed. THE REVISION IS DECODED ONCE. GitHub says head_sha is a SHA; nothing on the wire establishes it. Both producers decode through git_object_id_from_untagged_hex and refuse an undecodable value BEFORE any positive carrier exists, so no consumer can be handed a revision that is not one. One canonical GitObjectId is carried, never an authored CommitSha beside it -- two writable names for one fact could disagree. EVIDENCE IS A TYPE PARAMETER, NOT A VARIANT. GitHub is the first provider of both propositions and will not be the last; an accepted fabric receipt proves the same Required CI proposition through a different channel. `GitHub | Fabric` inside the positive carrier would make every consumer branch on a provenance it has no business branching on, and make adding a provider an edit to the admission carrier. NO PHASE ROSTER. RequiredCiSucceeded carries RequiredCiContractIdentity, derived from the artifact authority that emits the workflow. The fleet asks whether the exact contract succeeded for the exact revision; it does not own the contract's internal phase roster, and a `phases_run == 6` field would make every phase added to the floor a breaking change to fleet admission. The sole join produces AcceptedFleetRevision, and downstream only its .revision exists -- no candidate remains beside it to compare or accidentally substitute. The mismatch arm is load-bearing: Required CI proving A while the branch carries B is not a contradiction in the data (both facts true, different revisions, arriving together whenever a push lands mid-run); what is false is the CONJUNCTION anyone would infer from holding both. It refuses carrying both revisions, because "which two" is the entire content of the finding. 9/9 witnesses green. NOT IN THIS CUT, and named so it is not read as further along than it is: forward-only motion. A CAS makes the write ATOMIC, not MONOTONE -- a valid lease against a correctly observed prior will move the ref backwards to an older revision without complaint. Ancestry, the superseded-result no-op, and unverifiable-ancestry refusal come next, over the existing DeployRevisionRelation authority. No actuator consumes AcceptedFleetRevision yet, so nothing can advance on it in the meantime. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf

…ed-revision-two-facts

…gain This module carried `fleet_repository_full_name = "gunb-ai/gunbc"` and `fleet_default_branch = "main"` as data rows. Both are the sixth and seventh nicknames for facts that already have authorities. gunbc.repository exists precisely because five spellings of this repository's identity had accumulated across the tree, and its own note answers this case directly: the answer to five nicknames is not a sixth. gunbc.repo_identity owns the default-branch name and carries a perturbation oracle that moves every consumer when it changes -- a literal here is INVISIBLE to that oracle, which is what keeps this class hidden. Every individual literal looks obviously correct. Review flagged these as policy config that could later be lifted. It was not a later problem: the authorities already existed and this module simply was not reading them. OBSERVED WHILE DOING IT, and flagged rather than silently resolved: gunbc_repository ALSO carries a default_branch field, so the default branch appears to have two homes. They agree today. The branch reads from gunbc.repo_identity here because that module's note claims authority for branch facts explicitly and carries the oracle, while Repository.default_branch is part of the upstream API shape this project instantiates. Whether those should be one row is a real question and not this cut's to settle. 4/4 witnesses green; gunbc compile reports 0 blocking. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf

…ority, and close a trigger-grain fail-open THE PORT. gunbc.fleet_desired_admission consumed its own copy of workflow identity, trust checks, a floor_green Bool, candidate decoding and the old advance gate. #8720 and #8725 replaced all of it. This deletes those routes at the root rather than wrapping them: fleet_desired_admission_event_trusted, fleet_desired_floor_green, the old decide and the old push renderer are gone, and the live orchestration is now event -> fleet_desired_accepted_from_event (two producers, one join) -> fleet_desired_advance_input_wet (the only effectful step) -> decide_fleet_desired_advance -> fleet_desired_action_from_decision -> one rendered action fleet_desired_advance_input_wet does NOT re-classify the observed ref. It routes the already-classified result of fleet_desired_advance_expectation, so "absent vs unreadable vs unobserved" keeps one authority, and only the observed-current arm reaches git -- an event that produced no accepted revision can never trigger an ancestry probe. THE ACTION SUM. A successful decision no longer implies a push. Two of the three authorized actions mutate nothing (already-converged, superseded), and both render a NONEMPTY script by the renderer's shape rather than by an author remembering to echo. That is load-bearing: the executing step's `test -s` is the wall separating "authorization produced nothing" -- a writer or transport failure -- from "authorization said do nothing". If a no-op could render empty those two states would collide at the only place that can still tell them apart, and a dropped authorization would read as a converged fleet. Two witnesses pin it, plus one asserting no no-op contains `git push`. Names renamed to authorized_action end to end, including the emitted yml and the step title, so the human surface stops claiming every positive action is a push. THE FAIL-OPEN, found by nimble-fox-671 against origin/main and handed over rather than edited in parallel. The workflow_run trigger named no branches, so EVERY branch's floor completion created a run that entered the single constant concurrency group and only then skipped on the job-level head_branch condition. In the default group an arriving entry cancels the pending one, so a pull request's floor completing could evict a pending admission for a green main revision and do nothing in its place -- no advance, no refusal, no diagnostic, and a `cancelled` run indistinguishable from noise. Observed tally over 131 runs: 77 skipped, 45 cancelled, 6 failure, 3 success. Fixed at the trigger grain, not the concurrency grain. WorkflowRunCompleted gains a REQUIRED branches member emitted unconditionally like its Push and PullRequest siblings, so a caller cannot declare this trigger without deciding which branches it answers to. Documented semantics confirmed before emitting: `branches` on workflow_run filters on the branch of the TRIGGERING run, the same fact the job-level condition tests, one grain earlier. Widening the queue instead (ConcurrencyMappingQueueMax) would have stopped the eviction and left the cause, trading a silent drop for up to a hundred no-op entries stalled ahead of a real admission on a single-concurrency runner. The job-level condition and the in-model trust checks stay; the filter is defence in depth. The concurrency annotation's existing argument -- that losing a superseded pending admission is preferable to walking the fleet through revisions it has passed -- was SOUND. Its unstated premise, that every entry in the group is an admission, was false, and the falsifying fact lived three declarations away in the trigger. With the filter in place that argument is true as written for the first time, so the variant stays and the annotation now records why it was only accidentally right before. SCAFFOLD PREMISE CORRECTED. The dissolution row claimed no typed compare-and-swap carrier existed. #8697 falsified that. PushRefUpdateWithLease IS the typed wire capability; what is missing is the sole request-to-wire binder, a cited decoder for git's push-rejection output separating a stale lease from a failed push, and an independent remote readback. Moving to the typed row today would trade an honestly-untyped shell for a typed call whose refusal semantics this gate cannot read, so the shell survives with an honest premise instead of a false one. Stale citations of the deleted admit_fleet_desired_advance repointed at decide_fleet_desired_advance in three modules. EVIDENCE: all 17 witness rows run green by execution, individually, not by typecheck. The branch-filter row was run as a discriminating pair -- green with the filter, red with branches emptied, restore verified by diffstat. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf

gunbai-bot · 2026-08-21T20:55:50Z

Closing as superseded by #8733, not abandoned — every commit on this branch is contained in #8733, verified with `git merge-base --is-ancestor` rather than inferred from the diff.

This PR was based on #8720, which is based on main. That stack made sense while the three lanes were being reviewed separately; it stopped making sense once the later branch absorbed the earlier ones. Two concrete costs it was imposing:

witnesses.yml filters pull_request: branches: [main], so neither this PR nor Forward-only desired-ref admission: make the modelled wall the only route, and stop the queue dropping green advances #8733 was ever eligible for a CI run while stacked. That is why they sat with no checks.
MERGEABLE was true only against a stale base. Retargeting Forward-only desired-ref admission: make the modelled wall the only route, and stop the queue dropping green advances #8733 to main immediately turned it CONFLICTING — it had never actually been merged with main, and the stack was hiding that.

Retargeting this one to main instead of closing it would leave a PR proposing a strict subset of #8733 (which carries 81 commits beyond this branch), so the two would have to be reviewed and merged in lockstep for no benefit.

The accepted-revision two-fact join this PR introduced is live in #8733 — AcceptedFleetRevision with required_ci_evidence and default_branch_evidence, and the admission consumer ported onto it. Nothing here is dropped.

— sent from silent-bear-842

…oute, and stop the queue dropping green advances (#8733) * Shape git-update-ref's compare-and-swap form, so the unconditional write is unspellable `git update-ref <ref> <new> <old>` refuses unless the ref currently holds <old>. The two-argument form overwrites unconditionally. The difference between a compare-and-swap and a blind write is ONE ABSENT LIST ELEMENT, and nothing downstream can recover it: by the time the process runs, an argv missing its third word IS the unconditional write. So expected_old is a required GitObjectId? rendered inside the shape, never caller-supplied text, and creation is the same operation with an empty <old> emitted as a PRESENT argument -- git's documented spelling for "must not already exist". A caller holding `none` cannot degrade it into "no third argument", and cannot spell the unconditional form at all. PLACEMENT was forced. git.dag owns the shape_git_*_argv family, but object_store.dag already imports git.dag, so a GitObjectId-typed shape in git.dag would be an import cycle. object_store is the right home independently: git_update_ref_authority (citing git-scm.com/docs/git-update-ref), GitObjectId, GitRefName and git_object_id_wire_hex are all already there. This shapes an argv and observes nothing, per the module's own git_modeled_ref_transition_boundary_note: a transition is Applied only on an executing transport's observation, never on having produced the right command. EVIDENCE, by execution: 4 witnesses true MUT-A drop the prior word (the two-arg fail-open) all 4 assertion rows red MUT-B new oid in the prior slot (a CAS that can never fire, six words, right verb and ref) 3 rows red, arity row correctly blind object_store.dag restored byte-identical after each arm A FIFTH ROW WAS DELETED ON THAT MEASUREMENT. It asserted "a creation and an advance do not render identically", justified as catching a shape that ignored expected_old and emitted a constant. That justification is false: the advance row and the creation row demand DIFFERENT values in the SAME position (the prior oid, and ""), so together they already forbid any constant there. MUT-B reds all three, so the fifth row added no reach and restated a consequence of the two above it. The mutation designed to prove it necessary is what proved it redundant. The fixture carries its own decode control: git_sha1_object_id returns an option, so a hex typo yields none, the argv helper returns [], and every arity and absence assertion would be satisfied by the empty list -- green for the one reason that proves nothing. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * Give git.PublicationTransport a compare-and-swap ref advance PushRefUpdate's argv is `git push {remote} {refspec}`, which refuses only non-fast-forwards -- a weaker and DIFFERENT guarantee than naming the prior. Two advances racing on one ref are both fast-forwards, so both succeed and the later silently discards the earlier's decision. --force-with-lease=<ref>:<expect> refuses unless the remote ref still holds <expect>, which is what makes the loser of a race refuse instead of overwrite. WHY THE EXPECTATION IS A CLOSED SUM AND NOT GitObjectId?. On an option, `none` is one value doing two jobs, and the second job it silently acquires is "I could not observe the ref" -- which must never render as "therefore create it". RemoteRefMustBeAbsent is a positive claim about the remote; an unobserved remote is not that claim. gunbc.fleet_desired_observe conflates exactly this today (an unadvertised ref and a transport failure both return FleetDesiredUnobserved), so the sum is what stops that conflation reaching an actuation. ONE OPERATION, NOT TWO. RecordCommit/RecordEmptyCommit split because a shell argv template cannot branch on a Bool. Here the branch is over a closed sum whose arms differ in one rendered word, so collapsing it in a pure function keeps one operation and one literal template. CreateRemoteRefIfAbsent / UpdateRemoteRefIfCurrent would fork one upstream operation into two rows git does not distinguish. EVIDENCE, by execution: 4 witnesses true MUT-1 lease ignores the expectation (constant empty) advance row red ONLY MUT-2 refspec folds the expectation in (advance pushes the prior object, lease still correct) refspec row red ONLY publication_transport.dag restored byte-identical after each arm Each mutation is caught by exactly one row and each row catches exactly the defect it claims. MUT-2 is the reason the refspec row asserts INDEPENDENCE from the expectation rather than checking one case: the lease is correct, the arity is correct, the push succeeds, and the ref advances to where it already was. TWO EARLIER ATTEMPTS ARE NOT IN THIS DIFF. The first shaped `git update-ref`, which moves a LOCAL ref -- but refs/fleet/desired is observed through `git ls-remote origin`, so the local form fails by SUCCEEDING: exit 0, a local ref moves, every observer sees no change. The second put a --force-with-lease argv in extdeps.git.object_store as a free function, which is the parallel argv surface publication_transport's own header forbids: "shell argv lives only in git.PublicationTransport service transport rows -- no parallel free-fn argv surface". object_store.dag is restored byte-identical to main. NOT IN SCOPE, and both are blockers for the consumer rather than for this shape: admit_fleet_desired_advance takes floor_green: Bool, which binds greenness to no revision at all; and fleet_desired_observe has no ObservedAbsent arm, so nothing can yet produce RemoteRefMustBeAbsent honestly. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * Stop claiming PushRefUpdateWithLease separates a refused lease from a failed push The comment above the operation said a refused lease "must not be collapsed into the generic nonzero arm", and four lines below it the exit block reads `nonzero => String "Leased push refused or failed"` -- collapsing exactly that. The warning was written and the thing it warns against implemented in one block (raised in review 54192). NOT FIXED BY FAKING THE DISTINCTION. git reports both a stale-lease refusal and a transport failure as exit 1; the discriminating evidence is the "(stale info)" / "[rejected]" text on stderr. Deciding an outcome by matching upstream human-readable output is its own modeling job with its own cited authority, and guessing at it inside this row would fabricate a distinction rather than ground one -- worse than not carrying it. So the comment now states the boundary and declares its rung: mitigatable, with exit_code and stderr both retained as output fields so a caller CAN recover the distinction, and the next trigger named (the first consumer that must retry on a stale prior, which needs a cited decoder for git's push-rejection output). The old sentence is corrected in place rather than deleted, because a consumer reading only the warning would have believed the transport separated them, and that belief is the hazard. The distinction is real for the eventual consumer: a refused lease is an ANSWER -- the remote moved, re-observe and retry -- while a transport failure is the ABSENCE of an answer, whose remedy is not retrying with a fresh prior. Treating the second as the first would loop. Comment-only; the three assertion witnesses return true unchanged. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * Hoist the PushRefUpdateWithLease annotation to module grain CI refused publication_transport.dag:127-134 with "source annotation names no subject". The rationale block sat INSIDE the service body, above the operation it describes -- and an operation is not a module item, so every line of it refused (DESIGN section 4c: annotations attach to module-scope declarations only). Hoisted above the `service` declaration, which is where the existing RecordCommit/RecordEmptyCommit note already sits. Zero comments remain inside the service body. HOW IT GOT THERE, since the module was correct when first written: the original annotation WAS at module grain. Correcting the lease-refusal claim for review 54192 rewrote it in place, next to the operation it describes, because that is where a reader wants it. Fixing a truthfulness defect introduced a structural one. The section 4c rule and the instinct to put an explanation beside its subject pull in opposite directions, and the rule wins. WHY LOCAL RUNS DID NOT CATCH IT: all four witnesses returned true under `gunbc run --entry` before the push. An entry-scoped run resolves a narrow module set and does not apply the annotation admission the CI path does, so a file that is structurally inadmissible passes cleanly. Local green under --entry is not evidence of CI-path validity -- including for every mutation control in this branch, which proves the logic discriminates and says nothing about admissibility. Witnesses unchanged and still true; the edit moved a comment. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * Remove the observer-split increment that git add -A swept into this PR fecf00f28e was meant to hoist one annotation to module grain. It ran `git add -A` while the NEXT increment's uncommitted work was still in the worktree -- the FleetDesiredRevision split, the observer arms, the observation-to-expectation seam and its witness file -- so this PR silently grew from 2 files to 5, after three reviews had already approved it at the smaller scope. Restored to the two files this PR is about. The swept work is preserved as a patch and lands on its own branch, where it can be reviewed as what it is: a change to a type that four consumers match on. HOW IT HAPPENED, because the mechanism matters more than the mistake: the second increment was built on a branch created off this one, then a CI alert arrived and I checked this branch back out to fix it. Git carries uncommitted changes across a checkout when they do not conflict, so the next increment's edits followed me here and `git add -A` could not tell them apart from the fix. Two habits would each have caught it independently: staging by path rather than -A, and reading `git show --stat` before pushing rather than after. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * Split FleetDesiredRevision so an absent ref is a claim, not a failure to look ls-remote distinguishes three situations that this type collapsed into one FleetDesiredUnobserved with a cause STRING: a ref origin does not advertise, an advertisement that will not decode, and a transport that refused. The string told a human which had happened and told a consumer nothing, so the only safe reading was "no target" -- and the first creation of refs/fleet/desired was inexpressible, because nothing could say "the remote does not have this ref" as a claim rather than as a failure to look. FleetDesiredAdmitted the ref is at a decodable oid -> advance FROM it FleetDesiredAbsent origin advertises no such ref -> create it, ONLY here FleetDesiredUndecodable the ref exists and is garbage -> alarm; never write FleetDesiredUnobserved no answer at all -> refuse; claim nothing Undecodable is not folded into Unobserved even though both refuse a write, because their remedies differ: an undecodable advertisement means the ref EXISTS holding something unreadable, which a retry will not fix and a write would destroy; an unobserved ref means we failed to ask. Merging them lets a corrupt ref be retried forever as if it were a network fault. fleet_desired_advance_expectation is the seam, and its refusal arms are the load-bearing half. Rendering "I could not read the ref" as RemoteRefMustBeAbsent turns a network fault into a ref CREATION; rendering it as RemoteRefMustEqual needs an oid nobody observed. Both are the empty-observation narrow pointed at an actuator, so it yields nothing and the caller stops. This is what makes RemoteRefMustBeAbsent -- added in #8697 -- producible at all. Two of the five witnesses could not have been written against the old type. The compiler ran the census: splitting the sum made every exhaustive match refuse until given the new arms, including one inside fleet_desired_observe that a name-grep would not have surfaced as a consumer. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * Name the refusal that cannot license a write, instead of collapsing it An advance expectation is a claim about the ref's current state, and only two observations are such a claim: "the ref is at X" (lease that oid) and "origin advertises no such ref" (lease empty). The other two -- ls-remote refused, and the advertisement did not decode -- are absences of observation, and rendering either as a licence is the empty-observation narrow pointed at an actuator. The refusal arm previously carried one cause, so an undecodable advertisement was reported as an unobserved transport. That is a real loss: the two have opposite remedies (retry the network vs. read the bytes someone actually sent), and the undecodable line -- the only evidence of what went wrong -- was dropped. FleetDesiredExpectationRefusal splits them and keeps the advertised line. Mutation-proven, and the mutations are the argument for the split rather than decoration on it: MUT-A collapse Undecodable into the Unobserved refusal arm a_refused_transport_licenses_nothing true an_undecodable_advertisement_licenses_nothing true <- blind a_refused_transport_names_the_unobserved_cause true ...names_the_undecodable_cause_and_keeps_line FALSE <- sole detector MUT-B let an undecodable advertisement admit a write both undecodable rows red, both unobserved rows correctly blind MUT-A is the load-bearing receipt. Every row that asks "was the dangerous thing prevented?" stays green under the flattening, because the collapsed arm still refuses -- the defect is invisible to exactly the checks a reviewer runs first. Only a row asking "did the remedy survive?" catches it. Under the previous Option-shaped seam that row was unwritable (none == none), so this defect class had no possible detector; it was found by reading, not by testing. 7/7 witnesses green; both files carry no annotation-grain diagnostic. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * The admission gate consumes the observation's decision, not an Option-shaped prior The desired ref moves only when two independent facts hold: the candidate's floor is green (the revision is PROVEN) and the ref's current state was OBSERVED (the write is SAFE to attempt). The gate checked the first and took a `GitObjectId?` for the second -- and that Option was the exact collapse the observation type was split to remove, surviving one layer down. `none` meant BOTH "origin advertises no such ref, create it" and "we could not observe the ref", and the arm took the SAME action for both. So a refused ls-remote rendered as a ref CREATION: the empty-observation narrow with an actuator on the end of it. The gate now consumes FleetDesiredExpectationDecision, which has already refused the two observations that license nothing, so no unobservable state can reach an admitted advance -- construction, not a check. AdvanceAdmitted now carries the GitRemoteRefExpectation the compare-and-swap actually consumes (git.PublicationTransport PushRefUpdateWithLease), so the binder's input is total. The refusal cause is typed rather than a String, and its ORDERING is stated and tested: an unproven candidate reports the floor even when the ref is also unobservable, because the floor fact is intrinsic to the candidate and no retry fixes it. Also corrects a citation that was wrong in the direction that fails by succeeding. The comment cited `git update-ref <ref> <new> <old>`. refs/fleet/desired lives on origin and is read with ls-remote, so update-ref moves a LOCAL ref, exits 0, and leaves the fleet's desired state untouched while reporting an advance. That sentence was pointing the next implementer at the one operation whose failure mode is a silent success. 6/6 witnesses green. Two are newly writable: a_proven_revision_with_an_unobservable_ref_is_still_refused an_unproven_candidate_reports_the_floor_not_the_transport The first is the row the Option made impossible -- under `current: GitObjectId?` an unobservable ref and an absent ref were the same value taking the same arm, so no test could have separated them. The lease-identity assertion is also new: checking only the AdvanceAdmitted variant leaves both a lease naming the wrong prior (refuses forever) and a lease claiming absent-when-present (CLOBBERS) silent. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * One accepted fleet revision from two exact positive facts The desired ref must never move onto a revision whose floor did not run, and the failure that matters is not a red floor -- a red floor is loud and refuses. It is a GREEN floor belonging to SOMETHING ELSE: a PR's merge-subject run, a fork's branch, a different workflow in the same repository, a run that was cancelled rather than concluded. Each produces a truthful "a workflow run succeeded", and none proves what the fleet needs proved. TWO PROPOSITIONS, TWO PRODUCERS, and the split is the point: RequiredCiSucceeded the Required CI contract completed successfully for revision R DefaultBranchRevisionObserved revision R entered the default branch Neither implies the other and they are proved by different facts, so folding them into one predicate would let either stand in for the pair. A PR's merge-subject run CAN produce the first -- the floor genuinely ran and genuinely passed on that tree, and refusing it as a CI failure would be a lie about a real result -- and it CANNOT produce the second. That asymmetry is what stops the fleet following a revision main never had, and it is only expressible because the two are apart. THE SCM FACT IS NAMED FOR WHAT THE EVENT CAN PROVE. A workflow_run envelope carries the head branch and the originating event; it does not distinguish a PR merge from a direct fast-forward push, an authorized emergency push, or any other mechanism that moved the branch. So the carrier is DefaultBranchRevisionObserved, not MergedMainRevisionObserved: naming it for merges because merges are the ordinary producer would assert provenance nothing observed. THE REVISION IS DECODED ONCE. GitHub says head_sha is a SHA; nothing on the wire establishes it. Both producers decode through git_object_id_from_untagged_hex and refuse an undecodable value BEFORE any positive carrier exists, so no consumer can be handed a revision that is not one. One canonical GitObjectId is carried, never an authored CommitSha beside it -- two writable names for one fact could disagree. EVIDENCE IS A TYPE PARAMETER, NOT A VARIANT. GitHub is the first provider of both propositions and will not be the last; an accepted fabric receipt proves the same Required CI proposition through a different channel. `GitHub | Fabric` inside the positive carrier would make every consumer branch on a provenance it has no business branching on, and make adding a provider an edit to the admission carrier. NO PHASE ROSTER. RequiredCiSucceeded carries RequiredCiContractIdentity, derived from the artifact authority that emits the workflow. The fleet asks whether the exact contract succeeded for the exact revision; it does not own the contract's internal phase roster, and a `phases_run == 6` field would make every phase added to the floor a breaking change to fleet admission. The sole join produces AcceptedFleetRevision, and downstream only its .revision exists -- no candidate remains beside it to compare or accidentally substitute. The mismatch arm is load-bearing: Required CI proving A while the branch carries B is not a contradiction in the data (both facts true, different revisions, arriving together whenever a push lands mid-run); what is false is the CONJUNCTION anyone would infer from holding both. It refuses carrying both revisions, because "which two" is the entire content of the finding. 9/9 witnesses green. NOT IN THIS CUT, and named so it is not read as further along than it is: forward-only motion. A CAS makes the write ATOMIC, not MONOTONE -- a valid lease against a correctly observed prior will move the ref backwards to an older revision without complaint. Ancestry, the superseded-result no-op, and unverifiable-ancestry refusal come next, over the existing DeployRevisionRelation authority. No actuator consumes AcceptedFleetRevision yet, so nothing can advance on it in the meantime. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * Forward-only desired-ref admission: a lease is atomic, not monotone The correction that shapes this whole cut, because it is the thing most easily assumed. A compare-and-swap naming the observed prior refuses a CONCURRENT modification and says NOTHING about direction. A perfectly valid lease against a correctly observed prior will move the ref BACKWARDS to an older revision without complaint, and every check upstream will have passed: the revision was proven, the floor was green, the observation was real, the lease matched. Nothing in the CAS is capable of noticing. Forward-only motion is a separate property needing its own evidence. WHAT THE INPUTS WERE, AND WHY NONE SURVIVES: candidate: GitObjectId a target nameable independently of any evidence about it, so a caller could prove A and advance onto B floor_green: Bool unfalsifiable at the call site; asserts SOME floor was green and binds that greenness to no revision at all current: GitObjectId? none meant both "no such ref, create it" and "could not observe it", same arm for both, so a transport failure actuated a ref CREATION All three are replaced by carriers that cannot express the bad state rather than by checks that detect it. AcceptedFleetRevision is constructible only from two exact positive facts about ONE revision, so no candidate remains beside it and no Bool stands in for which revision was proven. THE RELATION IS SUBJECT-BOUND AND THE BINDING IS CHECKED, NOT TRUSTED. A bare DeployedIsAncestor is not evidence: it does not say WHICH TWO revisions were compared, so a relation computed for another pair would satisfy a decision about this one. The observation carries both endpoints and the decision refuses when they are not the exact pair under decision. Without that check the binding would be a naming convention rather than a wall. Five terminal states, and two are successes that write nothing. AlreadyConverged and SupersededNoOp are not failures: a late result for an older revision arriving after a newer one was admitted is the normal consequence of runs finishing out of order, and the desired state is already correct and more advanced. Rendering either as operational red trains an operator to ignore the channel, which is how a real refusal later goes unread. The admitted arms carry the SHAPE of their lease, not a general expectation: a create carries no prior because there is none, an advance carries exactly the prior it verified. Handing both a general GitRemoteRefExpectation would let a create arm carry MustEqual and an advance arm carry MustBeAbsent -- the clobbering pair -- which is representable in the general type and unrepresentable here. No `to:` field sits beside accepted.revision; a second writable name for the target would recreate the substitution this cut removes. The relation vocabulary is reused from gunbc.live_deploy.revision rather than re-coined; a second five-variant enum beside it would be the nickname. 9/9 witnesses green. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * Fix broken main: answer the two observation arms fleet_desired_admission never got main does not resolve at e9e42f2f24. gunbc.fleet_desired_admission fleet_desired_admission_decide matches FleetDesiredRevision with two arms; #8701 split that type into four. Both landed green on their own branches and neither textual merge had a conflict, so the breakage appeared only in the combination -- a semantic merge conflict, which is exactly the class the fail-closed census exists to catch and exactly the class a clean `git merge` cannot see. Verified against origin/main directly rather than inferred from my own branch: ./target/release/gunbc run --source-root dag --source-root src/v2 \ --entry dag/gunbc/fleet_desired_admission.dag --function fleet_desired_floor_green error: resolve failed for dag/gunbc/fleet_desired_admission.dag cause: dag/gunbc/fleet_desired_admission.dag:169:7: error: non-exhaustive match: missing variant(s) FleetDesiredAbsent, FleetDesiredUndecodable One root, two dependent entries (fleet_desired_admission_workflow reaches it; ci_spec only mentions it in prose and resolves fine). THE ANSWERS FOLLOW THAT FUNCTION'S OWN STATED POLICY rather than inventing one. It already declines to create the ref from an unobserved prior, reasoning that a first admission must arrive as a distinguished observation and not as an arm guessing. FleetDesiredAbsent IS that distinguished observation -- but authorizing creation here would be a NEW CAPABILITY landing as a side effect of a compile fix, so it refuses and says what it would take instead. Undecodable refuses on stronger grounds: the ref EXISTS holding something unreadable, so a write would destroy it and a retry would not help. TWO EXECUTING WITNESSES, NOT JUST A COMPILE. A compile fix alone would leave the two most dangerous inputs to an actuator covered by nothing that runs, which is how a repaired build acquires an untested arm. The causes are asserted DISTINCTLY -- the undecodable row asserts it does NOT carry the creation wording -- because the entire point of the four-way split is that these two remedies are not interchangeable, and a test that accepted either would have re-collapsed them. 4/4 witnesses green, including the two pre-existing rows. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * Port the live admission consumer to the typed expectation seam fleet_desired_admission_decide called admit_fleet_desired_advance with `current: Present { value: prior }` and patterned on AdvanceAdmitted { from: .. }. Both are the shape this branch replaces, so without this port the branch resolves cleanly on its own and breaks main on merge -- which is precisely how the non-exhaustive-match breakage this stack is already repairing got in. The call now passes the observation's own decision. The refusal is typed rather than a String, so it is rendered by fleet_desired_advance_refusal_message, which lives beside the type: a new refusal arm cannot be added without that fold refusing to compile, keeping the message set and the cause set one authority. Consumers that need to ROUTE still match the variants -- the renderer is for the line an operator reads, never a substitute for the typed cause. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * Deduplicate the fleet_desired_ref_name import (review 54265) The import list carried fleet_desired_ref_name twice, introduced by this PR. Now exactly once, and a whole-file sweep confirms no other import list in the module repeats a name. One correction to the finding's reasoning, kept because it is the more useful half: it predicted "unless the language silently coalesces identical imports it will fail to resolve." It does coalesce -- the duplicate resolved cleanly and all four witnesses ran green against it, which is how it survived my own checks. So this was a real defect that produced NO diagnostic, not a latent compile error. That is the worse shape of the two: a duplicate binding is invisible to the substrate, so nothing but review will ever catch one. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * Say what the module cannot EXECUTE, not what policy forbids (module owner's wording) The Absent arm's cause read as a prohibition on creating the ref. It is not one. fleet_main_revision says outright that an absent ref is where a create belongs ("create it, and ONLY here"), and its expectation seam already maps Absent to RemoteRefMustBeAbsent. The limit is executional and local to this module: AdmissionAdvanceAuthorized carries a NON-optional prior, and the push renderer spells only --force-with-lease=<ref>:<prior-hex>, which has no operand for "expect this ref to be absent". Reusing the advance path would name a prior nobody observed -- an unconditional write wearing a compare-and-swap, which overwrites silently if the absence reading were ever wrong. So the cause now says the module cannot yet EXECUTE a creation rather than that creation is refused, because that sentence is what whoever picks up the create reads first, and the two readings send them to different work. Wording from nimble-fox-671, the module's owner, who reached the same refusal independently. The witnesses assert the new wording, and the undecodable row still asserts it does NOT carry it, so the two arms cannot re-fuse at the assertion layer. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * Surface MergeBase's exit code and fold it into a subject-bound ancestry relation git.Inspect.MergeBase declared three exits and surfaced none of them. Its output carried only success: Bool from exit_success, so exit 1 -- the pair genuinely shares no merge base, an ANSWER about the pair -- and exit 128 -- invalid ref or not a repository, a failure to look -- arrived identically. A consumer holding that Bool has two moves and both are wrong: refuse both, discarding a real answer and blocking an advance unrelated-histories should have decided; or admit both, which reads an unreadable repository as PROOF that two revisions are unrelated. The distinction was always declared on the operation and was simply unreachable. THE FOLD IS PURE AND THE EFFECT IS NOT, AND THE SPLIT IS NOT TIDINESS. git.Inspect.MergeBase carries no mock_response, so any witness reaching it REFUSES under the hermetic floor envelope rather than running. Folding the ancestry policy into the effect would make the whole policy unwitnessable, and this tree has paid for that once already -- stage0_rust_host_observation_live_witness_test records a single unmocked operation taking down a 105-row batch. So the policy is hermetic and total, and only the reading of two commits is not. One merge base decides BOTH directions: a commit is an ancestor of another exactly when it IS their merge base, so no second probe is needed. A base that is neither endpoint means the histories diverged, and it folds to UnrelatedHistories to match the semantics the existing probe fold already assigns that variant -- reusing that vocabulary rather than minting Diverged keeps one authority for "how do these two revisions relate". Equality short-circuits before any probe result is consulted. 14/14 witnesses green. The load-bearing row asserts exit 1 and exit 128 TOGETHER, because either alone is satisfiable by a fold that ignores the exit code entirely -- one by always observing, the other by always refusing. It is the divergence between them that carries the claim, not either verdict on its own. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * Hoist the arm rationale to module grain (§4c): the floor refused during preparation CI run 32454621446 refused with 23 diagnostics at fleet_desired_admission.dag :179-201 -- "source annotation sits inside a declaration body". The explanatory block sat inside the match arms of fleet_desired_admission_decide. §4c admits standalone leading // blocks only at module-item grain; the content was fine and only its position was refused. It now reads as a preamble above the fn, which is how the rest of that module already does it. WHY THIS WAS NOT CAUGHT LOCALLY, recorded because the gap is the expensive part: `gunbc run --entry` and claim runs DO NOT enforce annotation grain. Every witness returned true against the refusing file. The check that does: gunbc compile --output-dir <dir> --source-root dag --source-root src/v2 --entry <file> now reports 0 blocking errors on this file. AND THE FAILURE MODE IS WORSE THAN ONE RED WITNESS: the floor refuses during PREPARATION, so the run reports `modules_resolved=3762 modules_excluded=4` with ZERO witnesses executed. That line reads like a floor that ran and found nothing wrong. It is the opposite -- nothing ran at all. The trap is specific and it repeated: correcting a comment's CONTENT tempts you to move it next to the subject it describes, which is exactly where §4c forbids it. Fixing a truthfulness defect introduced a structural one, in a commit whose entire purpose was to make that comment truer. Independently diagnosed by nimble-fox-671 from the same log. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * Three structural corrections: input sum, one unverifiable, and creation is not implied by absence Side-chat review of the forward-only cut found three things the decision got wrong. Each is a construction move rather than a check, and one of them was already visible in my own fixtures. 1. THE INPUT IS A SUM, SO IRRELEVANT EVIDENCE CANNOT BE SUPPLIED. decide_fleet_desired_advance took (accepted, expectation, relation) unconditionally, but only ONE of the three expectation outcomes raises an ancestry question: a refused expectation has no current revision to compare, and an absent ref has none either. The tell was in the tests -- the create witness constructed a same-revision relation purely to satisfy a parameter its arm ignores, and so did both refusal rows. A fixture that must invent a fact to call a function is reporting that the signature admits states the domain does not have, and a production caller would have invented the same one. FleetDesiredAdvanceInput's three variants carry evidence exactly where evidence exists. 2. ONE REPRESENTATION OF "UNVERIFIABLE", NOT TWO. FleetRevisionRelationObservation was a coproduct of Observed{relation} and Refused{cause}, while DeployRevisionRelation already has RelationUnverifiable{cause}. The proof that no distinction existed: the decision mapped both to the same refusal, so the outer variant carried nothing. It is now a record -- one pair, one relation result -- and every failure to establish direction is RelationUnverifiable. Remedies that later need separating belong inside a typed cause for that variant, not in a second outer refusal path beside it. 3. ABSENCE IS A STATE; CREATION IS A CAPABILITY. RemoteRefMustBeAbsent is a compare-and-swap PRECONDITION -- it proves the ref is not there -- and establishes nothing about whether this path may bring the fleet's root authority into existence. FleetDesiredCreateAdmitted inferred the second from the first, and porting the live consumer would have silently widened policy: gunbc.fleet_desired _admission refuses first creation today, deliberately, so a "consumer port" would have handed a workflow authorized only to ADVANCE the power to MINT. The arm is DELETED rather than left unreachable -- an admitted-create variant with no producer is the unconsumed capability this lane keeps refusing elsewhere -- and absence now refuses as InitialFleetDesiredCreationNotAuthorized, naming the revision whose creation was declined. When creation is authorized it arrives as its own positive carrier and only the conjunction may admit. Also lands the ancestry observer's decidable half. git.Inspect.MergeBase declared three exits and surfaced none: exit 1 (the pair shares no merge base -- an ANSWER) and exit 128 (invalid ref or not a repository -- a failure to look) both arrived as exit_success = false, so a consumer had to refuse both, discarding a real answer, or admit both, reading an unreadable repository as PROOF that two revisions are unrelated. The exit code is now carried and folded. THE FOLD IS PURE AND THE EFFECT IS NOT, and the split is not tidiness: git.Inspect.MergeBase carries no mock_response, so any witness reaching it REFUSES under the hermetic floor rather than running. Folding the policy into the effect would make the whole ancestry policy unwitnessable, a lesson this tree has already paid for once. One merge base decides both directions -- a commit is an ancestor exactly when it IS the merge base -- so no second probe is needed. 13/13 witnesses green. The transport-boundary mutation the review specified (collapse exit 1 and exit 128) reds exactly the row written for it and leaves the other three green. The exit-1 and exit-128 assertions live in ONE row deliberately: either alone is satisfiable by a fold that ignores the exit code entirely -- one by always observing, the other by always refusing -- so it is the divergence between them that carries the claim. §4c: the MergeBase rationale is at module grain above the service, not inside it. Verified by `gunbc compile` (0 blocking) rather than by a claim run, which does not enforce annotation grain. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * Take main's arm wording and drop this PR's stale copy of its witnesses gunbc#8744 landed the two restored arms on main while this branch was in flight, with different cause wording. Two consequences, both resolved toward main. The module-grain block describing those arms is main's; mine described arms this PR no longer contributes, so it is dropped rather than merged beside it. What this PR still owns in that file is the CALL SITE port -- the typed expectation seam and the AdvanceAdmitted { expected, .. } pattern -- which main does not have and which is what stops this branch breaking main a second time on merge. The two witness rows carried here asserted "cannot yet execute one", which was MY wording; main's arm says "cannot express a creation". They would have gone red against main and, worse, they would have gone red for a reason that looks like a behavior regression while the behavior is identical -- a stale assertion reporting on wording rather than on conduct. Those rows belong to gunbc#8738, which owns the executing coverage for these arms and already asserts main's actual strings, so the file is restored to main's version here rather than reconciled in two places. 3/3 pre-existing witnesses green; gunbc compile reports 0 blocking. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * Reuse the relation DECISION, not only its five variant names Review caught a fork I had introduced while believing I was avoiding one. This cut reused DeployRevisionRelation's vocabulary and then independently re-derived the classification from a merge-base object: base == current -> DeployedIsAncestor base == accepted -> CandidateIsAncestor otherwise -> UnrelatedHistories gunbc.live_deploy.revision already owned that answer through deploy_revision_relation_from_probes. So there were two places computing one decision -- the §3 fork in its quietest form. Not two names for one concept, which is the shape I was watching for, but two derivations agreeing today and free to drift apart tomorrow, with nothing to notice if a later correction reached only one and left two different meanings of CandidateIsAncestor in the tree. The classification is now revision_relation_from_ancestry_facts, taking ancestry FACTS, and the evidence shapes project into it: two directional probes from the deploy lane, one merge-base object from the fleet lane. One policy, two evidence realizations, which is the split that was actually wanted -- the vocabulary was shared while the policy was copied. Behavior-preserving on both sides: the probe fold now delegates and its existing witness (equal_shas_short_circuit_before_the_probes) stays green, and the three merge-base rows stay green. gunbc compile reports 0 blocking. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * The effectful half of the ancestry observation, and the sole constructor of one observe_fleet_revision_relation(current, accepted) probes git.Inspect.MergeBase and feeds the pure fold. Three properties are deliberate. SOLE PRODUCTION CONSTRUCTOR. The fold stays public because the POLICY must be witnessable hermetically -- MergeBase carries no mock_response, so any witness reaching it refuses under the hermetic envelope -- but product code must not author an exit_code, a base hex and a stderr and call it as though those were observed. Census after this commit: the fold's only production caller is this module; the three other call sites are witnesses, which is what the split is for. THE PRECONDITION IS STATED, NOT PARAMETERIZED. MergeBase takes no repository and runs in the PROCESS WORKING DIRECTORY, so this function requires its caller to be executing inside the repository whose history is compared -- which the live admission workflow already is. It deliberately takes NO `repo` argument: the operation provides no `git -C`, so a repo parameter would be silently ignored. A signature promising a capability the transport does not have is worse than an honest precondition, because it reads as checked. OutcomeIsData, NOT ExpectSuccess. Exit 1 from `git merge-base` means the pair shares no merge base -- an ANSWER about the pair, not an operational failure. Declaring it a failure is exactly the collapse the exit-code work removes, since `success` is false for both exit 1 and exit 128. (Noted while reading: the existing caller in gunbc.stage0_rust_host_observation does use ExpectSuccess and tests `!baseline.success`, so it cannot distinguish unrelated histories from an unreadable repository either. Not touched here -- different lane, and refusing both may well be correct for its question -- but it is the same collapse and it is now visible.) Equality short-circuits without invoking git, so the common converged case costs no subprocess and cannot be turned into a refusal by an unreadable repository. NOT YET CONSUMED. The observer has no caller until the live consumer port lands in this same PR, which is the next piece and the reason this stays draft. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * Read the repository and branch authorities instead of spelling them again This module carried `fleet_repository_full_name = "gunb-ai/gunbc"` and `fleet_default_branch = "main"` as data rows. Both are the sixth and seventh nicknames for facts that already have authorities. gunbc.repository exists precisely because five spellings of this repository's identity had accumulated across the tree, and its own note answers this case directly: the answer to five nicknames is not a sixth. gunbc.repo_identity owns the default-branch name and carries a perturbation oracle that moves every consumer when it changes -- a literal here is INVISIBLE to that oracle, which is what keeps this class hidden. Every individual literal looks obviously correct. Review flagged these as policy config that could later be lifted. It was not a later problem: the authorities already existed and this module simply was not reading them. OBSERVED WHILE DOING IT, and flagged rather than silently resolved: gunbc_repository ALSO carries a default_branch field, so the default branch appears to have two homes. They agree today. The branch reads from gunbc.repo_identity here because that module's note claims authority for branch facts explicitly and carries the oracle, while Repository.default_branch is part of the upstream API shape this project instantiates. Whether those should be one row is a real question and not this cut's to settle. 4/4 witnesses green; gunbc compile reports 0 blocking. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * Port the live fleet-desired admission onto the accepted-revision authority, and close a trigger-grain fail-open THE PORT. gunbc.fleet_desired_admission consumed its own copy of workflow identity, trust checks, a floor_green Bool, candidate decoding and the old advance gate. #8720 and #8725 replaced all of it. This deletes those routes at the root rather than wrapping them: fleet_desired_admission_event_trusted, fleet_desired_floor_green, the old decide and the old push renderer are gone, and the live orchestration is now event -> fleet_desired_accepted_from_event (two producers, one join) -> fleet_desired_advance_input_wet (the only effectful step) -> decide_fleet_desired_advance -> fleet_desired_action_from_decision -> one rendered action fleet_desired_advance_input_wet does NOT re-classify the observed ref. It routes the already-classified result of fleet_desired_advance_expectation, so "absent vs unreadable vs unobserved" keeps one authority, and only the observed-current arm reaches git -- an event that produced no accepted revision can never trigger an ancestry probe. THE ACTION SUM. A successful decision no longer implies a push. Two of the three authorized actions mutate nothing (already-converged, superseded), and both render a NONEMPTY script by the renderer's shape rather than by an author remembering to echo. That is load-bearing: the executing step's `test -s` is the wall separating "authorization produced nothing" -- a writer or transport failure -- from "authorization said do nothing". If a no-op could render empty those two states would collide at the only place that can still tell them apart, and a dropped authorization would read as a converged fleet. Two witnesses pin it, plus one asserting no no-op contains `git push`. Names renamed to authorized_action end to end, including the emitted yml and the step title, so the human surface stops claiming every positive action is a push. THE FAIL-OPEN, found by nimble-fox-671 against origin/main and handed over rather than edited in parallel. The workflow_run trigger named no branches, so EVERY branch's floor completion created a run that entered the single constant concurrency group and only then skipped on the job-level head_branch condition. In the default group an arriving entry cancels the pending one, so a pull request's floor completing could evict a pending admission for a green main revision and do nothing in its place -- no advance, no refusal, no diagnostic, and a `cancelled` run indistinguishable from noise. Observed tally over 131 runs: 77 skipped, 45 cancelled, 6 failure, 3 success. Fixed at the trigger grain, not the concurrency grain. WorkflowRunCompleted gains a REQUIRED branches member emitted unconditionally like its Push and PullRequest siblings, so a caller cannot declare this trigger without deciding which branches it answers to. Documented semantics confirmed before emitting: `branches` on workflow_run filters on the branch of the TRIGGERING run, the same fact the job-level condition tests, one grain earlier. Widening the queue instead (ConcurrencyMappingQueueMax) would have stopped the eviction and left the cause, trading a silent drop for up to a hundred no-op entries stalled ahead of a real admission on a single-concurrency runner. The job-level condition and the in-model trust checks stay; the filter is defence in depth. The concurrency annotation's existing argument -- that losing a superseded pending admission is preferable to walking the fleet through revisions it has passed -- was SOUND. Its unstated premise, that every entry in the group is an admission, was false, and the falsifying fact lived three declarations away in the trigger. With the filter in place that argument is true as written for the first time, so the variant stays and the annotation now records why it was only accidentally right before. SCAFFOLD PREMISE CORRECTED. The dissolution row claimed no typed compare-and-swap carrier existed. #8697 falsified that. PushRefUpdateWithLease IS the typed wire capability; what is missing is the sole request-to-wire binder, a cited decoder for git's push-rejection output separating a stale lease from a failed push, and an independent remote readback. Moving to the typed row today would trade an honestly-untyped shell for a typed call whose refusal semantics this gate cannot read, so the shell survives with an honest premise instead of a false one. Stale citations of the deleted admit_fleet_desired_advance repointed at decide_fleet_desired_advance in three modules. EVIDENCE: all 17 witness rows run green by execution, individually, not by typecheck. The branch-filter row was run as a discriminating pair -- green with the filter, red with branches emptied, restore verified by diffstat. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * Repair the fixture the previous commit captured mid-mutation, and correct that commit's evidence claim TWO DEFECTS IN THE PREVIOUS COMMIT, BOTH MINE, BOTH FROM THE SAME ROOT. FIRST, THE FIXTURE IS MALFORMED. observed_input passed a bare DeployRevisionRelation into FleetDesiredObservedCurrentInput.relation, which is declared FleetRevisionRelationObservation -- a nullary coproduct variant where a record is required. It reaches the correct record here instead. This matters beyond the type error. The whole point of carrying the OBSERVATION rather than the bare verdict is that a relation must say WHICH TWO REVISIONS it compared, so a relation computed for one pair cannot be applied to another. A fixture that hands over a bare verdict cannot exercise that proposition at all, so the file was not testing the thing it is named for. SECOND, THE EVIDENCE CLAIM WAS WRONG. That commit said "all 17 witness rows run green by execution". There are 21 rows, and 14 had receipts when it was written. All 21 are green now, each run individually, and the six whose receipts were taken while the file was temporarily mutated were re-run against the clean file. The number was not a typo -- it was a count I did not take, in the same message that insisted on execution over typecheck. THE ROOT OF BOTH: I ran mutation probes against the live working tree while other runs read it, so `git add -A` captured the tree mid-probe and one batch of receipts was measured against a file that was briefly not the committed one. Mutation probes belong in a separate checkout; running them in place makes the tree a shared mutable resource between the thing being measured and the measurement. WHAT THE MALFORMED FIXTURE INCIDENTALLY EXPOSED, recorded here because it is a real observation and NOT yet a claim: that construction compiled and failed only at runtime with NoSuchField. If a clean compile-clean-then-runtime-fail pair reproduces on a minimal specimen, it is an ordinary-compiler-floor gap -- values inhabiting declared types is the baseline, not the differentiator. It is being probed separately, as source text in a compiler specimen rather than as a malformed live value in a fabric witness, because a witness carrying a broken construction to serve as compiler evidence stops testing its own subject. No claim is made here and none should be read into this commit. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * Queue every admissible main completion instead of replacing it: forward-only is what makes the queue safe THE VARIANT WAS RIGHT YESTERDAY AND IS WRONG TODAY, BECAUSE OF THIS PR. The workflow used ConcurrencyMappingQueueNotMax -- the default group, which holds one running and one PENDING entry and CANCELS the pending one when a new entry arrives. The annotation argued for it: losing a superseded pending admission is preferable to walking the fleet through revisions it has already passed. That argument was sound. Its premise -- every entry in this group is an admission that subsumes the pending one -- was false in three separate ways, each found by someone turning an instrument on the previous fix: A PULL REQUEST'S FLOOR. Closed in the previous commit by the branch filter. A RED MAIN FLOOR. A red floor does not supersede a green admission; it cancels one and refuses in its place. AN OUT-OF-ORDER GREEN MAIN FLOOR. Completion order is not revision order, so an OLDER green floor completing later evicts a pending NEWER admission and then advances to the older revision. Forward-only keeps this from being wrong, but it is the same dropped advance -- and unlike the other two it is the STEADY STATE, not a fault: two clean merges, two green floors. That is what moved this from "declare the gap" to "the variant is wrong". (A manual dispatch and an older successful rerun on main are two more; both carry head_branch main and neither can advance.) THE BRANCH FILTER AND THE QUEUE ANSWER DIFFERENT HALVES AND ARE NOT ALTERNATIVES. The split is whether admissibility is DECIDABLE AT THE TRIGGER GRAIN. For a pull request's floor it is -- the platform knows the branch -- so the right move is to refuse the entry, and queueing those would have been the absorbing fallback: cannot compute which entries matter, so hold them all, deficit frequency zeroed by construction, cost denominated in the corpus of branches. For what remains -- every main-floor completion -- it is NOT decidable there: conclusion, originating event and ancestry are all read in-model, after the run exists. GitHub's workflow-level concurrency is structurally too early to know whether an arriving entry subsumes a pending one. Queueing is then not a widened container standing in for a decision; it is the honest handling of a question that layer cannot answer, deferred to the layer that can. WHAT MAKES THE QUEUE SAFE IS THE FORWARD-ONLY DECISION IN THIS SAME PR. Before it, queueing every main completion would have walked the desired ref BACKWARD -- an older admission arriving later observes the newer prior correctly, and --force-with-lease does not refuse a correctly-observed overwrite. Under that model the default group's drop was accidentally protective, and the sound-sounding argument above was collecting the benefit of a defect. decide_fleet_desired_advance now classifies a superseded candidate as a no-op, so every queued entry is harmless by construction: advance, converge, no-op, or refuse. The drop was buying safety that is now carried properly. cancel-in-progress is forced false, which preserves the one property the default group genuinely provided: a RUNNING admission is never interrupted, so no cancellation lands between the compare-and-swap decision and the push. The witness asserts it SEPARATELY from queue:max rather than as an implication, because it carries a different property. THE DECLARED GAP IS DELETED, NOT REWORDED. It had been wrong three times in one night -- each time a better sentence about which evictions are safe. A row characterising an eviction that can no longer happen is a premise with nothing to be true about, so the fix is the variant, not the prose. A NARROWER TERMINAL DESIGN EXISTS AND IS NAMED IN THE ANNOTATION: concurrency AFTER classification, so only a positive AcceptedFleetRevision enters serialized actuation. That needs a classification job feeding a serialized actuation job, or the fabric queue. The queue here is the correct interim, not a stand-in for it. EVIDENCE: emitted bytes carry `queue: max` and `cancel-in-progress: false`; the new witness is green by execution and was run as a discriminating pair -- it returns false when the model is reverted to the default group, restore verified. Found by nimble-fox-671 (routes two and three) and side-chat review (manual dispatch, reruns, and the argument that queueing is now the safer variant). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * git.Inspect.MergeBase names the repository it inspects instead of inheriting the process position AN AMBIENT OPERATION MAKES A WRONG ANSWER INDISTINGUISHABLE FROM A RIGHT ONE. `git merge-base` ran against whatever checkout the process happened to occupy, so the same call meant different things depending on where it was invoked from -- and two repositories can hold refs that look identical, so nothing about the result reveals which one answered. The operand is REQUIRED rather than optional because an omitted repository is exactly the ambient form being replaced; an optional operand would leave that state writable. THIS IS THE REPOSITORY'S OWN ESTABLISHED ANSWER, NOT A NEW CONVENTION. extdeps.git RemoteUrlIn already takes `repository_path` and renders `git -C {repository_path}`, for the same reason -- it could otherwise confirm the remote of the wrong checkout. Verified in tree before adopting it rather than taken on recommendation. WHY THE OPERAND SITS ON THE OPERATION, NOT ON THE INVOCATION. "Which repository does this inspect" is a fact about the git operation's SUBJECT; "what directory did the OS start this process in" is a transport fact. Modeling the first as the second would push repository selection into every handler that runs a command -- the N x M adapter shape. One repository-addressed operation with one shell realization is not that. extdeps.exec.command deliberately gains no cwd concept. WHAT FORCED IT. The fleet ancestry observation could not be witnessed against a controlled fixture: a witness cannot relocate its own process, so the only reachable repository was gunbc's live history -- which DESIGN's oracle rule forbids as a merge-blocking test's subject, and which is unstable by construction. With the repository named, the same observation points at a fixture directory with no process games. THE SIBLING POPULATION IS DECLARED, NOT SILENTLY LEFT. Five operations in this service are still repository-ambient by the same mechanism -- HeadCommit, WorkingTreeStatus, IgnoredFiles, ListTreePathsAtRevision, ShowTree -- each with its own consumer census, and this cut is scoped to the one that blocked a wet observation. Toplevel is deliberately NOT in that list: its purpose IS to discover the ambient repository, so naming one would be circular. RUNG for the five: mitigatable, mitigated only by production happening to run from the root. NEXT TRIGGER: the first consumer that must inspect a repository other than its own process position -- which is what forced this one. CONSUMER CENSUS AND PORT, all three call sites, enumerated by declaration rather than by module-name grep (the other ~40 MergeBase hits are unrelated types -- DiffMergeBase, GitMergeBaseObservation -- and the separate MergeBaseIsAncestor operation): gunbc.stage0_rust_host_observation stage0_rust_observation_repository_path gunbc.roadmap_acceptance_history_observation roadmap_acceptance_history_repository_path gunbc.fleet_desired_observe fleet_desired_observe_repository_path Each is `.` in production, and each is now a DECLARED `.` rather than an ambient one -- a value that can be reviewed and changed, instead of wherever the process started. fleet_desired_observe's precondition annotation is REWRITTEN, not amended: it said the repository was "STATED RATHER THAN PARAMETERIZED", which described a shape the operation now refuses. Ruled in side-chat review, which corrected my framing: model the repository being inspected, not the process working directory. I had been weighing a generic cwd and was unsure of the layer; the subject/transport split is the answer, and the in-tree precedent settles it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * Restore the creation capability this branch silently reverted, and bound the queue witness to what the platform actually promises TWO FIXES, BOTH FOUND BY OTHERS, AND THE FIRST IS A CAPABILITY REGRESSION THIS BRANCH WAS ABOUT TO SHIP BEHIND A GREEN WITNESS. 1. CREATION WAS DELETED BY A CLEAN MERGE AND DEFENDED BY MY OWN TEST. gunbc#8746 landed creation on main by widening the admitted decision to carry a GitRemoteRefExpectation, so RemoteRefMustBeAbsent and RemoteRefMustEqual became two inhabitants of one type and an absent ref authorizes a compare-and-swap creation. This branch forked before that. Its admitted decision carried a bare prior oid -- a carrier in which creation is NOT REPRESENTABLE -- and refused the absent arm with a typed cause, InitialFleetDesiredCreationNotAuthorized. That was correct against the main it forked from. Merging origin/main brought #8746's code in. The wholesale rewrite here replaced it. NOTHING CONFLICTED, because the two changes touched different declarations of one function, and the witness suite stayed green because this branch carried a row asserting the refusal. So the regression presented as a typed refusal that looks like a considered policy position, plus a passing discriminating witness that looks like proof of it. Both of the usual instruments said fine. RESTORED: the decision carries `expected: GitRemoteRefExpectation`, the absent input is ADMITTED as a creation, the refusal variant is deleted, and the push now routes through GitRemoteRefCasRequest with git_remote_ref_lease_word / git_remote_ref_cas_refspec instead of the hand-spelled `--force-with-lease=` string this rewrite had introduced -- which was a second rendering of the lease beside the carrier that owns it. THE WITNESS IS INVERTED, NOT DELETED, and that is the general point: a witness asserting a capability's ABSENCE is precisely the artifact that makes a silent capability deletion look verified. This one would have carried the regression through review. The receipt now names the expected prior on both arms, via a separate fleet_desired_receipt_expected_phrase. The receipt and the lease need DIFFERENT renderings of one fact and sharing one is how the operand was lost upstream: git spells absence as an EMPTY expect value, which is right for the lease word and useless in a receipt, where an empty string is indistinguishable from an operand nobody printed. The absent arm renders as a positive word, and the match is over the closed sum rather than over the lease's hex-or-empty text. Design owed to nimble-fox-671. 2. THE QUEUE WITNESS NAME OVERCLAIMED, AND THE BYTES CANNOT WITNESS THE CLAIM. It was named `..._queues_every_admissible_completion_...`. GitHub documents the ceiling: "Up to 100 jobs or workflow runs can be `pending` in the concurrency group. When the queue is full, any additional jobs or workflow runs are canceled." Verified against the documentation directly rather than taken on report -- the cancel-when-full half was relayed as unverified and is now checked. So the honest claim is retention-instead-of-pending-replacement WHILE THE GROUP SITS BELOW 100 PENDING. Renamed to the_admission_workflow_uses_the_maximum_pending_queue_instead_of_pending_replacement, with the ceiling stated beside it. The overclaim was not observable from the bytes the row reads, which is exactly why the NAME mattered: at 100 pending the mechanism cancels and a row reading the emitted mapping still greens. A name is the claim the next reader inherits. Also recorded: queue:max buys no ordering either, since pending entries are processed by when they began waiting. If losslessness ever becomes required the next rung is durable reconciliation over (eligible floor-green revisions MINUS recorded admission decisions) -- an event ledger, not a bigger transport cap. EVIDENCE, run individually, green by execution: an_a…

gunbai-bot Bot changed the title ~~compute fabric design~~ One accepted fleet revision from two exact positive facts Aug 21, 2026

gunbai-bot Bot changed the base branch from main to fleet/admission-consumes-expectation August 21, 2026 04:51

gunbai-bot Bot marked this pull request as ready for review August 21, 2026 04:51

Brian Searls added 2 commits August 21, 2026 05:30

Merge branch 'fleet/admission-consumes-expectation' into fleet/accept…

36530ac

…ed-revision-two-facts

Merge branch 'fleet/admission-consumes-expectation' into fleet/accept…

b455a8e

…ed-revision-two-facts

gunbai-bot Bot mentioned this pull request Aug 21, 2026

Forward-only desired-ref admission: make the modelled wall the only route, and stop the queue dropping green advances #8733

Merged

Brian Searls and others added 4 commits August 21, 2026 06:30

Merge branch 'fleet/admission-consumes-expectation' into fleet/accept…

07efdb8

…ed-revision-two-facts

Merge branch 'fleet/admission-consumes-expectation' into fleet/accept…

3f849ab

…ed-revision-two-facts

Merge branch 'fleet/admission-consumes-expectation' into fleet/accept…

7877843

…ed-revision-two-facts

gunbai-bot Bot closed this Aug 21, 2026

Navigation Menu

Repository navigation

One accepted fleet revision from two exact positive facts - #8725

One accepted fleet revision from two exact positive facts#8725
briansrls wants to merge 7 commits into
fleet/admission-consumes-expectationfrom
fleet/accepted-revision-two-facts

briansrls commented Aug 21, 2026 •

edited by gunbai-bot Bot

Loading

Uh oh!

gunbai-bot Bot commented Aug 21, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

briansrls commented Aug 21, 2026 • edited by gunbai-bot Bot Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Two propositions, two producers

The SCM fact is named for what the event can prove

Three smaller walls

The join

Evidence

Not in this cut

Uh oh!

gunbai-bot Bot commented Aug 21, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

briansrls commented Aug 21, 2026 •

edited by gunbai-bot Bot

Loading