carlos / platform Public

spec: host lifecycle claim rev 6, after joint round 3

R3-2: orphan established by record-then-claim reads, with the
one-claim-attempt-per-incarnation argument; R3-3: installation-scoped local
retirement marker, replaced by a guarded new install; R3-4: the at-rest
sweep discovers locations from the namespace, not the capped history.
Joint R3 findings copied unedited.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

claude 3 weeks ago 3ea3f90c44f66421c9740b92e460992b759076c9 parent 465fee9

2 files changed, +230 −13

docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md +67 −13
docs/superpowers/specs/CODEX-FINDINGS-JOINT-R3.md +163 −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 4ec253ad7..e3dca66ac 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 5.2** (rev 5 plus CC20 to CC22). A small primitive cited by:

+Design, 2026-10-03, **rev 6**. 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,10 @@ 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 5** folds in CC15 to CC19, required by the strict joint model

+**Rev 6** answers 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

(47e65af8, moves rev 6 at 7ac666fe).

**Rev 4** answered the claim-side findings of joint round 2

@@ -351,7 +354,27 @@ new operation will write (CC11). A pending chore there must finish first.

- **orphans whenever they land (CC17):** a record whose incarnation is

in `retired_incarnations`, or is not the claim's holder, is an

orphan at any time, not only inside the `cancelled_creates`

- window. A create that finds its record key occupied by one

+ window.

+ - **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.

+ 3. The record is an orphan only if that claim names neither `I` as

+ holder nor a `creating` operation for `I`.

+ 4. Delete it with `DeleteIfMatch(E)`.

+ Why `I` cannot become legitimate later:

+ - **Each incarnation gets exactly one claim attempt.** A create

+ assigns `CreatedAt`, and so its incarnation, in step 1, and

+ attempts the step 2 CAS once. A 412 restarts from step 0 with a

+ new `CreatedAt`.

+ - **A record exists only after its claim attempt succeeded** (C2).

+ - **So the claim named `I` once.** If a claim read *after* the record

+ no longer names `I`, the claim has since moved on, and `I` has no

+ attempt left.

+ A pause anywhere between these steps is harmless. A legitimate

+ successor's record at the same key has a different incarnation and

+ a different ETag, so the conditional delete fails; A create that finds its record key occupied by one

removes it with `DeleteIfMatch`, then retries its create-only

write. The pass removes any it meets. A late record write after

the window therefore never blocks a later recreate;

@@ -544,12 +567,28 @@ its own retirement id and manifest, and the verification repeats.

**Requests that complete after `H` (CC15).** C3a makes a very late

completion harmless to a successor, but it still leaves residue, and it

needs an owner. Each region's box runs an **at-rest sweep**: for every

-host it can see in its bucket that has no operation running. It lists:

-- the location of every incarnation in that host's

- `retired_incarnations`;

-- **`moves/<host>/`** (CC20): a staging write that completes after its

- move's cleanup would otherwise stay there for good;

+host it can see in its bucket that has no operation running.

+**It discovers locations from the namespace itself (R3-4).** It does not

+use `retired_incarnations`, which is capped at 32 entries and exists only

+to stop an incarnation being reused. It lists `instances/<host>/` and

+`moves/<host>/` with delimiter `/`, every page, and refuses on any listing

+error. Each child prefix is either:

+- an **incarnation location**: 64 hex characters. It is residue unless it

+ is the current `holder.location`;

+- a **legacy level directory** (`0000/` to `0009/`, litestream's level

+ layout), sitting directly under `instances/<host>/`. That is the legacy

+ location. It is residue unless `holder.location` is exactly

+ `instances/<host>`.

+So the sweep lists:

+- every incarnation location under the host's prefix, current excepted,

+ however old it is;

+- **`moves/<host>/`** (CC20), enumerated the same way: a staging write

+ that completes after its move's cleanup would otherwise stay there for

+ good;

- every generation within the live `holder.location` other than

`holder.generation` (the moves spec's dead generations).

@@ -616,10 +655,22 @@ 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 for the incarnation, so any later writer for that incarnation is

-refused. A pass that selected a row before an operation began therefore

-either finishes before retirement takes the guard, or fails at its next

-write.

+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.

+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

+non-home round trip (UK→US→UK) as an unmutated, deterministic witness.

+A pass that selected a row before an operation began therefore either

+finishes before retirement takes the guard, or fails at its next write.

The guard is local because these writers are local. The claim decides

what each writer is allowed to do. The model must run these as

@@ -853,6 +904,9 @@ the model catches it.

| CC20 | §6.2a at-rest sweep |

| CC21 | §5.3 step 1b, the purge fence |

| CC22 | §5.1 steps 0 and 2, §5.3 fence release, C5a |

+| 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 |

## 13. S3 behaviour this relies on, verified

diff --git a/docs/superpowers/specs/CODEX-FINDINGS-JOINT-R3.md b/docs/superpowers/specs/CODEX-FINDINGS-JOINT-R3.md

new file mode 100644

index 000000000..ab6b0695f

--- /dev/null

+++ b/docs/superpowers/specs/CODEX-FINDINGS-JOINT-R3.md

@@ -0,0 +1,163 @@

+**A, B and C are not yet ready to gate Phase 1 implementation planning.** Several round-2 fixes are complete, but restore remains underspecified, orphan cleanup introduces a destructive race, and local retirement can prevent a valid move back.

+I read AGENTS.md first. A was reviewed at `465fee96`; the clean worktree matches B and C at `dc7f2a63`. Opus was unavailable, so this is one independent review, without the repository-requested Opus review.

+Both requested runs 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 findings**, not reproduced failing seeds. Published sweep and witness counts remain unverified here. Nothing was changed.

+**1. Round-2 dispositions**

+“Resolved” applies to the specific finding, not the whole mechanism.

+|---|---|---|---|

+| R2-7: cancelled create publishes late | Partly | Partly | Indefinite orphan cleanup fixes the original blockage, but its observation order is unsafe; model cleanup is atomic and recreation also consults hidden pending-request state. |

+| R2-10: infrastructure failures counted as catches | Resolved | Partly | Individual-run classification is substantially fixed; orchestration failure or missing verdict files can still produce successful script exit. |

+The remaining **R2-5 specification contradiction** is concrete: [B §7.8](/home/paulca/amadan.net/carlos/platform-moves-design/docs/superpowers/specs/2026-10-02-move-any-app-design.md:1143) reuses *exactly* §7.6’s dirty-install phases, including [the `configured` gate](/home/paulca/amadan.net/carlos/platform-moves-design/docs/superpowers/specs/2026-10-02-move-any-app-design.md:1059) requiring `move.inputs`. If the target writes, configuration changes, and rollback is dirty, source recovery can fail before reaching the newly corrected recovery probe. Explicitly parameterize **both configuration and release materialization** for forward versus recovery installs.

+**2. Model fidelity and witnesses**

+The model is materially better, but “encodes the specs, nothing stronger” remains too strong.

+| Concern | Assessment |

+|---|---|

+| Restore | The exact-base shortcut is gone, but [`restore`](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/protocol_test.go:195) unions write IDs across all versions. It cannot represent conflicting updates, deletes, transaction gaps or choosing incompatible histories. |

+| Admission | The original claim-generation mismatch is fixed. However, wake admission is not a model of public traffic reaching an already-running probe. |

+| Cross-object atomicity | Flip, commit, rollback and close have separate record/claim steps. Most detailed phases still live only in the model’s claim; record reads, ETag selection and writes are atomic direct assignments. |

+| Local exclusion | Independent background processes now survive agent crashes. Their validation/write remains atomic, and [`plan`](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/world_test.go:308) carries neither selected operation nor release version. [`passExec`](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/background_test.go:247) cannot check them. |

+| Same-operation workers | Still unresolved: replica lease acquisition is an unconditional PUT; staging acquisition accepts the same operation regardless of worker identity. These do not exercise the specified exclusion. |

+| Oracle | It no longer repairs replica storage. However, [`release`](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/moves_test.go:907) calls only `checkDurable`, not the complete local/timer acknowledgment check. A later delete can erase evidence of an earlier loss. |

+| Late creates | [`createSteps`](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/console_test.go:205) refuses while `recPend` exists. A real console cannot know whether a timed-out request remains pending on the server. This suppresses relevant recreation races. |

+| Cleanup ordering | The model queues target parking at release and local retirement after return publication, before source recovery completes. B §7.8 explicitly delays target cleaning until `recovered_at`. |

+| Remaining abstractions | Permissions on reads/listings, pagination, durable rename/fsync failures, spawn-before-readiness, clock changes and executable enrollment remain gaps. B §14.2.6 now acknowledges most of these appropriately. |

+| Timing | The reversed `H`/cut-budget relationship and omitted `open_budget` mean this model cannot validate the production downtime promise. |

+**The witnesses do force useful schedules.** Held marker publication, stale staging completion, VM freeze/resume, agent restart during rollback, delayed opens and the two door races are explicit scheduled events rather than lucky random seeds.

+Their evidence has limits:

+- [`TestWitnesses`](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/witness_test.go:113) accepts **any** invariant violation. It does not require the failure named by the scenario.

+- [`reach`](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/witness_test.go:271) turns any missed milestone into INV-3. A broken setup can therefore satisfy a mutation’s expected failure.

+- Several bounded `drive` calls do not assert the intended milestone. Particularly for staging cleanup and source recovery, the witness should distinguish “reached the intended interleaving” from “eventually failed.”

+- A holding single mutation and failing combination establish protection **in that scenario**. They do not establish global redundancy. Run each witness against every relevant proper subset and assert its designated failure.

+The combination reporting is more candid than round 2: partner counts and failure categories are supplied. **`commit-before-open` is still incorrectly included among “caught” rules**, despite the text admitting that its combination detects only `dirty-return`’s failure. That rule remains independently unvalidated.

+**3. New findings**

+**R3-1 — P1: “replay every version” is not an implementable restore algorithm.**

+B §5.1; [model restore](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/protocol_test.go:164).

+A generation can contain the installed snapshot, later replication, duplicate copies and late versions. B specifies replaying every current and noncurrent object, but supplies no selection/order rule for overlapping transaction ranges or conflicting versions.

+The existing [`lease.Restore`](/home/paulca/amadan.net/carlos/platform-moves-design/internal/lease/lease.go:404) delegates to Litestream. Its S3 client opens an LTX key without a `VersionId`; restoration computes a transaction-range plan. It does not implement this new all-version contract. [Litestream S3 client](https://github.com/benbjohnson/litestream/blob/v0.5.14/s3/replica_client.go), [restore implementation](https://github.com/benbjohnson/litestream/blob/v0.5.14/replica.go).

+**Failure:** reusing the existing restore path ignores historical versions the proof relies on; literal replay-all can select conflicting or regressive database state. The model’s set union makes either problem invisible.

+**Fix:** specify immutable snapshot identity, continuation transaction position, version selection, ordering, duplicate/conflict handling and gaps. Validate against real LTX restoration with updates and deletes, not only accumulated write IDs.

+**R3-2 — P1: orphan cleanup can delete a legitimate successor’s record.**

+A §5.1 step 5, CC17; [modeled recovery](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/console_test.go:889).

+A legal implementation can:

+1. Read a free claim and pause.

+2. Let a creator claim the host and publish record B.

+3. Read B’s record, compare it with the earlier free claim, classify it as orphaned.

+4. Successfully `DeleteIfMatch` B’s record ETag.

+Conditioning on the record protects against replacement **after selection**. It does not validate the stale claim used to authorize deletion. A supplies no required observation order or cleanup reservation; the model performs the observations and deletion atomically.

+**Fix:** select the exact record first, then freshly establish its orphan status against the claim, with a documented argument preventing that identity becoming legitimate afterward—or reserve cleanup through a claim CAS. Add pauses between both observations and deletion.

+**R3-3 — P2: retirement fences prevent legitimate same-incarnation moves back.**

+A §6.4; B §§6.4, 7.6; [retirement marker](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/protocol_test.go:505), [admission refusal](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/protocol_test.go:357).

+Move UK→US successfully. Source retirement marks the incarnation retired on UK. Move US→UK: the incarnation is unchanged, so UK refuses the landing probe.

+The model clears this marker only while minting a **serving** row, not while installing a held landing. The second move therefore times out and rolls back. Terminal convergence allows that outcome, so a green sweep does not establish that valid return moves succeed. Legacy discovery can establish the same fence on future targets.

+**Fix:** scope retirement fencing to the retired installation/operation, or define a guarded new-install transition that advances the local fence while continuing to reject old workers. Require a successful non-home round trip in an unmutated deterministic test.

+**R3-4 — P2: bounded incarnation history loses ownership of arbitrarily late residue.**

+A §2 `retired_incarnations`, §6.2a; [modeled retention](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/console_test.go:464).

+A retains only 32 retired incarnations, while allowing requests to complete arbitrarily late. After enough recreate cycles, an old request can land under an incarnation no longer listed for sweeping. Its residue then has no specified cleanup owner.

+C retains every incarnation indefinitely, so it cannot expose this failure. It also retains an extra `legacyIncs` map for reconstructing historical legacy locations.

+**Fix:** discover retired locations from the namespace independently of the bounded anti-reuse list, or retain durable location records until retirement can safely be forgotten. Model the actual retention limit and legacy-location metadata.

+**R3-5 — P2: the model does not test public admission before commit.**

+B §14.2.5; [mutation site](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/moves_test.go:796), [shared witness](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/witness_test.go:615).

+Removing `commit-before-open` makes the target row ready while its probe already runs. The model has no distinct public-request action or assertion that such a request must be refused. `wake` returns immediately when a main process exists, and background writes are allowed during probes anyway.

+Thus the stated reason that an open row admits nothing because the claim is uncommitted is not established. B §9.5 specifies no edge changes; current routing gates on [row status](/home/paulca/amadan.net/carlos/platform-moves-design/internal/edge/edge.go:595).

+**Fix:** model public delivery separately from background execution, including the probe’s held activator entry. Assert no public delivery before commit. Classify this rule as unproven until its own violation is demonstrated; its partner’s write loss is insufficient.

+**R3-6 — P2: mutation orchestration can succeed without producing verdicts.**

+[mutate.sh:50](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/mutate.sh:50), [mutate.sh:129](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/mutate.sh:129).

+The script ignores directory-creation and `xargs` status, then counts bad lines in whatever verdict files exist. If workers cannot start or verdict files cannot be written, an empty result set contains zero bad lines and the script can exit successfully.

+**Fix:** fail on orchestration and output-write errors; require exactly one valid verdict per requested mutation. Also require the expected witness set to have run, rather than accepting missing witness output as `none`.

+**R3-7 — P2: the default cut budget cannot pass its own readiness formula.**

+[B §7.3 T11](/home/paulca/amadan.net/carlos/platform-moves-design/docs/superpowers/specs/2026-10-02-move-any-app-design.md:925).

+Three permitted attempts, each with 30 seconds plus a 20-second settle, require **150 seconds**, before stopping, transferring, restoring, rendering or the five-second open. The default window is 120 seconds.

+**Failure:** a builder following the stated worst-case formula refuses every default move, even for a tiny instance. C does not model T11’s calculation.

+**Fix:** make the permitted attempt count depend on the admitted budget, or supply a consistent configurable default and formula. Add a deterministic readiness calculation demonstrating that the default admits an eligible instance.

+No additional material P3 findings.

+**4. Verdicts**

+| Artifact | Ready for Phase 1 implementation planning? | Reason |

+|---|---|---|

+| **A — claim rev 5.2** | **No** | Define safe orphan-cleanup observations, same-incarnation local reinstallation and durable discovery of late residue. |

+| **B — moves rev 7.3** | **No** | Resolve the restore algorithm, dirty-recovery configuration contradiction, return-move fence and budget arithmetic; inherits A’s blockers. |

+| **C — executable model** | **No, as the planning gate** | Useful regression evidence, but restore, public admission, lifecycle observation boundaries and terminal acknowledgment checks still hide relevant failures. |

+Build the claim primitive first remains the right ordering. Before planning against these contracts, correct the identified boundaries and add deterministic tests requiring the intended successful outcomes as well as safe rollback.

+---

+**FIRST PROMPT:**

+Joint independent round-3, read-only review of two CARLOS specs and their executable model.

+**WHAT:**

+Assess round-2 fixes, model fidelity, new faults and Phase 1 readiness.

+**STATUS:**

+Review complete. All three verdicts remain not ready. Go runs were sandbox-blocked.

+**NEEDED:**

+Nothing for this review.

+**RECOMMENDED:**

+Resolve the contract gaps, strengthen targeted witnesses, then rerun the baseline and mutation suite.

+**SESSION:**

+Safe to close. No files changed; nothing remains running.

\ No newline at end of file