src/containers/bitset.bend

bend-collections@1.0.0.0 · 556 lines · 85 definitions

1import Base
2import bend-collections@1.0.0.0/src/math/pow2.bend as P2
3import bend-collections@1.0.0.0/src/containers/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
52type Wd is Data:
53  W{value: U32}
54
55type Bitset is Type:
56  BS{len: Nat, depth: Nat, words: Array<Wd>}
57
58def wval(x: Wd) -> U32:
59  match x:
60    case W{v}:
61      v
62
63# Word-level operations (native U32 arithmetic).
64
65type WordOp is Data:
66  KOr{}
67  KAnd{}
68  KDiff{}
69  KXor{}
70
71def low(w: U32) -> Bool:
72  Bool.not(U32.is_even(w))
73
74def word_get(w: U32, k: Nat) -> Bool:
75  low(U32.shrn(w, k))
76
77def 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
84def 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
95def 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.
103def 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
110def 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.
118def 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.
131def wordix(i: Nat) -> Nat:
132  Nat.div(i, 32n)
133
134def bitix(i: Nat) -> Nat:
135  Nat.mod(i, 32n)
136
137# 2^d.
138def 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.
149def 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).
156def 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
165def 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
170def 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).
175def 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.
179def 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).
185def new_at(+n: Nat, +d: Nat) -> Bitset:
186  BS{n, d, Array.new(Wd, d, W{0})}
187
188def new(+n: Nat) -> Bitset:
189  new_at(n, depth_for(n))
190
191def length(s: Bitset) -> Bitset & Nat:
192  match s:
193    case BS{+n, d, a}:
194      (BS{n, d, a}, n)
195
196# ---- get ----
197
198def 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
202def 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
209def 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
216def 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
220def 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
227def 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.
233def set(s: Bitset, +i: Nat) -> Bitset & Result<&2, &2, E.Error, Unit>:
234  assign(s, i, True{})
235
236# Set bit i to 0.
237def 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).
244def 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
247def 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.
255def 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
262def 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
266def 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
274def count_fin(p: Array<Wd> & Nat, +n: Nat, +d: Nat) -> Bitset & Nat:
275  (a, c) = p
276  (BS{n, d, a}, c)
277
278def 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.
289def 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.
297def 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
304def 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
308def 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
316def 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
320def 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
327def 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
332def 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
336def 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).
344def 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.
353def 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.
358def 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).
364def 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
368def 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.
374def dispose2_go(u: Unit, v: Unit) -> Unit:
375  match u v:
376    case Unit{} Unit{}:
377      Unit{}
378
379def dispose2(s: Bitset, t: Bitset) -> Unit:
380  dispose2_go(dispose(s), dispose(t))
381
382def 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
386def 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
393def 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.
400def 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
405def union(s: Bitset, t: Bitset) -> Bitset & Bitset & Result<&2, &2, E.Error, Unit>:
406  combine(KOr{}, s, t)
407
408def intersection(s: Bitset, t: Bitset) -> Bitset & Bitset & Result<&2, &2, E.Error, Unit>:
409  combine(KAnd{}, s, t)
410
411def difference(s: Bitset, t: Bitset) -> Bitset & Bitset & Result<&2, &2, E.Error, Unit>:
412  combine(KDiff{}, s, t)
413
414def 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
419def 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
426def fill_set(p: Bitset & Result<&2, &2, E.Error, Unit>) -> Bitset:
427  (s, x) = p
428  fill_drop(s, x)
429
430def 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
437def 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
444def 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).
452def 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
462def 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
467def 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
471def 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
478def 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
485def obs_unit(r: Bitset & Result<&2, &2, E.Error, Unit>) -> Bitset & E.Obs:
486  (s, x) = r
487  (s, E.OUnit{x})
488
489def 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.
496def 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
500def obs_bit(r: Bitset & Result<&2, &2, E.Error, Bool>) -> Bitset & E.Obs:
501  (s, x) = r
502  (s, E.OBit{x})
503
504def obs_nat(r: Bitset & Nat) -> Bitset & E.Obs:
505  (s, x) = r
506  (s, E.ONat{x})
507
508def obs_list(r: Bitset & List<&2, Nat>) -> Bitset & E.Obs:
509  (s, xs) = r
510  (s, E.OList{xs})
511
512def 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
536def 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
540def 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
544def 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
551def 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
555def run(ops: List<&2, E.Op>, s: Bitset) -> Bitset & List<&2, E.Obs>:
556  finish(run_acc(ops, (s, Nil{})))