amadan
spec: region HA spec 1 rev 2, answering Astra round 1 (A1-1 to A1-13)
Box records bound by the AWS-signed identity document, relocation phases with a pinned recovery set and a no-reinstall boundary, an ordered files manifest, replicated timer state, the termination queue, and the multi-box gate. K10 and K11 added.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2 files changed,
+494
−204
docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md+431 −204docs/superpowers/specs/CODEX-REVIEW-BRIEF-REGION-HA-2.md+63 −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 6feb48a85..a8c9aba6f 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,6 +1,10 @@ |
| # Region HA, spec 1: placing an instance on a box |
| -Design, 2026-10-04, **rev 1**. DRAFT. Nothing here is built. |
| +Design, 2026-10-04, **rev 2**. 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. |
| This is the first of four specs that give each region high availability |
| and autoscaling: |
| @@ -30,7 +34,7 @@ has. |
| | # | Ruling | |
| |---|---| |
| -| H1 | **The proof that a box is dead is that AWS terminated it.** Each region's boxes run in an Auto Scaling group with health checks. When the group terminates an unhealthy box, a region placer that has only read-only EC2 and Auto Scaling rights sees `terminated` and re-places the box's instances. The console still holds no EC2 rights. This replaces M16 / claim §7.2's operator-only declare-lost **for terminated boxes only**; a `stopped` box stays manual. It also replaces fleets D7's "no automatic reaper" for platform boxes. Lease expiry is still never proof (CC5). | |
| +| H1 | **The proof that a box is dead is that AWS terminated it.** Each region's boxes run in an Auto Scaling group with health checks. When the group terminates an unhealthy box, a region placer that has only read-only AWS rights sees `terminated` and re-places the box's instances. The console still holds no EC2 rights. This replaces M16 / claim §7.2's operator-only declare-lost **for terminated boxes only**; a `stopped` box stays manual. It also replaces fleets D7's "no automatic reaper" for platform boxes. Lease expiry is still never proof (CC5). | |
| | H2 | **Shape the claim now.** The HA specs cite the claim rather than invent a second primitive, and send the claim and moves sessions the exact changes they need (§9) before those specs are finalised on a one-box-per-region assumption. | |
| | H3 | **About one second of data loss, written down.** Litestream keeps shipping asynchronously. Writes that had not reached S3 when a box died are lost, and the docs and console say so. | |
| | H4 | **Placement policy: capacity plus soft spread.** Among eligible boxes, choose the one with the most headroom. Prefer a box that runs no other instance of the same app, but never refuse placement for that reason. If no box is eligible, the instance waits as `unplaced` and an operator is alerted. (Spec 2.) | |
| @@ -62,7 +66,7 @@ box" (`reconcile.go:179`). |
| A second box in a region would break three things: |
| 1. **Both boxes run the instance's route.** The S3 lease (`lock.json`, |
| - 15-minute TTL, `internal/lease/lease.go:38`) stops them running at |
| + 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`), |
| @@ -79,61 +83,75 @@ back the same machine, if it can (`infra/modules/region-host/main.tf:497`). |
| - **Box**: one platform host machine. Not a customer fleet box; fleets |
| keep their own mechanism and are out of scope. |
| -- **Box id**: the box's EC2 instance id (`status.InstanceID()`, |
| - `internal/status/instanceid.go:37`). Instance ids are never reused, so |
| - a box id names one machine for ever. Boxes that predate this spec keep |
| - their label (`status.Label(machine-id)`) and publish their instance id |
| - beside it (§5.1). |
| +- **Box id**: the name the claim uses for a box. For a box launched by |
| + an Auto Scaling group it is its EC2 instance id |
| + (`status.InstanceID()`, `internal/status/instanceid.go:37`), which AWS |
| + never reuses. A box that predates this spec keeps its label |
| + (`status.Label(machine-id)`). Either way the id is bound to one AWS |
| + instance by a **box record** (§5.1), never by an edges file. |
| - **Executor**: the one box the claim's `op.exec` names for a host. |
| -- **Eligible box**: a box that is fresh (nearest-region F1), reachable, |
| - hosting, serves the instance's pool, accepts inbound, holds the secrets |
| - key (R9), is not draining, and is not on the claim's `lost` list. |
| +- **Relocatable host**: an exec-backed instance or a sidecar, whose whole |
| + start state is in S3 or rendered from its record (HA5). Unit- and |
| + socket-backed routes (the console, platform services) are **not** |
| + relocatable: their unit definitions live outside the record. They stay |
| + on their box, as today (A1-8). |
| +- **Eligible box**: a box with a verified box record (§5.1) that is fresh |
| + (nearest-region F1), reachable, hosting, serves the instance's pool, |
| + accepts inbound, holds the secrets key (R9), publishes the HA |
| + capability (§8), is not draining, and is not on the claim's `lost` list. |
| - **Region placer**: one box per region, chosen by the existing lease |
| - election, that runs re-placement (spec 3) and drain (spec 4). Its |
| - election lease only decides who acts, never what is true. |
| + election, that runs relocation recovery, failover (spec 3) and drain |
| + (spec 4). Its election lease only decides who acts, never what is true. |
| - **Relocation**: changing a host's executor to another box **in the |
| - same region**. A move changes region; relocation does not. |
| + same region** (§5.8). A move changes region; relocation does not. |
| ## 3. Invariants |
| -**HA1. The claim names the executor.** A home-run host (exec, unit, |
| -socket, sidecar) runs only on the box its claim's `op.exec` names. This is |
| -claim C4 unchanged. What changes is that `op.exec` may now name any |
| -eligible box in the record's region, not "the region's box". |
| +**HA1. The claim names the executor.** A relocatable host runs only on |
| +the box its claim's `op.exec` names. This is claim C4 unchanged. What |
| +changes is that `op.exec` may now name any eligible box in the record's |
| +region, not "the region's box". |
| -**HA2. Region equality never admits.** Reconcile, the activator, config |
| -sync, release adoption and timers act for a host only on its executor. |
| -Being in the right region is necessary, never sufficient (claim C4 says |
| -this already; today's code does not do it). |
| +**HA2. Region equality never admits.** The activator, config sync, |
| +release adoption and timers act for a host only on its executor, or on a |
| +participant in the phase that permits it (§5.8). Being in the right |
| +region is necessary, never sufficient (claim C4 says this already; |
| +today's code does not do it). |
| -**HA3. A local copy is trusted only under the current installation.** A |
| -box may skip restore and serve its local database and files only when its |
| -local stamp record has `active_stamp == holder.stamp` from a fresh claim |
| -read (claim §6.4). Otherwise it restores from S3. This replaces the |
| -one-box warm-cache argument. |
| +**HA3. A local copy is trusted only if it is the current installation, |
| +completely installed.** Authority (`active_stamp`, claim §6.4) and |
| +evidence (an installation-complete marker, §5.5) are separate. A box |
| +skips restore only when both match the claim's `holder.stamp` and |
| +`holder.generation`. |
| **HA4. Edges follow the newest installation.** When two edges files claim |
| one host, the edge believes the one carrying the higher `holder.stamp`. |
| Stamps only increase (claim `gen`), so a dead box's stale file always |
| loses to its successor's, with no liveness rule. |
| -**HA5. Everything an instance needs to start is in S3.** The database, |
| -its files directory and its env file are under the incarnation's |
| -`holder.location`, or are rendered from the record (config, release). |
| -Nothing needed to start an instance lives only on the box running it. |
| +**HA5. Everything a relocatable host needs to start is in S3.** The |
| +database, files directory, env files and timer state are under the |
| +incarnation's `holder.location` in the current generation, or are |
| +rendered from the record (config, release). Nothing needed to start it |
| +lives only on the box running it. |
| **HA6. The executor changes only by a claim operation.** Create, a move, |
| -a relocation (§5.8). Each changes `op.exec` in a CAS that cites stop |
| -evidence (claim §6.1) or a termination fence (§5.9), and installs a new |
| -generation with a new stamp. |
| +or a relocation (§5.8). Each changes `op.exec` in a CAS that cites stop |
| +evidence (claim §6.1) or a termination fence (§5.9), and makes a fully |
| +populated new generation current with a new stamp. |
| + |
| +**HA7. Termination evidence is bound to the executor.** A fence counts |
| +only if the terminated instance is the one the executor's box record |
| +names, in the deployment's own account and the region's own AWS region |
| +(A1-1). |
| ## 4. What stays the same |
| - A region with one box behaves exactly as today, and every new rule |
| holds trivially there. |
| - Static sites and public addr routes still run on every box |
| - (`everywhereClass`, `reconcile.go:195`). Only home-run hosts gain an |
| - executor. |
| + (`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`). |
| - The ingress model: any edge serves any app and backhauls home-run |
| @@ -143,36 +161,66 @@ generation with a new stamp. |
| ## 5. Design |
| -### 5.1 Box identity and evidence |
| +### 5.1 Box identity, box records and evidence |
| + |
| +**The box record (A1-1).** Before a box may be named by any claim in a |
| +multi-box region, it writes, create-only: |
| + |
| + control/boxes/<box id>.json |
| + |
| +```json |
| +{ |
| + "v": 1, |
| + "box": "i-0abc…", |
| + "identity_document": "<base64 IMDS instance identity document>", |
| + "identity_signature": "<base64 PKCS7 signature from IMDS>", |
| + "written_at": "<RFC3339>" |
| +} |
| +``` |
| -Each box's edges file (`internal/host/edgesfile.go:157`) gains: |
| +- The identity document is AWS-signed and names `accountId`, `region` |
| + and `instanceId`. Every reader verifies the signature against AWS's |
| + 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. |
| +- 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. |
| + |
| +**Edges file fields.** Each box's edges file |
| +(`internal/host/edgesfile.go:157`) gains: |
| ```json |
| { |
| "box_id": "i-0abc…", |
| + "capabilities": ["region-ha-1"], |
| "draining": false, |
| "headroom": { "mem_free_mib": 2210, "disk_free_mib": 31200, "awake": 14 } |
| } |
| ``` |
| -- `box_id` is the EC2 instance id from IMDS, or the label on a machine |
| - with no IMDS (dev, Pi). A box launched by an Auto Scaling group uses its |
| - instance id as its label too, so the two are the same. |
| -- `draining` is set by the placer through the box (spec 4), and an |
| - eligible-box check refuses a draining box. |
| +- `box_id` must equal the box record's id; a mismatch makes the box |
| + ineligible. The edges file is evidence of liveness and configuration, |
| + never of identity. |
| +- `capabilities` gates multi-box admission (§8). |
| +- `draining` is set through the box by the placer (spec 4). |
| - `headroom` is the input to spec 2's choice. Spec 1 publishes it only. |
| The console already reads these files with freshness |
| (`internal/console/instancesplacement.go:93`). Nearest-region's |
| `regioncandidates.go` keeps deciding which **regions** are eligible. |
| -This spec adds `eligibleBoxes(snapshot, region, pool)`, which returns |
| -the boxes, applying the same predicate one box at a time (nearest-region |
| -`TestEligibilityNeverCombinesBoxes`). |
| +This spec adds `eligibleBoxes(snapshot, boxRecords, region, pool)`, |
| +which returns the boxes, applying the predicate one box at a time |
| +(nearest-region `TestEligibilityNeverCombinesBoxes`). |
| ### 5.2 Create names a box |
| Claim §5.1 step 4 becomes: CAS `op` to `serving` and set `exec` to |
| -`choose(eligibleBoxes(region, pool), app)`. |
| +`choose(eligibleBoxes(region, pool), app)` (K1). |
| - Until spec 2 lands, `choose` is: the eligible box running the fewest |
| claimed hosts, preferring one that runs no other instance of the app, |
| @@ -184,49 +232,79 @@ Claim §5.1 step 4 becomes: CAS `op` to `serving` and set `exec` to |
| - The choice is recorded only in the claim. The record keeps `Region` |
| and gains no box field, so a record still describes residency, not |
| placement. |
| +- A move into a multi-box region chooses its target box the same way, |
| + in its start CAS (K10). |
| -### 5.3 Reconcile admits only on the executor |
| - |
| -`inScope` (`reconcile.go:335`) keeps its pool and region test, and for |
| -home-run classes adds a fresh claim read: mint or keep the row only if |
| -`op.exec` names this box (claim C4, "reconcile's decision to create or |
| -keep a row"). |
| - |
| -- The safety gate is the activator's fresh claim read at every spawn |
| - (claim C4), not reconcile. So reconcile reads a host's claim only when |
| - it would **create** a row, and re-checks the rows it keeps on a slow |
| - sweep (every 10 minutes). Reading every claim on every pass would cost |
| - real money: 2,000 hosts every 30 seconds is about 5.8 million GETs, or |
| - about $2.30, a day per box. |
| -- A relocation tells both boxes directly: the placer bumps the region's |
| - control serial after each executor CAS, so reconcile runs at once and |
| - re-reads the claims of hosts it holds or would create. |
| -- A claim read error keeps an existing row and creates none (claim C6). |
| - A box that cannot read claims keeps serving what it already serves. |
| -- A row whose claim names another box is released through the claim's |
| - stale-hold rule (claim §8, CC10), never by deleting local state: |
| - retirement is the operation's job (§5.8). |
| +### 5.3 Reconcile: executing rows, held rows, former rows |
| + |
| +Reconcile distinguishes three cases for a relocatable host in its region |
| +(A1-6). Each is decided by a fresh claim read. |
| + |
| +| 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 | |
| + |
| +- Dropping a former executor's row is a registry change only. It never |
| + touches local files: that is the operation's `park-local` obligation |
| + (§5.8 step 6) under the host guard. This is a new rule (K11), separate |
| + from the stale-hold rule (claim §8, CC10), which only reopens a hold on |
| + the current executor. |
| +- **When reconcile reads claims.** The safety gate is the activator's |
| + fresh claim read at every spawn (claim C4), not reconcile. So |
| + reconcile reads a host's claim when it would mint a row, and re-checks |
| + the rows it keeps on a slow sweep, every 10 minutes. This is a stated |
| + exception to C4's "reconcile's decision to keep a row" (K11): a kept |
| + row that is stale for up to 10 minutes can route a request to this box, |
| + where the activator refuses to spawn. Reading every claim on every |
| + pass would cost about $2.30 a day per box at 2,000 hosts on 30-second |
| + passes. |
| +- **Prompt changes.** The placer bumps the region's control serial after |
| + each executor CAS, so both boxes reconcile at once and re-read the |
| + claims of the hosts they hold or would mint. |
| +- A claim read error keeps an existing row and mints none (claim C6). |
| ### 5.4 Edges and the home map |
| -- The edges-file writer (`edgesfile.go:185`) publishes a host as `home` |
| - only when this box is its executor, and adds the installation's stamp: |
| +- The edges-file pass (`edgesFilePass`, `edgesfile.go:272`) publishes a |
| + 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 higher stamp (HA4). Equal stamps can only come from two legacy files |
| - with no stamp; those keep today's sorted rule, and an alert fires |
| - because it means two boxes are serving one host. |
| + 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 |
| + publishes stamps, and an unstamped entry for a host that some file |
| + carries stamped is ignored. Two unstamped entries keep today's sorted |
| + rule and alert, because they mean the gate was bypassed (A1-9). |
| - The edge never reads claims on the request path. |
| ### 5.5 The activator's local copy |
| -The warm-cache path (`activator.go:1127`, `backend_exec.go:265`) checks |
| -HA3 before trusting a local database: under the host guard, it reads |
| -the claim fresh, compares `holder.stamp` with the box's `active_stamp`, |
| -and restores from S3 on any mismatch, including a missing local record. |
| -The comment's one-box argument is replaced with HA3. |
| +**The installation-complete marker (A1-5).** After a box has made an |
| +installation's data durable (database restored and fsynced, files |
| +applied to the manifest's sequence, timers imported), and only then, it |
| +writes and fsyncs: |
| + |
| + <DataDir>/.installed/<host>.json |
| + {"incarnation": "…", "generation": "…", "stamp": 41, |
| + "db_marker": "<the moves generation marker>", "files_seq": 1882} |
| + |
| +The warm-cache path (`activator.go:1127`, `backend_exec.go:265`) skips |
| +restore only when, under the host guard and against a fresh claim read: |
| -### 5.6 Files reach S3 continuously or by snapshot |
| +- the local stamp record's `active_stamp == holder.stamp` (authority); |
| +- the marker's `incarnation`, `generation` and `stamp` match the claim, |
| + and its `db_marker` matches the database's generation marker |
| + (evidence). |
| + |
| +Anything else, including a missing marker, restores from S3. A box that |
| +crashes mid-install therefore has authority and no evidence, and |
| +restores. Retirement (claim §6.3) parks the marker with the rest of the |
| +host's local state. The comment's one-box argument is replaced with HA3. |
| + |
| +### 5.6 Host files reach S3, in order |
| Moves carry the files directory (F4) and `<host>.env` (F6) as a sealed |
| archive taken from the live source (moves §6.1, §8). A dead source can't |
| @@ -234,151 +312,275 @@ produce one, so HA5 needs them in S3 already. |
| **The setting.** An app's manifest gains `files_durability`: |
| -- `continuous`: each changed file is uploaded within about one second of |
| - its last write (debounced on close and rename, via inotify on the |
| - host's directory, with a full listing every 10 minutes to catch |
| - anything a watch missed); |
| -- `snapshot`: a sealed archive of the whole directory every |
| +- `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); |
| +- `snapshot`: the whole directory is published every |
| `files_snapshot_interval`, default 15 minutes. |
| -Carloku maps its plans to this (H6). The default for an app with no |
| -setting is `snapshot`. |
| +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` and `<host>.env`. They are small and rarely change, and |
| -losing them is what kept kpmg down for 1h54m (moves §1.2). |
| - |
| -**Where.** Under the incarnation's own location, inside the current |
| -generation (claim C3a, moves §5.1): |
| - |
| - <holder.location>/files/<generation>/<relative path> (continuous) |
| - <holder.location>/files/<generation>/snapshots/<seq>.tar (snapshot) |
| - |
| -Both buckets are versioned, so a restore names exact versions (claim C3). |
| -A delete in the files directory is uploaded as a tombstone object, not |
| -an S3 delete. |
| - |
| -**Restore.** A box that becomes executor restores the database, then the |
| -files: the latest snapshot, then any continuous objects newer than it. |
| -The files and the database can disagree by up to the snapshot interval |
| -on a `snapshot` app, and the console says so on the app's Overview. |
| - |
| -**Moves.** A move keeps its sealed archive at the cut (moves §8). The |
| -continuous objects are an addition, not a replacement, so moves is |
| -unchanged. |
| - |
| -**Sidecars.** `<host>-sidecar.env` (F8) is treated like `<host>.env`. |
| -Moves refuses sidecar apps (M10); relocation (§5.8) does not need to, |
| -because nothing crosses a region. |
| +`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 |
| +1h54m (moves §1.2). |
| + |
| +**Ordering (A1-4).** Object versions do not say which update wins, so |
| +nothing is ever overwritten and one manifest decides. |
| + |
| +- **Objects are immutable.** Each upload goes to a new key, |
| + `<holder.location>/files/<generation>/objects/<seq>-<sha256>`, written |
| + create-only. A stalled upload that completes late creates an object no |
| + manifest names. |
| +- **One sequence per host.** The executor numbers every local mutation |
| + (write, rename, delete) with a monotonically increasing `seq`, kept |
| + under the host guard and recovered from the manifest on restart. |
| +- **The manifest** is one object, |
| + `<holder.location>/files/<generation>/manifest.json`, replaced only |
| + with `If-Match`: |
| + `{"seq": 1882, "base": "snapshots/0004.tar", "base_seq": 1700, |
| + "entries": {"<path>": {"object": "objects/1881-…", "seq": 1881} | |
| + {"deleted": true, "seq": 1874}}}`. |
| + A delete is a tombstone entry, never an S3 delete. The manifest is |
| + published only after every object it names is durable, and its `seq` |
| + only increases, so a late manifest write fails its `If-Match`. |
| +- **Snapshots** are sealed archives taken at a mutation boundary: the |
| + executor records `base_seq` before reading the directory, and |
| + mutations after `base_seq` go in `entries`. A snapshot becomes the |
| + base only through a manifest CAS. Older snapshots and unnamed objects |
| + are reaped after a day. |
| +- **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). |
| + |
| +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 |
| +Overview. |
| + |
| +**Moves.** A move keeps its sealed archive at the cut (moves §8), and |
| +installs a fresh manifest in its new generation (K8). |
| ### 5.7 What a new executor rebuilds |
| | State | How the new box gets it | |
| |---|---| |
| -| Database | restore from `holder.location`, current generation | |
| -| Files directory, env files | §5.6 | |
| +| 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) | |
| | `<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) | |
| -| Timers (`next_due`) | recomputed from the schedule at the first reconcile. A tick due during the gap runs once on the new box; a tick that ran on the dead box but whose result was not replicated may run again. Ticks are documented as at-least-once. | |
| | Certificates | the cert mirror's boot refresh (on main) | |
| -| Registry row | reconcile, once the claim names this box | |
| +| 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) | |
| -### 5.8 Relocation: the one operation that changes the box |
| - |
| -A new claim op kind, `relocating`, from `serving` only, same region only. |
| -Its intent names `{from, to, reason}`, where reason is `drain`, |
| +**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 |
| +therefore in S3 within about a second of the app being told it |
| +succeeded. On install the new box imports them with |
| +`ReplaceTimers`, preserving `next_at`, `due_at`, `attempts` and |
| +`registration`. |
| + |
| +- An occurrence that fell due while the host had no executor fires once |
| + when the new executor imports it: the converger catches up from the |
| + imported `next_at`, not from `Next(now)`. |
| +- A delivery that ran on the dead box but whose bookkeeping did not reach |
| + S3 runs again. Ticks are documented as **at-least-once** (open |
| + question 1). |
| + |
| +### 5.8 Relocation |
| + |
| +A new claim op kind, `relocating` (K2), from `serving` only, for a |
| +relocatable host, within one region. Its intent names |
| +`{from, to, reason, generation_from}`, where reason is `drain`, |
| `rebalance` or `failover`. |
| -1. **Start CAS:** `op = {relocating, id, intent, exec: from, participants: |
| - [from, to]}` (or `participants: [to]` for failover). Both write |
| - execution leases (claim §7.1) before leaving the first phase. |
| -2. **Release the source**, by one of: |
| - - **stop evidence** from `from` (claim §6.1), after a final |
| - replication flush, for drain and rebalance; or |
| - - a **termination fence** (§5.9), for failover. |
| -3. **Install on the target.** CAS `exec: to` with a new |
| - `holder.generation` and `holder.stamp` (claim §6.4). Late writes from |
| - the old installation land in the old generation, which nothing |
| - admitted reads (claim C3a, within one incarnation per moves §5.1). |
| -4. **Target restores** (§5.7), takes the replica lease, and the host goes |
| - back to `serving` once the target's probe passes (moves §7.7's probe, |
| - same region). |
| -5. **Source parks** its local state with `retire-installation` (claim |
| - §6.4), as a `park-local` obligation on `from`. A terminated box has no |
| - disk; the fence removes that obligation (claim §7.2's second case). |
| - |
| -**Recovery owner:** the region placer, from `intent`. It is a box, not |
| -the console, because failover must work when the console's box is the |
| -one that died. |
| +**Phases (A1-3).** Each is a claim CAS, conditional on `op.id` and the |
| +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 | |
| +|---|---|---|---|---| |
| +| `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` | |
| + |
| +**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. |
| +- **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. |
| + |
| +**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 |
| +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 |
| +installation land in `generation_from`, which nothing admitted reads |
| +again (claim C3a within one incarnation, moves §5.1). |
| + |
| +**The no-reinstall boundary (A1-3).** Once the `installed` CAS succeeds: |
| + |
| +- nobody restores `G'` again: replay from `installed` or `probing` goes |
| + forward (probe, then `serving`), never back to `installing`; |
| +- `to` writes its installation-complete marker (§5.5) before its probe |
| + spawns; |
| +- a worker that paused before `installed` and resumes revalidates the |
| + phase under the host guard and stops. |
| + |
| +Replay from `installing` (before `installed`) discards `to`'s partial |
| +local state (retire-artifacts, claim §6.4) and installs again from the |
| +same pinned set. Nothing has served from `G'` yet, so nothing is lost. |
| + |
| +**Exclusion.** Only `to` installs, holding the replica lease on `G'`; |
| +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 |
| +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. |
| **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). |
| ### 5.9 The termination fence |
| -A termination fence is a JSON object written into the operation's |
| -journal: |
| +A termination fence is written into the operation's journal: |
| ```json |
| -{"box": "i-0abc…", "state": "terminated", |
| - "observed_at": "<RFC3339>", "via": "ec2:DescribeInstances", "region": "eu-west-1"} |
| +{"box": "i-0abc…", "instance_id": "i-0abc…", "account": "123…", |
| + "aws_region": "eu-west-1", "state": "terminated", |
| + "observed_at": "<RFC3339>", "via": "describe" | "event", |
| + "event_id": "<EventBridge event id, when via=event>"} |
| ``` |
| -- Only `terminated` counts. `stopped` and `stopping` do not, because a |
| - stopped box can start again with its disk. A stopped box still needs |
| - the operator's `carlos ops host resolve --declare-lost` (claim §7.2). |
| -- The placer reads the state itself with its own read-only credentials |
| - (§6). It never trusts a box's own report, an edges file, or the Auto |
| - Scaling group's lifecycle event alone; the event only wakes it. |
| +**What counts (A1-1, A1-11).** |
| + |
| +- `instance_id`, `account` and `aws_region` must equal the executor's |
| + verified box record (§5.1, HA7). |
| +- Only `terminated`. `stopped` and `stopping` do not, because a stopped |
| + box can start again with its disk; those need the operator's |
| + `carlos ops host resolve --declare-lost` (claim §7.2). |
| +- A missing instance, `InvalidInstanceID.NotFound`, an API error, or a |
| + lookup in another account or region is **never** evidence. AWS keeps a |
| + terminated instance visible in `DescribeInstances` for typically under |
| + an hour, so absence proves nothing. |
| + |
| +**Two ways to observe it.** |
| + |
| +1. **The durable event.** An EventBridge rule in each region sends EC2 |
| + "Instance State-change Notification" events with `state: terminated` |
| + for the deployment's account to an SQS queue (14-day retention). The |
| + queue's policy accepts messages only from that rule's ARN. The placer |
| + reads the queue; an event whose `account`, `region` and instance id |
| + match a box record is evidence, `via: "event"`. |
| +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`. |
| + |
| +- 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. |
| - A terminated instance cannot run again, so a terminated box needs no |
| - quarantine or `--readmit`. Its id goes on `lost` anyway, so a forged or |
| - confused file naming it is refused. |
| + quarantine or `--readmit`. Its id still goes on `lost`, so any later |
| + file naming it is refused. |
| - The root volume must have `DeleteOnTermination`, so no disk outlives the |
| box (§6). |
| -- Late requests: once EC2 reports `terminated`, the machine sends |
| - nothing more. A request S3 had already accepted may still complete for |
| - a few seconds. It lands in the old generation (§5.8 step 3) and counts |
| - toward the H3 loss window. |
| - |
| -## 6. Infrastructure and IAM |
| - |
| -- Each box's role gains `ec2:DescribeInstances` and |
| - `autoscaling:DescribeAutoScalingGroups`, conditioned on its own region |
| - and the deployment's tag. No `ec2:Stop*`, `Terminate*` or `Modify*`. |
| - The console's role is unchanged (no EC2 rights). |
| -- Boxes need `s3:PutObject` and `s3:GetObjectVersion` on |
| - `instances/<host>/*/files/` in their region's data bucket (§5.6), and |
| - the claim CAS rights the claim spec already lists. |
| -- The `region-host` module gains `delete_on_termination = true` on the |
| - root volume. Moving to an Auto Scaling group is spec 4; spec 1 runs on |
| - today's fixed boxes and on a second fixed box added by hand. |
| + |
| +## 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 |
| + 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. |
| +- **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. |
| +- **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 |
| + a second fixed box added by hand. |
| ## 7. Failure modes |
| | What happens | Result | |
| |---|---| |
| | Executor box dies, region has another box | spec 3 relocates its hosts after the termination fence. Until then: requests 503 with Retry-After. | |
| -| Executor dies, region had one box | the Auto Scaling group launches a replacement; it wins the placer election, sees the old box terminated, and relocates every host to itself. | |
| +| Executor dies, region had one box | the Auto Scaling group launches a replacement; it wins the placer election, reads the termination event from the queue, and relocates every host to itself. | |
| | Box partitioned from the control bucket | it keeps serving what it serves (no execution lease while `serving`, claim §7.1). It can't take new work. The group's health check decides whether it is terminated. | |
| | Box alive but failing its health check | the group terminates it, then as above. Instances that were healthy lose up to H3's window. | |
| -| Two files claim a host | the higher stamp wins (HA4). Equal stamps alert. | |
| -| Claim read fails on reconcile | keep existing rows, create none (C6). | |
| +| 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). | |
| +| 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. | |
| -| Placer box dies mid-relocation | the next elected placer replays from `intent` (§5.8). | |
| +| A unit- or socket-backed route's box dies | not relocated (A1-8). It comes back with its box, or by the HA ladder's restore runbook, as today. | |
| -## 8. Rollout |
| +## 8. Rollout (A1-9) |
| 1. **Prerequisite:** the claim and its floor are live (claim §10), and |
| every host in the region has a claim (adopted under claim §9). |
| -2. Ship §5.1 to §5.7 dormant behind `CARLOS_REGION_HA`. With one box per |
| - region, every rule is a no-op; ship it to all four regions and watch. |
| -3. **A second box may join a region only when every home-run host there |
| - has a claim** (§9, K5). The join check is in `carlos system` and in the |
| - console's box list. |
| +2. Ship §5 dormant behind `CARLOS_REGION_HA`, with capability |
| + `region-ha-1` published in each box's edges file once enabled. With one |
| + box per region, every rule is a no-op; ship it to all four regions and |
| + watch. |
| +3. **The multi-box gate.** A second box may join a region only when: |
| + - every relocatable host there has a claim (K5); |
| + - every box in the region, and every edge in the deployment, publishes |
| + `region-ha-1` and runs at or above the HA floor; |
| + - every box in the region has a verified box record; |
| + - the region's termination queue exists. |
| + |
| + The HA floor joins the protocol floor (claim §10): every path that |
| + restores an executable (system apply, rollback, boot recovery from |
| + `carlos.prev`) refuses a binary below it once a region has two boxes. |
| + The gate is checked in `carlos system`, in the console's box list, and |
| + by each box at start: a box that finds a second box in its region |
| + without the gate satisfied refuses to mint relocatable rows and |
| + alerts. |
| 4. Rehearse on dev with two fixed boxes: create spreads across both; |
| - drain one (§5.8) with `moveprobe` shaped like ips (moves §14.4); |
| - terminate one by hand and run the spec 3 placer manually. |
| + drain one (§5.8) with `moveprobe` shaped like ips (moves §14.4), |
| + including timers and a `continuous` files app; terminate one by hand |
| + and run the spec 3 placer manually. |
| 5. Then specs 2, 3, 4. |
| ## 9. Changes requested of the claim and moves specs |
| @@ -388,52 +590,77 @@ those specs finalise a one-box-per-region assumption. |
| | # | Spec | Change | |
| |---|---|---| |
| -| K1 | claim §5.1 step 4 | `exec` is the box `choose()` returns 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`, recovery owner the region placer. Excludes moves and placements, as `placing` does. | |
| -| K3 | claim §7.2, CC5 | A **termination fence** (§5.9) is a lost-box fence, written automatically by the region placer. `terminated` only; `stopped` stays operator-only. No `--readmit` needed for a terminated box; it still goes on `lost`. | |
| +| 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. | |
| +| 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; a second box joins only after (§8 step 3). | |
| -| K6 | claim §2 | Box names in `op.exec`, `participants`, `touched.boxes`, `inventory` and `lost` are box ids (§2); legacy labels stay valid. | |
| +| 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 | The restore contract includes `files/<generation>/` (§5.6). F4 and F6 are also carried continuously; 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 mid-relocation, a stale edges file, a stale warm copy, late PUTs after termination. | |
| +| 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. | |
| +| 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. | |
| ## 10. Testing |
| -- **Unit:** `eligibleBoxes` (one box at a time, staleness, draining, |
| - `lost`); `choose` (spread, ties); home-map stamp resolution; HA3 |
| - restore decision; files tombstones and restore order. |
| +- **Unit:** box record verification (signature, account, region, |
| + `box id == instanceId`, legacy binding); `eligibleBoxes` (one box at a |
| + time, staleness, draining, `lost`, capability); `choose` (spread, |
| + ties); home-map stamp resolution and unstamped entries; HA3's two |
| + 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). |
| - **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; a stale |
| - local copy on the old box is not served after it becomes executor |
| - again. |
| + row; the edge backhauls to the executor; relocate by drain through |
| + every phase with a crash injected at each; a stale local copy on the |
| + old box is not served after it becomes executor again. |
| - **Joint model (K9)** decides readiness, as it does for the claim and |
| - moves. Prose rounds alone have stopped converging on this kind of |
| - protocol. |
| + moves. |
| - **Rehearsal** (§8 step 4). |
| ## 11. Open questions |
| 1. **Timers at-least-once (§5.7).** Is documenting ticks as |
| - at-least-once acceptable, or does a tick need an idempotency key |
| - carried in the claim? |
| + at-least-once acceptable, or does a delivery need an idempotency key |
| + carried in the timer state? |
| 2. **`files_durability` default.** `snapshot` for apps with no setting, |
| so existing apps pay nothing new until Carloku maps plans. Agreed? |
| 3. **The reconcile sweep (§5.3)** re-reads every kept host's claim every |
| - 10 minutes. If that's too slow to notice a stray row, spec 2 adds a |
| - per-region claim index; spec 1 doesn't. |
| + 10 minutes. A stray row is harmless (the activator refuses to spawn) |
| + but misroutes requests for up to that long. Shorter costs more GETs. |
| ## 12. Out of scope, for the later specs |
| - **Spec 2:** `headroom` thresholds, soft spread across an app's |
| instances, the `unplaced` state and its alert, rebalancing. |
| -- **Spec 3:** the placer loop: election, Auto Scaling event wake-up, |
| - the termination fence, relocating every host off a terminated box in |
| - bounded parallel, waking always-on and scheduled instances, the |
| - failover gap target. |
| +- **Spec 3:** the placer loop: election, reading the termination queue, |
| + relocating every host off a terminated box in bounded parallel, waking |
| + always-on and scheduled instances, the failover gap target. |
| - **Spec 4:** the Auto Scaling group per region, launch template and |
| join without SSM hand steps, ingress for boxes that come and go (a |
| per-region NLB with fixed EIPs, or an EIP pool claimed at boot), |
| HTTP-01 certificates, steering, scale-out on headroom, scale-in by |
| drain (§5.8), per-region minimum (H5). |
| +- **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 |
| + |
| +| Finding | Disposition | |
| +|---|---| |
| +| A1-1 P1 termination evidence not bound to identity | accepted: AWS-signed box records (§5.1), HA7, fence fields (§5.9), K6 | |
| +| A1-2 P1 new generation never populated | accepted: pinned recovery set and `installing` builds `G'` (§5.8), K8 | |
| +| A1-3 P1 replay overwrites an installation that has written | accepted: phase table, `installed` boundary, participant-terminated exits (§5.8), K2 | |
| +| A1-4 P1 file update and tombstone order | accepted: immutable objects, per-host `seq`, `If-Match` manifest, snapshot boundary (§5.6) | |
| +| A1-5 P2 `active_stamp` is not install evidence | accepted: installation-complete marker (§5.5), HA3 | |
| +| A1-6 P2 participant rows and former executors | accepted: three row cases (§5.3), K11 | |
| +| A1-7 P2 timers not reconstructible | accepted: timer state replicated continuously, imported with `ReplaceTimers`, catch-up (§5.7) | |
| +| A1-8 P2 unit and socket hosts | accepted: not relocatable (§2, §7, §12) | |
| +| A1-9 P2 adoption alone does not admit a second box | accepted: capability, HA floor and multi-box gate (§8), unstamped entries (§5.4) | |
| +| A1-10 P2 moves target box | accepted: K10 | |
| +| 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` | |
diff --git a/docs/superpowers/specs/CODEX-REVIEW-BRIEF-REGION-HA-2.md b/docs/superpowers/specs/CODEX-REVIEW-BRIEF-REGION-HA-2.md| new file mode 100644 |
| index 000000000..1603737a7 |
| --- /dev/null |
| +++ b/docs/superpowers/specs/CODEX-REVIEW-BRIEF-REGION-HA-2.md |
| @@ -0,0 +1,63 @@ |
| +# Review brief: region HA spec 1 (box placement), round 2 |
| + |
| +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.5: 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 2 |
| + |
| +This is rev 2, answering your round 1 (`CODEX-FINDINGS-REGION-HA-1.md`). |
| +First give a disposition table for each round 1 finding (A1-1 to A1-13): |
| +resolved, partly resolved (say what is left), or not resolved. Then |
| +report only **new** findings, including any that rev 2's fixes |
| +introduce: the relocation phase table (§5.8), the box record (§5.1), |
| +the files manifest (§5.6), timers (§5.7), the termination queue (§5.9) |
| +and the multi-box gate (§8) are all new mechanisms. |