amadan
spec: host lifecycle claim rev 3.1, CC14 sign-before-safeuntil for the staging-work lease
Correctness depends on the clock/pause assumption for the staging-work lease; SafeUntil is checked before every request signature.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+24
−5
docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md+24 −5
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 492396baf..2f79d7115 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 3**. A small primitive cited by: |
| +Design, 2026-10-02, **rev 3.1** (rev 3 plus CC14). A small primitive cited by: |
| - **#199**, deleting an instance and parking its data: |
| `2026-10-02-replica-ownership-design.md`, which this spec supersedes |
| @@ -180,10 +180,28 @@ horizon (§6.2a), and an install waits for the region's `quiet_after`. |
| participants can reach it (J-D4). The moves spec owns staging |
| sealing and draining. |
| -The clock and pause assumption of rev 1 §3.1 remains, but only for |
| -**liveness**: a worker that cannot renew stops. Correctness no longer |
| -depends on it, because every destructive request is bound to an exact |
| -version. |
| +The clock and pause assumption of rev 1 §3.1 remains. For most |
| +storage it matters only for **liveness**: a worker that cannot renew |
| +stops, and correctness doesn't depend on the assumption, because every |
| +destructive request is bound to an exact version. |
| + |
| +**One exception: the staging-work lease (CC14).** A cross-region staging |
| +round writes **new** objects. They aren't version-bound deletes, and the |
| +staging cleanup cannot name them in advance. A round that pauses past its |
| +lease and then signs its writes can land data after the cleanup finished: |
| +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; |
| +- never sign a staging write at or after `SafeUntil`. |
| + |
| +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 |
| +calls this its third staging rule (rev 5 §7.3). The joint model fails 156 |
| +of 30,000 seeds without it. |
| **C4. Fresh admission.** Admission reads the claim directly, never from a |
| listing snapshot. Admission checks happen at: |
| @@ -650,6 +668,7 @@ the model catches it. |
| | CC10 | §8 | |
| | CC11 | §4 | |
| | CC13 | §6.1 | |
| +| CC14 | C3, the staging-work lease exception | |
| ## 13. S3 behaviour this relies on, verified |