carlos / platform Public

spec: host lifecycle claim rev 6.6, writer epochs (R7-1, amadan #225)

Clean close writes closed.json after every upload is acknowledged; anything
else is lost replication state; a cold recovery is an installing CAS with a
new holder.generation and stamp; writers are bound to their generation's
prefix. Joint R7 copied unedited.

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

claude 3 weeks ago b10547e12ad88ccfba66821a223237600fbc82fa parent e0e3a82

2 files changed, +237 −1

docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md +60 −1
docs/superpowers/specs/CODEX-FINDINGS-JOINT-R7.md +177 −0

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 64b4051d0..e6d81f41b 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,7 @@

# The host lifecycle claim

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

+Design, 2026-10-04, **rev 6.6**. Joint rounds 6 and 7 judged the claim ready for primitive planning. Rev

+6.5 added the R6-4 rule. Rev 6.6 adds writer epochs (R7-1, amadan #225). A small primitive cited by:

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

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

@@ -826,6 +827,63 @@ 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

independent processes, with pauses between validation and the write.

+### 6.4a Writer epochs (R7-1, amadan #225)

+**The hazard.** Litestream writes each file to a key built from its level

+and TXID range only, and it writes unconditionally. A dead writer's

+in-flight level-0 upload for `[N+1]` can land after the next writer has

+cold-restored and uploaded its own `[N+1]`. The old file then replaces

+the new one, and the next restore loses acknowledged writes. `lock.json`

+cannot revoke an upload S3 has already accepted.

+So **two writers whose uploads could overlap never share a generation**.

+- **Clean close.** A writer stopping cleanly does three things, in order:

+ 1. waits until **every** upload it issued has returned success;

+ 2. writes `<holder.location>/<generation>/closed.json` as

+ `{stamp, max_txid, closed_at}`, conditionally (`If-None-Match`, so it

+ is written once);

+ 3. releases its lease.

+ A writer that saw any upload fail, time out or come back ambiguous

+ writes no `closed.json`.

+- **Lost replication state, defined.** When a box admits a writer, it

+ continues the current `holder.generation` only if all of these hold:

+ - `closed.json` exists for that generation;

+ - its `max_txid` equals the generation's remote maximum TXID;

+ - its `stamp` is the box's own `active_stamp`.

+ Otherwise the previous writer may still have uploads in flight. That

+ covers a crash, an out-of-memory kill, lease expiry or takeover, a

+ shared-pool failover, a lost box, and a missing or unreadable marker.

+ Then replication state is **lost**, and the start is a **cold

+ recovery**. When in doubt, it is a cold recovery.

+- **A cold recovery is an installing CAS (§2, R6-4).** Before admitting

+ any write, the box CASes the claim, conditional on the observed

+ `holder.generation`. The CAS writes a **new `holder.generation`**, a

+ fresh op id that is never reused, and a **new `holder.stamp`** (the

+ resulting `gen`). It requires `op.exec` to be this box. The box then:

+ 1. restores from the old generation;

+ 2. activates the new stamp locally (§6.4);

+ 3. replicates **only** into the new generation's prefix.

+ It is never a same-generation restart. A writer from the old

+ generation that is still running is refused locally by the stamp (§6.4)

+ and remotely by the prefix. Its late uploads land in the old

+ generation, which nothing reads once the pointer has moved. They are

+ parked as residue by the at-rest sweep (§6.2a, dead generations).

+- **Writers are bound to their generation.** A writer's replica client

+ is constructed for the `{holder.location, holder.generation}` it

+ validated under, and refuses any key outside

+ `<location>/<generation>/`. That covers level-0 files, compaction,

+ snapshots and retention. A writer never re-reads the generation while

+ running. A new generation means a new writer.

+The moves spec owns the data-path side: restoring from one generation

+while replicating into another, and the deterministic tests for both

+completion orders and the race between initialization and the remote

+position (rev 7.8).

### 6.5 Door reads pinned to versions (J-N10)

The pull door's listing:

@@ -1070,6 +1128,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 |

+| J7-R7-1 | §6.4a writer epochs: clean close, lost replication state, cold recovery as an installing CAS, generation-bound writers |

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

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

new file mode 100644

index 000000000..9f4ee39de

--- /dev/null

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

@@ -0,0 +1,177 @@

+**A is ready for claim-primitive implementation planning. B and C are not yet ready as the moves Phase 1 baseline.** The same-generation late-upload hazard is a P1: it can lose writes that the replacement process has successfully replicated.

+Reviewed A at `d36adcfa`, B/C/D at clean HEAD `05f7250f`, the round-6 findings, change note, facts write-up, claim-owner answers, production integration and cached pinned-library sources. AGENTS.md was read first.

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

+```

+This is a static review; I did not reproduce the reported sweeps. `bash -n internal/sim/hostlife/mutate.sh` passed. No files changed.

+**Round-6 dispositions**

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

+| R6-2: facts tests accepted loss | Resolved | D: resolved for the named assertions; C does not establish library facts | Exact N+1, nine-row survival, original-continuation disappearance, rooted refusal and newest-restore count are asserted. The broader Store gate still has limits below. |

+| R6-3: unpriced second restore | Resolved for that finding | C’s budget: resolved; lifecycle remains abstracted | B reuses the built database; arithmetic now separates regional S3 and disk costs and includes verification. C still represents installation through its simplified snapshot-and-restore path. |

+| R6-5: replay bytes | Partly | D: resolved encoder assertion; C abstracts bytes | Persisted timestamps fix deterministic encoding, but the specification conflates the pre-PUT input journal with the completed manifest; R7-4 below. |

+**R7-1 — P1: a cold recovery can reuse an LTX key while the previous writer’s upload remains in flight.**

+B [§5.1, especially its late-upload conclusion](/home/paulca/amadan.net/carlos/platform-moves-design/docs/superpowers/specs/2026-10-02-move-any-app-design.md:784); production [replica construction](/home/paulca/amadan.net/carlos/platform-moves-design/internal/lease/lease.go:283).

+The round-7 hazard is valid. Use a small database so both uploads are single-part PUTs:

+1. Generation G is remotely restorable through N.

+2. Process A sends `[N+1,N+1]`. The request remains outstanding; A dies and loses its disk.

+3. After acquiring the lease, B restores G through N. Ordinary cold recovery does not change G.

+4. B accepts new writes and successfully uploads its own `[N+1,N+1]`.

+5. A’s outstanding PUT completes afterward, replacing the current object at that key.

+6. A subsequent cold restore reads A’s file and loses B’s successfully replicated writes.

+The pinned S3 client constructs `PutObjectInput` without `If-Match`, `If-None-Match` or a lease token. Its object key contains only prefix, level and TXID range. [Pinned S3 client](https://raw.githubusercontent.com/benbjohnson/litestream/v0.5.14/s3/replica_client.go).

+CARLOS’s lease protects ownership of **another object**, `lock.json`. Renewal failure, cancellation, process death and compute fencing cannot revoke an already accepted data PUT. Waiting for lease expiry therefore does not establish that old data requests have finished.

+There is also a second schedule: the old file appears after B has initialized its local position but before `Replica.Sync` calculates the remote position. The library can then regard remote N+1 as already uploaded and skip B’s different local N+1. See [the pinned upload loop](/home/paulca/go/pkg/mod/github.com/benbjohnson/litestream@v0.5.14/replica.go:134).

+Both files can pass CRC verification. SQLite integrity checking does not establish which acknowledged history they contain. Later deltas can also combine pages from incompatible histories.

+**Fix:** give recovery that loses replication state a fresh, durably selected generation or writer epoch. Restore a version-pinned baseline into it, install its snapshot and anchor, then publish it under the claim before admitting writes. All subsequent L0, compaction, snapshot and retention operations must remain confined to that epoch.

+Conditional writes can help, but **adding create-only PUT alone is insufficient**:

+- If A wins, B must detect differing bytes and fail closed; it must not treat existence or a higher remote TXID as successful replication.

+- The remote-position shortcut must also enforce that identity.

+- Multipart completion needs equivalent conditions.

+- Delete markers can make a key eligible for creation again. [AWS conditional-write semantics](https://docs.aws.amazon.com/AmazonS3/latest/userguide/conditional-writes.html).

+A replica-client fence that merely checks the lease before sending has the same in-flight gap. A server-enforced publication fence or disjoint generation paths are needed. Reserving only N+1 with another unconditional anchor does not supply that fence.

+Add deterministic tests for **both completion orders**, the initialization/remote-position race, and cold restoration after B’s acknowledged write.

+**R7-2 — P2: the new oracle mask can hide later durable writes.**

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

+`exemptKeys` permanently masks every key touched by any exempt write in the incarnation. It does not stop masking when a later, non-exempt write establishes that key’s value.

+Concrete counterexample:

+- An exempt pre-crash write touched K.

+- The replacement durably updates or deletes K.

+- A stale upload restores the wrong value of K.

+- Another restored transaction supplies a sufficiently high `db.TX`.

+The numerical check at line 504 passes, and the state comparison removes K from both sides. The cold-restore oracle accepts the loss.

+**Fix:** represent uncertainty for particular writes and recovery histories, not permanent exemptions for keys. A later required write must restore the assertion for that key. Also check required write coverage using the model’s existing write identities; a maximum lineage TXID is insufficient after a fork.

+The unmasked local check may catch some schedules, but a correct warm database beside an incorrect replica can pass it. Consequently, “not found in 100,000 seeds” does not clear R7-1.

+**R7-3 — P2: retention can still remove newest L0.**

+[ltx_test.go:373](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/ltx_test.go:373), [ltx_test.go:387](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/ltx_test.go:387).

+The fix protects newest L0 only in the first deletion loop. The second deletes every L0 whose Max is below the previous snapshot.

+A reachable scheduling shape is:

+- Local position reaches 10 while uploads beyond 3 remain queued.

+- Compaction sees L0 `{1,2,3}`, preserves 3 and publishes snapshot 10.

+- Uploads 4 and 5 finish; 6 stalls; local position advances to 11.

+- Compaction preserves 5, publishes snapshot 11, then expires everything below previous snapshot 10—including L0 5.

+Remote L0 becomes empty, unlike pinned retention, which preserves its newest file. This creates artificial anchor-required recoveries and distorts mutation counts.

+**Fix:** preserve newest L0 in every retention path and add a witness with local position ahead of uploaded position. This is the unfinished round-6 fidelity correction, not a request to implement the explicitly deferred time-based retention model.

+**R7-4 — P2: the build-input journal and completion manifest need distinct states.**

+B [§5.1 step 2](/home/paulca/amadan.net/carlos/platform-moves-design/docs/superpowers/specs/2026-10-02-move-any-app-design.md:661), [§7.6 `building`](/home/paulca/amadan.net/carlos/platform-moves-design/docs/superpowers/specs/2026-10-02-move-any-app-design.md:1554).

+Step 2 requires encoding inputs persisted in the install manifest before PUTs. The phase table says to write that manifest afterward and declares `building` done when “the install manifest exists.”

+Following the former ordering literally, a crash after persisting inputs but before completing the snapshot and anchor leaves an existing manifest that satisfies the latter completion predicate.

+**Fix:** distinguish a durable build intent from a completed install manifest, either as separate objects or explicit states. Completion must require acknowledged artifact identities and verification results. Publish `generation.json` only from the completed state. Add crash cases between input persistence, each upload and completion publication.

+**R7-5 — P3: the Store gate promises more maintenance coverage than it asserts.**

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

+The test logs L2/L3 but asserts only L1 existence. It requires a snapshot newer than the original, not that snapshot retention removed an older one. “Exact contents” means row count; every inserted body is identical.

+Thus an upgrade disabling L2/L3 compaction or snapshot deletion can still pass. Equal-count payload damage is also outside its assertions.

+**Fix:** assert the maintenance events claimed, compare distinct row contents including updates/deletes, and force a restore that consumes compacted continuation files. Prefer observable completion conditions over fixed sleeps.

+**What D establishes**

+The three central facts now have useful, strict tests:

+- **Anchor:** installed L9 plus synthetic L0 `[N,N]` leads to exactly `[N+1,N+1]`, followed by restoration of all expected rows.

+- **Integrity:** real L0, snapshot and compactor output uses `HeaderFlagNoChecksum`, with file CRC verification and no post-apply database checksum.

+- **Root advancement:** genuine retention removes the original root’s continuation; the rooted restore refuses, while restoration from the successor succeeds.

+The new Store test materially improves lifetime grounding: it uses metadata isolation, real Store monitors, compaction levels, snapshot rotation and time-based L0 expiry across repeated restores. It does not run through `Held` or the activator, and it **closes the Store cleanly before each disk wipe**.

+| Production difference | Consequence |

+|---|---|

+| S3 listing uses filename order; ordinary retention ages files using `LastModified` | Copies and late uploads age differently from the file client’s encoded-timestamp mtime. |

+| Versioned objects and delete markers | File replacement/deletion cannot test version visibility or conditional-write behavior. |

+| Outstanding uploads across writer replacement | The fixture does not exercise R7-1. |

+| Production intervals and lease lifecycle | Shortened monitors test maintenance interaction, not production timing or fencing. |

+The timestamp difference does not invalidate N→N+1 initialization or the CRC finding. It does limit retention-timing equivalence. S3 does **not** order these listings by `LastModified`; the package/spec wording should distinguish ordering from aging.

+**Synthetic-anchor safety is supported for the tested pinned-library paths, but not established across arbitrary upgrades.** The new gate exercises much more of its lifetime, subject to R7-5. Keep the versions pinned and require these tests plus backend concurrency tests before upgrading. The anchor establishes a replication position; it does not establish writer ownership.

+**Model fidelity and classifications**

+The five requested stamp rules match A:

+- capture at work selection;

+- equality against active stamp under the guard;

+- activation retires the old active stamp;

+- artifact retirement changes no stamps;

+- missing local record refuses.

+The return-to-source correction and artifact retagging also match rev 6.5. This is exact for C’s represented DB/files artifacts, not a proof over every production inventory item.

+The legacy-prefix fix correctly keeps `g-<op>/` in the legacy location. The upload queue correctly prevents advancing past its outstanding head and retries that head’s bytes. That fixes the original non-sequential-upload fault; it does not prevent different process lifetimes from assigning different bytes to the same TXID.

+Root selection, overlap preference and successor advancement match the intended abstraction. Retention has R7-3. The model also does not reproduce the real first full L0 upload after cold initialization or the separate initialization/remote-position observations involved in R7-1.

+Static counting confirms **34 scenarios and 110 baseline/subset/full-set executions**. The harness requires every proper subset to hold and the full set’s first violation to match its named failure. The fourteen expected misses remain eleven combination-only rules, two liveness rules and one unreachable rule. Those classifications are honest **within the selected scenarios**; they do not establish global minimality. Witness-only coverage for `live-set-region` and the deliberately malformed `restore-gap-closed` fixture is clearly bounded.

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

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

+| **A — claim rev 6.5** | **Yes, primitive first** | The claim and stamp contracts are sufficiently explicit. Recovery generation selection must integrate with it. |

+| **B — moves rev 7.7** | **No** | Resolve same-generation recovery fencing and distinguish build intent from completed publication. |

+| **C — executable model** | **No, as the planning gate** | Repair the durability oracle and newest-L0 preservation; encode and exercise the late-upload schedules. |

+---

+**FIRST PROMPT:**

+Joint independent round-7 read-only review of the claim, moves, model and library spike.

+**WHAT:**

+Assess prior fixes, library grounding, model fidelity and Phase 1 readiness.

+**STATUS:**

+Complete: one P1, three P2s and one P3; Go execution sandbox-blocked.

+**NEEDED:**

+Nothing for this review.

+**RECOMMENDED:**

+Resolve recovery generation fencing, repair the oracle, then rerun deterministic cases and sweeps.

+**SESSION:**

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

\ No newline at end of file