src/containers/bitlist.bend

bend-collections@1.0.0.0 · 338 lines · 51 definitions

1import Base
2import bend-collections@1.0.0.0/src/containers/bitset.bend as B
3import bend-collections@1.0.0.0/src/containers/dynamic_array.bend as D
4import bend-collections@1.0.0.0/src/containers/types/dynamic_array.bend as DE
5import bend-collections@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{})))