#crdt

Conflict-Free Replicated Data Types (CRDTs) are one of the core technical building blocks behind Ossa's secure synchronization protocol. CRDTs are special data types that enable data synchronization without a central server and allow users to make document edits even while offline. To provide these features, CRDTs must satisfy certain mathematical properties.

These properties were defined by Shapiro et al., who required CRDTs to guarantee Strong Eventual Consistency (SEC). SEC ensures that an application's state eventually converges between replicas once they have received the same set of update operations. CRDTs satisfy SEC by making sure that concurrent operations commute. Here is the commutativity property stated mathematically (in Lean pseudocode):

def commutativity := forall st: CRDT, op1: Operation, op2: Operation,
  concurrent(op1, op2) =>
    st.apply(op1).apply(op2) == st.apply(op2).apply(op1)

In other words, given two concurrent operations op1 and op2, if you apply op1 and then op2 to a CRDT, its final state is the same as if you applied op2 and then op1. As a result, application state converges to the same value, regardless of the order that updates were received. In practice, this enables collaborative applications where devices can sync directly over peer-to-peer connections and users can update their documents while offline.

Designing data types that satisfy the required CRDT properties is not easy. Fortunately, there are many CRDT primitives for commonly used data structures like registers, sequences, sets, and maps. As an example, consider the simple Last Writer Wins CRDT that serves as a register.

struct LWW<Time, A> {
    time: Time,
    value: A,
}