amadan
spec: host lifecycle claim rev 5, CC15-CC19 from the strict joint model
At-rest sweep owns late completions; create registrations are leases drained only when expired and unnamed by the claim; retired-incarnation records are orphans whenever they land; holder.generation in the schema; staging writes signed once at the deadline check with SafeUntil = Until - skew - 15m.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+59
−8
docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md+59 −8
CI passed — 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 7bcf696ab..cb2597a7c 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-03, **rev 4**. A small primitive cited by: |
| +Design, 2026-10-03, **rev 5**. 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,7 +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 4** answers the claim-side findings of joint round 2 |
| +**Rev 5** folds in CC15 to CC19, required by the strict joint model |
| +(47e65af8, moves rev 6 at 7ac666fe). |
| + |
| +**Rev 4** answered the claim-side findings of joint round 2 |
| (`CODEX-FINDINGS-JOINT-R2.md`, cited `J2-…`): R2-1, R2-2, R2-3, R2-4, |
| R2-6, R2-7, and the legacy local-coverage gap noted under N5. |
| @@ -71,7 +74,8 @@ replaced whole with conditional writes (`If-Match` on the ETag read). |
| "key": "apps/bab/jam/instances/shop.bab.oncarlos.com.json", |
| "account": "bab", "app": "jam", "name": "", |
| "incarnation": "<hex>", "created_at": "<record CreatedAt>", |
| - "location": "instances/shop.bab.oncarlos.com/<incarnation>" |
| + "location": "instances/shop.bab.oncarlos.com/<incarnation>", |
| + "generation": "<op id of the installed generation, or \"\">" |
| }, |
| "op": { |
| "kind": "serving", |
| @@ -115,6 +119,10 @@ Field rules: |
| set and never changes while that holder holds the host. Same-incarnation |
| generations within it (moves, push) are the moves spec's, scoped by |
| operation id. |
| +- **`holder.generation`** names the installed generation within |
| + `holder.location` (CC18). The moves spec owns its values and its |
| + markers. Its start check compares this field with all three of its |
| + markers. |
| - **`op.intent`** holds the operation's reconstruction inputs. It is |
| written in the **same CAS** that starts the operation, before any other |
| object is touched (J-N4). |
| @@ -209,10 +217,18 @@ in the serving region, or in a region the instance has left. So, for the |
| staging-work lease, **correctness does depend on the clock and pause |
| assumption**, and the rule is: |
| -- check the staging-work lease's `SafeUntil` immediately before **every |
| - request signature**, not only at the start of a round; |
| +- `SafeUntil = Until − max clock skew − 15 minutes`, where `Until` is the |
| + lease's expiry (CC19); |
| +- **sign each staging request at the moment of the deadline check**, in |
| + the same step, and send that signature. **Never re-sign**: the SDK's |
| + automatic retry must not refresh the signature; |
| - never sign a staging write at or after `SafeUntil`. |
| +A box frozen between a passed check and the send then holds a signature |
| +S3 refuses once 15 minutes have passed. Because `SafeUntil` already |
| +subtracts those 15 minutes and the skew, any request S3 accepts was |
| +accepted before the lease expired. |
| + |
| Combined with S3's 15-minute signature-age limit (§13 row 8), a write |
| signed before `SafeUntil` either lands within that bound or is refused. |
| The staging cleanup's horizon (§6.2a) covers that bound. The moves spec |
| @@ -297,8 +313,10 @@ new operation will write (CC11). A pending chore there must finish first. |
| ### 5.1 Create (R3-12, J-N4) |
| 0. **App admission (J2-R2-2).** Register the create in |
| - `apps/<acct>/<app>/admission.json` with a CAS, as `{create id, host}`, |
| - which succeeds only while the app's admission is `open`. The |
| + `apps/<acct>/<app>/admission.json` with a CAS, as `{create id, host, |
| + expires}`, which succeeds only while the app's admission is `open`. |
| + **A registration is a lease (CC16):** the creating console renews it |
| + until the create reaches `serving` or is cancelled. The |
| registration is removed when the create reaches `serving` or is |
| cancelled. |
| 1. The console assigns `CreatedAt` = now (UTC, nanoseconds). A caller |
| @@ -320,6 +338,13 @@ new operation will write (CC11). A pending chore there must finish first. |
| anyway is an **orphan**. It is never admitted (C1). The pass |
| deletes it with `DeleteIfMatch` when its incarnation matches a |
| `cancelled_creates` entry, and retries until `until` (J2-R2-7); |
| + - **orphans whenever they land (CC17):** a record whose incarnation is |
| + in `retired_incarnations`, or is not the claim's holder, is an |
| + orphan at any time, not only inside the `cancelled_creates` |
| + window. A create that finds its record key occupied by one |
| + removes it with `DeleteIfMatch`, then retries its create-only |
| + write. The pass removes any it meets. A late record write after |
| + the window therefore never blocks a later recreate; |
| - anything else: wait. |
| ### 5.2 Delete and park (#199) |
| @@ -369,7 +394,14 @@ site now uses: |
| host set is then the app's records **plus** every host still |
| registered as an in-flight create. Purge waits for each registered |
| create to reach `serving` (then it is purged like the others) or to be |
| - cancelled by recovery, before fixing its host set. This is tested with |
| + cancelled by recovery, before fixing its host set. **The drain |
| + removes a registration only when it has expired *and* its host's |
| + claim does not name that create (CC16).** A claim that names it |
| + means the create already holds the host, so purge handles that host |
| + like any other. Expiry alone is not enough: dropping such a |
| + registration would let purge tear down a store the create already |
| + uses. A crashed console's registration therefore expires and drains, |
| + and does not block every purge. This is tested with |
| at least two hosts. |
| 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 |
| @@ -478,6 +510,20 @@ 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. |
| +**Requests that complete after `H` (CC15).** C3a makes a very late |
| +completion harmless to a successor, but it still leaves residue, and it |
| +needs an owner. Each region's box runs an **at-rest sweep**: for every |
| +host it can see in its bucket that has no operation running. It lists: |
| + |
| +- the location of every incarnation in that host's |
| + `retired_incarnations`; |
| +- every generation within the live `holder.location` other than |
| + `holder.generation` (the moves spec's dead generations). |
| + |
| +Anything found is parked as a further retirement event (§6.2), under a |
| +new obligation the sweeping box owns. A freed host's location never |
| +keeps late residue for good. |
| + |
| 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 |
| @@ -766,6 +812,11 @@ the model catches it. |
| | J2-R2-6 | §6.2 | |
| | J2-R2-7 | §5.1 step 5, §2 `cancelled_creates` | |
| | J2 N5 note | §9 | |
| +| CC15 | §6.2a at-rest sweep | |
| +| CC16 | §5.1 step 0, §5.3 step 1b | |
| +| CC17 | §5.1 step 5 | |
| +| CC18 | §2 `holder.generation` | |
| +| CC19 | C3, the staging-work lease exception | |
| ## 13. S3 behaviour this relies on, verified |