amadan
spec: host lifecycle claim rev 6.21, the moves spec's rev 7.13 notes
Warm admission's region is the admitted box's; entries born covered under a pending whole-location park; a lost-target return declares every target session since the cut; a live predecessor stays uncovered; three CASes compose CoverRegionPredecessors; the sweep covers what it parks; probe limits stated.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+38
−13
docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md+38 −13
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 c2475f511..4e41480d7 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.20**. Joint rounds 6 and 7 judged the claim ready for primitive planning. Rev |
| +Design, 2026-10-06, **rev 6.21**. 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 |
| @@ -15,7 +15,8 @@ planning the park engine. Rev 6.16 states what a box reference is |
| (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.20 refines proposed §7.3 after |
| -Plan 8's review. Rev 6.9 answered |
| +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 |
| 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 |
| @@ -1523,7 +1524,13 @@ 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; a warm admission keeps its predecessor's region. |
| + 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). |
| 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 |
| @@ -1535,8 +1542,12 @@ reached, and where their wording differs, this text wins. |
| 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 |
| - lost is `""`, and when `src_covered` is false a second |
| - `writes_lost` is recorded for the source's cut session. |
| + 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). |
| 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 |
| @@ -1559,7 +1570,10 @@ reached, and where their wording differs, this text wins. |
| one `PublishGeneration(observedOpID, observedPhase, observedSession, |
| publishedGeneration, region)` CAS walks the uncovered entries up to |
| and including the published one: |
| - - predecessor is the active generation: covered, no chore; |
| + - 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 |
| + superseded it, moves 7.13 note 6); |
| - `predecessor_region` is `""` (holds no objects): covered, no chore; |
| - `predecessor_region` is `region`: one deduplicated |
| `park-generation` chore in `region` (op `op.id`, or |
| @@ -1573,15 +1587,26 @@ reached, and where their wording differs, this text wins. |
| publication. Chore ids are opaque. |
| 6. **Foreign-region predecessors** stay uncovered until that region's |
| own next publication, or until `CoverRegionPredecessors(op, phase, |
| - region)` runs inside the CAS that queues that region's park of the |
| - whole location (a committed move's source cleanup). It covers them |
| - and queues nothing, because that park retires them wholesale. They |
| - are never queued into their region from another one, because a |
| - rollback may still need them. |
| -7. **A new agent process** stops any app it finds running for a host, |
| + region)` runs inside a CAS that queues that region's park of the |
| + whole location. There are three: a committed move's source cleanup, |
| + a rollback's release of the target region, and the console's |
| + lost-target release (moves 7.13 note 1). It covers them and queues |
| + nothing, because that park retires them wholesale. They are never |
| + queued into their region from another one, because a rollback may |
| + still need them. **The at-rest sweep covers what it parks**: |
| + `CoverParkedPredecessors(op, phase, region, generations)` runs in the |
| + CAS that queues a park-sweep (predecessors with a sweepable object) |
| + and in the CAS that acknowledges it (predecessors whose objects it |
| + retired on the way); a predecessor with nothing to sweep waits for its |
| + publication's chore (note 3). |
| +7. **Probe limits** (owned by the moves spec, stated here for the |
| + library's callers): a probe attempt's deadline is checked before each |
| + start and before readiness is accepted; a recovery probe's budget is |
| + nine attempts, three times a landing's three (moves 7.13 note 5). |
| +8. **A new agent process** stops any app it finds running for a host, |
| admits a new session, and only then restarts the app. It never |
| reattaches to a unit started under a dead session. |
| -8. **Lost boxes.** A declared-lost box's timers are declared on the |
| +9. **Lost boxes.** A declared-lost box's timers are declared on the |
| console's record, and alerted. Adoption sets `holder.writer_box` to |
| the box running the pre-release process; before the first writer of |
| a new incarnation it is `""`. |