amadan
spec: host lifecycle claim rev 6.8, writer sessions (joint round 8)
Every writer session is admitted by an AdmitWriter claim CAS (holder.session = its gen; warm or cold; journals the predecessor; never replaces the op, so recovery happens inside landing/restoring/reverting/probes). Clean-close certificates are per session and never deleted; a warm continuation moves the session forward, so old markers can't authorize anything. Baseline provenance from journalled predecessor and writer-written lineage. Empty bootstrap. Withdraws rev 6.7's delete-the-marker rule. Joint R8 copied.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2 files changed,
+318
−86
docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md+134 −86docs/superpowers/specs/CODEX-FINDINGS-JOINT-R8.md+184 −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 722a354e1..ff6aeb578 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,9 +1,9 @@ |
| # The host lifecycle claim |
| -Design, 2026-10-04, **rev 6.7**. Joint rounds 6 and 7 judged the claim ready for primitive planning. Rev |
| +Design, 2026-10-04, **rev 6.8**. Joint rounds 6 and 7 judged the claim ready for primitive planning. Rev |
| 6.5 added the R6-4 rule. Rev 6.6 added writer epochs (R7-1, amadan #225). |
| -Rev 6.7 answers the moves session's three notes on §6.4a: consuming the |
| -marker, the first wake, and the warm baseline. A small primitive cited by: |
| +Rev 6.7 answered the moves session's notes on §6.4a. Rev 6.8 rewrites §6.4a |
| +around writer sessions, for joint round 8 (R8-1 to R8-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 |
| @@ -93,7 +93,8 @@ replaced whole with conditional writes (`If-Match` on the ETag read). |
| "incarnation": "<hex>", "created_at": "<record CreatedAt>", |
| "location": "instances/shop.bab.oncarlos.com/<incarnation>", |
| "generation": "<op id of the installed generation, or \"\">", |
| - "stamp": 41 |
| + "stamp": 41, |
| + "session": 57 |
| }, |
| "op": { |
| "kind": "serving", |
| @@ -165,6 +166,8 @@ Field rules: |
| 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.session`** is the current writer session's admission `gen` |
| + (§6.4a). Every `AdmitWriter` CAS moves it forward. |
| - **`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 |
| @@ -829,90 +832,134 @@ 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) |
| +### 6.4a Writer sessions and epochs (R7-1, R8-1 to R8-4, 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 |
| +**The hazard.** Litestream writes each file to a key built only from its |
| +level and TXID range, 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`. |
| - |
| - **The marker is consumed when a writer opens it.** The admitted writer |
| - deletes `closed.json`, by the exact version it read, before it issues |
| - its first upload. If that delete fails, the writer does not continue |
| - the generation; it takes the cold-recovery path instead. A writer that |
| - continues after a clean close and then crashes with uploads in flight |
| - therefore leaves no marker, and the next wake recovers cold. The delete |
| - marker this leaves lets the writer's own later clean close write the |
| - key again with `If-None-Match`. |
| - |
| - **The first wake after a create or an adoption is a cold recovery.** No |
| - writer closed the origin generation. Nobody writes a marker it didn't |
| - earn, and an empty generation is not exempted, because a first writer |
| - that crashed with `[1,1]` in flight leaves the same state. A new |
| - instance's first generation snapshots an empty or near-empty |
| - database, so the cost is small. An adoption pays one full snapshot, |
| - once. |
| - |
| - 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. establishes its **baseline**: |
| - - **The warm local database**, if all of these hold: |
| - - its lineage marker (`<dbPath>.gen`) names the old generation; |
| - - it passes its integrity check; |
| - - the box's local stamp record shows **this box was the old |
| - generation's active writer**. |
| - |
| - A crash without disk loss leaves that database holding |
| - acknowledged writes that were never uploaded, so it is a superset |
| - of the remote. |
| - - **Otherwise, a restore from the old generation's remote.** Another |
| - box may have advanced the remote past this box's copy. |
| - 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). |
| +uploaded its own `[N+1]`, replacing it. The next restore then loses |
| +acknowledged writes. Neither `lock.json` nor any client-side deadline |
| +can revoke an upload S3 has already accepted. |
| + |
| +**The rule.** Two writers whose uploads could overlap never share a |
| +generation, and **every** path that opens replication goes through |
| +writer admission. That includes: |
| +- an ordinary wake; |
| +- a committed move's target serving while the claim is still `landing`; |
| +- a restarted probe; |
| +- a reverted source; |
| +- an opened rollback recovery; |
| +- a push's writer. |
| + |
| +#### Writer sessions in the claim (R8-1) |
| + |
| +`holder.session` is the claim `gen` of the CAS that admitted the |
| +current writer session. |
| + |
| +**`AdmitWriter`** is one claim CAS, made by the box **before the writer |
| +issues any upload**. It requires: |
| +- the observed `holder.session` and `holder.generation`; |
| +- `op.exec`, or the moves spec's phase table for the current op, to |
| + permit this box to open replication. |
| + |
| +It writes: |
| +- `holder.session = its own resulting gen`; |
| +- a **journal entry** in `op.journal.writers`: |
| + `{session, box, generation, stamp, mode, predecessor: {session, box, |
| + generation, stamp}}`. The predecessor is copied from the claim it |
| + observed. |
| +- in **cold** mode, a new `holder.generation` (a fresh op id) and |
| + `holder.stamp = the resulting gen`. This is an installing CAS (§2, |
| + R6-4). |
| + |
| +It never replaces the operation. Kind, id, phase, intent, participants, |
| +obligations and the rest of the journal are kept. **Recovery inside |
| +`landing`, `restoring`, `reverting` or a probe is therefore an |
| +`AdmitWriter` within that operation**, never a new operation (R8-2). The |
| +moves spec's phase table says which box may be admitted in which phase. |
| + |
| +#### The clean-close certificate is one-use by construction (R8-1) |
| + |
| +A writer session closes cleanly only after **every** request it issued |
| +has completed with success (R8-5, the moves spec's evidence rule). That |
| +includes: |
| +- every level-0 upload; |
| +- every compaction and snapshot upload; |
| +- every retention delete; |
| +- every timed-out original whose outcome is unknown. |
| + |
| +A writer that cannot prove completion writes no certificate. |
| +Litestream's `Replicator.Close` drops the initial `SyncAndWait` error |
| +today, so certificate eligibility needs its own evidence, not `Close`'s |
| +return value. |
| + |
| +A clean writer then writes |
| +`<location>/<generation>/closed/<session>.json` |
| +`{session, box, max_txid, closed_at}`, with `If-None-Match`. The key is |
| +per session, and the marker is never deleted or reused. |
| + |
| +**Warm continuation** is an `AdmitWriter` in **warm** mode. It is legal |
| +only if `closed/<holder.session>.json` exists for the observed session, |
| +its `max_txid` equals the generation's remote maximum TXID, and its `box` |
| +is the admitting box or the warm baseline rules below allow otherwise. |
| +The admitting CAS moves `holder.session` forward, so that marker now |
| +names a dead session. A delayed, replayed or re-created marker for any |
| +earlier session can never authorize anything again. No marker is ever |
| +deleted, and no S3 delete or version semantics are involved. (Rev 6.7's |
| +"consume the marker by deleting it" is withdrawn: deleting an exact |
| +version doesn't create a delete marker, and it can expose an older |
| +version.) |
| + |
| +Anything else is **cold**: no certificate for the observed session, a |
| +mismatched `max_txid`, or any doubt. That covers a crash, an |
| +out-of-memory kill, lease expiry or takeover, a shared-pool failover, a |
| +lost box, and a writer that continued and then crashed with uploads in |
| +flight. That last writer's own session has no certificate, whatever |
| +older certificates exist. |
| + |
| +#### Baselines and provenance (R8-4) |
| + |
| +A cold `AdmitWriter` journals its predecessor (`predecessor.session`, |
| +`.box`, `.generation` and `.stamp`) **before** the recovery stamp is |
| +activated anywhere. The new writer's baseline is: |
| +- **the warm local database**, only if all of these hold: |
| + - its local lineage file, written by the writer that opened it and |
| + naming `{generation, session}`, equals the journalled |
| + `predecessor.{generation, session}`; |
| + - `predecessor.box` is this box; |
| + - it passes its integrity check. |
| + |
| + Re-initializing a local stamp record from the current claim (§6.4) |
| + never writes a lineage file. So no claim read can manufacture evidence |
| + of earlier ownership; |
| +- **otherwise, a restore from the predecessor generation's remote.** |
| + |
| +The writer then activates the new stamp locally (§6.4), and replicates |
| +**only** into `<location>/<new generation>/`. |
| + |
| +#### Empty bootstrap (R8-3) |
| + |
| +The first writer after a create, or after an adoption with nothing |
| +replicated, is admitted cold with a fresh generation. A generation may be |
| +**empty**: until the first committed transaction, no LTX file is |
| +written, and no file with a zero TXID is ever written. The app may start |
| +and create its database before replication opens. The writer is admitted |
| +before its first upload, and that first upload is the first |
| +transaction's file. The moves spec owns the litestream mechanics: the |
| +level-0 anchor and snapshot rules for position 0. |
| + |
| +#### Generation-bound writers |
| + |
| +A writer's replica client is constructed for the `{location, generation, |
| +session}` it was admitted with. It refuses any key outside |
| +`<location>/<generation>/`: level-0, compaction, snapshot and retention. |
| +It never re-reads the generation, so a new admission means a new writer. |
| + |
| +An old writer's late uploads land in the old generation, or in the |
| +current generation **before** the session that superseded it opened. A |
| +cold successor has a new generation. A warm successor exists only after |
| +the old session certified that every one of its requests had completed. |
| +Dead generations are parked by the at-rest sweep (§6.2a). |
| ### 6.5 Door reads pinned to versions (J-N10) |
| @@ -1158,6 +1205,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 | |
| +| J8-R8-1 to R8-4 | §6.4a rewritten: writer sessions in the claim, per-session certificates (never deleted), admission inside any op, baseline provenance, empty bootstrap | |
| | moves 7.8 notes | §6.4a: marker consumed at open, first wake is cold, warm baseline only for the old generation's own writer | |
| | 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` | |
diff --git a/docs/superpowers/specs/CODEX-FINDINGS-JOINT-R8.md b/docs/superpowers/specs/CODEX-FINDINGS-JOINT-R8.md| new file mode 100644 |
| index 000000000..6b36fc31c |
| --- /dev/null |
| +++ b/docs/superpowers/specs/CODEX-FINDINGS-JOINT-R8.md |
| @@ -0,0 +1,184 @@ |
| +**A, B and C are not yet ready as the complete Phase 1 planning baseline.** Fresh writer generations are the right fix for R7-1, but marker reuse and admissions outside `serving` still permit the original collision. The library grounding and durability oracle have improved substantially. |
| + |
| +I reviewed A at `b10547e1` and B/C/D at clean HEAD `3c5f742a`. AGENTS.md was read first. The requested test command 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. |
| + |
| +The supplied change note contains no round-8 item; I used the committed diff and B §22.14. The answers file now includes **rev 6.7 answers**. Those clarify intent but do not change the requested rev 6.6 verdict. |
| + |
| +**Round-7 dispositions** |
| + |
| +| Finding | Spec | Model / executable evidence | Why | |
| +|---|---|---|---| |
| +| **R7-1: overlapping writers reuse LTX keys** | **Partly** | **Partly** | Fresh generations isolate the named schedules, but marker consumption/republication and non-`serving` admissions remain unsafe. | |
| +| **R7-2: permanent key exemptions hide durable writes** | **Resolved** | **Resolved** | Required writes are checked by identity; state is compared with replay of the carried writes. No permanent key mask remains. | |
| +| **R7-3: retention removes newest L0** | **Resolved** | **Resolved** | Both deletion paths preserve newest L0; the deterministic case exercises local position ahead of uploads. | |
| +| **R7-4: intent mistaken for completed installation** | **Resolved for the reported build path** | **Resolved within the artifact abstraction** | Separate intent/completion objects; snapshot and anchor precede publication. The model checks this ordering and crashes between steps. | |
| +| **R7-5: Store gate overclaims maintenance coverage** | **Resolved** | **D: resolved** | It now requires L1–L3 files, snapshot deletion, distinct contents with updates/deletes, and a restore requiring compacted continuation. | |
| + |
| +**R8-1 — P1: the clean-close certificate is not safely consumed once.** |
| + |
| +A §6.4a; [B §5.1 step 9](/home/paulca/amadan.net/carlos/platform-moves-design/docs/superpowers/specs/2026-10-02-move-any-app-design.md:850); [model admission](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/protocol_test.go:454); [installer PUT retries](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/world_test.go:509). |
| + |
| +There are two concrete failures. |
| + |
| +1. **Consumption is not awaited.** The model issues `rDelVer` and immediately starts the writer. Hold that delete; let the writer issue N+1, then crash with its disk before either request completes. The old marker still matches remote N and the active stamp. The replacement continues the generation, recreating R7-1. |
| + |
| + Rev 6.6 does not specify consumption at all. B adds consumption without an explicit successful-completion gate. The newer rev 6.7 answer supplies that gate, but C does not implement it. |
| + |
| +2. **A delayed marker retry can recreate a consumed certificate.** Recovery writes its installer marker through `ackedPut`, which proceeds after one attempt succeeds while older attempts can remain outstanding. After the admitted writer deletes that marker, an older `If-None-Match` attempt can arrive while the key is absent and succeed. If the writer then crashes with N+1 outstanding, the recreated `{stamp,N}` still matches and authorizes another writer in the same generation. |
| + |
| +The claim-owner notes also contain an incorrect S3 premise: **deleting an exact version does not create a delete marker**. It removes that version and may expose an older version. Furthermore, `If-None-Match` permits creation when the current object is absent or a delete marker, so a tombstone alone would not solve delayed republication. [AWS DeleteObject](https://docs.aws.amazon.com/AmazonS3/latest/API/API_DeleteObject.html), [AWS conditional writes](https://docs.aws.amazon.com/AmazonS3/latest/userguide/conditional-writes.html). |
| + |
| +**Fix:** make clean-close authority a one-use certificate with durable consumption before any writer activity. For example, retain an open/closed state object changed by conditional writes, with a unique writer-session token preventing reuse of an earlier state. Alternatively, bind consumption to a monotonic claim field. A delayed old close must never authorize a subsequent session. Add separate witnesses for delayed deletion and delayed marker republication with a **matching** stamp and TXID. |
| + |
| +**R8-2 — P1: writer epochs are bypassed while lifecycle operations still admit writers.** |
| + |
| +[B §7.9](/home/paulca/amadan.net/carlos/platform-moves-design/docs/superpowers/specs/2026-10-02-move-any-app-design.md:1797), [B §7.14](/home/paulca/amadan.net/carlos/platform-moves-design/docs/superpowers/specs/2026-10-02-move-any-app-design.md:1967), [model admission](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/protocol_test.go:379). |
| + |
| +The recovery CAS is allowed only from `serving`; the model checks replication state only when `!probe && op.Kind == "serving"`. |
| + |
| +A committed move admits public traffic while the claim remains `landing`, waiting for cleanup: |
| + |
| +1. Target A serves generation G and sends N+1. |
| +2. Its upload remains outstanding; A crashes and loses its database. |
| +3. Before finalization releases the claim, another wake restores G through N. |
| +4. That wake bypasses the epoch check because the claim is still `landing`. |
| +5. Its N+1 collides with A’s outstanding N+1. |
| + |
| +The same missing rule affects restarted probes, reverted-source writers and opened rollback recovery. A §6.4a says two potentially overlapping writers never share a generation; B/C implement a narrower rule. |
| + |
| +The new crash-with-disk fault is itself restricted to `serving`, so the sweep cannot exercise this committed-landing schedule. [Fault restriction](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/background_test.go:351). |
| + |
| +**Fix:** enforce writer-session admission for every path that opens replication. Define recovery within an existing lifecycle operation, preserving its journal, participants and obligations; do not replace that operation with an unrelated recovery. Test the collision during committed-but-unfinalized serving and during probe restart. |
| + |
| +**R8-3 — P2: first-wake recovery requires LTX files that cannot exist at position zero.** |
| + |
| +[B §7.14](/home/paulca/amadan.net/carlos/platform-moves-design/docs/superpowers/specs/2026-10-02-move-any-app-design.md:1968); [model recovery builder](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/moves_test.go:1691). |
| + |
| +Every create’s first wake now runs recovery, but a never-started instance can have no database and no replication position. The prescribed snapshot `[1,N]` then becomes `[1,0]`; its anchor would be `[0,0]`. |
| + |
| +Pinned LTX rejects zero minimum or maximum TXIDs. The model accepts the zero-position snapshot and skips the anchor, so it permits a bootstrap that the real encoder refuses. [Pinned header validation](/home/paulca/go/pkg/mod/github.com/superfly/ltx@v0.5.1/ltx.go:218). |
| + |
| +Production also deliberately starts a fresh application before replication because the application may create its database. [Existing first-boot ordering](/home/paulca/amadan.net/carlos/platform-moves-design/internal/activator/activator.go:1168). |
| + |
| +**Fix:** specify an empty-generation bootstrap explicitly. It must still allocate a fresh epoch, but either represent an empty installation without invalid LTX files or establish a valid initialized database and positive position before encoding. Preserve first-boot seed semantics. Add a real-library test starting with neither database nor replica. |
| + |
| +**R8-4 — P2: the warm-baseline rule lacks proof that this is the authoritative local database.** |
| + |
| +A §6.4a; [B recovery baseline](/home/paulca/amadan.net/carlos/platform-moves-design/docs/superpowers/specs/2026-10-02-move-any-app-design.md:1968); [model selection](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/moves_test.go:1682). |
| + |
| +A’s literal “restores from the old generation” can discard acknowledged, unuploaded writes even when the failed writer’s disk survives. B correctly allows the warm database, but matching `.gen` alone establishes identity, not freshness or prior writer ownership. A cached/restored copy of G at N must not replace G’s authoritative history through N+1 during takeover. |
| + |
| +The newer claim-owner answer requires three checks: matching generation, integrity, and a local record proving **this box was that generation’s active writer**. C checks incarnation and generation only. It does not encode the third condition. [Owner’s answer](/home/paulca/.cache/nearest-region/claim-rev61-answers.md:16). |
| + |
| +**Fix:** journal the predecessor’s generation, stamp and writer provenance before activating the recovery stamp. Use the warm database only with that provenance and integrity evidence, including committed WAL contents. Otherwise use a version-pinned remote restore. Reinitializing a stamp from the current claim must not manufacture evidence of earlier ownership. |
| + |
| +**R8-5 — P2: the model’s “every upload succeeded” condition checks only the current L0 queue.** |
| + |
| +[Clean close](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/ltx_test.go:304), [upload retry](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/ltx_test.go:332), [maintenance requests](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/ltx_test.go:425). |
| + |
| +Hold an L0 request until it times out; let its retry succeed. `ship` removes the queue entry and forgets the original request. `closeStep` can then write `closed.json` while that original remains outstanding. Compaction and snapshot requests are also outside its drain accounting. |
| + |
| +That differs from A/B’s explicit rule: any failed, timed-out or ambiguous upload prevents a clean marker. The existing witness holds all retries and completes them together, so it does not expose the difference. |
| + |
| +**Fix:** track every issued request for the writer lifetime, plus a sticky uncertainty flag. Include maintenance uploads. Add a witness where one retry succeeds while the earlier attempt stays unresolved. |
| + |
| +This matters when implementing #225: today’s `Replicator.Close` drops an initial `SyncAndWait` error, and a successful final close does not prove that every earlier background request succeeded. Marker eligibility needs its own evidence. [Production close](/home/paulca/amadan.net/carlos/platform-moves-design/internal/lease/lease.go:368). |
| + |
| +**R8-6 — P3: the retired-door coverage table contradicts its conclusion.** |
| + |
| +[B §14.2.5](/home/paulca/amadan.net/carlos/platform-moves-design/docs/superpowers/specs/2026-10-02-move-any-app-design.md:3252). |
| + |
| +The `door-reread+C3a` row says 414 failures, calls that “the partner’s count,” and gives the partner’s count as 361. Both retired rows still say the witness “violated,” with old door-failure counts. The following paragraph says the pairs add nothing. |
| + |
| +**Fix:** distinguish historical results from current results and remove claims of current witness evidence for retired witnesses. Aggregate failure counts alone do not establish redundancy. |
| + |
| +**What D establishes—and its limits** |
| + |
| +The tests establish the three requested facts for the tested, **nonempty** pinned-library fixtures: |
| + |
| +| Fact | Evidence | |
| +|---|---| |
| +| L9 plus synthetic L0 `[N,N]` continues at N+1 | Exact L0 ranges and subsequent restored row count are required. | |
| +| File integrity, without a post-apply database checksum | Real L0, snapshot and compactor output is decoded and verified with `HeaderFlagNoChecksum`, zero post-apply checksum and nonzero file CRC. | |
| +| The original root eventually loses its continuation | Two retention rounds remove that continuation; restoration rooted there must fail, while newest-root restoration must recover every expected row. | |
| + |
| +The revised [Store gate](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/litestreamfacts/facts_test.go:734) now provides useful lifetime coverage: repeated continuation, L1–L3 compaction, snapshot rotation/deletion, time-based L0 expiry, exact contents, and a final restore requiring L1 continuation. R7-5 is resolved. |
| + |
| +Its production fidelity remains bounded: |
| + |
| +- It constructs the same broad `DB`/`Replica`/`Store` shape and separate metadata directory. Production uses L1/L2/L3 intervals of 1h/6h/24h, default 24h snapshot interval/retention, five-minute L0 retention checked hourly, and a ten-second DB monitor. The spike accelerates these and forces each write through `SyncAndWait`. |
| +- Every simulated disk loss follows a **successful Store close**. It does not exercise abrupt replacement through `Held`, lease loss, or the activator. |
| +- File-client aging uses the encoded timestamp; ordinary S3 retention listings use `LastModified`. Filename ordering is distinct from aging, and B now says that correctly. |
| +- File replacement/deletion does not exercise version visibility, multipart requests, delayed completion, or the close-certificate protocol. |
| +- The new unconditional-PUT test inspects source text; it is not an S3 concurrency test and can skip if source discovery fails. |
| + |
| +**Synthetic anchors are supported by the tested pinned paths, not guaranteed safe across arbitrary upgrades.** The tests now exercise verification, compaction and retention substantially better. Keep the versions pinned and treat the spike as a required upgrade gate, supplemented by writer-session and backend-concurrency tests. The missing empty-bootstrap case is a concrete gap in the current grounding. |
| + |
| +**Model fidelity** |
| + |
| +The established stamp rules still match A §6.4 and rev 6.5: |
| + |
| +- capture at work selection; |
| +- equality with the active stamp under the guard; |
| +- activation retires the previous active stamp; |
| +- artifact retirement changes no stamps; |
| +- missing records refuse until initialization; |
| +- return-to-source restores S; the later installation activates R and retags its artifacts. |
| + |
| +That agreement covers the represented database/files inventory. **The new §6.4a rules are not exact**, for R8-1, R8-2 and R8-5. |
| + |
| +The three reported model repairs are present: |
| + |
| +- Full files replace state and carry the full write log. |
| +- The new crash-with-disk branch removes every process. Its disk fault still represents database loss, rather than loss of every local artifact. |
| +- Recovery takes stop evidence before choosing its baseline. |
| + |
| +The new durability oracle resolves R7-2: later required writes are no longer hidden by an earlier exempt write, and a high lineage TXID cannot substitute for the missing write’s identity. Its purity checks remain present. |
| + |
| +Anchor initialization, successor-root selection, overlap planning and newest-L0 preservation match D at the stated abstraction level. The zero-position bootstrap is an additional mismatch. Also, C reads remote L0 position on each upload decision; the pinned replica caches that position until initialization or an error. C therefore exposes the remote-position shortcut more broadly than production. |
| + |
| +Static counting confirms **84 rules, 42 witness entries and 122 baseline/subset/full-set executions**. The harness checks every proper subset and the named first failure for the full set. |
| + |
| +The witness-only classifications for `recovery-generation` and `closed-marker` are **honest as reported coverage**. Zero detections in 100,000 sweep seeds does not establish safety or redundancy. The deterministic cases inspect restoration immediately after the harmful completion; the sweep’s later observations can miss a transiently damaged replica subsequently repaired by a snapshot. The `closed-marker` mutation also combines several checks, while its witness uses an obviously stale TXID; it does not independently establish safe consumption or replay protection. |
| + |
| +The nine combination-only classifications are supported for their selected scenarios, not globally minimal mutation sets. The two door rules are now declared subsumed separately; the contradictory table should be corrected. |
| + |
| +**Writer epochs and the three notes** |
| + |
| +Writer epochs address both R7-1 and today’s lease-failover hazard in #225: accepted writes from an old client must remain confined to a prefix the new writer never modifies. Lease ownership and process fencing remain necessary, but cannot revoke an accepted S3 request. |
| + |
| +1. **Consume the marker at open:** required, explicitly and durably, before writer activity. The proposed delete/recreate protocol also needs protection from delayed marker republication. |
| +2. **First create/adoption pays recovery:** a defensible conservative choice, now explicitly accepted by the claim owner. An empty remote listing is not proof that no first upload is outstanding. I would retain fresh epochs and define the empty bootstrap, rather than add console data-bucket authority merely to avoid this path. |
| +3. **Warm baseline:** preserve the failed active writer’s valid local database, including its WAL. `.gen` alone is insufficient; implement the owner’s provenance condition. |
| + |
| +| Artifact | Ready for Phase 1 implementation planning? | Reason | |
| +|---|---|---| |
| +| **A — claim rev 6.6** | **No, as a complete contract** | The existing claim/stamp primitive remains plan-ready, but the new writer-epoch contract needs safe certificate consumption and explicit recovery integration. | |
| +| **B — moves rev 7.8** | **No** | Epoch admission misses lifecycle serving phases; empty bootstrap and warm-baseline authority need implementable rules. | |
| +| **C — executable model** | **No, as the planning gate** | It must model safe certificate use, all writer admissions, complete close evidence and valid bootstrap states. | |
| + |
| +--- |
| + |
| +**FIRST PROMPT:** |
| +Joint independent round-8 read-only review of the claim, moves, model and library spike. |
| + |
| +**WHAT:** |
| +Assess prior fixes, library grounding, writer epochs and Phase 1 readiness. |
| + |
| +**STATUS:** |
| +Complete: two P1, three P2 and one P3 findings. Go execution was sandbox-blocked. |
| + |
| +**NEEDED:** |
| +Nothing for this review. |
| + |
| +**RECOMMENDED:** |
| +Fix certificate consumption and lifecycle-wide epoch admission first; then align bootstrap, warm provenance and model evidence. |
| + |
| +**SESSION:** |
| +Safe to close. No files changed; nothing remains running. |
| \ No newline at end of file |