amadan
spec: move-any-app rev 7.11: joint round 10, the admitting CAS before the start (claim rev 6.10), every number rerun (#175)
Answers CODEX-FINDINGS-JOINT-R10 (R10-1 to R10-9) against claim rev 6.10 (3f916b05) with rev 6.9.1's answers. The admitting CAS comes first; a session belongs to the agent process; failed starts follow a retry policy (five attempts, a doubling backoff, then the host is marked failed); a cold admission's generation is unfinished until the marker names it, its predecessor stays live, the marker's publication queues the retire chores, a lagging marker is read through the writers journal (a chain of unfinished admissions is normal, anything else alerts), the journal survives a release; §7.5, §7.6, §7.8 and §7.9 rewritten around §7.14 (no claim transition moves holder.generation but a cold admission); the admission is shaped like E's (KeepStamp, BaselineCoversPredecessor, the five refused kinds, warm with an empty NewGeneration, session:<n> chores, @root); faults exempt nothing (INV-14, INV-15); startup PUTs are session evidence; the budget prices a restore per probe attempt (2 GiB: 117.9 s, one attempt; 2.5 GiB refused); structured counters. Beyond the review: a rollback is clean only when the seal recorded src_covered (seal-return), a seal from the remote does not cover the predecessor (from_db), a restarted agent stops a running app, a declared-lost target's rollback declares the source's cut session. Results on model bd1587a1: 30,000 and 100,000 seeds clean; 95 rules, 82 caught alone (65 at 3,000, 8 at 30,000, 3 at 100,000, 6 by witness), 8 combination-only, 2 subsumed, 2 liveness, 1 unreachable; every table regenerated from the retained verdicts. §22.17 has every disposition; §19.4 the eight notes for platform-1e.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
1 file changed,
+743
−199
docs/superpowers/specs/2026-10-02-move-any-app-design.md+743 −199
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 97fc68f9b..77079268c 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,62 @@ |
| # Move any app or instance to another region: Phase 1, a safe single-instance move |
| -**Date:** 2026-10-04 |
| -**Revision:** 7.10. |
| +**Date:** 2026-10-05 |
| +**Revision:** 7.11. |
| + |
| +- **Rev 7.11** answers **joint round 10** (`CODEX-FINDINGS-JOINT-R10.md`, |
| + cited "R10-n") and is written against **claim spec rev 6.10** |
| + (3f916b05, with rev 6.9.1's answers to rev 7.10's readings); §22.17 |
| + has every disposition. **The admitting CAS comes first** (R10-1): before |
| + the purge, the restore, the app start and readiness, so nothing the app |
| + acknowledges is ever outside a writer session; a session belongs to the |
| + **agent's replicator**, app restarts under the same agent stay in it, a |
| + new agent process is a new session and stops a running app it finds; |
| + failed starts are governed by a **retry policy** (five attempts under |
| + one session with a doubling backoff from one step, then the host is |
| + marked failed and gets no new session until an operator clears it). |
| + **A cold admission's generation is unfinished until `generation.json` |
| + names it** (R10-2): its journalled predecessor stays live, no chore |
| + retires it, and the sweep never parks it; the retire chores are queued |
| + by the marker's publication; a marker lagging behind |
| + `holder.generation` that names the predecessor of the latest admission, |
| + or of a chain of unfinished ones, is the normal state and no alert, any |
| + other disagreement leaves the location untouched and alerts. |
| + **§7.5, §7.6, §7.8 and §7.9 are rewritten around §7.14's protocol** |
| + (R10-3): the commit and the `probed` CASes move no generation; |
| + `holder.generation` is always the latest admission's. The admission is |
| + **API-shaped like the library's `Admission`** (R10-4): `KeepStamp` only |
| + when `holder.stamp > holder.session`, warm with an empty |
| + `NewGeneration`, refused in `creating`, `deleting`, `parking`, |
| + `purging` and `placing`, `BaselineCoversPredecessor` for a seal that |
| + covers the stopped predecessor (compared against the seal's own |
| + position; the journal says `baseline: sealed`, no `writes_lost`), the |
| + empty-generation ancestor restore only for the latest journalled |
| + unfinished admission. Serving-time chores use `op = "session:<n>"` and |
| + an adopted host's root generation is `"@root"` (R10-5). **Disk-loss |
| + faults exempt nothing** (R10-6): every exemption comes from a durable |
| + `writes_lost` declaration, alert delivery is checked separately |
| + (INV-14), timers are never exempted by the database rule, and a write |
| + the remote holds is never declared lost while its writer's box is with |
| + us (INV-15). **Startup PUTs are session evidence** (R10-7): the first |
| + upload and the anchor enter the ledger, a retry after the client's wait |
| + makes the session uncertain for good, server completion and client |
| + response are distinct, and the bytes of a retry are the original's. |
| + **The budget prices the new protocol** (R10-8): a restore per probe |
| + attempt, the admission's overhead, a fresh generation's full upload on a |
| + retried probe; the 2 GiB example runs to 117.9 s and admits one attempt, |
| + the review's 2.5 GiB is refused at 131.2 s; the replication interval is |
| + the normal window a failed upload extends. **Counters are structured** |
| + (R10-9): the baseline logs `COUNTERS {json}`, the generator fails on a |
| + missing field, §14.2.3 and the change note are regenerated. Two gaps the |
| + rerun found beyond the review: a rollback is **clean only when the |
| + source's own replica covered its stopped database** at the seal, else |
| + the return carries the seal, whether or not the target wrote (§7.8, |
| + rule `seal-return`, INV-15); and a pre-flip round never forces a sync on |
| + a session whose start is unfinished. Rules `admit-before-start`, |
| + `baseline-live`, `seal-return` (95 in all); witnesses for the |
| + acknowledgement before admission, the parked baseline, the first-upload |
| + and anchor retries and the uncovered return (57 in all). Results in |
| + §14.2.3 and §14.2.5. |
| - **Rev 7.10** answers **joint round 9** (`CODEX-FINDINGS-JOINT-R9.md`, |
| cited "R9-n") under Paul's ruling to **simplify**, and is written |
| @@ -924,8 +979,9 @@ fails there first (§14.2.6). |
| 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, 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 |
| + admitted before its app starts, and a box never reuses its local |
| + database (claim rev 6.10 §6.4a; R7-1, R8-1 to R8-5, R9-1 to R9-5, |
| + R10-1 to R10-7).** 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 |
| @@ -938,29 +994,66 @@ fails there first (§14.2.6). |
| `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, |
| + - **`AdmitWriter`, one claim CAS before the app process starts** |
| + (claim rev 6.10, R10-1; this reverses rev 6.8.2's order, which let |
| + an app acknowledge work before it had a session: a background worker |
| + committed and acknowledged, the app crashed before readiness, the |
| + old certificate still stood and the next warm admission purged the |
| + acknowledgement silently). The order is: the CAS; the purge and the |
| + restore of the baseline; the app start; readiness; uploads. A |
| + **session belongs to the agent's replicator**, not to the app |
| + process: an app that crashes or restarts while the same agent keeps |
| + replicating stays within the admitted session and is not re-admitted; |
| + **a new agent process is always a new session**, so an agent that |
| + restarts under a running app stops it (the replicator that was |
| + admitted died with the old agent) and its next wake is a new |
| + admission, which declares what the app acknowledged meanwhile. |
| + `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. |
| + PredecessorCertified, RemoteMaxTXID, KeepStamp, |
| + BaselineCoversPredecessor})` (R10-4), and this spec's model is shaped |
| + like it. 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 **`creating`, `deleting`, |
| + `parking`, `purging` and `placing`** (R9-4, R10-4): a create's first |
| + writer is admitted after `CompleteCreate`, under `serving`, and |
| + nothing writes while a placement runs. After a conflict the box |
| + re-establishes its evidence, the certificate, 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, |
| + baseline, 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; and the release of |
| + an operation to `serving` carries the writers journal over, so an |
| + admission whose start is unfinished at the release stays explained |
| + (below). |
| + - **Failed starts are governed by a retry policy, never by another |
| + admission** (R10-1). Within the admitted session the agent retries |
| + the app start with a doubling backoff from one step (1, 2, 4, 8, 16 |
| + steps in the model; seconds in production) up to **five attempts**; |
| + a start the environment is not ready for (config not rendered, the |
| + release not live) waits and counts no attempt. At the fifth failure |
| + the box marks the host **failed**, abandons the session's start, and |
| + creates no new session for the host until an operator clears it (or |
| + a health signal does; the model's operator clears it after half a |
| + horizon). An operation whose probe is the failed host rolls back |
| + ("target would not start") or counts one failed try. Five attempts |
| + because the start's own faults (a missing key, a bad bundle) do not |
| + heal within the window and a crash loop would otherwise churn |
| + generations; the backoff keeps five attempts within half a minute. |
| + An app's writes are never left in an interval without an admitted |
| + session: there is no app before the CAS, and the session stands until |
| + the next CAS. |
| - **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 |
| @@ -992,17 +1085,37 @@ fails there first (§14.2.6). |
| 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`. |
| + dead writer's uploads may still land in it); or a **fresh** id; warm |
| + passes an **empty** `NewGeneration` (R10-4). 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 app started and before the |
| + marker; the bytes are captured once and a retry carries the same |
| + bytes (R10-7). When the observed session had no certificate and the |
| + baseline does not cover the predecessor's last acknowledged position, |
| + 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. When the baseline is a **seal |
| + that covers the stopped predecessor** (a landing's, a push's, a |
| + return's prepared generation, built from the stopped database's |
| + every page), there is nothing to declare and the entry says |
| + `baseline: sealed` (`BaselineCoversPredecessor`, claim rev 6.9.1); |
| + the comparison is against the seal's own position, never a TXID from |
| + another region. A seal built from the **remote** because the disk |
| + was gone (`seal.from_db` false, §7.4) stops at the remote's |
| + position and covers nothing beyond it: the prepared generation's |
| + admission records `writes_lost` for the predecessor's acknowledged |
| + writes past it, as a cold admission from the remote would. The box is never inferred from `op.exec`. A write the |
| + host's remote holds, in any generation, is never declared lost while |
| + its writer's box is with us (INV-15): the lineage adopts the |
| + generation that holds it, a dirty return's lane, instead; a box |
| + declared lost may leave such writes behind, and so may a rollback |
| + whose target was declared lost (no return lane runs; the seal in the |
| + target's region is unreadable from the source); the record's |
| + `remote_max_txid` names where an operator finds them (§7.10). |
| - **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, |
| @@ -1012,18 +1125,64 @@ fails there first (§14.2.6). |
| `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>`. |
| + cold admission issues a new `holder.stamp` **except** when no writer |
| + was admitted since the current stamp was issued (`holder.stamp > |
| + holder.session`, the library's `KeepStamp`, claim rev 6.9.1): a |
| + landing's first probe after the flip keeps the stamp the flip issued |
| + and the target's record activated; a restarted probe, a push and a |
| + dirty return take a new one. |
| + - **A cold admission's generation is unfinished until `generation.json` |
| + names it** (claim rev 6.10, R10-2). Until then its baseline, the |
| + journalled predecessor, is part of the live set: no `park-generation` |
| + chore for it may be queued and the sweep never parks it (rev 7.10 |
| + queued the chore at the CAS, so a writer that died before its first |
| + upload could have its only baseline archived under it). The chores |
| + that retire superseded generations are queued by the **marker's |
| + publication**, one per dead generation (`QueueGenerationRetire` in |
| + the library): the predecessor; behind a lagging marker, every empty |
| + generation of the chain of unfinished admissions between the marker's |
| + generation and the new one, and the marker's; and the predecessor of |
| + any earlier cold admission of this operation whose journal entry |
| + shows no chore was queued (its writer died after its marker landed |
| + and before the chore CAS; the journal marks entries whose |
| + predecessor is covered). A chore queued while the claim is `serving` |
| + has `op = "session:<holder.session>"`; an adopted legacy host's |
| + generation is the location root itself, named by the sentinel |
| + **`"@root"`** so a chore can name it, `holder.generation` is `""` |
| + for such a host until its first cold admission, and the adoption |
| + writes `holder.writer_box` as the box running the pre-release |
| + process, so the first cold admission's `writes_lost` names the |
| + writer whose unuploaded writes it leaves behind (R10-5). A failed |
| + cold start leaves an empty, unpublished generation; the next |
| + attempt is cold again and the marker it publishes retires it. |
| + - **A marker that lags `holder.generation`** is read through the |
| + writers journal: when it names the predecessor of the latest |
| + admission, or the predecessor of a chain of admissions each of which |
| + died before its marker (two in a row happen: the second's purge |
| + failed after its CAS), that is the normal unfinished state, every |
| + generation of the chain and the marker's is live, and there is no |
| + alert; the baseline for the next admission is the nearest generation |
| + of the chain that holds an object, else the marker's; an empty |
| + `holder.generation` for any other reason is unexplained missing data: |
| + refuse the start and alert. A `holder.generation` that holds objects |
| + has its marker published again (from the operation's build journal |
| + for a prepared generation, rooted at `[1, 1]` otherwise) and the |
| + chores queued, before anything else. Any other disagreement between |
| + the marker and the claim leaves the location untouched and alerts |
| + (§6.4). |
| - **A clean close is a one-use certificate.** A writer session |
| stopping cleanly first waits until **every request it issued over |
| 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 |
| + wait** (R8-5, R9-5, R10-7): every level-0 upload, every compaction |
| + and snapshot upload, every retention delete, **and the start's own |
| + PUTs**, the fresh generation's first upload and a warm restore's |
| + anchor, which enter the same ledger. 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 |
| + make the session **uncertain for good**; server completion and the |
| + client's response are distinct, and only the latter advances the |
| + start. A session whose start has not opened replication, or whose |
| + replicator died with its agent, certifies nothing. 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 |
| @@ -1066,11 +1225,19 @@ fails there first (§14.2.6). |
| 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. |
| + its original stays unresolved, a maintenance retry, a lost response, a |
| + first-upload retry and an anchor retry write no certificate; a |
| + background acknowledgement right after the start, then a crash, is |
| + declared by the next admission (under rev 6.8.2's order it is purged |
| + silently); a crash before the first upload leaves the predecessor live |
| + until the marker names the new generation (with the chore at the CAS |
| + the predecessor is parked and the recovery restores nothing); a |
| + rollback whose source replica stopped short of the stopped database |
| + returns the seal. 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, a restore per probe attempt, and a dead generation |
| + to park. |
| So: |
| @@ -1548,7 +1715,13 @@ the sweep never parks or deletes an object version in the live set, never |
| touches the version `generation.json` names, never treats the marker as |
| residue, reads the live set under the same fresh claim observation it |
| uses for everything else, and touches nothing in a location whose marker |
| -disagrees with `holder.generation`, raising an alert instead. The model |
| +disagrees with `holder.generation`, raising an alert instead, **except** |
| +for the one disagreement that is normal (claim rev 6.10, R10-2): a marker |
| +that names the journalled predecessor of the latest admission, or of a |
| +chain of admissions each of which died before its marker, while |
| +`holder.generation` is ahead of it; then every generation of the chain |
| +and the marker's are live, protected, and no alert is raised (§5.1 step |
| +9). The model |
| keeps the real cap and shows a replication PUT of an incarnation 33 |
| recreates old landing after the list forgot it (`sweep-namespace`), and |
| an old US PUT for a legacy host serving in UK parked only when the live |
| @@ -1730,7 +1903,7 @@ placement, the target writes `moves/<acct>/<app>/<host>/<move id>/target.json`: |
| | T9 claim | the claim is `moving` with this move id, its holder is the record's incarnation, and this region and box are in `touched` (added by CAS before the first staging write, claim spec §2) | |
| | T10 return lane | this box can put and delete `moves/_lane/<move id>` in the source's bucket (M17) | |
| | T12 quiet region | the claim's `quiet_after` for the target region (CC1) has passed, so the landing's park of an earlier stay never waits inside the cut window. A move back into a region the instance left within H waits at `ready`, not mid-cut. **Defence in depth (model, rev 5):** under claim rev 3 no state reaches it, because every retirement acknowledges only after its own horizon and CC11 refuses a move over a pending chore; the model drops T12 and no cut ever waits (§14.2.5). It stays, because it costs one comparison and guards any future path that acknowledges early | |
| -| T11 budget | the **whole** stop-to-open estimate fits the operator's cut window (default 120 s) (codex R2-10, M11), from three measured rates, the **cross-region copy path**, **regional S3** (reads and writes from a box in the bucket's region) and the box's **disk**: stop + final checkpoint and `SyncAndWait` + final mirror (at most the 16 MiB bar at the cross-region rate) + archive build and upload + **the target's build (§7.6 `building`, R5-5, R6-3): the restore of the staged replica (the whole database read from regional S3 and written to disk), the snapshot write and the anchor write (each the whole database read from disk and written to regional S3)** + **the verification of the built database (§7.6 `restored`: one disk read for its sha256)** + render + **the probe attempts the window permits, each with its own settle** + the open (`open_budget`, 5 s) (joint N15, J2-N15). Rev 7.5 made the sealed transfer a snapshot of the stopped database and still priced the cross-region copy at the 16 MiB bar: a 2 GiB database over a 10 MiB/s path needs about 205 s for that copy alone, so T11 admitted a move the deadline then rolled back (R5-5). Rev 7.6 built the snapshot on the target and priced three passes at one local rate, then restored the generation cold a fourth time in `restored` without pricing it: the review's 3 GiB at 200 MiB/s with one probe came to 108.68 s priced and 124.04 s run (R6-3). Rev 7.7 verifies the built database instead of restoring it again and prices every byte moved. **The worked example**, the same in this spec, the change note and `budget_test.go`: 2 GiB at 10 MiB/s across regions, 250 MiB/s to regional S3, 500 MiB/s on disk gives 53.6 s of fixed costs (restore 12.3, snapshot 12.3, anchor 12.3, verify 4.1, the rest 12.6) and admits **one** attempt; the cross-region snapshot transfer (204.8 s) is refused by the same arithmetic, and so is the review's 3 GiB workload at 200 MiB/s (rev 7.6's arithmetic admitted it). **The permitted attempts depend on the budget (R3-7):** `attempts = min(3, floor((window − everything else) / (30 s + 20 s)))`, and the instance is eligible only if that is at least one; the probe loop (§7.7) runs at most that many. Rev 7.3 required all three attempts to fit, 150 s of probing against a 120 s default window, so no default move was ever eligible; `budget_test.go` (§14.2) states the arithmetic and shows a tiny instance admitted with two attempts, the boundary at 70 s of fixed costs, and never more than three. The estimate is recorded per phase as `cut_budget_s`, and admission sets an absolute `cut_deadline` (§7.4) | |
| +| T11 budget | the **whole** stop-to-open estimate fits the operator's cut window (default 120 s) (codex R2-10, M11), from three measured rates, the **cross-region copy path**, **regional S3** (reads and writes from a box in the bucket's region) and the box's **disk**: stop + final checkpoint and `SyncAndWait` + final mirror (at most the 16 MiB bar at the cross-region rate) + archive build and upload + **the target's build (§7.6 `building`, R5-5, R6-3): the restore of the staged replica (the whole database read from regional S3 and written to disk), the snapshot write and the anchor write (each the whole database read from disk and written to regional S3)** + **the verification of the built database (§7.6 `restored`: one disk read for its sha256)** + render + **the probe attempts the window permits, each with its own settle** + the open (`open_budget`, 5 s) (joint N15, J2-N15). Rev 7.5 made the sealed transfer a snapshot of the stopped database and still priced the cross-region copy at the 16 MiB bar: a 2 GiB database over a 10 MiB/s path needs about 205 s for that copy alone, so T11 admitted a move the deadline then rolled back (R5-5). Rev 7.6 built the snapshot on the target and priced three passes at one local rate, then restored the generation cold a fourth time in `restored` without pricing it: the review's 3 GiB at 200 MiB/s with one probe came to 108.68 s priced and 124.04 s run (R6-3). Rev 7.7 verifies the built database instead of restoring it again and prices every byte moved. **Rev 7.11 prices the probe's own protocol (R10-8):** every probe attempt is a cold admission that purges the built database and **restores the prepared generation again** before the app starts (one regional S3 read and one disk write of the whole database), plus the admission's overhead (the CAS, the purge, `generation.json`: 2 s), the probe and its settle; every attempt after the first is a **fresh generation** whose first upload is the whole database again (one disk read and one regional S3 write). Rev 7.10 priced the previous protocol, three build passes, a verification and the probe alone, so the review's 2.5 GiB at the example rates was admitted at 113.8 s against the 120 s window and would have run to 131.2 s (129.2 s before the admission's overhead). **The worked example**, the same in this spec, the change note and `budget_test.go`: 2 GiB at 10 MiB/s across regions, 250 MiB/s to regional S3, 500 MiB/s on disk gives 53.6 s of fixed costs (restore 12.3, snapshot 12.3, anchor 12.3, verify 4.1, the rest 12.6), a first attempt of 64.3 s (restore 12.3, admission 2, probe 30, settle 20), 117.9 s in all, and admits **one** attempt by 2.1 s; a second attempt would add 76.6 s; the cross-region snapshot transfer (204.8 s) is refused by the same arithmetic, so is the review's 3 GiB workload at 200 MiB/s (rev 7.6's arithmetic admitted it), and so is 2.5 GiB. **The permitted attempts depend on the budget (R3-7):** the attempts admitted are those whose summed costs fit the window after the fixed costs, `attempt(1) = restore + admission + 30 s + 20 s`, `attempt(i > 1) = attempt(1) + full upload`, at most three, and the instance is eligible only if that is at least one; the probe loop (§7.7) runs at most that many. Rev 7.3 required all three attempts to fit, 150 s of probing against a 120 s default window, so no default move was ever eligible; `budget_test.go` (§14.2) states the arithmetic and shows a tiny instance admitted with two attempts, the boundary at 70 s of fixed costs, and never more than three. The estimate is recorded per phase as `cut_budget_s`, and admission sets an absolute `cut_deadline` (§7.4) | |
| **Source readiness.** S1: a probe request (§7.7) to the readiness path on |
| the instance as it runs today answers 200 to 399 from its own process |
| @@ -1754,7 +1927,7 @@ Each phase is written to `cut_phase` before its side effects. |
| | `admitted` | source CAS, stamping `cut_at` | **only if** the report and source readiness are fresh **and** every pinned input version (`move.inputs`) still matches the current bundle etags, overlay etag, release and launch report; otherwise CAS back to `ready` so the checks rerun (codex R2-8) | abort is legal until `admitted` and refused after; both CAS the same field | |
| | `stopping` | source | row `moving`, `hold_op = move id`; `ReconstructStopEvidence` (§5.3) | its budget, then `reverting` | |
| | `stopped` | source | final checkpoint and `SyncAndWait`, so the replica holds every acknowledged transaction; record the **required final TXID** `N`, the `MaxTXID` of the newest level-0 file (§5.1 step 1); read `Replication` and `NextDue`; snapshot the timers rows to `move-snapshots/<host>/<move id>/timers.json` **and** `…/timers/` in staging; write `stopped-source.json` with `N`; CAS the claim's execution holder to `none` (§19 K3) | | |
| -| `staged` | source | byte-final mirror round into `replica/`, within the bar; the **seal**: `N` and the `versionId` of every current LTX file under `replica/`, of `files/…` and `timers/…`, in the op journal (§7.3) | 3 deferred rounds or its budget: `reverting` | |
| +| `staged` | source | byte-final mirror round into `replica/`, within the bar; the **seal**: `N` and the `versionId` of every current LTX file under `replica/`, of `files/…` and `timers/…`, in the op journal (§7.3), **and `src_covered`** (rev 7.11): whether the source's own replica of `holder.generation` reached the stopped database's position with no pending write, which decides a rollback's clean return (§7.8); **and `from_db`**: whether the seal was built from the stopped database itself, which decides whether the landing's admission has anything to declare (§5.1 step 9). A round never forces a sync on a session whose start has not opened replication (§7.14): it mirrors the remote as it stands | 3 deferred rounds or its budget: `reverting` | |
| | `archived` | source | build the final archive from the stopped directory, seal, write create-only to `move-snapshots/`, record both digests, copy into `files/` | over the cap, a special file, or its budget: `reverting` | |
| | `flipped` | source, the flip CAS | `region = to`, `state = landing`, `landing_deadline`; and the claim: `op.kind = landing`, execution holder = target (§19 K4) | | |
| @@ -1815,8 +1988,8 @@ phase, and its new kind, phase and execution holder: |
| | record transition | claim CAS that follows | execution holder | |
| |---|---|---| |
| | `flipped` | `moving`/`sealed` → `landing`, `landing_phase = checking` | `none` → target, citing the source's evidence (`stopped-source.json`) | |
| -| `committed` | `landing` → phase `committed`, `holder.generation = move id`, plus the obligations of §7.9 | unchanged (target) | |
| -| `rolling_back` | `landing` → `restoring` under the same op id, `rollback.id` from the record | unchanged until the target's evidence (§7.8) | |
| +| `committed` | `landing` → phase `committed`, plus the obligations of §7.9; **`holder.generation` is not touched**: it is the generation the latest admission chose, the target's probe (§7.14), and a commit that wrote the prepared generation back would put an obsolete one into authority after a restarted probe (R10-3) | unchanged (target) | |
| +| `rolling_back` | `landing` → `restoring` under the same op id, `rollback.id` from the record; `holder.generation` untouched here too | unchanged until the target's evidence (§7.8) | |
| **Any actor that reads both objects and sees the record ahead writes the |
| claim half**: the actor that wrote the record, on its next step; the other |
| @@ -1862,7 +2035,7 @@ journaled in `<DataDir>/.moves/<host>/<move id>/` (F12). |
| | `checking` | read `stopped-source.json`; require the claim's `op.kind = landing` with this move id and execution holder = this box; require this box in `touched.boxes` (CAS-add before any local write); read `move.json` and require its incarnation; under the host guard, from that fresh read, set the local record's `active_stamp = holder.stamp`, the stamp the flip CAS wrote (claim rev 6.5 §6.4, §6.4 here); acquire the lease on `instances/<host>/` in its own bucket (claim spec C3) and hold it through `published` | | replayable | |
| | `parking` | bucket-park whatever is at `holder.location` in its own bucket into `superseded/<move id>/<host>/` (an earlier stay of this incarnation) | the park manifest exists **and** its deletion set is deleted | replayable by the claim's rule (manifest present: replay the deletion set) | |
| | `building` | **build the generation from the staged replica** (§5.1 step 2, R5-5): restore the sealed versions under `replica/` with the planner into the generation's database file, verifying each file's CRC-64 trailer, requiring exactly `N` and `PRAGMA integrity_check`; write the **snapshot** `[1, N]` to `<location>g-<move id>/0009/<1>-<N>.ltx` and the **anchor** `[N, N]` to `<location>g-<move id>/0000/<N>-<N>.ltx` (§5.1 step 7); in this order (R7-4, §5.1 step 2): **the build intent** `<location>g-<move id>/build-intent.json` with the encoding inputs (the header timestamp, page size, commit, `N`), before any PUT; the snapshot PUT, acknowledged; the anchor PUT, acknowledged; then **the completed install manifest** `<location>g-<move id>/install.json` with the snapshot's key, the `versionId` each PUT returned, `N`, each CRC-64, `integrity_check`'s result and the sha256 of the database file the build produced (R4-1, R5-1, R5-2, R6-5) | the **completed** install manifest exists; the intent alone is not completion | replayable at every boundary: staging is immutable after the flip, the generation is new, and the build never deletes. A replay reads the intent, encodes identical bytes, and reuses a snapshot or anchor it finds current under its key; a crash after the intent, after either PUT, or before the manifest leaves no completion, so `published` never runs; a PUT that completes late lands in this generation again as another version of identical bytes, which nothing reads (§5.1). The model journals the same states (`install-copy`, `install-anchor`, `published`) and refuses, as INV-11, a `generation.json` naming a snapshot or anchor that has not landed | |
| -| `published` | write `<location>generation.json` with op, incarnation, the install manifest's sha256 and the snapshot identity: `snapshot_key`, `snapshot_version`, `snapshot_txid`, `snapshot_crc64` (§5.1) | `generation.json` names this move | replayable | |
| +| `published` | the build is complete and recorded; **`generation.json` is not written here** (R10-3; rev 7.9 wrote it): the probe's cold admission publishes it, with op, incarnation, the install manifest's sha256 and the snapshot identity (`snapshot_key`, `snapshot_version`, `snapshot_txid`, `snapshot_crc64`, §5.1), after its CAS and before replication opens (§7.14) | the journal records the phase | replayable | |
| | `local` | `retire-artifacts` (claim rev 6.5 §6.4, §6.4 here: never `retire-installation`, which would retire the stamp `checking` activated) any warm database (with `<dbPath>.gen`), files directory and `<host>.env` of an earlier stay into `.parked/superseded-<move id>/`; extract the archive's files; write `<host>.env` from the archive; `ReplaceTimers` from the snapshot (§9.4); set `Replication` and `NextDue`; remove the host's restore-verification entry (§6.3); fsync all; **then** write `.files-gen` | `.files-gen` names this op and incarnation, and the journal records each sub-step | each sub-step is idempotent and journaled; `.files-gen` is written last, so its presence vouches for all of them (codex R2-6) | |
| | `configured` | render through §9.1 and materialize through §9.2; **for a forward install (this landing, a push)** the move-bound ack's bundle etags must equal `move.inputs` | ack matches | replayable; a mismatch is a rollback ("configuration changed during the move"), and the source's recovery then runs on the new bundle (§7.7, J2-R2-5). **A recovery install (§7.8) runs this phase on current inputs and records them; it is never gated on `move.inputs`** (R2-5) | |
| | `restored` | **verify the database `building` produced** (R6-3): its sha256 equals the manifest's, `CheckDB` (`backend_exec.go:313`) passes, and `<dbPath>.gen` is written naming this generation and location; record `landing.installed_db_sha256`. No second cold restore: the file was built by the planner over the sealed versions on this box and verified at `N`, and a cold restore from the generation would yield the same pages by construction (the snapshot is every page of that file). The anchor's PUT was acknowledged in `building`, so litestream's open reads position `N` from the listing and replication starts at `N + 1` (§5.1 step 7); a `building` replayed after a crash rebuilds and the sha256 is checked again | | replayable until `probing`; a sha256 or `CheckDB` mismatch is a rollback | |
| @@ -1929,8 +2102,8 @@ held** (§9.6, §19 K9): the target row is not retired by the region change |
| | phase | action | |
| |---|---| |
| | `releasing` | row `releasing` with `hold_op = rollback id`; `ReconstructStopEvidence` | |
| -| `released` | digests after a final checkpoint: database sha256, files plaintext, timers. **Clean** when all three equal what was installed (`landing.installed_db_sha256`, `source.files.plain`, `source.timers_sha256`) or `landing_phase` never reached `probing`; otherwise **dirty**. Write `stopped-target.json`; CAS the claim's execution holder to `none` | |
| -| `returning` (dirty only) | the handoff back: after a final checkpoint and `SyncAndWait`, write a snapshot of its stopped database (one level-9 LTX file `[1, N']`, every page, as the pinned writers write it, §5.1 step 2) into the source bucket's `moves/<host>/<rollback id>/replica/0009/<1>-<N'>.ltx`, seal it by `versionId` with `N'`, publish its files archive and timers snapshot under `files/` and `timers/`, write `move.json`. The return is under the release deadline (15 min), not the cut window, so the whole snapshot crosses the region here | |
| +| `released` | digests after a final checkpoint: database sha256, files plaintext, timers. **Clean** when all three equal what was installed (`landing.installed_db_sha256`, `source.files.plain`, `source.timers_sha256`) or `landing_phase` never reached `probing`, **and the seal recorded `src_covered`** (§7.4: the source's own replica reached its stopped database's position); otherwise **dirty**. Rev 7.11 adds the second condition (rule `seal-return`, INV-15): when the source's final upload was still in flight at the stop, the seal holds a write the source's replica does not, and a clean return would restore the source without it, declaring lost a write the staging and the landing's built generation hold. Write `stopped-target.json`; CAS the claim's execution holder to `none` | |
| +| `returning` (dirty only) | the handoff back: after a final checkpoint and `SyncAndWait`, write a snapshot of its stopped database (one level-9 LTX file `[1, N']`, every page, as the pinned writers write it, §5.1 step 2) into the source bucket's `moves/<host>/<rollback id>/replica/0009/<1>-<N'>.ltx`, seal it by `versionId` with `N'`, publish its files archive and timers snapshot under `files/` and `timers/`, write `move.json`. **A target that never restored a database** (dirty only for want of `src_covered`) returns the staged seal as it was given, pinned by the versions the cut journalled, and the staged files and timers with it. The return is under the release deadline (15 min), not the cut window, so the whole snapshot crosses the region here | |
| | `returned` (dirty only) | every artifact published | |
| | `cleaning` | only after the source records `recovered_at` (below): **bucket-park its `instances/<host>/` and its staging `moves/<host>/<move id>/` into `superseded/<move id>/<host>/`**, local-park its database, `<dbPath>.gen`, files and `<host>.env`, delete its row (conditional on `hold_op = rollback id`), clear its timers rows | |
| | `cleaned` | CAS `rollback.target_parked_at` | |
| @@ -1949,9 +2122,9 @@ because, until then, a source failure might need the target's state again. |
| | `claimed` | CAS the claim: `op.kind = restoring`, execution holder = this box, citing the target's evidence (§19 K4), **and `holder.stamp = op.source_stamp`**, the source installation's own stamp the flip journaled (claim rev 6.5: a CAS that makes an existing installation current again writes that installation's stamp; R6-4). The source's fresh read then matches its record, or re-initializes a lost one, to `S` | | |
| | `restoring` | row `restoring`, `hold_op = rollback id` | replayable | |
| | clean: `verified` | files and timers digests equal its `stopped` digests (a mismatch is `stuck`, INV-4); its warm database's `<dbPath>.gen` equals its pre-move generation | replayable | |
| -| dirty: `parking`, `building`, `published`, `local`, `configured`, `restored` | the target's install phases of §7.6, on the source, from `moves/<host>/<rollback id>/` (`building` restores the returned snapshot, requires `N'`, and writes the rollback generation's snapshot and anchor), with destination `superseded/<rollback id>/<host>/` for what it supersedes, **with two differences: `configured` and the release materialization run on the inputs the source renders now, recorded as `recovery.inputs`, and are never gated on `move.inputs`** (§7.7, J2-R2-5); and the stamps: the install runs under the source's pre-move installation `S`, which the `claimed` CAS wrote back into `holder.stamp` and which stays active; `local` runs `retire-artifacts(S)` on the pre-move database, tagged `S`, which moves no stamp; the return generation's database and files are tagged `S` as they are installed; the `probed` CAS below, which names the return generation in `holder.generation`, writes the **new `holder.stamp` `R`** in the same write, and the source's fresh read under the guard activates `R` before the open, tagging the return generation's artifacts `R` and retiring `S` then (claim rev 6.5 §6.4: a dirty rollback installs a new generation and never keeps its predecessor's stamp, R5-4, R6-4; rev 7.5's model kept it, rev 7.6's activated the target's). Rev 7.3 said "exactly" and so inherited the landing's `configured` gate: a bundle published after admission, a target that wrote, and a dirty rollback would then have failed before the recovery probe (R2-5). The model's `recovery-current-inputs` witness is that case (§14.2.5) | as §7.6 | |
| -| `probing` | the probe | **never replays an earlier phase**: once its recovery process has started, its own new writes are authoritative (INV-2, INV-7) | |
| -| `probed` | dirty: the claim CAS that names the return generation (`holder.generation = <rollback id>`, §5.1) and writes `holder.stamp`, the return installation's new stamp, in one write (claim rev 6.5 §2, §6.4) | | |
| +| dirty: `parking`, `building`, `published`, `local`, `configured`, `restored` | the target's install phases of §7.6, on the source, from `moves/<host>/<rollback id>/` (`building` restores the returned snapshot, requires `N'`, and writes the rollback generation's snapshot and anchor), with destination `superseded/<rollback id>/<host>/` for what it supersedes, **with two differences: `configured` and the release materialization run on the inputs the source renders now, recorded as `recovery.inputs`, and are never gated on `move.inputs`** (§7.7, J2-R2-5); and the stamps: the install runs under the source's pre-move installation `S`, which the `claimed` CAS wrote back into `holder.stamp` and which stays active; `local` runs `retire-artifacts(S)` on the pre-move database, tagged `S`, which moves no stamp (a leftover tagged with a **retired** stamp, left by a cold admission that issued its stamp and then failed its purge, is parked too, rev 7.11); the return generation's database and files are tagged `S` as they are installed; the `probed` CAS below, which names the return generation in `holder.generation`, writes the **new `holder.stamp` `R`** in the same write, and the source's fresh read under the guard activates `R` before the open, tagging the return generation's artifacts `R` and retiring `S` then (claim rev 6.5 §6.4: a dirty rollback installs a new generation and never keeps its predecessor's stamp, R5-4, R6-4; rev 7.5's model kept it, rev 7.6's activated the target's). Rev 7.3 said "exactly" and so inherited the landing's `configured` gate: a bundle published after admission, a target that wrote, and a dirty rollback would then have failed before the recovery probe (R2-5). The model's `recovery-current-inputs` witness is that case (§14.2.5) | as §7.6 | |
| +| `probing` | the probe, an `AdmitWriter` (§7.14): dirty, cold into the return generation from its pinned seal (`baseline: sealed`, no `writes_lost`); clean, warm or cold into the source's own generation, which the return CAS named again | **never replays an earlier phase**: once its recovery process has started, its own new writes are authoritative (INV-2, INV-7); a probe that dies before its session opened replication, or in its settle, is restarted, a new admission | |
| +| `probed` | the phase CAS alone: **`holder.generation` and `holder.stamp` moved at the probe's cold admission** (§7.14; a dirty return's generation and its new stamp, claim rev 6.5 §2 and 6.9 §6.4a), and the `probed` CAS writes neither (R10-3; rev 7.10's row still named the return generation here). Dirty: the return lane's `park-staging` chore is queued now | | |
| | `recovered` | CAS `rollback.recovered_at` | | |
| | `opened` | the conditional open on `hold_op = rollback id`; CAS `rollback.opened_at` | | |
| @@ -1981,13 +2154,20 @@ runs anywhere. It converges when the target returns (INV-3). |
| 1. **Commit** (target): record CAS `probed` → `committed`, conditional on |
| `now ≤ cut_deadline` (§7.4); then the claim follows (§7.5): phase |
| - `committed`, `holder.generation = move id`, plus the obligations in |
| - the same claim write, `park-superseded` for the source's location in |
| - its region and box, and `park-staging` for the target's staging |
| - (§19.3). |
| + `committed`, plus the obligations in the same claim write, |
| + `park-superseded` for the source's location in its region and box, |
| + and `park-staging` for the target's staging (§19.3). |
| + **`holder.generation` is not written** (R10-3): it is whatever the |
| + latest admission chose, the prepared generation `g-<move id>/` when |
| + the first probe passed, a fresh generation restored from it when a |
| + probe was restarted (§7.14). Rev 7.9's commit wrote `move id` here; |
| + after a restarted probe that had acknowledged writes into its fresh |
| + generation, that put the obsolete prepared generation back into |
| + authority and the next restore lost them. |
| 2. **Open** (target): conditional open on `hold_op = move id`; CAS |
| - `opened_at`. From here the target serves; the claim's `landing` op with |
| - phase `committed` admits it (§19 K6). |
| + `opened_at`. From here the target serves on the session its probe was |
| + admitted with; the claim's `landing` op with phase `committed` admits |
| + its later wakes as `AdmitWriter`s like serving's (§19 K6, §7.14). |
| 3. **Source park** (source, holding the lease on its own |
| `instances/<host>/`, claim spec C3): bucket-park its `instances/<host>/` into |
| `superseded/<move id>/<host>/`; local-park its database (with |
| @@ -2003,6 +2183,21 @@ runs anywhere. It converges when the target returns (INV-3). |
| ### 7.10 Stuck and declare-lost (M16) |
| +**What a declared-lost box leaves behind (rev 7.11).** Its acknowledged |
| +writes beyond its uploads are declared by the next admission's |
| +`writes_lost` (the record's `remote_max_txid` names where an operator |
| +finds them in the seal or the box's generation); its **registered |
| +timers** are declared by the console's declare-lost record itself and |
| +alerted, since no return lane will carry them; neither is ever exempted |
| +silently (R10-6). When the target of a rollback is the lost box and the |
| +seal was the one holder of the **source's** writes beyond its own |
| +replica (`src_covered` false, §7.4, §7.8), the return is clean for want |
| +of a target and the source's re-admission from its own generation |
| +declares its **cut session** as well, a second `writes_lost` record |
| +(`{box: source, generation: source's, session: the cut's, |
| +remote_max_txid}`) with its alert: the seal in the lost target's region |
| +is unreadable from the source and no lane brings it. |
| + |
| - **`stuck`:** the source's recovery probe failed. Held. `carlos move |
| resolve --host <h> --retry` reruns the recovery's `probing` phase. |
| - **`--declare-lost <box>` (M16)**, operator-only. `carlos move resolve |
| @@ -2132,19 +2327,21 @@ 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): cold, into a fresh generation restored from the dead probe's, since the dead probe's session has no certificate | | |
| +| 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; the same for a push's, a revert's and a rollback's probe | | |
| +| any: the agent restarts under a running app | stops the app: the session's replicator died with the old agent and a new agent process is a new session (claim rev 6.10); the next wake is an `AdmitWriter`, cold, which declares what the app acknowledged meanwhile (§7.14) | the same | | |
| +| any: the admitted writer dies between its CAS and its marker | the generation is unfinished; its predecessor stays live; the next wake is a cold admission whose baseline is the predecessor, or the generation itself when it holds the first upload (§7.14) | the same | | |
| | 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 like any writer (§7.14) | | | |
| | stuck | held; operator | | | |
| -### 7.14 Writer admission (claim rev 6.9 §6.4a; R7-1, R8-1, R8-2, R9-1 to R9-4) |
| +### 7.14 Writer admission (claim rev 6.10 §6.4a; R7-1, R8-1, R8-2, R9-1 to R9-4, R10-1 to R10-5) |
| Every path that opens replication is an `AdmitWriter` (§5.1 step 9), one |
| -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 |
| +claim CAS made **before the app process starts** (claim rev 6.10, R10-1), |
| +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: |
| @@ -2158,7 +2355,7 @@ phase**, in which mode, into which generation, and the CAS that handed it |
| | `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) | | | |
| +| `creating`, `deleting`, `parking`, `purging`, `placing` | nobody: the admission CAS refuses these kinds (R9-4, R10-4, INV-13); a create's first writer is admitted after `CompleteCreate`, under `serving` | | | |
| 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 |
| @@ -2176,32 +2373,48 @@ A clean rollback's **return CAS names the source's generation again** |
| 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: |
| +**The admitted writer's start**, on its box, in this order; it is the |
| +agent's own loop around one claim CAS, not a set of claim transitions, |
| +and a new agent process never resumes it (a new agent is a new session): |
| | step | action | if it fails | |
| |---|---|---| |
| -| 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 | | |
| +| 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; `KeepStamp` when `holder.stamp > holder.session`; a lagging `generation.json` is read through the writers journal (below) | nothing happened | |
| +| **`AdmitWriter`** | the CAS of §5.1 step 9, **first**: session, writer_box, journal entry; cold: generation, stamp unless kept, `writes_lost` for an uncertified predecessor the baseline does not cover (`baseline: sealed` otherwise); **no chore**: the predecessor is the unfinished generation's baseline until the marker names the new one (R10-2); the carried files are retagged with the new stamp here | a conflict: re-establish the evidence and decide again | |
| +| purge | delete the local database, with an error-returning purge | the start waits and purges again; the session stands | |
| +| 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 baseline from this region's remote, the predecessor or, behind a lagging marker, the nearest generation of the chain that holds an object | the start waits; 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 it acknowledges is outside the session | the retry policy (§5.1 step 9): a doubling backoff from one step, five attempts, then the host is marked failed, the start abandoned, and no session is created until an operator clears it | |
| +| first upload (cold, fresh, a non-empty baseline) | the full file `[1, 1]` of the restored database, captured once and acknowledged to the client; the generation has a root; it is in the session's ledger (R10-7) | retried with the same bytes after the client's wait, whether the original timed out or completed unseen; the session is uncertain for good | |
| +| 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). **Then the retire chores**: one `park-generation` per dead generation, the predecessor and the chain's (§5.1 step 9) | retried after the timeout; the writer waits | |
| +| anchor (warm, when the restored position is above the level-0 maximum) | `[N, N]`, acknowledged to the client; in the ledger (R10-7) | retried with the same bytes; the session is uncertain for good | |
| +| open | replication opens; the replica reads its remote position at its first sync; every later upload is the session's. An app stopped idle before this point is not closed: the replicator opens, ships what the app wrote, then closes cleanly | | |
| 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. |
| +`holder.generation` naming an **unfinished** generation `generation.json` |
| +does not (R10-2): its journalled predecessor is the live baseline, no |
| +chore retires it and the sweep protects it. The next admission, by this |
| +box or another `op.exec` box, reads the lag through the writers journal |
| +(§5.1 step 9): the marker names the latest admission's predecessor, or |
| +the predecessor of a chain of unfinished admissions, so this is the |
| +normal state and no alert; a `holder.generation` that holds objects (the |
| +first upload landed) has its marker published again, from the |
| +operation's build journal for a prepared generation, and the retire |
| +chores queued; an empty one is skipped and the baseline is the nearest |
| +generation of the chain that holds an object, else the marker's; the new |
| +marker retires them all. An empty `holder.generation` the journal does |
| +not explain is unexplained missing data: the start is refused and the |
| +box alerts. 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. |
| +An operation's release to `serving` carries the writers journal over, so |
| +an admission unfinished at the release (an abort released over a source |
| +admitted a tick earlier) stays explained. A marker that lands after its |
| +writer died, before the writer queued the chores, leaves the predecessor |
| +unretired: the next admission's marker stage retires the predecessor of |
| +every earlier cold admission of the operation whose entry is not marked |
| +covered. A pre-flip round never forces a sync on a session whose start is |
| +unfinished: there is no open replicator, and a forced upload would write |
| +the first upload's key with other bytes. |
| **Behaviour change against today's activator.** Today `Restore` |
| materializes the local database from S3 only when it is absent, "a |
| @@ -2211,13 +2424,21 @@ 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. |
| +prices it, and prices the probe's restore per attempt), 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. **The loss is normally within the |
| +replication interval** (§7.3, the sync class), the window between syncs; |
| +a failed or stalled upload extends it back to the last upload that |
| +landed, so the bound is the interval in operation and the age of the |
| +last durable upload in a fault (R10-8). Two more changes against today's |
| +activator (rev 7.11): the admitting CAS precedes the app start, so a |
| +start that fails leaves a session and a retry policy behind it rather |
| +than nothing; and an agent that restarts under a running app stops it |
| +and re-admits, where today's activator reattaches to the running unit. |
| +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, |
| @@ -2463,6 +2684,21 @@ combination-only, unexercised), each with its reason. The sweep exits |
| nonzero on any ERROR, any unexpected MISSED, and any expected miss that is |
| now caught (STALE). |
| +**Rev 7.11: the rare-at-depth outcome.** `expected-outcomes.txt` may |
| +list a rule as `rare <N>`: it has no witness of its own and the random |
| +sweep reaches it only at N seeds or more; below N its miss is reported as |
| +EXPECTED-MISS, at N or more a miss is MISSED, and a catch is never STALE. |
| +Three rules moved below the 3,000-seed line this round (`hostguard`, |
| +`stale-hold-release`, `strict-spawn`, §14.2.5) and are listed so at |
| +30,000. |
| + |
| +**Rev 7.11: structured counters (R10-9).** The baseline logs one |
| +`COUNTERS {json}` line beside the human-readable outcome map; the table |
| +generator reads it and fails on a missing required field. Rev 7.10's |
| +generator parsed the map with a regular expression that split |
| +`admissions: cold:57938` at the wrong colon and published zeros for |
| +every counter whose name carried one. |
| + |
| **Rev 7.1: one binary, no copies.** Mutation checks never touch the |
| source. The test binary is built once (the only step that writes the Go |
| build cache); `mutate.sh` then runs it once per rule with |
| @@ -3031,6 +3267,162 @@ 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.11: joint round 10 and claim rev 6.10.** |
| + |
| +- **The admitting CAS first (R10-1, claim rev 6.10).** `spawn` decides |
| + (`admitWriter`), makes the CAS (`admitCommit`) and only then opens an |
| + `openState` whose stages the agent's own loop drives (`resumeOpen`, |
| + `resumeStart`): `restore` (the purge, then the baseline), `app` (the |
| + start and readiness, under the retry policy: `startAttemptsMax = 5`, |
| + a backoff of `1 << (fails - 1)` steps from `startBackoff0 = 1`, then |
| + `hostFailed` with the session's start abandoned; the operator clears a |
| + failed host after half a horizon), `first`, `marker`, `anchor`, `open`. |
| + A session is the agent's: `localDB.Epoch` records the agent process |
| + that was admitted; a restarted agent (`forget` bumps `box.Epoch` and |
| + clears `open`) neither replicates nor certifies for it, and its first |
| + role step stops an app it finds running. An app stopped idle before |
| + `open` is not closed: the replicator opens, ships what the app wrote |
| + (`flush`), then closes. Rule `admit-before-start` (the mutation runs |
| + the app before the CAS, rev 7.10's order); witness |
| + `wAckBeforeAdmission`: a background worker (`w.startHook`) acknowledges |
| + a write right after the start and the box crashes before replication |
| + opens; admitted first, the next cold admission declares it; under the |
| + mutation the next warm admission purges it silently (INV-2 local). |
| +- **Unfinished generations and live baselines (R10-2).** `admitCommit` |
| + queues no chore. The `marker` stage, once `generation.json` names the |
| + new generation, calls `queueGenerationRetire` with the dead set: |
| + `openState.Dead` (the predecessor; behind a lagging marker the chain's |
| + empty generations and the marker's) plus the predecessor of every |
| + earlier cold entry of the writers journal not yet marked `Retired` |
| + (a writer that died after its marker landed and before the chore CAS; |
| + the CAS marks every earlier entry covered). `unfinishedChain` reads a |
| + lagging marker through the journal: `holder.generation` must be the |
| + latest entry's, and each earlier cold entry's predecessor the next, |
| + down to the marker's generation; `spawn`, `deadGeneration` (the |
| + sweep), `residueOf` (the live set) and `restoreAsNext` (what the next |
| + admission restores, the oracle's baseline at a release) share it. An |
| + empty `holder.generation` the chain does not explain is refused with |
| + an alert (`start refused: unexplained empty generation`); a marker the |
| + chain does not explain leaves the location untouched and alerts once. |
| + The release of an operation and the start of a move or a push carry |
| + `op.Writers` over, so an unfinished admission at a release stays |
| + explained; `owed` treats the predecessor of an uncovered entry as owed |
| + a chore, as a pending chore's keys are. `forget` clears `b.open`, the |
| + retry count and the backoff. Rule `baseline-live` (the mutation queues |
| + the chore at the CAS, as rev 7.10 did); witness `wBaselineParked`: a |
| + cold admission into a fresh generation, the box crashes before the |
| + first upload, the predecessor's retirement runs out its quiet time; |
| + under the mutation the predecessor is parked and the recovery restores |
| + nothing (INV-2 local). |
| +- **Commit and `probed` move no generation (R10-3).** Unchanged in the |
| + model since rev 7.10 (`holder.generation` moves only at a cold |
| + admission's CAS); the spec's §7.5, §7.6, §7.8 and §7.9 were brought to |
| + it. |
| +- **The library's `Admission` shape (R10-4).** `admitInput` has |
| + `KeepStamp` (set when `holder.stamp > holder.session`; `admitCommit` |
| + issues a stamp otherwise) and `BaselineCoversPredecessor` (true for an |
| + operation's prepared generation built from the stopped database, false |
| + when its seal was built from the remote because the disk was gone: |
| + `op.SealFromDB`, `op.ReturnFromDB`); warm passes an empty |
| + `NewGeneration`; `admitWriter` and `admitCommit` refuse `creating`, |
| + `deleting`, `parking`, `purging` and `placing`; a `baseline: sealed` |
| + entry records no `writes_lost`; the empty-generation ancestor restore |
| + needs the chain. `holder.writer_box` is `-1` before any writer. |
| +- **Serving-time chores and the root generation (R10-5).** |
| + `queueGenerationRetire` names `op = "session:<n>"` when the claim is |
| + `serving` or the op id is empty, and `"@root"` for the origin |
| + generation; the `park-generation` chore maps `"@root"` back to the |
| + root's own keys. |
| +- **Faults exempt nothing (R10-6).** The crash-with-disk fault, the idle |
| + disk-loss fault and the witness helper `loseDisk` remove physical state |
| + only. Exemptions come from a `writes_lost` declaration (writes of the |
| + declared box not durable in the new lineage), from the final oracle's |
| + would-be declaration for an uncertified serving session, and from a |
| + declared-lost box's registered timers (the console's declaration names |
| + and alerts them). INV-14: every `writes_lost` record raised an alert. |
| + INV-15: a write the host's remote holds is never declared lost while |
| + its writer's box is with us (the dirty-return witness's named failure |
| + since this round). |
| +- **Startup PUTs in the ledger (R10-7).** The first upload and the |
| + anchor are `track`ed; a retry after the client's wait, whether the |
| + original timed out or completed unseen (a lost response), sets the |
| + sticky uncertainty; the stage advances only on client-observed success; |
| + the bytes are captured once (`openState.blob`) and a retry carries |
| + them, and the writes acknowledged since the capture stay pending. |
| + Witnesses `wFirstUploadRetry` and `wAnchorRetry` (close-evidence). |
| +- **The budget (R10-8).** `cutEstimate` prices `RestoreAttempt`, `Admit` |
| + and `FreshUpload`; `attemptsAdmitted` sums attempts; the tests pin the |
| + 2 GiB example at 53.6 s fixed, 64.3 s for the first attempt, 117.9 s in |
| + all, one attempt, and the review's 2.5 GiB at 113.8 s under rev 7.10's |
| + arithmetic and refused under rev 7.11's. |
| +- **Structured counters (R10-9).** The baseline logs `COUNTERS {json}`; |
| + `tables.py` reads it and fails on a missing field. |
| +- **The rollback's return carries the seal when the source's replica is |
| + short (rule `seal-return`, INV-15).** The seal CAS journals |
| + `src_covered` (the source's replica of its generation reached the |
| + stopped database's position, no write pending, the session's start |
| + complete); `releaseTarget` makes the return dirty when it is false; a |
| + target without a database returns the staged seal by version |
| + (`sealVersion`). Witness `wSealReturn`: the source's last upload is |
| + held when the cut stops it, the landing is rolled back after its build, |
| + and treated as clean the source declares a write the landing's built |
| + generation holds. |
| +- **Probes that die restart.** A push's, a revert's and a rollback's |
| + `probed` phase restart a probe whose process is gone instead of |
| + releasing or opening over it (the landing's already did); every |
| + `probed` phase waits for `b.open == nil`. |
| +- **Model faults found and fixed this round** (all before the final |
| + numbers; a 300-seed gate passed each intermediate build, the 30,000- |
| + and 100,000-seed baselines found them): a first upload or anchor whose |
| + completion the client never saw was never retried (seed 571 / 30,000); |
| + a rollback after the retry policy marked the target failed left its |
| + abandoned start to resume once the operator cleared the host, and two |
| + boxes ran the host (seed 25581 / 30,000: a start is abandoned when |
| + `op.exec` moves away or the host is marked failed); a purge that |
| + failed after the CAS and a crash before the marker made two unfinished |
| + admissions in a row, which the single-predecessor reading refused |
| + forever (seed 28216 / 30,000: the chain); a push released over a dead |
| + probe whose marker never landed (seed 487 / 30,000); an idle stop |
| + before replication opened certified position 0 over two unshipped |
| + writes (seed 2663 / 30,000); a pre-flip round forced a sync on a |
| + session whose first upload was in flight and wrote its key with other |
| + bytes (seed 17056 / 30,000), and on a dead session's database after an |
| + agent restart, where the skipped upload counted as durable (seed 12582 |
| + / 100,000); a first upload retried with fresh bytes carried a write |
| + the original did not, and the original landed last (seed 7574 / |
| + 30,000); a restarted agent continued a dead session's replication and |
| + its first sync was skipped at the dead session's remote position (seed |
| + 8528 / 30,000); the predecessor of a writer that died between its |
| + marker landing and its chore CAS was never retired (seeds 899, 4159, |
| + 26817 / 30,000); an abort released over a source admitted a tick |
| + earlier and the oracle restored an unfinished generation (seed 1052 / |
| + 30,000: the journal survives the release, the oracle restores as the |
| + next admission would); a declared-lost target's registered timers were |
| + lost undeclared (seed 4120 / 30,000); a clean rollback restored the |
| + source from a replica short of its stopped database and declared a |
| + write the seal held (seed 17056 / 30,000: `seal-return`); a cut or a |
| + push on a box without a database sealed an empty database when its |
| + remote's marker lagged (seeds 3987 and 14322 / 30,000: the seal is what |
| + the next admission would restore, and nothing is sealed over data that |
| + cannot be read); a seal built from the remote after a lost disk was |
| + taken to cover the predecessor and a pending write went undeclared |
| + (seed 34260 / 100,000); a declared-lost target that returned had its |
| + declared writes judged by INV-15 (seed 54594 / 100,000: the operation's |
| + lost box counts); a dirty install parked a dead installation's leftover |
| + under a newer active stamp (seed 65090 / 100,000: a retired stamp's |
| + artifact may be parked); the journal-wide retire set first queued a |
| + chore per generation and starved two restoring operations of their |
| + release (seeds 542 and 2412 / 3,000: uncovered entries only); a |
| + rollback whose target was declared lost before any lane ran declared a |
| + write the seal in the lost region held, which INV-15 refused (seed 8035 |
| + / 30,000: a lost box's rollback is INV-15's exception), and left the |
| + source's own cut-session writes undeclared (seeds 16395 and 27191 / |
| + 30,000: the source's re-admission declares its cut session too, §7.10); |
| + an adoption left `holder.writer_box` unset and the first cold |
| + admission's declaration named the wrong box, so the legacy process's |
| + writes lost with its disk went undeclared (seed 94288 / 100,000: the |
| + adoption names the box running the pre-release process). |
| + |
| **Rev 7.10: joint round 9 and claim rev 6.9.** |
| - **No local database reuse (R9-1, claim rev 6.9).** `spawn` admits every |
| @@ -3369,6 +3761,42 @@ 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.11, on the final model (claim rev 6.10: the admitting CAS before |
| +the app start, a session per agent process, the retry policy, unfinished |
| +generations with live baselines, the library's admission shape, |
| +declarations as the only exemptions, startup PUTs in the ledger, the |
| +uncovered return): 30,000 seeds, zero violations; 100,000 seeds, zero |
| +violations** (388 s and 1190 s). Across the 100,000 seeds: |
| +149,786 completed operations, among them 61,925 cold and |
| +16,748 warm admissions (19,934 clean closes, |
| +1,543 closes refused as uncertain, 0 stale |
| +certificates, 1,008 wakes that waited for a draining writer, |
| +55,816 local databases purged, 4,418 starts that |
| +waited for a failed purge, 48,474 writes_lost records declaring |
| +8,841 acknowledged writes lost, 29,100 full first |
| +uploads, 55,026 start steps that waited for their marker, |
| +532 markers published again, 3,854 probes |
| +restarted, 1,371 app starts that failed and were retried |
| +within their session, 256 hosts marked failed by the retry |
| +policy, 112 seals whose source replica was short and |
| +51 returns that carried the seal), 824 |
| +completed moves, 2,199 clean and 98 dirty |
| +rollbacks, 353 pre-flip reverts, 287 declared |
| +losses, 25,677 pushes, 89,192 delete-park-free cycles and |
| +4,927 lost disks (3,649 with a crash); |
| +9,331 LTX compactions, 6,543 snapshot rotations, |
| +557 level-0 upload retries, 30,198 anchors; |
| +26,074 local stamp records lost and re-initialized; |
| +43,228 requests completed after `H`; 32,872 staging |
| +signatures refused as stale; 30,501 creates restarted on a |
| +412. Every oracle left the system unchanged. The model faults the new |
| +protocol exposed before these baselines are listed in §14.2.2. Rev |
| +7.10's published counters for this paragraph were wrong (R10-9: the |
| +generator misparsed every name with a colon); its retained baseline |
| +reads 57,938 cold and 17,025 warm admissions, 1,283 closes refused as |
| +uncertain, 6,761 starts refused by a failed purge and 56,380 waits for |
| +the marker, and the zero-violation verdict stands. |
| + |
| **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 |
| @@ -3611,37 +4039,74 @@ 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.10 model (572066ec), with the strict classification, |
| +on the final rev 7.11 model (bd1587a1), 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 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 **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 |
| +same mutation, for the 48 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 **95 rules**: rev 7.10's 92 plus |
| +`admit-before-start` (R10-1), `baseline-live` (R10-2) and `seal-return` |
| +(rev 7.11 §7.8). `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.10's |
| +counts are in the rev 7.10 spec (33ce0a9c); the admitting CAS before the |
| +start and the retry policy change what every start does, so sweep counts |
| +moved throughout. **Every table below is regenerated from the retained |
| +verdict files** (R9-6; `~/.cache/nearest-region/rev711-sweeps/`), none is |
| carried over. |
| | | rules | |
| |---|---| |
| | 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) | |
| +| caught alone by the sweep at 30,000 (and by their witness, where one exists) | 8 (`evidence-whole-tree`, `hostguard`, `markers-last`, `orphan-order`, `restore-overlap`, `seal-return`, `stale-hold-release`, `strict-spawn`) | |
| +| caught alone by the sweep at 100,000 (and by its witness, where one exists) | 3 (`baseline-live`, `declare-lost-compute`, `newest-l0`) | |
| +| caught alone by their witness only; the sweep misses them at 30,000 | 6 (`admit-before-start`, `close-evidence`, `close-waits`, `closed-marker`, `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 | 8 | |
| +| subsumed: the witness holds under every combination tried, or the scenario is unreachable by construction | 2 (`door-reread`, `door-by-version`, by C3a and by writer epochs; historical results only, below). `start-check`, subsumed in rev 7.10, is caught alone by the sweep again since rev 7.11: with the whole check gone the lagging-marker reading is skipped and an empty generation is restored as if it held the data | |
| | liveness only | 2 (`readiness-key`, `config-before-probe`) | |
| | unreachable under claim rev 5 | 1 (`readiness-quiet`) | |
| | unexercised | **0** | |
| +**What rev 7.11 moved.** The three new rules: `admit-before-start` is |
| +witness-only (sweep 0 / 3,000, 0 / 30,000, 0 / 100,000: a background |
| +acknowledgement in the few ticks between the start and readiness, then a |
| +crash before replication opens, is a schedule the generator does not |
| +produce), `baseline-live` 0 / 3,000, 0 / 30,000, 2 / 100,000 (a crash |
| +between the CAS and the first upload, with the predecessor parked by the |
| +chore at the CAS), `seal-return` 0 / 3,000, 10 / 30,000, 26 / 100,000 (a |
| +source upload in flight at the cut, then a rollback). `start-check` |
| +(13 / 3,000, 181 / 30,000) and `start-check-claim-gen` (12 / 3,000, |
| +140 / 30,000) are caught alone again: the lagging-marker reading hangs on the |
| +generation clause, so the rev 5 check restores an empty generation as |
| +if it held the data; both leave `expected-outcomes.txt`. The orders |
| +changed by the new start moved several counts: `hostguard` |
| +0 / 3,000, 2 / 30,000, 2 / 100,000 and `stale-hold-release` 0 / 3,000, 15 / 30,000, 46 / 100,000 fell |
| +below the 3,000-seed line; `writer-session` 1 / 3,000, 19 / 30,000, 61 / 100,000, |
| +`admit-everywhere` 705 / 3,000, 6,772 / 30,000, 22,881 / 100,000, `writes-lost` |
| +11 / 3,000, 122 / 30,000, 395 / 100,000, `recovery-generation` 9 / 3,000, 98 / 30,000, 361 / 100,000, |
| +`anchor-acked` 13 / 3,000, 103 / 30,000, 358 / 100,000, `restore-anchor` |
| +58 / 3,000, 590 / 30,000, 1,954 / 100,000, `return-stamp` 74 / 3,000, 772 / 30,000, 2,583 / 100,000, |
| +`root-advance` 11 / 3,000, 115 / 30,000, 422 / 100,000, `location-per-incarnation` |
| +28 / 3,000, 360 / 30,000, 1,179 / 100,000, `dirty-return` 1 / 3,000, 25 / 30,000, |
| +`strict-spawn` 0 / 3,000, 1 / 30,000, 11 / 100,000 (back below the 3,000 line, with |
| +`hostguard` and `stale-hold-release`; the three are `rare 30000` in |
| +`expected-outcomes.txt`, §14.2.1). The witness-only rules keep their |
| +shape: `remote-baseline` witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000, `close-evidence` |
| +witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000, `closed-marker` witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000, |
| +`close-waits` witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000, |
| +`restore-gap-closed` witness; sweep 0 / 3,000, 0 / 30,000; `newest-l0` |
| +(0 / 3,000, 0 / 30,000, 1 / 100,000) and `live-set-region` (2 / 3,000, |
| +13 / 30,000) are reached by the sweep now; the pair `admit-bind-op` + |
| +`claim-cas-opid` 0 / 30,000, 0 / 100,000. The admission four |
| +143 / 30,000, 503 / 100,000; the |
| +three box-side fences |
| +140 / 30,000 with the witness |
| +held, caught through the generation clause's own catch, so the triple |
| +leaves `expected-outcomes.txt` too. |
| + |
| **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 |
| @@ -3740,51 +4205,55 @@ 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 | | 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 | |
| +| `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 | | 2 / 3,000, 12 / 30,000, 52 / 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, 30 / 30,000, 77 / 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, 1 / 100,000 | |
| | `watchdog-independent` (§7.1) | as above, with the agent alone paused, so the application keeps running | held | with `declare-lost-compute`: **violated**, INV-1 | 0 / 3,000 | |
| -| `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 | | 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 | |
| +| `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, 5 / 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, 5 / 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, 9 / 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, 6 / 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 | | 1 / 3,000, 2 / 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, 25 / 30,000 | |
| +| `commit-before-open` (INV-5; R3-5) | a public request reaches the target's edge while its probe runs | **violated**: INV-5 | | 2 / 3,000, 61 / 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 | |
| +| `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 / 3,000, 1 / 30,000, 11 / 100,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 | |
| +| `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) | | 336 / 3,000, 3,071 / 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 | 334 / 3,000, 3,017 / 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 | | 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 | |
| +| `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 | | 541 / 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 | | 2 / 3,000, 13 / 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, 2 / 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 | |
| +| `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) | | 58 / 3,000, 590 / 30,000, 1,954 / 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) | | 11 / 3,000, 115 / 30,000, 422 / 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) | | 13 / 3,000, 103 / 30,000, 358 / 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) | | 74 / 3,000, 772 / 30,000, 2,583 / 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) | | 9 / 3,000, 98 / 30,000, 361 / 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 | |
| +| `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) | | 699 / 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, 7 / 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` | | 2 / 3,000, 21 / 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` | | 40 / 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) | | 1 / 3,000, 19 / 30,000, 61 / 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 | | 705 / 3,000, 6,772 / 30,000, 22,881 / 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 | |
| +| `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) | | 41 / 3,000, 389 / 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 | |
| +| `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 | | 11 / 3,000, 122 / 30,000, 395 / 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 | |
| +| `admit-before-start` (claim rev 6.10 §6.4a, R10-1) | a background worker acknowledges a write right after the app starts; the box crashes before replication opens; admitted before the start, the acknowledgement is the session's and the next cold admission declares it | **violated**: under rev 6.8.2's order the acknowledgement is in a database the next warm admission purges silently (INV-2 local) | | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 | |
| +| `baseline-live` (claim rev 6.10 §6.4a, R10-2) | a cold admission into a fresh generation; the box crashes before the first upload; the predecessor's retirement runs out its quiet time; the recovery | **violated**: with the chore at the CAS the predecessor is parked and the recovery restores nothing (INV-2 local) | | 0 / 3,000, 0 / 30,000, 2 / 100,000 | |
| +| `seal-return` (rev 7.11 §7.8) | the source's last upload is in flight when the cut stops it; the landing is rolled back after its build; the return must carry the seal | **violated**: treated as clean, the source's cold admission declares a write the landing's built generation holds (INV-15) | | 0 / 3,000, 10 / 30,000, 26 / 100,000 | |
| +| `close-evidence` (R10-7), two more scenarios | (i) a fresh generation's first upload is held past the client's timeout and its retry lands; (ii) a warm admission's anchor is held and its retry lands; then a clean stop | **violated** in each: the certificate is written while a request of the session was retried after a timeout | | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 | |
| **The purge fence, the ETag condition and C5a.** `purge-claim-fence` |
| (CC21) is caught alone by the sweep: 28 / 3,000, 240 / 30,000. |
| @@ -3808,51 +4277,53 @@ 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: 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 ‡). |
| +**Caught alone: 82 of 95** (65 by the sweep at 3,000; 8 by the sweep at |
| +30,000, marked †; 3 at 100,000, |
| +marked ††; 6 by their witness alone, marked ‡). |
| | rule | seeds failing | | rule | seeds failing | |
| |---|---|---|---|---| |
| -| `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 | |
| +| `abort-target-owner` | 939 / 3,000 | | `admission-registration` | 32 / 3,000 | |
| +| `admit-before-start` ‡ | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 | | `admit-everywhere` | 705 / 3,000, 6,772 / 30,000, 22,881 / 100,000 | |
| +| `anchor-acked` | 13 / 3,000, 103 / 30,000, 358 / 100,000 | | `baseline-live` †† | 0 / 3,000, 0 / 30,000, 2 / 100,000 | |
| +| `build-completion` | 699 / 3,000 | | `cancelled-creates` | 383 / 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` | 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 | |
| +| `closed-marker` ‡ | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 | | `commit-before-open` | 2 / 3,000, 61 / 30,000 | |
| +| `cut-deadline` | 38 / 3,000 | | `declare-lost-compute` †† | 0 / 3,000, 0 / 30,000, 1 / 100,000 | |
| +| `dirty-return` | 1 / 3,000, 25 / 30,000 | | `evidence-from-state` | 2,610 / 3,000 | |
| +| `evidence-whole-tree` † | 0 / 3,000, 7 / 30,000 | | `fence-by-installation` | 336 / 3,000, 3,071 / 30,000 | |
| +| `fence-etag` | 26 / 3,000, 229 / 30,000 | | `fence-stamp` | 334 / 3,000, 3,017 / 30,000 | |
| +| `files-carried` | 33 / 3,000 | | `floor-boot-recovery` | 2,576 / 3,000 | |
| +| `fresh-admission` | 10 / 3,000 | | `fresh-incarnation` | 41 / 3,000 | |
| +| `generation-conditional` | 2 / 3,000, 12 / 30,000, 52 / 100,000 | | `hostguard` † | 0 / 3,000, 2 / 30,000, 2 / 100,000 | |
| +| `legacy-discovery` | 276 / 3,000, 2,738 / 30,000 | | `live-set-region` | 2 / 3,000, 13 / 30,000 | |
| +| `location-per-incarnation` | 28 / 3,000, 360 / 30,000, 1,179 / 100,000 | | `lost-quarantine` | 1 / 3,000, 5 / 30,000 | |
| +| `lost-return-park` | 1 / 3,000, 30 / 30,000, 77 / 100,000 | | `markers-last` † | 0 / 3,000, 5 / 30,000 | |
| +| `newest-l0` †† | 0 / 3,000, 0 / 30,000, 1 / 100,000 | | `obligations-block-ops` | 32 / 3,000 | |
| +| `orphan-no-deadline` | 41 / 3,000 | | `orphan-order` † | 0 / 3,000, 1 / 30,000 | |
| +| `park-all-versions` | 567 / 3,000 | | `park-by-version` | 2,527 / 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 | | | | |
| +| `purge-adopts` | 7 / 3,000 | | `purge-claim-fence` | 22 / 3,000, 232 / 30,000 | |
| +| `purge-journal` | 1,889 / 3,000 | | `purge-reserve-first` | 2,145 / 3,000 | |
| +| `quiet-before-ack` | 179 / 3,000 | | `recovery-current-inputs` | 40 / 3,000 | |
| +| `recovery-generation` | 9 / 3,000, 98 / 30,000, 361 / 100,000 | | `recovery-pass` | 2,482 / 3,000 | |
| +| `registration-recovery` | 2,116 / 3,000 | | `remote-baseline` ‡ | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 | |
| +| `restore-anchor` | 58 / 3,000, 590 / 30,000, 1,954 / 100,000 | | `restore-by-generation` | 133 / 3,000 | |
| +| `restore-gap-closed` ‡ | witness; sweep 0 / 3,000, 0 / 30,000 | | `restore-overlap` † | 0 / 3,000, 2 / 30,000 | |
| +| `retirement-ids` | 482 / 3,000 | | `return-stamp` | 74 / 3,000, 772 / 30,000, 2,583 / 100,000 | |
| +| `revalidate-before-effect` | 18 / 3,000, 188 / 30,000 | | `revert-journal` | 12 / 3,000 | |
| +| `rollback-journal` | 1 / 3,000, 9 / 30,000 | | `root-advance` | 11 / 3,000, 115 / 30,000, 422 / 100,000 | |
| +| `sdk-no-resign` | 10 / 3,000 | | `seal-by-version` | 1 / 3,000, 6 / 30,000 | |
| +| `seal-return` † | 0 / 3,000, 10 / 30,000, 26 / 100,000 | | `sign-at-check` | 11 / 3,000 | |
| +| `sign-before-safeuntil` | 17 / 3,000 | | `source-readiness` | 10 / 3,000 | |
| +| `staging-quiet` | 1 / 3,000, 2 / 30,000 | | `stale-hold-release` † | 0 / 3,000, 15 / 30,000, 46 / 100,000 | |
| +| `start-check` | 13 / 3,000, 181 / 30,000 | | `start-check-claim-gen` | 12 / 3,000, 140 / 30,000 | |
| +| `straggler-sweep` | 774 / 3,000 | | `strict-spawn` † | 0 / 3,000, 1 / 30,000, 11 / 100,000 | |
| +| `sweep-namespace` | 541 / 3,000 | | `sweep-staging` | 34 / 3,000 | |
| +| `target-park` | 25 / 3,000 | | `timer-canonical` | 3 / 3,000 | |
| +| `timer-freeze` | 2 / 3,000, 21 / 30,000 | | `valid-ltx` | 41 / 3,000, 389 / 30,000 | |
| +| `writer-session` | 1 / 3,000, 19 / 30,000, 61 / 100,000 | | `writes-lost` | 11 / 3,000, 122 / 30,000, 395 / 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` |
| @@ -3867,19 +4338,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) | 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 | |
| +| `purge-claim-fence` + `fence-etag` (**the re-read alone**, rev 7's CC21 as proposed) | 340 / 30,000 | `purge-claim-fence` 22 / 3,000, 232 / 30,000, `fence-etag` 26 / 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` | 269 / 30,000 | `registration-check` 0 / 3,000, `purge-claim-fence` 22 / 3,000, 232 / 30,000 | violated | the same | |
| +| `registration-check` + `fence-etag` | 270 / 30,000 | `registration-check` 0 / 3,000, `fence-etag` 26 / 3,000, 229 / 30,000 | violated | the same | |
| +| `exec-admission` + `hold-op-open` + `start-check-claim-gen` + `exec-writer` | 143 / 30,000, 503 / 100,000 | `exec-admission` 0 / 3,000, `hold-op-open` 0 / 3,000, `start-check-claim-gen` 12 / 3,000, 140 / 30,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` | 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 | |
| +| `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` 28 / 3,000, 360 / 30,000, 1,179 / 100,000 this round (rev 7.10's row said 336 / 30,000 against its own result of 357, R10-9) | 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` 28 / 3,000, 360 / 30,000, 1,179 / 100,000 this round | retired | the same | |
| +| `claim-cas-opid` + `revalidate-before-effect` | 898 / 30,000 | `claim-cas-opid` 0 / 3,000, `revalidate-before-effect` 18 / 3,000, 188 / 30,000 | violated | a stale step destroys a store | |
| +| `strict-spawn` + `evidence-whole-tree` | 86 / 30,000 | `strict-spawn` 0 / 3,000, 1 / 30,000, 11 / 100,000, `evidence-whole-tree` 0 / 3,000, 7 / 30,000 | violated | two writers | |
| +| `touched-incomplete` + `legacy-discovery` | 7,292 / 30,000 | `touched-incomplete` 0 / 3,000, `legacy-discovery` 276 / 3,000, 2,738 / 30,000 | violated | a freed host's residue | |
| +| `declare-lost-compute` + `watchdog-independent` | 0 / 30,000, 2 / 100,000 | `declare-lost-compute` 0 / 3,000, 0 / 30,000, 1 / 100,000, `watchdog-independent` 0 / 3,000 | violated | two writers after a paused or frozen target resumes | |
| +| `fence-stamp` + `hostguard` (no longer combination-only) | 3,966 / 30,000 | `fence-stamp` 334 / 3,000, 3,017 / 30,000, `hostguard` 0 / 3,000, 2 / 30,000, 2 / 100,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 |
| @@ -4299,6 +4770,56 @@ although the seal carries every write; the admitted writer's start |
| 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.9.1 and 6.10 (3f916b05), after joint round 10: no change |
| +requested, eight notes.** Rev 6.9.1 answered rev 7.10's seven readings |
| +(confirmed: the ancestor restore from a complete listing, the prepared |
| +generation opened once, the return CAS naming the source's generation, |
| +`writer_box` as a baseline choice only, C2 and the delete witness; |
| +refined: `KeepStamp` only when `holder.stamp > holder.session`; changed: |
| +no `writes_lost` behind a seal that covers the stopped predecessor, |
| +compared against the seal's own position). Rev 6.10 answers R10-1, |
| +R10-2, R10-4 and R10-5 (§6.4a: the CAS before the app start, a session |
| +per agent process, the retry policy with this spec's limit, unfinished |
| +generations with live baselines and chores after the marker, the five |
| +refused kinds, warm with an empty `NewGeneration`, the ancestor restore |
| +only for the latest journalled unfinished admission, `session:<n>` |
| +chores, `"@root"`). Rev 7.11 encodes all of it (§5.1 step 9, §7.14, |
| +§14.2.2). Notes for platform-1e (`moves-claim-questions.md`, rev 7.11 |
| +heading): **(1)** the retry limit is five attempts under one session |
| +with a doubling backoff from one step, then the host is marked failed |
| +and gets no session until an operator clears it; **(2)** "the marker |
| +names the journalled predecessor of the latest admission" is read to |
| +include a **chain**: a marker naming the predecessor of a run of |
| +admissions each of which died before its marker (the second's purge |
| +failed after its CAS) is the same normal state, every generation of the |
| +chain is live, and the baseline is the nearest that holds an object; |
| +**(3)** `op.journal.writers` must **survive the release** to `serving` |
| +and the start of the next operation, or the release must wait for an |
| +unfinished start: an abort released over a source admitted a tick |
| +earlier left a lagging marker nothing explained; **(4)** a writer that |
| +dies after its marker landed and before `QueueGenerationRetire` leaves |
| +its predecessor unretired: the next admission's marker retires the |
| +predecessor of every earlier cold entry the journal does not mark |
| +covered, so the journal needs that mark (or E's `QueueGenerationRetire` |
| +may be given every uncovered predecessor); **(5)** a rollback is clean |
| +only when the seal recorded the source's own replica as covering its |
| +stopped database (`src_covered`); otherwise the return carries the seal |
| +whether or not the target wrote, and a target that never restored a |
| +database returns the staged seal by version (rule `seal-return`); the |
| +clean/dirty verdict is this spec's, but the claim's "clean rollback |
| +restores the source from its own generation" should say "when its |
| +replica covers the stop"; **(6)** `BaselineCoversPredecessor` is true |
| +only for a seal built from the stopped database itself; a seal built |
| +from the remote because the disk was gone stops at the remote's |
| +position, and the prepared generation's admission records `writes_lost` |
| +for the writes beyond it; **(7)** "a new agent process is a new |
| +session" is read to mean the restarted agent **stops a running app** of |
| +the dead session and admits anew, where today's activator reattaches to |
| +the unit; **(8)** a declared-lost box's registered timers are declared |
| +by the console's record and alerted, since no return lane carries them; |
| +and `holder.writer_box` has no box before the first writer (the model |
| +uses `-1`; E's string names have no such ambiguity). |
| + |
| **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`, |
| @@ -4671,6 +5192,29 @@ 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.17 Joint round 10 (claim f6180ae4, moves rev 7.10 33ce0a9c, model 572066ec, library E fdff530f) |
| + |
| +Round 10 judged the simplification sound (generation reuse needs a |
| +one-use certificate; local database reuse is unnecessary) and found three |
| +P1s, five P2s and a P3. Claim rev 6.9.1 answered rev 7.10's readings and |
| +rev 6.10 (3f916b05) rewrote §6.4a's order; the library E at 090fb7a2 |
| +implements `KeepStamp`, `BaselineCoversPredecessor`, |
| +`QueueGenerationRetire` and `"@root"`. |
| + |
| +| finding | rev 7.11 | |
| +|---|---| |
| +| R10-1 (P1) an app could acknowledge writes before it had a writer session; failed starts needed retry control, not another admission | the admitting CAS comes first; a session belongs to the agent's replicator and a new agent process is a new session (it stops a running app it finds); the retry policy: five attempts under one session, a doubling backoff from one step, then the host is marked failed and gets no session until an operator clears it (§5.1 step 9, §7.14); rule `admit-before-start`, witness `wAckBeforeAdmission` | |
| +| R10-2 (P1) cleanup could retire the only recovery baseline before the successor had one; `forget()` kept `b.open`; the sweep treated a disagreeing marker as residue | a cold admission's generation is unfinished until `generation.json` names it; its predecessor is live, no chore retires it and the sweep protects it; the marker's publication queues the chores; a lagging marker that the writers journal explains (the predecessor of the latest admission, or of a chain) is the normal state and no alert, any other disagreement leaves the location untouched and alerts; `forget()` clears the open start (§5.1 step 9, §6.4, §7.14); rule `baseline-live`, witness `wBaselineParked` | |
| +| R10-3 (P1) §7.5 and §7.9 wrote `holder.generation = move id` at the commit; §7.6 and §7.8 kept obsolete publication and `probed` instructions | §7.5, §7.6, §7.8 and §7.9 rewritten around §7.14: the commit and the `probed` CASes move no generation, the marker is the probe's admission's, the return generation moves at the probe's cold admission | |
| +| R10-4 (P2) the shared admission contract differed: stamps, refused kinds, baseline, warm input | `KeepStamp` when `holder.stamp > holder.session`; refused in `creating`, `deleting`, `parking`, `purging`, `placing`; `BaselineCoversPredecessor` for a seal built from the stopped database, compared against the seal's position, `baseline: sealed`, no `writes_lost`; warm with an empty `NewGeneration`; the empty-generation ancestor restore only for a journalled unfinished admission (or chain); the model's `admitInput` is shaped like E's `Admission` (§5.1 step 9, §7.14) | |
| +| R10-5 (P2) E could not represent an ordinary serving admission's chores or an adopted root's retirement | serving-time chores use `op = "session:<holder.session>"`; the adopted host's root generation is `"@root"`, `holder.generation` `""` until the first cold admission, and `holder.writer_box` the box running the pre-release process, so the first cold admission's `writes_lost` names it (§5.1 step 9) | |
| +| R10-6 (P2) disk-loss faults exempted writes without a declaration and without the write-only restriction | the faults remove physical state only; exemptions come from durable `writes_lost` declarations (writes only), the final oracle's would-be declaration, and a declared-lost box's timer declaration; INV-14 checks alert delivery, INV-15 refuses declaring a write the remote holds (§14.2.2) | |
| +| R10-7 (P2) startup PUT retries bypassed the close evidence; object visibility advanced the start without client-observed acknowledgement | the first upload and the anchor enter the ledger; a retry after the client's wait, a timeout or a lost response, makes the session uncertain for good; only client-observed success advances the start; the bytes are captured once (§5.1 step 9, §7.14); witnesses `wFirstUploadRetry`, `wAnchorRetry` | |
| +| R10-8 (P2) the budget priced the old protocol; "bounded by the replication interval" was too strong | a restore per probe attempt, the admission's overhead and a fresh generation's upload on a retried probe are priced; the 2 GiB example runs to 117.9 s and admits one attempt, the 2.5 GiB workload is refused at 131.2 s (§7.3); the interval is the normal window and a failed upload extends the loss back to the last durable upload (§7.14) | |
| +| R10-9 (P3) the generated counters were wrong; a door row carried 336 against 357 | `COUNTERS {json}` in the baseline, a generator that fails on a missing field, §14.2.3 and the change note regenerated, the door rows read from the verdicts (§14.2.1, §14.2.3, §14.2.5) | |
| +| the readings judged | the ancestor restore needs cleanup protection (R10-2, done); the prepared generation opened once (confirmed); the landing flip's stamp kept only under `KeepStamp`'s rule; the clean return (kept, with `src_covered`); the landing's `writes_lost` behind a complete seal (dropped: `baseline: sealed`); startup retries as local bookkeeping (kept, within the session's ledger, and a new process is a new session); C2 and the delete witness (confirmed) | |
| +| beyond the review | `seal-return` and the agent-restart rule, found by the rerun (§14.2.2) | |
| + |
| ### 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 |