amadan
spec: move-any-app rev 7.8: joint round 7, writer epochs (claim rev 6.6), every number rerun (#175)
Written against claim rev 6.6 (b10547e1), whose §6.4a answers R7-1. R7-1 (P1): two writers whose uploads could overlap never share a generation (§5.1 step 9): the clean close and its marker, lost replication state decided by it, cold recovery as an installing CAS into a fresh generation (§7.14: the CAS, build under stop evidence, publish with the park-generation chore, release), writers bound to their generation; the data path owned here (warm database as baseline, the marker consumed at open, a wake waits for a draining writer, a replay reuses current artifacts). R7-2: the identity oracle. R7-3: the newest level-0 file in every retention path (§5.1 step 8). R7-4: build intent, acknowledged artifacts, completed manifest; generation.json only from completion (§5.1 step 2, §7.6). R7-5: the Store gate's assertions (§14.2.1). §14.2.2 to §14.2.6 for the rev 7.8 model (84 rules, 42 witnesses, the door witnesses retired, 30,000 and 100,000 seeds clean, the writer-epoch rules witness-only in the sweep); §19.4 claim rev 6.6 and three notes; §22.14 dispositions.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
1 file changed,
+487
−147
docs/superpowers/specs/2026-10-02-move-any-app-design.md+487 −147
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 68161e282..cfbb202fa 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.7. |
| +**Revision:** 7.8. |
| + |
| +- **Rev 7.8** answers **joint round 7** (`CODEX-FINDINGS-JOINT-R7.md`, |
| + cited "R7-n") and is written against **claim spec rev 6.6** (b10547e1), |
| + whose new §6.4a, writer epochs, answers R7-1; §22.14 has every |
| + disposition. **R7-1 (P1):** the hazard rev 7.7's note raised is real |
| + and now closed: litestream's level-0 PUT is unconditional and its key is |
| + prefix, level and TXID range only (`TestFact_R7_1_UnconditionalPut`), |
| + so a dead writer's in-flight upload for `[N + 1]` can replace the file |
| + the next writer uploaded for the same TXID, or make its upload loop |
| + skip it. **Two writers whose uploads could overlap never share a |
| + generation** (§5.1 step 9, §7.14): a writer that stops cleanly drains |
| + its uploads and writes `closed.json {stamp, max_txid}` once; a wake |
| + continues the generation only if that marker exists, its `max_txid` is |
| + the generation's remote maximum and its stamp is the box's own, and the |
| + writer consumes it as it opens; anything else is lost replication state |
| + and a **cold recovery**, an installing CAS into a fresh generation |
| + (new `holder.generation`, new `holder.stamp`), built under stop |
| + evidence from the warm database or the old generation restored, |
| + published, then served, with the old generation parked as a chore. |
| + Rules `recovery-generation`, `closed-marker`, `close-waits`; witnesses |
| + for both completion orders, the initialization/remote-position race, a |
| + stale marker, a crash before the marker, and a clean close that must |
| + wait. **R7-2 (P2):** the cold-restore oracle checks required writes by |
| + identity and compares the state with the replay of exactly the writes |
| + the restored files carry; the per-key mask is gone, with the review's |
| + counterexample as a witness. **R7-3 (P2):** every retention path keeps |
| + the newest level-0 file (`newest-l0`, witness with the local position |
| + ahead of the uploads). **R7-4 (P2):** a build is a durable intent, then |
| + acknowledged artifacts, then a completed manifest, and `generation.json` |
| + is published only from the completed state (§5.1 step 2, §7.6; INV-11, |
| + `build-completion`, witness with crashes between the steps). **R7-5 |
| + (P3):** the Store gate awaits each maintenance event it claims, compares |
| + row contents with updates and deletes, and forces a restore through |
| + compacted continuation files (§14.2.1). The model's full files replace |
| + the state they are applied to and carry every write they hold, which the |
| + rebuilt oracle needed. 84 rules, 42 witnesses (two rules the sweep no |
| + longer reaches at 3,000 seeds under writer epochs, `evidence-whole-tree` |
| + and `timer-freeze`, gained witnesses; the two door witnesses are |
| + retired). Results in §14.2.3 and §14.2.5. |
| - **Rev 7.7** answers **joint round 6** (`CODEX-FINDINGS-JOINT-R6.md`, |
| cited "R6-n") and is written against **claim spec rev 6.5** (d36adcfa), |
| @@ -658,20 +697,29 @@ fails there first (§14.2.6). |
| 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 encoding inputs are persisted before the |
| - PUTs** (R6-5): the install manifest records the header timestamp the |
| - builder used, with the page size, commit and `N`, so that a replay (a |
| - restarted `building`) encodes **identical bytes**; the bytes depend on |
| - the timestamp (`TestFact_R6_5_AnchorReplayBytes`: the same inputs give |
| - the same bytes, one millisecond's difference gives another file), and |
| - the identical-bytes argument for late PUTs (step 3, step 7) rests on |
| - this. A replay that finds its snapshot or anchor already current under |
| - the key reuses the object rather than writing again. The manifest also |
| - records the sha256 of the database file the build produced (§7.6 |
| - `restored`), the snapshot's key, the `versionId` the PUT returned, `N` |
| - and its CRC-64. The cost is three passes over the database, each |
| - across regional S3 and the disk, plus a verification read, which T11 |
| - prices (§7.3). |
| + requires (fact R5-1c). **A build is two durable states, never one |
| + object** (R7-4): first the **build intent**, |
| + `<location>g-<move id>/build-intent.json`, written before any PUT, with |
| + the encoding inputs the builder will use (the header timestamp, the |
| + page size, the commit, `N`) so that a replay (a restarted `building`) |
| + encodes **identical bytes** (R6-5: the bytes depend on the timestamp, |
| + `TestFact_R6_5_AnchorReplayBytes`); then, only once the snapshot PUT |
| + and the anchor PUT have both returned, the **completed install |
| + manifest**, `<location>g-<move id>/install.json`, with the artifacts' |
| + acknowledged identities (keys, the `versionId` each PUT returned, `N`, |
| + each file's CRC-64) and the verification results (`integrity_check` |
| + passed, the sha256 of the database file the build produced). The |
| + completion predicate is the manifest's existence, never the intent's: |
| + rev 7.7 said "the install manifest records the inputs before the PUTs" |
| + and "`building` is done when the install manifest exists", so a crash |
| + after the inputs and before the artifacts left a manifest that |
| + satisfied the completion predicate (R7-4). A replay reads the intent, |
| + encodes the same bytes, and reuses a snapshot or anchor it finds |
| + already current under its key rather than writing again (the model's |
| + cold recovery does the same, §7.14). `generation.json` is published |
| + only from the completed state (step 3). The cost is three passes over |
| + the database, each across regional S3 and the disk, plus a |
| + verification read, which T11 prices (§7.3). |
| 3. **`generation.json` names the snapshot**: `snapshot_key`, |
| `snapshot_version`, `snapshot_txid = N`, `snapshot_crc64`. These are |
| the snapshot identity: the **pinned root**. A second version under the |
| @@ -777,15 +825,87 @@ fails there first (§14.2.6). |
| 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). |
| + version under `holder.generation` and the pinned version (§6.4). **The |
| + newest level-0 file survives every retention path** (facts R5-1f to h; |
| + R7-3): compaction deletes its inputs bar the newest, and the expiry |
| + below the previous snapshot never takes the newest level-0 file, which |
| + is where a fresh box reads its position. Rev 7.7's model kept it only |
| + through compaction and expired it when the local position had run |
| + ahead of the uploads (R7-3; the model's `newest-l0`). |
| +9. **Writer epochs: two writers whose uploads could overlap never share a |
| + generation (claim rev 6.6 §6.4a, R7-1).** Litestream writes each file |
| + to a key built from the level and the TXID range only, and its PUT is |
| + unconditional (`TestFact_R7_1_UnconditionalPut`). So a writer A whose |
| + level-0 upload for `[N + 1]` is still in flight when A dies with its |
| + disk, and a writer B that restores the generation through `N` and |
| + uploads its own `[N + 1]`, collide: if A's PUT lands last it replaces |
| + B's file and the next cold restore loses B's acknowledged writes; if it |
| + lands after B initialized its position and before B's sync, B's upload |
| + loop takes the remote `[N + 1]` as already uploaded and skips B's |
| + (`replica.go` `Sync`), and B's write is never replicated at all. |
| + `lock.json` cannot revoke a PUT S3 has accepted, and waiting for the |
| + lease to expire proves nothing about requests already signed. Rev 7.7 |
| + raised this hazard; round 7 made it a P1. Claim rev 6.6 states the |
| + rule and this spec owns the data path: |
| + - **A clean close.** A writer stopping cleanly first waits until |
| + **every** upload it issued has returned success, then writes |
| + `<location>/<generation>/closed.json` as `{stamp, max_txid, |
| + closed_at}` once (`If-None-Match`), then releases its lease. A writer |
| + that saw any upload fail, time out or come back ambiguous writes no |
| + marker; a crash while draining leaves none; an operation that takes |
| + the writer over (a push, a move, a delete) drops a pending close, |
| + because the generation is being replaced. |
| + - **Lost replication state, decided by the marker.** A box admitting a |
| + writer continues `holder.generation` only if `closed.json` exists |
| + for it, its `max_txid` equals the generation's remote maximum TXID |
| + over every level, and its `stamp` is the box's own `active_stamp`. |
| + **The writer consumes the marker as it opens** (deletes it by the |
| + version it read), so a later crash of that writer leaves none; this |
| + spec adds the consumption, which the claim's text implies but does |
| + not state (§19.4). Everything else is lost replication state: a |
| + crash, an OOM kill, lease expiry or takeover, a failover, a lost |
| + box, a missing or stale marker, any doubt. A wake that finds the |
| + previous writer still draining waits for it (the lease is still |
| + held). |
| + - **A cold recovery is an installing CAS** (§7.14): conditional on the |
| + observed claim, it writes a new `holder.generation`, a fresh op id |
| + never reused, and a new `holder.stamp`, the resulting `gen`, with |
| + `op.exec` this box. The box then builds the new generation from the |
| + old one, under stop evidence, and publishes it before any write is |
| + admitted. |
| + - **Writers are bound to their generation.** The replica client is |
| + constructed for the `{holder.location, holder.generation}` the |
| + writer validated under and refuses any key outside |
| + `<location>/<generation>/`: level-0 files, compaction, snapshots, |
| + retention. It never re-reads the generation. A dead writer's late |
| + uploads land in the old generation, which nothing reads once the |
| + pointer has moved; the recovery parks it as a chore after the dead |
| + writer's horizon, and the at-rest sweep takes anything later (§6.4). |
| + - **Conditional PUT alone would not do** (R7 review): if A's file won a |
| + create-only race, B would have to detect differing bytes and fail |
| + closed; the remote-position shortcut would have to check identity; |
| + multipart completion would need the same condition; and a delete |
| + marker makes a key creatable again. Disjoint generation prefixes |
| + need none of that. |
| + |
| + The model encodes all of it (§14.2.2): both completion orders and the |
| + race are witnesses whose late upload lands harmlessly in the dead |
| + generation with the rule and loses B's write without it; a stale |
| + marker forces a cold recovery; a clean close with an upload in flight |
| + writes no marker until it returns; a crash after the drain and before |
| + the marker is a cold recovery. The cost is one snapshot, one anchor and |
| + one marker per recovery, three passes at the local rate as §7.3 prices |
| + an install, and a dead generation to park. Every wake after a crash |
| + pays it; a wake after a clean close does not. |
| So: |
| - a request that completes late can only add an object to **its own** |
| 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; |
| + (another version, never opened); a late LTX PUT from an old executor, |
| + or from a dead writer of the same incarnation (step 9), lands in a |
| + generation the claim no longer names. Neither is ever restored into |
| + the current state; |
| - the claim moves to a new generation only after that generation is fully |
| installed and probed, so a restore never meets a half-written one; |
| - what lands in a dead generation after its retirement is residue, not |
| @@ -1159,7 +1279,14 @@ Phase 1 uses the claim spec's park (§6.2 there) and local retirement |
| `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). **The return to source (claim rev 6.5, R6-4).** |
| + probe (R5-4). **A cold recovery is an installing CAS too** (claim rev 6.6 §6.4a; |
| + §5.1 step 9, §7.14): it writes a new `holder.generation` and a new |
| + `holder.stamp` in one write, the box's record activates the new stamp |
| + from its next fresh read, and the recovered database and the carried |
| + files are tagged with it; the dead writer's stamp retires with it. The |
| + recovery's own `closed.json` carries the new stamp, so the first wake |
| + of the recovered generation finds it intact. **The return to source |
| + (claim rev 6.5, R6-4).** |
| `holder.stamp` always names the installation `op.exec` should run, so |
| **every CAS that changes `op.exec` writes `holder.stamp` in the same |
| write**: a CAS that makes a new installation current writes the gen it |
| @@ -1551,7 +1678,7 @@ 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; 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.5 §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) | |
| -| `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`, its CRC-64, **the encoding inputs (the header timestamp, page size, commit) and the sha256 of the database file the build produced** (R4-1, R5-1, R5-2, R6-5) | the install manifest exists | replayable: staging is immutable after the flip, the generation is new, and the build never deletes. The encoding inputs are journaled before the first PUT, so a replay encodes identical bytes, and a replay that finds its object current reuses it; a PUT that completes late lands in this generation again as another version of identical bytes, which nothing reads (§5.1) | |
| +| `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); in this order (R7-4, §5.1 step 2): **the build intent** `<location>g-<move id>/build-intent.json` with the encoding inputs (the header timestamp, page size, commit, `N`), before any PUT; the snapshot PUT, acknowledged; the anchor PUT, acknowledged; then **the completed install manifest** `<location>g-<move id>/install.json` with the snapshot's key, the `versionId` each PUT returned, `N`, each CRC-64, `integrity_check`'s result and the sha256 of the database file the build produced (R4-1, R5-1, R5-2, R6-5) | the **completed** install manifest exists; the intent alone is not completion | replayable at every boundary: staging is immutable after the flip, the generation is new, and the build never deletes. A replay reads the intent, encodes identical bytes, and reuses a snapshot or anchor it finds current under its key; a crash after the intent, after either PUT, or before the manifest leaves no completion, so `published` never runs; a PUT that completes late lands in this generation again as another version of identical bytes, which nothing reads (§5.1). The model journals the same states (`install-copy`, `install-anchor`, `published`) and refuses, as INV-11, a `generation.json` naming a snapshot or anchor that has not landed | |
| | `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.5 §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) | |
| @@ -1828,6 +1955,28 @@ process state (§5.3). |
| | rolling_back: source phases | resumes its phase from its journal; never reinstalls after `probing` | | | |
| | stuck | held; operator | | | |
| +### 7.14 Cold recovery (claim rev 6.6 §6.4a, R7-1) |
| + |
| +A wake that finds lost replication state (§5.1 step 9) runs a **cold |
| +recovery**, an operation under the claim like a push, owned by the box the |
| +claim names as `op.exec`, with these phases in `op.phase`; each is written |
| +before its side effects, and each is replayable. |
| + |
| +| phase | action | replay | |
| +|---|---|---| |
| +| the CAS | `op.kind = recovering`, a fresh op id `rec-<n>`, `op.exec` = this box, `op.base_generation` = the observed `holder.generation`; **in the same write** `holder.generation = <rec id>` and `holder.stamp` = this CAS's `gen` (the installing CAS, claim rev 6.6 §6.4a). Conditional on the observed claim, from `serving` only; it waits for no obligation, because nothing it writes overlaps a pending chore (the new generation's prefix is fresh), and the old generation's park is its own chore | | |
| +| `build` | **stop evidence first** (§5.3): nothing of the host may run while the baseline is taken, or a descendant that outlived the main process writes after the snapshot and before the generation moves (the model's seed 86799 / 100,000). The **baseline** is the warm local database when its `<dbPath>.gen` names `op.base_generation` (it holds every acknowledged write, uploaded or not), else `op.base_generation` restored by the restore contract (§5.1 steps 4 and 5), version-pinned, in this box's region. Into the new generation's prefix: the snapshot `[1, N]` (every page, `N` the baseline's position), acknowledged; the anchor `[N, N]`, acknowledged (§5.1 step 7); `closed.json {stamp: the new holder.stamp, max_txid: N}`, the installer's clean close, so the first wake finds the generation intact. The local database is the new generation's from here: `<dbPath>.gen` and `.files-gen` name it (the files are unchanged, F7), its stamp is the new one, its replication position is what the new generation's listing shows, and its first upload carries every page (fact R5-1c) | a replay that finds a snapshot current in the new generation **reuses it as the baseline** and reuses a current anchor, never rebuilding from another baseline (a warm database replaced by a restore after a second disk loss carries other bytes under the same key) | |
| +| `publish` | `generation.json` names the new generation (§5.1 step 3, conditional on the marker it supersedes); then, in one CAS, `op.phase = release` and a `park-generation` obligation for this region: the old generation's keys within `holder.location`, after the dead writer's horizon (`request time + H`); anything later is the sweep's (§6.4) | replayable: a marker already naming the new generation is not written again | |
| +| `release` | the claim returns to `serving`; the next wake admits the writer into the recovered generation, whose marker it consumes | | |
| + |
| +A recovery costs the three local passes of an install (§7.3) and a dead |
| +generation to park. It runs after every crash, OOM kill, lease takeover |
| +or lost disk, and at the first wake of a created incarnation, whose |
| +origin generation has no marker and no writer yet (the model does so; a |
| +create that wrote the marker at step 4 would need the console to write |
| +into the data bucket, and this spec does not give it that right, §19.4). |
| +It does not run after a clean close. |
| + |
| ## 8. The archive (codex 19) |
| ### 8.1 Content |
| @@ -2140,6 +2289,22 @@ newest remote level-0 TXID plus one, and every cold restore holds |
| exactly the rows written. What the file client cannot show is stated in |
| the package doc and in §14.2.6. |
| +**Rev 7.8: the Store gate asserts what it claims (R7-5), and the PUT |
| +fact (R7-1).** The gate awaits each maintenance event as a condition |
| +rather than sleeping past it (a snapshot rotation, level-1, level-2 and |
| +level-3 compactions, snapshot retention leaving exactly one snapshot, |
| +time-based level-0 expiry); its rows have distinct bodies with an update |
| +and a delete per round, and every cold restore is compared row by row; a |
| +tail with the monitors stopped writes, compacts into level 1, expires |
| +every level-0 file but the newest, and forces a restore that must take |
| +the level-1 file beyond the newest snapshot. `TestFact_R7_1_UnconditionalPut` |
| +reads the pinned S3 client's source: its `PutObjectInput` carries no |
| +`If-Match` or `If-None-Match`, and its key is prefix, level and TXID |
| +range only, the two facts §5.1 step 9 rests on. The package doc now says |
| +that S3 lists LTX files in filename order and ages them by |
| +`LastModified`, where the file client uses the encoded timestamp as the |
| +mtime. |
| + |
| **Rev 7.7: the oracles are pure (R6-1).** Every invariant check that |
| restores (INV-2 at each release, the final oracle) calls the restore |
| calculation and nothing else, and asserts afterwards that the buckets' |
| @@ -2596,6 +2761,94 @@ readiness, and same-operation lease identities. |
| review's 3 GiB workload is reproduced (108.68 s with three passes at one |
| rate, 124.04 s with the fourth) and refused by rev 7.7's arithmetic. |
| +**Rev 7.8: joint round 7 and claim rev 6.6.** |
| + |
| +- **Writer epochs (R7-1, claim rev 6.6 §6.4a).** `idleStop` is a clean |
| + close: the writer drains its uploads (`closeStep` runs while no process |
| + runs), then PUTs `closed.json {stamp, max_txid}` once (`If-None-Match`); |
| + a crash while draining forgets the close (`forget`), and an operation |
| + that takes the writer over drops it. At an ordinary wake |
| + `replicationState` continues the generation only if the marker exists, |
| + its `max_txid` is the generation's remote maximum over every level and |
| + its stamp is the box's active stamp; the writer consumes the marker (a |
| + version delete) as it opens; a wake that finds the previous writer |
| + still draining waits. Otherwise `startRecovery` is the installing CAS |
| + (`op.kind = recovering`, a fresh id, `holder.generation` and |
| + `holder.stamp` in the same write) and `recoverStep` the data path: |
| + stop evidence, the baseline (the warm database when it is the old |
| + generation's, else `restoreCalc` of the old generation, or a snapshot |
| + already current in the new generation on a replay), the snapshot, the |
| + anchor and the installer's `closed.json` each acknowledged |
| + (`ackedPut`), `generation.json`, a `park-generation` obligation for the |
| + old generation after the dead writer's horizon, release. The database |
| + replicates only into its generation (`ltxKey(db.Loc, db.Gen, ...)`), |
| + its position is what the new generation's listing shows, and its first |
| + upload carries every page. The upload loop skips a local file at or |
| + below the remote position, as litestream's does, and the writer |
| + believes it replicated (`markDurable`), which is the |
| + initialization/remote-position race. Rules `recovery-generation` (the |
| + mutation is rev 7.7's same-generation restart), `closed-marker` (the |
| + mutation takes any marker as intact and consumes none), `close-waits` |
| + (the mutation writes the marker at once). Witnesses: `wLateUploadAfter` |
| + (A's upload lands after B's), `wLateUploadRace` (A's lands after B's |
| + initialization and before B's upload: B's skip), `wExemptKeyRestored` |
| + (R7-2's counterexample), `wCrashBeforeMarker`, `wStaleMarker`, |
| + `wCloseWaits`; each checks the cold restore the moment the late upload |
| + lands, before any snapshot of the warm database could repair the |
| + replica. A created incarnation's first wake is a cold recovery (its |
| + origin generation has no marker), so are a legacy adoption's and every |
| + wake after a crash; the random sweep counts them (`cold recoveries`). |
| + The agent-crash fault takes the disk with it in one case in three, so |
| + the sweep reaches a dead writer's upload in flight across a |
| + replacement. |
| +- **The oracle checks writes by identity (R7-2).** `checkDurable` |
| + requires every durable, non-exempt write to be in the restored files' |
| + log and compares the state with `expectFrom`, the replay in |
| + acknowledgement order of exactly the writes those files carry; a write |
| + declared lost that landed anyway is replayed because it is there, no |
| + key is masked, and a later required write re-establishes its key. A |
| + full file (a snapshot, an anchor, the first upload after a cold |
| + initialization, a compaction of one) replaces the state it is applied |
| + to and carries every write it holds, which the first rev 7.8 baseline |
| + needed (seed 12436 / 30,000: a full level-0 file carried a deletion's |
| + effect without the write). |
| +- **The newest level-0 file survives every retention path (R7-3)**: |
| + compaction keeps its newest input and the expiry below the previous |
| + snapshot skips the newest level-0 file (`newest-l0`). Witness: the |
| + local position runs ahead of the uploads across two compactions and |
| + rotations. |
| +- **Builds have intent, acknowledged artifacts and completion (R7-4).** |
| + A landing, a push and a dirty rollback journal `install-copy` |
| + (snapshot acknowledged), `install-anchor` (anchor acknowledged), then |
| + `published`; `publishGen` refuses, as INV-11, a marker naming a |
| + snapshot version that does not exist or an anchor that is not current |
| + (`build-completion`: the mutation publishes from the intent). Witness: |
| + a push's build with its snapshot, then its anchor, held, and the agent |
| + crashing in between each. |
| +- **Two witnesses the sweep's new shape needed.** With a cold recovery |
| + at every crash, `evidence-whole-tree` and `timer-freeze` fell to 0 / |
| + 3,000; each has a witness now: an adopted legacy host with an escaped |
| + descendant whose move must take evidence of the whole tree (INV-1), and |
| + a registered timer whose refused deliveries while the row is held must |
| + not advance the runner's bookkeeping (a clean rollback's digest check, |
| + `stuck`). |
| +- **Retired witnesses.** `door-reread` and `door-by-version` are |
| + subsumed: a recreated incarnation's first wake is a cold recovery into |
| + a fresh generation, which a listing scoped to the generation it was |
| + authorized for never selects, so the scenario holds with C3a dropped |
| + too; C3a stays as defence in depth (`expected-outcomes.txt`). |
| +- **Model faults found and fixed this round** (all before the final |
| + numbers): the first build of a cold recovery after a lost disk restored |
| + a generation whose stale marker a failed start had already consumed |
| + (the marker is consumed as the writer opens, not at the check); a |
| + pending clean close outlived a push and wrote a marker into a dead |
| + generation; the recovered database kept stamp 0 and files-gen named |
| + the old generation; a descendant wrote during a build (stop evidence); |
| + a replayed build rebuilt the snapshot from another baseline (reuse); the |
| + crash-with-disk fault first left a nested descendant alive to |
| + acknowledge writes into no database, which the oracle rightly called |
| + lost (nothing survives a lost volume). |
| + |
| #### 14.2.3 Invariants and results |
| The invariants are the table at the end of §4, with three checks rev 6 |
| @@ -2618,7 +2871,27 @@ 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.7, on the final model (claim rev 6.5: the return to source; |
| +**Rev 7.8, on the final model (claim rev 6.6: writer epochs; the |
| +identity oracle; the newest level-0 file kept; builds with intent and |
| +completion): 30,000 seeds, zero violations; 100,000 seeds, zero |
| +violations** (60 s and 183 s). Across the 100,000 seeds: 174,931 |
| +completed operations, among them 26,380 cold recoveries (24,846 |
| +clean closes, 303 stale markers, 2,303 wakes that waited for a |
| +draining writer, 22,252 build steps that found their snapshot already |
| +current, a replay or a wait), 1,306 |
| +completed moves, 1,538 clean and 85 dirty rollbacks, 315 pre-flip |
| +reverts, 249 declared losses, 25,252 pushes, 89,404 delete-park-free |
| +cycles and 1,839 lost disks; 25,843 LTX compactions, 18,113 |
| +snapshot rotations, 1,159 level-0 upload retries, 536 uploads skipped at |
| +the remote position (a writer's own landed file, never another's), |
| +42,449 anchors and 0 anchor waits; 26,075 local stamp records lost |
| +and re-initialized; 45,522 requests completed after `H`; 32,547 staging |
| +signatures were refused as stale; 30,706 creates restarted on a 412; |
| +72 targets were stopped mid-return. Every oracle left the system |
| +unchanged. The model faults the rebuilt oracle and the new protocol found |
| +before these baselines are listed in §14.2.2. |
| + |
| +**Rev 7.7, on claim rev 6.5 (the return to source; |
| the pure restore oracle, the acknowledged anchor, compaction keeping the |
| newest level-0 file, the lost local record): 30,000 seeds, zero |
| violations; 100,000 seeds, zero violations** (35 s and 115 s). Across |
| @@ -2791,50 +3064,66 @@ 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.7 model (45f93495), with the strict classification, |
| +on the final rev 7.8 model (734a7f5b), 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 33 rules that have them. A rule is caught if |
| +same mutation, for the 38 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 **79 rules**: rev 7.6's 77 plus |
| -`anchor-acked` (§5.1 step 7, R6-1) and `return-stamp` (claim rev 6.5, |
| -R6-4). `mutate.sh 3000` exited 0: no ERROR, no unexpected MISSED, no |
| -STALE; every combination was rerun this round. Seed numbers |
| +section does too. The model has **84 rules**: rev 7.7's 79 plus |
| +`recovery-generation`, `closed-marker` and `close-waits` (claim rev 6.6 |
| +§6.4a, R7-1), `newest-l0` (R7-3) and `build-completion` (R7-4). |
| +`mutate.sh 3000` exited 0: no ERROR, no unexpected MISSED, no STALE; |
| +every combination was rerun this round. Seed numbers |
| reproduce any sweep line with `HOSTLIFE_SEED`; `HOSTLIFE_WITNESS=<rule>` |
| -replays a witness with its trace. Rev 7.6's counts are in the rev 7.6 |
| -spec (f7f7c438); the pure oracle, the acknowledged anchor, the newest |
| -level-0 file kept by compaction and the lost-record fault reshuffled the |
| -seeds, so sweep counts moved; every witness verdict is unchanged. |
| +replays a witness with its trace. Rev 7.7's counts are in the rev 7.7 |
| +spec (05f7250f); writer epochs change what every wake after a crash |
| +does, so sweep counts moved throughout; every witness verdict is |
| +unchanged, bar the two door witnesses retired (below). |
| | | rules | |
| |---|---| |
| -| caught alone by the sweep at 3,000 seeds | 58 | |
| -| caught alone by the sweep at 30,000, and by their witness | 4 (`lost-quarantine`, `markers-last`, `orphan-order`, `rollback-journal`) | |
| -| 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 | 11 | |
| +| caught alone by the sweep at 3,000 seeds | 57 | |
| +| caught alone by the sweep at 30,000, and by their witness | 5 (`evidence-whole-tree`, `markers-last`, `orphan-order`, `restore-overlap`, `staging-quiet`) | |
| +| caught alone by the sweep at 100,000, and by its witness | 3 (`close-waits`, `declare-lost-compute`, `newest-l0`) | |
| +| caught alone by their witness only; the sweep misses them at 30,000 | 5 (`closed-marker`, `live-set-region`, `recovery-generation`, `restore-gap-closed`, `rollback-journal`) | |
| +| caught only in a stated combination: the witness holds alone and under every proper subset, and violates with the partners | 7 | |
| +| subsumed: the witness holds under every combination tried | 2 (`door-reread`, `door-by-version`, by C3a and by writer epochs) | |
| | liveness only | 2 (`readiness-key`, `config-before-probe`) | |
| | unreachable under claim rev 5 | 1 (`readiness-quiet`) | |
| | unexercised | **0** | |
| -**What rev 7.7 moved.** The two new rules are caught at once: |
| -`anchor-acked` 18 / 3,000, 129 / 30,000, 497 / 100,000 (every seed where a cold restore of a |
| -snapshot-only install meets a slow anchor PUT: opened at once, the host |
| -replicates from TXID 1 and the next cold restore loses the writes); |
| -`return-stamp` 59 / 3,000, 650 / 30,000, 2,289 / 100,000 (every dirty rollback: the source |
| -activates the target's stamp, INV-6). `restore-anchor` |
| -(35 / 3,000, 394 / 30,000, 1,356 / 100,000) and `root-advance` (30 / 3,000, 369 / 30,000, 1,360 / 100,000) hold |
| -their rate; `fence-stamp` (151 / 3,000, 1,545 / 30,000) and `fence-by-installation` |
| -(142 / 3,000, 1,334 / 30,000) move with the lost-record fault and the |
| -pure oracle. Rev 7.5's generator gains stand (`generation-conditional` |
| -8 / 3,000, 370 / 100,000, `declare-lost-compute` 0 / 3,000, 1 / 100,000, |
| -`sweep-namespace` 532 / 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). |
| +**What rev 7.8 moved.** The writer-epoch rules are **witness-only**: |
| +`recovery-generation` and `closed-marker` 0 / 3,000, 0 / 30,000, 0 / |
| +100,000. The random generator reaches a dead writer's upload in flight |
| +across a replacement (the crash-with-disk fault, 1,839 lost disks in |
| +100,000 seeds) but not the two completion orders that cost the next |
| +writer a write: the late upload must land after the next writer's own |
| +upload for the same TXID, or between its initialization and its sync, |
| +and must then be met by a cold restore before a snapshot of the warm |
| +database repairs the replica. The six witnesses are the evidence for |
| +R7-1 (§14.2.2), and the sweep's zeros say nothing against the hazard |
| +(R7-2's point about "not found in 100,000 seeds" stands). `close-waits` |
| +1 / 100,000 and `newest-l0` 1 / 100,000 are caught by the sweep at depth |
| +and by their witnesses; `build-completion` 676 / 3,000, 6,645 / 30,000, |
| +22,205 / 100,000 is caught everywhere (the mutation publishes before the |
| +artifacts land, and INV-11 sees it at once). Rev 7.7's rules hold their |
| +rates (`anchor-acked` 73 / 3,000, 794 / 30,000, 2,789 / 100,000; |
| +`return-stamp` 52 / 3,000, 518 / 30,000, 1,869 / 100,000; |
| +`restore-anchor` 37 / 3,000, 374 / 30,000, 1,275 / 100,000; |
| +`root-advance` 101 / 3,000, 934 / 30,000, 3,367 / 100,000). |
| +`location-per-incarnation` (29 / 3,000, 361 / 30,000, 1,153 / 100,000) |
| +is caught less often: with every recreated incarnation's writer in a |
| +fresh generation, a shared location reuses no key, and the door |
| +combinations (`door-reread` + `location-per-incarnation` 414 / 30,000, |
| +`door-by-version` + `location-per-incarnation` 361 / 30,000) are the |
| +partner's own count; their witnesses are retired (§14.2.2). |
| +`rollback-journal` fell to 0 / 30,000 and is witness-only this round; |
| +`evidence-whole-tree` (4 / 30,000) and `timer-freeze` (29 / 30,000) |
| +gained witnesses. Five rules are witness-only: `recovery-generation`, |
| +`closed-marker`, `rollback-journal`, `live-set-region` and |
| +`restore-gap-closed`. |
| **The witnesses.** One scenario per rule the sweep catches rarely or only |
| in combination, and one per rule a review round added; two for |
| @@ -2845,45 +3134,50 @@ witness to hold there; each witness violates with the failure it names. |
| | rule | the scenario | witness alone | witness with partners | sweep alone | |
| |---|---|---|---|---| |
| -| `generation-conditional` (model 29) | push p1's first `generation.json` PUT is accepted and its response lost; the agent publishes again and p1 completes; push p2 completes; the stale PUT lands | **violated**: the marker names p1, the claim p2, and the serving box cannot start | | 8 / 3,000, 370 / 100,000 | |
| -| `lost-return-park` (model 27) | the target writes in the settle window, the settle check fails, the target is stopped after its first return PUT and declared lost | **violated**: INV-10, the lane in the source region at the release | | 1 / 3,000, 28 / 30,000, 97 / 100,000 | |
| -| `declare-lost-compute` (model 5) | the target is frozen in its settle window and its execution lease expires; the VM resumes once the source has recovered | **violated**: INV-1, two boxes run the host | | 0 / 3,000, 1 / 100,000 | |
| -| `watchdog-independent` (§7.1) | as above, with the agent alone paused, so the application keeps running | held | with `declare-lost-compute`: **violated**, INV-1 | 0 / 3,000; the pair 0 / 30,000, 1 / 100,000 | |
| -| `lost-quarantine` (CC12) | the target is stopped while landing, declared lost, and started again with its old disk | **violated**: INV-10, local state for a host served elsewhere | | 0 / 3,000, 6 / 30,000 | |
| -| `markers-last` (R2-6) | the source has a registered timer; the target's agent crashes between extracting the files and writing the marker | **violated**: INV-2, the timer is lost | | 0 / 3,000, 12 / 30,000 | |
| -| `rollback-journal` (R2-3) | a dirty rollback; the source's agent crashes after its probe spawned the instance, which wrote and replicated into the return generation | **violated**: INV-2 on cold restore | | 0 / 3,000, 4 / 30,000 | |
| -| `seal-by-version` (J-N2) | a pre-cut staging round completes after the seal; the source wrote and replicated between them | **violated**: INV-2 on cold restore; the landing installs the stale snapshot | | 3 / 3,000 | |
| -| `staging-quiet` (J-N2) | a staging round completes after the landing's staging park acknowledged, before the release | **violated**: INV-10 at the release | | 1 / 3,000, 9 / 30,000 | |
| -| `dirty-return` (INV-2) | the target writes during its probe and is rolled back | **violated**: INV-2, the write is lost | | 5 / 3,000 | |
| -| `commit-before-open` (INV-5; R3-5) | a public request reaches the target's edge while its probe runs | **violated**: INV-5 | | 11 / 3,000 | |
| -| `claim-cas-opid` (C2) | a stalled source goroutine with the rollback's last read resumes after a purge claimed the host | held | with `revalidate-before-effect`: **violated**, the store is torn down under a serving host | 0 / 3,000; the pair 1,332 / 30,000 | |
| -| `exec-admission`, `hold-op-open`, `start-check-claim-gen` (J2-R2-8) | a paused open from an earlier operation lands after the commit while the source's row is still held; a request wakes the source | held, each, and under every pair | all three: **violated**, INV-1 | 0 each; the triple 5 / 30,000, 20 / 100,000 | |
| -| `start-check` (INV-4) | the same, dropping the whole start check | held, and under every pair | with `exec-admission` and `hold-op-open`: **violated**, INV-1 | 0; the triple with `start-check` 9 / 30,000 | |
| -| `strict-spawn` (J-D3) | the source runs a main process and a descendant placed as its parent was; the move cuts | held | with `evidence-whole-tree`: **violated**, INV-1 | 0; the pair 298 / 30,000 | |
| -| `touched-incomplete` (J-N5) | a legacy host with a pre-release replica in another region is adopted, then deleted | held | with `legacy-discovery`: **violated**, INV-10 after `free` | 0; the pair 7,589 / 30,000 | |
| -| `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 420 / 30,000 | |
| -| `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 363 / 30,000 | |
| -| `registration-check` (CC21) | the first create of a host registers and its console pauses; a purge of the app drains the expired registration, tears the store down and finishes; the creator resumes | held | with `fence-etag`: **violated**; with `purge-claim-fence`: **violated** | 0 / 3,000; the pairs 245 and 270 / 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) | | 142 / 3,000, 1,334 / 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 | 151 / 3,000, 1,545 / 30,000 (a pass that selected before the record existed); the pair 2,278 / 30,000 | |
| +| `generation-conditional` (model 29) | push p1's first `generation.json` PUT is accepted and its response lost; the agent publishes again and p1 completes; push p2 completes; the stale PUT lands | **violated**: the marker names p1, the claim p2, and the serving box cannot start | | 26 / 3,000, 574 / 100,000 | |
| +| `lost-return-park` (model 27) | the target writes in the settle window, the settle check fails, the target is stopped after its first return PUT and declared lost | **violated**: INV-10, the lane in the source region at the release | | 1 / 3,000, 21 / 30,000, 68 / 100,000 | |
| +| `declare-lost-compute` (model 5) | the target is frozen in its settle window and its execution lease expires; the VM resumes once the source has recovered | **violated**: INV-1, two boxes run the host | | 0 / 3,000, 2 / 100,000 | |
| +| `watchdog-independent` (§7.1) | as above, with the agent alone paused, so the application keeps running | held | with `declare-lost-compute`: **violated**, INV-1 | 0 / 3,000; the pair 2 / 30,000, 6 / 100,000 | |
| +| `lost-quarantine` (CC12) | the target is stopped while landing, declared lost, and started again with its old disk | **violated**: INV-10, local state for a host served elsewhere | | 2 / 3,000, 14 / 30,000 | |
| +| `markers-last` (R2-6) | the source has a registered timer; the target's agent crashes between extracting the files and writing the marker | **violated**: INV-2, the timer is lost | | 0 / 3,000, 10 / 30,000 | |
| +| `rollback-journal` (R2-3) | a dirty rollback; the source's agent crashes after its probe spawned the instance, which wrote and replicated into the return generation | **violated**: INV-2 on cold restore | | 0 / 3,000, 0 / 30,000 | |
| +| `seal-by-version` (J-N2) | a pre-cut staging round completes after the seal; the source wrote and replicated between them | **violated**: INV-2 on cold restore; the landing installs the stale snapshot | | 1 / 3,000 | |
| +| `staging-quiet` (J-N2) | a staging round completes after the landing's staging park acknowledged, before the release | **violated**: INV-10 at the release | | 0 / 3,000, 3 / 30,000 | |
| +| `dirty-return` (INV-2) | the target writes during its probe and is rolled back | **violated**: INV-2, the write is lost | | 2 / 3,000 | |
| +| `commit-before-open` (INV-5; R3-5) | a public request reaches the target's edge while its probe runs | **violated**: INV-5 | | 3 / 3,000 | |
| +| `claim-cas-opid` (C2) | a stalled source goroutine with the rollback's last read resumes after a purge claimed the host | held | with `revalidate-before-effect`: **violated**, the store is torn down under a serving host | 0 / 3,000; the pair 897 / 30,000 | |
| +| `exec-admission`, `hold-op-open`, `start-check-claim-gen` (J2-R2-8) | a paused open from an earlier operation lands after the commit while the source's row is still held; a request wakes the source | held, each, and under every pair | all three: **violated**, INV-1 | 0 each; the triple 5 / 30,000, 13 / 100,000 | |
| +| `start-check` (INV-4) | the same, dropping the whole start check | held, and under every pair | with `exec-admission` and `hold-op-open`: **violated**, INV-1 | 0; the triple with `start-check` 6 / 30,000 | |
| +| `strict-spawn` (J-D3) | the source runs a main process and a descendant placed as its parent was; the move cuts | held | with `evidence-whole-tree`: **violated**, INV-1 | 0; the pair 121 / 30,000 | |
| +| `touched-incomplete` (J-N5) | a legacy host with a pre-release replica in another region is adopted, then deleted | held | with `legacy-discovery`: **violated**, INV-10 after `free` | 0; the pair 7,825 / 30,000 | |
| +| `registration-check` (CC21) | the first create of a host registers and its console pauses; a purge of the app drains the expired registration, tears the store down and finishes; the creator resumes | held | with `fence-etag`: **violated**; with `purge-claim-fence`: **violated** | 0 / 3,000; the pairs 243 and 263 / 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) | | 484 / 3,000, 4,242 / 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 | 351 / 3,000, 3,434 / 30,000; the pair 4,354 / 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 | | 532 / 3,000 (the retention fixture, populated 2 to 33) | |
| +| `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 | | 539 / 3,000 (the retention fixture, populated 2 to 33) | |
| | `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 / 3,000, 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) | | 2 / 3,000, 7 / 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, 3 / 30,000 | |
| | `restore-gap-closed` (§5.1, R4-1) | the same generation with the next file missing and the one after current | **violated**: a restore across the gap returns a database short of the acknowledged writes | | 0 / 3,000, 0 / 30,000 | |
| -| `restore-anchor` (§5.1 step 7, R5-1) | a push installs a snapshot alone; the host wakes, writes three times, replicates, loses its disk and wakes cold | **violated**: INV-2, every write since the push is lost: replication restarted at TXID 1 below the snapshot and the planner skipped the files (facts R5-1a, b) | | 35 / 3,000, 394 / 30,000, 1,356 / 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) | | 30 / 3,000, 369 / 30,000, 1,360 / 100,000 | |
| -| `anchor-acked` (§5.1 step 7, R6-1) | a push installs a snapshot alone; the install's anchor PUT is held across forty attempted opens, then released; the host writes, replicates, loses its disk and wakes cold | **violated**: the host opened before its anchor was acknowledged; litestream's position would be 0 and the writes below the snapshot are lost on the cold restore (INV-2) | | 18 / 3,000, 129 / 30,000, 497 / 100,000 | |
| -| `return-stamp` (claim rev 6.5, R6-4) | a dirty rollback; the source's local stamp record is lost after the target's return; the return CAS writes the source installation's stamp back and the source re-initializes from it, installs under it and serves under its probe CAS's new stamp | **violated**: the source activates the target's stamp, issued for another box's installation (INV-6) | | 59 / 3,000, 650 / 30,000, 2,289 / 100,000 | |
| -| `recovery-current-inputs` (§7.7, §7.8; R2-5) | a bundle is published after admission; the target writes; the rollback is dirty | **violated**: `stuck` | | 44 / 3,000 | |
| +| `restore-anchor` (§5.1 step 7, R5-1) | a push installs a snapshot alone; the host wakes, writes three times, replicates, loses its disk and wakes cold | **violated**: INV-2, every write since the push is lost: replication restarted at TXID 1 below the snapshot and the planner skipped the files (facts R5-1a, b) | | 37 / 3,000, 374 / 30,000, 1,275 / 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) | | 101 / 3,000, 934 / 30,000, 3,367 / 100,000 | |
| +| `anchor-acked` (§5.1 step 7, R6-1) | a push installs a snapshot alone; the install's anchor PUT is held across forty attempted opens, then released; the host writes, replicates, loses its disk and wakes cold | **violated**: the host opened before its anchor was acknowledged; litestream's position would be 0 and the writes below the snapshot are lost on the cold restore (INV-2) | | 73 / 3,000, 794 / 30,000, 2,789 / 100,000 | |
| +| `return-stamp` (claim rev 6.5, R6-4) | a dirty rollback; the source's local stamp record is lost after the target's return; the return CAS writes the source installation's stamp back and the source re-initializes from it, installs under it and serves under its probe CAS's new stamp | **violated**: the source activates the target's stamp, issued for another box's installation (INV-6) | | 52 / 3,000, 518 / 30,000, 1,869 / 100,000 | |
| +| `recovery-generation` (claim rev 6.6 §6.4a, R7-1), three scenarios and a crash | writer A's upload `[N+1]` is held in flight, A dies with its disk, B wakes; (i) B replicates its own `[N+1]`, then A's lands; (ii) A's lands after B's position is initialized and before B's upload, so litestream's loop skips B's file; (iii) A's held write updated K, B durably updates K, A's lands; (iv) a clean stop drains, then the agent crashes before `closed.json` | **violated** in each: with the rule B recovers into a fresh generation and A's file lands in the dead one; without it B's acknowledged write is lost on the cold restore taken the moment A's file lands (INV-2), or no recovery runs after the crash (iv) | | 0 / 3,000, 0 / 30,000, 0 / 100,000 | |
| +| `closed-marker` (claim rev 6.6 §6.4a) | a stale `closed.json` (`max_txid` behind the remote maximum) beside the dead writer's outstanding upload | **violated**: taken as intact, B continues in place and A's late file replaces B's (INV-2) | | 0 / 3,000, 0 / 30,000, 0 / 100,000 | |
| +| `close-waits` (claim rev 6.6 §6.4a) | a clean stop with an upload in flight | **violated**: written at once, the marker vouches for an upload that has not returned | | 0 / 3,000, 0 / 30,000, 1 / 100,000 | |
| +| `newest-l0` (§5.1 step 8, R7-3) | the local position runs ahead of the uploads across two compactions and snapshot rotations | **violated**: retention below the previous snapshot removes the newest uploaded level-0 file | | 0 / 3,000, 0 / 30,000, 1 / 100,000 | |
| +| `build-completion` (§5.1 step 2, §7.6, R7-4) | a push's build with its snapshot, then its anchor, held, the agent crashing in between each | **violated**: `generation.json` published before its snapshot landed (INV-11) | | 676 / 3,000, 6,645 / 30,000, 22,205 / 100,000 | |
| +| `evidence-whole-tree` (§6.1, J-D3) | an adopted legacy host runs a descendant outside the cgroup; the move cuts | **violated**: evidence blind to the escapee certifies the stop and two boxes run the host (INV-1) | | 0 / 3,000, 4 / 30,000 | |
| +| `timer-freeze` (J-N14) | a registered timer on the source; the move holds the row; the runner's deliveries are refused; a clean rollback | **violated**: the refused deliveries advanced the runner's bookkeeping, the timer digest differs from the stop's, the source is `stuck` | | 1 / 3,000, 29 / 30,000 | |
| +| `recovery-current-inputs` (§7.7, §7.8; R2-5) | a bundle is published after admission; the target writes; the rollback is dirty | **violated**: `stuck` | | 41 / 3,000 | |
| **The purge fence, the ETag condition and C5a.** `purge-claim-fence` |
| -(CC21) is caught alone by the sweep: 31 / 3,000, 244 / 30,000. |
| -`fence-etag` (CC22): 29 / 3,000, 215 / 30,000. `claim-never-deleted` |
| +(CC21) is caught alone by the sweep: 28 / 3,000, 240 / 30,000. |
| +`fence-etag` (CC22): 28 / 3,000, 214 / 30,000. `claim-never-deleted` |
| (C5a): 3 / 3,000, 44 / 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`, 348 / 30,000); |
| -its two pairs 245 and 270 / 30,000. |
| +alone is shown insufficient (`purge-claim-fence` + `fence-etag`, 343 / 30,000); |
| +its two pairs 243 and 263 / 30,000. |
| **Rev 6's unexercised three, now caught (the biased schedule, §14.2.2).** |
| @@ -2899,48 +3193,50 @@ 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: 65 of 79** (58 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 ‡). |
| +**Caught alone: 70 of 84** (57 by the sweep at 3,000; 5 by the sweep at |
| +30,000 and by their witness, marked †; 3 at 100,000 and by its witness, |
| +marked ††; 5 by their witness alone, marked ‡). |
| | rule | seeds failing | | rule | seeds failing | |
| |---|---|---|---|---| |
| -| `recovery-pass` | 2,484 / 3,000 | | `fresh-incarnation` | 50 / 3,000 | |
| -| `legacy-discovery` | 400 / 3,000, 3,979 / 30,000 | | `location-per-incarnation` | 28 / 3,000, 363 / 30,000 | |
| -| `park-by-version` | 2,506 / 3,000 | | `park-all-versions` | 554 / 3,000 | |
| -| `park-skip-lock` | 2,718 / 3,000 | | `retirement-ids` | 314 / 3,000 | |
| -| `quiet-before-ack` | 209 / 3,000 | | `straggler-sweep` | 771 / 3,000 | |
| -| `sweep-staging` | 45 / 3,000 | | `sweep-namespace` | 532 / 3,000 | |
| -| `restore-by-generation` | 120 / 3,000 | | `restore-overlap` | 2 / 3,000, 7 / 30,000 | |
| -| `restore-gap-closed` ‡ | witness; sweep 0 / 30,000 | | `hostguard` | 6 / 3,000 | |
| -| `restore-anchor` | 35 / 3,000, 394 / 30,000, 1,356 / 100,000 | | `root-advance` | 30 / 3,000, 369 / 30,000, 1,360 / 100,000 | |
| -| `anchor-acked` | 18 / 3,000, 129 / 30,000, 497 / 100,000 | | `return-stamp` | 59 / 3,000, 650 / 30,000, 2,289 / 100,000 | |
| -| `purge-reserve-first` | 2,177 / 3,000 | | `purge-adopts` | 6 / 3,000 | |
| -| `purge-journal` | 1,946 / 3,000 | | `admission-registration` | 41 / 3,000 | |
| -| `registration-recovery` | 2,117 / 3,000 | | `purge-claim-fence` | 31 / 3,000, 244 / 30,000 | |
| -| `fence-etag` | 29 / 3,000, 215 / 30,000 | | `claim-never-deleted` | 3 / 3,000, 44 / 30,000 | |
| -| `cancelled-creates` | 376 / 3,000 | | `orphan-no-deadline` | 49 / 3,000 | |
| -| `orphan-order` † | 0 / 3,000, 1 / 30,000 | | `evidence-whole-tree` | 8 / 3,000, 103 / 30,000 | |
| -| `evidence-from-state` | 2,588 / 3,000 | | `floor-boot-recovery` | 2,614 / 3,000 | |
| -| `participant-rows` | 10 / 3,000 | | `revalidate-before-effect` | 65 / 3,000, 570 / 30,000 | |
| -| `sign-before-safeuntil` | 22 / 3,000 | | `sign-at-check` | 10 / 3,000 | |
| -| `sdk-no-resign` | 9 / 3,000 | | `lost-quarantine` † | 0 / 3,000, 6 / 30,000 | |
| -| `declare-lost-compute` †† | 0 / 3,000, 1 / 100,000 | | `cut-deadline` | 9 / 3,000 | |
| -| `revert-journal` | 12 / 3,000 | | `rollback-journal` † | 0 / 3,000, 4 / 30,000 | |
| -| `dirty-return` | 5 / 3,000 | | `commit-before-open` | 11 / 3,000 | |
| -| `lost-return-park` | 1 / 3,000, 28 / 30,000, 97 / 100,000 | | `target-park` | 38 / 3,000 | |
| -| `abort-target-owner` | 920 / 3,000 | | `timer-freeze` | 9 / 3,000 | |
| -| `timer-canonical` | 1 / 3,000 | | `markers-last` † | 0 / 3,000, 12 / 30,000 | |
| -| `source-readiness` | 13 / 3,000 | | `seal-by-version` | 3 / 3,000 | |
| -| `staging-quiet` | 1 / 3,000, 9 / 30,000 | | `fresh-admission` | 12 / 3,000 | |
| -| `stale-hold-release` | 4 / 3,000 | | `obligations-block-ops` | 44 / 3,000 | |
| -| `claim-op-exclusive` | 76 / 3,000 | | `recovery-current-inputs` | 44 / 3,000 | |
| -| `files-carried` | 65 / 3,000 | | `generation-conditional` | 8 / 3,000, 370 / 100,000 | |
| -| `fence-by-installation` | 142 / 3,000, 1,334 / 30,000 | | `live-set-region` ‡ | witness; sweep 0 / 30,000 | |
| -| `fence-stamp` | 151 / 3,000, 1,545 / 30,000 | | | | |
| - |
| -**Caught only in a combination: 11 rules**, every combination rerun this |
| -round. `fence-stamp`'s pair with `hostguard` is still reported because |
| +| `recovery-pass` | 2,494 / 3,000 | | `fresh-incarnation` | 44 / 3,000 | |
| +| `legacy-discovery` | 459 / 3,000, 4,628 / 30,000 | | `location-per-incarnation` | 29 / 3,000, 361 / 30,000, 1,153 / 100,000 | |
| +| `park-by-version` | 2,544 / 3,000 | | `park-all-versions` | 546 / 3,000 | |
| +| `park-skip-lock` | 2,716 / 3,000 | | `retirement-ids` | 302 / 3,000 | |
| +| `quiet-before-ack` | 201 / 3,000 | | `straggler-sweep` | 759 / 3,000 | |
| +| `sweep-staging` | 40 / 3,000 | | `sweep-namespace` | 539 / 3,000 | |
| +| `restore-by-generation` | 136 / 3,000 | | `restore-overlap` † | 0 / 3,000, 3 / 30,000 | |
| +| `restore-gap-closed` ‡ | witness; sweep 0 / 30,000 | | `hostguard` | 7 / 3,000 | |
| +| `restore-anchor` | 37 / 3,000, 374 / 30,000, 1,275 / 100,000 | | `root-advance` | 101 / 3,000, 934 / 30,000, 3,367 / 100,000 | |
| +| `anchor-acked` | 73 / 3,000, 794 / 30,000, 2,789 / 100,000 | | `return-stamp` | 52 / 3,000, 518 / 30,000, 1,869 / 100,000 | |
| +| `recovery-generation` ‡ | witness; sweep 0 / 30,000, 0 / 100,000 | | `closed-marker` ‡ | witness; sweep 0 / 30,000, 0 / 100,000 | |
| +| `close-waits` †† | 0 / 3,000, 0 / 30,000, 1 / 100,000 | | `newest-l0` †† | 0 / 3,000, 0 / 30,000, 1 / 100,000 | |
| +| `build-completion` | 676 / 3,000, 6,645 / 30,000, 22,205 / 100,000 | | `purge-reserve-first` | 2,186 / 3,000 | |
| +| `purge-adopts` | 6 / 3,000 | | `purge-journal` | 1,976 / 3,000 | |
| +| `admission-registration` | 37 / 3,000 | | `registration-recovery` | 2,137 / 3,000 | |
| +| `purge-claim-fence` | 28 / 3,000, 240 / 30,000 | | `fence-etag` | 28 / 3,000, 214 / 30,000 | |
| +| `claim-never-deleted` | 3 / 3,000, 44 / 30,000 | | `cancelled-creates` | 377 / 3,000 | |
| +| `orphan-no-deadline` | 47 / 3,000 | | `orphan-order` † | 0 / 3,000, 1 / 30,000 | |
| +| `evidence-whole-tree` † | 0 / 3,000, 4 / 30,000 | | `evidence-from-state` | 2,821 / 3,000 | |
| +| `floor-boot-recovery` | 2,605 / 3,000 | | `participant-rows` | 1 / 3,000 | |
| +| `revalidate-before-effect` | 19 / 3,000, 150 / 30,000 | | `sign-before-safeuntil` | 30 / 3,000 | |
| +| `sign-at-check` | 23 / 3,000 | | `sdk-no-resign` | 18 / 3,000 | |
| +| `lost-quarantine` | 2 / 3,000, 14 / 30,000 | | `declare-lost-compute` †† | 0 / 3,000, 2 / 100,000 | |
| +| `cut-deadline` | 6 / 3,000 | | `revert-journal` | 12 / 3,000 | |
| +| `rollback-journal` ‡ | witness; sweep 0 / 30,000 | | `dirty-return` | 2 / 3,000 | |
| +| `commit-before-open` | 3 / 3,000 | | `lost-return-park` | 1 / 3,000, 21 / 30,000, 68 / 100,000 | |
| +| `target-park` | 30 / 3,000 | | `abort-target-owner` | 894 / 3,000 | |
| +| `timer-freeze` | 1 / 3,000, 29 / 30,000 | | `timer-canonical` | 1 / 3,000 | |
| +| `markers-last` † | 0 / 3,000, 10 / 30,000 | | `source-readiness` | 13 / 3,000 | |
| +| `seal-by-version` | 1 / 3,000 | | `staging-quiet` † | 0 / 3,000, 3 / 30,000 | |
| +| `fresh-admission` | 9 / 3,000 | | `stale-hold-release` | 3 / 3,000 | |
| +| `obligations-block-ops` | 40 / 3,000 | | `claim-op-exclusive` | 78 / 3,000 | |
| +| `recovery-current-inputs` | 41 / 3,000 | | `files-carried` | 50 / 3,000 | |
| +| `generation-conditional` | 26 / 3,000, 574 / 100,000 | | `fence-by-installation` | 484 / 3,000, 4,242 / 30,000 | |
| +| `live-set-region` ‡ | witness; sweep 0 / 30,000 | | `fence-stamp` | 351 / 3,000, 3,434 / 30,000 | |
| + |
| +**Caught only in a combination: 9 rules**, every combination rerun this |
| +round; `door-reread` and `door-by-version` left the list (subsumed, above). `fence-stamp`'s 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 |
| @@ -2948,21 +3244,24 @@ subset in the gate. |
| | combination | sweep | partners alone (sweep) | witness | what the model finds | |
| |---|---|---|---|---| |
| -| `purge-claim-fence` + `fence-etag` (**the re-read alone**, rev 7's CC21 as proposed) | 348 / 30,000 | `purge-claim-fence` 244, `fence-etag` 215, `registration-check` 0 | (the two `registration-check` rows below) | a store destroyed under a creating or serving host | |
| -| `registration-check` + `purge-claim-fence` | 270 / 30,000 | `purge-claim-fence` 244 | violated | the same | |
| -| `registration-check` + `fence-etag` | 245 / 30,000 | `fence-etag` 215 | violated | the same | |
| -| `exec-admission` + `hold-op-open` + `start-check-claim-gen` | 5 / 30,000, 20 / 100,000 | every pair 0 / 30,000 (rev 7.5) | violated | two writers, Astra's J2-R2-8 trace | |
| -| `exec-admission` + `hold-op-open` + `start-check` | 9 / 30,000 | (above) | violated | the same, dropping the whole start check | |
| -| `door-reread` + `location-per-incarnation` | 420 / 30,000 | `location-per-incarnation` 363 / 30,000 | violated | door reads of another incarnation's data (196) | |
| -| `door-by-version` + `location-per-incarnation` | 363 / 30,000 | `location-per-incarnation` 363 / 30,000 | violated | door reads of another incarnation's data (60); the sweep count is the partner's, the witness is the evidence | |
| -| `claim-cas-opid` + `revalidate-before-effect` | 1,332 / 30,000 | `revalidate-before-effect` 570 / 30,000 | violated | a stale step destroys a store | |
| -| `strict-spawn` + `evidence-whole-tree` | 298 / 30,000 | `evidence-whole-tree` 103 / 30,000 | violated | two writers | |
| -| `touched-incomplete` + `legacy-discovery` | 7,589 / 30,000 | `legacy-discovery` 3,979 / 30,000 | violated | a freed host's residue | |
| -| `declare-lost-compute` + `watchdog-independent` | 0 / 30,000, 1 / 100,000 | `declare-lost-compute` 0 / 3,000, 1 / 100,000, `watchdog-independent` 0 / 3,000 | violated | two writers after a paused or frozen target resumes | |
| -| `fence-stamp` + `hostguard` (no longer combination-only) | 2,278 / 30,000 | `hostguard` 6 / 3,000, `fence-stamp` 151 / 3,000, 1,545 / 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 | |
| - |
| -Every combination was rerun on the rev 7.7 model; the pairwise zeros of |
| -the admission triple are rev 7.5's and were not rerun. |
| +| `purge-claim-fence` + `fence-etag` (**the re-read alone**, rev 7's CC21 as proposed) | 343 / 30,000 | `purge-claim-fence` 240, `fence-etag` 214, `registration-check` 0 | (the two `registration-check` rows below) | a store destroyed under a creating or serving host | |
| +| `registration-check` + `purge-claim-fence` | 263 / 30,000 | `purge-claim-fence` 240 | violated | the same | |
| +| `registration-check` + `fence-etag` | 243 / 30,000 | `fence-etag` 214 | violated | the same | |
| +| `exec-admission` + `hold-op-open` + `start-check-claim-gen` | 5 / 30,000, 13 / 100,000 | every pair 0 / 30,000 (rev 7.5) | violated | two writers, Astra's J2-R2-8 trace | |
| +| `exec-admission` + `hold-op-open` + `start-check` | 6 / 30,000 | (above) | violated | the same, dropping the whole start check | |
| +| `door-reread` + `location-per-incarnation` | 414 / 30,000 (the partner's count; witness retired) | `location-per-incarnation` 361 / 30,000 | violated | door reads of another incarnation's data (196) | |
| +| `door-by-version` + `location-per-incarnation` | 361 / 30,000 (the partner's count; witness retired) | `location-per-incarnation` 361 / 30,000 | violated | door reads of another incarnation's data (60); the sweep count is the partner's, the witness is the evidence | |
| +| `claim-cas-opid` + `revalidate-before-effect` | 897 / 30,000 | `revalidate-before-effect` 150 / 30,000 | violated | a stale step destroys a store | |
| +| `strict-spawn` + `evidence-whole-tree` | 121 / 30,000 | `evidence-whole-tree` 4 / 30,000 | violated | two writers | |
| +| `touched-incomplete` + `legacy-discovery` | 7,825 / 30,000 | `legacy-discovery` 4,628 / 30,000 | violated | a freed host's residue | |
| +| `declare-lost-compute` + `watchdog-independent` | 2 / 30,000, 6 / 100,000 | `declare-lost-compute` 0 / 3,000, 2 / 100,000, `watchdog-independent` 0 / 3,000 | violated | two writers after a paused or frozen target resumes | |
| +| `fence-stamp` + `hostguard` (no longer combination-only) | 4,354 / 30,000 | `hostguard` 7 / 3,000, `fence-stamp` 351 / 3,000, 3,434 / 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 | |
| + |
| +Every combination was rerun on the rev 7.8 model; the pairwise zeros of |
| +the admission triple are rev 7.5's and were not rerun. The door pairs |
| +now show the partner's own count: the witnesses that separated them are |
| +retired (§14.2.2), and the rows stay as a record that the pairs add |
| +nothing over C3a alone under writer epochs. |
| **Liveness only: 2.** `readiness-key` (T2) and `config-before-probe`. |
| They have no witness: neither can violate an invariant. |
| @@ -2972,8 +3271,8 @@ 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; 34 witnesses, 110 runs); the 30,000- and 100,000-seed |
| -baselines, this sweep and the witnesses are the evidence for rev 7.7. |
| +a second; 42 witnesses, 122 runs); the 30,000- and 100,000-seed |
| +baselines, this sweep and the witnesses are the evidence for rev 7.8. |
| #### 14.2.6 What the model does not prove |
| @@ -3020,12 +3319,18 @@ baselines, this sweep and the witnesses are the evidence for rev 7.7. |
| 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, keeping the newest); |
| - `integrity_check`. |
| -- **What the file client cannot show (R6 review).** `litestreamfacts` |
| - drives the pinned library through its file replica client. S3 orders |
| - and ages objects by `LastModified`, the file client by the encoded LTX |
| - timestamp kept as the file's mtime, so a copied or late-landing object |
| - can age differently for retention on S3; S3 keeps versions and delete |
| + `integrity_check`; a writer bound to its generation is modelled as |
| + keys under `db.Gen` and never as a client that refuses other keys; |
| + conditional PUTs are not used, so the review's list of what a |
| + create-only PUT would still need (differing bytes, the shortcut's |
| + identity, multipart, delete markers) stays a list. |
| +- **What the file client cannot show (R6 and R7 reviews).** `litestreamfacts` |
| + drives the pinned library through its file replica client. S3 lists LTX |
| + files in filename order and ages them for retention by `LastModified`, |
| + the file client by the encoded LTX timestamp kept as the file's mtime, |
| + so a copied or late-landing object can age differently for retention |
| + on S3; an upload outstanding across a writer replacement, the R7-1 |
| + hazard, is the model's, not the file client's; S3 keeps versions and delete |
| markers where the file client replaces and deletes outright; S3 |
| requests complete late. Those are the model's (versions, markers, late |
| completion, §14.2.2) and §15 step 8's (the S3 behaviours). The |
| @@ -3343,6 +3648,26 @@ 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. |
| +**Claim rev 6.6 (b10547e1), after joint round 7: no change requested, |
| +three notes.** Rev 6.6's §6.4a, writer epochs, answers R7-1: a clean |
| +close drains then writes `closed.json` once; a writer continues a |
| +generation only with an intact marker; everything else is a cold |
| +recovery, an installing CAS into a fresh generation with a new stamp; |
| +writers are bound to their generation. Rev 7.8 encodes it (§5.1 step 9, |
| +§7.14, §14.2.2) and owns the data path. Notes for platform-1e |
| +(`moves-claim-questions.md`, rev 7.8 heading): the marker is **consumed |
| +by the writer as it opens**, which the text implies ("written once") but |
| +does not state, and without which a continued writer that crashes leaves |
| +the earlier marker in place with a `max_txid` that may still equal the |
| +remote maximum (its own uploads in flight) and so look intact; the first |
| +wake of a **created** incarnation and of an adopted legacy host is a cold |
| +recovery under the literal rule, because no writer has closed the origin |
| +generation and the console cannot write the marker into the data bucket, |
| +which costs one recovery generation per create; and the recovery's |
| +baseline is the **warm database** when it is the old generation's, since |
| +it holds acknowledged writes the old generation may not, which the |
| +claim's "restores from the old generation" should be read to allow. |
| + |
| **Claim rev 6.5 (d36adcfa), after joint round 6: no request from this |
| spec.** Rev 6.5 answers R6-4 with one invariant: `holder.stamp` always |
| names the installation `op.exec` should run, so any CAS that changes |
| @@ -3671,3 +3996,18 @@ answers the rest and reruns every number. |
| | R6-5 (P3) replayed anchor bytes differ (the encoder's `time.Now()`) | the encoding inputs, timestamp included, are journaled in the install manifest before the PUTs and a replay reuses a current object (§5.1 step 2, §7.6 `building`); `TestFact_R6_5_AnchorReplayBytes` shows identical bytes for identical inputs and different bytes one millisecond apart | |
| | fidelity: compaction deleted the newest level-0 file, creating anchor-required cold restores the library would not | compaction keeps the newest input (§14.2.2); time-based level-0 retention stays deferred (§14.2.6) | |
| +### 22.14 Joint round 7 (claim d36adcfa, moves rev 7.7 05f7250f, model 05f7250f) |
| + |
| +The claim stayed ready; every R6 finding was resolved bar R6-5's |
| +ordering (R7-4); the round-7 hazard rev 7.7's note raised was judged a |
| +P1. Claim rev 6.6 (b10547e1) answered R7-1 with §6.4a, writer epochs. |
| + |
| +| finding | rev 7.8 | |
| +|---|---| |
| +| R7-1 (P1) a cold recovery reuses an LTX key while the previous writer's upload is in flight; the PUT is unconditional, the key is level and range only, `lock.json` revokes nothing; two schedules (A lands after B's upload; A lands between B's initialization and B's sync, which then skips B's file) | claim rev 6.6 §6.4a encoded: the clean-close marker, lost replication state decided by it, cold recovery as an installing CAS into a fresh generation, writers bound to their generation (§5.1 step 9, §7.14, §6.4). The data path: stop evidence, the warm database or the restored old generation as baseline, snapshot, anchor and marker acknowledged, publish, release, the old generation parked as a chore; the marker consumed as the writer opens. `TestFact_R7_1_UnconditionalPut` reads the two facts from the pinned source. Witnesses for both completion orders and the race, each checking the cold restore the moment the late upload lands, a stale marker, a crash before the marker, and a clean close that waits; rules `recovery-generation`, `closed-marker`, `close-waits` (§14.2.5) | |
| +| R7-2 (P2) the per-key mask hides a later durable write; required-write coverage by maximum TXID is insufficient after a fork | coverage by write identity and the state compared with the replay of exactly the writes the restored files carry (§14.2.2); the counterexample is `wExemptKeyRestored`; full files replace the state and carry every write, which the rebuilt oracle exposed | |
| +| R7-3 (P2) the second retention loop still removes the newest level-0 file | kept in every path (§5.1 step 8; `newest-l0`, witness with the local position ahead of the uploads) | |
| +| R7-4 (P2) the build-input journal and the completion manifest are one object; a crash between them satisfies the completion predicate | `build-intent.json` before any PUT, `install.json` only after both PUTs returned with their identities and verification results, `generation.json` only from completion (§5.1 step 2, §7.6); INV-11 in the model, `build-completion`, witness with crashes between the steps | |
| +| R7-5 (P3) the Store gate asserted less than it claimed | each maintenance event awaited as a condition, row contents compared with updates and deletes, a restore forced through compacted continuation files (§14.2.1); the listing-order wording fixed | |
| +| retained from R6: the door combinations | `door-reread` and `door-by-version` witnesses retired: writer epochs put a recreated incarnation under a fresh generation the listing never selects (§14.2.5) | |
| + |