crdt.bend

bend-kit-crdt@0.2.0.0 · 414 lines · 56 definitions

1# Replicated data types: grow-only counters with proved merges. Source: https://github.com/paymog/bend-kit/tree/main/crdt
2#
3# A GCounter is a list of U32 counts. Entry i is the count of replica i, and a
4# missing entry counts as 0. This is the state-based G-Counter of Shapiro et
5# al. (2011). Each replica must increment only its own entry. A KCounter is the
6# same counter keyed by sparse replica IDs of any Data type.
7import Base
8import bend-kit-bytes@0.3.3.0/bytes.bend as Bytes
9import bend-kit-cbor@0.3.0.0/cbor.bend as Cbor
10
11# The counter with no increments.
12def GCounter.new() -> List<&2, U32>:
13  Nil{}
14
15# The count of replica i.
16def GCounter.get(s: List<&2, U32>, i: Nat) -> U32:
17  match s i:
18    case Nil{} _:
19      0
20    case Con{c, t} 0n:
21      c
22    case Con{c, t} 1n+p:
23      GCounter.get(t, p)
24
25# Component-wise maximum. It is commutative, associative, and idempotent.
26def GCounter.merge(a: List<&2, U32>, b: List<&2, U32>) -> List<&2, U32>:
27  match a b:
28    case Nil{} Nil{}:
29      Nil{}
30    case Nil{} Con{y, ys}:
31      Con{y, ys}
32    case Con{x, xs} Nil{}:
33      Con{x, xs}
34    case Con{x, xs} Con{y, ys}:
35      Con{U32.max(x, y), GCounter.merge(xs, ys)}
36
37# The merge of every state in the list.
38def GCounter.merge_all(xs: List<&2, List<&2, U32>>) -> List<&2, U32>:
39  match xs:
40    case Nil{}:
41      Nil{}
42    case Con{x, t}:
43      GCounter.merge(x, GCounter.merge_all(t))
44
45# Zeros for replicas 0 to i - 1, then 1 for replica i.
46def GCounter.pad(i: Nat) -> List<&2, U32>:
47  match i:
48    case 0n:
49      [1]
50    case 1n+p:
51      Con{0, GCounter.pad(p)}
52
53def GCounter.cons(c: U32, m: Maybe<&2, List<&2, U32>>) -> Maybe<&2, List<&2, U32>>:
54  match m:
55    case None{}:
56      None{}
57    case Some{t}:
58      Some{Con{c, t}}
59
60# ok is false when n wrapped to 0.
61def GCounter.inc.at(ok: Bool, n: U32, t: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
62  match ok:
63    case True{}:
64      Some{Con{n, t}}
65    case False{}:
66      None{}
67
68# Adds 1 to the count of replica i. None when that count is 4294967295.
69def GCounter.inc(s: List<&2, U32>, i: Nat) -> Maybe<&2, List<&2, U32>>:
70  match s i:
71    case Nil{} _:
72      Some{GCounter.pad(i)}
73    case Con{+c, t} 0n:
74      GCounter.inc.at(U32.is_lt(c, U32.inc(c)), U32.inc(c), t)
75    case Con{c, t} 1n+p:
76      GCounter.cons(c, GCounter.inc(t, p))
77
78def GCounter.add(m: Maybe<&2, U32>, +c: U32) -> Maybe<&2, U32>:
79  match m:
80    case None{}:
81      None{}
82    case Some{+a}:
83      Bool.pick(Maybe<&2, U32>, U32.is_le(a, (a + c : U32)), Some{(a + c : U32)}, None{})
84
85def GCounter.value.go(s: List<&2, U32>, acc: Maybe<&2, U32>) -> Maybe<&2, U32>:
86  match s:
87    case Nil{}:
88      acc
89    case Con{c, t}:
90      GCounter.value.go(t, GCounter.add(acc, c))
91
92# The sum of all counts. None when the sum does not fit in a U32.
93def GCounter.value(s: List<&2, U32>) -> Maybe<&2, U32>:
94  GCounter.value.go(s, Some{0})
95
96# True when a is at most b in every entry.
97def GCounter.le(a: List<&2, U32>, b: List<&2, U32>) -> Bool:
98  match a b:
99    case Nil{} _:
100      True{}
101    case Con{x, xs} Nil{}:
102      Bool.and(U32.is_eq(x, 0), GCounter.le(xs, Nil{}))
103    case Con{x, xs} Con{y, ys}:
104      Bool.and(U32.is_le(x, y), GCounter.le(xs, ys))
105
106def GCounter.valid.go(t: List<&2, U32>, last: U32) -> Bool:
107  match t:
108    case Nil{}:
109      U32.is_ne(last, 0)
110    case Con{c, u}:
111      GCounter.valid.go(u, c)
112
113# A valid state has no trailing 0, so each count vector has one form.
114def GCounter.valid(s: List<&2, U32>) -> Bool:
115  match s:
116    case Nil{}:
117      True{}
118    case Con{c, t}:
119      GCounter.valid.go(t, c)
120
121def GCounter.size(s: List<&2, U32>) -> U32:
122  match s:
123    case Nil{}:
124      0
125    case Con{c, t}:
126      (1 + GCounter.size(t) : U32)
127
128def GCounter.to_cbor.items(s: List<&2, U32>) -> List<&1, Cbor.Val>:
129  match s:
130    case Nil{}:
131      Nil{}
132    case Con{c, t}:
133      Con{Cbor.UInt{Cbor.W64{0, c}}, GCounter.to_cbor.items(t)}
134
135# A CBOR array of unsigned integers: the count of replica i is item i.
136def GCounter.to_cbor(s: List<&2, U32>) -> Cbor.Val:
137  Cbor.Arr{GCounter.to_cbor.items(s)}
138
139def GCounter.from_cbor.word(ok: Bool, lo: U32, rest: Maybe<&2, List<&2, U32>>) -> Maybe<&2, List<&2, U32>>:
140  match ok:
141    case True{}:
142      GCounter.cons(lo, rest)
143    case False{}:
144      None{}
145
146def GCounter.from_cbor.item(v: Cbor.Val, rest: Maybe<&2, List<&2, U32>>) -> Maybe<&2, List<&2, U32>>:
147  match v:
148    case Cbor.UInt{w}:
149      Cbor.W64{+hi, lo} = w
150      GCounter.from_cbor.word(U32.is_eq(hi, 0), lo, rest)
151    case _:
152      None{}
153
154def GCounter.from_cbor.items(xs: List<&1, Cbor.Val>) -> Maybe<&2, List<&2, U32>>:
155  match xs:
156    case Nil{}:
157      Some{Nil{}}
158    case Con{v, t}:
159      GCounter.from_cbor.item(v, GCounter.from_cbor.items(t))
160
161def GCounter.from_cbor.gate(ok: Bool, s: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
162  match ok:
163    case True{}:
164      Some{s}
165    case False{}:
166      None{}
167
168def GCounter.from_cbor.check(m: Maybe<&2, List<&2, U32>>, +cap: U32) -> Maybe<&2, List<&2, U32>>:
169  match m:
170    case None{}:
171      None{}
172    case Some{+s}:
173      GCounter.from_cbor.gate(Bool.and(GCounter.valid(s), U32.is_le(GCounter.size(s), cap)), s)
174
175# A valid state with at most cap replicas, or None.
176def GCounter.from_cbor(v: Cbor.Val, +cap: U32) -> Maybe<&2, List<&2, U32>>:
177  match v:
178    case Cbor.Arr{xs}:
179      GCounter.from_cbor.check(GCounter.from_cbor.items(xs), cap)
180    case _:
181      None{}
182
183# Always Some: every item is an unsigned integer.
184def GCounter.encode(s: List<&2, U32>) -> Maybe<&1, Bytes.Bytes>:
185  Cbor.encode(GCounter.to_cbor(s))
186
187def GCounter.decode.go(m: Maybe<&1, Cbor.Val>, +cap: U32) -> Maybe<&2, List<&2, U32>>:
188  match m:
189    case None{}:
190      None{}
191    case Some{v}:
192      GCounter.from_cbor(v, cap)
193
194# CBOR bytes to a valid state with at most cap replicas, or None.
195def GCounter.decode(b: Bytes.Bytes, +cap: U32) -> Maybe<&2, List<&2, U32>>:
196  GCounter.decode.go(Cbor.decode(b), cap)
197
198# A G-Counter keyed by replica IDs. A valid state lists IDs in ascending cmp
199# order, each with a count above 0.
200type KCounter<-K: Data> is Data:
201  KNil{}
202  KCon{id: K, count: U32, rest: KCounter<K>}
203
204# The counter with no increments.
205def KCounter.new(-K: Data) -> KCounter<K>:
206  KNil{}
207
208# cmp(x, first ID of b), or EQ when b is empty.
209def KCounter.head(~K: Data, ~cmp: K -> K -> Cmp, +x: K, b: KCounter<K>) -> Cmp:
210  match b:
211    case KNil{}:
212      EQ{}
213    case KCon{y, d, t}:
214      cmp(x, y)
215
216# The comparison of the first IDs of a and b, or EQ when either is empty.
217def KCounter.heads(~K: Data, ~cmp: K -> K -> Cmp, a: KCounter<K>, b: KCounter<K>) -> Cmp:
218  match a:
219    case KNil{}:
220      EQ{}
221    case KCon{x, c, r}:
222      KCounter.head(~K, ~cmp, x, b)
223
224def KCounter.hit(c: Cmp, n: U32) -> U32:
225  match c:
226    case LT{}:
227      0
228    case EQ{}:
229      n
230    case GT{}:
231      0
232
233# The count of replica k: the largest count under an ID that cmp makes equal to k.
234def KCounter.get(~K: Data, ~cmp: K -> K -> Cmp, s: KCounter<K>, +k: K) -> U32:
235  match s:
236    case KNil{}:
237      0
238    case KCon{id, c, r}:
239      U32.max(KCounter.hit(cmp(k, id), c), KCounter.get(~K, ~cmp, r, k))
240
241# q is KCounter.heads(a, b). Passing it in lets match pick the step without closures.
242def KCounter.merge.go(~K: Data, ~cmp: K -> K -> Cmp, +a: KCounter<K>, +b: KCounter<K>, q: Cmp) -> KCounter<K>:
243  match a b q:
244    case KNil{} _ _:
245      b
246    case KCon{x, c, r} KNil{} _:
247      KCon{x, c, r}
248    case KCon{+x, +c, +r} KCon{+y, +d, +t} LT{}:
249      KCon{x, c, KCounter.merge.go(~K, ~cmp, r, KCon{y, d, t}, KCounter.heads(~K, ~cmp, r, KCon{y, d, t}))}
250    case KCon{+x, +c, +r} KCon{+y, +d, +t} EQ{}:
251      KCon{x, U32.max(c, d), KCounter.merge.go(~K, ~cmp, r, t, KCounter.heads(~K, ~cmp, r, t))}
252    case KCon{+x, +c, +r} KCon{+y, +d, +t} GT{}:
253      KCon{y, d, KCounter.merge.go(~K, ~cmp, KCon{x, c, r}, t, KCounter.head(~K, ~cmp, x, t))}
254
255# The union of two ID-sorted states, with the maximum count where IDs are equal.
256def KCounter.merge(~K: Data, ~cmp: K -> K -> Cmp, +a: KCounter<K>, +b: KCounter<K>) -> KCounter<K>:
257  KCounter.merge.go(~K, ~cmp, a, b, KCounter.heads(~K, ~cmp, a, b))
258
259# The merge of every state in the list.
260def KCounter.merge_all(~K: Data, ~cmp: K -> K -> Cmp, xs: List<&2, KCounter<K>>) -> KCounter<K>:
261  match xs:
262    case Nil{}:
263      KNil{}
264    case Con{x, t}:
265      KCounter.merge(~K, ~cmp, x, KCounter.merge_all(~K, ~cmp, t))
266
267def KCounter.cons(-K: Data, k: K, c: U32, m: Maybe<&2, KCounter<K>>) -> Maybe<&2, KCounter<K>>:
268  match m:
269    case None{}:
270      None{}
271    case Some{t}:
272      Some{KCon{k, c, t}}
273
274# ok is false when n wrapped to 0.
275def KCounter.inc.at(-K: Data, ok: Bool, x: K, n: U32, r: KCounter<K>) -> Maybe<&2, KCounter<K>>:
276  match ok:
277    case True{}:
278      Some{KCon{x, n, r}}
279    case False{}:
280      None{}
281
282# q is KCounter.head(k, s).
283def KCounter.inc.go(~K: Data, ~cmp: K -> K -> Cmp, s: KCounter<K>, +k: K, q: Cmp) -> Maybe<&2, KCounter<K>>:
284  match s q:
285    case KNil{} _:
286      Some{KCon{k, 1, KNil{}}}
287    case KCon{+x, +c, +r} LT{}:
288      Some{KCon{k, 1, KCon{x, c, r}}}
289    case KCon{+x, +c, +r} EQ{}:
290      KCounter.inc.at(K, U32.is_lt(c, U32.inc(c)), x, U32.inc(c), r)
291    case KCon{+x, +c, +r} GT{}:
292      KCounter.cons(K, x, c, KCounter.inc.go(~K, ~cmp, r, k, KCounter.head(~K, ~cmp, k, r)))
293
294# Adds 1 to the count of replica k. None when that count is 4294967295.
295def KCounter.inc(~K: Data, ~cmp: K -> K -> Cmp, +s: KCounter<K>, +k: K) -> Maybe<&2, KCounter<K>>:
296  KCounter.inc.go(~K, ~cmp, s, k, KCounter.head(~K, ~cmp, k, s))
297
298def KCounter.value.go(-K: Data, s: KCounter<K>, acc: Maybe<&2, U32>) -> Maybe<&2, U32>:
299  match s:
300    case KNil{}:
301      acc
302    case KCon{x, c, r}:
303      KCounter.value.go(K, r, GCounter.add(acc, c))
304
305# The sum of all counts. None when the sum does not fit in a U32.
306def KCounter.value(-K: Data, s: KCounter<K>) -> Maybe<&2, U32>:
307  KCounter.value.go(K, s, Some{0})
308
309# True when each count in a is at most the count of its ID in b.
310def KCounter.le(~K: Data, ~cmp: K -> K -> Cmp, a: KCounter<K>, +b: KCounter<K>) -> Bool:
311  match a:
312    case KNil{}:
313      True{}
314    case KCon{x, c, r}:
315      Bool.and(U32.is_le(c, KCounter.get(~K, ~cmp, b, x)), KCounter.le(~K, ~cmp, r, b))
316
317# True when s is empty or its first ID is above lo.
318def KCounter.above(~K: Data, ~cmp: K -> K -> Cmp, s: KCounter<K>, +lo: K) -> Bool:
319  match s:
320    case KNil{}:
321      True{}
322    case KCon{x, c, r}:
323      Cmp.is_lt(cmp(lo, x))
324
325# A valid state has strictly ascending IDs and no 0 count, so each counter has one form.
326def KCounter.valid(~K: Data, ~cmp: K -> K -> Cmp, s: KCounter<K>) -> Bool:
327  match s:
328    case KNil{}:
329      True{}
330    case KCon{+x, c, +r}:
331      Bool.and(Bool.and(U32.is_ne(c, 0), KCounter.above(~K, ~cmp, r, x)), KCounter.valid(~K, ~cmp, r))
332
333def KCounter.size(-K: Data, s: KCounter<K>) -> U32:
334  match s:
335    case KNil{}:
336      0
337    case KCon{x, c, r}:
338      (1 + KCounter.size(K, r) : U32)
339
340def KCounter.to_cbor.items(~K: Data, ~enc: K -> Cbor.Val, s: KCounter<K>) -> List<&1, Cbor.Val & Cbor.Val>:
341  match s:
342    case KNil{}:
343      Nil{}
344    case KCon{x, c, r}:
345      Con{(enc(x), Cbor.UInt{Cbor.W64{0, c}}), KCounter.to_cbor.items(~K, ~enc, r)}
346
347# A CBOR map from each encoded ID to its count, in ID order.
348def KCounter.to_cbor(~K: Data, ~enc: K -> Cbor.Val, s: KCounter<K>) -> Cbor.Val:
349  Cbor.Obj{KCounter.to_cbor.items(~K, ~enc, s)}
350
351def KCounter.from_cbor.word(-K: Data, ok: Bool, mk: Maybe<&2, K>, lo: U32, rest: Maybe<&2, KCounter<K>>) -> Maybe<&2, KCounter<K>>:
352  match ok mk:
353    case True{} Some{k}:
354      KCounter.cons(K, k, lo, rest)
355    case _ _:
356      None{}
357
358def KCounter.from_cbor.count(-K: Data, v: Cbor.Val, mk: Maybe<&2, K>, rest: Maybe<&2, KCounter<K>>) -> Maybe<&2, KCounter<K>>:
359  match v:
360    case Cbor.UInt{w}:
361      Cbor.W64{+hi, lo} = w
362      KCounter.from_cbor.word(K, U32.is_eq(hi, 0), mk, lo, rest)
363    case _:
364      None{}
365
366def KCounter.from_cbor.items(~K: Data, ~dec: Cbor.Val -> Maybe<&2, K>, xs: List<&1, Cbor.Val & Cbor.Val>) -> Maybe<&2, KCounter<K>>:
367  match xs:
368    case Nil{}:
369      Some{KNil{}}
370    case Con{(k, v), t}:
371      KCounter.from_cbor.count(K, v, dec(k), KCounter.from_cbor.items(~K, ~dec, t))
372
373def KCounter.from_cbor.gate(-K: Data, ok: Bool, s: KCounter<K>) -> Maybe<&2, KCounter<K>>:
374  match ok:
375    case True{}:
376      Some{s}
377    case False{}:
378      None{}
379
380def KCounter.from_cbor.check(~K: Data, ~cmp: K -> K -> Cmp, m: Maybe<&2, KCounter<K>>, +cap: U32) -> Maybe<&2, KCounter<K>>:
381  match m:
382    case None{}:
383      None{}
384    case Some{+s}:
385      KCounter.from_cbor.gate(K, Bool.and(KCounter.valid(~K, ~cmp, s), U32.is_le(KCounter.size(K, s), cap)), s)
386
387# A valid state with at most cap replicas, or None. dec reads one ID.
388def KCounter.from_cbor(
389  ~K: Data, ~cmp: K -> K -> Cmp, ~dec: Cbor.Val -> Maybe<&2, K>, v: Cbor.Val, +cap: U32
390) -> Maybe<&2, KCounter<K>>:
391  match v:
392    case Cbor.Obj{kvs}:
393      KCounter.from_cbor.check(~K, ~cmp, KCounter.from_cbor.items(~K, ~dec, kvs), cap)
394    case _:
395      None{}
396
397# None only when enc gives a value with no CBOR form.
398def KCounter.encode(~K: Data, ~enc: K -> Cbor.Val, s: KCounter<K>) -> Maybe<&1, Bytes.Bytes>:
399  Cbor.encode(KCounter.to_cbor(~K, ~enc, s))
400
401def KCounter.decode.go(
402  ~K: Data, ~cmp: K -> K -> Cmp, ~dec: Cbor.Val -> Maybe<&2, K>, m: Maybe<&1, Cbor.Val>, +cap: U32
403) -> Maybe<&2, KCounter<K>>:
404  match m:
405    case None{}:
406      None{}
407    case Some{v}:
408      KCounter.from_cbor(~K, ~cmp, ~dec, v, cap)
409
410# CBOR bytes to a valid state with at most cap replicas, or None.
411def KCounter.decode(
412  ~K: Data, ~cmp: K -> K -> Cmp, ~dec: Cbor.Val -> Maybe<&2, K>, b: Bytes.Bytes, +cap: U32
413) -> Maybe<&2, KCounter<K>>:
414  KCounter.decode.go(~K, ~cmp, ~dec, Cbor.decode(b), cap)