Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 16 additions & 0 deletions .changeset/code-contracts-live-query.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
---
'@tanstack/db': patch
---

Add code contracts for live query D2 multiplicity invariant.

Introduces a contract-based approach to ensure correctness in the live query system, inspired by Cheng Huang's article on AI-assisted development. Contracts verify runtime invariants during development/testing and can be disabled in production.

Key additions:

- `contracts.ts` with `precondition()`, `postcondition()`, and `invariant()` utilities
- D2 multiplicity contracts in `CollectionSubscriber.sendChangesToPipeline()` ensuring no duplicate keys are sent to the incremental view maintenance pipeline
- 16 contract verification tests covering multiplicity, tracking, and consistency
- 9 property-based tests using fast-check to explore edge cases with random operation sequences

Contracts are automatically disabled when `NODE_ENV=production` for zero runtime overhead in production builds.
1 change: 1 addition & 0 deletions packages/db/package.json
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,7 @@
"@tanstack/config": "^0.22.2",
"@vitest/coverage-istanbul": "^3.2.4",
"arktype": "^2.1.29",
"fast-check": "^4.5.3",
"mitt": "^3.0.1",
"superjson": "^2.2.6",
"temporal-polyfill": "^0.3.0"
Expand Down
200 changes: 200 additions & 0 deletions packages/db/src/contracts.ts
Original file line number Diff line number Diff line change
@@ -0,0 +1,200 @@
/**
* Contract utilities for runtime verification of preconditions, postconditions, and invariants.
*
* Inspired by Design by Contract (DbC) principles and Cheng Huang's approach to AI-assisted
* code verification. Contracts serve as executable specifications that:
* - Document expected behavior
* - Catch violations early during development/testing
* - Can be disabled in production for performance
*
* @example
* ```typescript
* function divide(a: number, b: number): number {
* precondition(b !== 0, 'divisor must be non-zero')
* const result = a / b
* postcondition(Number.isFinite(result), 'result must be finite')
* return result
* }
* ```
*/

// Contract checking is enabled by default, can be disabled via environment variable
// In production builds, bundlers can tree-shake contract checks when this is false
const CONTRACTS_ENABLED =
typeof process !== `undefined`
? process.env.NODE_ENV !== `production` &&
process.env.DISABLE_CONTRACTS !== `1`
: true

/**
* Base class for all contract violation errors.
* Extends TanStackDBError for consistent error handling.
*/
export class ContractViolationError extends Error {
constructor(
public readonly violationType:
| `precondition`
| `postcondition`
| `invariant`,
message: string,
) {
super(
`${violationType.charAt(0).toUpperCase() + violationType.slice(1)} violation: ${message}`,
)
this.name = `ContractViolationError`
}
}

/**
* Thrown when a precondition check fails.
* Preconditions define what must be true before a function executes.
*/
export class PreconditionViolationError extends ContractViolationError {
constructor(message: string) {
super(`precondition`, message)
this.name = `PreconditionViolationError`
}
}

/**
* Thrown when a postcondition check fails.
* Postconditions define what must be true after a function executes.
*/
export class PostconditionViolationError extends ContractViolationError {
constructor(message: string) {
super(`postcondition`, message)
this.name = `PostconditionViolationError`
}
}

/**
* Thrown when an invariant check fails.
* Invariants define what must always be true for an object/system.
*/
export class InvariantViolationError extends ContractViolationError {
constructor(message: string) {
super(`invariant`, message)
this.name = `InvariantViolationError`
}
}

/**
* Asserts a precondition that must be true before function execution.
* Use at the beginning of functions to validate inputs and state.
*
* @param condition - Boolean or function returning boolean to check
* @param message - Error message if condition is false
* @throws {PreconditionViolationError} if condition is false
*
* @example
* ```typescript
* function withdraw(amount: number) {
* precondition(amount > 0, 'amount must be positive')
* precondition(this.balance >= amount, 'insufficient balance')
* // ...
* }
* ```
*/
export function precondition(
condition: boolean | (() => boolean),
message: string,
): asserts condition {
if (!CONTRACTS_ENABLED) return

const result = typeof condition === `function` ? condition() : condition
if (!result) {
throw new PreconditionViolationError(message)
}
}

/**
* Asserts a postcondition that must be true after function execution.
* Use at the end of functions to validate outputs and final state.
*
* @param condition - Boolean or function returning boolean to check
* @param message - Error message if condition is false
* @throws {PostconditionViolationError} if condition is false
*
* @example
* ```typescript
* function sort(arr: number[]): number[] {
* const result = [...arr].sort((a, b) => a - b)
* postcondition(result.length === arr.length, 'length preserved')
* postcondition(isSorted(result), 'result is sorted')
* return result
* }
* ```
*/
export function postcondition(
condition: boolean | (() => boolean),
message: string,
): asserts condition {
if (!CONTRACTS_ENABLED) return

const result = typeof condition === `function` ? condition() : condition
if (!result) {
throw new PostconditionViolationError(message)
}
}

/**
* Asserts an invariant that must always be true.
* Use to verify system-wide or object-wide consistency.
*
* @param condition - Boolean or function returning boolean to check
* @param message - Error message if condition is false
* @throws {InvariantViolationError} if condition is false
*
* @example
* ```typescript
* class BinaryTree {
* insert(value: number) {
* // ... insertion logic ...
* invariant(this.isBalanced(), 'tree must remain balanced')
* }
* }
* ```
*/
export function invariant(
condition: boolean | (() => boolean),
message: string,
): asserts condition {
if (!CONTRACTS_ENABLED) return

const result = typeof condition === `function` ? condition() : condition
if (!result) {
throw new InvariantViolationError(message)
}
}

/**
* Helper to check if contracts are currently enabled.
* Useful for conditional contract logic or testing.
*/
export function areContractsEnabled(): boolean {
return CONTRACTS_ENABLED
}

/**
* Captures a value before an operation for use in postcondition checks.
* Returns undefined when contracts are disabled to avoid computation overhead.
*
* @param getValue - Function that computes the value to capture
* @returns The captured value, or undefined if contracts are disabled
*
* @example
* ```typescript
* function increment(counter: Counter) {
* const oldValue = captureForPostcondition(() => counter.value)
* counter.value++
* postcondition(
* oldValue === undefined || counter.value === oldValue + 1,
* 'value incremented by exactly 1'
* )
* }
* ```
*/
export function captureForPostcondition<T>(getValue: () => T): T | undefined {
if (!CONTRACTS_ENABLED) return undefined
return getValue()
}
51 changes: 51 additions & 0 deletions packages/db/src/query/live/collection-subscriber.ts
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,11 @@ import {
normalizeExpressionPaths,
normalizeOrderByPaths,
} from '../compiler/expressions.js'
import {
captureForPostcondition,
invariant,
postcondition,
} from '../../contracts.js'
import type { MultiSetArray, RootStreamBuilder } from '@tanstack/db-ivm'
import type { Collection } from '../../collection/index.js'
import type { ChangeMessage } from '../../types.js'
Expand Down Expand Up @@ -130,22 +135,40 @@ export class CollectionSubscriber<
return subscription
}

/**
* Sends filtered changes to the D2 pipeline, ensuring multiplicity invariants.
*
* @contract
* @invariant D2 multiplicity === 1 for all visible items (no duplicates)
* @invariant sentToD2Keys accurately tracks all keys currently in D2
* @postcondition All inserts in filteredChanges have unique keys
* @postcondition For each insert: key is added to sentToD2Keys
* @postcondition For each delete: key is removed from sentToD2Keys
*/
private sendChangesToPipeline(
changes: Iterable<ChangeMessage<any, string | number>>,
callback?: () => boolean,
) {
// Capture state before filtering for postcondition verification
const sentKeysBefore = captureForPostcondition(
() => new Set(this.sentToD2Keys),
)

// Filter changes to prevent duplicate inserts to D2 pipeline.
// This ensures D2 multiplicity stays at 1 for visible items, so deletes
// properly reduce multiplicity to 0 (triggering DELETE output).
const changesArray = Array.isArray(changes) ? changes : [...changes]
const filteredChanges: Array<ChangeMessage<any, string | number>> = []
const insertKeysInBatch = new Set<string | number>()

for (const change of changesArray) {
if (change.type === `insert`) {
if (this.sentToD2Keys.has(change.key)) {
// Skip duplicate insert - already sent to D2
continue
}
this.sentToD2Keys.add(change.key)
insertKeysInBatch.add(change.key)
} else if (change.type === `delete`) {
// Remove from tracking so future re-inserts are allowed
this.sentToD2Keys.delete(change.key)
Expand All @@ -154,6 +177,34 @@ export class CollectionSubscriber<
filteredChanges.push(change)
}

// Contract: Verify no duplicate insert keys in filtered output
// This invariant ensures D2 multiplicity stays at 1
const insertKeys = filteredChanges
.filter((c) => c.type === `insert`)
.map((c) => c.key)
const uniqueInsertKeys = new Set(insertKeys)
invariant(
insertKeys.length === uniqueInsertKeys.size,
`D2 multiplicity invariant violated: duplicate insert keys detected in batch: [${insertKeys.join(`, `)}]`,
)

// Contract: Verify sentToD2Keys state is consistent
if (sentKeysBefore !== undefined) {
for (const change of filteredChanges) {
if (change.type === `insert`) {
postcondition(
this.sentToD2Keys.has(change.key),
`sentToD2Keys must contain key ${change.key} after insert`,
)
} else if (change.type === `delete`) {
postcondition(
!this.sentToD2Keys.has(change.key),
`sentToD2Keys must not contain key ${change.key} after delete`,
)
}
}
}

// currentSyncState and input are always defined when this method is called
// (only called from active subscriptions during a sync session)
const input =
Expand Down
Loading
Loading