amadan
spec: host lifecycle claim rev 3, the joint model's required changes CC1-CC13
Late-completion horizon and per-region quiet_after for the replication exception; version-keyed park copies that accumulate; the parker's own lock excluded everywhere; discovery parks at adoption through one routine; purge adopts first and its reservation is its journal; declare-lost needs compute fencing only; self-fence ends on a fresh read; stale holds released; no op over a pending chore; quarantined boxes retire their own state; probes render held config.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+114
−23
docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md+114 −23
CI cancelled — superseded by a newer push — run details
diff --git a/docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md b/docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md| index 611af3cbb..3e6fb5948 100644 |
| --- a/docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md |
| +++ b/docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md |
| @@ -1,6 +1,6 @@ |
| # The host lifecycle claim |
| -Design, 2026-10-02, **rev 2**. A small primitive cited by: |
| +Design, 2026-10-02, **rev 3**. A small primitive cited by: |
| - **#199**, deleting an instance and parking its data: |
| `2026-10-02-replica-ownership-design.md`, which this spec supersedes |
| @@ -17,6 +17,10 @@ I-7, adopts its replacement for D4, and answers N1, N3 to N10, N12 and the |
| carried-forward R3-12. The moves-only findings (N2's move side, N11, N13, |
| N14, N15) are the moves spec's. §12 maps every finding to its section. |
| +**Rev 3** folds in CC1 to CC13, the claim changes required by the joint |
| +executable model (`internal/sim/hostlife/` at 1486345c on |
| +`design-moves-any-region`, moves spec §19.4). §12 maps them too. |
| + |
| The method changes too. The moves session is building an executable |
| joint model: a deterministic randomized Go simulation covering every |
| actor, the real IAM split, late S3 completion, crashes, partitions and old |
| @@ -87,7 +91,8 @@ replaced whole with conditional writes (`If-Match` on the ETag read). |
| "retirement": "rt_…", "owner": "region:ie"} |
| ], |
| "lost": [], |
| - "retired_incarnations": ["<hex>", "…"] |
| + "retired_incarnations": ["<hex>", "…"], |
| + "quiet_after": {"ie": "<RFC3339>"} |
| } |
| ``` |
| @@ -120,6 +125,9 @@ Field rules: |
| - **`retired_incarnations`** keeps the most recent 32 incarnations that |
| held this host. A create whose incarnation appears there is refused |
| (R3-12). |
| +- **`quiet_after`**, one entry per region, is the earliest time a new |
| + install may write the host's namespace in that region (§6.2a, CC1). |
| + Like `retired_incarnations`, it survives `free`. |
| ## 3. Invariants |
| @@ -151,8 +159,15 @@ Every destructive storage call names **an exact object version**: a |
| `key?versionId=`. Never a bare key. Both buckets are versioned |
| (deployment-buckets/main.tf:23, :28). A request that completes late |
| therefore touches only the version it named, never a later incarnation's |
| -object at the same key. That makes late server-side completion harmless |
| -(J-N1). |
| +object at the same key, so late completion of the **operation's own |
| +calls** is harmless (J-N1). |
| + |
| +**That does not cover the replication exception (CC1).** A serving |
| +process's ordinary replication is plain PUTs to LTX names, and those names |
| +repeat across lineages. A PUT signed before stop evidence can still land |
| +afterwards, up to S3's 15-minute signature-age limit plus the request's |
| +own duration. Every retirement therefore waits out a late-completion |
| +horizon (§6.2a), and an install waits for the region's `quiet_after`. |
| - **A bare-key delete is forbidden on these prefixes.** On a versioned |
| bucket it creates a delete marker that would hide a successor's current |
| @@ -218,6 +233,8 @@ not by itself transfer execution authority: `op.exec` changes only by a |
| CAS that cites stop evidence or a lost-box fence. |
| Only one operation runs at a time, and a new one starts from `serving`. |
| +The start CAS also fails if any open obligation names a region or box the |
| +new operation will write (CC11). A pending chore there must finish first. |
| ## 5. This spec's operations |
| @@ -275,8 +292,15 @@ site now uses: |
| ### 5.3 App purge (J-N9) |
| 1. **Reserve the app first.** Write `apps/<acct>/<app>/purge.json`, |
| - create-only. The create door refuses any create for an app with this |
| - reservation. |
| + create-only, as `{id, phase: "reserved"}`. The create door refuses any |
| + create for an app with this reservation. **The reservation is the |
| + purge's journal (CC7).** It records the purge's phase, and the |
| + recovery pass drives those phases in order: `reserved → adopted → |
| + claimed → torn-down → retired → done`. Only the purge's own completion |
| + removes it. A host claim going `free` never does. |
| +1a. **Adopt first (CC6).** Run the one adoption routine (§9) for every |
| + record of the app that has no claim, before deciding which hosts the |
| + app holds. |
| 2. **CAS every host claim of the app** to `{purging, id}`, from `serving`. |
| A host under any other operation fails the purge with its reason. The |
| ones already reserved stay reserved, and the operator retries. |
| @@ -322,11 +346,17 @@ certified as stopped just because its parent exited. Its host needs the |
| cleanup operation first. A box without cgroup delegation cannot produce |
| evidence, so lifecycle operations on its hosts are refused. |
| +**Probes (CC13).** Every lifecycle probe renders the **held** config and |
| +materializes the **held** release (`RenderHeld`, `MaterializeHeld`) |
| +before it spawns. That covers moves, reverts and a future push. A probe |
| +never uses whatever the ordinary passes last wrote. |
| + |
| ### 6.2 Parking, by exact version (J-N1, J-N6, J-N7, J-D5) |
| -**Destination.** Each retirement event has its own destination: |
| +**Destination.** Each retirement event has its own destination. Within |
| +it, each copy's key carries its source version (CC2): |
| - parked/<incarnation>/<host>/<retirement-id>/{instances,moves}/<relative key> |
| + parked/<incarnation>/<host>/<retirement-id>/{instances,moves}/<relative key>@<source versionId> |
| The moves spec's equivalent is `superseded/<op>/<host>/<retirement-id>/…`. |
| A manifest belongs to exactly one retirement event and is never reused. |
| @@ -338,10 +368,12 @@ A manifest belongs to exactly one retirement event and is never reused. |
| (`ListObjectVersions`). From that listing, take every current version |
| except the live `lock.json`. A coordination lock is never data and |
| never enters a manifest (J-N6). |
| -3. **Copy** each current version by `versionId` to the destination. |
| -4. **Write the manifest last.** It records each entry's source key, |
| - source version id, size, and destination key and version. A manifest |
| - that already exists is never rewritten. |
| +3. **Copy** each current version by `versionId` to its version-keyed |
| + destination. **Skip any destination that already exists**, so progress |
| + accumulates across retries (CC2). |
| +4. **Write the manifest only once every copy exists.** It records each |
| + entry's source key, source version id, size, and destination key and |
| + version. A manifest that already exists is never rewritten. |
| 5. **Delete** every version of each manifest key whose version id is in |
| the snapshot, **by version id**. That includes noncurrent versions, so |
| deleting the current one cannot resurrect an older one. A version that |
| @@ -350,7 +382,28 @@ A manifest belongs to exactly one retirement event and is never reused. |
| 6. **Release** this worker's own `lock.json` version, conditionally, after |
| the obligation's completion CAS. |
| 7. **Retry:** if the manifest exists, go straight to deletes of its |
| - recorded versions. If it doesn't, start again from step 2. |
| + recorded versions. If it doesn't, re-list (step 2) and continue. The |
| + copies already made are kept, because their destinations are keyed by |
| + version. |
| + |
| +**The parker's own lock (CC3).** Its own `lock.json` is renewed while it |
| +works, so it is excluded everywhere, not only from the snapshot: from the |
| +emptiness check, from the horizon re-listing (§6.2a) and from manifest |
| +completeness. |
| + |
| +### 6.2a The late-completion horizon (CC1) |
| + |
| +`H` = S3's signature-age limit (15 minutes) plus the longest request the |
| +platform issues. A retirement acknowledges only after a **verification |
| +listing taken later than `evidence time + H`**, where evidence time is the |
| +moment its stop evidence (§6.1) was established. Anything that listing |
| +finds goes into a further retirement event of the same obligation, with |
| +its own retirement id and manifest, and the verification repeats. |
| + |
| +On acknowledging, the owner CASes the claim's `quiet_after[region]` to at |
| +least `evidence time + H`. Any install into that region's host namespace |
| +waits until `quiet_after` has passed: a create's first wake, a move's |
| +landing, a push. This holds even after `free`. |
| IAM: the box needs `s3:ListBucketVersions`, `s3:GetObjectVersion` and |
| `s3:DeleteObjectVersion` on its own data bucket. Today it has only |
| @@ -432,6 +485,12 @@ While a host is under any operation, each participant box must hold an |
| - If it cannot renew before `expires`, the box **self-fences**: it kills |
| the host's process tree using the cleanup-only operation (§6.1) and |
| refuses admission until it can read the claim again. |
| +- **A fresh read that shows no operation, or shows this box is not a |
| + participant, ends the self-fence (CC9).** The box deletes its local |
| + execution-lease state. A stale local file must never keep a box fenced. |
| +- The lease is for **liveness only**. A whole-VM pause also stops the |
| + watchdog, and on resume the app can write before the watchdog fires. |
| + The lease is therefore never proof that a box has stopped (CC5). |
| - An operation does not leave its first phase until every participant has |
| written its execution lease. That is how the operation knows each |
| participant has seen it. |
| @@ -444,20 +503,29 @@ The move form, `carlos move resolve --declare-lost`, delegates to this |
| command and keeps the move spec's restrictions: before commit only, the |
| exact participant, the source refused, and loss confirmed explicitly. |
| -The command: |
| +The command **requires compute fencing, and nothing else (CC5)**. The |
| +operator supplies the box's instance id, and the CLI verifies through the |
| +cloud API, with the operator's own credentials, that the instance is |
| +`stopped` or `terminated`. The console never holds EC2 rights. Lease |
| +expiry alone is never accepted. |
| + |
| +Two states it must also cover: |
| -- refuses unless the box's execution lease has passed its expiry plus a |
| - 60-second margin; |
| -- or, if the box never wrote one, refuses unless the operator supplies |
| - compute-fencing evidence that the CLI verifies through the cloud API, |
| - using the operator's own credentials. The console never holds EC2 |
| - rights. For example, the instance must be `stopped` or `terminated`. |
| +- **A target that released dirty and was destroyed** before its writes |
| + were returned. Its unreturned data is declared lost explicitly, and the |
| + confirmation names the operation and phase. |
| +- **A destroyed box that owes only `park-local` chores**, which is legal |
| + after a commit. Declaring it lost removes those chores, because its |
| + local disk is gone with it. |
| Only then does it remove the box's obligations and execution authority. |
| It adds the box to `lost`, a quarantine list that survives the |
| operation's release. A box on `lost` is refused admission for any host |
| until its old state has been retired and an operator removes it with |
| -`--readmit`. |
| +`--readmit`. **The returning box retires its own state (CC12).** On |
| +start, before anything else, it checks the claims of every host in its |
| +local inventory. For each host where it is on `lost`, it runs local |
| +retirement (§6.3) under the host guard. Only then can it be readmitted. |
| **Cost.** This adds one renewal write per participant per 20 seconds, |
| only while an operation is running. A host that is simply serving holds |
| @@ -478,8 +546,16 @@ traffic. |
| Claims are listed only by the recovery pass, never on a hot path. |
| +**A stale hold (CC10).** Reconcile releases a held row whose `hold_op` is |
| +not the claim's current operation, on the box the claim names as executor |
| +of a `serving` host. |
| + |
| ## 9. Legacy hosts (R2, J-N5) |
| +**One adoption routine (CC8).** There is a single `claim.Adopt(host)`, |
| +discovery included. Every adopting actor calls it: reconcile, the doors, |
| +purge (§5.3 step 1a) and the recovery pass. |
| + |
| A host that exists before this release gets a claim from the first actor |
| that needs one. That claim is written create-only, with: |
| @@ -488,8 +564,15 @@ that needs one. That claim is written create-only, with: |
| - `touched.regions` set to the record's region; |
| - `touched.boxes` set to the box, if it has local state. |
| -Because `complete` is false, a delete parks **every** region and **every** |
| -box of the deployment (§5.2 step 3). An adopted host cannot be reused |
| +**Discovery at adoption (CC4).** The adoption CAS also adds a |
| +`park-replica` obligation for every deployment region other than the |
| +record's. Data there cannot be the live lineage. Each region's owner parks |
| +it (§6.2, §6.2a). `touched.complete` becomes true once they all |
| +acknowledge, so an adopted host stops carrying another region's residue |
| +while it serves. |
| + |
| +As a fallback, while `complete` is still false, a delete parks **every** |
| +region and **every** box of the deployment (§5.2 step 3). An adopted host cannot be reused |
| until all of them have acknowledged, even when they have nothing to park. |
| A create on a host with no claim and no record goes through the #199 |
| @@ -559,3 +642,11 @@ the model catches it. |
| | J-N12 | §10 | |
| | R3-12 | §5.1, §2 `retired_incarnations` | |
| | J-N2 (moves side), N11, N13, N14, N15 | move-any-app | |
| +| CC1 | C3, §2 `quiet_after`, §6.2a | |
| +| CC2, CC3 | §6.2 | |
| +| CC4, CC8 | §9 | |
| +| CC5, CC9, CC12 | §7 | |
| +| CC6, CC7 | §5.3 | |
| +| CC10 | §8 | |
| +| CC11 | §4 | |
| +| CC13 | §6.1 | |