amadan
docs: two-box model plan rev 6, Astra round 3: PinFailover's barrier only for an initial failover (explicit flag), converted moves pin before acknowledgement, the completion park described as the model's abstraction, round 3 dispositions
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+188
−52
docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md+188 −52
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 d4340d84a..a4c6cef8b 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,34 @@ |
| -# Region HA: the joint model with two boxes per region (L18) Implementation Plan (rev 5) |
| +# Region HA: the joint model with two boxes per region (L18) Implementation Plan (rev 6) |
| > **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:** 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. |
| +**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, 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 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 6: round 3 dispositions |
| + |
| +Astra's round 3 (`CODEX-PLAN-REGION-HA-TWO-BOX-R3.md`, against `ee6e35f3`) found all three of round 2's items resolved. It raised one new P2 and one P3, with the verdict "not ready". Both are accepted. Task 5C's patch is regenerated with the fixes (it is still a patch on Task 5B's tree), and Task 6's patch is regenerated on top of it. Tasks 1 to 5B are unchanged. |
| + |
| +| # | Evidence checked | Disposition | What changed | Where | Evidence | |
| +|---|---|---|---|---|---| |
| +| R3 #1 (P2) | Correct. Rev 5's guard held every pin with no release, which covered converted moves, nested failovers after a replacement and operator replays. In 1b-next rev 19, only the initial failover waits for `PinFailover`'s acknowledgements, on leaving `starting`. Those other three enter `pinning` directly, and `Worker.pinning` selects and journals the pin before it checks acknowledgements for `ToInstalling`. The model excluded that production interleaving. | accepted | `PinFailover`'s barrier is now explicit. `opState.PinFailover` stands for 1b-next's `starting` after `StartRelocation` with a fence. It is set by `startFailover` and by a drain's source lost in `starting` (1b-next keeps that one in `starting` until `PinFailover`). While it is set, the target is named and acknowledges, then the PinFailover CAS clears the flag, all before any pin is selected. A converted move, a nested failover and a replay never set it, and the replay clears it. Rule `reloc-failover-ack-before-pin` now guards only the flagged case; its mutation still selects the pin first. | Task 5C; ruling 4 | `TestFailoverPinWaitsForTheAcknowledgement` is unchanged (initial failover) and still fails under the mutation. The new `TestConvertedMovePinsBeforeAcknowledgement` terminates a move's source before the flip. It checks that the pin is journaled before the installing box has acknowledged, and that the acknowledgement still comes before `installing`. Run against rev 5's Task 5C tree, it fails: "box 3 acknowledged before the pin". | |
| +| R3 #2 (P3) | Correct. 1b-next rev 19's `CompleteRelocation` queues the local chores and the abandoned prepared generations. It neither drops the pinner's retained control object nor parks the pinned manifest's generation. The obsolete manifest is not ownerless either: claim §6.2a gives obsolete files to the at-rest sweep, and 1b-next ruling 21 gives retained control objects to the storage follow-up. | accepted | The text in "Rev 5: round 2 dispositions", in `relocationLeftovers`' comment and in the brief now says this. The model parks the pinned manifest's generation at completion as its own abstraction of those two paths, so that INV-10 can check the residue at completion. It is not a `CompleteRelocation` guarantee and not a 1b-next finding. | Task 5C (comment); Rev 5 section; brief | text only | |
| + |
| +**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 this document, then the regenerated Task 5C and 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 5B | identical | as in rev 5 | ok | |
| +| Task 5C (rev 6) | identical | 300, 0 failed, 486 | ok. `TestFailoverPinWaitsForTheAcknowledgement` fails under its mutation; `TestConvertedMovePinsBeforeAcknowledgement` passes, and fails on rev 5's tree. | |
| +| Task 6 | the same | the same | ok. `@regionha` lists 48 rules, 156 in all. | |
| + |
| +No mutation sweep was run, and the scratch module was then removed. |
| + |
| ## 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. |
| @@ -26,7 +45,7 @@ Astra's round 2 (`CODEX-PLAN-REGION-HA-TWO-BOX-R2.md`, against `64a0a793`) found |
| 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. |
| +`relocationLeftovers` now queues a `park-generation` for the pinned manifest's generation when that generation is no longer the holder's. With the fix, every seed passes. **(Corrected in rev 6, Astra round 3 finding 2.)** This park is the model's abstraction, not a `CompleteRelocation` guarantee. 1b-next rev 19's completion queues only the local chores and the abandoned prepared generations. The obsolete manifest is the at-rest sweep's (claim §6.2a), and the pinner's retained control object is the storage follow-up's (1b-next ruling 21). The model parks it at once so INV-10 can check the residue at completion. It is not a 1b-next finding. |
| **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. |
| @@ -196,12 +215,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; rev 5 amends 4. |
| +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 and rev 6 amend 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 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. |
| +4. **Failover starts at `pinning` with the target named there. For an initial failover the D6 barrier is checked before the pin is selected (rev 5, narrowed in rev 6); for every relocation it is checked 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. **(Rev 6, Astra round 3 finding 1.)** Only an initial failover waits. `opState.PinFailover` stands for 1b-next's `starting` after `StartRelocation` with a fence: `startFailover` sets it, and so does a drain whose source is lost in `starting`. While it is set, the operation in `pinning` names its target, waits for `requireAcks`, and clears it in the PinFailover CAS before any pin is selected (rule `reloc-failover-ack-before-pin`). A converted move, a nested failover and an operator's replay enter `pinning` directly, as in 1b-next. There `Worker.pinning` journals the pin first and checks the acknowledgements only for `ToInstalling`. 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 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. |
| @@ -7724,21 +7743,34 @@ 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) |
| +### Task 5C: Astra's rounds 2 and 3: PinFailover's barrier before an initial failover's pin, the published-marker boundary, and the adverse volume under a failover (rev 5, regenerated in rev 6) |
| -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. |
| +This is described in "Rev 5: round 2 dispositions" and "Rev 6: round 3 dispositions" above. It contains: |
| +- The new rule `reloc-failover-ack-before-pin`, in `relocPinning`, with `relocNameTarget` factored out. It applies only while `opState.PinFailover` is set (rev 6). |
| +- `TestConvertedMovePinsBeforeAcknowledgement` (rev 6). |
| - 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` |
| +- Modify: `regionha_test.go` (`relocPinning`, `relocNameTarget`, `relocationLeftovers`, `startFailover` and `fenceSource` set `PinFailover`, comments on `relocStarting`), `console_test.go` (the replay clears `PinFailover`), `protocol_test.go` (the yield in the start's `marker` case), `world_test.go` (`openYield`, `opState.PinFailover`), `rules_test.go`, `regionha_round1_test.go`, `regionha_cases_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 1e7f99d..8061165 100644 |
| +--- a/internal/sim/hostlife/console_test.go |
| ++++ b/internal/sim/hostlife/console_test.go |
| +@@ -1274,6 +1274,7 @@ func (w *world) operator() { |
| + default: |
| + w.abandonPrepared(n) |
| + n.Op.Stuck, n.Op.Replacements, n.Op.Excluded, n.Op.Resolved = "", 0, nil, true |
| ++ n.Op.PinFailover = false // the replay enters pinning directly (rev 6) |
| + if released && op.Exec >= 0 { |
| + n.Op.Excluded = []int{op.Exec} // the target that just failed its probe is not the operator's fresh choice (rev 4) |
| + } |
| 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 |
| @@ -7816,10 +7848,10 @@ index 36efb1e..39e9b52 100644 |
| } |
| diff --git a/internal/sim/hostlife/regionha_round1_test.go b/internal/sim/hostlife/regionha_round1_test.go |
| -index ad0f45d..2758cd7 100644 |
| +index ad0f45d..3f56952 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) { |
| +@@ -408,6 +408,127 @@ func TestFailoverPinWaitsOutTheDelay(t *testing.T) { |
| w.mustHold(t) |
| } |
| @@ -7883,11 +7915,71 @@ index ad0f45d..2758cd7 100644 |
| + w.finish(t) |
| + w.mustHold(t) |
| +} |
| ++ |
| ++// TestConvertedMovePinsBeforeAcknowledgement (rev 6, Astra round 3 |
| ++// finding 1): a move whose source is terminated before the flip becomes |
| ++// a relocation at pinning (moves §7.10). It enters pinning directly, as |
| ++// it does in 1b-next, where Worker.pinning selects and journals the pin |
| ++// first and checks the acknowledgements only for ToInstalling: the pin is |
| ++// journaled before the box that installs has acknowledged, and that box's |
| ++// acknowledgement still comes before the installing CAS. Under rev 5's |
| ++// wider guard the target acknowledged first, and this test fails. |
| ++func TestConvertedMovePinsBeforeAcknowledgement(t *testing.T) { |
| ++ w := twoBoxWitness() |
| ++ src := w.boxes[0] |
| ++ w.serve(src, 1, app0) |
| ++ w.running(t, src) |
| ++ w.published(t, src) |
| ++ w.moveTo(1) |
| ++ if w.claim.Op.Kind != "moving" { |
| ++ t.Fatalf("no move: %s", w.state()) |
| ++ } |
| ++ tgt := w.boxByID(w.claim.Op.Tgt) |
| ++ w.reach(t, 100, "staging begins", func() bool { |
| ++ c := w.claim |
| ++ return c.Op.Kind == "moving" && c.Op.Phase == "preparing" && contains(c.Regions, tgt.Region) |
| ++ }, w.act(src, tgt)) |
| ++ w.terminate(src) |
| ++ var acksAtPin []int |
| ++ if !w.stepUntil(t, 400, "the converted move's pin", func() bool { |
| ++ c := w.claim |
| ++ if c.Op.Kind == "relocating" && c.Op.Pin != nil { |
| ++ acksAtPin = append([]int(nil), c.Op.Acks...) |
| ++ return true |
| ++ } |
| ++ return false |
| ++ }) { |
| ++ w.mustHold(t) |
| ++ } |
| ++ if c := w.claim; c.Op.FenceBox != src.ID || c.Op.PinFailover { |
| ++ t.Fatalf("not a converted move: %s", w.state()) |
| ++ } |
| ++ var installer int = -1 |
| ++ if !w.stepUntil(t, 1500, "installing", func() bool { |
| ++ c := w.claim |
| ++ if c.Op.Kind == "relocating" && c.Op.Phase == "installing" { |
| ++ installer = c.Op.Exec |
| ++ if !acked(c) { |
| ++ t.Fatalf("installing without the acknowledgements: %s", w.state()) |
| ++ } |
| ++ return true |
| ++ } |
| ++ return false |
| ++ }) { |
| ++ w.mustHold(t) |
| ++ } |
| ++ if contains(acksAtPin, installer) { |
| ++ t.Fatalf("box %d acknowledged before the pin: a converted move waited for PinFailover's barrier", installer) |
| ++ } |
| ++ w.servingOn(t, w.boxByID(installer)) |
| ++ 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) { |
| +@@ -451,10 +572,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), |
| @@ -7903,7 +7995,7 @@ index ad0f45d..2758cd7 100644 |
| 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) { |
| +@@ -468,6 +591,16 @@ func TestCrashAtEachOpenBoundary(t *testing.T) { |
| if stage == "marker" { |
| w.holdKey(genMarkerKey(loc)) |
| } |
| @@ -7920,7 +8012,7 @@ index ad0f45d..2758cd7 100644 |
| 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) { |
| +@@ -481,6 +614,15 @@ func TestCrashAtEachOpenBoundary(t *testing.T) { |
| if stage == "open" { |
| return preparedOpened(c) && to.open == nil && hasMain(to) |
| } |
| @@ -7936,7 +8028,7 @@ index ad0f45d..2758cd7 100644 |
| return to.open != nil && to.open.Prepared && to.open.stage == stage |
| }) |
| if !hit { |
| -@@ -488,7 +570,7 @@ func TestCrashAtEachOpenBoundary(t *testing.T) { |
| +@@ -488,7 +630,7 @@ func TestCrashAtEachOpenBoundary(t *testing.T) { |
| } |
| w.crash(to) |
| to.envUnreadyFor = 0 |
| @@ -7946,19 +8038,24 @@ index ad0f45d..2758cd7 100644 |
| w.finish(t) |
| }) |
| diff --git a/internal/sim/hostlife/regionha_test.go b/internal/sim/hostlife/regionha_test.go |
| -index 11c1ee7..c754c40 100644 |
| +index 11c1ee7..28784de 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) { |
| +@@ -530,6 +530,33 @@ 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) |
| ++ // completes it is a dead generation's key, parked here. This is the |
| ++ // model's abstraction, not a CompleteRelocation guarantee (rev 6, |
| ++ // Astra round 3 finding 2): in 1b-next rev 19 completion queues only |
| ++ // the local chores and the abandoned prepared generations; an obsolete |
| ++ // files manifest is the at-rest sweep's (claim §6.2a), and the |
| ++ // pinner's retained control object is the storage follow-up's (1b-next |
| ++ // ruling 21). The model parks it at once so INV-10 can check the |
| ++ // residue at completion |
| + if h := n.Holder; h != nil && op.Pin != nil && op.Pin.ManKey != "" && op.Pin.ManGen != h.Gen { |
| + ret := op.Pin.ManGen |
| + if ret == "" { |
| @@ -7978,7 +8075,7 @@ index 11c1ee7..c754c40 100644 |
| 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) { |
| +@@ -546,8 +573,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 |
| @@ -7986,28 +8083,32 @@ index 11c1ee7..c754c40 100644 |
| -// 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 |
| ++// rule reloc-failover-ack-before-pin, rev 5 and 6). 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) { |
| +@@ -633,8 +662,41 @@ 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. |
| ++// An initial failover (op.PinFailover: 1b-next's starting after |
| ++// StartRelocation with a fence) first passes PinFailover's barrier (rev |
| ++// 5, Astra round 2 finding 1; narrowed in rev 6, round 3 finding 1): the |
| ++// target is named, every participant has acknowledged, and the PinFailover |
| ++// CAS clears the flag, all before any pin is selected; so a manifest that |
| ++// lands while the target's controller is unavailable is in the pin (rule |
| ++// reloc-failover-ack-before-pin). The flag is the model's starting |
| ++// (ruling 4). A converted move, a nested failover after a replacement and |
| ++// an operator's replay enter pinning directly, as in 1b-next, where |
| ++// Worker.pinning selects and journals the pin first and checks the |
| ++// acknowledgements only for ToInstalling. The mutation selects the pin |
| ++// before the barrier, 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.PinFailover && on("reloc-failover-ack-before-pin") { |
| + if op.Tgt < 0 { |
| + w.relocNameTarget(c) |
| + return |
| @@ -8016,11 +8117,21 @@ index 11c1ee7..c754c40 100644 |
| + w.stats["failover pin: waits for the acknowledgements"]++ |
| + return |
| + } |
| ++ if w.cas(c, func(n *claim) bool { |
| ++ ok := sameOp(n.Op.ID, op.ID) && n.Op.Kind == "relocating" && n.Op.Phase == "pinning" && n.Op.PinFailover && n.Op.Tgt == op.Tgt && n.Op.Stuck == "" |
| ++ if ok { |
| ++ n.Op.PinFailover = false |
| ++ } |
| ++ return ok |
| ++ }) { |
| ++ w.logf("relocation %s: PinFailover, box %d acknowledged", op.ID, op.Tgt) |
| ++ } |
| ++ 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) { |
| +@@ -659,17 +721,7 @@ func (w *world) relocPinning(b *box, c *claim) { |
| return |
| } |
| if op.Tgt < 0 { |
| @@ -8039,7 +8150,7 @@ index 11c1ee7..c754c40 100644 |
| return |
| } |
| if on("reloc-exec-ack-barrier") && !acked(c) { |
| -@@ -691,6 +724,23 @@ func (w *world) relocPinning(b *box, c *claim) { |
| +@@ -691,6 +743,23 @@ func (w *world) relocPinning(b *box, c *claim) { |
| } |
| } |
| @@ -8063,44 +8174,67 @@ index 11c1ee7..c754c40 100644 |
| // 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 { |
| +@@ -1594,11 +1663,14 @@ 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 |
| ++// with the target named there (ruling 4); op.PinFailover stands for |
| ++// 1b-next's starting, so the target is named and acknowledges before the |
| ++// pin is selected (PinFailover's barrier, rule |
| ++// reloc-failover-ack-before-pin, rev 5 and 6), 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) { |
| +- RelocReason: "failover", ReqAt: w.now, App: n.Holder.App, SrcGen: n.Holder.Gen, SrcStamp: n.Holder.Stamp, StopFiles: w.deadBoxFiles(x)} |
| ++ RelocReason: "failover", ReqAt: w.now, App: n.Holder.App, SrcGen: n.Holder.Gen, SrcStamp: n.Holder.Stamp, StopFiles: w.deadBoxFiles(x), PinFailover: true} |
| + w.stats["relocation started: failover"]++ |
| + } |
| + |
| +@@ -1608,8 +1680,10 @@ 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 |
| ++// then PinFailover; the model goes to pinning at once with |
| ++// op.PinFailover set for a source lost in starting, so the target |
| ++// 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. |
| +@@ -1622,6 +1696,7 @@ func (w *world) fenceSource(n *claim, x *box) { |
| + n.Op.Exec, n.Op.Phase = -1, "pinning" |
| + return |
| + } |
| ++ n.Op.PinFailover = n.Op.Phase == "starting" // 1b-next keeps it in starting until PinFailover (rev 6) |
| + n.Op.RelocReason, n.Op.Exec, n.Op.Phase = "failover", -1, "pinning" |
| + n.Op.Release, n.Op.StopFiles = nil, w.deadBoxFiles(x) |
| + w.stats["relocation: source lost before its release, converted to failover"]++ |
| diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go |
| -index 598d7ba..717ff34 100644 |
| +index 598d7ba..034684e 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) |
| ++ "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 a1b97b2..214f5cf 100644 |
| +index a1b97b2..f901aed 100644 |
| --- a/internal/sim/hostlife/world_test.go |
| +++ b/internal/sim/hostlife/world_test.go |
| -@@ -1086,6 +1086,11 @@ type world struct { |
| +@@ -837,6 +837,7 @@ type opState struct { |
| + ReleasingSince int // releasing_since: the release deadline's start (ruling 14) |
| + Attempts int // probe_attempts.<op.exec>: counted before each attempt, at most probeTries (ruling 19) |
| + PreparedOpened string // prepared_opened: journaled by the admission that opened P (rev 12 S1) |
| ++ PinFailover bool // (rev 6) the initial failover's starting, 1b-next's StartRelocation with a fence: set by startFailover and by a drain's source lost in starting, cleared by the PinFailover CAS once the target is named and every participant has acknowledged |
| + Resolved bool // an operator's resolve (model ruling 13): the source is eligible as a target again, and an empty listing is accepted |
| + Observed []int // every fence.<box>.observed_at the operation consumed, kept through replacements (rev 4) |
| + Acks []int // exec_ack.<box>: the participants that acknowledged, durable (rev 4) |
| +@@ -1086,6 +1087,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 |
| @@ -8123,16 +8257,17 @@ diff $TMPDIR/twobox/baseline-counters.json <(grep COUNTERS $TMPDIR/twobox/task5c |
| 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' |
| +nice -n 19 go test ./internal/sim/hostlife/ -run '^TestConvertedMovePinsBeforeAcknowledgement$' -count=1 2>&1 | tail -1 |
| 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`. |
| +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), `ok` for the converted move, `--- 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 |
| +git commit -m "sim: Astra's rounds 2 and 3 on the two-box model: an initial failover's target acknowledges before its pin is selected (PinFailover), while converted moves, nested failovers and replays pin first, 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>" |
| ``` |
| @@ -8150,7 +8285,7 @@ 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..37267d6 100644 |
| +index 72504e3..b6fc701 100644 |
| --- a/internal/sim/hostlife/expected-outcomes.txt |
| +++ b/internal/sim/hostlife/expected-outcomes.txt |
| @@ -21,3 +21,25 @@ admit-bind-op missed caught with claim-cas-opid: the model's general CAS conditi |
| @@ -8178,7 +8313,7 @@ index 72504e3..37267d6 100644 |
| +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 |
| ++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 |
| diff --git a/internal/sim/hostlife/mutate.sh b/internal/sim/hostlife/mutate.sh |
| index c583d97..883996e 100755 |
| --- a/internal/sim/hostlife/mutate.sh |
| @@ -8341,7 +8476,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 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`). |
| +- the plan that built it, `docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md` rev 6 (its rulings 1 to 25, ruling 4 as revs 5 and 6 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`). |
| ## Fixed: do not re-argue |
| @@ -8401,7 +8536,7 @@ prompt (branch `region-ha-hostlife-two-box`) against plan 1b-next rev |
| | files-live-set-moves-parks | claim §6.2a over moves' parks | model F4 (rev 4) | L13 | witness INV-3 | |
| | reloc-clear-after-cleanup | `Finish` after a successful scoped cleanup (ruling 20) | R4-5, claim §11 | §5.10 | witness INV-29 | |
| | fence-converts-committed-landing | none: model F5 (rev 4) | claim §11 (the record-commit race) | §5.9, moves §7.10 | witness INV-3 | |
| -| reloc-failover-ack-before-pin | `PinFailover`'s `requireAcks` | two-box R2 #1 | D6, §5.8 | expected miss (loss bound); `TestFailoverPinWaitsForTheAcknowledgement` | |
| +| 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` | |
| ## Findings F1 to F3, closed, and the open window L21 |
| @@ -8432,7 +8567,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. |
| -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? |
| +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`? |
| 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 |