carlos / platform Public

spec: move-any-app rev 7.16, joint round 15 and claim rev 6.23

R15-1: claim rev 6.23's park scope mirrored exactly: the location
grammar (instances/<host>, instances/<host>/<incarnation>,
moves/<host>/<op id>, moves/<host>; no trailing slash), the archive
incarnation, evidence_at always the original evidence or fencing bound
(a staging lane's seal bound, the seal plus the lease; never cleanup's
start), one deadline for every scope: a listing later than
evidence_at + H. Rev 7.15's separate staging treatment is gone; §6.4,
§7.14 item 9 rewritten; witness wStagingScopeDeadline; two notes for the
claim.

Model 6bfae153: 106 rules, 72 witnesses. Evidence under the policy: the
gate; the 30,000-seed baseline (clean, 45,059 operations, 71 s, niced,
started when the load fell below 12); one 3,000-seed sweep serially at
HOSTLIFE_PAR=2 under nice (92 caught, 14 expected misses, exit 0); 92 of
106 caught alone. Records in ~/.cache/nearest-region/rev716-sweeps/.

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

claude 2 weeks ago 6f2a93c91117f8e4e6d10d38bf3310e3a94614da parent 6bfae15

1 file changed, +234 −86

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

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 c779f3984..7ab94241b 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,36 @@

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

**Date:** 2026-10-06

-**Revision:** 7.15.

+**Revision:** 7.16.

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

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

+ (876d6908, §2's park scope: the location grammar, the archive

+ incarnation, `evidence_at` always the original evidence or fencing

+ bound, one deadline for every scope); E is merged to main as 99084d7,

+ F merges next; §22.22 has the disposition. **Every remote chore

+ carries the claim's scope from its queuing CAS** (R15-1): `location`

+ exactly one of `instances/<host>`, `instances/<host>/<incarnation>`,

+ `moves/<host>/<op id>` (a move's staging or a rollback's return lane)

+ or `moves/<host>` (the staging sweep), no trailing `/` (INV-23);

+ `incarnation` the location's own, the staging op's holder incarnation

+ or, for a free host's `moves/<host>` sweep, the newest retired one;

+ **`evidence_at` the original bound**, the cut's stop for the commit's

+ source park, the release or the declaration for the target region's,

+ **the seal bound for a staging lane** (the time after which no staging

+ writer, its lease holder included, can still write: the seal plus the

+ staging lease), the listing for a sweep, the publication for a

+ generation chore; **never the cleanup's start time**. **One deadline

+ for every scope, staging included:** acknowledge only after a listing

+ later than `evidence_at + H`; there is no separate staging contract

+ (rev 7.15 bound a staging park at cleanup and then kept the seal's

+ quiet time instead, which Astra's example exposed: sealed at 100,

+ deadline 560, a cleanup first running at 600 must acknowledge at

+ once, not at 660). Witness `wStagingScopeDeadline` (delayed cleanup

+ through an agent restart; INV-9 under the mutation);

+ `wParkScopeSurvivesRestart` takes its deadline from the persisted

+ scope. Rules unchanged (106); witnesses 72. Evidence under the policy

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

- **Rev 7.15** answers **joint round 14** (`CODEX-FINDINGS-JOINT-R14.md`,

cited "R14-n"), against claim spec rev 6.22 (0bf2f49f) with

@@ -2006,28 +2035,45 @@ no later retirement of that location may ever run. Claim rev 5's at-rest

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

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

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

-**The chore carries a persisted park scope** (claim rev 6.15 §2, R13-4):

-`{location, incarnation, evidence_at, request_limit}`, written at the

-queuing CAS (the sweeping box's complete listing is the evidence, taken

-then), so every retry, an agent restart's included, uses the same

-location, archive incarnation and **original** evidence time; a retry's

-own clock is never evidence, and a restart never starts the horizon

-again (rev 7.13's model kept the evidence time in a box-local map that

-the restart cleared; witness `wParkScopeSurvivesRestart`). Every remote

-chore has one (R14-5): a whole-location park binds its scope in a CAS

-before its first step runs, once its stop evidence is in hand; a

-generation chore takes its scope from the publication that queues it

-(the marker's publication is the evidence that the predecessor is dead);

-a staging park binds one before its first step and keeps the seal's own

-quiet time; INV-22, no remote chore runs a step unscoped. **The horizon

-after the evidence is `H`** (R14-3): the scope persists `request_limit`,

-the longest request, and the acknowledgement waits `evidence_at + H`

-with **`H` = the signature-age limit plus `request_limit`** (claim §6.2a,

-§2: 15 minutes plus 120 s in production; `sigAgeH + requestLimitH =

-horizonH` in the model, 45 + 15 = 60 steps), never `evidence_at +

-request_limit` alone, which rev 7.14 wrote here and which would have

-let a retirement be declared complete inside the window the signature

-age still covers. The sweep parks at once and acknowledges, with its

+**The chore carries a persisted park scope** (claim rev 6.23 §2; R13-4,

+R14-5, R15-1): `{location, incarnation, evidence_at, request_limit}`,

+written at the queuing CAS, so every retry, an agent restart's included,

+uses the same location, archive incarnation and **original** evidence

+time; a retry's own clock is never evidence, and a restart never starts

+the horizon again (rev 7.13's model kept the evidence time in a

+box-local map that the restart cleared; witness

+`wParkScopeSurvivesRestart`). **`location`** is exactly one of

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

+id>` (a move's staging or a rollback's return lane, the op id with no

+`/`) or `moves/<host>` (the staging sweep only, while no operation

+stages there), nothing else and no trailing `/` (the model's INV-23

+checks every scope against that grammar). **`incarnation`** names the

+archive: the location's own, the staging op's holder incarnation, or,

+for a free host's `moves/<host>` sweep, the newest retired incarnation.

+**`evidence_at` is always the original evidence or fencing bound**,

+never the cleanup's start time: the cut's stop evidence for the commit's

+park of the source region; the release's stop, or the declaration's

+`fenced_at`, for the target region's; **a staging lane's own seal

+bound**, the time after which no staging writer, its lease holder

+included, can still write (the seal plus the staging lease), persisted

+when the lane is sealed or fenced; the sweeping box's complete listing

+for a sweep; the publication that supersedes a generation for a

+generation chore. A chore queued without a scope (a delete's or an

+adoption's `park-replica`, whose CAS has no evidence time yet) binds one

+in a CAS before its first step runs, once its stop evidence is in hand,

+and never again; INV-22, no remote chore runs a step unscoped. **One

+deadline for every scope** (R15-1): acknowledge only after a

+verification listing later than **`evidence_at + H`**, with **`H` = the

+signature-age limit plus `request_limit`** (claim §6.2a, §2: 15 minutes

+plus 120 s in production; `sigAgeH + requestLimitH = horizonH` in the

+model, 45 + 15 = 60 steps). There is no separate staging contract: rev

+7.15 bound a staging park at cleanup and then kept the seal's quiet time

+instead of that bound, so a lane sealed at step 100, deadline 560, whose

+cleanup first ran at 600 would have waited until 660 (witness

+`wStagingScopeDeadline`: the cleanup acknowledges at once, through an

+agent restart, since the persisted deadline has passed). Rev 7.14 wrote

+`evidence_at + request_limit` here, dropping the signature-age

+allowance (R14-3). The sweep parks at once and acknowledges, with its

straggler pass, only after a **verification listing later than

`evidence_at + H`** (platform-1e's answer to rev 7.14 note 2: a

park-sweep is a retirement event and is not exempt from the horizon). **On a serving host** the chore's op is

@@ -2878,12 +2924,15 @@ this text wins.

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.

-9. **Park state** (claim rev 6.15, R13-4, R14-3 to R14-5; §6.4). Every

- remote chore carries a persisted park scope, bound before its first

- step, at the sweep's queuing CAS or at the publication that queues a

- generation chore, and every retry uses its original evidence time;

- the scope persists `request_limit` and every acknowledgement waits

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

+9. **Park state** (claim rev 6.23 §2; R13-4, R14-3 to R14-5, R15-1;

+ §6.4). Every remote chore carries a persisted park scope from its

+ queuing CAS (a delete's or adoption's park binds one before its first

+ step), `{location, incarnation, evidence_at, request_limit}` in the

+ claim's grammar; `evidence_at` is the original evidence or fencing

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

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

@@ -3816,6 +3865,41 @@ 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.16: joint round 15 and claim rev 6.23.**

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

+ `w.scoped(obligation, evidenceAt, inc)` attaches `parkScope{Location:

+ scopeLocation(prefix), Inc, EvidenceAt, RequestLimit}` at every

+ queuing site: the commit's source park (`op.StopAt`), the release's

+ target park (the release's step), the lost-target release

+ (`fenced_at`, the declaration's step), every staging lane

+ (`stagingBound(quiet)`, the seal bound: the lane's quiet time less

+ `H`, so the `staging-quiet` mutation's "now" yields a bound already

+ past), the sweep (the listing, now; the archive incarnation the

+ holder's or, on a free host, the newest retired), the generation

+ chores (the publication, now). `scopeLocation` strips the park

+ prefix's trailing `/`; INV-23 checks every scope's location against

+ the grammar (`scopeLocationRe`; the model's incarnation ids are

+ decimal). The delete's and adoption's `park-replica` still bind theirs

+ before the first step, once the stop evidence is in hand. Under the

+ `persisted-park-scope` mutation chores are queued unscoped and the

+ runner binds the cleanup's own clock, as rev 7.13 did.

+- **One deadline (R15-1).** `parkScope.deadline() = EvidenceAt + sigAgeH

+ + RequestLimit`; the runner's quiet for every scoped chore is the

+ larger of its queued quiet time and that deadline (a staging lane's

+ regardless of `quiet-before-ack`, since its queued quiet time was that

+ bound already); the acknowledgement's `quiet_after` uses it too. Rev

+ 7.15's staging exclusion is gone. Witness `wStagingScopeDeadline`: a

+ committed move's staging lane, deadline `seal + stagingTTL + H`; the

+ target region's obligation runner is withheld until 40 steps past it,

+ then the target's agent restarts and the cleanup begins: the

+ acknowledgement must come within 20 steps and never before the

+ deadline; under the mutation the fresh bound waits another `H` (568 →

+ acknowledged at 669 in the trace, the round's 560/600/660 example in

+ the model's steps). `wParkScopeSurvivesRestart` reads its deadline

+ from the chore's scope (the cut's stop plus `H`) and restarts the

+ agent 20 steps before it.

**Rev 7.15: joint round 14.**

- **The selected baseline is restored (R14-1).** `openState.SourcePin`

@@ -4601,6 +4685,25 @@ 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.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

+policy of §14.2.1). Across the 30,000 seeds: 45,059 completed

+operations, 20,487 cold and 4,803 warm admissions,

+148,810 scopes bound before a chore's first step (the delete's

+and adoption's parks; every other chore scoped at its queuing),

+11,350 holderless sweeps, 1 regions joining a

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

+0 starts restoring a selected run generation,

+16,733 writes_lost records declaring 2,408 writes

+(72 for a lost target's other sessions, 8 for

+the source's cut session), 224 completed moves,

+621 clean and 24 dirty rollbacks,

+97 reverts, 74 declared losses, 7,327

+pushes, 27,197 delete-park-free cycles, 2,746 final

+recovery admissions (0 unverified). Every oracle left

+the system unchanged.

**Rev 7.15, on the final model (joint round 14: the selected baseline

restored, declarations unique, the horizon's parts, joining, every chore

scoped): 30,000 seeds, zero violations** (97 s; no 100,000-seed run

@@ -5035,29 +5138,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.15 model (f6fb0579), with the strict classification,

+on the final rev 7.16 model (6bfae153), 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

if either catches it; `mutate.sh` reports the two separately, and this

-section does too. The model has **106 rules**: rev 7.14's 104 plus

-`restore-selected-baseline` (R14-1) and `unique-declarations` (R14-2).

+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).

`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. **Every table below is

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

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

+(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.

| | 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.15 (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.15 (evidence policy; Paul 2026-10-06) |

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

@@ -5065,6 +5169,15 @@ regenerated from the retained verdict files** (R9-6;

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

| unexercised | **0** |

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

+152 / 3,000, `straggler-sweep` 770 / 3,000,

+`sweep-namespace` 541 / 3,000, `sweep-staging`

+38 / 3,000, `staging-quiet` 1 / 3,000,

+`lost-return-park` 1 / 3,000, `holderless-park`

+561 / 3,000, `cover-at-park` 29 / 3,000.

**What rev 7.15 moved.** The two new rules: `restore-selected-baseline`

witness; sweep 0 / 3,000 (the start refuses the baseline the walk

selected and the recovery stalls) and `unique-declarations`

@@ -5296,36 +5409,36 @@ witness to hold there; each witness violates with the failure it names.

| `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) | | 304 / 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 | 303 / 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 |

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

| `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) | | 55 / 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) | | 20 / 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 |

| `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) | | 68 / 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) | | 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 |

+| `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) | | 711 / 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 |

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

| `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) | | 37 / 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 |

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

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

@@ -5335,7 +5448,7 @@ witness to hold there; each witness violates with the failure it names.

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

| `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.15 §2, R13-4) | a committed move's source-region park binds its scope in the claim; 45 steps on, the source region's agent restarts mid-park | held: the acknowledgement comes within the commit's evidence time plus the horizon and slack | **violated** under the mutation: the box-local evidence map is gone with the agent, the horizon starts again, the acknowledgement is late (INV-9) | 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 |

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

@@ -5365,24 +5478,24 @@ 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.15 (evidence policy; Paul 2026-10-06), so the one rare rule the sweep reaches only there, `hostguard`, has no verdict this round).

+**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).

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

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

| `cancelled-creates` | 377 / 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,633 / 3,000 |

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

-| `files-carried` | 25 / 3,000 | | `floor-boot-recovery` | 2,561 / 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 |

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

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

@@ -5394,27 +5507,27 @@ proper subsets hold. It is no longer run.

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

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

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

-| `recovery-current-inputs` | 36 / 3,000 | | `recovery-generation` | 12 / 3,000 |

-| `recovery-pass` | 2,442 / 3,000 | | `registration-recovery` | 2,013 / 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 |

+| `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` | 428 / 3,000 | | `return-stamp` | 68 / 3,000 |

-| `revalidate-before-effect` | 16 / 3,000 | | `revert-journal` | 12 / 3,000 |

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

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

+| `retirement-ids` | 459 / 3,000 | | `return-stamp` | 69 / 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` | 14 / 3,000 | | `sign-before-safeuntil` | 14 / 3,000 |

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

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

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

-| `strict-spawn` | 13 / 3,000 | | `sweep-namespace` | 542 / 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` | 2 / 3,000 |

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

-| `writer-session` | 5 / 3,000 | | `writes-lost` | 11 / 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 |

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

@@ -5429,19 +5542,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.15 (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.15 (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.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 |

| `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.15 (evidence policy; Paul 2026-10-06) | `fence-stamp` 303 / 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.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 |

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

@@ -5878,6 +5991,29 @@ 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.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

+id>`, `moves/<host>`), the archive incarnation (the location's own, the

+staging op's holder's, the newest retired for a free host's

+`moves/<host>` sweep), `evidence_at` always the original evidence or

+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

+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

+the first step, with the evidence time at which the stop evidence was

+first in hand, once and never again; the claim's "a chore without a

+scope is bound to one before its first step runs" is read to mean

+exactly that, and no other chore is bound late; **(2)** the model's

+incarnation ids are decimal where the claim's are 64 hex, and its op ids

+are its own; the grammar oracle (INV-23) checks the four forms with

+those alphabets.

**Platform-1e's answers to the rev 7.14 notes, and joint round 14: no

change requested, three notes.** All six notes agreed (joining

preferred; the sweep waits the full `H`; recovery replays only

@@ -6425,6 +6561,18 @@ 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.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

+A, B and C; E and F stayed merge-ready, and E is merged to main

+(99084d7). Claim rev 6.23 (876d6908) answers the A half.

+| finding | rev 7.16 |

+|---|---|

+| R15-1 (P2, A/B/C) staging scopes did not satisfy the shared path and deadline contract: A's grammar excluded `moves/<host>/…`; B required every acknowledgement after `evidence_at + H` and C bound a staging park at cleanup, then kept the seal's quiet time instead | claim rev 6.23's grammar mirrored, with the staging and staging-sweep forms and the archive incarnation; every chore scoped at its queuing CAS with the original bound, a staging lane's the seal bound (seal plus lease), never cleanup's start; one deadline for every scope; INV-23; witness `wStagingScopeDeadline` (delayed cleanup through a restart: acknowledged at once, never before the deadline; a fresh bound under the mutation) (§6.4, §7.14 item 9, §14.2.2) |

+| the three rev 7.15 notes | note 1 superseded by 6.23 (the staging scope's grammar and bound); notes 2 and 3 accepted as stated |

+| E, F | E merged to main as 99084d7; F merges next; nothing asked of them |

### 22.21 Joint round 14 (claim 0bf2f49f, moves rev 7.14 a4389280, model 4ebfa0a5, library E f0127321, selector F d7621a29)

Round 14 found no P1, judged A ready as the claim contract and E and F