src/containers/bitset.bend
bend-collections-laws-containers@1.0.0.0 · 556 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/src/math/pow2.bend as P2
3import bend-collections-laws-containers@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{})))