Region HA 1b-next: Relocation, Row Cases, Create Choice and Fences Implementation Plan (rev 19)

> For agentic workers: REQUIRED SUB-SKILL: Use superpowers:subagent-driven-development (recommended) or superpowers:executing-plans to implement this plan task-by-task. Steps use checkbox (- [ ]) syntax for tracking.

Goal: Build what region HA spec 1 had to leave until the host lifecycle claim was on main: the relocating operation within one region, released by the source's stop evidence (drain) or by its termination fence (failover); reconcile's row cases for it; create's once-only choice of executor box with boxchoice.Choose; and every claim CAS that consumes a termination fence. All of it dormant behind CARLOS_REGION_HA, and none of it mergeable until the joint two-box simulation round passes (L18).

Architecture: Two stages (ruling 24). Stage A, build now: Tasks 1 to 7 and 9a, buildable on main today and dry-run on every revision: the claim library's relocation transitions and released coverage (internal/hostclaim), create's executor selection (internal/hostclaim, internal/hostops), the row and wake decisions (internal/hostbox), the writers-stopped observation (internal/stopevidence), the regional worker and the participant driver (new internal/hostrelocate), and the box-side release adapter with its receipt verifier (internal/host). Stage B, gated: Tasks 8a, 8b, 8c, 9 and 10 bind to claim Plan 6b and moves Plans 1 and 2, none merged. They keep their design and contracts here; their code is rewritten against the real 6b code after it merges and re-reviewed then (the "Stage B re-plan" step before Task 8a lists every obligation rounds 1 to 15 placed on them). What those need and no plan declares is a numbered request, never an assumption. The last task is the merge gate. The worker only reads termination fences: hostfence.TerminationWorker writes them, and hostactors.Directory is the only roster reader.

Tech Stack: Go 1.26, module github.com/carlosframework/platform; release.Store (create-only and ETag compare-and-swap puts); the claim library (hostclaim), roster (hostactors), fences (hostfence, termfence), box choice (boxchoice), files (hostfiles), generation selection (genselect), stop evidence (stopevidence, internal/host stop receipts), execution controller (hostexec).

Spec: docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md, rev 5.4 with §24 (rulings H1 to H19 final). Read §0, §2, §5.2, §5.3, §5.8, §5.9, §5.10, §9 (L1 to L20, accepted) and §24 first. Then the claim spec rev 6.30 on origin/design-replica-ownership (docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md): §1.1's activation gate, §4 ("Same-region relocation (L1)" and the relocation exception to CC11), §5.1 and P5-D2/P5-D6 (the create intent), §6.1 ("Release before full stop (L10)"), §6.4a item 2 (released), §7.3 D2 ("Automatic termination (L2, L4)", "The fence's journal reference") and D4 ("Automatic loss persistence"). Then moves rev 7.22 on origin/design-moves-any-region §7.6 ("One install routine, two sources", L16 and L17) and §7.10 (the pre-flip conversion). The contracts note docs/superpowers/notes/2026-10-07-region-ha-contracts.md gives hostfiles v2, CopyManifest, Publish and boxchoice. Plan 1b (docs/superpowers/plans/2026-10-06-region-ha-1b-claim-readers.md) lists in "Waits for the claim" what this plan now builds.

Rev 19: round 18 dispositions

Astra's round 18 (CODEX-PLAN-REGION-HA-1BN-R18.md) resolved all three round 17 findings, accepted rulings 1 to 27, and raised two P2 test gaps. Both were checked against the plan's tests and accepted; none is declined. Neither exposed a production defect: the new events and oracle found no failing seed in the unchanged code. Stage A was dry-run on a clean 3407d114 in task order. The lifecycle property passed 200 seeds, niced, and then each lifecycle guard was removed in turn.

| # | Stage | Evidence checked | Disposition | What changed | Where | |---|---|---|---|---|---| | 1 (P2) | A | The property's events only started and completed operations. Its recovery oracle wanted every relocation to be ready again on this box. So it could not express a box excluded from an operation that goes on, and it would have rejected correct recovery there. | accepted | New events: replaced (this box, the target, is replaced within the same operation by sp2, and the relocation continues) and probeFailedAndReleased. In every fourth seed, a script follows round 18's trace: target installed, probe fails, release journaled, replaced, cleanup blocked, a pass, an agent crash, then the random events and recovery. The oracle now asks a participating box to be ready, and an excluded box to have finished its cleanup: no controller, no hostexec record, no journaled participation, with the operation still running. New invariant (i): nothing for an operation opens again on a box excluded from it. Invariants (a), cleanup before clear, and (h), persistence across a crash, stay. | Task 7 (TestRelocationControllerLifecycleProperties) | | 2 (P2) | A | TestExecutorChooserSpreadsThenBalancesThenHashes took the first choice as given and derived its later expectations from it. A chooser that hashed a constant instead of the record's host passed. | accepted | TestExecutorChooserHashesTheRecordsHostOnEqualLoads uses equal loads. It computes the winner independently (the greatest SHA-256 of host + "\x00" + box id, claim P5-D2) for shop.bab.oncarlos.com (box-b) and cafe.bab.oncarlos.com (box-a). The test itself asserts that the two winners differ, and requires Choose to return each one. Substituting a constant hostname in ExecutorChooser.Choose fails it (cafe chose box-b). | Task 2 |

Mutation check (property at 200 seeds, -failfast): Sweep finishing a participation whose box is excluded, killed at seed 4 (the excluded box never finishes its cleanup). Rev 14's guards, rechecked under the new events, were all killed again: the cleanup before a clear (seed 1, (a)), the verified forget (seed 3, (b)), lost-controller recovery (seed 10), the journal before the open (seed 1, (b)), the close before the clear (seed 6), and the restart path's verification (seed 1, (b)).

Rev 18: round 17 dispositions

Astra's round 17 (CODEX-PLAN-REGION-HA-1BN-R17.md) rated F1 to F3 as only partly closed, with one P1 and two P2s. It accepted ruling 26 and its cost. All three findings were checked against the rev 17 code, reproduced, and accepted; none is declined.

Stage A was dry-run on a clean 3407d114 in task order, and the lifecycle property passed 200 seeds, niced. Each new guard was removed in turn, and each removal failed its test.

| # | Stage | Evidence checked | Disposition | What changed | Where | |---|---|---|---|---|---| | 1 (P1, F2) | A, spec | Rev 17's filesPin returned the first manifest it found before checking any evidence. §5.6's pre-start copy can lack the instance.key the app mints after starting, so a nonempty database was pinned with no key. | accepted | Pin computes needKey: a writer was admitted and the pinned database is nonempty. filesPin then refuses with ErrFilesUnevidenced unless the pinned manifest has a live instance.key entry (InstanceKeyPath, liveEntry), and the worker marks the operation stuck (rev 17's path). Ruling 25 is amended. The durability window is recorded as the open request L21, with both candidate contracts, for Paul. | Task 5 (TestStorePinnerRefusesAKeylessManifestForANonemptyDatabase: keyless with a nonempty database refuses; keyed pins; keyless with an empty database at a release of 0 pins); Requests (L21) | | 2 (P2, F1) | A | Worker.Step sends a fenced target to replace before any phase check. replace returned the chooser's error for ever, so a target terminated after its release, with no spare, bypassed rev 17's bound. | accepted | New fence-consuming hostclaim.FenceTargetWithoutSpare, sharing FenceExhaustedTarget's body (fenceTargetStuck): it retains the loss, puts the box on lost, revokes a dead executor and records stuck with its reason. replace calls it ReleaseDeadline after the fence's observed_at when no eligible box exists. | Task 1; Task 5 (TestWorkerBoundsAProbeFailedWithNoSpare/target_terminated_after_its_release_true: waiting before the deadline; after it, stuck with the fence consumed, dst lost and op.exec "none") | | 3 (P2, F3) | A | ReplaceTarget's default branch (probe-failed, or after P's admission) deleted prepared without recording an unopened P. That happens when the probe deadline passes before any admission and the target is then terminated. | accepted | abandonPrepared(c) records the current P when no writer opened it. install and ReplaceTarget's default branch call it before they replace or drop P. FenceExhaustedTarget and FenceTargetWithoutSpare keep an unopened P for the operator, so they drop nothing. | Task 1 (TestRelocationParksAPDroppedFromProbeFailed: probe deadline before admission, target terminated, replaced, nested relocation completed; P1 is parked) |

Guards removed, each failing its test: the keyless refusal; needKey only for a nonempty database; the dead-target bound; the bound consuming the fence; ReplaceTarget recording the P it drops. That is five.

Rev 17: two-box model findings

The joint model (origin/region-ha-hostlife-two-box, model plan rev 2 at 6d25c54e) reported three gaps in rev 16 that review rounds 1 to 16 missed. Each comes with a direct test (TestFailoverBeforeTheFirstManifest, TestProbeFailedInATwoBoxRegion, TestAbandonedPreparedGenerationParked). I checked each against this plan's code first, and all three reproduce. All are accepted; none is declined.

Stage A was dry-run on a clean 3407d114 in task order. The lifecycle property passed its 200 seeds, niced. Each new guard was removed in turn, and each removal failed its test.

| # | Stage | Evidence checked | Disposition | What changed | Where | |---|---|---|---|---|---| | F2 (data loss) | A, B | StorePinner.filesPin pinned an empty files set whenever no manifest existed in the admitted chain, whatever the holder's writer history. An install from it starts with no instance.key, and the app mints a new one over data sealed with the old (model INV-4). | accepted (ruling 25) | filesPin refuses with ErrFilesUnevidenced unless no writer was ever admitted (session 0) or the journaled release flushed nothing (manifest_seq 0). Worker.pinUnderLease marks the operation stuck on that error. Stage B: 6b's cold admission writes its manifest copy before the app starts (§5.6), with a named test. | Task 5 (TestStorePinnerRefusesAnEmptyFilesPinAfterAWriter, TestStorePinnerPinsEmptyOnlyWithEvidence, TestWorkerMarksAnUnevidencedFilesPinStuck); stage B re-plan | | F1 (liveness) | A | In probe-failed with the release journaled, Worker.Step returned the chooser's error forever ("a later pass may find one"). With two boxes no spare exists, and replaceTargetSlot refuses the source. | accepted (ruling 26: stuck, not the source) | ReleaseDeadline after probe_failed_since with still no eligible box, the worker marks the operation stuck. Before that it waits as before. | Task 5 (TestWorkerBoundsAProbeFailedWithNoSpare: waiting before the deadline, stuck after it) | | F3 (leak) | A | CompleteRelocation queued park-local chores only. A P replaced while unopened (at installing, or a deadline probe-failed before any admission) stayed in holder.location for the at-rest sweep alone. | accepted (ruling 27) | install journals every unopened P it replaces in abandoned_prepared. The serving CAS queues a park-generation for each in the region (Owner region:<r>), deduplicated, never for an opened P. | Task 1 (TestRelocationParksEveryAbandonedPreparedGeneration: replaced at installing, completed on P2. P1 is parked and P2 is not.) |

Guards removed, each failing its test: install journaling the abandoned P; the serving CAS queuing its park; the opened-P exclusion; filesPin's refusal; the release-evidence exception; the worker's stuck on ErrFilesUnevidenced; the probe-failed bound; and waiting before the bound. That is eight.

Checked and unchanged: a target terminated with no spare in starting or releasing also waits for a spare. The live source still serves there (it is op.exec until its admission fence closes), so that is not an outage. The model's finding is the probe-failed case only.

Rev 16: round 15 dispositions

Astra's round 15 (CODEX-PLAN-REGION-HA-1BN-R15.md) resolved all four round 14 items and raised two P2s. I checked both against spec §5.8 (line 847, "a box that finds its receipt missing after that point … the op goes to stuck") and against the rev 15 property code. Both are accepted; none is declined.

Stage A was dry-run on a clean 3407d114 in task order. The lifecycle property passed 200 seeds, niced, in about four and a half minutes. Each new guard was then removed in turn.

| # | Stage | Evidence checked | Disposition | What changed | Where | |---|---|---|---|---|---| | 1 (P2) | A, B | Rev 15's Step called EnsureLocal only while P was unopened. After P opened it went straight to the next attempt, so a lost receipt never made the operation stuck as §5.8 requires. | accepted | Receipt verification is now separate from restoration. A new effect, VerifyReceipt, runs before every attempt once P is opened. It compares this box's durable receipt (the new Receipt provider: the install journal under its install_stamp) with the journaled local_install, and reads nothing else. If the receipt is missing or different, Step marks the operation stuck (MarkStuck, allowed in probing once P is opened) and makes no admission and no reinstall. Files, env and timers changed by the admitted writers are never compared or reverted. Stage B: the production Receipt, with named tests. | Task 6 (TestAParticipantIsStuckWhenItsReceiptIsLostAfterPOpens: P is opened and the agent restarts. With the receipt lost, the claim goes stuck and no admission follows. With it intact, the next attempt goes ahead and nothing is reinstalled or verified against content.) Task 7 (TestVerifyReceiptChecksTheReceiptOnly). Stage B re-plan | | 2 (P2) | A | Rev 15's restart repaired the faults it was meant to survive: it unblocked and un-failed the cleanup, and closed the old controllers in the background, so their hooks ran. | accepted | restart becomes crash, an abrupt death. No controller is closed and no hook runs or completes. A dead generation's cleanups, including ones waiting when it died, never return. Its clock never fires again, and the next generation uses fresh lock files: the kernel releases a dead process's locks. Durable records and every external fault persist; recovery stays its own later event. New invariant (h): a record goes only through a successful clear or a successor's open over it, never through a crash or any other step, and while a record exists root's §5.10 check refuses an executable update. | Task 7 (the property, 200 seeds) | | C1 | A | Found by the new crash event. In-process, a dead generation's hostexec goroutines still run: publish retries its "lost" write through a directory fd it already holds open. After a repair it recreated a record a live generation had just cleared (seed 75). | fixed in the test | Each generation reaches the data directory through its own symlink, and a crash removes the dead one, so newly opened paths fail. The repair waits 300 ms so a write already in flight through an open fd lands as part of the repair. A real dead process writes nothing, so production code is unchanged. | Task 7 (the property's dataLink, recoverAll) |

Mutation check, with the property at 200 seeds and -failfast, plus targeted tests:

| Guard removed | Result | |---|---| | Step marking stuck on a lost receipt after P opens | killed: TestAParticipantIsStuck… | | VerifyReceipt comparing the receipt exactly | killed: TestVerifyReceiptChecksTheReceiptOnly | | both EnsureLocal calls | killed, seed 182: (e) | | EnsureLocal before an attempt alone / before entering probing alone | each survived: the other covers it | | rev 14's ten lifecycle guards | all killed again; the crash event now kills "journal before the open" at (b) and the handover at (h) |

While building C1 I also tried an in-flight-open guard: no forgetting while an abandoned open might still write. It survived 200 seeds, so I removed it. ClearStale already refuses while such an open holds the host's lock, and recordIsMine refuses on anything unclear.

Astra's readings of rulings 1 to 24 stand.

Rev 15: round 14 dispositions

Astra's round 14 (CODEX-PLAN-REGION-HA-1BN-R14.md) resolved the lease-recovery finding. It left round 13's finding 2 partly resolved and raised three new P2s. All four are accepted; none is declined.

Stage A was dry-run again on a clean 3407d114, applied in task order. The lifecycle property passed its 200 seeds (about three minutes, niced) and was re-run for every mutation. Each new guard was removed in turn; the results are below.

| # | Stage | Evidence checked | Disposition | What changed | Where | |---|---|---|---|---|---| | R13-2 (partly) | A | Rev 14's recordIsMine decoded the JSON itself. A parseable record without its enrollment or incarnation, which hostexec's own reader refuses (State.validate, Binding.valid), was taken for another binding, and the participation was forgotten. | accepted | New hostexec.ReadLocal(dataDir, host) (internal/hostexec/readlocal.go) is hostexec's validated reader: the same checks Open, CheckLocal and ClearStale apply. recordIsMine uses it. Only an absent record, or a valid record of another binding, is "not mine"; anything hostexec refuses is an error, and the participation is kept. | Task 7 (TestARecordHostexecRefusesKeepsItsParticipation, for a missing enrollment and a missing incarnation: refused and kept, still kept after a restart, then the record is repaired and a cleanup and clear succeed) | | 1 (P2) | A, B | Claim rev 6.30 R18-1 and moves rev 7.22 §7.6 require the same thing: a create-only prepared manifest at sequence 0, bound to {location, P, op id, installation stamp}. The first admission consumes it by exact version, and the session publisher starts at sequence 1. Rev 14's ToInstalled required P's sequence to equal the pin's, and CopyPinnedManifest kept the source's sequence. | accepted | CopyPinnedManifest writes P's prepared manifest at sequence 0, keeping the pinned entries by their content-addressed objects. PreparedAuthority separates the manifest's identity from its provenance: FilesSeq must be 0, SourceFilesSeq must be the pin's sequence, and InstallStamp is bound by ToInstalled from install_stamp. Ruling 13 is corrected. Stage B: R1 has the first admission consume that manifest by its journaled digest as the publisher's baseline, and the re-plan names the tests. | Task 1 (TestRelocationPreparedManifestIsSequenceZero: a prepared manifest claimed at the source's sequence 7 is refused, one built from another source revision is refused, and the accepted one is bound to the stamp); Task 5 (TestPreparedManifestIsSequenceZeroAndTheSessionPublishesOne: source at 7, prepared at 0, first session publication at 1, inherited entries intact); stage B re-plan | | 2 (P2) | A, B | Step in installed with local_install journaled went straight to probing. Nothing checked that the install still existed after a lost lease's scoped cleanup retired the unopened P's local install. The property never reached installation. | accepted | hostrelocate.Effects.EnsureLocal runs before probing and before every attempt until P is opened. host.RelocationEffects.EnsureLocal verifies the receipt's install (VerifyLocal). If the install is retired, it restores it with the same Install under the same install_stamp, refuses a restore that is not the receipt's, and verifies again. It never touches an opened P. The property now also covers the target's role: half the seeds start with the local install journaled, and a new event hands the installation to this box. Its effects are stateful: Install makes the install, the scoped cleanup retires it unless P is opened, and Admit opens P. Two invariants are added: (f) P's first admission never meets a missing local install, and (g) an opened P is never reinstalled. Stage B: the production VerifyLocal and restore, with named tests. | Task 6 (TestAParticipantRestoresARetiredLocalInstallBeforeTheFirstAdmission), Task 7 (TestEnsureLocalRestoresARetiredInstallOnlyBeforePOpens, the property), stage B re-plan | | 3 (P2) | B | 6b's runtime.Prerequisites returns ClaimDependencyError for any probe or non-serving claim (6b plan, if p.Probe \|\| o.Claim.Op.Kind != hostclaim.KindServing). So a source that claim §4 and Task 1 let wake in starting and releasing could not, even after R1. | accepted (contract) | R1 now also asks for the source's cold-admission dispatch in starting and releasing while its admission fence is open, refused once the fence closes or the claim no longer names the box. A target's ordinary wake stays refused. The stage B checklist names the tests. | Requests (R1), stage B re-plan |

Mutation check, with the lifecycle property at 200 seeds and -failfast, plus targeted tests:

| Guard removed | Result | |---|---| | both EnsureLocal calls | killed, seed 32: (f) | | EnsureLocal before an attempt while P is unopened | killed, seed 142: (f) | | EnsureLocal before entering probing | survived: the attempt-time check covers it (defence in depth) | | EnsureLocal restoring a retired install / refusing a restore under another stamp | killed: TestEnsureLocal… | | recordIsMine through hostexec.ReadLocal | killed: TestARecordHostexecRefusesKeepsItsParticipation | | recordIsMine comparing the binding | killed, seed 3: (b) | | ToInstalled requiring sequence 0 / the pinned source sequence / binding the stamp | killed: TestRelocationPreparedManifestIsSequenceZero (each) | | CopyPinnedManifest writing sequence 0 | killed: TestCopyPinnedManifestEnforcesThePin | | rev 14's lifecycle guards (finish's cleanup before a clear, verified forget, lost recovery, bounded open, journal before open, handover, close before clear, ErrInactive superseded, verified restart forget) | all killed again (seeds 2 to 46) |

The EnsureLocal short-circuit for an opened P also survives, because the participant never calls EnsureLocal once P is opened. It is kept so the effect is safe on its own.

Astra's readings of rulings 1 to 24 stand. Ruling 13 is corrected as finding 1 requires.

Rev 14: round 13 dispositions

Astra's round 13 (CODEX-PLAN-REGION-HA-1BN-R13.md) resolved both findings from round 12 and raised two P2s, both in the execution-controller lifecycle. Both are accepted; none is declined. This is the sixth round in a row to find a controller cleanup or recovery interleaving (rounds 2, 4, 5, 6, 12 and 13). So rev 14 also closes the whole class with a property test over real hostexec controllers, not only the two examples.

The changes were dry-run on a clean 3407d114 with stage A applied in task order, building, vetting and running each task's tests after it, plus vet for darwin and windows and the cross-builds. The property test ran its 200 seeds niced, in about three minutes. Each lifecycle guard was then removed in turn (mutation check); the results are below.

| # | Stage | Evidence checked | Disposition | What changed | Where | |---|---|---|---|---|---| | 1 (P2) | A | One failed lease put makes hostexec latch the controller lost (controller.go, run: loseLocked(putErr)), and a lost controller never becomes ready again. Rev 13's Ready reported the error and kept the controller, Step reopens only a missing one, and Sweep keeps a running operation's controller. A transient storage fault in installing therefore stalled the relocation until the agent restarted. | accepted | RelocationControllers.live, used by Ready and Acknowledge, recovers within the same operation. If the open controller has lost its lease (Lost() is closed, newly on RelocationController), it is joined (Close, bounded by the pass) and the scoped cleanup is repeated. The object is then forgotten, but its journal entry is kept. Ready reports ErrNoController, and the participant's Acknowledge opens a fresh controller with fresh authority and its own lease. The claim keeps the first acknowledgement, as after a restart (rev 2, finding 10). The record on disk stays lost until the fresh controller replaces it, so denial is durable throughout. A failed join or cleanup keeps the lost controller, and the next pass repeats both. | Task 7 (TestRelocationAcknowledgeRetainsTheControllerUnderTheAgentLifetime: lost lease, cleanup failing, then recovered and reopened, no restart); the property test | | 2 (P2) | A | ClearStale returns ErrState for an absent or invalid claim (controller.go:619) and for an unreadable or mismatched local record, as well as for a record that names another binding. Rev 13's finish treated every ErrState as replacement and forgot the participation while this binding's record stayed. | accepted | finish no longer reads anything into the error. It asks the record itself (recordIsMine: <DataDir>/.hostexec/<host>.json, compared on box, enrollment, incarnation and operation, as ClearStale compares them). The participation is forgotten only when the record is absent or names another binding. An unreadable record, or this binding's record, keeps the participation and reports the error. RelocationControllers.DataDir is new; production sets it to the assembly's Guard.DataDir, and with it empty nothing is ever forgotten on a failed clear. | Task 7; the property test (claim read failure, absent claim, invalid local record, then restart and recovery) | | C1 | A | The class. | added | TestRelocationControllerLifecycleProperties (internal/host/relocationlifecycle_linux_test.go) runs over real hostexec controllers, a store that injects faults, and a clock the test drives. Each seed runs 30 random events: lease-renewal failure, a close that times out (a cleanup that blocks), cleanup failure, ClearStale failing for each of its causes (claim unreadable, claim absent, invalid local record, a successor that lists this box), agent restart, a successor starting before the sweep, completion, and recovery of the storage. Participant passes are the real Participant.Step and Sweep. After every step it asserts: (a) no clear without a successful scoped cleanup earlier in the same call; (b) no participation forgotten while its record exists; (c) at most one controller per host; (d) no pass past its deadline. Then (e), liveness: once faults stop, within eight passes the running relocation is ready again; after completion every record is cleared, no controller remains, and a new relocation opens. 200 seeds by default, 20 with -short. | Task 7 | | C2 | A | Found while building C1. hostexec.Open waits for its Cleanup hook without a context (err = <-cleaned), so rev 13's openBounded, which waited for Open to return, did not bound a pass whose cleanup blocks. | fixed | openBounded runs the open apart and returns when the pass's context ends. A controller that opens too late is closed, never kept. | Task 7; invariant (d) | | C3 | A | Found while building C1. After a handover, sweeping the predecessor called ClearStale while the successor's live controller held the host's lock, which waited out the whole pass. | fixed | With no controller object, finish reads the record first. If it is verifiably not this binding's (absent, or the successor's), the participation is forgotten without a clear: nothing of its own is left to clear. The handover no longer forgets superseded entries itself; the next sweep does, through that check. | Task 7 (TestASuccessorRelocationRetiresItsPredecessorsController now sweeps A after the handover) | | C4 | A | Found by the in-order dry run. TestProcessDescriptorsTellsSharedFromUnsharedThreadsByKernelIdentity (rev 7) failed about once in five full-package runs. Main's TestFDHoldersUnsharedThread can run its unshare on the leader thread, which then keeps a private table for the rest of the process, so no thread shares the leader's. | fixed | The real-kernel test re-executes the test binary and runs in a fresh process. Its guards still fail it (the KCMP_FILES check was rechecked). | Task 4 |

Mutation check: each lifecycle guard was removed in turn, and the property test was run with -failfast.

| Guard removed | Result | |---|---| | finish repeating the scoped cleanup before a clear | killed, seed 1: invariant (a) | | finish forgetting only a verified other binding | killed, seed 3: invariant (b) | | live recovering a lost controller | killed, seed 13: invariant (e) (the relocation never recovers) | | openBounded | killed: invariant (d) (a pass never returns) | | the journal written before the open | killed, seed 3: invariant (b) | | the handover before a successor opens | killed, seed 53: invariant (e) | | finish closing before the clear | killed, seed 2: invariant (e) (never clean) | | recordIsMine comparing the binding | killed, seed 3: invariant (b) | | a handover treating hostexec's ErrInactive as superseded | killed, seed 7: invariant (e) | | the restart path verifying the record before forgetting | killed, seed 3: invariant (b) | | live repeating the scoped cleanup before the reopen | survived 200 seeds |

The survivor is defence in depth, not a load-bearing guard. hostexec.Open runs the controller's Cleanup hook, which is the same scoped relocationCleanup (Task 8a), and fails if the cleanup fails. So no fresh controller, and no fresh authority, exists without a successful cleanup, and invariant (a) is about clears, which recovery never makes. The explicit cleanup is kept so that a failure surfaces at the pass that notices the loss.

Astra's readings of rulings 1 to 24 stand. Rev 13's statement that the predecessor's entry is removed "once the successor's open succeeds" is replaced by C3.

Rev 13: round 12 dispositions

Astra's round 12 (CODEX-PLAN-REGION-HA-1BN-R12.md) resolved the file-origin finding and raised two P2s. Both are accepted; none is declined. Finding 1 is stage A code. It was dry-run on a clean 3407d114 with stage A applied in task order, building and running each task's tests after it, plus vet for darwin and windows and the cross-builds. Four new guards were removed in turn, and each removal failed its test (listed in the Self-review). Finding 2 is a stage B contract and has no code.

| # | Stage | Evidence checked | Disposition | What changed | Where | |---|---|---|---|---|---| | 1 (P2) | A | Rev 12's Acknowledge looked controllers up by host and operation, and opened a missing one under e.Lifetime. hostexec.Open loops on ErrControllerBusy until its context ends (controller.go, Open), and a predecessor's controller keeps the host's lifetime lock until Close. ClearStale refuses with ErrInactive whenever the running operation lists this box, whatever its id (controller.go:643). The regression reproduces it: without the handover, B's acknowledgement waits out the whole pass. | accepted | Before opening a successor's controller, Acknowledge calls RelocationControllers.handover. It retires every other participation of the same host under the pass's context: close, then the repeated scoped cleanup, then the clear. A clear refused with ErrInactive because the successor lists this box counts as superseded. The lock is free by then, and the successor's Open replaces the record under it; the predecessor's journal entry is removed only once that open succeeds. A clear that finds another binding's record (ErrState) means this participation has no record left. The open itself is bounded by openBounded: the controller still lives under the agent's lifetime, but waits for the lock no longer than the pass. A controller that opens in the same instant the pass ends is closed, never kept with a cancelled life. | Task 7 (TestASuccessorRelocationRetiresItsPredecessorsController, on real hostexec controllers: A acknowledged; A completes and B starts before A's sweep. B's acknowledgement succeeds, only B is retained, and B's record blocks updates. A lock held by a controller this box does not retain is waited for no longer than the pass, and nothing is kept.) | | 2 (P2) | B | 6b rev 5: ClaimRoleAssembly.Preflight returns activator.ErrClaimIsolationUnavailable. runtime.Prerequisites calls Roles.Preflight before dispatch. The "External completion gates" section requires "the reservation-bearing extension of main's isolated root launch protocol … before any tenant shape can run with claims enabled", which "is not supplied by the external owner adapters". | accepted (contract) | Request R10 asks the claim session and the activator's owner for that protocol, with a relocation probe's "probe" work admitted through it. Task 8c is now gated on R10. Task 10 gains an activation gate: the passes stay dormant and refuse while the launcher lacks the protocol. The stage B re-plan names the production probe tests: success through the protocol, refusal without it before any attempt is counted, and the pass staying off. | Requests (R10), Task 8c, Task 10, stage B re-plan |

Astra's readings of rulings 1 to 24 stand.

Rev 12: round 11 dispositions

Astra's round 11 (CODEX-PLAN-REGION-HA-1BN-R11.md) resolved the chooser-test finding and raised one P2. It is accepted; none is declined.

The coordinator also asked for a check of every stage A use of holder.admissions as authority. That check found one more case, S1. Both changes were dry-run on a clean 3407d114 with stage A applied in task order (1, 2, 3, 4, 5, 6, 7, 9a), building and running each task's tests after it. Vet for darwin and windows and the cross-builds are clean. Four new guards were each removed in turn, and each removal failed its test (listed in the Self-review).

| # | Stage | Evidence checked | Disposition | What changed | Where | |---|---|---|---|---|---| | 1 (P2) | A | AdmitWriter drops a covered, loss-archived head once more than eight admissions are kept (generation.go:154). Rev 11's filesPin built its origins only from holder.generation and the retained admissions. A file published at g1 and never changed is still files/g1/objects/... at g10, because CopyManifest carries the entry and Stage writes nothing for unchanged content. The pin accepted that manifest, but CopyPinnedManifest refused it with ErrOrigin. Claim §6.2a ("Files in the live set (L13)") makes the live set every object the live manifests reference, computed independently of the database baseline. | accepted | filesPin adds referencedOrigins to the retained chain: the files prefix of every generation whose objects the pinned manifest's entries and platform items reference. Each referenced object must lie under this holder's location, which binds it to the incarnation, in this region's data bucket (the region binding), at files/<generation>/objects/. Any other reference refuses the pin (ErrRefused, hostfiles.ErrOrigin), so the pin never admits what the copy would refuse. CopyPinnedManifest's check is unchanged. | Task 5 (TestPinKeepsAFileOriginTheAdmissionListTrimmed: ten real AdmitWriter and PublishGeneration cycles with real CopyManifest and publication. The admission list is trimmed to eight and no longer names g1, yet g10's manifest still references g1's object for the unchanged file. The pin and the copy succeed, and a reference to another incarnation refuses.) | | S1 | A | From the check. preparedOpened, the boundary that stops P being opened twice or its local install remade (B1-1, B2-5), scanned only the retained admissions. The same goes for coverageFor's "P not opened" test. A covered P admission that is trimmed would let a later probe open P again. | fixed | The admission that opens P journals prepared_opened in the same CAS (relocationAdmission). preparedOpened, now exported as PreparedOpened for the participant, reads that key before the admission list. | Task 1 (TestRelocationPOpenedOutlivesTheAdmissionTrim, with P's admission removed as the trim would remove it: P's reopening is refused), Task 6 (coverageFor) |

The check found no other authority taken from the trimmed list. relocationAdmission and coverageFor compare against the last admission, which the trim never removes: it drops only the head, and only past eight entries. retainAutomaticLoss records evidence, not authority. An admission the trim dropped was covered and loss-archived (admissionLossArchived), so nothing it could vouch for is lost; it falls back to the holder's live writer session.

Astra's readings of rulings 1 to 24 stand.

Rev 11: round 10 dispositions

Astra's round 10 (CODEX-PLAN-REGION-HA-1BN-R10.md) resolved both findings from round 9 and raised one P2: a test that would still pass with its production wiring disconnected. It is accepted; none is declined.

I then checked every stage A test for the same weakness. For each test of production wiring, the question was whether its assertions still hold with the wiring replaced by a stub. Two more tests failed that check. Both are fixed here, and the table lists them as S1 and S2.

The changes were dry-run on a clean 3407d114, applying stage A in task order: build, vet for darwin and windows, cross-builds, and the targeted hostops, console and cmd/console tests. Four new guards were removed in turn, and each removal failed its test (listed in the Self-review).

| # | Stage | Evidence checked | Disposition | What changed | Where | |---|---|---|---|---|---| | 1 (P2) | A | TestCreateExecutorChooserReadsTheLiveEdgesAndTheClaims read an empty bucket. Both readers returning nothing satisfied every assertion. | accepted | The bucket now holds evidence for two boxes in ie: their edges files (box-b advertising region-ha-1) and fresh status snapshots. It also holds three serving claims, two on box-a for bab/jam and one on box-b for bab/tea. The test reads through the constructed chooser's Edges and Loads. It asserts each box's identity, freshness, placement and capabilities, and each box's host and per-app counts. Then the evidence changes: box-a starts draining and goes stale, and a fourth host serves on box-b. The next read must show both changes. | Task 2 (TestCreateExecutorChooserReadsTheLiveEdgesAndTheClaims) | | S1 | A | Found in the scan. TestProductionAuthoritySelectsOnlyWithAChooser used a one-box fixture, so a SelectExecutor that ignored the chooser and returned a fixed box-a still passed. | fixed | Two boxes, with box-a draining. The selection must be box-b with its roster enrollment. With both draining it must be ErrNoEligibleBox and no selection. | Task 2 | | S2 | A | Found in the scan. regionHAEnabled sets Config.RegionHA from CARLOS_REGION_HA, and no test covered it. | fixed | cmd/console/regionha_test.go: on only for strconv.ParseBool true values, with whitespace trimmed. Unset, 0, false, no and garbage are off. | Task 2 |

The scan found nothing else in stage A. These tests already run against real wiring:

• hostclaim's transitions, on a real store.
• ClaimLoads, on real claims.
• Guard.AdmissionFenced and Task 9a's fence observer, against a real BeginFence.
• RelocationPolicy, through Policy.Check.
• The writers-stopped scan, against the real kernel and a fixture /proc.
• The worker, over a signed roster, hostactors.Directory and hostfence.ClaimFenceAuthority.
• StopReceiptReleases, against stored receipts.
• ReleaseFlushFiles, against a real store and registry.
• ReleasePositionsFile and RelocationControllers, on disk.
• OpenRelocationController, with a real hostexec controller.

The remaining stubs are providers that Task 10 (stage B) supplies: the worker's Choose, Eligible, Leases and Prepared; StorePinner.SelectDB, whose production value is genselect.Select over the versioned bucket; and RelocationEffects' providers. The stage B re-plan has a row that requires each one to be tested with its production value.

Astra's readings of rulings 1 to 24 stand.

Rev 10: round 9 dispositions

Astra's round 9 (CODEX-PLAN-REGION-HA-1BN-R9.md) resolved both round 8 findings and raised two new ones. Both are accepted; none is declined.

This revision also adds a dry run that applies stage A in task order. The earlier dry runs applied every task at once, which is how finding 1 got through. This time a clean 3407d114 took Tasks 1, 2, 3, 4, 5, 6, 7 and 9a one at a time. After each task: go build ./..., vet of that task's packages, and that task's tests. With finding 1 fixed, every step built and passed and turned up no other ordering fault. The tree as a whole then passed vet for darwin and windows and the cross-builds.

| # | Stage | Evidence checked | Disposition | What changed | Where | |---|---|---|---|---|---| | 1 (P1) | A | Applied in order, Task 5 failed to build: internal/hostrelocate/pin.go:259:23: undefined: hostfiles.ValidateManifest. The helper was first defined in Task 7's internal/hostfiles/platform.go. | accepted | ValidateManifest now lives in its own file, internal/hostfiles/manifestcheck.go, which Task 5 creates (Files list, Step 4, the Step 5 run and the Step 6 git add). Task 7's platform.go keeps only EnvItem and StagePlatformDelete and uses the helper unchanged. | Task 5, Task 7; the in-order dry run | | 2 (P2) | A | Selection and completion in rev 9's test both named box-a, and the intent check called BeginCreateOn itself. The test still passed with Attempt's selection removed. | accepted | The fake authority now has a selected box, the box completion offers, and a call counter. With selection on box-b and completion offering box-a, Attempt must refuse with ErrWrongState. The persisted claim must still be creating, with selected_executor box-b and executor_enrollment enrollment-b. Complete with box-b then serves on box-b, and selection must have run exactly once. Removing Attempt's use of the selection (if selected made false) fails the test: the completion substitutes box-a. | Task 2 (TestCreateIsTodaysWithoutASelection) |

Astra's readings of rulings 1 to 24 stand.

Rev 9: round 8 dispositions

Astra's round 8 (CODEX-PLAN-REGION-HA-1BN-R8.md) resolved the release-retry finding and added two P2s. I checked both against internal/host/claimstop.go and internal/hostguard/fence.go and accepted both; none is declined. Both fixes are stage A code. They were dry-run on a clean 3407d114: build, vet for darwin and windows, cross-builds, and the targeted hostclaim, hostrelocate and host tests. Two new guards were each removed in turn and their tests failed (listed in the Self-review). Ruling 23 is amended.

| # | Stage | Evidence checked | Disposition | What changed | Where | |---|---|---|---|---|---| | 1 (P2) | A | Rev 8's FenceExhaustedTarget always set op.exec to "none" and the phase to pinning. In starting and releasing, op.exec is the live source, and the verified fence is the target's. Root's stop refuses a requester that is not op.exec (claimstop.go:184, observed.Claim.Op.Exec != req.Box). | accepted | The fix depends on who holds op.exec. If another box holds it (the live source in starting or releasing), the CAS consumes the target's fence, retains its loss, puts it on lost, drops it from the participants and records stuck. It leaves op.exec, the phase, the stamp and every release record unchanged. The old move to a stuck pinning with op.exec "none" now happens only when op.exec is the dead target itself (its own fence revokes it) or is already "none". | Task 1 (TestRelocationExhaustedTargetIsFencedIntoAStuckPinning/dead_while_the_source_executes_in_starting and …_in_releasing, the latter with the source's release journaled first); ruling 23 | | 2 (P2) | A | Rev 8's Release restored recorded.ExpectedDirectoryRevision only when the boot or controller had changed. Root's stop compares that revision with its stop inventory (claimstop.go:191). The fence target also carries it (hostguard.FenceTarget.DirectoryRevision, fence.go). | accepted | When matching positions are recorded, Release always asks under the recorded ExpectedDirectoryRevision, recovery or not. Only the recovery branch takes the recorded boot and controller. | Task 7 (TestRelocationReleaseReplaysOnlyRecordedPositions/root_fails_after_the_producers_closed: the retry runs under the same boot and controller, with the roster at revision 5. Root is asked at revision 4, and only the producers' drain and the receipt run.) |

Astra's readings of rulings 1 to 22 and 24 stand. Ruling 23 is amended as finding 1 requires.

Rev 8: round 7 dispositions

Astra's round 7 (CODEX-PLAN-REGION-HA-1BN-R7.md) resolved the kcmp finding, confirmed that stage B's contracts are complete, and added one P2. We checked it against internal/host/claimstop.go and accepted it; none is declined. The fix is stage A code. It was dry-run again on a clean 3407d114: build, vet for darwin and windows, cross-builds, and the targeted internal/host tests. Two new guards were removed in turn and each made the new test fail (listed in the Self-review).

| # | Stage | Evidence checked | Disposition | What changed | Where | |---|---|---|---|---|---| | 1 (P2) | A | In ClaimStopCoordinator, DrainClaim runs before Kernel.VerifyStopped and Guard.CompleteFence (claimstop.go:219 onward). If either fails, root has no durable receipt. On retry, BeginFence returns the same fence, FenceReceiptFor returns ErrNoFenceReceipt, and root asks for the drain again. Rev 7's Release read the recorded positions but still built a fresh releaseDrain, which repeated StopWriters, the observation and both flushes against a replicator its own producer drain had already closed. | accepted | When this controller has already recorded positions for the exact stop (same boot and controller, root without a receipt), Release marks its drain resumed and carries the recorded TXID and sequence. A resumed drain goes straight to the producers' own drain, which is idempotent, and leaves verification and the receipt to root. A restarted agent keeps the recovery path; a replayed receipt keeps pairing with the record. | Task 7 (TestRelocationReleaseReplaysOnlyRecordedPositions/root_fails_after_the_producers_closed: the drain closes the producers, root fails before persisting its receipt, and the retry without a restart runs only producers and receipt, with no flush, record or writers stop, and returns 41 and 8) |

Astra's readings of rulings 1 to 24 stand.

Rev 7: round 6 dispositions

Astra's round 6 (CODEX-PLAN-REGION-HA-1BN-R6.md, against 222ff1c6) resolved all six of round 5's findings and added one. It was checked against the plan and the kernel before anything changed, and is accepted; none is declined. The fix is stage A code, dry-run again on a clean 3407d114 (build; vet for darwin, windows and linux/arm64; cross-builds; the stopevidence tests run five times against the real kernel), with 3 new guards removed in turn (listed in the Self-review). Stage B is unchanged: R3's root endpoint calls the same WritersStopped.

| # | Stage | Evidence checked | Disposition | What changed | Where | |---|---|---|---|---|---| | 1 (P1) | A | scanOne exempted a thread's descriptor when the leader showed the same number and path. Confirmed on this kernel: a thread that runs unshare(CLONE_FILES) keeps a copied table with the database at the same number, and it can dup3 an independent open onto that number; /proc/<pid>/task/<tid>/fd/<n> reads the same path either way. kcmp(2) is the positive check: KCMP_FILES compares two tasks' descriptor tables and KCMP_FILE compares two descriptors' open file descriptions. golang.org/x/sys v0.46.0 has unix.SYS_KCMP on all 15 linux architectures but no unix.Kcmp and no constants, so the plan makes a raw Syscall6 with KCMP_FILE = 0 and KCMP_FILES = 2 from linux/kcmp.h. kcmp needs ptrace read access to both tasks. The agent always has it within its own thread group, and root's complete scan has it through CAP_SYS_PTRACE. This box runs CONFIG_KCMP=y and Yama scope 0. | accepted | A thread's descriptor is the leader's only if three things hold: the leader shows the same number and path, KCMP_FILES(pid, tid) is 0 (the thread shares the leader's table), and KCMP_FILE(pid, tid, n, n) is 0 (the same open file description). Otherwise it is reported with FD -1, which no allow-list exempts. A copied table counts as foreign even when the description is shared, because the thread could still use that description after the replicator closes. If a task exits mid-scan (ESRCH), it is skipped as before. EBADF is treated as "not the leader's". Any other kcmp error, including ENOSYS and EPERM, is ErrIncomplete. kcmp takes pids in the caller's pid namespace, so it is used only for the caller's own /proc. Any other root fails closed unless a test replaces kcmpFor. The //go:build linux file and the !linux stub stay as they were. | Task 4 (TestProcessDescriptorsTellsSharedFromUnsharedThreadsByKernelIdentity on the real kernel: a shared locked thread adds nothing; an unshared thread with the copied descriptor, and one that reopened the database and dup3'd it onto the leader's number, are each reported FD -1. TestWritersStoppedRefusesAnyOtherHolder's new fixture cases: an unshared thread at the leader's number and path, a shared table whose descriptor is another description, and kcmp unavailable (ENOSYS, EPERM) as ErrIncomplete for both scans) |

Astra's readings of rulings 1 to 24 stand.

Rev 6: round 5 dispositions

Astra's round 5 (CODEX-PLAN-REGION-HA-1BN-R5.md, against 996b24c3) left R4-5 partly resolved and added five findings. Each was checked against the tree at 3407d114 and the plan before anything changed; all six are accepted and none is declined. Every one lands in stage A code, dry-run again on a clean 3407d114 (build, vet for darwin and windows, cross-builds for darwin, windows and linux/arm64, targeted tests), with 11 new guards removed in turn (listed in the Self-review); R4-5's restart obligations are carried into the stage B re-plan as well.

| # | Stage | Evidence checked | Disposition | What changed | Where | |---|---|---|---|---|---| | R4-5 | A, B | hostexec.Controller.Close (controller.go:480) sets closed before returning errors.Join(err, c.CleanupError()) and returns nil on every later call; rev 5's Finish cleared after any nil Close, and the restart path cleared from the journaled binding with no cleanup at all. Rev 5 also journaled only inside Finish, so a record left by a crash (or a failed Open, which writes lost once it holds the live lock) before the first Finish was never found. | accepted | Repeat, do not trust: RelocationControllers.Cleanup(ctx, binding) is the scoped cleanup (Task 8a's relocationCleanup, authenticated to the binding's box and enrollment) and Finish runs it, and needs it to succeed, in the same call as every clear, after Close and on the restart path alike; a failure keeps the record, the entry and the journal. The participation is journaled before the controller opens (Acknowledge refuses without a journal), so a restart finds every record it may have left; the journal write syncs its directory. | Task 7 (TestFinishClearsTheDurableRecordAndRetriesAcrossARestart: cleanup failure, a sweep after it, a restart while it still fails, then success; TestARestartFindsAParticipationThatNeverReachedFinish; TestFinishClearsTheDurableRecordSoUpdatesAreEligible with a real hostexec controller whose cleanup fails); stage B re-plan | | 1 | A | hostops eligible excluded only Lost; Worker.next excluded the source, Lost and replaced targets; ReplaceTarget reaches install directly in installing and installed, never through ToInstalling's park-local check. | accepted | hostclaim.OwesLocal and LocalChoreBoxes. Selection excludes every box owing a park-local (the chooser's eligible set, so create, Permits and the worker's spare all agree; Worker.next too), and replaceTargetSlot refuses one with ErrPendingChore inside the CAS, for ReplaceTarget at every phase and NameTarget. | Task 1 (TestRelocationReplacementRefusesABoxOwingALocalRetirement, in starting, installing and installed), Task 2 (TestExecutorChooserNeverNamesAFencedLostOrUnknownBox/owing_a_local_retirement), Task 5 (TestWorkerNeverReplacesATargetWithABoxOwingALocalRetirement) | | 2 | A | fenceBox journaled the fence, added lost, discharged park-local and retained the loss, and touched no regional obligation; lost.go:302 reassigns box:<b>'s park-generation and park-replica to region:<r> for a declared loss. | accepted | fenceBox passes every park-generation and park-replica owned by box:<b> to region:<obligation's region> in the same CAS, changing nothing but owner (an obligation with no region refuses, as in DeclareLost); the retained AutomaticLoss names them (reassigned, the D4 record's reassign_regional). Every automatic fence CAS shares it: start, FenceSource, ReplaceTarget, FenceExhaustedTarget. | Task 1 (TestRelocationFenceReassignsTheDeadBoxsRegionalWork, unqualified and qualified discharge); R5 | | 3 | A | Task 9a's check replaced Serving with RelocationRow unconditionally; with both callbacks nil a moving executor participant is RowHeld and passed, and Install went on to Activate and RecordInventory before WorkSource.SelectAt (work.go:94) refused. | accepted | Reconciler.relocationAware() is FenceClosed != nil \|\| HoldRow != nil (Task 10 sets both only with CARLOS_REGION_HA). Off, check is today's Serving and Install skips the row decision and the hold-only path entirely. | Task 9a (TestReconcileWithoutAFenceObserverIsTodays: a relocating source in starting and releasing and a moving executor, dry run and real, refused with the claim's ETag and every file under the guard's data directory unchanged) | | 4 | A | journaled decoded every directory entry, so writeFileSynced's truncated .json.tmp failed the whole listing, and Retained dropped the error. | accepted | Only names ending .json are committed records; a .tmp is ignored (its participation opened nothing: the record precedes the open). A committed record that cannot be read is reported, joined into the error, beside every readable one. Effects.Retained returns ([]Participation, error); Sweep reports the error and still finishes every readable participation. | Task 7 (TestARestartFindsAParticipationThatNeverReachedFinish: one valid journal, one truncated .tmp, then one damaged committed entry), Task 6 (TestAParticipantFinishesItsControllerOnceTheOperationIsOver) | | 5 | A, B | Flush loads the existing manifest through hostfiles.Open and did nothing on ENOENT, so Platform[EnvItem] kept the old bytes. | accepted | (*hostfiles.Publisher).StagePlatformDelete(name) (in platform.go) drops the item at a new sequence; Flush stages it on ENOENT, so ReadPlatform on the final revision returns os.ErrNotExist. Stage B's local install treats that as "no env file" (re-plan). | Task 7 (TestReleaseFlushFilesCarriesTheLastWakeStateAndEnv: published, removed, flushed again, then a no-op repeat) |

Astra's readings of rulings 1 to 24 stand; ruling 20's cleanup is completed by R4-5 above.

Rev 5: round 4 dispositions

Astra's round 4 (CODEX-PLAN-REGION-HA-1BN-R4.md, against 418daf58) left three earlier findings partly resolved and added six. All nine are accepted; none is declined. Under ruling 24, stage A findings are fixed in code (dry-run on a clean 3407d114, 7 new guards removed in turn, listed in the Self-review); stage B findings are fixed at the contract level: what must happen, which request covers it, which test proves it.

| # | Stage | Disposition | What changed | Where | |---|---|---|---|---| | R1-9 | B | accepted | Region is 6b's field: Task 8a's Collect provider sets it on every request from the verified actor (the box's region never changes), initially and on recovery alike, beside Recover for the recorded owner's stop. | Task 8a | | N1 | B | accepted | The fixture's withExistingRow takes the hold everywhere it is called; the census literal carries 6b's actual fields (Inventory, Registry, Launches, Box, Enrollment, DirectoryRevision, Roots, SharedPaths), no Guard. | Task 9 | | N3 | B | accepted | R8's insertion point is after actor verification: 6b's Build calls an Extend(a *ClaimAssembly, actor hostbox.Actor) hook before it captures Policy.Check; applyRegionHA is that hook's body and binds the policy to actor.Box. | Task 10, R8 | | 1 | A | accepted | Guard.AdmissionFenced(host, claim, captured) takes no lock (one atomic record read; the claim is the caller's fresh read); Reconciler.FenceClosed takes the context and the observation and returns an error, which keeps rows and mints none; holdOnly re-decides on a fresh read under WithLocal. Tested with the real observer, a real BeginFence, and a bounded context on both the activation and the hold-only path. | Task 3, Task 9a (TestReconcileRelocationSourceReadyThenHeldWithTheRealFenceObserver) | | 2 | A, B | accepted | Policy half (A): a relocation target's probe is its own selected action, probe, which Policy.Check admits for a relocating claim and RelocationPolicy sends to WakePhase(probe=true); an ordinary spawn by the target stays refused. Dispatch half (B): R1 extended, 6b's runtime selects "probe" work for a relocation probe. | Task 3 (TestRelocationPolicyGivesEachActionItsRole, TestPolicyLetsAHeldParticipantReconcileItsRow), R1 | | 3 | B | accepted | The restore destination (the host's files directory and env path) is created and inventoried under the installation's authority before Restore, through 6b's typed inventory (a files entry at install_stamp), never an untracked MkdirAll; tested with a fresh spare that has no host directory. | Task 8c | | 4 | B | accepted | Held release staging needs root: request R9 asks moves for a relocation-aware relay authorizer (bound to the operation, executor, install stamp and the pinned release); the install verifies staging before it records its receipt; tested under the edge unit's filesystem restrictions. | Task 8c, R9 | | 5 | A | accepted | RelocationController.Clear (hostexec's ClearStale with the controller's config); Finish journals the participation before closing, keeps the entry and the record on a failed close or clear, clears the exact record after a successful cleanup, and a restart retries through the journaled binding. A real hostexec controller on disk shows root's §5.10 check (hostexecParticipation) refusing before and admitting after. | Task 7 (TestFinishClearsTheDurableRecordSoUpdatesAreEligible, TestFinishClearsTheDurableRecordAndRetriesAcrossARestart) | | 6 | A | accepted | The obsolete-hold clearance in Policy.Check needs Relocation set (region HA on); off, today's refusal. Tested both ways on the same held serving row. | Task 3 (TestPolicyLetsTheServingExecutorClearAnObsoleteHold) |

Rev 4: round 3 dispositions

Astra's round 3 (CODEX-PLAN-REGION-HA-1BN-R3.md, against d93c94d0) left three earlier findings partly resolved, one unresolved, and added six. All ten are accepted; none is declined. The un-gated changes were dry-run again on a clean 3407d114 (build, vet for darwin and windows, cross-builds, targeted tests) and each new guard removed in turn (8 removals, each failing its test; listed in the Self-review).

| # | Disposition | What changed | Where | |---|---|---|---| | R1-5 | accepted | PreparedFromInstallManifest.Verify compares P's entries against the pinner's retained copy (pin.Files.Retained), never the source manifest; a late source PUT changes nothing it reads. | Task 8b | | R1-9 | accepted | After a restart Release names the recorded owner's boot, controller and directory revision and offers RecoveryReleaseDrain; Task 8a's Collect provider sets 6b's Recover on that drain, so root's authenticated recovery path accepts the tuple and replays the receipt. | Task 7 (TestRelocationReleaseReplaysOnlyRecordedPositions/after_a_restart…), Task 8a | | R2-N4 | accepted | Policy.Check's serving branch lets exactly the serving executor's reconcile through an obsolete hold (one naming no operation the claim runs), so the adapter's clear is reachable; every other write under a hold still waits. | Task 3 (TestPolicyLetsTheServingExecutorClearAnObsoleteHold), Task 9 | | R2-N5 | accepted | See N2. | Task 7 | | N1 | accepted | Task 9's adapter insertion re-reads the claim under the captured authority (observed is defined there, validated against the captured incarnation and stamp); the test fixture (adapterFixture and its methods) is this task's code, over 6b's adapter and registry. | Task 9 | | N2 | accepted | Finish keeps the map entry until Close succeeds and forgets only that same controller, so a close the pass's context cut short is finished by a later sweep. | Task 7 (…RetainsTheControllerUnderTheAgentLifetime: a cancelled close, then a successful one) | | N3 | accepted | hostbox.RelocationPolicy(box) (un-gated, tested) and hostguard.Guard.AdmissionFenced (un-gated, tested) are the two providers; Task 10 wires them into the assembly between 6b's OpenProductionClaimAssembly and Build (which captures Policy.Check), gated on CARLOS_REGION_HA; with it off neither is set and behaviour is 6b's. The insertion point is request R8. | Task 3, Task 10, R8 | | N4 | accepted | Reconciler.Install takes the hold-only path for a held row whenever the box is not the executor or its admission fence is closed, so a fenced source still named op.exec in releasing writes its hold under WithLocal, never through the guarded path With refuses. | Task 9 | | N5 | accepted | FenceExhaustedTarget: a target terminated after the replacements are used is fenced into a stuck pinning in one CAS (loss retained, box on lost, op.exec "none", receipt dropped, P's remote build kept when unopened, nested when opened); the worker uses it instead of MarkStuck, which stays the live target's rule. | Task 1 (TestRelocationExhaustedTargetIsFencedIntoAStuckPinning), Task 5 (TestWorkerFencesAnExhaustedTargetThatDiedAfterItsLocalInstall); ruling 23 | | N6 | accepted | PinAfterRelease from releasing requires the acknowledgement barrier, so a target replaced after the source's release acknowledges before the operation leaves the phase. | Task 1 (TestRelocationReplacementInReleasingAcknowledgesBeforePinning) |

Rev 3: round 2 dispositions

Astra's round 2 (CODEX-PLAN-REGION-HA-1BN-R2.md, against ed992c46) left seven round 1 findings partly resolved and added seven. All fourteen are accepted; none is declined. Every un-gated change was dry-run again on a clean 3407d114 (build, vet for darwin and windows, cross-builds, targeted tests) and each new guard removed in turn (11 removals, each failing its test; listed in the Self-review).

| # | Disposition | What changed | Where | |---|---|---|---| | R1-2 | accepted | The build's authority is checked at every write, not once: authorityStore wraps the versioned store so each PutIfAbsent and CopyVersion re-reads the claim and the host-guard record (hostguard.Capture at install_stamp) first; the lease's loss cancels the rest. | Task 8b | | R1-4 | accepted | AutomaticLoss retains the holder's incarnation and stamp, the box's last writer session whether or not it is still the writer (its last admission record on the holder, LastAdmission), so a source fenced after the target's admission keeps its session and consequences. | Task 1 (TestRelocationLossRetainsAFormerWritersSession); R5 | | R1-5 | accepted | The pinner retains the exact manifest bytes in the control bucket (RetainedManifestKey, create-only) before the pin; CopyPinnedManifest writes P from that copy, validated by digest, sequence and origins (hostfiles.ValidateManifest), and never reads the source again. A late source PUT changes nothing. | Task 5 (TestCopyPinnedManifestEnforcesThePin), ruling 21 | | R1-9 | accepted | ReleasePositions.Recorded matches the installation and session, not the controller, and returns the request the flush was made under; after a restart Release asks root under that identity (so root finds the stop's durable receipt), offers no drain of its own, and pairs the replayed receipt with the recorded positions. A stop root never completed cannot be finished by a new process: the release deadline makes it stuck. | Task 7 (TestRelocationReleaseReplaysOnlyRecordedPositions/after_a_restart…, TestReleasePositionsFileBindsTheExactStop) | | R1-13 | accepted | A later probe attempt whose predecessor generation holds no LTX file (genselect.ErrEmpty) is an ordinary empty cold admission: Empty set, no baseline, 6b's own empty authority. | Task 8c | | R1-14 | accepted | See new finding 2. | Task 9 | | R1-16 | accepted | Exhaustion is checked before a replacement is looked for, in both paths: with the replacements used the operation is stuck now, never retried on "no eligible box". | Task 5 (TestWorkerMarksExhaustionStuckBeforeLookingForASpare) | | N1 | accepted | Prepared is set only by the two branches that open P; the retry branch resets Prepared and Empty and selects its baseline as an ordinary cold wake, so its marker follows the first durable root. | Task 8c | | N2 | accepted | The adapter test separates "no row to mint" (a box with no role and no row: ErrChanged, nothing written) from "an existing unexplained row to keep" (held, never served, never deleted), and asserts hold_op, not a status the implementation does not write. | Task 9 | | N3 | accepted | ProcessDescriptors reads only /proc/<pid> (its own process; another process's unreadable table does not matter); the complete scan is root's: RelocationEffects.Observe is a provider, production asks root over the instance-control socket (CollectWritersStopped, R3's server half), and an agent-side scan fails closed on the first unreadable table. | Task 4 (TestProcessDescriptorsNamesOneProcessesHolders), Task 7, Task 8a, R3 | | N4 | accepted | A RowReady row whose hold_op names an operation the claim no longer runs has its hold cleared under the activation's verified ownership (SetClaimHold(owner, old, "")); a hold of the running operation is never touched. | Task 9 (TestReconcileAdapterClearsTheHoldAfterCompletion), ruling 20 | | N5 | accepted | Effects.Retained and Finish; Participant.Sweep finishes every retained controller whose operation the claim no longer runs with this box as a participant, once per pass; the relocation controller's Cleanup hook is scoped to the relocation's own partial work and is a no-op once this box has admitted under the operation or serves the host, so finishing never stops the serving writer. | Task 6 (TestAParticipantFinishesItsControllerOnceTheOperationIsOver), Task 7 (Finish in TestRelocationAcknowledgeRetainsTheControllerUnderTheAgentLifetime), Task 8a, Task 10; ruling 20 | | N6 | accepted | MaxProbeAttempts = 3; BeginProbeAttempt counts the attempt in the claim before it is made (per box and operation, so a replacement starts at zero); the participant enters probe-failed on the fourth. Durable across restarts and lost responses. | Task 1 (TestRelocationProbeAttemptsAreBounded), Task 6 (TestAParticipantGivesUpAfterThreeProbeAttempts); ruling 19 | | N7 | accepted | A qualified discharge completes each park-local with CompleteObligation's own semantics, so a discovery operation's final chore marks discovery complete exactly as a retirement would. | Task 1 (TestRelocationDischargeCompletesDiscoveryLikeARetirement) |

Astra's readings of rulings 1 to 4, 6 to 8 and 10 to 17 stand; rulings 5, 9 and 18 are completed by R1-5, N6 and R1-4 above.

Rev 2: round 1 dispositions

Astra's round 1 (CODEX-PLAN-REGION-HA-1BN-R1.md, against eb5e9051) returned sixteen findings, "not ready". Each was checked against the tree at 3407d114 and the cited plans before anything changed. Fifteen are accepted in full and one in part (8: the un-gated half is built, the production body is a request to the claim session). None is declined. Every un-gated change below was dry-run again: applied to a clean 3407d114, built, vetted for darwin and windows, cross-built, tested, and each new guard removed in turn (25 removals, each failing its test; listed in the Self-review).

| # | Disposition | What changed | Where | |---|---|---|---| | 1 | accepted | Task 8 is three tasks against the declared types: moves.SealedObject{Key, VersionID, Size}, moves.InstallManifest (on main), moves.BuildInputs with Now from this plan's config, 6b's localStopIdentity, Wake.Producers, CollectClaimStop. What no plan supplies is now this plan's code (RelocationWakeInputs, the install journal, PreparedFromInstallManifest reading moves.InstallManifestKey) or a named request (R1 the probe dispatch 6b refuses today, R2, R3). | Tasks 8a, 8b, 8c; Requests | | 2 | accepted | The worker holds the replica lease on holder.location from pin selection to the journal CAS (Worker.Leases, pinUnderLease); a lease lost before the CAS refuses. The build runs under the same lease, re-reads the claim before each durable step and is cancelled when the lease is lost. | Task 5 (TestWorkerDrivesADrain's order, TestWorkerRefusesToJournalAPinAfterTheLeaseIsLost); Task 8b (TestRelocationBuildStopsWhenAuthorityChanges) | | 3 | accepted | ReleaseFlushFiles: Open, StageWake(ExportWake), StagePlatform(EnvItem), SyncDir, Commit as one revision; hostfiles.EnvItem added. | Task 7 (TestReleaseFlushFilesCarriesTheLastWakeStateAndEnv) | | 4 | accepted | D4 retention outside the operation: Claim.EvidenceRefs []AutomaticLoss (fence reference, observation time, box, role, last writer session, discharge verdict, timers unknown, reporting pending) and the loss id in LossRefs, written by fenceBox in the consuming CAS with a deterministic id; both survive CompleteRelocation, free and holder replacement. Claim.Validate checks them. | Task 1 (the failover test's completion checks, TestRelocationRetainsEveryFencedBoxAcrossCompletion); ruling 18 | | 5 | accepted | FilesPin.Origins (the admitted chain as pinned); hostrelocate.CopyPinnedManifest verifies the source bytes against the pin's digest and sequence, copies with the pinned origins, and refuses a copy whose entries differ from the pinned ones; the build and the verifier use it. | Task 5 (TestCopyPinnedManifestEnforcesThePin: a late revision, different bytes at the same sequence, inherited objects); Tasks 8b | | 6 | accepted | PinObject.N is gone. ClaimGen names the observation; the build takes pin.DB.MaxTXID; the empty branch is DB == nil. | Task 5, Task 8b | | 7 | accepted | ToInstalled requires FilesSeq == pin.FilesSeq and a FilesManifestSHA256 always (an empty pin included); the build writes P's files manifest before the database; the verifier reads both back. | Task 1 (TestRelocationDrainEndToEnd, TestRelocationEmptyPinNeedsItsEvidence); Task 8b (TestPreparedRefusesAPartialBuild) | | 8 | partly | RelocationEffects.StopWriters runs first in the drain, before the observation; its production body is request R2, because 6b has no writers-only stop and its ClaimProducers.DrainClaim cancels every producer. The live-process test is Task 8a's, gated on R2. | Task 7 (TestRelocationReleaseRunsStepsOneToThreeInsideTheDrain); Task 8a; Requests | | 9 | accepted | ReleasePositions: the flushed positions are recorded durably, bound to the exact stop request, before the producers close; a replayed receipt is paired with that record or refused. ReleasePositionsFile on disk. | Task 7 (TestRelocationReleaseReplaysOnlyRecordedPositions, TestReleasePositionsFileBindsTheExactStop) | | 10 | accepted | RelocationControllers retains controllers under Lifetime (the agent's context); Effects.Ready runs before every effect; a restarted agent reopens a controller and never re-journals the acknowledgement. | Task 6 (TestAParticipantChecksItsControllerBeforeEveryEffectAndReopensAfterARestart); Task 7 (TestRelocationAcknowledgeRetainsTheControllerUnderTheAgentLifetime); Task 10 | | 11 | accepted | The pin's key names the claim generation it was selected against (hostclaim.RecoveryPinKey, pin-<gen>.json); JournalPin binds it, so a pin whose CAS lost is abandoned and the retry selects afresh; every bound is checked before the object is written; the counter is gone. | Task 1, Task 5 (TestStorePinnerPinsTheNewestFilesManifestInTheChain, TestStorePinnerChecksTheBoundsBeforeItWrites); ruling 16 | | 12 | accepted | Worker.Eligible (ExecutorChooser.Permits: the complete eligible set, so stale edges, a missing capability or key, a draining box refuse) and Worker.Relocatable (the record's shape) at Start; a sidecar family is refused outright. | Task 2 (TestExecutorChooserPermitsOnlyTheEligibleSet), Task 5 (TestWorkerStartRefusesAnIneligibleTargetAndANonRelocatableHost), Task 10 | | 13 | accepted, narrowed | An empty pin is evidenced only by a journaled release at final_txid 0 or a holder that never admitted a writer; any other ErrEmpty refuses (ruling 15). A drain of a session-0 host is refused at Start (ruling 11 amended, request R4). FlushDB reports 0 on ErrEmpty after the sync; the verifier requires only the files manifest for an empty pin; the first probe is a cold admission into an empty generation. | Task 1 (TestRelocationEmptyPinNeedsItsEvidence), Task 5 (TestStorePinnerPinsEmptyOnlyWithEvidence, TestWorkerRefusesToDrainAHostThatNeverHadAWriter), Tasks 8a to 8c | | 14 | accepted | Policy.Check gains the reconcile action for a relocating participant (un-gated); Task 9 is rewritten around three authorities: activation only for the executor, WithLocal plus a conditional SetClaimHold for a kept row, and no mint for a target before installing (ruling 17). Its test drives 6b's ReconcileAdapter.Install for the source and the target in every phase. | Task 3 (TestPolicyLetsAHeldParticipantReconcileItsRow), Task 9 | | 15 | accepted | Authority.SelectExecutor returns selected; without one Attempt runs today's BeginCreate. ProductionAuthority.Executors nil means no selection; the console's chooser is nil unless Config.RegionHA (parsed by strconv.ParseBool) is on. | Task 2 (TestCreateIsTodaysWithoutASelection, TestProductionAuthoritySelectsOnlyWithAChooser, TestCreateExecutorChooserReadsTheLiveEdgesAndTheClaims) | | 16 | accepted | A live target's exhausted replacement goes through stuckOn from probe-failed; ReleaseDeadline marks a release never journaled stuck in releasing and probe-failed (ruling 14); relocationAdmission checks stuck before any phase. | Task 1 (a stuck source does not wake), Task 5 (TestWorkerMarksALiveTargetsThirdReplacementStuck, TestWorkerMarksAnOverdueReleaseStuck) |

Astra's readings of rulings 1 to 13 stand; ruling 5's exact-files enforcement is finding 5's fix, and ruling 9's promised behaviour is finding 16's.

Requests to the claim and moves sessions

Interfaces this plan needs that no merged or declared plan supplies. Each gated task names the request it waits for; nothing here is invented silently.

| # | To | Request | Waited for by | |---|---|---|---| | R1 | claim 6b | ClaimWakeAssembly.Build's runtime refuses every probe and every non-serving claim with a ClaimDependencyError naming moves C1. Region HA supplies host.RelocationWakeInputs (Task 8c) for relocating/probing where op.exec is this box. Ask: dispatch by Op.Kind to that provider in Prerequisites, Admit and Prepare, allowing p.Probe there, and expose one probe attempt as (*ClaimWakeAssembly).Probe(ctx, obs, StartPolicy) (session uint64, passed bool, err error) returning the attempt's exact health. Rev 5: for that attempt the runtime selects its spawn work as action "probe" (source.SelectAt(host, "probe", captured)), the action Task 3's policy gives probe authority to; ordinary "spawn" work for a relocation target stays refused. Rev 15 (round 14 finding 3): claim §4 and Task 1's phase table also let the source admit, cold, in starting and releasing, but 6b's runtime.Prerequisites refuses every non-serving claim (p.Probe || o.Claim.Op.Kind != KindServing, 6b's ClaimDependencyError naming moves C1). Ask: dispatch a relocating claim's ordinary wake to the existing wake inputs when this box is op.exec and the source, in starting or releasing, with its admission fence open (Task 3's WakePhase and RelocationPolicy); refuse it once the fence closes or the claim no longer names this box. A relocation target's ordinary wake stays refused; its only wake is the probe. Rev 15 (round 14 finding 1): the probe's first admission consumes P's prepared manifest (sequence 0) as the session publisher's baseline, by the digest prepared_authority.files_manifest_sha256 names (the store has no version-id read, ruling 5). The publisher starts at sequence 1. | Task 8c | | R2 | claim 6b | A writers-only stop on the admitted attempt, (*claimWakeAttempt).StopWriters(ctx) (ClaimWritersDrained, error): close admission, settle spawn reservations, cancel and join the app's role launch, drain the schedule runner's in-flight deliveries for the host, wait for the host's cgroup to empty; keep the replicator and the files publisher open; idempotent once stopped; report the three drained facts, the cgroup and the database paths. ClaimProducers.DrainClaim stays the full drain. | Task 8a (finding 8) | | R3 | claim 6b | Two halves of L10's observation, split at the privilege boundary (rev 3). Agent side: record the replicator's descriptors when it opens, stopevidence.ProcessDescriptors(ctx, "/proc", os.Getpid(), dbPaths) immediately before and after held.Replicate (it reads only /proc/self), the difference kept on the attempt as replicatorFDs with claimStopLocal.ProcessStart. Root side: an authenticated instance-control endpoint POST /claim/writers-stopped taking Task 8a's WritersStoppedRequest (host, drained facts, database paths, replicator pid, start and descriptors) from the carlos uid, running stopevidence.WritersStopped with root's cgroup manager and the complete /proc scan, and returning the evidence. The agent cannot read other processes' descriptor tables (carlos-edge.service: uid carlos, CAP_NET_BIND_SERVICE only); an agent-side scan fails closed. | Task 8a | | R4 | claim Plan 5 | The positive no-process witness for an installation with writer_session = 0 (6b's collectCapturedStop already names it). Until it lands a drain of a never-woken host is refused at Start (ruling 11); a failover relocates it. | Task 5's ruling 11 | | R5 | claim spec, console | Adopt evidence_refs as the claim field for D3's "enrollment-qualified fence references": this plan's hostclaim.AutomaticLoss shape, one per (operation, box, fence), with the loss id in loss_refs, carrying the fence reference and observation time, the holder's incarnation and stamp, the box's role, its last writer session and that session's admission record (coverage, declarations), the discharge verdict and timer knowledge (rev 3: complete retained consequences), and the regional obligations the fence passed to the region (rev 6: reassigned, D4's reassign_regional). The console's claim-recovery pass materializes each into control/host-loss/<id>.json (D4's automatic variant, write_sources from last_admission, timers unknown or partial) and sets reported; until then the claim keeps it. | After this plan | | R6 | claim spec | What evidences an empty generation on a failover of a host whose writer session is above 0 and whose listing holds no LTX file. Ruling 15 refuses it (the operation waits for an operator); if the claim session wants automatic recovery there, name the evidence. | ruling 15 | | R8 | claim 6b | A hook on ClaimAssembly, Extend func(*ClaimAssembly, hostbox.Actor), called by Build after a.Identity.Verify and before the WorkSource captures Policy.Check (6b's Build at the line that sets source := hostbox.WorkSource{…Policy: a.Policy.Check…}), so the verified box identity is available. Task 10's applyRegionHA is its body: with CARLOS_REGION_HA on it sets a.Policy.Relocation = hostbox.RelocationPolicy(actor.Box) and a.Reconcile.Reconciler.FenceClosed (over Guard.AdmissionFenced); off, it touches nothing. (Rev 4's insertion after OpenProductionClaimAssembly was before the box was known.) | Task 10 | | R9 | moves Plan 1 Task 7b | A relocation-aware held-release relay: release.ServeHeldStageRequests' authorizer accepts a request bound to a relocating operation (Op.Kind == relocating, Op.Exec == req.Box, op.journal.install_stamp equal to the request's stamp, and the pinned release equal to the version the local install recorded), beside the moving/landing requests it accepts today. Without it MaterializeHeld returns ErrStageBlocked under the edge unit's ProtectSystem=strict and the local install cannot complete. | Task 8c | | R10 | claim 6b (and the activator's owner) | The reservation-bearing extension of main's isolated root launch protocol, which 6b's own external completion gate names as required "before any tenant shape can run with claims enabled" and as "not supplied by the external owner adapters" (6b rev 5, "External completion gates"). Until it exists, ClaimRoleAssembly.Preflight returns activator.ErrClaimIsolationUnavailable for every launch (6b, Preflight), and the runtime's Prerequisites calls Roles.Preflight before any dispatch (6b, runtime.Prerequisites). Even with R1 every production probe would therefore be refused. The ask: the protocol binds each supported role launch to the durable claim reservation and preserves main's namespace isolation; Preflight admits a relocation probe's "probe" work through it, bound to op.exec, the operation and install_stamp; without the protocol, Preflight refuses before any probe attempt is counted. | Task 8c, Task 10 | | L21 | region HA spec (Paul) | Open: the durability of the always-continuous items between an app minting them and their first publish. §5.6 has every cold admission copy its manifest before the app starts, and H6 makes instance.key, report.token and the env files continuous. Continuous is not synchronous: an app can mint instance.key, write database rows sealed with it, and replicate them before the publisher's first manifest with the key lands. A box terminated in that window leaves a nonempty database whose key exists nowhere. Rev 18's pinner refuses that case and the operation goes stuck for an operator (ruling 25), but the database is not recoverable by any relocation. Closing the window needs an upstream durability contract, and there are two candidates, neither chosen here: the platform pre-provisions instance.key (and report.token) into the files directory and publishes them before the app's first start, or the replicator holds its first upload until the first manifest carrying the key has landed. Decided 2026-10-09 (Paul): the platform pre-provisions the key. At creation the platform generates it on the box (CSPRNG), writes it create-only (never overwriting) into the instance's overlay env file as CARLOS_INSTANCE_KEY, and publishes it before the app's first start. That file is platform-managed and always continuous. Existing instances get one forced publish before region HA is enabled. The app side is a framework contract, requested as rastrillo/rastrillo #66: detect the platform, use the app's own existing key first and the platform's only when it has none, never mint on the platform, and keep today's behaviour off it. The platform side is built only once #66 agrees the contract. The pinner's refusal (ruling 25) stays as the backstop. Residual: an app that later replaces its key reopens the window for the new key. | ruling 25 | | R7 | moves Plan 2 | Task 8's moves.InstallManifestKey, SnapshotKey, AnchorKey as declared, and BuildInputs.Source taking the pinned generation's full keys as genselect lists them (level and TXID range parsed from the key's tail by SealedClient). | Task 8b |

Rulings made while planning

Each was a conflict between the authorities or a gap in them. Each says what it costs if it is wrong.

1. Relocation lives in internal/hostclaim. Main already has KindRelocating, its phase validator and ConvertMovingToRelocating there, and Plan 6b's boundary table gives "relocating, released coverage, once-selected executor and two-box witnesses" to region HA. One implementation per concept: no second package grows claim transitions. Cost if wrong: the claim session moves the functions; the names stay.
2. The relocation release's stop request names the obligation relocation-release. Root's FenceAndStop requires an obligation component, and 6b's collectCapturedStop builds only retirement stops (it looks for this box's park-local under the operation). A release retires nothing. host.StopReceiptReleases accepts only receipts carrying relocation-release, so a retirement stop can never be offered as a release, nor the reverse. Cost if wrong: a one-line constant, and the 6b session may prefer another literal.
3. Discharge stays off until the roster records an enrollment time. boxvolumes.Discharge needs the enrollment time (§24 item 4) and hostactors.Box carries none. The production Discharge provider returns "the roster records no enrollment time", so a fenced box's park-local chores stay open for an operator. H19: this costs cleanup, never recovery. Ask of the claim session: add enrolled_at to box entries (D7); then the provider reads boxvolumes.List and calls boxvolumes.Discharge.
4. A box-started relocation needs claim §5.1's app-admission registration, with a {box, enrollment, controller} owner. Main has no apps/<acct>/<app>/admission.json registry yet. hostrelocate.Worker takes an Admission interface and refuses to start without one (ErrUnsupported). Task 10 is gated on claim Plan 5's app gate as well as 6b. Cost if wrong: none until that lands; nothing starts.
5. The pinned recovery set is an immutable object at control/relocations/<host>/<op>/pin-<claim gen>.json (rev 2, ruling 16: the generation it was selected against), written create-only and named in the journal by key and SHA-256 (spec §18's first correction: the store has no version-id read, so content is identified by digest). The files pin names its manifest by prefix, sequence and digest. Cost if wrong: a deny statement for that prefix in deployment-buckets is a follow-up; a rewritten pin is already caught, because every reader checks the journaled digest.
6. installed is the worker's CAS, made once a Prepared verifier reads P's install manifest complete (§5.8's phase table). The target enters probing itself. Cost if wrong: who makes one CAS; the claim rules are unchanged.
7. A converted move names its target in pinning (hostclaim.NameTarget), before installing, so the target acknowledges (D6) before it is handed op.exec (moves §7.10: "the replacement box choose() names when the relocation leaves pinning").
8. The final TXID N is read from the remote after SyncAndWait returns with every writer stopped, as the newest level-0 MaxTXID (§5.8 release step 2). With writers stopped and the sync acknowledged, the stopped database's position and that listing agree; a sync error is returned, never swallowed (claim P6-D4).
9. stuck is a journal entry, not a phase. The claim says exhaustion "records stuck without resetting the count"; validateRelocating lists no stuck phase. MarkStuck writes journal.stuck and every relocation transition refuses afterwards; it refuses between installed and a probe.
10. The probe deadline starts at the probing CAS (journal.probing_since), and the worker moves a live target to probe-failed 10 minutes later.
11. A host whose source never had a writer (session 0, writer_box empty) is relocated with coverage "", which declares nothing (claim §6.4a: "a created incarnation's first admission … declares nothing"), never released. Rev 2: only by failover. A drain of such a host is refused at Worker.Start: root refuses stop evidence for writer session 0 (validateRequest), and 6b's collectCapturedStop waits for claim Plan 5's no-process witness (R4). Its failover pin is an evidenced empty one (ruling 15). Cost if wrong: a box with never-woken hosts cannot be drained until R4 lands; nothing is lost.
12. L18's owner. The coordination post on #236 says moves owns internal/sim/hostlife; claim rev 6.30 §1.1 calls the two-box model "region HA's own … as part of region HA's plan"; the moves conflicts note defers it to "a joint round with the region HA session". This plan writes no model and ends with a merge gate that names the cases; whichever session builds the model, relocation does not merge until that round passes for a one-box and a two-box region.
13. Moves revision. The brief cites moves rev 7.20; the branch reads 7.22. Rev 7.21 and 7.22 bind the prepared files manifest to P (R18-1, R19-1). Corrected in rev 15 (round 14 finding 1): until rev 14 this plan did not follow that binding, because it copied the source manifest's sequence into P. Under claim rev 6.30 (R18-1) and moves rev 7.22 §7.6, P's prepared manifest is create-only at sequence 0 and bound to {location, P, op id, installation stamp}. The first admission consumes it by exact version, and the session publisher starts at sequence 1. The source pin's sequence is provenance only (PreparedAuthority.SourceFilesSeq). CopyPinnedManifest writes sequence 0, and ToInstalled requires it and binds the stamp. Nothing in L14 to L17 changed against it.
14. The release deadline is 10 minutes (hostrelocate.ReleaseDeadline, rev 2). §5.8 says a flush that never reaches N, and a probe-failed target that cannot finish its release, go to stuck, and names no bound. ToReleasing and ToProbeFailed journal when the phase began; a worker marks the operation stuck once that long has passed with no release journaled. The host stays where it is: nothing moves away from a live box without its stop evidence. Cost if wrong: a number; the stuck state and the operator path are the claim's.
15. An empty pin needs evidence a writer can give (rev 2; claim §6.4a "Empty bootstrap": no LTX file exists until the first commit, so a listing that finds nothing is a definite observation but says nothing about who wrote). A pin is Empty only when the journaled release reports final_txid 0 (the stopped writer flushed and found nothing), or the holder never admitted a writer (session 0, failover). A failover of a host whose session is above 0 with an empty listing refuses and waits for an operator; JournalPin enforces it, the pinner never writes it. Cost if wrong: that one case recovers by hand until R6 names its evidence.
16. A pin is bound to the claim generation it was selected against (rev 2; B2-3). Its key is control/relocations/<host>/<op>/pin-<gen>.json and JournalPin requires gen to be the observed claim's. A pin whose journal CAS lost is abandoned where it lies (never referenced, cheap, reaped by the storage follow-up of ruling 5); the next pass selects afresh at the new generation. Every bound JournalPin checks (the release's positions, the failover window) is checked before the object is written, so a doomed pin is never published. Cost if wrong: abandoned objects under a prefix nothing reads.
17. Reconcile has three authorities for a relocation row (rev 2; §5.3, 6b's ClaimOwnership.Valid needs a stamp). The executor (the source until its fence closes, the target from installing on) activates its own installation stamp and mints or keeps its row through the guarded path. A kept row of a box that is no longer the executor (the source after its release, a replaced target) gets its hold through registry.SetClaimHold under the flock, conditional on the row's recorded ownership: a hold grants nothing, so it needs no installation authority. A target before installing has no installation and mints nothing; the edges file already withholds the host from a box that is not op.exec (§24). Cost if wrong: a request that reaches a pre-installation target meets the box's unknown-host answer instead of a hold, for the seconds between starting and installing.
18. Probe attempts are counted before they are made (rev 3; §5.8 "limits": at most three, then probe-failed). BeginProbeAttempt is one CAS per attempt, keyed by box, so a crash, a lost response or a restart never buys a fourth and a replacement target starts at zero; the participant enters probe-failed when refused. Cost if wrong: an attempt lost to a crash before its admission still counts; the bound is the spec's.
19. A relocation's execution controller is finished when its participation ends (rev 3). hostexec keeps the host's lifetime lock until Close, so the participant sweeps its retained controllers once per pass and closes every one whose operation the claim no longer runs with this box as a participant. The relocation controller's Cleanup hook is scoped: it retires only the relocation's own partial installation (an unopened P's local install) and does nothing once this box has admitted a writer under the operation or serves the host, so closing it after a successful relocation stops nothing. Rev 6: a durable record is cleared only straight after that scoped cleanup succeeds in the same call (Finish repeats it after Close, and on a restart), because hostexec reports a cleanup failure from Close once and nil afterwards; the participation is journaled before its controller opens, so a restart finds every record. The serving writer belongs to the wake assembly's own controller from its admission on. A completed operation's hold_op on the serving executor's row is cleared by reconcile under the activation's verified ownership; a running operation's hold is never touched. Cost if wrong: a scope rule in one hook; the lock release is hostexec's.
20. The pinned files manifest is retained by the pinner (rev 3; B2-4). Before the pin object exists, the exact manifest bytes are written create-only to control/relocations/<host>/<op>/manifest-<sha256>.json, and P's manifest is written from that copy, never from the source prefix again: a late revision of the source changes nothing an admitted pin reads. Cost if wrong: one small object per pin under the prefix ruling 5's storage follow-up covers.
21. The writers-stopped observation is root's (rev 3; L10 "a complete privileged descriptor scan"). The agent, uid carlos with CAP_NET_BIND_SERVICE alone, can read only its own descriptor table; it records the replicator's descriptors from /proc/self at open and asks root, over the authenticated instance-control socket, to make the complete scan with its cgroup manager (R3). An agent-side scan fails closed on the first unreadable table. Cost if wrong: one more root endpoint, beside the stop collector's.
22. An exhausted target that dies is fenced into a stuck pinning (rev 4; §5.8 "The bound": "never between installed and a probe" is a live target's safe point). Rev 9: that holds only when the dead target is op.exec, or op.exec is already "none". While the live source is op.exec (starting, releasing), the CAS consumes the target's fence and records stuck. It keeps the source's execution identity, phase and release evidence, because a target's fence is no evidence against the source (claim §4), and root's stop needs the source to remain op.exec. Otherwise FenceExhaustedTarget consumes the fence in one CAS, retains the loss, revokes the dead installation's authority and leaves the operation stuck at pinning with its pin, and P's remote build when nothing opened it, for the operator's replacement; nothing chooses a third target. Cost if wrong: the stuck state's shape; the operator path is the claim's.
23. Two stages (controller ruling, rev 5). Rounds 3 and 4 found most of their defects in the gated tasks' integration with 6b, itself unmerged and changing; polishing code against a moving plan does not converge. Stage A (Tasks 1 to 7, 9a) is build-ready: compiled, dry-run, every finding fixed in code. Stage B (8a, 8b, 8c, 9, 10) keeps its design and contracts; its code is rewritten against the real 6b code after it merges and re-reviewed then. Stage B findings are answered at the contract level: what must happen, which request covers it, which test proves it. The "Stage B re-plan" step lists every stage B obligation from rounds 1 to 4, so none is lost. Cost if wrong: a second review round on stage B after 6b lands; the alternative is tuning against text that will not survive.
24. An empty files pin needs positive evidence; otherwise the operation is stuck (rev 17, two-box model finding F2). H6 makes instance.key, report.token and <host>.env continuous on every plan, and §5.6 has every cold admission write its manifest create-only before the app starts. So a holder with an admitted writer and no manifest anywhere in its chain cannot be shown never to have minted them. Examples are an adopted legacy host whose files never published, or a first manifest that never landed. Installing an empty set there would mint a fresh key over data sealed with the old one. StorePinner pins an empty files set only when no writer was ever admitted (session 0), or when the stopped writer's release flush, which publishes every file whatever the setting, reported manifest_seq 0. Otherwise it returns ErrFilesUnevidenced, and the worker marks the operation stuck for an operator, as ruling 15 and R6 do for the database. The alternative, requiring the first manifest that carries instance.key to land before the first admission, cannot be built here. The key is written by the app, not the platform, and §5.6 already orders the admission's manifest copy before the app starts. That ordering is a stage B obligation on 6b's cold admission (the re-plan names its test). The window between the app minting a key and the publisher's next publish is §5.6's continuous-sync bound, raised for the joint round. Cost if wrong: a host with no manifest and no key is stuck until an operator resolves it, rather than relocated empty. Rev 18 (round 17 finding 1): an existing manifest is not evidence either. When a writer was admitted and the pinned database is nonempty, the pinned manifest must carry a live instance.key, the minimum of H6's always-continuous items. A manifest copied before the app started, with the key minted after and never published, refuses the pin, and the operation is stuck. The durability window itself is not closed by this plan. It is the open request L21, for Paul to choose between the platform pre-provisioning the key and the replicator holding until it lands. Cost if wrong (rev 18): an app that never writes instance.key and has a nonempty database is stuck on every relocation until an operator resolves it; H6 names the key as platform-managed on every plan, so such an app should not exist.
25. A drain's probe-failed with no eligible spare is stuck after ReleaseDeadline, never sent back to the source (rev 17, finding F1). §5.8 excludes to from the choice after a failed probe, and a relocation's target is never its source (the start CAS, replaceTargetSlot). Letting the live source be the "replacement" would put a fresh install of P' into the same host paths that the source's own park-local chore retires once the operation completes (§5.8, "What a relocation leaves behind"). The same box would then hold the retiring installation and the new one under one name. So the worker waits for a spare and, ReleaseDeadline after probe_failed_since, marks the operation stuck. This follows the spec's own bound ("It alerts, and the op waits for carlos ops host resolve"). The operator's resolve is the claim's: it may return the host to the source, as the model's ruling 13 does. Cost if wrong: in a two-box region a failed drain waits ten minutes plus an operator instead of an automatic return.
26. Every abandoned prepared generation is parked by the operation that built it (rev 17, finding F3). §5.8 says "an abandoned P is parked by the at-rest sweep". This plan adds an earlier owner: install journals every unopened P it replaces (abandoned_prepared), and CompleteRelocation queues a park-generation chore for each in the region, beside its park-local chores. The at-rest sweep stays the backstop for an operation that never completes. A P that any admission opened is part of the writer lineage and is never on the list. Cost if wrong: one chore per abandoned build. Its objects are outside every live set (a prepared manifest names the source's objects, not P's), so parking them retires nothing live.
27. D4's automatic loss is retained as evidence_refs (rev 2; claim §7.3 D3 "enrollment-qualified fence references in evidence_refs and stable loss identities in loss_refs"). hostclaim.AutomaticLoss holds the fence reference, its observation time, the box, enrollment and role, the box's last writer session, the discharge verdict, timer knowledge unknown and whether the console has reported it; the id is deterministic over (operation, box, fence) so a replayed transition dedupes. It lives beside loss_refs, outside op, and so survives the serving CAS. The console's materialization is after this plan (R5). Cost if wrong: a field name; the retention is what D4 requires.

Why this is 1b-next, and what it leaves out

Plan 1b built every part of rev 5.4 that needed none of L1 to L20. Since then claim Plans 1 to 8b and 5 landed on main (3407d114): the roster (hostactors.Directory), the fence writer (hostfence.TerminationWorker), the fence reader for claims (hostclaim.VerifyFence, hostfence.ClaimFenceAuthority), the execution controller (hostexec), stop receipts (host.ClaimStopCoordinator), the box-started census (Directory.CensusBoxRelocation) and H14's start check (Directory.CheckBoxStart). This plan uses all of them and duplicates none.

Left out, with where it goes:

• The placer loop that decides what to relocate (spec 3): reading the termination queue, relocating every host off a dead box in bounded parallel, rebalancing. This plan's worker starts a relocation when asked and replays any it finds; Task 10's pass only replays.
• Automatic enrollment and the cross-region confirmer (spec 4, H16, H17).
• The console's copy of a fence into a D4 loss record and the roster's retirement of the box (claim D4 "Automatic loss persistence"). The fence CAS keeps the reference and the discharge verdict in the operation journal and puts the box on lost; materializing the loss record is the console's, and is listed under "After this plan".
• Storage policy for control/relocations/ (ruling 5).

Global Constraints

• Dormant. Nothing changes on a box or console where CARLOS_REGION_HA is unset or not true (strconv.ParseBool), and it is read from /etc/carlos/host.env by regionHAEnabled (internal/host/boxrecord.go). With one box per region every rule is a no-op (spec §4, §8 step 2).
• Activation gate (claim §1.1, L18). "relocating and the rules it depends on (L1, L9 to L13) must not be enabled until region HA's own two-box-per-region model (L18) … validate[s] them." Relocation may not merge until Task 11's joint round passes.
• One implementation per concept; main's wins (#236). Do not write a termination-fence writer (hostfence.TerminationWorker writes control/box-fences/<enrollment>.json using termfence.Verify). Do not write a roster reader (hostactors.Directory). Read fences only through hostclaim.VerifyFence (in claim CASes) and hostactors.ValidateTerminationFence (before them).
• H19, verbatim: "The failover fence rests on the terminated read alone; disk evidence only decides discharge of local chores." No volume record gates a fence, a relocation step or an admission.
• Absence is never evidence (§5.9). A fence that cannot be read or does not validate is an error, never "not fenced"; a box missing from the roster refuses.
• Every phase change is one claim CAS conditional on op.id, the phase and the ETag (claim C2). Two workers racing make the same CAS and one gets hostclaim.ErrConflict.
• Exact values. Failover pin delay 30 seconds after the fence's observed_at (hostclaim.FailoverPinDelay); probe deadline 10 minutes (hostrelocate.ProbeDeadline); at most 2 target replacements per operation (hostclaim.MaxTargetReplacements); reconcile's kept-row sweep 10 minutes (H9); release deadline 10 minutes (hostrelocate.ReleaseDeadline, ruling 14); probe attempts 3 per target installation (hostclaim.MaxProbeAttempts, ruling 19); create intent keys selected_executor and executor_enrollment (claim P5-D6); journal fence key fence.<box> holding {"enrollment","key","sha256"} (claim §7.3); release obligation relocation-release; pin objects control/relocations/<host>/<op>/pin-<claim gen>.json (hostclaim.RecoveryPinKey, ruling 16); loss ids auto-<32 hex> over (op, box, fence); the retained manifest control/relocations/<host>/<op>/manifest-<sha256>.json (ruling 21); the env platform item host.env (hostfiles.EnvItem).
• Gated tasks. Tasks 8a, 8b, 8c, 9 and 10 start with a "Gated on" line. Their code is written against the interfaces claim Plan 6b rev 5 declares (ClaimAssembly, ClaimWakeAssembly, ClaimWakeInputs, CollectClaimStop, localStopIdentity, hostbox.ReconcileAdapter, registry.SetClaimHold), moves Phase 1 Plan 2 Task 8 declares (moves.BuildGeneration, BuildInputs, SealedObject, the key helpers) and moves Plan 1 Task 7b declares (RenderHeld, MaterializeHeld), plus the requests R1 to R3 and R7. They were not compiled. When 6b and moves land, re-read their merged code and bind the same contracts to the names they actually have; the un-gated tasks do not change.
• No new module dependencies. Do not add a method to release.Store. Linux-only syscalls in *_linux.go with a !linux stub; CI cross-compiles darwin, windows and linux/arm64.
• Copy. No user-facing copy. Errors and log lines are operator-facing and follow the surrounding style. If a task finds it needs console or CLI text, stop: it waits for Paul's copy review.
• Go environment. GOFLAGS=-buildvcs=false. Leave GOCACHE at its default; if the sandbox refuses it, GOCACHE=$TMPDIR/gocache for that command. Socket tests need TMPDIR=/tmp/k (mkdir -p /tmp/k). Run tests niced (nice -n 19), targeted with -run; never the full -race suite, and no simulation sweeps. Scratch goes under $TMPDIR.
• Gate before each commit: go build ./... && go vet ./<pkgs>/ && gofmt -l <dirs> (empty), the task's targeted tests, then GOOS=darwin go build ./... && GOOS=windows go build ./.... (GOOS=windows go vet ./internal/... fails on main's own test files, release/versions_test.go, appconfig/syncexec_test.go and activator/activator_test.go; vet the task's packages instead.)
• Commit messages: lowercase area: prefix and a sentence stating the behaviour, then a blank line and Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>. Work on a branch cut from origin/main (suggested region-ha-1b-next). Merging is Paul's call, through amadan branch merge, and only after Task 11.
• Dry run. Tasks 1 to 7 were applied in order to origin/main at 3407d114, built, vetted, cross-built for darwin, windows and linux/arm64, and their tests run; nineteen guards were each removed in turn and their test watched to fail (rev 1), then rev 2's twenty-five, rev 3's eleven, rev 4's eight, rev 5's seven, rev 6's eleven, rev 7's three, rev 8's two, rev 9's two, rev 10's one, rev 11's four, rev 12's four, rev 13's four, rev 14's ten killed mutations of the lifecycle property, rev 15's twelve, rev 16's, rev 17's eight, rev 18's five and rev 19's two (listed in the Self-review); from rev 10 on, stage A is also applied one task at a time in plan order, building and testing after each. Then the code was removed; only this document is committed.

Review Focus

1. released coverage naming the wrong predecessor. A drain's first probe admission declares nothing; if the session it vouches for is not exactly the one whose release was journaled (another box, another session, another generation), a real loss goes unrecorded. Expect refusal. Task 1, TestRelocationAdmissionRules/released_names_another_predecessor, …/released_names_another_predecessor_box, …/released_after_P_was_opened.
2. P opened twice. A restarted probe that restores P again loses everything attempt two replicated (B1-1). Expect every attempt after the first to take a fresh generation, and P refused. Task 1, TestRelocationAdmissionRules/a_third_attempt_reopens_P.
3. A failover pinned too early. Requests S3 accepted from the terminated box can still land; a pin taken before observed_at + 30 s widens H3's window. Expect the worker to wait and the claim to refuse. Task 1 TestRelocationFailoverCitesTheFenceAndDeclaresTheLoss, Task 5 TestWorkerPinsNoEarlierThanThirtySecondsAfterTheFence.
4. A fence that cannot be read taken as no fence. A garbled control/box-fences/ object must stop the drain and the create choice, not let them proceed as if the box were alive. Task 2 TestExecutorChooserNeverNamesAFencedLostOrUnknownBox/an_unreadable_fence, Task 5 TestWorkerTreatsAnUnreadableFenceAsAnErrorNeverAsNoFence.
5. A database descriptor in an unshared thread exempted as the replicator's. Writers-stopped allows only the replicator's identified descriptors; a thread whose table no longer matches the leader's must count as a writer. A matching number and path is not enough: the kernel must say the table and the description are shared (rev 7). Task 4, TestWritersStoppedRefusesAnyOtherHolder/a_thread's_descriptor_the_leader's_table_does_not_show, …/an_unshared_thread_at_the_leader's_number_and_path, TestProcessDescriptorsTellsSharedFromUnsharedThreadsByKernelIdentity.

File Structure

| Path | Responsibility | Task | |---|---|---| | internal/hostclaim/relocation.go | The relocation transitions: start (drain, failover), source loss, barrier, release journal, pin, install, local install receipt, probe, serving, target replacement, stuck; fences consumed in the same CAS | 1 | | internal/hostclaim/generation.go, claim.go | AdmitWriter's relocating phase table and released coverage (L1, L9); evidence_refs, the retained automatic loss (D4) | 1 | | internal/hostclaim/create.go | ExecutorSelection, BeginCreateOn; CompleteCreate never substitutes | 2 | | internal/console/server.go, cmd/console/main.go | Config.RegionHA from CARLOS_REGION_HA | 2 | | internal/hostops/executor.go, loads.go, operations.go, backfill.go, backfill_controller.go | ExecutorChooser over the roster, the edges snapshot and claim loads, and Permits; Authority.SelectExecutor before the create CAS, or today's create without one | 2 | | internal/hostbox/relocationrows.go, wakepolicy.go, internal/hostguard/admissionfence.go | §5.3's row cases; who may wake under relocating; the policy's relocation owner, its reconcile action and RelocationPolicy; the admission-fence reader | 3 | | internal/stopevidence/writers*.go | L10's writers-stopped observation; one process's descriptors on the database | 4 | | internal/hostrelocate/worker.go, pin.go, internal/hostfiles/manifestcheck.go | The regional worker: start (eligibility, shape), one replayed CAS per step, the pin under the location lease, the release deadline; the pinned recovery set by claim generation, ReadPin, CopyPinnedManifest | 5 | | internal/hostrelocate/participant.go | A participant box's transitions, ordered over its local effects | 6 | | internal/host/relocationreleases.go, relocationeffects.go, relocationflush.go, internal/hostfiles/platform.go | Stop receipts as release evidence; the release sequence inside root's stop collection (stop writers, observe, flush, record, drain); retained controllers; durable positions; the full files flush; EnvItem | 7 | | internal/host/relocationassembly.go | Gated: the release providers bound to 6b's assembly | 8a | | internal/host/relocationbuild.go | Gated: P's build under the lease; the Prepared verifier | 8b | | internal/host/relocationinstall.go, relocationwake.go | Gated: the local install under its stamp; the probe's inputs | 8c | | internal/hostbox/reconcile.go, 6b's reconcile_adapter.go | Gated: held rows and the 10-minute sweep | 9 | | internal/console/hostclaimexecutor.go | The console's create chooser (constructed, not yet used by a door) | 2 | | internal/host/relocatepass.go | Gated: the passes, behind CARLOS_REGION_HA, and the create door's chooser | 10 |

---

Task 1: The relocating operation in the claim library (L1, L2 to L4, L9, L11)

Spec §5.8 and claim §4. Every transition is a func(*Claim) error for hostclaim.Update, except the four that cite evidence read from storage (StartRelocation, FenceSource, PinAfterRelease, ReplaceTarget), which verify it first and then make one CAS, as ConvertMovingToRelocating does. A fence is consumed only through VerifyFence against the exact bytes its reference names; the CAS that relies on it journals fence.<box>, puts the box on lost, and records the discharge verdict (L3), discharging the box's park-local chores only when the verdict qualifies; the same CAS passes the box's regional work (park-generation, park-replica owned by box:<b>) to region:<r>, as DeclareLost does (rev 6). A box owing a park-local is never named a target (replaceTargetSlot, rev 6).

Files:

• Create: internal/hostclaim/relocation.go
• Modify: internal/hostclaim/generation.go (the AdmitWriter kind switch, the coverage switch, a new relocationAdmission), internal/hostclaim/claim.go (EvidenceRefs, validated)
• Test: internal/hostclaim/relocation_test.go

Interfaces:

• Consumes (main): Update, RequireOp, VerifyFence, FenceRef, FenceAuthority, AcknowledgeExecution, AdmitWriter, validBoxReference, isHex64, KindRelocating, validateRelocating.
• Produces: constants ReasonDrain|ReasonRebalance|ReasonFailover, PhaseStarting … PhaseProbeFailed, MaxTargetReplacements = 2, FailoverPinDelay = 30s; errors ErrRelocation, ErrReplacementsExceeded, ErrAlreadyRecorded; types RelocationStart, LocalDischarge, Release, ReleaseAuthority (VerifyRelease(ctx, Claim, Release) error), RecoveryPin (with Empty), PreparedAuthority (with FilesSeq, FilesManifestSHA256), LocalInstall, Probe, Target{Box, Enrollment}, AutomaticLoss (with Incarnation, Stamp, LastAdmission, Reassigned) and Claim.EvidenceRefs; OwesLocal(c, box) bool, LocalChoreBoxes(c) []string, PreparedOpened(c) bool; MaxProbeAttempts = 3, ErrProbeAttemptsExhausted; functions RecoveryPinKey(host, op string, gen uint64) string, BeginProbeAttempt(opID, box string), FenceExhaustedTarget(ctx, s, observed, opID, FenceRef, *LocalDischarge, FenceAuthority) (Observed, error), RelocationStartGuard(c, region, source, target string, sourceFenced bool) error, StartRelocation(ctx, s, observed, RelocationStart, FenceAuthority) (Observed, error), FenceSource(ctx, s, observed, opID, FenceRef, *LocalDischarge, FenceAuthority) (Observed, error), ToReleasing(opID, now time.Time), JournalRelease(opID, Release), PinAfterRelease(ctx, s, observed, opID, ReleaseAuthority, *Target) (Observed, error), PinFailover(opID), JournalPin(opID, RecoveryPin), NameTarget(opID, Target), ToInstalling(opID, Target, prepared string), ToInstalled(opID, PreparedAuthority), RecordLocalInstall(opID, LocalInstall), ToProbing(opID, now time.Time), RecordProbe(opID, Probe), ToProbeFailed(opID, now time.Time), CompleteRelocation(opID, newID func() string), ReplaceTarget(ctx, s, observed, opID, FenceRef, *LocalDischarge, next Target, prepared string, FenceAuthority) (Observed, error), MarkStuck(opID, reason).
• Journal keys later tasks read: exec_ack.<box>, fence.<box>, fence.<box>.observed_at, discharge.<box>, reason, releasing_since, release, release.phase, released_by_target, pin, prepared, install_stamp, installed_boxes, prepared_authority, local_install, probing_since, probe_attempts.<box>, probe, probe_failed_since, replacements, excluded_targets, stuck, prepared_opened (rev 12). Claim fields: evidence_refs, loss_refs.

• [ ] Step 1: Write the failing tests

internal/hostclaim/relocation_test.go:

package hostclaim

import (
	"context"
	"crypto/sha256"
	"encoding/hex"
	"encoding/json"
	"errors"
	"reflect"
	"slices"
	"strings"
	"testing"
	"time"

	"github.com/carlosframework/platform/internal/boxid"
	"github.com/carlosframework/platform/internal/release"
	"github.com/carlosframework/platform/internal/termfence"
)

const (
	relSource = "adi-knitting"
	relTarget = "bri-knitting"
	relSpare  = "cai-knitting"
	relSpare2 = "dov-knitting"
)

var relObserved = time.Date(2026, 10, 7, 9, 0, 0, 0, time.UTC)

func relEnrollment(box string) string { return strings.Repeat(string(box[0]), 32) }

// relAuthority accepts any fence record for a box in this region.
type relAuthority struct{}

func (relAuthority) ValidateFence(_ context.Context, f termfence.Record) (FenceBinding, error) {
	if f.Enrollment != relEnrollment(f.Box) {
		return FenceBinding{}, ErrFence
	}
	return FenceBinding{Region: "ie", RosterRevision: 9, RosterETag: "roster"}, nil
}

type relReleases struct{ err error }

func (r relReleases) VerifyRelease(context.Context, Claim, Release) error { return r.err }

func putFence(t *testing.T, s release.Store, box string) FenceRef {
	t.Helper()
	f := termfence.Record{V: 1, Box: box, Enrollment: relEnrollment(box), State: "terminated",
		Cloud:      boxid.Cloud{Provider: "aws", Account: "123", Region: "eu-west-1", InstanceID: "i-" + box},
		ObservedAt: relObserved.Format(time.RFC3339Nano), Via: "describe", RequestID: "req",
		WrittenBy: termfence.WrittenBy{Box: "worker", Enrollment: strings.Repeat("e", 32)}}
	raw, err := json.Marshal(f)
	if err != nil {
		t.Fatal(err)
	}
	sum := sha256.Sum256(raw)
	ref := FenceRef{Enrollment: f.Enrollment, Key: "control/box-fences/" + f.Enrollment + ".json", SHA256: hex.EncodeToString(sum[:])}
	if _, err := s.Put(context.Background(), ref.Key, raw, ""); err != nil && !errors.Is(err, release.ErrCASConflict) {
		t.Fatal(err)
	}
	return ref
}

// relServing is a serving claim on relSource whose source has admitted one
// cold writer session (generation g1).
func relServing(t *testing.T) (release.Store, Observed) {
	t.Helper()
	ctx := context.Background()
	s := release.NewDirStore(t.TempDir())
	o := servingClaim(t, ctx, s)
	o, err := Update(ctx, s, o, AdmitWriter(Admission{Box: relSource, Mode: "cold", NewGeneration: "g1", Region: "ie", KeepStamp: true}))
	if err != nil {
		t.Fatal(err)
	}
	return s, o
}

func relStart(reason string, fence *FenceRef) RelocationStart {
	return RelocationStart{OpID: "rel-1", By: "worker", Now: relObserved, Region: "ie", Reason: reason,
		SourceBox: relSource, SourceEnrollment: relEnrollment(relSource),
		TargetBox: relTarget, TargetEnrollment: relEnrollment(relTarget),
		DirectoryRevision: 9, AdmissionID: "adm-1", Fence: fence}
}

func step(t *testing.T, s release.Store, o Observed, tr func(*Claim) error) Observed {
	t.Helper()
	next, err := Update(context.Background(), s, o, tr)
	if err != nil {
		t.Fatal(err)
	}
	return next
}

func ack(box string) func(*Claim) error {
	return AcknowledgeExecution(box, ExecutionAcknowledgement{Op: "rel-1", Enrollment: relEnrollment(box), BootID: "boot", ControllerID: "ctl", LeaseETag: "lease", Expires: relObserved.Add(time.Hour)})
}

// relPin is a pin selected against o: its key names o's claim generation.
func relPin(o Observed, maxTXID uint64, seq int64, at time.Time) RecoveryPin {
	return RecoveryPin{Key: RecoveryPinKey(o.Claim.Host, "rel-1", o.Claim.Gen), SHA256: strings.Repeat("a", 64), Generation: "g1", MaxTXID: maxTXID, FilesManifest: "instances/x/files/g1/manifest.json", FilesSeq: seq, PinnedAt: at, Empty: maxTXID == 0}
}

func relPrepared(gen string, maxTXID uint64, filesSeq int64) PreparedAuthority {
	a := PreparedAuthority{Generation: gen, SnapshotTXID: maxTXID, FilesSeq: 0, SourceFilesSeq: filesSeq, FilesManifestSHA256: strings.Repeat("f", 64)}
	if maxTXID > 0 {
		a.InstallManifest, a.SHA256 = "m", strings.Repeat("c", 64)
	}
	return a
}

func localInstall(c *Claim) LocalInstall {
	return LocalInstall{Box: c.Op.Exec, Enrollment: relEnrollment(c.Op.Exec), InstallStamp: journalUint(c.Op, "install_stamp"), FilesManifestVersion: 3, JournalSHA256: strings.Repeat("b", 64)}
}

// toProbing drives an operation at pinning (with its pin) through
// installing, installed and the local install receipt into probing.
func toProbing(t *testing.T, s release.Store, o Observed, prepared string, maxTXID uint64) Observed {
	t.Helper()
	target := Target{Box: o.Claim.Op.Intent["target_box"], Enrollment: o.Claim.Op.Intent["target_enrollment"]}
	o = step(t, s, o, ToInstalling("rel-1", target, prepared))
	var pin RecoveryPin
	readJournal(o.Claim.Op, "pin", &pin)
	o = step(t, s, o, ToInstalled("rel-1", relPrepared(prepared, maxTXID, pin.FilesSeq)))
	o = step(t, s, o, RecordLocalInstall("rel-1", localInstall(o.Claim)))
	return step(t, s, o, ToProbing("rel-1", relObserved))
}

func TestRelocationDrainEndToEnd(t *testing.T) {
	ctx := context.Background()
	s, o := relServing(t)
	o, err := StartRelocation(ctx, s, o, relStart(ReasonDrain, nil), relAuthority{})
	if err != nil {
		t.Fatal(err)
	}
	if c := o.Claim; c.Op.Exec != relSource || c.Op.Phase != PhaseStarting || !slices.Equal(c.Op.Participants, []string{relSource, relTarget}) || c.Op.Intent["stamp_from"] == "" {
		t.Fatalf("start: %+v", c.Op)
	}
	if _, err := Update(ctx, s, o, ToReleasing("rel-1", relObserved)); !errors.Is(err, ErrRelocation) {
		t.Fatalf("barrier without acknowledgements: %v", err)
	}
	o = step(t, s, o, ack(relSource))
	o = step(t, s, o, ack(relTarget))
	o = step(t, s, o, ToReleasing("rel-1", relObserved))
	if o.Claim.Op.Journal["releasing_since"] == "" {
		t.Fatal("releasing did not start its deadline")
	}
	h := o.Claim.Holder
	rel := Release{ReleasedBy: relSource, Enrollment: relEnrollment(relSource), Generation: h.Generation, Session: h.Session, FinalTXID: 40, ManifestSeq: 7, Receipt: "control/stop/r.json", ReceiptSHA256: strings.Repeat("d", 64)}
	o = step(t, s, o, JournalRelease("rel-1", rel))
	if _, err := PinAfterRelease(ctx, s, o, "rel-1", relReleases{err: errors.New("bad receipt")}, nil); err == nil {
		t.Fatal("pinned on an unverified receipt")
	}
	if o, err = PinAfterRelease(ctx, s, o, "rel-1", relReleases{}, nil); err != nil {
		t.Fatal(err)
	}
	stamp := o.Claim.Holder.Stamp
	if o.Claim.Op.Exec != "none" || o.Claim.Op.Phase != PhasePinning {
		t.Fatalf("pinning: %+v", o.Claim.Op)
	}
	if _, err := Update(ctx, s, o, JournalPin("rel-1", relPin(o, 39, 7, relObserved))); !errors.Is(err, ErrRelocation) {
		t.Fatalf("pin short of the release: %v", err)
	}
	stale := relPin(o, 40, 7, relObserved)
	stale.Key = RecoveryPinKey(o.Claim.Host, "rel-1", o.Claim.Gen-1)
	if _, err := Update(ctx, s, o, JournalPin("rel-1", stale)); !errors.Is(err, ErrRelocation) {
		t.Fatalf("a pin selected against an earlier observation was journaled: %v", err)
	}
	o = step(t, s, o, JournalPin("rel-1", relPin(o, 40, 7, relObserved)))
	if o.Claim.Holder.Stamp != stamp {
		t.Fatal("pinning changed the stamp")
	}
	o = step(t, s, o, ToInstalling("rel-1", Target{relTarget, relEnrollment(relTarget)}, "P1"))
	for name, a := range map[string]PreparedAuthority{
		"no files manifest":     {Generation: "P1", InstallManifest: "m", SHA256: strings.Repeat("c", 64), SnapshotTXID: 40},
		"another files seq":     {Generation: "P1", InstallManifest: "m", SHA256: strings.Repeat("c", 64), SnapshotTXID: 40, FilesSeq: 6, FilesManifestSHA256: strings.Repeat("f", 64)},
		"no install manifest":   {Generation: "P1", SnapshotTXID: 40, FilesSeq: 7, FilesManifestSHA256: strings.Repeat("f", 64)},
		"another snapshot txid": {Generation: "P1", InstallManifest: "m", SHA256: strings.Repeat("c", 64), SnapshotTXID: 41, FilesSeq: 7, FilesManifestSHA256: strings.Repeat("f", 64)},
	} {
		if _, err := Update(ctx, s, o, ToInstalled("rel-1", a)); !errors.Is(err, ErrRelocation) {
			t.Fatalf("%s: installed on an incomplete build: %v", name, err)
		}
	}
	o = step(t, s, o, ToInstalled("rel-1", relPrepared("P1", 40, 7)))
	o = step(t, s, o, RecordLocalInstall("rel-1", localInstall(o.Claim)))
	o = step(t, s, o, ToProbing("rel-1", relObserved))
	install := journalUint(o.Claim.Op, "install_stamp")
	if o.Claim.Op.Exec != relTarget || o.Claim.Holder.Stamp != install || !slices.Contains(o.Claim.Touched.Boxes, relTarget) {
		t.Fatalf("installation: exec %s stamp %d install %d", o.Claim.Op.Exec, o.Claim.Holder.Stamp, install)
	}
	o = step(t, s, o, AdmitWriter(Admission{ObservedOpID: "rel-1", ObservedPhase: PhaseProbing, ObservedSession: o.Claim.Holder.Session, ObservedGeneration: o.Claim.Holder.Generation,
		Box: relTarget, Mode: "cold", NewGeneration: "P1", KeepStamp: true, Coverage: "released", Region: "ie", PredecessorRegion: "ie"}))
	last := o.Claim.Holder.Admissions[len(o.Claim.Holder.Admissions)-1]
	if last.Coverage != "released" || last.WritesLost != nil || o.Claim.Holder.Stamp != install {
		t.Fatalf("released admission: %+v stamp %d", last, o.Claim.Holder.Stamp)
	}
	o = step(t, s, o, RecordProbe("rel-1", Probe{Box: relTarget, Session: o.Claim.Holder.Session}))
	o = step(t, s, o, CompleteRelocation("rel-1", counter()))
	c := o.Claim
	if c.Op.Kind != KindServing || c.Op.ID != "" || c.Op.Exec != relTarget || !slices.Equal(c.Op.Participants, []string{relTarget}) {
		t.Fatalf("serving: %+v", c.Op)
	}
	if len(c.Obligations) != 1 || c.Obligations[0].Kind != "park-local" || c.Obligations[0].Box != relSource || c.Obligations[0].Op != "rel-1" {
		t.Fatalf("the source's park-local: %+v", c.Obligations)
	}
}

func TestRelocationFailoverCitesTheFenceAndDeclaresTheLoss(t *testing.T) {
	ctx := context.Background()
	for _, qualified := range []bool{false, true} {
		s, o := relServing(t)
		o = step(t, s, o, func(c *Claim) error { // a chore the dead source already owed
			c.Obligations = append(c.Obligations, Obligation{ID: "old", Op: "old-op", Kind: "park-local", Box: relSource, Retirement: "r", Owner: "box:" + relSource})
			return nil
		})
		ref := putFence(t, s, relSource)
		sourceSession := o.Claim.Holder.Session
		in := relStart(ReasonFailover, &ref)
		in.Discharge = &LocalDischarge{Qualified: qualified, Records: []string{"control/box-volumes/x/1.json"}}
		o, err := StartRelocation(ctx, s, o, in, relAuthority{})
		if err != nil {
			t.Fatal(err)
		}
		c := o.Claim
		if c.Op.Exec != "none" || !slices.Equal(c.Op.Participants, []string{relTarget}) || !slices.Contains(c.Lost, relSource) || c.Op.Journal["fence."+relSource] == "" {
			t.Fatalf("failover start: %+v lost %v", c.Op, c.Lost)
		}
		if owes := slices.ContainsFunc(c.Obligations, func(o Obligation) bool { return o.Box == relSource }); owes == qualified {
			t.Fatalf("discharge qualified=%v left chores %+v", qualified, c.Obligations)
		}
		if _, err := Update(ctx, s, o, ToReleasing("rel-1", relObserved)); err == nil {
			t.Fatal("a failover entered releasing")
		}
		o = step(t, s, o, ack(relTarget))
		o = step(t, s, o, PinFailover("rel-1"))
		if _, err := Update(ctx, s, o, JournalPin("rel-1", relPin(o, 40, 7, relObserved.Add(29*time.Second)))); !errors.Is(err, ErrRelocation) {
			t.Fatalf("pinned inside the 30-second window: %v", err)
		}
		o = step(t, s, o, JournalPin("rel-1", relPin(o, 40, 7, relObserved.Add(FailoverPinDelay))))
		o = toProbing(t, s, o, "P1", 40)
		probe := Admission{ObservedOpID: "rel-1", ObservedPhase: PhaseProbing, ObservedSession: o.Claim.Holder.Session, ObservedGeneration: o.Claim.Holder.Generation,
			Box: relTarget, Mode: "cold", NewGeneration: "P1", KeepStamp: true, Coverage: "released", Region: "ie", PredecessorRegion: "ie"}
		if _, err := Update(ctx, s, o, AdmitWriter(probe)); !errors.Is(err, ErrWrongState) {
			t.Fatalf("a failover admission claimed released coverage: %v", err)
		}
		probe.Coverage = ""
		o = step(t, s, o, AdmitWriter(probe))
		last := o.Claim.Holder.Admissions[len(o.Claim.Holder.Admissions)-1]
		if last.WritesLost == nil || last.WritesLost.Box != relSource || last.WritesLost.Generation != "g1" {
			t.Fatalf("failover must declare the source's session: %+v", last)
		}
		o = step(t, s, o, RecordProbe("rel-1", Probe{Box: relTarget, Session: o.Claim.Holder.Session}))
		o = step(t, s, o, CompleteRelocation("rel-1", counter()))
		owes := slices.ContainsFunc(o.Claim.Obligations, func(ob Obligation) bool { return ob.Kind == "park-local" && ob.Box == relSource })
		if owes == qualified {
			t.Fatalf("qualified=%v: source chores at serving %+v", qualified, o.Claim.Obligations)
		}
		// D4: the loss outlives the operation, with the console still to
		// materialize it (nothing here stands in for the console).
		c = o.Claim
		if len(c.EvidenceRefs) != 1 || len(c.LossRefs) != 1 || c.EvidenceRefs[0].ID != c.LossRefs[0] {
			t.Fatalf("retained losses after serving: %+v refs %v", c.EvidenceRefs, c.LossRefs)
		}
		l := c.EvidenceRefs[0]
		if l.Box != relSource || l.Fence != ref || l.ObservedAt != relObserved.Format(time.RFC3339Nano) || l.Op != "rel-1" || l.Role != "source" ||
			l.Session != sourceSession || l.Generation != "g1" || l.Discharge.Qualified != qualified || l.Timers != TimersUnknown || l.Reported {
			t.Fatalf("retained loss: %+v", l)
		}
		if c.Op.Journal != nil || !slices.Contains(c.Lost, relSource) {
			t.Fatalf("serving kept the journal, or lost the box: %+v %v", c.Op, c.Lost)
		}
	}
}

func TestRelocationSourceLossBecomesFailover(t *testing.T) {
	ctx := context.Background()
	for _, tc := range []struct {
		name      string
		prepare   func(*testing.T, release.Store, Observed) Observed
		wantPhase string
		wantExec  string
		wantParts []string
	}{
		{"starting before acknowledging", func(t *testing.T, s release.Store, o Observed) Observed { return o }, PhaseStarting, "none", []string{relTarget}},
		{"starting after acknowledging", func(t *testing.T, s release.Store, o Observed) Observed { return step(t, s, o, ack(relSource)) }, PhaseStarting, "none", []string{relTarget}},
		{"releasing before its receipt", func(t *testing.T, s release.Store, o Observed) Observed {
			o = step(t, s, step(t, s, o, ack(relSource)), ack(relTarget))
			return step(t, s, o, ToReleasing("rel-1", relObserved))
		}, PhasePinning, "none", []string{relTarget}},
		{"releasing after its receipt", func(t *testing.T, s release.Store, o Observed) Observed {
			o = step(t, s, step(t, s, o, ack(relSource)), ack(relTarget))
			o = step(t, s, o, ToReleasing("rel-1", relObserved))
			h := o.Claim.Holder
			return step(t, s, o, JournalRelease("rel-1", Release{ReleasedBy: relSource, Enrollment: relEnrollment(relSource), Generation: h.Generation, Session: h.Session, FinalTXID: 1, Receipt: "r", ReceiptSHA256: strings.Repeat("d", 64)}))
		}, PhaseReleasing, relSource, []string{relSource, relTarget}},
	} {
		t.Run(tc.name, func(t *testing.T) {
			s, o := relServing(t)
			o, err := StartRelocation(ctx, s, o, relStart(ReasonDrain, nil), relAuthority{})
			if err != nil {
				t.Fatal(err)
			}
			o = tc.prepare(t, s, o)
			stamp := o.Claim.Holder.Stamp
			o, err = FenceSource(ctx, s, o, "rel-1", putFence(t, s, relSource), nil, relAuthority{})
			if err != nil {
				t.Fatal(err)
			}
			c := o.Claim
			if c.Op.Phase != tc.wantPhase || c.Op.Exec != tc.wantExec || !slices.Equal(c.Op.Participants, tc.wantParts) || c.Holder.Stamp != stamp || !slices.Contains(c.Lost, relSource) {
				t.Fatalf("phase %s exec %s parts %v stamp %d lost %v", c.Op.Phase, c.Op.Exec, c.Op.Participants, c.Holder.Stamp, c.Lost)
			}
			if c.Op.Intent["reason"] != ReasonDrain {
				t.Fatal("the intent was rewritten")
			}
		})
	}
}

// relAtPhase starts a drain and drives it to phase. "probing+P" is probing
// after the first admission opened P.
func relAtPhase(t *testing.T, phase string) (release.Store, Observed) {
	t.Helper()
	ctx := context.Background()
	s, o := relServing(t)
	o, err := StartRelocation(ctx, s, o, relStart(ReasonDrain, nil), relAuthority{})
	if err != nil {
		t.Fatal(err)
	}
	o = step(t, s, step(t, s, o, ack(relSource)), ack(relTarget))
	if phase == PhaseStarting {
		return s, o
	}
	o = step(t, s, o, ToReleasing("rel-1", relObserved))
	if phase == PhaseReleasing {
		return s, o
	}
	h := o.Claim.Holder
	o = step(t, s, o, JournalRelease("rel-1", Release{ReleasedBy: relSource, Enrollment: relEnrollment(relSource), Generation: h.Generation, Session: h.Session, FinalTXID: 40, ManifestSeq: 7, Receipt: "r", ReceiptSHA256: strings.Repeat("d", 64)}))
	if o, err = PinAfterRelease(ctx, s, o, "rel-1", relReleases{}, nil); err != nil {
		t.Fatal(err)
	}
	o = step(t, s, o, JournalPin("rel-1", relPin(o, 40, 7, relObserved)))
	if phase == PhasePinning {
		return s, o
	}
	o = step(t, s, o, ToInstalling("rel-1", Target{relTarget, relEnrollment(relTarget)}, "P1"))
	if phase == PhaseInstalling {
		return s, o
	}
	o = step(t, s, o, ToInstalled("rel-1", relPrepared("P1", 40, 7)))
	if phase == PhaseInstalled {
		return s, o
	}
	o = step(t, s, o, RecordLocalInstall("rel-1", localInstall(o.Claim)))
	o = step(t, s, o, ToProbing("rel-1", relObserved))
	if phase == PhaseProbing {
		return s, o
	}
	o = step(t, s, o, AdmitWriter(Admission{ObservedOpID: "rel-1", ObservedPhase: PhaseProbing, ObservedSession: o.Claim.Holder.Session, ObservedGeneration: o.Claim.Holder.Generation,
		Box: relTarget, Mode: "cold", NewGeneration: "P1", KeepStamp: true, Coverage: "released", Region: "ie", PredecessorRegion: "ie"}))
	return s, o
}

func TestRelocationReplacementTable(t *testing.T) {
	ctx := context.Background()
	for _, tc := range []struct {
		at, wantPhase, wantExec string
		newStamp, keepP         bool
	}{
		{PhaseStarting, PhaseStarting, relSource, false, false},
		{PhaseReleasing, PhaseReleasing, relSource, false, false},
		{PhasePinning, PhasePinning, "none", false, false},
		{PhaseInstalling, PhaseInstalling, relSpare, true, false},
		{PhaseInstalled, PhaseInstalled, relSpare, true, true},
		{PhaseProbing, PhaseInstalled, relSpare, true, true},
		{"probing+P", PhasePinning, "none", false, false},
	} {
		t.Run(tc.at, func(t *testing.T) {
			s, o := relAtPhase(t, tc.at)
			before := o.Claim.Holder.Stamp
			o, err := ReplaceTarget(ctx, s, o, "rel-1", putFence(t, s, relTarget), nil, Target{relSpare, relEnrollment(relSpare)}, "P2", relAuthority{})
			if err != nil {
				t.Fatal(err)
			}
			c := o.Claim
			if c.Op.Phase != tc.wantPhase || c.Op.Exec != tc.wantExec || c.Op.Intent["target_box"] != relSpare || !slices.Contains(c.Lost, relTarget) || slices.Contains(c.Op.Participants, relTarget) {
				t.Fatalf("phase %s exec %s intent %v lost %v parts %v", c.Op.Phase, c.Op.Exec, c.Op.Intent, c.Lost, c.Op.Participants)
			}
			if (c.Holder.Stamp != before) != tc.newStamp {
				t.Fatalf("stamp %d -> %d", before, c.Holder.Stamp)
			}
			if tc.keepP && c.Op.Journal["prepared"] != "P1" {
				t.Fatalf("the unopened P must be reused: %q", c.Op.Journal["prepared"])
			}
			if c.Op.Journal["local_install"] != "" {
				t.Fatal("a replacement inherited its predecessor's receipt")
			}
			if tc.wantPhase == PhaseInstalled {
				if _, err := Update(ctx, s, o, ToProbing("rel-1", relObserved)); err == nil {
					t.Fatal("probing without the replacement's own local install")
				}
			}
		})
	}
}

func TestRelocationTwoReplacementsThenStuck(t *testing.T) {
	ctx := context.Background()
	s, o := relAtPhase(t, PhasePinning)
	var err error
	for _, next := range []string{relSpare, relSpare2} {
		old := o.Claim.Op.Intent["target_box"]
		if o, err = ReplaceTarget(ctx, s, o, "rel-1", putFence(t, s, old), nil, Target{next, relEnrollment(next)}, "", relAuthority{}); err != nil {
			t.Fatal(err)
		}
	}
	if _, err = ReplaceTarget(ctx, s, o, "rel-1", putFence(t, s, relSpare2), nil, Target{"eve-knitting", relEnrollment("eve-knitting")}, "", relAuthority{}); !errors.Is(err, ErrReplacementsExceeded) {
		t.Fatalf("third replacement: %v", err)
	}
	o = step(t, s, o, MarkStuck("rel-1", "two target replacements used"))
	if journalUint(o.Claim.Op, "replacements") != 2 {
		t.Fatal("stuck reset the count")
	}
	if _, err := Update(ctx, s, o, ToInstalling("rel-1", Target{relSpare2, relEnrollment(relSpare2)}, "P9")); !errors.Is(err, ErrRelocation) {
		t.Fatalf("a stuck operation moved: %v", err)
	}
}

func TestRelocationReplacementInReleasingAcknowledgesBeforePinning(t *testing.T) {
	ctx := context.Background()
	s, o := relAtPhase(t, PhaseReleasing)
	h := o.Claim.Holder
	o = step(t, s, o, JournalRelease("rel-1", Release{ReleasedBy: relSource, Enrollment: relEnrollment(relSource), Generation: h.Generation, Session: h.Session, FinalTXID: 40, ManifestSeq: 7, Receipt: "r", ReceiptSHA256: strings.Repeat("d", 64)}))
	o, err := ReplaceTarget(ctx, s, o, "rel-1", putFence(t, s, relTarget), nil, Target{relSpare, relEnrollment(relSpare)}, "", relAuthority{})
	if err != nil || o.Claim.Op.Phase != PhaseReleasing {
		t.Fatalf("replacement in releasing: %v %+v", err, o.Claim.Op)
	}
	if _, err := PinAfterRelease(ctx, s, o, "rel-1", relReleases{}, nil); !errors.Is(err, ErrRelocation) {
		t.Fatalf("left releasing before the replacement acknowledged: %v", err)
	}
	o = step(t, s, o, ack(relSpare))
	if o, err = PinAfterRelease(ctx, s, o, "rel-1", relReleases{}, nil); err != nil || o.Claim.Op.Phase != PhasePinning {
		t.Fatalf("after the acknowledgement: %v %+v", err, o.Claim.Op)
	}
}

func TestRelocationExhaustedTargetIsFencedIntoAStuckPinning(t *testing.T) {
	ctx := context.Background()
	exhaust := func(t *testing.T, s release.Store, o Observed) Observed {
		var err error
		for _, next := range []string{relSpare, relSpare2} {
			old := o.Claim.Op.Intent["target_box"]
			if o, err = ReplaceTarget(ctx, s, o, "rel-1", putFence(t, s, old), nil, Target{next, relEnrollment(next)}, "", relAuthority{}); err != nil {
				t.Fatal(err)
			}
		}
		return o
	}
	t.Run("before exhaustion it is a replacement", func(t *testing.T) {
		s, o := relAtPhase(t, PhasePinning)
		if _, err := FenceExhaustedTarget(ctx, s, o, "rel-1", putFence(t, s, relTarget), nil, relAuthority{}); !errors.Is(err, ErrRelocation) {
			t.Fatalf("fenced as exhausted with replacements left: %v", err)
		}
	})
	// Round 8 finding 1: while the live source is still op.exec, the
	// target's fence consumes the target and records stuck; the source's
	// execution identity, phase and release evidence stay.
	for _, phase := range []string{PhaseStarting, PhaseReleasing} {
		t.Run("dead while the source executes in "+phase, func(t *testing.T) {
			s, o := relAtPhase(t, phase)
			if phase == PhaseReleasing {
				h := o.Claim.Holder
				o = step(t, s, o, JournalRelease("rel-1", Release{ReleasedBy: relSource, Enrollment: relEnrollment(relSource), Generation: h.Generation, Session: h.Session, FinalTXID: 40, ManifestSeq: 7, Receipt: "r", ReceiptSHA256: strings.Repeat("d", 64)}))
			}
			o = exhaust(t, s, o)
			before := o.Claim
			ref := putFence(t, s, relSpare2)
			o, err := FenceExhaustedTarget(ctx, s, o, "rel-1", ref, nil, relAuthority{})
			if err != nil {
				t.Fatal(err)
			}
			c := o.Claim
			if c.Op.Phase != phase || c.Op.Exec != relSource || c.Holder.Stamp != before.Holder.Stamp || c.Op.Journal["stuck"] == "" ||
				!slices.Contains(c.Op.Participants, relSource) || slices.Contains(c.Op.Participants, relSpare2) || !slices.Contains(c.Lost, relSpare2) {
				t.Fatalf("the live source was revoked: %+v lost %v", c.Op, c.Lost)
			}
			for _, k := range []string{"release", "release.phase", "releasing_since", "exec_ack." + relSource} {
				if c.Op.Journal[k] != before.Op.Journal[k] {
					t.Fatalf("%s changed: %q -> %q", k, before.Op.Journal[k], c.Op.Journal[k])
				}
			}
			if phase == PhaseReleasing && c.Op.Journal["release"] == "" {
				t.Fatal("the source's release evidence was dropped")
			}
			if l := c.EvidenceRefs[len(c.EvidenceRefs)-1]; l.Box != relSpare2 || l.Fence != ref {
				t.Fatalf("the dead target's loss: %+v", c.EvidenceRefs)
			}
			if err := c.Validate(); err != nil {
				t.Fatal(err)
			}
		})
	}
	t.Run("dead after its local install, P unopened", func(t *testing.T) {
		s, o := relAtPhase(t, PhasePinning)
		o = exhaust(t, s, o)
		o = step(t, s, o, ack(relSpare2))
		o = step(t, s, o, ToInstalling("rel-1", Target{relSpare2, relEnrollment(relSpare2)}, "P1"))
		o = step(t, s, o, ToInstalled("rel-1", relPrepared("P1", 40, 7)))
		o = step(t, s, o, RecordLocalInstall("rel-1", localInstall(o.Claim)))
		if _, err := Update(ctx, s, o, MarkStuck("rel-1", "x")); !errors.Is(err, ErrRelocation) {
			t.Fatalf("MarkStuck between installed and a probe: %v", err)
		}
		ref := putFence(t, s, relSpare2)
		o, err := FenceExhaustedTarget(ctx, s, o, "rel-1", ref, nil, relAuthority{})
		if err != nil {
			t.Fatal(err)
		}
		c := o.Claim
		if c.Op.Phase != PhasePinning || c.Op.Exec != "none" || c.Op.Journal["stuck"] == "" || slices.Contains(c.Op.Participants, relSpare2) || !slices.Contains(c.Lost, relSpare2) ||
			c.Op.Journal["local_install"] != "" || c.Op.Journal["pin"] == "" || c.Op.Journal["prepared"] != "P1" || c.Op.Journal["prepared_authority"] == "" {
			t.Fatalf("exhausted and dead: %+v lost %v", c.Op, c.Lost)
		}
		if len(c.EvidenceRefs) != 3 || c.EvidenceRefs[2].Box != relSpare2 || c.EvidenceRefs[2].Fence != ref {
			t.Fatalf("the dead target's loss: %+v", c.EvidenceRefs)
		}
		if _, err := Update(ctx, s, o, ToInstalling("rel-1", Target{relSpare2, relEnrollment(relSpare2)}, "P2")); !errors.Is(err, ErrRelocation) {
			t.Fatalf("a stuck operation moved: %v", err)
		}
		if _, err := FenceExhaustedTarget(ctx, s, o, "rel-1", ref, nil, relAuthority{}); err == nil {
			t.Fatal("the fence was consumed twice")
		}
	})
	t.Run("dead after P was opened", func(t *testing.T) {
		s, o := relAtPhase(t, "probing+P")
		o = exhaust(t, s, o) // after P's admission each replacement is a nested pinning
		o = step(t, s, o, ack(relSpare2))
		o = step(t, s, o, JournalPin("rel-1", relPin(o, 60, 9, relObserved.Add(FailoverPinDelay))))
		o = step(t, s, o, ToInstalling("rel-1", Target{relSpare2, relEnrollment(relSpare2)}, "P3"))
		o = step(t, s, o, ToInstalled("rel-1", relPrepared("P3", 60, 9)))
		o = step(t, s, o, RecordLocalInstall("rel-1", localInstall(o.Claim)))
		o = step(t, s, o, ToProbing("rel-1", relObserved))
		o = step(t, s, o, AdmitWriter(Admission{ObservedOpID: "rel-1", ObservedPhase: PhaseProbing, ObservedSession: o.Claim.Holder.Session, ObservedGeneration: o.Claim.Holder.Generation,
			Box: relSpare2, Mode: "cold", NewGeneration: "P3", KeepStamp: true, Region: "ie", PredecessorRegion: "ie"}))
		o, err := FenceExhaustedTarget(ctx, s, o, "rel-1", putFence(t, s, relSpare2), nil, relAuthority{})
		if err != nil {
			t.Fatal(err)
		}
		c := o.Claim
		if c.Op.Phase != PhasePinning || c.Op.Exec != "none" || c.Op.Journal["stuck"] == "" || c.Op.Journal["pin"] != "" || c.Op.Journal["prepared"] != "" {
			t.Fatalf("nested stuck pinning: %+v", c.Op)
		}
	})
}

func TestRelocationProbeFailureIsANestedRelocation(t *testing.T) {
	ctx := context.Background()
	s, o := relAtPhase(t, "probing+P")
	o = step(t, s, o, ToProbeFailed("rel-1", relObserved))
	if o.Claim.Op.Journal["probe_failed_since"] == "" {
		t.Fatal("probe-failed did not start its release deadline")
	}
	h := o.Claim.Holder
	rel := Release{ReleasedBy: relTarget, Enrollment: relEnrollment(relTarget), Generation: h.Generation, Session: h.Session, FinalTXID: 55, ManifestSeq: 9, Receipt: "r2", ReceiptSHA256: strings.Repeat("d", 64)}
	o = step(t, s, o, JournalRelease("rel-1", rel))
	if _, err := PinAfterRelease(ctx, s, o, "rel-1", relReleases{}, &Target{relTarget, relEnrollment(relTarget)}); err == nil {
		t.Fatal("the failed target was named again")
	}
	o, err := PinAfterRelease(ctx, s, o, "rel-1", relReleases{}, &Target{relSpare, relEnrollment(relSpare)})
	if err != nil {
		t.Fatal(err)
	}
	if o.Claim.Op.Phase != PhasePinning || o.Claim.Op.Exec != "none" {
		t.Fatalf("nested relocation: %+v", o.Claim.Op)
	}
	if _, err := Update(ctx, s, o, JournalPin("rel-1", relPin(o, 54, 9, relObserved))); !errors.Is(err, ErrRelocation) {
		t.Fatalf("pin lost the probe's writes: %v", err)
	}
	o = step(t, s, o, JournalPin("rel-1", relPin(o, 55, 9, relObserved)))
	o = step(t, s, o, ack(relSpare))
	o = toProbing(t, s, o, "P2", 55)
	// released coverage on P2's opening: the predecessor is the failed
	// target's probe session, whose release this operation journaled.
	o = step(t, s, o, AdmitWriter(Admission{ObservedOpID: "rel-1", ObservedPhase: PhaseProbing, ObservedSession: o.Claim.Holder.Session, ObservedGeneration: o.Claim.Holder.Generation,
		Box: relSpare, Mode: "cold", NewGeneration: "P2", KeepStamp: true, Coverage: "released", Region: "ie", PredecessorRegion: "ie"}))
	o = step(t, s, o, RecordProbe("rel-1", Probe{Box: relSpare, Session: o.Claim.Holder.Session}))
	o = step(t, s, o, CompleteRelocation("rel-1", counter()))
	var owed []string
	for _, ob := range o.Claim.Obligations {
		owed = append(owed, ob.Box)
	}
	slices.Sort(owed)
	if !slices.Equal(owed, []string{relSource, relTarget}) {
		t.Fatalf("park-local owed by the source and the abandoned target: %v", owed)
	}
}

func TestRelocationAdmissionRules(t *testing.T) {
	ctx := context.Background()
	probe := func(o Observed, gen, coverage string) Admission {
		return Admission{ObservedOpID: "rel-1", ObservedPhase: o.Claim.Op.Phase, ObservedSession: o.Claim.Holder.Session, ObservedGeneration: o.Claim.Holder.Generation,
			Box: o.Claim.Op.Exec, Mode: "cold", NewGeneration: gen, Coverage: coverage, Region: "ie", PredecessorRegion: "ie"}
	}
	for _, tc := range []struct {
		name, at string
		admit    func(Observed) Admission
	}{
		{"the target admits in installing", PhaseInstalling, func(o Observed) Admission { return probe(o, "P1", "") }},
		{"the target admits in installed", PhaseInstalled, func(o Observed) Admission { return probe(o, "P1", "") }},
		{"the first probe skips P", PhaseProbing, func(o Observed) Admission { return probe(o, "other", "") }},
		{"P is opened twice", "probing+P", func(o Observed) Admission { return probe(o, "P1", "") }},
		{"released after P was opened", "probing+P", func(o Observed) Admission { return probe(o, "P3", "released") }},
		{"warm probe", PhaseProbing, func(o Observed) Admission {
			a := probe(o, "", "")
			a.Mode, a.PredecessorCertified = "warm", true
			return a
		}},
		{"the source claims released", PhaseStarting, func(o Observed) Admission { return probe(o, "g2", "released") }},
	} {
		t.Run(tc.name, func(t *testing.T) {
			s, o := relAtPhase(t, tc.at)
			if _, err := Update(ctx, s, o, AdmitWriter(tc.admit(o))); !errors.Is(err, ErrWrongState) {
				t.Fatalf("admitted: %v", err)
			}
		})
	}
	t.Run("released names another predecessor", func(t *testing.T) {
		s, o := relAtPhase(t, PhaseProbing)
		o.Claim.Holder.Admissions[len(o.Claim.Holder.Admissions)-1].Session++
		if _, err := Update(ctx, s, o, AdmitWriter(probe(o, "P1", "released"))); !errors.Is(err, ErrWrongState) {
			t.Fatalf("admitted: %v", err)
		}
	})
	t.Run("released names another predecessor box", func(t *testing.T) {
		s, o := relAtPhase(t, PhaseProbing)
		o.Claim.Holder.Admissions[len(o.Claim.Holder.Admissions)-1].Box = relSpare
		if _, err := Update(ctx, s, o, AdmitWriter(probe(o, "P1", "released"))); !errors.Is(err, ErrWrongState) {
			t.Fatalf("admitted: %v", err)
		}
	})
	t.Run("a third attempt reopens P", func(t *testing.T) {
		s, o := relAtPhase(t, "probing+P")
		o = step(t, s, o, AdmitWriter(probe(o, "P3", ""))) // attempt two: a fresh generation
		if _, err := Update(ctx, s, o, AdmitWriter(probe(o, "P1", ""))); !errors.Is(err, ErrWrongState) {
			t.Fatalf("P was opened again: %v", err)
		}
	})
	t.Run("released outside relocating", func(t *testing.T) {
		s, o := relServing(t)
		if _, err := Update(ctx, s, o, AdmitWriter(Admission{ObservedSession: o.Claim.Holder.Session, ObservedGeneration: o.Claim.Holder.Generation, Box: relSource, Mode: "cold", NewGeneration: "g2", Coverage: "released", Region: "ie"})); !errors.Is(err, ErrWrongState) {
			t.Fatalf("admitted: %v", err)
		}
	})
	t.Run("the source wakes in starting", func(t *testing.T) {
		s, o := relAtPhase(t, PhaseStarting)
		if _, err := Update(ctx, s, o, AdmitWriter(probe(o, "g2", ""))); err != nil {
			t.Fatal(err)
		}
	})
	t.Run("a stuck source does not wake", func(t *testing.T) {
		s, o := relAtPhase(t, PhaseStarting)
		o = step(t, s, o, MarkStuck("rel-1", "operator"))
		if _, err := Update(ctx, s, o, AdmitWriter(probe(o, "g2", ""))); !errors.Is(err, ErrWrongState) {
			t.Fatalf("admitted: %v", err)
		}
	})
}

func TestRelocationEmptyPinNeedsItsEvidence(t *testing.T) {
	ctx := context.Background()
	t.Run("a release at txid 0 vouches", func(t *testing.T) {
		s, o := relAtPhase(t, PhaseReleasing)
		h := o.Claim.Holder
		o = step(t, s, o, JournalRelease("rel-1", Release{ReleasedBy: relSource, Enrollment: relEnrollment(relSource), Generation: h.Generation, Session: h.Session, FinalTXID: 0, ManifestSeq: 0, Receipt: "r", ReceiptSHA256: strings.Repeat("d", 64)}))
		o, err := PinAfterRelease(ctx, s, o, "rel-1", relReleases{}, nil)
		if err != nil {
			t.Fatal(err)
		}
		o = step(t, s, o, JournalPin("rel-1", relPin(o, 0, 0, relObserved)))
		o = step(t, s, o, ToInstalling("rel-1", Target{relTarget, relEnrollment(relTarget)}, "P1"))
		if _, err := Update(ctx, s, o, ToInstalled("rel-1", relPrepared("P1", 40, 0))); !errors.Is(err, ErrRelocation) {
			t.Fatalf("an empty pin accepted a database build: %v", err)
		}
		if _, err := Update(ctx, s, o, ToInstalled("rel-1", PreparedAuthority{Generation: "P1", FilesSeq: 0})); !errors.Is(err, ErrRelocation) {
			t.Fatalf("an empty P without its files manifest: %v", err)
		}
		step(t, s, o, ToInstalled("rel-1", relPrepared("P1", 0, 0)))
	})
	t.Run("a release at txid 40 does not", func(t *testing.T) {
		s, o := relAtPhase(t, PhaseReleasing)
		h := o.Claim.Holder
		o = step(t, s, o, JournalRelease("rel-1", Release{ReleasedBy: relSource, Enrollment: relEnrollment(relSource), Generation: h.Generation, Session: h.Session, FinalTXID: 40, Receipt: "r", ReceiptSHA256: strings.Repeat("d", 64)}))
		o, err := PinAfterRelease(ctx, s, o, "rel-1", relReleases{}, nil)
		if err != nil {
			t.Fatal(err)
		}
		if _, err := Update(ctx, s, o, JournalPin("rel-1", relPin(o, 0, 0, relObserved))); !errors.Is(err, ErrRelocation) {
			t.Fatalf("an empty pin against a release at 40: %v", err)
		}
	})
	t.Run("a failover of a host that had a writer does not", func(t *testing.T) {
		s, o := relServing(t)
		ref := putFence(t, s, relSource)
		o, err := StartRelocation(ctx, s, o, relStart(ReasonFailover, &ref), relAuthority{})
		if err != nil {
			t.Fatal(err)
		}
		o = step(t, s, step(t, s, o, ack(relTarget)), PinFailover("rel-1"))
		if _, err := Update(ctx, s, o, JournalPin("rel-1", relPin(o, 0, 0, relObserved.Add(FailoverPinDelay)))); !errors.Is(err, ErrRelocation) {
			t.Fatalf("a listing that found nothing was taken as empty: %v", err)
		}
	})
	t.Run("a failover of a never-woken host does", func(t *testing.T) {
		s := release.NewDirStore(t.TempDir())
		o := servingClaim(t, ctx, s) // session 0: no writer was ever admitted
		ref := putFence(t, s, relSource)
		o, err := StartRelocation(ctx, s, o, relStart(ReasonFailover, &ref), relAuthority{})
		if err != nil {
			t.Fatal(err)
		}
		o = step(t, s, step(t, s, o, ack(relTarget)), PinFailover("rel-1"))
		step(t, s, o, JournalPin("rel-1", relPin(o, 0, 0, relObserved.Add(FailoverPinDelay))))
	})
}

func TestRelocationProbeAttemptsAreBounded(t *testing.T) {
	ctx := context.Background()
	s, o := relAtPhase(t, PhaseProbing)
	for i := 0; i < MaxProbeAttempts; i++ {
		o = step(t, s, o, BeginProbeAttempt("rel-1", relTarget))
	}
	if journalUint(o.Claim.Op, "probe_attempts."+relTarget) != MaxProbeAttempts {
		t.Fatalf("count: %v", o.Claim.Op.Journal)
	}
	if _, err := Update(ctx, s, o, BeginProbeAttempt("rel-1", relTarget)); !errors.Is(err, ErrProbeAttemptsExhausted) {
		t.Fatalf("a fourth attempt: %v", err)
	}
	if _, err := Update(ctx, s, o, BeginProbeAttempt("rel-1", relSpare)); !errors.Is(err, ErrRelocation) {
		t.Fatalf("a non-executor counted an attempt: %v", err)
	}
	// A replacement target has its own count.
	o, err := ReplaceTarget(ctx, s, o, "rel-1", putFence(t, s, relTarget), nil, Target{relSpare, relEnrollment(relSpare)}, "", relAuthority{})
	if err != nil {
		t.Fatal(err)
	}
	if journalUint(o.Claim.Op, "probe_attempts."+relSpare) != 0 {
		t.Fatal("the replacement inherited attempts")
	}
}

func TestRelocationDischargeCompletesDiscoveryLikeARetirement(t *testing.T) {
	ctx := context.Background()
	s, o := relServing(t)
	o = step(t, s, o, func(c *Claim) error {
		c.Touched.DiscoveryOp = "disc"
		c.Obligations = append(c.Obligations, Obligation{ID: "d1", Op: "disc", Kind: "park-local", Box: relSource, Retirement: "r", Owner: "box:" + relSource})
		return nil
	})
	ref := putFence(t, s, relSource)
	in := relStart(ReasonFailover, &ref)
	in.Discharge = &LocalDischarge{Qualified: true}
	o, err := StartRelocation(ctx, s, o, in, relAuthority{})
	if err != nil {
		t.Fatal(err)
	}
	if len(o.Claim.Obligations) != 0 || !o.Claim.Touched.Complete || o.Claim.Touched.DiscoveryOp != "" {
		t.Fatalf("discharging the final discovery chore: %+v touched %+v", o.Claim.Obligations, o.Claim.Touched)
	}
}

func TestRelocationLossRetainsAFormerWritersSession(t *testing.T) {
	// The source is fenced after the target's probe admission made the
	// target the writer: the loss still names the source's last session.
	ctx := context.Background()
	s, o := relAtPhase(t, "probing+P")
	before := o.Claim.Holder
	var sourceAdmission AdmissionRecord
	for _, a := range before.Admissions {
		if a.Box == relSource {
			sourceAdmission = a
		}
	}
	o, err := FenceSource(ctx, s, o, "rel-1", putFence(t, s, relSource), nil, relAuthority{})
	if err != nil {
		t.Fatal(err)
	}
	l := o.Claim.EvidenceRefs[0]
	if l.Box != relSource || l.Session != sourceAdmission.Session || l.Generation != sourceAdmission.Generation || l.LastAdmission == nil || !reflect.DeepEqual(*l.LastAdmission, sourceAdmission) ||
		l.Incarnation != before.Incarnation || l.Stamp != before.Stamp {
		t.Fatalf("retained: %+v, source admission %+v", l, sourceAdmission)
	}
	if err := o.Claim.Validate(); err != nil {
		t.Fatal(err)
	}
}

func TestRelocationRetainsEveryFencedBoxAcrossCompletion(t *testing.T) {
	// A drain whose target is terminated in installing: the replacement
	// completes, and the dead target's loss is still on the claim.
	ctx := context.Background()
	s, o := relAtPhase(t, PhaseInstalling)
	ref := putFence(t, s, relTarget)
	o, err := ReplaceTarget(ctx, s, o, "rel-1", ref, nil, Target{relSpare, relEnrollment(relSpare)}, "P2", relAuthority{})
	if err != nil {
		t.Fatal(err)
	}
	o = step(t, s, o, ack(relSpare))
	o = step(t, s, o, ToInstalled("rel-1", relPrepared("P2", 40, 7)))
	o = step(t, s, o, RecordLocalInstall("rel-1", localInstall(o.Claim)))
	o = step(t, s, o, ToProbing("rel-1", relObserved))
	o = step(t, s, o, AdmitWriter(Admission{ObservedOpID: "rel-1", ObservedPhase: PhaseProbing, ObservedSession: o.Claim.Holder.Session, ObservedGeneration: o.Claim.Holder.Generation,
		Box: relSpare, Mode: "cold", NewGeneration: "P2", KeepStamp: true, Coverage: "released", Region: "ie", PredecessorRegion: "ie"}))
	o = step(t, s, o, RecordProbe("rel-1", Probe{Box: relSpare, Session: o.Claim.Holder.Session}))
	o = step(t, s, o, CompleteRelocation("rel-1", counter()))
	c := o.Claim
	if len(c.EvidenceRefs) != 1 || c.EvidenceRefs[0].Box != relTarget || c.EvidenceRefs[0].Role != "target" || c.EvidenceRefs[0].Session != 0 || !slices.Contains(c.LossRefs, c.EvidenceRefs[0].ID) {
		t.Fatalf("the abandoned target's loss: %+v refs %v", c.EvidenceRefs, c.LossRefs)
	}
	if err := c.Validate(); err != nil {
		t.Fatal(err)
	}
}

func TestRelocationStartGuard(t *testing.T) {
	serving := func(obs ...Obligation) *Claim {
		return &Claim{Holder: &Holder{Incarnation: "i"}, Op: Op{Kind: KindServing, Exec: relSource}, Obligations: obs}
	}
	for _, tc := range []struct {
		name   string
		ob     Obligation
		fenced bool
		want   error
	}{
		{"park-generation in the region (L11)", Obligation{Kind: "park-generation", Region: "ie"}, false, nil},
		{"park-replica in the region", Obligation{Kind: "park-replica", Region: "ie"}, false, ErrPendingChore},
		{"park-replica elsewhere", Obligation{Kind: "park-replica", Region: "uk"}, false, nil},
		{"park-local on the target", Obligation{Kind: "park-local", Box: relTarget}, true, ErrPendingChore},
		{"park-local on a live source", Obligation{Kind: "park-local", Box: relSource}, false, ErrPendingChore},
		{"park-local on a fenced source", Obligation{Kind: "park-local", Box: relSource}, true, nil},
	} {
		t.Run(tc.name, func(t *testing.T) {
			if err := RelocationStartGuard(serving(tc.ob), "ie", relSource, relTarget, tc.fenced); !errors.Is(err, tc.want) {
				t.Fatalf("got %v, want %v", err, tc.want)
			}
		})
	}
}

func TestRelocationLocalInstallReceiptIsBound(t *testing.T) {
	ctx := context.Background()
	for _, tc := range []struct {
		name   string
		mutate func(*LocalInstall)
	}{
		{"another box", func(l *LocalInstall) { l.Box = relSpare }},
		{"another enrollment", func(l *LocalInstall) { l.Enrollment = relEnrollment(relSpare) }},
		{"a later writer stamp", func(l *LocalInstall) { l.InstallStamp++ }},
	} {
		t.Run(tc.name, func(t *testing.T) {
			s, o := relAtPhase(t, PhaseInstalled)
			l := localInstall(o.Claim)
			tc.mutate(&l)
			if _, err := Update(ctx, s, o, RecordLocalInstall("rel-1", l)); !errors.Is(err, ErrRelocation) {
				t.Fatalf("recorded: %v", err)
			}
		})
	}
	s, o := relAtPhase(t, PhaseInstalled)
	l := localInstall(o.Claim)
	o = step(t, s, o, RecordLocalInstall("rel-1", l))
	if _, err := Update(ctx, s, o, RecordLocalInstall("rel-1", l)); !errors.Is(err, ErrAlreadyRecorded) {
		t.Fatalf("replay: %v", err)
	}
	if _, err := Update(ctx, s, o, MarkStuck("rel-1", "operator")); !errors.Is(err, ErrRelocation) {
		t.Fatalf("stuck between installed and a probe: %v", err)
	}
	// B1-2: probing is refused on another box's receipt, even one in the journal.
	foreign := l
	foreign.Box = relSpare
	raw, _ := json.Marshal(foreign)
	o.Claim.Op.Journal["local_install"] = string(raw)
	if _, err := Update(ctx, s, o, ToProbing("rel-1", relObserved)); !errors.Is(err, ErrRelocation) {
		t.Fatalf("probing on another box's receipt: %v", err)
	}
}

// Round 5 finding 1: a spare that still owes a local retirement for the
// host is never named a replacement target, whatever phase the
// replacement resumes at (installing and installed hand it op.exec in the
// same CAS); a clean spare is.
func TestRelocationReplacementRefusesABoxOwingALocalRetirement(t *testing.T) {
	ctx := context.Background()
	for _, phase := range []string{PhaseStarting, PhaseInstalling, PhaseInstalled} {
		t.Run(phase, func(t *testing.T) {
			s, o := relAtPhase(t, phase)
			o = step(t, s, o, func(c *Claim) error {
				c.Obligations = append(c.Obligations, Obligation{ID: "old", Op: "old-op", Kind: "park-local", Box: relSpare, Retirement: "r", Owner: "box:" + relSpare})
				return nil
			})
			ref := putFence(t, s, relTarget)
			if _, err := ReplaceTarget(ctx, s, o, "rel-1", ref, nil, Target{relSpare, relEnrollment(relSpare)}, "P2", relAuthority{}); !errors.Is(err, ErrPendingChore) {
				t.Fatalf("a box owing park-local was named: %v", err)
			}
			if _, err := Update(ctx, s, o, NameTarget("rel-1", Target{relSpare, relEnrollment(relSpare)})); err == nil {
				t.Fatal("NameTarget named a box owing park-local")
			}
			o, err := ReplaceTarget(ctx, s, o, "rel-1", ref, nil, Target{relSpare2, relEnrollment(relSpare2)}, "P2", relAuthority{})
			if err != nil {
				t.Fatal(err)
			}
			c := o.Claim
			if c.Op.Intent["target_box"] != relSpare2 || slices.Contains(c.Op.Participants, relSpare) || slices.Contains(c.Touched.Boxes, relSpare) {
				t.Fatalf("the clean spare was not chosen: %+v touched %v", c.Op, c.Touched.Boxes)
			}
			if phase != PhaseStarting && c.Op.Exec != relSpare2 {
				t.Fatalf("exec %s", c.Op.Exec)
			}
		})
	}
}

// Round 5 finding 2: the automatic fence passes the dead box's regional
// work (park-generation, park-replica owned by box:<b>) to its region in
// the same CAS, as DeclareLost does for a declared loss, keeping every
// other field; another box's work is untouched; local discharge, qualified
// or not, changes nothing about it.
func TestRelocationFenceReassignsTheDeadBoxsRegionalWork(t *testing.T) {
	ctx := context.Background()
	gen := Obligation{ID: "pg", Op: "old-op", Kind: "park-generation", Region: "ie", Generation: "g0", Retirement: "rg", Owner: "box:" + relSource}
	rep := Obligation{ID: "pr", Op: "old-op", Kind: "park-replica", Region: "uk", Retirement: "rr", Owner: "box:" + relSource}
	other := Obligation{ID: "po", Op: "old-op", Kind: "park-generation", Region: "ie", Generation: "g0b", Retirement: "ro", Owner: "box:" + relSpare}
	local := Obligation{ID: "pl", Op: "old-op", Kind: "park-local", Box: relSource, Retirement: "rl", Owner: "box:" + relSource}
	for _, qualified := range []bool{false, true} {
		s, o := relServing(t)
		o = step(t, s, o, func(c *Claim) error {
			c.Obligations = append(c.Obligations, gen, rep, other, local)
			return nil
		})
		ref := putFence(t, s, relSource)
		in := relStart(ReasonFailover, &ref)
		in.Discharge = &LocalDischarge{Qualified: qualified, Records: []string{"control/box-volumes/x/1.json"}}
		o, err := StartRelocation(ctx, s, o, in, relAuthority{})
		if err != nil {
			t.Fatal(err)
		}
		byID := map[string]Obligation{}
		for _, ob := range o.Claim.Obligations {
			byID[ob.ID] = ob
		}
		wantGen, wantRep := gen, rep
		wantGen.Owner, wantRep.Owner = "region:ie", "region:uk"
		if !reflect.DeepEqual(byID["pg"], wantGen) || !reflect.DeepEqual(byID["pr"], wantRep) || !reflect.DeepEqual(byID["po"], other) {
			t.Fatalf("qualified=%v: regional work %+v", qualified, o.Claim.Obligations)
		}
		if _, owes := byID["pl"]; owes == qualified {
			t.Fatalf("qualified=%v: the local chore %+v", qualified, o.Claim.Obligations)
		}
		want := []ObligationRef{{ID: "pg", Op: "old-op", Retirement: "rg"}, {ID: "pr", Op: "old-op", Retirement: "rr"}}
		if len(o.Claim.EvidenceRefs) != 1 || !reflect.DeepEqual(o.Claim.EvidenceRefs[0].Reassigned, want) {
			t.Fatalf("qualified=%v: the retained loss does not name the reassignment: %+v", qualified, o.Claim.EvidenceRefs)
		}
		if err := o.Claim.Validate(); err != nil {
			t.Fatal(err)
		}
	}
}

// Round 11's sweep: P's opening is journaled with the admission that made
// it, so it survives AdmitWriter's trim of holder.admissions to eight. The
// removal below stands in for that trim (generation.go drops a covered,
// loss-archived head once more than eight are kept); with P's admission
// gone from the list, P is still opened: never reopened, and the local
// install is never remade.
func TestRelocationPOpenedOutlivesTheAdmissionTrim(t *testing.T) {
	ctx := context.Background()
	s, o := relAtPhase(t, "probing+P")
	if o.Claim.Op.Journal["prepared_opened"] != "P1" {
		t.Fatalf("the opening was not journaled: %+v", o.Claim.Op.Journal)
	}
	o = step(t, s, o, func(c *Claim) error {
		c.Holder.Admissions = slices.DeleteFunc(c.Holder.Admissions, func(a AdmissionRecord) bool { return a.Generation == "P1" })
		return nil
	})
	if !PreparedOpened(o.Claim) {
		t.Fatal("P forgotten with its admission")
	}
	again := Admission{ObservedOpID: "rel-1", ObservedPhase: PhaseProbing, ObservedSession: o.Claim.Holder.Session, ObservedGeneration: o.Claim.Holder.Generation,
		Box: relTarget, Mode: "cold", NewGeneration: "P1", KeepStamp: true, Region: "ie", PredecessorRegion: "ie"}
	if _, err := Update(ctx, s, o, AdmitWriter(again)); !errors.Is(err, ErrWrongState) {
		t.Fatalf("P reopened after the trim: %v", err)
	}
	if _, err := Update(ctx, s, o, RecordLocalInstall("rel-1", localInstall(o.Claim))); err == nil {
		t.Fatal("the local install was remade after P was opened")
	}
}

// Round 14 finding 1: P's prepared manifest is at sequence 0 whatever the
// source's; the pin's sequence (7 here) is its provenance. ToInstalled
// refuses a prepared manifest claimed at the source's sequence, and one
// built from another source revision, and binds the one it accepts to
// the installation stamp.
func TestRelocationPreparedManifestIsSequenceZero(t *testing.T) {
	ctx := context.Background()
	s, o := relAtPhase(t, PhaseInstalling)
	var pin RecoveryPin
	readJournal(o.Claim.Op, "pin", &pin)
	if pin.FilesSeq != 7 {
		t.Fatalf("pin at %d", pin.FilesSeq)
	}
	atSource := relPrepared("P1", 40, 7)
	atSource.FilesSeq = 7
	if _, err := Update(ctx, s, o, ToInstalled("rel-1", atSource)); !errors.Is(err, ErrRelocation) {
		t.Fatalf("a prepared manifest at the source's sequence: %v", err)
	}
	if _, err := Update(ctx, s, o, ToInstalled("rel-1", relPrepared("P1", 40, 6))); !errors.Is(err, ErrRelocation) {
		t.Fatalf("a prepared manifest from another source revision: %v", err)
	}
	o = step(t, s, o, ToInstalled("rel-1", relPrepared("P1", 40, 7)))
	var a PreparedAuthority
	readJournal(o.Claim.Op, "prepared_authority", &a)
	if a.FilesSeq != 0 || a.SourceFilesSeq != 7 || a.InstallStamp == 0 || a.InstallStamp != journalUint(o.Claim.Op, "install_stamp") {
		t.Fatalf("journaled authority: %+v", a)
	}
}

// Two-box model finding F3: a target replaced in installing leaves its P
// unopened; the replacement builds P'. The serving CAS queues a
// park-generation for P in the region, and none for the opened P'.
func TestRelocationParksEveryAbandonedPreparedGeneration(t *testing.T) {
	ctx := context.Background()
	s, o := relAtPhase(t, PhaseInstalling)
	o, err := ReplaceTarget(ctx, s, o, "rel-1", putFence(t, s, relTarget), nil, Target{relSpare, relEnrollment(relSpare)}, "P2", relAuthority{})
	if err != nil {
		t.Fatal(err)
	}
	var abandoned []string
	if !readJournal(o.Claim.Op, "abandoned_prepared", &abandoned) || !slices.Equal(abandoned, []string{"P1"}) {
		t.Fatalf("abandoned: %v", abandoned)
	}
	o = step(t, s, o, ack(relSpare))
	o = step(t, s, o, ToInstalled("rel-1", relPrepared("P2", 40, 7)))
	o = step(t, s, o, RecordLocalInstall("rel-1", localInstall(o.Claim)))
	o = step(t, s, o, ToProbing("rel-1", relObserved))
	o = step(t, s, o, AdmitWriter(Admission{ObservedOpID: "rel-1", ObservedPhase: PhaseProbing, ObservedSession: o.Claim.Holder.Session, ObservedGeneration: o.Claim.Holder.Generation,
		Box: relSpare, Mode: "cold", NewGeneration: "P2", KeepStamp: true, Coverage: "released", Region: "ie", PredecessorRegion: "ie"}))
	o = step(t, s, o, RecordProbe("rel-1", Probe{Box: relSpare, Session: o.Claim.Holder.Session}))
	o = step(t, s, o, CompleteRelocation("rel-1", counter()))
	var parks []string
	for _, ob := range o.Claim.Obligations {
		if ob.Kind == "park-generation" && ob.Region == "ie" && ob.Owner == "region:ie" {
			parks = append(parks, ob.Generation)
		}
	}
	if !slices.Contains(parks, "P1") || slices.Contains(parks, "P2") {
		t.Fatalf("park-generation chores: %v (%+v)", parks, o.Claim.Obligations)
	}
	if err := o.Claim.Validate(); err != nil {
		t.Fatal(err)
	}
}

// Round 17 finding 3: the target's probe deadline passes before any
// admission (P1 unopened), it releases in probe-failed, then it is
// terminated; the replacement's default branch drops P1. It is recorded
// first, so the completion of the nested relocation parks it.
func TestRelocationParksAPDroppedFromProbeFailed(t *testing.T) {
	ctx := context.Background()
	s, o := relAtPhase(t, PhaseProbing)
	if PreparedOpened(o.Claim) {
		t.Fatal("P1 was opened")
	}
	o = step(t, s, o, ToProbeFailed("rel-1", relObserved))
	o, err := ReplaceTarget(ctx, s, o, "rel-1", putFence(t, s, relTarget), nil, Target{relSpare, relEnrollment(relSpare)}, "", relAuthority{})
	if err != nil {
		t.Fatal(err)
	}
	if o.Claim.Op.Phase != PhasePinning || o.Claim.Op.Journal["prepared"] != "" {
		t.Fatalf("nested: %+v", o.Claim.Op)
	}
	var abandoned []string
	if !readJournal(o.Claim.Op, "abandoned_prepared", &abandoned) || !slices.Equal(abandoned, []string{"P1"}) {
		t.Fatalf("abandoned: %v", abandoned)
	}
	o = step(t, s, o, ack(relSpare))
	o = step(t, s, o, JournalPin("rel-1", relPin(o, 40, 7, relObserved.Add(FailoverPinDelay))))
	o = toProbing(t, s, o, "P2", 40)
	o = step(t, s, o, AdmitWriter(Admission{ObservedOpID: "rel-1", ObservedPhase: PhaseProbing, ObservedSession: o.Claim.Holder.Session, ObservedGeneration: o.Claim.Holder.Generation,
		Box: relSpare, Mode: "cold", NewGeneration: "P2", KeepStamp: true, Region: "ie", PredecessorRegion: "ie"}))
	o = step(t, s, o, RecordProbe("rel-1", Probe{Box: relSpare, Session: o.Claim.Holder.Session}))
	o = step(t, s, o, CompleteRelocation("rel-1", counter()))
	parked := false
	for _, ob := range o.Claim.Obligations {
		if ob.Kind == "park-generation" && ob.Generation == "P1" && ob.Region == "ie" {
			parked = true
		}
	}
	if !parked {
		t.Fatalf("P1 was not parked: %+v", o.Claim.Obligations)
	}
}

• [ ] Step 2: Run them to see them fail

Run: nice -n 19 go test ./internal/hostclaim/ -run 'Relocation' -count=1 Expected: FAIL to compile: undefined: RelocationStart, undefined: StartRelocation, and the rest.

• [ ] Step 3: Write the transitions

internal/hostclaim/relocation.go:

package hostclaim

import (
	"context"
	"crypto/sha256"
	"encoding/hex"
	"encoding/json"
	"errors"
	"fmt"
	"slices"
	"strconv"
	"time"

	"github.com/carlosframework/platform/internal/release"
)

// Relocation (claim §4 "Same-region relocation", region HA spec 1 §5.8):
// the reasons, the phases and the bound on target replacements.
const (
	ReasonDrain     = "drain"
	ReasonRebalance = "rebalance"
	ReasonFailover  = "failover"

	PhaseStarting    = "starting"
	PhaseReleasing   = "releasing"
	PhasePinning     = "pinning"
	PhaseInstalling  = "installing"
	PhaseInstalled   = "installed"
	PhaseProbing     = "probing"
	PhaseProbeFailed = "probe-failed"

	// MaxTargetReplacements is spec 1 §5.8's bound: after two
	// replacements of the target in one operation it goes to stuck.
	MaxTargetReplacements = 2

	// MaxProbeAttempts is §5.8's probe bound: at most three admissions
	// per target installation within the probe deadline; running out is
	// probe-failed. Attempts are counted in the claim before they are
	// made, so a crash or a lost response never buys a fourth.
	MaxProbeAttempts = 3

	// FailoverPinDelay is §5.8's failover pin rule: pin no earlier than
	// the fence's observed_at plus 30 seconds, so requests S3 had already
	// accepted from the terminated box have completed (H3's window).
	FailoverPinDelay = 30 * time.Second
)

var (
	ErrRelocation             = errors.New("hostclaim: relocation transition refused")
	ErrReplacementsExceeded   = errors.New("hostclaim: relocation has used its target replacements")
	ErrAlreadyRecorded        = errors.New("hostclaim: relocation journal entry already recorded")
	ErrProbeAttemptsExhausted = errors.New("hostclaim: the target has used its probe attempts")
)

// RelocationStart is the start CAS's intent (spec 1 §5.8, claim §4). Fence
// is set for a failover only and names the source's termination fence.
type RelocationStart struct {
	OpID, By                    string
	Now                         time.Time
	Region, Reason              string
	SourceBox, SourceEnrollment string
	TargetBox, TargetEnrollment string
	DirectoryRevision           uint64
	AdmissionID                 string
	Fence                       *FenceRef
	Discharge                   *LocalDischarge
}

// LocalDischarge is a fenced box's volume evidence (claim D5 as amended by
// L3, spec 1 §5.9, H19): the volume records the caller read and judged with
// boxvolumes.Discharge. When it is nil, or Qualified is false, the box's
// park-local chores stay open for the operator path. It never gates the
// fence or the relocation.
type LocalDischarge struct {
	Qualified bool     `json:"qualified"`
	Records   []string `json:"records,omitempty"`
	Reason    string   `json:"reason,omitempty"`
}

// Release is the journal entry a live box writes after its release
// sequence (spec 1 §5.8 steps 1 to 4): its stopped database's final TXID,
// its final files manifest sequence and its full stop receipt.
type Release struct {
	ReleasedBy    string `json:"released_by"`
	Enrollment    string `json:"enrollment"`
	Generation    string `json:"generation"`
	Session       uint64 `json:"session"`
	FinalTXID     uint64 `json:"final_txid"`
	ManifestSeq   int64  `json:"manifest_seq"`
	Receipt       string `json:"receipt"`
	ReceiptSHA256 string `json:"receipt_sha256"`
}

// ReleaseAuthority verifies a journaled release's full stop receipt: the
// immutable object at Receipt hashes to ReceiptSHA256 and is complete stop
// evidence (claim §6.1, P6-D1) for this host, operation, box, incarnation
// and session. Plan 6b's receipt format is its only implementation.
type ReleaseAuthority interface {
	VerifyRelease(context.Context, Claim, Release) error
}

// RecoveryPin is the journal's reference to one pinned recovery set
// (§5.8 "The pinned recovery set"): the immutable pin object holding the
// exact versions, its digest, the database position it reaches, the files
// manifest it pins, and when it was taken.
type RecoveryPin struct {
	Key           string    `json:"key"`
	SHA256        string    `json:"sha256"`
	Generation    string    `json:"generation"`
	MaxTXID       uint64    `json:"max_txid"`
	FilesManifest string    `json:"files_manifest"`
	FilesSeq      int64     `json:"files_seq"`
	PinnedAt      time.Time `json:"pinned_at"`
	// Empty is the evidenced empty bootstrap (claim §6.4a "Empty
	// bootstrap", spec 1 §5.8 "A host with nothing replicated"): no LTX
	// file exists because no transaction was ever committed. It is legal
	// only when a journaled release reports final_txid 0, or the holder
	// never admitted a writer (session 0). A listing that merely finds
	// nothing is never evidence (JournalPin refuses it).
	Empty bool `json:"empty,omitempty"`
}

// RecoveryPinKey is where the pin selected against claim generation gen
// lives: control/relocations/<host>/<op>/pin-<gen>.json. The key binds the
// object to the exact observation it was selected against, so a pin whose
// journal CAS lost (the claim moved) is abandoned, never reused, and a
// retry selects afresh at the new generation (B2-3's round binding).
func RecoveryPinKey(host, op string, gen uint64) string {
	return "control/relocations/" + host + "/" + op + "/pin-" + strconv.FormatUint(gen, 10) + ".json"
}

// PreparedAuthority is the `installed` CAS's record of the remote build
// (§5.8 "Building the prepared generation"): the install manifest of
// generation P, verified complete by a fresh read.
type PreparedAuthority struct {
	Generation      string `json:"generation"`
	InstallManifest string `json:"install_manifest"`
	SHA256          string `json:"sha256"`
	SnapshotTXID    uint64 `json:"snapshot_txid"`
	// FilesSeq and FilesManifestSHA256 identify P's prepared files
	// manifest (claim rev 6.30 R18-1, moves rev 7.22 §7.6): create-only,
	// at sequence 0, never replaced; FilesManifestSHA256 is the digest of
	// the exact bytes a fresh read verified, the exact version the first
	// admission consumes as its baseline (the session publisher then
	// starts at sequence 1). SourceFilesSeq is provenance, not identity:
	// the pinned source manifest's sequence it was built from, which must
	// be the pin's (rev 15, round 14 finding 1). Required always, an empty
	// bootstrap included: a P without its files manifest is not built.
	FilesSeq            int64  `json:"files_seq"`
	SourceFilesSeq      int64  `json:"source_files_seq"`
	FilesManifestSHA256 string `json:"files_manifest_sha256"`
	// InstallStamp binds the prepared manifest to the installation that
	// built it ({location, P, op id, installation stamp}): ToInstalled
	// sets it from install_stamp in the CAS that journals the authority.
	InstallStamp uint64 `json:"install_stamp,omitempty"`
}

// AutomaticLoss is claim §7.3 D4's "Automatic loss persistence": what the
// transition that consumed a termination fence retains on the claim itself,
// outside the replaceable operation, until the console materializes the
// D4 host loss record. It survives CompleteRelocation, free and holder
// replacement because it lives beside loss_refs, not in op.journal.
type AutomaticLoss struct {
	ID         string   `json:"id"` // the loss identity, also in loss_refs
	Box        string   `json:"box"`
	Enrollment string   `json:"enrollment"`
	Fence      FenceRef `json:"fence"`
	ObservedAt string   `json:"observed_at"`
	Op         string   `json:"op"`
	Kind       string   `json:"kind"`
	Phase      string   `json:"phase"`
	Role       string   `json:"role"` // "source" | "target"
	// Incarnation and Stamp bind the loss to the holder it was taken
	// against; Generation and Session are the box's last writer session,
	// whether it is still the writer or was superseded, and LastAdmission
	// is that session's admission record when the claim holds one (the
	// consequences the console reports: its coverage and declarations).
	Incarnation   string           `json:"incarnation"`
	Stamp         uint64           `json:"stamp"`
	Generation    string           `json:"generation,omitempty"`
	Session       uint64           `json:"session,omitempty"`
	LastAdmission *AdmissionRecord `json:"last_admission,omitempty"`
	Discharge     LocalDischarge   `json:"discharge"`
	// Reassigned is the regional work (park-generation, park-replica)
	// the box owned that the same CAS passed to its region (L3, as
	// DeclareLost's reassign_regional): the console's D4 record names it.
	Reassigned []ObligationRef `json:"reassigned,omitempty"`
	Timers     TimerKnowledge  `json:"timers"`
	// Reported is set by the console once the D4 record holds this loss
	// and its alert work exists. Until then reporting is pending.
	Reported bool `json:"reported,omitempty"`
}

// automaticLossID is deterministic for one fence consumed by one
// operation for one box, so a replayed transition names the same loss and
// the console's materialization deduplicates on it (D4: "Retries
// deduplicate by the retained loss identity").
func automaticLossID(opID, box string, ref FenceRef) string {
	sum := sha256.Sum256([]byte(opID + "\x00" + box + "\x00" + ref.Enrollment + "\x00" + ref.SHA256))
	return "auto-" + hex.EncodeToString(sum[:16])
}

// LocalInstall is one box's local install receipt (§5.8, B1-2, B2-5).
type LocalInstall struct {
	Box                  string `json:"box"`
	Enrollment           string `json:"enrollment"`
	InstallStamp         uint64 `json:"install_stamp"`
	FilesManifestVersion int64  `json:"files_manifest_version"`
	JournalSHA256        string `json:"journal_sha256"`
}

// Probe is the target's journaled probe result for its admitted session.
type Probe struct {
	Box     string `json:"box"`
	Session uint64 `json:"session"`
}

// Target names a box for the relocation's target slot.
type Target struct {
	Box, Enrollment string
}

func journalJSON(c *Claim, key string, v any) error {
	raw, err := json.Marshal(v)
	if err != nil {
		return err
	}
	if c.Op.Journal == nil {
		c.Op.Journal = map[string]string{}
	}
	c.Op.Journal[key] = string(raw)
	return nil
}

func readJournal(op Op, key string, v any) bool {
	raw, ok := op.Journal[key]
	return ok && json.Unmarshal([]byte(raw), v) == nil
}

func journalUint(op Op, key string) uint64 {
	n, _ := strconv.ParseUint(op.Journal[key], 10, 64)
	return n
}

func requireRelocation(c *Claim, opID string, phases ...string) error {
	if err := RequireOp(opID)(c); err != nil {
		return err
	}
	if c.Holder == nil || c.Op.Kind != KindRelocating || !slices.Contains(phases, c.Op.Phase) {
		return fmt.Errorf("%w: %s/%s", ErrWrongState, c.Op.Kind, c.Op.Phase)
	}
	if c.Op.Journal["stuck"] != "" {
		return fmt.Errorf("%w: operation is stuck", ErrRelocation)
	}
	ensureJournal(c)
	return nil
}

// ensureJournal makes the journal writable: an empty one round-trips as nil.
func ensureJournal(c *Claim) {
	if c.Op.Journal == nil {
		c.Op.Journal = map[string]string{}
	}
}

// requireAcks is the D6 barrier: every current participant has recorded
// its execution acknowledgement before the operation leaves its phase.
func requireAcks(c *Claim) error {
	for _, box := range c.Op.Participants {
		if c.Op.Journal["exec_ack."+box] == "" {
			return fmt.Errorf("%w: %s has not acknowledged", ErrRelocation, box)
		}
	}
	return nil
}

func failover(op Op) bool {
	return op.Intent["reason"] == ReasonFailover || op.Journal["reason"] == ReasonFailover
}

// RelocationStartGuard is §4's start guard with the relocation exception
// (L11): a park-generation chore in the region does not block, a
// park-replica in the region does, a park-local on the target does, and a
// park-local on a fenced source does not block a failover.
func RelocationStartGuard(c *Claim, region, source, target string, sourceFenced bool) error {
	if c.Holder == nil || c.Op.Kind != KindServing || c.Op.ID != "" {
		return fmt.Errorf("%w: kind %q", ErrWrongState, c.Op.Kind)
	}
	for _, o := range c.Obligations {
		switch {
		case o.Kind == "park-replica" && o.Region == region:
			return fmt.Errorf("%w: park-replica in %s", ErrPendingChore, region)
		case o.Kind == "park-local" && o.Box == target:
			return fmt.Errorf("%w: park-local on %s", ErrPendingChore, target)
		case o.Kind == "park-local" && o.Box == source && !sourceFenced:
			return fmt.Errorf("%w: park-local on %s", ErrPendingChore, source)
		}
	}
	return nil
}

// OwesLocal reports whether box owes a park-local chore on this claim: a
// local retirement not yet done (spec 1 §2: such a box is never chosen to
// install the host, and §4: a park-local on the target refuses).
func OwesLocal(c *Claim, box string) bool {
	for _, o := range c.Obligations {
		if o.Kind == "park-local" && o.Box == box {
			return true
		}
	}
	return false
}

// LocalChoreBoxes lists every box that owes a park-local chore on the
// claim, for a chooser's exclusions.
func LocalChoreBoxes(c *Claim) []string {
	var out []string
	for _, o := range c.Obligations {
		if o.Kind == "park-local" && o.Box != "" && !slices.Contains(out, o.Box) {
			out = append(out, o.Box)
		}
	}
	return out
}

// fenceBox puts box on lost with its fence reference (L2, L4), passes the
// regional work the box owned (park-generation, park-replica owned by
// box:<box>) to its region, region:<r>, keeping each obligation's id,
// operation, retirement, region, generation and park scope (L3, exactly
// as DeclareLost does for a declared loss, lost.go), and, when the volume
// evidence qualifies (L3), discharges that box's park-local chores for
// this host, all in the same CAS. It never removes anything else. D4: the
// same CAS retains the loss outside the operation (evidence_refs,
// loss_refs) with the box's last writer session, the discharge verdict and
// timer knowledge "unknown", so the console can materialize the loss record
// after the operation is long gone.
func fenceBox(c *Claim, box string, ref FenceRef, observedAt string, d *LocalDischarge) error {
	key := "fence." + box
	raw, err := json.Marshal(ref)
	if err != nil {
		return err
	}
	if old, ok := c.Op.Journal[key]; ok && old != string(raw) {
		return fmt.Errorf("%w: fence reference already bound", ErrFence)
	}
	if c.Op.Journal == nil {
		c.Op.Journal = map[string]string{}
	}
	c.Op.Journal[key] = string(raw)
	c.Op.Journal[key+".observed_at"] = observedAt
	if !slices.Contains(c.Lost, box) {
		c.Lost = append(c.Lost, box)
	}
	var reassigned []ObligationRef
	for i := range c.Obligations {
		o := &c.Obligations[i]
		if (o.Kind == "park-generation" || o.Kind == "park-replica") && o.Owner == "box:"+box {
			if o.Region == "" {
				return fmt.Errorf("%w: regional obligation %q names no region", ErrWrongState, o.ID)
			}
			o.Owner = "region:" + o.Region
			reassigned = append(reassigned, ObligationRef{ID: o.ID, Op: o.Op, Retirement: o.Retirement})
		}
	}
	if d == nil {
		d = &LocalDischarge{Reason: "no volume evidence supplied"}
	}
	if err := journalJSON(c, "discharge."+box, d); err != nil {
		return err
	}
	if d.Qualified {
		// Each chore is completed with CompleteObligation's own semantics,
		// so a discovery operation whose final chore this discharges is
		// marked complete exactly as a retirement would (delete.go).
		for {
			var chore *Obligation
			for i := range c.Obligations {
				if c.Obligations[i].Kind == "park-local" && c.Obligations[i].Box == box {
					chore = &c.Obligations[i]
					break
				}
			}
			if chore == nil {
				break
			}
			if err := CompleteObligation(chore.Op, chore.ID)(c); err != nil {
				return err
			}
		}
	}
	return retainAutomaticLoss(c, box, ref, observedAt, *d, reassigned)
}

// retainAutomaticLoss is D4's retention, written once per (operation, box,
// fence): a replay finds its record and changes nothing.
func retainAutomaticLoss(c *Claim, box string, ref FenceRef, observedAt string, d LocalDischarge, reassigned []ObligationRef) error {
	id := automaticLossID(c.Op.ID, box, ref)
	for _, l := range c.EvidenceRefs {
		if l.ID == id {
			return nil
		}
	}
	role := "target"
	if box == c.Op.Intent["source_box"] {
		role = "source"
	}
	loss := AutomaticLoss{ID: id, Box: box, Enrollment: ref.Enrollment, Fence: ref, ObservedAt: observedAt,
		Op: c.Op.ID, Kind: c.Op.Kind, Phase: c.Op.Phase, Role: role, Discharge: d, Reassigned: reassigned, Timers: TimersUnknown}
	if h := c.Holder; h != nil {
		loss.Incarnation, loss.Stamp = h.Incarnation, h.Stamp
		// The box's last writer session: the live one when it is still
		// the writer, otherwise its last admission on this holder.
		if h.WriterBox == box {
			loss.Generation, loss.Session = h.Generation, h.Session
		}
		for i := len(h.Admissions) - 1; i >= 0; i-- {
			if h.Admissions[i].Box == box {
				last := h.Admissions[i]
				loss.LastAdmission = &last
				if loss.Session == 0 {
					loss.Generation, loss.Session = last.Generation, last.Session
				}
				break
			}
		}
	}
	c.EvidenceRefs = append(c.EvidenceRefs, loss)
	if !slices.Contains(c.LossRefs, id) {
		c.LossRefs = append(c.LossRefs, id)
	}
	return nil
}

func removeParticipant(c *Claim, box string) {
	c.Op.Participants = slices.DeleteFunc(slices.Clone(c.Op.Participants), func(b string) bool { return b == box })
}

func addParticipant(c *Claim, box string) {
	if !slices.Contains(c.Op.Participants, box) {
		c.Op.Participants = append(c.Op.Participants, box)
	}
}

// installedBoxes is every box this operation handed op.exec for an
// installation; each gets a park-local unless discharged (claim §4:
// "Every abandoned local installation receives an exact park-local").
func noteInstalledBox(c *Claim, box string) error {
	var boxes []string
	readJournal(c.Op, "installed_boxes", &boxes)
	if !slices.Contains(boxes, box) {
		boxes = append(boxes, box)
	}
	return journalJSON(c, "installed_boxes", boxes)
}

// StartRelocation is the start CAS (spec 1 §5.8, claim §4). A drain or
// rebalance starts with op.exec on the source; a failover cites the
// source's termination fence, starts with op.exec "none", keeps the stamp,
// and puts the source on lost. The caller has already checked the roster
// (hostactors.Directory.CheckBoxStart), the target's eligibility and the
// app-admission registration; this CAS records what it checked.
func StartRelocation(ctx context.Context, s release.Store, observed Observed, in RelocationStart, authority FenceAuthority) (Observed, error) {
	if observed.Absent || observed.Claim == nil || observed.ETag == "" {
		return Observed{}, ErrWrongState
	}
	switch in.Reason {
	case ReasonDrain, ReasonRebalance:
		if in.Fence != nil {
			return Observed{}, fmt.Errorf("%w: only a failover cites a fence", ErrRelocation)
		}
	case ReasonFailover:
		if in.Fence == nil {
			return Observed{}, fmt.Errorf("%w: a failover cites the source's fence", ErrRelocation)
		}
	default:
		return Observed{}, fmt.Errorf("%w: reason %q", ErrRelocation, in.Reason)
	}
	if in.OpID == "" || in.Region == "" || in.AdmissionID == "" || in.DirectoryRevision == 0 || in.Now.IsZero() ||
		!validBoxReference(in.SourceBox) || !validBoxReference(in.TargetBox) || in.SourceBox == "none" || in.TargetBox == "none" ||
		in.SourceBox == in.TargetBox || in.SourceEnrollment == "" || in.TargetEnrollment == "" {
		return Observed{}, fmt.Errorf("%w: incomplete start", ErrRelocation)
	}
	var observedAt string
	if in.Fence != nil {
		v, err := VerifyFence(ctx, s, authority, *in.Fence)
		if err != nil {
			return Observed{}, err
		}
		if v.record.Box != in.SourceBox || v.record.Enrollment != in.SourceEnrollment || v.binding.Region != in.Region {
			return Observed{}, ErrFence
		}
		observedAt = v.record.ObservedAt
	}
	return Update(ctx, s, observed, func(c *Claim) error {
		if c.Op.Exec != in.SourceBox || slices.Contains(c.Lost, in.TargetBox) {
			return fmt.Errorf("%w: the source is not the executor, or the target is lost", ErrWrongState)
		}
		if err := RelocationStartGuard(c, in.Region, in.SourceBox, in.TargetBox, in.Fence != nil); err != nil {
			return err
		}
		exec, participants := in.SourceBox, []string{in.SourceBox, in.TargetBox}
		if in.Fence != nil {
			exec, participants = "none", []string{in.TargetBox}
		}
		c.Op = Op{Kind: KindRelocating, ID: in.OpID, Phase: PhaseStarting, By: in.By, StartedAt: in.Now.UTC(),
			Exec: exec, Participants: participants,
			Intent: map[string]string{
				"region": in.Region, "reason": in.Reason,
				"source_box": in.SourceBox, "source_enrollment": in.SourceEnrollment,
				"target_box": in.TargetBox, "target_enrollment": in.TargetEnrollment,
				"stamp_from":         strconv.FormatUint(c.Holder.Stamp, 10),
				"generation_from":    c.Holder.Generation,
				"directory_revision": strconv.FormatUint(in.DirectoryRevision, 10),
				"admission_id":       in.AdmissionID,
			},
			Journal: map[string]string{}}
		if in.Fence != nil {
			return fenceBox(c, in.SourceBox, *in.Fence, observedAt, in.Discharge)
		}
		return nil
	})
}

// FenceSource is §5.8's source-loss rule (B1-6): a drain or rebalance
// whose source is terminated becomes a failover in one CAS citing the
// source's fence. In starting it stays in starting with the source off the
// barrier; in releasing before a release is journaled it goes to pinning
// with the fence as evidence; after a release (pinning on) the source only
// goes on lost. Every case keeps the stamp and the intent.
func FenceSource(ctx context.Context, s release.Store, observed Observed, opID string, ref FenceRef, d *LocalDischarge, authority FenceAuthority) (Observed, error) {
	if observed.Absent || observed.Claim == nil {
		return Observed{}, ErrWrongState
	}
	before := observed.Claim.Op
	source := before.Intent["source_box"]
	v, err := VerifyFence(ctx, s, authority, ref)
	if err != nil {
		return Observed{}, err
	}
	if v.record.Box != source || v.record.Enrollment != before.Intent["source_enrollment"] || v.binding.Region != before.Intent["region"] {
		return Observed{}, ErrFence
	}
	return Update(ctx, s, observed, func(c *Claim) error {
		if err := RequireOp(opID)(c); err != nil {
			return err
		}
		if c.Op.Kind != KindRelocating || c.Op.Intent["source_box"] != source {
			return ErrWrongState
		}
		ensureJournal(c)
		// Before its release is journaled the source's writes are not
		// kept by a release, so the op becomes a failover. After it, only
		// the source's liveness changes.
		if c.Op.Phase == PhaseStarting || (c.Op.Phase == PhaseReleasing && c.Op.Journal["release"] == "") {
			c.Op.Journal["reason"] = ReasonFailover
			removeParticipant(c, source)
			c.Op.Exec = "none"
			if c.Op.Phase == PhaseReleasing {
				c.Op.Phase = PhasePinning
			}
		}
		return fenceBox(c, source, ref, v.record.ObservedAt, d)
	})
}

// ToReleasing is a drain's barrier CAS: from starting, once every
// participant has acknowledged. A failover never enters releasing. now
// starts the release deadline (hostrelocate.ReleaseDeadline): a source
// that never journals its release goes to stuck.
func ToReleasing(opID string, now time.Time) func(*Claim) error {
	return func(c *Claim) error {
		if err := requireRelocation(c, opID, PhaseStarting); err != nil {
			return err
		}
		if failover(c.Op) {
			return fmt.Errorf("%w: a failover skips releasing", ErrRelocation)
		}
		if err := requireAcks(c); err != nil {
			return err
		}
		if now.IsZero() {
			return fmt.Errorf("%w: releasing needs its start time", ErrRelocation)
		}
		c.Op.Phase = PhaseReleasing
		c.Op.Journal["releasing_since"] = now.UTC().Format(time.RFC3339Nano)
		return nil
	}
}

// JournalRelease records a live box's completed release sequence. The
// source records it in releasing; a failed target in probe-failed. The
// release must be of the box's own current writer session.
func JournalRelease(opID string, r Release) func(*Claim) error {
	return func(c *Claim) error {
		if err := requireRelocation(c, opID, PhaseReleasing, PhaseProbeFailed); err != nil {
			return err
		}
		h := c.Holder
		writerMismatch := h.Session != 0 && h.WriterBox != r.ReleasedBy // a host never woken has no writer
		if r.ReleasedBy == "" || r.ReleasedBy != c.Op.Exec || r.Enrollment == "" || r.Receipt == "" || !isHex64(r.ReceiptSHA256) ||
			r.Generation != h.Generation || r.Session != h.Session || writerMismatch {
			return fmt.Errorf("%w: release is not the executor's current session", ErrRelocation)
		}
		want := c.Op.Intent["source_enrollment"]
		if c.Op.Phase == PhaseProbeFailed {
			want = c.Op.Intent["target_enrollment"]
		}
		if r.Enrollment != want {
			return fmt.Errorf("%w: release enrollment", ErrRelocation)
		}
		var old Release
		if readJournal(c.Op, "release", &old) && c.Op.Journal["release.phase"] == c.Op.Phase {
			if old == r {
				return ErrAlreadyRecorded
			}
			return fmt.Errorf("%w: a different release is journaled", ErrRelocation)
		}
		c.Op.Journal["release.phase"] = c.Op.Phase
		return journalJSON(c, "release", r)
	}
}

// PinAfterRelease leaves releasing (a drain) or probe-failed (a failed
// target, §5.8's nested relocation) for pinning, citing the journaled
// release's verified receipt. op.exec becomes "none" and the stamp is kept
// (claim R6-4, D5's non-installing form). From probe-failed, next names
// the replacement target, which must not be the failed one.
func PinAfterRelease(ctx context.Context, s release.Store, observed Observed, opID string, authority ReleaseAuthority, next *Target) (Observed, error) {
	if observed.Absent || observed.Claim == nil || authority == nil {
		return Observed{}, ErrWrongState
	}
	var r Release
	if !readJournal(observed.Claim.Op, "release", &r) {
		return Observed{}, fmt.Errorf("%w: no journaled release", ErrRelocation)
	}
	if err := authority.VerifyRelease(ctx, *observed.Claim, r); err != nil {
		return Observed{}, err
	}
	return Update(ctx, s, observed, func(c *Claim) error {
		if err := requireRelocation(c, opID, PhaseReleasing, PhaseProbeFailed); err != nil {
			return err
		}
		var now Release
		if !readJournal(c.Op, "release", &now) || now != r || c.Op.Journal["release.phase"] != c.Op.Phase || r.ReleasedBy != c.Op.Exec {
			return fmt.Errorf("%w: release changed", ErrRelocation)
		}
		if c.Op.Phase == PhaseReleasing {
			if next != nil {
				return fmt.Errorf("%w: a drain keeps its target", ErrRelocation)
			}
			// §5.8: a target replaced in releasing acknowledges before the
			// operation leaves the phase.
			if err := requireAcks(c); err != nil {
				return err
			}
		} else {
			if next == nil || next.Box == r.ReleasedBy {
				return fmt.Errorf("%w: a nested relocation names another target", ErrRelocation)
			}
			if err := replaceTargetSlot(c, *next); err != nil {
				return err
			}
			c.Op.Journal["released_by_target"] = r.ReleasedBy
		}
		c.Op.Exec, c.Op.Phase = "none", PhasePinning
		delete(c.Op.Journal, "pin")
		return nil
	})
}

// PinFailover leaves starting for pinning on a failover: the source's
// fence is journaled and every remaining participant has acknowledged.
func PinFailover(opID string) func(*Claim) error {
	return func(c *Claim) error {
		if err := requireRelocation(c, opID, PhaseStarting); err != nil {
			return err
		}
		if !failover(c.Op) || c.Op.Journal["fence."+c.Op.Intent["source_box"]] == "" || c.Op.Exec != "none" {
			return fmt.Errorf("%w: pinning without a release needs the source's fence", ErrRelocation)
		}
		if err := requireAcks(c); err != nil {
			return err
		}
		c.Op.Phase = PhasePinning
		return nil
	}
}

// JournalPin records the pinned recovery set in pinning. The pin's key
// must be RecoveryPinKey for this claim generation: the object was selected
// against exactly this observation (B2-3). After a release it must reach
// the journaled final TXID and files sequence; on a failover it must be
// taken no earlier than the fence's observed_at plus FailoverPinDelay. An
// Empty pin needs its evidence: a release at final_txid 0, or a holder
// that never admitted a writer.
func JournalPin(opID string, p RecoveryPin) func(*Claim) error {
	return func(c *Claim) error {
		if err := requireRelocation(c, opID, PhasePinning); err != nil {
			return err
		}
		if p.Key != RecoveryPinKey(c.Host, opID, c.Gen) {
			return fmt.Errorf("%w: pin %s was not selected against this observation (gen %d)", ErrRelocation, p.Key, c.Gen)
		}
		if !isHex64(p.SHA256) || p.FilesManifest == "" || p.PinnedAt.IsZero() || (p.Empty != (p.MaxTXID == 0)) {
			return fmt.Errorf("%w: incomplete pin", ErrRelocation)
		}
		var r Release
		released := readJournal(c.Op, "release", &r)
		if released {
			if p.MaxTXID < r.FinalTXID || p.FilesSeq < r.ManifestSeq {
				return fmt.Errorf("%w: pin %d/%d is short of the release's %d/%d", ErrRelocation, p.MaxTXID, p.FilesSeq, r.FinalTXID, r.ManifestSeq)
			}
		}
		if p.Empty && !((released && r.FinalTXID == 0) || (!released && c.Holder.Session == 0)) {
			return fmt.Errorf("%w: an empty pin needs a release at txid 0 or a holder that never had a writer", ErrRelocation)
		}
		for key, at := range c.Op.Journal {
			if len(key) > len(".observed_at") && key[len(key)-len(".observed_at"):] == ".observed_at" {
				t, err := time.Parse(time.RFC3339Nano, at)
				if err != nil || p.PinnedAt.Before(t.Add(FailoverPinDelay)) {
					return fmt.Errorf("%w: pinned before the fence's observation plus %s", ErrRelocation, FailoverPinDelay)
				}
			}
		}
		if readJournal(c.Op, "pin", new(RecoveryPin)) {
			return ErrAlreadyRecorded
		}
		return journalJSON(c, "pin", p)
	}
}

// NameTarget names the target of an operation that has none: a move
// converted to relocating before its flip (claim §4, moves §7.10). The
// named box acknowledges (D6) before ToInstalling hands it op.exec.
func NameTarget(opID string, t Target) func(*Claim) error {
	return func(c *Claim) error {
		if err := requireRelocation(c, opID, PhasePinning); err != nil {
			return err
		}
		if c.Op.Intent["target_box"] != "" {
			return fmt.Errorf("%w: the operation already has a target", ErrRelocation)
		}
		return replaceTargetSlot(c, t)
	}
}

// ToInstalling hands op.exec to the target for a new installation: a new
// stamp (this CAS's gen, R6-4), journaled as install_stamp, a fresh
// prepared generation id, and the target added to touched.boxes before its
// first effect. A converted operation with no target names it here.
func ToInstalling(opID string, t Target, prepared string) func(*Claim) error {
	return func(c *Claim) error {
		if err := requireRelocation(c, opID, PhasePinning); err != nil {
			return err
		}
		if !readJournal(c.Op, "pin", new(RecoveryPin)) || prepared == "" || prepared == c.Holder.Generation {
			return fmt.Errorf("%w: installing needs a pin and a fresh prepared generation", ErrRelocation)
		}
		if t.Box != c.Op.Intent["target_box"] || t.Enrollment != c.Op.Intent["target_enrollment"] || slices.Contains(c.Lost, t.Box) {
			return fmt.Errorf("%w: not the operation's target", ErrRelocation)
		}
		if OwesLocal(c, t.Box) {
			return fmt.Errorf("%w: park-local on %s", ErrPendingChore, t.Box)
		}
		if err := requireAcks(c); err != nil {
			return err
		}
		return install(c, t.Box, prepared, PhaseInstalling)
	}
}

// abandonPrepared journals the operation's current P as abandoned when
// no writer opened it, before a transition replaces or drops it: nothing
// will open it now, and the serving CAS parks it (rev 17, finding F3;
// rev 18: every transition that discards an unopened P calls it).
func abandonPrepared(c *Claim) error {
	old := c.Op.Journal["prepared"]
	if old == "" || preparedOpened(c) {
		return nil
	}
	var abandoned []string
	readJournal(c.Op, "abandoned_prepared", &abandoned)
	if slices.Contains(abandoned, old) {
		return nil
	}
	return journalJSON(c, "abandoned_prepared", append(abandoned, old))
}

func install(c *Claim, box, prepared, phase string) error {
	if c.Op.Journal["prepared"] != prepared {
		if err := abandonPrepared(c); err != nil {
			return err
		}
	}
	stamp := c.Gen + 1 // the resulting gen: Update sets gen = observed+1
	c.Op.Exec, c.Op.Phase = box, phase
	c.Holder.Stamp = stamp
	c.Op.Journal["install_stamp"] = strconv.FormatUint(stamp, 10)
	c.Op.Journal["prepared"] = prepared
	delete(c.Op.Journal, "local_install")
	if !slices.Contains(c.Touched.Boxes, box) {
		c.Touched.Boxes = append(c.Touched.Boxes, box)
	}
	return noteInstalledBox(c, box)
}

// ToInstalled records the verified remote build of P (§5.8, the
// no-reinstall boundary): the install manifest at the pin's N (none for an
// empty pin) and, always, P's files manifest at the pinned sequence, each
// verified by a fresh read. Nobody builds P again after this CAS.
func ToInstalled(opID string, a PreparedAuthority) func(*Claim) error {
	return func(c *Claim) error {
		if err := requireRelocation(c, opID, PhaseInstalling); err != nil {
			return err
		}
		var pin RecoveryPin
		readJournal(c.Op, "pin", &pin)
		if a.Generation == "" || a.Generation != c.Op.Journal["prepared"] || a.SnapshotTXID != pin.MaxTXID ||
			(pin.MaxTXID > 0 && (a.InstallManifest == "" || !isHex64(a.SHA256))) ||
			(pin.MaxTXID == 0 && (a.InstallManifest != "" || a.SHA256 != "")) {
			return fmt.Errorf("%w: prepared authority is not this pin's build of P", ErrRelocation)
		}
		if a.FilesSeq != 0 || a.SourceFilesSeq != pin.FilesSeq || !isHex64(a.FilesManifestSHA256) {
			return fmt.Errorf("%w: prepared authority lacks P's prepared files manifest (sequence 0, built from the pinned sequence)", ErrRelocation)
		}
		if err := requireAcks(c); err != nil {
			return err
		}
		c.Op.Phase = PhaseInstalled
		a.InstallStamp = journalUint(c.Op, "install_stamp")
		return journalJSON(c, "prepared_authority", a)
	}
}

// PreparedOpened reports whether P has been opened: journaled as
// prepared_opened by the admission that opened it (rev 12: AdmitWriter
// trims holder.admissions to eight, so the admission list alone could
// forget it), or named by a retained admission.
func PreparedOpened(c *Claim) bool { return preparedOpened(c) }

func preparedOpened(c *Claim) bool {
	p := c.Op.Journal["prepared"]
	if p == "" || c.Holder == nil {
		return false
	}
	if c.Op.Journal["prepared_opened"] == p {
		return true
	}
	for _, a := range c.Holder.Admissions {
		if a.Generation == p {
			return true
		}
	}
	return false
}

// RecordLocalInstall journals the executor's local install receipt in
// installed (B1-2). It is bound to op.exec, the target's enrollment and the
// journaled install_stamp, and refused once any admission has named P
// (B2-5): after that the local install is never remade.
func RecordLocalInstall(opID string, l LocalInstall) func(*Claim) error {
	return func(c *Claim) error {
		if err := requireRelocation(c, opID, PhaseInstalled); err != nil {
			return err
		}
		if l.Box != c.Op.Exec || l.Enrollment != c.Op.Intent["target_enrollment"] ||
			l.InstallStamp == 0 || l.InstallStamp != journalUint(c.Op, "install_stamp") || !isHex64(l.JournalSHA256) {
			return fmt.Errorf("%w: receipt is not this installation's", ErrRelocation)
		}
		if preparedOpened(c) {
			return fmt.Errorf("%w: P was admitted; the local install is never remade", ErrRelocation)
		}
		var old LocalInstall
		if readJournal(c.Op, "local_install", &old) {
			if old == l {
				return ErrAlreadyRecorded
			}
			return fmt.Errorf("%w: a different receipt is journaled", ErrRelocation)
		}
		return journalJSON(c, "local_install", l)
	}
}

// ToProbing enters probing, which requires a local install receipt for
// exactly op.exec, its enrollment and the journaled install_stamp. now
// starts the probe deadline (§5.8: 10 minutes).
func ToProbing(opID string, now time.Time) func(*Claim) error {
	return func(c *Claim) error {
		if err := requireRelocation(c, opID, PhaseInstalled); err != nil {
			return err
		}
		var l LocalInstall
		if !readJournal(c.Op, "local_install", &l) || l.Box != c.Op.Exec || l.Enrollment != c.Op.Intent["target_enrollment"] ||
			l.InstallStamp != journalUint(c.Op, "install_stamp") {
			return fmt.Errorf("%w: no local install receipt for the executor", ErrRelocation)
		}
		if err := requireAcks(c); err != nil {
			return err
		}
		if now.IsZero() {
			return fmt.Errorf("%w: probing needs its start time", ErrRelocation)
		}
		c.Op.Phase = PhaseProbing
		c.Op.Journal["probing_since"] = now.UTC().Format(time.RFC3339Nano)
		return nil
	}
}

// BeginProbeAttempt counts one probe attempt for the executor before it
// is made (§5.8 "limits"): the fourth is refused with
// ErrProbeAttemptsExhausted, and the participant then enters
// probe-failed. The count is per box and per operation, so a replacement
// target starts at zero and a fenced one is never counted again.
func BeginProbeAttempt(opID, box string) func(*Claim) error {
	return func(c *Claim) error {
		if err := requireRelocation(c, opID, PhaseProbing); err != nil {
			return err
		}
		if box == "" || box != c.Op.Exec {
			return fmt.Errorf("%w: only the executor probes", ErrRelocation)
		}
		key := "probe_attempts." + box
		n := journalUint(c.Op, key)
		if n >= MaxProbeAttempts {
			return ErrProbeAttemptsExhausted
		}
		c.Op.Journal[key] = strconv.FormatUint(n+1, 10)
		return nil
	}
}

// RecordProbe journals the executor's passing probe of its admitted session.
func RecordProbe(opID string, p Probe) func(*Claim) error {
	return func(c *Claim) error {
		if err := requireRelocation(c, opID, PhaseProbing); err != nil {
			return err
		}
		if p.Box != c.Op.Exec || p.Box != c.Holder.WriterBox || p.Session == 0 || p.Session != c.Holder.Session ||
			p.Session < journalUint(c.Op, "install_stamp") {
			return fmt.Errorf("%w: probe is not of the executor's admitted session", ErrRelocation)
		}
		return journalJSON(c, "probe", p)
	}
}

// ToProbeFailed records that the live target's probe failed or missed its
// deadline. The target then runs its release sequence (JournalRelease);
// now starts its release deadline.
func ToProbeFailed(opID string, now time.Time) func(*Claim) error {
	return func(c *Claim) error {
		if err := requireRelocation(c, opID, PhaseProbing); err != nil {
			return err
		}
		if now.IsZero() {
			return fmt.Errorf("%w: probe-failed needs its start time", ErrRelocation)
		}
		c.Op.Phase = PhaseProbeFailed
		c.Op.Journal["probe_failed_since"] = now.UTC().Format(time.RFC3339Nano)
		delete(c.Op.Journal, "release")
		delete(c.Op.Journal, "release.phase")
		return nil
	}
}

// CompleteRelocation is the serving CAS: the target's probe passed for its
// admitted session, so the host serves on it alone. Every other box this
// operation installed on, and a live source, owes a park-local unless a
// fence discharged it.
func CompleteRelocation(opID string, newID func() string) func(*Claim) error {
	return func(c *Claim) error {
		if err := requireRelocation(c, opID, PhaseProbing); err != nil {
			return err
		}
		var p Probe
		if !readJournal(c.Op, "probe", &p) || p.Box != c.Op.Exec || p.Session != c.Holder.Session || c.Holder.WriterBox != p.Box {
			return fmt.Errorf("%w: no passing probe of the current session", ErrRelocation)
		}
		target := c.Op.Exec
		var owed []string
		readJournal(c.Op, "installed_boxes", &owed)
		owed = append([]string{c.Op.Intent["source_box"]}, owed...)
		for _, box := range owed {
			if box == target || box == "" {
				continue
			}
			var d LocalDischarge
			if readJournal(c.Op, "discharge."+box, &d) && d.Qualified {
				continue
			}
			exists := false
			for _, o := range c.Obligations {
				if o.Kind == "park-local" && o.Box == box {
					exists = true
				}
			}
			if !exists {
				c.Obligations = append(c.Obligations, Obligation{ID: newID(), Op: opID, Kind: "park-local", Box: box, Retirement: newID(), Owner: "box:" + box})
			}
		}
		// Every prepared generation this operation built and no writer
		// opened is parked here, in the region, by the claim's own
		// park-generation chore (rev 17, finding F3); the at-rest sweep
		// stays the backstop the spec names.
		var abandoned []string
		readJournal(c.Op, "abandoned_prepared", &abandoned)
		region := c.Op.Intent["region"]
		for _, g := range abandoned {
			if g == "" || g == c.Holder.Generation || region == "" {
				continue
			}
			queued := false
			for _, o := range c.Obligations {
				if o.Kind == "park-generation" && o.Region == region && o.Generation == g {
					queued = true
				}
			}
			if !queued {
				c.Obligations = append(c.Obligations, Obligation{ID: newID(), Op: opID, Kind: "park-generation", Region: region, Generation: g, Retirement: newID(), Owner: "region:" + region})
			}
		}
		c.Op = Op{Kind: KindServing, Exec: target, Participants: []string{target}}
		return nil
	}
}

// replaceTargetSlot names t as the target, counting a replacement when it
// replaces another box. A replaced box is never named again for this host.
func replaceTargetSlot(c *Claim, t Target) error {
	if !validBoxReference(t.Box) || t.Box == "none" || t.Enrollment == "" || t.Box == c.Op.Intent["source_box"] || slices.Contains(c.Lost, t.Box) {
		return fmt.Errorf("%w: invalid target", ErrRelocation)
	}
	var excluded []string
	readJournal(c.Op, "excluded_targets", &excluded)
	if slices.Contains(excluded, t.Box) {
		return fmt.Errorf("%w: %s was replaced in this operation", ErrRelocation, t.Box)
	}
	if OwesLocal(c, t.Box) {
		// Spec 1 §2: a box owing a local retirement for this host is never
		// handed an installation, in any phase a replacement resumes at
		// (install is called below without ToInstalling's check).
		return fmt.Errorf("%w: park-local on %s", ErrPendingChore, t.Box)
	}
	old := c.Op.Intent["target_box"]
	if old != "" && old != t.Box {
		n := journalUint(c.Op, "replacements")
		if n >= MaxTargetReplacements {
			return ErrReplacementsExceeded
		}
		c.Op.Journal["replacements"] = strconv.FormatUint(n+1, 10)
		excluded = append(excluded, old)
		if err := journalJSON(c, "excluded_targets", excluded); err != nil {
			return err
		}
		removeParticipant(c, old)
	}
	c.Op.Intent["target_box"], c.Op.Intent["target_enrollment"] = t.Box, t.Enrollment
	addParticipant(c, t.Box)
	return nil
}

// ReplaceTarget is §5.8's replacement table for a target terminated by its
// fence. It records the fence (the old target goes on lost), names next,
// and resumes at the phase the table gives:
//
//	starting, releasing, pinning      -> the same phase
//	installing                        -> installing: next is op.exec, new stamp, fresh P'
//	installed, or probing before P    -> installed: next is op.exec, new stamp, same P, no receipt
//	probing after P, or probe-failed  -> pinning: a nested failover from holder.generation
//
// prepared is P' for installing and ignored otherwise. A third
// replacement is refused with ErrReplacementsExceeded; the worker then
// marks the operation stuck.
func ReplaceTarget(ctx context.Context, s release.Store, observed Observed, opID string, ref FenceRef, d *LocalDischarge, next Target, prepared string, authority FenceAuthority) (Observed, error) {
	if observed.Absent || observed.Claim == nil {
		return Observed{}, ErrWrongState
	}
	old := observed.Claim.Op.Intent["target_box"]
	v, err := VerifyFence(ctx, s, authority, ref)
	if err != nil {
		return Observed{}, err
	}
	if old == "" || v.record.Box != old || v.record.Enrollment != observed.Claim.Op.Intent["target_enrollment"] || v.binding.Region != observed.Claim.Op.Intent["region"] {
		return Observed{}, ErrFence
	}
	return Update(ctx, s, observed, func(c *Claim) error {
		if err := requireRelocation(c, opID, PhaseStarting, PhaseReleasing, PhasePinning, PhaseInstalling, PhaseInstalled, PhaseProbing, PhaseProbeFailed); err != nil {
			return err
		}
		if c.Op.Intent["target_box"] != old {
			return ErrStaleOp
		}
		phase := c.Op.Phase
		if err := fenceBox(c, old, ref, v.record.ObservedAt, d); err != nil {
			return err
		}
		if err := replaceTargetSlot(c, next); err != nil {
			return err
		}
		switch {
		case phase == PhaseStarting || phase == PhaseReleasing || phase == PhasePinning:
			return nil
		case phase == PhaseInstalling:
			if prepared == "" || prepared == c.Op.Journal["prepared"] || prepared == c.Holder.Generation {
				return fmt.Errorf("%w: a replacement in installing builds a fresh P'", ErrRelocation)
			}
			return install(c, next.Box, prepared, PhaseInstalling)
		case (phase == PhaseInstalled || phase == PhaseProbing) && !preparedOpened(c):
			return install(c, next.Box, c.Op.Journal["prepared"], PhaseInstalled)
		default:
			// After P's first admission, or from probe-failed: nested
			// failover from pinning, pinning from holder.generation as
			// observed. A P no writer opened (a probe deadline before any
			// admission) is recorded before it is dropped.
			if err := abandonPrepared(c); err != nil {
				return err
			}
			c.Op.Exec, c.Op.Phase = "none", PhasePinning
			for _, k := range []string{"pin", "prepared", "prepared_authority", "local_install", "probe", "release", "release.phase"} {
				delete(c.Op.Journal, k)
			}
			return nil
		}
	})
}

// FenceExhaustedTarget is the terminal transition for a target terminated
// after the operation has used its replacements (§5.8 "The bound"; round 3
// finding 5): it consumes the fence (the loss is retained, the box goes on
// lost) and records stuck. While another box is op.exec (the live source
// in starting or releasing; round 8 finding 1) nothing else changes: the
// target's fence revokes nothing of the source's. Otherwise (op.exec is
// the dead target, or none) it revokes the dead installation's authority (op.exec "none", the
// target off the barrier, its receipt dropped), leaves the operation at
// pinning with its pin and, when P was never opened, its remote build kept
// for the operator's replacement, or a nested pinning when P was opened,
// and records stuck in the same CAS. No third target is chosen. MarkStuck's
// "never between installed and a probe" is for a live target; a dead one
// has no probe to make.
func FenceExhaustedTarget(ctx context.Context, s release.Store, observed Observed, opID string, ref FenceRef, d *LocalDischarge, authority FenceAuthority) (Observed, error) {
	return fenceTargetStuck(ctx, s, observed, opID, ref, d, authority, "")
}

// FenceTargetWithoutSpare is FenceExhaustedTarget's transition for a
// terminated target with replacements left but no eligible box to name
// (rev 18, round 17 finding 2): the worker calls it once its bound has
// passed. The fence is consumed in the same CAS (loss retained, the box
// on lost, a dead executor's authority revoked), and the operation is
// stuck for an operator with reason, never left waiting unbounded.
func FenceTargetWithoutSpare(ctx context.Context, s release.Store, observed Observed, opID string, ref FenceRef, d *LocalDischarge, authority FenceAuthority, reason string) (Observed, error) {
	if reason == "" {
		return Observed{}, fmt.Errorf("%w: a stuck operation names its reason", ErrRelocation)
	}
	return fenceTargetStuck(ctx, s, observed, opID, ref, d, authority, reason)
}

// fenceTargetStuck is both: noSpare "" is the exhausted bound.
func fenceTargetStuck(ctx context.Context, s release.Store, observed Observed, opID string, ref FenceRef, d *LocalDischarge, authority FenceAuthority, noSpare string) (Observed, error) {
	if observed.Absent || observed.Claim == nil {
		return Observed{}, ErrWrongState
	}
	old := observed.Claim.Op.Intent["target_box"]
	v, err := VerifyFence(ctx, s, authority, ref)
	if err != nil {
		return Observed{}, err
	}
	if old == "" || v.record.Box != old || v.record.Enrollment != observed.Claim.Op.Intent["target_enrollment"] || v.binding.Region != observed.Claim.Op.Intent["region"] {
		return Observed{}, ErrFence
	}
	return Update(ctx, s, observed, func(c *Claim) error {
		if err := RequireOp(opID)(c); err != nil {
			return err
		}
		if c.Op.Kind != KindRelocating || c.Op.Intent["target_box"] != old {
			return ErrStaleOp
		}
		ensureJournal(c)
		if c.Op.Journal["stuck"] != "" {
			return ErrAlreadyRecorded
		}
		reason := noSpare
		if reason == "" {
			if journalUint(c.Op, "replacements") < MaxTargetReplacements {
				return fmt.Errorf("%w: replacements remain; replace the target instead", ErrRelocation)
			}
			reason = fmt.Sprintf("%s terminated after %d target replacements", old, MaxTargetReplacements)
		}
		if err := fenceBox(c, old, ref, v.record.ObservedAt, d); err != nil {
			return err
		}
		removeParticipant(c, old)
		if c.Op.Exec != old && c.Op.Exec != "none" {
			// The executor is another box (the live source in starting or
			// releasing): the target's fence is no evidence against it.
			// Its execution identity, phase and release records stay, so
			// root still accepts its own stop (claimstop.go requires the
			// requester to be op.exec); only stuck is new.
			c.Op.Journal["stuck"] = reason
			return nil
		}
		opened := preparedOpened(c)
		c.Op.Exec, c.Op.Phase = "none", PhasePinning
		keys := []string{"local_install", "probe", "release", "release.phase", "probing_since", "probe_failed_since"}
		if opened {
			// Nested: pinning again from holder.generation, as a replacement
			// after P's first admission would.
			keys = append(keys, "pin", "prepared", "prepared_authority")
		}
		// An unopened P is kept for the operator's replacement; it is on
		// the abandoned list only if a later transition drops it.
		for _, k := range keys {
			delete(c.Op.Journal, k)
		}
		if c.Op.Journal["stuck"] == "" {
			c.Op.Journal["stuck"] = reason
		}
		return nil
	})
}

// MarkStuck stops the operation at its current phase for an operator
// (`carlos ops host resolve`). It never resets the replacement count and
// never invents evidence; every later relocation transition refuses.
func MarkStuck(opID, reason string) func(*Claim) error {
	return func(c *Claim) error {
		if err := RequireOp(opID)(c); err != nil {
			return err
		}
		if c.Op.Kind != KindRelocating || reason == "" {
			return ErrWrongState
		}
		ensureJournal(c)
		if c.Op.Phase == PhaseInstalled && c.Op.Journal["local_install"] != "" && !preparedOpened(c) {
			return fmt.Errorf("%w: never stop between installed and a probe", ErrRelocation)
		}
		if c.Op.Journal["stuck"] != "" {
			return ErrAlreadyRecorded
		}
		c.Op.Journal["stuck"] = reason
		return nil
	}
}

• [ ] Step 4: Teach AdmitWriter the phase table and released, and the claim its retained losses

Apply to internal/hostclaim/claim.go (git apply): EvidenceRefs, D4's retained automatic losses, validated beside loss_refs:

diff --git a/internal/hostclaim/claim.go b/internal/hostclaim/claim.go
index 23d17858..50e55006 100644
--- a/internal/hostclaim/claim.go
+++ b/internal/hostclaim/claim.go
@@ -162,6 +162,7 @@ type Claim struct {
 	Lost                []string                  `json:"lost,omitempty"`
 	LostRevisions       map[string]uint64         `json:"lost_revisions,omitempty"`
 	LossRefs            []string                  `json:"loss_refs,omitempty"`
+	EvidenceRefs        []AutomaticLoss           `json:"evidence_refs,omitempty"`
 	RetiredIncarnations []string                  `json:"retired_incarnations,omitempty"`
 	QuietAfter          map[string]time.Time      `json:"quiet_after,omitempty"`
 	CancelledCreates    []CancelledCreate         `json:"cancelled_creates,omitempty"`
@@ -289,6 +290,16 @@ func (c *Claim) Validate() error {
 		}
 		seenLossRefs[id] = true
 	}
+	seenEvidence := map[string]bool{}
+	for _, l := range c.EvidenceRefs {
+		// D4: a retained automatic loss names a loss identity the claim
+		// also lists, a box, and a well-formed fence reference.
+		if !seenLossRefs[l.ID] || seenEvidence[l.ID] || l.Box == "" || !validFenceRef(l.Fence) || l.Enrollment != l.Fence.Enrollment || l.Op == "" ||
+			(l.Role != "source" && l.Role != "target") || (l.Timers != TimersComplete && l.Timers != TimersPartial && l.Timers != TimersUnknown) {
+			return fmt.Errorf("%w: invalid automatic loss evidence", ErrMalformed)
+		}
+		seenEvidence[l.ID] = true
+	}
 	if len(c.RetiredIncarnations) > retiredCap {
 		return fmt.Errorf("%w: retired_incarnations over cap", ErrMalformed)
 	}

Apply to internal/hostclaim/generation.go (git apply):

diff --git a/internal/hostclaim/generation.go b/internal/hostclaim/generation.go
index ffd7e058..74947b56 100644
--- a/internal/hostclaim/generation.go
+++ b/internal/hostclaim/generation.go
@@ -43,6 +43,10 @@ func AdmitWriter(in Admission) func(*Claim) error {
 		switch c.Op.Kind {
 		case KindCreating, KindDeleting, KindParking, KindPurging, KindPlacing:
 			return fmt.Errorf("%w: op kind %q cannot admit a writer", ErrWrongState, c.Op.Kind)
+		case KindRelocating:
+			if err := relocationAdmission(c, in); err != nil {
+				return err
+			}
 		}
 		h := c.Holder
 		if in.LossID != "" && !in.lossVerified {
@@ -87,6 +91,10 @@ func AdmitWriter(in Admission) func(*Claim) error {
 
 		switch in.Coverage {
 		case "", "sealed", "clean-return":
+		case "released": // checked by relocationAdmission (L9)
+			if c.Op.Kind != KindRelocating {
+				return ErrWrongState
+			}
 		default:
 			return ErrWrongState
 		}
@@ -261,3 +269,60 @@ func CoverParkedPredecessors(observedOpID, observedPhase string, region string,
 		return nil
 	}
 }
+
+// relocationAdmission is §4's phase table for relocating (L1) and §6.4a's
+// `released` coverage (L9). The source may admit in starting and releasing
+// (its local admission fence closes releasing); only op.exec admits in
+// probing, cold; nobody admits in any other phase. The first probe
+// admission opens the prepared generation P, which is opened at most once.
+// `released` is legal only on that opening, when the predecessor is exactly
+// the session whose release this operation journaled and its pin reaches
+// that release's final position.
+func relocationAdmission(c *Claim, in Admission) error {
+	if c.Op.Journal["stuck"] != "" {
+		// Ruling 9: a stuck operation runs nothing, the source's wake
+		// included; the operator resolves it (carlos ops host resolve).
+		return fmt.Errorf("%w: relocation is stuck", ErrWrongState)
+	}
+	switch c.Op.Phase {
+	case PhaseStarting, PhaseReleasing:
+		if in.Box != c.Op.Intent["source_box"] || in.Coverage == "released" {
+			return fmt.Errorf("%w: only the source admits before pinning", ErrWrongState)
+		}
+		return nil
+	case PhaseProbing:
+	default:
+		return fmt.Errorf("%w: relocating/%s admits no writer", ErrWrongState, c.Op.Phase)
+	}
+	if in.Mode != "cold" || in.Box != c.Op.Exec {
+		return fmt.Errorf("%w: a probe admission is the executor's, cold", ErrWrongState)
+	}
+	p, opened := c.Op.Journal["prepared"], preparedOpened(c)
+	if p == "" || (!opened && in.NewGeneration != p) || (opened && in.NewGeneration == p) {
+		return fmt.Errorf("%w: the first probe opens P, and only it", ErrWrongState)
+	}
+	if !opened {
+		// The opening is journaled with the admission, so it outlives the
+		// admission list's trim (rev 12): P is never opened twice.
+		ensureJournal(c)
+		c.Op.Journal["prepared_opened"] = p
+	}
+	if in.Coverage != "released" {
+		return nil
+	}
+	var r Release
+	var pin RecoveryPin
+	if opened || in.PredecessorCertified || !readJournal(c.Op, "release", &r) || !readJournal(c.Op, "pin", &pin) ||
+		pin.MaxTXID < r.FinalTXID || pin.FilesSeq < r.ManifestSeq {
+		return fmt.Errorf("%w: released coverage needs this operation's release and a pin reaching it", ErrWrongState)
+	}
+	h := c.Holder
+	predecessor := AdmissionRecord{Session: h.Session, Box: h.WriterBox, Generation: h.Generation}
+	if len(h.Admissions) > 0 {
+		predecessor = h.Admissions[len(h.Admissions)-1]
+	}
+	if predecessor.Box != r.ReleasedBy || predecessor.Session != r.Session || predecessor.Generation != r.Generation {
+		return fmt.Errorf("%w: released coverage names another predecessor", ErrWrongState)
+	}
+	return nil
+}

• [ ] Step 5: Run the tests

Run: nice -n 19 go test ./internal/hostclaim/ -count=1 Expected: PASS, every existing test included (TestC7… covers the conversion from moving, unchanged).

• [ ] Step 6: Commit

gofmt -l internal/hostclaim
git add internal/hostclaim/relocation.go internal/hostclaim/relocation_test.go internal/hostclaim/generation.go internal/hostclaim/claim.go
git commit -m "hostclaim: relocating within one region, released by stop evidence or a termination fence, with released coverage on P's one opening and the fenced box's loss retained

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>"

---

Task 2: Create names its executor once (H12, L8, P5-D2, P5-D6)

Spec §5.2. The executor is boxchoice.Choose(boxchoice.Eligible(...)) over the roster's active, unfenced boxes in the record's placement, chosen before the create CAS and recorded in its intent as selected_executor and executor_enrollment. CompleteCreate refuses any other box, so recovery never substitutes. Identity, placement and AWS region come from the roster (Roster.Regions[placement].AWSRegion); the edges snapshot gives liveness and configuration only; claim loads only balance. A fence that cannot be read refuses the choice. Permits is the same read without the choice: whether one named box is in the eligible set (Task 5's start check). Dormant: SelectExecutor reports whether it selected at all; with no chooser (ProductionAuthority.Executors nil, which the console leaves nil unless Config.RegionHA is on) the create is byte-for-byte today's, BeginCreate and Executor at completion, claim-enabled one-box regions included.

Files:

• Modify: internal/hostclaim/create.go, internal/hostclaim/create_test.go
• Create: internal/hostops/executor.go, internal/hostops/loads.go, internal/hostops/executor_test.go
• Modify: internal/hostops/operations.go (Authority.SelectExecutor, Attempt), internal/hostops/backfill_controller.go, internal/hostops/backfill.go (ProductionAuthority.Executors, SelectExecutor), internal/hostops/operations_test.go (the fake authority)
• Create: internal/console/hostclaimexecutor.go, internal/console/hostclaimexecutor_test.go (the console's chooser; the create door uses it once claim Plan 5's door lands, Task 10)
• Modify: internal/console/server.go (Config.RegionHA), cmd/console/main.go (sets it from CARLOS_REGION_HA with strconv.ParseBool)
• Test: cmd/console/regionha_test.go (rev 11: the switch itself)

Interfaces:

• Consumes: boxchoice.Eligible, boxchoice.Choose, boxchoice.Snapshot, boxchoice.Load, hostactors.Directory.Read, Directory.TerminationFence, hostactors.Roster.Regions; Task 1's hostclaim.LocalChoreBoxes (the eligible set excludes a box owing a park-local, rev 6).
• Produces: hostclaim.ExecutorSelection{Box, Enrollment}, hostclaim.BeginCreateOn(nh, body, opID, by, now, sel); hostops.ErrNoEligibleBox; hostops.ExecutorChooser{Directory, Edges func(ctx) (boxchoice.Snapshot, error), Loads func(ctx) (map[string]boxchoice.Load, error), SecretsKeyFP, HomeName, Now} with Choose(ctx, hostclaim.Observed, Record) (hostclaim.ExecutorSelection, error) and Permits(ctx, hostclaim.Observed, Record, box string) error; hostops.ClaimLoads(ctx, release.Store) (map[string]boxchoice.Load, error); Authority.SelectExecutor(ctx, hostclaim.Observed, Record) (sel hostclaim.ExecutorSelection, selected bool, err error); ProductionAuthority.Executors *ExecutorChooser; console.Config.RegionHA; (*console.Server).executorChooser(hostactors.Directory) *hostops.ExecutorChooser (nil with HA off).

• [ ] Step 1: Write the failing tests

Append to internal/hostclaim/create_test.go:

diff --git a/internal/hostclaim/create_test.go b/internal/hostclaim/create_test.go
index 53968923..c9a100e6 100644
--- a/internal/hostclaim/create_test.go
+++ b/internal/hostclaim/create_test.go
@@ -276,3 +276,27 @@ func TestCompleteCreateRefusesExecutionAuthority(t *testing.T) {
 		})
 	}
 }
+
+func TestCreateCompletesOnlyOnTheSelectedExecutor(t *testing.T) {
+	ctx := context.Background()
+	s := release.NewDirStore(t.TempDir())
+	now := time.Date(2026, 10, 4, 1, 0, 1, 0, time.UTC)
+	reg, _ := Read(ctx, s, testHost)
+	sel := ExecutorSelection{Box: "bri-knitting", Enrollment: "enrollment-b"}
+	if _, err := Update(ctx, s, reg, BeginCreateOn(newHolder(), record, "op_c1", "console", now, ExecutorSelection{})); !errors.Is(err, ErrMalformed) {
+		t.Fatalf("create with no selection: %v", err)
+	}
+	o, err := Update(ctx, s, reg, BeginCreateOn(newHolder(), record, "op_c1", "console", now, sel))
+	if err != nil {
+		t.Fatal(err)
+	}
+	if o.Claim.Op.Intent["selected_executor"] != sel.Box || o.Claim.Op.Intent["executor_enrollment"] != sel.Enrollment || o.Claim.Op.Exec != "" {
+		t.Fatalf("intent: %+v", o.Claim.Op)
+	}
+	if _, err := Update(ctx, s, o, CompleteCreate("op_c1", "adi-knitting")); !errors.Is(err, ErrWrongState) {
+		t.Fatalf("completion substituted a box: %v", err)
+	}
+	if o, err = Update(ctx, s, o, CompleteCreate("op_c1", sel.Box)); err != nil || o.Claim.Op.Exec != sel.Box {
+		t.Fatalf("complete: %v %+v", err, o.Claim.Op)
+	}
+}

internal/hostops/executor_test.go:

package hostops

import (
	"context"
	"crypto/ed25519"
	"crypto/rand"
	"crypto/sha256"
	"encoding/hex"
	"encoding/json"
	"errors"
	"strings"
	"testing"
	"time"

	"github.com/carlosframework/platform/internal/boxchoice"
	"github.com/carlosframework/platform/internal/hostactors"
	"github.com/carlosframework/platform/internal/hostclaim"
	"github.com/carlosframework/platform/internal/release"
	"github.com/carlosframework/platform/internal/termfence"
)

func chooserFixture(t *testing.T, boxes ...string) (ExecutorChooser, release.Store, *boxchoice.Snapshot, map[string]boxchoice.Load) {
	t.Helper()
	s := release.NewDirStore(t.TempDir())
	pub, key, err := ed25519.GenerateKey(rand.Reader)
	if err != nil {
		t.Fatal(err)
	}
	roster := hostactors.Roster{V: 1, DeploymentBucket: "bucket", Revision: 1,
		Regions: map[string]hostactors.Region{"ie": {Account: "123", AWSRegion: "eu-west-1"}},
		Boxes:   map[string]hostactors.Box{}, Consoles: map[string]hostactors.Console{}, Holds: map[string]hostactors.Reservation{}, Activations: map[string]hostactors.Reservation{}}
	snap := &boxchoice.Snapshot{Complete: true}
	yes := true
	for i, ref := range boxes {
		roster.Boxes[ref] = hostactors.Box{Enrollment: strings.Repeat(string("abcdef"[i]), 32), Namespace: "platform", BoxID: ref, Label: ref, Region: "ie", Pool: "default",
			Cloud: hostactors.Cloud{Provider: "aws", Account: "123", Region: "eu-west-1", InstanceID: "i-" + ref}, EvidenceSHA256: strings.Repeat("c", 64), State: "active"}
		snap.Boxes = append(snap.Boxes, boxchoice.Box{BoxID: ref, EIP: "203.0.113.1", Region: "eu-west-1", Placement: "ie", Fresh: true,
			HibernationConfigured: &yes, ServesSharedPool: &yes, AcceptsInbound: &yes, SecretsKeyFP: "fp", Capabilities: []string{boxchoice.Capability}})
	}
	wire, err := release.SignRootEnvelope(release.RootSigner(key), roster)
	if err != nil {
		t.Fatal(err)
	}
	if _, err := s.Put(context.Background(), hostactors.Key, wire, ""); err != nil {
		t.Fatal(err)
	}
	loads := map[string]boxchoice.Load{}
	x := ExecutorChooser{Directory: hostactors.Directory{Store: s, PublicKey: pub, Bucket: "bucket"}, SecretsKeyFP: "fp",
		Edges: func(context.Context) (boxchoice.Snapshot, error) { return *snap, nil },
		Loads: func(context.Context) (map[string]boxchoice.Load, error) { return loads, nil },
		Now:   func() time.Time { return time.Date(2026, 10, 7, 9, 0, 0, 0, time.UTC) }}
	return x, s, snap, loads
}

func chooserRecord() Record {
	return Record{Holder: hostclaim.NewHolder{Family: "instance", Account: "bab", App: "jam", Host: "shop.bab.oncarlos.com", Region: "ie"}}
}

func TestExecutorChooserSpreadsThenBalancesThenHashes(t *testing.T) {
	ctx := context.Background()
	x, _, _, loads := chooserFixture(t, "box-a", "box-b")
	absent := hostclaim.Observed{Host: "shop.bab.oncarlos.com", Absent: true}
	first, err := x.Choose(ctx, absent, chooserRecord())
	if err != nil {
		t.Fatal(err)
	}
	other := map[string]string{"box-a": "box-b", "box-b": "box-a"}[first.Box]
	if first.Enrollment != map[string]string{"box-a": strings.Repeat("a", 32), "box-b": strings.Repeat("b", 32)}[first.Box] {
		t.Fatalf("enrollment not the roster's: %+v", first)
	}
	// The hash winner already runs this app: spread prefers the other box.
	loads[first.Box] = boxchoice.Load{Hosts: 1, Apps: map[string]int{"bab/jam": 1}}
	if got, _ := x.Choose(ctx, absent, chooserRecord()); got.Box != other {
		t.Fatalf("soft spread: got %s, want %s", got.Box, other)
	}
	// Both run the app: the fewest hosts wins.
	loads[other] = boxchoice.Load{Hosts: 5, Apps: map[string]int{"bab/jam": 1}}
	if got, _ := x.Choose(ctx, absent, chooserRecord()); got.Box != first.Box {
		t.Fatalf("headroom: got %s, want %s", got.Box, first.Box)
	}
}

// Round 18 finding 2: with equal loads the winner is the greatest
// SHA-256 of host + "\x00" + box id (claim P5-D2), computed here
// independently of boxchoice. The two hostnames are chosen so that their
// winners differ: a chooser that hashed anything but the record's host
// would get at least one of them wrong.
func TestExecutorChooserHashesTheRecordsHostOnEqualLoads(t *testing.T) {
	ctx := context.Background()
	winner := func(host string) string {
		a := sha256.Sum256([]byte(host + "\x00box-a"))
		b := sha256.Sum256([]byte(host + "\x00box-b"))
		if hex.EncodeToString(a[:]) > hex.EncodeToString(b[:]) {
			return "box-a"
		}
		return "box-b"
	}
	hosts := []string{"shop.bab.oncarlos.com", "cafe.bab.oncarlos.com"}
	if winner(hosts[0]) == winner(hosts[1]) {
		t.Fatal("the fixture's hostnames must choose opposite boxes")
	}
	for _, host := range hosts {
		x, _, _, _ := chooserFixture(t, "box-a", "box-b")
		r := chooserRecord()
		r.Holder.Host = host
		got, err := x.Choose(ctx, hostclaim.Observed{Host: host, Absent: true}, r)
		if err != nil || got.Box != winner(host) {
			t.Fatalf("%s: chose %+v %v, want %s", host, got, err, winner(host))
		}
	}
}

func TestExecutorChooserNeverNamesAFencedLostOrUnknownBox(t *testing.T) {
	ctx := context.Background()
	absent := hostclaim.Observed{Host: "shop.bab.oncarlos.com", Absent: true}
	t.Run("lost", func(t *testing.T) {
		x, _, _, _ := chooserFixture(t, "box-a")
		obs := hostclaim.Observed{Host: "shop.bab.oncarlos.com", Claim: &hostclaim.Claim{Lost: []string{"box-a"}}}
		if _, err := x.Choose(ctx, obs, chooserRecord()); !errors.Is(err, ErrNoEligibleBox) {
			t.Fatalf("chose a lost box: %v", err)
		}
	})
	t.Run("owing a local retirement", func(t *testing.T) {
		// Spec 1 §2: a box whose old installation of the host is not yet
		// retired (park-local) is never chosen; the clean one is.
		x, _, _, _ := chooserFixture(t, "box-a", "box-b")
		obs := hostclaim.Observed{Host: "shop.bab.oncarlos.com", Claim: &hostclaim.Claim{Obligations: []hostclaim.Obligation{{ID: "old", Op: "old-op", Kind: "park-local", Box: "box-a", Retirement: "r", Owner: "box:box-a"}}}}
		for range 4 {
			if got, err := x.Choose(ctx, obs, chooserRecord()); err != nil || got.Box != "box-b" {
				t.Fatalf("got %+v %v, want the box with no chore", got, err)
			}
		}
		if err := x.Permits(ctx, obs, chooserRecord(), "box-a"); !errors.Is(err, ErrNoEligibleBox) {
			t.Fatalf("permitted a box owing park-local: %v", err)
		}
	})
	t.Run("fenced", func(t *testing.T) {
		x, s, _, _ := chooserFixture(t, "box-a", "box-w")
		f := termfence.Record{V: 1, Box: "box-a", Enrollment: strings.Repeat("a", 32), State: "terminated",
			Cloud:      hostactors.Cloud{Provider: "aws", Account: "123", Region: "eu-west-1", InstanceID: "i-box-a"},
			ObservedAt: "2026-10-07T08:00:00Z", Via: termfence.ViaDescribe, RequestID: "req",
			WrittenBy: termfence.WrittenBy{Box: "box-w", Enrollment: strings.Repeat("b", 32)}}
		raw, _ := json.Marshal(f)
		if _, err := s.Put(ctx, "control/box-fences/"+strings.Repeat("a", 32)+".json", raw, ""); err != nil {
			t.Fatal(err)
		}
		got, err := x.Choose(ctx, absent, chooserRecord())
		if err != nil || got.Box != "box-w" {
			t.Fatalf("got %+v %v, want the unfenced box", got, err)
		}
	})
	t.Run("an edges file for a box the roster does not hold", func(t *testing.T) {
		x, _, snap, _ := chooserFixture(t)
		yes := true
		snap.Boxes = append(snap.Boxes, boxchoice.Box{BoxID: "stray", EIP: "203.0.113.9", Region: "eu-west-1", Placement: "ie", Fresh: true,
			HibernationConfigured: &yes, ServesSharedPool: &yes, AcceptsInbound: &yes, SecretsKeyFP: "fp", Capabilities: []string{boxchoice.Capability}})
		if _, err := x.Choose(ctx, absent, chooserRecord()); !errors.Is(err, ErrNoEligibleBox) {
			t.Fatalf("chose an unenrolled box: %v", err)
		}
	})
	t.Run("an incomplete snapshot", func(t *testing.T) {
		x, _, snap, _ := chooserFixture(t, "box-a")
		snap.Complete = false
		if _, err := x.Choose(ctx, absent, chooserRecord()); !errors.Is(err, ErrNoEligibleBox) {
			t.Fatalf("chose from a partial read: %v", err)
		}
	})
	t.Run("an unreadable fence", func(t *testing.T) {
		x, s, _, _ := chooserFixture(t, "box-a")
		if _, err := s.Put(ctx, "control/box-fences/"+strings.Repeat("a", 32)+".json", []byte("{"), ""); err != nil {
			t.Fatal(err)
		}
		if _, err := x.Choose(ctx, absent, chooserRecord()); err == nil || errors.Is(err, ErrNoEligibleBox) {
			t.Fatalf("an unreadable fence must refuse, not skip: %v", err)
		}
	})
}

func TestExecutorChooserPermitsOnlyTheEligibleSet(t *testing.T) {
	ctx := context.Background()
	absent := hostclaim.Observed{Host: "shop.bab.oncarlos.com", Absent: true}
	for _, tc := range []struct {
		name   string
		change func(*boxchoice.Box)
	}{
		{"a stale edges file", func(b *boxchoice.Box) { b.Fresh = false }},
		{"no region-ha-1 capability", func(b *boxchoice.Box) { b.Capabilities = nil }},
		{"another secrets key", func(b *boxchoice.Box) { b.SecretsKeyFP = "other" }},
		{"a draining box", func(b *boxchoice.Box) { b.Draining = true }},
	} {
		t.Run(tc.name, func(t *testing.T) {
			x, _, snap, _ := chooserFixture(t, "box-a", "box-b")
			if err := x.Permits(ctx, absent, chooserRecord(), "box-a"); err != nil {
				t.Fatal(err)
			}
			tc.change(&snap.Boxes[0])
			if err := x.Permits(ctx, absent, chooserRecord(), "box-a"); !errors.Is(err, ErrNoEligibleBox) {
				t.Fatalf("permitted: %v", err)
			}
			if err := x.Permits(ctx, absent, chooserRecord(), "box-b"); err != nil {
				t.Fatalf("the other box: %v", err)
			}
		})
	}
	t.Run("an unknown box", func(t *testing.T) {
		x, _, _, _ := chooserFixture(t, "box-a")
		if err := x.Permits(ctx, absent, chooserRecord(), "box-z"); !errors.Is(err, ErrNoEligibleBox) {
			t.Fatalf("permitted: %v", err)
		}
	})
}

func TestClaimLoadsCountsExecutorsPerBoxAndApp(t *testing.T) {
	ctx := context.Background()
	s := release.NewDirStore(t.TempDir())
	created := time.Date(2026, 10, 4, 1, 0, 0, 0, time.UTC)
	for i, tc := range []struct{ host, app, box string }{
		{"a.bab.oncarlos.com", "jam", "box-a"}, {"b.bab.oncarlos.com", "jam", "box-a"}, {"c.bab.oncarlos.com", "tea", "box-b"},
	} {
		nh := hostclaim.NewHolder{Family: "instance", Key: "apps/bab/" + tc.app + "/instances/" + tc.host + ".json", Account: "bab", App: tc.app, Host: tc.host, Region: "ie", RecordRegion: "ie", CreatedAt: created}
		body := []byte(`{"host":"` + tc.host + `","account":"bab","app":"` + tc.app + `","region":"ie","created_at":"2026-10-04T01:00:00Z"}`)
		o, _ := hostclaim.Read(ctx, s, tc.host)
		o, err := hostclaim.Update(ctx, s, o, hostclaim.BeginCreateOn(nh, body, "c", "console", created, hostclaim.ExecutorSelection{Box: tc.box, Enrollment: "e"}))
		if err != nil {
			t.Fatal(err)
		}
		if i < 2 { // the third is still creating: it has no executor yet
			if _, err := hostclaim.Update(ctx, s, o, hostclaim.CompleteCreate("c", tc.box)); err != nil {
				t.Fatal(err)
			}
		}
	}
	if _, err := s.Put(ctx, "control/hosts/broken.bab.oncarlos.com.json", []byte("{"), ""); err != nil {
		t.Fatal(err)
	}
	loads, err := ClaimLoads(ctx, s)
	if err != nil {
		t.Fatal(err)
	}
	if loads["box-a"].Hosts != 2 || loads["box-a"].Apps["bab/jam"] != 2 || loads["box-b"].Hosts != 0 {
		t.Fatalf("loads: %+v", loads)
	}
}

func TestProductionAuthoritySelectsOnlyWithAChooser(t *testing.T) {
	// No chooser (CARLOS_REGION_HA off): no selection and no error, so the
	// create is today's.
	sel, selected, err := (ProductionAuthority{}).SelectExecutor(context.Background(), hostclaim.Observed{}, Record{})
	if err != nil || selected || sel != (hostclaim.ExecutorSelection{}) {
		t.Fatalf("no chooser: %+v %v %v", sel, selected, err)
	}
	// With a chooser the selection is the chooser's, read from its
	// evidence: box-a is draining, so box-b with its roster enrollment;
	// with both draining, no box and an error, never a selection.
	x, _, snap, _ := chooserFixture(t, "box-a", "box-b")
	snap.Boxes[0].Draining = true
	absent := hostclaim.Observed{Host: "shop.bab.oncarlos.com", Absent: true}
	sel, selected, err = (ProductionAuthority{Executors: &x}).SelectExecutor(context.Background(), absent, chooserRecord())
	if err != nil || !selected || sel.Box != "box-b" || sel.Enrollment != strings.Repeat("b", 32) {
		t.Fatalf("with a chooser: %+v %v %v", sel, selected, err)
	}
	snap.Boxes[1].Draining = true
	if sel, selected, err = (ProductionAuthority{Executors: &x}).SelectExecutor(context.Background(), absent, chooserRecord()); !errors.Is(err, ErrNoEligibleBox) || selected {
		t.Fatalf("no eligible box: %+v %v %v", sel, selected, err)
	}
}

internal/console/hostclaimexecutor_test.go:

package console

import (
	"context"
	"slices"
	"testing"
	"time"

	"github.com/carlosframework/platform/internal/boxchoice"
	"github.com/carlosframework/platform/internal/hostactors"
	"github.com/carlosframework/platform/internal/hostclaim"
	"github.com/carlosframework/platform/internal/release"
)

// The console's chooser reads the bucket through its two production
// readers: the live edges (each box's edges file joined with its status
// snapshot) and the serving claims' loads. The bucket holds real evidence,
// the assertions name boxes and counts, and a change to the stored
// evidence shows in the next read, so neither reader can be replaced by
// one returning nothing (round 10).
func TestCreateExecutorChooserReadsTheLiveEdgesAndTheClaims(t *testing.T) {
	ctx := context.Background()
	store := release.NewDirStore(t.TempDir())
	off := &Server{cfg: Config{Releases: store, HomeRegion: "ie"}}
	if off.executorChooser(hostactors.Directory{Store: store, Bucket: "bucket"}) != nil {
		t.Fatal("a chooser with CARLOS_REGION_HA off: create would change")
	}
	s := &Server{cfg: Config{Releases: store, HomeRegion: "ie", RegionHA: true}}
	x := s.executorChooser(hostactors.Directory{Store: store, Bucket: "bucket"})
	if x == nil || x.Edges == nil || x.Loads == nil || x.Now == nil || x.HomeName != "ie" || x.SecretsKeyFP != s.expectedSecretsFP() {
		t.Fatalf("chooser: %+v", x)
	}

	// Two live boxes in ie, each with its edges file and a fresh status
	// snapshot; box-b advertises the region-ha-1 capability.
	edges := func(box, extra string) string {
		return `{"v":1,"box":"` + box + `","box_id":"` + box + `","eip":"203.0.113.1","region":"eu-west-1","placement":"ie","hibernation_configured":true` + extra + `,"hosts":{}}`
	}
	for box, body := range map[string]string{"box-a": edges("box-a", ""), "box-b": edges("box-b", `,"capabilities":["`+boxchoice.Capability+`"]`)} {
		setBoxSnapshot(t, store, box, time.Now())
		if _, err := store.Put(ctx, "control/edges/"+box+".json", []byte(body), ""); err != nil {
			t.Fatal(err)
		}
	}
	// Two serving claims on box-a for bab/jam, one on box-b for bab/tea.
	created := time.Date(2026, 10, 4, 1, 0, 0, 0, time.UTC)
	serve := func(host, app, box string) {
		t.Helper()
		nh := hostclaim.NewHolder{Family: "instance", Key: "apps/bab/" + app + "/instances/" + host + ".json", Account: "bab", App: app, Host: host, Region: "ie", RecordRegion: "ie", CreatedAt: created}
		body := []byte(`{"host":"` + host + `","account":"bab","app":"` + app + `","region":"ie","created_at":"2026-10-04T01:00:00Z"}`)
		o, err := hostclaim.Read(ctx, store, host)
		if err != nil {
			t.Fatal(err)
		}
		if o, err = hostclaim.Update(ctx, store, o, hostclaim.BeginCreate(nh, body, "c", "console", created)); err != nil {
			t.Fatal(err)
		}
		if _, err = hostclaim.Update(ctx, store, o, hostclaim.CompleteCreate("c", box)); err != nil {
			t.Fatal(err)
		}
	}
	serve("a.bab.oncarlos.com", "jam", "box-a")
	serve("b.bab.oncarlos.com", "jam", "box-a")
	serve("c.bab.oncarlos.com", "tea", "box-b")

	read := func() (map[string]boxchoice.Box, map[string]boxchoice.Load) {
		t.Helper()
		snap, err := x.Edges(ctx)
		if err != nil || !snap.Complete {
			t.Fatalf("edges: %+v %v", snap, err)
		}
		boxes := map[string]boxchoice.Box{}
		for _, b := range snap.Boxes {
			boxes[b.BoxID] = b
		}
		loads, err := x.Loads(ctx)
		if err != nil {
			t.Fatal(err)
		}
		return boxes, loads
	}
	boxes, loads := read()
	if len(boxes) != 2 || !boxes["box-a"].Fresh || !boxes["box-b"].Fresh || boxes["box-a"].Placement != "ie" ||
		slices.Contains(boxes["box-a"].Capabilities, boxchoice.Capability) || !slices.Contains(boxes["box-b"].Capabilities, boxchoice.Capability) {
		t.Fatalf("live edges: %+v", boxes)
	}
	if loads["box-a"].Hosts != 2 || loads["box-a"].Apps["bab/jam"] != 2 || loads["box-b"].Hosts != 1 || loads["box-b"].Apps["bab/tea"] != 1 {
		t.Fatalf("loads: %+v", loads)
	}

	// The evidence changes: box-a starts draining and stops reporting
	// (stale), and a fourth host serves on box-b. The next read says so.
	_, etag, err := store.Get(ctx, "control/edges/box-a.json")
	if err != nil {
		t.Fatal(err)
	}
	if _, err := store.Put(ctx, "control/edges/box-a.json", []byte(edges("box-a", `,"draining":true`)), etag); err != nil {
		t.Fatal(err)
	}
	setBoxSnapshot(t, store, "box-a", time.Now().Add(-time.Hour))
	serve("d.bab.oncarlos.com", "tea", "box-b")
	boxes, loads = read()
	if !boxes["box-a"].Draining || boxes["box-a"].Fresh || !boxes["box-b"].Fresh {
		t.Fatalf("live edges after the change: %+v", boxes)
	}
	if loads["box-b"].Hosts != 2 || loads["box-b"].Apps["bab/tea"] != 2 || loads["box-a"].Hosts != 2 {
		t.Fatalf("loads after the change: %+v", loads)
	}
}

cmd/console/regionha_test.go (the switch that sets Config.RegionHA):

package main

import "testing"

// CARLOS_REGION_HA reaches Config.RegionHA through regionHAEnabled
// (strconv.ParseBool): only a true value turns the console's create-time
// chooser on; unset, false and garbage leave create as today.
func TestRegionHAEnabledParsesTheSwitch(t *testing.T) {
	for v, want := range map[string]bool{"": false, "0": false, "false": false, "no": false, "garbage": false,
		"1": true, "t": true, "true": true, "TRUE": true, " true ": true} {
		got := regionHAEnabled(func(k string) string {
			if k != "CARLOS_REGION_HA" {
				t.Fatalf("read %s", k)
			}
			return v
		})
		if got != want {
			t.Errorf("CARLOS_REGION_HA=%q: %v, want %v", v, got, want)
		}
	}
}

• [ ] Step 2: Run them to see them fail

Run: nice -n 19 go test ./internal/hostclaim/ ./internal/hostops/ ./internal/console/ -run 'SelectedExecutor|ExecutorChooser|ClaimLoads|ProductionAuthoritySelects|CreateIsTodays' -count=1 Expected: FAIL to compile: undefined: ExecutorSelection, undefined: BeginCreateOn, undefined: ExecutorChooser, undefined: ClaimLoads, s.executorChooser undefined.

• [ ] Step 3: Record the selection in the create intent

Apply to internal/hostclaim/create.go:

diff --git a/internal/hostclaim/create.go b/internal/hostclaim/create.go
index c8fe97cc..39badc04 100644
--- a/internal/hostclaim/create.go
+++ b/internal/hostclaim/create.go
@@ -80,6 +80,32 @@ func BeginCreate(nh NewHolder, recordBody []byte, opID, by string, now time.Time
 	}
 }
 
+// ExecutorSelection is the box create selects once, with
+// boxchoice.Choose over the eligible set (claim P5-D2, region HA §5.2,
+// H12), and its roster enrollment.
+type ExecutorSelection struct {
+	Box, Enrollment string
+}
+
+// BeginCreateOn is BeginCreate recording the selected executor in the
+// create intent, in the same step 2 CAS, before any effect (claim §5.1,
+// P5-D6 `selected_executor`, `executor_enrollment`). CompleteCreate then
+// sets op.exec to exactly that box; recovery never substitutes another.
+func BeginCreateOn(nh NewHolder, recordBody []byte, opID, by string, now time.Time, sel ExecutorSelection) func(*Claim) error {
+	begin := BeginCreate(nh, recordBody, opID, by, now)
+	return func(c *Claim) error {
+		if !validBoxReference(sel.Box) || sel.Box == "none" || sel.Enrollment == "" {
+			return fmt.Errorf("%w: create needs a selected executor", ErrMalformed)
+		}
+		if err := begin(c); err != nil {
+			return err
+		}
+		c.Op.Intent["selected_executor"] = sel.Box
+		c.Op.Intent["executor_enrollment"] = sel.Enrollment
+		return nil
+	}
+}
+
 func CompleteCreate(opID, execBox string) func(*Claim) error {
 	return func(c *Claim) error {
 		if err := RequireOp(opID)(c); err != nil {
@@ -88,6 +114,9 @@ func CompleteCreate(opID, execBox string) func(*Claim) error {
 		if c.Op.Kind != KindCreating || execBox == "" {
 			return fmt.Errorf("%w: kind %q", ErrWrongState, c.Op.Kind)
 		}
+		if selected := c.Op.Intent["selected_executor"]; selected != "" && execBox != selected {
+			return fmt.Errorf("%w: create selected %s; completion never substitutes %s", ErrWrongState, selected, execBox)
+		}
 		if err := requireNoCreateAuthority(c); err != nil {
 			return err
 		}

• [ ] Step 4: The chooser and the loads

internal/hostops/executor.go:

package hostops

import (
	"context"
	"errors"
	"fmt"
	"time"

	"github.com/carlosframework/platform/internal/boxchoice"
	"github.com/carlosframework/platform/internal/hostactors"
	"github.com/carlosframework/platform/internal/hostclaim"
)

// ErrNoEligibleBox is a create refused because no box in the placement is
// eligible (region HA §5.2). The console maps it to today's refusal.
var ErrNoEligibleBox = errors.New("hostops: region has no box that can take this")

// ExecutorChooser is create's executor selection: claim P5-D2's choose()
// over the complete eligible set (region HA spec 1 §5.2, H12, L8). It is
// made once, before the create CAS, and recorded in the create intent.
type ExecutorChooser struct {
	Directory hostactors.Directory
	// Edges is one read of every box's edges file with the caller's
	// liveness verdict per box. An incomplete snapshot selects nothing.
	Edges func(context.Context) (boxchoice.Snapshot, error)
	// Loads counts claimed hosts per box and per "acct/app", from the
	// claim-recovery listing (claim §5.1 step 5). A stale count only
	// affects balance, never safety.
	Loads        func(context.Context) (map[string]boxchoice.Load, error)
	SecretsKeyFP string
	HomeName     string
	Now          func() time.Time
}

// Choose returns the box, and its roster enrollment, that a new host in
// r's placement is created on. Identity, placement and AWS region come from
// the roster; a box with a valid termination fence, or not active, is never
// chosen; a box on the claim's lost list, or owing a park-local chore on
// it, is never chosen.
func (x ExecutorChooser) Choose(ctx context.Context, obs hostclaim.Observed, r Record) (hostclaim.ExecutorSelection, error) {
	o, cands, err := x.eligible(ctx, obs, r)
	if err != nil {
		return hostclaim.ExecutorSelection{}, err
	}
	loads, err := x.Loads(ctx)
	if err != nil {
		return hostclaim.ExecutorSelection{}, err
	}
	best, ok := boxchoice.Choose(r.Holder.Host, cands, loads, r.Holder.Account+"/"+r.Holder.App)
	if !ok {
		return hostclaim.ExecutorSelection{}, ErrNoEligibleBox
	}
	return hostclaim.ExecutorSelection{Box: best.BoxID, Enrollment: o.Roster.Boxes[best.BoxID].Enrollment}, nil
}

// Permits reports whether box is in the complete eligible set for a host
// in r's placement now (spec 1 §2, §5.8 "The start CAS ... refused ...
// when `to` is not eligible for the host"): the same read Choose makes,
// without choosing. A stale edges file, a missing capability or secrets
// key, a draining box, a fence, or an incomplete snapshot refuses.
func (x ExecutorChooser) Permits(ctx context.Context, obs hostclaim.Observed, r Record, box string) error {
	_, cands, err := x.eligible(ctx, obs, r)
	if err != nil {
		return err
	}
	for _, c := range cands {
		if c.BoxID == box {
			return nil
		}
	}
	return fmt.Errorf("%w: %s", ErrNoEligibleBox, box)
}

// eligible is one read of the roster, the fences and the edges files,
// reduced to boxchoice.Eligible's candidates.
func (x ExecutorChooser) eligible(ctx context.Context, obs hostclaim.Observed, r Record) (hostactors.Observed, []boxchoice.Candidate, error) {
	placement := r.Holder.Region
	if x.Edges == nil || x.Loads == nil || x.Now == nil || placement == "" {
		return hostactors.Observed{}, nil, ErrContract
	}
	o, err := x.Directory.Read(ctx)
	if err != nil {
		return hostactors.Observed{}, nil, err
	}
	region, ok := o.Roster.Regions[placement]
	if !ok || region.AWSRegion == "" {
		return hostactors.Observed{}, nil, ErrContract
	}
	roster := map[string]boxchoice.RosterBox{}
	for ref, b := range o.Roster.Boxes {
		if b.State != "active" || b.Region != placement {
			continue
		}
		fenced, err := x.Directory.TerminationFence(ctx, o, ref, x.Now())
		if err != nil {
			return hostactors.Observed{}, nil, err // C6: a read error never means "not fenced"
		}
		if !fenced {
			roster[ref] = boxchoice.RosterBox{Placement: b.Region, Cloud: b.Cloud}
		}
	}
	snap, err := x.Edges(ctx)
	if err != nil {
		return hostactors.Observed{}, nil, err
	}
	// Never a box on the claim's lost list, nor one that still owes a
	// park-local chore for this host (spec 1 §2: its old installation is
	// not yet retired).
	excluded := map[string]bool{}
	if !obs.Absent && obs.Claim != nil {
		for _, box := range obs.Claim.Lost {
			excluded[box] = true
		}
		for _, box := range hostclaim.LocalChoreBoxes(obs.Claim) {
			excluded[box] = true
		}
	}
	return o, boxchoice.Eligible(snap, roster, placement, region.AWSRegion, x.HomeName, x.SecretsKeyFP, excluded), nil
}

internal/hostops/loads.go:

package hostops

import (
	"context"
	"log"
	"strings"

	"github.com/carlosframework/platform/internal/boxchoice"
	"github.com/carlosframework/platform/internal/hostclaim"
	"github.com/carlosframework/platform/internal/release"
)

// ClaimLoads counts, from one listing of control/hosts/, the hosts whose
// claim names each box as op.exec, in total and per "acct/app": choose()'s
// second rule until spec 2 (region HA §5.2, claim P5-D2). The count only
// balances, so a claim that cannot be read is logged and left out; a
// listing that fails is an error, because a count of nothing would send
// every create to one box.
func ClaimLoads(ctx context.Context, s release.Store) (map[string]boxchoice.Load, error) {
	keys, err := s.List(ctx, "control/hosts/")
	if err != nil {
		return nil, err
	}
	out := map[string]boxchoice.Load{}
	for _, key := range keys {
		name, ok := strings.CutPrefix(key, "control/hosts/")
		host, isJSON := strings.CutSuffix(name, ".json")
		if !ok || !isJSON || strings.Contains(host, "/") {
			continue
		}
		obs, err := hostclaim.Read(ctx, s, host)
		if err != nil {
			log.Printf("hostops: claim loads: %s: %v", host, err)
			continue
		}
		if obs.Absent || obs.Claim.Holder == nil || obs.Claim.Op.Exec == "" || obs.Claim.Op.Exec == "none" {
			continue
		}
		box, h := obs.Claim.Op.Exec, obs.Claim.Holder
		l := out[box]
		if l.Apps == nil {
			l.Apps = map[string]int{}
		}
		l.Hosts++
		l.Apps[h.Account+"/"+h.App]++
		out[box] = l
	}
	return out, nil
}

• [ ] Step 5: Select before the create CAS, or create as today

Apply to internal/hostops/operations.go:

diff --git a/internal/hostops/operations.go b/internal/hostops/operations.go
index 8313b80e..d3f1665a 100644
--- a/internal/hostops/operations.go
+++ b/internal/hostops/operations.go
@@ -14,6 +14,12 @@ import (
 // These callbacks are authority providers, not optional best-effort hints.
 // Production construction waits for the decisions named in this plan.
 type Authority interface {
+	// SelectExecutor chooses the new host's executor once, before the
+	// create CAS (claim P5-D2, region HA §5.2). selected false means this
+	// deployment does not choose at create (CARLOS_REGION_HA off): the
+	// create proceeds exactly as today, and Executor names the box at
+	// completion. Production is ExecutorChooser.Choose behind that switch.
+	SelectExecutor(context.Context, hostclaim.Observed, Record) (sel hostclaim.ExecutorSelection, selected bool, err error)
 	Create(context.Context, hostclaim.Observed, Record, string) error
 	Executor(context.Context, hostclaim.Observed, Record) (string, error)
 	StartDelete(context.Context, hostclaim.Observed, Record) error
@@ -46,11 +52,21 @@ func (c Controller) Attempt(ctx context.Context, before hostclaim.Observed, r Re
 	if before.Host != r.Holder.Host || r.Holder.CreatedAt.IsZero() || id == "" {
 		return hostclaim.Observed{}, ErrIdentity
 	}
+	// With region HA on, the executor is selected once, before the CAS,
+	// and recorded in it; off, the create is today's.
+	sel, selected, err := c.Authority.SelectExecutor(ctx, before, r)
+	if err != nil {
+		return hostclaim.Observed{}, err
+	}
+	begin := hostclaim.BeginCreate(r.Holder, r.Body, id, by, c.Now())
+	if selected {
+		begin = hostclaim.BeginCreateOn(r.Holder, r.Body, id, by, c.Now(), sel)
+	}
 	// Last pre-CAS read of registration, open admission and purge reservation.
 	if err := c.Authority.Create(ctx, before, r, id); err != nil {
 		return hostclaim.Observed{}, err
 	}
-	obs, err := hostclaim.Update(ctx, c.Store, before, hostclaim.BeginCreate(r.Holder, r.Body, id, by, c.Now()))
+	obs, err := hostclaim.Update(ctx, c.Store, before, begin)
 	if err != nil {
 		return hostclaim.Observed{}, err
 	}

Apply to internal/hostops/backfill_controller.go (the backfill grants no create):

diff --git a/internal/hostops/backfill_controller.go b/internal/hostops/backfill_controller.go
index 08ebd856..dcbf750e 100644
--- a/internal/hostops/backfill_controller.go
+++ b/internal/hostops/backfill_controller.go
@@ -23,6 +23,9 @@ func (a BackfillAuthority) Adoption(ctx context.Context, r Record) (string, stri
 }
 func (a BackfillAuthority) ClaimBackfill() *Backfill { return a.p.Backfill }
 
+func (a BackfillAuthority) SelectExecutor(context.Context, hostclaim.Observed, Record) (hostclaim.ExecutorSelection, bool, error) {
+	return hostclaim.ExecutorSelection{}, false, nil // the backfill grants no create (Create refuses)
+}
 func (a BackfillAuthority) Create(context.Context, hostclaim.Observed, Record, string) error {
 	return ErrContract
 }

Apply to internal/hostops/backfill.go:

diff --git a/internal/hostops/backfill.go b/internal/hostops/backfill.go
index e20b1982..7c727f9d 100644
--- a/internal/hostops/backfill.go
+++ b/internal/hostops/backfill.go
@@ -89,6 +89,22 @@ type ProductionAuthority struct {
 	Signer                           release.Signer
 	Evidence                         hostactors.Evidence
 	Backfill                         *Backfill
+	// Executors is create's executor selection (region HA §5.2, L8). The
+	// create door sets it only with CARLOS_REGION_HA on; nil keeps today's
+	// create path, so a c