amadan
spec: move-any-app rev 7.14, joint round 13 and claim rev 6.22
The model's park state is the claim's (R13-4): a persisted park scope on every remote chore, a free host's sweep as a holderless parking op freed by FreeAfterPark, session:<n> on a serving host, INV-20. Coverage in exactly four ways (R13-2): birth (warm; a pending whole-location park), publication over every entry with its precondition, CoverRegionPredecessors at the three park CASes, CoverParkedPredecessors for what the sweep parks. The run walk stated precisely (R13-1): a covered foreign link is passed over, a covered local baseline refuses and alerts; restoreCalc the reference; TestInterruptedCleanReturn. additional_writes_lost (R13-3). Six notes for the claim under the rev 7.14 heading. The evidence policy (Paul, 2026-10-06) in §14.2.1: the gate and one 3,000-seed mutation sweep per revision, serially and niced; baselines at 30,000 only; the deep runs once, at a pre-implementation checkpoint. Model 4ebfa0a5: 104 rules, 68 witnesses; 30,000 seeds clean (169 s); 100,000 seeds clean (1021 s, run before the policy); mutation sweep at 3,000: 90 caught, 14 expected misses, exit 0; 90 of 104 caught alone (69 by the sweep, 21 by witness). The 30,000 and 100,000 sweeps were stopped and are marked not run. Records in ~/.cache/nearest-region/rev714-sweeps/.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
1 file changed,
+524
−183
docs/superpowers/specs/2026-10-02-move-any-app-design.md+524 −183
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 4f6e7e7af..10fb74664 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,53 @@ |
| # Move any app or instance to another region: Phase 1, a safe single-instance move |
| -**Date:** 2026-10-05 |
| -**Revision:** 7.13. |
| +**Date:** 2026-10-06 |
| +**Revision:** 7.14. |
| + |
| +- **Rev 7.14** answers **joint round 13** (`CODEX-FINDINGS-JOINT-R13.md`, |
| + cited "R13-n") and is written against **claim spec rev 6.22** |
| + (0bf2f49f, which adopts rev 7.13's seven notes in rev 6.21 and |
| + answers R13-1 to R13-3; rev 6.15 and 6.16 added the persisted park |
| + scope and the holderless sweep), the library E on |
| + `feat/hostclaim-r713` at f0127321 and the generation selector F on |
| + `feat/hostclaim-genselect` at d7621a29; §22.20 has every disposition. |
| + **The model's park state is the claim's** (R13-4): every remote chore |
| + carries a persisted **park scope** `{location, incarnation, |
| + evidence_at, request_limit}`, bound in a CAS before its first step or |
| + at the sweep's queuing CAS, so a retry after an agent restart keeps the |
| + original evidence time and never restarts the horizon; a free host's |
| + at-rest sweep is a **holderless parking op** `{kind: parking, intent: |
| + {park_sweep: "v1"}}` with no exec and no holder, carrying only scoped |
| + remote chores, which blocks the successor create and frees the claim |
| + again in its last acknowledgement's CAS (`FreeAfterPark`); on a |
| + serving host the sweep's chores carry `session:<n>`; INV-20, a create |
| + never claims a host over an outstanding park. **Coverage, completely** |
| + (R13-2): an entry becomes covered in exactly four ways, at birth (a |
| + warm entry; an entry admitted under a pending whole-location park of |
| + its predecessor's region), by publication (which requires an entry to |
| + name the published generation and walks every entry in order, skipping |
| + covered ones), by `CoverRegionPredecessors` in the three |
| + whole-location-park CASes, and by `CoverParkedPredecessors(region, |
| + generations)` in the sweep's queuing and acknowledgement CASes, only |
| + for the generations the sweep parks. **The run walk, precisely** |
| + (R13-1): from `holder.generation` back to the marker's generation, a |
| + link whose generation keeps its objects in another region is passed |
| + over, covered or not; a link in this region must be uncovered, and a |
| + covered local generation reached as a needed baseline refuses the |
| + start and alerts; `restoreCalc` stays the reference and |
| + `TestInterruptedCleanReturn` walks R → T → S and R2 → R → T → S. |
| + **`additional_writes_lost`** (R13-3): the lost-target return's extra |
| + declarations, one per target session since the cut, unique by `(box, |
| + session)`, each alerted. Rules `persisted-park-scope`, |
| + `holderless-park`, `covered-baseline-refused` (104 in all); witnesses |
| + `wParkScopeSurvivesRestart`, `wFreeSweepVsCreate`, |
| + `wCoveredLocalBaseline` (68 in all). Results in §14.2.3 and §14.2.5. |
| + **The evidence policy** (Paul, 2026-10-06; §14.2.1): each revision |
| + runs the gate and one mutation sweep at 3,000 seeds, serially and |
| + niced; baselines at 30,000 only; the 100,000-seed baseline and the |
| + 30,000- and 100,000-seed mutation sweeps run once, at a final |
| + pre-implementation checkpoint, when Paul says so. Rev 7.14's 100,000 |
| + baseline ran before the policy and is reported; its deeper sweeps were |
| + stopped and are marked not run. |
| - **Rev 7.13** answers **joint round 12** (`CODEX-FINDINGS-JOINT-R12.md`, |
| cited "R12-n") and is written against **claim spec rev 6.14** |
| @@ -1228,7 +1274,18 @@ fails there first (§14.2.6). |
| continuation that died are two; the first's writes are durable only |
| in the lost target's region, and no return lane carries either's; |
| seed 33373 / 100,000, hidden until the session-scoped match of |
| - R12-1), each alerted. Only |
| + R12-1). **Representation** (claim rev 6.22 item 2, R13-3): the |
| + admission entry carries `writes_lost` (one, the predecessor's |
| + session) and **`additional_writes_lost`** (a list, the other target |
| + sessions since the cut, and the source's cut session when |
| + `src_covered` is false), each `{box, generation, session, |
| + remote_max_txid}`, unique by `(box, session)`; the caller supplies |
| + the list and the library records it in the admitting CAS; the |
| + admitting box raises **one alert per declaration** after the CAS |
| + and retries until delivered, and the console's durable loss record |
| + is the long-term copy, so trimming a covered entry never loses a |
| + declaration (the model: `admissionRecord.AdditionalWritesLost`, an |
| + alert each, INV-14 counts them). 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, |
| @@ -1271,16 +1328,19 @@ fails there first (§14.2.6). |
| 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 |
| - **walks every uncovered cold record** of `holder.admissions` (claim |
| - rev 6.14 item 5): a predecessor whose `predecessor_region` is `""` |
| - (it holds nothing anywhere) is covered with no chore; one that is |
| - the published, live generation again (a clean return's source |
| - generation, a republished lagging marker's) is **left uncovered** |
| - with no chore (item 5's first bullet covers it; covered, nothing |
| - would retire it once a later admission supersedes it, since that |
| - admission's predecessor is the last record and not the generation |
| - it restored from: seed 41914 / 100,000 left the source's generation |
| - as residue; a reading for the claim, §19.4); one whose objects are in the publishing |
| + **requires `holder.generation` to be the published generation and |
| + an entry to name it, then walks every entry of `holder.admissions` |
| + in order, skipping covered ones** (claim rev 6.22 item 5, R13-2; |
| + bounded by the list's length; warm entries are born covered, so it |
| + visits every uncovered cold entry): a predecessor whose |
| + `predecessor_region` is `""` (it holds nothing anywhere) is covered |
| + with no chore; one that is the published, live generation again (a |
| + clean return's source generation, a republished lagging marker's) |
| + is **left uncovered** with no chore (covered, nothing would retire |
| + it once a later admission supersedes it, since that admission's |
| + predecessor is the last record and not the generation it restored |
| + from: seed 41914 / 100,000 left the source's generation as residue; |
| + rev 7.13 note 6, adopted); one whose objects are in the publishing |
| `region` gets one deduplicated `park-generation` chore there and is |
| covered; one whose objects are in **another region** stays |
| uncovered, with no chore, and the walk goes on. The walk finds what |
| @@ -1304,29 +1364,36 @@ fails there first (§14.2.6). |
| 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 and recorded** (claim rev |
| - 6.13 and 6.14, R12-3): a record is covered when its predecessor's |
| - retirement is in hand in the region that holds the predecessor's |
| - objects. A predecessor whose objects live in another region (a |
| - move's source generation, seen by the target's publication) is |
| - **never queued into its region from here**, since the rollback may |
| - still need it (seeds 1036 and 1296 / rev 7.12; witness |
| - `wRollbackBaselinePreserved`); it is covered either by that |
| - region's own next publication or by |
| - **`CoverRegionPredecessors(op, phase, region)`**, composed into the |
| - CAS that queues that region's park of the whole location, which |
| - retires those generations wholesale and so queues nothing: the |
| - commit's `park-superseded` of the source region (§7.9), a |
| - rollback's `park-superseded` of the target region at the target's |
| - release (§7.8), and the console's release of a declared-lost target |
| - (§7.10). Two readings for the claim (§19.4): a cold admission made |
| - while the claim already holds such a park for its predecessor's |
| - region is **born covered**, since a rollback's return is admitted |
| - after the release queued the target region's park and the CAS that |
| - queued it could not see the record (seed 1036 / 3,000); and the |
| - at-rest sweep (§6.4), which parks a region's dead generations |
| - wholesale, covers the records whose predecessors it parks in the |
| - CASes that queue and acknowledge its `park-sweep`. INV-17: when a |
| + behind (R10-5, R11-3). **Coverage, completely** (claim rev 6.22 item 5, |
| + R13-2): a record is covered when its predecessor's retirement is in |
| + hand in the region that holds the predecessor's objects, and an |
| + entry becomes covered in **exactly four ways**, no other transition |
| + covers anything: **at birth**, a warm entry (its predecessor is its |
| + own generation, which nothing retires; the next cold admission's |
| + record names it and queues the chore), or an entry admitted while |
| + the claim already holds a whole-location park of its |
| + `predecessor_region` (that park retires the predecessor: a |
| + rollback's return admitted after the release queued the target |
| + region's park, which the CAS that queued it could not see; seed |
| + 1036 / 3,000); **by publication**, above; **by |
| + `CoverRegionPredecessors(op, phase, region)`** in one of the three |
| + CASes that queue a whole-location park of `region`, every uncovered |
| + entry whose `predecessor_region` is `region`: the commit's |
| + `park-superseded` of the source region (§7.9), a rollback's |
| + `park-superseded` of the target region at the target's release |
| + (§7.8), and the console's release of a declared-lost target (§7.10), |
| + which retire those generations wholesale and so queue nothing; and |
| + **by `CoverParkedPredecessors(op, phase, region, generations)`** in |
| + the CAS that queues an at-rest `park-sweep` and in the CAS that |
| + acknowledges it, only the uncovered entries whose predecessor is one |
| + of the listed generations, the ones that sweep actually retires (a |
| + predecessor with a sweepable object at the queuing; one whose |
| + objects it retired on the way, at the acknowledgement): a sweep |
| + never covers a predecessor it did not park. A predecessor whose |
| + objects live in another region (a move's source generation, seen by |
| + the target's publication) is **never queued into its region from |
| + here**, since the rollback may still need it (seeds 1036 and 1296 / |
| + rev 7.12; witness `wRollbackBaselinePreserved`). INV-17: when a |
| whole-location park of `holder.location` completes in a region, no |
| record whose predecessor's objects were there is uncovered. A dead |
| generation holding nothing yet still gets its chore in the |
| @@ -1342,8 +1409,26 @@ fails there first (§14.2.6). |
| died before its marker (two in a row happen: the second's purge |
| failed after its CAS), that is the normal unfinished state, every |
| generation of the chain and the marker's is live, and there is no |
| - alert; the baseline for the next admission is the nearest generation |
| - of the chain that holds an object, else the marker's; an empty |
| + alert. **The run walk, in one region's bucket** (claim rev 6.22 |
| + §6.2a, R13-1): the next admission follows each record's |
| + `predecessor` back from `holder.generation` to the marker's |
| + generation, newest first. A link whose generation keeps its objects |
| + in **another region** is passed over, covered or not: it holds |
| + nothing in this bucket, and its own region's park retires it (a |
| + clean rollback's fresh source admission R, admitted after the |
| + target region's park was queued and dead before its first upload, |
| + walks R, then the target's T in the other region, born covered under |
| + that park, then the source's S, and restores S; |
| + `TestInterruptedCleanReturn` walks that and R2 → R → T → S after |
| + it). A link **in this region** must be uncovered: a covered local |
| + generation is retired or being retired here, so reaching one as a |
| + needed baseline **refuses the start and alerts** (rev 7.13 read |
| + objects alone and would restore the marker's retired generation as |
| + an empty database; witness `wCoveredLocalBaseline`); an uncovered |
| + local link that holds an object is the baseline, the nearest such; |
| + one that holds none (a fresh generation that never uploaded) is |
| + passed over; else the marker's generation. The model's `restoreCalc` |
| + over that baseline is the reference the selector F mirrors. An empty |
| `holder.generation` for any other reason is unexplained missing data: |
| refuse the start and alert. A `holder.generation` that holds objects |
| has its marker published again (from the operation's build journal |
| @@ -1879,6 +1964,32 @@ no later retirement of that location may ever run. Claim rev 5's at-rest |
| sweep owns it: for a host with no operation running, each region's box |
| lists the host's namespace and parks what is not live, as a further |
| retirement event, under a `park-sweep` obligation the sweeping box owns. |
| +**The chore carries a persisted park scope** (claim rev 6.15 §2, R13-4): |
| +`{location, incarnation, evidence_at, request_limit}`, written at the |
| +queuing CAS (the sweeping box's complete listing is the evidence, taken |
| +then), so every retry, an agent restart's included, uses the same |
| +location, archive incarnation and **original** evidence time; a retry's |
| +own clock is never evidence, and a restart never starts the horizon |
| +again (rev 7.13's model kept the evidence time in a box-local map that |
| +the restart cleared; witness `wParkScopeSurvivesRestart`). Every remote |
| +chore has one: a whole-location park binds its scope in a CAS before its |
| +first step runs, once its stop evidence is in hand. The sweep parks at |
| +once and acknowledges, with its straggler pass, only after the scope's |
| +`evidence_at + request_limit`. **On a serving host** the chore's op is |
| +`session:<holder.session>`, as for `PublishGeneration`. **On a free host** |
| +(no holder) the sweep is a **holderless sweep** (claim rev 6.15 §6.2a): |
| +one CAS sets `op = {kind: parking, id: <new op id>, intent: {park_sweep: |
| +"v1"}}` with no `exec` and no holder and queues only scoped remote chores |
| +owned by that op; it is the only holderless claim that may carry |
| +obligations, so it blocks `free`'s successor create while it runs (the |
| +create waits, it is not refused), and its last acknowledgement frees the |
| +claim again in the same CAS (`FreeAfterPark`), keeping `quiet_after` |
| +(witness `wFreeSweepVsCreate`; INV-20: a create never claims a host while |
| +a park of its namespace is outstanding). Another region's sweep while the |
| +op runs joins it with its own scoped chores; any other operation running |
| +suppresses new sweeps; the console's recovery pass leaves the op to its |
| +runners and only replays `FreeAfterPark` for one whose chores are all |
| +acknowledged. |
| **It discovers locations from the namespace itself** (claim rev 6 §6.2a, |
| R3-4), not from `retired_incarnations`, which is capped at 32 entries and |
| exists only to stop an incarnation being reused: it lists |
| @@ -2621,10 +2732,10 @@ and a new agent process never resumes it (a new agent is a new session): |
| | 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 | | |
| -#### Admissions, coverage and retirement (operative, rev 7.13) |
| +#### Admissions, coverage and retirement (operative, rev 7.14) |
| This list, with §5.1 step 9 and the two tables above, is the operative |
| -rule set for writer admission (R12-4), mirroring claim rev 6.14 §6.4a's |
| +rule set for writer admission (R12-4), mirroring claim rev 6.22 §6.4a's |
| operative subsection item for item. Where any other passage of this |
| spec reads differently (the restore contract's older wording in §5.1, |
| the §7.8 rows as rev 7.11 had them, the authoritative-region table, the |
| @@ -2638,10 +2749,11 @@ this text wins. |
| holder's fields (INV-16); `region` is the admitted box's region, where |
| its generation's objects are; `predecessor_region` is the last |
| record's `region`, before any record the writer box's region, `""` |
| - when the generation holds nothing anywhere. A record is **born |
| - covered** when the claim already holds a whole-location park of |
| - `holder.location` for its predecessor's region (a reading for the |
| - claim, §19.4). |
| + when the generation holds nothing anywhere; a warm admission |
| + continues the same generation in the same region, so its region |
| + equals its predecessor record's (a clean return's first admission is |
| + cold: an old source certificate does not certify the target's |
| + session). Born covered: item 5. |
| 2. **Coverage** `""` | `sealed` | `clean-return`, as §5.1 step 9 states |
| it: `sealed` for a `from_db` seal of the stopped predecessor, |
| `clean-return` for a clean rollback with `src_covered`, a target that |
| @@ -2650,34 +2762,48 @@ this text wins. |
| without a certificate it records `writes_lost` (behind a lost target, one |
| record for every session the target was admitted into since the cut, |
| and a second for the source's cut session when `src_covered` is |
| - false). A `writes_lost` record declares the writes of the session it |
| - names and no other (INV-18, R12-1). |
| + false): `writes_lost` (one) plus `additional_writes_lost` (a list), |
| + each `{box, generation, session, remote_max_txid}`, unique by `(box, |
| + session)`, one alert per declaration (R13-3). A `writes_lost` record |
| + declares the writes of the session it names and no other (INV-18, |
| + R12-1). |
| 3. **The baseline.** A prepared generation from its pinned snapshot in |
| the admitting box's region, opened once; otherwise the predecessor |
| generation's remote in this region; in an unfinished run the newest |
| - generation of the run that holds an object, else the marker's; an |
| + generation of the run that holds an object **in this region**, else |
| + the marker's, walked as §5.1 step 9 says (R13-1): a covered foreign |
| + link is passed over, a covered local baseline refuses and alerts; an |
| empty generation outside an unfinished run is refused and alerted. |
| 4. **Stamps.** A cold admission takes a new stamp except under |
| `KeepStamp` (`holder.stamp > holder.session`); a clean return's CAS may |
| name the source's generation and stamp again, leaving |
| `holder.session` alone. |
| -5. **Publication.** After the marker names the generation, one |
| - `PublishGeneration(observedOpID, observedPhase, observedSession, |
| - publishedGeneration, region, newID)` walks the uncovered records as |
| - §5.1 step 9 states: no objects anywhere, covered, no chore; live |
| - again, left uncovered, no chore; in `region`, one deduplicated chore, |
| - covered; another region, uncovered, no chore, the walk continues. |
| - Every cold admission publishes. Retirement happens only through it or |
| - through item 6. |
| -6. **Whole-location parks cover.** `CoverRegionPredecessors(op, phase, |
| +5. **Coverage, completely.** An entry becomes covered in exactly four |
| + ways (R13-2): at birth (a warm entry; an entry admitted while the |
| + claim holds a whole-location park of its predecessor's region); by |
| + publication; by `CoverRegionPredecessors` (item 6); by |
| + `CoverParkedPredecessors` (item 6). **Publication:** after the marker |
| + names the generation, one `PublishGeneration(observedOpID, |
| + observedPhase, observedSession, publishedGeneration, region, newID)` |
| + requires `holder.generation` to be the published generation and an |
| + entry to name it, then walks every entry in order, skipping covered |
| + ones, as §5.1 step 9 states: no objects anywhere, covered, no chore; |
| + live again, left uncovered, no chore; in `region`, one deduplicated |
| + chore, covered; another region, uncovered, no chore, the walk |
| + continues. Every cold admission publishes. Retirement happens only |
| + through it or through item 6. |
| +6. **Parks cover what they retire.** `CoverRegionPredecessors(op, phase, |
| region)` runs inside the CAS that queues a region's park of the whole |
| location: the commit's park of the source region, the target's |
| release and the console's lost-target release for the target region. |
| It covers every record whose predecessor's objects are that region's |
| - and queues nothing. The at-rest sweep covers what it parks in its own |
| - CASes (a reading, §19.4). INV-17 checks the composition as each such |
| - park completes. A foreign-region predecessor is never queued into its |
| - region from another one. |
| + and queues nothing. `CoverParkedPredecessors(op, phase, region, |
| + generations)` runs in the CAS that queues an at-rest `park-sweep` and |
| + in the CAS that acknowledges it, and covers only the records whose |
| + predecessor is among the generations that sweep parks. INV-17 checks |
| + the composition as each whole-location park completes. A |
| + foreign-region predecessor is never queued into its region from |
| + another one. |
| 7. **Starts.** The admitting CAS first; a new agent process stops a |
| running app, admits a new session and restarts it; failed starts are |
| the retry policy's, five under one session with a doubling backoff; |
| @@ -2691,6 +2817,14 @@ this text wins. |
| past an uncovered one; no compaction. A declared-lost box's timers are |
| declared on the console's record and alerted; adoption sets |
| `holder.writer_box` to the pre-release writer's box. |
| +9. **Park state** (claim rev 6.15, R13-4; §6.4). Every remote chore |
| + carries a persisted park scope, bound before its first step or at the |
| + sweep's queuing CAS, and every retry uses its original evidence time. |
| + A free host's at-rest sweep is a holderless `parking` op with |
| + `intent.park_sweep`, no exec and no holder, which blocks the successor |
| + create until `FreeAfterPark` frees the claim in its last |
| + acknowledgement's CAS; on a serving host sweep chores carry |
| + `session:<holder.session>`. |
| **History.** The paragraphs that follow and §14.2.2's per-revision |
| blocks record how these rules were reached; where they differ from the |
| @@ -2990,6 +3124,29 @@ 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). |
| +**The evidence policy (Paul, 2026-10-06).** The deep sweeps were using |
| +half the shared box's cores and starving other agents. From rev 7.14 on: |
| +each revision runs **the gate** (300 seeds plus the witnesses) and **one |
| +mutation sweep at 3,000 seeds**, serially, with `HOSTLIFE_PAR=2` under |
| +`nice -n 19`, never alongside another sweep or a baseline; **baselines |
| +run at 30,000 seeds only**; the 100,000-seed baseline and the 30,000- |
| +and 100,000-seed mutation sweeps run **once**, at a final |
| +pre-implementation checkpoint, and only when Paul says so. A table cell |
| +or column those sweeps would have filled says "not run" for the |
| +revision, never a placeholder and never a number carried over from an |
| +earlier revision. Rev 7.14's 100,000-seed baseline had already run, |
| +clean, before the policy was set and is reported in §14.2.3; its 30,000- |
| +and 100,000-seed mutation sweeps were stopped mid-run and are not |
| +evidence. |
| + |
| +**Rev 7.14: `TestInterruptedCleanReturn`, INV-20.** `go test` runs the |
| +positive case of the run walk across regions beside the witnesses: a |
| +clean rollback's fresh source admission dies before its first upload and |
| +the recovery walks R → T → S, then one more interrupted admission walks |
| +R2 → R → T → S; both restore the source's data. INV-20 is checked in the |
| +create's claim CAS: no obligation may be outstanding when a create claims |
| +a host. |
| + |
| **Rev 7.13: INV-17 at the park, `TestProbeWindow`.** The oracle for |
| regional coverage runs when a whole-location park of `holder.location` |
| completes in a region, not at the end: a record whose predecessor's |
| @@ -3065,8 +3222,10 @@ under a second. `mutate.sh` now fails on a scratch directory it cannot |
| create and on an `xargs` failure, requires exactly one well-formed |
| verdict per requested mutation, and reports a rule that has witnesses |
| but produced no witness output as an ERROR, never as "none" (R3-6). |
| -`go test` also runs `TestReadinessBudget`, T11's arithmetic (§7.3), and |
| -`TestProbeWindow`, the probe deadline's boundary (§7.7, rev 7.13). |
| +`go test` also runs `TestReadinessBudget`, T11's arithmetic (§7.3), |
| +`TestProbeWindow`, the probe deadline's boundary (§7.7, rev 7.13), and |
| +`TestInterruptedCleanReturn`, the run walk across regions (§5.1 step 9, |
| +rev 7.14). |
| **Rev 7.6: the pinned libraries, observed.** `internal/sim/litestreamfacts/` |
| is a second test-only package: it drives litestream v0.5.14 and |
| @@ -3592,6 +3751,69 @@ 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.14: joint round 13 and claim rev 6.22.** |
| + |
| +- **The park scope and the holderless sweep (R13-4; claim rev 6.15).** |
| + `obligation.Scope *parkScope{Location, Inc, EvidenceAt, Limit}`. A |
| + `park-replica` or `park-superseded` chore binds its scope in a CAS the |
| + first time its owner has the stop evidence (`park scope bound`), and |
| + every later step, an agent restart's included, reads `EvidenceAt` and |
| + `Limit` from the claim; the sweep writes the scope at its queuing CAS |
| + and acknowledges after `EvidenceAt + Limit` with its straggler pass. |
| + `sweep()` on a free claim sets `op = {Kind: "parking", ID, ParkSweep: |
| + "v1", Exec: -1}` in the CAS that queues its chores; another region's |
| + sweep joins the running op; on a serving host the chores carry |
| + `session:<n>`; the obligation runner's acknowledgement CAS performs |
| + `FreeAfterPark` (`op = {}`) when it removes the op's last chore |
| + (`free after park`, equal to `holderless sweeps` in every run); the |
| + console's recovery pass leaves such an op to its runners and replays |
| + `FreeAfterPark` only for one whose chores are gone. `createSteps` waits |
| + on a holderless sweep instead of abandoning the create, and its claim |
| + CAS checks INV-20 (no obligation outstanding). Rules |
| + `persisted-park-scope` (the mutation keeps rev 7.13's box-local |
| + evidence map, which `forget()` clears at an agent restart) and |
| + `holderless-park` (the mutation queues rev 7.13's bare `sweep` chores |
| + on the free claim and drops the create's wait on bare obligations); |
| + witnesses `wParkScopeSurvivesRestart` (a committed move's source park, |
| + 45 steps, the source's agent restarts, the acknowledgement must come |
| + within the commit's evidence plus the horizon and slack; INV-9 under |
| + the mutation) and `wFreeSweepVsCreate` (a deleted host, late residue |
| + in its region, a create requested at once; the create waits for |
| + `FreeAfterPark`; INV-20 under the mutation). |
| +- **Coverage, completely (R13-2; claim rev 6.22 item 5).** |
| + `publishGeneration` requires the last record to name the published |
| + generation and walks every entry in order, skipping covered ones, with |
| + the explicit bound `e.Session > session` (never reached under the |
| + CAS's session check); warm entries are born covered in `admitCommit` |
| + (`admissions born covered: warm`); born covered under a pending park |
| + applies to every mode; `coverRegionPredecessors` and INV-17 apply to |
| + every entry; `coverSweptPredecessors` became |
| + `coverParkedPredecessors(n, region, generations)` with |
| + `sweptPredecessors(n, region, retired)` supplying the list (sweepable |
| + predecessors at the queuing CAS, retired ones at the acknowledgement); |
| + trimming counts covered entries only. |
| +- **The run walk (R13-1; claim rev 6.22 §6.2a).** `unfinishedRun(c, bg)` |
| + returns the run's cold records newest first; `runBaseline(b, c, run, |
| + bg)` walks their predecessor links: a link whose `PredRegion` is not |
| + this region is passed over, covered or not; a covered link in this |
| + region refuses the start with an alert (`start refused: covered local |
| + baseline`); the nearest local link holding an object is the baseline, |
| + else the marker's. `hasFiles` reads current objects (rev 7.13 counted |
| + a key's presence, so a parked generation still looked like a |
| + baseline). `restoreAsNext`, the oracle's baseline, walks the same way. |
| + Rule `covered-baseline-refused` (the mutation ignores the covered flag |
| + and selects by objects alone); witness `wCoveredLocalBaseline` (an |
| + unfinished run g2 → g1 whose record is covered and whose g1 was |
| + retired: refused under the rule; under the mutation the walk passes |
| + over the empty g1 and restores the marker's g1 as an empty database, |
| + INV-2); `TestInterruptedCleanReturn` (above). `wOriginSwept` names the |
| + refusal as its failure under `absent-marker-origin`: the swept origin |
| + is a covered local baseline since rev 7.14, so the recovery refuses |
| + with an alert rather than restoring nothing. |
| +- **`additional_writes_lost` (R13-3).** `admissionRecord.LostMore` is |
| + `AdditionalWritesLost`, each entry alerted; the model already declared |
| + every target session since the cut (rev 7.13). |
| + |
| **Rev 7.13: joint round 12 and claim rev 6.14.** |
| - **Regions on the record (claim rev 6.14 item 1, R12-3).** |
| @@ -4268,6 +4490,51 @@ 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.14, on the final model (claim rev 6.22: the persisted park |
| +scope, the holderless sweep, coverage in four ways, the run walk across |
| +regions): 30,000 seeds, zero violations; 100,000 seeds, zero |
| +violations** (169 s and 1021 s; the 100,000-seed run finished |
| +before the evidence policy of §14.2.1 was set). Across the 100,000 seeds: |
| +150,124 completed operations, among them 69,017 cold and |
| +16,058 warm admissions (12,090 covered `sealed`, |
| +763 covered `clean-return`; 16,058 warm entries |
| +born covered, 384 born covered under a pending park, |
| +1,157 predecessors left uncovered by a publication for their |
| +own region, 0 live again and left uncovered, |
| +27,264 holding nothing anywhere, 748 records |
| +covered at the commit's park, 275 at a rollback's |
| +release, 3 at a lost-target release, 609 by |
| +the sweep's `CoverParkedPredecessors`; 497,273 park scopes bound |
| +before a chore's first step, 38,098 holderless sweeps and |
| +38,098 `FreeAfterPark` transitions; 0 |
| +starts refused on a covered local baseline; 19,236 clean closes, |
| +1,430 closes refused as uncertain, 0 stale |
| +certificates, 984 wakes that waited for a draining writer, |
| +52,808 local databases purged, 4,085 starts that |
| +waited for a failed purge, 56,370 writes_lost records declaring |
| +8,101 acknowledged writes lost (175 of the |
| +records in `additional_writes_lost`), 27,597 full first uploads, |
| +105,879 start steps that waited for their marker, |
| +608 markers published again, 3,614 probes |
| +restarted, 486 probe attempts ended by their window, a |
| +late readiness or their fifth failure (456 refused before |
| +the start by the deadline check), 1,554 app starts that |
| +failed and were retried within their session, 0 hosts |
| +marked failed by the retry policy, 90 seals whose source |
| +replica was short and 38 returns that carried the seal; |
| +9,339 final recovery admissions run by the oracle, |
| +0 unverified), 735 completed moves, |
| +2,105 clean and 89 dirty rollbacks, |
| +318 pre-flip reverts, 264 declared losses, |
| +24,755 pushes, 90,312 delete-park-free cycles and |
| +4,827 lost disks (3,474 with a crash); |
| +9,221 LTX compactions, 6,478 snapshot rotations, |
| +583 level-0 upload retries, 28,962 anchors; |
| +26,123 local stamp records lost and re-initialized; |
| +46,605 requests completed after `H`; 35,592 staging |
| +signatures refused as stale; 14,432 creates restarted on a |
| +412. Every oracle left the system unchanged. |
| + |
| **Rev 7.13, on the final model (claim rev 6.14: regions on the record, |
| the publication walk, `CoverRegionPredecessors` at whole-location parks, |
| the declared identity, the probe deadline before the start): 30,000 |
| @@ -4620,36 +4887,57 @@ 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.13 model (42af7bfc), 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 |
| +on the final rev 7.14 model (4ebfa0a5), with the strict classification, |
| +**in two ways**: the **random sweep**, 3,000 seeds each (the 30,000- and |
| +100,000-seed sweeps of earlier revisions were not run for rev 7.14: the |
| +evidence policy of §14.2.1, Paul 2026-10-06; their columns say so); and |
| the rule's **witness scenarios** (§14.2.2, `witness_test.go`) under the |
| -same mutation, for the 54 rules that have them. A rule is caught |
| +same mutation, for the 57 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 **101 rules**: rev 7.12's 96 plus |
| -`foreign-region-uncovered` and `cover-at-park` (claim rev 6.14 items 5 |
| -and 6, R12-3), `session-scoped-loss` (R12-1), `probe-window` (R12-2) |
| -and `absent-marker-origin` (R12's evidence note). `mutate.sh 3000` exited 0: no ERROR, no unexpected |
| +section does too. The model has **104 rules**: rev 7.13's 101 plus |
| +`persisted-park-scope` and `holderless-park` (claim rev 6.15, R13-4) and |
| +`covered-baseline-refused` (claim rev 6.22 §6.2a, R13-1). `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.12's |
| -counts are in the rev 7.12 spec (dd3e35f6). **Every table below is |
| +`HOSTLIFE_WITNESS=<rule>` replays a witness with its trace. Rev 7.13's |
| +counts, the last with the deeper sweeps, are in the rev 7.13 spec |
| +(1f511c42). **Every table below is |
| regenerated from the retained verdict files** (R9-6; |
| -`~/.cache/nearest-region/rev713-sweeps/`), none is carried over. |
| +`~/.cache/nearest-region/rev714-sweeps/`), none is carried over. |
| | | rules | |
| |---|---| |
| -| caught alone by the sweep at 3,000 seeds | 66 | |
| -| caught alone by the sweep at 30,000 (and by their witness, where one exists) | 11 (`declare-lost-compute`, `evidence-whole-tree`, `hostguard`, `lost-quarantine`, `markers-last`, `orphan-order`, `restore-overlap`, `seal-by-version`, `seal-return`, `staging-quiet`, `stale-hold-release`) | |
| -| caught alone by the sweep at 100,000 (and by its witness, where one exists) | 0 (none this round: rev 7.12's two moved, `declare-lost-compute` to 30,000 and `baseline-live` to witness-only) | |
| -| caught alone by their witness only; the sweep misses them at 30,000 | 11 (`absent-marker-origin`, `admit-before-start`, `baseline-live`, `close-evidence`, `close-waits`, `closed-marker`, `newest-l0`, `probe-window`, `remote-baseline`, `restore-gap-closed`, `session-scoped-loss`) | |
| +| caught alone by the sweep at 3,000 seeds | 69 | |
| +| caught alone by the sweep at 30,000 (and by their witness, where one exists) | not run for rev 7.14 (CPU budget; Paul 2026-10-06); without a verdict this round, the rare rules the sweep reaches only at 30,000: 1 (`hostguard`) | |
| +| caught alone by the sweep at 100,000 (and by its witness, where one exists) | not run for rev 7.14 (CPU budget; Paul 2026-10-06) | |
| +| caught alone by their witness only; the sweep at 3,000 misses them | 21 (`absent-marker-origin`, `admit-before-start`, `baseline-live`, `close-evidence`, `close-waits`, `closed-marker`, `covered-baseline-refused`, `declare-lost-compute`, `evidence-whole-tree`, `generation-conditional`, `lost-quarantine`, `markers-last`, `newest-l0`, `orphan-order`, `persisted-park-scope`, `probe-window`, `remote-baseline`, `restore-gap-closed`, `restore-overlap`, `seal-return`, `session-scoped-loss`) | |
| | 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.14 moved.** The three new rules: `persisted-park-scope` |
| +witness; sweep 0 / 3,000 (an agent restart mid-park starts the |
| +horizon again from the restart's clock), `holderless-park` |
| +561 / 3,000 (a create claims a host over an outstanding park, |
| +INV-20) and `covered-baseline-refused` witness; sweep 0 / 3,000 |
| +(the run walk restores a retired local baseline as an empty database). |
| +The rules the coverage and park changes touched: `cover-at-park` |
| +29 / 3,000, `foreign-region-uncovered` |
| +4 / 3,000, `absent-marker-origin` |
| +witness; sweep 0 / 3,000 (its witness names the covered-baseline |
| +refusal now), `baseline-live` witness; sweep 0 / 3,000, `writes-lost` |
| +13 / 3,000, `clean-return-identity` |
| +13 / 3,000, `lost-return-park` 1 / 3,000, |
| +`obligations-block-ops` 21 / 3,000, `sweep-namespace` |
| +542 / 3,000, `sweep-staging` 36 / 3,000, |
| +`straggler-sweep` 770 / 3,000, `quiet-before-ack` |
| +152 / 3,000, `hostguard` 0 / 3,000, |
| +`stale-hold-release` 1 / 3,000, `strict-spawn` |
| +13 / 3,000. The rules rev 7.13 caught only at 30,000 or 100,000 |
| +have no sweep verdict this round; the summary table lists them. |
| + |
| **What rev 7.13 moved.** The five new rules: `foreign-region-uncovered` |
| 2 / 3,000, 34 / 30,000 (a chore queued into the source's region |
| from the target's publication parks the rollback's baseline), |
| @@ -4833,61 +5121,64 @@ 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 | | 1 / 3,000, 9 / 30,000, 36 / 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 | | 2 / 3,000, 27 / 30,000, 64 / 100,000 | |
| -| `declare-lost-compute` (model 5) | the target is frozen in its settle window and its execution lease expires; the VM resumes once the source has recovered | **violated**: INV-1, two boxes run the host | | 0 / 3,000, 1 / 30,000, 1 / 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 | | witness; sweep 0 / 3,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 | |
| +| `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 | | witness; sweep 0 / 3,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 | | 0 / 3,000, 5 / 30,000 | |
| -| `markers-last` (R2-6) | the source has a registered timer; the target's agent crashes between extracting the files and writing the marker | **violated**: INV-2, the timer is lost | | 0 / 3,000, 4 / 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 | | 0 / 3,000, 5 / 30,000 | |
| -| `staging-quiet` (J-N2) | a staging round completes after the landing's staging park acknowledged, before the release | **violated**: INV-10 at the release | | 0 / 3,000, 1 / 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) | | 1 / 3,000, 9 / 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, 48 / 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 | | witness; sweep 0 / 3,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 | | witness; sweep 0 / 3,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 | |
| +| `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 | |
| +| `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 | |
| +| `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) | | 1 / 3,000 | |
| +| `commit-before-open` (INV-5; R3-5) | a public request reaches the target's edge while its probe runs | **violated**: INV-5 | | 3 / 3,000 | |
| | `claim-cas-opid` (C2) | a stalled source goroutine with the rollback's last read resumes after a purge claimed the host | held | with `revalidate-before-effect`: **violated**, the store is torn down under a serving host | 0 / 3,000 | |
| | `exec-admission`, `hold-op-open`, `start-check-claim-gen`, `exec-writer` (J2-R2-8; claim rev 6.8.1) | a paused open from an earlier operation lands after the commit while the source's row is still held; a request wakes the source | held, each, and under every proper subset | all four: **violated**, INV-1 (the non-exec source is admitted cold into a fresh generation restored from its own region's old files and serves beside the target) | 0 / 3,000 | |
| | `start-check` (INV-4) | the same, dropping the whole start check | retired in rev 7.10: with every restore from the box's own region, the stale source finds nothing of the target's generation to restore and cannot start; subsumed (`expected-outcomes.txt`) | | 0 | |
| -| `strict-spawn` (J-D3) | the source runs a main process and a descendant placed as its parent was; the move cuts | held | with `evidence-whole-tree`: **violated**, INV-1 | 9 / 3,000, 110 / 30,000, 374 / 100,000 | |
| +| `strict-spawn` (J-D3) | the source runs a main process and a descendant placed as its parent was; the move cuts | held | with `evidence-whole-tree`: **violated**, INV-1 | 13 / 3,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) | | 327 / 3,000, 2,978 / 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 | 332 / 3,000, 2,946 / 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 | | 544 / 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 | | 1 / 3,000, 18 / 30,000 | |
| -| `restore-overlap` (§5.1, R4-1) | a generation's snapshot ends at the push's TXID; the only continuation is a compacted file starting one below it; the disk is lost and the host wakes cold | **violated**: INV-3 since rev 7.10, the restore stops short of the certificate's `max_txid` and the box never starts (rev 7.4's `min == current + 1` discarded the file and lost four writes) | | 0 / 3,000, 1 / 30,000 | |
| -| `restore-gap-closed` (§5.1, R4-1) | the same generation with the next file missing and the one after current | **violated**: a restore across the gap returns a database short of the acknowledged writes | | witness; sweep 0 / 3,000, 0 / 30,000 | |
| -| `restore-anchor` (§5.1 step 7, R5-1) | a push installs a snapshot alone; the host wakes, writes three times, replicates, loses its disk and wakes cold | **violated**: INV-2, every write since the push is lost: replication restarted at TXID 1 below the snapshot and the planner skipped the files (facts R5-1a, b) | | 50 / 3,000, 521 / 30,000, 1,740 / 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) | | 9 / 3,000, 122 / 30,000, 432 / 100,000 | |
| -| `anchor-acked` (§5.1 step 7, R6-1) | a push installs a snapshot alone; the install's anchor PUT is held across forty attempted opens, then released; the host writes, replicates, loses its disk and wakes cold | **violated**: the host opened before its anchor was acknowledged; litestream's position would be 0 and the writes below the snapshot are lost on the cold restore (INV-2) | | 12 / 3,000, 91 / 30,000, 334 / 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) | | 69 / 3,000, 706 / 30,000, 2,339 / 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, 100 / 30,000, 354 / 100,000 | |
| -| `closed-marker` (claim rev 6.6 §6.4a; a certificate since rev 7.9) | a stale certificate (`max_txid` behind the remote maximum) beside the dead writer's outstanding upload | **violated**: taken as intact, B continues in place and A's late file replaces B's (INV-2) | | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 | |
| -| `close-waits` (claim rev 6.6 §6.4a) | a clean stop with an upload in flight | **violated**: written at once, the marker vouches for an upload that has not returned | | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 | |
| -| `newest-l0` (§5.1 step 8, R7-3) | the local position runs ahead of the uploads across two compactions and snapshot rotations | **violated**: retention below the previous snapshot removes the newest uploaded level-0 file | | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 | |
| -| `build-completion` (§5.1 step 2, §7.6, R7-4) | a push's build with its snapshot, then its anchor, held, the agent crashing in between each | **violated**: `generation.json` published before its snapshot landed (INV-11) | | 707 / 3,000 | |
| -| `evidence-whole-tree` (§6.1, J-D3) | an adopted legacy host runs a descendant outside the cgroup; the move cuts | **violated**: evidence blind to the escapee certifies the stop and two boxes run the host (INV-1) | | 0 / 3,000, 5 / 30,000 | |
| -| `timer-freeze` (J-N14) | a registered timer on the source; the move holds the row; the runner's deliveries are refused; a clean rollback | **violated**: the refused deliveries advanced the runner's bookkeeping, the timer digest differs from the stop's, the source is `stuck` | | 3 / 3,000, 13 / 30,000 | |
| -| `recovery-current-inputs` (§7.7, §7.8; R2-5) | a bundle is published after admission; the target writes; the rollback is dirty | **violated**: `stuck` | | 33 / 3,000 | |
| -| `writer-session` (claim rev 6.8 §6.4a, R8-1) | two sessions certify; the third dies with its disk and an upload in flight; the dead certificates still match the remote maximum | **violated**: the newest certificate readmits the box into the generation and the late upload replaces its file (INV-2) | | 4 / 3,000, 27 / 30,000, 77 / 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 | | 711 / 3,000, 6,844 / 30,000, 23,089 / 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) | | 39 / 3,000, 395 / 30,000 | |
| -| `close-evidence` (claim rev 6.8 §6.4a, R8-5) | an upload is held past the client's timeout; the retry lands; the original stays outstanding; a clean stop | **violated**: the certificate is written while the original is unresolved | | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 | |
| -| `close-evidence` (R9-5), two more scenarios | (i) a compaction's level-1 PUT is held past the client's timeout, the next pass retries and lands, the original completes afterwards; (ii) a snapshot PUT completes on the server after the client gave up on it | **violated** in each: the certificate is written while a request of the session was retried after a timeout, or its response was lost | | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 | |
| -| `remote-baseline` (claim rev 6.9 §6.4a, R9-1) | a session closes cleanly through N+1; the box's local database is a cached copy through N; the next wake | **violated**: the stale copy is served without the acknowledged write, and its upload for N+1 is skipped at the remote position (INV-2) | | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 | |
| -| `writes-lost` (claim rev 6.9 §6.4a, R9-2) | a writer acknowledges a write and crashes before uploading it; the next wake is cold | **violated**: lost silently, the serving database differs from the acknowledged writes (INV-2); with the rule the admission records writes_lost and alerts | | 13 / 3,000, 110 / 30,000, 368 / 100,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) | | 303 / 3,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 | 306 / 3,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 | | witness; sweep 0 / 3,000 | |
| +| `sweep-namespace` (claim rev 6 §6.2a, R3-4) | a replication PUT of incarnation 1 completes after 33 recreates dropped it from `retired_incarnations` | **violated**: INV-10, residue the sweep never finds | | 542 / 3,000 | |
| +| `live-set-region` (claim rev 6.4 §6.2a, R4-3) | a legacy host serving in UK with an earlier replica in US; discovery parks US; an old US replication PUT lands after | **violated**: INV-10, residue the US sweep exempts by key alone | | 2 / 3,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) | | witness; sweep 0 / 3,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 | |
| +| `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) | | 55 / 3,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) | | 17 / 3,000 | |
| +| `anchor-acked` (§5.1 step 7, R6-1) | a push installs a snapshot alone; the install's anchor PUT is held across forty attempted opens, then released; the host writes, replicates, loses its disk and wakes cold | **violated**: the host opened before its anchor was acknowledged; litestream's position would be 0 and the writes below the snapshot are lost on the cold restore (INV-2) | | 12 / 3,000 | |
| +| `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) | | 69 / 3,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) | | 12 / 3,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 | |
| +| `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 | |
| +| `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 | |
| +| `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) | | 710 / 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) | | witness; sweep 0 / 3,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 | |
| +| `recovery-current-inputs` (§7.7, §7.8; R2-5) | a bundle is published after admission; the target writes; the rollback is dirty | **violated**: `stuck` | | 37 / 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) | | 7 / 3,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 | | 717 / 3,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 | |
| +| `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) | | 38 / 3,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 | |
| +| `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 | |
| +| `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 | |
| +| `writes-lost` (claim rev 6.9 §6.4a, R9-2) | a writer acknowledges a write and crashes before uploading it; the next wake is cold | **violated**: lost silently, the serving database differs from the acknowledged writes (INV-2); with the rule the admission records writes_lost and alerts | | 13 / 3,000 | |
| | `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) | | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 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 | 15 / 3,000, 112 / 30,000, 332 / 100,000 | |
| -| `absent-marker-origin` (R11-1; its own rule since rev 7.13) | 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, reading absence as agreement, parks the origin and the recovery restores nothing (INV-2 local) | | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 | |
| -| `session-scoped-loss` (R12-1) | two writer sessions of one box each acknowledged an unuploaded write; a `writes_lost` record for the second is applied (a constructed-state oracle test) | held: only the second session's write is exempted | **violated** under the mutation: INV-18, the record for session 2 exempted session 1's undeclared write | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 | |
| -| `foreign-region-uncovered` (claim rev 6.14 item 5, R12-3) | a probed landing whose target published; the chore's quiet time brought forward; the source region's runner works within the settle window; a clean rollback | held: no chore was queued into the source's region, the return restores the source's generation | **violated** under the mutation: the chore parked the rollback's baseline and the return restored an empty database (INV-2) | 2 / 3,000, 34 / 30,000 | |
| -| `cover-at-park` (claim rev 6.14 item 6, R12-3), three scenarios | (i) a committed move: the commit's CAS queues the source region's park; (ii) the record flips to committed and every actor pauses past the horizon before anyone follows it; (iii) `followRecord` is called again after the commit | held: in each the target's record is covered in the CAS that queued the park, one park is queued, the replay is refused | **violated** under the mutation: INV-17 as the source region's park completes, the target's record uncovered | 34 / 3,000, 337 / 30,000 | |
| -| `probe-window` (R12-2) | the landing probe's launch environment is ready exactly 30 steps after the attempt's first app stage | held: the attempt fails before the start, the next admission's probe is accepted | **violated** under the mutation: the expired attempt starts and is accepted (INV-19) | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 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, 8 / 30,000, 22 / 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 | |
| +| `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 | |
| +| `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) | | witness; sweep 0 / 3,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 | |
| +| `absent-marker-origin` (R11-1; its own rule since rev 7.13) | 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, reading absence as agreement, parks the origin and the recovery restores nothing (INV-2 local) | | witness; sweep 0 / 3,000 | |
| +| `session-scoped-loss` (R12-1) | two writer sessions of one box each acknowledged an unuploaded write; a `writes_lost` record for the second is applied (a constructed-state oracle test) | held: only the second session's write is exempted | **violated** under the mutation: INV-18, the record for session 2 exempted session 1's undeclared write | witness; sweep 0 / 3,000 | |
| +| `foreign-region-uncovered` (claim rev 6.14 item 5, R12-3) | a probed landing whose target published; the chore's quiet time brought forward; the source region's runner works within the settle window; a clean rollback | held: no chore was queued into the source's region, the return restores the source's generation | **violated** under the mutation: the chore parked the rollback's baseline and the return restored an empty database (INV-2) | 4 / 3,000 | |
| +| `cover-at-park` (claim rev 6.14 item 6, R12-3), three scenarios | (i) a committed move: the commit's CAS queues the source region's park; (ii) the record flips to committed and every actor pauses past the horizon before anyone follows it; (iii) `followRecord` is called again after the commit | held: in each the target's record is covered in the CAS that queued the park, one park is queued, the replay is refused | **violated** under the mutation: INV-17 as the source region's park completes, the target's record uncovered | 29 / 3,000 | |
| +| `probe-window` (R12-2) | the landing probe's launch environment is ready exactly 30 steps after the attempt's first app stage | held: the attempt fails before the start, the next admission's probe is accepted | **violated** under the mutation: the expired attempt starts and is accepted (INV-19) | witness; sweep 0 / 3,000 | |
| +| `persisted-park-scope` (claim rev 6.15 §2, R13-4) | a committed move's source-region park binds its scope in the claim; 45 steps on, the source region's agent restarts mid-park | held: the acknowledgement comes within the commit's evidence time plus the horizon and slack | **violated** under the mutation: the box-local evidence map is gone with the agent, the horizon starts again, the acknowledgement is late (INV-9) | witness; sweep 0 / 3,000 | |
| +| `holderless-park` (claim rev 6.15 §6.2a, R13-4) | a deleted host's region keeps late residue; the free host's sweep and a create requested at once | held: the sweep runs as a holderless parking op, the create waits for `FreeAfterPark`, then serves | **violated** under the mutation: bare chores on the free claim, the create claims the host over the outstanding park (INV-20) | 561 / 3,000 | |
| +| `covered-baseline-refused` (claim rev 6.22 §6.2a, R13-1) | an unfinished run g2 → g1 whose record is covered and whose g1 was retired in the region | held: the start is refused and alerts, the host does not run | **violated** under the mutation: the walk passes over the empty g1 and restores the marker's retired g1 as an empty database (INV-2) | witness; sweep 0 / 3,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) | | witness; sweep 0 / 3,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 | |
| **The purge fence, the ETag condition and C5a.** `purge-claim-fence` |
| (CC21) is caught alone by the sweep: 28 / 3,000, 240 / 30,000. |
| @@ -4911,56 +5202,55 @@ combination** (R4 §3): each door rule's two-rule pair with C3a already |
| fails, so the three-rule row is a wider set and inherits no claim that its |
| proper subsets hold. It is no longer run. |
| -**Caught alone: 88 of 101** (66 by the sweep at 3,000; 11 by the sweep at |
| -30,000, marked †; 0 at 100,000, |
| -marked ††; 11 by their witness alone, marked ‡). |
| +**Caught alone: 90 of 104** (69 by the sweep at 3,000; 21 by their witness alone, marked ‡; the sweeps at 30,000 and 100,000 were not run for rev 7.14 (CPU budget; Paul 2026-10-06), so the one rare rule the sweep reaches only there, `hostguard`, has no verdict this round). |
| | rule | seeds failing | | rule | seeds failing | |
| |---|---|---|---|---| |
| -| `abort-target-owner` | 933 / 3,000 | | `absent-marker-origin` ‡ | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 | |
| -| `admission-registration` | 34 / 3,000 | | `admit-before-start` ‡ | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 | |
| -| `admit-everywhere` | 711 / 3,000, 6,844 / 30,000, 23,089 / 100,000 | | `anchor-acked` | 12 / 3,000, 91 / 30,000, 334 / 100,000 | |
| -| `baseline-live` ‡ | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 | | `build-completion` | 707 / 3,000 | |
| -| `cancelled-creates` | 385 / 3,000 | | `claim-never-deleted` | 4 / 3,000, 57 / 30,000 | |
| -| `claim-op-exclusive` | 82 / 3,000 | | `clean-return-identity` | 15 / 3,000, 112 / 30,000, 332 / 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, 48 / 30,000 | |
| -| `cover-at-park` | 34 / 3,000, 337 / 30,000 | | `cut-deadline` | 39 / 3,000 | |
| -| `declare-lost-compute` † | 0 / 3,000, 1 / 30,000, 1 / 100,000 | | `dirty-return` | 1 / 3,000, 9 / 30,000 | |
| -| `evidence-from-state` | 2,610 / 3,000 | | `evidence-whole-tree` † | 0 / 3,000, 5 / 30,000 | |
| -| `fence-by-installation` | 327 / 3,000, 2,978 / 30,000 | | `fence-etag` | 26 / 3,000, 226 / 30,000 | |
| -| `fence-stamp` | 332 / 3,000, 2,946 / 30,000 | | `files-carried` | 29 / 3,000 | |
| -| `floor-boot-recovery` | 2,577 / 3,000 | | `foreign-region-uncovered` | 2 / 3,000, 34 / 30,000 | |
| -| `fresh-admission` | 10 / 3,000 | | `fresh-incarnation` | 41 / 3,000 | |
| -| `generation-conditional` | 1 / 3,000, 9 / 30,000, 36 / 100,000 | | `hostguard` † | 0 / 3,000, 2 / 30,000, 2 / 100,000 | |
| -| `legacy-discovery` | 367 / 3,000, 3,561 / 30,000 | | `live-set-region` | 1 / 3,000, 18 / 30,000 | |
| -| `location-per-incarnation` | 28 / 3,000, 358 / 30,000, 1,185 / 100,000 | | `lost-quarantine` † | 0 / 3,000, 5 / 30,000 | |
| -| `lost-return-park` | 2 / 3,000, 27 / 30,000, 64 / 100,000 | | `markers-last` † | 0 / 3,000, 4 / 30,000 | |
| -| `newest-l0` ‡ | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 | | `obligations-block-ops` | 29 / 3,000 | |
| -| `orphan-no-deadline` | 41 / 3,000 | | `orphan-order` † | 0 / 3,000, 1 / 30,000 | |
| -| `park-all-versions` | 564 / 3,000 | | `park-by-version` | 2,527 / 3,000 | |
| -| `park-skip-lock` | 2,728 / 3,000 | | `participant-rows` | 4 / 3,000 | |
| -| `probe-window` ‡ | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 | | `purge-adopts` | 7 / 3,000 | |
| -| `purge-claim-fence` | 23 / 3,000, 235 / 30,000 | | `purge-journal` | 1,888 / 3,000 | |
| -| `purge-reserve-first` | 2,125 / 3,000 | | `quiet-before-ack` | 180 / 3,000 | |
| -| `recovery-current-inputs` | 33 / 3,000 | | `recovery-generation` | 10 / 3,000, 100 / 30,000, 354 / 100,000 | |
| -| `recovery-pass` | 2,473 / 3,000 | | `registration-recovery` | 2,114 / 3,000 | |
| -| `remote-baseline` ‡ | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 | | `restore-anchor` | 50 / 3,000, 521 / 30,000, 1,740 / 100,000 | |
| -| `restore-by-generation` | 124 / 3,000 | | `restore-gap-closed` ‡ | witness; sweep 0 / 3,000, 0 / 30,000 | |
| -| `restore-overlap` † | 0 / 3,000, 1 / 30,000 | | `retirement-ids` | 426 / 3,000 | |
| -| `return-stamp` | 69 / 3,000, 706 / 30,000, 2,339 / 100,000 | | `revalidate-before-effect` | 15 / 3,000, 178 / 30,000 | |
| -| `revert-journal` | 12 / 3,000 | | `rollback-journal` | 1 / 3,000, 9 / 30,000 | |
| -| `root-advance` | 9 / 3,000, 122 / 30,000, 432 / 100,000 | | `sdk-no-resign` | 10 / 3,000 | |
| -| `seal-by-version` † | 0 / 3,000, 5 / 30,000 | | `seal-return` † | 0 / 3,000, 8 / 30,000, 22 / 100,000 | |
| -| `session-scoped-loss` ‡ | witness; sweep 0 / 3,000, 0 / 30,000, 0 / 100,000 | | `sign-at-check` | 9 / 3,000 | |
| -| `sign-before-safeuntil` | 20 / 3,000 | | `source-readiness` | 10 / 3,000 | |
| -| `staging-quiet` † | 0 / 3,000, 1 / 30,000 | | `stale-hold-release` † | 0 / 3,000, 14 / 30,000, 52 / 100,000 | |
| -| `start-check` | 17 / 3,000, 214 / 30,000 | | `start-check-claim-gen` | 14 / 3,000, 167 / 30,000 | |
| -| `straggler-sweep` | 783 / 3,000 | | `strict-spawn` | 9 / 3,000, 110 / 30,000, 374 / 100,000 | |
| -| `sweep-namespace` | 544 / 3,000 | | `sweep-staging` | 32 / 3,000 | |
| -| `target-park` | 17 / 3,000 | | `timer-canonical` | 2 / 3,000 | |
| -| `timer-freeze` | 3 / 3,000, 13 / 30,000 | | `valid-ltx` | 39 / 3,000, 395 / 30,000 | |
| -| `writer-session` | 4 / 3,000, 27 / 30,000, 77 / 100,000 | | `writes-lost` | 13 / 3,000, 110 / 30,000, 368 / 100,000 | |
| +| `abort-target-owner` | 962 / 3,000 | | `absent-marker-origin` ‡ | witness; sweep 0 / 3,000 | |
| +| `admission-registration` | 48 / 3,000 | | `admit-before-start` ‡ | witness; sweep 0 / 3,000 | |
| +| `admit-everywhere` | 717 / 3,000 | | `anchor-acked` | 12 / 3,000 | |
| +| `baseline-live` ‡ | witness; sweep 0 / 3,000 | | `build-completion` | 710 / 3,000 | |
| +| `cancelled-creates` | 377 / 3,000 | | `claim-never-deleted` | 5 / 3,000 | |
| +| `claim-op-exclusive` | 120 / 3,000 | | `clean-return-identity` | 13 / 3,000 | |
| +| `close-evidence` ‡ | witness; sweep 0 / 3,000 | | `close-waits` ‡ | witness; sweep 0 / 3,000 | |
| +| `closed-marker` ‡ | witness; sweep 0 / 3,000 | | `commit-before-open` | 3 / 3,000 | |
| +| `cover-at-park` | 29 / 3,000 | | `covered-baseline-refused` ‡ | witness; sweep 0 / 3,000 | |
| +| `cut-deadline` | 40 / 3,000 | | `declare-lost-compute` ‡ | witness; sweep 0 / 3,000 | |
| +| `dirty-return` | 1 / 3,000 | | `evidence-from-state` | 2,632 / 3,000 | |
| +| `evidence-whole-tree` ‡ | witness; sweep 0 / 3,000 | | `fence-by-installation` | 303 / 3,000 | |
| +| `fence-etag` | 22 / 3,000 | | `fence-stamp` | 306 / 3,000 | |
| +| `files-carried` | 25 / 3,000 | | `floor-boot-recovery` | 2,563 / 3,000 | |
| +| `foreign-region-uncovered` | 4 / 3,000 | | `fresh-admission` | 11 / 3,000 | |
| +| `fresh-incarnation` | 53 / 3,000 | | `generation-conditional` ‡ | witness; sweep 0 / 3,000 | |
| +| `holderless-park` | 561 / 3,000 | | `legacy-discovery` | 367 / 3,000 | |
| +| `live-set-region` | 2 / 3,000 | | `location-per-incarnation` | 29 / 3,000 | |
| +| `lost-quarantine` ‡ | witness; sweep 0 / 3,000 | | `lost-return-park` | 1 / 3,000 | |
| +| `markers-last` ‡ | witness; sweep 0 / 3,000 | | `newest-l0` ‡ | witness; sweep 0 / 3,000 | |
| +| `obligations-block-ops` | 21 / 3,000 | | `orphan-no-deadline` | 45 / 3,000 | |
| +| `orphan-order` ‡ | witness; sweep 0 / 3,000 | | `park-all-versions` | 585 / 3,000 | |
| +| `park-by-version` | 2,539 / 3,000 | | `park-skip-lock` | 2,733 / 3,000 | |
| +| `participant-rows` | 3 / 3,000 | | `persisted-park-scope` ‡ | witness; sweep 0 / 3,000 | |
| +| `probe-window` ‡ | witness; sweep 0 / 3,000 | | `purge-adopts` | 7 / 3,000 | |
| +| `purge-claim-fence` | 28 / 3,000 | | `purge-journal` | 1,897 / 3,000 | |
| +| `purge-reserve-first` | 2,144 / 3,000 | | `quiet-before-ack` | 152 / 3,000 | |
| +| `recovery-current-inputs` | 37 / 3,000 | | `recovery-generation` | 12 / 3,000 | |
| +| `recovery-pass` | 2,431 / 3,000 | | `registration-recovery` | 2,011 / 3,000 | |
| +| `remote-baseline` ‡ | witness; sweep 0 / 3,000 | | `restore-anchor` | 55 / 3,000 | |
| +| `restore-by-generation` | 126 / 3,000 | | `restore-gap-closed` ‡ | witness; sweep 0 / 3,000 | |
| +| `restore-overlap` ‡ | witness; sweep 0 / 3,000 | | `retirement-ids` | 459 / 3,000 | |
| +| `return-stamp` | 69 / 3,000 | | `revalidate-before-effect` | 14 / 3,000 | |
| +| `revert-journal` | 13 / 3,000 | | `rollback-journal` | 1 / 3,000 | |
| +| `root-advance` | 17 / 3,000 | | `sdk-no-resign` | 12 / 3,000 | |
| +| `seal-by-version` | 1 / 3,000 | | `seal-return` ‡ | witness; sweep 0 / 3,000 | |
| +| `session-scoped-loss` ‡ | witness; sweep 0 / 3,000 | | `sign-at-check` | 16 / 3,000 | |
| +| `sign-before-safeuntil` | 15 / 3,000 | | `source-readiness` | 12 / 3,000 | |
| +| `staging-quiet` | 1 / 3,000 | | `stale-hold-release` | 1 / 3,000 | |
| +| `start-check` | 17 / 3,000 | | `start-check-claim-gen` | 15 / 3,000 | |
| +| `straggler-sweep` | 770 / 3,000 | | `strict-spawn` | 13 / 3,000 | |
| +| `sweep-namespace` | 542 / 3,000 | | `sweep-staging` | 36 / 3,000 | |
| +| `target-park` | 16 / 3,000 | | `timer-canonical` | 2 / 3,000 | |
| +| `timer-freeze` | 2 / 3,000 | | `valid-ltx` | 38 / 3,000 | |
| +| `writer-session` | 7 / 3,000 | | `writes-lost` | 13 / 3,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` |
| @@ -4975,19 +5265,19 @@ subset in the gate. |
| | combination | sweep | partners alone (sweep) | witness | what the model finds | |
| |---|---|---|---|---| |
| -| `purge-claim-fence` + `fence-etag` (**the re-read alone**, rev 7's CC21 as proposed) | 342 / 30,000 | `purge-claim-fence` 23 / 3,000, 235 / 30,000, `fence-etag` 26 / 3,000, 226 / 30,000 | (the two `registration-check` rows below) | a store destroyed under a creating or serving host | |
| -| `registration-check` + `purge-claim-fence` | 274 / 30,000 | `registration-check` 0 / 3,000, `purge-claim-fence` 23 / 3,000, 235 / 30,000 | violated | the same | |
| -| `registration-check` + `fence-etag` | 267 / 30,000 | `registration-check` 0 / 3,000, `fence-etag` 26 / 3,000, 226 / 30,000 | violated | the same | |
| -| `exec-admission` + `hold-op-open` + `start-check-claim-gen` + `exec-writer` | 166 / 30,000, 574 / 100,000 | `exec-admission` 0 / 3,000, `hold-op-open` 0 / 3,000, `start-check-claim-gen` 14 / 3,000, 167 / 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 | |
| +| `purge-claim-fence` + `fence-etag` (**the re-read alone**, rev 7's CC21 as proposed) | not run for rev 7.14 (CPU budget; Paul 2026-10-06) | `purge-claim-fence` 28 / 3,000, `fence-etag` 22 / 3,000 | (the two `registration-check` rows below) | a store destroyed under a creating or serving host | |
| +| `registration-check` + `purge-claim-fence` | not run for rev 7.14 (CPU budget; Paul 2026-10-06) | `registration-check` 0 / 3,000, `purge-claim-fence` 28 / 3,000 | violated | the same | |
| +| `registration-check` + `fence-etag` | not run for rev 7.14 (CPU budget; Paul 2026-10-06) | `registration-check` 0 / 3,000, `fence-etag` 22 / 3,000 | violated | the same | |
| +| `exec-admission` + `hold-op-open` + `start-check-claim-gen` + `exec-writer` | not run for rev 7.14 (CPU budget; Paul 2026-10-06) | `exec-admission` 0 / 3,000, `hold-op-open` 0 / 3,000, `start-check-claim-gen` 15 / 3,000, `exec-writer` 0 / 3,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 | |
| +| `admit-bind-op` + `claim-cas-opid` | not run for rev 7.14 (CPU budget; Paul 2026-10-06) | `admit-bind-op` 0 / 3,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` | 859 / 30,000 | `claim-cas-opid` 0 / 3,000, `revalidate-before-effect` 15 / 3,000, 178 / 30,000 | violated | a stale step destroys a store | |
| -| `strict-spawn` + `evidence-whole-tree` | 175 / 30,000 | `strict-spawn` 9 / 3,000, 110 / 30,000, 374 / 100,000, `evidence-whole-tree` 0 / 3,000, 5 / 30,000 | violated | two writers | |
| -| `touched-incomplete` + `legacy-discovery` | 7,475 / 30,000 | `touched-incomplete` 0 / 3,000, `legacy-discovery` 367 / 3,000, 3,561 / 30,000 | violated | a freed host's residue | |
| -| `declare-lost-compute` + `watchdog-independent` | 1 / 30,000, 3 / 100,000 | `declare-lost-compute` 0 / 3,000, 1 / 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,877 / 30,000 | `fence-stamp` 332 / 3,000, 2,946 / 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 | |
| +| `claim-cas-opid` + `revalidate-before-effect` | not run for rev 7.14 (CPU budget; Paul 2026-10-06) | `claim-cas-opid` 0 / 3,000, `revalidate-before-effect` 14 / 3,000 | violated | a stale step destroys a store | |
| +| `strict-spawn` + `evidence-whole-tree` | not run for rev 7.14 (CPU budget; Paul 2026-10-06) | `strict-spawn` 13 / 3,000, `evidence-whole-tree` witness; sweep 0 / 3,000 | violated | two writers | |
| +| `touched-incomplete` + `legacy-discovery` | not run for rev 7.14 (CPU budget; Paul 2026-10-06) | `touched-incomplete` 0 / 3,000, `legacy-discovery` 367 / 3,000 | violated | a freed host's residue | |
| +| `declare-lost-compute` + `watchdog-independent` | not run for rev 7.14 (CPU budget; Paul 2026-10-06) | `declare-lost-compute` witness; sweep 0 / 3,000, `watchdog-independent` 0 / 3,000 | violated | two writers after a paused or frozen target resumes | |
| +| `fence-stamp` + `hostguard` (no longer combination-only) | not run for rev 7.14 (CPU budget; Paul 2026-10-06) | `fence-stamp` 306 / 3,000, `hostguard` 0 / 3,000 | violated | a stale pass writes host state for a retired installation (INV-6); the witness is what shows the stamp load-bearing against the guard's own check | |
| Every live combination was rerun on the rev 7.9 model; the gate runs |
| every proper subset of the admission four with the witness, which holds |
| @@ -5407,6 +5697,40 @@ 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.15 to 6.22 (0bf2f49f), after joint round 13: no change |
| +requested, six notes.** Rev 6.15 and 6.16 added the persisted park scope |
| +and the holderless sweep; rev 6.21 adopted rev 7.13's seven notes; rev |
| +6.22 answers R13-1 to R13-3 (the run walk across regions, coverage in |
| +exactly four ways with warm entries born covered and |
| +`CoverParkedPredecessors`, the `additional_writes_lost` representation |
| +with one alert per declaration) and keeps E's warm-region check with |
| +note 4's reading. Rev 7.14 encodes all of it (§5.1 step 9, §6.4, §7.14's |
| +operative list, §14.2.2). Notes for platform-1e |
| +(`moves-claim-questions.md`, rev 7.14 heading): **(1)** another region's |
| +sweep while the holderless parking op runs **joins** it, adding its own |
| +scoped chores under the same op id, rather than waiting for |
| +`FreeAfterPark`; the claim's "one CAS queues only scoped remote chores |
| +owned by that op" is read to allow later CASes adding to the op; |
| +**(2)** the sweep's chore is acknowledged, with its straggler pass, only |
| +after the scope's `evidence_at + request_limit`, so a free host's |
| +successor create waits up to the horizon after the sweep found residue; |
| +rev 7.13's sweep acknowledged at once; **(3)** the console's recovery |
| +pass leaves a holderless sweep to the obligation runners and replays only |
| +`FreeAfterPark`, for an op whose chores are all acknowledged (a crash |
| +between the last acknowledgement's CAS and nothing: the CAS is one, so |
| +this is belt and braces); **(4)** INV-20 is the model's statement of |
| +"blocks `free`'s successor create": a create's claim CAS never finds an |
| +obligation outstanding; the create **waits** on the parking op rather |
| +than being refused, and `userCreate` does not even plan one while it |
| +runs; **(5)** the covered-baseline refusal also fires where rev 7.13 |
| +restored nothing: an origin swept under an unfinished admission by rev |
| +7.11's sweep (the `absent-marker-origin` mutation) is a covered local |
| +baseline now, and the recovery refuses with an alert instead of |
| +starting on an empty database; both are INV-2 for the witness, the |
| +refusal is the better failure; **(6)** a warm record's `region` is the |
| +admitted box's, which equals its predecessor record's region in every |
| +reachable warm admission, as 6.22 states; the model records the box's. |
| + |
| **Claim rev 6.13 (b3825827) and 6.14 (dc146058), after joint round 12: |
| no change requested, seven notes.** Rev 6.13 adopted rev 7.12's five |
| notes (the lost-target return is `""`; a probe never marks the host |
| @@ -5900,6 +6224,23 @@ answers the rest and reruns every number. |
| | R6-5 (P3) replayed anchor bytes differ (the encoder's `time.Now()`) | the encoding inputs, timestamp included, are journaled in the install manifest before the PUTs and a replay reuses a current object (§5.1 step 2, §7.6 `building`); `TestFact_R6_5_AnchorReplayBytes` shows identical bytes for identical inputs and different bytes one millisecond apart | |
| | fidelity: compaction deleted the newest level-0 file, creating anchor-required cold restores the library would not | compaction keeps the newest input (§14.2.2); time-based level-0 retention stays deferred (§14.2.6) | |
| +### 22.20 Joint round 13 (claim 1915bac2, moves rev 7.13 1f511c42, model 42af7bfc, library E 47426cc1, selector plan 85aa53f8) |
| + |
| +Round 13 found no P1 and judged E merge-ready; it held A, B, C and F on |
| +four P2s. Claim rev 6.22 (0bf2f49f) answers R13-1 to R13-3; E for round |
| +14 is `feat/hostclaim-r713` at f0127321 (47426cc1 plus rev 6.21 and |
| +6.22), F's code is `feat/hostclaim-genselect` at d7621a29 with plan 7b |
| +rev 3 (c3ea8fbd) and the four R13-1 table cases. |
| + |
| +| finding | rev 7.14 | |
| +|---|---| |
| +| R13-4 (P2) the model's sweep queued bare `sweep` chores on a free claim, with no holderless `parking` op, no persisted incarnation, evidence time or request bound; an agent restart cleared the evidence map and started the horizon again | `obligation.Scope` persisted (bound before the first step, or at the sweep's queuing CAS); a free host's sweep is `{kind: parking, intent.park_sweep: "v1"}` with no exec and no holder, freed by `FreeAfterPark` in its last acknowledgement's CAS; `session:<n>` on a serving host; the create waits, INV-20; rules `persisted-park-scope`, `holderless-park`; witnesses `wParkScopeSurvivesRestart`, `wFreeSweepVsCreate` (§6.4, §7.14 item 9, §14.2.2) | |
| +| R13-2 (P2) publication and coverage described different transitions (traversal bound, warm records, the live predecessor), and coverage composition was incomplete in A | claim rev 6.22's complete algorithm encoded: four coverage mechanisms, warm entries born covered, the publication walk over every entry with the precondition that an entry names the published generation, `CoverParkedPredecessors(region, generations)` selective at the sweep's queuing and acknowledgement CASes (§5.1 step 9, §7.14 items 5 and 6) | |
| +| R13-1 (P2) F rejected the interrupted clean-return recovery; B needed the walk stated precisely | §5.1 step 9 states the run walk: a covered foreign link is passed over, a covered local baseline refuses and alerts; `runBaseline` in the model with `restoreCalc` as the reference; rule `covered-baseline-refused`, witness `wCoveredLocalBaseline`; `TestInterruptedCleanReturn` (R → T → S, then R2 → R → T → S) | |
| +| R13-3 (P2) A lacked the all-target-sessions rule and a representation | `additional_writes_lost` as claim rev 6.22 states it: one `writes_lost` plus a list, unique by `(box, session)`, one alert per declaration; the model's `AdditionalWritesLost` (§5.1 step 9, §7.14 item 2) | |
| +| the seven rev 7.13 notes | all adopted in claim rev 6.21 and 6.22; note 4 with the round's reading (a clean return's first admission is cold) and E's warm-region check kept | |
| +| E verdict requested | round 14: an explicit MERGE-READY on f0127321 | |
| + |
| ### 22.19 Joint round 12 (claim b3825827, moves rev 7.12 dd3e35f6, model af9b89ed, library E 47426cc1) |
| Round 12 found no P1 and judged E merge-ready on static review; it held |