proofs/containers/bitset/model.bend
bend-collections-laws-containers@1.0.0.0 · 77 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/src/containers/bitset.bend as B
3
4# The word-list model of the packed representation.
5#
6# src/bitset.bend stores the words in a native Base.Array and addresses them
7# by index; the mathematics of "what the words mean" is easier to state over
8# the list of stored words, so these are the list-level counterparts of the
9# runtime walks. proofs/bitset/arr.bend proves that each runtime operation
10# does exactly what the corresponding function here says, on the list of the
11# array's slots, and proofs/bitset/state.bend then relates that list to the
12# independent bit-sequence specification.
13#
14# These definitions are the ones src/bitset.bend used before it moved to
15# Base.Array, so every lemma of proofs/bitset/state.bend about them is the
16# retained one.
17
18# Zero words covering n more bits; `free` counts unused bits left in the
19# last emitted word, so exactly ceil(n/32) words are produced from free = 0.
20def zeros(n: Nat, free: Nat) -> List<&2, U32>:
21 match n free:
22 case 0n _:
23 Nil{}
24 case 1n+p 0n:
25 Con{0, zeros(p, 31n)}
26 case 1n+p 1n+f:
27 zeros(p, f)
28
29def get_pick(b: Bool, w: U32, +i: Nat, r: Bool) -> Bool:
30 match b:
31 case True{}:
32 B.word_get(w, i)
33 case False{}:
34 r
35
36def get_walk(ws: List<&2, U32>, +i: Nat) -> Bool:
37 match ws:
38 case Nil{}:
39 False{}
40 case Con{w, t}:
41 get_pick(Nat.is_lt(i, 32n), w, i, get_walk(t, Nat.sub(i, 32n)))
42
43def put_pick(b: Bool, +v: Bool, +w: U32, +i: Nat, t: List<&2, U32>, r: List<&2, U32>) -> List<&2, U32>:
44 match b:
45 case True{}:
46 Con{B.word_put(v, w, i), t}
47 case False{}:
48 Con{w, r}
49
50def put_walk(+ws: List<&2, U32>, +i: Nat, +v: Bool) -> List<&2, U32>:
51 match ws:
52 case Nil{}:
53 Nil{}
54 case Con{+w, +t}:
55 put_pick(Nat.is_lt(i, 32n), v, w, i, t, put_walk(t, Nat.sub(i, 32n), v))
56
57def zip_words(+k: B.WordOp, ws: List<&2, U32>, vs: List<&2, U32>) -> List<&2, U32>:
58 match ws vs:
59 case Con{a, s} Con{b, t}:
60 Con{B.word_op(k, a, b), zip_words(k, s, t)}
61 case _ _:
62 Nil{}
63
64def count_words(ws: List<&2, U32>) -> Nat:
65 match ws:
66 case Nil{}:
67 0n
68 case Con{w, t}:
69 Nat.add(B.word_count(32n, w), count_words(t))
70
71def members_words(ws: List<&2, U32>, +off: Nat) -> List<&2, Nat>:
72 match ws:
73 case Nil{}:
74 Nil{}
75 case Con{w, t}:
76 B.word_members(32n, w, off, members_words(t, Nat.add(32n, off)))
77