TanStack
DB

Content temporarily unavailable

Initial-readiness design grammar: TLA+ control

This directory holds the bounded TLA+ control for the initial-query readiness grammar of PR #2115. It checks the internal consequences of the grammar's transition rules. It does not show that production refines the model. Model D in packages/db/tests/query/includes-temporal-oracle.test.ts and the receiving witnesses listed in ../progressive-source-readiness.md own that claim.

Frozen preservation list

The user confirmed these properties before extraction. S marks a source-stated property, and I marks an analyst-inferred property.

IDPropertyBasis
P1A consumer is initially ready exactly when every reachable current demand is settled and every eager source is ready.S, ARCHITECTURE.md law 10
P2A load settles only when its rows are visible or the source owns their absence.S, law 7
P3An obsolete or aborted acquisition neither satisfies nor blocks readiness. A truncate replacement takes over the hold.S, law 6 and replay rules
P4Live-query readiness and the end of Effect skipInitial suppression happen at the same point. Readers of live-query status (isReady, preload, Suspense, queryOnce, hydration) inherit it.I
P5Initial readiness is monotone across later truncate, rekey, and reset.I
P6A real load failure errors a live query and disposes an Effect. It never produces readiness.S, AGENTS.md
P7Without a subscriber or preload, nothing is acquired.S, law 15
P8An ordered window stays unpublished until its request chain settles.S
P9An eager source gates readiness. A source with no syncMode is eager.S
P10After onError retries a stream error, later loads settle when the stream recovers.I, from J1
P11A source that resumes from complete local rows settles its loads at once.S, Electric oracle
P12Freshness after readiness is outside this law.S, a limit

Grammar to model trace

Grammar itemTLA+ element
Source mode and Collection readiness (P9)RootMode, srcReady, MarkReadyEager
Acquisition: status, visible rows, current, Effect holdacq records
Shared rule sourcePermitsInitialReadinessRootPermits
The law, independent of both consumer rules (P1)Covered
Live-query ruleLiveRule, latched by UpdateConsumers
Effect rule: tracked holds that release on settle or abortEffectRule, held
G-lazy: lazy demand starts in the graph run that shows root rowsAddLazy in Start, DeliverRoot, SettleWith, MarkReadyEager
G-window: the continuation starts when the first segment settles (P8)NeedsContinuation, chain
Applied settlement (P2)Settle requires rows, SettleOnSnapshot installs rows
G-snap: a progressive load outside buffering follows the established snapshotSettleOnSnapshot, FailOnSnapshot, snap
Truncate with replacement takeover (P3)Truncate, TruncateSrc, MustRefetch
Rekey of lazy demand (P3)Rekey
Real failures (P6)FailLazy, StreamError
Retry and renew (P10)Retry
Complete resume (P11)Resume in Init
Deferred acquisition (P7)started, Start
CleanupCleanup, NoReadyAfterCleanup

Properties: ReadyMeansCovered and ReadyWhenCovered (P1), RowsAtReady (P2), NoSpuriousFailure (P3, P10), ConsumersAgree (P4), Monotone (P5), FailureNeverReady (P6), DeferredAcquisition (P7). P8, P9, and P11 enter through Covered and the configurations.

Boundary matrix and exclusions

Each axis lists the values in the model. Excluded values give a reason and their owner.

  • Consumers: live query, skipInitial Effect. Status readers are not separate rules. They read live-query status, and the exposure witnesses check them in each framework. toArrayWhenReady and stateWhenReady resolve through preload(). The audit found that they resolved on first data, and the user chose to make them follow readiness.
  • Source modes: an eager root; an on-demand root that buffers progressively; an on-demand root that resumes from complete rows; an on-demand lazy source. Excluded: an eager lazy source, whose readiness is the eager rule (Model D eager shapes).
  • Shapes: direct, ordered window with one continuation, lazy child. Excluded: two on-demand roots (#2117), and include children as distinct from lazy joins. Both use the same AddLazy rule in this abstraction.
  • Lifecycle events: start, delivery, settle, truncate, rekey, must-refetch, up-to-date, stream error, retry, real lazy failure, and cleanup. At most two disturbances and one stream error. Excluded: unload and restart (cleanup and restart oracle), and changes after readiness (P12).
  • Checkpoints: the readiness transition (history variables) and every state (invariants).

Runs

TLC 2.19 (rev 5a47802) through the Field Lab container, with -deadlock:

ConfigurationResult
safe-progressive-lazyno error, 11,426 distinct states
safe-progressive-orderedno error, 1,713 distinct states
safe-eager-lazyno error, 135 distinct states
safe-resume-lazyno error, 1,679 distinct states

Each weakened configuration turns on one wrong design and checks only its target property:

ConfigurationWrong designCounterexampleViolated
weak-old-rulegate an on-demand root on Collection readiness (#2113)Start, DeliverRoot, SettleReadyWhenCovered
weak-ignore-eagernever gate on Collection readinessStartReadyMeansCovered
weak-effect-no-takeoverEffect releases a truncated hold without its replacementStart, MustRefetchConsumersAgree
weak-effect-abort-latchEffect treats an aborted hold as a failureStart, MustRefetchNoSpuriousFailure
weak-abort-is-failurelive query fails truncated lazy demand (on main)UpToDate, Start, SettleOnSnapshot, TruncateNoSpuriousFailure
weak-settle-without-rowsa progressive load settles during a reset without rowsMustRefetch, Start, SettleEarlyRowsAtReady
weak-retry-no-renewa retry keeps the rejected snapshot (J1)Start, StreamError, Retry, FailOnSnapshotNoSpuriousFailure
weak-recomputereadiness is recomputed, not latchedStart, UpToDate, SettleOnSnapshot, CleanupMonotone
weak-window-earlythe continuation starts after a readiness passStart, UpToDate, SettleOnSnapshotReadyMeansCovered

Encoding receipt

The first safe run found a counterexample to ReadyMeansCovered in safe-progressive-lazy and safe-resume-lazy: Start, SettleOnSnapshot. The model made root rows visible at settlement but did not issue their lazy demand. That broke G-lazy, so it was an encoding failure, not a grammar failure. SettleWith now calls AddLazy. The failed run also ablates G-lazy: without it, the law fails.

Limits

  • The model has one root and one lazy source, at most seven acquisitions, and at most two disturbances.
  • Monotone latches readiness through cleanup. In production, cleanup moves the status to cleaned-up. The property claims only that cleanup adds no first-ready transition.
  • A load that is waiting when a stream error arrives fails, even if onError later retries. The model and production agree on this. Whether such a failure is real under P6 is a product decision.
  • The model has no fairness and no liveness property.

Run

shell
~/.claude/skills/field-lab/scripts/tlc . -deadlock -config safe-progressive-lazy.cfg InitialReadiness
Edit on GitHub
Overview