Skip to content

test(db-ivm): add DBSP incrementalization law properties #1741

Description

@KyleAMathews

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

  • A shared incrementalization-law helper can test both unary and binary D2 pipelines.
  • Generated cases include negative weights, duplicate contributors, cancelling changes, and simultaneous two-input batches.
  • Joins, reductions, ordering, and top-K satisfy full-recompute equivalence.
  • Atomic and valid split batch delivery converge.
  • Failures report a replayable FastCheck seed and shrink path.
  • Minimized failures are committed as deterministic regression cases.
  • The law suite has a focused package command suitable for high-run CI campaigns.

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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions