carlos / platform Public

spec: move-any-app rev 7.13, joint round 12 and claim rev 6.14

Regional coverage recorded and discharged (R12-3): region and
predecessor_region on every admission record, PublishGeneration's walk,
every cold admission publishing, CoverRegionPredecessors inside the CAS
that queues a region's whole-location park (the commit, a rollback's
release, the lost-target release); two readings for the claim (born
covered under a pending park; the sweep covers what it parks) and two
more the 100,000-seed baseline forced (a live predecessor is left
uncovered; a lost target's every session since the cut is declared).
INV-17 as a whole-location park completes.

The loss oracle matches the declared identity (R12-1); the probe
deadline is checked before each start and before readiness is accepted
(R12-2), INV-19 and TestProbeWindow; one operative rule set in §7.14
mirroring claim rev 6.14's structure, the contradicting passages
corrected or marked history (R12-4); the recovery limit is nine (R12-5);
retention is conservative (R12-6); the absent-marker mutant stands alone.

Model 42af7bfc: 101 rules, 65 witnesses; 30,000 and 100,000 seeds clean
(621 s, 1906 s); mutation sweeps at 3,000 (86 caught, 15 expected
misses), 30,000 (63, 2) and 100,000 (30, 0), exit 0; 88 of 101 caught
alone. Records in ~/.cache/nearest-region/rev713-sweeps/.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

claude 2 weeks ago 1f511c4222659590e2313dac993697cdad08af53 parent 42af7bf

1 file changed, +618 −154

docs/superpowers/specs/2026-10-02-move-any-app-design.md +618 −154

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 24137b7e0..4f6e7e7af 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,56 @@

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

**Date:** 2026-10-05

-**Revision:** 7.12.

+**Revision:** 7.13.

+- **Rev 7.13** answers **joint round 12** (`CODEX-FINDINGS-JOINT-R12.md`,

+ cited "R12-n") and is written against **claim spec rev 6.14**

+ (dc146058, whose §6.4a has one operative subsection, "Admissions,

+ coverage and retirement (operative, rev 6.14)", and answers R12-4 and

+ R12-6; rev 6.13, b3825827, adopted rev 7.12's five notes) and the

+ library E at 47426cc1 (unchanged since round 12 judged it

+ merge-ready); §22.19 has every disposition. **Coverage is regional

+ and recorded** (R12-3): every admission record carries `region` and

+ `predecessor_region`; `PublishGeneration` walks the uncovered records

+ (a predecessor holding nothing anywhere is covered with no chore, one

+ in the publishing region gets its chore and is covered, one in another

+ region stays uncovered with no chore, and one that is the live

+ generation again is left uncovered too, a reading against item 5's

+ first bullet: covered, nothing would retire it later), every cold admission publishes, a prepared generation's

+ included, and **`CoverRegionPredecessors`** runs inside the CAS that

+ queues a region's whole-location park: the commit's park of the

+ source region, a rollback's park of the target region, the console's

+ lost-target release (note 5's discharge, adopted). Two readings for

+ the claim: a record admitted while such a park is already queued for

+ its predecessor's region is **born covered**, and the sweep's CASes

+ cover the records whose predecessors it parks. INV-17 checks, as a

+ whole-location park completes, that no record whose predecessor was

+ there is uncovered. **The loss oracle matches the declared identity**

+ (R12-1): acknowledgements carry the writer session and generation of

+ the process that gave them, a `writes_lost` record exempts the writes

+ of the session it names and no other, the source-cut declaration

+ stays separate, and a declared-lost target's **every** session since

+ the cut is declared, certified or not (a probe session that certified

+ and a warm continuation that did not are two, and no return lane

+ carries either's writes); a two-session witness (INV-18). **The probe deadline

+ is checked before each start and before readiness is accepted**

+ (R12-2): an expired attempt never starts, a late readiness is not

+ accepted, INV-19 at every probe acceptance, and `TestProbeWindow`

+ walks k = 29, 30, 31. **One operative rule set for admission** (R12-4):

+ §7.14 states it, mirroring claim rev 6.14's structure, and the

+ passages that disagreed are corrected or marked history: the restore

+ contract's "after installed and probed", the dirty-return region

+ rows, the start table's failed-host marking (a serving wake's only; a

+ probe never marks the host failed), the recovery limit (nine attempts,

+ R12-5), and `holder.admissions` retention (conservative, no

+ compaction). The absent-marker sweep fault has its own rule and

+ mutant, `absent-marker-origin`, so `wOriginSwept`'s evidence no longer

+ rides on `baseline-live`. Rules `foreign-region-uncovered`,

+ `cover-at-park`, `session-scoped-loss`, `probe-window`,

+ `absent-marker-origin` (101 in all); witnesses

+ `wTwoSessionDeclaration`, `wRollbackBaselinePreserved`,

+ `wCommitCoverage`, `wCommitInterrupted`, `wCommitReplayed`,

+ `wProbeWindowAt` (65 in all). Results in §14.2.3 and §14.2.5.

- **Rev 7.12** answers **joint round 11** (`CODEX-FINDINGS-JOINT-R11.md`,

cited "R11-n") and is written against **claim spec rev 6.12**

@@ -1057,9 +1106,10 @@ fails there first (§14.2.6).

opened rollback recovery, a push's writer (R8-2). The library's call

is `AdmitWriter(Admission{ObservedOpID, ObservedPhase,

ObservedSession, ObservedGeneration, Box, Mode, NewGeneration,

- PredecessorCertified, RemoteMaxTXID, KeepStamp,

- BaselineCoversPredecessor})` (R10-4), and this spec's model is shaped

- like it. It requires the observed `op.id` and `op.phase` (serving's

+ PredecessorCertified, RemoteMaxTXID, KeepStamp, Coverage, Region,

+ PredecessorRegion})` (R10-4; `Coverage` since claim rev 6.12,

+ `Region` and `PredecessorRegion` since rev 6.13, E 47426cc1), and

+ this spec's model is shaped like it. It requires the observed `op.id` and `op.phase` (serving's

`""` compared literally, so a closure computed under serving fails

once any operation starts), the observed `holder.session` and

`holder.generation`, and **`op.exec` to be this box**, in every op

@@ -1070,9 +1120,14 @@ fails there first (§14.2.6).

re-establishes its evidence, the certificate, the exec handover,

rather than re-reading alone. It writes `holder.session = its

resulting gen`, `holder.writer_box = this box`, and a record in

- **`holder.admissions`** `{session, box, generation, predecessor:

- {session, box, generation, stamp}, mode, coverage, covered,

- writes_lost?}` (claim rev 6.12; the library's `AdmissionRecord`).

+ **`holder.admissions`** `{session, box, generation, region,

+ predecessor: {session, box, generation, stamp}, predecessor_region,

+ mode, coverage, covered, writes_lost?}` (claim rev 6.14 §6.4a item

+ 1; the library's `AdmissionRecord`). `region` is where the new

+ writer's generation keeps its objects, the admitted box's region;

+ `predecessor_region` is the last record's `region` (before any

+ record, the writer box's region, `""` when the generation holds

+ nothing anywhere, as after a create).

**The predecessor is the last record there**, with its own session,

box and generation; it never comes from the holder's fields, which a

clean return has reset to the source's generation for the restore

@@ -1080,8 +1135,11 @@ fails there first (§14.2.6).

journalled the target's session and box with the source's

generation, a writer that never was; INV-16). `holder.admissions`

lives in the holder, so it survives every operation transition,

- release and new operation; it is trimmed to the last eight covered

- records, never an uncovered one or the current predecessor. The

+ release and new operation; its retention is **deliberately

+ conservative** (claim rev 6.14 item 8, R12-6): covered records are

+ trimmed from the front only, while more than eight remain, an

+ uncovered record stops the trimming and everything behind it is

+ kept, and there is no compaction. The

admission **never replaces the operation**: kind, id, phase,

participants, obligations and the rest of the journal are kept.

- **Failed starts are governed by a retry policy, never by another

@@ -1164,7 +1222,13 @@ fails there first (§14.2.6).

**source's cut session** (`cut.session`, journalled at the stop)

only: a later session of the recovered source that dies uncertified

is declared like any other, and a return made clean only by a

- declared-lost target is not covered at all. Only

+ declared-lost target is not covered at all: it records `writes_lost`

+ for **every session the target was admitted into since the cut**,

+ certified or not (a probe session that closed cleanly and a warm

+ continuation that died are two; the first's writes are durable only

+ in the lost target's region, and no return lane carries either's;

+ seed 33373 / 100,000, hidden until the session-scoped match of

+ R12-1), each alerted. Only

coverage `""` with no certificate records `writes_lost`, and the

record always names its coverage, certified or not. A seal built

from the **remote** because the disk was gone (`seal.from_db` false,

@@ -1206,16 +1270,31 @@ fails there first (§14.2.6).

newID)`** CAS (claim rev 6.12, replacing `QueueGenerationRetire`):

bound to the observed operation and phase like the admission, legal

while serving and inside any operation a writer runs in (a restarted

- landing probe, a rollback's or a revert's source; R11-5), it marks

- every admission record up to the published generation covered and

- queues one `park-generation` per dead generation, deduplicated: the

- predecessor; behind a lagging marker, every generation of the chain

- of unfinished admissions between the marker's generation and the new

- one, and the marker's; and the predecessor of any earlier cold

- admission in `holder.admissions` not yet covered (its writer died

- after its marker landed and before the CAS). Its chores carry `op =

- op.id` inside an operation and `op = "session:<holder.session>"`

- while serving. **Retirement happens only through it, and only of

+ landing probe, a rollback's or a revert's source; R11-5), it

+ **walks every uncovered cold record** of `holder.admissions` (claim

+ rev 6.14 item 5): a predecessor whose `predecessor_region` is `""`

+ (it holds nothing anywhere) is covered with no chore; one that is

+ the published, live generation again (a clean return's source

+ generation, a republished lagging marker's) is **left uncovered**

+ with no chore (item 5's first bullet covers it; covered, nothing

+ would retire it once a later admission supersedes it, since that

+ admission's predecessor is the last record and not the generation

+ it restored from: seed 41914 / 100,000 left the source's generation

+ as residue; a reading for the claim, §19.4); one whose objects are in the publishing

+ `region` gets one deduplicated `park-generation` chore there and is

+ covered; one whose objects are in **another region** stays

+ uncovered, with no chore, and the walk goes on. The walk finds what

+ rev 7.12 enumerated: the predecessor; behind a lagging marker,

+ every generation of the chain of unfinished admissions between the

+ marker's generation and the new one, and the marker's; and the

+ predecessor of any earlier cold admission not yet covered (its

+ writer died after its marker landed and before the CAS). **Every

+ cold admission publishes**, a prepared generation's included (rev

+ 7.12's model left a prepared generation's predecessor to the

+ operation, R12-3): a landing's publication in the target's region

+ leaves the source's generation uncovered, and the commit covers it

+ (below). Its chores carry `op = op.id` inside an operation and `op =

+ "session:<holder.session>"` while serving. **Retirement happens only through it, and only of

predecessors recorded in `holder.admissions`** (R11-2). An adopted

legacy host's generation is the location root itself, named by the

sentinel **`"@root"`** so a chore can name it; `""` and `"@root"`

@@ -1225,20 +1304,37 @@ fails there first (§14.2.6).

admission, and the adoption writes `holder.writer_box` as the box

running the pre-release process, so the first cold admission's

`writes_lost` names the writer whose unuploaded writes it leaves

- behind (R10-5, R11-3). **Coverage is per region**: a record is

- covered when its predecessor's chore was queued in the region that

- holds the predecessor's objects (or the predecessor holds none

- anywhere); a predecessor whose objects live in another region (a

- move's source generation, seen by the target's publication whose

- chain walks back through it) stays uncovered for that region's next

- `PublishGeneration`, since a chore queued from the target's region

- would park nothing there and one queued into the source's region

- would park a generation the rollback may still need. A dead

- generation holding nothing yet still gets its chore in the publishing

- region: a dead writer's late upload or certificate may land in it

- within the chore's horizon. A failed

- cold start leaves an empty, unpublished generation; the next

- attempt is cold again and the marker it publishes retires it.

+ behind (R10-5, R11-3). **Coverage is per region and recorded** (claim rev

+ 6.13 and 6.14, R12-3): a record is covered when its predecessor's

+ retirement is in hand in the region that holds the predecessor's

+ objects. A predecessor whose objects live in another region (a

+ move's source generation, seen by the target's publication) is

+ **never queued into its region from here**, since the rollback may

+ still need it (seeds 1036 and 1296 / rev 7.12; witness

+ `wRollbackBaselinePreserved`); it is covered either by that

+ region's own next publication or by

+ **`CoverRegionPredecessors(op, phase, region)`**, composed into the

+ CAS that queues that region's park of the whole location, which

+ retires those generations wholesale and so queues nothing: the

+ commit's `park-superseded` of the source region (§7.9), a

+ rollback's `park-superseded` of the target region at the target's

+ release (§7.8), and the console's release of a declared-lost target

+ (§7.10). Two readings for the claim (§19.4): a cold admission made

+ while the claim already holds such a park for its predecessor's

+ region is **born covered**, since a rollback's return is admitted

+ after the release queued the target region's park and the CAS that

+ queued it could not see the record (seed 1036 / 3,000); and the

+ at-rest sweep (§6.4), which parks a region's dead generations

+ wholesale, covers the records whose predecessors it parks in the

+ CASes that queue and acknowledge its `park-sweep`. INV-17: when a

+ whole-location park of `holder.location` completes in a region, no

+ record whose predecessor's objects were there is uncovered. A dead

+ generation holding nothing yet still gets its chore in the

+ publishing region, as does one whose objects were parked already: a

+ dead writer's late upload or certificate may land in it within the

+ chore's horizon. A failed cold start leaves an empty, unpublished

+ generation; the next attempt is cold again and the marker it

+ publishes retires it.

- **A marker that lags `holder.generation`** (an absent marker is the

origin `""`, for the sweep as for the restore, R11-1) is read through

`holder.admissions`: when it names the predecessor of the latest

@@ -1332,8 +1428,16 @@ So:

or from a dead writer of the same incarnation (step 9), 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;

+- the claim moves to a new generation at its writer's **cold admission**,

+ before the restore, the app start and the probe (§7.14; rev 7.12's

+ wording here, "only after that generation is fully installed and

+ probed", described rev 7.9's protocol and is superseded, R12-4). A

+ restore still never meets a half-written generation: a prepared

+ generation is complete, snapshot and anchor, before any admission

+ opens it, and a fresh one is empty until its own writer's first

+ upload, which is the baseline's full file and lands before the marker

+ names the generation; a restore reads the baseline the admission

+ names, never a generation under construction;

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

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

@@ -1418,8 +1522,8 @@ is the region of the holder's current installation:

| `landing` after the flip, before the target's probe is admitted | the source's region: `holder.generation` is still the pre-move generation, and the target's prepared generation is not yet named |

| `landing` from the target's probe's cold admission on, committed or not | the target's region: `holder.generation` is the generation that admission chose, the prepared one or, for a restarted probe, a fresh one restored from it (§7.14; rev 7.11's row said "before the commit", R10-3) |

| `restoring`, clean, from the return CAS on | the source's region: the return CAS named the source's generation again for the restore, and the source's re-admission moves to a fresh generation there |

-| `restoring`, dirty, until the source's probe is admitted | the source's region, for the pre-move generation; the return generation is built there but not yet named |

-| `restoring`, dirty, from the source's probe's cold admission on | the source's region, for the return generation |

+| `restoring`, dirty, until the source's probe is admitted | the target's region, for `holder.generation`, which is still the target's last admission: a dirty return resets nothing (only a clean return's CAS names the source's generation again), and the generation stays the target's until the source's probe is admitted. In practice nothing is live there: the target stopped, and the target region's whole-location park is queued at the release with the records whose predecessors are there covered in that CAS (§7.8). The return generation is built in the source's region but not yet named (rev 7.12's row assigned the pre-move generation here, before any source admission, R12-4) |

+| `restoring`, dirty, from the source's probe's cold admission on | the source's region, for the return generation, which that admission named; its record's predecessor is the target's writer, in the target's region, born covered under the target region's park |

| `creating`, `deleting`, `parking`, `purging`, free | none: nothing is live |

**The start check (INV-4, J2-R2-8).** Before every spawn (`Start`, `Seed`,

@@ -2166,19 +2270,32 @@ 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, and never more than T11 admitted for this

- budget (§7.3, R3-7). **One attempt is one cold admission** (§7.14): its

- app may be restarted under the retry policy of §5.1 step 9 within the

- attempt's **30 s readiness window**, which runs from the first start

- (the waits total 15 s, each start's own time is on top), and the fifth

- failure or the window's end, whichever comes first, ends the attempt;

- the next attempt, if the budget allows one, is a new cold admission

- into a fresh generation restored from the dead attempt's. A probe never

- marks the host failed; the operation's rollback (or `stuck`) is its

- outcome. The budget's three attempts and the policy's five restarts are

- different things: at most three admissions, each with at most five

- starts inside 30 s. The absolute `cut_deadline` (§7.4) still bounds the

- whole.

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

+ for this budget (§7.3, R3-7); a recovery probe (a revert's or a

+ rollback's source) has **nine** before `stuck` (§7.8, §7.10; R12-5).

+ **One attempt is one cold admission** (§7.14): its app may be

+ restarted under the retry policy of §5.1 step 9 within the attempt's

+ **30 s readiness window**, which runs from the first start (the waits

+ total 15 s, each start's own time is on top), and the fifth failure or

+ the window's end, whichever comes first, ends the attempt; the next

+ attempt, if the budget allows one, is a new cold admission into a

+ fresh generation restored from the dead attempt's. **The deadline is

+ checked before each start and before readiness is accepted** (R12-2):

+ an attempt whose window passed while the agent was paused, or between

+ a failed start and its retry, does not start the app at all (rev 7.12

+ checked only while the environment was unready or after a failed

+ start, so a successful start after the window made an expired attempt

+ the probed writer); an app that answers readiness at or after the

+ deadline is stopped and the attempt fails; and the probe's acceptance

+ checks the attempt it accepts answered within its window (INV-19). At

+ the boundary, readiness k steps after the attempt's first start: k =

+ 29 is accepted, k = 30 fails before the start, k = 31 fails at the

+ deadline with the environment still unready (`TestProbeWindow`). A

+ probe never marks the host failed; the operation's rollback (or

+ `stuck`) is its outcome. The budget's attempts and the policy's five

+ restarts are different things: at most three (or nine) admissions,

+ each with at most five starts inside 30 s. The absolute `cut_deadline`

+ (§7.4) still bounds the whole.

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

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

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

**Obligations.** The target's `released` CAS also adds to the claim, in the

same write, a `park-superseded` obligation for the target box and region

(its replica, staging and local state; destination

-`superseded/<move id>/<host>/`), which its `cleaning` phase discharges. A

+`superseded/<move id>/<host>/`), which its `cleaning` phase discharges,

+and in the same write runs `CoverRegionPredecessors` for the target

+region (claim rev 6.14 item 6, R12-3): every record whose predecessor's

+objects are the target's (a restarted probe's record names the dead

+probe's generation there) is covered, with no chore, since the park

+retires the whole location. The console's release of a declared-lost

+target (§7.10) queues the same park and covers the same way. The

+source's return admission comes after this CAS, so its record, whose

+predecessor is the target's writer, is **born covered** under the park

+the claim already holds (§5.1 step 9). A

dirty source recovery adds one for its own region and box for what its

install supersedes. These are the claim spec's durable chores (§2 there);

§19.3 asks for the kind.

@@ -2244,7 +2370,9 @@ CAS-clears `move`. Until then `move` and the claim stay, so nothing else

can start on the host (codex 6). The source serves from `opened` on; the

held claim blocks only other operations.

-Three failed recovery probes: `stuck`, held (§7.10).

+Nine failed recovery probe attempts (three times the landing's budget of

+three; `probeTries*3` in the model): `stuck`, held (§7.10). Rev 7.12's

+sentence here said three, against its own model description (R12-5).

**Waiting.** If `release_deadline` passes with no target evidence, the move

stays in `rolling_back` ("waiting for uk to release"), paged, safe: nothing

@@ -2484,15 +2612,90 @@ and a new agent process never resumes it (a new agent is a new session):

| step | action | if it fails |

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

| decide | read the claim; `op.exec` must be this box and the kind one that admits; the certificate for `holder.session` decides warm or cold; a cold admission's generation is the operation's prepared one if `holder.generation` is not it or a descendant of it, else a fresh id; `KeepStamp` when `holder.stamp > holder.session`; `Coverage` `sealed` for a prepared generation from a `from_db` seal, `clean-return` for a clean rollback's return with `src_covered`, else `""`; a lagging `generation.json` is read through `holder.admissions` (below) | nothing happened |

-| **`AdmitWriter`** | the CAS of §5.1 step 9, **first**: session, writer_box, the `holder.admissions` record with the last record as its predecessor; cold: generation, stamp unless kept, `writes_lost` only for coverage `""` with no certificate; **no chore**: the predecessor is the unfinished generation's baseline until the marker names the new one (R10-2); the carried files are retagged with the new stamp here | a conflict: re-establish the evidence and decide again |

+| **`AdmitWriter`** | the CAS of §5.1 step 9, **first**: session, writer_box, the `holder.admissions` record with the last record as its predecessor, its own region and the predecessor's region; cold: generation, stamp unless kept, `writes_lost` only for coverage `""` with no certificate; **no chore**: the predecessor is the unfinished generation's baseline until the marker names the new one (R10-2); born covered when the claim already holds a whole-location park for the predecessor's region (a rollback's return); the carried files are retagged with the new stamp here | a conflict: re-establish the evidence and decide again |

| purge | delete the local database, with an error-returning purge | the start waits and purges again; the session stands |

| restore | warm: `holder.generation` from this region's remote, to at least the certificate's `max_txid`; cold, prepared: the prepared generation from its pinned snapshot and anchor (the operation's build journal); cold, fresh: the baseline from this region's remote, the predecessor or, behind a lagging marker, the nearest generation of the chain that holds an object | the start waits; a warm restore short of `max_txid` is an alert, the remote is incomplete |

-| start, readiness | the app starts on the restored database and answers its readiness path; nothing it acknowledges is outside the session | the retry policy (§5.1 step 9): a doubling backoff from one step, five attempts, then the host is marked failed, the start abandoned, and no session is created until an operator clears it |

+| start, readiness | the app starts on the restored database and answers its readiness path; nothing it acknowledges is outside the session. A probe checks its attempt's deadline before the start and before accepting readiness (§7.7, R12-2) | the retry policy (§5.1 step 9): a doubling backoff from one step, five attempts. **A serving wake**: at the fifth failure the host is marked failed, the start abandoned, and no session is created until an operator clears it. **A probe**: the fifth failure, the window's end or a late readiness ends the attempt, the operation counts one budgeted try, and the host is never marked failed (claim rev 6.14; rev 7.12's row applied the marking to probes too, R12-4) |

| first upload (cold, fresh, a non-empty baseline) | the full file `[1, 1]` of the restored database, captured once and acknowledged to the client; the generation has a root; it is in the session's ledger (R10-7) | retried with the same bytes after the client's wait, whether the original timed out or completed unseen; the session is uncertain for good |

-| marker (cold) | `generation.json` names the new generation: the pinned snapshot identity for a prepared one, `snapshot_txid = 0` for a fresh one (its root is `[1, 1]`); never before the root exists (INV-11). **Then `PublishGeneration`** (§5.1 step 9), bound to the operation and phase it observed, legal in `serving` and in every operation a writer runs in: the records up to the new generation are covered and one `park-generation` per dead generation is queued, the predecessor's, the chain's and any uncovered record's | retried after the timeout; the writer waits |

+| marker (cold) | `generation.json` names the new generation: the pinned snapshot identity for a prepared one, `snapshot_txid = 0` for a fresh one (its root is `[1, 1]`); never before the root exists (INV-11). **Then `PublishGeneration`** (§5.1 step 9), for every cold admission, a prepared generation's included, bound to the operation and phase it observed, legal in `serving` and in every operation a writer runs in: the walk over the uncovered records queues one `park-generation` per dead generation whose objects are in this region, the predecessor's, the chain's and any uncovered record's, and covers them; a predecessor in another region stays uncovered for that region's whole-location park or publication | retried after the timeout; the writer waits |

| anchor (warm, when the restored position is above the level-0 maximum) | `[N, N]`, acknowledged to the client; in the ledger (R10-7) | retried with the same bytes; the session is uncertain for good |

| open | replication opens; the replica reads its remote position at its first sync; every later upload is the session's. An app stopped idle before this point is not closed: the replicator opens, ships what the app wrote, then closes cleanly | |

+#### Admissions, coverage and retirement (operative, rev 7.13)

+This list, with §5.1 step 9 and the two tables above, is the operative

+rule set for writer admission (R12-4), mirroring claim rev 6.14 §6.4a's

+operative subsection item for item. Where any other passage of this

+spec reads differently (the restore contract's older wording in §5.1,

+the §7.8 rows as rev 7.11 had them, the authoritative-region table, the

+per-revision blocks of §14.2.2, which are history by construction),

+this text wins.

+1. **The record.** Each admission appends `{session, box, generation,

+ region, predecessor: {session, box, generation, stamp},

+ predecessor_region, mode, coverage, covered, writes_lost?}` to

+ `holder.admissions`. The predecessor is the last record, never the

+ holder's fields (INV-16); `region` is the admitted box's region, where

+ its generation's objects are; `predecessor_region` is the last

+ record's `region`, before any record the writer box's region, `""`

+ when the generation holds nothing anywhere. A record is **born

+ covered** when the claim already holds a whole-location park of

+ `holder.location` for its predecessor's region (a reading for the

+ claim, §19.4).

+2. **Coverage** `""` | `sealed` | `clean-return`, as §5.1 step 9 states

+ it: `sealed` for a `from_db` seal of the stopped predecessor,

+ `clean-return` for a clean rollback with `src_covered`, a target that

+ gave its evidence and no declared-lost box, speaking for the target's

+ probe session and the source's cut session only; `""` otherwise, and

+ without a certificate it records `writes_lost` (behind a lost target, one

+ record for every session the target was admitted into since the cut,

+ and a second for the source's cut session when `src_covered` is

+ false). A `writes_lost` record declares the writes of the session it

+ names and no other (INV-18, R12-1).

+3. **The baseline.** A prepared generation from its pinned snapshot in

+ the admitting box's region, opened once; otherwise the predecessor

+ generation's remote in this region; in an unfinished run the newest

+ generation of the run that holds an object, else the marker's; an

+ empty generation outside an unfinished run is refused and alerted.

+4. **Stamps.** A cold admission takes a new stamp except under

+ `KeepStamp` (`holder.stamp > holder.session`); a clean return's CAS may

+ name the source's generation and stamp again, leaving

+ `holder.session` alone.

+5. **Publication.** After the marker names the generation, one

+ `PublishGeneration(observedOpID, observedPhase, observedSession,

+ publishedGeneration, region, newID)` walks the uncovered records as

+ §5.1 step 9 states: no objects anywhere, covered, no chore; live

+ again, left uncovered, no chore; in `region`, one deduplicated chore,

+ covered; another region, uncovered, no chore, the walk continues.

+ Every cold admission publishes. Retirement happens only through it or

+ through item 6.

+6. **Whole-location parks cover.** `CoverRegionPredecessors(op, phase,

+ region)` runs inside the CAS that queues a region's park of the whole

+ location: the commit's park of the source region, the target's

+ release and the console's lost-target release for the target region.

+ It covers every record whose predecessor's objects are that region's

+ and queues nothing. The at-rest sweep covers what it parks in its own

+ CASes (a reading, §19.4). INV-17 checks the composition as each such

+ park completes. A foreign-region predecessor is never queued into its

+ region from another one.

+7. **Starts.** The admitting CAS first; a new agent process stops a

+ running app, admits a new session and restarts it; failed starts are

+ the retry policy's, five under one session with a doubling backoff;

+ the failed-host marking is a **serving wake's** at the fifth failure;

+ a probe attempt ends at the fifth failure, at its 30 s window, checked

+ before each start and before readiness is accepted, or at a late

+ readiness, counts one budgeted try (three for a landing, nine for a

+ recovery) and never marks the host failed.

+8. **Retention and lost boxes.** `holder.admissions` is trimmed

+ conservatively: covered records from the front only, to eight, never

+ past an uncovered one; no compaction. A declared-lost box's timers are

+ declared on the console's record and alerted; adoption sets

+ `holder.writer_box` to the pre-release writer's box.

+**History.** The paragraphs that follow and §14.2.2's per-revision

+blocks record how these rules were reached; where they differ from the

+list, the list governs.

An admitted writer that dies between its CAS and its marker leaves

`holder.generation` naming an **unfinished** generation `generation.json`

does not (R10-2): its journalled predecessor is the live baseline, no

@@ -2787,6 +2990,14 @@ combination-only, unexercised), each with its reason. The sweep exits

nonzero on any ERROR, any unexpected MISSED, and any expected miss that is

now caught (STALE).

+**Rev 7.13: INV-17 at the park, `TestProbeWindow`.** The oracle for

+regional coverage runs when a whole-location park of `holder.location`

+completes in a region, not at the end: a record whose predecessor's

+objects were there and that is still uncovered is INV-17 at that CAS

+(a record born after the park is not in question). `go test` runs

+`TestProbeWindow` beside the witnesses: the landing probe's environment

+ready k steps after the attempt's first start, for k = 29, 30, 31.

**Rev 7.12: the final oracle runs the recovery.** When the run is

quiescent with the serving host at rest after a session that did not

certify, the final oracle no longer exempts the acknowledged, unuploaded

@@ -2854,7 +3065,8 @@ 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).

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

+`TestProbeWindow`, the probe deadline's boundary (§7.7, rev 7.13).

**Rev 7.6: the pinned libraries, observed.** `internal/sim/litestreamfacts/`

is a second test-only package: it drives litestream v0.5.14 and

@@ -3380,6 +3592,119 @@ readiness, and same-operation lease identities.

review's 3 GiB workload is reproduced (108.68 s with three passes at one

rate, 124.04 s with the fourth) and refused by rev 7.7's arithmetic.

+**Rev 7.13: joint round 12 and claim rev 6.14.**

+- **Regions on the record (claim rev 6.14 item 1, R12-3).**

+ `admissionRecord` gains `Region` and `PredRegion` (`-1` for a

+ predecessor holding nothing anywhere); `admitInput` gains `Region`

+ and `PredecessorRegion`, mirroring E's `Admission` (47426cc1).

+ `predecessorRegion(holder)` is the last record's box's region, before

+ any record the writer box's, else wherever `holder.generation` holds

+ an object, else `-1`.

+- **The publication walk (item 5).** `publishGeneration(b, c,

+ observedOpID, observedPhase, session, published, region, newID)` loses

+ its `dead` set and `uncovered`: it walks every uncovered cold record,

+ covers one whose predecessor holds nothing anywhere, leaves one whose

+ predecessor is the published generation itself (live again; covered,

+ as item 5's first bullet reads, nothing retired it later, seed 41914 /

+ 100,000), queues one deduplicated chore for one whose predecessor is

+ this region's and covers it, and leaves one whose predecessor is

+ another region's. The marker stage calls it for every

+ cold admission, prepared generations included; the lag path's

+ republish calls it without a dead set. Trimming is E's: covered

+ records from the front only while more than eight remain, an

+ uncovered record stops it. Rule `foreign-region-uncovered` (the

+ mutation queues the chore into the predecessor's region); witness

+ `wRollbackBaselinePreserved`: a probed landing whose target published,

+ the chore's quiet time brought forward (the schedule seeds 1036 and

+ 1296 / rev 7.12 found with a landing open past the horizon), the

+ source region's runner within the settle window, then a clean

+ rollback; under the mutation the return restores an empty database

+ (INV-2).

+- **Coverage at whole-location parks (item 6).**

+ `coverRegionPredecessors(n, region, why)` is composed into three

+ CASes: the commit's (`followRecord`, the source region's

+ `park-superseded`), the target's release (`releaseTarget`, the target

+ region's) and the console's lost-target release (the same park). A

+ cold record is born covered when the CAS that admits it finds a

+ `park-superseded` of `holder.location` for its predecessor's region

+ already queued (seed 1036 / 3,000: the return's record is admitted

+ after the release). The sweep covers what it parks:

+ `coverSweptPredecessors` in the CAS that queues the `park-sweep` (a

+ predecessor with a sweepable object) and in the one that acknowledges

+ it (a predecessor whose objects it retired). Rule `cover-at-park`

+ (the mutation leaves every one of these uncovered); INV-17 in the

+ `park-superseded` acknowledgement CAS: an uncovered cold record whose

+ predecessor's objects were in that region, other than the live

+ generation. Witnesses `wCommitCoverage` (the commit's CAS covers the

+ target's record, one park queued), `wCommitInterrupted` (the record

+ flips to committed, every actor pauses past the horizon, whoever

+ follows the record later performs the one CAS), `wCommitReplayed`

+ (`followRecord` after the commit is refused, one park, coverage

+ stands); under the mutation INV-17 at the source region's park.

+- **The declared identity (R12-1).** `ack` gains `Session` and `Gen`,

+ set from the **process** that acknowledged (`proc.Session`, the

+ session the app was started under; a write into a purged database is

+ acknowledged into nowhere and is still that session's, seed 899 /

+ 3,000 under a database-based first cut); the push's mark, the legacy

+ writer (session 1) and every witness helper carry them.

+ `exemptDeclared(b, lost, holder, newGen, inv15)` applies a record

+ through `declaredBy`: box, incarnation, kind, and the record's session

+ and generation; the source-cut record goes through the same function

+ separately, and so does each record of `admissionRecord.LostMore`: behind

+ a declared-lost target the return's admission declares every session

+ the target was admitted into since the cut (`q.Box == op.Tgt &&

+ q.Session > op.CutSession`), certified or not (seed 33373 / 100,000:

+ the probe session certified and its writes, durable only in the lost

+ region, were hidden behind the record for the warm continuation). Rule `session-scoped-loss` (the mutation is rev 7.12's

+ match by box and incarnation); witness `wTwoSessionDeclaration`, a

+ constructed-state oracle test: two sessions of one box each

+ acknowledged an unuploaded write, a record for the second exempts only

+ its own, else INV-18.

+- **The probe deadline (R12-2).** In the app stage, `late` is computed

+ once per step from `openState.startedAt`; the attempt fails before the

+ start when the window has passed, whether the environment is ready

+ (`probe attempt failed: deadline before the start`) or not

+ (`environment`), and after a successful start whose readiness came at

+ or after the deadline the main process is stopped and the attempt

+ fails (`readiness after the deadline`; the model answers readiness in

+ the start's step, so this check is the belt to the first check's

+ braces). `box.lastProbe{startedAt, readyAt}` records the attempt;

+ `probeAccepted` is INV-19 at the four `probed` transitions (revert,

+ landing, restoring, push). Rule `probe-window` (the mutation makes no

+ deadline check at all); witness `wProbeWindowAt` (the target's

+ environment, by the knob `box.envUnreadyFor`, ready exactly 30 steps

+ after the first app stage; under the mutation the expired attempt is

+ accepted, INV-19); `TestProbeWindow` runs k = 29 (accepted, 29 steps),

+ 30 (failed before the start) and 31 (failed at the deadline, unready),

+ each followed by the retried admission and the run's end.

+- **The absent-marker mutant (R12 evidence).** Rule

+ `absent-marker-origin`: `deadGeneration` reads an absent

+ `generation.json` as the origin; the mutation reads it as agreement

+ with `holder.generation` (rev 7.11's sweep), with nothing else

+ changed. `wOriginSwept` moves to it from `baseline-live`, whose

+ mutation also queued the premature chore.

+- **The recovery limit (R12-5).** Nine: `probeTries*3` in

+ `probeAttemptFailed`, unchanged; §7.8's sentence corrected.

+- **Model faults found this round** (before the final numbers; the

+ 3,000-seed gate and the first 100,000-seed baseline found them): a

+ lost target's earlier, certified session went undeclared behind the

+ record for its last (seed 33373 / 100,000, above); a live predecessor

+ covered at a republished marker's publication was never retired once

+ superseded (seed 41914 / 100,000, above); the sim's legacy host

+ spawned its pre-release processes with no session, so their

+ acknowledgements escaped adoption's session-1 declaration under the

+ exact match (seed 44450 / 100,000: a fault of the sim's fixture, not

+ of the protocol); the console's lost-target release queued

+ the target region's park without covering (seed 1036: the third

+ composition site); acknowledgements took their session from the

+ database under the process, which a purge had removed (seed 899); the

+ `generation-conditional` witness started its second push while the

+ first push's publication chore still blocked operations in the region

+ (`obligations-block-ops`), since a prepared generation's predecessor

+ now gets its chore at the publication; the witness waits for the

+ obligations to clear.

**Rev 7.12: joint round 11 and claim rev 6.12.**

- **`holder.admissions` (claim rev 6.12).** `holder.Admissions

@@ -3412,7 +3737,8 @@ readiness, and same-operation lease identities.

`uncovered` reads `holder.admissions`.

- **The absent marker is the origin (R11-1).** `deadGeneration` reads a

missing `generation.json` as `""` before testing the chain, as

- `residueOf` always did; witness `wOriginSwept` (under `baseline-live`):

+ `residueOf` always did; witness `wOriginSwept` (under `baseline-live`

+ then; under `absent-marker-origin` since rev 7.13):

an adopted host's origin replica, a cold admission that crashes before

its first upload, the ordinary sweep for three horizons with no wake,

then the recovery; under the mutation the sweep parks the origin and

@@ -3942,6 +4268,48 @@ 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.13, on the final model (claim rev 6.14: regions on the record,

+the publication walk, `CoverRegionPredecessors` at whole-location parks,

+the declared identity, the probe deadline before the start): 30,000

+seeds, zero violations; 100,000 seeds, zero violations** (621 s and

+1906 s). Across the 100,000 seeds: 148,012 completed operations,

+among them 68,153 cold and 15,537 warm admissions

+(12,021 covered `sealed`, 757 covered

+`clean-return`; 1,123 predecessors left uncovered by a

+publication for their own region, 735 records covered at

+the commit's park, 267 at a rollback's release,

+3 at a lost-target release, 586 by the sweep,

+365 born covered under a pending park, 2

+predecessors live again at a publication and left uncovered, 26,793 holding

+nothing anywhere; 18,651 clean closes, 1,384 closes

+refused as uncertain, 0 stale certificates,

+970 wakes that waited for a draining writer, 52,025

+local databases purged, 4,124 starts that waited for a

+failed purge, 55,583 writes_lost records declaring

+8,001 acknowledged writes lost (181 of the records

+for a lost target's earlier sessions), 27,328 full first

+uploads, 106,044 start steps that waited for their marker,

+590 markers published again, 3,578 probes

+restarted, 474 probe attempts ended by their window, a

+late readiness or their fifth failure (438 of them refused

+before the start by the deadline check, 0 at a late

+readiness), 1,543 app starts that failed and were retried

+within their session, 0 hosts marked failed by the retry

+policy (serving wakes only), 93 seals whose source

+replica was short and 45 returns that carried the seal;

+9,360 final recovery admissions run by the oracle,

+0 unverified), 721 completed moves,

+2,000 clean and 91 dirty rollbacks,

+311 pre-flip reverts, 249 declared losses,

+24,340 pushes, 89,267 delete-park-free cycles and

+4,725 lost disks (3,423 with a crash);

+8,881 LTX compactions, 6,208 snapshot rotations,

+527 level-0 upload retries, 28,430 anchors;

+26,014 local stamp records lost and re-initialized;

+47,177 requests completed after `H`; 33,122 staging

+signatures refused as stale; 30,530 creates restarted on a

+412. Every oracle left the system unchanged.

**Rev 7.12, on the final model (claim rev 6.12: `holder.admissions`,

`Coverage`, `PublishGeneration`, the origin's absent marker, the final

recovery admission, a probe attempt's window): 30,000 seeds, zero

@@ -4252,34 +4620,62 @@ 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.12 model (af9b89ed), with the strict classification,

+on the final rev 7.13 model (42af7bfc), with the strict classification,

**in two ways**: the **random sweep**, 3,000 seeds each, 30,000 for every

rule not caught at 3,000 and for the new and the rare ones, 100,000 for

the rarest, 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 49 rules that have them. A rule is caught

+same mutation, for the 54 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 **96 rules**: rev 7.11's 95 plus

-`clean-return-identity` (claim rev 6.12, R11-4). `mutate.sh 3000` exited 0: no ERROR, no unexpected

+section does too. The model has **101 rules**: rev 7.12's 96 plus

+`foreign-region-uncovered` and `cover-at-park` (claim rev 6.14 items 5

+and 6, R12-3), `session-scoped-loss` (R12-1), `probe-window` (R12-2)

+and `absent-marker-origin` (R12's evidence note). `mutate.sh 3000` exited 0: no ERROR, no unexpected

MISSED, no STALE; every live combination was rerun this round. Seed

numbers reproduce any sweep line with `HOSTLIFE_SEED`;

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

-counts are in the rev 7.11 spec (ec982436). **Every table below is

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

+counts are in the rev 7.12 spec (dd3e35f6). **Every table below is

regenerated from the retained verdict files** (R9-6;

-`~/.cache/nearest-region/rev712-sweeps/`), none is carried over.

+`~/.cache/nearest-region/rev713-sweeps/`), none is carried over.

| | rules |

|---|---|

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

-| caught alone by the sweep at 30,000 (and by their witness, where one exists) | 10 (`dirty-return`, `evidence-whole-tree`, `hostguard`, `lost-return-park`, `markers-last`, `orphan-order`, `restore-overlap`, `seal-return`, `stale-hold-release`, `strict-spawn`) |

-| caught alone by the sweep at 100,000 (and by its witness, where one exists) | 2 (`baseline-live`, `declare-lost-compute`) |

-| caught alone by their witness only; the sweep misses them at 30,000 | 7 (`admit-before-start`, `close-evidence`, `close-waits`, `closed-marker`, `newest-l0`, `remote-baseline`, `restore-gap-closed`) |

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

+| caught alone by the sweep at 30,000 (and by their witness, where one exists) | 11 (`declare-lost-compute`, `evidence-whole-tree`, `hostguard`, `lost-quarantine`, `markers-last`, `orphan-order`, `restore-overlap`, `seal-by-version`, `seal-return`, `staging-quiet`, `stale-hold-release`) |

+| caught alone by the sweep at 100,000 (and by its witness, where one exists) | 0 (none this round: rev 7.12's two moved, `declare-lost-compute` to 30,000 and `baseline-live` to witness-only) |

+| caught alone by their witness only; the sweep misses them at 30,000 | 11 (`absent-marker-origin`, `admit-before-start`, `baseline-live`, `close-evidence`, `close-waits`, `closed-marker`, `newest-l0`, `probe-window`, `remote-baseline`, `restore-gap-closed`, `session-scoped-loss`) |

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

| subsumed: the witness holds under every combination tried, or the scenario is unreachable by construction | 2 (`door-reread`, `door-by-version`, by C3a and by writer epochs; historical results only, below). `start-check`, subsumed in rev 7.10, is caught alone by the sweep again since rev 7.11: with the whole check gone the lagging-marker reading is skipped and an empty generation is restored as if it held the data |

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

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

| unexercised | **0** |

+**What rev 7.13 moved.** The five new rules: `foreign-region-uncovered`

+2 / 3,000, 34 / 30,000 (a chore queued into the source's region

+from the target's publication parks the rollback's baseline),

+`cover-at-park` 34 / 3,000, 337 / 30,000 (a whole-location park that covers

+nothing leaves records uncovered, INV-17 as it completes),

+`session-scoped-loss` witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 (the random sweep cannot

+see an oracle-precision mutation: its witness constructs the two-session

+state), `probe-window` witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 (an attempt accepted after its

+window, INV-19) and `absent-marker-origin` witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000

+(`wOriginSwept`'s fault, isolated from `baseline-live`'s chore).

+`baseline-live` fell to witness-only (witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000; 2 / 100,000 on rev

+7.12: its mutation's premature chore no longer finds a baseline nobody

+else retires, now that every publication walks the uncovered records),

+and `declare-lost-compute` is caught at 30,000 this round (1 / 30,000;

+1 / 100,000 on rev 7.12). Caught alone: 88 of 101. The rules the

+coverage change touched: `writes-lost` 13 / 3,000, 110 / 30,000, 368 / 100,000,

+`clean-return-identity` 15 / 3,000, 112 / 30,000, 332 / 100,000, `seal-return`

+0 / 3,000, 8 / 30,000, 22 / 100,000, `dirty-return` 1 / 3,000, 9 / 30,000,

+`lost-return-park` 2 / 3,000, 27 / 30,000, 64 / 100,000, `obligations-block-ops`

+29 / 3,000 (a prepared generation's predecessor now

+gets its chore at the publication, so an obligation blocks the next

+operation for a horizon after every push), `recovery-current-inputs`

+33 / 3,000, `hostguard` 0 / 3,000, 2 / 30,000, 2 / 100,000,

+`stale-hold-release` 0 / 3,000, 14 / 30,000, 52 / 100,000, `strict-spawn`

+9 / 3,000, 110 / 30,000, 374 / 100,000.

**What rev 7.12 moved.** The new rule `clean-return-identity`

13 / 3,000, 125 / 30,000, 387 / 100,000 (a clean rollback after a probed target is a

schedule the sweep reaches; under the mutation the false predecessor is

@@ -4437,56 +4833,60 @@ witness to hold there; each witness violates with the failure it names.

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

-| `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 | | 1 / 3,000, 10 / 30,000, 42 / 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 | | 0 / 3,000, 29 / 30,000, 74 / 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 / 3,000, 0 / 30,000, 1 / 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 | | 1 / 3,000, 9 / 30,000, 36 / 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 | | 2 / 3,000, 27 / 30,000, 64 / 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 / 3,000, 1 / 30,000, 1 / 100,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 | | 1 / 3,000, 9 / 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 snapshot | | 1 / 3,000, 6 / 30,000 |

-| `dirty-return` (INV-2) | the target writes during its probe and replicates; the rollback is dirty and the return lane carries the write | **violated**: treated as clean with the source's replica covering the stop, the return is covered `clean-return`, nothing is declared and the serving database lacks the target's write (INV-2 local at the final recovery; rev 7.11 saw INV-15 at the declaration) | | 0 / 3,000, 11 / 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 snapshot | | 0 / 3,000, 5 / 30,000 |

+| `dirty-return` (INV-2) | the target writes during its probe and replicates; the rollback is dirty and the return lane carries the write | **violated**: treated as clean with the source's replica covering the stop, the return is covered `clean-return`, nothing is declared and the serving database lacks the target's write (INV-2 local at the final recovery; rev 7.11 saw INV-15 at the declaration) | | 1 / 3,000, 9 / 30,000 |

| `claim-cas-opid` (C2) | a stalled source goroutine with the rollback's last read resumes after a purge claimed the host | held | with `revalidate-before-effect`: **violated**, the store is torn down under a serving host | 0 / 3,000 |

| `exec-admission`, `hold-op-open`, `start-check-claim-gen`, `exec-writer` (J2-R2-8; claim rev 6.8.1) | a paused open from an earlier operation lands after the commit while the source's row is still held; a request wakes the source | held, each, and under every proper subset | all four: **violated**, INV-1 (the non-exec source is admitted cold into a fresh generation restored from its own region's old files and serves beside the target) | 0 / 3,000 |

| `start-check` (INV-4) | the same, dropping the whole start check | retired in rev 7.10: with every restore from the box's own region, the stale source finds nothing of the target's generation to restore and cannot start; subsumed (`expected-outcomes.txt`) | | 0 |

| `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 | with `fence-etag`: **violated**; with `purge-claim-fence`: **violated** | 0 / 3,000 |

-| `fence-by-installation` (claim rev 6.4 §6.4, R3-3) | UK→US, then US→UK; **unmutated, the instance must serve on UK again, running** | **violated**: the landing probe on UK is refused by the box's own installation record (INV-3) | | 342 / 3,000, 3,133 / 30,000 |

-| `fence-stamp` (claim rev 6.4 §6.4, R4-2) | a config-sync pass selects the row under the first installation and pauses; UK→US→UK; a new bundle is published; the pass takes the guard | held: the host guard's fresh re-validation refuses its stale bundle | with `hostguard`: **violated**, INV-6, a pass of a retired installation wrote host state | 337 / 3,000, 3,042 / 30,000 |

+| `fence-by-installation` (claim rev 6.4 §6.4, R3-3) | UK→US, then US→UK; **unmutated, the instance must serve on UK again, running** | **violated**: the landing probe on UK is refused by the box's own installation record (INV-3) | | 327 / 3,000, 2,978 / 30,000 |

+| `fence-stamp` (claim rev 6.4 §6.4, R4-2) | a config-sync pass selects the row under the first installation and pauses; UK→US→UK; a new bundle is published; the pass takes the guard | held: the host guard's fresh re-validation refuses its stale bundle | with `hostguard`: **violated**, INV-6, a pass of a retired installation wrote host state | 332 / 3,000, 2,946 / 30,000 |

| `orphan-order` (claim rev 6 §5.1 step 5, R3-2) | the recovery pass's cleanup pauses after its first observation; a create removes the orphan, claims and publishes; the paused cleanup resumes | **violated**: the record of the incarnation the claim names is deleted | | 0 / 3,000, 1 / 30,000 |

-| `sweep-namespace` (claim rev 6 §6.2a, R3-4) | a replication PUT of incarnation 1 completes after 33 recreates dropped it from `retired_incarnations` | **violated**: INV-10, residue the sweep never finds | | 541 / 3,000 |

-| `live-set-region` (claim rev 6.4 §6.2a, R4-3) | a legacy host serving in UK with an earlier replica in US; discovery parks US; an old US replication PUT lands after | **violated**: INV-10, residue the US sweep exempts by key alone | | 2 / 3,000, 16 / 30,000 |

-| `restore-overlap` (§5.1, R4-1) | a generation's snapshot ends at the push's TXID; the only continuation is a compacted file starting one below it; the disk is lost and the host wakes cold | **violated**: INV-3 since rev 7.10, the restore stops short of the certificate's `max_txid` and the box never starts (rev 7.4's `min == current + 1` discarded the file and lost four writes) | | 0 / 3,000, 2 / 30,000 |

+| `sweep-namespace` (claim rev 6 §6.2a, R3-4) | a replication PUT of incarnation 1 completes after 33 recreates dropped it from `retired_incarnations` | **violated**: INV-10, residue the sweep never finds | | 544 / 3,000 |

+| `live-set-region` (claim rev 6.4 §6.2a, R4-3) | a legacy host serving in UK with an earlier replica in US; discovery parks US; an old US replication PUT lands after | **violated**: INV-10, residue the US sweep exempts by key alone | | 1 / 3,000, 18 / 30,000 |

+| `restore-overlap` (§5.1, R4-1) | a generation's snapshot ends at the push's TXID; the only continuation is a compacted file starting one below it; the disk is lost and the host wakes cold | **violated**: INV-3 since rev 7.10, the restore stops short of the certificate's `max_txid` and the box never starts (rev 7.4's `min == current + 1` discarded the file and lost four writes) | | 0 / 3,000, 1 / 30,000 |

| `restore-gap-closed` (§5.1, R4-1) | the same generation with the next file missing and the one after current | **violated**: a restore across the gap returns a database short of the acknowledged writes | | witness; sweep 0 / 3,000, 0 / 30,000 |

-| `restore-anchor` (§5.1 step 7, R5-1) | a push installs a snapshot alone; the host wakes, writes three times, replicates, loses its disk and wakes cold | **violated**: INV-2, every write since the push is lost: replication restarted at TXID 1 below the snapshot and the planner skipped the files (facts R5-1a, b) | | 59 / 3,000, 593 / 30,000, 1,960 / 100,000 |

-| `root-advance` (§5.1 step 8, R5-3) | a push, then twelve replicated writes: four compactions, four snapshot rotations, retention expiring every file that continued from the pinned snapshot; the disk is lost | **violated**: INV-3, the host refuses to wake on a gap the retention made, while the newest snapshot holds every write (facts R5-3d, e) | | 12 / 3,000, 121 / 30,000, 434 / 100,000 |

-| `anchor-acked` (§5.1 step 7, R6-1) | a push installs a snapshot alone; the install's anchor PUT is held across forty attempted opens, then released; the host writes, replicates, loses its disk and wakes cold | **violated**: the host opened before its anchor was acknowledged; litestream's position would be 0 and the writes below the snapshot are lost on the cold restore (INV-2) | | 13 / 3,000, 104 / 30,000, 361 / 100,000 |

-| `return-stamp` (claim rev 6.5, R6-4) | a dirty rollback; the source's local stamp record is lost after the target's return; the return CAS writes the source installation's stamp back and the source re-initializes from it, installs under it and serves under its probe CAS's new stamp | **violated**: the source activates the target's stamp, issued for another box's installation (INV-6) | | 74 / 3,000, 773 / 30,000, 2,587 / 100,000 |

-| `recovery-generation` (claim rev 6.6 §6.4a, R7-1), three scenarios and a crash | writer A's upload `[N+1]` is held in flight, A dies with its disk, B wakes; (i) B replicates its own `[N+1]`, then A's lands; (ii) A's lands after B's position is initialized and before B's upload, so litestream's loop skips B's file; (iii) A's held write updated K, B durably updates K, A's lands; (iv) a clean stop drains, then the agent crashes before the certificate | **violated** in each: with the rule B recovers into a fresh generation and A's file lands in the dead one; without it B's acknowledged write is lost on the cold restore taken the moment A's file lands (INV-2), or no recovery runs after the crash (iv) | | 10 / 3,000, 105 / 30,000, 388 / 100,000 |

+| `restore-anchor` (§5.1 step 7, R5-1) | a push installs a snapshot alone; the host wakes, writes three times, replicates, loses its disk and wakes cold | **violated**: INV-2, every write since the push is lost: replication restarted at TXID 1 below the snapshot and the planner skipped the files (facts R5-1a, b) | | 50 / 3,000, 521 / 30,000, 1,740 / 100,000 |

+| `root-advance` (§5.1 step 8, R5-3) | a push, then twelve replicated writes: four compactions, four snapshot rotations, retention expiring every file that continued from the pinned snapshot; the disk is lost | **violated**: INV-3, the host refuses to wake on a gap the retention made, while the newest snapshot holds every write (facts R5-3d, e) | | 9 / 3,000, 122 / 30,000, 432 / 100,000 |

+| `anchor-acked` (§5.1 step 7, R6-1) | a push installs a snapshot alone; the install's anchor PUT is held across forty attempted opens, then released; the host writes, replicates, loses its disk and wakes cold | **violated**: the host opened before its anchor was acknowledged; litestream's position would be 0 and the writes below the snapshot are lost on the cold restore (INV-2) | | 12 / 3,000, 91 / 30,000, 334 / 100,000 |

+| `return-stamp` (claim rev 6.5, R6-4) | a dirty rollback; the source's local stamp record is lost after the target's return; the return CAS writes the source installation's stamp back and the source re-initializes from it, installs under it and serves under its probe CAS's new stamp | **violated**: the source activates the target's stamp, issued for another box's installation (INV-6) | | 69 / 3,000, 706 / 30,000, 2,339 / 100,000 |

+| `recovery-generation` (claim rev 6.6 §6.4a, R7-1), three scenarios and a crash | writer A's upload `[N+1]` is held in flight, A dies with its disk, B wakes; (i) B replicates its own `[N+1]`, then A's lands; (ii) A's lands after B's position is initialized and before B's upload, so litestream's loop skips B's file; (iii) A's held write updated K, B durably updates K, A's lands; (iv) a clean stop drains, then the agent crashes before the certificate | **violated** in each: with the rule B recovers into a fresh generation and A's file lands in the dead one; without it B's acknowledged write is lost on the cold restore taken the moment A's file lands (INV-2), or no recovery runs after the crash (iv) | | 10 / 3,000, 100 / 30,000, 354 / 100,000 |

| `closed-marker` (claim rev 6.6 §6.4a; a certificate since rev 7.9) | a stale certificate (`max_txid` behind the remote maximum) beside the dead writer's outstanding upload | **violated**: taken as intact, B continues in place and A's late file replaces B's (INV-2) | | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 |

| `close-waits` (claim rev 6.6 §6.4a) | a clean stop with an upload in flight | **violated**: written at once, the marker vouches for an upload that has not returned | | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 |

| `newest-l0` (§5.1 step 8, R7-3) | the local position runs ahead of the uploads across two compactions and snapshot rotations | **violated**: retention below the previous snapshot removes the newest uploaded level-0 file | | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 |

-| `build-completion` (§5.1 step 2, §7.6, R7-4) | a push's build with its snapshot, then its anchor, held, the agent crashing in between each | **violated**: `generation.json` published before its snapshot landed (INV-11) | | 704 / 3,000 |

-| `evidence-whole-tree` (§6.1, J-D3) | an adopted legacy host runs a descendant outside the cgroup; the move cuts | **violated**: evidence blind to the escapee certifies the stop and two boxes run the host (INV-1) | | 0 / 3,000, 7 / 30,000 |

-| `timer-freeze` (J-N14) | a registered timer on the source; the move holds the row; the runner's deliveries are refused; a clean rollback | **violated**: the refused deliveries advanced the runner's bookkeeping, the timer digest differs from the stop's, the source is `stuck` | | 2 / 3,000, 21 / 30,000 |

-| `writer-session` (claim rev 6.8 §6.4a, R8-1) | two sessions certify; the third dies with its disk and an upload in flight; the dead certificates still match the remote maximum | **violated**: the newest certificate readmits the box into the generation and the late upload replaces its file (INV-2) | | 2 / 3,000, 22 / 30,000, 63 / 100,000 |

-| `admit-everywhere` (claim rev 6.8 §6.4a, R8-2), two scenarios | (i) the committed move's target dies with its disk and an upload in flight before finalization; (ii) the landing's probe dies with its disk and an upload in flight in its settle window | **violated** in each: admitted for ordinary wakes alone, the target continues the generation and the late upload replaces its file (INV-2); the restarted probe reuses the install generation and the landing's restore loses its write | | 710 / 3,000, 6,840 / 30,000, 23,078 / 100,000 |

+| `build-completion` (§5.1 step 2, §7.6, R7-4) | a push's build with its snapshot, then its anchor, held, the agent crashing in between each | **violated**: `generation.json` published before its snapshot landed (INV-11) | | 707 / 3,000 |

+| `evidence-whole-tree` (§6.1, J-D3) | an adopted legacy host runs a descendant outside the cgroup; the move cuts | **violated**: evidence blind to the escapee certifies the stop and two boxes run the host (INV-1) | | 0 / 3,000, 5 / 30,000 |

+| `timer-freeze` (J-N14) | a registered timer on the source; the move holds the row; the runner's deliveries are refused; a clean rollback | **violated**: the refused deliveries advanced the runner's bookkeeping, the timer digest differs from the stop's, the source is `stuck` | | 3 / 3,000, 13 / 30,000 |

+| `writer-session` (claim rev 6.8 §6.4a, R8-1) | two sessions certify; the third dies with its disk and an upload in flight; the dead certificates still match the remote maximum | **violated**: the newest certificate readmits the box into the generation and the late upload replaces its file (INV-2) | | 4 / 3,000, 27 / 30,000, 77 / 100,000 |

+| `admit-everywhere` (claim rev 6.8 §6.4a, R8-2), two scenarios | (i) the committed move's target dies with its disk and an upload in flight before finalization; (ii) the landing's probe dies with its disk and an upload in flight in its settle window | **violated** in each: admitted for ordinary wakes alone, the target continues the generation and the late upload replaces its file (INV-2); the restarted probe reuses the install generation and the landing's restore loses its write | | 711 / 3,000, 6,844 / 30,000, 23,089 / 100,000 |

-| `valid-ltx` (R8-3) | a create's first wake into an empty generation (no LTX file), then a move of the never-written incarnation, whose seal is at position 0 | **violated**: the install writes `[1, 0]` and `[0, 0]`, which the encoder refuses (INV-12) | | 41 / 3,000, 391 / 30,000 |

+| `valid-ltx` (R8-3) | a create's first wake into an empty generation (no LTX file), then a move of the never-written incarnation, whose seal is at position 0 | **violated**: the install writes `[1, 0]` and `[0, 0]`, which the encoder refuses (INV-12) | | 39 / 3,000, 395 / 30,000 |

| `close-evidence` (claim rev 6.8 §6.4a, R8-5) | an upload is held past the client's timeout; the retry lands; the original stays outstanding; a clean stop | **violated**: the certificate is written while the original is unresolved | | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 |

| `close-evidence` (R9-5), two more scenarios | (i) a compaction's level-1 PUT is held past the client's timeout, the next pass retries and lands, the original completes afterwards; (ii) a snapshot PUT completes on the server after the client gave up on it | **violated** in each: the certificate is written while a request of the session was retried after a timeout, or its response was lost | | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 |

| `remote-baseline` (claim rev 6.9 §6.4a, R9-1) | a session closes cleanly through N+1; the box's local database is a cached copy through N; the next wake | **violated**: the stale copy is served without the acknowledged write, and its upload for N+1 is skipped at the remote position (INV-2) | | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 |

-| `writes-lost` (claim rev 6.9 §6.4a, R9-2) | a writer acknowledges a write and crashes before uploading it; the next wake is cold | **violated**: lost silently, the serving database differs from the acknowledged writes (INV-2); with the rule the admission records writes_lost and alerts | | 14 / 3,000, 125 / 30,000, 411 / 100,000 |

+| `writes-lost` (claim rev 6.9 §6.4a, R9-2) | a writer acknowledges a write and crashes before uploading it; the next wake is cold | **violated**: lost silently, the serving database differs from the acknowledged writes (INV-2); with the rule the admission records writes_lost and alerts | | 13 / 3,000, 110 / 30,000, 368 / 100,000 |

| `admit-bind-op` (claim rev 6.9 §6.4a, R9-4) | a wake's admission closure computed under serving resumes after a delete began that kept session, generation and executor | held: the model's general CAS condition on `op.id` (C2) refuses it too | with `claim-cas-opid`: **violated**, INV-13, a writer admitted into a host being deleted | 0; the pair 0 / 30,000, 0 / 100,000 |

| `admit-before-start` (claim rev 6.10 §6.4a, R10-1) | a background worker acknowledges a write right after the app starts; the box crashes before replication opens; admitted before the start, the acknowledgement is the session's and the next cold admission declares it | **violated**: under rev 6.8.2's order the acknowledgement is in a database the next warm admission purges silently (INV-2 local) | | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 |

-| `baseline-live` (claim rev 6.10 §6.4a, R10-2) | a cold admission into a fresh generation; the box crashes before the first upload; the predecessor's retirement runs out its quiet time; the recovery | **violated**: with the chore at the CAS the predecessor is parked and the recovery restores nothing (INV-2 local) | | 0 / 3,000, 0 / 30,000, 2 / 100,000 |

-| `clean-return-identity` (claim rev 6.12, R11-4) | a move's target is probed and writes nothing; the seal recorded `src_covered`; a clean rollback; the source's re-admission | held: the record's predecessor is the target's writer and its coverage `clean-return`; nothing is declared | **violated** under the mutation: INV-16, the record names the target's session and box with the source's generation, a writer that never was | 13 / 3,000, 125 / 30,000, 387 / 100,000 |

-| `baseline-live` (R11-1), a second scenario | an adopted host's origin replica with durable writes and no `generation.json`; a cold admission crashes before its first upload; the ordinary sweep runs for three horizons; the recovery | **violated**: the sweep parks the origin and the recovery restores nothing (INV-2 local) | | 0 / 3,000, 0 / 30,000, 2 / 100,000 |

-| `seal-return` (rev 7.11 §7.8) | the source's last upload is in flight when the cut stops it; the landing is rolled back after its build; the return must carry the seal | **violated**: treated as clean, the source's cold admission declares a write the landing's built generation holds (INV-15) | | 0 / 3,000, 12 / 30,000, 27 / 100,000 |

+| `baseline-live` (claim rev 6.10 §6.4a, R10-2) | a cold admission into a fresh generation; the box crashes before the first upload; the predecessor's retirement runs out its quiet time; the recovery | **violated**: with the chore at the CAS the predecessor is parked and the recovery restores nothing (INV-2 local) | | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 |

+| `clean-return-identity` (claim rev 6.12, R11-4) | a move's target is probed and writes nothing; the seal recorded `src_covered`; a clean rollback; the source's re-admission | held: the record's predecessor is the target's writer and its coverage `clean-return`; nothing is declared | **violated** under the mutation: INV-16, the record names the target's session and box with the source's generation, a writer that never was | 15 / 3,000, 112 / 30,000, 332 / 100,000 |

+| `absent-marker-origin` (R11-1; its own rule since rev 7.13) | an adopted host's origin replica with durable writes and no `generation.json`; a cold admission crashes before its first upload; the ordinary sweep runs for three horizons; the recovery | **violated**: the sweep, reading absence as agreement, parks the origin and the recovery restores nothing (INV-2 local) | | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 |

+| `session-scoped-loss` (R12-1) | two writer sessions of one box each acknowledged an unuploaded write; a `writes_lost` record for the second is applied (a constructed-state oracle test) | held: only the second session's write is exempted | **violated** under the mutation: INV-18, the record for session 2 exempted session 1's undeclared write | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 |

+| `foreign-region-uncovered` (claim rev 6.14 item 5, R12-3) | a probed landing whose target published; the chore's quiet time brought forward; the source region's runner works within the settle window; a clean rollback | held: no chore was queued into the source's region, the return restores the source's generation | **violated** under the mutation: the chore parked the rollback's baseline and the return restored an empty database (INV-2) | 2 / 3,000, 34 / 30,000 |

+| `cover-at-park` (claim rev 6.14 item 6, R12-3), three scenarios | (i) a committed move: the commit's CAS queues the source region's park; (ii) the record flips to committed and every actor pauses past the horizon before anyone follows it; (iii) `followRecord` is called again after the commit | held: in each the target's record is covered in the CAS that queued the park, one park is queued, the replay is refused | **violated** under the mutation: INV-17 as the source region's park completes, the target's record uncovered | 34 / 3,000, 337 / 30,000 |

+| `probe-window` (R12-2) | the landing probe's launch environment is ready exactly 30 steps after the attempt's first app stage | held: the attempt fails before the start, the next admission's probe is accepted | **violated** under the mutation: the expired attempt starts and is accepted (INV-19) | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 |

+| `seal-return` (rev 7.11 §7.8) | the source's last upload is in flight when the cut stops it; the landing is rolled back after its build; the return must carry the seal | **violated**: treated as clean, the source's cold admission declares a write the landing's built generation holds (INV-15) | | 0 / 3,000, 8 / 30,000, 22 / 100,000 |

| `close-evidence` (R10-7), two more scenarios | (i) a fresh generation's first upload is held past the client's timeout and its retry lands; (ii) a warm admission's anchor is held and its retry lands; then a clean stop | **violated** in each: the certificate is written while a request of the session was retried after a timeout | | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 |

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

@@ -4511,54 +4911,56 @@ combination** (R4 §3): each door rule's two-rule pair with C3a already

fails, so the three-rule row is a wider set and inherits no claim that its

proper subsets hold. It is no longer run.

-**Caught alone: 83 of 96** (64 by the sweep at 3,000; 10 by the sweep at

-30,000, marked †; 2 at 100,000,

-marked ††; 7 by their witness alone, marked ‡).

+**Caught alone: 88 of 101** (66 by the sweep at 3,000; 11 by the sweep at

+30,000, marked †; 0 at 100,000,

+marked ††; 11 by their witness alone, marked ‡).

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

-| `abort-target-owner` | 940 / 3,000 | | `admission-registration` | 32 / 3,000 |

-| `anchor-acked` | 13 / 3,000, 104 / 30,000, 361 / 100,000 | | `baseline-live` †† | 0 / 3,000, 0 / 30,000, 2 / 100,000 |

-| `build-completion` | 704 / 3,000 | | `cancelled-creates` | 383 / 3,000 |

-| `claim-never-deleted` | 4 / 3,000, 57 / 30,000 | | `claim-op-exclusive` | 82 / 3,000 |

-| `commit-before-open` | 2 / 3,000, 61 / 30,000 | | `cut-deadline` | 38 / 3,000 |

-| `declare-lost-compute` †† | 0 / 3,000, 0 / 30,000, 1 / 100,000 | | `dirty-return` † | 0 / 3,000, 11 / 30,000 |

-| `evidence-from-state` | 2,610 / 3,000 | | `evidence-whole-tree` † | 0 / 3,000, 7 / 30,000 |

-| `fence-by-installation` | 342 / 3,000, 3,133 / 30,000 | | `fence-etag` | 26 / 3,000, 229 / 30,000 |

-| `fence-stamp` | 337 / 3,000, 3,042 / 30,000 | | `files-carried` | 33 / 3,000 |

-| `floor-boot-recovery` | 2,576 / 3,000 | | `fresh-admission` | 10 / 3,000 |

-| `fresh-incarnation` | 42 / 3,000 | | `generation-conditional` | 1 / 3,000, 10 / 30,000, 42 / 100,000 |

-| `hostguard` † | 0 / 3,000, 2 / 30,000, 2 / 100,000 | | `legacy-discovery` | 273 / 3,000, 2,739 / 30,000 |

-| `live-set-region` | 2 / 3,000, 16 / 30,000 | | `location-per-incarnation` | 28 / 3,000, 359 / 30,000, 1,182 / 100,000 |

-| `lost-quarantine` | 1 / 3,000, 6 / 30,000 | | `lost-return-park` † | 0 / 3,000, 29 / 30,000, 74 / 100,000 |

-| `obligations-block-ops` | 31 / 3,000 | | `orphan-no-deadline` | 41 / 3,000 |

-| `orphan-order` † | 0 / 3,000, 1 / 30,000 | | `park-all-versions` | 568 / 3,000 |

-| `park-by-version` | 2,527 / 3,000 | | `park-skip-lock` | 2,728 / 3,000 |

-| `participant-rows` | 2 / 3,000 | | `purge-adopts` | 7 / 3,000 |

-| `purge-claim-fence` | 22 / 3,000, 232 / 30,000 | | `purge-journal` | 1,889 / 3,000 |

-| `purge-reserve-first` | 2,143 / 3,000 | | `quiet-before-ack` | 178 / 3,000 |

-| `recovery-current-inputs` | 40 / 3,000 | | `recovery-generation` | 10 / 3,000, 105 / 30,000, 388 / 100,000 |

-| `recovery-pass` | 2,482 / 3,000 | | `registration-recovery` | 2,118 / 3,000 |

-| `restore-overlap` † | 0 / 3,000, 2 / 30,000 | | `retirement-ids` | 463 / 3,000 |

-| `return-stamp` | 74 / 3,000, 773 / 30,000, 2,587 / 100,000 | | `revalidate-before-effect` | 17 / 3,000, 188 / 30,000 |

+| `admit-everywhere` | 711 / 3,000, 6,844 / 30,000, 23,089 / 100,000 | | `anchor-acked` | 12 / 3,000, 91 / 30,000, 334 / 100,000 |

+| `cancelled-creates` | 385 / 3,000 | | `claim-never-deleted` | 4 / 3,000, 57 / 30,000 |

+| `claim-op-exclusive` | 82 / 3,000 | | `clean-return-identity` | 15 / 3,000, 112 / 30,000, 332 / 100,000 |

+| `cover-at-park` | 34 / 3,000, 337 / 30,000 | | `cut-deadline` | 39 / 3,000 |

+| `declare-lost-compute` † | 0 / 3,000, 1 / 30,000, 1 / 100,000 | | `dirty-return` | 1 / 3,000, 9 / 30,000 |

+| `evidence-from-state` | 2,610 / 3,000 | | `evidence-whole-tree` † | 0 / 3,000, 5 / 30,000 |

+| `fence-by-installation` | 327 / 3,000, 2,978 / 30,000 | | `fence-etag` | 26 / 3,000, 226 / 30,000 |

+| `fence-stamp` | 332 / 3,000, 2,946 / 30,000 | | `files-carried` | 29 / 3,000 |

+| `floor-boot-recovery` | 2,577 / 3,000 | | `foreign-region-uncovered` | 2 / 3,000, 34 / 30,000 |

+| `fresh-admission` | 10 / 3,000 | | `fresh-incarnation` | 41 / 3,000 |

+| `generation-conditional` | 1 / 3,000, 9 / 30,000, 36 / 100,000 | | `hostguard` † | 0 / 3,000, 2 / 30,000, 2 / 100,000 |

+| `legacy-discovery` | 367 / 3,000, 3,561 / 30,000 | | `live-set-region` | 1 / 3,000, 18 / 30,000 |

+| `location-per-incarnation` | 28 / 3,000, 358 / 30,000, 1,185 / 100,000 | | `lost-quarantine` † | 0 / 3,000, 5 / 30,000 |

+| `lost-return-park` | 2 / 3,000, 27 / 30,000, 64 / 100,000 | | `markers-last` † | 0 / 3,000, 4 / 30,000 |

+| `orphan-no-deadline` | 41 / 3,000 | | `orphan-order` † | 0 / 3,000, 1 / 30,000 |

+| `park-all-versions` | 564 / 3,000 | | `park-by-version` | 2,527 / 3,000 |

+| `park-skip-lock` | 2,728 / 3,000 | | `participant-rows` | 4 / 3,000 |

+| `purge-claim-fence` | 23 / 3,000, 235 / 30,000 | | `purge-journal` | 1,888 / 3,000 |

+| `purge-reserve-first` | 2,125 / 3,000 | | `quiet-before-ack` | 180 / 3,000 |

+| `recovery-current-inputs` | 33 / 3,000 | | `recovery-generation` | 10 / 3,000, 100 / 30,000, 354 / 100,000 |

+| `recovery-pass` | 2,473 / 3,000 | | `registration-recovery` | 2,114 / 3,000 |

+| `restore-overlap` † | 0 / 3,000, 1 / 30,000 | | `retirement-ids` | 426 / 3,000 |

+| `return-stamp` | 69 / 3,000, 706 / 30,000, 2,339 / 100,000 | | `revalidate-before-effect` | 15 / 3,000, 178 / 30,000 |

| `revert-journal` | 12 / 3,000 | | `rollback-journal` | 1 / 3,000, 9 / 30,000 |

-| `root-advance` | 12 / 3,000, 121 / 30,000, 434 / 100,000 | | `sdk-no-resign` | 9 / 3,000 |

-| `seal-by-version` | 1 / 3,000, 6 / 30,000 | | `seal-return` † | 0 / 3,000, 12 / 30,000, 27 / 100,000 |

-| `sign-at-check` | 10 / 3,000 | | `sign-before-safeuntil` | 17 / 3,000 |

-| `source-readiness` | 10 / 3,000 | | `staging-quiet` | 1 / 3,000, 2 / 30,000 |

-| `stale-hold-release` † | 0 / 3,000, 14 / 30,000, 47 / 100,000 | | `start-check` | 16 / 3,000, 218 / 30,000 |

-| `start-check-claim-gen` | 15 / 3,000, 181 / 30,000 | | `straggler-sweep` | 774 / 3,000 |

-| `strict-spawn` † | 0 / 3,000, 1 / 30,000, 11 / 100,000 | | `sweep-namespace` | 541 / 3,000 |

-| `sweep-staging` | 34 / 3,000 | | `target-park` | 18 / 3,000 |

-| `timer-canonical` | 3 / 3,000 | | `timer-freeze` | 2 / 3,000, 21 / 30,000 |

-| `valid-ltx` | 41 / 3,000, 391 / 30,000 | | `writer-session` | 2 / 3,000, 22 / 30,000, 63 / 100,000 |

-| `writes-lost` | 14 / 3,000, 125 / 30,000, 411 / 100,000 | | | |

+| `root-advance` | 9 / 3,000, 122 / 30,000, 432 / 100,000 | | `sdk-no-resign` | 10 / 3,000 |

+| `seal-by-version` † | 0 / 3,000, 5 / 30,000 | | `seal-return` † | 0 / 3,000, 8 / 30,000, 22 / 100,000 |

+| `sign-before-safeuntil` | 20 / 3,000 | | `source-readiness` | 10 / 3,000 |

+| `staging-quiet` † | 0 / 3,000, 1 / 30,000 | | `stale-hold-release` † | 0 / 3,000, 14 / 30,000, 52 / 100,000 |

+| `start-check` | 17 / 3,000, 214 / 30,000 | | `start-check-claim-gen` | 14 / 3,000, 167 / 30,000 |

+| `straggler-sweep` | 783 / 3,000 | | `strict-spawn` | 9 / 3,000, 110 / 30,000, 374 / 100,000 |

+| `sweep-namespace` | 544 / 3,000 | | `sweep-staging` | 32 / 3,000 |

+| `target-park` | 17 / 3,000 | | `timer-canonical` | 2 / 3,000 |

+| `timer-freeze` | 3 / 3,000, 13 / 30,000 | | `valid-ltx` | 39 / 3,000, 395 / 30,000 |

+| `writer-session` | 4 / 3,000, 27 / 30,000, 77 / 100,000 | | `writes-lost` | 13 / 3,000, 110 / 30,000, 368 / 100,000 |

**Caught only in a combination: 9 rules**, every live combination rerun this

round; `admit-bind-op` joins with `claim-cas-opid` (R9-4); the `start-check`

@@ -4573,19 +4975,19 @@ subset in the gate.

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

-| `purge-claim-fence` + `fence-etag` (**the re-read alone**, rev 7's CC21 as proposed) | 340 / 30,000 | `purge-claim-fence` 22 / 3,000, 232 / 30,000, `fence-etag` 26 / 3,000, 229 / 30,000 | (the two `registration-check` rows below) | a store destroyed under a creating or serving host |

-| `exec-admission` + `hold-op-open` + `start-check-claim-gen` + `exec-writer` | 183 / 30,000, 644 / 100,000 | `exec-admission` 0 / 3,000, `hold-op-open` 0 / 3,000, `start-check-claim-gen` 15 / 3,000, 181 / 30,000, `exec-writer` 0 / 3,000, 0 / 30,000 | violated, INV-1 | the non-exec source admitted cold beside the target, Astra's J2-R2-8 trace under writer sessions |

+| `purge-claim-fence` + `fence-etag` (**the re-read alone**, rev 7's CC21 as proposed) | 342 / 30,000 | `purge-claim-fence` 23 / 3,000, 235 / 30,000, `fence-etag` 26 / 3,000, 226 / 30,000 | (the two `registration-check` rows below) | a store destroyed under a creating or serving host |

+| `exec-admission` + `hold-op-open` + `start-check-claim-gen` + `exec-writer` | 166 / 30,000, 574 / 100,000 | `exec-admission` 0 / 3,000, `hold-op-open` 0 / 3,000, `start-check-claim-gen` 14 / 3,000, 167 / 30,000, `exec-writer` 0 / 3,000, 0 / 30,000 | violated, INV-1 | the non-exec source admitted cold beside the target, Astra's J2-R2-8 trace under writer sessions |

| `exec-admission` + `hold-op-open` + `start-check` + `exec-writer` (**historical**, rev 7.9: 7 / 30,000, violated INV-6) | not rerun: the `start-check` witness is retired, subsumed by regional restores | | retired | the stale source cannot restore the target's generation from its own region |

| `admit-bind-op` + `claim-cas-opid` | 0 / 30,000, 0 / 100,000 | `admit-bind-op` 0 / 3,000, 0 / 30,000, `claim-cas-opid` 0 / 3,000 | violated, INV-13 | a stale serving-time closure admits a writer into a host being deleted |

| `door-reread` + `location-per-incarnation` (**historical**, rev 7.7: 432 / 30,000, 196 door violations, witness violated) | not rerun: the witness is retired and the rule is subsumed | `location-per-incarnation` 28 / 3,000, 360 / 30,000, 1,179 / 100,000 this round (rev 7.10's row said 336 / 30,000 against its own result of 357, R10-9) | retired | under writer epochs the pair adds nothing the partner's own count does not show; no current witness evidence is claimed |

| `door-by-version` + `location-per-incarnation` (**historical**, rev 7.7: 385 / 30,000, 60 door violations, witness violated with C3a alone) | not rerun: the witness is retired and the rule is subsumed | `location-per-incarnation` 28 / 3,000, 360 / 30,000, 1,179 / 100,000 this round | retired | the same |

-| `fence-stamp` + `hostguard` (no longer combination-only) | 3,994 / 30,000 | `fence-stamp` 337 / 3,000, 3,042 / 30,000, `hostguard` 0 / 3,000, 2 / 30,000, 2 / 100,000 | violated | a stale pass writes host state for a retired installation (INV-6); the witness is what shows the stamp load-bearing against the guard's own check |

+| `fence-stamp` + `hostguard` (no longer combination-only) | 3,877 / 30,000 | `fence-stamp` 332 / 3,000, 2,946 / 30,000, `hostguard` 0 / 3,000, 2 / 30,000, 2 / 100,000 | violated | a stale pass writes host state for a retired installation (INV-6); the witness is what shows the stamp load-bearing against the guard's own check |

Every live combination was rerun on the rev 7.9 model; the gate runs

every proper subset of the admission four with the witness, which holds

@@ -5005,6 +5407,50 @@ although the seal carries every write; the admitted writer's start

agent loop; and the model's C2 already binds every CAS to `op.id`, so

the `admit-bind-op` witness needs both rules off.

+**Claim rev 6.13 (b3825827) and 6.14 (dc146058), after joint round 12:

+no change requested, seven notes.** Rev 6.13 adopted rev 7.12's five

+notes (the lost-target return is `""`; a probe never marks the host

+failed; chore ids are opaque; `clean-return` speaks for two sessions;

+coverage is per region, with `region` and `predecessor_region` on the

+record, the publication walk and `CoverRegionPredecessors`). Rev 6.14

+answers R12-4 and R12-6: §6.4a has one operative subsection, the retry

+limit is a serving wake's, retention is conservative with no compaction.

+Rev 7.13 encodes all of it (§5.1 step 9, §7.7, §7.8, §7.14's operative

+list, §14.2.2). Notes for platform-1e (`moves-claim-questions.md`, rev

+7.13 heading): **(1)** item 6 names the committed move's source cleanup;

+the model composes `CoverRegionPredecessors` into **three** CASes, the

+commit's, the target's release and the console's lost-target release,

+since the last two queue the target region's whole-location park and a

+restarted probe's record names the dead probe's generation there (seed

+1036 / 3,000); **(2)** a rollback's return admission comes after the

+release queued the target region's park, so no `CoverRegionPredecessors`

+can see its record: the model reads such a record as **born covered**

+(the admitting CAS finds the park already queued for its predecessor's

+region), which keeps INV-17 as the park completes; the claim should say

+so, or have the park's acknowledgement CAS cover too; **(3)** the at-rest

+sweep retires a region's dead generations wholesale: the model covers

+the records whose predecessors it parks in the CASes that queue and

+acknowledge its `park-sweep`; **(4)** item 1's "a warm admission keeps

+its predecessor's region" is read as the admitted box's region, where

+the warm writer's generation keeps its objects: a clean return's warm

+re-admission is on the source, in the source's region, while the last

+record is the target's; **(5)** the probe attempt's deadline is checked

+before each start and before readiness is accepted (R12-2), and a

+recovery probe's budget is nine attempts, three times a landing's

+(R12-5), if the claim wants either stated; **(6)** item 5's first

+bullet, "predecessor is the active generation: covered, no chore", is

+read as **left uncovered**, no chore: the generation is live, its

+retirement comes with the publication that supersedes it, and a record

+covered now would leave it unretired then, since the superseding

+admission's predecessor is the last record rather than the generation it

+restored from (seed 41914 / 100,000: a republished lagging marker covered

+the target's record while the source's generation was live again, and

+the generation was residue); **(7)** item 2's lost-target return

+records `writes_lost` for **every** session the target was admitted into

+since the cut, certified or not, not only the last (seed 33373 /

+100,000: a probe session that certified left its writes in the lost

+region, and the record for the warm continuation did not name them).

**Claim rev 6.11 (63255a3c) and 6.12 (b202ea4e), after joint round 11:

no change requested, three notes.** Rev 6.11 answered rev 7.11's eight

notes (the retry limit confirmed; the chain generalized to a run of

@@ -5454,6 +5900,24 @@ answers the rest and reruns every number.

| R6-5 (P3) replayed anchor bytes differ (the encoder's `time.Now()`) | the encoding inputs, timestamp included, are journaled in the install manifest before the PUTs and a replay reuses a current object (§5.1 step 2, §7.6 `building`); `TestFact_R6_5_AnchorReplayBytes` shows identical bytes for identical inputs and different bytes one millisecond apart |

| fidelity: compaction deleted the newest level-0 file, creating anchor-required cold restores the library would not | compaction keeps the newest input (§14.2.2); time-based level-0 retention stays deferred (§14.2.6) |

+### 22.19 Joint round 12 (claim b3825827, moves rev 7.12 dd3e35f6, model af9b89ed, library E 47426cc1)

+Round 12 found no P1 and judged E merge-ready on static review; it held

+A, B and C on four P2s and a P3, adopted note 5's discharge, and asked

+for an isolated absent-marker mutant. Claim rev 6.14 (dc146058) answers

+R12-4 and R12-6; E is unchanged at 47426cc1.

+| finding | rev 7.13 |

+|---|---|

+| R12-3 (P2) B and C did not encode `region` and `predecessor_region`, the per-region walk or `CoverRegionPredecessors`; C skipped publication for prepared admissions | the record carries both regions; `PublishGeneration` is the 6.14 walk and every cold admission publishes; `CoverRegionPredecessors` inside the commit's, the release's and the lost-target release's park CAS; born covered under a pending park and the sweep's own coverage as readings; INV-17 as a whole-location park completes; rules `foreign-region-uncovered` and `cover-at-park`; witnesses for the rollback baseline, the commit, its interruption and its replay (§5.1 step 9, §7.8, §7.14, §14.2.2) |

+| R12-1 (P2) a `writes_lost` record for one session exempted another session's acknowledgements | acknowledgements carry the writer session and generation of the process that gave them; `declaredBy` matches the declared identity; the source-cut record is applied separately; rule `session-scoped-loss`, witness `wTwoSessionDeclaration` (INV-18). The exact match exposed a lost target's earlier certified session going undeclared (seed 33373 / 100,000): every target session since the cut is declared now |

+| R12-2 (P2) a successful start after the attempt's window bypassed the deadline | checked before each start and before readiness is accepted; INV-19 at every probe acceptance; rule `probe-window`, witness `wProbeWindowAt`, `TestProbeWindow` at k = 29, 30, 31 (§7.7, §7.14) |

+| R12-4 (P2) B's operative text contradicted itself: "generation changes only after install and probe", the dirty-return region row, failed-host marking for probes | one operative list in §7.14 mirroring claim rev 6.14's; the restore contract names the cold admission; the dirty-return rows name the target's last admission until the source's probe is admitted; the start table marks a host failed for serving wakes only; superseded text marked history |

+| R12-5 (P3) the recovery limit: three in §7.8, nine in the model | nine, stated in §7.7 and §7.8; the model unchanged |

+| R12-6 (P3, E) the eight-covered-record bound was not enforced as compaction | documented as conservative retention in A and B; the model trims from the front only, never past an uncovered record |

+| evidence: `wOriginSwept` did not isolate the absent-marker defect | rule `absent-marker-origin` with the single mutation; the witness moves to it |

+| E verdict | round 12: MERGE-READY, no numbered blockers; the clean joint round is Paul's gate |

### 22.18 Joint round 11 (claim 3f916b05, moves rev 7.11 ec982436, model bd1587a1, library E 090fb7a2)

Round 11 judged the admitting order sound and R10-1, R10-5, R10-7, R10-8