amadan
spec: region HA spec 1 rev 5, restated against claim rev 6.25 and Paul's rulings H10-H13
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+772
−411
docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md+772 −411
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 18587034b..17ece865c 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,14 +1,38 @@ |
| # Region HA, spec 1: placing an instance on a box |
| -Design, 2026-10-04, **rev 4.2**. DRAFT. Nothing here is built. |
| - |
| -Rev 4.2 answers Astra round 5 (`CODEX-FINDINGS-REGION-HA-5.md`, A5-1). |
| -Rev 4.1 answers Astra round 4 (`CODEX-FINDINGS-REGION-HA-4.md`, |
| +Design, 2026-10-06, **rev 5**. DRAFT. Plan 1a is built and merged |
| +(aadb860); nothing else here is built. |
| + |
| +**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 H13 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 |
| +admitted by `AdmitWriter`, every admission is cold until certificates |
| +work, a prepared generation is opened once, and regional work is done |
| +by any enrolled box in the region. So rev 5 drops spec 1's own box |
| +records as authority (H11), the trusted local copy (H13), and its own |
| +`holder.generation` install CAS. Relocation (§5.8) keeps every property |
| +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. |
| + |
| +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 |
| +plan. Rev 4.1 answers Astra round 4 (`CODEX-FINDINGS-REGION-HA-4.md`, |
| **A4-n**). Rev 4 answers Astra round 3 (`CODEX-FINDINGS-REGION-HA-3.md`, **A3-n**, |
| plus the A2-5, A2-7 and A1-1 residuals). Rev 3 answered Astra round 2 (`CODEX-FINDINGS-REGION-HA-2.md`, cited |
| **A2-n**, plus the round 1 findings it marked partly resolved). Rev 2 |
| answered round 1 (`CODEX-FINDINGS-REGION-HA-1.md`, **A1-n**). Every |
| -finding is accepted; §13 maps each to its section. |
| +finding is accepted; §13 maps each to its section. Where rev 5 changes a |
| +mechanism a disposition names, the disposition's property still holds, |
| +and the section it points to says how. |
| This is the first of four specs that give each region high availability |
| and autoscaling: |
| @@ -25,20 +49,20 @@ and autoscaling: |
| It builds on two specs still in review, and asks them for changes (§9): |
| -- the host lifecycle claim, rev 6.3 (`design-replica-ownership`, |
| - 8faa89a4), cited as **claim §n**; |
| -- move-any-app (`design-moves-any-region`), cited as **moves §n**. Rev |
| - 7.5 (cdc98845) is the last committed revision. **Rev 7.6**, which adds |
| - the level-0 anchor that relocation's install relies on (A2-1), is an |
| - uncommitted draft in the moves worktree as of 2026-10-04; its model |
| - half is committed at 29245f69. Citations of rev 7.6 are to that draft |
| - until it is committed, and the plan pins the commit (A4-3). |
| +- the host lifecycle claim, **rev 6.25** (`design-replica-ownership`, |
| + 413b12cb), cited as **claim §n**. Its sections marked PROPOSED (§5.9 |
| + P5-D1 to P5-D6, §6.6 P6-D1 to P6-D8, §7.3 D2 to D6, §10.1 D1 and D7) |
| + are cited as proposals, not as settled text. Rev 6.26 (98b45332) |
| + changes only the staging scope of a delete's park (R17-2) and touches |
| + nothing here; |
| +- move-any-app (`design-moves-any-region`), **rev 7.17** (39904c84), |
| + cited as **moves §n**. Rev 7.18 (a4711728) changes no rule. |
| It also builds on nearest-region (on main since 3f4a9bfd), whose box |
| -evidence in the edges file is how a console knows which boxes a region |
| -has. |
| +evidence in the edges file is how a console knows which enrolled boxes |
| +are alive, and on #212 option B for box references. |
| -## 0. Rulings (Paul, 2026-10-04) |
| +## 0. Rulings (Paul, 2026-10-04 and 2026-10-06) |
| | # | Ruling | |
| |---|---| |
| @@ -51,6 +75,14 @@ has. |
| | H7 | **Ticks are at-least-once.** A delivery that ran on a dead box but whose bookkeeping did not reach S3 may run again. Documented; apps that need exactly-once guard it themselves. | |
| | H8 | **`files_durability` defaults to `snapshot`** for apps with no setting. | |
| | H9 | **The reconcile sweep is 10 minutes** (§5.3). | |
| +| H10 | **(2026-10-06) Termination fences stay automatic, and the disk must die with the box.** H1 stands against claim §7.3's operator-only declare-lost. A box AWS reports `terminated` is fenced automatically by a region placer: a box with read-only EC2 rights. The console holds none. The fence additionally requires every EBS volume the instance had attached to be `DeleteOnTermination: true`, read from the same `DescribeInstances` reply's `BlockDeviceMappings`. Otherwise the operator path applies. Stopped, unclear or vanished boxes stay operator-only (claim §7.3 D2 as written). Absence is never evidence. | |
| +| 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. | |
| + |
| +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. |
| Standing rulings this spec keeps: |
| @@ -59,12 +91,17 @@ Standing rulings this spec keeps: |
| - Placement targets a region and pool, never a named box (fleets D5). |
| An operator or a customer still cannot pin an instance to a box; only |
| the placer chooses. |
| -- The console is the single control-plane writer and holds no EC2 rights |
| - (claim §7.2). |
| +- The console is the single control-plane writer for operator and |
| + customer requests, and holds no EC2 rights (claim §7.2). Boxes write |
| + claims too, as the claim allows them: writer admission, publication, |
| + their own chores and, under this spec, relocation. |
| - A box must hold the deployment's secrets key to receive instances (R9), |
| and every box reconcile would admit in a region must qualify |
| (nearest-region F2). |
| - Unreplicated state on a dead box is lost, and we say so. |
| +- **Claim R6:** a box never reuses its local database; every writer start |
| + restores from the certified remote (claim §6.4a). Under P6-D4, every |
| + admission is cold. |
| ## 1. Why |
| @@ -79,14 +116,15 @@ A second box in a region would break three things: |
| 1. **Both boxes run the instance's route.** The S3 lease (`lock.json`, |
| 15-minute TTL, `internal/lease/lease.go:37`) stops them running at |
| once, but whichever box a request reaches wins. |
| -2. **Both boxes claim the host to the edges.** The home map breaks the |
| +2. **Both boxes claim the host to the edges.** The home map broke the |
| tie by sorted box name, with no liveness (`foldHomes`, |
| - `internal/edge/homemap.go:538`, collision at `:582`), |
| - so a dead box that sorts first keeps winning. |
| + `internal/edge/homemap.go`), so a dead box that sorts first kept |
| + 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`). |
| - With two boxes taking turns, that is false. |
| + 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`). |
| @@ -95,25 +133,44 @@ back the same machine, if it can (`infra/modules/region-host/main.tf:497`). |
| - **Box**: one platform host machine. Not a customer fleet box; fleets |
| keep their own mechanism and are out of scope. |
| -- **Box id**: the name the claim uses for a box. For a box launched by |
| - an Auto Scaling group it is its EC2 instance id |
| - (`status.InstanceID()`, `internal/status/instanceid.go:37`), which AWS |
| - never reuses. A box that predates this spec keeps its label |
| - (`status.Label(machine-id)`). Either way the id is bound to one AWS |
| - instance by a **box record** (§5.1), never by an edges file. |
| +- **Box reference**: the name the claim uses for a box in `op.exec`, |
| + `participants`, `touched.boxes`, `inventory`, `lost`, owners and |
| + execution-lease keys. It is opaque and compared by exact equality |
| + (claim §2, rev 6.16). Under #212 option B it is the box's label key. |
| + The instance id is private: it lives in the box's roster entry, under |
| + `cloud` (H11). Spec 1 never parses a reference. The edges file keeps |
| + its field name `box_id` for it; plan 1a already publishes the label |
| + there. |
| +- **Roster**: `control/host-actors.json` (claim §10.1 D7, proposed, |
| + accepted for region HA by H11). Console-authored, root-signed, |
| + conditionally replaced. Each box entry binds a reference to its |
| + `enrollment`, `region`, `pool`, `state` (`active`, `quarantined`, |
| + `retired`) and `cloud: {provider, account, region, instance_id}`. |
| - **Executor**: the one box the claim's `op.exec` names for a host. |
| - **Relocatable host**: an exec-backed instance or a sidecar, whose whole |
| start state is in S3 or rendered from its record (HA5). Unit- and |
| socket-backed routes (the console, platform services) are **not** |
| relocatable: their unit definitions live outside the record. They stay |
| on their box, as today (A1-8). |
| -- **Eligible box**: a box with a verified box record (§5.1) that is fresh |
| - (nearest-region F1), reachable, hosting, serves the instance's pool, |
| - accepts inbound, holds the secrets key (R9), publishes the HA |
| - capability (§8), is not draining, and is not on the claim's `lost` list. |
| -- **Region placer**: one box per region, chosen by the existing lease |
| - election, that runs relocation recovery, failover (spec 3) and drain |
| - (spec 4). Its election lease only decides who acts, never what is true. |
| +- **Eligible box**: a box whose roster entry is `active`, whose `cloud` |
| + was proven by `internal/boxid` at enrollment (§5.1), and whose enrolled |
| + region and `cloud.region` are the placement's; whose edges file is fresh |
| + (nearest-region F1) and names the same reference; that is reachable, |
| + hosting, serves the instance's pool, accepts inbound, holds the secrets |
| + key (R9), publishes the HA capability (§8), and is not draining. For a |
| + given host it must also not be on that claim's `lost` list and not owe |
| + that host a `park-local` chore. |
| +- **Region placer**: a **regional worker** in claim P6-D5's sense: any |
| + active enrolled box in the region with access to the region's data |
| + bucket. It runs relocation recovery, failover (spec 3) and drain (spec |
| + 4). There is no separate leader roster. Correctness never depends on |
| + which worker acts: every step is a claim CAS conditional on `op.id`, |
| + the phase and the ETag (claim C2). Spec 3 may still use a lease to |
| + decide who **starts** relocations, for efficiency only. |
| +- **Prepared generation**: a generation built before any writer, from a |
| + sealed or pinned source, with its snapshot, level-0 anchor and install |
| + manifest, and opened at most once by a cold `AdmitWriter` (claim §6.4a |
| + item 3, P6-D3; moves §7.6). |
| - **Relocation**: changing a host's executor to another box **in the |
| same region** (§5.8). A move changes region; relocation does not. |
| @@ -130,11 +187,9 @@ participant in the phase that permits it (§5.8). Being in the right |
| region is necessary, never sufficient (claim C4 says this already; |
| today's code does not do it). |
| -**HA3. A local copy is trusted only if it is the current installation, |
| -completely installed.** Authority (`active_stamp`, claim §6.4) and |
| -evidence (an installation-complete marker, §5.5) are separate. A box |
| -skips restore only when both match the claim's `holder.stamp` and |
| -`holder.generation`. |
| +**HA3. Withdrawn (H13).** Claim R6 governs instead: no box skips restore. |
| +Every admitted writer purges its local database and restores from the |
| +certified remote (claim §6.4a), and under P6-D4 every admission is cold. |
| **HA4. Edges follow the newest installation.** When two edges files claim |
| one host, the edge believes the one carrying the higher `holder.stamp`. |
| @@ -149,13 +204,16 @@ lives only on the box running it. |
| **HA6. The executor changes only by a claim operation.** Create, a move, |
| or a relocation (§5.8). Each changes `op.exec` in a CAS that cites stop |
| -evidence (claim §6.1) or a termination fence (§5.9), and makes a fully |
| -populated new generation current with a new stamp. |
| +evidence (claim §6.1) or a lost-box fence, the termination fence |
| +included (§5.9), and writes `holder.stamp` in the same CAS (claim R6-4). |
| +A relocated host's data becomes current only through a cold |
| +`AdmitWriter` into a fully built prepared generation (claim §6.4a). |
| -**HA7. Termination evidence is bound to the executor.** A fence counts |
| -only if the terminated instance is the one the executor's box record |
| -names, in the deployment's own account and the region's own AWS region |
| -(A1-1). |
| +**HA7. Termination evidence is bound to the roster.** A fence counts only |
| +if the terminated instance is the one the box's roster entry records |
| +under `cloud`, in the deployment's own account and the region's own AWS |
| +region (A1-1, H11), and every EBS volume it had attached was |
| +`DeleteOnTermination: true` (H10). |
| ## 4. What stays the same |
| @@ -173,100 +231,106 @@ names, in the deployment's own account and the region's own AWS region |
| ## 5. Design |
| -### 5.1 Box identity, box records and evidence |
| +### 5.1 Box identity, the roster and evidence |
| + |
| +**Rev 5 (H11).** Spec 1's own `control/boxes/<id>.json` is no longer an |
| +authority. The roster is. What plan 1a built in `internal/boxid` becomes |
| +the evidence a box must present to be **enrolled**. |
| -**The box record (A1-1).** Before a box may be named by any claim in a |
| -multi-box region, it writes, create-only: |
| +**Enrollment.** A box asks to be enrolled by publishing its identity |
| +evidence, the record plan 1a defined: |
| - control/boxes/<box id>.json |
| + control/boxes/<box reference>.json |
| ```json |
| { |
| "v": 1, |
| - "box": "i-0abc…", |
| + "box": "<box reference>", |
| "identity_document": "<base64 IMDS instance identity document>", |
| - "identity_signature": "<base64 PKCS7 signature from IMDS>", |
| + "identity_signature": "<base64 RSA-SHA256 signature from IMDS>", |
| "written_at": "<RFC3339>" |
| } |
| ``` |
| -- The identity document is AWS-signed and names `accountId`, `region` |
| - and `instanceId`. Every reader verifies the signature against AWS's |
| - published certificate for the region, and checks that `accountId` is |
| - the deployment's account and `region` is the box's region. A record |
| - that fails is ignored and alerts. |
| -- For an Auto Scaling box, `box id == instanceId`, checked. Nothing |
| - else is needed: the signed document authenticates the whole id. |
| -- **A legacy box's label is not authenticated by AWS (A1-1 residual).** |
| - The signed document proves which instance wrote the record, not that |
| - the writer is entitled to the label. So a legacy record is admitted |
| - only with an operator's binding, `carlos ops box bind <label>`, run |
| - with the operator's own AWS credentials. It checks that: |
| - - the record's signed `instanceId` equals the instance id that the |
| - region's tofu state records for its `region-host` module (the |
| - module's `instance_id` output); |
| - - the label is the one already named in that region's claims |
| - (`touched.boxes`, `inventory`) and edges file. |
| - |
| - The command writes a second object, `control/boxes/<label>.bind.json`: |
| - `{"record_version_id": "…", "record_sha256": "…", "instance_id": "…", |
| - "tofu_instance_id": "…", "operator": "…", "at": "…"}`. It names the |
| - exact box record version it vouches for, so it can't be reused for a |
| - different record. |
| -- **Who may write what is enforced by S3, not by convention (A3-3).** |
| - The control bucket's policy (§6): |
| - - denies `PutObject` on `control/boxes/*.bind.json` to every principal |
| - except the deployment's operator roles; |
| - - denies `PutObject` on `control/boxes/*` without |
| - `s3:if-none-match: *`, so neither a record nor a bind can be |
| - replaced; |
| - - denies `DeleteObject` and `DeleteObjectVersion` on |
| - `control/boxes/*` to every principal, so neither can be removed to |
| - make room for a rebinding. |
| - |
| - A box can therefore write its own record once, and never a bind. A |
| - legacy record without a bind that names its exact version is not |
| - verified. All of this happens before any second box joins its region |
| - (§8). |
| -- The record is never rewritten. A box id whose record does not verify |
| - is never eligible, and a claim naming one is never relocated |
| - automatically: an operator resolves it. |
| +The object keeps plan 1a's storage rules: create-only, never deleted |
| +(§6). It grants nothing by itself. It is the evidence enrollment reads. |
| + |
| +Enrollment is the claim's (D7, L7). For region HA it must: |
| + |
| +- verify the record with `boxid.Verifier`: the signature under the |
| + embedded certificate for the document's region, `accountId` equal to |
| + the deployment's account, and the document's region equal to the AWS |
| + region the box is being enrolled into; |
| +- record the proven `accountId`, `region` and `instanceId` in the entry's |
| + `cloud: {provider: "aws", account, region, instance_id}`, and the |
| + record's SHA-256 beside it; |
| +- refuse a reference already enrolled to a different instance (#212's |
| + refusal to publish under a label another machine holds); |
| +- for a reference that already appears in claims (`touched.boxes`, |
| + `inventory`) or edges files, as a box predating region HA does, also |
| + check that the signed `instanceId` equals the region's tofu |
| + `region-host` module `instance_id` output. This is the check rev 4's |
| + operator bind made (A1-1 residual, A3-3). It now happens once, inside |
| + the operator-approved enrollment (claim §10.1 P3), so the separate bind |
| + object is not used. |
| + |
| +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. |
| **Edges file fields.** Each box's edges file |
| -(`internal/host/edgesfile.go:157`) gains: |
| +(`internal/host/edgesfile.go`) carries, as plan 1a built: |
| ```json |
| { |
| - "box_id": "i-0abc…", |
| + "box_id": "<box reference>", |
| "capabilities": ["region-ha-1"], |
| "draining": false, |
| "headroom": { "mem_free_mib": 2210, "disk_free_mib": 31200, "awake": 14 } |
| } |
| ``` |
| -- `box_id` must equal the box record's id; a mismatch makes the box |
| - ineligible. The edges file is evidence of liveness and configuration, |
| - never of identity. |
| +- `box_id` must equal an `active` roster reference; a file naming an |
| + unknown or inactive reference makes nothing eligible. The edges file is |
| + evidence of liveness and configuration, never of identity or |
| + membership (claim D7: heartbeats describe members, they do not create |
| + them). |
| - `capabilities` gates multi-box admission (§8). |
| - `draining` is set through the box by the placer (spec 4). |
| - `headroom` is the input to spec 2's choice. Spec 1 publishes it only. |
| -The console already reads these files with freshness |
| -(`internal/console/instancesplacement.go:93`). Nearest-region's |
| -`regioncandidates.go` keeps deciding which **regions** are eligible. |
| -This spec adds `eligibleBoxes(snapshot, boxRecords, region, pool)`, |
| -which returns the boxes, applying the predicate one box at a time |
| -(nearest-region `TestEligibilityNeverCombinesBoxes`). |
| +`eligibleBoxes(snapshot, roster, region, pool)` returns the boxes, |
| +applying the predicate one box at a time (nearest-region |
| +`TestEligibilityNeverCombinesBoxes`). The expected AWS region comes from |
| +the roster entry's enrolled region and `cloud.region`, never from a vote |
| +of edges files (§18's second correction, now answered). |
| ### 5.2 Create names a box |
| -Claim §5.1 step 4 becomes: CAS `op` to `serving` and set `exec` to |
| -`choose(eligibleBoxes(region, pool), app)` (K1). |
| - |
| -- Until spec 2 lands, `choose` is: the eligible box running the fewest |
| - claimed hosts, preferring one that runs no other instance of the app, |
| - ties broken by box id. It is a pure function over the snapshot and the |
| - claims the console already holds, and it is unit-tested alone. |
| +Claim §5.1's create intent names its executor (P5-D6 |
| +`selected_executor`, `executor_enrollment`), written in the step 2 CAS |
| +before any effect. For a relocatable host it is |
| +`choose(eligibleBoxes(region, pool), app)` (H12, L8). Step 4 |
| +(`CompleteCreate`) sets `op.exec` to exactly that box. |
| + |
| +`choose`, until spec 2 (H12): |
| + |
| +1. prefer a box that runs no instance of the app (H4's soft spread: it |
| + never refuses); |
| +2. then the most headroom; until spec 2 that is the fewest claimed hosts, |
| + counted from the console's claim-recovery listing (claim §5.1 step 5). |
| + A stale count only affects balance, never safety; |
| +3. then the greatest hexadecimal SHA-256 of `host + "\x00" + box |
| + reference` (claim P5-D2), and the smallest reference if two hashes |
| + are equal. |
| + |
| +It is a pure function over the roster, the edges snapshot and the |
| +counts, and it is unit-tested alone. |
| + |
| +- The choice is made once. Recovery never substitutes a newly available |
| + box (P5-D2). If the chosen box cannot complete the create (fenced, |
| + quarantined, or it never acknowledges), recovery cancels the create |
| + (claim §5.1 step 5, P5-D6), and the caller may create again. |
| - No eligible box: the create fails with today's "region has no box |
| that can take this" refusal (nearest-region). Spec 2 adds the |
| `unplaced` state for re-placement, where refusing is not possible. |
| @@ -274,81 +338,75 @@ Claim §5.1 step 4 becomes: CAS `op` to `serving` and set `exec` to |
| and gains no box field, so a record still describes residency, not |
| placement. |
| - A move into a multi-box region chooses its target box the same way, |
| - in its start CAS (K10). |
| + in its start CAS (L15). |
| ### 5.3 Reconcile: executing rows, held rows, former rows |
| -Reconcile distinguishes three cases for a relocatable host in its region |
| +Reconcile distinguishes these cases for a relocatable host in its region |
| (A1-6). Each is decided by a fresh claim read. |
| | The claim names this box as | Row | |
| |---|---| |
| | `op.exec`, op `serving` | mint or keep `ready` | |
| -| a participant whose phase's row column (§5.8 table; moves §9.6) says `ready` | keep `ready`. This is the relocating source in `starting`, and in `releasing` until its admission fence closes (A2-3) | |
| -| a participant whose phase's row column says held | mint or keep held, never `ready` | |
| -| neither, and no open obligation of its own for the host | **drop the registry row**, and nothing else | |
| - |
| -A box that still owes the host a `park-local` obligation keeps its row |
| -held until that obligation is done, so the guard and inventory it needs |
| -stay addressable. |
| - |
| -- Dropping a former executor's row is a registry change only. It never |
| - touches local files: that is the operation's `park-local` obligation |
| - (§5.8 step 6) under the host guard. This is a new rule (K11), separate |
| - from the stale-hold rule (claim §8, CC10), which only reopens a hold on |
| - the current executor. |
| +| `from` of a `relocating` op in `starting`, or in `releasing` until its admission fence closes (A2-3) | keep `ready` | |
| +| any other participant role of a running operation (§5.8 table; moves §9.6) | mint or keep held, with `hold_op` = the op id (moves §5.2), never `ready` | |
| +| the owner of an open `park-local` chore for the host | keep held until the chore's retirement removes the row | |
| +| none of these | mint nothing. An existing row is held, never served, and alerted as unexplained | |
| + |
| +- **Former executors (rev 5).** Rev 4.2 had reconcile drop a former |
| + executor's row as a registry change. Under claim P6-D2 a host's route |
| + and timer rows are typed inventory entries, and `park-local`'s |
| + retirement journal archives and removes them, conditional on their |
| + recorded ownership. So reconcile never deletes a relocatable host's |
| + row. It holds it, and the chore retires it under the host guard. A row |
| + is never removed by hostname alone, which could remove a successor's. |
| +- The stale-hold rule (claim §8, CC10) is unchanged: it reopens a hold |
| + only on the current executor of a `serving` host. |
| - **When reconcile reads claims.** The safety gate is the activator's |
| fresh claim read at every spawn (claim C4), not reconcile. So |
| reconcile reads a host's claim when it would mint a row, and re-checks |
| - the rows it keeps on a slow sweep, every 10 minutes. This is a stated |
| - exception to C4's "reconcile's decision to keep a row" (K11): a kept |
| - row that is stale for up to 10 minutes can route a request to this box, |
| - where the activator refuses to spawn. Reading every claim on every |
| - pass would cost about $2.30 a day per box at 2,000 hosts on 30-second |
| - passes. |
| + the rows it keeps on a slow sweep, every 10 minutes (H9). This is a |
| + stated exception to C4's "reconcile's decision to keep a row" (L12): a |
| + kept row that is stale for up to 10 minutes can route a request to |
| + this box, where the activator refuses to spawn. Reading every claim on |
| + every pass would cost about $2.30 a day per box at 2,000 hosts on |
| + 30-second passes. |
| - **Prompt changes.** The placer bumps the region's control serial after |
| - each executor CAS, so both boxes reconcile at once and re-read the |
| - claims of the hosts they hold or would mint. |
| + each executor CAS, so the region's boxes reconcile at once and re-read |
| + the claims of the hosts they hold or would mint. |
| - A claim read error keeps an existing row and mints none (claim C6). |
| ### 5.4 Edges and the home map |
| -- The edges-file pass (`edgesFilePass`, `edgesfile.go:272`) publishes a |
| - host as `home` (`:326`) only when this box is its executor, and adds |
| - the installation's stamp: |
| +- The edges-file pass (`edgesFilePass`, `edgesfile.go`) publishes a host |
| + as `home` only when this box is its executor **and** its row is |
| + `ready`, and adds the installation's stamp: |
| `"hosts": {"shop.bab.oncarlos.com": {"role": "home", "stamp": 41}}`. |
| -- The home map (`foldHomes`, `homemap.go:538`) resolves a host claimed by two files to |
| - the higher stamp (HA4). |
| + A relocation's `to` therefore publishes nothing while it installs and |
| + probes, and becomes home at `serving`. |
| +- The home map (`foldHomes`, `homemap.go`) resolves a host claimed by two |
| + files to the higher stamp (HA4). Plan 1a built this. |
| - **Unstamped entries.** Before §8's gate opens, every region has one |
| box, so there is no conflict to resolve. After it opens, every box |
| - publishes stamps, and an unstamped entry for a host that some file |
| - carries stamped is ignored. Two unstamped entries keep today's sorted |
| - rule and alert, because they mean the gate was bypassed (A1-9). |
| + publishes stamps for relocatable hosts, and an unstamped entry for a |
| + host that some file carries stamped is ignored. §18's correction |
| + stands: two unstamped entries are normal for everywhere-class routes, |
| + so the edge reports only two boxes at the same positive stamp. |
| - The edge never reads claims on the request path. |
| -### 5.5 The activator's local copy |
| - |
| -**The installation-complete marker (A1-5).** After a box has made an |
| -installation's data durable (database restored and fsynced, files |
| -applied to the manifest's sequence, timers imported), and only then, it |
| -writes and fsyncs: |
| +### 5.5 The activator's local copy: withdrawn (H13) |
| - <DataDir>/.installed/<host>.json |
| - {"incarnation": "…", "generation": "…", "stamp": 41, |
| - "db_marker": "<the moves generation marker>", "files_seq": 1882} |
| +Rev 4.2's installation-complete marker and its warm-cache check (HA3) are |
| +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. |
| -The warm-cache path (`activator.go:1127`, `backend_exec.go:265`) skips |
| -restore only when, under the host guard and against a fresh claim read: |
| - |
| -- the local stamp record's `active_stamp == holder.stamp` (authority); |
| -- the marker's `incarnation`, `generation` and `stamp` match the claim, |
| - and its `db_marker` matches the database's generation marker |
| - (evidence). |
| - |
| -Anything else, including a missing marker, restores from S3. A box that |
| -crashes mid-install therefore has authority and no evidence, and |
| -restores. Retirement (claim §6.3) parks the marker with the rest of the |
| -host's local state. The comment's one-box argument is replaced with 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 |
| +not evidence of a complete install, is answered more strongly: no local |
| +copy is ever trusted, complete or not. |
| ### 5.6 Host files reach S3, in order |
| @@ -393,11 +451,13 @@ Carloku maps its plans to this (H6). Apps with no setting get |
| **Always continuous, whatever the setting:** `instance.key`, |
| `report.token`, `<host>.env`, `<host>-sidecar.env`, and the host's wake |
| -state (§5.7: timer rows, the route's `NextDue` and `Replication`). They are small, and losing them is what kept kpmg down for |
| -1h54m (moves §1.2). |
| +state (§5.7: timer rows, the route's `NextDue` and `Replication`). They |
| +are small, and losing them is what kept kpmg down for 1h54m (moves §1.2). |
| **Ordering (A1-4).** Object versions do not say which update wins, so |
| -nothing is ever overwritten and one manifest decides. |
| +nothing is ever overwritten and one manifest decides. §18 records how |
| +plan 1a built it: content is identified by SHA-256, and `snapshot` is a |
| +periodic full publish with no `base`. |
| - **Objects are immutable.** Each upload goes to a new key, |
| `<holder.location>/files/<generation>/objects/<seq>-<sha256>`, written |
| @@ -406,46 +466,63 @@ nothing is ever overwritten and one manifest decides. |
| - **One sequence per host.** The executor numbers every local mutation |
| (write, rename, delete) with a monotonically increasing `seq`, kept |
| under the host guard and recovered from the manifest on restart. |
| -- **The manifest** is one object, |
| +- **The manifest** is one object per generation, |
| `<holder.location>/files/<generation>/manifest.json`, replaced only |
| - with `If-Match`: |
| - `{"seq": 1882, "base": "snapshots/0004.tar", "base_seq": 1700, |
| - "entries": {"<path>": {"object": "objects/1881-…", "seq": 1881} | |
| - {"deleted": true, "seq": 1874}}}`. |
| - A delete is a tombstone entry, never an S3 delete. The manifest is |
| - published only after every object it names is durable, and its `seq` |
| - only increases, so a late manifest write fails its `If-Match`. |
| -- **Snapshots** are sealed archives taken at a mutation boundary: the |
| - executor records `base_seq` before reading the directory, and |
| - mutations after `base_seq` go in `entries`. A snapshot becomes the |
| - base only through a manifest CAS. Older snapshots and unnamed objects |
| - are reaped after a day. |
| -- **Restore** reads the manifest once, then fetches its base and entries |
| - by the exact versions it lists (claim C3). Nothing else in the prefix |
| - is read. |
| + with `If-Match`. A delete is a tombstone entry, never an S3 delete. The |
| + manifest is published only after every object it names is durable, and |
| + its `seq` only increases, so a late manifest write fails its |
| + `If-Match`. |
| +- **Restore** reads the manifest once, then fetches the objects it names |
| + and checks each hash (§18). Nothing else in the prefix is read. |
| - **Release flush.** A box giving up a host publishes every pending |
| mutation, **whatever the app's setting**, before its stop evidence |
| (§5.8's release sequence). |
| +**Under the claim (rev 5).** Three rules follow from the claim as it now |
| +stands. |
| + |
| +- **The publisher is a generation-bound writer.** It belongs to the |
| + writer session, like the replicator: it is started for the `{location, |
| + generation, session}` the admission named, refuses any key outside |
| + `<location>/files/<generation>/`, and stops with the session. It is a |
| + producer for stop evidence (claim P6-D1) and is joined before the |
| + receipt. Its PUTs are a second ordinary-replication exception to claim |
| + C3 (L13). |
| +- **Each cold admission starts a new manifest.** Under P6-D4 every wake |
| + is a cold admission into a new generation. Before the app starts, the |
| + admitting box writes `files/<new generation>/manifest.json` |
| + create-only, as a copy of the predecessor generation's manifest read by |
| + exact version from the same baseline it restores. Its entries keep |
| + naming the predecessor's objects where they are, so an unchanged file |
| + is never uploaded again. A late write from the predecessor's publisher |
| + lands in the predecessor's prefix, which nothing admitted reads again. |
| +- **Old objects are retired by the claim, never reaped.** Rev 4.2's "reaped |
| + after a day" is withdrawn (plan 1a never built it). A dead generation's |
| + `files/<generation>/` prefix is retired with that generation, by the |
| + `park-generation` chore `PublishGeneration` queues, except objects that |
| + a manifest in the live set still names (L13). The at-rest sweep treats |
| + `files/` as part of the location, never as residue to classify |
| + blindly (claim P6-D3). |
| + |
| A `snapshot` app's files can be up to the interval older than its |
| database after a failover, and the console says so on the app's |
| Overview. |
| **Moves.** A move keeps its sealed archive at the cut (moves §8), and |
| -installs a fresh manifest in its new generation (K8). |
| +installs a fresh manifest in its new generation (L17). |
| ### 5.7 What a new executor rebuilds |
| | State | How the new box gets it | |
| |---|---| |
| -| Database | restored from the pinned recovery set (§5.8) into the new generation | |
| -| Files directory, env files | the manifest (§5.6), pinned | |
| +| Database | built from the pinned recovery set into a prepared generation, then restored from it by the probe's cold `AdmitWriter` (§5.8) | |
| +| Files directory, env files | the pinned manifest (§5.6), copied into the prepared generation | |
| | Wake state | the host's timer rows, as `Registry.ReplaceTimers` rows (moves §9.4), and the route's `NextDue` and `Replication` (moves §6.2), published continuously as one entry under the manifest (A1-7) | |
| -| `<host>.config.env` | rendered for the held row (moves §9.1), needs the secrets key (R9) | |
| -| Release | materialized for the held row (moves §9.2) | |
| +| `<host>.config.env` | rendered for the held row (`RenderHeld`, claim §6.1 CC13, P6-D3), needs the secrets key (R9) | |
| +| Release | materialized for the held row (`MaterializeHeld`) | |
| | Certificates | the cert mirror's boot refresh (on main) | |
| -| Registry row | reconcile, once the claim names this box (§5.3) | |
| -| Inventory | written by the new box before it first materializes state (claim §6.3) | |
| +| Registry row | reconcile, held while it installs, `ready` at `serving` (§5.3) | |
| +| Inventory | written by the new box before it first materializes state (claim §6.3, P6-D2) | |
| **Wake state (A1-7).** The executor publishes the host's wake state as |
| an always-continuous entry in the manifest whenever any of it changes: |
| @@ -460,7 +537,8 @@ landing does (moves §7.6). A once-timer the app registered is |
| therefore in S3 within about a second of the app being told it |
| succeeded. On install the new box imports the timer rows with |
| `ReplaceTimers`, preserving `next_at`, `due_at`, `attempts` and |
| -`registration`. |
| +`registration`. Timers on held rows stay frozen (moves §9.4, claim |
| +P6-D8) until the row is `ready`. |
| - An occurrence that fell due while the host had no executor fires once |
| when the new executor imports it: the converger catches up from the |
| @@ -470,29 +548,51 @@ succeeded. On install the new box imports the timer rows with |
| ### 5.8 Relocation |
| -A new claim op kind, `relocating` (K2), from `serving` only, for a |
| -relocatable host, within one region. Its intent names |
| -`{from, to, reason, generation_from}`, where reason is `drain`, |
| -`rebalance` or `failover`. |
| - |
| -**Phases (A1-3).** Each is a claim CAS, conditional on `op.id` and the |
| -ETag. The recovery owner for every phase is the region placer, which |
| -replays from the claim alone (claim C2). |
| - |
| -| Phase | Who acts | `op.exec` | Rows (§5.3) | May spawn | |
| -|---|---|---|---|---| |
| -| `starting` | placer writes intent; `from` (if alive) and `to` write execution leases | `from` | `from` ready; `to` held | `from` only | |
| -| `releasing` | `from` runs the **release sequence** (below). Or, for failover, the placer writes the termination fence (§5.9) | `from` until evidence | `from` ready until its admission fence closes, then held; `to` held | `from`, until its admission fence closes | |
| -| `pinning` | placer lists the recovery set in `generation_from` and journals exact versions (below) | `none` | `from` held (if alive); `to` held | nobody | |
| -| `installing` | `to` restores the pinned set into a new generation `G'`, applies the pinned manifest, imports wake state, and writes `G'`'s replication baseline (below) | `none` | `from` held (if alive); `to` held | nobody | |
| -| `installed` | placer CAS: `exec: to`, `holder.generation: G'`, `holder.stamp`: this CAS's `gen` | `to` | `from` held until its obligation; `to` held | `to` (probe only) | |
| -| `probing` | `to` probes (moves §7.7, same region), within the probe deadline | `to` | as `installed` | `to` (probe only) | |
| -| `probe-failed` | `to` runs the release sequence for `G'` (below) | `none` | as `installed` | nobody | |
| -| `serving` | placer CAS back to `serving`; `from` gets a `park-local` obligation unless terminated | `to` | `to` ready; `from` held until its obligation is done, then dropped | `to` | |
| +A new claim op kind, `relocating` (L1), from `serving` only, for a |
| +relocatable host, within one region. It is the stateful, same-region |
| +executor change the claim's `placing` refuses (P5-D5). |
| + |
| +**The start CAS** writes `op.kind`, `op.id` and the intent before any |
| +other effect (claim C2): |
| + |
| + {from, to, to_enrollment, region, reason, stamp_from, |
| + generation_from, fence?} |
| + |
| +`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. |
| + |
| +**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 |
| +regional workers (§2, claim P6-D5), which replay from the claim alone |
| +(claim C2). Each worker first checks its own roster entry is `active` in |
| +this region. Two workers racing make the same CAS, and one fails. `from` |
| +and `to` hold execution leases (claim §7.1, D6) for as long as they are |
| +participants. |
| + |
| +**Phases (A1-3).** In the "admits" column, "writer" means a writer |
| +admission (`AdmitWriter`) is legal for that box; nothing else may open |
| +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` | |
| +| `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 | |
| +| `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` | |
| **The release sequence (A3-2).** Whenever a live box gives up a host, |
| the source in `releasing` or a failed target in `probe-failed`, it does |
| -these in order, journaling each: |
| +these in order, journaling each. It runs inside claim P6-D1's stop |
| +collection: root's collector has recorded its durable fence, and the |
| +agent does steps 1 to 3 before it closes the producers and returns its |
| +drain acknowledgement. |
| 1. **Stop every writer (A4-1).** Close admission, drain spawn attempts, |
| drain in-flight timer deliveries (moves §9.4), then stop the host's |
| @@ -502,91 +602,156 @@ these in order, journaling each: |
| this host, identified by the agent's pid and the replicator's own |
| descriptors (A5-1). Any other holder fails the step. From here nothing |
| but the replicator can touch the database, and nothing at all can |
| - change files or wake state. |
| + change files or wake state. `internal/stopevidence` has no check of |
| + this form today: `Collect` requires the replicators closed. Rev 5 |
| + requests a writers-stopped check that allows exactly these |
| + descriptors (L10). |
| 2. **Flush the database:** final checkpoint and `SyncAndWait`, then |
| - record the **final TXID** `N`, the `MaxTXID` of the newest level-0 |
| - file (moves rev 7.6 §5.1 step 1). |
| + record the **final TXID** `N`: the stopped database's own position. |
| + The step passes only once a listing shows the newest level-0 file's |
| + `MaxTXID` equal to `N` (moves §5.1 step 1). A sync error is not |
| + swallowed (claim P6-D4's warning about `Replicator.Close`); it retries, |
| + and a flush that never reaches `N` goes to `stuck`. |
| 3. **Publish every pending file and wake-state mutation**, whatever the |
| app's `files_durability`, and record the manifest's final `seq`. |
| 4. **Finish stop evidence:** close the replicator (`DB.Close`) and the |
| - file publisher, then run claim §6.1's **unrestricted** check: no |
| - holder at all of the database, WAL or SHM files in `/proc/*/fd`, and |
| - every other condition. Only now is the release complete. |
| + file publisher, then root completes claim §6.1's **unrestricted** |
| + check (`stopevidence.Collect`, P6-D1): no holder at all of the |
| + database, WAL or SHM files in `/proc/*/fd`, and every other |
| + condition. The receipt is published (P5-D3) with its `evidence_at`. |
| + Only now is the release complete. |
| Because step 1 empties the process tree first, the positions recorded in |
| -steps 2 and 3 really are final. |
| +steps 2 and 3 really are final. The session ends uncertified, as every |
| +session does under P6-D4; coverage (below) is what keeps its writes. |
| The journal entry is `{"released_by": "<box>", "generation": "<G>", |
| -"final_txid": N, "manifest_seq": S}`, and `pinning` refuses to pin less |
| -than it. |
| +"session": S, "final_txid": N, "manifest_seq": M, "receipt": "<key>", |
| +"receipt_sha256": "…"}`, and `pinning` refuses to pin less than it. |
| -**The pinned recovery set (A1-2).** In `pinning`, the placer lists |
| -`generation_from` and journals the exact object versions that make up the |
| -database (latest snapshot and the LTX files after it) and the manifest |
| -version, files and timers included. |
| +**The pinned recovery set (A1-2).** In `pinning`, a worker runs |
| +`genselect.Select` against the claim observation of its `pinning` CAS: |
| +`holder.generation`, the unfinished run in `holder.admissions` and the |
| +marker, all in this region's bucket (claim §6.2a, §6.4a item 3). It |
| +journals the plan's exact object versions (the snapshot and every LTX |
| +file after it, contiguous) and the exact version of the files manifest |
| +of the same generation, files and timers included. |
| - **After a release sequence** (drain, rebalance, probe failure): the set |
| must reach the journaled `final_txid` and `manifest_seq`. If the listing |
| has not caught up, `pinning` waits; it never pins less than what the |
| releasing box flushed. |
| -- **Failover:** the placer pins after the fence plus 30 seconds, so |
| - requests S3 had already accepted from the terminated box have |
| - completed. Whatever did not land is the H3 loss window. |
| - |
| -**Populating the new generation (A1-2, A2-1).** `installing` restores |
| -from the pinned versions, never from "the current generation", and |
| -writes `G'`'s **replication baseline** before `installed`, exactly as a |
| -move's install does (moves rev 7.6 §5.1 steps 2 and 7): |
| - |
| -- a full snapshot of the restored database at its final TXID `N`; |
| -- the **level-0 anchor**, one level-0 LTX file `[N, N]`. The pinned |
| - Litestream derives a box's replication position from the newest remote |
| - level-0 file. A generation holding a snapshot and nothing at level 0 |
| - restarts at TXID 1, and a cold restore from the snapshot then skips |
| - every later write (moves rev 7.6 R5-1); |
| -- a manifest naming the files, env and wake state; |
| -- verification of all three by a fresh read before the `installed` CAS. |
| +- **Failover:** the worker pins after the fence's `observed_at` plus 30 |
| + seconds, so requests S3 had already accepted from the terminated box |
| + have completed. Whatever did not land is the H3 loss window. This is a |
| + loss bound, not a safety bound: the pin names exact versions, and a |
| + later PUT can only add a version nothing reads. |
| + |
| +**Building the prepared generation (A1-2, A2-1).** In `installing`, `to` |
| +builds `P` exactly as a move's landing builds its generation (moves §7.6 |
| +`building` and `published`, L16), with the pinned versions as its source |
| +in place of a staged replica: |
| + |
| +- under the replica lease on `holder.location` (claim C3), restore the |
| + pinned versions with the planner, verifying each file's checksum, |
| + contiguity, the final position `N` and `PRAGMA integrity_check`; |
| +- write the build intent, then the full **snapshot** `[1, N]`, then the |
| + **level-0 anchor** `[N, N]`, each acknowledged, then the completed |
| + **install manifest** with each `versionId`, `N`, checksums and the |
| + database's SHA-256. The pinned Litestream derives a box's replication |
| + position from the newest remote level-0 file. A generation holding a |
| + snapshot and nothing at level 0 restarts at TXID 1, and a cold restore |
| + 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). |
| + |
| +**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); |
| +- **`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); |
| +- **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`. |
| + |
| +**A host with nothing replicated.** If the pin's `N` is 0 (the app never |
| +committed a transaction), there is no prepared generation: claim |
| +P6-D3 forbids a `[1, 0]` snapshot or a `[0, 0]` anchor. `installing` |
| +then builds only the files manifest and local state, and the first |
| +probe attempt is an ordinary cold admission into a fresh, empty |
| +generation (claim §6.4a, "Empty bootstrap"). |
| The test is the moves one, run for relocation: relocate, write, |
| replicate, terminate the new executor, cold-restore, and check that every |
| -replicated write is present (`internal/sim/litestreamfacts`). Moves §5.1 forbids restoring another |
| -generation **as** the installed one; relocation instead builds `G'` from |
| -a pinned set and only then makes `G'` installed, which is the move |
| -landing's shape (moves §7.6) within one bucket. Late writes from the old |
| -installation land in `generation_from`, which nothing admitted reads |
| -again (claim C3a within one incarnation, moves §5.1). |
| +replicated write is present (`internal/sim/litestreamfacts`). Late writes |
| +from the old installation land in `generation_from`, which nothing |
| +admitted reads again, and which publication retires. |
| **The no-reinstall boundary (A1-3).** Once the `installed` CAS succeeds: |
| -- nobody restores `G'` again: replay from `installed` or `probing` goes |
| +- nobody builds `P` again: replay from `installed` or `probing` goes |
| forward (probe, then `serving`), never back to `installing`; |
| -- `to` writes its installation-complete marker (§5.5) before its probe |
| - spawns; |
| -- a worker that paused before `installed` and resumes revalidates the |
| - phase under the host guard and stops. |
| +- `P` is opened at most once. After its first admission, every restart |
| + takes a fresh generation from it; |
| +- a worker or `to` that paused and resumes revalidates the phase under |
| + the host guard, with the stamp it captured, and stops. |
| -Replay from `installing` (before `installed`) discards `to`'s partial |
| -local state (retire-artifacts, claim §6.4) and installs again from the |
| -same pinned set. Nothing has served from `G'` yet, so nothing is lost. |
| +Replay from `installing` (before `installed`) parks `to`'s partial local |
| +state with `retire-artifacts` (claim §6.4), and rebuilds `P` from the |
| +same pin. The build intent makes the bytes identical (moves §7.6). |
| +Nothing has opened `P` yet, so nothing is lost. |
| -**Exclusion.** Only `to` installs, holding the replica lease on `G'`; |
| -the placer is the only claim writer for this op, under its election |
| -lease, and every CAS is conditional on `op.id` and the phase. |
| +**Exclusion.** Only `op.exec` installs or admits, and only `to` is |
| +`op.exec` from `installing` on. Every CAS is conditional on `op.id` and |
| +the phase. `to` holds the replica lease while it builds. |
| **Replacing a participant (A2-2, A2-7).** The claim allows a new |
| -operation only from `serving`, so relocation defines its own exits |
| -(K2). Each is one CAS, conditional on `op.id` and the phase, that cites |
| -its evidence and names the replacement `to'`. Every rule that applied to |
| -the phase still applies, and `to'` writes its execution lease before |
| -the op leaves that phase. |
| +operation only from `serving`, so relocation defines its own exits (L1). |
| +Each is one CAS, conditional on `op.id` and the phase, that cites its |
| +evidence and names the replacement `to'`. A CAS that moves `op.exec` |
| +writes the stamp under R6-4. Every rule that applied to the phase still |
| +applies, and `to'` acknowledges its execution lease before the op leaves |
| +that phase. |
| | `to` stops being usable | Evidence | The op resumes at | |
| |---|---|---| |
| | 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` before the pin is journaled | `to`'s termination fence | `pinning` | |
| -| terminated after the pin is journaled, before `installed` | `to`'s termination fence | `installing` from the journaled pin, into a fresh generation `G''`. The old `to`'s partial `G'` objects are abandoned | |
| -| terminated at or after `installed` | `to`'s termination fence | a nested failover: `generation_from` becomes `G'` (which holds `to`'s baseline and anything it replicated), from `pinning` | |
| -| alive, but its probe fails or misses the **probe deadline** (10 minutes) | `to`'s release sequence, in `probe-failed` | a nested relocation from `G'`, 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 | |
| +| 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 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. |
| @@ -597,229 +762,367 @@ the op leaves that phase. |
| says why. |
| - A `probe-failed` target that cannot finish its release sequence (its |
| cgroup won't drain, claim §6.1, or its flush fails) also goes to |
| - `stuck`. Nothing moves away from |
| - a live box without its stop evidence. |
| + `stuck`. Nothing moves away from a live box without its stop evidence. |
| + |
| +**What a relocation leaves behind.** `generation_from` and the |
| +predecessor run are retired by `PublishGeneration`'s `park-generation` |
| +chores in this region. An abandoned `P` is parked by the at-rest sweep. |
| +`from`'s local state is retired by its `park-local` chore, or discharged |
| +with the fence (§5.9). Relocation installs into the region's host |
| +namespace, so it waits for `quiet_after[region]` like a push (claim |
| +§6.2a); for a live location that time has normally passed. |
| **Cost of a drain:** one cut of a few seconds, like a move's (M2), with |
| -no cross-region copy. Failover's gap is detection plus restore (spec 3). |
| +no cross-region copy, plus one snapshot and anchor of the database in |
| +the region (moves §7.3's T11 arithmetic, same region). Failover's gap is |
| +detection plus restore (spec 3). |
| ### 5.9 The termination fence |
| -A termination fence is written into the operation's journal: |
| +**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: |
| + |
| +- 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. |
| + |
| +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). |
| + |
| +- `stopped` and `stopping` do not count, because a stopped box can start |
| + again with its disk. A missing instance, `InvalidInstanceID.NotFound`, |
| + an API error, a partial reply, or a lookup in another account or |
| + region is **never** evidence. AWS keeps a terminated instance visible |
| + in `DescribeInstances` for typically under an hour, so absence proves |
| + nothing. All of those go to the operator: `carlos ops host resolve |
| + --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. |
| + |
| +**The fence record.** The worker writes one record per terminated |
| +enrollment, create-only (L4): |
| + |
| + control/box-fences/<enrollment>.json |
| ```json |
| -{"box": "i-0abc…", "instance_id": "i-0abc…", "account": "123…", |
| - "aws_region": "eu-west-1", "state": "terminated", |
| - "observed_at": "<RFC3339>", "via": "describe" | "event", |
| - "event_id": "<EventBridge event id, when via=event>"} |
| +{"v": 1, "box": "<box reference>", "enrollment": "<enrollment>", |
| + "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>", |
| + "written_by": {"box": "<reference>", "enrollment": "<enrollment>"}} |
| ``` |
| -**What counts (A1-1, A1-11).** |
| - |
| -- `instance_id`, `account` and `aws_region` must equal the executor's |
| - verified box record (§5.1, HA7). |
| -- Only `terminated`. `stopped` and `stopping` do not, because a stopped |
| - box can start again with its disk; those need the operator's |
| - `carlos ops host resolve --declare-lost` (claim §7.2). |
| -- A missing instance, `InvalidInstanceID.NotFound`, an API error, or a |
| - lookup in another account or region is **never** evidence. AWS keeps a |
| - terminated instance visible in `DescribeInstances` for typically under |
| - an hour, so absence proves nothing. |
| - |
| -**Three ways to observe it.** |
| - |
| -1. **The durable event.** An EventBridge rule in each region sends EC2 |
| - "Instance State-change Notification" events with `state: terminated` |
| - for the deployment's account to an SQS queue (14-day retention). The |
| - queue's policy accepts messages only from that rule's ARN. The placer |
| - reads the queue; an event whose `account`, `region` and instance id |
| - match a box record is evidence, `via: "event"`. |
| -2. **A direct read.** `DescribeInstances` for the instance id, in the |
| - region, returning `terminated` with the deployment's `OwnerId`, |
| - `via: "describe"`. |
| +It is not AWS-signed: like claim D2's operator observation, it is the |
| +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: |
| + |
| +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. |
| 3. **The group's own history.** For a box launched by an Auto Scaling |
| - group, `DescribeScalingActivities` for the region's group: an |
| - activity terminating that instance id with status `Successful`, |
| - `via: "activity"`. AWS keeps activity history for six weeks. Spec 4 |
| - verifies on dev that `Successful` is recorded only once the instance |
| - has reached `terminated`; until it is verified, this method is off. |
| + 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. |
| **What is not guaranteed (A2-4).** EC2 delivers state-change events to |
| -EventBridge on a best-effort basis, so the queue holds only events that |
| -arrived. When all three methods come back empty, there is **no |
| -automatic recovery**. The placer marks the box's hosts |
| -`awaiting-evidence`, alerts at once, and keeps retrying the three reads. |
| -The only way out is claim §7.2 unchanged: an operator's |
| -`carlos ops host resolve --declare-lost`, which needs the instance's |
| -terminal state (`stopped` or `terminated`) read through the cloud API |
| -with the operator's own credentials. A CloudTrail `TerminateInstances` |
| -record is **not** evidence (A3-1): it proves a request was made, and an |
| -instance can stay `shutting-down` after a successful one. The console |
| -may show it to help an operator find the instance, nothing more. If no |
| -terminal state can be read, the hosts stay `awaiting-evidence`. That is |
| -a liveness gap, accepted: it needs a lost event, a gap of more than an |
| -hour before anyone looks, and a group whose history doesn't show the |
| -termination. Absence is never evidence, at any point. Spec 3 sets how long the placer retries |
| -before alerting, and owns the loop that reads the queue and history. |
| - |
| -- The placer reads the state itself. It never trusts a box's own |
| - report, an edges file, or a box record's claims about liveness. |
| -- A terminated instance cannot run again, so a terminated box needs no |
| - quarantine or `--readmit`. Its id still goes on `lost`, so any later |
| - file naming it is refused. |
| -- The root volume must have `DeleteOnTermination`, so no disk outlives the |
| - box (§6). |
| +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 |
| +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 |
| +request was made, and an instance can stay `shutting-down` after a |
| +successful one. The console may show it to help an operator find the |
| +instance, nothing more. If no terminal state can be read, the hosts stay |
| +`awaiting-evidence`. That is a liveness gap, accepted. Absence is never |
| +evidence, at any point. Spec 3 sets how long the placer retries before |
| +alerting, and owns the loop that reads the queue and history. |
| + |
| +**What the fence does (L2 to L5).** |
| + |
| +- **It is a lost-box fence** (claim C5, §4) for every host whose claim |
| + names the box. A relocation started on it may move `op.exec` off the |
| + box. |
| +- **The box goes on each affected claim's `lost` list**, with the fence's |
| + reference. A terminated instance cannot run again, so it needs no |
| + quarantine and no `--readmit` (H1). Its reference never names a |
| + working box again. |
| +- **Its local chores are discharged.** Every volume was deleted with the |
| + instance (H10), 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 |
| + scopes (D5). Remote scopes it justifies take the fence's `observed_at` |
| + as their original evidence time (claim P5-D3, D5). |
| +- **The roster follows later.** The console moves the box's roster entry |
| + 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. |
| +- **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`: |
| + wake state was published continuously, up to H3's window. |
| ## 6. Infrastructure and IAM (A1-12) |
| -- **Box role** gains `ec2:DescribeInstances` with a condition on |
| - `ec2:Region`, and `autoscaling:DescribeScalingActivities` with a |
| - condition on `aws:RequestedRegion`, both equal to the box's region, plus |
| - SQS `ReceiveMessage`/`DeleteMessage` on its region's termination |
| - queue. Describe actions do not support resource-tag conditions, so |
| - deployment membership is **not** an IAM property: the verifier checks |
| - `OwnerId`, the region and the box record (§5.9). No `ec2:Stop*`, |
| - `Terminate*` or `Modify*`, and no Auto Scaling write rights. |
| +- **Box role** keeps plan 1a's `ec2:DescribeInstances` with a condition |
| + on `ec2:Region`, and `autoscaling:DescribeScalingActivities` with a |
| + condition on `aws:RequestedRegion`, both equal to the box's region, |
| + plus SQS `ReceiveMessage`/`DeleteMessage` on its termination queue. |
| + Describe actions do not support resource-tag conditions, so deployment |
| + membership is **not** an IAM property: the verifier checks `OwnerId`, |
| + the region and the roster entry (§5.9). No `ec2:Stop*`, `Terminate*` or |
| + `Modify*`, and no Auto Scaling write rights. It also needs the claim's |
| + own grants: `s3:ListBucketVersions`, `s3:GetObjectVersion` and |
| + `s3:DeleteObjectVersion` on its region's data bucket (claim §6.2a), |
| + which `genselect` and the parker use. |
| - **Console role:** unchanged, no EC2 rights. |
| - **S3 (A2-6).** Two kinds of write, kept apart: |
| - - **Create-only** (`If-None-Match: *`): content objects and snapshots, |
| - `instances/<host>/*/files/*/objects/` and `…/snapshots/`, in the |
| - region's data bucket; box records and binds, `control/boxes/`, in the |
| - control bucket. |
| + - **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. |
| - **Conditional replace** (`If-Match`, or `If-None-Match: *` for the |
| first write): `instances/<host>/*/files/*/manifest.json` only. |
| S3 enforces both in policy (A3-3): the data bucket denies `PutObject` |
| - on `…/objects/*` and `…/snapshots/*` without `s3:if-none-match: *`, and |
| - on `…/manifest.json` without either `s3:if-match` or |
| + on `…/objects/*` without `s3:if-none-match: *`, and on |
| + `…/manifest.json` without either `s3:if-match` or |
| `s3:if-none-match: *`. Each Deny carries |
| `s3:ObjectCreationOperation: true`, so it applies to `PutObject`, |
| `CopyObject` and `CompleteMultipartUpload`, never to |
| `CreateMultipartUpload` or `UploadPart`, which can't carry the headers |
| - (A4-2). A large snapshot is uploaded in parts and completed with |
| - `If-None-Match: *`; the `control/boxes/` rules in §5.1 carry the same |
| - qualifier. The one writer, `hostfiles.Publish`, sends the |
| - headers and is tested against both refusals, and for a multipart |
| - snapshot that completes with the header and one refused without it. The control bucket's |
| - `control/boxes/` rules are in §5.1. Each Deny is scoped to its prefix |
| - only: a broad Deny on this bucket once broke every lease release. Plus |
| - `s3:GetObjectVersion` on the files prefix, and the claim CAS rights the |
| - claim spec lists. |
| -- **Tofu:** the `region-host` module gains `delete_on_termination = true` |
| - on the root volume, the EventBridge rule and the queue. Moving to an |
| - Auto Scaling group is spec 4; spec 1 runs on today's fixed boxes and on |
| - a second fixed box added by hand. |
| + (A4-2). The one writer, `hostfiles.Publish`, sends the headers and is |
| + 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-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 |
| + retirement under `files/` is by exact version, through the parker, |
| + like every other retirement (claim C3). |
| +- **Tofu:** the `region-host` module has `delete_on_termination = true` |
| + on the root volume (plan 1a), and must have it on every other EBS |
| + volume a box attaches, since H10 refuses to fence a box with one that |
| + survives. Moving to an Auto Scaling group is spec 4; spec 1 runs on |
| + today's fixed boxes and on a second fixed box added by hand. |
| ## 7. Failure modes |
| | 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; it wins the placer election, reads the termination event from the queue, and relocates every host to itself. | |
| +| 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. | |
| +| 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. | |
| -| A forged or confused edges file names a terminated instance | ignored: identity comes only from the AWS-signed box record (HA7). | |
| -| Placer dies mid-relocation | the next elected placer replays from the claim (§5.8). | |
| -| Target dies after installing | a nested failover from `G'` (§5.8). | |
| +| 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 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). | |
| | Target alive but its probe keeps failing | stop evidence, then a nested relocation to another box; after two replacements, `stuck` and an alert (§5.8). | |
| | No termination evidence can be found | `awaiting-evidence`, an alert, and the operator's `--declare-lost` (§5.9). | |
| -| Two files claim a host | the higher stamp wins (HA4). Two unstamped entries alert. | |
| +| Two files claim a host | the higher stamp wins (HA4). Two at the same stamp are reported (§18). | |
| | Claim read fails on reconcile | keep existing rows, mint none (C6). | |
| | `snapshot` app fails over | files lose up to the interval; the database loses about a second. Stated on Overview. | |
| | A unit- or socket-backed route's box dies | not relocated (A1-8). It comes back with its box, or by the HA ladder's restore runbook, as today. | |
| ## 8. Rollout (A1-9) |
| -1. **Prerequisite:** the claim and its floor are live (claim §10), and |
| - every host in the region has a claim (adopted under claim §9). |
| +1. **Prerequisite:** the claim and its floor are live (claim §10), the |
| + roster exists with every box enrolled from `internal/boxid` evidence |
| + (§5.1), and every host in the region has a claim (adopted under claim |
| + §9 and P5-D2, which requires exactly one proven installation owner). |
| 2. Ship §5 dormant behind `CARLOS_REGION_HA`, with capability |
| `region-ha-1` published in each box's edges file once enabled. With one |
| box per region, every rule is a no-op; ship it to all four regions and |
| watch. |
| 3. **The multi-box gate.** A second box may join a region only when: |
| - - every relocatable host there has a claim (K5); |
| + - every relocatable host there has a claim; |
| - every box in the region, and every edge in the deployment, publishes |
| `region-ha-1` and runs at or above the HA floor; |
| - - every box in the region has a verified box record; |
| - - the region's termination queue exists. |
| + - 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 HA floor joins the protocol floor (claim §10): every path that |
| + The HA floor joins the protocol floor (claim §10, D1): every path that |
| restores an executable (system apply, rollback, boot recovery from |
| `carlos.prev`) refuses a binary below it once a region has two boxes. |
| The gate is checked in `carlos system`, in the console's box list, and |
| by each box at start: a box that finds a second box in its region |
| without the gate satisfied refuses to mint relocatable rows and |
| alerts. |
| -4. Rehearse on dev with two fixed boxes: create spreads across both; |
| +4. **Relocation by drain** stays off until the claim accepts L9; failover |
| + relocation needs L1 to L6. |
| +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. |
| -5. Then specs 2, 3, 4. |
| + 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). |
| +6. Then specs 2, 3, 4. |
| ## 9. Changes requested of the claim and moves specs |
| -For platform-1e (claim) and platform-d8 (moves). Each is needed before |
| -those specs finalise a one-box-per-region assumption. |
| - |
| -| # | Spec | Change | |
| -|---|---|---| |
| -| K1 | claim §5.1 step 4 | `exec` is the box `choose()` picks among the region's eligible boxes, not "the record region's box". | |
| -| K2 | claim §4, §8 | New op kind `relocating` (§5.8): same region, from `serving`, with its phase table, admission and rows per phase, the `installed` no-reinstall boundary, the phase-specific replacement table (termination and probe failure), the two-replacement bound and `stuck`, and the release sequence (stop every application writer first, allowing only the box's own replicator handles; then journal the final TXID and manifest `seq`; then close the replicator and run the unrestricted holder check; for the source and for a failed target). Recovery owner: the region placer. Excludes moves and placements, as `placing` does. | |
| -| K3 | claim §7.2, CC5 | A **termination fence** (§5.9), bound to a verified box record, is a lost-box fence, written automatically by the region placer. `terminated` only; `stopped` stays operator-only. No `--readmit` for a terminated box; it still goes on `lost`. The operator path keeps §7.2's terminal-state rule: a CloudTrail request record never substitutes for it. | |
| -| K4 | claim §8 | Region placers (boxes) need claim CAS rights for `relocating` and for removing a terminated box's obligations. | |
| -| K5 | claim §9 | Adoption names "the record region's serving box". With several boxes that is ambiguous, so adoption must finish while the region has one box (§8 step 3). | |
| -| K6 | claim §2 | Box names in `op.exec`, `participants`, `touched.boxes`, `inventory` and `lost` are box ids bound by `control/boxes/<id>.json` (§5.1). A legacy label is valid only with a verified record. | |
| -| K7 | moves §7.10 | A move whose participant is terminated mid-move takes the termination fence as M16's evidence automatically, under the same before-commit rules. Moves decides what the placer may do there; the placer only supplies the fence. | |
| -| K8 | moves §5.1, §6.1, §6.2, §9.4 | Relocation's install uses moves rev 7.6's replication baseline (snapshot plus level-0 anchor). A box releasing a host flushes all file mutations whatever the plan. The restore contract includes the files manifest and wake state (§5.6, §5.7). Every installation, a move's landing included, publishes a manifest in its new generation so unchanged files stay recoverable after the next failure. The archive at the cut stays. | |
| -| K9 | joint model | `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, a forged box id, a stale warm copy, a crash mid-install, late file uploads and late PUTs after termination. | |
| -| K10 | moves §7.1, §7.3 | A move into a multi-box region names its target **box** in the start CAS, chosen by `choose()`. Readiness, evidence, installation and recovery are bound to that box; replacing it is an explicit fenced transition (A1-10). | |
| -| K11 | claim C4, §8 | Reconcile's three row cases (§5.3): held participant rows, dropping a former executor's registry row without touching local state, and the 10-minute sweep as a stated exception to C4 for kept rows. | |
| +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, |
| +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) | |
| +| 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) | |
| +| 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 | |
| +| L10 | claim §6.1, §6.6 P6-D1, `internal/stopevidence` | A writers-stopped check for release step 1: cgroup empty, no member processes, and database holders limited to the agent's own identified replicator descriptors. `Collect` stays unchanged for step 4. | Requested | |
| +| L11 | claim §4 (CC11), `hostclaim.StartGuard` | A `park-generation` chore in the region does not block a `relocating` start there: relocation writes only its own new prepared generation, never one being retired. Under P6-D4 nearly every recently woken host has one, which would hold failover up to the park horizon. | Requested | |
| +| L12 | claim C4, §8 (CC10), §6.6 P6-D2; moves §9.6 | Reconcile's row cases for `relocating` (§5.3): held participant rows; a former executor's row kept held until its `park-local` retires it; the 10-minute sweep as a stated exception to C4 for kept rows (H9). | Requested | |
| +| L13 | claim C3, §6.2a, §6.6 P6-D3 | The files publisher is a second ordinary-replication exception, bound to `{location, generation, session}`. `files/<generation>/` belongs to that generation for the classifier; `park-generation` retires it except objects a live manifest names. | Requested | |
| +| L14 | moves §7.10 | A target terminated mid-move may be taken off the move by the termination fence, as M16's evidence, automatically, under the same before-commit rules. Moves decides what the move does then; the placer only supplies the fence. | Ruled (H10) | |
| +| L15 | moves §7.1, §7.3, §19.1 | A move into a multi-box region names its target **box** in the start CAS, chosen by `choose()`. Readiness, evidence, install and recovery bind to that box; replacing it is an explicit fenced transition (A1-10). | Ruled (H12) | |
| +| L16 | moves §5.1, §7.6, P6-D3's provider | Relocation's install reuses the landing's `building` and `published` phases and the prepared-generation authority, with a pinned set of remote versions as the source in place of a staged replica. One shared routine, so both get the same anchor and manifest rules. | Requested | |
| +| L17 | moves §6.1, §8, §9.4 | Every installation, a move's landing included, writes a files manifest in its new generation (§5.6), so unchanged files stay recoverable after the next failure; the archive at the cut stays. Timer freezing and draining apply to `relocating` holds. | Requested | |
| +| L18 | joint model, moves §14.2 | `internal/sim/hostlife` extends to two boxes per region: create spread, relocation by drain, termination mid-serve and in every relocation phase, nested failover, a stale edges file, an unenrolled reference, a volume without `DeleteOnTermination`, a crash mid-install, late file uploads and late PUTs after termination. | Requested | |
| + |
| +**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 |
| +L12. Three are dropped because the claim now satisfies them: |
| + |
| +- **K4** (claim CAS rights for placers): boxes already write claims |
| + (`AdmitWriter`, `PublishGeneration`, chores), and P6-D5 gives |
| + `region:<r>` work to any enrolled worker. L1 names the owner. |
| +- **K5** (adoption only while a region has one box): P5-D2 requires |
| + exactly one proven installation owner and refuses zero or several, |
| + which is the property K5 wanted, whatever the box count. |
| +- **K6** (box names bound by `control/boxes`): claim §2 rev 6.16 makes |
| + references opaque, and H11 makes the roster the binding (L7). |
| + |
| +The disposition tables (§13 to §17) still cite K numbers. They refer to |
| +rev 4.2's table; this mapping says where each now lives. |
| ## 10. Testing |
| -- **Unit:** box record verification (signature, account, region, |
| - `box id == instanceId`, legacy binding); `eligibleBoxes` (one box at a |
| - time, staleness, draining, `lost`, capability); `choose` (spread, |
| - ties); home-map stamp resolution and unstamped entries; HA3's two |
| - checks; the files manifest (immutable objects, tombstones, late |
| - uploads, snapshot boundary, `If-Match` races); timer catch-up; |
| +- **Unit:** enrollment evidence (signature, account, region, the tofu |
| + check for an existing reference, a reference held by another |
| + instance); `eligibleBoxes` (one box at a time, staleness, draining, |
| + roster state, `lost`, an owed `park-local`, capability, the expected |
| + region from the roster); `choose` (spread, fewest hosts, the SHA-256 |
| + tie-break); home-map stamp resolution; the files manifest (immutable |
| + 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, event, describe, activity, all three empty); the legacy bind |
| - (tofu id mismatch, label not in claims); 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 |
| + stopped, a volume without `DeleteOnTermination`, an empty mapping list, |
| + an event with no describe, all sources empty); 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`. |
| - **Relocation:** every row of the replacement table, the |
| - two-replacement bound, `probe-failed` without stop evidence, the |
| - source's rows through every phase, and relocate → write → replicate → |
| - terminate → cold restore with the 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). |
| + two-replacement bound, `probe-failed` without stop evidence, both |
| + participants' rows through every phase, the first probe opening `P` |
| + with `KeepStamp` and a restarted probe taking a fresh generation, and |
| + relocate → write → replicate → terminate → cold restore with the |
| + 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. |
| - **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 |
| - every phase with a crash injected at each; a stale local copy on the |
| - old box is not served after it becomes executor again. |
| -- **Joint model (K9)** decides readiness, as it does for the claim and |
| + every phase with a crash injected at each; the old box's local copy is |
| + never served after it becomes executor again (claim R6). |
| +- **Joint model (L18)** decides readiness, as it does for the claim and |
| moves. |
| -- **Rehearsal** (§8 step 4). |
| +- **Rehearsal** (§8 step 5). |
| ## 11. Open questions |
| -None. Rev 4.2's three were ruled as H7, H8 and H9 (2026-10-04). |
| +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.* |
| ## 12. Out of scope, for the later specs |
| - **Spec 2:** `headroom` thresholds, soft spread across an app's |
| instances, the `unplaced` state and its alert, rebalancing. |
| -- **Spec 3:** the placer loop: election, reading the termination queue, |
| - relocating every host off a terminated box in bounded parallel, waking |
| - always-on and scheduled instances, the failover gap target. |
| +- **Spec 3:** the placer loop: reading the termination queue, relocating |
| + 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, 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 (H5). |
| + join without SSM hand steps, enrollment of new boxes (§11 question 3), |
| + 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 |
| + (H5). |
| - **Not planned:** relocating unit- and socket-backed routes (the |
| console and platform services). Their HA is the HA ladder's, separately. |
| @@ -924,3 +1227,61 @@ Two limits to lift in plan 1b: a file over 64 MiB is recorded in the |
| manifest as skipped and is not published (the store takes a whole body in |
| memory), and the third termination-evidence source (Auto Scaling activity |
| history) is not built until spec 4 verifies it. |
| + |
| +## 19. What rev 5 means for plan 1a (2026-10-06) |
| + |
| +Plan 1a (aadb860) was built against rev 4.2. Rev 5 keeps most of it and |
| +changes how some of it is used. Plan 1b is written against rev 5. |
| + |
| +**Superseded.** |
| + |
| +- **`control/boxes/<id>.json` as authority (H11).** `boxid.Load` and |
| + `boxid.Verifier` are now used once, at enrollment, and their result is |
| + stored in the roster entry's `cloud`. `eligibleBoxes` takes its |
| + verified identities from the roster, not from loading records. The |
| + record object stays as the enrollment evidence, create-only, and grants |
| + nothing. |
| +- **The operator bind** (`Bind`, `control/boxes/<label>.bind.json`, `carlos ops |
| + box bind`, plan 1b item 13). Its tofu check moves into enrollment |
| + (§5.1). The bucket policy's bind statement is harmless and can go at |
| + the next apply. |
| +- **`WarmCopyTrusted` and the activator's warm path (H13).** Nothing skips |
| + a restore, so plan 1b item 4 is dropped. The `InstallMarker` type may |
| + serve as relocation's last local install journal entry, as moves' |
| + `.files-gen` does, or be removed; nothing reads it to trust a local |
| + database. |
| +- **`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). |
| + |
| +**Stays as built.** |
| + |
| +- `internal/boxid`'s record, signature check and embedded regional |
| + certificates (verified on the dev box), as enrollment evidence. |
| +- The edges file's `box_id` (the label, which is the reference under |
| + #212 option B), `capabilities`, `draining` and `headroom`. |
| +- The home map settling two claims by installation stamp, and reporting |
| + equal stamps. |
| +- `eligibleBoxes`' one-box-at-a-time predicate, with the roster as its |
| + source. |
| +- `internal/hostfiles`: the ordered manifest, immutable hashed objects, |
| + `SyncDir`, the continuous publisher, the watcher, restore and wake |
| + state. Plan 1b adds the generation binding, the copied manifest at |
| + each cold admission, and retirement by the claim (§5.6). |
| +- `registry.ReplaceTimers`. |
| +- The infrastructure: one termination queue per box, root volumes deleted |
| + on termination, the create-only `control/boxes/` policy. The fence |
| + prefix `control/box-fences/` needs the same create-only, never-deleted |
| + statements (§6). |
| + |
| +**Plan 1b's list, revised.** Items 1, 3, 5, 9 and 10 stand, read against |
| +rev 5 (item 10's expected region now comes from the roster). Item 2 |
| +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. |