amadan
spec: region HA spec 1 rev 5.4, Astra rev 5 round 4 (B4-1, B4-2)
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+48
−16
docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md+48 −16
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 b00b256eb..a28effa0a 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,16 @@ |
| # Region HA, spec 1: placing an instance on a box |
| -Design, 2026-10-06, **rev 5.3**. DRAFT. Plan 1a is built and merged |
| +Design, 2026-10-06, **rev 5.4**. DRAFT. Plan 1a is built and merged |
| (aadb860); nothing else here is built. |
| +**Rev 5.4** answers Astra's fourth review of rev 5 |
| +(`CODEX-FINDINGS-REGION-HA-REV5-4.md`, **B4-n**), which found no |
| +two-writer or data-loss path that depends on disk evidence. It removes |
| +the last runtime dependency on volume recording: the multi-box gate no |
| +longer checks it at box start, and recorder failure only alerts and |
| +keeps a dead box's chores open (B4-1). It also brings three summaries |
| +into line with H19 (B4-2). §23 maps both. |
| + |
| **Rev 5.3** records Paul's ruling **H19** (2026-10-06), which supersedes |
| H15 and the volume half of H10, and answers Astra's third review of rev |
| 5 (`CODEX-FINDINGS-REGION-HA-REV5-3.md`, **B3-n**) in §22. Rounds 1 to 3 |
| @@ -941,9 +949,9 @@ conditional on `op.id` and the phase, citing `from`'s fence: |
| | `from` terminated | The CAS | The op resumes at | |
| |---|---|---| |
| -| in `starting`, acknowledged or not | journals `failover_fence` (key, SHA-256) and `reason: failover`, keeping the intent and every acknowledgement; removes `from` from `participants` and from the barrier; sets `op.exec: none`, keeping the stamp (claim D5's non-installing form); adds `from` to `lost` and discharges its `park-local` chores (§5.9) | `starting`, waiting only for `to`'s acknowledgement; the next CAS goes to `pinning` with the fence as its evidence, skipping `releasing` | |
| +| in `starting`, acknowledged or not | journals `failover_fence` (key, SHA-256) and `reason: failover`, keeping the intent and every acknowledgement; removes `from` from `participants` and from the barrier; sets `op.exec: none`, keeping the stamp (claim D5's non-installing form); adds `from` to `lost`, and discharges its `park-local` chores only if its volume records qualify, otherwise leaves them open for an operator (§5.9, H19) | `starting`, waiting only for `to`'s acknowledgement; the next CAS goes to `pinning` with the fence as its evidence, skipping `releasing` | |
| | in `releasing`, before its receipt | the same | `pinning`, with the fence as evidence | |
| -| after its receipt (`pinning` on) | `from` only goes on `lost` and its chores are discharged; nothing else changes | the same phase | |
| +| after its receipt (`pinning` on) | `from` only goes on `lost`, and its chores are discharged if its volume records qualify, otherwise left open; nothing else changes | the same phase | |
| The pin for a converted op follows the failover rule (fence plus 30 |
| seconds), and the first admission's coverage is `""`. |
| @@ -1295,9 +1303,9 @@ operations. |
| retirement under `files/` is by exact version, through the parker, |
| like every other retirement (claim C3). |
| - **Tofu:** the `region-host` module has `delete_on_termination = true` |
| - on the root volume (plan 1a), and must have it on every other EBS |
| - volume a box attaches, since H10 refuses to fence a box with one that |
| - survives. Moving to an Auto Scaling group is spec 4; spec 1 runs on |
| + on the root volume (plan 1a), and should have it on every other EBS |
| + volume a box attaches. It never affects the fence (H19): it only lets |
| + a dead box's `park-local` chores be discharged automatically (§5.9). 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 |
| @@ -1305,7 +1313,7 @@ operations. |
| | 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; an enrolled box in another region confirms its group membership (H17) and the console enrolls it. It is then the region's worker: it reads the termination event, writes the fence from its predecessor's last volume record, and relocates every host to itself. | |
| +| Executor dies, region had one box | the Auto Scaling group launches a replacement; an enrolled box in another region confirms its group membership (H17) and the console enrolls it. It is then the region's worker: it reads the termination event, writes the fence from that `terminated` read alone, and relocates every host to itself. The dead box's chores are discharged only if its volume records qualify (H19). | |
| | A console's box is alive but its report is stale | a box-started relocation proceeds on the console's newest report if that met the floor and the box's update guard is armed (H18); otherwise it waits and alerts. | |
| | The console's box is the one that died | failover does not need it: the fence, the census exclusion and every relocation CAS are a regional worker's (§5.9, L5, L6). | |
| | 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. | |
| @@ -1342,16 +1350,26 @@ operations. |
| `region-ha-1` and runs at or above the HA floor; |
| - every box in the region is `active` in the roster with a proven |
| `cloud`; |
| - - the region's termination queues exist, and the regional workers |
| - are writing volume records for every box (§5.9). |
| + - the region's termination queues exist. |
| + |
| + **Volume recording is never part of this gate (B4-1, H19).** Spec 1 |
| + ships the recorder with the rest of §5, and rollout checks once that |
| + it runs, but neither the gate, nor a box's start, nor row minting, |
| + nor relocation, nor recovery ever waits on a volume record. A |
| + recorder that cannot write raises an alert, and its only effect is |
| + that a box that dies meanwhile keeps its `park-local` chores open for |
| + an operator (§5.9). |
| The HA floor joins the protocol floor (claim §10, D1): 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. |
| + The gate is checked in `carlos system` and in the console's box |
| + list. Each box re-checks at start only its runtime half: the |
| + capability and floor of the region's boxes and edges, and their |
| + roster entries. A box that finds a second box in its region without |
| + that half satisfied refuses to mint relocatable rows and alerts. The |
| + termination queues are a rollout check only: a missing queue loses |
| + one trigger, and the describe still fences (§5.9). |
| 4. **Relocation by drain** stays off until the claim accepts L9; failover |
| relocation needs L1 to L6. |
| 5. Rehearse on dev with two fixed boxes: create spreads across both; |
| @@ -1436,7 +1454,10 @@ rev 4.2's table; this mapping says where each now lives. |
| `shutting-down` read offered as evidence, and the fence accepted with |
| no volume record at all); chore discharge (all records `true`: |
| discharged; a `false` flag, a removed volume or no record: left open, |
| - with the relocation unaffected); the volume recorder (writes on change, |
| + with the relocation unaffected); a box starting while |
| + `control/box-volumes/` cannot be written: it mints its relocatable |
| + rows, takes part in relocation and recovers a dead peer's hosts, |
| + and only alerts (B4-1); the volume recorder (writes on change, |
| at least hourly, `removed_volumes` when a volume leaves the mapping); |
| cross-region confirmation (accepted only when the target region has no |
| `active` box, refused for another group, an instance not |
| @@ -1678,8 +1699,8 @@ changes how some of it is used. Plan 1b is written against rev 5. |
| rev 5 (item 10's expected region now comes from the roster). Item 2 |
| follows §5.3's revised table. Item 4 is dropped. Item 6 becomes |
| publishing the enrollment evidence at start. Item 7 is §5.8 as rev 5 |
| -states it, and waits for L1 and L9 to L11. Item 8 adds the roster and |
| -volume checks to the gate. |
| +states it, and waits for L1 and L9 to L11. Item 8 adds the roster check |
| +to the gate; volume recording is not part of it (B4-1). |
| Rev 5.1 adds to plan 1b: the removed-volume rule (§5.9), the local |
| install receipt (§5.8), and root's refusal on any controller record |
| @@ -1762,3 +1783,14 @@ host artifacts the new enrollment does not own; claim P6-D2 refuses to |
| initialize or materialize over ambiguous ownership, and every writer |
| restores from the certified remote anyway (claim R6), so the old |
| database is never served. |
| + |
| +## 23. Astra rev 5 round 4 dispositions |
| + |
| +Reviewed rev 5.3 at 27058fe1 (`CODEX-FINDINGS-REGION-HA-REV5-4.md`). |
| +Astra agreed B3-1 to B3-5 are moot under H19, and found no two-writer |
| +or data-loss path that depends on disk evidence. |
| + |
| +| Finding | Disposition | |
| +|---|---| |
| +| B4-1 P2 volume recording is still a runtime admission prerequisite through §8's gate | accepted: under H19, volume recording never gates execution, admission, relocation or recovery. The gate no longer checks it; a box's start re-checks only capability, floor and roster; recorder failure alerts and keeps a dead box's chores open; tested through start, row minting and recovery (§8, §10, §19) | |
| +| B4-2 P3 summaries still describe the disk-dependent fence | accepted: the source-loss table discharges chores only on qualifying records (§5.8); the tofu note says `delete_on_termination` affects only discharge (§6); the one-box row fences on the `terminated` read alone (§7) | |