carlos / platform Public

spec: move-any-app rev 7.4: joint round 3, claim rev 6 encoded (#175)

Written against claim rev 6 (3ea3f90c). The moves side of joint round
3: R3-1, the restore contract is an algorithm (the snapshot named by
version id and TXID in generation.json, continuation by contiguous TXID
over versioned listings, duplicates skipped, conflicts refused, gaps
reported), and the two changes litestream's restore needs are named;
R2-5, a recovery install's configured phase renders current inputs and
is never gated on move.inputs; R3-7, T11's permitted probe attempts
depend on the admitted budget, and budget_test.go shows rev 7.3's
formula refused every default move; R3-5, a public request reaching a
landing target before the commit is INV-5, and commit-before-open has
its own violation; R3-6, mutate.sh fails on orchestration errors and
missing witness output. Claim rev 6's installation-scoped marker,
ordered orphan cleanup and namespace sweep are taken into §6.4 and
§19.4, with three questions for platform-1e.

The model (9108f958) encodes all of it; every witness names its
failure and the gate proves it under every proper subset of its
mutation set. The harness no longer enforces a stated-set outcome on a
wider combination.

Results: 30,000 and 100,000 seeds clean. 71 rules: 57 caught alone (48
by the sweep at 3,000; 5 at 30,000 and by witness; 4 by witness only),
11 in stated combinations, 2 liveness, 1 unreachable, none unexercised.
§22.10 has every disposition.

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

claude 3 weeks ago 0e41b685f5d12dd8f382d05ad417c763ffa82a9c parent 9108f95

3 files changed, +390 −131

docs/superpowers/specs/2026-10-02-move-any-app-design.md +363 −128
internal/sim/hostlife/witness_test.go +25 −1
internal/sim/hostlife/world_test.go +2 −2

diff --git a/docs/superpowers/specs/2026-10-02-move-any-app-design.md b/docs/superpowers/specs/2026-10-02-move-any-app-design.md

index 49bf7f02e..02866d4cd 100644

--- a/docs/superpowers/specs/2026-10-02-move-any-app-design.md

+++ b/docs/superpowers/specs/2026-10-02-move-any-app-design.md

@@ -1,7 +1,35 @@

# Move any app or instance to another region: Phase 1, a safe single-instance move

**Date:** 2026-10-03

-**Revision:** 7.3.

+**Revision:** 7.4.

+- **Rev 7.4** answers the moves side of **joint round 3**

+ (`CODEX-FINDINGS-JOINT-R3.md`, cited "R3-n") and is written against

+ **claim spec rev 6** (3ea3f90c), which answers the claim side (R3-2,

+ R3-3, R3-4); §22.10 has every disposition. On the spec: **R3-1**, the

+ restore contract is an algorithm now (§5.1): `generation.json` names

+ the installed snapshot by version id and TXID, and the restore replays

+ the LTX chain that continues it, skipping what it already covers and

+ refusing a conflict, never guessing; **R2-5**, a recovery install's

+ `configured` phase renders current inputs and is never gated on

+ `move.inputs` (§7.6, §7.8); **R3-7**, T11's permitted probe attempts

+ depend on the admitted budget, and a test shows rev 7.3's formula

+ refused every default move (§7.3, `budget_test.go`); claim rev 6's

+ installation-scoped retired marker, ordered orphan cleanup and

+ namespace sweep are taken into §6.4 and §19.4. On the model (§14.2):

+ restore is a chain, not a union; the local fence is per installation

+ and a deterministic UK→US→UK round trip serves on UK again; orphan

+ cleanup is a plan with pauses; the sweep discovers locations from the

+ namespace with the 32-entry cap modelled; a public request to a landing

+ target before the commit is INV-5 (**R3-5**), which gives

+ `commit-before-open` its own violation; `mutate.sh` fails on

+ orchestration errors and missing witness output (**R3-6**); every

+ witness names its failure and the gate proves it under every proper

+ subset of its mutation set. Three new rules (`fence-by-installation`,

+ `orphan-order`, `sweep-namespace`), each with a witness. Results:

+ 30,000 and 100,000 seeds clean; 71 rules, 57 caught alone, 11 in

+ stated combinations, 2 liveness, 1 unreachable, none unexercised

+ (§14.2.5).

- **Rev 7.3** adds **deterministic witness scenarios** to the model

(§14.2.2, `witness_test.go`): one fixed, hand-scheduled scenario per

@@ -193,8 +221,8 @@ branch `design-nearest-region`.

from its §2 onward (tombstones become the claim's `deleting` and

`parking` operations).

- The claim spec, `docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md`,

- **rev 5.2 at 465fee96** on `design-replica-ownership`. Rev 7.2 is

- written against rev 5.2; rev 7.1 against rev 5.1 (64eec93b); rev 7

+ **rev 6 at 3ea3f90c** on `design-replica-ownership`. Rev 7.4 is

+ written against rev 6; rev 7.2 and 7.3 against rev 5.2 (465fee96); rev 7.1 against rev 5.1 (64eec93b); rev 7

against rev 5 (4a458a9c); rev 6 against rev 4 (a3c86fa5); rev 5 against rev 3

(8b5bccb2); rev 4 against rev 2 (cf3a7861).

@@ -296,6 +324,9 @@ Rev 4's model required CC1 to CC13 of claim rev 2, and claim rev 3

adopted them; rev 5's CC14 is in claim rev 3.1 and rev 4; rev 6's CC15 to

CC19 are in claim rev 5, rev 7's CC20 and CC21 in claim rev 5.1 (CC21

as a purge fence), and rev 7.1's CC22 in claim rev 5.2, with C5a (§19.4).

+Claim rev 6 (3ea3f90c) answers the claim side of joint round 3 (R3-2,

+R3-3, R3-4) with no request from this spec; rev 7.4 encodes it (§6.4,

+§14.2.2, §19.4).

Until platform-1e adopts them, this spec states each as the behaviour it

relies on.

@@ -460,30 +491,78 @@ by the commit's claim CAS (§7.9), by a push's probe CAS (F7), and by a

dirty rollback's source probe (§7.8). Restore reads it from the same fresh

admission read as `holder.location` (claim C3a).

-**The restore contract (J2-R2-1).** A restore reads `holder.location`,

-generation `holder.generation`, in the box's own bucket, and nothing else.

-It replays **every** replica object of that generation, current and

-noncurrent, as litestream replays every LTX file of a generation. It never

-picks "the newest object under the prefix". So:

+**The restore contract (J2-R2-1; R3-1).** A restore reads

+`holder.location`, generation `holder.generation`, in the box's own

+bucket, and nothing else. It never picks "the newest object under the

+prefix". Rev 7.3 said it "replays every replica object of that generation,

+current and noncurrent", which is not an algorithm (R3-1): a generation

+can hold the installed snapshot, later replication, a duplicate of the

+snapshot from a copy that completed late, and an LTX PUT that completed

+after a later one. **The algorithm:**

+1. **The snapshot is immutable and named.** `generation.json` records the

+ installed snapshot's `versionId` and its TXID (`snapshot_version`,

+ `snapshot_txid`), taken from the install manifest. The restore opens

+ exactly that version. A second `base` version under the generation (a

+ late copy) is never read.

+2. **Continuation is by TXID.** Every LTX object in the generation carries

+ its transaction range `[min, max]` in its key, as litestream writes

+ them. The restore takes, in TXID order, the objects whose `min` is

+ `snapshot_txid + 1` and then each next contiguous range, opening each

+ by the `versionId` the listing returned (noncurrent versions included,

+ so a key a later PUT overwrote still contributes its version).

+3. **Duplicates and older checkpoints are skipped.** A version whose

+ range the chain already covers is either a duplicate (identical

+ content, by its checksum) or an older checkpoint of the same

+ transactions; either way it adds nothing and is skipped.

+4. **A conflict refuses.** A version whose range overlaps the chain but

+ whose content differs from what the chain holds at those TXIDs is a

+ conflict: the restore stops with a member-safe reason and pages. It

+ never guesses which history is right; under this spec no such

+ version can exist within one generation, because one executor writes

+ a generation (INV-1) and every other write lands in its own generation.

+5. **A gap ends the chain.** The restore stops at the first missing TXID

+ and reports the gap. Litestream does not advance past a failed upload,

+ so a gap within a generation means a replica object was lost, which

+ this spec treats as a lost checkpoint (INV-2's RPO line, §14.2.3).

+So:

- a request that completes late can only add an object to **its own**

- generation. A late install copy repeats the sealed snapshot; a late LTX

- PUT from an old executor lands in a generation the claim no longer

- names. Neither is ever restored into the current state;

+ generation. A late install copy repeats the sealed snapshot (another

+ `base` version, never opened); a late LTX PUT from an old executor lands

+ in a generation the claim no longer names. Neither is ever restored

+ into the current state;

- the claim moves to a new generation only after that generation is fully

installed and probed, so a restore never meets a half-written one;

- what lands in a dead generation after its retirement is residue, not

data: the straggler sweep (§6.4) retires it.

-The model drops the contract (restoring the newest object under the

-location instead) and loses acknowledged writes (§14.2.5).

+**Against litestream.** `lease.Restore` (`internal/lease/lease.go:404`)

+delegates to litestream, whose S3 client opens LTX keys without a

+`VersionId` and plans a transaction range from the keys it lists. Phase 1

+needs two changes there: the snapshot opened by `versionId`, and the

+listing taken with versions so an overwritten key's older version is

+still a candidate for step 2. Both are implementation work in the restore

+plan (§15 step 8 verifies the S3 behaviour they rely on; rows 2, 3 and

+10 of claim §13). Until then a restore from a generation with a reused

+LTX key could miss the version a late PUT overwrote.

+**In the model** (§14.2.2) a history is an ordered list of transaction

+ids and every LTX object carries the whole history up to its checkpoint,

+so step 2 reads "a version continues the chain if its history extends

+it", step 3 "is a prefix of it", and step 4 "is neither". Rev 7.3's model

+took the union of every version's writes, which no restore can implement

+and which hid any conflict; the model drops the contract

+(`restore-by-generation`: the newest object under the location) and loses

+acknowledged writes (§14.2.5).

**Markers.** A generation is named in three markers. None is a record

field.

|---|---|---|---|

-| `generation.json` | `<location>generation.json`, beside `lock.json` | **last**, after the install manifest is complete and verified (§7.6); **conditionally**: If-Match the marker it supersedes, or If-None-Match when there is none (model 29) | `{"op","incarnation","host","box","installed_at","manifest_sha256"}` |

+| `generation.json` | `<location>generation.json`, beside `lock.json` | **last**, after the install manifest is complete and verified (§7.6); **conditionally**: If-Match the marker it supersedes, or If-None-Match when there is none (model 29) | `{"op","incarnation","host","box","installed_at","manifest_sha256","snapshot_version","snapshot_txid"}`: the last two name the installed snapshot's `versionId` and TXID, which the restore starts from (R3-1) |

| `<dbPath>.gen` | beside the local database | after a restore completes | `{"op","incarnation","location"}` |

| `.files-gen` | inside the files directory | **last**, after files, `<host>.env`, timers and the carried registry columns are all durable (§7.6) | `{"op","incarnation"}` |

@@ -728,7 +807,23 @@ Phase 1 uses the claim spec's park (§6.2 there) and local retirement

the same obligation, and the verification repeats.

- **Local retirement** takes the host guard and writes a retired marker

first (claim C7), so a stale background write for that incarnation is

- refused.

+ refused. **The marker is scoped to an installation** (claim rev 6 §6.4,

+ R3-3): `{incarnation, op id of the installation being retired}`. It

+ refuses a writer carrying that incarnation and an operation at or

+ before the retired one. A later **new installation** of the same

+ incarnation on this box, a move back to a region the instance left,

+ replaces the marker under the guard, in the landing's `checking` phase,

+ conditional on a fresh claim read showing the new operation current and

+ this box its target; the marker then names the new op, and the retired

+ installation's workers, carrying the old op, stay refused. Every

+ host-guard writer (config sync, release adoption) records the operation

+ it validated under when it selects a row, and the guard compares that

+ with the marker. Rev 7.3's marker fenced the whole incarnation, and the

+ model's move back never passed its probe: it timed out and rolled back,

+ which a green sweep did not distinguish from success. The model now

+ requires a successful UK→US→UK round trip as an unmutated witness

+ (§14.2.5, `fence-by-installation`). How operations are ordered in

+ production is a question for the claim spec (§19.4).

No park destination is an ancestor of a live prefix (codex 8). **A park is

its own journaled phase**, complete before any install into the vacated

@@ -741,10 +836,21 @@ can still land after it. Within one incarnation the restore contract

(§5.1) makes such a straggler harmless to data. It is still residue, and

no later retirement of that location may ever run. Claim rev 5's at-rest

sweep owns it: for a host with no operation running, each region's box

-lists the locations of the host's retired incarnations and every

-generation within `holder.location` other than `holder.generation`, and

-parks whatever it finds as a further retirement event, under a

-`park-sweep` obligation the sweeping box owns. Being an obligation, it

+lists the host's namespace and parks what is not live, as a further

+retirement event, under a `park-sweep` obligation the sweeping box owns.

+**It discovers locations from the namespace itself** (claim rev 6 §6.2a,

+R3-4), not from `retired_incarnations`, which is capped at 32 entries and

+exists only to stop an incarnation being reused: it lists

+`instances/<host>/` with delimiter `/`, every page, refusing on a listing

+error; a child prefix of 64 hex characters is an incarnation location,

+residue unless it is `holder.location`; a level directory directly under

+the host prefix is the legacy location, residue unless `holder.location`

+is the host prefix itself; and within `holder.location`, every generation

+other than `holder.generation` is residue. The version `generation.json`

+names as the snapshot (§5.1) is in the live set and is never touched. The

+model keeps the real cap and shows a replication PUT of an incarnation 33

+recreates old landing after the list forgot it (`sweep-namespace`,

+§14.2.5). Being an obligation, it

holds off any new operation over that region until it acknowledges (CC11),

and every delete names a snapshot version, so nothing written later is

touched.

@@ -922,7 +1028,7 @@ placement, the target writes `moves/<acct>/<app>/<host>/<move id>/target.json`:

| T9 claim | the claim is `moving` with this move id, its holder is the record's incarnation, and this region and box are in `touched` (added by CAS before the first staging write, claim spec §2) |

| T10 return lane | this box can put and delete `moves/_lane/<move id>` in the source's bucket (M17) |

| T12 quiet region | the claim's `quiet_after` for the target region (CC1) has passed, so the landing's park of an earlier stay never waits inside the cut window. A move back into a region the instance left within H waits at `ready`, not mid-cut. **Defence in depth (model, rev 5):** under claim rev 3 no state reaches it, because every retirement acknowledges only after its own horizon and CC11 refuses a move over a pending chore; the model drops T12 and no cut ever waits (§14.2.5). It stays, because it costs one comparison and guards any future path that acknowledges early |

-| T11 budget | the **whole** stop-to-open estimate fits the operator's cut window (default 120 s) (codex R2-10, M11), from measured rates: stop + final checkpoint + final mirror (at most the 16 MiB bar at the measured cross-region copy rate) + archive build and upload + install copy (replica size at the measured in-bucket copy rate) + restore (replica size at the measured restore rate) + render + **every permitted probe attempt, each with its own settle** (three times 30 s plus 20 s) + the open (`open_budget`, 5 s) (joint N15, J2-N15). The estimate is recorded per phase as `cut_budget_s`, and admission sets an absolute `cut_deadline` (§7.4) |

+| T11 budget | the **whole** stop-to-open estimate fits the operator's cut window (default 120 s) (codex R2-10, M11), from measured rates: stop + final checkpoint + final mirror (at most the 16 MiB bar at the measured cross-region copy rate) + archive build and upload + install copy (replica size at the measured in-bucket copy rate) + restore (replica size at the measured restore rate) + render + **the probe attempts the window permits, each with its own settle** + the open (`open_budget`, 5 s) (joint N15, J2-N15). **The permitted attempts depend on the budget (R3-7):** `attempts = min(3, floor((window − everything else) / (30 s + 20 s)))`, and the instance is eligible only if that is at least one; the probe loop (§7.7) runs at most that many. Rev 7.3 required all three attempts to fit, 150 s of probing against a 120 s default window, so no default move was ever eligible; `budget_test.go` (§14.2) states the arithmetic and shows a tiny instance admitted with two attempts, the boundary at 70 s of fixed costs, and never more than three. The estimate is recorded per phase as `cut_budget_s`, and admission sets an absolute `cut_deadline` (§7.4) |

**Source readiness.** S1: a probe request (§7.7) to the readiness path on

the instance as it runs today answers 200 to 399 from its own process

@@ -1056,7 +1162,7 @@ journaled in `<DataDir>/.moves/<host>/<move id>/` (F12).

| `copying` | per-key copy of `replica/`, by the sealed `versionId`s, into this move's own generation, `<location>g-<move id>/`, verifying each size; then write the install manifest `<location>g-<move id>/install.json` (every key and size) | the install manifest exists | replayable: staging is immutable after the flip, the generation is new, and the copy never deletes. A copy that completes late lands in this generation again (§5.1) |

| `local` | local-park any warm database (with `<dbPath>.gen`), files directory and `<host>.env` into `.parked/superseded-<move id>/`; extract the archive's files; write `<host>.env` from the archive; `ReplaceTimers` from the snapshot (§9.4); set `Replication` and `NextDue`; remove the host's restore-verification entry (§6.3); fsync all; **then** write `.files-gen` | `.files-gen` names this op and incarnation, and the journal records each sub-step | each sub-step is idempotent and journaled; `.files-gen` is written last, so its presence vouches for all of them (codex R2-6) |

-| `configured` | render through §9.1; the move-bound ack's bundle etags must equal `move.inputs` | ack matches | replayable; a mismatch is a rollback ("configuration changed during the move"), and the source's recovery then runs on the new bundle (§7.7, J2-R2-5) |

+| `configured` | render through §9.1 and materialize through §9.2; **for a forward install (this landing, a push)** the move-bound ack's bundle etags must equal `move.inputs` | ack matches | replayable; a mismatch is a rollback ("configuration changed during the move"), and the source's recovery then runs on the new bundle (§7.7, J2-R2-5). **A recovery install (§7.8) runs this phase on current inputs and records them; it is never gated on `move.inputs`** (R2-5) |

| `restored` | restore cold from `holder.location`, generation `<move id>` (the restore contract, §5.1), write `<dbPath>.gen`, `CheckDB` (`backend_exec.go:313`), record `landing.installed_db_sha256` | | replayable until `probing` |

@@ -1096,7 +1202,8 @@ only while the claim names this box as execution holder:

- the readiness path (`moves.ready_path` from the instances manifest, `/`

otherwise) answers 200 to 399 within 30 s (`backend_exec.go:36`);

- a 20 s settle, the process still running, and a second request;

-- up to three attempts.

+- up to three attempts, and never more than T11 admitted for this

+ budget (§7.3, R3-7).

The probe's activator entry is **held**: `RetireExcept`

(`internal/edge/edge.go:924`, `activator.go:2624`) keeps it, and the edge

@@ -1140,7 +1247,7 @@ because, until then, a source failure might need the target's state again.

| `claimed` | CAS the claim: `op.kind = restoring`, execution holder = this box, citing the target's evidence (§19 K4) | |

| `restoring` | row `restoring`, `hold_op = rollback id` | replayable |

| clean: `verified` | files and timers digests equal its `stopped` digests (a mismatch is `stuck`, INV-4); its warm database's `<dbPath>.gen` equals its pre-move generation | replayable |

-| dirty: `parking`, `copying`, `published`, `local`, `configured`, `restored` | exactly the target's install phases of §7.6, on the source, from `moves/<host>/<rollback id>/`, with destination `superseded/<rollback id>/<host>/` for what it supersedes | as §7.6 |

+| dirty: `parking`, `copying`, `published`, `local`, `configured`, `restored` | the target's install phases of §7.6, on the source, from `moves/<host>/<rollback id>/`, with destination `superseded/<rollback id>/<host>/` for what it supersedes, **with one difference: `configured` and the release materialization run on the inputs the source renders now, recorded as `recovery.inputs`, and are never gated on `move.inputs`** (§7.7, J2-R2-5). Rev 7.3 said "exactly" and so inherited the landing's `configured` gate: a bundle published after admission, a target that wrote, and a dirty rollback would then have failed before the recovery probe (R2-5). The model's `recovery-current-inputs` witness is that case (§14.2.5) | as §7.6 |

| `probing` | the probe | **never replays an earlier phase**: once its recovery process has started, its own new writes are authoritative (INV-2, INV-7) |

| `probed` | | |

| `recovered` | CAS `rollback.recovered_at` | |

@@ -1588,6 +1695,19 @@ A rule is caught if either catches it. A witness run that fails is an

ERROR (the witness is broken, not the rule). `HOSTLIFE_WITNESS=<rule>`

runs one rule's witnesses with their full trace.

+**Rev 7.4: the gate proves each witness's claim in full, and the harness

+cannot pass on an empty result.** Every witness names the failure its

+scenario produces (a substring of the violation). With no mutation the

+gate runs each witness in place (must hold), under **every proper subset**

+of its stated mutation set (must hold: a rule a combination names is

+shown necessary, not assumed) and under the whole set (must violate with

+its named failure, not merely some invariant); 26 witnesses, 92 runs,

+under a second. `mutate.sh` now fails on a scratch directory it cannot

+create and on an `xargs` failure, requires exactly one well-formed

+verdict per requested mutation, and reports a rule that has witnesses

+but produced no witness output as an ERROR, never as "none" (R3-6).

+`go test` also runs `TestReadinessBudget`, T11's arithmetic (§7.3).

#### 14.2.2 What it models

**Rev 6 (joint round 2): the model encodes the specs, nothing stronger.**

@@ -1711,6 +1831,48 @@ binary gave 49,743, 49,744 and 49,745 completed operations over 30,000

seeds. It drains in create-id order now, two runs agree exactly, and the

sweep counts in §14.2.5 are rerun on the deterministic model. It was the

only behaviour-affecting map iteration.

+**Rev 7.4: claim rev 6 and the moves side of joint round 3.**

+- **Restore is a chain (R3-1).** A history is an ordered list of

+ transaction ids; every replica object carries the whole history up to

+ its checkpoint. `generation.json` names the generation's snapshot by

+ version id (recorded by the install, `op.BaseVer`); the restore opens

+ that version and then takes, among every version of the generation's

+ LTX key, those whose history extends the chain (longest last), skips

+ those that are a prefix of it, and refuses on one that is neither. A

+ staging round's snapshot is the local database only if its history

+ continues the replica's. Rev 7.3 took the union of every version's

+ writes, which no restore can do. The baseline is unchanged by the

+ chain: every durable write stays reachable, which is the property the

+ protocol owes.

+- **The local fence is per installation (R3-3).** `{incarnation, op}`:

+ retirement writes the retiring operation's sequence; admission and the

+ host-guard passes compare the operation they validated under with it

+ (each pass records that sequence when it selects a row); the landing's

+ `checking` phase replaces the fence on a fresh read that shows the move

+ current and this box its target. Op ids carry the model's global

+ counter, so "at or before" is the id order.

+- **Orphan cleanup is a plan with pauses (R3-2).** The recovery pass and

+ a create that finds the record key occupied each run their own cleanup

+ plan: read the record (ETag, incarnation); on a later step read the

+ claim fresh and classify; on a later step `DeleteIfMatch`. Record ETags

+ are unique per write now (rev 7.3 reused values, which would have made

+ the conditional delete meaningless). The cleanup asserts that it never

+ deletes the record of the claim's holder or creating incarnation.

+- **The sweep discovers locations from the namespace (R3-4)** and

+ `retired_incarnations` is capped at 32, anti-reuse only. The legacy

+ location is the host prefix itself.

+- **Public delivery is modelled (R3-5).** The edge routes on the row: a

+ wake of a ready row on a landing target before the commit is INV-5,

+ checked whenever a request reaches the edge. `commit-before-open` has

+ its own violation now, alone, in the sweep and in its witness.

+- **Not taken in rev 7.4**, stated in §14.2.6: the target's cleanup is

+ still queued at release rather than after `recovered_at`; a create

+ still refuses while a record PUT is pending on the server, which a

+ real console cannot see; the release check still omits timers and

+ unreplicated local writes; same-operation workers still share a lease

+ identity; the timing scale is unchanged.

paginated listings, separate service, wall and monotonic clocks,

enrollment and console and updater versions, spawn separate from

readiness, and same-operation lease identities.

@@ -1812,8 +1974,22 @@ adds and one it makes stricter:

app is idle. Writes past the last completed checkpoint are lost by

design and declared so; every durable write must come back.

-**Rev 7.3, on the final model (rev 7.2's, with the deterministic purge

-drain): 30,000 seeds, zero violations; 100,000 seeds, zero violations**

+**Rev 7.4, on the final model (claim rev 6, the restore chain, the

+installation-scoped fence, the ordered orphan cleanup, the namespace

+sweep, public delivery): 30,000 seeds, zero violations; 100,000 seeds,

+zero violations** (42 s and 100 s). Across the 100,000 seeds: 165,084

+completed operations, among them 1,790 completed moves, 1,881 clean and

+95 dirty rollbacks, 432 pre-flip reverts, 382 declared losses, 31,588

+pushes, 94,712 delete-park-free cycles and 1,426 lost disks. 24,258

+requests completed after `H`; 30,949 staging signatures were refused as

+stale; 14,114 creates restarted on a 412; 117 targets were stopped

+mid-return. The orphan plans reshuffle the seeds against rev 7.3 (a plan

+is one more console entry to pick from), which is what the witnesses are

+for. No restore was refused for a conflicting history in any seed: with

+every rule in place no generation ever holds two histories.

+**Rev 7.3, on rev 7.2's model with the deterministic purge

+drain: 30,000 seeds, zero violations; 100,000 seeds, zero violations**

(35 s and 121 s). Across the 100,000 seeds: 165,834 completed

operations, among them 1,613 completed moves, 2,072 clean and 96 dirty

rollbacks, 443 pre-flip reverts, 388 declared losses, 31,682 pushes,

@@ -1905,145 +2081,157 @@ Each was a failing seed first, then a rule; each rule's mutation is in

#### 14.2.5 Mutation results

Every rule was dropped in turn, with the one prebuilt binary of §14.2.1,

-on the final rev 7.3 model, with the strict classification, and **in two

-ways** (rev 7.3): the **random sweep**, 3,000 seeds each, 30,000 for

-every rule not caught at 3,000, 100,000 for every rule not caught at

-30,000, 30,000 for each combination and 100,000 for the rarest; and the

-rule's **witness scenarios** (§14.2.2, `witness_test.go`) under the same

-mutation, for the 20 rules that have them. A rule is caught if either

-catches it; `mutate.sh` reports the two separately, and this section

-does too. The model has **68 rules**, as in rev 7.2. No run was an ERROR.

+on the final rev 7.4 model, with the strict classification, **in two

+ways**: the **random sweep**, 3,000 seeds each, 30,000 for every rule not

+caught at 3,000, 100,000 for every rule not caught at 30,000, 30,000 for

+each combination and 100,000 for the rarest; and the rule's **witness

+scenarios** (§14.2.2, `witness_test.go`) under the same mutation, for the

+25 rules that have them. A rule is caught if either catches it;

+`mutate.sh` reports the two separately, and this section does too. The

+model has **71 rules**: rev 7.3's 68 plus `fence-by-installation`,

+`orphan-order` and `sweep-namespace` (claim rev 6). No run was an ERROR.

Seed numbers reproduce any sweep line with `HOSTLIFE_SEED`;

-`HOSTLIFE_WITNESS=<rule>` replays a witness with its trace. Rev 7.2's

-counts are in the rev 7.2 spec (0c6058b0); the sweep counts below differ

-from them by a few seeds because the purge drain is deterministic now

-(§14.2.2), not because any seed was reshuffled.

+`HOSTLIFE_WITNESS=<rule>` replays a witness with its trace. Rev 7.3's

+counts are in the rev 7.3 spec (dc7f2a63); the orphan plans reshuffled

+the seeds (§14.2.3), so sweep counts moved by a few seeds while every

+witness verdict is unchanged.

| | rules |

|---|---|

-| caught alone by the sweep at 3,000 seeds | 46 |

-| caught alone by the sweep at 30,000, and by their witness | 5 (`lost-quarantine`, `markers-last`, `rollback-journal`, `seal-by-version`, `staging-quiet`) |

-| caught alone by their witness only; the sweep misses them at 100,000 | 2 (`generation-conditional`, `declare-lost-compute`) |

-| caught only in a stated combination: the witness holds alone and violates with the partners | 12 |

+| caught alone by the sweep at 3,000 seeds | 48 |

+| caught alone by the sweep at 30,000, and by their witness | 5 (`lost-quarantine`, `markers-last`, `rollback-journal`, `seal-by-version`, `orphan-order`) |

+| caught alone by their witness only; the sweep misses them at 30,000 or 100,000 | 4 (`generation-conditional`, `declare-lost-compute`, `fence-by-installation`, `sweep-namespace`) |

+| caught only in a stated combination: the witness holds alone and under every proper subset, and violates with the partners | 11 |

| liveness only | 2 (`readiness-key`, `config-before-probe`) |

| unreachable under claim rev 5 | 1 (`readiness-quiet`) |

-| unexercised | **0** (rev 7.2 had `generation-conditional`; rev 7.1 `lost-return-park`) |

+| unexercised | **0** |

**The witnesses.** One scenario per rule the sweep catches rarely or only

-in combination; two for `registration-check`, one per partner. "Alone"

-is the witness under the rule's own mutation; "with partners" under the

-stated combination. Where a rule holds alone, that is the redundancy the

-combination column states: the partner is what stops the scenario when

-the rule is gone, and vice versa.

+in combination, and one per rule claim rev 6 or this round added; two

+for `registration-check`, one per partner. "Alone" is the witness under

+the rule's own mutation; "with partners" under the stated combination.

+The gate also runs every proper subset of each combination and requires

+the witness to hold there, so a rule a combination names is shown

+necessary; each witness violates with the failure it names, not merely

+some invariant (R3 review).

|---|---|---|---|---|

-| `generation-conditional` (model 29) | push p1's first `generation.json` PUT is accepted and its response lost; the agent publishes again and p1 completes; push p2 completes; the stale PUT lands | **violated**: the marker names p1, the claim p2, and the serving box cannot start | | 0 / 100,000 (0 / 300,000 on rev 7.2; 2 / 100,000 on rev 7.1) |

-| `lost-return-park` (model 27) | the target writes in the settle window, the settle check fails, the target is stopped after its first return PUT and declared lost | **violated**: INV-10, the lane in the source region at the release | | 3 / 3,000, 32 / 30,000, 102 / 100,000 |

+| `generation-conditional` (model 29) | push p1's first `generation.json` PUT is accepted and its response lost; the agent publishes again and p1 completes; push p2 completes; the stale PUT lands | **violated**: the marker names p1, the claim p2, and the serving box cannot start | | 0 / 100,000 |

+| `lost-return-park` (model 27) | the target writes in the settle window, the settle check fails, the target is stopped after its first return PUT and declared lost | **violated**: INV-10, the lane in the source region at the release | | 3 / 3,000, 32 / 30,000, 112 / 100,000 |

| `declare-lost-compute` (model 5) | the target is frozen in its settle window and its execution lease expires; the VM resumes once the source has recovered | **violated**: INV-1, two boxes run the host | | 0 / 100,000 |

| `watchdog-independent` (§7.1) | as above, with the agent alone paused, so the application keeps running | held: with compute fencing the operator refuses, and the paused box is never declared lost | with `declare-lost-compute`: **violated**, INV-1; a watchdog inside the paused agent never fences | 0 / 100,000; the pair 3 / 100,000 |

| `lost-quarantine` (CC12) | the target is stopped while landing, declared lost, and started again with its old disk | **violated**: INV-10, a database and files for a host served elsewhere | | 0 / 3,000, 12 / 30,000 |

-| `rollback-journal` (R2-3) | a dirty rollback; the source's agent crashes after its probe spawned the instance, which wrote and replicated into the return generation | **violated**: INV-2 on cold restore; the restart at `claimed` parks the return generation | | 0 / 3,000, 4 / 30,000 |

-| `seal-by-version` (J-N2) | a pre-cut staging round completes after the seal; the source wrote and replicated between them | **violated**: INV-2 on cold restore; the landing installs the stale round | | 0 / 3,000, 11 / 30,000 |

-| `commit-before-open` (INV-5) | the same scenario; the mutation opens the target's row at the probe | held: an open row admits nothing while the claim is uncommitted | with `dirty-return`: violated, and the violation is `dirty-return`'s | 0; the pair 15 / 30,000 |

-| `claim-cas-opid` (C2) | a clean rollback; a second source goroutine reads the claim just before the release and stalls; the host is released, a purge claims it, the goroutine resumes | held: revalidation stops it | with `revalidate-before-effect`: **violated**, the stale release overwrites the purge and the store is torn down under a serving host | 0; the pair 1,021 / 30,000 |

-| `exec-admission`, `hold-op-open`, `start-check-claim-gen` (J2-R2-8) | an open from an earlier operation, paused on the source, lands after the commit while the source's row is still held; a request wakes the source | held, each: `hold_op` refuses the open, or the exec check refuses the wake, or the generation check refuses the start | all three: **violated**, INV-1, the source serves beside the target | 0 each; any pair 0 / 30,000; the triple 4 / 30,000, 12 / 100,000 |

-| `strict-spawn` (J-D3) | the source runs a main process and a descendant placed as its parent was; the move cuts | held: the whole-tree cleanup kills the escaped descendant | with `evidence-whole-tree`: **violated**, INV-1, the descendant writes beside the target | 0; the pair 129 / 30,000 |

-| `touched-incomplete` (J-N5) | a legacy host with a pre-release replica in another region is adopted, then deleted | held: discovery parked the other region at adoption | with `legacy-discovery`: **violated**, INV-10, the replica is residue after `free` | 0; the pair 9,092 / 30,000 |

-| `door-reread` (claim §6.5 O2) | a listing authorized before the delete selects after a recreate into the same location | held: with C3a the new incarnation's location differs, and the listing finds nothing | with `location-per-incarnation`: **violated**, a read authorized for inc 1 returns inc 2's data | 0; the pair 40 / 30,000 (10 door violations) |

-| `door-by-version` (claim §6.5) | a listing selects and signs before the delete; the file request opens after the recreate | held, as above | with `location-per-incarnation`: **violated**, the same; `door-reread` is not needed | 0; the pair 31 / 30,000 (2 door violations), with `door-reread` too 59 / 30,000 (30) |

-| `registration-check` (CC21) | the first create of a host registers and its console pauses; a purge of the app drains the expired registration, tears the store down and finishes; the creator resumes | held: the fence and the ETag condition refuse the CAS, and the 412 restarts the create on a store that exists again | with `fence-etag`: **violated**; with `purge-claim-fence`: **violated**; a host creating on a torn-down store | 0 / 30,000; the pairs 231 and 309 / 30,000 |

+| `rollback-journal` (R2-3) | a dirty rollback; the source's agent crashes after its probe spawned the instance, which wrote and replicated into the return generation | **violated**: INV-2 on cold restore; the restart at `claimed` parks the return generation | | 0 / 3,000, 3 / 30,000 |

+| `seal-by-version` (J-N2) | a pre-cut staging round completes after the seal; the source wrote and replicated between them | **violated**: INV-2 on cold restore; the landing installs the stale round | | 0 / 3,000, 15 / 30,000 |

+| `commit-before-open` (INV-5; R3-5) | a public request reaches the target's edge while its probe runs; the mutation opened the row at the probe, and the edge routes on the row | **violated**: INV-5, a public request reached the landing target before the commit | | 10 / 3,000, 115 / 30,000 (rev 7.3: never alone) |

+| `claim-cas-opid` (C2) | a clean rollback; a second source goroutine reads the claim just before the release and stalls; the host is released, a purge claims it, the goroutine resumes | held: revalidation stops it | with `revalidate-before-effect`: **violated**, the stale release overwrites the purge and the store is torn down under a serving host | 0; the pair 1,006 / 30,000 |

+| `exec-admission`, `hold-op-open`, `start-check-claim-gen` (J2-R2-8) | an open from an earlier operation, paused on the source, lands after the commit while the source's row is still held; a request wakes the source | held, each, and under every pair | all three: **violated**, INV-1, the source serves beside the target | 0 each; any pair 0 / 30,000; the triple 7 / 30,000, 19 / 100,000 |

+| `touched-incomplete` (J-N5) | a legacy host with a pre-release replica in another region is adopted, then deleted | held: discovery parked the other region at adoption | with `legacy-discovery`: **violated**, INV-10 after `free` | 0; the pair 9,092 / 30,000 |

+| `door-reread` (claim §6.5 O2) | a listing authorized before the delete selects after a recreate into the same location | held: with C3a the new incarnation's location differs | with `location-per-incarnation`: **violated**, a read authorized for inc 1 returns inc 2's data | 0; the pair 36 / 30,000 (8 door violations) |

+| `door-by-version` (claim §6.5) | a listing selects and signs before the delete; the file request opens after the recreate | held, as above | with `location-per-incarnation`: **violated**, the same; `door-reread` is not needed | 0; the pair 29 / 30,000 (2 door violations), with `door-reread` too 55 / 30,000 (27) |

+| `registration-check` (CC21) | the first create of a host registers and its console pauses; a purge of the app drains the expired registration, tears the store down and finishes; the creator resumes | held: the fence and the ETag condition refuse the CAS, and the 412 restarts the create on a store that exists again | with `fence-etag`: **violated**; with `purge-claim-fence`: **violated**; a host creating on a torn-down store | 0 / 30,000; the pairs 240 and 313 / 30,000 |

+| `fence-by-installation` (claim rev 6 §6.4, R3-3) | UK→US, then US→UK: the second landing must replace the marker UK wrote when it retired the first installation; **unmutated, the instance must serve on UK again, running** | **violated**: the move back never serves on UK (the probe is refused, the cut deadline passes, it rolls back); INV-3 at the witness's milestone | | 0 / 30,000: the sweep cannot tell a rolled-back move from a served one |

+| `orphan-order` (claim rev 6 §5.1 step 5, R3-2) | a cancelled create's record lands late; the recovery pass starts its cleanup and pauses after its first observation; a create of the next incarnation removes the orphan itself, claims and publishes; the paused cleanup resumes | **violated**: the cleanup, judging the new record by the stale claim, deletes the record of the incarnation the claim names | | 0 / 3,000, 2 / 30,000 |

+| `sweep-namespace` (claim rev 6 §6.2a, R3-4) | a replication PUT of incarnation 1 is accepted and completes after 33 delete-and-recreate cycles, by which time `retired_incarnations` no longer lists 1 | **violated**: INV-10, residue the sweep never finds | | 0 / 30,000: no seed recreates 33 times |

+| `recovery-current-inputs` (§7.7, §7.8; R2-5) | a bundle is published after admission; the target writes; the rollback is dirty; the source's recovery install must render current inputs | **violated**: `stuck`, the source could not recover | | 51 / 3,000, 506 / 30,000 |

**The purge fence, the ETag condition and C5a.** `purge-claim-fence`

-(CC21) is caught alone by the sweep: 25 / 3,000, 260 / 30,000.

-`fence-etag` (CC22): 17 / 3,000, 189 / 30,000. `claim-never-deleted`

-(C5a): 7 / 3,000, 79 / 30,000 (54 of the 79 on the main host while

-`creating`, 25 on the second host). `registration-check`, the creator's

+(CC21) is caught alone by the sweep: 26 / 3,000, 266 / 30,000.

+`fence-etag` (CC22): 18 / 3,000, 195 / 30,000. `claim-never-deleted`

+(C5a): 8 / 3,000, 77 / 30,000 (54 of the 77 on the main host while

+`creating`, 23 on the second host). `registration-check`, the creator's

re-read, is not caught alone by the sweep at 3,000 or 30,000 seeds, and

-its witness holds alone: with the fence and the ETag condition in place

-a drained registration always means a changed claim ETag, so the CAS

-fails whether or not the creator re-reads. The re-read alone, which is

-what rev 7's CC21 asked for, is shown insufficient in the combination

-table (`purge-claim-fence` + `fence-etag`, 298 / 30,000).

+its witness holds alone: with the fence and the ETag condition in place a

+drained registration always means a changed claim ETag, so the CAS fails

+whether or not the creator re-reads. The re-read alone, which is what

+rev 7's CC21 asked for, is shown insufficient in the combination table

+(`purge-claim-fence` + `fence-etag`, 307 / 30,000).

**Rev 6's unexercised three, now caught (the biased schedule, §14.2.2).**

| rule | result | what the model finds |

|---|---|---|

-| `location-per-incarnation` (claim C3a) | **caught alone**: 3 / 3,000, 31 / 30,000 | an incarnation's database holds writes of the previous incarnation: a replication PUT accepted before the delete completes after the recreate into the shared location, and the new incarnation's restore replays it; the cold-restore check at a later release and the start check both see it |

-| `door-reread` (claim §6.5 O2) | with `location-per-incarnation`: 40 / 30,000, of which 10 are door violations; witness violated | a listing authorized for the old incarnation selects, after the recreate, the new incarnation's object in the shared location, and signs it |

-| `door-by-version` (claim §6.5) | with `location-per-incarnation`: 31 / 30,000, of which 2 are door violations, and with `door-reread` as well 59 / 30,000 (30); witness violated with C3a alone | a handle signed before the delete opens the location's current object after the recreate |

+| `location-per-incarnation` (claim C3a) | **caught alone**: 3 / 3,000, 29 / 30,000 | an incarnation's database holds writes of the previous incarnation: a replication PUT accepted before the delete completes after the recreate into the shared location, and the new incarnation's restore replays it; the cold-restore check at a later release and the start check both see it. With the restore chain (R3-1) the same PUT can also make the chain refuse a conflicting history: the sweep reports it as `stuck` |

+| `door-reread` (claim §6.5 O2) | with `location-per-incarnation`: 36 / 30,000, of which 8 are door violations; witness violated | a listing authorized for the old incarnation selects, after the recreate, the new incarnation's object in the shared location, and signs it |

+| `door-by-version` (claim §6.5) | with `location-per-incarnation`: 29 / 30,000, of which 2 are door violations, and with `door-reread` as well 55 / 30,000 (27); witness violated with C3a alone | a handle signed before the delete opens the location's current object after the recreate |

Neither door rule can be violated while C3a holds, under any schedule: a

listing selects only under O1's location, and no later incarnation ever

writes there. They are defence in depth behind C3a, and each is shown

load-bearing once C3a is dropped, by its witness and by the sweep.

-**Caught alone: 53 of 68** (46 by the sweep at 3,000; 5 by the sweep at

-30,000 and by their witness, marked †; 2 by their witness alone, marked

+**Caught alone: 57 of 71** (48 by the sweep at 3,000; 5 by the sweep at

+30,000 and by their witness, marked †; 4 by their witness alone, marked

‡, with the sweep's count beside).

|---|---|---|---|---|

-| `recovery-pass` | 2,502 / 3,000 | | `fresh-incarnation` | 44 / 3,000 |

+| `recovery-pass` | 2,501 / 3,000 | | `fresh-incarnation` | 41 / 3,000 |

| `legacy-discovery` | 569 / 3,000 | | `location-per-incarnation` | 3 / 3,000 |

-| `park-by-version` | 2,066 / 3,000 | | `park-all-versions` | 681 / 3,000 |

-| `park-skip-lock` | 2,878 / 3,000 | | `retirement-ids` | 283 / 3,000 |

-| `quiet-before-ack` | 192 / 3,000 | | `straggler-sweep` | 135 / 3,000 |

-| `sweep-staging` | 43 / 3,000 | | `restore-by-generation` | 4 / 3,000 |

-| `hostguard` | 6 / 3,000 | | `purge-reserve-first` | 2,291 / 3,000 |

-| `purge-adopts` | 10 / 3,000 | | `purge-journal` | 1,976 / 3,000 |

-| `admission-registration` | 39 / 3,000 | | `registration-recovery` | 1,945 / 3,000 |

-| `purge-claim-fence` | 25 / 3,000 | | `fence-etag` | 17 / 3,000 |

-| `claim-never-deleted` | 7 / 3,000 | | `cancelled-creates` | 374 / 3,000 |

-| `orphan-no-deadline` | 29 / 3,000 | | `evidence-whole-tree` | 2 / 3,000 |

-| `evidence-from-state` | 2,793 / 3,000 | | `floor-boot-recovery` | 2,533 / 3,000 |

-| `participant-rows` | 5 / 3,000 | | `revalidate-before-effect` | 19 / 3,000 |

-| `sign-before-safeuntil` | 16 / 3,000 | | `sign-at-check` | 11 / 3,000 |

-| `sdk-no-resign` | 11 / 3,000 | | `lost-quarantine` † | 12 / 30,000 |

-| `cut-deadline` | 15 / 3,000 | | `revert-journal` | 17 / 3,000 |

-| `rollback-journal` † | 4 / 30,000 | | `dirty-return` | 2 / 3,000 |

-| `lost-return-park` | 3 / 3,000 | | `target-park` | 44 / 3,000 |

-| `abort-target-owner` | 1,066 / 3,000 | | `timer-freeze` | 7 / 3,000 |

-| `timer-canonical` | 4 / 3,000 | | `markers-last` † | 15 / 30,000 |

-| `source-readiness` | 8 / 3,000 | | `seal-by-version` † | 11 / 30,000 |

-| `staging-quiet` † | 10 / 30,000 | | `fresh-admission` | 17 / 3,000 |

-| `stale-hold-release` | 2 / 3,000 | | `obligations-block-ops` | 18 / 3,000 |

-| `claim-op-exclusive` | 85 / 3,000 | | `recovery-current-inputs` | 56 / 3,000 |

-`declare-lost-compute` was combination-only in rev 7 and rev 7.2 (0 /

-100,000 alone) and caught alone once in 100,000 in rev 7.1: a rule the

-sweep reaches by chance. Its witness freezes the target and expires its

-lease, and the mutation lets it resume beside the recovered source every

-time. `generation-conditional`'s witness holds the stale marker PUT until

-a newer marker is current, which the sweep did twice in 100,000 on rev

-7.1 and never since. Neither is in `expected-outcomes.txt` any more.

-**Caught only in a combination: 12 rules.** Each partner's own count, on

+| `park-by-version` | 2,063 / 3,000 | | `park-all-versions` | 677 / 3,000 |

+| `park-skip-lock` | 2,869 / 3,000 | | `retirement-ids` | 283 / 3,000 |

+| `quiet-before-ack` | 184 / 3,000 | | `straggler-sweep` | 133 / 3,000 |

+| `sweep-staging` | 42 / 3,000 | | `restore-by-generation` | 2 / 3,000 |

+| `hostguard` | 5 / 3,000 | | `purge-reserve-first` | 2,279 / 3,000 |

+| `purge-adopts` | 10 / 3,000 | | `purge-journal` | 1,969 / 3,000 |

+| `admission-registration` | 36 / 3,000 | | `registration-recovery` | 1,957 / 3,000 |

+| `purge-claim-fence` | 26 / 3,000 | | `fence-etag` | 18 / 3,000 |

+| `claim-never-deleted` | 8 / 3,000 | | `cancelled-creates` | 373 / 3,000 |

+| `orphan-no-deadline` | 60 / 3,000 | | `orphan-order` † | 2 / 30,000 |

+| `evidence-whole-tree` | 2 / 3,000 | | `evidence-from-state` | 2,778 / 3,000 |

+| `floor-boot-recovery` | 2,538 / 3,000 | | `participant-rows` | 4 / 3,000 |

+| `revalidate-before-effect` | 18 / 3,000 | | `sign-before-safeuntil` | 14 / 3,000 |

+| `sign-at-check` | 11 / 3,000 | | `sdk-no-resign` | 11 / 3,000 |

+| `lost-quarantine` † | 12 / 30,000 | | `cut-deadline` | 10 / 3,000 |

+| `revert-journal` | 17 / 3,000 | | `rollback-journal` † | 3 / 30,000 |

+| `dirty-return` | 2 / 3,000 | | `commit-before-open` | 10 / 3,000 |

+| `lost-return-park` | 3 / 3,000 | | `target-park` | 42 / 3,000 |

+| `abort-target-owner` | 1,061 / 3,000 | | `timer-freeze` | 6 / 3,000 |

+| `timer-canonical` | 3 / 3,000 | | `markers-last` † | 10 / 30,000 |

+| `source-readiness` | 7 / 3,000 | | `seal-by-version` † | 15 / 30,000 |

+| `staging-quiet` | 1 / 3,000 | | `fresh-admission` | 16 / 3,000 |

+| `stale-hold-release` | 2 / 3,000 | | `obligations-block-ops` | 22 / 3,000 |

+| `claim-op-exclusive` | 157 / 3,000 | | `recovery-current-inputs` | 51 / 3,000 |

+`fence-by-installation` and `sweep-namespace` are liveness and

+long-horizon properties the sweep cannot reach: a rolled-back move back

+converges like a served one, and no seed recreates a host 33 times. Their

+witnesses are the evidence, and the first is also the unmutated

+round-trip test claim rev 6 asks for.

+**Caught only in a combination: 11 rules.** Each partner's own count, on

the same seeds, shows what the combination adds; the witness column is

-the rule's witness under the combination.

+the rule's witness under the combination, having held under every

+proper subset in the gate.

|---|---|---|---|---|

-| `purge-claim-fence` + `fence-etag` (**the re-read alone**, rev 7's CC21 as proposed) | 298 / 30,000 | `purge-claim-fence` 260, `fence-etag` 189, `registration-check` 0 | (the two `registration-check` rows below) | the creator pauses after its re-read; purge drains, tears down and finishes; the CAS from free succeeds: a store destroyed under a creating or serving host. The re-read is not a fence |

+| `purge-claim-fence` + `fence-etag` (**the re-read alone**, rev 7's CC21 as proposed) | 307 / 30,000 | `purge-claim-fence` 266, `fence-etag` 195, `registration-check` 0 | (the two `registration-check` rows below) | the creator pauses after its re-read; purge drains, tears down and finishes; the CAS from free succeeds: a store destroyed under a creating or serving host. The re-read is not a fence |

| `declare-lost-compute` + `watchdog-independent` | 3 / 100,000 | `declare-lost-compute` 0 / 100,000 (its witness alone: violated), `watchdog-independent` 0 / 100,000 | violated | two writers after a paused or frozen target resumes |

+`commit-before-open` + `dirty-return` (124 / 30,000) is no longer a

+combination the model needs: `commit-before-open` is caught alone by

+INV-5 (115 / 30,000 and its witness), and the pair's extra seeds are

+`dirty-return`'s.

**Liveness only: 2.** `readiness-key` (T2) and `config-before-probe`.

They have no witness: neither can violate an invariant.

@@ -2053,9 +2241,9 @@ only after its own horizon, and CC11 holds; the biased schedules do not

change that, because they delay only data writes, never an

acknowledgement. No witness: there is no interleaving to force.

-**Seeds:** 300 in the gate, with every witness (about a second); the

-30,000- and 100,000-seed baselines, this sweep and the witnesses are the

-evidence for rev 7.3.

+**Seeds:** 300 in the gate, with every witness under every subset (about

+a second); the 30,000- and 100,000-seed baselines, this sweep and the

+witnesses are the evidence for rev 7.4.

#### 14.2.6 What the model does not prove

@@ -2079,6 +2267,22 @@ evidence for rev 7.3.

budget (320), the reverse of production (over 15 minutes against 120 s).

Results about orderings carry over; results about which wait fits inside

which window do not (J2 §2).

+- **Restore fidelity (R3-1).** The model's transactions are append-only

+ ids; a history is an ordered list, and a conflict is a history that is

+ neither an extension nor a prefix of the chain. Updates, deletes and

+ the content of a transaction are not modelled, so the chain proves

+ that no two histories are ever merged and that every durable write

+ stays reachable, which is what the proofs use; it does not validate

+ litestream's LTX planning against updates and deletes. That is

+ implementation work against the real restore (§5.1, §15 step 8).

+- **Observation boundaries not taken in rev 7.4** (R3 review): the

+ target's cleanup is queued at its release, not after the source's

+ `recovered_at` (§7.8); a create refuses while a record PUT is pending

+ on the server, which a real console cannot see; the release check runs

+ the cold-restore oracle only, not the local and timer acknowledgement

+ check, so a later delete could erase evidence of an earlier loss; two

+ workers of one operation share a lease identity; the local-exclusion

+ passes carry an operation sequence now but no release version.

- **Adversarial scheduling is partial.** Paused opens, door reads,

staging signers and an earlier incarnation's replica writes wake at the

worst moment the model knows of; everything else wakes at random. The

@@ -2323,6 +2527,18 @@ only the very first claim for a host is created create-only. Rev 7.2's

model encodes that text (§14.2.2) and gives C5a its own mutation

(§14.2.5). No further claim change is requested.

+**Claim rev 6 (3ea3f90c), after joint round 3: no request from this

+spec.** Rev 6 answers R3-2 (orphan cleanup in a fixed order: record, then

+the claim fresh, then `DeleteIfMatch`), R3-3 (the installation-scoped

+retired marker) and R3-4 (the sweep discovers locations from the

+namespace; `retired_incarnations` is anti-reuse only). Rev 7.4 encodes

+all three (§6.4, §14.2.2) and asks platform-1e three questions, in

+`moves-claim-questions.md`: how operations are ordered for "at or

+before" in production (the model uses its op counter); whether §5.1 step

+5 presupposes a claim object exists (a record with no claim is a legacy

+host to adopt, §9); and which spec owns the statement that a sweep never

+touches the version `generation.json` names.

**Not a change, a note for platform-1e (model, rev 5).** Under rev 3 the

install wait on `quiet_after` never bites: every retirement acknowledges

only after its own `evidence time + H`, so the `quiet_after` it writes has

@@ -2559,3 +2775,22 @@ gave `lost-return-park`. Rev 7.3 ends that treatment (§22.9).

Found on the way: the purge drain's map-order nondeterminism (§14.2.2),

fixed; rev 7.2's sweep counts were subject to it by a few seeds.

+### 22.10 Joint round 3 (claim 465fee96, moves rev 7.3 dc7f2a63, model dc7f2a63)

+Astra's verdicts were "not ready" for all three artifacts. Claim rev 6

+(3ea3f90c) answers R3-2, R3-3 and R3-4; rev 7.4 answers the moves side.

+| finding | rev 7.4 |

+|---|---|

+| R3-1 (P1) "replay every version" is not an implementable restore algorithm | §5.1 is an algorithm: the snapshot named by version id and TXID in `generation.json`, continuation by contiguous TXID over versioned listings, duplicates and older checkpoints skipped, a conflict refused, a gap reported; the two changes litestream's restore needs are named. The model's restore is a chain over histories, not a union (§14.2.2), and §14.2.6 says what that does and does not prove |

+| R2-5 (open) dirty recovery inherits the landing's `configured` gate | §7.6 marks the `move.inputs` gate as forward-only; §7.8's dirty row says a recovery install renders and materializes current inputs, recorded as `recovery.inputs`; the `recovery-current-inputs` witness is that case (51 / 3,000 by the sweep as well) |

+| R3-3 (P2) retirement fences prevent a same-incarnation move back | claim rev 6's installation-scoped marker, taken into §6.4; the model fences per installation, replaces the fence in the landing's `checking` phase on a fresh read, and the `fence-by-installation` witness is the unmutated UK→US→UK round trip, serving on UK again; the mutation (rev 7.3's marker) never serves on UK. One question to platform-1e: the production order of op ids (§19.4) |

+| R3-7 (P2) the default cut budget cannot pass its own readiness formula | T11's permitted attempts depend on the budget (§7.3, §7.7); `budget_test.go` shows rev 7.3's formula refused every default move and the new one admits a tiny instance with two attempts |

+| R3-5 (P2) public admission before commit is not tested | the edge routes on the row (§9.5 unchanged): a request reaching a ready row on a landing target before the commit is INV-5, checked at every wake; `commit-before-open` is caught alone by the sweep (10 / 3,000, 115 / 30,000) and by its own witness; its combination with `dirty-return` is retired (§14.2.5) |

+| R3-6 (P2) mutation orchestration can succeed without verdicts | `mutate.sh` fails on scratch creation and `xargs` errors, requires exactly one well-formed verdict per requested mutation, and reports a rule with witnesses and no witness output as an ERROR (§14.2.1) |

+| R3-2 (P1), claim side | encoded: the orphan cleanup is a console plan with pauses between its observations and its delete, record ETags are unique per write, and the cleanup asserts it never deletes the claim's holder's record; `orphan-order` reads the claim first and its witness deletes a legitimate successor (§14.2.5) |

+| R3-4 (P2), claim side | encoded: the sweep discovers locations from the namespace, `retired_incarnations` is capped at 32, and the `sweep-namespace` witness lands a replication PUT of an incarnation 33 recreates old |

+| witnesses accept any violation; `reach` turns a missed milestone into INV-3; subsets not run | every witness names its failure and must violate with it; a missed milestone is INV-3 only where the milestone is the property (the round trip); the gate runs every proper subset of each combination and requires the witness to hold there (§14.2.1) |

+| `commit-before-open` wrongly among "caught" | it now has its own violation (INV-5) and witness; the pair is retired |

+| model fidelity: restore, admission, cross-object atomicity, local exclusion, same-operation workers, oracle, late creates, cleanup ordering, timing | restore and public admission taken (above); passes carry an operation sequence (R2-3, partly); the rest is listed as not taken in §14.2.6, each with what it hides |

diff --git a/internal/sim/hostlife/witness_test.go b/internal/sim/hostlife/witness_test.go

index d2763de54..ee3bb080b 100644

--- a/internal/sim/hostlife/witness_test.go

+++ b/internal/sim/hostlife/witness_test.go

@@ -144,7 +144,31 @@ func TestWitnesses(t *testing.T) {

needs = false

}

- check(t, x, mutated, needs, only != "")

+ if needs {

+ check(t, x, mutated, true, only != "")

+ continue

+ }

+ // the mutation set is not the witness's: report, enforce nothing.

+ // A wider combination may well violate it (the whole start check

+ // in place of its generation clause, either registration-check

+ // partner); the proper-subset proofs live in the gate

+ report(t, x, mutated, only != "")

+ }

+func report(t *testing.T, x witness, m string, trace bool) {

+ saved := mutated

+ mutated = m

+ defer func() { mutated = saved }()

+ w := newWitness()

+ x.run(t, w)

+ tag := "held"

+ if len(w.violations) > 0 {

+ tag = "violated: " + w.violations[0]

+ }

+ t.Logf("witness %s under %q (needs %q): %s", x.rule, m, x.needs, tag)

+ if trace {

+ dump(t, w)

}

diff --git a/internal/sim/hostlife/world_test.go b/internal/sim/hostlife/world_test.go

index a483ebcdf..beaae28e6 100644

--- a/internal/sim/hostlife/world_test.go

+++ b/internal/sim/hostlife/world_test.go

@@ -1,7 +1,7 @@

// Package hostlife is a deterministic, randomized model of the host

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

-// rev 5.2, 465fee96) and Phase 1 of move-any-app

-// (docs/superpowers/specs/2026-10-02-move-any-app-design.md, rev 7.3).

+// rev 6, 3ea3f90c) and Phase 1 of move-any-app

+// (docs/superpowers/specs/2026-10-02-move-any-app-design.md, rev 7.4).

// Since joint round 2 the model encodes what the specs say and nothing

// stronger: restore reads the holder's location and the generation the