carlos / platform Public

spec: region HA spec 1 rev 3, answering Astra round 2 (A2-1 to A2-7)

Replication baseline with the level-0 anchor, phase-specific
participant replacement, probe deadline and stuck, per-phase rows,
a third termination evidence method and awaiting-evidence, the
continuous-sync deadline, the S3 write split, and the legacy bind.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Paul Campbell pushed by claude agent, operated by paul@keymail.dev b382186411ed619e83cc4e8cdb0220ca16a645d8 parent d17c843
3 files changed, +320 −66
  • docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md +180 −66
  • docs/superpowers/specs/CODEX-FINDINGS-REGION-HA-2.md +75 −0
  • docs/superpowers/specs/CODEX-REVIEW-BRIEF-REGION-HA-3.md +65 −0

CI failed — run details

diff --git a/docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md b/docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md
index a8c9aba6f..2db72008a 100644
--- a/docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md
+++ b/docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md
@@ -1,10 +1,11 @@
# Region HA, spec 1: placing an instance on a box
-Design, 2026-10-04, **rev 2**. DRAFT. Nothing here is built.
+Design, 2026-10-04, **rev 3**. DRAFT. Nothing here is built.
-Rev 2 answers Astra round 1 (`CODEX-FINDINGS-REGION-HA-1.md`, cited
-**A1-n**). All thirteen findings are accepted; §13 maps each to its
-section.
+Rev 3 answers Astra round 2 (`CODEX-FINDINGS-REGION-HA-2.md`, cited
+**A2-n**, plus the round 1 findings it marked partly resolved). Rev 2
+answered round 1 (`CODEX-FINDINGS-REGION-HA-1.md`, **A1-n**). Every
+finding is accepted; §13 maps each to its section.
This is the first of four specs that give each region high availability
and autoscaling:
@@ -23,8 +24,9 @@ It builds on two specs still in review, and asks them for changes (§9):
- the host lifecycle claim, rev 6.3 (`design-replica-ownership`,
8faa89a4), cited as **claim §n**;
-- move-any-app, rev 7.5 (`design-moves-any-region`, cdc98845), cited as
- **moves §n**.
+- move-any-app, rev 7.6 (`design-moves-any-region`, 29245f69), cited as
+ **moves §n**. Rev 7.6 adds the level-0 anchor that relocation's install
+ relies on (A2-1).
It also builds on nearest-region (on main since 3f4a9bfd), whose box
evidence in the edges file is how a console knows which boxes a region
@@ -183,10 +185,24 @@ multi-box region, it writes, create-only:
published certificate for the region, and checks that `accountId` is
the deployment's account and `region` is the box's region. A record
that fails is ignored and alerts.
-- For an Auto Scaling box, `box id == instanceId`, checked. For a legacy
- box, the record binds its label to its `instanceId`; it is written
- once, by the box itself, before any second box joins its region (§8),
- so a later file cannot rebind the label.
+- For an Auto Scaling box, `box id == instanceId`, checked. Nothing
+ else is needed: the signed document authenticates the whole id.
+- **A legacy box's label is not authenticated by AWS (A1-1 residual).**
+ The signed document proves which instance wrote the record, not that
+ the writer is entitled to the label. So a legacy record is admitted
+ only with an operator's binding, `carlos ops box bind <label>`, run
+ with the operator's own AWS credentials. It checks that:
+ - the record's signed `instanceId` equals the instance id that the
+ region's tofu state records for its `region-host` module (the
+ module's `instance_id` output);
+ - the label is the one already named in that region's claims
+ (`touched.boxes`, `inventory`) and edges file.
+
+ The command writes `"bound_by": {"operator": "…", "tofu_instance_id":
+ "…", "at": "…"}` into a second create-only object,
+ `control/boxes/<label>.bind.json`. A legacy record without one is not
+ verified. All of this happens before any second box joins its region
+ (§8), and create-only storage stops anything rebinding the label later.
- The record is never rewritten. A box id whose record does not verify
is never eligible, and a claim naming one is never relocated
automatically: an operator resolves it.
@@ -243,8 +259,13 @@ Reconcile distinguishes three cases for a relocatable host in its region
| The claim names this box as | Row |
|---|---|
| `op.exec`, op `serving` | mint or keep `ready` |
-| a participant whose phase permits a held row (§5.8 table; moves §9.6) | mint or keep held, never `ready` |
-| neither | **drop the registry row**, and nothing else |
+| a participant whose phase's row column (§5.8 table; moves §9.6) says `ready` | keep `ready`. This is the relocating source in `starting`, and in `releasing` until its admission fence closes (A2-3) |
+| a participant whose phase's row column says held | mint or keep held, never `ready` |
+| neither, and no open obligation of its own for the host | **drop the registry row**, and nothing else |
+
+A box that still owes the host a `park-local` obligation keeps its row
+held until that obligation is done, so the guard and inventory it needs
+stay addressable.
- Dropping a former executor's row is a registry change only. It never
touches local files: that is the operation's `park-local` obligation
@@ -312,10 +333,27 @@ produce one, so HA5 needs them in S3 already.
**The setting.** An app's manifest gains `files_durability`:
-- `continuous`: each changed file is published within about one second
- of its last write (debounced on close and rename, via inotify on the
- host's directory, with a full scan every 10 minutes to catch anything
- a watch missed);
+- `continuous`: a changed file is published within about one second
+ of its **first** unpublished modification, whether or not the app has
+ closed it (A2-5):
+ - **Watches.** inotify `IN_MODIFY`, `IN_CLOSE_WRITE`, `IN_MOVED_*`,
+ `IN_CREATE` and `IN_DELETE` on every directory of the tree, added
+ recursively as directories appear.
+ - **Deadline.** The first modification of a file arms a one-second
+ deadline. Later writes do not push it back. A file still being
+ written is published at the deadline, then again at the next one.
+ - **Overflow.** `IN_Q_OVERFLOW`, or any watch that can't be added,
+ triggers an immediate full scan, comparing size, mtime and inode with
+ the last published state.
+ - **A consistent image.** The uploader reads the file, then checks that
+ size, mtime and inode are unchanged. If they changed, it retries
+ within the deadline. A file that never holds still for a read is
+ published at the scan as it is, and flagged. The files directory is
+ not a database: apps that update a file in place must expect a torn
+ image after a failover, and the docs say so. The instance database is
+ Litestream's.
+ - **Repair.** A full scan every 10 minutes catches anything a watch
+ missed. It is repair, not the normal path;
- `snapshot`: the whole directory is published every
`files_snapshot_interval`, default 15 minutes.
@@ -323,8 +361,8 @@ Carloku maps its plans to this (H6). Apps with no setting get
`snapshot` (open question 2).
**Always continuous, whatever the setting:** `instance.key`,
-`report.token`, `<host>.env`, `<host>-sidecar.env`, and the host's timer
-state (§5.7). They are small, and losing them is what kept kpmg down for
+`report.token`, `<host>.env`, `<host>-sidecar.env`, and the host's wake
+state (§5.7: timer rows, the route's `NextDue` and `Replication`). They are small, and losing them is what kept kpmg down for
1h54m (moves §1.2).
**Ordering (A1-4).** Object versions do not say which update wins, so
@@ -371,19 +409,25 @@ installs a fresh manifest in its new generation (K8).
|---|---|
| Database | restored from the pinned recovery set (§5.8) into the new generation |
| Files directory, env files | the manifest (§5.6), pinned |
-| Timer state | the host's timer rows, as `Registry.ReplaceTimers` rows (moves §9.4), published continuously as a file of their own under the manifest (A1-7) |
+| Wake state | the host's timer rows, as `Registry.ReplaceTimers` rows (moves §9.4), and the route's `NextDue` and `Replication` (moves §6.2), published continuously as one entry under the manifest (A1-7) |
| `<host>.config.env` | rendered for the held row (moves §9.1), needs the secrets key (R9) |
| Release | materialized for the held row (moves §9.2) |
| Certificates | the cert mirror's boot refresh (on main) |
| Registry row | reconcile, once the claim names this box (§5.3) |
| Inventory | written by the new box before it first materializes state (claim §6.3) |
-**Timers (A1-7).** The executor publishes its timer rows for the host
-(active rows and their bookkeeping, moves §9.4's canonical digest) as an
-always-continuous entry in the manifest whenever a row changes: a
-registration, a delivery, a rearm. A once-timer the app registered is
+**Wake state (A1-7).** The executor publishes the host's wake state as
+an always-continuous entry in the manifest whenever any of it changes:
+- its timer rows (active rows and their bookkeeping, moves §9.4's
+ canonical digest), on a registration, a delivery or a rearm;
+- the route's `NextDue`, the app's own next wake
+ (`activator.go:2019-2030`), whenever the activator sets it;
+- the route's `Replication` mode.
+
+The new executor sets `NextDue` and `Replication` from it, as a move's
+landing does (moves §7.6). A once-timer the app registered is
therefore in S3 within about a second of the app being told it
-succeeded. On install the new box imports them with
+succeeded. On install the new box imports the timer rows with
`ReplaceTimers`, preserving `next_at`, `due_at`, `attempts` and
`registration`.
@@ -405,15 +449,16 @@ relocatable host, within one region. Its intent names
ETag. The recovery owner for every phase is the region placer, which
replays from the claim alone (claim C2).
-| Phase | Who acts | `op.exec` | Held row on | May spawn |
+| Phase | Who acts | `op.exec` | Rows (§5.3) | May spawn |
|---|---|---|---|---|
-| `starting` | placer writes intent; `from` (if alive) and `to` write execution leases | `from` | `to` | `from` only |
-| `releasing` | `from` drains: flushes the replica and manifest, records `flushed` in the journal, takes stop evidence. Or, for failover, the placer writes the termination fence (§5.9) | `from` until evidence | `to` | `from`, until its admission fence closes |
-| `pinning` | placer lists the recovery set in `generation_from` and journals exact versions (below) | `none` | `to` | nobody |
-| `installing` | `to` restores the pinned set into a new generation `G'`, applies the pinned manifest, imports timers, and writes `G'`'s baseline: a full database snapshot and a manifest | `none` | `to` | nobody |
-| `installed` | placer CAS: `exec: to`, `holder.generation: G'`, `holder.stamp`: this CAS's `gen` | `to` | `to` | `to` (probe only) |
-| `probing` | `to` probes (moves §7.7, same region) | `to` | `to` | `to` (probe only) |
-| `serving` | placer CAS back to `serving`; `from` gets a `park-local` obligation unless terminated | `to` | `to` (ready) | `to` |
+| `starting` | placer writes intent; `from` (if alive) and `to` write execution leases | `from` | `from` ready; `to` held | `from` only |
+| `releasing` | `from` drains: flushes the replica and manifest, records `flushed` in the journal, takes stop evidence. Or, for failover, the placer writes the termination fence (§5.9) | `from` until evidence | `from` ready until its admission fence closes, then held; `to` held | `from`, until its admission fence closes |
+| `pinning` | placer lists the recovery set in `generation_from` and journals exact versions (below) | `none` | `from` held (if alive); `to` held | nobody |
+| `installing` | `to` restores the pinned set into a new generation `G'`, applies the pinned manifest, imports wake state, and writes `G'`'s replication baseline (below) | `none` | `from` held (if alive); `to` held | nobody |
+| `installed` | placer CAS: `exec: to`, `holder.generation: G'`, `holder.stamp`: this CAS's `gen` | `to` | `from` held until its obligation; `to` held | `to` (probe only) |
+| `probing` | `to` probes (moves §7.7, same region), within the probe deadline | `to` | as `installed` | `to` (probe only) |
+| `probe-failed` | `to` takes stop evidence; placer journals it (below) | `none` | as `installed` | nobody |
+| `serving` | placer CAS back to `serving`; `from` gets a `park-local` obligation unless terminated | `to` | `to` ready; `from` held until its obligation is done, then dropped | `to` |
**The pinned recovery set (A1-2).** In `pinning`, the placer lists
`generation_from` and journals the exact object versions that make up the
@@ -427,9 +472,23 @@ version, files and timers included.
requests S3 had already accepted from the terminated box have
completed. Whatever did not land is the H3 loss window.
-**Populating the new generation (A1-2).** `installing` restores from the
-pinned versions, never from "the current generation", and writes `G'`'s
-baseline before `installed`. Moves §5.1 forbids restoring another
+**Populating the new generation (A1-2, A2-1).** `installing` restores
+from the pinned versions, never from "the current generation", and
+writes `G'`'s **replication baseline** before `installed`, exactly as a
+move's install does (moves rev 7.6 §5.1 steps 2 and 7):
+
+- a full snapshot of the restored database at its final TXID `N`;
+- the **level-0 anchor**, one level-0 LTX file `[N, N]`. The pinned
+ Litestream derives a box's replication position from the newest remote
+ level-0 file. A generation holding a snapshot and nothing at level 0
+ restarts at TXID 1, and a cold restore from the snapshot then skips
+ every later write (moves rev 7.6 R5-1);
+- a manifest naming the files, env and wake state;
+- verification of all three by a fresh read before the `installed` CAS.
+
+The test is the moves one, run for relocation: relocate, write,
+replicate, terminate the new executor, cold-restore, and check that every
+replicated write is present (`internal/sim/litestreamfacts`). Moves §5.1 forbids restoring another
generation **as** the installed one; relocation instead builds `G'` from
a pinned set and only then makes `G'` installed, which is the move
landing's shape (moves §7.6) within one bucket. Late writes from the old
@@ -453,21 +512,31 @@ same pinned set. Nothing has served from `G'` yet, so nothing is lost.
the placer is the only claim writer for this op, under its election
lease, and every CAS is conditional on `op.id` and the phase.
-**A participant terminated mid-relocation.** The claim allows a new
+**Replacing a participant (A2-2, A2-7).** The claim allows a new
operation only from `serving`, so relocation defines its own exits
-(K2):
-
-- `to` terminated before `installed`: the placer replaces `to` with a
- new `to'` in the same op, by a CAS citing the old `to`'s termination
- fence, and resumes at `installing` from the same pinned set. The old
- `to`'s partial `G'` objects are abandoned; `to'` installs into a fresh
- `G''`.
-- `to` terminated at or after `installed`: the placer starts a nested
- failover within the same op: a new `to'`, a new pin of `G'` (which now
- holds `to`'s baseline and any writes it replicated), and the phases
- from `pinning`.
-- `from` terminated during a drain's `releasing`: it becomes a failover,
- with the termination fence as evidence.
+(K2). Each is one CAS, conditional on `op.id` and the phase, that cites
+its evidence and names the replacement `to'`. Every rule that applied to
+the phase still applies, and `to'` writes its execution lease before
+the op leaves that phase.
+
+| `to` stops being usable | Evidence | The op resumes at |
+|---|---|---|
+| terminated in `starting` or `releasing` | `to`'s termination fence | the **same** phase. The source's release requirements are unchanged: a drain still needs `from`'s stop evidence |
+| terminated in `pinning` before the pin is journaled | `to`'s termination fence | `pinning` |
+| terminated after the pin is journaled, before `installed` | `to`'s termination fence | `installing` from the journaled pin, into a fresh generation `G''`. The old `to`'s partial `G'` objects are abandoned |
+| terminated at or after `installed` | `to`'s termination fence | a nested failover: `generation_from` becomes `G'` (which holds `to`'s baseline and anything it replicated), from `pinning` |
+| alive, but its probe fails or misses the **probe deadline** (10 minutes) | `to`'s stop evidence, in `probe-failed` | a nested relocation from `G'`, so writes made during the probe are kept, from `pinning`. `to` is excluded from the choice for this host |
+
+- `from` terminated during a drain's `releasing` turns it into a
+ failover, with the termination fence as evidence.
+- **The bound.** After two replacements of `to` in one op, the placer
+ stops at the current phase's safe point (never between `installed`
+ and a probe) and marks the op `stuck`. It alerts, and the op waits for
+ `carlos ops host resolve <host>`. The host stays down, and the console
+ says why.
+- A `probe-failed` target that cannot produce stop evidence (its cgroup
+ won't drain, claim §6.1) also goes to `stuck`. Nothing moves away from
+ a live box without its stop evidence.
**Cost of a drain:** one cut of a few seconds, like a move's (M2), with
no cross-region copy. Failover's gap is detection plus restore (spec 3).
@@ -495,7 +564,7 @@ A termination fence is written into the operation's journal:
terminated instance visible in `DescribeInstances` for typically under
an hour, so absence proves nothing.
-**Two ways to observe it.**
+**Three ways to observe it.**
1. **The durable event.** An EventBridge rule in each region sends EC2
"Instance State-change Notification" events with `state: terminated`
@@ -506,11 +575,23 @@ A termination fence is written into the operation's journal:
2. **A direct read.** `DescribeInstances` for the instance id, in the
region, returning `terminated` with the deployment's `OwnerId`,
`via: "describe"`.
-
-The queue is why a missed observation is recoverable: a replacement
-placer that starts after the instance vanished from `DescribeInstances`
-still finds its event for two weeks. Past that, an operator resolves it
-with `--declare-lost`.
+3. **The group's own history.** For a box launched by an Auto Scaling
+ group, `DescribeScalingActivities` for the region's group: an
+ activity terminating that instance id with status `Successful`,
+ `via: "activity"`. AWS keeps activity history for six weeks. Spec 4
+ verifies on dev that `Successful` is recorded only once the instance
+ has reached `terminated`; until it is verified, this method is off.
+
+**What is not guaranteed (A2-4).** EC2 delivers state-change events to
+EventBridge on a best-effort basis, so the queue holds only events that
+arrived. When all three methods come back empty, there is **no
+automatic recovery**. The placer marks the box's hosts
+`awaiting-evidence`, alerts at once, and keeps retrying the three reads.
+An operator resolves it with `carlos ops host resolve --declare-lost`,
+which checks CloudTrail's `TerminateInstances` record for the instance
+(90 days of event history) with the operator's own credentials. Absence
+is never evidence, at any point. Spec 3 sets how long the placer retries
+before alerting, and owns the loop that reads the queue and history.
- The placer reads the state itself. It never trusts a box's own
report, an edges file, or a box record's claims about liveness.
@@ -523,17 +604,26 @@ with `--declare-lost`.
## 6. Infrastructure and IAM (A1-12)
- **Box role** gains `ec2:DescribeInstances` with a condition on
- `ec2:Region` equal to the box's region, and the SQS
- `ReceiveMessage`/`DeleteMessage` rights on its region's termination
+ `ec2:Region`, and `autoscaling:DescribeScalingActivities` with a
+ condition on `aws:RequestedRegion`, both equal to the box's region, plus
+ SQS `ReceiveMessage`/`DeleteMessage` on its region's termination
queue. Describe actions do not support resource-tag conditions, so
deployment membership is **not** an IAM property: the verifier checks
`OwnerId`, the region and the box record (§5.9). No `ec2:Stop*`,
- `Terminate*` or `Modify*`. No Auto Scaling rights in spec 1.
+ `Terminate*` or `Modify*`, and no Auto Scaling write rights.
- **Console role:** unchanged, no EC2 rights.
-- **S3:** boxes need `s3:PutObject` (create-only via `If-None-Match`) on
- `instances/<host>/*/files/` and `control/boxes/`, and
- `s3:GetObjectVersion` on the files prefix, in their region's data
- bucket, plus the claim CAS rights the claim spec lists.
+- **S3 (A2-6).** Two kinds of write, kept apart:
+ - **Create-only** (`If-None-Match: *`): content objects and snapshots,
+ `instances/<host>/*/files/*/objects/` and `…/snapshots/`, in the
+ region's data bucket; box records and binds, `control/boxes/`, in the
+ control bucket.
+ - **Conditional replace** (`If-Match`, or `If-None-Match: *` for the
+ first write): `instances/<host>/*/files/*/manifest.json` only.
+
+ S3 policy cannot require either header, so the rule is enforced in the
+ one writer, `hostfiles.Publish`, and tested there. Plus
+ `s3:GetObjectVersion` on the files prefix, and the claim CAS rights the
+ claim spec lists.
- **Tofu:** the `region-host` module gains `delete_on_termination = true`
on the root volume, the EventBridge rule and the queue. Moving to an
Auto Scaling group is spec 4; spec 1 runs on today's fixed boxes and on
@@ -550,6 +640,8 @@ with `--declare-lost`.
| A forged or confused edges file names a terminated instance | ignored: identity comes only from the AWS-signed box record (HA7). |
| Placer dies mid-relocation | the next elected placer replays from the claim (§5.8). |
| Target dies after installing | a nested failover from `G'` (§5.8). |
+| Target alive but its probe keeps failing | stop evidence, then a nested relocation to another box; after two replacements, `stuck` and an alert (§5.8). |
+| No termination evidence can be found | `awaiting-evidence`, an alert, and the operator's `--declare-lost` (§5.9). |
| Two files claim a host | the higher stamp wins (HA4). Two unstamped entries alert. |
| Claim read fails on reconcile | keep existing rows, mint none (C6). |
| `snapshot` app fails over | files lose up to the interval; the database loses about a second. Stated on Overview. |
@@ -591,13 +683,13 @@ those specs finalise a one-box-per-region assumption.
| # | Spec | Change |
|---|---|---|
| K1 | claim §5.1 step 4 | `exec` is the box `choose()` picks among the region's eligible boxes, not "the record region's box". |
-| K2 | claim §4, §8 | New op kind `relocating` (§5.8): same region, from `serving`, with its phase table, admission per phase, the `installed` no-reinstall boundary, and its own exits when a participant terminates. Recovery owner: the region placer. Excludes moves and placements, as `placing` does. |
+| K2 | claim §4, §8 | New op kind `relocating` (§5.8): same region, from `serving`, with its phase table, admission and rows per phase, the `installed` no-reinstall boundary, the phase-specific replacement table (termination and probe failure), the two-replacement bound and `stuck`. Recovery owner: the region placer. Excludes moves and placements, as `placing` does. |
| K3 | claim §7.2, CC5 | A **termination fence** (§5.9), bound to a verified box record, is a lost-box fence, written automatically by the region placer. `terminated` only; `stopped` stays operator-only. No `--readmit` for a terminated box; it still goes on `lost`. |
| K4 | claim §8 | Region placers (boxes) need claim CAS rights for `relocating` and for removing a terminated box's obligations. |
| K5 | claim §9 | Adoption names "the record region's serving box". With several boxes that is ambiguous, so adoption must finish while the region has one box (§8 step 3). |
| K6 | claim §2 | Box names in `op.exec`, `participants`, `touched.boxes`, `inventory` and `lost` are box ids bound by `control/boxes/<id>.json` (§5.1). A legacy label is valid only with a verified record. |
| K7 | moves §7.10 | A move whose participant is terminated mid-move takes the termination fence as M16's evidence automatically, under the same before-commit rules. Moves decides what the placer may do there; the placer only supplies the fence. |
-| K8 | moves §5.1, §6.1, §9.4 | The restore contract includes the files manifest and timer state (§5.6, §5.7). Every installation, a move's landing included, publishes a manifest in its new generation so unchanged files stay recoverable after the next failure. The archive at the cut stays. |
+| K8 | moves §5.1, §6.1, §6.2, §9.4 | Relocation's install uses moves rev 7.6's replication baseline (snapshot plus level-0 anchor). The restore contract includes the files manifest and wake state (§5.6, §5.7). Every installation, a move's landing included, publishes a manifest in its new generation so unchanged files stay recoverable after the next failure. The archive at the cut stays. |
| K9 | joint model | `internal/sim/hostlife` extends to two boxes per region: create spread, relocation by drain, termination mid-serve and in every relocation phase, nested failover, a stale edges file, a forged box id, a stale warm copy, a crash mid-install, late file uploads and late PUTs after termination. |
| K10 | moves §7.1, §7.3 | A move into a multi-box region names its target **box** in the start CAS, chosen by `choose()`. Readiness, evidence, installation and recovery are bound to that box; replacing it is an explicit fenced transition (A1-10). |
| K11 | claim C4, §8 | Reconcile's three row cases (§5.3): held participant rows, dropping a former executor's registry row without touching local state, and the 10-minute sweep as a stated exception to C4 for kept rows. |
@@ -611,7 +703,15 @@ those specs finalise a one-box-per-region assumption.
checks; the files manifest (immutable objects, tombstones, late
uploads, snapshot boundary, `If-Match` races); timer catch-up;
termination-fence acceptance (NotFound, wrong account, wrong region,
- stopped, event vs describe).
+ stopped, event, describe, activity, all three empty); the legacy bind
+ (tofu id mismatch, label not in claims); continuous files with a file
+ held open (published at the deadline), inotify overflow, a file that
+ changes during its read; the create-only and replace split in
+ `hostfiles.Publish`.
+- **Relocation:** every row of the replacement table, the
+ two-replacement bound, `probe-failed` without stop evidence, the
+ source's rows through every phase, and relocate → write → replicate →
+ terminate → cold restore with the level-0 anchor.
- **Integration:** two agents against one fake region, one control
bucket: create lands on the chosen box only; the other box mints no
row; the edge backhauls to the executor; relocate by drain through
@@ -647,7 +747,7 @@ those specs finalise a one-box-per-region assumption.
- **Not planned:** relocating unit- and socket-backed routes (the
console and platform services). Their HA is the HA ladder's, separately.
-## 13. Astra round 1 dispositions
+## 13. Astra round 1 dispositions (rev 2)
| Finding | Disposition |
|---|---|
@@ -664,3 +764,17 @@ those specs finalise a one-box-per-region assumption.
| A1-11 P2 termination evidence can vanish | accepted: EventBridge to SQS with 14-day retention, NotFound never evidence (§5.9) |
| A1-12 P2 Describe permissions by tag | accepted: `ec2:Region` condition, membership checked by the verifier (§6) |
| A1-13 P3 citations | accepted: `lease.go:37`, `reconcile.go:202`, `edgesfile.go:272`/`:326` |
+
+## 14. Astra round 2 dispositions
+
+| Finding | Disposition |
+|---|---|
+| A1-1 residual: a legacy label's first registration | accepted: an operator's bind checked against the region's tofu `instance_id` output and the claims' existing label (§5.1) |
+| A1-7 residual: `routes.next_due` | accepted: wake state carries `NextDue` and `Replication` with the timer rows (§5.6, §5.7) |
+| A2-1 P1 snapshot-only baseline loses the replication position | accepted: moves rev 7.6's replication baseline with the level-0 anchor, verified before `installed`, and its test (§5.8), K8 |
+| A2-2 P1 early target replacement skips release and pinning | accepted: phase-specific replacement table (§5.8), K2 |
+| A2-3 P2 reconcile drops the relocating source | accepted: per-phase rows for both participants (§5.3, §5.8 table) |
+| A2-4 P2 event delivery is best-effort | accepted: a third method (Auto Scaling activity history, verified in spec 4 first), `awaiting-evidence` with an immediate alert, and operator resolution via CloudTrail when all are empty (§5.9) |
+| A2-5 P2 close and rename don't bound continuous sync | accepted: `IN_MODIFY` with a fixed one-second deadline from the first modification, recursive watches, overflow scans, a stable-read check (§5.6) |
+| A2-6 P2 create-only conflicts with manifest replacement | accepted: create-only and conditional-replace writes separated, enforced in one writer (§6) |
+| A2-7 P2 a live target whose probe never passes | accepted: a probe deadline, `probe-failed` with stop evidence, a nested relocation that keeps probe writes, and `stuck` after two replacements (§5.8), K2 |
diff --git a/docs/superpowers/specs/CODEX-FINDINGS-REGION-HA-2.md b/docs/superpowers/specs/CODEX-FINDINGS-REGION-HA-2.md
new file mode 100644
index 000000000..0caf9e6b5
--- /dev/null
+++ b/docs/superpowers/specs/CODEX-FINDINGS-REGION-HA-2.md
@@ -0,0 +1,75 @@
+| Round 1 finding | Disposition |
+|---|---|
+| A1-1 — termination identity | **Partly resolved.** Signed instance documents fix account/region/instance verification. They do not authenticate the surrounding legacy label. The first registration still needs an enforced binding between the registering instance and that label; create-only storage prevents replacement, not an incorrect first registration. |
+| A1-2 — unpopulated generation | **Partly resolved.** Pinning and baseline creation are specified. The snapshot-only baseline has a replication-position defect: A2-1 below. |
+| A1-3 — destructive replay | **Partly resolved.** The no-reinstall boundary addresses ordinary replay. The new participant-replacement transition skips required earlier phases: A2-2. |
+| A1-4 — file ordering | **Resolved.** Immutable objects, ordered mutations, tombstones and conditional manifest publication establish the missing ordering. |
+| A1-5 — installation evidence | **Resolved.** The completion marker separates installation evidence from authority. |
+| A1-6 — participant/former rows | **Partly resolved.** Former-row removal and K11 are explicit, but the new tables omit the relocating source: A2-3. |
+| A1-7 — timer reconstruction | **Partly resolved.** Timer rows and catch-up are covered. App-provided `routes.next_due` remains outside that snapshot; moves §6.2 carries it separately. Replicate and restore that wake state too. |
+| A1-8 — unit/socket routes | **Resolved.** Explicitly excluded from relocation. |
+| A1-9 — multi-box admission | **Resolved.** Capability checks, the HA floor, executable recovery checks and unstamped-entry handling are specified. |
+| A1-10 — move target selection | **Resolved.** K10 binds the chosen target box in the start CAS. |
+| A1-11 — disappearing termination evidence | **Partly resolved.** The queue retains delivered events, but delivery is not guaranteed: A2-4. |
+| A1-12 — Describe permissions | **Resolved.** Supported region restrictions replace resource-tag authorization. |
+| A1-13 — citations | **Resolved.** The three corrections are present. All code citations were checked against `d17c843a`; references to proposed behavior were assessed as change locations. |
+
+Reviewed spec rev 2 at `d17c843a`, against claim rev 6.3 (`8faa89a4`) and moves rev 7.5 (`cdc98845`). H1–H6 remain fixed. The later moves revision was inspected only to check the dependency defect below.
+
+1. **A2-1 — P1 — §5.8 `installing`; K8: a snapshot-only baseline does not establish the replication position.** [Location](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/region-ha/docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md:413)
+
+ **Problem:** The new generation receives a full database snapshot and manifest, without the level-0 state needed to continue replication from that snapshot’s transaction ID. Litestream v0.5.14 derives its remote position from level 0. This is also the defect addressed by the later moves rev 7.6, rather than the cited rev 7.5. [Pinned library source](https://raw.githubusercontent.com/benbjohnson/litestream/v0.5.14/db.go).
+
+ **Failing sequence:** B installs a snapshot through transaction N into G′. With fresh replication metadata and no level-0 anchor, its subsequent uploads restart at transaction 1. B then terminates. A cold restore starts from the snapshot at N and skips those lower-numbered uploads, losing writes that had reached storage.
+
+ **Fix:** Require a verified replication-position baseline before `installed`, including the level-0 anchor used by the corrected moves contract. Update the dependency and K8. Test relocation → write → replicate → terminate → cold restore. The existing [library reproducer](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/litestreamfacts/facts_test.go:256) covers the underlying failure; I inspected it but did not run it.
+
+2. **A2-2 — P1 — §5.8 participant-termination exits: early target replacement skips release and pinning.** [Location](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/region-ha/docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md:460)
+
+ **Problem:** Every target termination “before `installed`” resumes at `installing` using the same pinned set. That includes `starting` and `releasing`, when no pinned set exists and the source may still run.
+
+ **Failing sequence:** A→B enters `starting`; B terminates before A drains. The replacement transition selects C and jumps to `installing`. There is no recovery set to install. A correct implementation must stop there; proceeding by inventing a recovery set would also bypass A’s required stop evidence.
+
+ **Fix:** Make replacement phase-specific. Before source release, replace the target while preserving the release requirements. After release but before a durable pin, resume `pinning`. Only reuse an existing pinned set once it has been journaled. Carry these rules, including replacement participants’ execution leases, into K2.
+
+3. **A2-3 — P2 — §§5.3 and 5.8: reconciliation drops the current source during relocation.** [Location](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/region-ha/docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md:243)
+
+ **Problem:** §5.3 retains an executor’s ready row only when the operation is `serving`. Otherwise it retains only participants permitted a held row. The relocation table permits a held row only on `to`, including during `starting` and `releasing`.
+
+ **Failing sequence:** A serves a host. Its claim enters `relocating/starting`, still naming A as executor and permitting A to spawn. A’s next reconciliation matches neither retention case and drops its route. Requests fail before the intended drain, and the source loses registry state needed by the transfer.
+
+ **Fix:** Specify the source row throughout relocation: retain it while ordinary execution is permitted, then hold it before draining. Drop it only after its participant obligations allow removal. Make §5.3, the phase table and K11 agree.
+
+4. **A2-4 — P2 — §5.9: queue retention is treated as guaranteed termination capture.** [Location](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/region-ha/docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md:500)
+
+ **Problem:** EC2 state-change notifications reach EventBridge on a **best-effort** basis. Fourteen-day SQS retention protects events that arrive; it cannot recover an event that EC2 never delivered. [AWS event reference](https://docs.aws.amazon.com/eventbridge/latest/ref/events-ref-ec2.html).
+
+ **Failing sequence:** The sole box terminates, its notification is missed, and the replacement placer starts after `DescribeInstances` stops returning that instance. This happens within fourteen days, but neither observation method supplies evidence. The stated automatic recovery cannot proceed.
+
+ **Fix:** Explicitly define missing-event recovery immediately, rather than only after fourteen days. Assign durable capture/reconciliation and its availability boundary to spec 3, or state that this case requires operator resolution. Preserve the rule that absence is never fencing evidence.
+
+5. **A2-5 — P2 — §5.6: close/rename notifications do not provide the stated continuous-sync interval.** [Location](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/region-ha/docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md:315)
+
+ **Problem:** Publication is promised about one second after the last write, but the specified triggers are close and rename. A write to an open file produces a modification event; closing it is a separate event. [inotify documentation](https://man7.org/linux/man-pages/man7/inotify.7.html).
+
+ **Failing sequence:** An app writes and fsyncs an existing file, then keeps its descriptor open without further writes. No close or rename occurs. The box terminates five minutes later, before the ten-minute scan. Continuous mode loses a change made minutes earlier.
+
+ **Fix:** Track modifications and impose a publication deadline independent of close. Specify recursive watch coverage, overflow recovery and how uploads obtain a consistent file image. Keep the periodic scan as repair rather than the normal path for open files.
+
+6. **A2-6 — P2 — §§5.6 and 6: create-only permissions conflict with manifest updates.** [Location](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/region-ha/docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md:533)
+
+ **Problem:** §6 describes writes to the files namespace as create-only using `If-None-Match`. §5.6 requires repeated `If-Match` replacement of `manifest.json`.
+
+ **Failing sequence:** The first manifest is created successfully. A file changes. Implementing §6’s restriction prevents replacing the existing manifest, so subsequent file and timer updates never become recoverable.
+
+ **Fix:** Separate immutable object/snapshot permissions from mutable manifest permissions. Specify create-only initialization and conditional replacement for manifests, while retaining create-only publication for content objects and box records.
+
+7. **A2-7 — P2 — §5.8: a live target with a permanently failing probe has no recovery exit.** [Location](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/region-ha/docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md:439)
+
+ **Problem:** After `installed`, recovery only advances through probing to serving. Replacement is defined only when a participant terminates. There is no bounded failure path for a live target whose probe cannot pass.
+
+ **Failing sequence:** A drains successfully. B installs, but its probe consistently fails because of a target-local launch problem. B remains healthy as a platform box, so it is not terminated. The host stays held indefinitely, and the claim prevents another relocation from starting.
+
+ **Fix:** Define a probe deadline and a journaled recovery or operator-resolution state. Transferring away from a live target must obtain stop evidence and preserve any probe writes from G′. Add that transition to K2; the later failover-loop specification does not supply this missing relocation exit.
+
+**Verdict: not ready.**
\ No newline at end of file
diff --git a/docs/superpowers/specs/CODEX-REVIEW-BRIEF-REGION-HA-3.md b/docs/superpowers/specs/CODEX-REVIEW-BRIEF-REGION-HA-3.md
new file mode 100644
index 000000000..389f5de27
--- /dev/null
+++ b/docs/superpowers/specs/CODEX-REVIEW-BRIEF-REGION-HA-3.md
@@ -0,0 +1,65 @@
+# Review brief: region HA spec 1 (box placement), round 3
+
+You are an independent second reader. Review
+`docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md` at
+the commit named in the prompt, in the repository at the working
+directory (Go; carlos platform).
+
+## Fixed: do not re-argue
+
+§0's rulings H1 to H6 are Paul's and are fixed, as are the standing
+rulings listed under them. Report only mechanisms that fail to honour
+them, are unsafe, or are missing.
+
+## What the spec builds on
+
+- Host lifecycle claim rev 6.3: file
+ `/home/paulca/amadan.net/carlos/platform/.claude/worktrees/replica-ownership/docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md`
+- Move-any-app rev 7.6 (29245f69): file
+ `/home/paulca/amadan.net/carlos/platform-moves-design/docs/superpowers/specs/2026-10-02-move-any-app-design.md`
+- Nearest-region, on main: `docs/superpowers/specs/2026-10-01-nearest-region-default-design.md`
+ and `internal/console/regioncandidates.go`.
+
+Those specs are still in review themselves. Where spec 1 relies on them,
+check it relies on what they actually say; §9 lists the changes it asks
+of them.
+
+## Focus
+
+1. **One writer.** Can any sequence (create, relocation, termination,
+ a stale edges file, a stale warm copy, a placer that pauses, the
+ console's box dying, a partition from the control bucket) leave two
+ boxes running or writing one host, or a box serving a stale copy?
+2. **The termination fence (§5.9).** Is `terminated` from
+ DescribeInstances sufficient evidence? What about eventual
+ consistency of EC2 state, a box id that is a label not an instance
+ id, a box in another account or region, a forged edges file.
+3. **Files durability (§5.6).** Restore ordering, tombstones,
+ generation scoping, interaction with the moves archive, what a
+ `snapshot` app loses.
+4. **Reconcile and the edges (§5.3, §5.4).** The slow sweep, the stamp
+ rule, legacy files without stamps.
+5. **The K list (§9).** Is anything missing that the claim or moves
+ specs would need to change for multi-box regions?
+6. **Code citations.** Verify every `file:line` cited against the tree.
+
+A mechanism named, bounded and assigned to spec 2, 3 or 4 (§12) is
+complete at this level; don't pull later specs' depth into this one.
+
+## Output
+
+Findings ranked P1 (unsafe or blocks build), P2 (wrong or missing), P3
+(clarity). Each: section, the problem, a concrete failing sequence, and
+a suggested fix. End with a verdict: ready for plan, or not ready.
+
+## Round 3
+
+This is rev 3, answering your rounds 1 and 2 (`CODEX-FINDINGS-REGION-HA-1.md`
+and `CODEX-FINDINGS-REGION-HA-2.md`). First give a disposition table for
+each round 2 finding (A2-1 to A2-7) and the A1-1 and A1-7 residuals:
+resolved, partly resolved (say what is left), or not resolved. Then
+report only **new** findings, including any that rev 3's fixes
+introduce: the legacy bind (§5.1), per-phase rows (§5.3, §5.8), the
+replacement table, probe deadline and `stuck` (§5.8), the third evidence
+method and `awaiting-evidence` (§5.9), the continuous-sync deadline
+(§5.6) and the S3 write split (§6).