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, <host>.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/<id>.json authority. internal/boxid's AWS-signed IMDS identity verification becomes the evidence required to enroll a box. Enrollment records the proven account, region and instance id in the roster entry's cloud field, and the termination fence binds to that entry. Box references are opaque (claim §2, rev 6.16) and follow #212 option B: the label is the key, the instance id is private. | | H12 | (2026-10-06) Executor choice at create is spec 1's choose(): prefer a box running no instance of the app; then the most headroom (until spec 2, the fewest claimed hosts); then the claim's P5-D2 SHA-256 of host + "\x00" + box reference as the final tie-break. It is recorded once, in the create intent. Recovery never substitutes. | | H13 | (2026-10-06) Claim ruling R6 supersedes HA3 and §5.5. A box never reuses its local database. Every admission is cold until claim P6-D4 lifts. HA3 and §5.5 are deleted, and the activator half of plan 1a's install marker is not used. | | H14 | (2026-10-06) Relocation starts need no console reservation (L6). A relocation start requires that no executable update is reserved for from or to in control/host-actors.json, which the worker reads and never writes. Root on each box refuses to start an executable update while that box is a participant in a running claim operation. The update side's refusal is what closes the race with a reservation made after the start's read. (§5.10.) | | H15 | (2026-10-06) H10's volume check rests on a running-time record, not the terminated read. Tested on dev 2026-10-06: while shutting-down, DescribeInstances still listed both volumes of a test instance with their DeleteOnTermination flags; once terminated, BlockDeviceMappings was empty, the true root volume was already gone (InvalidVolume.NotFound) and the false volume survived as available. So the fence rests on (1) a record of the box's block device mappings taken by regional workers while it runs, refreshed on change, kept with its roster-bound evidence, showing every attached EBS volume DeleteOnTermination: true; (2) IAM denying ec2:ModifyInstanceAttribute and ec2:AttachVolume on platform boxes to every principal except operator roles, so the record cannot go stale behind the platform's back; (3) the terminated read (describe, event, later the group's history). A shutting-down read that still lists mappings may refresh the record but is never itself evidence. A missing record, one older than the stated bound, or one with any false volume sends the box to the operator path. (§5.9, §6.) 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/<id>.json is no longer an authority. The roster is. What plan 1a built in internal/boxid becomes the evidence a box must present to be enrolled.

Enrollment. A box asks to be enrolled by publishing its identity evidence, the record plan 1a defined:

control/boxes/<box reference>.json

{
  "v": 1,
  "box": "<box reference>",
  "identity_document": "<base64 IMDS instance identity document>",
  "identity_signature": "<base64 RSA-SHA256 signature from IMDS>",
  "written_at": "<RFC3339>"
}

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/<box reference>/<instance id>.json, from a fresh read-only autoscaling:DescribeAutoScalingInstances showing the instance a current member (Pending or InService) of that region's group, with the group name from the deployment's configuration. Anything else, a fixed box included, is enrolled only with an operator's approval. Spec 4 builds this; the claim's D7 needs to allow it (L19).

A 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/<box reference>/<instance id>.json, with {target_placement, aws_region, group_arn, instance_id, lifecycle_state, observed_at, request_ids, confirmer: {box, enrollment, region}}. Two confirmers race by the same conditional write: one creates it, the other gets a refusal, reads it, and stops.

The console accepts a cross-region confirmation only if, at enrollment, 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:

{
  "box_id": "<box reference>",
  "capabilities": ["region-ha-1"],
  "draining": false,
  "headroom": { "mem_free_mib": 2210, "disk_free_mib": 31200, "awake": 14 }
}

• box_id must equal 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 <host>.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, <host>.env, <host>-sidecar.env, and the host's wake state (§5.7: timer rows, the route's NextDue and Replication). They are small, and losing them is what kept kpmg down for 1h54m (moves §1.2).

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, <holder.location>/files/<generation>/objects/<seq>-<sha256>, 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, <holder.location>/files/<generation>/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 <location>/files/<generation>/, and stops with the session. It is a producer for stop evidence (claim P6-D1) and is joined before the receipt. Its PUTs are a second ordinary-replication exception to claim C3 (L13).
• Each cold admission starts a new manifest. Under P6-D4 every wake is a cold admission into a new generation. Before the app starts, the admitting box writes files/<new generation>/manifest.json create-only, as a copy of the 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/<generation>/ prefix is retired with that generation, by the park-generation chore PublishGeneration queues, except objects that a manifest in the live set still names (L13). The 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) | | <host>.config.env | rendered for the held row (RenderHeld, claim §6.1 CC13, P6-D3), needs the secrets key (R9) | | Release | materialized for the held row (MaterializeHeld) | | Certificates | the cert mirror's boot refresh (on main) | | Registry row | reconcile, 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, toenrollment, region, reason, stampfrom, generationfrom, fence?, directoryrevision}

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": "<box>", "generation": "<G>", "session": S, "final_txid": N, "manifest_seq": M, "receipt": "<key>", "receipt_sha256": "…"}, and pinning refuses to pin less than it.

The pinned recovery set (A1-2). In pinning, 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 <host>. 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/<enrollment>/<observed_at>.json

{"v": 1, "box": "<box reference>", "enrollment": "<enrollment>",
 "cloud": {"provider": "aws", "account": "123…",
           "region": "eu-west-1", "instance_id": "i-0abc…"},
 "instance_state": "running",
 "block_devices": [{"device": "/dev/xvda", "volume_id": "vol-…",
                    "delete_on_termination": true, "status": "attached"}],
 "removed_volumes": [],
 "observed_at": "<RFC3339>", "request_id": "<EC2 request id>",
 "written_by": {"box": "<reference>", "enrollment": "<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/<enrollment>.json

{"v": 1, "box": "<box reference>", "enrollment": "<enrollment>",
 "cloud": {"provider": "aws", "account": "123…",
           "region": "eu-west-1", "instance_id": "i-0abc…"},
 "state": "terminated",
 "observed_at": "<RFC3339>",
 "via": "describe" | "event" | "activity",
 "request_id": "<EC2 request id, when via=describe>",
 "event_id": "<EventBridge event id, when via=event>",
 "written_by": {"box": "<reference>", "enrollment": "<enrollment>"}}

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:<r>, keeping their ids, operations and scopes (D5). Remote scopes it justifies take the fence's observed_at as their original evidence time (claim P5-D3, D5).
• The roster follows later. The console moves the box's roster entry to retired, citing the record, when it next runs. Until then the record alone excludes the box from the census for lifecycle starts (L5), so failover never waits for a console.
• 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/<host>.json state as pending, durably (claim D6's existing state and write protocol);
2. then reads root's update state: the system-update journal and root's update-begun marker (below). If an update is begun or in progress for this box, it refuses to acknowledge, clears its pending state, and retries after the update finishes. The operation cannot leave starting without to's acknowledgement, so nothing has moved; the worker waits, or replaces to (§5.8).

Root, before it starts an update. Every path that begins an executable change (system apply, explicit rollback, a guarded activation under claim D1, the console's activation reservation being acted on), under root's existing system-update lock:

1. writes an update-begun marker, durably, beside the update journal (/opt/carlos/system/guard/update-begun.json, naming the update);
2. then scans <DataDir>/.hostexec/ 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/<host>/*/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/<host>/*/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).

1. Relocation by drain stays off until the claim accepts L9; failover relocation needs L1 to L6.
2. 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.
3. 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:<r>, any regional worker (P6-D5). The D6 barrier needs only to when the start cites a termination fence or after a source-loss CAS. Excludes moves, placements and pushes. | Ruled in direction (H10; #236: "a new op kind, or an equivalent that the claim prefers") | | L2 | claim §4, C5, §7.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:<r> as D5 says. | Ruled (H19) | | L4 | claim §7.3 D3 and D4, §5.9 P5-D3 | The fence record control/box-fences/<enrollment>.json, create-only, box-written, cited by evidence_refs. A terminated box goes on lost with that reference and no quarantine revision; it needs no readmission. The console later copies it into a D4 loss record and retires the roster entry. | Ruled in direction (H10, H1); record format for the claim session | | L5 | claim §10.1 D7 (required actors, console enrollments) | An enrolled box with a valid fence record is excluded from the census without waiting for the console to retire it. A console enrollment gains compute: {box, enrollment}, checked against its reports; a console whose compute box is fenced is excluded the same way (B1-7). | 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/<generation>/ 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:<r> work to any enrolled worker. L1 names the owner.
• K5 (adoption only while a region has one box): P5-D2 requires exactly one proven installation owner and refuses zero or several, which is the property K5 wanted, whatever the box count.
• K6 (box names bound by control/boxes): claim §2 rev 6.16 makes references opaque, and H11 makes the roster the binding (L7).

The disposition tables (§13 to §17) still cite K numbers. They refer to rev 4.2's table; this mapping says where each now lives.

10. Testing

• Unit: 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/<id>.json as authority (H11). boxid.Load and boxid.Verifier are now used once, at enrollment, and their result is stored in the roster entry's cloud. eligibleBoxes takes its verified identities from the roster, not from loading records. The record object stays as the enrollment evidence, create-only, and grants nothing.
• The operator bind (Bind, control/boxes/<label>.bind.json, carlos ops box bind, plan 1b item 13). Its tofu check moves into enrollment (§5.1). The bucket policy's bind statement is harmless and can go at the next apply.
• WarmCopyTrusted and the activator's warm path (H13). Nothing skips a restore, so plan 1b item 4 is dropped. The InstallMarker type may serve as relocation's last local install journal entry, as moves' .files-gen does, or be removed; nothing reads it to trust a local database.
• chooseBox's last tie-break. The lowest box id becomes P5-D2's greatest SHA-256 of host + "\x00" + reference (H12). The first two rules stand.
• termfence's binding and inputs. Verify binds to a boxid.Identity; it must bind to the roster entry's cloud and produce §5.9's record. It takes no volume input (H19); a separate function decides chore discharge from the volume records. FromDescribe and FromEvent stay as the two terminated reads; a shutting-down observation is never accepted. Plan 1b adds the volume recorder, the discharge check, §5.10's two checks and, for spec 4, the membership confirmation (H16).

Stays as built.

• internal/boxid's record, signature check and embedded regional certificates (verified on the dev box), as enrollment evidence.
• The edges file's box_id (the label, which is the reference under #212 option B), capabilities, draining and headroom.
• The home map settling two claims by installation stamp, and reporting equal stamps.
• eligibleBoxes' one-box-at-a-time predicate, with the roster as its source.
• internal/hostfiles: the ordered manifest, immutable hashed objects, SyncDir, the continuous publisher, the watcher, restore and wake state. Plan 1b adds the generation binding, the copied manifest at each cold admission, and retirement by the claim (§5.6).
• registry.ReplaceTimers.
• The infrastructure: one termination queue per box, root volumes deleted on termination, the create-only control/boxes/ policy. The fence prefix control/box-fences/ needs the same create-only, never-deleted statements (§6).

Plan 1b's list, revised. Items 1, 3, 5, 9 and 10 stand, read against rev 5 (item 10's expected region now comes from the roster). Item 2 follows §5.3's revised table. Item 4 is dropped. Item 6 becomes publishing the enrollment evidence at start. Item 7 is §5.8 as rev 5 states it, and waits for L1 and L9 to L11. Item 8 adds the roster check to the gate; volume recording is not part of it (B4-1).

Rev 5.1 adds to plan 1b: the removed-volume rule (§5.9), the local install receipt (§5.8), and root's refusal on any controller record (§5.10). Rev 5.1 and 5.2's hold, release, guard attestation and SCP are withdrawn by H19 and are not built.

20. Astra rev 5 round 1 dispositions

Reviewed rev 5 at 2a9165d4 (CODEX-FINDINGS-REGION-HA-REV5-1.md). Each citation was checked against claim 98b45332, moves a4711728 and main before acceptance.

| Finding | Disposition | |---|---| | B1-1 P1 probe retries restore P again and lose replicated writes; released suppresses loss too widely | accepted: claim §6.4a item 3 and moves §7.14's restore row choose a fresh admission's baseline from its predecessor. Only the first attempt opens P; later attempts restore through genselect.Select; coverage is decided per admission, released only on P's opening with a predecessor matching the journaled release (§5.8, L9) | | B1-2 P1 a replacement at installed never makes its local install | accepted: the remote build and the per-box local install are separate; probing requires a local install receipt bound to op.exec, its enrollment and holder.stamp; a replacement makes its own from P's files manifest, and P is still built once and opened once (§5.8, L1) | | B1-3 P1 an operator's volume change before a refresh, or a detach, allows a false destroyed-disk fence | accepted: a hold written before the change suspends disk evidence; a volume leaving a running box's mapping suspends it too; release needs a newer all-true record and an operator's attestation for every removed volume (§5.9, §6, §7) | | B1-4 P1 the guard rests on an unprotected tag; the non-Organizations fallback still fences | accepted: the SCP also denies changing carlos:role except at launch; exemption narrowed to one hold-gated role; a root-signed guard attestation is required, and without one there is no automatic fence. Stricter than H15, never weaker (§5.9, §6, §8) | | B1-5 P1 a lost controller stops excluding updates | accepted: claim D6 does define lost and keeps its deny on failed cleanup. Root now refuses on any controller record in any state or any unreadable one, until D6's clearing with cleanup complete (§5.10, L6) | | B1-6 P2 the source lost in starting has no transition | accepted: a source-loss CAS converts the op to failover from starting or releasing, keeping the intent and acknowledgements, removing from from the barrier (§5.8, L1) | | B1-7 P2 a dead console stays in the D7 census | accepted: claim D7 does require every console. Console enrollments gain a compute binding; a console on a fenced box is excluded. A live console with a stale report was ruled as H18 (§5.9, L5, L20) | | B1-8 P2 automatic enrollment cannot bootstrap an emptied region | accepted: §2 makes a confirmer an active enrolled box in the region, so none is left. ruled as H17: an enrolled box in another region confirms, with read-only cross-region describes only, so one-box regions recover automatically (§5.1, §6, §7, L19) | | B1-9 P3 stale code citations | accepted, checked on main: provision.go:49, reconcile.go:348/:820, :192, :215, activator.go:1164-1168, :2204, edge.go:2466, main.tf:521. Disposition tables §13 to §17 keep their historical anchors |

21. Astra rev 5 round 2 dispositions

Reviewed rev 5.1 at fdc0fe07 (CODEX-FINDINGS-REGION-HA-REV5-2.md). Each finding was checked against claim 98b45332, moves a4711728, main and AWS's documented API and policy contracts before acceptance.

| Finding | Disposition | |---|---| | B1-2 partly resolved: the receipt dies with the next probe stamp | answered by B2-5 | | B1-3 partly resolved: release can precede authorized mutations | answered by B2-2 | | B1-4 partly resolved: root replacement unguarded; the attestation conflicts with Auto Scaling | answered by B2-1 and B2-3 | | B1-8 partly resolved: H17's emptiness test is circular | answered by B2-6 | | B2-1 P1 CreateReplaceRootVolumeTask bypasses the guard | accepted: added to the deny, with snapshots and images (which also leave a copy of the disk), the hold workflow and the rehearsal; a replaced root volume shows as removed (§5.9, §6, §8, L2) | | B2-2 P1 a release does not close the change's authority | accepted: the hold names its instance and the role's exemption is limited to it; release revokes the role's earlier sessions, waits for no attaching, detaching, replace-root, snapshot or image task and for the signature-age bound, then needs a validating record after that barrier. Session tags are acknowledged as the caller's word; the hold-first order is the operator trust boundary, as in claim D2 (§5.9) | | B2-3 P1 Auto Scaling's service-linked role defeats the attestation | accepted: the attestation no longer asserts that no service role can touch a disk. It reads every service-linked role's managed policy at its default version and requires each disk or tag action to map to an initiating API the SCP denies; Auto Scaling's (refresh, group create and update, warm pool, attach) are denied but for the hold-gated role; a policy version change invalidates it (§6, §7) | | B2-4 P1 the files pin follows the database baseline and can drop published files | accepted: the files pin is the newest manifest in the admitted chain, chosen independently; the files live set covers it through holder.generation and any running op's pin (§5.6, §5.8, L13) | | B2-5 P2 later probe stamps invalidate the receipt and invite a reinstall | accepted: the receipt binds to op.journal.install_stamp, the stamp of the CAS that handed op.exec; after the first admission the local install is never remade, and a lost receipt is stuck (§5.8, L1) | | B2-6 P2 the dead box stays active, so H17 never fires | accepted: the confirmer requires a positive terminated read for every active or quarantined enrollment in the region, in the same pass, as part of confirming membership; it is not a fence and retires nothing. The new box then fences through the ordinary path (§5.1, §7, L19) |

22. Astra rev 5 round 3 dispositions, and H19

Reviewed rev 5.2 at 075d709f (CODEX-FINDINGS-REGION-HA-REV5-3.md). Each finding was checked against AWS's documented contracts. All five are about the volume guard. Paul's ruling H19 (2026-10-06) took the disk out of the failover path, so they no longer bear on safety.

| Finding | Disposition | |---|---| | B3-1 P1 Recycle Bin keeps volumes deleted on termination | correct about AWS, and moot for the fence under H19: a retained volume cannot run or write, and is never admitted as the executor. For chore discharge it is a retention concern for the operator path; §6 asks the deployment to configure no retention rule over platform volumes (§5.9, §6) | | B3-2 P1 CopyVolumes bypasses the copy guard | correct, and moot under H19 for the same reason: a copy is a data-retention concern, never a second writer (§5.9) | | B3-3 P1 another Auto Scaling group can overwrite the protected tag | moot: H19 removes the tag-conditioned guard; nothing in the fence or discharge reads the carlos:role tag any more (§5.1, §6) | | B3-4 P1 concurrent releases move the revocation cutoff back | moot: holds, releases and the change role are withdrawn (§5.9, §6) | | B3-5 P2 the release barrier omits Auto Scaling workflows | moot: there is no release barrier. A root replacement under any workflow shows as a removed volume, which only keeps the chores open (§5.9) | | B2-1, B2-2, B2-3 (partly resolved in round 3) | withdrawn with the mechanisms they patched; the property they protected is no longer needed for execution (H19) |

Earlier volume-guard findings, revisited. B1-3 (operator changes before a refresh), B1-4 (an unprotected tag, the non-Organizations fallback), B2-1 (root replacement, snapshots, images), B2-2 (release authority) and B2-3 (service-linked roles) all showed ways a disk could outlive its box despite the records. Under H19 each such disk is a cleanup concern: the box is fenced by its terminated read alone, and a surviving disk can never become the executor, because admission needs op.exec to name an enrolled, active box (claim C4, HA7), and a new instance is a new enrollment. What remains of them is one cheap rule: any false flag or removed volume in any record keeps the dead box's chores open for an operator. Their dispositions in §20 and §21 stand as history.

Checked after removing the guard. H17's confirmer no longer reads the carlos:role tag, and needs nothing else from the guard. The volume recorder stays, for discharge only. §5.10, the census (L5, L20), relocation (§5.8) and the fence read no disk evidence. CC11 lets a relocation start while a dead box's park-local is open, since it names only that box. A surviving disk attached to a new instance brings host artifacts the new enrollment does not own; claim P6-D2 refuses to initialize or materialize over ambiguous ownership, and every writer restores from the certified remote anyway (claim R6), so the old database is never served.

23. Astra rev 5 round 4 dispositions

Reviewed rev 5.3 at 27058fe1 (CODEX-FINDINGS-REGION-HA-REV5-4.md). Astra agreed B3-1 to B3-5 are moot under H19, and found no two-writer or data-loss path that depends on disk evidence.

| Finding | Disposition | |---|---| | B4-1 P2 volume recording is still a runtime admission prerequisite through §8's gate | accepted: under H19, volume recording never gates execution, admission, relocation or recovery. The gate no longer checks it; a box's start re-checks only capability, floor and roster; recorder failure alerts and keeps a dead box's chores open; tested through start, row minting and recovery (§8, §10, §19) | | B4-2 P3 summaries still describe the disk-dependent fence | accepted: the source-loss table discharges chores only on qualifying records (§5.8); the tofu note says delete_on_termination affects only discharge (§6); the one-box row fences on the terminated read alone (§7) |

24. Notes from plan 1b (2026-10-06)

Plan docs/superpowers/plans/2026-10-06-region-ha-1b-claim-readers.md builds the parts of rev 5.4 that need none of L1 to L20: enrollment evidence, §19's corrections, the agent publishing its identity record, the fence bound to the roster's cloud, volume records and the discharge check, the edges file following op.exec, and root's half of §5.10. All of it is dormant behind CARLOS_REGION_HA. It keeps every property above and settles five details:

1. Enrollment refuses one instance under two references (§5.1). The record's box field is not covered by AWS's signature, so box A's record copied to B's key with that field rewritten still verifies. boxid.Verifier.Enroll refuses an instance the roster holds under another reference, as well as a reference the roster holds for another instance, counting entries in every state.
2. A positive stamp is the relocatable mark (§18's open question). Only relocatable hosts with a claim, and their aliases and served catch-alls, carry a stamp, so the edge's report of two boxes at one positive stamp already concerns them alone. No separate marker.
3. The edges file's claim reads (§5.4). A relocatable host with no claim is published as before, unstamped: §8's gate admits a second box only once every host has a claim. A read that fails keeps the last decision. Each read stands 10 minutes (H9), at most 256 reads a pass.
4. "The first record taken at enrollment" (§5.9) is the earliest volume record for the enrollment, observed within one hour of the roster's enrollment time. A later first record cannot speak for a volume attached and removed before it, so the chores stay open. And (controller ruling, 2026-10-06) the newest record must be no more than two hours older than the termination observation; otherwise the chores stay open for the operator path.
5. No volume record from a terminated read. Its mappings are empty (§8 step 5's dev test), and recording it would list every volume as removed.

It also removes plan 1a's Bind, BindKey, Verifier.Verify and activator.WarmCopyTrusted, and makes every box-evidence prefix create-only and never deleted in the deployment bucket's policy.

Controller rulings of 2026-10-06, on Paul's behalf: the edges file withholds a relocatable host when op.exec names another box or none (§5.4 as written); root's §5.10 refusal stays behind CARLOS_REGION_HA until claim D6 lands, then becomes unconditional; the *.bind.json statement and operator_role_arns stay until no root sets the variable.