amadan
spec: region HA spec 1 rev 5, Paul's rulings H14-H16 (relocation starts, volume records, enrollment)
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+253
−103
docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md+253 −103
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 17ece865c..ec08eea19 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 |
| @@ -7,7 +7,7 @@ Design, 2026-10-06, **rev 5**. DRAFT. Plan 1a is built and merged |
| stands, rev 6.25 (413b12cb on `design-replica-ownership`), with its |
| library on main (`internal/hostclaim`, `internal/hostguard`, |
| `internal/stopevidence`, `internal/park`, `internal/genselect`), and |
| -records Paul's rulings H10 to H13 of 2026-10-06. Rev 4.2 was written |
| +records Paul's rulings H10 to H16 of 2026-10-06. Rev 4.2 was written |
| against claim rev 6.3 and asked for changes K1 to K11. Those sessions |
| never saw the request, and the claim moved on: box references are |
| opaque, `control/host-actors.json` is the one roster, every writer is |
| @@ -19,9 +19,14 @@ records as authority (H11), the trusted local copy (H13), and its own |
| it had, and installs through the claim's prepared-generation and |
| `AdmitWriter` rules instead. The termination fence stays automatic, now |
| also requiring every EBS volume to be deleted with the instance (H10). |
| -§9's K-table is replaced by requests L1 to L18 against claim rev 6.25 |
| -and moves rev 7.17. §19 says what of plan 1a is superseded. §11 lists |
| -three points the claim's current text leaves for Paul. |
| +A dev test showed a terminated instance's describe lists no volumes, so |
| +that proof comes from a record taken while the box runs, kept true by |
| +IAM (H15). A relocation is started without a console: the boxes, not a |
| +roster reservation, keep it apart from executable updates (H14, §5.10). |
| +§9's K-table is replaced by requests L1 to L19 against claim rev 6.25 |
| +and moves rev 7.17. §19 says what of plan 1a is superseded. The three |
| +points rev 5 first left open were ruled the same day as H14 to H16 |
| +(§11). |
| Rev 4.2 answered Astra round 5 (`CODEX-FINDINGS-REGION-HA-5.md`, A5-1), |
| and Astra round 6 (`CODEX-FINDINGS-REGION-HA-6.md`) found it ready for |
| @@ -79,10 +84,15 @@ are alive, and on #212 option B for box references. |
| | H11 | **(2026-10-06) The roster is the claim's `control/host-actors.json`** (claim §10.1 D7). Region HA drops its own `control/boxes/<id>.json` authority. `internal/boxid`'s AWS-signed IMDS identity verification becomes the evidence required to enroll a box. Enrollment records the proven account, region and instance id in the roster entry's `cloud` field, and the termination fence binds to that entry. Box references are opaque (claim §2, rev 6.16) and follow #212 option B: the label is the key, the instance id is private. | |
| | 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.) | |
| +| 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 H13 supersede only what they name: H10 adds the volume condition |
| -to H1, H11 replaces §5.1's box records as authority, H13 replaces HA3 |
| -and §5.5. Everything else in H1 to H9 stands. |
| +H10 to H16 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, and H16 settles enrollment for spec 4. |
| +Everything else in H1 to H9 stands. |
| Standing rulings this spec keeps: |
| @@ -274,6 +284,18 @@ Enrollment is the claim's (D7, L7). For region HA it must: |
| the operator-approved enrollment (claim §10.1 P3), so the separate bind |
| object is not used. |
| +**Auto Scaling boxes (H16, spec 4).** The console enrolls a box launched |
| +by the region's Auto Scaling group itself, with no operator, when two |
| +pieces of evidence agree: its `boxid` record verifies with the |
| +deployment's account and the region's AWS region, and a regional worker |
| +has written a create-only membership confirmation, |
| +`control/box-enrollment/<box reference>/<instance id>.json`, from a fresh |
| +read-only `autoscaling:DescribeAutoScalingInstances` showing the instance |
| +a current member (`Pending` or `InService`) of that region's group, with |
| +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 box whose entry is not `active` with a proven `cloud` is never |
| eligible, and a claim naming one is never relocated automatically: an |
| operator resolves it. |
| @@ -556,13 +578,16 @@ executor change the claim's `placing` refuses (P5-D5). |
| other effect (claim C2): |
| {from, to, to_enrollment, region, reason, stamp_from, |
| - generation_from, fence?} |
| + generation_from, fence?, directory_revision} |
| `reason` is `drain`, `rebalance` or `failover`. For failover, `fence` |
| names the termination fence record (§5.9) by key and SHA-256. The start |
| is refused by the claim's start guard (claim §4, CC11, as amended by |
| -L11), and when `to` is not eligible for the host (§2). Participants are |
| -`from` and `to`, or `to` alone for a failover. |
| +L11), when `to` is not eligible for the host (§2), and when the roster |
| +shows an executable update reserved for `from` or `to` (§5.10, H14). |
| +`directory_revision` is the roster revision that check read. No console |
| +reservation is taken. Participants are `from` and `to`, or `to` alone |
| +for a failover. |
| **Who acts.** Every phase is a claim CAS conditional on `op.id`, the |
| phase and the ETag. The recovery owner for every phase is the region's |
| @@ -779,19 +804,63 @@ detection plus restore (spec 3). |
| ### 5.9 The termination fence |
| -**What counts (A1-1, A1-11, H10).** A box is fenced by termination only |
| -when one fresh `DescribeInstances` reply, made by a regional worker in |
| -the box's AWS region with its own read-only rights, shows all of: |
| +**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`, and lists at least one EBS volume. It, and every record |
| + written after it, shows every attached EBS volume |
| + `DeleteOnTermination: true`. |
| +2. **The IAM guard is in place** (§6): nobody but an operator role can |
| + change a platform box's block device mapping or attach a volume to it, |
| + so the record cannot go stale behind the platform's back. |
| +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. |
| + |
| +**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: |
| + |
| + control/box-volumes/<enrollment>/<observed_at>.json |
| + |
| +```json |
| +{"v": 1, "box": "<box reference>", "enrollment": "<enrollment>", |
| + "cloud": {"provider": "aws", "account": "123…", |
| + "region": "eu-west-1", "instance_id": "i-0abc…"}, |
| + "instance_state": "running", |
| + "block_devices": [{"device": "/dev/xvda", "volume_id": "vol-…", |
| + "delete_on_termination": true, "status": "attached"}], |
| + "observed_at": "<RFC3339>", "request_id": "<EC2 request id>", |
| + "written_by": {"box": "<reference>", "enrollment": "<enrollment>"}} |
| +``` |
| -- the instance id, account (`OwnerId`) and region equal to the box's |
| - roster entry's `cloud` (H11, HA7); |
| -- state exactly `terminated`; |
| -- every EBS volume in `BlockDeviceMappings` with `DeleteOnTermination: |
| - true`, and at least one mapping present. |
| +- 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. |
| -If any volume was not `DeleteOnTermination`, or the reply carries no |
| -mappings, the box is not fenced automatically; the operator path |
| -applies (§11 question 2 is about the second case). |
| +**What never counts.** |
| - `stopped` and `stopping` do not count, because a stopped box can start |
| again with its disk. A missing instance, `InvalidInstanceID.NotFound`, |
| @@ -814,11 +883,12 @@ enrollment, create-only (L4): |
| "cloud": {"provider": "aws", "account": "123…", |
| "region": "eu-west-1", "instance_id": "i-0abc…"}, |
| "state": "terminated", |
| - "block_devices": [{"device": "/dev/xvda", "volume_id": "vol-…", |
| - "delete_on_termination": true}], |
| - "observed_at": "<RFC3339>", "request_id": "<EC2 request id>", |
| - "trigger": "describe" | "event" | "activity", |
| - "event_id": "<EventBridge event id, when trigger=event>", |
| + "volume_record": {"key": "control/box-volumes/<enrollment>/<…>.json", |
| + "sha256": "…"}, |
| + "observed_at": "<RFC3339>", |
| + "via": "describe" | "event" | "activity", |
| + "request_id": "<EC2 request id, when via=describe>", |
| + "event_id": "<EventBridge event id, when via=event>", |
| "written_by": {"box": "<reference>", "enrollment": "<enrollment>"}} |
| ``` |
| @@ -827,27 +897,31 @@ 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 triggers, one proof.** The record always comes from a describe, |
| -because only a describe carries `BlockDeviceMappings`. The other two |
| -sources say when to look: |
| +**Three ways to observe `terminated`.** Since the volumes come from the |
| +record, 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 |
| deployment's account to an SQS queue (14-day retention). Plan 1a |
| built one queue per box. The queue's policy accepts messages only from |
| that rule's ARN. An event whose account, region and instance id match |
| - a roster entry makes the worker describe the instance at once. |
| -2. **A direct read.** A worker describes the region's enrolled instances |
| - on its sweep. |
| + a roster entry's `cloud` is the read, `via: "event"`. |
| +2. **A direct read.** `DescribeInstances` for the instance id, in the |
| + region, returning `terminated` with the deployment's `OwnerId`, |
| + `via: "describe"`. Workers make it on their sweep and whenever an |
| + event or the group's history suggests a termination. |
| 3. **The group's own history.** For a box launched by an Auto Scaling |
| - group, a `DescribeScalingActivities` activity terminating that |
| - instance id with status `Successful` makes the worker describe it. |
| - Spec 4 verifies this source on dev; until then it is off. |
| + group, `DescribeScalingActivities` for the region's group: an activity |
| + terminating that instance id with status `Successful`, |
| + `via: "activity"`. Spec 4 verifies on dev that `Successful` is |
| + recorded only once the instance has reached `terminated`; until then |
| + this source is off. |
| **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 describe returns the |
| -proof, there is **no automatic recovery**. The placer marks the box's |
| +`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 |
| 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 |
| @@ -868,7 +942,7 @@ alerting, and owns the loop that reads the queue and history. |
| 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), so its `park-local` chores are discharged in the same |
| + 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 |
| are reassigned to `region:<r>`, keeping their ids, operations and |
| @@ -883,6 +957,67 @@ alerting, and owns the loop that reads the queue and history. |
| durable loss record when it next runs, with timer knowledge `partial`: |
| wake state was published continuously, up to H3's window. |
| +### 5.10 Relocation starts and executable updates (H14) |
| + |
| +Claim D7 serializes a lifecycle start against executable updates with a |
| +reservation the console writes into the roster. A relocation must start |
| +when the console is down, so H14 moves the serialization to the boxes. |
| +Each side records its own intent durably first, then checks the |
| +other's, so of two that race at least one sees the other. |
| + |
| +**The worker, at the start.** Before the start CAS, the worker reads |
| +`control/host-actors.json` as an exact object and verifies its root |
| +signature (an unreadable or unverifiable roster refuses the start). It |
| +requires `to`, and `from` unless the start cites a fence, to be |
| +`active`, and requires that no entry in `activations` names `from`'s or |
| +`to`'s enrollment. It records the revision it read as |
| +`directory_revision` in the intent. It writes nothing to the roster. |
| + |
| +**A participant, before it acknowledges.** A box becomes a participant |
| +in practice when it acknowledges the operation (claim D6). Before its |
| +first execution-lease PUT, its controller: |
| + |
| +1. writes its `.hostexec/<host>.json` state as `pending`, durably (claim |
| + D6's existing state and write protocol); |
| +2. then reads root's update state: the system-update journal and root's |
| + **update-begun** marker (below). If an update is begun or in progress |
| + for this box, it refuses to acknowledge, clears its `pending` state, |
| + and retries after the update finishes. The operation cannot leave |
| + `starting` without `to`'s acknowledgement, so nothing has moved; the |
| + worker waits, or replaces `to` (§5.8). |
| + |
| +**Root, before it starts an update.** Every path that begins an |
| +executable change (system apply, explicit rollback, a guarded |
| +activation under claim D1, the console's activation reservation being |
| +acted on), under root's existing system-update lock: |
| + |
| +1. writes an **update-begun** marker, durably, beside the update journal |
| + (`/opt/carlos/system/guard/update-begun.json`, naming the update); |
| +2. then scans `<DataDir>/.hostexec/` for any host whose state is |
| + `pending` or `active`. If any is found, the box is a participant in a |
| + running claim operation: root removes its marker, refuses the update, |
| + and leaves the console's activation reservation held, to retry later; |
| +3. otherwise it proceeds. The marker stays until the update finishes or |
| + is recovered. |
| + |
| +Boot recovery of an update already begun before any participation needs |
| +no new check: no participant acknowledged meanwhile, because step 2 of |
| +the participant's side saw the marker. |
| + |
| +**The race.** If the console reserves an update for `to` after the |
| +worker's roster read, the start proceeds, and the reservation is |
| +harmless by itself. Whichever of `to`'s acknowledgement and root's |
| +begin writes its marker first, the other sees it and refuses: either |
| +the update waits until the operation returns to `serving` and D6 clears |
| +the controller's state, or the acknowledgement waits until the update |
| +finishes. Root's refusal is what closes the race (H14). A box stays a |
| +participant from its `pending` state until D6 clears it, so an update |
| +never runs under a relocation's `installing`, `probing` or release. |
| + |
| +This holds for every claim operation a box takes part in, not only |
| +relocations. L6 asks the claim to make it D7's rule for box-started |
| +operations. |
| + |
| ## 6. Infrastructure and IAM (A1-12) |
| - **Box role** keeps plan 1a's `ec2:DescribeInstances` with a condition |
| @@ -896,12 +1031,30 @@ alerting, and owns the loop that reads the queue and history. |
| 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).** 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 |
| + 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 |
| + `region-host` module create every volume with `DeleteOnTermination`. |
| + An operator who attaches or changes a volume on a platform box must |
| + refresh its volume record before leaving it (`carlos ops box volumes |
| + refresh <box>`); until the next record, the box's fence rests on the |
| + previous one, which is why §5.9 bounds its age. |
| +- **Auto Scaling enrollment (H16, spec 4).** The box role gains |
| + `autoscaling:DescribeAutoScalingInstances`, conditioned on |
| + `aws:RequestedRegion`, read-only. |
| - **Console role:** unchanged, no EC2 rights. |
| - **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/`, and fence records, |
| - `control/box-fences/`, in the control bucket. |
| + 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 |
| first write): `instances/<host>/*/files/*/manifest.json` only. |
| @@ -916,6 +1069,7 @@ alerting, and owns the loop that reads the queue and history. |
| tested against both refusals. The control bucket denies `PutObject` |
| without `s3:if-none-match: *`, and `DeleteObject` and |
| `DeleteObjectVersion`, on `control/boxes/*` (plan 1a's policy) and on |
| + `control/box-volumes/*`, `control/box-enrollment/*` and |
| `control/box-fences/*`. Each Deny is scoped to its prefix only: a |
| broad Deny on this bucket once broke every lease release. The |
| `*.bind.json` statement plan 1a added is no longer needed (§19). Data |
| @@ -936,7 +1090,9 @@ alerting, and owns the loop that reads the queue and history. |
| | 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). | |
| +| 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 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). | |
| | A forged or confused edges file names a terminated instance | ignored: identity comes only from the roster's `cloud`, proven at enrollment (HA7). | |
| | Placer dies mid-relocation | another regional worker replays from the claim (§5.8). | |
| | Target dies after its probe admitted | a nested failover from `holder.generation` (§5.8). | |
| @@ -963,8 +1119,9 @@ alerting, and owns the loop that reads the queue and history. |
| `region-ha-1` and runs at or above the HA floor; |
| - every box in the region is `active` in the roster with a proven |
| `cloud`; |
| - - the region's termination queues exist, and every attached EBS volume |
| - has `DeleteOnTermination`. |
| + - the region's termination queues exist, every box has a current |
| + volume record showing every attached EBS volume |
| + `DeleteOnTermination`, and the volume guard (§6) is in place. |
| The HA floor joins the protocol floor (claim §10, D1): every path that |
| restores an executable (system apply, rollback, boot recovery from |
| @@ -978,27 +1135,35 @@ alerting, and owns the loop that reads the queue and history. |
| 5. Rehearse on dev with two fixed boxes: create spreads across both; |
| drain one (§5.8) with `moveprobe` shaped like ips (moves §14.4), |
| including timers and a `continuous` files app; terminate one by hand |
| - and run the spec 3 placer manually. On the same dev box, record what |
| - `DescribeInstances` returns for `BlockDeviceMappings` once an instance |
| - is `terminated` (§11 question 2). |
| + and run the spec 3 placer manually. **Done on 2026-10-06 (H15):** a |
| + t4g.nano launched with a `DeleteOnTermination: true` root and a |
| + `DeleteOnTermination: false` extra volume, then terminated. While |
| + `shutting-down`, `DescribeInstances` still listed both volumes, with |
| + 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 by a non-operator |
| + role is refused. |
| 6. Then specs 2, 3, 4. |
| ## 9. Changes requested of the claim and moves specs |
| 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 H13, |
| +never received. "Ruled" means Paul's rulings of 2026-10-06 (H10 to H16, |
| 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 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, bound to the roster entry's `cloud`, every EBS volume `DeleteOnTermination`, from a describe. Stopped, unclear and vanished boxes keep D2's operator path unchanged. | Ruled (H10) | |
| +| 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) | |
| | 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) | |
| -| L6 | claim §10.1 D7 (lifecycle reservations, `actors_hold`) | A relocation started by a regional worker cannot get a console-created reservation if the console is down. The claim needs a box path. | **Open: needs Paul** (§11 question 1) | |
| +| L6 | claim §10.1 D7 (lifecycle reservations, `actors_hold`) | 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 host's controller state is `pending` or `active`. | Ruled (H14) | |
| | L7 | claim §10.1 D7, §7.3 D2, §5.9 P5-D2, §6.6 P6-D2 | Enrollment of a platform box requires `internal/boxid` evidence; it records `cloud` from it, and checks the tofu `instance_id` for a reference already in claims or edges files. No other roster, and no `control/boxes` authority. | Ruled (H11) | |
| | L8 | claim §5.1 steps 2 and 4, §5.9 P5-D2 and P5-D6 | The executor in the create intent is `choose()` (§5.2), with P5-D2's SHA-256 as the final tie-break; chosen once, never substituted; a create whose box can't complete is cancelled. | Ruled (H12) | |
| | L9 | claim §6.4a item 2, `hostclaim.AdmitWriter` | A coverage value `released`: a prepared generation built from a pin that reaches the `final_txid` a released box recorded from its stopped database, under that box's stop receipt. It declares nothing. Without it every drain declares a false loss. | Requested | |
| @@ -1011,6 +1176,7 @@ the text. |
| | 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. | Ruled (H16) | |
| **Rev 4.2's requests, mapped.** K1 is L8. K2 is L1, with L9 to L11. K3 |
| is L2 to L5. K7 is L14. K8 is L16 and L17. K9 is L18. K10 is L15. K11 is |
| @@ -1039,8 +1205,13 @@ 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, a volume without `DeleteOnTermination`, an empty mapping list, |
| - an event with no describe, all sources empty); continuous files with a |
| + 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); the volume recorder |
| + (writes on change, at least hourly, never on an unchanged sweep |
| + otherwise); continuous files with a |
| file held open (published at the deadline), inotify overflow, a file |
| that changes during its read; the create-only and replace split in |
| `hostfiles.Publish`. |
| @@ -1052,7 +1223,16 @@ rev 4.2's table; this mapping says where each now lives. |
| level-0 anchor; a release with a live embedded replicator (step 1 |
| passes with only its descriptors, step 4 passes only after `DB.Close`, |
| any other holder fails step 1); a failover admission declaring |
| - `writes_lost` for `from`'s session and a drain declaring nothing. |
| + `writes_lost` for `from`'s session and a drain declaring nothing; the |
| + start refused when the roster reserves an update for `from` or `to`. |
| +- **Starts and updates (§5.10):** root's begin and a participant's |
| + acknowledgement interleaved at every point, with a crash between each |
| + 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 |
| + 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 |
| @@ -1064,51 +1244,17 @@ rev 4.2's table; this mapping says where each now lives. |
| ## 11. Open questions |
| -Rev 4.2's three were ruled as H7, H8 and H9 (2026-10-04). The claim's |
| -current text leaves three for Paul. |
| - |
| -1. **Who reserves the actors for a relocation a box starts (L6).** Claim |
| - D7 has every protected start record a lifecycle reservation, created |
| - by the console with a CAS on the root-signed roster, so a start cannot |
| - race an executable change. A regional worker cannot write the roster, |
| - and #236 wants failover to work when the console's box is the one |
| - that died. Options: |
| - - **(a)** A box path: a relocation's start CAS requires the roster to |
| - show no executable activation reservation for `from` or `to`, and |
| - root's update path refuses to begin an activation on a box that is |
| - a participant of a running operation, read under the host guard. |
| - The serialization moves to the boxes. *Recommended.* |
| - - **(b)** Failover waits for a console to reserve. Simple, but a |
| - console outage stalls every failover, against #236's intent. |
| - - **(c)** A standing per-region reservation the console keeps for |
| - relocations. It blocks executable updates on every box it names for |
| - as long as it is held, so updates would need to release and retake |
| - it. |
| -2. **What if a terminated instance's describe has no block devices.** |
| - H10 reads `DeleteOnTermination` from the same `DescribeInstances` |
| - reply. AWS may return an empty `BlockDeviceMappings` once an instance |
| - is `terminated` (to be confirmed on dev, §8 step 5), and EventBridge's |
| - state-change event carries none. If so, H10 as written never fences. |
| - Options: |
| - - **(a)** Keep H10 as written and accept that failover is manual |
| - whenever the mappings are gone. *Only if dev shows they stay.* |
| - - **(b)** Record each box's mappings from a describe while it is |
| - `running` (at enrollment and on every sweep), deny |
| - `ec2:ModifyInstanceAttribute` and `ec2:AttachVolume` on platform |
| - boxes to every role but the operators', and fence on the terminated |
| - read plus the newest running record. *Recommended if (a) fails.* |
| - - **(c)** Also accept EventBridge's "EBS Volume Notification" |
| - `deleteVolume` result `deleted` for each recorded volume as positive |
| - proof. Best-effort delivery, so it adds to (b) and never replaces it. |
| -3. **How an Auto Scaling box is enrolled (spec 4, not blocking spec 1).** |
| - Claim P3's recommendation is operator-approved enrollment, but H5 |
| - scales out automatically. Options: **(a)** every enrollment is |
| - approved by an operator, so scale-out waits for a person; **(b)** the |
| - console enrolls a box automatically when its `boxid` evidence is in |
| - the deployment's account and region and a regional worker reports the |
| - instance a member of the region's group |
| - (`autoscaling:DescribeAutoScalingInstances`, read-only), and asks an |
| - operator for anything else. *Recommended.* |
| +None. Rev 4.2's three were ruled as H7, H8 and H9 (2026-10-04). The |
| +three rev 5 first left open were ruled on 2026-10-06: |
| + |
| +1. **Who reserves the actors for a relocation a box starts (L6).** |
| + Ruled as H14: the box-side check, §5.10. |
| +2. **A terminated instance's describe has no block devices.** Tested on |
| + dev and ruled as H15: a running-time volume record kept true by IAM, |
| + §5.9 and §6. |
| +3. **How an Auto Scaling box is enrolled.** Ruled as H16: automatically, |
| + on `boxid` evidence plus a worker's group-membership confirmation, |
| + §5.1, L19. Spec 4 builds it. |
| ## 12. Out of scope, for the later specs |
| @@ -1118,7 +1264,8 @@ current text leaves three for Paul. |
| every host off a terminated box in bounded parallel, waking always-on |
| and scheduled instances, the failover gap target. |
| - **Spec 4:** the Auto Scaling group per region, launch template and |
| - join without SSM hand steps, enrollment of new boxes (§11 question 3), |
| + join without SSM hand steps, automatic enrollment of new boxes (H16, |
| + L19), |
| ingress for boxes that come and go (a per-region NLB with fixed EIPs, |
| or an EIP pool claimed at boot), HTTP-01 certificates, steering, |
| scale-out on headroom, scale-in by drain (§5.8), per-region minimum |
| @@ -1253,11 +1400,14 @@ changes how some of it is used. Plan 1b is written against rev 5. |
| - **`chooseBox`'s last tie-break.** The lowest box id becomes P5-D2's |
| greatest SHA-256 of `host + "\x00" + reference` (H12). The first two |
| rules stand. |
| -- **`termfence`'s binding and source.** `Verify` binds to a |
| - `boxid.Identity`; it must bind to the roster entry's `cloud`, require |
| - every block device `DeleteOnTermination` and at least one mapping, and |
| - produce §5.9's record. `FromEvent` becomes a trigger: an event alone |
| - never fences (H10). |
| +- **`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 |
| + reads; a `shutting-down` observation is never accepted. Plan 1b adds |
| + the volume recorder, §5.10's two checks, the volume guard and, for |
| + spec 4, the membership confirmation (H16). |
| **Stays as built.** |