lazily Wire Protocol Specification

Normative source of truth for all lazily language bindings.

Shared Types

NodeId / PeerId

NodeId = u64
PeerId = u64

Wire-stable identifiers decoupled from internal SlotId. Serialized as bare JSON numbers.

Producer bound. A peer whose runtime represents integers as IEEE-754 doubles MUST keep emitted NodeId/PeerId values at or below 2^53 − 1 (Number.MAX_SAFE_INTEGER). The constraint is the runtime’s numeric representation, not the source language: it binds every JavaScript target — which includes Dart, Kotlin, and TypeScript compiled to JavaScript — and does not bind a Dart or Kotlin peer running on the VM/JVM. Earlier wording named “JavaScript/TypeScript peers”, which read as a source-language rule and left compiled-to-JS peers apparently exempt.

Decoder obligation — refuse, never round (#lzspecdecoderbound). A decoder that cannot represent a received NodeId/PeerId exactly MUST reject the frame. It MUST NOT round, truncate, saturate, wrap, or otherwise substitute a nearby representable value. Rounding is the worst available behaviour: the frame decodes cleanly, the identifier now addresses a different node, and nothing downstream can detect the substitution — whereas a rejected frame is a visible protocol error a peer recovers from by resync (§ Resync / gap handling). The producer bound keeps a conforming producer from ever provoking this; the decoder clause is what makes a non-conforming producer, or a corrupted frame, fail loudly instead of silently. The bound stated only the producer half until #lzspecdecoderbound, and the receiving half is exactly where bindings diverged.

A binding’s exact range MAY be narrower than u64. The wire type stays u64; a binding whose identity type is narrower is interoperable over the sub-range it represents and satisfies the clause by failing the decode outside it — it is not required to widen. Audited ranges:

Only lazily-js and lazily-dart carried the rule deliberately; the other seven inherited it from a parser that happens to fail closed, which is a property no test held in place — and two of them did not hold it. lazily-cpp’s msgpack reader cast a uint 64 straight to int64_t, so u64::MAX decoded as -1: a well-formed identifier for a different node, with no error anywhere. Its json parser refused the same value, but by letting std::stoll throw std::out_of_range, which is a std::logic_error and therefore escaped the std::runtime_error every caller guards a decode with. Both are fixed; the fixture is what found them. conformance/codec/nodeid_exact_range.json makes the clause executable in both json and msgpack form. Its wire frames are carried as raw text (json) and hex bytes (msgpack), and the expected identifier as a decimal string, because a runner that parsed the fixture as JSON on a double runtime would round the expected value before it ever compared anything. The 2^53 − 1 scenarios are exact — every binding MUST decode them to that value, which is what stops a runner that rejects everything from passing vacuously; 2^53 + 1 and u64::MAX are exact_or_reject. A decoder that yields a different number fails.

NodeKey

NodeKey = string   // a "/"-joined path, e.g. "scores/alice", "outer/k1/inner/k2"

An optional, wire-stable keyed address for a collection entry (a SourceMap / ComputedMap entry). Unlike NodeId — the volatile internal handle a producer may re-mint after a resync or remove-then-readd — a NodeKey is producer-defined and stable across NodeId churn, so a peer can subscribe to “entry scores/alice” without an out-of-band key→NodeId map. A multi-segment path addresses nested collections (an entry of a SourceMap inside a SourceMap entry) with no extra machinery.

NodeKey is additive — it never changes NodeId semantics. It appears only as the optional key field on NodeSnapshot and the NodeAdd delta op.

Bounds (reject on construction and on the wire): path ≤ 1024 bytes; ≤ 32 /-separated segments; empty path and empty segments (leading/trailing/double /) are rejected.

Serialization is format-aware. Self-describing codecs (JSON, MessagePack) omit the key field when absent, so pre-key encoders/decoders and existing conformance fixtures round-trip unchanged; positional Postcard always carries the optional discriminant for binary schema stability. Cross-language implementations (lazily-py, lazily-zig, lazily-js, lazily-kt, lazily-go) add the optional nullable key field; they need not emit it when no key is set. Multi-producer key uniqueness (last-writer rule) is owned by the distributed CRDT plane, not this protocol.

Omit-when-absent binds the ENCODER; the decoder is lenient (#lzkeynullstrict). A conforming encoder omits key when there is no key. A decoder MUST accept both the omitted field and an explicit key: null, and read both as absent — it MUST NOT refuse the null form, and MUST NOT construct a key from it. This was previously stated only as “a decoder that sees no key field treats it as absent”, which settled the omitted form and left the null form undefined; three bindings then diverged. The null form is not hypothetical: a serde-based peer that simply did not apply skip_serializing_if emits it, rmp_serde’s own decoder reads it back as absent, and a decoder that refuses is stricter than the reference implementation on a frame the reference implementation produces.

Note the asymmetry that makes this easy to get wrong. CrdtOp.key is always written, null when unset, because an anti-entropy op’s addressing is part of its merge identity (§ Anti-entropy wire format) — so every decoder is already obliged to read key: null as absent one field over. Every binding that got NodeSnapshot/NodeAdd wrong had CrdtOp right, in the same file.

Audited (#lzkeynullstrict) — the field appears on NodeSnapshot and on the NodeAdd delta op:

All three are fixed. lazily-kt’s is the reason the clause says MUST NOT construct a key from it rather than only MUST NOT refuse: a decoder that invents an entry address is worse than one that fails loudly, and a refusal-only rule would have called it conforming.

conformance/codec/nodekey_null_leniency.json replays the rule in both codecs and on both fields. It pins the decoded key as absent and pins the re-encoded frame: a decoder may read the null form, but an encoder must still emit only the omitted one, so a binding cannot satisfy the clause by round-tripping null straight through.

IpcValue (payload)

A DeltaOp cell payload is carried as an externally-tagged IpcValue:

IpcValue = { "Inline": [u8] }           // inline byte array (JSON array of 0..255)
          | { "SharedBlob": ShmBlobRef } // descriptor into a shared-memory arena

NodeState

A NodeSnapshot / NodeAdd node body is carried as an externally-tagged NodeState:

NodeState = { "Payload": [u8] }          // concrete serialized value bytes
           | { "SharedBlob": ShmBlobRef } // concrete value in shared memory
           | "Opaque"                      // visible node whose value cannot be serialized

Opaque serialized value bytes are owned by the producing language; type-aware decoding is fixed by the stable type_tag carried on the node. Over the JSON codec, bytes are transmitted as JSON arrays of integers in 0..255 (not base64). Under the negotiated json-base64 feature (#lzspecbase64, see § Capability Negotiation), a peer MAY instead encode Inline/Payload byte arrays as a base64 string, cutting ~4× wire bloat and ~3× parse cost; json-u8 stays the canonical fixture form.

type_tag

Each serializable node carries a type_tag: &'static str — a stable cross-process key that maps to a language-local deserialization constructor. The type-tag registry is per-implementation; tags must not collide across nodes.

Batch string-intern table (#lzspecintern)

A Snapshot, Delta, or CrdtSync batch that repeats the same type_tag string or the same NodeKey prefix across many nodes pays a per-node string cost that dominates wire size at scale. A batch MAY carry an optional sidecar intern table that assigns small integer ids to repeated strings; nodes then reference the id instead of inlining the string.

InternTable = { strings: [string] }   # index → string; position is the id

• An empty or absent intern field is the default and means “all strings are inlined” — existing decoders are unaffected (additive, backward-compatible).
• A sender populates intern.strings with the deduplicated type_tag values (and, opt-in, repeated NodeKey namespace prefixes) appearing in the batch, then writes the integer id in each node’s tagged field. The reference is scoped to the batch and does not persist across frames.
• A receiver resolves ids against intern.strings; an id with no entry is a decode error (fail closed).
• The intern table is a pure wire optimization: the decoded IpcMessage is identical whether or not interning was used. Conformance fixtures exercise both the interned and inlined forms.

IPC: Snapshot + Incremental Update Protocol

lazily-IPC transmits a reactive graph’s state to a remote observer and keeps it in sync as the graph mutates.

Two message kinds

• Snapshot — full graph state. Sent on connect and on resync.
• Delta — incremental change set. Sent once per outermost batch-flush invalidation pass.

Epoch / versioning

A context-level monotonic ipc_epoch: u64 advances once per outermost batch flush, not per write.

• Snapshot carries epoch.
• Each Delta carries { base_epoch, epoch } with epoch >= base_epoch + 1. The common single-flush case is epoch == base_epoch + 1; a multi-epoch-span delta (epoch > base_epoch + 1) coalesces several accepted-event epochs into one op batch (see § Multi-epoch-span delta). The span epoch - base_epoch is the count of accepted (deduped) events this batch advances past — a re-emit that dedups to a no-op adds no span. epoch < base_epoch + 1 (empty or backward) is never valid.
• Deltas are contiguous by base, not strictly unit-stepped. A receiver detects gaps, reorders, or sender restarts by checking base_epoch == last_epoch: a delta whose base_epoch != last_epoch is a gap and triggers resync (§ Reliable Sync) regardless of its span.

Snapshot

{
  "Snapshot": {
    "epoch": 1,
    "nodes": [
      { "node": 1, "type_tag": "i32", "state": { "Payload": [1, 2, 3, 4] } }
    ],
    "edges": [
      { "dependent": 2, "dependency": 1 }
    ],
    "roots": [1]
  }
}

NodeSnapshot

{ "node": 1, "type_tag": "i32", "state": { "Payload": [1, 2, 3, 4] } }

EdgeSnapshot

{ "dependent": 1, "dependency": 0 }

Delta

{
  "Delta": {
    "base_epoch": 40,
    "epoch": 41,
    "ops": [
      { "CellSet":    { "node": 1, "payload": { "Inline": [10] } } },
      { "SlotValue":  { "node": 2, "payload": { "Inline": [20] } } },
      { "Invalidate": { "node": 3 } },
      { "NodeAdd":    { "node": 4, "type_tag": "u64", "state": { "Payload": [64] } } },
      { "NodeRemove": { "node": 5 } },
      { "EdgeAdd":    { "dependent": 2, "dependency": 1 } },
      { "EdgeRemove": { "dependent": 3, "dependency": 1 } }
    ]
  }
}

DeltaOp variants

All DeltaOp, IpcValue, NodeState, and IpcMessage variants are externally tagged: a single-key JSON object whose key is the PascalCase variant name and whose value is the body (or a bare "Opaque" / unit string).

QueueCell op-log delta form (#queue-oplog)

A QueueCell reconciles by two complementary wire forms, chosen by plane:

• Snapshot plane → storage-snapshot form. The full queue state is the storage backend’s snapshot (the reference VecDequeStorage serializes as a FIFO-ordered JSON array — cell-model.md § Wire and snapshot shape). This is the state form.
• Delta plane → op-log form. Incremental change is the ordered op-log of QueuePush / QueuePop / QueueClose shell ops above, carried in a Delta exactly like any other DeltaOp (same base_epoch/epoch span, gap rule, and batch = fold semantics). This is the op-log form.

Why a queue needs the op-log form and cannot use state-supersede coalescing: a queue’s order and multiplicity are its value, and the consumer’s pop position is receiver-side state a sender snapshot cannot see — so collapsing the unacked suffix to a state snapshot would break exactly-once FIFO consumption. Instead the op-log fuses a maximal run of same-direction QueuePush ops into one multi-epoch batch Delta (order-preserving, lossless; a QueuePop/QueueClose is a fusion boundary). Fusion bounds frame count, not memory — see § Backpressure & outbox coalescing.

SPSC crossing rule. In the default producer→consumer sync the producer’s op-log carries QueuePush/QueueClose; the remote consumer owns consumption, so its QueuePop is local and does not cross. Only a mirror sync (an authoritatively-replicated consumer) also carries QueuePop so mirrors converge on the consumption position. A re-delivered queue op (base_epoch < last_epoch) is Ignored by the ResyncCoordinator, so at-least-once replay neither drops nor double-applies a push or pop.

Consistency invariants

• PartialEq cell guard: An equal set emits no CellSet and no downstream ops.
• Memo equality suppression: A dirty memo() that recomputes to an equal value emits no SlotValue and no downstream Invalidate.
• Coalesced frontier: A dependent reached through many changed cells in one batch appears at most once per delta.
• Eager Signal values are concrete: A changed eager Signal emits a concrete SlotValue for its backing slot, not a bare Invalidate.

The companion Lean model in formal/lean encodes these IPC transition rules and checks them with lake build.

Eager Signal nodes

A Signal is the eager derived value in the Slot -> Cell -> Signal family. It is not a separate wire type. A Signal is represented by the ordinary backing slot node that stores its materialized value:

• Snapshot: the backing slot appears as a NodeSnapshot with a concrete payload/shared-blob payload like any other readable slot.
• Delta: a value change appears as SlotValue for the backing slot’s NodeId. Because the value is recomputed during the invalidation flush, eager Signals do not emit bare Invalidate ops for their own changed value.
• Memo guard: an eager recompute that yields an equal value suppresses SlotValue and downstream invalidation exactly like a lazy memoized slot.
• Local puller: the producer-side effect that keeps the Signal eager is local execution state and is not serialized as a graph node.

Consumers therefore need no protocol extension to read eager Signals from a producer. They observe the same permission-filtered Snapshot/Delta state plane and see Signals as slots whose changed values are reliably materialized.

Lazy reconciliation

• Value-mirror (default): At flush, the sender resolves each invalidated allowlisted slot so the delta carries concrete SlotValues. The receiver holds no compute closures.
• Mirror-lazy: The sender emits bare Invalidate; the receiver keeps a stale marker. Requires compute closure replication. Deferred to lazily-distributed.

Wire shape. The value-mirror default means an allowlisted dirty slot appears in a flush Delta as a concrete SlotValue, never a bare Invalidate (the latter is the mirror-lazy form). This invariant — and the eager-Signal rule that a changed Signal publishes a SlotValue for its backing slot, not an Invalidate — is pinned by the IPC fixtures delta_sequential.json and delta_shared_blob.json, both of which carry SlotValue ops for resolved slots.

Resync / gap handling

On a Delta whose base_epoch != last_epoch:

1. Receiver discards the delta.
2. Receiver requests a fresh Snapshot.
3. Sender replies with Snapshot { epoch }.
4. Deltas resume from the new epoch.

This narrative is the informal shape; the normative decision function (inbound frame → Apply / RequestSnapshot / Ignore) is the ResyncCoordinator state machine specified in § Reliable Sync, which also fixes the durable-outbox replay and sync-driver loop that make gap recovery, reconnect backfill, and at-least-once delivery a protocol rather than an each-consumer hand-roll.

Messages are length-prefixed and tagged Snapshot / Delta. The protocol is transport-agnostic (unix socket, pipe, WebSocket, shared memory).

Multi-epoch-span delta

A Delta MAY advance more than one epoch in a single frame: epoch > base_epoch + 1. This models a producer whose epoch is a cumulative count of accepted (deduped) events and who coalesces several such events into one flush (agent-doc’s WireDelta is exactly this: a delta “may span multiple epochs”, epoch = per-document accepted-event count). The op list is still the ordered change set; epoch - base_epoch records how many accepted events the batch folds.

Normative apply semantics:

• Batch = fold. Applying one Delta { base_epoch, epoch, ops } MUST equal applying the same ops in order as a run of unit deltas that advances last_epoch from base_epoch to epoch. The receiver observes only the endpoints (base_epoch, epoch); intermediate epochs are not separately materialized. Proven equivalent in lazily-formal (ReliableSync.multi_epoch_apply_eq_fold).
• Atomic advance. The receiver advances last_epoch to epoch only after the whole op list applies; a partial application never leaves last_epoch at an intermediate value.
• Gap rule unchanged. Acceptance still requires base_epoch == last_epoch; the span does not relax gap detection. A delta with base_epoch != last_epoch is a gap at any span.
• Idempotent re-emit adds no span. A re-emitted delta that dedups to no accepted change carries epoch == base_epoch worth of new effect and is either omitted or applied as a no-op; it never advances last_epoch.

Wire-compat: the unit-step case (epoch == base_epoch + 1) is the span-1 special case, so every existing Delta fixture remains valid. Conformance: conformance/reliable-sync/multi_epoch_delta.json.

Shared-memory IPC

ShmBlobArena provides the shared-memory payload path (a required layer wherever the platform supports it — see § Shared-memory payload path is required):

• Arena writes a fixed header before each payload: { generation, epoch, length, checksum }.
• Readers validate the header before accepting a descriptor.
• IpcMessage control frames carry ShmBlobRef descriptors instead of embedding large bytes inline.

Shared memory carries large blob payloads; ordinary control transport carries framed IpcMessages. Each process keeps its own local Context / ThreadSafeContext and reconciles via snapshots and deltas. A binding whose platform cannot host a shared-memory arena carries every large payload Inline over the control transport (IPC / WebSocket / WebRTC) — the I/O channel accesses the memory directly, so the peer still receives the bytes without a shared-memory descriptor.

Capability Negotiation

Each non-local session starts with a compatibility handshake:

{
  "protocol_id": "lazily-ipc",
  "protocol_major_version": 1,
  "codec": "json",
  "max_frame_size": 1048576,
  "fragmentation_supported": false,
  "ordered_reliable": true,
  "peer_id": 1,
  "session_id": "abc-123",
  "features": ["shared-blob", "signaling-relay"]
}

max_frame_size is a positive receive ceiling, not an equality constraint. Peers with different ceilings remain compatible and negotiate min(local.max_frame_size, remote.max_frame_size). Both directions use that common ceiling; a binding MUST retain the negotiated value rather than continuing with its local advertisement. A zero ceiling is invalid and fails closed.

Fragmentation is available to the session only when both peers advertise fragmentation_supported = true. A true/false pair remains compatible but negotiates false; treating one peer’s support as sufficient would ask the other peer to reassemble a frame it said it cannot accept.

session_id names the shared graph/session, while peer_id names one endpoint. The two handshakes MUST carry the same non-empty session_id; their peer_id values may and normally do differ.

If peers disagree on protocol_major_version, codec, ordered_reliable, session_id, or required features, or if either max_frame_size is zero, they fail closed before applying any Snapshot or Delta.

Feature flags. The features array advertises optional capabilities both peers must offer to use. Defined flags:

protobuf-graph-boundary-v1 is an additive typed boundary family, not another encoding of IpcMessage and not a second graph runtime. Its ProtocolEnvelope carries stable identity, causality, bounded mutations, projections, effect intents, and receipts. Canonical JSON remains the fixture and diagnostic authority, and logical identity hashes canonical values rather than Protobuf bytes.

Frame codecs

Every serialized IpcMessage frame (Snapshot, Delta, CrdtSync) carries the same logical wire schema; the codec handshake field selects only how those fields are bytes-encoded. Three codecs are defined; a binding advertises the set it can encode/decode and the peers negotiate one.

Two senses of “canonical” — read this first. This spec keeps two terms distinct:

• Reference codec = a role: the required, dependency-free, human-inspectable encoding that every binding MUST speak, that the FFI baseline re-encodes to, and that conformance fixtures / logs / receipts are written in. json is the reference codec. It is chosen for this role because it is universal (a parser in every stdlib), inspectable, and deterministic — not because it is efficient (it is the least efficient codec).
• Canonical bytes = a property of one codec+message: the single deterministic byte string a given codec produces for a given IpcMessage. json and positional postcard are byte-canonical (one byte form per message per codec). msgpack named-field maps are not byte-canonical across encoders (map key order is encoder-defined), so msgpack is the reference-compatible efficient transport, never the reference codec.

These are orthogonal: “reference codec” answers which encoding is the required interop floor; “canonical bytes” answers does this codec produce one deterministic byte form.

Default selection. A local, same-process, same-language pairing MAY default to postcard. A boundary that crosses languages (the plugin⇄controller boundary, browser peers) negotiates msgpack; json is the interoperable fallback and the required reference codec (also the FFI baseline form). Peers never apply a frame under a codec they did not negotiate.

MessagePack encoding is named-field. msgpack frames encode each struct as a MessagePack map keyed by the JSON field name (Rust: rmp_serde::to_vec_named), not as a positional array. This keeps the field names identical to the json schema, so the omit-when-absent rule for optional fields (the nullable key on NodeSnapshot/NodeAdd/CrdtOp, § NodeKey) holds uniformly across json and msgpack, and a decoder that predates a later optional field ignores it. Positional postcard instead always carries the optional discriminant for binary schema stability.

Conformance is semantic round-trip, not byte-identical, for the map codecs. Because a MessagePack map’s key order is encoder-defined, two conforming bindings MAY emit byte-different msgpack frames for the same IpcMessage; conformance requires only that decode(encode(m)) == m and that decoding a peer’s frame yields the equal IpcMessage. Only postcard (positional) is byte-canonical across encoders. Cross-language msgpack fixtures therefore pin the decoded value, never a golden byte string.

The codec requirement is executable, not prose (#lzmsgpackparity). Stating “every frame MUST round-trip through both json and msgpack” in this document proved nothing: the conformance ladder verifies fixture content replay (was the file opened, were its keys consumed, were they asserted, were all its scenarios replayed), and content replay never exercises a codec. A binding could therefore carve out a MUST-level codec and stay green everywhere. Two canonical fixtures now carry the obligation:

Both carry the same three wire values (one per IpcMessage variant) so one runner shape serves both codecs. A runner MUST decode wire, re-encode the decoded message, decode it again, and evaluate every expect key against that second decode — asserting against the fixture literal proves nothing, because the literal never passed through the codec. The msgpack fixture additionally pins encoded_envelope_key and the sorted encoded_body_field_names, which is the executable form of the named-field rule above: a positional encoder round-trips a value correctly and fails those keys. postcard carries no cross-language fixture — it is MAY, and by construction only two peers sharing a struct layout can speak it.

A binding that does not implement msgpack is not silently exempt. Its scripts/check-conformance-coverage.sh sees the canonical fixture and fails until the binding either replays it or names it in KNOWN_UNCOVERED with a reason — the same ledger every other declared gap lives in — and coverage.json carries one row per codec flavor so the matrix shows the carve-out beside every other parity fact.

Shipping a MessagePack codec is not implementing msgpack. The codec token names one wire, not a serialization technology: the externally-tagged frame ({"Snapshot": {…}}) over named-field maps whose keys are the json field names, with the same omit-when-absent rule for optional fields. A codec that packs the same data as an internally-tagged envelope ({"type": 0, "value": …}), gives NodeState/IpcValue integer kind discriminators instead of the Payload/Inline external tags, or uses positional arrays, is a private codec that happens to use MessagePack framing — a peer that negotiated msgpack with it would not decode its frames. That distinction is invisible to a file-presence audit and is exactly what the round-trip fixture makes checkable, which is why the matrix distinguishes ✅ from ~ on this row.

Causal Receipts

Some integrations send a command or publish an effectful request and need a durable, queryable outcome for that causation id. lazily supplies a generic causal receipt primitive for that use case; it is not a transport ACK and does not make delivery success authoritative.

{
  "CausalReceipts": {
    "receipts": [
      {
        "receipt_id": "receipt-1",
        "causation_id": "patch-123",
        "observer": "editor",
        "generation": 7,
        "outcome": "applied",
        "reason": null,
        "payload_hash": "sha256:2cf24dba5fb0a30e26e83b2ac5b9e29e1b161e5c1fa7425e73043362938b9824"
      }
    ]
  }
}

Receipt projection rules:

• observed and accepted are non-terminal. They may model ACK-like transport or queue admission observations, but a domain MUST NOT treat them as proof that an effect happened.
• applied and rejected are terminal. They are the generic outcome vocabulary that domain-specific facts refine (for example an editor may publish EditorPatchApplied / EditorPatchRejected facts keyed by the same causation_id).
• A stale-generation receipt is ignored by the current projection and may be retained only as audit/debug data.
• A second terminal receipt for the same causation_id and generation with a different terminal outcome is a terminal conflict; consumers fail closed instead of selecting a winner.
• The primitive is state/projection data. Transports may still provide their own delivery acknowledgements internally, but lazily does not expose delivery ACKs as authority.

Command / RPC Message Plane

Editor and runtime integrations issue commands — Run Agent Doc, sync, focus, save, session operations — and need one reusable admission, dedupe, cancellation, generation-guard, progress, and reconnect story instead of a per-caller ad hoc request/response contract. lazily supplies an evented command message plane for that use case. It is an additive sibling family to Snapshot / Delta / CrdtSync; it does not add new state-plane variants.

The plane is feature-gated. Peers advertise command-plane-v1 in the Capability Negotiation features array. A peer that lacks command-plane-v1 fails closed before accepting command traffic; a command that requires the plane is not silently downgraded.

Four externally-tagged frames make up the family:

CommandSubmit

{
  "CommandSubmit": {
    "command_id": "cmd-run-1",
    "causation_id": "cmd-run-1",
    "source": "vscode-plugin",
    "target": "project-controller",
    "namespace": "agent-doc",
    "name": "editor_route",
    "authority_generation": 42,
    "idempotency_key": "project-root:plan.md:run",
    "deadline_ms": 120000,
    "policy": { "dedupe": "same_idempotency_key", "supersede": false, "cancel_on_preempt": true },
    "payload_type": "agent-doc.editor_route.v1",
    "payload_hash": "sha256:…",
    "payload": { "Inline": [123, 34, 102, 34, 58, 34, 46, 34, 125] },
    "required_features": ["causal-receipts", "command-events"]
  }
}

lazily owns the envelope (command_id, correlation, idempotency, generation, policy, payload framing). The namespace owns the payload: lazily never interprets the payload body, which is a normal IpcValue (inline bytes or a shared-memory blob). payload_type and payload_hash identify and pin the domain body.

CommandCancel

CommandCancel preempts a still-non-terminal command by command_id at a given authority_generation, with an optional reason. A stale-generation cancel is ignored. A cancel after a terminal outcome never rewrites it.

CommandEvents

CommandEvents batches progress/detail events keyed by command_id. Event kinds are observed, accepted, started, progress, cancelled, superseded, timed_out. Events are UX and diagnostics only — queue position, retry advice, copied CLI output. They are never terminal proof. Even cancelled / superseded / timed_out events are surfaced for UX; their terminal authority is a matching rejected causal receipt.

CommandProjection

CommandProjection is the folded, queryable image of known command state: per-command status, an explicit terminal flag, generation, terminal reason, and the terminal_receipt_id / last_event_id that produced it. It is also the reconnect resync frame: after a controller handoff/recycle a plugin folds a fresh CommandProjection and recovers in-flight and terminal state without replaying the underlying events.

Projection rules

• Terminal authority is the causal receipt, not the event or the transport. A command becomes terminal (applied / rejected / cancelled / superseded / timed_out) only when a terminal CausalReceipt for its command_id folds in. observed / accepted / started / queued admission are non-terminal progress. A network ACK is never terminal.
• Generation guards. Events and receipts whose generation does not match the command’s current authority generation are ignored by the projection and retained only as audit data.
• Idempotency. A replayed CommandSubmit, event, or receipt (same command_id / event_id / receipt_id) is a no-op; the projection is unchanged.
• Cancel before terminal only. A cancel terminally rejects a non-terminal command; a cancel after applied is ignored.
• Terminal conflict fails closed. Two terminal receipts at the same generation with different outcomes is a conflict; consumers fail closed rather than pick a winner (the same rule as Causal Receipts).
• Reconnect equivalence. Folding a CommandProjection image is equivalent to folding the events and receipts it summarizes.

RPC facade

Bindings expose an RPC-style API (call / submit / cancel / observe / projection) implemented entirely over these frames:

• call builds and sends a CommandSubmit, observes events and receipts, and resolves only when the command projection reaches a terminal causal receipt. A transport ACK, controller admission, or accepted / queued event never resolves a unary call.
• submit returns the command_id immediately for callers that manage events and projection themselves.
• cancel sends CommandCancel and returns the resulting projection.
• observe / stream exposes CommandEvents and projection updates for UI progress.
• Reconnect uses CommandProjection; callers replay a call only when the idempotency policy says replay is safe.
• The terminal-result error shape exposes the terminal command projection (status, reason), not a collapsed boolean.

Unary RPC completion means command effect completion, proven by a terminal causal receipt — not network delivery. The schema is schemas/message-passing.json; fixtures live in conformance/message-passing/.

Cross-language Channel Compatibility

All channels carry the same IpcMessage state plane:

Cross-language rules

• Compute closures are language-local. Cross-language sync shares the cell state plane.
• Permission filtering happens before serialization on every channel.
• Back-pressure: if frames gap, reorder, or truncate, the receiver requests a fresh Snapshot.

Binding Conformance Matrix

A lazily binding is a language port that intends to interoperate with the wider lazily ecosystem (lazily-rs, lazily-py, lazily-zig, lazily-js, lazily-kt, lazily-dart, lazily-go, …). The layers below are required of every binding; none is an optional lazily-rs extension. A binding that omits a MUST row is non-conforming and MUST advertise its missing surface via Capability Negotiation rather than failing silently.

¹ C-ABI FFI has a platform carve-out — see § C-ABI FFI is required. ² The thread-safe and async context layers have a platform carve-out — see § Concurrency layers are required. ³ The shared-memory payload path has a platform carve-out (I/O-channel fallback) — see § Shared-memory payload path is required. CRDT and the keyed cell collections have no carve-out: they are wire/logic properties implementable on any runtime that speaks the wire.

C-ABI FFI is required

Every binding whose platform can host a native in-process boundary MUST expose and consume the C-ABI FFI boundary: the LazilyFfiBytes / LazilyFfiStatus / LazilyFfiMessageKind contract with explicit allocation ownership, panics caught before crossing the C ABI, and a channel that decodes each accepted frame as IpcMessage and re-encodes canonical JSON bytes. The FFI message kind discriminant MUST include CrdtSync = 3 and the reliable-sync control frames ResyncRequest = 4 / OutboxAck = 5 (§ Reliable Sync). This is the lingua franca that lets any binding embed any other without a language-specific bridge.

Platform carve-out. A binding whose runtime structurally cannot host a native C ABI declares the ffi capability as none; otherwise it declares host. none is reserved for platforms with no shared in-process address space (for example browser/Worker JS, or a fully-sandboxed runtime) — a binding MAY NOT declare none merely because FFI is inconvenient or unimplemented. This is a binding-level conformance declaration (advertised in the binding’s conformance statement and discoverable at build/link time), not a per-session wire flag, since in-process embedding is not a runtime session.

A ffi = none binding:

• conforms to the interop contract but not the in-process embedding contract, and MUST NOT advertise itself as embeddable;
• MUST still expose the full state plane — including CrdtSync — over IPC/WebSocket/WebRTC, so it interoperate without in-process embedding; and
• MUST be treated by peers/host tooling as unable to be loaded in-process (fail closed on any attempt to do so, rather than silently degrading).

This reuses the existing fail-closed principle: the limitation is explicit and advertised, never silent. There is no equivalent carve-out for CRDT or the cell/collections model — those are implementable on any Turing-complete runtime that speaks the wire.

CRDT is required

Every binding MUST implement the CrdtSync plane — the merge: crdt mechanism, the WireStamp version-vector frontier, and the causal-stability watermark / GC contract — and MUST round-trip a CrdtSync IpcMessage byte-identically. Multi-write convergence is a property of the cell model, not an optional distributed extra; a binding that ships only the single-producer Snapshot/Delta mirror conforms only to the single-writer subset and MUST downgrade its advertised capability accordingly.

Concurrency layers are required

The reactive core ships as three context layers — single-threaded (base), thread-safe (lock-backed), and async (future-returning) — defined in Reactive Graph § Context layers and Async Reactive Context. The single-threaded base context is unconditionally required of every binding (it is the reactive-core row above). The thread-safe and async layers are required conditionally: a binding whose platform structurally supports a layer MUST implement that layer.

Thread-safe context. A binding whose platform exposes preemptive multi-threading or shared-memory concurrency (native threads, OS goroutines, JVM threads, Kotlin coroutines over a shared heap, etc.) MUST ship the lock-backed context whose handles are clonable and whose transition function and state are Send + Sync, so observers fire synchronously within the invalidating send/batch preserving glitch-free pull-based ordering. “Synchronously within” mandates glitch-free ordering, not literal in-lock dispatch — a threaded binding MAY defer observer dispatch out of the graph lock provided the ordering invariant holds (#lzspecobserverclarify). A platform with no shared-memory threading model — a strictly single-threaded runtime, or a process/actor-isolation model (e.g. a Dart isolate, a browser Worker) where peers do not share an address space — declares the thread_safe capability as none.

Async context. A binding whose platform exposes an async/future runtime (async/await, promises, coroutines, an executor that suspends and resumes across .await points) MUST ship the async context with its full slot state machine (Empty / Computing / Resolved / Error), revision tracking, five-point cancellation contract, and get_async re-resolve loop. A platform with no notion of suspendable async computation declares the async capability as none.

A none declaration, for either layer:

• is a binding-level conformance declaration (advertised in the binding’s conformance statement and discoverable at build time), not a per-session wire flag, because in-process concurrency structure is not a runtime session;
• MUST be reserved for platforms that structurally lack the primitive — a binding MAY NOT declare none merely because the layer is inconvenient or unimplemented; and
• MUST be advertised rather than fail silently, reusing the existing fail-closed principle.

There is no carve-out for the keyed cell collections, the state machine, the state charts, the reactive core, or CRDT — those are implementable on any Turing-complete runtime that speaks the wire, single-threaded or not.

Shared-memory payload path is required

The shared-memory payload path (ShmBlobArena + ShmBlobRef descriptors) is the zero-copy large-payload transport for IpcValue and NodeState. A binding whose platform exposes a shared-memory primitive (POSIX shm / memory-mapped files / OS shared memory / a peer-reachable arena) MUST implement it: payloads above the inline threshold are written into the arena, the control frame carries the ShmBlobRef descriptor, and readers validate the { generation, epoch, length, checksum } header before accepting it.

Platform carve-out — I/O-channel fallback. A binding whose runtime structurally cannot host a shared-memory arena (browser/Worker JS, a sandboxed runtime, WASM without shared memory) declares the shared_memory capability as none. Such a binding MUST fall back to I/O channels accessing the memory: every payload that would have been a SharedBlob descriptor is instead carried Inline over the ordinary IPC / WebSocket / WebRTC transport, so the same IpcMessage state plane reaches the peer without a shared-memory descriptor. The wire format already supports both paths (IpcValue and NodeState are externally-tagged Inline | SharedBlob); the fallback simply never emits the SharedBlob variant on that binding and treats an absent descriptor as Inline on read.

Shared memory is negotiated per session via the shared-blob entry in the Capability Negotiation features array: two peers that both advertise shared-blob MAY exchange ShmBlobRef descriptors; if either peer omits it, both sides carry payloads Inline over the control transport for that session. (The thread_safe, async, and ffi capabilities, by contrast, are binding-level declarations — in-process properties — and are not per-session wire flags.)

This reuses the existing fail-closed principle: the limitation is explicit and advertised, never silent. The shared-blob conformance fixtures (snapshot_shared_blob.json / delta_shared_blob.json) fix the descriptor shape for bindings that ship the arena; an Inline-only binding round-trips the same fixtures with the blob bytes inlined.

The backend discriminator: absence is lenient, an unknown value is not (#lzblobbackendstrict)

ShmBlobRef.backend selects which pluggable backend resolves a descriptor (shm | arrow | in_process, optional, default shm — see docs/zero-copy-transport.md). The two ways a decoder can fail to recognise it are not the same fact and MUST get opposite answers:

• An OMITTED backend MUST decode as shm. This is the forward-compatibility channel, and the only one. Every descriptor minted before the field existed has this shape, which is exactly why the field is optional. A conforming encoder MUST also omit it when the backend is shm, so a pre-field descriptor round-trips byte-identically — the same encoder/decoder split § NodeKey makes for key.
• A PRESENT backend outside the enum MUST be rejected, with the offending token named in the error. A decoder MUST NOT normalize it to shm, to any other backend, or to a sentinel.
• An explicit backend: null is the ABSENT form, not a present-unknown one, and MUST decode as shm. This follows § NodeKey rather than the bullet above, and for the same reason: a serde-style peer that did not apply skip_serializing_if to an optional field emits null where a conforming encoder omits, so refusing it is stricter than the reference implementation on a frame the reference implementation produces. Four bindings raised this edge independently while implementing the clause, and they had already split three ways on it — accept-as-shm, error.ExpectedString naming nothing, and a refusal naming the token ''.
• shm is the permanent default. A future revision MUST NOT redefine which backend an omitted backend denotes. The omitted form is the only shape a pre-field descriptor can have, so changing its meaning would silently reinterpret every descriptor ever written rather than break them visibly — the one genuinely undecidable case on this wire, and cheaper to pin as a sentence than to discover as an incident.

Two obligations on the refusal itself.

It must be catchable through the codec’s documented decode-error type. A refusal raised as a type outside the family every caller already guards a decode with is invisible: the frame still fails, but it fails past the handler. In C++ that means std::runtime_error and specifically not std::invalid_argument, which derives from std::logic_error — the identical hierarchy trap that let a std::out_of_range from std::stoll escape every decode guard until the NodeId bound was audited. The general rule: a decoder’s refusals belong in one catchable family, and this clause adds no exception to it.

Naming the token is bounded. A binding MAY truncate the offending token in its error (64 bytes is sufficient), and a truncated name satisfies the obligation. The refusal path is the path a hostile or corrupt producer controls, so an unbounded “echo the token back” requirement is an allocation and log-flood vector; a truncated name still identifies the producer, where an absent one does not.

The cost this accepts, stated plainly. A refusal fails the whole frame, not just the descriptor. So a fourth backend added later is a hard break for every older peer rather than a degraded read, and at the decoder a corrupt frame and a future-version frame are indistinguishable — nothing on the frame carries a protocol version, only the session-level shared-blob capability flag. That is the deliberate trade: a visible break a peer recovers from by resync, in exchange for never resolving a descriptor against a backend its producer did not name. The alternative buys graceful degradation with a guarantee that holds only until a checksum collides.

The asymmetry is not stylistic. A new backend enters the protocol by adding an enum value — a spec change with a fixture, not a wire event (§ Pluggable backends in the zero-copy transport doc) — so an unknown token is not a newer peer talking to an older one. It is a corrupt frame or a non-conforming producer, and both are conditions a peer recovers from by resync (§ Resync / gap handling).

Normalizing it is worse than it looks, and the reason is a theorem the model already proves. resolve_wrong_backend states that a descriptor of one kind never resolves against a different backend’s table — receivers route by kind. Reading an unknown kind as shm is routing a non-shm descriptor into the shm table; the {generation, epoch, len, checksum} verification then usually rejects it, so the observable outcome is right most of the time. That is the trap: the guarantee is supposed to be structural, discharged by routing, and normalization silently downgrades it to a probabilistic one discharged by a 64-bit checksum, against a backend this build genuinely resolves. It is the same substitution the decoder bound already outlaws for NodeId in § NodeId / PeerId — the frame decodes cleanly, addresses something other than what the producer named, and nothing downstream can tell.

Audited (#lzblobbackendstrict) across the library decode surface of all nine bindings, which had split 5–2 — and every one of the five documented its choice as deliberate wire forward-compat:

The lazily-cs row is wrong and is left standing as a record of the error. Replaying fixture v2 found a real dispatch site there — IpcWire.ReadBlob on decode, IpcWire.WriteBlob on encode, and BlobTransport.EffectiveBackend at every routing site. “No dispatch site” was a review conclusion, and it is the kind of conclusion a replay overturns: an audit that reads for a switch finds nothing when the discriminator is read through a field-typed path that dispatches anyway.

The five agreed with each other on the defence, too: the checksum catches it, so the descriptor resolves to nothing rather than to another backend’s bytes. That argument is what the theorem exists to make unnecessary. An undocumented default and a deliberate one are indistinguishable from the outside — and, it turns out, so are two deliberate ones pointing in opposite directions. conformance/codec/blob_backend_discriminator.json replays both halves in both codecs. It carries an arrow scenario so the leniency cannot be implemented by ignoring the discriminator outright, and pins the re-encoded frame so a binding cannot satisfy the clause by round-tripping whatever it received. The encoder half is a separate obligation and is not implied by the decoder half: lazily-rs has carried skip_serializing_if since the commit that introduced the field, while a binding can implement strict rejection and still emit backend: "shm" — which is why the re-encode assertions exist rather than being inferred.

Fixture v2 (#lzblobbackendstrict) closes four holes v1 left. Every one of them was found by a binding replaying v1, not by reviewing it — which is the argument for replaying a fixture in nine places before trusting it. The fixture is now 14 scenarios, seven wire shapes in both codecs:

• in_process is carried, not merely declared. v1 listed three backends in assertions.backends and shipped scenarios for two, so a binding that knew only {shm, arrow} rejected in_process — naming the token, conformingly, by the letter of this clause — and passed all eight scenarios while implementing a smaller enum than the clause declares. Found independently by three bindings. The arrow control proves the discriminator is read; in_process proves the vocabulary is complete, and no scenario count substitutes for it: the missing fact was a set difference, so the corpus-side guard is now a set difference (test_backend_fixture_carries_every_backend_it_declares).
• The null bullet above is executed, not just written. Four bindings raised it independently while implementing v1 and had already split three ways. It is an accept scenario that is deliberately schema-invalid: the string-typed enum binds the ENCODER, and the decoder’s leniency is the separate fact under test. The re-encode assertion still applies, so the null does not survive a round trip.
• A non-string backend is a scenario. The clause is written entirely about tokens, so a runtime whose reader coerces rather than throws on a number in a string position normalizes silently there — the same failure this clause names, arriving through a door it does not describe. One binding’s only real defect under v1 was exactly this. Both reject forms now assert expect.rejection_is_decode_error, which is the It must be catchable obligation above made executable; expect.rejection_kind distinguishes them, and only unknown_token carries error_names_token, because a type error has no token to name and requiring the field name would pin a message format no codec’s native type error produces.
• expect.epoch is gone, replaced by frame_epoch (9) and blob_epoch (5). v1 carried 9 in both the Delta frame and the ShmBlobRef descriptor, so a runner reading the frame’s epoch and one reading the descriptor’s both passed a single assertion. Found by two bindings. The key was removed rather than redefined so a runner still reading it fails loudly instead of silently reading the other one.

Two codecs are still not two implementations. Several bindings bridge MessagePack into the same DOM the JSON decoder produces, or share one serde impl, so the msgpack half of a scenario pair can yield one discriminator verdict rather than an independent second one. It still covers the bridge and the encoder; a fully green run must not be read as two implementations agreeing, and a binding whose two codecs share a decode path should record that in its own ledger rather than infer independence from the scenario count. This one is not fixable in the corpus — it is a property of the bindings — so it stays stated rather than pinned.

What v2 found when the nine bindings replayed it. The four holes above were predictions about what an unexecuted clause hides; this is what was actually behind them:

• Four of nine bindings REFUSED the explicit null — lazily-rs (#[serde(default)] supplies the default when the key is missing, so a present null still reached BlobBackendKind::Deserialize and failed as a type error in both codecs), lazily-cs (a ValueKind error), lazily-zig (error.ExpectedString), lazily-kt (JsonNull is a JsonPrimitive whose isString is false, so it fell into the non-string arm). Each returned a decode error for a frame the reference implementation emits. The bullet stating the rule had been in this document since the clause landed; it was prose, and four bindings read it and still got it wrong — including lazily-rs, which the row above records as reaching the conforming answer on the unknown token independently. Being right about the hard half of a clause is not evidence of being right about the easy half. That ratio is the argument for making an adjudication executable rather than writing it down.

  The lazily-rs fix carries a detail the other bindings do not face: serde_json’s deserialize_str constructs the invalid_type error itself on a null and never calls the visitor, so reading the null requires deserialize_option — and that forced a branch on is_human_readable(), since postcard writes no option tag for this field and asking it for one would misalign the frame. The strict deserialize_str path stays for non-self-describing codecs.

• Two bindings had no decode-error family at all. lazily-zig’s decode errors were an inferred error set nobody had written down, and lazily-kt raised IllegalStateException from one refusal and IllegalArgumentException from the other — neither a subtype of the other, so a caller catching the documented one had the other fail past the handler. Both now name the family (ipc.BlobDescriptorDecodeError; sealed class IpcDecodeException). The It must be catchable obligation above was unassertable until rejection_is_decode_error existed, which is why a refusal being wrong in this specific way survived a nine-binding audit.

• rejected and rejection_is_decode_error are genuinely two facts. lazily-cpp demonstrated it on demand: throwing std::invalid_argument for the non-string turns rejection_is_decode_error red while rejected stays green. A bare is-error assertion passes the hierarchy trap.

• A fifth false-green shape, distinct from the four already catalogued. rejection_kind must be asserted against what the LIBRARY raised — a distinct error type, or the message the refusal actually produced. A runner that derives it from the scenario’s own backend_form compares the fixture to itself and passes while proving nothing. Raised by lazily-kt, which made its two refusals distinct types precisely so the assertion has something of the library’s to compare against. The four already on record are: a stale build artifact, a filter matching nothing, a probe aimed at a value the corpus never carries, and a filtered build run reporting N/N passed while selecting the target test not at all.

Two bindings’ green is worth less than it looks, and both say so in their own runners rather than letting the scenario count imply otherwise: lazily-cpp bridges MessagePack into the same JsonValue DOM decode_json produces, and lazily-py bridges into the same DOM as well, so each scenario pair there yields one discriminator verdict. The msgpack half still covers the bridge and the msgpack encoder, which are distinct failures.

FFI Boundary

Types

typedef struct {
    uint8_t* ptr;
    size_t   len;
} LazilyFfiBytes;

typedef enum {
    LazilyFfiStatus_Ok            = 0,
    LazilyFfiStatus_Empty         = 1,
    LazilyFfiStatus_NullPointer   = 2,
    LazilyFfiStatus_InvalidMessage = 3,
    LazilyFfiStatus_EncodeFailed  = 4,
    LazilyFfiStatus_Panic         = 5,
} LazilyFfiStatus;

typedef enum {
    LazilyFfiMessageKind_Unknown       = 0,
    LazilyFfiMessageKind_Snapshot      = 1,
    LazilyFfiMessageKind_Delta         = 2,
    LazilyFfiMessageKind_CrdtSync      = 3,
    LazilyFfiMessageKind_ResyncRequest = 4,  /* #lzsync control frame */
    LazilyFfiMessageKind_OutboxAck     = 5,  /* #lzsync control frame */
} LazilyFfiMessageKind;

Contract

• All allocation ownership is explicit: caller owns input bytes; Rust owns output buffers until the paired free function is called.
• Errors return LazilyFfiStatus; panics are caught before crossing the C ABI.
• The channel decodes each accepted frame as IpcMessage, then re-encodes canonical JSON bytes.

Signaling Protocol (WebSocket)

Client → Server

Server → Client

Anti-spoofing

The from field on every forwarded frame is the sender connection’s registered peer id, never client-supplied.

Example frames

{ "type": "join", "peer": 1 }
{ "type": "welcome", "peer": 1, "peers": [] }
{ "type": "offer", "to": 2, "sdp": "v=0\r\n..." }
{ "type": "answer", "from": 2, "sdp": "v=0\r\n..." }
{ "type": "ice", "from": 2, "candidate": "candidate:..." }
{ "type": "relay", "to": 2, "payload": { "any": "json" } }
{ "type": "peer-joined", "peer": 2 }
{ "type": "leave" }

Permission modes

Distributed: CRDT Cell Plane

This plane specifies merge: crdt — the first multi-write merge mechanism of the Cell Model. CRDT is one mechanism among several the cell model reserves (lww, ot, lease, custom); it is the first defined because it converges without coordination. Everything here applies to a multi-write cell that declares merge: crdt; the cell-kind classification, ingress-on-roots-only boundary, and cell-as-merge-unit granularity are defined once, mechanism-independently, in the Cell Model.

Cell register types

These are the CRDT-mechanism register types (the value shapes available within merge: crdt); they are distinct from the cell-model’s MergeMechanism axis.

CRDT properties

• Each replicated cell is keyed by a hybrid logical clock (HLC): wall-clock for human-meaningful ordering, logical counter for causal tiebreak.
• Local PartialEq invalidation guard applies after merge: equal values invalidate nothing.
• Memo equality suppression holds post-merge.
• lazily-ipc’s Delta generalizes to per-peer causal stamps: each peer keeps its own sequence; cross-peer order comes from HLC/dot metadata.

Anti-entropy wire format (CrdtSync)

The plane rides the same lazily-ipc transport as Snapshot/Delta. Alongside the single-producer mirror, a third IpcMessage variant carries multi-writer plane traffic:

# Snapshot/Delta/CrdtSync are the forward (state) plane; ResyncRequest/OutboxAck
# are the reverse-channel reliable-sync control frames (§ Reliable Sync, #lzsync).
IpcMessage = Snapshot(Snapshot) | Delta(Delta) | CrdtSync(CrdtSync)
           | ResyncRequest(ResyncRequest) | OutboxAck(OutboxAck)

WireStamp = { wall_time: u64, logical: u64, peer: u64 }   # total order (wall, logical, peer)

CrdtOp = {
  node:  NodeId,           # volatile target id
  key:   NodeKey?,         # optional wire-stable address (survives NodeId churn, #lzwirekey)
  stamp: WireStamp,        # the HLC stamp that produced this state
  state: IpcValue,         # the converged CRDT state to merge (state-based / CvRDT)
}

CrdtSync = {
  frontier: [(peer: u64, WireStamp)]?,   # the sender's per-peer stamp frontier
  ops:      [CrdtOp],                    # the op batch this frame ships
}

WireStamp is the wire mirror of the runtime HLC stamp (all plain integers), so the wire format is codec-stable whether or not a peer compiles the CRDT runtime in. It round-trips across all three codecs (JSON, MessagePack, postcard) and is classified by the FFI message kind (CrdtSync = 3).

Frontier suppression (#lzspecfrontiersuppress). frontier is optional. A frame that omits frontier (JSON/msgpack) or carries the sentinel frontier: [] means “the sender’s stamp frontier is unchanged since the last frame the receiver accepted” — the receiver reuses its last-merged frontier to compute the watermark. This is a pure wire savings on chatty peers (a frame shipping only ops need not repeat an unchanged frontier). The self-describing codecs (JSON, msgpack) omit the field when unchanged; positional postcard carries a 1-bit discriminant. A sender MUST include frontier whenever its advertised stamp has advanced; a receiver that receives a frontier-less frame with no prior frontier (cold start) MUST request a full CrdtSync (fail closed). Conformance risk is medium: paired fixtures exercise both the suppressed and the full forms.

State-based, idempotent. Each CrdtOp ships the converged register/sequence/text state for a node. The receiver merges state into its local replica; because every cell CRDT merge is commutative, associative, and idempotent (proven in formal/lean/LazilyFormal/CRDT.lean, stampJoin_{comm,assoc,idem}), out-of-order, duplicated, or batched delivery all converge. Re-sending a frame the receiver already has is a no-op.

Stamp-frontier exchange. CrdtSync.frontier advertises the highest WireStamp the sender has observed from each peer. The receiver merges it into its own frontier (per-peer max); the causal-stability watermark is the min over membership of that frontier — the causal point every replica has provably passed.

Watermark / GC contract. A tombstone whose delete stamp is ≤ the stability watermark is collectable on every replica, so dropping it cannot lose an edit. This safety property is formally proven (LazilyFormal.CRDT.collectable_implies_observed_everywhere: a collectable stamp is ≤ every member’s observation) and drives the runtime SeqCrdt::gc / TextCrdt::gc_with. A single replica’s local clock is explicitly not a sound watermark; only the version-vector minimum is.

GC scheduling (#lzspecgcdefer). The contract above fixes when a tombstone is collectable; it does not mandate when collection runs. A binding MAY defer GC to an idle window, batch it under memory pressure, or run it incrementally (sweep a bounded number of tombstones per anti-entropy round), provided (a) no tombstone below the watermark is re-examined after reclaim and (b) unbounded accrual is reported via the instrumentation surface. Deferring GC changes only memory footprint, never observable values.

Permission filtering. CrdtSync.filter_readable(peer) drops ops for non-readable nodes entirely (omission, not redaction — like Delta). The frontier advertisement is retained in full: it names peers and stamps, not node content, and the receiver needs the whole frontier to compute a sound watermark.

Status. The wire format, codec round-trips, permission filtering, and point-to-point IpcSink/IpcSource delivery are implemented (#lzcrdtplane5a). Wiring the plane to live merge: crdt root cells (local edits → CrdtOps; remote CrdtOps → ReplicatedCell ingress merge) and BridgeHub fan-out of CrdtSync is the runtime-integration slice (#lzcrdtplane5b).

Delta-CRDT sync (#lzspecdeltacrdt). Today each CrdtOp ships the full converged register state per anti-entropy round (state-based / CvRDT). For LWW/MV registers and PN-counters whose state is small this is acceptable, but for OR-set membership and large register values the full-state ship is wasteful when little changed. The watermark + join algebra already exist (formal/lean/LazilyFormal/CRDT.lean, stampJoin_{comm,assoc,idem}); the #lztextsync pattern (cell-model.md § Delta sync) already proves the version_vector / delta_since(their_vv) / apply_delta triad for text.

This section lifts the same delta pattern to the cell-register plane as an additive, optional control frame:

DeltaSinceRequest = { node: NodeId, their_vv: [(peer, counter)] }

• A receiver of a DeltaSinceRequest responds with a CrdtSync whose ops carry only the states whose stamp is past their_vv (the delta), instead of the full converged state. An empty delta (nothing past their_vv) is a valid response.
• The join is the same semilattice: apply_delta ≡ merge — commutative, associative, idempotent — so a delta is safe to resend and applies in any order.
• A binding that does not implement delta-CRDT sync continues to ship full state; the DeltaSinceRequest frame is opt-in and the receiver falls back to full state when it does not recognize the request. Conformance fixtures exercise both the full-state and the delta-sync paths and assert they converge to the same state (#lzspecdeltacrdt).

Reactive keyed-map sync (#lzfamilysync)

A keyed reactive map (ReactiveMap — its SourceMap / ComputedMap specializations; cell-model.md § “Keyed cell collections”) is a local keyed reactive collection. This section fixes its distributed contract: what a peer does with a keyed CrdtOp (NodeKey = namespace/suffix) for a map entry it has not registered locally.

The base plane, given such an op, resolves the node by NodeKey; if no cell is registered under that key the op is dropped. For a keyed map that is wrong: a key added on one replica would never appear on another, and any derived aggregate over the map (a count of entries) would diverge.

Map-granularity sync closes the gap with materialize-on-ingest: a replica registers a keyed map under a namespace; an inbound keyed op whose first NodeKey segment matches a registered map materializes a fresh entry (a new local NodeId, indexed by the wire NodeKey) seeded from the op’s converged register, then merges. Because the materialized entry is seeded from the op state, materialize-on-ingest is exactly the pointwise CRDT merge, so it inherits the full semilattice convergence.

Contract (proven in lazily-formal FamilySync.lean):

• Materialize, never drop. A keyed op for an absent family entry makes that key present and adopts the op’s value (applyOp_present, applyOp_absent_adopts).
• Membership propagation. After sync a key is present iff it was present on either replica — the union (present_merge). The present set only grows (deferral-not-dealloc); a removed entry is a value-level tombstone, not a dropped key.
• Convergence + idempotence. Materialize-on-ingest equals merging the op’s single-entry state (applyOp_eq_merge), so op delivery is order-independent (applyOp_comm) and re-delivery is a no-op (applyOp_idem).
• Derived-aggregate transparency. Once two replicas converge, any derived count over the keyed map agrees regardless of sync direction/batching (aggregate_converges, aggregate_batch_invariant) — e.g. a live-editor / open-document count converges across editors. A NodeId-churn-stable membership signal drives the recompute so a remote-materialized key is picked up by the derived aggregate.

Conformance: conformance/familysync/materialize_on_ingest.json.

Single-writer effect authority

CRDT convergence covers state. For irreversible external actions (send email, charge card, fire webhook), gate the effect behind a single-writer authority — a designated peer (or small Raft group) decides when the effect fires, at-most-once.

Durable effect sinks (#lzdurablesink)

Durable storage is an effect sink, not a transition authority. While a Lazily runtime is live, transitions are decided from Lazily state; durable storage receives a projection or an ordered fact as an effect, and a sink MUST NOT reload storage to arbitrate the transition it is currently persisting. A projection (latest recoverable state) is an idempotent upsert of the settled epoch from an Effect / AsyncEffect; lossless history uses the existing TopicCell / DurableOutbox drain (append / replay / ack with a stable cursor). Success advances a monotone durable_through(epoch); failure stays represented in live state as pending / retrying / backpressured. Cold loading and migration belong to a separate startup hydrator, never the decision seam. Ephemeral-plane values MUST NOT enter a durable sink — reuse the existing Durable marker. Full authority rule, the projection-vs-history shape table, and the two reference examples (coalesced projection; lossless ordered fact sink) live in docs/durable-sinks.md; the formal backstop is lazily-formal/LazilyFormal/DurableSink.lean.

Reliable Sync (#lzsync)

The Snapshot/Delta and CrdtSync planes above define what is on the wire and how state converges once delivered. They do not define delivery reliability: what a receiver does with a gap, what a sender does with a send that failed, or how a reconnected peer catches up. Today each consumer hand-rolls that loop (and Delta::apply_status → ResyncRequired is a signal with no production handler). This section fixes the reliable-sync protocol so gap recovery, reconnect backfill, and at-least-once delivery are specified and cross-language-conformant, not re-invented per integration.

Layering — mechanism here, policy injected. The three components below are pure protocol: identical logic in every binding, no I/O, no clock, no storage engine. The environment-specific choices — which byte transport, which persistence backend, retry cadence, threading — are supplied by the host application behind the named seams (SnapshotProvider, DurableOutbox store, Clock/scheduler, the IpcSink/IpcSource transport). A binding ships the protocol and a default in-memory backend; the host plugs durable storage and a real transport.

Control frames are IpcMessage variants, not a side channel. ResyncRequest and OutboxAck are two new externally-tagged IpcMessage variants (FFI message kinds 4 / 5), riding the same framed, codec-negotiated, bidirectional message plane as Snapshot/Delta/CrdtSync — the reverse (receiver → sender) direction of that plane. This is deliberate over a separate control type: they share one encode/decode path, one demux point, one FFI kind discriminant, and — because they interleave in the same ordered stream as the deltas — a well-defined in-band position (an OutboxAck { through_epoch: N } is meaningful relative to the deltas already sent on that channel). The liveness ops are CrdtOps on the existing CrdtSync variant. A binding MUST add both variants to its IpcMessage enum and its FFI message-kind mapping.

Codec. Every reliable-sync frame (the two control variants and the liveness CrdtOps) is an ordinary framed message on the negotiated codec. Per § Frame codecs the cross-language boundary negotiates msgpack (self-describing, evolution-safe, named-field), with json as the required reference codec; postcard stays the Rust-only fast path. Conformance requires every new frame to round-trip through both json and msgpack (semantic round-trip, not byte-identical, for the map codecs), the same discipline the three prior IpcMessage variants already hold.

ResyncCoordinator (#resync-coord)

A pure receiver-side decision function over the inbound frame stream. It holds one piece of state per source — last_epoch (the highest epoch this receiver has fully applied) — and classifies each inbound Snapshot/Delta:

enum ResyncAction { Apply, RequestSnapshot { from: u64 }, Ignore }

// pure; no I/O. `ingest` inspects a frame and returns the action; the caller performs it.
fn ingest(&mut self, msg: &IpcMessage) -> ResyncAction

Decision table (given receiver last_epoch = L):

• RequestSnapshot { from } is emitted at most once per detected gap; a coordinator that has already requested and not yet applied a covering Snapshot suppresses duplicate requests for the same gap (it stays in a resyncing sub-state, Ignore-ing further deltas until the snapshot lands). This bounds request storms under a burst of ahead-of-cursor deltas.
• Convergence guarantee. A receiver that drops an arbitrary suffix of deltas, then applies the resync Snapshot, reaches the same graph state as one that saw every delta — gap recovery is state-equivalent, not lossy (proven ReliableSync.resync_convergence). This holds because a Snapshot is a full-state frame, not an incremental one.
• Idempotent re-delivery. A Delta with base_epoch < L (a frame the receiver already folded, re-sent by the outbox) is Ignored, so at-least-once delivery yields exactly-once effect.

The application supplies snapshots for the sender side of a resync via:

trait SnapshotProvider { fn snapshot(&self, from_epoch: u64) -> IpcMessage; }  // returns Snapshot { epoch >= from_epoch }

DurableOutbox (#durable-outbox)

The sender-side contract that makes delivery at-least-once across a crash/reconnect. Today a failed send leaves a permanent gap (the out-epoch is bumped before the send; a reconnect is a fresh peer at epoch 0 with no backfill). The outbox closes that: every frame is durably recorded before it is sent, retained until the peer proves receipt, and replayed from the peer’s cursor on reconnect.

trait DurableOutbox {
    fn append(&mut self, epoch: u64, msg: &IpcMessage);          // MUST persist before the send is attempted
    fn ack_through(&mut self, epoch: u64);                        // peer proved receipt through `epoch`; retained frames <= epoch may be pruned
    fn replay_from(&self, cursor: u64) -> impl Iterator<Item = (u64, IpcMessage)>;  // frames with epoch > cursor, in epoch order
    fn retained_depth(&self) -> usize;                           // unacked queue depth — the backpressure fill level (Progress.retained)
    fn coalesce_to_snapshot(&mut self, epoch: u64, snapshot: &IpcMessage) -> bool { false }  // state cells: replace the unacked suffix with one snapshot; op-log frames decline (false)
}

Normative contract:

• Append-before-send. A frame MUST be durably appended before it is handed to the transport. If the process dies between append and a confirmed send, the frame is still in the outbox and is replayed on reconnect. (The pre-send epoch bump that caused the permanent-gap bug is replaced by: append at epoch, send, and only ack_through retires it.)
• Replay-from-cursor. On (re)connect the peer advertises the highest epoch it has applied (its ResyncCoordinator.last_epoch, carried in the reconnect handshake or an OutboxAck); the sender replay_from(cursor) re-sends every retained frame with epoch > cursor in order. A frame the peer already applied (base_epoch < last_epoch) is Ignored by the coordinator — replay is safe.
• At-least-once ⇒ exactly-once effect. Replay delivers every op at least once; idempotent apply (the coordinator’s re-delivery Ignore + the CRDT/PartialEq guards) makes the net effect exactly-once — no lost op, no doubled op (proven ReliableSync.outbox_at_least_once_exactly_once_effect).
• Ack semantics. ack_through(e) is a retention signal (safe to prune <= e), never a delivery-success authority for a domain effect (that is a causal receipt). An outbox MAY prune lazily; correctness does not depend on prompt pruning, only on not pruning un-acked frames.
• OutboxAck frame. The receiver periodically (or on request) sends OutboxAck { through_epoch: u64 } — a new framed IpcMessage — so the sender can advance retention and so a reconnect handshake can carry the resume cursor.
• Coalescing (optional, element-algebra-gated). An outbox MAY bound its retained depth without dropping an op, per § Backpressure & outbox coalescing. A state outbox (LWW/OR-set/counter/graph frames) collapses the unacked suffix to one Snapshot via coalesce_to_snapshot (memory-bounded — the coalesce is the cell’s own join, e.g. LWW → last value, proven ReliableSync.coalesce_by_join_sound / coalesce_to_snapshot_state_equiv). An op-log outbox (QueueCell frames) declines snapshot-coalesce (returns false) and instead fuses a run of same-direction ops into one batch frame (framing-bounded, order-preserving, ReliableSync.batch_fusion_state); it relies on source-side QueueCell.is_full for memory bounding. Coalescing is a retention optimization only — it never changes which effects the receiver observes.

Bindings ship an InMemoryOutbox (default; correct within a process lifetime) and a reference file-backed impl for tests/conformance (proves the crash-replay path deterministically). The host plugs its own durable store (agent-doc: SQLite) behind the same trait; the cursor math is protocol, the storage is not.

SyncDriver (#sync-driver)

The loop shape that wires an outbound producer to a transport through the outbox, and drives resync on reconnect. It owns no clock and no runtime: the host calls tick() from its own scheduler, so the driver stays a pure state machine with injected seams.

struct SyncDriver<S: IpcSink, R: IpcSource, O: DurableOutbox, C: Clock> { /* transport, outbox, coordinator, clock */ }

impl SyncDriver {
    // One scheduler-driven step. Returns Progress (sent N, applied M, resynced) or a DriverError.
    fn tick(&mut self) -> Result<Progress, DriverError>;
}

tick() performs, in order:

1. Drain inbound. Pull available frames from IpcSource; feed each to ResyncCoordinator.ingest and perform the returned action (Apply into the local graph, emit a ResyncRequest / OutboxAck, or drop). Advance last_epoch on applied frames.
2. Send outbound. For each new local flush, outbox.append(epoch, frame) then IpcSink.send(frame). A send error does not unwind the driver and does not lose the frame: the frame stays in the outbox, the driver records the transport as degraded, and the send is retried from the outbox on a later tick (cadence/backoff is the injected Clock’s policy).
3. Resync on reconnect. When the transport reports a fresh/reopened peer, exchange cursors (peer’s OutboxAck.through_epoch) and replay_from(cursor); if the local receiver is behind, emit its ResyncRequest.
4. Retention. On an inbound OutboxAck, outbox.ack_through(through_epoch).

Contract:

• No frame lost on send failure. The append-before-send + retain-on-error rule means a frame is delivered on a subsequent tick once the transport recovers (the exact bug the current ?-propagating poll has, where a failed send bumps the epoch and unwinds).
• Bounded work per tick. tick() does a bounded amount of drain/send work and returns; the host controls cadence. No internal blocking, no async runtime baked in.
• Injected clock/transport. Retry cadence, backoff, and “is the peer fresh” come from the injected Clock and transport signals — policy stays in the host, mechanism in the driver.
• Backpressure is host policy, not driver mechanism. The driver does not bound its outbound staging or block the producer: enqueue is unbounded and the DurableOutbox retains every unacked frame until the peer’s OutboxAck (this is the at-least-once durability guarantee — a frame is not dropped to relieve pressure). Instead the driver exposes the signals a host uses to apply backpressure itself: the stall state (is_stalled / stalled_for) and the retained-outbox depth (Progress.retained). A host bounds memory by (a) rate-limiting or coalescing enqueues off those signals — a re-emit at an already-accepted epoch is an idempotent no-op delta, so coalescing is the natural limiter — and (b) choosing a DurableOutbox that spills to durable storage rather than RAM (e.g. a SQLite-backed outbox), so a long-stalled peer grows disk, not heap. A bounded outbox with an is_full / high-watermark cap, and the per-item coalesce modes that keep it bounded without shedding an op, are specified in § Backpressure & outbox coalescing.

IpcSink/IpcSource are the existing abstract transport traits (feature ipc); the byte carrier is any DataChannel. Un-gating: the driver and the BridgeHub fan-out it can wrap depend only on these abstract ipc traits, so they MUST be usable without the webrtc feature (a caller supplying a Unix-domain-socket DataChannel gets reliable sync with no WebRTC dependency). The per-document channel decision (one driver/transport per document vs one hub with document_hash+NodeKey namespacing) is a host concern; the pull-only consumer path may not need BridgeHub fan-out at all.

Backpressure & outbox coalescing (#lzsync-backpressure)

The unacked outbox is a bounded cursor-queue, and that framing makes backpressure a queue property rather than a bolt-on: append is a push to the tail, OutboxAck.through_epoch is the consumer cursor, replay_from is a FIFO peek of the unacked suffix, and the retained depth (Progress.retained) is the fill level. A peer that stops acking is a consumer that stops advancing its cursor, so the queue fills — and a bounded outbox surfaces that as an is_full / high-watermark signal a host uses to throttle the producer. Recovery is the reactive dual: an OutboxAck advances the cursor, the queue drains below the watermark, and the fill signal clears so the producer resumes — the same reactive backpressure the QueueCell model pins (queuecell_bounded_backpressure), applied to the outbox. Non-ack is backpressure; the liveness cells disambiguate a slow consumer (queue fills — wait) from a dead one (queue drains — reconnect + replay). Formalized as ReliableSync.outbox_is_bounded_queue (enqueue grows depth by one, ack dequeues the acked front FIFO, a coalesced suffix is one frame).

A bounded queue must not grow unbounded under a persistently-slow peer, and the outbox stays bounded by coalescing its unacked suffix — never by dropping an op. How it coalesces is dispatched by the element’s merge algebra, not by a single global switch. Every cell type supplies its own coalesce, and each falls into one of two families by whether the type has an idempotent join:

The unifying law: coalesce = the element’s semilattice join folded over the unacked suffix.

• Join / snapshot coalesce (idempotent cells: LWW, OR-set, counter, graph). The suffix collapses to one merged value — order-, regroup-, and retry-independent (ReliableSync.coalesce_by_join_sound; for the whole-graph frame, adopting the snapshot subsumes the dropped deltas — ReliableSync.coalesce_to_snapshot_state_equiv). This bounds memory: a peer arbitrarily far behind costs one frame, not the whole backlog. It is the CRDT answer to “don’t block the producer” — the producer keeps appending; the queue keeps collapsing. LWW-to-last-value is exactly the join being max-stamp.
• Batch-fusion coalesce (op-log cells: QueueCell). A queue has no idempotent join — order and multiplicity are the value — so it cannot collapse; it only fuses a run of same-direction ops (QueuePush(a); QueuePush(b); QueuePush(c) → one atomic batch Delta, the op-log delta form of § QueueCell op-log delta form). Lossless and order-preserving (ReliableSync.batch_fusion_state; a fused multi-epoch delta equals its expanded unit run, multi_epoch_apply_eq_fold). This bounds frame count and per-frame overhead (one header, one codec envelope, one reactive invalidation on apply), not memory — a queue cannot drop elements and stay a queue. An op-log sync therefore still needs source-side try_push → Full (QueueCell.is_full) to bound memory; batch-fusion complements it, it does not replace it. Fuse only runs of same-direction ops; do not fuse across a pop in a bidirectional log.

Rule of thumb: a state sync (LWW/OR-set/counter/graph) absorbs pressure by collapsing (memory-bounded, never blocks the producer); an op-log sync (QueueCell) absorbs it by rejecting at the source (is_full, blocks the producer) and may fuse frames to cut overhead. Both keep every accepted op’s effect; neither sheds load silently.

Bounding producer memory (op-log). is_full / try_push → Full bounds the queue, not the producer: if the producer answers Full by stashing the rejected item in an unbounded side-buffer, the queue is bounded but memory is not — the backlog just moved up one hop. A QueueCell sync bounds producer memory only when the Full signal terminates at a stoppable or sheddable source, and no hop in between holds an unbounded buffer:

• Suspend (the lazily-native path). The producer is a reactive effect that reads is_full; while full it does not run, and the pop that clears full (true→false) invalidates the reader and re-fires it. Producer memory is bounded because a not-running effect holds no backlog — it generates on demand, gated by the queue. This is the queuecell_bounded_backpressure loop used as a producer gate rather than a mere status read.
• Propagate upstream. An imperative producer fed by its own bounded input returns Full/pending to its source, recursively, until the chain reaches something that can actually stop (a pull-based reader; a socket whose reads pause, so TCP advertises a zero window and the remote sender stops). Every hop is bounded-and-backpressuring; the stop propagates to the origin.
• Shed. When the source cannot stop (a real-time feed, an external peer that will not slow), the only way to bound memory is an overflow drop policy — drop-oldest / drop-newest, the non-reject QueueStorage backends the QueueCell model names — or a lossy summary. Dropping is a deliberate, observable choice, not silent truncation.

The invariant: backpressure bounds memory only if it ends at a stoppable or sheddable source; an unbounded buffer at any hop defeats it. The queue supplies the signal and the bound at the queue; the producer must convert that signal into actually-not-generating (suspend/propagate) or actually-discarding (shed) — never into unbounded local absorption. (A state cell escapes this because its coalesce is an unbounded-absorption-that-stays-bounded: churn collapses into the join. A queue has no such join, which is exactly why its producer must pause or drop.)

Two seam refinements this makes explicit, both host-invisible in the current traits:

• Ack-as-credit. For non-ack to mean consumer backpressure (not merely non-receipt), a receiver SHOULD gate its OutboxAck.through_epoch on its consumer’s drain cursor, not on mere fold-into-projection — otherwise a backed-up consumer keeps acking and the credit signal never forms. The unacked depth then behaves as a sliding credit window; withholding the ack pushes back end-to-end onto the sender’s outbox.
• Sink would-block. IpcSink::send returning only Ok/Err cannot express a transport that is up but momentarily full (kernel socket buffer, DataChannel.bufferedAmount); that fullness is a distinct layer from consumer-slowness and is invisible to the ack. A binding MAY widen the sink outcome to distinguish Full (re-stage the frame + back off — not a reconnect) from a hard failure. This is the one backpressure axis the ack cursor structurally cannot cover.

Transport seam (IpcSink / IpcSource, #lzsync-transport-seam)

The SyncDriver is generic over exactly two host-supplied seams. Every binding that ports the driver MUST provide the same two-method contract so the loop above is identical across languages; the seams are the injected boundary the design assigns to the host (“which socket” is a deployment choice), so they carry no wire form of their own — what crosses the wire is the codec-encoded IpcMessage frame (msgpack is the cross-language default; see § Frame codecs). A binding names them idiomatically (Rust traits, Kotlin/TS interfaces); the semantics are normative:

// Outbound: deliver exactly one already-encoded protocol frame.
trait IpcSink   { fn send(&mut self, msg: &IpcMessage) -> Result<(), SinkError>; }
// Inbound: poll for the next frame without blocking.
trait IpcSource { fn recv(&mut self) -> Result<Option<IpcMessage>, SourceError>; }

• send MAY fail and MAY be lossy. A send error means the frame was not durably handed to the peer. At-least-once is a driver property, not a sink property: on a send error the driver keeps the frame in the DurableOutbox and replays it after the next reconnect. A sink is therefore free to be a plain best-effort write (one connect-send-receipt on a Unix socket, one DataChannel frame, …) — it never has to buffer or retry, because the outbox already does.
• recv is poll, not block. Ok(None) means the source is currently exhausted or closed; the driver treats it as “no inbound progress this tick” and returns — it never parks a thread on the source (cadence is the host’s Clock/scheduler policy). Ok(Some(frame)) yields one frame.
• A recv Err is the reconnect signal. A source read failure surfaces from tick() as DriverError::Source; the host re-establishes the byte carrier and calls on_reconnect(), after which the next tick() replays the unacked outbox suffix from the peer ack cursor and re-advertises the receiver cursor. (A sink failure, by contrast, is retain-and-stall, not a DriverError — it is reported through Progress/stall signals so the host can back off.)

Because the seam has no wire representation, it adds no conformance fixture: the reliable-sync fixtures already pin the driver’s observable behavior (gap→resync convergence, outbox replay, idempotent redelivery) at the message-sequence level, which is the correct abstraction — the seam sits deliberately below it. This is also why the seam is not formalized in ReliableSync.lean: “send/receive a frame” has no algebraic content to prove; the invariants that matter (resync_convergence, outbox_at_least_once_exactly_once_effect, the liveness lattice joins) are proven over frame sequences, above the transport.

Liveness cells: OR-set and LWW (#lzsync-liveness)

Cross-process liveness — “editor pid X has doc Y open”, “pid X holds the owner lease” — is carried as CRDT cells on the CrdtSync plane, not as a bespoke frame, so it inherits that plane’s idempotent, frontier-resumable, re-delivery-safe convergence. Two register shapes cover the liveness needs:

• OR-set membership — the open-set of (doc, pid) presence. An observed-remove set: a (doc, pid) is present iff some add-tag for it is not shadowed by a remove-tag that observed that add. This gives the exact “add wins over a concurrent stale remove” bias liveness needs (a re-open concurrent with a lagging close keeps the doc open), and re-delivery of an add/remove is a lattice join → idempotent. Whole-editor death removes every (doc, pid) for that pid.
• LWW liveness flag — a per-pid alive: bool and the owner lease as HLC-stamped last-writer-wins registers (the CRDT plane’s default register, § Cell register types). The OS process-exit event writes alive[pid] = false; the highest-stamp write wins, and a stale re-assert is dominated.

Normative semantics:

• Frontier-resumable. A liveness op that fails to send while the peer is down is re-sent on reconnect from the CrdtSync.frontier (the plane is already “safe to resend”); no liveness state is lost across a disconnect. This is what lets the open-set/lease survive a controller recycle without the editor re-announcing.
• Derived authority is reactive. “Is doc Y live” = any present (doc, pid) in the OR-set whose alive[pid] is true — a derived aggregate over the liveness keyed map (the #lzfamilysync materialize-on-ingest + derived-count contract). One alive[pid] = false write fans out to every doc that pid held (whole-editor death cascade), reactively.
• Idempotent + convergent. OR-set join and LWW join are semilattice joins, so out-of-order, duplicated, or batched delivery all converge and re-delivery is a no-op (proven ReliableSync.crdt_liveness_convergence_under_retry, building on the existing CRDT lattice proofs).
• Per-doc isolation. Liveness keys are namespaced (document_hash, …) like every other keyed op, so a stale overlay for doc B cannot flip doc A’s authority.

Partition & eviction (#lzsync-partition-eviction)

A slow peer, a partitioned peer, and a dead peer are three different states, and dropping a peer is the last rung of an escalation ladder — never the first response to a missed ack. This section fixes when a peer is dropped, how the network is isolated from one bad peer, and how a dropped peer rejoins.

Per-peer outbox isolation (normative). In a multi-peer fan-out each peer MUST have its own DurableOutbox and ack cursor. A single shared outbox would make the slowest peer the network’s pace-setter (head-of-line blocking) and let one partition stall every peer. With a per-peer outbox, a slow or partitioned peer fills only its own cursor-queue; fast peers are untouched, and the drop decision is per-peer, not network-wide. This is what lets backpressure (§ Backpressure & outbox coalescing) be contained rather than contagious.

Escalation ladder. A degraded peer is handled in this order; each rung is exhausted before the next:

Eviction is gated on the liveness lease, not on missed acks. A peer is dropped only when its OR-set / LWW liveness lease expires (the partition/death signal) — or, for a persistently-slow op-log peer, when its own bounded outbox is exceeded and neither coalescing (a queue cannot state-supersede coalesce) nor producer-suspension (the source cannot stop) can bound it. Eviction MUST be observable (it removes the peer’s (doc, pid) presence, a visible OR-set remove), never silent. A state peer effectively never reaches rung 4 on slowness alone: coalescing collapses its backlog to one frame, so a slow state peer costs one snapshot, not an eviction.

A returning peer rejoins as fresh. An evicted peer that reconnects is a fresh receiver (state empty, last_epoch = 0): it MUST full-resync by adopting a Snapshot, not replay from a stale cursor (its retained frames were reclaimed on eviction). Convergence is lossless — the fresh receiver reaches the sender’s full state (ReliableSync.evicted_peer_resyncs_fresh, a corollary of resync_convergence). The OR-set add-wins-over-stale-remove bias (ReliableSync.orset_add_wins_over_stale_remove) protects the race where a peer returns just as its lease expires: the rejoin add is not shadowed by the lagging eviction remove, so a peer that is coming back is not wrongly dropped.

Partition rule differs for queues (CAP). Because a queue’s total order is authoritative (a single sequencer in SPSC) and has no idempotent join, divergent queue order across a partition cannot losslessly converge — a queue cannot be AP-and-lossless. So a distributed (consensus-backed) queue favors CP under partition: the minority side (no quorum) blocks writes rather than dropping the peer — it refuses writes it could not later reconcile, and rejoins the majority order on heal. You do not “drop the partition”; you decline minority writes and evict individual peers only on lease expiry. State cells (LWW/OR-set) are the opposite: their join converges, so they MAY stay AP — accept writes on both sides of the partition and merge on heal. This is why distribution of a QueueCell is a consensus storage-backend property (the distributed-queue PRD / RaftQueueStorage), while liveness/register cells distribute on the plain CrdtSync plane. See § QueueCell op-log delta form.

Conformance

New fixtures under conformance/reliable-sync/ pin the protocol cross-language (rs/js/kt):

Every fixture’s frames MUST round-trip through both json and msgpack. The ResyncCoordinator, DurableOutbox, and liveness models are the shared cross-language pins; lazily-formal ReliableSync.lean is the correctness backstop the implementations must match.

Permission Boundary (RemoteOp)

Only nodes on the per-peer allowlist are serialized into a snapshot or delta. Non-allowlisted nodes are omitted entirely (not even as Opaque).

RemoteOp

RemoteOp = { kind: OpKind, node: NodeId }
OpKind = "read" | "write" | "trigger_effect"

• Three kinds are gated independently: a read grant never implies write or effect-trigger.
• PeerPermissions is default-deny per-peer allowlist.
• filter_readable(peer, nodes) drops non-readable nodes from results before serialization.