amadan
spec: region HA spec 1 rev 5.1, Astra rev 5 round 1 (B1-1 to B1-9)
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+309
−106
docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md+309 −106
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 46fac1483..ec21ab17d 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,24 @@ |
| # Region HA, spec 1: placing an instance on a box |
| -Design, 2026-10-06, **rev 5**. DRAFT. Plan 1a is built and merged |
| +Design, 2026-10-06, **rev 5.1**. DRAFT. Plan 1a is built and merged |
| (aadb860); nothing else here is built. |
| +**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 |
| +from its real predecessor, and `released` coverage is bound to one |
| +session (B1-1). A replacement target must make its own local install |
| +before probing (B1-2). An operator's volume change first suspends |
| +automatic disk evidence, and a volume that leaves a running box keeps it |
| +suspended until accounted for (B1-3). The volume guard protects its own |
| +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). |
| + |
| **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`, |
| @@ -116,10 +132,10 @@ Standing rulings this spec keeps: |
| ## 1. Why |
| Today a region is one box. Placement is per region: a bucket record has |
| -`Region` and `Pool` and no box (`internal/provision/provision.go:39`). |
| +`Region` and `Pool` and no box (`internal/provision/provision.go:49`). |
| Every box whose `CARLOS_REGION` matches mints the route |
| -(`internal/provision/reconcile.go:335`, called at `:799`). Nothing |
| -enforces "exactly one box": `reconcile.go:179` states it as intent only. |
| +(`inScope`, `internal/provision/reconcile.go:348`, called at `:820`). Nothing |
| +enforces "exactly one box": `reconcile.go:192` states it as intent only. |
| A second box in a region would break three things: |
| @@ -132,12 +148,13 @@ A second box in a region would break three things: |
| winning. Plan 1a settles it by installation stamp (§5.4). |
| 3. **A box can serve a stale local copy.** The activator trusts a local |
| database as the warm cache because "on one box … the local copy can |
| - only be what we ourselves checkpointed" (`internal/activator/activator.go:1127`). |
| + only be what we ourselves checkpointed" (`internal/activator/activator.go:1164-1168`). |
| With two boxes taking turns, that is false. Claim R6 removes the |
| warm cache altogether (H13). |
| And when a box dies, its instances stay down. EC2 auto-recover brings |
| -back the same machine, if it can (`infra/modules/region-host/main.tf:497`). |
| +back the same machine, if it can (`host_auto_recover`, |
| +`infra/modules/region-host/main.tf:521`). |
| ## 2. Words |
| @@ -230,10 +247,10 @@ region (A1-1, H11), and every EBS volume it had attached was |
| - A region with one box behaves exactly as today, and every new rule |
| holds trivially there. |
| - Static sites and public addr routes still run on every box |
| - (`everywhereClass`, `reconcile.go:202`). Only relocatable hosts gain an |
| + (`everywhereClass`, `reconcile.go:215`). Only relocatable hosts gain an |
| executor that can change; unit- and socket-backed routes keep theirs. |
| - Customer fleets keep their binding stamps (`internal/host/fleetbind.go`) |
| - and per-request fallback (`internal/edge/edge.go:2432`). |
| + and per-request fallback (`fleetChannelFor`, `internal/edge/edge.go:2466`). |
| - The ingress model: any edge serves any app and backhauls home-run |
| hosts to their box (multi-region ingress). This spec changes which box |
| is "home", not how backhaul works. |
| @@ -294,7 +311,9 @@ 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). |
| +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). |
| A box whose entry is not `active` with a proven `cloud` is never |
| eligible, and a claim naming one is never relocated automatically: an |
| @@ -423,7 +442,7 @@ deleted. Claim R6 replaces them: every admitted writer purges any local |
| database with the error-returning purge and restores from the certified |
| remote (claim §6.4a, "The baseline is always the certified remote"). |
| Under P6-D4 every admission is cold. The activator's one-box comment at |
| -`activator.go:1127` is replaced by a reference to claim R6, not to HA3. |
| +`activator.go:1164-1168` is replaced by a reference to claim R6, not to HA3. |
| Plan 1a's `activator.WarmCopyTrusted` is not used, and nothing reads the |
| install marker to skip a restore (§19). A1-5's concern, that authority is |
| @@ -551,7 +570,7 @@ an always-continuous entry in the manifest whenever any of it changes: |
| - its timer rows (active rows and their bookkeeping, moves §9.4's |
| canonical digest), on a registration, a delivery or a rearm; |
| - the route's `NextDue`, the app's own next wake |
| - (`activator.go:2019-2030`), whenever the activator sets it; |
| + (`activator.go:2204`), whenever the activator sets it; |
| - the route's `Replication` mode. |
| The new executor sets `NextDue` and `Replication` from it, as a move's |
| @@ -603,12 +622,12 @@ replication. |
| | Phase | Who acts | `op.exec` | `holder.stamp` | Rows (§5.3) | Admits | |
| |---|---|---|---|---|---| |
| -| `starting` | a worker writes the intent; `from` (if alive) and `to` write execution leases and `exec_ack` (D6). The barrier needs only `to` when the intent cites a fence | `from` | `stamp_from` | `from` ready; `to` held | `from`, as for `serving` | |
| +| `starting` | a worker writes the intent; `from` (if alive) and `to` write execution leases and `exec_ack` (D6). The barrier needs only `to` when the intent cites a fence, or once a source-loss CAS (below) has removed `from` | `from`, or `none` after a source-loss CAS | `stamp_from` | `from` ready; `to` held | `from`, as for `serving` | |
| | `releasing` | `from` runs the **release sequence** (below) and publishes its stop receipt; for failover the fence is already in the intent and this phase is skipped | `from` until evidence | unchanged | `from` ready until its admission fence closes, then held; `to` held | `from`, until its admission fence closes | |
| | `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, and **builds `P`** (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) | `to` | `S'` | as `installing` | nobody | |
| -| `probing` | `to` enters it by CAS, 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 | |
| +| `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 | |
| | `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` | |
| @@ -689,43 +708,72 @@ in place of a staged replica: |
| from the snapshot then skips every later write (moves R5-1); |
| - write `P`'s files manifest, create-only, as the pinned manifest's |
| entries (objects named where they are, §5.6), with the files, env and |
| - wake state; |
| -- apply the files and env to the local directory, `ReplaceTimers` the |
| - wake state, set `NextDue` and `Replication`, `RenderHeld` and |
| - `MaterializeHeld` with current inputs, recorded as the relocation's |
| - inputs (P6-D3); |
| -- journal the local install, last. |
| - |
| -`installed` is written only after a fresh read verifies all three |
| -objects. `generation.json` is not written here: the probe's admission |
| -publishes it (moves §7.14). |
| + wake state. |
| + |
| +That is the **remote build**: immutable, built once, and complete when |
| +a fresh read verifies all three objects. `installed` records it. |
| +`generation.json` is not written here: the probe's admission publishes |
| +it (moves §7.14). |
| + |
| +**The local install (B1-2)** is separate, because it belongs to one box. |
| +The box that is `op.exec`, under the host guard with the stamp it |
| +activated: |
| + |
| +- applies the files and env from `P`'s files manifest to the local |
| + directory, `ReplaceTimers` the wake state, and sets `NextDue` and |
| + `Replication`; |
| +- runs `RenderHeld` and `MaterializeHeld` with current inputs, recorded |
| + 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. |
| **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` |
| and phase `probing`: |
| - **mode** cold, always (P6-D4, H13); |
| -- **generation:** the first attempt opens `P`, which no admission has |
| - named (P6-D3's opened-once evidence). A restarted attempt is cold into |
| - a fresh generation restored from `P`, never `P` again (claim §6.4a item |
| - 3); |
| +- **generation and baseline (B1-1):** the first attempt opens `P`, |
| + which no admission has named (P6-D3's opened-once evidence), and |
| + restores it from its pinned snapshot and anchor |
| + (`genselect.SelectPrepared`). Every later attempt is cold into a fresh |
| + generation whose baseline is chosen as for any cold admission: |
| + `genselect.Select` from the predecessor, `holder.generation` as |
| + observed, through the unfinished run (claim §6.4a item 3; moves §7.14's |
| + restore row). So attempt three restores attempt two's generation with |
| + everything it replicated, not `P`. Prepared authority is used once; |
| - **`KeepStamp`** on the first attempt, because no writer has been |
| admitted since the `installing` CAS issued `S'` (`holder.stamp > |
| holder.session`). Later attempts take a new stamp; |
| -- **coverage:** for a drain, a rebalance or a probe failure the pin |
| - reaches the released box's stopped-database position, so nothing was |
| - lost. Rev 5 requests a coverage value for that, `released` (L9). Until |
| - L9 is accepted, relocation by drain is not enabled (§8), because |
| - coverage `""` would declare a false loss on every drain. For a |
| - failover, coverage is `""`: the admission records `writes_lost` for |
| - `from`'s last session with `remote_max_txid` = the pin's `N`, and `to` |
| - raises the alert. That is H3's written-down loss, declared, never |
| - silent; |
| -- then, as for every cold admission: purge, restore `P` from its pinned |
| - snapshot and anchor (`genselect.SelectPrepared`), start, readiness, |
| - `generation.json`, then `PublishGeneration`, which queues the |
| - `park-generation` chore that retires `generation_from` in this region |
| - (claim §6.4a item 5); |
| +- **coverage, per admission (B1-1):** decided for the session the |
| + admission's predecessor actually is, the last entry of |
| + `holder.admissions`, never for the operation as a whole: |
| + - `released` (L9) only on the admission that opens `P`, and only when |
| + that predecessor is exactly the `{box, session}` whose release |
| + receipt this op journaled and whose `final_txid` the pin reached. |
| + That is a drain, a rebalance, or the nested relocation after a |
| + `probe-failed`. Until L9 is accepted, relocation by drain is not |
| + enabled (§8), because coverage `""` would declare a false loss on |
| + every drain; |
| + - `""` everywhere else: a failover (the admission records |
| + `writes_lost` for `from`'s last session, `remote_max_txid` the pin's |
| + `N`, H3's written-down loss), and every later probe attempt, whose |
| + predecessor is the previous attempt's uncertified session. `to` |
| + raises one alert per declaration; |
| +- then, as for every cold admission: purge, restore the chosen baseline, |
| + start, readiness, `generation.json`, then `PublishGeneration`, which |
| + queues `park-generation` for the dead generations of this region in |
| + the chain (`generation_from` at the first publication; an earlier |
| + attempt's generation at a later one) (claim §6.4a item 5). A queued |
| + park never touches a generation a later attempt still needs: the |
| + baseline is always the newest generation, protected as the unfinished |
| + run until its successor publishes (claim §6.2a); |
| - **limits:** at most three attempts within the probe deadline, as a |
| landing's (claim §6.4a item 7). A probe never marks the host failed; |
| running out of attempts is `probe-failed`. |
| @@ -746,9 +794,10 @@ 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 (probe, then `serving`), never back to `installing`; |
| + forward (local install if the executor has no receipt, probe, then |
| + `serving`), never back to `installing`; |
| - `P` is opened at most once. After its first admission, every restart |
| - takes a fresh generation from it; |
| + takes a fresh generation from its predecessor; |
| - a worker or `to` that paused and resumes revalidates the phase under |
| the host guard, with the stamp it captured, and stops. |
| @@ -774,12 +823,22 @@ that phase. |
| | terminated in `starting` or `releasing` | `to`'s termination fence | the **same** phase. The source's release requirements are unchanged: a drain still needs `from`'s stop evidence | |
| | terminated in `pinning` | `to`'s termination fence | `pinning` | |
| | terminated in `installing` | `to`'s termination fence | `installing`, with `op.exec: to'`, a new stamp and a fresh prepared id `P'`, from the journaled pin. The old `P` was never opened; the at-rest sweep parks it | |
| -| terminated at `installed`, or in `probing` before its first `AdmitWriter` succeeded | `to`'s termination fence | `installed`, with `op.exec: to'` and a new stamp. `P` was never opened, so `to'` opens it | |
| +| terminated at `installed`, or in `probing` before its first `AdmitWriter` succeeded (no admission entry names `P`) | `to`'s termination fence | `installed`, with `op.exec: to'`, a new stamp, and no local install receipt. `to'` activates the stamp, makes its own local install from `P`'s files manifest and records its receipt (B1-2), then enters `probing`. `P` was never opened, so `to'` opens it | |
| | terminated after its first `AdmitWriter` | `to`'s termination fence | a nested failover from `pinning`, pinning from `holder.generation` as observed (`P` or a later fresh generation, with `to`'s replicated writes). Coverage `""` declares `to`'s sessions | |
| | alive, but its probe fails or misses the **probe deadline** (10 minutes) | `to`'s release sequence, in `probe-failed` | a nested relocation from `pinning`, pinned to at least `to`'s journaled `final_txid` and `manifest_seq`, so writes made during the probe are kept. `to` is excluded from the choice for this host | |
| -- `from` terminated during a drain's `releasing` turns it into a |
| - failover, with the termination fence as evidence. |
| +**Losing the source (B1-6).** A drain or rebalance whose `from` is |
| +terminated before its stop receipt becomes a failover, in one CAS |
| +conditional on `op.id` and the phase, citing `from`'s fence: |
| + |
| +| `from` terminated | The CAS | The op resumes at | |
| +|---|---|---| |
| +| in `starting`, acknowledged or not | journals `failover_fence` (key, SHA-256) and `reason: failover`, keeping the intent and every acknowledgement; removes `from` from `participants` and from the barrier; sets `op.exec: none`, keeping the stamp (claim D5's non-installing form); adds `from` to `lost` and discharges its `park-local` chores (§5.9) | `starting`, waiting only for `to`'s acknowledgement; the next CAS goes to `pinning` with the fence as its evidence, skipping `releasing` | |
| +| in `releasing`, before its receipt | the same | `pinning`, with the fence as evidence | |
| +| after its receipt (`pinning` on) | `from` only goes on `lost` and its chores are discharged; nothing else changes | the same phase | |
| + |
| +The pin for a converted op follows the failover rule (fence plus 30 |
| +seconds), and the first admission's coverage is `""`. |
| - **The bound.** After two replacements of `to` in one op, the placer |
| stops at the current phase's safe point (never between `installed` |
| and a probe) and marks the op `stuck`. It alerts, and the op waits for |
| @@ -810,12 +869,16 @@ 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. |
| + `cloud`, shows the guard's tag on it, and lists at least one EBS |
| + volume. It, and every record written after it, shows every attached |
| + EBS volume `DeleteOnTermination: true`. And **disk evidence is not |
| + suspended** for the enrollment (below, B1-3). |
| +2. **The IAM guard is in place and attested** (§6, B1-4): an Organizations |
| + policy, recorded in a valid guard attestation, denies every principal |
| + but the one volume-change role any change to a platform box's block |
| + device mapping, any attach or detach, and any change to the guard's |
| + tag, so the record cannot go stale behind the platform's back. With |
| + no valid attestation, nothing is fenced automatically. |
| 3. **A terminated read.** A regional worker, with its own read-only |
| rights in the box's AWS region, observes state exactly `terminated` |
| for the instance id, account (`OwnerId`) and region in the roster |
| @@ -859,6 +922,38 @@ 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). |
| + |
| +**Suspending disk evidence (B1-3).** A record's age bound cannot cover an |
| +operator's change made just before a termination, and a detached volume |
| +is not in any later record at all. So disk evidence is suspended |
| +**before** any exempt change, and resumes only after the change is |
| +accounted for: |
| + |
| +- **Before.** The only principal the guard exempts is the volume-change |
| + role (§6). `carlos ops box volumes change <box>` first writes a |
| + create-only hold, `control/box-volumes/<enrollment>/hold-<id>.json` |
| + (`{id, operator, reason, 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. |
| +- **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 |
| + 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. |
| + |
| +A hold or removal therefore never leaves a window: from the hold's write |
| +until a release, the box cannot be fenced automatically, whatever its |
| +records say. |
| **What never counts.** |
| @@ -952,6 +1047,16 @@ alerting, and owns the loop that reads the queue and history. |
| to `retired`, citing the record, when it next runs. Until then the |
| record alone excludes the box from the census for lifecycle starts |
| (L5), so failover never waits for a console. |
| +- **A console that ran on the box leaves the census too (B1-7).** Claim |
| + D7 requires a fresh report from every console able to mutate the |
| + namespace. A console enrollment gains `compute: {box, enrollment}`, |
| + the platform box its process runs on, set at console enrollment and |
| + checked against every console report, which that box's trusted writer |
| + 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. |
| - **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`: |
| @@ -993,10 +1098,12 @@ 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; |
| +2. then scans `<DataDir>/.hostexec/` completely. **Any** controller |
| + record there, in any state (`pending`, `active` or `lost`), and any |
| + record root cannot read or parse, or a directory it cannot list, means |
| + the box may still be a participant: root removes its marker, refuses |
| + the update, and leaves the console's activation reservation held, to |
| + retry later (B1-5); |
| 3. otherwise it proceeds. The marker stays until the update finishes or |
| is recovered. |
| @@ -1004,6 +1111,15 @@ 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. |
| +**When exclusion ends (B1-5).** A controller record is removed only by |
| +claim D6's clearing: a fresh claim read showing `serving`, `free`, or |
| +that the box no longer participates, **and** any cleanup the record |
| +requires complete. A `lost` record whose cleanup-only termination failed |
| +is never cleared: claim D6 keeps that deny, and root's refusal stays |
| +with it. A box whose processes may still run under an operation never |
| +takes an executable update. An operator who needs to update such a box |
| +first resolves the host (`carlos ops host resolve`). |
| + |
| **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 |
| @@ -1011,8 +1127,10 @@ 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. |
| +participant from its `pending` state until D6 clears its record, through |
| +`active` and `lost` alike, so an update never runs under a relocation's |
| +`installing`, `probing` or release, nor while a lost controller's |
| +cleanup is unfinished. |
| 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 |
| @@ -1031,22 +1149,39 @@ operations. |
| own grants: `s3:ListBucketVersions`, `s3:GetObjectVersion` and |
| `s3:DeleteObjectVersion` on its region's data bucket (claim §6.2a), |
| which `genselect` and the parker use. |
| -- **The volume guard (H15).** An Organizations service control policy on |
| - the deployment's account denies `ec2:ModifyInstanceAttribute`, |
| - `ec2:AttachVolume` and `ec2:DetachVolume` on instances tagged as |
| - platform boxes (`aws:ResourceTag/carlos:role = platform-box`) to every |
| - principal whose ARN is not one of the deployment's operator roles. |
| - `DetachVolume` is there because a volume detached from a running box |
| - survives termination with the box's data, which is exactly what the |
| - fence must rule out. Where the account |
| - has no Organizations, tofu puts the same Deny in every role and user it |
| - manages; that is weaker, since it cannot bind principals tofu does not |
| - know, and `carlos system` says so. The launch template and the |
| - `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. |
| +- **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 |
| + `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. |
| + |
| + 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. |
| + |
| + **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 |
| + 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 |
| + 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. |
| @@ -1054,8 +1189,8 @@ operations. |
| - **S3 (A2-6).** Two kinds of write, kept apart: |
| - **Create-only** (`If-None-Match: *`): content objects, |
| `instances/<host>/*/files/*/objects/`, in the region's data bucket; |
| - box identity records, `control/boxes/`, volume records, |
| - `control/box-volumes/`, membership confirmations, |
| + box identity records, `control/boxes/`, volume records, holds and |
| + releases, `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 |
| @@ -1089,12 +1224,16 @@ 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; once enrolled, it is a regional worker, reads the termination event from the queue, describes the instance, writes the fence and relocates every host to itself. | |
| +| 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. | |
| | The console's box is the one that died | failover does not need it: the fence, the census exclusion and every relocation CAS are a regional worker's (§5.9, L5, L6). | |
| | Box partitioned from the control bucket | it keeps serving what it serves (no execution lease while `serving`, claim §7.1). It can't take new work. The group's health check decides whether it is terminated. | |
| | Box alive but failing its health check | the group terminates it, then as above. Instances that were healthy lose up to H3's window, declared by `writes_lost`. | |
| | A terminated box had a volume without `DeleteOnTermination` | no automatic fence: `awaiting-evidence`, an alert, and the operator's `--declare-lost` (§5.9). The running box's record already alerted. | |
| | A terminated box's newest volume record is missing or over 2 hours old | no automatic fence: the operator path (§5.9, H15). | |
| +| An operator changes a box's volumes, or a volume vanishes from a running box's mapping | disk evidence is suspended from the hold (or the record showing the removal) until a release; a termination meanwhile goes to the operator (§5.9, B1-3). | |
| +| The account has no attested volume guard | no automatic fence anywhere in it (§6, B1-4). | |
| +| A participant's execution lease is lost and its cleanup fails | its controller record stays; root refuses executable updates on that box until the host is resolved (§5.10, B1-5). | |
| +| The source dies while a drain is in `starting` | the op becomes a failover in place (§5.8, B1-6). | |
| | An update is reserved for `to` while a relocation starts | root refuses to begin it while `to` is a participant, or `to` refuses to acknowledge while it runs; never both running (§5.10). | |
| | 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). | |
| @@ -1124,7 +1263,9 @@ operations. |
| `cloud`; |
| - 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. |
| + `DeleteOnTermination` and the guard's tag, no box has an unreleased |
| + hold or removal, and the account has a valid guard attestation |
| + (§6). |
| The HA floor joins the protocol floor (claim §10, D1): every path that |
| restores an executable (system apply, rollback, boot recovery from |
| @@ -1147,8 +1288,10 @@ operations. |
| (`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. |
| + 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 |
| + volume-change role cannot be assumed without a hold tag. |
| 6. Then specs 2, 3, 4. |
| ## 9. Changes requested of the claim and moves specs |
| @@ -1161,15 +1304,15 @@ the text. |
| | # | Amends | Change | Status | |
| |---|---|---|---| |
| -| L1 | claim §4, §8, §6.4a (which kinds and phases admit), §7.3 D6 | New op kind `relocating` (§5.8): same region, stateful, from `serving`; its phase table with `op.exec`, stamp, rows and admission per phase; the `installed` no-reinstall boundary; the replacement table; two replacements then `stuck`; the release sequence. Recovery owner `region:<r>`, any regional worker (P6-D5). The D6 barrier needs only `to` when the start cites a termination fence. Excludes moves, placements and pushes. | Ruled in direction (H10; #236: "a new op kind, or an equivalent that the claim prefers") | |
| -| L2 | claim §4, C5, §7.3 D2 | A termination fence (§5.9) is a lost-box fence, written by a regional worker with no person in the loop: `terminated` only (by event, describe or, later, the group's history), bound to the roster entry's `cloud`, with a running-time volume record no more than 2 hours old showing every EBS volume `DeleteOnTermination`, under the IAM volume guard (no `ModifyInstanceAttribute`, `AttachVolume` or `DetachVolume` on platform boxes except by operator roles). A `shutting-down` read is never evidence. Stopped, unclear and vanished boxes keep D2's operator path unchanged. | Ruled (H10, H15) | |
| +| 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) | |
| | 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`) | 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) | |
| +| 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 | |
| +| 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) | |
| -| 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 | |
| +| L9 | claim §6.4a item 2, `hostclaim.AdmitWriter` | A coverage value `released`, legal only on the admission that opens a prepared generation built from a pin reaching the `final_txid` a released box recorded from its stopped database, and only when the admission's predecessor (the last `holder.admissions` entry) is exactly that box and session, under its stop receipt. It declares nothing. Without it every drain declares a false loss (B1-1). | Requested | |
| | 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 | |
| @@ -1179,7 +1322,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) | |
| +| 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 | |
| **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 |
| @@ -1212,9 +1355,11 @@ rev 4.2's table; this mapping says where each now lives. |
| 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 |
| + refreshes the record with a `false` volume, a record without the |
| + guard's tag, no guard attestation, an unreleased hold, a removed |
| + volume with and without a release, a release with no later running |
| + record); the volume recorder (writes on change, at least hourly, |
| + `removed_volumes` when a volume leaves the mapping); 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`. |
| @@ -1227,14 +1372,21 @@ rev 4.2's table; this mapping says where each now lives. |
| 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; the |
| - start refused when the roster reserves an update for `from` or `to`. |
| + start refused when the roster reserves an update for `from` or `to`; |
| + 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 |
| + another box's receipt (B1-2); `from` terminated in `starting` before |
| + and after acknowledging (B1-6). |
| - **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`, `DetachVolume` and a |
| - block device mapping change by the box role and a non-operator role, and allows an |
| + by retry; a lease lost during `probing` with cleanup failing, and an |
| + unreadable controller record, both refusing the update (B1-5). |
| +- **IAM:** the volume guard refuses `AttachVolume`, `DetachVolume`, a |
| + `carlos:role` tag change and a block device mapping change by the box role and a non-operator role, and allows an |
| operator role (rehearsed on dev, §8 step 5). |
| - **Integration:** two agents against one fake region, one control |
| bucket: create lands on the chosen box only; the other box mints no |
| @@ -1247,17 +1399,45 @@ 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). 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. |
| +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). |
| ## 12. Out of scope, for the later specs |
| @@ -1438,3 +1618,26 @@ follows §5.3's revised table. Item 4 is dropped. Item 6 becomes |
| publishing the enrollment evidence at start. Item 7 is §5.8 as rev 5 |
| states it, and waits for L1 and L9 to L11. Item 8 adds the roster and |
| volume checks to the gate. |
| + |
| +Rev 5.1 adds to plan 1b: the hold, release and removed-volume rules and |
| +their CLI (§5.9), the guard attestation and the tag statements (§6), the |
| +local install receipt (§5.8), and root's refusal on any controller |
| +record (§5.10). |
| + |
| +## 20. Astra rev 5 round 1 dispositions |
| + |
| +Reviewed rev 5 at 2a9165d4 (`CODEX-FINDINGS-REGION-HA-REV5-1.md`). Each |
| +citation was checked against claim 98b45332, moves a4711728 and main |
| +before acceptance. |
| + |
| +| Finding | Disposition | |
| +|---|---| |
| +| B1-1 P1 probe retries restore `P` again and lose replicated writes; `released` suppresses loss too widely | accepted: claim §6.4a item 3 and moves §7.14's restore row choose a fresh admission's baseline from its predecessor. Only the first attempt opens `P`; later attempts restore through `genselect.Select`; coverage is decided per admission, `released` only on `P`'s opening with a predecessor matching the journaled release (§5.8, L9) | |
| +| B1-2 P1 a replacement at `installed` never makes its local install | accepted: the remote build and the per-box local install are separate; `probing` requires a local install receipt bound to `op.exec`, its enrollment and `holder.stamp`; a replacement makes its own from `P`'s files manifest, and `P` is still built once and opened once (§5.8, L1) | |
| +| B1-3 P1 an operator's volume change before a refresh, or a detach, allows a false destroyed-disk fence | accepted: a hold written before the change suspends disk evidence; a volume leaving a running box's mapping suspends it too; release needs a newer all-true record and an operator's attestation for every removed volume (§5.9, §6, §7) | |
| +| 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-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 | |