1	import Base
2	import ../math/pow2.bend as P2
3	import ./types/bitset.bend as E
4	
5	# Packed fixed-size bitset over native Base.Array.
6	#
7	# A bitset of logical size `len` stores its bits LSB-first in a Base.Array of
8	# 2^depth 32-bit words: bit i lives in word i/32 at bit position i%32. The
9	# array holds at least ceil(len/32) words; every bit at a position >= len
10	# (the unused tail of the last used word, and any whole padding word) is
11	# zero. Both facts are the invariant proven in proofs/bitset.bend;
12	# union/intersection/difference/xor rely on it (e.g. difference is a AND NOT
13	# b, which stays masked because a's tail is zero).
14	#
15	# Representation note: `Base.Array` is a *linear* fixed-capacity array with
16	# O(1) indexed read and write, so every operation takes the bitset and gives
17	# it back, exactly like src/dynamic_array.bend. The earlier list-of-words
18	# representation made get/set O(words), which is not the algorithm the C
19	# reference runs; this one makes them a single indexed word access and matches
20	# the flat uint32_t array of benchmarks/native/bitset.c word for word.
21	#
22	# Capacity: `depth_for` stops at depth 31, i.e. 2^31 words = 2^36 bits, so
23	# every word index is a representable U32 and Base's index masking over the
24	# word array is the identity. The specification laws about `new(n)` therefore
25	# carry the explicit premise that n fits that capacity (proofs/bitset.bend
26	# `capacity`); every other law holds at every state satisfying the invariant,
27	# and the invariant implies the premise. This is the same kind of explicit,
28	# documented capacity bound that src/dynamic_array.bend carries, and the same
29	# one benchmarks/native/bitset.c has. It is a real narrowing compared with the
30	# earlier list-of-words representation, which had no capacity: see
31	# PROOF_STATUS.md and docs/archive/.
32	#
33	# Errors never change the state: get/set/clear with index >= len fail with
34	# IndexOutOfRange; binary operations on operands of different logical size
35	# fail with LengthMismatch and give both operands back unchanged. Because the
36	# array is linear, a binary operation returns BOTH operands (a linear API has
37	# to give back what it borrowed) and a bitset that is no longer needed is
38	# released with `dispose`; `clone` makes two independent copies.
39	#
40	# Cost (w = 2^depth words): new O(w); length O(1); get/set/clear one indexed
41	# word read (and, for set/clear, one indexed word write) plus a constant
42	# amount of word arithmetic; count/to_list O(32 * w) (32 shifts per word, the
43	# same loop the C reference runs); binary operations O(w); clone O(w);
44	# dispose O(w).
45	#
46	# "One indexed word access" is a claim about Bend's native C backend, not
47	# folklore: `Base.Array` is a flat array there, and the measured cost of
48	# `Array.get`/`Array.set` is constant across sizes 64 .. 262144 and at parity
49	# with the same access in C (see the cost model at the top of BENCHMARKS.md
50	# and the `bitset.get` / `bitset.set` rows). None of the proofs depend on it.
51	
52	type Wd is Data:
53	  W{value: U32}
54	
55	type Bitset is Type:
56	  BS{len: Nat, depth: Nat, words: Array<Wd>}
57	
58	def wval(x: Wd) -> U32:
59	  match x:
60	    case W{v}:
61	      v
62	
63	# Word-level operations (native U32 arithmetic).
64	
65	type WordOp is Data:
66	  KOr{}
67	  KAnd{}
68	  KDiff{}
69	  KXor{}
70	
71	def low(w: U32) -> Bool:
72	  Bool.not(U32.is_even(w))
73	
74	def word_get(w: U32, k: Nat) -> Bool:
75	  low(U32.shrn(w, k))
76	
77	def word_put(v: Bool, w: U32, k: Nat) -> U32:
78	  match v:
79	    case True{}:
80	      U32.or(w, U32.shln(1, k))
81	    case False{}:
82	      U32.and(w, U32.not(U32.shln(1, k)))
83	
84	def word_op(k: WordOp, a: U32, b: U32) -> U32:
85	  match k:
86	    case KOr{}:
87	      U32.or(a, b)
88	    case KAnd{}:
89	      U32.and(a, b)
90	    case KDiff{}:
91	      U32.and(a, U32.not(b))
92	    case KXor{}:
93	      U32.xor(a, b)
94	
95	def bit_value(b: Bool) -> Nat:
96	  match b:
97	    case True{}:
98	      1n
99	    case False{}:
100	      0n
101	
102	# Number of set bits among the low m bits of w.
103	def word_count(m: Nat, +w: U32) -> Nat:
104	  match m:
105	    case 0n:
106	      0n
107	    case 1n+p:
108	      Nat.add(bit_value(low(w)), word_count(p, U32.shr(w)))
109	
110	def member_pick(b: Bool, +off: Nat, rest: List<&2, Nat>) -> List<&2, Nat>:
111	  match b:
112	    case True{}:
113	      Con{off, rest}
114	    case False{}:
115	      rest
116	
117	# Indices (from off) of set bits among the low m bits of w, then rest.
118	def word_members(m: Nat, +w: U32, +off: Nat, rest: List<&2, Nat>) -> List<&2, Nat>:
119	  match m:
120	    case 0n:
121	      rest
122	    case 1n+p:
123	      member_pick(low(w), off, word_members(p, U32.shr(w), 1n+off, rest))
124	
125	# ---- index arithmetic ----
126	
127	# The word index of bit i and the bit position inside that word. Base's
128	# Nat.div / Nat.mod are structural definitions the proofs can peel 32 steps
129	# at a time (proofs/bitset/index.bend) and the native backend evaluates in
130	# constant time.
131	def wordix(i: Nat) -> Nat:
132	  Nat.div(i, 32n)
133	
134	def bitix(i: Nat) -> Nat:
135	  Nat.mod(i, 32n)
136	
137	# 2^d.
138	def pow2(d: Nat) -> Nat:
139	  match d:
140	    case 0n:
141	      1n
142	    case 1n+p:
143	      Nat.double(pow2(p))
144	
145	# 2^31 words = 2^36 bits: the capacity of the packed representation (the
146	# constant is never materialised as a value; `depth_for` simply stops at this
147	# depth). Every word index is then a representable U32 and Base's index
148	# masking over the word array is the identity.
149	def max_depth() -> Nat:
150	  31n
151	
152	# The smallest depth whose 2^depth words hold n bits, capped at max_depth.
153	# `fuel` bounds the search structurally, `cap` is 2^d and `done` is the exit
154	# test `n <= 32 * cap`, so a depth that comes out of the loop below the cap
155	# always satisfies it (proofs/bitset/depth.bend).
156	def depth_go(fuel: Nat, +n: Nat, d: Nat, +cap: Nat, done: Bool) -> Nat:
157	  match fuel done:
158	    case 0n _:
159	      d
160	    case 1n+f True{}:
161	      d
162	    case 1n+f False{}:
163	      depth_go(f, n, 1n+d, Nat.double(cap), Nat.is_le(n, Nat.mul(Nat.double(cap), 32n)))
164	
165	def depth_for(+n: Nat) -> Nat:
166	  depth_go(max_depth(), n, 0n, 1n, Nat.is_le(n, Nat.mul(1n, 32n)))
167	
168	# ---- array access ----
169	
170	def read_fin(p: Array<Wd> & Wd) -> Array<Wd> & U32:
171	  (a, x) = p
172	  (a, wval(x))
173	
174	# Word q of the array (q < 2^depth).
175	def read(a: Array<Wd>, +d: Nat, +q: Nat) -> Array<Wd> & U32:
176	  read_fin(Array.get(Wd, a, U32.from_nat(q)))
177	
178	# Replace word q.
179	def write(a: Array<Wd>, +d: Nat, +q: Nat, +v: U32) -> Array<Wd>:
180	  Array.set(Wd, a, U32.from_nat(q), W{v})
181	
182	# ---- public API ----
183	
184	# All-zero bitset of logical size n (see the capacity note).
185	def new_at(+n: Nat, +d: Nat) -> Bitset:
186	  BS{n, d, Array.new(Wd, d, W{0})}
187	
188	def new(+n: Nat) -> Bitset:
189	  new_at(n, depth_for(n))
190	
191	def length(s: Bitset) -> Bitset & Nat:
192	  match s:
193	    case BS{+n, d, a}:
194	      (BS{n, d, a}, n)
195	
196	# ---- get ----
197	
198	def get_read(p: Array<Wd> & U32, +n: Nat, +d: Nat, +b: Nat) -> Bitset & Result<&2, &2, E.Error, Bool>:
199	  (a, w) = p
200	  (BS{n, d, a}, Done{word_get(w, b)})
201	
202	def get_if(ok: Bool, +n: Nat, +d: Nat, a: Array<Wd>, +i: Nat) -> Bitset & Result<&2, &2, E.Error, Bool>:
203	  match ok:
204	    case True{}:
205	      get_read(read(a, d, wordix(i)), n, d, bitix(i))
206	    case False{}:
207	      (BS{n, d, a}, Fail{E.IndexOutOfRange{}})
208	
209	def get(s: Bitset, +i: Nat) -> Bitset & Result<&2, &2, E.Error, Bool>:
210	  match s:
211	    case BS{+n, +d, a}:
212	      get_if(Nat.is_lt(i, n), n, d, a, i)
213	
214	# ---- set / clear ----
215	
216	def assign_read(p: Array<Wd> & U32, +n: Nat, +d: Nat, +q: Nat, +b: Nat, +v: Bool) -> Bitset & Result<&2, &2, E.Error, Unit>:
217	  (a, w) = p
218	  (BS{n, d, write(a, d, q, word_put(v, w, b))}, Done{Unit{}})
219	
220	def assign_if(ok: Bool, +n: Nat, +d: Nat, a: Array<Wd>, +i: Nat, +v: Bool) -> Bitset & Result<&2, &2, E.Error, Unit>:
221	  match ok:
222	    case True{}:
223	      assign_read(read(a, d, wordix(i)), n, d, wordix(i), bitix(i), v)
224	    case False{}:
225	      (BS{n, d, a}, Fail{E.IndexOutOfRange{}})
226	
227	def assign(s: Bitset, +i: Nat, +v: Bool) -> Bitset & Result<&2, &2, E.Error, Unit>:
228	  match s:
229	    case BS{+n, +d, a}:
230	      assign_if(Nat.is_lt(i, n), n, d, a, i, v)
231	
232	# Set bit i to 1.
233	def set(s: Bitset, +i: Nat) -> Bitset & Result<&2, &2, E.Error, Unit>:
234	  assign(s, i, True{})
235	
236	# Set bit i to 0.
237	def clear(s: Bitset, +i: Nat) -> Bitset & Result<&2, &2, E.Error, Unit>:
238	  assign(s, i, False{})
239	
240	# ---- whole-array walks ----
241	
242	# Sum of the populations of words q, q+1, ... (m of them).
243	# Eight bits per iteration: word_count_t unrolled (the same shifts and adds).
244	def bv8(+w: U32) -> Nat:
245	  Nat.add(bit_value(low(w)), Nat.add(bit_value(low(U32.shr(w))), Nat.add(bit_value(low(U32.shr(U32.shr(w)))), Nat.add(bit_value(low(U32.shr(U32.shr(U32.shr(w))))), Nat.add(bit_value(low(U32.shr(U32.shr(U32.shr(U32.shr(w)))))), Nat.add(bit_value(low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))), Nat.add(bit_value(low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w)))))))), bit_value(low(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w))))))))))))))))
246	
247	def word_count_8(k: Nat, +w: U32, +acc: Nat) -> Nat:
248	  match k:
249	    case 0n:
250	      acc
251	    case 1n+p:
252	      word_count_8(p, U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(U32.shr(w)))))))), Nat.add(acc, bv8(w)))
253	
254	# A zero word contributes nothing and is skipped.
255	def count_word(+w: U32, +acc: Nat, zero: Bool) -> Nat:
256	  match zero:
257	    case True{}:
258	      acc
259	    case False{}:
260	      word_count_8(4n, w, acc)
261	
262	def count_add(p: Array<Wd> & U32, +acc: Nat) -> Array<Wd> & Nat:
263	  (a, +w) = p
264	  (a, count_word(w, acc, U32.is_eq(w, 0)))
265	
266	def count_go(m: Nat, p: Array<Wd> & Nat, +d: Nat, +q: Nat) -> Array<Wd> & Nat:
267	  match m:
268	    case 0n:
269	      p
270	    case 1n+r:
271	      (a, acc) = p
272	      count_go(r, count_add(read(a, d, q), acc), d, 1n+q)
273	
274	def count_fin(p: Array<Wd> & Nat, +n: Nat, +d: Nat) -> Bitset & Nat:
275	  (a, c) = p
276	  (BS{n, d, a}, c)
277	
278	def count(s: Bitset) -> Bitset & Nat:
279	  match s:
280	    case BS{+n, +d, a}:
281	      count_fin(count_go(P2.pow2t(d), (a, 0n), d, 0n), n, d)
282	
283	# Indices of set bits, ascending. Walks the words from the last to the first
284	# so the list is built in ascending order without an append.
285	# The members of one word, by two TAIL loops: the set offsets are pushed in
286	# DESCENDING order onto a scratch list (low bit first), which is then
287	# reversed onto rest -- the same list word_members builds, without its
288	# non-tail recursion.
289	def word_desc(m: Nat, +w: U32, +off: Nat, acc: List<&2, Nat>) -> List<&2, Nat>:
290	  match m:
291	    case 0n:
292	      acc
293	    case 1n+p:
294	      word_desc(p, U32.shr(w), 1n+off, member_pick(low(w), off, acc))
295	
296	# A zero word has no members and is skipped.
297	def members_word(+w: U32, +off: Nat, rest: List<&2, Nat>, zero: Bool) -> List<&2, Nat>:
298	  match zero:
299	    case True{}:
300	      rest
301	    case False{}:
302	      List.reverse.go(&2, Nat, word_desc(32n, w, off, Nil{}), rest)
303	
304	def members_cons(p: Array<Wd> & U32, +off: Nat, rest: List<&2, Nat>) -> Array<Wd> & List<&2, Nat>:
305	  (a, +w) = p
306	  (a, members_word(w, off, rest, U32.is_eq(w, 0)))
307	
308	def members_go(m: Nat, p: Array<Wd> & List<&2, Nat>, +d: Nat) -> Array<Wd> & List<&2, Nat>:
309	  match m:
310	    case 0n:
311	      p
312	    case 1n+ +r:
313	      (a, acc) = p
314	      members_go(r, members_cons(read(a, d, r), Nat.mul(r, 32n), acc), d)
315	
316	def members_fin(p: Array<Wd> & List<&2, Nat>, +n: Nat, +d: Nat) -> Bitset & List<&2, Nat>:
317	  (a, xs) = p
318	  (BS{n, d, a}, xs)
319	
320	def to_list(s: Bitset) -> Bitset & List<&2, Nat>:
321	  match s:
322	    case BS{+n, +d, a}:
323	      members_fin(members_go(P2.pow2t(d), (a, Nil{}), d), n, d)
324	
325	# ---- binary operations ----
326	
327	def zip_write(pa: Array<Wd> & U32, pb: Array<Wd> & U32, +k: WordOp, +d: Nat, +q: Nat) -> Array<Wd> & Array<Wd>:
328	  (a, x) = pa
329	  (b, y) = pb
330	  (write(a, d, q, word_op(k, x, y)), b)
331	
332	def zip_step(p: Array<Wd> & Array<Wd>, +k: WordOp, +d: Nat, +q: Nat) -> Array<Wd> & Array<Wd>:
333	  (a, b) = p
334	  zip_write(read(a, d, q), read(b, d, q), k, d, q)
335	
336	def zip_go(m: Nat, p: Array<Wd> & Array<Wd>, +k: WordOp, +d: Nat, +q: Nat) -> Array<Wd> & Array<Wd>:
337	  match m:
338	    case 0n:
339	      p
340	    case 1n+r:
341	      zip_go(r, zip_step(p, k, d, q), k, d, 1n+q)
342	
343	# Discard a linear array (`dispose` below is the public form).
344	def burn_list(xs: List<Wd>) -> Unit:
345	  match xs:
346	    case Nil{}:
347	      Unit{}
348	    case Con{x, t}:
349	      burn_list(t)
350	
351	# Releasing the word array is dropping it: `Base.Array` is linear, so the
352	# runtime frees the block when the last reference is erased.
353	def burn(a: Array<Wd>) -> Unit:
354	  Unit{}
355	
356	# Release a bitset. `Base.Array` is linear, so a caller that stops using a
357	# bitset has to say so; every operation above gives the bitset back instead.
358	def dispose(s: Bitset) -> Unit:
359	  match s:
360	    case BS{n, d, a}:
361	      burn(a)
362	
363	# Two independent bitsets with the same contents (the linear form of sharing).
364	def clone_fin(p: Array<Wd> & Array<Wd>, +n: Nat, +d: Nat) -> Bitset & Bitset:
365	  (a, b) = p
366	  (BS{n, d, a}, BS{n, d, b})
367	
368	def clone(s: Bitset) -> Bitset & Bitset:
369	  match s:
370	    case BS{+n, +d, a}:
371	      clone_fin(Array.clone(Wd, a), n, d)
372	
373	# Release two bitsets.
374	def dispose2_go(u: Unit, v: Unit) -> Unit:
375	  match u v:
376	    case Unit{} Unit{}:
377	      Unit{}
378	
379	def dispose2(s: Bitset, t: Bitset) -> Unit:
380	  dispose2_go(dispose(s), dispose(t))
381	
382	def zip_fin(p: Array<Wd> & Array<Wd>, +n: Nat, +d: Nat, +m: Nat, +e: Nat) -> Bitset & Bitset & Result<&2, &2, E.Error, Unit>:
383	  (a, b) = p
384	  (BS{n, d, a}, BS{m, e, b}, Done{Unit{}})
385	
386	def combine_if(ok: Bool, +k: WordOp, +n: Nat, +d: Nat, a: Array<Wd>, +m: Nat, +e: Nat, b: Array<Wd>) -> Bitset & Bitset & Result<&2, &2, E.Error, Unit>:
387	  match ok:
388	    case True{}:
389	      zip_fin(zip_go(P2.pow2t(d), (a, b), k, d, 0n), n, d, m, e)
390	    case False{}:
391	      (BS{n, d, a}, BS{m, e, b}, Fail{E.LengthMismatch{}})
392	
393	def combine_b(+k: WordOp, +n: Nat, +d: Nat, a: Array<Wd>, t: Bitset) -> Bitset & Bitset & Result<&2, &2, E.Error, Unit>:
394	  match t:
395	    case BS{+m, +e, b}:
396	      combine_if(Bool.and(Nat.is_eq(n, m), Nat.is_eq(d, e)), k, n, d, a, m, e, b)
397	
398	# The operands are given back unchanged apart from the result written into the
399	# left one: a linear API has to return what it borrowed.
400	def combine(+k: WordOp, s: Bitset, t: Bitset) -> Bitset & Bitset & Result<&2, &2, E.Error, Unit>:
401	  match s:
402	    case BS{+n, +d, a}:
403	      combine_b(k, n, d, a, t)
404	
405	def union(s: Bitset, t: Bitset) -> Bitset & Bitset & Result<&2, &2, E.Error, Unit>:
406	  combine(KOr{}, s, t)
407	
408	def intersection(s: Bitset, t: Bitset) -> Bitset & Bitset & Result<&2, &2, E.Error, Unit>:
409	  combine(KAnd{}, s, t)
410	
411	def difference(s: Bitset, t: Bitset) -> Bitset & Bitset & Result<&2, &2, E.Error, Unit>:
412	  combine(KDiff{}, s, t)
413	
414	def xor(s: Bitset, t: Bitset) -> Bitset & Bitset & Result<&2, &2, E.Error, Unit>:
415	  combine(KXor{}, s, t)
416	
417	# ---- building from a bit sequence ----
418	
419	def fill_drop(s: Bitset, x: Result<&2, &2, E.Error, Unit>) -> Bitset:
420	  match x:
421	    case Fail{e}:
422	      s
423	    case Done{u}:
424	      s
425	
426	def fill_set(p: Bitset & Result<&2, &2, E.Error, Unit>) -> Bitset:
427	  (s, x) = p
428	  fill_drop(s, x)
429	
430	def fill_pick(b: Bool, s: Bitset, +i: Nat) -> Bitset:
431	  match b:
432	    case True{}:
433	      fill_set(set(s, i))
434	    case False{}:
435	      s
436	
437	def fill(bs: List<&2, Bool>, +i: Nat, s: Bitset) -> Bitset:
438	  match bs:
439	    case Nil{}:
440	      s
441	    case Con{b, t}:
442	      fill(t, 1n+i, fill_pick(b, s, i))
443	
444	def bool_count(bs: List<&2, Bool>) -> Nat:
445	  match bs:
446	    case Nil{}:
447	      0n
448	    case Con{b, t}:
449	      1n+bool_count(t)
450	
451	# Bitset whose logical bits are exactly bs (bit 0 first).
452	def from_bools(+bs: List<&2, Bool>) -> Bitset:
453	  fill(bs, 0n, new(bool_count(bs)))
454	
455	# ---- combining with a bit sequence ----
456	#
457	# The trace runner's binary operations take the operand as a bit sequence.
458	# The logical sizes are compared *before* the operand bitset is built, so an
459	# operand of a different size costs nothing and can never be materialised at
460	# a size the representation cannot hold.
461	
462	def drop_right_go(s: Bitset, u: Unit, x: Result<&2, &2, E.Error, Unit>) -> Bitset & Result<&2, &2, E.Error, Unit>:
463	  match u:
464	    case Unit{}:
465	      (s, x)
466	
467	def drop_right(p: Bitset & Bitset & Result<&2, &2, E.Error, Unit>) -> Bitset & Result<&2, &2, E.Error, Unit>:
468	  (s, t, x) = p
469	  drop_right_go(s, dispose(t), x)
470	
471	def comb_go(ok: Bool, +k: WordOp, +n: Nat, +d: Nat, a: Array<Wd>, +ys: List<&2, Bool>) -> Bitset & Result<&2, &2, E.Error, Unit>:
472	  match ok:
473	    case True{}:
474	      drop_right(combine(k, BS{n, d, a}, from_bools(ys)))
475	    case False{}:
476	      (BS{n, d, a}, Fail{E.LengthMismatch{}})
477	
478	def comb_bits(+k: WordOp, s: Bitset, +ys: List<&2, Bool>) -> Bitset & Result<&2, &2, E.Error, Unit>:
479	  match s:
480	    case BS{+n, +d, a}:
481	      comb_go(Nat.is_eq(n, bool_count(ys)), k, n, d, a, ys)
482	
483	# ---- trace runner ----
484	
485	def obs_unit(r: Bitset & Result<&2, &2, E.Error, Unit>) -> Bitset & E.Obs:
486	  (s, x) = r
487	  (s, E.OUnit{x})
488	
489	def obs_pair_done(s: Bitset, u: Unit, x: Result<&2, &2, E.Error, Unit>) -> Bitset & E.Obs:
490	  match u:
491	    case Unit{}:
492	      (s, E.OUnit{x})
493	
494	# The trace runner owns the operand it built from the operation, so it
495	# releases it once the combination has been applied.
496	def obs_pair(r: Bitset & Bitset & Result<&2, &2, E.Error, Unit>) -> Bitset & E.Obs:
497	  (s, t, x) = r
498	  obs_pair_done(s, dispose(t), x)
499	
500	def obs_bit(r: Bitset & Result<&2, &2, E.Error, Bool>) -> Bitset & E.Obs:
501	  (s, x) = r
502	  (s, E.OBit{x})
503	
504	def obs_nat(r: Bitset & Nat) -> Bitset & E.Obs:
505	  (s, x) = r
506	  (s, E.ONat{x})
507	
508	def obs_list(r: Bitset & List<&2, Nat>) -> Bitset & E.Obs:
509	  (s, xs) = r
510	  (s, E.OList{xs})
511	
512	def step(s: Bitset, op: E.Op) -> Bitset & E.Obs:
513	  match op:
514	    case E.Length{}:
515	      obs_nat(length(s))
516	    case E.Get{i}:
517	      obs_bit(get(s, i))
518	    case E.Set{i}:
519	      obs_unit(set(s, i))
520	    case E.Clear{i}:
521	      obs_unit(clear(s, i))
522	    case E.Count{}:
523	      obs_nat(count(s))
524	    case E.Union{ys}:
525	      obs_unit(comb_bits(KOr{}, s, ys))
526	    case E.Intersection{ys}:
527	      obs_unit(comb_bits(KAnd{}, s, ys))
528	    case E.Difference{ys}:
529	      obs_unit(comb_bits(KDiff{}, s, ys))
530	    case E.Xor{ys}:
531	      obs_unit(comb_bits(KXor{}, s, ys))
532	
533	    case E.ToList{}:
534	      obs_list(to_list(s))
535	
536	def record(acc: List<&2, E.Obs>, r: Bitset & E.Obs) -> Bitset & List<&2, E.Obs>:
537	  (s, o) = r
538	  (s, Con{o, acc})
539	
540	def step_acc(op: E.Op, st: Bitset & List<&2, E.Obs>) -> Bitset & List<&2, E.Obs>:
541	  (s, acc) = st
542	  record(acc, step(s, op))
543	
544	def run_acc(ops: List<&2, E.Op>, st: Bitset & List<&2, E.Obs>) -> Bitset & List<&2, E.Obs>:
545	  match ops:
546	    case Nil{}:
547	      st
548	    case Con{op, rest}:
549	      run_acc(rest, step_acc(op, st))
550	
551	def finish(st: Bitset & List<&2, E.Obs>) -> Bitset & List<&2, E.Obs>:
552	  (s, acc) = st
553	  (s, List.reverse(&2, E.Obs, acc))
554	
555	def run(ops: List<&2, E.Op>, s: Bitset) -> Bitset & List<&2, E.Obs>:
556	  finish(run_acc(ops, (s, Nil{})))