carlos / platform Public

docs: two-box model plan rev 5, Astra round 2: PinFailover's barrier before the failover's pin (ruling 4 amended), the published-marker crash boundary, the adverse volume under a failover, Task 5C and the round 2 dispositions

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

claude 2 weeks ago ab169b712574b63e5673ab6b4cc4373a0f97c99d parent dcf68aa

1 file changed, +460 −14

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

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 87d3ae063..d4340d84a 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,43 @@

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

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

> **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:** Eight tasks (rev 4 adds Task 5B) 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 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:** Nine tasks (rev 4 adds Task 5B, rev 5 Task 5C) 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) answers round 2: PinFailover's barrier before the pin, the boundary between the published marker and the open replication, and the adverse volume under a failover. 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 5: round 2 dispositions

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

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

+| R1 #8 (partly resolved) | Correct. In the model, generation.json's landing, `PublishGeneration` and the replication's open run in one call of the start (`resumeOpen`'s `marker` case falls through to `open`), so no test could stop between them. | accepted | A witness hook, `world.openYield`, returns from the start after the marker is published and before replication opens. The start resumes at `open` on its next call. It is nil outside the witnesses, so the sweeps don't change. `TestCrashAtEachOpenBoundary` gains a fourth stage, `published`. It stops there and checks that generation.json already names P, then crashes the target, in a one-box and a two-box region. | Task 5C | (coverage) `published` fails if the yield is not reached |

+| R2 #1 (P2) | Correct. A failover entered `pinning` with no target and journaled its pin before it named a target or checked acknowledgements. 1b-next rev 19's `PinFailover` needs every participant's acknowledgement before `pinning`. So a manifest that landed while the target's controller was down was missing from the pin. Ruling 4's phase collapse moved that guard. | accepted | A pin with no release (a failover, a converted move, a replay) now names its target first and selects the pin only once `requireAcks` holds. The phase stays `pinning` (ruling 4, amended), and the guard sits exactly where 1b-next's barrier stands. It is the new rule `reloc-failover-ack-before-pin`. Its mutation selects the pin first, as rev 4 did. It is an expected miss (a loss bound like `reloc-failover-pin-delay`). | Task 5C; ruling 4 | `TestFailoverPinWaitsForTheAcknowledgement`. The executor's newer manifest is in flight at its termination. The target is named, but its controller does not run, so for the delay plus 20 steps only a third box works. The test asserts no acknowledgement and no pin, then lands the manifest. Once the target acknowledges, the pin must name the newer manifest. |

+| R2 #2 (P2) | Correct. The two-box case drained before it terminated the former executor, so no executor failed. | accepted | Both shapes now terminate the current executor with `DeleteOnTermination=false`. With no operator acting, the host must reach serving on the region's other box (two-box) or on the group's replacement (one-box). The dead box's `park-local` must be open at that point and still open 200 steps later. The operator's destroyed-local declaration (`finish`) then closes it, and the test checks that it closed. | Task 5C | (coverage) the test fails if the fence discharges without evidence (`fence-discharge-qualified` is the witness) |

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

+1. A superseded generation's `park-generation` ran while the relocation still pinned that generation's manifest.

+2. The files live set kept the manifest, which was correct.

+3. Nothing parked it after the relocation completed, so INV-10 reported it as residue.

+`relocationLeftovers` now queues a `park-generation` for the pinned manifest's generation when that generation is no longer the holder's. This stands in for the pinner's retained copy, which 1b-next ruling 21 makes `CompleteRelocation`'s to drop. With the fix, every seed passes. The joint round should check that 1b-next's `CompleteRelocation` retires the retained copy. It is not raised as a 1b-next finding, because the model cannot see that code.

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

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

+| Tasks 1 to 5B | identical (as in rev 4) | 447, 449, 464, 478, 480, 480, 487 | ok |

+| Task 5C | identical | 300, 0 failed, 486 | ok. Under its mutation, `TestFailoverPinWaitsForTheAcknowledgement` fails ("pinned before a target was named and acknowledged"). `TestCrashAtEachOpenBoundary` (4 stages × 2 shapes) and `TestL18AdverseVolume` (2 shapes) pass. |

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

## Rev 4: round 1 dispositions

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

@@ -168,12 +196,12 @@ The two-box sweep at Task 6 starts 15 drains and 4 failovers and completes 17 re

## Rulings made while planning

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

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

1. **The one-box shape is a different random stream only where the two-box shape draws more.** Every seed of the one-box sweep must stay byte-identical to the baseline (spec §4: "a region with one box behaves exactly as today"). So a two-box world draws its extra values only after the one-box draws of the same step (`newWorld` adds its second boxes last; `step` draws for termination, drains and the publisher only when `perRegion > 1`), and no one-box code path calls the random source where it did not before. The gate proves it: every task compares the one-box `COUNTERS` line to the baseline's and, from rev 4, the whole trace of a one-box create's interruption and a hash of every one-box seed's trace (Task 1 Step 1). Rev 3's Task 1 passed the COUNTERS check while it cancelled an interrupted one-box create; region HA's create behaviour (the recovered-create cancellation, the eligibility of a sole box) is the two-box shape's alone. *Cost if wrong:* a seed reshuffle, which the gate shows at once; the fix is to move the draw.

2. **The two-box sweep is the revision's one 3,000-seed sweep.** The evidence policy (moves §14.2, Paul 2026-10-06) allows one mutation sweep per revision. The one-box path is byte-identical at the gate's 300 seeds, so the one-box verdicts of rev 7.22 stand for it; the new guards are reachable only with two boxes, so the sweep runs with `HOSTLIFE_BOXES=2`. One caveat the brief states: Task 2 replaces the body of `relocate`, which the one-box shape reaches only through a converted move (`fence-converts-moving`); the 300-seed one-box sweep never converts, so its `COUNTERS` line cannot show a change there, and the `fence-converts-moving` witness is the evidence that the converted path still completes. *Cost if wrong:* a one-box regression in a guard this plan touches would show first in the gate's 300-seed one-box run, which every task runs.

3. **A regional worker is any live, enrolled, non-lost box of the region.** Claim P6-D5 and spec §2 say correctness never depends on which worker acts; two make the same CAS and one fails. The model lets every such box run the region's chores and the relocation's worker steps. The one-box path is unchanged, since the region's one box was the only candidate. *Cost if wrong:* a chore run by two boxes at once that the park's idempotent copies and single manifest did not make safe; the sweep would show it as INV-10 or non-convergence, which is a finding for the claim, not a model bug.

-4. **Failover starts at `pinning` with the target named there; the D6 barrier is checked at the installing CAS.** Spec §5.8 and 1b-next's `StartRelocation` name the target in the failover's start CAS and pass through `starting` for its acknowledgement (`PinFailover`). The model's converted move already enters at `pinning` with no target (moves §7.10), so one entry point serves both, and `to`'s execution lease must be current before `installing` (`requireAcks` in `ToInstalling`). A drain whose source is lost in `starting` goes to `pinning` at once for the same reason (1b-next keeps it in `starting` until `PinFailover`). *Cost if wrong:* a phase the brief says is collapsed; no guard moves.

+4. **Failover starts at `pinning` with the target named there. The D6 barrier is checked before the pin is selected (rev 5), and again at the installing CAS.** Spec §5.8 and 1b-next's `StartRelocation` name the target in the failover's start CAS and pass through `starting` for its acknowledgement (`PinFailover`). The model's converted move already enters at `pinning` with no target (moves §7.10), so one entry point serves both, and `to`'s execution lease must be current before `installing` (`requireAcks` in `ToInstalling`). A drain whose source is lost in `starting` goes to `pinning` at once for the same reason (1b-next keeps it in `starting` until `PinFailover`). **(Rev 5, Astra round 2 finding 1.)** Rev 4's collapse did move a guard: the pin was selected before any acknowledgement, where `PinFailover` waits for them all. Now, in `pinning`, a pin with no release names its target first and is selected only once `requireAcks` holds (rule `reloc-failover-ack-before-pin`). That is the same barrier at the same point in the order of events. Only the phase's name differs. *Cost if wrong:* a phase the brief says is collapsed. The guard is now 1b-next's.

5. **`released` coverage is modelled as the claim defines it, and relocation by drain is enabled in the model.** Spec §5.8 says a drain is not enabled until L9 is accepted; claim rev 6.30 §6.4a carries L9. The model implements it so the review can judge it, and the brief says so. *Cost if wrong:* the drain scenarios are evidence for L9, not against anything.

6. **`stuck` is a journal entry; the operator resolves it** (plan ruling 13 says how). 1b-next ruling 9: `stuck` is not a phase. *Cost if wrong:* the operator's act is one function.

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

@@ -7696,9 +7724,424 @@ Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>"

---

+### Task 5C: Astra's round 2: PinFailover's barrier before the pin, the published-marker boundary, and the adverse volume under a failover (rev 5)

+This is described in "Rev 5: round 2 dispositions" above. It contains:

+- The new rule `reloc-failover-ack-before-pin`, in `relocPinning`, with `relocNameTarget` factored out.

+- The witness hook `openYield` and the `published` stage of `TestCrashAtEachOpenBoundary`.

+- `TestFailoverPinWaitsForTheAcknowledgement`.

+- `TestL18AdverseVolume`, rewritten for both shapes.

+- In `relocationLeftovers`, a park of the pinned manifest's generation.

+**Files:**

+- Modify: `regionha_test.go` (`relocPinning`, `relocNameTarget`, `relocationLeftovers`, comments on `relocStarting`, `startFailover` and `fenceSource`), `protocol_test.go` (the yield in the start's `marker` case), `world_test.go` (`openYield`), `rules_test.go`, `regionha_round1_test.go`, `regionha_cases_test.go`

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

+```diff

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

+index 219c9e2..3f442bc 100644

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

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

+@@ -925,6 +925,9 @@ func (w *world) resumeOpen(b *box, c *claim, o *openState) bool {

+ }

+ o.stage = "open"

++ if w.openYield != nil && w.openYield(b) {

++ return false // the marker is published; replication is not open yet

++ }

+ case "open":

+ if !hasMain(b) && b.DB != nil {

+ // the app was stopped idle while the start was still

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

+index 36efb1e..39e9b52 100644

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

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

+@@ -223,31 +223,42 @@ func TestL18UnenrolledReference(t *testing.T) {

+ })

+ }

++// TestL18AdverseVolume (claim §11's adverse-volume case; H19; rev 5, Astra

++// round 2 finding 2): the current executor is terminated with a

++// volume that was not DeleteOnTermination. Execution recovery proceeds

++// to serving on the region's other box (two-box) or on the group's

++// replacement (one-box) with no operator, and the dead box's park-local

++// stays open throughout; only the operator's cleanup (the declared

++// destroyed-local loss) removes it.

+ func TestL18AdverseVolume(t *testing.T) {

+ bothShapes(t, func(t *testing.T, w *world, boxes int) {

+ from := w.serveAndPublish(t)

+ from.DeleteOnTermination = false

+- if boxes == 2 {

+- // a former executor that still owes its park-local

+- w.drainTo(t, w.peer())

+- w.servingOn(t, w.peer())

+- if !w.owesLocal(w.claim, from) {

+- t.Fatalf("the former executor owes no park-local: %s", w.state())

+- }

++ w.terminate(from) // the current executor

++ if !w.reach(t, 3000, "serving after the failover, with no operator", func() bool {

++ c := w.claim

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

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

++ return

+ }

+- w.terminate(from)

+- if boxes == 2 {

+- w.reach(t, 60, "the former executor fenced", func() bool { return contains(w.claim.Lost, from.ID) }, w.act(w.peer()))

+- if !w.owesLocal(w.claim, from) {

+- t.Fatalf("the fence discharged the park-local without qualifying evidence: %s", w.state())

+- }

+- } else {

+- w.failedOver(t, from) // execution recovery proceeds (H19)

++ to := w.execBox(w.claim)

++ if boxes == 2 && to != w.peer() {

++ t.Fatalf("served on %v, want the region's other box %d", to, w.peer().ID)

++ }

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

++ t.Fatalf("the dead box's park-local is not open after the failover: %s", w.state())

+ }

+ if w.stats["fence: park-local chores left open (volume evidence)"] == 0 || w.stats["fence: park-local chores discharged"] != 0 {

+ t.Fatalf("the fence's discharge ignored the volume evidence: %v", w.stats)

+ }

++ w.drive(200, never, w.actAll(), w.recoveryPass, w.wakeExec)

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

++ t.Fatalf("the dead box's park-local closed without the operator: %s", w.state())

++ }

+ w.finish(t) // the operator's destroyed-local declaration clears it

++ if w.owesLocal(w.claim, from) {

++ t.Fatalf("the park-local is still open after the operator's cleanup: %s", w.state())

++ }

+ })

+ }

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

+index ad0f45d..2758cd7 100644

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

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

+@@ -408,6 +408,67 @@ func TestFailoverPinWaitsOutTheDelay(t *testing.T) {

+ w.mustHold(t)

+ }

++// TestFailoverPinWaitsForTheAcknowledgement (reloc-failover-ack-before-pin;

++// rev 5, Astra round 2 finding 1; 1b-next rev 19 PinFailover): the

++// executor's newer files manifest is still in flight when it is

++// terminated. The target is named, but its controller does not run, so

++// it has not acknowledged; the pin waits past the delay, the manifest

++// lands, and only then does the target acknowledge. The pin names the

++// newer manifest. The mutation pins before the acknowledgement, and the

++// pin misses it.

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

++ w := twoBoxWitness()

++ from := w.boxes[0]

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

++ w.running(t, from)

++ w.published(t, from)

++ spare := w.extraBox(0, 30) // a second live box of the region: the worker while the target's controller is down

++ c := w.claim

++ loc, gen := c.Holder.Location, c.Holder.Gen

++ from.Files.Env++ // a newer files state: the admin token rotated

++ newer := manifestKey(loc, gen, from.pubSeq+1)

++ w.holdKey(newer)

++ w.publishFiles(from)

++ w.hold = nil

++ if from.pubSeq == 0 || manifestKey(loc, gen, from.pubSeq) != newer {

++ t.Fatalf("the newer manifest was not issued: %s", w.state())

++ }

++ w.terminate(from)

++ if !w.stepUntil(t, 400, "the failover's target named", func() bool {

++ c := w.claim

++ return c.Op.Kind == "relocating" && (c.Op.Tgt >= 0 || c.Op.Pin != nil)

++ }) {

++ w.mustHold(t)

++ }

++ if w.claim.Op.Pin != nil {

++ t.Fatalf("pinned before a target was named and acknowledged: %s", w.state())

++ }

++ tgt := w.boxByID(w.claim.Op.Tgt)

++ worker := spare

++ if tgt == spare {

++ worker = w.boxes[3]

++ }

++ w.drive(failoverPinDelay+20, never, w.act(worker)) // the target's controller does not run

++ if contains(w.claim.Op.Acks, tgt.ID) {

++ t.Fatalf("the target acknowledged without running")

++ }

++ if p := w.claim.Op.Pin; p != nil {

++ t.Fatalf("pinned %s before the target acknowledged: %s", p.ManKey, w.state())

++ }

++ if n := w.completeHeld(newer); n != 1 {

++ t.Fatalf("held manifest PUTs completed: %d, want 1", n)

++ }

++ if !w.reach(t, 400, "the pin", func() bool { return w.claim.Op.Pin != nil }, w.act(worker, tgt)) {

++ w.mustHold(t)

++ }

++ if p := w.claim.Op.Pin; p.ManKey != newer {

++ t.Fatalf("the pin names %s, want the manifest that landed while the target had not acknowledged, %s", p.ManKey, newer)

++ }

++ w.servingOn(t, tgt)

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

+@@ -451,10 +512,12 @@ func TestPinNeverShortOfTheRelease(t *testing.T) {

+ // admission, marker publication and replication opening"): the target's

+ // agent crashes exactly at each boundary of P's first admitted session:

+ // admitted with the app starting (its launch environment held unready),

+-// admitted with generation.json's PUT in flight (held), and replication

+-// open; in a one-box and a two-box region.

++// admitted with generation.json's PUT in flight (held), generation.json

++// published and replication not yet open (rev 5, Astra round 2: the

++// witness yield openYield stops the start between the two), and

++// replication open; in a one-box and a two-box region.

+ func TestCrashAtEachOpenBoundary(t *testing.T) {

+- for _, stage := range []string{"app", "marker", "open"} {

++ for _, stage := range []string{"app", "marker", "published", "open"} {

+ t.Run(stage, func(t *testing.T) {

+ bothShapes(t, func(t *testing.T, w *world, boxes int) {

+ from := w.serveAndPublish(t)

+@@ -468,6 +531,16 @@ func TestCrashAtEachOpenBoundary(t *testing.T) {

+ if stage == "marker" {

+ w.holdKey(genMarkerKey(loc))

+ }

++ yielded := false

++ if stage == "published" {

++ w.openYield = func(b *box) bool {

++ if yielded || b.open == nil || !b.open.Prepared {

++ return false

++ }

++ yielded = true

++ return true

++ }

+ var to *box

+ hit := w.stepUntil(t, 2000, "P's open at "+stage, func() bool {

+ c := w.claim

+@@ -481,6 +554,15 @@ func TestCrashAtEachOpenBoundary(t *testing.T) {

+ if stage == "open" {

+ return preparedOpened(c) && to.open == nil && hasMain(to)

+ }

++ if stage == "published" {

++ if !yielded || to.open == nil || to.open.stage != "open" {

++ return false

++ }

++ if g, _ := w.bucketGen(to, loc); g != to.open.Gen {

++ t.Fatalf("yielded before generation.json named %q", to.open.Gen)

++ }

++ return true

++ }

+ return to.open != nil && to.open.Prepared && to.open.stage == stage

+ })

+ if !hit {

+@@ -488,7 +570,7 @@ func TestCrashAtEachOpenBoundary(t *testing.T) {

+ }

+ w.crash(to)

+ to.envUnreadyFor = 0

+- w.hold = nil

++ w.hold, w.openYield = nil, nil

+ w.servingOn(t, nil)

+ w.finish(t)

+ })

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

+index 11c1ee7..c754c40 100644

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

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

+@@ -530,6 +530,28 @@ func (w *world) relocationLeftovers(n *claim, op opState) {

+ w.stats["relocation: abandoned prepared generation parked"]++

+ }

++ // the pinned manifest of a superseded generation (rev 5): the files

++ // live set kept it while the operation ran, so a park-generation of

++ // that generation that ran meanwhile left it; once the operation

++ // completes it is a dead generation's key, retired here (the stand-in

++ // for the pinner's retained copy, 1b-next ruling 21, which

++ // CompleteRelocation drops)

++ if h := n.Holder; h != nil && op.Pin != nil && op.Pin.ManKey != "" && op.Pin.ManGen != h.Gen {

++ ret := op.Pin.ManGen

++ if ret == "" {

++ ret = "@root"

++ }

++ queued := false

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

++ if o.Kind == "park-generation" && o.Region == op.SrcRegion && o.Ret == ret && o.Prefix == h.Location {

++ queued = true

++ }

++ if !queued {

++ n.Obl = append(n.Obl, w.scoped(obligation{ID: w.newID("ob"), Op: op.ID, Kind: "park-generation", Region: op.SrcRegion, Box: -1, Prefix: h.Location, Ret: ret, Quiet: w.now + horizonH}, w.now, h.Inc))

++ w.stats["relocation: the pinned manifest's generation parked"]++

++ }

+ owed := append([]int{op.Src}, op.InstalledOn...)

+ for _, id := range owed {

+ if id < 0 || id == op.Exec || contains(op.Discharged, id) {

+@@ -546,8 +568,10 @@ func (w *world) relocationLeftovers(n *claim, op opState) {

+ // drain leaves starting for releasing once both participants' execution

+ // leases are current (role() writes them on every read of the claim), and

+ // the CAS records releasing_since for the release deadline; a failover

+-// never enters starting in this model (it starts at pinning, Task 3). The

+-// mutation of reloc-exec-ack-barrier moves on with no acknowledgement.

++// never enters starting in this model (it starts at pinning, Task 3, and

++// PinFailover's barrier is checked there before the pin is selected:

++// rule reloc-failover-ack-before-pin, rev 5). The mutation of

++// reloc-exec-ack-barrier moves on with no acknowledgement.

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

+ op := c.Op

+ if on("reloc-exec-ack-barrier") && !acked(c) {

+@@ -633,8 +657,27 @@ func (w *world) relocReleasing(b *box, c *claim) {

+ // target for a new installation (ToInstalling): a new stamp, journaled as

+ // install_stamp, and a fresh prepared generation id (claim R6-4). The

+ // target must owe no park-local for the host.

++//

++// A pin with no release (a failover, a converted move, a resolved

++// operation) is PinFailover's (rev 5, Astra round 2 finding 1; 1b-next

++// rev 19): the target is named and every participant has acknowledged

++// before the pin is selected, so a manifest that lands while a

++// participant's controller is unavailable is in the pin (rule

++// reloc-failover-ack-before-pin). The model keeps the phase at pinning

++// (ruling 4); this guard is the barrier 1b-next checks on leaving

++// starting. The mutation selects the pin first, as rev 4 did.

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

+- op, h := c.Op, c.Holder

++ op := c.Op

++ if op.Pin == nil && op.Release == nil && on("reloc-failover-ack-before-pin") {

++ if op.Tgt < 0 {

++ w.relocNameTarget(c)

++ return

++ }

++ if !acked(c) {

++ w.stats["failover pin: waits for the acknowledgements"]++

++ return

++ }

+ if op.Pin == nil {

+ if on("reloc-failover-pin-delay") && (op.Release == nil || on("reloc-pin-delay-every-fence")) && w.now < latestObservation(op)+failoverPinDelay {

+ return

+@@ -659,17 +702,7 @@ func (w *world) relocPinning(b *box, c *claim) {

+ return

+ }

+ if op.Tgt < 0 {

+- to := w.chooseBoxExcept(op.SrcRegion, h.App, relocExcept(op)...)

+- if to == nil {

+- return // no eligible box: the recovery pass alerts once (moves §7.10)

+- }

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

+- ok := sameOp(n.Op.ID, op.ID) && n.Op.Kind == "relocating" && n.Op.Phase == "pinning" && n.Op.Tgt < 0

+- if ok {

+- ok = w.nameReplacement(n, to.ID, "pinning")

+- }

+- return ok

+- })

++ w.relocNameTarget(c)

+ return

+ }

+ if on("reloc-exec-ack-barrier") && !acked(c) {

+@@ -691,6 +724,23 @@ func (w *world) relocPinning(b *box, c *claim) {

+ }

++// relocNameTarget is NameTarget at pinning: choose() in the source region

++// over the eligible boxes, the excluded ones left out.

++func (w *world) relocNameTarget(c *claim) {

++ op := c.Op

++ to := w.chooseBoxExcept(op.SrcRegion, c.Holder.App, relocExcept(op)...)

++ if to == nil {

++ return // no eligible box: the recovery pass alerts once (moves §7.10)

++ }

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

++ ok := sameOp(n.Op.ID, op.ID) && n.Op.Kind == "relocating" && n.Op.Phase == "pinning" && n.Op.Tgt < 0

++ if ok {

++ ok = w.nameReplacement(n, to.ID, "pinning")

++ }

++ return ok

++ })

++}

+ // abandonPrepared is abandonPrepared(c) in hostclaim (1b-next ruling

+ // 27, rev 18 finding 3): before an unopened P is replaced or dropped, it

+ // is journaled in abandoned_prepared, so the serving CAS parks it. Every

+@@ -1594,7 +1644,9 @@ func (w *world) deadBoxFiles(x *box) *filesDir {

+ // startFailover is the fence's start of a relocation for a serving

+ // executor (§5.8 reason failover, StartRelocation with a fence; spec 3's

+ // placer supplies the decision): op.exec none, the stamp kept, at pinning

+-// with the target named there (ruling 4); the pin waits out

++// with the target named there (ruling 4); the target is named and

++// acknowledges before the pin is selected (PinFailover's barrier, rule

++// reloc-failover-ack-before-pin, rev 5), and the pin waits out

+ // failoverPinDelay from the fence.

+ func (w *world) startFailover(n *claim, x *box) {

+ n.Op = opState{Kind: "relocating", ID: w.newID("rl"), Phase: "pinning", Exec: -1, Src: x.ID, Tgt: -1, SrcRegion: x.Region,

+@@ -1608,8 +1660,9 @@ func (w *world) startFailover(n *claim, x *box) {

+ // the barrier, its files directory the publisher's stand-in; after its

+ // release only its liveness changes. (1b-next keeps a source lost in

+ // starting at starting until the remaining participant acknowledges,

+-// then PinFailover; the model goes to pinning at once, where the pin

+-// waits out the delay and installing waits for the barrier.) The

++// then PinFailover; the model goes to pinning at once, where the target

++// is named and acknowledges before the pin is selected, rule

++// reloc-failover-ack-before-pin, and the pin waits out the delay.) The

+ // mutation of reloc-source-loss takes a source lost in releasing as

+ // released at what the remote holds, so its unuploaded writes go

+ // undeclared.

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

+index 598d7ba..717ff34 100644

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

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

+@@ -197,4 +197,5 @@ 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-failover-ack-before-pin", // rev 5 (Astra round 2 finding 1; 1b-next rev 19 PinFailover): a pin with no release is selected only after the target is named and every participant acknowledged; the mutation pins first, and a manifest that lands while the target's controller is unavailable is left out (a loss bound: TestFailoverPinWaitsForTheAcknowledgement)

+ }

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

+index a1b97b2..214f5cf 100644

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

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

+@@ -1086,6 +1086,11 @@ type world struct {

+ // startHook runs right after the app starts, before replication opens:

+ // a witness's background worker acknowledging work (R10-1)

+ startHook func(b *box) bool // true: the hook crashed the box

++ // openYield (rev 5, Astra round 2 on claim §11's open boundaries): a

++ // witness's yield after generation.json names the new generation and

++ // before replication opens; true: the start returns there and resumes

++ // at "open" on the next call. Nil outside the witnesses

++ openYield func(b *box) bool

+ // lastIssued is the request issue saw last, for a caller that needs

+ // the request object behind a helper's return value (resumeOpen)

+ lastIssued *request

+```

+- [ ] **Step 2: Run the gate, the identity traces, and the new test under its 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/task5c.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

+nice -n 19 go test ./internal/sim/hostlife/ -run '^(TestCrashAtEachOpenBoundary|TestL18AdverseVolume)$' -count=1 -v 2>&1 | grep -cE '^ --- PASS'

+HOSTLIFE_MUTATE=reloc-failover-ack-before-pin nice -n 19 go test ./internal/sim/hostlife/ -run '^TestFailoverPinWaitsForTheAcknowledgement$' -count=1 2>&1 | grep -E '^(ok|--- FAIL)' | head -1

+```

+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`, `6` (the four stages and the two shapes of the adverse volume, counted as subtests at the second level), `--- FAIL: TestFailoverPinWaitsForTheAcknowledgement`.

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

+```bash

+git add internal/sim/hostlife/

+git commit -m "sim: Astra's round 2 on the two-box model: a failover's target acknowledges before its pin is selected (PinFailover), a crash between the published marker and the open replication, the adverse volume under a failover of the current executor, and the pinned manifest's generation parked at completion

+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 47 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 21 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 48 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 22 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`

@@ -7707,10 +8150,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..6154bdb

+index 72504e3..37267d6 100644

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

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

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

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

@@ -7735,8 +8178,9 @@ index 72504e3..6154bdb

+reloc-pin-delay-every-fence missed a loss bound like reloc-failover-pin-delay; TestPinWaitsForEveryFenceObservation replaces the target after the source's release and fails under the mutation

+reloc-deadline-from-observed-at missed liveness: a deadline from the termination marks stuck earlier than 1b-next would, which the operator then resolves; TestDeadTargetDeadlineFromObservation delays the observation past the deadline and fails under the mutation

+tie-hash-host missed a preference: either winner is a correct choice; TestTieHashFollowsTheHost computes both hosts' winners independently and fails under the mutation

++reloc-failover-ack-before-pin missed a loss bound like reloc-failover-pin-delay: a pin selected before the target acknowledged misses only files that land later, and the sweep's controllers acknowledge within a step of being named; TestFailoverPinWaitsForTheAcknowledgement holds the target's controller while the newer manifest lands and fails under the mutation

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

-index c583d97..883996e

+index c583d97..883996e 100755

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

+++ b/internal/sim/hostlife/mutate.sh

@@ -9,6 +9,9 @@

@@ -7849,11 +8293,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`, `47`, `155`, `ok`.

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

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

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

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

```bash

export GOFLAGS=-buildvcs=false

@@ -7897,7 +8341,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 4 (its rulings 1 to 25; 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).

+- the plan that built it, `docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md` rev 5 (its rulings 1 to 25, ruling 4 as rev 5 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`).

## Fixed: do not re-argue

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

|---|---|---|---|---|

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

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

@@ -7987,7 +8432,8 @@ The model's rev 4 found two gaps that neither 1b-next rev 19 nor moves rev 7.22

11. The plan's rulings 13 to 19 (14, 16 and 17 as rev 3 rewrote them to mirror 1b-next rulings 26, 27 and 25): accept each, or say why it is wrong.

12. Dormancy: anything in the two-box code that changes a one-box outcome (the COUNTERS line and the trace comparisons say no; check the reasoning, ruling 1, and ruling 2's caveat on the converted move).

13. (Rev 4) Astra round 1's fixes: stuck refuses admission; region HA checks a sole box; durable acknowledgements, kept apart from controller readiness, gate every transition; every fence observation is retained and the deadline runs from `observed_at`; `TestL18TerminationAtEveryExactPhase` stops in exactly each phase, `probe-failed` included; each named guard's direct test fails without it.

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

+15. (Rev 5) Astra round 2's fixes: PinFailover's barrier before the failover's pin (ruling 4 as amended: is the barrier at `pinning` equivalent to 1b-next's at `starting`?), the published-marker boundary, the adverse volume under a failover of the current executor, and the pinned manifest's generation parked at completion: does 1b-next's `CompleteRelocation` retire the pinner's retained copy?

+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

@@ -8026,7 +8472,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, 47 rules; rev 3 added four for rev 17 to 19, rev 4 ten for Astra's round 1); 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, 47 rules; rev 3 added four for rev 17 to 19, rev 4 ten for Astra's round 1, rev 5 one for round 2); 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.