crdt.bend
bend-kit-crdt@0.1.0.0 · 195 lines · 0 definitions
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.
6import Base
7import bend-kit-bytes@0.3.2.0/bytes.bend as Bytes
8import bend-kit-cbor@0.2.0.0/cbor.bend as Cbor
9
10# The counter with no increments.
11def GCounter.new() -> List<&2, U32>:
12 Nil{}
13
14# The count of replica i.
15def 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.
25def 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.
37def 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.
45def 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
52def 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.
60def 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.
68def 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
77def 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
84def 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.
92def 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.
96def 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
105def 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.
113def 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
120def 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
127def 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.
135def GCounter.to_cbor(s: List<&2, U32>) -> Cbor.Val:
136 Cbor.Arr{GCounter.to_cbor.items(s)}
137
138def 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
145def 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
153def 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
160def 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
167def 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.
175def 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.
183def GCounter.encode(s: List<&2, U32>) -> Maybe<&1, Bytes.Bytes>:
184 Cbor.encode(GCounter.to_cbor(s))
185
186def 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.
194def GCounter.decode(b: Bytes.Bytes, +cap: U32) -> Maybe<&2, List<&2, U32>>:
195 GCounter.decode.go(Cbor.decode(b), cap)