diff --git a/docs/contributing/oracle-coverage.md b/docs/contributing/oracle-coverage.md index 9944a382f2..77c377a017 100644 --- a/docs/contributing/oracle-coverage.md +++ b/docs/contributing/oracle-coverage.md @@ -1472,7 +1472,7 @@ generic visitor behavior outside the named collectors. | Surface | Primary executable owners | Independent judgment and important limit | | -------------------------------------------- | --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | | 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 pins `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. Other hash-based operators retain hashing's declared domain. 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 pinned 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 pins 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 pinned 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 lane 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 pins 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 lane. 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. | +| 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 lane 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 and the callback-visible rows of an Effect without `skipInitial` 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 pins 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 lane. 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-oracle.test.ts), [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 lanes, 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. | diff --git a/docs/contributing/oracle-reviews/progressive-source-readiness.md b/docs/contributing/oracle-reviews/progressive-source-readiness.md index 0544eeb2ea..22174f9371 100644 --- a/docs/contributing/oracle-reviews/progressive-source-readiness.md +++ b/docs/contributing/oracle-reviews/progressive-source-readiness.md @@ -314,3 +314,46 @@ outcome of every async hold. Model D. - Before the full sync, an Electric progressive query's rows do not receive live changes. The source contract owns that behavior, not this law. + +## Effect without `skipInitial` round + +Base: `db476b8ed`. This entry covers the change that adds the +`effect-initial-rows` consumer to Model D +([TanStack/db#2117](https://github.com/TanStack/db/issues/2117)). + +Law (ARCHITECTURE.md, Effects and initial readiness): every Effect passes its +gate at initial-query readiness, but `skipInitial` "only decides whether the +initial rows are delivered", and "other ordinary initial/refinement requests +keep their existing callback timing". So an Effect without `skipInitial` shows +the query's current result at every checkpoint, before readiness too. The +architecture sentence on the gate could also be read as holding initial rows +until readiness. The callback-timing sentence and the current production +behavior agree on the first reading, and the lane enacts it. + +Grammar and observation: the same 156 histories as the `skipInitial` Effect +lane (direct, lazy join, and both eager roots, with truncate and rekey +disturbances). The observation is the callback-visible result rebuilt from +`enter`, `exit`, and `update` events, with a count of events inconsistent with +that result. Between a truncate and its settlement the model does not judge +the rows; the metamorphic twin does. + +Reach (`createOracleReach`, bounded exhaustive cells): rows visible before +initial-query readiness, 117 cells; a row written after readiness is visible, +46 cells; truncate replay before settlement, 80 cells. + +Mutants, run against the whole Model D lane. Only the new cells reject either +one; every other cell of every consumer passes: + +| Mutant | Rejecting cells | Outcome | +| --------------------------------------------------- | ------------------------------------------------- | ------------------------------- | +| Without `skipInitial`, hold callbacks until the gate | 52 `direct`, 92 `join`, 4 `eager-root`, 4 `eager-default` | Assertion failure, checkpoint 1–5 | +| Ignore `skipInitial: false` (drop initial rows) | the same 152 cells | Assertion failure | + +Each eager shape has two survivors: histories in which `source-ready` comes +first. No row is visible before readiness there, so both mutants are +equivalent within those histories. The earlier record's survivor, "tracking +initial loads without `skipInitial`", stays equivalent; the first mutant is +the non-equivalent neighbor that makes the argument executable. + +Open: Effects without `skipInitial` over an ordered window, an include, or a +single result, and `useLiveQueryEffect`, have no lane. diff --git a/packages/db/tests/query/includes-temporal-oracle.test.ts b/packages/db/tests/query/includes-temporal-oracle.test.ts index e76104463d..5eaafd70f2 100644 --- a/packages/db/tests/query/includes-temporal-oracle.test.ts +++ b/packages/db/tests/query/includes-temporal-oracle.test.ts @@ -17,6 +17,7 @@ import { DeduplicatedLoadSubset } from '../../src/query/subset-dedupe.js' import { createEffect } from '../../src/query/effect.js' import { LoadSubsetOperationAbortedError } from '../../src/errors.js' import { runTrace } from '../trace-runner.js' +import { createOracleReach } from '../oracle-reach.js' import { oraclePropertyOptions, oracleReplayTest, @@ -2568,6 +2569,13 @@ async function expectProgressiveTraceMatches( // already visible; the live query itself preloads from the start. A read // that starts after readiness resolves with the rows it sees then. An Effect with `skipInitial` // suppresses every delta until the same point and delivers every later delta. +// An Effect without `skipInitial` passes the same gate, but the gate holds no +// callback: "other ordinary initial/refinement requests keep their existing +// callback timing", and `skipInitial` "only decides whether the initial rows +// are delivered" (ARCHITECTURE.md, Effects and initial readiness). Its +// callback-visible result is the query's current result at every checkpoint, +// before readiness too. Its cells reject an Effect that holds or drops its +// initial deltas until readiness. // // Each on-demand cell also runs a metamorphic twin: the same consumer over an // on-demand source that is ready from its start, receiving every other step. @@ -2600,9 +2608,9 @@ async function expectProgressiveTraceMatches( // The live-query shapes put the lagging source at a direct root, a // single-result root, an ordered root window, a correlated include child, // the lazy side of a join, an eager root that sets `syncMode: 'eager'`, and -// an eager root that leaves `syncMode` at its default. The Effect lane uses -// the direct, lazy-join, and both eager-root shapes; Effects over an ordered -// window or an include are not covered here. The eager roots are the nearby +// an eager root that leaves `syncMode` at its default. Both Effect lanes, with +// and without `skipInitial`, use the direct, lazy-join, and both eager-root +// shapes; Effects over an ordered window or an include are not covered here. The eager roots are the nearby // witnesses: a design that ignores source readiness entirely completes them // too early, and one that exempts every source not configured as eager // misses the default. A design that waits for every source's Collection @@ -2617,7 +2625,8 @@ async function expectProgressiveTraceMatches( // without the truncate replacement reports rows too early. A live query that // treats an aborted lazy-demand load as a failure enters error. Between a // truncate and its settlement the replay barrier owns publication, so the -// model does not judge live-query rows there; the metamorphic twin does. +// model does not judge live-query rows or an Effect's callback-visible rows +// there; the metamorphic twin does. // // The driver uses real Collections, a live-query preload or `createEffect`, // and controlled source writes. Each step is followed by a timer turn. Each @@ -2639,6 +2648,7 @@ type LaggingSourceShape = type LaggingSourceConsumer = | `live-query` | `effect` + | `effect-initial-rows` | `query-once` | `to-array-when-ready` | `state-when-ready` @@ -2765,6 +2775,17 @@ type EffectObservation = { acquisitions: number } +// An Effect without `skipInitial` has a callback-visible result: the rows it +// entered and has not exited. The recorder counts an `enter` for a visible +// key, and an `exit` or `update` for an absent key, as inconsistent, so a +// duplicate or lost delta reaches the comparison. `visible` is `null` between +// a truncate and its settlement, where the replay barrier owns publication. +type InitialRowsEffectObservation = { + visible: { rows: number; postIds: Array } | null + inconsistentEvents: number + acquisitions: number +} + // An unordered shape publishes held rows as a partial result. The `find-one` // shape is the reported trace (TanStack/db#2113): a single result filtered by // the initial post's id, so the later change never matches it. The ordered @@ -2819,6 +2840,31 @@ function expectedEffectObservation( } } +// Without `skipInitial`, initial-query readiness holds the Effect's gate but +// no callback: ordinary initial requests keep their callback timing. So the +// callback-visible result is the shape's current result at every checkpoint, +// before readiness too. A left-join parent always shows one row, matched or +// unmatched. +function expectedInitialRowsEffectObservation( + shape: LaggingSourceShape, + facts: LaggingSourceFacts, +): InitialRowsEffectObservation { + const postIds = facts.posts + .filter((post) => postMatchesShape(shape, facts, post)) + .map(({ id }) => id) + .sort((a, b) => a - b) + return { + visible: facts.replayPending + ? null + : { + rows: shape === `join` ? Math.max(postIds.length, 1) : postIds.length, + postIds, + }, + inconsistentEvents: 0, + acquisitions: LAGGING_SOURCE_SHAPES[shape] === `on-demand` ? 1 : 0, + } +} + // A written post reaches the consumer when it matches the current parent: the // selected user for the join, or `userId = 2` for the root shapes. After // initial readiness it enters the Effect; a left-join parent that showed no @@ -3006,8 +3052,9 @@ function rowPostIds( return [row.id as number] } -// One consumer of a lagging source: a live query with its preload, or a -// `skipInitial` Effect with the deltas it reported. +// One consumer of a lagging source: a live query with its preload, a +// `skipInitial` Effect with the deltas it reported, or an Effect without +// `skipInitial` with its callback-visible rows. type LaggingSourceConsumerState = { source: LaggingPosts resolvedIds: Array | undefined @@ -3016,6 +3063,8 @@ type LaggingSourceConsumerState = { effect: Effect | undefined enteredPostIds: Array otherEvents: number + visibleRows: Map> + inconsistentEvents: number // Starts a live query's `toArrayWhenReady()` or `stateWhenReady()` read. startRead: (() => void) | undefined } @@ -3049,6 +3098,8 @@ function startLaggingSourceConsumer( effect: undefined, enteredPostIds: [], otherEvents: 0, + visibleRows: new Map(), + inconsistentEvents: 0, startRead: undefined, } const query = laggingSourceQuery(shape, source.collection, users) @@ -3076,14 +3127,23 @@ function startLaggingSourceConsumer( } } } else { + const skipInitial = consumer === `effect` state.effect = createEffect({ query, - skipInitial: true, + skipInitial, onBatch: (events) => { for (const event of events) { - if (event.type === `enter`) - state.enteredPostIds.push(...rowPostIds(shape, event.value)) - else state.otherEvents += 1 + if (skipInitial) { + if (event.type === `enter`) + state.enteredPostIds.push(...rowPostIds(shape, event.value)) + else state.otherEvents += 1 + continue + } + const visible = state.visibleRows.has(event.key) + if (event.type === `enter` ? visible : !visible) + state.inconsistentEvents += 1 + if (event.type === `exit`) state.visibleRows.delete(event.key) + else state.visibleRows.set(event.key, event.value) } }, }) @@ -3258,12 +3318,25 @@ function observeLaggingSourceConsumer( shape: LaggingSourceShape, facts: LaggingSourceFacts, state: LaggingSourceConsumerState, -): LiveQueryObservation | EffectObservation | ReadObservation { +): LaggingSourceObservation { if (isReadConsumer(consumer)) return { resolvedIds: state.resolvedIds, acquisitions: observedAcquisitions(shape, facts, state.source), } + if (consumer === `effect-initial-rows`) { + const rows = [...state.visibleRows.values()] + return { + visible: { + rows: rows.length, + postIds: rows + .flatMap((row) => rowPostIds(shape, row)) + .sort((a, b) => a - b), + }, + inconsistentEvents: state.inconsistentEvents, + acquisitions: observedAcquisitions(shape, facts, state.source), + } + } return consumer === `live-query` ? { ready: state.live!.isReady(), @@ -3281,7 +3354,10 @@ function observeLaggingSourceConsumer( } type LaggingSourceObservation = - LiveQueryObservation | EffectObservation | ReadObservation + | LiveQueryObservation + | EffectObservation + | InitialRowsEffectObservation + | ReadObservation type LaggingSourceCheck = { observation: LaggingSourceObservation @@ -3289,9 +3365,38 @@ type LaggingSourceCheck = { twinDisagreement: LaggingSourceObservation | undefined } +// The states the `effect-initial-rows` cells exist to reach. Each is read from +// the production observation together with the model's facts at a checkpoint. +const INITIAL_ROWS_EFFECT_REACH_STATES = [ + `rows visible before initial-query readiness`, + `row written after initial-query readiness is visible`, + `truncate replay before settlement`, +] as const +type InitialRowsEffectReach = ReturnType< + typeof createOracleReach<(typeof INITIAL_ROWS_EFFECT_REACH_STATES)[number]> +> + +function recordInitialRowsEffectReach( + reach: InitialRowsEffectReach, + shape: LaggingSourceShape, + facts: LaggingSourceFacts, + { visible }: InitialRowsEffectObservation, +): void { + if (facts.replayPending) reach.reach(`truncate replay before settlement`) + if (visible === null) return + if ( + visible.postIds.length > 0 && + !initiallyReady(LAGGING_SOURCE_SHAPES[shape], facts) + ) + reach.reach(`rows visible before initial-query readiness`) + if (facts.writtenAfterReadiness.some((id) => visible.postIds.includes(id))) + reach.reach(`row written after initial-query readiness is visible`) +} + function laggingSourceProjection( consumer: LaggingSourceConsumer, shape: LaggingSourceShape, + reach: InitialRowsEffectReach | undefined, ): TraceProjection { return { observe: ({ facts, main, twin }) => { @@ -3303,11 +3408,16 @@ function laggingSourceProjection( ) const twinObservation = twin && observeLaggingSourceConsumer(consumer, shape, facts, twin) + if (reach && `visible` in observation) + recordInitialRowsEffectReach(reach, shape, facts, observation) return { - observation: - facts.replayPending && `postIds` in observation + observation: !facts.replayPending + ? observation + : `postIds` in observation ? { ...observation, postIds: null } - : observation, + : `visible` in observation + ? { ...observation, visible: null } + : observation, twinDisagreement: twinObservation && JSON.stringify(twinObservation) !== JSON.stringify(observation) @@ -3321,7 +3431,9 @@ function laggingSourceProjection( ? expectedLiveQueryObservation(shape, facts) : isReadConsumer(consumer) ? expectedReadObservation(consumer, mode, facts) - : expectedEffectObservation(mode, facts), + : consumer === `effect-initial-rows` + ? expectedInitialRowsEffectObservation(shape, facts) + : expectedEffectObservation(mode, facts), twinDisagreement: undefined, }), assertEqual: (observed, expected) => { @@ -3335,11 +3447,12 @@ async function expectLaggingSourceTraceMatches( consumer: LaggingSourceConsumer, shape: LaggingSourceShape, steps: ReadonlyArray, + reach?: InitialRowsEffectReach, ): Promise { await runTrace({ steps, driver: createLaggingSourceDriver(consumer, shape), - projection: laggingSourceProjection(consumer, shape), + projection: laggingSourceProjection(consumer, shape, reach), }) } @@ -3534,6 +3647,7 @@ describe(`includes temporal oracle`, () => { `eager-default`, ], effect: [`direct`, `join`, `eager-root`, `eager-default`], + 'effect-initial-rows': [`direct`, `join`, `eager-root`, `eager-default`], 'query-once': [`direct`, `eager-root`], 'to-array-when-ready': [`direct`, `find-one`, `join`, `eager-root`], 'state-when-ready': [`direct`, `find-one`, `eager-root`], @@ -3548,9 +3662,28 @@ describe(`includes temporal oracle`, () => { })), ), ) - it.each(cells)(`$consumer $shape: $history`, ({ consumer, shape, steps }) => - expectLaggingSourceTraceMatches(consumer, shape, steps), + const initialRowsReach = createOracleReach( + `includes-temporal.effect-initial-rows`, + INITIAL_ROWS_EFFECT_REACH_STATES, + ) + it.each(cells)( + `$consumer $shape: $history`, + ({ consumer, shape, steps }) => { + if (consumer !== `effect-initial-rows`) + return expectLaggingSourceTraceMatches(consumer, shape, steps) + initialRowsReach.beginHistory() + return expectLaggingSourceTraceMatches( + consumer, + shape, + steps, + initialRowsReach, + ) + }, ) + // The cells are a bounded exhaustive enumeration, so each declared state + // must be reached by at least one of them. + it(`effect-initial-rows cells reach every declared state`, () => + initialRowsReach.assertReached()) }) // Grammar: one parent receives 2..4 distinct-key children while its acquisition