amadan
spec: host lifecycle claim rev 6.9, no local DB reuse (Paul R6), joint round 9
Every writer restores from the certified remote; lost writes declared via writes_lost with holder.writer_box; admission is warm or cold only, bound to op id, phase and kind (never in deleting/parking/purging/placing); holder.generation is the only authoritative generation; park-generation chore. Joint R9 copied unedited.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2 files changed,
+269
−31
docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md+71 −31docs/superpowers/specs/CODEX-FINDINGS-JOINT-R9.md+198 −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 0017d21b1..88ba25161 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,12 @@ |
| # The host lifecycle claim |
| -Design, 2026-10-04, **rev 6.8.2**. Joint rounds 6 and 7 judged the claim ready for primitive planning. Rev |
| +Design, 2026-10-04, **rev 6.9**. 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 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: |
| +Rev 6.7 answered the moves session's notes on §6.4a. Rev 6.8 rewrote §6.4a |
| +around writer sessions, for joint round 8. Rev 6.9 answers joint round 9 |
| +(R9-1 to R9-4) and takes **Paul's ruling R6 (2026-10-04): a box never |
| +reuses its local database. Every writer start restores from the |
| +certified remote.** A small primitive cited by: |
| - **#199**, deleting an instance and parking its data: |
| `2026-10-02-replica-ownership-design.md`, which this spec supersedes |
| @@ -94,7 +97,8 @@ replaced whole with conditional writes (`If-Match` on the ETag read). |
| "location": "instances/shop.bab.oncarlos.com/<incarnation>", |
| "generation": "<op id of the installed generation, or \"\">", |
| "stamp": 41, |
| - "session": 57 |
| + "session": 57, |
| + "writer_box": "adi-knitting" |
| }, |
| "op": { |
| "kind": "serving", |
| @@ -168,6 +172,9 @@ Field rules: |
| are retired there. |
| - **`holder.session`** is the current writer session's admission `gen` |
| (§6.4a). Every `AdmitWriter` CAS moves it forward. |
| +- **`holder.writer_box`** is the box admitted as that session's writer |
| + (§6.4a). It lives in the holder, not only in an operation's journal, so |
| + it survives an operation being replaced (R9-2). |
| - **`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 |
| @@ -186,7 +193,10 @@ Field rules: |
| - **`inventory`** maps each box to its local paths for the host, for both |
| layouts (§6.3). It is persisted here, independently of any operation's |
| journal (J-I-7). |
| -- **`obligations`** are durable chores. Each names its operation, its |
| +- **`obligations`** are durable chores. Kinds: `park-replica` (a region's |
| + whole location), `park-local` (a box's local state) and `park-generation` |
| + (one dead generation `{region, generation}` within a live location, |
| + R9-3). Each names its operation, its |
| retirement event (§6.2) and the actor that must do it. All of them |
| block `free`. Each operation also defines which of them block its own |
| release to `serving`. A release keeps any obligation owned by other |
| @@ -851,7 +861,7 @@ writer admission. That includes: |
| - an opened rollback recovery; |
| - a push's writer. |
| -#### Writer sessions in the claim (R8-1) |
| +#### Writer sessions in the claim (R8-1, R9-3, R9-4) |
| `holder.session` is the claim `gen` of the CAS that admitted the |
| current writer session. |
| @@ -859,6 +869,12 @@ 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`; |
| +- **the observed `op.id` and `op.phase`.** The admission is bound to the |
| + operation and phase whose evidence justified it (R9-4). Plain serving |
| + has `op.id == ""`, which is compared for equality like any other, so a |
| + stale admission built while serving fails once any operation starts; |
| +- an op kind that permits writing: **never `deleting`, `parking`, |
| + `purging` or `placing`**; |
| - `op.exec == this box`. **Only `op.exec` may open replication, in every |
| op kind.** At most one box writes a host's replica at any time, and |
| `op.exec` names it. A landing target, a probe box or a recovering |
| @@ -877,7 +893,27 @@ It writes: |
| `holder.stamp = the resulting gen`. This is an installing CAS (§2, |
| R6-4). |
| -It never replaces the operation. Kind, id, phase, intent, participants, |
| +After a conflicting CAS, the box re-establishes its **evidence** |
| +(certificate, readiness, the `op.exec` handover) before retrying. A |
| +fresh read alone isn't enough. |
| + |
| +**The admission API is exactly two modes (R9-3).** |
| +- **warm**: same generation, only with a certificate. |
| +- **cold**: a new generation. |
| + |
| +A first install, after a create or an adoption, is a **cold** admission |
| +into an empty generation. There is no separate "fresh", "reserve", |
| +"build" or "open" step. `holder.generation` is the **only** authoritative |
| +generation in every op kind and phase. A probe or recovery that opens |
| +replication is a cold admission that moves `holder.generation`, never a |
| +generation kept in the op's journal. A cold admission whose restore or |
| +build fails before its first upload leaves an empty generation behind, |
| +which the at-rest sweep parks. The next attempt is another cold |
| +admission. Dead generations that an operation must retire explicitly use |
| +the `park-generation` chore (§2): `{region, generation}`, owned by |
| +`region:<r>`. |
| + |
| +The admission 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 |
| @@ -931,30 +967,33 @@ issued before the admitting CAS has succeeded. A start that fails its |
| checks admits nothing, and leaves `holder.session` unchanged. This keeps |
| a crash-looping app from driving a storm of cold admissions. |
| -#### 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.** |
| - If a writer's local disk was lost, for example a source during a revert |
| - or rollback, its unreplicated writes are gone. The cold admission then |
| - records `writes_lost: {box, generation, last_known_txid}` in its |
| - journal entry, and raises an alert. Lost writes are always declared, |
| - never silent. |
| - |
| -The writer then activates the new stamp locally (§6.4), and replicates |
| -**only** into `<location>/<new generation>/`. |
| +#### The baseline is always the certified remote (R6, R9-1) |
| + |
| +**A box never reuses its local database.** Every admitted writer: |
| + |
| +1. purges any local database and its companions, using the |
| + error-returning purge (§5.6). A failed purge means the writer doesn't |
| + start; |
| +2. restores from the remote: |
| + - **warm:** the same generation, up to the certificate's `max_txid`; |
| + - **cold:** the predecessor generation's remote, as far as it goes; |
| +3. replicates only into `<location>/<holder.generation>/`. |
| + |
| +That removes the lineage and provenance machinery entirely. |
| + |
| +**Lost writes are declared, never silent.** A writer that crashed with |
| +acknowledged writes not yet uploaded loses them, because its successor |
| +starts from the remote. A **cold** admission whose observed session has |
| +no certificate records, in the same CAS: |
| + |
| + writes_lost: {box: <observed holder.writer_box>, |
| + generation: <observed holder.generation>, |
| + session: <observed holder.session>, |
| + remote_max_txid: <the remote maximum it restores to>} |
| + |
| +It records this in its journal entry, and the admitting box raises an |
| +alert. `holder.writer_box` makes the box known even when the operation |
| +that admitted the crashed writer has since been replaced (R9-2). |
| #### Empty bootstrap (R8-3) |
| @@ -1224,6 +1263,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 | |
| +| J9-R9-1 to R9-4, Paul R6 | §6.4a: no local DB reuse (always the certified remote), `holder.writer_box`, `writes_lost`, two-mode admission bound to op id, phase and kind, `park-generation` | |
| | 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 | |
diff --git a/docs/superpowers/specs/CODEX-FINDINGS-JOINT-R9.md b/docs/superpowers/specs/CODEX-FINDINGS-JOINT-R9.md| new file mode 100644 |
| index 000000000..0705dec0c |
| --- /dev/null |
| +++ b/docs/superpowers/specs/CODEX-FINDINGS-JOINT-R9.md |
| @@ -0,0 +1,198 @@ |
| +**A, B and C are not yet a consistent Phase 1 planning baseline, and I would not merge E yet.** The session certificate fixes the original replay hazard. Two remaining provenance gaps can lose acknowledged data; the moves admission protocol also differs materially from the implemented primitive. |
| + |
| +I reviewed A at `a963d98d`, B/C/D at clean HEAD `831a2ea2`, and E at `a67d9f47`. AGENTS.md was read first. This was read-only. |
| + |
| +`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 |
| +``` |
| + |
| +The findings below are static traces, not newly executed counterexamples. `bash -n internal/sim/hostlife/mutate.sh` passed. I inspected the supplied sweep verdicts but did not reproduce them. |
| + |
| +The answers file acquired a **rev 6.8.2** section during review. I distinguish those later answers from pinned A, rev 6.8.1. |
| + |
| +| Round-8 finding | A | B | C | Why | |
| +|---|---|---|---|---| |
| +| **R8-1: certificate consumption/republication** | Resolved | Resolved | Resolved within represented semantics | Admission advances the claim session; old certificates cannot authorize another writer. No deletion/recreation protocol remains. | |
| +| **R8-2: admission outside `serving`** | Resolved | Partly | Partly | Executor checks cover the named paths, but probe/install admission uses extensions absent from A/E; see R9-3. | |
| +| **R8-3: invalid empty bootstrap** | Resolved | Resolved | Resolved | Empty installations write no zero-TXID LTX; D now tests the pinned library’s empty behavior. | |
| +| **R8-4: warm-baseline provenance** | Partly | Partly | Partly | Cold recovery checks provenance, but warm continuation bypasses it, and writer identity is lost across operation replacement. | |
| +| **R8-5: complete close evidence** | Resolved contract | Resolved contract | Partly | Both specs require lifetime evidence; C still treats maintenance completion more permissively. | |
| +| **R8-6: retired-door evidence table** | — | Resolved for those rows | Resolved for retired witnesses | Historical door results are distinguished correctly. Other current-result counts remain stale; see R9-6. | |
| + |
| +**R9-1 — P1: a valid close certificate admits a stale local database without checking its provenance.** |
| + |
| +Locations: A §6.4a, warm continuation versus baseline rules; B [§5.1 step 9](/home/paulca/amadan.net/carlos/platform-moves-design/docs/superpowers/specs/2026-10-02-move-any-app-design.md:939); C [warm admission](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/protocol_test.go:610), [local database retention](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/protocol_test.go:374). |
| + |
| +A concrete variant of `wWarmLineageMismatch`: |
| + |
| +1. B cleanly closes session S through N+1. Its certificate matches the remote maximum. |
| +2. Its local database is the cached copy through N, with matching generation/location but foreign lineage—the fault already represented by that witness. |
| +3. `warmCertificate` accepts S. `spawn` keeps the existing database. `warmProvenance` is called only by cold recovery. |
| +4. Admission overwrites the lineage file with the new session and starts the stale database. |
| + |
| +The application immediately lacks acknowledged state. In C, its next local N+1 upload can also be skipped because the remote already contains N+1, losing the new acknowledged write on restore. |
| + |
| +**Fix:** separate permission to reuse a replica generation from permission to retain a local database. Validate local provenance before **warm or cold** reuse; otherwise restore the certified remote baseline. Add the clean-close variant of the existing witness, checking local state and subsequent replication. |
| + |
| +This is not the deferred SQLite-integrity abstraction: a valid SQLite database can still be the wrong historical copy. |
| + |
| +**R9-2 — P1: operation replacement loses the predecessor writer’s identity.** |
| + |
| +Locations: A §6.4a, predecessor journal; E `a67d9f47:internal/hostclaim/generation.go:55–62`; C [release](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/moves_test.go:1116), [predecessor fallback](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/protocol_test.go:683). |
| + |
| +`holder.session` survives an operation transition, but the writer’s box exists only in `op.journal.writers`. C replaces the operation at move start and release, dropping that journal. E derives `predecessor.box` from the last journal entry and otherwise writes an empty string. C instead substitutes current `op.exec`. |
| + |
| +Following B/C’s release behavior with E therefore gives this failure: |
| + |
| +- A writer serves after finalization and acknowledges an unreplicated write. |
| +- It crashes, retaining its database and matching lineage. |
| +- Cold admission has no predecessor box. |
| +- B’s provenance rule rejects the intact local database and restores the older remote state. |
| + |
| +C’s fallback masks that integration failure. Current execution authority is not evidence of historical writer ownership. |
| + |
| +**Fix:** retain the current writer identity independently of operation lifetime, or explicitly preserve its matching journal entry through every transition. Validate that entry against the holder’s session and generation. Define the legacy-adoption bootstrap separately. |
| + |
| +**R9-3 — P2: B/C’s admission protocol cannot be implemented exactly through E’s A-shaped API.** |
| + |
| +Locations: B [§7.14](/home/paulca/amadan.net/carlos/platform-moves-design/docs/superpowers/specs/2026-10-02-move-any-app-design.md:2112); C [admission modes](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/protocol_test.go:577); E `generation.go:27–80`, `claim.go:214–224`. |
| + |
| +The differences are operational: |
| + |
| +- **Probe recovery:** B/C can advance an operation’s installation generation while leaving `holder.generation` unchanged. E requires the observed generation to equal `holder.generation`, and cold admission always changes that holder field. |
| +- **Opening a completed cold build:** C’s `open` marks an existing entry opened without advancing its session. E accepts only `warm` and `cold`; neither expresses that operation. |
| +- **First installation probe:** C has `fresh` admission. E has no corresponding explicit contract. |
| +- **Recovery cleanup:** B requires `park-generation`; E’s validator rejects that obligation kind. |
| +- **Ordering:** B says admission occurs after health checks and before process start. HTTP readiness requires an already-running process. Moreover, C’s initial **cold** CAS occurs before its modeled health check; only `admitCommit` occurs afterward. |
| + |
| +A restarted landing probe is the concrete integration case: passing its installation generation to E fails the observation check; passing the holder generation changes the wrong contract. |
| + |
| +**Fix:** agree on explicit reservation/build/open transitions, the authoritative generation during probing, cleanup obligations, and retry behavior. Then make A, B, C and E use those same transitions. This is distinct from the already-declared model simplification of atomic spawn/readiness. |
| + |
| +**R9-4 — P2: the admission transition is not bound to the operation whose evidence justified it.** |
| + |
| +Locations: A C2; E `generation.go:27–35`, `ops.go:14–18`, `store.go:63–116`. |
| + |
| +The initial ETag race is handled correctly. The problem is retrying against a fresh observation: a new operation can preserve session, generation and executor, so the original `AdmitWriter` closure still succeeds. For example, `BeginDelete` preserves those fields while changing the operation, allowing stale wake evidence to be reused during deletion. |
| + |
| +`RequireOp` cannot directly guard ordinary serving because it rejects an empty expected ID. |
| + |
| +**Fix:** bind admission to the expected operation and applicable phase, or provide a documented composed transition that does so. After a conflict, revalidate the evidence rather than merely rereading storage. Test operation changes and ambiguous successful writes. |
| + |
| +**R9-5 — P2: maintenance timeouts and client outcomes remain missing from close eligibility.** |
| + |
| +Locations: C [request ledger](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/ltx_test.go:309), [maintenance uploads](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/ltx_test.go:506), [request completion definition](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/world_test.go:236). |
| + |
| +Only the L0 retry loop sets permanent `Uncertain`. Compaction and snapshot attempts can be repeated without doing so. `settled()` checks server `done`, which includes refusal and does not establish client-observed success. |
| + |
| +Hold a compaction PUT beyond its timeout, let a later attempt succeed, then complete the original. C can certify that session, contrary to B’s permanent-uncertainty rule. |
| + |
| +**Fix:** represent success, timeout and ambiguous outcomes for every request class. Add maintenance-retry and lost-response witnesses. This is a fidelity defect; I have not demonstrated a new corruption schedule from it. |
| + |
| +**R9-6 — P3: the current mutation-results table still contains earlier counts.** |
| + |
| +Location: B [§14.2.5 combination table](/home/paulca/amadan.net/carlos/platform-moves-design/docs/superpowers/specs/2026-10-02-move-any-app-design.md:3622), compared with [supplied 30k verdicts](/home/paulca/.cache/nearest-region/rev79-sweeps/mutate30k.out). |
| + |
| +Examples: |
| + |
| +| Combination | B says | Supplied result | |
| +|---|---:|---:| |
| +| `strict-spawn,evidence-whole-tree` | 121 | 94 | |
| +| `claim-cas-opid,revalidate-before-effect` | 897 | 868 | |
| +| `fence-stamp,hostguard` | 4,354 | 5,652 | |
| + |
| +The summary also says **8** combination-only rules, while the later text and classification require **10**. |
| + |
| +**Fix:** regenerate the current tables from the retained verdicts. The retired-door correction itself is sound. |
| + |
| +The **one-use certificate design is sound against delayed, replayed and multipart marker completion**, subject to its evidence preconditions. Authority comes from equality with the current claim session. Once admission advances it, a late completion at `closed/old-session.json` cannot restore that authority. This does not depend on deletion semantics. |
| + |
| +For R7-1/#225, the other half remains essential: an uncertain predecessor’s data requests must stay confined to its old generation. A/B now require evidence covering L0, compaction, snapshots, retention and timed-out originals. Both explicitly identify `Replicator.Close` dropping the initial `SyncAndWait` error; production [still does so](/home/paulca/amadan.net/carlos/platform-moves-design/internal/lease/lease.go:368). Returning nil from `Close` is therefore insufficient. |
| + |
| +B’s execution handovers are present: |
| + |
| +- landing target: flip citing source stop evidence; |
| +- rollback source: return after target release, or the declared-lost fence; |
| +- reverting source: its own stop evidence before probing; |
| +- committed target and restarted probes: retained executor authority; |
| +- ordinary wake and push: existing executor authority. |
| + |
| +I found no represented path intentionally admitting a **non-executor**. E also enforces `op.exec == box` for every operation kind. Executor equality, however, does not replace phase admission or repair R9-3/R9-4. |
| + |
| +**E implements the basic warm/cold mutation correctly, but not the complete caller contract.** |
| + |
| +| Aspect | Assessment | |
| +|---|---| |
| +| Observations | Checks holder presence, observed session/generation and nonempty matching executor. | |
| +| Warm write | Advances session; preserves generation and stamp. | |
| +| Cold write | Advances session, generation and stamp atomically to the resulting claim revision. | |
| +| Preservation | Keeps operation identity, phase, participants, obligations and unrelated journal fields. | |
| +| Journal | Appends the stated entry fields, but predecessor ownership is defective as above. `writers` is a JSON-encoded array inside the string-valued journal map; document that wire representation explicitly. | |
| +| Storage CAS | `Update` deep-copies, increments revision, performs conditional storage write and maps storage conflicts to `ErrConflict`. | |
| +| Retries | No automatic retries; admission is not idempotent. Old observation conflicts; a fresh observation with old session arguments returns `ErrWrongState`. | |
| +| Caller duties | Certificate validation, genuinely fresh generation IDs, operation/phase permission, and recovery/open reconciliation remain outside the primitive. | |
| + |
| +The tests meaningfully check fields, refusal behavior, operation preservation and unchanged storage after refusal. They do not cover competing admissions, lost responses, operation-bound retries or writer history surviving operation transitions. The cross-box warm test also changes executor without modeling the required stamp handover, so it is not an end-to-end protocol test. |
| + |
| +The three moves-side readings need these judgments: |
| + |
| +1. **“Allow otherwise.”** Refusing another box’s certificate is conservative for replica-generation reuse. It is not the only sound interpretation: a complete certificate proves that the predecessor has no outstanding data requests, regardless of the successor’s box. Local database provenance is a separate decision. B’s promised remote fallback on lineage mismatch is currently missing from warm admission, R9-1. The later **6.8.2 answer explicitly chooses cross-box continuation**, contradicting B 7.9’s restriction. |
| +2. **Admission after readiness.** Sound for opening replication if no upload can occur before the successful CAS. It needs a real sequence separating cold reservation/build, application startup, readiness, and replication opening. B’s literal ordering and blanket “failed starts admit nothing” claim do not describe C’s cold path. |
| +3. **Disk-lost source skipping digest verification.** Reasonable for an absent database: restore from an identified authoritative remote baseline and report unreplicated loss. It must not waive checks on surviving files, keys or timers. The later 6.8.2 answer requires cold admission plus a durable `writes_lost` record and alert; that stronger rule is not pinned B’s “warm or cold” wording. |
| + |
| +The **empty-generation correction is grounded in D**. [TestFact_R8_3_EmptyBootstrap](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/litestreamfacts/facts_test.go:921) checks rejection of zero-TXID headers, empty-replica restore failure, no upload for an absent database, first L0 `[1,1]`, and successful subsequent restoration. |
| + |
| +Implementation must preserve the activator’s existing order: restore classification → optional first-boot seed → application start → replication. An explicitly empty generation must preserve “fresh” semantics without converting arbitrary restore errors into first boot. D tests library behavior, not that complete activator integration. |
| + |
| +For **model fidelity and evidence**, all nine reported repairs are visible: |
| + |
| +| Reported fault | Static disposition | |
| +|---|---| |
| +| Failing starts repeatedly admit sessions | Final admission moved after modeled health; cold reservation still occurs earlier. | |
| +| Stalled worker replays completed recovery | Step comparison now includes writer/recovery state. | |
| +| Carried files retain retired stamp | Recovery retags carried files. | |
| +| Disk-lost source sticks on digest | Missing-database path bypasses that comparison. | |
| +| Declared-lost writes return through remote | Local oracle includes returned writes carried by the database. | |
| +| Position-zero database with transactions treated as empty | Snapshot construction assigns positive position. | |
| +| Unbounded holds consume convergence window | Such holds are restricted to chaos scheduling. | |
| +| Lost target’s recovery blocks rollback | Successor executor/participant abandons and parks it. | |
| +| Lifecycle writers never certify close | Close eligibility now includes the relevant lifecycle states. | |
| + |
| +Static counting confirms **90 rules, 49 witnesses and 182 baseline/subset/full-set executions**. The harness requires every proper subset to hold and the full set to produce its named first failure. That establishes necessity within each witness schedule, not global minimality. |
| + |
| +The supplied 100k verdicts accurately report these six as witness-only: |
| + |
| +`admit-everywhere`, `warm-provenance`, `close-evidence`, `recovery-generation`, `closed-marker`, `close-waits`. |
| + |
| +`writer-session` is caught once, at seed **63342**. The four admission fences together are caught **17** times. The three box-side fences alone are correctly recorded as **EXPECTED-MISS**, zero of 30,000, witness held: `exec-writer` remains effective. |
| + |
| +Those classifications are honest. They do not establish coverage of warm stale-baseline admission or maintenance client outcomes. The current numeric tables need R9-6’s correction. |
| + |
| +| Artifact | Verdict | Reason | |
| +|---|---|---| |
| +| **A** | **Not ready as the complete moves contract** | Preserve writer identity across operations, apply provenance to warm local reuse, and reconcile admission transitions with B. | |
| +| **B** | **Not ready for Phase 1 implementation planning** | Warm-path data loss and incompatible admission/build/open rules remain. | |
| +| **C** | **Not ready as the joint planning gate** | Add the clean-close stale-baseline witness, remove inferred predecessor ownership, and model complete close outcomes. | |
| +| **E** | **Not ready to merge** | Resolve provenance persistence and operation-bound retry semantics; test the agreed moves integration contract. | |
| + |
| +--- |
| + |
| +**FIRST PROMPT:** |
| +Joint independent round-9 read-only review of the two specs, model, facts spike and claim library. |
| + |
| +**WHAT:** |
| +Assess round-8 fixes, writer-session safety and Phase 1 readiness. |
| + |
| +**STATUS:** |
| +Complete: two P1, three P2 and one P3 findings. Test execution was sandbox-blocked. |
| + |
| +**NEEDED:** |
| +Nothing for this review. |
| + |
| +**RECOMMENDED:** |
| +Fix both provenance gaps first, then align admission transitions and add the missing witnesses. |
| + |
| +**SESSION:** |
| +Safe to close. No files changed; no test or server remains running. |
| \ No newline at end of file |