March Docs

CRDT

CRDT: state-based conflict-free replicated data types.

All CRDTs share the same contract: merge(a, b) -- commutative, associative, idempotent join equal(a, b) -- structural equality on the internal state

Sub-modules: CRDT.GCounter -- grow-only counter CRDT.PNCounter -- increment/decrement counter (two GCounters) CRDT.LWWRegister -- last-write-wins register (uses VectorClock) CRDT.ORSet -- observed-remove set (add/remove with UUID tags)

Types

ptypeTT = GCounter(Map(String, Int))#
ptypeTT = PNCounter(Map(String, Int), Map(String, Int))#
typeTT(a) = LWWRegister(a, VectorClock)#
ptypeTT(a) = ORSet(Map(String, (a, List(String))))#

Functions

fnaddadd(s : T(a), elem : a, to_key : a -> String, tag : String) : T(a)#

Add elem with a unique tag (use UUID.v4() for the tag).

fnaddadd(c : T, actor_id : String, n : Int) : T#

Add n to actor_id's slot (n must be >= 0).

fnclockclock(r : T(a)) : VectorClock#

Read the vector clock of the last write.

fncontainscontains(s : T(a), elem : a, to_key : a -> String) : Bool#

True if elem has at least one surviving tag.

fndecrementdecrement(c : T, actor_id : String) : T#

Decrement the counter for actor_id.

fnelementselements(s : T(a)) : List(a)#

All elements currently in the set.

fnentriesentries(c : T) : List((String, Int))#

All (actor_id, count) pairs.

fnequalequal(a : T(x), b : T(x)) : Bool#

True when both ORSets have the same elements (ignoring tag identity).

fnequalequal(a : T(x), b : T(x)) : Bool#

True when both registers hold the same clock (values may still differ on concurrent writes).

fnequalequal(a : T, b : T) : Bool#

True when both PNCounters have the same net increments and decrements.

fnequalequal(a : T, b : T) : Bool#

True when both counters have identical internal state.

fngetget(r : T(a)) : a#

Read the current value.

fnincrementincrement(c : T, actor_id : String) : T#

Increment the counter for actor_id.

fnincrementincrement(c : T, actor_id : String) : T#

Increment actor_id's slot by 1.

fnmergemerge(a : T(x), b : T(x)) : T(x)#

Merge: union tags for each element key.

fnmergemerge(a : T(x), b : T(x)) : T(x)#

Merge: keep the value with the causally later clock. Concurrent = keep left.

fnmergemerge(a : T, b : T) : T#

Merge two PNCounters: join both P and N maps independently.

fnmergemerge(a : T, b : T) : T#

Component-wise maximum — the CRDT join.

fnnewnew() : T(a)#

An empty set.

fnnewnew(value : a, clock : VectorClock) : T(a)#

Create a new register with an initial value and the clock at write time.

fnnewnew() : T#

An empty counter with value 0.

fnnewnew() : T#

An empty counter (all actor counts are 0).

fnremoveremove(s : T(a), elem : a, to_key : a -> String) : T(a)#

Remove all observed tags for elem (concurrent adds in-flight survive).

fnsetset(r : T(a), new_val : a, actor_id : String) : T(a)#

Write a new value, advancing the actor's clock slot.

fnsizesize(s : T(a)) : Int#

Number of elements with at least one tag.

fnvaluevalue(c : T) : Int#

Current value: sum of increments minus sum of decrements.

fnvaluevalue(c : T) : Int#

Sum of all actor slots.