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.
7	import Base
8	import bend-kit-bytes@0.3.3.0/bytes.bend as Bytes
9	import bend-kit-cbor@0.3.0.0/cbor.bend as Cbor
10	
11	# The counter with no increments.
12	def GCounter.new() -> List<&2, U32>:
13	  Nil{}
14	
15	# The count of replica i.
16	def 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.
26	def 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.
38	def 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.
46	def 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	
53	def 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.
61	def 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.
69	def 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	
78	def 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	
85	def 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.
93	def 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.
97	def 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	
106	def 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.
114	def 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	
121	def 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	
128	def 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.
136	def GCounter.to_cbor(s: List<&2, U32>) -> Cbor.Val:
137	  Cbor.Arr{GCounter.to_cbor.items(s)}
138	
139	def 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	
146	def 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	
154	def 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	
161	def 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	
168	def 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.
176	def 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.
184	def GCounter.encode(s: List<&2, U32>) -> Maybe<&1, Bytes.Bytes>:
185	  Cbor.encode(GCounter.to_cbor(s))
186	
187	def 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.
195	def 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.
200	type KCounter<-K: Data> is Data:
201	  KNil{}
202	  KCon{id: K, count: U32, rest: KCounter<K>}
203	
204	# The counter with no increments.
205	def KCounter.new(-K: Data) -> KCounter<K>:
206	  KNil{}
207	
208	# cmp(x, first ID of b), or EQ when b is empty.
209	def 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.
217	def 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	
224	def 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.
234	def 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.
242	def 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.
256	def 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.
260	def 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	
267	def 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.
275	def 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).
283	def 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.
295	def 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	
298	def 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.
306	def 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.
310	def 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.
318	def 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.
326	def 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	
333	def 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	
340	def 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.
348	def 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	
351	def 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	
358	def 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	
366	def 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	
373	def 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	
380	def 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.
388	def 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.
398	def 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	
401	def 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.
411	def 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)