diff --git a/.changeset/cleanup-discarded-rows-stay-cleared.md b/.changeset/cleanup-discarded-rows-stay-cleared.md new file mode 100644 index 0000000000..607156818d --- /dev/null +++ b/.changeset/cleanup-discarded-rows-stay-cleared.md @@ -0,0 +1,5 @@ +--- +'@tanstack/db': patch +--- + +An explicit `cleanup()` now keeps the optimistic rows of a transaction that is still persisting cleared after the Collection restarts. Previously, a write made after the restart brought those rows back, so a row that cleanup had discarded reappeared. The transaction still holds its Collection until it settles. diff --git a/docs/contributing/oracle-coverage.md b/docs/contributing/oracle-coverage.md index c66b169a7b..f6b172febb 100644 --- a/docs/contributing/oracle-coverage.md +++ b/docs/contributing/oracle-coverage.md @@ -2093,7 +2093,7 @@ generic visitor behavior outside the named collectors. | ------------------------------------------ | ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | | Ordered relations and BTree | [top-K relation oracle](https://github.com/TanStack/db/blob/main/packages/db-ivm/tests/operators/topk-relation-oracle.test.ts), [fractional-index window moves](https://github.com/TanStack/db/blob/main/packages/db-ivm/tests/operators/topKWithFractionalIndex-oracle.test.ts), [BTree/Map](https://github.com/TanStack/db/blob/main/packages/db/tests/btree-map-oracle.test.ts), [incrementalization laws](https://github.com/TanStack/db/blob/main/packages/db-ivm/tests/incrementalization-law-oracle.property.test.ts) | Independent ordered relations and cumulative signed output. Each generated incrementalization campaign sums the checker's delivery counts and requires one atomic delivery per checkpoint and more split deliveries than an unsplit run makes; a checker that stops splitting fails all six campaigns. Most ordered steps edit the previous world by one removal or insertion, and a reconstruction check counts promotions of retained rows over the executed fixed campaign (25 global and 21 per parity at 100 runs; independent worlds gave 2 and 2). A type test fixes `join(other, type)`'s nullable pair sides for every join type. Top-K consolidation compares same-key values without hashing, including cyclic replacements and fresh transient cancellation. The fractional-index test checks an empty output message for a window move after all rows retract; it does not prove downstream lazy acquisition. The [distinct incrementalization extension](../../packages/db-ivm/tests/distinct-incrementalization-oracle.property.test.ts) recomputes unique immutable `{id: string, value: integer}` selections across real hash collisions, with two unequal collision members and a constructively verified noncolliding anchor. Its shared [model and grammar](../../packages/db-ivm/tests/distinct-incrementalization-oracle.ts) vary collision-member order, atomic versus separate insertion, duplicate support, partial and last removal, replacement, cancellation, and reinsertion, with a noncolliding anchor. The existing incrementalization checker compares net weighted deltas and retained rows after every logical batch in atomic and legal unit-split D2 deliveries, for selected-value and default-tuple distinct. The [public receiving witness](../../packages/db/tests/query/distinct-collision-oracle.test.ts) checks the same law and histories after every applied source transaction through ordered and unordered live-query Collections; the [reported seeded pair](../../packages/db/tests/query/distinct-reported-collision.test.ts) replays that shared judgment. Each campaign declares and measures collision coexistence, duplicate support, partial removal, last removal, and reinsertion separately for its receiving path. The original hash-only operator, equality buckets with shared output keys, and counts capped at one all fail value comparisons. These checks do not promise representative choice for unselected fields, intermediate source-transaction publications, framework render scheduling, arbitrary payload types, or collision freedom of the digest. The [issue 2306 audit](oracle-reviews/2026-10-30-distinct-collisions.md) records RED, GREEN, mutants, bounds, and byte cost. The wider representative and includes receiving grammars are recorded under [Distinct collision review extension](#distinct-collision-review-extension-2026-10-30). Other hash-based operators remain outside this distinct repair; the Index structural-collision trace is recorded there with its owner. Algebra does not specify client readiness. The BTree/Map oracle checks point operations, neighbor pairs, and full, partial, boundary, exclusive-high, and empty range scans for integer keys and node sizes 4–8. It does not check balance or space, and it assumes consistent comparators ([code-weight BTree review](oracle-reviews/code-weight-btree-trim.md)). The generated groupBy law compares JSON values; a fixed contract test in `packages/db-ivm/tests/operators/groupBy.test.ts` records that after a delete, `min` and `max` return a value hash-equal to a remaining member, not necessarily the remaining instance (`-0` for `0`, an equal Date), which is why the query compiler keeps its own exact-value keys. It checks both insertion orders, reads the group's row by integrating output multiplicities, deletes the minimum and the maximum, and shows that an aggregate input that tells the rows apart returns the remaining instance, for -0/0 in both directions and for both `min` and `max`. The contract holds while every member has positive multiplicity. It records the current behavior separately: the delete's retraction is the last record a shared hash entry gets, so the deleted instance comes back in either insertion order, for -0/0 in either direction and for an equal Date. For -0/0 and equal Dates the contract assertions only show hash equality, which is all the contract promises. Open: the incrementalization law's value policy compares JSON and clones by `structuredClone`, so no generated history sees -0 or Date identity; a value-identity policy with -0/0 and equal-time Dates would generalize this fixed contract. | | Includes and publication | [cross-formulation](https://github.com/TanStack/db/blob/main/packages/db/tests/query/includes-cross-formulation-oracle.property.test.ts), [temporal](https://github.com/TanStack/db/blob/main/packages/db/tests/query/includes-temporal-oracle.test.ts), [Collection includes](https://github.com/TanStack/db/blob/main/packages/db/tests/query/includes-collection-oracle.property.test.ts), [architecture and complete suite map](https://github.com/TanStack/db/blob/main/packages/db/src/query/live/ARCHITECTURE.md#executable-contracts) | Per-parent/flat-join/partition relations, callback-time rows, nested values, and route histories. Fragmented lazy-demand consolidation covers delta growth and successful, rejected/retried, and obsolete replacements at the Collection request boundary; it observes exact key unions and abort checkpoints. A compiled-includes fixture makes adapter unload evict owned child rows and proves a rejected union cannot remove established public child rows. Retry after that terminal live-query failure remains covered at the acquisition boundary; no automatic in-place recovery is claimed. Observe raw promised order; fresh queries do not establish continuous publication safety. The temporal owner's source-readiness grammar enumerates every legal order of delivery, settlement, source readiness, and one later change for a source whose Collection readiness lags its settled subsets. It checks live-query readiness, preload settlement, and visible rows for direct, single-result, ordered-window, include-child, lazy-join, and eager-root sources; `queryOnce` results for the direct and eager-root shapes; `toArrayWhenReady()` and `stateWhenReady()` results for a read started after rows are visible but before readiness, over the direct, single-result, and eager-root shapes (and the lazy join for `toArrayWhenReady()`); and Effect `skipInitial` deltas for the direct, lazy-join, and eager-root shapes, and every on-demand cell of every consumer is crossed with a truncate or (join and include) a parent rekey before settlement. Each on-demand cell also compares its consumer with a metamorphic twin over a source that is ready from its start, which does not rely on the model's eager/on-demand rule. A live-query observer test checks that a hydration seed hands off at subset settlement, and an Electric test checks that a ready progressive query's rows update only at the full sync's swap. Effects over an ordered window or an include have no grammar. It rejects both a design that waits for every source's Collection readiness and one that ignores source readiness. Electric live-query tests are the receiving witnesses for a real progressive source and an on-demand source that is ready before its subset loads; a React Suspense test checks that Suspense and `isReady` release together. Other framework adapters have no Suspense witness. | -| Collection lifecycle | [mutation startup](https://github.com/TanStack/db/blob/main/packages/db/tests/collection-mutation-startup.test.ts) (fixed tests; no oracle owner (tracked in #2264)), [change-event history](https://github.com/TanStack/db/blob/main/packages/db/tests/change-event-history-oracle.test.ts), [sync publication reentrancy](https://github.com/TanStack/db/blob/main/packages/db/tests/collection-sync-reentrancy-oracle.test.ts), [history](https://github.com/TanStack/db/blob/main/packages/db/tests/collection-subscription-lifecycle-history-oracle.property.test.ts), [publication](https://github.com/TanStack/db/blob/main/packages/db/tests/collection-subscription-lifecycle-publication-oracle.property.test.ts), [replay](https://github.com/TanStack/db/blob/main/packages/db/tests/collection-subscription-replay-oracle.property.test.ts), [effect disposal](https://github.com/TanStack/db/blob/main/packages/db/tests/effect-disposal-oracle.test.ts), [GC and persisting transactions](https://github.com/TanStack/db/blob/main/packages/db/tests/collection-gc-transaction-oracle.property.test.ts), [GC retention boundaries](https://github.com/TanStack/db/blob/main/packages/db/tests/collection-gc-retention-oracle.property.test.ts), [shared GC model](https://github.com/TanStack/db/blob/main/packages/db/tests/collection-gc-retention-oracle.ts), [GC mutation projection](https://github.com/TanStack/db/blob/main/packages/db/tests/collection-gc-mutation-oracle.property.test.ts), [native idle receiver](https://github.com/TanStack/db/tree/main/packages/db/e2e/collection-gc), [initial GC review evidence](oracle-reviews/pr-2258-gc-retention.md), [second GC review and decisions](oracle-reviews/pr-2258-gc-retention-round2.md), [interaction and mutation receiving evidence](oracle-reviews/pr-2258-gc-retention-round3.md), [GC checker calibration](https://github.com/TanStack/db/blob/main/packages/db/tests/collection-gc-retention-oracle.test.ts), [Electric confirmation receiver](https://github.com/TanStack/db/blob/main/packages/electric-db-collection/e2e/collection-gc.e2e.test.ts), [PR #1902 review](oracle-reviews/pr-1902-change-event-history.md), [batch-order decision review](oracle-reviews/change-event-batch-order.md), [absent-key insert review](oracle-reviews/2026-10-02-insert-for-absent-key.md) | Core Collection `insert`/`update`/`delete` admission while `startSync:false` is idle; complete public-row/change-message agreement across bounded one- and two-key histories plus replayable four-key campaigns, where every message must be valid for a strict consumer (insert only for an absent key, update or delete only for a present one; [absent-key insert review](oracle-reviews/2026-10-02-insert-for-absent-key.md)); a two-key deferred sync history checks each key's causal insert/update/delete trace while allowing any cross-key interleaving. Reversing all deferred messages fails that check; reversing each sync transaction's distinct-key messages passes. Queued duplicate admission and cancellation, ownership and phase histories, exact caller/error/publication evidence, and late completion and restart have separate witnesses. Generated deferred histories with cancellation or reentrant callbacks need a witness in the change-event history owner before claiming general batch-shape coverage. Every bounded change-event history, and about half of each generated campaign, runs again on a local-only Collection that ends with `reload()`: it must resolve with the Collection `ready`, the change-message mirror of valid messages must equal the public rows, the public rows must equal the history's kept rows (maintainer decision: a local-only reload keeps the user's writes, and `initialData` loads only into a Collection that starts empty), and a later write must reach both. The adapter that re-inserted `initialData` in each run failed 210 histories (a crash when a kept row changed, or a mix of kept rows and `initialData`); a reset to `initialData` fails 344, and loading `initialData` whenever the Collection is empty fails 45 (a history that deleted every row). Query write utilities and effect self-dependent disposal remain separate contracts. During a truncate, a ready callback can write to any key after a prior optimistic request. Each subscriber, with or without initial state or a filter, must receive valid messages after the Collection is ready and end at the Collection's rows. A ready callback that throws while entering sync surfaces when the sync function returns, whether it calls markReady or commits a truncate ([round 3 follow-ups](oracle-reviews/2026-10-05-round-3-followups.md)). Callback rollbacks, non-optimistic callback writes, and several writing callbacks remain open ([ready-callback truncate review](oracle-reviews/2026-10-05-truncate-ready-callback-delete.md)). The GC property (`collection-lifecycle.gc-persisting-transaction`) checks on a fake clock that automatic garbage collection retires a Collection only after `gcTime` with no subscriber and no persisting transaction, that the delay restarts when the last transaction completes or fails, and that explicit `cleanup()` still retires it while a transaction persists. Histories run over two Collections, with inserts through one Collection's `onInsert` or through a manually committed transaction that touches both. After each subscribe, unsubscribe, insert, settlement, and clock step it compares each Collection's `cleaned-up` status and each persisting row's visibility with an independent deadline model. `main` before the fix, a hold that never restarts the delay, a restart only on completion, and a restart only for the first Collection a transaction touched each fail it. The companion `collection-lifecycle.gc-retention-boundaries` property separates elapsed eligibility from host idle delivery. Its shared reference model checks the absolute 50ms startup/preload handoff, real last unsubscribe, pending versus persisting transactions, delayed commit, success/failure/rollback, surviving siblings, disabled GC, and old idle work after renewal. Generated configured delays are 1, 10, 49, 50, 51, and 100ms; observations include immediately before and at the independent deadline. Eager sync and write-started sync both run. A Chromium receiving driver uses the same model/checker with native idle delivery and cancellation and controlled elapsed timers. It records the actual budget core reads and checks public status at core delivery and a usable native observation opportunity. Exact wall-clock cleanup latency is not promised. Paced mutations, offline transaction restoration, live-query Collections, and actual Electric `awaitTxId` plus provider delivery are not generated by these GC owners. The boundary grammar now generates repeated warm preloads over queued idle and persisting holds, successful and failed cold preloads as first or last releases, both sibling settlement orders, and pending drafts held by subscriptions. Held adapter cleanup crosses settlement with surviving pending or persisting siblings, both before and after cleanup settlement. Exact key comparisons reject leftover settled rows and cleanup resurrection; tracked transaction identities still match unsettled transactions. The 250-history fixed and random campaigns require all 33 declared states. Alongside the 15 focused grammar, constructive interaction histories combine up to seven transactions and three subscribers, delayed commit, three persisting siblings, non-FIFO settlement and preload between releases. Automatic GC also starts held or rejecting adapter cleanup, checks synchronous row discard before adapter settlement, and rejects pending-sibling resurrection. The shared model additionally receives direct updates/deletes, shared update/delete and cancelled insert/delete ownership with a surviving peer update through `collection-lifecycle.gc-mutation-shapes`. Its independent source/intent projection checks exact keys and values across completion/failure/rollback, both Collection orientations and subscriber states; each 150-history campaign requires all 11 declared states. The maintainer chose first-usable-idle retirement as a fixture scheduling assumption, not a public liveness guarantee. The maintainer also chose caller-owned pending draft visibility: keep a subscription; restart after GC does not promise draft restoration. The boundary grammar therefore does not establish post-GC draft restoration, paced/offline restoration, or arbitrary cleanup/source-recovery histories. A real Electric/Postgres receiving driver now crosses gcTime 10/100ms with absent/last-unsubscribed owners, holds an assigned uncommitted txid across the unheld deadline, and observes pending caller, persisting phase, optimistic row, genuine confirmation, successful settlement, synced row, renewed GC and idle delivery. Its 12 paths retain four one-write cases and add eight two-write cases with separate real SQL transactions and both local settlement orders. A genuine acknowledgement releases only one hold; the other SQL transaction remains open beyond the first-release deadline. It shares the model/checker and rejects no-hold and first-release runtime mutants. Native host and real provider are witnessed separately; their combined browser/provider schedule, three-or-more provider writers, provider failure/recovery and persistence wrappers remain outside these bounded receiving histories. The Collection lifecycle GC owners still use fresh disjoint optimistic keys. Before claiming the combined same-key rollback-cascade or confirming-sync-queue law with GC, this owner needs a generated receiving history that crosses those semantic owners at retention and cleanup checkpoints. The history owner's demand-change grammar (`demandChangeLifecycleHistoryArbitrary`, a fixed seed and the random campaign `subscription-lifecycle.demand-change`) adds a third demand, a `replace` command (`replaceSnapshots`: a held replacement whose own load did not fail covers the owners it replaces, law 10), and a `change` command that retires several owners through one `releaseSnapshot(...wheres)` call; the model judges an open replay once after the whole change (law 9). Declared reach: a change during a replay, a replacement covering a failed owner, and a change whose verdict between releases would differ. Per-release judging, first-release-alone, and batching only two-owner changes each fail it. A covered owner's failed replay load reports `loadSubset:error` whatever its settlement order (the model's existing reporting rule; suppressing the last settler fails it), and a prompt cancellation of a covered owner settles the replay as any settlement does. An aborted held replacement covers nothing: the abort ended its load before it applied (maintainer decision: an abort ends the load; law 10), so its replaced owner's failure keeps the replay failed (two 30-times counterexamples, now `keeps a replay failed when a replacement aborted after its replaced owner failed` and its peer-loaded twin; RED on the first simplification, which counted the aborted replacement as covering; a mutant that drops the check fails both). The controller always aborts and releases a segment together, so it never makes that case. An abort ends the load (maintainer decision): the history model's `abort`, and a truncate that replaces an attempt, stop that attempt's gating at once in both `manual` and `reject` cancellation; an owner whose attempt the abort ended before it settled owes the replay nothing, and a rejection after the abort decides nothing (a failure settled before the abort stays). The publication model finishes a replacement at an abort, and the replay oracle's newer attempt drops the older attempts' pending loads. A synchronous throw from `loadSubset` is a rejection (maintainer decision): an acquisition that core releases, also in the acquisition-cell and replay witnesses. RED on 2bc79fc7c: 18 lifecycle tests, 1 refinement test. Mutants that fail: a replay that waits for an aborted load (14), an aborted rejection reported as `loadSubset:error` (19), an aborted load that still holds readiness (17). | +| Collection lifecycle | [mutation startup](https://github.com/TanStack/db/blob/main/packages/db/tests/collection-mutation-startup.test.ts) (fixed tests; no oracle owner (tracked in #2264)), [change-event history](https://github.com/TanStack/db/blob/main/packages/db/tests/change-event-history-oracle.test.ts), [sync publication reentrancy](https://github.com/TanStack/db/blob/main/packages/db/tests/collection-sync-reentrancy-oracle.test.ts), [history](https://github.com/TanStack/db/blob/main/packages/db/tests/collection-subscription-lifecycle-history-oracle.property.test.ts), [publication](https://github.com/TanStack/db/blob/main/packages/db/tests/collection-subscription-lifecycle-publication-oracle.property.test.ts), [replay](https://github.com/TanStack/db/blob/main/packages/db/tests/collection-subscription-replay-oracle.property.test.ts), [effect disposal](https://github.com/TanStack/db/blob/main/packages/db/tests/effect-disposal-oracle.test.ts), [GC and persisting transactions](https://github.com/TanStack/db/blob/main/packages/db/tests/collection-gc-transaction-oracle.property.test.ts), [GC retention boundaries](https://github.com/TanStack/db/blob/main/packages/db/tests/collection-gc-retention-oracle.property.test.ts), [shared GC model](https://github.com/TanStack/db/blob/main/packages/db/tests/collection-gc-retention-oracle.ts), [GC mutation projection](https://github.com/TanStack/db/blob/main/packages/db/tests/collection-gc-mutation-oracle.property.test.ts), [native idle receiver](https://github.com/TanStack/db/tree/main/packages/db/e2e/collection-gc), [initial GC review evidence](oracle-reviews/pr-2258-gc-retention.md), [second GC review and decisions](oracle-reviews/pr-2258-gc-retention-round2.md), [interaction and mutation receiving evidence](oracle-reviews/pr-2258-gc-retention-round3.md), [GC checker calibration](https://github.com/TanStack/db/blob/main/packages/db/tests/collection-gc-retention-oracle.test.ts), [Electric confirmation receiver](https://github.com/TanStack/db/blob/main/packages/electric-db-collection/e2e/collection-gc.e2e.test.ts), [PR #1902 review](oracle-reviews/pr-1902-change-event-history.md), [batch-order decision review](oracle-reviews/change-event-batch-order.md), [absent-key insert review](oracle-reviews/2026-10-02-insert-for-absent-key.md) | Core Collection `insert`/`update`/`delete` admission while `startSync:false` is idle; complete public-row/change-message agreement across bounded one- and two-key histories plus replayable four-key campaigns, where every message must be valid for a strict consumer (insert only for an absent key, update or delete only for a present one; [absent-key insert review](oracle-reviews/2026-10-02-insert-for-absent-key.md)); a two-key deferred sync history checks each key's causal insert/update/delete trace while allowing any cross-key interleaving. Reversing all deferred messages fails that check; reversing each sync transaction's distinct-key messages passes. Queued duplicate admission and cancellation, ownership and phase histories, exact caller/error/publication evidence, and late completion and restart have separate witnesses. Generated deferred histories with cancellation or reentrant callbacks need a witness in the change-event history owner before claiming general batch-shape coverage. Every bounded change-event history, and about half of each generated campaign, runs again on a local-only Collection that ends with `reload()`: it must resolve with the Collection `ready`, the change-message mirror of valid messages must equal the public rows, the public rows must equal the history's kept rows (maintainer decision: a local-only reload keeps the user's writes, and `initialData` loads only into a Collection that starts empty), and a later write must reach both. The adapter that re-inserted `initialData` in each run failed 210 histories (a crash when a kept row changed, or a mix of kept rows and `initialData`); a reset to `initialData` fails 344, and loading `initialData` whenever the Collection is empty fails 45 (a history that deleted every row). Query write utilities and effect self-dependent disposal remain separate contracts. During a truncate, a ready callback can write to any key after a prior optimistic request. Each subscriber, with or without initial state or a filter, must receive valid messages after the Collection is ready and end at the Collection's rows. A ready callback that throws while entering sync surfaces when the sync function returns, whether it calls markReady or commits a truncate ([round 3 follow-ups](oracle-reviews/2026-10-05-round-3-followups.md)). Callback rollbacks, non-optimistic callback writes, and several writing callbacks remain open ([ready-callback truncate review](oracle-reviews/2026-10-05-truncate-ready-callback-delete.md)). The GC property (`collection-lifecycle.gc-persisting-transaction`) checks on a fake clock that automatic garbage collection retires a Collection only after `gcTime` with no subscriber and no persisting transaction, that the delay restarts when the last transaction completes or fails, and that explicit `cleanup()` still retires it while a transaction persists. Its owned production is `lifecycle.ts` and the settlement restarts in `Transaction.commit`, `Transaction.rollback`, and `Transaction.touchCollection` (`transactions.ts`). Clock steps are 1, 20, 60, and 120 ms. Before `gcTime` no retirement is owed. From `gcTime` to `gcTime` + 20 ms either outcome is allowed, since exact cleanup latency is not promised. From `gcTime` + 20 ms retirement is owed. A retirement two milliseconds early is rejected; one millisecond early is not observed at the 99 ms checkpoint and survives as indistinguishable from `gcTime`. Histories run over two Collections, with inserts through one Collection's `onInsert` or through a manually committed transaction that touches both. After each subscribe, unsubscribe, insert, settlement, and clock step it compares each Collection's `cleaned-up` status and each persisting row's visibility with an independent deadline model. `main` before the fix, a hold that never restarts the delay, a restart only on completion, and a restart only for the first Collection a transaction touched each fail it. Seven constructed histories, one or more for each of its seven declared reach states, enter those states in every campaign, so its reach gate does not depend on the seed; half of each campaign's histories are constructed, and the reach counts include the constructed histories, so a floor of 1 does not show what the generated histories reach alone. GC that ignores subscribers fails the fixed-seed and random campaigns. The companion `collection-lifecycle.gc-retention-boundaries` property separates elapsed eligibility from host idle delivery. Its shared reference model checks the absolute 50ms startup/preload handoff, real last unsubscribe, pending versus persisting transactions, delayed commit, success/failure/rollback, surviving siblings, disabled GC, and old idle work after renewal. Generated configured delays are 1, 10, 49, 50, 51, and 100ms; observations include immediately before and at the independent deadline. Eager sync and write-started sync both run. A Chromium receiving driver uses the same model/checker with native idle delivery and cancellation and controlled elapsed timers. It records the actual budget core reads and checks public status at core delivery and a usable native observation opportunity. Exact wall-clock cleanup latency is not promised. Paced mutations, offline transaction restoration, live-query Collections, and actual Electric `awaitTxId` plus provider delivery are not generated by these GC owners. The boundary grammar now generates repeated warm preloads over queued idle and persisting holds, successful and failed cold preloads as first or last releases, both sibling settlement orders, and pending drafts held by subscriptions. Held adapter cleanup crosses settlement with surviving pending or persisting siblings, both before and after cleanup settlement. Exact key comparisons reject leftover settled rows and cleanup resurrection; tracked transaction identities still match unsettled transactions. The 250-history fixed and random campaigns require all 33 declared states. Alongside the 15 focused grammar, constructive interaction histories combine up to seven transactions and three subscribers, delayed commit, three persisting siblings, non-FIFO settlement and preload between releases. Automatic GC also starts held or rejecting adapter cleanup, checks synchronous row discard before adapter settlement, and rejects pending-sibling resurrection. The shared model additionally receives direct updates/deletes, shared update/delete and cancelled insert/delete ownership with a surviving peer update through `collection-lifecycle.gc-mutation-shapes`. Its independent source/intent projection checks exact keys and values across completion/failure/rollback, both Collection orientations and subscriber states; each 150-history campaign requires all 11 declared states. The maintainer chose first-usable-idle retirement as a fixture scheduling assumption, not a public liveness guarantee. The maintainer also chose caller-owned pending draft visibility: keep a subscription; restart after GC does not promise draft restoration. The boundary grammar therefore does not establish post-GC draft restoration, paced/offline restoration, or arbitrary cleanup/source-recovery histories. A real Electric/Postgres receiving driver now crosses gcTime 10/100ms with absent/last-unsubscribed owners, holds an assigned uncommitted txid across the unheld deadline, and observes pending caller, persisting phase, optimistic row, genuine confirmation, successful settlement, synced row, renewed GC and idle delivery. Its 12 paths retain four one-write cases and add eight two-write cases with separate real SQL transactions and both local settlement orders. A genuine acknowledgement releases only one hold; the other SQL transaction remains open beyond the first-release deadline. It shares the model/checker and rejects no-hold and first-release runtime mutants. Native host and real provider are witnessed separately; their combined browser/provider schedule, three-or-more provider writers, provider failure/recovery and persistence wrappers remain outside these bounded receiving histories. The Collection lifecycle GC owners still use fresh disjoint optimistic keys. Before claiming the combined same-key rollback-cascade or confirming-sync-queue law with GC, this owner needs a generated receiving history that crosses those semantic owners at retention and cleanup checkpoints. The history owner's demand-change grammar (`demandChangeLifecycleHistoryArbitrary`, a fixed seed and the random campaign `subscription-lifecycle.demand-change`) adds a third demand, a `replace` command (`replaceSnapshots`: a held replacement whose own load did not fail covers the owners it replaces, law 10), and a `change` command that retires several owners through one `releaseSnapshot(...wheres)` call; the model judges an open replay once after the whole change (law 9). Declared reach: a change during a replay, a replacement covering a failed owner, and a change whose verdict between releases would differ. Per-release judging, first-release-alone, and batching only two-owner changes each fail it. A covered owner's failed replay load reports `loadSubset:error` whatever its settlement order (the model's existing reporting rule; suppressing the last settler fails it), and a prompt cancellation of a covered owner settles the replay as any settlement does. An aborted held replacement covers nothing: the abort ended its load before it applied (maintainer decision: an abort ends the load; law 10), so its replaced owner's failure keeps the replay failed (two 30-times counterexamples, now `keeps a replay failed when a replacement aborted after its replaced owner failed` and its peer-loaded twin; RED on the first simplification, which counted the aborted replacement as covering; a mutant that drops the check fails both). The controller always aborts and releases a segment together, so it never makes that case. An abort ends the load (maintainer decision): the history model's `abort`, and a truncate that replaces an attempt, stop that attempt's gating at once in both `manual` and `reject` cancellation; an owner whose attempt the abort ended before it settled owes the replay nothing, and a rejection after the abort decides nothing (a failure settled before the abort stays). The publication model finishes a replacement at an abort, and the replay oracle's newer attempt drops the older attempts' pending loads. A synchronous throw from `loadSubset` is a rejection (maintainer decision): an acquisition that core releases, also in the acquisition-cell and replay witnesses. RED on 2bc79fc7c: 18 lifecycle tests, 1 refinement test. Mutants that fail: a replay that waits for an aborted load (14), an aborted rejection reported as `loadSubset:error` (19), an aborted load that still holds readiness (17). | | Paced mutations | [virtual-clock oracle](https://github.com/TanStack/db/blob/main/packages/db/tests/paced-mutations-oracle.test.ts) | `createPacedMutations` with queue front/back options, bounded waiting capacity at zero and one, cleanup draining in FIFO/LIFO order after a held write, cleanup timing at the configured wait for immediate writes, admitted writes after separate Collection cleanup, debounce and throttle schedules with explicit and omitted options, and first-leading throttle execution at epoch zero. Finite histories compare optimistic rows, returned transaction identity and receipt outcome, execution order and virtual-clock time. Held writes verify queue serialization. Leading-only throttle and debounce witnesses reject skipped calls immediately with their named dropped-call errors, including omitted edges, both edges disabled, and same-row rollback while a prior write is held. Capacity witnesses cover overflow rejection, distinct-key optimistic rollback, same-key admitted-write survival, and in-flight versus waiting admission. Cleanup witnesses check repeated queue cleanup, eventual admitted receipt settlement, direct queue strategy rejection of new callbacks, public post-cleanup rollback with `QueueDisposedError`, pending debounce transactions that wait until the last call's quiet edge after separate Collection cleanup, and a trailing throttle timer that runs at its regular edge after separate Collection cleanup. Deferred custom queue and batch callbacks check compatibility with `void` and `false` execute results, respectively. Frozen options verify factory non-mutation; a mutable option witness checks that debounce uses its construction-time trailing setting. Throwing `onMutate` histories check leading-edge reuse before any row change, failed-row restoration when a pending transaction already has admitted work, eligible leading writes behind a held handler, and throttle pending merges at the throw, start, receipt, and later-timer cuts. New debounce/throttle admission after cleanup, manual commit of a strategy-owned transaction, longer throwing/reentrant bursts, failed persistence, broader capacities and schedules remain outside this owner. | | React paced-mutation render cuts | [render-cut oracle](https://github.com/TanStack/db/blob/main/packages/react-db/tests/usePacedMutations-render-cuts-oracle.test.tsx), [PR #2170 review](oracle-reviews/pr-2170-react-paced-render-cuts.md) | `usePacedMutations` publishes callbacks only from committed renders and does so before descendant layout effects, while callback-only commits preserve mutate identity. An independent committed-document model crosses ordinary and StrictMode schedules with mutation before or after a suspended candidate, mutation after the candidate commits, and delayed or immediate mutation from a descendant layout effect. It compares ordered callback traces and public rows at the mutation cut, the trace after persistence, and mutate identity at the commit cut. Render-time publication, layout-effect-only publication, and split insertion/layout publication mutants fail at the intended comparisons. A commit between transaction admission and persistence, arbitrary React schedules, server delivery, and other frameworks remain outside this receiving owner. | | Optimistic state | [same-key composition](https://github.com/TanStack/db/blob/main/packages/db/tests/optimistic-composition-oracle.test.ts), [history model](https://github.com/TanStack/db/blob/main/packages/db/tests/optimistic-history-oracle.ts), [core property](https://github.com/TanStack/db/blob/main/packages/db/tests/optimistic-history-oracle.property.test.ts) (`optimistic-history.core`), [generated histories](https://github.com/TanStack/db/blob/main/packages/db/tests/optimistic-transaction-oracle.property.test.ts), [outcomes](https://github.com/TanStack/db/blob/main/packages/db/tests/optimistic-history-outcomes-oracle.test.ts), [publication](https://github.com/TanStack/db/blob/main/packages/db/tests/optimistic-history-publication-oracle.test.ts) | `optimistic-history.core` runs the core grammar through `oracleProperty`: the history resolves to a plan of concrete actions, the driver records each checkpoint, and the model owes allowed cuts, rows, outcomes, receipts, and tracked transactions, judged as named laws; the former settlement-boundary regressions are its fixed histories, and the seven observation mutants are calibrations, each rejected by its named law. Its grammar does not yet generate pending manual edits, external completion, rejected handlers, reentrant drains, partial updates, ordered operations, or schema defaults; those dimensions are still covered only by fixed histories in the owners that drive `runOptimisticHistory` (open: move them into the grammar). Optimistic state drops at settlement and held sync transactions publish with it ([settlement-drop review](oracle-reviews/2026-10-03-settlement-drop.md)); whole-row active overlays, metadata and prior-value events. A raw subscriber without initial state checks that each truncate batch inserts a key once ([2026-10-02 review](oracle-reviews/2026-10-02-truncate-raw-subscriber.md)). Never rebase a pending snapshot merely to simplify the model. Generated histories also write source batches inside mutation handlers, before they return; the Collection must own the request by then ([handler source batch review](oracle-reviews/2026-10-01-handler-source-batch.md)). The same-key transaction grammar also authors a delete followed by a reinsert, which must be visible optimistically and net to the truth-table request ([state mutation round 2](oracle-reviews/2026-10-02-state-mutation-round-2.md)). Source rows are written as `insert` for a key the source lacks, and batches may delete keys the source holds ([state-stack mutation gaps](oracle-reviews/2026-10-02-state-stack-mutant-gaps.md)). Batches may also delete a key the source never held. That delete leaves an active request in place ([absent-key source delete review](oracle-reviews/2026-10-02-absent-key-source-delete.md)). A separate partial campaign keeps the default partial row update mode, where source updates may omit a field and merge into the source row, not into an optimistic row ([round 3 review](oracle-reviews/2026-10-05-state-mutation-round-3.md)). An aborted open batch restores the driver's own source rows as well as its keys, so a later partial update still omits the field ([aborted-batch review](oracle-reviews/2026-10-08-partial-update-aborted-batch.md)). A failed synchronous manual `mutate` callback is now checked after same-key update, distinct insert, and same-key delete, with and without earlier intent, plus two two-Collection cases, one with a restoration listener failure. The throw cut compares public rows and pending payload; the later commit checks only surviving intent. A restoration listener error retains the callback error as the aggregate cause and does not stop other Collection restoration. These witnesses allow transient notifications during the callback and do not cover nested throwing callbacks or async work after the synchronous scope. After every step the driver also checks, by transaction identity, that the Collection tracks exactly its unsettled transactions, so a failed or rolled-back transaction leaves the map ([failed transaction retention review](oracle-reviews/failed-transaction-retention.md)). The [transaction ownership oracle](https://github.com/TanStack/db/blob/main/packages/db/tests/transaction-ownership-oracle.property.test.ts) owns release across two Collections: merged-away pairs, conflicting rollbacks with a throwing subscriber, asynchronous success and failure settlements with a throwing subscriber, rollbacks from a `truncate` listener during a sync commit, a reused transaction id, and a `mutate()` callback that throws, checked in the same call stack and after promises flush. It also checks the settlement error shape and that a settled transaction's set of tracking Collections is empty; its mutations still name their Collection, so neither owner claims the Collection is collectable. Focused [restoration ownership](https://github.com/TanStack/db/blob/main/packages/offline-transactions/tests/restoration-ownership.test.ts) witnesses check that repeated offline `mutate()` calls add to one transaction, that a completed restoration settles `when('settled')`, and that a restoration one Collection cannot track leaves no Collection tracking it. Its grammar also has direct writes (`insert`, `update` and `delete` outside a transaction), optionally with a throwing subscriber that may have been sent the rows first; it captures each direct write's own transaction and requires it to fail when the admission throws and to complete otherwise, counts handler calls (none for a rejected write), and keeps a mirror subscriber on each Collection that must match the rows after every step. A write whose admission throws rolls back only its own transaction and rethrows. The [change-event history oracle](https://github.com/TanStack/db/blob/main/packages/db/tests/change-event-history-oracle.test.ts) generates local-only direct writes that meet a throwing subscriber, registered after the mirror, and requires the call to rethrow with its transaction completed and the rows following the model. Focused witnesses cover a local-only subscriber that writes the key it was told about, and a subscriber that throws a value that is not an Error; whether a throwing subscriber may stop a later subscriber is not decided. Open (approved limits): a direct write made inside another write's change subscriber reports its subscriber failure to the outer write; on a local-only Collection a direct write whose subscriber throws completes on the fast path but rolls back on the transaction path, and the change-event oracle generates only the fast path; a direct write admitted from inside a sync-commit listener, where the rollback's recompute is deferred, is not generated; the generated ownership histories read every receipt themselves, so only a focused witness (rolling back an empty manual transaction) checks that an unread receipt reaches no `unhandledrejection`; two Collection instances with one id, a Collection cleaned up before its transaction settles, and offline restoration have focused witnesses only; no generated history combines a held completed row with a second Collection. | diff --git a/packages/db/src/collection/state.ts b/packages/db/src/collection/state.ts index 3ecec40b7f..edd2a12003 100644 --- a/packages/db/src/collection/state.ts +++ b/packages/db/src/collection/state.ts @@ -150,6 +150,9 @@ export class CollectionStateManager< // Core state - make public for testing public transactions: SortedMap> + // Transactions whose rows cleanup discarded. They keep their hold, but they + // never overlay this Collection again, even after a restart. + private discardedTransactions = new WeakSet>() public pendingSyncedTransactions: Array< PendingSyncedTransaction > = [] @@ -709,8 +712,13 @@ export class CollectionStateManager< continue } // Settlement can outlive cleanup. Keep pruning settled transactions, - // but do not republish a sibling from the discarded sync run. - if (this.lifecycle.hasStartedCleanup()) continue + // but do not republish a sibling from the discarded sync run, or any + // write that arrives while that cleanup is still running. + if ( + this.lifecycle.isCleaningUp() || + this.discardedTransactions.has(transaction) + ) + continue for (const mutation of transaction.mutations) { if (mutation.collection !== this.collection) continue this.pendingLocalChanges.add(mutation.key) @@ -1647,6 +1655,8 @@ export class CollectionStateManager< */ public cleanup(): void { this.syncRunGeneration++ + for (const transaction of this.transactions.values()) + this.discardedTransactions.add(transaction) for (const transaction of this.pendingSyncedTransactions) { transaction.applied.reject(new SyncTransactionAbortedError()) } diff --git a/packages/db/tests/collection-gc-transaction-oracle.property.test.ts b/packages/db/tests/collection-gc-transaction-oracle.property.test.ts index a024f71ae7..0bfb254261 100644 --- a/packages/db/tests/collection-gc-transaction-oracle.property.test.ts +++ b/packages/db/tests/collection-gc-transaction-oracle.property.test.ts @@ -1,18 +1,12 @@ import fc from 'fast-check' -import { expect, it, vi } from 'vitest' +import { vi } from 'vitest' import { createCollection } from '../src/collection/index.js' import { createDeferred } from '../src/deferred.js' import { createTransaction } from '../src/transactions.js' -import { - oracleFixedSeed, - oraclePropertyOptions, - oracleRoute, - oracleRouteOf, - readOracleRunConfig, -} from './oracle-config.js' import { declareOracle } from './oracle-declaration.js' -import { createOracleReach } from './oracle-reach.js' +import { differs, oracleProperty, pass, violation } from './oracle-property.js' import { resetCleanupQueue, withOracleCleanup } from './utils.js' +import type { Verdict } from './oracle-property.js' import type { Deferred } from '../src/deferred.js' /** @@ -25,8 +19,12 @@ import type { Deferred } from '../src/deferred.js' * the `gcTime` delay starts again when the last such transaction settles, * whether it completes or fails. A transaction that touches several * Collections holds each of them. An explicit `cleanup()` retires the - * Collection despite persisting transactions. This synchronous adapter fixture - * collapses cleanup start and adapter settlement into one observation. + * Collection despite persisting transactions, and discards the rows they show. + * Until the next subscribe, an explicitly cleaned-up Collection stays cleaned + * up, and its subscriber count keeps counting. A transaction that is still + * persisting after the cleanup and the restart keeps its hold, but its rows + * stay cleared. This synchronous adapter fixture collapses cleanup start and + * adapter settlement into one observation. * * Authority: `gcTime` is the time a Collection with no subscribers waits * before it is collected (`BaseCollectionConfig.gcTime`), and collecting it @@ -36,6 +34,16 @@ import type { Deferred } from '../src/deferred.js' * Collection (Electric's `awaitTxId`, for example). Collecting the Collection * in that window drops rows the user just wrote and fails the handler's wait. * Explicit cleanup is a caller's decision, so it keeps its current contract. + * The post-cleanup rules have these sources. The glossary's `cleanup` entry + * says a direct subscription survives cleanup, so the count is not reset. Its + * `cleanup` and `cleanup start` entries say restart then starts a new sync run, + * so in this grammar only a subscribe restarts a cleaned-up Collection. The + * review record `oracle-reviews/pr-2258-gc-retention-round3.md` says cleanup + * starts by discarding public rows and that explicit cleanup overrides + * retention. `oracle-reviews/pr-2258-gc-retention.md` records the repair of + * sibling-row resurrection during and after explicit cleanup (commit 3e4052e65, + * "keep discarded transaction rows cleared after cleanup"). So a restart does + * not show a row that cleanup discarded. * * The model keeps an elapsed clock and, for each of two Collections, the * subscriber count, the set of persisting transactions that touch it, and @@ -50,50 +58,109 @@ import type { Deferred } from '../src/deferred.js' * The history grammar, with `gcTime` 100: subscribe to either Collection, * unsubscribe one of its current subscribers, insert a row whose handler * stays pending, complete or fail the oldest pending handler, and advance the - * clock by 20, 60, or 120 ms. An insert writes to one Collection through its + * clock by 1, 20, 60, or 120 ms. An insert writes to one Collection through its * `onInsert` handler, or to both through `createTransaction` with a manual - * commit. A subscribe after retirement restarts that Collection. A history - * ends in one of two ways. It cleans up both Collections explicitly, or it + * commit. A `cleanup` step calls `cleanup()` on one Collection or on both at + * any point, so a settlement or an unsubscribe can follow it. A subscribe + * after retirement or cleanup restarts that Collection. A history ends in one + * of two ways. It cleans up both Collections explicitly, or it * drains: it unsubscribes everyone, settles every pending handler with one * outcome, and advances past the deadlines, so each drained history ends * with retirements that follow its last settlement. Inserting into a retired * Collection is not generated: it would restart the sync, which is the * subscribe step's job. Unsubscribing more subscribers than exist is not - * legal. + * legal. `resolve` drops those steps, so the plan the driver runs is legal. + * + * Constructed histories make each reach state happen in every campaign. A + * constructed history opens with the steps that enter its states, then keeps + * the generated steps, so the steps after each state stay random. Its + * builder never changes the end of a generated history, except that the + * explicit-cleanup state needs a `cleanup` end. The opening steps come first, + * so the state is entered whatever the generated steps are. The one state that + * is entered at the end, a cleanup while a transaction persists, also drops + * the generated settlements, so the opening insert is still pending at the + * cleanup. Every builder's output stays inside the grammar, so its failures + * shrink like generated ones. Half of a campaign's histories are constructed. * * The production driver uses two real Collections with a synchronous ready * sync, public `subscribeChanges`, `insert`, `createTransaction`, and * `cleanup()`, and controls each handler through a deferred. After each - * step, on a fake clock whose pending timers and microtasks have run, the - * comparison checks two public facts for each Collection: whether it is - * `cleaned-up`, and the exact persisting rows in this empty-source fixture. + * action, on a fake clock whose pending timers and microtasks have run, it + * records two public facts for each Collection: whether it is `cleaned-up`, + * and the exact persisting rows in this empty-source fixture. The model + * computes the same facts for each checkpoint from the plan alone, and the + * check compares them, so the driver decides nothing. * * Limits: paced mutations, offline transactions, live-query Collections, and * wall-clock corrections are not generated. A transaction that never settles - * holds its Collections for as long as it persists. + * holds its Collections for as long as it persists. Writes into a cleaned-up + * Collection, which restart it, are not generated, and this oracle claims no + * owner for that restart. A settlement on a cleaned-up Collection starts no + * `gcTime` delay, but no public fact shows that delay, so the model states no + * rule for it, and no observation checks it. + * + * Retirement latency. The law makes a Collection eligible at `gcTime`, and + * exact cleanup latency is not promised. So a checkpoint before the deadline + * owes no retirement, a checkpoint from the deadline up to + * `RETIREMENT_LATENCY_MS` (20 ms) after it allows either outcome, and a + * checkpoint at or after that bound owes retirement. The 1 ms step lets a + * history observe a checkpoint one millisecond before the deadline, so an early + * retirement at `gcTime` - 1 ms is rejected. A retirement at `gcTime` + 1 ms to + * `gcTime` + 19 ms is allowed, since latency is not promised. Limit: a timer + * one millisecond early (`gcTime` - 1 ms) is not observed at the 99 ms + * checkpoint in this harness, so it survives as indistinguishable from an + * exact-deadline retirement, which is allowed. A timer two milliseconds early + * (`gcTime` - 2 ms) is rejected. */ const GC_TIME_MS = 100 +const MAX_STEPS = 24 +// A retirement is owed once this long has passed since the deadline. It is a +// checker bound, not a product promise. Exact cleanup latency is not promised, +// so before this bound the outcome at the deadline is either. +const RETIREMENT_LATENCY_MS = 20 type Row = { id: number } type Side = `a` | `b` +const sides: Array = [`a`, `b`] + +// The history as the grammar generates it. type Step = | { kind: `subscribe`; side: Side } | { kind: `unsubscribe`; side: Side } | { kind: `insert`; into: Side | `both` } | { kind: `settle`; outcome: `complete` | `fail` } - | { kind: `advance`; elapsedMs: 20 | 60 | 120 } + | { kind: `advance`; elapsedMs: 1 | 20 | 60 | 120 } + | { kind: `cleanup`; side: Side | `both` } type History = { steps: Array end: `cleanup` | `drain-complete` | `drain-fail` } -type ReachState = - | `gc-due-while-persisting` - | `retired-after-completion` - | `retired-after-failure` - | `retired-after-shared-settlement` - | `settled-while-subscribed` - | `cleanup-while-persisting` - | `restarted-after-retirement` + +// The plan `resolve` produces: legal actions that name their handlers by id. +// It holds no expected observations. +type Action = + | { kind: `subscribe`; side: Side } + | { kind: `unsubscribe`; side: Side } + | { kind: `insert`; into: Side | `both`; id: number } + | { kind: `settle`; id: number; outcome: `complete` | `fail` } + | { kind: `advance`; elapsedMs: number } + | { kind: `cleanup`; side: Side } + +const reachStates = [ + `gc-due-while-persisting`, + `retired-after-completion`, + `retired-after-failure`, + `retired-after-shared-settlement`, + `settled-while-subscribed`, + `cleanup-while-persisting`, + `restarted-after-retirement`, + `settle-after-cleanup`, + `unsubscribe-after-cleanup`, + `restart-after-cleanup`, + `write-while-discarded`, + `one-millisecond-before-deadline`, +] as const +type ReachState = (typeof reachStates)[number] type CollectionModel = { subscribers: number @@ -102,6 +169,11 @@ type CollectionModel = { // Which hold's end set the deadline, for reach only. deadlineAfter: { outcome: `complete` | `fail`; shared: boolean } | undefined retired: boolean + // Set by an explicit cleanup and cleared by a subscribe, for reach only. + cleaned: boolean + // Persisting transactions whose rows cleanup discarded. They keep their hold + // and stay cleared after a restart. A settlement removes them. + discarded: Array // When the Collection last lost its last subscriber, for reach only. unsubscribedAt: number | undefined } @@ -112,11 +184,35 @@ type Model = { pendingHandlers: Array<{ id: number; sides: Array }> } -const sides: Array = [`a`, `b`] +// What the two Collections show after an action: cleaned up, and the rows +// they hold. Both the model and the driver produce this shape. +// At its deadline a Collection may or may not be retired yet: `either`. +type Visible = { cleanedUp: boolean | `either`; keys: Array } +type Snapshot = Record +type Checkpoint = { checkpoint: string; value: Snapshot } +type Expected = { checkpoints: Array; reached: Array } + +const byId = (a: number, b: number) => a - b const held = (collection: CollectionModel) => collection.subscribers > 0 || collection.persisting.length > 0 +const startModel = (): CollectionModel => ({ + subscribers: 0, + persisting: [], + deadline: GC_TIME_MS, + deadlineAfter: undefined, + retired: false, + cleaned: false, + discarded: [], + unsubscribedAt: 0, +}) +const freshModel = (): Model => ({ + now: 0, + collections: { a: startModel(), b: startModel() }, + pendingHandlers: [], +}) + // A hold just ended: the Collection becomes due `gcTime` from now. function release( model: Model, @@ -129,38 +225,243 @@ function release( collection.deadlineAfter = after } -// The cleanup queue's timer adds one tick, so production retires the -// Collection just after its deadline, not at it. Clock steps are at least -// 20 ms, so a step that passes the deadline also passes that tick. +// Retirement is owed once RETIREMENT_LATENCY_MS has passed since the deadline. function advanceModel(model: Model, elapsedMs: number): void { model.now += elapsedMs for (const collection of Object.values(model.collections)) { - if (collection.deadline !== undefined && collection.deadline < model.now) { + if ( + collection.deadline !== undefined && + collection.deadline + RETIREMENT_LATENCY_MS <= model.now + ) { collection.retired = true collection.deadline = undefined } } } -const runConfig = readOracleRunConfig() -let reach = createReach() -function createReach() { - return createOracleReach( - `collection-lifecycle.gc-persisting-transaction`, - [ - `gc-due-while-persisting`, - `retired-after-completion`, - `retired-after-failure`, - `retired-after-shared-settlement`, - `settled-while-subscribed`, - `cleanup-while-persisting`, - `restarted-after-retirement`, - ], - ) +// Applies one legal action to the model and returns the reach states it +// enters. The model's rules are the ones the oracle has always enforced. +function applyModel(model: Model, action: Action): Array { + const reached: Array = [] + if (action.kind === `subscribe`) { + const expected = model.collections[action.side] + if (expected.retired) reached.push(`restarted-after-retirement`) + if (expected.cleaned) reached.push(`restart-after-cleanup`) + expected.subscribers++ + expected.retired = false + expected.cleaned = false + expected.deadline = undefined + expected.unsubscribedAt = undefined + } else if (action.kind === `unsubscribe`) { + const expected = model.collections[action.side] + if (expected.cleaned) reached.push(`unsubscribe-after-cleanup`) + // Cleanup does not reset the count: a direct subscription survives it. + expected.subscribers-- + if (expected.subscribers === 0) expected.unsubscribedAt = model.now + release(model, action.side) + } else if (action.kind === `insert`) { + const into = action.into === `both` ? sides : [action.into] + for (const side of into) { + if (model.collections[side].discarded.length > 0) + reached.push(`write-while-discarded`) + } + model.pendingHandlers.push({ id: action.id, sides: into }) + for (const side of into) { + model.collections[side].persisting.push(action.id) + model.collections[side].deadline = undefined + } + } else if (action.kind === `settle`) { + const settled = model.pendingHandlers.shift()! + for (const side of settled.sides) { + const expected = model.collections[side] + if (expected.subscribers > 0) reached.push(`settled-while-subscribed`) + if (expected.cleaned) reached.push(`settle-after-cleanup`) + expected.persisting = expected.persisting.filter( + (id) => id !== settled.id, + ) + expected.discarded = expected.discarded.filter((id) => id !== settled.id) + release(model, side, { + outcome: action.outcome, + shared: settled.sides.length > 1, + }) + } + } else if (action.kind === `advance`) { + const before = sides.map((side) => model.collections[side].retired) + advanceModel(model, action.elapsedMs) + for (const [index, side] of sides.entries()) { + const expected = model.collections[side] + if ( + expected.persisting.length > 0 && + expected.unsubscribedAt !== undefined && + model.now - expected.unsubscribedAt >= GC_TIME_MS + ) + reached.push(`gc-due-while-persisting`) + if ( + expected.deadline !== undefined && + expected.deadline - model.now === 1 + ) + reached.push(`one-millisecond-before-deadline`) + const after = expected.deadlineAfter + if (before[index] || !expected.retired || !after) continue + reached.push( + after.outcome === `complete` + ? `retired-after-completion` + : `retired-after-failure`, + ) + if (after.shared) reached.push(`retired-after-shared-settlement`) + } + } else { + // An explicit cleanup retires the Collection whatever persists in it, and + // stays in effect until the next subscribe. + const expected = model.collections[action.side] + if (expected.persisting.length > 0) reached.push(`cleanup-while-persisting`) + expected.retired = true + expected.cleaned = true + expected.discarded = [...expected.persisting] + expected.deadline = undefined + } + return reached +} + +// Exactly at the deadline, the law makes the Collection eligible, and exact +// cleanup latency is not promised, so either outcome is owed. A later +// checkpoint owes retirement, and one before the deadline owes none. +function owedSnapshot(model: Model): Snapshot { + const view = (side: Side): Visible => { + const collection = model.collections[side] + const cleanedUp = collection.retired + ? true + : collection.deadline !== undefined && collection.deadline <= model.now + ? `either` + : false + return { + cleanedUp, + keys: collection.retired + ? [] + : collection.persisting + .filter((id) => !collection.discarded.includes(id)) + .sort(byId), + } + } + return { a: view(`a`), b: view(`b`) } +} + +// The plan: each step that the grammar allows, with its handler named by id, +// then the history's end. A drain unsubscribes everyone, settles every pending +// handler with one outcome, and advances past the deadlines. +function resolve(history: History): Array { + const model = freshModel() + const plan: Array = [] + let nextId = 1 + const take = (action: Action) => { + applyModel(model, action) + plan.push(action) + } + for (const step of history.steps) { + if (step.kind === `subscribe`) { + take({ kind: `subscribe`, side: step.side }) + } else if (step.kind === `unsubscribe`) { + if (model.collections[step.side].subscribers > 0) + take({ kind: `unsubscribe`, side: step.side }) + } else if (step.kind === `insert`) { + const into = step.into === `both` ? sides : [step.into] + if (into.every((side) => !model.collections[side].retired)) + take({ kind: `insert`, into: step.into, id: nextId++ }) + } else if (step.kind === `settle`) { + const first = model.pendingHandlers[0] + if (first) take({ kind: `settle`, id: first.id, outcome: step.outcome }) + } else if (step.kind === `cleanup`) { + for (const side of step.side === `both` ? sides : [step.side]) + take({ kind: `cleanup`, side }) + } else { + take({ kind: `advance`, elapsedMs: step.elapsedMs }) + } + } + if (history.end === `cleanup`) { + for (const side of sides) take({ kind: `cleanup`, side }) + return plan + } + for (const side of sides) + while (model.collections[side].subscribers > 0) + take({ kind: `unsubscribe`, side }) + const outcome = history.end === `drain-complete` ? `complete` : `fail` + while (model.pendingHandlers.length > 0) + take({ kind: `settle`, id: model.pendingHandlers[0]!.id, outcome }) + take({ kind: `advance`, elapsedMs: 120 }) + return plan +} + +// Each action is one checkpoint, after the action and its macrotask. +const checkpointOf = (index: number, action: Action) => + `step ${index} ${action.kind}` + +const expectedOf = (plan: ReadonlyArray): Expected => { + const state = freshModel() + const checkpoints: Array = [ + { checkpoint: `start`, value: owedSnapshot(state) }, + ] + const reached = new Set() + for (const [index, action] of plan.entries()) { + for (const entered of applyModel(state, action)) reached.add(entered) + checkpoints.push({ + checkpoint: checkpointOf(index, action), + value: owedSnapshot(state), + }) + } + return { checkpoints, reached: [...reached] } } -async function runHistory(history: History): Promise { - reach.beginHistory() +const LAW = `retirement` +const DIFFERENCE = `the Collection's cleaned-up status or visible rows differ from the owed retirement and visibility` + +// Where the owed state allows either retirement outcome, the observed state +// takes the owed value, so only the rows and the other Collection are compared. +const admitting = (owed: Snapshot, observed: Snapshot): Snapshot => { + const side = (name: Side): Visible => ({ + cleanedUp: + owed[name].cleanedUp === `either` ? `either` : observed[name].cleanedUp, + keys: observed[name].keys, + }) + return { a: side(`a`), b: side(`b`) } +} + +// Judges the recorded checkpoints in order, then whether the trace is complete. +const check = ( + _plan: ReadonlyArray, + observations: ReadonlyArray<{ checkpoint: string; value: unknown }>, + expected: Expected, +): Verdict => { + for (const [index, owed] of expected.checkpoints.entries()) { + const observed = observations[index] + if (observed === undefined) break + if (observed.checkpoint !== owed.checkpoint) + return violation( + owed.checkpoint, + `the driver recorded ${observed.checkpoint} where the plan owes ${owed.checkpoint}`, + LAW, + ) + const verdict = differs( + owed.checkpoint, + LAW, + admitting(owed.value, observed.value as Snapshot), + owed.value, + DIFFERENCE, + ) + if (verdict) return verdict + } + return observations.length === expected.checkpoints.length + ? pass + : violation( + `trace`, + `the driver recorded ${observations.length} of ${expected.checkpoints.length} checkpoints`, + LAW, + ) +} + +async function driver( + plan: ReadonlyArray, + observe: (checkpoint: string, value: unknown) => void, +): Promise { vi.useFakeTimers() vi.setSystemTime(0) resetCleanupQueue() @@ -185,157 +486,60 @@ async function runHistory(history: History): Promise { a: [], b: [], } - const startModel = (): CollectionModel => ({ - subscribers: 0, - persisting: [], - deadline: GC_TIME_MS, - deadlineAfter: undefined, - retired: false, - unsubscribedAt: 0, - }) - const model: Model = { - now: 0, - collections: { a: startModel(), b: startModel() }, - pendingHandlers: [], - } - let nextId = 1 // Run every timer due by now, and the microtasks they start. const settle = () => vi.advanceTimersByTimeAsync(0) - const check = (label: string) => { - for (const side of sides) { - const expected = model.collections[side] - const collection = collections[side] - expect( - collection.status === `cleaned-up`, - `${label}: ${side} cleaned up at ${model.now} ms`, - ).toBe(expected.retired) - expect( - [...collection.keys()].sort((a, b) => a - b), - `${label}: ${side} visible keys`, - ).toEqual( - expected.retired ? [] : [...expected.persisting].sort((a, b) => a - b), - ) - } - } + const visible = (side: Side): Visible => ({ + cleanedUp: collections[side].status === `cleaned-up`, + keys: [...collections[side].keys()].sort(byId), + }) + const record = (checkpoint: string) => + observe(checkpoint, { a: visible(`a`), b: visible(`b`) }) - const apply = async (step: Step, label: string) => { - if (step.kind === `subscribe`) { - const expected = model.collections[step.side] - if (expected.retired) reach.reach(`restarted-after-retirement`) - subscriptions[step.side].push( - collections[step.side].subscribeChanges(() => {}), + const run = async (action: Action) => { + if (action.kind === `subscribe`) { + subscriptions[action.side].push( + collections[action.side].subscribeChanges(() => {}), ) - expected.subscribers++ - expected.retired = false - expected.deadline = undefined - expected.unsubscribedAt = undefined - } else if (step.kind === `unsubscribe`) { - const subscription = subscriptions[step.side].pop() - if (!subscription) return - subscription.unsubscribe() - const expected = model.collections[step.side] - expected.subscribers-- - if (expected.subscribers === 0) expected.unsubscribedAt = model.now - release(model, step.side) - } else if (step.kind === `insert`) { - const into = step.into === `both` ? sides : [step.into] - if (into.some((side) => model.collections[side].retired)) return - const id = nextId++ + } else if (action.kind === `unsubscribe`) { + subscriptions[action.side].pop()!.unsubscribe() + } else if (action.kind === `insert`) { const handler = createDeferred() - handlers.set(id, handler) - if (step.into === `both`) { + handlers.set(action.id, handler) + if (action.into === `both`) { const transaction = createTransaction({ autoCommit: false, mutationFn: () => handler.promise, }) transaction.mutate(() => { - collections.a.insert({ id }) - collections.b.insert({ id }) + collections.a.insert({ id: action.id }) + collections.b.insert({ id: action.id }) }) transaction.commit().catch(() => {}) } else { - collections[step.into] - .insert({ id }) - .when('settled') + collections[action.into] + .insert({ id: action.id }) + .when(`settled`) .catch(() => {}) } - model.pendingHandlers.push({ id, sides: into }) - for (const side of into) { - model.collections[side].persisting.push(id) - model.collections[side].deadline = undefined - } - } else if (step.kind === `settle`) { - const settled = model.pendingHandlers.shift() - if (!settled) return - const handler = handlers.get(settled.id)! - if (step.outcome === `complete`) handler.resolve() - else handler.reject(new Error(`handler ${settled.id} failed`)) - for (const side of settled.sides) { - const expected = model.collections[side] - if (expected.subscribers > 0) reach.reach(`settled-while-subscribed`) - expected.persisting = expected.persisting.filter( - (id) => id !== settled.id, - ) - release(model, side, { - outcome: step.outcome, - shared: settled.sides.length > 1, - }) - } + } else if (action.kind === `settle`) { + const handler = handlers.get(action.id)! + if (action.outcome === `complete`) handler.resolve() + else handler.reject(new Error(`handler ${action.id} failed`)) + } else if (action.kind === `advance`) { + await vi.advanceTimersByTimeAsync(action.elapsedMs) } else { - const before = sides.map((side) => model.collections[side].retired) - advanceModel(model, step.elapsedMs) - await vi.advanceTimersByTimeAsync(step.elapsedMs) - for (const [index, side] of sides.entries()) { - const expected = model.collections[side] - if ( - expected.persisting.length > 0 && - expected.unsubscribedAt !== undefined && - model.now - expected.unsubscribedAt >= GC_TIME_MS - ) - reach.reach(`gc-due-while-persisting`) - const after = expected.deadlineAfter - if (before[index] || !expected.retired || !after) continue - reach.reach( - after.outcome === `complete` - ? `retired-after-completion` - : `retired-after-failure`, - ) - if (after.shared) reach.reach(`retired-after-shared-settlement`) - } + await collections[action.side].cleanup() } - await settle() - check(label) } await withOracleCleanup(async () => { await settle() - check(`start`) - for (const [index, step] of history.steps.entries()) - await apply(step, `step ${index} ${step.kind}`) - if (history.end === `cleanup`) { - if (model.pendingHandlers.length > 0) - reach.reach(`cleanup-while-persisting`) - for (const side of sides) { - await collections[side].cleanup() - expect(collections[side].status, `explicit cleanup of ${side}`).toBe( - `cleaned-up`, - ) - expect( - [...collections[side].keys()], - `explicit cleanup rows of ${side}`, - ).toEqual([]) - } - } else { - const outcome = history.end === `drain-complete` ? `complete` : `fail` - const drain: Array = [ - ...sides.flatMap((side) => - subscriptions[side].map((): Step => ({ kind: `unsubscribe`, side })), - ), - ...model.pendingHandlers.map((): Step => ({ kind: `settle`, outcome })), - { kind: `advance`, elapsedMs: 120 }, - ] - for (const step of drain) await apply(step, `drain ${step.kind}`) + record(`start`) + for (const [index, action] of plan.entries()) { + await run(action) + await settle() + record(checkpointOf(index, action)) } }, [ async () => { @@ -391,50 +595,201 @@ const stepArbitrary: fc.Arbitrary = fc.oneof( }), weight: 3, }, + { + arbitrary: fc.record({ + kind: fc.constant(`advance` as const), + elapsedMs: fc.constant(1 as const), + }), + weight: 1, + }, + { + arbitrary: fc.record({ + kind: fc.constant(`cleanup` as const), + side: fc.constantFrom(`a` as const, `b` as const, `both` as const), + }), + weight: 1, + }, ) -const property = fc.asyncProperty( - fc.record({ - steps: fc.array(stepArbitrary, { minLength: 1, maxLength: 14 }), - end: fc.constantFrom( - `cleanup` as const, - `drain-complete` as const, - `drain-fail` as const, - ), - }), - (history) => runHistory(history), -) +const historyArbitrary: fc.Arbitrary = fc.record({ + steps: fc.array(stepArbitrary, { minLength: 1, maxLength: MAX_STEPS }), + end: fc.constantFrom( + `cleanup` as const, + `drain-complete` as const, + `drain-fail` as const, + ), +}) + +// A constructed history opens with `prefix`, then keeps the generated steps. +const openWith = + (...prefix: Array) => + (generated: History): History => ({ + steps: [...prefix, ...generated.steps].slice(0, MAX_STEPS), + end: generated.end, + }) + +const insertStep = (into: Side | `both`): Step => ({ kind: `insert`, into }) +const settleStep = (outcome: `complete` | `fail`): Step => ({ + kind: `settle`, + outcome, +}) +const advanceStep = (elapsedMs: 1 | 20 | 60 | 120): Step => ({ + kind: `advance`, + elapsedMs, +}) +const cleanupStep = (side: Side): Step => ({ kind: `cleanup`, side }) // What this oracle owns: the garbage-collection hold that a persisting -// transaction places on each Collection it touches, in lifecycle.ts. The -// cleanup-queue oracle owns the timer dispatch that runs the deadline. +// transaction places on each Collection it touches, in lifecycle.ts, and the +// settlement that releases it. A transaction settles in `commit` (completion) +// or `rollback` (failure), and both reach `touchCollection`, which restarts the +// delay for each Collection the transaction touched. The oracle judges those +// three functions with their static call trees. The cleanup-queue oracle owns +// the timer dispatch that runs the deadline. declareOracle({ - owns: [`src/collection/lifecycle.ts`], + owns: [ + `src/collection/lifecycle.ts`, + `src/transactions.ts#Transaction.commit`, + `src/transactions.ts#Transaction.rollback`, + `src/transactions.ts#Transaction.touchCollection`, + ], grammar: [stepArbitrary], }) // Replay one history with TANSTACK_DB_ORACLE_SEED, TANSTACK_DB_ORACLE_PATH, // and TANSTACK_DB_ORACLE_PROPERTY=collection-lifecycle.gc-persisting-transaction. -it.each( - runConfig.campaignSeed === undefined ? [20261024, undefined] : [undefined], -)( - `retires a Collection only after gcTime with no subscriber and no persisting transaction (seed %s)`, - async (seed) => { - reach = createReach() - const parameters = { - ...oraclePropertyOptions( - 100, - `collection-lifecycle.gc-persisting-transaction`, - ), - ...(seed === undefined || runConfig.replayPath !== undefined - ? {} - : oracleFixedSeed(seed)), - } - oracleRoute(oracleRouteOf(parameters)) - await fc.assert(property, parameters) - reach.assertReached() - console.info( - `GC transaction reach: ${JSON.stringify(Object.fromEntries(reach.counts()))}`, - ) +// Each constructed history names the states it enters, with the steps that +// enter it, and every declared state has at least one. The constructed +// histories run beside the generated ones in each campaign, so a path recorded +// before they were added may select a different history. +oracleProperty({ + id: `collection-lifecycle.gc-persisting-transaction`, + law: { + statement: `Automatic garbage collection retires a Collection only after gcTime with no subscriber and no persisting transaction; a persisting transaction holds each Collection it touches, and the delay restarts when the last such transaction completes or fails; explicit cleanup() retires a Collection while a transaction persists.`, + authority: `BaseCollectionConfig.gcTime; the persisting-transaction hold in packages/db/src/collection/lifecycle.ts (optimistic rows and adapter awaitTxId waits); explicit cleanup keeps its current contract`, + limits: `Two Collections with a synchronous ready sync and empty source; keys as numbers, up to ${MAX_STEPS} steps; clock steps of 1, 20, 60, and 120 ms with gcTime 100; paced mutations, offline transactions, live-query Collections, writes into a cleaned-up Collection, and wall-clock corrections are not generated. The delay after a settlement on a cleaned-up Collection is not observable.`, + owner: `Collection garbage collection under persisting transactions`, }, -) + histories: { + arbitrary: historyArbitrary, + states: reachStates, + runs: 100, + fixedSeeds: [20261024], + constructed: [ + { + name: `gc due while a transaction persists`, + enters: [`gc-due-while-persisting`], + build: openWith(insertStep(`a`), advanceStep(120)), + }, + { + name: `retired after completion`, + enters: [`retired-after-completion`], + build: openWith( + insertStep(`a`), + settleStep(`complete`), + advanceStep(120), + ), + }, + { + name: `retired after failure`, + enters: [`retired-after-failure`], + build: openWith(insertStep(`a`), settleStep(`fail`), advanceStep(120)), + }, + { + name: `retired after a shared settlement`, + enters: [`retired-after-shared-settlement`, `retired-after-failure`], + build: openWith( + insertStep(`both`), + settleStep(`fail`), + advanceStep(120), + ), + }, + { + name: `settled while subscribed`, + enters: [`settled-while-subscribed`], + build: openWith( + { kind: `subscribe`, side: `a` }, + insertStep(`a`), + settleStep(`complete`), + advanceStep(120), + ), + }, + { + name: `subscribe again after retirement`, + enters: [`restarted-after-retirement`], + build: openWith( + insertStep(`a`), + settleStep(`complete`), + advanceStep(120), + { kind: `subscribe`, side: `a` }, + ), + }, + { + name: `settle after cleanup`, + enters: [`settle-after-cleanup`], + build: openWith( + insertStep(`a`), + cleanupStep(`a`), + settleStep(`complete`), + advanceStep(120), + ), + }, + { + name: `unsubscribe after cleanup`, + enters: [`unsubscribe-after-cleanup`], + build: openWith( + { kind: `subscribe`, side: `a` }, + cleanupStep(`a`), + { kind: `unsubscribe`, side: `a` }, + advanceStep(120), + ), + }, + { + name: `subscribe again after cleanup`, + enters: [`restart-after-cleanup`], + build: openWith(cleanupStep(`a`), { kind: `subscribe`, side: `a` }), + }, + { + // Sixty, then twenty, then nineteen 1 ms steps: a checkpoint lands one + // millisecond before the deadline set at time 0. + name: `one millisecond before the deadline`, + enters: [`one-millisecond-before-deadline`], + build: openWith( + advanceStep(60), + advanceStep(20), + ...Array.from({ length: 19 }, () => advanceStep(1)), + ), + }, + { + // A write after the restart must not bring back the discarded row. + name: `write after restart while a discarded row persists`, + enters: [`write-while-discarded`], + build: openWith( + insertStep(`b`), + cleanupStep(`a`), + cleanupStep(`b`), + { kind: `subscribe`, side: `b` }, + insertStep(`b`), + ), + }, + { + // The opening insert must still be pending at the cleanup, so the + // generated settlements are dropped. Its end becomes cleanup. + name: `explicit cleanup while a transaction persists`, + enters: [`cleanup-while-persisting`], + build: (generated): History => ({ + steps: [ + insertStep(`b`), + ...generated.steps.filter((step) => step.kind !== `settle`), + ].slice(0, MAX_STEPS), + end: `cleanup`, + }), + }, + ], + }, + resolve, + model: expectedOf, + reached: (_plan, _trace, expected) => expected.reached, + driver, + check, +}) diff --git a/packages/db/tests/oracle-replay-manifest.ts b/packages/db/tests/oracle-replay-manifest.ts index 79d9c72486..7dea99ff8d 100644 --- a/packages/db/tests/oracle-replay-manifest.ts +++ b/packages/db/tests/oracle-replay-manifest.ts @@ -1027,10 +1027,6 @@ const replayTestNames = new Map([ `collection-lifecycle.gc-mutation-shapes`, `retains every touched Collection across mutation shapes.*seed undefined`, ], - [ - `collection-lifecycle.gc-persisting-transaction`, - `retires a Collection only after gcTime.*seed undefined`, - ], [ `collection-lifecycle.gc-retention-boundaries`, `preserves retention across transaction phases.*seed undefined`,