crdt/causal
one replica's n-th event.
Since: crdt-spice-plan C2
Dot
(defstruct Dot [replica : Sym counter : int])
mk-dot
(mk-dot [r : Sym n : int] :)
mint a dot.
| r | the replica | |
| n | its counter value for this event |
The Dot (r, n).
(mk-dot (quote alice) 3)
Since: crdt-spice-plan C2
dot-replica
(dot-replica [^borrow d : Dot] :)
the replica that minted this dot.
| d | the dot |
Its replica.
(dot-replica (mk-dot (quote alice) 3)) ; => alice
Since: crdt-spice-plan C2
dot-counter
(dot-counter [^borrow d : Dot] :)
the counter value of this dot.
| d | the dot |
Its counter.
(dot-counter (mk-dot (quote alice) 3)) ; => 3
Since: crdt-spice-plan C2
DotContext
(defstruct DotContext [seen : int])
the causal history a replica has observed.
Since: crdt-spice-plan C2
dotctx-new
(dotctx-new :)
an empty causal history.
A DotContext that has observed nothing.
(dotctx-new)
Since: crdt-spice-plan C2
dotctx-witness
(dotctx-witness [c : DotContext ^borrow d : Dot] :)
record that a dot has been observed.
| c | the context | |
| d | the dot |
A new DotContext including d.
(dotctx-witness (dotctx-new) (mk-dot (quote alice) 1))
Since: crdt-spice-plan C2
dotctx-seen?
(dotctx-seen? [^borrow c : DotContext ^borrow d : Dot] :)
has this dot been observed?
| c | the context | |
| d | the dot |
true when the context's counter for d's replica is at least d's.
(dotctx-seen? ctx (mk-dot (quote alice) 1))
Since: crdt-spice-plan C2
dotctx-next
(dotctx-next [^borrow c : DotContext r : Sym] :)
the next dot this replica may mint.
| c | the context | |
| r | the replica |
The dot one past the highest this context has for r.
(dotctx-next ctx (quote alice))
Since: crdt-spice-plan C2
dotctx-count
(dotctx-count [^borrow c : DotContext] :)
how many replicas this context has heard from.
| c | the context |
The number of distinct replicas in the version vector.
(dotctx-count ctx) ; => 2
Since: crdt-spice-plan C2
DotSet
(defstruct DotSet [dots : int])
an EXACT set of dots.
Since: crdt-spice-plan C4
dotset-new
(dotset-new :)
an empty dot set.
A DotSet holding no dots.
(dotset-new)
Since: crdt-spice-plan C4
dotset-add
(dotset-add [s : DotSet ^borrow d : Dot] :)
add one dot.
| s | the set | |
| d | the dot |
A new DotSet containing d.
(dotset-add (dotset-new) (mk-dot (quote alice) 3))
Since: crdt-spice-plan C4
dotset-has?
(dotset-has? [^borrow s : DotSet ^borrow d : Dot] :)
is this exact dot in the set?
| s | the set | |
| d | the dot |
true only for the dot itself -- never for an earlier one, which is the whole difference from dotctx-seen?.
(dotset-has? s (mk-dot (quote alice) 3))
Since: crdt-spice-plan C4
dotset-count
(dotset-count [^borrow s : DotSet] :)
how many dots the set holds.
| s | the set |
The total over every replica.
(dotset-count s) ; => 2
Since: crdt-spice-plan C4
dotset-union
(dotset-union [a : DotSet b : DotSet] :)
every dot from both sets.
| a | first set | |
| b | second set |
Their union.
(dotset-union x y)
Since: crdt-spice-plan C4
dotctx-witness-set
(dotctx-witness-set [c : DotContext ^borrow s : DotSet] :)
record every dot of a DotSet as observed.
| c | the context | |
| s | the exact dots to witness |
A DotContext that has observed all of them.
(dotctx-witness-set ctx (dotset-add (dotset-new) (mk-dot (quote alice) 3)))
Since: crdt-spice-plan C4
Internal definitions
__inner-dots-- internal: one replica's counter set, or a fresh empty one.__dotset-count-loop-- internal.__dotset-union-loop-- internal: fold b's replicas into acc.__counters-union-- internal: union two counter sets.__counters-union-loop-- internal.JoinSemilattice[DotSet]-- union.BoundedJoin[DotSet]-- the empty set is the least element.Eq[DotSet]-- same number of dots.__witness-reps-loop-- internal: witness each replica's counters.__max-counter-- internal: the highest counter in a counter set.__max-counter-loop-- internal.__imax__cx-- internal: the larger of two ints.JoinSemilattice[DotContext]-- pointwise maximum of the version vectors.BoundedJoin[DotContext]-- the empty history is the least element.Eq[DotContext]-- same replicas, same counters.__dotctx-sum-- internal: sum of the counters, a cheap content digest.__sum-loop__cx-- internal.