amadan
spec: host lifecycle claim rev 6.2, after joint round 4
R4-2: installation stamps (claim gen captured at the CAS that made an installation current), equality with the active stamp for admission; R4-3: the sweep's live set is region-qualified, matching keys elsewhere are residue; R4-4: purge retires records under its own claim, purging->parking, never back to serving. Joint R4 findings copied unedited.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2 files changed,
+256
−40
docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md+86 −40docs/superpowers/specs/CODEX-FINDINGS-JOINT-R4.md+170 −0
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 cbb26c626..fdb16e669 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.1** (rev 6 plus answers to the moves session's three questions). A small primitive cited by: |
| +Design, 2026-10-03, **rev 6.2**. A small primitive cited by: |
| - **#199**, deleting an instance and parking its data: |
| `2026-10-02-replica-ownership-design.md`, which this spec supersedes |
| @@ -17,7 +17,11 @@ I-7, adopts its replacement for D4, and answers N1, N3 to N10, N12 and the |
| carried-forward R3-12. The moves-only findings (N2's move side, N11, N13, |
| N14, N15) are the moves spec's. §12 maps every finding to its section. |
| -**Rev 6** answers the claim side of joint round 3 |
| +**Rev 6.2** answers the claim side of joint round 4 |
| +(`CODEX-FINDINGS-JOINT-R4.md`): R4-2, the claim half of R4-3, R4-4, and |
| +Q2. |
| + |
| +**Rev 6** answered the claim side of joint round 3 |
| (`CODEX-FINDINGS-JOINT-R3.md`): R3-2, R3-3, R3-4. |
| **Rev 5** folded in CC15 to CC19, required by the strict joint model |
| @@ -468,10 +472,23 @@ site now uses: |
| 2. **CAS every host claim of the app** to `{purging, id}`, from `serving`. |
| A host under any other operation fails the purge with its reason. The |
| ones already reserved stay reserved, and the operator retries. |
| -3. **Only then** tear down stores and email, as today (ownership.go:404), |
| - then run §5.2 for each record and remove the app prefix |
| - (`PurgeApp`). |
| -4. **The boxes' auto-purge** (domains/reconcile.go:232) runs the same |
| +3. **Only then** tear down stores and email, as today (ownership.go:404). |
| +4. **Retire each record under the purge's own claim (R4-4).** §5.2's |
| + step 1 (deleting, from `serving`) does not apply, because the host |
| + is already in `purging`. Instead, for each host: |
| + 1. Record the exact record version (key and ETag) in the purge's |
| + `op.intent`. |
| + 2. `DeleteIfMatch` that version. This replays as in §5.2 step 2. |
| + 3. CAS `purging → parking` with the obligations, exactly as §5.2 |
| + step 3. This transition is legal only from `purging`, only with the |
| + record authoritatively gone, and only with the purge journal at |
| + `torn-down` or later. |
| + 4. Continue as §5.2 steps 4 and 5. |
| + |
| + A purged host **never returns to `serving`**. Recovery drives these |
| + steps from the purge journal and the host's `op.intent`. Then remove |
| + the app prefix (`PurgeApp`). |
| +5. **The boxes' auto-purge** (domains/reconcile.go:232) runs the same |
| steps. |
| ### 5.4 Placement (J-N8) |
| @@ -600,21 +617,33 @@ So the sweep lists: |
| Anything found is parked as a further retirement event (§6.2), under a |
| 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. |
| +A freed host's location never keeps late residue for good. |
| + |
| +**What a sweep never touches (Q3, R4-3).** This spec owns the sweep, so |
| +it owns this rule. The **live set** is the triple |
| +`{authoritative region, holder.location, holder.generation}`, together |
| +with the exact object versions the moves spec supplies for that |
| +generation, including any pinned noncurrent version (moves owns |
| +generation-specific live-object selection). |
| + |
| +- **In the authoritative region's bucket only**, the sweep never parks or |
| + deletes an object version in the live set. It never touches the |
| + version that `generation.json` names, and never treats the marker |
| + itself as residue. |
| +- **In every other region's bucket**, keys that match `holder.location` |
| + are **residue**, not live, and are parked like any other residue. |
| + Take a legacy host serving in UK: a replica PUT for it that lands in US |
| + after the US retirement is parked. It is not exempted. |
| + |
| +The authoritative region is the region of the holder's current |
| +installation, as the claim names it. That is `op.exec`'s region while |
| +serving, or what the moves spec's phase table names during a move. |
| 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. |
| +(rev 7.4 §6.4). The sweep reads the live set under the same fresh claim |
| +observation it uses for everything else. If the marker and |
| +`holder.generation` disagree, it touches nothing in that location and |
| +raises an alert. |
| On acknowledging, the owner CASes the claim's `quiet_after[region]` to at |
| least `evidence time + H`. Any install into that region's host namespace |
| @@ -674,27 +703,40 @@ held one. Only then does it write. A process that validated, then paused, |
| re-validates under the lock, so a pause before taking the lock is |
| 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, 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, 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 |
| +**Installation stamps (R3-3, R4-2).** Local fencing is scoped to an |
| +installation, not to the whole incarnation. |
| + |
| +- **The stamp.** An installation's stamp is the claim `gen` **captured |
| + at the CAS that made that installation current** on this box: a |
| + create's step 4, or a landing or reinstall made current by its |
| + operation. It is a captured revision, never "the current revision". |
| + The stamp is kept for as long as the installation exists, serving |
| + included. |
| +- **The writer.** Every host-state writer carries |
| + `{incarnation, stamp}` for the installation it acts for. It takes them |
| + from its fresh read under the guard (§6.4). |
| +- **The local record.** Under the guard, each box keeps a record per |
| + host: `{incarnation, active_stamp | none, retired_stamps}`. |
| +- **Admission.** A writer is admitted only if its incarnation equals the |
| + record's **and its stamp equals `active_stamp`**. Every other writer is |
| + refused: |
| + - a stamp lower than `active_stamp`; |
| + - a stamp in `retired_stamps`; |
| + - any stamp while `active_stamp` is `none`. |
| +- **Retirement** (§6.3), under the guard, moves `active_stamp` into |
| + `retired_stamps` and sets it to `none`. |
| +- **A new installation** of the same incarnation, such as a move back to |
| + a region the instance left, sets `active_stamp` to its own captured |
| + stamp. It does this under the guard, conditional on a fresh claim read |
| + showing that its operation is current and that `op.exec`, or the |
| + landing participant, is this box. Claim `gen` only increases, so the |
| + new stamp is greater than every retired one. |
| + |
| +So the new installation is admitted at its own stamp. A stale writer |
| +from a retired installation is refused across any number of retire and |
| +reinstall cycles, because its stamp is never the active one again. |
| +Operations are ordered only by claim `gen`. Op ids are opaque and never |
| +compared (Q1). 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 |
| @@ -935,6 +977,10 @@ the model catches it. |
| | J3-R3-2 | §5.1 step 5, how an orphan is established | |
| | J3-R3-3 | §6.4, the installation-scoped marker | |
| | J3-R3-4 | §6.2a, namespace discovery | |
| +| J4-R4-2 | §6.4, installation stamps | |
| +| J4-R4-3 | §6.2a, the region-qualified live set | |
| +| J4-R4-4 | §5.3 step 4 | |
| +| J4-Q2 | §5.1 step 5 | |
| ## 13. S3 behaviour this relies on, verified |
diff --git a/docs/superpowers/specs/CODEX-FINDINGS-JOINT-R4.md b/docs/superpowers/specs/CODEX-FINDINGS-JOINT-R4.md| new file mode 100644 |
| index 000000000..4a15bc659 |
| --- /dev/null |
| +++ b/docs/superpowers/specs/CODEX-FINDINGS-JOINT-R4.md |
| @@ -0,0 +1,170 @@ |
| +**A, B and C are not yet ready as the joint Phase 1 planning baseline.** Most round-3 fixes are present. The remaining blockers are narrower: the production retirement-fence contract, executable restore semantics, and two lifecycle transitions the model handles differently from the prose. |
| + |
| +I read AGENTS.md first and reviewed A at `3ea3f90c`, B/C at clean HEAD `0e41b685`. Opus was unavailable; this is one independent review. |
| + |
| +Both requested commands failed before compilation: |
| + |
| +```text |
| +go test ./internal/sim/hostlife/ -count=1 |
| +go test ./internal/sim/hostlife/ -run Witness -count=1 -v |
| + |
| +go: creating work dir: mkdir /home/paulca/.cache/tmp/go-build…: read-only file system |
| +``` |
| + |
| +The findings below are static counterexamples, not reproduced failing seeds. `bash -n mutate.sh` passed. Source inspection confirms **26 witnesses, 92 gate runs and 11 combination-only expectations**. Published sweep results remain unverified here. Nothing changed. |
| + |
| +**1. Round-3 dispositions** |
| + |
| +“Resolved” applies to the specific reported defect. |
| + |
| +| Finding | Spec | Model | Why | |
| +|---|---|---|---| |
| +| R3-1: restore algorithm | **Partly** | **Partly** | Snapshot version identity and ordered continuation replace replay-all, but real compacted LTX ranges still lack a complete selection/conflict contract; full histories conceal that problem. | |
| +| R3-2: orphan cleanup deletes a legitimate successor | **Resolved** | **Resolved** | Record-first, fresh-claim-second, conditional deletion; separate modeled observations and a targeted witness. Absent-claim handling is discussed below. | |
| +| R3-3: same-incarnation return move refused | **Partly** | **Resolved within its abstraction** | The round-trip witness requires success, but production ordering is undefined and the model’s replacement fence differs from the specified value. | |
| +| R3-4: bounded history loses old residue | **Resolved** | **Resolved** | Namespace discovery replaces the retired-incarnation list; the model caps that list and forces a completion after 33 recreates. A separate region-selection defect remains. | |
| +| R3-5: public admission before commit | **Resolved** | **Resolved** | `wake` now checks public delivery before its already-running-process shortcut; the mutation has its own INV-5 witness. | |
| +| R3-6: orchestration succeeds without verdicts | **Resolved** | **Resolved** | Directory creation, `xargs`, verdict count and missing witness output now fail the harness. | |
| +| R3-7: default budget admits nothing | **Resolved** | **Resolved for the arithmetic** | Attempts depend on remaining budget; boundary tests cover eligibility. This does not validate the separate, explicitly deferred timing model. | |
| +| Carried R2-5: dirty recovery uses pinned inputs | **Resolved** | **Resolved for the modeled case** | §7.8 explicitly overrides configuration and release materialization with current recovery inputs; the dirty-recovery witness exercises it. | |
| + |
| +The round-3 witness-evidence concern is also substantially resolved: [`check`](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/witness_test.go:178) requires the designated first failure, while the gate checks every proper subset. A missed setup milestone cannot satisfy an unrelated named failure. |
| + |
| +I have not re-raised the explicitly deferred §14.2.6 items, except the requested restore question where the concrete consequence is P1. |
| + |
| +**2. New findings** |
| + |
| +**R4-1 — P1: the restore algorithm can discard a valid compacted continuation.** |
| +B §5.1 steps 2–5 and §7.6; [`restore`](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/protocol_test.go:221). |
| + |
| +The required next object has `min == currentTXID + 1`. That is insufficient for compacted LTX ranges. Consider: |
| + |
| +1. The selected snapshot ends at TXID 100. |
| +2. The replica contains a valid compacted range `[91,110]`; individual `[101,101]` through `[110,110]` objects have been retired from the current listing. |
| +3. The mirror copies that current replica shape. |
| +4. The specified restore finds no object beginning at 101. |
| + |
| +No acknowledged checkpoint need have been lost. The continuation exists, but overlaps the snapshot. Litestream’s restore planner explicitly considers overlapping ranges that extend the current maximum; LTX compaction retains page state rather than every intermediate transaction history. [Litestream restore implementation](https://raw.githubusercontent.com/benbjohnson/litestream/v0.5.14/replica.go), [LTX compactor](https://raw.githubusercontent.com/superfly/ltx/v0.5.1/compactor.go). |
| + |
| +The specification also asks the builder to compare content “at those TXIDs” without defining how to recover intermediate states from compacted objects. Treating unequal bytes as conflicting history can reject valid updates or deletes. |
| + |
| +**Failure:** a builder either refuses a healthy replica or restores only through 100. If that older database passes readiness, the move can commit without already-durable transactions 101–110. Calling this the RPO exception is incorrect: that exception covers writes beyond the last completed checkpoint. |
| + |
| +**Fix:** specify one implementable representation and algorithm. Either normalize the sealed transfer into a verified final snapshot with an explicit continuation position, or define overlapping-range selection and validation against real LTX semantics. Specify the snapshot key as well as its version, the required final TXID, and fail closed when restoration falls short. §7.6 currently requires copying the replica, not producing that normalized snapshot. |
| + |
| +The model cannot expose this: each LTX object carries the complete historical ID sequence, so a later object automatically supplies all preceding transactions. |
| + |
| +**R4-2 — P2: the replacement retirement fence rejects its own new installation if implemented literally.** |
| +A §6.4; [B §6.4](/home/paulca/amadan.net/carlos/platform-moves-design/docs/superpowers/specs/2026-10-02-move-any-app-design.md:808); [`landTarget`](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/moves_test.go:725). |
| + |
| +Both specs say: |
| + |
| +- reject operations **at or before** the marker; |
| +- replace the marker with the **new operation ID** during installation. |
| + |
| +Those rules reject the new operation itself. The model avoids that by writing: |
| + |
| +```go |
| +b.Fence[inc] = w.opSeq(op.ID) - 1 |
| +``` |
| + |
| +Its admission predicate remains `seq <= fence`. |
| + |
| +There is a second mismatch: [`opSeq`](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/world_test.go:351) supplies a global ordering and interprets the empty serving operation as “now.” Neither behavior has a production contract. |
| + |
| +**Failure:** a literal implementation still refuses the return landing. Comparing opaque IDs lexically can also reverse old/new installations. |
| + |
| +**Fix:** define an ordered, durable installation identity and explicit active-versus-retired semantics. For example, capture a claim revision at installation, retain it through serving, reject older installations, and admit equality only for the active installation. Keep operation IDs opaque. Make the model encode precisely that contract, including stale writers across retirement and reinstallation. |
| + |
| +**R4-3 — P2: the sweep exempts the current generation in the wrong region.** |
| +A §6.2a; B §6.4; [`sweepable` and `deadGeneration`](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/moves_test.go:1305). |
| + |
| +`deadGeneration` preserves the current generation’s `base` and `ltx` keys without checking the bucket’s region. It checks executor-region equality only for `generation.json`. |
| + |
| +A concrete schedule is: |
| + |
| +1. Adopt a legacy host serving in UK, with an earlier replica in US. |
| +2. Complete US’s discovery retirement. |
| +3. An old US replication request completes after the retirement horizon. |
| +4. Its location and origin generation equal the current holder’s. |
| +5. The US sweep permanently exempts it. |
| + |
| +The final residue oracle would detect this state, but the legacy fixture does not force that late remote completion. |
| + |
| +**Failure:** residue remains indefinitely in a region the instance left. A namespace-only interpretation of the specs reproduces the model’s mistake. |
| + |
| +**Fix:** define the live set using **region, location and generation together**. Matching keys are protected only in the authoritative region; elsewhere they are residue. Add a witness that releases an old regional PUT after adoption cleanup. |
| + |
| +This is separate from R3-4’s now-fixed bounded-history problem. |
| + |
| +**R4-4 — P2: purge invokes a retirement sequence whose entry condition it has already invalidated.** |
| +A §5.2 step 1 and §5.3 steps 2–3; [`deleteSteps`](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/console_test.go:567). |
| + |
| +Purge first changes each host from `serving` to `purging`. After store teardown it says to run §5.2, whose first step acquires `deleting` **from `serving` only**. |
| + |
| +The model silently supplies a different contract: `deleteSteps` accepts both `deleting` and `purging`, then proceeds directly to record removal and parking. |
| + |
| +**Failure:** a builder reusing the specified retirement entry point gets a conflict after stores have already been removed; purge cannot finish. |
| + |
| +**Fix:** explicitly define retirement under an existing purge claim, preserving the purge operation ID and recording the exact record version before deletion. State the legal `purging → parking` transition and its recovery prerequisites. Do not temporarily release to `serving`. |
| + |
| +**3. Model fidelity and mutation evidence** |
| + |
| +**The global operation counter hides a production-contract fault.** It is a reasonable abstraction only after the production ordering and fence boundaries are specified. Currently it supplies ordering, a predecessor value and a serving-state sequence that the prose does not provide. R4-2 is a concrete consequence, not merely a concern about randomness. |
| + |
| +**The four witness-only rules force useful schedules:** |
| + |
| +| Rule | What is forced | Meaning of the sweep miss | |
| +|---|---|---| |
| +| `generation-conditional` | Hold the first marker PUT across two completed pushes, then release it. | The random generator lacks a marker-specific worst-moment schedule. Zero catches does not establish redundancy. | |
| +| `declare-lost-compute` | Freeze the target through lease expiry, recover the source under the mutation, resume the target before its agent. | Freeze and expiry are representable; the dangerous ordering is rare under random scheduling. | |
| +| `fence-by-installation` | Complete UK→US→UK and require the instance running back in UK. | Primarily an **oracle gap**: random convergence accepts rollback as a terminal outcome. | |
| +| `sweep-namespace` | Complete 33 recreate cycles before releasing incarnation 1’s PUT. | A **history-depth gap**: the bounded random runs do not exercise the retention boundary. | |
| + |
| +Their named failures distinguish them from arbitrary setup failures. For `fence-by-installation`, however, the successful baseline validates the model’s `newSequence - 1` repair, not the literal specification. |
| + |
| +The random generator should gain targeted marker/freeze schedules, successful-move assertions and a retention-boundary fixture. More seeds alone will not address all four gaps. |
| + |
| +**The 11 combination-only classifications are defensible as scenario-specific results.** The gate checks the necessary subsets for each declared witness set. This supports “these guards jointly prevent this schedule,” not “each guard is globally redundant.” |
| + |
| +One reporting qualification: the extra three-rule door combination in B’s results table is not a minimal combination—its two-rule subsets already have failing witnesses. It should not inherit the blanket claim that every proper subset holds. This does not invalidate the count of 11 classified rules. |
| + |
| +**IDs-only restoration is a real fidelity gap here.** Opaque IDs can adequately represent operation preservation if the underlying restore contract is already established. Full-history prefix comparison additionally assumes access to history that compacted LTX objects do not retain. R4-1 demonstrates why updates, deletes, overlapping ranges and missing deltas need a real restoration test before this model can support the data-preservation claim. |
| + |
| +**4. Answers to the claim-owner questions** |
| + |
| +1. **Operation ordering:** A does not answer it. Either proposed approach can supply an order, but only when assigned through the successful claim CAS and paired with explicit equality/serving semantics. Prefer a captured claim revision as the installation stamp; do not compare random IDs or use a continually changing “current revision” as installation identity. |
| + |
| +2. **Orphan cleanup with no claim:** **Do not delete.** A §9 requires legacy adoption, and C5a means absence cannot represent a previously retired claimed host. The model’s `orphanOf(nil, …) == false` is the safe interpretation. Add that explicit branch to §5.1. |
| + |
| +3. **Protecting the named snapshot:** B §6.4 already states the protection. B should own generation-specific live-object selection; A should require its sweep to preserve that supplied live set. The protection must apply in the authoritative bucket, including the pinned noncurrent version—not exempt matching keys in every region. |
| + |
| +**5. Verdicts** |
| + |
| +| Artifact | Ready for Phase 1 implementation planning? | Reason | |
| +|---|---|---| |
| +| **A — claim rev 6** | **No** | Resolve installation-fence semantics, region-qualified sweeping and retirement under purge ownership. | |
| +| **B — moves rev 7.4** | **No** | Resolve executable LTX restoration and inherit the corrected claim contract. Dirty recovery and budget arithmetic are substantially improved. | |
| +| **C — model at `0e41b685`** | **No, as the planning gate** | Stronger mutation evidence, but the fence differs from the prose, the sweep misses a valid residue state, and restore has stronger historical information than production. | |
| + |
| +Building the claim primitive first remains the correct ordering. These are targeted contract corrections; they do not require reopening M1–M18. |
| + |
| +--- |
| + |
| +**FIRST PROMPT:** |
| +Joint independent round-4, read-only review of two CARLOS specs and their executable model. |
| + |
| +**WHAT:** |
| +Assess prior fixes, model fidelity, new faults and Phase 1 readiness. |
| + |
| +**STATUS:** |
| +Review complete: one P1 and three P2 findings. Go runs blocked before compilation. |
| + |
| +**NEEDED:** |
| +Nothing for this review. |
| + |
| +**RECOMMENDED:** |
| +Resolve the four contracts, align the model, and add the targeted restoration and residue tests. |
| + |
| +**SESSION:** |
| +Safe to close. No files changed; nothing remains running. |
| \ No newline at end of file |