amadan
spec: host lifecycle claim rev 6.9.1, the moves session's rev 7.10 readings
Empty-generation predecessor; prepared generations opened once; cold keeps the stamp only when no writer since it was issued; the return CAS may name the source generation; no writes_lost when a seal covers the predecessor; writer start is local; library binds admission directly.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+46
−1
docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md+46 −1
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 88ba25161..783918693 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-04, **rev 6.9**. Joint rounds 6 and 7 judged the claim ready for primitive planning. Rev |
| +Design, 2026-10-05, **rev 6.9.1** (rev 6.9 plus answers to the moves session's rev 7.10 readings). 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.9 answers joint round 9 |
| @@ -995,6 +995,51 @@ It records this in its journal entry, and the admitting box raises an |
| alert. `holder.writer_box` makes the box known even when the operation |
| that admitted the crashed writer has since been replaced (R9-2). |
| +#### Readings settled with the moves spec (rev 7.10) |
| + |
| +These are the rulings on the moves spec's rev 7.10 readings: |
| + |
| +1. **The predecessor to restore from** is the observed `holder.generation`. |
| + The exception: when a complete, paginated listing shows that |
| + generation holds no file at all, because a writer died between its CAS |
| + and its first upload. The baseline is then the nearest ancestor that |
| + holds a file, the one `generation.json` names. A listing error means |
| + refuse, never "empty". |
| +2. **A prepared generation**, built by a landing, a push or a dirty |
| + rollback from a sealed archive before any writer exists, may be named |
| + as a cold admission's new generation. Its baseline is its own pinned |
| + snapshot, in the admitting box's region. It is **opened at most once**. |
| + A restarted probe takes a fresh generation, restored from it. |
| +3. **Stamps on cold admission.** A cold admission issues a new stamp, |
| + **except** when no writer has been admitted since the current stamp |
| + was issued (`holder.stamp > holder.session`). In that case it may keep |
| + the stamp, because the installation it opens has never had a writer: |
| + for example, a landing's first probe after the flip. A restarted probe, |
| + a push's prepared generation and a dirty return all take a new stamp. |
| +4. **A clean rollback's return** may set `holder.generation` back to the |
| + source's generation, recorded at the flip, in the same CAS that writes |
| + the source's stamp (rev 6.5). It never touches `holder.session`. The |
| + source's writer is then admitted like any other, cold unless the |
| + generation is certified. |
| +5. **`writes_lost`** is recorded only when the new writer's baseline does |
| + not cover the predecessor's last acknowledged position. A cold |
| + admission whose baseline is a seal of the stopped predecessor, as at a |
| + move's landing, records **no** `writes_lost` and raises no alert. Its |
| + journal entry says `baseline: sealed`. |
| +6. **A writer's start is local bookkeeping** after its admission. |
| + Retrying an unacknowledged PUT within the same session needs no claim |
| + transition, and close eligibility (R8-5) accounts for every attempt. A |
| + box that recognises its own earlier session in `holder.writer_box` may |
| + use that **only** to choose its baseline (item 1). It never skips |
| + admission, and a new process is always a new session. |
| +7. **The library binds admission to `op.id`, phase and kind directly**, |
| + with no general C2 helper, and tests the stale-closure-during-delete |
| + case directly. |
| + |
| +The library will add `KeepStamp` (item 3, enforcing |
| +`holder.stamp > holder.session`) and `BaselineCoversPredecessor` (item 5) |
| +to `Admission`, together with joint round 10's findings. |
| + |
| #### Empty bootstrap (R8-3) |
| The first writer after a create, or after an adoption with nothing |