amadan
spec: host lifecycle claim rev 6.12, joint round 11
PublishGeneration bound to op and phase, legal wherever a writer runs, the only way to retire (origin "" == @root); the predecessor is the last recorded writer, independent of the restore generation; admission coverage "" | sealed | clean-return. Joint R11 copied unedited.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2 files changed,
+222
−5
docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md+26 −5docs/superpowers/specs/CODEX-FINDINGS-JOINT-R11.md+196 −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 148f7adf3..efd0f48fe 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,11 +1,12 @@ |
| # The host lifecycle claim |
| -Design, 2026-10-05, **rev 6.11**. Joint rounds 6 and 7 judged the claim ready for primitive planning. Rev |
| +Design, 2026-10-05, **rev 6.12**. 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.10 answers joint round 10 |
| (R10-1, R10-2, R10-4, R10-5). Rev 6.11 answers the moves spec's rev 7.11 |
| -notes. Rev 6.9 answered joint round 9 |
| +notes. Rev 6.12 answers joint round 11 (R11-2 to R11-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: |
| @@ -1066,11 +1067,31 @@ that admitted the crashed writer has since been replaced (R9-2). |
| chain is known. |
| 3. **The admissions record survives release** and the next operation, |
| because it lives in `holder.admissions`, not in an operation's |
| - journal. Writes-lost declarations are kept there too. `op.journal` |
| + journal. **An admission's predecessor is always the last writer |
| + recorded there,** with its own session, box and generation. It never |
| + comes from whatever `holder.generation` an operation chose for a |
| + restore (R11-4). A clean return resets `holder.generation` to the |
| + source's generation for the restore, but the predecessor is still the |
| + target's writer. The admission's **coverage** says how the |
| + predecessor's writes are accounted for: `""` (uncovered, so |
| + `writes_lost` is recorded unless certified), `sealed` (a `from_db` |
| + seal) or `clean-return` (a clean rollback with `src_covered`). Only |
| + `""` with no certificate records `writes_lost`. The journal entry |
| + always names its coverage, including when the admission is also |
| + certified. Writes-lost declarations are kept there too. `op.journal` |
| keeps no separate writers record. |
| 4. **Uncovered predecessors.** Publishing a generation's marker is |
| - followed by one `PublishGeneration` CAS, `(observedSession, |
| - publishedGeneration, region)`. It marks every admission entry up to |
| + followed by one `PublishGeneration` CAS, `(observedOpID, observedPhase, |
| + observedSession, publishedGeneration, region)`. It is bound to the |
| + observed operation and phase, like admission (R11-5). It is legal in |
| + `serving` and in any operation kind where a writer may run, for example |
| + a restarted landing probe, restoring or reverting. The chores it queues |
| + carry `op = op.id` inside an operation, and `op = "session:<n>"` while |
| + serving. **Retirement only happens through it,** and only of |
| + predecessors recorded in `holder.admissions` (R11-2). The origin `""` |
| + and `@root` are the same generation, so nothing can retire the active |
| + legacy replica of an adopted host before a cold admission has created |
| + a successor and published it. It marks every admission entry up to |
| and including `publishedGeneration` as covered, and queues a |
| `park-generation` chore (op `session:<n>`) for every predecessor |
| generation in that chain other than `publishedGeneration`, without |
diff --git a/docs/superpowers/specs/CODEX-FINDINGS-JOINT-R11.md b/docs/superpowers/specs/CODEX-FINDINGS-JOINT-R11.md| new file mode 100644 |
| index 000000000..b17153022 |
| --- /dev/null |
| +++ b/docs/superpowers/specs/CODEX-FINDINGS-JOINT-R11.md |
| @@ -0,0 +1,196 @@ |
| +**Hold A/B/C as the joint Phase 1 planning baseline, and hold E’s merge.** Admission-before-start is fixed, but an origin-baseline sweep path remains unsafe, B retains contradictory generation instructions, and E has two concrete guard/attribution defects. |
| + |
| +Reviewed pins: A `3f916b05`; B/C/D `ec982436` with model `bd1587a1`; E `090fb7a2`. Later claim-owner answers are not credited to these pins. No files changed. Independent passes used GPT-6 Astra because the required Opus reviewer was unavailable. |
| + |
| +Both requested 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 separately. `bash -n internal/sim/hostlife/mutate.sh` passed. I inspected the retained sweep results; I did not rerun the sweeps or witnesses. |
| + |
| +**Round-10 dispositions** |
| + |
| +“Contract” means the requirement is stated; “caller” means E does not implement that filesystem, replication, or alerting action. “—” means outside that artifact’s scope. |
| + |
| +| Finding | A | B | C | E | Why | |
| +|---|---|---|---|---|---| |
| +| R10-1: acknowledgement before admission | Resolved | Resolved | Resolved | Caller | CAS now precedes purge, restore and app start. C witnesses an acknowledgement followed by a startup crash. | |
| +| R10-2: unfinished baseline retirement/crash state | Partly | Resolved contract | **Partly** | Partly | C clears volatile startup state and delays chores, but its sweep misses an absent origin marker. A lacks the complete chain/journal-survival contract. | |
| +| R10-3: obsolete generation restored to authority | — | **Partly** | Resolved | Caller | B’s corrected commit/probed rows coexist with older contradictory instructions. | |
| +| R10-4: differing admission contracts | Partly | Partly | Resolved admission shape | Partly | Modes, five refused kinds, warm input and KeepStamp agree. Recovery-history and retirement-helper scope still differ. | |
| +| R10-5: serving/origin chores unrepresentable | Resolved | Resolved | Resolved | Resolved representation | `session:<n>` and `@root` exist. E’s new alias-guard defect is separate, below. | |
| +| R10-6: undeclared disk-loss exemptions | Contract | Contract | **Partly** | Records; alerts caller-owned | Physical faults no longer exempt writes, but C’s final oracle still exempts through a hypothetical future declaration. | |
| +| R10-7: startup PUTs bypass close evidence | Contract | Resolved | Resolved | Caller | First-upload and anchor attempts enter the ledger; retries retain bytes and make uncertainty sticky. | |
| +| R10-8: understated restore cost/loss window | — | Resolved arithmetic | Resolved arithmetic | — | Restore/admission costs and later-attempt uploads are included; failed uploads extend the loss window. Retry timing needs clarification below. | |
| +| R10-9: incorrect generated counters | — | Resolved | Resolved | — | Structured counters and required-field checks replace the broken parser; current published counts match retained results. | |
| + |
| +R10-3 still matters. B [§5.1](/home/paulca/amadan.net/carlos/platform-moves-design/docs/superpowers/specs/2026-10-02-move-any-app-design.md:793) says commit writes `holder.generation`; the dirty-return [installation row](/home/paulca/amadan.net/carlos/platform-moves-design/docs/superpowers/specs/2026-10-02-move-any-app-design.md:2125) says `probed` writes generation/stamp, immediately before the corrected row says it writes neither. Implementing those older instructions can select the original prepared generation after a restarted probe has written into its successor. |
| + |
| +The [authoritative-region table and start check](/home/paulca/amadan.net/carlos/platform-moves-design/docs/superpowers/specs/2026-10-02-move-any-app-design.md:1329) also remain outdated: precommit landing is not always source-authoritative after target admission, and a restarted probe must use its admitted generation rather than the operation’s original prepared generation. These need one consistent rewrite. |
| + |
| +**New findings** |
| + |
| +**R11-1 — P1: C’s ordinary sweep can retire an unfinished admission’s origin baseline.** |
| + |
| +Locations: [deadGeneration](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/moves_test.go:1756), [absent-marker interpretation](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/protocol_test.go:342), [baseline witness](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/witness_test.go:2128). |
| + |
| +Concrete schedule: |
| + |
| +1. An adopted origin replica contains durable acknowledged writes and has no `generation.json`. |
| +2. Cold admission names G1, then crashes before G1’s first upload/marker. |
| +3. The ordinary serving-time sweep runs before recovery. |
| +4. `deadGeneration` skips unfinished-chain protection because the marker object is absent. It classifies origin data as dead and parks it. |
| +5. Recovery traces G1 back to origin, but its live restore baseline is gone. |
| + |
| +The residue oracle correctly treats an absent marker as origin; the sweep does not. The existing witness exercises the prematurely queued retirement chore. With the rules enabled, its “chores settled” condition is immediately true, so it does not force this ordinary-sweep schedule. |
| + |
| +**Fix:** use the same absent-is-origin interpretation in sweep selection and the oracle. Add an explicit origin → unfinished admission → ordinary sweep → recovery witness. This is a static counterexample, not a reproduced test failure. |
| + |
| +**R11-2 — P2: E’s `@root` alias bypasses its current-generation retirement guard.** |
| + |
| +Location: [generation.go:130](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/hostclaim/internal/hostclaim/generation.go:130). |
| + |
| +Immediately after adoption, the serving claim has `Session == 0` and `Generation == ""`. This mutation passes: |
| + |
| +```go |
| +QueueGenerationRetire(0, "", "ie", RootGeneration, newID) |
| +``` |
| + |
| +The current-generation comparison sees `"@root" != ""`, although both identify the active legacy replica. Validation accepts the resulting `park-generation` obligation. |
| + |
| +**Fix:** normalize origin before comparing retirement targets and refuse retirement without an admitted successor. Test refusal immediately after adoption, alongside the existing successful retirement after cold admission. |
| + |
| +**R11-3 — P2: E’s adoption loses the known legacy writer identity.** |
| + |
| +Locations: [adopt.go:19](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/hostclaim/internal/hostclaim/adopt.go:19), [loss-record construction](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/hostclaim/internal/hostclaim/generation.go:108). |
| + |
| +`Adopt` receives `servingBox` but leaves `Holder.WriterBox` empty. The first uncertified cold admission therefore records `writes_lost.box == ""` for the legacy process’s unuploaded acknowledgements. |
| + |
| +B explicitly requires adoption to record that writer. C’s twentieth self-found repair implements it; E does not. E’s adoption test supplies `PredecessorCertified: true` and expects an empty predecessor box, so it misses the loss case. |
| + |
| +**Fix:** initialize `WriterBox: servingBox`. Test uncertified admission after adoption, including an intervening operation replacement. |
| + |
| +**R11-4 — P2: clean return creates a predecessor identity that never existed.** |
| + |
| +Locations: A §6.4a, reading 4; B [§7.14](/home/paulca/amadan.net/carlos/platform-moves-design/docs/superpowers/specs/2026-10-02-move-any-app-design.md:2371); C [return CAS](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/moves_test.go:1383), [admission journal](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/protocol_test.go:1359). |
| + |
| +After a target probe, clean return resets `holder.generation` to the source generation while retaining the target’s session and writer box. The next source admission consequently journals: |
| + |
| +```text |
| +target box + target session + source generation |
| +``` |
| + |
| +That tuple never represented an admitted writer. C also takes its ordinary cold branch without carrying clean-return coverage evidence, producing a misleading loss declaration even when the unchanged target and complete source replica establish preservation. |
| + |
| +**Fix:** preserve the predecessor writer’s complete identity independently of the generation selected for restoration. Carry explicit clean-return coverage evidence into admission; test both the identity tuple and absence of a false loss declaration. |
| + |
| +**R11-5 — P2: B’s publication-time retirement procedure cannot use E’s helper during an operation.** |
| + |
| +Locations: B [§5.1](/home/paulca/amadan.net/carlos/platform-moves-design/docs/superpowers/specs/2026-10-02-move-any-app-design.md:1140); E [generation.go:132](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/hostclaim/internal/hostclaim/generation.go:132). |
| + |
| +B queues retirement when a successor marker publishes, including recovery admissions during active operations. E’s `QueueGenerationRetire` accepts only `serving`; its tests deliberately refuse landing, restoring, reverting and pushing. |
| + |
| +A restarted landing probe can therefore publish its fresh generation and then fail B’s prescribed helper call. |
| + |
| +**Fix:** either extend the helper with operation/phase binding and operation-owned chores, or specify and test a separate caller-composed transition. The current shared procedure is incomplete. |
| + |
| +**Ordering, baselines and loss declarations** |
| + |
| +The corrected order is sound: **CAS → purge → restore → app start → readiness → uploads**. A failed start remains inside an admitted session. B also explicitly stops an app surviving its agent before admitting the replacement; C clears `open` and checks agent epochs. This closes R10-1’s unjournalled-start interval within the model’s stated granularity. |
| + |
| +Baseline protection is not yet complete across the artifacts. B correctly protects the whole unfinished chain until publication. Pinned A recognizes only the latest immediate predecessor and does not require admission history to survive operation replacement. Two failed admissions can leave marker G0, holder G2 and immediate predecessor G1—a valid recovery chain that literal A does not explain. R11-1 adds a separate missing protection in C. |
| + |
| +Loss reporting is substantially stronger, but not proved on every path: |
| + |
| +- Seals built from the stopped database correctly suppress loss declarations. |
| +- Seals built from a short remote correctly do not establish predecessor coverage. |
| +- Adoption attribution and clean-return identity remain defective. |
| +- C’s [final oracle](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/sim_test.go:553) directly exempts writes because a future admission *would* declare them. It records no declaration or alert and does this even with `writes-lost` disabled. INV-14 cannot detect that omission because neither counter increases. |
| + |
| +That last exception is disclosed in B, but it leaves R10-6 partial. Execute the recovery admission before judging loss reporting, or report those terminal cases separately as unverified prospective declarations. |
| + |
| +B’s activator behavior-change statement is accurate for the exec-backed path: every admission restores, local-only unuploaded state can be lost, and agent replacement now stops/re-admits the app. The revised budget correctly gives approximately **117.9 seconds for 2 GiB** and rejects **2.5 GiB at 131.2 seconds** under the stated rates. |
| + |
| +**E’s admission implementation and tests** |
| + |
| +The core mutation substantially matches A6.10: |
| + |
| +| Requirement | Assessment | |
| +|---|---| |
| +| Literal observed op/phase comparison, including serving’s `""` | Correct | |
| +| Refuse creating/deleting/parking/purging/placing | Correct | |
| +| Executor, observed session and generation checks | Correct | |
| +| Warm certificate assertion; empty warm `NewGeneration` | Correct | |
| +| Cold generation change | Correct structurally; identifier freshness remains caller-owned | |
| +| `KeepStamp` requires cold and `stamp > session` | Correct | |
| +| Atomic session, generation, stamp, writer and journal update | Correct | |
| +| Sealed coverage suppresses uncertified-predecessor loss | Correct | |
| +| Preserve the current operation | Correct | |
| +| Conditional update and conflict behavior | Correct; no automatic evidence retry | |
| +| Origin/serving obligation representation | Present, with R11-2’s guard defect | |
| + |
| +Certificate verification, seal coverage, publication, purge/start ordering and alert delivery remain caller responsibilities. Accepting evidence booleans does not verify those actions. |
| + |
| +One minor metadata discrepancy remains: when both certification and sealed coverage are true, E omits `baseline: sealed`. This does not cause a loss declaration, but differs from A’s literal wording. |
| + |
| +The competing-admission, stale-operation/phase, KeepStamp and writer-identity tests are meaningful. The lost-response test discards a successful result and retries the old observation; it checks duplicate rejection, not ambiguous storage-error recovery. The operation-replacement test proves `writer_box` survives, but deliberately discards the journal, so it does not establish unfinished-chain recovery. |
| + |
| +**The eight moves-side notes** |
| + |
| +| Note | Judgment | |
| +|---|---| |
| +| 1. Five failed-start attempts | Reasonable bounded policy. Define how these attempts share the probe’s 30-second deadline. Actual retry waits before attempt five total 15 seconds; readiness time is additional. “Within half a minute” is not a general startup bound. | |
| +| 2. Unfinished admission chains | Necessary. A must explicitly protect and restore through the complete chain. | |
| +| 3. Journal survives release and replacement | Necessary recovery evidence. Carry it through every operation replacement, or store it outside the replaceable operation journal. | |
| +| 4. Publication succeeds before chore CAS | Necessary. Persist which predecessors remain uncovered and replay queuing idempotently. | |
| +| 5. `seal-return` / `src_covered` | Correct and necessary. An unchanged target does not prove the source replica covers the stop. Returning the staged seal when no target DB exists is the right path. | |
| +| 6. `from_db` seal provenance | Correct. A remote-derived seal cannot certify writes beyond that remote position. | |
| +| 7. New agent stops inherited app | Correct. Reattaching must not resume the dead agent’s replication session. | |
| +| 8. Lost timers, source cut session, adoption identity | Necessary. Separate loss records are appropriate; E still misses adoption identity. Clean-return predecessor identity also needs R11-4’s correction. | |
| + |
| +The five-attempt policy should be retained as a product choice, with an explicit aggregate deadline for move probes. It is distinct from the maximum three budgeted probe attempts. The absolute cut deadline still prevents a late commit. |
| + |
| +**Model and evidence assessment** |
| + |
| +The retained evidence supports the reported counts: |
| + |
| +- **95 rules; 57 witnesses; 186 baseline/subset/full-set executions.** |
| +- **82 rules caught alone:** 65 at 3,000 seeds, eight additional at 30,000, three at 100,000, six witness-only. |
| +- Eight combination-only, two subsumed, two liveness-only, one unreachable. |
| + |
| +The six witness-only rules are `admit-before-start`, `close-evidence`, `close-waits`, `closed-marker`, `remote-baseline`, and `restore-gap-closed`. The last has retained sweeps through 30,000; the other five through 100,000. The `admit-bind-op,claim-cas-opid` combination also remains witness-only. |
| + |
| +The harness correctly requires every proper subset to hold and the full mutation set to produce the named first failure. This establishes the witness’s discrimination, not completeness of scheduling. |
| + |
| +The twenty self-found faults are substantive, and their repairs are visible: startup retries and immutable bytes, agent epochs, unfinished chains, uncovered predecessors, dead probes, seal coverage/return, lost timers and adopted writer identity. They demonstrate useful model feedback. R11-1 shows why they do not establish closure. |
| + |
| +D’s ten real-library tests remain useful grounding for anchors, position initialization, retention, root advancement, checksums, replay bytes, unconditional writes and empty bootstrap. **No new D defect found.** They do not verify the new claim/startup/cleanup integration. I have not re-raised B §14.2.6’s accepted limitations. |
| + |
| +| Artifact | Verdict | |
| +|---|---| |
| +| **A** | Hold the joint planning baseline: incorporate chain protection, durable admission history and the agreed return/coverage rules. | |
| +| **B** | Hold: remove contradictory normative generation instructions and resolve predecessor identity/retirement integration. | |
| +| **C** | Hold as the implementation gate: fix absent-origin sweep protection and tighten loss-reporting evidence, then rerun. | |
| +| **E** | Hold merge, despite having no callers: fix root-retirement protection and adoption attribution; settle helper scope before calling it aligned with B. | |
| + |
| +--- |
| + |
| +**FIRST PROMPT:** |
| +Joint independent round-11 read-only review of CARLOS specs, model, facts spike and claim library. |
| + |
| +**WHAT:** |
| +Assess round-10 fixes, new defects and planning/merge readiness. |
| + |
| +**STATUS:** |
| +Review complete. Five new findings; R10-2, R10-3 and R10-6 remain partly unresolved. Go execution was sandbox-blocked. |
| + |
| +**NEEDED:** |
| +Nothing for this review. |
| + |
| +**RECOMMENDED:** |
| +Fix origin-baseline retirement first, reconcile the shared contract, then rerun witnesses, sweeps and library tests. |
| + |
| +**SESSION:** |
| +Safe to close. No files changed; no review processes remain running. |
| \ No newline at end of file |