Start here
Overview
crdtlib is a Lean 4 library of operation-based CRDTs. A small set of combinators builds complex CRDTs out of simpler ones, and each combinator proves that its result converges. Anything you assemble from them is therefore a CRDT by construction: verified in Lean and executable.
Get started
Add the dependency, compose a CRDT from library parts, check that replicas converge, and write your own primitive.
Read ConceptsThe model
The system model, strong eventual consistency, what a CRDT is in Lean, and why composites need no new proofs.
Read ReferenceCombinators
The prinicpal and derived combinators that facilitate convergence by construction
Read ReferenceCatalog
Registers, sets and the list CRDT, each with its construction, its definition, and the combinators it uses.
ReadThe building blocks
Every CRDT in the library is assembled from primitives and principal and derived combinators. The same colors mark them throughout the documentation.
- Principal combinator
- Derived combinator
- Primitive CRDT
The primitive CRDTs are written by hand, with a hand-written commutativity proof. The combinators each preserve commutativity:
Product
product c₁ c₂Applies every operation to two CRDTs at once. The only combinator that combines two states.
ωσσ₁ × σ₂γγ₁ × γ₂MapState
map_state f f'Changes how the state is laid out, through a function with a left inverse.
ωσσ₂γγAssociate
associate κ cTurns one CRDT into a keyed family: a map from keys to independent copies.
κ × ωσAssociate κ σγAssociateInterp κ γTraverse
traverse f cTurns one operation into a list of inner operations: none, one, or several.
ω₂σσγγMapInterpretation
map_interpretation f cChanges what the application observes. Operations and state stay the same.
ωσσγγ₂The derived combinators are defined in terms of the principal ones, so they do not need their own proof:
MapOp
map_op f cTranslates each operation into exactly one inner operation. A traverse with singleton lists.
ω₂σσγγDisjointProduct
disjoint_product c₁ c₂Two CRDTs side by side; each operation targets one of them.
ω₁ ⊕ ω₂σσ₁ × σ₂γγ₁ × γ₂JointProduct
joint_product c₁ c₂Two CRDTs side by side; each operation updates both, atomically.
ω₁ × ω₂σσ₁ × σ₂γγ₁ × γ₂TaggedUnion
tagged_unionₜ c₁ c₂Either one CRDT or the other, with a register deciding which one is active.
(ω₁ ⊕ ω₂) ⊕ Choiceσ(σ₁ × σ₂) × …γγ₁ ⊕ γ₂Reading the source
Code excerpts in this documentation are taken from the library. To follow along in the repository:
| Path | Contents |
|---|---|
Crdtlib/CRDT/Basic.lean | CRDT and CRDTₜ, and the conversion between them |
Crdtlib/CRDT/Pkg.lean, Concurrent.lean | Events, timestamps and concurrency |
Crdtlib/CRDT/Primitive/ | The primitive families: ac_fun and mv_regₜ |
Crdtlib/Combinator/Principal/ | Product, MapState, Associate, Traverse, MapInterpretation |
Crdtlib/Combinator/Derived/ | MapOp, DisjointProduct, JointProduct, TaggedUnion |
Crdtlib/CRDT/Std/ | The catalog: registers, counters, sets and lists |