carlos / platform Public

spec: host lifecycle claim rev 4, after joint round 2

Per-incarnation replica locations held in the claim (no cross-incarnation
reliance on a completion bound); app admission closed and drained by purge;
a cross-process flock guard with fresh claim reads; door reads bracketed by
two claim observations; all-version archive with separate archive and
deletion sets; cancelled creates cleaned up; adoption discovery covers
every other box. Joint R2 findings copied unedited.

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

claude 3 weeks ago a3c86fa566f0f90531fffaf656abd4a0c201322a parent bf61e6a

2 files changed, +329 −24

docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md +121 −24
docs/superpowers/specs/CODEX-FINDINGS-JOINT-R2.md +208 −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 2f79d7115..7bcf696ab 100644

--- a/docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md

+++ b/docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md

@@ -1,6 +1,6 @@

# The host lifecycle claim

-Design, 2026-10-02, **rev 3.1** (rev 3 plus CC14). A small primitive cited by:

+Design, 2026-10-03, **rev 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

@@ -17,7 +17,11 @@ I-7, adopts its replacement for D4, and answers N1, N3 to N10, N12 and the

carried-forward R3-12. The moves-only findings (N2's move side, N11, N13,

N14, N15) are the moves spec's. §12 maps every finding to its section.

-**Rev 3** folds in CC1 to CC13, the claim changes required by the joint

+**Rev 4** answers the claim-side findings of joint round 2

+(`CODEX-FINDINGS-JOINT-R2.md`, cited `J2-…`): R2-1, R2-2, R2-3, R2-4,

+R2-6, R2-7, and the legacy local-coverage gap noted under N5.

+**Rev 3** folded in CC1 to CC13, the claim changes required by the joint

executable model (`internal/sim/hostlife/` at 1486345c on

`design-moves-any-region`, moves spec §19.4). §12 maps them too.

@@ -66,7 +70,8 @@ replaced whole with conditional writes (`If-Match` on the ETag read).

"family": "instance",

"key": "apps/bab/jam/instances/shop.bab.oncarlos.com.json",

"account": "bab", "app": "jam", "name": "",

- "incarnation": "<hex>", "created_at": "<record CreatedAt>"

+ "incarnation": "<hex>", "created_at": "<record CreatedAt>",

+ "location": "instances/shop.bab.oncarlos.com/<incarnation>"

"op": {

"kind": "serving",

@@ -92,7 +97,8 @@ replaced whole with conditional writes (`If-Match` on the ETag read).

"lost": [],

"retired_incarnations": ["<hex>", "…"],

- "quiet_after": {"ie": "<RFC3339>"}

+ "quiet_after": {"ie": "<RFC3339>"},

+ "cancelled_creates": [{"key": "…", "incarnation": "…", "until": "…"}]

}

```

@@ -102,6 +108,13 @@ Field rules:

successful claim write. It is not an installed-data generation (J-D2).

- **`holder`** names the exact record, so a sidecar is never looked up as

an instance. It is absent only while the host is **free**.

+- **`holder.location`** is the replica location of this incarnation

+ (J2-R2-1, §3a). A new incarnation gets

+ `instances/<host>/<incarnation>`. An adopted legacy host gets

+ `instances/<host>`, its existing location. It is set when the holder is

+ set and never changes while that holder holds the host. Same-incarnation

+ generations within it (moves, push) are the moves spec's, scoped by

+ operation id.

- **`op.intent`** holds the operation's reconstruction inputs. It is

written in the **same CAS** that starts the operation, before any other

object is touched (J-N4).

@@ -128,6 +141,9 @@ Field rules:

- **`quiet_after`**, one entry per region, is the earliest time a new

install may write the host's namespace in that region (§6.2a, CC1).

Like `retired_incarnations`, it survives `free`.

+- **`cancelled_creates`** lists creates that recovery cancelled, with the

+ record key and incarnation to clean up if a late write lands (§5.1,

+ J2-R2-7). It survives `free`.

## 3. Invariants

@@ -203,6 +219,28 @@ The staging cleanup's horizon (§6.2a) covers that bound. The moves spec

calls this its third staging rule (rev 5 §7.3). The joint model fails 156

of 30,000 seeds without it.

+**C3a. No storage location is shared between incarnations (J2-R2-1).**

+Fencing by source version stops a late call from touching the wrong

+**source** object. It doesn't stop a late copy or PUT from creating a new

+object at a **destination**. AWS separates accepting a copy from

+completing it, and S3's 15-minute signature limit bounds acceptance, not

+how long an accepted request keeps running.

+So the claim does not rely on a completion bound for anything that

+crosses incarnations. Every incarnation writes only under its own

+`holder.location`, and a successor's location is a different prefix. A

+request from an old incarnation that completes arbitrarily late therefore

+lands in that old incarnation's location, which nothing admitted will

+ever read again. Any such straggler is found and parked by the next

+retirement listing of that location.

+Restore reads **only** `holder.location`, plus the moves spec's

+generation within it, taken from the claim in the same fresh admission

+read (C4). Within one incarnation, the moves spec owns operation-scoped

+generation identities and their restore contract. The §6.2a horizon

+stays, as defence in depth and for the legacy location, which is shared

+by construction: an adopted host's `instances/<host>`.

**C4. Fresh admission.** Admission reads the claim directly, never from a

listing snapshot. Admission checks happen at:

@@ -258,6 +296,11 @@ new operation will write (CC11). A pending chore there must finish first.

### 5.1 Create (R3-12, J-N4)

+0. **App admission (J2-R2-2).** Register the create in

+ `apps/<acct>/<app>/admission.json` with a CAS, as `{create id, host}`,

+ which succeeds only while the app's admission is `open`. The

+ registration is removed when the create reaches `serving` or is

+ cancelled.

1. The console assigns `CreatedAt` = now (UTC, nanoseconds). A caller

cannot supply it. `CreateRecord` and `CreateSidecarRecord` refuse a

zero or caller-supplied time on this path.

@@ -271,7 +314,12 @@ new operation will write (CC11). A pending chore there must finish first.

`control/hosts/` every few minutes and handles claims whose `op` is not

`serving` and older than five minutes:

- the record exists with this incarnation: do step 4;

- - it is authoritatively absent: CAS back to free;

+ - it is authoritatively absent: CAS back to free, adding the

+ incarnation to `retired_incarnations` and `{key, incarnation, until:

+ now + 1h}` to `cancelled_creates`. A late record PUT that lands

+ anyway is an **orphan**. It is never admitted (C1). The pass

+ deletes it with `DeleteIfMatch` when its incarnation matches a

+ `cancelled_creates` entry, and retries until `until` (J2-R2-7);

- anything else: wait.

### 5.2 Delete and park (#199)

@@ -316,6 +364,13 @@ site now uses:

recovery pass drives those phases in order: `reserved → adopted →

claimed → torn-down → retired → done`. Only the purge's own completion

removes it. A host claim going `free` never does.

+1b. **Close and drain admission (J2-R2-2).** CAS the app's

+ `admission.json` to `closed`, so no new create can register. The purge's

+ host set is then the app's records **plus** every host still

+ registered as an in-flight create. Purge waits for each registered

+ create to reach `serving` (then it is purged like the others) or to be

+ cancelled by recovery, before fixing its host set. This is tested with

+ at least two hosts.

1a. **Adopt first (CC6).** Run the one adoption routine (§9) for every

record of the app that has no claim, before deciding which hosts the

app holds.

@@ -383,24 +438,29 @@ A manifest belongs to exactly one retirement event and is never reused.

1. **Lease.** Take the replica lease on each location the owner can read.

2. **Snapshot.** List the location's object versions

- (`ListObjectVersions`). From that listing, take every current version

- except the live `lock.json`. A coordination lock is never data and

- never enters a manifest (J-N6).

-3. **Copy** each current version by `versionId` to its version-keyed

- destination. **Skip any destination that already exists**, so progress

+ (`ListObjectVersions`), every page, and refuse on any listing error.

+ From it, form two sets (J2-R2-6), both excluding the live `lock.json`

+ (J-N6):

+ - the **archive set**: every non-marker version, current and

+ noncurrent;

+ - the **deletion set**: every version in the snapshot, delete markers

+ included.

+3. **Copy** each archive-set version by `versionId` to its

+ version-keyed destination. **Skip any destination that already exists**, so progress

accumulates across retries (CC2).

-4. **Write the manifest only once every copy exists.** It records each

- entry's source key, source version id, size, and destination key and

- version. A manifest that already exists is never rewritten.

-5. **Delete** every version of each manifest key whose version id is in

- the snapshot, **by version id**. That includes noncurrent versions, so

- deleting the current one cannot resurrect an older one. A version that

+4. **Write the manifest only once every copy exists.** It records the

+ archive set (each source key, source version id, size, and destination

+ key and version) **and the deletion set**, delete markers included. A manifest that already exists is never rewritten.

+5. **Delete** every version in the manifest's deletion set, **by version

+ id**, markers included. A noncurrent version is never left to

+ resurface, and the head of a key is never a marker hiding data that

+ wasn't archived. A version that

is not in the snapshot is left alone, which keeps a later

incarnation's object at the same key safe even from a late delete.

6. **Release** this worker's own `lock.json` version, conditionally, after

the obligation's completion CAS.

7. **Retry:** if the manifest exists, go straight to deletes of its

- recorded versions. If it doesn't, re-list (step 2) and continue. The

+ recorded deletion set. If it doesn't, re-list (step 2) and continue. The

copies already made are kept, because their destinations are keyed by

version.

@@ -461,9 +521,20 @@ Every host-specific local write on a box goes through

- the admin token;

- the timer registry.

-The guard is a per-host in-process lock. Under it, the box re-reads the

-admission state it caches (C4) and refuses if the incarnation or the

-operation has moved on.

+The guard is an **exclusive `flock` on `/run/carlos/hostguard/<host>.lock`**,

+shared by every OS process that writes host state (J2-R2-3):

+- the agent;

+- `carlos-adopt.service`;

+- `carlos-config-sync.service`;

+- any later root command.

+Under it, the writer does a **fresh** claim read, never a cached one, in

+line with C4. It refuses if the incarnation or the operation has moved

+on, or if the config or release identity it selected is no longer the

+held one. Only then does it write. A process that validated, then paused,

+re-validates under the lock, so a pause before taking the lock is

+harmless.

Local retirement (§6.3) takes the same guard, then writes a retired

marker for the incarnation, so any later writer for that incarnation is

@@ -472,11 +543,22 @@ either finishes before retirement takes the guard, or fails at its next

write.

The guard is local because these writers are local. The claim decides

-what each writer is allowed to do.

+what each writer is allowed to do. The model must run these as

+independent processes, with pauses between validation and the write.

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

-The pull door's listing resolves each LTX coordinate to an exact object

+The pull door's listing:

+1. reads the claim (observation O1);

+2. authorizes the caller against O1's holder;

+3. selects versions **only under `O1.holder.location`**;

+4. reads the claim again (O2);

+5. refuses if O2's `gen` differs from O1's in holder or op

+ (J2-R2-4).

+Each handle it signs carries the selected version, the location and O1's

+holder incarnation. So it resolves each LTX coordinate to an exact object

version and returns an opaque, console-signed handle. A file request

names that handle, and the console opens `key?versionId=`. A handler that

stalls between authorization and open can therefore only ever read the

@@ -582,8 +664,16 @@ that needs one. That claim is written create-only, with:

- `touched.regions` set to the record's region;

- `touched.boxes` set to the box, if it has local state.

-**Discovery at adoption (CC4).** The adoption CAS also adds a

-`park-replica` obligation for every deployment region other than the

+**Discovery at adoption (CC4, J2 N5 note).** The adoption CAS also adds

+a `park-replica` obligation for every deployment region other than the

+record's, **and a `park-local` obligation for every deployment box other

+than the record region's serving box.** Local state on any other box

+cannot be the live instance's. `touched.complete` becomes true only once

+**all** of those acknowledge, regions and boxes alike. A rev 3 rule let an

+adopted host become complete while an old box still held its database,

+key or env files.

+The adoption obligations cover every deployment region other than the

record's. Data there cannot be the live lineage. Each region's owner parks

it (§6.2, §6.2a). `touched.complete` becomes true once they all

acknowledge, so an adopted host stops carrying another region's residue

@@ -669,6 +759,13 @@ the model catches it.

| CC11 | §4 |

| CC13 | §6.1 |

| CC14 | C3, the staging-work lease exception |

+| J2-R2-1 | C3a, §2 `holder.location` |

+| J2-R2-2 | §5.1 step 0, §5.3 step 1b |

+| J2-R2-3 | §6.4 |

+| J2-R2-4 | §6.5 |

+| J2-R2-6 | §6.2 |

+| J2-R2-7 | §5.1 step 5, §2 `cancelled_creates` |

+| J2 N5 note | §9 |

## 13. S3 behaviour this relies on, verified

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

new file mode 100644

index 000000000..e411ff3e7

--- /dev/null

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

@@ -0,0 +1,208 @@

+**A, B and C are not ready to support Phase 1 implementation planning.** The revisions resolve many round-1 findings, but several remaining safety and recovery gaps are hidden by stronger or more atomic behavior in the model.

+I read AGENTS.md first and reviewed the requested revisions with three independent GPT-6 reviewers; Opus was unavailable. The worktree matches B at `4ec3282b` and C at `7a3e94e7`. Nothing was changed.

+Both requested test commands failed before compilation:

+```text

+go test ./internal/sim/hostlife/ -count=1

+HOSTLIFE_SEEDS=30000 go test ./internal/sim/hostlife/ -run TestHostLifecycle -count=1

+go: creating work dir: mkdir /home/paulca/.cache/tmp/go-build…: read-only file system

+```

+The conclusions below are therefore **static-review findings**, not reproduced failing seeds. I inspected `mutate.sh` but could not independently confirm its published counts.

+**1. Round-1 dispositions**

+“Resolved” means the specific contract or modeled behavior is addressed—not that implementation correctness is established. Model dispositions include fidelity to the specified behavior.

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

+| D4: staging permissions/exclusion | Partly | Partly | Shared lease and version seal address the original race; timing proof remains incomplete, and model lease acquisition does not exclude workers of the same operation. |

+| D7: transitions and recovery writer | Partly | Partly | B §7.5 lets the source complete target handoff; K4 still reserves that transition to the receiving participant. Model also uses a different claim/record ordering. |

+For N5 specifically, A §9’s new completion rule defeats its own fallback: once foreign **bucket** obligations finish, §5.2 no longer requires every box to acknowledge. An old box’s database, key or sibling env files can remain unretired when the host becomes free.

+**2. Model fidelity**

+| Abstraction | Fault it can hide | Concrete model change |

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

+| Permissions checked on modeled mutations; reads/listings access maps directly | A worker depends on a read or listing its credentials cannot perform | Route Get, Head, ListVersions, control-bucket access and copy-source reads through principal-aware APIs. |

+| Exact base-version pointer plus historical LTX selection | Actual prefix restore selects a stale current object after a late destination write | Represent real replica keys, regional generation markers and the actual restore-selection algorithm. |

+| Every request completes by `issue + H` | An accepted request completes after retirement has acknowledged | Separate signing, server acceptance, timeout and completion; allow completion beyond `H` unless an enforced bound exists. |

+| Check/sign and check/local-write are atomic | A process pauses after authorization or lease validation, then acts after revocation | Split these into independently scheduled events, including independent root processes. |

+| Replica “lease acquisition” is unconditional PUT; staging lease accepts the same op | Two same-operation workers execute conflicting work simultaneously | Give each worker a lease identity and model conditional acquire, renewal, expiry and release. |

+| Claim transitions followed immediately by `fixRecord` | Crashes between B’s record-first transition and claim update are missed | Model both objects, conditional writes, ambiguous responses and recovery in B’s specified order. |

+| Atomic `localPark` | Crash between rename, journal, directory fsync and acknowledgement loses replay information | Represent individual artifacts and durability barriers; inject crashes between them. |

+| Complete map listings | A failed/truncated/paginated inventory is treated as complete | Model pages, continuation tokens, failures after successful pages, and mutations between pages. |

+| Fixed clock skew; one global time | Clock steps or pause margins invalidate signing horizons and cross-box deadlines | Separate service time, wall time and monotonic time; exercise clock adjustment and post-check pauses. |

+| Old executable is a Boolean fault | Old console, stale enrollment report or pre-floor updater bypasses the floor | Model enrollment and distinct console, agent and boot-updater versions and activation decisions. |

+| Config is an incarnation integer; first failed probe never creates a process | Same-incarnation config changes and writes before first readiness failure disappear | Track bundle/release/environment versions; separate spawn from readiness success/failure. |

+Two additional scope gaps matter:

+- **One host** prevents testing purge’s multi-host enumeration and admission protocol.

+- **Return staging** bypasses the forward path’s lease and stalled-signer machinery at [moves_test.go:808](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/moves_test.go:808), and uses `now + H` rather than the forward staging horizon.

+The time scaling also reverses an important relationship: model `H=60` is shorter than `cutBudget=320`; production `H` exceeds fifteen minutes while the default cut budget is 120 seconds. Successful schedules in one configuration cannot establish the other’s timing behavior.

+**Mutation results: useful, but not trustworthy as protocol-wide proof.**

+- **37 caught alone:** plausible evidence that these switches affect this model. The counts are unverified here, and some detections are non-convergence rather than the claimed safety failure.

+- **9 with partners:** useful interaction evidence, but additional failing seeds do not by themselves establish which guard prevented which fault. Preserve and compare minimized traces.

+- **2 liveness-only:** supported only within the represented state space. In particular, configuration is too coarse to establish a general claim about real config failures.

+- **The admission/hold/start-check triple:** materially misleading. Its third fence is stronger than B specifies; finding R2-8 below explains why.

+- **`restore-lineage-filter`:** correctly described as adding no detection beyond its partner. That is unproven protection, not proof of redundancy.

+- **`readiness-quiet`:** its unreachability is credible under the encoded ordering: acknowledgements already wait for the horizon and conflicting obligations block new operations. It does not validate the horizon itself.

+- **Harness classification:** build failures and timeouts can be counted as `CAUGHT`; finding R2-10 below prevents accepting the summary without underlying logs.

+**3. New failure traces and model defects**

+These include failures in the proposed round-1 remedies. They do not reopen M1–M18.

+**R2-1 — P1: storage fencing remains incomplete at the destination and completion boundary.**

+**A C3/§6.2a; B §§6.4, 7.6, 15.**

+A copy naming an exact **source** version still creates a new destination version. Consider an accepted install-copy request whose client times out: a retry succeeds, the operation advances, and the earlier request completes after retirement or namespace reuse. The source-version condition does not protect the destination.

+The proposed horizon does not yet exclude that schedule. The 14/16-minute experiment tests whether S3 accepts an old signature, not how long an already accepted operation may continue. AWS also distinguishes copy acceptance from completion and provides separate destination conditions. [AWS CopyObject documentation](https://docs.aws.amazon.com/AmazonS3/latest/API/API_CopyObject.html).

+The model assumes completion within `H`, then further protects restore with exact `BaseVer` and historical lineage selection at [protocol_test.go:178](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/protocol_test.go:178). B specifies neither that persistent restore pointer nor that selection algorithm.

+**Fix:** define destination-side fencing or immutable generation identities and the corresponding restore contract. If correctness still depends on `H`, establish an enforceable server-completion bound covering every request type; client timeout is insufficient. Model destination writes after publication and retirement.

+**R2-2 — P1: purge can miss a creator already past its reservation check.**

+**A §§5.1–5.3; [console_test.go:76](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/console_test.go:76).**

+A creator reads “no purge reservation” and pauses. Purge reserves the app, enumerates its hosts and claims them. The creator then claims a previously unused hostname and publishes its record while purge tears down stores or deletes the app prefix.

+The reservation check and host CAS concern different objects. The model performs both atomically inside `userCreate`.

+**Fix:** register in-flight creators through an app-level admission protocol. Purge must close admission and drain or reconcile those creators before fixing its host set and beginning teardown. Test at least two hosts.

+**R2-3 — P1: the local host guard excludes only threads in one process.**

+**A §6.4; [background_test.go:222](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/background_test.go:222).**

+Release adoption and config work also run through separate root commands: [carlos-adopt.service:17](/home/paulca/amadan.net/carlos/platform-moves-design/internal/host/units/carlos-adopt.service:17) and [carlos-config-sync.service:25](/home/paulca/amadan.net/carlos/platform-moves-design/internal/host/units/carlos-config-sync.service:25).

+One process can validate, pause, then write an old env file or release pointer after another process retires or holds the host. An in-process mutex cannot serialize them. A’s cached-admission wording further conflicts with C4.

+**Fix:** use a guard shared by all relevant OS processes, with fresh durable incarnation/operation checks under it. Include the selected config/release identity. Model independent processes and pauses between validation and the filesystem mutation.

+**R2-4 — P1: pinning the door’s read leaves authorization-to-version-selection exposed.**

+**A §6.5; [console_test.go:436](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/console_test.go:436).**

+The console authorizes a listing for incarnation A, then pauses before resolving object versions. The host is deleted and recreated for B. The listing resumes and signs a handle for B’s current version. Opening that exact version preserves the wrong authorization decision.

+The model selects versions atomically with authorization and filters on an incarnation tag that ordinary legacy LTX objects need not have.

+**Fix:** bind authorization and version selection to the same holder/operation observation—for example, validate the claim around selection and reject if it changed. Sign the selected identity and authorization scope. Inject the pause **before version selection**, not only before object open.

+**R2-5 — P1: a config update can make automatic rollback permanently fail.**

+**B §§7.6–7.8, 9.1.**

+Admission pins bundle V1. A normal config/secrets update publishes V2 after the cut. Target `configured` rejects the changed ETag and starts rollback. Source recovery also renders current configuration, but every recovery probe must satisfy the pinned V1 inputs. Each retry encounters the same mismatch.

+No specified mechanism preserves/render-selects V1, serializes its publication, or authorizes a recovery-specific replacement. Model assignments such as [moves_test.go:892](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/moves_test.go:892) cannot represent V1 versus V2.

+**Fix:** choose one complete policy for updates during a move and for recovery: durable pinned inputs, serialized publication, or explicitly validated recovery inputs. Test a change after admission and after a writable probe.

+**R2-6 — P2: A’s park manifest cannot replay its stated deletion set.**

+**A §6.2 steps 2–7; [protocol_test.go:379](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/protocol_test.go:379).**

+A selects/copies current versions and records those copies, then requires deleting noncurrent snapshot versions too. After a crash, retry knows only the manifest’s recorded versions. Historical data behind a delete marker is particularly ambiguous.

+B §6.4 and the model instead snapshot every version; the model archives every non-marker version. They validate a different algorithm.

+**Fix:** persist separate archive and deletion sets, including the policy for delete markers, or explicitly adopt all-version archiving in A. Test crashes after manifest publication with several historical versions and a marker at the head.

+**R2-7 — P2: create recovery can free the claim before record publication completes.**

+**A §5.1 step 5 and §8; [console_test.go:498](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/console_test.go:498).**

+Recovery observes an absent record and frees the creating claim. An earlier submitted record PUT completes afterward. Admission refuses the orphan, but the record also blocks ordinary recreation; A supplies no explicit replay rule for removing it safely.

+The model’s record creation is synchronous, and its recovery pass contains additional orphan deletion absent from A’s operation table.

+**Fix:** specify publication/cancellation recovery, including conditional orphan cleanup or roll-forward from durable intent. Model late control-bucket writes and ambiguous responses.

+**R2-8 — P2: the advertised third admission fence does not exist in B’s start check.**

+**B §§5.1, 14.2.5; [background_test.go:77](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/background_test.go:77).**

+After target commit, before source retirement, the source’s old DB marker, files marker and **source-region** bucket marker still agree. That satisfies B’s specified start check.

+The model instead compares the source with the globally committed **target** lineage, updated at [moves_test.go:658](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/moves_test.go:658).

+Thus, with only `exec-admission` and `hold-op-open` removed, a delayed open can make the source ready and let it wake beside the target under B’s rules. The model invents a third barrier and requires the triple mutation.

+**Fix:** model regional generation markers faithfully and run the pair against this exact schedule. Correct the redundancy claim, or explicitly add a global committed-generation check to the protocol. The unmutated admission/open protections still prevent this trace.

+**R2-9 — P2: the final cold-restore check repairs storage before checking it.**

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

+Before cold restore, the checker directly writes the complete surviving local DB into the bucket. A missing or stale replica can therefore pass because the checker just supplied the missing data.

+Moreover, write-loss checks run only for the final holder. A bad move followed by deletion/recreation can escape that final assertion.

+**Fix:** check storage at explicit promised durability boundaries without modifying it. Check each terminal operation before a later deletion can erase the evidence. Exercise cold restart with local state unavailable after a completed checkpoint.

+**R2-10 — P2: mutation infrastructure errors count as detections.**

+**[mutate.sh:40](/home/paulca/amadan.net/carlos/platform-moves-design/internal/sim/hostlife/mutate.sh:40).**

+Any nonzero Go exit becomes `CAUGHT`, including compilation failure, read-only cache failure and timeout. `MISSED` also does not make the sweep fail.

+**Fix:** count only a parsed invariant violation with a reproducible seed as detection. Classify infrastructure failures as errors, preserve logs, and fail the sweep on errors. Declare expected redundant/liveness-only outcomes separately.

+There are no additional material P3 findings.

+**4. Verdicts**

+| Artifact | Ready for Phase 1 planning? | Reason |

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

+| **A — claim rev 3.1** | **No** | Purge/create admission, cross-process local exclusion, authorization/version selection, legacy local coverage and storage-completion guarantees remain incomplete. |

+| **B — move rev 5** | **No** | Inherits A’s blockers; config-update recovery is incomplete; record/claim ordering and handoff authority remain inconsistent; the cut promise still differs from the enforced deadline. |

+| **C — model** | **No, as the planning gate** | Useful for finding faults, but stronger restore/admission behavior, atomic transaction boundaries and a repairing final oracle prevent its green results from validating the specified protocol. |

+The next round should begin with deterministic regressions for these traces, faithful record/claim and regional-marker behavior, and a corrected mutation harness. Then rerun the seed sweep. Increasing seed counts alone will not exercise states the model cannot represent.

+---

+**FIRST PROMPT:**

+Joint independent, read-only round-2 review of the two specs and executable model.

+**WHAT:**

+Assess prior fixes, model fidelity, new faults and Phase 1 readiness.

+**STATUS:**

+Review complete. All three verdicts are not ready. Go execution was sandbox-blocked.

+**NEEDED:**

+Nothing for this review.

+**RECOMMENDED:**

+Resolve the protocol gaps and model mismatches, then rerun deterministic regressions and mutations.

+**SESSION:**

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

\ No newline at end of file