amadan
spec: region HA spec 1 rev 5.1, Paul's rulings H17-H18 (cross-region confirmer, stale console report)
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2 files changed,
+113
−62
docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md+102 −58docs/superpowers/specs/CODEX-REVIEW-BRIEF-REGION-HA-REV5-2.md+11 −4
CI passed — run details
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 ec21ab17d..184b425ff 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 |
| @@ -15,15 +15,17 @@ tag, needs an attested Organizations policy, and without one there is no |
| automatic fence (B1-4). A lost or unreadable execution-lease state keeps |
| updates out (B1-5). A source lost in `starting` turns the drain into a |
| failover (B1-6). A console bound to a fenced box leaves the census |
| -(B1-7). Code citations are refreshed (B1-9). Two points need Paul (§11): |
| -how the first box of an emptied region is enrolled (B1-8), and whether a |
| -live console with a stale report may hold up a failover (B1-7). |
| +(B1-7). Code citations are refreshed (B1-9). The two points this raised |
| +for Paul were ruled the same day: an enrolled box in another region |
| +confirms the first box of an emptied region (H17), and a box-started |
| +relocation accepts a console's newest report when its box's update |
| +guard is armed (H18). §11 is empty again. |
| **Rev 5** restates the design against the host lifecycle claim as it now |
| 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 H16 of 2026-10-06. Rev 4.2 was written |
| +records Paul's rulings H10 to H18 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 |
| @@ -39,7 +41,7 @@ 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 |
| +§9's K-table is replaced by requests L1 to L20 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). |
| @@ -103,11 +105,15 @@ are alive, and on #212 option B for box references. |
| | 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.) The controller added `ec2:DetachVolume` to the deny in (2), as within the ruling's intent. | |
| | H16 | **(2026-10-06) Auto Scaling boxes are enrolled automatically, with evidence (spec 4, L19).** The console enrolls an Auto Scaling box itself when its `boxid` evidence verifies (the deployment's account, the region's AWS region) and a regional worker confirms, with read-only Auto Scaling rights, that the instance is a current member of that region's group. Anything else still needs an operator's approval. | |
| +| 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.) | |
| -H10 to H16 supersede only what they name: H10 adds the volume condition |
| +H10 to H18 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. |
| +reservation for relocation starts, H16 and H17 settle enrollment for |
| +spec 4, and H18 narrows claim D7's console census for box-started |
| +relocations. |
| Everything else in H1 to H9 stands. |
| Standing rulings this spec keeps: |
| @@ -311,9 +317,38 @@ 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 region with no |
| -active worker left has no confirmer; how its first box is enrolled is |
| -§11 question 1 (B1-8). |
| +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 |
| +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: |
| + |
| +- it reads the target region's group name and ARN from the roster's |
| + `regions` entry for that placement (claim P5-D2's extension), never |
| + from the new box or an edges file; |
| +- it calls `DescribeAutoScalingInstances` for the instance id in the |
| + 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; |
| +- it writes the same create-only object, |
| + `control/box-enrollment/<box reference>/<instance id>.json`, with |
| + `{target_placement, aws_region, group_arn, instance_id, |
| + lifecycle_state, observed_at, request_ids, confirmer: {box, |
| + enrollment, region}}`. Two confirmers race by the same conditional |
| + 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 |
| +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). |
| A box whose entry is not `active` with a proven `cloud` is never |
| eligible, and a claim naming one is never relocated automatically: an |
| @@ -966,7 +1001,11 @@ records say. |
| --declare-lost`, with claim §7.3 D2's binding, attestation and |
| challenge as written (H10). |
| - The worker reads the state itself. It never trusts a box's own report, |
| - an edges file, or anything a box publishes about itself. |
| + 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. |
| **The fence record.** The worker writes one record per terminated |
| enrollment, create-only (L4): |
| @@ -1055,8 +1094,17 @@ alerting, and owns the loop that reads the queue and history. |
| publishes with its own `boot_id`. A console whose `compute` box has a |
| valid fence record is excluded from the census exactly as the box is |
| (L5). A console with no `compute` binding is never excluded this way. |
| - A console whose box is alive but whose report is stale still blocks a |
| - relocation start; whether it should is §11 question 2. |
| +- **A stale console report (H18).** For a relocation a box starts, and |
| + nothing else, the census accepts a console's **newest** report however |
| + old, when that report met every D7 floor check (protocol minimum, |
| + authenticated release minimum, matching floor digest) and the |
| + console's `compute` box has reported `floor_guard_ready` with the same |
| + floor digest. Claim D1 makes an armed guard permanent (it never |
| + expires and cannot be lowered offline), so that box cannot run an |
| + older console binary underneath. A console with no `compute` binding, |
| + or whose box never reported the guard armed, still needs a fresh |
| + report. Every other D7 rule, and every console-started operation, is |
| + unchanged (L20). |
| - **The loss is recorded twice.** The admission that takes over records |
| `writes_lost` (§5.8), and the console copies the fence into claim D4's |
| durable loss record when it next runs, with timer knowledge `partial`: |
| @@ -1178,13 +1226,24 @@ operations. |
| 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. The launch template and the `region-host` module create |
| + 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. |
| -- **Auto Scaling enrollment (H16, spec 4).** The box role gains |
| - `autoscaling:DescribeAutoScalingInstances`, conditioned on |
| - `aws:RequestedRegion`, read-only. |
| +- **Auto Scaling enrollment (H16, H17, spec 4).** The box role gains one |
| + separate statement: `autoscaling:DescribeAutoScalingInstances` and |
| + `ec2:DescribeInstances`, read-only, conditioned on |
| + `aws:RequestedRegion` being one of the deployment's AWS regions (any of |
| + them, not only the box's own). Nothing else is granted across regions: |
| + every other statement keeps its own-region condition, and no write, |
| + queue or S3 right crosses regions. The code calls another region only |
| + to confirm membership for a region with no `active` box (§5.1), and |
| + the fence, volume records and relocation refuse any observation not |
| + made in the box's own region. |
| - **Console role:** unchanged, no EC2 rights. |
| - **S3 (A2-6).** Two kinds of write, kept apart: |
| - **Create-only** (`If-None-Match: *`): content objects, |
| @@ -1224,7 +1283,8 @@ operations. |
| | What happens | Result | |
| |---|---| |
| | Executor box dies, region has another box | spec 3 relocates its hosts after the termination fence. Until then: requests 503 with Retry-After. | |
| -| Executor dies, region had one box | the Auto Scaling group launches a replacement, but no regional worker is left to confirm its group membership (H16), so it cannot be enrolled automatically; until §11 question 1 is ruled, an operator approves its enrollment (B1-8). Once enrolled it is a regional worker: it reads the termination event, writes the fence and relocates every host to itself. | |
| +| Executor dies, region had one box | the Auto Scaling group launches a replacement; an enrolled box in another region confirms its group membership (H17) and the console enrolls it. It is then the region's worker: it reads the termination event, writes the fence from its predecessor's last volume record, and relocates every host to itself. | |
| +| A console's box is alive but its report is stale | a box-started relocation proceeds on the console's newest report if that met the floor and the box's update guard is armed (H18); otherwise it waits and alerts. | |
| | The console's box is the one that died | failover does not need it: the fence, the census exclusion and every relocation CAS are a regional worker's (§5.9, L5, L6). | |
| | Box partitioned from the control bucket | it keeps serving what it serves (no execution lease while `serving`, claim §7.1). It can't take new work. The group's health check decides whether it is terminated. | |
| | 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`. | |
| @@ -1292,13 +1352,16 @@ operations. |
| 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 |
| 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 |
| + cross-region statement allows only the two describe calls. |
| 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 H16, |
| +never received. "Ruled" means Paul's rulings of 2026-10-06 (H10 to H18, |
| and amadan #236) decide the direction; the owning session still writes |
| the text. |
| @@ -1308,7 +1371,7 @@ the text. |
| | 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) | |
| | 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). Whether a live console with a stale report may be passed over is §11 question 2. | Ruled (H10, H14; #236: failover works when the console's box died); the stale-console part open | |
| +| 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) | |
| | 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) | |
| @@ -1322,7 +1385,8 @@ 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. The confirmer for a region with no active worker left is §11 question 1 (B1-8). | Ruled (H16); the empty-region confirmer open | |
| +| 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) | |
| +| 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 |
| is L2 to L5. K7 is L14. K8 is L16 and L17. K9 is L18. K10 is L15. K11 is |
| @@ -1359,7 +1423,14 @@ rev 4.2's table; this mapping says where each now lives. |
| 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); continuous files with a |
| + `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 |
| + 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 |
| 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`. |
| @@ -1399,45 +1470,18 @@ rev 4.2's table; this mapping says where each now lives. |
| ## 11. Open questions |
| +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). |
| -Astra's rev 5 review raised two that only Paul can settle: |
| - |
| -1. **Enrolling the first box of a region whose last box died (B1-8).** |
| - H16 has a regional worker confirm a new box's group membership. In a |
| - one-box region, H5's default, the box that died was the only worker, |
| - so its replacement cannot be confirmed, cannot be enrolled |
| - automatically, and cannot fence its predecessor or recover its hosts. |
| - Rev 5.1 says so (§7) instead of claiming automatic recovery. Options: |
| - - **(a)** A confirmer from another region: any active enrolled box, |
| - given read-only `autoscaling:DescribeAutoScalingInstances` (and |
| - `ec2:DescribeInstances`) for every region of the deployment, |
| - confirms membership for a region with no active worker. Only the |
| - confirmation crosses regions; the fence and relocation stay with |
| - the new box once it is enrolled. *Recommended.* It keeps H16's |
| - evidence and the console's lack of AWS rights. |
| - - **(b)** Operator approval for a region's first box. One-box regions |
| - then have no automatic recovery, which H5's default of 1 makes the |
| - common case. |
| - - **(c)** Keep at least two boxes in every region that wants automatic |
| - recovery (H5's minimum raised to 2 for those regions). |
| -2. **A live console with a stale report (B1-7).** Rev 5.1 removes a |
| - console from the census when its box is fenced. A console whose box |
| - is alive but whose report has gone stale (hung, partitioned) still |
| - fails claim D7's census, so a box-started relocation, a failover |
| - included, waits for it. Options: |
| - - **(a)** Keep D7 as written: the relocation waits and alerts. Safe |
| - against a console that is about to write the claim with an old |
| - protocol, but a hung console can hold up failover indefinitely. |
| - - **(b)** For box-started relocations only, accept a console's newest |
| - report, however old, when it met the floor and its `compute` box's |
| - root guard is armed (claim D1): that guard already stops any binary |
| - below the floor from running, even offline. *Recommended.* |
| - - **(c)** As (b), but only for a stated time (for example an hour), |
| - then (a). |
| +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). |
| ## 12. Out of scope, for the later specs |
| @@ -1638,6 +1682,6 @@ before acceptance. |
| | B1-4 P1 the guard rests on an unprotected tag; the non-Organizations fallback still fences | accepted: the SCP also denies changing `carlos:role` except at launch; exemption narrowed to one hold-gated role; a root-signed guard attestation is required, and without one there is no automatic fence. Stricter than H15, never weaker (§5.9, §6, §8) | |
| | B1-5 P1 a `lost` controller stops excluding updates | accepted: claim D6 does define `lost` and keeps its deny on failed cleanup. Root now refuses on any controller record in any state or any unreadable one, until D6's clearing with cleanup complete (§5.10, L6) | |
| | B1-6 P2 the source lost in `starting` has no transition | accepted: a source-loss CAS converts the op to failover from `starting` or `releasing`, keeping the intent and acknowledgements, removing `from` from the barrier (§5.8, L1) | |
| -| 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 is §11 question 2 (§5.9, L5) | |
| -| 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. §7 no longer claims automatic recovery for one-box regions; the confirmer is §11 question 1 (§5.1, §7, L19) | |
| +| 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 | |
diff --git a/docs/superpowers/specs/CODEX-REVIEW-BRIEF-REGION-HA-REV5-2.md b/docs/superpowers/specs/CODEX-REVIEW-BRIEF-REGION-HA-REV5-2.md| index 82a48b5fd..307b58a4e 100644 |
| --- a/docs/superpowers/specs/CODEX-REVIEW-BRIEF-REGION-HA-REV5-2.md |
| +++ b/docs/superpowers/specs/CODEX-REVIEW-BRIEF-REGION-HA-REV5-2.md |
| @@ -36,13 +36,18 @@ disposition table. The mechanisms changed: |
| region; the empty-region confirmer is an open question for Paul. |
| - **Citations (B1-9)** refreshed. |
| -§11 now holds two questions for Paul (the empty-region confirmer, a |
| -live console with a stale report). Do not answer them; report only if |
| -the spec relies on an answer it does not have. |
| +Paul ruled both questions those fixes raised, on 2026-10-06, and they |
| +are now fixed text: **H17** (an enrolled box in another region, with |
| +read-only cross-region Auto Scaling and EC2 describe rights and no other |
| +cross-region use, confirms the first box of a region with no enrolled |
| +box; §5.1, §6, L19) and **H18** (for box-started relocations only, the |
| +census accepts a console's newest report however old if it met the floor |
| +and the console's box has the D1 update guard armed; §5.9, L20). §11 is |
| +empty. Review how H17 and H18 are specified, not whether they should be. |
| ## Fixed: do not re-argue |
| -Rulings H1 to H16 in §0, and the claim's own ruled text (R6 in |
| +Rulings H1 to H18 in §0, and the claim's own ruled text (R6 in |
| particular: no warm reuse of a local database). Report only mechanisms |
| that fail to honour them, are unsafe, or are missing. |
| @@ -66,6 +71,8 @@ that fail to honour them, are unsafe, or are missing. |
| replacements and crashes; the source-loss CAS against claim D5 and |
| D6; holds, releases and removed volumes against the 2-hour bound and |
| the fence; the SCP's tag statements against Auto Scaling launches; |
| + the cross-region confirmation (H17) and its IAM; the stale-console |
| + census rule (H18) against D1 and D7; |
| root's refusal against D6's clearing; the console `compute` binding |
| against D7. Do not re-report a round 1 finding unless its fix is |
| incomplete. |