1	import Base
2	import ./bitset.bend as B
3	import ./dynamic_array.bend as D
4	import ./types/dynamic_array.bend as DE
5	import ./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	
33	type Bitlist is Type:
34	  BL{limit: Maybe<&2, Nat>, len: Nat, words: D.DynArray<&2, U32>}
35	
36	def new() -> Bitlist:
37	  BL{None{}, 0n, D.new(U32)}
38	
39	def with_limit(+n: Nat) -> Bitlist:
40	  BL{Some{n}, 0n, D.new(U32)}
41	
42	# Room for one more bit under the limit.
43	def 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	
50	def length(s: Bitlist) -> Bitlist & Nat:
51	  BL{lim, +n, w} = s
52	  (BL{lim, n, w}, n)
53	
54	def limit(s: Bitlist) -> Bitlist & Maybe<&2, Nat>:
55	  BL{+lim, n, w} = s
56	  (BL{lim, n, w}, lim)
57	
58	# ---- get ----
59	
60	def 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	
67	def 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	
74	def 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	
80	def 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.
88	def 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	
95	def 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	
102	def 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	
106	def set(s: Bitlist, +i: Nat) -> Bitlist & Result<&2, &2, E.Error, Unit>:
107	  assign(s, i, True{})
108	
109	def unset(s: Bitlist, +i: Nat) -> Bitlist & Result<&2, &2, E.Error, Unit>:
110	  assign(s, i, False{})
111	
112	# ---- push ----
113	
114	def 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).
122	def 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	
129	def 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	
136	def 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	
140	def 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	
147	def 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	
153	def 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.
161	def 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	
168	def 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	
175	def 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	
182	def 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	
188	def clear(s: Bitlist) -> Bitlist:
189	  BL{lim, n, w} = s
190	  BL{lim, 0n, D.clear(U32, w)}
191	
192	# ---- count ----
193	
194	def 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	
201	def 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	
209	def 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	
213	def 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	
217	def 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.
224	def 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).
233	def 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.
241	def 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	
249	def 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	
253	def 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	
257	def 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	
263	def from_push(p: Bitlist & Result<&2, &2, E.Error, Unit>) -> Bitlist:
264	  (s, r) = p
265	  s
266	
267	def 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.
275	def from_bools(bs: List<&2, Bool>) -> Bitlist:
276	  from_go(bs, new())
277	
278	# ---- one operation, for traces ----
279	
280	def obs_nat(r: Bitlist & Nat) -> Bitlist & E.Obs:
281	  (s, x) = r
282	  (s, E.ONat{x})
283	
284	def obs_bit(r: Bitlist & Result<&2, &2, E.Error, Bool>) -> Bitlist & E.Obs:
285	  (s, x) = r
286	  (s, E.OBit{x})
287	
288	def obs_unit(r: Bitlist & Result<&2, &2, E.Error, Unit>) -> Bitlist & E.Obs:
289	  (s, x) = r
290	  (s, E.OUnit{x})
291	
292	def obs_limit(r: Bitlist & Maybe<&2, Nat>) -> Bitlist & E.Obs:
293	  (s, x) = r
294	  (s, E.OLimit{x})
295	
296	def obs_bits(r: Bitlist & List<&2, Bool>) -> Bitlist & E.Obs:
297	  (s, x) = r
298	  (s, E.OBits{x})
299	
300	def 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	
321	def 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	
325	def 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	
333	def 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	
337	def run(ops: List<&2, E.Op>, s: Bitlist) -> Bitlist & List<&2, E.Obs>:
338	  finish(run_acc(ops, (s, Nil{})))