Record the observed judge-source revision on every admission receipt, and refuse to actuate when it cannot be observed

[gunbai-bot]

What this records

Every admission receipt now names the source revision the admission checkout was sitting on when it adjudicated:

[fleet-desired] admitted <candidate> expected-prior <prior> judge-source-observed <J>

on all three authorized actions — the advance and both no-ops. A no-op is also an adjudication: "this source decided not to mutate" is exactly as attributable as an advance, and recording only the mutating arm would leave the two most common outcomes unattributable.

The wet entry point refuses to actuate when that revision cannot be observed, rather than writing a receipt nobody can attribute.

What the name deliberately does NOT claim

An earlier revision of this PR called the field judge and said it recorded "which code adjudicated the advance." That outruns the evidence, and the overclaim is the interesting part:

identity	what it is	status here
C	candidate revision	admitted
F	Required CI receipt subject	structurally joined to C by acceptance
J	judge source observed	what this PR records
W	workflow transport (GITHUB_WORKFLOW_SHA)	named, not landed

What is actually established is a checkout-HEAD observation. It is not the revision of the binary that ran — nothing embeds that yet. 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 — which is exactly the cut this recording exists to make falsifiable.

So the field is named for the observation, not for the inference. The recording rung lands before pinning so that the pin has something to contradict rather than something to assume.

Rung

Mitigatable → the refusal is real and typed, 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.

Evidence

Three claims added, and the second one earned its shape:

• the_advance_receipt_names_the_observed_judge_source_revision
• the_observed_judge_source_is_present_and_distinct_from_target_and_prior
• both_no_op_receipts_also_name_the_observed_judge_source

The middle row originally asserted only the two negations. Both are satisfied vacuously by deleting the operand altogether, so it returned PASS against a receipt carrying no judge field at all while its sibling returned FAIL — a claim that could not fail for the reason it existed. Presence-before-distinctness fixes it. Caught by a deliberately-emptied receipt, not by review.

Separately, the required floor was confirmed to both enrol and discriminate on this module: a planted deliberately-false witness produced planned=10254 executed=10254 terminal=10254 passed=9946 failed=1 with the probe named in the failure. A green floor alone would have established neither.

Rebase note

Rebuilt over main after #8733 landed. The creation arm is gone — FleetDesiredRemoteAdvance { accepted, expected_prior } now carries the prior structurally, so RemoteRefMustBeAbsent has no spelling in the advance arm. My earlier fleet_desired_receipt_expected_phrase renderer and its two creation-witnesses dissolved into that shape rather than being carried forward; the surviving the_receipt_names_the_expected_prior_beside_the_target covers the same subject at a higher rung.

[gunbai-bot]

Re-derived over main — the prior approvals were given against a different program, so please re-read rather than relying on the tally.

Two things changed since the approving reviews:

1. #8733 landed underneath this. It restructured the same decision path — AdmissionAdvanceAuthorized { expected, to } became AdmissionActionAuthorized { action } over a three-variant FleetDesiredAuthorizedAction. Every conflict hunk was a choice between two different programs, not two edits to one, so I took main's shape whole and re-derived the recording on top of it.

Worth flagging explicitly: my own merged #8768 renderer fleet_desired_receipt_expected_phrase and its two creation witnesses are not carried forward. That is a rung climb, not 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, and restoring it would have re-opened exactly what #8733 closed. Only the evidence carries forward.

2. The naming was narrowed, which was the substantive review objection and it was correct. The field recorded a checkout-HEAD observation while the title, body, parameter, refusal string, and witness names all claimed "which code adjudicated." Nothing here establishes binary identity — no binary embeds its own source revision. The identities coincide today only because the job checks out one tree, builds the deciding binary from it in the same job, and adjudicates in that same checkout: a property of the caller, not of this function, and it diverges the moment the binary is pinned. That is §4b rung inflation surviving in the durable surfaces after the run-log field had already been fixed.

Now judge_source_observed / judge-source-observed throughout, and the refusal reads "the admission checkout's source revision could not be observed." It deliberately names no cause, because observe_local_tree_revision returns a bare GitObjectId? conflating "not a git repository" with "HEAD undecodable" — splitting that Optional is separate work.

Also extended to both no-op arms: "this source decided not to mutate" is as attributable as an advance, and recording only the mutating arm would leave the two most common outcomes unattributable.

Rung: mitigatable. Typed refusal is real; the caller-coupling is held by an annotation, not by construction. Next-rung trigger is a self-reported embedded build revision.

Evidence — green plus a discriminating red, both executed:

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 targeted red is doing two jobs: the advance rows holding green proves the no-op row is not riding on them, and the nonempty-script control holding green proves the failure is the missing field rather than a broken arm.

One process note against myself: my first batch run ended in | tail -35, so I read 15 of 26 verdicts and would have reported "all pass" from a truncated view. The footer's 26 witness(es) caught it. The numbers above are from an unfiltered re-run with the verdict count, FAIL list, and verdictless-witness set computed explicitly.

§4c: 0 annotation-grain diagnostics, against a compile confirmed to have emitted (243 files) — a bare grep -c zero cannot distinguish no-match from nothing-to-match.

— sent from nimble-fox-671

[gunbai-bot]

Fixed in 4b2e91d2c01 — the two clauses are merged into one and the doubled observe_fleet_desired_revision is gone.

You correctly diagnosed the cause too: it was residue of this branch's conflict resolution. #8733 restructured the module and already imported gunbc.fleet_desired_observe; my side added a second clause for observe_local_tree_revision. Taking "ours" for that hunk kept both. Re-verified by execution rather than assumed, since an import edit can break resolution — 26/26 PASS, 0 FAIL, 0 verdictless, no resolve error.

I went looking for whether the class was broader, and it is — but it is more benign than it first looked. Census over dag + src/v2: 151 files carry two import clauses for the same module, and 12 import the same symbol twice. Only one of those twelve pulls a symbol from two different module names — src/v2/extdeps/languages/lean.dag takes Empty from both std.algebra and v2.std.algebra.

That looked like a live specimen of the silent last-import-wins hole DESIGN §4b records at zero live exposure. It is not. v2.std.algebra imports Empty from std.algebra, so both paths reach one declaration — two module names, one authority via re-export. So the census corroborates the zero-exposure claim rather than refuting it, and every one of the twelve is redundancy, not ambiguity.

Worth noting the class is decidable and therefore a construction-wall candidate rather than a permanent ratchet, but at 151 sites it is its own change, not this PR's.

— sent from nimble-fox-671