amadan
spec: move-any-app rev 7.9: joint round 8, writer sessions (claim rev 6.8, 6.8.1), every number rerun (#175)
R8-1: per-session certificates never deleted, one-use through the admitting CAS; R8-2: AdmitWriter on every path, inside the operation, only op.exec, with the phase table of which box is admitted when; R8-3: the empty generation; R8-4: provenance for the warm baseline; R8-5: close evidence over the writer's lifetime; R8-6: the retired-door rows separate historical from current results. 90 rules, 49 witnesses; 30,000 and 100,000 seeds clean; mutate.sh at 3,000, 30,000 and 100,000; the model faults the sweep found before the final numbers; §19.4 notes for claim rev 6.8; §22.15 dispositions.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
1 file changed,
+582
−163
docs/superpowers/specs/2026-10-02-move-any-app-design.md+582 −163
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 cfbb202fa..26d8ddcc8 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,54 @@ |
| # Move any app or instance to another region: Phase 1, a safe single-instance move |
| -**Date:** 2026-10-03 |
| -**Revision:** 7.8. |
| +**Date:** 2026-10-04 |
| +**Revision:** 7.9. |
| + |
| +- **Rev 7.9** answers **joint round 8** (`CODEX-FINDINGS-JOINT-R8.md`, |
| + cited "R8-n") and is written against **claim spec rev 6.8** (5462d293), |
| + whose rewritten §6.4a, writer sessions and epochs, answers R8-1 to |
| + R8-4, and **rev 6.8.1** (a963d98d): only `op.exec` may open |
| + replication, in every op kind; §22.15 has every disposition. **R8-1 |
| + (P1):** rev 7.8's `closed.json` was consumed by deleting the version |
| + the writer read, which is not one-use under S3's semantics (an exact |
| + version delete removes it and exposes an older version; a delayed or |
| + replayed PUT recreates it); the certificate is now **per writer |
| + session**, `closed/<session>.json`, never deleted, and what makes it |
| + one-use is the **admitting CAS** that moves `holder.session` forward: |
| + a certificate names a dead session from then on, whatever its stamp |
| + and `max_txid` say. **R8-2 (P1):** rev 7.8 checked replication state |
| + only at an ordinary wake; **every** path that opens replication is an |
| + `AdmitWriter` now (a committed landing's serving, a restarted probe, a |
| + reverted source, an opened rollback recovery, a push's writer), and a |
| + cold admission runs **inside** the operation it interrupts, keeping its |
| + kind, id, journal, participants and obligations (§7.14's phase table |
| + says which box may be admitted in which phase; `op.exec` is handed |
| + over before any probe or landing write). **R8-3 (P2):** a created |
| + incarnation's first wake is a cold admission into an **empty** |
| + generation: no snapshot `[1, 0]`, no anchor `[0, 0]` (the pinned |
| + encoder refuses a zero TXID, `TestFact_R8_3_EmptyBootstrap`); the app |
| + starts first and may create its database, and the first transaction's |
| + file is the first upload. **R8-4 (P2):** the warm database is the cold |
| + baseline only with **provenance**: a lineage file naming the |
| + journalled predecessor's `{generation, session}`, the predecessor's box |
| + being this box, and an integrity check; re-initializing a stamp record |
| + never writes lineage. **R8-5 (P2):** the clean close's evidence is |
| + every request of the writer's lifetime, level-0, compaction, snapshot |
| + and retention, with a sticky uncertainty flag for a timed-out original |
| + whose retry succeeded. **R8-6 (P3):** §14.2.5's retired-door rows |
| + separate the historical results from the current ones. Rules |
| + `writer-session`, `admit-everywhere`, `exec-writer`, |
| + `warm-provenance`, `valid-ltx`, `close-evidence`; witnesses for a dead |
| + session's certificate replayed, the collision during a committed |
| + landing's serving and during a probe restart, a non-exec writer, a |
| + warm database with a foreign lineage, an empty first wake, and a retry |
| + that succeeds while its original stays unresolved. 90 rules, 49 |
| + witnesses. The model faults this round found before the final numbers |
| + (a stalled worker replaying a finished build, the carried files |
| + untagged, a source that lost its disk during a rollback, the biased |
| + schedule's unbounded hold in the calm phase, a lost target's unfinished |
| + admission blocking the rollback, every close outside `serving` |
| + dropped) are in §14.2.2. Results in |
| + §14.2.3 and §14.2.5. |
| - **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), |
| @@ -716,7 +763,7 @@ fails there first (§14.2.6). |
| 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 |
| + cold admission 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). |
| @@ -832,55 +879,124 @@ fails there first (§14.2.6). |
| 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. |
| +9. **Writer sessions and epochs: two writers whose uploads could overlap |
| + never share a generation, and every path that opens replication is |
| + admitted (claim rev 6.8 §6.4a and rev 6.8.1; R7-1, R8-1 to R8-5).** |
| + 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. Claim rev 6.8 states |
| + the rule and this spec owns the data path: |
| + - **`AdmitWriter`, one claim CAS before any upload.** `holder.session` |
| + is the claim `gen` of the CAS that admitted the current writer |
| + session. Every path that opens replication makes this CAS first: an |
| + ordinary wake, a committed move's target serving while the claim is |
| + still `landing`, a restarted probe, a reverted source, an opened |
| + rollback recovery, a push's writer (R8-2). It requires the observed |
| + `holder.session` and `holder.generation` and **`op.exec` to be this |
| + box**, in every op kind (claim rev 6.8.1): at most one box writes a |
| + host's replica at any time, and `op.exec` names it; §7.14's phase |
| + table says when `op.exec` is handed to which box, always before that |
| + box's first probe or landing write. The CAS writes |
| + `holder.session = its resulting gen` and a journal entry in |
| + `op.journal.writers`, `{session, box, generation, stamp, mode, |
| + predecessor: {session, box, generation, stamp}}`, the predecessor |
| + copied from the claim it observed. It **never replaces the |
| + operation**: a cold admission inside `landing`, `restoring`, |
| + `reverting`, `pushing` or a probe keeps the operation's kind, id, |
| + phase, participants, obligations and the rest of its journal |
| + (§7.14). The model makes this CAS as the process starts, after the |
| + start checks and the health check, so a start that fails admits |
| + nothing (a storm of cold admissions from failing starts was the |
| + first rev 7.9 model's fault). |
| + - **A clean close is a one-use certificate.** A writer session |
| + stopping cleanly first waits until **every request it issued over |
| + its lifetime** has completed with success (R8-5): every level-0 |
| + upload, every compaction and snapshot upload, every retention |
| + delete, and every timed-out original whose outcome is unknown. A |
| + request the client timed out and retried makes the session |
| + **uncertain for good**, whatever its retry returned, because the |
| + original may still land; a crash while draining leaves nothing. A |
| + session that can prove completion writes |
| + `<location>/<generation>/closed/<session>.json` as `{session, box, |
| + max_txid, closed_at}` once (`If-None-Match`), then releases its |
| + lease. **No certificate is ever deleted or reused**, and no S3 |
| + delete or version semantics are involved: rev 7.8's "consume the |
| + marker by deleting the version read" is withdrawn (R8-1: deleting an |
| + exact version makes no delete marker and can expose an older |
| + version; a delayed or replayed PUT of the same stamp and TXID |
| + recreates it). Litestream's `Replicator.Close` drops the initial |
| + `SyncAndWait` error (`internal/lease/lease.go`), so certificate |
| + eligibility needs its own evidence, never `Close`'s return value. |
| + - **Warm continuation** is an `AdmitWriter` in **warm** mode: legal |
| + only if `closed/<holder.session>.json` exists for the observed |
| + session, its `max_txid` equals the generation's remote maximum TXID |
| + over every level, and its `box` is the admitting box. The admitting |
| + CAS moves `holder.session` forward, so that certificate now names a |
| + dead session: a delayed, replayed or re-created certificate of any |
| + earlier session can never authorize anything again, however its |
| + stamp and `max_txid` read. The writer opens under the new session, |
| + writes its **lineage file** `{generation, session}` beside the |
| + database, and reads its remote position at its first sync |
| + (litestream initializes it lazily, R8-5). |
| + - **Everything else is cold**: no certificate for the observed |
| + session, a mismatched `max_txid`, another box's certificate, any |
| + doubt. That covers a crash, an out-of-memory kill, lease expiry or |
| + takeover, a shared-pool failover, a lost box, and a writer that |
| + continued and then crashed with uploads in flight (its own session |
| + has no certificate, whatever older ones exist). A **cold admission |
| + is an installing CAS** (§7.14): in the same write, a new |
| + `holder.generation` (a fresh op id never reused) and `holder.stamp = |
| + the resulting gen`, with the predecessor journalled **before** the |
| + new stamp is activated anywhere (R8-4). The box then builds the new |
| + generation under stop evidence and publishes it before the writer |
| + opens. |
| + - **The baseline needs provenance (R8-4).** The warm local database is |
| + the cold build's baseline only if all three hold: its lineage file, |
| + written by the writer that opened it, names the journalled |
| + `predecessor.{generation, session}`; `predecessor.box` is this box; |
| + and it passes its integrity check with its WAL in place (committed |
| + frames count). Re-initializing a local stamp record from the current |
| + claim (§6.4) never writes a lineage file, so no claim read can |
| + manufacture evidence of earlier ownership. Otherwise the baseline is |
| + the predecessor generation restored from its remote by the restore |
| + contract, version-pinned, and acknowledged writes that never |
| + replicated are declared lost. A cached or restored copy of `G` |
| + through `N` therefore never replaces `G`'s history through `N + 1`. |
| + - **An empty generation (R8-3).** The first writer after a create, or |
| + after an adoption with nothing replicated, is admitted cold with a |
| + fresh generation that may be **empty**: until the first committed |
| + transaction no LTX file exists, and no file with a zero TXID is |
| + ever written (the pinned encoder refuses `[1, 0]` and `[0, 0]`, |
| + `TestFact_R8_3_EmptyBootstrap`: "maximum transaction id required", |
| + "minimum transaction id required"). The build at position 0 writes |
| + no snapshot and no anchor; `generation.json` names the generation |
| + with `snapshot_txid = 0` and no snapshot identity, and a restore of |
| + an empty generation yields an empty database. The app starts first |
| + and may create its database, as the activator does today |
| + (`activator.go`, first-boot seeding); litestream opened on an absent |
| + database against an empty replica syncs nothing, and the first |
| + transaction's file is the first upload, `[1, 1]` (facts R8-3b to e). |
| + The writer is admitted before that upload. |
| - **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 |
| + constructed for the `{holder.location, holder.generation, session}` |
| + the writer was admitted with 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). |
| + retention. It never re-reads the generation, so a new admission is a |
| + new writer. A dead writer's late uploads land in the old generation, |
| + or in the current one **before** the session that superseded it |
| + opened; a cold successor has a new generation, and a warm successor |
| + exists only after the old session certified that every one of its |
| + requests had completed. Dead generations are parked by the |
| + admission's chore and the at-rest sweep (§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; |
| @@ -890,13 +1006,17 @@ fails there first (§14.2.6). |
| 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. |
| + generation with the rule and loses B's write without it; a dead |
| + session's certificate with a matching stamp and `max_txid` authorizes |
| + nothing; the collision during a committed landing's serving and during |
| + a probe restart is caught by the admission inside the operation; a |
| + non-exec writer is refused; a warm database with a foreign lineage is |
| + restored over; an empty first wake writes no file; a retry that |
| + succeeds while its original stays unresolved writes no certificate. |
| + The cost is one snapshot and one anchor per cold admission (none for |
| + an empty generation), 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 certified close does not. |
| So: |
| @@ -1279,14 +1399,21 @@ 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). **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).** |
| + probe (R5-4). **A cold admission is an installing CAS too** (claim rev |
| + 6.8 §6.4a; §5.1 step 9, §7.14): it writes a new `holder.generation` |
| + and a new `holder.stamp` in one write, with the predecessor's |
| + `{session, box, generation, stamp}` journalled in the same write, |
| + before the new stamp is activated anywhere (R8-4); the box's record |
| + activates the new stamp from its next fresh read, and the built |
| + database **and the carried files** are tagged with it (the first rev |
| + 7.9 model left the files under the dead writer's stamp, and the next |
| + dirty install parked an artifact of a retired stamp, seed 453 / |
| + 30,000); the dead writer's stamp retires with it. Re-initializing the |
| + record from the claim writes no lineage file: the lineage file is the |
| + writer's, written as it opens, and it is what a later cold admission |
| + reads for provenance (§5.1 step 9). The admission's writer opens the |
| + new generation without a certificate of its own; its clean close |
| + writes the first one. **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 |
| @@ -1949,33 +2076,85 @@ process state (§5.3). |
| | flipped, record CAS done, claim CAS not | completes the claim CAS | waits for the claim | | |
| | reverting | resumes the recovery, held | n/a | | |
| | landing: checking to restored | holds `moving` | replays the phase per §7.6 | | |
| -| landing: probing | | kills the tree, restarts the probe | | |
| +| landing: probing, probed (the settle window) | | kills the tree, restarts the probe, which is an `AdmitWriter` within the landing (§7.14); a probe whose disk went with the crash is admitted cold into a fresh install generation | | |
| +| committed, the claim still `landing` | resumes the park | the target's next wake is an `AdmitWriter` within the landing (§7.14) | | |
| | committed | resumes the park | opens | | |
| | rolling_back: target phases | | resumes its phase; evidence from actual state | the deadline sweep is a CAS | |
| -| rolling_back: source phases | resumes its phase from its journal; never reinstalls after `probing` | | | |
| +| rolling_back: source phases | resumes its phase from its journal; never reinstalls after `probing`; a source whose database went with the crash verifies nothing and is admitted at its probe, warm or cold (§7.14) | | | |
| | stuck | held; operator | | | |
| -### 7.14 Cold recovery (claim rev 6.6 §6.4a, R7-1) |
| +### 7.14 Writer admission and cold admission (claim rev 6.8 §6.4a, 6.8.1; R7-1, R8-1, R8-2) |
| -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. |
| +Every path that opens replication is an `AdmitWriter` (§5.1 step 9), one |
| +claim CAS made as the process starts, by the box the claim names as |
| +`op.exec`, and never by another. **Which box may be admitted in which |
| +phase**, and the CAS that handed it `op.exec` first: |
| + |
| +| op kind, phase | the box admitted | `op.exec` handed to it by | |
| +|---|---|---| |
| +| `serving` | the serving box, at every wake | the create's claim CAS, a push's release, a move's finalization or rollback release (§7.9, §7.8) | |
| +| `pushing: probing` | the pushing box, as its probe starts | the push's claim CAS (`op.exec` = the serving box) | |
| +| `moving` (before the flip) | the source, at every wake; the target writes nothing | the move's claim CAS (`op.exec` = source) | |
| +| `reverting: probing, probed` | the source, as its probe starts and at every wake after | the revert CAS, which cites the stop evidence of the cut (§7.5) | |
| +| `landing: probing, probed` | the target, as its probe starts and at every restart of it | the flip CAS, which cites the source's stop evidence (§7.5) | |
| +| `landing`, committed, not yet finalized | the target, at every wake | the same flip CAS | |
| +| `restoring: probing, probed, opened` (the source's rollback) | the source, as its probe starts and at every wake after | the return CAS (`op.exec = op.src`, claim rev 6.5), after the target's release wrote `op.exec = -1` with stop evidence | |
| +| `restoring`, the target's phases | nobody: the target is stopping and never opens replication again | | |
| +| `creating`, `purging`, `deleting` | nobody | | |
| + |
| +Two writers never overlap because `op.exec` moves only through a CAS that |
| +cites stop evidence or a lost-box fence (§5.3, §7.10), and the admission |
| +CAS requires `op.exec == this box` (rule `exec-writer`). The admission is |
| +made **after** the start checks and the health check and **before** the |
| +process starts, so a start that fails admits nothing and a process that |
| +runs was admitted. |
| + |
| +**Warm** (the certificate of the observed session is intact, §5.1 step |
| +9) and **open** (the box's own cold admission has published its |
| +generation and the writer opens it) change the session alone. **Cold** |
| +is an installing CAS and a build, run **inside the operation** the wake |
| +found, by the box it admitted, before that operation's own step; the |
| +operation's kind, id, phase, participants, obligations and journal are |
| +kept, and the console refuses a move, push or delete while a cold |
| +admission is in progress. Its phases, in `op.journal.recovery`, each |
| +written before its side effects and each 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. |
| +| the CAS | conditional on the observed `holder.session`, `holder.generation` and `op.exec == this box`: `holder.session` = this CAS's `gen`; a writers journal entry `{session, box, generation: <rec id>, stamp, mode: cold, predecessor: {session, box, generation, stamp}}` from the claim observed; `op.journal.recovery = {generation: <rec id>, base: the observed generation, phase: build}`; **in the same write** the new generation and `holder.stamp` = this CAS's `gen` (the installing CAS, §6.4): when the observed generation is `holder.generation` it is `holder.generation` that moves, when it is an install generation under construction (a landing's or a push's `g-<op id>/`, a dirty rollback's return generation) it is the operation's install generation that moves and the claim's follows at the operation's own publish | | |
| +| `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 (seed 86799 / 100,000, rev 7.8). The **baseline** is the warm local database only with provenance (§5.1 step 9: lineage equal to the journalled predecessor's `{generation, session}`, predecessor box this box, integrity check); else the predecessor generation restored by the restore contract (§5.1 steps 4 and 5), version-pinned, in this box's region, with the warm database's acknowledged, unreplicated writes declared lost. Into the new generation's prefix, **when the baseline's position `N` is above 0**: the snapshot `[1, N]` (every page), acknowledged; the anchor `[N, N]`, acknowledged (§5.1 step 7). At position 0 nothing is written (R8-3; the encoder refuses a zero TXID) and the generation is empty until the writer's first upload. No certificate is written by the build: the admitted writer's own clean close writes the first one. The local database is the new generation's from here: `<dbPath>.gen` and `.files-gen` name it, the files are unchanged (F7) and retagged with the new stamp, the database's stamp is the new one, its request ledger starts empty, and its replication position is what the new generation's listing shows | a replay that finds a snapshot current in the new generation **reuses it as the baseline** and reuses a current anchor; a stalled worker whose claim read predates the admission's completion revalidates and does nothing, because the writer state (`holder.session`, `holder.generation`, `holder.stamp`, the recovery journal, the writers journal) is part of the step it compares (rev 7.9: a replayed build killed the running writer and replaced its database with the snapshot, seed 10382 / 30,000) | |
| +| `publish` | `generation.json` names the new generation (§5.1 step 3, conditional on the marker it supersedes; `snapshot_txid = 0` and no snapshot identity for an empty generation); then, in one CAS, `op.journal.recovery` cleared 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 | |
| +| the open | the next start of the admitted box opens the writer in the new generation under the session the CAS produced (mode `open`: the writers entry is marked opened in one CAS), writes its lineage file, and reads its remote position at its first sync | | |
| + |
| +A cold admission in progress belongs to `op.exec`. A CAS that moves |
| +`op.exec` away from the admitting box before its build has published (a |
| +rollback's release of the target, a declared loss) orphans it: the box |
| +that holds `op.exec` next, or any participant while nobody does, clears |
| +the recovery journal in one CAS and parks the half-built generation as a |
| +chore before its own admission (rev 7.9: a rollback's source probe could |
| +not be admitted behind the lost target's unfinished build, seed 58795 / |
| +100,000). A writer running inside an operation certifies its clean close |
| +like any other; the close is dropped only when an operation is taking |
| +the writer over, a push, a move's cut, a delete or a purge, whose |
| +generation is being replaced or parked (the first rev 7.9 model dropped |
| +every close outside `serving`, so a rollback's reopened source was |
| +admitted cold at every wake and the rollback never released, seed 84087 |
| +/ 100,000; its second let a push's writer certify into the generation |
| +the push superseded, which outlived the park, seed 4493 / 30,000). |
| + |
| +A cold admission costs the three local passes of an install (§7.3), none |
| +for an empty generation, and a dead generation to park. It runs after |
| +every crash, OOM kill, lease takeover or lost disk, after a close that |
| +could not certify (an upload retried, R8-5), and at the first wake of a |
| +created incarnation or an adopted legacy host, whose origin generation |
| +has no writer yet. It does not run after a certified close. |
| + |
| +**The source that lost its disk** during a revert or a rollback has |
| +nothing to verify against the digest it recorded at the stop: its |
| +recovery skips the digest check and its probe is admitted like any other |
| +writer, warm if its generation is intact (the certified close before the |
| +cut), cold otherwise (rev 7.9: the crash-with-disk fault reaches every |
| +operation now, R8-2). |
| ## 8. The archive (codex 19) |
| @@ -2289,6 +2468,18 @@ 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.9: the empty bootstrap, observed (R8-3).** |
| +`TestFact_R8_3_EmptyBootstrap` starts with neither a database file nor a |
| +replica: the pinned encoder refuses a header `[1, 0]` ("maximum |
| +transaction id required") and `[0, 0]` ("minimum transaction id |
| +required"); a restore from an empty replica fails ("cannot calc restore |
| +plan: transaction not available"); litestream opened on an absent |
| +database against an empty replica syncs without error and uploads |
| +nothing; after the first transactions and one sync the replica holds |
| +level 0 `[1, 1]` alone (a TXID is one sync's WAL frames, not one SQLite |
| +transaction), and a cold restore then holds the row. The spec's empty |
| +generation (§5.1 step 9) rests on these five facts. |
| + |
| **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 |
| @@ -2761,6 +2952,124 @@ 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.9: joint round 8, claim rev 6.8 and 6.8.1.** |
| + |
| +- **Writer sessions (R8-1, claim rev 6.8 §6.4a).** `holder.session` is |
| + the gen of the admitting CAS; `admitWriter` decides the mode (`open`: |
| + the box's own cold admission has published; `warm`: the certificate of |
| + the observed session is intact, `warmCertificate`; `fresh`: an |
| + install's first probe into the generation it built; else `cold`) and |
| + `admitCommit` makes the CAS as the process starts, after the start and |
| + health checks, bumping `holder.session` and appending the writers |
| + journal entry with its predecessor. The writer records `db.Session`, |
| + writes `box.lineage[inc] = {generation, session}` and reads its remote |
| + position lazily at its first sync (`RemotePos = -1`). The certificate |
| + is `closed/<session>.json` `{session, box, max_txid}`, written once |
| + with `If-None-Match` and never deleted; the live set keeps every |
| + session's certificate of the live generation. Rule `writer-session` |
| + (the mutation takes the newest certificate of any session, as rev 7.8 |
| + took `closed.json`). Witness `wDeadSessionCertificate`: two sessions |
| + certify, the third dies with its disk and an upload in flight; the |
| + dead certificates stand with a `max_txid` that still matches the |
| + remote maximum; the next wake is cold under the rule and continues the |
| + generation under the mutation, where the late upload replaces its file |
| + (INV-2). |
| +- **Admission on every path (R8-2, claim rev 6.8 §6.4a and 6.8.1).** |
| + `spawn` admits every non-legacy start: ordinary wakes, a committed |
| + landing's wakes while the claim is still `landing`, a probe, a probe |
| + restarted in its settle window (the landing's `probed` phase respawns a |
| + probe that died, as §7.13 says), a reverted source, a rollback's |
| + source probe and its wakes after `opened`, a push's probe. A cold |
| + admission runs **inside** the operation: `op.Rec` (`recState`: |
| + generation, base, session, box, phase, predecessor, the build's |
| + artifacts) is cleared at publish; `recStep` runs before the |
| + operation's own step on the admitted box; the console refuses a move, |
| + push or delete while it is in progress; the generation that moves is |
| + `holder.generation` for a wake and the operation's install generation |
| + (`op.InstGen`, read through `opGen`) for a probe into a generation |
| + under construction. The admission CAS requires `op.exec == this box` |
| + (rule `exec-writer`); `admit-everywhere` is the rule that every path is |
| + admitted (the mutation gates ordinary wakes alone, rev 7.8's rule). |
| + The crash-with-disk fault fires in every operation whose `op.exec` is |
| + the box. Witnesses: `wCommittedLandingCrash` (the committed target |
| + dies with its disk and an upload in flight before finalization; its |
| + next wake is cold within the landing, or under the mutation continues |
| + the generation and the late upload replaces its file), `wProbeRestart` |
| + (the landing's probe dies with its disk and an upload in flight; the |
| + restarted probe is cold into a fresh install generation, or under the |
| + mutation reuses it and the landing's restore loses the restarted |
| + probe's write), and the admission scenario (`wAdmissionTriple`) with |
| + `exec-writer` as a fourth fence: with all four gone the non-exec |
| + source's wake is a cold admission whose installing CAS moves |
| + `holder.stamp` under the target (INV-6), on its way to two writers |
| + (INV-1); the three box-side fences alone no longer hold the scenario, |
| + since under writer sessions the source's wake has no certificate for |
| + the current session and would be admitted cold rather than refused by |
| + its generation check, and `exec-writer` alone holds it, so the four |
| + are one combination. |
| +- **The empty generation (R8-3).** `snapshotOf` encodes a database with |
| + transactions but no replication position at TXID 1 (litestream's first |
| + sync) and only a database with no transaction at all at 0; a build or |
| + install at position 0 writes no snapshot and no anchor and publishes a |
| + marker with `snapshot_txid = 0`; `restoreCalc` of such a generation |
| + yields an empty database; INV-12 in `issue` refuses any LTX PUT with a |
| + zero TXID. Rule `valid-ltx` (the mutation writes `[1, 0]` and `[0, |
| + 0]`, rev 7.8's build). Witness `wEmptyBootstrap`: a create's first |
| + wake, no LTX file before the first transaction, the first transaction |
| + as the first upload, a disk loss and a cold wake. |
| +- **Provenance (R8-4).** `warmProvenance`: the lineage file names the |
| + journalled predecessor's `{generation, session}`, the predecessor's |
| + box is this box, and the database stands at or beyond its generation's |
| + remote position (the integrity check's stand-in: its uploads came from |
| + it). Otherwise the build restores the predecessor generation and |
| + declares the warm database's unreplicated acknowledged writes lost. |
| + `initRecord` writes no lineage. Rule `warm-provenance` (the mutation |
| + takes any database of the predecessor generation, rev 7.8's rule). |
| + Witness `wWarmLineageMismatch`: a stale copy of the database with a |
| + foreign lineage replaces the box's; the cold admission restores from |
| + the remote under the rule, and under the mutation serves the copy, |
| + missing a durable write (INV-2). |
| +- **Close evidence (R8-5).** `localDB.Issued` tracks every request of the |
| + writer's lifetime (level-0 uploads, compactions and their retention |
| + deletes, snapshots and their retention), `Uncertain` is set when the |
| + client gives up on an upload and retries it, and `settled` is every |
| + tracked request done, the queue drained and not uncertain; `closeStep` |
| + refuses to certify an uncertain session. Rule `close-evidence` (the |
| + mutation checks the level-0 queue alone, rev 7.8's drain). Witness |
| + `wRetryUnresolved`: one upload is held, the client times out and |
| + retries, the retry lands, the original stays outstanding; the clean |
| + stop writes no certificate under the rule and writes one under the |
| + mutation. |
| +- **Model faults found and fixed this round** (all before the final |
| + numbers): the first rev 7.9 build made the admission CAS before the |
| + health check, so failing starts admitted sessions in a storm (13 / 300 |
| + seeds); a stalled worker's replay of a finished cold admission's build |
| + took stop evidence of the running writer and replaced its database |
| + with the build's snapshot (seed 10382 / 30,000; the revalidation step |
| + now includes the writer state); the cold build left the carried files |
| + under the dead writer's stamp, and the next dirty install parked an |
| + artifact of a retired stamp (seed 453 / 30,000, INV-6); a source that |
| + lost its disk during a rollback or revert compared a missing database |
| + with its stop digest and stuck (seed 95 / 300); the local oracle |
| + refused a write declared lost that landed anyway and came back through |
| + a cold admission's remote baseline (seed 5863 / 30,000; it now accepts |
| + what the files carry, as the cold-restore oracle does); a seal of a |
| + database with transactions and position 0 was taken for empty and the |
| + landing installed nothing (seed 19023 / 30,000); the biased schedule's |
| + unbounded hold, one per park of a dead generation, chained across the |
| + whole convergence window (seed 20077 / 30,000; chaos only now); a lost |
| + target's unfinished cold admission inside the landing blocked the |
| + source's rollback probe for good (seed 58795 / 100,000; the next holder |
| + of `op.exec` abandons it and parks its generation); every clean close |
| + outside `serving` was dropped, so a rollback's reopened source was |
| + admitted cold at every wake and the rollback never released (seed 84087 |
| + / 100,000; a writer inside an operation certifies like any other, and |
| + the close is dropped only for a push, a move's cut, a delete or a |
| + purge, since the first correction let a push's writer certify into the |
| + superseded generation, seed 4493 / 30,000). The |
| + diagnostics added for these (why an admission is cold, which baseline a |
| + build takes, what keeps a run from converging) stay in the model. |
| + |
| **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 |
| @@ -2871,7 +3180,31 @@ 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.8, on the final model (claim rev 6.6: writer epochs; the |
| +**Rev 7.9, on the final model (claim rev 6.8 and 6.8.1: writer sessions, |
| +admission on every path, the empty generation, provenance, close |
| +evidence): 30,000 seeds, zero violations; 100,000 seeds, zero |
| +violations** (145 s and 327 s). Across the 100,000 seeds: |
| +147,788 completed operations, among them 43,976 cold admissions |
| +(21,499 warm, 24,385 opened after a cold build, 26,228 |
| +fresh installs; 25,754 clean closes, 644 closes |
| +refused as uncertain, 2 stale certificates, 3,930 |
| +wakes that waited for a draining writer, 30,732 builds from |
| +the remote and 14,731 from the warm database, 1,459 |
| +warm databases refused for want of provenance, 171 probes |
| +restarted, 3 cold admissions abandoned when their box lost `op.exec`), 1,126 completed moves, 1,396 clean and |
| +121 dirty rollbacks, 266 pre-flip reverts, |
| +258 declared losses, 24,666 pushes, 89,526 |
| +delete-park-free cycles and 7,561 lost disks (4,935 |
| +with a crash); 19,392 LTX compactions, 13,463 snapshot |
| +rotations, 945 level-0 upload retries, 0 uploads |
| +skipped at the remote position, 54,460 anchors; 25,969 |
| +local stamp records lost and re-initialized; 49,209 requests |
| +completed after `H`; 32,144 staging signatures refused as |
| +stale; 30,756 creates restarted on a 412. Every oracle left |
| +the system unchanged. The model faults the new protocol exposed before |
| +these baselines are listed in §14.2.2. |
| + |
| +**Rev 7.8, on 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 |
| @@ -3064,37 +3397,69 @@ 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.8 model (734a7f5b), with the strict classification, |
| +on the final rev 7.9 model (bdd9d404; its Go files are dfc352ef's), 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 38 rules that have them. A rule is caught if |
| +same mutation, for the 44 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 **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.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). |
| +section does too. The model has **90 rules**: rev 7.8's 84 plus |
| +`writer-session` (R8-1), `admit-everywhere` and `exec-writer` (R8-2, |
| +claim rev 6.8.1), `valid-ltx` (R8-3), `warm-provenance` (R8-4) and |
| +`close-evidence` (R8-5). `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.8's |
| +counts are in the rev 7.8 spec (3c5f742a); writer sessions change what |
| +every wake does, so sweep counts moved throughout; every witness |
| +verdict is unchanged, bar the admission scenario, whose named failure is |
| +INV-6 now (below). |
| | | rules | |
| |---|---| |
| -| 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) | |
| +| caught alone by the sweep at 3,000 seeds | 59 | |
| +| caught alone by the sweep at 30,000, and by their witness | 6 (`declare-lost-compute`, `evidence-whole-tree`, `lost-quarantine`, `orphan-order`, `restore-overlap`, `rollback-journal`) | |
| +| caught alone by the sweep at 100,000, and by its witness | 2 (`newest-l0`, `writer-session`) | |
| +| caught alone by their witness only; the sweep misses them at 30,000 | 8 (`admit-everywhere`, `close-evidence`, `close-waits`, `closed-marker`, `live-set-region`, `recovery-generation`, `restore-gap-closed`, `warm-provenance`) | |
| +| caught only in a stated combination: the witness holds alone and under every proper subset, and violates with the partners | 8 (the admission combination has four members now) | |
| +| subsumed: the witness holds under every combination tried | 2 (`door-reread`, `door-by-version`, by C3a and by writer epochs; historical results only, below) | |
| | liveness only | 2 (`readiness-key`, `config-before-probe`) | |
| | unreachable under claim rev 5 | 1 (`readiness-quiet`) | |
| | unexercised | **0** | |
| -**What rev 7.8 moved.** The writer-epoch rules are **witness-only**: |
| +**What rev 7.9 moved.** Of the six new rules, `valid-ltx` is caught |
| +everywhere (558 / 3,000, 5,273 / 30,000: a position-0 build writes a |
| +file the encoder refuses, and INV-12 sees it at the PUT), `exec-writer` |
| +only in the admission combination (its witness holds alone and under |
| +every proper subset of the four), and four are witness-only at 3,000 and |
| +30,000: `writer-session` (0, 0, then **1 / 100,000**, seed 63342: the |
| +random sweep reached a dead session's certificate that still matched |
| +the remote maximum, the R8-1 schedule), `admit-everywhere` (0 / 3,000, 0 |
| +/ 30,000, 0 / 100,000), `warm-provenance` (0, 0, 0) and `close-evidence` |
| +(0, 0, 0). Rev 7.8's writer-epoch rules keep their shape: |
| +`recovery-generation`, `closed-marker` and `close-waits` 0 / 3,000, 0 / |
| +30,000, 0 / 100,000, `newest-l0` 0, 0, 1 / 100,000, `build-completion` |
| +655 / 3,000. The admission scenario's named failure is INV-6: with the |
| +four fences gone the non-exec source's wake is a cold admission whose |
| +installing CAS moves `holder.stamp` under the target, before the two |
| +writers would collide (INV-1); the four-rule combination 7 / 30,000, 17 |
| +/ 100,000, the four with `start-check` in place of its generation clause |
| +7 / 30,000, and the three box-side fences alone **0 / 30,000 with the |
| +witness held**: under writer sessions the old source's wake has no |
| +certificate for the current session, and `exec-writer` alone refuses it |
| +(`expected-outcomes.txt`). Rev 7.7's rules hold their rates |
| +(`anchor-acked` 110 / 3,000, 1,218 / 30,000, 4,303 / 100,000; |
| +`return-stamp` 48 / 3,000, 503 / 30,000, 1,774 / 100,000; |
| +`restore-anchor` 75 / 3,000, 854 / 30,000, 2,905 / 100,000; |
| +`root-advance` 68 / 3,000, 643 / 30,000, 2,267 / 100,000; |
| +`location-per-incarnation` 28 / 3,000, 336 / 30,000, 1,081 / 100,000). |
| +Sixteen rules the sweep misses at 3,000 are caught by their witnesses, |
| +six of them by the sweep at 30,000 and two more at 100,000; the sweep's |
| +zeros for the writer-session rules say nothing against the hazards, |
| +which the witnesses are the evidence for (R7-2's point stands). |
| + |
| +**What rev 7.8 moved.** The writer-epoch rules were **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 |
| @@ -3146,8 +3511,8 @@ witness to hold there; each witness violates with the failure it names. |
| | `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 | |
| +| `exec-admission`, `hold-op-open`, `start-check-claim-gen`, `exec-writer` (J2-R2-8; claim rev 6.8.1) | a paused open from an earlier operation lands after the commit while the source's row is still held; a request wakes the source | held, each, and under every proper subset | all four: **violated**, INV-6 (the non-exec source's cold admission moves `holder.stamp` under the target, on the way to INV-1) | 0 each; the four 7 / 30,000, 17 / 100,000 | |
| +| `start-check` (INV-4) | the same, dropping the whole start check | held, and under every proper subset | with `exec-admission`, `hold-op-open` and `exec-writer`: **violated**, INV-6 | 0; the four with `start-check` 7 / 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 | |
| @@ -3162,14 +3527,20 @@ witness to hold there; each witness violates with the failure it names. |
| | `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 | |
| +| `recovery-generation` (claim rev 6.6 §6.4a, R7-1), three scenarios and a crash | writer A's upload `[N+1]` is held in flight, A dies with its disk, B wakes; (i) B replicates its own `[N+1]`, then A's lands; (ii) A's lands after B's position is initialized and before B's upload, so litestream's loop skips B's file; (iii) A's held write updated K, B durably updates K, A's lands; (iv) a clean stop drains, then the agent crashes before the certificate | **violated** in each: with the rule B recovers into a fresh generation and A's file lands in the dead one; without it B's acknowledged write is lost on the cold restore taken the moment A's file lands (INV-2), or no recovery runs after the crash (iv) | | 0 / 3,000, 0 / 30,000, 0 / 100,000 | |
| +| `closed-marker` (claim rev 6.6 §6.4a; a certificate since rev 7.9) | a stale certificate (`max_txid` behind the remote maximum) beside the dead writer's outstanding upload | **violated**: taken as intact, B continues in place and A's late file replaces B's (INV-2) | | 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 | |
| +| `recovery-current-inputs` (§7.7, §7.8; R2-5) | a bundle is published after admission; the target writes; the rollback is dirty | **violated**: `stuck` | | 33 / 3,000 | |
| +| `writer-session` (claim rev 6.8 §6.4a, R8-1) | two sessions certify; the third dies with its disk and an upload in flight; the dead certificates still match the remote maximum | **violated**: the newest certificate readmits the box into the generation and the late upload replaces its file (INV-2) | | 0 / 3,000, 0 / 30,000, 1 / 100,000 | |
| +| `admit-everywhere` (claim rev 6.8 §6.4a, R8-2), two scenarios | (i) the committed move's target dies with its disk and an upload in flight before finalization; (ii) the landing's probe dies with its disk and an upload in flight in its settle window | **violated** in each: admitted for ordinary wakes alone, the target continues the generation and the late upload replaces its file (INV-2); the restarted probe reuses the install generation and the landing's restore loses its write | | 0 / 3,000, 0 / 30,000, 0 / 100,000 | |
| +| `exec-writer` (claim rev 6.8.1) | the admission scenario above | held alone, and under every proper subset of the four | with the three box-side fences: **violated**, INV-6 | 0; the four 7 / 30,000, 17 / 100,000 | |
| +| `warm-provenance` (claim rev 6.8 §6.4a, R8-4) | a stale copy of the database with a foreign lineage replaces the box's before a crash; the cold admission takes its baseline | **violated**: the copy is served and a durable write is missing (INV-2) | | 0 / 3,000, 0 / 30,000, 0 / 100,000 | |
| +| `valid-ltx` (R8-3) | a create's first wake into an empty generation, then a disk loss and a cold wake | **violated**: the build writes `[1, 0]` and `[0, 0]`, which the encoder refuses (INV-12) | | 558 / 3,000, 5,273 / 30,000 | |
| +| `close-evidence` (claim rev 6.8 §6.4a, R8-5) | an upload is held past the client's timeout; the retry lands; the original stays outstanding; a clean stop | **violated**: the certificate is written while the original is unresolved | | 0 / 3,000, 0 / 30,000, 0 / 100,000 | |
| **The purge fence, the ETag condition and C5a.** `purge-claim-fence` |
| (CC21) is caught alone by the sweep: 28 / 3,000, 240 / 30,000. |
| @@ -3184,8 +3555,8 @@ its two pairs 243 and 263 / 30,000. |
| | rule | result | what the model finds | |
| |---|---|---| |
| | `location-per-incarnation` (claim C3a) | **caught alone**: 31 / 3,000, 385 / 30,000 | with the shared location, the planner takes the previous incarnation's files (highest `MaxTXID` wins), and the cold restore equals neither incarnation's acknowledged writes; the C3a and door oracles see the rest | |
| -| `door-reread` (claim §6.5 O2) | with `location-per-incarnation`: 432 / 30,000, of which 196 are door violations; witness violated | a listing authorized for the old incarnation selects the new incarnation's object | |
| -| `door-by-version` (claim §6.5) | with `location-per-incarnation`: 385 / 30,000, of which 60 are door violations; witness violated with C3a alone | a handle signed before the delete opens the key's current object after the recreate | |
| +| `door-reread` (claim §6.5 O2) | **rev 7.4 to 7.7, historical**: with `location-per-incarnation` 432 / 30,000, of which 196 were door violations, and its witness violated. **Since rev 7.8**: witness retired; the pair's sweep count is the partner's own (below) | a listing authorized for the old incarnation selected the new incarnation's object, when a recreated incarnation reused the generation | |
| +| `door-by-version` (claim §6.5) | **rev 7.4 to 7.7, historical**: with `location-per-incarnation` 385 / 30,000, of which 60 were door violations, and its witness violated with C3a alone. **Since rev 7.8**: witness retired; the pair's sweep count is the partner's own (below) | a handle signed before the delete opened the key's current object after the recreate, when a recreated incarnation reused the generation | |
| The three-rule combination `door-by-version` + `door-reread` + |
| `location-per-incarnation` that rev 7.4 also reported is **not a minimal |
| @@ -3193,50 +3564,56 @@ 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: 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 ‡). |
| +**Caught alone: 75 of 90** (59 by the sweep at 3,000; 6 by the sweep at |
| +30,000 and by their witness, marked †; 2 at 100,000 and by its witness, |
| +marked ††; 8 by their witness alone, marked ‡). |
| | rule | seeds failing | | rule | seeds failing | |
| |---|---|---|---|---| |
| -| `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 |
| +| `abort-target-owner` | 887 / 3,000 | | `admission-registration` | 38 / 3,000 | |
| +| `admit-everywhere` ‡ | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 | | `anchor-acked` | 110 / 3,000, 1,218 / 30,000, 4,303 / 100,000 | |
| +| `build-completion` | 655 / 3,000 | | `cancelled-creates` | 383 / 3,000 | |
| +| `claim-never-deleted` | 3 / 3,000, 44 / 30,000 | | `claim-op-exclusive` | 69 / 3,000 | |
| +| `close-evidence` ‡ | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 | | `close-waits` ‡ | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 | |
| +| `closed-marker` ‡ | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 | | `commit-before-open` | 8 / 3,000, 82 / 30,000 | |
| +| `cut-deadline` | 9 / 3,000 | | `declare-lost-compute` † | 0 / 3,000, 1 / 30,000, 1 / 100,000 | |
| +| `dirty-return` | 1 / 3,000, 21 / 30,000 | | `evidence-from-state` | 2,824 / 3,000 | |
| +| `evidence-whole-tree` † | 0 / 3,000, 3 / 30,000 | | `fence-by-installation` | 505 / 3,000, 4,403 / 30,000 | |
| +| `fence-etag` | 30 / 3,000, 218 / 30,000 | | `fence-stamp` | 466 / 3,000, 4,603 / 30,000 | |
| +| `files-carried` | 39 / 3,000 | | `floor-boot-recovery` | 2,605 / 3,000 | |
| +| `fresh-admission` | 9 / 3,000 | | `fresh-incarnation` | 46 / 3,000 | |
| +| `generation-conditional` | 33 / 3,000, 313 / 30,000, 972 / 100,000 | | `hostguard` | 7 / 3,000 | |
| +| `legacy-discovery` | 347 / 3,000, 3,413 / 30,000 | | `live-set-region` ‡ | witness; sweep 0 / 3,000, 0 / 30,000 | |
| +| `location-per-incarnation` | 28 / 3,000, 336 / 30,000, 1,081 / 100,000 | | `lost-quarantine` † | 0 / 3,000, 15 / 30,000 | |
| +| `lost-return-park` | 4 / 3,000, 38 / 30,000, 110 / 100,000 | | `markers-last` | 2 / 3,000, 9 / 30,000 | |
| +| `newest-l0` †† | 0 / 3,000, 0 / 30,000, 1 / 100,000 | | `obligations-block-ops` | 35 / 3,000 | |
| +| `orphan-no-deadline` | 49 / 3,000 | | `orphan-order` † | 0 / 3,000, 1 / 30,000 | |
| +| `park-all-versions` | 539 / 3,000 | | `park-by-version` | 2,547 / 3,000 | |
| +| `park-skip-lock` | 2,716 / 3,000 | | `participant-rows` | 2 / 3,000 | |
| +| `purge-adopts` | 6 / 3,000 | | `purge-claim-fence` | 29 / 3,000, 241 / 30,000 | |
| +| `purge-journal` | 1,962 / 3,000 | | `purge-reserve-first` | 2,158 / 3,000 | |
| +| `quiet-before-ack` | 197 / 3,000 | | `recovery-current-inputs` | 33 / 3,000 | |
| +| `recovery-generation` ‡ | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 | | `recovery-pass` | 2,488 / 3,000 | |
| +| `registration-recovery` | 2,136 / 3,000 | | `restore-anchor` | 75 / 3,000, 854 / 30,000, 2,905 / 100,000 | |
| +| `restore-by-generation` | 87 / 3,000 | | `restore-gap-closed` ‡ | witness; sweep 0 / 3,000, 0 / 30,000 | |
| +| `restore-overlap` † | 0 / 3,000, 5 / 30,000 | | `retirement-ids` | 412 / 3,000 | |
| +| `return-stamp` | 48 / 3,000, 503 / 30,000, 1,774 / 100,000 | | `revalidate-before-effect` | 14 / 3,000, 173 / 30,000 | |
| +| `revert-journal` | 13 / 3,000 | | `rollback-journal` † | 0 / 3,000, 1 / 30,000 | |
| +| `root-advance` | 68 / 3,000, 643 / 30,000, 2,267 / 100,000 | | `sdk-no-resign` | 10 / 3,000 | |
| +| `seal-by-version` | 1 / 3,000, 9 / 30,000 | | `sign-at-check` | 10 / 3,000 | |
| +| `sign-before-safeuntil` | 25 / 3,000 | | `source-readiness` | 12 / 3,000 | |
| +| `staging-quiet` | 1 / 3,000, 7 / 30,000 | | `stale-hold-release` | 2 / 3,000 | |
| +| `straggler-sweep` | 753 / 3,000 | | `sweep-namespace` | 546 / 3,000 | |
| +| `sweep-staging` | 23 / 3,000 | | `target-park` | 30 / 3,000 | |
| +| `timer-canonical` | 2 / 3,000 | | `timer-freeze` | 1 / 3,000, 27 / 30,000 | |
| +| `valid-ltx` | 558 / 3,000, 5,273 / 30,000 | | `warm-provenance` ‡ | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 | |
| +| `writer-session` †† | 0 / 3,000, 0 / 30,000, 1 / 100,000 | | | | |
| + |
| +**Caught only in a combination: 10 rules**, every combination rerun this |
| +round; `exec-writer` joins the admission combination (claim rev 6.8.1); |
| +`door-reread` and `door-by-version` are subsumed (above) and their rows |
| +below are **historical**, kept only to record what the pairs once |
| +showed. `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 |
| @@ -3247,21 +3624,22 @@ subset in the gate. |
| | `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 | |
| +| `exec-admission` + `hold-op-open` + `start-check-claim-gen` + `exec-writer` | 7 / 30,000, 17 / 100,000 | every proper subset 0 in the gate (300 seeds, witness held); the three box-side fences 0 / 30,000 | violated, INV-6 | the non-exec source admitted cold under the target, Astra's J2-R2-8 trace under writer sessions | |
| +| `exec-admission` + `hold-op-open` + `start-check` + `exec-writer` | 7 / 30,000 | (above) | violated, INV-6 | the same, dropping the whole start check | |
| +| `door-reread` + `location-per-incarnation` (**historical**, rev 7.7: 432 / 30,000, 196 door violations, witness violated) | not rerun: the witness is retired and the rule is subsumed | `location-per-incarnation` 336 / 30,000 this round | retired | under writer epochs the pair adds nothing the partner's own count does not show; no current witness evidence is claimed | |
| +| `door-by-version` + `location-per-incarnation` (**historical**, rev 7.7: 385 / 30,000, 60 door violations, witness violated with C3a alone) | not rerun: the witness is retired and the rule is subsumed | `location-per-incarnation` 336 / 30,000 this round | retired | the same | |
| | `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. |
| +Every live combination was rerun on the rev 7.9 model; the gate runs |
| +every proper subset of the admission four with the witness, which holds |
| +under each. The door rows are historical (R8-6): rev 7.8 reported the |
| +partner's count in the pair's column and still said "witness violated"; |
| +the pairs have not been rerun since the witnesses were retired, and the |
| +rows claim no current evidence beyond the partner's own count. |
| **Liveness only: 2.** `readiness-key` (T2) and `config-before-probe`. |
| They have no witness: neither can violate an invariant. |
| @@ -3271,8 +3649,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; 42 witnesses, 122 runs); the 30,000- and 100,000-seed |
| -baselines, this sweep and the witnesses are the evidence for rev 7.8. |
| +a second; 49 witnesses, 182 runs); the 30,000- and 100,000-seed |
| +baselines, this sweep and the witnesses are the evidence for rev 7.9. |
| #### 14.2.6 What the model does not prove |
| @@ -3648,6 +4026,30 @@ 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.8 (5462d293) and 6.8.1 (a963d98d), after joint round 8: |
| +no change requested, three notes.** Rev 6.8's §6.4a answers R8-1 to |
| +R8-4: `AdmitWriter` as the one CAS before any upload, `holder.session`, |
| +the writers journal with its predecessor, cold mode as the installing |
| +CAS that never replaces the operation, per-session certificates never |
| +deleted, the three provenance conditions, the empty bootstrap; rev 6.8.1 |
| +adds that only `op.exec` may open replication, in every op kind. Rev 7.9 |
| +encodes all of it (§5.1 step 9, §7.14, §14.2.2) and owns the data path: |
| +the phase table of which box is admitted in which phase and the CAS that |
| +handed it `op.exec` (§7.14), the evidence rule for the certificate |
| +(every request of the session's lifetime, a sticky uncertainty, R8-5), |
| +the integrity check's content (the WAL in place), the build at position |
| +0 (no files; `snapshot_txid = 0`), the stand-in for "a database that |
| +holds transactions but never replicated" (a snapshot at TXID 1, the |
| +first sync's TXID). Notes for platform-1e (`moves-claim-questions.md`, |
| +rev 7.9 heading): the warm rule's "or the warm baseline rules below allow |
| +otherwise" is read here as nothing beyond the three conditions, so a |
| +certificate of another box never admits warm; the admission CAS is made |
| +as the process starts, after the start and health checks, so a start |
| +that fails admits no session (the claim's "before the writer issues any |
| +upload" allows either order, and the earlier one stormed); and a source |
| +that lost its disk during a revert or rollback skips the digest check |
| +and is admitted at its probe, since it has nothing to verify (§7.14). |
| + |
| **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 |
| @@ -3996,6 +4398,23 @@ 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.15 Joint round 8 (claim b10547e1, moves rev 7.8 3c5f742a, model 734a7f5b) |
| + |
| +Round 8 found rev 7.8's marker consumption unsound under S3's semantics |
| +and its admission check too narrow (two P1s), and three P2s and a P3. |
| +Claim rev 6.8 (5462d293) rewrote §6.4a as writer sessions and epochs; |
| +rev 6.8.1 (a963d98d) added that only `op.exec` may open replication. |
| + |
| +| finding | rev 7.9 | |
| +|---|---| |
| +| R8-1 (P1) the clean-close marker is not one-use: deleting the version read makes no delete marker and can expose an older version; a delayed or replayed PUT with a matching stamp and TXID recreates it | claim rev 6.8 encoded: `holder.session`, `AdmitWriter` as one CAS before any upload, the certificate per session (`closed/<session>.json`) never deleted, warm continuation only for the observed session's certificate, which the admitting CAS retires by moving the session (§5.1 step 9, §7.14). Rule `writer-session`; witness: a dead session's certificate with a matching stamp and `max_txid` (§14.2.5) | |
| +| R8-2 (P1) the epoch check ran only at an ordinary wake; a committed landing's wake, a restarted probe, a reverted source, an opened rollback recovery and a push bypassed it; recovery replaced the operation; the crash-with-disk fault reached `serving` alone | every path admitted, inside the operation, by `op.exec` alone (claim rev 6.8.1); §7.14's phase table; the fault reaches every operation. Rules `admit-everywhere`, `exec-writer`; witnesses: the committed landing's crash, the probe restart, the non-exec writer (§14.2.5) | |
| +| R8-3 (P2) a never-started instance has no position; the prescribed snapshot `[1, 0]` and anchor `[0, 0]` are files the pinned encoder refuses | the empty generation: no file until the first transaction, the app starts first, `snapshot_txid = 0` (§5.1 step 9, §7.14); INV-12 and rule `valid-ltx`, witness: a create's first wake; `TestFact_R8_3_EmptyBootstrap` (§14.2.1) | |
| +| R8-4 (P2) the warm baseline rule proved identity, not ownership or freshness | the three conditions (lineage equal to the journalled predecessor's `{generation, session}`, predecessor box this box, integrity with the WAL in place), the predecessor journalled before the stamp is activated, re-initialization writes no lineage (§5.1 step 9, §6.4, §7.14). Rule `warm-provenance`; witness: a stale copy with a foreign lineage | |
| +| R8-5 (P2) the model's drain checked the level-0 queue alone; a timed-out original's retry could succeed and the marker be written; maintenance uploads were outside the accounting | every request of the session's lifetime tracked, a sticky uncertainty, maintenance included (§5.1 step 9); the pinned replica's lazy remote position modelled. Rule `close-evidence`; witness: a retry that lands while its original stays unresolved | |
| +| R8-6 (P3) the retired-door table contradicted its conclusion | historical and current results separated; no current witness evidence claimed for the retired witnesses; the pairs not rerun (§14.2.5) | |
| +| D's limits: the empty bootstrap was the concrete gap in the grounding | closed by `TestFact_R8_3_EmptyBootstrap`; the other limits (no abrupt replacement through `Held`, no S3 version visibility, no multipart or delayed completion in the real-library tests) stand as §14.2.6 says | |
| + |
| ### 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 |