amadan
spec: host lifecycle claim rev 6.10, joint round 10
Admit before the app starts (session = agent replicator; retry policy for failed starts); protect unfinished-admission baselines until generation.json names the successor; refused kinds include creating; warm input empty; empty generation only for an unfinished latest admission; serving chores use session:<n>; @root names an adopted host's root generation. Joint R10 copied.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2 files changed,
+286
−13
docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md+63 −13docs/superpowers/specs/CODEX-FINDINGS-JOINT-R10.md+223 −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 783918693..2bda2e6de 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,10 @@ |
| # The host lifecycle claim |
| -Design, 2026-10-05, **rev 6.9.1** (rev 6.9 plus answers to the moves session's rev 7.10 readings). Joint rounds 6 and 7 judged the claim ready for primitive planning. Rev |
| +Design, 2026-10-05, **rev 6.10**. 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 rewrote §6.4a |
| -around writer sessions, for joint round 8. Rev 6.9 answers joint round 9 |
| +around writer sessions, for joint round 8. Rev 6.10 answers joint round 10 |
| +(R10-1, R10-2, R10-4, R10-5). Rev 6.9 answered 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: |
| @@ -674,6 +675,23 @@ new obligation the sweeping box owns. |
| A freed host's location never keeps late residue for good. |
| +**Baselines an unfinished admission needs are protected (R10-2).** A |
| +cold admission's new generation is **unfinished** until its first durable |
| +root is published, meaning `generation.json` names it. Until then: |
| +- its baseline generation, the journalled predecessor, is part of the |
| + live set; |
| +- no `park-generation` chore for the baseline may be queued, and the |
| + sweep never parks it. |
| + |
| +A chore retiring a superseded generation is queued only after |
| +`generation.json` names `holder.generation`. |
| + |
| +**Marker and claim disagreements.** If `holder.generation` is ahead of |
| +`generation.json` and the marker names the journalled predecessor of the |
| +latest admission, that is the normal unfinished state. Protect both |
| +generations, and raise no alert. Any other disagreement means touch |
| +nothing in that location, and alert. |
| + |
| **What a sweep never touches (Q3, R4-3).** This spec owns the sweep, so |
| it owns this rule. The **live set** is the triple |
| `{authoritative region, holder.location, holder.generation}`, together |
| @@ -873,8 +891,10 @@ issues any upload**. It requires: |
| 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`**; |
| +- an op kind that permits writing: **never `creating`, `deleting`, |
| + `parking`, `purging` or `placing`** (R10-4). A first writer comes after |
| + `CompleteCreate`, under `serving`, and nothing writes while a placement |
| + runs; |
| - `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 |
| @@ -897,8 +917,18 @@ 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. |
| +**Chores raised while serving, and the root generation (R10-5).** A chore |
| +queued while the claim is `serving` has `op = "session:<holder.session>"`, |
| +and is owned as usual. An example is retiring a superseded generation |
| +once its successor's root is published. An adopted legacy host's |
| +generation is the location root itself (level directories directly |
| +under `instances/<host>/`). Its name is the sentinel **`@root`**, so a |
| +`park-generation` chore can name it. `holder.generation` is `""` for such |
| +a host until its first cold admission. |
| + |
| **The admission API is exactly two modes (R9-3).** |
| -- **warm**: same generation, only with a certificate. |
| +- **warm**: same generation, only with a certificate. The new-generation |
| + input is **empty** for warm (R10-4). |
| - **cold**: a new generation. |
| A first install, after a create or an adoption, is a **cold** admission |
| @@ -961,11 +991,25 @@ 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. |
| -**When admission happens.** A box may start the app and pass its |
| -readiness checks before admission, but **no upload of any kind** may be |
| -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. |
| +**When admission happens (R10-1; this reverses rev 6.8.2).** Admission |
| +comes **before the app process starts**, so before the app can commit or |
| +acknowledge anything. The order is: |
| +1. the `AdmitWriter` CAS; |
| +2. purge local and restore the baseline; |
| +3. start the app; |
| +4. readiness; |
| +5. uploads. |
| + |
| +A writer session belongs to the agent's replicator, not to the app |
| +process. If the app crashes or restarts while the same agent process |
| +keeps replicating, it stays within the admitted session and is not |
| +re-admitted. A new agent process is always a new session. |
| + |
| +**Failed-start churn is controlled by retry policy.** Start attempts |
| +within a session back off. After the moves spec's limit, the box marks |
| +the host failed and stops creating sessions for it, until an operator or |
| +a successful health signal clears it. An app's writes are never left in |
| +an interval without an admitted session. |
| #### The baseline is always the certified remote (R6, R9-1) |
| @@ -1001,8 +1045,11 @@ These are the rulings on the moves spec's rev 7.10 readings: |
| 1. **The predecessor to restore from** is the observed `holder.generation`. |
| The exception: when a complete, paginated listing shows that |
| - generation holds no file at all, because a writer died between its CAS |
| - and its first upload. The baseline is then the nearest ancestor that |
| + generation holds no file at all, **and** it is the generation of the |
| + latest journalled admission, still unfinished (R10-2), because a |
| + writer died between its CAS and its first upload. An empty generation |
| + for any other reason is unexplained missing data: refuse, and |
| + alert. The baseline is then the nearest ancestor that |
| holds a file, the one `generation.json` names. A listing error means |
| refuse, never "empty". |
| 2. **A prepared generation**, built by a landing, a push or a dirty |
| @@ -1022,7 +1069,9 @@ These are the rulings on the moves spec's rev 7.10 readings: |
| source's writer is then admitted like any other, cold unless the |
| generation is certified. |
| 5. **`writes_lost`** is recorded only when the new writer's baseline does |
| - not cover the predecessor's last acknowledged position. A cold |
| + not cover the predecessor's last acknowledged position. With a seal, |
| + that comparison is against the **seal's** position, not a TXID from |
| + the target region. A cold |
| admission whose baseline is a seal of the stopped predecessor, as at a |
| move's landing, records **no** `writes_lost` and raises no alert. Its |
| journal entry says `baseline: sealed`. |
| @@ -1308,6 +1357,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 | |
| +| J10-R10-1, R10-2, R10-4, R10-5 | §6.4a: admit before app start; protect unfinished-admission baselines; refused kinds include creating; warm input empty; serving chores `session:<n>`; `@root` | |
| | 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 | |
diff --git a/docs/superpowers/specs/CODEX-FINDINGS-JOINT-R10.md b/docs/superpowers/specs/CODEX-FINDINGS-JOINT-R10.md| new file mode 100644 |
| index 000000000..88db1c428 |
| --- /dev/null |
| +++ b/docs/superpowers/specs/CODEX-FINDINGS-JOINT-R10.md |
| @@ -0,0 +1,223 @@ |
| +**A/B/C are not yet a consistent Phase 1 planning baseline. I would also hold E’s merge until the admission contract and cleanup-obligation representation are reconciled.** The simplification removes the stale-local-copy hazard, but introduces gaps around startup, unfinished admissions, and recovery cleanup. |
| + |
| +I reviewed the requested pins: A `f6180ae4`, B/C/D `33ce0a9c` (model `572066ec`), and E `fdff530f`. Later text appeared in the claim worktree; it is not included in these verdicts. No files were changed. |
| + |
| +Both requested Go test commands failed before compilation: |
| + |
| +```text |
| +go: creating work dir: mkdir /home/paulca/.cache/tmp/go-build…: read-only file system |
| +``` |
| + |
| +E was already checked out in its separate worktree. `bash -n internal/sim/hostlife/mutate.sh` passed. I inspected the retained results and checked their counts, but did not reproduce the sweeps. The failure traces below are static findings. |
| + |
| +**Round-9 dispositions** |
| + |
| +“Caller” means E implements the claim mutation, while the filesystem or replication work belongs to its caller. |
| + |
| +| Finding | A | B | C | E | Why | |
| +|---|---|---|---|---|---| |
| +| R9-1: certified session admits stale local DB | Resolved | Resolved | Resolved for completed starts | Resolved at caller boundary | Every new admission requires remote restoration; the clean-close/stale-copy witness now exists. C’s unfinished-start crash path remains defective, below. | |
| +| R9-2: writer identity disappears with operation | Resolved | Resolved | Resolved | Resolved | `holder.writer_box` survives operation replacement; predecessor identity no longer comes from the operation journal or executor. | |
| +| R9-3: incompatible admission transitions | Partly | Partly | Partly | Partly | Two modes and one authoritative holder generation are established, but stamps, refusal kinds, cleanup shapes and older transition tables still disagree. | |
| +| R9-4: admission not operation-bound | Resolved | Partly | Partly | Resolved against A | Literal operation/phase comparison is implemented, including serving’s empty ID. B/C’s refusal set differs from A/E. | |
| +| R9-5: incomplete close outcomes | Resolved contract | Resolved contract | Partly | Caller responsibility | Maintenance timeout witnesses were added, but startup uploads bypass the request ledger and client response delivery is still approximated. | |
| +| R9-6: inaccurate evidence tables | — | Partly | Partly | — | Live mutation counts were updated. The counter generator misparses colon-bearing names and publishes false zeros. | |
| + |
| +**New findings, ranked** |
| + |
| +**R10-1 — P1: an app can acknowledge writes before it has a writer session.** |
| + |
| +Locations: A `f6180ae4`, §6.4a, lines 964–968; B [§7.14 startup sequence](/home/paulca/amadan.net/carlos/platform-moves-design/docs/superpowers/specs/2026-10-02-move-any-app-design.md:2187); C [startup/admission ordering](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/protocol_test.go:570). |
| + |
| +Concrete failure: |
| + |
| +1. Session S closes cleanly. |
| +2. Its successor restores S’s remote database and starts the app before `AdmitWriter`. |
| +3. A background worker commits a database update and acknowledges its work to an external queue. |
| +4. The app crashes before readiness/admission. |
| +5. The claim still names S, whose certificate remains valid. The next attempt chooses warm, purges the database, and records no `writes_lost`. |
| + |
| +This violates the explicit loss-declaration requirement. Holding public HTTP traffic does not stop background work; C itself treats acknowledgements to the outside world as writes requiring preservation. |
| + |
| +**Fix:** admit before the application can acknowledge work, or enforce a real barrier preventing all such work until admission. Failed-start admission churn needs retry control, not an unjournalled writer interval. |
| + |
| +This revisits the deferred spawn/readiness granularity specifically because it hides a P1, as permitted by your instruction. |
| + |
| +**R10-2 — P1: cleanup can retire the only remote recovery baseline before the successor has one. C also preserves unfinished-start memory across crashes.** |
| + |
| +Locations: B [§7.14 admission and first upload](/home/paulca/amadan.net/carlos/platform-moves-design/docs/superpowers/specs/2026-10-02-move-any-app-design.md:2188); C [queued predecessor cleanup](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/protocol_test.go:1042), [cleanup execution](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/protocol_test.go:1288), [crash reset](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/world_test.go:510). |
| + |
| +A cold CAS names empty generation G1 and immediately queues G0 for parking. The writer dies before G1’s first upload becomes durable. Recovery explicitly needs G0, but its chore can archive and delete G0 without requiring a complete replacement baseline. |
| + |
| +For origin G0, the subsequent empty remote can be interpreted as an empty bootstrap. For a pinned nonempty generation, recovery can instead fail indefinitely. Neither outcome meets the recovery contract. |
| + |
| +The model’s `forget()` never clears `b.open`, including its database pointer and outstanding-request state. A reboot can therefore resume the old admitted session from memory that should be gone. This masks the required abandoned-generation recovery path. |
| + |
| +The ordinary sweep has a related mismatch: `deadGeneration` treats a disagreeing marker as residue, although B §6.4 requires leaving that location untouched and alerting. |
| + |
| +**Fix:** protect every baseline needed by an unfinished admission until a durable successor root is established. Apply that protection to explicit chores and sweeping. Clear volatile open state on process death and add a witness with crash, predecessor cleanup, then recovery. |
| + |
| +**R10-3 — P1: B’s commit instructions can put an obsolete generation back into authority.** |
| + |
| +Locations: B [§7.5 transition table](/home/paulca/amadan.net/carlos/platform-moves-design/docs/superpowers/specs/2026-10-02-move-any-app-design.md:1817), [§7.9 commit](/home/paulca/amadan.net/carlos/platform-moves-design/docs/superpowers/specs/2026-10-02-move-any-app-design.md:1982), versus §7.14. |
| + |
| +Both older sections still instruct commit to write `holder.generation = move id`. |
| + |
| +After a landing probe crashes, its replacement correctly admits into recovery generation R and may durably acknowledge new writes there. Following §7.9 then switches authority back to the original prepared generation M. A subsequent restore misses R’s writes. |
| + |
| +C correctly avoids this commit-time assignment. B also retains obsolete publication/probed-generation instructions in §7.6 and §7.8. |
| + |
| +**Fix:** rewrite the earlier transition tables around §7.14’s final protocol. Commit and later `probed` transitions must preserve the generation selected by the latest admission. |
| + |
| +**R10-4 — P2: the shared admission contract still differs materially.** |
| + |
| +Locations: A §6.4a; B §§5.1, 7.14, 19.4; C [cold admission](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/protocol_test.go:1023); E [AdmitWriter](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/hostclaim/internal/hostclaim/generation.go:56). |
| + |
| +- **Stamp:** A/E issue a new stamp on every cold admission. B’s seventh-round readings and C retain the landing flip’s stamp. C explicitly says issuing another stamp caused its probe to refuse itself. |
| +- **Kinds:** A/E refuse `deleting`, `parking`, `purging`, `placing`. B/C substitute `creating` for `placing`. E’s tests deliberately permit `creating`. |
| +- **Baseline:** pinned A says cold restores the predecessor remote. Prepared-generation restoration and empty-generation ancestry are substantive extensions in B/C. |
| +- **Warm input:** C supplies the current generation in `NewGeneration`; E requires that field to be empty for warm admission. It is not an exact API-shaped model. |
| + |
| +**Fix:** agree one contract and exercise the same admission vectors against C and E, including landing, restarted probes, creation, placement and clean return. |
| + |
| +**R10-5 — P2: E cannot represent cleanup chores produced by an ordinary origin-generation admission.** |
| + |
| +Locations: B §5.1 defines origin as `""`; C [chore creation](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/protocol_test.go:1049), [operation assignment](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/protocol_test.go:1329); E [obligation validation](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/hostclaim/internal/hostclaim/claim.go:210). |
| + |
| +E requires both `Obligation.Op != ""` and `park-generation.Generation != ""`. C’s ordinary serving admission supplies an empty operation ID; retiring an adopted origin replica also supplies an empty generation. |
| + |
| +Composing B’s required admission and chore into E’s `Update` therefore fails validation. Omitting the chore changes the specified transition. |
| + |
| +**Fix:** define an explicit origin-generation representation and the identity owning serving-time admission chores. Test the complete admission-plus-cleanup transaction, including adoption. |
| + |
| +**R10-6 — P2: C’s disk-loss faults exempt writes without a `writes_lost` declaration.** |
| + |
| +Locations: [crash-with-disk fault](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/background_test.go:356), idle disk-loss path in the same file, and `loseDisk` in `witness_test.go`. |
| + |
| +The fault injector directly sets `ack.Exempt = true`. It does not require a matching admission journal entry or alert. These branches also lack the `Kind == "write"` restriction used by the admission’s exemption logic. |
| + |
| +Consequently, disk-loss schedules can pass the oracle even when loss reporting is missing. The new `wSilentLoss` witness checks an ordinary crash, not this bypass. |
| + |
| +**Fix:** make the fault remove physical state only. Authorize write exemptions through a matching durable loss declaration; verify alert delivery separately. Never exempt timer acknowledgements through the database-loss rule. |
| + |
| +**R10-7 — P2: startup PUT retries bypass the complete-close evidence rule.** |
| + |
| +Locations: C [resumeOpen](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/protocol_test.go:895), [settled](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/ltx_test.go:331). |
| + |
| +First-upload and anchor requests issued by `resumeOpen` never enter `db.Issued` or set sticky uncertainty when retried. Object visibility also advances startup without establishing client-observed acknowledgement. |
| + |
| +Hold the first upload beyond timeout, let its retry land, then cleanly stop the writer. C can certify despite the unresolved original. That contradicts A/B’s lifetime-evidence rule, even if these particular repeated bytes are identical. |
| + |
| +**Fix:** include startup data requests in the session ledger and distinguish server completion from client response delivery. Extend the maintenance witnesses to first-upload and anchor retries. |
| + |
| +**R10-8 — P2: the new restore cost is absent from the readiness budget; the stated loss bound is too strong.** |
| + |
| +Locations: B §§7.3 T11, [7.14 costs](/home/paulca/amadan.net/carlos/platform-moves-design/docs/superpowers/specs/2026-10-02-move-any-app-design.md:2205); C [budget arithmetic](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/budget_test.go:63). |
| + |
| +The budget still prices the previous protocol: build three passes, verify the built database, then probe. The new protocol purges that database and restores again before each probe attempt. |
| + |
| +At the documented rates, **2.5 GiB costs 113.8 seconds under the current estimate, versus 129.16 seconds including one additional restore**. It is admitted against a 120-second window. |
| + |
| +“Bounded by the replication interval” is also not a hard guarantee during failed or stalled uploads. Loss extends back to the last successful durable replication. |
| + |
| +**Fix:** price restore per attempt, any fresh-generation upload on retries, and admission/publication overhead. Describe the replication interval as the normal operating window, with failures extending it. |
| + |
| +**R10-9 — P3: the generated baseline counters are wrong.** |
| + |
| +Locations: B [§14.2.3](/home/paulca/amadan.net/carlos/platform-moves-design/docs/superpowers/specs/2026-10-02-move-any-app-design.md:3377); [table generator](/home/paulca/.cache/nearest-region/rev710-sweeps/tables.py:108); [retained baseline](/home/paulca/.cache/nearest-region/rev710-sweeps/base100k.out). |
| + |
| +The regex parses `admissions: cold:57938` as key `cold`. Lookup of `admissions: cold` then silently defaults to zero. |
| + |
| +| Counter | Published | Retained result | |
| +|---|---:|---:| |
| +| Cold admissions | 0 | 57,938 | |
| +| Warm admissions | 0 | 17,025 | |
| +| Closes refused as uncertain | 0 | 1,283 | |
| +| Starts refused by failed purge | 0 | 6,761 | |
| +| Waits for generation marker | 0 | 56,380 | |
| + |
| +The change note repeats affected zeros. Historical door rows also retain a “this round” partner count of 336 where the current result is 357. |
| + |
| +**Fix:** emit structured counters, fail on missing required fields, and regenerate both summaries. The retained zero-violation verdict itself is not contradicted by this parser defect. |
| + |
| +**Simplification and production behavior** |
| + |
| +The central rule is sound: **generation reuse requires a one-use certificate; local database reuse is unnecessary.** Purging removes the provenance ambiguity behind R9-1. Advancing the claim session prevents an old certificate from authorizing another writer. |
| + |
| +It is not yet complete because startup writes and unfinished-admission baselines lack the protections above. “Every loss is declared and alerted” is therefore not established. |
| + |
| +B accurately describes today’s **exec-backed** activator. [ExecBackend.Restore](/home/paulca/amadan.net/carlos/platform-moves-design/internal/activator/backend_exec.go:264) returns immediately when the database exists; [doWake](/home/paulca/amadan.net/carlos/platform-moves-design/internal/activator/activator.go:1127) relies on that cache, then seeds if fresh, starts the app and opens replication. `internal/lease.Restore` performs the remote restore when called. Unit-backed routes have a different, no-op restore implementation. |
| + |
| +The stated extra restore and loss of unuploaded same-box state are real. The budget and failure-time loss bound need R10-8’s correction. `Replicator.Close` still discards its initial `SyncAndWait` error, so its return value remains insufficient certificate evidence. |
| + |
| +**E’s implementation and tests** |
| + |
| +Against pinned A’s *claim-mutation contract*, `AdmitWriter` is substantially correct: |
| + |
| +- Literal operation/phase equality includes serving’s empty values. |
| +- Session, generation and nonempty executor are checked. |
| +- A’s four forbidden kinds are refused. |
| +- Warm preserves generation/stamp; cold advances them. |
| +- Writer identity and uncertified-predecessor `writes_lost` are written atomically. |
| +- Other operation fields are preserved. |
| +- `Update` deep-copies, increments revision and conditionally writes storage. |
| +- Storage conflicts become `ErrConflict`; stale evidence after rereading becomes `ErrWrongState`. There is no automatic retry. |
| + |
| +Certificate validation, fresh-generation uniqueness, filesystem cleanup, phase-specific evidence and alerts remain caller responsibilities. E does not prove those merely by accepting `PredecessorCertified`. |
| + |
| +The new tests are meaningful. Competing admissions test stale-observation CAS failure and stale-evidence rejection after reread. Operation/phase/delete tests exercise binding directly. Operation replacement tests verify persistent writer identity and its use in the next loss record. |
| + |
| +The lost-response test models “the write succeeded but its result was discarded” by retrying the old observation. It does **not** inject an ambiguous storage error or test recovery through startup, publication and alerting. These are useful primitive tests, not end-to-end admission tests. |
| + |
| +**The seven moves-side readings** |
| + |
| +| Reading | Judgment | |
| +|---|---| |
| +| 1. Restore an ancestor when an admitted generation is empty | Necessary recovery extension, but absent from pinned A and unsafe unless cleanup preserves that ancestor. Empty must mean an unfinished admission, not unexplained missing data. | |
| +| 2. Open a prepared generation from its own pinned snapshot | Correct for landing and dirty return; substantive clarification needed in A. Never reopening an already-used prepared generation is essential. | |
| +| 3. Retain the landing flip’s stamp | Plausible installation semantics, but directly contradicts pinned A/E. Requires an agreed rule and integration test. | |
| +| 4. Clean return restores source generation authority | Reasonable with verified clean release and retained source replica. Keep the session monotonic and document the resulting predecessor/loss semantics. | |
| +| 5. Landing records loss despite a complete seal | Conservative under current E, but a complete seal is evidence of preserved data. A target-region predecessor TXID is not necessarily the restored seal’s position. Distinguish uncertainty from demonstrated baseline coverage. | |
| +| 6. Startup retries are local bookkeeping | Correct only for the surviving admitted writer. Process death must discard that state and trigger fresh admission; C currently violates this. Requests still belong in lifetime close evidence. | |
| +| 7. C2 makes the delete witness require two mutations | Correct for that witness. It does not make phase binding redundant. E’s direct delete tests are appropriate. | |
| + |
| +**Model fidelity and evidence** |
| + |
| +Static counting confirms **92 rules, 52 witnesses and 176 baseline/subset/full-set executions**. The witness harness requires every proper subset to hold and the complete mutation set to produce the named first failure. That establishes necessity within those schedules, not general completeness. |
| + |
| +The retained classifications are supported: 77 caught-alone rules, nine combination-only, three subsumed, two liveness-only and one unreachable. Seven individual rules remain witness-only across the supplied runs: |
| + |
| +`restore-gap-closed`, `closed-marker`, `close-waits`, `newest-l0`, `remote-baseline`, `close-evidence`, `live-set-region`. |
| + |
| +The `admit-bind-op,claim-cas-opid` pair is also witness-only. `strict-spawn` is now caught alone. |
| + |
| +The reported self-found repairs are visible in the code: ancestor fallback, one-use prepared generations, resumed startup, stamp handling, no-database target return, descendant-aware closing, moving-session certificates, transient purge failures, full-input compaction and refreshed probe stamps. They are useful evidence. They do not establish the unfinished-start crash claim while `b.open` survives `forget()`, or complete loss reporting while disk faults directly exempt acknowledgements. |
| + |
| +D remains useful, narrower evidence: the ten real-library tests cover anchors, position initialization, retention/root advancement, checksums, replay bytes, unconditional writes and empty bootstrap. I found no new D defect. They do not test the new claim/startup/cleanup integration. |
| + |
| +| Artifact | Verdict | |
| +|---|---| |
| +| **A** | **Not ready as the complete moves contract:** close the pre-admission loss gap and settle recovery-baseline/stamp extensions. | |
| +| **B** | **Not ready for Phase 1 planning:** resolve the P1 paths, remove obsolete generation transitions, and reprice probes. | |
| +| **C** | **Not ready as the joint gate:** correct crash-state survival, cleanup protection and loss/evidence oracles, then rerun. | |
| +| **E** | **Hold merge:** agree the shared admission contract and make origin/serving cleanup representable. No callers limits immediate exposure but does not resolve the contract. | |
| + |
| +--- |
| + |
| +**FIRST PROMPT:** |
| +Joint independent round-10 read-only review of the CARLOS specs, model, facts spike and claim library. |
| + |
| +**WHAT:** |
| +Assess round-9 fixes, simplification safety and planning/merge readiness. |
| + |
| +**STATUS:** |
| +Review complete: three P1, five P2 and one P3 findings. Go tests were sandbox-blocked. |
| + |
| +**NEEDED:** |
| +Nothing for this review. |
| + |
| +**RECOMMENDED:** |
| +Fix startup admission and baseline-retirement ordering first; align A/B/C/E, then rerun the corrected model and library tests. |
| + |
| +**SESSION:** |
| +Safe to close. No files changed; no processes remain running. |
| \ No newline at end of file |