Crate safemesh_crdt 

Delta-state G-Counter and PN-Counter for constrained mesh links.

This crate is the PRODUCT half of the SafeMesh verification-guided loop: a thin no_std + alloc implementation of exactly the model proven in lean/SafeMesh/ (carrier = join-semilattice, merge = join, delta = single-coordinate bump), held to those proofs by a differential conformance test (tests/conformance.rs) that replays a Lean-emitted JSON corpus through this code and compares state vectors, sets, read vectors, numeric values, ownership decisions and optional allocation/sequence results with the parsed expectations.

What is PROVEN (in Lean, kernel-checked) vs what is TESTED (here): the Lean theorems are universal; this crate is checked against them over a finite corpus. The bridge (Lean compiled eval → JSON → this crate) is the named trusted component. See the repo README for the full TCB statement.

Modules

laws

local

Linux/local-filesystem packet-A adapter. All writers for a replica set must use the same directory and fixed configuration. Keep fence files in place. LocalReplica acknowledges in memory; DurableReplica commits before acknowledgement and offers checked ordinary restart of an existing committed store.

ownership

Transcription of SafeMesh.RecordKernel ownership rules. The existing Lean corpus binds these decisions to their specification; no Lean runtime is used.

wire

Canonical wire codec implementations for the CRDT types.

Structs

CollectionLimits

Optional count budget for each built-in collection and collection delta.

CollisionReport

The wire message that carries collision alarms to a peer.

DecodeLimits

Record and collection limits for EventLog::from_wire_bytes_with_limits.

EnableWinsFlag

Enable-wins boolean flag.

EventLog

Append-only, deduplicating event log for CRDT deltas. Equality compares log data, excluding the in-memory first-admission binding flag and the in-memory collision register.

GCounter

A grow-only counter: one tally per replica, join = pointwise max.

GCounterDelta

Delta for a grow-only counter: one replica coordinate and its asserted tally.

GSet

A grow-only set: merge = union.

InMemoryTransport

Deterministic in-memory adapter for coverage-contract fault campaigns.

LwwDot

Total-order dot for last-writer-wins registers.

LwwEntry

One LWW register assignment.

LwwMap

Last-writer-wins map.

LwwRegister

Last-writer-wins register.

LwwRegisterDelta

Delta for a last-writer-wins register.

OrSet

Observed-remove set with add-wins semantics.

PnCounter

An increment/decrement counter: a pair of G-Counters (increments P, decrements N), join = componentwise.

Record

An event-log record carrying a CRDT delta.

RecordCollision

One record ID held with two different payloads.

RecordId

Stable identity for an event-log record.

Replica

Owned state and admitted history. A nonempty initial state need not be reproducible from its initially empty log.

Rga

RGA-family sequence state: positioned values plus tombstoned positions.

TransportEnvelope

VersionVector

Per-replica contiguous prefixes for anti-entropy pulls.

VersionVectorLimits

Optional collection budgets for VersionVector::from_peer_prefixes_with_limits.

WireCursor

Borrowed, bounds-checked reader for canonical wire primitives.

Enums

Admission

Full decoded payload equality distinguishes redelivery from an ID collision.

AppendError

CollisionVerdict

What merging one report entry did to the receiving log.

CoordinateError

Rejection of an invalid counter domain or replica coordinate.

DecodeError

Failure from the bounded event-log decoder. Separate from WireError to preserve existing exhaustive matches.

EnableWinsFlagDelta

Delta for an observed-token enable-wins flag.

LegacyFrame

An EventLog frame layout written by an earlier encoder, named by WireError::LegacyEventLogFrame.

LwwMapDelta

Delta for a last-writer-wins map.

MergeError

Error raised by full-state merge (merge or try_merge).

OrSetDelta

Delta for an observed-remove set.

PnCounterDelta

ReplicaError

The operation that failed; invalid admission remains a verdict.

RgaDelta

Delta for an RGA-family ordered sequence.

TransportError

VersionVectorError

VersionVectorLimitError

Failure from opt-in bounded peer-version reconstruction. Separate from VersionVectorError to preserve existing exhaustive matches.

WireError

Traits

Crdt

Delta application surface for CRDT product types.

Mergeable

State-based merge contract: merge is expected to be a semilattice join.

TransportAdapter

Engineered transport coverage contract.

WireDecode

Decode one payload from a shared cursor using its public read methods. Self::from_wire_bytes additionally rejects trailing bytes.

WireEncode

Encode a payload using the canonical wire primitives.

WireSchema

Stable, versioned identity for persisted payloads, independent of Rust names. External implementations must use a globally unique schema and change it when the wire interpretation changes. Never reuse a built-in safemesh/ identity.

Functions

anti_entropy

Queue repair and admit the deliveries available for to, returning every record ID and verdict with its sending peer. In particular, Invalid is reported again on every retry, with its original reason. Refusals are not acknowledgements and are not cached: fixing the receiver permits the next ordinary sync to admit the record. Dropped or partitioned packets retain the adapter’s usual delivery semantics.

queue_anti_entropy

Queue missing records. Admission happens at the receiver; use anti_entropy when both replicas are available to observe refusals.

write_bytes

Append a u32 length prefix followed by the bytes verbatim. Returns LengthOverflow without changing out if the slice length exceeds u32::MAX. Read the prefix with WireCursor::read_len and the payload with WireCursor::read_exact.

write_len

Append len as a four-byte little-endian u32. Returns LengthOverflow without changing out if len exceeds u32::MAX. The result can be read with WireCursor::read_len.

write_u8

Append one byte in the same format as WireCursor::read_u8.

write_u32

Append a u32 as four little-endian bytes, matching WireCursor::read_u32.

write_u64

Append a u64 as eight little-endian bytes, matching WireCursor::read_u64.