Live simulations
These are not animations. Each visualization below runs the engine's actual algorithm — ported faithfully from the Go source into TypeScript and executed in your browser. Move the controls and watch the real math run: the IBLT peels the real symmetric difference, the CRDT converges on real causal dots, the tri-temporal resolver computes the real supremum.
Fidelity
Every algorithm here is a byte-faithful port of the engine source: pkg/sync/iblt.go (IBLT subtract + peel), pkg/sync/crdt.go (dot minting + Join + Lamport advance), and internal/database/query.go (AsOf point-in-window + Range interval-intersection + max(systemTime) supremum). The only deviation is the hash primitive — the engine uses runtime maphash; the browser uses a deterministic mixer so the runs are reproducible. The algebra is identical.
Set reconciliation by IBLT subtraction
The engine does not exchange rows between peers — it exchanges digests. Two Invertible Bloom Lookup Tables are subtracted bucket-by-bucket, and the symmetric difference is recovered by a peeling cascade. Bandwidth scales with |A−B|, not |A|+|B|.
Move the sliders to change how many keys each replica holds and how much they overlap. The bucket grid is the real A.subtract(B) diff IBLT; +1/−1 cells are pure and peel first, un-colliding their neighbors until the table empties — or until collisions exceed capacity, which the engine surfaces honestly as the StratifiedAntiEntropyFallback counter.
|A−B|, not |A|+|B|. pkg/sync/iblt.go. +1/−1 buckets are pure (one key, hash-verified) and peel first, un-colliding neighbors in a cascade until the table empties — or until collisions exceed capacity, which the engine surfaces honestly as the StratifiedAntiEntropyFallback counter. The math. Each bucket holds three XOR accumulators — Count (signed), KeySum, HashSum. Insert adds the key to k=3 buckets; subtract diffs all three. A bucket is pure when |Count| = 1 and hash(KeySum) = HashSum — a cryptographic guarantee of exactly one uncollided key. Peeling that key from its k neighbors reduces their counts and frequently un-collides them, cascading until the table is empty. This is why the engine claims 0.00% false positives for state reconciliation: purity is hash-verified, not probabilistic.
Causal CRDT convergence: the join-semilattice meet
Every mutation is a causal dot (NodeID, Counter) — a node is the sole minter of its own Lamport counter, so dots are globally unique. Join is a pure set-union on dots: idempotent, commutative, associative. Replicas that receive the same dots reach byte-identical state regardless of merge order.
Press the sync buttons to exchange deltas. Watch the Lamport clock jump to max(local, remote) on receive (AdvanceLamportTo), and watch both replicas converge to identical dot sets — then press re-sync to prove idempotence (nothing changes).
(NodeID, Counter). Join is a pure set-union on dots — idempotent, commutative, associative — so replicas that receive the same dots reach byte-identical state regardless of order. AdvanceLamportTo jumps the local clock to max(local, remote). pkg/sync/crdt.go. Join keeps the existing entry on dot-collision (idempotent) and never drops a dot — conflict resolution is deferred to the read path (the tri-temporal supremum), exactly as the engine's frozen merge-union mandates. The convergence guarantee. Because each dot is globally unique and Join never drops a dot (it keeps the existing entry on collision), the engine state is a pure function of the dot set — not the order deltas arrived, not which peer sent first. This is the join-semilattice meet: Join(A, Join(B, C)) = Join(Join(A, B), C) = A ∪ B ∪ C. Conflict resolution is deferred to the read path (the tri-temporal supremum below) — Join itself is a lossless merge-union, exactly as the frozen core mandates.
Tri-temporal time travel: the supremum read
State carries three time axes: valid time (when the fact is true), system time (when it was asserted), and assertion time (the causal order, carried but not consulted by the query path). A point query asks: given a valid-time point and an as-of horizon, which row wins?
Drag valid time (the vertical query line on the lower axis) and the as-of horizon (the vertical line marking how far into system-time you can see). The resolver returns the row with the latest systemTime whose valid-window contains the query point and is visible at the horizon — max(SystemTime), strictly. A row at the incumbent's system time does not displace it.
systemTime whose valid-window contains the query point and is visible at the horizon — max(SystemTime), strictly. internal/database/query.go: systemTime ≤ asOf AND validStart ≤ validTime < validEnd (half-open), winner = max(systemTime) strictly. Watch the supremum flip as the horizon passes a correction — that is the engine's load-bearing bitemporal read, not a lookup. The load-bearing predicate. AsOf is point-in-window: systemTime ≤ asOf AND validStart ≤ validTime < validEnd (half-open). Range is interval-intersection: systemTime ≤ asOf AND validStart < rangeHi AND validEnd > rangeLo. The sweep bar at the bottom shows the supremum flipping as the as-of horizon passes a correction — querying before the correction sees the old value, querying after sees the new one. That is bitemporal time travel, not a lookup, and it is the engine's answer to "what did we believe was true, when."
Why three axes, not two
A two-temporal (valid × system) database can answer "what is true now" and "what did we believe at time T." The third axis — assertion time, the causal dot — lets the engine answer "in what order did we come to believe these things, and are they consistent with causality" across a partitioned mesh. The query path consults only valid + system (the supremum); the causal order governs convergence and replay. This separation is the moat.
How it fits together
(NodeID, Counter) and lands in the live HAMT.localHas set is the delta's send-key set.max(systemTime) among visible rows whose valid window contains the query.