amadan
spec: move-any-app rev 7.12: joint round 11, holder.admissions and PublishGeneration (claim rev 6.12), every number rerun (#175)
Answers CODEX-FINDINGS-JOINT-R11 (R11-1 to R11-5, the R10-3 leftovers, R10-6's final oracle, the probe retry deadline) against claim rev 6.12 (b202ea4e, with rev 6.11's answers) and the library E at 34224a29. holder.admissions replaces op.journal.writers; the predecessor is the last record (INV-16); Coverage "" | sealed | clean-return replaces BaselineCoversPredecessor, with clean-return speaking for the target's probe session and the source's cut session only; PublishGeneration is the one retirement path, bound to op and phase, legal in every operation a writer runs in, with per-region coverage; the sweep reads an absent marker as the origin; the final oracle runs the recovery admission for real; a probe attempt's five restarts share its 30 s window and a probe never marks the host failed; §5.1, §7.8 and the authoritative-region table assign holder.generation only at a cold admission's CAS or the clean return. Results on model af9b89ed: 30,000 and 100,000 seeds clean; 96 rules, 83 caught alone (64 at 3,000, 10 at 30,000, 2 at 100,000, 7 by witness), 8 combination-only, 2 subsumed, 2 liveness, 1 unreachable; every table regenerated from the retained verdicts. §22.18 has every disposition; §19.4 the notes for platform-1e.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
1 file changed,
+440
−158
docs/superpowers/specs/2026-10-02-move-any-app-design.md+440 −158
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 77079268c..24137b7e0 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,45 @@ |
| # Move any app or instance to another region: Phase 1, a safe single-instance move |
| **Date:** 2026-10-05 |
| -**Revision:** 7.11. |
| +**Revision:** 7.12. |
| + |
| +- **Rev 7.12** answers **joint round 11** (`CODEX-FINDINGS-JOINT-R11.md`, |
| + cited "R11-n") and is written against **claim spec rev 6.12** |
| + (b202ea4e, which answers rev 7.11's eight notes and R11-2 to R11-5) |
| + and the library E at 34224a29; §22.18 has every disposition. |
| + **`holder.admissions`** replaces `op.journal.writers`: the record of |
| + admissions lives in the holder, so it survives every operation, |
| + release and new operation, trimmed to eight covered records and never |
| + an uncovered one or the current predecessor. **An admission's |
| + predecessor is always the last record there** (session, box, |
| + generation), never the generation an operation chose for a restore |
| + (R11-4): a clean return resets `holder.generation` to the source's |
| + for the restore, but the predecessor is still the target's writer |
| + (INV-16). **`Coverage`** `""` | `sealed` | `clean-return` replaces |
| + `BaselineCoversPredecessor`: only `""` with no certificate records |
| + `writes_lost`, and the record always names its coverage; a clean |
| + rollback with `src_covered` declares nothing. **`PublishGeneration`** |
| + replaces `QueueGenerationRetire`: the one retirement path, bound to |
| + the observed operation and phase, legal while serving and inside any |
| + operation a writer runs in (R11-5), chores with `op = op.id` inside an |
| + operation and `session:<n>` while serving, only of predecessors in |
| + `holder.admissions`; `""` and `"@root"` are one origin, so nothing |
| + retires an adopted host's replica before a cold admission has |
| + published a successor (R11-2). **The sweep reads an absent |
| + `generation.json` as the origin** (R11-1), as the residue oracle does, |
| + so an unfinished admission's chain protects an adopted host's replica; |
| + witness `wOriginSwept`. **The final oracle runs the recovery |
| + admission for real** when the serving session is uncertified and |
| + judges by what it declared; an admission that cannot run is counted as |
| + an unverified prospective declaration, never exempted (R10-6). **A |
| + probe attempt's five app restarts share its 30 s readiness window** |
| + (§7.7): the fifth failure or the window ends the attempt and the |
| + operation counts one of its three budgeted attempts; a probe never |
| + marks the host failed. §5.1, §7.8 and the authoritative-region table |
| + carry no instruction left that assigns `holder.generation` outside a |
| + cold admission's CAS or the clean return (R10-3). Rule |
| + `clean-return-identity` (96 in all); witnesses `wCleanReturnIdentity` |
| + and `wOriginSwept` (59 in all). Results in §14.2.3 and §14.2.5. |
| - **Rev 7.11** answers **joint round 10** (`CODEX-FINDINGS-JOINT-R10.md`, |
| cited "R10-n") and is written against **claim spec rev 6.10** |
| @@ -791,8 +829,11 @@ is `0000/0000000000000008-0000000000000008.ltx`. Rev 7.5 wrote |
| one in this spec and in the model. |
| The claim names the current one, **`holder.generation`** (CC18): written |
| -by the commit's claim CAS (§7.9), by a push's probe CAS (F7), and by a |
| -dirty rollback's source probe (§7.8). Restore reads it from the same fresh |
| +only by a cold admission's `AdmitWriter` CAS (a landing's, a push's or a |
| +dirty rollback's probe into its prepared generation, every recovery into |
| +a fresh one, §7.14) and by a clean rollback's return CAS, which names the |
| +source's generation again for the restore (§7.8; R10-3: no commit, |
| +`probed` or install phase writes it). Restore reads it from the same fresh |
| admission read as `holder.location` (claim C3a). |
| **The restore contract (J2-R2-1; R3-1; R4-1).** A restore reads |
| @@ -1028,32 +1069,43 @@ fails there first (§14.2.6). |
| 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). |
| + resulting gen`, `holder.writer_box = this box`, and a record in |
| + **`holder.admissions`** `{session, box, generation, predecessor: |
| + {session, box, generation, stamp}, mode, coverage, covered, |
| + writes_lost?}` (claim rev 6.12; the library's `AdmissionRecord`). |
| + **The predecessor is the last record there**, with its own session, |
| + box and generation; it never comes from the holder's fields, which a |
| + clean return has reset to the source's generation for the restore |
| + while the predecessor is still the target's writer (R11-4; rev 7.11 |
| + journalled the target's session and box with the source's |
| + generation, a writer that never was; INV-16). `holder.admissions` |
| + lives in the holder, so it survives every operation transition, |
| + release and new operation; it is trimmed to the last eight covered |
| + records, never an uncovered one or the current predecessor. The |
| + admission **never replaces the operation**: kind, id, phase, |
| + participants, obligations and the rest of the journal are kept. |
| - **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. |
| + release not live) waits and counts no attempt. For a **serving |
| + wake**, 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). For a **probe**, |
| + the restarts share the probe attempt's 30 s readiness window (§7.7): |
| + the fifth failure or the window's end, whichever comes first, ends |
| + the attempt, the operation counts one of its budgeted attempts, and |
| + the host is not marked failed. 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 waits |
| + between attempts total 15 s (1 + 2 + 4 + 8); each attempt's own |
| + start and readiness time is on top, so five attempts are not a |
| + bound on a serving wake's duration, only on its count. 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 |
| @@ -1101,14 +1153,25 @@ fails there first (§14.2.6). |
| 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 |
| + every page), there is nothing to declare: the admission's |
| + **`Coverage`** is `sealed` (claim rev 6.12, replacing rev 6.9.1's |
| + `BaselineCoversPredecessor`); the comparison is against the seal's |
| + own position, never a TXID from another region. A clean rollback's |
| + return with `src_covered` (§7.8) is covered too, `clean-return`: the |
| + unchanged target and the source's complete replica establish |
| + preservation, and the source's re-admission declares nothing. The |
| + coverage speaks for the **target's probe session** and for the |
| + **source's cut session** (`cut.session`, journalled at the stop) |
| + only: a later session of the recovered source that dies uncertified |
| + is declared like any other, and a return made clean only by a |
| + declared-lost target is not covered at all. Only |
| + coverage `""` with no certificate records `writes_lost`, and the |
| + record always names its coverage, certified or not. 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 has coverage `""` and 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 |
| @@ -1138,25 +1201,47 @@ fails there first (§14.2.6). |
| 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 |
| + publication**, through one **`PublishGeneration(observedOpID, |
| + observedPhase, observedSession, publishedGeneration, region, |
| + newID)`** CAS (claim rev 6.12, replacing `QueueGenerationRetire`): |
| + bound to the observed operation and phase like the admission, legal |
| + while serving and inside any operation a writer runs in (a restarted |
| + landing probe, a rollback's or a revert's source; R11-5), it marks |
| + every admission record up to the published generation covered and |
| + queues one `park-generation` per dead generation, deduplicated: the |
| + predecessor; behind a lagging marker, every 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 in `holder.admissions` not yet covered (its writer died |
| + after its marker landed and before the CAS). Its chores carry `op = |
| + op.id` inside an operation and `op = "session:<holder.session>"` |
| + while serving. **Retirement happens only through it, and only of |
| + predecessors recorded in `holder.admissions`** (R11-2). An adopted |
| + legacy host's generation is the location root itself, named by the |
| + sentinel **`"@root"`** so a chore can name it; `""` and `"@root"` |
| + are one origin, so nothing retires the active legacy replica before |
| + a cold admission has created a successor and published 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, R11-3). **Coverage is per region**: a record is |
| + covered when its predecessor's chore was queued in the region that |
| + holds the predecessor's objects (or the predecessor holds none |
| + anywhere); a predecessor whose objects live in another region (a |
| + move's source generation, seen by the target's publication whose |
| + chain walks back through it) stays uncovered for that region's next |
| + `PublishGeneration`, since a chore queued from the target's region |
| + would park nothing there and one queued into the source's region |
| + would park a generation the rollback may still need. A dead |
| + generation holding nothing yet still gets its chore in the publishing |
| + region: a dead writer's late upload or certificate may land in it |
| + within the chore's horizon. 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 |
| + - **A marker that lags `holder.generation`** (an absent marker is the |
| + origin `""`, for the sweep as for the restore, R11-1) is read through |
| + `holder.admissions`: 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 |
| @@ -1330,21 +1415,25 @@ is the region of the holder's current installation: |
| |---|---| |
| | `serving`, `pushing` | `op.exec`'s region | |
| | `moving` (before the flip), `reverting` | the source's region | |
| -| `landing` (after the flip, before the commit) | the source's region: `holder.generation` is still the pre-move generation, and the target's new generation is not yet named | |
| -| `landing` after the commit, until the claim releases | the target's region | |
| -| `restoring`, clean | the source's region | |
| -| `restoring`, dirty, until the source's probe names the return generation | the source's region | |
| -| `restoring`, dirty, after the source's probe | the source's region, for the return generation | |
| +| `landing` after the flip, before the target's probe is admitted | the source's region: `holder.generation` is still the pre-move generation, and the target's prepared generation is not yet named | |
| +| `landing` from the target's probe's cold admission on, committed or not | the target's region: `holder.generation` is the generation that admission chose, the prepared one or, for a restarted probe, a fresh one restored from it (§7.14; rev 7.11's row said "before the commit", R10-3) | |
| +| `restoring`, clean, from the return CAS on | the source's region: the return CAS named the source's generation again for the restore, and the source's re-admission moves to a fresh generation there | |
| +| `restoring`, dirty, until the source's probe is admitted | the source's region, for the pre-move generation; the return generation is built there but not yet named | |
| +| `restoring`, dirty, from the source's probe's cold admission on | the source's region, for the return generation | |
| | `creating`, `deleting`, `parking`, `purging`, free | none: nothing is live | |
| **The start check (INV-4, J2-R2-8).** Before every spawn (`Start`, `Seed`, |
| `ProbeWake`), the activator requires: |
| 1. the box's own `<location>generation.json` (absent is origin) to name |
| - **the generation the claim expects**: `holder.generation` for an |
| - ordinary wake, or, for a probe, the generation the probing operation is |
| - installing (the move id, the rollback id, the push id); and its |
| - incarnation to be the holder's; |
| + **the generation the claim expects**: `holder.generation`, as the |
| + admission's CAS left it, for every start; a probe's first admission |
| + publishes the operation's prepared generation (the move id, the |
| + rollback id, the push id) and a restarted probe's a fresh generation |
| + restored from it (§7.14; rev 7.11's clause named the prepared |
| + generation for every probe, R10-3); a lagging marker is read through |
| + `holder.admissions` (§5.1 step 9); and its incarnation to be the |
| + holder's; |
| 2. `.files-gen`, when the files directory exists, to name the same |
| generation and incarnation; |
| 3. `<dbPath>.gen` to name the same generation and location. A warm |
| @@ -2078,7 +2167,18 @@ only while the claim names this box as execution holder: |
| otherwise) answers 200 to 399 within 30 s (`backend_exec.go:36`); |
| - a 20 s settle, the process still running, and a second request; |
| - up to three attempts, and never more than T11 admitted for this |
| - budget (§7.3, R3-7). |
| + budget (§7.3, R3-7). **One attempt is one cold admission** (§7.14): its |
| + app may be restarted under the retry policy of §5.1 step 9 within the |
| + attempt's **30 s readiness window**, which runs from the first start |
| + (the waits total 15 s, each start's own time is on top), and the fifth |
| + failure or the window's end, whichever comes first, ends the attempt; |
| + the next attempt, if the budget allows one, is a new cold admission |
| + into a fresh generation restored from the dead attempt's. A probe never |
| + marks the host failed; the operation's rollback (or `stuck`) is its |
| + outcome. The budget's three attempts and the policy's five restarts are |
| + different things: at most three admissions, each with at most five |
| + starts inside 30 s. The absolute `cut_deadline` (§7.4) still bounds the |
| + whole. |
| The probe's activator entry is **held**: `RetireExcept` |
| (`internal/edge/edge.go:924`, `activator.go:2624`) keeps it, and the edge |
| @@ -2119,10 +2219,10 @@ because, until then, a source failure might need the target's state again. |
| | phase | action | replay | |
| |---|---|---| |
| | `waiting` | until `released` (clean) or `returned` (dirty) and the claim's execution holder is `none` | | |
| -| `claimed` | CAS the claim: `op.kind = restoring`, execution holder = this box, citing the target's evidence (§19 K4), **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` | | |
| +| `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); **clean, with `src_covered`: `holder.generation = op.journal.src_gen`**, the source's generation again, for the restore. The predecessor of the source's re-admission is still the target's writer, the last record of `holder.admissions` (claim rev 6.12, R11-4), and its coverage is `clean-return`: nothing is declared. 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 (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 | |
| +| 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 probe's cold admission** (§7.14), which names the return generation in `holder.generation`, issues the **new `holder.stamp` `R`** in the same write (`KeepStamp` false: a writer was admitted since `S` was issued), 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.11's row still said the `probed` CAS wrote them, R10-3). 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` | | |
| @@ -2369,9 +2469,13 @@ rollback's return generation) is built by the operation's install phases |
| and becomes `holder.generation` at its probe's cold admission, never |
| before; the flip and the commit move no generation (rev 7.9's commit did). |
| A clean rollback's **return CAS names the source's generation again** |
| -(`op.journal.src_gen`, recorded at the flip), since the target's probe had |
| -moved `holder.generation` to the target's and the target wrote nothing; |
| -the source's probe then restores from its own region's remote of it. |
| +(`op.journal.src_gen`, recorded at the flip; only with `src_covered`, |
| +§7.8), since the target's probe had moved `holder.generation` to the |
| +target's and the target wrote nothing; the source's probe then restores |
| +from its own region's remote of it, is covered `clean-return`, and |
| +journals the **target's writer** as its predecessor, the last record of |
| +`holder.admissions`, never the holder's reset fields (claim rev 6.12, |
| +R11-4, INV-16). |
| **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, |
| @@ -2379,13 +2483,13 @@ 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; `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 | |
| +| 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`; `Coverage` `sealed` for a prepared generation from a `from_db` seal, `clean-return` for a clean rollback's return with `src_covered`, else `""`; a lagging `generation.json` is read through `holder.admissions` (below) | nothing happened | |
| +| **`AdmitWriter`** | the CAS of §5.1 step 9, **first**: session, writer_box, the `holder.admissions` record with the last record as its predecessor; cold: generation, stamp unless kept, `writes_lost` only for coverage `""` with no certificate; **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 | |
| +| 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 `PublishGeneration`** (§5.1 step 9), bound to the operation and phase it observed, legal in `serving` and in every operation a writer runs in: the records up to the new generation are covered and one `park-generation` per dead generation is queued, the predecessor's, the chain's and any uncovered record's | 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 | | |
| @@ -2393,7 +2497,7 @@ An admitted writer that dies between its CAS and its marker leaves |
| `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 |
| +box or another `op.exec` box, reads the lag through `holder.admissions` |
| (§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 |
| @@ -2406,13 +2510,12 @@ 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 |
| +`holder.admissions` lives in the holder, so an admission unfinished at a |
| +release (an abort released over a source admitted a tick earlier) stays |
| +explained through the next operation. A marker that lands after its |
| +writer died, before the writer's `PublishGeneration`, leaves the |
| +predecessor unretired: the next admission's `PublishGeneration` retires |
| +the predecessor of every record not yet 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. |
| @@ -2684,6 +2787,16 @@ 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.12: the final oracle runs the recovery.** When the run is |
| +quiescent with the serving host at rest after a session that did not |
| +certify, the final oracle no longer exempts the acknowledged, unuploaded |
| +writes as a prospective declaration (R10-6: that recorded and alerted |
| +nothing, with `writes-lost` off too). It wakes the host, runs the cold |
| +admission for real, drives its chores to quiescence, and judges the |
| +database by what the admission declared; a recovery that cannot run |
| +within the bound is counted (`final: unverified prospective |
| +declaration`) and the local check is skipped for it, never exempted. |
| + |
| **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 |
| @@ -3267,6 +3380,74 @@ 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.12: joint round 11 and claim rev 6.12.** |
| + |
| +- **`holder.admissions` (claim rev 6.12).** `holder.Admissions |
| + []admissionRecord{Session, Box, Gen, Predecessor, Mode, Coverage, |
| + Covered, Lost, LostSrc}` replaces `op.Writers`; the release and the |
| + move's and push's start carry nothing. `lastAdmission(holder)` is the |
| + next admission's predecessor; `admitCommit` journals it (session, box, |
| + generation) and INV-16 refuses a record whose predecessor is not the |
| + last admitted writer. `PublishGeneration` trims covered records beyond |
| + the last eight; an uncovered record and the newest are never trimmed. |
| +- **Coverage (R11-4).** `admitInput.Coverage` `""` | `"sealed"` (a |
| + prepared generation from a `from_db` seal) | `"clean-return"` (a |
| + rollback with `DirtyKnown && !Dirty && SrcCovered`, the source |
| + re-admitted into its own generation, and no declared-lost target); |
| + `writes_lost` only for `""` without a certificate. Rule |
| + `clean-return-identity` (the mutation takes the predecessor from the |
| + holder's fields and gives the clean return no coverage); witness |
| + `wCleanReturnIdentity`: a probed target that wrote nothing, a clean |
| + rollback, the source's re-admission journals the target's writer and |
| + declares nothing; under the mutation INV-16. `dirty-return`'s named |
| + failure is INV-2 local at the final recovery: treated as clean with the |
| + source's replica covering the stop, the return is covered and declares |
| + nothing, and the target's write is gone from the serving database. |
| +- **`PublishGeneration` (R11-5).** `publishGeneration(b, c, observedOpID, |
| + observedPhase, session, published, region, newID, dead)` replaces |
| + `queueGenerationRetire`: bound to the observed `op.id` and phase like |
| + the admission, legal in serving and in every operation kind, its |
| + chores carry `op = op.id` inside an operation and `session:<n>` while |
| + serving; the marker stage and the lag path's republish call it; |
| + `uncovered` reads `holder.admissions`. |
| +- **The absent marker is the origin (R11-1).** `deadGeneration` reads a |
| + missing `generation.json` as `""` before testing the chain, as |
| + `residueOf` always did; witness `wOriginSwept` (under `baseline-live`): |
| + an adopted host's origin replica, a cold admission that crashes before |
| + its first upload, the ordinary sweep for three horizons with no wake, |
| + then the recovery; under the mutation the sweep parks the origin and |
| + the recovery restores nothing (INV-2 local). |
| +- **The final oracle runs the recovery (R10-6).** `final()` wakes an |
| + at-rest, uncertified serving host, drives the cold admission and its |
| + chores to quiescence, then judges; `final: recovery admission run` and |
| + `final: unverified prospective declaration` count the cases. It found |
| + a false coverage at once: a return made clean by a declared-lost target |
| + was covered `clean-return` and the target's write went undeclared |
| + (the `lost-return-park` witness under no mutation). |
| +- **A probe attempt's window (§7.7).** `openState.startedAt`, |
| + `probeStartWindow = 30`: in a probe, the fifth failed start or the |
| + window's end abandons the attempt (`probeAttemptFailed` counts one |
| + budgeted try: a landing rolls back at three, a revert or a rollback's |
| + source is stuck at nine), the environment wait included; a probe never |
| + marks the host failed. `recovery-current-inputs`'s witness reaches |
| + `stuck` through this path now. |
| +- **Adoption names the writer (R11-3).** Unchanged since rev 7.11 |
| + (`WriterBox: eb.ID` at `adopt`). |
| +- **Model faults found and fixed this round** (all before the final |
| + numbers; the 100,000-seed baseline found them): a `clean-return` |
| + coverage applied to a later session of the recovered source, whose |
| + uncertified death then went undeclared (seed 95491: the coverage speaks |
| + for the target's probe session and the source's cut session only, |
| + `op.CutSession`); `PublishGeneration` queued a dead generation's chore |
| + in the publishing region alone, so a move's source generation covered |
| + by the target's publication was never parked in the source's region |
| + (seeds 33646 and 40148: coverage is per region, and a chore is queued |
| + only where the generation holds objects; a first fix that queued chores |
| + into the other regions parked the source's own generation under a |
| + rollback, seeds 1036 and 1296 / 3,000, and was withdrawn; an empty dead |
| + generation still gets its chore, since a dead writer's late upload or |
| + certificate may land in it, seeds 15273 and 20810 / 30,000). |
| + |
| **Rev 7.11: joint round 10 and claim rev 6.10.** |
| - **The admitting CAS first (R10-1, claim rev 6.10).** `spawn` decides |
| @@ -3761,6 +3942,38 @@ 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.12, on the final model (claim rev 6.12: `holder.admissions`, |
| +`Coverage`, `PublishGeneration`, the origin's absent marker, the final |
| +recovery admission, a probe attempt's window): 30,000 seeds, zero |
| +violations; 100,000 seeds, zero violations** (673 s and 2231 s). |
| +Across the 100,000 seeds: 150,033 completed operations, among them |
| +71,784 cold and 16,875 warm admissions (13,689 |
| +covered `sealed`, 919 covered `clean-return`; |
| +20,049 clean closes, 1,568 closes refused as |
| +uncertain, 0 stale certificates, 1,063 wakes |
| +that waited for a draining writer, 56,566 local databases |
| +purged, 4,443 starts that waited for a failed purge, |
| +57,206 writes_lost records declaring 8,884 acknowledged |
| +writes lost, 29,236 full first uploads, 108,295 start |
| +steps that waited for their marker, 663 markers published |
| +again, 3,883 probes restarted, 541 probe |
| +attempts ended by their window or fifth failure, 2,324 app |
| +starts that failed and were retried within their session, |
| +0 hosts marked failed by the retry policy (a probe no longer marks one, and no serving wake failed five times in these seeds), |
| +111 seals whose source replica was short and |
| +51 returns that carried the seal; 9,326 final |
| +recovery admissions run by the oracle, 0 unverified), |
| +825 completed moves, 2,199 clean and |
| +101 dirty rollbacks, 356 pre-flip reverts, |
| +287 declared losses, 25,894 pushes, 89,204 |
| +delete-park-free cycles and 4,945 lost disks (3,672 |
| +with a crash); 9,418 LTX compactions, 6,608 snapshot |
| +rotations, 564 level-0 upload retries, 30,446 |
| +anchors; 26,101 local stamp records lost and re-initialized; |
| +49,321 requests completed after `H`; 33,312 staging |
| +signatures refused as stale; 30,514 creates restarted on a |
| +412. Every oracle left the system unchanged. |
| + |
| **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, |
| @@ -4039,37 +4252,56 @@ 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.11 model (bd1587a1), with the strict classification, |
| +on the final rev 7.12 model (af9b89ed), 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 48 rules that have them. A rule is caught |
| +same mutation, for the 49 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 |
| +section does too. The model has **96 rules**: rev 7.11's 95 plus |
| +`clean-return-identity` (claim rev 6.12, R11-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.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. |
| +`HOSTLIFE_WITNESS=<rule>` replays a witness with its trace. Rev 7.11's |
| +counts are in the rev 7.11 spec (ec982436). **Every table below is |
| +regenerated from the retained verdict files** (R9-6; |
| +`~/.cache/nearest-region/rev712-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, 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 alone by the sweep at 3,000 seeds | 64 | |
| +| caught alone by the sweep at 30,000 (and by their witness, where one exists) | 10 (`dirty-return`, `evidence-whole-tree`, `hostguard`, `lost-return-park`, `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) | 2 (`baseline-live`, `declare-lost-compute`) | |
| +| caught alone by their witness only; the sweep misses them at 30,000 | 7 (`admit-before-start`, `close-evidence`, `close-waits`, `closed-marker`, `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 | 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.12 moved.** The new rule `clean-return-identity` |
| +13 / 3,000, 125 / 30,000, 387 / 100,000 (a clean rollback after a probed target is a |
| +schedule the sweep reaches; under the mutation the false predecessor is |
| +INV-16 at the source's re-admission). The final oracle's real recovery |
| +and the probe window moved a few counts: `dirty-return` |
| +0 / 3,000, 11 / 30,000, `lost-return-park` 0 / 3,000, 29 / 30,000, 74 / 100,000, |
| +`writes-lost` 14 / 3,000, 125 / 30,000, 411 / 100,000, `baseline-live` 0 / 3,000, 0 / 30,000, 2 / 100,000, |
| +`seal-return` 0 / 3,000, 12 / 30,000, 27 / 100,000, `recovery-current-inputs` |
| +40 / 3,000, `hostguard` 0 / 3,000, 2 / 30,000, 2 / 100,000, |
| +`stale-hold-release` 0 / 3,000, 14 / 30,000, 47 / 100,000, `strict-spawn` |
| +0 / 3,000, 1 / 30,000, 11 / 100,000; `dirty-return` and `lost-return-park` |
| +now need 30,000 seeds (the final oracle's recovery declares what the |
| +hypothetical declaration used to exempt, and the serving database is |
| +judged by it), and `newest-l0` fell back to witness-only (0 / 100,000; |
| +1 / 100,000 on rev 7.11). The witness-only rules keep their shape: |
| +`admit-before-start` witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000, `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; the pair `admit-bind-op` |
| ++ `claim-cas-opid` 0 / 30,000, 0 / 100,000; the admission |
| +four 183 / 30,000, 644 / 100,000. |
| + |
| **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 |
| @@ -4205,16 +4437,16 @@ 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 | | 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 | |
| +| `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 | | 1 / 3,000, 10 / 30,000, 42 / 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 | | 0 / 3,000, 29 / 30,000, 74 / 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, 5 / 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, 6 / 30,000 | |
| | `markers-last` (R2-6) | the source has a registered timer; the target's agent crashes between extracting the files and writing the marker | **violated**: INV-2, the timer is lost | | 0 / 3,000, 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 | |
| +| `dirty-return` (INV-2) | the target writes during its probe and replicates; the rollback is dirty and the return lane carries the write | **violated**: treated as clean with the source's replica covering the stop, the return is covered `clean-return`, nothing is declared and the serving database lacks the target's write (INV-2 local at the final recovery; rev 7.11 saw INV-15 at the declaration) | | 0 / 3,000, 11 / 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 | |
| @@ -4222,37 +4454,39 @@ witness to hold there; each witness violates with the failure it names. |
| | `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) | | 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 | |
| +| `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) | | 342 / 3,000, 3,133 / 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 | 337 / 3,000, 3,042 / 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 | | 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 | |
| +| `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, 16 / 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) | | 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 | |
| +| `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) | | 59 / 3,000, 593 / 30,000, 1,960 / 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) | | 12 / 3,000, 121 / 30,000, 434 / 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, 104 / 30,000, 361 / 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, 773 / 30,000, 2,587 / 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) | | 10 / 3,000, 105 / 30,000, 388 / 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 | | 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 | |
| +| `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) | | 704 / 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 | |
| +| `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) | | 2 / 3,000, 22 / 30,000, 63 / 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 | | 710 / 3,000, 6,840 / 30,000, 23,078 / 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) | | 41 / 3,000, 389 / 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, 391 / 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 | | 11 / 3,000, 122 / 30,000, 395 / 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 | | 14 / 3,000, 125 / 30,000, 411 / 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 | |
| +| `clean-return-identity` (claim rev 6.12, R11-4) | a move's target is probed and writes nothing; the seal recorded `src_covered`; a clean rollback; the source's re-admission | held: the record's predecessor is the target's writer and its coverage `clean-return`; nothing is declared | **violated** under the mutation: INV-16, the record names the target's session and box with the source's generation, a writer that never was | 13 / 3,000, 125 / 30,000, 387 / 100,000 | |
| +| `baseline-live` (R11-1), a second scenario | an adopted host's origin replica with durable writes and no `generation.json`; a cold admission crashes before its first upload; the ordinary sweep runs for three horizons; the recovery | **violated**: the sweep parks the origin 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, 12 / 30,000, 27 / 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` |
| @@ -4277,53 +4511,54 @@ 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: 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 ‡). |
| +**Caught alone: 83 of 96** (64 by the sweep at 3,000; 10 by the sweep at |
| +30,000, marked †; 2 at 100,000, |
| +marked ††; 7 by their witness alone, marked ‡). |
| | rule | seeds failing | | rule | seeds failing | |
| |---|---|---|---|---| |
| -| `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` | 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` | 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 | |
| +| `abort-target-owner` | 940 / 3,000 | | `admission-registration` | 32 / 3,000 | |
| +| `admit-before-start` ‡ | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 | | `admit-everywhere` | 710 / 3,000, 6,840 / 30,000, 23,078 / 100,000 | |
| +| `anchor-acked` | 13 / 3,000, 104 / 30,000, 361 / 100,000 | | `baseline-live` †† | 0 / 3,000, 0 / 30,000, 2 / 100,000 | |
| +| `build-completion` | 704 / 3,000 | | `cancelled-creates` | 383 / 3,000 | |
| +| `claim-never-deleted` | 4 / 3,000, 57 / 30,000 | | `claim-op-exclusive` | 82 / 3,000 | |
| +| `clean-return-identity` | 13 / 3,000, 125 / 30,000, 387 / 100,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` | 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` † | 0 / 3,000, 11 / 30,000 | |
| +| `evidence-from-state` | 2,610 / 3,000 | | `evidence-whole-tree` † | 0 / 3,000, 7 / 30,000 | |
| +| `fence-by-installation` | 342 / 3,000, 3,133 / 30,000 | | `fence-etag` | 26 / 3,000, 229 / 30,000 | |
| +| `fence-stamp` | 337 / 3,000, 3,042 / 30,000 | | `files-carried` | 33 / 3,000 | |
| +| `floor-boot-recovery` | 2,576 / 3,000 | | `fresh-admission` | 10 / 3,000 | |
| +| `fresh-incarnation` | 42 / 3,000 | | `generation-conditional` | 1 / 3,000, 10 / 30,000, 42 / 100,000 | |
| +| `hostguard` † | 0 / 3,000, 2 / 30,000, 2 / 100,000 | | `legacy-discovery` | 273 / 3,000, 2,739 / 30,000 | |
| +| `live-set-region` | 2 / 3,000, 16 / 30,000 | | `location-per-incarnation` | 28 / 3,000, 359 / 30,000, 1,182 / 100,000 | |
| +| `lost-quarantine` | 1 / 3,000, 6 / 30,000 | | `lost-return-park` † | 0 / 3,000, 29 / 30,000, 74 / 100,000 | |
| +| `markers-last` † | 0 / 3,000, 5 / 30,000 | | `newest-l0` ‡ | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 | |
| +| `obligations-block-ops` | 31 / 3,000 | | `orphan-no-deadline` | 41 / 3,000 | |
| +| `orphan-order` † | 0 / 3,000, 1 / 30,000 | | `park-all-versions` | 568 / 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` | 22 / 3,000, 232 / 30,000 | | `purge-journal` | 1,889 / 3,000 | |
| +| `purge-reserve-first` | 2,143 / 3,000 | | `quiet-before-ack` | 178 / 3,000 | |
| +| `recovery-current-inputs` | 40 / 3,000 | | `recovery-generation` | 10 / 3,000, 105 / 30,000, 388 / 100,000 | |
| +| `recovery-pass` | 2,482 / 3,000 | | `registration-recovery` | 2,118 / 3,000 | |
| +| `remote-baseline` ‡ | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 | | `restore-anchor` | 59 / 3,000, 593 / 30,000, 1,960 / 100,000 | |
| +| `restore-by-generation` | 136 / 3,000 | | `restore-gap-closed` ‡ | witness; sweep 0 / 3,000, 0 / 30,000 | |
| +| `restore-overlap` † | 0 / 3,000, 2 / 30,000 | | `retirement-ids` | 463 / 3,000 | |
| +| `return-stamp` | 74 / 3,000, 773 / 30,000, 2,587 / 100,000 | | `revalidate-before-effect` | 17 / 3,000, 188 / 30,000 | |
| +| `revert-journal` | 12 / 3,000 | | `rollback-journal` | 1 / 3,000, 9 / 30,000 | |
| +| `root-advance` | 12 / 3,000, 121 / 30,000, 434 / 100,000 | | `sdk-no-resign` | 9 / 3,000 | |
| +| `seal-by-version` | 1 / 3,000, 6 / 30,000 | | `seal-return` † | 0 / 3,000, 12 / 30,000, 27 / 100,000 | |
| +| `sign-at-check` | 10 / 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, 14 / 30,000, 47 / 100,000 | | `start-check` | 16 / 3,000, 218 / 30,000 | |
| +| `start-check-claim-gen` | 15 / 3,000, 181 / 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` | 18 / 3,000 | |
| +| `timer-canonical` | 3 / 3,000 | | `timer-freeze` | 2 / 3,000, 21 / 30,000 | |
| +| `valid-ltx` | 41 / 3,000, 391 / 30,000 | | `writer-session` | 2 / 3,000, 22 / 30,000, 63 / 100,000 | |
| +| `writes-lost` | 14 / 3,000, 125 / 30,000, 411 / 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` |
| @@ -4341,16 +4576,16 @@ subset in the gate. |
| | `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-claim-gen` + `exec-writer` | 183 / 30,000, 644 / 100,000 | `exec-admission` 0 / 3,000, `hold-op-open` 0 / 3,000, `start-check-claim-gen` 15 / 3,000, 181 / 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` 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 | |
| +| `claim-cas-opid` + `revalidate-before-effect` | 901 / 30,000 | `claim-cas-opid` 0 / 3,000, `revalidate-before-effect` 17 / 3,000, 188 / 30,000 | violated | a stale step destroys a store | |
| +| `strict-spawn` + `evidence-whole-tree` | 88 / 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,298 / 30,000 | `touched-incomplete` 0 / 3,000, `legacy-discovery` 273 / 3,000, 2,739 / 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 | |
| +| `fence-stamp` + `hostguard` (no longer combination-only) | 3,994 / 30,000 | `fence-stamp` 337 / 3,000, 3,042 / 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 |
| @@ -4770,6 +5005,33 @@ 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.11 (63255a3c) and 6.12 (b202ea4e), after joint round 11: |
| +no change requested, three notes.** Rev 6.11 answered rev 7.11's eight |
| +notes (the retry limit confirmed; the chain generalized to a run of |
| +admissions; `holder.admissions` in the holder; `PublishGeneration` |
| +replacing `QueueGenerationRetire`; the clean return only with |
| +`src_covered`; `BaselineCoversPredecessor` only for a `from_db` seal; a |
| +new agent stops a running app; the lost box's timers, the source's cut |
| +session and adoption's `writer_box`). Rev 6.12 answers R11-2 to R11-5: |
| +retirement only through `PublishGeneration` and only of predecessors in |
| +`holder.admissions`, `""` and `"@root"` one origin; adoption sets |
| +`writer_box`; the predecessor is always the last record and admission |
| +carries `Coverage` `""` | `sealed` | `clean-return`; |
| +`PublishGeneration(observedOpID, observedPhase, observedSession, |
| +publishedGeneration, region, newID)` bound to the operation and phase, |
| +legal in serving and in move kinds. Rev 7.12 encodes all of it (§5.1 |
| +step 9, §7.8, §7.14, §14.2.2). Notes for platform-1e |
| +(`moves-claim-questions.md`, rev 7.12 heading): **(1)** a return made |
| +clean only by a declared-lost target is **not** `clean-return`: the |
| +target may have written and its session is uncovered, so `writes_lost` |
| +is recorded for it (and the source's cut session when `src_covered` is |
| +false); **(2)** a probe attempt's app restarts share the attempt's 30 s |
| +readiness window, the fifth failure or the window ends the attempt, and |
| +a probe never marks the host failed (the retry policy's failed-host |
| +marking is a serving wake's); **(3)** when `PublishGeneration` queues |
| +several chores for one `newID`, the model names the second and later |
| +ones `<newID>-<generation>`; E's naming is the one to mirror. |
| + |
| **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 |
| @@ -5192,6 +5454,26 @@ 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.18 Joint round 11 (claim 3f916b05, moves rev 7.11 ec982436, model bd1587a1, library E 090fb7a2) |
| + |
| +Round 11 judged the admitting order sound and R10-1, R10-5, R10-7, R10-8 |
| +and R10-9 resolved; it found one P1 and four P2s and kept R10-2, R10-3 |
| +and R10-6 partly open. Claim rev 6.11 answered rev 7.11's notes and rev |
| +6.12 (b202ea4e) answers R11-2 to R11-5; the library E at 34224a29 gains |
| +`Holder.Admissions`, `Coverage`, `PublishGeneration` and adoption's |
| +`writer_box`. |
| + |
| +| finding | rev 7.12 | |
| +|---|---| |
| +| R11-1 (P1) the model's sweep skipped the chain protection when `generation.json` was absent, so an adopted origin replica could be parked under an unfinished admission | the sweep reads an absent marker as the origin, as the residue oracle does (§5.1 step 9, §6.4); witness `wOriginSwept` (origin, an unfinished admission, three horizons of ordinary sweeps, the recovery) | |
| +| R10-3 leftovers (B) §5.1 said the commit writes `holder.generation`; the dirty-return row said `probed` writes generation and stamp; the authoritative-region table and the start check were stale | one rewrite: `holder.generation` is written only by a cold admission's CAS and the clean return (§5.1); the dirty install row names the probe's admission; the region table follows the target's or the source's admission; the start check expects the generation the admission chose (§5.1) | |
| +| R11-4 (P2) a clean return journalled {target session, target box, source generation}, and declared a false loss | the predecessor is the last record of `holder.admissions` (INV-16); `Coverage` `clean-return` for a clean rollback with `src_covered` records nothing; rule `clean-return-identity`, witness `wCleanReturnIdentity` (the identity tuple and the absence of a declaration) | |
| +| R10-6 (C) the final oracle exempted writes a future admission would declare | the oracle runs the recovery admission for real and judges by what it declared; a recovery that cannot run is an unverified prospective declaration, counted, never exempted (§14.2.1); it found the declared-lost return's false coverage at once | |
| +| R11-5 (P2) publication-time retirement during operations could not use E's serving-only helper | `PublishGeneration(observedOpID, observedPhase, observedSession, publishedGeneration, region, newID)` bound to the operation and phase, legal in serving and in every operation a writer runs in, chores with `op = op.id` inside an operation (§5.1 step 9, §7.14) | |
| +| probe retry deadline | one attempt is one cold admission; its five restarts share the 30 s readiness window (the waits total 15 s), the fifth failure or the window ends the attempt and the operation counts one of its three budgeted attempts; a probe never marks the host failed (§5.1 step 9, §7.7) | |
| +| R11-2, R11-3 (E) | mirrored: retirement only through `PublishGeneration` of predecessors in `holder.admissions`, `""` and `"@root"` one origin; adoption's `writer_box` (already in the model since rev 7.11) | |
| +| the eight notes judged | all accepted in claim rev 6.11; the aggregate probe deadline defined above | |
| + |
| ### 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 |