amadan
spec: host lifecycle claim rev 6.1, answers to the moves session's questions
Q1: installations ordered by claim gen (markers store the retiring CAS's gen; writers carry their validated gen). Q2: a record with no claim is legacy, adopted, never an orphan. Q3: the claim owns the sweep's never-touch rule for the live generation and the version generation.json names.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+35
−7
docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md+35 −7
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 e3dca66ac..cbb26c626 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-03, **rev 6**. A small primitive cited by: |
| +Design, 2026-10-03, **rev 6.1** (rev 6 plus answers to the moves session's three questions). A small primitive cited by: |
| - **#199**, deleting an instance and parking its data: |
| `2026-10-02-replica-ownership-design.md`, which this spec supersedes |
| @@ -355,6 +355,11 @@ new operation will write (CC11). A pending chore there must finish first. |
| in `retired_incarnations`, or is not the claim's holder, is an |
| orphan at any time, not only inside the `cancelled_creates` |
| window. |
| + - **A record with no claim object is not an orphan (Q2).** Under C5a, |
| + a claim object is never deleted, so an absent claim means the host |
| + has never had one. Such a record is a **legacy** host, adopted |
| + through `claim.Adopt` (§9). The orphan rules below assume a claim |
| + exists. |
| - **How an orphan is established (R3-2).** The order is fixed. |
| 1. Read the record, keeping its ETag `E` and incarnation `I`. |
| 2. Read the claim **afterwards**, fresh. |
| @@ -593,7 +598,22 @@ So the sweep lists: |
| `holder.generation` (the moves spec's dead generations). |
| Anything found is parked as a further retirement event (§6.2), under a |
| -new obligation the sweeping box owns. A freed host's location never |
| +new obligation the sweeping box owns. |
| + |
| +**What a sweep never touches (Q3).** This spec owns the sweep, so it |
| +owns this rule: |
| +- the sweep never parks or deletes anything in the live |
| + `holder.location` that belongs to `holder.generation`; |
| +- in particular, it never parks or deletes the S3 object version that |
| + the moves spec's generation marker (`generation.json`) names as |
| + current; |
| +- the marker itself is never residue. |
| + |
| +The marker's format and its If-Match write rules are the moves spec's |
| +(rev 7.4 §6.4). The sweep reads the marker under the same fresh claim |
| +observation it uses to decide what is live. If the marker and |
| +`holder.generation` disagree, the sweep touches nothing in that location |
| +and raises an alert. A freed host's location never |
| keeps late residue for good. |
| On acknowledging, the owner CASes the claim's `quiet_after[region]` to at |
| @@ -656,17 +676,25 @@ harmless. |
| Local retirement (§6.3) takes the same guard, then writes a retired |
| marker. **The marker is scoped to an installation, not to the whole |
| -incarnation (R3-3).** It is written as `{incarnation, op id of the |
| -installation being retired}`, and it refuses any writer carrying that |
| -incarnation and an operation at or before the retired one. |
| +incarnation (R3-3).** It is written as `{incarnation, gen}`, where `gen` |
| +is the claim's `gen` of the CAS that retired the installation. It refuses |
| +any writer carrying that incarnation and a validated claim `gen` **at or |
| +before** it, that is `writer gen ≤ marker gen`. |
| + |
| +**Ordering, defined (Q1).** Operations are ordered by the claim's `gen`. |
| +It is durable, and strictly increasing per host, because every claim |
| +write increments it (§2). Op ids stay opaque, unique names and are |
| +never compared. Every host-state writer carries the claim `gen` it |
| +validated under, from its fresh read under the guard. |
| A later **new installation** of the same incarnation on this box replaces |
| the marker. A move back to a region the instance left is one example. |
| The replacement happens under the guard, conditional on a fresh claim |
| read showing that the new operation is current and that `op.exec`, or |
| the landing participant, is this box. The marker then reads |
| -`{incarnation, new op id}`. Workers of the retired installation still |
| -carry the old op id and stay refused. The model must show a successful |
| +`{incarnation, gen of the CAS that made the new installation current}`. |
| +Workers of the retired installation validated under an earlier `gen`, |
| +and stay refused. The model must show a successful |
| non-home round trip (UK→US→UK) as an unmutated, deterministic witness. |
| A pass that selected a row before an operation began therefore either |