amadan
spec: host lifecycle claim rev 6.13, the moves spec's rev 7.12 notes
Coverage is per region: admissions record region and predecessor_region; PublishGeneration covers and queues only its own region's predecessors, a foreign one stays uncovered until its region publishes or CoverRegionPredecessors runs in that region's whole-location park CAS. A lost-target return is not clean-return; a probe never marks the host failed; chore ids are opaque.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+58
−9
docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md+58 −9
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 efd0f48fe..a3d8763e9 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,11 +1,12 @@ |
| # The host lifecycle claim |
| -Design, 2026-10-05, **rev 6.12**. Joint rounds 6 and 7 judged the claim ready for primitive planning. Rev |
| +Design, 2026-10-05, **rev 6.13**. 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 |
| (R10-1, R10-2, R10-4, R10-5). Rev 6.11 answers the moves spec's rev 7.11 |
| -notes. Rev 6.12 answers joint round 11 (R11-2 to R11-5). Rev 6.9 answered |
| +notes. Rev 6.12 answers joint round 11 (R11-2 to R11-5). Rev 6.13 |
| +answers the moves spec's rev 7.12 notes (coverage is per region). 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 |
| @@ -102,7 +103,8 @@ replaced whole with conditional writes (`If-Match` on the ETag read). |
| "stamp": 41, |
| "session": 57, |
| "writer_box": "adi-knitting", |
| - "admissions": [{"session": 57, "generation": "g…", "predecessor": "g…", |
| + "admissions": [{"session": 57, "generation": "g…", "region": "eu-west-1", |
| + "predecessor": "g…", "predecessor_region": "eu-west-1", |
| "mode": "cold", "covered": false}] |
| }, |
| "op": { |
| @@ -181,9 +183,12 @@ Field rules: |
| is not yet finished, or whose predecessors are not yet queued for |
| retirement (rev 7.11 notes 3 and 4). It lives in the holder, so it |
| survives every operation transition, release and new operation. Each |
| - entry is `{session, generation, predecessor, mode, covered, |
| - writes_lost?}`. Entries are trimmed once covered, keeping at most the |
| - last 8. |
| + entry is `{session, generation, region, predecessor, |
| + predecessor_region, mode, covered, writes_lost?}`. `region` is where |
| + the entry's generation keeps its objects; `predecessor_region` is where |
| + the predecessor's are (`""`: it holds none anywhere). Entries are |
| + trimmed once covered, keeping at most the last 8; an uncovered entry is |
| + never trimmed (rev 7.12 note 5). |
| - **`holder.writer_box`** is the box admitted as that session's writer |
| (§6.4a). It lives in the holder, not only in an operation's journal, so |
| it survives an operation being replaced (R9-2). |
| @@ -1051,12 +1056,55 @@ 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.12) |
| + |
| +1. **A return made clean by a declared-lost target is not |
| + `clean-return`.** Coverage `clean-return` needs a target that gave |
| + its evidence: the dirty flag known and clear, `src_covered`, and no |
| + declared-lost box. When the console releases a return because the |
| + target is lost, the target's session is uncovered: the admission's |
| + coverage is `""` and it records `writes_lost` for the target's |
| + session (and the second `writes_lost` for the source's cut session |
| + when `src_covered` is false, rev 7.11 reading 8). Agreed. |
| +2. **A probe never marks the host failed.** Rev 7.11 reading 1's |
| + failed-host marking belongs to a serving wake. One probe attempt is |
| + one cold admission; its five app restarts share the attempt's 30 s |
| + readiness window; the fifth failure or the end of the window ends the |
| + attempt, and the operation counts one of its three budgeted attempts. |
| + Agreed as the moves spec states it. |
| +3. **Chore ids.** `PublishGeneration` calls `newID` once for each chore's |
| + id and once for each chore's retirement id. Ids are opaque and never |
| + parsed; the model may name them as it likes, provided they are |
| + distinct. |
| +4. **`clean-return` speaks for two sessions only:** the target's probe |
| + session and the source's cut session (`cut.session`). Any later |
| + session that dies uncertified is declared like any other. Agreed. |
| +5. **Coverage is per region.** Each admission records its own region and |
| + its predecessor's region (above). `PublishGeneration(…, region)`, for |
| + each uncovered entry up to the published generation: |
| + - a predecessor that is the active generation: covered, no chore; |
| + - a predecessor holding no objects (`predecessor_region` `""`): |
| + covered, no chore; |
| + - a predecessor in `region`: one deduplicated `park-generation` chore |
| + in `region`, covered; |
| + - a predecessor in another region: **left uncovered**, no chore, and |
| + the walk continues. It is never queued into the other region from |
| + here, because a rollback may still need it. |
| + |
| + An uncovered foreign-region entry is covered either by that region's |
| + own next `PublishGeneration`, or by `CoverRegionPredecessors(op, |
| + phase, region)` composed into the CAS that queues that region's |
| + park of the whole location (a committed move's source cleanup), which |
| + retires those generations wholesale. A warm admission stays in its |
| + predecessor's region. Reading 4 of rev 7.11 below is amended to match. |
| + |
| #### Readings settled with the moves spec (rev 7.11) |
| 1. **Retry limit:** five start attempts within one session, with doubling |
| backoff (1, 2, 4, 8, 16). A start the environment isn't ready for waits |
| - without counting an attempt. At the fifth failure the box marks the |
| - host failed and creates no session until an operator or a health |
| + without counting an attempt. At the fifth failure of a **serving |
| + wake** the box marks the host failed (a probe never does, rev 7.12 |
| + reading 2) and creates no session until an operator or a health |
| signal clears it. Confirmed. |
| 2. **A chain of unfinished admissions.** The unfinished state covers a |
| **run** of admissions, each of which died before its generation's |
| @@ -1095,7 +1143,8 @@ that admitted the crashed writer has since been replaced (R9-2). |
| and including `publishedGeneration` as covered, and queues a |
| `park-generation` chore (op `session:<n>`) for every predecessor |
| generation in that chain other than `publishedGeneration`, without |
| - duplicates. A writer that dies after its marker landed but before this |
| + duplicates, **in its own region only** (rev 7.12 reading 5: a |
| + predecessor in another region stays uncovered). A writer that dies after its marker landed but before this |
| CAS leaves entries uncovered. The next admission's `PublishGeneration` |
| covers them. This replaces `QueueGenerationRetire`. |
| 5. **A clean rollback** returns the source to its own generation **only |