carlos / platform Public

docs: two-box model plan rev 10, Astra round 7: only a terminated box's volume evidence discharges local cleanup (INV-26 on the operation's discharges), the operator stops only an unrecoverable release, Task 5G and the round 7 dispositions

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

claude 2 weeks ago c160de8c1b18d68b3a92c8ac58d168b1bba98d93 parent 03eef47

1 file changed, +311 −12

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

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 36f86e4e8..a016048d3 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,36 @@

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

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

> **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:** 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.

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

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

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

+| R7 #1 (P2) | Correct. 5F's operator stop leaves the box's disk and `Terminated=false`. The next resolve's declared loss calls `fenceBox`, whose discharge read only `DeleteOnTermination`, so the stopped box went into `Op.Discharged` and completion queued no `park-local` for it. Claim §7.3 D5 and H19 keep a stopped box's local retirement owed. In 1b-next rev 19 `fenceBox` runs only under a verified termination fence, so the gap was the model's own. | accepted | Automatic discharge needs `Terminated` and qualifying volume evidence (rule `fence-discharge-qualified`, its predicate tightened). A stopped box is never fenced automatically (`fence-terminated-only`, unchanged). Its declared loss on the operator's path puts it on lost and discharges nothing, so its `park-local` stays owed. INV-26 now also fires when a box enters `Op.Discharged` without being terminated with qualifying evidence, even though no chore exists yet. The operator's destroyed-local declaration (claim §7.2) stays a separate, explicit attestation. | Task 5G; plan ruling 10 | `TestStoppedTargetKeepsItsLocalCleanup`: the failed target loses its database and files, so the operator stops it (with `DeleteOnTermination=true`), the next resolve replays, and the recovery completes with no operator cleanup. The box's `park-local` must still be owed. Under `fence-discharge-qualified`'s mutation INV-26 fires. |

+| R7 #2 (P2) | Correct. 5F's condition was a live target, stuck in `probe-failed` with no journaled release. It never checked the replicator, the files or a recorded flush, so a release that was merely slow was stopped. 1b-next rev 19 has no operator resolve; the spec leaves `carlos ops host resolve` open and plan ruling 13 is the model's own. So 1b-next has nothing over-broad to report. The stop was this plan's addition. | accepted | `releaseUnrecoverable`: the operator stops the box only when no flush is recorded for this stop and the session's replicator or the box's files are gone. Either loss makes `relocRelease` refuse for good. In every other case the resolve clears `stuck` and sends the target back to `probe-failed`, where its release resumes. The new rule `operator-stop-unrecoverable-only` is the model's operator rule; its mutation is rev 9's broad stop. It is an expected miss: the declared loss that follows is legal in the model. | Task 5G; plan ruling 13 | `TestOperatorResumesASlowRelease`: the failed target's final manifest PUT is held past the deadline. The resolve must resume rather than stop, and once the PUT lands the release journals and the host serves. `TestOperatorResumesARecordedFlush`: the release is recorded and then the agent restarts before the journal. The resolve must resume, and the record is replayed. Both fail under the mutation. The missing-state case is `TestStoppedTargetKeepsItsLocalCleanup` and the `reloc-verify-receipt` witness. |

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

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

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

+| Task 5G | identical | 300, 0 failed, 486. The operator stopped 3 targets, each unrecoverable, and resolved 7 stuck operations. | ok. The three new tests pass. Both resume tests fail under `operator-stop-unrecoverable-only`, and the stopped-target test fails under `fence-discharge-qualified` (INV-26). |

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

## Rev 9: round 6 dispositions

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

@@ -319,10 +340,10 @@ Each was a gap or a conflict between the authorities. Each says what it costs if

7. **Terminated is not stopped.** The model's `Destroyed` box may come back with its disk in the final heal (a stopped instance started again). Termination is new, permanent and observable: a `Terminated` box never returns, and only a terminated, enrolled box is fenced (H1, H10, H19). A stopped box stays the operator's declare-lost (claim D2), as today. *Cost if wrong:* none to the one-box path, which never terminates.

8. **Liveness, loss, determinism and defence-in-depth guards are `missed` with their reasons** in `expected-outcomes.txt`, each with a direct test that shows its effect. A mutation check needs an invariant violation, and spec §5.8 says itself that the pin delay "is a loss bound, not a safety bound". *Cost if wrong:* a later revision finds an invariant for one and the entry becomes STALE, which the harness reports.

9. **The stale edges file is the former executor's row.** The model has no edge or home map. Spec §5.4 publishes a host as `home` only from a `ready` row on its executor, and the model's edge "routes on the row" (`wake`). So a stale edges file is a row the former executor still holds after `op.exec` moved, and the hazard is a wake reaching it. HA4's stamp resolution is plan 1a's unit-tested code, not modelled. *Cost if wrong:* the brief names it as the one HA4 gap.

-10. **Volume evidence is one flag per box.** 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.

+10. **Volume evidence is one flag per box, and it counts only for a terminated box** (rev 10: a stopped box keeps its disk, so its `park-local` stays owed whatever the flag says; claim §7.3 D5). H19 and §5.9: the fence never reads it; only automatic discharge of the dead box's `park-local` chores does. The model draws `DeleteOnTermination` per box and the discharge rule reads it in the fence CAS; the recorder, the two-hour bound and `removed_volumes` are plan 1b's unit tests, and 1b-next ruling 3 keeps production discharge off until the roster records an enrollment time. *Cost if wrong:* the adverse-volume case still proves what claim §11 asks: recovery proceeds and the chores stay open.

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

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

-13. **The operator's resolve (`carlos ops host resolve`) has three cases** (rev 9 adds a fourth: 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.

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

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

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

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

@@ -9494,9 +9515,284 @@ Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>"

---

+### Task 5G: Astra's round 7: a stopped box keeps its local cleanup, and the operator stops only an unrecoverable release (rev 10)

+This is described in "Rev 10: round 7 dispositions" above. It contains:

+- `fenceBox`'s discharge, which now needs `Terminated`, and INV-26 on `Op.Discharged`.

+- `releaseUnrecoverable` in the operator's resolve, with the rule `operator-stop-unrecoverable-only`.

+- The helpers `probeFailedTarget` and `resolveOnly`.

+- The tests `TestOperatorResumesASlowRelease`, `TestOperatorResumesARecordedFlush` and `TestStoppedTargetKeepsItsLocalCleanup`.

+**Files:**

+- Modify: `regionha_test.go` (`fenceBox`), `console_test.go` (`operator`, `releaseUnrecoverable`), `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 ca3a2b6..9c219e2 100644

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

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

+@@ -1252,7 +1252,7 @@ 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") {

++ 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") && w.releaseUnrecoverable(ex, c) {

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

+@@ -1344,6 +1344,28 @@ func (w *world) operator() {

+ w.declareTargetLost(c)

+ }

++// releaseUnrecoverable is the operator's check before it stops a live

++// target that has not released (rev 10, Astra round 7): only when no

++// release can ever come. That needs no flush recorded for this stop, and

++// either the session's replicator or the box's files directory gone for

++// good (relocRelease refuses without either). Any other release, a slow

++// acknowledgement or a recorded flush not yet journaled, is resumed: the

++// resolve clears stuck and sends the target back to probe-failed. The

++// mutation of operator-stop-unrecoverable-only stops every such target,

++// as rev 9 did.

++func (w *world) releaseUnrecoverable(b *box, c *claim) bool {

++ if !on("operator-stop-unrecoverable-only") {

++ return true

++ }

++ h := c.Holder

++ if r := b.relRecord; r != nil && r.Op == c.Op.ID && r.Phase == c.Op.Phase && r.E.Session == h.Session && r.E.Gen == h.Gen {

++ return false // a recorded flush: the release replays it

++ }

++ replicator := b.DB != nil && b.DB.Inc == h.Inc && b.DB.Gen == h.Gen && b.DB.Epoch == b.Epoch && b.DB.Session == h.Session

++ files := b.Files != nil && b.Files.Inc == h.Inc

++ return !replicator || !files

++}

+ // declareTargetLost is the declared loss of a landing's or a rollback's

+ // target that is gone (claim D2, moves §7.10): the operator's path, and,

+ // for a terminated target, the regional worker's automatic fence (claim

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

+index 24937fa..4e8d93b 100644

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

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

+@@ -849,6 +849,133 @@ func TestReleaseReplaysTheRecordedFlush(t *testing.T) {

+ w.mustHold(t)

+ }

++// probeFailedTarget drains the host from box 0 to box 3, whose app

++// fails its probe, with a spare box 30 for the nested relocation, and

++// stops once the operation is in probe-failed with box 3 op.exec and no

++// release journaled.

++func (w *world) probeFailedTarget(t *testing.T) (from, to *box) {

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

++ to.FailApp = true

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

++ w.running(t, from)

++ w.published(t, from)

++ w.drainTo(t, to)

++ w.extraBox(0, 30)

++ if !w.stepUntil(t, 1500, "probe-failed on the target", func() bool {

++ c := w.claim

++ return c.Op.Phase == "probe-failed" && c.Op.Exec == to.ID && c.Op.Release == nil

++ }) {

++ w.mustHold(t)

++ }

++ return from, to

++}

++// resolveOnly is the operator's resolve of a stuck relocation and

++// nothing else (the destroyed-local declaration is left out).

++func (w *world) resolveOnly() {

++ if c := w.claim; c != nil && c.Op.Kind == "relocating" && c.Op.Stuck != "" {

++ w.operator()

++ }

++}

++// TestOperatorResumesASlowRelease (operator-stop-unrecoverable-only; rev

++// 10, Astra round 7 finding 2): the failed target's final manifest PUT is

++// not acknowledged before the release deadline, so the operation is

++// stuck. Its replicator and files are intact: the operator's resolve

++// resumes the release rather than stopping the box; once the PUT lands

++// the release is journaled and the nested relocation serves. The

++// mutation stops the box.

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

++ w := twoBoxWitness()

++ _, to := w.probeFailedTarget(t)

++ h := w.claim.Holder

++ held := dataKey(h.Location, h.Gen, "files/")

++ w.holdKey(held)

++ if !w.reach(t, 2*releaseDeadline, "stuck at the release deadline", func() bool { return w.claim.Op.Stuck != "" }, w.actAll(), w.recoveryPass) {

++ w.mustHold(t)

++ }

++ if c := w.claim; c.Op.Phase != "probe-failed" || c.Op.Release != nil {

++ t.Fatalf("not stuck in probe-failed without a release: %s", w.state())

++ }

++ w.resolveOnly()

++ if c := w.claim; to.Destroyed || c.Op.Stuck != "" || c.Op.Phase != "probe-failed" || c.Op.Exec != to.ID {

++ t.Fatalf("the resolve did not resume the target's release (stopped %v): %s", to.Destroyed, w.state())

++ }

++ w.hold = nil

++ w.completeHeld(held)

++ w.servingOn(t, nil)

++ if w.stats["operator stopped a target that cannot release"] != 0 || w.stats["release journaled: failed target"] == 0 {

++ t.Fatalf("the target was stopped, or never released: %v", w.stats)

++ }

++ w.finish(t)

++ w.mustHold(t)

++}

++// TestOperatorResumesARecordedFlush (operator-stop-unrecoverable-only;

++// rev 10, Astra round 7 finding 2): the failed target completes its

++// release sequence and records it, then its agent restarts (the

++// session's replicator is gone) before the release is journaled, and the

++// deadline passes. The recorded flush is a release waiting to be

++// journaled: the resolve resumes it, the target replays the record, and

++// the nested relocation serves. The mutation stops the box.

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

++ w := twoBoxWitness()

++ from, to := w.probeFailedTarget(t)

++ var r *releaseEntry

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

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

++ w.tick()

++ }

++ if r == nil {

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

++ }

++ w.crash(to)

++ spare := w.boxByID(30)

++ if !w.reach(t, 2*releaseDeadline, "stuck at the release deadline", func() bool { return w.claim.Op.Stuck != "" }, w.act(from, spare), w.recoveryPass) {

++ w.mustHold(t)

++ }

++ w.resolveOnly()

++ if c := w.claim; to.Destroyed || c.Op.Stuck != "" || c.Op.Phase != "probe-failed" {

++ t.Fatalf("the resolve did not resume the recorded release (stopped %v): %s", to.Destroyed, w.state())

++ }

++ w.servingOn(t, nil)

++ if w.stats["operator stopped a target that cannot release"] != 0 || w.stats["release: replayed from the recorded positions"] == 0 {

++ t.Fatalf("the target was stopped, or its record not replayed: %v", w.stats)

++ }

++ w.finish(t)

++ w.mustHold(t)

++}

++// TestStoppedTargetKeepsItsLocalCleanup (fence-discharge-qualified,

++// operator-stop-unrecoverable-only; rev 10, Astra round 7 findings 1 and

++// 2): the failed target loses its database and files with its agent, so

++// its release is unrecoverable; the operator stops the box and the next

++// resolve declares it lost and replays. The box's volume would be deleted

++// on termination, but it was stopped, not terminated: its disk is kept,

++// so when the recovery completes its park-local is still owed (claim §7.3

++// D5, H19). The mutation of fence-discharge-qualified discharges it.

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

++ w := twoBoxWitness()

++ _, to := w.probeFailedTarget(t)

++ to.DeleteOnTermination = true

++ w.crash(to)

++ to.Files, to.DB, to.receipt = nil, nil, nil

++ if !w.reach(t, 3000, "serving after the operator's stop and replay", func() bool {

++ c := w.claim

++ return c.Op.Kind == "serving" && c.Op.Exec >= 0 && c.Op.Exec != to.ID

++ }, w.actAll(), w.recoveryPass, w.wakeExec, w.resolveOnly) {

++ w.mustHold(t)

++ }

++ if !to.Destroyed || to.Terminated || w.stats["operator stopped a target that cannot release"] == 0 {

++ t.Fatalf("the target was not stopped by the operator: %s", w.state())

++ }

++ if !w.owesLocal(w.claim, to) {

++ t.Fatalf("the stopped target's local cleanup was discharged: %s", w.state())

++ }

++ w.finish(t) // the operator's destroyed-local declaration, an explicit attestation, retires it

++ 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 17338b8..1407d22 100644

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

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

+@@ -1665,7 +1665,13 @@ func (w *world) fenceBox(n *claim, x *box) {

+ }

+- qualified := x.DeleteOnTermination

++ // a fence exists only for a terminated box (TerminationWorker verifies

++ // terminated), and only a terminated box's volume evidence says

++ // anything: a stopped box keeps its disk, so its park-local chores

++ // stay owed whatever DeleteOnTermination says (claim §7.3 D5, H19;

++ // rev 10, Astra round 7). The operator's declared loss of a stopped

++ // box reaches this function too, and discharges nothing

++ qualified := x.Terminated && x.DeleteOnTermination

+ if !on("fence-discharge-qualified") {

+ qualified = true

+ }

+@@ -1676,8 +1682,8 @@ func (w *world) fenceBox(n *claim, x *box) {

+ var keep []obligation

+ for _, o := range n.Obl {

+ if o.Kind == "park-local" && o.Box == x.ID {

+- if !x.DeleteOnTermination {

+- w.violate("INV-26: box %d's park-local chore %s discharged without qualifying volume evidence (§5.9, H19)", x.ID, o.ID)

++ if !x.Terminated || !x.DeleteOnTermination {

++ w.violate("INV-26: box %d's park-local chore %s discharged without qualifying volume evidence (§5.9, H19; terminated %v)", x.ID, o.ID, x.Terminated)

+ }

+ w.stats["fence: park-local chores discharged"]++

+ continue

+@@ -1685,6 +1691,11 @@ func (w *world) fenceBox(n *claim, x *box) {

+ keep = append(keep, o)

+ }

+ n.Obl = keep

++ if !x.Terminated || !x.DeleteOnTermination {

++ // INV-26 (rev 10): a discharge recorded for the operation's

++ // leftovers is a discharge too, though no chore exists yet

++ w.violate("INV-26: box %d's local retirement discharged without qualifying volume evidence (§5.9, H19, claim §7.3 D5; terminated %v)", x.ID, x.Terminated)

++ }

+ n.Op.Discharged = addUniq(n.Op.Discharged, x.ID)

+ }

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

+index 12fd159..a35e999 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)

++ "operator-stop-unrecoverable-only", // rev 10 (Astra round 7; plan ruling 13, no 1b-next code): the operator stops a live target that has not released only when its release is unrecoverable (no recorded flush, and the session's replicator or its files gone); otherwise the resolve resumes the release; the mutation stops every such target (TestOperatorResumesASlowRelease, TestOperatorResumesARecordedFlush)

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

+```

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

+```bash

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

+diff $TMPDIR/twobox/baseline-counters.json <(grep COUNTERS $TMPDIR/twobox/task5g.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=operator-stop-unrecoverable-only nice -n 19 go test ./internal/sim/hostlife/ -run '^TestOperatorResumes(ASlowRelease|ARecordedFlush)$' -count=1 -v 2>&1 | grep -cE '^--- FAIL'

+HOSTLIFE_MUTATE=fence-discharge-qualified nice -n 19 go test ./internal/sim/hostlife/ -run '^TestStoppedTargetKeepsItsLocalCleanup$' -count=1 2>&1 | grep -E '^(ok|--- 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`, `--- FAIL: TestStoppedTargetKeepsItsLocalCleanup`.

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

+```bash

+git add internal/sim/hostlife/

+git commit -m "sim: Astra's round 7 on the two-box model: only a terminated box's volume evidence discharges its local cleanup, so a stopped box keeps it, and INV-26 checks the operation's discharges; the operator stops a target only when its release is unrecoverable and otherwise resumes it

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

+`mutate.sh` already runs one mutation check per rule in `allRules`, so each of the 53 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 27 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`

@@ -9505,10 +9801,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..07cbf56 100644

+index 72504e3..b70bf86 100644

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

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

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

+@@ -21,3 +21,30 @@ 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)

@@ -9538,6 +9834,7 @@ index 72504e3..07cbf56 100644

+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

++operator-stop-unrecoverable-only missed a fidelity guard on the operator's resolve: the mutation stops a target that could still release, and the declared loss and replay that follow are legal in the model, so no invariant fails; TestOperatorResumesASlowRelease and TestOperatorResumesARecordedFlush 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

@@ -9652,11 +9949,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`, `52`, `160`, `ok`.

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

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

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

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

```bash

export GOFLAGS=-buildvcs=false

@@ -9700,7 +9997,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 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).

+- the plan that built it, `docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md` rev 10 (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; "Rev 10: round 7 dispositions" answers round 7, `CODEX-PLAN-REGION-HA-TWO-BOX-R7.md`).

## Fixed: do not re-argue

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

-| fence-discharge-qualified | `fenceBox` with `LocalDischarge` | R2-7 | §5.9, L3, H19 | witness INV-26 |

@@ -9765,6 +10062,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` |

| reloc-release-needs-flush | Task 7 `Release`, `releaseDrain`, `relocationFlushDB`, `ReleaseFlushFiles`, `ReleasePositions` | two-box R6 #1 | §5.8 | expected miss; `TestReleaseRefusedAfterACrashBeforeTheFlush`, `TestReleaseReplaysTheRecordedFlush` |

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

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

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?

+20. (Rev 10) Astra round 7's fixes: discharge only for a terminated box with qualifying evidence (INV-26 on the operation's discharges), and the operator's stop narrowed to an unrecoverable release. Is `releaseUnrecoverable` the right line between resume and stop?

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

@@ -9839,7 +10138,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, 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.

+- **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, 53 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, rev 10 one for round 7); 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.