Skip to content
SafeMesh

The proof and its boundary — main (unreleased)

Source: WHAT-IS-PROVEN.md. Build commit: a6fc8ebe8234f971265bcd280293a90da57d9961. Main (unreleased); this identifies source, not a successful test run.

v0 scope: G-Counter and OR-Set are the v0 focus types, within the language-path limits. G-Set, PN-Counter, RGA/Text, LWW Register (LwwRegister), Enable-wins Flag (EnableWinsFlag) and LWW Map (LwwMap) are experimental, including their deltas and wrappers. Existing proof/test evidence is unchanged by release status.

Reproduction commands use Rust 1.96.1, the full-gate CI and demo toolchain; the consumer crate floor is Rust 1.89. Install rustup and select the toolchain using the build toolchain setup before running them.

SafeMesh follows verification-guided development:

  1. Lean definitions state the semantics.
  2. Lean theorems prove convergence properties over those definitions.
  3. A Lean executable emits an oracle corpus from the same definitions.
  4. Rust product code replays that JSON corpus and compares state vectors, sets, read vectors, numeric values, ownership decisions and optional allocation/sequence results with the parsed expectations. TESTED — Evidence: conformance; run from rust/: cargo test -p safemesh-crdt --test conformance --locked.

The proof is in Lean. The Rust crate is a second implementation held to the proof by differential conformance.

Claim-to-evidence map

Section titled “Claim-to-evidence map”

Theorems prove Lean model results. Corpus-checked below means finite Rust comparisons against outputs of the compiled Lean definitions, not a proof of Rust; Rust tests means separate test evidence without that corpus bridge.

Model resultRust validation mechanismEvidence linkExcluded real-world guarantee
Carrier convergence: in a bottomed join-semilattice, equal delivered delta sets give equal state, independent of order and duplicates.Corpus-checked: G-Counter, PN-Counter, G-Set, OR-Set and RGA operations are compared with model states/reads; G-Counter also checks split delivery followed by merge.Delta theorem, Lean emitter, corpus, Rust conformance assertions.No delivery or eventual recovery guarantee; OR-Set removes observed tokens, and RGA positions are caller supplied. Finite samples do not prove every Rust execution.
Ownership/allocation: the guard enforces modeled writer, coordinate, token and generation conditions; valid authors have disjoint tokens, and successful allocation/sequence results satisfy bounds.Corpus-checked: ownership::refuses, allocate_token and next_sequence are compared with the ownership, allocation and sequence oracle sections.Record-kernel definitions and theorems, Lean emitter, owned_writes_match_lean_oracle.No proof that OS locks are exclusive, generation inputs are correct, or writer identities are authentic.
Admission/replay: only accepted records mutate the modeled replica; reachable live state equals log replay, and equal accepted logs give equal live states.Rust tests, not corpus-checked: EventLog::admit_with is exercised for acceptance, duplicates, collisions and live/replay agreement.admission, idempotence, collision, replayAgrees, record_1_1_live_and_replay, duplicates_and_collisions_do_not_invoke_application.No crash atomicity between real log/cache writes, or convergence for equal input sets containing conflicting payloads.
Checked restart: a successful checkedRestart on decoded history returns live state equal to replay and an allocation mark equal to the saved mark.Rust tests, not corpus-checked: DurableReplica::restart_counter and restart_utf8_set test restored state, fresh allocation and rejection of invalid histories.checkedRestartSound, restart_still_works_and_fresh_allocation, restart_invalid_history.No theorem for frame decoding, lock reacquisition, fsync, rename or power-loss recovery; the model theorem covers only successful restart.
Additional carriers: no Lean result claimed for LwwRegister, EnableWinsFlag or LwwMap.Rust tests, not corpus-checked: wire round trips and sampled merge/delivery laws.Wire tests, laws harness tests.No universal convergence proof for these implementations from passing sampled laws.
Bindings/wire: no separate Lean theorem for serialization, C ABI, WASM/TypeScript or Python wrappers.Rust tests and integration smoke, not corpus-checked: exact bytes, round trips, malformed input, header drift, C calls and installed binding packages.Wire tests, header test, C smoke, package smoke.No end-to-end proof of a language integration, arbitrary byte-input safety, or registry availability from these tests.
Transport: no Lean theorem for the transport implementation.Rust tests, not corpus-checked: InMemoryTransport exercises subscriptions, connectivity, drops, duplicates, reordering, partitions/healing and version-vector anti-entropy.Transport assertions.No radio/network delivery, authentication or eventual recovery guarantee.

Lean proof surface

Section titled “Lean proof surface”

The SafeMesh Lean suite proves the following model properties. The general delta model assumes a join-semilattice with bottom and equal sets of delivered deltas; it does not assume causal delivery or supply missing deltas. Eventual recovery is a delivery assumption. OR-Set membership uses observed tokens; RGA positions are caller supplied, and identifier allocation is outside its model. Model and assumptions.

Record kernel

Section titled “Record kernel”

lean/SafeMesh/RecordKernel.lean, namespace SafeMesh.RecordKernel, declares 21 theorems. The module is imported by lean/SafeMesh.lean, so the default SafeMesh target builds it, and each of the 21 has its axiom set pinned by #guard_msgs in Test/Axioms.lean, itself a default target; lake build in CI therefore fails on any new axiom, sorry or native_decide in any of them. At source revision 279926bbe05eb6cc592af54c1c4c28a9f21f84e9 the SafeMesh CI run 34390575569 built that gate successfully. This is commit-specific evidence, not certification of every later commit.

Read the theorems against the model the file defines. A Replica is a log of (id, payload) records plus a cached live state; outcome classifies a record as accepted, duplicate or collision by comparing the full payload, not a hash; step mutates only on acceptance; Reachable is what step can produce from empty. Payloads range over any bottomed join-semilattice, so the same theorems apply to every carrier.

  • admission: for a replica whose provenance equals its log, the log changes if and only if the record is accepted, the live state changes if and only if the record is accepted, and the live value after the step is the old value joined with the payload when the record is accepted and the old value unchanged otherwise; a redundant payload can leave the value equal in both cases, so the value alone does not characterize acceptance. replayAgrees supplies that provenance premise for every reachable replica. PROVEN — Evidence: admission.
  • idempotence: step (step s r) r = step s r for every replica s, including one with an arbitrary cache. PROVEN — Evidence: idempotence.
  • collision: an id already present in an id-unique log with a different payload yields the collision outcome and leaves the replica unchanged; and any two reachable replicas with equal logs have equal live state. PROVEN — Evidence: collision.
  • replayAgrees: every reachable replica’s live state equals replay of its log; the retired legacyStep transition really produces the measured Rust defect (RustDefect legacyWitness, checked by the kernel rather than by native evaluation); and no reachable replica exhibits that defect. PROVEN — Evidence: replayAgrees.
  • tokenOwner, tokenDisjoint, tokenSequence, allocatedOwned, sequenceFresh: a token is defined as sequence * writers + author; modulo recovers the author, so two distinct valid authors mint distinct tokens at every pair of sequences; equal tokens from one author force equal sequences when the writer count is positive; a successful allocateToken implies a valid author, a positive sequence and a result at most maxWord; a successful nextSequence strictly increases and stays at most maxWord. PROVEN — Evidence: tokenOwner; tokenDisjoint; tokenSequence; allocatedOwned; sequenceFresh.
  • validPermitted, ownedWriter, ownedCoordinate, competingRefused, staleRefused, foreignCoordinateRefused, foreignTokenRefused, refusedUnchanged, ownedReachable, ownedConvergence: refuses is defined as the negation of the decidable permitted predicate, so exactly the permitted domain passes by that definition, and validPermitted is the one-way positive control that a permitted write is not refused; a passing write has an author below the writer count and, for a local write, equal to the configured writer, and a passing counter payload names the author’s own coordinate; a write is refused when the lock is not held, when the generation differs from the current one, when a counter coordinate is foreign, or when an add’s token is not the one allocated to that author and sequence; a refused ownedStep returns its input unchanged; a guarded step from a reachable replica reaches a reachable replica; and equal logs still give equal live state. PROVEN — Evidence: validPermitted; ownedWriter; ownedCoordinate; competingRefused; staleRefused; foreignCoordinateRefused; foreignTokenRefused; refusedUnchanged; ownedReachable; ownedConvergence.
  • replayOwnedReachable, checkedRestartSound: replaying a history through the guard from a reachable state yields a reachable state, so a successful checkedRestart returns a replica whose live state equals replay of its log and whose allocation mark equals the saved mark. replayOwned and checkedRestart are defined to return none on a refused or non-accepted record and on a mismatched mark; the theorem speaks only about the some case. PROVEN — Evidence: replayOwnedReachable; checkedRestartSound.

What the record kernel does not establish. Its transitions are atomic because they are functions, which says nothing about a crash between a log append and a cache update in a real process. Equal accepted sets determine state; equal input sets with conflicting payloads do not, because rejection makes the accepted set depend on arrival order. held, generation and currentGeneration are inputs, so the theorems prove the decision taken on those facts, not that the OS lock is exclusive or that the generation was read correctly. checkedRestart takes an already-decoded history, so frame validation, lock reacquisition, fsync, rename and power-loss recovery are outside it. No theorem here covers version vectors, cursors, envelopes, authentication, or how a collision is reported to a peer. The alarm is tested, not proven. The collision alarm is raised by EventLog and Replica and by the Python and WASM replica bindings when a peer offers a held record ID with a different payload. An equal payload remains a duplicate with no new alarm. collision_report_bytes produces a CollisionReport (wire tag 0x05) for the peer. LocalReplica and DurableReplica also record the alarm on Admission::Collision, and their logs produce a collision report. The C FFI has no collision-report surface. Restoring an encoded plain log drops the alarm; a restarted durable replica keeps raised alarms in a separate synced alarm file. It does not repair the fork. Offer-based detection requires a peer to offer the other payload; version-vector anti-entropy between equal prefixes offers nothing. Separately, merge_collision_report_bytes takes a received report on the sender’s word: any well-formed report within the decode limits that names a held ID with a different payload records a fork, or keeps an existing alarm. A peer can therefore make a replica record a fork that no replica admitted; a report is not evidence that any replica admitted that payload. Evidence: collision_alarm; run from rust/: cargo test -p safemesh-crdt --test collision_alarm --locked.

PROVEN — The upstream crdt-lean corpus also proves the state-based CvRDT laws, conditional liveness under explicit fairness and quiescence assumptions, G-Set, G-Counter, PN-Counter, OR-Set, and Sequence/RGA convergence. Evidence at the pinned upstream revision: Crdt.strong_eventual_consistency, Crdt.DeliverySystem.eventual_agreement, G-Set and counter instances, Crdt.ORSet.strong_eventual_consistency, and Crdt.Sequence.read_strong_eventual_consistency.

Rust product surface today

Section titled “Rust product surface today”

rust/crates/safemesh-crdt currently ships:

TESTED — The Lean-backed CRDT carriers are no_std + alloc, forbid unsafe, and are checked by tests/conformance.rs against tests/corpus.json. EventLog is engineered infrastructure and is tested by Rust unit tests; it is not by itself a Lean-proven application-state convergence theorem, although its admit_with decision transcribes the record kernel’s step and is tested against it. LwwRegister, EnableWinsFlag, and LwwMap are also engineered/tested, not Lean-proven. Evidence: crate attributes and implementation, conformance tests (cargo test -p safemesh-crdt --test conformance --locked from rust/).

TESTED — The wire format and C ABI are also engineered infrastructure. They are covered by exact-byte, round-trip, malformed-input, FFI smoke, and header-drift tests, not by Lean theorems. TESTED — Evidence: wire; run from rust/: cargo test -p safemesh-crdt --test wire --locked. FFI smoke (scripts/ffi-c-smoke.sh from the repository root); committed_header_has_not_drifted (cargo test -p safemesh-ffi --test header --locked from rust/).

The record kernel reaches Rust in two different ways. The ownership guard, token allocation and sequence counter are emitted into the ownership, allocation and sequence sections of tests/corpus.json from the same Lean definitions the theorems are about, and tests/conformance.rs replays them through the Rust ownership module. Record admission in EventLog::admit_with and the durable restart path in local::DurableReplica::restart_counter and restart_utf8_set are transcriptions checked by Rust unit tests (tests/record_admission.rs and the tests inside src/local.rs); they are not in the corpus. All of this is tested, not proven; only the ownership part is corpus-conformant. TESTED — Evidence: conformance; run from rust/: cargo test -p safemesh-crdt --test conformance --locked. TESTED — Evidence: record_1_1_live_and_replay; duplicates_and_collisions_do_not_invoke_application; run from rust/: cargo test -p safemesh-crdt --features laws --test record_admission --locked. TESTED — Evidence: restart_still_works_and_fresh_allocation; restart_invalid_history; run from rust/: cargo test -p safemesh-crdt --features laws --lib --locked.

API present: WASM/TypeScript and Python expose wrappers over the Rust core. Runtime tested: their Rust-side tests check core calls, canonical record/log bytes, and convergence by merging those bytes. Integration tested: the Linux package smoke flow exercises a generated WASM package in Node and an installed Python wheel. Artifact available: these flows create local packages; registry availability is not established by them. Maintainer-supported status for both bindings is unknown. These binding tests are not separate Lean proofs. Binding exposure for LwwRegister, EnableWinsFlag, and LwwMap inherits those types’ tested-not-proven labels. TESTED — Evidence: package smoke (scripts/package-smoke.sh from the repository root); WASM tests; Python tests.

The break-it demo and cold-chain kill-test are also engineered evidence. They are useful because they are visible and re-runnable, but they are not substitutes for the Lean proof or differential corpus. TESTED — Evidence: cold_chain_kill_test; run from rust/: cargo test -p safemesh-crdt --examples --locked.

The transport coverage contract is engineered/tested. InMemoryTransport validates subscription, connectivity, drop, duplicate, reorder, partition, heal, and version-vector anti-entropy behavior in CI. This does not prove radio or network delivery. TESTED — Evidence: transport; run from rust/: cargo test -p safemesh-crdt --test transport --locked.

The honesty boundary

Section titled “The honesty boundary”

The Lean theorems are universal over their mathematical models. The Rust implementation is not itself proven in Lean. It is differentially tested against the Lean-generated corpus. This corpus bridge is the honesty artifact that keeps “verified” tied to the proof.

Property tests, fuzzers, and demos are useful, but they cannot by themselves justify a proven claim.

The record kernel widens the proof surface, not this boundary. Its theorems are about a modeled log, cache and guard; the Rust EventLog, ownership and local modules are held to that model by tests, and for ownership by the corpus, and the facts the guard decides on come from a filesystem shell that is tested rather than proven.

Laws harness

Section titled “Laws harness”

The optional Rust laws module checks merge commutativity, associativity, idempotence, identity, redelivery, shuffled delivery, and split/drop-then-merge convergence over user-supplied examples. It is designed so third-party CRDT types can run the same behavioral bar in their own CI.

The harness is not a theorem prover. Passing it labels a type as laws-tested, not Lean-proven. TESTED — Evidence: merge_laws_hold_for_in_house_samples; convergence_harness_hammers_delta_delivery_shapes; run from rust/: cargo test -p safemesh-crdt --features laws --test laws --locked.