Region HA: the joint model with two boxes per region (L18) Implementation Plan (rev 11)

> 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: Extend internal/sim/hostlife, the joint executable model of the host lifecycle claim and instance moves, from one box per region to one or two boxes per region, with region HA's relocating operation modelled as spec 1 §5.8 and plan 1b-next rev 19 define it (drain, failover, pinning, the replacement table, stuck), every case claim rev 6.30 §11 and spec L18 name for region HA's validation milestone as a scenario in a one-box and in a two-box region, and one mutation check per guard; then write the brief for the joint round that gates the merge of relocation (claim §1.1, R18-3; plan 1b-next Task 11).

Architecture: Fourteen tasks (rev 4 adds Task 5B, rev 5 Task 5C, rev 7 Task 5D, rev 8 Task 5E, rev 9 Task 5F, rev 10 Task 5G, rev 11 Task 5H) over one Go test package (every file is _test.go; nothing here is product code). Task 1 generalises the world's shape (boxesPerRegion, 1 or 2) so the one-box sweep stays byte-identical to the baseline and a two-box sweep runs beside it. Task 2 replaces the collapsed relocate with spec §5.8's full phase table for a drain, with 1b-next rev 16's guards on it: the release sequence and its deadline, the acknowledgement barrier on every phase change, the pin bound to the claim version it was selected against and to an evidenced empty listing, the prepared generation, the local install with its receipt, EnsureLocal before P's first admission and VerifyReceipt after it, prepared_opened journaled, three probe attempts counted before they are made, released coverage, the row cases, nested relocation after probe-failed and the replacement cap. Task 3 adds termination by the cloud with the regional worker's fence (lost, timers declared, regional chores passed to the region, local chores discharged only on qualifying volume evidence), automatic enrollment, failover from serving, source loss, the target replacement table, the phase-sensitive exhausted-target fence and the park-local exclusion from replacement. Task 4 adds the files publisher, P's prepared manifest at sequence 0, the files pin and the files live set. Task 5 writes the scenarios: a witness for every safety guard, every L18 case in a one-box and in a two-box region, claim §11's extras, direct evidence for every bound, and three findings. Task 5B (rev 4) answers Astra's round 1 on this plan: faithful guards with a discriminating test each, the exact phase matrix and claim §11's remaining cases. Task 5C (rev 5, regenerated in rev 6) answers rounds 2 and 3: PinFailover's barrier before an initial failover's pin, the boundary between the published marker and the open replication, and the adverse volume under a failover. Task 5D (rev 7) answers round 4: the target is named before any pin on every path, the phase predicates know PinFailover, and a failover passes Worker.Start's guards. Task 5E (rev 8) answers round 5: a pending fence holds the phase, as Worker.Step's early return does. Task 5F (rev 9) answers round 6: a release needs its own flush or the positions it recorded. Task 5G (rev 10) answers round 7: a stopped box keeps its local cleanup, and the operator stops only a target whose release cannot come. Task 5H (rev 11) answers round 8: recorded positions finish a release only for their own controller or with root's receipt. Task 6 wires the shape and the region HA rule group into mutate.sh and expected-outcomes.txt. Task 7 writes the joint-round brief against 1b-next rev 16. Every rule is a named guard in rules_test.go whose comment names the 1b-next function it mirrors.

Tech Stack: Go 1.26 test files, standard library only (the model imports nothing else; hash/fnv for the tie-break stand-in over the box id in Tasks 1 to 5A; from Task 5B crypto/sha256 over the host, as 1b-next hashes it). go test ./internal/sim/hostlife/ is the gate; mutate.sh runs the prebuilt binary per rule.

Spec: region HA spec 1 docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md on origin/main (rev 5.4 with §24; rulings H1 to H19 in §0; §2 words; §3 invariants HA1 to HA7; §5.2 create; §5.3 rows; §5.4 edges; §5.6 files; §5.8 relocation; §5.9 the fence; §5.10 updates; §7 failure modes; §9 L1 to L20). Plan 1b-next rev 19 (rev 2 of this plan synced to rev 16; rev 3 adds rulings 25 to 27, the "Rev 17" to "Rev 19" dispositions and request L21) git show origin/plan-region-ha-1b-next:docs/superpowers/plans/2026-10-07-region-ha-1b-next-relocation.md (Astra's round 18: "stage A ready to build"; its rulings 1 to 24, its dispositions tables for revs 2 to 16, Task 1's transitions, Task 5's worker and pinner, Task 6's participant, Task 11's merge gate) and the review findings beside it, CODEX-PLAN-REGION-HA-1BN-R1.md to R18.md. Claim rev 6.30 git show origin/design-replica-ownership:docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md (§4 "Same-region relocation (L1)"; §6.2a "Files in the live set (L13)"; §6.4a item 2; §7.3 D2 to D6; §11 "Region HA's validation milestone" and the additional witnesses). Moves rev 7.22 on this branch, docs/superpowers/specs/2026-10-02-move-any-app-design.md (§7.6, §7.10 the conversion; §14.2 the model, its evidence policy and the harness). The model's own rules are in internal/sim/hostlife/rules_test.go; read world_test.go's package comment and §14.2 before Task 1.

Rev 11: round 8 dispositions

Astra's round 8 (CODEX-PLAN-REGION-HA-TWO-BOX-R8.md, against 54a37976) found both round 7 findings resolved and raised one P2 and one P3. Its verdict was "not ready". Both are accepted. The P2 is fixed in a new Task 5H, a patch on Task 5G's tree, and Task 6's patch is regenerated on top of it. The P3 is fixed in Task 1 Step 1's identity test; the later tasks' patches do not touch that file.

| # | Evidence checked | Disposition | What changed | Where | Guard removed: the test that fails | |---|---|---|---|---|---| | R8 #1 (P2) | Correct. In 1b-next rev 19 (Task 7), Release records the flushed positions before the producers drain and before root persists the stop receipt. After a restart the request names the recorded identity, RecoveryReleaseDrain refuses, and only root's durable receipt finishes the release. A retry by the same controller resumes at the producers' drain. Rev 9's releaseRecord replayed the positions alone, so a crash between the record and the receipt looked like a finished stop. | accepted | releaseRecord now keeps the flushing controller (Ctl, the agent process: box.Epoch) and Receipt, root's persisted stop receipt, apart from the positions. The release sequence ends at the record. The next step, by the same controller, is the producers' drain and the receipt, and only then is the release returned. After a restart a record with a receipt replays. A record without one is refused, so there is no release and the deadline makes the operation stuck. releaseUnrecoverable counts a record as recoverable only with the receipt, or while its own controller still runs. This is the new rule reloc-release-needs-receipt. Its mutation replays the positions alone, as rev 10 did. It is an expected miss: the replayed release is the flushed one, so no invariant fails. | Task 5H | TestReleaseRefusedAfterACrashBeforeTheReceipt: the source records, then crashes before the receipt. No release and no pin appear, it is stuck at the deadline, and the resolve returns the host to the source. TestOperatorStopsATargetWithNoReceipt: the same for a failed target, which the operator stops before the host serves elsewhere. Both fail under the mutation. The other side of the receipt, a crash after it, is TestReleaseReplaysTheRecordedFlush and TestOperatorResumesARecordedFlush, whose release sequence now runs through the receipt before the crash. | | R8 #2 (P3) | Correct. TestOneBoxSeedTraces hashed seeds 0 to 299, and the gate's sweep runs 1 to 300. | accepted | The identity loop runs 1..n, the gate's range, and its 300 lines are seeds 1 to 300. | Task 1 Step 1 | (coverage) |

Astra also noted that R5-3 (HA-disabled reconcile) and R5-5 (the env file's deletion) rest on 1b-next's own tests. They join the adapter-only rows of "Past findings, and where their evidence lives" (rev 4); the model has no step for either.

Dry run (2026-10-08). The scratch module was rebuilt from the baseline. The corrected identity test was added and the baseline's traces recorded with it, and Task 1 was applied from prose. The patches for Tasks 2 to 5G were applied from this document, then Task 5H and the regenerated Task 6. After each: build, vet, gofmt, the gate, and the COUNTERS and both trace files compared byte for byte with the baseline's. The seed file runs 1 to 300.

| After | One-box COUNTERS and traces | Two-box | Gate | |---|---|---|---| | Tasks 1 to 5G | identical | as in rev 10 | ok | | Task 5H | identical | 300, 0 failed, 483. The release's receipt is its own step, so the sweep's trajectories moved: 9 receipts persisted, 12 releases refused, and 2 targets stopped by the operator. | ok. The two new tests pass and fail under reloc-release-needs-receipt. Both replay tests still pass. | | Task 6 | the same | the same | ok. @regionha lists 54 rules, 162 in all. |

No mutation sweep was run, and the scratch module was then removed.

Rev 10: round 7 dispositions

Astra's round 7 (CODEX-PLAN-REGION-HA-TWO-BOX-R7.md, against 979c38da) found round 6's finding resolved and raised two new P2s. Its verdict was "not ready". Both are accepted and fixed in a new Task 5G, a patch on Task 5F's tree. Task 6's patch is regenerated on top of it. Tasks 1 to 5F are unchanged.

| # | Evidence checked | Disposition | What changed | Where | Guard removed: the test that fails | |---|---|---|---|---|---| | R7 #1 (P2) | Correct. 5F's operator stop leaves the box's disk and Terminated=false. The next resolve's declared loss calls fenceBox, whose discharge read only DeleteOnTermination, so the stopped box went into Op.Discharged and completion queued no park-local for it. Claim §7.3 D5 and H19 keep a stopped box's local retirement owed. In 1b-next rev 19 fenceBox runs only under a verified termination fence, so the gap was the model's own. | accepted | Automatic discharge needs Terminated and qualifying volume evidence (rule fence-discharge-qualified, its predicate tightened). A stopped box is never fenced automatically (fence-terminated-only, unchanged). Its declared loss on the operator's path puts it on lost and discharges nothing, so its park-local stays owed. INV-26 now also fires when a box enters Op.Discharged without being terminated with qualifying evidence, even though no chore exists yet. The operator's destroyed-local declaration (claim §7.2) stays a separate, explicit attestation. | Task 5G; plan ruling 10 | TestStoppedTargetKeepsItsLocalCleanup: the failed target loses its database and files, so the operator stops it (with DeleteOnTermination=true), the next resolve replays, and the recovery completes with no operator cleanup. The box's park-local must still be owed. Under fence-discharge-qualified's mutation INV-26 fires. | | R7 #2 (P2) | Correct. 5F's condition was a live target, stuck in probe-failed with no journaled release. It never checked the replicator, the files or a recorded flush, so a release that was merely slow was stopped. 1b-next rev 19 has no operator resolve; the spec leaves carlos ops host resolve open and plan ruling 13 is the model's own. So 1b-next has nothing over-broad to report. The stop was this plan's addition. | accepted | releaseUnrecoverable: the operator stops the box only when no flush is recorded for this stop and the session's replicator or the box's files are gone. Either loss makes relocRelease refuse for good. In every other case the resolve clears stuck and sends the target back to probe-failed, where its release resumes. The new rule operator-stop-unrecoverable-only is the model's operator rule; its mutation is rev 9's broad stop. It is an expected miss: the declared loss that follows is legal in the model. | Task 5G; plan ruling 13 | TestOperatorResumesASlowRelease: the failed target's final manifest PUT is held past the deadline. The resolve must resume rather than stop, and once the PUT lands the release journals and the host serves. TestOperatorResumesARecordedFlush: the release is recorded and then the agent restarts before the journal. The resolve must resume, and the record is replayed. Both fail under the mutation. The missing-state case is TestStoppedTargetKeepsItsLocalCleanup and the reloc-verify-receipt witness. |

Against 1b-next. Neither finding is a 1b-next defect. fenceBox there is reached only through a verified termination fence (VerifyFence in StartRelocation, FenceSource, ReplaceTarget and fenceTargetStuck). Its LocalDischarge comes from the volume recorder for that termination. 1b-next writes no operator resolve, so it has no stop to over-apply. The model's operator path (ruling 13) is what both fixes narrow.

Dry run (2026-10-08). The scratch module was rebuilt from the baseline, with the identity tests and Task 1 from prose. The patches for Tasks 2 to 5F were applied from this document, then Task 5G and the regenerated Task 6. After each: build, vet, gofmt, the gate, and the COUNTERS and both trace files compared byte for byte with the baseline's.

| After | One-box COUNTERS and traces | Two-box | Gate | |---|---|---|---| | Tasks 1 to 5F | identical | as in rev 9 | ok | | Task 5G | identical | 300, 0 failed, 486. The operator stopped 3 targets, each unrecoverable, and resolved 7 stuck operations. | ok. The three new tests pass. Both resume tests fail under operator-stop-unrecoverable-only, and the stopped-target test fails under fence-discharge-qualified (INV-26). | | Task 6 | the same | the same | ok. @regionha lists 53 rules, 161 in all. |

No mutation sweep was run, and the scratch module was then removed.

Rev 9: round 6 dispositions

Astra's round 6 (CODEX-PLAN-REGION-HA-TWO-BOX-R6.md, against b9d0046d) found round 5's finding resolved and raised one new P2. Its verdict was "not ready". It is accepted and fixed in a new Task 5F, a patch on Task 5E's tree. Task 6's patch is regenerated on top of it. Tasks 1 to 5E are unchanged.

| # | Evidence checked | Disposition | What changed | Where | Guard removed: the test that fails | |---|---|---|---|---|---| | R6 #1 (P2) | Correct. When the session's replicator was gone (an agent crash changes the epoch), relocRelease took the remote position and returned a release with Flushed=false, and the drain went on to pinning. In 1b-next rev 19 (Task 7), relocationFlushDB refuses without the session's replicator, and releaseDrain returns that error. Release recovers only from positions recorded against the exact stop (ReleasePositions); a replayed receipt with no recorded flush is refused. | accepted | relocRelease now returns nothing unless the box holds the session's own database and replicator (same incarnation, generation, epoch and session). The exception is a releaseRecord: the positions this box recorded for this stop (operation, phase, session, generation) once its writers stopped and its database and files flushed. That record is durable on its disk and survives an agent restart, and the release is then replayed from it unchanged. Otherwise the release deadline makes the operation stuck. This is the new rule reloc-release-needs-flush. Its mutation is rev 8's fallback. It is an expected miss: the fallback's declared loss is legal in the model. | Task 5F | TestReleaseRefusedAfterACrashBeforeTheFlush: the source crashes with its flush's upload held. No release and no pin appear; at the deadline the operation is stuck in releasing, and the operator's resolve returns the host to its source. TestReleaseReplaysTheRecordedFlush: the release sequence completes and records, the agent crashes before the journal, and the journaled release must be the recorded one (Flushed, the same final_txid and manifest_seq). Both fail under the mutation. |

Every release and flush path, compared with 1b-next Task 7.

| 1b-next rev 19 | Model before rev 9 | Rev 9 | |---|---|---| | releaseDrain steps 1 to 3 in order: StopWriters, Observe (the tree empty), FlushDB, FlushFiles, then Positions.Record, then the producers' drain and root's receipt | holdRow, evidence, the database flush, the files manifest, the entry | same order; the record is written last, as Record is | | relocationFlushDB: the session's replicator (att.rep) or ErrClaimStopUnavailable; SyncAndWait; N from the listing; no LTX file means N = 0 | fell back to the remote position, Flushed=false, when the box had no database of the session (a failed target that never admitted) or its replicator was gone | Fixed: refused (R6 #1) | | ReleaseFlushFiles: this box's own files directory, wake state and env, committed as one revision even when unchanged | fell back to the files set its installation applied when the box held no files directory of the incarnation | Fixed: refused under the same rule. ReleaseFlushFiles publishes only what the box holds. | | Release after a restart: Positions.Recorded for this stop; a replayed receipt with no recorded flush is refused; a retry by the same controller resumes at the producers' drain without flushing again | no record; every retry flushed again or fell back | Fixed: releaseRecord, replayed unchanged for the same stop. The model has one controller identity per box and no receipt store, so both of 1b-next's recovery cases (another controller's durable receipt, and the same controller's resume) become this replay. | | JournalRelease: the release is of the executor's current session; for a session that admitted a writer, the writer box is the releaser | the CAS checks op.exec, the phase and that no release is journaled | same effect: a box without the session's own database no longer produces a release | | FenceSource in releasing before a release: no release is synthesised; the operation becomes a failover | the same (the synthesised release is reloc-source-loss's mutation only) | unchanged |

One consequence for the operator's resolve (plan ruling 13). A live target sent to probe-failed that has lost its database and files (the reloc-verify-receipt witness's volume replacement) can now never release, so the resolve looped. In that case the operator now stops the box. Claim D2's declared loss needs the box stopped, and the next resolve declares it lost and replays from pinning. The two-box gate's sweep refused 9 unflushed releases, and the operator stopped such a target 3 times. Every seed converged.

Dry run (2026-10-08). The scratch module was rebuilt from the baseline, with the identity tests and Task 1 from prose. The patches for Tasks 2 to 5E were applied from this document, then Task 5F and the regenerated Task 6. After each: build, vet, gofmt, the gate, and the COUNTERS and both trace files compared byte for byte with the baseline's.

| After | One-box COUNTERS and traces | Two-box | Gate | |---|---|---|---| | Tasks 1 to 5E | identical | as in rev 8 | ok | | Task 5F | identical | 300, 0 failed, 486 | ok. Both new tests pass, and both fail under reloc-release-needs-flush. Every witness holds, under every proper subset, and violates its named failure. | | Task 6 | the same | the same | ok. @regionha lists 52 rules, 160 in all. |

No mutation sweep was run, and the scratch module was then removed.

Rev 8: round 5 dispositions

Astra's round 5 (CODEX-PLAN-REGION-HA-TWO-BOX-R5.md, against 56ea4a15) found all three round 4 findings resolved and raised one new P2. Its verdict was "not ready". It is accepted and fixed in a new Task 5E, a patch on Task 5D's tree. Task 6's patch is regenerated on top of it. Tasks 1 to 5D are unchanged.

| # | Evidence checked | Disposition | What changed | Where | Guard removed: the test that fails | |---|---|---|---|---|---| | R5 #1 (P2) | Correct. fenceStep reported only a changed claim. When a terminated target had no eligible replacement before its deadline, replaceTarget refused the CAS, and workerMode went on into role and the phase switch. 1b-next rev 19's Worker.Step instead returns w.replace(...) as soon as it finds the target's fence, before the phase switch. | accepted | fenceStep now returns (changed, pending). A fence it could not consume for a relocation's source or target is pending. workerMode passes that to role as box.fencePending. While it is set, relocate makes no regional transition: no ToReleasing, PinAfterRelease, pin, ToInstalling or deadline marks. The live executor's own release sequence and its journal still run (relocJournalRelease), because that is the participant's work (1b-next Task 7), not Worker.Step's. So do leases, acknowledgements, cleanups and admissions, which role runs before relocate. This is the new rule reloc-fence-pending-blocks. Its mutation goes on into the phase switch. It is an expected miss: no invariant tells the phases apart, and the gate's two-box sweep never met a pending fence. | Task 5E | TestPendingTargetFenceHoldsThePhase, with subtests starting and pinning. A drain's target has acknowledged; in starting the source has not yet. The target is terminated, and the region's group launches no replacement. For releaseDeadline - 10 steps of the source's worker, the phase must not move, no pin may be selected, and the target must not be fenced. Past the deadline the fence is consumed into stuck. Under the mutation, both subtests fail at the first step (releasing; a pin). |

The worker's checks before the phase switch, compared with 1b-next Worker.Step in order.

| 1b-next Worker.Step | Model (workerMode, fenceStep, role, relocate) | Rev 8 | |---|---|---| | 1. ready, then self: a worker whose own box is fenced is not a worker | a destroyed box does not run; fenceStep and relocate refuse a box that is lost or unenrolled | same | | 2. read the claim; return unless relocating, in this worker's region, and not stuck | fenceStep considers boxes of the worker's own region only; fence consumes nothing for a stuck operation; relocate returns for another region or a stuck operation | same effect. The stuck check comes after fenceStep in the model, but fence refuses a stuck operation, so nothing is written. | | 3. the source's fence, if the source is not on lost: FenceSource, return | the source ranked first | same | | 4. the target's fence, if a target is named and not on lost: return w.replace(...), whatever it wrote | candidates were the source first, then any other named box in box order. The target could follow a chore owner's fence, and a refused replacement fell through to the phase switch. | Fixed: the order is source, then target, then other named boxes (a chore owner's fence is the termination worker's, not Worker.Step's). A refused replacement is pending and holds the phase (R5 #1). | | 5. the phase switch | relocate's switch | unchanged |

role runs participant work (lease renewal, recordAck, finishParticipation, the start's resume, admissions) between fenceStep and relocate. None of it is a Worker.Step transition, and all of it stays schedulable while a fence is pending. The stalled-worker fault (resumeStale) resumes a step read earlier, without a new fenceStep. It stands for a Worker.Step that stalled after its own fence checks: it revalidates the step (revalidate-before-effect), and its CAS carries the version it read. A pending fence writes nothing, so production's stalled step could make the same CAS. It is unchanged.

Dry run (2026-10-08). The scratch module was rebuilt from the baseline, with the identity tests and Task 1 from prose. The patches for Tasks 2 to 5D were applied from this document, then Task 5E and the regenerated Task 6. After each: build, vet, gofmt, the gate, and the COUNTERS and both trace files compared byte for byte with the baseline's.

| After | One-box COUNTERS and traces | Two-box | Gate | |---|---|---|---| | Tasks 1 to 5D | identical | as in rev 7 | ok | | Task 5E | identical | 300, 0 failed, 486 | ok. TestPendingTargetFenceHoldsThePhase passes, and both subtests fail under reloc-fence-pending-blocks. | | Task 6 | the same | the same | ok. @regionha lists 51 rules, 159 in all. |

No mutation sweep was run, and the scratch module was then removed.

Rev 7: round 4 dispositions

Astra's round 4 (CODEX-PLAN-REGION-HA-TWO-BOX-R4.md, against cc69376d) found both round 3 findings resolved and raised three new P2 fidelity findings. Its verdict was "not ready". All three are accepted, and each is fixed in a new Task 5D, a patch on Task 5C's tree. Task 6's patch is regenerated on top of it. Tasks 1 to 5C are unchanged.

| # | Evidence checked | Disposition | What changed | Where | Guard removed: the test that fails | |---|---|---|---|---|---| | R4 #1 (P2) | Correct. 1b-next rev 19's Worker.pinning names a missing target with NameTarget before it selects any pin. The model named it before the pin only while PinFailover was set, so a converted move or a replay could pin while no box was eligible and miss a manifest that landed meanwhile. | accepted | A relocation at pinning with no target names one before anything else, on every path. With no eligible box it waits. New rule reloc-name-before-pin; its mutation pins first, as rev 6 did. It is an expected miss (a loss bound). The acknowledgement barrier stays the initial failover's alone. | Task 5D | TestConvertedMoveWaitsForATargetBeforeItsPin: the source's newer manifest is in flight and no box of the region is eligible. No target and no pin appear past the delay. The manifest lands, a box becomes eligible, and the pin must name the newer manifest. TestConvertedMovePinsBeforeAcknowledgement is rewritten: the target is named while there is no pin, and its controller then does not run while another worker pins. The pin is journaled without its acknowledgement, and installing waits for it. | | R4 #2 (P2) | Correct. atPhase("pinning") held while PinFailover was still set, which is production's starting, and the one-box matrix skipped starting. | accepted | relocPhaseName names the model's pinning with PinFailover set as starting. atPhase and the matrix's assertion use it, and pinning must also have the flag cleared and no executor. The one-box matrix now includes target@starting, so it has 25 subtests. | Task 5D | (coverage) TestL18TerminationAtEveryExactPhase one-box target@starting and target@pinning. Also TestFailoverTargetLossAroundPinFailover: in a two-box region with a spare, the failover's target is terminated with PinFailover set and, in a second run, after it cleared but before installation. In both runs it must be replaced in the same phase. | | R4 #3 (P2) | Correct. The fence of a serving executor called startFailover unconditionally. 1b-next's Worker.Start needs an eligible target and the app's admission registration and its recheck. StartRelocation then applies RelocationStartGuard with the source fenced. | accepted | failoverStart runs Worker.Start's checks in its order before the fence CAS: an eligible target, then admission open. failoverStartAllowed runs in the CAS: the admission recheck, the target not on lost, and relocationStartGuard(..., sourceFenced=true). The fenced source's own park-local does not block, as before, and a same-region park-replica does. Without a start nothing is fenced, so the claim still names the dead box and a later pass retries. The failover starts with its target named and as the only participant, as StartRelocation does. New rule reloc-failover-start-guard; its mutation starts at once with no target, as rev 6 did. It is an expected miss (no invariant tells the earlier start apart). | Task 5D | TestFailoverStartWaitsForAdmission (admission closed, then reopened). TestFailoverStartWaitsForParkReplica: a park-replica in region 0 and the source's own park-local (DeleteOnTermination=false). The start waits for the park-replica only, and the park-local stays open. TestL18UnenrolledReference and TestUnenrolledReferenceNeverChosen now expect the claim to stay serving, unfenced, until a box is eligible. |

Every entry point into a relocation, compared with 1b-next rev 19 in order. The comparison covers each guard's order as well as its presence. "Fixed" marks an ordering difference this revision corrects.

| Entry | 1b-next rev 19, in order | Model before rev 7 | Rev 7 | |---|---|---|---| | Drain start (userRelocate) | Worker.Start: serves on the source; Relocatable; Eligible(target); roster and region; the source not fenced; a writer session (ruling 11); CheckBoxStart; census; Admission.Register; Recheck. Then StartRelocation's CAS: op.exec is the source, the target not lost, RelocationStartGuard. | admission checked first, before the writer check and the target; no recheck in the CAS; no target-not-lost check | Fixed: writer check, eligible target, admission; the CAS rechecks admission, refuses a lost target, then applies the guard. The roster, census and H14 reservation checks have no model state. | | Failover start (fence of the serving executor) | the same Worker.Start, with the source's fence; StartRelocation cites it, names the target, enters starting, participants are the target alone; then starting: requireAcks, PinFailover | no target, no admission check, no start guard; target named later at pinning | Fixed (R4 #3): eligible target, then admission, before the CAS; recheck, target not lost and the guard (source fenced) in it; target named at the start; PinFailover flag for starting. | | Source lost in a drain (fenceSource) | FenceSource: in starting it stays in starting (then PinFailover); in releasing before a release it goes to pinning; after a release only the liveness changes | the same (rev 6) | unchanged | | Converted move (convertToRelocating) | moves §7.10's conversion enters pinning with no target; Worker.pinning: NameTarget, the fence delay, the pin under the lease, requireAcks, ToInstalling | pin first, then name the target | Fixed (R4 #1): name, delay, pin, acknowledgements, install. | | Nested failover (replaceTarget after P opened; relocProbeFailed) | Worker.replace: exhausted first, then next, with no spare the deadline; ReplaceTarget fences, names the replacement and goes to pinning in one CAS. probe-failed: release or its deadline, exhausted, next (none: deadline), PinAfterRelease names the target | the same order | unchanged; the target is named in the same CAS, so pinning starts with it | | Operator's replay (plan ruling 13) | no 1b-next code (the resolve is the claim's); it enters pinning like a converted move | pin first, then name | Fixed (R4 #1): it enters pinning with no target, so it names one first; PinFailover cleared. | | Committed landing (finding F5, model only) | none | flag set, target named at pinning | unchanged. It has no 1b-next path; its target is named first under the flag. |

Dry run (2026-10-08). The scratch module was rebuilt from the baseline, with the identity tests and Task 1 from prose. The patches for Tasks 2 to 5C were applied from this document, then Task 5D and the regenerated Task 6. After each: build, vet, gofmt, the gate, and the COUNTERS and both trace files compared byte for byte with the baseline's.

| After | One-box COUNTERS and traces | Two-box | Gate | |---|---|---|---| | Tasks 1 to 5C | identical | as in rev 6 | ok | | Task 5D | identical | 300, 0 failed, 486 (the sweep met "no eligible target yet" 5 times) | ok. TestConvertedMoveWaitsForATargetBeforeItsPin fails under reloc-name-before-pin. TestFailoverStartWaitsForAdmission and TestFailoverStartWaitsForParkReplica fail under reloc-failover-start-guard. TestFailoverPinWaitsForTheAcknowledgement still fails under its mutation. | | Task 6 | the same | the same | ok. @regionha lists 50 rules, 158 in all. |

No mutation sweep was run, and the scratch module was then removed.

Rev 6: round 3 dispositions

Astra's round 3 (CODEX-PLAN-REGION-HA-TWO-BOX-R3.md, against ee6e35f3) found all three of round 2's items resolved. It raised one new P2 and one P3, with the verdict "not ready". Both are accepted. Task 5C's patch is regenerated with the fixes (it is still a patch on Task 5B's tree), and Task 6's patch is regenerated on top of it. Tasks 1 to 5B are unchanged.

| # | Evidence checked | Disposition | What changed | Where | Evidence | |---|---|---|---|---|---| | R3 #1 (P2) | Correct. Rev 5's guard held every pin with no release, which covered converted moves, nested failovers after a replacement and operator replays. In 1b-next rev 19, only the initial failover waits for PinFailover's acknowledgements, on leaving starting. Those other three enter pinning directly, and Worker.pinning selects and journals the pin before it checks acknowledgements for ToInstalling. The model excluded that production interleaving. | accepted | PinFailover's barrier is now explicit. opState.PinFailover stands for 1b-next's starting after StartRelocation with a fence. It is set by startFailover and by a drain's source lost in starting (1b-next keeps that one in starting until PinFailover). While it is set, the target is named and acknowledges, then the PinFailover CAS clears the flag, all before any pin is selected. A converted move, a nested failover and a replay never set it, and the replay clears it. Rule reloc-failover-ack-before-pin now guards only the flagged case; its mutation still selects the pin first. | Task 5C; ruling 4 | TestFailoverPinWaitsForTheAcknowledgement is unchanged (initial failover) and still fails under the mutation. The new TestConvertedMovePinsBeforeAcknowledgement terminates a move's source before the flip. It checks that the pin is journaled before the installing box has acknowledged, and that the acknowledgement still comes before installing. Run against rev 5's Task 5C tree, it fails: "box 3 acknowledged before the pin". | | R3 #2 (P3) | Correct. 1b-next rev 19's CompleteRelocation queues the local chores and the abandoned prepared generations. It neither drops the pinner's retained control object nor parks the pinned manifest's generation. The obsolete manifest is not ownerless either: claim §6.2a gives obsolete files to the at-rest sweep, and 1b-next ruling 21 gives retained control objects to the storage follow-up. | accepted | The text in "Rev 5: round 2 dispositions", in relocationLeftovers' comment and in the brief now says this. The model parks the pinned manifest's generation at completion as its own abstraction of those two paths, so that INV-10 can check the residue at completion. It is not a CompleteRelocation guarantee and not a 1b-next finding. | Task 5C (comment); Rev 5 section; brief | text only |

Dry run (2026-10-08). The scratch module was rebuilt from the baseline, with the identity tests and Task 1 from prose. The patches for Tasks 2 to 5B were applied from this document, then the regenerated Task 5C and Task 6. After each: build, vet, gofmt, the gate, and the COUNTERS and both trace files compared byte for byte with the baseline's.

| After | One-box COUNTERS and traces | Two-box | Gate | |---|---|---|---| | Tasks 1 to 5B | identical | as in rev 5 | ok | | Task 5C (rev 6) | identical | 300, 0 failed, 486 | ok. TestFailoverPinWaitsForTheAcknowledgement fails under its mutation; TestConvertedMovePinsBeforeAcknowledgement passes, and fails on rev 5's tree. | | Task 6 | the same | the same | ok. @regionha lists 48 rules, 156 in all. |

No mutation sweep was run, and the scratch module was then removed.

Rev 5: round 2 dispositions

Astra's round 2 (CODEX-PLAN-REGION-HA-TWO-BOX-R2.md, against 64a0a793) found seven of round 1's findings resolved and one partly resolved, and raised two new P2s. Its verdict was "not ready". All three are accepted, and each is fixed in a new Task 5C, a patch on Task 5B's tree. Task 6's patch is regenerated on top of it. Tasks 1 to 5B are unchanged.

| # | Evidence checked | Disposition | What changed | Where | Guard removed: the test that fails | |---|---|---|---|---|---| | R1 #8 (partly resolved) | Correct. In the model, generation.json's landing, PublishGeneration and the replication's open run in one call of the start (resumeOpen's marker case falls through to open), so no test could stop between them. | accepted | A witness hook, world.openYield, returns from the start after the marker is published and before replication opens. The start resumes at open on its next call. It is nil outside the witnesses, so the sweeps don't change. TestCrashAtEachOpenBoundary gains a fourth stage, published. It stops there and checks that generation.json already names P, then crashes the target, in a one-box and a two-box region. | Task 5C | (coverage) published fails if the yield is not reached | | R2 #1 (P2) | Correct. A failover entered pinning with no target and journaled its pin before it named a target or checked acknowledgements. 1b-next rev 19's PinFailover needs every participant's acknowledgement before pinning. So a manifest that landed while the target's controller was down was missing from the pin. Ruling 4's phase collapse moved that guard. | accepted | A pin with no release (a failover, a converted move, a replay) now names its target first and selects the pin only once requireAcks holds. The phase stays pinning (ruling 4, amended), and the guard sits exactly where 1b-next's barrier stands. It is the new rule reloc-failover-ack-before-pin. Its mutation selects the pin first, as rev 4 did. It is an expected miss (a loss bound like reloc-failover-pin-delay). | Task 5C; ruling 4 | TestFailoverPinWaitsForTheAcknowledgement. The executor's newer manifest is in flight at its termination. The target is named, but its controller does not run, so for the delay plus 20 steps only a third box works. The test asserts no acknowledgement and no pin, then lands the manifest. Once the target acknowledges, the pin must name the newer manifest. | | R2 #2 (P2) | Correct. The two-box case drained before it terminated the former executor, so no executor failed. | accepted | Both shapes now terminate the current executor with DeleteOnTermination=false. With no operator acting, the host must reach serving on the region's other box (two-box) or on the group's replacement (one-box). The dead box's park-local must be open at that point and still open 200 steps later. The operator's destroyed-local declaration (finish) then closes it, and the test checks that it closed. | Task 5C | (coverage) the test fails if the fence discharges without evidence (fence-discharge-qualified is the witness) |

A model gap the new ordering exposed. Once the pin waited for the acknowledgement, two-box seed 29 failed. The order was:

1. A superseded generation's park-generation ran while the relocation still pinned that generation's manifest.
2. The files live set kept the manifest, which was correct.
3. Nothing parked it after the relocation completed, so INV-10 reported it as residue.

relocationLeftovers now queues a park-generation for the pinned manifest's generation when that generation is no longer the holder's. With the fix, every seed passes. (Corrected in rev 6, Astra round 3 finding 2.) This park is the model's abstraction, not a CompleteRelocation guarantee. 1b-next rev 19's completion queues only the local chores and the abandoned prepared generations. The obsolete manifest is the at-rest sweep's (claim §6.2a), and the pinner's retained control object is the storage follow-up's (1b-next ruling 21). The model parks it at once so INV-10 can check the residue at completion. It is not a 1b-next finding.

Dry run (2026-10-08). The scratch module was rebuilt from the baseline, with the identity tests and Task 1 from prose. The patches for Tasks 2 to 5B were applied from rev 4 of this document, then Task 5C and the regenerated Task 6. After each task: build, vet, gofmt, the gate, and the COUNTERS and both trace files compared byte for byte with the baseline's.

| After | One-box COUNTERS and traces | Two-box | Gate | |---|---|---|---| | Tasks 1 to 5B | identical (as in rev 4) | 447, 449, 464, 478, 480, 480, 487 | ok | | Task 5C | identical | 300, 0 failed, 486 | ok. Under its mutation, TestFailoverPinWaitsForTheAcknowledgement fails ("pinned before a target was named and acknowledged"). TestCrashAtEachOpenBoundary (4 stages × 2 shapes) and TestL18AdverseVolume (2 shapes) pass. | | Task 6 | the same | the same | ok. @regionha lists 48 rules, 156 in all. bash -n is clean. |

No mutation sweep was run, and the scratch module was then removed.

Rev 4: round 1 dispositions

Astra's round 1 on this plan (CODEX-PLAN-REGION-HA-TWO-BOX-R1.md, against 3c74454f) was "not ready", with one P1 and seven P2s. All eight are accepted; none is declined. Finding 1 is fixed in Task 1. Findings 2 to 8 are fixed in a new task, Task 5B, a patch on Task 5A's tree, and Task 6's patch is regenerated on top of it. Tasks 2 to 5A are unchanged, and their patches still apply.

| # | Evidence checked | Disposition | What changed | Where | Guard removed: the test that fails | |---|---|---|---|---|---| | 1 (P1) | The trace Astra describes was reproduced: a create's record persists, its box stops, and recovery runs past its 15-step wait. The baseline waits for the region's box. Rev 3's Task 1 cancelled the incarnation. Aggregate COUNTERS did not show it. | accepted | createExecutor is today's region-wide pick when perRegion == 1, and the recovered-create cancellation runs only in the two-box shape. Task 1 Step 1 adds onebox_identity_test.go, built from baseline APIs only, before any change. TestOneBoxCreateInterruptionTrace writes the whole trace of that interruption, once with the box restarted and once replaced. TestOneBoxSeedTraces writes a SHA-256 per one-box seed of its full trace, with map-ordered state masked. Every task compares both files byte for byte with the baseline's. | Task 1 (Steps 1, 4, 6); Global Constraints | rev 3's Task 1 code: TestOneBoxCreateInterruptionTrace differs at "recovery: cancelled create" | | 2 (P2) | admits and admitWriter had no stuck check, so an exhausted fence in starting left the live source admissible. | accepted | Both refuse while Op.Stuck is set, mirroring relocationAdmission. Rule reloc-stuck-refuses-admission. | Task 5B | TestStuckSourceRefusesAdmission | | 3 (P2) | chooseBoxExcept returned a region's only box unchecked. | accepted | The shortcut is the one-box shape's alone. With region HA on, a single candidate is checked for enrollment, key, executable, lost and park-local. Rule ha-sole-box-eligibility. | Task 5B | TestHASoleBoxIsCheckedLikeAnyOther (five refusals; the one-box shape keeps today's pick) | | 4 (P2) | The barrier read current leases (leasesSeen), and installed and probing had none. | accepted | Durable acknowledgements are opState.Acks (exec_ack.<box>). A participant whose controller is ready (lease current) journals its acknowledgement in role (recordAck). acked is requireAcks and gates starting→releasing, releasing→pinning, pinning→installing, installing→installed and installed→probing. Controller readiness stays the participant's own check. A controller now renews its lease on its own clock in the two-box step (renewController), not only when the worker happens to run. | Task 5B | TestReplacementWithoutAcknowledgementHoldsEachTransition | | 5 (P2) | The pin delay was skipped after a release, and the dead-target deadline ran from the termination. | accepted | The first worker to see a terminated box writes the fence record (box.FenceObservedAt). The fence CAS retains every observed_at in opState.Observed. The pin waits on the newest of them, release or not (rule reloc-pin-delay-every-fence). FenceTargetWithoutSpare's deadline runs from observed_at (rule reloc-deadline-from-observed-at). | Task 5B | TestPinWaitsForEveryFenceObservation; TestDeadTargetDeadlineFromObservation (observation delayed past the deadline) | | 6 (P2) | relocPhase accepted later phases, the matrix had no probe-failed, and it added spares first. | accepted | stepUntil advances one actor transition at a time and stops the moment its condition holds. TestL18TerminationAtEveryExactPhase stops exactly in each of the nine phases, probe-failed included, and asserts the phase and region 0's live-box count immediately before the termination. No spare is added; replacements come from the modelled group after the loss. It has 24 subtests over the one-box and two-box regions and the source and target roles, and replaces TestL18TerminationInEveryRelocationPhase. | Task 5B | (coverage) | | 7 (P2) | Five guards had no discriminating test. | accepted | A direct test for each, failing under its mutation. TestOnlyTheExecutorWritesP runs only the source at installing. TestInstallAppliesThePinnedManifest lands the newer manifest between pin and install. TestFailoverPinWaitsOutTheDelay and TestPinWaitsForEveryFenceObservation assert before the delay passes. TestReplacementWithoutAcknowledgementHoldsEachTransition covers the barrier. TestPinNeverShortOfTheRelease hides the release's newest file. | Task 5B | each fails under its rule's mutation (Step 2) | | 8 (P2) | Claim §11 lists eight additional witnesses for the executable model, and rev 3 had four. | accepted | Model events and witnesses for the missing four, with file objects and admission trimming modelled far enough to exercise R11-1 (below). The host-dependent tie-break is real SHA-256 over the host (tieHashFor, rule tie-hash-host, TestTieHashFollowsTheHost). | Task 5B; the evidence map below | witnesses below |

Claim §11's additional witnesses, each in this model now (claim rev 6.30 §11: "The additional witnesses are: …").

| Claim §11 text | Model evidence | Rule whose mutation it catches | |---|---|---| | "Relocation start racing purge or app-placement admission closure." | TestRelocationStartRacesPurge | (behaviour; ruling 4 of 1b-next) | | "Empty-database drain with files and timers." | TestEmptyDatabaseDrain | | | "Generation parking while relocation pins referenced files." | witness files-live-set; witness files-origins-referenced (wOriginsAfterTrim) | files-live-set, files-origins-referenced | | "Move landing, source cleanup, then target failure with an unchanged file." | witness files-objects-region-bound (wMoveUnchangedFile). The landing writes its generation's prepared manifest (moves §7.6, L17) in the target region. The unchanged file is uploaded there before it is named. The source region is cleaned, and the target's failover pins the object. | files-objects-region-bound | | "Automatic target loss racing the record commit CAS." | TestAutomaticTargetLossRacesRecordCommit covers both orders: the regional worker's automatic fence takes the operator's record-first path (declareTargetLost). Witness fence-converts-committed-landing (wCommittedLandingTargetLost) covers the after-commit order (finding F5). | fence-converts-committed-landing | | "A failed cleanup leaving a controller record that blocks executable updates." | witness reloc-clear-after-cleanup (wClearAfterCleanup). New model state: the controller record (execRecord), the scoped cleanup in finishParticipation, and executable updates refused while a record exists (updateExecutable, drawn in the two-box sweep). New oracle INV-29. | reloc-clear-after-cleanup | | "First released admission followed by an uncertified failed probe." | TestReleasedThenFailedProbe | reloc-released-coverage (witness) | | "Crash between prepared admission, marker publication and replication opening." | TestCrashAtEachOpenBoundary crashes the target exactly with P's session at the app start (launch environment held), with generation.json's PUT in flight (held), and with replication open, in both region shapes. | (coverage) |

Files objects (for R11-1 and the unchanged file). A files directory now names the object that holds its content (filesDir.Obj, ObjRegion). The generation that first holds the content writes the object create-only and acknowledges it before any manifest names it. An unchanged file keeps naming an older generation's object. A host from another region uploads its objects again first (region binding). The pin checks that the named object is current in this region's bucket under the holder's location. The files live set keeps every object a live manifest or a live files directory names. hasFilesIn and the sweep treat objects as files, never as database objects.

New findings (none contradicts the claim or moves; each is a gap the joint round must place):

• F4. Moves' parks archive region HA's files tree. A push parks its whole location before installing. The same is true of a landing's install park and a rollback's return park. None of them excludes the files live set, so a later failover cannot pin the host's files. The model keeps the live set in those three parks (rule files-live-set-moves-parks, witness wPushKeepsLiveFiles; plan ruling 21). Claim §6.2a's live set should bind moves' parks explicitly.
• F5. A landing committed by its record whose target is then terminated has no owner. The record forbids a rollback, the dead target can never release, and neither moves §7.10 nor 1b-next consumes a fence for a landing. The model converts it to a failover in the target's region (rule fence-converts-committed-landing; plan ruling 20). Before the commit, the automatic fence takes the operator's record-first rollback, as claim D2 makes automatic termination equivalent to a declared loss.
• F6 (model only). 1b-next's FenceSource after the source's release leaves the source op.exec on lost until PinAfterRelease, transiently. INV-27 now allows exactly that: a released executor (plan ruling 24).

Past findings, and where their evidence lives. Claim §11 asks for the cases above in the executable model. Separately, it requires "targeted tests against the real hostclaim, park, stopevidence, hostfiles and hostexec boundaries; model results do not replace those adapter tests." Each 1b-next finding the model cannot represent is therefore proven by a 1b-next stage A artifact, which this plan does not duplicate:

| Findings | What they are about | Proven by (1b-next rev 19) | |---|---|---| | R1-2 | the pin selected and journaled under the location lease; a lease lost before the CAS | Task 5 TestWorkerRefusesToJournalAPinAfterTheLeaseIsLost, TestWorkerDrivesADrain; Task 8b TestRelocationBuildStopsWhenAuthorityChanges | | R1-4, R2-4 | durable automatic-loss evidence (evidence_refs) across replacement and completion | Task 1 TestRelocationRetainsEveryFencedBoxAcrossCompletion, TestRelocationLossRetainsAFormerWritersSession | | R2-7 | discovery completion when a discharge completes the final local chore | Task 1 TestRelocationDischargeCompletesDiscoveryLikeARetirement | | R11-1 | origins from referenced objects after admission trimming | Task 5 TestPinKeepsAFileOriginTheAdmissionListTrimmed, and this model's witness files-origins-referenced | | R2-5, R3-2, R4-5, R5-4, R12-1, R13-1, R13-2, R14-2, R15-2, R18-1 | controller lifecycle: cleanup failures, lifetime locks, durable participation, removal during an ongoing operation | Task 7 TestRelocationControllerLifecycleProperties (200 seeds, invariants (a) to (i)) and its named tests. The model keeps only claim §11's case, a failed cleanup keeping the update-blocking record (witness reloc-clear-after-cleanup). | | R18-2 | host-dependent hash selection | Task 2 TestExecutorChooserHashesTheRecordsHostOnEqualLoads, and this model's TestTieHashFollowsTheHost | | R1-1, R3-1, R3-3, R4-N1 to N3, R6-1, R7-1, R8-2, R9-1, R10-1, R12-2, R14-3 | compilation, adapters, privileges, kernel descriptors, production wiring | the production-boundary tests each disposition names (Tasks 2, 3, 4, 7, 9a, 10) | | R5-3, R5-5 (added in rev 11, Astra round 8) | the HA-disabled reconcile; the env file's deletion in the release flush | 1b-next's own tests (Task 9a TestReconcileWithoutAFenceObserverIsTodays; Task 7 TestReleaseFlushFilesCarriesTheLastWakeStateAndEnv); the model has no step for either |

Dry run (2026-10-08). The scratch module was built from the baseline. The identity tests were added and the baseline's two trace files recorded. Task 1 was applied from its prose, and the patches for Tasks 2 to 6 from this document, one at a time. After each task: build, vet, gofmt, the gate, and both trace files compared byte for byte with the baseline's.

| After | One-box COUNTERS | One-box traces (interruption, 300 seed hashes) | Two-box | Gate | |---|---|---|---|---| | Task 1 | identical | identical | 300, 0 failed, 447 | ok | | Task 2 | identical | identical | 300, 0 failed, 449 | ok | | Task 3 | identical | identical | 300, 0 failed, 464 | ok | | Task 4 | identical | identical | 300, 0 failed, 478 | ok | | Task 5 | identical | identical | 300, 0 failed, 480 | ok | | Task 5A | identical | identical | 300, 0 failed, 480 | ok | | Task 5B | identical | identical | 300, 0 failed, 487 | ok. 28 region HA witnesses hold, hold under every proper subset, and violate their named failure. Each of the ten new direct tests fails under its rule's mutation. | | Task 6 | identical | identical | the same | ok. @regionha lists 47 rules, 155 in all. |

No mutation sweep was run, and the scratch module was then removed.

Rev 3: sync to 1b-next rev 19

Rev 2 reported three gaps in 1b-next rev 16 (F1 to F3). 1b-next fixed them in rev 17, tightened the fixes in rev 18 (Astra's round 17 found each only partly closed), and Astra accepted rev 19 as "stage A ready to build" (round 18 raised test gaps only). Rev 3 replaces the model's own stand-ins for F1 to F3 (rev 2's rulings 14, 16 and 17) with mirrors of 1b-next's fixes, turns the three finding tests into evidence that the gaps are closed, adds a mutation check that reopens each gap, and models the open request L21 as an explicit window. Everything is in one new task, Task 5A, a patch on Task 5's tree; Task 6's patch is regenerated on top of it (one more expected-outcomes.txt line). Tasks 1 to 5 are unchanged.

| Gap | 1b-next fix | Model rule (new) | Mutation reopens it | Evidence | |---|---|---|---|---| | F2 | ruling 25 as rev 18 amended it: when a writer was admitted and the pinned database is nonempty, the pinned manifest must carry a live instance.key (needKey, liveEntry); otherwise ErrFilesUnevidenced and stuck. No manifest at all is the same case. | files-pin-needs-key (selectPin, manifestHasKey) | pins the keyless files; the install mints a fresh key over the sealed rows | witness files-pin-needs-key (INV-4, the L21 window); TestFailoverBeforeTheFirstManifest (now: stuck, nothing installed) | | F1 | ruling 26: probe-failed with no eligible spare is stuck ReleaseDeadline after probe_failed_since, never sent to the source | reloc-no-spare-bound (relocProbeFailed) | waits for a spare for ever | witness reloc-no-spare-bound (INV-3); TestProbeFailedInATwoBoxRegion (now also: waits before the deadline, never names the source) | | F1 | rev 18 finding 2: a dead target with no spare is fenced into stuck ReleaseDeadline after its observed_at (FenceTargetWithoutSpare, sharing fenceTargetStuck with the exhausted fence) | reloc-dead-target-bound (replaceTarget, fenceTargetStuck) | the fence is never consumed and nothing moves | witness reloc-dead-target-bound (INV-3) | | F3 | ruling 27 and rev 18 finding 3: every unopened P is journaled in abandoned_prepared before it is replaced or dropped (abandonPrepared: install, the replacement table's nested branch, and here also the nested relocation after probe-failed and the operator's replay) and parked by the serving CAS | reloc-abandoned-prepared (abandonPrepared, opState.Abandoned, replacing rev 2's Built) | records nothing | TestAbandonedPreparedGenerationParked, now on both paths (installing, and rev 18's probe-failed before any admission); an expected miss, because the model's at-rest sweep, which ruling 27 keeps as the backstop, retires an unrecorded P before any invariant sees it |

L21, explicit. The witness files-pin-needs-key (wL21Window) scripts the open window: the cold admission's pre-start manifest copy lands without instance.key (§5.6 copies it before the app starts), the app mints the key after it starts, writes and replicates rows sealed with it, and the box is terminated before the publisher's manifest carrying the key lands. With the rule the failover is stuck and installs nothing; without it the keyless pin installs a fresh key over the sealed rows (INV-4). The window itself stays open (L21 is Paul's: the platform pre-provisions the key, or the replicator holds its first upload until the key's manifest lands). Recovery there is stuck by design and no operator replay accepts a keyless pin, so the sweep, which must converge, never terminates such an executor (ruling 17, rewritten).

Other effects. The files-live-set witness now names INV-3: with the chain's live manifest archived, the failover finds no keyed manifest and is stuck, where rev 2 showed the fresh key (INV-4). Ruling 25 turned that data loss into a stuck operation. fenceExhaustedTarget keeps its rule and now calls the shared fenceTargetStuck. The two-box sweep's summary is unchanged (300 seeds, 0 failed, 480 completed): the sweep never reaches the new refusals.

New gaps in 1b-next rev 19: none found. One observation for the round: F3's fix cannot be caught by any invariant in the model, because the at-rest sweep cleans up first. Its value is that the operation owns the cleanup, which the direct test checks.

Dry run (2026-10-08). The worktree's model at fbdad381 was copied into a scratch module, Task 1 was reapplied from its prose, and the rev 2 patches for Tasks 2 to 5 were applied from this document. Task 5A and the regenerated Task 6 were then applied, and the gate was run after each, niced, at default seeds:

| After | One-box | Two-box | Gate | |---|---|---|---| | Task 5 (rev 2) | 300, 0 failed, 483; COUNTERS byte-identical | 300, 0 failed, 480 | ok | | Task 5A | 300, 0 failed, 483; COUNTERS byte-identical | 300, 0 failed, 480 | ok. The 23 region HA witnesses hold, hold under every proper subset, and violate their named failure under their set. Each of the three finding tests fails under its mutation. | | Task 6 | the same | the same | ok. HOSTLIFE_LIST=1 mutate.sh 0 @regionha lists 37 rules, 145 in all. |

No mutation sweep was run. The scratch module was then removed.

Rev 2: sync to 1b-next rev 16

Rev 1 was written against 1b-next rev 1 and only its Task 1 was dry-run. Rev 2 maps 1b-next rev 16's guards and transitions into the model, makes every L18 case a scenario in a one-box and in a two-box region, and dry-runs every task: each task is now a patch made on a clean copy of the baseline (fbdad381's model, the commit this worktree branched from), applied in task order, built, vetted and gated after each, with the one-box COUNTERS line compared byte for byte every time. The patches below are those dry-run patches, verbatim. Rev 1's code for Tasks 2 to 5 did not converge as written (six two-box seeds failed at Task 2 alone); the defects it had are listed under "Rev 1 defects" below, and none survives in the patches.

What changed, by task.

| Task | Rev 2 change | 1b-next rev 16 source | |---|---|---| | 2 | The release deadline (ReleasingSince, FailedAt): a release not journaled releaseDeadline after releasing or probe-failed began marks the operation stuck. Rule reloc-release-deadline. | ruling 14, Worker.releaseOverdue | | 2 | The acknowledgement barrier on releasing to pinning, beside the ones on starting and installing. Rule reloc-ack-before-pinning. | rev 4 N6, PinAfterRelease | | 2 | The pin is selected against an observation and journaled only against that claim version (pinEntry.ClaimVer); it names the generation it reads, chosen as genselect would over the admitted chain (pinSource), not holder.generation's listing alone. Rule reloc-pin-claim-gen. | ruling 16, RecoveryPinKey, JournalPin | | 2 | An empty listing pins only with evidence: a release flushed at 0, or a holder that never admitted a writer; otherwise stuck for the operator. Rule reloc-pin-evidenced-empty. | ruling 15, R1-13 | | 2 | prepared_opened journaled by the admission that opens P (opState.PreparedOpened, set in admitCommit) and read before holder.admissions. Rule reloc-prepared-opened-journal. | rev 12 S1, PreparedOpened | | 2 | EnsureLocal: before P's first admission the local install is verified before the probing CAS and before every attempt, and restored under the same install_stamp when a lost controller lease's scoped cleanup retired it (scopedCleanup, called from role). Rule reloc-ensure-local. | rev 15 finding 2, Effects.EnsureLocal | | 2 | VerifyReceipt: after P opens, the box's durable install journal (box.receipt) must be the journaled receipt; a missing or different one marks the operation stuck before any further admission, and nothing is compared against content. Rule reloc-verify-receipt. | rev 16 finding 1, Effects.VerifyReceipt | | 2 | Three probe attempts, each counted in the claim before it is made (opState.Attempts, reset per executor); the fourth is probe-failed. Rule reloc-probe-attempts. | ruling 19, BeginProbeAttempt | | 2 | A host that never admitted a writer is never drained (failover only); a box-started drain needs the app's admission registration open. Rule reloc-drain-needs-writer. | rulings 4 and 11, Worker.Start | | 2 | Exhaustion is checked before a spare is looked for, in probe-failed as at a fence. MarkStuck refuses between installed and a probe while P is unopened. | R1-16, MarkStuck | | 3 | The exhausted-target fence is phase-sensitive: while the live source is op.exec (starting, releasing) the fence records stuck and changes nothing else; otherwise op.exec none at pinning, the receipt and release dropped, P kept when unopened. Rule reloc-exhausted-fence. | ruling 23 as rev 9 amended it, FenceExhaustedTarget | | 3 | A replacement target never owes a park-local for the host, checked by the chooser and again inside the CAS (nameReplacement). Rule reloc-replace-not-owing. | rev 6 finding 1, replaceTargetSlot, LocalChoreBoxes | | 3 | The fence passes the dead box's regional chores (obligation.Owner == "box:<b>") to its region in the same CAS. Rule fence-reassigns-regional. | rev 6 finding 2, fenceBox | | 3 | A stuck operation consumes no fence (Worker.Step returns first); the operator's resolve declares a dead executor lost. A target with no spare is fenced on a later pass, not emptied. | Worker.Step, Worker.next | | 4 | P's prepared files manifest is written create-only at sequence 0 before anything of the database, and the session publisher of every generation starts at 1. Rule files-prepared-seq-zero; new oracle INV-28. | rev 15 finding 1 (claim R18-1, moves rev 7.22 §7.6), CopyPinnedManifest, PreparedAuthority | | 4 | The files live set keeps the chain's newest landed manifest (the "unchanged file" that rev 12 finding 1 traced through ten generations), not only holder.generation's; the files pin walks genParent, which no trim shortens. Rule files-live-set widened. | rev 12 finding 1, referencedOrigins | | 4 | The pin reads the manifest by exact version id; the model's versioned bucket stands for the pinner's retained copy (ruling 21), and the files live set keeps that version from every park. No separate rule (see "Mapped without a rule"). | ruling 21 | | 4 | A dead box's files directory is never read in the two-box shape (deadBoxFiles): the files come from the pinned manifest alone. | §5.6, HA5 | | 5 | Every L18 case runs in a one-box region and a two-box region (regionWorld, bothShapes, a per-region minimum for the one-box region). 20 witnesses (18 alone, 2 in stated combinations), 30 direct tests, three findings. | L18, claim §11 | | 6 | mutate.sh tags every verdict with the shape, accepts @regionha for the 33 region HA rules (one mutation check per guard), and lists without running under HOSTLIFE_LIST=1. | evidence policy | | 7 | The brief maps all 33 rules to 1b-next rev 16 functions and asks the joint round about the three findings. | Task 11 |

Mapped without a rule (the model already has the property, or has no actor that could break it): the retained manifest bytes (ruling 21; the versioned bucket's exact-version read, and the files live set); released coverage's predecessor check against the last admission, which the trim never removes (rev 12's "no other authority"); the D4 retention (evidence_refs, R5), which is the console's materialization and outside the model; the stage B gates R1 to R10 (6b and moves Plan 1 integration), which no model step represents.

Rev 1 defects the dry run found (fixed in the patches; each was a model bug, not a spec finding):

1. The probing check b.Files.Gen != op.Prepared read every later attempt's re-tagged files directory as a lost install and marked healthy relocations stuck; rev 2 checks the receipt instead (VerifyReceipt), as 1b-next rev 16 does.
2. A failed target whose install was retired released with no files and its successor minted a fresh instance.key (INV-4); the pin now carries the files set it was taken with, and a release never invents one.
3. The pin read holder.generation's listing alone, so a cold admission whose first upload had not landed pinned an empty set over a predecessor that held data; pinSource selects as genselect does over the chain.
4. The stat admissions covered: released was counted twice (in admitWriter and admitCommit); only admitCommit counts it.
5. adoptionOwner took a region's last remaining box as the owner after the other was terminated; in the two-box shape ownership needs proof whatever the count.
6. Termination of a participant of a move, push, create or delete left that operation with no recovery owner (they are moves' and the claim's declare-lost paths); plan ruling 15 scopes termination.
7. hasFilesIn counted a files manifest as a database object, so the recovery walk chose a generation holding only a manifest as a baseline.
8. TestReleaseWaitsForEscapedDescendant assumed a stray survives the stop; under evidence-whole-tree the cleanup kills it, so the test now shows that (TestReleaseStopsAnEscapedDescendant).
9. Five rev 1 witnesses could not violate as written (reloc-release-first, reloc-exec-only-installs, reloc-start-guard, reloc-row-cases, files-live-set): two now force their interleaving, two are expected misses with direct tests, and reloc-row-cases needs only exec-admission and exec-writer and names INV-6.

Findings for the joint round (the model shows each; none is a model bug; the model's handling is a ruling the round should confirm or replace):

• F1. A drain's failed probe has no exit in a two-box region. replaceTargetSlot refuses the source and Worker.Step in probe-failed waits for a spare with no bound ("no eligible box yet: a later pass may find one"). With two boxes the host serves nowhere until an operator acts, and nothing marks the operation stuck. The model marks it stuck after releaseDeadline and the operator's resolve may name the source again (plan rulings 13, 14; TestProbeFailedInATwoBoxRegion).
• F2. A failover before the host's first files manifest lands loses its instance.key. StorePinner pins "Empty for a host that never published files", so the install mints a fresh key over data sealed with the old one (INV-4 in the model, TestFailoverBeforeTheFirstManifest). An adopted legacy host whose platform files were never published, or a new host inside the publisher's first second, is exposed. The sweep never terminates such an executor (plan ruling 17).
• F3. An abandoned prepared generation is never retired by the operation. A replacement at installing, an exhausted fence or a nested pinning leaves P's remote build in holder.location; CompleteRelocation queues park-local chores only, so only the at-rest sweep can reach P's objects, and the claim's INV-10 at the operation's end finds them. The model parks every unopened P in the serving CAS (plan ruling 16, TestAbandonedPreparedGenerationParked).

Conflicts between 1b-next rev 16 and the claim or moves model rules. None of the claim's or moves' rules had to change: every new behaviour is a new rule or a branch that only a relocation or the two-box shape reaches, and the one-box COUNTERS line is byte-identical after every task. F1 to F3 are gaps in 1b-next, not contradictions of the claim. One reading to confirm: claim §4's phase table lets the source admit in starting and releasing; the model admits it there only while its admission fence is open (its row ready), as 1b-next's request R1 asks 6b to do.

Dry run (2026-10-08, scratch module at $TMPDIR/twobox/mod, the worktree's internal/sim/hostlife at 99a3defe copied in, nice -n 19, default 300 seeds, GOCACHE=$TMPDIR/gocache where the default was refused):

| After | One-box summary | One-box COUNTERS | Two-box summary | Gate | |---|---|---|---|---| | baseline | 300 seeds, 0 failed, 483 completed | recorded | | ok | | Task 1 | 300, 0 failed, 483 | identical | 300, 0 failed, 447 | ok | | Task 2 | 300, 0 failed, 483 | identical | 300, 0 failed, 449 | ok | | Task 3 | 300, 0 failed, 483 | identical | 300, 0 failed, 464 | ok | | Task 4 | 300, 0 failed, 483 | identical | 300, 0 failed, 478 | ok | | Task 5 | 300, 0 failed, 483 | identical | 300, 0 failed, 480 | ok; 20 region HA witnesses hold, hold under every proper subset, and violate their named failure under their set | | Task 6 | 300, 0 failed, 483 | identical | 300, 0 failed, 480 | ok; bash -n mutate.sh; HOSTLIFE_LIST=1 mutate.sh 0 @regionha lists 33 rules |

The two-box sweep at Task 6 starts 15 drains and 4 failovers and completes 17 relocations, writes 192 fences over 1,130 terminations, takes 12 released admissions, retires 54 unopened local installs through the scoped cleanup, resolves 10 stuck operations by the operator, and parks 12 abandoned prepared generations. No mutation sweep was run: the revision's one 3,000-seed sweep is Task 6 Step 3's. The scratch module was removed afterwards; only this document is committed.

Rulings made while planning

Each was a gap or a conflict between the authorities. Each says what it costs if it is wrong. Rulings 1 to 11 are rev 1's; 12 is amended; 13 to 19 are rev 2's; 20 to 25 are rev 4's, and rev 4 amends 1 and 15; revs 5, 6 and 7 amend 4.

1. The one-box shape is a different random stream only where the two-box shape draws more. Every seed of the one-box sweep must stay byte-identical to the baseline (spec §4: "a region with one box behaves exactly as today"). So a two-box world draws its extra values only after the one-box draws of the same step (newWorld adds its second boxes last; step draws for termination, drains and the publisher only when perRegion > 1), and no one-box code path calls the random source where it did not before. The gate proves it: every task compares the one-box COUNTERS line to the baseline's and, from rev 4, the whole trace of a one-box create's interruption and a hash of every one-box seed's trace (Task 1 Step 1). Rev 3's Task 1 passed the COUNTERS check while it cancelled an interrupted one-box create; region HA's create behaviour (the recovered-create cancellation, the eligibility of a sole box) is the two-box shape's alone. Cost if wrong: a seed reshuffle, which the gate shows at once; the fix is to move the draw.
2. The two-box sweep is the revision's one 3,000-seed sweep. The evidence policy (moves §14.2, Paul 2026-10-06) allows one mutation sweep per revision. The one-box path is byte-identical at the gate's 300 seeds, so the one-box verdicts of rev 7.22 stand for it; the new guards are reachable only with two boxes, so the sweep runs with HOSTLIFE_BOXES=2. One caveat the brief states: Task 2 replaces the body of relocate, which the one-box shape reaches only through a converted move (fence-converts-moving); the 300-seed one-box sweep never converts, so its COUNTERS line cannot show a change there, and the fence-converts-moving witness is the evidence that the converted path still completes. Cost if wrong: a one-box regression in a guard this plan touches would show first in the gate's 300-seed one-box run, which every task runs.
3. A regional worker is any live, enrolled, non-lost box of the region. Claim P6-D5 and spec §2 say correctness never depends on which worker acts; two make the same CAS and one fails. The model lets every such box run the region's chores and the relocation's worker steps. The one-box path is unchanged, since the region's one box was the only candidate. Cost if wrong: a chore run by two boxes at once that the park's idempotent copies and single manifest did not make safe; the sweep would show it as INV-10 or non-convergence, which is a finding for the claim, not a model bug.
4. Failover starts at pinning with the target named there. For an initial failover the D6 barrier is checked before the pin is selected (rev 5, narrowed in rev 6); for every relocation it is checked again at the installing CAS. Spec §5.8 and 1b-next's StartRelocation name the target in the failover's start CAS and pass through starting for its acknowledgement (PinFailover). The model's converted move already enters at pinning with no target (moves §7.10), so one entry point serves both, and to's execution lease must be current before installing (requireAcks in ToInstalling). A drain whose source is lost in starting goes to pinning at once for the same reason (1b-next keeps it in starting until PinFailover). (Rev 5, Astra round 2 finding 1.) Rev 4's collapse did move a guard: the pin was selected before any acknowledgement, where PinFailover waits for them all. (Rev 6, Astra round 3 finding 1.) Only an initial failover waits. opState.PinFailover stands for 1b-next's starting after StartRelocation with a fence: startFailover sets it, and so does a drain whose source is lost in starting. While it is set, the operation in pinning names its target, waits for requireAcks, and clears it in the PinFailover CAS before any pin is selected (rule reloc-failover-ack-before-pin). A converted move, a nested failover and an operator's replay enter pinning directly, as in 1b-next. There Worker.pinning journals the pin first and checks the acknowledgements only for ToInstalling. That is the same barrier at the same point in the order of events; only the phase's name differs. (Rev 7, Astra round 4.) The serving executor's failover now starts the way Worker.Start and StartRelocation start it: with an eligible target named, the admission registered and rechecked, and RelocationStartGuard passed, the fenced source excepted. The flag is that failover's starting, and relocPhaseName names it so. On every path a relocation at pinning with no target names one before it selects a pin (rule reloc-name-before-pin), as Worker.pinning does. Cost if wrong: a phase the brief says is collapsed. The guards are 1b-next's, in its order.
5. released coverage is modelled as the claim defines it, and relocation by drain is enabled in the model. Spec §5.8 says a drain is not enabled until L9 is accepted; claim rev 6.30 §6.4a carries L9. The model implements it so the review can judge it, and the brief says so. Cost if wrong: the drain scenarios are evidence for L9, not against anything.
6. stuck is a journal entry; the operator resolves it (plan ruling 13 says how). 1b-next ruling 9: stuck is not a phase. Cost if wrong: the operator's act is one function.
7. Terminated is not stopped. The model's Destroyed box may come back with its disk in the final heal (a stopped instance started again). Termination is new, permanent and observable: a Terminated box never returns, and only a terminated, enrolled box is fenced (H1, H10, H19). A stopped box stays the operator's declare-lost (claim D2), as today. Cost if wrong: none to the one-box path, which never terminates.
8. Liveness, loss, determinism and defence-in-depth guards are missed with their reasons in expected-outcomes.txt, each with a direct test that shows its effect. A mutation check needs an invariant violation, and spec §5.8 says itself that the pin delay "is a loss bound, not a safety bound". Cost if wrong: a later revision finds an invariant for one and the entry becomes STALE, which the harness reports.
9. The stale edges file is the former executor's row. The model has no edge or home map. Spec §5.4 publishes a host as home only from a ready row on its executor, and the model's edge "routes on the row" (wake). So a stale edges file is a row the former executor still holds after op.exec moved, and the hazard is a wake reaching it. HA4's stamp resolution is plan 1a's unit-tested code, not modelled. Cost if wrong: the brief names it as the one HA4 gap.
10. Volume evidence is one flag per box, and it counts only for a terminated box (rev 10: a stopped box keeps its disk, so its park-local stays owed whatever the flag says; claim §7.3 D5). H19 and §5.9: the fence never reads it; only automatic discharge of the dead box's park-local chores does. The model draws DeleteOnTermination per box and the discharge rule reads it in the fence CAS; the recorder, the two-hour bound and removed_volumes are plan 1b's unit tests, and 1b-next ruling 3 keeps production discharge off until the roster records an enrollment time. Cost if wrong: the adverse-volume case still proves what claim §11 asks: recovery proceeds and the chores stay open.
11. The files publisher exists where region HA is enabled, which the model ties to the two-box shape. Spec §5.6 is region HA's; the one-box model has no publisher and carries files at the cut (StopFiles), and a converted move keeps that stand-in. In the two-box shape the executor publishes a manifest whenever its files or wake state change, whether or not the app runs, and a dead box's disk is never read (deadBoxFiles). Cost if wrong: a one-box drain would also want it; the one-box shape has no drain.
12. The review findings are on the branch now (amended in rev 2). CODEX-PLAN-REGION-HA-1BN-R1.md to R16.md sit beside 1b-next rev 16. The hazards the model must catch were taken from them and from the dispositions tables of revs 2 to 16; the "What changed, by task" table above names the finding each rule answers, and Task 7's table carries a column for it. Findings about stage B integration with claim 6b and moves Plans 1 and 2 (R1 to R10, the lifecycle property of rev 14 to 16) have no model step and are listed as such.
13. The operator's resolve (carlos ops host resolve) has three cases (rev 9 adds a fourth, narrowed in rev 10: a live target in probe-failed whose release is unrecoverable is stopped by the operator, and the next resolve declares it lost and replays. Unrecoverable means no flush recorded for the stop, and the session's replicator or the box's files gone. Every other live target is resumed. The stopped box's local cleanup stays owed). The spec names the command and leaves its effect open. Nothing moves away from a live box without its stop evidence: a live source still op.exec in starting or releasing with no release journaled is returned to serving (the relocation is abandoned); a live target op.exec without a release is sent to probe-failed, where it runs its release; otherwise (op.exec none, released or lost, a dead executor first declared lost as claim D2's operator path does) the operation is replayed from pinning with the replacement count reset, the exclusions cleared, the source eligible again, and an empty listing accepted (Resolved); never a keyless files pin for a nonempty database (rev 3, ruling 17). Cost if wrong: one function in console_test.go; the guards are unchanged.
14. (Rev 3) probe-failed or a dead target with no spare is stuck after releaseDeadline, mirroring 1b-next ruling 26 and rev 18 finding 2 (finding F1, closed). In probe-failed with no eligible spare, the operation is stuck releaseDeadline after probe_failed_since (rule reloc-no-spare-bound). A dead target with no spare is fenced into stuck releaseDeadline after its termination, with the fence consumed (rule reloc-dead-target-bound, fenceTargetStuck). Neither ever names the source. Only the operator's resolve may, by plan ruling 13. Rev 2's version of this ruling was the model's own stand-in with no guard. Cost if wrong: in a two-box region a failed drain waits for the deadline and then for an operator, rather than returning to the source automatically, as 1b-next ruling 26 accepts.
15. Termination is drawn only where region HA owns the loss. The sweep terminates a box only when the claim names it, if at all, as a serving executor, a relocation's participant or a chore's owner, and never a box holding a legacy host before its adoption. A participant of a move, landing, rollback, revert, push, create or delete is recovered from a lost box by moves' and the claim's declare-lost paths (L14), which the model walks for a stopped box, and a push never starts on a terminated executor. Cost if wrong: those paths are untested under termination here; the brief lists it under "After this plan". (Rev 4) One exception, from claim §11's "automatic target loss racing the record commit CAS": a landing's or a rollback's target that is terminated is fenced by the regional worker as claim D2 makes automatic termination equivalent to a declared loss, by the operator's own record-first path (declareTargetLost), and a landing already committed by its record converts to a failover (ruling 20). The sweep still never draws such a termination; TestAutomaticTargetLossRacesRecordCommit and the witness fence-converts-committed-landing script it.
16. (Rev 3) Every unopened P is recorded when it is replaced or dropped, and parked at completion, mirroring 1b-next ruling 27 and rev 18 finding 3 (finding F3, closed). abandonPrepared journals it in opState.Abandoned (abandoned_prepared) on every path: install, the replacement table's nested branch, the nested relocation after probe-failed, and the operator's replay. The serving CAS queues a scoped park-generation for each one in the source region (rule reloc-abandoned-prepared). An opened P is part of the writer lineage and is never listed. This replaces rev 2's list of every built P. Cost if wrong: the model's at-rest sweep is the backstop, as it is in 1b-next. That is why the rule's mutation is an expected miss, shown by a direct test.
17. (Rev 3) A nonempty database pins only files that carry instance.key, mirroring 1b-next ruling 25 as rev 18 amended it, and the L21 window fails safe (finding F2, closed). In the two-box shape, a pin for a holder with an admitted writer and a nonempty pinned database needs a pinned manifest that carries a live instance.key. With no manifest, or a keyless one (the pre-start copy of §5.6), the operation is stuck (rule files-pin-needs-key), and no operator replay accepts a keyless pin. The window between the app minting the key and the first keyed manifest landing is L21, still open. A host terminated inside it cannot be recovered by any relocation, so the sweep, which must converge, never terminates such an executor (regionHAOwnsLoss). The witness files-pin-needs-key and TestFailoverBeforeTheFirstManifest script the window. Cost if wrong: the sweep never meets the L21 refusal; the witness and the test do, and they fail if the refusal goes.
18. A one-box region inside the two-box shape is a witness world's (regionWorld(1), oneBoxRegion): region HA on, region 0 kept at one box by its group (H5's minimum is per region), regions 1 and 2 with two. The sweep's one-box shape has region HA off, so L18's one-box cases are direct tests, not seeds. Cost if wrong: a one-box-region interleaving the scenarios do not script is unexplored; the joint round may ask for a mixed sweep shape.
19. INV-28 is new: a timer is never declared lost while the manifest its box published last in that generation carries it. It is the oracle for P's prepared manifest at sequence 0 (the seq order must be the publication order); it reads the issue order the model records in each manifest blob. Cost if wrong: a manifest landing out of order with a timer added and then removed would be a false positive; the timer would be delivered, and delivered timers are never declared.
20. (Rev 4) A landing committed by its record whose target is then terminated converts to a failover in the target's region (finding F5; rule fence-converts-committed-landing). The record forbids moves' rollback, and the dead target can never release, so without the conversion the host has no recovery owner. The conversion enters at pinning like moves' §7.10 conversion of a move, with the source region's chores left to the region and the landing's prepared manifest as the files pin. Cost if wrong: moves or 1b-next may prefer another owner; the model's guard is one branch in fence.
21. (Rev 4) Moves' parks keep region HA's files live set (finding F4; rule files-live-set-moves-parks). A push's park, a landing's install park and a rollback's return park park the whole location today, which archives the objects a later failover pins. The model passes the live set to all three as it does to park-generation. Cost if wrong: claim §6.2a may bind the live set to a different step; the witness shows the loss either way.
22. (Rev 4) A controller renews its own execution lease. 1b-next's controller is a long-running process; in rev 3 the model renewed a lease only when the box's worker ran a role, which let a calm box's lease lapse and churned durable acknowledgements. renewController runs per box in the two-box step and draws nothing. Cost if wrong: none to safety; acknowledgements are still journaled only while the lease is current.
23. (Rev 4) The injected app failure never applies to a relocation's own source, and the operator's replay keeps a failed target excluded. The source has just run the app; a probe on it failing at random made a ping-pong between two failing boxes that no protocol produces. The replay's exclusion is plan ruling 13's, now kept for the target that failed. Cost if wrong: a source whose app genuinely fails is not modelled; the operator's resolve is its path.
24. (Rev 4) INV-27 allows a released executor that has been fenced (F6, model only). 1b-next's FenceSource after the source's release leaves op.exec on the lost box until PinAfterRelease; nothing runs there. Cost if wrong: a write from a lost, released executor would go unseen by INV-27; INV-1 and INV-2 still see it.
25. (Rev 4) Files are objects, referenced by manifests and files directories (R11-1; rules files-origins-referenced, files-objects-region-bound). Rev 3 carried files as manifest content, so trimming an admission could not drop an origin. Rev 4 models the object key, its creation before it is named, its region, the live set over referenced objects and origins taken from references, never from admissions. Cost if wrong: the object store's semantics beyond create-once and region are not modelled; hostfiles' adapter tests own them (claim §11).

Global Constraints

• One-box byte-identical. After every task: nice -n 19 go test ./internal/sim/hostlife/ -run '^TestHostLifecycle$' -count=1 -v | grep COUNTERS equals the baseline's line (Task 1 Step 1 records it at $TMPDIR/twobox/baseline-counters.json; the task that breaks it stops and moves its draw). (Rev 4) And both one-box traces equal the baseline's byte for byte: HOSTLIFE_TRACE_OUT=$TMPDIR/twobox/trace.txt HOSTLIFE_TRACE_OUT_SEEDS=$TMPDIR/twobox/seeds.txt nice -n 19 go test ./internal/sim/hostlife/ -run '^TestOneBox' -count=1, then cmp each with baseline-trace.txt and baseline-seeds.txt. COUNTERS alone missed rev 3's one-box change (Astra round 1 finding 1).
• Additive. Moves and the claim own guards in this model. No existing rule's semantics change; existing functions gain branches or calls that only a relocation, a termination or the two-box shape reaches. New code lives in new files (twobox_test.go, regionha_test.go, regionha_witness_test.go, regionha_cases_test.go) except where a hook must sit in an existing function.
• Every rule is a named guard: an entry in allRules, in the region HA block, with a comment naming the spec section and the 1b-next rev 16 function it mirrors, on("<rule>") at exactly the decision the rule governs, and either a witness in witness_test.go or an expected-outcomes.txt line with its reason and the direct test that shows its effect.
• Witness discipline (moves §14.2, rev 7.3): a witness holds with every rule on, holds under every proper subset of its mutation set, and violates its named failure under the whole set. TestWitnesses checks all three in the gate. Liveness and preference guards get direct tests (TestXxx), never witnesses.
• The patches are the dry run's. Each task's code is one patch made against the previous task's tree. Apply it from the worktree root with git apply; if it does not apply cleanly, the tree is not the previous task's: stop and say so, never hand-merge.
• CPU budget (hard; shared machine). The gate (300 one-box seeds, 300 two-box seeds, the witnesses, the direct tests; about 4 seconds) runs niced after every task: nice -n 19 go test ./internal/sim/hostlife/ -count=1. One mutation sweep per revision: 3,000 seeds, serial, nice -n 19, HOSTLIFE_PAR=2, never beside another sweep or a baseline (Task 6 Step 3). Deep runs of 30,000 seeds or more only on Paul's explicit say-so, never in this plan. No sweep during Tasks 1 to 5.
• Go environment. GOFLAGS=-buildvcs=false. Leave GOCACHE at its default; the sandbox refused it intermittently during the rev 2 dry run (open /home/paulca/.cache/go-build/...: read-only file system), in which case GOCACHE=$TMPDIR/gocache for that command. Scratch under $TMPDIR/twobox/, removed at the end of Task 7.
• Exact values. failoverPinDelay = 2 steps (§5.8's 30 seconds; one step is about 20 seconds, since sigAgeH = 45 steps is the 15-minute signature age); probeDeadline = 3*probeStartWindow + 10 (three attempts' windows); releaseDeadline = probeDeadline (1b-next's 10 minutes, the same as its probe deadline); maxReplacements = 2; probeTries = 3 attempts per executor; enrollDelay = 20 steps (automatic enrollment, H16); replaceDelay = 30 steps (the group's replacement launch); second boxes have ids nRegions + r; manifests live at dataKey(loc, gen, "files/m-<seq>"), P's prepared manifest at seq 0.
• Commit messages: lowercase sim: prefix and a sentence stating the behaviour, a blank line, then Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>. Branch region-ha-hostlife-two-box (this worktree). No push; merging is Paul's call after the joint round.
• Gate before each commit: gofmt -l internal/sim/hostlife/ empty; go vet ./internal/sim/hostlife/; the gate above; the one-box COUNTERS and trace comparisons.

Review Focus

1. A pin selected against an older claim. A pinner that observed the first round and stalled must not journal its selection after a nested reset: the CAS binds the claim version (1b-next ruling 16). Expect the stale selection refused. Task 5, witness reloc-pin-claim-gen.
2. The receipt after P opens. A box whose install journal is gone after P's first admission must stop the operation, never admit again over a missing install, and never compare content the admitted writers changed. Expect stuck, then the operator's resolve. Task 2 verifyReceipt; Task 5 witness reloc-verify-receipt.
3. The exhausted fence while the source still executes. Three targets die in starting; the source must keep op.exec, its phase and its release, and only stuck is new. Expect no second writer. Task 3 fenceExhaustedTarget; Task 5 witness reloc-exhausted-fence.
4. P's prepared manifest sequence. The session publisher in P must sort after the prepared manifest, or a later pin takes stale files and timers. Expect seq 0 and INV-28 to hold. Task 4 buildPreparedFiles; Task 5 witness files-prepared-seq-zero.
5. The three findings, closed (rev 3). F1, F2 and F3 are now mirrors of 1b-next rev 19's fixes, each with a mutation that reopens it. The L21 window is scripted (witness files-pin-needs-key): recovery must be stuck there and must never install a database without its key. Tell us if a mirror is weaker than its 1b-next guard.
6. (Rev 4) The one-box shape's create, and Astra round 1's guards. The trace comparison must show no one-box change after any task; the five guards round 1 named must each have a test that fails without them. Task 1 Step 1 and Step 6; Task 5B Step 2.

File Structure

| Path | Responsibility | Task | |---|---|---| | internal/sim/hostlife/twobox_test.go | The shape (boxesPerRegion, regionBoxes, addBox), placement (chooseBox, chooseBoxExcept, tieHash, hostsOn), adoption's owner, regional ownership of chores (box:<b> owners included) | 1, 2, 3, 5 | | internal/sim/hostlife/world_test.go | Additive fields: perRegion, issued, oneBoxRegion, NewBox; on box Terminated, Enrolled, EnrollAt, DeleteOnTermination, installEpoch, receipt, attemptTag, the publisher's pubGen, pubSeq, published, releaseSeq; the relocation journal on opState (RelocReason, FenceAt, FailedAt, Release, Pin, Prepared, InstallStamp, Receipt, ProbingSince, Replacements, Excluded, InstalledOn, Discharged, Stuck, ReleasingSince, Attempts, PreparedOpened, Resolved, Built); releaseEntry, pinEntry, receiptEntry; obligation.Owner; liteHost.Box; clone | 1 to 5 | | internal/sim/hostlife/sim_test.go | newWorld's second boxes, terminate fault and volume flags, sweep, TestHostLifecycleTwoBox, the two-box step in step, heal (a terminated box never returns), INV-27 in checkStep, the files live set in residueOf | 1 to 4 | | internal/sim/hostlife/regionha_test.go | The relocation phases (relocStarting to relocSettle), the release sequence and its deadline, pinSource, selectPin, restoreUpTo, handExec, localInstall, ensureLocal, verifyReceipt, preparedOpened, scopedCleanup, nameReplacement, markStuck, relocationLeftovers; termination, launches, enrollment, the fence worker, fenceBox, failover, source loss, the replacement table, fenceExhaustedTarget, regionHAOwnsLoss, deadBoxFiles; the files publisher, buildPreparedFiles, newestManifest, lastLandedManifest, filesLive, pinnedManifest, timerCarried; regionMin | 2 to 5 | | internal/sim/hostlife/regionha_witness_test.go | twoBoxWitness, the Task 2 to 4 direct tests, the scenario helpers (regionWorld, bothShapes, drainTo, relocPhase, servingOn, published, spareID) and the witness functions | 2 to 5 | | internal/sim/hostlife/regionha_cases_test.go | Every L18 case in a one-box and a two-box region, claim §11's extras, the direct evidence for every bound, the findings' reproductions | 5 | | internal/sim/hostlife/witness_test.go | The witnesses entries for the region HA rules (mutate.sh reads this file); newWitness sets perRegion: 1 and enrolls its boxes; tick runs the two-box step | 1, 2, 5 | | internal/sim/hostlife/console_test.go | createSteps and recoveryPass use the recorded executor; moveTo chooses; h2Box; the operator's resolve of a stuck relocation; no push on a terminated executor | 1, 2, 3, 5 | | internal/sim/hostlife/background_test.go | adopt uses adoptionOwner; replaceDestroyed fills to the region's minimum; reconcileClaimed's relocation row case | 1, 2, 5 | | internal/sim/hostlife/moves_test.go | workerMode uses ownsObligation and runs the fence step first; role's scoped cleanup on a lost lease; relocate dispatches the phases; convertToRelocating sets the failover fields; release queues the leftovers; genOf and deadGeneration know manifests and the files live set | 1 to 4 | | internal/sim/hostlife/protocol_test.go | admits for the new phases; admitWriter's released coverage; admitCommit journals prepared_opened; installGen for P; appStart's FailApp for relocation probes; localPark drops the install journal; hasFilesIn skips manifests; doObligation's park-generation keep for the files live set | 2, 4, 5 | | internal/sim/hostlife/rules_test.go | The 47 region HA rules, in one block at the end | 1 to 5B | | internal/sim/hostlife/onebox_identity_test.go | (Rev 4) The one-box create-interruption trace and the per-seed trace hashes, compared with the baseline's after every task | 1 | | internal/sim/hostlife/regionha_round1_test.go | (Rev 4) Astra round 1's direct tests: one per guard it named, the forced open boundaries, the record-commit race, the host tie-break | 5B | | internal/sim/hostlife/expected-outcomes.txt | The missed entries, each with its reason and its direct test | 6 | | internal/sim/hostlife/mutate.sh | The shape tag on every verdict, @regionha, HOSTLIFE_LIST | 6 | | docs/superpowers/plans/CODEX-REVIEW-BRIEF-TWO-BOX-R1.md | The joint-round brief | 7 |

Baseline (recorded 2026-10-07, worktree region-ha-two-box at fbdad381, origin/design-moves-any-region; rechecked 2026-10-08 at 99a3defe)

$ GOFLAGS=-buildvcs=false GOCACHE=$TMPDIR/gocache nice -n 19 go test ./internal/sim/hostlife/ -count=1 -v
    sim_test.go:934: 300 seeds, 0 failed, 483 completed operations; mutated=""
PASS
ok  	github.com/carlosframework/platform/internal/sim/hostlife	1.830s

Nine tests pass (TestReadinessBudget, TestHostLifecycle, TestWitnesses, TestLegacyLostTargetReturn, TestForeignManifestReplayRefused, TestStagingSurvivesLegacyPark, TestJoinHolderlessSweep, TestInterruptedCleanReturn, TestProbeWindow). The COUNTERS line begins {"abandoned empty generation skipped":1,"abort":106,"admission: no predecessor writer, nothing declared":78,... and ends ..."writes_lost: the legacy identity (session 0)":30}; Task 1 Step 1 saves it whole. 99a3defe changes only this document, so the model is fbdad381's; the rev 2 dry run recorded the same summary and the same 1,992-byte COUNTERS line.

Every task was dry-run in order on this baseline (see "Rev 2: sync to 1b-next rev 16"). Task 1's code below is rev 1's, unchanged, and its rev 2 dry run gave the same two summary lines. Tasks 2 to 6 are patches.

---

Task 1: The world's shape, one or two boxes per region (L18; spec §2, §4, §5.2, H5, H12, L8, L15)

Dry-run on the baseline in rev 1 and again in revs 2 to 4. Rev 4 adds the identity tests (Step 1) and keeps createExecutor and the recovered-create cancellation out of the one-box shape (Astra round 1 finding 1); otherwise its code is rev 1's, and the later tasks' patches assume exactly this tree. The model gains a shape, boxesPerRegion, read from HOSTLIFE_BOXES and set by TestHostLifecycleTwoBox; a second enrolled box per region in the two-box shape, drawn after every one-box draw; chooseBox, spec §5.2's choose(), used by a create (recorded once in the intent, rule create-choice-once) and a move's start (L15); adoptionOwner (P5-D2's one proven owner); regional chores owned by any live box of the region; replacements launched up to the region's minimum (H5).

Files:

• Create: internal/sim/hostlife/twobox_test.go
• Modify: internal/sim/hostlife/world_test.go (opState, world), internal/sim/hostlife/sim_test.go (newWorld, TestHostLifecycle), internal/sim/hostlife/console_test.go (createSteps steps 1 and 4, moveTo, recoveryPass creating), internal/sim/hostlife/background_test.go (adopt, replaceDestroyed), internal/sim/hostlife/moves_test.go (workerMode), internal/sim/hostlife/witness_test.go (newWitness), internal/sim/hostlife/rules_test.go
• Test: the gate, both shapes

Interfaces:

• Produces: var boxesPerRegion int; world.perRegion int; opState.NewBox int; (*world) regionBoxes(r int) []*box; (*world) addBox(r int) *box; tieHash(id int) uint32; (*world) hostsOn(b *box, app string) int; (*world) owesLocal(c *claim, b *box) bool; (*world) chooseBox(r int, app string) *box; (*world) adoptionOwner(r int) *box; (*world) ownsObligation(o obligation, b *box) bool; (*world) createExecutor(c *claim) *box; sweep(t *testing.T); rule create-choice-once.

• [ ] Step 1: Record the baseline

export GOFLAGS=-buildvcs=false GOCACHE=$TMPDIR/gocache; mkdir -p $TMPDIR/twobox
nice -n 19 go test ./internal/sim/hostlife/ -count=1 -v 2>&1 | tee $TMPDIR/twobox/baseline.log | grep -E "seeds, |^ok|^FAIL"
grep COUNTERS $TMPDIR/twobox/baseline.log | sed 's/.*COUNTERS //' > $TMPDIR/twobox/baseline-counters.json

Expected: 300 seeds, 0 failed, 483 completed operations; mutated="" and ok. If the numbers differ from the Baseline section, the tree is not fbdad381's model: stop and say so.

(Rev 4) Then, before any code change, add the one-box identity tests. They use only the baseline's APIs, so they compile against fbdad381. Record their traces.

Create internal/sim/hostlife/onebox_identity_test.go:

package hostlife

import (
	"crypto/sha256"
	"fmt"
	"os"
	"regexp"
	"strings"
	"testing"
)

// TestOneBoxCreateInterruptionTrace is a deterministic trace of the
// interruptions a one-box create recovers from (two-box plan rev 4,
// Astra round 1 finding 1): the create's record persists, then its
// selected box stops, then recovery runs for longer than its 15-step
// wait; the box starts again (stopped) or the region's group replaces
// it (destroyed). It writes the whole trace to $HOSTLIFE_TRACE_OUT when
// set, so the trace at the baseline and after each task can be compared
// byte for byte; the one-box shape must not change it.
func TestOneBoxCreateInterruptionTrace(t *testing.T) {
	var out []string
	for _, how := range []string{"restarted", "replaced"} {
		w := newWitness()
		w.console = append(w.console, &consolePlan{Kind: "create", Host: "h", App: app0, OpID: w.newID("cr"), Inc: 1, Region: 0})
		w.admit[app0].Reg[w.console[0].OpID] = regEntry{Until: w.now + 1000}
		w.drive(60, func() bool { return w.rec != nil && w.claim != nil && w.claim.Op.Kind == "creating" }, w.runConsole)
		b := w.boxes[0]
		b.Destroyed, b.Procs = true, nil
		w.logf("trace: box %d stopped after the record persisted", b.ID)
		w.drive(40, func() bool { return false }, w.runConsole, w.recoveryPass)
		if how == "restarted" {
			b.Destroyed = false
			b.forget()
		} else {
			w.replaceDestroyed()
		}
		w.logf("trace: box %s", how)
		w.drive(200, func() bool { return w.claim != nil && w.claim.Op.Kind == "serving" }, w.runConsole, w.recoveryPass, w.actAll())
		out = append(out, "== "+how)
		out = append(out, w.trace...)
		c := w.claim
		out = append(out, fmt.Sprintf("final: op=%s/%s exec=%d holder=%+v rec=%+v lost=%v obl=%d", c.Op.Kind, c.Op.ID, c.Op.Exec, c.Holder, w.rec, c.Lost, len(c.Obl)))
	}
	if p := os.Getenv("HOSTLIFE_TRACE_OUT"); p != "" {
		if err := os.WriteFile(p, []byte(strings.Join(out, "\n")+"\n"), 0o644); err != nil {
			t.Fatal(err)
		}
	}
}

// TestOneBoxSeedTraces writes one line per seed of the one-box sweep,
// the SHA-256 of its whole trace, to $HOSTLIFE_TRACE_OUT_SEEDS (and is
// skipped without it): the per-seed evidence that a task leaves every
// one-box trace as the baseline's, beyond the aggregate COUNTERS line.
// Map-ordered fields in state dumps are masked.
func TestOneBoxSeedTraces(t *testing.T) {
	p := os.Getenv("HOSTLIFE_TRACE_OUT_SEEDS")
	if p == "" {
		t.Skip("HOSTLIFE_TRACE_OUT_SEEDS is not set")
	}
	mask := regexp.MustCompile(`admission=\[[^\]]*\]`)
	var out []string
	for seed := int64(1); seed <= int64(seedsFromEnv(300)); seed++ { // the gate's seeds, 1..n (rev 11, Astra round 8)
		w := runSeed(seed, true)
		sum := sha256.Sum256([]byte(mask.ReplaceAllString(strings.Join(w.trace, "\n"), "admission=[masked]")))
		out = append(out, fmt.Sprintf("%d %x %d", seed, sum[:8], len(w.trace)))
	}
	if err := os.WriteFile(p, []byte(strings.Join(out, "\n")+"\n"), 0o644); err != nil {
		t.Fatal(err)
	}
}

nice -n 19 go test ./internal/sim/hostlife/ -run '^TestOneBox' -count=1 2>&1 | tail -1
HOSTLIFE_TRACE_OUT=$TMPDIR/twobox/baseline-trace.txt HOSTLIFE_TRACE_OUT_SEEDS=$TMPDIR/twobox/baseline-seeds.txt nice -n 19 go test ./internal/sim/hostlife/ -run '^TestOneBox' -count=1 >/dev/null
wc -l $TMPDIR/twobox/baseline-trace.txt $TMPDIR/twobox/baseline-seeds.txt

Expected: ok; 300 lines in baseline-seeds.txt. The interruption trace has both cases, and at the baseline each ends final: op=serving/..., the create recovered on the region's box.

• [ ] Step 2: Create twobox_test.go

package hostlife

import (
	"fmt"
	"hash/fnv"
	"os"
)

// Two boxes per region (region HA spec 1 §9 L18; claim rev 6.30 §11).
//
// boxesPerRegion is the world's shape: one box per region, today's model,
// where every seed is byte-identical to the one-box baseline (spec §4: a
// region with one box behaves exactly as today); or two, where every
// region starts with a second enrolled box and the placement, relocation
// and termination rules below apply. HOSTLIFE_BOXES=2 selects the two-box
// shape for a sweep (mutate.sh inherits it); TestHostLifecycleTwoBox sets
// it for its own run. A two-box world draws its extra random values only
// after the one-box draws of the same step, so the one-box stream is
// untouched.
var boxesPerRegion = 1

func init() {
	if os.Getenv("HOSTLIFE_BOXES") == "2" {
		boxesPerRegion = 2
	}
}

// regionBoxes is every live box of region r, by id.
func (w *world) regionBoxes(r int) []*box {
	var out []*box
	for _, b := range w.boxes {
		if b.Region == r && !b.Destroyed {
			out = append(out, b)
		}
	}
	return out
}

// addBox enrolls a second box in region r of a witness world: the secrets
// key held, no faults, id nRegions+r (the sweep's second boxes carry the
// same ids; replacements are 100 and up).
func (w *world) addBox(r int) *box {
	b := &box{ID: nRegions + r, Region: r, HasKey: true}
	b.forget()
	w.boxes = append(w.boxes, b)
	w.logf("witness: box %d enrolled in region %d", b.ID, r)
	return b
}

// tieHash is the model's stand-in for claim P5-D2's SHA-256 of
// host + "\x00" + box reference: a fixed function of the reference, never
// a draw, so the choice is the same on every replay.
func tieHash(id int) uint32 {
	h := fnv.New32a()
	h.Write([]byte(fmt.Sprintf("%s\x00%d", host, id)))
	return h.Sum32()
}

// hostsOn counts the instances of app placed on b (app "" counts every
// app): the claimed host on its executor, or on the box its create or
// move named.
func (w *world) hostsOn(b *box, app string) int {
	c := w.claim
	if c == nil || c.Holder == nil || (app != "" && c.Holder.App != app) {
		return 0
	}
	switch {
	case c.Op.Kind == "creating" && c.Op.NewBox == b.ID:
		return 1
	case c.Op.Exec == b.ID:
		return 1
	}
	return 0
}

// owesLocal: an open park-local chore names b.
func (w *world) owesLocal(c *claim, b *box) bool {
	if c == nil {
		return false
	}
	for _, o := range c.Obl {
		if o.Kind == "park-local" && o.Box == b.ID {
			return true
		}
	}
	return false
}

// chooseBox is region HA §5.2's choose() (H12, L8; a move's target under
// L15): among the eligible boxes of region r (§2: live, running the
// claim's executable, holding the secrets key, not on lost, not owing a
// park-local for the host), prefer one running no instance of app, then
// the fewest hosts, then the greatest tieHash. With one box in the region
// it is that box, as today (spec §4). It is a pure function of the world;
// the caller records the choice in the claim's intent and never
// substitutes (rule create-choice-once).
func (w *world) chooseBox(r int, app string) *box {
	bs := w.regionBoxes(r)
	if len(bs) <= 1 {
		if len(bs) == 0 {
			return nil
		}
		return bs[0]
	}
	c := w.claim
	var best *box
	var bestKey [3]int
	for _, b := range bs {
		if b.Old || !b.HasKey || (c != nil && contains(c.Lost, b.ID)) || w.owesLocal(c, b) {
			continue
		}
		key := [3]int{w.hostsOn(b, app), w.hostsOn(b, ""), -int(tieHash(b.ID))}
		if best == nil || key[0] < bestKey[0] || key[0] == bestKey[0] && (key[1] < bestKey[1] || key[1] == bestKey[1] && key[2] < bestKey[2]) {
			best, bestKey = b, key
		}
	}
	return best
}

// adoptionOwner is the box adoption runs on (claim P5-D2, region HA §9 K5):
// with one live box in the record's region it is that box, as today; with
// more, exactly one box must hold the legacy host's local state (its row
// or database), and zero or several refuse adoption.
func (w *world) adoptionOwner(r int) *box {
	bs := w.regionBoxes(r)
	if len(bs) <= 1 {
		if len(bs) == 0 {
			return nil
		}
		return bs[0]
	}
	var owner *box
	for _, b := range bs {
		holds := b.Row != nil && b.Row.Inc == w.rec.Inc || b.DB != nil && b.DB.Inc == w.rec.Inc
		if !holds {
			continue
		}
		if owner != nil {
			return nil // several proven owners: refused
		}
		owner = b
	}
	return owner
}

// ownsObligation: b may run chore o. A park-local is its box's alone; a
// regional chore is any live box of its region's (claim P6-D5: regional
// workers), as it was the region's one box's.
func (w *world) ownsObligation(o obligation, b *box) bool {
	if o.Kind == "park-local" {
		return w.ownerOf(o) == b
	}
	return b.Region == o.Region && !b.Destroyed
}

• [ ] Step 3: The additive fields and the shape in world_test.go and sim_test.go

In world_test.go, opState, after NewSerial int:

	NewBox               int // the executor a create named once (region HA §5.2, H12): never substituted

In world_test.go, type world struct {, as its first field (then gofmt -w the file, which realigns the block):

	perRegion int // boxes per region at the start (region HA L18): 1, today's model, or 2

In sim_test.go, newWorld, the first line of the literal becomes:

	w := &world{seed: seed, rng: &counting{r: rand.New(rand.NewSource(seed))}, verbose: verbose, perRegion: boxesPerRegion,

and, between the retentionStart() block's closing brace and return w:

	// the two-box shape (region HA L18): a second enrolled box in every
	// region, drawn after every one-box draw of this world, so the one-box
	// stream is untouched; id nRegions+r, as addBox gives a witness
	for r := 0; r < nRegions && w.perRegion > 1; r++ {
		b := &box{ID: nRegions + r, Region: r, HasKey: w.rng.Intn(4) != 0, Skew: w.rng.Intn(3) - 1, Nested: w.rng.Intn(2) == 0}
		if w.rng.Intn(4) == 0 {
			b.FailApp = true
		}
		if w.rng.Intn(10) == 0 {
			b.FailArchive = true
		}
		if w.rng.Intn(2) == 0 {
			b.FailSettle = true
		}
		b.forget()
		w.boxes = append(w.boxes, b)
	}

Replace the head of TestHostLifecycle (its comment's last line, the signature and the first if) with:

// prints its trace; HOSTLIFE_BOXES=2 runs the two-box shape (region HA
// L18) in place of the one-box one.
func TestHostLifecycle(t *testing.T) {
	sweep(t)
}

// TestHostLifecycleTwoBox runs the joint model with two boxes per region
// (region HA L18) beside the one-box sweep, so the gate covers both
// shapes. With HOSTLIFE_BOXES set, TestHostLifecycle runs that shape and
// this test stands aside.
func TestHostLifecycleTwoBox(t *testing.T) {
	if os.Getenv("HOSTLIFE_BOXES") != "" {
		t.Skip("HOSTLIFE_BOXES is set: TestHostLifecycle runs that shape")
	}
	saved := boxesPerRegion
	boxesPerRegion = 2
	defer func() { boxesPerRegion = saved }()
	sweep(t)
}

func sweep(t *testing.T) {
	if s := os.Getenv("HOSTLIFE_SEED"); s != "" {

and the summary line becomes:

	t.Logf("%d seeds, %d failed, %d completed operations; mutated=%q boxes=%d", n, failed, ops, mutated, boxesPerRegion)

(mutate.sh's grep 0 failed.*mutated="$r" still matches.)

In witness_test.go, newWitness, the literal's first line gains perRegion: 1,:

	w := &world{seed: -1, rng: quiet{}, verbose: true, now: 100, perRegion: 1,

• [ ] Step 4: The callers: create, move, adoption, chores, replacements

console_test.go, createSteps case 1, replace b := w.regionBox(p.Region) with:

		// the executor, chosen once and recorded in the intent (region HA
		// §5.2, H12, L8; claim P5-D6 selected_executor)
		b := w.chooseBox(p.Region, p.App)

and in the same case's CAS, the n.Op = opState{Kind: "creating", ...} literal gains NewBox: b.ID, after NewRegion: p.Region,.

createSteps default case: replace b := w.regionBox(c.Op.NewRegion) with b := w.createExecutor(c) (the following if b == nil { return false } stays).

Before moveTo, add:

// createExecutor is the box a create's step 4 hands op.exec to: the one
// its intent named, never another (region HA §5.2, claim P5-D2: recovery
// never substitutes a newly available box); nil while that box is gone.
// The mutation of create-choice-once chooses again, as rev 7.22's
// region-wide pick did.
func (w *world) createExecutor(c *claim) *box {
	if w.perRegion <= 1 {
		return w.regionBox(c.Op.NewRegion) // the one-box shape: today's region-wide pick, unchanged (spec §4; rev 4, Astra R1-1)
	}
	if !on("create-choice-once") {
		return w.chooseBox(c.Op.NewRegion, c.Holder.App)
	}
	b := w.boxByID(c.Op.NewBox)
	if b == nil || b.Destroyed {
		return nil
	}
	return b
}

In moveTo, replace tgt := w.regionBox(r) with:

	tgt := w.chooseBox(r, c.Holder.App) // the target box, chosen in the start CAS (region HA L15)

In recoveryPass, case "creating", replace the four lines from b := w.regionBox(c.Op.NewRegion) through its } with:

			b := w.createExecutor(c)
			if b == nil {
				if nb := w.boxByID(c.Op.NewBox); w.perRegion > 1 && on("create-choice-once") && (nb == nil || nb.Destroyed) {
					// the chosen box cannot complete the create (the two-box
					// shape only; the one-box shape waits for its region's
					// box, as the baseline does): recovery cancels it (claim
					// §5.1 step 5, P5-D6), retiring the
					// incarnation; the record is an orphan the cleanup removes
					inc, app, id := c.Holder.Inc, c.Holder.App, c.Op.ID
					if w.cas(c, func(n *claim) bool {
						if !sameOp(n.Op.ID, id) {
							return false
						}
						n.Holder, n.Op = nil, opState{}
						n.Regions, n.Boxes = nil, nil
						n.Retired = retire(n.Retired, inc)
						n.Cancelled = append(n.Cancelled, cancelledCreate{Inc: inc, Until: w.now + 4*horizonH})
						return true
					}) {
						delete(w.admit[app].Reg, id)
						w.stats["create cancelled: its box is gone"]++
						w.logf("recovery: cancelled create %s inc %d, its chosen box %d is gone", id, inc, c.Op.NewBox)
					}
				}
				return
			}

background_test.go, adopt: replace eb := w.regionBox(w.rec.Region) with eb := w.adoptionOwner(w.rec.Region) // exactly one proven owner (claim P5-D2).

background_test.go, replaceDestroyed: replace if w.regionBox(r) == nil { with for len(w.regionBoxes(r)) < w.perRegion { // the region's minimum (H5): the group launches replacements.

moves_test.go, workerMode: replace if w.ownerOf(o) == b { with if w.ownsObligation(o, b) {.

rules_test.go, at the end of allRules:

	// region HA (two boxes per region, L18)
	"create-choice-once", // region HA §5.2, claim P5-D2/P5-D6: the create's executor is chosen once and recorded in the intent; recovery never substitutes, it cancels a create whose box is gone

• [ ] Step 5: Build, vet, run both shapes

gofmt -w internal/sim/hostlife/world_test.go && gofmt -l internal/sim/hostlife/
nice -n 19 go vet ./internal/sim/hostlife/
nice -n 19 go test ./internal/sim/hostlife/ -count=1 -v 2>&1 | tee $TMPDIR/twobox/task1.log | grep -E "seeds, |^--- FAIL|^ok|^FAIL"

Expected: gofmt prints nothing; two summary lines, 300 seeds, 0 failed, 483 completed operations; mutated="" boxes=1 and 300 seeds, 0 failed, <n> completed operations; mutated="" boxes=2 (the dry run gave 447); ok.

• [ ] Step 6: Prove the one-box shape byte-identical

diff $TMPDIR/twobox/baseline-counters.json <(grep COUNTERS $TMPDIR/twobox/task1.log | head -1 | sed 's/.*COUNTERS //') && echo ONE-BOX-COUNTERS-IDENTICAL
grep COUNTERS $TMPDIR/twobox/task1.log | sed -n 2p | sed 's/.*COUNTERS //' > $TMPDIR/twobox/twobox-counters-task1.json
HOSTLIFE_TRACE_OUT=$TMPDIR/twobox/trace.txt HOSTLIFE_TRACE_OUT_SEEDS=$TMPDIR/twobox/seeds.txt nice -n 19 go test ./internal/sim/hostlife/ -run '^TestOneBox' -count=1 >/dev/null
cmp $TMPDIR/twobox/baseline-trace.txt $TMPDIR/twobox/trace.txt && cmp $TMPDIR/twobox/baseline-seeds.txt $TMPDIR/twobox/seeds.txt && echo ONE-BOX-TRACES-IDENTICAL

Expected: ONE-BOX-COUNTERS-IDENTICAL and ONE-BOX-TRACES-IDENTICAL. If diff prints anything, a one-box path drew where it did not before: find the draw (git diff shows every call site) and move it under w.perRegion > 1. If only a trace differs, a one-box path behaves differently with the same draws. Rev 3's createExecutor and recovered-create cancellation did that (Astra round 1 finding 1), so both are now the two-box shape's alone.

• [ ] Step 7: Commit

git add internal/sim/hostlife/
git commit -m "sim: one or two boxes per region (region HA L18): HOSTLIFE_BOXES and TestHostLifecycleTwoBox, choose() for creates and move targets recorded once, adoption's one proven owner, regional chores for any box of the region, replacements to the region's minimum; the one-box sweep is byte-identical

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

Task 2: Relocation by drain, the full phase table, with 1b-next rev 16's guards (spec §5.8; claim §4 L1; L9 to L12; 1b-next Tasks 1, 5, 6, 7 and rulings 9, 11, 14 to 16, 19)

The existing relocate in moves_test.go collapsed the operation to pinning → probing → probed → opened for the one-box conversion of a pre-flip move (rev 7.20). This task replaces its body with spec §5.8's phase table, starting → releasing → pinning → installing → installed → probing → (probe-failed) → serving, keeping the conversion CAS (convertToRelocating, rule fence-converts-moving) and the settle steps (probed, opened). The witness fence-converts-moving must still pass: it drives a converted operation from pinning to serving on the replacement box.

Guards this task adds, each with the 1b-next rev 16 function it mirrors:

| Rule | 1b-next rev 16 | What the model does | |---|---|---| | reloc-start-guard | RelocationStartGuard | a park-generation never blocks a start (L11); a park-replica in the region and a park-local on the target or a live source do | | reloc-exec-ack-barrier | requireAcks in ToReleasing, ToInstalling | every participant's execution lease is current before starting is left and before op.exec is handed over | | reloc-ack-before-pinning | PinAfterRelease's requireAcks (rev 4 N6) | the same barrier before releasing is left | | reloc-release-first | PinAfterRelease cites the journaled release | pinning needs the source's release entry | | reloc-release-deadline | Worker.releaseOverdue, ReleaseDeadline (ruling 14) | a release not journaled releaseDeadline after releasing or probe-failed began marks the operation stuck | | reloc-pin-reaches-release | JournalPin's release bound | the pin's position reaches the release's final_txid | | reloc-pin-claim-gen | RecoveryPinKey, JournalPin (ruling 16) | the pin CAS requires the claim version it was selected against | | reloc-pin-evidenced-empty | JournalPin, StorePinner's Empty (ruling 15) | an empty listing pins only after a release flushed at 0 or for a holder that never had a writer; otherwise stuck | | reloc-failover-pin-delay | FailoverPinDelay | a failover pins no earlier than the fence's observedat plus 30 s | | reloc-exec-only-installs | §5.8 Exclusion; ToInstalling | only op.exec builds P and makes the local install (HA2) | | reloc-install-receipt | RecordLocalInstall, ToProbing | probing needs a receipt for exactly op.exec and `installstamp; a replacement never inherits one | | reloc-ensure-local | Effects.EnsureLocal (rev 15 finding 2) | before P's first admission the install is verified, and restored under the same stamp after a lost lease's scoped cleanup | | reloc-verify-receipt | Effects.VerifyReceipt, MarkStuck in probing (rev 16 finding 1) | after P opens, a missing or different install journal marks the operation stuck before any admission | | reloc-no-reinstall | RecordLocalInstall refused after PreparedOpened | the install is never remade after P's first admission | | reloc-prepared-opened-journal | prepared_opened (rev 12 S1) | P's opening is journaled with its admission and read before the trimmed admission list | | reloc-probe-attempts | BeginProbeAttempt, MaxProbeAttempts (ruling 19) | each attempt is counted in the claim before it is made; the fourth is probe-failed | | reloc-released-coverage | relocationAdmission, coverageFor (L9) | released only on the admission that opens P, for exactly the flushed release's box, session and generation, with the pin reaching it | | reloc-row-cases | hostbox.RelocationRow, Task 9a (L12) | the source's row is held once its release is journaled | | reloc-replacement-cap | MaxTargetReplacements, stuckOn | a third replacement is stuck; exhaustion is checked before a spare is looked for (R1-16) | | reloc-drain-needs-writer | Worker.Start (ruling 11) | a host with no writer session is never drained; a drain also needs the app's admission open (ruling 4) | | reloc-enrolled-only | eligibleBoxes` | named here; Task 3 gives it behaviour and a witness |

The model also mirrors, without a rule of its own: MarkStuck's refusal between installed and a probe while P is unopened; ToProbeFailed dropping the journaled release; install's reset of the probe attempts for a new executor; CompleteRelocation's park-local leftovers; the operator's resolve (plan ruling 13); and the bounded wait in probe-failed (plan ruling 14, finding F1).

Files:

• Create: internal/sim/hostlife/regionha_test.go, internal/sim/hostlife/regionha_witness_test.go
• Modify: world_test.go (box, opState, the journal types, claim.clone, forget), twobox_test.go (chooseBoxExcept), moves_test.go (relocate, convertToRelocating, release, role), protocol_test.go (admits, admitWriter, admitCommit, installGen, localPark), background_test.go (replaceDestroyed, reconcileClaimed), console_test.go (operator), sim_test.go (newWorld, step, checkStep), witness_test.go (newWitness), rules_test.go
• Test: the gate; TestDrainEndToEnd

Interfaces:

• Consumes: Task 1's chooseBox, regionBoxes, addBox, owesLocal; the model's evidence, ship, deltaOf, remoteMax, currentLTX, snapshotOf, ackedPut, anchorAcked, issueStamp, holdRow, openRow, admits, spawn, probeAccepted, release, leasesSeen, retireArtifacts, hasFiles, bucketGen, unfinishedRun, runBaseline, cas, sameOp.
• Produces: constants failoverPinDelay, probeDeadline, releaseDeadline, maxReplacements, enrollDelay, replaceDelay; types releaseEntry, pinEntry{Gen, TX, ManKey, ManVer, ManSeq, At, ClaimVer, Files, Timers}, receiptEntry{Op, Box, Stamp}; (*world) chooseBoxExcept(r int, app string, except ...int) *box; (*world) userRelocate(); relocExcept(op opState, extra ...int) []int; (*world) relocRelease, pinSource, selectPin, restoreUpTo, relocFiles, relocTimers, nameReplacement, markStuck, relocationLeftovers, handExec, localInstall, ensureLocal, verifyReceipt, scopedCleanup; preparedOpened(c *claim) bool; the phase handlers relocStarting to relocSettle; buildPreparedFiles (a no-op until Task 4); twoBoxWitness().

• [ ] Step 1: Apply the patch

From the worktree root, git apply this patch (the dry run's, made against Task 1's tree):

diff --git a/internal/sim/hostlife/background_test.go b/internal/sim/hostlife/background_test.go
index cf45639..19c5874 100644
--- a/internal/sim/hostlife/background_test.go
+++ b/internal/sim/hostlife/background_test.go
@@ -232,6 +232,14 @@ func (w *world) reconcileClaimed(b *box, c *claim) {
 			w.retireRow(b)
 		}
 	default:
+		if c.Op.Kind == "relocating" && b.ID == c.Op.Src && b.Row != nil && b.Row.Status == "ready" && c.Op.Release != nil {
+			// §5.3, L12 (rule reloc-row-cases): the former executor's row is
+			// held once its admission fence closed, never ready, until its
+			// park-local retires it. The mutation reopens it as a stale hold
+			if on("reloc-row-cases") {
+				b.Row.Status, b.Row.HoldOp = "relocating", c.Op.ID
+			}
+		}
 		if w.isParticipant(c, b) {
 			if !on("participant-rows") && w.rec.Region != b.Region && b.Row != nil {
 				w.retireRow(b) // region mismatch retires a participant's row
@@ -470,7 +478,7 @@ func (w *world) replaceDestroyed() {
 	for r := 0; r < nRegions; r++ {
 		for len(w.regionBoxes(r)) < w.perRegion { // the region's minimum (H5): the group launches replacements
 			w.nextID++
-			nb := &box{ID: 100 + w.nextID, Region: r, HasKey: true}
+			nb := &box{ID: 100 + w.nextID, Region: r, HasKey: true, Enrolled: w.perRegion == 1, EnrollAt: w.now, DeleteOnTermination: true}
 			nb.forget()
 			w.boxes = append(w.boxes, nb)
 			w.logf("box %d replaces the destroyed box in region %d", nb.ID, r)
diff --git a/internal/sim/hostlife/console_test.go b/internal/sim/hostlife/console_test.go
index b02f9a3..942bb8a 100644
--- a/internal/sim/hostlife/console_test.go
+++ b/internal/sim/hostlife/console_test.go
@@ -1219,6 +1219,55 @@ func (w *world) operator() {
 			return
 		}
 	}
+	// a stuck relocation (§5.8): carlos ops host resolve (model ruling 13;
+	// the spec names the command and leaves its effect open). Nothing
+	// moves away from a live box without its stop evidence:
+	//   - a live source still op.exec (starting, releasing, no release):
+	//     the relocation is abandoned and the host serves on the source;
+	//   - a live target op.exec without a release (its receipt lost after
+	//     P opened, its release overdue): it is sent to probe-failed, where
+	//     it runs its release sequence;
+	//   - op.exec none, released, or lost: replayed from pinning with the
+	//     replacement count reset, the exclusions cleared and the source
+	//     eligible again (Resolved), an empty listing accepted
+	if c.Holder != nil && c.Op.Kind == "relocating" && c.Op.Stuck != "" {
+		op := c.Op
+		released := op.Release != nil && op.Release.Box == op.Exec
+		var what string
+		if w.cas(c, func(n *claim) bool {
+			if !sameOp(n.Op.ID, op.ID) || n.Op.Kind != "relocating" || n.Op.Stuck == "" {
+				return false
+			}
+			switch {
+			case op.Exec >= 0 && op.Exec == op.Src && !released && !contains(n.Lost, op.Exec) && (op.Phase == "starting" || op.Phase == "releasing"):
+				src := op.Src
+				n.Op = opState{Kind: "serving", Exec: src, Parts: []int{src}}
+				what = "abandoned; the host serves on its source"
+			case op.Exec >= 0 && !released && !contains(n.Lost, op.Exec):
+				n.Op.Stuck, n.Op.Phase, n.Op.FailedAt, n.Op.Release = "", "probe-failed", w.now, nil
+				what = "sent its live target to probe-failed"
+			default:
+				n.Op.Stuck, n.Op.Replacements, n.Op.Excluded, n.Op.Resolved = "", 0, nil, true
+				n.Op.Phase, n.Op.Exec, n.Op.Tgt = "pinning", -1, -1
+				n.Op.Pin, n.Op.Prepared, n.Op.Receipt = nil, "", nil
+				n.Op.BaseKey, n.Op.BaseVer, n.Op.BaseTX = "", 0, 0
+				n.Op.ProbeTries, n.Op.Attempts = 0, 0
+				var parts []int
+				for _, p := range n.Op.Parts {
+					if !contains(n.Lost, p) && p != op.Exec {
+						parts = append(parts, p)
+					}
+				}
+				n.Op.Parts = parts
+				what = "replayed from pinning"
+			}
+			return true
+		}) {
+			w.stats["operator resolved a stuck relocation"]++
+			w.logf("operator resolved stuck relocation %s: %s", op.ID, what)
+		}
+		return
+	}
 	// a host marked failed by the retry policy (rev 7.11 §7.14): the operator
 	// looks at it and clears the mark; the next attempt is a new session
 	for _, b := range w.liveBoxes() {
diff --git a/internal/sim/hostlife/moves_test.go b/internal/sim/hostlife/moves_test.go
index d547b8d..078094e 100644
--- a/internal/sim/hostlife/moves_test.go
+++ b/internal/sim/hostlife/moves_test.go
@@ -151,6 +151,9 @@ func (w *world) role(b *box, c *claim) {
 	w.initRecord(b, c)
 	// exec lease (claim §7.1)
 	if w.isParticipant(c, b) && !contains(c.Lost, b.ID) {
+		if b.ExecUntil > 0 && w.localNow(b) > b.ExecUntil {
+			w.scopedCleanup(b, c) // the relocation controller's lease was lost (1b-next rev 14 finding 1)
+		}
 		if b.ExecUntil == 0 || b.ExecUntil-w.localNow(b) < execRenew {
 			b.ExecUntil = w.localNow(b) + execTTL
 			w.execLease[b.ID] = execLease{Op: c.Op.ID, Expires: w.now + execTTL}
@@ -242,6 +245,8 @@ func (w *world) convertToRelocating(c *claim, src *box) {
 			return false
 		}
 		n.Op.Kind, n.Op.Phase, n.Op.Exec, n.Op.FenceBox = "relocating", "pinning", -1, src.ID
+		n.Op.RelocReason, n.Op.FenceAt, n.Op.Tgt, n.Op.Src = "failover", w.now, -1, src.ID
+		n.Op.Pin, n.Op.Prepared, n.Op.Receipt, n.Op.Release = nil, "", nil, nil
 		// the files the relocation installs: region HA §5.6's files
 		// publisher kept the source's files directory in S3 as it served
 		// (L17); this model has no publisher, so the fence takes the
@@ -267,92 +272,34 @@ func (w *world) convertToRelocating(c *claim, src *box) {
 	}
 }
 
-// relocate is the relocation's worker on a box of the source's region
-// (claim rev 6.28 §4's table, collapsed as this model collapses an install:
-// pinning hands execution to the region's one eligible box with a new
-// installation stamp, the install and the probe are the cold admission's
-// restore of the pinned generation from this region's remote, and the
-// release preserves the outstanding lane park, which is disjoint from the
-// serving location).
+// relocate is the relocation's worker on a box of the operation's region
+// (region HA §5.8's phase table; claim rev 6.30 §4): every live, enrolled
+// box of the region that is not on lost may act, and each phase's CAS is
+// conditional on the operation, the phase and the ETag, so two workers
+// racing make the same CAS and one fails. The phases live in
+// regionha_test.go. A stuck operation waits for the operator.
 func (w *world) relocate(b *box, c *claim) {
 	op := c.Op
-	if b.Region != op.SrcRegion || b.Destroyed || contains(c.Lost, b.ID) {
+	if b.Region != op.SrcRegion || b.Destroyed || contains(c.Lost, b.ID) || !b.Enrolled || op.Stuck != "" {
 		return
 	}
 	switch op.Phase {
+	case "starting":
+		w.relocStarting(b, c)
+	case "releasing":
+		w.relocReleasing(b, c)
 	case "pinning":
-		if op.Exec != -1 {
-			return
-		}
-		if w.cas(c, func(n *claim) bool {
-			if !sameOp(n.Op.ID, op.ID) || n.Op.Kind != "relocating" || n.Op.Phase != "pinning" || n.Op.Exec != -1 {
-				return false
-			}
-			n.Op.Exec, n.Op.Tgt, n.Op.Phase = b.ID, b.ID, "probing"
-			n.Op.Parts = []int{b.ID}
-			n.Boxes = addUniq(n.Boxes, b.ID)
-			n.Holder.Stamp = w.issueStamp(n, b.ID) // a new installation's stamp (claim rev 6.28 §4)
-			return true
-		}) {
-			// the local install (collapsed): the published files directory
-			// (L17) materialized under the new stamp, before the probe
-			if op.StopFiles != nil && b.Files == nil {
-				f := op.StopFiles.clone()
-				f.Done = true
-				b.Files = f
-			}
-			w.logf("relocation %s: box %d takes the host in region %d", op.ID, b.ID, b.Region)
-		}
+		w.relocPinning(b, c)
+	case "installing":
+		w.relocInstalling(b, c)
+	case "installed":
+		w.relocInstalled(b, c)
 	case "probing":
-		if op.Exec != b.ID {
-			return
-		}
-		if b.Row == nil {
-			w.holdRow(b, "landing", op.ID, c)
-			return
-		}
-		if !w.admits(b, c, op.ID) {
-			return
-		}
-		if b.HasKey { // RenderHeld + MaterializeHeld before every probe
-			b.Config, b.CfgVer, b.Live, b.LiveInc = c.Holder.Inc, w.cfgVer[c.Holder.App], c.Holder.App, c.Holder.Inc
-		}
-		if hasMain(b) || w.spawn(b, c, c.Holder.Gen, true) {
-			w.probeAccepted(b, c)
-			w.cas(c, func(n *claim) bool { n.Op.Phase = "probed"; return sameOp(n.Op.ID, op.ID) })
-			return
-		}
-		if b.hostFailed && !b.failCounted {
-			b.failCounted = true
-		} else if b.open != nil || b.hostFailed {
-			return
-		}
-		w.cas(c, func(n *claim) bool {
-			n.Op.ProbeTries++
-			if n.Op.ProbeTries >= probeTries*3 {
-				n.Op.Phase = "stuck"
-			}
-			return sameOp(n.Op.ID, op.ID)
-		})
-	case "probed":
-		if op.Exec != b.ID {
-			return
-		}
-		if b.open != nil {
-			return
-		}
-		if !hasMain(b) {
-			w.stats["probe restarted"]++
-			w.cas(c, func(n *claim) bool { n.Op.Phase = "probing"; return sameOp(n.Op.ID, op.ID) })
-			return
-		}
-		if w.openRow(b, op.ID) {
-			w.cas(c, func(n *claim) bool { n.Op.Phase = "opened"; return sameOp(n.Op.ID, op.ID) })
-		}
-	case "opened":
-		if op.Exec == b.ID {
-			w.release(c, b.ID) // outstanding disjoint parks do not block serving (claim rev 6.28 §4)
-		}
+		w.relocProbing(b, c)
+	case "probe-failed":
+		w.relocProbeFailed(b, c)
+	case "probed", "opened":
+		w.relocSettle(b, c)
 	}
 }
 
@@ -1343,6 +1290,9 @@ func (w *world) release(c *claim, execBox int) {
 		// holder.admissions survives the release by living in the holder
 		// (claim rev 6.12): an admission whose start is unfinished at the
 		// release stays explained (seed 1052 / 30,000)
+		if op.Kind == "relocating" {
+			w.relocationLeftovers(n, op) // the abandoned installations' park-local chores (claim §4)
+		}
 		n.Op = opState{Kind: "serving", Exec: execBox, Parts: []int{execBox}}
 		return true
 	}) {
diff --git a/internal/sim/hostlife/protocol_test.go b/internal/sim/hostlife/protocol_test.go
index ec383bb..8ff23c1 100644
--- a/internal/sim/hostlife/protocol_test.go
+++ b/internal/sim/hostlife/protocol_test.go
@@ -1435,6 +1435,9 @@ func (w *world) admits(b *box, c *claim, probe string) bool {
 		if probe != "" {
 			return probe == op.ID && role(op.Tgt) && op.Phase == "probing"
 		}
+		if role(op.Src) && (op.Phase == "starting" || op.Phase == "releasing" && op.Release == nil) {
+			return b.Row.Status == "ready" // the source serves until its admission fence closes (§5.3, §5.8)
+		}
 		return role(op.Tgt) && op.Phase == "opened" && b.Row.Status == "ready"
 	}
 	return false
@@ -1485,8 +1488,11 @@ func (w *world) certificate(b *box, c *claim) *version {
 // holder.generation is the only authoritative generation, in every kind
 // and phase).
 func installGen(op *opState) string {
-	if op.Kind == "restoring" {
+	switch op.Kind {
+	case "restoring":
 		return op.RollbackID
+	case "relocating":
+		return op.Prepared // P, fresh per installation (region HA §5.8)
 	}
 	return op.ID
 }
@@ -1651,6 +1657,26 @@ func (w *world) admitWriter(b *box, c *claim, want string, probe bool) (admitInp
 		covers = c.Op.ReturnFromDB
 	}
 	a.Mode, a.NewGeneration = "cold", want
+	if c.Op.Kind == "relocating" {
+		// released (claim §6.4a item 2, L9): only on the admission that
+		// opens P, and only when the predecessor is exactly the box and
+		// session whose flushed release this operation journaled and whose
+		// final_txid the pin reached; a failover's first admission and every
+		// later attempt declare (coverage ""). The mutation of
+		// reloc-released-coverage grants it to every first opening of P
+		r := c.Op.Release
+		predBox, predSession, predGen := h.WriterBox, h.Session, h.Gen // the predecessor's identity as admitCommit journals it
+		if l := lastAdmission(h); l != nil {
+			predBox, predSession, predGen = l.Box, l.Session, l.Gen
+		}
+		switch {
+		case !on("reloc-released-coverage"):
+			a.Coverage = "released"
+		case r != nil && r.Flushed && c.Op.Pin != nil && c.Op.Pin.TX >= r.FinalTX && predBox == r.Box && predSession == r.Session && predGen == r.Gen:
+			a.Coverage = "released"
+		}
+		return a, true
+	}
 	if covers {
 		a.Coverage = "sealed"
 	}
@@ -1869,7 +1895,7 @@ func (w *world) admitCommit(b *box, c *claim, a admitInput) bool {
 			// unfinished admission until generation.json names the new
 			// generation; the chore is queued then (claim rev 6.10, R10-2).
 			// The mutation of baseline-live queues it now, as rev 7.10 did
-			if !on("baseline-live") && a.Coverage != "sealed" {
+			if !on("baseline-live") && a.Coverage != "sealed" && a.Coverage != "released" {
 				ret := h.Gen
 				if ret == "" {
 					ret = "@root"
@@ -1877,6 +1903,9 @@ func (w *world) admitCommit(b *box, c *claim, a admitInput) bool {
 				n.Obl = append(n.Obl, w.scoped(obligation{ID: w.newID("ob"), Op: fmt.Sprintf("session:%d", n.Holder.Session), Kind: "park-generation", Region: b.Region, Box: -1, Prefix: n.Holder.Location, Ret: ret, Quiet: w.now + horizonH}, w.now, n.Holder.Inc))
 			}
 		}
+		if n.Op.Kind == "relocating" && n.Op.Prepared != "" && gen == n.Op.Prepared {
+			n.Op.PreparedOpened = gen // prepared_opened, journaled with the admission that opens P (1b-next rev 12 S1)
+		}
 		n.Holder.Admissions = append(n.Holder.Admissions, e)
 		entry = e
 		return true
@@ -2169,6 +2198,7 @@ func (w *world) localPark(b *box, inc int) bool {
 	case len(b.Timers) > 0 || len(b.History) > 0 || b.Attempt != 0:
 		b.Timers, b.History, b.Attempt = nil, nil, 0
 	default:
+		b.receipt = nil // a relocation's install journal goes with the installation
 		return true
 	}
 	b.Parked++
diff --git a/internal/sim/hostlife/regionha_test.go b/internal/sim/hostlife/regionha_test.go
new file mode 100644
index 0000000..4627712
--- /dev/null
+++ b/internal/sim/hostlife/regionha_test.go
@@ -0,0 +1,997 @@
+package hostlife
+
+import "fmt"
+
+// ---------- relocation (region HA spec 1 §5.8; claim rev 6.30 §4, L1; plan 1b-next rev 16) ----------
+//
+// A same-region executor change. The model's steps are abstract time:
+// probeStartWindow (30) is a probe attempt's readiness window, so the
+// probe deadline holds three attempts; sigAgeH (45) is the 15-minute
+// signature age, so the failover pin delay (30 s) is two steps. Each
+// guard names the plan 1b-next rev 16 function it mirrors.
+
+const (
+	failoverPinDelay = 2                       // §5.8: pin no earlier than the fence's observed_at plus 30 s (hostclaim.FailoverPinDelay)
+	probeDeadline    = 3*probeStartWindow + 10 // §5.8: at most three attempts within the probe deadline (hostrelocate.ProbeDeadline)
+	releaseDeadline  = probeDeadline           // 1b-next ruling 14: a release not journaled this long after releasing or probe-failed began is stuck (hostrelocate.ReleaseDeadline, 10 minutes like the probe deadline)
+	maxReplacements  = 2                       // §5.8: after two replacements of the target, stuck (hostclaim.MaxTargetReplacements)
+	enrollDelay      = 20                      // H16, H17: a launched box is confirmed and enrolled by a worker some time later
+	replaceDelay     = 30                      // H5: the group launches a replacement for a terminated box
+)
+
+// userRelocate is a scale-in drain (§5.8, reason drain; spec 4 owns the
+// decision): the serving host's executor is asked to give the host to
+// another eligible box of its region. The start CAS (StartRelocation)
+// records the intent, op.exec stays on the source, and both participants
+// acknowledge by writing execution leases (role()). The two-box step
+// draws it. A host that never admitted a writer is not drained (1b-next
+// ruling 11, Worker.Start; rule reloc-drain-needs-writer): its release has
+// no writer session to stop, so root refuses its stop evidence and the
+// drain could only wait for its release deadline; a failover relocates it.
+func (w *world) userRelocate() {
+	c := w.claim
+	if c == nil || c.Holder == nil || c.Op.Kind != "serving" {
+		return
+	}
+	from := w.execBox(c)
+	if from == nil || from.Destroyed || from.Old || !from.Enrolled {
+		return
+	}
+	if ad := w.admit[c.Holder.App]; ad != nil && ad.Closed {
+		return // a box-started relocation needs the app's admission registration (1b-next ruling 4): a purge closed it
+	}
+	if on("reloc-drain-needs-writer") && c.Holder.Session == 0 {
+		w.stats["drain refused: the host never had a writer"]++
+		return
+	}
+	to := w.chooseBoxExcept(from.Region, c.Holder.App, from.ID)
+	if to == nil || to.Old {
+		return
+	}
+	id := w.newID("rl")
+	if w.cas(c, func(n *claim) bool {
+		if n.Holder == nil || n.Op.Kind != "serving" || n.Op.Exec != from.ID || !w.relocationStartAllowed(n, from, to) {
+			return false
+		}
+		n.Op = opState{Kind: "relocating", ID: id, Phase: "starting", Exec: from.ID, Parts: []int{from.ID, to.ID},
+			Src: from.ID, Tgt: to.ID, SrcRegion: from.Region, RelocReason: "drain", ReqAt: w.now, App: n.Holder.App,
+			SrcGen: n.Holder.Gen, SrcStamp: n.Holder.Stamp}
+		return true
+	}) {
+		w.stats["relocation started: drain"]++
+		w.logf("relocation %s: drain of inc %d from box %d to box %d in region %d", id, c.Holder.Inc, from.ID, to.ID, from.Region)
+	}
+}
+
+// relocationStartAllowed is the claim's start guard as L11 amends it for
+// relocating (RelocationStartGuard): a park-replica or any other
+// whole-location chore in the region blocks (CC11), a park-local on the
+// target or on a live source blocks, and a park-generation in the region
+// does not: relocation writes only its own new prepared generation, never
+// one being retired. The mutation of reloc-start-guard starts over
+// anything.
+func (w *world) relocationStartAllowed(c *claim, from, to *box) bool {
+	if !on("reloc-start-guard") {
+		return true
+	}
+	for _, o := range c.Obl {
+		switch {
+		case o.Kind == "park-generation":
+			continue // L11
+		case o.Kind == "park-local":
+			if o.Box == to.ID || o.Box == from.ID && !contains(c.Lost, from.ID) {
+				return false
+			}
+		case o.Region == from.Region:
+			return false
+		}
+	}
+	return true
+}
+
+// relocExcept is every box the operation may not name as its target
+// (replaceTargetSlot, Worker.next): the source, unless an operator's
+// resolve made it eligible again (model ruling 13), every replaced target,
+// and the extra boxes given.
+func relocExcept(op opState, extra ...int) []int {
+	var out []int
+	if !op.Resolved {
+		out = append(out, op.Src)
+	}
+	out = append(out, op.Excluded...)
+	return append(out, extra...)
+}
+
+// relocRelease is the release sequence (§5.8, A3-2; 1b-next Task 7's
+// Release) a live box runs to give the host up: the source in releasing,
+// a failed target in probe-failed. One step per call; it returns the
+// journal entry once every step is done, nil while one is owed.
+//
+//  1. stop every writer: admission closed (the row held), the process
+//     tree stopped and empty; an escaped descendant fails the step (L10);
+//  2. flush: the final checkpoint and SyncAndWait, passing only once the
+//     listing shows the stopped database's position N (moves §5.1 step
+//     1). When the session's replicator died with its agent (claim rev
+//     6.10) nothing can flush: the entry names what the remote holds,
+//     Flushed false, and the next admission declares the rest;
+//  3. publish every pending file and wake-state mutation: the entry
+//     carries them until Task 4's manifest.
+func (w *world) relocRelease(b *box, c *claim) *releaseEntry {
+	h := c.Holder
+	if b.Row != nil && b.Row.Status == "ready" {
+		w.holdRow(b, "relocating", c.Op.ID, c)
+	}
+	if !w.evidence(b, c.Op.ID) {
+		w.stats["release: a process survives the stop"]++
+		return nil
+	}
+	prefix := dataKey(h.Location, h.Gen, "")
+	remote := w.remoteMax(w.buckets[b.Region], prefix)
+	n, flushed := remote, false
+	if db := b.DB; db != nil && db.Inc == h.Inc && db.Gen == h.Gen {
+		if db.Epoch == b.Epoch && db.Session == h.Session {
+			if len(db.Pending) > 0 {
+				bl := w.deltaOf(db, db.Inc)
+				db.FirstFull = false
+				db.Queue = append(db.Queue, bl)
+				db.Pos, db.Pending = bl.Max, nil
+			}
+			w.ship(b)
+			if len(db.Queue) > 0 || db.InFlight != nil || remote < db.Pos {
+				w.stats["release: waits for the flush"]++
+				return nil
+			}
+			n, flushed = db.Pos, true
+		} else {
+			w.stats["release: the session's replicator is gone, unflushed"]++
+		}
+	}
+	// the files the box holds, or, when it holds none of this incarnation's
+	// (a failed target whose unopened install a scoped cleanup retired),
+	// the set its own installation applied: a release never invents a
+	// files identity
+	files := b.Files.clone()
+	if files == nil || files.Inc != h.Inc {
+		files = w.relocFiles(c).clone()
+	}
+	return &releaseEntry{Box: b.ID, Session: h.Session, Gen: h.Gen, FinalTX: n, Flushed: flushed,
+		Files: files, Timers: append([]int(nil), b.Timers...), At: w.now}
+}
+
+// pinSource is the generation the pin reads (StorePinner's genselect.Select
+// over the admitted chain): holder.generation when it holds an object or
+// the marker names it; else the baseline the recovery walk selects for an
+// unfinished run of cold admissions (claim rev 6.22 §6.2a), as a cold
+// admission would restore it. An unexplained empty generation refuses:
+// absence is never evidence (§5.9).
+func (w *world) pinSource(b *box, c *claim) (string, bool) {
+	h := c.Holder
+	loc := h.Location
+	if w.hasFiles(b, loc, h.Gen) {
+		return h.Gen, true
+	}
+	bg, _ := w.bucketGen(b, loc)
+	if bg == h.Gen {
+		return h.Gen, true
+	}
+	run, ok := w.unfinishedRun(c, bg)
+	if !ok {
+		return "", false
+	}
+	return w.runBaseline(b, c, run, bg)
+}
+
+// selectPin is StorePinner.Pin against the observation c: the source
+// generation and its listing's newest position N, after a release only
+// once N reaches the release's final_txid (rule reloc-pin-reaches-release),
+// and an empty listing only with evidence (ruling 15, rule
+// reloc-pin-evidenced-empty): a journaled release that flushed at 0, or a
+// holder that never admitted a writer; any other empty listing marks the
+// operation stuck for an operator. The pin carries the claim version it
+// was selected against (ruling 16, RecoveryPinKey). Task 4 adds the files
+// pin. It returns nil while the pin must wait.
+func (w *world) selectPin(b *box, c *claim) *pinEntry {
+	op, h := c.Op, c.Holder
+	src, ok := w.pinSource(b, c)
+	if !ok {
+		w.stats["pin: the source generation cannot be selected yet"]++
+		return nil
+	}
+	n := w.remoteMax(w.buckets[b.Region], dataKey(h.Location, src, ""))
+	r := op.Release
+	if r != nil && on("reloc-pin-reaches-release") && n < r.FinalTX {
+		w.stats["pin: waits for the release's final txid"]++
+		return nil
+	}
+	if n == 0 && on("reloc-pin-evidenced-empty") && !op.Resolved && h.Session != 0 && !(r != nil && r.Flushed && r.FinalTX == 0) {
+		w.markStuck(c, fmt.Sprintf("an empty listing of %q is no evidence of an empty database (session %d)", src, h.Session))
+		return nil
+	}
+	return &pinEntry{Gen: src, TX: n, ClaimVer: c.Ver, At: w.now, Files: w.relocFiles(c).clone(), Timers: append([]int(nil), w.relocTimers(c)...)}
+}
+
+// restoreUpTo restores generation gen of region r from its current
+// listing, capped at TXID upto: the newest current snapshot at or below
+// upto as the root, then the planner's rule (ltx.IsContiguous, highest
+// max, lowest min, higher level) over the current level-0 and level-1
+// files whose range ends at or below upto. It is §5.8's build from the
+// pinned recovery set: nothing past the pin is restored, and a listing
+// that does not reach upto refuses (nil), as a pin short of its release
+// would. It reads the bucket and writes nothing.
+func (w *world) restoreUpTo(r, inc int, loc, gen string, upto int) *localDB {
+	bk := w.buckets[r]
+	prefix := dataKey(loc, gen, "")
+	db := &localDB{Inc: inc, Loc: loc, Gen: gen, State: map[string]int{}}
+	var root *blob
+	for _, s := range w.currentLTX(bk, prefix, 9) {
+		if s.B.Max <= upto && (root == nil || s.B.Max > root.Max) {
+			root = s.B
+		}
+	}
+	cur := 0
+	var applied []*blob
+	if root != nil {
+		apply(db.State, root)
+		cur = root.Max
+		applied = append(applied, root)
+		db.Key = root.SealKey
+		if root.Inc != 0 {
+			db.Inc = root.Inc
+		}
+	}
+	var cands []*blob
+	for _, level := range []int{0, 1} {
+		for _, f := range w.currentLTX(bk, prefix, level) {
+			if f.B.Max <= upto {
+				cands = append(cands, f.B)
+			}
+		}
+	}
+	for cur < upto {
+		var best *blob
+		for _, f := range cands {
+			if f.Min <= cur+1 && f.Max > cur && (best == nil || f.Max > best.Max || f.Max == best.Max && (f.Min < best.Min || f.Min == best.Min && f.Level > best.Level)) {
+				best = f
+			}
+		}
+		if best == nil {
+			return nil // the listing does not reach upto: a gap, or objects still landing
+		}
+		apply(db.State, best)
+		cur = best.Max
+		applied = append(applied, best)
+		if db.Key == 0 {
+			db.Key = best.SealKey
+		}
+		if best.Inc != 0 {
+			db.Inc = best.Inc
+		}
+	}
+	db.Log = txsOf(applied...)
+	db.TX = w.lineageTX(applied...)
+	db.Pos = cur
+	return db
+}
+
+// relocFiles is the files directory the local install applies: the
+// pinned set's (the pin carries the files and wake state it was taken
+// with), else the release's (a drain, a nested relocation), else the
+// converted move's or the failover's stand-in for the files publisher
+// (moves §14.2.6). Task 4 puts the pinned manifest first.
+func (w *world) relocFiles(c *claim) *filesDir {
+	if p := c.Op.Pin; p != nil && p.Files != nil {
+		return p.Files
+	}
+	if r := c.Op.Release; r != nil && r.Files != nil {
+		return r.Files
+	}
+	return c.Op.StopFiles
+}
+
+// relocTimers is the wake state the local install replaces timers with.
+func (w *world) relocTimers(c *claim) []int {
+	if p := c.Op.Pin; p != nil && p.Files != nil {
+		return p.Timers
+	}
+	if r := c.Op.Release; r != nil {
+		return r.Timers
+	}
+	return nil
+}
+
+// nameReplacement names next as the operation's target in n, counting a
+// replacement when it replaces another box (replaceTargetSlot): the
+// replaced box is excluded for this host, and past maxReplacements the
+// operation is marked stuck at the current phase instead (rule
+// reloc-replacement-cap). Inside the CAS it refuses a box that owes a
+// park-local for the host (rule reloc-replace-not-owing, Task 3). It
+// reports whether next was named.
+func (w *world) nameReplacement(n *claim, next int, phase string) bool {
+	if on("reloc-replace-not-owing") {
+		if b := w.boxByID(next); b != nil && w.owesLocal(n, b) {
+			w.stats["replacement refused: the box owes a park-local"]++
+			return false
+		}
+	}
+	old := n.Op.Tgt
+	if old >= 0 && old != next {
+		if on("reloc-replacement-cap") && n.Op.Replacements >= maxReplacements {
+			n.Op.Stuck = fmt.Sprintf("two replacements of the target used; a third was needed at %s", n.Op.Phase)
+			w.stats["relocation stuck: replacement cap"]++
+			return false
+		}
+		n.Op.Replacements++
+		n.Op.Excluded = addUniq(n.Op.Excluded, old)
+		var parts []int
+		for _, p := range n.Op.Parts {
+			if p != old {
+				parts = append(parts, p)
+			}
+		}
+		n.Op.Parts = parts
+	}
+	n.Op.Tgt = next
+	n.Op.Parts = addUniq(n.Op.Parts, next)
+	n.Op.Phase = phase
+	return true
+}
+
+// markStuck is MarkStuck: a journal entry, never a phase; every relocation
+// step refuses afterwards until the operator resolves it. It never stops
+// an operation between installed and a probe while P is unopened: that
+// live target's safe point is its probe.
+func (w *world) markStuck(c *claim, why string) {
+	id := c.Op.ID
+	if w.cas(c, func(n *claim) bool {
+		if !sameOp(n.Op.ID, id) || n.Op.Kind != "relocating" || n.Op.Stuck != "" {
+			return false
+		}
+		if n.Op.Phase == "installed" && n.Op.Receipt != nil && !preparedOpened(n) {
+			return false
+		}
+		n.Op.Stuck = why
+		return true
+	}) {
+		w.alerts++
+		w.stats["relocation stuck"]++
+		w.logf("relocation %s stuck: %s", id, why)
+	}
+}
+
+// relocationLeftovers queues, inside the serving CAS (CompleteRelocation),
+// the park-local chore every abandoned installation owes (claim §4: "every
+// abandoned local installation receives an exact park-local"): the
+// source, when it is alive and its fence did not discharge it, and every
+// other box this operation handed op.exec to.
+func (w *world) relocationLeftovers(n *claim, op opState) {
+	owed := append([]int{op.Src}, op.InstalledOn...)
+	for _, id := range owed {
+		if id < 0 || id == op.Exec || contains(op.Discharged, id) {
+			continue
+		}
+		if b := w.boxByID(id); b == nil || w.owesLocal(n, b) {
+			continue
+		}
+		n.Obl = append(n.Obl, obligation{ID: w.newID("ob"), Op: op.ID, Kind: "park-local", Box: id, Region: -1, Ret: op.ID})
+	}
+}
+
+// relocStarting: the barrier (claim D6, requireAcks in ToReleasing). A
+// drain leaves starting for releasing once both participants' execution
+// leases are current (role() writes them on every read of the claim), and
+// the CAS records releasing_since for the release deadline; a failover
+// never enters starting in this model (it starts at pinning, Task 3). The
+// mutation of reloc-exec-ack-barrier moves on with no acknowledgement.
+func (w *world) relocStarting(b *box, c *claim) {
+	op := c.Op
+	if on("reloc-exec-ack-barrier") && !w.leasesSeen(c) {
+		return
+	}
+	w.cas(c, func(n *claim) bool {
+		if !sameOp(n.Op.ID, op.ID) || n.Op.Kind != "relocating" || n.Op.Phase != "starting" {
+			return false
+		}
+		n.Op.Phase, n.Op.ReleasingSince = "releasing", w.now
+		return true
+	})
+}
+
+// relocReleasing: the source runs the release sequence and journals it
+// (JournalRelease); then a worker's CAS (PinAfterRelease) cites the entry
+// and leaves for pinning with op.exec none and the stamp kept (claim
+// R6-4), once every participant has acknowledged (rule
+// reloc-ack-before-pinning: a target replaced in releasing acknowledges
+// before the operation leaves the phase; 1b-next rev 4 N6). A source that
+// has not journaled its release releaseDeadline after releasing began is
+// stuck (rule reloc-release-deadline, Worker.releaseOverdue): nothing
+// moves away from a live box without its stop evidence. The mutation of
+// reloc-release-first pins without the entry: the source is never
+// stopped.
+func (w *world) relocReleasing(b *box, c *claim) {
+	op := c.Op
+	if op.Release == nil {
+		if on("reloc-release-deadline") && w.now > op.ReleasingSince+releaseDeadline {
+			w.markStuck(c, fmt.Sprintf("box %d has not released the host %d steps after releasing", op.Exec, releaseDeadline))
+			return
+		}
+		if b.ID != op.Exec {
+			if !on("reloc-release-first") {
+				w.cas(c, func(n *claim) bool {
+					ok := sameOp(n.Op.ID, op.ID) && n.Op.Kind == "relocating" && n.Op.Phase == "releasing"
+					if ok {
+						n.Op.Phase, n.Op.Exec = "pinning", -1
+					}
+					return ok
+				})
+			}
+			return
+		}
+		r := w.relocRelease(b, c)
+		if r == nil {
+			return
+		}
+		if w.cas(c, func(n *claim) bool {
+			ok := sameOp(n.Op.ID, op.ID) && n.Op.Kind == "relocating" && n.Op.Phase == "releasing" && n.Op.Exec == b.ID && n.Op.Release == nil
+			if ok {
+				n.Op.Release = r
+			}
+			return ok
+		}) {
+			w.stats["release journaled: source"]++
+			w.logf("relocation %s: box %d released the host at TXID %d (flushed=%v)", op.ID, b.ID, r.FinalTX, r.Flushed)
+		}
+		return
+	}
+	if on("reloc-ack-before-pinning") && !w.leasesSeen(c) {
+		w.stats["pin after release: waits for the acknowledgements"]++
+		return
+	}
+	w.cas(c, func(n *claim) bool {
+		ok := sameOp(n.Op.ID, op.ID) && n.Op.Kind == "relocating" && n.Op.Phase == "releasing" && n.Op.Release != nil && n.Op.Release.Box == n.Op.Exec
+		if ok {
+			n.Op.Phase, n.Op.Exec = "pinning", -1
+		}
+		return ok
+	})
+}
+
+// relocPinning: a worker selects the pin against its observation and
+// journals it (JournalPin) in a CAS bound to that observation's claim
+// version (rule reloc-pin-claim-gen, ruling 16: a pin selected against an
+// older claim is abandoned, and the next pass selects afresh); a failover
+// pins no earlier than the fence's observed_at plus failoverPinDelay (rule
+// reloc-failover-pin-delay, a loss bound). Then it names a target when the
+// operation has none (NameTarget: a converted move, a resolved stuck
+// operation, a target lost with no spare); then, with every participant's
+// lease current (rule reloc-exec-ack-barrier), hands op.exec to the
+// target for a new installation (ToInstalling): a new stamp, journaled as
+// install_stamp, and a fresh prepared generation id (claim R6-4). The
+// target must owe no park-local for the host.
+func (w *world) relocPinning(b *box, c *claim) {
+	op, h := c.Op, c.Holder
+	if op.Pin == nil {
+		if op.Release == nil && on("reloc-failover-pin-delay") && w.now < op.FenceAt+failoverPinDelay {
+			return
+		}
+		pin := w.selectPin(b, c)
+		if pin == nil {
+			return
+		}
+		if w.cas(c, func(n *claim) bool {
+			ok := sameOp(n.Op.ID, op.ID) && n.Op.Kind == "relocating" && n.Op.Phase == "pinning" && n.Op.Pin == nil && n.Op.Stuck == ""
+			if ok && on("reloc-pin-claim-gen") && n.Ver != pin.ClaimVer {
+				w.stats["pin: selected against an older claim, abandoned"]++
+				ok = false
+			}
+			if ok {
+				n.Op.Pin = pin
+			}
+			return ok
+		}) {
+			w.logf("relocation %s: pinned %q at TXID %d (selected against claim version %d)", op.ID, pin.Gen, pin.TX, pin.ClaimVer)
+		}
+		return
+	}
+	if op.Tgt < 0 {
+		to := w.chooseBoxExcept(op.SrcRegion, h.App, relocExcept(op)...)
+		if to == nil {
+			return // no eligible box: the recovery pass alerts once (moves §7.10)
+		}
+		w.cas(c, func(n *claim) bool {
+			ok := sameOp(n.Op.ID, op.ID) && n.Op.Kind == "relocating" && n.Op.Phase == "pinning" && n.Op.Tgt < 0
+			if ok {
+				ok = w.nameReplacement(n, to.ID, "pinning")
+			}
+			return ok
+		})
+		return
+	}
+	if on("reloc-exec-ack-barrier") && !w.leasesSeen(c) {
+		return
+	}
+	to := op.Tgt
+	if w.cas(c, func(n *claim) bool {
+		if !sameOp(n.Op.ID, op.ID) || n.Op.Kind != "relocating" || n.Op.Phase != "pinning" || n.Op.Tgt != to || n.Op.Pin == nil || n.Op.Stuck != "" || contains(n.Lost, to) {
+			return false
+		}
+		if t := w.boxByID(to); t == nil || w.owesLocal(n, t) {
+			return false
+		}
+		w.handExec(n, to, "installing", w.newID("P"))
+		n.Op.BaseKey, n.Op.BaseVer, n.Op.BaseTX = "", 0, 0
+		return true
+	}) {
+		w.logf("relocation %s: box %d installs with stamp %d", op.ID, to, w.claim.Holder.Stamp)
+	}
+}
+
+// handExec is install() in hostclaim: op.exec to box at phase with
+// prepared generation P, a new stamp (this CAS's), journaled as
+// install_stamp, no receipt, the probe attempts reset for the new
+// executor (BeginProbeAttempt counts per box), and the box noted as owing
+// a park-local should it be abandoned.
+func (w *world) handExec(n *claim, box int, phase, prepared string) {
+	n.Op.Exec, n.Op.Phase, n.Op.Prepared = box, phase, prepared
+	n.Holder.Stamp = w.issueStamp(n, box)
+	n.Op.InstallStamp = n.Holder.Stamp
+	if on("reloc-install-receipt") {
+		n.Op.Receipt = nil
+	}
+	n.Op.Attempts = 0
+	n.Op.InstalledOn = addUniq(n.Op.InstalledOn, box)
+	n.Boxes = addUniq(n.Boxes, box)
+}
+
+// relocInstalling: the target builds P, the remote prepared generation,
+// exactly as a landing builds its generation (moves §7.6, L16): the
+// snapshot [1, N] of the pinned generation, create-only and acknowledged,
+// then the level-0 anchor [N, N], acknowledged, then the installed CAS
+// (ToInstalled, R7-4). A pin at N = 0 builds nothing: the probe is an
+// empty bootstrap (claim P6-D3). Only op.exec installs (rule
+// reloc-exec-only-installs, HA2: being in the region is never enough).
+func (w *world) relocInstalling(b *box, c *claim) {
+	op, h := c.Op, c.Holder
+	if on("reloc-exec-only-installs") && op.Exec != b.ID {
+		return
+	}
+	loc, g := h.Location, op.Prepared
+	bk := w.buckets[b.Region]
+	installed := func(n *claim) bool {
+		ok := sameOp(n.Op.ID, op.ID) && n.Op.Kind == "relocating" && n.Op.Phase == "installing" && n.Op.Exec == op.Exec && n.Op.Prepared == g
+		if ok {
+			n.Op.Phase = "installed"
+		}
+		return ok
+	}
+	if !w.buildPreparedFiles(b, c) {
+		return // Task 4: P's prepared files manifest first
+	}
+	if op.Pin.TX == 0 {
+		w.cas(c, installed)
+		return
+	}
+	if op.BaseKey == "" {
+		db := w.restoreUpTo(b.Region, h.Inc, loc, op.Pin.Gen, op.Pin.TX)
+		if db == nil || db.Pos != op.Pin.TX {
+			w.stats["build: the pinned set cannot be restored yet"]++
+			return
+		}
+		key := snapKey(loc, g, op.Pin.TX)
+		if !w.ackedPut(b, key, snapshotOf(db, h.Inc), true) {
+			return
+		}
+		v := bk.current(key)
+		if v == nil {
+			return
+		}
+		w.cas(c, func(n *claim) bool {
+			ok := sameOp(n.Op.ID, op.ID) && n.Op.Kind == "relocating" && n.Op.Phase == "installing" && n.Op.Exec == op.Exec && n.Op.Prepared == g && n.Op.BaseKey == ""
+			if ok {
+				n.Op.BaseKey, n.Op.BaseVer, n.Op.BaseTX = key, v.ID, op.Pin.TX
+			}
+			return ok
+		})
+		return
+	}
+	if !w.anchorAcked(b, loc, g, op.BaseKey, op.BaseVer, op.BaseTX) {
+		return
+	}
+	if w.cas(c, installed) {
+		w.logf("relocation %s: P %q built on box %d at TXID %d", op.ID, g, b.ID, op.BaseTX)
+	}
+}
+
+// buildPreparedFiles is Task 4's prepared files manifest; before it, the
+// build has nothing to write for files.
+func (w *world) buildPreparedFiles(b *box, c *claim) bool { return true }
+
+// localInstall advances the executor's local install by one step (§5.8,
+// B1-2; 1b-next Task 8c's Install) and reports whether it is whole: park
+// what an earlier stay left as retire-artifacts of its stamp (claim §6.4),
+// extract the files, replace the timers with the pinned wake state (the
+// files Done marker last), render and materialize with current inputs,
+// and write the box's install journal (its receipt) under install_stamp.
+// EnsureLocal reuses it to restore a retired install under the same
+// stamp.
+func (w *world) localInstall(b *box, c *claim) bool {
+	op, h := c.Op, c.Holder
+	g := op.Prepared
+	if b.Files == nil || b.Files.Gen != g {
+		for _, st := range []int{dbStamp(b.DB), filesStamp(b.Files)} {
+			if st != 0 && st != b.stampOf(h.Inc) {
+				w.retireArtifacts(b, h.Inc, st)
+			}
+		}
+		if b.DB != nil {
+			b.DB = nil // never reused (claim R6); the probe's admission restores
+			b.Parked++
+		}
+		src := w.relocFiles(c)
+		if src == nil {
+			w.nextID++
+			src = &filesDir{Inc: h.Inc, Key: w.nextID, Env: w.nextID}
+		}
+		f := src.clone()
+		f.Inc, f.Gen, f.Done, f.Stamp = h.Inc, g, false, b.stampOf(h.Inc)
+		if !on("markers-last") {
+			f.Done = true
+		}
+		b.Files = f
+		b.pendingTimers = append([]int(nil), w.relocTimers(c)...)
+		return false
+	}
+	if !b.Files.Done {
+		b.Timers = append([]int(nil), b.pendingTimers...) // ReplaceTimers: the pinned wake state
+		b.Attempt, b.History = 0, nil
+		b.Files.Done = true
+		b.installEpoch = b.Epoch
+		return false
+	}
+	if b.HasKey {
+		b.Config, b.CfgVer = h.Inc, w.cfgVer[h.App]
+	}
+	b.Live, b.LiveInc = h.App, h.Inc
+	b.receipt = &receiptEntry{Op: op.ID, Box: b.ID, Stamp: op.InstallStamp}
+	return true
+}
+
+// relocInstalled: the executor's local install, then its receipt by CAS
+// (RecordLocalInstall), bound to this box and install_stamp; probing
+// needs that exact receipt (ToProbing; rule reloc-install-receipt), and
+// the install is verified, and restored if a lost lease's scoped cleanup
+// retired it, before the probing CAS (EnsureLocal; rule
+// reloc-ensure-local). The mutation of reloc-install-receipt lets a
+// replacement inherit its predecessor's receipt and skip its install.
+func (w *world) relocInstalled(b *box, c *claim) {
+	op := c.Op
+	if on("reloc-exec-only-installs") && op.Exec != b.ID {
+		return
+	}
+	probing := func(n *claim) bool {
+		ok := sameOp(n.Op.ID, op.ID) && n.Op.Kind == "relocating" && n.Op.Phase == "installed" && n.Op.Exec == op.Exec && n.Op.Receipt != nil
+		if ok {
+			n.Op.Phase, n.Op.ProbingSince = "probing", w.now
+		}
+		return ok
+	}
+	if r := op.Receipt; r != nil {
+		mine := r.Box == b.ID && r.Stamp == op.InstallStamp
+		if !mine && !on("reloc-install-receipt") {
+			w.cas(c, probing) // the mutation: any receipt will do, the install is skipped
+			return
+		}
+		if mine {
+			if w.ensureLocal(b, c) {
+				w.cas(c, probing)
+			}
+			return
+		}
+	}
+	if op.Exec != b.ID || !w.localInstall(b, c) {
+		return
+	}
+	w.cas(c, func(n *claim) bool {
+		ok := sameOp(n.Op.ID, op.ID) && n.Op.Kind == "relocating" && n.Op.Phase == "installed" && n.Op.Exec == b.ID && n.Op.InstallStamp == op.InstallStamp && !preparedOpened(n)
+		if ok {
+			n.Op.Receipt = &receiptEntry{Op: op.ID, Box: b.ID, Stamp: op.InstallStamp}
+		}
+		return ok
+	})
+}
+
+// ensureLocal is EnsureLocal (1b-next rev 15 finding 2): before P's first
+// admission the executor's local install must be whole, so it is
+// verified before the probing CAS and before every attempt, and a
+// retired one (the scoped cleanup of a lost controller lease retires an
+// unopened P's local install, role()) is restored under the same
+// install_stamp. It never touches an opened P. It reports whether the
+// install is whole now. The mutation goes on without verifying, so P's
+// first admission can meet a missing install.
+func (w *world) ensureLocal(b *box, c *claim) bool {
+	op := c.Op
+	if preparedOpened(c) || !on("reloc-ensure-local") {
+		return true
+	}
+	if b.Files != nil && b.Files.Gen == op.Prepared && b.Files.Done && b.receipt != nil && b.receipt.Op == op.ID && b.receipt.Stamp == op.InstallStamp {
+		return true
+	}
+	if w.localInstall(b, c) {
+		w.stats["local install restored before the first admission"]++
+		w.logf("relocation %s: box %d restored its retired local install under stamp %d", op.ID, b.ID, op.InstallStamp)
+		return true
+	}
+	return false
+}
+
+// verifyReceipt is VerifyReceipt (1b-next rev 16 finding 1): once P is
+// opened the local install is never remade, and before every attempt the
+// box's durable receipt (its install journal) must still be the one the
+// claim journaled; a missing or different one marks the operation stuck
+// and nothing is admitted. Files, env and timers the admitted writers
+// changed are never compared. The mutation goes on to the next attempt.
+func (w *world) verifyReceipt(b *box, c *claim) bool {
+	op := c.Op
+	if r := b.receipt; r != nil && r.Op == op.ID && r.Box == b.ID && r.Stamp == op.InstallStamp {
+		return true
+	}
+	if !on("reloc-verify-receipt") {
+		w.stats["receipt missing after P opened, attempt made anyway (mutation)"]++
+		return true
+	}
+	w.markStuck(c, fmt.Sprintf("box %d's local install receipt is missing after P was admitted", b.ID))
+	return false
+}
+
+// preparedOpened is PreparedOpened: an admission has named P (B2-5). The
+// admission that opens P journals prepared_opened in the same CAS
+// (admitCommit), so the fact outlives holder.admissions' trim to eight
+// (1b-next rev 12 S1; rule reloc-prepared-opened-journal); the mutation
+// reads the retained admissions alone, as rev 11 did.
+func preparedOpened(c *claim) bool {
+	if c.Op.Prepared == "" || c.Holder == nil {
+		return false
+	}
+	if on("reloc-prepared-opened-journal") && c.Op.PreparedOpened == c.Op.Prepared {
+		return true
+	}
+	for _, e := range c.Holder.Admissions {
+		if e.Gen == c.Op.Prepared {
+			return true
+		}
+	}
+	return false
+}
+
+// relocProbing: each attempt is counted in the claim before it is made
+// (BeginProbeAttempt, ruling 19; rule reloc-probe-attempts: a crash, a
+// lost response or a restart never buys a fourth), then one cold
+// AdmitWriter by op.exec into P (the first) or a fresh generation
+// restored from the previous attempt's (claim §6.4a; spawn and admitWriter
+// do both), then the probe. The fourth is refused and the target enters
+// probe-failed, as it does past the probe deadline. Before P's first
+// admission the local install is verified and restored (ensureLocal);
+// after it, the receipt alone is verified (verifyReceipt) and the install
+// is never remade (rule reloc-no-reinstall; its mutation reapplies the
+// pinned wake state on every agent restart, as rev 4.2's install marker
+// did, over the timers the admitted session registered).
+func (w *world) relocProbing(b *box, c *claim) {
+	op, h := c.Op, c.Holder
+	failed := func(n *claim) bool {
+		ok := sameOp(n.Op.ID, op.ID) && n.Op.Kind == "relocating" && n.Op.Phase == "probing" && n.Op.Exec == op.Exec
+		if ok {
+			n.Op.Phase, n.Op.FailedAt, n.Op.Release = "probe-failed", w.now, nil
+		}
+		return ok
+	}
+	if op.Exec != b.ID {
+		if w.now > op.ProbingSince+probeDeadline && op.Exec >= 0 {
+			w.stats["probe-failed: deadline"]++
+			w.cas(c, failed) // the worker's: ToProbeFailed past the probe deadline
+		}
+		return
+	}
+	if b.Row == nil || b.Row.Status == "ready" {
+		w.holdRow(b, "relocating", op.ID, c)
+	}
+	opened := preparedOpened(c)
+	if !opened {
+		if !w.ensureLocal(b, c) {
+			return
+		}
+	} else if !w.verifyReceipt(b, c) {
+		return
+	}
+	if !on("reloc-no-reinstall") && opened && b.installEpoch != b.Epoch {
+		b.Timers = append([]int(nil), w.relocTimers(c)...) // the mutation: the install marker re-applied after a restart
+		b.installEpoch = b.Epoch
+		w.stats["local install remade after admission (mutation)"]++
+	}
+	if !w.admits(b, c, op.ID) {
+		return
+	}
+	if b.HasKey {
+		b.Config, b.CfgVer, b.Live, b.LiveInc = h.Inc, w.cfgVer[h.App], h.App, h.Inc
+	}
+	probed := func(n *claim) bool {
+		ok := sameOp(n.Op.ID, op.ID) && n.Op.Phase == "probing" && n.Op.Exec == b.ID
+		if ok {
+			n.Op.Phase = "probed"
+		}
+		return ok
+	}
+	if hasMain(b) {
+		w.probeAccepted(b, c)
+		w.cas(c, probed)
+		return
+	}
+	if w.now > op.ProbingSince+probeDeadline {
+		w.stats["probe-failed: deadline"]++
+		w.cas(c, failed)
+		return
+	}
+	tag := fmt.Sprintf("%s/%d", op.ID, op.Attempts)
+	if b.open == nil {
+		// a new attempt: counted before it is made. attemptTag is the
+		// attempt this agent counted (tag) or made (tag+"+"); one made and
+		// ended, or none counted, is counted now
+		if on("reloc-probe-attempts") && b.attemptTag != tag {
+			if op.Attempts >= probeTries {
+				w.stats["probe-failed: attempts"]++
+				w.cas(c, failed)
+				return
+			}
+			if w.cas(c, func(n *claim) bool {
+				ok := sameOp(n.Op.ID, op.ID) && n.Op.Phase == "probing" && n.Op.Exec == b.ID && n.Op.Attempts == op.Attempts
+				if ok {
+					n.Op.Attempts++
+				}
+				return ok
+			}) {
+				b.attemptTag = fmt.Sprintf("%s/%d", op.ID, op.Attempts+1)
+			}
+			return
+		}
+		if !on("reloc-probe-attempts") && op.ProbeTries >= probeTries {
+			w.stats["probe-failed: attempts"]++
+			w.cas(c, failed) // the mutation: failures counted after the fact, as rev 1 did
+			return
+		}
+	}
+	if b.open == nil {
+		b.attemptTag = tag + "+" // made now
+	}
+	if w.spawn(b, c, op.Prepared, true) {
+		w.probeAccepted(b, c)
+		w.cas(c, probed)
+	}
+}
+
+// relocProbeFailed: the live target runs its own release sequence (§5.8
+// probe-failed; JournalRelease), then a worker starts the nested
+// relocation from pinning (PinAfterRelease with a next target), pinned to
+// at least the target's final TXID (the release entry, which
+// relocPinning reads), the failed target excluded and counted as a
+// replacement. Exhaustion is checked before a replacement is looked for
+// (1b-next R1-16): with the replacements used the operation is stuck. A
+// target that cannot finish its release within releaseDeadline goes to
+// stuck (ruling 14): nothing moves away from a live box without its stop
+// evidence. With no eligible box for releaseDeadline the operation is
+// stuck too (model ruling 14: 1b-next waits for a spare with no bound,
+// and in a two-box region the source is never a spare).
+func (w *world) relocProbeFailed(b *box, c *claim) {
+	op, h := c.Op, c.Holder
+	if op.Release == nil || op.Release.Box != op.Exec {
+		if on("reloc-release-deadline") && w.now > op.FailedAt+releaseDeadline {
+			w.markStuck(c, fmt.Sprintf("box %d cannot finish its release sequence", op.Exec))
+			return
+		}
+		if b.ID != op.Exec {
+			return
+		}
+		r := w.relocRelease(b, c)
+		if r == nil {
+			return
+		}
+		if w.cas(c, func(n *claim) bool {
+			ok := sameOp(n.Op.ID, op.ID) && n.Op.Kind == "relocating" && n.Op.Phase == "probe-failed" && n.Op.Exec == b.ID && (n.Op.Release == nil || n.Op.Release.Box != b.ID)
+			if ok {
+				n.Op.Release = r
+			}
+			return ok
+		}) {
+			w.stats["release journaled: failed target"]++
+		}
+		return
+	}
+	if on("reloc-replacement-cap") && op.Replacements >= maxReplacements {
+		w.markStuck(c, fmt.Sprintf("two replacements of the target used; a third was needed at %s", op.Phase))
+		return
+	}
+	next := w.chooseBoxExcept(op.SrcRegion, h.App, relocExcept(op, op.Exec)...)
+	if next == nil {
+		if w.now > op.FailedAt+releaseDeadline {
+			w.markStuck(c, "no eligible box for the nested relocation")
+		}
+		return
+	}
+	w.cas(c, func(n *claim) bool {
+		if !sameOp(n.Op.ID, op.ID) || n.Op.Kind != "relocating" || n.Op.Phase != "probe-failed" || n.Op.Release == nil || n.Op.Release.Box != n.Op.Exec {
+			return false
+		}
+		if !w.nameReplacement(n, next.ID, "pinning") {
+			return n.Op.Stuck != "" // stuck: the CAS records it
+		}
+		n.Op.Exec = -1
+		n.Op.Pin, n.Op.Prepared, n.Op.Receipt = nil, "", nil
+		n.Op.BaseKey, n.Op.BaseVer, n.Op.BaseTX = "", 0, 0
+		n.Op.ProbeTries, n.Op.Attempts = 0, 0
+		w.stats["nested relocation after probe-failed"]++
+		return true
+	})
+}
+
+// relocSettle is the settle window and the open (rev 7.20's steps, kept):
+// a probe that died in its window is restarted, cold, from its own
+// generation; then the row opens and the operation is released to
+// serving (CompleteRelocation), where the leftovers' park-local chores
+// are queued (release()).
+func (w *world) relocSettle(b *box, c *claim) {
+	op := c.Op
+	if op.Exec != b.ID {
+		return
+	}
+	switch op.Phase {
+	case "probed":
+		if b.open != nil {
+			return
+		}
+		if !hasMain(b) {
+			w.stats["probe restarted"]++
+			w.cas(c, func(n *claim) bool {
+				ok := sameOp(n.Op.ID, op.ID) && n.Op.Phase == "probed"
+				if ok {
+					n.Op.Phase = "probing"
+				}
+				return ok
+			})
+			return
+		}
+		if w.openRow(b, op.ID) {
+			w.cas(c, func(n *claim) bool {
+				ok := sameOp(n.Op.ID, op.ID) && n.Op.Phase == "probed"
+				if ok {
+					n.Op.Phase = "opened"
+				}
+				return ok
+			})
+		}
+	case "opened":
+		w.release(c, b.ID) // outstanding disjoint parks do not block serving (claim rev 6.28 §4)
+	}
+}
+
+// scopedCleanup is the relocation controller's scoped cleanup when its
+// lease was lost (1b-next rev 14 finding 1, Task 7's live): an unopened
+// P's local install is retired and its receipt (the install journal)
+// kept, so EnsureLocal restores it before the first admission. role()
+// calls it when the executor's execution lease expired before it renewed
+// it (a freeze, a pause, a partition longer than the TTL).
+func (w *world) scopedCleanup(b *box, c *claim) {
+	if c == nil || c.Holder == nil || c.Op.Kind != "relocating" || c.Op.Exec != b.ID || preparedOpened(c) {
+		return
+	}
+	if f := b.Files; f != nil && f.Gen == c.Op.Prepared && f.Gen != "" {
+		w.retireArtifacts(b, c.Holder.Inc, f.Stamp)
+		w.stats["relocation controller lost: unopened local install retired"]++
+		w.logf("box %d: relocation %s's controller lease was lost; the scoped cleanup retired its unopened local install", b.ID, c.Op.ID)
+	}
+}
+
+// twoBoxStep is the two-box shape's extra step: a drain now and then
+// during the chaos (Task 3 adds termination, enrollment and replacement
+// launches). It draws only in the two-box shape.
+func (w *world) twoBoxStep() {
+	if !w.calm && w.rng.Intn(60) == 0 {
+		w.userRelocate()
+	}
+}
diff --git a/internal/sim/hostlife/regionha_witness_test.go b/internal/sim/hostlife/regionha_witness_test.go
new file mode 100644
index 0000000..82ffbce
--- /dev/null
+++ b/internal/sim/hostlife/regionha_witness_test.go
@@ -0,0 +1,53 @@
+package hostlife
+
+import "testing"
+
+// twoBoxWitness is newWitness with a second enrolled box in every region.
+func twoBoxWitness() *world {
+	w := newWitness()
+	w.perRegion = 2
+	for r := 0; r < nRegions; r++ {
+		w.addBox(r)
+	}
+	return w
+}
+
+// TestDrainEndToEnd: a serving host is drained from box 0 to box 3 in
+// region 0 through every phase of §5.8's table; the host serves on box 3
+// with every acknowledged write and timer, box 0's installation is
+// retired by its park-local, and the first probe admission's coverage is
+// released (no writes_lost declared, L9).
+func TestDrainEndToEnd(t *testing.T) {
+	w := twoBoxWitness()
+	from, to := w.boxes[0], w.boxes[3]
+	w.serve(from, 1, app0)
+	w.reach(t, 50, "the host runs on box 0", func() bool { return hasMain(from) }, w.actAll(), func() { w.wake(from) })
+	w.appWrite(from)
+	w.nextW++
+	from.Timers = append(from.Timers, w.nextW)
+	w.acks = append(w.acks, ack{W: w.nextW, Inc: 1, Box: from.ID, Session: w.claim.Holder.Session, At: w.now, Kind: "timer"})
+	w.userRelocate()
+	if c := w.claim; c.Op.Kind != "relocating" || c.Op.Src != from.ID || c.Op.Tgt != to.ID || c.Op.Phase != "starting" {
+		t.Fatalf("the drain did not start: %s", w.state())
+	}
+	seen := map[string]bool{}
+	w.reach(t, 1500, "serving on box 3", func() bool {
+		seen[w.claim.Op.Phase] = true
+		return w.claim.Op.Kind == "serving" && w.claim.Op.Exec == to.ID
+	}, w.actAll(), w.recoveryPass, func() { w.wake(to) })
+	for _, p := range []string{"starting", "releasing", "pinning", "installing", "installed", "probing", "probed", "opened"} {
+		if !seen[p] {
+			t.Errorf("phase %s never observed", p)
+		}
+	}
+	if w.stats["admissions covered: released"] != 1 || w.stats["writes_lost declared"] != 0 {
+		t.Errorf("released coverage: %d released, %d writes_lost (want 1 and 0)", w.stats["admissions covered: released"], w.stats["writes_lost declared"])
+	}
+	w.finish(t)
+	if len(w.violations) > 0 {
+		t.Fatalf("%s", w.violations[0])
+	}
+	if from.DB != nil || from.Files != nil || from.Row != nil {
+		t.Errorf("box 0 still holds local state after its park-local: db=%v files=%v row=%v", from.DB != nil, from.Files != nil, from.Row)
+	}
+}
diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go
index a4f337d..545acad 100644
--- a/internal/sim/hostlife/rules_test.go
+++ b/internal/sim/hostlife/rules_test.go
@@ -145,5 +145,27 @@ var allRules = []string{
 	"config-before-probe",       // L3 (the kpmg outage)
 	"recovery-current-inputs",   // rev 6 §7.7 (J2-R2-5): a recovery probe is not bound to the move's pinned inputs
 	// region HA (two boxes per region, L18)
-	"create-choice-once", // region HA §5.2, claim P5-D2/P5-D6: the create's executor is chosen once and recorded in the intent; recovery never substitutes, it cancels a create whose box is gone
+	"create-choice-once",        // region HA §5.2, claim P5-D2/P5-D6: the create's executor is chosen once and recorded in the intent; recovery never substitutes, it cancels a create whose box is gone
+	"reloc-start-guard",         // region HA §5.8, claim §4 CC11 as L11 amends it (plan 1b-next RelocationStartGuard): a park-generation in the region never blocks a relocation start; a park-replica in the region and a park-local on the target or a live source do
+	"reloc-exec-ack-barrier",    // claim D6, region HA §5.8 (requireAcks): every participant's execution lease is current before the operation leaves starting or hands op.exec to the target
+	"reloc-release-first",       // region HA §5.8 releasing, A3-2 (PinAfterRelease): pinning cites the source's journaled release; the mutation pins while the source still runs
+	"reloc-pin-reaches-release", // region HA §5.8 (JournalPin): a pin after a release reaches its final_txid; the mutation pins the listing as it stands
+	"reloc-failover-pin-delay",  // region HA §5.8 (JournalPin, FailoverPinDelay): a failover pins no earlier than the fence's observed_at plus 30 s; a loss bound, not a safety bound (expected miss)
+	"reloc-exec-only-installs",  // region HA §5.8 Exclusion, HA2: only op.exec builds P and makes the local install; the mutation lets every box of the region materialize
+	"reloc-install-receipt",     // region HA §5.8 B1-2 (RecordLocalInstall, ToProbing): probing needs a receipt for exactly op.exec and install_stamp; the mutation lets a replacement inherit its predecessor's and skip its install
+	"reloc-no-reinstall",        // region HA §5.8 B2-5 (RecordLocalInstall after preparedOpened): after P's first admission the local install is never remade; the mutation reapplies the pinned wake state on every agent restart
+	"reloc-released-coverage",   // claim §6.4a item 2, L9 (AdmitWriter): released only on the admission opening P whose predecessor is exactly the flushed release's box and session and whose pin reached final_txid; the mutation grants it to every first opening of P, a failover's included
+	"reloc-row-cases",           // region HA §5.3, L12 (hostbox.RelocationRow): the former executor's row is held once its admission fence closed; the mutation reopens it as a stale hold (an admission fence: caught with exec-admission and its partners)
+	"reloc-replacement-cap",     // region HA §5.8 (replaceTargetSlot, MaxTargetReplacements): a third replacement of the target marks the operation stuck; an operator bound (expected miss)
+	"reloc-enrolled-only",       // region HA §2, HA7 (eligibleBoxes): an unenrolled reference is never chosen as a target; Task 3 gives it its witness
+	// plan 1b-next rev 16's additions to the phase table (rev 2 of this plan)
+	"reloc-drain-needs-writer",      // 1b-next ruling 11 (Worker.Start): a host that never admitted a writer is never drained, only failed over; liveness (expected miss)
+	"reloc-ack-before-pinning",      // 1b-next rev 4 N6 (PinAfterRelease requires requireAcks from releasing): a target replaced in releasing acknowledges before the operation leaves the phase; defence in depth (expected miss)
+	"reloc-pin-claim-gen",           // 1b-next ruling 16 (JournalPin, RecoveryPinKey pin-<gen>.json): a pin is journaled only against the claim version it was selected against; the mutation journals a pin selected before a nested reset
+	"reloc-pin-evidenced-empty",     // 1b-next ruling 15 (JournalPin, StorePinner's Empty evidence): an empty pin needs a release flushed at 0 or a holder that never had a writer; otherwise stuck for an operator (expected miss: the model's listings are exact and the probe declares)
+	"reloc-release-deadline",        // 1b-next ruling 14 (Worker.releaseOverdue, ReleaseDeadline): a release not journaled 10 minutes after releasing or probe-failed began marks the operation stuck; the mutation waits forever (INV-3)
+	"reloc-probe-attempts",          // 1b-next ruling 19 (BeginProbeAttempt, MaxProbeAttempts): each probe attempt is counted in the claim before it is made, the fourth is probe-failed; liveness (expected miss)
+	"reloc-ensure-local",            // 1b-next rev 15 finding 2 (Effects.EnsureLocal): before P's first admission the local install is verified, and restored under the same install_stamp if a lost lease's scoped cleanup retired it; the mutation admits over a missing install
+	"reloc-verify-receipt",          // 1b-next rev 16 finding 1 (Effects.VerifyReceipt, MarkStuck in probing): after P opens, a missing or different receipt marks the operation stuck before any further admission; the mutation makes the attempt anyway
+	"reloc-prepared-opened-journal", // 1b-next rev 12 S1 (prepared_opened, PreparedOpened): P's opening is journaled with its admission and outlives holder.admissions' trim; the mutation reads the trimmed list and remakes the install after P opened
 }
diff --git a/internal/sim/hostlife/sim_test.go b/internal/sim/hostlife/sim_test.go
index fbe5f8e..92813d5 100644
--- a/internal/sim/hostlife/sim_test.go
+++ b/internal/sim/hostlife/sim_test.go
@@ -27,7 +27,7 @@ func newWorld(seed int64, verbose bool) *world {
 		w.fail[f] = w.rng.Intn(2) == 0
 	}
 	for r := 0; r < nRegions; r++ {
-		b := &box{ID: r, Region: r, HasKey: r == 0 || w.rng.Intn(4) != 0, Skew: w.rng.Intn(3) - 1, Nested: w.rng.Intn(2) == 0}
+		b := &box{ID: r, Region: r, HasKey: r == 0 || w.rng.Intn(4) != 0, Skew: w.rng.Intn(3) - 1, Nested: w.rng.Intn(2) == 0, Enrolled: true}
 		if r != 0 && w.rng.Intn(4) == 0 {
 			b.FailApp = true
 		}
@@ -49,7 +49,7 @@ func newWorld(seed int64, verbose bool) *world {
 	// region, drawn after every one-box draw of this world, so the one-box
 	// stream is untouched; id nRegions+r, as addBox gives a witness
 	for r := 0; r < nRegions && w.perRegion > 1; r++ {
-		b := &box{ID: nRegions + r, Region: r, HasKey: w.rng.Intn(4) != 0, Skew: w.rng.Intn(3) - 1, Nested: w.rng.Intn(2) == 0}
+		b := &box{ID: nRegions + r, Region: r, HasKey: w.rng.Intn(4) != 0, Skew: w.rng.Intn(3) - 1, Nested: w.rng.Intn(2) == 0, Enrolled: true}
 		if w.rng.Intn(4) == 0 {
 			b.FailApp = true
 		}
@@ -149,6 +149,9 @@ func (w *world) step() {
 		}
 	}
 	w.runStalled()
+	if w.perRegion > 1 {
+		w.twoBoxStep() // the two-box shape's own draws, after the one-box ones (ruling 1)
+	}
 	bs := w.liveBoxes()
 	b := bs[w.rng.Intn(len(bs))]
 	n := w.rng.Intn(100)
@@ -388,6 +391,14 @@ func (w *world) checkStep() {
 	if c := w.claim; c != nil && c.Op.Kind == "reverting" && c.Op.RevPhase == "stuck" {
 		w.violate("stuck: source could not revert %s", c.Op.ID)
 	}
+	// INV-27 (region HA HA1, HA7): while relocating, op.exec is none or an
+	// enrolled box that is not on lost; execution authority never names a
+	// fenced or unenrolled reference
+	if c := w.claim; c != nil && c.Op.Kind == "relocating" && c.Op.Exec >= 0 {
+		if e := w.boxByID(c.Op.Exec); e == nil || !e.Enrolled || contains(c.Lost, e.ID) {
+			w.violate("INV-27: relocation %s names box %d as op.exec, which is unenrolled or lost", c.Op.ID, c.Op.Exec)
+		}
+	}
 }
 
 func (w *world) boxesState() string {
diff --git a/internal/sim/hostlife/twobox_test.go b/internal/sim/hostlife/twobox_test.go
index 5b6de60..e54a6cf 100644
--- a/internal/sim/hostlife/twobox_test.go
+++ b/internal/sim/hostlife/twobox_test.go
@@ -40,7 +40,7 @@ func (w *world) regionBoxes(r int) []*box {
 // key held, no faults, id nRegions+r (the sweep's second boxes carry the
 // same ids; replacements are 100 and up).
 func (w *world) addBox(r int) *box {
-	b := &box{ID: nRegions + r, Region: r, HasKey: true}
+	b := &box{ID: nRegions + r, Region: r, HasKey: true, Enrolled: true, DeleteOnTermination: true}
 	b.forget()
 	w.boxes = append(w.boxes, b)
 	w.logf("witness: box %d enrolled in region %d", b.ID, r)
@@ -87,17 +87,23 @@ func (w *world) owesLocal(c *claim, b *box) bool {
 }
 
 // chooseBox is region HA §5.2's choose() (H12, L8; a move's target under
-// L15): among the eligible boxes of region r (§2: live, running the
-// claim's executable, holding the secrets key, not on lost, not owing a
-// park-local for the host), prefer one running no instance of app, then
-// the fewest hosts, then the greatest tieHash. With one box in the region
-// it is that box, as today (spec §4). It is a pure function of the world;
-// the caller records the choice in the claim's intent and never
+// L15) with nothing excluded.
+func (w *world) chooseBox(r int, app string) *box { return w.chooseBoxExcept(r, app) }
+
+// chooseBoxExcept is choose() over the region's eligible boxes minus
+// except (a relocation's source, its replaced targets): among the
+// eligible boxes of region r (§2: live, running the claim's executable,
+// holding the secrets key, not on lost, not owing a park-local for the
+// host, enrolled: an unenrolled reference is never eligible, HA7; rule
+// reloc-enrolled-only, Task 3), prefer one running no instance of app,
+// then the fewest hosts, then the greatest tieHash. With one box in the
+// region it is that box, as today (spec §4). It is a pure function of the
+// world; the caller records the choice in the claim's intent and never
 // substitutes (rule create-choice-once).
-func (w *world) chooseBox(r int, app string) *box {
+func (w *world) chooseBoxExcept(r int, app string, except ...int) *box {
 	bs := w.regionBoxes(r)
 	if len(bs) <= 1 {
-		if len(bs) == 0 {
+		if len(bs) == 0 || contains(except, bs[0].ID) {
 			return nil
 		}
 		return bs[0]
@@ -106,7 +112,10 @@ func (w *world) chooseBox(r int, app string) *box {
 	var best *box
 	var bestKey [3]int
 	for _, b := range bs {
-		if b.Old || !b.HasKey || (c != nil && contains(c.Lost, b.ID)) || w.owesLocal(c, b) {
+		if contains(except, b.ID) || b.Old || !b.HasKey || (c != nil && contains(c.Lost, b.ID)) || w.owesLocal(c, b) {
+			continue
+		}
+		if on("reloc-enrolled-only") && !b.Enrolled {
 			continue
 		}
 		key := [3]int{w.hostsOn(b, app), w.hostsOn(b, ""), -int(tieHash(b.ID))}
diff --git a/internal/sim/hostlife/witness_test.go b/internal/sim/hostlife/witness_test.go
index 94a4f5c..88394c3 100644
--- a/internal/sim/hostlife/witness_test.go
+++ b/internal/sim/hostlife/witness_test.go
@@ -350,7 +350,7 @@ func newWitness() *world {
 		control: newBucket(), delivered: map[int]bool{}, durable: map[string]map[int]bool{}, writeInc: map[int]int{}, txs: map[int]tx{}, legacyIncs: map[int]bool{}, purgeOp: map[string]string{}, genParent: map[string]string{}, markerAlerted: map[string]bool{}, execLease: map[int]execLease{}, fail: map[string]bool{}, stats: map[string]int{}}
 	for r := 0; r < nRegions; r++ {
 		w.buckets[r] = newBucket()
-		b := &box{ID: r, Region: r, HasKey: true}
+		b := &box{ID: r, Region: r, HasKey: true, Enrolled: true, DeleteOnTermination: true}
 		b.forget()
 		w.boxes = append(w.boxes, b)
 	}
diff --git a/internal/sim/hostlife/world_test.go b/internal/sim/hostlife/world_test.go
index ef69ba7..f945e1f 100644
--- a/internal/sim/hostlife/world_test.go
+++ b/internal/sim/hostlife/world_test.go
@@ -359,6 +359,21 @@ type box struct {
 	FailArchive bool // the final archive fails (too large) on this box
 	FailSettle  bool // the app passes one readiness check, works, then fails
 	Nested      bool // nested layout: children survive an agent crash
+	// region HA (two boxes per region, L18)
+	Terminated          bool // the cloud terminated the instance (H1): it never runs again and never returns; a Destroyed box that is not Terminated is stopped and may start again with its disk
+	TerminatedAt        int
+	Enrolled            bool // the roster holds an active entry with its proven cloud identity (H11); a replacement box is enrolled automatically enrollDelay steps after it launches (H16, H17)
+	EnrollAt            int
+	DeleteOnTermination bool // every volume the box had attached carried the flag while it ran (§5.9): decides only the automatic discharge of its park-local chores (H19), never a fence
+	installEpoch        int  // the agent process that made this box's local install for a relocation (B2-5): a later process never remakes it once an admission named P
+	// receipt is the box's install journal for a relocation (1b-next Task 8c,
+	// VerifyReceipt): durable, it survives an agent restart; a park of the
+	// installation removes it, and so does a lost volume (a witness)
+	receipt *receiptEntry
+	// attemptTag is the probe attempt this agent process has counted and
+	// not yet ended (memory: a restart forgets it, and the next attempt is
+	// counted again, ruling 19)
+	attemptTag string
 
 	Row     *row
 	DB      *localDB
@@ -558,6 +573,7 @@ func (b *box) forget() {
 	b.mem = map[string]bool{}
 	b.evidAt = map[string]int{}
 	b.pendingTimers = nil
+	b.attemptTag = ""
 	if b.DB != nil {
 		b.DB.InFlight = nil // the upload's client is gone; the restarted replica uploads the same file again
 		// a writer that was draining before its clean close is gone with
@@ -781,6 +797,27 @@ type opState struct {
 	NewRegion            int
 	NewSerial            int
 	NewBox               int // the executor a create named once (region HA §5.2, H12): never substituted
+	// region HA relocation (spec 1 §5.8; claim rev 6.30 §4 L1). The
+	// journal entries below are what the claim's op.journal carries
+	RelocReason  string        // drain or failover
+	FenceAt      int           // fence.<box>.observed_at of the latest fence the operation cites; 0 none
+	FailedAt     int           // when the target entered probe-failed
+	Release      *releaseEntry // the release sequence's journal entry (§5.8): the source's in releasing, a failed target's in probe-failed
+	Pin          *pinEntry     // the pinned recovery set
+	Prepared     string        // P, the prepared generation this installation builds; "" before installing
+	InstallStamp int           // the stamp of the CAS that handed op.exec to the current target (op.journal.install_stamp)
+	Receipt      *receiptEntry // the executor's local install receipt (local_install)
+	ProbingSince int
+	Replacements int   // targets replaced in this operation; two, then stuck
+	Excluded     []int // replaced targets, never named again for this host
+	InstalledOn  []int // every box this operation handed op.exec for an installation: each owes a park-local at serving unless discharged
+	Discharged   []int // fenced boxes whose park-local chores the fence CAS discharged (L3, H19)
+	Stuck        string
+	// 1b-next rev 16's journal additions
+	ReleasingSince int    // releasing_since: the release deadline's start (ruling 14)
+	Attempts       int    // probe_attempts.<op.exec>: counted before each attempt, at most probeTries (ruling 19)
+	PreparedOpened string // prepared_opened: journaled by the admission that opened P (rev 12 S1)
+	Resolved       bool   // an operator's resolve (model ruling 13): the source is eligible as a target again, and an empty listing is accepted
 
 	// journal
 	ReportAt     int
@@ -859,6 +896,50 @@ type opState struct {
 	BaseVer int
 }
 
+// releaseEntry is §5.8's release journal entry: the box, generation and
+// session that gave the host up, its stopped database's final TXID (the
+// listing shows it before pinning may cite it), and, until Task 4's files
+// manifest, the files directory and wake state the box published. Flushed
+// is false when the session's replicator was gone (an agent restart) and
+// the entry names what the remote held: released coverage never applies
+// to it, and the next admission declares the rest.
+type releaseEntry struct {
+	Box, Session int
+	Gen          string
+	FinalTX      int
+	ManifestSeq  int
+	Flushed      bool
+	Files        *filesDir
+	Timers       []int
+	At           int
+}
+
+// pinEntry is §5.8's pinned recovery set: the database position N the
+// build restores to (exact versions in the real pin; the model's build
+// never restores past N), the files manifest version (Task 4), and when
+// the pin was taken (after a release's final_txid is visible, or after a
+// fence's observed_at plus failoverPinDelay).
+type pinEntry struct {
+	Gen            string // the generation the pin reads (genselect over the admitted chain)
+	TX             int
+	ManKey         string
+	ManVer, ManSeq int
+	At             int
+	ClaimVer       int // the claim version it was selected against (1b-next ruling 16: pin-<gen>.json)
+	// Files and Timers are the files set the pin was taken with, until
+	// Task 4's manifest: the release's, or a failover's stand-in
+	Files  *filesDir
+	Timers []int
+}
+
+// receiptEntry is the local install receipt (§5.8 local_install): the
+// box and the install_stamp of the CAS that handed it op.exec. A
+// replacement executor never inherits its predecessor's.
+type receiptEntry struct {
+	Op         string
+	Box, Stamp int
+}
+
 type digest struct {
 	Writes string
 	Files  string
@@ -1122,6 +1203,25 @@ func (c *claim) clone() *claim {
 	}
 	n.Op.Parts = append([]int(nil), c.Op.Parts...)
 	n.Op.StopFiles = c.Op.StopFiles.clone()
+	n.Op.Excluded = append([]int(nil), c.Op.Excluded...)
+	n.Op.InstalledOn = append([]int(nil), c.Op.InstalledOn...)
+	n.Op.Discharged = append([]int(nil), c.Op.Discharged...)
+	if r := c.Op.Release; r != nil {
+		cp := *r
+		cp.Files = r.Files.clone()
+		cp.Timers = append([]int(nil), r.Timers...)
+		n.Op.Release = &cp
+	}
+	if p := c.Op.Pin; p != nil {
+		cp := *p
+		cp.Files = p.Files.clone()
+		cp.Timers = append([]int(nil), p.Timers...)
+		n.Op.Pin = &cp
+	}
+	if r := c.Op.Receipt; r != nil {
+		cp := *r
+		n.Op.Receipt = &cp
+	}
 	if c.Holder != nil {
 		n.Holder.Admissions = append([]admissionRecord(nil), c.Holder.Admissions...)
 		for i := range n.Holder.Admissions {

• [ ] Step 2: Run the gate

export GOFLAGS=-buildvcs=false
gofmt -l internal/sim/hostlife/; nice -n 19 go vet ./internal/sim/hostlife/
nice -n 19 go test ./internal/sim/hostlife/ -count=1 -v 2>&1 | tee $TMPDIR/twobox/task2.log | grep -E "seeds, |^--- FAIL|^ok|^FAIL|^    sim_test.go:[0-9]+: seed"
diff $TMPDIR/twobox/baseline-counters.json <(grep COUNTERS $TMPDIR/twobox/task2.log | head -1 | sed 's/.*COUNTERS //') && echo ONE-BOX-COUNTERS-IDENTICAL

Expected (the dry run's): gofmt prints nothing; 300 seeds, 0 failed, 483 completed operations; mutated="" boxes=1, 300 seeds, 0 failed, 449 completed operations; mutated="" boxes=2; ok; ONE-BOX-COUNTERS-IDENTICAL. TestDrainEndToEnd and TestWitnesses (including fence-converts-moving) pass. A two-box seed that fails is a finding: replay it with HOSTLIFE_BOXES=2 HOSTLIFE_SEED=<n> go test ./internal/sim/hostlife/ -run '^TestHostLifecycle$' -v, decide whether the model or the spec is wrong, and record it in Task 7's brief either way; do not weaken an oracle to pass.

• [ ] Step 3: Commit

git add internal/sim/hostlife/
git commit -m "sim: relocation by drain through region HA §5.8's phase table with plan 1b-next rev 16's guards: the release and its deadline, the barrier on every phase change, a pin bound to its claim version and to evidenced emptiness, EnsureLocal and VerifyReceipt around P's first admission, prepared_opened journaled, three probe attempts counted first, released coverage, the row cases and the replacement cap

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

---

Task 3: Termination, enrollment, the fence, failover and the replacement table (spec §5.9, §5.8 "Losing the source", "Replacing a participant"; H1, H10, H11, H16, H17, H19; L2 to L5, L14; 1b-next StartRelocation, FenceSource, ReplaceTarget, FenceExhaustedTarget, fenceBox, Worker.Step)

A box can now be terminated by the cloud: permanently gone, its in-flight requests still completing later (late PUTs after termination). A regional worker that observes a terminated, enrolled box the claim names writes the fence in one CAS, source first as Worker.Step orders it: the box goes on lost, the timers acknowledged on it are declared, its regional chores pass to its region, its park-local chores are discharged only when its volume evidence qualifies, and the operation's rule applies: a serving executor becomes a failover relocation; a relocation's source becomes a failover (source loss); its target is replaced per the table, or, with the replacements used, fenced into stuck (phase-sensitive); a pre-flip move's source converts (existing). A stuck operation consumes no fence; the operator's resolve does. Replacement boxes launch after a delay, unenrolled, and enroll automatically after another (H16, H17); an unenrolled reference is never chosen. Termination is drawn only where region HA owns the loss (plan ruling 15). Until Task 4's publisher, a fenced box's files directory stands in for what it published (deadBoxFiles).

| Rule | 1b-next rev 16 | What the model does | |---|---|---| | fence-terminated-only | termfence.Verify, VerifyFence | only a terminated, enrolled box is fenced; a stopped box is the operator's | | fence-discharge-qualified | fenceBox with LocalDischarge (L3, H19) | park-local chores discharged only on qualifying volume evidence; INV-26 is the oracle | | fence-declares-timers | the D4 loss record, timers unknown/partial | timers acknowledged on the fenced box and carried by no landed manifest are declared and alerted | | fence-reassigns-regional | fenceBox's region:<r> reassignment (rev 6 finding 2) | the dead box's box:<b> regional chores pass to its region in the fence CAS | | reloc-source-loss | FenceSource (B1-6) | a source lost before its release makes a failover, which declares its writes | | reloc-replacement-table | ReplaceTarget | the table's four rows; a target lost after P's first admission is a nested failover | | reloc-replace-not-owing | replaceTargetSlot's ErrPendingChore, Worker.next (rev 6 finding 1) | a replacement never owes a park-local, in the chooser and inside the CAS | | reloc-exhausted-fence | FenceExhaustedTarget (ruling 23 as rev 9 amended it) | with the live source op.exec only stuck is new; otherwise op.exec none at pinning, P kept when unopened | | reloc-enrolled-only | eligibleBoxes, ExecutorChooser | an unenrolled reference is never chosen |

Files:

• Modify: regionha_test.go (termination, launches, enrollment, the fence, failover, source loss, replacement, the exhausted fence, regionHAOwnsLoss, deadBoxFiles), twobox_test.go (chooseBoxExcept's park-local rule, adoptionOwner in the two-box shape, ownsObligation for box:<b> owners), moves_test.go (workerMode: the fence step first), sim_test.go (newWorld: the terminate fault and volume flags; heal), console_test.go (userPush), world_test.go (obligation.Owner), rules_test.go, regionha_witness_test.go (two direct tests)
• Test: the gate; TestUnenrolledReferenceNeverChosen, TestTwoWorkersOneChore

Interfaces:

• Produces: (*world) terminate, launchReplacements, enrollStep, regionHAOwnsLoss, fenceStep(b, c) bool, claimNames, fence, fenceBox, declareTimers, timerCarried (no landed manifest yet), deadBoxFiles, startFailover, fenceSource, replaceTarget(n, x) bool, fenceExhaustedTarget; boxOwner(id int) string; w.fail["terminate"]; stats terminated, fences written, relocation started: failover.

• [ ] Step 1: Apply the patch

diff --git a/internal/sim/hostlife/console_test.go b/internal/sim/hostlife/console_test.go
index 942bb8a..3c17855 100644
--- a/internal/sim/hostlife/console_test.go
+++ b/internal/sim/hostlife/console_test.go
@@ -444,7 +444,7 @@ func (w *world) userPush() {
 		return
 	}
 	b := w.execBox(c)
-	if b == nil || b.FailApp {
+	if b == nil || b.FailApp || b.Terminated { // a terminated executor is fenced and failed over, never pushed (region HA §5.9)
 		return
 	}
 	if on("obligations-block-ops") {
@@ -1233,11 +1233,21 @@ func (w *world) operator() {
 	if c.Holder != nil && c.Op.Kind == "relocating" && c.Op.Stuck != "" {
 		op := c.Op
 		released := op.Release != nil && op.Release.Box == op.Exec
+		dead := w.boxByID(op.Exec)
+		if dead != nil && !dead.Destroyed {
+			dead = nil
+		}
 		var what string
 		if w.cas(c, func(n *claim) bool {
 			if !sameOp(n.Op.ID, op.ID) || n.Op.Kind != "relocating" || n.Op.Stuck == "" {
 				return false
 			}
+			if dead != nil && !contains(n.Lost, dead.ID) {
+				// a stopped or terminated executor: the operator's declare-lost
+				// (claim D2) puts it on lost, as a fence would, before the replay
+				w.fenceBox(n, dead)
+				released = false
+			}
 			switch {
 			case op.Exec >= 0 && op.Exec == op.Src && !released && !contains(n.Lost, op.Exec) && (op.Phase == "starting" || op.Phase == "releasing"):
 				src := op.Src
diff --git a/internal/sim/hostlife/moves_test.go b/internal/sim/hostlife/moves_test.go
index 078094e..4969dac 100644
--- a/internal/sim/hostlife/moves_test.go
+++ b/internal/sim/hostlife/moves_test.go
@@ -51,6 +51,9 @@ func (w *world) workerMode(b *box, obl bool) {
 	} else if w.rng.Intn(10) == 0 {
 		b.stale = c.clone()
 	}
+	if w.fenceStep(b, c) {
+		return // the regional worker's termination fence (region HA §5.9), before its role
+	}
 	w.role(b, c)
 }
 
diff --git a/internal/sim/hostlife/regionha_test.go b/internal/sim/hostlife/regionha_test.go
index 4627712..66f63b2 100644
--- a/internal/sim/hostlife/regionha_test.go
+++ b/internal/sim/hostlife/regionha_test.go
@@ -987,11 +987,432 @@ func (w *world) scopedCleanup(b *box, c *claim) {
 	}
 }
 
-// twoBoxStep is the two-box shape's extra step: a drain now and then
-// during the chaos (Task 3 adds termination, enrollment and replacement
-// launches). It draws only in the two-box shape.
+// ---------- termination, enrollment and the fence (region HA §5.9; H1, H10, H11, H16, H17, H19) ----------
+
+// terminate is the cloud terminating a box (H1): nothing on it runs
+// again, it never returns (a stopped box may; heal skips a terminated
+// one), and the requests it issued still complete at their own time,
+// which is the late-PUT-after-termination case. The two-box step draws
+// it; it never leaves the world without an enrolled live box, since H17's
+// cross-region confirmer must exist for a replacement to enroll.
+func (w *world) terminate(b *box) {
+	if b.Destroyed {
+		return
+	}
+	enrolled := 0
+	for _, x := range w.liveBoxes() {
+		if x.Enrolled && x != b {
+			enrolled++
+		}
+	}
+	if enrolled == 0 {
+		return
+	}
+	b.Destroyed, b.Terminated, b.TerminatedAt = true, true, w.now
+	b.Procs, b.plans = nil, nil
+	w.stats["terminated"]++
+	w.logf("box %d terminated by the cloud (region %d)", b.ID, b.Region)
+}
+
+// launchReplacements: the group keeps the region at its minimum (H5): a
+// replacement launches replaceDelay steps after the termination that left
+// the region short, unenrolled (H16), with its volume flag drawn (two-box
+// sweeps only: a witness world's quiet source draws nothing).
+func (w *world) launchReplacements() {
+	for r := 0; r < nRegions; r++ {
+		if len(w.regionBoxes(r)) >= w.perRegion {
+			continue
+		}
+		last := 0
+		for _, b := range w.boxes {
+			if b.Region == r && b.Terminated && b.TerminatedAt > last {
+				last = b.TerminatedAt
+			}
+		}
+		if last == 0 || w.now < last+replaceDelay {
+			continue
+		}
+		w.nextID++
+		nb := &box{ID: 100 + w.nextID, Region: r, HasKey: true, EnrollAt: w.now, DeleteOnTermination: w.rng.Intn(8) != 0}
+		nb.forget()
+		w.boxes = append(w.boxes, nb)
+		w.stats["replacements launched"]++
+		w.logf("box %d launched in region %d, unenrolled", nb.ID, r)
+	}
+}
+
+// enrollStep is automatic enrollment (H16, L19): a launched box's boxid
+// evidence verifies and an enrolled box confirms its group membership
+// enrollDelay steps after launch. Any enrolled box of any region may
+// confirm (H17: the first box of an emptied region is confirmed from
+// another region); with none, nothing enrolls.
+func (w *world) enrollStep() {
+	confirmer := false
+	for _, b := range w.liveBoxes() {
+		if b.Enrolled {
+			confirmer = true
+		}
+	}
+	if !confirmer {
+		return
+	}
+	for _, b := range w.liveBoxes() {
+		if !b.Enrolled && w.now >= b.EnrollAt+enrollDelay {
+			b.Enrolled = true
+			w.stats["boxes enrolled automatically"]++
+			w.logf("box %d enrolled (region %d)", b.ID, b.Region)
+		}
+	}
+}
+
+// twoBoxStep is the two-box shape's extra step (ruling 1): replacements
+// launch and enroll; during the chaos a box is terminated now and then,
+// and a drain is asked for now and then.
 func (w *world) twoBoxStep() {
+	w.launchReplacements()
+	w.enrollStep()
+	if !w.calm && w.fail["terminate"] && w.rng.Intn(200) == 0 {
+		bs := w.liveBoxes()
+		if b := bs[w.rng.Intn(len(bs))]; w.regionHAOwnsLoss(b) {
+			w.terminate(b)
+		}
+	}
 	if !w.calm && w.rng.Intn(60) == 0 {
 		w.userRelocate()
 	}
 }
+
+// regionHAOwnsLoss: the loss of b is region HA's to recover (model ruling
+// 15): the claim holds the host and names b, if at all, only as a serving
+// executor, a relocation's participant or a chore's owner; a box holding
+// a legacy host's state before its adoption is never terminated. A participant of a move,
+// a landing, a rollback, a revert, a push, a create or a delete is
+// recovered from a lost box by moves' and the claim's declare-lost paths
+// (L14), which the model walks for a destroyed box that is stopped and
+// may return; the sweep never terminates one.
+func (w *world) regionHAOwnsLoss(b *box) bool {
+	c := w.claim
+	if c == nil || c.Holder == nil {
+		return b.Row == nil && b.DB == nil && b.Files == nil // a legacy host not yet adopted is not region HA's
+	}
+	switch c.Op.Kind {
+	case "serving", "relocating":
+		return true
+	}
+	return !(c.Op.Exec == b.ID || contains(c.Op.Parts, b.ID) || c.Op.Src == b.ID || c.Op.Tgt == b.ID || c.Op.NewBox == b.ID)
+}
+
+// fenceStep is the regional worker's termination fence (§5.9; claim L2
+// to L5; Worker.Step's "evidence first"): for a terminated, enrolled box
+// of its own region that the claim still names, it writes the fence in
+// one CAS (fence). A stopped box is never fenced (rule
+// fence-terminated-only: "stopped and stopping do not count, because a
+// stopped box can start again with its disk"); the mutation fences any
+// destroyed box. An unenrolled box has no roster entry to bind the fence
+// to (HA7) and is never fenced. The source's fence is consumed before the
+// target's, as Worker.Step orders them.
+func (w *world) fenceStep(b *box, c *claim) bool {
+	if c == nil || !b.Enrolled || contains(c.Lost, b.ID) {
+		return false
+	}
+	var cands []*box
+	for _, x := range w.boxes {
+		if x.Region != b.Region || x == b || !x.Destroyed || !x.Enrolled || contains(c.Lost, x.ID) {
+			continue
+		}
+		if !x.Terminated && on("fence-terminated-only") {
+			continue
+		}
+		if !w.claimNames(c, x) {
+			continue
+		}
+		if c.Op.Kind == "relocating" && x.ID == c.Op.Src {
+			cands = append([]*box{x}, cands...)
+		} else {
+			cands = append(cands, x)
+		}
+	}
+	if len(cands) == 0 {
+		return false
+	}
+	before := w.claim.Ver
+	w.fence(b, c, cands[0])
+	return w.claim.Ver != before
+}
+
+// claimNames: the claim gives x a role, so a fence changes it.
+func (w *world) claimNames(c *claim, x *box) bool {
+	if c.Op.Exec == x.ID || contains(c.Op.Parts, x.ID) || c.Op.Kind == "creating" && c.Op.NewBox == x.ID || c.Op.Kind == "moving" && c.Op.Src == x.ID {
+		return true
+	}
+	if c.Op.Kind == "relocating" && (c.Op.Src == x.ID || c.Op.Tgt == x.ID) {
+		return true
+	}
+	for _, o := range c.Obl {
+		if o.Owner == boxOwner(x.ID) {
+			return true
+		}
+	}
+	return w.owesLocal(c, x)
+}
+
+// boxOwner is an obligation's owner box:<b> (claim §2): the legacy form a
+// regional chore may carry; "" is region:<r>, any eligible worker of the
+// region (P6-D5).
+func boxOwner(id int) string { return fmt.Sprintf("box:%d", id) }
+
+// fence is the fence CAS for x, observed terminated by worker b. Moves'
+// cases keep their owners: a pre-flip move's source converts (moves
+// §7.10, the existing CAS); a move's target before the flip, a landing's
+// or a rollback's target are moves' declare-lost path, which this model
+// gives the operator (L14); a create's box is cancelled by the recovery
+// pass (Task 1). Everything else is one CAS here: the box goes on lost
+// with the fence reference and observed_at, its chores are discharged if
+// its volume evidence qualifies, its regional work passes to its region,
+// and the operation's rule applies (StartRelocation's failover,
+// FenceSource, ReplaceTarget, FenceExhaustedTarget). A target with no
+// spare to name is fenced on a later pass (Worker.next: "no eligible box
+// yet").
+func (w *world) fence(b *box, c *claim, x *box) {
+	op := c.Op
+	switch {
+	case op.Kind == "moving" && op.Src == x.ID:
+		if on("fence-converts-moving") && !op.Committed && !(w.rec != nil && w.rec.MoveID == op.ID && w.rec.MoveState == "landing") {
+			w.convertToRelocating(c, x)
+		}
+		return
+	case op.Kind == "moving" && op.Tgt == x.ID, (op.Kind == "landing" || op.Kind == "restoring") && op.Tgt == x.ID, op.Kind == "creating":
+		return
+	case op.Kind == "relocating" && op.Stuck != "":
+		return // Worker.Step consumes no fence of a stuck operation: the operator's resolve does
+	}
+	id := op.ID
+	if w.cas(c, func(n *claim) bool {
+		if !sameOp(n.Op.ID, id) || n.Op.Kind != op.Kind || contains(n.Lost, x.ID) {
+			return false
+		}
+		switch {
+		case n.Holder != nil && n.Op.Kind == "serving" && n.Op.Exec == x.ID:
+			w.startFailover(n, x)
+		case n.Op.Kind == "relocating" && n.Op.Stuck != "":
+			return false
+		case n.Op.Kind == "relocating" && n.Op.Src == x.ID:
+			w.fenceSource(n, x)
+		case n.Op.Kind == "relocating" && n.Op.Tgt == x.ID:
+			if !w.replaceTarget(n, x) {
+				return false // no spare yet
+			}
+		}
+		w.fenceBox(n, x)
+		return true
+	}) {
+		w.stats["fences written"]++
+		w.logf("box %d fenced box %d (terminated at %d) under %s/%s", b.ID, x.ID, x.TerminatedAt, w.claim.Op.Kind, w.claim.Op.ID)
+		w.declareTimers(x, w.claim.Holder)
+	}
+}
+
+// fenceBox is plan 1b-next's fenceBox: lost with the fence reference
+// (FenceBox, FenceAt); the box's regional work (a park-generation or
+// park-replica owned by box:<x>) passed to region:<r> keeping its
+// identity (rule fence-reassigns-regional, 1b-next rev 6 finding 2, as
+// DeclareLost does for a declared loss); and the box's park-local chores
+// discharged only when its volume evidence qualifies (L3, H19: every
+// attached volume DeleteOnTermination while it ran); otherwise they stay
+// open for the operator path, and nothing about recovery waits on them.
+// The mutation of fence-discharge-qualified discharges regardless (INV-26
+// is the oracle); the mutation of fence-reassigns-regional leaves the
+// regional work with the dead box, where nothing runs it.
+func (w *world) fenceBox(n *claim, x *box) {
+	n.Lost = addUniq(n.Lost, x.ID)
+	n.Op.FenceBox, n.Op.FenceAt = x.ID, w.now
+	var parts []int
+	for _, p := range n.Op.Parts {
+		if p != x.ID {
+			parts = append(parts, p)
+		}
+	}
+	n.Op.Parts = parts
+	if on("fence-reassigns-regional") {
+		for i := range n.Obl {
+			if o := &n.Obl[i]; o.Kind != "park-local" && o.Owner == boxOwner(x.ID) {
+				o.Owner = "" // region:<r>, the chore's id, operation, retirement and scope kept
+				w.stats["fence: regional work passed to the region"]++
+			}
+		}
+	}
+	qualified := x.DeleteOnTermination
+	if !on("fence-discharge-qualified") {
+		qualified = true
+	}
+	if !qualified {
+		w.stats["fence: park-local chores left open (volume evidence)"]++
+		return
+	}
+	var keep []obligation
+	for _, o := range n.Obl {
+		if o.Kind == "park-local" && o.Box == x.ID {
+			if !x.DeleteOnTermination {
+				w.violate("INV-26: box %d's park-local chore %s discharged without qualifying volume evidence (§5.9, H19)", x.ID, o.ID)
+			}
+			w.stats["fence: park-local chores discharged"]++
+			continue
+		}
+		keep = append(keep, o)
+	}
+	n.Obl = keep
+	n.Op.Discharged = addUniq(n.Op.Discharged, x.ID)
+}
+
+// declareTimers: the timers acknowledged on a fenced box and not yet
+// delivered are declared lost with it and alerted (moves §7.10: no return
+// lane carries them; §5.9: the loss record's timer knowledge is partial).
+// Task 4 narrows it to the timers its last published manifest does not
+// carry. The mutation of fence-declares-timers drops them silently.
+func (w *world) declareTimers(x *box, h *holder) {
+	if h == nil || !on("fence-declares-timers") {
+		return
+	}
+	n := 0
+	for i := range w.acks {
+		a := &w.acks[i]
+		if a.Box == x.ID && a.Inc == h.Inc && a.Kind == "timer" && !a.Exempt && !w.delivered[a.W] && !w.timerCarried(x, h, a.W) {
+			a.Exempt = true
+			n++
+		}
+	}
+	if n > 0 {
+		w.stats["timers declared lost"] += n
+		w.alert("box %d fenced: %d acknowledged timers registered on it are lost with it", x.ID, n)
+	}
+}
+
+// timerCarried is Task 4's: a landed manifest carries the timer. Before
+// the files publisher nothing does.
+func (w *world) timerCarried(x *box, h *holder, id int) bool { return false }
+
+// deadBoxFiles is what a fenced box's files directory contributes to the
+// recovery: until Task 4's files publisher, its local directory stands in
+// for what it published (L17), as convertToRelocating's does.
+func (w *world) deadBoxFiles(x *box) *filesDir {
+	return x.Files.clone()
+}
+
+// startFailover is the fence's start of a relocation for a serving
+// executor (§5.8 reason failover, StartRelocation with a fence; spec 3's
+// placer supplies the decision): op.exec none, the stamp kept, at pinning
+// with the target named there (ruling 4); the pin waits out
+// failoverPinDelay from the fence; deadBoxFiles is the files publisher's
+// stand-in until Task 4.
+func (w *world) startFailover(n *claim, x *box) {
+	n.Op = opState{Kind: "relocating", ID: w.newID("rl"), Phase: "pinning", Exec: -1, Src: x.ID, Tgt: -1, SrcRegion: x.Region,
+		RelocReason: "failover", ReqAt: w.now, App: n.Holder.App, SrcGen: n.Holder.Gen, SrcStamp: n.Holder.Stamp, StopFiles: w.deadBoxFiles(x)}
+	w.stats["relocation started: failover"]++
+}
+
+// fenceSource is §5.8's source loss (B1-6, FenceSource): a drain whose
+// source is terminated before its release is journaled becomes a
+// failover in the same CAS, op.exec none, the stamp kept, the source off
+// the barrier, its files directory the publisher's stand-in; after its
+// release only its liveness changes. (1b-next keeps a source lost in
+// starting at starting until the remaining participant acknowledges,
+// then PinFailover; the model goes to pinning at once, where the pin
+// waits out the delay and installing waits for the barrier.) The
+// mutation of reloc-source-loss takes a source lost in releasing as
+// released at what the remote holds, so its unuploaded writes go
+// undeclared.
+func (w *world) fenceSource(n *claim, x *box) {
+	switch {
+	case n.Op.Phase == "starting", n.Op.Phase == "releasing" && n.Op.Release == nil:
+		if !on("reloc-source-loss") && n.Op.Phase == "releasing" {
+			h := n.Holder
+			n.Op.Release = &releaseEntry{Box: x.ID, Session: h.Session, Gen: h.Gen, FinalTX: w.remoteMax(w.buckets[x.Region], dataKey(h.Location, h.Gen, "")), Flushed: true, Files: w.deadBoxFiles(x), Timers: append([]int(nil), x.Timers...), At: w.now}
+			n.Op.Exec, n.Op.Phase = -1, "pinning"
+			return
+		}
+		n.Op.RelocReason, n.Op.Exec, n.Op.Phase = "failover", -1, "pinning"
+		n.Op.Release, n.Op.StopFiles = nil, w.deadBoxFiles(x)
+		w.stats["relocation: source lost before its release, converted to failover"]++
+	default:
+		w.stats["relocation: source lost after its release"]++
+	}
+}
+
+// replaceTarget is §5.8's replacement table (ReplaceTarget) for a target
+// terminated by its fence, within the fence's CAS:
+//
+//	starting, releasing, pinning      -> the same phase, to' named
+//	installing                        -> installing: to' is op.exec, a new stamp, a fresh P'
+//	installed, or probing before P    -> installed: to' is op.exec, a new stamp, the same P, no receipt
+//	after P's first admission, or     -> pinning: a nested failover from holder.generation as observed
+//	probe-failed
+//
+// Exhaustion is checked first (Worker.replace, 1b-next R1-16): with the
+// replacements used the fence goes to fenceExhaustedTarget and no spare
+// is looked for. With no eligible spare it reports false and the fence
+// waits for a later pass (Worker.next). The mutation of
+// reloc-replacement-table resumes every late loss at installed with the
+// same P.
+func (w *world) replaceTarget(n *claim, x *box) bool {
+	phase := n.Op.Phase
+	if on("reloc-replacement-cap") && n.Op.Replacements >= maxReplacements {
+		w.fenceExhaustedTarget(n, x)
+		return true
+	}
+	next := w.chooseBoxExcept(n.Op.SrcRegion, n.Holder.App, relocExcept(n.Op, x.ID)...)
+	if next == nil {
+		w.stats["relocation: target lost, no spare yet"]++
+		return false
+	}
+	if !w.nameReplacement(n, next.ID, phase) {
+		return n.Op.Stuck != ""
+	}
+	w.stats["relocation: target replaced at "+phase]++
+	late := preparedOpened(n) || phase == "probe-failed" || phase == "probed" || phase == "opened"
+	switch {
+	case phase == "starting" || phase == "releasing" || phase == "pinning":
+	case phase == "installing":
+		n.Op.BaseKey, n.Op.BaseVer, n.Op.BaseTX = "", 0, 0
+		w.handExec(n, next.ID, "installing", w.newID("P"))
+	case !late || !on("reloc-replacement-table"):
+		w.handExec(n, next.ID, "installed", n.Op.Prepared) // P was never opened: to' makes its own local install and opens it
+	default:
+		n.Op.Exec, n.Op.Phase = -1, "pinning"
+		n.Op.Pin, n.Op.Prepared, n.Op.Receipt, n.Op.Release = nil, "", nil, nil
+		n.Op.BaseKey, n.Op.BaseVer, n.Op.BaseTX = "", 0, 0
+		n.Op.ProbeTries, n.Op.Attempts = 0, 0
+		w.stats["nested failover after P was admitted"]++
+	}
+	return true
+}
+
+// fenceExhaustedTarget is FenceExhaustedTarget (1b-next ruling 23 as rev
+// 9 amended it; rule reloc-exhausted-fence): a target terminated after
+// the operation used its replacements is fenced (the caller's fenceBox)
+// and the operation is stuck, with no third target chosen. While another
+// box is op.exec (the live source in starting or releasing) only stuck is
+// new: the target's fence is no evidence against the source, whose
+// execution identity, phase and release stay, so its own stop evidence
+// still decides. Otherwise (op.exec the dead target, or none) the dead
+// installation's authority is revoked: op.exec none at pinning, its
+// receipt and release dropped, and P's pin and remote build kept when P
+// was never opened, dropped for a nested pinning when it was. The
+// mutation is rev 8's: always op.exec none at pinning, which revokes a
+// live source without its stop evidence.
+func (w *world) fenceExhaustedTarget(n *claim, x *box) {
+	why := fmt.Sprintf("box %d terminated after %d target replacements", x.ID, maxReplacements)
+	w.stats["relocation: exhausted target fenced"]++
+	if on("reloc-exhausted-fence") && n.Op.Exec >= 0 && n.Op.Exec != x.ID {
+		n.Op.Stuck = why
+		return
+	}
+	opened := preparedOpened(n)
+	n.Op.Exec, n.Op.Phase = -1, "pinning"
+	n.Op.Receipt, n.Op.Release = nil, nil
+	n.Op.ProbeTries, n.Op.Attempts = 0, 0
+	if opened {
+		n.Op.Pin, n.Op.Prepared = nil, ""
+		n.Op.BaseKey, n.Op.BaseVer, n.Op.BaseTX = "", 0, 0
+	}
+	n.Op.Stuck = why
+}
diff --git a/internal/sim/hostlife/regionha_witness_test.go b/internal/sim/hostlife/regionha_witness_test.go
index 82ffbce..4552c10 100644
--- a/internal/sim/hostlife/regionha_witness_test.go
+++ b/internal/sim/hostlife/regionha_witness_test.go
@@ -51,3 +51,66 @@ func TestDrainEndToEnd(t *testing.T) {
 		t.Errorf("box 0 still holds local state after its park-local: db=%v files=%v row=%v", from.DB != nil, from.Files != nil, from.Row)
 	}
 }
+
+// TestUnenrolledReferenceNeverChosen (§2, HA7; Review Focus 4): the
+// executor is terminated; the region's other enrolled box holds no
+// secrets key, so it may work but cannot take the host (R9); the
+// replacement that launched is not yet enrolled. The failover must wait
+// at pinning with no target until the replacement enrolls, never name
+// the unenrolled reference (which could not be fenced if it died).
+func TestUnenrolledReferenceNeverChosen(t *testing.T) {
+	w := twoBoxWitness()
+	from, peer := w.boxes[0], w.boxes[3]
+	w.serve(from, 1, app0)
+	peer.HasKey = false
+	w.terminate(from)
+	w.now += replaceDelay
+	w.launchReplacements()
+	nb := w.boxes[len(w.boxes)-1]
+	if nb.Region != 0 || nb.Enrolled {
+		t.Fatalf("no unenrolled replacement in region 0: %+v", nb)
+	}
+	w.reach(t, 100, "the executor fenced by the peer", func() bool {
+		return contains(w.claim.Lost, from.ID) && w.claim.Op.Kind == "relocating"
+	}, w.act(peer), w.recoveryPass)
+	// the witness schedule never runs enrollStep: nb stays unenrolled, and
+	// the relocation must wait at pinning with no target
+	w.drive(enrollDelay, func() bool { return false }, w.actAll(), w.recoveryPass)
+	if c := w.claim; c.Op.Kind != "relocating" || c.Op.Tgt != -1 || c.Op.Exec != -1 {
+		t.Fatalf("an unenrolled box was named, or the relocation moved on: %s", w.state())
+	}
+	w.now += enrollDelay
+	w.enrollStep()
+	if !nb.Enrolled {
+		t.Fatalf("the replacement did not enroll")
+	}
+	w.reach(t, 1500, "serving on the replacement", func() bool {
+		c := w.claim
+		return c.Op.Kind == "serving" && c.Op.Exec == nb.ID
+	}, w.actAll(), w.recoveryPass, w.operator, func() { w.wake(nb) })
+	w.finish(t)
+	if len(w.violations) > 0 {
+		t.Fatalf("%s", w.violations[0])
+	}
+}
+
+// TestTwoWorkersOneChore (claim P6-D5; Review Focus 1): a push leaves a
+// dead generation; both boxes of the region run its park-generation at
+// once. The chore converges with no residue and no double declaration.
+func TestTwoWorkersOneChore(t *testing.T) {
+	w := twoBoxWitness()
+	b := w.boxes[0]
+	w.serve(b, 1, app0)
+	w.userPush()
+	w.reach(t, 800, "the push served and its predecessor's chore queued", func() bool {
+		c := w.claim
+		return c.Op.Kind == "serving" && len(c.Obl) > 0
+	}, w.actAll(), w.recoveryPass, func() { w.wake(b) })
+	w.finish(t)
+	if len(w.violations) > 0 {
+		t.Fatalf("%s", w.violations[0])
+	}
+	if r := w.residue(); len(r) > 0 {
+		t.Fatalf("residue after both workers ran the chore: %v", r)
+	}
+}
diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go
index 545acad..2516bf2 100644
--- a/internal/sim/hostlife/rules_test.go
+++ b/internal/sim/hostlife/rules_test.go
@@ -168,4 +168,13 @@ var allRules = []string{
 	"reloc-ensure-local",            // 1b-next rev 15 finding 2 (Effects.EnsureLocal): before P's first admission the local install is verified, and restored under the same install_stamp if a lost lease's scoped cleanup retired it; the mutation admits over a missing install
 	"reloc-verify-receipt",          // 1b-next rev 16 finding 1 (Effects.VerifyReceipt, MarkStuck in probing): after P opens, a missing or different receipt marks the operation stuck before any further admission; the mutation makes the attempt anyway
 	"reloc-prepared-opened-journal", // 1b-next rev 12 S1 (prepared_opened, PreparedOpened): P's opening is journaled with its admission and outlives holder.admissions' trim; the mutation reads the trimmed list and remakes the install after P opened
+	// termination, the fence and the replacement table (Task 3)
+	"fence-terminated-only",     // region HA §5.9 "What never counts", H10, H19 (termfence.Verify, VerifyFence): only a terminated, enrolled box is fenced; the mutation fences a stopped box, which may start again with its disk
+	"fence-discharge-qualified", // region HA §5.9, L3, H19 (fenceBox with LocalDischarge): a fenced box's park-local chores are discharged automatically only when every volume record qualifies; the mutation discharges regardless (INV-26)
+	"fence-declares-timers",     // moves §7.10, region HA §5.9 (the D4 loss record, timer knowledge partial): the timers acknowledged on a fenced box are declared lost and alerted; the mutation drops them silently
+	"fence-reassigns-regional",  // 1b-next rev 6 finding 2 (fenceBox, as DeclareLost's reassign_regional): the fence passes the dead box's park-generation and park-replica chores to its region; the mutation leaves them with the dead box, where nothing runs them
+	"reloc-source-loss",         // region HA §5.8 B1-6 (FenceSource): a source terminated before its release is journaled makes the operation a failover, which declares its writes; the mutation takes it as released at what the remote holds
+	"reloc-replacement-table",   // region HA §5.8 (ReplaceTarget): a target lost after P's first admission is a nested failover from holder.generation; the mutation resumes at installed with the same P (the admission rules refuse the reopening: expected miss, see expected-outcomes.txt)
+	"reloc-replace-not-owing",   // 1b-next rev 6 finding 1 (replaceTargetSlot's ErrPendingChore, Worker.next's LocalChoreBoxes): a replacement target never owes a park-local for the host, in the chooser and inside the CAS; the mutation lifts both for a relocation's target
+	"reloc-exhausted-fence",     // 1b-next ruling 23 as rev 9 amended it (FenceExhaustedTarget): an exhausted target's fence while the live source is op.exec records stuck and changes nothing else; the mutation is rev 8's, op.exec none at pinning, revoking the source without its stop evidence
 }
diff --git a/internal/sim/hostlife/sim_test.go b/internal/sim/hostlife/sim_test.go
index 92813d5..1a35848 100644
--- a/internal/sim/hostlife/sim_test.go
+++ b/internal/sim/hostlife/sim_test.go
@@ -62,6 +62,12 @@ func newWorld(seed int64, verbose bool) *world {
 		b.forget()
 		w.boxes = append(w.boxes, b)
 	}
+	if w.perRegion > 1 {
+		w.fail["terminate"] = w.rng.Intn(2) == 0
+		for _, b := range w.boxes {
+			b.DeleteOnTermination = w.rng.Intn(8) != 0 // one box in eight has a volume without the flag (§5.9, H19)
+		}
+	}
 	return w
 }
 
@@ -241,7 +247,7 @@ func (w *world) heal(final bool) {
 	}
 	if final {
 		for _, b := range w.boxes {
-			if b.Destroyed && w.regionBox(b.Region) == nil && w.rng.Intn(2) == 0 {
+			if b.Destroyed && !b.Terminated && w.regionBox(b.Region) == nil && w.rng.Intn(2) == 0 {
 				b.Destroyed = false // started again, with its old disk
 				b.forget()
 				w.logf("stopped box %d started again", b.ID)
diff --git a/internal/sim/hostlife/twobox_test.go b/internal/sim/hostlife/twobox_test.go
index e54a6cf..d837ae0 100644
--- a/internal/sim/hostlife/twobox_test.go
+++ b/internal/sim/hostlife/twobox_test.go
@@ -112,9 +112,12 @@ func (w *world) chooseBoxExcept(r int, app string, except ...int) *box {
 	var best *box
 	var bestKey [3]int
 	for _, b := range bs {
-		if contains(except, b.ID) || b.Old || !b.HasKey || (c != nil && contains(c.Lost, b.ID)) || w.owesLocal(c, b) {
+		if contains(except, b.ID) || b.Old || !b.HasKey || (c != nil && contains(c.Lost, b.ID)) {
 			continue
 		}
+		if w.owesLocal(c, b) && (len(except) == 0 || on("reloc-replace-not-owing")) {
+			continue // §2: a box owing a park-local for the host is never chosen (the mutation of reloc-replace-not-owing lifts it for a relocation's target)
+		}
 		if on("reloc-enrolled-only") && !b.Enrolled {
 			continue
 		}
@@ -127,12 +130,13 @@ func (w *world) chooseBoxExcept(r int, app string, except ...int) *box {
 }
 
 // adoptionOwner is the box adoption runs on (claim P5-D2, region HA §9 K5):
-// with one live box in the record's region it is that box, as today; with
-// more, exactly one box must hold the legacy host's local state (its row
-// or database), and zero or several refuse adoption.
+// in the one-box shape it is the region's box, as today; in the two-box
+// shape exactly one live box must hold the legacy host's local state (its
+// row or database), and zero or several refuse adoption, even when only
+// one box of the region is left (placement does not prove ownership).
 func (w *world) adoptionOwner(r int) *box {
 	bs := w.regionBoxes(r)
-	if len(bs) <= 1 {
+	if w.perRegion <= 1 {
 		if len(bs) == 0 {
 			return nil
 		}
@@ -159,5 +163,8 @@ func (w *world) ownsObligation(o obligation, b *box) bool {
 	if o.Kind == "park-local" {
 		return w.ownerOf(o) == b
 	}
+	if o.Owner != "" {
+		return o.Owner == boxOwner(b.ID) && !b.Destroyed // box:<b>, the legacy owner form: that box alone, until a fence or a declared loss passes it to the region
+	}
 	return b.Region == o.Region && !b.Destroyed
 }
diff --git a/internal/sim/hostlife/world_test.go b/internal/sim/hostlife/world_test.go
index f945e1f..f76c223 100644
--- a/internal/sim/hostlife/world_test.go
+++ b/internal/sim/hostlife/world_test.go
@@ -663,6 +663,7 @@ type obligation struct {
 	Ret    string
 	Quiet  int        // not before
 	Scope  *parkScope // the persisted park scope of a remote chore (claim rev 6.15 §2), bound before its first step runs
+	Owner  string     // a regional chore's owner: "" is region:<r> (any worker of the region, P6-D5); box:<b> is the legacy form a fence passes to the region (1b-next rev 6 finding 2)
 }
 
 // parkScope is claim rev 6.23's park scope {location, incarnation,

• [ ] Step 2: Run the gate

gofmt -l internal/sim/hostlife/; nice -n 19 go vet ./internal/sim/hostlife/
nice -n 19 go test ./internal/sim/hostlife/ -count=1 -v 2>&1 | tee $TMPDIR/twobox/task3.log | grep -E "seeds, |^--- FAIL|^ok|^FAIL|^    sim_test.go:[0-9]+: seed"
diff $TMPDIR/twobox/baseline-counters.json <(grep COUNTERS $TMPDIR/twobox/task3.log | head -1 | sed 's/.*COUNTERS //') && echo ONE-BOX-COUNTERS-IDENTICAL

Expected (the dry run's): 300 seeds, 0 failed, 483 completed operations; mutated="" boxes=1, 300 seeds, 0 failed, 464 completed operations; mutated="" boxes=2; ok; ONE-BOX-COUNTERS-IDENTICAL. The two-box COUNTERS carry terminated, fences written, relocation started: failover, replacements launched, boxes enrolled automatically. A failing two-box seed is handled as in Task 2 Step 2.

• [ ] Step 3: Commit

git add internal/sim/hostlife/
git commit -m "sim: termination by the cloud, automatic enrollment, the regional worker's fence (lost, timers declared, regional chores passed to the region, local chores discharged only on qualifying volume evidence), failover from serving, source loss, the replacement table, the phase-sensitive exhausted fence and no replacement owing a park-local

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

---

Task 4: The files publisher, P's prepared manifest, the files pin and the files live set (spec §5.6, §5.8 "the files pin", L13, L17; H6, H7; claim §6.2a, R18-1; moves rev 7.22 §7.6; 1b-next StorePinner, CopyPinnedManifest, PreparedAuthority, referencedOrigins, 1b-next rulings 13 and 21)

In the two-box shape the executor publishes a manifest of its files directory and wake state whenever they change, whether or not the app runs, at the generation's next sequence from 1; the PUT may complete late, after the box is gone. A relocation's target publishes only once P is opened, into its own generations. The release sequence's step 3 publishes a final manifest and journals its sequence. The pin names the newest landed manifest of the admitted chain by key and version (walking genParent, which no trim shortens); a drain's pin must reach the release's manifest. P's build writes P's prepared manifest create-only at sequence 0 before anything of the database, bound to the operation and install_stamp, and the installed CAS waits for it. The local install applies the pinned manifest's files and timers, never the newest. The files live set keeps the pinned manifest, P's, holder.generation's and the chain's newest landed one from every park and from the residue oracle. The fence declares only the timers no landed manifest carries. A dead box's files directory is no longer read (deadBoxFiles returns nothing in the two-box shape), and a files manifest is no database object for the recovery walk (hasFilesIn). Termination now spares an executor none of whose manifests has landed (ruling 17, finding F2).

| Rule | 1b-next rev 16 | What the model does | |---|---|---| | files-pin-exact | RecoveryPin.FilesManifest, StorePinner, the retained copy (ruling 21) | the install applies the pinned version, read by version id | | files-live-set | the classifier's files live set; referencedOrigins (rev 12 finding 1) | a park-generation never archives the chain's live manifest, holder.generation's, P's or the pinned one | | files-prepared-seq-zero | CopyPinnedManifest at sequence 0, PreparedAuthority.FilesSeq/SourceFilesSeq (rev 15 finding 1) | P's prepared manifest at 0, the session publisher from 1; INV-28 is the oracle |

Files:

• Modify: regionha_test.go (the publisher, buildPreparedFiles, manifestKey, isManifestKey, filesState, newestManifest, lastLandedManifest, filesLive, filesLiveSet, pinnedManifest, timerCarried with INV-28; relocRelease step 3; selectPin's files pin; relocFiles, relocTimers; relocationLeftovers parks every prepared generation the operation built and no writer opened, which the prepared manifest made visible as residue (plan ruling 16, finding F3; handExec records them in opState.Built); deadBoxFiles; regionHAOwnsLoss), world_test.go (box's publisher fields, pinEntry.ManGen, opState.Built, world.issued), moves_test.go (genOf, deadGeneration), protocol_test.go (hasFilesIn, hadFilesIn, the park-generation keep), sim_test.go (residueOf), rules_test.go, regionha_witness_test.go (TestLateFileUploads; TestUnenrolledReferenceNeverChosen publishes before the termination)
• Test: the gate; TestLateFileUploads

Interfaces:

• Produces: manifestKey(loc, gen string, seq int) string; isManifestKey(k string) bool; filesState(timers []int, f *filesDir) string; (*world) publishFiles(b *box); (*world) newestManifest(r int, loc, gen string) (key string, ver, seq int, mgen string, m *blob); (*world) lastLandedManifest(r int, loc, gen string) *blob; (*world) filesLive(c *claim, k string) bool, filesLiveSet; (*world) pinnedManifest(c *claim) *blob; box.pubGen, pubSeq, published, releaseSeq; world.issued (each manifest blob carries its issue order in Base); INV-28.

• [ ] Step 1: Apply the patch

diff --git a/internal/sim/hostlife/moves_test.go b/internal/sim/hostlife/moves_test.go
index 4969dac..a12678a 100644
--- a/internal/sim/hostlife/moves_test.go
+++ b/internal/sim/hostlife/moves_test.go
@@ -1886,6 +1886,9 @@ func locationOf(k string) string {
 // in every region.
 func (w *world) deadGeneration(c *claim, r int, k string) bool {
 	h := c.Holder
+	if w.filesLive(c, k) {
+		return false
+	}
 	e := w.execBox(c)
 	authoritative := e != nil && e.Region == r
 	if !on("live-set-region") {
@@ -1944,6 +1947,14 @@ func (w *world) deadGeneration(c *claim, r int, k string) bool {
 		}
 		return true // a dead generation's certificates
 	}
+	if isManifestKey(k) {
+		// a files manifest outside the files live set (region HA §5.6, L13):
+		// its generation's, as the data keys are
+		if genOf(h.Location, k) == h.Gen {
+			return !authoritative
+		}
+		return true
+	}
 	return isDataKey(k)
 }
 
@@ -1953,6 +1964,9 @@ func (w *world) deadGeneration(c *claim, r int, k string) bool {
 // the lock).
 func genOf(loc, k string) string {
 	rest := strings.TrimPrefix(k, loc)
+	if strings.HasPrefix(rest, "files/") {
+		return "" // a files manifest of the origin generation (region HA §5.6)
+	}
 	if strings.HasPrefix(rest, "g-") {
 		if i := strings.Index(rest, "/"); i > 0 {
 			return rest[2:i]
diff --git a/internal/sim/hostlife/protocol_test.go b/internal/sim/hostlife/protocol_test.go
index 8ff23c1..a0d45bd 100644
--- a/internal/sim/hostlife/protocol_test.go
+++ b/internal/sim/hostlife/protocol_test.go
@@ -1146,7 +1146,7 @@ func (w *world) coverParkedPredecessors(n *claim, region int, gens []string) {
 // that never had anything (INV-17).
 func (w *world) hadFilesIn(r int, loc, gen string) bool {
 	for _, k := range w.buckets[r].keys(dataKey(loc, gen, "")) {
-		if genOf(loc, k) == gen {
+		if genOf(loc, k) == gen && !isManifestKey(k) { // a files manifest is no database object (region HA §5.6)
 			return true
 		}
 	}
@@ -1158,7 +1158,7 @@ func (w *world) hadFilesIn(r int, loc, gen string) bool {
 func (w *world) hasFilesIn(r int, loc, gen string) bool {
 	bk := w.buckets[r]
 	for _, k := range bk.keys(dataKey(loc, gen, "")) {
-		if genOf(loc, k) == gen && bk.current(k) != nil {
+		if genOf(loc, k) == gen && bk.current(k) != nil && !isManifestKey(k) { // a files manifest is no database object (region HA §5.6)
 			return true
 		}
 	}
@@ -2360,7 +2360,9 @@ func (w *world) doObligation(b *box, c *claim, o obligation) {
 				retire = "" // the origin generation's sentinel (claim rev 6.10)
 			}
 			inner := keep
-			keep = func(k string) bool { return genOf(o.Prefix, k) != retire || inner != nil && inner(k) }
+			keep = func(k string) bool {
+				return genOf(o.Prefix, k) != retire || w.filesLive(w.claim, k) || inner != nil && inner(k)
+			}
 		}
 		if !w.parkStep(b, o.Prefix, o.Dest(), quiet, o.Scope, keep) {
 			return
diff --git a/internal/sim/hostlife/regionha_test.go b/internal/sim/hostlife/regionha_test.go
index 66f63b2..2884f05 100644
--- a/internal/sim/hostlife/regionha_test.go
+++ b/internal/sim/hostlife/regionha_test.go
@@ -1,6 +1,9 @@
 package hostlife
 
-import "fmt"
+import (
+	"fmt"
+	"strings"
+)
 
 // ---------- relocation (region HA spec 1 §5.8; claim rev 6.30 §4, L1; plan 1b-next rev 16) ----------
 //
@@ -154,7 +157,29 @@ func (w *world) relocRelease(b *box, c *claim) *releaseEntry {
 	if files == nil || files.Inc != h.Inc {
 		files = w.relocFiles(c).clone()
 	}
-	return &releaseEntry{Box: b.ID, Session: h.Session, Gen: h.Gen, FinalTX: n, Flushed: flushed,
+	// 3. (Task 4) publish every pending file and wake-state mutation,
+	// whatever the app's files_durability, as one final manifest of the
+	// generation (ReleaseFlushFiles): create-only, acknowledged before the
+	// entry is journaled, its sequence journaled as manifest_seq
+	seq := 0
+	if w.perRegion > 1 {
+		if b.pubGen != h.Gen {
+			b.pubGen, b.pubSeq, b.releaseSeq = h.Gen, 0, 0
+		}
+		if b.releaseSeq == 0 {
+			b.pubSeq++
+			b.releaseSeq = b.pubSeq
+		}
+		w.issued++
+		bl := &blob{Kind: "files", Inc: h.Inc, Gen: h.Gen, Seq: b.releaseSeq, Files: files.clone(), Timers: append([]int(nil), b.Timers...), Base: w.issued}
+		if !w.ackedPut(b, manifestKey(h.Location, h.Gen, b.releaseSeq), bl, true) {
+			w.stats["release: waits for its manifest"]++
+			return nil
+		}
+		seq, b.releaseSeq = b.releaseSeq, 0
+		b.published = filesState(b.Timers, files)
+	}
+	return &releaseEntry{Box: b.ID, Session: h.Session, Gen: h.Gen, FinalTX: n, ManifestSeq: seq, Flushed: flushed,
 		Files: files, Timers: append([]int(nil), b.Timers...), At: w.now}
 }
 
@@ -207,7 +232,18 @@ func (w *world) selectPin(b *box, c *claim) *pinEntry {
 		w.markStuck(c, fmt.Sprintf("an empty listing of %q is no evidence of an empty database (session %d)", src, h.Session))
 		return nil
 	}
-	return &pinEntry{Gen: src, TX: n, ClaimVer: c.Ver, At: w.now, Files: w.relocFiles(c).clone(), Timers: append([]int(nil), w.relocTimers(c)...)}
+	pin := &pinEntry{Gen: src, TX: n, ClaimVer: c.Ver, At: w.now, Files: w.relocFiles(c).clone(), Timers: append([]int(nil), w.relocTimers(c)...)}
+	// (Task 4) the files pin: the newest landed manifest of the admitted
+	// chain, by exact version, independently of the database baseline
+	// (B2-4); after a release it must reach the release's manifest_seq
+	if mk, mv, ms, mg, _ := w.newestManifest(b.Region, h.Location, h.Gen); mk != "" {
+		if r != nil && r.ManifestSeq > 0 && on("reloc-pin-reaches-release") && (mg != r.Gen || ms < r.ManifestSeq) {
+			w.stats["pin: waits for the release's manifest"]++
+			return nil
+		}
+		pin.ManKey, pin.ManVer, pin.ManSeq, pin.ManGen = mk, mv, ms, mg
+	}
+	return pin
 }
 
 // restoreUpTo restores generation gen of region r from its current
@@ -279,6 +315,9 @@ func (w *world) restoreUpTo(r, inc int, loc, gen string, upto int) *localDB {
 // converted move's or the failover's stand-in for the files publisher
 // (moves §14.2.6). Task 4 puts the pinned manifest first.
 func (w *world) relocFiles(c *claim) *filesDir {
+	if m := w.pinnedManifest(c); m != nil && m.Files != nil {
+		return m.Files
+	}
 	if p := c.Op.Pin; p != nil && p.Files != nil {
 		return p.Files
 	}
@@ -290,6 +329,9 @@ func (w *world) relocFiles(c *claim) *filesDir {
 
 // relocTimers is the wake state the local install replaces timers with.
 func (w *world) relocTimers(c *claim) []int {
+	if m := w.pinnedManifest(c); m != nil {
+		return m.Timers
+	}
 	if p := c.Op.Pin; p != nil && p.Files != nil {
 		return p.Timers
 	}
@@ -364,6 +406,20 @@ func (w *world) markStuck(c *claim, why string) {
 // source, when it is alive and its fence did not discharge it, and every
 // other box this operation handed op.exec to.
 func (w *world) relocationLeftovers(n *claim, op opState) {
+	// every prepared generation this operation built and no writer ever
+	// opened is a dead generation of holder.location: its remote build is
+	// retired by a park-generation queued here (model ruling 16; 1b-next's
+	// CompleteRelocation queues park-local chores only, and nothing else
+	// retires an abandoned P's objects before the at-rest sweep)
+	if h := n.Holder; h != nil {
+		for _, g := range op.Built {
+			if g == h.Gen || w.ancestorGen(h.Location, h.Gen, g) {
+				continue
+			}
+			n.Obl = append(n.Obl, w.scoped(obligation{ID: w.newID("ob"), Op: op.ID, Kind: "park-generation", Region: op.SrcRegion, Box: -1, Prefix: h.Location, Ret: g, Quiet: w.now + horizonH}, w.now, h.Inc))
+			w.stats["relocation: abandoned prepared generation parked"]++
+		}
+	}
 	owed := append([]int{op.Src}, op.InstalledOn...)
 	for _, id := range owed {
 		if id < 0 || id == op.Exec || contains(op.Discharged, id) {
@@ -538,6 +594,9 @@ func (w *world) handExec(n *claim, box int, phase, prepared string) {
 		n.Op.Receipt = nil
 	}
 	n.Op.Attempts = 0
+	if prepared != "" && !hasStr(n.Op.Built, prepared) {
+		n.Op.Built = append(n.Op.Built, prepared)
+	}
 	n.Op.InstalledOn = addUniq(n.Op.InstalledOn, box)
 	n.Boxes = addUniq(n.Boxes, box)
 }
@@ -601,9 +660,30 @@ func (w *world) relocInstalling(b *box, c *claim) {
 	}
 }
 
-// buildPreparedFiles is Task 4's prepared files manifest; before it, the
-// build has nothing to write for files.
-func (w *world) buildPreparedFiles(b *box, c *claim) bool { return true }
+// buildPreparedFiles writes P's prepared files manifest before anything
+// of the database (1b-next Task 8b; CopyPinnedManifest; claim rev 6.30
+// R18-1, moves rev 7.22 §7.6): create-only at sequence 0, bound to
+// {location, P, op id, install_stamp}, with the pinned manifest's files
+// and wake state; the installed CAS waits for its acknowledgement
+// (ToInstalled requires files_seq 0 and the pin's source sequence as
+// provenance). The first admission consumes it as the session
+// publisher's baseline, and the publisher starts at sequence 1 (rule
+// files-prepared-seq-zero); the mutation keeps the source manifest's
+// sequence, as rev 14 did, so the session's first manifests sort below
+// it. In the one-box shape there is no publisher (ruling 11) and nothing
+// to write.
+func (w *world) buildPreparedFiles(b *box, c *claim) bool {
+	if w.perRegion <= 1 {
+		return true
+	}
+	op, h := c.Op, c.Holder
+	seq := 0
+	if !on("files-prepared-seq-zero") && op.Pin != nil {
+		seq = op.Pin.ManSeq
+	}
+	bl := &blob{Kind: "files", Inc: h.Inc, Gen: op.Prepared, Seq: seq, Files: w.relocFiles(c).clone(), Timers: append([]int(nil), w.relocTimers(c)...), Text: fmt.Sprintf("%s/%d", op.ID, op.InstallStamp), Base: w.issued}
+	return w.ackedPut(b, manifestKey(h.Location, op.Prepared, seq), bl, true)
+}
 
 // localInstall advances the executor's local install by one step (§5.8,
 // B1-2; 1b-next Task 8c's Install) and reports whether it is whole: park
@@ -1071,6 +1151,9 @@ func (w *world) enrollStep() {
 func (w *world) twoBoxStep() {
 	w.launchReplacements()
 	w.enrollStep()
+	for _, b := range w.liveBoxes() {
+		w.publishFiles(b)
+	}
 	if !w.calm && w.fail["terminate"] && w.rng.Intn(200) == 0 {
 		bs := w.liveBoxes()
 		if b := bs[w.rng.Intn(len(bs))]; w.regionHAOwnsLoss(b) {
@@ -1097,6 +1180,15 @@ func (w *world) regionHAOwnsLoss(b *box) bool {
 	}
 	switch c.Op.Kind {
 	case "serving", "relocating":
+		if c.Op.Exec == b.ID && w.perRegion > 1 {
+			// finding F2 (model ruling 17): an executor none of whose files
+			// manifests has landed (an adopted legacy host before its first
+			// publication, a new host before its first manifest lands) would
+			// fail over to a fresh instance.key; the sweep leaves it alone,
+			// and TestFailoverBeforeTheFirstManifest shows the loss
+			_, _, _, _, m := w.newestManifest(b.Region, c.Holder.Location, c.Holder.Gen)
+			return m != nil
+		}
 		return true
 	}
 	return !(c.Op.Exec == b.ID || contains(c.Op.Parts, b.ID) || c.Op.Src == b.ID || c.Op.Tgt == b.ID || c.Op.NewBox == b.ID)
@@ -1287,14 +1379,32 @@ func (w *world) declareTimers(x *box, h *holder) {
 	}
 }
 
-// timerCarried is Task 4's: a landed manifest carries the timer. Before
-// the files publisher nothing does.
-func (w *world) timerCarried(x *box, h *holder, id int) bool { return false }
+// timerCarried: the newest landed manifest of the admitted chain carries
+// the timer (Task 4), so the install that follows restores it and the
+// fence does not declare it. INV-28 is the oracle beside it: a timer the
+// manifest published last of the generation carries is never declared,
+// whatever the sequences say.
+func (w *world) timerCarried(x *box, h *holder, id int) bool {
+	_, _, _, _, m := w.newestManifest(x.Region, h.Location, h.Gen)
+	if m != nil && contains(m.Timers, id) {
+		return true
+	}
+	if last := w.lastLandedManifest(x.Region, h.Location, h.Gen); last != nil && contains(last.Timers, id) {
+		w.violate("INV-28: box %d's timer %d is declared lost, but the manifest published last in generation %q carries it (seq %d)", x.ID, id, last.Gen, last.Seq)
+	}
+	return false
+}
 
 // deadBoxFiles is what a fenced box's files directory contributes to the
-// recovery: until Task 4's files publisher, its local directory stands in
-// for what it published (L17), as convertToRelocating's does.
+// recovery: in the one-box shape, which has no files publisher (ruling
+// 11), its local directory stands in for what it published (L17), as
+// convertToRelocating's does; in the two-box shape nothing, because a
+// dead box's disk is never read: the files come from the pinned manifest
+// alone.
 func (w *world) deadBoxFiles(x *box) *filesDir {
+	if w.perRegion > 1 {
+		return nil
+	}
 	return x.Files.clone()
 }
 
@@ -1302,8 +1412,7 @@ func (w *world) deadBoxFiles(x *box) *filesDir {
 // executor (§5.8 reason failover, StartRelocation with a fence; spec 3's
 // placer supplies the decision): op.exec none, the stamp kept, at pinning
 // with the target named there (ruling 4); the pin waits out
-// failoverPinDelay from the fence; deadBoxFiles is the files publisher's
-// stand-in until Task 4.
+// failoverPinDelay from the fence.
 func (w *world) startFailover(n *claim, x *box) {
 	n.Op = opState{Kind: "relocating", ID: w.newID("rl"), Phase: "pinning", Exec: -1, Src: x.ID, Tgt: -1, SrcRegion: x.Region,
 		RelocReason: "failover", ReqAt: w.now, App: n.Holder.App, SrcGen: n.Holder.Gen, SrcStamp: n.Holder.Stamp, StopFiles: w.deadBoxFiles(x)}
@@ -1416,3 +1525,169 @@ func (w *world) fenceExhaustedTarget(n *claim, x *box) {
 	}
 	n.Op.Stuck = why
 }
+
+// ---------- the files publisher and the files pin (region HA §5.6, L13, L17) ----------
+
+// manifestKey is a files manifest of generation gen within loc, by
+// sequence; isManifestKey recognizes one. genOf reads files/ under the
+// origin generation as "".
+func manifestKey(loc, gen string, seq int) string {
+	return dataKey(loc, gen, fmt.Sprintf("files/m-%06d", seq))
+}
+
+func isManifestKey(k string) bool { return strings.Contains(k, "files/m-") }
+
+// filesState is what a manifest carries, as the publisher compares it.
+func filesState(timers []int, f *filesDir) string {
+	if f == nil {
+		return fmt.Sprint(timers)
+	}
+	return fmt.Sprint(timers, f.Key, f.Env)
+}
+
+// publishFiles is the files publisher (§5.6, H6: platform-managed files
+// and wake state sync continuously on every plan): the executor
+// publishes a manifest, files and timers as they stand, whenever that
+// state changed since its last one, at the generation's next sequence
+// (the publisher of a generation starts at 1; a relocation's P has its
+// prepared manifest at 0). The PUT goes through issue, so it may complete
+// late, after the box is terminated: the late-file-upload case. A
+// relocation's target publishes its probe session's state under P
+// (B2-4). Only the two-box shape runs it (ruling 11).
+func (w *world) publishFiles(b *box) {
+	c := w.claim
+	if c == nil || c.Holder == nil || !w.agentUp(b) || b.Row == nil || b.Files == nil || b.Files.Inc != c.Holder.Inc {
+		return
+	}
+	if c.Op.Exec != b.ID || !(c.Op.Kind == "serving" || c.Op.Kind == "relocating" && (b.ID == c.Op.Src || preparedOpened(c))) {
+		return // a relocation's target publishes only once P is opened, into its own generations
+	}
+	h := c.Holder
+	if b.pubGen != h.Gen {
+		b.pubGen, b.pubSeq, b.releaseSeq = h.Gen, 0, 0
+	}
+	state := filesState(b.Timers, b.Files)
+	if state == b.published {
+		return
+	}
+	b.pubSeq++
+	w.issued++
+	bl := &blob{Kind: "files", Inc: h.Inc, Gen: h.Gen, Seq: b.pubSeq, Files: b.Files.clone(), Timers: append([]int(nil), b.Timers...), Base: w.issued}
+	w.issue(b.ID, &request{kind: rPut, region: b.Region, key: manifestKey(h.Location, h.Gen, b.pubSeq), b: bl})
+	b.published = state
+	w.stats["files manifests published"]++
+}
+
+// newestManifest is the files pin's choice (§5.8, B2-4; StorePinner): the
+// newest landed manifest in the admitted chain, holder.generation first,
+// then each generation it superseded (genParent: the files live set's
+// chain, which no trim of holder.admissions shortens; 1b-next rev 12
+// finding 1), by sequence; not the database baseline's generation.
+// Nothing landed: "" and nil.
+func (w *world) newestManifest(r int, loc, gen string) (key string, ver, seq int, mgen string, m *blob) {
+	bk := w.buckets[r]
+	seen := map[string]bool{}
+	for p := dataKey(loc, gen, ""); !seen[p]; {
+		seen[p] = true
+		var best *blob
+		for _, k := range bk.keys(p + "files/") {
+			v := bk.current(k)
+			if v == nil || v.B == nil || v.B.Kind != "files" {
+				continue
+			}
+			if best == nil || v.B.Seq > seq {
+				key, ver, seq, mgen, best = k, v.ID, v.B.Seq, v.B.Gen, v.B
+			}
+		}
+		if best != nil {
+			return key, ver, seq, mgen, best
+		}
+		next, ok := w.genParent[p]
+		if !ok {
+			break
+		}
+		p = next
+	}
+	return "", 0, 0, "", nil
+}
+
+// lastLandedManifest is INV-28's ground truth: of the first generation in
+// the chain that holds a landed manifest, the one published last (the
+// issue order the model records in the blob), whatever its sequence.
+func (w *world) lastLandedManifest(r int, loc, gen string) *blob {
+	_, _, _, mg, m := w.newestManifest(r, loc, gen)
+	if m == nil {
+		return nil
+	}
+	bk := w.buckets[r]
+	last := m
+	for _, k := range bk.keys(dataKey(loc, mg, "files/")) {
+		if v := bk.current(k); v != nil && v.B != nil && v.B.Kind == "files" && v.B.Gen == mg && v.B.Base > last.Base {
+			last = v.B
+		}
+	}
+	return last
+}
+
+// filesLive is the files live set (L13; claim §6.2a "Files in the live
+// set"): a manifest of holder.generation, of a relocation's prepared
+// generation, the one a running relocation's pin names, and the newest
+// landed manifest of the admitted chain (the live manifest, which an
+// unchanged file keeps referencing generations after it was published)
+// is never archived by a park-generation or read as residue. The
+// mutation of files-live-set protects nothing, so a park-generation of an
+// older generation archives the live or the pinned manifest.
+func (w *world) filesLive(c *claim, k string) bool {
+	return on("files-live-set") && w.filesLiveSet(c, k)
+}
+
+// filesLiveSet is the files live set itself, which the residue oracle
+// reads whatever is mutated.
+func (w *world) filesLiveSet(c *claim, k string) bool {
+	if c == nil || c.Holder == nil || !isManifestKey(k) {
+		return false
+	}
+	loc := c.Holder.Location
+	if !strings.HasPrefix(k, loc) {
+		return false
+	}
+	g := genOf(loc, k)
+	if g == c.Holder.Gen {
+		return true
+	}
+	if c.Op.Kind == "relocating" {
+		if c.Op.Pin != nil && k == c.Op.Pin.ManKey {
+			return true
+		}
+		if c.Op.Prepared != "" && g == c.Op.Prepared {
+			return true
+		}
+	}
+	for r := 0; r < nRegions; r++ {
+		if mk, _, _, _, _ := w.newestManifest(r, loc, c.Holder.Gen); mk == k {
+			return true
+		}
+	}
+	return false
+}
+
+// pinnedManifest is the manifest the local install applies: the exact
+// version the pin names (rule files-pin-exact; the model's versioned
+// bucket reads it by version id, where the real store, which has none,
+// reads the pinner's retained copy, 1b-next ruling 21); the mutation
+// reads the newest manifest at install time, which a late PUT from the
+// dead box may have changed since the pin.
+func (w *world) pinnedManifest(c *claim) *blob {
+	p := c.Op.Pin
+	if p == nil || p.ManKey == "" || c.Holder == nil {
+		return nil
+	}
+	if !on("files-pin-exact") {
+		_, _, _, _, m := w.newestManifest(c.Op.SrcRegion, c.Holder.Location, c.Holder.Gen)
+		return m
+	}
+	if v := w.buckets[c.Op.SrcRegion].byID(p.ManKey, p.ManVer); v != nil && !v.Marker {
+		return v.B
+	}
+	return nil
+}
diff --git a/internal/sim/hostlife/regionha_witness_test.go b/internal/sim/hostlife/regionha_witness_test.go
index 4552c10..790220b 100644
--- a/internal/sim/hostlife/regionha_witness_test.go
+++ b/internal/sim/hostlife/regionha_witness_test.go
@@ -62,6 +62,8 @@ func TestUnenrolledReferenceNeverChosen(t *testing.T) {
 	w := twoBoxWitness()
 	from, peer := w.boxes[0], w.boxes[3]
 	w.serve(from, 1, app0)
+	w.publishFiles(from) // its files are in S3 before it dies (Task 4: a dead box's disk is never read)
+	w.completeDue(true)
 	peer.HasKey = false
 	w.terminate(from)
 	w.now += replaceDelay
@@ -114,3 +116,53 @@ func TestTwoWorkersOneChore(t *testing.T) {
 		t.Fatalf("residue after both workers ran the chore: %v", r)
 	}
 }
+
+// TestLateFileUploads (§5.6, §5.8; Review Focus 5): the executor
+// registers a timer, its manifest PUT is held by the witness, and it is
+// terminated. The failover pins the previous manifest, the install
+// applies exactly that version, the held PUT lands after the pin, and
+// the timer it carried is declared, never silently dropped; the late
+// manifest is parked with generation_from.
+func TestLateFileUploads(t *testing.T) {
+	w := twoBoxWitness()
+	w.perRegion = 2
+	from, to := w.boxes[0], w.boxes[3]
+	w.serve(from, 1, app0)
+	w.reach(t, 50, "the host runs on box 0", func() bool { return hasMain(from) }, w.actAll(), func() { w.wake(from) })
+	w.publishFiles(from) // the first manifest lands
+	w.completeDue(true)
+	w.nextW++
+	late := w.nextW
+	from.Timers = append(from.Timers, late)
+	w.acks = append(w.acks, ack{W: late, Inc: 1, Box: from.ID, Session: w.claim.Holder.Session, At: w.now, Kind: "timer"})
+	w.holdKey(w.claim.Holder.Location + "files/")
+	w.publishFiles(from) // the second manifest, held
+	w.hold = nil
+	w.terminate(from)
+	w.reach(t, 1500, "serving on box 3", func() bool {
+		c := w.claim
+		return c.Op.Kind == "serving" && c.Op.Exec == to.ID
+	}, w.actAll(), w.recoveryPass, w.operator, func() { w.wake(to) })
+	if contains(to.Timers, late) {
+		t.Fatalf("the install applied a manifest that had not landed at the pin")
+	}
+	declared := false
+	for _, a := range w.acks {
+		if a.W == late && a.Exempt {
+			declared = true
+		}
+	}
+	if !declared {
+		t.Fatalf("the timer the late manifest carried was not declared with the fence")
+	}
+	if n := w.completeHeld(w.claim.Holder.Location + "files/"); n != 1 {
+		t.Fatalf("held manifest PUTs completed: %d, want 1", n)
+	}
+	w.finish(t)
+	if len(w.violations) > 0 {
+		t.Fatalf("%s", w.violations[0])
+	}
+	if r := w.residue(); len(r) > 0 {
+		t.Fatalf("the late manifest was never parked: %v", r)
+	}
+}
diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go
index 2516bf2..ac25284 100644
--- a/internal/sim/hostlife/rules_test.go
+++ b/internal/sim/hostlife/rules_test.go
@@ -177,4 +177,8 @@ var allRules = []string{
 	"reloc-replacement-table",   // region HA §5.8 (ReplaceTarget): a target lost after P's first admission is a nested failover from holder.generation; the mutation resumes at installed with the same P (the admission rules refuse the reopening: expected miss, see expected-outcomes.txt)
 	"reloc-replace-not-owing",   // 1b-next rev 6 finding 1 (replaceTargetSlot's ErrPendingChore, Worker.next's LocalChoreBoxes): a replacement target never owes a park-local for the host, in the chooser and inside the CAS; the mutation lifts both for a relocation's target
 	"reloc-exhausted-fence",     // 1b-next ruling 23 as rev 9 amended it (FenceExhaustedTarget): an exhausted target's fence while the live source is op.exec records stuck and changes nothing else; the mutation is rev 8's, op.exec none at