amadan
docs: two-box model plan rev 8, Astra round 5: a pending relocation fence holds the regional phase as Worker.Step's early return does, the worker's checks in Worker.Step's order, Task 5E and the round 5 dispositions
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+317
−9
docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md+317 −9
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 fea58c6cb..5f99ed7cb 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,45 @@ |
| -# Region HA: the joint model with two boxes per region (L18) Implementation Plan (rev 7) |
| +# Region HA: the joint model with two boxes per region (L18) Implementation Plan (rev 8) |
| > **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:** Ten tasks (rev 4 adds Task 5B, rev 5 Task 5C, rev 7 Task 5D) 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 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:** Eleven tasks (rev 4 adds Task 5B, rev 5 Task 5C, rev 7 Task 5D, rev 8 Task 5E) over one Go test package (every file is `_test.go`; nothing here is product code). Task 1 generalises the world's shape (`boxesPerRegion`, 1 or 2) so the one-box sweep stays byte-identical to the baseline and a two-box sweep runs beside it. Task 2 replaces the collapsed `relocate` with spec §5.8's full phase table for a drain, with 1b-next rev 16's guards on it: the release sequence and its deadline, the acknowledgement barrier on every phase change, the pin bound to the claim version it was selected against and to an evidenced empty listing, the prepared generation, the local install with its receipt, EnsureLocal before P's first admission and VerifyReceipt after it, `prepared_opened` journaled, three probe attempts counted before they are made, `released` coverage, the row cases, nested relocation after `probe-failed` and the replacement cap. Task 3 adds termination by the cloud with the regional worker's fence (lost, timers declared, regional chores passed to the region, local chores discharged only on qualifying volume evidence), automatic enrollment, failover from `serving`, source loss, the target replacement table, the phase-sensitive exhausted-target fence and the park-local exclusion from replacement. Task 4 adds the files publisher, P's prepared manifest at sequence 0, the files pin and the files live set. Task 5 writes the scenarios: a witness for every safety guard, every L18 case in a one-box and in a two-box region, claim §11's extras, direct evidence for every bound, and three findings. Task 5B (rev 4) answers Astra's round 1 on this plan: faithful guards with a discriminating test each, the exact phase matrix and claim §11's remaining cases. Task 5C (rev 5, regenerated in rev 6) answers rounds 2 and 3: PinFailover's barrier before an initial failover's pin, the boundary between the published marker and the open replication, and the adverse volume under a failover. Task 5D (rev 7) answers round 4: the target is named before any pin on every path, the phase predicates know `PinFailover`, and a failover passes Worker.Start's guards. Task 5E (rev 8) answers round 5: a pending fence holds the phase, as Worker.Step's early return does. Task 6 wires the shape and the region HA rule group into `mutate.sh` and `expected-outcomes.txt`. Task 7 writes the joint-round brief against 1b-next rev 16. Every rule is a named guard in `rules_test.go` whose comment names the 1b-next function it mirrors. |
| **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 8: round 5 dispositions |
| + |
| +Astra's round 5 (`CODEX-PLAN-REGION-HA-TWO-BOX-R5.md`, against `56ea4a15`) found all three round 4 findings resolved and raised one new P2. Its verdict was "not ready". It is accepted and fixed in a new **Task 5E**, a patch on Task 5D's tree. Task 6's patch is regenerated on top of it. Tasks 1 to 5D are unchanged. |
| + |
| +| # | Evidence checked | Disposition | What changed | Where | Guard removed: the test that fails | |
| +|---|---|---|---|---|---| |
| +| R5 #1 (P2) | Correct. `fenceStep` reported only a changed claim. When a terminated target had no eligible replacement before its deadline, `replaceTarget` refused the CAS, and `workerMode` went on into `role` and the phase switch. 1b-next rev 19's `Worker.Step` instead returns `w.replace(...)` as soon as it finds the target's fence, before the phase switch. | accepted | `fenceStep` now returns `(changed, pending)`. A fence it could not consume for a relocation's source or target is pending. `workerMode` passes that to `role` as `box.fencePending`. While it is set, `relocate` makes no regional transition: no ToReleasing, PinAfterRelease, pin, ToInstalling or deadline marks. The live executor's own release sequence and its journal still run (`relocJournalRelease`), because that is the participant's work (1b-next Task 7), not Worker.Step's. So do leases, acknowledgements, cleanups and admissions, which `role` runs before `relocate`. This is the new rule `reloc-fence-pending-blocks`. Its mutation goes on into the phase switch. It is an expected miss: no invariant tells the phases apart, and the gate's two-box sweep never met a pending fence. | Task 5E | `TestPendingTargetFenceHoldsThePhase`, with subtests `starting` and `pinning`. A drain's target has acknowledged; in `starting` the source has not yet. The target is terminated, and the region's group launches no replacement. For `releaseDeadline - 10` steps of the source's worker, the phase must not move, no pin may be selected, and the target must not be fenced. Past the deadline the fence is consumed into `stuck`. Under the mutation, both subtests fail at the first step (`releasing`; a pin). | |
| + |
| +**The worker's checks before the phase switch, compared with 1b-next `Worker.Step` in order.** |
| + |
| +| 1b-next `Worker.Step` | Model (`workerMode`, `fenceStep`, `role`, `relocate`) | Rev 8 | |
| +|---|---|---| |
| +| 1. `ready`, then `self`: a worker whose own box is fenced is not a worker | a destroyed box does not run; `fenceStep` and `relocate` refuse a box that is lost or unenrolled | same | |
| +| 2. read the claim; return unless relocating, in this worker's region, and not stuck | `fenceStep` considers boxes of the worker's own region only; `fence` consumes nothing for a stuck operation; `relocate` returns for another region or a stuck operation | same effect. The stuck check comes after `fenceStep` in the model, but `fence` refuses a stuck operation, so nothing is written. | |
| +| 3. the source's fence, if the source is not on lost: `FenceSource`, return | the source ranked first | same | |
| +| 4. the target's fence, if a target is named and not on lost: `return w.replace(...)`, whatever it wrote | candidates were the source first, then **any other named box in box order**. The target could follow a chore owner's fence, and a refused replacement fell through to the phase switch. | **Fixed:** the order is source, then target, then other named boxes (a chore owner's fence is the termination worker's, not `Worker.Step`'s). A refused replacement is pending and holds the phase (R5 #1). | |
| +| 5. the phase switch | `relocate`'s switch | unchanged | |
| + |
| +`role` runs participant work (lease renewal, `recordAck`, `finishParticipation`, the start's resume, admissions) between `fenceStep` and `relocate`. None of it is a `Worker.Step` transition, and all of it stays schedulable while a fence is pending. The stalled-worker fault (`resumeStale`) resumes a step read earlier, without a new `fenceStep`. It stands for a `Worker.Step` that stalled after its own fence checks: it revalidates the step (`revalidate-before-effect`), and its CAS carries the version it read. A pending fence writes nothing, so production's stalled step could make the same CAS. It is unchanged. |
| + |
| +**Dry run (2026-10-08).** The scratch module was rebuilt from the baseline, with the identity tests and Task 1 from prose. The patches for Tasks 2 to 5D were applied from this document, then Task 5E and the regenerated Task 6. After each: build, vet, gofmt, the gate, and the COUNTERS and both trace files compared byte for byte with the baseline's. |
| + |
| +| After | One-box COUNTERS and traces | Two-box | Gate | |
| +|---|---|---|---| |
| +| Tasks 1 to 5D | identical | as in rev 7 | ok | |
| +| Task 5E | identical | 300, 0 failed, 486 | ok. `TestPendingTargetFenceHoldsThePhase` passes, and both subtests fail under `reloc-fence-pending-blocks`. | |
| +| Task 6 | the same | the same | ok. `@regionha` lists 51 rules, 159 in all. | |
| + |
| +No mutation sweep was run, and the scratch module was then removed. |
| + |
| ## Rev 7: round 4 dispositions |
| Astra's round 4 (`CODEX-PLAN-REGION-HA-TWO-BOX-R4.md`, against `cc69376d`) found both round 3 findings resolved and raised three new P2 fidelity findings. Its verdict was "not ready". All three are accepted, and each is fixed in a new **Task 5D**, a patch on Task 5C's tree. Task 6's patch is regenerated on top of it. Tasks 1 to 5C are unchanged. |
| @@ -8896,9 +8926,284 @@ Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>" |
| --- |
| +### Task 5E: Astra's round 5: a pending fence holds the phase, and the worker's checks in Worker.Step's order (rev 8) |
| + |
| +This is described in "Rev 8: round 5 dispositions" above. It contains: |
| +- `fenceStep` returns `(changed, pending)` and ranks its candidates source, target, others. |
| +- `box.fencePending`, set by `workerMode` around `role`. |
| +- In `relocate`, the rule `reloc-fence-pending-blocks`, with `relocJournalRelease` as the participant's release. |
| +- `TestPendingTargetFenceHoldsThePhase`. |
| + |
| +**Files:** |
| +- Modify: `regionha_test.go` (`fenceStep`, `relocJournalRelease`), `moves_test.go` (`workerMode`, `relocate`), `world_test.go` (`box.fencePending`), `rules_test.go`, `regionha_round1_test.go` |
| + |
| +- [ ] **Step 1: Apply the patch** |
| + |
| +```diff |
| +diff --git a/internal/sim/hostlife/moves_test.go b/internal/sim/hostlife/moves_test.go |
| +index 6150cf5..fd657a5 100644 |
| +--- a/internal/sim/hostlife/moves_test.go |
| ++++ b/internal/sim/hostlife/moves_test.go |
| +@@ -51,10 +51,18 @@ func (w *world) workerMode(b *box, obl bool) { |
| + } else if w.rng.Intn(10) == 0 { |
| + b.stale = c.clone() |
| + } |
| +- if w.fenceStep(b, c) { |
| ++ changed, pending := w.fenceStep(b, c) |
| ++ if changed { |
| + return // the regional worker's termination fence (region HA §5.9), before its role |
| + } |
| ++ // a relocation participant's fence this worker could not consume yet |
| ++ // (a dead target with no spare before its deadline): Worker.Step |
| ++ // returns w.replace(...) before the phase switch, so the regional |
| ++ // transitions wait; the participant work that does not go through |
| ++ // Worker.Step still runs (rev 8, Astra round 5) |
| ++ b.fencePending = pending |
| + w.role(b, c) |
| ++ b.fencePending = false |
| + } |
| + |
| + // initRecord is claim rev 6.5 §6.4's initialization (R5-4): a box creates |
| +@@ -295,6 +303,18 @@ func (w *world) relocate(b *box, c *claim) { |
| + if b.Region != op.SrcRegion || b.Destroyed || contains(c.Lost, b.ID) || !b.Enrolled || op.Stuck != "" { |
| + return |
| + } |
| ++ if b.fencePending && on("reloc-fence-pending-blocks") { |
| ++ // Worker.Step returned w.replace(...) before its phase switch (rev |
| ++ // 8, Astra round 5): no regional transition while a participant's |
| ++ // fence is pending. A live executor's own release sequence is the |
| ++ // participant's (1b-next Task 7), not Worker.Step's, so it runs. |
| ++ // The mutation goes on into the phase switch, as rev 7 did |
| ++ w.stats["relocation: phase held, a participant's fence is pending"]++ |
| ++ if (op.Phase == "releasing" || op.Phase == "probe-failed") && b.ID == op.Exec && (op.Release == nil || op.Release.Box != op.Exec) { |
| ++ w.relocJournalRelease(b, c) |
| ++ } |
| ++ return |
| ++ } |
| + switch op.Phase { |
| + case "starting": |
| + w.relocStarting(b, c) |
| +diff --git a/internal/sim/hostlife/regionha_round1_test.go b/internal/sim/hostlife/regionha_round1_test.go |
| +index 6cc4581..28f7dd7 100644 |
| +--- a/internal/sim/hostlife/regionha_round1_test.go |
| ++++ b/internal/sim/hostlife/regionha_round1_test.go |
| +@@ -710,6 +710,63 @@ func TestFailoverTargetLossAroundPinFailover(t *testing.T) { |
| + } |
| + } |
| + |
| ++// TestPendingTargetFenceHoldsThePhase (reloc-fence-pending-blocks; rev |
| ++// 8, Astra round 5): a drain's target has acknowledged and is terminated, |
| ++// once in starting and once in pinning before a pin; the region's group |
| ++// launches no replacement, so the fence cannot be consumed until its |
| ++// deadline. Until then the source's worker makes no regional transition: |
| ++// starting does not go to releasing, and pinning selects no pin. Under |
| ++// the mutation the worker goes on into the phase switch and this test |
| ++// fails. Past the deadline the fence is consumed and the operation is |
| ++// stuck, as FenceTargetWithoutSpare makes it. |
| ++func TestPendingTargetFenceHoldsThePhase(t *testing.T) { |
| ++ for _, phase := range []string{"starting", "pinning"} { |
| ++ t.Run(phase, func(t *testing.T) { |
| ++ w := twoBoxWitness() |
| ++ from, to := w.boxes[0], w.boxes[3] |
| ++ w.serve(from, 1, app0) |
| ++ w.running(t, from) |
| ++ w.published(t, from) |
| ++ w.oneBoxRegion[0] = true // no replacement launches: no spare |
| ++ w.drainTo(t, to) |
| ++ if phase == "starting" { |
| ++ // the target's controller acknowledges (AcknowledgeExecution); |
| ++ // the source has not yet, so the operation stays in starting |
| ++ to.ExecUntil = w.localNow(to) + execTTL |
| ++ w.recordAck(to, w.claim.clone()) |
| ++ } else if !w.stepUntil(t, 1500, "the target acknowledged at "+phase, func() bool { |
| ++ c := w.claim |
| ++ return contains(c.Op.Acks, to.ID) && w.atPhase(phase)() && c.Op.Pin == nil |
| ++ }) { |
| ++ w.mustHold(t) |
| ++ } |
| ++ if c := w.claim; !contains(c.Op.Acks, to.ID) || !w.atPhase(phase)() || c.Op.Pin != nil { |
| ++ t.Fatalf("not at %s with the target acknowledged: %s", phase, w.state()) |
| ++ } |
| ++ w.oneBoxRegion[0] = false |
| ++ w.terminate(to) |
| ++ w.oneBoxRegion[0] = true |
| ++ for i := 0; i < releaseDeadline-10; i++ { |
| ++ w.tick(w.act(from)) |
| ++ c := w.claim |
| ++ if relocPhaseName(c.Op) != phase || c.Op.Pin != nil { |
| ++ t.Fatalf("the phase moved on while the target's fence was pending (step %d): %s", i, w.state()) |
| ++ } |
| ++ if contains(c.Lost, to.ID) { |
| ++ t.Fatalf("the dead target was fenced with no spare before its deadline: %s", w.state()) |
| ++ } |
| ++ } |
| ++ w.mustHold(t) |
| ++ if w.stats["relocation: phase held, a participant's fence is pending"] == 0 { |
| ++ t.Fatalf("no worker step held the phase") |
| ++ } |
| ++ if !w.reach(t, 100, "the fence consumed into stuck", func() bool { c := w.claim; return contains(c.Lost, to.ID) && c.Op.Stuck != "" }, w.act(from)) { |
| ++ 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 cb1d257..376e151 100644 |
| +--- a/internal/sim/hostlife/regionha_test.go |
| ++++ b/internal/sim/hostlife/regionha_test.go |
| +@@ -2,6 +2,7 @@ package hostlife |
| + |
| + import ( |
| + "fmt" |
| ++ "sort" |
| + "strings" |
| + ) |
| + |
| +@@ -1440,9 +1441,9 @@ func (w *world) regionHAOwnsLoss(b *box) bool { |
| + // destroyed box. An unenrolled box has no roster entry to bind the fence |
| + // to (HA7) and is never fenced. The source's fence is consumed before the |
| + // target's, as Worker.Step orders them. |
| +-func (w *world) fenceStep(b *box, c *claim) bool { |
| ++func (w *world) fenceStep(b *box, c *claim) (changed, pending bool) { |
| + if c == nil || !b.Enrolled || contains(c.Lost, b.ID) { |
| +- return false |
| ++ return false, false |
| + } |
| + var cands []*box |
| + for _, x := range w.boxes { |
| +@@ -1455,15 +1456,23 @@ func (w *world) fenceStep(b *box, c *claim) bool { |
| + if !w.claimNames(c, x) { |
| + continue |
| + } |
| +- if c.Op.Kind == "relocating" && x.ID == c.Op.Src { |
| +- cands = append([]*box{x}, cands...) |
| +- } else { |
| +- cands = append(cands, x) |
| +- } |
| ++ cands = append(cands, x) |
| + } |
| + if len(cands) == 0 { |
| +- return false |
| ++ return false, false |
| ++ } |
| ++ // Worker.Step's order (rev 8): the source's fence, then the target's, |
| ++ // then any other box the claim names (a chore's owner) |
| ++ rank := func(x *box) int { |
| ++ switch { |
| ++ case c.Op.Kind == "relocating" && x.ID == c.Op.Src: |
| ++ return 0 |
| ++ case c.Op.Kind == "relocating" && x.ID == c.Op.Tgt: |
| ++ return 1 |
| ++ } |
| ++ return 2 |
| + } |
| ++ sort.SliceStable(cands, func(i, j int) bool { return rank(cands[i]) < rank(cands[j]) }) |
| + if x := cands[0]; x.FenceObservedAt == 0 { |
| + // hostfence.TerminationWorker: the first worker to observe the |
| + // terminated state writes the box-fences record with that |
| +@@ -1474,7 +1483,12 @@ func (w *world) fenceStep(b *box, c *claim) bool { |
| + } |
| + before := w.claim.Ver |
| + w.fence(b, c, cands[0]) |
| +- return w.claim.Ver != before |
| ++ if w.claim.Ver != before { |
| ++ return true, false |
| ++ } |
| ++ // nothing written: for a relocation's source or target the fence is |
| ++ // pending (rule reloc-fence-pending-blocks) |
| ++ return false, c.Op.Kind == "relocating" && rank(cands[0]) < 2 |
| + } |
| + |
| + // claimNames: the claim gives x a role, so a fence changes it. |
| +@@ -2258,3 +2272,31 @@ func (w *world) preparedManifestHere(b *box, c *claim, gen string) bool { |
| + bl := &blob{Kind: "files", Inc: h.Inc, Gen: gen, Seq: 0, Files: b.Files.clone(), Timers: append([]int(nil), b.Timers...), Text: c.Op.ID, Base: w.issued} |
| + return w.ackedPut(b, manifestKey(h.Location, gen, 0), bl, true) |
| + } |
| ++ |
| ++// relocJournalRelease is the participant's release (1b-next Task 7): the |
| ++// live executor runs its release sequence and journals it |
| ++// (JournalRelease), the source in releasing, a failed target in |
| ++// probe-failed. It is the release branch of relocReleasing and |
| ++// relocProbeFailed, run by itself while a fence is pending (rev 8). |
| ++func (w *world) relocJournalRelease(b *box, c *claim) { |
| ++ op := c.Op |
| ++ phase := op.Phase |
| ++ r := w.relocRelease(b, c) |
| ++ if r == nil { |
| ++ return |
| ++ } |
| ++ if w.cas(c, func(n *claim) bool { |
| ++ ok := sameOp(n.Op.ID, op.ID) && n.Op.Kind == "relocating" && n.Op.Phase == phase && n.Op.Exec == b.ID && (n.Op.Release == nil || phase == "probe-failed" && n.Op.Release.Box != b.ID) |
| ++ if ok { |
| ++ n.Op.Release = r |
| ++ } |
| ++ return ok |
| ++ }) { |
| ++ if phase == "releasing" { |
| ++ w.stats["release journaled: source"]++ |
| ++ } else { |
| ++ w.stats["release journaled: failed target"]++ |
| ++ } |
| ++ w.logf("relocation %s: box %d released the host at TXID %d (flushed=%v), a fence pending", op.ID, b.ID, r.FinalTX, r.Flushed) |
| ++ } |
| ++} |
| +diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go |
| +index 06b9849..ed23391 100644 |
| +--- a/internal/sim/hostlife/rules_test.go |
| ++++ b/internal/sim/hostlife/rules_test.go |
| +@@ -197,6 +197,7 @@ var allRules = []string{ |
| + "files-live-set-moves-parks", // finding F4 (rev 4), claim §6.2a: moves' parks (a push's whole-location park, a landing's install park, a rollback's return park) keep the files live set; the mutation archives it with the rest and the next failover can never pin the live files (INV-3) |
| + "reloc-clear-after-cleanup", // 1b-next ruling 20 and rev 6 R4-5 (Finish clears the record only after a successful scoped cleanup): a failed cleanup keeps the controller record, which blocks executable updates (claim §11's witness); the mutation clears it and an update runs over the unfinished cleanup (INV-29) |
| + "fence-converts-committed-landing", // finding F5 (rev 4; claim §11 "automatic target loss racing the record commit CAS"): a landing whose record committed and whose target is then terminated becomes a failover in the target's region; the mutation leaves it to the operator, and it never completes (INV-3) |
| ++ "reloc-fence-pending-blocks", // rev 8 (Astra round 5; 1b-next rev 19 Worker.Step returns w.replace(...) before its phase switch): while a relocation participant's fence is pending (a dead target, no spare, before its deadline) no regional phase transition runs; the participant's own release still does; the mutation goes on into the phase switch (TestPendingTargetFenceHoldsThePhase) |
| + "reloc-name-before-pin", // rev 7 (Astra round 4 finding 1; 1b-next rev 19 Worker.pinning): a relocation at pinning with no target names one before it selects a pin, on every path; the mutation pins first, and a manifest that lands while no box is eligible is left out (a loss bound: TestConvertedMoveWaitsForATargetBeforeItsPin) |
| + "reloc-failover-start-guard", // rev 7 (Astra round 4 finding 3; 1b-next rev 19 Worker.Start, StartRelocation): a serving executor's failover starts only with an eligible target, the app admitting the registration (and its recheck) and RelocationStartGuard with the source fenced; the mutation starts at once (TestFailoverStartWaitsForAdmission, TestFailoverStartWaitsForParkReplica) |
| + "reloc-failover-ack-before-pin", // rev 5 and 6 (Astra rounds 2 and 3; 1b-next rev 19 PinFailover): an initial failover (op.PinFailover, the model's starting) selects its pin only after the target is named and every participant acknowledged; converted moves, nested failovers and replays pin first, as Worker.pinning does; 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 f901aed..5cb9f47 100644 |
| +--- a/internal/sim/hostlife/world_test.go |
| ++++ b/internal/sim/hostlife/world_test.go |
| +@@ -373,6 +373,7 @@ type box struct { |
| + execRecord string |
| + cleanupPending bool |
| + cleanupFails bool |
| ++ fencePending bool // (rev 8) this worker step found a relocation participant's fence it could not consume |
| + FenceObservedAt int // the box-fences record's observed_at: when a worker first saw it terminated; 0 no record (rev 4) |
| + Enrolled bool // the roster holds an active entry with its proven cloud identity (H11); a replacement box is enrolled automatically enrollDelay steps after it launches (H16, H17) |
| + EnrollAt int |
| +``` |
| + |
| +- [ ] **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/ |
| +nice -n 19 go test ./internal/sim/hostlife/ -count=1 -v 2>&1 | tee $TMPDIR/twobox/task5e.log | grep -E "seeds, |^--- FAIL|^ --- FAIL|^ok|^FAIL" |
| +diff $TMPDIR/twobox/baseline-counters.json <(grep COUNTERS $TMPDIR/twobox/task5e.log | head -1 | sed 's/.*COUNTERS //') && echo ONE-BOX-COUNTERS-IDENTICAL |
| +HOSTLIFE_TRACE_OUT=$TMPDIR/twobox/trace.txt HOSTLIFE_TRACE_OUT_SEEDS=$TMPDIR/twobox/seeds.txt nice -n 19 go test ./internal/sim/hostlife/ -run '^TestOneBox' -count=1 >/dev/null |
| +cmp $TMPDIR/twobox/baseline-trace.txt $TMPDIR/twobox/trace.txt && cmp $TMPDIR/twobox/baseline-seeds.txt $TMPDIR/twobox/seeds.txt && echo ONE-BOX-TRACES-IDENTICAL |
| +HOSTLIFE_MUTATE=reloc-fence-pending-blocks nice -n 19 go test ./internal/sim/hostlife/ -run '^TestPendingTargetFenceHoldsThePhase$' -count=1 -v 2>&1 | grep -cE '^ --- FAIL' |
| +``` |
| + |
| +Expected (the dry run's): `300 seeds, 0 failed, 483 completed operations; mutated="" boxes=1`, `300 seeds, 0 failed, 486 completed operations; mutated="" boxes=2`, `ok`, `ONE-BOX-COUNTERS-IDENTICAL`, `ONE-BOX-TRACES-IDENTICAL`, `2`. |
| + |
| +- [ ] **Step 3: Commit** |
| + |
| +```bash |
| +git add internal/sim/hostlife/ |
| +git commit -m "sim: Astra's round 5 on the two-box model: a relocation participant's fence that cannot be consumed yet holds the regional phase, as Worker.Step returns before its phase switch, and the worker fences the source, then the target, then any other box |
| + |
| +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 50 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 24 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 51 region HA rules is checked by the sweep once it exists. This task makes the shape explicit in every verdict (`[boxes=N]`), adds `@regionha` (the rules of the region HA block, one mutation check per guard, for a rerun of the new guards alone), adds `HOSTLIFE_LIST=1` (print the rules a run would check and run nothing), and lists the 25 region HA rules that are not caught alone, each with its reason and the direct test that shows it. |
| **Files:** |
| - Modify: `internal/sim/hostlife/mutate.sh`, `internal/sim/hostlife/expected-outcomes.txt` |
| @@ -8907,10 +9212,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..71ab604 100644 |
| +index 72504e3..4a75aab 100644 |
| --- a/internal/sim/hostlife/expected-outcomes.txt |
| +++ b/internal/sim/hostlife/expected-outcomes.txt |
| -@@ -21,3 +21,27 @@ admit-bind-op missed caught with claim-cas-opid: the model's general CAS conditi |
| +@@ -21,3 +21,28 @@ 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) |
| @@ -8938,6 +9243,7 @@ index 72504e3..71ab604 100644 |
| +reloc-failover-ack-before-pin missed a loss bound like reloc-failover-pin-delay: an initial failover's pin selected before its 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 |
| +reloc-name-before-pin missed a loss bound like reloc-failover-pin-delay: a converted move's or a replay's pin selected before a target is named misses only files that land while no box is eligible; TestConvertedMoveWaitsForATargetBeforeItsPin holds every box ineligible while the newer manifest lands and fails under the mutation |
| +reloc-failover-start-guard missed a fidelity guard: the mutation starts the failover earlier (no target yet, admission closed, a park-replica outstanding), and no model invariant distinguishes the earlier start, whose target is then named at pinning; TestFailoverStartWaitsForAdmission and TestFailoverStartWaitsForParkReplica fail under the mutation |
| ++reloc-fence-pending-blocks missed a fidelity guard: under the mutation the phase moves on while a dead target's fence waits for a spare, and the fence is consumed later by the replacement table at whatever phase the operation reached, which no model invariant distinguishes; TestPendingTargetFenceHoldsThePhase fails under the mutation |
| diff --git a/internal/sim/hostlife/mutate.sh b/internal/sim/hostlife/mutate.sh |
| index c583d97..883996e 100755 |
| --- a/internal/sim/hostlife/mutate.sh |
| @@ -9052,11 +9358,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`, `50`, `158`, `ok`. |
| +Expected (the dry run's): `SYNTAX-OK`, `51`, `159`, `ok`. |
| - [ ] **Step 3: The revision's sweep (the one allowed; serial, niced)** |
| -Run only when Tasks 1 to 5D are committed, nothing else is sweeping on the machine (`pgrep -f hostlife.test` empty), and the gate passes: |
| +Run only when Tasks 1 to 5E are committed, nothing else is sweeping on the machine (`pgrep -f hostlife.test` empty), and the gate passes: |
| ```bash |
| export GOFLAGS=-buildvcs=false |
| @@ -9100,7 +9406,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 7 (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). |
| +- the plan that built it, `docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md` rev 8 (its rulings 1 to 25, ruling 4 as revs 5 to 7 amended it; rulings 14, 16 and 17 mirror 1b-next's fixes for F1 to F3; "Rev 4: round 1 dispositions" answers Astra's round 1 on the plan, `CODEX-PLAN-REGION-HA-TWO-BOX-R1.md`, and maps each past finding to its proving artifact; "Rev 5: round 2 dispositions" answers round 2, `CODEX-PLAN-REGION-HA-TWO-BOX-R2.md`; "Rev 6: round 3 dispositions" answers round 3, `CODEX-PLAN-REGION-HA-TWO-BOX-R3.md`; "Rev 7: round 4 dispositions" answers round 4, `CODEX-PLAN-REGION-HA-TWO-BOX-R4.md`, and compares every entry point with 1b-next; "Rev 8: round 5 dispositions" answers round 5, `CODEX-PLAN-REGION-HA-TWO-BOX-R5.md`, and compares the worker's checks with `Worker.Step`). |
| ## Fixed: do not re-argue |
| @@ -9163,6 +9469,7 @@ prompt (branch `region-ha-hostlife-two-box`) against plan 1b-next rev |
| | reloc-failover-ack-before-pin | `PinFailover`'s `requireAcks`, the initial failover only | two-box R2 #1, R3 #1 | D6, §5.8 | expected miss (loss bound); `TestFailoverPinWaitsForTheAcknowledgement` | |
| | reloc-name-before-pin | `Worker.pinning`'s `NameTarget` before `pinUnderLease` | two-box R4 #1 | §5.8, moves §7.10 | expected miss (loss bound); `TestConvertedMoveWaitsForATargetBeforeItsPin` | |
| | 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-fence-pending-blocks | `Worker.Step` returns `w.replace(...)` before its phase switch | two-box R5 #1 | §5.8, §5.9 | expected miss; `TestPendingTargetFenceHoldsThePhase` | |
| ## Findings F1 to F3, closed, and the open window L21 |
| @@ -9196,6 +9503,7 @@ The model's rev 4 found two gaps that neither 1b-next rev 19 nor moves rev 7.22 |
| 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, which is the model's abstraction of the at-rest sweep (claim §6.2a) and the storage follow-up (1b-next ruling 21), not a `CompleteRelocation` step. |
| 16. (Rev 6) Astra round 3's fix: only an initial failover (`opState.PinFailover`) waits for the acknowledgements before its pin; a converted move, a nested failover and a replay pin first (`TestConvertedMovePinsBeforeAcknowledgement`). Is the flag a faithful stand-in for 1b-next's `starting`? |
| 17. (Rev 7) Astra round 4's fixes and the entry-point table in "Rev 7: round 4 dispositions": the target named before any pin on every path, `relocPhaseName`, and the failover started through Worker.Start's guards in their order. Is any entry point still ordered differently from 1b-next? |
| +18. (Rev 8) Astra round 5's fix and the `Worker.Step` order table in "Rev 8: round 5 dispositions": a pending fence holds every regional transition, while the participant's own release and the box's other work stay schedulable. Is anything the model still runs while a fence is pending a `Worker.Step` transition? |
| 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 |
| @@ -9235,7 +9543,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, 50 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); 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, 51 rules; rev 3 added four for rev 17 to 19, rev 4 ten for Astra's round 1, rev 5 one for round 2, rev 7 two for round 4, rev 8 one for round 5); the findings the model cannot reach are mapped to 1b-next's own tests in "Rev 4: round 1 dispositions"; the stage B contracts (R1 to R10, the lifecycle property of revs 14 to 16, hostexec's controller recovery) have no model step and are named as such. Each rule's comment names its 1b-next function. |
| - **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. |