amadan
spec: host lifecycle claim rev 6.20, proposed §7.3 refinements from Plan 8's review
Successive declarations by strictly newer revision; local-only declarations against a serving claim; denial durable before the guard is released after an ambiguous renewal.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+9
−2
docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md+9 −2
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 f41d922c7..c2475f511 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-06, **rev 6.19**. Joint rounds 6 and 7 judged the claim ready for primitive planning. Rev |
| +Design, 2026-10-06, **rev 6.20**. Joint rounds 6 and 7 judged the claim ready for primitive planning. Rev |
| 6.5 added the R6-4 rule. Rev 6.6 added writer epochs (R7-1, amadan #225). |
| Rev 6.7 answered the moves session's notes on §6.4a. Rev 6.8 rewrote §6.4a |
| around writer sessions, for joint round 8. Rev 6.10 answers joint round 10 |
| @@ -14,7 +14,8 @@ planning the park engine. Rev 6.16 states what a box reference is |
| (amadan #212). Rev 6.17 adds the PROPOSED contracts §7.3 and §10.1 |
| (Plan 8's D1 to D7), awaiting Paul's rulings P1 to P3 and joint review. Rev 6.18 adds the |
| PROPOSED §5.9 (Plan 5's P5-D1 to P5-D6). Rev 6.19 adds the PROPOSED §6.6 |
| -(Plan 6's P6-D1 to P6-D8). Rev 6.9 answered |
| +(Plan 6's P6-D1 to P6-D8). Rev 6.20 refines proposed §7.3 after |
| +Plan 8's review. Rev 6.9 answered |
| joint round 9 |
| (R9-1 to R9-4) and takes **Paul's ruling R6 (2026-10-04): a box never |
| reuses its local database. Every writer start restores from the |
| @@ -2366,6 +2367,8 @@ The current private box report names the completion object’s digest. The conso |
| An interrupted readmission leaves the global deny active. A concurrent declaration increments the revision and defeats the older final write. An older readmission cannot remove a newer per-host quarantine entry. |
| +**Successive declarations (rev 6.20).** A box may be declared lost more than once for the same host (for example, a stopped instance first, then confirmed disk destruction). Each declaration is freshly bound and carries a strictly newer quarantine revision; it may apply only its own confirmed consequences. An older revision is refused, and a readmission bound to an older revision cannot clear a newer one. |
| + |
| Readmission grants no executor, installation stamp or writer session. Any subsequent writer uses fresh claim authority, a new admission and certified-remote restoration. A retired installation stamp cannot be reactivated through readmission. |
| A replacement machine cannot complete the old enrollment’s retirement merely by reusing its label. It receives a distinct identity/enrollment; old quarantine and retirement obligations remain attached to the original machine. |
| @@ -2481,6 +2484,10 @@ New remote retirement scopes justified by the compute fence use the declaration |
| - Validated durable target data is recovered where available. |
| - The destroyed-local-only exception may discharge exact local chores after commit without reopening data authority. |
| +**Local-only declarations against a serving claim (rev 6.20).** An adopted host returns to `serving` with an empty `op.id` while discovery `park-local` chores may remain. A destroyed-local-only declaration is then legal against the serving claim, narrowly: it binds the claim revision and each discharged chore's original operation and retirement identity, discharges only those `park-local` chores, and changes nothing else (the serving executor, `holder.stamp`, sessions and every other obligation are preserved). |
| + |
| +**Denial is durable before the guard is released (rev 6.20).** After an ambiguous lease renewal the box keeps the host guard until its denial is durable; if persisting the lost state fails, the on-disk state must still deny (it may never fail open to an older `active` record), and cleanup proceeds independently. |
| + |
| #### D6. Lease failures, local state and phase acknowledgement |
| The execution-lease wire contract remains exactly: |