lazily-spec

Language-agnostic wire protocol specification for the lazily reactive signals family.

This site is the rendered companion to the lazily-spec repository. It defines the canonical message schemas shared across every lazily implementation:

• lazily-rs (Rust)
• lazily-py (Python)
• lazily-zig (Zig)
• @lazily/signaling (TypeScript / Cloudflare Worker)

Cell Model

Upstream of every transport, the Cell Model fixes how a cell’s value converges. A cell is either single-writer (local/direct, no merge) or multi-write, and a multi-write cell carries a pluggable merge: <mechanism> attribute. CRDT is the first multi-write merge mechanism (merge: crdt), not the only one — lww, ot, lease, and custom are reserved alongside it. All transports below carry cells classified by this model.

Protocol Layers

Every layer in this matrix is required of every binding. The Distributed CRDT row and the required keyed cell collections layer are unconditional. The C-ABI FFI row is required by default with a narrow platform carve-out (a binding whose runtime cannot host a native in-process C ABI — e.g. browser/Worker JS — declares ffi = none and interops over the wire instead). The thread-safe and async reactive contexts are required where the platform supports them (a platform that structurally lacks threading or suspendable async declares thread_safe = none / async = none); the shared-memory payload path is required where the platform supports it, with an I/O-channel fallback (Inline payloads over IPC/WebSocket/WebRTC) when it does not. See the Binding Conformance Matrix for the full MUST/MAY breakdown and the carve-out terms.

Wire Format

All messages use JSON with serde-compatible tagging ("type" discriminant). Future binary codecs (bincode, postcard, protobuf) encode the same schemas — the JSON representation is normative.

Schema Format

Schemas are provided as JSON Schema (Draft 2020-12). Each implementation must validate against these schemas. See JSON Schemas.

Scope & non-goals

This repo extracts the cross-language, wire-protocol, and behavioral sections from lazily-rs/SPEC.md into a standalone reference. Every lazily-rs feature area is accounted for here exactly once: either normatively specified (with a link below) or explicitly marked Rust-specific. Rust-specific internals remain in the Rust crate and are intentionally out of scope.

Covered (normative, cross-language)

Out of scope (Rust-specific implementation)

These lazily-rs features are implementation choices, not cross-language contracts. Other bindings pick their own; they MUST meet the normative contracts above but need not mirror Rust’s approach.

Versioning

Protocol versioning follows the IPC capability negotiation: each session exchanges { protocol_id, protocol_major_version, codec } before any graph state flows. A major version bump is a breaking change; minor additions are additive.

Reactive Graph

The reactive graph is the dependency-tracking core of every lazily binding: a set of nodes whose values are derived from each other, where a change to a source invalidates only its transitive dependents and recomputation is pull-based and glitch-free. This chapter fixes the cross-language behavior — the lazily-formal kernel and the lazily-rs / lazily-py / lazily-zig / lazily-kt implementations are the executable references.

The reactive graph is compute, not protocol: only resolved values cross IPC/FFI as ordinary cell payloads. Every binding that ships a reactive graph MUST honor this contract.

The reactive family

A cell is a value-bearing reactive node — a node with a readable value. There are exactly two kinds of cell and one sink:

Cell is the value-bearing-node concept, never a handle. The word Cell names “a reactive node with a readable value”; the two kinds of cell are the SourceCell and the ComputedCell (the arena nodes Node::Source(SourceNode) and Node::Computed(ComputedNode)). A caller never holds a Cell — the two handles are the concrete types Source<T, M> and Computed<T>. There is no Cell<T, K> genus struct and no phantom kind parameter: Source’s policy M is a real parameter of the Source<T, M> handle, present only where writes exist. Reactive is the umbrella adjective — the reactive graph is cells plus effects — never a type and never a synonym for one kind.

The partition is one axis with both sides covered and no leftover: a cell’s value comes either from outside it (a SourceCell) or from upstream of it (a ComputedCell). Effect has no value to read, so it cannot be folded in — the sink position is a real boundary, not a naming accident.

A plain cell — Cell ≡ Source<KeepLatest> — is the keep-latest instance of the source kind; this is a default type parameter, not a spec assertion. A binding MAY implement Source<T> as that instance or keep it as a distinct fast path with identical semantics.

The eager construct is an eager Computed, not a distinct kind. The eager construction is computed(compute).eager(): a guarded Computed plus a puller Effect that reads it on creation and after every invalidation, so its value is materialized by the time the invalidating set/batch returns (readers never see an intermediate unset state — relaycell-backpressure-analysis.md §4.0). .eager() is declarative and idempotent and returns the same Computed handle, mutated — so the per-write puller of the old Signal cannot be constructed (see Eager computed cells under Semantics, and §9.2.2’s theorem that a writer is always a sink). .lazy() is the reverse transition; is_eager() is the predicate, so the bare verbs are never confused with a query.

The normative eager semantics are four observable clauses — materialize once at creation, fresh at mutator return, once per flush rather than once per write, and disposal that removes only the puller. They are stated under Eager computed cells below and fixtured in conformance/reactive-graph/signal_*.json. The computed-plus-puller construction is the recommended way to satisfy them, not itself a requirement.

Values are lazy by default; call .eager() on a Computed when eager push semantics are required. Handles are the two concrete types — Source<T, M>, Computed<T> — plus EffectHandle: lightweight, copyable ids over a shared node table (arena slots; see Handles and identity), usable only with the owning context.

Read is on every cell; write is on the source kind. Both handles expose get (auto-subscribing) — and only get; there is no subscribe, because observation is a declared dependency edge, never a registered callback (see Reactives have no observers). Writing is not a supertype/subtype relationship but a kind restriction: set (replace) and merge (fold under the source’s policy) live on the inherent impl for Source<T, M> alone, so computed.set(…) is a compile error — no method found, no trait in sight. A Computed reads and never writes; a Source does both. The payoff (relaycell-backpressure-analysis.md §4.0): a composite reader that needs to accept either kind takes a small per-binding read-only view (an enum, or Go’s Cell[T] interface below) and the backend chooses the impl — pull-computed, push-fed source, or polling-computed — behind one type, so ownership of the mutation (not the type) decides the invalidation source. Where a binding has no way to restrict methods by type parameter (Go), a read-only interface Cell[T] carrying Get is reintroduced, with SourceCell/ComputedCell as structs — the same compile error under a different mechanism (§4 of the design).

API surface

Two constructors and one transition, symmetric with the kernel. source / computed / .eager() replace the eight old constructors (cell, merge_cell, computed, memo, slot, signal, get_signal, dispose_signal) — and because every Computed is now guarded, the old computed-vs-memo distinction is gone: memo is removed and computed is the guarded derivation.

Semantics

• Pull-based, glitch-free refresh. A Computed that reads other cells always observes values consistent with the current inputs. On get, it first refreshes its own dependencies (recursively, lazy pull), then recomputes only if any dependency actually changed — it never observes a half-updated graph.
• Unified shared-owner reads (#lzrsgetarc). A context may expose a binding-specific shared-owner form of get (Rust’s local spelling is Context::get_rc). When exposed as a generic alternate read, it is a read mode, not another cell kind: it MUST accept both Source and Computed, MUST return the same current value as get, MUST refresh a dirty Computed in the same way, and MUST register the same dependency edge when invoked through a running computation. It MUST NOT add a Clone/deep-copy requirement merely to read the value. Allocation identity, reference-count operations, and inline value fallbacks are binding-level mechanics and are not wire-visible. The formal pins are Reactive.readShared_eq_readCell, Reactive.trackedSharedRead_eq_trackedRead, and Reactive.trackedSharedRead_registers_edge in lazily-formal.
• Every cell is guarded — one rule, two sides. A cell suppresses an equal value. On the source side this is the == guard on set: setting an equal value is a no-op, no downstream cascade fires. On the computed side it is the equality guard on recompute: an equal recompute suppresses downstream invalidation — the Computed’s value version does not bump, so subscribers see no change (matching TC39 Signal.Computed). Equality is structural/value equality, not reference identity, so two distinct-but-equal values suppress invalidation. T: PartialEq is the uniform bound on every cell, source and computed alike — the guard is not a mode a caller opts into.
• There is no unguarded cell, and no equals:false escape. The guard is never wrong: if it suppresses an update you wanted, the value did not encode the change. To always propagate, make the value genuinely PartialEq-distinct (encode the distinction you care about into the value), or use a merge policy to express accumulate/always-apply semantics. This is not a library toggle, and there is no unguarded constructor — memo (the old guarded form) has been removed because computed is now guarded and the two are the same thing.
• Dynamic dependencies. A tracking stack auto-discovers edges on each recompute: every get read inside a running Computed/effect registers a dependency. Stale dependencies from a previous run are removed before re-registering; a Computed that reads a different set of inputs on rerun has its edge set updated to match. There is no manual subscribe/unsubscribe.

Implementation note. The dedup that keeps edge registration idempotent is an implementation concern, not an observable one — the contract fixes the edge set, not how membership is tested. A binding MAY dedup by linear scan while a node’s degree is small; above a wide-fanout threshold it SHOULD promote to a hash-indexed edge set, so registration stays amortized O(1) in node degree and a wide-fanout graph does not degrade to O(n²) per propagation. The threshold matters in both directions: below it the linear scan is measurably the faster of the two, so an unconditional hash set is a regression on the common low-degree case (#lzspecedgeindex).

The threshold is not portable — measure it per binding. Naively it is where a scan of contiguous ids crosses the cost of one hash lookup, so it moves with both, and the same number can be right or wrong in the same language depending on unrelated choices. In lazily-rs that crossover measured near degree 170 with the standard library’s SipHash and near degree 40 once ids were hashed with a multiply-shift finalizer — a 4x shift from changing the hash function alone. lazily-dart measured 60 under AOT and 96 under JIT, a 1.6x spread from compilation mode with no code change at all. Copying another binding’s constant is how a promotion threshold ends up making mid-degree nodes slower than the scan it replaced. Across bindings the measured thresholds so far are 32, 64, 128 and 160 — there is no family constant.

Measure the hybrid, not the pure crossover. The crossover between a pure scan and a pure index is the wrong number, because a list arriving at degree T pays the full scan plus the one-time index build, with no indexed insert at exactly T to amortize against. Every candidate threshold therefore parks a regression on its own width, and the pure crossover cannot predict where. Sweep the real implementation against the unfixed tree across candidate thresholds and take the knee — lazily-dart’s pure crossover said 60–96, but the hybrid sweep put the worst-case regression at 1.63x for T=64 and 1.31x for T=128, so 128 shipped.

Two ways to get this measurement wrong, both observed:

• Comparing always-indexed against always-scanning inflates the crossover. It charges the index’s overhead on every one-element dependency list to the wide list. lazily-cpp first estimated 96 this way against a true 32 — a 3x error. Sweep the threshold constant alone, with everything else fixed.
• A width ladder’s narrow rungs cannot answer the low-degree question. A few hundred registrations is noise; lazily-dart measured 1.4x run-to-run variance at widths 2–4 and nearly reported a phantom regression at width 96 from ladder data. Low-degree behavior needs a separate high-repetition harness, not the tail of the ladder.

Two further hazards, both observed:

• Demotion needs hysteresis, or it thrashes. A dependent list oscillates by one on every recompute, because edges are removed and re-registered, so a single shared promote/demote boundary makes a list sitting at the threshold rebuild its index on every recompute. Demote well below the promote threshold, or do not demote at all.

  The cost is severe where the hazard exists and varies far more than the mechanism suggests: ~4x in lazily-rs, 7.67x in lazily-js, and 21.5x in lazily-kt — each at exactly threshold+1 and within noise at every neighbouring width, which is why a ladder must cluster rungs there or it will not see this at all.

  It is not universal, and the reason is structural: the hazard needs a list that oscillates by one. lazily-zig has no demotion path, so nothing can thrash. lazily-dart clears its dependent list wholesale during cascade rather than removing one edge at a time, and no thrash was observable at threshold±1 (0.99–1.05x) — it keeps hysteresis as cheap insurance on the detach path, not because measurement forced it. A binding SHOULD check which shape its own recompute has before assuming either result.

• A recycled id must not inherit an index. Where the index is held outside the node — a side table keyed by owner — its entries have to be dropped whenever the list is cleared or the owner is torn down. A binding that recycles ids will otherwise alias a stale index onto an unrelated node.

• Disposal is explicit. Handles are copyable ids, not owners, so dropping every handle to a node reclaims nothing: without an explicit disposal call the node and its edges live as long as the context. A binding whose nodes can outlive their usefulness — anything with subscribe/unsubscribe churn — SHOULD expose disposal for computed and source cells, not only for effects, or a workload whose live size is constant still grows without bound in both memory and propagation cost. Disposal detaches edges in both directions; reading a disposed node afterwards is an error, the same contract as disposing an effect (#lzspecedgeindex).

  Detection of a stale handle is bounded, deliberately. A binding that recycles ids and checks only the node’s kind catches a handle naming a disposed node of a different kind, but cannot catch one whose id has been reused by a new node of the same kind — the classic ABA case. Closing that requires generational ids or reference-counted handles, and this spec does not require either: both cost either handle size or the copyability that fan-out depends on. Conforming bindings therefore reject the cross-kind case and MAY admit the same-kind one. Callers must not rely on read-after- dispose failing.

  Garbage collection does not substitute for this. The reverse edge set is a strong reference to each dependent, so a long-lived source retains every node that ever read it — the same unbounded growth a manual binding has, arrived at by a different route. A tracing binding that wants reclamation to follow reachability MUST make its back-edges weak; until it does, its disposal story is exactly the explicit one above.

• Teardown scopes (scope). A scope records what was created through it and disposes that set when it ends. It bounds teardown, not visibility: a scope’s nodes read parent- and sibling-owned nodes freely, and scoping never restricts what an edge may point at.

  Ending a scope MUST be observationally equal to disposing each of its members individually — a scope introduces no disposal semantics of its own, it only names a set and a moment. Proved as disposeScope_eq_disposeAll in the standalone lazily-formal LazilyFormal.Reactive module. A binding is therefore free to implement the scope as a bulk sweep rather than a loop, and SHOULD, since reading each node’s kind from the arena at teardown is cheaper than a per-node dispatch.

  The resulting graph state depends only on the set of members, not on their order or multiplicity (disposeAll_order_independent). Effect cleanups are a different matter: they are side effects, so the order they run in is observable, and a binding MUST tear a scope down in reverse creation order — dependents before what they read — so a scope never transiently dangles inside itself and every binding runs cleanups in the same sequence. Order is therefore free for the edge bookkeeping and fixed for the cleanups.

  A scope carries the same hazard as dispose: ending it tears down its nodes even if something outside the scope still reads them. A binding MUST NOT present scope teardown as safe against that; only reference-counted handles close it, and they cost copyable handles.

• Scope and reachability are different questions. Disposal and teardown scopes answer “this work is over — free it now”, deterministically, at a point the program names. Weak back-edges and reference-counted handles answer “is anyone still using this?”, and answer it whenever the collector or the last release gets around to it. Neither subsumes the other, and a binding SHOULD offer both rather than picking one:

  binding class	scope	reachability
  non-GC, no destructors (zig)	scopes, ended at an explicit deinit/defer	none available; explicit disposal is the whole story
  non-GC, destructors (rs, cpp)	scopes, ended by the scope’s own destructor	reference-counted handles, opt-in — they cost copyable handles, which fan-out needs
  tracing GC (js, kt, py, go, dart)	scopes, ended by an explicit call	weak back-edges, which need no user-facing API

  Reference-counted handles are opt-in in every class because a source read by two dependents cannot be moved twice, so making the handle an owner forces a clone at every fan-out capture site. Per-node destructor ownership is not a third option: a node an arena-stored closure can capture must outlive the capture, so a handle that borrows the context can only ever be a leaf — the constraint that makes the scope, not the node, the right unit of teardown.

• Cycle detection. A Computed that depends on itself (directly or transitively) is detected during refresh and throws — the graph is acyclic by construction.

• batch coalesces. Multiple set calls inside batch(run) queue their invalidation roots; at the outermost batch exit the roots propagate and effects flush once. Mutation inside a batch is synchronous; only the invalidation propagation is deferred to the boundary.

• Effects are scheduled, not inline. An effect rerun is scheduled when a tracked dependency invalidates and runs in the subsequent flush (which may be the same tick, at batch exit). A rerun does not start until the previous cleanup completes. Disposal removes pending reruns, runs the current cleanup, and unsubscribes all dependency edges.

• Eager computed cells (.eager()). Eagerness is not a kind — it is a Computed with a puller Effect attached, produced by computed(compute).eager(): the effect reads it on creation and after every invalidation, forcing it to re-materialize. Because the puller runs inside the invalidating set/batch’s effect flush, the value is fresh by the time the mutator returns. .eager() is declarative and idempotent — a second call is a no-op, so a Computed never acquires two pullers and the per-write over-compute is structurally unrepresentable. .lazy() (or disposing the Computed) reverts it to lazy behaviour (the backing value stays readable but is no longer eagerly kept fresh); is_eager() reports the current state.

  Normative eager semantics. The four clauses below are what a binding conforms to. They are stated as observations a caller can make, so that any implementation strategy satisfying them conforms — see Composition is recommended, not required below. (The conformance fixtures still carry the historical signal filenames; the concept is an eager Computed.)

  1. Creation materializes once. computed(compute).eager() MUST run compute exactly once at creation and MUST NOT expose an intermediate unset state. A reader immediately after creation observes the computed value without triggering a compute of its own.
  2. Fresh at mutator return. After a set that invalidates the eager Computed’s dependency cone returns, its value MUST already equal what compute yields from the current sources, with no intervening read. This is the clause a lazy Computed does not satisfy, and it is the operational meaning of “eager”.
  3. Once per flush, not once per write. Inside batch(run), an eager Computed whose dependencies are written N times MUST re-materialize once, at the outermost batch exit — not once per write. The puller is an effect and obeys Effects are scheduled, not inline; a Computed that re-materializes during invalidation rather than during the flush violates this clause even though it satisfies (2). N writes inside a batch MUST produce exactly one compute.
  4. .lazy() removes only the puller. Reverting an eager Computed to lazy MUST dispose the eager puller and MUST NOT dispose the backing value. After .lazy() the value remains readable, remains correct on read (it reverts to lazy recompute-on-read), and MUST NOT re-materialize on write. This is why the operation is a state transition back to lazy rather than a teardown, and why the old dispose_signal naming was an inaccuracy.

  Composition is recommended, not required. Clauses 1–4 are observable. “A guarded Computed plus a puller effect” is the construction that satisfies them and is what every binding SHOULD use — it is five lines over the public API and needs no teardown special case. It is deliberately not a MUST, because which nodes exist internally is not something a caller can observe, and this specification does not mandate unobservable representation (the same rule that lets a binding choose weak back-edges). A binding that welds eagerness into its computed-cell invalidation path conforms if and only if it satisfies all four clauses — and clause 3 is the one such a binding is most likely to fail, because re-pulling during invalidation is earlier than the flush.

  A binding MUST NOT make eagerness a node kind in its graph representation: the kernel’s node enumeration is SourceCell, ComputedCell, Effect — the two value-bearing cell kinds plus the sink. An eager Computed is a ComputedCell with an Effect, not a fourth kind to dispatch on. This is now a MUST NOT rather than the old SHOULD NOT, because computed().eager() makes the composition the only way to build eagerness: the handle a caller holds is the Computed itself, read with ordinary get, and there is no Signal type left to ship. The kernel stays closed because the DAG positions are closed — the same reason this specification declines to mandate weak back-edges is why it need not police a construction that cannot be written.

  Conformance: conformance/reactive-graph/signal_*.json (historical filenames).

  Measured 2026-07-20. What replaying the three signal fixtures against every context each binding ships actually found. Recorded as measurements, not as inferences from which types exist — the discipline established by the capability table above.

  Binding	Clauses 1, 2, 4	Clause 3	Construction
  lazily-js	pass	pass	composed
  lazily-kt	pass	pass	composed
  lazily-cpp	pass (Context)	pass	composed
  lazily-py	pass	failed, fixed	welded → composed
  lazily-dart	pass	failed, fixed	welded → composed
  lazily-go	pass	failed, fixed	welded → composed → Memo-backed
  lazily-zig	4 fails on AsyncContext	failed on ThreadSafeContext, fixed	composed

  Clause 3 caught four bindings across two unrelated mechanisms, and every one of them produced correct values while doing 2–3× the computes — which is why none of the other 11 reactive-graph fixtures saw them.

  Mechanism A, welded eagerness (py, dart, go). Three bindings independently grew a signal-specific slot subclass whose invalidation handler re-pulled the signal inline. Re-pulling during invalidation is earlier than the effect flush, so the compute count scaled with the number of changed sources. No effect existed anywhere in the construction. Nobody coordinated this; the same wrong design was reached three times in three languages.

  Mechanism B, a batch that does not bound the flush (zig). set flushed effects unconditionally while batch only nested a depth counter, so a correctly composed puller still ran once per write. A composition is not sufficient if the batch boundary does not gate the flush.

  The async surface is the family’s weakest, systematically. lazily-cpp’s AsyncContext exposes no signal API at all and its async slots carry no dependency graph; lazily-zig’s async context has no lazy mode, so every derived slot is eager whether or not a puller is attached and clause 4 is unobservable there; lazily-py and lazily-dart ship no async signal constructor. A binding MAY omit signal from a context — clause conformance is per surface, and a context that does not offer the constructor is not non-conformant. What it MUST NOT do is offer it and diverge silently.

  lazily-go was the deepest case and is now resolved. Its Memo implemented the == guard by recomputing during invalidation, so a memo-backed signal could not satisfy clauses 3 and 4 while a slot-backed one lost equal-recompute suppression — neither could hold, because the cascade consumed reverse edges as it walked. Marking a dependent clean without recomputing meant it never re-registered, so its source could no longer reach it and the next write was lost at depth two, which is hybrid_serves_stale_value_at_depth_two.

  Its sync plane now uses a non-consuming mark-frontier walk with a pull-time guard, converged on lazily-rs’s model rather than a new design. Two details from that convergence are worth recording for any binding attempting the same migration, because both were initially judged redundant and both were forced back by the corpus:

  • Notifying dependents when a slot’s value actually changed is what makes the pull walk order-independent. Without it, a dependent that refreshes in an unlucky order observes “no dependency changed” and keeps a stale cache. Full-cone marking does not subsume it.
  • A force-run flag on effects. Without one the guard cannot reach effects at all: a transitively scheduled effect runs before the memo can suppress it. The pull-time re-mark must not re-schedule effects, or an effect re-runs itself mid-flush.

  Its AsyncContext was deliberately scoped out and still does value-only suppression where the sync plane suppresses downstream entirely. That divergence between a single binding’s two planes is recorded in the binding rather than resolved here.

Reactives have no observers (#lzdartobservercow)

No reactive exposes an observer API. Not a Source, not a Computed, eager or lazy — no kind of cell. No subscribe, no on_write, no on_change, no add_listener, no callback collection of any kind attached to a reactive node. A binding MUST NOT provide one, and MUST NOT carry per-node storage reserved for one.

The clause is stated on reactives rather than on Cell because it was first written too narrowly and a second registry survived it: lazily-py carried a Signal.subscribe — documented in its own docstring as “an external (non-reactive) change callback”, with the real graph edges tracked separately — that a Cell-only prohibition did not reach. It deduplicated by equality via a set, the same defect this section elsewhere calls a MUST NOT. If the rule is worth having it is worth having on every node kind, so it is written that way.

This is a MUST NOT about a mechanism rather than a behavior, which is unusual for this document. It is stated that way because the mechanism cannot be made safe by constraining it — every constraint below was tried, written down, and abandoned.

Observation is a graph edge, not a callback

Reading a cell inside a computation declares a dependency. The tracking stack records the edge, invalidation propagates structurally, and the graph decides when dependents run. Nobody registers anything. That is the whole design, and every guarantee the family makes — batching, glitch-freedom, coalescing, cone-settled consistency — follows from the graph knowing what depends on what.

A callback list attached to a cell knows none of that. It cannot batch, because it has no notion of a cone to settle. It cannot be glitch-free, because it fires mid-update by construction. It cannot participate in scope teardown, because it is not a node. It is the observer pattern, living inside the reactive primitive and bypassing it.

This is the substance behind a common objection: “isn’t a reactive just an observer with extra steps?” While Cell.subscribe existed the answer was embarrassing, because in four bindings it was literally true — there was an observer registry inside the cell, and callers could reach it. The honest answer is that a reactive is not an observer, and the way to be able to say so is to not ship one. Observation is declarative and structural; if a caller is registering callbacks against a value, they have left the reactive model, and the library should say so rather than provide a door.

How to tell an edge set from a registry

A binding auditing itself against this clause needs a test that does not depend on what a collection is called, because naming is exactly what hid these:

Anything that survives an invalidation is not a graph edge.

Dependency edges are re-discovered on every recompute — the tracking stack clears them and the next run re-registers whatever it actually reads. That is what makes dependencies dynamic. A collection that persists across invalidation is therefore not participating in dependency tracking, whatever its name, whatever its docstring, and whatever it sits next to.

This criterion is stated because it was arrived at expensively. lazily-py carried three registries — on Cell, on Signal, and on Slot — and every one of them was either labelled or assumed to be dependency-graph state. Two separate readers, with the source open, misclassified one each. In every case the registry sat beside a real edge set with a similar name (_subscribers next to _parents), and in every case the deciding fact was a single line: the edge set is rebound and cleared on invalidation, the registry is iterated and kept.

Apply the criterion mechanically rather than reading intent. It resolves all three without argument, and it is the only check here that does not require trusting a description.

Effect and observer are not two spellings of one thing

The distinction is worth stating flatly, because the two look interchangeable at the call site and are not:

Coalescence is the row that matters most, and it is not one mechanism but five. This family coalesces at every layer: the == store-guard drops an equal write entirely; the computed guard drops an equal recompute so downstream never learns; batch folds many writes into one invalidation and one flush; store-without-cascade skips effect scheduling for a cell whose cone holds no effect; and the merge algebra folds a run of ops into one state through ⊕. Every one of those is the graph deciding that some change does not need to be propagated — which is most of what makes a lazy reactive graph cheaper than recomputing everything.

Merge coalescence is where an observer fails hardest, and it is worth spelling out because it is not a quality-of-implementation matter. Associativity is the irreducible law of MergePolicy, and what it buys is variable flush points: a bounded relay may flush at any post-merge watermark and converge identically. The converged state is guaranteed; the sequence of intermediate values is not. Two runs of the same program over the same ops may legitimately produce different intermediate values under different backpressure, buffer sizes, or transports.

An Effect reads the converged state, which is the value the algebra actually promises. An observer fires on intermediate writes — so what it receives is an artifact of flush timing rather than data, and it is non-deterministic by design, not by defect. A caller cannot write correct code against it, because there is no contract there to be correct against.

Last-writer-wins sharpens this to a point. KeepLatest is old ⊕ op = op — the new op annihilates the previous state — and Cell ≡ Source<KeepLatest>, so every plain source cell in the family is already an LWW instance. Under a timestamped LWW register (CrdtJoin<LwwRegister>) a losing write is dropped outright: after convergence, it never happened. An observer that fired on that write reported an event the system has since decided did not occur, and any side effect it took — a log line, a queue push, a paint, an outbound message — is now describing a state that no replica will ever agree existed. An Effect never sees it, because it observes only what survived the merge.

That is the general shape of the whole objection, stated at its most concrete: observers report writes; the system’s actual semantics are about values that survive. Those are different questions, and in a coalescing, converging, distributed graph they diverge constantly.

An Effect is downstream of all four. It sees what the graph decided was worth propagating, which is why it can be glitch-free and why an unobserved subgraph costs nothing to write to.

An observer is upstream of all four and outside all of them. It fires on the raw write, before coalescence has a chance to apply. That is not a different observation strategy; it means a caller holding an observer is looking at a system whose central optimization is invisible to them, and cannot tell the difference between a change that mattered and one the graph suppressed.

Use an Effect

Everything an observer expressed, an Effect expresses:

// instead of: cell.subscribe(cb)
ctx.effect(|ctx| cb(ctx.get(&cell)))

The effect is batched, glitch-free, participates in teardown scopes, and is disposed by handle. Where a caller wants both the previous and the new value — the state-machine on_transition shape — the effect captures the previous value in its closure; see lazily-rs state_machine.rs for the reference form.

The behavioral difference is real and intended: under a batch, an effect observes the settled value. Writing A → B → C inside one batch reports A → C. Intermediate states are not observable, because that is what a batch asserts. A caller who did not want that should not have opened a batch.

Use a Topic when you need every transition

A Cell is a value: latest-wins, batched, glitch-free. A stream of every transition is a different thing, and the family already has it — Topic, present in all eight bindings, with cursors and durability. Topic.subscribe keeps its name because a topic genuinely is a subscription: an ordered stream a consumer reads at its own position.

The design error this section removes was a Topic hiding inside a Cell. A consumer needing every write — a mutation log, a replication feed, a persistence tap — should publish to a topic. That also makes the cost honest: only machines that actually expose a stream allocate one, and a plain cell pays nothing.

Why not keep it, constrained

Recorded so the argument is not re-run from scratch. Cell.subscribe was specified in detail before being removed, and each clause below was a genuine attempt to make it safe:

• Firing order is registration order, because a set- or hash-backed collection reorders on rehash and lazily-go’s map iteration is deliberately randomized. Four bindings had four answers.
• No deduplication by callback identity or equality, because two components subscribing the same bound method silently share one registration and the first to unsubscribe cancels the second. lazily-py deduplicated by equality, lazily-zig by address.
• Subscribe during notify is deferred, or a self-feeding observer extends the loop it is running in and never terminates.
• Unsubscribe during notify takes effect immediately, because in a manually-managed binding unsubscribe is routinely the step before freeing the state the callback reads, so one more call is a use-after-free.
• Disposers latch, or an unlatched second call removes a later registration belonging to a caller who never asked.
• Delivery is per write and batch does not coalesce it — which put the mechanism in permanent conflict with the batching model it sat beside.

Six clauses, four bindings, and the specification was still wrong twice in a single day: it omitted a violated clause in one binding, and its central argument cited two bindings that had never implemented the mechanism at all. A primitive requiring six normative clauses to be safe, that still diverges across the family, and whose delivery discipline contradicts the surrounding model, is not under-specified. It is misdesigned.

Two things settled it: memory carried by the graph itself, and semantics that were footguns at the edges.

The memory is measured, not estimated. Removing the observer API from lazily-zig moved @sizeOf(Cell(u64)) from 168 bytes to 32 — 136 bytes, 81%, reclaimed from every cell in every program whether or not anything ever registered. It was not only the callback collections: the reentrancy counters (notify_depth, before_notify_depth, and two tombstone flags) and the monotonic registration counter were all unconditional per-node state that existed solely to make the notify loop safe. At cell-family scale that is the dominant memory term in the graph, paid by every reactive value to support a feature with one caller family-wide. A reactive graph’s whole value proposition is holding many nodes cheaply; a per-node cost multiplied across the graph is the one kind of overhead it cannot absorb.

The semantics were worse, because the failures were all at the edges where they are hardest to find. Delivery that ignores batch while everything beside it honours it. Firing order that depends on a collection’s rehash. Two components sharing a bound method and silently sharing one registration, so the first to unsubscribe cancels the second. A disposer that removes a later caller’s registration. An observer invoked once more after asking to stop, which is harmless under a tracing collector and a use-after-free without one. Each of these is fine in the common case and wrong in a case the caller cannot see coming, which is the definition of a footgun rather than a bug: correct code and broken code look identical at the call site.

Underneath all of them is the defect no clause could patch: an observer cannot distinguish batching from coalescence. It receives a flat sequence of callbacks with no framing. Three invocations may be three separate updates or one logical update whose writes were grouped, and nothing in the callback distinguishes them — there is no signal for where an update begins or ends. Nor can it see what the graph coalesced away: a write dropped by the == store-guard, a recompute dropped by the computed guard, a flush skipped because the cone held no effect. So “the value did not change”, “nothing was written”, and “the graph decided this did not need propagating” are all the same non-event to an observer. It is an event stream stripped of both its transaction boundaries and its elisions.

This is not a missing feature to be added. It follows from sitting outside the graph: the graph is what knows where an update starts and stops, and a callback list attached to one node is structurally unable to observe that. An Effect has the framing for free, because running once per settled cone is the transaction boundary. The two mechanisms are therefore not two ways of observing a value — one can express “this update is complete” and the other cannot, at any level of specification effort.

Conformance

There are no observer fixtures. The clauses above were removed along with the mechanism, and conformance/reactive-graph/observer_*.json no longer exists. A binding conforms to this section by not having the API.

lazily-rs, lazily-cpp, lazily-js, and lazily-kt never implemented one and require no change. lazily-py, lazily-dart, lazily-go, and lazily-zig carried one and remove it, re-expressing on_transition as an effect.

The reactive-graph fixtures that remain cover disposal, teardown scopes, and eager computed cells. They require TeardownScope (ctx.scope() / disarm()) and dependency-graph introspection (dependents_of, dependencies_of, cleanup_order). Every binding replays this corpus as of 2026-07-19.

The eager-computed fixtures (historical filenames signal_*.json) need one observable the rest of the corpus does not: computes_of. It maps a node id to the cumulative number of times its compute function has run, counted from the start of the scenario. A runner MUST count every invocation of the compute, including the one at creation, and MUST NOT reset it per step. This key exists because an eager Computed and a lazy Computed return identical values for every read sequence — the only caller-observable difference between them is when compute runs, so a corpus that asserts values alone cannot distinguish computed().eager() from computed() and will pass against a binding that implements the former as the latter.

Three ops are specific to these fixtures. The caller-facing transitions are .eager() / .lazy() (§Eager computed cells); the fixture ops retain the historical signal / dispose_signal names, which a runner maps to those transitions (create-eager and revert-to-lazy). A runner MUST accept these op names — the runner panics on an unknown op, so this acceptance is the contract:

batch is a single op rather than a begin_batch/end_batch pair so that a runner need not carry nesting state. Bindings whose batch API is a closure take the writes as the closure body; bindings with explicit begin/end call them around the writes. Note that batch also appears in the reliable-sync and collections areas with unrelated semantics — these are per-area op vocabularies, not one global namespace.

Fixture shape is declared, not inferred. Every ReactiveGraph fixture carries a top-level "shape" field, either "steps" or "scenarios". A runner MUST switch on that field rather than probing for whichever key happens to be present, and MUST NOT special-case a fixture by filename — the first runner written against this corpus did exactly that, which goes stale silently the moment a second scenarios fixture is added. The schema suite cross-checks the declaration against the keys actually present, so shape cannot drift from the fixture it describes.

The two shapes are not interchangeable and the split is deliberate. A steps fixture asserts a single trace. A scenarios fixture asserts a relation between two op streams — scope_teardown_equals_fold_of_disposals.json claims that ending a scope is observationally equal to disposing its members individually, and a single steps array structurally cannot express “these two paths must agree.” It names the scenarios that must agree in expected.observationally_equal.

One trap in that fixture, stated here because every runner will hit it: cleanup_order is cumulative across a scenario, not per-step. The individual_disposal scenario spreads three disposals across three steps and pins the whole resulting order on the last of them, while scope_teardown produces all three from a single end_scope. A runner reading cleanup_order per-step will see the scenarios disagree and report a divergence that is not there.

The merge algebra and Source<T, M> (#relaycell)

A Source<T, M> is a source cell whose write is a merge rather than a replace: merge(handle, op) computes ⊕(current, op) under MergePolicy M and routes the result through set — so the == store-guard, store-without-cascade, and batch all apply unchanged. A plain Cell is exactly Source<KeepLatest> (the keep-latest instance, the default of the one source kind); a binding MAY implement it as that instance or keep it as a distinct fast path with identical semantics. The policy M is a real parameter of the Source<T, M> handle, so it exists exactly where writes exist and is absent on the computed side — never a third parameter every signature must spell.

Theorem — merge policies must be cheap (§9.2.1). MergePolicy::merge MUST NOT block and SHOULD be O(1)-ish in the size of old. The algebra is the convergence guarantee, so the fold stays synchronous; the async or expensive work that produces an op lives in the Effect that feeds the cell, never in the fold. In a ThreadSafeContext the fold runs under the mutex, so an expensive merge holds the lock for its duration. This constrains implementations rather than observable behaviour, so it is review-enforced, not fixtured — the same construction the observer prohibition uses.

Feeding a Source from another reactive

A recurring question, answered here because the answer is not obvious and the failure mode is one cycle detection cannot see.

A Source never acquires a dependency edge. That is what makes it a source: source and computed partition the graph by incoming edges, so a node fed by the graph would be both, and Computed → Source → Computed would become constructible. So “feed this source cell from that reactive” is not a new capability on the cell.

Theorem — a writer is always a sink (§9.2.2). Writing is not having a value: anything whose job is to write reads something and produces no readable value, which is incoming edges and no value — the Effect position. So a network-fed cell, a feedback writer, and an eager puller are each an Effect, not a new node kind. The kernel is closed because the DAG positions are closed. The family reached this answer three times from three directions — eager values (proposed as Signal), feedback (proposed as FeedbackEffect), and writer encapsulation — and each was an Effect composed with set/merge/.eager(). Stating it once retires the question; only the ergonomics (a named feed_async constructor) stay open, and those wait on two real call sites.

So feeding a source is an Effect that reads the reactive and calls merge:

effect(|ctx| { merge(acc, ctx.get(upstream)) })

The edge belongs to the effect. The cell stays edge-free, the partition holds, and the construction needs no new node kind — the same answer the family gave for eager values.

Delivery is per settled cone, not per write. The effect runs once per flush carrying the post-coalescence value, so 1 → 2 → 3 inside a batch produces one merge, of 3. This is a feature rather than a limitation: the intermediates were never materialized, because eliding them is what a lazy graph is for. An Effect is the only mechanism with the framing to do this correctly — it sees a settled value at a boundary, where an observer would see raw writes with neither.

Therefore merge granularity is flush granularity, and this MUST be stated wherever the construction is offered. With a non-idempotent policy (+, count, append-to-log) the accumulated result depends on how writes were batched: three unbatched writes fold three times, the same three writes inside a batch fold once. That is not a defect — it follows from Effects are scheduled, not inline — but the accumulator is the case callers reach for first, and it is the case where the difference is visible.

For an exact fold over every operation, do not drive it from a dependency edge. Drive it from explicit merge calls or from a Topic:

The first two are exact because the caller or the topic decides how many operations exist. The third is flush-granular because the graph decides, and deciding not to produce an intermediate is the graph working as designed. This is the same event-versus-state split recorded in relaycell-backpressure-analysis.md — retained events versus coalescible state — and it is why the answer to “I need every transition” is Topic, not a new capability on a reactive.

merge folds synchronously inside a batch; only propagation defers. This follows from merge routing through set and from Mutation inside a batch is synchronous, but it is stated explicitly because “does batching lose my merges?” is the first question the accumulator case raises. It does not. Every merge call folds when it is called. What a batch defers is the invalidation and the flush, so N calls inside a batch produce N folds and one invalidation.

Feedback: the construction cycle detection cannot see

An effect that reads R and merges into M, where M is upstream of R, closes a loop through the scheduler rather than through the graph. It is not a dependency cycle, so the acyclicity check will not fire.

Theorem — feedback is when an argument is also a dependency (§9.2.3). An Effect relates to a cell in two ways that look alike and behave nothing alike. A write target is an argument: passed in, captured by the closure, known statically, creating no edge — and, because set/merge are kind-restricted to Source, an effect cannot even take a Computed as a write-argument (it does not compile). A read is a dependency: discovered at run time by the tracking stack and re-discovered on every rerun. Feedback is exactly the case where an effect writes a cell it also reads — a write-argument that is also in deps(E). Nothing about that is a graph cycle (the argument is no edge), which is why acyclicity never fires and the loop closes through the scheduler. Prefer this phrasing over “an effect that writes into its own dependency cone,” which makes a scheduler property sound like a graph one.

This is deliberate and it is the family’s only way to express feedback: the dependency graph is acyclic by construction, so a cycle cannot be an edge. Closing it through the scheduler makes each iteration a flush, which bounds it in time and makes it observable — a discrete-time recurrence rather than an unbounded walk:

x_{n+1}  =  x_n ⊕ f(x_n)

Termination needs two properties, and the policy’s algebra supplies only one.

Where ⊕ is a join on a semilattice — idempotent, commutative, associative, the properties a CRDT policy carries — every step satisfies x_{n+1} ⊒ x_n, so the state traces a non-decreasing chain. That is the ascent, and it is all the join gives you.

It does not give you termination. The chain stabilizes only if the lattice also satisfies the ascending chain condition — no infinite strictly increasing chains — and idempotence, commutativity and associativity imply nothing about chain height. A G-Set or OR-Set over an unbounded domain is a perfectly good join semilattice whose chain ascends forever if f keeps producing fresh elements; LWW over unbounded timestamps is the same. Most CRDT policies are not finite-height. A policy declaration therefore does not certify that a feedback loop over it terminates; ACC is a separate property of the value domain and must be established separately.

ACC and bounded height are different properties, and the weaker one is the one that matters. ACC says no ascending chain is infinite. Bounded height says there is a single constant H bounding the length of every chain. Bounded height implies ACC; the converse fails. A witness: take ⊥, a top ⊤, and for each n ≥ 1 a disjoint ladder (n,1) ⊏ … ⊏ (n,n), with joins across different ladders landing on ⊤. Every ascending chain is finite — so ACC holds — while chain lengths are unbounded, so no H exists. Termination needs only ACC. The distinction is recorded because a flag can only ever declare the stronger property (see below), so the two must not be written as synonyms.

Where ACC does hold, the == store-guard is the fixpoint detector: once the join stops moving the value, nothing invalidates and the cascade ends. f need not be monotone for the ascent, which is why this is not the classical monotone-framework result — Kleene iteration requires a monotone transfer function and delivers the least fixed point. This construction reaches a fixed point and offers no leastness guarantee.

The termination condition, stated correctly, is x ⊕ f(x) == x — the loop ends exactly when the store-guard suppresses. Two consequences that an earlier draft of this section got wrong:

• An identity is sufficient, never necessary, and need not exist. If f(x) is the policy’s identity the step is a no-op, but any absorbing or saturating value is equally a fixed point — a Sum at its maximum absorbs every op. And a MergePolicy is only required to be an associative fold; nothing mandates a unit. KeepLatest is a right-zero band and has none, so “terminates when f yields the identity” is not merely false there, it is undefined.
• Correspondingly, a non-idempotent policy does not diverge by construction. It has no guaranteed fixed point; whether it reaches one is a property of f and the value domain, and the caller owns that argument.

The three termination classes

The split is not two-way, and the default policy is in the third class.

KeepLatest is the case a caller will actually hit, because Cell ≡ Source<KeepLatest> — an effect that reads a Computed and writes back to a plain source cell is the most reachable feedback loop in the family. Under a right-zero band the merge discards prior state entirely, so there is no ascent, ACC is irrelevant, and the lattice framing does not apply at all. What remains is x_{n+1} = f(x_n) over unbounded state with arbitrary f, which is Turing complete: no analysis can decide in general whether such a loop halts.

A caller in that class cannot appeal to the algebra. They must supply one of: a decreasing measure, an iteration bound, or a cancellation observed in the effect body (see below).

Accordingly:

• A caller building a scheduler-closed feedback loop MUST be able to state why it terminates. The policy’s declared algebra is sufficient evidence only for a join over a domain satisfying ACC. In every other class the caller owes an argument the specification cannot supply.

• Bindings MUST bound the effect-drain iteration count within a single flush, and report exhaustion rather than spinning. Note this is not re-entry depth: every binding surveyed guards re-entrant flushes and returns immediately, so the loop is a flat unbounded drain at constant stack depth, and a re-entry-depth bound would be pinned at 1 and could never fire.

  The bound’s value is deliberately unspecified and is not part of the contract — it is a binding’s tuning parameter, and pinning a number would make a legitimately long cascade non-conformant. What is normative is that the drain has an exit other than an empty worklist, and that taking that exit is observable: exhaustion MUST surface as a distinguishable outcome (a raised error, a reported diagnostic, a context-level status) and MUST NOT be a silent truncation of the cascade. A silently truncated flush leaves the graph in a state no clause of this specification describes — dependents marked dirty with their effects never run — which is worse than the livelock it replaced, because it is indistinguishable from convergence.

  Why this was raised from SHOULD. Three flush loops were read directly (lazily-rs Context::flush_effects and ThreadSafeContext::flush_effects, lazily-js flushEffects). All three are re-entrancy-guarded flat drains whose only exit is an empty worklist; none bounds anything. A SHOULD that no surveyed binding implements is not a requirement, and the failure it permits is a silent livelock on a thread that has starved whatever would diagnose it. The bound is also the enabling condition for fixturing this section at all: a conformance runner cannot replay a divergent feedback loop against a binding whose only exit is convergence, because the fixture hangs the runner. This section has stood as unfixtured normative prose precisely because there was no bounded failure mode to assert against.

Where a cancellation can be observed. In a synchronous context the flush does not return to the caller between iterations, so the calling thread cannot observe an interrupt and in fact starves whatever would deliver one. The available yield point is the effect body, which is caller code running once per iteration; declining to write ends the cascade, because an empty worklist is the drain’s only exit. Async contexts additionally suspend between iterations. Unmeasured: whether any binding’s async drain observes cancellation between iterations has not been checked.

Exhaustion SHOULD say what was cycling. A bound that reports only that it was hit sends the reader to a debugger on a thread that has just stopped livelocking. A binding SHOULD report the nodes that re-ran repeatedly and, where cheap, the repeating values — the difference between “drain exhausted after N iterations” and “drain exhausted; acc and total alternated”. Only the second is actionable. Representation is a binding’s choice.

Termination state belongs in the graph, not in a closure

The stop predicate that ends a feedback loop SHOULD be a Computed, read by the effect, rather than a branch buried in the effect body:

done = computed(|ctx| ctx.get(acc) >= threshold)
effect(|ctx| { if ctx.get(done) { return } merge(acc, f(ctx.get(upstream))) })

This is a recommendation about where to put a condition, not new surface — it is a Computed and an Effect, both already kinds. What it buys:

• It is inspectable. Other nodes may read done; a UI can show it; another effect can react to it.
• It is fixturable. A fixture can assert done transitions and that merging stops. A predicate inside an effect body is opaque to the corpus, which is part of why this area went untested.
• It is reviewable. The termination argument the clause above requires a caller to state becomes a named node rather than a comment.

The shape is legal under the source/computed partition, which is worth checking explicitly because it looks circular: acc → done → effect → acc. The final hop is a write, not a dependency edge, so acc acquires no incoming edge and no dependency cycle exists. It remains scheduler-closed, one iteration per flush.

It does not make termination decidable. A done that never becomes true diverges exactly as before; the drain bound remains the backstop.

Accumulators

An accumulator is a Source<M> under an accumulating policy. That is what the merge algebra is for.

A Computed cannot be an accumulator, for two independent reasons, and the second is a live hazard:

1. No self-edge. A Computed‘s value is a function of its dependencies’ current values; accumulation is a function of history. Reading its own previous value would be a self-dependency, which the acyclic graph forbids.
2. Recomputes are elidable, so an impure workaround silently loses data. A compute body closing over a mutable counter compiles everywhere and looks correct. But the graph is free not to run it: the guard suppresses a recompute whose value is unchanged, a Computed with no readers never runs, and a batch coalesces N invalidations into one recompute. Each of those drops an increment. A binding MUST NOT document or example this pattern.

The structural rule, stated once because it decides these questions generally:

Memory of its own past implies a Source. A Computed must be recomputable from its dependencies, and a value determined by history is not. This is why a Source<M> is a source even though it computes — ⊕(current, op) reads its own prior state, which no Computed may do.

The exception that confirms it: a Computed folding a Topic’s retained events is an ordinary derivation, because the history is materialized in the topic and the fold is a pure function of current state.

Recall also that driving merge from a dependency edge is flush-granular, so an accumulator fed that way counts flushes, not writes. For an exact count, drive it from explicit merge calls or from a Topic.

There is no fixpoint construct, and this records why

A termination construct was designed for this section and declined. Recorded briefly so it is not re-derived; this is rationale, not specification.

The proposal was a fixpoint restricted to policies declaring a new BOUNDED_HEIGHT, plus a fixpoint_with(cell, f, measure) taking a strictly-decreasing measure. Three reasons it failed:

1. The flag would be unverifiable. COMMUTATIVE and IDEMPOTENT are honest because they are refutable by sampling — one counterexample disproves a claim; neither is confirmable, and this document does not pretend otherwise. ACC is not even refutable: every finite chain observed is consistent with it. The stronger bounded-height-with-constant is refutable and is vacuous — Max over a 64-bit integer has height 2^64. A declared property that is unverifiable or vacuous is worse than no property, and that test generalizes past this proposal.
2. It could not cover the reachable case. Cell ≡ Source<KeepLatest>, and a right-zero band has no ascent, so an ACC-restricted construct is by construction absent from the class callers actually hit.
3. A measure parameter adds no capability, and the construct is a composition promoted to a primitive. A caller who can compute a decreasing measure over their own state can compute a stop predicate over that same state — which is the Computed pattern above, written with kinds that already exist. Signal was retired for exactly this shape.

What the proposal genuinely offered was diagnosis, which is retained above as a SHOULD on exhaustion reporting.

Conformance for this section

Three fixtures are specified; they are not yet written.

Deliberately absent: the bound’s value, the exhaustion outcome’s representation, and any assertion about how many times a given effect ran.

Unfixtured and unverified, stated explicitly. Until these exist, treat cross-binding agreement on this whole section as unverified — the eager-computed semantics sat in exactly this state for months while a binding shipped a different construction under a green checkmark. Separately unmeasured: whether any binding’s async drain observes cancellation between iterations. And the MUST above is currently satisfied by no surveyed binding; it describes required behavior, not observed behavior.

A MergePolicy is an associative fold ⊕ : T × T → T. The properties it satisfies are selected by the transport contract, not fixed (relaycell-backpressure-analysis.md §2):

Policies are open. A binding MUST permit application-defined policies. The list below is canonical, not exhaustive: a MergePolicy is any associative fold with honestly declared flags, and a binding that ships a closed enum of policies has implemented a subset rather than the algebra. Merge semantics are domain knowledge — a text register, a set of tags, a running quantile, a per-tenant precedence rule — and the family cannot enumerate them in advance. A binding MUST expose the policy interface publicly, and SHOULD accept a custom policy anywhere a canonical one is accepted.

With one obligation attached, and it is the whole cost of the openness. An application-defined policy MUST declare COMMUTATIVE and IDEMPOTENT truthfully, and a binding MUST ship the law-test harness that checks a policy against its own declarations — the same harness that verifies the canonical policies, exposed for application use.

A policy that misdeclares its flags does not fail loudly. It converges correctly in every single-replica test, every in-order test, and every test without redelivery — and diverges only under the conditions the flag was supposed to license: a claimed-commutative policy that isn’t will disagree between replicas that saw the same ops in different orders, and a claimed-idempotent one that isn’t will drift under at-least-once delivery. Both surface as replicas that silently stop agreeing, arbitrarily far from the code that caused it. That is why the flags are verified rather than trusted for the canonical policies, and the reasoning does not weaken for a policy an application wrote. Shipping the checker is therefore part of shipping the extension point — an unverifiable declaration is worse than no declaration, because the relay acts on it.

The canonical policies (each names its algebraic structure and flags):

A replicated cell that accepts writes from more than one authority MUST use a commutative policy. This follows from the reordering tax above, but it is stated separately because the default is the trap: Cell ≡ Source<KeepLatest>, and KeepLatest is not commutative. A plain cell replicated to peers that also write it will converge differently depending on arrival order — the exact defect the algebra exists to prevent, arrived at by writing no policy at all. The multi-writer replicated case wants CrdtJoin<LwwRegister> or another commutative policy, chosen deliberately.

“More than one authority” is about who may write, not about topology. A replicated derivation pushed to a peer that only reads it has one authority and needs no commutativity — on that peer it is read-only, exposing only get without the Source write methods, which is the read-only replicated cell shape. Commutativity becomes mandatory the moment the receiving peer may also write.

Derived default with user override. A recurring shape worth naming, because it looks like it needs a new primitive and does not. Where a value has a computed default that a user may override:

• Co-located — use the graph, not a policy. A Source holding the override (absent = defer), a Computed holding the derivation, and a Computed selecting override ?? derived. Glitch-free, self-documenting, and “reset to default” is clearing the override cell. No arbitration exists to get wrong.

• Distributed — a merge policy is required, and a valid one exists: tag ops with provenance and fold by precedence (user outranks derived, LWW within the user rank). It satisfies all three properties — associative because a higher rank absorbs a lower one regardless of grouping, commutative because rank comparison is order-free and ties resolve by timestamp, idempotent because re-applying an op of equal rank and stamp is a no-op.

  The hazard is reset-to-default, and it is not obvious. Clearing an override is an op that lowers precedence, and a naive “a clear beats the user rank” rule is not commutative — a clear arriving after a newer user edit would wrongly win. The clear MUST carry a timestamp and lose to any user op newer than itself, which makes it an ordinary participant in the LWW rank rather than a special case. A binding that special-cases the clear will pass single-replica tests and diverge only under reordering.

KeepLatest (positional last-writer-wins, not commutative) is distinct from a timestamped LWW register (CrdtJoin<LwwRegister>, commutative): both conflate, they differ only on commutativity — the CRDT-vs-LWW branch. RawFifo cannot conflate (order and multiplicity are meaning); its only bounded-lossless option is Spill (Phase 3+). CrdtJoin<C> wires the existing cell CRDT units (Merge mechanisms) into the algebra without reimplementing their join.

Verification form. The three properties are algebraic identities over T values ((a⊕b)⊕c == a⊕(b⊕c), (a⊕b)⊕c == (a⊕c)⊕b, (a⊕b)⊕b == a⊕b), so a binding pins them with property-based law-tests (associativity for every policy; commutativity/idempotency asserted exactly when the flag is set, plus a counterexample proving a cleared flag does not lie) — lazily-rs uses tests/merge_laws.rs. The cross-language converged-state determinism invariant (same op multiset, any grouping → same egress) is additionally pinned by the mergecell_algebra.json compute fixture.

Invalidation propagation

When set changes a value (post-==-guard):

1. The cell’s dependents are marked dirty (computed cells) or scheduled (effects).
2. Dirty marks propagate transitively through computed dependents — a dirty Computed marks its own dependents, and so on. A Computed that recomputes to an equal value stops the propagation (the computed guard).
3. On the next get of a dirty Computed, it refreshes: it pulls each dependency (recursively refreshing/ recomputing as needed), and recomputes only if a dependency actually changed value.

This is a push-invalidated, pull-recomputed graph — invalidation travels downstream eagerly (so effects fire), but the new value is computed lazily on read (so untouched branches do no work).

Store-without-cascade (the write-side dual of lazy reads). When set changes a value whose transitive dependent cone contains no Effect, the new value is stored (step 1’s dirty-marking of lazy computed dependents still happens, so a future subscriber reads the current value glitch-free — late-subscribe correctness) but no effect flush is scheduled — there is no active reactor to run. A binding MAY skip the flush machinery entirely in this case. Combined with demand-driven derivation on the read side, an unobserved reactive node — pull-derived or push-populated — costs approximately its raw storage: the merge cost law tiers the write cost by dependent kind (none → store only; lazy-only → store + O(deps) dirty-mark, no flush; active → store + dirty + flush). A burst of N value-changing writes with no interleaved active read pays the transitive dirty-mark once (dirty-marking is idempotent and monotonic — an already-dirty Computed is not re-walked), i.e. N·(==/⊕) + one dirty-propagation. See relaycell-backpressure-analysis.md §4.0.

Handles and identity

A handle is a Source<T, M> or Computed<T> (or EffectHandle) carrying a SlotId — and here Slot is the storage concept, not a reactive value: a slot is the arena position that holds a node, and it holds any kind (SourceCell, ComputedCell, or Effect). SlotId, SlotValue, and the slab vocabulary are accurate under this storage meaning and are unchanged by the kernel rename; the reactive-value node the arena holds is a SourceCell or a ComputedCell. The slot persists across recycling; its occupant does not (recycled_id_inherits_nothing).

Slot ids are minted monotonically and recycled on dispose. A disposed handle is inert: reads on a disposed Computed return its last cached value if any; reads on a disposed Source, or on a Computed whose eager puller was disposed, are undefined (the caller MUST NOT retain a handle past disposal). Re-entrancy of a disposed effect is prevented by removing it from the schedule before running cleanup. Detection of a stale handle is bounded (see Disposal is explicit): a binding that recycles slot ids MAY admit a same-kind ABA read unless its SlotId carries a generation tag.

Context layers

• Single-threaded — the base context (mirrors lazily-rs Context). The graph is not Send/Sync; it lives on one thread/executor. Unconditionally required of every binding (it is the reactive core).
• Thread-safe — a lock-backed counterpart (mirrors lazily-rs ThreadSafeContext); handles are clonable and the transition function and state are Send + Sync. Effects are scheduled and flushed within the invalidating send/batch, preserving glitch-free pull-based ordering. Required of any binding whose platform exposes preemptive multi-threading or shared-memory concurrency — see Wire Protocol § Concurrency layers are required.
• Async — a separate reactive surface for future-returning computations; see Async Reactive Context. Required of any binding whose platform exposes an async/future runtime — see Wire Protocol § Concurrency layers are required.

The single-threaded context is the unconditional base; the thread-safe and async layers are required conditionally. A platform that structurally lacks either primitive (a strictly single-threaded runtime, a process/actor-isolation model, or a platform with no suspendable async computation) declares the matching thread_safe / async capability as none and advertises it, never silently. The flat State Machine and State Charts compose with whichever reactive context a binding ships, with identical send semantics.

Conformance

A reactive context conforms when:

1. The kernel’s two cell kinds — nodes SourceCell / ComputedCell, handles Source<T, M> / Computed<T> — and the sink Effect are implemented; an eager Computed (computed().eager()) is the eager construct — not a fourth kind.
2. Every cell is guarded on T: PartialEq: set is ==-guarded (equal value is a no-op) and computed is guarded on recompute (an equal recompute suppresses downstream). There is no unguarded mode.
3. Refresh is pull-based and glitch-free: a Computed observes consistent inputs; untouched branches are not recomputed.
4. Dependencies are tracked dynamically through a tracking stack (edges re-registered each recompute; no manual subscribe).
5. Cycles are detected and throw.
6. batch coalesces into one propagation + effect flush at the outermost exit.
7. Effects fire scheduled (not inline), cleanup runs before each rerun and on dispose, and disposal unsubscribes edges.
8. An eager Computed is materialized by the time the invalidating set/batch returns (eager push).
9. Read on every cell, write on the source kind. Reads (get) are on every cell — Source and Computed alike. Any generic alternate read surface (for example the optional get_shared / Rust Context::get_rc) MUST cover the same two kinds and preserve ordinary-read value, refresh, and dependency-tracking semantics. Writes (set/merge) are on Source<T, M> alone — a compile error on a Computed, enforced by the type rather than a trait (a read-only interface in Go, §4 of the design). There is no subscribe — see Reactives have no observers.
10. The merge algebra (#relaycell). merge(handle, op) folds under an associative MergePolicy and routes through the ==-guarded set (so an idempotent policy’s no-op merge fires no cascade). Cell ≡ Source<KeepLatest>. Every policy is associative; the COMMUTATIVE and IDEMPOTENT flags match the policy’s algebra (verified by law-tests); the converged egress state is independent of merge grouping/order for a commutative policy (verified by mergecell_algebra.json).

Declared context capabilities

A binding MUST declare, per context it ships, where that context sits on two independent axes. The declaration exists so the conformance harness can decide which fixtures apply. It has no other purpose, and the constraints below are part of the requirement rather than commentary on it.

Axis 1 — read discipline. Either blocking (reads return values) or async (reads return futures/promises). Mutually exclusive per context.

Axis 2 — concurrent access. One of:

The three-way split on axis 2 is not pedantry — it was added because a two-way thread-safe: yes/no flag would have been satisfied by four bindings offering materially different guarantees. Measured 2026-07-19: lazily-rs and lazily-py share one graph across OS threads; lazily-js shares an Atomics-backed lock across worker realms while each realm keeps its own graph; lazily-dart is a single-isolate reentrancy guard with no cross-isolate anything. Every one of those is individually honest and documented, but a fixture asserting concurrent-access behavior is meaningful only at shared-graph and vacuous at serialized. A flag that cannot tell them apart produces exactly the failure this chapter exists to prevent: a suite that passes while testing nothing.

Feature-group rule. A serialized context is a meaningful execution flavor when it supplies a distinct linearization boundary for reentrant or concurrent logical callers, even though its graph is realm-local. It joins every portable Core feature test that its surface supports (ordering, membership, atomic move, materialization). It does not join shared-graph stress/model-check tests. A binding may instead declare the context absent; then it is staged out of that peer group. Merely publishing a duplicate type is not support: an incomplete wrapper remains partial/absent, and a test runner MUST NOT fill its gaps with a base-context object, ad hoc mutex, or ordinary dictionary.

The axes are independent. Read discipline does not imply a concurrency level and vice versa. Single-threaded async is fully concurrent while requiring no thread-safety at all, and a blocking context may be shared-graph. A binding MUST NOT infer one axis from the other.

The declaration is not wire-visible. Context capability MUST NOT appear in any protocol message, influence sync behavior, or be observable by a peer. The reactive graph is compute, not protocol; only resolved values cross IPC/FFI, and convergence is a property of the merge algebra rather than of any replica’s local execution model. Associativity already licenses variable flush points, so local scheduling is unconstrained by the protocol — which is precisely why the execution model producing that scheduling is irrelevant to a peer. A replica running an async context and one running a shared-graph context converge because ⊕ says so, not because they agree about threads.

This constraint is stated because the failure mode is quiet. Nobody sets out to leak the execution model into the protocol; it happens when a sync path needs a decision and a capability declaration is conveniently in scope. The declaration answers exactly one question — which fixtures run — and the moment it answers a second, the layering is broken.

Thread-safe context conformance

The lock-backed context (Context layers) is required of any binding whose platform exposes preemptive multi-threading or shared-memory concurrency. A binding’s thread-safe context conforms when it holds these deterministic properties under concurrent access:

1. Handles are clonable, and the transition function and source/computed node state are Send + Sync; one reactive graph is shared across OS threads.

   This clause applies only to a context declaring shared-graph (see Declared context capabilities). A serialized context — lazily-js, whose graph is per-realm, or lazily-dart, whose guard is single-isolate — cannot satisfy it and is not required to. Conformance for those is the linearization property alone: concurrent callers are ordered, and none observes a half-updated graph. Requiring a shared graph of every “thread-safe” context would have made two bindings permanently non-conforming for having chosen a design their platform actually permits.

2. Effects run glitch-free under concurrent access, preserving the same ordering as the single-threaded context — a concurrent reader never observes a half-updated graph. This mandates glitch-free ordering (every effect that runs sees the fully settled cone, never an intermediate state), not literal in-lock dispatch. A threaded binding MAY defer effect dispatch out of the graph lock, so a callback may re-enter the context, provided the ordering invariant holds: effects are delivered in dependency order and none observes a mixed state.

   (This clause previously governed observer callbacks, under #lzspecobserverclarify. Observers were removed from the family — see Reactives have no observers — and the requirement now attaches to effects, which are the only remaining way user code runs inside an invalidation wave.)

3. The == (PartialEq) source guard and the Computed equality guard both hold under concurrent mutation: an equal write invalidates nothing, an equal recompute suppresses downstream work.

4. The graph lock is released before user compute/effect/cleanup callbacks run, so callbacks may re-enter the same context without deadlock.

5. An in-flight recompute is parked on a per-slot generation/condvar sidecar; a stale completion (the slot was invalidated during compute) is discarded and the waiter retried against a fresh value rather than observing a mixed state.

Verification form. Concurrent interleaving is not a deterministic load/replay sequence, so it is not pinned by a portable conformance fixture in lazily-spec. Each binding verifies its lock-backed context with a synchronization-model checker over the same semantics above — lazily-rs uses Loom (tests/thread_safe_loom.rs, behind the loom feature). The five properties above are the contract that model check exercises; a binding with no such tooling MUST at minimum exercise 1–4 under a threaded stress harness.

Implementation status

The single-threaded reactive context is required of every binding that advertises the reactive core. lazily-rs, lazily-py, lazily-zig, lazily-kt, and lazily-js implement it. The thread-safe and async counterparts are required of any binding whose platform supports them (see Wire Protocol § Concurrency layers are required); a platform that structurally lacks either declares the matching thread_safe / async capability as none and advertises it, never silently.

Measured 2026-07-19. Shipping a type named AsyncContext or ThreadSafeContext is not the same as implementing the capability, so this records what was found by reading each implementation rather than by counting type names:

lazily-cpp’s async context is a stub and MUST NOT be counted as implementing the capability: AsyncSlotNode carries no dependents or dependencies fields, get_async unconditionally recomputes on every call, and the synchronous get() returns a cached value that nothing ever invalidates. Depth tests “pass” through get_async only because nothing is ever memoized. Per the rule above it should declare async: none until it has a dependency graph, or implement one.

The unmeasured entries are deliberately not guesses. Absence of a finding is not a finding — that lesson is recorded in Reactives have no observers, where three bindings’ omission from a divergence table turned out to mean nobody had looked.

lazily Cell Model Specification

Normative source of truth for cell kinds and the multi-write merge mechanism.

This chapter defines the cell-kind model that the Wire Protocol serves. It is upstream of every transport: IPC, FFI, signaling, and the distributed plane all carry cells whose convergence semantics are fixed here. The Distributed: CRDT Cell Plane section specifies merge: crdt — the first multi-write merge mechanism defined below.

The single axis: writer count

A lazily graph is a set of cells. The only axis that determines how a cell’s value converges is how many writers can concurrently produce a value for it — not whether those writers are local or remote, in one process or many.

The kind is a static property of what the cell represents, chosen at definition time. There is no dynamic per-write mode switching: a multi-write cell stays multi-write even when only one writer is currently live, and a single-writer cell never becomes multi-write because a value happens to arrive over a wire.

Single-writer cells (local / direct)

A single-writer cell has exactly one writer:

• this runtime’s own derivation graph (a derived cell is always single-writer — see Derived cells), or
• a single owning runtime that one-way mirrors the cell to other runtimes via a delta projection (today’s lazily-rs → lazily-kt #lazilystatesync push is exactly this shape).

Propagation is direct reactive push/pull over the IPC or FFI channels. A mirror is still single-writer: the receiving side observes, it does not write back. No merge step exists, and none is permitted — a single-writer cell that receives a concurrent remote write is a conformance error, not a merge.

A cell mirrored one-way to N readers is single-writer. Locality does not make a cell multi-write; a second concurrent writer does.

Multi-write cells

A multi-write cell admits concurrent writes from multiple replicas. New values arrive as remote ops merged through the cell’s declared mechanism; the merged result is fed into the reactive graph as an ordinary cell update, after which propagation is identical to a single-writer cell.

A multi-write cell carries a merge: <mechanism> attribute. The mechanism is a parameter of the cell, not a separate cell kind:

Cell      = SingleWriter
          | MultiWrite { merge: MergeMechanism }

This framing is deliberate. An implementation MUST model multi-write as one cell category parameterized by a merge mechanism, and MUST NOT hardcode a single crdt cell kind. New mechanisms slot in without a new kind, and every mechanism shares the ingress boundary, the merge-unit granularity, and the downstream propagation rules below.

Merge mechanisms

crdt is the first mechanism this spec defines and the only one with a normative wire schema today (distributed.json). The mechanism slot is open by construction so later mechanisms slot in alongside it. Every mechanism MUST be deterministic — replicas applying the same op set MUST reach the same value regardless of arrival order or lag.

crdt is chosen as the first mechanism because it converges without coordination — no central ordering authority, no lock round-trip — which is the property the editor-as-replica use case needs. Reserved mechanisms are named to fix the extension shape; an implementation MAY reject any mechanism it does not implement, but MUST reject it explicitly (capability negotiation) rather than silently treating it as crdt.

A multi-write cell with a single live writer degenerates to a near-free merge (no concurrent ops to reconcile) under every mechanism. This is why the kind is chosen statically by representation: a shared cell that is usually edited by one replica still declares merge: so that the moment a second writer attaches, convergence is already guaranteed.

Merge is an ingress operation on root cells only

The merge mechanism is an ingress step at the boundary where remote ops enter a replica. It applies only to root (input) cells.

Derived cells are never multi-write

A derived cell is a deterministic function of its inputs. It has exactly one writer — the derivation — and therefore is always single-writer. Replicas converge on a derived cell because they converge on its roots, never by merging the derived value itself. An implementation MUST NOT replicate or merge a derived cell directly.

Propagate guard (computed / computed_ripple_when / slot)

A derived cell carries a propagate guard: after it recomputes, the guard decides whether the recompute is forwarded to its dependents. The guard governs propagation, never computation — a derived cell is always recomputed when it is dirty and read (laziness is the only compute gate), so a reader MUST always observe a value current with the inputs. The guard only decides whether dependents are invalidated. This is the glitch-suppression that lets a diamond re-converge without re-running consumers whose input did not meaningfully change.

Three constructors expose the guard; all always compute, and differ only in the guard predicate changed(old, new) (propagate iff true):

• computed(f) — the default. Guards by the value’s natural equality: changed = (old ≠ new). An equal recompute MUST NOT invalidate dependents. This is the #lzcellkernel guarded computed; equality semantics are the host language’s (PartialEq / == / equals), so for reference-typed values (e.g. a fresh array each recompute) suppression is host-defined and MAY not fire — this is permitted (an unsuppressed cascade is a missed optimization, never incorrect).
• computed_ripple_when(f, changed) — the same guard with an explicit, pure changed(old, new) predicate: a cheaper/custom equality (dedup a large value by a version/hash field; epsilon compare; hysteresis; monotonic gate; or “propagate every N” when the counter lives in the value). changed MUST be a pure function of (old, new); value-carried state is a permitted input, external mutable state is NOT (it would key off recompute/read frequency and break determinism). computed(f) ≡ computed_ripple_when(f, ≠).
• slot(f) — pass-through: no guard (changed ≡ true). Every recompute propagates. The escape for values with no cheap equality (!PartialEq, non- comparable collections) that a binding is fine re-firing. This is a derived constructor and is distinct from the internal storage-sense Slot that a computed node occupies.

The guard is proved in lazily-formal as recomputeSlot_equal_preserves_dependents (equal recompute leaves dependents’ dirty flags untouched) and its specialization recomputeSlot_ripple_when_false_preserves_dependents for a custom changed.

Dependency tracking (the fortified compute view)

A derived cell discovers its dependencies dynamically: on each recompute it runs its compute function and records every cell that function reads. The recorded set is re-bound every recompute (not accumulated), so a conditional read (cond ? a : b) drops the branch it did not take — an implementation MUST NOT retain a dependency a recompute did not read.

The identity that a read must attribute to — which node is being recomputed — is carried into the compute function as a value, through a per-recompute compute view (lazily-rs: Compute, the sole implementor besides Context of the ComputeOps operations subset). It is NOT ambient (thread-local / module global). This is normative because ambient state is clobbered across suspension: an async compute that reads a dependency after an await would attribute it to whatever else ran on the executor. A value threaded through the closure survives suspension (it is captured), so it is the only mechanism that tracks correctly post-await — and the only one that works where no ambient carrier exists (browser JS has no AsyncLocalStorage). Bindings whose runtime does provide a suspension-surviving ambient carrier (Python contextvars, Dart Zone, Node AsyncLocalStorage) MAY use it; all others MUST thread the value.

The compute view SHOULD be fortified so misattribution is prevented by construction, not convention:

• Sole tracking surface — a tracked read is available ONLY through the compute view; reading through the owning context registers no edge (the explicit untracked escape). A normal read therefore cannot silently miss tracking.
• Non-escapable — the view MUST NOT outlive the recompute (lazily-rs binds it by lifetime and makes it !Send), so it cannot be stored and later replayed to register an edge against the wrong node.
• Generation-stamped — a read against a node disposed/recycled mid-recompute is detected, never misattributed.

Edge-attribution invariant (normative): every dependency edge registered during the recompute of node n has n as its dependent. Because the node is a value parameter of the compute view, this holds by construction. Proved in lazily-formal as registerReads_dependent_is_recomputing_node.

Effects stay single-writer

Effects (irreversible external actions — send email, charge card, fire webhook) are not multi-write. State convergence does not authorize an effect to fire on every replica. Effects MUST be gated behind a single-writer authority (a designated peer or small consensus group) that decides when the effect fires, at-most-once. See Single-writer effect authority.

                 remote ops
                     │
                     ▼
        ┌──────────────────────────┐
        │  merge: <mechanism>      │   ← ingress, ROOT cells only
        │  (crdt | lww | …)        │
        └──────────────────────────┘
                     │  merged value as ordinary cell update
                     ▼
        root cell ──► derived cells ──► effects
                    (single-writer)   (single-writer authority)
                     └─ direct reactive propagation, identical for all kinds ─┘

Cell = merge unit

The cell is the unit of merge. Each multi-write cell converges independently; a merge mechanism operates within one cell’s value and MUST NOT move content across cell boundaries.

This is normative because the cell graph already supplies the natural merge boundaries: making the cell the merge unit makes cross-cell contamination impossible by construction. A whole-document merge that splices one logical region’s content into another (for example an agent’s console output bleeding into a queue region) is a conformance violation — each region is a distinct cell and converges on its own.

An implementation MUST scope every merge to a single cell. Coarser-grained merge (whole snapshot, whole document) is permitted only as an optimization that is observably equivalent to per-cell merge; if it can produce a result no sequence of per-cell merges could, it is non-conforming.

The per-cell merge ⊕ is characterized as an associative fold by the merge algebra (#relaycell): a MergeCell<T, M> is a cell whose write folds under a MergePolicy M, and a plain Cell is MergeCell<KeepLatest>. The merge mechanisms below are the semilattice policies (CrdtJoin<C>) of that algebra; associativity is the invariant that lets a bounded relay flush at any watermark and still converge (Phase 2+).

Liveness vs mechanism

Whether a cell is multi-write (merge: present) is static. How many writers are live against it at a given moment is dynamic, governed by an attach/detach authority state machine (e.g. an editor plugin attaching or detaching). The authority SM governs only liveness — it never changes a cell’s kind or mechanism:

• No live writer → the cell still declares its mechanism, but with zero concurrent ops the merge is inert and a durable replica MAY be ephemeral (rebuilt from a checkpoint on demand).
• One or more live writers → ops flow and the declared mechanism reconciles them.

Mechanism is a property of the cell’s meaning; liveness is a property of the current session. Conforming implementations MUST keep these independent.

Cross-process liveness as a CRDT cell. When session liveness itself must cross a process boundary — “editor pid X has doc Y open”, “pid X holds the owner lease” — it is modeled as an ordinary multi-write cell on the CRDT plane, not as out-of-band state: an OR-set for open-set membership (observed-remove, so a re-open wins over a lagging close) and an LWW register for the per-pid alive flag / lease. The derived “is this doc live” aggregate is then a plain reactive memo over that liveness keyed map (the #lzfamilysync derived-aggregate contract), and an OS process-exit event is just the highest-stamp write to alive[pid]. This keeps liveness on the same convergent, idempotent, frontier-resumable substrate as every other replicated cell. Normative semantics: protocol.md § Liveness cells.

Conformance summary

An implementation conforms to the cell model when:

1. Every cell is classified single-writer or multi-write, statically, by representation.
2. Multi-write cells carry a merge: <mechanism> attribute; multi-write is not modeled as a hardcoded crdt cell kind.
3. crdt is implemented as the first mechanism; unimplemented reserved mechanisms are rejected explicitly, never silently aliased.
4. Merge is an ingress step on root cells only; derived cells and effects are never merged.
5. Every merge is scoped to a single cell (cell = merge unit); no cross-cell content movement.
6. Downstream reactive propagation is the same direct mechanism regardless of cell kind.
7. The attach/detach authority governs writer liveness only, never a cell’s kind or mechanism.
8. A keyed cell collection (ReactiveMap — the SourceMap/ComputedMap specializations) is implemented — entries are ordinary cells, a dedicated membership cell tracks the key set, and the value / set-membership / order reactivity-independence, stable-handle, and atomic-move invariants below hold. Collections are required of every binding, not optional.
9. An ordered keyed tree (SourceTree) is implemented, inheriting the per-cell merge and atomic-move guarantees node-by-node (required of every binding).
10. Keyed reconciliation emits the move-minimized {insert, remove, move, update} op set (LIS over prior indices preserved), and a stable entry is not invalidated by a sibling reorder (required of every binding).
11. A reactive queue (QueueCell) is implemented — a FIFO collection whose reactive shell invalidates by reader kind (head / length / empty / full / closed), backed by a pluggable QueueStorage backend. The shell / storage split, closure observable contract, bounded-queue backpressure, and ordering guarantees below hold (required of every binding).
12. Materialization is eager by default — a ComputedMap’s derived entries are pre-minted over the keyset; lazy materialization (get_or_insert_with mint-on-access) is opt-in, keyed, and observationally transparent — identical read values, allocation deferred only (see Materialization). It is a behavior, not a mode flag. Lazy evaluation (bounded-viewport recompute) is provided either way and is never conflated with lazy materialization.

Materialization (a caller-provided recipe)

Cell kind (above) fixes how a cell converges. Materialization is an orthogonal axis: it fixes when a derived cell’s backing node is allocated — not what it computes, not how it converges, not how it merges. It trades memory and first-touch latency against cold full-scan cost, and it MUST NOT be observable through the value of any cell.

Why a behavior, not a mode. Materialization was first pinned as a bespoke ReactiveFamily type carrying an eager/lazy mode — a reaction to one binding (lazily-zig) implementing lazy materialization in the spreadsheet benchmark and thereby diverging from the others. Standardizing a type with a mode invites re-divergence: each binding builds it slightly differently, and most never need it. What must agree is the observable behavior the benchmark measures — transparency (a lazy read equals an eager read) and deferral (an unread lazy entry costs nothing) — not any type or flag. So materialization is normative as a behavior of the keyed primitive: it is simply what ComputedMap does — get_or_insert_with mints a derived slot on first access (lazy); a pre-mint loop over the keyset is eager. There is no materialization mode and no family type — the family types (ReactiveFamily / CellFamily) are removed; ComputedMap (a ReactiveMap specialization) is the vehicle.

The materialization recipe

Materialization is caller-provided: a keyed collection (a SourceMap or any keyed address space) plus a per-key factory whose return type is the materialization choice. Nothing new is required beyond the cell/slot/signal primitives a binding already has:

• Eager entry — the factory yields an input cell or an eager signal (a memo-slot + puller effect): the node is allocated/pulled up front; a read is a direct node access.
• Lazy entry — the factory yields a lazy slot: the node is allocated on its first observe, addressed by key. A never-observed lazy entry is never allocated.

So the caller provides materialization through two levers it already owns — whether it observes a key (unread lazy entries stay unallocated) and what the factory returns (slot ⇒ lazy, signal ⇒ eager) — with no mode flag and no per-read toggle. This is the same “lazy by default, eager when asked (via signal)” model lazily already uses at the single-cell level, applied per key. Entry kind is the pinned axis:

• Cell entries (H = Source) are input nodes — always materialized; an input has no derivation to defer. Minting an input on first get is a collection concern, not materialization.
• Slot entries (H = Computed) are derived — the ones deferral governs: an eager factory allocates them up front, a lazy factory defers each to first observe.

Entry kind is orthogonal to the materialization choice (proved in lazily-formal’s Materialization module as cell_entries_materialized_in_every_mode / slot_entries_deferred_under_lazy): lazy defers only slot entries, never cell entries.

Normative rules on the recipe:

• Eager is the default. Absent an explicit lazy opt-in, derived entries are eager — a read is a direct node access and a full recompute pays only compute. A binding MUST make eager the default.
• Lazy is an explicit opt-in overlay on the eager core, addressed by key, never the default and never a per-read toggle on an eager handle. The first observe of key k constructs the same node the eager build would have, then caches it — a keyed overlay, not a second graph engine. A binding that offers lazy MUST expose it as an explicit opt-in (e.g. a keyed factory / keyed-context constructor).

Observational transparency (normative)

For every node and every read, the observed value MUST be identical under either mode. Materialization mode is not observable on the value axis — it changes allocation timing and memory, never results:

observe(build(eager, spec), id) = observe(build(lazy, spec), id) = spec.val(id)   ∀ id

This is proved in lazily-formal’s Materialization module (observe_canonical, eager_lazy_observationally_equivalent). An implementation MUST preserve these consequences:

1. Same values. A lazy read returns the value an eager read would (observe_canonical).
2. No churn from allocation. Materializing one node MUST NOT change any other node’s observed value (materialize_preserves_observe).
3. Deferral, not de-allocation. Lazy materialization only grows the materialized set; a materialized node is never silently dropped, and the lazy set is a subset of the eager set (materialize_present_monotone, lazy_present_subset_eager).
4. Reactivity is orthogonal. Lazy evaluation — leaving off-viewport derived cells dirty and never recomputing them (the microsecond bounded-viewport read) — is required of both modes and is independent of materialization. Eager materialization still evaluates lazily; lazy materialization additionally defers allocation. An implementation MUST NOT conflate the two.

Execution-context flavors (thread-safe / async)

ComputedMap runs against a context, and the context is a third axis orthogonal to both entry kind and materialization: it fixes where and how the graph executes, not what it computes. The materialization laws hold over each context a binding provides — the ReactiveMap line has one flavor per context, and each carries the context-specific law below:

• Single-threaded (ComputedMap, over the base Context) — the reference semantics above.
• Thread-safe (ThreadSafeComputedMap, over a lock-backed context) — a Send + Sync map that can live in a cross-thread owner (e.g. a hub behind a global mutex, where an Rc-based map cannot go). It carries the same materialization laws, plus materialization confluence: the present set and every observed value are independent of the order in which keys are materialized. This is what makes lock-serialized concurrent materialization safe — any order the lock admits yields the same observable map. Proved in lazily-formal’s Materialization module (materialize_present_comm / materialize_observe_comm).
• Async (AsyncComputedMap, over an async context) — derived (slot) entries resolve asynchronously, so a non-blocking read returns an optional value (None while pending, Some(v) once resolved). Observational transparency weakens to eventual transparency: once a node resolves, its observed value is the canonical value — identical to what the synchronous ComputedMap observes. Input cells are resolved at build. Proved in lazily-formal’s AsyncMaterialization module (eventual_transparency, async_resolved_matches_sync; a pending read is never a stale value, observe_pending_is_none).

A binding SHOULD keep the per-key factory uniform across flavors, so the flavors differ only in execution context — a derived async slot wraps that factory in a ready computation. The factory SHOULD receive the entry’s own tracking view (Fn(&Compute, &K) -> V, not Fn(&K) -> V): without it a derived entry cannot read another reactive and have that read register a dependency edge, which silently reduces ComputedMap to a cache.

A flavor MUST preserve the entry-kind and materialization laws above, MUST expose the Core surface defined under “Core surface vs. binding extensions” below, and adds the context-specific guarantee (confluence for thread-safe, eventual transparency for async). Ordering and atomic move are not exempt: they are Core, and they bind every flavor the binding advertises. A binding that advertises a thread-safe or async map but ships Core only on its single-threaded map is non-conforming on that advertised flavor. A context declared absent is staged out of that peer group; a runner-local lock, dictionary, or synchronous stand-in MUST NOT be used to make the missing flavor appear covered.

When to opt into lazy

Lazy pays off only for sparsely-touched large keyed address spaces — e.g. a 10,000,000-cell spreadsheet where a session reads ~1% of the derived cells: it lowers peak memory and makes “open” cost O(inputs) rather than O(derived cells). It costs a keyed-cache lookup per read instead of a handle dereference, and a cold full scan pays allocation and compute together (eager_materializes_all vs lazy_defers_slots). Handle-based graphs that read most of what they build SHOULD stay eager. The choice is a per-context construction decision, not a per-cell or per-read one.

Keyed cell collections

A keyed cell collection is a composition of cells, not a new cell kind. It maps keys K to per-entry reactive nodes and adds a dedicated membership cell tracking the set of keys. There is one keyed primitive, generic over the entry’s handle kind:

• ReactiveMap<K, V, H> — a mutable reactive keyed dict: reactive membership + order, get_or_insert_with (mint-on-access), remove, move. H is the entry handle kind. Its two specializations are the concrete types a binding exposes:
  • SourceMap<K, V> = ReactiveMap<K, V, Source> — input-cell entries. Adds set(key, value) (an input is settable). Minting is eager-by-value.
  • ComputedMap<K, V> = ReactiveMap<K, V, Computed> — derived-slot entries. get_or_insert_with(key, factory) mints a slot on first access (lazy materialization); a slot’s value is derived, so ComputedMap has no set. Eager materialization is a pre-mint loop over the keyset; lazy is mint-on-access — there is no eager/lazy mode flag.

Deprecated spellings. SourceMap and ComputedMap were previously CellMap and SlotMap, with ThreadSafeCellMap / ThreadSafeSlotMap and AsyncCellMap / AsyncSlotMap as their per-context variants. The rename finishes the v2 kernel migration: the node kinds became Source and Computed, and the map names now say which kind they hold instead of naming a vocabulary the kernel no longer uses. A binding SHOULD keep the old names as deprecated aliases of the new ones rather than removing them, so a caller that has not migrated still compiles. Runners MUST accept the old model spellings in a fixture ("CellMap", "SlotMap") alongside the new ones — the same dual-accept the corpus already uses for the signal/eager and dispose_signal/lazy op names. The fixture FILE names keep their historical spelling; a file name is not a type name, and renaming them would invalidate every binding’s replay ledger at once for no semantic gain.

set(key, value) is therefore cell-only (lives on the SourceMap specialization); the shared surface — get_or_insert_with / remove / move / membership / order — lives on the generic ReactiveMap. There are no family types: the “keyed materialized family” is ComputedMap + the mint recipe, and the “auto-mint keyed default” is get_or_insert_with — neither needs a separate type (see § Materialization).

Required. The keyed cell collections layer is normative for every lazily binding — it is not an optional lazily-rs extension. A conforming binding MUST implement ReactiveMap (at least its SourceMap specialization; ComputedMap where the binding supports derived slots), the ordered keyed tree (SourceTree), and keyed reconciliation, and MUST validate against the canonical fixtures in conformance/collections/. The single-writer / multi-write classification, merge: mechanism, and ingress rules below are exactly those defined above — the collection adds no new merge unit.

It conforms to the cell model when:

1. Each entry is an ordinary cell — its single-writer / multi-write classification, merge: mechanism, and ingress rules are exactly those above. The collection adds no new merge unit; cell = merge unit still holds per entry.
2. Value, set-membership, and order reactivity are independent: writing one entry’s value MUST NOT invalidate membership or order readers; adding/removing a key MUST NOT invalidate readers of unrelated entry values; and a pure reorder (atomic move) MUST NOT invalidate set-membership readers (len / contains) — only order readers (keys).
3. A key resolves to a stable handle for the key’s lifetime; membership and order changes are signalled by their dedicated cells, never by mutating sibling entries.
4. Atomic ordered move (move_to / move_before / move_after): reordering a key MUST keep the entry’s same cell handle, dependents, and lineage (not remove + re-mint) and bump only the order signal once.

Exact-key dependency availability (#lzdependencyavailability)

A non-minting observe(key) correctly reports that an entry is absent, but it cannot register an edge to a node that does not exist. A computed that must react when an exact key is published later therefore uses a dependency reactive:

DependencyReactive<T> = Unavailable | Available(T)

DependencyMap<K, T> is the SourceMap<K, DependencyReactive<T>> specialization whose lifecycle is explicit:

• observe_dependency(key) materializes one stable input cell for the exact key, seeded with Unavailable, and observes it. This materializes only the dependency handle; it does not fabricate T or run an expensive value factory.
• publish(key, value) is an ordinary source transition to Available(value). If observation happened first, publication invalidates exactly that key’s consumers. Publishing an unrelated key does not invalidate them.
• unpublish(key) transitions the same source back to Unavailable; it does not remove or re-mint the handle. A later publish reuses the same identity.
• Multiple first observers, including concurrent observers on thread-safe and async flavors, converge on one stored handle without orphan nodes.
• The dependency handle lives until its owning graph scope is torn down. Logical unavailability is a value transition, not disposal.

This API is deliberately separate from observe(key): the existing Core observation remains pure and non-minting. Implementations MUST NOT approximate exact-key availability by observing the whole membership cell, polling/retrying, sleeping, or consulting durable storage. Those mechanisms either invalidate unrelated readers or move live transition authority outside the graph.

Core surface vs. binding extensions

The clauses above are laws. This section says which methods a binding must expose for those laws to be observable, and — just as importantly — which methods are not spec surface at all.

The distinction exists because the family drifted without it. A survey of all nine bindings’ single-threaded maps found method counts from 11 to 32, and the drift splits cleanly in two: methods present in 8 or 9 bindings are laws with a fixture behind them and one binding that never implemented them, while methods present in 7 or fewer are conveniences with no fixture and no law — is_empty is len() == 0, len_untracked is a tracking-discipline escape hatch, reconcile belongs to a higher layer, insert is set under another name. Without this split, “kt is missing seven required methods” and “cs also ships a reconcile helper” are indistinguishable: both read as divergence, and the coverage matrix marks both green.

Core — REQUIRED

A conforming binding MUST expose all of the following, on every flavor it ships (single-threaded, thread-safe, async), spelled in the binding’s own naming convention:

Two Core entries are load-bearing in ways that are easy to miss:

• observe MUST NOT mint. A read that takes a factory and allocates is a different operation with a different contract; it cannot express “is this key absent” and it cannot be called from a reader without a write side effect.
• handle is not optional. Clause 3’s stable handle and clause 4’s “same cell handle” are unassertable without a way to observe entry identity. A map whose entries are plain cached values rather than reactive nodes cannot satisfy this, and MUST be recorded as divergent rather than marked green.

The kind specializations bind per entry kind, not per flavor: set is SourceMap-only on all three flavors, materialize_all is ComputedMap-only on all three. Ordering, by contrast, binds every flavor — it touches no entry handle and awaits nothing, so it is neither thread-coloured nor async-coloured.

Extended — OPTIONAL, non-normative

The following ship in some bindings and are explicitly not spec surface. A binding MAY offer them, MAY name them differently, and MAY omit them entirely; their absence is not a conformance gap and MUST NOT be scored in the coverage matrix.

entry / entry_with (eager value-minting convenience), is_empty, len_untracked, get_or_insert_handle, reconcile, insert, Try*-prefixed naming variants, and any binding-local accessors for the membership/order signals themselves.

Ordered keyed tree

An ordered keyed tree (SourceTree) is a further composition: each node is (stable id, value cell, ordered keyed child collection). It conforms when per-node value reactivity holds (editing a node invalidates only that node’s readers), per-level membership/order reactivity holds (a sibling subtree or descendant change MUST NOT invalidate an unrelated level’s child readers), and child reorder inherits the atomic-move guarantee. The tree is still a composition of cells — not a new cell kind — so per-cell merge applies node-by-node.

This is the runtime substrate for stable keyed/wire addressing of collection entries (see the protocol spec’s node-key addressing) and for keyed reconciliation of document trees (minimal {insert, remove, move, update} ops per item → per-cell CRDT merge).

Keyed reconciliation

Reconciling a level diffs two keyed sequences by stable key, not position, emitting the minimal {insert, remove, move, update} op set. It conforms when reordering is move-minimized (keys already in relative order — the longest-increasing-subsequence over their prior indices — MUST NOT move; only the remainder emit move), and when applied to the reactive collection a stable entry (unchanged value, in the LIS) MUST NOT have its value cell invalidated by a sibling reorder. Applying this minimal op set per-cell is the enabling step for per-cell CRDT merge of a document tree — it replaces whole-subtree replacement with proportional-to-the-diff work.

Memoized semantic tree

The syntactic tree holds input cells; a semantic tree (unresolved prompts, drainable heads, summaries) is a layer of memoized computeds derived from it — one memo slot per node folding (node value, child derived values). It conforms when the derivation is incremental and glitch-free: editing one node recomputes only its ancestor chain (a sibling subtree’s derived value stays cached), and a node edit that does not change the folded result MUST NOT re-run a downstream consumer (memo equality guard). Semantics are derived, not materialized eagerly — cost is proportional to the diff, not the document.

Manufactured identity for text

Markdown has no inherent node ids, so reconciliation keys are manufactured from text in three layers: in-band anchors (exact, survive a body rewrite), content-derived hashes of normalized text (survive reflow/reorder, change on edit), and alignment by similarity (word-LCS ratio) to distinguish an edit (key inherited from the matched predecessor → an update) from a genuine insert. A true rewrite legitimately reads as insert+remove. This is why the controlled skeleton uses in-band markers: stable identity is the linchpin that keeps keyed reconciliation from degrading to whole-document replacement over unstable text.

Free-text CRDT + re-parse

For anchorless prose under concurrent edits the merge unit drops to characters: a Fugue/RGA-style character CRDT (each char an element with a unique id + left origin; deletes tombstoned) whose order is a pure function of the element set, so merge is commutative, associative, idempotent and concurrent same-point inserts converge with both preserved. The structural tree is then a projection of the merged text (re-parse → manufactured-identity keys → reconcile), not the merge unit. Honest floor: a true rewrite is a replace — no character identity survives it. The anchored layer keeps per-node lineage; the free-text layer’s guarantee is “merge the text, re-derive the tree.”

Delta sync (#lztextsync)

Whole-replica merge requires transporting the entire element set; a conformant binding also exposes delta synchronization so replicas converge by exchanging only what a partner lacks. Three operations, over the same element set:

• version_vector() → {peer → counter} — the greatest [OpId] counter this replica holds per originating peer, taken over both insert ids and tombstone (delete) ids. It is the compact frontier a replica publishes; an op (c, p) is unknown to a partner iff c > their_vv[p] (absent peer = 0).
• delta_since(their_vv) → [TextOp] — the ops this replica holds that their_vv has not observed: elements whose insert id is newer, plus elements whose tombstone id is newer (a fresh deletion of an already-shared element). Each TextOp is the transport form of one element — { id, ch, origin, deleted }. A whole-state snapshot is delta_since(∅).
• apply_delta(ops) — applies a delta op list with the same algebra as merge: a new id adds its element (preserving that id); an incoming tombstone is merged sticky-minimally (concurrent deletes keep the smaller delete id); the local Lamport counter advances past every observed id. It is therefore commutative, associative, and idempotent, and re-applying a delta is a no-op.

Identity preservation is the load-bearing property: rebuilding a replica by apply_delta-ing a snapshot onto a fresh buffer keeps every character’s OpId, so a later concurrent edit merges without duplication — unlike re-parsing the text, which would mint fresh ids and double content on the next merge. This is what lets a canonical replica fork per-member replicas from an encoded snapshot and keep them converged by bidirectional delta_since/apply_delta.

The three operations and their convergence/idempotence/identity invariants are pinned by the compute fixture conformance/collections/textcrdt_delta_sync.json (#lztextsync): version-vector shape, bidirectional exchange, whole-snapshot fork identity, and no-op re-apply.

Move-aware sequence order

Sibling order under concurrency is a separate composition above per-cell value merge: a move-aware sequence CRDT (fractional-index positions tiebroken by peer). It conforms when a move is a single LWW reassignment of an element’s position — not delete + reinsert — so two concurrent moves of the same element converge to the later one without duplication, and a concurrent move + value-edit of one element both apply (position and value are independent registers). Removal is an LWW tombstone. This is the order layer beneath keyed reconciliation; it lives only at the multi-writer boundary, leaving the single-producer Snapshot/Delta mirror unchanged.

Forking a replica (#lzzigforkhlcpeer). A fork copies the element set under a new peer identity, and the two halves of its clock are governed separately. The forked replica MUST inherit the source’s causal position — the HLC’s last observed wall time and logical counter — because it has already observed everything the source holds; a fork that restarts its clock at zero mints stamps behind state it already carries the moment its next local op supplies a backwards-skewed now, and since every register adopts only on a strictly greater stamp, that replica’s own write is silently rejected rather than applied. The forked replica MUST NOT inherit the source’s peer id: the peer is the stamp’s final tiebreaker, so two replicas stamping under one id can mint an identical (wall, logical, peer) triple, neither adopts the other, and they diverge permanently. Both halves are pinned by conformance/collections/seqcrdt_convergence.json (fork_carries_the_clock_so_a_backwards_skewed_write_survives, fork_stamps_with_its_own_peer_so_equal_wall_edits_converge). A same-peer copy — clone — inherits both, because it is the same replica continuing rather than a new one.

Tombstone garbage collection

Tombstones (both the sequence-CRDT LWW flag and the character-CRDT sticky delete, which carries the delete’s own id) accumulate without bound — the standard set-CRDT memory-bloat cost. Conformant GC is causal-stability-gated: a tombstone is collectable only once every replica has observed the deletion (the version-vector frontier supplied by the distributed plane, never a single replica’s clock). The sequence layer drops a stable tombstone directly (observationally inert: order/contains already skip it, re-merge re-adopts it as a tombstone, a genuine resurrection wins by LWW). The character layer is conservative: it collects a stable deleted element only when nothing references it as a left origin, so removal never orphans a survivor; interior tombstones are reclaimed bottom-up. Bloat is bounded to the multi-writer plane — the single-producer Snapshot/Delta mirror accrues none.

Scheduling (#lzspecgcdefer). The safety contract fixes which tombstones are collectable; it does not mandate when collection runs. A binding MAY defer GC to idle, batch it under memory pressure, or reclaim incrementally per anti-entropy round, provided no collectable tombstone is re-examined after reclaim and unbounded accrual is surfaced via instrumentation. Deferral changes only memory footprint, never observable values.

Cascade depth is scheduling, not safety (#lzspecgcreferencedtombstone). “Bottom-up” describes the ORDER reclamation is safe in, not how much of it one call must perform. Collecting a leaf can unreference its origin, making that origin collectable in turn; a binding MAY run a single pass and leave the newly-unreferenced tombstone for the next call, or iterate to a fixpoint within one call. The family is split roughly evenly between the two and both conform — the difference is memory footprint at a point in time, which the clause above already places outside the contract. Conformance fixtures therefore assert which tombstones survive a collection, never how many passes it took, and a runner that pinned a cascade count would be encoding one binding’s schedule as a requirement.

What is not optional is the conservative rule itself: a stable tombstone that any surviving element still names as its left origin MUST be kept, or removal orphans a survivor. That half is pinned by conformance/collections/textcrdt_convergence.json (gc_keeps_a_tombstone_that_is_still_a_left_origin) — deleting an INTERIOR character, since a scenario that deletes the last one has no referenced tombstone to keep and so cannot tell a conforming collector from one that ignores origins entirely.

Reactive queues

A reactive queue (QueueCell) is a FIFO collection composed of cells — not a new cell kind — that adds queue semantics (push to tail, pop from head) to the reactive graph. Like the keyed collections above, it adds no new merge unit; each element’s value is an ordinary cell subject to the same single-writer / multi-write classification.

The distinguishing property of a reactive queue is that invalidation is scoped to reader kind, not to individual positions: a push invalidates length/empty/full readers (and the tail signal); a pop invalidates head/length/empty/full readers. The head reader observes the current head value — after a pop, the head reader sees the next element (or empty), not a stale value. There is no random-access queue[N] reader; per-position reactivity is the domain of SourceMap, not QueueCell.

QueueCell — SPSC primitive with MPSC usage rule

QueueCell is specified as a single-producer, single-consumer (SPSC) primitive: one writer owns the tail, one reader owns the head. The producer is the natural FIFO sequencer (push order = delivery order).

MPSC (multi-producer, single-consumer) is a usage rule on the same primitive, not a separate type. Multiple producers push to the same tail inside a batch(); the batch boundary serializes the pushes into a deterministic order. A conforming implementation MUST document the MPSC usage rule and MUST NOT introduce a separate MPSCQueueCell type.

Naming discipline. The cardinality of producers/consumers is not a type parameter. SPSCQueueCell would imply MPSCQueueCell / SPMCQueueCell / MPMCQueueCell siblings — but those shapes differ in semantics (invalidation model, handoff exclusivity), not cardinality. See § Future queue primitives for the genuinely distinct primitives (TopicCell, WorkQueueCell).

The queue family — two axes (semantics defines the primitive)

QueueCell, TopicCell, and WorkQueueCell are one family of reactive cursor-stream cells, separated by two orthogonal axes. Only the first defines the primitive; the second is a usage tier every primitive shares.

Axis 1 — consumer delivery semantics (the primitive axis). Where does each pushed element go?

Axis 2 — topology / ordering (a usage tier, not a type). Producer and consumer counts — fan-in and fan-out — never change which primitive you have; they only set the ordering guarantee and its cost. Opt into exactly the tier you need:

Why not name by cardinality or by fan-in/fan-out. Both are the same mistake — naming a primitive by topology instead of by delivery semantics:

• SP*/MP* mixes two axes: QueueCell already covers SPSC and MPSC (both single-consumer; MPSC is the multi-producer usage). WorkQueueCell and TopicCell are each usable single- or multi-producer, so SPMC/MPMC cannot tell them apart.
• FanOutCell/FanInCell fails identically. Fan-in (many producers → one consumer) is just QueueCell used multi-producer — the ordering tier, not a distinct primitive; a FanInCell collapses back into QueueCell. Fan-out (one → many consumers) is ambiguous between broadcast and competing — TopicCell and WorkQueueCell both fan out, and one FanOutCell name cannot say whether an element goes to all or to one. And fan-in and fan-out are not mutually exclusive (a topic or work queue may be many-producer and many-consumer at once), so they are orthogonal descriptors of wiring, not primitive identities.

So fan-in and fan-out are real and useful — but as the topology axes describing how a primitive is wired, not as names: fan-in = the multi-producer ordering tier (Axis 2); fan-out = multi-consumer, which subdivides into broadcast (TopicCell) vs competing (WorkQueueCell) by Axis 1. A primitive is always named by its Axis-1 delivery semantics, which carries meaning a topology name cannot.

Naming rationale (suffix). The shared family suffix is Cell; Queue appears only where consumption is destructive and exclusive — QueueCell and WorkQueueCell. A TopicCell is a non-destructive broadcast log (reading removes nothing; every subscriber reads every element), so it carries no Queue — TopicQueueCell would conflate the deliberately contrasting messaging terms queue (consumed once) and topic (delivered to all). Parity is the Cell suffix + this family section, not a forced Queue infix.

What multi-producer actually buys (fan-in): a single merged fan-in aggregation stream, one shared backpressure / capacity bound, and — only at the total-order tier — an agreed order. Consensus is the price of agreed total order under partition only, never of multi-producer itself; per-producer FIFO needs no sequencer (it is multiplexed single-producer channels). Full cross-replica retention (every replica holds each item until all consumers ack + compaction) is a replication/HA cost, orthogonal to producer count — a non-replicated queue retains each item once.

Distribution cost differs by primitive (Axis 1 decides it):

¹ A topic is consensus-free only at the per-producer-FIFO tier; total-order broadcast (all subscribers agreeing on one order) is atomic broadcast ≡ consensus — the same cost as an ordered WorkQueueCell. Quorum-intersection safety for WorkQueueCell assignment is proven ReliableSync.majorities_intersect. Detailed semantics follow in § Future queue primitives.

Reactive shell vs storage backend

A QueueCell factors into two layers:

  ┌─────────────────────────────────────────────────────────┐
  │                   Reactive shell                         │
  │  head version cell │ tail version cell │ closed cell     │
  │  len / is_empty / is_full / head — reactive reads       │
  │  invalidation scoped by reader kind                     │
  └────────────────────────┬────────────────────────────────┘
                           │ QueueStorage trait
                           │  try_push(v) → Result<(), Full|Closed>
                           │  try_pop() → Result<T, Empty|Closed>
                           │  len() → usize
                           │  capacity() → Option<usize>
                           │  is_closed() → bool
   ┌───────────────────────┼───────────────────────────────┐
   │                       │                               │
   ▼                       ▼                               ▼
 VecDequeStorage      RaftQueueStorage              KafkaStorage
 (local default)      (embedded consensus;          (external broker;
                       per distributed-queue PRD)    via adapter)

The reactive shell owns the version cells and invalidation logic; it is storage-agnostic and is what the formal model (QueueCell.lean) pins. The reader-kind plane is pinned separately by QueueReaderKinds.lean: the invalidation set is proven to be a function of the transition alone (the bound, the pre-op length, emptiness, and the closed flag) and never of the elements, which is what licenses running the identical rule on all three flavors. It also proves the atomicity requirement above, and — as the queue-family instance of the thread-safe confluence obligation — that invalidation is order-independent and idempotent, because it consults membership in a set rather than a sequence. QueueFamilyReaderKinds.lean carries the same obligation to the other two primitives: the WorkQueueCell rule invalidates a reader kind iff that kind’s value moved (so it neither over- nor under-invalidates) and reads only the before/after counts; a TopicCell publish changes the observed suffix of exactly the connected subscribers; a cursor read depends on that subscriber’s own record alone, which is why the independence law holds structurally rather than by discipline; and safe GC provably changes no reader’s value, which is what licenses gc taking no context on any flavor. The storage backend owns the actual FIFO data structure and is pluggable via the QueueStorage trait (Rust) / concept (C++) / interface (Py/JS/etc.).

An implementation MUST split the shell from the storage. The shell MUST NOT assume a specific storage type (VecDeque, ring buffer, broker client). A binding MAY ship multiple backends; the default MUST be an unbounded VecDeque-backed storage.

Storage backend contract

Minimal required contract. A QueueStorage backend MUST implement exactly try_push / try_pop / len / is_closed / close. peek and capacity are optional capabilities with a default of “absent” (None): a backend that satisfies only the five required methods — a raw channel, a consuming stream, a Go channel — is fully conforming. It simply has no head reader (no peek) and no is_full reader (unbounded, capacity() → None), exactly as an unbounded backend has always had no is_full. A backend that can cheaply inspect its head MAY expose peek to gain a reactive head; a backend that is bounded MUST expose capacity() → Some(n). head was never in the MUST-reactive set (see “Named observables” below), so removing peek from the required contract removes no required reader.

Footnote — LookaheadShim. A caller that wants a head reader over a non-peekable backend MAY opt into a shell-level lookahead shim that prefetches (early-pops) one element into a one-slot buffer. This is SPSC-local only — early-popping is incorrect for competing-consumer or consensus backends, where an element must not be committed to one consumer before assignment. The shim is not part of the core contract.

A conforming backend MUST also satisfy:

1. FIFO order: try_pop returns elements in the order they were try_push-ed. A backend that reorders or silently drops elements is non-conforming.
2. Cardinality compatibility: the backend’s native producer/consumer shape MUST be a superset of the shell’s required shape. (SPSC shell = any backend; MPSC usage requires a backend that accepts multi-writer pushes.)
3. Bounded contract (optional): a bounded backend exposes capacity() → Some(n) and try_push returns Full when at capacity. The overflow policy (block / drop-oldest / drop-newest / reject) is a backend property — the shell’s observable contract only distinguishes Full from Empty/Closed.
4. Position identity: invalidation is phrased over reader kind (head/len/empty/full), not over storage indices. A ring-buffer backend whose slot index wraps MUST NOT cause spurious invalidations; the shell layers its own logical reader-kind derivations above the storage.

Closure and lifecycle

Closure is an observable contract, not a mechanism:

1. try_pop on a closed, non-empty queue returns the next element (drain continues).
2. try_pop on a closed, empty queue returns Closed — a signal distinct from Empty.
3. try_push on a closed queue is an error, regardless of capacity.
4. Close is idempotent (closing an already-closed queue is a no-op) and terminal (once closed, a queue cannot be reopened).

The mechanism (a dedicated closed cell, a flag in storage, a sentinel value) is a binding-level choice. The formal model pins closure as a monotonic flag: Closed_then_stays_Closed.

Bounded queue and reactive backpressure

When the storage backend is bounded (capacity() → Some(n)), the reactive shell exposes is_full as a reactive read. A consumer’s pop that transitions the queue from full to not-full MUST invalidate is_full readers (true → false), enabling push-side effects to react to capacity recovery without polling. This is the backpressure signal: a producer observes is_full and backs off; a consumer’s pop invalidates the producer’s is_full subscription and the producer resumes.

An implementation MUST expose is_full as a reactive cell when the backend is bounded. The unbounded default (capacity() → None) has no is_full reader to invalidate.

Ordering guarantee

A consumer MUST NOT assume total-FIFO across multiple producers. If total order across producers is required, route all pushes through a single producer or use a consensus-backed storage backend (per the distributed-queue PRD).

Wire and snapshot shape

The QueueCell shell’s version cells have no own IPC schema — the head/tail/closed counters are trivial and not independently serialized. A queue reconciles by two complementary wire forms, chosen by plane:

• Snapshot plane → storage-snapshot form. Full queue state is the storage backend’s snapshot form. The reference VecDequeStorage backend serializes as a JSON array (element order = FIFO order) for conformance fixtures; bindings MAY choose a more efficient binary encoding (bincode, postcard) for production. Cross-backend interop (e.g. VecDeque-backed on one peer, RaftQueueStorage on another) requires explicit storage-format agreement; the shell does not mandate a canonical storage snapshot.
• Delta plane → op-log form. Incremental change is the ordered shell op-log — QueuePush / QueuePop / QueueClose — carried in a Delta like any other DeltaOp (protocol.md § QueueCell op-log delta form). These are shell ops (storage-agnostic append/remove-head/close), so they need no storage-format agreement; the op-log is the form reliable-sync fuses under backpressure (a queue cannot state-supersede coalesce — order, multiplicity, and the receiver’s pop position forbid it). The op-log delta form is normative here; a distributed storage backend (per the distributed-queue PRD) remains a separate v1 non-goal.

Distribution

Distribution of a QueueCell is a storage-backend property, not a shell property. A QueueCell is distributable iff its storage backend provides a distributed synchronization mechanism. The shell itself is sync-mechanism-agnostic.

v1 does not specify any distributed backend. The Native Distributed Queue PRD covers the future consensus-based RaftQueueStorage backend (Phase 1+) and the positioning relative to external brokers (Kafka, RabbitMQ, Redis Streams, SQS) via the QueueStorage adapter. CRDT-based distribution is explicitly out of scope for queues — destructive pop requires agreement, not merge (see the PRD’s § “Background: Why Consensus, Not CRDT”).

Threading, permissions, and instrumentation

• Threading contract: QueueCell inherits the Context threading model. MPSC on the same Context uses batch(); cross-thread MPSC requires a ThreadSafeContext-bound flavor; cross-process requires a distributed storage backend.

  This sentence was aspirational prose for the whole v1 line: it named ThreadSafeContext as the way to reach cross-thread MPSC while no binding had a constructor that accepted one, so the only documented path to the guarantee was unimplementable. It is now normative — a thread-safe flavor is Core (see § “Core surface vs. binding extensions (queue family)”) and a binding that ships the family on a single-threaded context only is non-conforming on the other two flavors, not merely unfinished. Recording a capability as absent is fine; documenting a route to it that does not exist is not.

• Permissions: over the distributed plane, push and pop are distinct capabilities under PeerPermissions (distributed.json). A peer MAY be granted push-only, pop-only, or both.

• Atomicity: push and pop are individually atomic. Multi-op transactions (e.g., “enqueue N items then close”) MUST use batch() so a concurrent observer never sees a partial state.

• Instrumentation: a binding SHOULD expose depth / push-count / pop-count metrics via the standard instrumentation surface (parallel to effect_queue_pushes / max_effect_queue_depth).

• Named observables: is_empty and len are reactive reads dual to is_full. All three (is_empty / len / is_full) MUST be reactive when their respective conditions can change.

• Demand-driven derivation (#lzspecdemanddriven): a reader-kind MUST be observable-consistent — a get returns the value consistent with all preceding ops — and a binding SHOULD defer its derivation until it has a subscriber (the measured collapse is ~32× per op — 327 ns → ~10 ns — per docs/relaycell-backpressure-analysis.md §5). A reader-kind is a derived value (a Slot), not an eagerly-written cell; an op with no subscriber to a given reader-kind SHOULD only mark it stale (O(1)) and derive it lazily on the next get, provided the derived value is consistent with all preceding ops. This preserves the observable contract (conformance fixtures read the values and MUST stay green) while an unsubscribed QueueCell collapses toward raw-storage cost — the reactive shell is charged only along a path an effect actually observes. A binding that eagerly derives reader-kinds remains conformant (values stay green by construction) but forgoes the write-cost win. See docs/relaycell-backpressure-analysis.md §5 (demand-driven reader-kinds) and §4.0 (the merge cost law).

Queue family extensions

QueueCell covers SPSC and MPSC. TopicCell is the broadcast member of the family; WorkQueueCell remains the competing-consumer extension. They differ in invalidation model and handoff semantics, not merely producer/consumer cardinality:

TopicCell (broadcast)

A broadcast topic: every subscriber receives every pushed element. Invalidation is “all subscribers,” not “head reader.” Each subscriber holds its own cursor; the topic retains an element until all durable cursors pass it (or a TTL expires). Reading is non-destructive — a subscriber’s advance never removes the element for others.

Relationship to QueueCell: not a multi-consumer queue. A QueueCell consumer destructively pops; a TopicCell subscriber reads by cursor and removes nothing. Different invalidation models in kind.

Normative state and operations

A TopicCell<T> state is the tuple (base_offset, elements, subscriptions):

• base_offset: u64 is the absolute offset of elements[0]; end_offset is base_offset + elements.len.
• elements: [T] is the retained append log in per-producer FIFO order.
• subscriptions: Map<SubscriberId, Subscription> is keyed by stable subscriber identity. Each record contains an absolute cursor (the next offset to read), durability (durable or ephemeral), and connected. Every stored cursor MUST remain in base_offset..=end_offset. An ephemeral record MUST be connected: disconnecting it removes the record instead of persisting an offline ephemeral cursor.

The following operations and observables are required:

• subscribe(id, durable) creates a new cursor at end_offset. Reconnecting an existing durable id MUST reuse its persisted cursor; it MUST NOT silently jump to the tail. Disconnecting an ephemeral subscription removes its record, so a later subscription with that id starts at the then-current tail.
• publish(value) appends exactly one element and leaves every cursor unchanged. Every connected subscriber whose cursor is now behind end_offset is invalidated independently. An offline durable subscriber is not scheduled, but the element remains readable after it reconnects.
• read(id) observes the element at that subscriber’s cursor without changing the log or any cursor. Reads from an unknown or disconnected subscription are unavailable. advance(id) moves only a connected subscription’s cursor by one; it is a no-op for unknown/disconnected subscriptions and at end_offset. Therefore base_offset ≤ cursor ≤ end_offset is preserved by every non-TTL operation, and an offline durable cursor is frozen until reconnect.
• The retention frontier is the minimum cursor across durable subscriptions, or end_offset when there are none. Safe GC removes only offsets below that frontier, advances base_offset, and leaves absolute subscriber cursors unchanged. It MUST preserve every durable subscriber’s future read stream. Ephemeral subscriptions never hold the frontier.
• GC is observational maintenance and invalidates no subscriber when it stays below the frontier. TTL-forced truncation beyond a durable cursor is a separate gap/resync policy and is not part of the v1 semantic core.

The canonical replay fixtures are topiccell_broadcast_cursor_isolation.json, topiccell_durable_replay_gc.json, and topiccell_ephemeral_lifecycle.json, with connected-session boundary behavior pinned by topiccell_offline_tail_bounds.json. The executable universal reference is lazily-formal/LazilyFormal/TopicCell.lean.

Distribution is cheap — no assignment consensus. Every subscriber gets every element, so there is no “who gets this” decision to arbitrate. A distributed topic is N independent per-subscriber cursor-queues — the per-peer DurableOutbox fan-out already pinned for reliable sync. At-least-once fan-out + idempotent apply per subscriber = effectively-once, no quorum. Caveat: this holds only at the per-producer-FIFO tier; total-order broadcast (all subscribers agree on one order) is atomic broadcast ≡ consensus.

Durable vs ephemeral subscriptions. A durable subscription persists its cursor and replays elements missed while offline; an ephemeral subscription sees only elements published while connected (fire-and-forget). Durable subscriptions drive retention.

Backpressure is per-subscriber, and the answer is the state-vs-event split. Each subscriber’s delivery buffer is itself a bounded QueueCell, so a slow subscriber’s is_full fires locally; what happens then is a per-subscription policy, and the right one depends on message semantics — the same dichotomy as outbox coalescing:

• State topic (broadcasting a value) — old elements are worthless once superseded, so a lagging subscriber conflates to latest (drop intermediates, keep the newest): the LWW/last-value coalesce applied to a subscriber. Memory-bounded and effect-lossless — the laggard simply gets current state, and the producer feels nothing.
• Event/log topic (each element a distinct event) — no conflation is possible (order and multiplicity are meaning), so a lagging subscriber resolves overflow one of three ways:
  • Drop (lossy, isolated) — drop-oldest / drop-newest for that subscription; fast subscribers and the producer are unaffected. This is the broadcast default — coupling defeats fan-out.
  • Couple + backpressure (lossless, slowest-paces) — the subscriber withholds ack, retention grows, and the producer throttles to the slowest durable subscriber. Opt-in, for “all-must-receive-losslessly” topics; the operator accepts one slow subscriber pacing the whole topic.
  • Evict (bounded) — on sustained lag past a liveness lease, drop the whole subscription (§ Partition & eviction); it full-resyncs (durable) or resumes from now (ephemeral) on return.

So a TopicCell producer feels backpressure only if a subscription opts into coupling; by default a slow subscriber conflates (state) or drops/evicts (event), and failure is isolated — a dead subscriber grows only its retention, never stalling other subscribers or the producer. This is the opposite of QueueCell, where the single consumer is the backpressure path.

Consumer groups = a topic of work queues. The “Kafka consumer group” shape is a composition, not a fourth primitive: WorkQueueCell semantics within a group (competing) and TopicCell semantics across groups (each group gets the full stream). Model it as a TopicCell whose subscribers are WorkQueueCells.

Status: the local semantic core, conformance fixtures, and Lean proofs ship in v0.31.0. The consensus-backed distributed storage integration remains in the distributed-queue PRD Phase 3.

WorkQueueCell (competing consumers)

A work queue: N consumers compete for elements from a shared FIFO; each element is delivered to exactly one consumer (exclusive handoff).

Why pure CRDT cannot do this. A queue pop is not idempotent-commutative: two consumers concurrently popping the same head both survive a CRDT merge → duplicate delivery, and there is no “un-pop.” Exclusive handoff therefore needs a single serialization point for the assignment decision — a designated leader assigning each element to one consumer, or a consensus-committed assignment log. This is the queue’s CP nature made concrete.

Safety via quorum intersection. With consensus-committed assignment, “element X → consumer W” is a majority-committed log entry. Because any two majorities of an n-voter set intersect in ≥1 voter (ReliableSync.majorities_intersect / majorities_overcount), two conflicting assignments of the same element can never both commit — no double-delivery, ever — and a minority (no quorum) cannot commit an assignment, so it blocks rather than risking a duplicate.

Three populations — do not conflate.

• Workers/consumers — any count; clients of the queue, not voters. Scale freely.
• Replication peers (per-peer outbox) — any count; transport, not voting.
• Voting replicas (order + commit assignments) — want an odd count: 2f+1 replicas tolerate f failures; odd maximizes tolerance-per-node and keeps quorum unambiguous. Make an even data set odd with a witness/arbiter (votes, holds no data).

Partition behavior. Only a partition holding a majority makes progress; the rest block (safe, no double-pop). A 2–2 split of 4 voters gives neither side a majority → both stall (the even-group hazard, fixed by a witness). A 2–2–1 split of 5 voters leaves no side with 3 → all block until partitions heal enough for some side to reach a majority. Odd counts protect two-way splits; they never guarantee a majority under multi-way fragmentation. Halting is correct — safety over liveness.

Delivery & lifecycle (#lzworkqueue):

• Assignment IDs + ack/nack. Each handoff carries a delivery ID; the worker acks (done, remove) or nacks (requeue). Exactly-once commit is the consensus assignment; exactly-once effect needs an idempotent worker or a causal receipt on completion; delivery is at-least-once (redelivery on failure) — so effectively-once = at-least-once + idempotency.
• Visibility-timeout / lease. An assigned-but-unacked element is leased with a TTL; on expiry it reassigns (worker presumed dead) — the per-item analog of the liveness lease.
• Dead-letter queue + poison detection. An element exceeding a max-redelivery count (repeatedly crashing its worker) routes to a DLQ instead of redelivering forever.
• Fairness / dedup. Assignment policy (round-robin, weighted, pull-based) + producer/consumer dedup keys are policy extensions; the portable core uses pull-based FIFO assignment.

Portable local-authority contract. Every binding ships the same in-process WorkQueueCell state machine. The owning instance is the serialization point; hosts MUST serialize calls using the binding’s ordinary context/threading boundary. A local instance does not claim to be a distributed consensus implementation. A cross-process or HA backend MUST put the claim decision behind a leader or consensus-committed assignment log while preserving these operations and outcomes:

• push(value) -> item_id appends a fresh, monotonically increasing item to the pending FIFO.
• claim(worker, now) -> delivery? removes the oldest pending item and creates a fresh, monotonically increasing delivery_id. The returned lease contains the stable item_id, value, worker, 1-based attempt, and deadline = now + visibility_timeout. Empty claim is a no-op.
• ack(worker, delivery_id) -> bool removes only that worker’s matching in-flight delivery. Unknown, stale, or wrong-worker acknowledgements are no-ops. Re-acking is therefore idempotent.
• nack(worker, delivery_id) -> bool validates ownership, then either appends the item to the pending tail or moves it to the dead-letter list when the configured max_deliveries has been reached.
• reap_expired(now) -> count expires leases whose deadline < now (the deadline itself remains live), in ascending delivery-ID order. Each expired item is requeued at the pending tail or dead-lettered under the same attempt limit. A redelivery receives a new delivery ID while keeping its item ID and value.

visibility_timeout is a positive logical-clock duration and max_deliveries >= 1. Requeue-at-tail means retries do not block newer work. The portable reactive reader kinds are pending_len, is_empty (pending only), in_flight_len, and dead_letter_len; a mutation invalidates only readers whose values may have changed, and these reader-kinds SHOULD be demand-driven (#lzspecdemanddriven, see § “Demand-driven derivation” above). The canonical fixtures are conformance/collections/workqueue_competing_delivery.json and workqueue_lease_deadletter.json.

Assignment-FIFO ≠ processing-FIFO. Competing consumers trade ordering for parallelism: even if elements are assigned FIFO, N workers process concurrently, so completion order is unordered. A slow worker holding element 1 does not block element 2 (it routes to another worker) — the point of the primitive — but a consumer MUST NOT assume total processing order. For total order, use one consumer (QueueCell) or route through a single worker.

Pull beats push for balancing. A pull model (workers request when ready) is naturally load-balancing and backpressure-friendly — a fast worker pulls more, a saturated worker stops pulling. A push model needs the assigner to track worker capacity. Pull-based competing consumers are the simpler, self-throttling default.

Backpressure & failure — most resilient of the three. A single slow worker does not fill the queue (its items route to others); the queue backpressures only when all workers are saturated and depth grows. A worker death does not stall the queue — its in-flight (unacked) items reassign on lease expiry; throughput degrades, delivery continues. Opposite of QueueCell, whose single consumer dying stalls until failover.

Status: the portable local-authority state machine, reactive reader kinds, Lean safety model, and cross-language conformance are shipped. Distributed/HA assignment still requires the consensus adapter from the distributed-queue PRD Phase 2; the local shell must not be mistaken for that adapter.

Core surface vs. binding extensions (queue family)

The clauses above are laws. This section says which methods a binding must expose on QueueCell / TopicCell / WorkQueueCell for those laws to be observable, and which methods are not spec surface at all. It mirrors § “Core surface vs. binding extensions” for ReactiveMap, and exists for the same reason: without the split, “this binding ships no ordering on two flavors” and “that binding also ships a convenience helper” both read as divergence and both score green.

The split is drawn from a survey of the bindings that ship the family. When it was first written that was eight, lazily-cs excepted; lazily-cs has since landed the single-threaded family and satisfies every Core entry below, so the survey is now 9 of 9 — unanimous, therefore law — and the rest are conveniences.

Core — REQUIRED

A conforming binding MUST expose all of the following on every flavor it ships (single-threaded, thread-safe, async), spelled in the binding’s own naming convention:

Three Core entries are load-bearing in ways that are easy to miss:

• is_empty is Core here, unlike on ReactiveMap. On the map it is Extended, because it is just len() == 0. For a queue it is a named reactive observable that § “Threading, permissions, and instrumentation” already requires — “is_empty and len are reactive reads dual to is_full; all three MUST be reactive when their respective conditions can change”. The reader-kind independence law is stated over that triple, so dropping one makes the law unassertable.
• A reader kind MUST be reactive, and polling a counter is not reactive. A version counter the caller must poll registers no dependency edge, so no reader can be invalidated by it and the independence law cannot be observed. A binding whose reader kinds are polled counters, or which derives them by diffing a snapshot, MUST be recorded as divergent rather than marked green.
• try_pop MUST distinguish empty from closed. The closure lifecycle law needs Closed to be observably different from Empty; a pop returning a bare optional collapses them.

Ordering-style reasoning applies to the whole family: none of the Core surface touches an entry handle and none of it awaits, so it is neither thread-coloured nor async-coloured and binds every flavor. Confirmed empirically — across all nine bindings the queue-family sources contain no async fn, suspend fun, Future, Task, Promise, or await anywhere. A flavor is not permitted to colour pop.

Which flavors each binding actually ships, and how that is proved

Auditing this table against the nine bindings found it wrong in both directions at once (#lzcoverageaudit), which is worth stating because the two failure modes hide from different reviewers:

• Understated. lazily-go and lazily-cpp ship and replay all three flavors of all three primitives, and lazily-py / lazily-kt / lazily-dart ship and replay the thread-safe and async WorkQueueCell and the async TopicCell. All of it read absent. An understated table is the more dangerous of the two: nobody files a bug about coverage they are told they lack, so a “project this family into the bindings” task reads as unstarted work that is in fact done.
• Overstated. lazily-js was marked as shipping the thread-safe and async QueueCell and the thread-safe TopicCell. It ships none of them — its own flavor ledger records them unshipped and no such type exists in src/.

A mark is only clearable by replay, never by the type existing. Every binding’s suite carries a flavor ledger checked against its own sources in both directions, so a row cannot claim a flavor with no type and a type cannot exist unreplayed; and the replays are fed by a runtime fixture manifest, so “this binary opened these bytes” is observed rather than grepped. lazily-zig is the case that proves the distinction matters: it ships TopicCell and WorkQueueCell and had tests named after the canonical fixtures whose expected values were transcribed into the source, with the fixtures themselves listed as known-uncovered. The types shipped, the corpus did not run, and the honest fix was to add the replay — not to flip the cell.

Reader-kind derivation — one design, pinned

A conforming binding MUST implement reader kinds as memoized derivation with explicit invalidation: each reader kind is a derived node with no graph dependencies, and a successful op clears exactly those whose value provably changed, in one atomic frontier walk.

Three designs were in the field. This one is pinned because:

• it is what § “Demand-driven derivation” already specifies, and the only one that realises its cost win — a version-cell design charges a graph write on every op even with no subscriber, which is precisely what that clause exists to avoid;
• it is the shape the whole family converged on for ReactiveMap, where all nine bindings now hold a graph-agnostic ordering/bookkeeping core beside per-flavor version cells minted on each flavor’s own graph. Forking the queue family onto a different reader-kind design would split the family’s own structure for no gain.

A binding MAY keep a version-cell implementation and remain conformant only if reads still register a dependency edge and the invalidation set is exact; it forgoes the demand-driven win. Polled counters and snapshot diffing are not conformant under any reading.

Per-flavor obligation

A flavor MUST preserve the reader-kind independence law, the closure lifecycle, and the single-frontier-walk atomicity requirement — one op invalidates all of its changed reader kinds together, so a subscriber never observes len bumped while is_full has not yet flipped. On top of that it adds exactly its context-specific guarantee: confluence for thread-safe, eventual transparency for async.

Two flavor questions are settled here rather than left to each binding:

• TopicCell fan-out needs nothing extra under a thread-safe context. Each subscriber owns its cursor and a cursor only advances, so concurrent subscriber reads commute and the retained-until-all-cursors-pass rule is a monotone function of the cursor set. Broadcast is confluent by construction.
• WorkQueueCell lease expiry stays caller-driven on every flavor. reap_expired takes the current time as a parameter; a flavor MUST NOT substitute an owned timer. Time as an input is what makes lease expiry deterministic and fixture-replayable, and an async flavor that grew its own clock would be unreplayable for no gain.

Extended — OPTIONAL, non-normative

The following ship in some bindings and are explicitly not spec surface. A binding MAY offer them, MAY name them differently, and MAY omit them entirely; their absence is not a conformance gap and MUST NOT be scored in the coverage matrix.

push / pop as panicking or asserting variants of try_push / try_pop, peek, elements (whole-buffer snapshot), base_offset, snapshot / from_snapshot, restart, gc as a caller-visible entry point when retention is already automatic, reader_handle accessors for the reader-kind nodes themselves, and any binding-local accessors for the version cells.

RelayCell — Algebra-Backed Backpressure

RelayCell is the algebra-typed conflating relay: a stream transform that sits on an edge, adapts a fast ingress to a bounded/slow egress by an algebra-typed merge, a reactive backpressure policy, and an optional paged durable spill. This chapter is the normative surface of the phased plan in relaycell-backpressure-analysis.md; the merge algebra (Phase 1) is its foundation and the lazily-formal Lean model (LazilyFormal.Merge, LazilyFormal.Relay) is the executable reference for the invariants below.

Status. Phases 1–8 are complete across all eight bindings. The lazily-rs reference implementation and Lean pins validate the API shapes: Phase 1–4 (merge algebra, RelayCell core, SpillStore, Transport — merge.rs, relay.rs, spill.rs, relay_transport.rs), Phase 5 (Inbox/Outbox role facades — relay_roles.rs), Phase 6 (the extra Rate/Window/Expiry/Priority/keyed policies — relay_policy.rs), and Phase 7 (example systems as integration tests — relay_examples.rs). The Phase 6 policies are formally corollaries of the core theorems (window → flush-grouping, priority/sharding → reorder), and every binding exercises the Phase 2–6 behavior in its relay tests.

Invariant above all else (§9). Policy and transport are local mechanism; the converged egress state is independent of binding and mechanism whenever the merge ⊕ is associative. Every RelayCell fixture asserts this, and the Lean relay_converges theorem pins it. Break it — a non-associative merge, or a non-lattice merge on a reordering transport — and portability, determinism, and the formal pin all fail together.

1. Not a new node — a composite (Phase 2)

RelayCell<T, M> is not a new Axis-1 delivery primitive and not a new reactive node category. It decomposes into the reactive family:

• the hot head is a SourceCell<T, M> (write = ⊕ under policy M);
• its reactive reads (depth / bytes / pending_keys / is_full / is_spilling / is_draining / lag) are FormulaCells — demand-driven, so an unobserved relay costs N·⊕ and nothing more (the merge cost law);
• an ingress Effect drives the merge from the transport.

It composes onto QueueCell / TopicCell / WorkQueueCell edges and subsumes today’s scattered backpressure logic: DurableOutbox.coalesce_to_snapshot is a RelayCell<_, CrdtJoin<Lww>> + a SpillStore; per-subscriber TopicCell conflation is a per-sub RelayCell; op-log outbox fusion is a RelayCell<_, RawFifo> + Spill (no conflate).

      ingress          ┌──────────── RelayCell ─────────────┐         egress
 ───(Transport)───────►│ hot head : accumulating merge (⊕)  │───────►(Transport)──►
    ops arrive fast    │ BackpressurePolicy (watermarks)     │  drained on egress
                       │ overflow: Block|Drop|Conflate|Spill │  readiness (credit)
                       │ SpillStore (paged durable tail)     │
                       │ reactive reads: depth/bytes/keys     │
                       └─────────────────────────────────────┘

2. BackpressurePolicy — reactive limits (Phase 2)

Every limit is a reactive cell, so an operator or an adaptive controller retunes it live and every dependent relay reacts:

Hysteresis is required: high_water ≠ low_water so a relay riding the bound does not flap open/closed. An adaptive controller is an ordinary formula cell that observes depth/lag/downstream latency and drives high_water — the control loop is reactive policy driving reactive limits, not a config struct.

3. Overflow actions and policy-flag validation (Phase 2)

The merge algebra, not the relay, decides which overflow is sound. A RelayCell MUST reject an (overflow, transport) pair the policy’s flags forbid, at construction:

A relay MUST additionally reject reordered pages / shards for a non-commutative policy (the reordering tax), and MUST log its overflow action and expose dropped / conflated counters — no silent truncation.

Merge swap (can_reconfigure): M MAY be swapped only when the hot head is empty (changing ⊕ mid-stream changes meaning); the relay exposes can_reconfigure (true iff head empty), and re-validates overflow/transport against the new policy’s flags at swap time.

4. SpillStore — paged durable tail (Phase 3)

SpillStore generalizes DurableOutbox: a hot page in RAM (actively merged) plus immutable cold pages on durable store, a bounded manifest (page_id → location, watermark, bytes), an egress cursor, and ack-before-reclaim. Memory is O(hot page) + O(manifest) for any algebra. Retrieval is pull-metered by egress credit; associativity lets a lagging consumer receive a conflated catch-up. Reconstruction (cold pages in order, then hot head) reproduces the flat fold — paged spill loses nothing (Lean spill_lossless). Crash recovery replays the last unacked page; because a page is one coalesced summary op at the egress, replay is a no-op for an idempotent policy (Lean spill_replay_idempotent) — at-least-once delivery converges.

SpillPolicy (all reactive): page_size; mode = CompactOnWrite (keep-latest, minimizes disk) | AppendCompact (LSM-style, preserves increments for accumulating semilattices); retention = BoundedDisk | UnboundedLog | Ttl; rehydrate = Sequential | Parallel. Parallel rehydrate requires a commutative merge (pages merge out of order).

5. Transport seam (Phase 4)

Transport abstracts ingress/egress delivery so the mechanism is pluggable and per-binding: InProc (direct) | CrossThread (native mpsc or shared ThreadSafeContext) | IpcTransport | WsTransport. RelayCell is written once against Transport; a binding drives it on a goroutine, an async task, or an evented IO interface. The merge algebra — not the transport — guarantees converged state (Lean transport_independent), so transports may differ across bindings and still converge to the same egress.

A channel is a Transport, not a QueueStorage. With peek optional (QueueCell) a native channel satisfies the minimal storage contract directly, but its real role is cross-thread delivery: the idiomatic form is CrossThread, where a worker owns the channel (its mailbox), drains it, and merges into the hot-head SourceCell (the push-fed regime — the pop message carries the value). Crossing a thread boundary requires the thread-safe context.

6. Inbox / Outbox — directional roles (Phase 5)

RelayCell is direction-neutral. Inbox and Outbox are role facades (typed constructors with direction-appropriate defaults), not reimplementations — mirroring “MPSC is a usage of QueueCell, not a subtype”. They earn names because they differ in the backpressure-propagation contract — who you can backpressure and how:

A network link is Outbox → Transport → Inbox, and end-to-end backpressure is a chain of relays: the local producer’s is_full ← Outbox fullness ← (credits / TCP window) ← remote Inbox fullness ← remote app’s consumption. Both ends share one RelayCell core so the signal propagates through the link as one continuous reactive edge. Fan-out reuse: per-subscriber RelayCells wire into TopicCell (the state-vs-event choice becomes a MergePolicy choice); WorkQueueCell stays as-is (competing consumers, no conflate).

7. Extra reactive policies (Phase 6)

Optional reactive stages composed onto the relay egress, each covering a row of the backpressure case matrix:

WindowPolicy and RatePolicy only change where the relay flushes, so the converged state is invariant (relay_converges). PriorityStorage and keyed sharding reorder ops, so they are sound exactly when the policy is commutative.

8. Conformance

A RelayCell implementation conforms when:

1. Composite, not a new node. The relay is built from a SourceCell hot head, demand-driven FormulaCell reads, and an ingress Effect — no new node category.
2. Converged-egress invariance (§9). For an associative M, the egress state after any flush schedule equals the lossless flat fold of the delivered ops. Pinned per-binding by replaying mergecell_algebra.json through a relay and by the Lean relay_converges / transport_independent theorems.
3. Overflow validation. An (overflow, transport) pair the policy’s flags forbid is rejected at construction; Conflate on RawFifo, Drop on a lossless policy, and reordered pages/shards on a non-commutative policy all fail fast. Lossy actions log and increment dropped/conflated counters.
4. Spill losslessness + idempotent replay. Reconstruction from cold pages + hot head reproduces the flat fold; crash-replay of the last unacked page converges (idempotent policy or spill dedup). Lean spill_lossless / spill_replay_idempotent.
5. Reordering tax. A commutative policy is invariant under reordering (priority egress, keyed sharding, out-of-order pages); a non-commutative one preserves arrival order. Lean reorder_adjacent.
6. Reactive policy. BackpressurePolicy/SpillPolicy limits are reactive cells with hysteresis; retuning a limit live re-drives dependent relays.

Verification form. The converged-state and algebra invariants are pinned by the Lean model (LazilyFormal.Relay) and the mergecell_algebra.json compute fixture; per-binding behavior (overflow validation, spill, transport) is exercised by each binding’s relay tests. Concurrency/transport interleaving is not a deterministic replay, so — like the thread-safe context — it is verified by each binding’s model checker / stress harness, not a portable fixture.

State Machine

A state machine is the flat finite-state-machine primitive — a reactive cell holding the current state plus a pure transition function. It is the kernel a single-region State Chart compiles down to, and the Lean formal model in lazily-formal (LazilyFormal/StateMachine.lean) fixes its semantics normatively.

A state machine is compute, not protocol. Like a chart, it is never serialized as a distinct wire kind — only its current state crosses IPC/FFI as an ordinary cell Payload (a CellSet op on the active-state cell). Each binding implements it natively; this chapter fixes the behavior so a machine defined in one language means the same thing in another.

The kernel

The pure transition core is:

Transition : State -> Event -> Option State
Machine    = { current: State, transition: Transition }
send(m, e) = match m.transition(m.current, e) of
             | Some next => { current: next, ... }   // accepted
             | None      => m                         // rejected (guard)

A binding wraps the current State in a reactive cell and exposes send as the mutator. The transition function is pure: given the current state and an event it returns the next state (Some) or rejects the event (None, a guard).

API surface

Semantics

• PartialEq guard (no-op suppression): a transition to an equal state is accepted (send returns true) but does not invalidate dependents — the active-state cell’s equality guard suppresses the no-op update. This is the flat analogue of the chart self-transition rule. To force re-entry, clear the cell’s dependents before send.
• Reactive integration: any formula, driven formula, or effect that reads state_handle() automatically recomputes or reruns on a real transition.
• On-enter / on-exit: model with an effect that has a cleanup closure — the body is on-enter, the returned cleanup is on-exit (runs before the next rerun). on_transition provides a single (old, new) observer instead.
• Batch atomicity: a batch coalesces multiple send calls — effects fire once after the batch settles.
• Deterministic transition function: the transition function MUST be pure and deterministic. send never changes the transition function — a machine is fully described by its transition function and current state.

Proven invariants

The Lean kernel (lazily-formal/LazilyFormal/StateMachine.lean) proves the properties that are easiest to blur across bindings:

• Guard rejection preserves state — a rejected event (None) leaves current unchanged.
• Accepted transitions advance state — an accepted Some(next) sets current = next.
• Self-transitions are no-ops — Some(current) leaves current unchanged and sends returns false.
• Changed transitions send true — Some(next) with next != current reports a real change.
• send preserves the transition function.

Relationship to state charts

A single-region chart refines this send: the chart’s active leaf is the State, the chart event is the Event, and the chart’s walk-up + LCA + descend-initial logic is a pure function returning Some(new_leaf) or None. The confluence/determinism of a single-region chart is inherited from this kernel (see single_region_refines_flat_machine in lazily-formal/LazilyFormal/StateChart.lean). A flat StateMachine is the degenerate chart with no nesting.

Context layers

The flat kernel is context-agnostic. A binding offers it over each reactive context layer it implements, with identical semantics:

• Single-threaded — backed by the single-threaded reactive context.
• Thread-safe — a lock-backed counterpart over the thread-safe context; the transition function and state are Send + Sync, the machine is a clonable handle to the same state cell, and observers fire synchronously within the invalidating send/batch call preserving glitch-free pull-based ordering.
• Async — backed by the async context; send and state stay synchronous (cells are the synchronous input layer), while reactive observers use the async effect/signal APIs and settle on the runtime rather than within send.

Implementation status

The flat machine is required of all bindings that ship a reactive graph. The thread-safe and async counterparts are required of any binding whose platform supports them (see Wire Protocol § Concurrency layers are required); a binding MAY omit one only when it has declared the matching thread_safe / async capability as none. In every case the single-threaded machine and its PartialEq no-op suppression MUST be present wherever a chart is supported (a chart depends on this kernel). lazily-rs, lazily-zig, and lazily-py implement it; the Lean model is the executable reference.

State Charts

A state chart is a Harel/SCXML hierarchical state machine. This chapter specifies the full cross-language subset all lazily bindings implement: compound (nested) states, orthogonal (parallel / AND) regions, history states (shallow and deep), entry/exit/run actions, internal/external transitions, guards, and extended state (context). It also fixes the declarative chart form the conformance fixtures use and how a chart relates to the reactive Cell Model and the flat FSM kernel in the Lean Formal Model.

A state chart is compute, not protocol. It is never serialized over the wire as a distinct kind — only its converged active configuration crosses IPC/FFI as an ordinary cell Payload. Each binding implements the chart natively; this chapter fixes the behavior so a chart defined in one language means the same thing in another (validated by the conformance fixtures).

The declarative chart form is normatively defined by schemas/statechart.json (JSON Schema, Draft 2020-12). The prose below fixes its semantics.

Why a chart reduces to existing machinery

The Lean kernel (formal/lean/LazilyFormal/StateMachine.lean) defines a pure transition State → Event → Option State. A single-region chart compiles to exactly this kernel: the chart’s active leaf is the State, the event is the Event, and the chart’s transition logic (walk-up + LCA + descend-initial) is a pure function returning Some(new_leaf) or None.

Orthogonal regions generalize State from a single leaf to an active configuration (a set of leaves, one per region). The transition is still a pure Configuration → Event → Option Configuration: enabled transitions, conflict resolution, and exit/enter-set computation are all deterministic functions of the chart definition and the current configuration. Because of this, a chart cell is single-writer by the Cell Model rules — it is either a direct cell (reactive bindings) or a derived cell keyed off event cells. It is therefore never multi-write: replicas converge on the event stream, and each replica’s chart recomputes deterministically. No merge: mechanism is defined or needed for charts.

Reactive vs. projection bindings

A chart is never exposed over FFI. Every binding implements the transition as pure logic with zero system dependencies; routing it through JNA/koffi to a Rust Context would be circular (the only thing FFI buys a consumer is an authoritative projection, which a local chart is not).

Declarative chart form

Conformance fixtures and cross-language chart definitions use a flat id map. States form a tree via parent. The full form:

{
  "initial": "<state-id>",
  "context"?: { … },
  "states": {
    "<id>": {
      "parent"?: "<id>",
      "kind"?: "atomic" | "compound" | "parallel" | "history" | "final",
      "initial"?: "<child-id>",          // compound only
      "parallel"?: true,                  // AND-state: children are concurrent regions
      "history"?: "shallow" | "deep",     // history pseudo-state
      "default"?: "<target-id>",          // history: resume target before any recording
      "on"?: { "<event>": <transition>, … },
      "entry"?: [<action>, …],
      "exit"?:  [<action>, …],
      "run"?:    [<action>, …]
    }
  }
}

kind is optional and inferred: history when history is set; parallel when parallel is true; compound when the state has children; otherwise atomic. When kind is present it is authoritative, not an annotation: it MUST be one of the five values above and MUST agree with the structural fields and child relation. final is the only kind that cannot be inferred; it MUST have no children, initial, parallel, or history. A contradictory or unknown declared kind makes the entire chart malformed.

Every id-valued reference MUST name a state declared in the same states map before the chart can execute. This includes parent, compound initial, history default, transition target, and the chart-level initial. Implementations MUST reject an unresolved reference while building the chart; they MUST NOT infer an undeclared id as an atomic leaf or allow it into the active configuration.

A <transition> is a bare target-id string (shorthand for {"target": id}) or an object:

{ "target": "<id>", "guard"?: <guard>, "action"?: [<action>], "internal"?: false }

Structural rules

• Exactly one state has no parent — the root.
• A compound state (one with children) MUST declare initial, which MUST resolve to a leaf by descending compound initials.
• A parallel state MUST NOT declare initial; its children are the concurrent regions, and all of them are active whenever the parallel state is.
• A history state MUST NOT declare initial or parallel; it MUST declare history and SHOULD declare default. Its parent is the region whose configuration it records.
• An atomic state has no children, no initial, and no parallel.
• A final state signals completion of its parent region (see Completion).

Active configuration

The active configuration is the set of states that are currently active:

• A state is active if any of its children is active (compound), or all of its region children are active (parallel), or it is an active leaf.
• For a single-region chart, the configuration is the path root → active leaf and contains exactly one leaf.
• For a chart with parallel regions, the configuration contains one leaf per region plus all their ancestors (including the parallel state itself).

The set of active leaves is the subset of atomic active states.

Transition selection

send(event) runs run-to-completion: it computes the next configuration from the current one with no interleaving of external events.

1. Enabled transitions

For each active leaf, walk up its ancestor chain. At each ancestor, collect every transition whose on[event] matches event and whose guard passes. A guard passes when it is absent, resolves true (see Guards), or — for a context-expression guard — evaluates true against context. A single event may enable transitions in more than one region (parallel charts fire concurrently).

2. Conflict resolution

Two enabled transitions conflict if their exit sets (computed next) intersect — i.e. one would exit a state the other needs. Resolve conflicts by:

1. If one transition’s source is a descendant of the other’s source, keep the descendant (innermost wins).
2. Otherwise keep the one that appears first in document order (the order states and their on entries are declared).

The surviving set is taken atomically.

3. Exit and enter sets

For each taken transition with source s and target t:

• lca = the lowest state that is an ancestor of both the active leaf in s’s region and t. (For a transition internal to one parallel region, the lca stays inside that region and the sibling regions are untouched.)
• Exit set = active states strictly below lca, restricted to s’s region subtree.
• Enter set = the path lca → t, then:
  • if t is compound, descend via initial to a leaf;
  • if t is parallel, enter every region child and descend each;
  • if entering a region whose recorded history exists, descend via the recorded configuration instead of initial (see History);
  • if t is a history state, resume its parent region per its recorded configuration (or default if none).

The total exit set is the union over taken transitions; the total enter set is the union, plus any parallel siblings forced active by entering a parallel state. Exit actions run innermost-first (reverse document order within the exit set); then transition actions run; then entry actions run outermost-first (document order within the enter set).

Internal vs external. A transition with internal: true whose target is the source or a descendant of it does not exit/re-enter the source — only its action runs and descendants below the target are reconfigured. The default is external (exit/re-enter the source).

4. Apply

The new configuration is the old one minus the total exit set plus the total enter set. If no transition was enabled, the event is rejected: return false, state unchanged.

Single-region specialization

With no parallel regions the algorithm collapses to the SCXML single-region rule: walk up from the one active leaf, take the first passing transition, and compute exit/enter through the lca. lca makes sibling-substate transitions (e.g. a.x → a.y) cheap (exit only x, enter y) and cross-subtree transitions (a.x → b.y) correct (exit a.x…, enter b.y…).

Queries

• active() → the active leaf id. Defined for single-region charts; for charts with parallel regions it is undefined (use configuration()).
• configuration() → the full set of active state ids (leaves plus all active ancestors).
• activeLeaves() → the set of active atomic state ids (one per region).
• matches(id) → true iff id is in configuration() (the hierarchical “state-in” predicate).

History

A history pseudo-state records its parent region’s active configuration whenever that region is exited, and resumes it when the region is re-entered by a transition targeting the history state.

• Shallow ("history": "shallow"): records/restores the direct child of the parent region that was active. Nested configuration below that child is re-derived from the child’s own initial.
• Deep ("history": "deep"): records/restores the full nested leaf configuration of the parent region, across all descendant compound and parallel levels.
• First entry: when a region with a history child has never been exited (no recording), a transition targeting the history state enters default instead. default SHOULD be declared; if absent, the region’s initial is used.

A region records history on every exit, including exits caused by a transition that leaves the region without targeting its history, so a later re-entry via history resumes the most recent configuration.

Actions

Actions are host-resolved side effects, never part of the configuration. A binding accepts an action handler name → effect; for conformance replay, each step asserts the ordered trace of action names that fired.

• entry — fired when the state enters, after its ancestors’ entries.
• exit — fired when the state exits, before its ancestors’ exits.
• run — ongoing (do) actions: started on entry, cancelled on exit. Host-managed; not part of conformance replay.
• transition action — fired after the exit set and before the enter set.

Order, restated: exit actions (innermost-first) → transition action → entry actions (outermost-first), per the exit/enter set computation.

Guards

A transition may name a guard. A guard is either:

• a bare string — a named guard resolved by the caller’s guard resolver (name → bool); when no resolver is supplied or the name is unknown it is treated as false (fail-closed); or
• an object {"expr": "…"} — an extended-state expression the host evaluates against context.

Guards are pure predicates over caller-supplied state, never over the chart’s own configuration. For conformance replay, each step supplies its guard outcomes explicitly by name, so every binding reproduces identical behavior without shipping a guard evaluator.

Extended state

context is optional host-resolved caller state over which context-expression guards evaluate. It is never serialized as part of the active configuration; it lives outside the chart. A binding that supports context exposes it to guard expressions and transition/entry actions; a binding that does not MUST reject charts that use {"expr": …} guards explicitly rather than silently treating them as passing.

Completion

A final state marks its parent region complete. When every region of a parallel state reaches a final child, the parallel state itself is complete and a completion (done) event is raised for the parent. This is the SCXML automatic transition on completion. (Bindings MAY defer final/completion to a later revision, but MUST reject final explicitly if unsupported.)

Reactive binding

In reactive bindings the active configuration lives in a Cell. On send(event) the pure transition produces a new configuration; the cell’s != (PartialEq) guard suppresses downstream invalidation when the configuration is unchanged (e.g. a no-op self-transition or a parallel-region transition that doesn’t change the leaf set). Any Slot / Signal / subscriber reading active(), configuration(), or matches() is invalidated on a real transition.

Context-layer variants (non-normative)

A binding MAY expose the chart over each concurrency layer its context stack supports, exactly as it does for the flat StateMachine — one chart type per context layer, sharing a single context-free transition engine so the Harel semantics (and hence conformance) are identical across layers. lazily-rs ships StateChart (single-threaded Context), ThreadSafeStateChart (ThreadSafeContext), and AsyncStateChart (AsyncContext); lazily-kt ships StateChart + ThreadSafeStateChart (it has no async state machine); projection-only bindings without a reactive graph (lazily-js) expose a single plain-Set chart with no thread-safe/async variant. Which layers exist is a binding property; the transition function they compute is the same one this spec fixes.

Typed builder (non-normative)

fromChart (the declarative JSON form above) is the normative, conformance- tested definition path. A binding MAY additionally offer a typed native builder that constructs the same ChartDef — e.g. lazily-rs ChartBuilder, lazily-kt ChartBuilder, lazily-js ChartBuilder. A chart assembled by the builder MUST be behaviourally identical to the same chart parsed from JSON (both derive the children / root / depth structure through one shared assembly step); the builder is a source-ergonomic convenience, not a distinct semantics.

Self-transitions

A transition whose resulting configuration equals the current one is a no-op: accepted (true) but the cell’s PartialEq guard suppresses downstream invalidation, identical to the flat StateMachine self-transition rule. (For an external self-transition that must re-run entry/exit, the configuration object is still replaced; whether that invalidates dependents is the binding’s documented choice — conformance asserts the action trace, not invalidation counts.)

Conformance fixtures

Canonical charts live in conformance/statechart/. Each binding loads them, asserts initial_active (and initial_actions when present), replays the steps, and asserts accepted, active, matches, and (when present) actions after each step. For parallel charts active is an array of active leaves (sorted); for single-region charts it is a single leaf id.

Fixture schema

{
  "description": "…",
  "kind": "StateChart",
  "initial_active": "leaf" | ["leaf", …],
  "initial_actions"?: ["action", …],
  "chart": { …per schemas/statechart.json… },
  "steps": [
    {
      "event": "START",
      "guards"?: { "name": true },
      "accepted": true,
      "active": "leaf" | ["leaf", …],
      "matches"?: { "state-id": true },
      "actions"?: ["action", …]
    }
  ]
}

• initial_active — expected active leaf (or leaves for parallel) after descending chart.initial, asserted once before any step.
• initial_actions (optional) — ordered action names fired during initial entry.
• event — the event sent.
• guards (optional) — per-step named guard outcomes for this send.
• accepted — expected send return value.
• active — expected active leaf (single) or active-leaf set (parallel) after the step.
• matches (optional) — { state-id: bool } expectations for matches().
• actions (optional) — ordered action names fired during the step (exit → transition → entry).

Current fixtures:

Implementation status

The single-region subset (compound states, walk-up resolution, LCA, guards, self-transitions) is required of all bindings. Orthogonal regions, history, actions, and extended state are specified here in full; a binding MAY implement a subset, but MUST reject any feature it does not implement explicitly (never silently ignore a parallel, history, entry/exit/run, or {"expr": …} guard). Each binding’s conformance run selects the fixtures that match its implemented subset.

Async Reactive Context

An async context is a separate reactive surface for computations whose values are produced by async/future-returning functions. It is not an overload of the synchronous or thread-safe context; it is a distinct graph with its own handles, because futures introduce in-flight state, cancellation, stale completion, and dependency tracking across suspension points that the synchronous graph does not have.

This chapter fixes the cross-language contract. An async context is compute, not protocol — only resolved slot values cross IPC/FFI as ordinary cell payloads, exactly like the synchronous graph.

Why a separate surface

A synchronous reactive context tracks dependencies through a thread-local stack touched on every read, and a slot’s value is either present or unset. An async computation can be in-flight (suspended at an .await) when its inputs change, can complete after those inputs are gone, and can be canceled mid-flight. Those states require:

• an explicit per-slot state machine (not just present/absent),
• revision tracking so a stale completion is discarded,
• dependency edges registered before the read is awaited, and
• a cancellation contract that is safe under waiter drop, supersession, and context disposal.

A binding gates this surface behind a separate feature flag so downstream users do not accidentally accept the larger semantic surface.

Handles

An async context exposes its own copyable, id-only handles, distinct from the synchronous handles:

Handles are id-only and copyable; they are usable only with the owning async context.

AsyncSource and AsyncComputed are the canonical public value kinds in every binding. Published pre-v2 spellings such as AsyncCellHandle and AsyncSlotHandle may remain only as deprecated aliases of those exact types. Constructing through an old spelling must still return the canonical type.

API surface

Sources are the synchronous input layer: source, get, and set are synchronous. Only computed evaluation and effects are async. The constructor and read/write vocabulary is deliberately the same as the local and thread-safe contexts; only the async handle types and get_async are execution-model-specific.

The public state projection is AsyncComputedState. The formal theorem/module name remains AsyncSlotState, because it describes the storage state machine, not a public value-handle kind. Bindings with a published AsyncSlotState API keep it as a deprecated alias of AsyncComputedState; formal references are not renamed mechanically.

Async computed state machine (formal AsyncSlotState)

Each async slot tracks its state through a finite state machine:

            first get_async /         future Ok,          dependency
   Empty ──────────────────► Computing ──────► Resolved ──────► Computing
     ▲         (spawn)        │    │                              │
     │                         │    │ future Err                   │
     │                         │    ▼                              │
     │                         │  Error ──────────────────────────┘
     │                         │   retry get_async
     │                         ▼
     │      dependency invalidation      revision mismatch on
     └──── during in-flight compute ──► (stale) Computing ──► complete discards;
      hard clear                                                new future spawned

Revision tracking is load-bearing: a computation records the slot revision at start; at publish time the graph accepts the value only if the revision is still current. This is what makes stale completion safe.

Transitions:

• Empty → Computing — first get_async or invalidation with no cached value.
• Computing → Resolved — future completes Ok and the recorded revision still matches.
• Computing → Error — future completes Err and the recorded revision still matches.
• Computing → Computing (stale) — invalidation advances the slot revision during an in-flight computation. The completing future finds its revision no longer matches and discards the result; a new future is spawned for the updated revision.
• Resolved → Computing — invalidation marks the cached value stale and spawns a new computation.
• Error → Computing — get_async retry after an error. This transition is mandatory, not optional: a slot in Error holds no cached result, so the next read re-spawns for the current revision. A binding that replays the stored error to every later reader is non-conforming — it makes a transient failure (a timed-out fetch, a disconnected peer) permanent for the lifetime of the slot, with no read path that can recover it. invalidate on an Error slot is therefore a no-op rather than a repair: the retry is owned by the read, not by a dependency change. The executable form is LazilyFormal.AsyncSlotState.step … SlotEvent.retry, which maps error → computing and is a no-op from every other state.

Cancellation contract

A conforming async context MUST honor all five of:

1. Waiter cancellation is safe. Dropping one get_async future does not cancel the shared in-flight computation while other waiters still need it. Each waiter holds a shared handle; dropping a receiver does not abort the in-flight task.

2. Stale completion is discarded, not published. When invalidation advances the slot revision during an in-flight computation, the completing future finds its recorded revision no longer matches and discards the result. Waiting callers are retried against the new revision or attached to the newly spawned future.

3. Explicit cancellation. A hard clear, invalidation, or context disposal may mark the in-flight revision as canceled; if an abort handle is available, the task is aborted. User futures MUST be cancellation-safe, because aborting drops them at an .await boundary.

4. Context disposal. Dropping the async context cancels all in-flight computations via their abort handles and awaits completion of all active cleanup futures before returning.

5. Effect cleanup is triggered by rerun or dispose, and completes before the next body. An effect’s cleanup future MUST run only when the effect reruns or is disposed — the trigger fixed by reactive-graph.md § Conformance (“cleanup runs before each rerun and on dispose”) — and when it runs on a rerun it MUST complete before the next body starts. Disposal removes pending reruns before awaiting cleanup.

   A binding MUST NOT run cleanup at the end of the flush that ran the body. This clause previously stated only the ordering (“cleanup completes before the next body starts”) and left the trigger to reactive-graph.md, which turned out to be enough rope: lazily-py’s async effect awaited cleanup at flush end whenever no rerun was queued, and satisfied the ordering vacuously because there was no next body to be ordered against. Found 2026-07-19 by disarm_disposes_nothing, which asserts cleanup_order: [] at a step where nothing was disposed or invalidated, and observed a cleanup.

   The reason the trigger matters rather than just the ordering: the canonical effect acquires a resource in the body and releases it in the cleanup. Running cleanup at flush end releases the resource while the effect is still live and will rerun later — an effect that subscribes and returns an unsubscribe would unsubscribe itself immediately. lazily-go and lazily-dart both retain the cleanup between runs and execute it at the start of the next one; that is the family behavior.

get_async re-resolve contract

get_async MUST treat the slot state as authoritative and re-resolve rather than assert, because the slot can change between its lock acquisitions and a notifier can close under it. It runs an outer loop that, each pass, re-reads the slot via the get() fast path and then re-locks to attach to or spawn a computation. Two concurrency windows are benign (not data inconsistencies — the published value is always correct):

1. Resolved-since-get(): the slot can transition Computing → Resolved between the fast-path get() (which releases the lock) and the re-lock. Observing Resolved at the re-lock is expected; the cached value is read directly. It is not an unreachable state.
2. Notifier dropped: the per-computation waiters can all close without a final Resolved signal when an in-flight compute is superseded by a newer revision (the stale Computing → Computing transition early-returns) or the slot is invalidated. A “the world changed” error means re-resolve from current slot state — return the now-published value, attach to the new in-flight compute, or respawn. It MUST NOT panic.

Dependency tracking

Async compute and effect callbacks do not use a thread-local tracking stack (a thread-local does not survive executor thread migration or suspension/resume across .await). Instead each callback receives a compute context:

Edges register immediately, so source invalidation while the future is suspended can cancel or supersede the in-flight computation before it publishes stale data. On rerun, stale dependencies are removed and new ones registered; the dependency set is carried by the compute context, not a thread-local.

Async effects

An async effect runs an effect body returning an optional async cleanup:

• Serialized reruns: reruns are serialized per effect — a rerun does not start until the previous cleanup future completes.
• Cleanup trigger and ordering: cleanup runs on rerun or dispose and at no other time — not at the end of the flush that ran the body. When it runs on a rerun, the previous run’s cleanup completes before the next body starts; disposal awaits the current cleanup before removing the node. The cleanup is therefore retained between runs rather than executed eagerly. See § “Conformance” item 5 for why the trigger is normative and not merely the ordering.
• Auto-tracking: the body receives a compute context and tracks dependencies through get_async / get.
• Scheduled, not inline: dependency invalidation schedules an async rerun after the current invalidation pass; the rerun runs on the runtime executor, not inline within send/batch.
• Disposal: removes pending scheduled reruns, awaits the current cleanup future, and unsubscribes dependency edges.

Batch support

batch(run) is a synchronous boundary. Cell updates queue invalidation roots; at batch exit, queued roots trigger propagation. Async slots and effects are scheduled for rerun but do not execute inside the batch callback — async reruns execute after the batch returns, on the runtime executor. Mutation semantics stay synchronous at the graph boundary: invalidations schedule async reruns only after the outermost batch exits.

In-flight deduplication & fast path

• One in-flight computation per revision: each async slot has one published cache and at most one in-flight computation for the current revision. Concurrent get_async callers await the same in-flight result instead of spawning duplicate futures.
• Synchronous fast path: get() returns the cached value synchronously when the slot is Resolved, avoiding async overhead. get_async() calls get() first; only unresolved or dirty slots enter the async spawn path.

Async state machine

A flat State Machine over the async context keeps send and state synchronous (sources are the synchronous input layer) while reactive observers use the async APIs: on_transition returns an async effect handle and state_is returns an async signal handle. Because resolution is asynchronous, eager recomputation settles on the runtime rather than synchronously within send.

Conformance

An async context conforms when:

1. The slot state machine (Empty/Computing/Resolved/Error) and its transitions, including the stale Computing → Computing discard, are implemented exactly.
2. Revision tracking discards every stale completion; a stale value is never published.
3. All five cancellation properties hold, and disposal awaits cleanup.
4. get_async re-resolves through both benign-race windows without panicking.
5. Dependencies are tracked through the compute context (not a thread-local) and registered before the awaited read.
6. Async effect reruns are serialized, cleanup-before-body ordered, and executor-scheduled rather than inline.
7. Batching is synchronous at the mutation boundary; async reruns fire only after the outermost batch exits.

Implementation status

The async surface is required of any binding whose platform exposes an async/future runtime (async/await, promises, coroutines, a suspending executor) — see Wire Protocol § Concurrency layers are required. A binding on a platform with no notion of suspendable async computation declares the async capability as none and advertises it, never silently. A binding that ships the async context MUST honor the full cancellation and re-resolve contract above. API-shape checks for the canonical async-v2 names are informational only: they do not admit a peer to transport, CRDT, queue, or sync feature groups. Network-suite membership continues to follow the binding’s advertised production capabilities, channels, codecs, and variants. Concurrency-window coverage is pinned by targeted deterministic tests rather than exhaustive interleaving exploration, because the async resolve loop runs on a real async executor whose primitives a synchronization-model checker cannot shim.

Lossless Tree CRDT

LosslessTreeCrdt is a single rooted concrete-syntax tree whose leaves own every rendered byte, so the tree itself is the lossless wire authority — no separate flat text CRDT floor is required for capable sessions. The defining invariant is losslessness:

render(tree) == source_text

for valid, invalid, and unknown source alike. This chapter specifies the M1 syntax-agnostic core: the tree state model, node/op id formats, the leaf and element node variants, the dotted non-contiguous version frontier, the op vocabulary, the byte-offset policy, and the compute-fixture contract every binding replays. The Lean model of the render algebra, convergence, and frontier soundness lives in lazily-formal (LazilyFormal.LosslessTree, LazilyFormal.LosslessTreeSync).

M1 scope. Create / tombstone / intra-parent reorder / leaf-edit / split-leaf / merge-adjacent-leaves, plus op-based delta sync, plus the op-delta wire schema (see Wire schemas). Deferred to later milestones: cross-parent move (single-parent + acyclicity enforcement), metadata/kind mutation, subtree replace, snapshot/GC and its wire schema, and full SessionHandshake capability negotiation (the capability name is reserved below). The Kotlin and JS bindings land in M2. In the create-only + intra-parent-reorder algebra, single-parent and acyclicity hold by construction.

Tree state model

The document is one rooted tree. Every node has a stable identity and belongs to exactly one parent’s ordered child list.

• DocumentRoot — the sentinel root element (TreeNodeId {counter: 0, peer: 0}).
• ElementNode — an internal semantic node with a kind and an ordered list of children. Owns structure only, never text.
• Leaf — owns one exact source span, classified by a LeafKind:
  • Token — a syntax delimiter or marker;
  • Trivia — whitespace, blank lines, indentation, comments, separators;
  • Raw — valid text the adapter deliberately keeps opaque;
  • Error — invalid or ambiguous text that must still round-trip exactly.

render is a depth-first concatenation of the live leaves’ text in child order. Because every rendered byte belongs to exactly one live leaf and elements own no text, unknown or invalid spans round-trip exactly as Raw/Error leaves rather than being discarded — the requirement that keeps a semantic AST from being mistaken for a lossless tree.

Identity and clock

• TreeOpId {counter, peer} — a dotted operation id: a Lamport counter tiebroken by peer, totally ordered by (counter, peer). The counter advances past every observed op, so a causally-later write wins last-writer-wins and concurrent ops tiebreak deterministically by peer. (No HLC is needed; tree anti-entropy is op-based.)
• TreeNodeId — a node’s identity is the id of the op that created it, so a node keeps its id through reorder, edit, and (future) move.
• SortKey {frac, peer} — a fractional-index child position: orderable bytes tiebroken by the minting peer, so concurrent inserts into the same gap get a deterministic total order. Positions travel inside create/reorder ops, so both replicas store byte-identical keys.

Operation vocabulary

Every mutation is one op carrying everything a remote replica needs to converge deterministically (positions and seed text travel inside the op):

Split and merge reseed a leaf’s text destructively, so per-leaf text ops form a causal chain: each LeafEdit/SplitLeaf/MergeLeaves carries the prior text-op id (prev) and is buffered until it arrives, keeping out-of-order delivery convergent.

Dotted version frontier

The frontier summarizing “which ops do I hold” is a dot set — per peer, a contiguous prefix plus out-of-order holes — never a per-peer max counter:

frontier[peer] = { contiguous, sparse: {…} }

diff(their_frontier) returns the ops a replica holds that the partner’s frontier lacks (a true set difference over dots), ordered by dotted id. apply_update is idempotent (already-held ops are skipped) and buffers ops whose parent/target or prev has not arrived yet.

A per-peer max would record only the highest delivered dot and imply every lower dot is held; delivering dot 3 while dot 2 is missing would make the partner believe it holds 2, so its diff would omit an op it genuinely lacks and the replicas would never converge. The dot set keeps the hole representable and re-requestable. This is proven in LazilyFormal.LosslessTreeSync (frontier_no_skip, perPeerMax_skips) and exercised by the non_contiguous_anti_entropy fixture.

Offset policy

Wire and API text offsets are UTF-8 byte offsets, leaf-local. The embedded text CRDT is char-indexed, so the byte→char conversion happens only at the two byte-taking mutators (edit_leaf, split_leaf), against that leaf’s current text. Offsets must land on a UTF-8 char boundary and within the leaf, else the mutation is rejected. No binding may treat UTF-16 code units as wire offsets; the Kotlin/JS bindings (later milestones) must convert.

Conformance

The M1 fixtures live in conformance/lossless-tree/ as compute fixtures — each builds an initial tree on replica a, runs a schedule of ops / forks / anti-entropy syncs across named replicas, and asserts exact rendered text, live-node counts, and convergence across delivery orders:

• exact_roundtrip — Token/Trivia/Raw/Error leaves incl. an invalid span and multi-byte text; render == source;
• one_leaf_edit_delta — a one-leaf edit at a byte offset into multi-byte text, delivered by anti-entropy;
• split_merge — split then merge, render preserved, live-node count grows then restores;
• concurrent_insert_same_parent — two replicas insert into the same gap; both survive, deterministic order;
• concurrent_reorder_and_leaf_edit — a concurrent move + text edit both apply;
• non_contiguous_anti_entropy — a delivery hole is re-requested and converges;
• token_trivia_preservation — a leaf edit leaves adjacent Token/Trivia leaves byte-for-byte unchanged;
• invalid_source_roundtrip — unclosed fence / comment carried as Error leaves round-trips exactly, and editing an adjacent Raw leaf keeps the Error spans;
• concurrent_conflict_preserves_text — incompatible concurrent shapes (element wrap vs bare leaf) both survive with no bytes dropped (text preservation wins over semantic shape; adapter-level raw/error degradation layers above the core);
• apply_update_advances_counter — the counter advance above, observed: a replica reorders AFTER syncing in six remote reorders, and its new op must outrank the stamp it just ingested. The failure is symmetric (both replicas converge on the wrong text), so render_on is what sees it, not converged;
• out_of_order_delivery_buffers — a three-op batch delivered in reversed order (deliver.order) must drain through the dependency buffer; a binding that drops what it cannot yet apply still records the dot, so the following full sync returns nothing and the loss is permanent.

See Conformance Fixtures for the fixture format and the binding replay contract.

Wire schemas

The op-delta wire form is pinned by two JSON Schemas, derived from the lazily-rs reference’s serde output (which is the normative form):

• schemas/lossless-tree.json — the shared vocabulary $defs: OpId, SortKey (frac is a u8 array, never base64), LeafKind (PascalCase on the wire), NodeSeed, TextOp, the externally-tagged TreeOpKind / TreeOp, and the dotted TreeVersionFrontier / DotRange.
• schemas/lossless-tree-delta.json — the TreeUpdate message: { "ops": [TreeOp, …] }, the output of diff and the input to apply_update.

The reference validates its own TreeUpdate and frontier serde output against these schemas (lazily-rs/tests/lossless_tree_schema.rs), and the M2 Kotlin/JS ports validate their emitted frames against the same files. The snapshot/checkpoint wire schema is deferred with snapshot/GC.

Capability

A binding that implements this chapter advertises the capability name lossless_tree_crdt_v1 (reserved here; wired into SessionHandshake capability negotiation in a later milestone). A peer that lacks it falls back to the flat text CRDT floor.

CrdtTree Contract (#lzcrdttree)

CrdtTree is the shared lossless document-CRDT seam used by snapshots, relay canonicals, and document-op replication. An implementation exposes:

• version_vector() — a compact distributed frontier;
• delta_since(frontier) — every operation the frontier has not observed;
• apply_delta(delta) — an identity-preserving, idempotent fold;
• text() / value() — the visible lossless projection; and
• merge_from(other) — the state join.

The join and delta fold are commutative, associative, and idempotent. A full snapshot is exactly delta_since(empty_frontier); applying it to an empty replica must preserve operation identities, not reparse the visible text and mint a new lineage. Applying delta_since(version_vector()) is a no-op.

The compute fixture at conformance/crdt-tree/algebra.json pins merge order independence, idempotence, snapshot equivalence, and incremental round-trip behavior. The Lean model in LazilyFormal.Replication pins the three join laws.

Durable Outbox Stores (#lzdurableoutbox)

Reliable sync separates protocol from persistence:

OutboxStore (ordered byte CRUD) → Outbox<S> (ack/prune/replay protocol) → SyncDriver

OutboxStore owns only put, delete_through, scan_after, load_cursor, and save_cursor. Outbox<S> owns serialization and the invariants:

1. append before send;
2. retain every frame until the peer acknowledges its epoch;
3. keep the acknowledgment cursor monotone, including when a stale storage handle writes after a newer handle;
4. prune only epochs at or below that cursor; and
5. replay epochs above the cursor in ascending order after restart.

Persistent save_cursor(epoch) implementations MUST serialize max(stored_cursor, epoch) atomically. A process-local maximum is insufficient: two handles can both open at cursor zero, then write 9 and 3 in that order. The serialized result must remain 9, and a subsequent protocol read must observe 9.

Bindings may provide platform stores without duplicating this protocol. Rust ships InMemoryStore and feature-gated SqliteStore; Kotlin ships a SQLite/Room-shaped store; browser JS ships IndexedDbStore; other native bindings ship append-only file journals. SQLite is never a default/WASM feature.

conformance/reliable-sync/outbox_store_protocol.json pins the storage-independent behavior. LazilyFormal.Replication proves cursor monotonicity and that replay never contains a pruned epoch.

An append-only journal is a versioned durable wire surface: a later process, and possibly a different build of the same binding, reads records written earlier. Readers MUST reject a complete record whose opcode they do not recognize. They MUST NOT skip it as though it were a cursor marker, because an ignored pruning operation can resurrect acknowledged frames and redeliver them while reporting a successful scan.

The sole recovery exception is a torn trailing record. A crash may interrupt the last append, so a reader MUST forgive one incomplete final record and preserve every complete record before it. The same malformed bytes in an interior record are corruption and MUST be rejected. The logical, encoding-neutral cases are pinned by conformance/reliable-sync/outbox_journal_decode.json; bindings encode them into their native JSON-lines or binary journal format before replay.

Durable Effect Sinks (#lzdurablesink)

Lazily fixes one direction of authority between live reactive state and durable storage:

cold durable state ──hydrate once──▶ live Lazily state
                                      │
                                      ▼
                          computed projection or ordered fact stream
                                      │
                                      ▼
                              Effect / AsyncEffect
                                      │
                                      ▼
                             write-only durable sink
                                      │
                                ack / failure
                                      └────────▶ live Lazily state

Invariant. While a Lazily runtime is live, transitions are decided from Lazily state. Durable storage receives a projection or an ordered fact as an effect. A sink MUST NOT reload storage and use it to arbitrate the transition it is currently persisting.

This makes durable storage an effect sink. It does not claim that every effect is durable, nor that durable storage is always eventually consistent. Lazily is not a database framework: applications continue to own serialization, transactions, schema migration, storage selection, and startup recovery. Lazily ships no SQLite, filesystem, or cloud-store adapter as part of this decision — the sink is an application-owned trait (see examples below).

Authority rule

• Live coordination, compare-and-swap, ownership, deduplication, leases, and transition selection happen in Lazily state.
• Durable I/O runs from an Effect / AsyncEffect, or from a TopicCell / DurableOutbox drain when history must be lossless.
• A runtime sink is write-only with respect to transition authority. Loading and migration belong to a separate startup hydrator that runs once before the runtime is live, not on the decision seam.
• Computed values and transition reducers stay pure — a reducer MUST NOT perform I/O or read storage to decide a transition.
• Success advances a monotone acknowledgement such as durable_through(epoch).
• Failure stays represented in live state as pending / retrying / backpressured. It MUST NOT trigger a database reload at the decision seam.
• Values on the existing Ephemeral plane MUST NOT enter a durable sink. Reuse the existing Durable marker — do not invent a second marker hierarchy. (The Ephemeral-never-Durable separation is already pinned by Presence.ephemeral_never_durable.)

Projection vs history — pick the shape before the API

Ordinary Effect / AsyncEffect observe settled reactive state. Lazily already coalesces effect reruns across a batch, so a batch containing A → B → C may persist only C. That is correct for a durable projection (current/recoverable state). Durable history has a different contract: every accepted fact must survive and remain ordered. It uses the existing TopicCell / DurableOutbox family — stable cursor, replay, idempotency key, and monotone acknowledgement — not ordinary effects. Do not modify ordinary effects to retain intermediate values; that would weaken their coalescing semantics and duplicate the ordered-stream primitives.

Before choosing an API, answer two questions:

1. Is this sink persisting the latest projection or an ordered history?
2. Must the transition be durable before it is externally visible?

Those two answers fix the shape:

Application-owned sink trait

The sink is a narrow, write-only trait owned by the application. The reactive graph holds no reference to a query/hydration interface — those live in a separate module used only by the startup hydrator, never passed into the runtime effect. (Phase 3 adds architecture tests that fail if a hot-path actor module imports the persistence query/CAS or file-lock modules.)

The two examples below sketch the trait shape in Rust-flavoured pseudocode. The store API is deliberately minimal — upsert_latest for a projection, append_fact for history — and always carries the epoch so success can advance a monotone durable_through.

Example 1 — coalesced current-state projection

A Computed projects the actor’s current state. An Effect reads it and upserts only the settled value; intermediate batch values are coalesced away by Lazily’s existing effect-batch dedup, so the sink sees one write per batch. Acknowledgement advances durable_through; a sink failure flips the live actor to retrying without reloading storage.

#![allow(unused)]
fn main() {
// Application-owned, write-only. No read/CAS surface reaches the runtime effect.
trait ProjectionSink {
    fn upsert_latest(&mut self, epoch: u64, state: &ActorState) -> Result<(), SinkErr>;
}

// Live state. Pure reducer; no I/O.
let live_state: Source<ActorState> = ctx.source(initial);
let epoch:     Source<u64>         = ctx.source(0);
let projected: Computed<ActorState> = ctx.computed(|c| c.get(live_state).clone());

// Durable I/O runs from an Effect — never reads storage to decide a transition.
ctx.effect(|c| {
    let s = c.get(projected);
    let e = c.get(epoch);
    match sink.upsert_latest(e, s) {
        Ok(())  => c.set(durable_through, e),            // monotone ack
        Err(_)  => c.set(status, Status::Retrying),      // failure stays live
    }
});
}

Example 2 — lossless ordered fact sink

Every accepted fact must survive and stay ordered, so the source is a TopicCell (or the existing DurableOutbox), drained by an effect into the application store. Replay from a stable cursor covers every epoch after the durable frontier; duplicate delivery is idempotent by the event_id key. This is the DurableOutbox append-before-send / replay-from-cursor / ack_through contract, applied as a sink.

#![allow(unused)]
fn main() {
trait HistorySink {
    fn append_fact(&mut self, epoch: u64, fact: &Fact) -> Result<(), SinkErr>;
    fn ack_through(&mut self, epoch: u64);
}

let facts: TopicCell<Fact> = ctx.topic();
// Drain: every unacked fact is appended in order; ack advances the cursor.
ctx.effect(|c| {
    while let Some(fact) = facts.read_after(cursor) {
        sink.append_fact(fact.epoch, &fact)?;
        sink.ack_through(fact.epoch);          // cursor advances; GC-safe below it
        cursor = fact.epoch;
    }
});
}

Visibility policy (caller-chosen)

A caller picks an explicit policy per transition; Lazily mandates none:

• eventual_projection — live state is immediately authoritative; the sink persists in the background and may lag.
• durable_before_applied — external visibility waits for the durable_through(epoch) acknowledgement before the transition is observed as applied (an ordered fact plus an application acknowledgement cell).
• ephemeral — no durable sink; the value lives on the Ephemeral plane.

Cold restart

Restart recovery is the hydrator’s job, run once at startup before the runtime is live: load the last acknowledged projection (or replay the ordered fact log up to the durable cursor) into live state, then resume. After hydration, authority is live-only — a sink failure during a live transition never rolls authority backward by rehydrating storage at the decision seam.

Formal backstop

lazily-formal/LazilyFormal/DurableSink.lean pins the load-bearing invariants: durable_through is monotone; a batched projection persists only the settled epoch (coalescing); an ordered history replays every epoch past the durable cursor; and a sink failure leaves live authority unchanged (no rehydrate-at- decision-seam). The Ephemeral-never-Durable separation is already proven in Presence.ephemeral_never_durable.

Transport-agnostic reactive egress (#lzegress)

Egress is the send-side mirror of reactive ingress. The pure EgressCore<T> owns delivery authority:

• monotone sequence assignment;
• the pending queue and bounded unacknowledged window;
• the monotone cumulative acknowledgement watermark;
• retry attempts, bounded exponential backoff, and exhaustion; and
• the producer-generation fence.

The graph shells expose that state as Computeds. Transport I/O lives in exactly one Effect per attachment:

EgressCore<T>                 sequence, window, watermark, retry, fence
├── EgressCell<T>             Context shell
├── ThreadSafeEgressCell<T>   ThreadSafeContext shell
└── AsyncEgressCell<T>        AsyncContext shell
          │
          └── one attached Effect ──send──▶ transport

An Effect is not an egress family by itself: it has no retained delivery state. The Effect observes the pending and inflight projections, asks the core to claim eligible envelopes, and sends those envelopes. The core decides whether a claim, acknowledgement, failure, retry, or reconnect is admissible.

This is reactive projection, not a request/ACK protocol. Enqueue invalidates pending; claiming moves an envelope to inflight; an acknowledgement invalidates inflight and re-runs the same attachment when it reopens a bounded send window. The acknowledgement is domain delivery input to the core, not an acknowledgement of a projection request.

Envelope identity and ordering

Each enqueue assigns the next sequence in the current sequence space:

enqueue(payload) =
  pending.push({ generation, sequence: next_sequence, attempt: 0, payload })
  next_sequence += 1

(generation, sequence) is the transport idempotency identity. Pending records are claimed oldest-sequence first. A successful claim increments attempt and moves the record into the unacknowledged window. A claim is refused when that window reaches inflight_limit.

An acknowledgement is cumulative. ack(generation, through) advances acked_through only when through is greater than the current watermark, and removes all pending, in-flight, or retry-parked records at or below it.

Send-side generation fence

Every transport Effect captures the generation current when it attaches. Every send-side transition supplies that generation to the core. A mismatched generation is rejected without changing state or invalidating a reader.

reconnect(new_generation) must strictly advance the generation. It:

1. fences the old Effect;
2. preserves next_sequence and acked_through;
3. moves every unacknowledged in-flight or retry-parked record back to pending in sequence order; and
4. rewrites all pending envelopes to the new generation.

The old Effect remains attached but inert. The replacement transport receives one new Effect, which replays the retained pending projection under the new incarnation.

Retry

retry_budget counts retries after the first send attempt. A failed in-flight record is parked until the derived backoff elapses:

backoff(attempt) =
  min(retry_ceiling, retry_base * 2^(attempt - 1))

While budget remains, retry_now returns the parked record to pending in sequence order. Once exhausted, the record is terminal and cannot be scheduled again. Parking is explicit so a failed send cannot cause the attachment Effect to spin in an immediate reactive retry loop.

Reader kinds and invalidation

No-op and stale-generation transitions invalidate nothing. The async shell uses synchronous Computeds for the delivery state; only the transport attachment is async-coloured.

Composition boundaries

Egress does not duplicate existing storage or flow-control primitives:

• use RelayCell / Outbox ahead of enqueue for conflation and backpressure;
• use SpillStore for overflow-to-storage;
• use DurableOutbox for durable recovery; and
• use transport framing outside the core.

Those adapters feed or persist the egress state machine. They do not move sequence assignment, acknowledgement authority, or the generation fence into an Effect.

Conformance and formal obligations

The canonical corpus in conformance/egress/ covers ordered cumulative ACK, window reopening, bounded retry, and reconnect fencing. Binding runners must assert both returned outcomes and the full projected state after every step.

The Lean model proves:

• sequence assignment is monotone;
• acknowledgement progress is monotone;
• stale-generation send-side transitions preserve state;
• reconnect strictly advances generation while preserving the ACK watermark; and
• permitted retry attempts are bounded by the configured budget.

Cross-Language Feature Coverage

This is the canonical feature-coverage matrix for the lazily family. Each binding’s README reproduces it; this page is the source of truth. It is a status view (what each port ships today), distinct from the normative Binding Conformance Matrix, which fixes what every binding must eventually provide.

Legend: ✅ shipped · ~ partial · — absent · ⊘ not applicable (see notes).

The table below is generated from coverage.json by scripts/sync-coverage.mjs. Edit coverage.json and run make coverage-sync (or node scripts/sync-coverage.mjs) to update this table and every binding README in one shot; make coverage-check guards drift in CI.

Summary — family × language

Roll-up rule: a family cell is ✅ only when every required row in that family is ✅; ~ when the family is mixed (some shipped or partial); — when no required row is shipped or partial; ⊘ only when every required row in the family is not applicable. Rows the spec marks MAY (optional, shown as opt below) are excluded from the roll-up — declining an optional feature is not a gap.

Reactive graph

Materialization

Family sync

Statecharts

Keyed collections

Reactive queue

Broadcast topic

Work queue

CRDT data types

Lossless tree

Egress

Ingress

Wire codec

Transport & FFI

Message passing

Reliable sync

Distributed plane

Causal receipts

Security boundary

Membership

Coordination

Presence

Temporal

Rate shaping

Windowing

Resilience

Portable stdlib

Service plane

Instrumentation

Convergence and the wire protocol are pinned by the shared conformance fixtures and JSON Schemas in this repo and the Lean models in lazily-formal.

Notes

• ᵃ Python reactive graph: Cell / Slot / Signal / Effect (sync) and the top-level batch(run) boundary ship; the != PartialEq memo guard applies to cells, slots, and signals. The async counterpart (AsyncEffect) queues reruns at the batch boundary for asyncio reactors.
• ᵇ Dart reactive graph: Context / Slot / Cell / Signal ship; there is no standalone Effect type (observers subscribe on cells) and batch is scoped to the async context.
• ᶜ Zig reactive graph: Cell / Slot / Signal / Effect and the public batch(run) boundary ship (context.zig coalesces the eager-recompute drain at the outermost batch exit).
• ᵈ Serialized context (JS / Dart) — decision: both are meaningful as serialized, realm-local execution flavors, not as shared-graph contexts. They are scored when their own surfaces replay the portable Core fixtures, and are excluded from cross-thread shared-graph stress/model-check tests. A duplicate wrapper is not sufficient by itself: unsupported Core features remain staged, and runner-local locks/dictionaries cannot stand in for them. Either binding may remove the flavor and declare it absent; while it advertises the flavor, it must join every feature peer group it actually supports. See protocol.md § Concurrency layers are required for the conditional layer requirement and reactive-graph.md § Declared context capabilities for the serialized / shared-graph distinction.
• ᵉ Zig async context: Zig removed language async and has no suspendable executor, so the layer is a task-queue + settle() drain surface — the synchronous graph’s pending_recompute/drainPendingRecompute generalized with revision tracking and the 4-state slot machine (async_context.zig).
• ᶠ Zig collections: SourceMap / ComputedMap with atomic move, SourceTree (per-level membership/order reactivity, atomic child move), and the LIS-move-minimized reconcile op-set all ship (collection.zig, cell_tree.zig, reconcile.zig).
• ᵍ Shared-memory blob path (JS / Dart): carry ShmBlobRef wire references but no host-side ShmBlobArena — the I/O-channel fallback of the shared-memory carve-out (see protocol.md § Shared-memory payload path is required).
• ʰ Dart distributed CRDT plane: the CrdtPlane engine (HLC / stamp frontier / stability watermark) ships, but is not yet wired to live merge: crdt root cells.
• ⁱ C-ABI FFI (JS): platform carve-out ffi = none — browser/Worker JS has no shared in-process C ABI. The full state plane (including CrdtSync) still flows over IPC / WebSocket / WebRTC (see protocol.md § C-ABI FFI is required).
• Distributed plane — WebRTC transport + signaling (Rust / Kotlin / JS / Zig): the portable stack (signaling protocol + client, the DataChannel seam, permission- filtering sink/source, in-memory loopback, and the CRDT plane runtime) ships and is conformance-tested; the concrete native WebRTC backend is a platform adapter (str0m in Rust; the browser RTCPeerConnection in JS; a consumer-provided seam in Kotlin and Zig), matching the reference design where the heavy transport is optional behind the seam.

1. Reactive graph — two cell kinds (nodes SourceCell / ComputedCell; handles Source<T, M> / Computed<T>) + Effect sink + eager Computed (computed().eager()) / all cells guarded / batch ↩

2. Thread-safe context (lock-backed) ↩

3. Async reactive context ↩

4. Merge algebra + Source<T, M> — associative MergePolicy (KeepLatest/Sum/Max/SetUnion/RawFifo), Cell ≡ Source<KeepLatest>, read-any-cell/write-Source split (#relaycell) ↩

5. Keyed-map materialization (ComputedMap) — mint-on-access derived slots: transparency + deferral (#lzmatmode) ↩

6. Thread-safe keyed map (ThreadSafeComputedMap) — Send + Sync + materialization confluence (#lzmatmode) ↩

7. Async keyed map (AsyncComputedMap) — eventual transparency (#lzmatmode) ↩

8. Keyed-map sync — membership propagation + materialize-on-ingest + derived-aggregate transparency (#lzfamilysync) ↩

9. Flat state machine ↩

10. Harel state charts ↩

11. Keyed reactive maps (ReactiveMap: SourceMap / ComputedMap) + SourceTree + reconcile ↩

12. ReactiveMap Core surface — single-threaded flavor (cell-model.md § Core surface vs. binding extensions) ↩

13. ReactiveMap Core surface — thread-safe flavor (ordering + membership reactivity) ↩

14. ReactiveMap Core surface — async flavor (ordering + membership reactivity) ↩

15. Exact-key dependency availability (DependencyMap: observe before publish, unrelated-key isolation, stable identity; #lzdependencyavailability) ↩

16. Atomic ordered move replayed against all three flavors (cellmap_atomic_move + cellmap_independence) ↩

17. Memoized semantic tree (SemTree) ↩

18. Stable-id alignment (manufactured identity) ↩

19. Reactive queue (QueueCell SPSC/MPSC + QueueStorage adapter) Core surface — single-threaded flavor ↩

20. Reactive queue (QueueCell SPSC/MPSC + QueueStorage adapter) Core surface — thread-safe flavor (reader kinds + closure lifecycle) ↩

21. Reactive queue (QueueCell SPSC/MPSC + QueueStorage adapter) Core surface — async flavor (reader kinds + eventual transparency) ↩

22. Broadcast topic (TopicCell) Core surface — single-threaded flavor — independent cursors + durable replay + safe GC (#lztopiccell) ↩

23. Broadcast topic (TopicCell) Core surface — thread-safe flavor (reader kinds + closure lifecycle) ↩

24. Broadcast topic (TopicCell) Core surface — async flavor (reader kinds + eventual transparency) ↩

25. Competing-consumer work queue (WorkQueueCell) Core surface — single-threaded flavor — exclusive leases + ack/nack + redelivery + DLQ (#lzworkqueue) ↩

26. Competing-consumer work queue (WorkQueueCell) Core surface — thread-safe flavor (reader kinds + closure lifecycle) ↩

27. Competing-consumer work queue (WorkQueueCell) Core surface — async flavor (reader kinds + eventual transparency) ↩

28. Free-text character CRDT (TextCrdt) ↩

29. TextCrdt delta sync (version_vector / delta_since / apply_delta) ↩

30. CrdtTree lossless document contract (#lzcrdttree) ↩

31. Move-aware sequence CRDT (SeqCrdt) ↩

32. Registers (LWW / MV) + PnCounter + CellCrdt ↩

33. Lossless tree CRDT core (LosslessTreeCrdt, M1) ↩

34. Lossless tree — dotted-frontier anti-entropy ↩

35. Lossless tree — concurrent merge convergence ↩

36. Transport-agnostic reactive egress (EgressCore) — monotone sequence assignment, bounded unacknowledged window, cumulative ACK watermark, bounded retry/backoff/exhaustion, producer-generation fence (#lzegress) ↩

37. Egress family — Send + Sync flavor (ThreadSafeEgressCell): delivery authority stays in the shared core, one attached transport Effect per incarnation (#lzegress) ↩

38. Egress family — async flavor (AsyncEgressCell): the delivery-state readers stay synchronous Computeds; only the transport attachment is async-coloured (#lzegress) ↩

39. RelayCell — conflating relay + BackpressurePolicy + SpillStore + Transport + Inbox/Outbox + Rate/Window/Expiry/Priority/keyed policies (#relaycell) ↩

40. Transport-agnostic reactive ingress (IngressCell) — keyed lifecycle scopes, generation/sequence/freshness envelopes, reorder buffer, accepted/dropped/error receipt readers (#designimplementtransport) ↩

41. Ingress family — Send + Sync flavor (ThreadSafeIngressCell): one frontier walk per admission (#designimplementtransport) ↩

42. Ingress family — async flavor (AsyncIngressCell): admission is not async-coloured (#designimplementtransport) ↩

43. Boundary-ingress adapter (BoundaryIngressAdapter) — the non-reactive/reactive seam ahead of IngressCell: one monotone channel cursor per producer generation, snapshot-plus-event bootstrap applied as one batch, derived ReplayRequired(from) on a cursor gap, generation fence + hot resubscribe (#designimplementtransport) ↩

44. IPC wire — Snapshot + Delta + CrdtSync ↩

45. Frame codec — json reference codec: dependency-free interop floor, FFI baseline form, byte-canonical (MUST) — executable round-trip obligation (conformance/codec/frame_roundtrip_json.json, #lzmsgpackparity) ↩

46. Frame codec — msgpack cross-language binary default: externally-tagged frame over named-field maps, semantic (not byte-identical) round-trip (MUST) — executable round-trip obligation (conformance/codec/frame_roundtrip_msgpack.json, #lzmsgpackparity). Shipping a MessagePack codec does not earn this mark: lazily-cpp read ~ here while its private internally-tagged framing wore the token, and only flipped once it shipped the spec wire (#lzcppmsgpackwire) ↩

47. Frame codec — postcard positional same-schema fast path: smallest + byte-canonical, not cross-language (MAY) ↩

48. NodeId / PeerId exact-representation bound (MUST) — a decoder that cannot represent a received identifier exactly rejects the frame rather than rounding it (conformance/codec/nodeid_exact_range.json, #lzspecdecoderbound). A binding’s exact range MAY be narrower than the u64 wire type; ✅ means it refuses outside that range instead of substituting a neighbouring id, not that it carries the full u64. Exact ranges: full u64 in Rust / Zig / C#, unbounded in Python, [0, 2^63) in Kotlin / Go / C++, [0, 2^53) in JS, and platform-split in Dart (63-bit on the VM, 53-bit on web). protocol.md stated only the PRODUCER half until this audit, and two C++ decoders were substituting rather than refusing. ↩

49. NodeKey null-leniency on decode (MUST) — omit-when-absent binds the ENCODER; a decoder reads both an omitted key and an explicit key: null as absent, refusing neither and constructing a key from neither (conformance/codec/nodekey_null_leniency.json, #lzkeynullstrict). Replayed on BOTH optional-key sites (NodeSnapshot, the NodeAdd delta op) in both codecs, and the fixture pins the RE-ENCODED field set as well: reading null as absent and writing it back out is a correct decode with a non-conforming encoder. Before the audit lazily-py and lazily-zig refused the null form, and lazily-kt decoded it into a real key named null — all three had the same field right on CrdtOp, in the same file. ↩

50. Capability negotiation (SessionHandshake) ↩

51. Shared-memory blob path (ShmBlobArena) ↩

52. Cross-process zero-copy transport (BlobBackend / shm / arrow) ↩

53. C-ABI FFI boundary ↩

54. Message-passing + RPC command plane (command-plane-v1) ↩

55. Reliable sync — resync coordinator + at-least-once durable outbox + OR-set/LWW liveness (#lzsync) ↩

56. Storage-independent durable outbox (OutboxStore + shared outbox protocol; SQLite/Room/IndexedDB/file adapters) ↩

57. Reliable-sync transport seam + full-duplex SyncDriver loop (IpcSink/IpcSource, #sync-driver) ↩

58. Distributed CRDT plane (CrdtPlaneRuntime / anti-entropy) ↩

59. Distributed plane — WebRTC transport + signaling ↩

60. State projection / mirror ↩

61. Causal receipts (CausalReceipts outcome projection) ↩

62. Permission boundary (PeerPermissions / RemoteOp) ↩

63. Membership + failure detection — MembershipCell (SWIM + Phi-accrual) / PeerSet / PeerChangeEvent (#lzmemb) ↩

64. Distributed coordination — LeaseCell / LeaderCell / LockCell / SemaphoreCell / BarrierCell+QuorumCell (#lzcoord) ↩

65. Presence + ephemeral plane — PresenceCell / AwarenessCell / EphemeralCell + Ephemeral/Durable markers (#lzpresence) ↩

66. Temporal sources — TimerCell / IntervalCell / CronCell / DeadlineCell over a logical clock (#lztime) ↩

67. Rate-shaping operators — DebounceCell / ThrottleCell / SampleCell / ProbabilisticSampleCell (#lzrateshape) ↩

68. Stream windowing — TumblingWindow / SlidingWindow / SessionWindow over the merge algebra (#lzwindow) ↩

69. Fault tolerance — CircuitBreakerCell / RetryPolicyCell / BulkheadCell / TimeoutCell (#lzresilience) ↩

70. Portable stdlib Timer (stdlib_timer_v1) — canonical fixture + mutation-gate verified ↩

71. Portable stdlib caller-driven Timeout<T> (stdlib_timeout_v1) — distinct from reactive TimeoutCell ↩

72. Portable stdlib RevisionBarrier (stdlib_revision_barrier_v1) — register/recheck lost-wakeup guard ↩

73. Embedded-service plane — HealthCell / ReadinessCell / DiscoveryCell / ServiceRegistry (#lzservice) ↩

74. Instrumentation / benchmarks ↩