carlos / platform Public

spec: region HA spec 1 rev 4, answering Astra round 3 (A3-1 to A3-4)

One release sequence journaling final TXID and manifest seq, an
operator-only bind enforced by bucket policy, CloudTrail never as
fencing evidence, polling while watch coverage is missing, and S3
conditional-write policies.

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

Paul Campbell pushed by claude 3 weeks ago ff92ca2e03c26557c28b66e6aeb7992d379d5565 parent b382186

3 files changed, +213 −34

docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md +98 −34
docs/superpowers/specs/CODEX-FINDINGS-REGION-HA-3.md +50 −0
docs/superpowers/specs/CODEX-REVIEW-BRIEF-REGION-HA-4.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 2db72008a..2ff01a52c 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,8 +1,9 @@

# Region HA, spec 1: placing an instance on a box

-Design, 2026-10-04, **rev 3**. DRAFT. Nothing here is built.

+Design, 2026-10-04, **rev 4**. DRAFT. Nothing here is built.

-Rev 3 answers Astra round 2 (`CODEX-FINDINGS-REGION-HA-2.md`, cited

+Rev 4 answers Astra round 3 (`CODEX-FINDINGS-REGION-HA-3.md`, **A3-n**,

+plus the A2-5, A2-7 and A1-1 residuals). Rev 3 answered 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.

@@ -62,8 +63,8 @@ Standing rulings this spec keeps:

Today a region is one box. Placement is per region: a bucket record has

`Region` and `Pool` and no box (`internal/provision/provision.go:39`).

Every box whose `CARLOS_REGION` matches mints the route

-(`internal/provision/reconcile.go:335`). Nothing enforces "exactly one

-box" (`reconcile.go:179`).

+(`internal/provision/reconcile.go:335`, called at `:799`). Nothing

+enforces "exactly one box": `reconcile.go:179` states it as intent only.

A second box in a region would break three things:

@@ -71,7 +72,8 @@ A second box in a region would break three things:

15-minute TTL, `internal/lease/lease.go:37`) stops them running at

once, but whichever box a request reaches wins.

2. **Both boxes claim the host to the edges.** The home map breaks the

- tie by sorted box name, with no liveness (`internal/edge/homemap.go:585`),

+ tie by sorted box name, with no liveness (`foldHomes`,

+ `internal/edge/homemap.go:538`, collision at `:582`),

so a dead box that sorts first keeps winning.

3. **A box can serve a stale local copy.** The activator trusts a local

database as the warm cache because "on one box … the local copy can

@@ -154,8 +156,8 @@ names, in the deployment's own account and the region's own AWS region

- Static sites and public addr routes still run on every box

(`everywhereClass`, `reconcile.go:202`). Only relocatable hosts gain an

executor that can change; unit- and socket-backed routes keep theirs.

-- Customer fleets keep their binding stamps and per-request fallback

- (`internal/edge/fleetbind.go`).

+- Customer fleets keep their binding stamps (`internal/host/fleetbind.go`)

+ and per-request fallback (`internal/edge/edge.go:2432`).

- The ingress model: any edge serves any app and backhauls home-run

hosts to their box (multi-region ingress). This spec changes which box

is "home", not how backhaul works.

@@ -198,11 +200,26 @@ multi-box region, it writes, create-only:

- 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

+ The command writes a second object, `control/boxes/<label>.bind.json`:

+ `{"record_version_id": "…", "record_sha256": "…", "instance_id": "…",

+ "tofu_instance_id": "…", "operator": "…", "at": "…"}`. It names the

+ exact box record version it vouches for, so it can't be reused for a

+ different record.

+- **Who may write what is enforced by S3, not by convention (A3-3).**

+ The control bucket's policy (§6):

+ - denies `PutObject` on `control/boxes/*.bind.json` to every principal

+ except the deployment's operator roles;

+ - denies `PutObject` on `control/boxes/*` without

+ `s3:if-none-match: *`, so neither a record nor a bind can be

+ replaced;

+ - denies `DeleteObject` and `DeleteObjectVersion` on

+ `control/boxes/*` to every principal, so neither can be removed to

+ make room for a rebinding.

+ A box can therefore write its own record once, and never a bind. A

+ legacy record without a bind that names its exact version 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.

+ (§8).

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

@@ -292,7 +309,7 @@ stay addressable.

host as `home` (`:326`) only when this box is its executor, and adds

the installation's stamp:

`"hosts": {"shop.bab.oncarlos.com": {"role": "home", "stamp": 41}}`.

-- The home map (`homemap.go:529`) resolves a host claimed by two files to

+- The home map (`foldHomes`, `homemap.go:538`) resolves a host claimed by two files to

the higher stamp (HA4).

- **Unstamped entries.** Before §8's gate opens, every region has one

box, so there is no conflict to resolve. After it opens, every box

@@ -348,12 +365,18 @@ produce one, so HA5 needs them in S3 already.

- **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

+ still published **at every deadline**, as the last image read, and

+ flagged as possibly torn. It never waits for a scan (A2-5 residual).

+ - **Missing coverage.** While any directory has no working watch

+ (overflow, a watch that can't be added, the watch limit reached), the

+ publisher **polls** that subtree once a second, comparing size, mtime

+ and inode, until the watch is restored. Polling is reported as a

+ box metric, and alerts if it lasts an hour. 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;

+ missed. It is repair, never the path a change waits on;

- `snapshot`: the whole directory is published every

`files_snapshot_interval`, default 15 minutes.

@@ -392,9 +415,9 @@ nothing is ever overwritten and one manifest decides.

- **Restore** reads the manifest once, then fetches its base and entries

by the exact versions it lists (claim C3). Nothing else in the prefix

is read.

-- **Drain flush.** Before stop evidence, the source publishes a manifest

- whose `seq` covers every local mutation, and records that `seq` in the

- relocation journal (§5.8).

+- **Release flush.** A box giving up a host publishes every pending

+ mutation, **whatever the app's setting**, before its stop evidence

+ (§5.8's release sequence).

A `snapshot` app's files can be up to the interval older than its

database after a failover, and the console says so on the app's

@@ -452,22 +475,39 @@ replays from the claim alone (claim C2).

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

-| `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 |

+| `releasing` | `from` runs the **release sequence** (below). 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 |

| `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 |

+**The release sequence (A3-2).** Whenever a live box gives up a host,

+the source in `releasing` or a failed target in `probe-failed`, it does

+these in order, journaling each:

+1. close admission and drain spawn attempts (claim §6.1);

+2. flush the database: final checkpoint and `SyncAndWait`, then record

+ the **final TXID** `N`, the `MaxTXID` of the newest level-0 file

+ (moves rev 7.6 §5.1 step 1);

+3. publish every pending file and wake-state mutation, **whatever the

+ app's `files_durability`**, and record the manifest's final `seq`;

+4. take stop evidence (claim §6.1).

+The journal entry is `{"released_by": "<box>", "generation": "<G>",

+"final_txid": N, "manifest_seq": S}`, and `pinning` refuses to pin less

+than it.

**The pinned recovery set (A1-2).** In `pinning`, the placer lists

`generation_from` and journals the exact object versions that make up the

database (latest snapshot and the LTX files after it) and the manifest

version, files and timers included.

-- **Drain:** the set must reach the journaled `flushed` position and

- manifest `seq`. If the listing has not caught up, `pinning` waits; it

- never pins less than what the source flushed.

+- **After a release sequence** (drain, rebalance, probe failure): the set

+ must reach the journaled `final_txid` and `manifest_seq`. If the listing

+ has not caught up, `pinning` waits; it never pins less than what the

+ releasing box flushed.

- **Failover:** the placer pins after the fence plus 30 seconds, so

requests S3 had already accepted from the terminated box have

completed. Whatever did not land is the H3 loss window.

@@ -525,7 +565,7 @@ the op leaves that phase.

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

+| alive, but its probe fails or misses the **probe deadline** (10 minutes) | `to`'s release sequence, in `probe-failed` | a nested relocation from `G'`, from `pinning`, pinned to at least `to`'s journaled `final_txid` and `manifest_seq`, so writes made during the probe are kept. `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.

@@ -534,8 +574,9 @@ the op leaves that phase.

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 `probe-failed` target that cannot finish its release sequence (its

+ cgroup won't drain, claim §6.1, or its flush fails) 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

@@ -587,10 +628,17 @@ 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

+The only way out is claim §7.2 unchanged: an operator's

+`carlos ops host resolve --declare-lost`, which needs the instance's

+terminal state (`stopped` or `terminated`) read through the cloud API

+with the operator's own credentials. A CloudTrail `TerminateInstances`

+record is **not** evidence (A3-1): it proves a request was made, and an

+instance can stay `shutting-down` after a successful one. The console

+may show it to help an operator find the instance, nothing more. If no

+terminal state can be read, the hosts stay `awaiting-evidence`. That is

+a liveness gap, accepted: it needs a lost event, a gap of more than an

+hour before anyone looks, and a group whose history doesn't show the

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

@@ -620,8 +668,13 @@ before alerting, and owns the loop that reads the queue and history.

- **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 enforces both in policy (A3-3): the data bucket denies `PutObject`

+ on `…/objects/*` and `…/snapshots/*` without `s3:if-none-match: *`, and

+ on `…/manifest.json` without either `s3:if-match` or

+ `s3:if-none-match: *`. The one writer, `hostfiles.Publish`, sends the

+ headers and is tested against both refusals. The control bucket's

+ `control/boxes/` rules are in §5.1. Each Deny is scoped to its prefix

+ only: a broad Deny on this bucket once broke every lease release. 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`

@@ -683,13 +736,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 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`. |

+| 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`, and the release sequence (final TXID and manifest `seq` journaled before stop evidence, for the source and for a failed target). 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`. The operator path keeps §7.2's terminal-state rule: a CloudTrail request record never substitutes for it. |

| 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, §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. |

+| 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). A box releasing a host flushes all file mutations whatever the plan. 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. |

@@ -778,3 +831,14 @@ those specs finalise a one-box-per-region assumption.

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

+## 15. Astra round 3 dispositions

+| Finding | Disposition |

+|---|---|

+| A2-5 residual: an unstable file waits for the scan; a failed watch | accepted: published at every deadline as the last image, flagged; per-second polling while coverage is missing (§5.6) |

+| A2-7 residual and A3-2 P1: probe failure skips the target's durability barrier | accepted: one release sequence for the source and a failed target, journaling `final_txid` and `manifest_seq` before stop evidence, all files flushed whatever the plan; pinning must reach them (§5.8), K2, K8 |

+| A1-1 residual and A3-3 P1: the bind isn't operator-authenticated | accepted: binds name the exact record version; the control bucket's policy limits binds to operator roles and denies replace and delete under `control/boxes/` (§5.1) |

+| A3-1 P1: a CloudTrail request is not compute fencing | accepted: claim §7.2's terminal-state rule unchanged; CloudTrail is a finding aid only; otherwise `awaiting-evidence` (§5.9), K3 |

+| A3-3 (part): S3 can enforce conditional headers | accepted: `s3:if-none-match` and `s3:if-match` policy conditions, scoped per prefix (§6) |

+| A3-4 P3: citations | accepted: `internal/host/fleetbind.go`, `edge.go:2432`, `homemap.go:538`/`:582`, `reconcile.go:335`/`:799` |

diff --git a/docs/superpowers/specs/CODEX-FINDINGS-REGION-HA-3.md b/docs/superpowers/specs/CODEX-FINDINGS-REGION-HA-3.md

new file mode 100644

index 000000000..0a34cad7b

--- /dev/null

+++ b/docs/superpowers/specs/CODEX-FINDINGS-REGION-HA-3.md

@@ -0,0 +1,50 @@

+| Finding | Disposition |

+|---|---|

+| A2-1 — replication baseline | **Resolved.** Snapshot, level-0 anchor and verification are required before `installed`, matching moves rev 7.6. |

+| A2-2 — early target replacement | **Resolved.** Replacement preserves release requirements and resumes at the appropriate phase. Replacement execution leases are explicit. |

+| A2-3 — source reconciliation | **Resolved.** The source remains ready until its admission fence closes, then held through its obligations. |

+| A2-4 — missed termination events | **Resolved.** Missing evidence explicitly prevents automatic recovery. The new operator fallback introduces A3-1 below. |

+| A2-5 — continuous-sync deadline | **Partly resolved.** Modification events and a fixed deadline cover open files. However, an unstable file may wait until “the scan,” and a failed watch triggers only one immediate scan. Subsequent writes can therefore wait ten minutes. Require deadline-driven publication or polling while watch coverage is missing. |

+| A2-6 — manifest permissions | **Resolved.** Immutable objects and replaceable manifests are distinguished. The new enforcement explanation has a separate defect, included in A3-3. |

+| A2-7 — permanently failing probe | **Partly resolved.** A deadline, replacement path and bounded `stuck` state now exist. Preservation of the failed target’s writes remains incomplete: A3-2. |

+| A1-1 residual — legacy identity binding | **Partly resolved.** The operator’s tofu check establishes the intended mapping, but the resulting bind object lacks an enforced operator-only writer: A3-3. |

+| A1-7 residual — wake state | **Resolved.** Continuous publication and restoration now include `NextDue` and `Replication` alongside timer rows. |

+Reviewed `b3821864` against claim rev 6.3 (`8faa89a4`), moves rev 7.6 (`29245f69`) and the nearest-region implementation. H1–H6 remain fixed.

+1. **A3-1 — P1 — §5.9: a CloudTrail termination request is not compute-fencing evidence.** [Location](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/region-ha/docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md:590)

+ **Problem:** The new operator fallback checks a `TerminateInstances` record. That proves an API request occurred, not that execution stopped. Even a successful response can report `shutting-down`; AWS explicitly documents that termination can remain in that state. [AWS API reference](https://docs.aws.amazon.com/AWSEC2/latest/APIReference/API_TerminateInstances.html).

+ **Failing sequence:** A termination request is accepted while the old executor is still shutting down and running its app. No terminal observation is available. The operator resolves using the CloudTrail request, and the placer starts a replacement before the old process stops.

+ **Fix:** Retain claim §7.2’s requirement for verified compute fencing. CloudTrail may help locate the request, but must not substitute for terminal-state evidence. If no qualifying evidence exists, remain `awaiting-evidence`. Reflect this explicitly in K3.

+2. **A3-2 — P1 — §5.8: live probe-failure replacement skips the target’s durability barrier.** [Location](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/region-ha/docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md:528)

+ **Problem:** The new transition obtains stop evidence and resumes at `pinning`, promising to preserve probe writes. Claim §6.1’s stop evidence proves that processes and replicators stopped; it does not establish the final replicated position or file-manifest sequence. The original source’s `flushed` journal entry cannot establish those values for the failed target’s generation.

+ **Failing sequence:** A drains to B. During its probe, B creates an application file on a `snapshot` plan, then fails readiness. B produces stop evidence before the next snapshot. The placer pins B’s existing manifest and installs C. C lacks the file even though B remained alive and its data could have been transferred.

+ **Fix:** Give `probe-failed` a journaled target-release sequence: close admission, drain, flush the database and **all** file mutations regardless of plan, persist B’s final replication position and manifest sequence, then permit pinning. Require the pin to reach those values. Add this contract to K2 and K8.

+3. **A3-3 — P1 — §§5.1 and 6: the new legacy bind object does not authenticate operator approval.** [Location](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/region-ha/docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md:201)

+ **Problem:** `bound_by.operator` and `tofu_instance_id` are ordinary JSON fields. The spec does not restrict bind creation to an operator principal or require a verifiable operator signature. Section 6 includes binds in the writable `control/boxes/` namespace, while the existing box policy permits writes throughout the deployment bucket. Create-only publication authenticates neither the first writer nor the claimed tofu check.

+ **Failing sequence:** Before the legitimate bind exists, a writer using box credentials publishes a legacy-label record containing a valid identity document for another, terminated instance, plus a fabricated `.bind.json`. Readers accept the purported operator binding. Genuine termination evidence for that other instance then authorizes replacement of the still-running legacy executor.

+ **Fix:** Make the bind namespace writable only by explicitly authorized operator principals, and bind the attestation to the exact box record. Prevent replacement or deletion that would permit rebinding. Also correct §6’s assertion that S3 cannot enforce conditional headers: AWS supports `s3:if-match` and `s3:if-none-match` policy conditions. Enforce the stated immutability in storage, alongside application checks. [AWS conditional-write enforcement](https://docs.aws.amazon.com/AmazonS3/latest/userguide/conditional-writes-enforce.html).

+4. **A3-4 — P3 — §§1, 4 and 5.4: one cited path is absent and two line anchors need correction.** [Location](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/region-ha/docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md:158)

+ **Problem and failing sequence:** Following `internal/edge/fleetbind.go` fails because that file does not exist. `homemap.go:529` reaches a role-filtering comment; `reconcile.go:179` states the intended single-box invariant rather than demonstrating the missing enforcement.

+ **Fix:** Cite:

+ - `internal/host/fleetbind.go` for binding publication and `internal/edge/edge.go:2432` for per-request fallback.

+ - `internal/edge/homemap.go:538` or `:582` for home-map folding and collision selection.

+ - `internal/provision/reconcile.go:335` and the admission call sites at `:799` and `:936` for region-based admission.

+All code citations were checked against the requested tree. The simulation packages are in the referenced moves worktree, not this commit. No files were changed or tests run.

+**Verdict: not ready.**

\ No newline at end of file

diff --git a/docs/superpowers/specs/CODEX-REVIEW-BRIEF-REGION-HA-4.md b/docs/superpowers/specs/CODEX-REVIEW-BRIEF-REGION-HA-4.md

new file mode 100644

index 000000000..4bdcdbfc0

--- /dev/null

+++ b/docs/superpowers/specs/CODEX-REVIEW-BRIEF-REGION-HA-4.md

@@ -0,0 +1,65 @@

+# Review brief: region HA spec 1 (box placement), round 4

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

+This is rev 4, answering rounds 1 to 3 (`CODEX-FINDINGS-REGION-HA-1.md`

+to `-3.md`). First give a disposition table for each round 3 finding

+(A3-1 to A3-4) and the A2-5, A2-7 and A1-1 residuals: resolved, partly

+resolved (say what is left), or not resolved. Then report only **new**

+findings, including any that rev 4's fixes introduce: the release

+sequence (§5.8), the bind and the `control/boxes/` bucket policy (§5.1),

+polling while watch coverage is missing (§5.6), and the S3 conditional

+policies (§6). Don't re-raise anything a previous round's disposition

+marked resolved unless rev 4 broke it.