amadan
spec: move-any-app rev 7.7: joint round 6, claim rev 6.5 encoded, every number rerun (#175)
Written against claim rev 6.5 (d36adcfa). R6-1: the restore is a pure calculation for every oracle; the activator opens replication only once the anchor PUT is acknowledged and reads the position from the listing (§5.1 step 7; anchor-acked); oracles assert their purity (§14.2.1, §14.2.2). R6-2: litestreamfacts asserts exact facts and gains the anchored lineage through the Store (§14.2.1); the file client's limits stated (§14.2.6). R6-3: `restored` verifies the database `building` produced instead of restoring again; T11 prices regional S3, the disk and the verification read; one worked example in spec, note and test (§7.3, §7.6). R6-4: the return to source as claim rev 6.5 states it: the flip journals the source's stamp, the return CAS writes it back, a lost record re-initializes from it, activation tags artifacts, retire-artifacts parks by tag (§6.4, §7.8; return-stamp). R6-5: the anchor's encoding inputs are journaled before the PUTs (§5.1 step 2, §7.6). §14.2.3 and §14.2.5 rerun in full on 45f93495: 79 rules, 34 witnesses, 30,000 and 100,000 seeds clean, every combination rerun; §19.4 claim rev 6.5; §22.13 dispositions.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
1 file changed,
+387
−150
docs/superpowers/specs/2026-10-02-move-any-app-design.md+387 −150
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 00a689154..68161e282 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,47 @@ |
| # Move any app or instance to another region: Phase 1, a safe single-instance move |
| **Date:** 2026-10-03 |
| -**Revision:** 7.6. |
| +**Revision:** 7.7. |
| + |
| +- **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), |
| + whose new invariant answers R6-4: `holder.stamp` always names the |
| + installation `op.exec` should run, so every CAS that changes `op.exec` |
| + writes it, a new installation's new gen or an existing installation's |
| + own stamp from the op journal; §22.13 has every disposition. Round 6 |
| + judged the claim ready for planning and found no P1. **R6-1 (P2):** the |
| + model's restore oracle wrote anchors into the system it checked and |
| + granted a position before the anchor PUT succeeded; the restore is now |
| + a pure calculation (`restoreCalc`) that every oracle uses, and the |
| + activator's initialization (`restoreInit`) opens replication only once |
| + the anchor PUT is **acknowledged**, reading the position from the |
| + listing, never from the restored TXID (§5.1 step 7; rule |
| + `anchor-acked`, witness: the anchor PUT held across attempted opens); |
| + every oracle asserts its purity (buckets, versions, queues, anchors, |
| + console, random draws unchanged), and every number in §14.2 is rerun. |
| + **R6-2 (P2):** `litestreamfacts` asserts exact facts and fails on any |
| + alternative (the newest level-0 file retained by identity, the next |
| + TXID exactly `N + 1`, every row, the original continuation gone, the |
| + rooted restore's exact refusal), and gains the missing integration |
| + gate: one anchored lineage through the production Store shape with |
| + compaction, snapshot rotation, time-based level-0 expiry, disk loss and |
| + repeated cold restores, exact positions and contents asserted |
| + (§14.2.1). **R6-3 (P2):** the `restored` phase **verifies** the database |
| + `building` produced instead of restoring it again, T11 prices regional |
| + S3 and the disk separately and the verification pass too, and the |
| + worked example is one set of numbers in the spec, the note and the test |
| + (2 GiB at 10 / 250 / 500 MiB/s: 53.6 s fixed, one attempt; §7.3, §7.6). |
| + **R6-4 (P3):** the return to source encoded as claim rev 6.5 states it |
| + (the flip keeps the source's stamp in the journal, the return CAS |
| + writes it back, a lost local record re-initializes from it, artifacts |
| + are tagged when the new stamp activates, `retire-artifacts` parks by |
| + tag; §6.4, §7.8; rule `return-stamp`, witness: a dirty return with a |
| + lost local record). **R6-5 (P3):** the anchor's encoding inputs, the |
| + header timestamp included, are persisted in the install manifest so a |
| + replayed PUT repeats identical bytes (§5.1 step 2; |
| + `TestFact_R6_5_AnchorReplayBytes`). Compaction in the model keeps the |
| + newest level-0 file, as litestream's retention does. 79 rules, 34 |
| + witnesses. Results in §14.2.3 and §14.2.5. |
| - **Rev 7.6** answers the moves side of **joint round 5** |
| (`CODEX-FINDINGS-JOINT-R5.md`, cited "R5-n") and is written against |
| @@ -618,10 +658,20 @@ 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 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). |
| + 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). |
| 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 |
| @@ -685,13 +735,28 @@ fails there first (§14.2.6). |
| `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 |
| + install, a dirty rollback's install on the source (§7.8). **The PUT |
| + must be acknowledged before replication opens, and the position is |
| + what the listing then shows** (R6-1): litestream derives its position |
| + from the remote level-0 files actually present, so an anchor still in |
| + flight is no anchor, and an activator that opened on the strength of |
| + having issued the PUT would replicate from TXID 1. The activator |
| + therefore waits for the PUT's response, retrying the same bytes after |
| + its client timeout (the original may still land, identical), and only |
| + then opens; it never sets the position itself. Rev 7.6's model did |
| + (`db.Pos = cur`, R6-1); rev 7.7's `restoreInit` returns nothing until |
| + the anchor is acknowledged and reads the position from the listing |
| + (rule `anchor-acked`; the witness holds the anchor PUT across forty |
| + attempted opens and requires the host not to open, §14.2.5). 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`). |
| + (fact R5-1f, asserted by identity), so a fresh box continues at exactly |
| + `N + 1` (facts R5-1g, h; `TestGate_AnchoredLineageThroughStore` for |
| + three disk losses in a row). 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`). Oracles never |
| + write one: a cold-restore check is the pure calculation of steps 4, 5 |
| + and 8 (R6-1). |
| 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 |
| @@ -791,7 +856,7 @@ 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.4 §6.2a, R4-3).** The live set is |
| +**The authoritative region (claim rev 6.5 §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; every current version under the |
| @@ -1037,10 +1102,10 @@ 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.4 §6.4, R3-3, R4-2, |
| + refused. **Installation stamps** (claim rev 6.5 §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 |
| + (claim rev 6.5 §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 |
| @@ -1050,7 +1115,7 @@ Phase 1 uses the claim spec's park (§6.2 there) and local retirement |
| 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 |
| + (claim rev 6.5 §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 |
| @@ -1060,7 +1125,7 @@ Phase 1 uses the claim spec's park (§6.2 there) and local retirement |
| 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 |
| + the box's local record when it selected its work** (claim rev 6.5'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 |
| @@ -1068,10 +1133,17 @@ Phase 1 uses the claim spec's park (§6.2 there) and local retirement |
| 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 |
| + call** (claim rev 6.5 §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 |
| + the retired set; rev 6.4's answer 2 withdraws that). It parks **by |
| + tag**: every local artifact carries the stamp of the installation that |
| + produced it (claim §6.3's inventory), `retire-artifacts(S)` parks the |
| + ones tagged `S` and leaves the rest, and a caller that expected another |
| + tag has made a mistake the model records (R6-4). Where the files |
| + directory is carried into the new generation (a push, F7; a landing's |
| + `restored` phase; the activator's park of a warm database before a cold |
| + restore) the retirement is of the database alone. 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 |
| @@ -1087,12 +1159,34 @@ 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). Op ids are opaque and never compared (claim rev 6.1 Q1). |
| + probe (R5-4). **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 |
| + produces; a CAS that makes an existing installation current again |
| + writes that installation's own stamp, taken from the op journal. The |
| + flip records the source's pre-move stamp `S` in the journal |
| + (`op.source_stamp`) as it writes the target's `F`; a rollback's return |
| + CAS (§7.8 `claimed`: `op.exec` back to the source) writes `holder.stamp |
| + = S`, never `F`. The source's initialization then finds `holder.stamp` |
| + equal to its `active_stamp` and changes nothing; a source whose local |
| + record was lost (a reboot) re-initializes to `S` from the same fresh |
| + read. A dirty rollback's install runs under `S`, its artifacts tagged |
| + `S`; the probe CAS issues `R` with `holder.generation`, and |
| + **activation of `R` tags the generation's artifacts `R`** and retires |
| + `S`. `F` was only ever active on the target and retires there |
| + (`retire-installation` at `cleaning`). Rev 7.6's model returned |
| + execution with `holder.stamp` still `F`, so the source activated the |
| + target's installation and tagged its artifacts `F` (R6-4); rev 7.7 |
| + encodes rev 6.5 and records any activation of a stamp the claim issued |
| + for another box as INV-6 (`return-stamp`, with a witness whose source |
| + has lost its record, §14.2.5). 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 |
| + exactly as claim rev 6.5 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 |
| @@ -1124,7 +1218,7 @@ 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.4 §6.2a, R4-3): `{authoritative region, |
| +region-qualified** (claim rev 6.5 §6.2a, R4-3): `{authoritative region, |
| holder.location, holder.generation}` plus the versions §5.1 names for the |
| generation, the snapshot version `generation.json` names included, is |
| protected in the authoritative region's bucket only (the table in §5.1); |
| @@ -1326,7 +1420,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 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) | |
| +| T11 budget | the **whole** stop-to-open estimate fits the operator's cut window (default 120 s) (codex R2-10, M11), from three measured rates, the **cross-region copy path**, **regional S3** (reads and writes from a box in the bucket's region) and the box's **disk**: stop + final checkpoint and `SyncAndWait` + final mirror (at most the 16 MiB bar at the cross-region rate) + archive build and upload + **the target's build (§7.6 `building`, R5-5, R6-3): the restore of the staged replica (the whole database read from regional S3 and written to disk), the snapshot write and the anchor write (each the whole database read from disk and written to regional S3)** + **the verification of the built database (§7.6 `restored`: one disk read for its sha256)** + 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 built the snapshot on the target and priced three passes at one local rate, then restored the generation cold a fourth time in `restored` without pricing it: the review's 3 GiB at 200 MiB/s with one probe came to 108.68 s priced and 124.04 s run (R6-3). Rev 7.7 verifies the built database instead of restoring it again and prices every byte moved. **The worked example**, the same in this spec, the change note and `budget_test.go`: 2 GiB at 10 MiB/s across regions, 250 MiB/s to regional S3, 500 MiB/s on disk gives 53.6 s of fixed costs (restore 12.3, snapshot 12.3, anchor 12.3, verify 4.1, the rest 12.6) and admits **one** attempt; the cross-region snapshot transfer (204.8 s) is refused by the same arithmetic, and so is the review's 3 GiB workload at 200 MiB/s (rev 7.6's arithmetic admitted it). **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 |
| @@ -1455,13 +1549,13 @@ journaled in `<DataDir>/.moves/<host>/<move id>/` (F12). |
| | phase | action | done when | replay | |
| |---|---|---|---| |
| -| `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 | |
| +| `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` 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) | |
| +| `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) | |
| | `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) | |
| +| `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) | |
| -| `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` | |
| +| `restored` | **verify the database `building` produced** (R6-3): its sha256 equals the manifest's, `CheckDB` (`backend_exec.go:313`) passes, and `<dbPath>.gen` is written naming this generation and location; record `landing.installed_db_sha256`. No second cold restore: the file was built by the planner over the sealed versions on this box and verified at `N`, and a cold restore from the generation would yield the same pages by construction (the snapshot is every page of that file). The anchor's PUT was acknowledged in `building`, so litestream's open reads position `N` from the listing and replication starts at `N + 1` (§5.1 step 7); a `building` replayed after a crash rebuilds and the sha256 is checked again | | replayable until `probing`; a sha256 or `CheckDB` mismatch is a rollback | |
| | `probing` | the probe (§7.7) | | **never replays an earlier phase** (INV-7); a crash restarts only the probe | |
| | `probed` | probe passed | | | |
| @@ -1542,12 +1636,12 @@ because, until then, a source failure might need the target's state again. |
| | phase | action | replay | |
| |---|---|---| |
| | `waiting` | until `released` (clean) or `returned` (dirty) and the claim's execution holder is `none` | | |
| -| `claimed` | CAS the claim: `op.kind = restoring`, execution holder = this box, citing the target's evidence (§19 K4) | | |
| +| `claimed` | CAS the claim: `op.kind = restoring`, execution holder = this box, citing the target's evidence (§19 K4), **and `holder.stamp = op.source_stamp`**, the source installation's own stamp the flip journaled (claim rev 6.5: a CAS that makes an existing installation current again writes that installation's stamp; R6-4). The source's fresh read then matches its record, or re-initializes a lost one, to `S` | | |
| | `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`, `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 | |
| +| 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 `S`, which the `claimed` CAS wrote back into `holder.stamp` and which stays active; `local` runs `retire-artifacts(S)` on the pre-move database, tagged `S`, which moves no stamp; the return generation's database and files are tagged `S` as they are installed; the `probed` CAS below, which names the return generation in `holder.generation`, writes the **new `holder.stamp` `R`** in the same write, and the source's fresh read under the guard activates `R` before the open, tagging the return generation's artifacts `R` and retiring `S` then (claim rev 6.5 §6.4: a dirty rollback installs a new generation and never keeps its predecessor's stamp, R5-4, R6-4; rev 7.5's model kept it, rev 7.6's activated the target's). 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` | 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) | | |
| +| `probed` | dirty: the claim CAS that names the return generation (`holder.generation = <rollback id>`, §5.1) and writes `holder.stamp`, the return installation's new stamp, in one write (claim rev 6.5 §2, §6.4) | | |
| | `recovered` | CAS `rollback.recovered_at` | | |
| | `opened` | the conditional open on `hold_op = rollback id`; CAS `rollback.opened_at` | | |
| @@ -2017,9 +2111,46 @@ 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 |
| +go test ./internal/sim/litestreamfacts/ # about 9 s |
| ``` |
| +**Rev 7.7: exact facts, and the anchored lineage through the Store |
| +(R6-2).** Rev 7.6's facts logged what they saw and some accepted either |
| +outcome: the level-0 expiry test passed when replication restarted and |
| +seven rows of nine survived, the retention test logged the newest |
| +restore's row count without asserting it, the anchor test required a |
| +position past `N` rather than exactly `N + 1`. Every fact is now an |
| +exact assertion that fails on any alternative behaviour: the newest |
| +level-0 file retained by identity through TXID- and time-based |
| +retention; the next upload exactly `[N + 1, N + 1]`; every row restored; |
| +the original continuation gone after the second rotation; the rooted |
| +restore refused with litestream's own message for the gap after TXID 1; |
| +the newest restore's exact row count. `TestFact_R6_5_AnchorReplayBytes` |
| +shows the anchor's bytes identical for the same inputs and different for |
| +another timestamp (R6-5). `TestGate_AnchoredLineageThroughStore` is the |
| +integration gate the review asked for: one anchored lineage through |
| +`internal/lease`'s Store shape (a DB with its own metadata directory, a |
| +replica client, `litestream.NewStore` with the compaction ladder, the |
| +snapshot and level-0 retention monitors), every interval shortened from |
| +hours to fractions of a second, three rounds of eight writes with |
| +level-1 to level-3 compaction, snapshot rotation and time-based level-0 |
| +expiry running, then disk loss and a cold restore; every sync advances |
| +the position by exactly one, a reopened box continues at exactly the |
| +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.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' |
| +version counter and every version, the pending requests, the boxes' |
| +upload queues and anchors, the console's plans and the random source's |
| +draw count are what they were before; a check that changed any of them |
| +is its own violation. The final oracle's start check initializes the |
| +stamp record on a copy of the box. Rev 7.6's cold-restore oracle wrote |
| +anchors into the system it was checking (R6-1); every number in §14.2.3 |
| +and §14.2.5 is from the pure model. |
| + |
| #### 14.2.2 What it models |
| **Rev 6 (joint round 2): the model encodes the specs, nothing stronger.** |
| @@ -2421,6 +2552,50 @@ readiness, and same-operation lease identities. |
| step the model distinguishes; the seal names one version, not one per |
| staged file. |
| +**Rev 7.7: joint round 6 and claim rev 6.5.** |
| + |
| +- **Restore split in two (R6-1).** `restoreCalc` is the restore contract |
| + as a pure calculation over one region's bucket: §5.1 steps 4, 5 and 8, |
| + returning the database and the position it restored to, or nothing |
| + when the contract refuses. `restoreInit` is the activator's: the |
| + calculation, then the restore-to-replication initialization. When the |
| + restored position is above the newest remote level-0 file it issues |
| + the anchor PUT and returns nothing until one of its PUTs is |
| + acknowledged (retrying the same bytes after `uploadTimeout`); the wake |
| + tries again later. Only then does it read the position, from the |
| + listing (`anchor-acked`). A box's outstanding anchor PUTs are forgotten |
| + with its agent (the restarted activator issues them again, identical). |
| + The mutation of `anchor-acked` opens at once with whatever the listing |
| + shows, which is litestream's behaviour with no anchor present; the |
| + witness holds the anchor PUT across forty attempted opens of a push's |
| + install and requires the host not to open. |
| +- **The oracles assert their purity (R6-1).** `fingerprint` and `pure`, |
| + around `checkDurable` and the final oracle (§14.2.1). |
| +- **Claim rev 6.5's return to source (R6-4).** `op.SrcStamp` is the |
| + source installation's stamp, journaled by the flip; the return CAS |
| + (`waiting → claimed`, `op.exec` back to the source) writes |
| + `holder.stamp = op.SrcStamp` (`return-stamp`). `issueStamp` records, |
| + for every stamp an installing CAS writes, the box whose installation it |
| + names; `activate` (initialization and reinstall) refuses, as INV-6, a |
| + stamp issued for another box, retires the old active stamp, sets the |
| + new one and tags the artifacts of the generation the claim names with |
| + it. `retireArtifacts(b, inc, S)` parks the database and files tagged |
| + `S` and nothing else; `retireDatabase` the database alone where the |
| + files are carried; callers assert the tags they expect (a landing never |
| + parks its own active stamp's artifact; a dirty install parks the |
| + pre-move database while its stamp is active). A reboot loses the local |
| + stamp record in one case in eight; the next fresh read re-initializes |
| + it. Witness: a dirty return whose source lost its record (the source |
| + must serve under the probe CAS's stamp, its database so tagged, the |
| + pre-move stamp retired). |
| +- **Compaction keeps the newest level-0 file**, as litestream's retention |
| + does (facts R5-1f to h), so the model no longer creates anchor-required |
| + cold restores that the library would not. |
| +- **The budget (R6-3, `budget_test.go`)** prices regional S3 and the disk |
| + as separate rates and the `restored` phase as a verification read; the |
| + 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. |
| + |
| #### 14.2.3 Invariants and results |
| The invariants are the table at the end of §4, with three checks rev 6 |
| @@ -2443,7 +2618,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.6, on the final model (claim rev 6.4: `holder.stamp`, |
| +**Rev 7.7, on the final model (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 |
| +the 100,000 seeds: 155,280 completed operations, among them 1,739 |
| +completed moves, 1,871 clean and 89 dirty rollbacks, 426 |
| +pre-flip reverts, 332 declared losses, 29,995 pushes, 89,101 |
| +delete-park-free cycles and 1,563 lost disks; 18,465 LTX |
| +compactions, 12,889 snapshot rotations, 751 level-0 upload retries, |
| +32,387 anchors written at cold restores and 12,307 wakes that waited |
| +for an anchor's acknowledgement; 26,127 local stamp records lost with a |
| +reboot and re-initialized; 38,225 requests completed after `H`; |
| +33,527 staging signatures were refused as stale; 30,646 creates |
| +restarted on a 412; 99 targets were stopped mid-return. Every oracle |
| +left the system unchanged (the purity assertion, §14.2.1). One oracle |
| +fault found and fixed before these baselines (§14.2.2): a write declared |
| +lost with a disk whose upload landed anyway and was applied by a later |
| +restore; the comparison now masks such keys (seed 68282 / 100,000 under |
| +rev 7.7's first binary). |
| + |
| +**Rev 7.6, on 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 |
| @@ -2596,27 +2791,27 @@ 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.6 model (50b1e51d), with the strict classification, |
| +on the final rev 7.7 model (45f93495), 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 |
| +same mutation, for the 33 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 |
| +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 |
| 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). |
| +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. |
| | | rules | |
| |---|---| |
| -| 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 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 | |
| @@ -2624,25 +2819,22 @@ verdict is unchanged, and `fence-stamp` is caught alone by the sweep now |
| | unreachable under claim rev 5 | 1 (`readiness-quiet`) | |
| | unexercised | **0** | |
| -**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). |
| +**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). |
| **The witnesses.** One scenario per rule the sweep catches rarely or only |
| in combination, and one per rule a review round added; two for |
| @@ -2653,43 +2845,45 @@ 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 | | 13 / 3,000, 114 / 30,000, 383 / 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 | | 5 / 3,000, 35 / 30,000, 113 / 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 / 30,000, 3 / 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 / 100,000; the pair 1 / 30,000, 4 / 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 | | 3 / 3,000, 7 / 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 | | 1 / 3,000, 6 / 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, 8 / 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, 19 / 30,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, 6 / 30,000 | |
| -| `dirty-return` (INV-2) | the target writes during its probe and is rolled back | **violated**: INV-2, the write is lost | | 8 / 3,000, 58 / 30,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, 109 / 30,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; the pair 1,365 / 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; any pair 0 / 30,000; the triple 11 / 30,000, 21 / 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 | the triple 11 / 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 828 / 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,407 / 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 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.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 | |
| +| `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 | |
| | `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 | |
| -| `recovery-current-inputs` (§7.7, §7.8; R2-5) | a bundle is published after admission; the target writes; the rollback is dirty | **violated**: `stuck` | | 48 / 3,000 | |
| +| `sweep-namespace` (claim rev 6 §6.2a, R3-4) | a replication PUT of incarnation 1 completes after 33 recreates dropped it from `retired_incarnations` | **violated**: INV-10, residue the sweep never finds | | 532 / 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-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 | |
| **The purge fence, the ETag condition and C5a.** `purge-claim-fence` |
| -(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): 6 / 3,000, 48 / 30,000. `registration-check` is not caught alone |
| +(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` |
| +(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`, 333 / |
| -30,000); its two pairs 271 and 272 / 30,000. |
| +alone is shown insufficient (`purge-claim-fence` + `fence-etag`, 348 / 30,000); |
| +its two pairs 245 and 270 / 30,000. |
| **Rev 6's unexercised three, now caught (the biased schedule, §14.2.2).** |
| @@ -2705,47 +2899,48 @@ 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: 63 of 77** (56 by the sweep at 3,000; 4 by the sweep at |
| +**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 ‡). |
| | rule | seeds failing | | rule | seeds failing | |
| |---|---|---|---|---| |
| -| `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` | 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-gap-closed` ‡ | witness; sweep 0 / 30,000 | | `hostguard` | 8 / 3,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 | |
| -| `source-readiness` | 11 / 3,000 | | `seal-by-version` | witness; sweep 0 / 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-by-installation` | 221 / 3,000, 1,988 / 30,000 | | `live-set-region` ‡ | witness; sweep 0 / 30,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 |
| +| `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 |
| 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 |
| @@ -2753,23 +2948,21 @@ 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) | 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 | |
| -| `registration-check` + `purge-claim-fence` | 272 / 30,000 | `purge-claim-fence` 241 | violated | the same | |
| -| `registration-check` + `fence-etag` | 271 / 30,000 | `fence-etag` 223 | violated | the same | |
| -| `exec-admission` + `hold-op-open` + `start-check-claim-gen` | 18 / 100,000 (6 / 30,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` | 11 / 30,000 (rev 7.5) | (above) | violated | the same, dropping the whole start check | |
| -| `door-reread` + `location-per-incarnation` | 432 / 30,000 (rev 7.5) | `location-per-incarnation` 385 | violated | door reads of another incarnation's data (196) | |
| -| `door-by-version` + `location-per-incarnation` | 385 / 30,000 (rev 7.5) | `location-per-incarnation` 385 | 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,365 / 30,000 (rev 7.5) | `revalidate-before-effect` 610 | violated | a stale step destroys a store | |
| -| `strict-spawn` + `evidence-whole-tree` | 828 / 30,000 (rev 7.5) | `evidence-whole-tree` 504 | violated | two writers | |
| -| `touched-incomplete` + `legacy-discovery` | 7,407 / 30,000 (rev 7.5) | `legacy-discovery` 3,814 | violated | a freed host's residue | |
| -| `declare-lost-compute` + `watchdog-independent` | 3 / 30,000, 8 / 100,000 | `declare-lost-compute` 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) | 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). |
| +| `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. |
| **Liveness only: 2.** `readiness-key` (T2) and `config-before-probe`. |
| They have no witness: neither can violate an invariant. |
| @@ -2779,8 +2972,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; 32 witnesses, 106 runs); the 30,000- and 100,000-seed |
| -baselines, this sweep and the witnesses are the evidence for rev 7.6. |
| +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. |
| #### 14.2.6 What the model does not prove |
| @@ -2826,7 +3019,20 @@ baselines, this sweep and the witnesses are the evidence for rev 7.6. |
| 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`. |
| + 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 |
| + 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 |
| + repository has no S3 fake litestream's client can talk to (the lease |
| + tests' `fakeMirror` is a `MirrorStore` seam), so no S3-fake test was |
| + added; the production experiment of §15 step 7's rehearsals is where |
| + the two meet. |
| - **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 |
| @@ -3137,6 +3343,21 @@ 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.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 |
| +`op.exec` writes `holder.stamp` in the same write, the new gen when it |
| +makes a new installation current, the installation's existing stamp |
| +from the op journal when it makes an existing one current again. A |
| +dirty rollback's return to source is the second case: it writes the |
| +source's pre-move stamp `S`, not the target's `F`; the source's |
| +initialization then changes nothing, the installed database keeps `S`, |
| +the probe CAS issues `R`, and activating `R` retires `S`; `F` was only |
| +ever active on the target and retires there. Rev 7.7 encodes it (§6.4, |
| +§7.8, §14.2.2): the flip journals `S`, the return CAS writes it back, a |
| +lost local record re-initializes from it, and the oracle refuses an |
| +activation of another box's stamp. No claim question this round. |
| + |
| **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 |
| only after its own `evidence time + H`, so the `quiet_after` it writes has |
| @@ -3434,3 +3655,19 @@ d96f781c) and answers the moves side from what it observed. |
| | 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 | |
| +### 22.13 Joint round 6 (claim 697f0f9f, moves rev 7.6 f7f7c438, model f7f7c438) |
| + |
| +The claim was judged ready for implementation planning; the moves spec |
| +and the model were not yet ready as the joint baseline, on three P2 and |
| +two P3 findings, no P1. Claim rev 6.5 (d36adcfa) answered R6-4. Rev 7.7 |
| +answers the rest and reruns every number. |
| + |
| +| finding | rev 7.7 | |
| +|---|---| |
| +| R6-1 (P2) the restore oracle changes the system it checks (it writes anchors), and anchor initialization bypasses durability (`db.Pos = cur` before the PUT succeeds; a held PUT still replicates at `N + 1`) | the restore is split: `restoreCalc`, pure, is every oracle's; `restoreInit`, the activator's, opens replication only once an anchor PUT is acknowledged and reads the position from the listing (§5.1 step 7; rule `anchor-acked`). Every oracle asserts its purity across buckets, versions, pending requests, queues, anchors, console and random draws; the final oracle's start check initializes the record on a copy. Witness: a push's anchor PUT held across forty attempted opens; opened at once the model shows the position litestream would read, 0, and names the failure. Baselines and mutations rerun on the pure model (§14.2.3, §14.2.5) | |
| +| R6-2 (P2) the facts gate accepted the loss behaviour (7 of 9 rows with a restart), logged rather than asserted counts, required "past `N`" rather than `N + 1`; no anchored lineage through the production Store | every fact exact and failing on any alternative (§14.2.1); `TestGate_AnchoredLineageThroughStore`: the anchored lineage through `internal/lease`'s Store shape with compaction, rotation, time-based level-0 expiry, three disk losses and cold restores, exact positions and contents; the file client's limits stated (§14.2.6), no S3 fake in the repository | |
| +| R6-3 (P2) T11 omits the `restored` phase's second cold restore (3 GiB at 200 MiB/s: 108.68 s priced, 124.04 s run); the example's 50 MiB/s is 200 in the test | `restored` verifies the database `building` produced (sha256 against the manifest, `CheckDB`) and restores nothing again, which is sound because the planner built the file on this box from the sealed versions and verified it at `N` (§7.6); T11 prices regional S3 and the disk separately and the verification read (§7.3); one worked example in the spec, the note and `budget_test.go` (2 GiB at 10 / 250 / 500 MiB/s, 53.6 s fixed, one attempt), and the review's workload reproduced and refused | |
| +| R6-4 (P3) rollback stamps: the source activated the target's `F`, artifacts kept `F` after `R`, `retireArtifacts` ignored its arguments | claim rev 6.5's invariant encoded: the flip journals `S`, the return CAS writes `holder.stamp = S`, a lost record re-initializes from it, activation of `R` tags the generation's artifacts and retires `S`, `F` retires on the target (§6.4, §7.8). `retire-artifacts` parks by tag and callers assert tags; the oracle refuses an activation of another box's stamp (INV-6). Rule `return-stamp`; witness: a dirty return with a lost local record (§14.2.5) | |
| +| 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) | |
| + |