proofs/containers/hash_table/words.bend
bend-collections-laws-containers@1.0.0.0 · 272 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/src/containers/hash_table.bend as H
4
5# Check words, bit by bit (generic in the width; U32 is width 32 = 1 + 31).
6# top(p) the word with only its top bit set (U32: 2^31, H.tag())
7# low(p) every bit but the top one (U32: 2^31 - 1)
8# one(p) the word 1
9
10def top(+p: Nat) -> Word(1n+p):
11 match p:
12 case 0n:
13 WCon{True{}, WNil{}}
14 case 1n+q:
15 WCon{False{}, top(q)}
16
17def low(+p: Nat) -> Word(1n+p):
18 match p:
19 case 0n:
20 WCon{False{}, WNil{}}
21 case 1n+q:
22 WCon{True{}, low(q)}
23
24def one(+p: Nat) -> Word(2n+p):
25 WCon{True{}, Word.zero(1n+p)}
26
27# the top bit
28def topb(+p: Nat, w: Word(1n+p)) -> Bool:
29 match p w:
30 case 0n WCon{b, WNil{}}:
31 b
32 case 1n+q WCon{b, t}:
33 topb(q, t)
34
35def tag_top() -> {H.tag() == U32{top(31n)} : U32}:
36 {==}
37
38def low_lit() -> {2147483647 == U32{low(31n)} : U32}:
39 {==}
40
41def one_lit() -> {1 == U32{one(30n)} : U32}:
42 {==}
43
44def zero_lit() -> {0 == U32{Word.zero(32n)} : U32}:
45 {==}
46
47# ---- comparison with the top bit ----
48
49def ge_fin_false(+c: Cmp, +b: Bool) -> {Cmp.is_ge(Word.cmp.fin(b, False{}, c)) == Cmp.is_ge(c) : Bool}:
50 match c b:
51 case LT{} _:
52 {==}
53 case EQ{} True{}:
54 {==}
55 case EQ{} False{}:
56 {==}
57 case GT{} _:
58 {==}
59
60def ge_top_leaf(+b: Bool) -> {Cmp.is_ge(Word.cmp(1n, WCon{b, WNil{}}, top(0n))) == b : Bool}:
61 match b:
62 case True{}:
63 {==}
64 case False{}:
65 {==}
66
67# w >= 2^p is its top bit
68def ge_top(+p: Nat, +w: Word(1n+p)) -> {Cmp.is_ge(Word.cmp(1n+p, w, top(p))) == topb(p, w) : Bool}:
69 match p w:
70 case 0n WCon{b, WNil{}}:
71 ge_top_leaf(b)
72 case 1n+q WCon{b, t}:
73 Equal.trans(Bool, Cmp.is_ge(Word.cmp.fin(b, False{}, Word.cmp(1n+q, t, top(q)))), Cmp.is_ge(Word.cmp(1n+q, t, top(q))), topb(q, t), ge_fin_false(Word.cmp(1n+q, t, top(q)), b), ge_top(q, t))
74
75# ---- or / and with top and low ----
76
77def or_true(+b: Bool) -> {Bool.or(b, True{}) == True{} : Bool}:
78 match b:
79 case True{}:
80 {==}
81 case False{}:
82 {==}
83
84def or_false(+b: Bool) -> {Bool.or(b, False{}) == b : Bool}:
85 match b:
86 case True{}:
87 {==}
88 case False{}:
89 {==}
90
91def and_true(+b: Bool) -> {Bool.and(b, True{}) == b : Bool}:
92 match b:
93 case True{}:
94 {==}
95 case False{}:
96 {==}
97
98def and_false(+b: Bool) -> {Bool.and(b, False{}) == False{} : Bool}:
99 match b:
100 case True{}:
101 {==}
102 case False{}:
103 {==}
104
105def topb_or_top(+p: Nat, +x: Word(1n+p)) -> {topb(p, Word.or(1n+p, x, top(p))) == True{} : Bool}:
106 match p x:
107 case 0n WCon{b, WNil{}}:
108 or_true(b)
109 case 1n+q WCon{b, t}:
110 topb_or_top(q, t)
111
112def topb_and_low(+p: Nat, +x: Word(1n+p)) -> {topb(p, Word.and(1n+p, x, low(p))) == False{} : Bool}:
113 match p x:
114 case 0n WCon{b, WNil{}}:
115 and_false(b)
116 case 1n+q WCon{b, t}:
117 topb_and_low(q, t)
118
119def topb_or(+p: Nat, +x: Word(1n+p), +y: Word(1n+p)) -> {topb(p, Word.or(1n+p, x, y)) == Bool.or(topb(p, x), topb(p, y)) : Bool}:
120 match p x y:
121 case 0n WCon{a, WNil{}} WCon{b, WNil{}}:
122 {==}
123 case 1n+q WCon{a, s} WCon{b, t}:
124 topb_or(q, s, t)
125
126def topb_zero(+p: Nat) -> {topb(p, Word.zero(1n+p)) == False{} : Bool}:
127 match p:
128 case 0n:
129 {==}
130 case 1n+q:
131 topb_zero(q)
132
133def topb_one(+p: Nat) -> {topb(1n+p, one(p)) == False{} : Bool}:
134 topb_zero(p)
135
136# clearing the top bit of x with the top bit set gives back x without it
137def and_low_or_top(+p: Nat, +x: Word(1n+p), +h: {topb(p, x) == False{} : Bool}) -> {Word.and(1n+p, Word.or(1n+p, x, top(p)), low(p)) == x : Word(1n+p)}:
138 match p x:
139 case 0n WCon{b, WNil{}}:
140 Equal.cong(Bool, Word(1n), c => WCon{c, WNil{}}, Bool.and(Bool.or(b, True{}), False{}), b, Equal.trans(Bool, Bool.and(Bool.or(b, True{}), False{}), False{}, b, and_false(Bool.or(b, True{})), Equal.sym(Bool, b, False{}, h)))
141 case 1n+q WCon{b, t}:
142 +e1 = Equal.trans(Bool, Bool.and(Bool.or(b, False{}), True{}), Bool.or(b, False{}), b, and_true(Bool.or(b, False{})), or_false(b))
143 +e2 = and_low_or_top(q, t, h)
144 Equal.trans(Word(2n+q), WCon{Bool.and(Bool.or(b, False{}), True{}), Word.and(1n+q, Word.or(1n+q, t, top(q)), low(q))}, WCon{b, Word.and(1n+q, Word.or(1n+q, t, top(q)), low(q))}, WCon{b, t},
145 Equal.cong(Bool, Word(2n+q), c => WCon{c, Word.and(1n+q, Word.or(1n+q, t, top(q)), low(q))}, Bool.and(Bool.or(b, False{}), True{}), b, e1),
146 Equal.cong(Word(1n+q), Word(2n+q), w => WCon{b, w}, Word.and(1n+q, Word.or(1n+q, t, top(q)), low(q)), t, e2))
147
148# ---- nonzero words ----
149
150def eq_fin_false(+b: Bool, +c: Cmp, +h: {Cmp.is_eq(c) == False{} : Bool}) -> {Cmp.is_eq(Word.cmp.fin(b, False{}, c)) == False{} : Bool}:
151 match c:
152 case LT{}:
153 {==}
154 case EQ{}:
155 Empty.absurd({Cmp.is_eq(Word.cmp.fin(b, False{}, EQ{})) == False{} : Bool}, L.true_false(h))
156 case GT{}:
157 {==}
158
159def top_nonzero_g(+p: Nat, +w: Word(1n+p), +h: {topb(p, w) == True{} : Bool}) -> {Cmp.is_eq(Word.cmp(1n+p, w, Word.zero(1n+p))) == False{} : Bool}:
160 match p w:
161 case 0n WCon{True{}, WNil{}}:
162 {==}
163 case 0n WCon{False{}, WNil{}}:
164 Empty.absurd({Cmp.is_eq(Word.cmp(1n, WCon{False{}, WNil{}}, Word.zero(1n))) == False{} : Bool}, L.false_true(h))
165 case 1n+q WCon{b, t}:
166 eq_fin_false(b, Word.cmp(1n+q, t, Word.zero(1n+q)), top_nonzero_g(q, t, h))
167
168def fin_tf(+c: Cmp) -> {Cmp.is_eq(Word.cmp.fin(True{}, False{}, c)) == False{} : Bool}:
169 match c:
170 case LT{}:
171 {==}
172 case EQ{}:
173 {==}
174 case GT{}:
175 {==}
176
177def bit0_nonzero(+p: Nat, +t: Word(p)) -> {Cmp.is_eq(Word.cmp(1n+p, WCon{True{}, t}, Word.zero(1n+p))) == False{} : Bool}:
178 fin_tf(Word.cmp(p, t, Word.zero(p)))
179
180# ---- the U32 check words ----
181
182def lt_ge(+c: Cmp) -> {Cmp.is_lt(c) == Bool.not(Cmp.is_ge(c)) : Bool}:
183 match c:
184 case LT{}:
185 {==}
186 case EQ{}:
187 {==}
188 case GT{}:
189 {==}
190
191def not_true(+b: Bool, +h: {Bool.not(b) == True{} : Bool}) -> {b == False{} : Bool}:
192 match b:
193 case True{}:
194 Empty.absurd({True{} == False{} : Bool}, L.false_true(h))
195 case False{}:
196 {==}
197
198# a code below 2^31 has its top bit clear
199def small_top(+cw: Word(32n), +h: {U32.is_lt(U32{cw}, H.tag()) == True{} : Bool}) -> {topb(31n, cw) == False{} : Bool}:
200 +c = Word.cmp(32n, cw, top(31n))
201 not_true(topb(31n, cw), Equal.trans(Bool, Bool.not(topb(31n, cw)), Bool.not(Cmp.is_ge(c)), True{}, Equal.cong(Bool, Bool, z => Bool.not(z), topb(31n, cw), Cmp.is_ge(c), Equal.sym(Bool, Cmp.is_ge(c), topb(31n, cw), ge_top(31n, cw))), Equal.trans(Bool, Bool.not(Cmp.is_ge(c)), Cmp.is_lt(c), True{}, Equal.sym(Bool, Cmp.is_lt(c), Bool.not(Cmp.is_ge(c)), lt_ge(c)), h)))
202
203def is_short_top(+w: Word(32n)) -> {H.is_short(U32{w}) == topb(31n, w) : Bool}:
204 ge_top(31n, w)
205
206def short_is_short(+c: U32) -> {H.is_short(H.short_word(c)) == True{} : Bool}:
207 match c:
208 case U32{+cw}:
209 Equal.trans(Bool, H.is_short(U32{Word.or(32n, cw, top(31n))}), topb(31n, Word.or(32n, cw, top(31n))), True{}, is_short_top(Word.or(32n, cw, top(31n))), topb_or_top(31n, cw))
210
211def short_nonzero(+c: U32) -> {U32.is_eq(H.short_word(c), 0) == False{} : Bool}:
212 match c:
213 case U32{+cw}:
214 top_nonzero_g(31n, Word.or(32n, cw, top(31n)), topb_or_top(31n, cw))
215
216# masking a short word gives back its character code
217def short_back(+c: U32, +h: {U32.is_lt(c, H.tag()) == True{} : Bool}) -> {U32.and(H.short_word(c), 2147483647) == c : U32}:
218 match c:
219 case U32{+cw}:
220 Equal.cong(Word(32n), U32, w => U32{w}, Word.and(32n, Word.or(32n, cw, top(31n)), low(31n)), cw, and_low_or_top(31n, cw, small_top(cw, h)))
221
222def short_inj(+a: U32, +b: U32, +ha: {U32.is_lt(a, H.tag()) == True{} : Bool}, +hb: {U32.is_lt(b, H.tag()) == True{} : Bool}, +e: {H.short_word(a) == H.short_word(b) : U32}) -> {a == b : U32}:
223 Equal.trans(U32, a, U32.and(H.short_word(a), 2147483647), b, Equal.sym(U32, U32.and(H.short_word(a), 2147483647), a, short_back(a, ha)),
224 Equal.trans(U32, U32.and(H.short_word(a), 2147483647), U32.and(H.short_word(b), 2147483647), b, Equal.cong(U32, U32, z => U32.and(z, 2147483647), H.short_word(a), H.short_word(b), e), short_back(b, hb)))
225
226def lw_word(+hw: Word(32n)) -> Word(32n):
227 Word.or(32n, Word.and(32n, hw, low(31n)), one(30n))
228
229def long_top(+hw: Word(32n)) -> {topb(31n, lw_word(hw)) == False{} : Bool}:
230 +x = Word.and(32n, hw, low(31n))
231 %Equal.sym(Bool, topb(31n, Word.or(32n, x, one(30n))), Bool.or(topb(31n, x), topb(31n, one(30n))), topb_or(31n, x, one(30n))) : {_ == False{} : Bool}
232 %Equal.sym(Bool, topb(31n, x), False{}, topb_and_low(31n, hw)) : {Bool.or(_, topb(31n, one(30n))) == False{} : Bool}
233 topb_one(30n)
234
235def long_is_long(+h: U32) -> {H.is_short(H.long_word(h)) == False{} : Bool}:
236 match h:
237 case U32{+hw}:
238 Equal.trans(Bool, H.is_short(U32{lw_word(hw)}), topb(31n, lw_word(hw)), False{}, is_short_top(lw_word(hw)), long_top(hw))
239
240def or_bit0(+p: Nat, +b: Bool, +t: Word(p)) -> {Word.or(1n+p, WCon{b, t}, WCon{True{}, Word.zero(p)}) == WCon{True{}, Word.or(p, t, Word.zero(p))} : Word(1n+p)}:
241 Equal.cong(Bool, Word(1n+p), z => WCon{z, Word.or(p, t, Word.zero(p))}, Bool.or(b, True{}), True{}, or_true(b))
242
243def long_nonzero(+h: U32) -> {U32.is_eq(H.long_word(h), 0) == False{} : Bool}:
244 match h:
245 case U32{WCon{+b0, +rest}}:
246 +b = Bool.and(b0, True{})
247 +t = Word.and(31n, rest, low(30n))
248 +u = Word.or(31n, t, Word.zero(31n))
249 L.subst(Word(32n), w => {Cmp.is_eq(Word.cmp(32n, w, Word.zero(32n))) == False{} : Bool}, WCon{True{}, u}, lw_word(WCon{b0, rest}), Equal.sym(Word(32n), lw_word(WCon{b0, rest}), WCon{True{}, u}, or_bit0(31n, b, t)), bit0_nonzero(31n, u))
250
251# a long word is never a short word
252def long_not_short(+h: U32, +c: U32, +e: {H.long_word(h) == H.short_word(c) : U32}) -> Empty:
253 L.true_false(Equal.trans(Bool, True{}, H.is_short(H.short_word(c)), False{}, Equal.sym(Bool, H.is_short(H.short_word(c)), True{}, short_is_short(c)), Equal.trans(Bool, H.is_short(H.short_word(c)), H.is_short(H.long_word(h)), False{}, Equal.cong(U32, Bool, z => H.is_short(z), H.short_word(c), H.long_word(h), Equal.sym(U32, H.long_word(h), H.short_word(c), e)), long_is_long(h))))
254
255
256
257
258# a word with its top bit set is its low bits with the top bit set
259def or_and_low_top(+p: Nat, +x: Word(1n+p), +h: {topb(p, x) == True{} : Bool}) -> {Word.or(1n+p, Word.and(1n+p, x, low(p)), top(p)) == x : Word(1n+p)}:
260 match p x:
261 case 0n WCon{b, WNil{}}:
262 Equal.cong(Bool, Word(1n), c => WCon{c, WNil{}}, Bool.or(Bool.and(b, False{}), True{}), b, Equal.trans(Bool, Bool.or(Bool.and(b, False{}), True{}), True{}, b, or_true(Bool.and(b, False{})), Equal.sym(Bool, b, True{}, h)))
263 case 1n+q WCon{b, t}:
264 +e1 = Equal.trans(Bool, Bool.or(Bool.and(b, True{}), False{}), Bool.and(b, True{}), b, or_false(Bool.and(b, True{})), and_true(b))
265 Equal.trans(Word(2n+q), WCon{Bool.or(Bool.and(b, True{}), False{}), Word.or(1n+q, Word.and(1n+q, t, low(q)), top(q))}, WCon{b, Word.or(1n+q, Word.and(1n+q, t, low(q)), top(q))}, WCon{b, t},
266 Equal.cong(Bool, Word(2n+q), c => WCon{c, Word.or(1n+q, Word.and(1n+q, t, low(q)), top(q))}, Bool.or(Bool.and(b, True{}), False{}), b, e1),
267 Equal.cong(Word(1n+q), Word(2n+q), w => WCon{b, w}, Word.or(1n+q, Word.and(1n+q, t, low(q)), top(q)), t, or_and_low_top(q, t, h)))
268
269def short_eta(+x: U32, +h: {H.is_short(x) == True{} : Bool}) -> {H.short_word(U32.and(x, 2147483647)) == x : U32}:
270 match x:
271 case U32{+w}:
272 Equal.cong(Word(32n), U32, z => U32{z}, Word.or(32n, Word.and(32n, w, low(31n)), top(31n)), w, or_and_low_top(31n, w, Equal.trans(Bool, topb(31n, w), H.is_short(U32{w}), True{}, Equal.sym(Bool, H.is_short(U32{w}), topb(31n, w), is_short_top(w)), h)))