carlos / platform Public

docs: two-box model plan rev 4, Astra round 1: one-box create path restored with trace identity tests, Task 5B for the guards, exact phase matrix and claim §11's remaining witnesses, dispositions and coverage tables

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

claude 2 weeks ago 13f56f1016a27bb703d37320286af193b7b8b623 parent 54fa0c5

1 file changed, +2101 −216

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

CI cancelled — superseded by a newer push — run details

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 37f66a9e5..87d3ae063 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,78 @@

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

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

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

-**Tech Stack:** Go 1.26 test files, standard library only (the model imports nothing else; `hash/fnv` for the tie-break stand-in). `go test ./internal/sim/hostlife/` is the gate; `mutate.sh` runs the prebuilt binary per rule.

+**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 4: round 1 dispositions

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

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

+| 1 (P1) | The trace Astra describes was reproduced: a create's record persists, its box stops, and recovery runs past its 15-step wait. The baseline waits for the region's box. Rev 3's Task 1 cancelled the incarnation. Aggregate COUNTERS did not show it. | accepted | `createExecutor` is today's region-wide pick when `perRegion == 1`, and the recovered-create cancellation runs only in the two-box shape. Task 1 Step 1 adds `onebox_identity_test.go`, built from baseline APIs only, before any change. `TestOneBoxCreateInterruptionTrace` writes the whole trace of that interruption, once with the box restarted and once replaced. `TestOneBoxSeedTraces` writes a SHA-256 per one-box seed of its full trace, with map-ordered state masked. Every task compares both files byte for byte with the baseline's. | Task 1 (Steps 1, 4, 6); Global Constraints | rev 3's Task 1 code: `TestOneBoxCreateInterruptionTrace` differs at "recovery: cancelled create" |

+| 3 (P2) | `chooseBoxExcept` returned a region's only box unchecked. | accepted | The shortcut is the one-box shape's alone. With region HA on, a single candidate is checked for enrollment, key, executable, `lost` and `park-local`. Rule `ha-sole-box-eligibility`. | Task 5B | `TestHASoleBoxIsCheckedLikeAnyOther` (five refusals; the one-box shape keeps today's pick) |

+| 4 (P2) | The barrier read current leases (`leasesSeen`), and `installed` and `probing` had none. | accepted | Durable acknowledgements are `opState.Acks` (`exec_ack.<box>`). A participant whose controller is ready (lease current) journals its acknowledgement in `role` (`recordAck`). `acked` is `requireAcks` and gates `starting`→`releasing`, `releasing`→`pinning`, `pinning`→`installing`, `installing`→`installed` and `installed`→`probing`. Controller readiness stays the participant's own check. A controller now renews its lease on its own clock in the two-box step (`renewController`), not only when the worker happens to run. | Task 5B | `TestReplacementWithoutAcknowledgementHoldsEachTransition` |

+| 5 (P2) | The pin delay was skipped after a release, and the dead-target deadline ran from the termination. | accepted | The first worker to see a terminated box writes the fence record (`box.FenceObservedAt`). The fence CAS retains every `observed_at` in `opState.Observed`. The pin waits on the newest of them, release or not (rule `reloc-pin-delay-every-fence`). `FenceTargetWithoutSpare`'s deadline runs from `observed_at` (rule `reloc-deadline-from-observed-at`). | Task 5B | `TestPinWaitsForEveryFenceObservation`; `TestDeadTargetDeadlineFromObservation` (observation delayed past the deadline) |

+| 6 (P2) | `relocPhase` accepted later phases, the matrix had no `probe-failed`, and it added spares first. | accepted | `stepUntil` advances one actor transition at a time and stops the moment its condition holds. `TestL18TerminationAtEveryExactPhase` stops exactly in each of the nine phases, `probe-failed` included, and asserts the phase and region 0's live-box count immediately before the termination. No spare is added; replacements come from the modelled group after the loss. It has 24 subtests over the one-box and two-box regions and the source and target roles, and replaces `TestL18TerminationInEveryRelocationPhase`. | Task 5B | (coverage) |

+| 7 (P2) | Five guards had no discriminating test. | accepted | A direct test for each, failing under its mutation. `TestOnlyTheExecutorWritesP` runs only the source at `installing`. `TestInstallAppliesThePinnedManifest` lands the newer manifest between pin and install. `TestFailoverPinWaitsOutTheDelay` and `TestPinWaitsForEveryFenceObservation` assert before the delay passes. `TestReplacementWithoutAcknowledgementHoldsEachTransition` covers the barrier. `TestPinNeverShortOfTheRelease` hides the release's newest file. | Task 5B | each fails under its rule's mutation (Step 2) |

+| 8 (P2) | Claim §11 lists eight additional witnesses for the executable model, and rev 3 had four. | accepted | Model events and witnesses for the missing four, with file objects and admission trimming modelled far enough to exercise R11-1 (below). The host-dependent tie-break is real SHA-256 over the host (`tieHashFor`, rule `tie-hash-host`, `TestTieHashFollowsTheHost`). | Task 5B; the evidence map below | witnesses below |

+**Claim §11's additional witnesses, each in this model now** (claim rev 6.30 §11: "The additional witnesses are: …").

+| Claim §11 text | Model evidence | Rule whose mutation it catches |

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

+| "Relocation start racing purge or app-placement admission closure." | `TestRelocationStartRacesPurge` | (behaviour; ruling 4 of 1b-next) |

+| "Empty-database drain with files and timers." | `TestEmptyDatabaseDrain` | |

+| "Generation parking while relocation pins referenced files." | witness `files-live-set`; witness `files-origins-referenced` (`wOriginsAfterTrim`) | `files-live-set`, `files-origins-referenced` |

+| "Move landing, source cleanup, then target failure with an unchanged file." | witness `files-objects-region-bound` (`wMoveUnchangedFile`). The landing writes its generation's prepared manifest (moves §7.6, L17) in the target region. The unchanged file is uploaded there before it is named. The source region is cleaned, and the target's failover pins the object. | `files-objects-region-bound` |

+| "Automatic target loss racing the record commit CAS." | `TestAutomaticTargetLossRacesRecordCommit` covers both orders: the regional worker's automatic fence takes the operator's record-first path (`declareTargetLost`). Witness `fence-converts-committed-landing` (`wCommittedLandingTargetLost`) covers the after-commit order (finding F5). | `fence-converts-committed-landing` |

+| "A failed cleanup leaving a controller record that blocks executable updates." | witness `reloc-clear-after-cleanup` (`wClearAfterCleanup`). New model state: the controller record (`execRecord`), the scoped cleanup in `finishParticipation`, and executable updates refused while a record exists (`updateExecutable`, drawn in the two-box sweep). New oracle INV-29. | `reloc-clear-after-cleanup` |

+| "First `released` admission followed by an uncertified failed probe." | `TestReleasedThenFailedProbe` | `reloc-released-coverage` (witness) |

+| "Crash between prepared admission, marker publication and replication opening." | `TestCrashAtEachOpenBoundary` crashes the target exactly with P's session at the app start (launch environment held), with generation.json's PUT in flight (held), and with replication open, in both region shapes. | (coverage) |

+**Files objects (for R11-1 and the unchanged file).** A files directory now names the object that holds its content (`filesDir.Obj`, `ObjRegion`). The generation that first holds the content writes the object create-only and acknowledges it before any manifest names it. An unchanged file keeps naming an older generation's object. A host from another region uploads its objects again first (region binding). The pin checks that the named object is current in this region's bucket under the holder's location. The files live set keeps every object a live manifest or a live files directory names. `hasFilesIn` and the sweep treat objects as files, never as database objects.

+**New findings** (none contradicts the claim or moves; each is a gap the joint round must place):

+- **F4. Moves' parks archive region HA's files tree.** A push parks its whole location before installing. The same is true of a landing's install park and a rollback's return park. None of them excludes the files live set, so a later failover cannot pin the host's files. The model keeps the live set in those three parks (rule `files-live-set-moves-parks`, witness `wPushKeepsLiveFiles`; plan ruling 21). Claim §6.2a's live set should bind moves' parks explicitly.

+- **F5. A landing committed by its record whose target is then terminated has no owner.** The record forbids a rollback, the dead target can never release, and neither moves §7.10 nor 1b-next consumes a fence for a landing. The model converts it to a failover in the target's region (rule `fence-converts-committed-landing`; plan ruling 20). Before the commit, the automatic fence takes the operator's record-first rollback, as claim D2 makes automatic termination equivalent to a declared loss.

+- **F6 (model only).** 1b-next's `FenceSource` after the source's release leaves the source `op.exec` on `lost` until `PinAfterRelease`, transiently. INV-27 now allows exactly that: a released executor (plan ruling 24).

+**Past findings, and where their evidence lives.** Claim §11 asks for the cases above in the executable model. Separately, it requires "targeted tests against the real `hostclaim`, `park`, `stopevidence`, `hostfiles` and `hostexec` boundaries; model results do not replace those adapter tests." Each 1b-next finding the model cannot represent is therefore proven by a 1b-next stage A artifact, which this plan does not duplicate:

+| Findings | What they are about | Proven by (1b-next rev 19) |

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

+| R1-2 | the pin selected and journaled under the location lease; a lease lost before the CAS | Task 5 `TestWorkerRefusesToJournalAPinAfterTheLeaseIsLost`, `TestWorkerDrivesADrain`; Task 8b `TestRelocationBuildStopsWhenAuthorityChanges` |

+| R1-4, R2-4 | durable automatic-loss evidence (`evidence_refs`) across replacement and completion | Task 1 `TestRelocationRetainsEveryFencedBoxAcrossCompletion`, `TestRelocationLossRetainsAFormerWritersSession` |

+| R2-7 | discovery completion when a discharge completes the final local chore | Task 1 `TestRelocationDischargeCompletesDiscoveryLikeARetirement` |

+| R11-1 | origins from referenced objects after admission trimming | Task 5 `TestPinKeepsAFileOriginTheAdmissionListTrimmed`, and this model's witness `files-origins-referenced` |

+| R2-5, R3-2, R4-5, R5-4, R12-1, R13-1, R13-2, R14-2, R15-2, R18-1 | controller lifecycle: cleanup failures, lifetime locks, durable participation, removal during an ongoing operation | Task 7 `TestRelocationControllerLifecycleProperties` (200 seeds, invariants (a) to (i)) and its named tests. The model keeps only claim §11's case, a failed cleanup keeping the update-blocking record (witness `reloc-clear-after-cleanup`). |

+| R18-2 | host-dependent hash selection | Task 2 `TestExecutorChooserHashesTheRecordsHostOnEqualLoads`, and this model's `TestTieHashFollowsTheHost` |

+| R1-1, R3-1, R3-3, R4-N1 to N3, R6-1, R7-1, R8-2, R9-1, R10-1, R12-2, R14-3 | compilation, adapters, privileges, kernel descriptors, production wiring | the production-boundary tests each disposition names (Tasks 2, 3, 4, 7, 9a, 10) |

+**Dry run (2026-10-08).** The scratch module was built from the baseline. The identity tests were added and the baseline's two trace files recorded. Task 1 was applied from its prose, and the patches for Tasks 2 to 6 from this document, one at a time. After each task: build, vet, gofmt, the gate, and both trace files compared byte for byte with the baseline's.

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

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

## Rev 3: sync to 1b-next rev 19

Rev 2 reported three gaps in 1b-next rev 16 (F1 to F3). 1b-next fixed them in rev 17, tightened the fixes in rev 18 (Astra's round 17 found each only partly closed), and Astra accepted rev 19 as "stage A ready to build" (round 18 raised test gaps only). Rev 3 replaces the model's own stand-ins for F1 to F3 (rev 2's rulings 14, 16 and 17) with mirrors of 1b-next's fixes, turns the three finding tests into evidence that the gaps are closed, adds a mutation check that reopens each gap, and models the open request L21 as an explicit window. Everything is in one new task, **Task 5A**, a patch on Task 5's tree; Task 6's patch is regenerated on top of it (one more `expected-outcomes.txt` line). Tasks 1 to 5 are unchanged.

@@ -105,9 +168,9 @@ 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.

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

-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. *Cost if wrong:* a seed reshuffle, which the gate shows at once; the fix is to move the draw.

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

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

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

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

@@ -121,15 +184,21 @@ Each was a gap or a conflict between the authorities. Each says what it costs if

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

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

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

-15. **Termination is drawn only where region HA owns the loss.** The sweep terminates a box only when the claim names it, if at all, as a serving executor, a relocation's participant or a chore's owner, and never a box holding a legacy host before its adoption. A participant of a move, landing, rollback, revert, push, create or delete is recovered from a lost box by moves' and the claim's declare-lost paths (L14), which the model walks for a stopped box, and a push never starts on a terminated executor. *Cost if wrong:* those paths are untested under termination here; the brief lists it under "After this plan".

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

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

17. **(Rev 3) A nonempty database pins only files that carry `instance.key`, mirroring 1b-next ruling 25 as rev 18 amended it, and the L21 window fails safe** (finding F2, closed). In the two-box shape, a pin for a holder with an admitted writer and a nonempty pinned database needs a pinned manifest that carries a live `instance.key`. With no manifest, or a keyless one (the pre-start copy of §5.6), the operation is stuck (rule `files-pin-needs-key`), and no operator replay accepts a keyless pin. The window between the app minting the key and the first keyed manifest landing is L21, still open. A host terminated inside it cannot be recovered by any relocation, so the sweep, which must converge, never terminates such an executor (`regionHAOwnsLoss`). The witness `files-pin-needs-key` and `TestFailoverBeforeTheFirstManifest` script the window. *Cost if wrong:* the sweep never meets the L21 refusal; the witness and the test do, and they fail if the refusal goes.

18. **A one-box region inside the two-box shape is a witness world's** (`regionWorld(1)`, `oneBoxRegion`): region HA on, region 0 kept at one box by its group (H5's minimum is per region), regions 1 and 2 with two. The sweep's one-box shape has region HA off, so L18's one-box cases are direct tests, not seeds. *Cost if wrong:* a one-box-region interleaving the scenarios do not script is unexplored; the joint round may ask for a mixed sweep shape.

19. **INV-28 is new: a timer is never declared lost while the manifest its box published last in that generation carries it.** It is the oracle for P's prepared manifest at sequence 0 (the seq order must be the publication order); it reads the issue order the model records in each manifest blob. *Cost if wrong:* a manifest landing out of order with a timer added and then removed would be a false positive; the timer would be delivered, and delivered timers are never declared.

+20. **(Rev 4) A landing committed by its record whose target is then terminated converts to a failover in the target's region** (finding F5; rule `fence-converts-committed-landing`). The record forbids moves' rollback, and the dead target can never release, so without the conversion the host has no recovery owner. The conversion enters at `pinning` like moves' §7.10 conversion of a move, with the source region's chores left to the region and the landing's prepared manifest as the files pin. *Cost if wrong:* moves or 1b-next may prefer another owner; the model's guard is one branch in `fence`.

+21. **(Rev 4) Moves' parks keep region HA's files live set** (finding F4; rule `files-live-set-moves-parks`). A push's park, a landing's install park and a rollback's return park park the whole location today, which archives the objects a later failover pins. The model passes the live set to all three as it does to `park-generation`. *Cost if wrong:* claim §6.2a may bind the live set to a different step; the witness shows the loss either way.

+22. **(Rev 4) A controller renews its own execution lease.** 1b-next's controller is a long-running process; in rev 3 the model renewed a lease only when the box's worker ran a role, which let a calm box's lease lapse and churned durable acknowledgements. `renewController` runs per box in the two-box step and draws nothing. *Cost if wrong:* none to safety; acknowledgements are still journaled only while the lease is current.

+23. **(Rev 4) The injected app failure never applies to a relocation's own source, and the operator's replay keeps a failed target excluded.** The source has just run the app; a probe on it failing at random made a ping-pong between two failing boxes that no protocol produces. The replay's exclusion is plan ruling 13's, now kept for the target that failed. *Cost if wrong:* a source whose app genuinely fails is not modelled; the operator's resolve is its path.

+24. **(Rev 4) INV-27 allows a released executor that has been fenced** (F6, model only). 1b-next's `FenceSource` after the source's release leaves `op.exec` on the lost box until `PinAfterRelease`; nothing runs there. *Cost if wrong:* a write from a lost, released executor would go unseen by INV-27; INV-1 and INV-2 still see it.

+25. **(Rev 4) Files are objects, referenced by manifests and files directories** (R11-1; rules `files-origins-referenced`, `files-objects-region-bound`). Rev 3 carried files as manifest content, so trimming an admission could not drop an origin. Rev 4 models the object key, its creation before it is named, its region, the live set over referenced objects and origins taken from references, never from admissions. *Cost if wrong:* the object store's semantics beyond create-once and region are not modelled; `hostfiles`' adapter tests own them (claim §11).

## Global Constraints

-- **One-box byte-identical.** After every task: `nice -n 19 go test ./internal/sim/hostlife/ -run '^TestHostLifecycle$' -count=1 -v | grep COUNTERS` equals the baseline's line (Task 1 Step 1 records it at `$TMPDIR/twobox/baseline-counters.json`; the task that breaks it stops and moves its draw).

+- **One-box byte-identical.** After every task: `nice -n 19 go test ./internal/sim/hostlife/ -run '^TestHostLifecycle$' -count=1 -v | grep COUNTERS` equals the baseline's line (Task 1 Step 1 records it at `$TMPDIR/twobox/baseline-counters.json`; the task that breaks it stops and moves its draw). **(Rev 4)** And both one-box traces equal the baseline's byte for byte: `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`, then `cmp` each with `baseline-trace.txt` and `baseline-seeds.txt`. COUNTERS alone missed rev 3's one-box change (Astra round 1 finding 1).

- **Additive.** Moves and the claim own guards in this model. No existing rule's semantics change; existing functions gain branches or calls that only a relocation, a termination or the two-box shape reaches. New code lives in new files (`twobox_test.go`, `regionha_test.go`, `regionha_witness_test.go`, `regionha_cases_test.go`) except where a hook must sit in an existing function.

- **Every rule is a named guard**: an entry in `allRules`, in the region HA block, with a comment naming the spec section and the 1b-next rev 16 function it mirrors, `on("<rule>")` at exactly the decision the rule governs, and either a witness in `witness_test.go` or an `expected-outcomes.txt` line with its reason and the direct test that shows its effect.

- **Witness discipline (moves §14.2, rev 7.3):** a witness holds with every rule on, holds under every proper subset of its mutation set, and violates its named failure under the whole set. `TestWitnesses` checks all three in the gate. Liveness and preference guards get direct tests (`TestXxx`), never witnesses.

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

- **Go environment.** `GOFLAGS=-buildvcs=false`. Leave `GOCACHE` at its default; the sandbox refused it intermittently during the rev 2 dry run (`open /home/paulca/.cache/go-build/...: read-only file system`), in which case `GOCACHE=$TMPDIR/gocache` for that command. Scratch under `$TMPDIR/twobox/`, removed at the end of Task 7.

- **Exact values.** `failoverPinDelay = 2` steps (§5.8's 30 seconds; one step is about 20 seconds, since `sigAgeH = 45` steps is the 15-minute signature age); `probeDeadline = 3*probeStartWindow + 10` (three attempts' windows); `releaseDeadline = probeDeadline` (1b-next's 10 minutes, the same as its probe deadline); `maxReplacements = 2`; `probeTries = 3` attempts per executor; `enrollDelay = 20` steps (automatic enrollment, H16); `replaceDelay = 30` steps (the group's replacement launch); second boxes have ids `nRegions + r`; manifests live at `dataKey(loc, gen, "files/m-<seq>")`, P's prepared manifest at seq 0.

- **Commit messages:** lowercase `sim:` prefix and a sentence stating the behaviour, a blank line, then `Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>`. Branch `region-ha-hostlife-two-box` (this worktree). No push; merging is Paul's call after the joint round.

-- **Gate before each commit:** `gofmt -l internal/sim/hostlife/` empty; `go vet ./internal/sim/hostlife/`; the gate above; the one-box COUNTERS comparison.

+- **Gate before each commit:** `gofmt -l internal/sim/hostlife/` empty; `go vet ./internal/sim/hostlife/`; the gate above; the one-box COUNTERS and trace comparisons.

## Review Focus

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

3. **The exhausted fence while the source still executes.** Three targets die in `starting`; the source must keep `op.exec`, its phase and its release, and only `stuck` is new. Expect no second writer. Task 3 `fenceExhaustedTarget`; Task 5 witness `reloc-exhausted-fence`.

4. **P's prepared manifest sequence.** The session publisher in P must sort after the prepared manifest, or a later pin takes stale files and timers. Expect seq 0 and INV-28 to hold. Task 4 `buildPreparedFiles`; Task 5 witness `files-prepared-seq-zero`.

5. **The three findings, closed (rev 3).** F1, F2 and F3 are now mirrors of 1b-next rev 19's fixes, each with a mutation that reopens it. The L21 window is scripted (witness `files-pin-needs-key`): recovery must be stuck there and must never install a database without its key. Tell us if a mirror is weaker than its 1b-next guard.

+6. **(Rev 4) The one-box shape's create, and Astra round 1's guards.** The trace comparison must show no one-box change after any task; the five guards round 1 named must each have a test that fails without them. Task 1 Step 1 and Step 6; Task 5B Step 2.

## File Structure

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

| `internal/sim/hostlife/background_test.go` | `adopt` uses `adoptionOwner`; `replaceDestroyed` fills to the region's minimum; `reconcileClaimed`'s relocation row case | 1, 2, 5 |

| `internal/sim/hostlife/moves_test.go` | `workerMode` uses `ownsObligation` and runs the fence step first; `role`'s scoped cleanup on a lost lease; `relocate` dispatches the phases; `convertToRelocating` sets the failover fields; `release` queues the leftovers; `genOf` and `deadGeneration` know manifests and the files live set | 1 to 4 |

| `internal/sim/hostlife/protocol_test.go` | `admits` for the new phases; `admitWriter`'s `released` coverage; `admitCommit` journals `prepared_opened`; `installGen` for P; `appStart`'s `FailApp` for relocation probes; `localPark` drops the install journal; `hasFilesIn` skips manifests; `doObligation`'s `park-generation` keep for the files live set | 2, 4, 5 |

-| `internal/sim/hostlife/rules_test.go` | The 33 region HA rules, in one block at the end | 1 to 4 |

+| `internal/sim/hostlife/rules_test.go` | The 47 region HA rules, in one block at the end | 1 to 5B |

+| `internal/sim/hostlife/onebox_identity_test.go` | (Rev 4) The one-box create-interruption trace and the per-seed trace hashes, compared with the baseline's after every task | 1 |

+| `internal/sim/hostlife/regionha_round1_test.go` | (Rev 4) Astra round 1's direct tests: one per guard it named, the forced open boundaries, the record-commit race, the host tie-break | 5B |

| `internal/sim/hostlife/expected-outcomes.txt` | The `missed` entries, each with its reason and its direct test | 6 |

| `internal/sim/hostlife/mutate.sh` | The shape tag on every verdict, `@regionha`, `HOSTLIFE_LIST` | 6 |

| `docs/superpowers/plans/CODEX-REVIEW-BRIEF-TWO-BOX-R1.md` | The joint-round brief | 7 |

@@ -185,7 +257,7 @@ Every task was dry-run in order on this baseline (see "Rev 2: sync to 1b-next re

### Task 1: The world's shape, one or two boxes per region (L18; spec §2, §4, §5.2, H5, H12, L8, L15)

-Dry-run on the baseline in rev 1 and again in rev 2, with the same results; its code is unchanged from rev 1, and the later tasks' patches assume exactly this tree. The model gains a shape, `boxesPerRegion`, read from `HOSTLIFE_BOXES` and set by `TestHostLifecycleTwoBox`; a second enrolled box per region in the two-box shape, drawn after every one-box draw; `chooseBox`, spec §5.2's `choose()`, used by a create (recorded once in the intent, rule `create-choice-once`) and a move's start (L15); `adoptionOwner` (P5-D2's one proven owner); regional chores owned by any live box of the region; replacements launched up to the region's minimum (H5).

+Dry-run on the baseline in rev 1 and again in revs 2 to 4. Rev 4 adds the identity tests (Step 1) and keeps `createExecutor` and the recovered-create cancellation out of the one-box shape (Astra round 1 finding 1); otherwise its code is rev 1's, and the later tasks' patches assume exactly this tree. The model gains a shape, `boxesPerRegion`, read from `HOSTLIFE_BOXES` and set by `TestHostLifecycleTwoBox`; a second enrolled box per region in the two-box shape, drawn after every one-box draw; `chooseBox`, spec §5.2's `choose()`, used by a create (recorded once in the intent, rule `create-choice-once`) and a move's start (L15); `adoptionOwner` (P5-D2's one proven owner); regional chores owned by any live box of the region; replacements launched up to the region's minimum (H5).

**Files:**

- Create: `internal/sim/hostlife/twobox_test.go`

@@ -205,6 +277,92 @@ grep COUNTERS $TMPDIR/twobox/baseline.log | sed 's/.*COUNTERS //' > $TMPDIR/twob

Expected: `300 seeds, 0 failed, 483 completed operations; mutated=""` and `ok`. If the numbers differ from the Baseline section, the tree is not fbdad381's model: stop and say so.

+**(Rev 4)** Then, before any code change, add the one-box identity tests. They use only the baseline's APIs, so they compile against fbdad381. Record their traces.

+Create `internal/sim/hostlife/onebox_identity_test.go`:

+```go

+package hostlife

+import (

+ "crypto/sha256"

+ "fmt"

+ "os"

+ "regexp"

+ "strings"

+ "testing"

+// TestOneBoxCreateInterruptionTrace is a deterministic trace of the

+// interruptions a one-box create recovers from (two-box plan rev 4,

+// Astra round 1 finding 1): the create's record persists, then its

+// selected box stops, then recovery runs for longer than its 15-step

+// wait; the box starts again (stopped) or the region's group replaces

+// it (destroyed). It writes the whole trace to $HOSTLIFE_TRACE_OUT when

+// set, so the trace at the baseline and after each task can be compared

+// byte for byte; the one-box shape must not change it.

+func TestOneBoxCreateInterruptionTrace(t *testing.T) {

+ var out []string

+ for _, how := range []string{"restarted", "replaced"} {

+ w := newWitness()

+ w.console = append(w.console, &consolePlan{Kind: "create", Host: "h", App: app0, OpID: w.newID("cr"), Inc: 1, Region: 0})

+ w.admit[app0].Reg[w.console[0].OpID] = regEntry{Until: w.now + 1000}

+ w.drive(60, func() bool { return w.rec != nil && w.claim != nil && w.claim.Op.Kind == "creating" }, w.runConsole)

+ b := w.boxes[0]

+ b.Destroyed, b.Procs = true, nil

+ w.logf("trace: box %d stopped after the record persisted", b.ID)

+ w.drive(40, func() bool { return false }, w.runConsole, w.recoveryPass)

+ if how == "restarted" {

+ b.Destroyed = false

+ b.forget()

+ } else {

+ w.replaceDestroyed()

+ }

+ w.logf("trace: box %s", how)

+ w.drive(200, func() bool { return w.claim != nil && w.claim.Op.Kind == "serving" }, w.runConsole, w.recoveryPass, w.actAll())

+ out = append(out, "== "+how)

+ out = append(out, w.trace...)

+ c := w.claim

+ out = append(out, fmt.Sprintf("final: op=%s/%s exec=%d holder=%+v rec=%+v lost=%v obl=%d", c.Op.Kind, c.Op.ID, c.Op.Exec, c.Holder, w.rec, c.Lost, len(c.Obl)))

+ }

+ if p := os.Getenv("HOSTLIFE_TRACE_OUT"); p != "" {

+ if err := os.WriteFile(p, []byte(strings.Join(out, "\n")+"\n"), 0o644); err != nil {

+ t.Fatal(err)

+ }

+// TestOneBoxSeedTraces writes one line per seed of the one-box sweep,

+// the SHA-256 of its whole trace, to $HOSTLIFE_TRACE_OUT_SEEDS (and is

+// skipped without it): the per-seed evidence that a task leaves every

+// one-box trace as the baseline's, beyond the aggregate COUNTERS line.

+// Map-ordered fields in state dumps are masked.

+func TestOneBoxSeedTraces(t *testing.T) {

+ p := os.Getenv("HOSTLIFE_TRACE_OUT_SEEDS")

+ if p == "" {

+ t.Skip("HOSTLIFE_TRACE_OUT_SEEDS is not set")

+ }

+ mask := regexp.MustCompile(`admission=\[[^\]]*\]`)

+ var out []string

+ for seed := int64(0); seed < int64(seedsFromEnv(300)); seed++ {

+ w := runSeed(seed, true)

+ sum := sha256.Sum256([]byte(mask.ReplaceAllString(strings.Join(w.trace, "\n"), "admission=[masked]")))

+ out = append(out, fmt.Sprintf("%d %x %d", seed, sum[:8], len(w.trace)))

+ }

+ if err := os.WriteFile(p, []byte(strings.Join(out, "\n")+"\n"), 0o644); err != nil {

+ t.Fatal(err)

+ }

+```

+```bash

+nice -n 19 go test ./internal/sim/hostlife/ -run '^TestOneBox' -count=1 2>&1 | tail -1

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

+wc -l $TMPDIR/twobox/baseline-trace.txt $TMPDIR/twobox/baseline-seeds.txt

+```

+Expected: `ok`; 300 lines in `baseline-seeds.txt`. The interruption trace has both cases, and at the baseline each ends `final: op=serving/...`, the create recovered on the region's box.

- [ ] **Step 2: Create `twobox_test.go`**

```go

@@ -470,6 +628,9 @@ Before `moveTo`, add:

// The mutation of create-choice-once chooses again, as rev 7.22's

// region-wide pick did.

func (w *world) createExecutor(c *claim) *box {

+ if w.perRegion <= 1 {

+ return w.regionBox(c.Op.NewRegion) // the one-box shape: today's region-wide pick, unchanged (spec §4; rev 4, Astra R1-1)

+ }

if !on("create-choice-once") {

return w.chooseBox(c.Op.NewRegion, c.Holder.App)

}

@@ -492,9 +653,11 @@ In `recoveryPass`, case `"creating"`, replace the four lines from `b := w.region

```go

b := w.createExecutor(c)

if b == nil {

- if nb := w.boxByID(c.Op.NewBox); on("create-choice-once") && (nb == nil || nb.Destroyed) {

- // the chosen box cannot complete the create: recovery

- // cancels it (claim §5.1 step 5, P5-D6), retiring the

+ if nb := w.boxByID(c.Op.NewBox); w.perRegion > 1 && on("create-choice-once") && (nb == nil || nb.Destroyed) {

+ // the chosen box cannot complete the create (the two-box

+ // shape only; the one-box shape waits for its region's

+ // box, as the baseline does): recovery cancels it (claim

+ // §5.1 step 5, P5-D6), retiring the

// incarnation; the record is an orphan the cleanup removes

inc, app, id := c.Holder.Inc, c.Holder.App, c.Op.ID

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

@@ -544,9 +707,11 @@ Expected: gofmt prints nothing; two summary lines, `300 seeds, 0 failed, 483 com

```bash

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

grep COUNTERS $TMPDIR/twobox/task1.log | sed -n 2p | sed 's/.*COUNTERS //' > $TMPDIR/twobox/twobox-counters-task1.json

+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

```

-Expected: `ONE-BOX-COUNTERS-IDENTICAL`. If `diff` prints anything, a one-box path drew where it did not before: find the draw (`git diff` shows every call site) and move it under `w.perRegion > 1`.

+Expected: `ONE-BOX-COUNTERS-IDENTICAL` and `ONE-BOX-TRACES-IDENTICAL`. If `diff` prints anything, a one-box path drew where it did not before: find the draw (`git diff` shows every call site) and move it under `w.perRegion > 1`. If only a trace differs, a one-box path behaves differently with the same draws. Rev 3's `createExecutor` and recovered-create cancellation did that (Astra round 1 finding 1), so both are now the two-box shape's alone.

- [ ] **Step 7: Commit**

@@ -5832,212 +5997,1916 @@ 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 37 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 16 region HA rules that are not caught alone, each with its reason and the direct test that shows it.

+### Task 5B: Astra's round 1: the guards made faithful and discriminated, the exact phase matrix, and claim §11's remaining witnesses (rev 4)

+This task holds every rev 4 change except Task 1's identity fix. It is described in "Rev 4: round 1 dispositions" above. In short:

+- stuck refuses admission;

+- the sole box is checked in an HA region;

+- durable acknowledgements gate every transition, and controllers renew on their own clock;

+- fence observations are retained, and deadlines run from `observed_at`;

+- `stepUntil` and the exact phase matrix replace the old phase test;

+- five discriminating direct tests;

+- files objects, with origins and region binding;

+- moves' parks keep the files live set (F4);

+- the automatic target fence takes the record-first path, and a committed landing whose target is lost converts to a failover (F5);

+- the relocation controller record, executable updates and INV-29;

+- the forced open boundaries;

+- `tieHashFor` over the real host.

+Two model refinements came from the dry run. The injected `FailApp` fault no longer applies to a relocation's own source, which has just run the app. The operator's replay after a failed probe does not name that same target again.

+| Rule (new) | 1b-next / claim | Evidence |

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

+| `reloc-stuck-refuses-admission` | `relocationAdmission`'s stuck check (ruling 9, R1-16) | `TestStuckSourceRefusesAdmission` (expected miss in the sweep) |

+| `ha-sole-box-eligibility` | spec §2 eligibility with region HA on | `TestHASoleBoxIsCheckedLikeAnyOther` |

+| `reloc-pin-delay-every-fence` | `JournalPin` over every `fence.<box>.observed_at` | `TestPinWaitsForEveryFenceObservation` |

+| `reloc-deadline-from-observed-at` | `FenceTargetWithoutSpare` from `observed_at` | `TestDeadTargetDeadlineFromObservation` |

+| `tie-hash-host` | claim P5-D2, R18-2 | `TestTieHashFollowsTheHost` |

+| `files-origins-referenced` | `filesPin`'s `referencedOrigins` (R11-1) | witness INV-3 |

+| `files-objects-region-bound` | §5.6, the pin's region binding; claim §11's move case | witness INV-3 |

+| `files-live-set-moves-parks` | claim §6.2a over moves' parks (F4) | witness INV-3 |

+| `reloc-clear-after-cleanup` | `Finish` after a successful scoped cleanup (ruling 20, R4-5); claim §5.10 | witness INV-29 |

+| `fence-converts-committed-landing` | finding F5; claim §11's record-commit race | witness INV-3 |

**Files:**

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

+- Create: `internal/sim/hostlife/regionha_round1_test.go`

+- Modify:

+ - `regionha_test.go`: `acked`, `recordAck`, `finishParticipation`, `updateExecutable`, `latestObservation`, `observedAt`, `renewController`, `keepFilesLive`, `preparedManifestHere`, the files objects (`objectKey`, `isFilesKey`, `objectCurrent`, `ensureObject`, `originAuthorized`, `objectReferenced`), the fence record in `fenceStep`, the committed-landing and automatic target fences in `fence`, and `twoBoxStep`

+ - `twobox_test.go`: `tieHashFor`, `chooseBoxFor`

+ - `world_test.go`: `opState.Acks`, `Observed`; `box.FenceObservedAt`, `execRecord`, `cleanupPending`, `cleanupFails`; `filesDir.Obj`, `ObjRegion`

+ - `moves_test.go`: `role` (finish, acknowledge); the three moves parks' keep; `installLocal`'s prepared manifest; `deadGeneration` for files keys

+ - `protocol_test.go`: the stuck refusal in `admits` and `admitWriter`; `appStart`'s `FailApp`; `hasFilesIn`

+ - `console_test.go`: `declareTargetLost`, factored out of `operator`; `h2Box` hashes `h2`; the operator's replay excludes the failed target

+ - `sim_test.go`: INV-27 allows a released executor

+ - `rules_test.go`

+ - `witness_test.go`: five entries

+ - `regionha_witness_test.go`: five witness functions

+ - `regionha_cases_test.go`: the superseded phase test removed

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

```diff

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

-index 72504e3..9e372fb

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

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

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

-+create-choice-once missed no box-side effect precedes the serving CAS in this model, so a substituted executor leaves nothing behind; the rule's effect is the cancellation of a create whose box is gone (TestCreateNamesItsExecutorOnce fails under the mutation)

-+reloc-start-guard missed the chooser's §2 eligibility already excludes a target owing a park-local, a live source never owes one for the host it serves, and a whole-location chore cannot be pending in the region the host serves in (a move into it waits, CC11); TestRelocationStartGuardRefuses shows the refusal

-+reloc-exec-ack-barrier missed liveness only: without the barrier a target that never acknowledged is handed op.exec and the operation waits there instead of in starting

-+reloc-pin-reaches-release missed the release's step 2 already waits for the listing to show N (relocRelease), so the pin's own check is never the first to see a short listing in this model; in the real pinner the listing is a separate read (JournalPin)

-+reloc-failover-pin-delay missed a loss bound, not a safety bound (§5.8): the pin names exact versions and a later PUT adds a version nothing reads; TestL18LatePutAfterTermination shows the late upload parked

-+reloc-exec-only-installs missed every installing CAS is conditional on op.exec, so a non-executor's build of P writes the same create-only objects and its local install is retired by its park-local; the guard keeps it from writing at all (HA2), which no invariant here observes; TestOnlyTheExecutorInstalls shows the property

-+reloc-install-receipt missed caught with reloc-ensure-local (witness): EnsureLocal restores a replacement's missing install whatever the receipt says, as 1b-next rev 14 found ("each covers the other")

-+reloc-row-cases missed caught with exec-admission and exec-writer (witness): a reopened stale row routes a request to a box the exec check and AdmitWriter refuse

-+reloc-replacement-cap missed an operator bound: without the cap the operation replaces its target a third time instead of waiting for carlos ops host resolve; TestStuckAfterTwoReplacements fails under the mutation

-+reloc-drain-needs-writer missed liveness only (1b-next ruling 11): a never-woken host's drain would wait for a release root refuses, until the release deadline; TestDrainRefusedForANeverWokenHost fails under the mutation

-+reloc-ack-before-pinning missed defence in depth (1b-next rev 4 N6): installing still waits for the barrier, so a replaced target that never acknowledged holds the operation at pinning instead of releasing; TestReplacedTargetAcknowledgesBeforePinning fails under the mutation

-+reloc-probe-attempts missed liveness only (ruling 19): uncounted attempts still end at the probe deadline; TestProbeAttemptsCountedBeforeTheyAreMade fails under the mutation

-+fence-terminated-only missed redundant alone: a stopped box fenced by mistake is on lost, so lost-quarantine retires its state and exec-admission refuses it when it starts again; TestStoppedBoxNeverFenced fails under the mutation

-+reloc-replacement-table missed after P's first admission the admission rules (recovery-generation, remote-baseline) already refuse reopening P, so resuming at installed with the same P admits a fresh generation from P's remote, as the nested failover does; TestL18NestedFailover fails under the mutation (no nested failover)

-+files-pin-exact missed a determinism rule (§5.8): a later manifest PUT adds a version nothing reads, and the fence declares what no landed manifest carries; TestL18LateFileUploads shows the pinned version applied

-+reloc-abandoned-prepared missed the at-rest sweep, which 1b-next ruling 27 keeps as the backstop, retires an unrecorded P before any invariant sees it; the operation's own park is the rule's effect, and TestAbandonedPreparedGenerationParked (both paths) fails under the mutation

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

-index c583d97..883996e

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

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

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

- # internal/sim/hostlife/mutate.sh 3000 # every rule

- # internal/sim/hostlife/mutate.sh 30000 rule-a rule-b # named rules

- # internal/sim/hostlife/mutate.sh 30000 rule-a,rule-b # a combination, dropped together

-+# HOSTLIFE_BOXES=2 internal/sim/hostlife/mutate.sh 3000 # the two-box shape (region HA L18); unset is one box per region

-+# HOSTLIFE_BOXES=2 internal/sim/hostlife/mutate.sh 3000 @regionha # the region HA rules alone (rules_test.go's region HA block)

-+# HOSTLIFE_LIST=1 internal/sim/hostlife/mutate.sh 0 @regionha # print the rules a run would check, and run nothing

- #

- # Each rule gets two runs under its mutation (rev 7.3): the random sweep

- # (TestHostLifecycle over the seeds) and the rule's deterministic witness

-@@ -50,6 +53,18 @@ ROOT=$(git -C "$(dirname "$0")" rev-parse --show-toplevel)

- PKG="$ROOT/internal/sim/hostlife"

- SCRATCH=${HOSTLIFE_SCRATCH:-${TMPDIR:?}/hostlife-sim}

- BIN=${HOSTLIFE_BIN:-$SCRATCH/hostlife.test}

-+SHAPE=${HOSTLIFE_BOXES:-1}

-+RULES="$*"

-+if [ -z "$RULES" ]; then

-+ RULES=$(sed -n '/^var allRules/,/^}/p' "$PKG/rules_test.go" | grep -o '^\s*"[a-z0-9-]*"' | tr -d ' "\t')

-+elif [ "$RULES" = "@regionha" ]; then

-+ # every rule of the region HA block: one mutation check per guard

-+ RULES=$(sed -n '/^\t\/\/ region HA (two boxes per region, L18)/,/^}/p' "$PKG/rules_test.go" | grep -o '^\s*"[a-z0-9-]*"' | tr -d ' "\t')

-+fi

-+if [ -n "${HOSTLIFE_LIST:-}" ]; then

-+ printf '%s\n' $RULES

-+ exit 0

-+fi

- mkdir -p "$SCRATCH/logs" "$SCRATCH/verdicts" || { echo "cannot create $SCRATCH" >&2; exit 2; }

- if [ ! -x "$BIN" ]; then

- echo "no test binary at $BIN; build it with: go test -c -o $BIN ./internal/sim/hostlife/" >&2

-@@ -59,10 +74,6 @@ if [ -n "$(find "$PKG" -name '*.go' -newer "$BIN")" ]; then

- echo "the test binary $BIN is older than the source; rebuild it" >&2

- exit 2

- fi

--RULES="$*"

--if [ -z "$RULES" ]; then

-- RULES=$(sed -n '/^var allRules/,/^}/p' "$PKG/rules_test.go" | grep -o '^\s*"[a-z0-9-]*"' | tr -d ' "\t')

--fi

- # the rules that have witnesses (witness_test.go): a run of one of them

- # with no witness output is an ERROR, never "none" (R3-6)

- WRULES=$(grep -o '^\s*{"[a-z0-9-]*",' "$PKG/witness_test.go" | tr -d ' \t{",' | sort -u)

-@@ -75,7 +86,7 @@ one() {

- verdict="$SCRATCH/verdicts/$tag"

- for x in $(echo "$r" | tr ',' ' '); do

- if ! sed -n '/^var allRules/,/^}/p' "$PKG/rules_test.go" | grep -q "^\s*\"$x\","; then

-- echo "ERROR $r: no rule named $x" | tee "$verdict"

-+ echo "ERROR $r [boxes=$SHAPE]: no rule named $x" | tee "$verdict"

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

+index 88980b1..1e7f99d

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

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

+@@ -387,7 +387,7 @@ func (w *world) userMove() {

+ // choose() in region 0, where the model keeps the control-plane-only

+ // host. With one box per region it is box 0, as the model always implied.

+ func (w *world) h2Box(app string) int {

+- if b := w.chooseBox(0, app); b != nil {

++ if b := w.chooseBoxFor("h2", 0, app); b != nil {

+ return b.ID

+ }

+ return 0

+@@ -1274,6 +1274,9 @@ func (w *world) operator() {

+ default:

+ w.abandonPrepared(n)

+ n.Op.Stuck, n.Op.Replacements, n.Op.Excluded, n.Op.Resolved = "", 0, nil, true

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

++ }

+ n.Op.Phase, n.Op.Exec, n.Op.Tgt = "pinning", -1, -1

+ n.Op.Pin, n.Op.Prepared, n.Op.Receipt = nil, "", nil

+ n.Op.BaseKey, n.Op.BaseVer, n.Op.BaseTX = "", 0, 0

+@@ -1326,6 +1329,15 @@ func (w *world) operator() {

return

- fi

- done

-@@ -108,19 +119,19 @@ one() {

- wit=held

- fi

- if [ $wrc -ne 0 ] || grep -q "^panic:\|test timed out" "$wlog"; then

-- echo "ERROR $r: witness run rc=$wrc; see $wlog" | tee "$verdict"

-+ echo "ERROR $r [boxes=$SHAPE]: witness run rc=$wrc; see $wlog" | tee "$verdict"

+ }

++ w.declareTargetLost(c)

++}

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

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

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

++// D2 "Automatic termination", rev 4). It proceeds record first, so a loss

++// racing the record's commit CAS follows whichever the record holds.

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

+ if c.Holder == nil {

return

- fi

- if [ "$wit" = none ]; then

- for x in $(echo "$r" | tr ',' ' '); do

- if echo "$WRULES" | grep -qx "$x"; then

-- echo "ERROR $r: $x has witnesses but the run produced no witness output; see $wlog" | tee "$verdict"

-+ echo "ERROR $r [boxes=$SHAPE]: $x has witnesses but the run produced no witness output; see $wlog" | tee "$verdict"

- return

- fi

- done

- fi

- if [ -z "$sweep" ]; then

-- echo "ERROR $r: rc=$rc, no parsable sweep verdict; see $log" | tee "$verdict"

-+ echo "ERROR $r [boxes=$SHAPE]: rc=$rc, no parsable sweep verdict; see $log" | tee "$verdict"

+ }

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

+index a12678a..6150cf5

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

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

+@@ -152,6 +152,7 @@ func (w *world) resumeStale(b *box, old *claim) {

+ // acting on the claim c it read.

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

+ w.initRecord(b, c)

++ w.finishParticipation(b, c) // a relocation controller whose participation ended (rev 4)

+ // exec lease (claim §7.1)

+ if w.isParticipant(c, b) && !contains(c.Lost, b.ID) {

+ if b.ExecUntil > 0 && w.localNow(b) > b.ExecUntil {

+@@ -161,6 +162,14 @@ func (w *world) role(b *box, c *claim) {

+ b.ExecUntil = w.localNow(b) + execTTL

+ w.execLease[b.ID] = execLease{Op: c.Op.ID, Expires: w.now + execTTL}

+ }

++ if c.Op.Kind == "relocating" {

++ w.recordAck(b, c) // exec_ack.<box>, durable (rev 4)

++ if cur := w.claim; cur != nil && cur.Ver != c.Ver {

++ nc := cur.clone()

++ nc.readStamp = c.readStamp

++ c = nc

++ }

+ } else if c == nil || !w.isParticipant(c, b) {

+ b.ExecUntil = 0

+ }

+@@ -1022,7 +1031,7 @@ func (w *world) landTarget(b *box, c *claim) {

+ w.violate("INV-9: the cut of %s waits on quiet_after[%d] until %d", op.ID, b.Region, c.Quiet[b.Region])

+ }

+ // an earlier stay of this incarnation, in its location here

+- if w.parkStep(b, loc, fmt.Sprintf("superseded/%s/%s/install/", op.ID, host), c.Quiet[b.Region], w.opScope(c, loc), confine(loc)) {

++ if w.parkStep(b, loc, fmt.Sprintf("superseded/%s/%s/install/", op.ID, host), c.Quiet[b.Region], w.opScope(c, loc), w.keepFilesLive(confine(loc))) {

+ w.cas(c, func(n *claim) bool { n.Op.LandPhase = "install-copy"; return sameOp(n.Op.ID, op.ID) })

+ }

+ case "install-copy":

+@@ -1217,6 +1226,9 @@ func (w *world) landTarget(b *box, c *claim) {

+ // written last (R2-6). seal names the files archive version.

+ func (w *world) installLocal(b *box, c *claim, gen string, seal ref, _ string, next func(n *claim)) {

+ if b.Files != nil && b.Files.Gen == gen && b.Files.Done && b.Files.Inc == c.Holder.Inc {

++ if w.perRegion > 1 && !w.preparedManifestHere(b, c, gen) {

++ return // moves §7.6 (L17, R18-1) in the two-box shape: the generation's prepared manifest first

++ }

+ // the marker vouches for everything before it

+ w.cas(c, func(n *claim) bool { next(n); return true })

return

- fi

- caught=0

-@@ -129,20 +140,20 @@ one() {

- fi

- if [ $caught -eq 1 ]; then

- if [ "$expect" = "missed" ]; then

-- echo "STALE $r: $sweep; witness $wit; but expected-outcomes.txt says missed" | tee "$verdict"

-+ echo "STALE $r [boxes=$SHAPE]: $sweep; witness $wit; but expected-outcomes.txt says missed" | tee "$verdict"

- else

-- echo "CAUGHT $r: $sweep; witness $wit" | tee "$verdict"

-+ echo "CAUGHT $r [boxes=$SHAPE]: $sweep; witness $wit" | tee "$verdict"

- fi

- elif [ "$expect" = "missed" ]; then

-- echo "EXPECTED-MISS $r: $sweep; witness $wit" | tee "$verdict"

-+ echo "EXPECTED-MISS $r [boxes=$SHAPE]: $sweep; witness $wit" | tee "$verdict"

- elif [ "$expect" = "rare" ] && [ -n "$depth" ] && [ "$SEEDS" -lt "$depth" ]; then

-- echo "EXPECTED-MISS $r: $sweep; witness $wit (rare: caught at $depth seeds)" | tee "$verdict"

-+ echo "EXPECTED-MISS $r [boxes=$SHAPE]: $sweep; witness $wit (rare: caught at $depth seeds)" | tee "$verdict"

- else

-- echo "MISSED $r: $sweep; witness $wit" | tee "$verdict"

-+ echo "MISSED $r [boxes=$SHAPE]: $sweep; witness $wit" | tee "$verdict"

- fi

+@@ -1281,6 +1293,9 @@ func (w *world) installLocal(b *box, c *claim, gen string, seal ref, _ string, n

+ b.Row.Repl, b.Row.Next = c.Op.Repl, c.Op.Next

+ }

+ b.Files.Done = true

++ if w.perRegion > 1 && !w.preparedManifestHere(b, c, gen) {

++ return // the first branch finishes once the prepared manifest is acknowledged

++ }

+ w.cas(c, func(n *claim) bool { next(n); return true })

}

- export -f one

--export SEEDS PKG SCRATCH BIN WRULES

-+export SEEDS PKG SCRATCH BIN WRULES SHAPE

- printf '%s\n' $RULES | xargs -P "${HOSTLIFE_PAR:-8}" -I{} bash -c 'one "$@"' _ {}

- xrc=$?

- if [ $xrc -ne 0 ]; then

-```

-- [ ] **Step 2: Check the script without running a sweep**

-```bash

-bash -n internal/sim/hostlife/mutate.sh && echo SYNTAX-OK

-HOSTLIFE_LIST=1 internal/sim/hostlife/mutate.sh 0 @regionha | wc -l

-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`, `37`, `145`, `ok`.

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

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

-```bash

-export GOFLAGS=-buildvcs=false

-mkdir -p $TMPDIR/hostlife-sim && nice -n 19 go test -c -o $TMPDIR/hostlife-sim/hostlife.test ./internal/sim/hostlife/

-HOSTLIFE_BOXES=2 HOSTLIFE_PAR=2 nice -n 19 internal/sim/hostlife/mutate.sh 3000 2>&1 | tee $TMPDIR/twobox/sweep-two-box-3000.log

-```

-Expected: exit 0; every rule `CAUGHT` or `EXPECTED-MISS`, none `MISSED`, `STALE` or `ERROR`, every verdict tagged `[boxes=2]`. Each of the 23 witnessed region HA rules is `CAUGHT` with `witness violated` (the two combinations, `reloc-install-receipt` and `reloc-row-cases`, are listed `missed` and report `EXPECTED-MISS ... witness held` alone); the two-box sweep may also catch one-box rules it did not before (a wider catch is fine). A `STALE` region HA rule means the sweep caught what this plan says it cannot: read the seed, and either move the rule to a witness or correct the reason. Record the verdict lines for Task 7. Do not rerun the whole sweep for one fix: a rule that needs rework reruns alone (`HOSTLIFE_BOXES=2 HOSTLIFE_PAR=1 nice -n 19 internal/sim/hostlife/mutate.sh 3000 <rule>`), or the region HA rules together (`... mutate.sh 3000 @regionha`). The one-box sweep is not rerun this revision (ruling 2). No 30,000-seed run.

-Afterwards: `rm -rf $TMPDIR/hostlife-sim`.

-- [ ] **Step 4: Commit**

-```bash

-git add internal/sim/hostlife/mutate.sh internal/sim/hostlife/expected-outcomes.txt

-git commit -m "sim: mutate.sh reports the shape (HOSTLIFE_BOXES), runs the region HA rules as a group and lists without running; expected-outcomes.txt lists the region HA rules caught only in combination or bounded by liveness, loss, determinism or the operator, with the test that shows each

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

-```

----

-### Task 7: The joint-round brief (against 1b-next rev 19)

-**Files:**

-- Create: `docs/superpowers/plans/CODEX-REVIEW-BRIEF-TWO-BOX-R1.md`

-- [ ] **Step 1: Write the brief**

-The brief is for Astra (the independent second reader) and for the claim and moves sessions, who review the model together against 1b-next rev 19. It follows the shape of the latest `CODEX-PLAN-REGION-HA-1BN-BRIEF-*.md` (on `origin/plan-region-ha-1b-next`): what to review, the authorities, what is fixed, what to check, the output wanted. Its content is this plan's evidence, so it is written last, from the logs in `$TMPDIR/twobox/`:

-```markdown

-# Review brief: the joint model with two boxes per region (L18), round 1

-You are an independent second reader, reviewing with the claim and moves

-sessions. Review `internal/sim/hostlife` at the commit named in the

-prompt (branch `region-ha-hostlife-two-box`) against plan 1b-next rev

-19, which Astra's round 18 accepted as "stage A ready to build":

-- plan 1b-next rev 19 `git show origin/plan-region-ha-1b-next:docs/superpowers/plans/2026-10-07-region-ha-1b-next-relocation.md` (rulings 1 to 27; the dispositions of revs 2 to 19, rev 17's for this model's findings F1 to F3; request L21; Task 1's transitions, Task 5's worker and pinner, Task 6's participant, Task 11's gate) and its findings `CODEX-PLAN-REGION-HA-1BN-R1.md` to `R18.md`;

-- 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 3 (its rulings 1 to 19; rulings 14, 16 and 17 mirror 1b-next's fixes for F1 to F3).

-## Fixed: do not re-argue

-- H1 to H19, L1 to L20 as accepted, claim rev 6.30 §1.1's gate, 1b-next rev 19's rulings 1 to 27 as Astra read them; L21 is open and Paul's.

-- The one-box shape is the baseline: its 300-seed COUNTERS line is byte-identical to rev 7.22's after every task (`<paste the line>`), so every one-box verdict of rev 7.22 stands (ruling 2 states the converted-move caveat).

-- The evidence policy: one 3,000-seed sweep per revision (two-box, this round); no deep runs without Paul.

-- The model's abstractions, as moves §14.2 lists them, plus this round's: a failover enters at `pinning` with the D6 barrier at the installing CAS (ruling 4); the stale edges file is the former executor's row (ruling 9); volume evidence is one flag per box (ruling 10); the files publisher runs in the two-box shape and a dead box's disk is never read there (ruling 11); a manifest carries its files as content, so 1b-next's object origins are the chain's newest manifest; the stage B integration with claim 6b and moves Plans 1 and 2 (R1 to R10) has no model step.

-## The guards, mapped

+@@ -1503,7 +1518,7 @@ func (w *world) recoverSource(b *box, c *claim) {

+ if !w.evidence(b, op.RollbackID) {

+ return

+ }

+- if w.parkStep(b, c.Holder.Location, fmt.Sprintf("superseded/%s/%s/return/", op.ID, host), op.StopAt+horizonH, w.opScope(c, c.Holder.Location), confine(c.Holder.Location)) {

++ if w.parkStep(b, c.Holder.Location, fmt.Sprintf("superseded/%s/%s/return/", op.ID, host), op.StopAt+horizonH, w.opScope(c, c.Holder.Location), w.keepFilesLive(confine(c.Holder.Location))) {

+ w.cas(c, func(n *claim) bool { n.Op.SrcPhase = "install-copy"; return sameOp(n.Op.ID, op.ID) })

+ }

+ case "install-copy":

+@@ -1635,7 +1650,7 @@ func (w *world) pushStep(b *box, c *claim) {

+ return true

+ })

+ case "park":

+- if w.parkStep(b, loc, fmt.Sprintf("superseded/%s/%s/push/", op.ID, host), op.StopAt+horizonH, w.opScope(c, loc), confine(loc)) {

++ if w.parkStep(b, loc, fmt.Sprintf("superseded/%s/%s/push/", op.ID, host), op.StopAt+horizonH, w.opScope(c, loc), w.keepFilesLive(confine(loc))) {

+ w.cas(c, func(n *claim) bool { n.Op.Phase = "install"; return sameOp(n.Op.ID, op.ID) })

+ }

+ case "install":

+@@ -1947,8 +1962,8 @@ func (w *world) deadGeneration(c *claim, r int, k string) bool {

+ }

+ return true // a dead generation's certificates

+ }

+- if isManifestKey(k) {

+- // a files manifest outside the files live set (region HA §5.6, L13):

++ if isFilesKey(k) {

++ // a files manifest or object outside the files live set (region HA §5.6, L13):

+ // its generation's, as the data keys are

+ if genOf(h.Location, k) == h.Gen {

+ return !authoritative

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

+index 3ad1cc3..219c9e2

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

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

+@@ -592,7 +592,7 @@ func (w *world) appStart(b *box, c *claim, want string, probe bool, mode string)

+ return false // not an app failure: the agent waits for its config pass

+ }

+ // FailApp is the injected "the target cannot run it" fault: landing probes only

+- healthy := !(probe && b.FailApp && (c.Op.Kind == "landing" || c.Op.Kind == "relocating")) // and relocation probes (region HA, Task 5)

++ healthy := !(probe && b.FailApp && (c.Op.Kind == "landing" || c.Op.Kind == "relocating" && b.ID != c.Op.Src)) // and relocation probes (region HA, Task 5)

+ // §7.7: the probe checks the launch environment at spawn. The forward

+ // path requires the inputs pinned at admission. A recovery probe (the

+ // source's revert or rollback) runs on the inputs it rendered now and

+@@ -1146,7 +1146,7 @@ func (w *world) coverParkedPredecessors(n *claim, region int, gens []string) {

+ // that never had anything (INV-17).

+ func (w *world) hadFilesIn(r int, loc, gen string) bool {

+ for _, k := range w.buckets[r].keys(dataKey(loc, gen, "")) {

+- if genOf(loc, k) == gen && !isManifestKey(k) { // a files manifest is no database object (region HA §5.6)

++ if genOf(loc, k) == gen && !isFilesKey(k) { // a files manifest is no database object (region HA §5.6)

+ return true

+ }

+@@ -1158,7 +1158,7 @@ func (w *world) hadFilesIn(r int, loc, gen string) bool {

+ func (w *world) hasFilesIn(r int, loc, gen string) bool {

+ bk := w.buckets[r]

+ for _, k := range bk.keys(dataKey(loc, gen, "")) {

+- if genOf(loc, k) == gen && bk.current(k) != nil && !isManifestKey(k) { // a files manifest is no database object (region HA §5.6)

++ if genOf(loc, k) == gen && bk.current(k) != nil && !isFilesKey(k) { // a files manifest is no database object (region HA §5.6)

+ return true

+ }

+@@ -1432,6 +1432,9 @@ func (w *world) admits(b *box, c *claim, probe string) bool {

+ case "pushing":

+ return probe == op.ID && op.Phase == "probing"

+ case "relocating":

++ if op.Stuck != "" && on("reloc-stuck-refuses-admission") {

++ return false // relocationAdmission: a stuck operation admits nobody, the source's wake included (ruling 9, R1-16; rev 4, Astra R1-2)

++ }

+ if probe != "" {

+ return probe == op.ID && role(op.Tgt) && op.Phase == "probing"

+ }

+@@ -1607,6 +1610,10 @@ func (w *world) admitWriter(b *box, c *claim, want string, probe bool) (admitInp

+ w.stats["admission refused: op kind"]++

+ return a, false

+ }

++ if c.Op.Kind == "relocating" && c.Op.Stuck != "" && on("reloc-stuck-refuses-admission") {

++ w.stats["admission refused: relocation stuck"]++

++ return a, false

++ }

+ a.KeepStamp = h.Stamp > h.Session

+ if !on("admit-everywhere") && c.Op.Kind != "serving" {

+ a.Mode, a.NewGeneration = "unguarded", want // the mutation: writer sessions for ordinary wakes only (rev 7.8)

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

+index 6086dcb..36efb1e

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

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

+@@ -128,46 +128,6 @@ func TestL18TerminationDuringServing(t *testing.T) {

+ })

+ }

+-func TestL18TerminationInEveryRelocationPhase(t *testing.T) {

+- phases := []string{"starting", "releasing", "pinning", "installing", "installed", "probing", "probed", "opened"}

+- for _, boxes := range []int{1, 2} {

+- for _, who := range []string{"source", "target"} {

+- for _, phase := range phases {

+- if boxes == 1 && (who == "source" || phase == "starting" || phase == "releasing") {

+- continue // a one-box region relocates only by failover, which starts at pinning with the source fenced

+- }

+- name := map[int]string{1: "one-box region", 2: "two-box region"}[boxes] + "/" + who + "@" + phase

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

+- w := regionWorld(boxes)

+- from := w.serveAndPublish(t)

+- w.appWrite(from)

+- w.timerOn(from)

+- w.extraBox(0, spareID()) // a spare for the replacement table

+- if boxes == 2 {

+- w.drainTo(t, nil)

+- } else {

+- w.terminate(from)

+- if w.relocTarget(t) == nil {

+- t.Fatalf("%s", w.violations[0])

+- }

+- if !w.relocPhase(t, phase, w.actAll(), w.recoveryPass) {

+- t.Fatalf("%s", w.violations[0])

+- }

+- if who == "source" {

+- w.terminate(from)

+- } else if x := w.boxByID(w.claim.Op.Tgt); x != nil && w.claim.Op.Kind == "relocating" {

+- w.terminate(x)

+- }

+- w.servingOn(t, nil)

+- w.finish(t)

+- w.mustHold(t)

+- })

+- }

+-}

+ func TestL18NestedFailover(t *testing.T) {

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

+ from := w.serveAndPublish(t)

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

+new file mode 100644

+index 0000000..ad0f45d

+--- /dev/null

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

+@@ -0,0 +1,572 @@

++package hostlife

++import (

++ "crypto/sha256"

++ "fmt"

++ "testing"

++)

++// Astra's round 1 on the two-box plan (rev 4): a direct test for every

++// guard the round found unproven, the phase matrix stopped between single

++// actor transitions, and claim §11's additional witnesses that rev 3 left

++// outside the model. Each test names the rule whose mutation makes it

++// fail.

++// stepUntil advances the world one actor at a time and stops the moment

++// done holds: the tick's own work (completions, stalls, the two-box

++// step), then each live box's worker, obligation runner, reconcile and

++// passes, the executor's wake, then the recovery pass, with done checked

++// after every single one. A fault injected after it returns lands

++// exactly between two transitions.

++func (w *world) stepUntil(t *testing.T, max int, what string, done func() bool) bool {

++ t.Helper()

++ if done() {

++ return true

++ }

++ for i := 0; i < max; i++ {

++ w.now++

++ w.completeDue(false)

++ if p := w.recPend; p != nil && p.at <= w.now {

++ w.recPend = nil

++ if w.rec == nil {

++ w.rec = p.rec

++ }

++ w.runStalled()

++ if w.perRegion > 1 {

++ w.twoBoxStep()

++ }

++ if done() {

++ return true

++ }

++ for _, b := range w.liveBoxes() {

++ for _, act := range []func(){

++ func() { w.worker(b) }, func() { w.obligationRunner(b) }, func() { w.reconcile(b) },

++ func() {

++ if len(b.plans) == 0 {

++ w.passPlan(b, "config")

++ w.passPlan(b, "adopt")

++ }

++ w.passExec(b)

++ },

++ w.wakeExec,

++ } {

++ act()

++ if len(w.violations) > 0 {

++ return false

++ }

++ if done() {

++ return true

++ }

++ w.recoveryPass()

++ w.checkStep()

++ if len(w.violations) > 0 {

++ return false

++ }

++ if done() {

++ return true

++ }

++ w.violate("INV-3 (witness): %s not reached within %d steps: %s", what, max, w.state())

++ return false

++}

++// atPhase: the relocation is exactly in phase p (not beyond it).

++func (w *world) atPhase(p string) func() bool {

++ return func() bool { c := w.claim; return c.Op.Kind == "relocating" && c.Op.Phase == p && c.Op.Stuck == "" }

++}

++// liveIn counts region r's live boxes.

++func (w *world) liveIn(r int) int { return len(w.regionBoxes(r)) }

++// ---------- finding 6: the termination matrix, exact ----------

++// TestL18TerminationAtEveryExactPhase (L18 "termination during every

++// relocation phase", rev 4): the relocation is stopped exactly in each

++// phase of §5.8's table, probe-failed included, between two single

++// actor transitions; the phase and the region's live topology are

++// asserted immediately before the participant is terminated; no spare

++// exists beforehand, and replacements come only from the modelled group

++// after the loss. One-box region: the failover's target (the box the

++// group launched) is terminated. Two-box region: the drain's source or

++// target is.

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

++ phases := []string{"starting", "releasing", "pinning", "installing", "installed", "probing", "probe-failed", "probed", "opened"}

++ for _, boxes := range []int{1, 2} {

++ for _, who := range []string{"source", "target"} {

++ for _, phase := range phases {

++ if boxes == 1 && (who == "source" || phase == "starting" || phase == "releasing") {

++ continue // a one-box region relocates only by failover, which starts at pinning with the source fenced

++ }

++ if phase == "probe-failed" && who == "source" {

++ continue // the source has released before any probe; its loss is the pinning case

++ }

++ name := fmt.Sprintf("%s/%s@%s", map[int]string{1: "one-box region", 2: "two-box region"}[boxes], who, phase)

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

++ w := regionWorld(boxes)

++ from := w.serveAndPublish(t)

++ w.appWrite(from)

++ w.timerOn(from)

++ var target func() *box

++ if boxes == 2 {

++ w.drainTo(t, nil)

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

++ tgt.FailApp = phase == "probe-failed"

++ target = func() *box { return w.boxByID(w.claim.Op.Tgt) }

++ } else {

++ w.terminate(from)

++ if !w.stepUntil(t, 400, "a target named", func() bool { c := w.claim; return c.Op.Kind == "relocating" && c.Op.Tgt >= 0 }) {

++ w.mustHold(t)

++ }

++ w.boxByID(w.claim.Op.Tgt).FailApp = phase == "probe-failed"

++ target = func() *box { return w.boxByID(w.claim.Op.Tgt) }

++ }

++ if !w.stepUntil(t, 2000, "relocation exactly at "+phase, w.atPhase(phase)) {

++ w.mustHold(t)

++ }

++ // immediately before the injection: the exact phase, and the

++ // region's live topology (no spare)

++ if c := w.claim; c.Op.Phase != phase {

++ t.Fatalf("not at %s: %s", phase, w.state())

++ }

++ if n := w.liveIn(0); n != boxes {

++ t.Fatalf("region 0 has %d live boxes before the injection, want %d", n, boxes)

++ }

++ victim := from

++ if who == "target" {

++ victim = target()

++ }

++ if victim == nil || victim.Destroyed {

++ t.Fatalf("no live %s at %s: %s", who, phase, w.state())

++ }

++ w.terminate(victim)

++ w.servingOn(t, nil)

++ w.finish(t)

++ w.mustHold(t)

++ if c := w.claim; c.Op.Exec == victim.ID {

++ t.Fatalf("serving on the terminated %s", who)

++ }

++ })

++ }

++}

++// ---------- finding 2: stuck refuses admission ----------

++// TestStuckSourceRefusesAdmission (reloc-stuck-refuses-admission): three

++// targets die in starting, so the exhausted fence leaves the live source

++// op.exec with its ready row and the operation stuck. A request then

++// reaches the source, whose app has stopped: no writer is admitted.

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

++ w := twoBoxWitness()

++ from := w.boxes[0]

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

++ w.running(t, from)

++ b30, b31 := w.extraBox(0, 30), w.extraBox(0, 31)

++ w.userRelocate()

++ for _, x := range []*box{w.boxByID(w.claim.Op.Tgt), b30, b31, w.boxes[3]} {

++ if x == nil || x.Destroyed || x.ID != w.claim.Op.Tgt {

++ continue

++ }

++ w.terminate(x)

++ w.reach(t, 60, "the dead target fenced", func() bool { return contains(w.claim.Lost, x.ID) }, w.act(from))

++ }

++ if c := w.claim; c.Op.Stuck == "" || c.Op.Exec != from.ID || c.Op.Phase != "starting" || from.Row == nil || from.Row.Status != "ready" {

++ t.Fatalf("not stuck in starting with the live source op.exec and its row ready: %s", w.state())

++ }

++ from.Procs = nil // the app stopped; the next request wakes it

++ before := w.stats["admissions: cold"] + w.stats["admissions: warm"]

++ w.drive(30, never, func() { w.wake(from) })

++ w.mustHold(t)

++ if n := w.stats["admissions: cold"] + w.stats["admissions: warm"] - before; n != 0 || hasMain(from) {

++ t.Fatalf("a stuck operation admitted %d writers on its source (running %v)", n, hasMain(from))

++ }

++}

++// ---------- finding 3: the sole box is checked in an HA region ----------

++// TestHASoleBoxIsCheckedLikeAnyOther (ha-sole-box-eligibility): in a

++// one-box region with region HA on, the only box is refused when it is

++// unenrolled, lacks the secrets key, runs an old executable, is on lost or

++// owes a park-local for the host; in the one-box shape (region HA off)

++// the region's box is chosen as today.

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

++ for _, why := range []string{"unenrolled", "no key", "old executable", "lost", "owes a park-local"} {

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

++ w := regionWorld(1)

++ b := w.boxes[0]

++ w.serve(w.boxes[1], 1, app0) // the claim lives in region 1; region 0 is the create's

++ switch why {

++ case "unenrolled":

++ b.Enrolled = false

++ case "no key":

++ b.HasKey = false

++ case "old executable":

++ b.Old = true

++ case "lost":

++ w.claim.Lost = addUniq(w.claim.Lost, b.ID)

++ case "owes a park-local":

++ w.claim.Obl = append(w.claim.Obl, obligation{ID: "pl", Op: "old", Kind: "park-local", Box: b.ID, Region: -1, Ret: "old"})

++ }

++ if got := w.chooseBox(0, app0); got != nil {

++ t.Fatalf("region HA chose its sole box %d although it is %s", got.ID, why)

++ }

++ })

++ }

++ t.Run("one-box shape keeps today's pick", func(t *testing.T) {

++ w := newWitness()

++ w.boxes[0].Enrolled = false

++ if got := w.chooseBox(0, app0); got != w.boxes[0] {

++ t.Fatalf("the one-box shape did not pick the region's box: %v", got)

++ }

++ })

++}

++// ---------- finding 4: the acknowledgement barrier at every transition ----------

++// TestReplacementWithoutAcknowledgementHoldsEachTransition

++// (reloc-exec-ack-barrier): the target dies at installing and the spare

++// that replaces it has not acknowledged. Driving the installation's steps

++// without the spare's acknowledgement, the operation stays at installing

++// (ToInstalled's requireAcks); once the spare acknowledges, it proceeds.

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

++ w := twoBoxWitness()

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

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

++ w.running(t, from)

++ w.published(t, from)

++ w.drainTo(t, to)

++ spare := w.extraBox(0, 30)

++ if !w.reach(t, 1500, "installing", w.atPhase("installing"), w.act(from, to), w.recoveryPass) {

++ w.mustHold(t)

++ }

++ w.terminate(to)

++ w.reach(t, 60, "replaced at installing", func() bool { return w.claim.Op.Exec == spare.ID }, w.act(from))

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

++ t.Fatalf("the spare acknowledged before it ran")

++ }

++ // the spare's installation steps, without its acknowledgement

++ spare.ExecUntil = w.localNow(spare) + execTTL

++ for i := 0; i < 40; i++ {

++ w.tick()

++ w.relocInstalling(spare, w.claim.clone())

++ }

++ w.mustHold(t)

++ if c := w.claim; c.Op.Phase != "installing" {

++ t.Fatalf("left installing without the spare's acknowledgement: %s", w.state())

++ }

++ w.servingOn(t, spare)

++ w.finish(t)

++ w.mustHold(t)

++}

++// ---------- finding 5: deadlines and delays from the fence record ----------

++// TestPinWaitsForEveryFenceObservation (reloc-pin-delay-every-fence): the

++// source's release is journaled, then the target is terminated and

++// replaced by a spare before any pin. The pin waits out the target's

++// fence observation plus the delay, a release notwithstanding.

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

++ w := twoBoxWitness()

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

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

++ w.running(t, from)

++ w.published(t, from)

++ w.drainTo(t, to)

++ spare := w.extraBox(0, 30)

++ if !w.stepUntil(t, 1500, "the source's release journaled", func() bool { c := w.claim; return c.Op.Release != nil && c.Op.Pin == nil }) {

++ w.mustHold(t)

++ }

++ w.terminate(to)

++ ok := w.stepUntil(t, 400, "the pin", func() bool {

++ c := w.claim

++ if c.Op.Pin != nil && len(c.Op.Observed) > 0 && w.now < latestObservation(c.Op)+failoverPinDelay {

++ t.Fatalf("pinned at %d, before the target's observation %d plus %d", w.now, latestObservation(c.Op), failoverPinDelay)

++ }

++ return c.Op.Pin != nil

++ })

++ if !ok {

++ w.mustHold(t)

++ }

++ if !contains(w.claim.Lost, to.ID) || w.claim.Op.Tgt != spare.ID {

++ t.Fatalf("the target was not replaced before the pin: %s", w.state())

++ }

++ w.servingOn(t, spare)

++ w.finish(t)

++ w.mustHold(t)

++}

++// TestDeadTargetDeadlineFromObservation (reloc-deadline-from-observed-at):

++// the drain's target dies at installing while no worker of the region can

++// observe it (the source is frozen) for longer than the deadline, and the

++// group launches no spare. The first observation writes the fence record;

++// the operation waits a whole deadline from it before it is stuck.

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

++ w := twoBoxWitness()

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

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

++ w.running(t, from)

++ w.published(t, from)

++ w.drainTo(t, to)

++ w.oneBoxRegion[0] = true // no replacement launches: no spare

++ if !w.reach(t, 1500, "installing", w.atPhase("installing"), w.act(from, to), w.recoveryPass) {

++ w.mustHold(t)

++ }

++ w.terminate(to)

++ from.Frozen = true

++ w.drive(releaseDeadline+20, never, w.act(w.boxes[1], w.boxes[2]))

++ from.Frozen = false

++ w.stepUntil(t, 40, "the fence record", func() bool { return to.FenceObservedAt > 0 })

++ seen := w.now

++ w.drive(releaseDeadline-5, never, w.act(from), w.recoveryPass)

++ if w.claim.Op.Stuck != "" {

++ t.Fatalf("stuck %d steps after the observation at %d, before its deadline (terminated at %d)", w.now-seen, seen, to.TerminatedAt)

++ }

++ w.reach(t, 60, "stuck after the deadline", func() bool { return w.claim.Op.Stuck != "" }, w.act(from), w.recoveryPass)

++ w.mustHold(t)

++}

++// ---------- finding 7: the five guards, each discriminated ----------

++// TestOnlyTheExecutorWritesP (reloc-exec-only-installs): at installing,

++// only the source (not op.exec) runs: nothing is written under P and no

++// local install is made on it.

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

++ w := twoBoxWitness()

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

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

++ w.running(t, from)

++ w.published(t, from)

++ w.drainTo(t, to)

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

++ w.mustHold(t)

++ }

++ p := w.claim.Op.Prepared

++ for _, k := range w.buckets[0].keys(dataKey(w.claim.Holder.Location, p, "")) {

++ w.buckets[0].objs[k] = nil // whatever the target began is set aside: only the source acts now

++ delete(w.buckets[0].objs, k)

++ }

++ w.drive(40, never, w.act(from))

++ if ks := w.buckets[0].keys(dataKey(w.claim.Holder.Location, p, "")); len(ks) > 0 || from.receipt != nil || from.Files != nil && from.Files.Gen == p {

++ t.Fatalf("the source, not op.exec, wrote P or installed it: %v", ks)

++ }

++}

++// TestInstallAppliesThePinnedManifest (files-pin-exact): a newer manifest

++// of the dead executor lands between the pin and the install; the install

++// applies the pinned version, never the newest.

++func TestInstallAppliesThePinnedManifest(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)

++ loc := w.claim.Holder.Location

++ late := w.timerOn(from)

++ w.holdKey(loc + "files/")

++ w.publishFiles(from) // the newer manifest, carrying the timer, held

++ w.hold = nil

++ w.terminate(from)

++ if !w.stepUntil(t, 400, "the pin journaled", func() bool { c := w.claim; return c.Op.Pin != nil }) {

++ w.mustHold(t)

++ }

++ if n := w.completeHeld(loc + "files/"); n == 0 {

++ t.Fatalf("no held manifest to land")

++ }

++ if !w.servingOn(t, to) {

++ w.mustHold(t)

++ }

++ if contains(to.Timers, late) {

++ t.Fatalf("the install applied the manifest that landed after the pin")

++ }

++}

++// TestFailoverPinWaitsOutTheDelay (reloc-failover-pin-delay): no pin

++// before the fence's observed_at plus the delay.

++func TestFailoverPinWaitsOutTheDelay(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.terminate(from)

++ ok := w.stepUntil(t, 400, "the pin", func() bool {

++ c := w.claim

++ if c.Op.Pin != nil && w.now < c.Op.FenceAt+failoverPinDelay {

++ t.Fatalf("pinned at %d, before the fence's observation %d plus %d", w.now, c.Op.FenceAt, failoverPinDelay)

++ }

++ return c.Op.Kind == "relocating" && c.Op.Pin != nil

++ })

++ if !ok {

++ w.mustHold(t)

++ }

++ w.servingOn(t, to)

++ w.finish(t)

++ w.mustHold(t)

++}

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

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

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

++func TestPinNeverShortOfTheRelease(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.appWrite(from)

++ w.drainTo(t, to)

++ if !w.stepUntil(t, 1500, "the release journaled", func() bool { c := w.claim; return c.Op.Release != nil && c.Op.Pin == nil }) {

++ w.mustHold(t)

++ }

++ c := w.claim

++ bk := w.buckets[0]

++ var hidden string

++ var vs []*version

++ for _, k := range bk.keys(dataKey(c.Holder.Location, c.Op.Release.Gen, "")) {

++ if l, _, max, ok := ltxLevel(k); ok && l == 0 && max == c.Op.Release.FinalTX {

++ hidden, vs = k, bk.objs[k]

++ delete(bk.objs, k)

++ }

++ if hidden == "" {

++ t.Fatalf("no level-0 file at the release's final_txid %d", c.Op.Release.FinalTX)

++ }

++ w.drive(20, never, w.act(from, to))

++ if p := w.claim.Op.Pin; p != nil && p.TX < c.Op.Release.FinalTX {

++ t.Fatalf("pinned at TXID %d, short of the release's %d", p.TX, c.Op.Release.FinalTX)

++ }

++ bk.objs[hidden] = vs

++ w.servingOn(t, to)

++ w.finish(t)

++ w.mustHold(t)

++}

++// ---------- finding 8: claim §11's additional witnesses ----------

++// TestCrashAtEachOpenBoundary (claim §11 "Crash between prepared

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

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

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

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

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

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

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

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

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

++ from := w.serveAndPublish(t)

++ w.timerOn(from)

++ loc := w.claim.Holder.Location

++ if boxes == 2 {

++ w.drainTo(t, nil)

++ } else {

++ w.terminate(from)

++ }

++ if stage == "marker" {

++ w.holdKey(genMarkerKey(loc))

++ }

++ var to *box

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

++ c := w.claim

++ if c.Op.Kind != "relocating" || c.Op.Tgt < 0 {

++ return false

++ }

++ to = w.boxByID(c.Op.Tgt)

++ if stage == "app" && c.Op.Phase == "probing" && to.envUnreadyFor == 0 {

++ to.envUnreadyFor = 20 // the launch environment is not ready yet

++ }

++ if stage == "open" {

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

++ }

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

++ })

++ if !hit {

++ return

++ }

++ w.crash(to)

++ to.envUnreadyFor = 0

++ w.hold = nil

++ w.servingOn(t, nil)

++ w.finish(t)

++ })

++ }

++}

++// TestAutomaticTargetLossRacesRecordCommit (claim §11 "Automatic target

++// loss racing the record commit CAS"): a move's target is terminated

++// just before, and just after, its record commit CAS; the regional

++// worker's automatic fence takes the operator's record-first path, so the

++// claim follows whichever the record holds: a rollback to the source

++// before the commit, a committed landing (then a failover in the target's

++// region) after it.

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

++ for _, when := range []string{"before the commit", "after the commit"} {

++ t.Run(when, func(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)

++ ok := w.stepUntil(t, 1500, "the commit boundary", func() bool {

++ c := w.claim

++ if when == "before the commit" {

++ return c.Op.Kind == "landing" && c.Op.LandPhase == "probed" && w.rec != nil && w.rec.MoveState == "landing" && w.now >= c.Op.ProbedAt+15

++ }

++ return w.rec != nil && w.rec.MoveState == "committed" && c.Op.Kind == "landing" && !c.Op.Committed

++ })

++ if !ok {

++ w.mustHold(t)

++ }

++ w.terminate(tgt)

++ w.servingOn(t, nil)

++ w.finish(t)

++ w.mustHold(t)

++ c := w.claim

++ if when == "before the commit" && (w.rec.Region != src.Region || w.execBox(c).Region != src.Region) {

++ t.Fatalf("a loss before the commit did not return the host to the source's region: %s", w.state())

++ }

++ if when == "after the commit" && (w.rec.Region != 1 || w.execBox(c).Region != 1) {

++ t.Fatalf("a loss after the commit did not keep the host in the target's region: %s", w.state())

++ }

++ })

++ }

++}

++// ---------- R18-2: the tie-break follows the host ----------

++// TestTieHashFollowsTheHost (tie-hash-host; 1b-next R18-2): on equal

++// loads two hostnames may choose different boxes; the model's tie-break

++// hashes each host's own name.

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

++ w := regionWorld(2)

++ a, b := w.boxes[0], w.peer()

++ sum := func(host string, id int) uint32 { // claim P5-D2, computed here independently of the model

++ s := sha256.Sum256([]byte(fmt.Sprintf("%s\x00%d", host, id)))

++ return uint32(s[0])<<24 | uint32(s[1])<<16 | uint32(s[2])<<8 | uint32(s[3])

++ }

++ wantH, wantH2 := a, a

++ if sum("h", b.ID) > sum("h", a.ID) {

++ wantH = b

++ }

++ if sum("h2", b.ID) > sum("h2", a.ID) {

++ wantH2 = b

++ }

++ if wantH == wantH2 {

++ t.Skip("hosts h and h2 choose the same box among boxes 0 and 3")

++ }

++ if got := w.chooseBoxFor("h", 0, app0); got != wantH {

++ t.Fatalf("host h chose %v, want %d", got, wantH.ID)

++ }

++ if got := w.chooseBoxFor("h2", 0, app0); got != wantH2 {

++ t.Fatalf("host h2 chose %v, want %d", got, wantH2.ID)

++ }

++}

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

+index 9d8e987..11c1ee7

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

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

+@@ -166,6 +166,10 @@ func (w *world) relocRelease(b *box, c *claim) *releaseEntry {

+ if b.pubGen != h.Gen {

+ b.pubGen, b.pubSeq, b.releaseSeq = h.Gen, 0, 0

+ }

++ if !w.ensureObject(b, h, files) {

++ w.stats["release: waits for its files object"]++

++ return nil

++ }

+ if b.releaseSeq == 0 {

+ b.pubSeq++

+ b.releaseSeq = b.pubSeq

+@@ -257,9 +261,86 @@ func (w *world) selectPin(b *box, c *claim) *pinEntry {

+ w.markStuck(c, fmt.Sprintf("the pinned files carry no instance.key for a nonempty database (TXID %d)", n))

+ return nil

+ }

++ if m := w.pinnedManifestOf(b.Region, pin); m != nil && m.Files != nil && m.Files.Obj != "" && !w.originAuthorized(b.Region, c, m.Files.Obj) {

++ // filesPin's referencedOrigins (1b-next rev 12 finding 1, R11-1):

++ // the object the pinned manifest names must be current in this

++ // region's bucket, under this holder's location, at an origin the

++ // pin may cite; otherwise the pin refuses (ErrOrigin) and the

++ // worker retries on a later pass

++ w.stats["pin: files object refused"]++

++ w.logf("DEBUG pin refused obj %s cur=%v", m.Files.Obj, w.buckets[b.Region].current(m.Files.Obj) != nil)

++ return nil

++ }

+ return pin

+ }

++// ---------- files objects (rev 4, Astra R1-8; spec §5.6 "Objects are immutable") ----------

++// objectKey is a files object: <holder.location>/files/<generation>/objects/<content>,

++// written create-only by the generation that first held the content.

++func objectKey(loc, gen string, f *filesDir) string {

++ return dataKey(loc, gen, fmt.Sprintf("files/objects/%d-%d", f.Key, f.Env))

++}

++// isFilesKey: a manifest or an object of the files tree.

++func isFilesKey(k string) bool {

++ return strings.Contains(k, "files/m-") || strings.Contains(k, "files/objects/")

++}

++// objectCurrent: f names an object holding its content, in b's region

++// (the region binding; the mutation of files-objects-region-bound accepts

++// another region's object, as a moved host's carried reference).

++func (w *world) objectCurrent(b *box, f *filesDir) bool {

++ if f == nil || f.Obj == "" || !strings.HasSuffix(f.Obj, fmt.Sprintf("/%d-%d", f.Key, f.Env)) {

++ return false

++ }

++ return f.ObjRegion == b.Region || !on("files-objects-region-bound")

++}

++// ensureObject uploads f's content as an object of the current

++// generation when f names none for it in this region (a changed file, or

++// a host that came from another region), and reports once one is

++// acknowledged; an unchanged file keeps naming the object an older

++// generation wrote, which is what keeps that generation's objects live.

++func (w *world) ensureObject(b *box, h *holder, f *filesDir) bool {

++ if f == nil || w.objectCurrent(b, f) {

++ return true

++ }

++ k := objectKey(h.Location, h.Gen, f)

++ if !w.ackedPut(b, k, &blob{Kind: "files-object", Inc: h.Inc, Gen: h.Gen, Files: f.clone()}, true) {

++ return false

++ }

++ f.Obj, f.ObjRegion = k, b.Region

++ w.stats["files objects written"]++

++ return true

++}

++// originAuthorized is the pin's check of one referenced object: current

++// in region r's bucket under the holder's location, and at an authorized

++// origin. With the rule (files-origins-referenced) the origins are the

++// generations the pinned manifest references, so any such object is

++// authorized; the mutation derives them from holder.generation and the

++// retained admissions, as rev 11 did, which the trim to eight shortens.

++func (w *world) originAuthorized(r int, c *claim, obj string) bool {

++ h := c.Holder

++ if !strings.HasPrefix(obj, h.Location) || w.buckets[r].current(obj) == nil {

++ return false

++ }

++ if on("files-origins-referenced") {

++ return true

++ }

++ g := genOf(h.Location, obj)

++ if g == h.Gen || c.Op.Prepared != "" && g == c.Op.Prepared {

++ return true

++ }

++ for _, e := range h.Admissions {

++ if e.Gen == g || e.Predecessor.Gen == g {

++ return true

++ }

++ return false

++}

+ // pinnedManifestOf is the manifest pin names, read by version.

+ func (w *world) pinnedManifestOf(r int, pin *pinEntry) *blob {

+ if pin.ManKey == "" {

+@@ -469,7 +550,7 @@ func (w *world) relocationLeftovers(n *claim, op opState) {

+ // 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") && !w.leasesSeen(c) {

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

+ return

+ }

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

+@@ -527,7 +608,7 @@ func (w *world) relocReleasing(b *box, c *claim) {

+ }

+ return

+ }

+- if on("reloc-ack-before-pinning") && !w.leasesSeen(c) {

++ if on("reloc-ack-before-pinning") && !acked(c) {

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

+ return

+ }

+@@ -555,7 +636,7 @@ func (w *world) relocReleasing(b *box, c *claim) {

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

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

+ if op.Pin == nil {

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

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

+ return

+ }

+ pin := w.selectPin(b, c)

+@@ -591,7 +672,7 @@ func (w *world) relocPinning(b *box, c *claim) {

+ })

+ return

+ }

+- if on("reloc-exec-ack-barrier") && !w.leasesSeen(c) {

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

+ return

+ }

+ to := op.Tgt

+@@ -661,6 +742,9 @@ func (w *world) relocInstalling(b *box, c *claim) {

+ bk := w.buckets[b.Region]

+ installed := func(n *claim) bool {

+ ok := sameOp(n.Op.ID, op.ID) && n.Op.Kind == "relocating" && n.Op.Phase == "installing" && n.Op.Exec == op.Exec && n.Op.Prepared == g

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

++ ok = false // ToInstalled's requireAcks (rev 4, Astra R1-4)

++ }

+ if ok {

+ n.Op.Phase = "installed"

+ }

+@@ -793,6 +877,9 @@ func (w *world) relocInstalled(b *box, c *claim) {

+ }

+ probing := func(n *claim) bool {

+ ok := sameOp(n.Op.ID, op.ID) && n.Op.Kind == "relocating" && n.Op.Phase == "installed" && n.Op.Exec == op.Exec && n.Op.Receipt != nil

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

++ ok = false // ToProbing's requireAcks (rev 4, Astra R1-4)

++ }

+ if ok {

+ n.Op.Phase, n.Op.ProbingSince = "probing", w.now

+ }

+@@ -1201,6 +1288,7 @@ func (w *world) twoBoxStep() {

+ w.launchReplacements()

+ w.enrollStep()

+ for _, b := range w.liveBoxes() {

++ w.renewController(b)

+ w.publishFiles(b)

+ }

+ if !w.calm && w.fail["terminate"] && w.rng.Intn(200) == 0 {

+@@ -1212,6 +1300,10 @@ func (w *world) twoBoxStep() {

+ if !w.calm && w.rng.Intn(60) == 0 {

+ w.userRelocate()

+ }

++ if !w.calm && w.rng.Intn(400) == 0 {

++ bs := w.liveBoxes()

++ w.updateExecutable(bs[w.rng.Intn(len(bs))]) // claim §5.10: refused while a controller record exists (rev 4)

++ }

+ }

+ // regionHAOwnsLoss: the loss of b is region HA's to recover (model ruling

+@@ -1278,6 +1370,14 @@ func (w *world) fenceStep(b *box, c *claim) bool {

+ if len(cands) == 0 {

+ return false

+ }

++ if x := cands[0]; x.FenceObservedAt == 0 {

++ // hostfence.TerminationWorker: the first worker to observe the

++ // terminated state writes the box-fences record with that

++ // observed_at; every deadline and delay runs from it, never from

++ // the termination itself, which no worker saw (rev 4, Astra R1-5)

++ x.FenceObservedAt = w.now

++ w.logf("box %d observed box %d terminated: fence record, observed_at %d", b.ID, x.ID, w.now)

++ }

+ before := w.claim.Ver

+ w.fence(b, c, cands[0])

+ return w.claim.Ver != before

+@@ -1324,7 +1424,34 @@ func (w *world) fence(b *box, c *claim, x *box) {

+ w.convertToRelocating(c, x)

+ }

+ return

+- case op.Kind == "moving" && op.Tgt == x.ID, (op.Kind == "landing" || op.Kind == "restoring") && op.Tgt == x.ID, op.Kind == "creating":

++ case op.Kind == "landing" && op.Committed && op.Tgt == x.ID && on("fence-converts-committed-landing"):

++ // finding F5 (rev 4): the record committed the landing, so no

++ // rollback is possible, and its dead target can never finish it.

++ // The fence makes it a failover in the target's region, as a

++ // serving executor's fence does (plan ruling 20); the mutation

++ // leaves it to the operator's path, which has nothing to do

++ id := op.ID

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

++ if !sameOp(n.Op.ID, id) || n.Op.Kind != "landing" || !n.Op.Committed || contains(n.Lost, x.ID) {

++ return false

++ }

++ w.startFailover(n, x)

++ w.fenceBox(n, x)

++ return true

++ }) {

++ w.stats["fences written"]++

++ w.stats["relocation started: failover of a committed landing"]++

++ w.logf("box %d fenced box %d, the committed landing %s's dead target: failover in region %d", b.ID, x.ID, id, x.Region)

++ w.declareTimers(x, w.claim.Holder)

++ }

++ return

++ case (op.Kind == "landing" || op.Kind == "restoring") && op.Tgt == x.ID:

++ // claim D2's automatic termination for a move's target (rev 4,

++ // claim §11 "automatic target loss racing the record commit CAS"):

++ // the same record-first declared loss the operator makes

++ w.declareTargetLost(c)

++ return

++ case op.Kind == "moving" && op.Tgt == x.ID, op.Kind == "creating":

+ return

+ case op.Kind == "relocating" && op.Stuck != "":

+ return // Worker.Step consumes no fence of a stuck operation: the operator's resolve does

+@@ -1368,7 +1495,12 @@ func (w *world) fence(b *box, c *claim, x *box) {

+ // regional work with the dead box, where nothing runs it.

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

+ n.Lost = addUniq(n.Lost, x.ID)

+- n.Op.FenceBox, n.Op.FenceAt = x.ID, w.now

++ at := x.FenceObservedAt

++ if at == 0 {

++ at = w.now

++ }

++ n.Op.FenceBox, n.Op.FenceAt = x.ID, at

++ n.Op.Observed = append(n.Op.Observed, at) // fence.<box>.observed_at, retained for every later pin (JournalPin)

+ var parts []int

+ for _, p := range n.Op.Parts {

+ if p != x.ID {

+@@ -1521,7 +1653,7 @@ func (w *world) replaceTarget(n *claim, x *box) bool {

+ }

+ next := w.chooseBoxExcept(n.Op.SrcRegion, n.Holder.App, relocExcept(n.Op, x.ID)...)

+ if next == nil {

+- if on("reloc-dead-target-bound") && w.now > x.TerminatedAt+releaseDeadline {

++ if on("reloc-dead-target-bound") && x.FenceObservedAt > 0 && w.now > observedAt(x)+releaseDeadline {

+ // FenceTargetWithoutSpare (1b-next rev 18 finding 2): the fence

+ // is consumed ReleaseDeadline after its observed_at and the

+ // operation is stuck; the mutation waits for a spare for ever

+@@ -1633,9 +1765,12 @@ func (w *world) publishFiles(b *box) {

+ b.pubGen, b.pubSeq, b.releaseSeq = h.Gen, 0, 0

+ }

+ state := filesState(b.Timers, b.Files)

+- if state == b.published {

++ if state == b.published && w.objectCurrent(b, b.Files) {

+ return

+ }

++ if !w.ensureObject(b, h, b.Files) {

++ return // the object first: a manifest names only durable objects (§5.6)

++ }

+ b.pubSeq++

+ w.issued++

+ bl := &blob{Kind: "files", Inc: h.Inc, Gen: h.Gen, Seq: b.pubSeq, Files: b.Files.clone(), Timers: append([]int(nil), b.Timers...), Base: w.issued}

+@@ -1710,9 +1845,12 @@ func (w *world) filesLive(c *claim, k string) bool {

+ // filesLiveSet is the files live set itself, which the residue oracle

+ // reads whatever is mutated.

+ func (w *world) filesLiveSet(c *claim, k string) bool {

+- if c == nil || c.Holder == nil || !isManifestKey(k) {

++ if c == nil || c.Holder == nil || !isFilesKey(k) {

+ return false

+ }

++ if !isManifestKey(k) {

++ return w.objectReferenced(c, k)

++ }

+ loc := c.Holder.Location

+ if !strings.HasPrefix(k, loc) {

+ return false

+@@ -1766,3 +1904,203 @@ func (w *world) regionMin(r int) int {

+ }

+ return w.perRegion

+ }

++// ---------- acknowledgements (rev 4, Astra R1-4) ----------

++// acked is requireAcks: every current participant has a durable

++// exec_ack.<box> entry in the journal. It reads only the claim; whether a

++// participant's controller is ready now is the participant's own check

++// before its effects (recordAck, and role()'s lease), never the barrier.

++func acked(c *claim) bool {

++ for _, p := range c.Op.Parts {

++ if !contains(c.Op.Acks, p) {

++ return false

++ }

++ return true

++}

++// recordAck is AcknowledgeExecution: a participant whose controller is

++// ready (its execution lease current, role() renews it first) journals

++// exec_ack.<box> once; the entry outlives a lost lease or an agent

++// restart (1b-next rev 2 finding 10: the claim keeps the first

++// acknowledgement). A box replaced out of the participants keeps its

++// entry, which the barrier no longer reads.

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

++ if c == nil || c.Op.Kind != "relocating" || !contains(c.Op.Parts, b.ID) || contains(c.Op.Acks, b.ID) || contains(c.Lost, b.ID) {

++ return

++ }

++ if b.ExecUntil == 0 || w.localNow(b) > b.ExecUntil {

++ return // no ready controller: nothing to acknowledge with

++ }

++ id := c.Op.ID

++ // the controller's durable record exists before the acknowledgement

++ // (1b-next Task 7: journaled before the open), and stays until a

++ // successful scoped cleanup clears it (finishParticipation)

++ b.execRecord, b.cleanupPending = id, true

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

++ ok := sameOp(n.Op.ID, id) && n.Op.Kind == "relocating" && contains(n.Op.Parts, b.ID) && !contains(n.Op.Acks, b.ID)

++ if ok {

++ n.Op.Acks = append(n.Op.Acks, b.ID)

++ }

++ return ok

++ }) {

++ w.logf("relocation %s: box %d acknowledged execution", id, b.ID)

++ }

++}

++// finishParticipation is the participant's Sweep and Finish (1b-next

++// Task 6 and 7, rulings 20): once the claim no longer runs the operation

++// with this box as a live participant, the scoped cleanup runs (it

++// retires an unopened P's local install of that operation, and is a

++// no-op on a box that admitted a writer or serves the host); only when it

++// succeeds is the durable record cleared (rule reloc-clear-after-cleanup;

++// the mutation clears it after a failed cleanup, as rev 4 of 1b-next

++// did). A box whose cleanup fails keeps the record, and root refuses an

++// executable update while it exists (claim §5.10).

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

++ if b.execRecord == "" || c == nil {

++ return

++ }

++ if c.Op.Kind == "relocating" && c.Op.ID == b.execRecord && contains(c.Op.Parts, b.ID) && !contains(c.Lost, b.ID) {

++ return // still a participant

++ }

++ if b.cleanupFails {

++ w.stats["relocation controller: scoped cleanup failed"]++

++ if on("reloc-clear-after-cleanup") {

++ return // the record stays, and so does the refusal of updates

++ }

++ b.execRecord = "" // the mutation: cleared anyway

++ return

++ }

++ if f := b.Files; f != nil && f.Gen != "" && c.Holder != nil && f.Inc == c.Holder.Inc && strings.HasPrefix(f.Gen, "P") && !(c.Op.Kind == "serving" && c.Op.Exec == b.ID) && f.Gen != c.Holder.Gen && !w.ancestorGen(c.Holder.Location, c.Holder.Gen, f.Gen) {

++ w.retireArtifacts(b, f.Inc, f.Stamp) // an unopened P's local install of the finished operation

++ }

++ b.execRecord, b.cleanupPending = "", false

++ w.stats["relocation controller: record cleared"]++

++}

++// updateExecutable is an executable update on b (claim §5.10, region HA

++// §5.10): root refuses it while a relocation controller's record exists.

++// INV-29 is the oracle: an update never runs on a box whose relocation

++// participation's scoped cleanup has not succeeded.

++func (w *world) updateExecutable(b *box) bool {

++ if b.Destroyed {

++ return false

++ }

++ if b.execRecord != "" {

++ w.stats["executable update refused: controller record"]++

++ return false

++ }

++ if b.cleanupPending {

++ w.violate("INV-29: box %d updated its executable while a relocation's scoped cleanup had not succeeded (claim §5.10)", b.ID)

++ }

++ w.stats["executable updated"]++

++ return true

++}

++// latestObservation is the newest observed_at the operation's journal

++// retains (JournalPin checks every fence.<box>.observed_at, a release or

++// not: rev 4, Astra R1-5); FenceAt covers a converted move's fence.

++func latestObservation(op opState) int {

++ at := op.FenceAt

++ for _, o := range op.Observed {

++ if o > at {

++ at = o

++ }

++ return at

++}

++// observedAt is when the fence record says the box was observed

++// terminated (FenceTargetWithoutSpare's deadline basis); the mutation of

++// reloc-deadline-from-observed-at uses the termination itself, which no

++// worker may have seen yet.

++func observedAt(x *box) int {

++ if !on("reloc-deadline-from-observed-at") {

++ return x.TerminatedAt

++ }

++ return x.FenceObservedAt

++}

++// objectReferenced: a live manifest (the chain's newest in any region,

++// the pinned one, holder.generation's or P's) names the object, or a

++// live box's files directory does (its next manifest will): the files

++// live set is every object the live manifests reference (claim §6.2a).

++func (w *world) objectReferenced(c *claim, k string) bool {

++ loc := c.Holder.Location

++ names := func(m *blob) bool { return m != nil && m.Files != nil && m.Files.Obj == k }

++ for r := 0; r < nRegions; r++ {

++ if _, _, _, _, m := w.newestManifest(r, loc, c.Holder.Gen); names(m) {

++ return true

++ }

++ bk := w.buckets[r]

++ for _, g := range []string{c.Holder.Gen, c.Op.Prepared} {

++ if g == "" && g != c.Holder.Gen {

++ continue

++ }

++ for _, mk := range bk.keys(dataKey(loc, g, "files/m-")) {

++ if v := bk.current(mk); v != nil && names(v.B) {

++ return true

++ }

++ if c.Op.Kind == "relocating" && c.Op.Pin != nil && c.Op.Pin.ManKey != "" {

++ if names(w.pinnedManifestOf(c.Op.SrcRegion, c.Op.Pin)) {

++ return true

++ }

++ for _, b := range w.liveBoxes() {

++ if b.Files != nil && b.Files.Obj == k {

++ return true

++ }

++ return false

++}

++// keepFilesLive wraps a moves park's keep (a push's whole-location park,

++// a landing's install park, a rollback's return park) so it never

++// archives the files live set (finding F4, rev 4: claim §6.2a's live set

++// binds every park; moves' parks predate region HA's files tree). Only

++// the two-box shape has files keys, so the one-box shape is unchanged.

++// The mutation of files-live-set-moves-parks archives them with the rest.

++func (w *world) keepFilesLive(keep func(string) bool) func(string) bool {

++ return func(k string) bool {

++ return keep(k) || on("files-live-set-moves-parks") && w.filesLive(w.claim, k)

++ }

++}

++// renewController is a relocation controller's own renewal loop (hostexec

++// renews its lease on its own clock, not when the regional worker happens

++// to run; rev 4): an agent that is up and holds a current lease for a

++// relocation it participates in keeps it current. A lease is still lost

++// when the agent is down, paused, frozen or partitioned past the TTL,

++// which is the scoped cleanup's case. Two-box shape only.

++func (w *world) renewController(b *box) {

++ c := w.claim

++ if c == nil || c.Op.Kind != "relocating" || !contains(c.Op.Parts, b.ID) || !w.agentUp(b) || b.Partitioned {

++ return

++ }

++ if b.ExecUntil > 0 && w.localNow(b) <= b.ExecUntil && b.ExecUntil-w.localNow(b) < execRenew {

++ b.ExecUntil = w.localNow(b) + execTTL

++ w.execLease[b.ID] = execLease{Op: c.Op.ID, Expires: w.now + execTTL}

++ }

++}

++// preparedManifestHere is moves rev 7.22 §7.6's one install routine (L16,

++// L17; claim R18-1) for a landing or a return in the two-box shape (rev

++// 4, claim §11 "move landing, source cleanup, then target failure with an

++// unchanged file"): the generation's prepared files manifest, create-only

++// at sequence 0 in this region, naming objects in this region's bucket

++// (an unchanged file the host carried from another region is uploaded

++// here first), acknowledged before the install's CAS. Without it a

++// target lost right after its commit would leave no files in its region.

++func (w *world) preparedManifestHere(b *box, c *claim, gen string) bool {

++ h := c.Holder

++ if !w.ensureObject(b, h, b.Files) {

++ return false

++ }

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

++}

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

+index 2523a7f..5757177

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

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

+@@ -822,3 +822,148 @@ func wDeadTargetBound(t *testing.T, w *world) {

+ w.servingOn(t, from)

+ w.finish(t)

+ }

++// rev 4: Astra's round 1, claim §11's witnesses

++// wMoveUnchangedFile (files-objects-region-bound; claim §11 "move

++// landing, source cleanup, then target failure with an unchanged file"):

++// the host moves to region 1 carrying a file unchanged since region 0

++// published it; the landing's prepared manifest and the target's

++// publications name an object in region 1's bucket; the source region is

++// cleaned up; the target is terminated and the failover in region 1 pins

++// that object. Without the region binding the manifests keep naming

++// region 0's object, which no failover in region 1 can pin (INV-3).

++func wMoveUnchangedFile(t *testing.T, w *world) {

++ w.twoBox()

++ src := w.boxes[0]

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

++ w.running(t, src)

++ w.published(t, src)

++ w.moveTo(1)

++ if !w.servingOn(t, nil) {

++ return

++ }

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

++ if e.Region != 1 {

++ w.violate("witness: the move did not land in region 1: %s", w.state())

++ return

++ }

++ w.reach(t, 1200, "the source region cleaned up", func() bool { return len(w.claim.Obl) == 0 }, w.actAll(), w.recoveryPass)

++ w.published(t, e)

++ w.terminate(e)

++ w.reach(t, 3000, "serving again after the target's failover", func() bool {

++ c := w.claim

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

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

++ w.finish(t)

++}

++// wOriginsAfterTrim (files-origins-referenced; 1b-next rev 12 finding 1,

++// R11-1): a file published in the origin generation never changes while

++// ten cold admissions follow, so holder.admissions is trimmed past it

++// while the live manifest still names the origin's object. The failover

++// pins that object; authorized from the trimmed admissions alone, the pin

++// is refused for ever (INV-3).

++func wOriginsAfterTrim(t *testing.T, w *world) {

++ w.twoBox()

++ from := w.boxes[0]

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

++ w.running(t, from)

++ w.published(t, from)

++ for i := 0; i < 10; i++ {

++ w.crash(from)

++ if !w.reach(t, 400, "a fresh cold admission serving", func() bool {

++ return hasMain(from) && from.open == nil && len(w.claim.Obl) == 0

++ }, w.actAll(), w.recoveryPass, func() { w.wake(from) }) {

++ return

++ }

++ for _, e := range w.claim.Holder.Admissions {

++ if e.Gen == "" || e.Predecessor.Gen == "" {

++ w.violate("witness: the origin generation is still in holder.admissions: %s", w.state())

++ return

++ }

++ w.terminate(from)

++ w.servingOn(t, w.boxes[3])

++ w.finish(t)

++}

++// wClearAfterCleanup (reloc-clear-after-cleanup; claim §11 "a failed

++// cleanup leaving a controller record that blocks executable updates"):

++// the drain completes; the former source's participation is over, but its

++// scoped cleanup fails, so its controller record stays and root refuses

++// an executable update; once the cleanup succeeds the record is cleared

++// and the update runs. Without the rule the record is cleared after the

++// failed cleanup and the update runs over it (INV-29).

++func wClearAfterCleanup(t *testing.T, w *world) {

++ w.twoBox()

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

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

++ w.running(t, from)

++ w.published(t, from)

++ w.drainTo(t, to)

++ from.cleanupFails = true

++ if !w.servingOn(t, to) {

++ return

++ }

++ w.drive(20, never, w.act(from))

++ if w.updateExecutable(from) {

++ if on("reloc-clear-after-cleanup") {

++ w.violate("witness: an update ran while the controller record existed")

++ }

++ return

++ }

++ from.cleanupFails = false

++ w.reach(t, 100, "the record cleared", func() bool { return from.execRecord == "" }, w.act(from))

++ if !w.updateExecutable(from) {

++ w.violate("INV-3 (witness): the update stayed refused after a successful cleanup")

++ }

++ w.finish(t)

++}

++// wCommittedLandingTargetLost (fence-converts-committed-landing; claim

++// §11 "automatic target loss racing the record commit CAS", finding F5):

++// the record commits the landing, and the target is terminated before

++// the claim follows; the fence makes the committed landing a failover in

++// region 1, which serves; without it nothing ever finishes it (INV-3).

++func wCommittedLandingTargetLost(t *testing.T, w *world) {

++ w.twoBox()

++ src := w.boxes[0]

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

++ w.running(t, src)

++ w.published(t, src)

++ w.moveTo(1)

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

++ if !w.stepUntil(t, 1500, "the record committed, the claim not yet", func() bool {

++ c := w.claim

++ return w.rec != nil && w.rec.MoveState == "committed" && c.Op.Kind == "landing" && !c.Op.Committed

++ }) {

++ return

++ }

++ w.terminate(tgt)

++ w.servingOn(t, nil)

++ w.finish(t)

++}

++// wPushKeepsLiveFiles (files-live-set-moves-parks; finding F4): a push

++// parks the whole location before installing its generation; the files

++// live set survives it, so a later failover pins the live manifest's

++// object. Without the rule the push archives them, and the failover can

++// never pin the host's files (INV-3).

++func wPushKeepsLiveFiles(t *testing.T, w *world) {

++ w.twoBox()

++ from := w.boxes[0]

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

++ w.running(t, from)

++ w.published(t, from)

++ w.userPush()

++ if !w.reach(t, 800, "the push served", func() bool { c := w.claim; return c.Op.Kind == "serving" && c.Holder.Gen != "" && len(c.Obl) == 0 }, w.actAll(), w.recoveryPass, func() { w.wake(from) }) {

++ return

++ }

++ w.drive(10, never, w.act(from))

++ w.completeDue(true)

++ w.terminate(from)

++ w.servingOn(t, w.boxes[3])

++ w.finish(t)

++}

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

+index 7af7a80..598d7ba

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

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

+@@ -186,4 +186,15 @@ var allRules = []string{

+ "reloc-dead-target-bound", // 1b-next rev 18 finding 2 (FenceTargetWithoutSpare): a dead target with no spare is fenced into stuck ReleaseDeadline after its observed_at; the mutation waits for ever (INV-3)

+ "reloc-abandoned-prepared", // 1b-next ruling 27, rev 18 finding 3 (abandonPrepared, abandoned_prepared): every unopened P that is replaced or dropped, on every path, is parked at completion; the mutation records none (INV-10)

+ "files-pin-needs-key", // 1b-next ruling 25 as rev 18 amended it (F2, L21): a nonempty database with an admitted writer pins only a manifest carrying instance.key, else stuck; the mutation pins it keyless and the install mints a fresh key (INV-4)

++ // Astra's round 1 on this plan (rev 4)

++ "reloc-stuck-refuses-admission", // 1b-next relocationAdmission's stuck check (ruling 9, R1-16): a stuck operation admits no writer, the live source's ordinary wake included; the mutation admits it

++ "ha-sole-box-eligibility", // region HA §2 with region HA on: the last remaining box of a region is checked for enrollment, key, executable, lost and park-local like any other; the mutation keeps the one-box shortcut

++ "reloc-pin-delay-every-fence", // JournalPin checks every retained fence observation, after a release too (a target replaced after the source's release); the mutation skips the delay once a release exists

++ "reloc-deadline-from-observed-at", // FenceTargetWithoutSpare's deadline runs from the fence record's observed_at; the mutation runs it from the termination, which no worker saw

++ "tie-hash-host", // claim P5-D2, 1b-next R18-2 (ExecutorChooser hashes the record's host): the tie-break is SHA-256(host + "\x00" + box); the mutation hashes a constant name

++ "files-origins-referenced", // 1b-next rev 12 finding 1 (filesPin's referencedOrigins, R11-1): the pin authorizes the generations the pinned manifest's objects lie in, never only those the trimmed admission list names; the mutation refuses an unchanged file's old origin and the failover waits for ever (INV-3)

++ "files-objects-region-bound", // §5.6 region binding (filesPin: the object in this region's data bucket): a host that came from another region uploads its unchanged files again before naming them; the mutation keeps naming the source region's objects and the failover can never pin (INV-3)

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

+ }

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

+index da4a709..acce63d

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

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

+@@ -401,7 +401,8 @@ func (w *world) checkStep() {

+ // enrolled box that is not on lost; execution authority never names a

+ // fenced or unenrolled reference

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

+- if e := w.boxByID(c.Op.Exec); e == nil || !e.Enrolled || contains(c.Lost, e.ID) {

++ released := c.Op.Release != nil && c.Op.Release.Box == c.Op.Exec // a released executor fenced before PinAfterRelease (FenceSource after the release, rev 4)

++ if e := w.boxByID(c.Op.Exec); e == nil || !e.Enrolled || contains(c.Lost, e.ID) && !released {

+ w.violate("INV-27: relocation %s names box %d as op.exec, which is unenrolled or lost", c.Op.ID, c.Op.Exec)

+ }

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

+index 0d6c828..34a2f02

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

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

+@@ -1,11 +1,14 @@

+ package hostlife

+ import (

++ "crypto/sha256"

+ "fmt"

+ "hash/fnv"

+ "os"

+ )

++var _ = fnv.New32a // rev 1's stand-in hash, kept importable

+ // Two boxes per region (region HA spec 1 §9 L18; claim rev 6.30 §11).

+ //

+ // boxesPerRegion is the world's shape: one box per region, today's model,

+@@ -50,10 +53,19 @@ func (w *world) addBox(r int) *box {

+ // tieHash is the model's stand-in for claim P5-D2's SHA-256 of

+ // host + "\x00" + box reference: a fixed function of the reference, never

+ // a draw, so the choice is the same on every replay.

+-func tieHash(id int) uint32 {

+- h := fnv.New32a()

+- h.Write([]byte(fmt.Sprintf("%s\x00%d", host, id)))

+- return h.Sum32()

++func tieHash(id int) uint32 { return tieHashFor(host, id) }

++// tieHashFor is claim P5-D2's tie-break for the named host (rev 4, Astra

++// R1-8 and 1b-next R18-2): the first four bytes of SHA-256(host + "\x00" +

++// box reference), so two hostnames on equal loads may choose different

++// boxes. The mutation of tie-hash-host hashes a constant name, as the

++// round-18 chooser bug did.

++func tieHashFor(hostName string, id int) uint32 {

++ if !on("tie-hash-host") {

++ hostName = host

++ }

++ sum := sha256.Sum256([]byte(fmt.Sprintf("%s\x00%d", hostName, id)))

++ return uint32(sum[0])<<24 | uint32(sum[1])<<16 | uint32(sum[2])<<8 | uint32(sum[3])

+ }

+ // hostsOn counts the instances of app placed on b (app "" counts every

+@@ -105,8 +117,16 @@ func (w *world) chooseBox(r int, app string) *box { return w.chooseBoxExcept(r,

+ // world; the caller records the choice in the claim's intent and never

+ // substitutes (rule create-choice-once).

+ func (w *world) chooseBoxExcept(r int, app string, except ...int) *box {

++ return w.chooseBoxFor(host, r, app, except...)

++}

++// chooseBoxFor is choose() for the named host (its tie-break hashes that

++// name). The sole-box shortcut, today's behaviour, is the one-box shape's

++// alone: with region HA on, one remaining candidate is checked like any

++// other (rev 4, Astra R1-3; rule ha-sole-box-eligibility).

++func (w *world) chooseBoxFor(hostName string, r int, app string, except ...int) *box {

+ bs := w.regionBoxes(r)

+- if len(bs) <= 1 {

++ if len(bs) <= 1 && (w.perRegion <= 1 || !on("ha-sole-box-eligibility")) {

+ if len(bs) == 0 || contains(except, bs[0].ID) {

+ return nil

+ }

+@@ -125,7 +145,7 @@ func (w *world) chooseBoxExcept(r int, app string, except ...int) *box {

+ if on("reloc-enrolled-only") && !b.Enrolled {

+ continue

+ }

+- key := [3]int{w.hostsOn(b, app), w.hostsOn(b, ""), -int(tieHash(b.ID))}

++ key := [3]int{w.hostsOn(b, app), w.hostsOn(b, ""), -int(tieHashFor(hostName, b.ID))}

+ if best == nil || key[0] < bestKey[0] || key[0] == bestKey[0] && (key[1] < bestKey[1] || key[1] == bestKey[1] && key[2] < bestKey[2]) {

+ best, bestKey = b, key

+ }

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

+index 5b7fa77..a93c223

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

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

+@@ -241,6 +241,17 @@ var witnesses = []witness{

+ {"files-prepared-seq-zero", "files-prepared-seq-zero", "INV-28",

+ "the source's manifests reach sequence 3; P's prepared manifest keeps 3, the probe session publishes its timer at 1, and the nested failover pins and declares from the stale prepared manifest", wFilesPreparedSeqZero},

+ // rev 3: 1b-next rev 17 to 19's fixes for the model's findings, and the L21 window

++ // rev 4: Astra's round 1 and claim §11's additional witnesses

++ {"files-objects-region-bound", "files-objects-region-bound", "INV-3",

++ "claim §11: the host moves to region 1 with a file unchanged since region 0 published it, the source region is cleaned up, then the target dies; the failover pins an object in region 1's bucket, or, without the region binding, can never pin region 0's", wMoveUnchangedFile},

++ {"files-origins-referenced", "files-origins-referenced", "INV-3",

++ "R11-1: a file unchanged through ten cold admissions, holder.admissions trimmed past its origin; the failover pins the origin's object, or, authorized from the trimmed list, is refused for ever", wOriginsAfterTrim},

++ {"reloc-clear-after-cleanup", "reloc-clear-after-cleanup", "INV-29",

++ "claim §11: the former source's scoped cleanup fails after the drain; its controller record stays and root refuses an executable update until the cleanup succeeds; without the rule the update runs over the unfinished cleanup", wClearAfterCleanup},

++ {"fence-converts-committed-landing", "fence-converts-committed-landing", "INV-3",

++ "claim §11, F5: the record commits a landing and its target dies before the claim follows; the fence makes it a failover in the target's region, or nothing ever finishes it", wCommittedLandingTargetLost},

++ {"files-live-set-moves-parks", "files-live-set-moves-parks", "INV-3",

++ "F4: a push parks the whole location; the files live set survives, so the later failover pins the live object, or can never pin the host's files", wPushKeepsLiveFiles},

+ {"files-pin-needs-key", "files-pin-needs-key", "INV-4",

+ "L21, explicit: the pre-start manifest copy landed without instance.key, the app minted the key after starting and replicated rows sealed with it, and the box died before the keyed manifest landed; with the rule recovery is stuck and installs nothing, without it the keyless pin installs a fresh key over the sealed rows", wL21Window},

+ {"reloc-no-spare-bound", "reloc-no-spare-bound", "INV-3",

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

+index cfb51f7..a1b97b2

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

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

+@@ -259,6 +259,11 @@ type filesDir struct {

+ Env int // admin token identity in <host>.env

+ Done bool // markers written last

+ Stamp int // the installation stamp that produced it (claim rev 6.5 §6.3)

++ // Obj is the files object that holds this content (region HA §5.6,

++ // rev 4): written by the generation that first held it, in ObjRegion's

++ // bucket; an unchanged file keeps naming it generations later

++ Obj string

++ ObjRegion int

+ }

+ func (f *filesDir) clone() *filesDir {

+@@ -360,8 +365,15 @@ type box struct {

+ FailSettle bool // the app passes one readiness check, works, then fails

+ Nested bool // nested layout: children survive an agent crash

+ // region HA (two boxes per region, L18)

+- Terminated bool // the cloud terminated the instance (H1): it never runs again and never returns; a Destroyed box that is not Terminated is stopped and may start again with its disk

+- TerminatedAt int

++ Terminated bool // the cloud terminated the instance (H1): it never runs again and never returns; a Destroyed box that is not Terminated is stopped and may start again with its disk

++ TerminatedAt int

++ // a relocation controller's durable record (hostexec, 1b-next Task 7):

++ // the operation it belongs to, whether its scoped cleanup is still owed

++ // (ground truth for INV-29), and the fault that makes the cleanup fail

++ execRecord string

++ cleanupPending bool

++ cleanupFails bool

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

+ Enrolled bool // the roster holds an active entry with its proven cloud identity (H11); a replacement box is enrolled automatically enrollDelay steps after it launches (H16, H17)

+ EnrollAt int

+ DeleteOnTermination bool // every volume the box had attached carried the flag while it ran (§5.9): decides only the automatic discharge of its park-local chores (H19), never a fence

+@@ -826,6 +838,8 @@ type opState struct {

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

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

+ Abandoned []string // abandoned_prepared: every unopened P the operation replaced or dropped, parked at serving (1b-next ruling 27)

+ // journal

+@@ -1222,6 +1236,8 @@ func (c *claim) clone() *claim {

+ n.Op.InstalledOn = append([]int(nil), c.Op.InstalledOn...)

+ n.Op.Discharged = append([]int(nil), c.Op.Discharged...)

+ n.Op.Abandoned = append([]string(nil), c.Op.Abandoned...)

++ n.Op.Acks = append([]int(nil), c.Op.Acks...)

++ n.Op.Observed = append([]int(nil), c.Op.Observed...)

+ if r := c.Op.Release; r != nil {

+ cp := *r

+ cp.Files = r.Files.clone()

+```

+- [ ] **Step 2: Run the gate, the identity traces, the new witnesses, and every new direct test under its mutation**

+```bash

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

+diff $TMPDIR/twobox/baseline-counters.json <(grep COUNTERS $TMPDIR/twobox/task5b.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

+for r in files-objects-region-bound files-origins-referenced reloc-clear-after-cleanup fence-converts-committed-landing files-live-set-moves-parks; do

+ HOSTLIFE_WITNESS=$r nice -n 19 go test ./internal/sim/hostlife/ -run '^TestWitnesses$' -count=1 -v 2>&1 | grep -E "witness .* under" | sed 's/^ *witness_test.go:[0-9]*: //' | cut -c1-150

+done

+for pair in reloc-stuck-refuses-admission:TestStuckSourceRefusesAdmission ha-sole-box-eligibility:TestHASoleBoxIsCheckedLikeAnyOther reloc-exec-ack-barrier:TestReplacementWithoutAcknowledgementHoldsEachTransition reloc-pin-delay-every-fence:TestPinWaitsForEveryFenceObservation reloc-deadline-from-observed-at:TestDeadTargetDeadlineFromObservation reloc-exec-only-installs:TestOnlyTheExecutorWritesP files-pin-exact:TestInstallAppliesThePinnedManifest reloc-failover-pin-delay:TestFailoverPinWaitsOutTheDelay reloc-pin-reaches-release:TestPinNeverShortOfTheRelease tie-hash-host:TestTieHashFollowsTheHost; do

+ HOSTLIFE_MUTATE=${pair%%:*} nice -n 19 go test ./internal/sim/hostlife/ -run "^${pair#*:}\$" -count=1 2>&1 | grep -E '^(ok|FAIL|--- FAIL)' | head -1 | sed "s/^/${pair%%:*}: /"

+done

+```

+Expected (the dry run's): `300 seeds, 0 failed, 483 completed operations; mutated="" boxes=1`, `300 seeds, 0 failed, 487 completed operations; mutated="" boxes=2`, `ok`, `ONE-BOX-COUNTERS-IDENTICAL`, `ONE-BOX-TRACES-IDENTICAL`. For each of the five witnesses: `held`, then `violated: ...` naming INV-3 or, for `reloc-clear-after-cleanup`, INV-29. Every direct-test line is `--- FAIL`. `TestL18TerminationAtEveryExactPhase` runs 24 subtests, and none is skipped.

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

+```bash

+git add internal/sim/hostlife/

+git commit -m "sim: Astra's round 1 on the two-box model: stuck refuses admission, region HA checks a sole box, durable acknowledgements gate every transition, deadlines from the fence record, the exact phase matrix, a discriminating test per guard, files objects with origins and region binding, moves' parks keep the files live set, committed-landing and record-race fences, the controller record that blocks updates, the forced open boundaries, and the tie-break over the real host

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

+```

+---

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

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

+**Files:**

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

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

+```diff

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

+index 72504e3..6154bdb

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

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

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

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

++create-choice-once missed no box-side effect precedes the serving CAS in this model, so a substituted executor leaves nothing behind; the rule's effect is the cancellation of a create whose box is gone (TestCreateNamesItsExecutorOnce fails under the mutation)

++reloc-start-guard missed the chooser's §2 eligibility already excludes a target owing a park-local, a live source never owes one for the host it serves, and a whole-location chore cannot be pending in the region the host serves in (a move into it waits, CC11); TestRelocationStartGuardRefuses shows the refusal

++reloc-exec-ack-barrier missed liveness in the sweep: without the barrier a target that never acknowledged is handed op.exec and the operation waits there instead; TestReplacementWithoutAcknowledgementHoldsEachTransition fails under the mutation (rev 4)

++reloc-pin-reaches-release missed the release's step 2 already waits for the listing to show N, so in the sweep the pin's own check is never the first to see a short listing; TestPinNeverShortOfTheRelease hides the newest file after the release and fails under the mutation (rev 4)

++reloc-failover-pin-delay missed a loss bound, not a safety bound (§5.8): the pin names exact versions and a later PUT adds a version nothing reads; TestFailoverPinWaitsOutTheDelay fails under the mutation (rev 4)

++reloc-exec-only-installs missed every installing CAS is conditional on op.exec, so in the sweep a non-executor's writes are the same create-only objects and its install is retired by its park-local; TestOnlyTheExecutorWritesP lets only the source act at installing and fails under the mutation (rev 4)

++reloc-install-receipt missed caught with reloc-ensure-local (witness): EnsureLocal restores a replacement's missing install whatever the receipt says, as 1b-next rev 14 found ("each covers the other")

++reloc-row-cases missed caught with exec-admission and exec-writer (witness): a reopened stale row routes a request to a box the exec check and AdmitWriter refuse

++reloc-replacement-cap missed an operator bound: without the cap the operation replaces its target a third time instead of waiting for carlos ops host resolve; TestStuckAfterTwoReplacements fails under the mutation

++reloc-drain-needs-writer missed liveness only (1b-next ruling 11): a never-woken host's drain would wait for a release root refuses, until the release deadline; TestDrainRefusedForANeverWokenHost fails under the mutation

++reloc-ack-before-pinning missed defence in depth (1b-next rev 4 N6): installing still waits for the barrier, so a replaced target that never acknowledged holds the operation at pinning instead of releasing; TestReplacedTargetAcknowledgesBeforePinning fails under the mutation

++reloc-probe-attempts missed liveness only (ruling 19): uncounted attempts still end at the probe deadline; TestProbeAttemptsCountedBeforeTheyAreMade fails under the mutation

++fence-terminated-only missed redundant alone: a stopped box fenced by mistake is on lost, so lost-quarantine retires its state and exec-admission refuses it when it starts again; TestStoppedBoxNeverFenced fails under the mutation

++reloc-replacement-table missed after P's first admission the admission rules (recovery-generation, remote-baseline) already refuse reopening P, so resuming at installed with the same P admits a fresh generation from P's remote, as the nested failover does; TestL18NestedFailover fails under the mutation (no nested failover)

++files-pin-exact missed a determinism rule (§5.8): a later manifest PUT adds a version nothing reads; TestInstallAppliesThePinnedManifest lands the newer manifest between the pin and the install and fails under the mutation (rev 4)

++reloc-abandoned-prepared missed the at-rest sweep, which 1b-next ruling 27 keeps as the backstop, retires an unrecorded P before any invariant sees it; the operation's own park is the rule's effect, and TestAbandonedPreparedGenerationParked (both paths) fails under the mutation

++reloc-stuck-refuses-admission missed the stuck operation's live source is still op.exec, so admitting its wake makes no second writer; the refusal keeps a stuck operation from running anything until the operator resolves it (ruling 9); TestStuckSourceRefusesAdmission fails under the mutation

++ha-sole-box-eligibility missed the sweep's HA regions keep two boxes until a termination, and a depleted region's last box is normally eligible; TestHASoleBoxIsCheckedLikeAnyOther checks each refusal and fails under the mutation

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

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

+index c583d97..883996e

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

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

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

+ # internal/sim/hostlife/mutate.sh 3000 # every rule

+ # internal/sim/hostlife/mutate.sh 30000 rule-a rule-b # named rules

+ # internal/sim/hostlife/mutate.sh 30000 rule-a,rule-b # a combination, dropped together

++# HOSTLIFE_BOXES=2 internal/sim/hostlife/mutate.sh 3000 # the two-box shape (region HA L18); unset is one box per region

++# HOSTLIFE_BOXES=2 internal/sim/hostlife/mutate.sh 3000 @regionha # the region HA rules alone (rules_test.go's region HA block)

++# HOSTLIFE_LIST=1 internal/sim/hostlife/mutate.sh 0 @regionha # print the rules a run would check, and run nothing

+ #

+ # Each rule gets two runs under its mutation (rev 7.3): the random sweep

+ # (TestHostLifecycle over the seeds) and the rule's deterministic witness

+@@ -50,6 +53,18 @@ ROOT=$(git -C "$(dirname "$0")" rev-parse --show-toplevel)

+ PKG="$ROOT/internal/sim/hostlife"

+ SCRATCH=${HOSTLIFE_SCRATCH:-${TMPDIR:?}/hostlife-sim}

+ BIN=${HOSTLIFE_BIN:-$SCRATCH/hostlife.test}

++SHAPE=${HOSTLIFE_BOXES:-1}

++RULES="$*"

++if [ -z "$RULES" ]; then

++ RULES=$(sed -n '/^var allRules/,/^}/p' "$PKG/rules_test.go" | grep -o '^\s*"[a-z0-9-]*"' | tr -d ' "\t')

++elif [ "$RULES" = "@regionha" ]; then

++ # every rule of the region HA block: one mutation check per guard

++ RULES=$(sed -n '/^\t\/\/ region HA (two boxes per region, L18)/,/^}/p' "$PKG/rules_test.go" | grep -o '^\s*"[a-z0-9-]*"' | tr -d ' "\t')

++fi

++if [ -n "${HOSTLIFE_LIST:-}" ]; then

++ printf '%s\n' $RULES

++ exit 0

++fi

+ mkdir -p "$SCRATCH/logs" "$SCRATCH/verdicts" || { echo "cannot create $SCRATCH" >&2; exit 2; }

+ if [ ! -x "$BIN" ]; then

+ echo "no test binary at $BIN; build it with: go test -c -o $BIN ./internal/sim/hostlife/" >&2

+@@ -59,10 +74,6 @@ if [ -n "$(find "$PKG" -name '*.go' -newer "$BIN")" ]; then

+ echo "the test binary $BIN is older than the source; rebuild it" >&2

+ exit 2

+ fi

+-RULES="$*"

+-if [ -z "$RULES" ]; then

+- RULES=$(sed -n '/^var allRules/,/^}/p' "$PKG/rules_test.go" | grep -o '^\s*"[a-z0-9-]*"' | tr -d ' "\t')

+-fi

+ # the rules that have witnesses (witness_test.go): a run of one of them

+ # with no witness output is an ERROR, never "none" (R3-6)

+ WRULES=$(grep -o '^\s*{"[a-z0-9-]*",' "$PKG/witness_test.go" | tr -d ' \t{",' | sort -u)

+@@ -75,7 +86,7 @@ one() {

+ verdict="$SCRATCH/verdicts/$tag"

+ for x in $(echo "$r" | tr ',' ' '); do

+ if ! sed -n '/^var allRules/,/^}/p' "$PKG/rules_test.go" | grep -q "^\s*\"$x\","; then

+- echo "ERROR $r: no rule named $x" | tee "$verdict"

++ echo "ERROR $r [boxes=$SHAPE]: no rule named $x" | tee "$verdict"

+ return

+ fi

+ done

+@@ -108,19 +119,19 @@ one() {

+ wit=held

+ fi

+ if [ $wrc -ne 0 ] || grep -q "^panic:\|test timed out" "$wlog"; then

+- echo "ERROR $r: witness run rc=$wrc; see $wlog" | tee "$verdict"

++ echo "ERROR $r [boxes=$SHAPE]: witness run rc=$wrc; see $wlog" | tee "$verdict"

+ return

+ fi

+ if [ "$wit" = none ]; then

+ for x in $(echo "$r" | tr ',' ' '); do

+ if echo "$WRULES" | grep -qx "$x"; then

+- echo "ERROR $r: $x has witnesses but the run produced no witness output; see $wlog" | tee "$verdict"

++ echo "ERROR $r [boxes=$SHAPE]: $x has witnesses but the run produced no witness output; see $wlog" | tee "$verdict"

+ return

+ fi

+ done

+ fi

+ if [ -z "$sweep" ]; then

+- echo "ERROR $r: rc=$rc, no parsable sweep verdict; see $log" | tee "$verdict"

++ echo "ERROR $r [boxes=$SHAPE]: rc=$rc, no parsable sweep verdict; see $log" | tee "$verdict"

+ return

+ fi

+ caught=0

+@@ -129,20 +140,20 @@ one() {

+ fi

+ if [ $caught -eq 1 ]; then

+ if [ "$expect" = "missed" ]; then

+- echo "STALE $r: $sweep; witness $wit; but expected-outcomes.txt says missed" | tee "$verdict"

++ echo "STALE $r [boxes=$SHAPE]: $sweep; witness $wit; but expected-outcomes.txt says missed" | tee "$verdict"

+ else

+- echo "CAUGHT $r: $sweep; witness $wit" | tee "$verdict"

++ echo "CAUGHT $r [boxes=$SHAPE]: $sweep; witness $wit" | tee "$verdict"

+ fi

+ elif [ "$expect" = "missed" ]; then

+- echo "EXPECTED-MISS $r: $sweep; witness $wit" | tee "$verdict"

++ echo "EXPECTED-MISS $r [boxes=$SHAPE]: $sweep; witness $wit" | tee "$verdict"

+ elif [ "$expect" = "rare" ] && [ -n "$depth" ] && [ "$SEEDS" -lt "$depth" ]; then

+- echo "EXPECTED-MISS $r: $sweep; witness $wit (rare: caught at $depth seeds)" | tee "$verdict"

++ echo "EXPECTED-MISS $r [boxes=$SHAPE]: $sweep; witness $wit (rare: caught at $depth seeds)" | tee "$verdict"

+ else

+- echo "MISSED $r: $sweep; witness $wit" | tee "$verdict"

++ echo "MISSED $r [boxes=$SHAPE]: $sweep; witness $wit" | tee "$verdict"

+ fi

+ }

+ export -f one

+-export SEEDS PKG SCRATCH BIN WRULES

++export SEEDS PKG SCRATCH BIN WRULES SHAPE

+ printf '%s\n' $RULES | xargs -P "${HOSTLIFE_PAR:-8}" -I{} bash -c 'one "$@"' _ {}

+ xrc=$?

+ if [ $xrc -ne 0 ]; then

+```

+- [ ] **Step 2: Check the script without running a sweep**

+```bash

+bash -n internal/sim/hostlife/mutate.sh && echo SYNTAX-OK

+HOSTLIFE_LIST=1 internal/sim/hostlife/mutate.sh 0 @regionha | wc -l

+HOSTLIFE_LIST=1 internal/sim/hostlife/mutate.sh 0 | wc -l

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

+```

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

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

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

+```bash

+export GOFLAGS=-buildvcs=false

+mkdir -p $TMPDIR/hostlife-sim && nice -n 19 go test -c -o $TMPDIR/hostlife-sim/hostlife.test ./internal/sim/hostlife/

+HOSTLIFE_BOXES=2 HOSTLIFE_PAR=2 nice -n 19 internal/sim/hostlife/mutate.sh 3000 2>&1 | tee $TMPDIR/twobox/sweep-two-box-3000.log

+```

+Expected: exit 0; every rule `CAUGHT` or `EXPECTED-MISS`, none `MISSED`, `STALE` or `ERROR`, every verdict tagged `[boxes=2]`. Each of the 26 region HA rules witnessed alone is `CAUGHT` with `witness violated` (the two combinations, `reloc-install-receipt` and `reloc-row-cases`, are listed `missed` and report `EXPECTED-MISS ... witness held` alone); the two-box sweep may also catch one-box rules it did not before (a wider catch is fine). A `STALE` region HA rule means the sweep caught what this plan says it cannot: read the seed, and either move the rule to a witness or correct the reason. Record the verdict lines for Task 7. Do not rerun the whole sweep for one fix: a rule that needs rework reruns alone (`HOSTLIFE_BOXES=2 HOSTLIFE_PAR=1 nice -n 19 internal/sim/hostlife/mutate.sh 3000 <rule>`), or the region HA rules together (`... mutate.sh 3000 @regionha`). The one-box sweep is not rerun this revision (ruling 2). No 30,000-seed run.

+Afterwards: `rm -rf $TMPDIR/hostlife-sim`.

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

+```bash

+git add internal/sim/hostlife/mutate.sh internal/sim/hostlife/expected-outcomes.txt

+git commit -m "sim: mutate.sh reports the shape (HOSTLIFE_BOXES), runs the region HA rules as a group and lists without running; expected-outcomes.txt lists the region HA rules caught only in combination or bounded by liveness, loss, determinism or the operator, with the test that shows each

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

+```

+---

+### Task 7: The joint-round brief (against 1b-next rev 19)

+**Files:**

+- Create: `docs/superpowers/plans/CODEX-REVIEW-BRIEF-TWO-BOX-R1.md`

+- [ ] **Step 1: Write the brief**

+The brief is for Astra (the independent second reader) and for the claim and moves sessions, who review the model together against 1b-next rev 19. It follows the shape of the latest `CODEX-PLAN-REGION-HA-1BN-BRIEF-*.md` (on `origin/plan-region-ha-1b-next`): what to review, the authorities, what is fixed, what to check, the output wanted. Its content is this plan's evidence, so it is written last, from the logs in `$TMPDIR/twobox/`:

+```markdown

+# Review brief: the joint model with two boxes per region (L18), round 1

+You are an independent second reader, reviewing with the claim and moves

+sessions. Review `internal/sim/hostlife` at the commit named in the

+prompt (branch `region-ha-hostlife-two-box`) against plan 1b-next rev

+19, which Astra's round 18 accepted as "stage A ready to build":

+- plan 1b-next rev 19 `git show origin/plan-region-ha-1b-next:docs/superpowers/plans/2026-10-07-region-ha-1b-next-relocation.md` (rulings 1 to 27; the dispositions of revs 2 to 19, rev 17's for this model's findings F1 to F3; request L21; Task 1's transitions, Task 5's worker and pinner, Task 6's participant, Task 11's gate) and its findings `CODEX-PLAN-REGION-HA-1BN-R1.md` to `R18.md`;

+- region HA spec 1 `docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md` on `origin/main` (rev 5.4, §24; H1 to H19; §2, §3, §5.2, §5.3, §5.4, §5.6, §5.8, §5.9, §5.10, §7, §9 L1 to L20);

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

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

+- the plan that built it, `docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md` rev 4 (its rulings 1 to 25; rulings 14, 16 and 17 mirror 1b-next's fixes for F1 to F3; "Rev 4: round 1 dispositions" answers Astra's round 1 on the plan, `CODEX-PLAN-REGION-HA-TWO-BOX-R1.md`, and maps each past finding to its proving artifact).

+## Fixed: do not re-argue

+- H1 to H19, L1 to L20 as accepted, claim rev 6.30 §1.1's gate, 1b-next rev 19's rulings 1 to 27 as Astra read them; L21 is open and Paul's.

+- The one-box shape is the baseline: its 300-seed COUNTERS line, a create-interruption trace and the trace hash of every one of its 300 seeds are byte-identical to rev 7.22's after every task (`<paste the COUNTERS line>`), so every one-box verdict of rev 7.22 stands (ruling 2 states the converted-move caveat).

+- The evidence policy: one 3,000-seed sweep per revision (two-box, this round); no deep runs without Paul.

+- The model's abstractions, as moves §14.2 lists them, plus this round's: a failover enters at `pinning` with the D6 barrier at the installing CAS (ruling 4); the stale edges file is the former executor's row (ruling 9); volume evidence is one flag per box (ruling 10); the files publisher runs in the two-box shape and a dead box's disk is never read there (ruling 11); files are objects named by manifests and files directories, created before they are named and bound to a region (plan ruling 25); the stage B integration with claim 6b and moves Plans 1 and 2 (R1 to R10) has no model step.

+## The guards, mapped

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

@@ -6078,16 +7947,30 @@ prompt (branch `region-ha-hostlife-two-box`) against plan 1b-next rev

| reloc-abandoned-prepared | `abandonPrepared`, `abandoned_prepared`, `CompleteRelocation` (ruling 27) | model F3 (rev 17), R17-3 (rev 18) | §5.8 | expected miss (the at-rest sweep backstops); `TestAbandonedPreparedGenerationParked` |

+| files-origins-referenced | `filesPin`'s `referencedOrigins` | R11-1 | §5.6, L13 | witness INV-3 |

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

The model's rev 2 raised F1 (no exit after a failed probe in a two-box region), F2 (a failover before the first files manifest lands mints a fresh `instance.key`) and F3 (an abandoned P never retired by its operation). 1b-next rev 17 to 19 closed them (rulings 25 to 27, rev 18 findings 1 to 3). The model now mirrors each fix. A mutation reopens each gap, and the finding tests pass because the gaps are closed. Check that each mirror is as strong as its guard. L21 stays open: the witness `files-pin-needs-key` scripts the window (a keyless pre-start manifest, a key minted after the start, rows sealed with it and replicated, the box terminated before the keyed manifest lands) and requires recovery to be stuck, never to install the database without its key. Say whether the model's window is the one L21 describes, and whether either candidate contract (pre-provisioning the key, or the replicator holding its first upload) would let the model drop plan ruling 17's restriction on the sweep.

+## Findings F4 to F6 (rev 4), open

+The model's rev 4 found two gaps that neither 1b-next rev 19 nor moves rev 7.22 places, and modelled a fix for each so the sweep converges: F4, moves' parks (push, landing install, rollback return) archive the files live set (rule `files-live-set-moves-parks`, plan ruling 21); F5, a landing committed by its record whose target is then terminated has no recovery owner, and the model converts it to a failover (rule `fence-converts-committed-landing`, plan ruling 20). F6 is model-only: `FenceSource` after a release leaves `op.exec` on a lost box until the pin (plan ruling 24). Say which plan or spec should own F4 and F5, and whether the model's fix is the one it should adopt.

## Results

- Gate: `<the two summary lines, the witness count, the direct tests>`.

- Two-box 3,000-seed sweep: `<every verdict line from $TMPDIR/twobox/sweep-two-box-3000.log>`.

-- Findings the model made while being built, beyond F1 to F3 (rev 3 found none in 1b-next rev 19): `<each seed or witness that violated with the rules on, what it showed, and whether the model or a spec was changed; "none" if none>`.

+- Findings the model made while being built, beyond F1 to F6: `<each seed or witness that violated with the rules on, what it showed, and whether the model or a spec was changed; "none" if none>`.

## What to check

@@ -6102,11 +7985,13 @@ The model's rev 2 raised F1 (no exit after a failed probe in a two-box region),

9. The one-box region (ruling 18): is a witness world with region 0 held at one box a faithful stand-in for a region HA region of one box, or does the round want a mixed sweep shape?

10. The expected misses: is each reason right, or is there an invariant the model should check?

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 says no; check the reasoning, ruling 1, and ruling 2's caveat on the converted move).

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

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

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

## Output

-Findings ranked P1 (a two-writer or data-loss path the model admits, a witness that does not prove its claim, a one-box change), P2 (a case from claim §11 or L18 not covered, a guard whose mutation is wrong, a 1b-next rev 16 guard the model does not mirror), P3 (clarity). Each gives the file and line, the problem, the evidence (a seed, a witness trace, a spec or plan line), and a concrete fix. End with a verdict: the round passes for the one-box and the two-box shape, or it does not, and what would make it pass; and, for each of F1 to F3, which plan or spec should change.

+Findings ranked P1 (a two-writer or data-loss path the model admits, a witness that does not prove its claim, a one-box change), P2 (a case from claim §11 or L18 not covered, a guard whose mutation is wrong, a 1b-next rev 16 guard the model does not mirror), P3 (clarity). Each gives the file and line, the problem, the evidence (a seed, a witness trace, a spec or plan line), and a concrete fix. End with a verdict: the round passes for the one-box and the two-box shape, or it does not, and what would make it pass; and, for each of F4 and F5, which plan or spec should change.

```

Fill every `<...>` from the logs; none may remain.

@@ -6141,8 +8026,8 @@ 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, 37 rules; rev 3 added four for rev 17 to 19); 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 the existing `fence-converts-moving` witness. §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.

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

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

-- **Review Focus.** 1: Task 5 witness `reloc-pin-claim-gen`. 2: Task 2 `verifyReceipt`, witness `reloc-verify-receipt`. 3: Task 3 `fenceExhaustedTarget`, witness `reloc-exhausted-fence`. 4: Task 4 `buildPreparedFiles`, witness `files-prepared-seq-zero`. 5: Task 5's findings tests.

+- **Review Focus.** 1: Task 5 witness `reloc-pin-claim-gen`. 2: Task 2 `verifyReceipt`, witness `reloc-verify-receipt`. 3: Task 3 `fenceExhaustedTarget`, witness `reloc-exhausted-fence`. 4: Task 4 `buildPreparedFiles`, witness `files-prepared-seq-zero`. 5: Task 5's findings tests. 6: Task 1 Steps 1 and 6, Task 5B Step 2.