src/containers/bitlist.bend
bend-collections-laws-containers@1.0.0.0 · 338 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/src/containers/bitset.bend as B
3import bend-collections-laws-containers@1.0.0.0/src/containers/dynamic_array.bend as D
4import bend-collections-laws-containers@1.0.0.0/src/containers/types/dynamic_array.bend as DE
5import bend-collections-laws-containers@1.0.0.0/src/containers/types/bitlist.bend as E
6
7# Packed growable bit list (SSZ-style Bitlist[N]).
8#
9# A bitlist is an ordered sequence of `len` bits with a maximum length
10# `limit` (N). Bits are stored LSB-first in a dynamic array of 32-bit words:
11# bit i lives in word i/32 at bit position i%32. The array holds at least
12# ceil(len/32) words and every stored bit at a position >= len is zero (the
13# masked tail). pop never shrinks the word array, so a later push reuses the
14# zeroed word; push appends a word only when every stored bit is in use.
15#
16# Errors never change the state: get/assign with index >= len fail with
17# IndexOutOfRange, push at len == limit fails with Full, pop of an empty
18# list fails with Empty.
19#
20# Capacity: the word array is a dynamic array of depth limit 31 (2^31
21# words), so a bitlist holds at most 2^36 bits; a push past that fails with
22# Full exactly like a push past the limit. new() has no limit (None);
23# with_limit(n) is Bitlist[n].
24#
25# Cost: length/limit O(1); get one word read; assign one word read and one
26# write; push amortized O(1) (a word read and write, or one append; pushing
27# a zero bit into allocated space only bumps the length); pop one word read
28# and at most one write; count O(words); to_list O(len); clear O(capacity).
29#
30# Correctness: proofs/containers/bitlist refines every operation against an
31# independent list-of-Bool specification.
32
33type Bitlist is Type:
34 BL{limit: Maybe<&2, Nat>, len: Nat, words: D.DynArray<&2, U32>}
35
36def new() -> Bitlist:
37 BL{None{}, 0n, D.new(U32)}
38
39def with_limit(+n: Nat) -> Bitlist:
40 BL{Some{n}, 0n, D.new(U32)}
41
42# Room for one more bit under the limit.
43def below(lim: Maybe<&2, Nat>, +n: Nat) -> Bool:
44 match lim:
45 case None{}:
46 True{}
47 case Some{k}:
48 Nat.is_lt(n, k)
49
50def length(s: Bitlist) -> Bitlist & Nat:
51 BL{lim, +n, w} = s
52 (BL{lim, n, w}, n)
53
54def limit(s: Bitlist) -> Bitlist & Maybe<&2, Nat>:
55 BL{+lim, n, w} = s
56 (BL{lim, n, w}, lim)
57
58# ---- get ----
59
60def get_word(+i: Nat, +lim: Maybe<&2, Nat>, +n: Nat, r: D.DynArray<&2, U32> & Result<&2, &2, DE.Error, U32>) -> Bitlist & Result<&2, &2, E.Error, Bool>:
61 match r:
62 case Tuple{w, Done{x}}:
63 (BL{lim, n, w}, Done{B.word_get(x, B.bitix(i))})
64 case Tuple{w, Fail{e}}:
65 (BL{lim, n, w}, Fail{E.IndexOutOfRange{}})
66
67def get_if(ok: Bool, +lim: Maybe<&2, Nat>, +n: Nat, w: D.DynArray<&2, U32>, +i: Nat) -> Bitlist & Result<&2, &2, E.Error, Bool>:
68 match ok:
69 case True{}:
70 get_word(i, lim, n, D.get(U32, w, B.wordix(i)))
71 case False{}:
72 (BL{lim, n, w}, Fail{E.IndexOutOfRange{}})
73
74def get(s: Bitlist, +i: Nat) -> Bitlist & Result<&2, &2, E.Error, Bool>:
75 BL{+lim, +n, w} = s
76 get_if(Nat.is_lt(i, n), lim, n, w, i)
77
78# ---- assign ----
79
80def assign_set(+lim: Maybe<&2, Nat>, +n: Nat, r: D.DynArray<&2, U32> & Result<&2, &2, DE.Error, Unit>) -> Bitlist & Result<&2, &2, E.Error, Unit>:
81 match r:
82 case Tuple{w, Done{u}}:
83 (BL{lim, n, w}, Done{Unit{}})
84 case Tuple{w, Fail{e}}:
85 (BL{lim, n, w}, Fail{E.IndexOutOfRange{}})
86
87# Rewrite bit i of its word (the word read is r); the list gets length n.
88def assign_word(+i: Nat, +v: Bool, +lim: Maybe<&2, Nat>, +n: Nat, r: D.DynArray<&2, U32> & Result<&2, &2, DE.Error, U32>) -> Bitlist & Result<&2, &2, E.Error, Unit>:
89 match r:
90 case Tuple{w, Done{+x}}:
91 assign_set(lim, n, D.set(U32, w, B.wordix(i), B.word_put(v, x, B.bitix(i))))
92 case Tuple{w, Fail{e}}:
93 (BL{lim, n, w}, Fail{E.IndexOutOfRange{}})
94
95def assign_if(ok: Bool, +lim: Maybe<&2, Nat>, +n: Nat, w: D.DynArray<&2, U32>, +i: Nat, +v: Bool) -> Bitlist & Result<&2, &2, E.Error, Unit>:
96 match ok:
97 case True{}:
98 assign_word(i, v, lim, n, D.get(U32, w, B.wordix(i)))
99 case False{}:
100 (BL{lim, n, w}, Fail{E.IndexOutOfRange{}})
101
102def assign(s: Bitlist, +i: Nat, +v: Bool) -> Bitlist & Result<&2, &2, E.Error, Unit>:
103 BL{+lim, +n, w} = s
104 assign_if(Nat.is_lt(i, n), lim, n, w, i, v)
105
106def set(s: Bitlist, +i: Nat) -> Bitlist & Result<&2, &2, E.Error, Unit>:
107 assign(s, i, True{})
108
109def unset(s: Bitlist, +i: Nat) -> Bitlist & Result<&2, &2, E.Error, Unit>:
110 assign(s, i, False{})
111
112# ---- push ----
113
114def push_new(+lim: Maybe<&2, Nat>, +n: Nat, r: D.DynArray<&2, U32> & Result<&2, &2, DE.Error, Unit>) -> Bitlist & Result<&2, &2, E.Error, Unit>:
115 match r:
116 case Tuple{w, Done{u}}:
117 (BL{lim, 1n+n, w}, Done{Unit{}})
118 case Tuple{w, Fail{e}}:
119 (BL{lim, n, w}, Fail{E.Full{}})
120
121# Bit n already lies in a stored word, where it is zero (masked tail).
122def push_in(+lim: Maybe<&2, Nat>, +n: Nat, w: D.DynArray<&2, U32>, +v: Bool) -> Bitlist & Result<&2, &2, E.Error, Unit>:
123 match v:
124 case False{}:
125 (BL{lim, 1n+n, w}, Done{Unit{}})
126 case True{}:
127 assign_word(n, True{}, lim, 1n+n, D.get(U32, w, B.wordix(n)))
128
129def push_where(inside: Bool, +lim: Maybe<&2, Nat>, +n: Nat, w: D.DynArray<&2, U32>, +v: Bool) -> Bitlist & Result<&2, &2, E.Error, Unit>:
130 match inside:
131 case True{}:
132 push_in(lim, n, w, v)
133 case False{}:
134 push_new(lim, n, D.push(U32, w, B.word_put(v, 0, 0n)))
135
136def push_room(+lim: Maybe<&2, Nat>, +n: Nat, +v: Bool, r: D.DynArray<&2, U32> & Nat) -> Bitlist & Result<&2, &2, E.Error, Unit>:
137 (w, +k) = r
138 push_where(Nat.is_lt(n, Nat.mul(k, 32n)), lim, n, w, v)
139
140def push_if(ok: Bool, +lim: Maybe<&2, Nat>, +n: Nat, w: D.DynArray<&2, U32>, +v: Bool) -> Bitlist & Result<&2, &2, E.Error, Unit>:
141 match ok:
142 case True{}:
143 push_room(lim, n, v, D.length(U32, w))
144 case False{}:
145 (BL{lim, n, w}, Fail{E.Full{}})
146
147def push(s: Bitlist, +v: Bool) -> Bitlist & Result<&2, &2, E.Error, Unit>:
148 BL{+lim, +n, w} = s
149 push_if(below(lim, n), lim, n, w, v)
150
151# ---- pop ----
152
153def pop_set(+lim: Maybe<&2, Nat>, +m: Nat, r: D.DynArray<&2, U32> & Result<&2, &2, DE.Error, Unit>) -> Bitlist & Result<&2, &2, E.Error, Bool>:
154 match r:
155 case Tuple{w, Done{u}}:
156 (BL{lim, m, w}, Done{True{}})
157 case Tuple{w, Fail{e}}:
158 (BL{lim, m, w}, Done{True{}})
159
160# The last bit b of word x: a set bit is cleared so the tail stays zero.
161def pop_bit(+lim: Maybe<&2, Nat>, +m: Nat, w: D.DynArray<&2, U32>, +x: U32, +b: Bool) -> Bitlist & Result<&2, &2, E.Error, Bool>:
162 match b:
163 case False{}:
164 (BL{lim, m, w}, Done{False{}})
165 case True{}:
166 pop_set(lim, m, D.set(U32, w, B.wordix(m), B.word_put(False{}, x, B.bitix(m))))
167
168def pop_word(+lim: Maybe<&2, Nat>, +m: Nat, r: D.DynArray<&2, U32> & Result<&2, &2, DE.Error, U32>) -> Bitlist & Result<&2, &2, E.Error, Bool>:
169 match r:
170 case Tuple{w, Done{+x}}:
171 pop_bit(lim, m, w, x, B.word_get(x, B.bitix(m)))
172 case Tuple{w, Fail{e}}:
173 (BL{lim, m, w}, Fail{E.Empty{}})
174
175def pop_at(+lim: Maybe<&2, Nat>, +n: Nat, w: D.DynArray<&2, U32>) -> Bitlist & Result<&2, &2, E.Error, Bool>:
176 match n:
177 case 0n:
178 (BL{lim, 0n, w}, Fail{E.Empty{}})
179 case 1n+ +m:
180 pop_word(lim, m, D.get(U32, w, B.wordix(m)))
181
182def pop(s: Bitlist) -> Bitlist & Result<&2, &2, E.Error, Bool>:
183 BL{+lim, +n, w} = s
184 pop_at(lim, n, w)
185
186# ---- clear ----
187
188def clear(s: Bitlist) -> Bitlist:
189 BL{lim, n, w} = s
190 BL{lim, 0n, D.clear(U32, w)}
191
192# ---- count ----
193
194def count_add(g: D.DynArray<&2, U32> & Result<&2, &2, DE.Error, U32>, +acc: Nat) -> D.DynArray<&2, U32> & Nat:
195 match g:
196 case Tuple{w, Done{+x}}:
197 (w, B.count_word(x, acc, U32.is_eq(x, 0)))
198 case Tuple{w, Fail{e}}:
199 (w, acc)
200
201def count_go(k: Nat, p: D.DynArray<&2, U32> & Nat, +q: Nat) -> D.DynArray<&2, U32> & Nat:
202 match k:
203 case 0n:
204 p
205 case 1n+r:
206 (w, +acc) = p
207 count_go(r, count_add(D.get(U32, w, q), acc), 1n+q)
208
209def count_fin(+lim: Maybe<&2, Nat>, +n: Nat, p: D.DynArray<&2, U32> & Nat) -> Bitlist & Nat:
210 (w, c) = p
211 (BL{lim, n, w}, c)
212
213def count_len(+lim: Maybe<&2, Nat>, +n: Nat, r: D.DynArray<&2, U32> & Nat) -> Bitlist & Nat:
214 (w, +k) = r
215 count_fin(lim, n, count_go(k, (w, 0n), 0n))
216
217def count(s: Bitlist) -> Bitlist & Nat:
218 BL{+lim, +n, w} = s
219 count_len(lim, n, D.length(U32, w))
220
221# ---- to_list ----
222
223# The low m bits of x, bit 0 first, in front of rest.
224def word_bits(m: Nat, +x: U32, rest: List<&2, Bool>) -> List<&2, Bool>:
225 match m:
226 case 0n:
227 rest
228 case 1n+p:
229 Con{B.low(x), word_bits(p, U32.shr(x), rest)}
230
231# Word q holds bits 32q .. 32q+31; of the first n bits it contributes
232# min(32, n - 32q) (none once 32q >= n).
233def bits_add(+m: Nat, acc: List<&2, Bool>, g: D.DynArray<&2, U32> & Result<&2, &2, DE.Error, U32>) -> D.DynArray<&2, U32> & List<&2, Bool>:
234 match g:
235 case Tuple{w, Done{+x}}:
236 (w, word_bits(m, x, acc))
237 case Tuple{w, Fail{e}}:
238 (w, acc)
239
240# The first n bits, emitted from the last stored word down to word 0.
241def bits_go(k: Nat, st: D.DynArray<&2, U32> & List<&2, Bool>, +n: Nat) -> D.DynArray<&2, U32> & List<&2, Bool>:
242 match k:
243 case 0n:
244 st
245 case 1n+ +q:
246 (w, acc) = st
247 bits_go(q, bits_add(Nat.min(32n, Nat.sub(n, Nat.mul(q, 32n))), acc, D.get(U32, w, q)), n)
248
249def to_list_fin(+lim: Maybe<&2, Nat>, +n: Nat, p: D.DynArray<&2, U32> & List<&2, Bool>) -> Bitlist & List<&2, Bool>:
250 (w, xs) = p
251 (BL{lim, n, w}, xs)
252
253def to_list_len(+lim: Maybe<&2, Nat>, +n: Nat, r: D.DynArray<&2, U32> & Nat) -> Bitlist & List<&2, Bool>:
254 (w, +k) = r
255 to_list_fin(lim, n, bits_go(k, (w, Nil{}), n))
256
257def to_list(s: Bitlist) -> Bitlist & List<&2, Bool>:
258 BL{+lim, +n, w} = s
259 to_list_len(lim, n, D.length(U32, w))
260
261# ---- from_bools ----
262
263def from_push(p: Bitlist & Result<&2, &2, E.Error, Unit>) -> Bitlist:
264 (s, r) = p
265 s
266
267def from_go(bs: List<&2, Bool>, s: Bitlist) -> Bitlist:
268 match bs:
269 case Nil{}:
270 s
271 case Con{+b, t}:
272 from_go(t, from_push(push(s, b)))
273
274# The bits of bs, in order, in an unbounded bitlist.
275def from_bools(bs: List<&2, Bool>) -> Bitlist:
276 from_go(bs, new())
277
278# ---- one operation, for traces ----
279
280def obs_nat(r: Bitlist & Nat) -> Bitlist & E.Obs:
281 (s, x) = r
282 (s, E.ONat{x})
283
284def obs_bit(r: Bitlist & Result<&2, &2, E.Error, Bool>) -> Bitlist & E.Obs:
285 (s, x) = r
286 (s, E.OBit{x})
287
288def obs_unit(r: Bitlist & Result<&2, &2, E.Error, Unit>) -> Bitlist & E.Obs:
289 (s, x) = r
290 (s, E.OUnit{x})
291
292def obs_limit(r: Bitlist & Maybe<&2, Nat>) -> Bitlist & E.Obs:
293 (s, x) = r
294 (s, E.OLimit{x})
295
296def obs_bits(r: Bitlist & List<&2, Bool>) -> Bitlist & E.Obs:
297 (s, x) = r
298 (s, E.OBits{x})
299
300def step(s: Bitlist, op: E.Op) -> Bitlist & E.Obs:
301 match op:
302 case E.Length{}:
303 obs_nat(length(s))
304 case E.Limit{}:
305 obs_limit(limit(s))
306 case E.Get{+i}:
307 obs_bit(get(s, i))
308 case E.Assign{+i, +v}:
309 obs_unit(assign(s, i, v))
310 case E.Push{+v}:
311 obs_unit(push(s, v))
312 case E.Pop{}:
313 obs_bit(pop(s))
314 case E.Clear{}:
315 (clear(s), E.OUnit{Done{Unit{}}})
316 case E.Count{}:
317 obs_nat(count(s))
318 case E.ToList{}:
319 obs_bits(to_list(s))
320
321def record(acc: List<&2, E.Obs>, r: Bitlist & E.Obs) -> Bitlist & List<&2, E.Obs>:
322 (s, o) = r
323 (s, Con{o, acc})
324
325def run_acc(ops: List<&2, E.Op>, st: Bitlist & List<&2, E.Obs>) -> Bitlist & List<&2, E.Obs>:
326 match ops:
327 case Nil{}:
328 st
329 case Con{op, rest}:
330 (s, acc) = st
331 run_acc(rest, record(acc, step(s, op)))
332
333def finish(st: Bitlist & List<&2, E.Obs>) -> Bitlist & List<&2, E.Obs>:
334 (s, os) = st
335 (s, List.reverse(&2, E.Obs, os))
336
337def run(ops: List<&2, E.Op>, s: Bitlist) -> Bitlist & List<&2, E.Obs>:
338 finish(run_acc(ops, (s, Nil{})))