amadan
spec: region HA spec 1 rev 5, ec2:DetachVolume in the H15 volume guard
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+11
−8
docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md+11 −8
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 ec08eea19..46fac1483 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 |
| @@ -85,7 +85,7 @@ are alive, and on #212 option B for box references. |
| | H12 | **(2026-10-06) Executor choice at create** is spec 1's `choose()`: prefer a box running no instance of the app; then the most headroom (until spec 2, the fewest claimed hosts); then the claim's P5-D2 SHA-256 of `host + "\x00" + box reference` as the final tie-break. It is recorded once, in the create intent. Recovery never substitutes. | |
| | H13 | **(2026-10-06) Claim ruling R6 supersedes HA3 and §5.5.** A box never reuses its local database. Every admission is cold until claim P6-D4 lifts. HA3 and §5.5 are deleted, and the activator half of plan 1a's install marker is not used. | |
| | H14 | **(2026-10-06) Relocation starts need no console reservation (L6).** A relocation start requires that no executable update is reserved for `from` or `to` in `control/host-actors.json`, which the worker reads and never writes. Root on each box refuses to start an executable update while that box is a participant in a running claim operation. The update side's refusal is what closes the race with a reservation made after the start's read. (§5.10.) | |
| -| H15 | **(2026-10-06) H10's volume check rests on a running-time record, not the terminated read.** Tested on dev 2026-10-06: while `shutting-down`, `DescribeInstances` still listed both volumes of a test instance with their `DeleteOnTermination` flags; once `terminated`, `BlockDeviceMappings` was empty, the `true` root volume was already gone (`InvalidVolume.NotFound`) and the `false` volume survived as `available`. So the fence rests on (1) a record of the box's block device mappings taken by regional workers while it runs, refreshed on change, kept with its roster-bound evidence, showing every attached EBS volume `DeleteOnTermination: true`; (2) IAM denying `ec2:ModifyInstanceAttribute` and `ec2:AttachVolume` on platform boxes to every principal except operator roles, so the record cannot go stale behind the platform's back; (3) the terminated read (describe, event, later the group's history). A `shutting-down` read that still lists mappings may refresh the record but is never itself evidence. A missing record, one older than the stated bound, or one with any `false` volume sends the box to the operator path. (§5.9, §6.) | |
| +| H15 | **(2026-10-06) H10's volume check rests on a running-time record, not the terminated read.** Tested on dev 2026-10-06: while `shutting-down`, `DescribeInstances` still listed both volumes of a test instance with their `DeleteOnTermination` flags; once `terminated`, `BlockDeviceMappings` was empty, the `true` root volume was already gone (`InvalidVolume.NotFound`) and the `false` volume survived as `available`. So the fence rests on (1) a record of the box's block device mappings taken by regional workers while it runs, refreshed on change, kept with its roster-bound evidence, showing every attached EBS volume `DeleteOnTermination: true`; (2) IAM denying `ec2:ModifyInstanceAttribute` and `ec2:AttachVolume` on platform boxes to every principal except operator roles, so the record cannot go stale behind the platform's back; (3) the terminated read (describe, event, later the group's history). A `shutting-down` read that still lists mappings may refresh the record but is never itself evidence. A missing record, one older than the stated bound, or one with any `false` volume sends the box to the operator path. (§5.9, §6.) The controller added `ec2:DetachVolume` to the deny in (2), as within the ruling's intent. | |
| | H16 | **(2026-10-06) Auto Scaling boxes are enrolled automatically, with evidence (spec 4, L19).** The console enrolls an Auto Scaling box itself when its `boxid` evidence verifies (the deployment's account, the region's AWS region) and a regional worker confirms, with read-only Auto Scaling rights, that the instance is a current member of that region's group. Anything else still needs an operator's approval. | |
| H10 to H16 supersede only what they name: H10 adds the volume condition |
| @@ -1032,10 +1032,13 @@ operations. |
| `s3:DeleteObjectVersion` on its region's data bucket (claim §6.2a), |
| which `genselect` and the parker use. |
| - **The volume guard (H15).** An Organizations service control policy on |
| - the deployment's account denies `ec2:ModifyInstanceAttribute` and |
| - `ec2:AttachVolume` on instances tagged as platform boxes |
| - (`aws:ResourceTag/carlos:role = platform-box`) to every principal whose |
| - ARN is not one of the deployment's operator roles. Where the account |
| + the deployment's account denies `ec2:ModifyInstanceAttribute`, |
| + `ec2:AttachVolume` and `ec2:DetachVolume` on instances tagged as |
| + platform boxes (`aws:ResourceTag/carlos:role = platform-box`) to every |
| + principal whose ARN is not one of the deployment's operator roles. |
| + `DetachVolume` is there because a volume detached from a running box |
| + survives termination with the box's data, which is exactly what the |
| + fence must rule out. Where the account |
| has no Organizations, tofu puts the same Deny in every role and user it |
| manages; that is weaker, since it cannot bind principals tofu does not |
| know, and `carlos system` says so. The launch template and the |
| @@ -1159,7 +1162,7 @@ the text. |
| | # | Amends | Change | Status | |
| |---|---|---|---| |
| | L1 | claim §4, §8, §6.4a (which kinds and phases admit), §7.3 D6 | New op kind `relocating` (§5.8): same region, stateful, from `serving`; its phase table with `op.exec`, stamp, rows and admission per phase; the `installed` no-reinstall boundary; the replacement table; two replacements then `stuck`; the release sequence. Recovery owner `region:<r>`, any regional worker (P6-D5). The D6 barrier needs only `to` when the start cites a termination fence. Excludes moves, placements and pushes. | Ruled in direction (H10; #236: "a new op kind, or an equivalent that the claim prefers") | |
| -| L2 | claim §4, C5, §7.3 D2 | A termination fence (§5.9) is a lost-box fence, written by a regional worker with no person in the loop: `terminated` only (by event, describe or, later, the group's history), bound to the roster entry's `cloud`, with a running-time volume record no more than 2 hours old showing every EBS volume `DeleteOnTermination`, under the IAM volume guard. A `shutting-down` read is never evidence. Stopped, unclear and vanished boxes keep D2's operator path unchanged. | Ruled (H10, H15) | |
| +| L2 | claim §4, C5, §7.3 D2 | A termination fence (§5.9) is a lost-box fence, written by a regional worker with no person in the loop: `terminated` only (by event, describe or, later, the group's history), bound to the roster entry's `cloud`, with a running-time volume record no more than 2 hours old showing every EBS volume `DeleteOnTermination`, under the IAM volume guard (no `ModifyInstanceAttribute`, `AttachVolume` or `DetachVolume` on platform boxes except by operator roles). A `shutting-down` read is never evidence. Stopped, unclear and vanished boxes keep D2's operator path unchanged. | Ruled (H10, H15) | |
| | L3 | claim §7.3 D5 | A fenced terminated box's `park-local` chores are discharged in the fence CAS: H10's volume check is D5's destroyed-local proof. Regional chores move to `region:<r>` as D5 says. | Ruled (H10) | |
| | L4 | claim §7.3 D3 and D4, §5.9 P5-D3 | The fence record `control/box-fences/<enrollment>.json`, create-only, box-written, cited by `evidence_refs`. A terminated box goes on `lost` with that reference and no quarantine revision; it needs no readmission. The console later copies it into a D4 loss record and retires the roster entry. | Ruled in direction (H10, H1); record format for the claim session | |
| | L5 | claim §10.1 D7 (required actors) | An enrolled box with a valid fence record is excluded from the census without waiting for the console to retire it. | Ruled (H10; #236: failover works when the console's box died) | |
| @@ -1230,8 +1233,8 @@ rev 4.2's table; this mapping says where each now lives. |
| marker and its check: never an update and an acknowledged |
| participation at once, and a crash leaves at most a refusal, cleared |
| by retry. |
| -- **IAM:** the volume guard refuses `AttachVolume` and a block device |
| - mapping change by the box role and a non-operator role, and allows an |
| +- **IAM:** the volume guard refuses `AttachVolume`, `DetachVolume` and a |
| + block device mapping change by the box role and a non-operator role, and allows an |
| operator role (rehearsed on dev, §8 step 5). |
| - **Integration:** two agents against one fake region, one control |
| bucket: create lands on the chosen box only; the other box mints no |