carlos / platform Public

spec: move-any-app rev 7.17, joint round 16, claim rev 6.24 and 6.25

R16-2: a park executes strictly within its scope; the sweep groups
residue by location and archive incarnation, INV-23 checks membership
for every manifest source, the delete parks only holder.location plus
moves/<host> (claim rev 6.25 §5.2); "mirrors it exactly" withdrawn.
R16-3: the legacy identity is session 0 with generation "" (@root),
valid in both loss fields; INV-24; a created incarnation's first
admission declares nothing (an E bug, fixed on main 67547f5). R16-1:
sealed staging beside a legacy instance park. Born-covered narrowed.
The sweep's wider protection disclosed. Four notes answered by rev 6.25.

Model b9e97783: 107 rules, 73 witnesses. Evidence under the policy: the
gate; the 30,000-seed baseline (clean, 45,047 operations, 84 s, niced,
no load gate at Paul's word); one 3,000-seed sweep serially at
HOSTLIFE_PAR=2 under nice (93 caught, 14 expected misses, exit 0); 93 of
107 caught alone. Records in ~/.cache/nearest-region/rev717-sweeps/.

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

claude 2 weeks ago 39904c84ffdbc6d76da7f063aa1ce3625221d3f6 parent b9e9778

1 file changed, +299 −76

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

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 7ab94241b..318a24138 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,44 @@

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

**Date:** 2026-10-06

-**Revision:** 7.16.

+**Revision:** 7.17.

+- **Rev 7.17** answers **joint round 16** (`CODEX-FINDINGS-JOINT-R16.md`,

+ cited "R16-n") and is written against **claim spec rev 6.24**

+ (0b821896: the legacy identity, scope namespaces, the narrowed

+ born-covered) **and rev 6.25** (413b12cb, which answers this

+ revision's four notes: §5.2 now has a delete park only

+ `holder.location` plus `moves/<host>`, never the whole host prefix,

+ as the model does); the code the model aligns with is **main at

+ 67547f5**, which carries platform-1e's R16-1 and R16-3 fixes

+ (c7e595b, "park, hostclaim: scopes stay in their own namespace; the

+ legacy session-0 loss identity") and the first-admission fix (a

+ created incarnation's first admission declares nothing; note 2 was

+ an E bug); §22.23 has every disposition. **A park executes

+ strictly within its scope** (R16-2): the model's sweep groups residue

+ by the location it belongs to, an incarnation's own, the legacy

+ `instances/<host>` (never a child incarnation) or `moves/<host>`, and

+ queues one chore per location with that scope and its archive

+ incarnation; the archive names the incarnation; every scoped chore's

+ listing is confined to its scope and INV-23 checks every key a chore

+ would archive for membership, not only the location's syntax; the

+ delete parks the deleted incarnation's own location and the staging

+ namespace, never the whole host prefix. **The legacy identity is

+ session 0** (R16-3): an adopted host's pre-claim writer is `{session:

+ 0, generation: "" (@root), box: holder.writer_box}`, valid in both

+ `writes_lost` and `additional_writes_lost`; every other declaration

+ has a session above 0, and a declaration always names a box, so a

+ created incarnation's first admission, whose predecessor has no

+ writer, declares nothing (INV-24); the model no longer gives adoption

+ session 1; `TestLegacyLostTargetReturn` walks adopt → a move with

+ `src_covered` false → a cold target admission → the target declared

+ lost → the return declaring the target's session and the source's cut

+ session 0. **An instance park never touches staging** (R16-1):

+ `TestStagingSurvivesLegacyPark`. **Born covered, narrowed** (6.24 item

+ 5): only an unscoped `park-replica` or a park scoped exactly to

+ `holder.location`. Rule `scope-membership` (107 in all); witness

+ `wSweepScopeMembership` (73 in all). Evidence under the policy of

+ §14.2.1: the gate, the 30,000-seed baseline, one 3,000-seed sweep.

- **Rev 7.16** answers **joint round 15** (`CODEX-FINDINGS-JOINT-R15.md`,

cited "R15-1") and is written against **claim spec rev 6.23**

@@ -1427,18 +1464,30 @@ 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, completely** (claim rev 6.22 item 5,

+ behind (R10-5, R11-3). **That writer is the legacy identity**

+ (claim rev 6.24, R16-3): `{session: 0, generation: "" (read as

+ @root), box: holder.writer_box}`, adoption's `holder.session` being

+ 0; it is valid in both `writes_lost` and `additional_writes_lost`

+ (a lost-target return after a move cut at session 0 declares it

+ there), every other declaration has a session above 0, and a

+ declaration always names a box: a created incarnation's first

+ admission, whose predecessor has no writer (`holder.writer_box`

+ empty), declares nothing (INV-24; rev 7.13 to 7.16 gave adoption

+ session 1 and declared a boxless record for a created

+ incarnation's first admission). **Coverage, completely** (claim rev 6.22 item 5,

R13-2): a record is covered when its predecessor's retirement is in

hand in the region that holds the predecessor's objects, and an

entry becomes covered in **exactly four ways**, no other transition

covers anything: **at birth**, a warm entry (its predecessor is its

own generation, which nothing retires; the next cold admission's

record names it and queues the chore), or an entry admitted while

- the claim already holds a whole-location park of its

- `predecessor_region` (that park retires the predecessor: a

- rollback's return admitted after the release queued the target

- region's park, which the CAS that queued it could not see; seed

- 1036 / 3,000); **by publication**, above; **by

+ the claim already holds a park of the whole location in its

+ `predecessor_region`: an unscoped `park-replica`, or a park scoped

+ **exactly to `holder.location`**; a scoped park of an old

+ incarnation or of a staging prefix does not count (claim rev 6.24

+ item 5; that park retires the predecessor: a rollback's return

+ admitted after the release queued the target region's park, which

+ the CAS that queued it could not see; seed 1036 / 3,000); **by publication**, above; **by

`CoverRegionPredecessors(op, phase, region)`** in one of the three

CASes that queue a whole-location park of `region`, every uncovered

entry whose `predecessor_region` is `region`: the commit's

@@ -2102,7 +2151,27 @@ error; a child prefix of 64 hex characters is an incarnation location,

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

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

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

-other than `holder.generation` is residue. **The live set is

+other than `holder.generation` is residue. **What it finds is grouped by

+the location it belongs to** (claim rev 6.24 §2, R16-2): each

+incarnation location its own, the legacy `instances/<host>` (a level

+directory or generation directly under the host prefix, never a child

+incarnation), `moves/<host>` for staging residue; **one chore per

+location**, scoped to that location with its archive incarnation (the

+location's own; the holder's for the legacy location or the staging

+sweep; the newest retired on a free host), and the archive is written

+under that incarnation. **A park executes strictly within its scope**:

+its listing is confined to the scope's namespace (an `instances/…`

+scope never lists or parks anything under `moves/`, the legacy

+`instances/<host>` scope excludes child incarnations, a staging lane's

+scope only its own lane), and every key a chore would archive must be a

+member of its scope (the model's INV-23 checks membership on the

+manifest's sources, not only the location's syntax; rev 7.16 scoped the

+whole `instances/<host>/` listing as `instances/<host>` under the

+serving incarnation and archived a deleted incarnation's late object

+from there; witness `wSweepScopeMembership`). The same confinement

+governs a delete's parks, which cover the deleted incarnation's own

+location and the staging namespace, never the whole host prefix (claim

+rev 6.25 §5.2); an older incarnation's residue is this sweep's. **The live set is

region-qualified** (claim rev 6.5 §6.2a, R4-3): `{authoritative region,

holder.location, holder.generation}` plus the versions §5.1 names for the

generation, the snapshot version `generation.json` names included, is

@@ -2869,7 +2938,11 @@ this text wins.

false, under its persisted `cut.session`): `writes_lost` (one) plus

`additional_writes_lost` (a list), each `{box, generation, session,

remote_max_txid}`, unique by `(box, session)` across both, one alert

- per declaration (R13-3, R14-2; INV-21). A `writes_lost` record

+ per declaration (R13-3, R14-2; INV-21). The legacy identity `{session

+ 0, generation "" (@root), holder.writer_box}` is valid in both; every

+ other declaration has a session above 0, and every declaration names

+ a box, so a predecessor with no writer is not declared (INV-24, claim

+ rev 6.24, R16-3). 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

@@ -2887,7 +2960,8 @@ this text wins.

`holder.session` alone.

5. **Coverage, completely.** An entry becomes covered in exactly four

ways (R13-2): at birth (a warm entry; an entry admitted while the

- claim holds a whole-location park of its predecessor's region); by

+ claim holds an unscoped `park-replica`, or a park scoped exactly to

+ `holder.location`, in its predecessor's region, claim rev 6.24); by

publication; by `CoverRegionPredecessors` (item 6); by

`CoverParkedPredecessors` (item 6). **Publication:** after the marker

names the generation, one `PublishGeneration(observedOpID,

@@ -2932,7 +3006,12 @@ this text wins.

bound (a staging lane's is its seal bound, the seal plus the lease),

never the cleanup's start; every retry uses it; every acknowledgement,

a staging lane's included, waits a listing later than `evidence_at +

- H`, `H` the signature-age limit plus `request_limit`.

+ H`, `H` the signature-age limit plus `request_limit`. A park executes

+ strictly within its scope's namespace (claim rev 6.24 §2, R16-1,

+ R16-2): the sweep's chores are grouped by location, each with its

+ archive incarnation; an `instances/…` scope never touches `moves/`

+ and the legacy `instances/<host>` scope excludes child incarnations;

+ INV-23 checks membership for every key a chore archives.

A free host's at-rest sweep is a holderless `parking` op with

`intent.park_sweep`, no exec and no holder, which blocks the successor

create until `FreeAfterPark` frees the claim in its last

@@ -3338,8 +3417,10 @@ but produced no witness output as an ERROR, never as "none" (R3-6).

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

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

`TestInterruptedCleanReturn`, the run walk across regions (§5.1 step 9,

-rev 7.14), and `TestJoinHolderlessSweep`, two regions' residue under one

-holderless op (§6.4, rev 7.15).

+rev 7.14), `TestJoinHolderlessSweep`, two regions' residue under one

+holderless op (§6.4, rev 7.15), `TestLegacyLostTargetReturn`, the legacy

+identity through a lost-target return, and `TestStagingSurvivesLegacyPark`,

+sealed staging beside a legacy instance park (rev 7.17).

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

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

@@ -3865,6 +3946,55 @@ 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.17: joint round 16 and claim rev 6.24.**

+- **Scope membership (R16-2).** `scopeOf(k)` is the scope location a

+ key belongs to (`moves/<host>` for staging; an incarnation location;

+ the legacy `instances/<host>` for a level directory or generation

+ directly under the host prefix) and `inScope(k, loc)` its membership

+ (a staging lane's scope by its own prefix). `sweep()` groups the

+ sweepable keys by `scopeOf` and queues one `park-sweep` per location,

+ scoped with `incOf(claim, loc)` (the location's own incarnation; the

+ holder's for the legacy location or the staging sweep; the newest

+ retired on a free host); `Dest()` for a scoped sweep is

+ `parked/sweep/<host>/<incarnation>/<ob id>/`. The runner confines

+ every scoped chore's listing to its scope (`keep` composes

+ `!inScope`), and INV-23 checks each key a chore would archive for

+ membership before the park step. `parkingObligations` (the delete)

+ parks `holder.location` and `moves/<host>/`, not the whole host prefix.

+ Rule `scope-membership` (the mutation is rev 7.16's whole-prefix

+ grouping and listing); witness `wSweepScopeMembership`: incarnation 1

+ deleted, incarnation 2 serving, a late object under

+ `instances/<host>/1/g-old/`; the chore that parks it is scoped to

+ `instances/<host>/1` with incarnation 1; under the mutation INV-23

+ fires on the delete's `instances/<host>` park archiving a child

+ incarnation's object.

+- **The legacy identity (R16-3).** `adopt()` writes `Session: 0` (the

+ stamp stays 1); the sim's and the witnesses' pre-release processes,

+ acknowledgements and certificate fixtures carry session 0; INV-24 in

+ `admitCommit`: every declaration names a box, and session 0 comes only

+ with generation `""`; a created incarnation's first admission, whose

+ predecessor is `{session 0, box -1}`, records no `writes_lost`

+ (`admission: no predecessor writer, nothing declared`; rev 7.16

+ recorded a boxless one). `TestLegacyLostTargetReturn`: adopt, the

+ pre-claim writer's last write held off the replica, a move cut at

+ session 0 with `src_covered` false, the target admitted cold and

+ declared lost, the return's record declaring `{target, probe session}`

+ and `{source, session 0}` once each.

+- **Staging beside a legacy park (R16-1).** `TestStagingSurvivesLegacyPark`:

+ a legacy host whose earlier stay left a replica in the target region;

+ the landing's install park, scoped to the legacy instance location,

+ leaves the sealed `moves/<host>/<move>/db` and `files` current and the

+ landing is probed.

+- **Born covered, narrowed (claim rev 6.24 item 5).** `admitCommit`

+ counts an unscoped `park-replica`, or a `park-superseded` of

+ `holder.location` whose scope, if any, is exactly that location.

+- **Disclosed difference (the sweep's walk).** `deadGeneration` protects

+ every generation of an unfinished run in the authoritative region

+ without the run walk's region or coverage filtering, which main

+ applies when it selects a baseline; the sweep's protection is the

+ wider, conservative set (§14.2.6).

**Rev 7.16: joint round 15 and claim rev 6.23.**

- **The scope on every chore, from its queuing CAS (R15-1).**

@@ -4685,6 +4815,24 @@ 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.17, on the final model (joint round 16, claim rev 6.24: scope

+membership, the legacy identity, the narrowed born-covered): 30,000

+seeds, zero violations** (84 s; no 100,000-seed run under the

+evidence policy of §14.2.1). Across the 30,000 seeds: 45,047

+completed operations, 20,484 cold and 4,803 warm admissions,

+8,051 first admissions with no predecessor writer and nothing

+declared, 3,320 declarations of the legacy identity (session 0),

+11,878 holderless sweeps, 1 regions joining a

+running one, 11,878 `FreeAfterPark` transitions,

+148,792 scopes bound before a chore's first step, 8,678

+writes_lost records declaring 2,409 writes (72

+for a lost target's other sessions, 8 for the source's cut

+session), 225 completed moves, 621 clean and

+24 dirty rollbacks, 97 reverts, 74

+declared losses, 7,327 pushes, 27,194 delete-park-free

+cycles, 2,745 final recovery admissions (0

+unverified). Every oracle left the system unchanged.

**Rev 7.16, on the final model (joint round 15, claim rev 6.23: the park

scope on every chore from its queuing CAS, one deadline): 30,000 seeds,

zero violations** (71 s; no 100,000-seed run under the evidence

@@ -5138,30 +5286,30 @@ 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.16 model (6bfae153), with the strict classification,

+on the final rev 7.17 model (b9e97783), with the strict classification,

**in two ways**: the **random sweep**, 3,000 seeds each (the 30,000- and

100,000-seed sweeps of earlier revisions are not run under the evidence

policy of §14.2.1, Paul 2026-10-06; their columns say so); and

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

-same mutation, for the 59 rules that have them. A rule is caught

+same mutation, for the 60 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 **106 rules**, unchanged since rev

-7.15 (rev 7.16 changes what `persisted-park-scope` persists, not the

-rule set).

+section does too. The model has **107 rules**: rev 7.16's 106 plus

+`scope-membership` (claim rev 6.24 §2, R16-1, R16-2).

`mutate.sh 3000`, run serially at `HOSTLIFE_PAR=2` under `nice -n 19`, 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.13's

counts, the last with the deeper sweeps, are in the rev 7.13 spec

-(1f511c42); rev 7.14's in a4389280, rev 7.15's in 63fc6a71. **Every

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

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

+(1f511c42); rev 7.14's in a4389280, rev 7.15's in 63fc6a71, rev 7.16's

+in 6f2a93c9. **Every table below is regenerated from the retained

+verdict files** (R9-6; `~/.cache/nearest-region/rev717-sweeps/`), none

+is carried over.

| | rules |

|---|---|

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

-| caught alone by the sweep at 30,000 (and by their witness, where one exists) | not run for rev 7.16 (evidence policy; Paul 2026-10-06); without a verdict this round, the rare rules the sweep reaches only at 30,000: 1 (`hostguard`) |

-| caught alone by the sweep at 100,000 (and by its witness, where one exists) | not run for rev 7.16 (evidence policy; Paul 2026-10-06) |

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

+| caught alone by the sweep at 30,000 (and by their witness, where one exists) | not run for rev 7.17 (evidence policy; Paul 2026-10-06); without a verdict this round, the rare rules the sweep reaches only at 30,000: 1 (`hostguard`) |

+| caught alone by the sweep at 100,000 (and by its witness, where one exists) | not run for rev 7.17 (evidence policy; Paul 2026-10-06) |

| caught alone by their witness only; the sweep at 3,000 misses them | 22 (`absent-marker-origin`, `admit-before-start`, `baseline-live`, `close-evidence`, `close-waits`, `closed-marker`, `covered-baseline-refused`, `declare-lost-compute`, `evidence-whole-tree`, `generation-conditional`, `lost-quarantine`, `markers-last`, `newest-l0`, `orphan-order`, `persisted-park-scope`, `probe-window`, `remote-baseline`, `restore-gap-closed`, `restore-overlap`, `restore-selected-baseline`, `seal-return`, `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 |

@@ -5169,6 +5317,17 @@ table below is regenerated from the retained verdict files** (R9-6;

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

| unexercised | **0** |

+**What rev 7.17 moved.** The new rule `scope-membership`

+1,252 / 3,000 (a park archives a key outside its scope,

+INV-23). The rules the scoped delete and sweep touched: `sweep-namespace`

+984 / 3,000, `straggler-sweep` 1,192 / 3,000,

+`sweep-staging` 38 / 3,000, `legacy-discovery`

+367 / 3,000, `touched-incomplete` 0 / 3,000,

+`location-per-incarnation` 29 / 3,000,

+`live-set-region` 2 / 3,000, `quiet-before-ack`

+152 / 3,000, `holderless-park` 562 / 3,000,

+`writes-lost` 16 / 3,000, `cover-at-park` 30 / 3,000.

**What rev 7.16 moved.** No new rule; `persisted-park-scope`

witness; sweep 0 / 3,000 gains the staging-deadline scenario, and

the scope's queuing-time binding touched `quiet-before-ack`

@@ -5402,43 +5561,43 @@ witness to hold there; each witness violates with the failure it names.

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

| `markers-last` (R2-6) | the source has a registered timer; the target's agent crashes between extracting the files and writing the marker | **violated**: INV-2, the timer is lost | | witness; sweep 0 / 3,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 |

| `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 |

| `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) | | 301 / 3,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 | 299 / 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) | | 170 / 3,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 | 261 / 3,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 | | witness; sweep 0 / 3,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 |

+| `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 | | 984 / 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 |

| `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) | | witness; sweep 0 / 3,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 |

| `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) | | 57 / 3,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) | | 16 / 3,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) | | 17 / 3,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 |

-| `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 |

+| `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) | | 70 / 3,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) | | 13 / 3,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 |

| `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 |

| `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 |

-| `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) | | 710 / 3,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) | | 711 / 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) | | witness; sweep 0 / 3,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 |

-| `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) | | 5 / 3,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) | | 6 / 3,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 | | 716 / 3,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) | | 38 / 3,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 |

| `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 |

| `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 |

| `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 |

-| `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 | | 15 / 3,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 | | 16 / 3,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 |

| `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 |

@@ -5446,10 +5605,11 @@ witness to hold there; each witness violates with the failure it names.

| `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 |

| `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 |

| `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) | 4 / 3,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 | 29 / 3,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 | 30 / 3,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 |

| `persisted-park-scope` (claim rev 6.23 §2, R13-4, R15-1), two scenarios | (i) a committed move's source-region park, scoped at the commit with the cut's stop evidence; the source region's agent restarts 20 steps before the deadline; (ii) the move's staging lane, scoped with its seal bound; the target region's cleanup first runs 40 steps past the deadline, under a restarted agent | held: (i) acknowledged within the persisted deadline and slack; (ii) acknowledged at once, never before the deadline | **violated** under the mutation: the chores are unscoped and the runner binds the cleanup's own clock, so the horizon starts again at the restart (i) and the staging lane waits a fresh `H` past its deadline (ii) (INV-9) | witness; sweep 0 / 3,000 |

-| `holderless-park` (claim rev 6.15 §6.2a, R13-4) | a deleted host's region keeps late residue; the free host's sweep and a create requested at once | held: the sweep runs as a holderless parking op, the create waits for `FreeAfterPark`, then serves | **violated** under the mutation: bare chores on the free claim, the create claims the host over the outstanding park (INV-20) | 561 / 3,000 |

+| `holderless-park` (claim rev 6.15 §6.2a, R13-4) | a deleted host's region keeps late residue; the free host's sweep and a create requested at once | held: the sweep runs as a holderless parking op, the create waits for `FreeAfterPark`, then serves | **violated** under the mutation: bare chores on the free claim, the create claims the host over the outstanding park (INV-20) | 562 / 3,000 |

+| `scope-membership` (claim rev 6.24 §2, R16-2) | incarnation 1 is deleted and incarnation 2 serves; a late object lands under `instances/<host>/1/g-old/` | held: the sweep queues a chore scoped to `instances/<host>/1` with archive incarnation 1 and parks within it | **violated** under the mutation: rev 7.16's whole-prefix parks, scoped `instances/<host>`, archive the child incarnation's object from outside their scope (INV-23) | 1,252 / 3,000 |

| `covered-baseline-refused` (claim rev 6.22 §6.2a, R13-1) | an unfinished run g2 → g1 whose record is covered and whose g1 was retired in the region | held: the start is refused and alerts, the host does not run | **violated** under the mutation: the walk passes over the empty g1 and restores the marker's retired g1 as an empty database (INV-2) | witness; sweep 0 / 3,000 |

| `restore-selected-baseline` (R14-1) | the marker names S; R's first upload is in flight when R crashes; R2 is admitted over the empty R and crashes before uploading; R's upload lands | held: the next start selects R from R2 → R → S and restores it rooted at `[1, 1]` | **violated** under the mutation: the start restores R through the marker, which names S, refuses it, and the valid recovery stalls (INV-3) | witness; sweep 0 / 3,000 |

| `unique-declarations` (R14-2), two scenarios | (i) the target is destroyed after the flip and before its first admission, `src_covered` false, the source's cut session uncertified; (ii) the same after the target's probe was admitted | held: the source's cut session is declared once, in `writes_lost` (i) or in the list (ii); nothing twice | **violated** under the mutation: the cut session is declared twice, through `writes_lost` and the separate path (INV-21) | 3 / 3,000 |

@@ -5478,56 +5638,57 @@ 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: 92 of 106** (70 by the sweep at 3,000; 22 by their witness alone, marked ‡; the sweeps at 30,000 and 100,000 were not run for rev 7.16 (evidence policy; Paul 2026-10-06), so the one rare rule the sweep reaches only there, `hostguard`, has no verdict this round).

+**Caught alone: 93 of 107** (71 by the sweep at 3,000; 22 by their witness alone, marked ‡; the sweeps at 30,000 and 100,000 were not run for rev 7.17 (evidence policy; Paul 2026-10-06), so the one rare rule the sweep reaches only there, `hostguard`, has no verdict this round).

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

| `admit-everywhere` | 716 / 3,000 | | `anchor-acked` | 12 / 3,000 |

-| `cancelled-creates` | 377 / 3,000 | | `claim-never-deleted` | 5 / 3,000 |

+| `cancelled-creates` | 376 / 3,000 | | `claim-never-deleted` | 5 / 3,000 |

| `claim-op-exclusive` | 120 / 3,000 | | `clean-return-identity` | 13 / 3,000 |

| `dirty-return` | 1 / 3,000 | | `evidence-from-state` | 2,632 / 3,000 |

-| `fence-etag` | 22 / 3,000 | | `fence-stamp` | 299 / 3,000 |

-| `files-carried` | 25 / 3,000 | | `floor-boot-recovery` | 2,563 / 3,000 |

+| `fence-etag` | 22 / 3,000 | | `fence-stamp` | 261 / 3,000 |

+| `files-carried` | 26 / 3,000 | | `floor-boot-recovery` | 2,563 / 3,000 |

| `foreign-region-uncovered` | 4 / 3,000 | | `fresh-admission` | 11 / 3,000 |

-| `holderless-park` | 561 / 3,000 | | `legacy-discovery` | 367 / 3,000 |

+| `holderless-park` | 562 / 3,000 | | `legacy-discovery` | 367 / 3,000 |

| `live-set-region` | 2 / 3,000 | | `location-per-incarnation` | 29 / 3,000 |

-| `obligations-block-ops` | 21 / 3,000 | | `orphan-no-deadline` | 45 / 3,000 |

+| `obligations-block-ops` | 21 / 3,000 | | `orphan-no-deadline` | 44 / 3,000 |

| `park-by-version` | 2,539 / 3,000 | | `park-skip-lock` | 2,733 / 3,000 |

-| `purge-claim-fence` | 28 / 3,000 | | `purge-journal` | 1,896 / 3,000 |

-| `purge-reserve-first` | 2,144 / 3,000 | | `quiet-before-ack` | 152 / 3,000 |

+| `purge-claim-fence` | 28 / 3,000 | | `purge-journal` | 1,897 / 3,000 |

+| `purge-reserve-first` | 2,142 / 3,000 | | `quiet-before-ack` | 152 / 3,000 |

| `recovery-current-inputs` | 37 / 3,000 | | `recovery-generation` | 13 / 3,000 |

| `recovery-pass` | 2,432 / 3,000 | | `registration-recovery` | 2,011 / 3,000 |

-| `retirement-ids` | 459 / 3,000 | | `return-stamp` | 69 / 3,000 |

+| `retirement-ids` | 461 / 3,000 | | `return-stamp` | 70 / 3,000 |

| `revalidate-before-effect` | 14 / 3,000 | | `revert-journal` | 13 / 3,000 |

-| `rollback-journal` | 1 / 3,000 | | `root-advance` | 16 / 3,000 |

-| `sdk-no-resign` | 11 / 3,000 | | `seal-by-version` | 1 / 3,000 |

-| `sign-at-check` | 15 / 3,000 | | `sign-before-safeuntil` | 19 / 3,000 |

-| `source-readiness` | 12 / 3,000 | | `staging-quiet` | 1 / 3,000 |

-| `stale-hold-release` | 1 / 3,000 | | `start-check` | 17 / 3,000 |

-| `start-check-claim-gen` | 15 / 3,000 | | `straggler-sweep` | 770 / 3,000 |

-| `strict-spawn` | 12 / 3,000 | | `sweep-namespace` | 541 / 3,000 |

-| `sweep-staging` | 38 / 3,000 | | `target-park` | 16 / 3,000 |

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

-| `unique-declarations` | 3 / 3,000 | | `valid-ltx` | 38 / 3,000 |

-| `writer-session` | 5 / 3,000 | | `writes-lost` | 15 / 3,000 |

+| `rollback-journal` | 1 / 3,000 | | `root-advance` | 17 / 3,000 |

+| `scope-membership` | 1,252 / 3,000 | | `sdk-no-resign` | 12 / 3,000 |

+| `sign-before-safeuntil` | 19 / 3,000 | | `source-readiness` | 12 / 3,000 |

+| `staging-quiet` | 1 / 3,000 | | `stale-hold-release` | 1 / 3,000 |

+| `start-check` | 17 / 3,000 | | `start-check-claim-gen` | 15 / 3,000 |

+| `straggler-sweep` | 1,192 / 3,000 | | `strict-spawn` | 13 / 3,000 |

+| `sweep-namespace` | 984 / 3,000 | | `sweep-staging` | 38 / 3,000 |

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

+| `timer-freeze` | 3 / 3,000 | | `unique-declarations` | 3 / 3,000 |

+| `valid-ltx` | 39 / 3,000 | | `writer-session` | 6 / 3,000 |

+| `writes-lost` | 16 / 3,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`

@@ -5542,19 +5703,19 @@ subset in the gate.

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

-| `purge-claim-fence` + `fence-etag` (**the re-read alone**, rev 7's CC21 as proposed) | not run for rev 7.16 (evidence policy; Paul 2026-10-06) | `purge-claim-fence` 28 / 3,000, `fence-etag` 22 / 3,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` | not run for rev 7.16 (evidence policy; Paul 2026-10-06) | `exec-admission` 0 / 3,000, `hold-op-open` 0 / 3,000, `start-check-claim-gen` 15 / 3,000, `exec-writer` 0 / 3,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) | not run for rev 7.17 (evidence policy; Paul 2026-10-06) | `purge-claim-fence` 28 / 3,000, `fence-etag` 22 / 3,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` | not run for rev 7.17 (evidence policy; Paul 2026-10-06) | `exec-admission` 0 / 3,000, `hold-op-open` 0 / 3,000, `start-check-claim-gen` 15 / 3,000, `exec-writer` 0 / 3,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 |

| `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) | not run for rev 7.16 (evidence policy; Paul 2026-10-06) | `fence-stamp` 299 / 3,000, `hostguard` 0 / 3,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) | not run for rev 7.17 (evidence policy; Paul 2026-10-06) | `fence-stamp` 261 / 3,000, `hostguard` 0 / 3,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

@@ -5605,6 +5766,13 @@ baselines, this sweep and the witnesses are the evidence for rev 7.10.

would differ, and the model's covered-local refusal (§5.1 step 9)

reaches such a generation before its emptiness is consulted in every

schedule the sweeps produced. Exact equivalence is not claimed.

+- **The sweep protects more than the run walk selects (R16).** The

+ sweep's `deadGeneration` protects every generation of an unfinished run

+ in the authoritative region, without the run walk's region or coverage

+ filtering (§5.1 step 9), which main applies when it selects a baseline.

+ The sweep's set is the wider, conservative one: it never parks what

+ the walk could select, and may keep a covered or foreign link's

+ objects until a publication's chore retires them.

- **Admission trimming is E's rule, mirrored (R14).** Covered entries are

dropped from the front only while more than eight entries remain, and

an uncovered head stops the trimming; the model counted covered entries

@@ -5991,6 +6159,42 @@ 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.24 (0b821896), after joint round 16, and rev 6.25

+(413b12cb), which answers the four notes below: note 1 agreed and now

+§5.2 (a delete's `park-replica` per touched region is scoped to

+`holder.location`, the incarnation location or the legacy

+`instances/<host>` excluding child incarnations, plus one scoped to

+`moves/<host>`, never the whole host prefix; E's `BeginDelete` queues

+them unscoped, bound to `holder.location` at the first step, and the

+console's delete wiring queues the `moves/<host>` chore); note 2 agreed

+and fixed in code, main 67547f5 (E had recorded a boxless `writes_lost`

+on a created incarnation's first admission); notes 3 and 4 noted, no

+claim change.** Rev 6.24 sets the legacy identity (session 0, generation

+`""` read as @root, `holder.writer_box` the pre-release process's box,

+valid in both loss fields), the scope namespaces (a scope covers only

+its own namespace; an `instances/…` scope never touches `moves/`; the

+legacy `instances/<host>` scope excludes child incarnations; staging is

+parked only under an explicit `moves/…` scope) and the narrowed

+born-covered (an unscoped `park-replica` or a park scoped exactly to

+`holder.location`). Rev 7.17 encodes all of it (§5.1 step 9, §6.4,

+§7.14 items 2, 5 and 9, §14.2.2). Notes for platform-1e

+(`moves-claim-questions.md`, rev 7.17 heading): **(1)** the model's

+delete parks the deleted incarnation's own location and the staging

+namespace, one chore each, never the whole host prefix; an older

+incarnation's residue is the at-rest sweep's, as R3-4 intended; if the

+claim's delete (§5.2) is read to park the whole host prefix, say so and

+the model follows; **(2)** a created incarnation's first admission has

+a predecessor with no writer (`holder.writer_box` empty, session 0 in

+the model, generation `""`): since every declaration names a box, it

+records no `writes_lost`, nothing having been acknowledged; the model's

+INV-24 enforces it; **(3)** the model's witness fixture for a legacy

+host writes a certificate for session 0 so that a warm first wake can

+be exercised; a real pre-release writer leaves no certificate and a

+real first wake is cold; the fixture is disclosed in the model, not a

+reading of the claim; **(4)** the sweep protects every generation of an

+unfinished run in the authoritative region without the run walk's

+region and coverage filtering, a wider, conservative set (§14.2.6).

**Claim rev 6.23 (876d6908), after joint round 15: no change requested,

two notes.** Rev 6.23's §2 gives the park scope its grammar

(`instances/<host>`, `instances/<host>/<incarnation>`, `moves/<host>/<op

@@ -6001,8 +6205,9 @@ fencing bound (a staging lane's seal bound, persisted at seal or fence

time, never cleanup's start) and one deadline for every scope, a

listing later than `evidence_at + H`; it also states that a second

region's sweep joins the running op and that every sweep acknowledgement

-waits the horizon. Rev 7.16 mirrors it exactly (§6.4, §7.14 item 9,

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

+waits the horizon. Rev 7.16 mirrored its grammar, bounds and deadline (§6.4, §7.14 item

+9, §14.2.2); R16-2 found the sweep's scope grouping short of it, and rev

+7.17 corrects that under rev 6.24. Notes for platform-1e (`moves-claim-questions.md`, rev 7.16

heading): **(1)** a delete's and an adoption's `park-replica` are queued

by a CAS that has no evidence time yet (the stop evidence is proven by

the parking box later), so the model binds their scope in a CAS before

@@ -6561,6 +6766,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.23 Joint round 16 (claim 876d6908, moves rev 7.16 6f2a93c9, model 6bfae153, merged code 7f403a77)

+Round 16 found R15-1 resolved, no P1 and three P2s: two in the merged

+code (R16-1, the park engine; R16-3, `Adopt`'s session zero), which

+platform-1e fixed and merged to main as c7e595b (squashed from

+`fix/hostclaim-r16` f093f7b8), and one in the model. Claim rev 6.25

+(413b12cb) answers rev 7.17's notes, and main 67547f5 adds the

+first-admission fix.

+Claim rev 6.24 (0b821896) states the rules for all three.

+| finding | rev 7.17 |

+|---|---|

+| R16-2 (P2, C) the model's instance sweep ran outside its persisted scope: incarnation 2 serving, a late object under `instances/<host>/1/…`, a chore scoped `instances/<host>` with incarnation 2 parked it; INV-23 accepted the syntax and the archive ignored the incarnation | chores grouped by location and archive incarnation, executed strictly within the scope, INV-23 checking membership for every manifest source, the archive under the incarnation; the delete's parks scoped to the deleted location; rule `scope-membership`, witness `wSweepScopeMembership`; B's "mirrors it exactly" withdrawn (§6.4, §7.14 item 9, §19.4) |

+| R16-3 (P2, code; alignment for the model) adoption's session 1 hid the session-zero case | the legacy identity is session 0 with generation `""` (@root), valid in both loss fields; INV-24; a created incarnation's first admission declares nothing; `TestLegacyLostTargetReturn` (adopt → `src_covered` false → cold target → lost → the return declares the target's session and cut session 0) (§5.1 step 9, §7.14 item 2) |

+| R16-1 (P2, code; alignment for the model) a legacy instance park also deleted staging | the model's instance parks never list `moves/`, and the legacy scope excludes child incarnations; `TestStagingSurvivesLegacyPark` (§6.4) |

+| born covered, narrowed (6.24 item 5) | an unscoped `park-replica` or a park scoped exactly to `holder.location` (§5.1 step 9, §7.14 item 5) |

+| the sweep's walk | disclosed as the wider, conservative set (§14.2.6) |

### 22.22 Joint round 15 (claim 0bf2f49f, moves rev 7.15 63fc6a71, model f6fb0579, library E f0127321, selector F d7621a29)

Round 15 found all five round-14 items resolved and one new P2 across