amadan
spec: host lifecycle claim rev 6.14, joint round 12 (R12-4, R12-6)
One operative rule set in §6.4a (Admissions, coverage and retirement); the readings sections become history. AdmitWriter writes holder.admissions, never op.journal; no box identity in baseline choice (R6); writes_lost identity from the last admission record; §6.2a protects an unfinished run; the retry limit is a serving wake's; trimming retention documented.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+141
−39
docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md+141 −39
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 a3d8763e9..b9d317f12 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,12 +1,14 @@ |
| # The host lifecycle claim |
| -Design, 2026-10-05, **rev 6.13**. Joint rounds 6 and 7 judged the claim ready for primitive planning. Rev |
| +Design, 2026-10-05, **rev 6.14**. 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.13 |
| -answers the moves spec's rev 7.12 notes (coverage is per region). Rev 6.9 answered |
| +answers the moves spec's rev 7.12 notes (coverage is per region). Rev |
| +6.14 answers joint round 12 (R12-4, R12-6): §6.4a now has one operative |
| +rule set, and the readings sections are history. 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 |
| @@ -186,9 +188,12 @@ Field rules: |
| 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). |
| + the predecessor's are (`""`: it holds none anywhere). Trimming |
| + drops covered entries from the **front** only, while more than 8 |
| + remain. An uncovered entry is never trimmed, and it stops trimming, so |
| + covered entries behind it are kept too. That retention is deliberately |
| + conservative: history needed for recovery is never dropped, at the |
| + cost of a longer list until the head is covered (R12-6). |
| - **`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). |
| @@ -693,20 +698,26 @@ A freed host's location never keeps late residue for good. |
| **Baselines an unfinished admission needs are protected (R10-2).** A |
| cold admission's new generation is **unfinished** until its first durable |
| -root is published, meaning `generation.json` names it. Until then: |
| -- its baseline generation, the journalled predecessor, is part of the |
| - live set; |
| -- no `park-generation` chore for the baseline may be queued, and the |
| - sweep never parks it. |
| +root is published, meaning `generation.json` names it. Admissions that |
| +die before publishing form an **unfinished run** in `holder.admissions`: |
| +each entry's predecessor is the previous entry's generation, from the |
| +generation `generation.json` names through `holder.generation` (§6.4a, |
| +"Admissions, coverage and retirement"). Until the run is published: |
| +- every generation in the run, and the marker's generation, is part of |
| + the live set; |
| +- no `park-generation` chore for any of them may be queued, and the |
| + sweep never parks them. |
| A chore retiring a superseded generation is queued only after |
| `generation.json` names `holder.generation`. |
| **Marker and claim disagreements.** If `holder.generation` is ahead of |
| -`generation.json` and the marker names the journalled predecessor of the |
| -latest admission, that is the normal unfinished state. Protect both |
| -generations, and raise no alert. Any other disagreement means touch |
| -nothing in that location, and alert. |
| +`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. |
| **What a sweep never touches (Q3, R4-3).** This spec owns the sweep, so |
| it owns this rule. The **live set** is the triple |
| @@ -920,14 +931,13 @@ issues any upload**. It requires: |
| `op.exec`. |
| It writes: |
| -- `holder.session = its own resulting gen`; |
| -- a **journal entry** in `op.journal.writers`: |
| - `{session, box, generation, stamp, mode, predecessor: {session, box, |
| - generation, stamp}}`. The predecessor is copied from the claim it |
| - observed. |
| +- `holder.session = its own resulting gen`, and `holder.writer_box = |
| + this box`; |
| +- an entry appended to **`holder.admissions`** (never to `op.journal`), |
| + as set out in "Admissions, coverage and retirement" below; |
| - in **cold** mode, a new `holder.generation` (a fresh op id) and |
| - `holder.stamp = the resulting gen`. This is an installing CAS (§2, |
| - R6-4). |
| + `holder.stamp = the resulting gen`, unless the stamp is kept (below). |
| + This is an installing CAS (§2, R6-4). |
| After a conflicting CAS, the box re-establishes its **evidence** |
| (certificate, readiness, the `op.exec` handover) before retrying. A |
| @@ -991,8 +1001,8 @@ only if `closed/<holder.session>.json` exists for the observed session, |
| and its `max_txid` equals the generation's remote maximum TXID. The |
| certificate proves every upload of that session completed, so any |
| `op.exec` box may continue the generation. The admitting box need not |
| -be the certificate's box. Which box it is decides only the baseline (see |
| -below): the local database, or a remote restore. |
| +be the certificate's box, and which box it is decides nothing: the |
| +baseline is always the remote (R6, below). |
| The admitting CAS moves `holder.session` forward, so that marker now |
| names a dead session. A delayed, replayed or re-created marker for any |
| earlier session can never authorize anything again. No marker is ever |
| @@ -1023,10 +1033,15 @@ keeps replicating, it stays within the admitted session and is not |
| re-admitted. A new agent process is always a new session. |
| **Failed-start churn is controlled by retry policy.** Start attempts |
| -within a session back off. After the moves spec's limit, the box marks |
| -the host failed and stops creating sessions for it, until an operator or |
| -a successful health signal clears it. An app's writes are never left in |
| -an interval without an admitted session. |
| +within a session back off: five attempts, doubling from 1 s (1, 2, 4, 8, |
| +16); a start the environment isn't ready for waits without counting. |
| +At the fifth failure of a **serving wake**, the box marks the host |
| +failed and stops creating sessions for it, until an operator or a |
| +successful health signal clears it. **A probe never marks the host |
| +failed:** one probe attempt is one cold admission whose five restarts |
| +share a 30 s readiness window, and its failure counts one of the |
| +operation's budgeted attempts (the moves spec owns that budget). An |
| +app's writes are never left in an interval without an admitted session. |
| #### The baseline is always the certified remote (R6, R9-1) |
| @@ -1044,19 +1059,105 @@ That removes the lineage and provenance machinery entirely. |
| **Lost writes are declared, never silent.** A writer that crashed with |
| acknowledged writes not yet uploaded loses them, because its successor |
| -starts from the remote. A **cold** admission whose observed session has |
| -no certificate records, in the same CAS: |
| +starts from the remote. A **cold** admission whose predecessor is not |
| +certified and whose coverage is `""` records, in its own admissions |
| +entry, in the same CAS: |
| - writes_lost: {box: <observed holder.writer_box>, |
| - generation: <observed holder.generation>, |
| - session: <observed holder.session>, |
| + writes_lost: {box: <predecessor's box>, |
| + generation: <predecessor's generation>, |
| + session: <predecessor's session>, |
| remote_max_txid: <the remote maximum it restores to>} |
| -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) |
| +The **predecessor** is the last entry in `holder.admissions`, never the |
| +holder's current fields (which a clean return may have reset; R11-4). |
| +Only when the list is empty does it come from the holder's own |
| +`session`, `writer_box` and `generation`. The admitting box raises an |
| +alert. Because admissions live in the holder, the box is known even when |
| +the operation that admitted the crashed writer has since been replaced |
| +(R9-2). |
| + |
| +#### Admissions, coverage and retirement (operative, rev 6.14) |
| + |
| +This subsection and the ones above are the operative rules. The |
| +readings sections after it are history: they record how each rule was |
| +reached, and where their wording differs, this text wins. |
| + |
| +1. **The entry.** Each admission appends `{session, box, generation, |
| + region, predecessor, predecessor_region, mode, coverage, covered: |
| + false, writes_lost?}` to `holder.admissions`. `predecessor` and |
| + `predecessor_region` are the last entry's `generation` and `region` |
| + (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. |
| +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 |
| + landing). No `writes_lost`. A seal built from the remote, because |
| + the disk was gone, is not `sealed` coverage. |
| + - `clean-return`: a clean rollback whose seal records `src_covered`, |
| + whose target gave its evidence (dirty flag known and clear) and |
| + 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 |
| + lost is `""`, and when `src_covered` is false a second |
| + `writes_lost` is recorded for the source's cut session. |
| +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 |
| + sealed archive, before any writer) is restored from its own pinned |
| + 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 |
| + 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. |
| +4. **Stamps.** A cold admission takes a new stamp, except when no writer |
| + has been admitted since the current stamp was issued (`holder.stamp > |
| + holder.session`), when it may keep it (a landing's first probe after |
| + the flip). A restarted probe, a push's prepared generation and a |
| + 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, |
| + 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_region` is `""` (holds no objects): covered, no chore; |
| + - `predecessor_region` is `region`: one deduplicated |
| + `park-generation` chore in `region` (op `op.id`, or |
| + `session:<holder.session>` while serving), covered; |
| + - any other region: left uncovered, no chore, and the walk goes on. |
| + |
| + It is legal wherever a writer may run, and refused in `creating`, |
| + `deleting`, `parking`, `purging` and `placing`. Retirement of a |
| + superseded generation happens only through it, or through item 6. A |
| + writer that dies before this CAS leaves its entries for the next |
| + 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, |
| + 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 |
| + 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 `""`. |
| + |
| +#### History: how the rules above were reached |
| + |
| +Everything from here to "Empty bootstrap" is the record of settled |
| +readings, newest first. It is not operative; the subsection above is. |
| + |
| +##### 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 |
| @@ -1098,7 +1199,7 @@ that admitted the crashed writer has since been replaced (R9-2). |
| 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) |
| +##### 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 |
| @@ -1167,7 +1268,7 @@ that admitted the crashed writer has since been replaced (R9-2). |
| pre-release process. Before the first writer of a new incarnation, |
| `writer_box` is `""`. |
| -#### Readings settled with the moves spec (rev 7.10) |
| +##### Readings settled with the moves spec (rev 7.10) |
| These are the rulings on the moves spec's rev 7.10 readings: |
| @@ -1485,6 +1586,7 @@ the model catches it. |
| | J4-R4-4 | §5.3 step 4 | |
| | J4-Q2 | §5.1 step 5 | |
| | J5-R5-4 | §2 `holder.stamp`, §6.4 initialization, refusal with no record, the two retirements | |
| +| J12-R12-4, R12-6; moves 7.12 notes | §6.4a one operative rule set ("Admissions, coverage and retirement"), readings marked history; §6.2a unfinished run; per-region coverage; conservative trimming documented | |
| | J10-R10-1, R10-2, R10-4, R10-5 | §6.4a: admit before app start; protect unfinished-admission baselines; refused kinds include creating; warm input empty; serving chores `session:<n>`; `@root` | |
| | J9-R9-1 to R9-4, Paul R6 | §6.4a: no local DB reuse (always the certified remote), `holder.writer_box`, `writes_lost`, two-mode admission bound to op id, phase and kind, `park-generation` | |
| | J8-R8-1 to R8-4 | §6.4a rewritten: writer sessions in the claim, per-session certificates (never deleted), admission inside any op, baseline provenance, empty bootstrap | |