carlos / platform Public

spec: move-any-app rev 7.15, joint round 14

R14-1: the start restores what the run walk selected, a run generation
rooted at [1, 1] or the marker's through generation.json, as the
oracle does. R14-2: one writes_lost plus additional_writes_lost, unique
by (box, session), the source's cut session under its persisted identity,
one alert per declaration, INV-21. R14-3: the horizon after the evidence
is H, the signature-age limit plus request_limit; the scope persists
request_limit; a park-sweep acknowledges only after a listing later than
evidence_at + H (rev 7.14's formula corrected in §6.4 and §19.4). R14-4:
a running holderless sweep admits another region's chores. R14-5: every
remote chore runs under a persisted scope, INV-22. Fidelity limits in
§14.2.6 (occupancy by current objects; trimming and the publication's
precondition aligned with E). Three notes for the claim.

Model f6fb0579: 106 rules, 71 witnesses. Evidence under the policy: the
gate, the 30,000-seed baseline (clean, 45,026 operations, 97 s, niced),
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/rev715-sweeps/.

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

claude 2 weeks ago 63fc6a7111e6c7a886b08b5d500b6f8b21857141 parent f6fb057

1 file changed, +303 −86

docs/superpowers/specs/2026-10-02-move-any-app-design.md +303 −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 10fb74664..c779f3984 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,37 @@

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

**Date:** 2026-10-06

-**Revision:** 7.14.

+**Revision:** 7.15.

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

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

+ platform-1e's answers to the six rev 7.14 notes, E f0127321 and F

+ d7621a29, both MERGE-READY there; §22.21 has every disposition. **The

+ start restores what the run walk selected** (R14-1): the open state

+ carries the restore mode, the marker's generation through

+ `generation.json` or a run generation rooted at `[1, 1]`, so the start

+ and the recovery oracle use one selection; witness

+ `wIntermediateBaseline` (R's first upload pending at its crash, an

+ empty R2, R's upload landing). **One `writes_lost` plus

+ `additional_writes_lost`, unique by `(box, session)`** (R14-2): the

+ source's cut session joins the list under its persisted identity, the

+ separate representation is gone, one alert per declaration, INV-21;

+ witnesses before and after the target's first admission. **The

+ horizon keeps its signature-age allowance** (R14-3): the park scope

+ persists `request_limit`, and every acknowledgement waits

+ `evidence_at + H` with `H` the signature-age limit plus

+ `request_limit`; a park-sweep acknowledges only after a verification

+ listing later than that (platform-1e's answer to note 2). **A running

+ holderless sweep admits another region's chores** (R14-4;

+ `TestJoinHolderlessSweep`). **Every remote chore runs under a

+ persisted scope** (R14-5): generation chores take theirs from the

+ publication, staging parks bind one before their first step, INV-22.

+ Two fidelity limits stated in §14.2.6 (occupancy by current objects;

+ the publication's precondition and trimming aligned with E). Rules

+ `restore-selected-baseline`, `unique-declarations` (106 in all);

+ witnesses `wIntermediateBaseline`, `wNoDuplicateDeclarationEarly`,

+ `wNoDuplicateDeclarationLate` (71 in all). Evidence under the policy

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

- **Rev 7.14** answers **joint round 13** (`CODEX-FINDINGS-JOINT-R13.md`,

cited "R13-n") and is written against **claim spec rev 6.22**

@@ -1274,12 +1304,16 @@ fails there first (§14.2.6).

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

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

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

- R12-1). **Representation** (claim rev 6.22 item 2, R13-3): the

+ R12-1). **Representation** (claim rev 6.22 item 2, R13-3, R14-2): the

admission entry carries `writes_lost` (one, the predecessor's

session) and **`additional_writes_lost`** (a list, the other target

- sessions since the cut, and the source's cut session when

- `src_covered` is false), each `{box, generation, session,

- remote_max_txid}`, unique by `(box, session)`; the caller supplies

+ sessions since the cut, and the source's cut session, under its

+ persisted identity `cut.session`, when `src_covered` is false),

+ each `{box, generation, session, remote_max_txid}`, **unique by

+ `(box, session)` across both**: a target destroyed after the flip

+ and before its first admission leaves the source's cut session as

+ the predecessor itself, declared once (rev 7.14 declared it twice,

+ through a separate field; INV-21); the caller supplies

the list and the library records it in the admitting CAS; the

admitting box raises **one alert per declaration** after the CAS

and retries until delivered, and the console's durable loss record

@@ -1427,8 +1461,16 @@ fails there first (§14.2.6).

an empty database; witness `wCoveredLocalBaseline`); an uncovered

local link that holds an object is the baseline, the nearest such;

one that holds none (a fresh generation that never uploaded) is

- passed over; else the marker's generation. The model's `restoreCalc`

- over that baseline is the reference the selector F mirrors. An empty

+ passed over; else the marker's generation. **The start restores

+ what the walk selected** (R14-1): the marker's generation through

+ `generation.json`, as every ordinary restore; a run generation the

+ walk selected **rooted at `[1, 1]`**, its first full upload, never

+ through the marker, which still names the run's baseline (rev

+ 7.14's start selected R from R2 → R → S and then refused it because

+ the marker named S, while the oracle restored it; the marker is

+ never published backwards). The model's `restoreCalc` over the

+ marker's generation and `restoreWith` rooted at `[1, 1]` over a

+ selected one are the reference the selector F mirrors. An empty

`holder.generation` for any other reason is unexplained missing data:

refuse the start and alert. A `holder.generation` that holds objects

has its marker published again (from the operation's build journal

@@ -1972,10 +2014,23 @@ 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: a whole-location park binds its scope in a CAS before its

-first step runs, once its stop evidence is in hand. The sweep parks at

-once and acknowledges, with its straggler pass, only after the scope's

-`evidence_at + request_limit`. **On a serving host** the chore's op is

+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

+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

`session:<holder.session>`, as for `PublishGeneration`. **On a free host**

(no holder) the sweep is a **holderless sweep** (claim rev 6.15 §6.2a):

one CAS sets `op = {kind: parking, id: <new op id>, intent: {park_sweep:

@@ -1986,8 +2041,11 @@ create waits, it is not refused), and its last acknowledgement frees the

claim again in the same CAS (`FreeAfterPark`), keeping `quiet_after`

(witness `wFreeSweepVsCreate`; INV-20: a create never claims a host while

a park of its namespace is outstanding). Another region's sweep while the

-op runs joins it with its own scoped chores; any other operation running

-suppresses new sweeps; the console's recovery pass leaves the op to its

+op runs **joins** it with its own scoped chores under the same op id

+(R14-4, platform-1e's preferred reading of rev 7.14 note 1;

+`TestJoinHolderlessSweep` has two regions' residue parked under one op

+and one `FreeAfterPark`); any other operation running suppresses new

+sweeps; the console's recovery pass leaves the op to its

runners and only replays `FreeAfterPark` for one whose chores are all

acknowledged.

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

@@ -2762,9 +2820,10 @@ this text wins.

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

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

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

- false): `writes_lost` (one) plus `additional_writes_lost` (a list),

- each `{box, generation, session, remote_max_txid}`, unique by `(box,

- session)`, one alert per declaration (R13-3). A `writes_lost` record

+ 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

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

@@ -2772,8 +2831,10 @@ this text wins.

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

generation of the run that holds an object **in this region**, else

the marker's, walked as §5.1 step 9 says (R13-1): a covered foreign

- link is passed over, a covered local baseline refuses and alerts; an

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

+ link is passed over, a covered local baseline refuses and alerts; the

+ start restores the selected run generation rooted at `[1, 1]`, the

+ marker's through `generation.json` (R14-1); an empty generation

+ outside an unfinished run is refused and alerted.

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

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

name the source's generation and stamp again, leaving

@@ -2817,9 +2878,12 @@ 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; §6.4). Every remote chore

- carries a persisted park scope, bound before its first step or at the

- sweep's queuing CAS, and every retry uses its original evidence time.

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

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

@@ -3223,9 +3287,10 @@ create and on an `xargs` failure, requires exactly one well-formed

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

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

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

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

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

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

-rev 7.14).

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

+holderless op (§6.4, rev 7.15).

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

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

@@ -3751,6 +3816,52 @@ 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.15: joint round 14.**

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

+ carries the restore mode the run walk chose: `-1`, the marker's

+ generation through `generation.json` (`restoreCalc`); `0`, a run

+ generation rooted at `[1, 1]` (`restoreWith(..., 0)`), as

+ `restoreAsNext` always restored it. The restore stage calls

+ `restoreWith` with it. Rule `restore-selected-baseline` (the mutation

+ is rev 7.14's `restoreCalc` on the selected source, which the marker

+ refuses); witness `wIntermediateBaseline`: S named by the marker; R's

+ first upload held in flight, R crashes; R2 admitted over the empty R

+ and crashed before uploading; R's upload lands; the next start selects

+ R from R2 → R → S and restores it (`restore: run generation rooted`);

+ under the mutation the start cannot restore it and the valid recovery

+ stalls (INV-3).

+- **One plus a list, unique (R14-2).** `admissionRecord.LostSrc` is gone;

+ the source's cut session, under `op.CutSession`, joins

+ `AdditionalWritesLost` through one `add` that refuses a `(box,

+ session)` already in `Lost` or the list; one alert per entry; INV-21

+ after the CAS. Rule `unique-declarations` (the mutation appends without

+ the check, as rev 7.14's separate path did); witnesses

+ `wNoDuplicateDeclarationEarly` (the target destroyed after the flip and

+ before its first admission, `src_covered` false, the source's cut

+ session uncertified: declared once) and `wNoDuplicateDeclarationLate`

+ (after the target's probe: the predecessor is the target's session, the

+ list carries the cut session once, nothing twice).

+- **The horizon's parts (R14-3).** `horizonH = sigAgeH + requestLimitH`

+ (45 + 15); `parkScope.RequestLimit` persists the request bound; every

+ quiet and acknowledgement computation is `EvidenceAt + sigAgeH +

+ RequestLimit`; the park-sweep's acknowledgement waits that, its

+ straggler pass the verification listing.

+- **Joining (R14-4).** `sweep()`'s outer guard admits a holderless

+ sweep's claim; `sweep joined a running holderless op` counts;

+ `TestJoinHolderlessSweep`.

+- **Every remote chore scoped (R14-5).** `park-generation` chores carry

+ `Scope{EvidenceAt: now}` from the publication (both sites, the

+ `baseline-live` mutation's included) and their quiet is the scope's

+ horizon; `park-staging` binds a scope before its first step, keeping

+ `SealQuiet`; INV-22 in the runner: no remote chore runs a step

+ unscoped under `persisted-park-scope`.

+- **Fidelity.** The publication's precondition is that **any** entry

+ names the published generation, as A and E read it (rev 7.14 required

+ the last); trimming is E's: covered entries from the front only while

+ more than eight entries remain. Occupancy stays by current objects

+ (§14.2.6).

**Rev 7.14: joint round 13 and claim rev 6.22.**

- **The park scope and the holderless sweep (R13-4; claim rev 6.15).**

@@ -4490,6 +4601,43 @@ 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.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

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

+45,026 completed operations, among them 20,602 cold and

+5,021 warm admissions (3,594 covered `sealed`,

+235 covered `clean-return`; 5,021 warm entries

+born covered, 126 born covered under a pending park,

+359 predecessors left uncovered by a publication for their

+own region, 0 live again and left uncovered,

+8,065 holding nothing anywhere, 229 records

+covered at the commit's park, 81 at a rollback's

+release, 1 at a lost-target release, 179 by

+the sweep; 160,230 park scopes bound before a chore's first step,

+11,341 holderless sweeps, 2 regions joining a

+running one and 11,341 `FreeAfterPark` transitions;

+0 starts that restored a selected run generation rooted at

+`[1, 1]`; 0 starts refused on a covered local

+baseline; 5,964 clean closes, 440 closes refused

+as uncertain, 330 wakes that waited for a draining writer,

+16,012 local databases purged, 1,267 starts that

+waited for a failed purge, 16,854 writes_lost records declaring

+2,455 acknowledged writes lost (78 of the

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

+source's cut session behind a lost target), 8,276 full first

+uploads, 160 markers published again, 1,061

+probes restarted, 143 probe attempts ended (136

+by the deadline check before the start), 474 app starts

+retried within their session, 0 hosts marked failed;

+2,763 final recovery admissions run by the oracle,

+0 unverified), 226 completed moves,

+622 clean and 22 dirty rollbacks,

+96 pre-flip reverts, 74 declared losses,

+7,327 pushes, 27,180 delete-park-free cycles and

+1,485 lost disks (1,071 with a crash). Every oracle

+left the system unchanged.

**Rev 7.14, on the final model (claim rev 6.22: the persisted park

scope, the holderless sweep, coverage in four ways, the run walk across

regions): 30,000 seeds, zero violations; 100,000 seeds, zero

@@ -4887,36 +5035,49 @@ 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.14 model (4ebfa0a5), with the strict classification,

+on the final rev 7.15 model (f6fb0579), 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 were not run for rev 7.14: the

-evidence policy of §14.2.1, Paul 2026-10-06; their columns say so); 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 57 rules that have them. A rule is caught

+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 **104 rules**: rev 7.13's 101 plus

-`persisted-park-scope` and `holderless-park` (claim rev 6.15, R13-4) and

-`covered-baseline-refused` (claim rev 6.22 §6.2a, R13-1). `mutate.sh 3000` exited 0: no ERROR, no unexpected

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

+`restore-selected-baseline` (R14-1) and `unique-declarations` (R14-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). **Every table below is

+(1f511c42); rev 7.14's in a4389280. **Every table below is

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

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

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

| | rules |

|---|---|

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

-| caught alone by the sweep at 30,000 (and by their witness, where one exists) | not run for rev 7.14 (CPU budget; 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.14 (CPU budget; Paul 2026-10-06) |

-| caught alone by their witness only; the sweep at 3,000 misses them | 21 (`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`, `seal-return`, `session-scoped-loss`) |

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

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

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

| unexercised | **0** |

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

+3 / 3,000 (the source's cut session declared twice,

+INV-21). The rules the scope and declaration changes touched:

+`persisted-park-scope` witness; sweep 0 / 3,000, `holderless-park`

+561 / 3,000, `covered-baseline-refused`

+witness; sweep 0 / 3,000, `writes-lost` 11 / 3,000,

+`lost-return-park` 1 / 3,000, `quiet-before-ack`

+132 / 3,000, `straggler-sweep` 778 / 3,000,

+`sweep-namespace` 542 / 3,000, `cover-at-park`

+29 / 3,000, `baseline-live` witness; sweep 0 / 3,000.

**What rev 7.14 moved.** The three new rules: `persisted-park-scope`

witness; sweep 0 / 3,000 (an agent restart mid-park starts the

horizon again from the restart's clock), `holderless-park`

@@ -5138,33 +5299,33 @@ witness to hold there; each witness violates with the failure it names.

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

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

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

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

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

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

@@ -5177,6 +5338,8 @@ witness to hold there; each witness violates with the failure it names.

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

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

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

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

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

@@ -5202,24 +5365,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: 90 of 104** (69 by the sweep at 3,000; 21 by their witness alone, marked ‡; the sweeps at 30,000 and 100,000 were not run for rev 7.14 (CPU budget; 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.15 (evidence policy; Paul 2026-10-06), so the one rare rule the sweep reaches only there, `hostguard`, has no verdict this round).

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

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

+| `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,632 / 3,000 |

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

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

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

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

@@ -5231,26 +5394,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,897 / 3,000 |

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

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

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

-| `return-stamp` | 69 / 3,000 | | `revalidate-before-effect` | 14 / 3,000 |

-| `revert-journal` | 13 / 3,000 | | `rollback-journal` | 1 / 3,000 |

-| `root-advance` | 17 / 3,000 | | `sdk-no-resign` | 12 / 3,000 |

-| `sign-before-safeuntil` | 15 / 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` | 13 / 3,000 |

-| `sweep-namespace` | 542 / 3,000 | | `sweep-staging` | 36 / 3,000 |

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

-| `timer-freeze` | 2 / 3,000 | | `valid-ltx` | 38 / 3,000 |

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

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

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

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

@@ -5265,19 +5429,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.14 (CPU budget; 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.14 (CPU budget; 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.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 |

| `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.14 (CPU budget; Paul 2026-10-06) | `fence-stamp` 306 / 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.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 |

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

@@ -5317,7 +5481,24 @@ baselines, this sweep and the witnesses are the evidence for rev 7.10.

identity (only one box writes staging, and a restarted agent's

goroutines die with it). Each could hide a fault; each is a next step,

in that order of likely yield.

-- **Timing is scaled, not real.** `H` (60 steps) is shorter than the cut

+- **Occupancy is by current objects (R14).** The model's run walk and

+ oracles judge a generation as holding an object by its **current**

+ versions in a region's bucket; a key whose every version was deleted

+ (a parked generation) counts as empty for selection and as "had

+ objects" only for INV-17 and the sweep's retired set. The selector F

+ also counts tombstoned or history-bearing generations as nonempty and

+ fails closed on them. The two agree on every case in F's table; a

+ generation with delete markers and no current version is where they

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

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

+ rather than entries until rev 7.15. The publication's precondition is

+ that any entry names the published generation, as A and E read it.

+- **Timing is scaled, not real.** `H` (60 steps, the signature-age

+ allowance 45 plus the request bound 15) is shorter than the cut

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

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

which window do not (J2 §2).

@@ -5697,6 +5878,23 @@ 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.

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

+`FreeAfterPark`; a create waits on the parking op; the covered-baseline

+refusal; a warm record's region). Notes for platform-1e

+(`moves-claim-questions.md`, rev 7.15 heading): **(1)** a staging park

+(`park-staging`, CC20, this spec's kind) binds a persisted scope before

+its first step like a whole-location park but keeps the seal's own

+quiet time, bounded by the staging lease, rather than `evidence_at +

+H`; **(2)** a generation chore's scope takes `evidence_at` from the

+publication that queues it, the marker's publication being the evidence

+that the predecessor is dead, so its horizon is the publication's time

+plus `H`, equal to the chore's queued quiet time; **(3)** the model

+decomposes `H` into a signature-age allowance and the request bound

+(45 + 15 steps) so the scope's `request_limit` has the claim's meaning;

+nothing in the claim need change.

**Claim rev 6.15 to 6.22 (0bf2f49f), after joint round 13: no change

requested, six notes.** Rev 6.15 and 6.16 added the persisted park scope

and the holderless sweep; rev 6.21 adopted rev 7.13's seven notes; rev

@@ -5712,7 +5910,10 @@ scoped chores under the same op id, rather than waiting for

`FreeAfterPark`; the claim's "one CAS queues only scoped remote chores

owned by that op" is read to allow later CASes adding to the op;

**(2)** the sweep's chore is acknowledged, with its straggler pass, only

-after the scope's `evidence_at + request_limit`, so a free host's

+after a verification listing later than `evidence_at + H`, `H` the

+signature-age limit plus `request_limit` (rev 7.14 wrote `evidence_at +

+request_limit` here and in §6.4, dropping the signature-age allowance,

+R14-3; platform-1e's answer confirmed the full `H`), so a free host's

successor create waits up to the horizon after the sweep found residue;

rev 7.13's sweep acknowledged at once; **(3)** the console's recovery

pass leaves a holderless sweep to the obligation runners and replays only

@@ -6224,6 +6425,22 @@ 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.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

+merge-ready, and held B on one P2 and C on two P2s and two P3s.

+Platform-1e agreed all six rev 7.14 notes.

+| finding | rev 7.15 |

+|---|---|

+| R14-1 (P2, C) the start could not restore an intermediate run generation the recovery oracle accepts (the marker names the run's baseline) | `openState.SourcePin` carries the walk's restore mode; the start restores a selected run generation rooted at `[1, 1]`, the marker's through `generation.json`, as the oracle does; rule `restore-selected-baseline`, witness `wIntermediateBaseline` (§5.1 step 9, §7.14 item 3) |

+| R14-2 (P2, C) the source-cut loss had a separate representation and could duplicate the ordinary declaration | one `writes_lost` plus `additional_writes_lost`, unique by `(box, session)`, the cut session under its persisted identity, one alert per declaration, INV-21; rule `unique-declarations`, witnesses before and after the target's first admission (§5.1 step 9, §7.14 item 2) |

+| R14-3 (P2, B) the persisted-scope acknowledgement formula dropped the signature-age allowance | `evidence_at + H`, `H` the signature-age limit plus `request_limit`; the scope persists `request_limit` (`parkScope.RequestLimit`), the model's `horizonH = sigAgeH + requestLimitH`; a park-sweep acknowledges only after a listing later than that (§6.4, §7.14 item 9, §19.4 note 2 corrected) |

+| R14-4 (P3, C) joining a running holderless sweep was unreachable | the sweep's outer guard admits the holderless state; `TestJoinHolderlessSweep` (§6.4) |

+| R14-5 (P3, C) not every remote chore had a persisted scope | generation chores take theirs from the publication, staging parks bind one before their first step; INV-22 (§6.4, §7.14 item 9) |

+| fidelity limits named by the review | occupancy by current objects stated in §14.2.6; trimming aligned with E's front-only rule over more than eight entries; the publication's precondition is any entry naming the generation |

+| E, F | MERGE-READY on f0127321 and d7621a29; nothing asked of them |

### 22.20 Joint round 13 (claim 1915bac2, moves rev 7.13 1f511c42, model 42af7bfc, library E 47426cc1, selector plan 85aa53f8)

Round 13 found no P1 and judged E merge-ready; it held A, B, C and F on