Cache-generation oracle audit

This is a self-review of the oracle expansion. Reviewed code commit: 53ded62d8ef70ccd63b75d0e6dbc0a964f14b17c. This record covers the oracle and coverage-map changes in that commit. It does not claim that the whole cache-eviction bug class is closed. No production code changed in the reviewed commit.

The glossary defines a persisted cache claim as one sync run's expiring authority over one persisted cache generation. The approved on-demand recovery contract in the Electric collection guide requires a run that loses that authority to reload its demanded subsets. The SQLite owner checks transaction-time admission; the persisted owner checks physical-ID notice routing; the Browser owner checks a warm peer and an expired run through a real SQLite database and a controlled coordinator wire.

Generated-history controls

The managed-claim read grammar fixes an initial claim at clock 1000 with a 100 ms lifetime. A peer claims the same physical ID 10–80 ms later. The held read uses clock cuts -9, -1, 0, +1, and +9 ms around the first claim's expiry. The peer remains live at every generated read cut. The model uses half-open claim intervals and computes both expiries from these authored inputs, rather than from the adapter's returned expiry. It varies includeRows and zero to three seeded rows. Six fixed histories reconstruct the reported second-check race and the exact-expiry boundary with both row-inclusion options.

Ablation: Removing the clock cut loses expiry and equality; removing includeRows loses the position-only no-row-read promise; removing row count loses empty and multiple-row membership; removing peer delay loses the independent later claim interval.
Range: The adjacent clock cuts are -1, 0, and +1 ms; 0 and 3 rows bound the generated row count. A peer acquired after the held read, or expired by its own read, is excluded from this grammar rather than silently skipped.
Checkpoint: The real loadResumeSnapshot transaction is held before its claim query. An expired read rejects with no generation-specific SQL beyond claim validation. A live read returns the modeled rows and metadata, while the peer reads the same exact durable rows and metadata. A harmless global catalog query before validation is allowed.

The generation-notice grammar fixes rotation from one physical ID to another. It varies an absent, commit, or reset old notice; old row versions 1 and 10; new row versions 1 and 3; and an absent or present new notice. The four fixed histories reconstruct queued commit/reset delivery with the old version below or above the new version. An old version has no semantic effect when no old commit exists; a new version has no effect when the new notice is absent.

Ablation: Omitting old notices removes the queued-callback case. Omitting the absent-old control loses the rotation-only work baseline. Omitting the absent-new control permits unexplained later work. Omitting either version order permits comparison by row version instead of physical ID. Omitting commit or reset loses one callback path.
Range and exclusion: Versions 1/10 and 1/3 cover the two orderings. The grammar queues any old notice before rotation binds; delivery to an old subscription created only after unsubscribe is outside its legal histories.
Checkpoint: After the queued callback crosses the wrapper's apply mutex, the active subset has exactly its one rotation request and no retired public row. A new notice requests additional source work against the new ID. This stub records requests, not source evidence or a completed snapshot.

Both grammars run the same driver and comparison with a fixed seed and a random seed. The fixed seeds are 2056 (30 runs) and 2069 (24 runs). The package oracle registry accepts direct seed-and-shrink-path replay for each property.

Hostile checks and replay

Temporary source mutants were restored after each run. These outcomes are assertion failures at the intended comparison, not setup errors or timeouts:

Wrong design	Observed result
Accept a claim at its exact expiry (>=)	Both fixed equality histories rejected the resolved read. Generated history shrank to elapsedMs=0, includeRows=false, peerDelayMs=10, rowCount=0.
Read collection metadata before transaction claim validation	Four expired fixed histories failed the generation-specific statement check.
Read key-set evidence before transaction claim validation	All six fixed histories failed the generation-specific statement-order check.
Scan rows for a live includeRows=false read and discard them	The live position-only fixed history failed its row-query count.
Process a queued retired commit after rotation without checking its physical ID	Both fixed commit histories failed because the old notice added source requests. Generated history shrank to old commit/version 1, new version 1, and no new notice.

A temporary harmless sqlite_master read before claim validation passed all six fixed histories. It is outside the claimed generation and does not weaken the first generation-specific statement check. The Browser receiving witness also rejected an unconditional-current-head rotation mutant at its exact head-ID comparison during the initial review campaign.

Direct replay of the expiry mutant used property sqlite-resume.managed-claim-read, seed 2056, path 0:1. It selected only the random-or-replayed property and failed after one test with the same counterexample. Direct replay of the retired-commit mutant used property persistence.generation-notice, seed 2069, path 1:1:1. It likewise selected only that property and failed after one test with the same counterexample.

ORC-001–014 audit

Requirement	Outcome at the reviewed code commit
ORC-001 authority and limits	Applicable. The glossary and approved on-demand recovery contract provide the claim and private-recovery law. Opening prose and the coverage map bound each owner.
ORC-002 independent judgment	Applicable. The SQLite model computes half-open intervals from authored clock/TTL inputs. The notice model expects work by physical identity and presence of a new notice; it does not call the production classifier.
ORC-003 literate responsibilities	Applicable. Each owner states the law before mechanics and places grammar, controlled driver, observations, and checkpoint beside the code. The notice owner claims request isolation, not source settlement.
ORC-004 grammar controls	Applicable to both new generated properties. Reconstruction, ablation, range, and exclusion are recorded above. Conditional axes are identified explicitly.
ORC-005 production path and observation	Applicable. Real SQLite executes the held resume transaction. The real persisted wrapper processes queued notices. Browser wa-sqlite compares two claims, both public snapshots, both claimed durable stores, and a distinct warm source demand after the expired run rotates.
ORC-006 checker calibration	Applicable. The table above records killed mutants and the accepted harmless-catalog variation. The old notice's extra source request fails at its own checkpoint.
ORC-007 fixed/random/replay	Applicable. Both generated properties have equal-budget fixed and random campaigns. Captured seed/path replays reproduced each selected mutant failure directly. Neither property uses fc.commands.
ORC-008 stateful-model minimality	Not triggered: these additions use small stateless predictions over bounded phase histories. The separate TLA+ authority model owns general state exploration.
ORC-009 vocabulary mapping	Applicable. persisted cache claim, persisted cache generation, sync run, demand, and source request follow the glossary. Model clock values stand for the adapter's controlled host clock; notice work counts stand for coordinator request calls.
ORC-010 failure fidelity and cleanup	Applicable. The SQLite driver preserves the primary error through database close. The generated notice driver bounds recovery/cleanup through cleanupPersistedOracle, which preserves an earlier assertion failure. The Browser receiver uses failure-preserving cleanup.
ORC-011 independent second formulation	Applicable. The controlled notice fixture shares one row Map across physical IDs, so it cannot prove exact durable isolation. The Browser receiver supplies real SQLite physical stores and a warm-peer observation. Native coordinator emission remains open below.
ORC-012 review evidence	Applicable. This versioned record names every requirement and is tied to the exact reviewed code commit above. The class remains open at the boundaries below.
ORC-013 boundary witness	Applicable. -1/0/+1 ms fixed cuts distinguish expiry from an inclusive threshold; the inclusive mutant failed. Old versions below and above new versions distinguish physical-ID routing from version-order routing.
ORC-014 controlled-premise handoff	Applicable. The Browser receiver commits the peer write to real SQLite before manually delivering a matching targeted notice. It proves receiver admission, not native coordinator emission. The missing host handoff is assigned below.

Validation on the reviewed code: 798 active SQLite oracle tests passed, with one existing todo; all 30 Browser coordinator-oracle tests passed. Both affected packages typechecked. ESLint reported no errors, and Prettier and git diff --check passed. The pre-commit hook's dependency install received a private-registry 403; the verified code commit bypassed that hook.

Open cells remain in the coverage map: a composed real-SQLite-to-wrapper startup rejection, native Browser coordinator emission and multi-tab/OPFS scheduling, arbitrary notice interleavings, and retired physical-cache reclamation. The SQLite resume owner, Browser coordinator owner, and cache-generation lifecycle owner respectively retain those cells.