lazily-spec

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

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

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

Protocol Layers

Wire Format

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

Schema Format

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

Relationship to lazily-rs SPEC.md

This repo extracts the wire-protocol and cross-language compatibility sections from lazily-rs/SPEC.md into a standalone reference. Rust-specific internals (Context, ThreadSafeContext, lock strategy, benchmarks) remain in the Rust crate.

Versioning

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

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. JavaScript/TypeScript peers must keep values at or below Number.MAX_SAFE_INTEGER (2^53).

IpcPayload

Opaque serialized value bytes. The producing language owns type-aware encoding through stable type_tag strings; the channel only moves bytes.

IpcPayload = { type_tag: string, bytes: base64-string }

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.

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.
• Deltas are strictly sequential. A receiver detects gaps, reorders, or sender restarts by checking base_epoch == last_epoch.

Snapshot

{
  "type": "snapshot",
  "epoch": 0,
  "nodes": [
    { "slot_id": 0, "type_tag": "i32", "state": "resolved", "payload": "base64..." }
  ],
  "edges": [
    { "dependent": 1, "dependency": 0 }
  ],
  "roots": [0]
}

NodeSnapshot

{
  "slot_id": 0,
  "type_tag": "i32",
  "state": "resolved",
  "payload": "base64..."
}

EdgeSnapshot

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

Delta

{
  "type": "delta",
  "base_epoch": 0,
  "epoch": 1,
  "ops": [
    { "op": "cell_set", "slot_id": 0, "payload": "base64..." },
    { "op": "slot_value", "slot_id": 1, "payload": "base64..." },
    { "op": "invalidate", "slot_id": 2 },
    { "op": "node_add", "slot_id": 3, "type_tag": "string", "payload": "base64..." },
    { "op": "node_remove", "slot_id": 4 },
    { "op": "edge_add", "dependent": 5, "dependency": 0 },
    { "op": "edge_remove", "dependent": 5, "dependency": 0 }
  ]
}

DeltaOp variants

Consistency invariants

• PartialEq cell guard: An equal set_cell emits no cell_set and no downstream ops.
• Memo equality suppression: A dirty memo() that recomputes to an equal value emits no slot_value 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 slot_value 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 slot_value 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 slot_value 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 slot_values. 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.

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.

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

Shared-memory IPC

ShmBlobArena provides the shared-memory payload path:

• 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.

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"]
}

If peers disagree on protocol_major_version, codec, ordered_reliable, or required features, they fail closed before applying any Snapshot or Delta.

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.

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;

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

Cell register types

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.

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.

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.

Conformance Fixtures

The conformance/ directory contains canonical test fixtures that all IPC-capable bindings must validate against. Each binding’s CI should deserialize the wire field, run the assertions, and re-serialize to confirm round-trip fidelity.

Fixture schema

{
  "description": "Human-readable summary",
  "protocol_version": 1,
  "kind": "Snapshot" | "Delta",
  "assertions": { "…language-agnostic field checks…" },
  "wire": { "…IpcMessage as serde_json…" }
}

Current fixtures

Adding a new binding

Copy the fixture-loading pattern from lazily-rs/tests/conformance.rs. Each test should:

1. Load the fixture.
2. Parse the wire field into the binding’s native IpcMessage type.
3. Assert the assertions fields.
4. Re-serialize and compare for byte-for-byte round-trip fidelity.

Examples

snapshot_minimal.json

{
  "description": "Minimal snapshot with one payload node and no edges",
  "protocol_version": 1,
  "kind": "Snapshot",
  "assertions": {
    "epoch": 1,
    "node_count": 1,
    "edge_count": 0,
    "root_count": 1,
    "first_node_type_tag": "i32"
  },
  "wire": {
    "Snapshot": {
      "epoch": 1,
      "nodes": [
        {
          "node": 1,
          "type_tag": "i32",
          "state": {
            "Payload": [1, 2, 3, 4]
          }
        }
      ],
      "edges": [],
      "roots": [1]
    }
  }
}

snapshot_multi_node.json

{
  "description": "Snapshot with payload nodes, opaque node, edges, and roots",
  "protocol_version": 1,
  "kind": "Snapshot",
  "assertions": {
    "epoch": 7,
    "node_count": 3,
    "edge_count": 2,
    "root_count": 2,
    "has_opaque_node": true,
    "opaque_node_id": 3
  },
  "wire": {
    "Snapshot": {
      "epoch": 7,
      "nodes": [
        {
          "node": 1,
          "type_tag": "i32",
          "state": {
            "Payload": [1, 2, 3]
          }
        },
        {
          "node": 2,
          "type_tag": "f64",
          "state": {
            "Payload": [0, 0, 0, 0, 0, 0, 240, 63]
          }
        },
        {
          "node": 3,
          "type_tag": "opaque-type",
          "state": "Opaque"
        }
      ],
      "edges": [
        { "dependent": 2, "dependency": 1 },
        { "dependent": 3, "dependency": 1 }
      ],
      "roots": [1, 2]
    }
  }
}

snapshot_shared_blob.json

{
  "description": "Snapshot with a shared-blob node referencing shared memory",
  "protocol_version": 1,
  "kind": "Snapshot",
  "assertions": {
    "epoch": 9,
    "node_count": 1,
    "edge_count": 0,
    "root_count": 1,
    "first_node_state_kind": "SharedBlob",
    "blob_offset": 0,
    "blob_len": 16,
    "blob_epoch": 9
  },
  "wire": {
    "Snapshot": {
      "epoch": 9,
      "nodes": [
        {
          "node": 7,
          "type_tag": "text/plain",
          "state": {
            "SharedBlob": {
              "offset": 0,
              "len": 16,
              "generation": 1,
              "epoch": 9,
              "checksum": 123456789
            }
          }
        }
      ],
      "edges": [],
      "roots": [7]
    }
  }
}

delta_sequential.json

{
  "description": "Sequential delta covering all 7 DeltaOp variants",
  "protocol_version": 1,
  "kind": "Delta",
  "assertions": {
    "base_epoch": 40,
    "epoch": 41,
    "is_sequential": true,
    "op_count": 7,
    "has_all_op_variants": true
  },
  "wire": {
    "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 } }
      ]
    }
  }
}

delta_non_sequential.json

{
  "description": "Non-sequential delta with gap (requires resync)",
  "protocol_version": 1,
  "kind": "Delta",
  "assertions": {
    "base_epoch": 12,
    "epoch": 13,
    "is_sequential": true,
    "resync_after_epoch_10": true
  },
  "wire": {
    "Delta": {
      "base_epoch": 12,
      "epoch": 13,
      "ops": []
    }
  }
}

delta_shared_blob.json

{
  "description": "Delta with shared-blob payload referencing shared memory",
  "protocol_version": 1,
  "kind": "Delta",
  "assertions": {
    "base_epoch": 8,
    "epoch": 9,
    "op_count": 1,
    "first_op_kind": "SlotValue",
    "first_op_payload_kind": "SharedBlob"
  },
  "wire": {
    "Delta": {
      "base_epoch": 8,
      "epoch": 9,
      "ops": [
        {
          "SlotValue": {
            "node": 7,
            "payload": {
              "SharedBlob": {
                "offset": 40,
                "len": 17,
                "generation": 2,
                "epoch": 9,
                "checksum": 987654321
              }
            }
          }
        }
      ]
    }
  }
}

JSON Schemas

Schemas are provided as JSON Schema (Draft 2020-12). Each implementation must validate against these schemas. The JSON representation of the wire format is normative; future binary codecs encode the same shapes.

snapshot.json

{
  "$schema": "https://json-schema.org/draft/2020-12/schema",
  "$id": "https://lazily.dev/schemas/snapshot.json",
  "title": "Snapshot",
  "description": "Full graph state message for lazily-IPC",
  "type": "object",
  "properties": {
    "type": { "const": "snapshot" },
    "epoch": { "type": "integer", "minimum": 0, "description": "Current IPC epoch" },
    "nodes": {
      "type": "array",
      "items": { "$ref": "#/$defs/NodeSnapshot" },
      "description": "All serialized nodes"
    },
    "edges": {
      "type": "array",
      "items": { "$ref": "#/$defs/EdgeSnapshot" },
      "description": "Dependency edges"
    },
    "roots": {
      "type": "array",
      "items": { "type": "integer", "minimum": 0 },
      "description": "Cell and source slot IDs"
    }
  },
  "required": ["type", "epoch", "nodes", "edges", "roots"],
  "additionalProperties": false,
  "$defs": {
    "NodeSnapshot": {
      "type": "object",
      "properties": {
        "slot_id": { "type": "integer", "minimum": 0 },
        "type_tag": { "type": "string", "description": "Stable cross-process type key" },
        "state": {
          "type": "string",
          "enum": ["resolved", "dirty", "unset"],
          "description": "Node state"
        },
        "payload": {
          "type": ["string", "null"],
          "contentEncoding": "base64",
          "description": "Serialized value (null if unset)"
        }
      },
      "required": ["slot_id", "type_tag", "state"],
      "additionalProperties": false
    },
    "EdgeSnapshot": {
      "type": "object",
      "properties": {
        "dependent": { "type": "integer", "minimum": 0 },
        "dependency": { "type": "integer", "minimum": 0 }
      },
      "required": ["dependent", "dependency"],
      "additionalProperties": false
    }
  }
}

delta.json

{
  "$schema": "https://json-schema.org/draft/2020-12/schema",
  "$id": "https://lazily.dev/schemas/delta.json",
  "title": "Delta",
  "description": "Incremental change set for lazily-IPC",
  "type": "object",
  "properties": {
    "type": { "const": "delta" },
    "base_epoch": {
      "type": "integer",
      "minimum": 0,
      "description": "Epoch this delta applies to"
    },
    "epoch": {
      "type": "integer",
      "minimum": 0,
      "description": "New epoch (must equal base_epoch + 1)"
    },
    "ops": {
      "type": "array",
      "items": { "$ref": "#/$defs/DeltaOp" },
      "description": "Ordered operations"
    }
  },
  "required": ["type", "base_epoch", "epoch", "ops"],
  "additionalProperties": false,
  "$defs": {
    "DeltaOp": {
      "oneOf": [
        {
          "type": "object",
          "title": "CellSet",
          "properties": {
            "op": { "const": "cell_set" },
            "slot_id": { "type": "integer", "minimum": 0 },
            "payload": {
              "type": "string",
              "contentEncoding": "base64",
              "description": "Serialized cell value"
            }
          },
          "required": ["op", "slot_id", "payload"],
          "additionalProperties": false
        },
        {
          "type": "object",
          "title": "SlotValue",
          "properties": {
            "op": { "const": "slot_value" },
            "slot_id": { "type": "integer", "minimum": 0 },
            "payload": {
              "type": "string",
              "contentEncoding": "base64",
              "description": "Serialized slot value"
            }
          },
          "required": ["op", "slot_id", "payload"],
          "additionalProperties": false
        },
        {
          "type": "object",
          "title": "Invalidate",
          "properties": {
            "op": { "const": "invalidate" },
            "slot_id": { "type": "integer", "minimum": 0 }
          },
          "required": ["op", "slot_id"],
          "additionalProperties": false
        },
        {
          "type": "object",
          "title": "NodeAdd",
          "properties": {
            "op": { "const": "node_add" },
            "slot_id": { "type": "integer", "minimum": 0 },
            "type_tag": { "type": "string" },
            "payload": {
              "type": ["string", "null"],
              "contentEncoding": "base64"
            }
          },
          "required": ["op", "slot_id", "type_tag"],
          "additionalProperties": false
        },
        {
          "type": "object",
          "title": "NodeRemove",
          "properties": {
            "op": { "const": "node_remove" },
            "slot_id": { "type": "integer", "minimum": 0 }
          },
          "required": ["op", "slot_id"],
          "additionalProperties": false
        },
        {
          "type": "object",
          "title": "EdgeAdd",
          "properties": {
            "op": { "const": "edge_add" },
            "dependent": { "type": "integer", "minimum": 0 },
            "dependency": { "type": "integer", "minimum": 0 }
          },
          "required": ["op", "dependent", "dependency"],
          "additionalProperties": false
        },
        {
          "type": "object",
          "title": "EdgeRemove",
          "properties": {
            "op": { "const": "edge_remove" },
            "dependent": { "type": "integer", "minimum": 0 },
            "dependency": { "type": "integer", "minimum": 0 }
          },
          "required": ["op", "dependent", "dependency"],
          "additionalProperties": false
        }
      ]
    }
  }
}

ffi.json

{
  "$schema": "https://json-schema.org/draft/2020-12/schema",
  "$id": "https://lazily.dev/schemas/ffi.json",
  "title": "FFI Types",
  "description": "C ABI types for the lazily FFI boundary",

  "$defs": {
    "LazilyFfiBytes": {
      "type": "object",
      "description": "Owned byte buffer crossing the FFI boundary",
      "properties": {
        "ptr": { "type": "integer", "minimum": 0, "description": "Pointer to byte buffer" },
        "len": { "type": "integer", "minimum": 0, "description": "Buffer length in bytes" }
      },
      "required": ["ptr", "len"],
      "additionalProperties": false
    },
    "LazilyFfiStatus": {
      "type": "integer",
      "enum": [0, 1, 2, 3, 4, 5],
      "description": "FFI operation status code",
      "oneOf": [
        { "const": 0, "title": "Ok" },
        { "const": 1, "title": "Empty" },
        { "const": 2, "title": "NullPointer" },
        { "const": 3, "title": "InvalidMessage" },
        { "const": 4, "title": "EncodeFailed" },
        { "const": 5, "title": "Panic" }
      ]
    },
    "LazilyFfiMessageKind": {
      "type": "integer",
      "enum": [0, 1, 2],
      "description": "IPC message kind discriminator",
      "oneOf": [
        { "const": 0, "title": "Unknown" },
        { "const": 1, "title": "Snapshot" },
        { "const": 2, "title": "Delta" }
      ]
    }
  }
}

signaling.json

{
  "$schema": "https://json-schema.org/draft/2020-12/schema",
  "$id": "https://lazily.dev/schemas/signaling.json",
  "title": "Signaling Protocol",
  "description": "WebSocket signaling frames for lazily peer discovery",
  "$comment": "Validates both client→server and server→client frames",

  "oneOf": [
    {
      "title": "ClientMessage",
      "oneOf": [
        {
          "type": "object",
          "title": "Join",
          "properties": {
            "type": { "const": "join" },
            "peer": { "type": "integer", "minimum": 0, "maximum": 9007199254740991 },
            "capabilities": { "type": "array", "items": { "type": "string" } }
          },
          "required": ["type", "peer"],
          "additionalProperties": false
        },
        {
          "type": "object",
          "title": "Offer",
          "properties": {
            "type": { "const": "offer" },
            "to": { "type": "integer", "minimum": 0 },
            "sdp": { "type": "string" }
          },
          "required": ["type", "to", "sdp"],
          "additionalProperties": false
        },
        {
          "type": "object",
          "title": "Answer",
          "properties": {
            "type": { "const": "answer" },
            "to": { "type": "integer", "minimum": 0 },
            "sdp": { "type": "string" }
          },
          "required": ["type", "to", "sdp"],
          "additionalProperties": false
        },
        {
          "type": "object",
          "title": "Ice",
          "properties": {
            "type": { "const": "ice" },
            "to": { "type": "integer", "minimum": 0 },
            "candidate": { "type": "string" }
          },
          "required": ["type", "to", "candidate"],
          "additionalProperties": false
        },
        {
          "type": "object",
          "title": "Relay",
          "properties": {
            "type": { "const": "relay" },
            "to": { "type": "integer", "minimum": 0 },
            "payload": {}
          },
          "required": ["type", "to", "payload"],
          "additionalProperties": false
        },
        {
          "type": "object",
          "title": "Leave",
          "properties": {
            "type": { "const": "leave" }
          },
          "required": ["type"],
          "additionalProperties": false
        }
      ]
    },
    {
      "title": "ServerMessage",
      "oneOf": [
        {
          "type": "object",
          "title": "Welcome",
          "properties": {
            "type": { "const": "welcome" },
            "peer": { "type": "integer", "minimum": 0 },
            "peers": {
              "type": "array",
              "items": { "type": "integer", "minimum": 0 }
            }
          },
          "required": ["type", "peer", "peers"],
          "additionalProperties": false
        },
        {
          "type": "object",
          "title": "PeerJoined",
          "properties": {
            "type": { "const": "peer-joined" },
            "peer": { "type": "integer", "minimum": 0 }
          },
          "required": ["type", "peer"],
          "additionalProperties": false
        },
        {
          "type": "object",
          "title": "PeerLeft",
          "properties": {
            "type": { "const": "peer-left" },
            "peer": { "type": "integer", "minimum": 0 }
          },
          "required": ["type", "peer"],
          "additionalProperties": false
        },
        {
          "type": "object",
          "title": "ForwardedOffer",
          "properties": {
            "type": { "const": "offer" },
            "from": { "type": "integer", "minimum": 0 },
            "sdp": { "type": "string" }
          },
          "required": ["type", "from", "sdp"],
          "additionalProperties": false
        },
        {
          "type": "object",
          "title": "ForwardedAnswer",
          "properties": {
            "type": { "const": "answer" },
            "from": { "type": "integer", "minimum": 0 },
            "sdp": { "type": "string" }
          },
          "required": ["type", "from", "sdp"],
          "additionalProperties": false
        },
        {
          "type": "object",
          "title": "ForwardedIce",
          "properties": {
            "type": { "const": "ice" },
            "from": { "type": "integer", "minimum": 0 },
            "candidate": { "type": "string" }
          },
          "required": ["type", "from", "candidate"],
          "additionalProperties": false
        },
        {
          "type": "object",
          "title": "ForwardedRelay",
          "properties": {
            "type": { "const": "relay" },
            "from": { "type": "integer", "minimum": 0 },
            "payload": {}
          },
          "required": ["type", "from", "payload"],
          "additionalProperties": false
        },
        {
          "type": "object",
          "title": "Error",
          "properties": {
            "type": { "const": "error" },
            "code": { "type": "string" },
            "message": { "type": "string" }
          },
          "required": ["type", "code", "message"],
          "additionalProperties": false
        }
      ]
    }
  ]
}

distributed.json

{
  "$schema": "https://json-schema.org/draft/2020-12/schema",
  "$id": "https://lazily.dev/schemas/distributed.json",
  "title": "Distributed Types",
  "description": "CRDT and permission types for lazily-distributed",

  "$defs": {
    "PeerId": {
      "type": "integer",
      "minimum": 0,
      "maximum": 9007199254740991,
      "description": "Wire-stable peer identifier (u64, must stay ≤ Number.MAX_SAFE_INTEGER)"
    },
    "NodeId": {
      "type": "integer",
      "minimum": 0,
      "description": "Wire-stable node identifier (decoupled from internal SlotId)"
    },
    "OpKind": {
      "type": "string",
      "enum": ["read", "write", "trigger_effect"],
      "description": "Permission-gated operation kind"
    },
    "RemoteOp": {
      "type": "object",
      "description": "Gated, serializable unit a peer requests",
      "properties": {
        "kind": { "$ref": "#/$defs/OpKind" },
        "node": { "$ref": "#/$defs/NodeId" }
      },
      "required": ["kind", "node"],
      "additionalProperties": false
    },
    "CellRegisterType": {
      "type": "string",
      "enum": ["lww", "mv", "pn-counter"],
      "description": "CRDT register type for a replicated cell"
    },
    "HLCStamp": {
      "type": "object",
      "description": "Hybrid logical clock stamp for causal ordering",
      "properties": {
        "wall_time": {
          "type": "integer",
          "minimum": 0,
          "description": "Wall-clock microseconds since epoch"
        },
        "logical": {
          "type": "integer",
          "minimum": 0,
          "description": "Logical counter for causal tiebreak"
        },
        "peer_id": { "$ref": "#/$defs/PeerId" }
      },
      "required": ["wall_time", "logical", "peer_id"],
      "additionalProperties": false
    }
  }
}

Lean Formal Model

formal/lean is a small Lean 4 Lake package for the IPC Snapshot/Delta state machine. It is a spec companion, not an implementation replacement.

The model proves the invariants that are easiest to blur across language bindings:

• delta epochs are strictly sequential (epoch = base_epoch + 1);
• gap, reorder, and restart cases fail closed to snapshot resync;
• equal set_cell writes are silent;
• equal memo recomputes suppress slot_value and downstream invalidation;
• eager Signal changes publish concrete slot_value ops rather than bare invalidate ops for their backing slot;
• batch flushes carry a coalesced frontier and advance the IPC epoch once.

Run it through the local check target:

make check

Keep the Lean package narrow. JSON Schema, Rust implementation behavior, cross-language conformance fixtures, Loom/thread-safe tests, and live transport validation remain separate verification layers.