carlos / platform Public

spec: move-any-app rev 7.6: joint round 5, the pinned libraries observed, claim rev 6.4 encoded (#175)

Written against claim rev 6.4 (697f0f9f) and the facts
internal/sim/litestreamfacts established about litestream v0.5.14 and ltx
v0.5.1 as pinned.

R5-1: the level-0 anchor [N, N] at every install (§5.1 step 7, §7.6
building, §7.8); the -txid sidecar is follow-only.
R5-2: verification by what the format supplies: per-file CRC-64,
integrity_check, the required TXID, the gap refusal; no post-apply
checksum (§5.1 step 5); snapshot_checksum -> snapshot_crc64.
R5-3: snapshot rotation and retention; the root advances to the newest
current successor snapshot at or past the pinned one (§5.1 steps 4, 8).
R5-4: claim rev 6.3/6.4's stamp lifecycle (§6.4, §7.6, §7.8, §19.4):
holder.stamp, initialization under the guard, no record refuses, the
stamp captured at work selection, retire-artifacts moves no stamp,
activation and retire-installation do, a dirty rollback's new stamp with
holder.generation in one write.
R5-5: the sealed snapshot is built on the target from the staged replica
(§5.1 steps 1-2, §7.3 T11, §7.4, §7.6 building).
R5-6: the retention fixture; the pinned S3 layout
<prefix>/<4-hex level>/<min>-<max>.ltx; §14.2.6 points at litestreamfacts.
§14.2 rewritten for the rev 7.6 model: 77 rules, 32 witnesses, 30,000 and
100,000 seeds clean, the sweep's counts; §22.12 dispositions.

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

claude 3 weeks ago f7f7c43862c5da03dab7fe6edf8cf0b95f43632f parent 50b1e51

1 file changed, +620 −213

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

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 1cf1ffaa4..00a689154 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,46 @@

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

**Date:** 2026-10-03

-**Revision:** 7.5.

+**Revision:** 7.6.

+- **Rev 7.6** answers the moves side of **joint round 5**

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

+ **claim spec rev 6.4** (697f0f9f), which answers the claim side of

+ R5-4 (rev 6.3: `holder.stamp`, the record's initialization, two named

+ retirements; rev 6.4: the stamp captured at work selection,

+ `retire-artifacts` never moves a stamp, the legacy location's children);

+ §22.12 has every disposition. Round 5 found that rev 7.5

+ described the pinned libraries from their documentation; rev 7.6

+ starts from **their observed behaviour**: `internal/sim/litestreamfacts/`

+ drives litestream v0.5.14 and `superfly/ltx` v0.5.1 as pinned and

+ asserts each fact this spec relies on (§14.2.6). **R5-1 (P1):** a

+ snapshot-only install restarts replication at TXID 1 (fact R5-1a) and a

+ later cold restore loses the new writes (R5-1b); the install now writes

+ a **level-0 anchor** `[N, N]` beside the snapshot, which the pinned

+ open takes as its position (R5-1c, d); `-txid` is follow-only (R5-1e).

+ **R5-2:** the pinned writers set `HeaderFlagNoChecksum`, so there is no

+ post-apply checksum to compare; verification is what the format

+ supplies, the per-file CRC-64 trailer, plus SQLite's integrity check and

+ the required TXID (§5.1 step 5); the whole-state checksum is gone from

+ the model. **R5-3:** snapshot rotation and retention are specified and

+ modelled; the restore roots at the **newest current successor

+ snapshot** of the named generation at or past the pinned one, and only

+ at the pinned version when no successor is current (R5-3d, e). **R5-4:**

+ claim rev 6.4's stamp lifecycle, encoded exactly (§6.4): `holder.stamp`

+ written by every installing CAS, the local record initialized only from

+ a fresh read under the guard, no record refuses, `retire-artifacts`

+ against `retire-installation`, and a dirty rollback's install carries

+ its own stamp. **R5-5:** the sealed snapshot is **built on the target**

+ from the staged replica; T11 prices the final delta within the bar and

+ the target's restore, snapshot and anchor at the local rate, and

+ `budget_test.go` shows a 2 GiB database over 10 MiB/s admitted that

+ way and refused as a cross-region transfer (§7.3, §7.6). **R5-6:** the

+ retention fixture populates 2 to 33 and asserts the injected

+ incarnation absent. LTX keys follow the pinned S3 client's layout,

+ `<prefix>/<level, 4 hex>/<min>-<max>.ltx`. Two new rules, each with a

+ witness (`restore-anchor`, `root-advance`). Results: 30,000 and 100,000

+ seeds clean; 77 rules, 63 caught alone, 11 in stated combinations, 2

+ liveness, 1 unreachable, none unexercised (§14.2.3, §14.2.5).

- **Rev 7.5** answers the moves side of **joint round 4**

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

@@ -516,7 +555,16 @@ per push, and per dirty rollback. Each generation has its own key prefix:

| generation | replica objects |

|---|---|

| origin | `<location>` itself, the layout litestream writes today (`<location>ltx…`, a legacy host's existing objects) |

-| an operation `op` | `<location>g-<op id>/…`: the installed snapshot and every LTX object replicated on top of it |

+| an operation `op` | `<location>g-<op id>/…`: the installed snapshot, its anchor and every LTX object replicated on top of them |

+Within a generation prefix the objects are litestream's, in the layout

+the pinned S3 client writes (`s3/replica_client.go`, `ltx.FormatFilename`):

+`<prefix>/<level as four hex digits>/<MinTXID as sixteen hex digits>-<MaxTXID

+as sixteen hex digits>.ltx`, so a snapshot ending at TXID 7 is

+`0009/0000000000000001-0000000000000007.ltx` and a level-0 file for TXID 8

+is `0000/0000000000000008-0000000000000008.ltx`. Rev 7.5 wrote

+`ltx/<level>/`, which is not the layout (R5-6). Rev 7.6 writes the real

+one in this spec and in the model.

The claim names the current one, **`holder.generation`** (CC18): written

by the commit's claim CAS (§7.9), by a push's probe CAS (F7), and by a

@@ -533,65 +581,146 @@ are the state at `Max`, deletes the inputs, and so leaves overlapping

ranges and no individual intermediate objects. A snapshot ending at 100

with one current continuation `[91, 110]` is a healthy replica; rev 7.4

would have refused it, or restored through 100 and let a move commit

-without transactions 101 to 110. Rev 7.5 takes **one implementable

+without transactions 101 to 110. Rev 7.5 took **one implementable

contract: the sealed transfer is a verified final snapshot, and the

restore is litestream's own planner over that snapshot and the

-generation's later files**, exactly as `litestream` v0.5.14 and

-`superfly/ltx` v0.5.1, the versions this repository pins, behave.

-1. **The sealed transfer is a snapshot.** At the cut, after the final

- checkpoint, the source writes a snapshot of the stopped database: one

- LTX file at litestream's snapshot level (9), `MinTXID = 1`, `MaxTXID =

- N`, every page, with its `PostApplyChecksum`. It seals that object by

- key and `versionId` (`seal.db`, §7.4). Nothing else of the replica is

- transferred: not the level-0 and level-1 files, which the snapshot

- subsumes. `N` is the **required final TXID** of the transfer.

-2. **The install copies the snapshot into the generation**, by

- `versionId`, to `<location>g-<move id>/ltx/9/<1>-<N>.ltx` (litestream's

- layout under the generation prefix), verifying its size and its

- trailer checksum, and records in the install manifest the key, the

- `versionId` the copy created, `N` and the checksum (§7.6 `copying`).

+generation's later files**. Joint round 5 showed that rev 7.5 described

+`litestream` v0.5.14 and `superfly/ltx` v0.5.1, the versions this

+repository pins, from their documentation and got three things wrong

+(R5-1, R5-2, R5-3). Rev 7.6 writes the contract against the libraries'

+**observed** behaviour: `internal/sim/litestreamfacts/facts_test.go`

+drives the pinned libraries with the file replica client and asserts

+every fact cited below as "fact R5-n"; a library upgrade that changes one

+fails there first (§14.2.6).

+1. **The sealed transfer is the staged replica at the required final

+ TXID (R5-5).** At the cut, after the final checkpoint and

+ `SyncAndWait`, the source's replication position is `N`: the

+ `MaxTXID` of its newest level-0 file. The final mirror round

+ (`staged`, §7.4) copies the delta of the source's replica into

+ staging's `replica/`, within the 16 MiB bar, and the **seal** records

+ `N` and the exact `versionId` of every current LTX file under

+ `replica/`. Nothing larger crosses the region boundary at the cut: rev

+ 7.5 shipped a whole snapshot of the stopped database after the stop,

+ which a 2 GiB database over a 10 MiB/s path cannot do in a 120 s

+ window, while T11 priced only the 16 MiB delta (R5-5). `N` is the

+ **required final TXID** of the transfer.

+2. **The target builds the generation's snapshot from the staged

+ replica** (§7.6 `building`). It restores the sealed versions with the

+ planner of step 4, in its own region, verifying each file's trailer

+ (`ltx.Decoder.Verify`: the CRC-64 `FileChecksum`), and requires the

+ result to reach exactly `N` and to pass `PRAGMA integrity_check`.

+ From that database it writes two files into the move's own

+ generation: the **snapshot**, one level-9 LTX file `[1, N]`, every

+ page, at `<location>g-<move id>/0009/<1>-<N>.ltx`; and the **anchor**

+ (step 7), one level-0 LTX file `[N, N]`, every page, at

+ `<location>g-<move id>/0000/<N>-<N>.ltx`. Both are written as the

+ pinned writers write theirs: `HeaderFlagNoChecksum` set, pre- and

+ post-apply checksums zero, the trailer's CRC-64 present (fact R5-2);

+ the anchor's `WALOffset` is the WAL header size, which `Verify`

+ requires (fact R5-1c). The install manifest records the snapshot's

+ key, the `versionId` the PUT returned, `N` and its CRC-64. The cost is

+ three passes over the database at the local rate, which T11 prices

+ (§7.3).

3. **`generation.json` names the snapshot**: `snapshot_key`,

- `snapshot_version`, `snapshot_txid = N`, `snapshot_checksum`. These

- are the snapshot identity; a second `base` version under the

- generation, from a copy that completed late, is never read.

+ `snapshot_version`, `snapshot_txid = N`, `snapshot_crc64`. These are

+ the snapshot identity: the **pinned root**. A second version under the

+ same key, from a PUT that completed late, is identical bytes and is

+ never read.

4. **The restore is litestream's planner** (`replica.go`

- `CalcRestorePlan`), with one substitution: the snapshot it starts from

- is the one `generation.json` names, opened by `versionId`, not "the

- latest snapshot under the prefix". From `current = N` it takes, among

- the generation's current files at every level, the file with

- `MinTXID ≤ current + 1` and `MaxTXID > current` (overlap allowed:

- `ltx.IsContiguous`), preferring the highest `MaxTXID`, then the lowest

- `MinTXID`, then the higher level, applies it, sets `current =

- MaxTXID`, and repeats until nothing extends the range. A compacted

+ `CalcRestorePlan`, v0.5.14), rooted in the named generation and

+ nowhere else. Its **root** is the newest current level-9 file of the

+ generation whose `MaxTXID ≥ snapshot_txid` (a **verified successor

+ snapshot**, step 8), or, when no such file is current, the pinned

+ snapshot opened by `snapshot_version`. From `current = root.MaxTXID` it

+ takes, among the generation's current files at levels 0 to 8, the

+ file with `MinTXID ≤ current + 1` and `MaxTXID > current` (overlap

+ allowed: `ltx.IsContiguous`), preferring the highest `MaxTXID`, then

+ the lowest `MinTXID`, then the higher level, applies it, sets `current

+ = MaxTXID`, and repeats until nothing extends the range. A compacted

`[91, 110]` over a snapshot at 100 is taken: its pages are the state

at 110, so applying them over the state at 100 is exact. Files are

taken from the current listing, as litestream lists them; nothing

- reads noncurrent LTX versions, because compaction's deletes make the

- superseded files noncurrent on purpose.

-5. **Fail closed.** The restore refuses, with a member-safe reason and a

- page, and never produces a database, when: the snapshot version is

- missing or its `MaxTXID` is not `snapshot_txid`; a current file starts

- beyond `current + 1` once nothing extends the range (litestream's

- "non-contiguous ltx files": a gap); or the database checksum after the

- last applied file is not that file's `PostApplyChecksum`. "Compare

- content at those TXIDs" is gone: compacted objects do not retain

- intermediate states, and the checksum is the validation LTX provides.

- A restore that falls short of `snapshot_txid` is a refusal, not a

- result.

+ reads noncurrent LTX versions, because compaction's and retention's

+ deletes make the superseded files noncurrent on purpose. Rev 7.5 said

+ "every level" and rooted at the pinned snapshot for good; after

+ retention that root has no continuation (fact R5-3d) and the restore

+ would have refused a healthy replica (R5-3).

+5. **Fail closed, by what the format supplies (R5-2).** The pinned level-0

+ writer, snapshot writer and compactor all set `HeaderFlagNoChecksum`;

+ `PreApplyChecksum` and `PostApplyChecksum` are zero in every file, and

+ `ltx.Trailer.Validate` requires them to be with that flag (fact R5-2,

+ litestream `db.go:1948`, `db.go:2412`, ltx `compactor.go`). There is no

+ database checksum to compare after applying a file; rev 7.5's step 5

+ would have refused every healthy continuation, or been skipped. What

+ the format supplies is **per-file integrity**: the trailer's CRC-64

+ over the file, which `Decoder.Verify` checks, and which SQLite's own

+ `PRAGMA integrity_check` (`CheckDB`, `backend_exec.go:313`) complements

+ over the result. The restore refuses, with a member-safe reason and a

+ page, and never produces a database, when: no root is current and the

+ pinned version is missing or its `MaxTXID` is not `snapshot_txid`; a

+ file fails `Verify`; a current file starts beyond `current + 1` once

+ nothing extends the range (litestream's "non-contiguous ltx files": a

+ gap); the result fails `integrity_check`; or, at an install, the

+ result is not at the required final TXID. End-state checksums would

+ need the three writers changed; Phase 1 does not change them, and the

+ model carries none (§14.2.2).

6. **What a gap means.** Litestream does not advance past a failed

- upload, and a timed-out upload is retried before the next range, so a

- gap in a generation's current listing is a lost or not-yet-landed

- object, never a healthy replica. The refusal holds until the object

- lands, or pages an operator.

+ upload, and a timed-out upload is retried with the same bytes before

+ the next range, so a gap in a generation's current listing is a lost

+ or not-yet-landed object, never a healthy replica. The refusal holds

+ until the object lands, or pages an operator.

+7. **The anchor: restore-to-replication initialization (R5-1).**

+ Litestream's open (`db.go` `checkDatabaseBehindReplica`) takes a fresh

+ box's replication position from the **newest remote level-0 file**; a

+ `<db>-txid` sidecar is read in follow mode only (fact R5-1e). A

+ generation holding a snapshot and nothing at level 0 therefore starts

+ replication at TXID 1: the first upload is `[1, 1]` (fact R5-1a), later

+ writes land below `N`, and a cold restore rooted at `N` skips them and

+ loses every write since the install (fact R5-1b; the R5-1

+ counterexample, confirmed). The remedy the pinned library supports

+ unchanged is the **anchor** of step 2: a level-0 file `[N, N]` with

+ every page, beside the snapshot. The open takes `N` as its position,

+ the local WAL does not match it, and the next sync is a full upload at

+ `N + 1` (fact R5-1c); a cold restore afterwards holds every row (fact

+ R5-1d). Every install of a generation writes its anchor before any

+ process may open the database: a landing (§7.6 `building`), a push's

+ install, a dirty rollback's install on the source (§7.8). A **cold

+ restore of a replica that has replicated since needs no anchor**: the

+ newest level-0 file is never removed by TXID- or time-based retention

+ (fact R5-1f), so a fresh box continues at `N + 1` (facts R5-1g, h). The

+ wake writes one anyway whenever the restored TXID is above the newest

+ current level-0 file, which costs nothing when it is not (the model's

+ `restore-anchor`).

+8. **Rotation, retention and root advancement (R5-3).** Litestream writes

+ a new snapshot `[1, P]` at its snapshot interval, and

+ `EnforceSnapshotRetention` keeps the newest, returning

+ `minSnapshotTXID` = the `MaxTXID` of the snapshot before the oldest

+ kept one; the store then expires every level-1 and higher file whose

+ `MaxTXID` is below it, and level 0 by time (fact R5-3a, b). After two

+ rotations no current file continues from the pinned snapshot (fact

+ R5-3f): a restore rooted there fails with "non-contiguous ltx files:

+ have up to 1 but next file starts at 5" (fact R5-3d) while a restore

+ from the newest snapshot holds every row (fact R5-3e). Protecting the

+ pinned version alone does not protect its continuation; **the root

+ advances**. A **verified successor snapshot** is a current level-9

+ file of the named generation with `MaxTXID ≥ snapshot_txid` that

+ passes `Verify`; only the generation's own replicator writes under its

+ prefix (C3a, and the generation name is the operation's), and a

+ stale re-upload of a rotated snapshot is identical bytes under the

+ same key, so the newest current one is the one litestream itself

+ restores from. `generation.json` is not rewritten at rotation: the

+ pinned root is the install's identity and the floor the successor must

+ clear, not the only root (step 4). The sweep protects every current

+ version under `holder.generation` and the pinned version (§6.4).

So:

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

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

- version, never opened); a late LTX PUT from an old executor lands in a

- generation the claim no longer names. Neither is ever restored into the

- current state;

+ generation. A late snapshot or anchor PUT repeats identical bytes

+ (another version, never opened); a late LTX PUT from an old executor

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

+ restored into the current state;

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

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

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

@@ -599,35 +728,51 @@ So:

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

delegates to `Replica.Restore`, whose planner lists each level without

-versions and opens LTX files by key. Phase 1 needs two changes there: the

-snapshot opened by the `versionId` `generation.json` names, and the plan

-rooted at that snapshot rather than the latest one listed. The rest of

-the planner, overlap rule, preference order and the non-contiguous error

-included, is used as it is. The repository's compaction ladder

-(`lease.go:55`: levels 0 to 3) is what produces the overlapping ranges

-step 4 handles. §15 step 8 verifies the S3 behaviour (claim §13 rows 2,

+versions and opens LTX files by key. Phase 1 needs three things beside

+it, none a change to the pinned library: the root rule of step 4 (the

+newest current successor snapshot of the named generation, else the

+pinned version opened by `versionId`, never another generation's or

+"the latest under the location"); the builder of step 2 (restore the

+staged versions, write the snapshot and the anchor with `ltx.NewEncoder`

+as `litestreamfacts` does); and the wake's anchor check of step 7. The

+rest of the planner, overlap rule, preference order and the

+non-contiguous error included, is used as it is. The repository's

+compaction ladder (`lease.go:55`: levels 0 to 3) is what produces the

+overlapping ranges step 4 handles. `internal/sim/litestreamfacts/`

+verifies the library behaviour this section relies on (facts R5-1 to

+R5-3, §14.2.6); §15 step 8 verified the S3 behaviour (claim §13 rows 2,

3 and 10).

-**In the model** (§14.2.2) a database is a map of keys to values;

-transactions insert, update and delete; an LTX file carries its range,

-the final image of every key it touches and the checksum after `Max`;

-compaction merges three level-0 files into a level-1 file and deletes the

-inputs; a snapshot is the file `[1, TX]` with every page. The restore is

-step 4 and step 5 as written. The model drops the contract

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

-loses acknowledged writes; it drops the overlap rule (`restore-overlap`:

-rev 7.4's `min == current + 1`) and loses a compacted continuation; it

-drops the gap refusal (`restore-gap-closed`) and wakes a host without

-durable transactions (§14.2.5). Rev 7.4's model carried a full

-transaction history in every object, which no LTX file has, and so could

-not show any of this (R4-1).

+**In the model** (§14.2.2) a database is a map of keys to values with

+a lineage TXID and, separately, a **replication position**; transactions

+insert, update and delete; an LTX file carries its level, its range in

+replication numbering and the final image of every key it touches, and

+no checksum (R5-2); the serving process ships one level-0 file per sync

+at `position + 1`; compaction merges three level-0 files into a level-1

+file and deletes the inputs, then rotates a snapshot `[1, position]` and

+enforces retention as step 8 states (R5-3). The restore is steps 4, 5, 7

+and 8 as written: the root is the newest current successor snapshot at

+or past the pinned one, the position is read from the newest current

+level-0 file, and the anchor is written when the restored TXID is above

+it. The model drops the contract (`restore-by-generation`: the newest

+object under the location) and loses acknowledged writes; it drops the

+overlap rule (`restore-overlap`: rev 7.4's `min == current + 1`) and

+loses a compacted continuation; it drops the gap refusal

+(`restore-gap-closed`) and wakes a host without durable transactions; it

+drops the anchor (`restore-anchor`) and a snapshot-only install that

+wrote, replicated and lost its disk loses every write since the push;

+it drops root advancement (`root-advance`) and a host whose replica

+rotated four times refuses to wake (§14.2.5). Rev 7.4's model carried a

+full transaction history in every object, which no LTX file has; rev

+7.5's carried a whole-state checksum no pinned file has and a position

+that litestream never derives from a snapshot (R5-1, R5-2).

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

field.

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

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

+| `generation.json` | `<location>generation.json`, beside `lock.json` | **last**, after the install manifest is complete and verified (§7.6); **conditionally**: If-Match the marker it supersedes, or If-None-Match when there is none (model 29) | `{"op","incarnation","host","box","installed_at","manifest_sha256","snapshot_key","snapshot_version","snapshot_txid","snapshot_crc64"}`: the pinned root, the install's snapshot identity and the floor a successor snapshot must clear (R3-1, R4-1, R5-3) |

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

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

@@ -646,10 +791,11 @@ content digest, and from F4's definition of the files directory (§6.1).

Absent everywhere means origin. The claim's `gen` is a per-write version

(claim spec §2), not a generation, so it never appears in a marker.

-**The authoritative region (claim rev 6.2 §6.2a, R4-3).** The live set is

+**The authoritative region (claim rev 6.4 §6.2a, R4-3).** The live set is

`{authoritative region, holder.location, holder.generation}` plus the

versions this spec names for the generation (the snapshot version in

-`generation.json`, noncurrent included). Objects of the generation are

+`generation.json`, noncurrent included; every current version under the

+generation, successor snapshots and anchors among them). Objects of the generation are

live only in the authoritative region's bucket; a matching key in any

other region is residue, and the sweep parks it. The authoritative region

is the region of the holder's current installation:

@@ -891,32 +1037,70 @@ Phase 1 uses the claim spec's park (§6.2 there) and local retirement

the same obligation, and the verification repeats.

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

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

- refused. **Installation stamps** (claim rev 6.2 §6.4, R3-3, R4-2): an

- installation's stamp is the claim `gen` captured at the CAS that made it

- current on this box (a create's serving CAS, a landing's flip), kept

- for as long as the installation exists, serving included. Each box

- keeps, under the guard, a record per host incarnation:

- `{active_stamp | none, retired_stamps}`. Every host-state writer

- (config sync, release adoption, the activator's admission) carries

- `{incarnation, stamp}` from the record it read under the guard when it

- selected its work, and is admitted only if its stamp **equals** the

- active stamp; a lower stamp, a retired stamp, or any stamp while the

- active stamp is `none` is refused. Retirement moves the active stamp

- into the retired set and sets `none`. A new installation of the same

- incarnation, a move back to a region the instance left, sets the active

- stamp to its own captured stamp in the landing's `checking` phase, under

- the guard, after a fresh claim read shows its operation current and

- this box the landing participant. Op ids are opaque and never compared

- (claim rev 6.2 Q1). Rev 7.4's marker compared operations by an order

- the production system does not have and admitted its own installation

- only by a `- 1` in the model (R4-2); rev 7.3's marker fenced the whole

- incarnation, and the move back never passed its probe. The model keeps

- the stamp record exactly as claim rev 6.2 states it, requires the

- UK→US→UK round trip to serve on UK again unmutated, records a landing

- probe refused by its own installation record as a violation, and shows

- a stale config pass admitted across a retire-and-reinstall only when

- the stamp check and the host guard's fresh check are both gone

- (§14.2.5, `fence-by-installation`, `fence-stamp`).

+ refused. **Installation stamps** (claim rev 6.4 §6.4, R3-3, R4-2,

+ R5-4): an installation's stamp is the claim `gen` produced by the CAS

+ that made it current, and **that CAS writes it into `holder.stamp`**

+ (claim rev 6.4 §2), so the claim is the durable record of every

+ installation's stamp and the recovery source for every box. The CASes

+ that install, and so write `holder.stamp`, are: a create's serving CAS

+ (claim §5.1 step 4); adoption (claim §9); a landing's flip (§7.5); a

+ push's probe CAS (F7); a dirty rollback's source probe CAS (§7.8); a

+ reinstall after quarantine. A dirty rollback installs a new generation

+ and **never keeps its predecessor's stamp** (rev 7.5's model did,

+ R5-4). The stamp is kept for as long as the installation exists,

+ serving included. Each box keeps, under the guard, a record per host

+ incarnation: `{active_stamp | none, retired_stamps}`. **Initialization

+ (claim rev 6.4 §6.4):** a box creates or refreshes its record only from

+ a fresh claim read under the guard, only when that read names it

+ `op.exec` or the landing participant (the phase table, §5.1), setting

+ `active_stamp = holder.stamp`: a create's first wake, adoption on the

+ serving box after the adoption CAS, a landing in its `checking` phase,

+ a box whose record was lost, on restart. Rev 7.5's model initialized

+ the record from the claim revision at reconciliation, which

+ intervening claim writes change (R5-4). **No local record: refuse.**

+ Every host-state writer (config sync, release adoption, the

+ activator's admission) carries `{incarnation, stamp}` **captured from

+ the box's local record when it selected its work** (claim rev 6.4's

+ answer 1: the fresh claim read under the guard is still required, for

+ the incarnation, the operation and the config and release identity,

+ but the stamp is the selection's), and is admitted only if its stamp

+ **equals** the active stamp; a lower stamp, a retired

+ stamp, any stamp while the active stamp is `none`, and any stamp while

+ the box has no record, are refused (rev 7.5's model admitted a writer

+ when no record existed, R5-4). **Two retirements, named at every

+ call** (claim rev 6.4 §6.4): `retire-artifacts(S)` parks the local

+ artifacts tagged with stamp `S` and **moves no stamp**: neither

+ `active_stamp` nor `retired_stamps` changes (rev 6.3 had it add `S` to

+ the retired set; rev 6.4's answer 2 withdraws that). It is what a

+ landing that has activated its own stamp in `checking` uses in `local`

+ to park its predecessor's database, files and `<host>.env`, what the

+ activator uses on a warm database from an earlier stay, and what a

+ dirty rollback's install uses on the source, whose pre-move stamp is

+ still active at that point. Only two things move a stamp:

+ **activation**, which puts the old `active_stamp`, if any, into

+ `retired_stamps` and then sets the new one (so the dirty rollback's

+ pre-move stamp retires when its probe CAS's new stamp activates), and

+ `retire-installation`, which moves `active_stamp` into

+ `retired_stamps`, sets `none` and parks every artifact; it is the local

+ park at a delete, a move away (the source's finalization, §7.9), a

+ rolled-back target's `cleaning` and quarantine (CC12). Nothing calls

+ `retire-installation` to clean up a predecessor: rev 7.5's §7.6

+ reused the general local park in `local`, which read literally retires

+ the installation `checking` had just activated and refuses its own

+ probe (R5-4). Op ids are opaque and never compared (claim rev 6.1 Q1).

+ Rev 7.4's marker compared operations by an order the production system

+ does not have and admitted its own installation only by a `- 1` in the

+ model (R4-2); rev 7.3's marker fenced the whole incarnation, and the

+ move back never passed its probe. The model keeps the stamp record

+ exactly as claim rev 6.4 states it (every installing CAS writes

+ `holder.stamp`, `initRecord` under the guard, refusal without a record,

+ activation the only move of the old stamp, `retire-artifacts` a named

+ no-op on the record), requires the UK→US→UK round

+ trip to serve on UK again unmutated, records a landing probe refused by

+ its own installation record as a violation, and shows a stale config

+ pass admitted across a retire-and-reinstall only when the stamp check

+ and the host guard's fresh check are both gone (§14.2.5,

+ `fence-by-installation`, `fence-stamp`).

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

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

@@ -940,10 +1124,19 @@ residue unless it is `holder.location`; a level directory directly under

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

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

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

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

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

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

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

protected in the authoritative region's bucket only (the table in §5.1);

+within `holder.generation` every current version is live, the successor

+snapshots and the anchor among them (§5.1 steps 7 and 8); and, in claim

+rev 6.4 §6.2a's words, **a child prefix that is not an incarnation id

+(64 hex) belongs to the host prefix's own location**: a level directory

+`0000` to `0009` or a generation prefix `g-<op id>/` directly under the

+host prefix is the legacy location's, never an incarnation location (the

+model's `locationOf`; rev 7.6's first baseline misread `g-<op>/` under a

+legacy host as an incarnation and swept the live generation, caught in 2

+seeds of 3,000);

a matching key in any other region is residue and is parked, so a

replica PUT for a legacy host serving in UK that lands in US after US's

retirement is parked, not exempted. Claim §6.2a owns the sweep-side rule:

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

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

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

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

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

+| T11 budget | the **whole** stop-to-open estimate fits the operator's cut window (default 120 s) (codex R2-10, M11), from measured rates: stop + final checkpoint and `SyncAndWait` + final mirror (at most the 16 MiB bar at the measured cross-region copy rate) + archive build and upload + **the target's build (§7.6 `building`, R5-5): the restore of the staged replica, the snapshot write and the anchor write, each the whole database at the measured local rate** + render + **the probe attempts the window permits, each with its own settle** + the open (`open_budget`, 5 s) (joint N15, J2-N15). Rev 7.5 made the sealed transfer a snapshot of the stopped database and still priced the cross-region copy at the 16 MiB bar: a 2 GiB database over a 10 MiB/s path needs about 205 s for that copy alone, so T11 admitted a move the deadline then rolled back (R5-5). Rev 7.6 keeps the delta within the bar and builds the snapshot on the target (§5.1 steps 1 and 2), and `budget_test.go` shows that database admitted with one attempt at 50 MiB/s local, and the cross-region snapshot transfer refused by the same arithmetic. **The permitted attempts depend on the budget (R3-7):** `attempts = min(3, floor((window − everything else) / (30 s + 20 s)))`, and the instance is eligible only if that is at least one; the probe loop (§7.7) runs at most that many. Rev 7.3 required all three attempts to fit, 150 s of probing against a 120 s default window, so no default move was ever eligible; `budget_test.go` (§14.2) states the arithmetic and shows a tiny instance admitted with two attempts, the boundary at 70 s of fixed costs, and never more than three. The estimate is recorded per phase as `cut_budget_s`, and admission sets an absolute `cut_deadline` (§7.4) |

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

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

@@ -1156,8 +1349,8 @@ Each phase is written to `cut_phase` before its side effects.

| `admitted` | source CAS, stamping `cut_at` | **only if** the report and source readiness are fresh **and** every pinned input version (`move.inputs`) still matches the current bundle etags, overlay etag, release and launch report; otherwise CAS back to `ready` so the checks rerun (codex R2-8) | abort is legal until `admitted` and refused after; both CAS the same field |

-| `stopped` | source | read `Replication` and `NextDue`; snapshot the timers rows to `move-snapshots/<host>/<move id>/timers.json` **and** `…/timers/` in staging; write `stopped-source.json`; CAS the claim's execution holder to `none` (§19 K3) | |

+| `stopped` | source | final checkpoint and `SyncAndWait`, so the replica holds every acknowledged transaction; record the **required final TXID** `N`, the `MaxTXID` of the newest level-0 file (§5.1 step 1); read `Replication` and `NextDue`; snapshot the timers rows to `move-snapshots/<host>/<move id>/timers.json` **and** `…/timers/` in staging; write `stopped-source.json` with `N`; CAS the claim's execution holder to `none` (§19 K3) | |

+| `staged` | source | byte-final mirror round into `replica/`, within the bar; the **seal**: `N` and the `versionId` of every current LTX file under `replica/`, of `files/…` and `timers/…`, in the op journal (§7.3) | 3 deferred rounds or its budget: `reverting` |

| `archived` | source | build the final archive from the stopped directory, seal, write create-only to `move-snapshots/`, record both digests, copy into `files/` | over the cap, a special file, or its budget: `reverting` |

| `flipped` | source, the flip CAS | `region = to`, `state = landing`, `landing_deadline`; and the claim: `op.kind = landing`, execution holder = target (§19 K4) | |

@@ -1262,13 +1455,13 @@ journaled in `<DataDir>/.moves/<host>/<move id>/` (F12).

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

-| `checking` | read `stopped-source.json`; require the claim's `op.kind = landing` with this move id and execution holder = this box; require this box in `touched.boxes` (CAS-add before any local write); read `move.json` and require its incarnation; acquire the lease on `instances/<host>/` in its own bucket (claim spec C3) and hold it through `published` | | replayable |

+| `checking` | read `stopped-source.json`; require the claim's `op.kind = landing` with this move id and execution holder = this box; require this box in `touched.boxes` (CAS-add before any local write); read `move.json` and require its incarnation; under the host guard, from that fresh read, set the local record's `active_stamp = holder.stamp`, the stamp the flip CAS wrote (claim rev 6.4 §6.4, §6.4 here); acquire the lease on `instances/<host>/` in its own bucket (claim spec C3) and hold it through `published` | | replayable |

| `parking` | bucket-park whatever is at `holder.location` in its own bucket into `superseded/<move id>/<host>/` (an earlier stay of this incarnation) | the park manifest exists **and** its deletion set is deleted | replayable by the claim's rule (manifest present: replay the deletion set) |

-| `copying` | copy the **sealed snapshot** (`seal.db`: one level-9 LTX file `[1, N]`, by `versionId`, §5.1 step 1) into this move's own generation at `<location>g-<move id>/ltx/9/<1>-<N>.ltx`, verifying its size and trailer checksum; then write the install manifest `<location>g-<move id>/install.json` with the snapshot's key, the `versionId` the copy created, `N` and the checksum (R4-1) | the install manifest exists | replayable: staging is immutable after the flip, the generation is new, and the copy never deletes. A copy that completes late lands in this generation again as another version, which nothing reads (§5.1) |

-| `published` | write `<location>generation.json` with op, incarnation, the install manifest's sha256 and the snapshot identity: `snapshot_key`, `snapshot_version`, `snapshot_txid`, `snapshot_checksum` (§5.1) | `generation.json` names this move | replayable |

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

+| `building` | **build the generation from the staged replica** (§5.1 step 2, R5-5): restore the sealed versions under `replica/` with the planner into the generation's database file, verifying each file's CRC-64 trailer, requiring exactly `N` and `PRAGMA integrity_check`; write the **snapshot** `[1, N]` to `<location>g-<move id>/0009/<1>-<N>.ltx` and the **anchor** `[N, N]` to `<location>g-<move id>/0000/<N>-<N>.ltx` (§5.1 step 7); then write the install manifest `<location>g-<move id>/install.json` with the snapshot's key, the `versionId` its PUT returned, `N` and its CRC-64 (R4-1, R5-1, R5-2) | the install manifest exists | replayable: staging is immutable after the flip, the generation is new, and the build never deletes. A PUT that completes late lands in this generation again as another version of identical bytes, which nothing reads (§5.1) |

+| `published` | write `<location>generation.json` with op, incarnation, the install manifest's sha256 and the snapshot identity: `snapshot_key`, `snapshot_version`, `snapshot_txid`, `snapshot_crc64` (§5.1) | `generation.json` names this move | replayable |

+| `local` | `retire-artifacts` (claim rev 6.4 §6.4, §6.4 here: never `retire-installation`, which would retire the stamp `checking` activated) any warm database (with `<dbPath>.gen`), files directory and `<host>.env` of an earlier stay into `.parked/superseded-<move id>/`; extract the archive's files; write `<host>.env` from the archive; `ReplaceTimers` from the snapshot (§9.4); set `Replication` and `NextDue`; remove the host's restore-verification entry (§6.3); fsync all; **then** write `.files-gen` | `.files-gen` names this op and incarnation, and the journal records each sub-step | each sub-step is idempotent and journaled; `.files-gen` is written last, so its presence vouches for all of them (codex R2-6) |

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

-| `restored` | restore cold from `holder.location`, generation `<move id>` (the restore contract, §5.1: the planner from the named snapshot, which at install is the snapshot alone and must reach `snapshot_txid`, or the phase fails and rolls back), write `<dbPath>.gen`, `CheckDB` (`backend_exec.go:313`), record `landing.installed_db_sha256` | | replayable until `probing` |

+| `restored` | restore cold from `holder.location`, generation `<move id>` (the restore contract, §5.1: the planner from the named snapshot, which at install is the snapshot and its anchor and must reach `snapshot_txid`, or the phase fails and rolls back; the anchor is present, so litestream's open starts replication at `N + 1`, §5.1 step 7), write `<dbPath>.gen`, `CheckDB` (`backend_exec.go:313`), record `landing.installed_db_sha256` | | replayable until `probing` |

@@ -1333,7 +1526,7 @@ held** (§9.6, §19 K9): the target row is not retired by the region change

|---|---|

| `releasing` | row `releasing` with `hold_op = rollback id`; `ReconstructStopEvidence` |

| `released` | digests after a final checkpoint: database sha256, files plaintext, timers. **Clean** when all three equal what was installed (`landing.installed_db_sha256`, `source.files.plain`, `source.timers_sha256`) or `landing_phase` never reached `probing`; otherwise **dirty**. Write `stopped-target.json`; CAS the claim's execution holder to `none` |

-| `returning` (dirty only) | the handoff back: write a snapshot of its stopped database (one level-9 LTX file `[1, N']`, §5.1 step 1) into the source bucket's `moves/<host>/<rollback id>/db`, seal it by `versionId`, publish its files archive and timers snapshot under `files/` and `timers/`, write `move.json` |

+| `returning` (dirty only) | the handoff back: after a final checkpoint and `SyncAndWait`, write a snapshot of its stopped database (one level-9 LTX file `[1, N']`, every page, as the pinned writers write it, §5.1 step 2) into the source bucket's `moves/<host>/<rollback id>/replica/0009/<1>-<N'>.ltx`, seal it by `versionId` with `N'`, publish its files archive and timers snapshot under `files/` and `timers/`, write `move.json`. The return is under the release deadline (15 min), not the cut window, so the whole snapshot crosses the region here |

| `returned` (dirty only) | every artifact published |

| `cleaning` | only after the source records `recovered_at` (below): **bucket-park its `instances/<host>/` and its staging `moves/<host>/<move id>/` into `superseded/<move id>/<host>/`**, local-park its database, `<dbPath>.gen`, files and `<host>.env`, delete its row (conditional on `hold_op = rollback id`), clear its timers rows |

| `cleaned` | CAS `rollback.target_parked_at` |

@@ -1352,9 +1545,9 @@ because, until then, a source failure might need the target's state again.

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

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

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

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

+| dirty: `parking`, `building`, `published`, `local`, `configured`, `restored` | the target's install phases of §7.6, on the source, from `moves/<host>/<rollback id>/` (`building` restores the returned snapshot, requires `N'`, and writes the rollback generation's snapshot and anchor), with destination `superseded/<rollback id>/<host>/` for what it supersedes, **with two differences: `configured` and the release materialization run on the inputs the source renders now, recorded as `recovery.inputs`, and are never gated on `move.inputs`** (§7.7, J2-R2-5); and the stamps: the install runs under the source's pre-move installation, whose stamp stays active; `local` runs `retire-artifacts` on the pre-move database, tagged with that stamp, which moves no stamp; the `probed` CAS below, which names the return generation in `holder.generation`, writes a **new `holder.stamp`** in the same write, and the source's record activates it from a fresh read under the guard before the open, retiring the pre-move stamp then (claim rev 6.4 §6.4 and its answer 2: a dirty rollback installs a new generation and never keeps its predecessor's stamp, R5-4; rev 7.5's model kept it). Rev 7.3 said "exactly" and so inherited the landing's `configured` gate: a bundle published after admission, a target that wrote, and a dirty rollback would then have failed before the recovery probe (R2-5). The model's `recovery-current-inputs` witness is that case (§14.2.5) | as §7.6 |

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

-| `probed` | | |

+| `probed` | dirty: the claim CAS that names the return generation (`holder.generation = <rollback id>`, §5.1) and writes `holder.stamp`, the return installation's stamp, in one write (claim rev 6.4 §2, §6.4) | |

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

| `opened` | the conditional open on `hold_op = rollback id`; CAS `rollback.opened_at` | |

@@ -1813,6 +2006,20 @@ 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).

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

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

+`superfly/ltx` v0.5.1 as this repository pins them, with the file replica

+client the lease tests use, and asserts every library fact §5.1 cites as

+"fact R5-n" (replication position after a snapshot-only install and with

+the anchor, `-txid` follow-only, level-0 retention, the checksum flags,

+snapshot rotation and retention, the rooted-restore gap). It needs no

+S3. A library upgrade that changes a fact fails there before it reaches

+the model or the spec:

+```

+go test ./internal/sim/litestreamfacts/ # about 4 s

+```

#### 14.2.2 What it models

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

@@ -2126,6 +2333,94 @@ readiness, and same-operation lease identities.

fencing only; the purge journal's phases; `RenderHeld` and

`MaterializeHeld` before every probe.

+**Rev 7.6: joint round 5, the pinned libraries and claim rev 6.4.**

+- **Replication position and lineage are separate (R5-1, `ltx_test.go`).**

+ A database has a lineage TXID (the oracle's) and a replication

+ position `Pos`, litestream's TXID numbering in the generation: the

+ serving process ships one level-0 file `[Pos + 1, Pos + 1]` per sync

+ (full pages at position 0, as litestream's first sync is), and the

+ position advances as the upload is issued, because a timed-out upload

+ is retried with the same bytes and the next write takes the next TXID.

+ A cold restore reads its position from the newest current level-0 file

+ of the generation (`db.go` `checkDatabaseBehindReplica`), which is 0

+ for a snapshot-only install; when the restored TXID is above it, the

+ restore writes the **anchor** `[cur, cur]` with every page before the

+ database may be opened (`restore-anchor`, §5.1 step 7). The model's

+ seal ships the pending writes first (`SyncAndWait`), so the snapshot is

+ at the position. The mutation leaves the position where litestream's

+ open finds it, and the witness (a push's snapshot-only install, three

+ writes replicated, the disk lost, a cold wake) loses every write since

+ the push: INV-2.

+- **No whole-state checksum (R5-2).** An LTX file carries its level, its

+ range and the final image of every key it touches, nothing else: the

+ pinned writers set `HeaderFlagNoChecksum` (fact R5-2). The oracle's

+ state comparison and the planner's gap refusal are the model's whole

+ verification, as §5.1 step 5's per-file CRC-64 and `integrity_check`

+ are the implementation's.

+- **Snapshot rotation and retention (R5-3).** A compaction (three current

+ level-0 files into one level-1 file, inputs deleted) is followed by a

+ snapshot `[1, Pos]` when the position has moved past the newest

+ snapshot, then retention: every older snapshot is deleted, and level-1

+ and level-0 files whose `Max` is below the previous snapshot's `Max`

+ (litestream's `minSnapshotTXID`) are deleted, all by key, so the

+ versions stay noncurrent. The restore roots at the newest current

+ snapshot of the generation at or past the pinned one (`root-advance`),

+ and at the pinned version only when none is current; the origin

+ generation, which has no pinned snapshot, roots at its newest snapshot

+ as litestream does. The mutation roots at the pinned snapshot for good;

+ the witness (a push, then four rotations, then the disk lost) refuses

+ to wake on a gap the retention made: INV-3.

+- **Claim rev 6.4's stamp lifecycle (R5-4).** `holder.stamp` is a claim

+ field written by every installing CAS: create step 4 (the console and

+ the recovery pass finishing it), adoption, the flip, a push's probe CAS,

+ a dirty rollback's source probe CAS. A box's local record is created or

+ refreshed only by `initRecord`: a fresh claim read under the guard that

+ names the box `op.exec` or the landing participant, `active_stamp =

+ holder.stamp`, run at the top of every role pass and at the recovery

+ pass's mint. A writer for a host with no record is refused (rev 7.5's

+ model admitted it). The two retirements are two helpers:

+ `retireArtifacts(inc, S)` names the retirement and moves no stamp (the

+ landing's `local`, the activator's park of a warm database from an

+ earlier stay, a dirty install on the source); `retireStamp(inc)` moves

+ the active stamp into the retired set and sets none (the local park at

+ a delete, a move away, quarantine); activation (`install`) moves the

+ old active stamp into the retired set before setting the new one, as

+ claim rev 6.4's answer 2 has it. Passes capture the stamp from the

+ record when they select their work (answer 1). The

+ landing's `checking` installs from `holder.stamp`, not from a claim

+ revision it computed. Local artifacts (`localDB.Stamp`,

+ `filesDir.Stamp`) carry the stamp of the installation that produced

+ them.

+- **The S3 layout (R5-6).** LTX keys are

+ `<generation prefix>/<level, 4 hex>/<min, 16 hex>-<max, 16 hex>.ltx`

+ (`ltxKey`, `ltxKeyRe`); the sweep's `locationOf` treats a child prefix

+ that is not an incarnation id (a level directory, a `g-<op>/` prefix)

+ as the host prefix's own location, and a decimal child (the claim's 64

+ hex characters) as an incarnation location (claim rev 6.4 §6.2a).

+- **Uploads are sequential (R5-1, step 6).** Each sync writes its level-0

+ file locally and the replica uploads the local files in TXID order,

+ never sending the next before the one ahead completed; an upload the

+ client has waited eight steps for is retried with the same bytes, and

+ the original may still land as an identical version. A gap in the

+ current listing is therefore always a file that has not landed. Rev

+ 7.6's second baseline shipped the next file while the first was in

+ flight and lost a cold restore to the gap in 9 seeds of 30,000.

+- **The retention fixture (R5-6)** populates `retired_incarnations` with

+ 2 to 33 and panics unless the injected incarnation 1 is absent and the

+ list is at its cap.

+- **The budget (R5-5, `budget_test.go`)** prices the final delta at the

+ bar, then the target's restore of the staged replica, snapshot write

+ and anchor write at the local rate; a 2 GiB database over 10 MiB/s is

+ admitted with one attempt at 50 MiB/s local and refused as a

+ cross-region snapshot transfer (205 s).

+- **Not taken in rev 7.6**, stated in §14.2.6: the model has no bytes, so

+ the staged replica is one object holding the stopped source's state and

+ the install copies it into the generation as the snapshot; where the

+ snapshot is built is a cost the budget test prices, not a protocol

+ step the model distinguishes; the seal names one version, not one per

+ staged file.

#### 14.2.3 Invariants and results

The invariants are the table at the end of §4, with three checks rev 6

@@ -2148,7 +2443,32 @@ 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.5, on the final model (claim rev 6.2: installation stamps, the

+**Rev 7.6, on the final model (claim rev 6.4: `holder.stamp`,

+initialization under the guard, the two retirements; the replication

+position, the anchor, sequential uploads, snapshot rotation and

+retention, root advancement; no whole-state checksum; the pinned S3

+layout): 30,000 seeds, zero violations; 100,000 seeds, zero violations**

+(39 s and 120 s: without the whole-state checksum the page-image model

+runs at rev 7.4's speed again). Across the 100,000 seeds: 154,958

+completed operations, among them 1,823 completed moves, 1,884 clean and

+95 dirty rollbacks, 386 pre-flip reverts, 330 declared losses, 30,057

+pushes, 89,042 delete-park-free cycles and 1,491 lost disks; 14,530 LTX

+compactions, 10,184 snapshot rotations, 737 level-0 upload retries and

+34,658 anchors written at cold restores; 38,827 requests completed after

+`H`; 33,363 staging signatures were refused as stale; 30,693 creates

+restarted on a 412; 120 targets were stopped mid-return. No restore was

+refused for a gap with every rule in place. Three faults the rebuilt

+model found in itself before these baselines, each fixed in the model

+step (§14.2.2): the sweep misread `g-<op>/` under a legacy host as an

+incarnation location and parked the live generation (2 / 3,000); the

+replicator shipped the next level-0 file while the one ahead was still

+in flight, so a cold restore met a gap (9 / 30,000, 19 / 100,000); and,

+before that, a seal advanced the position without shipping its file.

+Rev 7.5's explanation of its own fix below, the `-txid` sidecar, was

+wrong (R5-1, fact R5-1e); the position comes from the newest level-0

+file, which is why the anchor exists.

+**Rev 7.5, on claim rev 6.2 (installation stamps, the

region-qualified live set, retirement under purge; LTX files with

compaction and litestream's restore planner; the marker-hold and

targeted-freeze schedules and the retention fixture): 30,000 seeds, zero

@@ -2276,45 +2596,53 @@ 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.5 model, with the strict classification, **in two

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

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

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

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

-29 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 **75 rules**: rev 7.4's 71 plus `fence-stamp` (claim rev 6.2

-§6.4), `live-set-region` (claim rev 6.2 §6.2a), `restore-overlap` and

-`restore-gap-closed` (§5.1). No run was an ERROR. Seed numbers reproduce

-any sweep line with `HOSTLIFE_SEED`; `HOSTLIFE_WITNESS=<rule>` replays a

-witness with its trace. Rev 7.4's counts are in the rev 7.4 spec

-(0e41b685); the new schedules and fixture reshuffled every seed, and the

-LTX model changed what many mutations break, so sweep counts moved; every

-witness verdict is unchanged, and three rules the sweep could not reach

-before are caught by it now.

+on the final rev 7.6 model (50b1e51d), with the strict classification,

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

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

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

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

+same mutation, for the 31 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 **77 rules**: rev 7.5's 75 plus

+`restore-anchor` and `root-advance` (§5.1, R5-1, R5-3). `mutate.sh 3000`

+exited 0: no ERROR, no unexpected MISSED, no STALE. Seed numbers

+reproduce any sweep line with `HOSTLIFE_SEED`; `HOSTLIFE_WITNESS=<rule>`

+replays a witness with its trace. Rev 7.5's counts are in the rev 7.5

+spec (cdc98845); the sequential uploader, the rotation and the stamp

+lifecycle reshuffled the seeds, so sweep counts moved; every witness

+verdict is unchanged, and `fence-stamp` is caught alone by the sweep now

+(below).

| | rules |

|---|---|

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

-| caught alone by the sweep at 30,000, and by their witness | 4 (`fence-by-installation`, `orphan-order`, `rollback-journal`, `staging-quiet`) |

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

+| caught alone by the sweep at 30,000, and by their witness | 4 (`orphan-order`, `rollback-journal`, `staging-quiet`, `restore-overlap`) |

| caught alone by the sweep at 100,000, and by its witness | 1 (`declare-lost-compute`) |

| caught alone by their witness only; the sweep misses them at 30,000 | 2 (`live-set-region`, `restore-gap-closed`) |

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

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

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

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

| unexercised | **0** |

-**What the generator changes bought (R4 §3).** `generation-conditional`

-was witness-only at 0 / 100,000 in rev 7.4; the marker-hold schedule

-makes it 13 / 3,000 and 383 / 100,000. `declare-lost-compute` was

-witness-only at 0 / 100,000; the targeted freeze makes it 3 / 100,000.

-`sweep-namespace` was witness-only at 0 / 30,000; the retention fixture

-makes it 88 / 3,000. `fence-by-installation` was witness-only at 0 /

-30,000; the probe-fence oracle makes it 2 / 30,000, because a move back

-that rolls back is a violation now, not a converged terminal. Two rules

-stay witness-only: `live-set-region` (the sweep's legacy fixture never has

-an old regional PUT land after discovery) and `restore-gap-closed` (no

-seed loses a replica object with every rule in place).

+**What the rev 7.6 changes moved.** The two new rules are caught at

+once: `restore-anchor` 43 / 3,000, 437 / 30,000, 1,430 / 100,000 (every

+seed that cold-restores a snapshot-only install and then writes);

+`root-advance` 38 / 3,000, 317 / 30,000, 986 / 100,000 (every seed whose

+replica rotated past its pinned snapshot before a cold restore).

+`fence-stamp` was witness-only in rev 7.5; under claim rev 6.4's "no

+local record: refuse", a pass that selected its work before the box's

+record was initialized carries no stamp, and the equality check alone

+refuses it, so the sweep catches the rule at 180 / 3,000 and 1,588 /

+30,000; its witness still needs `hostguard` dropped, as the text

+predicts. `fence-by-installation` rose from 2 / 30,000 to 221 / 3,000:

+the record is initialized from `holder.stamp` on every pass now, so the

+mutation's whole-incarnation fence bites on every reinstall. Rev 7.5's

+generator gains stand (`generation-conditional` 371 / 100,000,

+`declare-lost-compute` 2 / 100,000, `sweep-namespace` 543 / 3,000). Two

+rules stay witness-only: `live-set-region` (the sweep's legacy fixture

+never has an old regional PUT land after discovery) and

+`restore-gap-closed` (no seed loses a replica object with every rule in

+place; the uploader never produces a gap, §5.1 step 6).

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

in combination, and one per rule a review round added; two for

@@ -2344,22 +2672,24 @@ witness to hold there; each witness violates with the failure it names.

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

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

| `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 / 30,000; the pairs 271 and 269 / 30,000 |

-| `fence-by-installation` (claim rev 6.2 §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) | | 0 / 3,000, 2 / 30,000 |

-| `fence-stamp` (claim rev 6.2 §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 | 0 / 30,000; the pair 61 / 30,000, which is `hostguard`'s own 61: the sweep does not separate them, the witness does |

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

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

-| `live-set-region` (claim rev 6.2 §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 | | 0 / 30,000 |

-| `restore-overlap` (§5.1, R4-1) | a generation's snapshot ends at TXID 11; the only continuation is a compacted file `[10, 15]`; the disk is lost and the host wakes cold | **violated**: INV-2, the wake loses four acknowledged writes (rev 7.4's `min == current + 1` discards the file) | | 27 / 3,000, 186 / 30,000 |

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

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

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

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

+| `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 | | 0 / 30,000 |

+| `restore-overlap` (§5.1, R4-1) | a generation's snapshot ends at the push's TXID; the only continuation is a compacted file starting one below it; the disk is lost and the host wakes cold | **violated**: INV-2, the wake loses four acknowledged writes (rev 7.4's `min == current + 1` discards the file) | | 0 / 3,000, 4 / 30,000 (rotation now usually leaves a snapshot the planner can root at instead) |

+| `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 | | 0 / 30,000 |

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

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

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

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

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

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

-(C5a): 5 / 3,000, 46 / 30,000. `registration-check` is not caught alone

-by the sweep at 3,000 or 30,000 seeds, and its witness holds alone; the

-re-read alone is shown insufficient (`purge-claim-fence` + `fence-etag`,

-331 / 30,000).

+(C5a): 6 / 3,000, 48 / 30,000. `registration-check` is not caught alone

+by the sweep at 3,000 seeds, and its witness holds alone; the re-read

+alone is shown insufficient (`purge-claim-fence` + `fence-etag`, 333 /

+30,000); its two pairs 271 and 272 / 30,000.

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

@@ -2375,62 +2705,71 @@ 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: 60 of 75** (53 by the sweep at 3,000; 4 by the sweep at

+**Caught alone: 63 of 77** (56 by the sweep at 3,000; 4 by the sweep at

30,000 and by their witness, marked †; 1 at 100,000 and by its witness,

marked ††; 2 by their witness alone, marked ‡).

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

-| `recovery-pass` | 2,465 / 3,000 | | `fresh-incarnation` | 52 / 3,000 |

+| `recovery-pass` | 2,458 / 3,000 | | `fresh-incarnation` | 51 / 3,000 |

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

-| `park-by-version` | 2,522 / 3,000 | | `park-all-versions` | 574 / 3,000 |

-| `park-skip-lock` | 2,721 / 3,000 | | `retirement-ids` | 333 / 3,000 |

-| `quiet-before-ack` | 211 / 3,000 | | `straggler-sweep` | 781 / 3,000 |

-| `sweep-staging` | 51 / 3,000 | | `sweep-namespace` | 88 / 3,000 |

-| `restore-by-generation` | 189 / 3,000 | | `restore-overlap` | 27 / 3,000 |

-| `purge-reserve-first` | 2,167 / 3,000 | | `purge-adopts` | 7 / 3,000 |

-| `purge-journal` | 1,883 / 3,000 | | `admission-registration` | 40 / 3,000 |

-| `registration-recovery` | 2,117 / 3,000 | | `purge-claim-fence` | 29 / 3,000 |

-| `fence-etag` | 24 / 3,000 | | `claim-never-deleted` | 5 / 3,000 |

-| `cancelled-creates` | 374 / 3,000 | | `orphan-no-deadline` | 50 / 3,000 |

-| `orphan-order` † | 2 / 30,000 | | `evidence-whole-tree` | 67 / 3,000 |

-| `evidence-from-state` | 2,614 / 3,000 | | `floor-boot-recovery` | 2,519 / 3,000 |

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

-| `sign-before-safeuntil` | 20 / 3,000 | | `sign-at-check` | 14 / 3,000 |

-| `sdk-no-resign` | 14 / 3,000 | | `lost-quarantine` | 3 / 3,000 |

-| `declare-lost-compute` †† | 3 / 100,000 | | `cut-deadline` | 13 / 3,000 |

-| `revert-journal` | 13 / 3,000 | | `rollback-journal` † | 8 / 30,000 |

-| `dirty-return` | 8 / 3,000 | | `commit-before-open` | 11 / 3,000 |

-| `lost-return-park` | 5 / 3,000 | | `target-park` | 52 / 3,000 |

-| `abort-target-owner` | 940 / 3,000 | | `timer-freeze` | 4 / 3,000 |

-| `timer-canonical` | 7 / 3,000 | | `markers-last` | 1 / 3,000 |

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

-| `staging-quiet` † | 6 / 30,000 | | `fresh-admission` | 16 / 3,000 |

-| `stale-hold-release` | 5 / 3,000 | | `obligations-block-ops` | 20 / 3,000 |

-| `claim-op-exclusive` | 79 / 3,000 | | `recovery-current-inputs` | 47 / 3,000 |

-| `files-carried` | 77 / 3,000 | | `generation-conditional` | 13 / 3,000 |

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

+| `park-by-version` | 2,522 / 3,000 | | `park-all-versions` | 577 / 3,000 |

+| `park-skip-lock` | 2,721 / 3,000 | | `retirement-ids` | 338 / 3,000 |

+| `quiet-before-ack` | 217 / 3,000 | | `straggler-sweep` | 784 / 3,000 |

+| `sweep-staging` | 53 / 3,000 | | `sweep-namespace` | 543 / 3,000 |

+| `restore-by-generation` | 175 / 3,000 | | `restore-overlap` † | 0 / 3,000, 4 / 30,000 |

+| `restore-anchor` | 43 / 3,000, 437 / 30,000, 1,430 / 100,000 | | `root-advance` | 38 / 3,000, 317 / 30,000, 986 / 100,000 |

+| `purge-reserve-first` | 2,162 / 3,000 | | `purge-adopts` | 7 / 3,000 |

+| `purge-journal` | 1,861 / 3,000 | | `admission-registration` | 40 / 3,000 |

+| `registration-recovery` | 2,112 / 3,000 | | `purge-claim-fence` | 29 / 3,000 |

+| `fence-etag` | 24 / 3,000 | | `claim-never-deleted` | 6 / 3,000 |

+| `cancelled-creates` | 370 / 3,000 | | `orphan-no-deadline` | 49 / 3,000 |

+| `orphan-order` † | 1 / 30,000 | | `evidence-whole-tree` | 11 / 3,000 |

+| `evidence-from-state` | 2,614 / 3,000 | | `floor-boot-recovery` | 2,571 / 3,000 |

+| `participant-rows` | 7 / 3,000 | | `revalidate-before-effect` | 79 / 3,000 |

+| `sign-before-safeuntil` | 18 / 3,000 | | `sign-at-check` | 14 / 3,000 |

+| `sdk-no-resign` | 15 / 3,000 | | `lost-quarantine` | 2 / 3,000 |

+| `declare-lost-compute` †† | 2 / 100,000 | | `cut-deadline` | 7 / 3,000 |

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

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

+| `lost-return-park` | 4 / 3,000, 32 / 30,000, 112 / 100,000 | | `target-park` | 52 / 3,000 |

+| `abort-target-owner` | 944 / 3,000 | | `timer-freeze` | 7 / 3,000 |

+| `timer-canonical` | 3 / 3,000 | | `markers-last` | 1 / 3,000 |

+| `staging-quiet` † | 1 / 3,000, 9 / 30,000 | | `fresh-admission` | 17 / 3,000 |

+| `stale-hold-release` | 4 / 3,000 | | `obligations-block-ops` | 26 / 3,000 |

+| `claim-op-exclusive` | 80 / 3,000 | | `recovery-current-inputs` | 48 / 3,000 |

+| `files-carried` | 73 / 3,000 | | `generation-conditional` | 15 / 3,000, 371 / 100,000 |

+| `fence-stamp` | 180 / 3,000, 1,588 / 30,000 | | | |

+**Caught only in a combination: 11 rules.** `fence-stamp` left this list

+in rev 7.6 (above); its pair with `hostguard` is still reported because

+the witness needs it. Each partner's own count, on

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

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

subset in the gate.

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

-| `purge-claim-fence` + `fence-etag` (**the re-read alone**, rev 7's CC21 as proposed) | 331 / 30,000 | `purge-claim-fence` 240, `fence-etag` 223, `registration-check` 0 | (the two `registration-check` rows below) | a store destroyed under a creating or serving host |

+| `purge-claim-fence` + `fence-etag` (**the re-read alone**, rev 7's CC21 as proposed) | 333 / 30,000 | `purge-claim-fence` 241, `fence-etag` 223, `registration-check` 0 | (the two `registration-check` rows below) | a store destroyed under a creating or serving host |

+| `fence-stamp` + `hostguard` (no longer combination-only) | 2,292 / 30,000 | `hostguard` 8 / 3,000, `fence-stamp` 1,588 / 30,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 |

+Combinations marked "rev 7.5" were not rerun in rev 7.6: their rules

+and witnesses are unchanged, each witness held under every proper subset

+and violated under the set in the rev 7.6 gate, and their sweep counts

+are rev 7.5's (cdc98845).

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

They have no witness: neither can violate an invariant.

@@ -2440,14 +2779,16 @@ only after its own horizon, and CC11 holds. No witness: there is no

interleaving to force.

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

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

-witnesses are the evidence for rev 7.5.

+a second; 32 witnesses, 106 runs); the 30,000- and 100,000-seed

+baselines, this sweep and the witnesses are the evidence for rev 7.6.

#### 14.2.6 What the model does not prove

- **It is a model.** It checks the protocol, not the code that will

implement it. Its S3 is a versioned map with the documented semantics,

- every one checked against the real service (§15 step 8).

+ every one checked against the real service (§15 step 8). Its

+ litestream is the behaviour `internal/sim/litestreamfacts/` observed

+ in the pinned library (§14.2.1), not the library itself.

- **Granularity.** One data-plane host, three regions, one box per region,

and a second hostname for creates and purges only. One step is atomic,

except where rev 6 splits it (§14.2.2).

@@ -2465,16 +2806,27 @@ witnesses are the evidence for rev 7.5.

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

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

which window do not (J2 §2).

-- **Restore fidelity (R3-1, R4-1).** The model's LTX files have ranges,

- final page images, checksums and compaction, and its restore is

- litestream's planner (§5.1), so a compacted continuation, a gap and a

- stale image are all representable and each has a witness. What the

- model's pages are not is bytes: a key's image is one integer, a

- checksum is a digest of the whole state, and page size, WAL salts and

- the lock page are absent. The claim it supports is that the planner as

- specified restores exactly the acknowledged transactions up to the

- TXID it reaches and refuses otherwise; byte-level LTX decoding is

- validated against the real restore (§15 step 8).

+- **Restore fidelity (R3-1, R4-1, R5-1 to R5-3).** The model's LTX files

+ have levels, ranges in replication numbering and final page images,

+ with compaction, snapshot rotation and retention as the pinned library

+ does them, and its restore is litestream's planner with the root rule,

+ the anchor and the position read of §5.1, so a compacted continuation,

+ a gap, a snapshot-only install and a rotated-away root are all

+ representable and each has a witness. What the model's pages are not is

+ bytes: a key's image is one integer, there is no checksum of any kind

+ (the pinned files carry a per-file CRC-64 and no database checksum,

+ fact R5-2), and page size, WAL salts and the lock page are absent. The

+ claim it supports is that the planner as specified restores exactly

+ the acknowledged transactions up to the TXID it reaches and refuses

+ otherwise. What the real library does with real files is established

+ by `internal/sim/litestreamfacts/` (§14.2.1): rev 7.5 pointed here at

+ §15 step 8, which verified S3 behaviours and never ran litestream

+ (R5 review). Not modelled: bytes and so the cost of a transfer (the

+ budget test prices it, §7.3); the staged replica as several files with

+ one sealed version each (the model's seal names one object holding the

+ stopped source's state, which is what the target's build yields from

+ the staged files); litestream's time-based level-0 retention (the

+ model expires level 0 with level 1, by TXID); `integrity_check`.

- **Observation boundaries not taken in rev 7.4 or 7.5** (R3 review):

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

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

@@ -2739,7 +3091,7 @@ spec.** Rev 6.1 (79a5243c) answered the three questions: operations are

ordered by claim `gen`, op ids opaque; a record with no claim object is a

legacy host, never an orphan; the claim owns the sweep-side rule for the

live set and this spec owns generation-specific live-object selection.

-Rev 6.2 then took joint round 4's claim side: **installation stamps**

+Rev 6.2 took joint round 4's claim side: **installation stamps**

(§6.4 there: the stamp is the claim `gen` captured at the CAS that made

the installation current, a writer is admitted only at the active stamp,

retirement sets `none`, a reinstall sets its own stamp under the guard),

@@ -2750,8 +3102,40 @@ protected in the authoritative region only; the authoritative region is

and **retirement under purge** (§5.3 step 4 there: the record version in

`op.intent`, `DeleteIfMatch`, `purging → parking` only with the record

gone and the journal at `torn-down`; a purged host never returns to

-`serving`). Rev 7.5 encodes all of it (§5.1, §6.4, §14.2.2) and raises no

-new claim question (`moves-claim-questions.md`, rev 7.5 heading).

+`serving`). Rev 7.5 encoded all of it (§5.1, §6.4, §14.2.2) and raised no

+new claim question.

+**Claim rev 6.3 (8faa89a4) and rev 6.4 (697f0f9f), after joint round 5:

+no request from this spec.** Rev 6.3 takes R5-4's claim side: **`holder.stamp`** in the claim

+schema (§2 there), written by the CAS that makes an installation

+current, so the claim is the durable record and the recovery source;

+**initialization** of a box's local record only from a fresh read under

+the guard that names the box `op.exec` or the landing participant

+(`active_stamp = holder.stamp`: a create's first wake, adoption, a lost

+record on restart); **no local record: refuse**; **two retirements**,

+`retire-artifacts(S)` (parks the artifacts tagged `S`, adds `S` to the

+retired set, leaves `active_stamp`) and `retire-installation` (moves the

+active stamp into the retired set, sets `none`, parks everything), with

+every helper naming which it is; and a dirty rollback that never keeps

+its predecessor's stamp. Rev 6.4 answers rev 7.6's three notes

+(`moves-claim-questions.md`, rev 7.6 heading): the stamp is captured

+from the box's local record at work selection and compared with

+`active_stamp` under the guard, the fresh claim read still serving the

+incarnation, operation and config and release identity, so `fence-stamp`

+and its witness stand; `retire-artifacts(S)` only parks the files tagged

+`S` and never changes `active_stamp` or `retired_stamps`, activation (old

+active into retired, then the new one) and `retire-installation` being

+the only moves of a stamp, so a dirty rollback parks its pre-move

+database with `S` still active and `S` retires when the probe CAS's new

+stamp activates, issuance staying with `holder.generation` in one write;

+and §6.2a now says that a child prefix that is not an incarnation id (64

+hex) belongs to the host prefix's own location. Rev 7.6 encodes all of

+it (§6.4, §7.6, §7.8, §14.2.2): every installing CAS in the model writes

+`holder.stamp`, `initRecord` is the only writer of a box's record,

+`retireArtifacts` moves no stamp and `install` retires the old active

+stamp, and the landing's `checking` installs from `holder.stamp`. This

+spec's phase table (§5.1) is what the claim's "landing participant"

+defers to.

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

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

@@ -3027,3 +3411,26 @@ half of R4-3, and R4-4. Rev 7.5 answers the moves side and encodes rev 6.2.

| §3: the random generator lacks marker and freeze schedules, a successful-move assertion and a retention fixture | all four added (§14.2.2): the marker-hold and targeted-freeze schedules, the retention-boundary fixture, and two oracles that refuse a rolled-back move as a terminal where it should have served; `generation-conditional`, `sweep-namespace` and `restore-overlap` are caught by the sweep alone now (§14.2.5) |

| §3: the three-rule door combination is not minimal | the results table says so: `door-by-version` + `location-per-incarnation` is the minimal pair and the three-rule row is reported as a wider combination whose two-rule subsets already fail (§14.2.5) |

| §3: ids-only restoration is a fidelity gap | closed with R4-1: transactions update and delete, and the oracle compares states, not id sets (§14.2.6 says what a page is not) |

+### 22.12 Joint round 5 (claim 30d572c4, moves rev 7.5 cdc98845, model cdc98845)

+Astra's verdicts were "not ready" for the moves spec and the model, on the

+pinned libraries: three findings where rev 7.5 described litestream

+v0.5.14 and ltx v0.5.1 from their documentation and the libraries do

+otherwise, one on the stamp lifecycle, one on the budget, one on a

+fixture. Claim rev 6.3 (8faa89a4) took R5-4's claim side and rev 6.4

+(697f0f9f) answered rev 7.6's three notes. Rev 7.6 starts

+from a spike against the pinned libraries (`internal/sim/litestreamfacts/`,

+d96f781c) and answers the moves side from what it observed.

+| finding | rev 7.6 |

+|---|---|

+| R5-1 (P1) restoring the sealed snapshot does not establish the replication position; `-txid` is follow-only; a snapshot-only install restarts at TXID 1 and a later cold restore loses the new writes | confirmed against the pinned library (facts R5-1a, b, e). The install writes a **level-0 anchor** `[N, N]` with every page beside the snapshot, which the pinned open takes as its position so the next sync is `N + 1` (facts R5-1c, d); a replica that has replicated since needs none, because retention never removes the newest level-0 file (facts R5-1f to h). §5.1 step 7, §7.6 `building`, §7.8. The model separates the replication position from the lineage TXID, reads the position as litestream does and writes the anchor (`restore-anchor`); its witness is the finding's sequence: snapshot-only install, write, replicate, lose the disk, restore cold (§14.2.5) |

+| R5-2 (P2) the pinned writers set `HeaderFlagNoChecksum`; the required post-apply checksum comparison would refuse every healthy continuation or be skipped | confirmed (fact R5-2). Verification is what the format supplies: the per-file CRC-64 trailer (`Decoder.Verify`), `PRAGMA integrity_check`, the required TXID at an install, the gap refusal (§5.1 step 5); end-state checksums would need three writers changed and Phase 1 does not change them. The whole-state checksum is gone from the model, `snapshot_checksum` is `snapshot_crc64` |

+| R5-3 (P2) rooting at the installation snapshot for good conflicts with snapshot retention; "every level" excluded later snapshots | confirmed (facts R5-3a to f: after two rotations no current file continues from the pinned snapshot, the rooted restore fails "non-contiguous", litestream's own restore from the newest snapshot holds every row). The root is the newest current **verified successor snapshot** of the named generation at or past the pinned one, the pinned version only when none is current (§5.1 steps 4 and 8). The model rotates snapshots and enforces retention as the library does, and `root-advance` has a witness: four rotations, then the disk lost (§14.2.5) |

+| R5-4 (P2) stamps lack a durable initialization and replacement contract: creation's stamp from `c.Ver` at reconciliation, no recovery source, a dirty rollback keeps the old stamp, the general local park would retire the landing's own stamp, a writer admitted with no record | claim rev 6.3 §2 and §6.4, with rev 6.4's answers, encoded exactly (§6.4, §7.6, §7.8, §14.2.2): `holder.stamp` written by every installing CAS; the local record initialized only by a fresh read under the guard naming the box; no record refuses; `retire-artifacts` (moves no stamp) against `retire-installation`, named at every call; activation retires the old active stamp; a dirty rollback's probe CAS issues a new stamp with `holder.generation` in one write; the pass's stamp is captured at work selection. The admit-when-absent branch is gone |

+| R5-5 (P2) T11 budgets a 16 MiB mirror while the sealed transfer is a whole snapshot: 2 GiB over 10 MiB/s is admitted and rolled back | the sealed snapshot is **built on the target** from the staged replica (§5.1 steps 1 and 2, §7.4 `stopped` and `staged`, §7.6 `building`): the delta stays within the bar and the seal names `N` and the staged versions; T11 prices the target's restore, snapshot and anchor at the local rate (§7.3). `budget_test.go` shows the example admitted that way and refused as a cross-region transfer. The model has no bytes and does not distinguish where the snapshot is built (§14.2.6) |

+| R5-6 (P3) the retention fixture never crossed the boundary it claims | populates 2 to 33 and asserts 1 absent and the list at its cap (`retentionStart`); the layout question raised beside it is fixed too: LTX keys are the pinned S3 client's `<prefix>/<level, 4 hex>/<min>-<max>.ltx` in the spec and the model (§5.1), and §14.2.6 points at `litestreamfacts`, not at §15 step 8, for library behaviour |

+| fidelity: `fence-stamp`'s equal sweep counts with `hostguard` add no independent evidence | under claim rev 6.4's "no local record: refuse", a pass that selected its work before the box's record was initialized carries no stamp, and the equality check alone refuses it: `fence-stamp` is caught alone by the sweep now (§14.2.5); the witness is unchanged and still needs `hostguard` dropped, as the text predicts |

+| fidelity: `restore-gap-closed` is a malformed-replica test, not evidence the uploader produces the sequence | agreed, and stated in its row: the uploader never produces a gap (§5.1 step 6); the witness shows the refusal, the sweep shows no seed loses an object with every rule in place |