Problem
@tanstack/db-ivm has focused example tests for its operators, but it does not have a reusable property-test harness for the central incrementalization law: applying an operator's emitted delta to its old output must produce the same result as evaluating the query from scratch over the updated input.
PR #1740 makes the D2 graph the source of truth for includes materialization. That makes this invariant more important, but the invariant belongs to the generic IVM package rather than to the includes implementation PR.
Law
For query Q, input state x, and weighted update batch δ:
apply(Q(x), QΔ(x, δ)) = Q(apply(x, δ))
Equivalently, the incremental operator must emit exactly the consolidated difference between the old and new fully evaluated outputs:
QΔ(x, δ) = Q(x + δ) - Q(x)
Here a delta is a Z-set/multiset of positive and negative weights, not CRUD intent.
Proposed test harness
- Add reusable FastCheck helpers under
packages/db-ivm/tests for:
- small initial weighted input states;
- legal insert, delete, replacement, duplicate, and cancelling batches;
- one-input and two-input operators;
- consolidation and exact output-delta comparison;
- fresh full evaluation before and after each batch.
- Exercise the most stateful operators first:
- inner and outer joins, including simultaneous deltas on both inputs;
- reduce and grouped reductions;
- consolidate;
- order/grouped order and top-K;
- representative composed pipelines.
- Add a batch-partition property: one atomic batch and equivalent valid split deliveries must converge to the same consolidated output.
- Use random seeds for broad histories, fixed seeds or exhaustive enumeration for named structural cells, and preserve shrunk failures as deterministic examples.
- Keep this below the Collection, query compiler, includes, demand, and facade layers so a failure points directly at IVM behavior.
Acceptance criteria
Limits
These laws detect incorrect incremental state transitions. They do not prove that a query has the intended SQL semantics if the incremental pipeline and full evaluator share the same semantic mistake; independent formulation/metamorphic tests remain useful above this layer.
Follow-up to #1740 and RFC #1658.
Problem
@tanstack/db-ivmhas focused example tests for its operators, but it does not have a reusable property-test harness for the central incrementalization law: applying an operator's emitted delta to its old output must produce the same result as evaluating the query from scratch over the updated input.PR #1740 makes the D2 graph the source of truth for includes materialization. That makes this invariant more important, but the invariant belongs to the generic IVM package rather than to the includes implementation PR.
Law
For query
Q, input statex, and weighted update batchδ:Equivalently, the incremental operator must emit exactly the consolidated difference between the old and new fully evaluated outputs:
Here a delta is a Z-set/multiset of positive and negative weights, not CRUD intent.
Proposed test harness
packages/db-ivm/testsfor:Acceptance criteria
Limits
These laws detect incorrect incremental state transitions. They do not prove that a query has the intended SQL semantics if the incremental pipeline and full evaluator share the same semantic mistake; independent formulation/metamorphic tests remain useful above this layer.
Follow-up to #1740 and RFC #1658.