carlos / platform Public

docs: two-box model plan rev 9, Astra round 6: a release needs the session's own flush or its recorded positions, every release and flush path compared with 1b-next Task 7, the operator's stop of a target that cannot release, Task 5F and the round 6 dispositions

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

claude 2 weeks ago 9f49c1a18981cc8f6cbacca3c3e7fd859b8e2a1e parent 52e2179

1 file changed, +306 −10

docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md +306 −10

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

index 5f99ed7cb..36f86e4e8 100644

--- 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

@@ -1,15 +1,46 @@

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

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

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

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

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

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

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

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

+## Rev 9: round 6 dispositions

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

+|---|---|---|---|---|---|

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

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

+| 1b-next rev 19 | Model before rev 9 | Rev 9 |

+|---|---|---|

+| `releaseDrain` steps 1 to 3 in order: `StopWriters`, `Observe` (the tree empty), `FlushDB`, `FlushFiles`, then `Positions.Record`, then the producers' drain and root's receipt | `holdRow`, `evidence`, the database flush, the files manifest, the entry | same order; the record is written last, as `Record` is |

+| `relocationFlushDB`: the session's replicator (`att.rep`) or `ErrClaimStopUnavailable`; `SyncAndWait`; N from the listing; no LTX file means N = 0 | **fell back to the remote position, `Flushed=false`,** when the box had no database of the session (a failed target that never admitted) or its replicator was gone | **Fixed:** refused (R6 #1) |

+| `ReleaseFlushFiles`: this box's own files directory, wake state and env, committed as one revision even when unchanged | **fell back to the files set its installation applied** when the box held no files directory of the incarnation | **Fixed:** refused under the same rule. `ReleaseFlushFiles` publishes only what the box holds. |

+| `Release` after a restart: `Positions.Recorded` for this stop; a replayed receipt with no recorded flush is refused; a retry by the same controller resumes at the producers' drain without flushing again | no record; every retry flushed again or fell back | **Fixed:** `releaseRecord`, replayed unchanged for the same stop. The model has one controller identity per box and no receipt store, so both of 1b-next's recovery cases (another controller's durable receipt, and the same controller's resume) become this replay. |

+| `JournalRelease`: the release is of the executor's current session; for a session that admitted a writer, the writer box is the releaser | the CAS checks op.exec, the phase and that no release is journaled | same effect: a box without the session's own database no longer produces a release |

+| `FenceSource` in releasing before a release: no release is synthesised; the operation becomes a failover | the same (the synthesised release is `reloc-source-loss`'s mutation only) | unchanged |

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

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

+|---|---|---|---|

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

## Rev 8: round 5 dispositions

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

@@ -291,7 +322,7 @@ Each was a gap or a conflict between the authorities. Each says what it costs if

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, and 1b-next ruling 3 keeps production discharge off until the roster records an enrollment time. *Cost if wrong:* the adverse-volume case still proves what claim §11 asks: recovery proceeds and the chores stay open.

11. **The files publisher exists where region HA is enabled, which the model ties to the two-box shape.** Spec §5.6 is region HA's; the one-box model has no publisher and carries files at the cut (`StopFiles`), and a converted move keeps that stand-in. In the two-box shape the executor publishes a manifest whenever its files or wake state change, whether or not the app runs, and a dead box's disk is never read (`deadBoxFiles`). *Cost if wrong:* a one-box drain would also want it; the one-box shape has no drain.

12. **The review findings are on the branch now** (amended in rev 2). `CODEX-PLAN-REGION-HA-1BN-R1.md` to `R16.md` sit beside 1b-next rev 16. The hazards the model must catch were taken from them and from the dispositions tables of revs 2 to 16; the "What changed, by task" table above names the finding each rule answers, and Task 7's table carries a column for it. Findings about stage B integration with claim 6b and moves Plans 1 and 2 (R1 to R10, the lifecycle property of rev 14 to 16) have no model step and are listed as such.

-13. **The operator's resolve (`carlos ops host resolve`) has three cases.** The spec names the command and leaves its effect open. Nothing moves away from a live box without its stop evidence: a live source still `op.exec` in `starting` or `releasing` with no release journaled is returned to `serving` (the relocation is abandoned); a live target `op.exec` without a release is sent to `probe-failed`, where it runs its release; otherwise (op.exec none, released or lost, a dead executor first declared lost as claim D2's operator path does) the operation is replayed from `pinning` with the replacement count reset, the exclusions cleared, the source eligible again, and an empty listing accepted (`Resolved`); never a keyless files pin for a nonempty database (rev 3, ruling 17). *Cost if wrong:* one function in `console_test.go`; the guards are unchanged.

+13. **The operator's resolve (`carlos ops host resolve`) has three cases** (rev 9 adds a fourth: a live target in `probe-failed` that cannot release, because its replicator and files are gone and nothing recorded a flush, is stopped by the operator, and the next resolve declares it lost and replays). The spec names the command and leaves its effect open. Nothing moves away from a live box without its stop evidence: a live source still `op.exec` in `starting` or `releasing` with no release journaled is returned to `serving` (the relocation is abandoned); a live target `op.exec` without a release is sent to `probe-failed`, where it runs its release; otherwise (op.exec none, released or lost, a dead executor first declared lost as claim D2's operator path does) the operation is replayed from `pinning` with the replacement count reset, the exclusions cleared, the source eligible again, and an empty listing accepted (`Resolved`); never a keyless files pin for a nonempty database (rev 3, ruling 17). *Cost if wrong:* one function in `console_test.go`; the guards are unchanged.

14. **(Rev 3) `probe-failed` or a dead target with no spare is stuck after `releaseDeadline`, mirroring 1b-next ruling 26 and rev 18 finding 2** (finding F1, closed). In `probe-failed` with no eligible spare, the operation is stuck `releaseDeadline` after `probe_failed_since` (rule `reloc-no-spare-bound`). A dead target with no spare is fenced into `stuck` `releaseDeadline` after its termination, with the fence consumed (rule `reloc-dead-target-bound`, `fenceTargetStuck`). Neither ever names the source. Only the operator's resolve may, by plan ruling 13. Rev 2's version of this ruling was the model's own stand-in with no guard. *Cost if wrong:* in a two-box region a failed drain waits for the deadline and then for an operator, rather than returning to the source automatically, as 1b-next ruling 26 accepts.

15. **Termination is drawn only where region HA owns the loss.** The sweep terminates a box only when the claim names it, if at all, as a serving executor, a relocation's participant or a chore's owner, and never a box holding a legacy host before its adoption. A participant of a move, landing, rollback, revert, push, create or delete is recovered from a lost box by moves' and the claim's declare-lost paths (L14), which the model walks for a stopped box, and a push never starts on a terminated executor. *Cost if wrong:* those paths are untested under termination here; the brief lists it under "After this plan". **(Rev 4)** One exception, from claim §11's "automatic target loss racing the record commit CAS": a landing's or a rollback's target that is terminated is fenced by the regional worker as claim D2 makes automatic termination equivalent to a declared loss, by the operator's own record-first path (`declareTargetLost`), and a landing already committed by its record converts to a failover (ruling 20). The sweep still never draws such a termination; `TestAutomaticTargetLossRacesRecordCommit` and the witness `fence-converts-committed-landing` script it.

16. **(Rev 3) Every unopened P is recorded when it is replaced or dropped, and parked at completion, mirroring 1b-next ruling 27 and rev 18 finding 3** (finding F3, closed). `abandonPrepared` journals it in `opState.Abandoned` (`abandoned_prepared`) on every path: install, the replacement table's nested branch, the nested relocation after `probe-failed`, and the operator's replay. The serving CAS queues a scoped `park-generation` for each one in the source region (rule `reloc-abandoned-prepared`). An opened P is part of the writer lineage and is never listed. This replaces rev 2's list of every built P. *Cost if wrong:* the model's at-rest sweep is the backstop, as it is in 1b-next. That is why the rule's mutation is an expected miss, shown by a direct test.

@@ -9201,9 +9232,271 @@ Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>"

---

+### Task 5F: Astra's round 6: a release needs its own flush or its recorded positions (rev 9)

+This is described in "Rev 9: round 6 dispositions" above. It contains:

+- Rule `reloc-release-needs-flush`, in `relocRelease`.

+- `releaseRecord` and `box.relRecord`, the model's `ReleasePositions`.

+- The operator's stop of a live target that cannot release.

+- `TestReleaseRefusedAfterACrashBeforeTheFlush` and `TestReleaseReplaysTheRecordedFlush`.

+**Files:**

+- Modify: `regionha_test.go` (`relocRelease`), `world_test.go` (`releaseRecord`, `box.relRecord`), `console_test.go` (`operator`), `rules_test.go`, `regionha_round1_test.go`

+- [ ] **Step 1: Apply the patch**

+```diff

+diff --git a/internal/sim/hostlife/console_test.go b/internal/sim/hostlife/console_test.go

+index 8061165..ca3a2b6 100644

+--- a/internal/sim/hostlife/console_test.go

++++ b/internal/sim/hostlife/console_test.go

+@@ -1252,6 +1252,17 @@ func (w *world) operator() {

+ if dead != nil && !dead.Destroyed {

+ dead = nil

+ }

++ if ex := w.boxByID(op.Exec); ex != nil && !ex.Destroyed && op.Phase == "probe-failed" && !released && !contains(c.Lost, ex.ID) && on("reloc-release-needs-flush") {

++ // a live target that cannot release (its replicator and its

++ // files are gone and nothing recorded a flush, rev 9): no

++ // release will ever come, so the operator stops the box, and

++ // its declared loss (claim D2) lets the next resolve replay

++ // the operation from pinning

++ w.stop(ex)

++ w.stats["operator stopped a target that cannot release"]++

++ w.logf("operator stopped box %d: it cannot release relocation %s", ex.ID, op.ID)

++ return

++ }

+ var what string

+ if w.cas(c, func(n *claim) bool {

+ if !sameOp(n.Op.ID, op.ID) || n.Op.Kind != "relocating" || n.Op.Stuck == "" {

+diff --git a/internal/sim/hostlife/regionha_round1_test.go b/internal/sim/hostlife/regionha_round1_test.go

+index 28f7dd7..24937fa 100644

+--- a/internal/sim/hostlife/regionha_round1_test.go

++++ b/internal/sim/hostlife/regionha_round1_test.go

+@@ -767,6 +767,88 @@ func TestPendingTargetFenceHoldsThePhase(t *testing.T) {

+ }

++// TestReleaseRefusedAfterACrashBeforeTheFlush (reloc-release-needs-flush;

++// rev 9, Astra round 6): a drain's source is in releasing, its last write

++// not yet uploaded, when its agent crashes: the session's replicator is

++// gone and nothing recorded a flush for this stop. No release is

++// journaled and no pin selected; at the release deadline the operation

++// is stuck, and the operator's resolve returns the host to its source.

++// The mutation journals the remote position with Flushed false.

++func TestReleaseRefusedAfterACrashBeforeTheFlush(t *testing.T) {

++ w := twoBoxWitness()

++ from, to := w.boxes[0], w.boxes[3]

++ w.serve(from, 1, app0)

++ w.running(t, from)

++ w.published(t, from)

++ w.drainTo(t, to)

++ w.appWrite(from)

++ w.holdKey(w.claim.Holder.Location) // the flush's upload does not land

++ if !w.stepUntil(t, 1500, "the source waiting for its flush", func() bool {

++ return w.claim.Op.Phase == "releasing" && w.stats["release: waits for the flush"] > 0

++ }) {

++ w.mustHold(t)

++ }

++ w.crash(from)

++ w.hold = nil

++ for i := 0; i < releaseDeadline+20; i++ {

++ w.tick(w.act(from, to))

++ c := w.claim

++ if c.Op.Release != nil || c.Op.Pin != nil {

++ t.Fatalf("a release or a pin without the source's flush (step %d): %s", i, w.state())

++ }

++ if c.Op.Stuck != "" {

++ break

++ }

++ if c := w.claim; c.Op.Stuck == "" || c.Op.Phase != "releasing" {

++ t.Fatalf("not stuck in releasing at the release deadline: %s", w.state())

++ }

++ w.finish(t)

++ w.mustHold(t)

++ if c := w.claim; c.Op.Kind != "serving" || c.Op.Exec != from.ID {

++ t.Fatalf("the operator's resolve did not return the host to its source: %s", w.state())

++ }

++}

++// TestReleaseReplaysTheRecordedFlush (reloc-release-needs-flush; rev 9,

++// Astra round 6): the source's release sequence completes and records

++// its flushed positions (ReleasePositions), and its agent crashes before

++// the release is journaled. The restarted agent has no replicator for

++// the session, but the record is durable: the release is replayed with

++// the recorded positions, Flushed, and the drain completes. The mutation

++// records nothing and journals the remote position with Flushed false.

++func TestReleaseReplaysTheRecordedFlush(t *testing.T) {

++ w := twoBoxWitness()

++ from, to := w.boxes[0], w.boxes[3]

++ w.serve(from, 1, app0)

++ w.running(t, from)

++ w.published(t, from)

++ w.drainTo(t, to)

++ w.appWrite(from)

++ if !w.stepUntil(t, 1500, "releasing", w.atPhase("releasing")) {

++ w.mustHold(t)

++ }

++ var r *releaseEntry

++ for i := 0; i < 60 && r == nil; i++ {

++ r = w.relocRelease(from, w.claim.clone()) // steps 1 to 3 and the record, not yet journaled

++ w.tick()

++ }

++ if r == nil || !r.Flushed {

++ t.Fatalf("the release sequence did not complete: %v %s", r, w.state())

++ }

++ w.crash(from)

++ if !w.reach(t, 60, "the release journaled", func() bool { return w.claim.Op.Release != nil }, w.act(from, to)) {

++ w.mustHold(t)

++ }

++ got := w.claim.Op.Release

++ if !got.Flushed || got.FinalTX != r.FinalTX || got.ManifestSeq != r.ManifestSeq {

++ t.Fatalf("the journaled release %+v is not the recorded one %+v", got, r)

++ }

++ w.servingOn(t, to)

++ w.finish(t)

++ w.mustHold(t)

++}

+ // TestPinNeverShortOfTheRelease (reloc-pin-reaches-release): the listing

+ // lags behind the journaled release (its newest file is not yet visible);

+ // no pin is journaled short of the release's final_txid.

+diff --git a/internal/sim/hostlife/regionha_test.go b/internal/sim/hostlife/regionha_test.go

+index 376e151..17338b8 100644

+--- a/internal/sim/hostlife/regionha_test.go

++++ b/internal/sim/hostlife/regionha_test.go

+@@ -144,9 +144,27 @@ func (w *world) relocRelease(b *box, c *claim) *releaseEntry {

+ w.stats["release: a process survives the stop"]++

+ return nil

+ }

++ if r := b.relRecord; r != nil && on("reloc-release-needs-flush") && r.Op == c.Op.ID && r.Phase == c.Op.Phase && r.E.Session == h.Session && r.E.Gen == h.Gen {

++ // a flush this box recorded for this stop (ReleasePositions.Recorded):

++ // the release is replayed with the recorded positions, never

++ // flushed or guessed again (rev 9)

++ e := r.E

++ e.Files, e.Timers = r.E.Files.clone(), append([]int(nil), r.E.Timers...)

++ w.stats["release: replayed from the recorded positions"]++

++ return &e

++ }

+ prefix := dataKey(h.Location, h.Gen, "")

+ remote := w.remoteMax(w.buckets[b.Region], prefix)

+ n, flushed := remote, false

++ if on("reloc-release-needs-flush") && !(b.DB != nil && b.DB.Inc == h.Inc && b.DB.Gen == h.Gen && b.DB.Epoch == b.Epoch && b.DB.Session == h.Session) {

++ // relocationFlushDB needs the session's own replicator, and

++ // nothing recorded a flush for this stop: no release (1b-next Task

++ // 7; rev 9, Astra round 6). The release deadline makes the

++ // operation stuck; the mutation journals the remote position with

++ // Flushed false, as rev 8 did

++ w.stats["release: no replicator and no recorded flush, refused"]++

++ return nil

++ }

+ 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 {

+@@ -171,6 +189,12 @@ func (w *world) relocRelease(b *box, c *claim) *releaseEntry {

+ // files identity

+ files := b.Files.clone()

+ if files == nil || files.Inc != h.Inc {

++ if on("reloc-release-needs-flush") {

++ // ReleaseFlushFiles publishes this box's own files directory;

++ // there is none to publish (rev 9)

++ w.stats["release: no files directory to flush, refused"]++

++ return nil

++ }

+ files = w.relocFiles(c).clone()

+ }

+ // 3. (Task 4) publish every pending file and wake-state mutation,

+@@ -199,8 +223,14 @@ func (w *world) relocRelease(b *box, c *claim) *releaseEntry {

+ seq, b.releaseSeq = b.releaseSeq, 0

+ b.published = filesState(b.Timers, files)

+ }

+- return &releaseEntry{Box: b.ID, Session: h.Session, Gen: h.Gen, FinalTX: n, ManifestSeq: seq, Flushed: flushed,

++ e := &releaseEntry{Box: b.ID, Session: h.Session, Gen: h.Gen, FinalTX: n, ManifestSeq: seq, Flushed: flushed,

+ Files: files, Timers: append([]int(nil), b.Timers...), At: w.now}

++ if on("reloc-release-needs-flush") {

++ // ReleasePositions.Record: durable before the producers close

++ b.relRecord = &releaseRecord{Op: c.Op.ID, Phase: c.Op.Phase, E: *e}

++ b.relRecord.E.Files, b.relRecord.E.Timers = files.clone(), append([]int(nil), b.Timers...)

++ }

++ return e

+ }

+ // pinSource is the generation the pin reads (StorePinner's genselect.Select

+diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go

+index ed23391..12fd159 100644

+--- a/internal/sim/hostlife/rules_test.go

++++ b/internal/sim/hostlife/rules_test.go

+@@ -197,6 +197,7 @@ var allRules = []string{

+ "files-live-set-moves-parks", // finding F4 (rev 4), claim §6.2a: moves' parks (a push's whole-location park, a landing's install park, a rollback's return park) keep the files live set; the mutation archives it with the rest and the next failover can never pin the live files (INV-3)

+ "reloc-clear-after-cleanup", // 1b-next ruling 20 and rev 6 R4-5 (Finish clears the record only after a successful scoped cleanup): a failed cleanup keeps the controller record, which blocks executable updates (claim §11's witness); the mutation clears it and an update runs over the unfinished cleanup (INV-29)

+ "fence-converts-committed-landing", // finding F5 (rev 4; claim §11 "automatic target loss racing the record commit CAS"): a landing whose record committed and whose target is then terminated becomes a failover in the target's region; the mutation leaves it to the operator, and it never completes (INV-3)

++ "reloc-release-needs-flush", // rev 9 (Astra round 6; 1b-next rev 19 Task 7 Release, relocationFlushDB, ReleaseFlushFiles, ReleasePositions): a release needs the session's own replicator and the box's own files directory, or the positions it recorded for this stop; otherwise none, and the deadline makes the operation stuck; the mutation journals the remote position with Flushed false (TestReleaseRefusedAfterACrashBeforeTheFlush, TestReleaseReplaysTheRecordedFlush)

+ "reloc-fence-pending-blocks", // rev 8 (Astra round 5; 1b-next rev 19 Worker.Step returns w.replace(...) before its phase switch): while a relocation participant's fence is pending (a dead target, no spare, before its deadline) no regional phase transition runs; the participant's own release still does; the mutation goes on into the phase switch (TestPendingTargetFenceHoldsThePhase)

+ "reloc-name-before-pin", // rev 7 (Astra round 4 finding 1; 1b-next rev 19 Worker.pinning): a relocation at pinning with no target names one before it selects a pin, on every path; the mutation pins first, and a manifest that lands while no box is eligible is left out (a loss bound: TestConvertedMoveWaitsForATargetBeforeItsPin)

+ "reloc-failover-start-guard", // rev 7 (Astra round 4 finding 3; 1b-next rev 19 Worker.Start, StartRelocation): a serving executor's failover starts only with an eligible target, the app admitting the registration (and its recheck) and RelocationStartGuard with the source fenced; the mutation starts at once (TestFailoverStartWaitsForAdmission, TestFailoverStartWaitsForParkReplica)

+diff --git a/internal/sim/hostlife/world_test.go b/internal/sim/hostlife/world_test.go

+index 5cb9f47..af8e364 100644

+--- a/internal/sim/hostlife/world_test.go

++++ b/internal/sim/hostlife/world_test.go

+@@ -373,9 +373,10 @@ type box struct {

+ execRecord string

+ cleanupPending bool

+ cleanupFails bool

+- fencePending bool // (rev 8) this worker step found a relocation participant's fence it could not consume

+- FenceObservedAt int // the box-fences record's observed_at: when a worker first saw it terminated; 0 no record (rev 4)

+- 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)

++ relRecord *releaseRecord // (rev 9) ReleasePositions: the flushed positions of one release, recorded on disk against its stop; an agent restart keeps it

++ fencePending bool // (rev 8) this worker step found a relocation participant's fence it could not consume

++ FenceObservedAt int // the box-fences record's observed_at: when a worker first saw it terminated; 0 no record (rev 4)

++ 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

+@@ -928,6 +929,15 @@ type opState struct {

+ // 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.

++// releaseRecord is 1b-next Task 7's ReleasePositions record: the

++// release a box computed once its writers stopped and its database and

++// files flushed, bound to the stop (the operation, the phase and the

++// writer session), durable before the producers close (rev 9).

++type releaseRecord struct {

++ Op, Phase string

++ E releaseEntry

++}

+ type releaseEntry struct {

+ Box, Session int

+ Gen string

+```

+- [ ] **Step 2: Run the gate, the identity traces, and the new tests under their mutation**

+```bash

+gofmt -l internal/sim/hostlife/; nice -n 19 go vet ./internal/sim/hostlife/

+diff $TMPDIR/twobox/baseline-counters.json <(grep COUNTERS $TMPDIR/twobox/task5f.log | head -1 | sed 's/.*COUNTERS //') && echo ONE-BOX-COUNTERS-IDENTICAL

+HOSTLIFE_TRACE_OUT=$TMPDIR/twobox/trace.txt HOSTLIFE_TRACE_OUT_SEEDS=$TMPDIR/twobox/seeds.txt nice -n 19 go test ./internal/sim/hostlife/ -run '^TestOneBox' -count=1 >/dev/null

+cmp $TMPDIR/twobox/baseline-trace.txt $TMPDIR/twobox/trace.txt && cmp $TMPDIR/twobox/baseline-seeds.txt $TMPDIR/twobox/seeds.txt && echo ONE-BOX-TRACES-IDENTICAL

+HOSTLIFE_MUTATE=reloc-release-needs-flush nice -n 19 go test ./internal/sim/hostlife/ -run '^TestRelease(RefusedAfterACrashBeforeTheFlush|ReplaysTheRecordedFlush)$' -count=1 -v 2>&1 | grep -cE '^--- FAIL'

+```

+Expected (the dry run's): `300 seeds, 0 failed, 483 completed operations; mutated="" boxes=1`, `300 seeds, 0 failed, 486 completed operations; mutated="" boxes=2`, `ok`, `ONE-BOX-COUNTERS-IDENTICAL`, `ONE-BOX-TRACES-IDENTICAL`, `2`.

+- [ ] **Step 3: Commit**

+```bash

+git add internal/sim/hostlife/

+git commit -m "sim: Astra's round 6 on the two-box model: a release needs the session's own replicator and files, or the positions recorded for its stop, and is otherwise refused until the deadline; the operator stops a target that can never release

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

+```

+---

### Task 6: The harness: `mutate.sh`'s shape and the region HA group, `expected-outcomes.txt`, and the revision's one sweep (moves §14.2; the evidence policy)

-`mutate.sh` already runs one mutation check per rule in `allRules`, so each of the 51 region HA rules is checked by the sweep once it exists. This task makes the shape explicit in every verdict (`[boxes=N]`), adds `@regionha` (the rules of the region HA block, one mutation check per guard, for a rerun of the new guards alone), adds `HOSTLIFE_LIST=1` (print the rules a run would check and run nothing), and lists the 25 region HA rules that are not caught alone, each with its reason and the direct test that shows it.

+`mutate.sh` already runs one mutation check per rule in `allRules`, so each of the 52 region HA rules is checked by the sweep once it exists. This task makes the shape explicit in every verdict (`[boxes=N]`), adds `@regionha` (the rules of the region HA block, one mutation check per guard, for a rerun of the new guards alone), adds `HOSTLIFE_LIST=1` (print the rules a run would check and run nothing), and lists the 26 region HA rules that are not caught alone, each with its reason and the direct test that shows it.

**Files:**

- Modify: `internal/sim/hostlife/mutate.sh`, `internal/sim/hostlife/expected-outcomes.txt`

@@ -9212,10 +9505,10 @@ Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>"

```diff

diff --git a/internal/sim/hostlife/expected-outcomes.txt b/internal/sim/hostlife/expected-outcomes.txt

-index 72504e3..4a75aab 100644

+index 72504e3..07cbf56 100644

--- a/internal/sim/hostlife/expected-outcomes.txt

+++ b/internal/sim/hostlife/expected-outcomes.txt

-@@ -21,3 +21,28 @@ admit-bind-op missed caught with claim-cas-opid: the model's general CAS conditi

+@@ -21,3 +21,29 @@ admit-bind-op missed caught with claim-cas-opid: the model's general CAS conditi

hostguard rare 30000 the guard's race is reached by the sweep at 30,000 (2 / 30,000 on rev 7.11; 5 / 3,000 on rev 7.10, before the admitting CAS moved ahead of the start)

stale-hold-release rare 30000 reached at 30,000 (15 / 30,000 on rev 7.11; 2 / 3,000 on rev 7.10)

strict-spawn rare 30000 its witness holds alone (the combination with evidence-whole-tree is the witness's); the sweep reaches it at 30,000 (1 / 30,000 on rev 7.11; 3 / 3,000 on rev 7.10)

@@ -9244,6 +9537,7 @@ index 72504e3..4a75aab 100644

+reloc-name-before-pin missed a loss bound like reloc-failover-pin-delay: a converted move's or a replay's pin selected before a target is named misses only files that land while no box is eligible; TestConvertedMoveWaitsForATargetBeforeItsPin holds every box ineligible while the newer manifest lands and fails under the mutation

+reloc-failover-start-guard missed a fidelity guard: the mutation starts the failover earlier (no target yet, admission closed, a park-replica outstanding), and no model invariant distinguishes the earlier start, whose target is then named at pinning; TestFailoverStartWaitsForAdmission and TestFailoverStartWaitsForParkReplica fail under the mutation

+reloc-fence-pending-blocks missed a fidelity guard: under the mutation the phase moves on while a dead target's fence waits for a spare, and the fence is consumed later by the replacement table at whatever phase the operation reached, which no model invariant distinguishes; TestPendingTargetFenceHoldsThePhase fails under the mutation

++reloc-release-needs-flush missed a fidelity guard: the mutation's unflushed release is legal in the model (the next admission declares what the remote does not hold, as writes_lost), so no invariant fails, but 1b-next refuses it and waits for the deadline; TestReleaseRefusedAfterACrashBeforeTheFlush and TestReleaseReplaysTheRecordedFlush fail under the mutation

diff --git a/internal/sim/hostlife/mutate.sh b/internal/sim/hostlife/mutate.sh

index c583d97..883996e 100755

--- a/internal/sim/hostlife/mutate.sh

@@ -9358,11 +9652,11 @@ HOSTLIFE_LIST=1 internal/sim/hostlife/mutate.sh 0 | wc -l

nice -n 19 go test ./internal/sim/hostlife/ -count=1 2>&1 | tail -1

```

-Expected (the dry run's): `SYNTAX-OK`, `51`, `159`, `ok`.

+Expected (the dry run's): `SYNTAX-OK`, `52`, `160`, `ok`.

- [ ] **Step 3: The revision's sweep (the one allowed; serial, niced)**

-Run only when Tasks 1 to 5E are committed, nothing else is sweeping on the machine (`pgrep -f hostlife.test` empty), and the gate passes:

+Run only when Tasks 1 to 5F are committed, nothing else is sweeping on the machine (`pgrep -f hostlife.test` empty), and the gate passes:

```bash

export GOFLAGS=-buildvcs=false

@@ -9406,7 +9700,7 @@ prompt (branch `region-ha-hostlife-two-box`) against plan 1b-next rev

- 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);

- claim rev 6.30 `git show origin/design-replica-ownership:docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md` (§4 L1, §6.2a L13, §6.4a item 2, §7.3 D2 to D6, §11);

- moves rev 7.22 on this branch (§7.6, §7.10, §14.2);

-- the plan that built it, `docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md` rev 8 (its rulings 1 to 25, ruling 4 as revs 5 to 7 amended it; rulings 14, 16 and 17 mirror 1b-next's fixes for F1 to F3; "Rev 4: round 1 dispositions" answers Astra's round 1 on the plan, `CODEX-PLAN-REGION-HA-TWO-BOX-R1.md`, and maps each past finding to its proving artifact; "Rev 5: round 2 dispositions" answers round 2, `CODEX-PLAN-REGION-HA-TWO-BOX-R2.md`; "Rev 6: round 3 dispositions" answers round 3, `CODEX-PLAN-REGION-HA-TWO-BOX-R3.md`; "Rev 7: round 4 dispositions" answers round 4, `CODEX-PLAN-REGION-HA-TWO-BOX-R4.md`, and compares every entry point with 1b-next; "Rev 8: round 5 dispositions" answers round 5, `CODEX-PLAN-REGION-HA-TWO-BOX-R5.md`, and compares the worker's checks with `Worker.Step`).

+- the plan that built it, `docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md` rev 9 (its rulings 1 to 25, ruling 4 as revs 5 to 7 amended it; rulings 14, 16 and 17 mirror 1b-next's fixes for F1 to F3; "Rev 4: round 1 dispositions" answers Astra's round 1 on the plan, `CODEX-PLAN-REGION-HA-TWO-BOX-R1.md`, and maps each past finding to its proving artifact; "Rev 5: round 2 dispositions" answers round 2, `CODEX-PLAN-REGION-HA-TWO-BOX-R2.md`; "Rev 6: round 3 dispositions" answers round 3, `CODEX-PLAN-REGION-HA-TWO-BOX-R3.md`; "Rev 7: round 4 dispositions" answers round 4, `CODEX-PLAN-REGION-HA-TWO-BOX-R4.md`, and compares every entry point with 1b-next; "Rev 8: round 5 dispositions" answers round 5, `CODEX-PLAN-REGION-HA-TWO-BOX-R5.md`, and compares the worker's checks with `Worker.Step`; "Rev 9: round 6 dispositions" answers round 6, `CODEX-PLAN-REGION-HA-TWO-BOX-R6.md`, and compares every release and flush path with Task 7).

## Fixed: do not re-argue

@@ -9470,6 +9764,7 @@ prompt (branch `region-ha-hostlife-two-box`) against plan 1b-next rev

| reloc-failover-start-guard | `Worker.Start` (`Eligible`, `Admission.Register`, `Recheck`), `StartRelocation`'s `RelocationStartGuard` with the source fenced | two-box R4 #3 | §5.8, L11 | expected miss; `TestFailoverStartWaitsForAdmission`, `TestFailoverStartWaitsForParkReplica` |

## Findings F1 to F3, closed, and the open window L21

@@ -9504,6 +9799,7 @@ The model's rev 4 found two gaps that neither 1b-next rev 19 nor moves rev 7.22

16. (Rev 6) Astra round 3's fix: only an initial failover (`opState.PinFailover`) waits for the acknowledgements before its pin; a converted move, a nested failover and a replay pin first (`TestConvertedMovePinsBeforeAcknowledgement`). Is the flag a faithful stand-in for 1b-next's `starting`?

17. (Rev 7) Astra round 4's fixes and the entry-point table in "Rev 7: round 4 dispositions": the target named before any pin on every path, `relocPhaseName`, and the failover started through Worker.Start's guards in their order. Is any entry point still ordered differently from 1b-next?

18. (Rev 8) Astra round 5's fix and the `Worker.Step` order table in "Rev 8: round 5 dispositions": a pending fence holds every regional transition, while the participant's own release and the box's other work stay schedulable. Is anything the model still runs while a fence is pending a `Worker.Step` transition?

+19. (Rev 9) Astra round 6's fix and the release-path table in "Rev 9: round 6 dispositions": no release without the session's own flush or a recorded one, the replay of a recorded flush, and the operator's stop of a target that can never release (plan ruling 13). Is the single `releaseRecord` a faithful stand-in for both of 1b-next's recovery cases?

14. (Rev 4) Claim §11's cases: the move with an unchanged file, the automatic target loss racing the record commit, the failed cleanup that blocks executable updates (INV-29), the forced open boundaries (four, the published marker before replication opens included). Are the file-object model (plan ruling 25) and the controller record faithful enough to stand for them, and is the coverage table in the plan's rev 4 section right about which findings only 1b-next's own tests can prove?

## Output

@@ -9543,7 +9839,7 @@ Then hand the brief to the Codex second reader as memory `codex-second-reader.md

## Self-review

-- **1b-next rev 19 coverage.** Every guard its dispositions list for stage A that a model step can reach has a rule (the guards table above, 51 rules; rev 3 added four for rev 17 to 19, rev 4 ten for Astra's round 1, rev 5 one for round 2, rev 7 two for round 4, rev 8 one for round 5); the findings the model cannot reach are mapped to 1b-next's own tests in "Rev 4: round 1 dispositions"; the stage B contracts (R1 to R10, the lifecycle property of revs 14 to 16, hostexec's controller recovery) have no model step and are named as such. Each rule's comment names its 1b-next function.

+- **1b-next rev 19 coverage.** Every guard its dispositions list for stage A that a model step can reach has a rule (the guards table above, 52 rules; rev 3 added four for rev 17 to 19, rev 4 ten for Astra's round 1, rev 5 one for round 2, rev 7 two for round 4, rev 8 one for round 5, rev 9 one for round 6); the findings the model cannot reach are mapped to 1b-next's own tests in "Rev 4: round 1 dispositions"; the stage B contracts (R1 to R10, the lifecycle property of revs 14 to 16, hostexec's controller recovery) have no model step and are named as such. Each rule's comment names its 1b-next function.

- **L18 and claim §11.** Every L18 case is a `TestL18*` with one-box and two-box subtests; claim §11's extras are direct tests or witnesses, each listed in "Rev 4: round 1 dispositions". §5.8's table (Task 2), the release (Tasks 2, 4), the pin (Tasks 2, 4), P's build (Tasks 2, 4), the local install, EnsureLocal and VerifyReceipt (Task 2), the probe (Task 2), the replacement table, source loss and the exhausted fence (Task 3), the cap and stuck (Tasks 2, 3), what a relocation leaves behind (Tasks 2, 4). §5.9 (Task 3). §5.2 (Tasks 1, 5). §5.3 (Task 2). §5.6 (Task 4). §5.10 is root's and the participant's controller: not modelled.

- **Placeholders.** Every task carries its dry-run patch. The brief's `<...>` fields are filled from logs in Task 7 Step 1 and may not remain.

- **Type consistency.** The patches compiled and passed in order; `go vet` was clean after each.