amadan
spec: region HA spec 1 rev 5.3, Paul's ruling H19 and Astra rev 5 round 3 (B3-1 to B3-5)
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+172
−257
docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md+172 −257
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 2c590675a..b00b256eb 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,21 @@ |
| # Region HA, spec 1: placing an instance on a box |
| -Design, 2026-10-06, **rev 5.2**. DRAFT. Plan 1a is built and merged |
| +Design, 2026-10-06, **rev 5.3**. DRAFT. Plan 1a is built and merged |
| (aadb860); nothing else here is built. |
| +**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 |
| +kept finding new ways a disk could outlive its box behind the volume |
| +guard. H19 takes the disk out of the failover path: a terminated |
| +instance can never run again, so the execution fence rests on the |
| +verified `terminated` read alone. Disk evidence decides only whether |
| +the dead box's `park-local` chores are discharged automatically; when |
| +it cannot be proven, they stay open for an operator, and recovery waits |
| +on nothing. The SCP, holds, the change role, the guard attestation and |
| +the service-role audit are removed. Most of round 3 is moot under H19; |
| +§22 says which, and why. |
| + |
| **Rev 5.2** answers Astra's second review (`CODEX-FINDINGS-REGION-HA-REV5-2.md`, |
| cited **B2-n**): four P1 and two P2, all accepted; §21 maps each, with |
| the round 1 items it marked partly resolved. The volume guard now |
| @@ -120,13 +133,16 @@ are alive, and on #212 option B for box references. |
| | 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. | |
| | H17 | **(2026-10-06) The first box of an emptied region is confirmed from another region.** Any enrolled box in another region holds cross-region read-only Auto Scaling and EC2 describe rights and may confirm a new box's group membership (H16) for a region that has no enrolled box. That is its only cross-region use. One-box regions therefore recover automatically. (§5.1, §6, L19.) | |
| | H18 | **(2026-10-06) A stale console report does not hold up a box-started relocation.** For box-started relocations only, the census accepts a console's newest report however old, provided that report met the protocol floor and the console's box has the claim's D1 root update guard armed, so it cannot be swapped for an older binary underneath. Everything else in claim D7 is unchanged. (§5.9, L20.) | |
| +| H19 | **(2026-10-06) The failover fence rests on the `terminated` read alone; disk evidence only decides discharge of local chores.** Supersedes H15 and the volume half of H10; H10's automatic failover stands. The execution fence is a verified `terminated` read, bound to the roster's `cloud` identity, from the event or a describe (later the group's history); absence is never evidence. This is the claim's own lost-box rule for execution (§7.2), which needs no volume condition: a terminated instance can never run again, a surviving disk cannot write to storage by itself, and a disk attached to another instance is a different box with a different enrollment, never admitted as the old executor. The disk question belongs only to claim D5's destroyed-local exception: whether the dead box's `park-local` chores can be discharged automatically. That needs the volume evidence (the box's launch-time mappings all `DeleteOnTermination`, recorded while running); if it cannot be proven, the chores stay open for an operator (claim D2 and D5) and nothing about recovery waits on them. A surviving copy of a disk is a data-retention and cleanup concern for the operator path, not a two-writer risk. Tofu keeps `delete_on_termination = true`. (§5.9, §6, L2, L3.) | |
| -H10 to H18 supersede only what they name: H10 adds the volume condition |
| +H10 to H19 supersede only what they name: H10 adds the volume condition |
| to H1 and H15 says where it is read from, H11 replaces §5.1's box records |
| as authority, H13 replaces HA3 and §5.5, H14 replaces claim D7's console |
| reservation for relocation starts, H16 and H17 settle enrollment for |
| -spec 4, and H18 narrows claim D7's console census for box-started |
| -relocations. |
| +spec 4, H18 narrows claim D7's console census for box-started |
| +relocations, and H19 supersedes H15 and the volume half of H10 (the |
| +fence needs no disk evidence; only automatic discharge of local chores |
| +does). |
| Everything else in H1 to H9 stands. |
| Standing rulings this spec keeps: |
| @@ -258,8 +274,9 @@ A relocated host's data becomes current only through a cold |
| **HA7. Termination evidence is bound to the roster.** A fence counts only |
| if the terminated instance is the one the box's roster entry records |
| under `cloud`, in the deployment's own account and the region's own AWS |
| -region (A1-1, H11), and every EBS volume it had attached was |
| -`DeleteOnTermination: true` (H10). |
| +region (A1-1, H11). No disk condition applies to the fence (H19): disk |
| +evidence decides only whether the box's local chores are discharged |
| +automatically (§5.9). |
| ## 4. What stays the same |
| @@ -346,8 +363,7 @@ group, not to anything the new box says: |
| target region's AWS region, and requires the reply to name exactly that |
| group, lifecycle state `Pending` or `InService`, and an availability |
| zone in that AWS region; then `DescribeInstances` there, requiring the |
| - instance `pending` or `running`, the deployment's `OwnerId` and the |
| - `carlos:role` tag; |
| + instance `pending` or `running` with the deployment's `OwnerId`; |
| - **the region is empty (B2-6).** The roster entry of a dead box stays |
| `active` until a fence retires it, and only a regional worker can write |
| the fence, so the roster alone would never show the region empty. The |
| @@ -375,7 +391,7 @@ target region appears in the confirmation's `terminated_enrollments` |
| placement, and the `boxid` record's region equals `aws_region`. Once |
| enrolled, the new box is the region's worker: it writes its own volume |
| records, fences its predecessor through the ordinary §5.9 path (its own |
| -terminated read and the predecessor's last volume record), and recovers |
| +terminated read), and recovers |
| the hosts (§5.8). So a one-box region recovers automatically (§7). |
| A box whose entry is not `active` with a proven `cloud` is never |
| @@ -955,43 +971,47 @@ detection plus restore (spec 3). |
| ### 5.9 The termination fence |
| -**What counts (A1-1, A1-11, H10, H15).** A box is fenced by termination |
| -only when all three of these hold: |
| - |
| -1. **A volume record.** The newest **volume record** taken while the |
| - instance was `running` (below) is no more than **2 hours** older than |
| - the terminated observation, names the instance in the roster entry's |
| - `cloud`, shows the guard's tag on it, and lists at least one EBS |
| - volume. It, and every record written after it, shows every attached |
| - EBS volume `DeleteOnTermination: true`. And **disk evidence is not |
| - suspended** for the enrollment (below, B1-3). |
| -2. **The IAM guard is in place and attested** (§6, B1-4): an Organizations |
| - policy, recorded in a valid guard attestation, denies every principal |
| - but the one volume-change role any change to a platform box's block |
| - device mapping, any attach or detach, and any change to the guard's |
| - tag, so the record cannot go stale behind the platform's back. With |
| - no valid attestation, nothing is fenced automatically. |
| -3. **A terminated read.** A regional worker, with its own read-only |
| - rights in the box's AWS region, observes state exactly `terminated` |
| - for the instance id, account (`OwnerId`) and region in the roster |
| - entry's `cloud` (H11, HA7), by one of the three sources below. |
| - |
| -The terminated read itself never carries the volumes. On dev on |
| -2026-10-06 (§8 step 5), a terminated instance's `BlockDeviceMappings` |
| -was empty, its `DeleteOnTermination: true` root volume was already gone |
| -(`InvalidVolume.NotFound`), and its `false` volume survived as |
| -`available`. That is why the proof is the running-time record. |
| - |
| -If the newest record is missing, is older than the bound, or shows any |
| -volume `false`, the box is not fenced automatically; the operator path |
| -applies. |
| +**What counts (A1-1, A1-11, H10, H19).** A box is fenced by termination |
| +when a regional worker, with its own read-only rights in the box's AWS |
| +region, observes state exactly **`terminated`** for the instance id, |
| +account (`OwnerId`) and region in the box's roster entry's `cloud` |
| +(H11, HA7), by one of the three sources below. Nothing else is needed |
| +(H19). This is claim §7.2's rule for execution, that the instance is |
| +fenced by the cloud, without the operator: a terminated instance can |
| +never run again; a disk that survives it cannot write to storage by |
| +itself; and a disk attached to another instance is a different box, |
| +with a different instance id and enrollment, never admitted as this |
| +box's executor (claim C4, HA7). |
| + |
| +**Disk evidence, for discharging local chores only (H19, claim D5).** |
| +Whether the dead box's `park-local` chores can be discharged without |
| +retirement is a separate question, about cleanup, not about who may |
| +write. A worker discharges them automatically, in the fence CAS, only |
| +when the box's **volume records** (below) show its block device |
| +mappings, from the first record taken at enrollment (the launch-time |
| +mappings) to the last taken while it ran, with every attached EBS volume |
| +`DeleteOnTermination: true` and no volume ever removed. Otherwise the |
| +chores stay open for an operator's destroyed-local declaration or the |
| +returning-box retirement (claim D2, D5). Nothing about recovery waits on |
| +them: the fence, the relocation and the census do not read volume |
| +records (§5.8, L5). |
| + |
| +This is not proof that no copy of the disk exists. A volume kept by a |
| +Recycle Bin rule, copied, snapshotted or imaged, or detached by an |
| +operator, can survive. That is a data-retention concern, handled by the |
| +operator path and the deployment's own retention settings, never a |
| +second writer: no such disk can act as the executor (above). The dev |
| +test of 2026-10-06 (§8 step 5) showed why the evidence must be recorded |
| +while the box runs: once `terminated`, `BlockDeviceMappings` was empty, |
| +the `DeleteOnTermination: true` root volume was already gone |
| +(`InvalidVolume.NotFound`), and the `false` volume survived as |
| +`available`. |
| **The volume record.** Regional workers describe each enrolled box in |
| their region while it runs: at enrollment, on every 10-minute sweep, and |
| at once when a describe shows `shutting-down`. A worker writes a new |
| record, create-only, whenever the mapping differs from the newest |
| -record, and otherwise at least once an hour, so a healthy box's newest |
| -record is never more than about an hour old: |
| +record, and otherwise at least once an hour: |
| control/box-volumes/<enrollment>/<observed_at>.json |
| @@ -1002,76 +1022,19 @@ record is never more than about an hour old: |
| "instance_state": "running", |
| "block_devices": [{"device": "/dev/xvda", "volume_id": "vol-…", |
| "delete_on_termination": true, "status": "attached"}], |
| + "removed_volumes": [], |
| "observed_at": "<RFC3339>", "request_id": "<EC2 request id>", |
| "written_by": {"box": "<reference>", "enrollment": "<enrollment>"}} |
| ``` |
| - A record is bound to the roster entry: its `cloud` must equal the |
| entry's, and a record for another instance is ignored. |
| -- A **`shutting-down`** read that still lists mappings may write a fresh |
| - record, with `instance_state: "shutting-down"`. If it shows any volume |
| - `false`, that record is the newest and the fence is refused. It is |
| - never itself termination evidence. |
| -- A record showing a `false` volume on a running box alerts at once: |
| - that box can never be fenced automatically until the volume is fixed. |
| -- The record also lists the instance's and each volume's tags as |
| - described, so the fence can check the guard's tag on all of them (§6). |
| - |
| -**Suspending disk evidence (B1-3).** A record's age bound cannot cover an |
| -operator's change made just before a termination, and a detached volume |
| -is not in any later record at all. So disk evidence is suspended |
| -**before** any exempt change, and resumes only after the change is |
| -accounted for: |
| - |
| -- **Before.** The only principal the guard exempts is the volume-change |
| - role (§6). `carlos ops box volumes change <box>` first writes a |
| - create-only hold, `control/box-volumes/<enrollment>/hold-<id>.json` |
| - (`{id, operator, reason, instance_id, at}`), and only then assumes that |
| - role with the session tags `carlos:volume-hold = <id>` and |
| - `carlos:instance = <instance id>`, for at most one hour. The role's |
| - trust policy requires both tags, and the guard's exemption covers only |
| - requests on the instance the tag names (§6). Session tags are the |
| - caller's own word, so they do not prove a hold exists: the operator |
| - workflow is what writes the hold first, and an operator who bypasses |
| - it is outside this design's trust, as an operator who attests falsely |
| - under claim D2 is. A box with a hold that has no later release is |
| - never fenced automatically: its termination goes to the operator |
| - path. |
| -- **Removed volumes.** Whenever a worker's describe of a running box |
| - shows a volume that the previous record listed and this one does not |
| - (a detach, or a root volume replaced by a new volume id), the new |
| - record carries `removed_volumes`, and that also suspends disk |
| - evidence, hold or no hold: the volume may survive with the box's data. |
| -- **After (B2-2).** `carlos ops box volumes release <box> <hold id>` |
| - closes the change in this order, and resumes disk evidence only at the |
| - end: |
| - 1. **No further requests.** It revokes every session of the |
| - volume-change role issued before now (an IAM deny on |
| - `aws:TokenIssueTime` earlier than the revocation, AWS's "revoke |
| - active sessions"), and records the revocation time `R` in a |
| - create-only `closing-<id>.json`. From `R` no credential the hold's |
| - change obtained can sign a request AWS accepts; |
| - 2. **Nothing in flight.** It waits until a worker's describe after `R` |
| - shows no volume of the instance `attaching` or `detaching`, |
| - `DescribeReplaceRootVolumeTasks` shows no task for it `pending` or |
| - `in-progress`, and no snapshot or image of its volumes is `pending`. |
| - Requests signed before `R` are bounded by S3 and EC2's 15-minute |
| - signature age, so it also waits until `R + 15 minutes`; |
| - 3. **A validating record after the barrier.** A worker's running record |
| - observed after both points shows every attached volume `true`; |
| - 4. **Removed volumes accounted for.** For every volume removed since the |
| - enrollment's last release (including a replaced root volume, and |
| - any snapshot or image taken), the operator attests (as in claim D2) |
| - that it was destroyed or never held host artifacts. |
| - |
| - The CLI then writes `release-<id>.json` create-only, naming the |
| - closing record, the validating record and each attestation. The fence |
| - needs a running record newer than the release. A release missing any |
| - step is invalid, and the hold stays open. |
| - |
| -A hold or removal therefore never leaves a window: from the hold's write |
| -until a release, the box cannot be fenced automatically, whatever its |
| -records say. |
| +- `removed_volumes` lists any volume the previous record had and this |
| + one lacks (a detach, or a replaced root volume). Any removal, or any |
| + `false` flag in any record, rules out automatic discharge for that |
| + enrollment for good, and alerts once so an operator knows. |
| +- A `shutting-down` read may add a record; it is never termination |
| + evidence. |
| **What never counts.** |
| @@ -1087,8 +1050,8 @@ records say. |
| an edges file, or anything a box publishes about itself. A volume |
| record is a cloud read, not such a report: any regional worker may |
| write one, the described box included, under the claim's trusted |
| - box-writer boundary (P5-D3). In a one-box region the box's records are |
| - its own, since H17 allows no other cross-region use. |
| + box-writer boundary (P5-D3). It decides only cleanup (above), so a |
| + wrong one can leave a disk unretired, never admit a writer. |
| **The fence record.** The worker writes one record per terminated |
| enrollment, create-only (L4): |
| @@ -1100,8 +1063,6 @@ enrollment, create-only (L4): |
| "cloud": {"provider": "aws", "account": "123…", |
| "region": "eu-west-1", "instance_id": "i-0abc…"}, |
| "state": "terminated", |
| - "volume_record": {"key": "control/box-volumes/<enrollment>/<…>.json", |
| - "sha256": "…"}, |
| "observed_at": "<RFC3339>", |
| "via": "describe" | "event" | "activity", |
| "request_id": "<EC2 request id, when via=describe>", |
| @@ -1114,8 +1075,8 @@ worker's authenticated report of a cloud read, made with rights the |
| console does not hold. Every relocation and claim CAS that relies on it |
| cites its key and SHA-256 (`evidence_refs`, claim P5-D3). |
| -**Three ways to observe `terminated`.** Since the volumes come from the |
| -record, any of these is the terminated read: |
| +**Three ways to observe `terminated`.** Any of these is the terminated |
| +read: |
| 1. **The durable event.** An EventBridge rule sends EC2 "Instance |
| State-change Notification" events with `state: terminated` for the |
| @@ -1137,8 +1098,7 @@ record, any of these is the terminated read: |
| **What is not guaranteed (A2-4).** EC2 delivers state-change events to |
| EventBridge on a best-effort basis, and a terminated instance leaves |
| `DescribeInstances` after about an hour. When no source shows |
| -`terminated`, or the volume record does not qualify, there is **no |
| -automatic recovery**. The placer marks the box's |
| +`terminated`, there is **no automatic recovery**. The placer marks the box's |
| hosts `awaiting-evidence`, alerts at once, and keeps retrying. The only |
| way out is the operator's `--declare-lost` (claim §7.3 D2). A CloudTrail |
| `TerminateInstances` record is **not** evidence (A3-1): it proves a |
| @@ -1158,10 +1118,14 @@ alerting, and owns the loop that reads the queue and history. |
| reference. A terminated instance cannot run again, so it needs no |
| quarantine and no `--readmit` (H1). Its reference never names a |
| working box again. |
| -- **Its local chores are discharged.** Every volume was deleted with the |
| - instance (H10, H15: the record, kept true by IAM), so its `park-local` chores are discharged in the same |
| - CAS, by `CompleteObligation` semantics, without retirement. That is |
| - claim D5's destroyed-local exception, now proven (L3). Regional chores |
| +- **Its local chores are discharged, if the disk evidence allows (H19).** |
| + When the volume records qualify (above), its `park-local` chores are |
| + discharged in the same CAS, by `CompleteObligation` semantics, without |
| + retirement: claim D5's destroyed-local exception (L3). The fence CAS |
| + cites the records it relied on. When they do not qualify, the chores |
| + stay open for an operator, and the relocation proceeds regardless: |
| + a dead box's `park-local` names only that box, which no relocation |
| + writes (claim CC11). Regional chores |
| are reassigned to `region:<r>`, keeping their ids, operations and |
| scopes (D5). Remote scopes it justifies take the fence's `observed_at` |
| as their original evidence time (claim P5-D3, D5). |
| @@ -1280,90 +1244,18 @@ operations. |
| own grants: `s3:ListBucketVersions`, `s3:GetObjectVersion` and |
| `s3:DeleteObjectVersion` on its region's data bucket (claim §6.2a), |
| which `genselect` and the parker use. |
| -- **The volume guard (H15, B1-4).** An Organizations service control |
| - policy on the deployment's account denies, to every principal whose |
| - ARN is not the deployment's **volume-change role**: |
| - - `ec2:ModifyInstanceAttribute`, `ec2:AttachVolume`, |
| - `ec2:DetachVolume` and `ec2:CreateReplaceRootVolumeTask` on instances |
| - tagged `aws:ResourceTag/carlos:role = platform-box`, and on volumes |
| - tagged the same (the launch template tags each box's volumes too). |
| - `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. `CreateReplaceRootVolumeTask` is there for the |
| - same reason: it replaces a running box's root disk and by default |
| - keeps the old volume (B2-1); |
| - - `ec2:CreateSnapshot`, `ec2:CreateSnapshots` and `ec2:CreateImage` on |
| - those instances and volumes: a snapshot or image is a copy of the |
| - disk that outlives it just as a kept volume does. No Data Lifecycle |
| - Manager or AWS Backup policy may select them (checked by the |
| - attestation); |
| - - `ec2:CreateTags` and `ec2:DeleteTags` on any instance or volume when |
| - `aws:TagKeys` includes `carlos:role`, except `CreateTags` with |
| - `ec2:CreateAction = RunInstances`, so a launch can tag a new box and |
| - its volumes but nobody can strip, add or change the tag on a running |
| - one or its disks. |
| - |
| - - `autoscaling:StartInstanceRefresh`, `autoscaling:UpdateAutoScalingGroup`, |
| - `autoscaling:CreateAutoScalingGroup`, `autoscaling:PutWarmPool` and |
| - `autoscaling:AttachInstances` on the deployment's platform groups: |
| - these are the requests that start Auto Scaling's own disk and tag |
| - work (B2-3, below). |
| - |
| - The volume-change role is assumable only by operators, and its trust |
| - policy requires the session tags `carlos:volume-hold` and |
| - `carlos:instance` (§5.9's hold). Its exemption from the EC2 statements |
| - applies only where the resource is that instance or its volumes. Every |
| - other operator role is denied these actions like everyone else. |
| - |
| - **Auto Scaling's service-linked role (B2-3).** No SCP binds a |
| - service-linked role, and `AWSServiceRoleForAutoScaling`'s managed |
| - policy (`AutoScalingServiceRolePolicy`) includes |
| - `ec2:ModifyInstanceAttribute`, `ec2:CreateReplaceRootVolumeTask` and |
| - tag changes, which cannot be edited away. So the guard does not claim |
| - that no service-linked role can touch a disk. It constrains what makes |
| - the service act. The service role acts on a group's instances only on |
| - behalf of that group's configuration and of requests to it: launches |
| - and terminations, an instance refresh (whose `ReplaceRootVolume` |
| - strategy replaces root disks), warm pools (which stop instances with |
| - their disks), and attaching existing instances. Every one of those is |
| - started by an Auto Scaling API in the list above, denied to all but |
| - the volume-change role; a launch template change only affects new |
| - instances, whose volume records then show what they got. Spec 4 must |
| - not use a warm pool or a `ReplaceRootVolume` refresh for enrolled |
| - boxes; an operator who must, does it under a hold. |
| - |
| - **Coverage is attested, not assumed.** An SCP does not bind the |
| - Organizations management account or service-linked roles. The |
| - operator workflow therefore verifies, with operator credentials, that |
| - the deployment's account is a member account and that the policy is |
| - attached with exactly these statements. It then lists every |
| - service-linked role in the account and reads each one's managed policy |
| - **at its current default version**. For every action in them that can |
| - change, copy or replace a disk, its `DeleteOnTermination`, or the |
| - `carlos:role` tag, it requires an entry in a reviewed table naming the |
| - initiating API that makes the service use it, and that API must be one |
| - the SCP denies (as above for Auto Scaling). An action with no entry, |
| - or a service-linked role the table does not know, fails the |
| - attestation. No Data Lifecycle Manager or AWS Backup policy may select |
| - platform boxes or their volumes. It writes a root-signed **guard |
| - attestation**, `control/volume-guard.json` (`{account, policy_id, |
| - policy_sha256, service_roles: [{role, policy_arn, default_version, |
| - document_sha256}], checked_at, operator}`). A service-linked policy |
| - whose default version changes after the attestation makes it invalid |
| - until rechecked; the regional workers' sweep reads the versions |
| - (`iam:GetRole` and `iam:GetPolicy`, read-only, on those roles and |
| - policies only) and alerts on a change. The fence requires a valid one for the box's |
| - account (§5.9). An account with no Organizations, or none attested, |
| - has **no automatic fence**: every termination there goes to the |
| - operator path. This is H15's condition (2) unmet, not a weaker |
| - variant of it. Both deployment accounts are Organizations member |
| - accounts, checked 2026-10-06: organization `o-sgnzdj0z0c`, all |
| - features enabled, management account 665106592142; flagship |
| - 271376211898 and dev 640012953448. So the SCP route is available for |
| - both, and neither deployment account is the management account. The launch template and the `region-host` module create |
| - every volume with `DeleteOnTermination` and tag every box |
| - `carlos:role = platform-box`; enrollment refuses a box without the |
| - tag. |
| +- **Disks (H19).** Nothing in IAM guards a box's disks for the fence's |
| + sake: rev 5.2's SCP, holds, volume-change role, guard attestation and |
| + service-role audit are withdrawn. The launch template and the |
| + `region-host` module keep `delete_on_termination = true` on every |
| + volume, which is cheap and makes automatic discharge of local chores |
| + the usual case (§5.9). The deployment should configure no Recycle Bin |
| + rule, Data Lifecycle Manager or AWS Backup policy that selects |
| + platform box volumes; one that does is a data-retention choice, and |
| + the operator path then owns their cleanup. The deployment accounts |
| + are Organizations members (organization `o-sgnzdj0z0c`, management |
| + account 665106592142; flagship 271376211898, dev 640012953448, checked |
| + 2026-10-06), which no longer matters to the fence. |
| - **Auto Scaling enrollment (H16, H17, spec 4).** The box role gains one |
| separate statement: `autoscaling:DescribeAutoScalingInstances` and |
| `ec2:DescribeInstances`, read-only, conditioned on |
| @@ -1378,8 +1270,8 @@ operations. |
| - **S3 (A2-6).** Two kinds of write, kept apart: |
| - **Create-only** (`If-None-Match: *`): content objects, |
| `instances/<host>/*/files/*/objects/`, in the region's data bucket; |
| - box identity records, `control/boxes/`, volume records, holds and |
| - releases, `control/box-volumes/`, membership confirmations, |
| + box identity records, `control/boxes/`, volume records, |
| + `control/box-volumes/`, membership confirmations, |
| `control/box-enrollment/`, and fence records, `control/box-fences/`, |
| in the control bucket. |
| - **Conditional replace** (`If-Match`, or `If-None-Match: *` for the |
| @@ -1418,13 +1310,9 @@ operations. |
| | 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. | |
| | Box alive but failing its health check | the group terminates it, then as above. Instances that were healthy lose up to H3's window, declared by `writes_lost`. | |
| -| A terminated box had a volume without `DeleteOnTermination` | no automatic fence: `awaiting-evidence`, an alert, and the operator's `--declare-lost` (§5.9). The running box's record already alerted. | |
| -| A terminated box's newest volume record is missing or over 2 hours old | no automatic fence: the operator path (§5.9, H15). | |
| -| An operator changes a box's volumes, or a volume vanishes from a running box's mapping | disk evidence is suspended from the hold (or the record showing the removal) until a release, which first revokes the change role's sessions and waits out in-flight disk tasks; a termination meanwhile goes to the operator (§5.9, B1-3, B2-2). | |
| -| A root volume is replaced, or a snapshot or image is taken, outside a hold | refused by the guard; Auto Scaling cannot be asked to do it either (§6, B2-1, B2-3). | |
| -| An Auto Scaling service-linked policy gains a new disk action | the attestation is invalid until reviewed; no automatic fence meanwhile (§6, B2-3). | |
| +| A terminated box had a volume without `DeleteOnTermination`, or one was removed | fenced and relocated as usual; its `park-local` chores stay open for an operator (§5.9, H19). | |
| +| A copy of a dead box's disk survives (Recycle Bin, a copy, a snapshot) | a retention and cleanup matter for the operator; it can never act as the executor (§5.9, H19). | |
| | A region's only box dies and its roster entry is still `active` | the cross-region confirmer reads it `terminated` and confirms the replacement; the replacement fences it (§5.1, B2-6). | |
| -| The account has no attested volume guard | no automatic fence anywhere in it (§6, B1-4). | |
| | A participant's execution lease is lost and its cleanup fails | its controller record stays; root refuses executable updates on that box until the host is resolved (§5.10, B1-5). | |
| | The source dies while a drain is in `starting` | the op becomes a failover in place (§5.8, B1-6). | |
| | An update is reserved for `to` while a relocation starts | root refuses to begin it while `to` is a participant, or `to` refuses to acknowledge while it runs; never both running (§5.10). | |
| @@ -1454,11 +1342,8 @@ 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, every box has a current |
| - volume record showing every attached EBS volume |
| - `DeleteOnTermination` and the guard's tag, no box has an unreleased |
| - hold or removal, and the account has a valid guard attestation |
| - (§6). |
| + - the region's termination queues exist, and the regional workers |
| + are writing volume records for every box (§5.9). |
| The HA floor joins the protocol floor (claim §10, D1): every path that |
| restores an executable (system apply, rollback, boot recovery from |
| @@ -1479,14 +1364,11 @@ operations. |
| their flags and status `attached`. Once `terminated`, |
| `BlockDeviceMappings` was `[]`, the root volume was already gone |
| (`InvalidVolume.NotFound`), and the `false` volume survived as |
| - `available`. The fence therefore reads volumes from the running-time |
| - record (§5.9). The rehearsal repeats this with the record and the |
| - volume guard in place, and checks that an attach, a detach, a flag |
| - change, a root-volume replacement that keeps the old volume, a |
| - snapshot, an image, an instance refresh and a removal of the |
| - `carlos:role` tag by a non-operator role and by an ordinary operator |
| - role are refused, and that the |
| - volume-change role cannot be assumed without a hold tag. |
| + `available`. So disk evidence comes from records taken while the box |
| + runs, and decides only the discharge of local chores (H19, §5.9). The |
| + rehearsal terminates a box with an all-`true` mapping (chores |
| + discharged) and one with a `false` volume (fenced and relocated |
| + alike, chores left open). |
| The rehearsal also enrolls a box into a dev region with no `active` |
| box, confirmed from another region (H17), and checks that the |
| cross-region statement allows only the two describe calls. |
| @@ -1496,15 +1378,15 @@ operations. |
| For platform-1e (claim rev 6.25, 413b12cb) and platform-d8 (moves rev |
| 7.17, 39904c84). They replace rev 4.2's K1 to K11, which those sessions |
| -never received. "Ruled" means Paul's rulings of 2026-10-06 (H10 to H18, |
| +never received. "Ruled" means Paul's rulings of 2026-10-06 (H10 to H19, |
| and amadan #236) decide the direction; the owning session still writes |
| the text. |
| | # | Amends | Change | Status | |
| |---|---|---|---| |
| | L1 | claim §4, §8, §6.4a (which kinds and phases admit), §7.3 D5 and 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 for the remote build, with a per-box local install receipt, bound to the stamp of the CAS that handed the box `op.exec`, required before `probing` and never remade after the first admission; probe attempts after the first restoring from their predecessor; the replacement table; the source-loss conversion to failover from `starting` or `releasing`; 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 or after a source-loss CAS. 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` and the guard's tag, no unreleased hold or removal, and an attested volume guard (no `ModifyInstanceAttribute`, `AttachVolume`, `DetachVolume`, `CreateReplaceRootVolumeTask`, snapshot, image, Auto Scaling refresh or warm pool, or `carlos:role` tag change on platform boxes except by the hold-gated volume-change role; service-linked roles covered through the APIs that start them). A hold is released only after revoking the role's sessions and waiting out in-flight disk tasks. 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) | |
| +| L2 | claim §4, C5, §7.2, §7.3 D2 | A termination fence (§5.9) is a lost-box fence for execution, written by a regional worker with no person in the loop: a verified `terminated` read (event, describe or, later, the group's history), bound to the roster entry's `cloud`. No disk condition. A `shutting-down` read is never evidence. Stopped, unclear and vanished boxes keep D2's operator path unchanged. | Ruled (H10, H19) | |
| +| L3 | claim §7.3 D5 | A fenced terminated box's `park-local` chores are discharged automatically in the fence CAS only when its volume records, from enrollment to its last running record, show every attached EBS volume `DeleteOnTermination` and none removed; that is D5's destroyed-local proof for discharge. Otherwise they stay open for D2/D5's operator path, and no recovery step waits on them. Regional chores move to `region:<r>` as D5 says. | Ruled (H19) | |
| | 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, console enrollments) | An enrolled box with a valid fence record is excluded from the census without waiting for the console to retire it. A console enrollment gains `compute: {box, enrollment}`, checked against its reports; a console whose `compute` box is fenced is excluded the same way (B1-7). | Ruled (H10, H14; #236: failover works when the console's box died) | |
| | L6 | claim §10.1 D7 (lifecycle reservations, `actors_hold`), §7.3 D6 | For operations a box starts, replace the console reservation with §5.10's box-side check: the worker reads (never writes) the roster and refuses if an update is reserved for `from` or `to`; a participant writes its `pending` controller state, then refuses to acknowledge while root has an update begun; root writes its update-begun marker, then refuses an update while any controller record exists in any state, `lost` included, or cannot be read. A record is removed only by D6's clearing with its cleanup complete (B1-5). | Ruled (H14) | |
| @@ -1550,23 +1432,18 @@ rev 4.2's table; this mapping says where each now lives. |
| objects, tombstones, late uploads, `If-Match` races, a cold admission's |
| copied manifest naming the predecessor's objects); timer catch-up; |
| termination-fence acceptance (NotFound, wrong account, wrong region, |
| - stopped, all sources empty, an event alone with a good record, a |
| - record with a `false` volume, a missing record, a record just inside |
| - and just past the 2-hour bound, a record for another instance, a |
| - `shutting-down` read offered as evidence, a `shutting-down` read that |
| - refreshes the record with a `false` volume, a record without the |
| - guard's tag, no guard attestation, an unreleased hold, a removed |
| - volume with and without a release, a release with no later running |
| - record); 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 `Pending`/`InService`, |
| - a confirmer not `active`, a region mismatch, a second confirmer |
| - losing the create-only race, and an emptied region whose dead box is |
| - still `active`: confirmed on a `terminated` read, refused on NotFound |
| - or `stopped`, B2-6); a hold released while a detach is in flight, or |
| - before `R + 15 minutes`, refused (B2-2); the attestation failing on an |
| - unknown service-linked disk action (B2-3); the console census for a box-started |
| + stopped, all sources empty, an event alone, a describe alone, a |
| + `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, |
| + 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 |
| + `Pending`/`InService`, a confirmer not `active`, a region mismatch, a |
| + second confirmer losing the create-only race, and an emptied region |
| + whose dead box is still `active`: confirmed on a `terminated` read, |
| + refused on NotFound or `stopped`, B2-6); the console census for a box-started |
| relocation (a stale report accepted with an armed guard, refused with |
| no `compute` binding, no armed-guard report or a floor mismatch, and |
| unchanged for a console-started operation); continuous files with a |
| @@ -1599,9 +1476,6 @@ rev 4.2's table; this mapping says where each now lives. |
| participation at once, and a crash leaves at most a refusal, cleared |
| by retry; a lease lost during `probing` with cleanup failing, and an |
| unreadable controller record, both refusing the update (B1-5). |
| -- **IAM:** the volume guard refuses `AttachVolume`, `DetachVolume`, a |
| - `carlos:role` tag change 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 |
| row; the edge backhauls to the executor; relocate by drain through |
| @@ -1617,14 +1491,16 @@ None. |
| Rev 4.2's three were ruled as H7, H8 and H9 (2026-10-04). Rev 5's first |
| three were ruled on 2026-10-06 as H14 (the box-side reservation check, |
| -§5.10), H15 (the running-time volume record, §5.9 and §6) and H16 |
| -(automatic enrollment, §5.1, L19). |
| +§5.10), H15 (the running-time volume record, since superseded by H19) |
| +and H16 (automatic enrollment, §5.1, L19). |
| Astra's rev 5 review raised two more, ruled the same day as H17 (an |
| enrolled box in another region confirms the first box of an emptied |
| region, §5.1, §6, L19) and H18 (a box-started relocation accepts a |
| console's newest report when its box's update guard is armed, §5.9, |
| -L20). |
| +L20). Astra's rev 5 round 3 found more ways around the volume guard; |
| +Paul answered with H19, which takes disk evidence out of the failover |
| +path (§5.9, §22). |
| ## 12. Out of scope, for the later specs |
| @@ -1771,12 +1647,11 @@ changes how some of it is used. Plan 1b is written against rev 5. |
| greatest SHA-256 of `host + "\x00" + reference` (H12). The first two |
| rules stand. |
| - **`termfence`'s binding and inputs.** `Verify` binds to a |
| - `boxid.Identity`; it must bind to the roster entry's `cloud`, take the |
| - newest volume record as an input and require it within the 2-hour |
| - bound with every volume `DeleteOnTermination` (H15), and produce §5.9's |
| - record. `FromDescribe` and `FromEvent` stay as the two terminated |
| + `boxid.Identity`; it must bind to the roster entry's `cloud` and |
| + produce §5.9's record. It takes no volume input (H19); a separate |
| + function decides chore discharge from the volume records. `FromDescribe` and `FromEvent` stay as the two terminated |
| reads; a `shutting-down` observation is never accepted. Plan 1b adds |
| - the volume recorder, §5.10's two checks, the volume guard and, for |
| + the volume recorder, the discharge check, §5.10's two checks and, for |
| spec 4, the membership confirmation (H16). |
| **Stays as built.** |
| @@ -1806,10 +1681,10 @@ 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. |
| -Rev 5.1 adds to plan 1b: the hold, release and removed-volume rules and |
| -their CLI (§5.9), the guard attestation and the tag statements (§6), the |
| -local install receipt (§5.8), and root's refusal on any controller |
| -record (§5.10). |
| +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 |
| +(§5.10). Rev 5.1 and 5.2's hold, release, guard attestation and SCP are |
| +withdrawn by H19 and are not built. |
| ## 20. Astra rev 5 round 1 dispositions |
| @@ -1847,3 +1722,43 @@ and AWS's documented API and policy contracts before acceptance. |
| | B2-4 P1 the files pin follows the database baseline and can drop published files | accepted: the files pin is the newest manifest in the admitted chain, chosen independently; the files live set covers it through `holder.generation` and any running op's pin (§5.6, §5.8, L13) | |
| | B2-5 P2 later probe stamps invalidate the receipt and invite a reinstall | accepted: the receipt binds to `op.journal.install_stamp`, the stamp of the CAS that handed `op.exec`; after the first admission the local install is never remade, and a lost receipt is `stuck` (§5.8, L1) | |
| | B2-6 P2 the dead box stays `active`, so H17 never fires | accepted: the confirmer requires a positive `terminated` read for every `active` or `quarantined` enrollment in the region, in the same pass, as part of confirming membership; it is not a fence and retires nothing. The new box then fences through the ordinary path (§5.1, §7, L19) | |
| + |
| +## 22. Astra rev 5 round 3 dispositions, and H19 |
| + |
| +Reviewed rev 5.2 at 075d709f (`CODEX-FINDINGS-REGION-HA-REV5-3.md`). |
| +Each finding was checked against AWS's documented contracts. All five |
| +are about the volume guard. Paul's ruling H19 (2026-10-06) took the disk |
| +out of the failover path, so they no longer bear on safety. |
| + |
| +| Finding | Disposition | |
| +|---|---| |
| +| B3-1 P1 Recycle Bin keeps volumes deleted on termination | correct about AWS, and moot for the fence under H19: a retained volume cannot run or write, and is never admitted as the executor. For chore discharge it is a retention concern for the operator path; §6 asks the deployment to configure no retention rule over platform volumes (§5.9, §6) | |
| +| B3-2 P1 `CopyVolumes` bypasses the copy guard | correct, and moot under H19 for the same reason: a copy is a data-retention concern, never a second writer (§5.9) | |
| +| B3-3 P1 another Auto Scaling group can overwrite the protected tag | moot: H19 removes the tag-conditioned guard; nothing in the fence or discharge reads the `carlos:role` tag any more (§5.1, §6) | |
| +| B3-4 P1 concurrent releases move the revocation cutoff back | moot: holds, releases and the change role are withdrawn (§5.9, §6) | |
| +| B3-5 P2 the release barrier omits Auto Scaling workflows | moot: there is no release barrier. A root replacement under any workflow shows as a removed volume, which only keeps the chores open (§5.9) | |
| +| B2-1, B2-2, B2-3 (partly resolved in round 3) | withdrawn with the mechanisms they patched; the property they protected is no longer needed for execution (H19) | |
| + |
| +**Earlier volume-guard findings, revisited.** B1-3 (operator changes |
| +before a refresh), B1-4 (an unprotected tag, the non-Organizations |
| +fallback), B2-1 (root replacement, snapshots, images), B2-2 (release |
| +authority) and B2-3 (service-linked roles) all showed ways a disk could |
| +outlive its box despite the records. Under H19 each such disk is a |
| +cleanup concern: the box is fenced by its `terminated` read alone, and |
| +a surviving disk can never become the executor, because admission needs |
| +`op.exec` to name an enrolled, active box (claim C4, HA7), and a new |
| +instance is a new enrollment. What remains of them is one cheap rule: |
| +any `false` flag or removed volume in any record keeps the dead box's |
| +chores open for an operator. Their dispositions in §20 and §21 stand as |
| +history. |
| + |
| +**Checked after removing the guard.** H17's confirmer no longer reads |
| +the `carlos:role` tag, and needs nothing else from the guard. The |
| +volume recorder stays, for discharge only. §5.10, the census (L5, L20), |
| +relocation (§5.8) and the fence read no disk evidence. CC11 lets a |
| +relocation start while a dead box's `park-local` is open, since it |
| +names only that box. A surviving disk attached to a new instance brings |
| +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. |