crdt.bend
bend-kit-crdt@0.1.1.0 · 414 lines · 0 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.2.0/bytes.bend as Bytes
9import bend-kit-cbor@0.2.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)