carlos / platform Public

spec: host lifecycle claim rev 6.5, holder.stamp follows op.exec (R6-4)

Joint round 6 judged rev 6.4 ready for implementation planning. Rev 6.5 adds
the invariant that any CAS changing op.exec writes holder.stamp, returning
an existing installation's stamp on a return-to-source. Joint R6 copied
unedited.

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

claude 3 weeks ago d36adcfaedeab95c7c56e9478905a6970095ceee parent 697f0f9

2 files changed, +182 −1

docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md +17 −1
docs/superpowers/specs/CODEX-FINDINGS-JOINT-R6.md +165 −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 88525d4b8..4c460dc2f 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-04, **rev 6.4**. A small primitive cited by:

+Design, 2026-10-04, **rev 6.5**. Joint round 6 judged rev 6.4 ready for claim-primitive implementation planning. Rev 6.5 adds one rule for R6-4. A small primitive cited by:

- **#199**, deleting an instance and parking its data:

`2026-10-02-replica-ownership-design.md`, which this spec supersedes

@@ -147,6 +147,21 @@ Field rules:

Each writes `holder.stamp = its own resulting gen`. A transition that

doesn't change the installation leaves `holder.stamp` alone.

+ **Invariant (R6-4).** `holder.stamp` always names the installation that

+ `op.exec` should be running. **Any CAS that changes `op.exec` writes

+ `holder.stamp` in the same write:**

+ - a new resulting gen, if the CAS makes a new installation current;

+ - the **existing** stamp of the installation it returns execution to,

+ taken from the operation's journal, if it makes an existing

+ installation current again.

+ A dirty rollback's return to the source is the second case. It writes

+ the source's pre-move stamp `S`, not the flip's `F`. The source's

+ initialization then finds `holder.stamp == active_stamp == S`, and

+ changes nothing. The probe's later CAS issues `R`, and activating `R`

+ retires `S`. `F` was only ever active on the target, so its records

+ are retired there.

- **`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

@@ -1047,6 +1062,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 |

+| J6-R6-4 | §2 `holder.stamp` invariant: any CAS that changes `op.exec` writes `holder.stamp` |

| moves 7.6 notes | §6.4 stamp captured at selection; only activation and retire-installation move stamps; §6.2a non-incarnation children |

## 13. S3 behaviour this relies on, verified

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

new file mode 100644

index 000000000..7585bef59

--- /dev/null

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

@@ -0,0 +1,165 @@

+**A is ready for claim-primitive implementation planning. B and C are not yet ready as the joint moves Phase 1 baseline.** No new P1 established. The main remaining problems are a model oracle that modifies the replica, incomplete regression assertions, and an understated cut budget.

+Reviewed A at `697f0f9f`, B/C/D at clean HEAD `f7f7c438`, the round-5 findings, change note, facts write-up and claim-owner answers. I read AGENTS.md first. Three independent GPT-6 subreviews supported this review; Opus was unavailable.

+`go test ./internal/sim/... -count=1` failed before compilation:

+```text

+go: creating work dir: mkdir /home/paulca/.cache/tmp/go-build…: read-only file system

+```

+These are static findings. Published sweep results were not independently reproduced. `bash -n internal/sim/hostlife/mutate.sh` passed. No files changed.

+**Round-5 dispositions**

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

+**R6-1 — P2: the restore oracle changes the system it is checking, and anchor initialization bypasses durability.**

+[sim_test.go:464](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/sim_test.go:464), [protocol_test.go:279](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/protocol_test.go:279).

+`checkDurable` calls `w.restore`, documented as reading the bucket and writing nothing. Restore now issues an anchor PUT whenever its restored position exceeds remote L0.

+Consequently, an invariant check can:

+- repair missing replication-position evidence without a real cold wake;

+- create versions, alter durability bookkeeping and consume scheduling randomness;

+- enqueue another delayed request.

+`final()` checks quiescence **before** these calls, so it can finish after its own oracle creates pending work.

+Separately, restore sets `db.Pos = cur`, ignores the anchor PUT’s result, and returns an openable database. Holding that PUT leaves no remote anchor, yet C can replicate at N+1. The real library would still derive its initial position from the remote L0 files actually present.

+**Fix:** separate pure restoration from stateful replication initialization. Oracles must use the pure calculation. Actual initialization must acknowledge the anchor before opening replication and derive the resulting position from durable evidence. Add an oracle-purity assertion and a witness that holds the anchor PUT across an attempted open. Rerun the baseline and mutations afterward.

+**R6-2 — P2: D’s claimed regression gate explicitly accepts the data-loss behavior it should reject.**

+[facts_test.go:414](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/litestreamfacts/facts_test.go:414), [facts_test.go:564](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/litestreamfacts/facts_test.go:564).

+The L0-expiry test passes when `restarted` is true and only **seven of nine rows** survive. Thus an upgrade that removes the newest L0 file, restarts numbering and loses the new writes can pass this “facts” gate.

+The retention test also:

+- accepts the original continuation remaining;

+- logs, but never asserts, the newest restore’s row count.

+The anchor test requires advancement **past N**, rather than asserting the claimed next position N+1.

+These checks support observations from the reported run, but not B’s promise that changing those facts makes an upgrade fail here first.

+**Fix:** assert retained L0 identity, exact next TXID, disappearance of the original continuation, the expected rooted-restore refusal, and exact restored contents. Treat unexpected alternative behavior as a failed contract requiring review.

+**R6-3 — P2: T11 still omits one full restore from the cut.**

+B §7.3 T11 and [§7.6](/home/paulca/amadan.net/carlos/platform-moves-design/docs/superpowers/specs/2026-10-02-move-any-app-design.md:1460); [budget_test.go:60](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/budget_test.go:60).

+`building` restores the staged replica, writes the snapshot and writes the anchor. These are the three full-database passes priced by the budget.

+The later `restored` phase explicitly performs **another cold restore** from the installed generation before probing. It has no budget term.

+Using the test’s arithmetic:

+| Workload | Time |

+|---|---:|

+| 3 GiB; local rate 200 MiB/s; cross-region rate 10 MiB/s; one probe | 108.68 s |

+| Additional cold restore | 15.36 s |

+| Actual modeled total | **124.04 s** |

+T11 admits that workload into the 120-second window.

+**Fix:** budget the fourth pass, or explicitly reuse the verified database constructed during `building` and remove the second restore from the protocol. Price regional S3 reads/writes separately where disk throughput does not represent them.

+Also correct the example: B and the change note say **50 MiB/s**, but the test uses **200 MiB/s**. At 50 MiB/s, the existing three-pass estimate already refuses the 2 GiB example.

+**R6-4 — P3: rollback stamp execution differs from the specified lifecycle.**

+B [§6.4](/home/paulca/amadan.net/carlos/platform-moves-design/docs/superpowers/specs/2026-10-02-move-any-app-design.md:1078); [moves_test.go:57](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/moves_test.go:57), [moves_test.go:1128](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/moves_test.go:1128).

+B says the source’s pre-move stamp S stays active through dirty installation, retiring when the recovery probe’s new stamp R activates.

+C instead does this:

+1. Flip writes target stamp F.

+2. Rollback returns execution to the source while `holder.stamp` remains F.

+3. `role()` calls `initRecord`, activating F on the source and retiring S.

+4. Installed DB/files receive F.

+5. The probe issues R, but the artifacts retain F.

+Moreover, `retireArtifacts` ignores its arguments; callers directly remove selected objects. C therefore does not exercise the real inventory’s stamp-filtered retirement.

+**Fix:** specify the return-to-source transition, including recovery after loss of the local record, and define artifact tagging when R activates. Encode selective retirement and assert the intended tags.

+This is a demonstrated contract/fidelity discrepancy, not demonstrated data loss.

+**R6-5 — P3: replayed anchor encoding is not byte-identical as promised.**

+B §5.1 steps 2–3 and §7.6 `building`; [facts_test.go:188](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/litestreamfacts/facts_test.go:188).

+B requires late/replayed snapshot and anchor PUTs to repeat identical bytes and directs builders to encode as the spike does. The anchor encoder uses `time.Now().UnixMilli()`.

+Rebuilding the same sealed database at another time changes the header, CRC and bytes. The logical database can remain identical, so this alone does not establish lost writes; it does invalidate the stated immutable-byte argument.

+**Fix:** persist encoding inputs, including timestamp, or reuse a durably encoded artifact. Test byte equality across replay.

+**What D establishes, and what remains unproven**

+The three central changes are grounded in the pinned implementation:

+- **Anchor:** the anchor test exercises snapshot installation, subsequent replication and a later cold restore that retains the added rows. Source inspection supports the N→N+1 initialization: newest remote L0 supplies position; the synthetic WAL metadata causes a fresh full upload. [Pinned database implementation](https://raw.githubusercontent.com/benbjohnson/litestream/v0.5.14/db.go).

+- **Checksums:** D directly exercises the L0 writer, snapshot writer and compactor. They produce `HeaderFlagNoChecksum` files with file CRCs, not post-apply database checksums.

+- **Root advancement:** D exercises genuine retention functions and the genuine restore planner. The reported old-root gap is credible, but R6-2 prevents treating its present assertions as a strict regression gate.

+The file client does **not** conceal an identified incompatibility in basic anchor initialization or checksum verification. It does conceal relevant lifetime differences:

+| Production | D |

+|---|---|

+| `Held.Replicate` opens a `litestream.Store`, with maintenance monitors | Opens a DB and invokes maintenance manually |

+| L1/L2/L3 intervals are 1h/6h/24h; startup maintenance can run immediately | Separate, sequential fixture operations |

+| L0 expires through time-based maintenance | Rotation fixture expires L0 by TXID; a separate test exercises time expiry |

+| S3 listings use object `LastModified` | File client preserves the encoded LTX timestamp as filesystem mtime |

+| Versioned objects, delete markers and delayed completion | Ordinary file replacement/deletion |

+See [production setup](/home/paulca/amadan.net/carlos/platform-moves-design/internal/lease/lease.go:283), [pinned Store](https://raw.githubusercontent.com/benbjohnson/litestream/v0.5.14/store.go), and [pinned S3 client](https://raw.githubusercontent.com/benbjohnson/litestream/v0.5.14/s3/replica_client.go). Copied or delayed objects can therefore age differently for retention.

+**Synthetic-anchor safety is supported for initial use on these pinned versions, not established over its entire lifetime or across upgrades.** Static inspection found no pinned compaction requirement that the first input start at 1, and the library preserves newest L0. But D never takes an **anchor-derived lineage** through compaction, retention and repeated cold restoration; those tests use separate setups.

+The missing integration gate is one anchored lineage through production Store configuration, repeated writes, L1–L3 compaction, time-based L0 expiry, snapshot rotations, disk loss and cold restoration, asserting exact positions and contents. Backend tests should cover S3 timestamp and version behavior. No production experiment is needed for this review.

+**Model fidelity and classifications**

+The five requested stamp primitives are correctly encoded: selection captures the stamp; guarded admission checks equality; activation retires the previous active stamp; artifact retirement moves neither stamp set; missing records refuse. R6-4 limits the stronger claim that the complete rollback/artifact lifecycle is exact.

+Root advancement and the old-root gap are represented. Retention is an approximation: [compaction](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/ltx_test.go:358) deletes every input L0, including the newest. This creates anchor-required cold restores that normal pinned retention should not create. I am treating this as requested fidelity analysis, **not reopening the deferred L0-retention work in §14.2.6**.

+Both self-found fixes are sound within C:

+- Legacy `g-<op>/` children remain part of the legacy host location.

+- `ship` queues uploads in order and retries the same head blob before advancing; delayed originals can add duplicate versions without skipping a range.

+The classifications are honestly bounded. Static inspection confirms **32 witnesses and 106 baseline/subset/full-set executions**. Every proper subset must hold; the full set’s first violation must match the named failure. The fourteen expected misses comprise eleven combination-only rules, two liveness rules and one unreachable rule.

+That establishes necessity within each selected scenario, not global minimality. `live-set-region` and `restore-gap-closed` are honestly witness-only; the latter deliberately supplies malformed replica state. R6-1 nevertheless means the published model results need rerunning after the oracle stops intervening.

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

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

+| **A — claim rev 6.4** | **Yes, primitive first** | The requested stamp and retirement contracts are explicit. Resolve the return-path detail jointly with B/C. |

+| **B — moves rev 7.6** | **No, as the joint baseline** | Correct the cut workload and tighten the library integration/upgrade gate and replay contract. |

+| **C — model** | **No, as the planning gate** | Separate oracle observation from anchor installation, enforce anchor durability, align rollback stamps, then rerun the evidence. |

+---

+**FIRST PROMPT:** Joint independent round-6 read-only review of A–D.

+**WHAT:** Assess prior fixes, library grounding, model fidelity and planning readiness.

+**STATUS:** Complete: three P2 and two P3 findings; Go execution sandbox-blocked.

+**NEEDED:** Nothing for this review.

+**RECOMMENDED:** Fix oracle/anchor initialization, strengthen D, reconcile the cut budget, then rerun validation.

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

\ No newline at end of file