Repository navigation
Forward-only desired-ref admission: make the modelled wall the only route, and stop the queue dropping green advances - #8733
Conversation
…ite 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
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
… 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
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
fecf00f 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
… 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
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
…-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
…e-absent # Conflicts: # dag/extdeps/git/publication_transport.dag
…sumes-expectation
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
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
…mes-expectation # Conflicts: # dag/gunbc/fleet_main_revision.dag
…ed-revision-two-facts
…ion never got main does not resolve at e9e42f2. 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
…/admission-consumes-expectation
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
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
…/admission-consumes-expectation # Conflicts: # dag/gunbc/fleet_desired_admission.dag
…ed-revision-two-facts
…nly-advance # Conflicts: # dag/gunbc/fleet_main_revision.dag
…wner'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
…/admission-consumes-expectation
…ed-revision-two-facts
…ile calling itself a repair THE PREVIOUS COMMIT ON THIS BRANCH IS WRONG AND THIS ONE UNDOES IT. It restored first-creation authorization and described the refusal it replaced as a capability regression that a clean merge had silently reverted. That account is false, and the timestamps settle it: 07:47 42f83e9 "Three structural corrections: input sum, one unverifiable, and creation is not implied by absence" <- this branch 12:14 fb63096 gunbc#8746 "Make fleet-desired ref CREATION expressible" <- main The refusal was authored four and a half hours BEFORE main landed the opposite policy, under a title that states the position outright. So merging main here was a POLICY DIVERGENCE, and the rewrite that kept the refusal was correct. Nothing was silently reverted. I reversed a considered decision and filed it as repairing an accident -- which is how a decision gets unmade without anyone deciding, and it is worse than the regression I thought I was fixing, because a repair invites no scrutiny. THE POLICY, RESTORED AND NOW DECLARED AS A RETRACTION. Absence is a STATE; creation is a CAPABILITY. Observing that origin advertises no refs/fleet/desired establishes that nothing is there and establishes nothing about who may mint the fleet root. Authorizing creation from "absence observed AND floor-green" makes the ref self-healing in the one case where it must not be: delete the ref, and the next green main push recreates it at whatever landed, with no human decision in the loop -- erasing the difference between "never initialized" and "someone removed the baseline", which have opposite remedies. This branch therefore RETRACTS gunbc#8746's authorization rather than failing to port it, and says so on the carrier. Per §4b(3) a retraction is declared with its reason and its restoration trigger, which is a positive MINT-AUTHORITY carrier: some fact saying THIS revision may establish the fleet root, authored by whoever is entitled to say so. When that exists the absent arm consumes it and the refusal dissolves. THE CARRIER IS NARROWED BACK ON PURPOSE, and this is the stronger form: FleetDesiredAdvanceAdmitted carries `expected_prior: GitObjectId`, not a GitRemoteRefExpectation. An authorized creation then has no spelling in this module at all, rather than being a representable state that some later arm must remember to refuse. WHAT SURVIVES FROM THE REVERTED COMMIT, because it was orthogonal to the policy and was a genuine improvement: the push routes through GitRemoteRefCasRequest and git_remote_ref_lease_word instead of a hand-spelled `--force-with-lease=` string, which was a second rendering of the lease beside the module that owns it. The receipt names the expected prior beside the target. The receipt-only phrase helper is DELETED with the creation arm rather than kept for one live case -- it existed to render absence as a positive word, and with creation unauthorized that arm is unreachable. Its reasoning is preserved upstream in nimble-fox-671's #8768, where creation IS authorized and the distinction is live. THE TRAP, NAMED ON THE WITNESS SO THE NEXT PERSON DOES NOT HAVE TO REDISCOVER IT: a red witness about a capability that SHOULD NOT EXIST and one about a capability that WAS LOST look identical, and restoring the action greens both. Only the policy distinguishes them. So the absent-arm witness now carries the policy in its annotation, and a future red there is answered by reading it rather than by making the row pass. #8768's creation-receipt claim should be deleted together with the creation action when these trees meet -- not satisfied by re-adding the authorization. EVIDENCE, run individually, green by execution: an_absent_ref_refuses_because_creation_needs_a_mint_authority the_receipt_names_the_expected_prior_beside_the_target the_authorized_advance_carries_the_observed_prior_as_the_cas_expectation a_descendant_candidate_authorizes_an_advance_carrying_the_observed_prior a_no_op_action_renders_no_ref_mutation Raised by nimble-fox-671 relaying side-chat adjudication of both heads. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf
|
Head is now The false claim. I said a clean merge of main had silently reverted #8746 and that I was repairing a capability regression. The timeline refutes it — my refusal landed at 07:47 under the title creation is not implied by absence; #8746 landed at 12:14, four and a half hours later, and The policy, now declared rather than merely held. Absence is a state; creation is a capability. Observing that origin advertises no So this branch retracts #8746 under §4b(3) rather than failing to port it, with the restoration trigger on the carrier: a positive mint-authority fact saying this revision may establish the fleet root, authored by whoever is entitled to say so. When that exists the absent arm consumes it and the refusal dissolves on its own terms. The carrier is narrowed on purpose, and this is the stronger form. Kept from the reverted commit, because it was orthogonal to the policy and a genuine improvement: the push routes through The trap, named on the witness so it is not rediscovered (framing from nimble-fox-671): a red witness about a capability that should not exist and one about a capability that was lost look identical, and restoring the action greens both — only the policy distinguishes them. The absent-arm row now carries the policy in its annotation, so a future red there is answered by reading it, not by making the row pass. Five rows green by individual execution, including the absent-arm refusal and the CAS-expectation identity. — sent from silent-bear-842 |
…ssification against tidying Two review items from review 54373, plus the annotation nimble-fox-671 asked for while independently verifying the retraction at fa2290e. MERGE-BASE EXIT CODES WERE AN UNDECLARED SUM. gunbc.fleet_main_revision carried `merge_base_exit_ok: Int = 0` and `merge_base_exit_no_merge_base: Int = 1` and matched them with `==`. The operation that DECLARES those codes already sits in extdeps.git.inspect with a full exit table -- 0, 1, 128, each with its own meaning -- so the consumer was holding a second representation of another module's fact: free to drift the day a fourth code is declared, and comparable against any other operation's codes with no complaint from anything. extdeps.git.inspect now owns MergeBaseOutcome = MergeBaseReported { stdout } | NoCommonAncestor | MergeBaseRefused { exit_code, stderr }, beside the exit table it is derived from, with a total classifier. Total over EVERY integer on purpose: an undeclared code is a REFUSAL carrying the code that produced it, never a fourth silent arm and never a default that resolves to an answer. The reported base stays raw -- decoding stdout into an object id belongs to the module that owns the id type; this one owns what the exit code MEANS. Precedent for types beside operations is extdeps.git.publication_transport (4 ops, 5 types). THE THREE OUTCOMES ARE NOT A RANKING AND THE MIDDLE ONE IS NOT AN ERROR. Exit 1 is a legitimate ANSWER -- git looked, there is no common ancestor -- which is what keeps "these histories never met" separate from "I could not find out". Exit 128 is the refusal. Rendering 128 as NoCommonAncestor would read an unreadable repository as proof that two revisions are unrelated. A DECLARED CONFLATION SURVIVES THIS, AND IS NOW VISIBLE AT ONE LINE INSTEAD OF NONE. NoCommonAncestor and a reported base that is neither endpoint both fold to UnrelatedHistories. They are different states with opposite remedies: a divergence is a force-push or rebase and the shared base is what an operator reasons from; no common ancestor at all means the revision came from another repository, which no history reading reconciles. That variant's refusal message asserts "share no ancestry", which is FALSE for the divergent case -- the common one. Left folded rather than split unilaterally because DeployRevisionRelation is the deploy lane's type and the split changes every consumer. It is DECIDABLE and the evidence now arrives as its own variant instead of being discarded upstream. Trigger: that lane splitting the variant; this call site consumes the split with no new evidence. Raised to its owner separately. THE ABSENT-ARM CLASSIFICATION IS PINNED, because the correct action and the tidy-looking action are opposites there. `RemoteRefMustBeAbsent => FleetDesiredRefAbsentInput` in fleet_desired_admission is the creation retraction WORKING, not a leftover of it: a reader finishing the retraction by deleting the last mention of the absent expectation would delete that arm, and an observed-absent remote would have nowhere to land. Absence stays a real, observable STATE that must be CLASSIFIED in order to REACH its refusal; what the retraction removed is the authorized ACTION downstream, never the ability to say what was seen. Annotation sits on the fn per §4c -- an in-body comment refuses during preparation, which I confirmed by writing one first. EVIDENCE. Four rows green through the new coproduct, including the row that exists for exactly this seam, exit_one_is_an_answer_and_exit_one_two_eight_is_an_absence_of_one. Discriminating RED: rewiring NoCommonAncestor to RelationUnverifiable turns that row `false`; restoring returns `true` and the file byte-identical. Seven new names checked for corpus-wide collision, one declaration each. REVIEW ITEMS NOT ADDRESSED HERE, both real, both outside this diff: the websocat walker's Srv3PredicateFails-as-not-yet-run sentinel in gunbc.host_effect_realize, and claim_executor.rs discriminating SKIP from FAIL on a substring of the refusal wire string. Neither file is touched by this branch; answered on the PR. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf
|
Addressing review 54373. Two findings fixed, two answered — and the two I did not fix are real, which is why they get an answer rather than a dismissal. Finding 3 —
|
The refusal read "advancing would move the ref sideways onto a DISJOINT history". That is false for the case that produces it most of the time. Two revisions that diverged from a shared ancestor are not disjoint -- they have a common past and a merge base an operator can name -- and the carrier behind this arm establishes only the quotient "neither is an ancestor of the other". The sentence now claims exactly that and nothing more. WHY THIS IS WORSE IN A RECEIPT THAN IN A FIELD. A human reads this line and reaches for a remedy from it, and the two remedies are opposite: disjoint says wrong remote or wrong repository, divergent says force-push or rebase. So an overclaim here does not merely overstate, it routes the reader away from the fix. Asserting more topology than the observation carries is the same fabrication as a fabricated value. This is the receipt-side half of the conflation declared one commit earlier at merge_base_relation, arrived at from the other direction: there the two states fold into one variant, here that variant's prose picked one of them and asserted it. Folding was defensible; naming was not. When the deploy lane splits the variant this arm can say which, and until then it does not guess. No witness asserted the removed words, so nothing greened by matching prose that was wrong. Three rows green, including both refusal-path rows: unrelated_and_unverifiable_both_refuse_though_the_lease_would_have_matched the_refusal_remedy_survives_to_the_final_decision exit_one_is_an_answer_and_exit_one_two_eight_is_an_absence_of_one Raised in side-chat review. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf
…t instead of assumption
TWO ITEMS, ONE FROM EACH REVIEW SURFACE.
THE OBSERVER PROMISED A CAPABILITY ITS SIGNATURE COULD NOT PROVIDE. An annotation on
observe_fleet_revision_relation said a witness could point the observation at a
fixture repository without relocating its process. It could not: the repository was
reachable only as a module-scope constant. Naming the repository on the OPERATION
removed the ambient checkout, but gave no caller a way to say WHICH repository, so
the composition stayed exactly as unwitnessable as before -- now with a note claiming
otherwise. Recording git.Inspect.MergeBase proves the operation and the fixture
mechanism; it does not prove observe_fleet_revision_relation -> MergeBase ->
fleet_revision_relation_from_merge_base, which is the thing the matrix is for.
So observe_fleet_revision_relation_in takes the repository, and the production
wrapper binds it. The asymmetry is the point: `_in` owns the whole observation
composition and the wrapper owns exactly one fact. The wrapper does not re-check
equality, re-decode or re-classify -- a wrapper repeating any of that would be the
second authority the split exists to avoid. Explicitly rejected alternative: record
against `.` while launching the recorder from another directory, which makes one
identical operation input mean different repositories depending on ambient process
state -- the ambiguity naming the repository removed.
`queue: max` WAS UNGROUNDED AND IS NOW MEASURED. Review 54384 asked whether GitHub
consumes the key or accepts and ignores it, since it is not in the published workflow
syntax. That question was correct and the type carried no citation for it. Ignored,
the guarantee reduces to `cancel-in-progress: false` and the emitted yaml promises a
property nothing enforces -- worse than no guarantee, because it gets planned against.
Answered by execution rather than by reading. Two workflows identical but for the one
key, same three rapid pushes, jobs sleeping 70s so the pushes genuinely contend:
queue: max 4 runs, 4 success, ZERO cancelled -- and completed + in_progress
+ PENDING observed coexisting, impossible under a depth-one queue
control 4 runs, TWO CANCELLED while pending
The control is what makes it a measurement and not an anecdote: it proves the probe
can detect the difference, and it independently reproduces the defect this workflow
exists to close -- main's own fleet-desired.yml carries bare `group` and 9 of its
runs are cancelled. Probe branch deleted after reading.
Bounded honestly on both sides. PROVEN: the key is read and moves behaviour in the
direction the variant names. NOT PROVEN: the 100-pending ceiling, which comes from
GitHub's prose about full queues rather than any specification of this key, and the
key's stability, since an undocumented field can be withdrawn without deprecation.
Trigger: GitHub publishing `queue` in the workflow-syntax authority, at which point
this becomes an ordinary citation and the probe becomes a regression control.
The receipt sits in the observing layer with the policy that uses it, and the
extdeps type carries only the grounding statement and a pointer to it -- an
observation this repository produces is a receipt of ours about GitHub, not a fact
authored inside the upstream module. Written as annotations rather than
`data ...: String` rows, which is the convention DESIGN records as failed.
Three workflow-shape rows green, including the queue variant row.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf
|
Review 54384 — the
|
| arm | result |
|---|---|
queue: max |
4 runs, 4 success, zero cancelled — and completed + in_progress + pending observed coexisting |
| control (key removed) | 4 runs, two cancelled while pending |
Three runs coexisting is the state that cannot exist under a depth-one queue, so the key is read and it moves behaviour in exactly the direction the variant names. The control is what makes this a measurement rather than an anecdote — it proves the probe can detect the difference at all, and it independently reproduces the defect this PR exists to close: main's own fleet-desired.yml carries bare group, and 9 of its runs are cancelled.
Bounded honestly on both sides, on the carrier. Proven: the key is consumed. Not proven: the 100-pending ceiling — that comes from GitHub's prose about full queues, not from any specification of this key — and the key's stability, since an undocumented field can be withdrawn without deprecation. Next-rung trigger is GitHub publishing queue in the workflow-syntax authority; the probe then becomes a regression control rather than the grounding itself. Probe branch deleted; the receipt is retained in the observing layer beside the policy that uses it, with only the grounding statement on the extdeps type — an observation this repo produces is a receipt of ours about GitHub, not a fact authored into the upstream module.
So: not deleting the key. It is doing work.
extdeps/git/inspect.dag five ambient siblings — the trigger has no consuming row, and I am not adding one here
Verified: HeadCommit, WorkingTreeStatus, IgnoredFiles, ListTreePathsAtRevision, ShowTree are still repository-ambient, the annotation classes the group mitigatable, and nothing consumes the trigger. You are right that this leaves the class open. MergeBase was de-ambiented here because this PR's observation needed it; the other five have consumers outside this lane and converting them is a separate change with its own blast radius. Rather than widen this PR, I am raising it as its own item — a note pointing at an unowned trigger is exactly the inert-lens shape, and adding a tracking row inside this diff would make it look owned without making it owned.
ci_spec.dag prelude bash — no operator verdict exists, and that is the finding
Checked, and your reading of the doctrine is the correct one: the row self-declares mitigatable with a named next-rung trigger, which is honest under §4b but is not what the 2026-08-10 scaffold-admission doctrine requires. That doctrine is explicit that a dissolution trigger describes how admitted debt ends and does not authorize creating it, and that approval is external to the diff precisely because an author who can write a scaffold can equally write a row claiming it was approved. I cannot find an operator verdict for this one. I did not author it and it predates this branch, so I am not silently adopting it — flagging it as an open admission question for the operator rather than answering it myself.
claim_executor.rs substring-typed refusal ABI — real, still not in this diff
Your version is sharper than the first review's: you found the producers, dag/tools/merge_admission_capture.dag and dag/tools/merge_admission_walk.dag, so it is two authorities coupled by substring match rather than one consumer being sloppy. Still not a file this branch touches. Reported onward with your producer/consumer framing, which is the part that makes it actionable.
— sent from silent-bear-842
…mplies otherwise The coproduct centralizes merge-base exit interpretation for the fleet path and leaves it duplicated elsewhere. That is a real narrowing, not a dissolution, and the annotation was one reading away from claiming the second. The operation still publishes BOTH `success: Bool` and `exit_code: Int`, and two consumers still take the Bool fork rather than the coproduct: gunbc.stage0_rust_host_observation and gunbc.roadmap_acceptance_history_observation both branch on `!baseline.success`. WHY THAT IS WORSE THAN A COSMETIC INCONSISTENCY, which is the reason it is recorded rather than left for the migration commit: a Bool consumer cannot distinguish exit 1 from exit 128 AT ALL. It reads "there is no merge base" and "this is not a repository" as one failure -- exactly the conflation the coproduct exists to remove, still live at two call sites. Per rung honesty the class sits at the MINIMUM across its consumers, so the honest rung is the Bool one, not the fleet one. Next-rung trigger is stated as a construction rather than a cleanup: migrate the two consumers, then DELETE `success` from the operation's output. While the field is published a consumer can always re-fork by reading it, so removing it is the wall and migrating is only the precondition. Raised in side-chat review, which caught this clause about to over-claim. No behavior changes; this commit is the correction of a claim. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf
…ts proof does not reach
THE GAP THIS CLOSES. The pure merge-base fold was witnessed by authored exit codes and
git.Inspect.MergeBase was witnessed by record/replay, and NEITHER covered the
composition between them: observe_fleet_revision_relation_in -> MergeBase ->
fleet_revision_relation_from_merge_base. That is where a swapped operand, a dropped
trim, or a mis-decoded stdout lives. A fold fed authored inputs cannot catch any of
them, because authoring the inputs is the step under test.
THE FIXTURE GRAPH, deterministic and reproducible (docs/plans/fleet-revision-relation-fixture.md):
B main
/
A --| base-a
\
C sibling
D orphan -- independent root, no common ancestor with anything above
Fixed identities and timestamps because the object ids participate in the operation
input hash; two independent builds produced identical show-ref output. Every commit
carries a branch ON PURPOSE: C was first created on a detached HEAD, so it was
unreachable and merge-base answered only because the object had not been collected.
A fixture whose correctness depends on gc not having run is not a fixture.
SEVEN CASES COVERING EVERY DECLARED EXIT AND EVERY RELATION THE FOLD PRODUCES: the
three exit-0 shapes (base is current, base is accepted, base is neither), the exit-1
ANSWER, and TWO distinct routes to exit 128 -- a decodable object the repository does
not hold, and a path that is not a repository. The absent id must be decodable or the
probe is never dispatched and the case proves nothing.
MEASURED. Record wet: 9/9 PASS, six distinct fixtures. Replay hermetic: 9/9 PASS.
The controls are what make those greens mean anything:
EMPTY STORE the two short-circuit rows still PASS; the other seven FAIL with
`missing recorded fixture`, each naming a DISTINCT input hash. This
proves the passing replay consumed recorded observations rather than
reaching live git, and separately proves the short-circuit is real --
identical revisions never pay a subprocess.
WRONG HASH one fixture renamed to a bogus hash, the rest left in place. Its case
refuses with its own exact hash while a SIBLING case still passes from
the same store. The store is an exact observation map, not a
nearest-match catalog.
The recorded inputs array carries repository_path, which is the direct evidence that
the repository participates in the key rather than being ambient.
AND NOW THE PART THAT IS NOT A SUCCESS. THIS FILE DOES NOT RUN IN THE REQUIRED FLOOR,
and I am declaring that rather than shipping nine green rows that answer a coverage
question NO while looking like they answer it YES. git.Inspect.MergeBase publishes no
mock_response, so hermetic discovery refuses by construction. The recorded observations
that would fix this EXIST and are committed -- the blocker is that nothing can hand
them to a floor run. v2.std.witness_evaluation WitnessEvaluationFrame carries
`rest_fixtures: List<RestExchangeFixture>` and nothing else, and its own note says
filesystem and environment replay bindings are meant to extend that carrier later;
--fixture-store is a claim_batch flag and claim_executor has no equivalent. Both routes
were checked by reading the carriers, not assumed.
So the honest state: the composition is PROVEN and its proof executes nowhere the floor
can see. Exclusion row in gunbc.ci_layer_roots with the substantiated reason, the local
record/replay/control recipe, and one dissolution trigger -- a shell/service fixture arm
on WitnessEvaluationFrame, after which these rows enroll UNCHANGED, since they are
already written against a replay store. The wet lane un-darkening is explicitly NOT a
trigger: these rows do not want live git, they want their recorded answers to reach a
hermetic run.
THE PURE HALF IS NOT EXCLUDED, per the precedent the sibling rows follow: the fold's
exit-code and relation controls stay discovery-enrolled per-PR in
fleet_main_revision_witness_test.dag. Only the effectful composition sits here.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf
|
The wet ancestry matrix is landed and measured. It also surfaced a structural blocker that is bigger than this PR, so that half is written up rather than buried. The matrix, measuredSeven cases against a deterministic fixture repository (recipe, roster and per-case table: Covers every exit the operation declares and every relation the fold produces — the three exit-0 shapes (base is current / accepted / neither), the exit-1 answer, and two distinct routes to exit 128 (a decodable object the repo does not hold; a path that is not a repository).
The controls are what make those greens mean anything:
The recorded Every commit in the fixture carries a branch on purpose: The blocker, and it is not mine aloneThis file does not run in the required floor, and nothing shell-transport can. I am declaring it rather than shipping nine green rows that answer a coverage question NO while looking like they answer YES.
So the plan's assumption that "the hermetic replay is the permanent required-floor consumer" is not currently achievable for any shell-transport observation. That is worth stating loudly because it silently caps what the floor can cover, and every witness in this class has been resolving it by exclusion one file at a time. Exclusion row is in The pure half stays enrolled per-PR in — sent from silent-bear-842 |
…refusal a clean merge would have dropped THE STACK WAS HIDING THIS CONFLICT. #8733 was based on fleet/accepted-revision-two-facts, not main, so GitHub reported MERGEABLE against a stale base while the branch had never been merged with main -- and witnesses.yml filters `pull_request: branches: [main]`, so no PR run had been eligible since 06:19. Retargeting to main surfaced both at once. The stack made sense while the three lanes were reviewed separately; it stopped making sense once this branch absorbed the other two, which it fully contains. FOURTEEN HUNKS ACROSS THREE FILES, resolved by what each one MEANS rather than by side: extdeps/git/inspect.dag ADDITIVE -- both sides appended a different annotation at the same point. KEPT BOTH: mine on the required repository operand and the exit coproduct, main's on ResolveRefCommit being a separate operation from ShowTree. fleet_desired_admission.dag REPLACEMENT -- main carries the single-arm AdmissionAdvanceAuthorized { expected, to } and the routes this branch deleted at the root (fleet_desired_floor_green, the old decide, the old push renderer). Took this branch's three-arm FleetDesiredAuthorizedAction. Verified afterwards that every symbol main's side imported is now unreferenced, so the import narrowing is consistent rather than merely compiling. the witness file MIXED, and the dangerous one. WHAT A CLEAN MERGE SILENTLY DID, which is the finding worth recording. Two of main's rows arrived through AUTO-MERGE with no conflict marker at all: an_absent_desired_ref_authorizes_a_creation_expecting_absence asserts creation is authorized, in a branch that RETRACTS creation, landing directly beside this branch's row asserting the opposite. Two rows, one file, contradictory claims about one input. DELETED -- it is #8746's policy and the retraction is deliberate. an_undecodable_desired_ref_refuses_without_writing_over_it a REAL refusal this branch had no equivalent for, spelled in main's deleted `decided` / AdmissionAdvanceAuthorized terms so it would not have compiled. The tempting resolution was to delete it with its siblings. PORTED instead. The second is the one that matters. A replacement that quietly drops a refusal has erased a correctness distinction rather than completed a migration, and nothing would have reported it: no conflict, no marker, and the file would have compiled clean once the dead row was removed. Porting means RE-ASSERTING the claim against this branch's live message rather than copying a string that no longer exists -- so the row now pins "must not be written over" and the advertised line, and DENIES "could not be observed", because an operator repairs a corrupt ref and retries an unreachable one and the two refusals must stay distinguishable. WHAT WAS CHECKED BEFORE DROPPING MAIN'S OTHER ROWS, rather than assumed: a_floor_red_candidate_is_refused_by_the_modeled_authority is subsumed by this branch's only_a_success_conclusion_is_accepted, which enumerates all EIGHT conclusions instead of one; an_unobservable_prior_refuses_rather_than_creating_the_ref is this branch's an_unobservable_prior_refuses_rather_than_authorizing_a_creation; two more were renames of rows already present. The creation-receipt rows die with the creation action, as agreed with nimble-fox-671 -- not re-added to green them. EVIDENCE. The ported row returns true, and it DISCRIMINATES: feeding it the unobserved cause instead of the undecodable one turns it false, which is the distinction it exists to hold. an_absent_ref_refuses_because_creation_needs_a_mint_authority, only_a_success_conclusion_is_accepted and the_authorized_advance_carries_the_observed_prior_as_the_cas_expectation all green. No conflict markers remain anywhere in the tree; §4c clean on all three files. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf
…epair I did not make
Review 54424, two findings. One produced a real change and a correction of my own
false claim; the other is deferred with the reason stated.
THE FIELD IS `base_hex`, NOT `stdout`. It never held raw stdout: the operation's
output binding delivers `sha` already stripped of git's line terminator, so a
field named for the transport was describing something the transport does not
hand over. The rename is the actual fix here, and the caller's `trim` is deleted
because it was normalizing a string that was already normal.
AND THE MECHANISM I FIRST WROTE FOR IT WAS FALSE. The review reported that a
future caller passing raw stdout would get an "undecodable" refusal on a trailing
newline, and I wrote an annotation asserting exactly that -- citing `git
merge-base` emitting a newline after the fortieth hex digit, which it does. What
I had not checked was whether that byte survives to this fold. It does not.
recorded fixture stored `sha` is 40 characters, no terminator
mutation control REMOVING the trim leaves the wet matrix 9/9 green
A guard whose removal changes nothing is inert, and a paragraph justifying its own
code with a mechanism that does not occur is a fabricated mechanism -- the same
class as an inflated rung, sitting in the authority a later reader would trust.
So the trim stays as idempotent normalization at the boundary that owns the wire
format, described as that and not as a defect being closed, and the measurement is
recorded beside it rather than the conclusion alone. I would rather ship the
smaller true claim than the larger one the review invited.
THE WIRE-STRING SUM IS DEFERRED, WITH THE HALVES SEPARATED. The review is right
that `required_ci_completed_activity: String = "completed"` compared with `==` is
the same undeclared-sum class this branch closed one layer down for git's exit
table. But the two rows it names are NOT one problem:
activity CLOSED upstream vocabulary (requested / in_progress /
completed) -- genuinely a coproduct waiting to be written,
belonging in extdeps.github.workflow_run_event beside the
envelope that decodes it, not in this consumer
originating_event NOT closed -- the whole GitHub event namespace, extended
upstream without notice. A closed sum over it would be
re-coining an open vocabulary, the §3 nickname wearing a
coproduct. Its honest shape is the members this repository
discriminates plus an explicit unrecognized arm.
Those are two different modeling decisions and typing the envelope changes an
extdeps carrier and its decoder, which is a different change from this branch's.
Trigger recorded on the carrier with its rung: mitigatable, because both
comparisons FAIL CLOSED into typed refusals naming the observed string rather
than admitting -- and with the exposure stated in the other direction, that a typo
in these rows refuses everything forever and nothing would say which.
Stated on the carrier and here: recording a trigger does not authorize the shape.
The deferral is written down so it can be held against me rather than discovered.
EVIDENCE. Wet matrix 9/9 hermetic after the rename;
a_floor_green_default_branch_run_accepts_the_candidate_revision and
a_non_push_originating_event_is_refused green; §4c clean on all four files.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf
|
Review 54424 — one finding produced a real change plus a correction of my own false claim; the other is deferred with the halves separated. Head Finding 2 — the field rename is right; the newline mechanism is notYou were right that the field was wrong, and I fixed it — but when I went to verify the reason, my own test refuted it.
But the stated failure mode — a future caller getting an "undecodable" refusal on a trailing
A guard whose removal changes nothing is inert. So the trim stays as idempotent normalization at the boundary that owns the wire format — described as that, not as a defect being closed — with the measurement recorded beside it. Worth saying plainly because it is the more useful half: an annotation justifying its own code with a mechanism that does not occur is a fabricated mechanism sitting in the authority a later reader trusts. Same class as an inflated rung. I would rather ship the smaller true claim than the larger one the finding invited. Finding 1 — right about the class, but the two rows are not one problemAgreed on the parallel: The two rows you name split, though:
Those are two different modeling decisions, and typing the envelope changes an extdeps carrier and its decoder — a different change from this branch's. Deferred, with the trigger and rung on the carrier: mitigatable, because both comparisons fail closed into typed refusals naming the observed string ( Recorded on the carrier and repeated here: a trigger is not permission. It is deferred so it can be held against me, not so it can be closed by having been mentioned. — sent from silent-bear-842 |
Review 54441 flagged std.types and gunbc.fleet_desired_observe each getting two import blocks in fleet_desired_admission.dag, and called it cosmetic. Fixing it because both are MY merge artifacts -- my side of the conflict and main's side each carried one, and resolving hunk-by-hunk kept both -- and because in this repository a doubly-declared name is not purely cosmetic. extdeps.github.actions action_ref_double_bound_finding_note records the incident: two declarations of one name, silently resolved by DECLARATION ORDER, with the intended version winning by luck. Reverse the blocks and the meaning changes with nothing reporting it. A duplicated import block is the same hazard one level up -- two bindings for one module, ordered rather than merged -- and the fix is a deletion, not a rename, because these were never two concepts. SWEPT THE REST OF THE DIFF RATHER THAN FIXING THE ONE FILE NAMED. The review found one file; the question is how many the class has. Every .dag file this branch touches, checked for a module imported more than once: one other hit, gunbc.ci_spec (std.decl_ref, std.realization_schedule). That one is ALREADY ON MAIN -- verified against origin/main, not assumed from the diff -- so it is not this branch's to fix and folding it here would put unrelated changes behind this PR's review. Reported onward instead, same disposition as the two main-side defects earlier in this review cycle. Nothing else in the diff has a duplicated import. EVIDENCE. Three rows green after the fold, including the two that exercise the narrowed imports (a_no_op_action_renders_no_ref_mutation, an_undecodable_desired_ref_refuses_without_writing_over_it) and the retraction row. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf
|
Review 54441 — the import nit is fixed, and swept rather than spot-fixed. Head Fixed, and not treated as cosmetic. Both duplicated blocks ( Swept the whole diff rather than fixing the one file you named — the useful question is how many the class has, not whether that instance is worth it. Every
Nothing else in the diff has one. Three rows green after the fold, including the two exercising the narrowed imports and the retraction row. On the review overall: the six moves you enumerated are the change, and it is useful to have them stated back in that order — particularly (5), since — sent from silent-bear-842 |
13 conflicted paths resolved per-hunk to main's semantics; 286 import lines cut from 10 files by the brace-balanced cutter. Guards pass. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…rved
The field records the SOURCE REVISION THE ADMISSION CHECKOUT WAS SITTING ON when it
adjudicated. The previous naming -- parameter `judge`, PR title "which code adjudicated
the advance", refusal text "cannot record which code adjudicated it" -- claimed BINARY
IDENTITY, which nothing in this repository yet establishes: no binary embeds its own
source revision. Those identities coincide in today's workflow only because the job
checks out one tree, builds the deciding binary from it in the same job, and adjudicates
in that same checkout. That is a property of the CALLER, not of this function, and it
diverges the moment the binary is pinned or prebuilt -- precisely the cut this recording
exists to make falsifiable. Naming it for the inference rather than the observation is
the rung inflation of Sec 4b, surviving in the durable review and witness surfaces after
the run-log field had already been fixed. Raised in side-chat review.
Extended to BOTH no-op arms: "this source decided not to mutate" is exactly as
attributable an adjudication as an advance, and recording only the mutating arm would
leave the two most common outcomes unattributable.
Rung: mitigatable. The refusal is real and typed -- the wet entry point declines to
actuate when the revision cannot be observed, rather than publishing an unattributable
receipt -- but the caller-coupling is held by an annotation, not by construction.
Next-rung trigger: a self-reported embedded build revision, at which point the binary's
source stops being inferred from the adjacent checkout.
The refusal names no cause on purpose: observe_local_tree_revision returns a bare
GitObjectId?, conflating "not a git repository" with "HEAD undecodable". Splitting that
Optional is separate work and is not required for this change's correctness.
EVIDENCE (green-by-execution plus a discriminating red, both run):
green 26/26 PASS, 0 FAIL, 0 verdictless, 26 enrolled
red dropped the field from the CONVERGED arm only:
FAIL both_no_op_receipts_also_name_the_observed_judge_source
PASS the_advance_receipt_names_the_observed_judge_source_revision
PASS the_observed_judge_source_is_present_and_distinct_from_target_and_prior
PASS a_no_op_action_still_renders_a_nonempty_script
The two advance rows holding green proves the no-op row is not riding on
them; the nonempty-script control holding green proves the failure is the
missing field rather than a broken arm.
Sec 4c 0 annotation-grain diagnostics, against a compile confirmed to emit (243 files)
-- a bare grep -c zero cannot distinguish no-match from nothing-to-match.
REBASED over main after #8733 landed. That PR restructured the same decision path
(AdmissionAdvanceAuthorized -> AdmissionActionAuthorized over a three-variant coproduct),
so this change was RE-DERIVED against the new shape rather than textually merged: each
conflict hunk was a choice between two different programs, not two edits to one.
My own merged #8768 renderer fleet_desired_receipt_expected_phrase and its two creation
witnesses are NOT carried forward, and that is a rung CLIMB rather than lost work.
FleetDesiredRemoteAdvance { accepted, expected_prior } now carries the prior
structurally, so RemoteRefMustBeAbsent has no spelling in the advance arm -- the state
that renderer existed to serve is unwritable. Restoring it would have re-opened exactly
what #8733 closed. Only the evidence carries forward: the surviving
the_receipt_names_the_expected_prior_beside_the_target covers the same subject one rung up.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Residue of this branch's conflict resolution: #8733 restructured the module and already imported gunbc.fleet_desired_observe, while my side added a second clause for observe_local_tree_revision. Taking "ours" for that hunk kept both, so the module carried two import authorities for one module and named observe_fleet_desired_revision twice. Raised by review 54484 (non-blocking). Verified by execution rather than assumed, because an import edit can break resolution: 26/26 PASS, 0 FAIL, 0 verdictless, no resolve error. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…claims that said otherwise (#8824) Both paragraphs corrected here were false in the present tense, in the module that IS this repository's claim to running its own CI on the fabric. MEASURED, on main after #8733: floor_run_command 4 production consumers (the argv renderer) floor_work_contract 0 floor_execution_requirements 0 floor_offer_affordability 0 floor_buy_terms 0 floor_admission_terms 0 floor_satisfaction_requirement 0 floor_grant_duration 0 One function of ten crosses into anything outside this module, and what it renders is a shell word. CLAIM 1: "the argv ... is PRODUCED BY THE FABRIC UNDER A GRANT ... No grant, no command -- so the authorization is not a label beside the run, it is the only thing that can yield a run." `floor_run_command` is NULLARY and there is no grant anywhere on the workflow path. The sentence described a wall that does not exist. CLAIM 2: the budget ceiling is an argument "precisely so that there is no arm here that admits a floor run without clearing a price." No floor run has ever cleared a price, because `floor_offer_affordability` and `floor_buy_terms` have no caller. A fold with no consumer cannot enforce anything. WHY THIS IS WORSE THAN SITTING LOW, which is why it is a commit rather than a cleanup: a class reported at the top rung never ranks for climbing (DESIGN 4b), and a reader planning the cutover against these paragraphs would budget for extending an allocator that was never built. It cost exactly that already -- answering "where is the fabric in our CI" required measuring past this prose instead of reading it. WHAT IS TRUE, and now written: the command is DEFINED BY THE FABRIC WORK AUTHORITY and CURRENTLY TRANSPORTED BY GITHUB ACTIONS, which owns triggering, queueing, runner selection, concurrency, lifecycle, logs and check publication. AND THE WALL BELONGS SOMEWHERE ELSE THAN WHERE THAT SENTENCE PUT IT. A Grant authorizes REALIZATION OF AN ATTEMPT, not construction of a command value. Inspecting, hashing, comparing, caching or rendering a command spends no resource; executing it does. So the invariant to build toward is no committed Grant -> no process and no host effect and NOT "no grant, no command". Threading a Grant into the constructor would fuse semantic Work identity with scheduling authority and make one Work compare unequal to itself depending on whose Grant it ran under -- a defect, not a stricter version of the same idea. I proposed exactly that thread before it was refuted in review; recording the refutation beside the trigger so the next person does not re-derive the wrong boundary from the right instinct. NOTHING IS DELETED. Both folds stay -- they are the modeled decisions a broker will consume, and deleting them would delete the design rather than the overstatement. What changes is that they are described as UNCONSUMED, so the gap is countable instead of assumed closed. Two next-rung triggers named: an executor holding an ExecutionGrant against a reserved slot, and a broker fold that selects an Offer for this Demand. No behavior changes; this commit is the correction of a claim. Three rows over the module green, §4c clean. Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
… and refuse to actuate when it cannot be observed (#8797) * Record which code adjudicated the advance, and refuse to actuate when it cannot be observed The receipt named what the compare-and-swap DID (#8768: target and expected prior) and never which code DECIDED it. That fact is not recoverable from anything else the run leaves behind: the admission workflow's checkout carries no `ref:`, so on a workflow_run event it takes the DEFAULT BRANCH TIP AT RUN START rather than the triggering head_sha. J == C is therefore a timing coincidence -- it holds while main has not moved between floor completion and admission start, and #8733's bounded queue makes the divergence ordinary rather than rare, since an entry can wait while main advances and then be adjudicated by whatever main became. This is the RECORDING half only. Pinning the judge to the candidate is a separate change, ruled on separately, and deliberately lands after this one: without a recorded judge the pinning is a belief about GitHub's checkout semantics, and with it the receipts say whether J == C actually held. Recording is unconditional under either pinning, which is why it goes first. THE UNOBSERVABLE CASE REFUSES RATHER THAN FABRICATES. observe_local_tree_revision returns a bare GitObjectId?, so the run cannot distinguish "the judge is X" from "I could not tell what the judge is" -- and a receipt naming an unattributable judge is worse than no receipt. The advance therefore refuses to actuate with a typed, located reason instead of publishing an advance whose adjudicator is unknown. (That carrier's answer/ignorance conflation is real and already leaking: fleet_revision_standing renders its Absent arm as "not a git repository, or HEAD undecodable" -- an `or` in a cause string, because the carrier cannot tell the two apart. Splitting it is a separate change and is not required for this one to be correct.) WITNESSES, and the second one is here because the RED CONTROL CAUGHT IT PASSING VACUOUSLY: - the receipt names the judge, distinctly from the target and the prior - the judge operand is not the target or the prior -- which, as first written, was trivially true when the operand was DELETED ENTIRELY. It returned PASS against a receipt with no judge at all while its sibling correctly returned FAIL. It now asserts the operand is PRESENT before asserting what it is not, and fails under the same plant. RED CONTROL: removing the judge operand takes BOTH judge claims FAIL and leaves the three pre-existing receipt/lease claims PASS. The fixture uses a third distinct hex so a renderer echoing the target or the prior into the judge position cannot satisfy them. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Name what the judge operand is NOT, before pinning makes its absence misleading `ref:` on the checkout pins repository CONTENT. It does not pin the WORKFLOW TRANSPORT: for a workflow_run event GitHub requires the .yml to exist on the DEFAULT BRANCH and takes it from there regardless of the triggering branch, and GITHUB_SHA for such a run is the last commit on the default branch. Verified against the upstream reference, not inferred. WHY THIS LANDS NOW RATHER THAN WITH THE PINNING. Today, with no `ref:`, the checkout HEAD and GITHUB_SHA are THE SAME SHA -- judge and transport coincide by accident of configuration, so a receipt naming only the judge is harmless. They DIVERGE the moment the checkout is pinned to the candidate: the judge becomes the candidate while the transport stays main's. At that point a receipt carrying judge alone invites the reader to conclude every byte involved came from the candidate -- an inference that is false and, worse, UNFALSIFIABLE from the receipt itself. So the omission is named where the field would go, on the rule that an absent field reads as "not a subject". The judge is the revision of the checked-out tree this process was built from; it is not the transport, not the candidate, and not the subject the required floor judged. The full field set -- candidate, judge, required-CI receipt subject, workflow transport, the first two CHECKED equal and the transport RECORDED-not-equal -- belongs to the pinning change, because that is when the divergence exists. Shipping four fields whose values are provably identical today would land equality checks that cannot fail, which is the vacuous-claim failure the red control caught in this branch's own witness one commit ago. Annotation only; no behavior change. §4c grain checked locally: 0 `source annotation` diagnostics. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * The judge field is caller-coupled: name the condition it holds under What the read observes is the CHECKOUT's HEAD. What the receipt asserts is the provenance of the BINARY THAT DECIDED. Those are one fact only because the workflow builds that binary from that checkout inside the same job -- `cargo build --release -p v1-compiler --bin gunbc`, toolchain cache off -- which is a property of the CALLER, not of observe_local_tree_revision. Hand that job a cached, prebuilt, or externally-installed gunbc and HEAD still reports the checkout. The receipt would then name a judge that did not judge, confidently, with nothing in the receipt able to reveal it. That is the same defect this branch exists to fix, one level up: a field whose subject is narrower than its name. THE CONDITION, stated so it can be checked rather than assumed: the binary executing this decision was built, in this job, from the tree this read observes. It holds today. It is not enforced anywhere, and nothing fails if a future workflow edit breaks it. Closing it properly means the binary carrying its own build provenance rather than the run inferring it from a neighbouring checkout. Until then the field is honest evidence under a named condition, not a structural guarantee -- and a reviewer can now attack the condition instead of discovering it. Annotation only; no behavior change. §4c grain checked locally: 0 `source annotation` diagnostics. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Name the field judge-source-observed, because "judge" outruns what the run establishes "judge" asserts the identity of the BINARY THAT DECIDED. What is established is an OBSERVATION OF A SOURCE REVISION, valid under a caller condition stated one commit ago: the binary was built in this job from this checkout, no other binary was substituted, and tracked source did not change between build and decision. The prose already said that, and the prose is not where this is read. The field sits in operator-facing run-log text, so a reader sees `judge <sha>` and the qualification lives in a .dag comment they will never open. A name that outruns its evidence in the one place the evidence is consumed is rung inflation -- §4b calls that worse than sitting low, because an inflated class never ranks for climbing. It earns the stronger name when the pinning cut binds the build: observe/pin J before build, build the judge from J, re-observe before actuation, require both observations equal the candidate. An embedded self-reported build revision is stronger still and is the real terminal. Verified after the rename: both judge claims PASS, including the vacuity-guarded one. The first returned NO-VERDICT twice in batch position -- that is the 700s timeout killing a cold first run, not a defect; run alone it passes, and its sibling sharing the same fixture, pattern and module passed in the same batch, which is what rules out a compile break. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Narrow the judge claim to what the run establishes: judge-source-observed The field records the SOURCE REVISION THE ADMISSION CHECKOUT WAS SITTING ON when it adjudicated. The previous naming -- parameter `judge`, PR title "which code adjudicated the advance", refusal text "cannot record which code adjudicated it" -- claimed BINARY IDENTITY, which nothing in this repository yet establishes: no binary embeds its own source revision. Those identities coincide in today's workflow only because the job checks out one tree, builds the deciding binary from it in the same job, and adjudicates in that same checkout. That is a property of the CALLER, not of this function, and it diverges the moment the binary is pinned or prebuilt -- precisely the cut this recording exists to make falsifiable. Naming it for the inference rather than the observation is the rung inflation of Sec 4b, surviving in the durable review and witness surfaces after the run-log field had already been fixed. Raised in side-chat review. Extended to BOTH no-op arms: "this source decided not to mutate" is exactly as attributable an adjudication as an advance, and recording only the mutating arm would leave the two most common outcomes unattributable. Rung: mitigatable. The refusal is real and typed -- the wet entry point declines to actuate when the revision cannot be observed, rather than publishing an unattributable receipt -- but the caller-coupling is held by an annotation, not by construction. Next-rung trigger: a self-reported embedded build revision, at which point the binary's source stops being inferred from the adjacent checkout. The refusal names no cause on purpose: observe_local_tree_revision returns a bare GitObjectId?, conflating "not a git repository" with "HEAD undecodable". Splitting that Optional is separate work and is not required for this change's correctness. EVIDENCE (green-by-execution plus a discriminating red, both run): green 26/26 PASS, 0 FAIL, 0 verdictless, 26 enrolled red dropped the field from the CONVERGED arm only: FAIL both_no_op_receipts_also_name_the_observed_judge_source PASS the_advance_receipt_names_the_observed_judge_source_revision PASS the_observed_judge_source_is_present_and_distinct_from_target_and_prior PASS a_no_op_action_still_renders_a_nonempty_script The two advance rows holding green proves the no-op row is not riding on them; the nonempty-script control holding green proves the failure is the missing field rather than a broken arm. Sec 4c 0 annotation-grain diagnostics, against a compile confirmed to emit (243 files) -- a bare grep -c zero cannot distinguish no-match from nothing-to-match. REBASED over main after #8733 landed. That PR restructured the same decision path (AdmissionAdvanceAuthorized -> AdmissionActionAuthorized over a three-variant coproduct), so this change was RE-DERIVED against the new shape rather than textually merged: each conflict hunk was a choice between two different programs, not two edits to one. My own merged #8768 renderer fleet_desired_receipt_expected_phrase and its two creation witnesses are NOT carried forward, and that is a rung CLIMB rather than lost work. FleetDesiredRemoteAdvance { accepted, expected_prior } now carries the prior structurally, so RemoteRefMustBeAbsent has no spelling in the advance arm -- the state that renderer existed to serve is unwritable. Restoring it would have re-opened exactly what #8733 closed. Only the evidence carries forward: the surviving the_receipt_names_the_expected_prior_beside_the_target covers the same subject one rung up. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Merge the two fleet_desired_observe import clauses into one Residue of this branch's conflict resolution: #8733 restructured the module and already imported gunbc.fleet_desired_observe, while my side added a second clause for observe_local_tree_revision. Taking "ours" for that hunk kept both, so the module carried two import authorities for one module and named observe_fleet_desired_revision twice. Raised by review 54484 (non-blocking). Verified by execution rather than assumed, because an import edit can break resolution: 26/26 PASS, 0 FAIL, 0 verdictless, no resolve error. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
The desired-ref admission gate had a modelled wall and an actuator that walked around it. This makes the wall the only route, and closes a live fail-open found on
mainwhile doing it.Ready. Every gate this PR named is met, and the only thing outstanding is the operator decision above. The wet ancestry matrix landed (seven cases, 9/9 recorded and 9/9 replayed, with empty-store and wrong-hash controls). Required CI is green on the merge with main — run on
939bed4a, the commit resolving all 14 conflicts.One correction to how this PR was previously presented, since it cost real time: it was based on
fleet/accepted-revision-two-facts, notmain, so GitHub reportedMERGEABLEagainst a stale base andwitnesses.yml(which filterspull_request: branches: [main]) had never been eligible to run on it. Retargeting tomainsurfaced both at once — a genuine conflict with main, and CI. Both are now resolved, and the stack is collapsed: this branch fully contains #8720 and #8725.What this replaces, at the root
gunbc.fleet_desired_admissioncarried its own copy of workflow identity, trust checks, afloor_green: Bool, candidate decoding, and the old advance gate. #8720 and #8725 replaced all of it. Those routes are deleted, not wrapped —fleet_desired_admission_event_trusted,fleet_desired_floor_green, the old decide, and the old push renderer are gone.fleet_desired_advance_input_wetdoes not re-classify the observed ref. It routes the already-classified result offleet_desired_advance_expectation, so "absent vs unreadable vs unobserved" keeps one authority — and only the observed-current arm reaches git, so an event that produced no accepted revision can never trigger an ancestry probe.Four refusals the old wall made are preserved, two of them more strictly (the workflow is matched by path rather than name; the repository is matched against the repository authority rather than only against itself, so a fork whose head and base agree no longer passes). One refusal is new: a non-push originating event, which the old wall did not check at all.
A successful decision no longer implies a push
Two of the three authorized actions mutate nothing. Both render a nonempty script by the renderer's shape, not by remembering to echo — every arm opens
set -euand the return type isNonEmptyStr.That is load-bearing rather than tidy. The executing step's
test -sis 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.The fail-open, found on main
The
workflow_runtrigger 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 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 greenmainrevision and do nothing in its place — no advance, no refusal, no diagnostic, and acancelledrun indistinguishable from noise. Observed tally over 131 runs: 77 skipped, 45 cancelled, 6 failure, 3 success.Two fixes, answering different halves. The split is whether admissibility is decidable at the trigger grain:
branches: [main]on the triggerqueue: maxQueueing the first population would have been the absorbing fallback — it cannot compute which entries matter, so it holds them all, the deficit's frequency goes to zero by construction, and the cost is denominated in the corpus of branches. Queueing the second is not a widened container standing in for a decision; GitHub's workflow-level concurrency is structurally too early to know whether an arriving entry subsumes a pending one, so it is the honest handling of a question that layer cannot answer.
What makes the queue safe is this PR. Before forward-only, queueing every main completion would have walked the ref backward — an older admission arriving later observes the newer prior correctly, and
--force-with-leasedoes not refuse a correctly-observed overwrite. The default group's drop was accidentally protective.decide_fleet_desired_advancenow makes a superseded candidate a no-op, so every queued entry is harmless: advance, converge, no-op, or refuse.cancel-in-progress: falseis asserted separately, because it carries a different property: a running admission is never interrupted between the compare-and-swap decision and the push.Scaffold premise corrected
The dissolution row claimed no typed compare-and-swap carrier existed. #8697 falsified that.
PushRefUpdateWithLeaseis the typed wire capability — it just takesleaseandrefspecas three independentNonEmptyStrwith nothing binding them to one request, collapses a refused lease into the same nonzero-and-String as a transport failure, and has zero consumers. So the debt is the binder, a cited decoder for git's push-rejection output, and an independent readback — not a missing capability. Moving to the typed row today would trade an honestly-untyped shell for a typed call whose refusal semantics this gate cannot read.Evidence
All 21 witness rows green by execution, run individually. Two run as discriminating pairs: the branch filter goes red when
branchesis emptied, andqueue: maxgoes red when the model reverts to the default group. Restores verified by diffstat.Not claimed here
A malformed fixture in an earlier commit of this PR passed a nullary coproduct variant where a record is declared. It compiled clean and failed only at runtime with
NoSuchField. The fixture is repaired. Whether that is an ordinary-compiler-floor gap is being probed separately as minimal source specimens — no claim is made in this PR, and this PR's own model shape excludes the state regardless, since the live route constructs the record throughobserve_fleet_revision_relation.Remaining before ready
MergeBasehas nomock_response, so this needs a fixture repository. This is the last construction item.mainmerged in, and a fresh Required CI on that exact composed tree.Found and sharpened by
nimble-fox-671(three of the eviction routes) and side-chat review.