amadan
spec: move-any-app rev 7.10: joint round 9, no local database reuse (claim rev 6.9), every number rerun (#175)
Paul's ruling to simplify: a box never reuses its local database; every admitted writer purges it and restores the certified remote, warm (any op.exec box, up to the certificate's max_txid) or cold (the predecessor's remote, or an operation's prepared generation opened once). Only warm and cold; holder.generation the only authoritative generation; holder.writer_box and writes_lost; the admission bound to the observed op.id and phase (INV-13); close evidence by client outcome for every request class; the behaviour change against today's activator stated (§7.14). §14.2.5's tables regenerated from the retained verdicts (R9-6). 92 rules, 52 witnesses; 30,000 and 100,000 seeds clean; mutate.sh at 3,000, 30,000 and 100,000; the model faults the sweeps found before the final numbers; §19.4 readings for claim rev 6.9; §22.16 dispositions.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
1 file changed,
+596
−305
docs/superpowers/specs/2026-10-02-move-any-app-design.md+596 −305
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 26d8ddcc8..97fc68f9b 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,50 @@ |
| # Move any app or instance to another region: Phase 1, a safe single-instance move |
| **Date:** 2026-10-04 |
| -**Revision:** 7.9. |
| +**Revision:** 7.10. |
| + |
| +- **Rev 7.10** answers **joint round 9** (`CODEX-FINDINGS-JOINT-R9.md`, |
| + cited "R9-n") under Paul's ruling to **simplify**, and is written |
| + against **claim spec rev 6.9** (f6180ae4); §22.16 has every disposition. |
| + **A box never reuses its local database.** Every admitted writer, warm |
| + or cold, in every phase, purges the local database (an error-returning |
| + purge; if it fails the writer does not start) and restores from the |
| + certified remote: warm, the same generation up to the certificate's |
| + `max_txid`; cold, the predecessor generation's remote. Lineage, |
| + provenance and the `warm-provenance` rule are gone (R9-1 closed by |
| + construction; its clean-close stale-database scenario is the witness |
| + `wStaleLocalAfterClose`). Warm continuation needs only the certificate |
| + for the observed session with a matching `max_txid`, and **any |
| + `op.exec` box** may continue (claim rev 6.8.2 reverses rev 7.9's |
| + same-box reading). **`holder.writer_box`** is set by every admission and |
| + survives operation replacement; a cold admission of an uncertified |
| + session records **`writes_lost {box: observed writer_box, generation, |
| + session, remote_max_txid}`** in its journal entry and the box alerts, so |
| + a crash with acknowledged, unuploaded writes loses them declared, never |
| + silently (R9-2). **Only warm and cold survive** (R9-3): a first install |
| + is a cold admission into an empty generation; `holder.generation` is the |
| + only authoritative generation in every kind and phase; a probe or |
| + recovery that opens replication is a cold admission that moves it; an |
| + operation's prepared generation is opened once, by its probe's cold |
| + admission, and never re-entered; a fresh generation roots at the |
| + writer's full first upload, made after the CAS and before its marker; |
| + a failed cold start leaves an empty, unpublished generation for the |
| + sweep and the next attempt is cold again. Admission happens after |
| + readiness and before any upload, and is **bound to the observed `op.id` |
| + and `op.phase`**, serving's `""` compared literally, refused in |
| + deleting, parking, purging and creating (R9-4; INV-13). Close evidence |
| + is **client-observed success** for every request class, level-0, |
| + compaction, snapshot and retention, with a sticky uncertainty for a |
| + timeout or a lost response (R9-5). §14.2.5's tables are regenerated from |
| + the retained verdicts (R9-6). The spec states plainly how today's |
| + activator differs (§7.14: production keeps the warm cache and restores |
| + only when the local copy is absent; this is a behaviour change, costing |
| + a restore per wake and the unuploaded writes on a crash). Rules |
| + `remote-baseline`, `writes-lost`, `admit-bind-op` (92 in all); |
| + witnesses for the stale local database after a clean close, the silent |
| + loss, the stale closure during a delete, a maintenance retry and a lost |
| + response (52 in all); the whole-start-check witness is retired, subsumed |
| + by regional restores. Results in §14.2.3 and §14.2.5. |
| - **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), |
| @@ -880,112 +923,122 @@ fails there first (§14.2.6). |
| through compaction and expired it when the local position had run |
| ahead of the uploads (R7-3; the model's `newest-l0`). |
| 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). |
| + never share a generation, every path that opens replication is |
| + admitted, and a box never reuses its local database (claim rev 6.9 |
| + §6.4a; R7-1, R8-1 to R8-5, R9-1 to R9-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.9 states the rule and this spec owns the data path: |
| + - **`AdmitWriter`, one claim CAS after readiness and before any |
| + upload.** `holder.session` is the claim `gen` of the CAS that |
| + admitted the current writer session; `holder.writer_box` is the box |
| + it admitted (R9-2). Every path that opens replication makes this CAS: |
| + an ordinary wake, a committed move's target serving while the claim |
| + is still `landing`, a probe and a restarted probe, a reverted source, |
| + an opened rollback recovery, a push's writer (R8-2). The library's |
| + call is `AdmitWriter(Admission{ObservedOpID, ObservedPhase, |
| + ObservedSession, ObservedGeneration, Box, Mode, NewGeneration, |
| + PredecessorCertified, RemoteMaxTXID})`. It requires the observed |
| + `op.id` and `op.phase` (serving's `""` compared literally, so a |
| + closure computed under serving fails once any operation starts), the |
| + observed `holder.session` and `holder.generation`, and **`op.exec` to |
| + be this box**, in every op kind (claim rev 6.8.1); it is refused in |
| + `deleting`, `parking`, `purging` and `creating` (R9-4). After a |
| + conflict the box re-establishes its evidence, the certificate, the |
| + readiness, the exec handover, rather than re-reading alone. It |
| + writes `holder.session = its resulting gen`, `holder.writer_box = |
| + this box`, and a journal entry in `op.journal.writers` `{session, |
| + box, generation, stamp, mode, predecessor: {session, box, generation, |
| + stamp}, writes_lost?}`, the predecessor copied from the claim it |
| + observed. It **never replaces the operation**: kind, id, phase, |
| + participants, obligations and the rest of the journal are kept. |
| + - **A box never reuses its local database (R9-1).** Before it starts, |
| + every admitted writer purges the local database with an |
| + error-returning purge; if the purge fails the writer does not start |
| + (a transient error: the next attempt purges again). It then restores |
| + from the certified remote baseline, under the lease, and starts the |
| + app on that; the restore is version-pinned and the planner's (steps |
| + 4 and 5). A warm database is never the baseline, whatever it holds: |
| + acknowledged writes it held that never uploaded are lost, and they |
| + are **declared** (below), never silently dropped. There is no |
| + lineage file and no provenance check. |
| + - **Warm continuation** is an admission in **warm** mode: legal only |
| + if `closed/<holder.session>.json` exists for the observed session and |
| + its `max_txid` equals the generation's remote maximum TXID over every |
| + level (`PredecessorCertified`). **Any `op.exec` box** may continue |
| + on it (claim rev 6.8.2): the certificate proves every upload of the |
| + session completed, whichever box made them. The admitting CAS moves |
| + `holder.session` forward, so that certificate names a dead session: a |
| + delayed, replayed or re-created certificate of any earlier session |
| + can never authorize anything again. The writer restores the same |
| + generation **up to the certificate's `max_txid`**, refusing to start |
| + on a restore that stops short of it, and reads its remote position |
| + at its first sync (litestream initializes it lazily). |
| + - **Everything else is cold**: no certificate for the observed |
| + session, a mismatched `max_txid`, any doubt. A cold admission is an |
| + installing CAS: in the same write a new `holder.generation` |
| + (`NewGeneration`) and `holder.stamp = the resulting gen`. The new |
| + generation is either the operation's **prepared** generation (a |
| + landing's or a push's `g-<op id>/`, built from the sealed archive |
| + with its snapshot `[1, N]` and anchor `[N, N]`; a dirty rollback's |
| + return generation), opened exactly once, by its probe, and never |
| + re-entered once it is `holder.generation` or an ancestor of it (a |
| + dead writer's uploads may still land in it); or a **fresh** id. The |
| + writer restores the prepared generation from its pinned snapshot, or |
| + the predecessor generation's remote (`holder.generation` as |
| + observed) for a fresh one, in its own region; a fresh generation is |
| + **empty** until the writer's first upload, the full file `[1, 1]` of |
| + the restored baseline (fact R5-1c), made after the CAS and before the |
| + marker. When the observed session had no certificate, the CAS |
| + records **`writes_lost {box: holder.writer_box, generation, session, |
| + remote_max_txid}`** in its journal entry and the box raises an alert |
| + (R9-2): the predecessor's acknowledged writes beyond its uploads are |
| + gone with its database. The box is never inferred from `op.exec`. |
| + - **Only warm and cold exist (R9-3).** A first install, after a create |
| + or an adoption with nothing replicated, is a cold admission into an |
| + empty generation: no LTX file until the first committed transaction, |
| + never a zero-TXID file (`TestFact_R8_3_EmptyBootstrap`); the app |
| + starts first and may create its database, as the activator does |
| + today. There is no fresh, reserve, build or open transition. |
| + `holder.generation` is the only authoritative generation in every |
| + kind and phase: a probe or a recovery that opens replication is a |
| + cold admission that moves it, never an op-journal generation. A |
| + failed cold start leaves an empty, unpublished generation for the |
| + sweep, and the next attempt is cold again. Dead generations are |
| + parked by a `park-generation {region, generation}` chore with owner |
| + `region:<r>`. |
| - **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. |
| + its lifetime** returned **success to the client, within the client's |
| + wait** (R8-5, R9-5): every level-0 upload, every compaction and |
| + snapshot upload, every retention delete. A request the client timed |
| + out on, whether or not it later completed on the server (a lost |
| + response), one the server refused, and any retry after a timeout |
| + make the session **uncertain for good**. A session that can prove |
| + completion writes `<location>/<generation>/closed/<session>.json` |
| + `{session, box, max_txid, closed_at}` once (`If-None-Match`), then |
| + releases its lease; nothing of the host may run when it certifies |
| + (the unit stop kills the cgroup; a descendant that escaped it makes |
| + the close fail rather than wait, since its writes would be lost |
| + silently at the next purge, and the next wake is cold and declares). |
| + A certificate PUT not acknowledged within the client's wait ends the |
| + close uncertified: the PUT may still land, and a later wake that |
| + finds it may continue warm, since the drain was complete; the next |
| + wake is cold. **No certificate is ever deleted or reused**. |
| + 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. An operation that |
| + takes the writer over, a push, a move's cut, a delete or a purge, |
| + drops a pending close: the generation is being replaced or parked. |
| - **Writers are bound to their generation.** The replica client is |
| constructed for the `{holder.location, holder.generation, session}` |
| the writer was admitted with and refuses any key outside |
| @@ -995,8 +1048,7 @@ fails there first (§14.2.6). |
| 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). |
| + requests had completed. |
| - **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; |
| @@ -1010,13 +1062,15 @@ fails there first (§14.2.6). |
| 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. |
| + non-exec writer is refused; a valid certificate over a stale local |
| + database restores the remote; a crash with an unuploaded write is |
| + declared; a stale closure during a delete is refused; an empty first |
| + wake and an empty install write no file; a retry that succeeds while |
| + its original stays unresolved, a maintenance retry and a lost response |
| + write no certificate. The cost is a restore at every wake, warm or |
| + cold, a full first upload per fresh cold generation (none for an |
| + empty one), three local passes for an operation's prepared generation |
| + as §7.3 prices an install, and a dead generation to park. |
| So: |
| @@ -1400,20 +1454,22 @@ Phase 1 uses the claim spec's park (§6.2 there) and local retirement |
| 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 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).** |
| + 6.9 §6.4a; §5.1 step 9, §7.14): it writes a new `holder.generation`, |
| + a new `holder.stamp` and `holder.writer_box` in one write, with the |
| + predecessor's `{session, box, generation, stamp}` journalled in the |
| + same write; the box's record activates the new stamp from its next |
| + fresh read, and the carried files are retagged with it at the CAS, |
| + whether or not the start completes (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; rev 7.10's first |
| + model retagged them only at the start, seed 62 / 300); the restored |
| + database carries it; the dead writer's stamp retires with it. The |
| + purge of the local database that precedes every restore (§5.1 step 9) |
| + is not a retirement event: it deletes a file no installation will run |
| + again. There is no lineage file (rev 7.10). 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 |
| @@ -2076,85 +2132,108 @@ 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, 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 | | |
| +| landing: probing, probed (the settle window) | | kills the tree, restarts the probe, which is an `AdmitWriter` within the landing (§7.14): cold, into a fresh generation restored from the dead probe's, since the dead probe's session has no certificate | | |
| | 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`; a source whose database went with the crash verifies nothing and is admitted at its probe, warm or cold (§7.14) | | | |
| +| 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 like any writer (§7.14) | | | |
| | stuck | held; operator | | | |
| -### 7.14 Writer admission and cold admission (claim rev 6.8 §6.4a, 6.8.1; R7-1, R8-1, R8-2) |
| +### 7.14 Writer admission (claim rev 6.9 §6.4a; R7-1, R8-1, R8-2, R9-1 to R9-4) |
| 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: |
| +claim CAS made after readiness and before any upload, by the box the |
| +claim names as `op.exec`, and never by another. Two modes exist, **warm** |
| +and **cold**; nothing else (R9-3). **Which box may be admitted in which |
| +phase**, in which mode, into which generation, 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 | | |
| +| op kind, phase | the box admitted | mode and generation | `op.exec` handed to it by | |
| +|---|---|---|---| |
| +| `serving` | the serving box, at every wake | warm into `holder.generation` on a certificate for `holder.session`; else cold into a fresh generation restored from `holder.generation` | 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 | cold into the push's prepared generation `g-<push id>/` (its snapshot and anchor), opened once; a restarted probe is cold into a fresh generation restored from it | the push's claim CAS (`op.exec` = the serving box) | |
| +| `moving` (before the flip) | the source, at every wake; the target writes nothing | warm or cold as for `serving`; the source's clean closes certify | the move's claim CAS (`op.exec` = source) | |
| +| `reverting: probing, probed` | the source, as its probe starts and at every wake after | warm or cold as for `serving` (`holder.generation` is still the source's) | 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 | cold into the landing's prepared generation `g-<move id>/`, opened once; a restarted probe is cold into a fresh generation restored from it | the flip CAS, which cites the source's stop evidence (§7.5) | |
| +| `landing`, committed, not yet finalized | the target, at every wake | warm or cold as for `serving` | the same flip CAS | |
| +| `restoring: probing, probed, opened` (the source's rollback) | the source, as its probe starts and at every wake after | dirty: cold into the return generation prepared from the target's sealed copy, opened once; clean: the return CAS named the source's generation again, and the probe is warm or cold into it as for `serving` | 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`, `deleting`, `parking`, `purging` | nobody: the admission CAS refuses these kinds (R9-4, INV-13) | | | |
| 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 | |
| +CAS requires `op.exec == this box` (rule `exec-writer`) and is bound to |
| +the observed `op.id`, `op.phase` and kind (rule `admit-bind-op`; the |
| +model's general CAS condition on `op.id`, C2, already refuses a closure |
| +whose operation changed, so the binding adds the phase and the kinds). |
| +**`holder.generation` is the only authoritative generation** in every |
| +kind and phase: an operation's prepared generation (`g-<op id>/`, a |
| +rollback's return generation) is built by the operation's install phases |
| +and becomes `holder.generation` at its probe's cold admission, never |
| +before; the flip and the commit move no generation (rev 7.9's commit did). |
| +A clean rollback's **return CAS names the source's generation again** |
| +(`op.journal.src_gen`, recorded at the flip), since the target's probe had |
| +moved `holder.generation` to the target's and the target wrote nothing; |
| +the source's probe then restores from its own region's remote of it. |
| + |
| +**The admitted writer's start**, on its box, in this order; it is local |
| +bookkeeping around one claim CAS, not a set of claim transitions: |
| + |
| +| step | action | if it fails | |
| |---|---|---| |
| -| 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 |
| +| decide | read the claim; `op.exec` must be this box and the kind one that admits; the certificate for `holder.session` decides warm or cold; a cold admission's generation is the operation's prepared one if `holder.generation` is not it or a descendant of it, else a fresh id | nothing happened | |
| +| purge | delete the local database, with an error-returning purge | the writer does not start; the next attempt purges again | |
| +| restore | warm: `holder.generation` from this region's remote, to at least the certificate's `max_txid`; cold, prepared: the prepared generation from its pinned snapshot and anchor (the operation's build journal); cold, fresh: the predecessor from this region's remote. A lagging `generation.json` is this box's own unfinished start (below) or a refusal | the writer does not start; a warm restore short of `max_txid` is an alert, the remote is incomplete | |
| +| start, readiness | the app starts on the restored database and answers its readiness path | nothing admitted, the session unchanged | |
| +| **`AdmitWriter`** | the CAS of §5.1 step 9: session, writer_box, journal entry; cold: generation, stamp, `writes_lost` for an uncertified predecessor, a `park-generation {region, generation}` chore for a fresh generation's predecessor (an operation's prepared generation leaves its predecessor to the operation's finalization or rollback); the carried files are retagged with the new stamp here | a conflict: re-establish the evidence and decide again | |
| +| first upload (cold, fresh, a non-empty baseline) | the full file `[1, 1]` of the restored database, acknowledged; the generation has a root | retried with the same bytes after the client's timeout; the writer waits | |
| +| marker (cold) | `generation.json` names the new generation: the pinned snapshot identity for a prepared one, `snapshot_txid = 0` for a fresh one (its root is `[1, 1]`); never before the root exists (INV-11) | retried after the timeout; the writer waits | |
| +| anchor (warm, when the restored position is above the level-0 maximum) | `[N, N]`, acknowledged (§5.1 step 7) | retried after the timeout; the writer waits | |
| +| open | replication opens; the replica reads its remote position at its first sync; every later upload is the session's | | |
| + |
| +An admitted writer that dies between its CAS and its marker leaves |
| +`holder.generation` naming a generation `generation.json` does not: its |
| +own next attempt finds `holder.writer_box` to be itself and the marker an |
| +ancestor of `holder.generation`, and publishes the marker again (a |
| +prepared generation, from the operation's build journal) or, for a fresh |
| +generation that holds no file, takes the marker's generation as the |
| +baseline and starts cold again (the empty generation is the sweep's); |
| +another box's lagging marker is the start check's refusal (J2-R2-8). A |
| +clean rollback's return leaves the marker naming a descendant of |
| +`holder.generation`; the source publishes the source generation's marker |
| +again from its last version before anything else. |
| + |
| +**Behaviour change against today's activator.** Today `Restore` |
| +materializes the local database from S3 only when it is absent, "a |
| +no-op when the warm-cache copy is still on disk", and `doWake` relies on |
| +that: "when it's still on disk it is the warm cache: on one box, with the |
| +lease held, the local copy can only be what we ourselves checkpointed at |
| +the last sleep" (`internal/activator/activator.go`). Rev 7.10 changes |
| +this: every wake restores, warm or cold. It costs a restore per wake, |
| +one pass over the database from regional S3 at the local rate (§7.3 |
| +prices it), and it loses the acknowledged writes a crash left |
| +unuploaded, which the warm cache preserved on a same-box restart; those |
| +are declared through `writes_lost` and an alert, and bounded by the |
| +replication interval (§7.3, the sync class). What it buys is one rule |
| +with no provenance machinery: a box's database is always the certified |
| +remote's, so a cached, truncated or foreign copy can never be served |
| +(R9-1), and the claim alone decides who writes what. |
| + |
| +A cold admission costs the three local passes of an install (§7.3) for |
| +an operation's prepared generation, one full upload for a fresh one, |
| +none for an empty one, 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. |
| +could not certify (a retry, a timeout, a lost response, R9-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). |
| +writer (rev 7.9, R8-2); a target that never restored a database returns |
| +nothing dirty (rev 7.10: the probe's admission restores it, so a target |
| +whose probe never started has none). |
| ## 8. The archive (codex 19) |
| @@ -2952,6 +3031,116 @@ 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.10: joint round 9 and claim rev 6.9.** |
| + |
| +- **No local database reuse (R9-1, claim rev 6.9).** `spawn` admits every |
| + non-legacy start through `admitWriter` (the decision, no CAS) and |
| + `admitCommit` (the `AdmitWriter` CAS): it purges the box's database |
| + (`PurgeFails`, a transient fault injected at reboots and healed in the |
| + calm phase: the writer does not start), restores from the remote |
| + (`restoreCalc` of `holder.generation` for warm, to at least the |
| + certificate's `max_txid`; `restorePinned` of the operation's prepared |
| + generation from its build journal; `restoreCalc` of the predecessor for |
| + a fresh cold generation), checks readiness, makes the CAS, then |
| + finishes the start as an `openState` on the box: the full first upload |
| + `[1, 1]` for a fresh generation with content, the marker, the warm |
| + anchor when the restored position is above the level-0 maximum, each a |
| + PUT acknowledged before the next, retried with the same bytes after the |
| + client's timeout and driven by the agent's own loop (`resumeStart`), |
| + not by wakes; `atRest` counts an open in progress. A warm admission's |
| + first upload is full (fact R5-1c applies to every restore now), so |
| + `compact` makes its output full when any input is. `warmCertificate` |
| + became `certificate`: no box check (claim rev 6.8.2). Rule |
| + `remote-baseline` (the mutation keeps a local database of the |
| + generation it opens); witness `wStaleLocalAfterClose`. |
| +- **`holder.writer_box` and `writes_lost` (R9-2).** `holder.WriterBox` is |
| + written by every admission; a cold admission with `PredecessorCertified` |
| + false records `writesLost{Box: observed writer_box, Gen, Session, |
| + RemoteMaxTXID}` in its journal entry, declares the predecessor box's |
| + acknowledged, non-durable writes lost (the oracles' exemption) and logs |
| + the alert; timers are not writes. Rule `writes-lost` (the mutation loses |
| + them silently); witness `wSilentLoss`. |
| +- **Warm and cold only (R9-3).** `op.Rec`, `recStep`, `op.InstGen`, |
| + `op.Fresh`, the `open` and `fresh` modes and the recovery build are |
| + gone. `installGen` names an operation's prepared generation; its probe |
| + is a cold admission with `NewGeneration` the prepared one, never |
| + re-entered once `holder.generation` or an ancestor of it |
| + (`ancestorGen`), else a fresh id; the landing's prepared generation |
| + keeps the flip's stamp (`op.FlipGen`), every other cold admission |
| + issues one. The flip, the commit, the push's probed CAS and the dirty |
| + rollback's probed CAS move no generation; the return CAS names |
| + `op.SrcGen` (recorded at the flip) again for a clean rollback and the |
| + source republishes that generation's marker from its last version |
| + (`republishMarker`); a lagging marker is accepted only for this box's |
| + own unfinished admission or the source after a return, and an |
| + abandoned empty generation yields to its nearest ancestor with files |
| + (`parentGen`). A `park-generation` chore for a fresh generation's |
| + predecessor, in the admitting box's region. The landing's and the |
| + push's `published` phases publish nothing; the landing's `restore` |
| + phase computes the installed digest from a pure restore; a target that |
| + never restored a database returns nothing dirty. |
| +- **The admission bound to the operation (R9-4).** `admitInput` carries |
| + `ObservedOpID`, `ObservedPhase` (`phaseOf`), `ObservedSession`, |
| + `ObservedGeneration`, `Box`, `Mode`, `NewGeneration`, |
| + `PredecessorCertified`, `RemoteMaxTXID`; the CAS refuses a changed op |
| + id or phase and the kinds `deleting`, `parking`, `purging`, |
| + `creating`; INV-13 in `admitCommit` (no writer admitted into those |
| + kinds). Rule `admit-bind-op` (the mutation compares session and |
| + generation alone); witness `wStaleClosureDelete`, with |
| + `claim-cas-opid` as its partner, since the model's general CAS |
| + condition on `op.id` (C2) already refuses a closure whose operation |
| + changed. |
| +- **Close evidence by client outcome (R9-5).** `track` records every |
| + request whose success the client did not see at once and marks a |
| + refusal uncertain; `settled` requires every tracked request done within |
| + the client's wait (`doneAt - at < uploadTimeout`), marks a timeout or a |
| + completion after the wait (a lost response) uncertain for good, and |
| + covers level-0, compaction, snapshot and retention alike; the pre-cut |
| + source certifies (`moving` is inside); the idle stop kills the cgroup |
| + and the close waits while any process lives. Witnesses |
| + `wMaintenanceRetry` and `wLostResponse`. |
| +- **Witnesses moved.** `wEmptyBootstrap` exercises the empty install |
| + through a move of the never-written incarnation (a push's seal carries |
| + its own mark and is never empty; the valid-ltx mutation now reaches the |
| + anchor `[0, 0]`); `restore-overlap`'s named failure is INV-3 (a restore |
| + short of the certificate's `max_txid` refuses to start, where rev 7.4's |
| + rule lost four writes); the admission scenario's named failure is |
| + INV-1 again; the whole-start-check witness is retired (with every |
| + restore from the box's own region, the stale source of a cross-region |
| + move finds nothing to restore; `expected-outcomes.txt`); |
| + `wGenerationConditional` holds the probe's marker publication; |
| + `wDirtyReturn` replicates the target's write so no declaration can |
| + cover it; `wRollbackJournal` and `wProbeRestart` read |
| + `holder.generation`. |
| +- **Model faults found and fixed this round** (all before the final |
| + numbers): a lagging marker refused every later start (the admitted |
| + writer's own unfinished start was not recognized); a cold admission |
| + restored an abandoned empty generation and lost the data (its parent is |
| + the baseline); the position-0 build of a never-replicated seal (the |
| + TXID-1 rule, rev 7.9) and an empty seal treated alike; the files tag |
| + checked against the marker refused probes after the admission retagged |
| + them; the purge fault, left on, starved a box for the whole calm phase |
| + (one-shot); a prepared generation opened twice (seeds 43 and 87 / 300); |
| + a target that never restored a database returned a spurious dirty seal |
| + that the source then restored, empty (seed 62 / 300); a descendant |
| + surviving the idle stop acknowledged writes the certificate did not |
| + cover and the next purge lost silently (seed 17 / 300); every close in |
| + `moving` was dropped and the pre-cut source churned generations (seed |
| + 62 / 300); the admitted writer waiting for its marker was resumed only |
| + by a wake (seed 5094 / 30,000); the landing's prepared generation got a |
| + second stamp and the probe was refused by its own record (seed 1117 / |
| + 30,000); the return's lagging marker (seed 9554 / 30,000); a compaction |
| + of a full input into a delta lost a deletion (seed 27371 / 30,000); a |
| + close that waited for an escaped descendant, and one that waited for a |
| + certificate PUT late by three horizons, held a revert's probe until it |
| + stuck (seed 97950 / 100,000: the close is refused, not delayed); a |
| + stalled probe step carried the stamp active at its read, before a cold |
| + admission's installing CAS, and the box's record refused its own probe |
| + (seed 67671 / 100,000: the resumed step re-reads its record with the |
| + claim). Under the new start, `strict-spawn` is caught alone by the sweep |
| + (a non-strict descendant surviving the idle stop acknowledges writes the |
| + purge then loses), so it leaves `expected-outcomes.txt`. |
| + |
| **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 |
| @@ -3180,7 +3369,32 @@ adds and one it makes stricter: |
| app is idle. Writes past the last completed checkpoint are lost by |
| design and declared so; every durable write must come back. |
| -**Rev 7.9, on the final model (claim rev 6.8 and 6.8.1: writer sessions, |
| +**Rev 7.10, on the final model (claim rev 6.9: no local database reuse, |
| +warm and cold only, writer_box and writes_lost, the admission bound to the |
| +operation, close evidence by client outcome): 30,000 seeds, zero |
| +violations; 100,000 seeds, zero violations** (84 s and 279 s). |
| +Across the 100,000 seeds: 149,973 completed operations, among them |
| +0 cold and 0 warm admissions (20,116 clean |
| +closes, 0 closes refused as uncertain, 0 |
| +stale certificates, 1,003 wakes that waited for a draining |
| +writer, 202,837 local databases purged, 0 starts |
| +refused by a failed purge, 57,938 writes_lost records declaring |
| +5,817 acknowledged writes lost, 25,140 full first |
| +uploads, 0 starts that waited for their marker, |
| +0 markers published again, 179 probes |
| +restarted), 1,433 completed moves, 1,715 clean and |
| +143 dirty rollbacks, 352 pre-flip reverts, |
| +305 declared losses, 25,627 pushes, 89,152 |
| +delete-park-free cycles and 6,234 lost disks (4,763 |
| +with a crash); 9,706 LTX compactions, 6,802 snapshot |
| +rotations, 581 level-0 upload retries, 30,362 |
| +anchors; 26,035 local stamp records lost and re-initialized; |
| +41,855 requests completed after `H`; 32,791 staging |
| +signatures refused as stale; 30,496 creates restarted on a 412. |
| +Every oracle left the system unchanged. The model faults the new rules |
| +exposed before these baselines are listed in §14.2.2. |
| + |
| +**Rev 7.9, on 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: |
| @@ -3397,37 +3611,64 @@ 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.9 model (bdd9d404; its Go files are dfc352ef's), with the strict classification, |
| +on the final rev 7.10 model (572066ec), 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 44 rules that have them. A rule is caught if |
| +same mutation, for the 45 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 **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). |
| +section does too. The model has **92 rules**: rev 7.9's 90 less |
| +`warm-provenance` (gone with the lineage, R9-1) plus `remote-baseline` |
| +(R9-1), `writes-lost` (R9-2) and `admit-bind-op` (R9-4). `mutate.sh 3000` |
| +exited 0: no ERROR, no unexpected MISSED, no STALE; every live |
| +combination was rerun this round. Seed numbers reproduce any sweep line |
| +with `HOSTLIFE_SEED`; `HOSTLIFE_WITNESS=<rule>` replays a witness with |
| +its trace. Rev 7.9's counts are in the rev 7.9 spec (831a2ea2); a restore |
| +at every wake changes what every start does, so sweep counts moved |
| +throughout. **Every table below is regenerated from the retained |
| +verdict files** (R9-6; `~/.cache/nearest-region/rev710-sweeps/`), none is |
| +carried over. |
| | | rules | |
| |---|---| |
| -| 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) | |
| +| caught alone by the sweep at 3,000 seeds | 65 | |
| +| caught alone by the sweep at 30,000, and by their witness | 4 (`evidence-whole-tree`, `orphan-order`, `restore-overlap`, `staging-quiet`) | |
| +| 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 | 7 (`close-evidence`, `close-waits`, `closed-marker`, `live-set-region`, `newest-l0`, `remote-baseline`, `restore-gap-closed`) | |
| +| caught only in a stated combination: the witness holds alone and under every proper subset, and violates with the partners | 9 | |
| +| subsumed: the witness holds under every combination tried, or the scenario is unreachable by construction | 3 (`door-reread`, `door-by-version`, by C3a and by writer epochs; `start-check`, by regional restores since rev 7.10; 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.10 moved.** The restore at every wake makes the random |
| +sweep reach what it could not before. `writer-session` is caught by the |
| +sweep (3 / 3,000, 18 / 30,000, 55 / 100,000; rev 7.9: once in 100,000), `admit-everywhere` everywhere |
| +(698 / 3,000, 6,691 / 30,000, 22,531 / 100,000: a stale source continuing the generation now collides at |
| +once), `recovery-generation` (11 / 3,000, 77 / 30,000, 266 / 100,000; rev 7.9: 0 at every depth), |
| +`rollback-journal` (1 / 3,000, 6 / 30,000), `lost-quarantine` (1 / 3,000, 6 / 30,000), |
| +`markers-last` (1 / 3,000, 7 / 30,000) and `timer-freeze` (3 / 3,000, 27 / 30,000). Of the three new |
| +rules, `writes-lost` is caught everywhere (13 / 3,000, 95 / 30,000, 318 / 100,000: a silent loss shows in |
| +the serving database at once), `remote-baseline` is witness-only |
| +(0 / 3,000, 0 / 30,000, 0 / 100,000: the stale cached copy with a matching certificate is a schedule |
| +the generator does not produce) and `admit-bind-op` is caught only with |
| +`claim-cas-opid` (the pair 0 / 30,000, 0 / 100,000, witness-only: the model's |
| +C2 already binds every CAS to `op.id`). `strict-spawn` is caught alone now |
| +(3 / 3,000, 24 / 30,000: a non-strict descendant surviving the idle stop acknowledges |
| +writes the next purge loses), so it leaves the combination-only list; |
| +`start-check` leaves the witnesses, subsumed by regional restores. The |
| +admission four 4 / 30,000, 20 / 100,000, the three box-side fences 0 / 30,000 with the |
| +witness held (`exec-writer` alone holds the scenario). Rev 7.8's |
| +remaining writer-epoch rules keep their shape: `closed-marker`, |
| +`close-waits` and `close-evidence` witness-only at every depth, |
| +`newest-l0` 0 / 3,000, 0 / 30,000, 0 / 100,000. Rev 7.7's rules hold their rates (`anchor-acked` |
| +12 / 3,000, 95 / 30,000, 346 / 100,000; `return-stamp` 73 / 3,000, 630 / 30,000, 2,161 / 100,000; `restore-anchor` 69 / 3,000, 627 / 30,000, 2,107 / 100,000; |
| +`root-advance` 19 / 3,000, 163 / 30,000, 489 / 100,000; `location-per-incarnation` 29 / 3,000, 357 / 30,000, 1,158 / 100,000). |
| +Twelve rules the sweep misses at 3,000 are caught by their witnesses, and |
| +the sweep's zeros for them say nothing against the hazards (R7-2's point |
| +stands). |
| + |
| **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` |
| @@ -3499,48 +3740,51 @@ 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 | | 26 / 3,000, 574 / 100,000 | |
| -| `lost-return-park` (model 27) | the target writes in the settle window, the settle check fails, the target is stopped after its first return PUT and declared lost | **violated**: INV-10, the lane in the source region at the release | | 1 / 3,000, 21 / 30,000, 68 / 100,000 | |
| -| `declare-lost-compute` (model 5) | the target is frozen in its settle window and its execution lease expires; the VM resumes once the source has recovered | **violated**: INV-1, two boxes run the host | | 0 / 3,000, 2 / 100,000 | |
| -| `watchdog-independent` (§7.1) | as above, with the agent alone paused, so the application keeps running | held | with `declare-lost-compute`: **violated**, INV-1 | 0 / 3,000; the pair 2 / 30,000, 6 / 100,000 | |
| -| `lost-quarantine` (CC12) | the target is stopped while landing, declared lost, and started again with its old disk | **violated**: INV-10, local state for a host served elsewhere | | 2 / 3,000, 14 / 30,000 | |
| -| `markers-last` (R2-6) | the source has a registered timer; the target's agent crashes between extracting the files and writing the marker | **violated**: INV-2, the timer is lost | | 0 / 3,000, 10 / 30,000 | |
| -| `rollback-journal` (R2-3) | a dirty rollback; the source's agent crashes after its probe spawned the instance, which wrote and replicated into the return generation | **violated**: INV-2 on cold restore | | 0 / 3,000, 0 / 30,000 | |
| -| `seal-by-version` (J-N2) | a pre-cut staging round completes after the seal; the source wrote and replicated between them | **violated**: INV-2 on cold restore; the landing installs the stale snapshot | | 1 / 3,000 | |
| +| `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 | | 22 / 3,000, 203 / 30,000, 624 / 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 | | 6 / 3,000, 47 / 30,000, 123 / 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, 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 / 3,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 | | 1 / 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 | | 1 / 3,000, 7 / 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 | | 1 / 3,000, 6 / 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 | | 2 / 3,000, 10 / 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, 3 / 30,000 | |
| -| `dirty-return` (INV-2) | the target writes during its probe and is rolled back | **violated**: INV-2, the write is lost | | 2 / 3,000 | |
| -| `commit-before-open` (INV-5; R3-5) | a public request reaches the target's edge while its probe runs | **violated**: INV-5 | | 3 / 3,000 | |
| -| `claim-cas-opid` (C2) | a stalled source goroutine with the rollback's last read resumes after a purge claimed the host | held | with `revalidate-before-effect`: **violated**, the store is torn down under a serving host | 0 / 3,000; the pair 897 / 30,000 | |
| -| `exec-admission`, `hold-op-open`, `start-check-claim-gen`, `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 | |
| -| `fence-by-installation` (claim rev 6.4 §6.4, R3-3) | UK→US, then US→UK; **unmutated, the instance must serve on UK again, running** | **violated**: the landing probe on UK is refused by the box's own installation record (INV-3) | | 484 / 3,000, 4,242 / 30,000 | |
| -| `fence-stamp` (claim rev 6.4 §6.4, R4-2) | a config-sync pass selects the row under the first installation and pauses; UK→US→UK; a new bundle is published; the pass takes the guard | held: the host guard's fresh re-validation refuses its stale bundle | with `hostguard`: **violated**, INV-6, a pass of a retired installation wrote host state | 351 / 3,000, 3,434 / 30,000; the pair 4,354 / 30,000 | |
| +| `dirty-return` (INV-2) | the target writes during its probe and is rolled back | **violated**: INV-2, the write is lost | | 1 / 3,000, 17 / 30,000 | |
| +| `commit-before-open` (INV-5; R3-5) | a public request reaches the target's edge while its probe runs | **violated**: INV-5 | | 12 / 3,000, 102 / 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 / 3,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-1 (the non-exec source is admitted cold into a fresh generation restored from its own region's old files and serves beside the target) | 0 / 3,000 | |
| +| `start-check` (INV-4) | the same, dropping the whole start check | retired in rev 7.10: with every restore from the box's own region, the stale source finds nothing of the target's generation to restore and cannot start; subsumed (`expected-outcomes.txt`) | | 0 | |
| +| `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 | 3 / 3,000, 24 / 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 / 3,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 | |
| +| `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) | | 442 / 3,000, 4,043 / 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 | 367 / 3,000, 3,564 / 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 | | 539 / 3,000 (the retention fixture, populated 2 to 33) | |
| -| `live-set-region` (claim rev 6.4 §6.2a, R4-3) | a legacy host serving in UK with an earlier replica in US; discovery parks US; an old US replication PUT lands after | **violated**: INV-10, residue the US sweep exempts by key alone | | 0 / 3,000, 0 / 30,000 | |
| -| `restore-overlap` (§5.1, R4-1) | a generation's snapshot ends at the push's TXID; the only continuation is a compacted file starting one below it; the disk is lost and the host wakes cold | **violated**: INV-2, the wake loses four acknowledged writes (rev 7.4's `min == current + 1` discards the file) | | 0 / 3,000, 3 / 30,000 | |
| -| `restore-gap-closed` (§5.1, R4-1) | the same generation with the next file missing and the one after current | **violated**: a restore across the gap returns a database short of the acknowledged writes | | 0 / 3,000, 0 / 30,000 | |
| -| `restore-anchor` (§5.1 step 7, R5-1) | a push installs a snapshot alone; the host wakes, writes three times, replicates, loses its disk and wakes cold | **violated**: INV-2, every write since the push is lost: replication restarted at TXID 1 below the snapshot and the planner skipped the files (facts R5-1a, b) | | 37 / 3,000, 374 / 30,000, 1,275 / 100,000 | |
| -| `root-advance` (§5.1 step 8, R5-3) | a push, then twelve replicated writes: four compactions, four snapshot rotations, retention expiring every file that continued from the pinned snapshot; the disk is lost | **violated**: INV-3, the host refuses to wake on a gap the retention made, while the newest snapshot holds every write (facts R5-3d, e) | | 101 / 3,000, 934 / 30,000, 3,367 / 100,000 | |
| -| `anchor-acked` (§5.1 step 7, R6-1) | a push installs a snapshot alone; the install's anchor PUT is held across forty attempted opens, then released; the host writes, replicates, loses its disk and wakes cold | **violated**: the host opened before its anchor was acknowledged; litestream's position would be 0 and the writes below the snapshot are lost on the cold restore (INV-2) | | 73 / 3,000, 794 / 30,000, 2,789 / 100,000 | |
| -| `return-stamp` (claim rev 6.5, R6-4) | a dirty rollback; the source's local stamp record is lost after the target's return; the return CAS writes the source installation's stamp back and the source re-initializes from it, installs under it and serves under its probe CAS's new stamp | **violated**: the source activates the target's stamp, issued for another box's installation (INV-6) | | 52 / 3,000, 518 / 30,000, 1,869 / 100,000 | |
| -| `recovery-generation` (claim rev 6.6 §6.4a, R7-1), three scenarios and a crash | writer A's upload `[N+1]` is held in flight, A dies with its disk, B wakes; (i) B replicates its own `[N+1]`, then A's lands; (ii) A's lands after B's position is initialized and before B's upload, so litestream's loop skips B's file; (iii) A's held write updated K, B durably updates K, A's lands; (iv) a clean stop drains, then the agent crashes before 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` | | 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 | |
| +| `sweep-namespace` (claim rev 6 §6.2a, R3-4) | a replication PUT of incarnation 1 completes after 33 recreates dropped it from `retired_incarnations` | **violated**: INV-10, residue the sweep never finds | | 542 / 3,000 | |
| +| `live-set-region` (claim rev 6.4 §6.2a, R4-3) | a legacy host serving in UK with an earlier replica in US; discovery parks US; an old US replication PUT lands after | **violated**: INV-10, residue the US sweep exempts by key alone | | witness; sweep 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-3 since rev 7.10, the restore stops short of the certificate's `max_txid` and the box never starts (rev 7.4's `min == current + 1` discarded the file and lost four writes) | | 0 / 3,000, 1 / 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 | | witness; sweep 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) | | 69 / 3,000, 627 / 30,000, 2,107 / 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) | | 19 / 3,000, 163 / 30,000, 489 / 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) | | 12 / 3,000, 95 / 30,000, 346 / 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) | | 73 / 3,000, 630 / 30,000, 2,161 / 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) | | 11 / 3,000, 77 / 30,000, 266 / 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) | | witness; sweep 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 | | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 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 | | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 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) | | 691 / 3,000 | |
| +| `evidence-whole-tree` (§6.1, J-D3) | an adopted legacy host runs a descendant outside the cgroup; the move cuts | **violated**: evidence blind to the escapee certifies the stop and two boxes run the host (INV-1) | | 0 / 3,000, 5 / 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` | | 3 / 3,000, 27 / 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` | | 42 / 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) | | 3 / 3,000, 18 / 30,000, 55 / 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 | | 698 / 3,000, 6,691 / 30,000, 22,531 / 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 / 3,000, 0 / 30,000 | |
| +| `valid-ltx` (R8-3) | a create's first wake into an empty generation (no LTX file), then a move of the never-written incarnation, whose seal is at position 0 | **violated**: the install writes `[1, 0]` and `[0, 0]`, which the encoder refuses (INV-12) | | 42 / 3,000, 402 / 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 | | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 | |
| +| `close-evidence` (R9-5), two more scenarios | (i) a compaction's level-1 PUT is held past the client's timeout, the next pass retries and lands, the original completes afterwards; (ii) a snapshot PUT completes on the server after the client gave up on it | **violated** in each: the certificate is written while a request of the session was retried after a timeout, or its response was lost | | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 | |
| +| `remote-baseline` (claim rev 6.9 §6.4a, R9-1) | a session closes cleanly through N+1; the box's local database is a cached copy through N; the next wake | **violated**: the stale copy is served without the acknowledged write, and its upload for N+1 is skipped at the remote position (INV-2) | | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 | |
| +| `writes-lost` (claim rev 6.9 §6.4a, R9-2) | a writer acknowledges a write and crashes before uploading it; the next wake is cold | **violated**: lost silently, the serving database differs from the acknowledged writes (INV-2); with the rule the admission records writes_lost and alerts | | 13 / 3,000, 95 / 30,000, 318 / 100,000 | |
| +| `admit-bind-op` (claim rev 6.9 §6.4a, R9-4) | a wake's admission closure computed under serving resumes after a delete began that kept session, generation and executor | held: the model's general CAS condition on `op.id` (C2) refuses it too | with `claim-cas-opid`: **violated**, INV-13, a writer admitted into a host being deleted | 0; the pair 0 / 30,000, 0 / 100,000 | |
| **The purge fence, the ETag condition and C5a.** `purge-claim-fence` |
| (CC21) is caught alone by the sweep: 28 / 3,000, 240 / 30,000. |
| @@ -3564,53 +3808,55 @@ 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: 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 ‡). |
| +**Caught alone: 77 of 92** (65 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 ††; 7 by their witness alone, marked ‡). |
| | rule | seeds failing | | rule | seeds failing | |
| |---|---|---|---|---| |
| -| `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 | |
| +| `abort-target-owner` | 933 / 3,000 | | `admission-registration` | 33 / 3,000 | |
| +| `admit-everywhere` | 698 / 3,000, 6,691 / 30,000, 22,531 / 100,000 | | `anchor-acked` | 12 / 3,000, 95 / 30,000, 346 / 100,000 | |
| +| `build-completion` | 691 / 3,000 | | `cancelled-creates` | 384 / 3,000 | |
| +| `claim-never-deleted` | 4 / 3,000, 57 / 30,000 | | `claim-op-exclusive` | 81 / 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); |
| +| `closed-marker` ‡ | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 | | `commit-before-open` | 12 / 3,000, 102 / 30,000 | |
| +| `cut-deadline` | 10 / 3,000 | | `declare-lost-compute` †† | 0 / 3,000, 0 / 30,000, 3 / 100,000 | |
| +| `dirty-return` | 1 / 3,000, 17 / 30,000 | | `evidence-from-state` | 2,612 / 3,000 | |
| +| `evidence-whole-tree` † | 0 / 3,000, 5 / 30,000 | | `fence-by-installation` | 442 / 3,000, 4,043 / 30,000 | |
| +| `fence-etag` | 28 / 3,000, 229 / 30,000 | | `fence-stamp` | 367 / 3,000, 3,564 / 30,000 | |
| +| `files-carried` | 33 / 3,000 | | `floor-boot-recovery` | 2,575 / 3,000 | |
| +| `fresh-admission` | 11 / 3,000 | | `fresh-incarnation` | 34 / 3,000 | |
| +| `generation-conditional` | 22 / 3,000, 203 / 30,000, 624 / 100,000 | | `hostguard` | 5 / 3,000 | |
| +| `legacy-discovery` | 357 / 3,000, 3,433 / 30,000 | | `live-set-region` ‡ | witness; sweep 0 / 3,000, 0 / 30,000 | |
| +| `location-per-incarnation` | 29 / 3,000, 357 / 30,000, 1,158 / 100,000 | | `lost-quarantine` | 1 / 3,000, 6 / 30,000 | |
| +| `lost-return-park` | 6 / 3,000, 47 / 30,000, 123 / 100,000 | | `markers-last` | 1 / 3,000, 7 / 30,000 | |
| +| `newest-l0` ‡ | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 | | `obligations-block-ops` | 23 / 3,000 | |
| +| `orphan-no-deadline` | 44 / 3,000 | | `orphan-order` † | 0 / 3,000, 1 / 30,000 | |
| +| `park-all-versions` | 567 / 3,000 | | `park-by-version` | 2,523 / 3,000 | |
| +| `park-skip-lock` | 2,728 / 3,000 | | `participant-rows` | 2 / 3,000 | |
| +| `purge-adopts` | 7 / 3,000 | | `purge-claim-fence` | 23 / 3,000, 230 / 30,000 | |
| +| `purge-journal` | 1,883 / 3,000 | | `purge-reserve-first` | 2,135 / 3,000 | |
| +| `quiet-before-ack` | 174 / 3,000 | | `recovery-current-inputs` | 42 / 3,000 | |
| +| `recovery-generation` | 11 / 3,000, 77 / 30,000, 266 / 100,000 | | `recovery-pass` | 2,488 / 3,000 | |
| +| `registration-recovery` | 2,117 / 3,000 | | `remote-baseline` ‡ | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 | |
| +| `restore-anchor` | 69 / 3,000, 627 / 30,000, 2,107 / 100,000 | | `restore-by-generation` | 140 / 3,000 | |
| +| `restore-gap-closed` ‡ | witness; sweep 0 / 3,000, 0 / 30,000 | | `restore-overlap` † | 0 / 3,000, 1 / 30,000 | |
| +| `retirement-ids` | 407 / 3,000 | | `return-stamp` | 73 / 3,000, 630 / 30,000, 2,161 / 100,000 | |
| +| `revalidate-before-effect` | 14 / 3,000, 149 / 30,000 | | `revert-journal` | 9 / 3,000 | |
| +| `rollback-journal` | 1 / 3,000, 6 / 30,000 | | `root-advance` | 19 / 3,000, 163 / 30,000, 489 / 100,000 | |
| +| `sdk-no-resign` | 15 / 3,000 | | `seal-by-version` | 2 / 3,000, 10 / 30,000 | |
| +| `sign-at-check` | 15 / 3,000 | | `sign-before-safeuntil` | 27 / 3,000 | |
| +| `source-readiness` | 10 / 3,000 | | `staging-quiet` † | 0 / 3,000, 3 / 30,000 | |
| +| `stale-hold-release` | 2 / 3,000 | | `straggler-sweep` | 757 / 3,000 | |
| +| `strict-spawn` | 3 / 3,000, 24 / 30,000 | | `sweep-namespace` | 542 / 3,000 | |
| +| `sweep-staging` | 31 / 3,000 | | `target-park` | 39 / 3,000 | |
| +| `timer-canonical` | 2 / 3,000 | | `timer-freeze` | 3 / 3,000, 27 / 30,000 | |
| +| `valid-ltx` | 42 / 3,000, 402 / 30,000 | | `writer-session` | 3 / 3,000, 18 / 30,000, 55 / 100,000 | |
| +| `writes-lost` | 13 / 3,000, 95 / 30,000, 318 / 100,000 | | | | |
| + |
| +**Caught only in a combination: 9 rules**, every live combination rerun this |
| +round; `admit-bind-op` joins with `claim-cas-opid` (R9-4); the `start-check` |
| +four is historical; |
| `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 |
| @@ -3621,18 +3867,19 @@ 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) | 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` + `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 | |
| +| `purge-claim-fence` + `fence-etag` (**the re-read alone**, rev 7's CC21 as proposed) | 339 / 30,000 | `purge-claim-fence` 23 / 3,000, 230 / 30,000, `fence-etag` 28 / 3,000, 229 / 30,000 | (the two `registration-check` rows below) | a store destroyed under a creating or serving host | |
| +| `registration-check` + `purge-claim-fence` | 268 / 30,000 | `registration-check` 0 / 3,000, `purge-claim-fence` 23 / 3,000, 230 / 30,000 | violated | the same | |
| +| `registration-check` + `fence-etag` | 268 / 30,000 | `registration-check` 0 / 3,000, `fence-etag` 28 / 3,000, 229 / 30,000 | violated | the same | |
| +| `exec-admission` + `hold-op-open` + `start-check-claim-gen` + `exec-writer` | 4 / 30,000, 20 / 100,000 | `exec-admission` 0 / 3,000, `hold-op-open` 0 / 3,000, `start-check-claim-gen` 0 / 3,000, `exec-writer` 0 / 3,000, 0 / 30,000 | violated, INV-1 | the non-exec source admitted cold beside the target, Astra's J2-R2-8 trace under writer sessions | |
| +| `exec-admission` + `hold-op-open` + `start-check` + `exec-writer` (**historical**, rev 7.9: 7 / 30,000, violated INV-6) | not rerun: the `start-check` witness is retired, subsumed by regional restores | | retired | the stale source cannot restore the target's generation from its own region | |
| +| `admit-bind-op` + `claim-cas-opid` | 0 / 30,000, 0 / 100,000 | `admit-bind-op` 0 / 3,000, 0 / 30,000, `claim-cas-opid` 0 / 3,000 | violated, INV-13 | a stale serving-time closure admits a writer into a host being deleted | |
| | `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 | |
| +| `claim-cas-opid` + `revalidate-before-effect` | 869 / 30,000 | `claim-cas-opid` 0 / 3,000, `revalidate-before-effect` 14 / 3,000, 149 / 30,000 | violated | a stale step destroys a store | |
| +| `strict-spawn` + `evidence-whole-tree` | 158 / 30,000 | `strict-spawn` 3 / 3,000, 24 / 30,000, `evidence-whole-tree` 0 / 3,000, 5 / 30,000 | violated | two writers | |
| +| `touched-incomplete` + `legacy-discovery` | 7,431 / 30,000 | `touched-incomplete` 0 / 3,000, `legacy-discovery` 357 / 3,000, 3,433 / 30,000 | violated | a freed host's residue | |
| +| `declare-lost-compute` + `watchdog-independent` | 0 / 30,000, 4 / 100,000 | `declare-lost-compute` 0 / 3,000, 0 / 30,000, 3 / 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,574 / 30,000 | `fence-stamp` 367 / 3,000, 3,564 / 30,000, `hostguard` 5 / 3,000 | violated | a stale pass writes host state for a retired installation (INV-6); the witness is what shows the stamp load-bearing against the guard's own check | |
| Every live combination was rerun on the rev 7.9 model; the gate runs |
| every proper subset of the admission four with the witness, which holds |
| @@ -3649,8 +3896,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; 49 witnesses, 182 runs); the 30,000- and 100,000-seed |
| -baselines, this sweep and the witnesses are the evidence for rev 7.9. |
| +a second; 52 witnesses, 176 runs); the 30,000- and 100,000-seed |
| +baselines, this sweep and the witnesses are the evidence for rev 7.10. |
| #### 14.2.6 What the model does not prove |
| @@ -4026,6 +4273,32 @@ 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.9 (f6180ae4), with rev 6.8.2's answers, after joint round |
| +9: no change requested, seven readings.** Rev 6.9 rewrites §6.4a under |
| +Paul's ruling to simplify: no local database reuse, warm and cold only, |
| +`holder.writer_box`, `writes_lost`, admission after readiness and before |
| +any upload, bound to the observed `op.id` and `op.phase`, and the |
| +`park-generation {region, generation}` chore; rev 6.8.2 lets any |
| +`op.exec` box continue on a certificate and requires the disk-lost |
| +source's admission to record `writes_lost`. Rev 7.10 encodes all of it |
| +(§5.1 step 9, §7.14, §14.2.2) and mirrors the library's names |
| +(`AdmitWriter(Admission{ObservedOpID, ObservedPhase, ObservedSession, |
| +ObservedGeneration, Box, Mode, NewGeneration, PredecessorCertified, |
| +RemoteMaxTXID})`, `Holder.WriterBox`, `Obligation.Generation`). The |
| +readings for platform-1e (`moves-claim-questions.md`, rev 7.10 heading): |
| +the predecessor to restore from is `holder.generation` unless it holds |
| +no file, when the nearest ancestor with files, the marker's generation, |
| +is the baseline; an operation's prepared generation is opened once by |
| +its probe's cold admission from its pinned snapshot in the box's own |
| +region and never re-entered; the landing's prepared generation keeps the |
| +flip's stamp while a push's and a dirty return's take a new one; a clean |
| +rollback's return CAS names the source's generation again; a move's |
| +landing records `writes_lost` for the source's uncertified session |
| +although the seal carries every write; the admitted writer's start |
| +(first upload, marker, anchor) is local bookkeeping driven by its own |
| +agent loop; and the model's C2 already binds every CAS to `op.id`, so |
| +the `admit-bind-op` witness needs both rules off. |
| + |
| **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`, |
| @@ -4398,6 +4671,24 @@ 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.16 Joint round 9 (claim a963d98d, moves rev 7.9 831a2ea2, model bdd9d404, library E a67d9f47) |
| + |
| +Round 9 judged the session certificate sound and found two P1s in local |
| +database reuse, three P2s and a P3. Paul ruled to simplify: a box never |
| +reuses its local database. Claim rev 6.9 (f6180ae4) rewrote §6.4a; the |
| +library E at fdff530f implements `AdmitWriter(Admission{...})`, |
| +`Holder.WriterBox` and `park-generation`. |
| + |
| +| finding | rev 7.10 | |
| +|---|---| |
| +| R9-1 (P1) a valid certificate admitted a stale local database; provenance was checked by cold recovery alone | gone by construction: every admitted writer purges the local database and restores the certified remote, warm or cold (§5.1 step 9, §7.14); lineage, provenance and `warm-provenance` removed; rule `remote-baseline`, witness `wStaleLocalAfterClose` (the clean-close variant, §14.2.5) | |
| +| R9-2 (P1) operation replacement lost the predecessor writer's identity; the model inferred it from `op.exec` | `holder.writer_box`, set by every admission, survives the operation; `writes_lost {box: observed writer_box, generation, session, remote_max_txid}` recorded and alerted at every uncertified cold admission; rule `writes-lost`, witness `wSilentLoss` | |
| +| R9-3 (P2) the admission protocol (open, fresh, probe recovery advancing an installation generation, park-generation, ordering) could not be implemented through E | only warm and cold; `holder.generation` the only authoritative generation; a probe opens the prepared generation by cold admission; a first install is cold into an empty generation; a failed cold start leaves an empty generation to the sweep; `park-generation {region, generation}`; admission after readiness, before any upload (§7.14's phase table and start sequence) | |
| +| R9-4 (P2) the admission was not bound to the operation whose evidence justified it | bound to the observed `op.id`, `op.phase` and kind; refused in deleting, parking, purging, creating; INV-13; rule `admit-bind-op`, witness `wStaleClosureDelete` with `claim-cas-opid` | |
| +| R9-5 (P2) maintenance timeouts and client outcomes missing from close eligibility | client-observed success for every request class, a sticky uncertainty for a timeout, a refusal or a lost response (§5.1 step 9); witnesses `wMaintenanceRetry`, `wLostResponse` | |
| +| R9-6 (P3) the combination table carried earlier counts; 8 against 10 combination-only rules | every table regenerated from the retained verdict files; the counts follow the classification (§14.2.5) | |
| +| the readings judged | "allow otherwise" resolved by 6.8.2 (any `op.exec` box); admission after readiness kept, with the cold reservation gone (the CAS is the only claim write of a start); the disk-lost source's admission records `writes_lost` (6.8.2) | |
| + |
| ### 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 |