Issue #2085: leader close during a source commit#

Review date: 2026-10-08. Source: issue #2085, including its setup, result, and three proposed responses. Baseline commit: f6aba314e44afdfa413d6d70bf8e272dfa67af85. This record describes the uncommitted codex/issue-2085-repro worktree diff against that commit. The source has no file/line references or severity labels and no visible comments. The claim ledger was written before testing and retains source order.

Reviewer assessment#

This is an issue report, not a pull-request review. Its stack trace and failing phase accurately identify the coordinator and persisted wrapper boundaries. The six-run count and proposed remedies are useful hypotheses, but they do not decide the recovery contract. One report does not support a hiring recommendation.

Lossless claim ledger#

confirmed-open means the reported symptom or a valuable question remains open; it does not imply that every variant was reproduced. accepted-design cites existing contract behavior. No item is deferred or called fixed.

Accounting: 11 raw items = 5 confirmed-open + 2 accepted-design + 3 design-decision + 1 stale. There are no duplicates, refutations, fixes, or agreed deferrals.

Law discovery and tension#

Existing law, approved: After a mutating RPC loses transport, the requester retries only when it still knows the same non-null leader ID and term. Unknown or changed leadership yields IndeterminateCommitError; the application reconciles. The browser README and core README state this. The existing fails indeterminate when a committed success is lost across leader change test enforces it. A closed leader can have committed without answering, as the host durable snapshot confirmed; retrying the mutation blindly against the new leader would violate the uncertain-outcome boundary.

Candidate law from the issue: For a source-backed Collection in a surviving tab, a normal close of another tab should not make the surviving sync run permanently unusable. The first source receipt may reject as uncertain. After leadership transfer and reconciliation, a later source commit should settle and the Collection should be ready. This candidate is not an approved product contract. The new assertions intentionally stay RED pending a decision.

The rival policy is application-led reconciliation. It permits the current terminal error and requires the application to inspect durable state and restart or recreate the Collection. The issue's source-backed premise could justify a different owner because the source cursor is durable with the rows, but that does not itself specify who restarts the sync run, whether a public snapshot may remain visible while checking durable state, or how pending applied receipts settle. Both policies agree that the original RPC must not be blindly resent to a replacement leader.

The smallest distinguishing history is the one tested: the leader finishes a durable PersistedTx, its answer is held, the page closes, and the follower takes leadership. The idle-close control keeps all other setup similar and shows that ordinary takeover succeeds. A second necessary branch is close before durability; it remains open. The source of policy authority, rather than the test harness, must choose between automatic and application-led recovery.

Oracle chain and RED evidence#

Exact results on baseline f6aba314e44afdfa413d6d70bf8e272dfa67af85:

• The existing direct-RPC indeterminate test passed: 1 passed, 153 skipped.
• The new controlled candidate test failed at collectionStatus: expected ready, actual error; later source receipt expected fulfilled, actual rejected.
• The new Chromium/OPFS pair yielded 1 passed idle-close control and 1 failed in-flight case. The failed case recorded firstOutcome.errorName = IndeterminateCommitError, term 1→2, collectionStatus = error, the later receipt rejected with the same error, public IDs [crossing], and durable IDs [crossing]. Cleanup completed without secondary failure.
• Browser package TypeScript check passed after installing the relevant locked dependencies from the local cache. The full workspace offline install could not complete because an unrelated Electron tarball was absent; the filtered browser and Electric/e2e dependencies sufficed for these checks.

This is a source-backed manual sync witness and a real host transport witness. It is not an Electric redelivery witness. It does not reproduce the reported nondeterministic 3/6 rate, on-demand hydration, seven Collections, update(), or the leader's active-write error. Those cells remain assigned to the Browser composed owner, persisted-history owner, and live Electric OPFS receiver as stated above.

Oracle guide audit#

The candidate law is encoded for these two finite host histories and enforced at the named public cut; baseline production proves sensitivity. It is not fully encoded for before-durable loss, queued hydration, Electric restart, or all Collections. Under the current approved application-reconciliation contract, RED demonstrates the requested symptom and a policy conflict, not an authorized production defect repair.

Next design decision#

Choose whether a surviving source-backed Collection automatically reconciles an uncertain coordinator commit or whether the application must explicitly restart it. For automatic recovery, specify the durable snapshot and cursor read, first-receipt result, public snapshot during recovery, retry scope, and when the Collection becomes ready; then add before/after-durable and Electric receiver histories before changing production. For application-led recovery, document and test a supported cleanup/recreation sequence that checks durable state and resumes source delivery. A faster page-close rejection can be evaluated separately after the outcome policy is set.

Follow-up: exact-ID source reconciliation#

The preceding ledger and RED observations are the original baseline audit. They are retained in source order. The follow-up chose same-run reconciliation for a source sync transaction when the elected SQLite adapter can certify its outcome. A direct mutating RPC still rejects as indeterminate after an unknown or changed route. The persisted wrapper holds the source applied receipt while the replacement leader checks the immutable txId under the writer lock. An existing ID fulfills the receipt at its original durable position. An absent ID permits one application only when the durable row version and reset epoch still equal the pre-send anchor. An intervening durable write, reset, pruned ID, or unavailable proof retains the original indeterminate error. The bounded recovery keeps the source Collection and mounted live query in the same sync run. The published row and opaque source cursor are one durable transaction.

Updated claim ledger#

The following dispositions supersede the baseline ledger; the original 11 source claims above remain unchanged for loss accounting.

Accounting: 11 original items = 5 confirmed-open + 2 accepted-design + 1 design-decision + 1 fixed-now + 1 stale + 1 already-fixed. There are no refutations, duplicates, or agreed deferrals. The open rows name unproved receiving paths; they are not claims that the bounded repair failed.

Adversarial oracle review ledger#

Two independent reviewers attacked the model, production driver, and receiving schedules. This ledger retains their distinct findings and challenges rather than merging them into the issue ledger.

The reviewers separated product failures, test-integrity defects, a refuted ordering concern, and real receiving gaps. Their high-signal findings changed the oracle and repair. Both would receive a positive reviewer recommendation; neither claimed a passing finite suite proved arbitrary histories.

Law chain, checkpoints, and calibration#

The controlled wrapper oracle is the primary source-lifecycle owner. The SQLite adapter oracle supplies an independent durable ledger. The Browser coordinator oracle owns route and writer-lock order. The OPFS host test is the receiving witness for real browser transport and storage; its manual source is not the Electric SDK. source-reconciliation-repeat also tests orphan metadata through the real Collection sync implementation. The orphan key is absent from loaded rows, so full replacement would clear it. The added internal delegation finds that exact mismatch without exposing the state map to the persistence package.

Verification and remaining boundary#

The focused SQLite CLI contract passed 43 tests; the wrapper suite passed 653 with one existing todo; the Browser coordinator suite passed 158 after its local better-sqlite3 binary was restored from the matching package version. Chromium/OPFS passed all five schedules. Core and Browser TypeScript checks passed. The new orphan-metadata assertion was RED before the fix and GREEN after it. The reconciliation-marker mutant was killed at the first passive public row checkpoint after the peer-before-reconciliation gate and restored. Vitest printed unrelated missing Expo tsconfig diagnostics; its test results above completed.

These are finite same-version, manual-source histories. A live Electric receiving witness, a real-host queued-hydration close, and an active-write leader diagnostic remain outside this evidence. They are recorded in the coverage map with receiving owners. The implementation deliberately keeps an absent ID after another durable write indeterminate, because no contiguous ledger proof can establish that a late source payload will not regress a newer row or cursor. That valid history does not enter same-run recovery.

Follow-up: Electric receiving and prep review#

The preceding verification paragraph records its earlier manual-source cut. The new electric-leader-close.opfs.spec.ts supplies the installed Electric SDK at the reported after-durable boundary. PostgreSQL authors one crossing row. The follower's Electric sync creates its source transaction, and the leader's collection-specific scoped adapter holds only after SQLite applies it. The page then closes without an RPC answer. At the first receipt checkpoint, the original Electric applied receipt has fulfilled in sync run one; the source Collection and mounted live query are ready with the row; the durable row and the exact applied transaction ID agree. The source transaction itself contains the electric:resume set. Its kind, offset, handle, and shape ID equal the first durable resume identity, whose offset has advanced from the empty baseline. A later PostgreSQL row advances the offset again and reaches public, live, and durable rows in the same run. The direct coordinator RPC still reports IndeterminateCommitError. A manual-source Collection owns only the first leader term; this does not model two Electric streams contending in both tabs or seven concurrent Collections.

The first two Electric attempts timed out before the held boundary because the fixture intercepted the root adapter rather than the Collection-specific adapter; the unmounted live query also cleaned itself up. They are setup failures, not RED evidence. The corrected driver reaches the held durable boundary and passes. The complete Electric OPFS suite passed 16 tests with the new witness.

Electric oracle attack ledger#

Two independent oracle reviewers inspected the new receiving law and driver. Each raw suggestion remains distinct even where it overlaps another.

The reviewers correctly separated a setup path, receipt settlement, cursor provenance, and a valid receiving limit. Their findings improved the test without changing the product law. Both would receive a positive reviewer recommendation: the findings were technically accurate, specific, and prioritized by false-green risk.

Electric review loss audit: 10 raw items = 8 fixed-now + 2 duplicate. No Electric review item remains open inside the declared one-provider after-durable history.

Prep review ledger#

The correctness review and simplifier review were read-only. Their raw items appear in source order within each review; C03 and S01 intentionally overlap.

Prep loss audit: 10 raw items = 5 fixed-now + 1 duplicate + 4 already-fixed. There are no omitted footnotes, unagreed deferrals, or remaining prep-review findings. The correctness reviewer found one P2 product bug and one host assertion gap; its proposed narrow repairs were accurate. The simplifier's two wire/type reductions and reset-epoch name were safe, and its four rejected reductions preserved real oracle or trust-boundary value. Both reviews had high signal and would receive positive reviewer recommendations.

Updated law coverage and limits#

The repaired claim is bounded by source-backed immutable transaction IDs, same-version tabs, exact-ID certification under SQLite's writer lock, and an unchanged durable anchor for an absent ID. The wrapper's legal histories cover before/after durability, held receipt, queued hydration, unknown result, local/remote durability failures, later work, equal-row reload, orphan metadata, sparse arrays, and extra array properties. SQLite owns the ledger, version, reset, and cursor decision. Browser coordination owns route and lock order. The five manual-source OPFS schedules observe real transport, publication, live rows, event counts, and exact IDs. The Electric receiver adds the reported provider path for one after-durable crossing and later row. Each owner asserts its promised public observation at the named held, certified, and later checkpoints.

ORC-001/002/003: the contract and its limits appear beside independent models; the Electric expected rows come from PostgreSQL, and no production classifier computes them. ORC-004/007/008: the new host history is fixed and adds no generated grammar or stateful reference model. ORC-005: the held scoped-adapter apply, SDK-authored transaction, original receipt, exact ID, public/live rows, and durable cursor are reached and compared. ORC-006: baseline manual-source terminal failure, the peer-publication mutant, the orphan-metadata shortcut, and sparse-array comparison failure reject plausible wrong designs at their respective checkpoints. A temporary Electric-path mutant that threw the original indeterminate error after a successful exact-ID response reached the first receipt checkpoint and failed: the applied receipt rejected and source/live status became error despite the durable row. The mutant was restored; the Electric test passed again. ORC-009: source transaction, applied receipt, sync run, and publication follow the glossary. ORC-010: the host preserves a primary mismatch separately from cleanup failures and closes its pages and PostgreSQL connection. ORC-011/014: the installed Electric SDK is a second provider formulation and supplies the after-durable premise previously controlled manually. ORC-012/013: the review record names the original crossing, idle/before-durable neighboring histories, hostile wrong designs, and remaining owner cells.

The remaining receiving limits are a real-host queued-hydration close, an active-write leader diagnostic, two Electric streams in both tabs, the reported seven-Collection topology, and other browsers. Direct application update() after recovery is also unobserved because this fixture has no application mutation handler; the later installed Electric row proves source continuation. These are named coverage cells, not evidence of a reachable in-scope counterexample to the certified source receipt law. An absent ID after an intervening durable write still fails closed by design.

Final integrated verification#

The exact reviewed executable head is 013aa2cb788f562e87ffa0bbc10c1a1073dead43. It includes the 362be03006baa210461ce31ba2cf134f3243596b merge of origin/main. The later review-record and changeset commit changes no executable code. At this head, the real SQLite adapter oracle passed 43 tests. The persisted wrapper oracle passed 655 tests with one existing todo. The Browser coordinator oracle passed 158 tests. All five manual-source Chromium/OPFS leader-close schedules passed. The full Electric OPFS suite passed 16 tests. TypeScript checks passed for @tanstack/db, SQLite persistence core, and Browser persistence after the final fixture type correction. The earlier Vitest Expo tsconfig warnings did not fail these suites.

Follow-up: CodeRabbit evaluation and Electron receiving path#

This addendum evaluates CodeRabbit review 5463528038 at reviewed commit 613dbc9e001f6a2b93076375e1fcb05932078eda. Its four inline comments, subclaims, and optional CLI suggestion yield ten source-order items. The exact executable follow-up commit is a1a3dd8c1cecc6761e93f2c7feaf946bc0830b45; this addendum changes no executable code. The earlier verification paragraphs remain historical records for their named commits.

The review had high signal: its lint and timing findings were accurate, and CR-1 exposed a real route inconsistency. Its suggested ownership fence was wrong for a legal same-term history. Fix quality was mixed; the reviewer earns a positive recommendation with that caveat. The final loss audit is ten raw items = three fixed-now + six already-fixed + one refuted as a required process action. No CodeRabbit item is deferred or omitted.

Law, history, path, and checkpoint audit#

For CR-1, exclusive per-Collection Web Lock ownership is the route authority. The Browser oracle captures a real former-owner heartbeat before a no-write release, elects the successor at the same term, queues exact-ID reconciliation behind the writer lock, then delivers the captured heartbeat. It observes the successor's route at the queued cut, an applied-once exact-ID result after release, and the next sequence on a later source write; the former adapter applies nothing. The original handler let reconciliation succeed but made that later write fail. CodeRabbit's fence made reconciliation fail. Both RED runs reached their intended comparisons; the repaired handler passes. The existing queued-transfer history separately checks genuine ownership loss. These are bounded controlled Browser histories, not arbitrary browser scheduling.

For CR-4a/b, the established reconciliation-reload law removes orphan row metadata without duplicate row events and publishes durable value shape even when ordinary change-event equality equates sparse and dense arrays. The wrapper oracle controls loadSubset entry and release. At the held cut, metadata and authored array shapes remain public. At the settled cut, orphan metadata is absent, source and live-query rows have the durable shape, and unchanged rows emitted no duplicate events. The old single-flush assertions failed before reload completion. A skip-publication mutant reached the positive settled comparisons and failed all three cases. The OPFS passive-tab history remains the separate real-browser publication receiver.

CI uncovered a separate Electron receiving gap: the renderer/main IPC bridge did not expose reconcileCommittedTx, so the shared SQLite adapter contract failed at its explicit operation assertion. The bridge now transports the immutable transaction and durable anchor, returns the complete result, and requires protocol v3. The registered SQLite contract exercises exact-ID reconciliation through both in-process handlers and a real Electron main process. A resolved-adapter witness checks distinct Collection modes and schema versions in the reconciliation envelopes; dropping resolution fails at that assertion. An adapter without the optional operation returns unknown without a durable write; a temporary blind-apply-then-unknown mutant changed the durable row and version and failed at the no-write assertion. Tests also reject v1 and v2 peers in both directions and preserve durability error code and path over IPC. The Electron correctness review found the missing error path; its fix passed a test that was RED at the path assertion. The simplifier's only remaining proposal was a shorter forwarding method with no behavior or clarity gain, so the explicit method remains.

The full Electron package passed 163 tests with no type errors. The exact-ID contract passed through a real Electron main process in isolation. The full Browser coordinator suite passed 263 tests, the persisted wrapper suite passed 876 tests with two existing todos, and all five real Chromium/OPFS leader-close schedules passed on the named executable commit. The final affected-file ESLint check had no errors and 37 existing require-await warnings in the large Browser and wrapper oracle files. Electron TypeScript, formatting, and git diff --check passed. An optional broader real-process Electron run had five other failures: two multi-Collection leadership checks and three function-bearing collation cases, so that broader run is not claimed green.

The real-process witness executes the renderer adapter in Vitest and sends its envelope through IPC to Electron main. It does not execute that adapter inside an Electron renderer or cover concurrent requests from multiple renderers in one live main process. A delayed reconciliation IPC reply after main applies is an untested transport history, recorded with the Electron receiving owner in the coverage map. Passing prompt-reply histories do not establish general Electron same-run recovery. The Browser and Electron coverage boundaries stay separate from the original source-backed Collection law.

Follow-up: CodeRabbit review 5463932998#

CodeRabbit reviewed b25d83b50cb24308b793b858bc25eb4918975c6b and reported one inline documentation defect. Its review body also repeated an optional CLI suggestion. The checkbox, run metadata, file inventory, and skipped-file list contained no other findings.

The reviewer made one accurate, precise finding with a minimal correct fix. This is a positive recommendation for targeted documentation review. This review does not establish product-law review depth. The final loss audit is two raw items = one fixed-now + one refuted as a required process action. No item remains open or deferred.

Follow-up: medium-effort review at b4a46a4fe#

The user supplied ten code-reading findings against b4a46a4fe5d3b08edfa4084dc7a46299857f6c60; the review reported no executed checks. The executable repair is d6e2493b17b3f023b30ddef0482bae88f9f674ee. The earlier review records above remain evidence for their named commits. This addendum accounts for each new claim and the oracle attack that followed the repair.

Laws, experiments, and inference#

The model, history, path, and observation boundaries are explicit in those owners. The term model keeps durable term state because a later cold election distinguishes two histories with the same caller memory. The reset checks keep durable position and publicly applied position distinct because the next notification can distinguish them. The controlled Browser channel supplies notice ordering; the real coordinator supplies route transitions. The wrapper adapter supplies held read cuts; the real wrapper supplies Collection and live query publication. These bounded histories establish their asserted cuts, not all browser schedules or arbitrary reset interleavings.

Lossless finding ledger#

The four accepted designs preserve observations or limits already in the README, glossary, and coverage map. None is a deferred in-scope repair. The remaining receiving cells have named owners above; no reachable counterexample to the repaired laws was left known at this head.

Oracle-guide audit for the follow-up#

• ORC-001 to ORC-003: the README, glossary, and opening oracle prose state the laws and bounds; independent durable-term, authored-row, and value-shape ledgers sit beside their grammars, production drivers, public observations, and checkpoints. No production comparator computes the expected prototype.
• ORC-004 and ORC-007: this follow-up adds fixed, controlled histories, not a new important generated property. Existing generated campaigns and replay interfaces are unchanged.
• ORC-005 and ORC-006: the Browser coordinator, real SQLite adapter, persisted wrapper, and Chromium host run production paths. The original route and nested-shape RED checks and the reset fence/public-version mutants fail at public comparisons. Setup and timeout failures are not counted as kills.
• ORC-008 and ORC-009: the durable-term ledger retains state distinguishable by a cold successor; durable and publicly applied positions remain separate. New cross-subsystem terms appear in the glossary.
• ORC-010: controlled gates release in cleanup; the wrapper and host preserve primary failure separately from cleanup diagnostics.
• ORC-011 and ORC-014: real SQLite supplies the durable no-write reservation and version-zero reset premises; Chromium supplies the Web Lock/OPFS election. The joined real-adapter reset/publication and nested-serialization receiving cells remain explicitly open with their owners in the coverage map.
• ORC-012 and ORC-013: this revision-bound record states outcomes and non-applicable generated triggers, original and neighboring histories, hostile wrong designs, and remaining cells. Known/cold successors and both reset notice orders distinguish the reusable boundaries.

Verification and reviewer assessment#

On d6e2493b1, the persisted wrapper oracle passed 662 tests with one existing todo. Its six focused reset tests passed separately. Both reset mutants failed the intended public-row assertions and were restored. The Browser coordinator oracle passed 164 tests after the shared guard extraction. Earlier on the same repair, the DB utils oracle passed 132 tests, Browser coordinator suites 320, Electron suites 128, Node SQLite adapter contract 36, and all six real Chromium/OPFS leader-close histories. Four affected packages typechecked. Changed files passed Prettier and git diff --check; ESLint had zero errors and 52 warnings in test fixtures. Vitest's optional package typecheck emitted workspace rootDir source errors when run alongside tests; standalone package TypeScript checks passed. The tests above ran with that Vitest typecheck disabled. The production source diff at the executable commit is 330 added and 102 deleted lines; tests and contract documentation are reported separately in the commit diff.

The reviewer had high discovery value: passive routing, the missing index, shared bookkeeping, and nested public shape were all useful findings. Proposed fixes were less reliable: memory-only term maximum missed the cold successor, and the retry cap sacrificed a legal reroute. The resume-generation and 90-second claims exceeded the evidence. Recommend hiring for code review, with adversarial history checks before treating a proposed mechanism as the cure.

Final accounting: ten raw findings = six fixed-now (M01, M02, M03, M05, M07, M09) plus four accepted-design (M04, M06, M08, M10). Zero items were dropped, deferred, or left as confirmed-open. Accounting and authorized repairs are complete at the named executable commit; the bounded receiving gaps above remain in the coverage map.

Follow-up: collections CI and CodeRabbit review 5472852817#

This addendum evaluated the complete CodeRabbit review of 3d7bd9e73 and the failed Test (collections) job on that head. The executable repair is ef287d8464e3cbd640ab60098a838ac4384751ab. Earlier entries remain versioned evidence for their own heads. In particular, the earlier sentence that called Electron IPC protocol v3 is superseded: the reviewed and repaired protocol is v4. The Electron README and changeset now say v4, and both directions of the IPC version test reject v3 as well as v1 and v2.

Laws, experiments, and inference#

The reset experiment tests a controlled envelope accepted by the wrapper, not an emitted built-in reset. Its work count is measured, but no elapsed latency or host-size bound follows. The older same-version protocol limit and the separate real SQLite reset premise still apply. The new gap witness is bounded to eager active rows and a recording adapter without pullSince; the Electric fixture repair covers ordinary contiguous peer histories, not the same lost-notice schedule.

Lossless CodeRabbit ledger#

The remaining 17 hidden file comments say LGTM and contain no additional change request. The autofix checkbox and repeated agent prompts add no distinct technical claim. Four raw claims are accounted for: two fixed-now, one accepted-design, and one refuted as a required process action. No item is deferred or silently dropped.

Verification and reviewer assessment#

The original persisted gap witness was RED at an exposed empty Collection and GREEN after the atomic replacement. The no-fence mutant failed the new same-term test at the stale public row. On the executable repair, the full Electric package passed 629 tests, the persisted wrapper oracle passed 664 tests with one existing todo, and Electron IPC passed 58 tests. All three affected packages passed standalone TypeScript checks after the Electric package declarations were built. Affected-file ESLint had zero errors and pre-existing require-await warnings in the large wrapper test; Prettier and git diff --check passed. These local checks do not substitute for the pending required CI checks on the pushed head.

CodeRabbit found a real documentation mismatch and a useful reset-work observation. It assigned major severity to a synthetic receive path without establishing a built-in reset sender, and its one-reload suggestion would lose the old-epoch safety witness. It also treated a deliberately optional generic capability as a supported coordinated-election fallback. Recommend hiring for review work with explicit protocol-history and oracle calibration before accepting proposed fixes. The accounting is complete at the reviewed head; the executable repair is complete for the bounded laws above, with real-host receiving limits retained in the coverage map.

Design grammar and TLC addendum (2026-10-09)#

The new bounded model, runner, case inventory, and exact TLC receipts are in review-evidence/issue-2085-tla/. This is a design experiment, not a TypeScript/SQLite refinement check. The model abstracts one source transaction X, one same-key peer write Y, A/B leadership, passive C, one reset, optional exact-ID pruning, lost and reordered notices, position-only observation, and receipt settlement. The README states legal actions, exclusions, fairness, and public checkpoints; the mapping names each production boundary.

Laws and rival predictions#

TLC exhausted 8 route, 2,866 exact-ID, and 22,746 reset states with no safety error. The same graphs passed the explicitly fair local-progress properties. Thirteen wrong-design cases failed at their named invariant, and six negated reachability controls found the intended lawful histories. The runner rejects a different invariant or a TLC/tool error as a mutant kill.

Two control repairs mattered. A first lost-notice witness marked X lost after C had already reloaded; the retained witness records loss at reconciliation and then a later reload. Pruning initially allowed A to apply the same original request twice; the grammar now excludes that illegal history. Neither was a production defect.

Wrapper receiving witness#

The persisted wrapper oracle now composes X's version-1 exact-ID acknowledgment with a same-key Y at durable version 2, then runs owned resume certification. Its source receipt fulfills in one sync run; public X and durable Y/cursor are both observed; the later snapshot makes key-set evidence incompatible. A temporary collaborator mutant that reported Y's position as X's made that last assertion fail: it returned consistent evidence. The mutation was restored. This covers the wrapper boundary with a controlled coordinator. A real SQLite adapter plus wrapper in one receiving path remains open; the adapter's exact-ID result is separately checked against SQLite.

Candidate law outside the established cut#

A separate TLC challenge deliberately asserts that no old row can be published after durable reset before C has received a reset signal. It fails in seven states: A commits X; B reserves term 2 and resets to empty epoch 1; C receives A's version-1 notice before B's reset signal and publishes X while durable rows are empty. The signal and commit messages come from different owners and may be reordered. C has no new-epoch knowledge at that cut. The built-in coordinator currently has no collection:reset sender, so this is an unresolved proposed cross-tab reset law, not a confirmed PR #2088 product regression. A future sender must define the pre-signal public guarantee and add a real Browser/OPFS receiving witness.

The model is exhaustive only within its stated small grammar. One real host join of missed notice, empty election, and passive public rows remains open. Cross-version peers, concurrent source transactions, multiple Collections, provider cursor semantics, physical crash durability, and Electron IPC reply loss remain outside this TLC claim.

CI follow-up: no-write term reservation during Electric resume (2026-10-09)#

The browser E2E workflow on bfa09cc8a5b010473e4bb31065ebb1870caba057 failed twice in electric-hydration-straddle.opfs.spec.ts after reopening the last tab. Both runs reported Electric persisted resume baseline could not be certified at the preloading checkpoint. The host log recorded the error and public row, but not the generation tuple. The following controlled histories test a specific explanation; the new-head browser run is still required to confirm the host repair.

Law and authority. The atomic-resume contract in the persistence README certifies rows, source cursor, stream position, key set, and reset epoch from one snapshot. A no-write election may reserve a greater durable term with sequence zero while row version and reset epoch remain fixed. That transition does not change rows or the source cursor, so an already certified on-demand baseline remains usable. A committed write or schema reset does change the baseline generation and cannot inherit that certification.

Competing predictions. The old exact (term, seq, rowVersion, resetEpoch) guard marks the harmless election incompatible. The repaired guard accepts a greater term at sequence zero only while row version and reset epoch equal the owned baseline. It continues to reject a changed row version or reset epoch.

Experiments. A focused persisted-wrapper test gives its recording adapter (1, 1, 1, 0) and then (2, 0, 1, 0) during on-demand certification. The old guard was RED at getKeySetEvidence(): incompatible instead of consistent. A second held-snapshot test composes the real SQLite adapter, the persisted wrapper, and a mocked Electric stream. SQLite reserves term 2 at sequence zero, keeps row version 1 and the reset epoch, and retains consistent key-set evidence. With the old guard restored temporarily, this receiving test was RED at the post-up-to-date Collection checkpoint: error instead of ready. Restoring the narrow guard made both GREEN. The existing held-snapshot committed-write and schema-reset tests remain negative controls.

Scope and verification. The full persisted wrapper oracle passed 666 tests with one existing todo; the full Electric package passed 630 tests. Both affected packages passed standalone TypeScript checks. ESLint reported zero errors after removing an unnecessary optional-method guard, with 24 existing fixture warnings in the large persisted oracle. The local Electric witness uses real in-memory SQLite and a mocked ShapeStream. It does not enact the Chromium/OPFS restart, Web Lock election, or live Electric delivery; the new head's browser E2E owns that receiving result. The coverage map records this join and its remaining host limit.