Durable compare-and-set: the store owns the refusal, not a lock the caller holds

[gunbai-bot]

B needs a durable compare-and-set whose refusal arm is the store's, not a lock the caller happens to hold.

That sentence is the whole reason this lands before the GitHub poller, the allocation fold, the worker actuation, or the Check Run publisher. Every one of those is executable only under a single-process assumption the fabric explicitly rejects, and none of them can be written honestly until the commit authority exists.

Why this is not std.temporal_effect's LeaseEpoch

LeaseEpoch already carries a generation, so the obvious move is to reuse it. It is the wrong carrier, and the reason is worth stating precisely: a fencing token excludes nothing on its own. Holding generation N does not stop another writer from acting — it only lets a store reject a stale writer, and only if the store performs the check.

In gunbc.fleet_converge_plan_cli the exclusion that actually holds is flock. That is single-host by construction, so it cannot serialize two writers on different machines, which is the only configuration the fabric ever runs in. This module is the missing half: the store-side check itself.

CasGeneration is therefore deliberately distinct from LeaseEpoch.generation. They answer different questions — serial position in the canonical history versus a fence on one leased resource — and collapsing them into Int and relying on field names to keep them apart is how they get mixed at a boundary.

The two load-bearing shapes

CasExpectation = ExpectSlotAbsent | ExpectSlotGeneration { generation }. A store that encodes absence as generation 0 puts "nothing is here" and a real generation into one ordered type, so create-if-absent and update-from-0 become indistinguishable and one silently overwrites the other. Here absence is a constructor, so that conflation has no representation to be written in — not a check that catches it. Create-if-absent and update-if-unchanged are then one operation with two expectations rather than two operations.

CasOutcome has no widening arm. No "retried and assume it worked", no "proceed as if the precondition held". CasPreconditionFailed carries both the expectation and the observation, because a caller that only learns "it failed" cannot tell losing a race from addressing the wrong slot — and would retry forever against the second.

The non-present observations are three typed arms (CasSlotMalformed, CasSlotContentMissing, CasSlotReadRefused), not one arm with a detail string. They have different remedies: repair by hand, re-derive a write that did not land, retry against the store. A string discriminator puts that distinction in prose the compiler cannot see, and routes all three to whatever the caller guesses.

Critically, none of them fold into CasSlotAbsent. "The slot holds nothing" and "I could not determine what the slot holds" are different states, and rendering the second as the first is the empty-observation narrow — a writer would create a row on top of one it merely failed to read.

Evidence

Seven witnesses, run individually through gunbc run, not merely compiled.

The one that does the work is the_loser_of_a_race_can_commit_against_the_generation_that_won. Steps 1 and 2 are the race; step 3 is the discriminating one, because a store that simply wedged after any conflict would satisfy steps 1 and 2 and fail there. Generations are 7/8/9 rather than 0/1 on purpose: at low values one fixture's "next" equals another's literal, so a constant-returning arm would pass every assertion. A fixture sitting at that coincidence erases the test it appears to perform.

an_unreadable_slot_is_a_store_refusal_not_a_lost_race is the narrow-class control, paired with the_same_expectation_that_was_refused_when_unreadable_commits_when_absent so the refusal is attributable to unreadability rather than to the expectation being unsatisfiable in general.

Declared rung

range(min: 1) on CasGeneration is not enforced at compile time — the compiler reports where-refinement unenforced: predicate deferred. A generation of zero or below is writable, and this carrier sits at mitigatable for that class. Next-rung trigger: refinement enforcement on branded carriers.

What is not deferred, and is the actual structural claim: the absent-versus-present distinction, which has no representation to get wrong regardless of refinement.

A substrate finding, filed not worked around

docs/plans/branded-carrier-construction-finding.md records that a branded carrier can compile with 0 blocking errors and refuse at evaluation — including cannot cast Int to Int, and including a declaration containing no cast at all. It carries an executed 2x2 matrix, two positive controls (one of them existing corpus code), and three hypotheses I stated and then falsified, kept deliberately.

The module uses field-position literals, the corpus idiom, and keeps the brand. Dropping CasGeneration to a plain Int would have made every error vanish while deleting the distinction the type exists to carry — the author-side absorbing fallback, which is the line-stop signal rather than a landing state.

Not in scope

No store realization, no poller, no outbox. This is the interface and its decision fold; a transport is a Realization handler bound to it, never fused into it.

Two open questions I owe the design thread rather than resolving unilaterally: its FabricStateGeneration uses range(min: 0) to encode genesis, which re-introduces exactly the absent-as-zero conflation ExpectSlotAbsent removes; and its FabricHeadRead and this CasSlotObservation are the same coproduct under two names — one has to go, or the first carrier B lands violates single authority.

[gunbai-bot]

Both taken. The first is fixed by narrowing, not checking; the second resolves in this PR, and the resolution is that there is nothing to delete.

ITEM 1 — accepted, and it was worse than reported. cas_expectation_admits had the same defect: three unreadable arms answering false, which reports an absence of evidence as a lost race. So the narrow appeared twice in the module, and the caller-ordering argument covered both.

The fix is the first option:

type CasReadableSlot
= CasReadableAbsent
| CasReadablePresent { version: CasSlotVersion }

cas_expectation_admits and cas_committed_generation now take CasReadableSlot. The unreadable arms are deleted rather than handled. cas_decide performs the classification as a type transition into a new cas_decide_readable, so the ordering that used to be a convention is now the only way to obtain the argument.

I also removed the _ wildcard from cas_decide while in there. It was not in your report and it is the same class one level up: a wildcard silently absorbs any observation arm added later, so the next variant would have been swallowed into the commit path instead of refused. Both readable arms are explicit now.

RUNG: the class moves from mitigatable-by-caller-ordering to structurally impossible for the helpers. There is deliberately no new witness, because no test can construct the bad input — that is the point of the climb. The seven existing witnesses stay enrolled as regression controls per 4b's dissolution-on-climb, which deletes production machinery and never the evidence.

Re-verified after the restructure rather than assuming: 7/7 witnesses green, and the mutation control re-run against the NEW shape (a control that passed against the old one proves nothing about this one).

ITEM 2 — resolved, and the answer is that no duplicate exists. I grepped dag/ and src/ for FabricHeadRead, FabricStateHead and FabricStateGeneration. Zero hits. They are proposals in the design thread, not code. So this is not a nickname in the corpus and there is no second authority to delete.

The resolution therefore runs forward, and I am stating it so it binds rather than leaving it to be rediscovered: CasSlotObservation is the surviving authority for "what the store found", and FabricHeadRead must not be authored as a second coproduct over the same question. If the store realization needs a head-read type, it uses this one.

One thing I will not silently accept from the thread's sketch, because it contradicts the fix above: FabricStateGeneration is specified as range(min: 0) with genesis encoded as zero. That is exactly the absent-as-zero conflation ExpectSlotAbsent exists to remove — it puts "no state yet" and a real generation into one ordered type. If a fabric head type is authored later it must carry absence as a constructor. Mine starts at 1 for that reason.

Agreed on the inherited red — not chasing it. Worth noting 4caaa6f lands as #8652 (fix/regen-v1-emit-rust-mirror), which is MERGEABLE/CLEAN and regenerates 17 mirrors including v1_compiler_emit_rust.rs. It unblocks main and four of my PRs in one merge, and duplicating it on my branch would create a competing authority for generated bytes.

[gunbai-bot]

The failing check is inherited from main and cannot be fixed on this branch

Re-verified at head e8c4bf5, not restated from an earlier check.

The failure is one line:

required-regen: planned=129 executed=129 first_generation_equal=false
required-regen: FAIL generated surface drift: v1_compiler_emit_rust.rs

That step compares 129 generated mirrors against their .dag authorities. One mirror is stale because #8614 landed a change to src/v1/05_emit_rust.dag without regenerating it, and #8618 had just re-armed the fixed-point check. main itself is red on the identical step at 4cec10f66.

This PR's own contribution is clean. The floor fold ran planned=9790 executed=9790 terminal=9790 passed=9482 known_red_held=308 failed=0 — exactly at parity with the previous head, and +7/+7 against the main-derived baseline, which is precisely the seven witnesses this PR adds. None of its three files is in the regen surface.

Regenerating the mirror here would be actively harmful. #8652 (fix/regen-v1-emit-rust-mirror) already carries the converged regeneration of all 17 drifted mirrors and is MERGEABLE/CLEAN. A second set of generated bytes for the same artifact is a competing authority — and the generated-artifact merge driver refuses rather than taking a side, so the two branches would collide in the one place a conflict cannot be hand-resolved.

Merging #8652 clears main, this PR, #8629 and #8641 together. There is no branch-local fix.

— sent from silent-bear-842

[gunbai-bot]

Correction: I claimed construction for a property this module does not have

In an earlier comment I wrote that deleting the observation-side key means "an observation is of the slot the attempt names, because no other slot can be described." The first half is right and the second does not follow. Retracting it here because I asserted it publicly, and because this module is meant to become the authority other durable-fabric work builds on — a wrong claim in it propagates further than a missing feature.

What was actually true

Deleting the duplicated key closed the disagreement between two copies of one fact. I then asserted it closed the relation between the observation and the attempt. Those are different propositions and only the first followed.

An unkeyed observation describes no slot, which is not the same as describing the slot. cas_decide_readable never reads attempt.key, so this remains writable:

attempt    key = A, expected generation 7
readable   actually read from slot B, generation 7
           -> generations agree -> COMMITS to A

Deleting the key removed the evidence of a mismatch, not its possibility. Unobservable is not unconstructible. And it is weaker in one specific respect than what preceded it: while two copies existed a refusal arm could have caught the disagreement; now nothing can.

The deletion itself was still correct — two writable copies that cas_decide never compared was a live wrong-slot commit path. The error is in what I claimed the deletion bought.

The sharpest form of the refutation, which I had the evidence for and missed: the existence of CasAttempt.key is itself the proof that the guarantee is not free. "Only one slot can be described" would hold only for a store with exactly one global slot — and such a store would not need the field. My own type refutes my own comment.

What changed in this push

1. The comment is corrected in place, keeping both the original reasoning and why it fails, rather than quietly replacing it.
2. The key relation is declared outside the modeled guarantee, exactly parallel to the content/digest obligation already in the file — sole_constructor as the candidate wall, and the sealing shape named: compare_and_set(attempt) -> CasOutcome with the store reading attempt.key itself, or a store-minted bound observation callers cannot forge.
3. A discriminating control is enrolled while the defect is still constructible: the_decision_is_invariant_under_the_attempt_key asserts that two attempts differing only in slot produce identical outcomes. That is the defect, made executable instead of left as prose.

That witness is written to fail loudly at the right moment: when a bound observation makes the pairing unformable, it must stop compiling. That is the signal the relation was sealed, and it then dissolves into the construction evidence under the same §4b rule that retired the helpers' unreadable arms.

Its header states explicitly that a green there is not a safety claim — it is the receipt for a declared gap. Otherwise it would read as evidence for the very property it documents the absence of.

Rung, restated honestly

The narrowing of the decision helpers stands and remains a real climb to structurally impossible. The observation-to-slot relation is not part of it: that sits at outside the modeled guarantee, observed and refused at the store boundary, never proven here.

— sent from silent-bear-842