# Region HA, spec 1: placing an instance on a box Design, 2026-10-06, **rev 5.4**. DRAFT. Plan 1a is built and merged (aadb860); nothing else here is built. **Rev 5.4** answers Astra's fourth review of rev 5 (`CODEX-FINDINGS-REGION-HA-REV5-4.md`, **B4-n**), which found no two-writer or data-loss path that depends on disk evidence. It removes the last runtime dependency on volume recording: the multi-box gate no longer checks it at box start, and recorder failure only alerts and keeps a dead box's chores open (B4-1). It also brings three summaries into line with H19 (B4-2). §23 maps both. **Rev 5.3** records Paul's ruling **H19** (2026-10-06), which supersedes H15 and the volume half of H10, and answers Astra's third review of rev 5 (`CODEX-FINDINGS-REGION-HA-REV5-3.md`, **B3-n**) in §22. Rounds 1 to 3 kept finding new ways a disk could outlive its box behind the volume guard. H19 takes the disk out of the failover path: a terminated instance can never run again, so the execution fence rests on the verified `terminated` read alone. Disk evidence decides only whether the dead box's `park-local` chores are discharged automatically; when it cannot be proven, they stay open for an operator, and recovery waits on nothing. The SCP, holds, the change role, the guard attestation and the service-role audit are removed. Most of round 3 is moot under H19; §22 says which, and why. **Rev 5.2** answers Astra's second review (`CODEX-FINDINGS-REGION-HA-REV5-2.md`, cited **B2-n**): four P1 and two P2, all accepted; §21 maps each, with the round 1 items it marked partly resolved. The volume guard now covers root-volume replacement, snapshots and images (B2-1), and Auto Scaling's own service-linked role, through the APIs that start its work (B2-3). A hold is closed by revoking the change role's sessions and waiting for in-flight disk tasks before the validating record (B2-2). The files manifest is pinned from the newest admitted generation, not from the database baseline's (B2-4). The local install receipt is bound to the installation stamp, and a box that has admitted a writer never reinstalls (B2-5). H17's confirmer may treat an enrolled box as gone on a positive `terminated` read (B2-6). **Rev 5.1** answers Astra's first review of rev 5 (`CODEX-FINDINGS-REGION-HA-REV5-1.md`, cited **B1-n**): five P1, three P2 and one P3, all accepted; §20 maps each. A restarted probe now restores from its real predecessor, and `released` coverage is bound to one session (B1-1). A replacement target must make its own local install before probing (B1-2). An operator's volume change first suspends automatic disk evidence, and a volume that leaves a running box keeps it suspended until accounted for (B1-3). The volume guard protects its own tag, needs an attested Organizations policy, and without one there is no automatic fence (B1-4). A lost or unreadable execution-lease state keeps updates out (B1-5). A source lost in `starting` turns the drain into a failover (B1-6). A console bound to a fenced box leaves the census (B1-7). Code citations are refreshed (B1-9). The two points this raised for Paul were ruled the same day: an enrolled box in another region confirms the first box of an emptied region (H17), and a box-started relocation accepts a console's newest report when its box's update guard is armed (H18). §11 is empty again. **Rev 5** restates the design against the host lifecycle claim as it now stands, rev 6.25 (413b12cb on `design-replica-ownership`), with its library on main (`internal/hostclaim`, `internal/hostguard`, `internal/stopevidence`, `internal/park`, `internal/genselect`), and records Paul's rulings H10 to H18 of 2026-10-06. Rev 4.2 was written against claim rev 6.3 and asked for changes K1 to K11. Those sessions never saw the request, and the claim moved on: box references are opaque, `control/host-actors.json` is the one roster, every writer is 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). A dev test showed a terminated instance's describe lists no volumes, so that proof comes from a record taken while the box runs, kept true by IAM (H15). A relocation is started without a console: the boxes, not a roster reservation, keep it apart from executable updates (H14, §5.10). §9's K-table is replaced by requests L1 to L20 against claim rev 6.25 and moves rev 7.17. §19 says what of plan 1a is superseded. The three points rev 5 first left open were ruled the same day as H14 to H16 (§11). 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. 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: 1. **Box placement** (this spec). With several boxes in a region, the host lifecycle claim names the one box that runs each instance, and every box, edge and activator follows the claim. 2. **Placement policy.** Which eligible box a new or displaced instance goes to. 3. **Failover.** A dead box's instances are re-placed onto the region's survivors. 4. **Autoscaling.** A region's boxes are an Auto Scaling group that grows on demand and shrinks by draining. It builds on two specs still in review, and asks them for changes (§9): - 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 enrolled boxes are alive, and on #212 option B for box references. ## 0. Rulings (Paul, 2026-10-04 and 2026-10-06) | # | Ruling | |---|---| | H1 | **The proof that a box is dead is that AWS terminated it.** Each region's boxes run in an Auto Scaling group with health checks. When the group terminates an unhealthy box, a region placer that has only read-only AWS rights sees `terminated` and re-places the box's instances. The console still holds no EC2 rights. This replaces M16 / claim §7.2's operator-only declare-lost **for terminated boxes only**; a `stopped` box stays manual. It also replaces fleets D7's "no automatic reaper" for platform boxes. Lease expiry is still never proof (CC5). | | H2 | **Shape the claim now.** The HA specs cite the claim rather than invent a second primitive, and send the claim and moves sessions the exact changes they need (§9) before those specs are finalised on a one-box-per-region assumption. | | H3 | **About one second of data loss, written down.** Litestream keeps shipping asynchronously. Writes that had not reached S3 when a box died are lost, and the docs and console say so. | | H4 | **Placement policy: capacity plus soft spread.** Among eligible boxes, choose the one with the most headroom. Prefer a box that runs no other instance of the same app, but never refuse placement for that reason. If no box is eligible, the instance waits as `unplaced` and an operator is alerted. (Spec 2.) | | H5 | **Each region's minimum is configurable: 1 by default, 2 where HA is sold.** Scale-out is automatic on low headroom. Scale-in is automatic too, but only after the box has been drained into the region's other boxes. (Spec 4.) | | H6 | **File durability follows the paid plan.** Continuous sync on the top plan, periodic snapshots on the bottom one. The platform exposes this as a per-app setting (§5.6) and Carloku maps its plans to it. Platform-managed files (`instance.key`, `report.token`, `.env`) sync continuously on every plan. | | 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/.json` authority. `internal/boxid`'s AWS-signed IMDS identity verification becomes the evidence required to enroll a box. Enrollment records the proven account, region and instance id in the roster entry's `cloud` field, and the termination fence binds to that entry. Box references are opaque (claim §2, rev 6.16) and follow #212 option B: the label is the key, the instance id is private. | | H12 | **(2026-10-06) Executor choice at create** is spec 1's `choose()`: prefer a box running no instance of the app; then the most headroom (until spec 2, the fewest claimed hosts); then the claim's P5-D2 SHA-256 of `host + "\x00" + box reference` as the final tie-break. It is recorded once, in the create intent. Recovery never substitutes. | | H13 | **(2026-10-06) Claim ruling R6 supersedes HA3 and §5.5.** A box never reuses its local database. Every admission is cold until claim P6-D4 lifts. HA3 and §5.5 are deleted, and the activator half of plan 1a's install marker is not used. | | H14 | **(2026-10-06) Relocation starts need no console reservation (L6).** A relocation start requires that no executable update is reserved for `from` or `to` in `control/host-actors.json`, which the worker reads and never writes. Root on each box refuses to start an executable update while that box is a participant in a running claim operation. The update side's refusal is what closes the race with a reservation made after the start's read. (§5.10.) | | H15 | **(2026-10-06) H10's volume check rests on a running-time record, not the terminated read.** Tested on dev 2026-10-06: while `shutting-down`, `DescribeInstances` still listed both volumes of a test instance with their `DeleteOnTermination` flags; once `terminated`, `BlockDeviceMappings` was empty, the `true` root volume was already gone (`InvalidVolume.NotFound`) and the `false` volume survived as `available`. So the fence rests on (1) a record of the box's block device mappings taken by regional workers while it runs, refreshed on change, kept with its roster-bound evidence, showing every attached EBS volume `DeleteOnTermination: true`; (2) IAM denying `ec2:ModifyInstanceAttribute` and `ec2:AttachVolume` on platform boxes to every principal except operator roles, so the record cannot go stale behind the platform's back; (3) the terminated read (describe, event, later the group's history). A `shutting-down` read that still lists mappings may refresh the record but is never itself evidence. A missing record, one older than the stated bound, or one with any `false` volume sends the box to the operator path. (§5.9, §6.) The controller added `ec2:DetachVolume` to the deny in (2), as within the ruling's intent. | | H16 | **(2026-10-06) Auto Scaling boxes are enrolled automatically, with evidence (spec 4, L19).** The console enrolls an Auto Scaling box itself when its `boxid` evidence verifies (the deployment's account, the region's AWS region) and a regional worker confirms, with read-only Auto Scaling rights, that the instance is a current member of that region's group. Anything else still needs an operator's approval. | | H17 | **(2026-10-06) The first box of an emptied region is confirmed from another region.** Any enrolled box in another region holds cross-region read-only Auto Scaling and EC2 describe rights and may confirm a new box's group membership (H16) for a region that has no enrolled box. That is its only cross-region use. One-box regions therefore recover automatically. (§5.1, §6, L19.) | | H18 | **(2026-10-06) A stale console report does not hold up a box-started relocation.** For box-started relocations only, the census accepts a console's newest report however old, provided that report met the protocol floor and the console's box has the claim's D1 root update guard armed, so it cannot be swapped for an older binary underneath. Everything else in claim D7 is unchanged. (§5.9, L20.) | | H19 | **(2026-10-06) The failover fence rests on the `terminated` read alone; disk evidence only decides discharge of local chores.** Supersedes H15 and the volume half of H10; H10's automatic failover stands. The execution fence is a verified `terminated` read, bound to the roster's `cloud` identity, from the event or a describe (later the group's history); absence is never evidence. This is the claim's own lost-box rule for execution (§7.2), which needs no volume condition: a terminated instance can never run again, a surviving disk cannot write to storage by itself, and a disk attached to another instance is a different box with a different enrollment, never admitted as the old executor. The disk question belongs only to claim D5's destroyed-local exception: whether the dead box's `park-local` chores can be discharged automatically. That needs the volume evidence (the box's launch-time mappings all `DeleteOnTermination`, recorded while running); if it cannot be proven, the chores stay open for an operator (claim D2 and D5) and nothing about recovery waits on them. A surviving copy of a disk is a data-retention and cleanup concern for the operator path, not a two-writer risk. Tofu keeps `delete_on_termination = true`. (§5.9, §6, L2, L3.) | H10 to H19 supersede only what they name: H10 adds the volume condition to H1 and H15 says where it is read from, H11 replaces §5.1's box records as authority, H13 replaces HA3 and §5.5, H14 replaces claim D7's console reservation for relocation starts, H16 and H17 settle enrollment for spec 4, H18 narrows claim D7's console census for box-started relocations, and H19 supersedes H15 and the volume half of H10 (the fence needs no disk evidence; only automatic discharge of local chores does). Everything else in H1 to H9 stands. Standing rulings this spec keeps: - One writer: a home-run instance runs on exactly one box (claim C4, multi-region ingress, sidecar members). - 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 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 Today a region is one box. Placement is per region: a bucket record has `Region` and `Pool` and no box (`internal/provision/provision.go:49`). Every box whose `CARLOS_REGION` matches mints the route (`inScope`, `internal/provision/reconcile.go:348`, called at `:820`). Nothing enforces "exactly one box": `reconcile.go:192` states it as intent only. A second box in a region would break three things: 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 broke the tie by sorted box name, with no liveness (`foldHomes`, `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:1164-1168`). With two boxes taking turns, that is false. Claim R6 removes the warm cache altogether (H13). And when a box dies, its instances stay down. EC2 auto-recover brings back the same machine, if it can (`host_auto_recover`, `infra/modules/region-host/main.tf:521`). ## 2. Words - **Box**: one platform host machine. Not a customer fleet box; fleets keep their own mechanism and are out of scope. - **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 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. ## 3. Invariants **HA1. The claim names the executor.** A relocatable host runs only on the box its claim's `op.exec` names. This is claim C4 unchanged. What changes is that `op.exec` may now name any eligible box in the record's region, not "the region's box". **HA2. Region equality never admits.** The activator, config sync, release adoption and timers act for a host only on its executor, or on a 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. 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`. Stamps only increase (claim `gen`), so a dead box's stale file always loses to its successor's, with no liveness rule. **HA5. Everything a relocatable host needs to start is in S3.** The database, files directory, env files and timer state are under the incarnation's `holder.location` in the current generation, or are rendered from the record (config, release). Nothing needed to start it 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 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 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). No disk condition applies to the fence (H19): disk evidence decides only whether the box's local chores are discharged automatically (§5.9). ## 4. What stays the same - A region with one box behaves exactly as today, and every new rule holds trivially there. - Static sites and public addr routes still run on every box (`everywhereClass`, `reconcile.go:215`). Only relocatable hosts gain an executor that can change; unit- and socket-backed routes keep theirs. - Customer fleets keep their binding stamps (`internal/host/fleetbind.go`) and per-request fallback (`fleetChannelFor`, `internal/edge/edge.go:2466`). - The ingress model: any edge serves any app and backhauls home-run hosts to their box (multi-region ingress). This spec changes which box is "home", not how backhaul works. - Latency steering and ingress for boxes that come and go are spec 4. ## 5. Design ### 5.1 Box identity, the roster and evidence **Rev 5 (H11).** Spec 1's own `control/boxes/.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**. **Enrollment.** A box asks to be enrolled by publishing its identity evidence, the record plan 1a defined: control/boxes/.json ```json { "v": 1, "box": "", "identity_document": "", "identity_signature": "", "written_at": "" } ``` 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. **Auto Scaling boxes (H16, spec 4).** The console enrolls a box launched by the region's Auto Scaling group itself, with no operator, when two pieces of evidence agree: its `boxid` record verifies with the deployment's account and the region's AWS region, and a regional worker has written a create-only membership confirmation, `control/box-enrollment//.json`, from a fresh read-only `autoscaling:DescribeAutoScalingInstances` showing the instance a current member (`Pending` or `InService`) of that region's group, with the group name from the deployment's configuration. Anything else, a fixed box included, is enrolled only with an operator's approval. Spec 4 builds this; the claim's D7 needs to allow it (L19). **A region with no enrolled box (H17).** When the target region has no **live** enrolled box, the confirmer may be any `active` enrolled box of another region, acting as a regional worker of its own region and checking its own entry first. This is the only thing it ever does across regions. Its confirmation binds to the target region's group, not to anything the new box says: - it reads the target region's group name and ARN from the roster's `regions` entry for that placement (claim P5-D2's extension), never from the new box or an edges file; - it calls `DescribeAutoScalingInstances` for the instance id in the target region's AWS region, and requires the reply to name exactly that group, lifecycle state `Pending` or `InService`, and an availability zone in that AWS region; then `DescribeInstances` there, requiring the instance `pending` or `running` with the deployment's `OwnerId`; - **the region is empty (B2-6).** The roster entry of a dead box stays `active` until a fence retires it, and only a regional worker can write the fence, so the roster alone would never show the region empty. The confirmer therefore describes, in the same region and the same pass, every other enrollment the roster lists there as `active` or `quarantined`, and requires each to read **`terminated`**, positively, for its roster `cloud`. `InvalidInstanceID.NotFound`, any other state, an error or a partial reply refuses the confirmation (absence is never evidence; a box that has left `DescribeInstances` goes to an operator). The confirmation lists those reads (`terminated_enrollments: [{box, enrollment, instance_id, observed_at, request_id}]`). They only show the region has no live worker. They are not a termination fence, they discharge nothing, and they never retire a roster entry; - it writes the same create-only object, `control/box-enrollment//.json`, with `{target_placement, aws_region, group_arn, instance_id, lifecycle_state, observed_at, request_ids, confirmer: {box, enrollment, region}}`. Two confirmers race by the same conditional write: one creates it, the other gets a refusal, reads it, and stops. The console accepts a cross-region confirmation only if, at enrollment, every enrollment the roster lists as `active` or `quarantined` in the target region appears in the confirmation's `terminated_enrollments` (any new one refuses), the confirmer was `active`, the group ARN equals the roster's for that placement, and the `boxid` record's region equals `aws_region`. Once enrolled, the new box is the region's worker: it writes its own volume records, fences its predecessor through the ordinary §5.9 path (its own terminated read), and recovers the hosts (§5.8). So a one-box region recovers automatically (§7). A box whose entry is not `active` with a proven `cloud` is never eligible, and a claim naming one is never relocated automatically: an operator resolves it. **Edges file fields.** Each box's edges file (`internal/host/edgesfile.go`) carries, as plan 1a built: ```json { "box_id": "", "capabilities": ["region-ha-1"], "draining": false, "headroom": { "mem_free_mib": 2210, "disk_free_mib": 31200, "awake": 14 } } ``` - `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. `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'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. - The choice is recorded only in the claim. The record keeps `Region` 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 (L15). ### 5.3 Reconcile: executing rows, held rows, former rows 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` | | `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 (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 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`) 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}}`. 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 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: withdrawn (H13) 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:1164-1168` is replaced by a reference to claim R6, not to HA3. Plan 1a's `activator.WarmCopyTrusted` is not used, and nothing reads the install marker to skip a restore (§19). A1-5's concern, that authority is 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 Moves carry the files directory (F4) and `.env` (F6) as a sealed archive taken from the live source (moves §6.1, §8). A dead source can't produce one, so HA5 needs them in S3 already. **The setting.** An app's manifest gains `files_durability`: - `continuous`: a changed file is published within about one second of its **first** unpublished modification, whether or not the app has closed it (A2-5): - **Watches.** inotify `IN_MODIFY`, `IN_CLOSE_WRITE`, `IN_MOVED_*`, `IN_CREATE` and `IN_DELETE` on every directory of the tree, added recursively as directories appear. - **Deadline.** The first modification of a file arms a one-second deadline. Later writes do not push it back. A file still being written is published at the deadline, then again at the next one. - **Overflow.** `IN_Q_OVERFLOW`, or any watch that can't be added, triggers an immediate full scan, comparing size, mtime and inode with the last published state. - **A consistent image.** The uploader reads the file, then checks that size, mtime and inode are unchanged. If they changed, it retries within the deadline. A file that never holds still for a read is still published **at every deadline**, as the last image read, and flagged as possibly torn. It never waits for a scan (A2-5 residual). - **Missing coverage.** While any directory has no working watch (overflow, a watch that can't be added, the watch limit reached), the publisher **polls** that subtree once a second, comparing size, mtime and inode, until the watch is restored. Polling is reported as a box metric, and alerts if it lasts an hour. The files directory is not a database: apps that update a file in place must expect a torn image after a failover, and the docs say so. The instance database is Litestream's. - **Repair.** A full scan every 10 minutes catches anything a watch missed. It is repair, never the path a change waits on; - `snapshot`: the whole directory is published every `files_snapshot_interval`, default 15 minutes. Carloku maps its plans to this (H6). Apps with no setting get `snapshot` (H8). **Always continuous, whatever the setting:** `instance.key`, `report.token`, `.env`, `-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). **Ordering (A1-4).** Object versions do not say which update wins, so 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, `/files//objects/-`, written create-only. A stalled upload that completes late creates an object no manifest names. - **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 per generation, `/files//manifest.json`, replaced only 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 `/files//`, 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//manifest.json` create-only, as a copy of the **files pin**: the newest manifest in the admitted chain, read by exact version (B2-4). That is the manifest of `holder.generation` as observed, or, if that generation has none (its copy never completed, so its app never started), of the nearest predecessor in `holder.admissions` that has one. It is chosen independently of the database baseline: the files publisher and the replicator make progress separately, so a generation can hold published files before its first database upload. Its entries keep naming the predecessor's objects where they are, so an unchanged file is never uploaded again. A late write from the predecessor's publisher lands in the predecessor's prefix, which nothing admitted reads again. - **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//` 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 **files live set** is every manifest from the files pin through `holder.generation`, plus any manifest a running operation has journaled in its pin, and every object they name. A park that runs while an operation is in progress keeps all of them. The at-rest sweep treats `files/` as part of the location, never as residue to classify blindly (claim P6-D3). 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 (L17). ### 5.7 What a new executor rebuilds | State | How the new box gets it | |---|---| | 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) | | `.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, 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: - its timer rows (active rows and their bookkeeping, moves §9.4's canonical digest), on a registration, a delivery or a rearm; - the route's `NextDue`, the app's own next wake (`activator.go:2204`), whenever the activator sets it; - the route's `Replication` mode. The new executor sets `NextDue` and `Replication` from it, as a move's 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`. 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 imported `next_at`, not from `Next(now)`. - A delivery that ran on the dead box but whose bookkeeping did not reach S3 runs again. Ticks are documented as **at-least-once** (H7). ### 5.8 Relocation 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?, directory_revision} `reason` is `drain`, `rebalance` or `failover`. For failover, `fence` names the termination fence record (§5.9) by key and SHA-256. The start is refused by the claim's start guard (claim §4, CC11, as amended by L11), when `to` is not eligible for the host (§2), and when the roster shows an executable update reserved for `from` or `to` (§5.10, H14). `directory_revision` is the roster revision that check read. No console reservation is taken. Participants are `from` and `to`, or `to` alone for a failover. **Who acts.** Every phase is a claim CAS conditional on `op.id`, the phase and the ETag. The recovery owner for every phase is the region's 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, or once a source-loss CAS (below) has removed `from` | `from`, or `none` after a source-loss CAS | `stamp_from` | `from` ready; `to` held | `from`, as for `serving` | | `releasing` | `from` runs the **release sequence** (below) and publishes its stop receipt; for failover the fence is already in the intent and this phase is skipped | `from` until evidence | unchanged | `from` ready until its admission fence closes, then held; `to` held | `from`, until its admission fence closes | | `pinning` | a worker CAS citing the receipt or the fence: `op.exec: none`, a non-installing transition that keeps the stamp (claim R6-4, D5's form). Then it selects and journals the **pinned recovery set** (below) | `none` | unchanged | `from` held (if alive); `to` held | nobody | | `installing` | a worker CAS that journals the pin and a fresh prepared-generation id `P`, hands `op.exec` to `to`, and writes `holder.stamp` = this CAS's `gen` (R6-4: a new installation), adding `to` to `touched.boxes`. `to` activates that stamp under the host guard (claim §6.4), writes its inventory entry, **builds `P`** and makes its **local install** (below) | `to` | `S'` | `to` held; `from` held | nobody: `to` writes local state under the guard, starts no app and admits no writer | | `installed` | a worker CAS once `P`'s install manifest is complete and verified, journaling `P`'s prepared authority (claim P6-D3). The executor then journals its **local install receipt** by CAS, if this CAS did not already carry it (a replacement makes its own, below) | `to` | `S'` | as `installing` | nobody: the executor may make its local install, nothing else | | `probing` | `to` enters it by CAS, which requires a local install receipt for exactly `op.exec`, its enrollment and `op.journal.install_stamp`; then each probe attempt is one cold `AdmitWriter` (below), then the probe (moves §7.7, same region), within the probe deadline | `to` | `S'`, kept by the first admission | as `installing` | `to`, writer, probe only | | `probe-failed` | `to` runs the release sequence for its own session | `to` until evidence | unchanged | as `installing` | nobody | | `serving` | a worker CAS back to `serving` with `participants: [to]`; `from` gets a `park-local` chore unless it is discharged under H10 (§5.9) | `to` | `S'` | `to` ready; `from` held until its chore retires the row | `to` | **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. 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 process tree and wait for it to be empty: the per-host cgroup's `populated 0` and no member processes. The database, WAL and SHM files may still be held, but **only** by the box's own replicator for 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. `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 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 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. The session ends uncertified, as every session does under P6-D4; coverage (below) is what keeps its writes. The journal entry is `{"released_by": "", "generation": "", "session": S, "final_txid": N, "manifest_seq": M, "receipt": "", "receipt_sha256": "…"}`, and `pinning` refuses to pin less than it. **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, chosen separately, the exact version of the **files pin** (§5.6: the newest manifest in the admitted chain, not the database baseline's generation), with files and timers included. The two can come from different generations; each is the newest durable state of its own publisher (B2-4). - **After a release sequence** (drain, rebalance, probe failure): the set must reach the journaled `final_txid` and `manifest_seq`. If the listing has not caught up, `pinning` waits; it never pins less than what the releasing box flushed. - **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. That is the **remote build**: immutable, built once, and complete when a fresh read verifies all three objects. `installed` records it. `generation.json` is not written here: the probe's admission publishes it (moves §7.14). **The local install (B1-2)** is separate, because it belongs to one box. The box that is `op.exec`, under the host guard with the stamp it activated: - applies the files and env from `P`'s files manifest to the local directory, `ReplaceTimers` the wake state, and sets `NextDue` and `Replication`; - runs `RenderHeld` and `MaterializeHeld` with current inputs, recorded as the relocation's inputs (P6-D3); - journals each step locally, and then, last, records its **local install receipt** in the op journal by CAS: `local_install: {box, enrollment, install_stamp, files_manifest_version, journal_sha256}`. **`install_stamp`** is the stamp of the CAS that handed this box `op.exec` (`installing`, or a replacement's), journaled by that CAS as `op.journal.install_stamp`. It is the installation's provenance, not the current writer's stamp: later probe admissions take new stamps (§6.4a item 4) and leave it alone (B2-5). A receipt counts only when its box, enrollment and `install_stamp` equal `op.exec`, its enrollment and `op.journal.install_stamp`, so a replacement executor never inherits its predecessor's. Remaking the local install before the first admission is not a reinstall: `P` is not touched. **After the first admission, the local install is never remade (B2-5).** Once any admission entry names `P` (or a later generation of this op), the box's local files, env and wake state are the live state of that writer lineage. A new agent on the same box stops the app and admits a new session, as for any cold wake; it never reapplies `P`'s files or timers. A box that finds its receipt missing after that point has lost local state it cannot rebuild from `P`: the op goes to `stuck`, and the operator resolves it (or a fence makes it a nested failover from `holder.generation` and the files pin). **The probe's admission.** Each probe attempt is one `AdmitWriter` (claim §6.4a), made by `to` as `op.exec`, bound to the observed `op.id` and phase `probing`: - **mode** cold, always (P6-D4, H13); - **generation and baseline (B1-1):** the first attempt opens `P`, which no admission has named (P6-D3's opened-once evidence), and restores it from its pinned snapshot and anchor (`genselect.SelectPrepared`). Every later attempt is cold into a fresh generation whose baseline is chosen as for any cold admission: `genselect.Select` from the predecessor, `holder.generation` as observed, through the unfinished run (claim §6.4a item 3; moves §7.14's restore row). So attempt three restores attempt two's generation with everything it replicated, not `P`. Prepared authority is used once; - **`KeepStamp`** on the first attempt, because no writer has been admitted since the `installing` CAS issued `S'` (`holder.stamp > holder.session`). Later attempts take a new stamp; - **coverage, per admission (B1-1):** decided for the session the admission's predecessor actually is, the last entry of `holder.admissions`, never for the operation as a whole: - `released` (L9) only on the admission that opens `P`, and only when that predecessor is exactly the `{box, session}` whose release receipt this op journaled and whose `final_txid` the pin reached. That is a drain, a rebalance, or the nested relocation after a `probe-failed`. Until L9 is accepted, relocation by drain is not enabled (§8), because coverage `""` would declare a false loss on every drain; - `""` everywhere else: a failover (the admission records `writes_lost` for `from`'s last session, `remote_max_txid` the pin's `N`, H3's written-down loss), and every later probe attempt, whose predecessor is the previous attempt's uncertified session. `to` raises one alert per declaration; - then, as for every cold admission: purge, restore the chosen baseline, start, readiness, `generation.json`, then `PublishGeneration`, which queues `park-generation` for the dead generations of this region in the chain (`generation_from` at the first publication; an earlier attempt's generation at a later one) (claim §6.4a item 5). A queued park never touches a generation a later attempt still needs: the baseline is always the newest generation, protected as the unfinished run until its successor publishes (claim §6.2a); - **limits:** at most three attempts within the probe deadline, as a landing's (claim §6.4a item 7). A probe never marks the host failed; running out of attempts is `probe-failed`. **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`). 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 builds `P` again: replay from `installed` or `probing` goes forward (the local install only if the executor has no receipt and no admission has named `P`; then the probe, then `serving`), never back to `installing`; - `P` is opened at most once. After its first admission, every restart takes a fresh generation from its predecessor; - a worker or `to` that paused and resumes revalidates the phase under the host guard, with the stamp it captured, and stops. 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 `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 (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` | `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 (no admission entry names `P`) | `to`'s termination fence | `installed`, with `op.exec: to'`, a new stamp, and no local install receipt. `to'` activates the stamp, makes its own local install from `P`'s files manifest and records its receipt (B1-2), then enters `probing`. `P` was never opened, so `to'` opens it | | terminated after its first `AdmitWriter` | `to`'s termination fence | a nested failover from `pinning`, pinning from `holder.generation` as observed (`P` or a later fresh generation, with `to`'s replicated writes). Coverage `""` declares `to`'s sessions | | alive, but its probe fails or misses the **probe deadline** (10 minutes) | `to`'s release sequence, in `probe-failed` | a nested relocation from `pinning`, pinned to at least `to`'s journaled `final_txid` and `manifest_seq`, so writes made during the probe are kept. `to` is excluded from the choice for this host | **Losing the source (B1-6).** A drain or rebalance whose `from` is terminated before its stop receipt becomes a failover, in one CAS conditional on `op.id` and the phase, citing `from`'s fence: | `from` terminated | The CAS | The op resumes at | |---|---|---| | in `starting`, acknowledged or not | journals `failover_fence` (key, SHA-256) and `reason: failover`, keeping the intent and every acknowledgement; removes `from` from `participants` and from the barrier; sets `op.exec: none`, keeping the stamp (claim D5's non-installing form); adds `from` to `lost`, and discharges its `park-local` chores only if its volume records qualify, otherwise leaves them open for an operator (§5.9, H19) | `starting`, waiting only for `to`'s acknowledgement; the next CAS goes to `pinning` with the fence as its evidence, skipping `releasing` | | in `releasing`, before its receipt | the same | `pinning`, with the fence as evidence | | after its receipt (`pinning` on) | `from` only goes on `lost`, and its chores are discharged if its volume records qualify, otherwise left open; nothing else changes | the same phase | The pin for a converted op follows the failover rule (fence plus 30 seconds), and the first admission's coverage is `""`. - **The bound.** After two replacements of `to` in one op, the placer stops at the current phase's safe point (never between `installed` and a probe) and marks the op `stuck`. It alerts, and the op waits for `carlos ops host resolve `. The host stays down, and the console 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. **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, 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 **What counts (A1-1, A1-11, H10, H19).** A box is fenced by termination when a regional worker, with its own read-only rights in the box's AWS region, observes state exactly **`terminated`** for the instance id, account (`OwnerId`) and region in the box's roster entry's `cloud` (H11, HA7), by one of the three sources below. Nothing else is needed (H19). This is claim §7.2's rule for execution, that the instance is fenced by the cloud, without the operator: a terminated instance can never run again; a disk that survives it cannot write to storage by itself; and a disk attached to another instance is a different box, with a different instance id and enrollment, never admitted as this box's executor (claim C4, HA7). **Disk evidence, for discharging local chores only (H19, claim D5).** Whether the dead box's `park-local` chores can be discharged without retirement is a separate question, about cleanup, not about who may write. A worker discharges them automatically, in the fence CAS, only when the box's **volume records** (below) show its block device mappings, from the first record taken at enrollment (the launch-time mappings) to the last taken while it ran, with every attached EBS volume `DeleteOnTermination: true` and no volume ever removed. Otherwise the chores stay open for an operator's destroyed-local declaration or the returning-box retirement (claim D2, D5). Nothing about recovery waits on them: the fence, the relocation and the census do not read volume records (§5.8, L5). This is not proof that no copy of the disk exists. A volume kept by a Recycle Bin rule, copied, snapshotted or imaged, or detached by an operator, can survive. That is a data-retention concern, handled by the operator path and the deployment's own retention settings, never a second writer: no such disk can act as the executor (above). The dev test of 2026-10-06 (§8 step 5) showed why the evidence must be recorded while the box runs: once `terminated`, `BlockDeviceMappings` was empty, the `DeleteOnTermination: true` root volume was already gone (`InvalidVolume.NotFound`), and the `false` volume survived as `available`. **The volume record.** Regional workers describe each enrolled box in their region while it runs: at enrollment, on every 10-minute sweep, and at once when a describe shows `shutting-down`. A worker writes a new record, create-only, whenever the mapping differs from the newest record, and otherwise at least once an hour: control/box-volumes//.json ```json {"v": 1, "box": "", "enrollment": "", "cloud": {"provider": "aws", "account": "123…", "region": "eu-west-1", "instance_id": "i-0abc…"}, "instance_state": "running", "block_devices": [{"device": "/dev/xvda", "volume_id": "vol-…", "delete_on_termination": true, "status": "attached"}], "removed_volumes": [], "observed_at": "", "request_id": "", "written_by": {"box": "", "enrollment": ""}} ``` - A record is bound to the roster entry: its `cloud` must equal the entry's, and a record for another instance is ignored. - `removed_volumes` lists any volume the previous record had and this one lacks (a detach, or a replaced root volume). Any removal, or any `false` flag in any record, rules out automatic discharge for that enrollment for good, and alerts once so an operator knows. - A `shutting-down` read may add a record; it is never termination evidence. **What never counts.** - `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. A volume record is a cloud read, not such a report: any regional worker may write one, the described box included, under the claim's trusted box-writer boundary (P5-D3). It decides only cleanup (above), so a wrong one can leave a disk unretired, never admit a writer. **The fence record.** The worker writes one record per terminated enrollment, create-only (L4): control/box-fences/.json ```json {"v": 1, "box": "", "enrollment": "", "cloud": {"provider": "aws", "account": "123…", "region": "eu-west-1", "instance_id": "i-0abc…"}, "state": "terminated", "observed_at": "", "via": "describe" | "event" | "activity", "request_id": "", "event_id": "", "written_by": {"box": "", "enrollment": ""}} ``` 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 ways to observe `terminated`.** Any of these is the terminated read: 1. **The durable event.** An EventBridge rule sends EC2 "Instance State-change Notification" events with `state: terminated` for the deployment's account to an SQS queue (14-day retention). Plan 1a built one queue per box. The queue's policy accepts messages only from that rule's ARN. An event whose account, region and instance id match a roster entry's `cloud` is the read, `via: "event"`. 2. **A direct read.** `DescribeInstances` for the instance id, in the region, returning `terminated` with the deployment's `OwnerId`, `via: "describe"`. Workers make it on their sweep and whenever an event or the group's history suggests a termination. 3. **The group's own history.** For a box launched by an Auto Scaling group, `DescribeScalingActivities` for the region's group: an activity terminating that instance id with status `Successful`, `via: "activity"`. Spec 4 verifies on dev that `Successful` is recorded only once the instance has reached `terminated`; until then this source is off. **What is not guaranteed (A2-4).** EC2 delivers state-change events to EventBridge on a best-effort basis, and a terminated instance leaves `DescribeInstances` after about an hour. When no source shows `terminated`, 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, if the disk evidence allows (H19).** When the volume records qualify (above), its `park-local` chores are discharged in the same CAS, by `CompleteObligation` semantics, without retirement: claim D5's destroyed-local exception (L3). The fence CAS cites the records it relied on. When they do not qualify, the chores stay open for an operator, and the relocation proceeds regardless: a dead box's `park-local` names only that box, which no relocation writes (claim CC11). Regional chores are reassigned to `region:`, 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. - **A console that ran on the box leaves the census too (B1-7).** Claim D7 requires a fresh report from every console able to mutate the namespace. A console enrollment gains `compute: {box, enrollment}`, the platform box its process runs on, set at console enrollment and checked against every console report, which that box's trusted writer publishes with its own `boot_id`. A console whose `compute` box has a valid fence record is excluded from the census exactly as the box is (L5). A console with no `compute` binding is never excluded this way. - **A stale console report (H18).** For a relocation a box starts, and nothing else, the census accepts a console's **newest** report however old, when that report met every D7 floor check (protocol minimum, authenticated release minimum, matching floor digest) and the console's `compute` box has reported `floor_guard_ready` with the same floor digest. Claim D1 makes an armed guard permanent (it never expires and cannot be lowered offline), so that box cannot run an older console binary underneath. A console with no `compute` binding, or whose box never reported the guard armed, still needs a fresh report. Every other D7 rule, and every console-started operation, is unchanged (L20). - **The loss is recorded twice.** The admission that takes over records `writes_lost` (§5.8), and the console copies the fence into claim D4's durable loss record when it next runs, with timer knowledge `partial`: wake state was published continuously, up to H3's window. ### 5.10 Relocation starts and executable updates (H14) Claim D7 serializes a lifecycle start against executable updates with a reservation the console writes into the roster. A relocation must start when the console is down, so H14 moves the serialization to the boxes. Each side records its own intent durably first, then checks the other's, so of two that race at least one sees the other. **The worker, at the start.** Before the start CAS, the worker reads `control/host-actors.json` as an exact object and verifies its root signature (an unreadable or unverifiable roster refuses the start). It requires `to`, and `from` unless the start cites a fence, to be `active`, and requires that no entry in `activations` names `from`'s or `to`'s enrollment. It records the revision it read as `directory_revision` in the intent. It writes nothing to the roster. **A participant, before it acknowledges.** A box becomes a participant in practice when it acknowledges the operation (claim D6). Before its first execution-lease PUT, its controller: 1. writes its `.hostexec/.json` state as `pending`, durably (claim D6's existing state and write protocol); 2. then reads root's update state: the system-update journal and root's **update-begun** marker (below). If an update is begun or in progress for this box, it refuses to acknowledge, clears its `pending` state, and retries after the update finishes. The operation cannot leave `starting` without `to`'s acknowledgement, so nothing has moved; the worker waits, or replaces `to` (§5.8). **Root, before it starts an update.** Every path that begins an executable change (system apply, explicit rollback, a guarded activation under claim D1, the console's activation reservation being acted on), under root's existing system-update lock: 1. writes an **update-begun** marker, durably, beside the update journal (`/opt/carlos/system/guard/update-begun.json`, naming the update); 2. then scans `/.hostexec/` completely. **Any** controller record there, in any state (`pending`, `active` or `lost`), and any record root cannot read or parse, or a directory it cannot list, means the box may still be a participant: root removes its marker, refuses the update, and leaves the console's activation reservation held, to retry later (B1-5); 3. otherwise it proceeds. The marker stays until the update finishes or is recovered. Boot recovery of an update already begun before any participation needs no new check: no participant acknowledged meanwhile, because step 2 of the participant's side saw the marker. **When exclusion ends (B1-5).** A controller record is removed only by claim D6's clearing: a fresh claim read showing `serving`, `free`, or that the box no longer participates, **and** any cleanup the record requires complete. A `lost` record whose cleanup-only termination failed is never cleared: claim D6 keeps that deny, and root's refusal stays with it. A box whose processes may still run under an operation never takes an executable update. An operator who needs to update such a box first resolves the host (`carlos ops host resolve`). **The race.** If the console reserves an update for `to` after the worker's roster read, the start proceeds, and the reservation is harmless by itself. Whichever of `to`'s acknowledgement and root's begin writes its marker first, the other sees it and refuses: either the update waits until the operation returns to `serving` and D6 clears the controller's state, or the acknowledgement waits until the update finishes. Root's refusal is what closes the race (H14). A box stays a participant from its `pending` state until D6 clears its record, through `active` and `lost` alike, so an update never runs under a relocation's `installing`, `probing` or release, nor while a lost controller's cleanup is unfinished. This holds for every claim operation a box takes part in, not only relocations. L6 asks the claim to make it D7's rule for box-started operations. ## 6. Infrastructure and IAM (A1-12) - **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. - **Disks (H19).** Nothing in IAM guards a box's disks for the fence's sake: rev 5.2's SCP, holds, volume-change role, guard attestation and service-role audit are withdrawn. The launch template and the `region-host` module keep `delete_on_termination = true` on every volume, which is cheap and makes automatic discharge of local chores the usual case (§5.9). The deployment should configure no Recycle Bin rule, Data Lifecycle Manager or AWS Backup policy that selects platform box volumes; one that does is a data-retention choice, and the operator path then owns their cleanup. The deployment accounts are Organizations members (organization `o-sgnzdj0z0c`, management account 665106592142; flagship 271376211898, dev 640012953448, checked 2026-10-06), which no longer matters to the fence. - **Auto Scaling enrollment (H16, H17, spec 4).** The box role gains one separate statement: `autoscaling:DescribeAutoScalingInstances` and `ec2:DescribeInstances`, read-only, conditioned on `aws:RequestedRegion` being one of the deployment's AWS regions (any of them, not only the box's own). Nothing else is granted across regions: every other statement keeps its own-region condition, and no write, queue or S3 right crosses regions. The code calls another region only to confirm membership for a region with no `active` box (§5.1), and the fence, volume records and relocation refuse any observation not made in the box's own region. - **Console role:** unchanged, no EC2 rights. - **S3 (A2-6).** Two kinds of write, kept apart: - **Create-only** (`If-None-Match: *`): content objects, `instances//*/files/*/objects/`, in the region's data bucket; box identity records, `control/boxes/`, volume records, `control/box-volumes/`, membership confirmations, `control/box-enrollment/`, and fence records, `control/box-fences/`, in the control bucket. - **Conditional replace** (`If-Match`, or `If-None-Match: *` for the first write): `instances//*/files/*/manifest.json` only. S3 enforces both in policy (A3-3): the data bucket denies `PutObject` 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). 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-volumes/*`, `control/box-enrollment/*` and `control/box-fences/*`. Each Deny is scoped to its prefix only: a broad Deny on this bucket once broke every lease release. The `*.bind.json` statement plan 1a added is no longer needed (§19). Data 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 should have it on every other EBS volume a box attaches. It never affects the fence (H19): it only lets a dead box's `park-local` chores be discharged automatically (§5.9). 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; an enrolled box in another region confirms its group membership (H17) and the console enrolls it. It is then the region's worker: it reads the termination event, writes the fence from that `terminated` read alone, and relocates every host to itself. The dead box's chores are discharged only if its volume records qualify (H19). | | A console's box is alive but its report is stale | a box-started relocation proceeds on the console's newest report if that met the floor and the box's update guard is armed (H18); otherwise it waits and alerts. | | The console's box is the one that died | failover does not need it: the fence, the census exclusion and every relocation CAS are a regional worker's (§5.9, L5, L6). | | Box partitioned from the control bucket | it keeps serving what it serves (no execution lease while `serving`, claim §7.1). It can't take new work. The group's health check decides whether it is terminated. | | Box alive but failing its health check | the group terminates it, then as above. Instances that were healthy lose up to H3's window, declared by `writes_lost`. | | A terminated box had a volume without `DeleteOnTermination`, or one was removed | fenced and relocated as usual; its `park-local` chores stay open for an operator (§5.9, H19). | | A copy of a dead box's disk survives (Recycle Bin, a copy, a snapshot) | a retention and cleanup matter for the operator; it can never act as the executor (§5.9, H19). | | A region's only box dies and its roster entry is still `active` | the cross-region confirmer reads it `terminated` and confirms the replacement; the replacement fences it (§5.1, B2-6). | | A participant's execution lease is lost and its cleanup fails | its controller record stays; root refuses executable updates on that box until the host is resolved (§5.10, B1-5). | | The source dies while a drain is in `starting` | the op becomes a failover in place (§5.8, B1-6). | | An update is reserved for `to` while a relocation starts | root refuses to begin it while `to` is a participant, or `to` refuses to acknowledge while it runs; never both running (§5.10). | | A forged or confused edges file names a terminated instance | ignored: identity comes only from the roster's `cloud`, proven at enrollment (HA7). | | Placer dies mid-relocation | another regional worker replays from the claim (§5.8). | | 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 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), 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; - 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 is `active` in the roster with a proven `cloud`; - the region's termination queues exist. **Volume recording is never part of this gate (B4-1, H19).** Spec 1 ships the recorder with the rest of §5, and rollout checks once that it runs, but neither the gate, nor a box's start, nor row minting, nor relocation, nor recovery ever waits on a volume record. A recorder that cannot write raises an alert, and its only effect is that a box that dies meanwhile keeps its `park-local` chores open for an operator (§5.9). 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` and in the console's box list. Each box re-checks at start only its runtime half: the capability and floor of the region's boxes and edges, and their roster entries. A box that finds a second box in its region without that half satisfied refuses to mint relocatable rows and alerts. The termination queues are a rollout check only: a missing queue loses one trigger, and the describe still fences (§5.9). 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. **Done on 2026-10-06 (H15):** a t4g.nano launched with a `DeleteOnTermination: true` root and a `DeleteOnTermination: false` extra volume, then terminated. While `shutting-down`, `DescribeInstances` still listed both volumes, with their flags and status `attached`. Once `terminated`, `BlockDeviceMappings` was `[]`, the root volume was already gone (`InvalidVolume.NotFound`), and the `false` volume survived as `available`. So disk evidence comes from records taken while the box runs, and decides only the discharge of local chores (H19, §5.9). The rehearsal terminates a box with an all-`true` mapping (chores discharged) and one with a `false` volume (fenced and relocated alike, chores left open). The rehearsal also enrolls a box into a dev region with no `active` box, confirmed from another region (H17), and checks that the cross-region statement allows only the two describe calls. 6. Then specs 2, 3, 4. ## 9. Changes requested of the claim and moves specs For platform-1e (claim rev 6.25, 413b12cb) and platform-d8 (moves rev 7.17, 39904c84). They replace rev 4.2's K1 to K11, which those sessions never received. "Ruled" means Paul's rulings of 2026-10-06 (H10 to H19, 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 D5 and D6 | New op kind `relocating` (§5.8): same region, stateful, from `serving`; its phase table with `op.exec`, stamp, rows and admission per phase; the `installed` no-reinstall boundary for the remote build, with a per-box local install receipt, bound to the stamp of the CAS that handed the box `op.exec`, required before `probing` and never remade after the first admission; probe attempts after the first restoring from their predecessor; the replacement table; the source-loss conversion to failover from `starting` or `releasing`; two replacements then `stuck`; the release sequence. Recovery owner `region:`, any regional worker (P6-D5). The D6 barrier needs only `to` when the start cites a termination fence or after a source-loss CAS. Excludes moves, placements and pushes. | Ruled in direction (H10; #236: "a new op kind, or an equivalent that the claim prefers") | | L2 | claim §4, C5, §7.2, §7.3 D2 | A termination fence (§5.9) is a lost-box fence for execution, written by a regional worker with no person in the loop: a verified `terminated` read (event, describe or, later, the group's history), bound to the roster entry's `cloud`. No disk condition. A `shutting-down` read is never evidence. Stopped, unclear and vanished boxes keep D2's operator path unchanged. | Ruled (H10, H19) | | L3 | claim §7.3 D5 | A fenced terminated box's `park-local` chores are discharged automatically in the fence CAS only when its volume records, from enrollment to its last running record, show every attached EBS volume `DeleteOnTermination` and none removed; that is D5's destroyed-local proof for discharge. Otherwise they stay open for D2/D5's operator path, and no recovery step waits on them. Regional chores move to `region:` as D5 says. | Ruled (H19) | | L4 | claim §7.3 D3 and D4, §5.9 P5-D3 | The fence record `control/box-fences/.json`, create-only, box-written, cited by `evidence_refs`. A terminated box goes on `lost` with that reference and no quarantine revision; it needs no readmission. The console later copies it into a D4 loss record and retires the roster entry. | Ruled in direction (H10, H1); record format for the claim session | | L5 | claim §10.1 D7 (required actors, console enrollments) | An enrolled box with a valid fence record is excluded from the census without waiting for the console to retire it. A console enrollment gains `compute: {box, enrollment}`, checked against its reports; a console whose `compute` box is fenced is excluded the same way (B1-7). | Ruled (H10, H14; #236: failover works when the console's box died) | | L6 | claim §10.1 D7 (lifecycle reservations, `actors_hold`), §7.3 D6 | For operations a box starts, replace the console reservation with §5.10's box-side check: the worker reads (never writes) the roster and refuses if an update is reserved for `from` or `to`; a participant writes its `pending` controller state, then refuses to acknowledge while root has an update begun; root writes its update-begun marker, then refuses an update while any controller record exists in any state, `lost` included, or cannot be read. A record is removed only by D6's clearing with its cleanup complete (B1-5). | Ruled (H14) | | L7 | claim §10.1 D7, §7.3 D2, §5.9 P5-D2, §6.6 P6-D2 | Enrollment of a platform box requires `internal/boxid` evidence; it records `cloud` from it, and checks the tofu `instance_id` for a reference already in claims or edges files. No other roster, and no `control/boxes` authority. | Ruled (H11) | | L8 | claim §5.1 steps 2 and 4, §5.9 P5-D2 and P5-D6 | The executor in the create intent is `choose()` (§5.2), with P5-D2's SHA-256 as the final tie-break; chosen once, never substituted; a create whose box can't complete is cancelled. | Ruled (H12) | | L9 | claim §6.4a item 2, `hostclaim.AdmitWriter` | A coverage value `released`, legal only on the admission that opens a prepared generation built from a pin reaching the `final_txid` a released box recorded from its stopped database, and only when the admission's predecessor (the last `holder.admissions` entry) is exactly that box and session, under its stop receipt. It declares nothing. Without it every drain declares a false loss (B1-1). | Requested | | L10 | claim §6.1, §6.6 P6-D1, `internal/stopevidence` | A writers-stopped check for release step 1: cgroup empty, no member processes, and database holders limited to the agent's own identified replicator descriptors. `Collect` stays unchanged for step 4. | Requested | | L11 | claim §4 (CC11), `hostclaim.StartGuard` | A `park-generation` chore in the region does not block a `relocating` start there: relocation writes only its own new prepared generation, never one being retired. Under P6-D4 nearly every recently woken host has one, which would hold failover up to the park horizon. | Requested | | L12 | claim C4, §8 (CC10), §6.6 P6-D2; moves §9.6 | Reconcile's row cases for `relocating` (§5.3): held participant rows; a former executor's row kept held until its `park-local` retires it; the 10-minute sweep as a stated exception to C4 for kept rows (H9). | Requested | | L13 | claim C3, §6.2a, §6.6 P6-D3 | The files publisher is a second ordinary-replication exception, bound to `{location, generation, session}`. `files//` belongs to that generation for the classifier; `park-generation` retires it except objects named by the files live set: every manifest from the files pin through `holder.generation`, and any manifest a running operation's pin journals (B2-4). | Requested | | L14 | moves §7.10 | A target terminated mid-move may be taken off the move by the termination fence, as M16's evidence, automatically, under the same before-commit rules. Moves decides what the move does then; the placer only supplies the fence. | Ruled (H10) | | L15 | moves §7.1, §7.3, §19.1 | A move into a multi-box region names its target **box** in the start CAS, chosen by `choose()`. Readiness, evidence, install and recovery bind to that box; replacing it is an explicit fenced transition (A1-10). | Ruled (H12) | | L16 | moves §5.1, §7.6, P6-D3's provider | Relocation's install reuses the landing's `building` and `published` phases and the prepared-generation authority, with a pinned set of remote versions as the source in place of a staged replica. One shared routine, so both get the same anchor and manifest rules. | Requested | | L17 | moves §6.1, §8, §9.4 | Every installation, a move's landing included, writes a files manifest in its new generation (§5.6), so unchanged files stay recoverable after the next failure; the archive at the cut stays. Timer freezing and draining apply to `relocating` holds. | Requested | | L18 | joint model, moves §14.2 | `internal/sim/hostlife` extends to two boxes per region: create spread, relocation by drain, termination mid-serve and in every relocation phase, nested failover, a stale edges file, an unenrolled reference, a volume without `DeleteOnTermination`, a crash mid-install, late file uploads and late PUTs after termination. | Requested | | L19 | claim §10.1 D7 (enrollment), with P3 | An Auto Scaling box is enrolled by the console with no operator when its `boxid` evidence verifies (deployment account, the region's AWS region) and a regional worker's create-only confirmation shows it a current member of the region's group (§5.1). Every other enrollment stays operator-approved. Spec 4 builds it. For a region with no live enrolled box (every enrollment there read `terminated`, positively, in the same pass, B2-6), any `active` box of another region confirms, by the same create-only write, bound to the group ARN the roster records for that placement; its cross-region rights are the two read-only describes and nothing else (H17). | Ruled (H16, H17) | | L20 | claim §10.1 D7 (required actors, console reports) | For box-started relocations only, a console's newest report counts however old if it met every floor check and the console's `compute` box has reported its D1 root update guard armed with the same floor digest. Every other census rule is unchanged. | Ruled (H18) | **Rev 4.2's requests, mapped.** K1 is L8. K2 is L1, with L9 to L11. K3 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:` 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:** 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, all sources empty, an event alone, a describe alone, a `shutting-down` read offered as evidence, and the fence accepted with no volume record at all); chore discharge (all records `true`: discharged; a `false` flag, a removed volume or no record: left open, with the relocation unaffected); a box starting while `control/box-volumes/` cannot be written: it mints its relocatable rows, takes part in relocation and recovers a dead peer's hosts, and only alerts (B4-1); the volume recorder (writes on change, at least hourly, `removed_volumes` when a volume leaves the mapping); cross-region confirmation (accepted only when the target region has no `active` box, refused for another group, an instance not `Pending`/`InService`, a confirmer not `active`, a region mismatch, a second confirmer losing the create-only race, and an emptied region whose dead box is still `active`: confirmed on a `terminated` read, refused on NotFound or `stopped`, B2-6); the console census for a box-started relocation (a stale report accepted with an armed guard, refused with no `compute` binding, no armed-guard report or a floor mismatch, and unchanged for a console-started operation); continuous files with a file held open (published at the deadline), inotify overflow, a file that changes during its read; the create-only and replace split in `hostfiles.Publish`. - **Relocation:** every row of the replacement table, the 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; the start refused when the roster reserves an update for `from` or `to`; a files update published by a probe session before its first database upload, then termination: the files pin keeps it while the database baseline falls back (B2-4); a crash during `probing` after the second admission: no reinstall, and the receipt still valid by `install_stamp` (B2-5); probe attempts one, two and three, with attempt three restoring attempt two's replicated writes and declaring attempt two's session (B1-1); a target terminated at `installed` replaced by one that makes its own local install before probing, and a `probing` CAS refused with another box's receipt (B1-2); `from` terminated in `starting` before and after acknowledging (B1-6). - **Starts and updates (§5.10):** root's begin and a participant's acknowledgement interleaved at every point, with a crash between each marker and its check: never an update and an acknowledged participation at once, and a crash leaves at most a refusal, cleared by retry; a lease lost during `probing` with cleanup failing, and an unreadable controller record, both refusing the update (B1-5). - **Integration:** two agents against one fake region, one control bucket: create lands on the chosen box only; the other box mints no row; the edge backhauls to the executor; relocate by drain through 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 5). ## 11. Open questions None. Rev 4.2's three were ruled as H7, H8 and H9 (2026-10-04). Rev 5's first three were ruled on 2026-10-06 as H14 (the box-side reservation check, §5.10), H15 (the running-time volume record, since superseded by H19) and H16 (automatic enrollment, §5.1, L19). Astra's rev 5 review raised two more, ruled the same day as H17 (an enrolled box in another region confirms the first box of an emptied region, §5.1, §6, L19) and H18 (a box-started relocation accepts a console's newest report when its box's update guard is armed, §5.9, L20). Astra's rev 5 round 3 found more ways around the volume guard; Paul answered with H19, which takes disk evidence out of the failover path (§5.9, §22). ## 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: 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, automatic enrollment of new boxes (H16, L19), ingress for boxes that come and go (a per-region NLB with fixed EIPs, or an EIP pool claimed at boot), HTTP-01 certificates, steering, scale-out on headroom, scale-in by drain (§5.8), per-region minimum (H5). - **Not planned:** relocating unit- and socket-backed routes (the console and platform services). Their HA is the HA ladder's, separately. ## 13. Astra round 1 dispositions (rev 2) | Finding | Disposition | |---|---| | A1-1 P1 termination evidence not bound to identity | accepted: AWS-signed box records (§5.1), HA7, fence fields (§5.9), K6 | | A1-2 P1 new generation never populated | accepted: pinned recovery set and `installing` builds `G'` (§5.8), K8 | | A1-3 P1 replay overwrites an installation that has written | accepted: phase table, `installed` boundary, participant-terminated exits (§5.8), K2 | | A1-4 P1 file update and tombstone order | accepted: immutable objects, per-host `seq`, `If-Match` manifest, snapshot boundary (§5.6) | | A1-5 P2 `active_stamp` is not install evidence | accepted: installation-complete marker (§5.5), HA3 | | A1-6 P2 participant rows and former executors | accepted: three row cases (§5.3), K11 | | A1-7 P2 timers not reconstructible | accepted: timer state replicated continuously, imported with `ReplaceTimers`, catch-up (§5.7) | | A1-8 P2 unit and socket hosts | accepted: not relocatable (§2, §7, §12) | | A1-9 P2 adoption alone does not admit a second box | accepted: capability, HA floor and multi-box gate (§8), unstamped entries (§5.4) | | A1-10 P2 moves target box | accepted: K10 | | A1-11 P2 termination evidence can vanish | accepted: EventBridge to SQS with 14-day retention, NotFound never evidence (§5.9) | | A1-12 P2 Describe permissions by tag | accepted: `ec2:Region` condition, membership checked by the verifier (§6) | | A1-13 P3 citations | accepted: `lease.go:37`, `reconcile.go:202`, `edgesfile.go:272`/`:326` | ## 14. Astra round 2 dispositions | Finding | Disposition | |---|---| | A1-1 residual: a legacy label's first registration | accepted: an operator's bind checked against the region's tofu `instance_id` output and the claims' existing label (§5.1) | | A1-7 residual: `routes.next_due` | accepted: wake state carries `NextDue` and `Replication` with the timer rows (§5.6, §5.7) | | A2-1 P1 snapshot-only baseline loses the replication position | accepted: moves rev 7.6's replication baseline with the level-0 anchor, verified before `installed`, and its test (§5.8), K8 | | A2-2 P1 early target replacement skips release and pinning | accepted: phase-specific replacement table (§5.8), K2 | | A2-3 P2 reconcile drops the relocating source | accepted: per-phase rows for both participants (§5.3, §5.8 table) | | A2-4 P2 event delivery is best-effort | accepted: a third method (Auto Scaling activity history, verified in spec 4 first), `awaiting-evidence` with an immediate alert, and operator resolution via CloudTrail when all are empty (§5.9) | | A2-5 P2 close and rename don't bound continuous sync | accepted: `IN_MODIFY` with a fixed one-second deadline from the first modification, recursive watches, overflow scans, a stable-read check (§5.6) | | A2-6 P2 create-only conflicts with manifest replacement | accepted: create-only and conditional-replace writes separated, enforced in one writer (§6) | | A2-7 P2 a live target whose probe never passes | accepted: a probe deadline, `probe-failed` with stop evidence, a nested relocation that keeps probe writes, and `stuck` after two replacements (§5.8), K2 | ## 15. Astra round 3 dispositions | Finding | Disposition | |---|---| | A2-5 residual: an unstable file waits for the scan; a failed watch | accepted: published at every deadline as the last image, flagged; per-second polling while coverage is missing (§5.6) | | A2-7 residual and A3-2 P1: probe failure skips the target's durability barrier | accepted: one release sequence for the source and a failed target, journaling `final_txid` and `manifest_seq` before stop evidence, all files flushed whatever the plan; pinning must reach them (§5.8), K2, K8 | | A1-1 residual and A3-3 P1: the bind isn't operator-authenticated | accepted: binds name the exact record version; the control bucket's policy limits binds to operator roles and denies replace and delete under `control/boxes/` (§5.1) | | A3-1 P1: a CloudTrail request is not compute fencing | accepted: claim §7.2's terminal-state rule unchanged; CloudTrail is a finding aid only; otherwise `awaiting-evidence` (§5.9), K3 | | A3-3 (part): S3 can enforce conditional headers | accepted: `s3:if-none-match` and `s3:if-match` policy conditions, scoped per prefix (§6) | | A3-4 P3: citations | accepted: `internal/host/fleetbind.go`, `edge.go:2432`, `homemap.go:538`/`:582`, `reconcile.go:335`/`:799` | ## 16. Astra round 4 dispositions | Finding | Disposition | |---|---| | A4-1 P1: the release sequence flushes before stopping writers | accepted: stop and empty the process tree and timer deliveries first, then flush and journal, then finish stop evidence (§5.8), K2 | | A4-2 P2: the conditional Deny blocks multipart preparation | accepted: `s3:ObjectCreationOperation: true` on every header Deny; multipart completion carries the header; tested (§6) | | A4-3 P3: 29245f69 is not moves rev 7.6 | accepted: rev 7.6 named as an uncommitted draft, rev 7.5 at cdc98845 as the last committed; the plan pins the commit (header) | ## 17. Astra round 5 dispositions | Finding | Disposition | |---|---| | A5-1 P1: step 1 waits for the replicator's handle, closed only in step 4 | accepted: step 1 allows only the box's own replicator descriptors; step 4 closes it and runs the unrestricted check; tested with a live replicator (§5.8), K2 | ## 18. Notes from plan 1a (2026-10-05) Plan `docs/superpowers/plans/2026-10-05-region-ha-1a-foundations.md` builds the parts of this spec that need no claim. It keeps every property above and changes three mechanisms: 1. **Exact content by hash, not by S3 version id (§5.6, §5.1).** The store abstraction has no version-id read and the box role has no `s3:GetObjectVersion`. Objects are immutable, their key contains their SHA-256, the manifest records it, and a reader verifies it. A bind names its record by `record_sha256` in place of `record_version_id`. 2. **The identity signature (§5.1).** The record carries IMDS's base64 RSA-SHA256 signature (`/latest/dynamic/instance-identity/signature`), verified with the regional certificate, in place of the PKCS7 form. Same document, same signer, no new dependency. 3. **`snapshot` is a periodic full publish, not a sealed archive (§5.6).** `hostfiles.SyncDir` stages every difference between the directory and the manifest. Run on the snapshot interval it gives the `snapshot` setting; run every ten minutes it is the continuous setting's repair scan; run before stop evidence it is the release flush. The manifest therefore has no `base` or `base_seq`, and restore reads one manifest and the objects it names. Two corrections to the spec, found while planning: - **§5.4's alert for two unstamped entries is dropped.** Static sites and public address routes run on every box, so every box publishes them as `home`, unstamped: that is normal, and the edge cannot tell them from relocatable hosts. The edge reports only two boxes at the same positive stamp. Plan 1b decides whether the publisher marks relocatable entries so the edge can alert on those alone. - **§5.1's region check has two halves.** `boxid.Verify` proves which region a box is in. Whoever uses that compares it with the region it expects: `eligibleBoxes` takes the placement's AWS region and refuses a box whose signed region differs, and `termfence.Verify` compares the observation's region with the signed one. Plan 1b must supply the expected region from something better than a majority vote of the unsigned edges files. - Build tags (Task 6): the descriptor-based directory code is `//go:build unix`, not `linux`, so the CLI's macOS build uses it too; Windows gets a stub that publishes nothing. 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/.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/