amadan

carlos / platform Public

plans: region HA two-box joint model (L18): one or two boxes per region with the one-box sweep byte-identical, relocation by drain through §5.8's phase table, termination with the regional worker's fence, failover, source loss and the replacement table, the files publisher and pin, witnesses and direct tests for every milestone case, the harness's shape and the joint-round brief; Task 1 dry-run against the baseline

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
claude 99a3defee706bd8477957a6fcffdc0c42354d294 parent fbdad38
1 file changed, +3328 −0
  • docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md +3328 −0

CI passed — run details

diff --git a/docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md b/docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md
new file mode 100644
index 000000000..8efd6cdcf
--- /dev/null
+++ b/docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md
@@ -0,0 +1,3328 @@
+# Region HA: the joint model with two boxes per region (L18) Implementation Plan
+
+> **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 define it (drain, failover, pinning, the replacement table, `stuck`), every case claim rev 6.30 §11 names for region HA's validation milestone as a scenario or an invariant with a witness, and one mutation check per new 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:** Seven tasks 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: the release sequence, the pin, the prepared generation, the local install receipt, `released` coverage, the row cases, nested relocation after `probe-failed` and the replacement cap (L1, L9 to L12). Task 3 adds termination by the cloud with the regional worker's fence, automatic enrollment, volume evidence and the discharge rule, failover from `serving`, source loss and the target replacement table with nested failover (H1, H10, H11, H16, H17, H19, L2 to L5). Task 4 adds the files publisher, the files pin and the files live set (§5.6, L13, L17). Task 5 writes the scenarios: deterministic witnesses for every safety guard, direct tests for every liveness, loss or determinism bound, and the claim's §11 extra witnesses. Task 6 wires the two-box shape into `mutate.sh` and `expected-outcomes.txt` and runs the revision's one sweep. Task 7 writes the joint-round brief. Every new rule is a named guard in `rules_test.go` whose name maps to a guard in plan 1b-next (the table in Task 7), so the review can walk from a model catch to the code that must have it.
+
+**Tech Stack:** Go 1.26 test files, standard library only (the model imports nothing else; `hash/fnv` for the tie-break stand-in). `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 `git show origin/plan-region-ha-1b-next:docs/superpowers/plans/2026-10-07-region-ha-1b-next-relocation.md` (Task 1's transitions and guards; Task 11's merge gate; its rulings 6, 9, 10, 11). 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)"; §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.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.
+
+## Rulings made while planning
+
+Each was a gap or a conflict between the authorities. Each says what it costs if it is wrong.
+
+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: Task 1 Step 6 compares the one-box `COUNTERS` line to the baseline's. *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, 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`. *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; the D6 barrier is checked at the installing CAS.** Spec §5.8 has failover pass through `starting` for `to`'s acknowledgement, then `pinning`. The model's converted move already enters at `pinning` with no target (moves §7.10), so one entry point serves both; `to`'s execution lease must be current before `installing` (the plan's `requireAcks` in `ToInstalling`). *Cost if wrong:* a phase the brief must say is collapsed (it does, Task 7); no guard moves.
+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 from `pinning`.** Plan 1b-next ruling 9: `stuck` is not a phase. The spec says the op waits for `carlos ops host resolve`, which it does not define. The model's operator (calm phase) resets the replacement count and replays from `pinning` with a fresh choice; the count is never reset by the worker. *Cost if wrong:* the operator's act is one function; the cap's guard (`reloc-replacement-cap`) stays an operator bound either way.
+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. **The pin's exactness, the failover pin delay, the replacement cap, the D6 barrier, the start guard's L11 exemption and the create choice are liveness, loss or determinism bounds, listed as `missed` with their reasons.** A mutation check needs an invariant violation. Spec §5.8 says itself that the pin delay "is a loss bound, not a safety bound" and that "a later PUT can only add a version nothing reads". These guards are modelled, each has a direct test that shows its effect, and `expected-outcomes.txt` says why no invariant catches them alone. *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 (Task 7).
+10. **Volume evidence is one flag per box.** 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. *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`). In the two-box shape the serving box publishes a manifest whenever its wake state changes, and the pin names one by version. *Cost if wrong:* a one-box drain would also want it; the one-box shape has no drain.
+12. **Plan 1b-next's review findings file was not on its branch.** The brief names `CODEX-PLAN-REGION-HA-1BN-R1.md`; `origin/plan-region-ha-1b-next` holds only `CODEX-PLAN-REGION-HA-1BN-BRIEF-1.md` (the brief, commit eb5e9051). The hazards this plan's guards must catch were taken from that brief's "What to check" list, the plan's Review Focus, and its Self-review's nineteen removed guards. When the findings land, Task 7's table gets a column for them. *Cost if wrong:* a finding with no guard here is a Task 6 addition, not a redesign.
+
+## 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).
+- **Additive.** Moves and the claim own guards in this model. No existing rule's semantics change; existing functions gain branches or calls, never rewrites. New code lives in new files (`twobox_test.go`, `regionha_test.go`, `regionha_witness_test.go`) except where a hook must sit in an existing function.
+- **Every new rule is a named guard**: an entry in `allRules` with a comment naming the spec section and the plan 1b-next guard it maps to, `on("<rule>")` at exactly the decision the rule governs, and an `expected-outcomes.txt` line when it is not caught alone.
+- **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. Liveness and preference guards get direct tests (`TestXxx`), never witnesses.
+- **CPU budget (hard; shared machine).** The gate (300 one-box seeds, 300 two-box seeds, the witnesses, the direct tests) 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). 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 during planning (`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 = 30` steps (10 minutes); `maxReplacements = 2`; `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>")`.
+- **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 comparison.
+
+## Review Focus
+
+1. **Two regional workers acting on one chore.** With two boxes of a region both owning a `park-generation`, each may list, copy and write the manifest; the second manifest must not resurrect a key the first already deleted. Expect the park to converge with no INV-10 residue and no double declaration. Task 3, `TestTwoWorkersOneChore`.
+2. **A drain whose source has a process that escaped the cgroup.** Release step 1 needs the tree empty; an escaped descendant (the model's non-strict process) must fail the step and keep `op.exec` on the source. Expect no handover while it lives (INV-1 if it were handed over). Task 5, `TestReleaseWaitsForEscapedDescendant`.
+3. **A late level-0 PUT from the terminated executor landing after the pin.** The pin names exact versions; the late object lands in `generation_from`, is read by nothing and is parked. Expect no residue at the end and no change to what the replacement restored. Task 5, `TestLatePutAfterTermination`.
+4. **An unenrolled replacement chosen as the target.** It cannot be fenced if it dies, so the operation could never replace it. Expect the chooser to refuse it until enrolled and the relocation to wait. Task 3, `TestUnenrolledReferenceNeverChosen`; Task 5, witness `reloc-enrolled-only`.
+5. **A manifest PUT from the dead box landing incomplete or late.** The install must apply the pinned manifest version, never the newest; timers acknowledged on the dead box after its last manifest are declared, never silently dropped. Task 4, `TestLateFileUploads`; Task 5, witness `fence-declares-timers`.
+
+## 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 | 1, 2, 5 |
+| `internal/sim/hostlife/world_test.go` | Additive fields: `perRegion`, `NewBox`, `Terminated`, `Enrolled`, `EnrollAt`, `DeleteOnTermination`, the relocation journal (`RelocReason`, `FenceAt`, `FailedAt`, `Release`, `Pin`, `Prepared`, `InstallStamp`, `Receipt`, `ProbingSince`, `Replacements`, `Excluded`, `InstalledOn`, `Discharged`, `Stuck`), the publisher's fields, `liteHost.Box`, `clone` | 1, 2, 4, 5 |
+| `internal/sim/hostlife/sim_test.go` | `newWorld`'s second boxes and fault flags, `sweep`, `TestHostLifecycleTwoBox`, the two-box step in `step`, `heal`, INV-27 in `checkStep`, the files live set in `residueOf` | 1, 2, 3, 4 |
+| `internal/sim/hostlife/regionha_test.go` | The relocation phases (`relocStarting` to `relocSettle`), the release sequence, `restoreUpTo`, `userRelocate`, the start guard, `nameReplacement`, `markStuck`, `relocationLeftovers`; termination, replacements, enrollment, the fence worker, failover, source loss, the replacement table; the files publisher, `newestManifest`, `filesLive` | 2, 3, 4 |
+| `internal/sim/hostlife/regionha_witness_test.go` | `twoBoxWitness`, the scenario helpers, the witness functions and the direct tests for the two-box cases | 2, 3, 4, 5 |
+| `internal/sim/hostlife/witness_test.go` | The `witnesses` entries for the new rules (mutate.sh reads this file for rules with witnesses); `newWitness` sets `perRegion: 1` and enrolls its boxes | 1, 2, 5 |
+| `internal/sim/hostlife/console_test.go` | `createSteps` and `recoveryPass` use the recorded executor; `moveTo` chooses; the operator's resolve of a stuck relocation; h2's create records its box | 1, 2, 5 |
+| `internal/sim/hostlife/background_test.go` | `adopt` uses `adoptionOwner`; `replaceDestroyed` fills to `perRegion`; `reconcileClaimed`'s relocation row cases | 1, 2 |
+| `internal/sim/hostlife/moves_test.go` | `workerMode` uses `ownsObligation` and runs the fence step; `relocate` dispatches the phases; `convertToRelocating` sets the failover fields; `release` queues relocation's `park-local` chores; `genOf` and `deadGeneration` know the files live set | 1, 2, 3, 4 |
+| `internal/sim/hostlife/protocol_test.go` | `admits` for the new phases; `admitWriter`'s `released` coverage; `installGen` for P; `appStart`'s `FailApp` for relocation probes; `doObligation`'s `park-generation` keep for the files live set | 2, 4, 5 |
+| `internal/sim/hostlife/rules_test.go` | The new rules, in a "region HA" block at the end | 1 to 4 |
+| `internal/sim/hostlife/expected-outcomes.txt` | The new `missed` and combination entries | 6 |
+| `internal/sim/hostlife/mutate.sh` | `HOSTLIFE_BOXES` pass-through and the verdict's shape tag | 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`)
+
+```
+$ 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. The default `GOCACHE` was refused by the sandbox (`open /home/paulca/.cache/go-build/...: read-only file system`), so every command here used `GOCACHE=$TMPDIR/gocache`.
+
+**Task 1 was dry-run** on this baseline: applied, built, vetted, both shapes run (one-box `300 seeds, 0 failed, 483 completed operations`, COUNTERS identical to the baseline byte for byte; two-box `300 seeds, 0 failed, 447 completed operations`), all witnesses and direct tests passing, then removed. Its code below is the dry-run's, verbatim.
+
+---
+
+### 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 (see above). 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**
+
+```bash
+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.
+
+- [ ] **Step 2: Create `twobox_test.go`**
+
+```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`:
+
+```go
+ 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):
+
+```go
+ 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:
+
+```go
+ 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`:
+
+```go
+ // 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:
+
+```go
+// 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:
+
+```go
+ 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,`:
+
+```go
+ 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:
+
+```go
+ // 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:
+
+```go
+// 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 !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:
+
+```go
+ 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:
+
+```go
+ b := w.createExecutor(c)
+ if b == nil {
+ if nb := w.boxByID(c.Op.NewBox); on("create-choice-once") && (nb == nil || nb.Destroyed) {
+ // the chosen box cannot complete the create: 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`:
+
+```go
+ // 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**
+
+```bash
+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**
+
+```bash
+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
+```
+
+Expected: `ONE-BOX-COUNTERS-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`.
+
+- [ ] **Step 7: Commit**
+
+```bash
+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 (spec §5.8; claim §4 L1; L9, L10, L11, L12; plan 1b-next Task 1, 3, 4, 6, 7)
+
+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`) as they are. The witness `fence-converts-moving` must still pass: it drives a converted operation from `pinning` to `serving` on the replacement box and bounds the claim writes while no box exists at 8.
+
+Guards this task adds (each maps to a plan 1b-next guard; the table is in Task 7):
+`reloc-start-guard` (RelocationStartGuard, L11), `reloc-exec-ack-barrier` (requireAcks, D6), `reloc-release-first` (PinAfterRelease cites the receipt), `reloc-pin-reaches-release` (JournalPin's `final_txid`), `reloc-exec-only-installs` (§5.8 Exclusion, HA2), `reloc-install-receipt` (RecordLocalInstall, ToProbing), `reloc-no-reinstall` (B2-5), `reloc-released-coverage` (L9), `reloc-row-cases` (L12), `reloc-replacement-cap` (replaceTargetSlot's bound; the counting is here, since a nested relocation after `probe-failed` is a replacement).
+
+**Files:**
+- Create: `internal/sim/hostlife/regionha_test.go`
+- Modify: `internal/sim/hostlife/world_test.go` (`box`, `opState`, `claim.clone`), `internal/sim/hostlife/twobox_test.go` (`chooseBoxExcept`), `internal/sim/hostlife/moves_test.go` (`relocate`, `convertToRelocating`, `release`), `internal/sim/hostlife/protocol_test.go` (`admits`, `admitWriter`, `installGen`), `internal/sim/hostlife/background_test.go` (`reconcileClaimed`), `internal/sim/hostlife/console_test.go` (`operator`), `internal/sim/hostlife/sim_test.go` (`step`, `checkStep`), `internal/sim/hostlife/rules_test.go`
+- Test: the gate; `TestDrainEndToEnd` (below)
+
+**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`, `cas`, `sameOp`.
+- Produces: constants `failoverPinDelay`, `probeDeadline`, `maxReplacements`, `enrollDelay`, `replaceDelay`; types `releaseEntry`, `pinEntry`, `receiptEntry`; fields on `box` (`Terminated`, `TerminatedAt`, `Enrolled`, `EnrollAt`, `DeleteOnTermination`, `installEpoch`) and on `opState` (`RelocReason`, `FenceAt`, `FailedAt`, `Release`, `Pin`, `Prepared`, `InstallStamp`, `Receipt`, `ProbingSince`, `Replacements`, `Excluded`, `InstalledOn`, `Discharged`, `Stuck`); `(*world) chooseBoxExcept(r int, app string, except ...int) *box`; `(*world) userRelocate()`; `(*world) relocationStartAllowed(c *claim, from, to *box) bool`; `(*world) relocRelease(b *box, c *claim) *releaseEntry`; `(*world) restoreUpTo(r, inc int, loc, gen string, upto int) *localDB`; `(*world) nameReplacement(n *claim, next int, phase string) bool`; `(*world) markStuck(c *claim, why string)`; `(*world) relocationLeftovers(n *claim, op opState)`; `(*world) relocFiles(c *claim) *filesDir`; `(*world) relocTimers(c *claim) []int`; phase handlers `relocStarting`, `relocReleasing`, `relocPinning`, `relocInstalling`, `relocInstalled`, `relocProbing`, `relocProbeFailed`, `relocSettle`.
+
+- [ ] **Step 1: The additive fields**
+
+`world_test.go`, `type box struct`, after `Nested bool // nested layout: children survive an agent crash`:
+
+```go
+ // 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
+```
+
+`world_test.go`, `type opState struct`, after `NewBox int ...`:
+
+```go
+ // 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
+```
+
+`world_test.go`, before `type digest struct`:
+
+```go
+// 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 {
+ TX int
+ ManKey string
+ ManVer, ManSeq int
+ At 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{ Box, Stamp int }
+```
+
+`world_test.go`, `(c *claim) clone()`, after `n.Op.StopFiles = c.Op.StopFiles.clone()`:
+
+```go
+ 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
+ n.Op.Pin = &cp
+ }
+ if r := c.Op.Receipt; r != nil {
+ cp := *r
+ n.Op.Receipt = &cp
+ }
+```
+
+`sim_test.go`, `newWorld`: every initial box is enrolled. In the first loop's literal add `Enrolled: true,` after `Nested: w.rng.Intn(2) == 0` (no draw), and the same in the two-box loop's literal; in `background_test.go`, `replaceDestroyed`, the literal becomes `nb := &box{ID: 100 + w.nextID, Region: r, HasKey: true, Enrolled: w.perRegion == 1, EnrollAt: w.now, DeleteOnTermination: true}` (one box per region: the replacement is enrolled by hand, as today; two: Task 3's automatic enrollment lands enrollDelay later). In `witness_test.go`, `newWitness`'s box literal gains `Enrolled: true, DeleteOnTermination: true`, and `addBox` (Task 1) gains the same two fields.
+
+`twobox_test.go`: rename `chooseBox`'s body into `chooseBoxExcept` and make `chooseBox` delegate:
+
+```go
+// chooseBox is choose() 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): §2's eligibility
+// adds enrollment (an unenrolled reference is never eligible, HA7; rule
+// reloc-enrolled-only, Task 3).
+func (w *world) chooseBoxExcept(r int, app string, except ...int) *box {
+ bs := w.regionBoxes(r)
+ if len(bs) <= 1 {
+ if len(bs) == 0 || contains(except, bs[0].ID) {
+ return nil
+ }
+ return bs[0]
+ }
+ c := w.claim
+ 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) {
+ continue
+ }
+ if on("reloc-enrolled-only") && !b.Enrolled {
+ 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
+}
+```
+
+(`reloc-enrolled-only` is added to `allRules` in Task 3; add the rule name now in Step 8 so `on` has it, and Task 3 gives it behaviour.)
+
+- [ ] **Step 2: `regionha_test.go`: the start, the start guard, the release sequence, the capped restore**
+
+```go
+package hostlife
+
+import "fmt"
+
+// ---------- relocation (region HA spec 1 §5.8; claim rev 6.30 §4, L1) ----------
+//
+// 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.
+
+const (
+ failoverPinDelay = 2 // §5.8: pin no earlier than the fence's observed_at plus 30 s
+ probeDeadline = 3*probeStartWindow + 10 // §5.8: at most three attempts within the probe deadline (10 minutes)
+ maxReplacements = 2 // §5.8: after two replacements of the target, stuck
+ 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 records the intent,
+// op.exec stays on the source, and both participants acknowledge by
+// writing execution leases (role()). The two-box step draws 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 {
+ return
+ }
+ to := w.chooseBoxExcept(from.Region, c.Holder.App, from.ID)
+ if to == nil || to.Old || !w.relocationStartAllowed(c, from, to) {
+ return
+ }
+ id := w.newID("rl")
+ if w.cas(c, func(n *claim) bool {
+ if n.Op.Kind != "serving" || n.Op.Exec != from.ID {
+ 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: c.Holder.App,
+ SrcGen: c.Holder.Gen, SrcStamp: c.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 (plan 1b-next 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
+}
+
+// relocRelease is the release sequence (§5.8, A3-2) 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"]++
+ }
+ }
+ return &releaseEntry{Box: b.ID, Session: h.Session, Gen: h.Gen, FinalTX: n, Flushed: flushed,
+ Files: b.Files.clone(), Timers: append([]int(nil), b.Timers...), At: w.now}
+}
+
+// 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
+// release's (a drain, a nested relocation), else the converted move's
+// stand-in (moves §14.2.6). Task 4 replaces both with the pinned manifest.
+func (w *world) relocFiles(c *claim) *filesDir {
+ 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 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 (§5.8's replacement table;
+// plan 1b-next 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). It reports whether
+// next was named.
+func (w *world) nameReplacement(n *claim, next int, phase string) bool {
+ 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 plan 1b-next's MarkStuck: a journal entry, never a phase;
+// every relocation step refuses afterwards until the operator resolves it.
+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
+ }
+ 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, 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})
+ }
+}
+```
+
+- [ ] **Step 3: `regionha_test.go`: the phase handlers**
+
+```go
+// relocStarting: the barrier (claim D6). A drain leaves starting for
+// releasing once both participants' execution leases are current (role()
+// writes them on every read of the claim); 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 = "releasing"
+ return true
+ })
+}
+
+// relocReleasing: the source runs the release sequence and journals it;
+// then a worker's CAS cites the entry and leaves for pinning with
+// op.exec none and the stamp kept (claim R6-4, D5's non-installing form).
+// 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 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
+ }
+ 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 pins once the listing reaches the release's
+// final TXID (rule reloc-pin-reaches-release), or, with no release, once
+// the fence's observed_at plus failoverPinDelay has passed (rule
+// reloc-failover-pin-delay, a loss bound); then names a target when the
+// operation has none (a converted move, a resolved stuck operation);
+// then, with every participant's lease current (rule
+// reloc-exec-ack-barrier), hands op.exec to the target for a new
+// installation: a new stamp, journaled as install_stamp, and a fresh
+// prepared generation id (claim R6-4).
+func (w *world) relocPinning(b *box, c *claim) {
+ op, h := c.Op, c.Holder
+ prefix := dataKey(h.Location, h.Gen, "")
+ if op.Pin == nil {
+ n := w.remoteMax(w.buckets[b.Region], prefix)
+ if r := op.Release; r != nil {
+ if on("reloc-pin-reaches-release") && n < r.FinalTX {
+ w.stats["pin: waits for the release's final txid"]++
+ return
+ }
+ } else if on("reloc-failover-pin-delay") && w.now < op.FenceAt+failoverPinDelay {
+ return
+ }
+ pin := &pinEntry{TX: n, At: w.now}
+ 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
+ if ok {
+ n.Op.Pin = pin
+ }
+ return ok
+ }) {
+ w.logf("relocation %s: pinned at TXID %d", op.ID, pin.TX)
+ }
+ return
+ }
+ if op.Tgt < 0 {
+ to := w.chooseBoxExcept(op.SrcRegion, h.App, append([]int{op.Src}, op.Excluded...)...)
+ 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 {
+ n.Op.Tgt = to.ID
+ n.Op.Parts = addUniq(n.Op.Parts, to.ID)
+ }
+ 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 {
+ return false
+ }
+ n.Op.Exec, n.Op.Phase, n.Op.Prepared = to, "installing", w.newID("P")
+ n.Holder.Stamp = w.issueStamp(n, to)
+ n.Op.InstallStamp = n.Holder.Stamp
+ n.Op.Receipt = nil
+ n.Op.BaseKey, n.Op.BaseVer, n.Op.BaseTX = "", 0, 0
+ n.Op.InstalledOn = addUniq(n.Op.InstalledOn, to)
+ n.Boxes = addUniq(n.Boxes, to)
+ return true
+ }) {
+ w.logf("relocation %s: box %d installs with stamp %d", op.ID, to, w.claim.Holder.Stamp)
+ }
+}
+
+// relocInstalling: the target builds P, the remote prepared generation,
+// exactly as a landing builds its generation (moves §7.6, L16): the
+// snapshot [1, N] from the pinned set, create-only and acknowledged, then
+// the level-0 anchor [N, N], acknowledged, then the installed CAS (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
+ if ok {
+ n.Op.Phase = "installed"
+ }
+ return ok
+ }
+ if op.Pin.TX == 0 {
+ w.cas(c, installed)
+ return
+ }
+ if op.BaseKey == "" {
+ db := w.restoreUpTo(b.Region, h.Inc, loc, h.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.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)
+ }
+}
+
+// relocInstalled: the executor's local install (§5.8, B1-2), journaled
+// so the marker is written last: 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, render and materialize with
+// current inputs, then record the receipt by CAS, bound to this box and
+// install_stamp; probing needs that exact receipt (rule
+// reloc-install-receipt). The mutation lets a replacement inherit its
+// predecessor's receipt and skip its own install.
+func (w *world) relocInstalled(b *box, c *claim) {
+ op, h := c.Op, c.Holder
+ 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
+ if ok {
+ n.Op.Phase, n.Op.ProbingSince = "probing", w.now
+ }
+ return ok
+ }
+ if !on("reloc-install-receipt") && op.Receipt != nil {
+ w.cas(c, probing) // the mutation: any receipt will do, the install is skipped
+ return
+ }
+ 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
+ }
+ 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
+ }
+ if b.HasKey {
+ b.Config, b.CfgVer = h.Inc, w.cfgVer[h.App]
+ }
+ b.Live, b.LiveInc = h.App, h.Inc
+ if op.Receipt == nil || op.Receipt.Box != b.ID || op.Receipt.Stamp != op.InstallStamp {
+ 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
+ if ok {
+ n.Op.Receipt = &receiptEntry{Box: b.ID, Stamp: op.InstallStamp}
+ }
+ return ok
+ })
+ return
+ }
+ w.cas(c, probing)
+}
+
+// preparedOpened: an admission has named P (B2-5): the local install is
+// never remade after it.
+func preparedOpened(c *claim) bool {
+ if c.Op.Prepared == "" || c.Holder == nil {
+ return false
+ }
+ for _, e := range c.Holder.Admissions {
+ if e.Gen == c.Op.Prepared {
+ return true
+ }
+ }
+ return false
+}
+
+// relocProbing: each attempt is 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. Three
+// attempts within the probe deadline, then probe-failed. After the first
+// admission the local install is never remade (rule reloc-no-reinstall):
+// a restarted agent that finds its files directory gone goes to stuck;
+// the mutation reapplies the pinned wake state on every 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
+ if op.Exec != b.ID {
+ return
+ }
+ if b.Row == nil || b.Row.Status == "ready" {
+ w.holdRow(b, "relocating", op.ID, c)
+ }
+ opened := preparedOpened(c)
+ if b.Files == nil || b.Files.Gen != op.Prepared {
+ if opened && on("reloc-no-reinstall") {
+ w.markStuck(c, fmt.Sprintf("box %d lost its local install after P was admitted", b.ID))
+ return
+ }
+ w.cas(c, func(n *claim) bool { // before any admission: remake the local install from P (not a reinstall)
+ ok := sameOp(n.Op.ID, op.ID) && n.Op.Kind == "relocating" && n.Op.Phase == "probing" && n.Op.Exec == b.ID
+ if ok {
+ n.Op.Phase, n.Op.Receipt = "installed", nil
+ }
+ return ok
+ })
+ 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
+ }
+ if hasMain(b) || w.spawn(b, c, op.Prepared, true) {
+ w.probeAccepted(b, c)
+ w.cas(c, func(n *claim) bool {
+ ok := sameOp(n.Op.ID, op.ID) && n.Op.Phase == "probing"
+ if ok {
+ n.Op.Phase = "probed"
+ }
+ return ok
+ })
+ return
+ }
+ failed := func(n *claim) bool {
+ ok := sameOp(n.Op.ID, op.ID) && n.Op.Kind == "relocating" && n.Op.Phase == "probing"
+ if ok {
+ n.Op.Phase, n.Op.FailedAt = "probe-failed", w.now
+ }
+ return ok
+ }
+ if w.now > op.ProbingSince+probeDeadline {
+ w.stats["probe-failed: deadline"]++
+ w.cas(c, failed)
+ return
+ }
+ if b.hostFailed && !b.failCounted {
+ b.failCounted = true
+ } else if b.open != nil || b.hostFailed {
+ return
+ }
+ tries := op.ProbeTries + 1
+ w.cas(c, func(n *claim) bool {
+ ok := sameOp(n.Op.ID, op.ID)
+ if ok {
+ n.Op.ProbeTries = tries
+ }
+ return ok
+ })
+ if tries >= probeTries {
+ w.stats["probe-failed: attempts"]++
+ w.cas(c, failed)
+ }
+}
+
+// relocProbeFailed: the live target runs its own release sequence (§5.8
+// probe-failed), then a worker starts the nested relocation from pinning,
+// pinned to at least the target's final TXID (the release entry, which
+// relocPinning reads), the failed target excluded and counted as a
+// replacement. A target that cannot finish its release within the probe
+// deadline goes to stuck: nothing moves away from a live box without its
+// stop evidence.
+func (w *world) relocProbeFailed(b *box, c *claim) {
+ op, h := c.Op, c.Holder
+ if op.Release == nil || op.Release.Box != op.Exec {
+ if b.ID != op.Exec {
+ return
+ }
+ r := w.relocRelease(b, c)
+ if r == nil {
+ if w.now > op.FailedAt+probeDeadline {
+ w.markStuck(c, fmt.Sprintf("box %d cannot finish its release sequence", b.ID))
+ }
+ 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
+ }
+ next := w.chooseBoxExcept(op.SrcRegion, h.App, append([]int{op.Src, op.Exec}, op.Excluded...)...)
+ if next == nil {
+ 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 true // 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 = 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, 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)
+ }
+}
+```
+
+- [ ] **Step 4: Dispatch, admission, coverage, rows, leftovers, the operator**
+
+`moves_test.go`: replace the body of `relocate` (keep its doc comment, rewritten as below) with the dispatch:
+
+```go
+// 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) || !b.Enrolled || op.Stuck != "" {
+ return
+ }
+ switch op.Phase {
+ case "starting":
+ w.relocStarting(b, c)
+ case "releasing":
+ w.relocReleasing(b, c)
+ case "pinning":
+ w.relocPinning(b, c)
+ case "installing":
+ w.relocInstalling(b, c)
+ case "installed":
+ w.relocInstalled(b, c)
+ case "probing":
+ w.relocProbing(b, c)
+ case "probe-failed":
+ w.relocProbeFailed(b, c)
+ case "probed", "opened":
+ w.relocSettle(b, c)
+ }
+}
+```
+
+`moves_test.go`, `convertToRelocating`'s CAS: after `n.Op.Kind, n.Op.Phase, n.Op.Exec, n.Op.FenceBox = "relocating", "pinning", -1, src.ID` add:
+
+```go
+ 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
+```
+
+(`Src` is the move's source already; `Tgt` becomes -1 so pinning names a box of the source's region, not the move's target.)
+
+`moves_test.go`, `release`: inside the CAS closure, before `n.Op = opState{Kind: "serving", ...}`:
+
+```go
+ if op.Kind == "relocating" {
+ w.relocationLeftovers(n, op) // the abandoned installations' park-local chores (claim §4)
+ }
+```
+
+`protocol_test.go`, `admits`, the `case "relocating":` becomes:
+
+```go
+ case "relocating":
+ 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"
+```
+
+`protocol_test.go`, `installGen`:
+
+```go
+func installGen(op *opState) string {
+ switch op.Kind {
+ case "restoring":
+ return op.RollbackID
+ case "relocating":
+ return op.Prepared // P, fresh per installation (region HA §5.8)
+ }
+ return op.ID
+}
+```
+
+`protocol_test.go`, `admitWriter`: in the final block (the operation's prepared generation opened for the first time), after `a.Mode, a.NewGeneration = "cold", want` and before `if covers {`:
+
+```go
+ 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"
+ w.stats["admissions covered: released"]++
+ }
+ return a, true
+ }
+```
+
+and in `admitCommit`, where `Coverage` decides whether `writes_lost` is recorded (the `case a.Coverage == "sealed"` family), add `"released"` beside `"sealed"` wherever a sealed baseline is taken as covering the predecessor (search `"sealed"` in `admitCommit`; there are two sites: the decision not to declare, and the `stats["admissions covered: "+a.Coverage]` line, which needs nothing).
+
+`background_test.go`, `reconcileClaimed`, in the `default:` branch, before `if w.isParticipant(c, b) {`:
+
+```go
+ 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
+ }
+ }
+```
+
+and in `reconcileClaimed`'s `case "serving", "creating", "pushing":`, the stale-hold reopen (`on("stale-hold-release")`) already applies only to `c.Op.Exec == b.ID`; nothing changes there.
+
+`console_test.go`, `operator`, after the quarantined-box readmit loop and before the failed-host loop:
+
+```go
+ // a stuck relocation (§5.8): carlos ops host resolve. The operator
+ // replays it from pinning with a fresh choice and the replacement
+ // count reset, and only when nothing moves away from a live box
+ // without its evidence: the target is gone from execution, released,
+ // or fenced
+ if c.Holder != nil && c.Op.Kind == "relocating" && c.Op.Stuck != "" {
+ op := c.Op
+ if op.Exec < 0 || op.Release != nil && op.Release.Box == op.Exec || contains(c.Lost, op.Exec) {
+ if w.cas(c, func(n *claim) bool {
+ if !sameOp(n.Op.ID, op.ID) || n.Op.Kind != "relocating" || n.Op.Stuck == "" {
+ return false
+ }
+ n.Op.Stuck, n.Op.Replacements = "", 0
+ 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 = 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
+ return true
+ }) {
+ w.stats["operator resolved a stuck relocation"]++
+ w.logf("operator resolved stuck relocation %s from pinning", op.ID)
+ }
+ }
+ return
+ }
+```
+
+`sim_test.go`, `step`: after `w.runStalled()` add
+
+```go
+ if w.perRegion > 1 {
+ w.twoBoxStep() // the two-box shape's own draws, after the one-box ones (ruling 1)
+ }
+```
+
+and in `regionha_test.go`:
+
+```go
+// 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()
+ }
+}
+```
+
+`sim_test.go`, `checkStep`, at the end:
+
+```go
+ // 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)
+ }
+ }
+```
+
+- [ ] **Step 5: The rules**
+
+`rules_test.go`, in the region HA block after `create-choice-once`:
+
+```go
+ "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
+```
+
+- [ ] **Step 6: The direct test**
+
+`regionha_witness_test.go` (created here; Task 5 fills it):
+
+```go
+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)
+ }
+}
+```
+
+- [ ] **Step 7: Run the gate**
+
+```bash
+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: both shapes `0 failed`; the two-box COUNTERS line now has `relocation started: drain`, `relocation`, `admissions covered: released`; `TestDrainEndToEnd` and `TestWitnesses` (including `fence-converts-moving`) pass; `ONE-BOX-COUNTERS-IDENTICAL`. 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 8: Commit**
+
+```bash
+git add internal/sim/hostlife/
+git commit -m "sim: relocation by drain through region HA §5.8's phase table: the release sequence, the pin, the prepared generation, the local install receipt, released coverage, the row cases, nested relocation after probe-failed and the replacement cap; twelve named guards
+
+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; plan 1b-next Task 1 `StartRelocation`, `FenceSource`, `ReplaceTarget`, `fenceBox`, Task 5)
+
+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: the box goes on `lost`, the timers acknowledged on it are declared, 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 (nested failover after P's first admission); a pre-flip move's source converts (existing). Replacement boxes launch after a delay, unenrolled, and enroll automatically after another (H16, H17); an unenrolled reference is never chosen.
+
+Guards: `fence-terminated-only` (§5.9 "What never counts"; H10), `fence-discharge-qualified` (L3, H19), `fence-declares-timers` (moves §7.10 "What a declared-lost box leaves behind"; §5.9 "The loss is recorded twice"), `reloc-source-loss` (B1-6, `FenceSource`), `reloc-replacement-table` (`ReplaceTarget`), `reloc-enrolled-only` (behaviour; the name is from Task 2).
+
+**Files:**
+- Modify: `internal/sim/hostlife/regionha_test.go` (termination, enrollment, the fence, failover, source loss, replacement), `internal/sim/hostlife/moves_test.go` (`workerMode`: the fence step), `internal/sim/hostlife/sim_test.go` (`newWorld`: the terminate fault and volume flags; `heal`), `internal/sim/hostlife/rules_test.go`, `internal/sim/hostlife/regionha_witness_test.go` (two direct tests)
+- Test: the gate; `TestUnenrolledReferenceNeverChosen`, `TestTwoWorkersOneChore`
+
+**Interfaces:**
+- Produces: `(*world) terminate(b *box)`; `(*world) launchReplacements()`; `(*world) enrollStep()`; `(*world) fenceStep(b *box, c *claim)`; `(*world) claimNames(c *claim, x *box) bool`; `(*world) fence(b *box, c *claim, x *box)`; `(*world) fenceBox(n *claim, x *box)`; `(*world) startFailover(n *claim, x *box)`; `(*world) fenceSource(n *claim, x *box)`; `(*world) replaceTarget(n *claim, x *box)`; `(*world) declareTimers(x *box, h *holder)`; `w.fail["terminate"]`; stats `terminated`, `fences written`, `relocation started: failover`.
+
+- [ ] **Step 1: Termination, replacements and enrollment**
+
+`regionha_test.go`:
+
+```go
+// ---------- 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 flags drawn.
+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 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)
+ }
+ }
+}
+```
+
+Replace Task 2's `twoBoxStep` with:
+
+```go
+// twoBoxStep is the two-box shape's extra step, after the one-box draws
+// (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()
+ w.terminate(bs[w.rng.Intn(len(bs))])
+ }
+ if !w.calm && w.rng.Intn(60) == 0 {
+ w.userRelocate()
+ }
+}
+```
+
+`sim_test.go`, `newWorld`, after the two-box box loop (still inside the function, before `return w`):
+
+```go
+ 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)
+ }
+ }
+```
+
+`sim_test.go`, `heal`: the restart of a stopped box becomes `if b.Destroyed && !b.Terminated && w.regionBox(b.Region) == nil && w.rng.Intn(2) == 0 {` (a terminated box never returns; the one-box shape has none, so its draws are unchanged).
+
+- [ ] **Step 2: The fence worker**
+
+`moves_test.go`, `workerMode`, before `w.role(b, c)` (the non-obligation path's last line):
+
+```go
+ w.fenceStep(b, c) // the regional worker's termination fence (region HA §5.9), before its role
+```
+
+`regionha_test.go`:
+
+```go
+// fenceStep is the regional worker's termination fence (§5.9; claim L2
+// to L5): 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.
+func (w *world) fenceStep(b *box, c *claim) {
+ if c == nil || !b.Enrolled || contains(c.Lost, b.ID) {
+ return
+ }
+ 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
+ }
+ w.fence(b, c, x)
+ return
+ }
+}
+
+// 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
+ }
+ return w.owesLocal(c, x)
+}
+
+// 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, and the operation's rule applies.
+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
+ }
+ 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.Op.Kind == "serving" && n.Op.Exec == x.ID:
+ w.startFailover(n, x)
+ case n.Op.Kind == "relocating" && n.Op.Src == x.ID && n.Op.Stuck == "":
+ w.fenceSource(n, x)
+ case n.Op.Kind == "relocating" && n.Op.Tgt == x.ID && n.Op.Stuck == "":
+ w.replaceTarget(n, x)
+ }
+ 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), 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: a discharge without qualifying evidence.
+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
+ qualified := x.DeleteOnTermination
+ if !on("fence-discharge-qualified") {
+ qualified = true
+ }
+ if !qualified {
+ w.stats["fence: park-local chores left open (volume evidence)"]++
+ return
+ }
+ if !x.DeleteOnTermination {
+ w.violate("INV-26: box %d's park-local chores discharged without qualifying volume evidence (§5.9, H19)", x.ID)
+ }
+ var keep []obligation
+ for _, o := range n.Obl {
+ if o.Kind == "park-local" && o.Box == x.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] {
+ 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)
+ }
+}
+
+// startFailover is the fence's start of a relocation for a serving
+// executor (§5.8 reason failover; 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.
+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}
+ w.stats["relocation started: failover"]++
+}
+
+// fenceSource is §5.8's source loss (B1-6, plan 1b-next 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; after its release only its liveness changes.
+// 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, 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 = nil
+ 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 (plan 1b-next 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
+//
+// With no eligible box now, the slot is emptied and the operation falls
+// back to pinning, where a box that enrolls later is named (one step
+// more conservative than the table: P is rebuilt from the same pin). A
+// third replacement marks the operation stuck (nameReplacement). The
+// mutation of reloc-replacement-table resumes every late loss at
+// installed with the same P.
+func (w *world) replaceTarget(n *claim, x *box) {
+ phase := n.Op.Phase
+ next := w.chooseBoxExcept(n.Op.SrcRegion, n.Holder.App, append([]int{n.Op.Src, x.ID}, n.Op.Excluded...)...)
+ if next == nil {
+ 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", phase)
+ w.stats["relocation stuck: replacement cap"]++
+ return
+ }
+ n.Op.Replacements++
+ n.Op.Excluded = addUniq(n.Op.Excluded, x.ID)
+ n.Op.Tgt = -1
+ if phase != "starting" && phase != "releasing" {
+ n.Op.Exec, n.Op.Phase = -1, "pinning"
+ n.Op.Prepared, n.Op.Receipt = "", nil
+ n.Op.BaseKey, n.Op.BaseVer, n.Op.BaseTX = "", 0, 0
+ if preparedOpened(n) || phase == "probe-failed" {
+ n.Op.Pin, n.Op.Release = nil, nil
+ }
+ }
+ w.stats["relocation: target lost, no replacement yet"]++
+ return
+ }
+ if !w.nameReplacement(n, next.ID, phase) {
+ return
+ }
+ w.stats["relocation: target replaced at "+phase]++
+ install := func(p string, prepared string) {
+ n.Op.Exec, n.Op.Phase, n.Op.Prepared = next.ID, p, prepared
+ n.Holder.Stamp = w.issueStamp(n, next.ID)
+ n.Op.InstallStamp = n.Holder.Stamp
+ n.Op.Receipt = nil
+ n.Op.InstalledOn = addUniq(n.Op.InstalledOn, next.ID)
+ n.Boxes = addUniq(n.Boxes, next.ID)
+ }
+ 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
+ install("installing", w.newID("P"))
+ case !late || !on("reloc-replacement-table"):
+ install("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 = 0
+ w.stats["nested failover after P was admitted"]++
+ }
+}
+```
+
+- [ ] **Step 3: Rules**
+
+`rules_test.go`, region HA block:
+
+```go
+ "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
+ "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)
+```
+
+- [ ] **Step 4: Direct tests**
+
+`regionha_witness_test.go`:
+
+```go
+// 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])
+ }
+}
+```
+
+```go
+// 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)
+ }
+}
+```
+
+- [ ] **Step 5: Run the gate; commit**
+
+```bash
+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: both shapes `0 failed`; the two-box COUNTERS carry `terminated`, `fences written`, `relocation started: failover`, `replacements launched`, `boxes enrolled automatically`; `ONE-BOX-COUNTERS-IDENTICAL`. A two-box seed that fails is handled as in Task 2 Step 7.
+
+```bash
+git add internal/sim/hostlife/
+git commit -m "sim: termination by the cloud, automatic enrollment of replacements, the regional worker's fence (lost, timers declared, chores discharged only on qualifying volume evidence), failover from serving, source loss and the target replacement table with nested failover
+
+Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>"
+```
+
+---
+
+### Task 4: The files publisher, the files pin and the files live set (spec §5.6, §5.8 "the files pin", L13, L17; H6, H7; plan 1b-next Task 5 `StorePinner`, Task 1 `RecoveryPin.FilesManifest`)
+
+In the two-box shape the executor publishes a manifest of its files directory and wake state whenever that state changes (continuous sync; the PUT may complete late, after the box is gone). The release sequence's step 3 publishes a final manifest and journals its sequence. The pin names the newest landed manifest in the admitted chain by key and version; a drain's pin must reach the release's sequence. The local install applies the pinned manifest's files and timers, never the newest. The files live set keeps the pinned manifest and the live generation's manifests from every park (L13). The fence's timer declaration narrows to the timers the newest landed manifest does not carry.
+
+Guards: `files-pin-exact` (the install applies the pinned version; a determinism rule, expected miss), `files-live-set` (L13: a `park-generation` never archives a manifest the pin names or the live generation's).
+
+**Files:**
+- Modify: `internal/sim/hostlife/world_test.go` (`box`: `pubSeq`, `published`, `releaseSeq`), `internal/sim/hostlife/regionha_test.go` (publisher, `newestManifest`, `manifestKey`, `isManifestKey`, `filesLive`; `relocRelease` step 3; `relocPinning`'s manifest; `relocFiles`, `relocTimers`; `declareTimers`), `internal/sim/hostlife/moves_test.go` (`genOf`, `deadGeneration`), `internal/sim/hostlife/protocol_test.go` (`doObligation`'s `park-generation` keep), `internal/sim/hostlife/sim_test.go` (`residueOf`), `internal/sim/hostlife/rules_test.go`, `internal/sim/hostlife/regionha_witness_test.go` (`TestLateFileUploads`)
+
+**Interfaces:**
+- Produces: `manifestKey(loc, gen string, seq int) string`; `isManifestKey(k string) bool`; `(*world) publishFiles(b *box)`; `(*world) newestManifest(r int, loc, gen string) (key string, ver, seq int, b *blob)`; `(*world) filesLive(c *claim, k string) bool`; `box.pubSeq`, `box.published`, `box.releaseSeq`.
+
+- [ ] **Step 1: The publisher**
+
+`world_test.go`, `type box struct`, after `installEpoch int ...`:
+
+```go
+ pubSeq int // the files publisher's sequence (§5.6)
+ published string // the wake state and files identity the last manifest carried (in memory)
+ releaseSeq int // the release sequence's final manifest, while its PUT is outstanding
+```
+
+`regionha_test.go`:
+
+```go
+// ---------- 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-") }
+
+// 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. 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" {
+ return
+ }
+ state := fmt.Sprint(b.Timers, b.Files.Key, b.Files.Env)
+ if state == b.published {
+ return
+ }
+ b.pubSeq++
+ bl := &blob{Kind: "files", Inc: c.Holder.Inc, Gen: c.Holder.Gen, Seq: b.pubSeq, Files: b.Files.clone(), Timers: append([]int(nil), b.Timers...)}
+ w.issue(b.ID, &request{kind: rPut, region: b.Region, key: manifestKey(c.Holder.Location, c.Holder.Gen, b.pubSeq), b: bl})
+ b.published = state
+ w.stats["files manifests published"]++
+}
+
+// newestManifest is the files pin's choice (§5.8, B2-4): the newest
+// landed manifest in the admitted chain, holder.generation first, then
+// each generation it superseded (genParent), by sequence; not the
+// database baseline's generation. Nothing landed: "" and nil.
+func (w *world) newestManifest(r int, loc, gen string) (string, int, int, *blob) {
+ bk := w.buckets[r]
+ seen := map[string]bool{}
+ for p := dataKey(loc, gen, ""); p != "" && !seen[p]; p = w.genParent[p] {
+ seen[p] = true
+ key, ver, seq := "", 0, 0
+ 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, best = k, v.ID, v.B.Seq, v.B
+ }
+ }
+ if best != nil {
+ return key, ver, seq, best
+ }
+ }
+ return "", 0, 0, nil
+}
+
+// filesLive is the files live set (L13): a manifest of
+// holder.generation, of a relocation's prepared generation, or the one a
+// running relocation's pin names, is never archived by a park-generation
+// or read as residue. The mutation of files-live-set protects nothing,
+// so a park-generation of generation_from archives the pinned manifest.
+func (w *world) filesLive(c *claim, k string) bool {
+ if !on("files-live-set") || 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
+ }
+ }
+ return false
+}
+```
+
+`twoBoxStep`, after `w.enrollStep()`:
+
+```go
+ for _, b := range w.liveBoxes() {
+ w.publishFiles(b)
+ }
+```
+
+`moves_test.go`, `genOf`: after the `g-` branch, before the data-key test, add:
+
+```go
+ if strings.HasPrefix(rest, "files/") {
+ return "" // a files manifest of the origin generation (region HA §5.6)
+ }
+```
+
+- [ ] **Step 2: The release's final manifest, the pin's manifest, the install's source**
+
+`relocRelease`, replace the final `return &releaseEntry{...}` with:
+
+```go
+ // 3. publish every pending file and wake-state mutation, whatever the
+ // app's files_durability, and record the manifest's final seq: one
+ // PUT, create-only, acknowledged before the entry is journaled
+ if b.releaseSeq == 0 {
+ b.pubSeq++
+ b.releaseSeq = b.pubSeq
+ }
+ bl := &blob{Kind: "files", Inc: h.Inc, Gen: h.Gen, Seq: b.releaseSeq, Files: b.Files.clone(), Timers: append([]int(nil), b.Timers...)}
+ 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 = fmt.Sprint(b.Timers, b.Files.Key, b.Files.Env)
+ return &releaseEntry{Box: b.ID, Session: h.Session, Gen: h.Gen, FinalTX: n, ManifestSeq: seq, Flushed: flushed,
+ Files: b.Files.clone(), Timers: append([]int(nil), b.Timers...), At: w.now}
+```
+
+(`b.Files` may be nil for a host never woken on this box; `clone` handles nil, and `bl.Files` nil is a manifest with no files, which the install treats as Task 2's fresh-identity fallback.)
+
+`relocPinning`, in the `op.Pin == nil` branch, after the release and delay checks and before `pin := ...`:
+
+```go
+ mk, mv, ms, _ := w.newestManifest(b.Region, h.Location, h.Gen)
+ if r := op.Release; r != nil && on("reloc-pin-reaches-release") && ms < r.ManifestSeq {
+ w.stats["pin: waits for the release's manifest"]++
+ return
+ }
+ pin := &pinEntry{TX: n, ManKey: mk, ManVer: mv, ManSeq: ms, At: w.now}
+```
+
+(and delete the earlier `pin := &pinEntry{TX: n, At: w.now}` line).
+
+`relocFiles` and `relocTimers` become:
+
+```go
+// pinnedManifest is the manifest the local install applies: the exact
+// version the pin names (rule files-pin-exact); 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 == "" {
+ return nil
+ }
+ bk := w.buckets[c.Op.SrcRegion]
+ if !on("files-pin-exact") {
+ _, _, _, m := w.newestManifest(c.Op.SrcRegion, c.Holder.Location, c.Holder.Gen)
+ return m
+ }
+ if v := bk.byID(p.ManKey, p.ManVer); v != nil && !v.Marker {
+ return v.B
+ }
+ return nil
+}
+
+// relocFiles is the files directory the local install applies: the
+// pinned manifest's, else the release entry's, else a converted move's
+// stand-in (moves §14.2.6, the one-box shape).
+func (w *world) relocFiles(c *claim) *filesDir {
+ if m := w.pinnedManifest(c); m != nil && m.Files != nil {
+ return m.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 m := w.pinnedManifest(c); m != nil {
+ return m.Timers
+ }
+ if r := c.Op.Release; r != nil {
+ return r.Timers
+ }
+ return nil
+}
+```
+
+`declareTimers`: narrow to what no landed manifest carries. Replace its loop's condition with:
+
+```go
+ _, _, _, m := w.newestManifest(x.Region, h.Location, h.Gen)
+ carried := map[int]bool{}
+ if m != nil {
+ for _, id := range m.Timers {
+ carried[id] = true
+ }
+ }
+ 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] && !carried[a.W] {
+ a.Exempt = true
+ n++
+ }
+ }
+```
+
+- [ ] **Step 3: The live set in every park and the residue oracle**
+
+`protocol_test.go`, `doObligation`, the `park-generation` keep:
+
+```go
+ keep = func(k string) bool { return genOf(o.Prefix, k) != retire || w.filesLive(c, k) || inner != nil && inner(k) }
+```
+
+`moves_test.go`, `deadGeneration`, first line of the body after `h := c.Holder`:
+
+```go
+ if w.filesLive(c, k) {
+ return false
+ }
+```
+
+`sim_test.go`, `residueOf`, the `continue` condition gains `|| r == serving && w.filesLive(c, k)`:
+
+```go
+ if strings.HasSuffix(k, "lock.json") || (r == serving && (live[k] || isDataKey(k) && live[genPrefixOf(k)] || isClosedKey(k) && live[k[:strings.LastIndex(k, "closed/")+7]] || w.filesLive(c, k))) {
+```
+
+(`c` is `w.claim` in that function; `filesLive` handles nil.)
+
+- [ ] **Step 4: Rules and the direct test**
+
+`rules_test.go`, region HA block:
+
+```go
+ "files-pin-exact", // region HA §5.8 the pinned recovery set, B2-4 (RecoveryPin.FilesManifest, StorePinner): the local install applies the manifest version the pin names; the mutation reads the newest at install time. A determinism rule: a later PUT adds a version nothing reads (expected miss)
+ "files-live-set", // region HA §5.6, L13 (the classifier's files live set): a park-generation never archives a manifest the pin names, the live generation's, or P's; the mutation archives the pinned manifest with its dead generation
+```
+
+`regionha_witness_test.go`:
+
+```go
+// 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)
+ }
+}
+```
+
+- [ ] **Step 5: Run the gate; commit**
+
+```bash
+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/task4.log | grep -E "seeds, |^--- FAIL|^ok|^FAIL|^ sim_test.go:[0-9]+: seed"
+diff $TMPDIR/twobox/baseline-counters.json <(grep COUNTERS $TMPDIR/twobox/task4.log | head -1 | sed 's/.*COUNTERS //') && echo ONE-BOX-COUNTERS-IDENTICAL
+```
+
+Expected: both shapes `0 failed`; the two-box COUNTERS carry `files manifests published`; `ONE-BOX-COUNTERS-IDENTICAL` (the publisher runs only in the two-box step; the one-box release path is never reached).
+
+```bash
+git add internal/sim/hostlife/
+git commit -m "sim: the files publisher, the release's final manifest, the files pin by exact version, the files live set kept from every park, and timers declared only when no landed manifest carries them
+
+Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>"
+```
+
+---
+
+### Task 5: The scenarios: witnesses for every safety guard, direct tests for every bound, and claim §11's extra witnesses
+
+Every case claim rev 6.30 §11 lists for the milestone gets a scenario here, and every guard from Tasks 1 to 4 gets its mutation evidence: a witness (holds with the rule, violates its named failure under the mutation) for a safety guard, a direct test for a liveness, loss or determinism bound (ruling 8). The witness entries must live in `witness_test.go`'s `witnesses` slice (mutate.sh reads that file for the rules that have witnesses); the scenario functions live in `regionha_witness_test.go`.
+
+| Required case (claim §11, spec L18) | Scenario | Kind |
+|---|---|---|
+| create spread | `TestCreateSpread` | direct (preference, H4) |
+| relocation by drain | `TestDrainEndToEnd` (Task 2), `wRelocReleaseFirst` | direct, witness |
+| termination during serving | `wFenceDeclaresTimers`, `wRelocReleasedCoverage`, `TestLatePutAfterTermination` | witness, direct |
+| termination in every relocation phase | `TestTerminationInEveryRelocationPhase` | direct (the replacement table) |
+| nested failover | `TestNestedFailover`, `wFilesLiveSet` | direct, witness |
+| stale edges file | `wRelocRowCases`, `TestStaleEdgesFile` | witness, direct |
+| unenrolled reference | `wRelocEnrolledOnly`, `TestUnenrolledReferenceNeverChosen` (Task 3) | witness, direct |
+| a volume without DeleteOnTermination | `wFenceDischargeQualified`, `TestAdverseVolume` | witness, direct |
+| crashes during installation | `TestCrashMidInstall` | direct |
+| late file uploads | `TestLateFileUploads` (Task 4) | direct |
+| late PUTs after termination | `TestLatePutAfterTermination` | direct |
+| §11: start racing purge or admission closure | `TestRelocationStartRacesPurge` | direct |
+| §11: empty-database drain with files and timers | `TestEmptyDatabaseDrain` | direct |
+| §11: generation parking while relocation pins referenced files | `wFilesLiveSet` | witness |
+| §11: first `released` admission followed by an uncertified failed probe | `TestReleasedThenFailedProbe` | direct |
+| §11: the one-box conversion holding at `pinning` | `wFenceConvertsMoving` (existing) | witness |
+| the two-replacement cap and `stuck` | `TestStuckAfterTwoReplacements` | direct |
+| two regional workers on one chore | `TestTwoWorkersOneChore` (Task 3) | direct |
+| an escaped descendant at the release | `TestReleaseWaitsForEscapedDescendant` | direct |
+
+**Files:**
+- Create/extend: `internal/sim/hostlife/regionha_witness_test.go`
+- Modify: `internal/sim/hostlife/witness_test.go` (the `witnesses` entries), `internal/sim/hostlife/world_test.go` (`liteHost.Box`), `internal/sim/hostlife/console_test.go` (h2's create records its box), `internal/sim/hostlife/twobox_test.go` (`hostsOn` counts h2), `internal/sim/hostlife/protocol_test.go` (`appStart`: `FailApp` applies to relocation probes)
+
+- [ ] **Step 1: The second host's box, and FailApp for relocation probes**
+
+`world_test.go`, `type liteHost struct`, after `App string`: `Box int // the box its create named (region HA §5.2); control-plane only`.
+
+`console_test.go`, `createSteps` case 1, the h2 branch: `w.h2 = liteHost{Inc: p.Inc, App: p.App, Kind: "creating", OpID: p.OpID, At: w.now}` gains `Box: w.h2Box(p.App)`, with, beside `createExecutor`:
+
+```go
+// h2Box is the executor the second host's create names (region HA §5.2):
+// choose() in region 0, where the model keeps the control-plane-only
+// host. With one box per region it is box 0, as the model always implied.
+func (w *world) h2Box(app string) int {
+ if b := w.chooseBox(0, app); b != nil {
+ return b.ID
+ }
+ return 0
+}
+```
+
+`twobox_test.go`, `hostsOn`: before `c := w.claim`, add
+
+```go
+ n := 0
+ if w.h2.Kind != "" && w.h2.Box == b.ID && (app == "" || w.h2.App == app) {
+ n = 1
+ }
+```
+
+and make every `return 1` into `return n + 1` and the final `return 0` into `return n`.
+
+`protocol_test.go`, `appStart`: `healthy := !(probe && b.FailApp && c.Op.Kind == "landing")` becomes `healthy := !(probe && b.FailApp && (c.Op.Kind == "landing" || c.Op.Kind == "relocating"))` (the injected "the target cannot run it" fault applies to relocation probes as to landing probes; the one-box shape has no relocation probe on a `FailApp` box, since its converted move's replacement box is created with `FailApp` false).
+
+- [ ] **Step 2: The witness entries**
+
+`witness_test.go`, at the end of `witnesses` (before the closing `}`):
+
+```go
+ // region HA, two boxes per region (L18; plan 2026-10-07-region-ha-hostlife-two-box)
+ {"reloc-release-first", "reloc-release-first", "INV-1",
+ "a drain: the worker pins while the source still runs the host; the target's probe starts beside it", wRelocReleaseFirst},
+ {"reloc-exec-only-installs", "reloc-exec-only-installs", "INV-6",
+ "a drain: the released source, in the region but not op.exec, activates the installation stamp issued for the target", wRelocExecOnlyInstalls},
+ {"reloc-install-receipt", "reloc-install-receipt", "INV-4",
+ "the target is terminated at installed, after its receipt; its replacement inherits the receipt, skips its local install and starts over data sealed with the old key", wRelocInstallReceipt},
+ {"reloc-no-reinstall", "reloc-no-reinstall", "acknowledged timer",
+ "the first probe admitted P and registered a timer; the agent restarts and re-applies the pinned wake state over it", wRelocNoReinstall},
+ {"reloc-released-coverage", "reloc-released-coverage", "INV-2",
+ "a failover: the executor is terminated with an acknowledged write whose upload is still in flight; the first admission of P takes released coverage and the write is neither restored nor declared", wRelocReleasedCoverage},
+ {"reloc-source-loss", "reloc-source-loss", "INV-2",
+ "a drain whose source is terminated in releasing before its receipt, with an unuploaded write; taken as released at what the remote holds, the write goes undeclared", wRelocSourceLoss},
+ {"reloc-row-cases", "reloc-row-cases,exec-admission,hold-op-open,start-check-claim-gen,exec-writer", "INV-1",
+ "a stale edges file: after the drain the former executor's held row is reopened as ready, a request reaches it, and with the admission fences down it runs the host beside the new executor", wRelocRowCases},
+ {"reloc-start-guard", "reloc-start-guard", "INV",
+ "a drain started over a park-local chore owed by the target: the chore retires the fresh installation under the target", wRelocStartGuard},
+ {"fence-discharge-qualified", "fence-discharge-qualified", "INV-26",
+ "a terminated box with a volume that was not DeleteOnTermination has its park-local chores discharged automatically", wFenceDischargeQualified},
+ {"fence-declares-timers", "fence-declares-timers", "acknowledged timer",
+ "the executor registers a timer after its last manifest and is terminated; the fence drops the timer silently", wFenceDeclaresTimers},
+ {"reloc-enrolled-only", "reloc-enrolled-only", "INV-27",
+ "the only other box of the region holds no key and a replacement has launched unenrolled; the failover names the unenrolled reference", wRelocEnrolledOnly},
+ {"files-live-set", "files-live-set", "INV-4",
+ "the pinned manifest lives in generation_from; its park-generation archives it, and the nested failover's install starts over data sealed with a key the fresh files directory does not carry", wFilesLiveSet},
+```
+
+- [ ] **Step 3: The scenario helpers and the witnesses**
+
+`regionha_witness_test.go` (add to Task 2's file):
+
+```go
+// twoBox turns a witness world into the two-box shape.
+func (w *world) twoBox() {
+ w.perRegion = 2
+ for r := 0; r < nRegions; r++ {
+ w.addBox(r)
+ }
+}
+
+// extraBox enrolls a third box in region r with the given id (a
+// replacement for the replacement in the nested scenarios).
+func (w *world) extraBox(r, id int) *box {
+ b := &box{ID: id, Region: r, HasKey: true, Enrolled: true, DeleteOnTermination: true}
+ b.forget()
+ w.boxes = append(w.boxes, b)
+ return b
+}
+
+// running drives the serving host until it runs on b.
+func (w *world) running(t *testing.T, b *box) {
+ w.reach(t, 60, "the host runs", func() bool { return hasMain(b) }, w.actAll(), func() { w.wake(b) })
+}
+
+// drainTo starts a drain of the serving host to the region's other box
+// and fails the test if it did not start.
+func (w *world) drainTo(t *testing.T, to *box) {
+ w.userRelocate()
+ if c := w.claim; c.Op.Kind != "relocating" || c.Op.Tgt != to.ID {
+ t.Fatalf("witness: the drain to box %d did not start: %s", to.ID, w.state())
+ }
+}
+
+// relocPhase drives until the relocation is in phase p (or beyond it, by
+// the table's order), with the actors given.
+func (w *world) relocPhase(t *testing.T, p string, actors ...func()) bool {
+ order := []string{"starting", "releasing", "pinning", "installing", "installed", "probing", "probed", "opened"}
+ at := func(x string) int {
+ for i, o := range order {
+ if o == x {
+ return i
+ }
+ }
+ return -1
+ }
+ return w.reach(t, 1500, "relocation at "+p, func() bool {
+ c := w.claim
+ return c.Op.Kind == "relocating" && at(c.Op.Phase) >= at(p) || c.Op.Kind == "serving" && p == "serving"
+ }, actors...)
+}
+
+// servingOn drives until the host serves on b (any box, when b is nil).
+func (w *world) servingOn(t *testing.T, b *box) bool {
+ return w.reach(t, 2000, "serving on the new executor", func() bool {
+ c := w.claim
+ return c.Op.Kind == "serving" && (b == nil && c.Op.Exec >= 0 || b != nil && c.Op.Exec == b.ID)
+ }, w.actAll(), w.recoveryPass, w.operator, w.wakeExec)
+}
+
+// wakeExec wakes the executor, whichever box it is.
+func (w *world) wakeExec() {
+ if e := w.execBox(w.claim); e != nil {
+ w.wake(e)
+ }
+}
+
+// timerOn registers an acknowledged timer on b's running host.
+func (w *world) timerOn(b *box) int {
+ w.nextW++
+ b.Timers = append(b.Timers, w.nextW)
+ sess, gen := w.sessionOf(b)
+ w.acks = append(w.acks, ack{W: w.nextW, Inc: w.claim.Holder.Inc, Box: b.ID, Session: sess, Gen: gen, At: w.now, Kind: "timer"})
+ return w.nextW
+}
+
+func wRelocReleaseFirst(t *testing.T, w *world) {
+ w.twoBox()
+ from, to := w.boxes[0], w.boxes[3]
+ w.serve(from, 1, app0)
+ w.running(t, from)
+ w.drainTo(t, to)
+ w.servingOn(t, to)
+ w.finish(t)
+}
+
+func wRelocExecOnlyInstalls(t *testing.T, w *world) {
+ w.twoBox()
+ from, to := w.boxes[0], w.boxes[3]
+ w.serve(from, 1, app0)
+ w.running(t, from)
+ w.drainTo(t, to)
+ w.servingOn(t, to)
+ w.finish(t)
+}
+
+func wRelocInstallReceipt(t *testing.T, w *world) {
+ w.twoBox()
+ from, to := w.boxes[0], w.boxes[3]
+ third := w.extraBox(0, 30)
+ w.serve(from, 1, app0)
+ w.running(t, from)
+ w.drainTo(t, to)
+ if !w.reach(t, 1500, "the target's receipt", func() bool {
+ c := w.claim
+ return c.Op.Kind == "relocating" && c.Op.Phase == "installed" && c.Op.Receipt != nil && c.Op.Receipt.Box == to.ID
+ }, w.act(from, to), w.recoveryPass) {
+ return
+ }
+ w.terminate(to)
+ w.servingOn(t, third)
+ w.finish(t)
+}
+
+func wRelocNoReinstall(t *testing.T, w *world) {
+ w.twoBox()
+ from, to := w.boxes[0], w.boxes[3]
+ w.serve(from, 1, app0)
+ w.running(t, from)
+ w.drainTo(t, to)
+ if !w.reach(t, 1500, "the probe runs on the target", func() bool {
+ return preparedOpened(w.claim) && hasMain(to)
+ }, w.act(from, to), w.recoveryPass) {
+ return
+ }
+ w.timerOn(to)
+ w.crash(to)
+ w.servingOn(t, to)
+ w.finish(t)
+}
+
+func wRelocReleasedCoverage(t *testing.T, w *world) {
+ w.twoBox()
+ from, to := w.boxes[0], w.boxes[3]
+ w.serve(from, 1, app0)
+ w.running(t, from)
+ w.appWrite(from)
+ w.holdKey(w.claim.Holder.Location) // every upload of the executor is held
+ w.replicate(from)
+ w.hold = nil
+ w.terminate(from)
+ w.servingOn(t, to)
+ w.finish(t)
+}
+
+func wRelocSourceLoss(t *testing.T, w *world) {
+ w.twoBox()
+ from, to := w.boxes[0], w.boxes[3]
+ w.serve(from, 1, app0)
+ w.running(t, from)
+ w.appWrite(from)
+ w.holdKey(w.claim.Holder.Location) // the flush and the final manifest are held: no receipt
+ w.drainTo(t, to)
+ w.relocPhase(t, "releasing", w.act(from, to), w.recoveryPass)
+ w.drive(20, func() bool { return false }, w.act(from, to))
+ if w.claim.Op.Release != nil {
+ t.Fatalf("witness: the release was journaled while its uploads were held")
+ }
+ w.hold = nil
+ w.terminate(from)
+ w.servingOn(t, to)
+ w.finish(t)
+}
+
+func wRelocRowCases(t *testing.T, w *world) {
+ w.twoBox()
+ from, to := w.boxes[0], w.boxes[3]
+ w.serve(from, 1, app0)
+ w.running(t, from)
+ w.drainTo(t, to)
+ w.servingOn(t, to)
+ // the former executor still holds a row (its park-local has not run):
+ // reconcile decides it, and a request reaches the box through its
+ // stale edges file
+ w.drive(30, func() bool { return false }, func() {
+ w.reconcile(from)
+ w.wake(from)
+ w.worker(to)
+ w.reconcile(to)
+ })
+ w.finish(t)
+}
+
+func wRelocStartGuard(t *testing.T, w *world) {
+ w.twoBox()
+ from, to := w.boxes[0], w.boxes[3]
+ w.serve(from, 1, app0)
+ w.running(t, from)
+ // the target owes a park-local from an earlier stay: stale artifacts under an old stamp
+ to.DB = &localDB{Inc: 1, Loc: w.claim.Holder.Location, State: map[string]int{}, Stamp: 7, Epoch: to.Epoch}
+ to.install(1, 7)
+ w.claim.Obl = append(w.claim.Obl, obligation{ID: w.newID("ob"), Op: "stay", Kind: "park-local", Box: to.ID, Region: -1, Ret: "stay"})
+ w.userRelocate()
+ if on("reloc-start-guard") && w.claim.Op.Kind == "relocating" {
+ t.Fatalf("witness: the drain started over the target's park-local")
+ }
+ w.servingOn(t, nil)
+ w.finish(t)
+}
+
+func wFenceDischargeQualified(t *testing.T, w *world) {
+ w.twoBox()
+ from, to := w.boxes[0], w.boxes[3]
+ from.DeleteOnTermination = false
+ w.serve(from, 1, app0)
+ w.running(t, from)
+ w.drainTo(t, to)
+ w.servingOn(t, to)
+ if !w.owesLocal(w.claim, from) {
+ t.Fatalf("witness: the former executor owes no park-local: %s", w.state())
+ }
+ w.terminate(from)
+ w.reach(t, 60, "the former executor fenced", func() bool { return contains(w.claim.Lost, from.ID) }, w.act(to))
+ w.finish(t)
+}
+
+func wFenceDeclaresTimers(t *testing.T, w *world) {
+ w.twoBox()
+ from, to := w.boxes[0], w.boxes[3]
+ w.serve(from, 1, app0)
+ w.running(t, from)
+ w.publishFiles(from)
+ w.completeDue(true)
+ w.timerOn(from) // after the last manifest
+ w.terminate(from)
+ w.servingOn(t, to)
+ w.finish(t)
+}
+
+func wRelocEnrolledOnly(t *testing.T, w *world) {
+ w.twoBox()
+ from, peer := w.boxes[0], w.boxes[3]
+ w.serve(from, 1, app0)
+ peer.HasKey = false
+ w.terminate(from)
+ w.now += replaceDelay
+ w.launchReplacements()
+ w.reach(t, 100, "the executor fenced", func() bool { return contains(w.claim.Lost, from.ID) }, w.act(peer), w.recoveryPass)
+ w.drive(enrollDelay, func() bool { return false }, w.actAll(), w.recoveryPass) // under the mutation the unenrolled replacement is named here (INV-27)
+ w.now += enrollDelay
+ w.enrollStep()
+ w.servingOn(t, nil)
+ w.finish(t)
+}
+
+func wFilesLiveSet(t *testing.T, w *world) {
+ w.twoBox()
+ from, to := w.boxes[0], w.boxes[3]
+ third := w.extraBox(0, 30)
+ w.serve(from, 1, app0)
+ w.running(t, from)
+ w.timerOn(from)
+ w.drainTo(t, to)
+ if !w.reach(t, 1500, "P admitted and generation_from's park-generation queued", func() bool {
+ c := w.claim
+ if !preparedOpened(c) {
+ return false
+ }
+ for _, o := range c.Obl {
+ if o.Kind == "park-generation" && o.Region == 0 {
+ return true
+ }
+ }
+ return false
+ }, w.act(from, to), w.recoveryPass, func() { w.wake(to) }) {
+ return
+ }
+ // the park runs to completion while the relocation is still open; the
+ // pinned manifest in generation_from must survive it
+ w.reach(t, 1500, "generation_from parked", func() bool {
+ for _, o := range w.claim.Obl {
+ if o.Kind == "park-generation" && o.Region == 0 {
+ return false
+ }
+ }
+ return true
+ }, w.act(from, to), w.recoveryPass)
+ w.terminate(to) // after P's first admission: a nested failover pins from P, whose files pin is generation_from's manifest
+ w.servingOn(t, third)
+ w.finish(t)
+}
+```
+
+- [ ] **Step 4: The direct tests**
+
+```go
+func TestCreateSpread(t *testing.T) {
+ w := twoBoxWitness()
+ w.serve(w.boxes[0], 1, app0)
+ w.h2 = liteHost{}
+ w.console = append(w.console, &consolePlan{Kind: "create", Host: "h2", App: app0, OpID: w.newID("cr"), Inc: 9})
+ w.reach(t, 50, "the second host of app A placed", func() bool { return w.h2.Kind == "serving" }, w.runConsole)
+ if w.h2.Box != 3 {
+ t.Fatalf("spread: the second instance of app A landed on box %d, want the box running none (3)", w.h2.Box)
+ }
+ w.h2 = liteHost{}
+ w.console = append(w.console, &consolePlan{Kind: "create", Host: "h2", App: app1, OpID: w.newID("cr"), Inc: 10})
+ w.reach(t, 50, "the second host of app B placed", func() bool { return w.h2.Kind == "serving" }, w.runConsole)
+ want := 0
+ if tieHash(3) > tieHash(0) {
+ want = 3
+ }
+ if w.h2.Box != want {
+ t.Fatalf("tie-break: app B landed on box %d, want the greater tieHash (%d); hosts on 0: %d, on 3: %d", w.h2.Box, want, w.hostsOn(w.boxes[0], ""), w.hostsOn(w.boxes[3], ""))
+ }
+}
+
+// TestTerminationInEveryRelocationPhase: a drain driven to each phase of
+// §5.8's table; the source or the target is terminated there; the
+// operation converges by the replacement table, with no violation.
+func TestTerminationInEveryRelocationPhase(t *testing.T) {
+ for _, who := range []string{"from", "to"} {
+ for _, phase := range []string{"starting", "releasing", "pinning", "installing", "installed", "probing", "probed", "opened"} {
+ t.Run(who+"@"+phase, func(t *testing.T) {
+ w := twoBoxWitness()
+ from, to := w.boxes[0], w.boxes[3]
+ w.extraBox(0, 30)
+ w.serve(from, 1, app0)
+ w.running(t, from)
+ w.appWrite(from)
+ w.timerOn(from)
+ w.drainTo(t, to)
+ if !w.relocPhase(t, phase, w.act(from, to), w.recoveryPass, func() { w.wake(to) }) {
+ t.Fatalf("%s", w.violations[0])
+ }
+ if who == "from" {
+ w.terminate(from)
+ } else {
+ w.terminate(to)
+ }
+ w.servingOn(t, nil)
+ w.finish(t)
+ if len(w.violations) > 0 {
+ t.Fatalf("%s", w.violations[0])
+ }
+ t.Logf("%s terminated at %s: fences %d, replaced %v, nested %d, converted %d", who, phase, w.stats["fences written"],
+ w.stats["relocation: target replaced at "+phase] > 0, w.stats["nested failover after P was admitted"], w.stats["relocation: source lost before its release, converted to failover"])
+ })
+ }
+ }
+}
+
+func TestNestedFailover(t *testing.T) {
+ w := twoBoxWitness()
+ from, to := w.boxes[0], w.boxes[3]
+ third := w.extraBox(0, 30)
+ w.serve(from, 1, app0)
+ w.running(t, from)
+ w.drainTo(t, to)
+ w.reach(t, 1500, "the probe runs on the target", func() bool { return preparedOpened(w.claim) && hasMain(to) }, w.act(from, to), w.recoveryPass, func() { w.wake(to) })
+ wr := w.appWrite(to)
+ w.replicate(to)
+ w.completeDue(true) // the target's write is replicated before it dies
+ w.terminate(to)
+ w.servingOn(t, third)
+ w.finish(t)
+ if len(w.violations) > 0 {
+ t.Fatalf("%s", w.violations[0])
+ }
+ if !contains(third.DB.Log, wr) {
+ t.Fatalf("the nested failover lost the target's replicated write %d", wr)
+ }
+ if w.stats["nested failover after P was admitted"] != 1 {
+ t.Fatalf("no nested failover: %v", w.stats)
+ }
+}
+
+func TestStaleEdgesFile(t *testing.T) {
+ w := twoBoxWitness()
+ from, to := w.boxes[0], w.boxes[3]
+ w.serve(from, 1, app0)
+ w.running(t, from)
+ w.drainTo(t, to)
+ w.servingOn(t, to)
+ if from.Row == nil || from.Row.Status == "ready" {
+ t.Fatalf("the former executor's row is not held: %+v", from.Row)
+ }
+ w.drive(30, func() bool { return false }, func() { w.reconcile(from); w.wake(from) })
+ if hasMain(from) {
+ t.Fatalf("a request through the stale edges file started the host on the former executor")
+ }
+ w.finish(t)
+ if len(w.violations) > 0 {
+ t.Fatalf("%s", w.violations[0])
+ }
+}
+
+func TestAdverseVolume(t *testing.T) {
+ w := twoBoxWitness()
+ from, to := w.boxes[0], w.boxes[3]
+ from.DeleteOnTermination = false
+ w.serve(from, 1, app0)
+ w.running(t, from)
+ w.terminate(from)
+ w.servingOn(t, to) // execution recovery proceeds (H19)
+ if w.stats["fence: park-local chores left open (volume evidence)"]+w.stats["fence: park-local chores discharged"] != 0 {
+ t.Logf("fence stats: %v", w.stats)
+ }
+ if contains(w.claim.Op.Discharged, from.ID) {
+ t.Fatalf("the fence discharged chores without qualifying evidence")
+ }
+ if !w.owesLocal(w.claim, from) {
+ t.Fatalf("the dead box's park-local is not open for the operator: %s", w.state())
+ }
+ w.finish(t) // the operator's destroyed-local declaration clears it
+ if len(w.violations) > 0 {
+ t.Fatalf("%s", w.violations[0])
+ }
+}
+
+func TestCrashMidInstall(t *testing.T) {
+ for _, at := range []string{"installing", "installed"} {
+ t.Run(at, func(t *testing.T) {
+ w := twoBoxWitness()
+ from, to := w.boxes[0], w.boxes[3]
+ w.serve(from, 1, app0)
+ w.running(t, from)
+ w.timerOn(from)
+ w.drainTo(t, to)
+ w.relocPhase(t, at, w.act(from, to), w.recoveryPass)
+ w.drive(2, func() bool { return false }, w.act(to)) // a step into the phase: a PUT issued, a files directory extracted
+ w.crash(to)
+ w.servingOn(t, to)
+ w.finish(t)
+ if len(w.violations) > 0 {
+ t.Fatalf("%s", w.violations[0])
+ }
+ })
+ }
+}
+
+func TestLatePutAfterTermination(t *testing.T) {
+ w := twoBoxWitness()
+ from, to := w.boxes[0], w.boxes[3]
+ w.serve(from, 1, app0)
+ w.running(t, from)
+ late := w.appWrite(from)
+ w.holdKey(w.claim.Holder.Location)
+ w.replicate(from) // the upload of the late write is held
+ w.hold = nil
+ w.terminate(from)
+ w.servingOn(t, to)
+ pinned := w.claim.Holder.Gen
+ if contains(to.DB.Log, late) {
+ t.Fatalf("the install restored a write whose upload had not landed at the pin")
+ }
+ if n := w.completeHeld(w.claim.Holder.Location); n == 0 {
+ t.Fatalf("no held upload to complete")
+ }
+ 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 PUT was never parked: %v (serving generation %q)", r, pinned)
+ }
+}
+
+// TestRelocationStartRacesPurge (claim §11): a worker read the serving
+// claim, then paused; a purge started meanwhile (admission closed, the
+// claim purging). The stalled worker resumes its start: C3's
+// revalidation stops it, and no relocation runs over a purging host.
+func TestRelocationStartRacesPurge(t *testing.T) {
+ w := twoBoxWitness()
+ from := w.boxes[0]
+ w.serve(from, 1, app0)
+ old := w.claim.clone() // the worker's read, before the purge
+ w.userPurge()
+ w.reach(t, 100, "the purge started", func() bool { return w.claim.Op.Kind == "purging" || w.admit[app0].Closed }, w.runConsole)
+ // the stalled worker resumes with its old read (rev 4's actor):
+ // resumeStale re-reads under its lease and, since the world moved,
+ // stops; its role never reaches the start CAS
+ w.resumeStale(from, old)
+ w.userRelocate() // a fresh start reads the purging claim and refuses
+ if w.claim.Op.Kind == "relocating" {
+ t.Fatalf("a relocation started over a purging host: %s", w.state())
+ }
+ w.finish(t)
+ if len(w.violations) > 0 {
+ t.Fatalf("%s", w.violations[0])
+ }
+}
+```
+
+```go
+func TestEmptyDatabaseDrain(t *testing.T) {
+ w := twoBoxWitness()
+ w.console = append(w.console, &consolePlan{Kind: "create", Host: "h", App: app0, OpID: w.newID("cr"), Inc: 1, Region: 0})
+ w.reach(t, 100, "created", func() bool { c := w.claim; return c != nil && c.Holder != nil && c.Op.Kind == "serving" }, w.runConsole, w.recoveryPass)
+ from := w.execBox(w.claim)
+ to := w.boxes[3]
+ if from.ID == to.ID {
+ to = w.boxes[0]
+ }
+ w.reach(t, 60, "a row minted", func() bool { return from.Row != nil }, w.actAll())
+ from.Files = &filesDir{Inc: 1, Key: 55, Env: 55, Done: true, Stamp: from.stampOf(1)}
+ id := w.timerOn(from)
+ w.drainTo(t, to)
+ w.servingOn(t, to)
+ w.finish(t)
+ if len(w.violations) > 0 {
+ t.Fatalf("%s", w.violations[0])
+ }
+ if !contains(to.Timers, id) && !w.delivered[id] {
+ t.Fatalf("the timer did not survive the empty-database drain")
+ }
+ if to.Files == nil || to.Files.Key != 55 {
+ t.Fatalf("the files did not survive the empty-database drain: %+v", to.Files)
+ }
+}
+
+func TestReleasedThenFailedProbe(t *testing.T) {
+ w := twoBoxWitness()
+ from, to := w.boxes[0], w.boxes[3]
+ third := w.extraBox(0, 30)
+ to.FailApp = true
+ w.serve(from, 1, app0)
+ w.running(t, from)
+ w.drainTo(t, to)
+ w.servingOn(t, third)
+ w.finish(t)
+ if len(w.violations) > 0 {
+ t.Fatalf("%s", w.violations[0])
+ }
+ if w.stats["admissions covered: released"] != 2 || w.stats["writes_lost declared"] != 0 {
+ t.Fatalf("released %d, writes_lost %d; want 2 and 0 (the failed probe's release covers its uncertified session)", w.stats["admissions covered: released"], w.stats["writes_lost declared"])
+ }
+}
+
+func TestStuckAfterTwoReplacements(t *testing.T) {
+ w := twoBoxWitness()
+ from, to := w.boxes[0], w.boxes[3]
+ b30, b31, b32 := w.extraBox(0, 30), w.extraBox(0, 31), w.extraBox(0, 32)
+ w.serve(from, 1, app0)
+ w.running(t, from)
+ w.drainTo(t, to)
+ for i, x := range []*box{to, b30, b31} {
+ if !w.reach(t, 1500, "a target installing", func() bool { c := w.claim; return c.Op.Kind == "relocating" && c.Op.Phase == "installing" && c.Op.Exec == x.ID }, w.actAll(), w.recoveryPass) {
+ t.Fatalf("target %d (%d) never installed: %s", i, x.ID, w.state())
+ }
+ w.terminate(x)
+ w.reach(t, 100, "fenced", func() bool { return contains(w.claim.Lost, x.ID) }, w.actAll(), w.recoveryPass)
+ }
+ if w.claim.Op.Stuck == "" {
+ t.Fatalf("a third replacement did not mark the operation stuck: %s", w.state())
+ }
+ w.servingOn(t, b32) // the operator resolves it
+ w.finish(t)
+ if len(w.violations) > 0 {
+ t.Fatalf("%s", w.violations[0])
+ }
+ if w.stats["operator resolved a stuck relocation"] != 1 {
+ t.Fatalf("the operator did not resolve it: %v", w.stats)
+ }
+}
+
+func TestReleaseWaitsForEscapedDescendant(t *testing.T) {
+ saved := mutated
+ mutated = "evidence-whole-tree"
+ defer func() { mutated = saved }()
+ w := twoBoxWitness()
+ from, to := w.boxes[0], w.boxes[3]
+ w.serve(from, 1, app0)
+ w.running(t, from)
+ from.Procs = append(from.Procs, &proc{Main: false, Strict: false, Inc: 1, Box: from.ID, Session: w.claim.Holder.Session}) // escaped the cgroup
+ w.drainTo(t, to)
+ w.drive(300, func() bool { return false }, w.act(from, to), w.recoveryPass)
+ if c := w.claim; c.Op.Kind != "relocating" || c.Op.Phase != "releasing" || c.Op.Exec != from.ID || c.Op.Release != nil {
+ t.Fatalf("the release moved on with a writer alive: %s", w.state())
+ }
+ if w.stats["release: a process survives the stop"] == 0 {
+ t.Fatalf("the escaped descendant never failed step 1")
+ }
+}
+```
+
+- [ ] **Step 5: Run the gate, then each witness alone with its trace**
+
+```bash
+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/task5.log | grep -E "seeds, |^--- FAIL|^ --- FAIL|^ok|^FAIL|witness .* under"
+for r in reloc-release-first reloc-exec-only-installs reloc-install-receipt reloc-no-reinstall reloc-released-coverage reloc-source-loss reloc-row-cases reloc-start-guard fence-discharge-qualified fence-declares-timers reloc-enrolled-only files-live-set; do
+ HOSTLIFE_WITNESS=$r nice -n 19 go test ./internal/sim/hostlife/ -run '^TestWitnesses$' -count=1 -v 2>&1 | grep -E "witness .* under|^--- FAIL|^ok" | head -5
+done
+diff $TMPDIR/twobox/baseline-counters.json <(grep COUNTERS $TMPDIR/twobox/task5.log | head -1 | sed 's/.*COUNTERS //') && echo ONE-BOX-COUNTERS-IDENTICAL
+```
+
+Expected: every new witness `held` under `""`, `held` under each proper subset (only `reloc-row-cases` has one: thirty subsets), `violated: ...<its want>` under its set; every direct test passes; `ONE-BOX-COUNTERS-IDENTICAL`. A witness that holds under its mutation is broken, not the rule: read its trace (`HOSTLIFE_WITNESS=<rule>` prints it) and fix the scenario, never the oracle. A witness that violates with the rules on has found something: it is a finding for Task 7's brief, and the scenario stays as evidence; only if the trace shows a model bug (an actor the real system does not have) is the model fixed.
+
+- [ ] **Step 6: Commit**
+
+```bash
+git add internal/sim/hostlife/
+git commit -m "sim: two-box scenarios: twelve witnesses for the relocation and fence guards, direct tests for create spread, termination in every relocation phase, nested failover, the stale edges file, the adverse volume, crashes mid-install, late PUTs after termination, the start racing a purge, an empty-database drain, released then a failed probe, stuck after two replacements, and an escaped descendant at the release
+
+Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>"
+```
+
+---
+
+### Task 6: The harness: `mutate.sh`'s shape, `expected-outcomes.txt`, and the revision's one sweep (moves §14.2; the evidence policy)
+
+**Files:**
+- Modify: `internal/sim/hostlife/mutate.sh`, `internal/sim/hostlife/expected-outcomes.txt`
+
+- [ ] **Step 1: The shape in `mutate.sh`**
+
+The script inherits `HOSTLIFE_BOXES` from its environment (the test binary reads it in `init`). Make the shape explicit in its header comment and its verdict tag so a log says which shape it is. In the header comment, after the three usage lines, add:
+
+```bash
+# HOSTLIFE_BOXES=2 internal/sim/hostlife/mutate.sh 3000 # the two-box shape (region HA L18); unset is one box per region
+```
+
+and after `BIN=${HOSTLIFE_BIN:-$SCRATCH/hostlife.test}` add `SHAPE=${HOSTLIFE_BOXES:-1}`; export it with the others (`export SEEDS PKG SCRATCH BIN WRULES SHAPE`), and in `one()` prefix every verdict's rule with the shape, so each `echo "... $r: ..."` becomes `echo "... $r [boxes=$SHAPE]: ..."` (seven sites: the five verdict kinds plus the two ERROR lines). The grep that parses the sweep's clean line, `0 failed.*mutated=\"$r\"`, still matches Task 1's `mutated="<r>" boxes=<n>`.
+
+- [ ] **Step 2: `expected-outcomes.txt`**
+
+Append:
+
+```
+create-choice-once missed no box-side effect precedes the serving CAS in this model, so a substituted executor leaves nothing behind; the rule's effect is the cancellation of a create whose box is gone (TestHostLifecycleTwoBox's "create cancelled: its box is gone" counter)
+reloc-exec-ack-barrier missed liveness only: without the barrier a target that never acknowledged is handed op.exec and the operation waits there instead of in starting; TestTerminationInEveryRelocationPhase shows the replacement either way
+reloc-pin-reaches-release missed the release's step 2 already waits for the listing to show N (relocRelease), so the pin's own check is never the first to see a short listing in this model; in the real pinner the listing is a separate read (plan 1b-next JournalPin)
+reloc-failover-pin-delay missed a loss bound, not a safety bound (§5.8): the pin names exact versions and a later PUT adds a version nothing reads; TestLatePutAfterTermination shows the late upload parked
+reloc-replacement-cap missed an operator bound: without the cap the operation replaces its target a third time instead of waiting for carlos ops host resolve; TestStuckAfterTwoReplacements shows stuck and the resolve
+reloc-replacement-table missed after P's first admission the admission rules (recovery-generation, remote-baseline) already refuse reopening P, so resuming at installed with the same P admits a fresh generation from P's remote, as the nested failover does without the pin delay (a loss bound); TestTerminationInEveryRelocationPhase and TestNestedFailover show every row
+reloc-row-cases missed one of the admission fences: a reopened stale row routes a request to a box exec-admission and its partners refuse; caught with exec-admission, hold-op-open, start-check-claim-gen and exec-writer (witness)
+fence-terminated-only missed redundant alone: a stopped box fenced by mistake is on lost, so lost-quarantine retires its state and exec-admission refuses it when it starts again; the rule keeps claim D2's attestation path for stopped boxes, which the model does not represent
+files-pin-exact missed a determinism rule (§5.8): a later manifest PUT adds a version nothing reads, and the fence declares what no landed manifest carries; TestLateFileUploads shows the pinned version applied
+```
+
+- [ ] **Step 3: The revision's sweep (the one allowed; serial, niced)**
+
+Run only when Tasks 1 to 5 are committed, nothing else is sweeping on the machine (`pgrep -f hostlife.test` empty), and the gate passes:
+
+```bash
+export GOFLAGS=-buildvcs=false GOCACHE=$TMPDIR/gocache
+mkdir -p $TMPDIR/hostlife-sim && nice -n 19 go test -c -o $TMPDIR/hostlife-sim/hostlife.test ./internal/sim/hostlife/
+HOSTLIFE_BOXES=2 HOSTLIFE_PAR=2 nice -n 19 internal/sim/hostlife/mutate.sh 3000 2>&1 | tee $TMPDIR/twobox/sweep-two-box-3000.log
+```
+
+Expected: exit 0; every rule `CAUGHT` or `EXPECTED-MISS`, none `MISSED`, `STALE` or `ERROR`. Each new safety guard is `CAUGHT` with `witness violated`; the two-box sweep may also catch one-box rules it did not before (a wider catch is fine). Record the verdict lines for Task 7. Do not rerun the whole sweep for one fix: a rule that needs rework reruns alone (`HOSTLIFE_BOXES=2 HOSTLIFE_PAR=1 nice -n 19 internal/sim/hostlife/mutate.sh 3000 <rule>`). The one-box sweep is not rerun this revision (ruling 2); its rev 7.22 verdicts stand because the one-box COUNTERS line is byte-identical. No 30,000-seed run.
+
+Afterwards: `rm -rf $TMPDIR/hostlife-sim`.
+
+- [ ] **Step 4: Commit**
+
+```bash
+git add internal/sim/hostlife/mutate.sh internal/sim/hostlife/expected-outcomes.txt
+git commit -m "sim: mutate.sh reports the shape (HOSTLIFE_BOXES) and expected-outcomes.txt lists the two-box rules caught only in combination, or bounded by liveness, loss or the operator, with the reason for each
+
+Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>"
+```
+
+---
+
+### Task 7: The joint-round brief
+
+**Files:**
+- Create: `docs/superpowers/plans/CODEX-REVIEW-BRIEF-TWO-BOX-R1.md`
+
+- [ ] **Step 1: Write the brief**
+
+The brief is for Astra (the independent second reader) and for the claim and moves sessions. It follows the shape of `CODEX-PLAN-REGION-HA-1BN-BRIEF-1.md` (on `origin/plan-region-ha-1b-next`): what to review, the authorities, what is fixed, what to check, the output wanted. Its content is this plan's evidence, so it is written last, from the logs in `$TMPDIR/twobox/`:
+
+```markdown
+# Review brief: the joint model with two boxes per region (L18), round 1
+
+You are an independent second reader. Review `internal/sim/hostlife` at
+the commit named in the prompt (branch `region-ha-hostlife-two-box`)
+against:
+
+- region HA spec 1 `docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md` on `origin/main` (rev 5.4, §24; H1 to H19; §2, §3, §5.2, §5.3, §5.4, §5.6, §5.8, §5.9, §5.10, §7, §9 L1 to L20);
+- plan 1b-next `git show origin/plan-region-ha-1b-next:docs/superpowers/plans/2026-10-07-region-ha-1b-next-relocation.md` (Task 1's transitions, its rulings, Task 11's gate);
+- claim rev 6.30 `git show origin/design-replica-ownership:docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md` (§4 L1, §6.4a item 2, §7.3 D2 to D6, §11);
+- moves rev 7.22 on this branch (§7.10, §14.2);
+- the plan that built it, `docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md` (its rulings 1 to 12).
+
+## Fixed: do not re-argue
+
+- H1 to H19, L1 to L20 as accepted, claim rev 6.30 §1.1's gate.
+- The one-box shape is the baseline: its 300-seed COUNTERS line is byte-identical to rev 7.22's (`<paste the line>`), so every one-box verdict of rev 7.22 stands.
+- The evidence policy: one 3,000-seed sweep per revision (two-box, this round); no deep runs without Paul.
+- The model's abstractions, as moves §14.2 lists them, plus this round's: a failover enters at `pinning` with the D6 barrier checked at the installing CAS (plan ruling 4); the stale edges file is the former executor's row (ruling 9); volume evidence is one flag per box (ruling 10); the files publisher runs in the two-box shape (ruling 11); `stuck` is a journal entry the operator resolves from `pinning` (ruling 6).
+
+## The guards, mapped
+
+| Model rule | Plan 1b-next guard | Spec | Evidence |
+|---|---|---|---|
+| create-choice-once | `BeginCreateOn`/`CompleteCreate` never substitutes (Task 2) | §5.2, P5-D2 | expected miss; `create cancelled: its box is gone` |
+| reloc-start-guard | `RelocationStartGuard` (Task 1) | §5.8, L11 | witness INV |
+| reloc-exec-ack-barrier | `requireAcks` (Task 1) | D6 | expected miss (liveness) |
+| reloc-release-first | `PinAfterRelease` cites the receipt (Task 1); release steps 1 to 4 (Tasks 4, 7) | §5.8 A3-2, L10 | witness INV-1 |
+| reloc-pin-reaches-release | `JournalPin` (Task 1) | §5.8 | expected miss (redundant with step 2 here) |
+| reloc-failover-pin-delay | `FailoverPinDelay` (Tasks 1, 5) | §5.8 | expected miss (loss bound) |
+| reloc-exec-only-installs | §5.8 Exclusion; `ToInstalling` names op.exec | HA2 | witness INV-6 |
+| reloc-install-receipt | `RecordLocalInstall`, `ToProbing` (Task 1) | §5.8 B1-2 | witness INV-4 |
+| reloc-no-reinstall | `preparedOpened` refusal (Task 1) | §5.8 B2-5 | witness INV-2 (timer) |
+| reloc-released-coverage | `AdmitWriter` released (Task 1) | §6.4a item 2, L9 | witness INV-2 |
+| reloc-row-cases | `RelocationRow` (Task 3) | §5.3, L12 | witness INV-1 with the admission fences |
+| reloc-replacement-cap | `MaxTargetReplacements`, `MarkStuck` (Task 1) | §5.8 | expected miss (operator bound); `TestStuckAfterTwoReplacements` |
+| reloc-enrolled-only | `ExecutorChooser` over the roster (Task 2); `eligibleBoxes` | §2, HA7 | witness INV-27 |
+| fence-terminated-only | `termfence.Verify`, `VerifyFence` | §5.9, H10 | expected miss (redundant with lost-quarantine and exec-admission) |
+| fence-discharge-qualified | `fenceBox` with `LocalDischarge` (Task 1) | §5.9, L3, H19 | witness INV-26; `TestAdverseVolume` |
+| fence-declares-timers | the D4 loss record, timer knowledge partial | §5.9, moves §7.10 | witness INV-2 (timer) |
+| reloc-source-loss | `FenceSource` (Task 1) | §5.8 B1-6 | witness INV-2 |
+| reloc-replacement-table | `ReplaceTarget` (Task 1) | §5.8 | expected miss (the admission rules refuse reopening P); `TestTerminationInEveryRelocationPhase` |
+| files-pin-exact | `RecoveryPin.FilesManifest`, `StorePinner` (Tasks 1, 5) | §5.8, B2-4 | expected miss (determinism); `TestLateFileUploads` |
+| files-live-set | the classifier's files live set | §5.6, L13 | witness INV-4 |
+
+## Results
+
+- Gate: `<the two summary lines, the witness count, the direct tests>`.
+- Two-box 3,000-seed sweep: `<every verdict line from $TMPDIR/twobox/sweep-two-box-3000.log>`.
+- Findings the model made while being built: `<each seed or witness that violated with the rules on, what it showed, and whether the model or a spec was changed; "none" if none>`.
+
+## What to check
+
+1. Each witness forces the interleaving its rule exists for, and nothing else fails under its mutation (the named failure is the first violation).
+2. The phase table as modelled against §5.8 and plan 1b-next Task 1: every CAS's conditions, what each phase admits, who may act.
+3. The release sequence's four steps, `released` coverage's binding to the flushed release, and the drain of a host whose session's replicator was gone (`Flushed` false: it declares).
+4. Source loss, the replacement table's rows, nested failover from `holder.generation`, the cap, and the operator's resolve.
+5. The fence: terminated only, bound to an enrolled reference, timers declared, chores discharged only with qualifying evidence, and that no recovery step waits on volume evidence.
+6. The files pin and the files live set against L13 and B2-4.
+7. The expected misses: is each reason right, or is there an invariant the model should check?
+8. The plan's twelve rulings: accept each, or say why it is wrong.
+9. Dormancy: anything in the two-box code that changes a one-box outcome (the COUNTERS line says no; check the reasoning, ruling 1).
+
+## Output
+
+Findings ranked P1 (a two-writer or data-loss path the model admits, a witness that does not prove its claim, a one-box change), P2 (a case from claim §11 or L18 not covered, a guard whose mutation is wrong), P3 (clarity). Each gives the file and line, the problem, the evidence (a seed, a witness trace, a spec line), and a concrete fix. End with a verdict: the round passes for the one-box and the two-box shape, or it does not, and what would make it pass.
+```
+
+Fill every `<...>` from the logs; none may remain.
+
+- [ ] **Step 2: Commit and clean up**
+
+```bash
+git add docs/superpowers/plans/CODEX-REVIEW-BRIEF-TWO-BOX-R1.md
+git commit -m "docs: the joint-round brief for the two-box model (L18), round 1
+
+Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>"
+rm -rf $TMPDIR/twobox $TMPDIR/hostlife-sim
+```
+
+Then hand the brief to the Codex second reader as memory `codex-second-reader.md` describes, and post the round's start on amadan #236 (the coordination post), naming the commit. Merging relocation (plan 1b-next Task 11) waits for the round to pass.
+
+---
+
+## After this plan
+
+| What | Waits for |
+|---|---|
+| HA4's stamp resolution (two edges files, the higher stamp wins) in the model | an edge actor in the model; plan 1a's unit tests cover it today (ruling 9) |
+| The volume recorder's two-hour bound and `removed_volumes` | plan 1b's unit tests (ruling 10) |
+| Claim D4's loss record materialized by the console from a fence | the console's claim-recovery pass (plan 1b-next "After this plan") |
+| A move into a two-box region choosing its target (L15 is modelled by `chooseBox`; its fenced-target path, L14) | moves Phase 1 Plans 2 and 4; the model keeps the operator's declare-lost for it |
+| The one-box mutation sweep at 3,000 seeds on this revision | the next revision's sweep, or Paul's say-so (ruling 2) |
+| 30,000-seed baselines of either shape | Paul's say-so |
+
+## Self-review
+
+- **Spec coverage.** L18's list: create spread (Task 5 `TestCreateSpread`; Task 1 `chooseBox`), relocation by drain (Task 2), termination mid-serve (Task 3 `startFailover`; Task 5 witnesses) and in every phase (Task 5 `TestTerminationInEveryRelocationPhase`; Task 3 `replaceTarget`, `fenceSource`), nested failover (Task 3 default row; Task 5 `TestNestedFailover`, `wFilesLiveSet`), a stale edges file (Task 2 row cases; Task 5 `wRelocRowCases`, `TestStaleEdgesFile`), an unenrolled reference (Tasks 2, 3; Task 5 `wRelocEnrolledOnly`), a volume without DeleteOnTermination (Task 3 `fenceBox`; Task 5 `wFenceDischargeQualified`, `TestAdverseVolume`), a crash mid-install (Task 5 `TestCrashMidInstall`; Task 2's replayable build and journaled install), late file uploads (Task 4), late PUTs after termination (Task 3 `terminate` leaves requests pending; Task 5 `TestLatePutAfterTermination`). Claim §11's extras for region HA: the start racing purge (Task 5), the empty-database drain (Task 5; Task 2's N = 0 path), generation parking while pinned (Task 4 live set; Task 5 `wFilesLiveSet`), released then an uncertified failed probe (Task 5), the one-box conversion (existing witness, kept passing by Task 2). §5.8's table (Task 2), its release sequence (Task 2, Task 4 step 3), the pinned set (Task 2 `restoreUpTo`, Task 4 manifest), P's build (Task 2), the local install and receipt (Task 2), the probe's admission and coverage (Task 2), the replacement table and source loss (Task 3), the cap and stuck (Tasks 2, 3), what a relocation leaves behind (Task 2 `relocationLeftovers`). §5.9 (Task 3). §5.2 (Task 1). §5.3 (Task 2). §5.6 (Task 4). §5.10 is root's and the participant's controller: not modelled, stated in the brief's fixed list by omission; add it to "After this plan" if the reader asks.
+- **Placeholders.** Every step carries its code. The brief's `<...>` fields are filled from logs in Task 7 Step 1 and may not remain.
+- **Type consistency.** `releaseEntry{Box, Session, Gen, FinalTX, ManifestSeq, Flushed, Files, Timers, At}` (Task 2) is read by `relocPinning`, `admitWriter`, `fenceSource` (Task 3) and `relocRelease` step 3 (Task 4). `pinEntry{TX, ManKey, ManVer, ManSeq, At}` (Task 2) is written by `relocPinning` (Tasks 2, 4) and read by `relocInstalling`, `pinnedManifest`, `filesLive`. `receiptEntry{Box, Stamp}`. `chooseBoxExcept(r, app, except...)` (Task 2) is used by `userRelocate`, `relocPinning`, `relocProbeFailed`, `replaceTarget`. `nameReplacement(n, next, phase) bool` (Task 2) is used by `relocProbeFailed` and `replaceTarget`. `preparedOpened(c)` (Task 2) by `relocProbing`, `replaceTarget`, `wFilesLiveSet`. `w.twoBox()`, `twoBoxWitness()`, `extraBox`, `running`, `drainTo`, `relocPhase`, `servingOn`, `timerOn` (Task 5) match their uses. Stats names used in assertions match their increments (`admissions covered: released`, `fences written`, `nested failover after P was admitted`, `relocation: target replaced at <phase>`, `operator resolved a stuck relocation`, `release: a process survives the stop`, `fence: park-local chores left open (volume evidence)`).
+- **Review Focus.** 1 (two workers, one chore): Task 3 `TestTwoWorkersOneChore`. 2 (escaped descendant at the release): Task 5 `TestReleaseWaitsForEscapedDescendant`. 3 (late level-0 PUT after the pin): Task 5 `TestLatePutAfterTermination`. 4 (unenrolled replacement): Task 3 `TestUnenrolledReferenceNeverChosen`, Task 5 `wRelocEnrolledOnly`. 5 (late or incomplete manifest): Task 4 `TestLateFileUploads`, Task 5 `wFenceDeclaresTimers`.