1	# Replicated data types: a grow-only counter with a proved merge. 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.
6	import Base
7	import bend-kit-bytes@0.3.2.0/bytes.bend as Bytes
8	import bend-kit-cbor@0.2.0.0/cbor.bend as Cbor
9	
10	# The counter with no increments.
11	def GCounter.new() -> List<&2, U32>:
12	  Nil{}
13	
14	# The count of replica i.
15	def GCounter.get(s: List<&2, U32>, i: Nat) -> U32:
16	  match s i:
17	    case Nil{} _:
18	      0
19	    case Con{c, t} 0n:
20	      c
21	    case Con{c, t} 1n+p:
22	      GCounter.get(t, p)
23	
24	# Component-wise maximum. It is commutative, associative, and idempotent.
25	def GCounter.merge(a: List<&2, U32>, b: List<&2, U32>) -> List<&2, U32>:
26	  match a b:
27	    case Nil{} Nil{}:
28	      Nil{}
29	    case Nil{} Con{y, ys}:
30	      Con{y, ys}
31	    case Con{x, xs} Nil{}:
32	      Con{x, xs}
33	    case Con{x, xs} Con{y, ys}:
34	      Con{U32.max(x, y), GCounter.merge(xs, ys)}
35	
36	# The merge of every state in the list.
37	def GCounter.merge_all(xs: List<&2, List<&2, U32>>) -> List<&2, U32>:
38	  match xs:
39	    case Nil{}:
40	      Nil{}
41	    case Con{x, t}:
42	      GCounter.merge(x, GCounter.merge_all(t))
43	
44	# Zeros for replicas 0 to i - 1, then 1 for replica i.
45	def GCounter.pad(i: Nat) -> List<&2, U32>:
46	  match i:
47	    case 0n:
48	      [1]
49	    case 1n+p:
50	      Con{0, GCounter.pad(p)}
51	
52	def GCounter.cons(c: U32, m: Maybe<&2, List<&2, U32>>) -> Maybe<&2, List<&2, U32>>:
53	  match m:
54	    case None{}:
55	      None{}
56	    case Some{t}:
57	      Some{Con{c, t}}
58	
59	# ok is false when n wrapped to 0.
60	def GCounter.inc.at(ok: Bool, n: U32, t: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
61	  match ok:
62	    case True{}:
63	      Some{Con{n, t}}
64	    case False{}:
65	      None{}
66	
67	# Adds 1 to the count of replica i. None when that count is 4294967295.
68	def GCounter.inc(s: List<&2, U32>, i: Nat) -> Maybe<&2, List<&2, U32>>:
69	  match s i:
70	    case Nil{} _:
71	      Some{GCounter.pad(i)}
72	    case Con{+c, t} 0n:
73	      GCounter.inc.at(U32.is_lt(c, U32.inc(c)), U32.inc(c), t)
74	    case Con{c, t} 1n+p:
75	      GCounter.cons(c, GCounter.inc(t, p))
76	
77	def GCounter.add(m: Maybe<&2, U32>, +c: U32) -> Maybe<&2, U32>:
78	  match m:
79	    case None{}:
80	      None{}
81	    case Some{+a}:
82	      Bool.pick(Maybe<&2, U32>, U32.is_le(a, (a + c : U32)), Some{(a + c : U32)}, None{})
83	
84	def GCounter.value.go(s: List<&2, U32>, acc: Maybe<&2, U32>) -> Maybe<&2, U32>:
85	  match s:
86	    case Nil{}:
87	      acc
88	    case Con{c, t}:
89	      GCounter.value.go(t, GCounter.add(acc, c))
90	
91	# The sum of all counts. None when the sum does not fit in a U32.
92	def GCounter.value(s: List<&2, U32>) -> Maybe<&2, U32>:
93	  GCounter.value.go(s, Some{0})
94	
95	# True when a is at most b in every entry.
96	def GCounter.le(a: List<&2, U32>, b: List<&2, U32>) -> Bool:
97	  match a b:
98	    case Nil{} _:
99	      True{}
100	    case Con{x, xs} Nil{}:
101	      Bool.and(U32.is_eq(x, 0), GCounter.le(xs, Nil{}))
102	    case Con{x, xs} Con{y, ys}:
103	      Bool.and(U32.is_le(x, y), GCounter.le(xs, ys))
104	
105	def GCounter.valid.go(t: List<&2, U32>, last: U32) -> Bool:
106	  match t:
107	    case Nil{}:
108	      U32.is_ne(last, 0)
109	    case Con{c, u}:
110	      GCounter.valid.go(u, c)
111	
112	# A valid state has no trailing 0, so each count vector has one form.
113	def GCounter.valid(s: List<&2, U32>) -> Bool:
114	  match s:
115	    case Nil{}:
116	      True{}
117	    case Con{c, t}:
118	      GCounter.valid.go(t, c)
119	
120	def GCounter.size(s: List<&2, U32>) -> U32:
121	  match s:
122	    case Nil{}:
123	      0
124	    case Con{c, t}:
125	      (1 + GCounter.size(t) : U32)
126	
127	def GCounter.to_cbor.items(s: List<&2, U32>) -> List<&1, Cbor.Val>:
128	  match s:
129	    case Nil{}:
130	      Nil{}
131	    case Con{c, t}:
132	      Con{Cbor.UInt{Cbor.W64{0, c}}, GCounter.to_cbor.items(t)}
133	
134	# A CBOR array of unsigned integers: the count of replica i is item i.
135	def GCounter.to_cbor(s: List<&2, U32>) -> Cbor.Val:
136	  Cbor.Arr{GCounter.to_cbor.items(s)}
137	
138	def GCounter.from_cbor.word(ok: Bool, lo: U32, rest: Maybe<&2, List<&2, U32>>) -> Maybe<&2, List<&2, U32>>:
139	  match ok:
140	    case True{}:
141	      GCounter.cons(lo, rest)
142	    case False{}:
143	      None{}
144	
145	def GCounter.from_cbor.item(v: Cbor.Val, rest: Maybe<&2, List<&2, U32>>) -> Maybe<&2, List<&2, U32>>:
146	  match v:
147	    case Cbor.UInt{w}:
148	      Cbor.W64{+hi, lo} = w
149	      GCounter.from_cbor.word(U32.is_eq(hi, 0), lo, rest)
150	    case _:
151	      None{}
152	
153	def GCounter.from_cbor.items(xs: List<&1, Cbor.Val>) -> Maybe<&2, List<&2, U32>>:
154	  match xs:
155	    case Nil{}:
156	      Some{Nil{}}
157	    case Con{v, t}:
158	      GCounter.from_cbor.item(v, GCounter.from_cbor.items(t))
159	
160	def GCounter.from_cbor.gate(ok: Bool, s: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
161	  match ok:
162	    case True{}:
163	      Some{s}
164	    case False{}:
165	      None{}
166	
167	def GCounter.from_cbor.check(m: Maybe<&2, List<&2, U32>>, +cap: U32) -> Maybe<&2, List<&2, U32>>:
168	  match m:
169	    case None{}:
170	      None{}
171	    case Some{+s}:
172	      GCounter.from_cbor.gate(Bool.and(GCounter.valid(s), U32.is_le(GCounter.size(s), cap)), s)
173	
174	# A valid state with at most cap replicas, or None.
175	def GCounter.from_cbor(v: Cbor.Val, +cap: U32) -> Maybe<&2, List<&2, U32>>:
176	  match v:
177	    case Cbor.Arr{xs}:
178	      GCounter.from_cbor.check(GCounter.from_cbor.items(xs), cap)
179	    case _:
180	      None{}
181	
182	# Always Some: every item is an unsigned integer.
183	def GCounter.encode(s: List<&2, U32>) -> Maybe<&1, Bytes.Bytes>:
184	  Cbor.encode(GCounter.to_cbor(s))
185	
186	def GCounter.decode.go(m: Maybe<&1, Cbor.Val>, +cap: U32) -> Maybe<&2, List<&2, U32>>:
187	  match m:
188	    case None{}:
189	      None{}
190	    case Some{v}:
191	      GCounter.from_cbor(v, cap)
192	
193	# CBOR bytes to a valid state with at most cap replicas, or None.
194	def GCounter.decode(b: Bytes.Bytes, +cap: U32) -> Maybe<&2, List<&2, U32>>:
195	  GCounter.decode.go(Cbor.decode(b), cap)