Expand description
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
corpus through this code and requires byte-identical outputs.
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.
Structs§
- Enable
Wins Flag - Enable-wins boolean flag.
- Event
Log - Append-only, deduplicating event log for CRDT deltas.
- GCounter
- A grow-only counter: one tally per replica, join = pointwise max.
- GCounter
Delta - Delta for a grow-only counter: one replica coordinate and its asserted tally.
- GSet
- A grow-only set: merge = union.
- InMemory
Transport - 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.
- LwwRegister
Delta - 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, decrementsN), join = componentwise. - Record
- An event-log record carrying a CRDT delta.
- Record
Id - Stable identity for an event-log record.
- Rga
- RGA-family sequence state: positioned values plus tombstoned positions.
- Transport
Envelope - Version
Vector - Per-replica contiguous prefixes for anti-entropy pulls.
- Wire
Cursor
Enums§
- Admission
- Full decoded payload equality distinguishes redelivery from an ID collision.
- Append
Error - Coordinate
Error - Rejection of a counter delta with an invalid replica coordinate.
- Enable
Wins Flag Delta - Delta for an observed-token enable-wins flag.
- LwwMap
Delta - Delta for a last-writer-wins map.
- Merge
Error - Error raised by the checked full-state merge (
try_merge). - OrSet
Delta - Delta for an observed-remove set.
- PnCounter
Delta - RgaDelta
- Delta for an RGA-family ordered sequence.
- Transport
Error - Wire
Error
Traits§
- Crdt
- Delta application surface for CRDT product types.
- Mergeable
- State-based merge contract:
mergeis expected to be a semilattice join. - Transport
Adapter - Engineered transport coverage contract.
- Wire
Decode - Wire
Encode - Wire
Schema - 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.