amadan
spec: host lifecycle claim rev 6.3, the installation stamp's lifecycle (R5-4)
holder.stamp written by every installing CAS (create, adoption, flip, reinstall, dirty rollback, push commit); local records initialized only from a fresh claim read naming this box; no record means refuse; retire-artifacts(S) distinct from retire-installation. Joint R5 copied unedited.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2 files changed,
+205
−11
docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md+53 −11docs/superpowers/specs/CODEX-FINDINGS-JOINT-R5.md+152 −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 fdb16e669..852b43783 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.2**. A small primitive cited by: |
| +Design, 2026-10-03, **rev 6.3**. 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 6.2** answers the claim side of joint round 4 |
| +**Rev 6.3** answers R5-4 from joint round 5 (`CODEX-FINDINGS-JOINT-R5.md`): |
| +the installation stamp's lifecycle. |
| + |
| +**Rev 6.2** answered the claim side of joint round 4 |
| (`CODEX-FINDINGS-JOINT-R4.md`): R4-2, the claim half of R4-3, R4-4, and |
| Q2. |
| @@ -82,7 +85,8 @@ replaced whole with conditional writes (`If-Match` on the ETag read). |
| "account": "bab", "app": "jam", "name": "", |
| "incarnation": "<hex>", "created_at": "<record CreatedAt>", |
| "location": "instances/shop.bab.oncarlos.com/<incarnation>", |
| - "generation": "<op id of the installed generation, or \"\">" |
| + "generation": "<op id of the installed generation, or \"\">", |
| + "stamp": 41 |
| }, |
| "op": { |
| "kind": "serving", |
| @@ -126,6 +130,19 @@ Field rules: |
| set and never changes while that holder holds the host. Same-incarnation |
| generations within it (moves, push) are the moves spec's, scoped by |
| operation id. |
| +- **`holder.stamp`** is the current installation's stamp (§6.4, R5-4): |
| + the claim `gen` produced by the CAS that made that installation |
| + current. **That same CAS writes it**, so it is persisted atomically with |
| + the transition, and the claim is always where a box recovers it. These |
| + CASes are: |
| + - create step 4 (`creating → serving`); |
| + - adoption; |
| + - a move's flip; |
| + - a reinstall, a dirty rollback's install of a new generation, and a |
| + push's commit. |
| + |
| + Each writes `holder.stamp = its own resulting gen`. A transition that |
| + doesn't change the installation leaves `holder.stamp` alone. |
| - **`holder.generation`** names the installed generation within |
| `holder.location` (CC18). The moves spec owns its values and its |
| markers. Its start check compares this field with all three of its |
| @@ -706,12 +723,13 @@ harmless. |
| **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 stamp.** An installation's stamp is the claim `gen` **produced by |
| + the CAS that made that installation current**. That CAS also wrote it |
| + into `holder.stamp` (§2). It is a captured revision, never "the |
| + current revision". The stamp is kept for as long as the installation |
| + exists, serving included. Every transition that installs a new |
| + generation issues a new stamp. That includes a dirty rollback, which |
| + never keeps its predecessor's stamp. |
| - **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). |
| @@ -723,8 +741,31 @@ installation, not to the whole incarnation. |
| - 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`. |
| +- **Initialization (R5-4).** A box creates or refreshes its local record |
| + only from a fresh claim read under the guard, and only when the claim |
| + names this box as `op.exec` (or as the landing participant, per the |
| + moves spec's phase table). It sets `active_stamp = holder.stamp`. That |
| + covers: |
| + - a create's first wake; |
| + - adoption, on the box serving the legacy host, after the adoption CAS; |
| + - a box whose local record was lost, on restart. |
| + |
| + In every case the claim is the recovery source. |
| +- **No local record:** refuse. A writer for a host with no local stamp |
| + record is never admitted until initialization has run. |
| +- **Two different retirements (R5-4).** Local artifacts are tagged in |
| + the inventory (§6.3) with the stamp of the installation that produced |
| + them. |
| + - **`retire-artifacts(stamp S)`** parks only the artifacts tagged `S` |
| + and adds `S` to `retired_stamps`. It never touches `active_stamp`. |
| + A landing that has activated its own stamp uses this to park its |
| + predecessor's leftovers. |
| + - **`retire-installation`** (§6.3, local park at delete or a move away) |
| + moves `active_stamp` into `retired_stamps`, sets it to `none`, and |
| + parks every artifact. |
| + |
| + A helper must name which of the two it is. Nothing calls |
| + `retire-installation` to clean up a predecessor. |
| - **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 |
| @@ -981,6 +1022,7 @@ the model catches it. |
| | J4-R4-3 | §6.2a, the region-qualified live set | |
| | 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 | |
| ## 13. S3 behaviour this relies on, verified |
diff --git a/docs/superpowers/specs/CODEX-FINDINGS-JOINT-R5.md b/docs/superpowers/specs/CODEX-FINDINGS-JOINT-R5.md| new file mode 100644 |
| index 000000000..f0a43fcbd |
| --- /dev/null |
| +++ b/docs/superpowers/specs/CODEX-FINDINGS-JOINT-R5.md |
| @@ -0,0 +1,152 @@ |
| +**A, B and C are not yet ready as the joint Phase 1 planning baseline.** The main remaining blocker is the integration with pinned Litestream: replication restart, checksum availability and snapshot retention differ materially from the model. |
| + |
| +I read AGENTS.md first. Reviewed A at `30d572c4` and B/C at clean HEAD `cdc98845`, including the prior findings and change notes. Two GPT-6 subreviews supported this review; the repository-requested Opus model was unavailable. |
| + |
| +Both requested tests 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 |
| +``` |
| + |
| +These are **static findings**, not reproduced failing seeds. Shell syntax checking passed for `mutate.sh`. Source inspection confirms **75 rules, 30 witnesses, 102 baseline/subset/full-set runs and 15 expected misses**. Published sweep results remain unverified here. No files changed. |
| + |
| +The round-4 dispositions are: |
| + |
| +| Round-4 finding or point | Spec | Model | Why | |
| +|---|---|---|---| |
| +| **R4-1: compacted continuation** | **Partly** | **Partly** | Overlap selection and explicit snapshot identity fix the reported algorithm defect; real replication restart, checksums and retention remain incompatible. | |
| +| **R4-2: replacement retirement fence** | **Partly** | **Partly** | Equality and captured revisions remove the off-by-one and opaque-ID ordering problems; stamp initialization and replacement are not fully specified or faithfully encoded. | |
| +| **R4-3: wrong-region live-set exemption** | **Resolved** | **Resolved** | Region qualifies protection for data and markers; the late remote PUT has a targeted witness. | |
| +| **R4-4: purge cannot enter retirement** | **Resolved** | **Resolved** | A §5.3 explicitly permits purge-owned retirement; C records the version, deletes conditionally and requires teardown before parking. | |
| +| **Full histories conceal restore defects** | **Resolved within the stated abstraction** | **Resolved within the stated abstraction** | Restoration consumes page images and ranges; transaction history is oracle-only. This does not establish library integration. | |
| +| **Witness-specific failures and subset evidence** | **Resolved** | **Resolved** | The gate requires every proper subset to hold and the full set’s first violation to match its named failure. | |
| +| **Generator lacks targeted schedules and successful outcomes** | **Partly** | **Partly** | Marker holds, target freezes and successful round trips are present; the retention fixture has an off-by-one error. | |
| +| **Combination reporting overstates minimality** | **Resolved** | **Resolved for the declared scenarios** | The relevant minimal pairs are identified; subset checks support scenario-specific necessity, not global redundancy. | |
| +| **Q1 / model-only operation ordering** | **Resolved conceptually** | **Partly** | A chooses captured claim revision and active equality. C still uses a later revision for creation. | |
| +| **Q2: orphan with no claim** | **Resolved** | **Resolved** | Absence means legacy adoption, never orphan deletion. | |
| +| **Q3: ownership of pinned-version protection** | **Resolved** | **Resolved for the reported protection** | A owns the regional sweep guarantee; B supplies generation-specific versions. The current generation’s versions are preserved in the authoritative bucket. | |
| + |
| +The new findings follow. I have not reopened M1–M18 or the explicitly deferred §14.2.6 items. |
| + |
| +**R5-1 — P1: restoring the sealed snapshot does not establish the replication position assumed by the model.** |
| + |
| +B §5.1, §7.6; [protocol_test.go:245](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/protocol_test.go:245). |
| + |
| +`e08c5fd0` sets both `db.TX` and `db.Rep` to the restored TXID. That fixes the abstract model’s malformed subsequent delta, but its explanation—Litestream’s `-txid` sidecar—is incorrect for ordinary replication. |
| + |
| +Pinned Litestream writes that sidecar for **follow mode**. Normal replication derives its position from local or remote **L0 files**; its initialization returns without establishing a position when remote L0 is absent. B deliberately installs only an L9 snapshot. [Pinned restore implementation](https://raw.githubusercontent.com/benbjohnson/litestream/v0.5.14/replica.go), [pinned database initialization](https://raw.githubusercontent.com/benbjohnson/litestream/v0.5.14/db.go). |
| + |
| +Concrete failure: |
| + |
| +1. Install and restore the sealed snapshot ending at N. |
| +2. Start replication with rebuilt local metadata and no remote L0. |
| +3. Replication starts its numbering at 1. |
| +4. Newly acknowledged writes are uploaded with TXIDs below N. |
| +5. A subsequent cold restore, rooted at N, skips those files and loses the new writes. |
| + |
| +**Fix:** specify a durable restore-to-replication initialization procedure supported by the pinned library. Test snapshot-only install → write → successful replication → loss of local DB and metadata → cold restore. Setting the model’s counters is necessary but does not implement that procedure. |
| + |
| +**R5-2 — P2: the required post-apply checksums are absent from ordinary pinned Litestream files.** |
| + |
| +[B §5.1 steps 1–5](/home/paulca/amadan.net/carlos/platform-moves-design/docs/superpowers/specs/2026-10-02-move-any-app-design.md:542); [ltx_test.go:164](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/ltx_test.go:164). |
| + |
| +The pinned L0 writer, snapshot writer and compactor set `HeaderFlagNoChecksum`. LTX v0.5.1 requires `PostApplyChecksum == 0` with that flag. The model supplies a whole-state checksum for every file. See pinned `db.go:1948`, `db.go:2412`, `compactor.go:165` and `ltx.go:356`. |
| + |
| +A builder following B’s final database-checksum comparison literally will reject healthy continuations. Skipping the comparison silently removes a guarantee that the specification and model currently claim. |
| + |
| +**Fix:** either provide end-state checksums through explicitly changed writers and compaction, or define verification using guarantees the pinned format actually supplies. A file CRC is not a whole-database post-apply checksum. Add a test using real pinned-library output. |
| + |
| +**R5-3 — P2: permanently rooting restoration at the installation snapshot conflicts with normal retention.** |
| + |
| +B §5.1 step 4; [ltx_test.go:265](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/ltx_test.go:265). |
| + |
| +The model excludes later L9 snapshots and models only L0→L1 compaction. Real Litestream creates newer snapshots and expires older lower-level ranges through snapshot retention. [Pinned retention implementation](https://raw.githubusercontent.com/benbjohnson/litestream/v0.5.14/store.go). |
| + |
| +After sufficiently many newer snapshots, the current listing can contain: |
| + |
| +- the original pinned snapshot N, still retrievable by version; |
| +- newer complete snapshots; |
| +- continuation files beginning beyond N+1, because earlier ranges were legitimately retired. |
| + |
| +C ignores the newer snapshots and refuses the resulting gap. Ordinary Litestream restoration can use a newer snapshot. Protecting the original snapshot version alone does not preserve its continuation. |
| + |
| +B’s “every level” wording needs clarification: its stated reuse of `CalcRestorePlan`, and C’s implementation, exclude subsequent L9 snapshots. |
| + |
| +**Fix:** either retain a complete continuation from the pinned root, or define verified successor snapshots and safe advancement of that root. Model snapshot rotation and retention, then test cold restoration afterward. |
| + |
| +**R5-4 — P2: installation stamps lack a complete durable initialization and replacement contract.** |
| + |
| +A §6.4; B §§6.4, 7.6, 7.8; [background_test.go:198](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/background_test.go:198). |
| + |
| +The equality predicate is now sound. Its lifecycle is incomplete: |
| + |
| +- Creation must capture its serving-CAS revision, but C initializes the stamp later from `c.Ver` during reconciliation. Intervening claim writes change that value. |
| +- Landing explicitly persists `FlipGen`; creation has no equivalent specified recovery source. |
| +- Dirty rollback installs a new generation but retains the source’s old stamp. |
| +- B activates the new stamp during `checking`, then later local-parks old artifacts. A’s general local-retirement rule clears the active stamp. Reusing that helper literally can retire the new installation and refuse its probe. |
| + |
| +C also [admits a writer when no stamp record exists](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/world_test.go:403), whereas A requires equality with an active installation. |
| + |
| +**Fix:** persist each authorizing revision atomically with its claim transition; specify creation, adoption and dirty-reinstall initialization. Distinguish retiring predecessor artifacts from retiring the active installation. Encode those rules and crash boundaries in C. |
| + |
| +**R5-5 — P2: readiness still budgets a small incremental mirror after switching to a full final snapshot.** |
| + |
| +[B §7.3 T11](/home/paulca/amadan.net/carlos/platform-moves-design/docs/superpowers/specs/2026-10-02-move-any-app-design.md:1136), versus §5.1 step 1. |
| + |
| +T11 prices the final cross-region transfer as at most **16 MiB**. Rev 7.5 instead creates and transfers a complete snapshot after stopping the source. |
| + |
| +For example, a 2 GiB database over a 10 MiB/s transfer path requires roughly 205 seconds for that transfer alone. The existing formula can still admit it into a 120-second window by pricing only the small delta. Deadline enforcement then rolls back a predictably impossible move. |
| + |
| +**Fix:** budget snapshot construction and its full cross-region transfer, or explicitly construct the sealed snapshot on the target from previously staged material. Update the cut phases and budget test together. This is a new workload mismatch, separate from the deferred simulation timing scale. |
| + |
| +**R5-6 — P3: the retention-boundary fixture has not crossed the boundary it claims.** |
| + |
| +[sim_test.go:55](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/sim_test.go:55). |
| + |
| +`retentionStart` fills `Retired` with incarnations 1–32, then injects residue for `old := 1`. Incrementing `nextInc` does not remove 1 from the list. |
| + |
| +**Fix:** retire incarnation 33 first, or populate 2–33, and assert that the injected incarnation is absent. The deterministic 33-recreate witness remains valid; this finding concerns the new random fixture and its coverage claim. |
| + |
| +On the requested fidelity questions: |
| + |
| +- **Planner and page abstraction:** the overlap predicate and preference order match the pinned planner. Final page images, updates and deletes address R4’s historical-information problem. Overall fidelity remains partial because of R5-1 through R5-3. |
| +- **Oracle:** replaying acknowledged transactions into expected state is sound for this KV abstraction. Restoration does not consult the oracle’s transaction lists; those lists establish durability separately. The lineage assumption requires the real initialization contract in R5-1. The already-deferred release-time omissions remain limitations, not new findings here. |
| +- **`live-set-region`:** genuinely forces the old remote PUT to complete after adoption discovery finishes. |
| +- **`restore-gap-closed`:** genuinely forces refusal of snapshot 11 plus file 13 with file 12 missing. It is a deliberately malformed-replica test with an explicit refusal assertion, not evidence that this sequence arises through the normal sequential uploader. |
| +- **`fence-stamp`:** the witness establishes scenario-specific protection. Either the stamp or the fresh bundle check stops its stale config write; removing both produces the named failure. Equal sweep counts with `hostguard` alone add no independent evidence. An unchanged-bundle round trip would test the stamp without that particular redundant rejection. |
| +- **Generator changes:** marker holding and targeted freezing are legitimate scheduling changes; they do not weaken the invariant checks. R5-6 limits the retention-fixture claim. |
| +- **Physical format:** B/C’s `/ltx/<level>/` paths are filesystem-style. The pinned S3 client uses `<prefix>/<level-as-four-hex-digits>/<filename>`. A’s `0000/…0009/` description is correct. The adapter must explicitly reconcile this difference. |
| +- **Validation claim:** §14.2.6 points to §15 step 8 for real LTX validation, but that section records AWS object-operation checks, not the required restore/replicate/retention tests. |
| + |
| +The claim-owner questions are answered by A: **Q1** chooses captured revisions, subject to R5-4’s durable initialization; **Q2** requires legacy adoption, not deletion; **Q3** assigns sweep protection to A and generation-specific version selection to B. |
| + |
| +| Artifact | Ready for Phase 1 implementation planning? | Reason | |
| +|---|---|---| |
| +| **A — claim rev 6.2** | **No, as the joint contract** | Finish durable stamp initialization and replacement ordering. R4’s regional sweep and purge-transition defects are closed. | |
| +| **B — moves rev 7.5** | **No** | Define real replication initialization, checksum verification, retention-compatible restoration and the full-snapshot cut budget. | |
| +| **C — model at `cdc98845`** | **No, as the planning gate** | Stronger oracle and witness evidence, but key production behaviors are assumed or omitted; stamps are not encoded exactly. | |
| + |
| +Build the claim primitive first after resolving its stamp contract. The remaining changes do not require reopening the product rulings. |
| + |
| +--- |
| + |
| +**FIRST PROMPT:** |
| +Joint independent round-5, read-only review of two CARLOS specs and their executable model. |
| + |
| +**WHAT:** |
| +Assess prior fixes, model fidelity, new defects and Phase 1 planning readiness. |
| + |
| +**STATUS:** |
| +Review complete: one P1, four P2 and one P3. Go execution was sandbox-blocked. |
| + |
| +**NEEDED:** |
| +Nothing for this review. |
| + |
| +**RECOMMENDED:** |
| +Resolve the pinned-library contracts and stamp lifecycle, align C, then run real-library integration tests and the model gate. |
| + |
| +**SESSION:** |
| +Safe to close. No files changed; nothing remains running. |
| \ No newline at end of file |