proofs/containers/bitset/word.bend
bend-collections-laws-containers@1.0.0.0 · 246 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
5import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
6import bend-collections-laws-containers@1.0.0.0/spec/containers/bitset.bend as S
7import bend-collections-laws-containers@1.0.0.0/src/containers/bitset.bend as B
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/lists.bend as BL
9
10# Bit-level meaning of the native U32 operations used by src/bitset.bend,
11# derived from Base's Word definitions (U32 = U32{Word(32n)}, bit 0 first).
12
13def wbits(n: Nat, w: Word(n)) -> List<&2, Bool>:
14 match n:
15 case 0n:
16 Nil{}
17 case 1n+p:
18 match w:
19 case WCon{b, t}:
20 Con{b, wbits(p, t)}
21
22def ubits(x: U32) -> List<&2, Bool>:
23 match x:
24 case U32{w}:
25 wbits(32n, w)
26
27def len_wbits(+n: Nat, +w: Word(n)) -> {SC.length(Bool, wbits(n, w)) == n : Nat}:
28 match n:
29 case 0n:
30 {==}
31 case 1n+p:
32 match w:
33 case WCon{b, t}:
34 N.succ_cong(SC.length(Bool, wbits(p, t)), p, len_wbits(p, t))
35
36def ulen(+x: U32) -> {SC.length(Bool, ubits(x)) == 32n : Nat}:
37 match x:
38 case U32{w}:
39 len_wbits(32n, w)
40
41# ---- bitwise operations are element-wise ----
42
43def w_or(+n: Nat, +a: Word(n), +b: Word(n)) -> {wbits(n, Word.or(n, a, b)) == BL.zipk(B.KOr{}, wbits(n, a), wbits(n, b)) : List<&2, Bool>}:
44 match n:
45 case 0n:
46 {==}
47 case 1n+p:
48 match a b:
49 case WCon{x, s} WCon{y, t}:
50 LL.cons_cong(Bool, Bool.or(x, y), wbits(p, Word.or(p, s, t)), BL.zipk(B.KOr{}, wbits(p, s), wbits(p, t)), w_or(p, s, t))
51
52def w_and(+n: Nat, +a: Word(n), +b: Word(n)) -> {wbits(n, Word.and(n, a, b)) == BL.zipk(B.KAnd{}, wbits(n, a), wbits(n, b)) : List<&2, Bool>}:
53 match n:
54 case 0n:
55 {==}
56 case 1n+p:
57 match a b:
58 case WCon{x, s} WCon{y, t}:
59 LL.cons_cong(Bool, Bool.and(x, y), wbits(p, Word.and(p, s, t)), BL.zipk(B.KAnd{}, wbits(p, s), wbits(p, t)), w_and(p, s, t))
60
61def w_diff(+n: Nat, +a: Word(n), +b: Word(n)) -> {wbits(n, Word.and(n, a, Word.not(n, b))) == BL.zipk(B.KDiff{}, wbits(n, a), wbits(n, b)) : List<&2, Bool>}:
62 match n:
63 case 0n:
64 {==}
65 case 1n+p:
66 match a b:
67 case WCon{x, s} WCon{y, t}:
68 LL.cons_cong(Bool, Bool.and(x, Bool.not(y)), wbits(p, Word.and(p, s, Word.not(p, t))), BL.zipk(B.KDiff{}, wbits(p, s), wbits(p, t)), w_diff(p, s, t))
69
70def w_xor(+n: Nat, +a: Word(n), +b: Word(n)) -> {wbits(n, Word.xor(n, a, b)) == BL.zipk(B.KXor{}, wbits(n, a), wbits(n, b)) : List<&2, Bool>}:
71 match n:
72 case 0n:
73 {==}
74 case 1n+p:
75 match a b:
76 case WCon{x, s} WCon{y, t}:
77 LL.cons_cong(Bool, Bool.xor(x, y), wbits(p, Word.xor(p, s, t)), BL.zipk(B.KXor{}, wbits(p, s), wbits(p, t)), w_xor(p, s, t))
78
79def u_op(+k: B.WordOp, +a: U32, +b: U32) -> {ubits(B.word_op(k, a, b)) == BL.zipk(k, ubits(a), ubits(b)) : List<&2, Bool>}:
80 match k a b:
81 case B.KOr{} U32{x} U32{y}:
82 w_or(32n, x, y)
83 case B.KAnd{} U32{x} U32{y}:
84 w_and(32n, x, y)
85 case B.KDiff{} U32{x} U32{y}:
86 w_diff(32n, x, y)
87 case B.KXor{} U32{x} U32{y}:
88 w_xor(32n, x, y)
89
90# ---- low bit ----
91
92def and_zero(+n: Nat, +t: Word(n)) -> {Word.and(n, t, Word.zero(n)) == Word.zero(n) : Word(n)}:
93 match n:
94 case 0n:
95 match t:
96 case WNil{}:
97 {==}
98 case 1n+p:
99 match t:
100 case WCon{True{}, r}:
101 %Equal.sym(Word(p), Word.and(p, r, Word.zero(p)), Word.zero(p), and_zero(p, r)) : {WCon{False{}, _} == WCon{False{}, Word.zero(p)} : Word(1n+p)}
102 {==}
103 case WCon{False{}, r}:
104 %Equal.sym(Word(p), Word.and(p, r, Word.zero(p)), Word.zero(p), and_zero(p, r)) : {WCon{False{}, _} == WCon{False{}, Word.zero(p)} : Word(1n+p)}
105 {==}
106
107def low_word(+b: Bool, +t: Word(31n)) -> {B.low(U32{WCon{b, t}}) == b : Bool}:
108 match b:
109 case True{}:
110 %Equal.sym(Word(31n), Word.and(31n, t, Word.zero(31n)), Word.zero(31n), and_zero(31n, t)) : {Bool.not(U32.is_eq(U32{WCon{True{}, _}}, 0)) == True{} : Bool}
111 {==}
112 case False{}:
113 %Equal.sym(Word(31n), Word.and(31n, t, Word.zero(31n)), Word.zero(31n), and_zero(31n, t)) : {Bool.not(U32.is_eq(U32{WCon{False{}, _}}, 0)) == False{} : Bool}
114 {==}
115
116def low_nth(+x: U32) -> {SC.nth(Bool, ubits(x), 0n) == Some{B.low(x)} : Maybe<&2, Bool>}:
117 match x:
118 case U32{w}:
119 match w:
120 case WCon{b, t}:
121 %Equal.sym(Bool, B.low(U32{WCon{b, t}}), b, low_word(b, t)) : {Some{b} == Some{_} : Maybe<&2, Bool>}
122 {==}
123
124# ---- shifts ----
125
126def pad(+n: Nat, +w: Word(n)) -> {wbits(1n+n, Word.shr.pad(n, w)) == SC.snoc(Bool, wbits(n, w), False{}) : List<&2, Bool>}:
127 match n:
128 case 0n:
129 match w:
130 case WNil{}:
131 {==}
132 case 1n+p:
133 match w:
134 case WCon{b, t}:
135 LL.cons_cong(Bool, b, wbits(1n+p, Word.shr.pad(p, t)), SC.snoc(Bool, wbits(p, t), False{}), pad(p, t))
136
137def u_shr(+b: Bool, +t: Word(31n)) -> {ubits(U32.shr(U32{WCon{b, t}})) == SC.snoc(Bool, wbits(31n, t), False{}) : List<&2, Bool>}:
138 pad(31n, t)
139
140def shr_nth(+x: U32, +j: Nat, +h: {Nat.is_lt(j, 31n) == True{} : Bool}) -> {SC.nth(Bool, ubits(U32.shr(x)), j) == SC.nth(Bool, ubits(x), 1n+j) : Maybe<&2, Bool>}:
141 match x:
142 case U32{w}:
143 match w:
144 case WCon{b, t}:
145 %Equal.sym(List<&2, Bool>, ubits(U32.shr(U32{WCon{b, t}})), SC.snoc(Bool, wbits(31n, t), False{}), u_shr(b, t)) : {SC.nth(Bool, _, j) == SC.nth(Bool, wbits(31n, t), j) : Maybe<&2, Bool>}
146 %Equal.sym(List<&2, Bool>, SC.snoc(Bool, wbits(31n, t), False{}), SC.append(Bool, wbits(31n, t), Con{False{}, Nil{}}), LL.snoc_append(Bool, wbits(31n, t), False{})) : {SC.nth(Bool, _, j) == SC.nth(Bool, wbits(31n, t), j) : Maybe<&2, Bool>}
147 LL.nth_append_left(Bool, wbits(31n, t), Con{False{}, Nil{}}, j, L.subst(Nat, x => {Nat.is_lt(j, x) == True{} : Bool}, 31n, SC.length(Bool, wbits(31n, t)), Equal.sym(Nat, SC.length(Bool, wbits(31n, t)), 31n, len_wbits(31n, t)), h))
148
149def shrn_nth(+k: Nat, +x: U32, +j: Nat, +h: {Nat.is_lt(Nat.add(j, k), 32n) == True{} : Bool}) -> {SC.nth(Bool, ubits(U32.shrn(x, k)), j) == SC.nth(Bool, ubits(x), Nat.add(j, k)) : Maybe<&2, Bool>}:
150 match k:
151 case 0n:
152 %Equal.sym(Nat, Nat.add(j, 0n), j, N.add_zero(j)) : {SC.nth(Bool, ubits(x), j) == SC.nth(Bool, ubits(x), _) : Maybe<&2, Bool>}
153 {==}
154 case 1n+p:
155 %Equal.sym(Nat, Nat.add(j, 1n+p), 1n+Nat.add(j, p), N.add_succ(j, p)) : {SC.nth(Bool, ubits(U32.shr(U32.shrn(x, p))), j) == SC.nth(Bool, ubits(x), _) : Maybe<&2, Bool>}
156 +h1 = L.subst(Nat, v => {Nat.is_lt(v, 32n) == True{} : Bool}, Nat.add(j, 1n+p), 1n+Nat.add(j, p), N.add_succ(j, p), h)
157 Equal.trans(Maybe<&2, Bool>, SC.nth(Bool, ubits(U32.shr(U32.shrn(x, p))), j), SC.nth(Bool, ubits(U32.shrn(x, p)), 1n+j), SC.nth(Bool, ubits(x), 1n+Nat.add(j, p)),
158 shr_nth(U32.shrn(x, p), j, N.le_lt_trans(j, Nat.add(j, p), 31n, N.le_add_right(j, p), h1)),
159 shrn_nth(p, x, 1n+j, h1))
160
161def word_get(+w: U32, +k: Nat, +h: {Nat.is_lt(k, 32n) == True{} : Bool}) -> {Some{B.word_get(w, k)} == SC.nth(Bool, ubits(w), k) : Maybe<&2, Bool>}:
162 Equal.trans(Maybe<&2, Bool>, Some{B.low(U32.shrn(w, k))}, SC.nth(Bool, ubits(U32.shrn(w, k)), 0n), SC.nth(Bool, ubits(w), k),
163 Equal.sym(Maybe<&2, Bool>, SC.nth(Bool, ubits(U32.shrn(w, k)), 0n), Some{B.low(U32.shrn(w, k))}, low_nth(U32.shrn(w, k))),
164 shrn_nth(k, w, 0n, h))
165
166def shl_put(+n: Nat, +c: Bool, +w: Word(n)) -> {wbits(n, Word.shl.put(n, c, w)) == SC.take(Bool, Con{c, wbits(n, w)}, n) : List<&2, Bool>}:
167 match n:
168 case 0n:
169 {==}
170 case 1n+p:
171 match w:
172 case WCon{b, t}:
173 LL.cons_cong(Bool, c, wbits(p, Word.shl.put(p, b, t)), SC.take(Bool, Con{b, wbits(p, t)}, p), shl_put(p, b, t))
174
175def u_shl(+x: U32) -> {ubits(U32.shl(x)) == SC.take(Bool, Con{False{}, ubits(x)}, 32n) : List<&2, Bool>}:
176 match x:
177 case U32{w}:
178 match w:
179 case WCon{b, t}:
180 LL.cons_cong(Bool, False{}, wbits(31n, Word.shl.put(31n, b, t)), SC.take(Bool, Con{b, wbits(31n, t)}, 31n), shl_put(31n, b, t))
181
182# 1 << k is the one-hot mask for bit k.
183def onehot(+k: Nat, +h: {Nat.is_lt(k, 32n) == True{} : Bool}) -> {ubits(U32.shln(1, k)) == SC.update(Bool, BL.rep(32n), k, True{}) : List<&2, Bool>}:
184 match k:
185 case 0n:
186 {==}
187 case 1n+p:
188 +hp = N.lt_trans(p, 1n+p, 32n, N.lt_succ(p), h)
189 %Equal.sym(List<&2, Bool>, ubits(U32.shl(U32.shln(1, p))), SC.take(Bool, Con{False{}, ubits(U32.shln(1, p))}, 32n), u_shl(U32.shln(1, p))) : {_ == SC.update(Bool, BL.rep(32n), 1n+p, True{}) : List<&2, Bool>}
190 %Equal.sym(List<&2, Bool>, ubits(U32.shln(1, p)), SC.update(Bool, BL.rep(32n), p, True{}), onehot(p, hp)) : {SC.take(Bool, Con{False{}, _}, 32n) == SC.update(Bool, BL.rep(32n), 1n+p, True{}) : List<&2, Bool>}
191 LL.cons_cong(Bool, False{}, SC.take(Bool, SC.update(Bool, BL.rep(32n), p, True{}), 31n), SC.update(Bool, BL.rep(31n), p, True{}), BL.take_onehot(31n, p, h))
192
193def word_put(+v: Bool, +w: U32, +k: Nat, +h: {Nat.is_lt(k, 32n) == True{} : Bool}) -> {ubits(B.word_put(v, w, k)) == SC.update(Bool, ubits(w), k, v) : List<&2, Bool>}:
194 match v:
195 case True{}:
196 %Equal.sym(List<&2, Bool>, ubits(B.word_op(B.KOr{}, w, U32.shln(1, k))), BL.zipk(B.KOr{}, ubits(w), ubits(U32.shln(1, k))), u_op(B.KOr{}, w, U32.shln(1, k))) : {_ == SC.update(Bool, ubits(w), k, True{}) : List<&2, Bool>}
197 %Equal.sym(List<&2, Bool>, ubits(U32.shln(1, k)), SC.update(Bool, BL.rep(32n), k, True{}), onehot(k, h)) : {BL.zipk(B.KOr{}, ubits(w), _) == SC.update(Bool, ubits(w), k, True{}) : List<&2, Bool>}
198 %ulen(w) : {BL.zipk(B.KOr{}, ubits(w), SC.update(Bool, BL.rep(_), k, True{})) == SC.update(Bool, ubits(w), k, True{}) : List<&2, Bool>}
199 BL.or_onehot(ubits(w), k)
200 case False{}:
201 %Equal.sym(List<&2, Bool>, ubits(B.word_op(B.KDiff{}, w, U32.shln(1, k))), BL.zipk(B.KDiff{}, ubits(w), ubits(U32.shln(1, k))), u_op(B.KDiff{}, w, U32.shln(1, k))) : {_ == SC.update(Bool, ubits(w), k, False{}) : List<&2, Bool>}
202 %Equal.sym(List<&2, Bool>, ubits(U32.shln(1, k)), SC.update(Bool, BL.rep(32n), k, True{}), onehot(k, h)) : {BL.zipk(B.KDiff{}, ubits(w), _) == SC.update(Bool, ubits(w), k, False{}) : List<&2, Bool>}
203 %ulen(w) : {BL.zipk(B.KDiff{}, ubits(w), SC.update(Bool, BL.rep(_), k, True{})) == SC.update(Bool, ubits(w), k, False{}) : List<&2, Bool>}
204 BL.diff_onehot(ubits(w), k)
205
206# ---- counting and enumeration by repeated shifting ----
207
208def word_count(+m: Nat, +x: U32) -> {B.word_count(m, x) == S.count(SC.take(Bool, ubits(x), m)) : Nat}:
209 match m x:
210 case 0n U32{w}:
211 match w:
212 case WCon{b, t}:
213 {==}
214 case 1n+p U32{w}:
215 match w:
216 case WCon{True{}, t}:
217 %Equal.sym(Bool, B.low(U32{WCon{True{}, t}}), True{}, low_word(True{}, t)) : {Nat.add(B.bit_value(_), B.word_count(p, U32.shr(U32{WCon{True{}, t}}))) == 1n+S.count(SC.take(Bool, wbits(31n, t), p)) : Nat}
218 %Equal.sym(Nat, B.word_count(p, U32.shr(U32{WCon{True{}, t}})), S.count(SC.take(Bool, ubits(U32.shr(U32{WCon{True{}, t}})), p)), word_count(p, U32.shr(U32{WCon{True{}, t}}))) : {1n+_ == 1n+S.count(SC.take(Bool, wbits(31n, t), p)) : Nat}
219 %Equal.sym(List<&2, Bool>, ubits(U32.shr(U32{WCon{True{}, t}})), SC.snoc(Bool, wbits(31n, t), False{}), u_shr(True{}, t)) : {1n+S.count(SC.take(Bool, _, p)) == 1n+S.count(SC.take(Bool, wbits(31n, t), p)) : Nat}
220 N.succ_cong(S.count(SC.take(Bool, SC.snoc(Bool, wbits(31n, t), False{}), p)), S.count(SC.take(Bool, wbits(31n, t), p)), BL.count_take_snoc(wbits(31n, t), p))
221 case WCon{False{}, t}:
222 %Equal.sym(Bool, B.low(U32{WCon{False{}, t}}), False{}, low_word(False{}, t)) : {Nat.add(B.bit_value(_), B.word_count(p, U32.shr(U32{WCon{False{}, t}}))) == S.count(SC.take(Bool, wbits(31n, t), p)) : Nat}
223 %Equal.sym(Nat, B.word_count(p, U32.shr(U32{WCon{False{}, t}})), S.count(SC.take(Bool, ubits(U32.shr(U32{WCon{False{}, t}})), p)), word_count(p, U32.shr(U32{WCon{False{}, t}}))) : {_ == S.count(SC.take(Bool, wbits(31n, t), p)) : Nat}
224 %Equal.sym(List<&2, Bool>, ubits(U32.shr(U32{WCon{False{}, t}})), SC.snoc(Bool, wbits(31n, t), False{}), u_shr(False{}, t)) : {S.count(SC.take(Bool, _, p)) == S.count(SC.take(Bool, wbits(31n, t), p)) : Nat}
225 BL.count_take_snoc(wbits(31n, t), p)
226
227def word_members(+m: Nat, +x: U32, +off: Nat, +rest: List<&2, Nat>) -> {B.word_members(m, x, off, rest) == SC.append(Nat, S.members(SC.take(Bool, ubits(x), m), off), rest) : List<&2, Nat>}:
228 match m x:
229 case 0n U32{w}:
230 match w:
231 case WCon{b, t}:
232 {==}
233 case 1n+p U32{w}:
234 match w:
235 case WCon{True{}, t}:
236 %Equal.sym(Bool, B.low(U32{WCon{True{}, t}}), True{}, low_word(True{}, t)) : {B.member_pick(_, off, B.word_members(p, U32.shr(U32{WCon{True{}, t}}), 1n+off, rest)) == Con{off, SC.append(Nat, S.members(SC.take(Bool, wbits(31n, t), p), 1n+off), rest)} : List<&2, Nat>}
237 %Equal.sym(List<&2, Nat>, B.word_members(p, U32.shr(U32{WCon{True{}, t}}), 1n+off, rest), SC.append(Nat, S.members(SC.take(Bool, ubits(U32.shr(U32{WCon{True{}, t}})), p), 1n+off), rest), word_members(p, U32.shr(U32{WCon{True{}, t}}), 1n+off, rest)) : {Con{off, _} == Con{off, SC.append(Nat, S.members(SC.take(Bool, wbits(31n, t), p), 1n+off), rest)} : List<&2, Nat>}
238 %Equal.sym(List<&2, Bool>, ubits(U32.shr(U32{WCon{True{}, t}})), SC.snoc(Bool, wbits(31n, t), False{}), u_shr(True{}, t)) : {Con{off, SC.append(Nat, S.members(SC.take(Bool, _, p), 1n+off), rest)} == Con{off, SC.append(Nat, S.members(SC.take(Bool, wbits(31n, t), p), 1n+off), rest)} : List<&2, Nat>}
239 %Equal.sym(List<&2, Nat>, S.members(SC.take(Bool, SC.snoc(Bool, wbits(31n, t), False{}), p), 1n+off), S.members(SC.take(Bool, wbits(31n, t), p), 1n+off), BL.members_take_snoc(wbits(31n, t), p, 1n+off)) : {Con{off, SC.append(Nat, _, rest)} == Con{off, SC.append(Nat, S.members(SC.take(Bool, wbits(31n, t), p), 1n+off), rest)} : List<&2, Nat>}
240 {==}
241 case WCon{False{}, t}:
242 %Equal.sym(Bool, B.low(U32{WCon{False{}, t}}), False{}, low_word(False{}, t)) : {B.member_pick(_, off, B.word_members(p, U32.shr(U32{WCon{False{}, t}}), 1n+off, rest)) == SC.append(Nat, S.members(SC.take(Bool, wbits(31n, t), p), 1n+off), rest) : List<&2, Nat>}
243 %Equal.sym(List<&2, Nat>, B.word_members(p, U32.shr(U32{WCon{False{}, t}}), 1n+off, rest), SC.append(Nat, S.members(SC.take(Bool, ubits(U32.shr(U32{WCon{False{}, t}})), p), 1n+off), rest), word_members(p, U32.shr(U32{WCon{False{}, t}}), 1n+off, rest)) : {_ == SC.append(Nat, S.members(SC.take(Bool, wbits(31n, t), p), 1n+off), rest) : List<&2, Nat>}
244 %Equal.sym(List<&2, Bool>, ubits(U32.shr(U32{WCon{False{}, t}})), SC.snoc(Bool, wbits(31n, t), False{}), u_shr(False{}, t)) : {SC.append(Nat, S.members(SC.take(Bool, _, p), 1n+off), rest) == SC.append(Nat, S.members(SC.take(Bool, wbits(31n, t), p), 1n+off), rest) : List<&2, Nat>}
245 %Equal.sym(List<&2, Nat>, S.members(SC.take(Bool, SC.snoc(Bool, wbits(31n, t), False{}), p), 1n+off), S.members(SC.take(Bool, wbits(31n, t), p), 1n+off), BL.members_take_snoc(wbits(31n, t), p, 1n+off)) : {SC.append(Nat, _, rest) == SC.append(Nat, S.members(SC.take(Bool, wbits(31n, t), p), 1n+off), rest) : List<&2, Nat>}
246 {==}