amadan
spec: host lifecycle claim rev 6.22, joint round 13 (R13-1 to R13-3)
The unfinished run's walk passes over covered foreign links and refuses a covered local baseline; coverage stated as exactly four mechanisms; the publication walk visits every entry and warm entries are born covered; the warm-region rule stands (round 13 note 4); multiple declarations' representation and alerts made operative.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+61
−20
docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md+61 −20
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 4e41480d7..483b88c2b 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.21**. Joint rounds 6 and 7 judged the claim ready for primitive planning. Rev |
| +Design, 2026-10-06, **rev 6.22**. 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 |
| @@ -16,7 +16,9 @@ planning the park engine. Rev 6.16 states what a box reference is |
| 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.20 refines proposed §7.3 after |
| Plan 8's review. Rev 6.21 answers the moves spec's rev 7.13 notes in the |
| -operative §6.4a subsection. Rev 6.9 answered |
| +operative §6.4a subsection. Rev 6.22 answers joint round 13 (R13-1 to |
| +R13-3): the run walk across regions, coverage stated completely, the |
| +publication walk over every entry, and the declaration representation. 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 |
| @@ -1149,10 +1151,22 @@ A chore retiring a superseded generation is queued only after |
| **Marker and claim disagreements.** If `holder.generation` is ahead of |
| `generation.json` and the marker names the start of an unfinished run |
| recorded in `holder.admissions` (the chain of predecessors from |
| -`holder.generation` back reaches the marker's generation through |
| -uncovered entries), that is the normal unfinished state. Protect every |
| -generation in the run, and raise no alert. Any other disagreement means |
| -touch nothing in that location, and alert. |
| +`holder.generation` back reaches the marker's generation), that is the |
| +normal unfinished state. Protect every generation in the run, and raise |
| +no alert. Any other disagreement means touch nothing in that location, |
| +and alert. |
| + |
| +**Walking the run in one region's bucket (R13-1).** The walk follows |
| +each entry's `predecessor` back from `holder.generation` to the |
| +marker's generation. A link whose generation keeps its objects in |
| +**another region** is passed over, covered or not: it holds nothing in |
| +this bucket, and its own region's park retires it (a clean return's |
| +fresh source admission after the target's park was queued walks R, then |
| +the target's T in the other region, then the source's S). A link **in |
| +this region** must be uncovered: a covered local generation is retired |
| +or being retired here, so reaching one as a needed baseline refuses, and |
| +alerts. Only this region's generations in the run are part of this |
| +bucket's live set. |
| **What a sweep never touches (Q3, R4-3).** This spec owns the sweep, so |
| it owns this rule. The **live set** is the triple |
| @@ -1524,13 +1538,10 @@ reached, and where their wording differs, this text wins. |
| (or, for the first entry, the holder's generation and the |
| caller-supplied region of its objects, `""` when it holds none, as |
| after a create). `region` is where the new writer's generation keeps |
| - its objects: the admitted box's region, for a warm admission too (a |
| - clean return's warm re-admission is on the source, in the source's |
| - region, while its predecessor record is the target's; moves 7.13 |
| - note 4). An entry is **born covered** when the claim already holds a |
| - `park-replica` of the whole location in its `predecessor_region`, |
| - because that park retires the predecessor (a rollback's return |
| - admission after the release queued the target region's park; note 2). |
| + its objects. A warm admission continues the same generation in the |
| + same region, so its region equals its predecessor record's region (a |
| + clean return's first admission is cold: an old source certificate |
| + does not certify the target's session, R13 note 4). |
| 2. **Coverage** says how the predecessor's writes are accounted for: |
| - `sealed`: a seal built from the stopped database (`from_db`) |
| covers the predecessor's last acknowledged position (a move's |
| @@ -1541,13 +1552,21 @@ reached, and where their wording differs, this text wins. |
| which no declared-lost box ended. It speaks for two sessions only: |
| the target's probe session and the source's cut session. |
| - `""`: anything else. Without a certificate it records |
| - `writes_lost`. A return the console released because the target is |
| + `writes_lost` (the predecessor). A return the console released because the target is |
| lost is `""`, and it declares **every target session since the |
| cut** (each record with `box` = the target and `session` > |
| `cut.session`, certified or not, because no return lane carries |
| their writes), in `additional_writes_lost` beside the ordinary |
| - `writes_lost`, each alerted; when `src_covered` is false the |
| - source's cut session is declared too (moves 7.13 note 7). |
| + `writes_lost`; when `src_covered` is false the source's cut session |
| + is declared there too (moves 7.13 note 7, R13-3). **Representation:** |
| + the same admission entry carries `writes_lost` (one) and |
| + `additional_writes_lost` (a list), each `{box, generation, session, |
| + remote_max_txid}`, unique by `(box, session)`; the caller supplies |
| + the list, the library records it in the admitting CAS. **Alerts:** |
| + the admitting box raises one alert per declaration after the CAS |
| + succeeds, and retries until delivered; the console's durable loss |
| + record (proposed §7.3 D4) is the long-term copy, so trimming a |
| + covered entry never loses a declaration. |
| 3. **The baseline** of a cold admission is the predecessor |
| generation's remote, as far as it goes, with two cases. A prepared |
| generation (built by a landing, a push or a dirty rollback from a |
| @@ -1555,7 +1574,9 @@ reached, and where their wording differs, this text wins. |
| snapshot in the admitting box's region, and is opened at most once, |
| so a restarted probe takes a fresh generation restored from it. In |
| an unfinished run the baseline is the newest generation in the run |
| - that holds an object, else the marker's generation. Emptiness is |
| + that holds an object in this region, else the marker's generation, |
| + walked as §6.2a says (a covered foreign link is passed over; a covered |
| + local baseline refuses). Emptiness is |
| judged by a complete paginated listing; a listing error means |
| refuse. An empty generation that is not part of an unfinished run is |
| unexplained missing data: refuse, and alert. |
| @@ -1566,10 +1587,30 @@ reached, and where their wording differs, this text wins. |
| dirty return take a new stamp. A clean return may set |
| `holder.generation` back to the source's generation, with the |
| source's stamp, in one CAS that leaves `holder.session` alone. |
| -5. **Publication.** After a writer's marker publishes its generation, |
| +5. **Coverage, completely (R13-2).** An entry becomes covered in exactly |
| + four ways, and no other transition covers anything: |
| + - **at birth:** a warm entry (its predecessor is its own generation, |
| + which nothing retires); or an entry admitted while the claim holds |
| + a `park-replica` of the whole location in its `predecessor_region` |
| + (that park retires the predecessor; a rollback's return admitted |
| + after the release queued the target region's park, moves 7.13 note 2); |
| + - **by publication** (below); |
| + - **by `CoverRegionPredecessors(op, phase, region)`** in one of the |
| + three CASes that queue a whole-location park of `region` (item 6): |
| + every uncovered entry whose `predecessor_region` is `region`; |
| + - **by `CoverParkedPredecessors(op, phase, region, generations)`** in |
| + the CAS that queues an at-rest park-sweep and in the CAS that |
| + acknowledges it: only the uncovered entries whose |
| + `predecessor_region` is `region` and whose predecessor is one of the |
| + listed generations, the ones that sweep actually retires (or retired |
| + on the way). A sweep never covers a predecessor it did not park. |
| + |
| + **Publication.** After a writer's marker publishes its generation, |
| one `PublishGeneration(observedOpID, observedPhase, observedSession, |
| - publishedGeneration, region)` CAS walks the uncovered entries up to |
| - and including the published one: |
| + publishedGeneration, region)` CAS requires `holder.generation` to be |
| + the published generation and an entry to name it, then walks **every** |
| + entry of `holder.admissions` in order (bounded by the list's length), |
| + skipping covered ones, so it visits every uncovered cold entry: |
| - predecessor is the active generation: left **uncovered**, no chore |
| (the publication that later supersedes that generation queues its |
| chore; covering it here left it unretired once a later admission |