Skip to content
SafeMesh

Claims and assurance evidence — main (unreleased)

Source: CLAIMS.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.

Evidence labels apply to individual statements. Evidence links name source artifacts; commands reproduce tests, not universal proofs. The site pins repository evidence links to its build commit.

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

SafeMesh’s verified claim is deliberately narrow:

The Lean models of the in-house CRDT types backed by the Lean suite are universally proved insensitive to duplicate and reordered delivery, and convergent after missing deltas are eventually recovered by merge/anti-entropy; the separately implemented Rust product is finitely tested against the Lean-generated differential oracle corpus, not universally proved. Passing that corpus is conformance evidence for Rust. PROVEN — Evidence: delta_dissemination_sec; merge_deltaState. TESTED — Evidence: conformance; run from rust/: cargo test -p safemesh-crdt --test conformance --locked.

Proven

Section titled “Proven”
  • The Lean delta suite in lean/SafeMesh/ proves Strong Eventual Consistency for delta dissemination over the supported CRDT carriers. PROVEN — Evidence: delta_dissemination_sec; merge_deltaState.
  • The Lean record kernel in lean/SafeMesh/RecordKernel.lean (namespace SafeMesh.RecordKernel) is machine-checked on the same default build target and per-theorem axiom gate as the delta suite. Every theorem in it is about a model: a log, a cached live state, one admission transition, and the ownership facts a local writer is handed. WHAT-IS-PROVEN.md enumerates all 21 theorems and how each reaches Rust. The product claims that may be repeated from the kernel are the five below, and each carries the limit that must travel with it. PROVEN — Evidence: admission; checkedRestartSound.
    • Record admission (admission, idempotence, collision): in every reachable modeled replica the log and the live state change exactly when a record is accepted; delivering the same record again changes nothing, however many times it arrives; and a different payload under an id already in the log is refused as a collision and mutates nothing, provided the log holds one payload per id. Limit: the theorem is about the modeled transition. The Rust EventLog::admit_with is a transcription held to it by Rust unit tests, not by the Lean oracle corpus, and decoding, authentication, version vectors and reporting a collision to a peer are outside the theorem. PROVEN — Evidence: admission; idempotence; collision.
    • Replay agreement (replayAgrees, collision): every reachable modeled cache equals an independent replay of its log, and two reachable replicas whose accepted logs are equal have equal live state, whatever the delivery order and however many duplicates or rejections occurred. Limit: equal accepted sets, not equal input sets. When two payloads conflict under one id, arrival order decides which is accepted, so same-input-set convergence is not claimed and the replicas stay forked. Outside the theorem, 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. A restarted durable replica keeps raised alarms in a separate synced alarm file; restoring an encoded plain log still drops them. 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. This alarm is tested, not proven (run from rust/: cargo test -p safemesh-crdt --test collision_alarm --locked). The model’s transitions are atomic because they are functions; nothing here proves crash atomicity or storage durability in a running process. PROVEN — Evidence: replayAgrees; collision.
    • Token ownership (tokenDisjoint, with tokenOwner, tokenSequence, allocatedOwned, sequenceFresh): under a fixed positive writer count, two distinct valid authors never mint the same token at any pair of sequences, one author never mints one token at two different sequences, allocation returns a token only for a valid author, a positive sequence and a value within the 64-bit bound; and a successful next-sequence step returns a strictly larger sequence that stays within the 64-bit bound. Limit: this is arithmetic on the token and nextSequence definitions. Whether a running process is the author it claims is a fact the local-filesystem shell supplies, and the Rust allocation is checked against a finite corpus. PROVEN — Evidence: tokenDisjoint; tokenOwner; tokenSequence; allocatedOwned; sequenceFresh.
    • Ownership guard (competingRefused, staleRefused, foreignCoordinateRefused, foreignTokenRefused, refusedUnchanged, with validPermitted, ownedWriter, ownedCoordinate, ownedReachable, ownedConvergence): the modeled guard refuses a write when the lock is not held, when the generation is stale, when a counter coordinate is not the author’s own, or when an add carries a token other than the one allocated to that author at that sequence; a refused write leaves log, live state and allocation mark unchanged; a permitted write is not refused; and guarded steps keep the replay-agreement invariant. The modeled guard is defined as the negation of the decidable permitted predicate, so exactly the permitted domain passes by that definition; no theorem concludes the converse, and validPermitted proves only that a permitted write passes. Limit: the guard decides on facts it is given, namely lock held, generation current and local write. It does not prove that an OS lock is exclusive or that a generation file was read correctly, and the Rust decision is tested over a finite corpus matrix. PROVEN — Evidence: competingRefused; staleRefused; foreignCoordinateRefused; foreignTokenRefused; refusedUnchanged; validPermitted; ownedWriter; ownedCoordinate; ownedReachable; ownedConvergence.
    • Checked restart (checkedRestartSound, with replayOwnedReachable): when the modeled checked restart succeeds, the state it returns has a cache equal to replay of its log and an allocation mark equal to the saved one. The modeled restart is defined to fail on any history containing a refused or non-accepted record; the theorem speaks only about the successful case. Limit: the model receives an already-decoded history. It proves nothing about frame validation, lock reacquisition, file sync, rename or power-loss recovery, and the Rust restart path is Linux-only and held to the model by its own unit tests. PROVEN — Evidence: checkedRestartSound; replayOwnedReachable.

Tested, not proven

Section titled “Tested, not proven”

  • G-Set, G-Counter, PN-Counter, OR-Set, and RGA/Text have Rust implementations that are differentially tested against tests/corpus.json, emitted from the Lean definitions by lake exe corpus. TESTED — Evidence: conformance; run from rust/: cargo test -p safemesh-crdt --test conformance --locked.

  • The Rust EventLog is a deduplicating append/merge/since/version infrastructure layer. Its admission decision, admit_with, transcribes the record-kernel model below and is tested against that model, not proven. It supports the product surface, but the proven convergence claim lives in the CRDT carriers and their Lean-backed corpus bridge. 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.

  • LwwRegister is tested-not-proven. It is a flat max-register over (timestamp, replica, value) and is covered by Rust laws/wire tests, but it is not in the current Lean oracle corpus. TESTED — Evidence: lww_register_wire_is_stable_and_roundtrips; run from rust/: cargo test -p safemesh-crdt --test wire lww_register --locked. Laws tests.

  • EnableWinsFlag is tested-not-proven. It is a flat observed-token boolean flag and is covered by Rust laws/wire tests, but it is not in the current Lean oracle corpus. TESTED — Evidence: enable_wins_flag_wire_is_stable_and_roundtrips; run from rust/: cargo test -p safemesh-crdt --test wire enable_wins_flag --locked. Laws tests.

  • LwwMap is tested-not-proven. It is a flat per-key LWW map with remove tombstones and is covered by Rust laws/wire tests, but it is not in the current Lean oracle corpus. TESTED — Evidence: lww_map_wire_is_stable_and_roundtrips; run from rust/: cargo test -p safemesh-crdt --test wire lww_map --locked. Laws tests.

  • Rust code is checked against a finite Lean-generated corpus. Passing the corpus is strong conformance evidence, not a universal theorem about the Rust compiler or hardware. TESTED — Evidence: conformance; run from rust/: cargo test -p safemesh-crdt --test conformance --locked.

  • Property tests and the laws feature harness test algebraic behavior over generated scenarios. They supplement the Lean-oracle differential test; they do not replace it. 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.

  • Canonical wire encoding, binding glue, FFI, WASM, Python, demos, and storage or transport adapters are outside the Lean proof claim. For binding support facts, use the separate API present, artifact available, build checked, runtime tested, integration tested, and maintainer-supported statements in the root README; name the test environment rather than combining them into a single “tested” label. Transport adapters can be tested against the coverage contract, but SafeMesh does not prove network delivery. Bindings and adapters must call the Rust core rather than reimplementing merge semantics. NOT COVERED — Scope evidence: proof boundary; binding evidence: six support fields.

  • Integrity vertical examples, including the cold-chain kill-test, are engineered evaluation artifacts. They test modeled software convergence; they do not prove sensor truth, legal custody, storage durability, or real transport delivery. TESTED — Evidence: cold_chain_kill_test; run from rust/: cargo test -p safemesh-crdt --examples --locked.

  • User-defined types are tested by their authors against the merge laws. SafeMesh does not prove arbitrary user reducers. NOT COVERED — Scope evidence: author-supplied laws harness.

  • The Rust transcriptions of the record kernel are tested, not proven. The ownership guard, token allocation and sequence counter are replayed from the ownership, allocation and sequence sections of tests/corpus.json; EventLog::admit_with and the durable restart path are checked by Rust unit tests only. Passing these is conformance evidence over finite cases, not a theorem about the Rust code, the Linux filesystem, or the lock it relies on. 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.

Not covered in v0

Section titled “Not covered in v0”
  • For a pre-protection append-log store, restart truncates a final journal entry that fails its length or checksum test and reports the discarded bytes through torn_tail(). SafeMesh does not claim that an acknowledged final record survives later damage to its bytes. Such damage is discarded as a torn tail and is not refused for a pre-protection store; a protected store refuses if the lost entry carried own-writer progress. A damaged entry followed by other data is refused as History(IntegrityMismatch). NOT COVERED — Scope evidence: append_log_torn_tail_is_truncated_and_reported; append_log_damage_before_the_tail_is_refused.
  • A new Rust durable store keeps an own-writer sequence counter outside the store directory and a protection marker inside it. If only the store directory is restored and that restore loses an own-writer record, restart refuses as RecoveryRequired; the caller must open the restored store as a new writer. A refused fresh create caused by a leftover counter leaves no new file in the store directory. A batch advances the counter once to its last sequence before writing its journal entries and syncing the journal once. A crash after the counter sync and before the journal sync, including a batch with only its first entry present, makes an honest restart refuse. A copy that also copies the counter still passes. Losing only other writers’ records is not detected by this own-writer counter. Pre-protection stores with neither marker nor counter keep their existing restart behavior. This is a one-machine check, tested rather than proven. TESTED — Evidence: refused_create_leaves_no_store_files; rollback_batch_crash_boundaries; rollback_r1_store_only_restore_refuses; rollback_r4_crash_write_boundaries; rollback_r7_limit_whole_machine_copy_passes.
  • The EventLog CRC detects accidental damage; it is not a MAC and does not stop a deliberate forger. NOT COVERED — Scope evidence: frame_crc32.
  • References between objects. NOT COVERED — Scope evidence: assurance boundary.
  • Trees and ordered move semantics. NOT COVERED — Scope evidence: assurance boundary.
  • Leader election or consensus. NOT COVERED — Scope evidence: assurance boundary.
  • Guaranteed network delivery or radio-transport correctness. NOT COVERED — Scope evidence: assurance boundary.
  • Hardware puck behavior. NOT COVERED — Scope evidence: assurance boundary.
  • Storage durability, crash atomicity, or lock exclusivity as proven properties. The record kernel proves decisions over facts the local-filesystem shell supplies; the shell itself is tested. NOT COVERED — Scope evidence: assurance boundary.
  • Flag or Map as proven SafeMesh product types, unless matching Lean proofs and corpus-backed Rust conformance are added. LwwRegister, EnableWinsFlag, and LwwMap exist, but remain tested-not-proven until that proof bridge lands. NOT COVERED — Scope evidence: assurance boundary.

Wording rule

Section titled “Wording rule”

Use: “provably converges (once deltas are delivered)”, “duplicate delivery does not duplicate modeled state”, “machine-checked”, and “re-runnable in your CI”.

Do not use: “can’t corrupt”, “unbreakable”, “guaranteed delivery”, or “a faster Yjs”.