amadan
spec: region HA spec 1 rev 5.2, Astra rev 5 round 2 (B2-1 to B2-6)
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+227
−65
docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md+227 −65
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 184b425ff..2c590675a 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.1**. DRAFT. Plan 1a is built and merged |
| +Design, 2026-10-06, **rev 5.2**. DRAFT. Plan 1a is built and merged |
| (aadb860); nothing else here is built. |
| +**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 |
| +covers root-volume replacement, snapshots and images (B2-1), and Auto |
| +Scaling's own service-linked role, through the APIs that start its work |
| +(B2-3). A hold is closed by revoking the change role's sessions and |
| +waiting for in-flight disk tasks before the validating record (B2-2). |
| +The files manifest is pinned from the newest admitted generation, not |
| +from the database baseline's (B2-4). The local install receipt is bound |
| +to the installation stamp, and a box that has admitted a writer never |
| +reinstalls (B2-5). H17's confirmer may treat an enrolled box as gone on |
| +a positive `terminated` read (B2-6). |
| + |
| **Rev 5.1** answers Astra's first review of rev 5 |
| (`CODEX-FINDINGS-REGION-HA-REV5-1.md`, cited **B1-n**): five P1, three P2 |
| and one P3, all accepted; §20 maps each. A restarted probe now restores |
| @@ -319,9 +332,9 @@ the group name from the deployment's configuration. Anything else, a |
| fixed box included, is enrolled only with an operator's approval. Spec 4 |
| builds this; the claim's D7 needs to allow it (L19). |
| -**A region with no enrolled box (H17).** When the roster shows no |
| -`active` box in the target region, the confirmer may be any `active` |
| -enrolled box of another region, acting as a regional worker of its own |
| +**A region with no enrolled box (H17).** When the target region has no |
| +**live** enrolled box, the confirmer may be any `active` enrolled box of |
| +another region, acting as a regional worker of its own |
| region and checking its own entry first. This is the only thing it ever |
| does across regions. Its confirmation binds to the target region's |
| group, not to anything the new box says: |
| @@ -335,6 +348,19 @@ group, not to anything the new box says: |
| zone in that AWS region; then `DescribeInstances` there, requiring the |
| instance `pending` or `running`, the deployment's `OwnerId` and the |
| `carlos:role` tag; |
| +- **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 |
| + confirmer therefore describes, in the same region and the same pass, |
| + every other enrollment the roster lists there as `active` or |
| + `quarantined`, and requires each to read **`terminated`**, positively, |
| + for its roster `cloud`. `InvalidInstanceID.NotFound`, any other state, |
| + an error or a partial reply refuses the confirmation (absence is never |
| + evidence; a box that has left `DescribeInstances` goes to an operator). |
| + The confirmation lists those reads (`terminated_enrollments: [{box, |
| + enrollment, instance_id, observed_at, request_id}]`). They only show |
| + the region has no live worker. They are not a termination fence, they |
| + discharge nothing, and they never retire a roster entry; |
| - it writes the same create-only object, |
| `control/box-enrollment/<box reference>/<instance id>.json`, with |
| `{target_placement, aws_region, group_arn, instance_id, |
| @@ -343,12 +369,14 @@ group, not to anything the new box says: |
| write: one creates it, the other gets a refusal, reads it, and stops. |
| The console accepts a cross-region confirmation only if, at enrollment, |
| -the roster still shows no `active` box in the target region, the |
| -confirmer was `active`, the group ARN equals the roster's for that |
| +every enrollment the roster lists as `active` or `quarantined` in the |
| +target region appears in the confirmation's `terminated_enrollments` |
| +(any new one refuses), the confirmer was `active`, the group ARN equals the roster's for that |
| 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 and recovers the hosts (§5.9, §5.8). So |
| -a one-box region recovers automatically (§7). |
| +records, fences its predecessor through the ordinary §5.9 path (its own |
| +terminated read and the predecessor's last volume record), 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 |
| eligible, and a claim naming one is never relocated automatically: an |
| @@ -567,8 +595,14 @@ stands. |
| - **Each cold admission starts a new manifest.** Under P6-D4 every wake |
| is a cold admission into a new generation. Before the app starts, the |
| admitting box writes `files/<new generation>/manifest.json` |
| - create-only, as a copy of the predecessor generation's manifest read by |
| - exact version from the same baseline it restores. Its entries keep |
| + create-only, as a copy of the **files pin**: the newest manifest in the |
| + admitted chain, read by exact version (B2-4). That is the manifest of |
| + `holder.generation` as observed, or, if that generation has none (its |
| + copy never completed, so its app never started), of the nearest |
| + predecessor in `holder.admissions` that has one. It is chosen |
| + independently of the database baseline: the files publisher and the |
| + replicator make progress separately, so a generation can hold |
| + published files before its first database upload. Its entries keep |
| naming the predecessor's objects where they are, so an unchanged file |
| is never uploaded again. A late write from the predecessor's publisher |
| lands in the predecessor's prefix, which nothing admitted reads again. |
| @@ -576,7 +610,11 @@ stands. |
| after a day" is withdrawn (plan 1a never built it). A dead generation's |
| `files/<generation>/` prefix is retired with that generation, by the |
| `park-generation` chore `PublishGeneration` queues, except objects that |
| - a manifest in the live set still names (L13). The at-rest sweep treats |
| + a manifest in the live set still names (L13). The **files live set** is |
| + every manifest from the files pin through `holder.generation`, plus any |
| + manifest a running operation has journaled in its pin, and every |
| + object they name. A park that runs while an operation is in progress |
| + keeps all of them. The at-rest sweep treats |
| `files/` as part of the location, never as residue to classify |
| blindly (claim P6-D3). |
| @@ -662,7 +700,7 @@ replication. |
| | `pinning` | a worker CAS citing the receipt or the fence: `op.exec: none`, a non-installing transition that keeps the stamp (claim R6-4, D5's form). Then it selects and journals the **pinned recovery set** (below) | `none` | unchanged | `from` held (if alive); `to` held | nobody | |
| | `installing` | a worker CAS that journals the pin and a fresh prepared-generation id `P`, hands `op.exec` to `to`, and writes `holder.stamp` = this CAS's `gen` (R6-4: a new installation), adding `to` to `touched.boxes`. `to` activates that stamp under the host guard (claim §6.4), writes its inventory entry, **builds `P`** and makes its **local install** (below) | `to` | `S'` | `to` held; `from` held | nobody: `to` writes local state under the guard, starts no app and admits no writer | |
| | `installed` | a worker CAS once `P`'s install manifest is complete and verified, journaling `P`'s prepared authority (claim P6-D3). The executor then journals its **local install receipt** by CAS, if this CAS did not already carry it (a replacement makes its own, below) | `to` | `S'` | as `installing` | nobody: the executor may make its local install, nothing else | |
| -| `probing` | `to` enters it by CAS, which requires a local install receipt for exactly `op.exec`, its enrollment and `holder.stamp`; then each probe attempt is one cold `AdmitWriter` (below), then the probe (moves §7.7, same region), within the probe deadline | `to` | `S'`, kept by the first admission | as `installing` | `to`, writer, probe only | |
| +| `probing` | `to` enters it by CAS, which requires a local install receipt for exactly `op.exec`, its enrollment and `op.journal.install_stamp`; then each probe attempt is one cold `AdmitWriter` (below), then the probe (moves §7.7, same region), within the probe deadline | `to` | `S'`, kept by the first admission | as `installing` | `to`, writer, probe only | |
| | `probe-failed` | `to` runs the release sequence for its own session | `to` until evidence | unchanged | as `installing` | nobody | |
| | `serving` | a worker CAS back to `serving` with `participants: [to]`; `from` gets a `park-local` chore unless it is discharged under H10 (§5.9) | `to` | `S'` | `to` ready; `from` held until its chore retires the row | `to` | |
| @@ -713,8 +751,11 @@ The journal entry is `{"released_by": "<box>", "generation": "<G>", |
| `holder.generation`, the unfinished run in `holder.admissions` and the |
| marker, all in this region's bucket (claim §6.2a, §6.4a item 3). It |
| journals the plan's exact object versions (the snapshot and every LTX |
| -file after it, contiguous) and the exact version of the files manifest |
| -of the same generation, files and timers included. |
| +file after it, contiguous), and, chosen separately, the exact version of |
| +the **files pin** (§5.6: the newest manifest in the admitted chain, not |
| +the database baseline's generation), with files and timers included. |
| +The two can come from different generations; each is the newest |
| +durable state of its own publisher (B2-4). |
| - **After a release sequence** (drain, rebalance, probe failure): the set |
| must reach the journaled `final_txid` and `manifest_seq`. If the listing |
| @@ -761,13 +802,28 @@ activated: |
| as the relocation's inputs (P6-D3); |
| - journals each step locally, and then, last, records its **local |
| install receipt** in the op journal by CAS: |
| - `local_install: {box, enrollment, stamp, files_manifest_version, |
| - journal_sha256}`. |
| - |
| -A receipt counts only for the box, enrollment and stamp it names, so a |
| -replacement executor (new stamp, below) never inherits its |
| -predecessor's. Remaking the local install is not a reinstall: `P` is not |
| -touched. |
| + `local_install: {box, enrollment, install_stamp, |
| + files_manifest_version, journal_sha256}`. |
| + |
| +**`install_stamp`** is the stamp of the CAS that handed this box |
| +`op.exec` (`installing`, or a replacement's), journaled by that CAS as |
| +`op.journal.install_stamp`. It is the installation's provenance, not the |
| +current writer's stamp: later probe admissions take new stamps (§6.4a |
| +item 4) and leave it alone (B2-5). A receipt counts only when its box, |
| +enrollment and `install_stamp` equal `op.exec`, its enrollment and |
| +`op.journal.install_stamp`, so a replacement executor never inherits its |
| +predecessor's. Remaking the local install before the first admission is |
| +not a reinstall: `P` is not touched. |
| + |
| +**After the first admission, the local install is never remade |
| +(B2-5).** Once any admission entry names `P` (or a later generation of |
| +this op), the box's local files, env and wake state are the live state |
| +of that writer lineage. A new agent on the same box stops the app and |
| +admits a new session, as for any cold wake; it never reapplies `P`'s |
| +files or timers. A box that finds its receipt missing after that point |
| +has lost local state it cannot rebuild from `P`: the op goes to `stuck`, |
| +and the operator resolves it (or a fence makes it a nested failover |
| +from `holder.generation` and the files pin). |
| **The probe's admission.** Each probe attempt is one `AdmitWriter` |
| (claim §6.4a), made by `to` as `op.exec`, bound to the observed `op.id` |
| @@ -829,8 +885,9 @@ admitted reads again, and which publication retires. |
| **The no-reinstall boundary (A1-3).** Once the `installed` CAS succeeds: |
| - nobody builds `P` again: replay from `installed` or `probing` goes |
| - forward (local install if the executor has no receipt, probe, then |
| - `serving`), never back to `installing`; |
| + forward (the local install only if the executor has no receipt and no |
| + admission has named `P`; then the probe, then `serving`), never back to |
| + `installing`; |
| - `P` is opened at most once. After its first admission, every restart |
| takes a fresh generation from its predecessor; |
| - a worker or `to` that paused and resumes revalidates the phase under |
| @@ -957,8 +1014,8 @@ record is never more than about an hour old: |
| 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 tags as described, so the fence |
| - can check the guard's tag (§6). |
| +- 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 |
| @@ -969,22 +1026,48 @@ 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, at}`), and only then assumes that role with |
| - the session tag `carlos:volume-hold = <id>`, which the role's trust |
| - policy requires. A box with a hold that has no later release is never |
| - fenced automatically: its termination goes to the operator path. |
| + (`{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, |
| - the new record carries `removed_volumes`, and that also suspends disk |
| + 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.** `carlos ops box volumes release <box> <hold id>` resumes it |
| - only when a worker's running record written after the hold shows every |
| - attached volume `true`, and, for every volume removed since the |
| - enrollment's last release, the operator attests (as in claim D2) that |
| - it was destroyed or never held host artifacts. The CLI writes |
| - `release-<id>.json` create-only, naming the record and each |
| - attestation. The fence then needs a running record newer than the |
| - release. |
| +- **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 |
| @@ -1200,29 +1283,76 @@ operations. |
| - **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` and |
| - `ec2:DetachVolume` on instances tagged |
| - `aws:ResourceTag/carlos:role = platform-box`. `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; |
| - - `ec2:CreateTags` and `ec2:DeleteTags` on any instance when |
| + - `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 but |
| - nobody can strip, add or change the tag on a running one. |
| + `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 tag `carlos:volume-hold` (§5.9's hold). |
| - Every other operator role is denied these actions like everyone else. |
| + 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, that the policy is |
| - attached with exactly these statements, and that no service-linked |
| - role in the account can modify, attach or detach volumes on running |
| - instances, and writes a root-signed **guard attestation**, |
| - `control/volume-guard.json` (`{account, policy_id, policy_sha256, |
| - checked_at, operator}`). The fence requires a valid one for the box's |
| + 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 |
| @@ -1290,7 +1420,10 @@ operations. |
| | 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; a termination meanwhile goes to the operator (§5.9, B1-3). | |
| +| 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 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). | |
| @@ -1349,8 +1482,10 @@ operations. |
| `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 and a removal of the `carlos:role` tag by a non-operator role |
| - and by an ordinary operator role are refused, and that the |
| + 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. |
| The rehearsal also enrolls a box into a dev region with no `active` |
| box, confirmed from another region (H17), and checks that the |
| @@ -1367,8 +1502,8 @@ 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 required before `probing`; 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` or `carlos:role` tag change on platform boxes except by the hold-gated volume-change role). A `shutting-down` read is never evidence. Stopped, unclear and vanished boxes keep D2's operator path unchanged. | Ruled (H10, H15) | |
| +| 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) | |
| | 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) | |
| @@ -1379,13 +1514,13 @@ the text. |
| | L10 | claim §6.1, §6.6 P6-D1, `internal/stopevidence` | A writers-stopped check for release step 1: cgroup empty, no member processes, and database holders limited to the agent's own identified replicator descriptors. `Collect` stays unchanged for step 4. | Requested | |
| | L11 | claim §4 (CC11), `hostclaim.StartGuard` | A `park-generation` chore in the region does not block a `relocating` start there: relocation writes only its own new prepared generation, never one being retired. Under P6-D4 nearly every recently woken host has one, which would hold failover up to the park horizon. | Requested | |
| | L12 | claim C4, §8 (CC10), §6.6 P6-D2; moves §9.6 | Reconcile's row cases for `relocating` (§5.3): held participant rows; a former executor's row kept held until its `park-local` retires it; the 10-minute sweep as a stated exception to C4 for kept rows (H9). | Requested | |
| -| L13 | claim C3, §6.2a, §6.6 P6-D3 | The files publisher is a second ordinary-replication exception, bound to `{location, generation, session}`. `files/<generation>/` belongs to that generation for the classifier; `park-generation` retires it except objects a live manifest names. | Requested | |
| +| L13 | claim C3, §6.2a, §6.6 P6-D3 | The files publisher is a second ordinary-replication exception, bound to `{location, generation, session}`. `files/<generation>/` belongs to that generation for the classifier; `park-generation` retires it except objects named by the files live set: every manifest from the files pin through `holder.generation`, and any manifest a running operation's pin journals (B2-4). | Requested | |
| | L14 | moves §7.10 | A target terminated mid-move may be taken off the move by the termination fence, as M16's evidence, automatically, under the same before-commit rules. Moves decides what the move does then; the placer only supplies the fence. | Ruled (H10) | |
| | L15 | moves §7.1, §7.3, §19.1 | A move into a multi-box region names its target **box** in the start CAS, chosen by `choose()`. Readiness, evidence, install and recovery bind to that box; replacing it is an explicit fenced transition (A1-10). | Ruled (H12) | |
| | L16 | moves §5.1, §7.6, P6-D3's provider | Relocation's install reuses the landing's `building` and `published` phases and the prepared-generation authority, with a pinned set of remote versions as the source in place of a staged replica. One shared routine, so both get the same anchor and manifest rules. | Requested | |
| | L17 | moves §6.1, §8, §9.4 | Every installation, a move's landing included, writes a files manifest in its new generation (§5.6), so unchanged files stay recoverable after the next failure; the archive at the cut stays. Timer freezing and draining apply to `relocating` holds. | Requested | |
| | L18 | joint model, moves §14.2 | `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, an unenrolled reference, a volume without `DeleteOnTermination`, a crash mid-install, late file uploads and late PUTs after termination. | Requested | |
| -| L19 | claim §10.1 D7 (enrollment), with P3 | An Auto Scaling box is enrolled by the console with no operator when its `boxid` evidence verifies (deployment account, the region's AWS region) and a regional worker's create-only confirmation shows it a current member of the region's group (§5.1). Every other enrollment stays operator-approved. Spec 4 builds it. For a region with no `active` box, any `active` box of another region confirms, by the same create-only write, bound to the group ARN the roster records for that placement; its cross-region rights are the two read-only describes and nothing else (H17). | Ruled (H16, H17) | |
| +| L19 | claim §10.1 D7 (enrollment), with P3 | An Auto Scaling box is enrolled by the console with no operator when its `boxid` evidence verifies (deployment account, the region's AWS region) and a regional worker's create-only confirmation shows it a current member of the region's group (§5.1). Every other enrollment stays operator-approved. Spec 4 builds it. For a region with no live enrolled box (every enrollment there read `terminated`, positively, in the same pass, B2-6), any `active` box of another region confirms, by the same create-only write, bound to the group ARN the roster records for that placement; its cross-region rights are the two read-only describes and nothing else (H17). | Ruled (H16, H17) | |
| | L20 | claim §10.1 D7 (required actors, console reports) | For box-started relocations only, a console's newest report counts however old if it met every floor check and the console's `compute` box has reported its D1 root update guard armed with the same floor digest. Every other census rule is unchanged. | Ruled (H18) | |
| **Rev 4.2's requests, mapped.** K1 is L8. K2 is L1, with L9 to L11. K3 |
| @@ -1426,8 +1561,12 @@ rev 4.2's table; this mapping says where each now lives. |
| `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, and a second confirmer |
| - losing the create-only race); the console census for a box-started |
| + 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 |
| 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 |
| @@ -1444,7 +1583,11 @@ rev 4.2's table; this mapping says where each now lives. |
| any other holder fails step 1); a failover admission declaring |
| `writes_lost` for `from`'s session and a drain declaring nothing; the |
| start refused when the roster reserves an update for `from` or `to`; |
| - probe attempts one, two and three, with attempt three restoring |
| + a files update published by a probe session before its first database |
| + upload, then termination: the files pin keeps it while the database |
| + baseline falls back (B2-4); a crash during `probing` after the second |
| + admission: no reinstall, and the receipt still valid by |
| + `install_stamp` (B2-5); probe attempts one, two and three, with attempt three restoring |
| attempt two's replicated writes and declaring attempt two's session |
| (B1-1); a target terminated at `installed` replaced by one that makes |
| its own local install before probing, and a `probing` CAS refused with |
| @@ -1685,3 +1828,22 @@ before acceptance. |
| | B1-7 P2 a dead console stays in the D7 census | accepted: claim D7 does require every console. Console enrollments gain a `compute` binding; a console on a fenced box is excluded. A live console with a stale report was ruled as H18 (§5.9, L5, L20) | |
| | B1-8 P2 automatic enrollment cannot bootstrap an emptied region | accepted: §2 makes a confirmer an active enrolled box in the region, so none is left. ruled as H17: an enrolled box in another region confirms, with read-only cross-region describes only, so one-box regions recover automatically (§5.1, §6, §7, L19) | |
| | B1-9 P3 stale code citations | accepted, checked on main: `provision.go:49`, `reconcile.go:348`/`:820`, `:192`, `:215`, `activator.go:1164-1168`, `:2204`, `edge.go:2466`, `main.tf:521`. Disposition tables §13 to §17 keep their historical anchors | |
| + |
| +## 21. Astra rev 5 round 2 dispositions |
| + |
| +Reviewed rev 5.1 at fdc0fe07 (`CODEX-FINDINGS-REGION-HA-REV5-2.md`). |
| +Each finding was checked against claim 98b45332, moves a4711728, main |
| +and AWS's documented API and policy contracts before acceptance. |
| + |
| +| Finding | Disposition | |
| +|---|---| |
| +| B1-2 partly resolved: the receipt dies with the next probe stamp | answered by B2-5 | |
| +| B1-3 partly resolved: release can precede authorized mutations | answered by B2-2 | |
| +| B1-4 partly resolved: root replacement unguarded; the attestation conflicts with Auto Scaling | answered by B2-1 and B2-3 | |
| +| B1-8 partly resolved: H17's emptiness test is circular | answered by B2-6 | |
| +| B2-1 P1 `CreateReplaceRootVolumeTask` bypasses the guard | accepted: added to the deny, with snapshots and images (which also leave a copy of the disk), the hold workflow and the rehearsal; a replaced root volume shows as removed (§5.9, §6, §8, L2) | |
| +| B2-2 P1 a release does not close the change's authority | accepted: the hold names its instance and the role's exemption is limited to it; release revokes the role's earlier sessions, waits for no attaching, detaching, replace-root, snapshot or image task and for the signature-age bound, then needs a validating record after that barrier. Session tags are acknowledged as the caller's word; the hold-first order is the operator trust boundary, as in claim D2 (§5.9) | |
| +| B2-3 P1 Auto Scaling's service-linked role defeats the attestation | accepted: the attestation no longer asserts that no service role can touch a disk. It reads every service-linked role's managed policy at its default version and requires each disk or tag action to map to an initiating API the SCP denies; Auto Scaling's (refresh, group create and update, warm pool, attach) are denied but for the hold-gated role; a policy version change invalidates it (§6, §7) | |
| +| 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) | |