u32.bend
bend-mathlib@0.8.0.0 · 1,059 lines · 0 definitions
1# bend-mathlib/u32.bend: machine words as naturals; Word(n) and U32 operations agree with Nat arithmetic
2# (compare, add, sub, inc, not, min, max, from_nat).
3import Base
4import bend-mathlib@0.8.0.0/nat.bend as MNat
5
6def internal_succ_double_lt(a: Nat, b: Nat, h: MNat.lt(a, b)) -> MNat.lt(1n+Nat.double(a), Nat.double(b)):
7 match a b:
8 case 0n 0n:
9 Empty.absurd(MNat.lt(1n, 0n), MNat.internal_false_ne_true(h))
10 case 0n 1n+q:
11 {==}
12 case 1n+p 0n:
13 Empty.absurd(MNat.lt(3n+Nat.double(p), 0n), MNat.internal_false_ne_true(h))
14 case 1n+p 1n+q:
15 internal_succ_double_lt(p, q, h)
16
17# A word's value is below two to the width: to_nat w < 2^n.
18law word_to_nat_lt:
19 for n: Nat
20 for w: Word(n)
21 MNat.lt(Word.to_nat(n, w), Nat.pow(2n, n))
22
23def word_to_nat_lt(n, w):
24 match n:
25 case 0n:
26 {==}
27 case 1n++p:
28 match w:
29 case WCon{False{}, t}:
30 +t = t
31 %MNat.two_pow_succ_sym(p) : MNat.lt(Nat.double(Word.to_nat(p, t)), _)
32 MNat.double_lt_double(Word.to_nat(p, t), Nat.pow(2n, p), word_to_nat_lt(p, t))
33 case WCon{True{}, t}:
34 +t = t
35 %MNat.two_pow_succ_sym(p) : MNat.lt(1n+Nat.double(Word.to_nat(p, t)), _)
36 internal_succ_double_lt(Word.to_nat(p, t), Nat.pow(2n, p), word_to_nat_lt(p, t))
37
38# The zero word is the natural zero: to_nat (zero n) = 0.
39law word_to_nat_zero:
40 for n: Nat
41 {Word.to_nat(n, Word.zero(n)) == 0n : Nat}
42
43def word_to_nat_zero(n):
44 match n:
45 case 0n:
46 {==}
47 case 1n++p:
48 Equal.cong(Nat, Nat, x => Nat.double(x), Word.to_nat(p, Word.zero(p)), 0n, word_to_nat_zero(p))
49
50# Distinct words have distinct values: to_nat a = to_nat b implies a = b.
51law word_to_nat_inj:
52 for n: Nat
53 for a: Word(n)
54 for b: Word(n)
55 for e: {Word.to_nat(n, a) == Word.to_nat(n, b) : Nat}
56 {a == b : Word(n)}
57
58def word_to_nat_inj(n, a, b, e):
59 match n:
60 case 0n:
61 match a b:
62 case WNil{} WNil{}:
63 {==}
64 case 1n++p:
65 match a b:
66 case WCon{False{}, +at} WCon{False{}, +bt}:
67 Equal.cong(Word(p), Word(1n+p), w => WCon{False{}, w}, at, bt, word_to_nat_inj(p, at, bt, MNat.double_inj(Word.to_nat(p, at), Word.to_nat(p, bt), e)))
68 case WCon{True{}, +at} WCon{True{}, +bt}:
69 Equal.cong(Word(p), Word(1n+p), w => WCon{True{}, w}, at, bt, word_to_nat_inj(p, at, bt, MNat.double_inj(Word.to_nat(p, at), Word.to_nat(p, bt), MNat.succ_inj(Nat.double(Word.to_nat(p, at)), Nat.double(Word.to_nat(p, bt)), e))))
70 case WCon{False{}, +at} WCon{True{}, +bt}:
71 Empty.absurd({WCon{False{}, at} == WCon{True{}, bt} : Word(1n+p)}, MNat.double_ne_succ_double(Word.to_nat(p, at), Word.to_nat(p, bt))(e))
72 case WCon{True{}, +at} WCon{False{}, +bt}:
73 Empty.absurd({WCon{True{}, at} == WCon{False{}, bt} : Word(1n+p)}, MNat.double_ne_succ_double(Word.to_nat(p, bt), Word.to_nat(p, at))(Equal.sym(Nat, 1n+Nat.double(Word.to_nat(p, at)), Nat.double(Word.to_nat(p, bt)), e)))
74
75def internal_bv(b: Bool) -> Nat:
76 Bool.pick(Nat, b, 1n, 0n)
77
78def internal_to_nat_con(-p: Nat, b: Bool, -t: Word(p)) -> {Nat.add(internal_bv(b), Nat.double(Word.to_nat(p, t))) == Word.to_nat(1n+p, WCon{b, t}) : Nat}:
79 match b:
80 case False{}:
81 {==}
82 case True{}:
83 {==}
84
85def internal_cmp_bits(x: Nat, y: Nat, ab: Bool, bb: Bool) -> {Word.cmp.fin(ab, bb, Nat.cmp(x, y)) == Nat.cmp(Nat.add(internal_bv(ab), Nat.double(x)), Nat.add(internal_bv(bb), Nat.double(y))) : Cmp}:
86 match x y:
87 case 0n 0n:
88 match ab bb:
89 case False{} False{}:
90 {==}
91 case False{} True{}:
92 {==}
93 case True{} False{}:
94 {==}
95 case True{} True{}:
96 {==}
97 case 0n 1n+q:
98 match ab bb:
99 case False{} False{}:
100 {==}
101 case False{} True{}:
102 {==}
103 case True{} False{}:
104 {==}
105 case True{} True{}:
106 {==}
107 case 1n+p 0n:
108 match ab bb:
109 case False{} False{}:
110 {==}
111 case False{} True{}:
112 {==}
113 case True{} False{}:
114 {==}
115 case True{} True{}:
116 {==}
117 case 1n+p 1n+q:
118 match ab bb:
119 case False{} False{}:
120 internal_cmp_bits(p, q, False{}, False{})
121 case False{} True{}:
122 internal_cmp_bits(p, q, False{}, True{})
123 case True{} False{}:
124 internal_cmp_bits(p, q, True{}, False{})
125 case True{} True{}:
126 internal_cmp_bits(p, q, True{}, True{})
127
128# Comparing words compares their values: cmp a b = cmp (to_nat a) (to_nat b).
129law word_cmp_to_nat:
130 for n: Nat
131 for a: Word(n)
132 for b: Word(n)
133 {Word.cmp(n, a, b) == Nat.cmp(Word.to_nat(n, a), Word.to_nat(n, b)) : Cmp}
134
135def word_cmp_to_nat(n, a, b):
136 match n:
137 case 0n:
138 {==}
139 case 1n++p:
140 match a b:
141 case WCon{+ab, +at} WCon{+bb, +bt}:
142 %internal_to_nat_con(p, ab, at) : {Word.cmp.fin(ab, bb, Word.cmp(p, at, bt)) == Nat.cmp(_, Word.to_nat(1n+p, WCon{bb, bt})) : Cmp}
143 %internal_to_nat_con(p, bb, bt) : {Word.cmp.fin(ab, bb, Word.cmp(p, at, bt)) == Nat.cmp(Nat.add(internal_bv(ab), Nat.double(Word.to_nat(p, at))), _) : Cmp}
144 %Equal.sym(Cmp, Word.cmp(p, at, bt), Nat.cmp(Word.to_nat(p, at), Word.to_nat(p, bt)), word_cmp_to_nat(p, at, bt)) : {Word.cmp.fin(ab, bb, _) == Nat.cmp(Nat.add(internal_bv(ab), Nat.double(Word.to_nat(p, at))), Nat.add(internal_bv(bb), Nat.double(Word.to_nat(p, bt)))) : Cmp}
145 internal_cmp_bits(Word.to_nat(p, at), Word.to_nat(p, bt), ab, bb)
146
147# One plus a word plus its complement is two to the width: 1 + to_nat (not w) + to_nat w = 2^n.
148law word_not_add:
149 for n: Nat
150 for w: Word(n)
151 {1n+Nat.add(Word.to_nat(n, Word.not(n, w)), Word.to_nat(n, w)) == Nat.pow(2n, n) : Nat}
152
153def word_not_add(n, w):
154 match n:
155 case 0n:
156 {==}
157 case 1n++p:
158 match w:
159 case WCon{False{}, +t}:
160 -u = Word.to_nat(p, Word.not(p, t))
161 -x = Word.to_nat(p, t)
162 %MNat.two_pow_succ_sym(p) : {2n+Nat.add(Nat.double(u), Nat.double(x)) == _ : Nat}
163 %word_not_add(p, t) : {2n+Nat.add(Nat.double(u), Nat.double(x)) == Nat.double(_) : Nat}
164 %MNat.double_add(Word.to_nat(p, Word.not(p, t)), Word.to_nat(p, t)) : {2n+_ == 2n+Nat.double(Nat.add(u, x)) : Nat}
165 {==}
166 case WCon{True{}, +t}:
167 -u = Word.to_nat(p, Word.not(p, t))
168 -x = Word.to_nat(p, t)
169 %MNat.add_succ_sym(Nat.double(Word.to_nat(p, Word.not(p, t))), Nat.double(Word.to_nat(p, t))) : {1n+_ == Nat.pow(2n, 1n+p) : Nat}
170 %MNat.two_pow_succ_sym(p) : {2n+Nat.add(Nat.double(u), Nat.double(x)) == _ : Nat}
171 %word_not_add(p, t) : {2n+Nat.add(Nat.double(u), Nat.double(x)) == Nat.double(_) : Nat}
172 %MNat.double_add(Word.to_nat(p, Word.not(p, t)), Word.to_nat(p, t)) : {2n+_ == 2n+Nat.double(Nat.add(u, x)) : Nat}
173 {==}
174
175def internal_pick_pow(o: Bool, p: Nat) -> {Nat.double(Bool.pick(Nat, o, Nat.pow(2n, p), 0n)) == Bool.pick(Nat, o, Nat.pow(2n, 1n+p), 0n) : Nat}:
176 match o:
177 case False{}:
178 {==}
179 case True{}:
180 MNat.two_pow_succ_sym(p)
181
182def internal_carry(n: Nat, a: Word(n), b: Word(n), c: Bool) -> Bool:
183 match n:
184 case 0n:
185 c
186 case 1n+p:
187 match a b:
188 case WCon{False{}, at} WCon{+bb, bt}:
189 internal_carry(p, at, bt, Bool.and(bb, c))
190 case WCon{True{}, at} WCon{+bb, bt}:
191 internal_carry(p, at, bt, Bool.or(bb, c))
192
193def internal_full_add(a: Bool, b: Bool, c: Bool) -> {Nat.add(Nat.add(internal_bv(a), internal_bv(b)), internal_bv(c)) == Nat.add(internal_bv(Pair.fst(Bool, Bool, Bool.full_add(a, b, c))), Nat.double(internal_bv(Pair.snd(Bool, Bool, Bool.full_add(a, b, c))))) : Nat}:
194 match a b c:
195 case False{} False{} False{}:
196 {==}
197 case False{} False{} True{}:
198 {==}
199 case False{} True{} False{}:
200 {==}
201 case False{} True{} True{}:
202 {==}
203 case True{} False{} False{}:
204 {==}
205 case True{} False{} True{}:
206 {==}
207 case True{} True{} False{}:
208 {==}
209 case True{} True{} True{}:
210 {==}
211
212def internal_adc_nat(+s: Nat, +k: Nat, +a: Nat, +b: Nat, +c: Nat, +e: Nat, +q: Nat, +x: Nat, +y: Nat,
213 ih: {Nat.add(e, q) == Nat.add(Nat.add(x, y), k) : Nat},
214 fa: {Nat.add(Nat.add(a, b), c) == Nat.add(s, Nat.double(k)) : Nat})
215 -> {Nat.add(Nat.add(s, Nat.double(e)), Nat.double(q)) == Nat.add(Nat.add(Nat.add(a, Nat.double(x)), Nat.add(b, Nat.double(y))), c) : Nat}:
216 -d = Nat.double(Nat.add(x, y))
217 -r = Nat.add(Nat.add(Nat.add(a, Nat.double(x)), Nat.add(b, Nat.double(y))), c)
218 %MNat.add_assoc_sym(s, Nat.double(e), Nat.double(q)) : {_ == r : Nat}
219 %MNat.double_add(e, q) : {Nat.add(s, _) == r : Nat}
220 %Equal.sym(Nat, Nat.add(e, q), Nat.add(Nat.add(x, y), k), ih) : {Nat.add(s, Nat.double(_)) == r : Nat}
221 %MNat.double_add_sym(Nat.add(x, y), k) : {Nat.add(s, _) == r : Nat}
222 -l = Nat.add(s, Nat.add(d, Nat.double(k)))
223 %MNat.add_add_add_comm(a, b, Nat.double(x), Nat.double(y)) : {l == Nat.add(_, c) : Nat}
224 %MNat.double_add(x, y) : {l == Nat.add(Nat.add(Nat.add(a, b), _), c) : Nat}
225 %MNat.add_right_comm_sym(Nat.add(a, b), Nat.double(Nat.add(x, y)), c) : {l == _ : Nat}
226 %Equal.sym(Nat, Nat.add(Nat.add(a, b), c), Nat.add(s, Nat.double(k)), fa) : {l == Nat.add(_, d) : Nat}
227 %MNat.add_assoc_sym(s, Nat.double(k), Nat.double(Nat.add(x, y))) : {l == _ : Nat}
228 %MNat.add_comm(Nat.double(Nat.add(x, y)), Nat.double(k)) : {l == Nat.add(s, _) : Nat}
229 {==}
230
231def internal_adc_core(n: Nat, a: Word(n), b: Word(n), c: Bool) -> {Nat.add(Word.to_nat(n, Word.adc(n, a, b, False{}, c)), Bool.pick(Nat, internal_carry(n, a, b, c), Nat.pow(2n, n), 0n)) == Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), internal_bv(c)) : Nat}:
232 match n:
233 case 0n:
234 match c:
235 case False{}:
236 {==}
237 case True{}:
238 {==}
239 case 1n++p:
240 match a b:
241 case WCon{False{}, +at} WCon{+bb, +bt}:
242 +c = c
243 -e = Word.adc(p, at, bt, False{}, Bool.and(bb, c))
244 -o = internal_carry(p, at, bt, Bool.and(bb, c))
245 -r = Nat.add(Nat.add(Word.to_nat(1n+p, WCon{False{}, at}), Word.to_nat(1n+p, WCon{bb, bt})), internal_bv(c))
246 %internal_to_nat_con(p, Bool.xor(bb, c), Word.adc(p, at, bt, False{}, Bool.and(bb, c))) : {Nat.add(_, Bool.pick(Nat, o, Nat.pow(2n, 1n+p), 0n)) == r : Nat}
247 %internal_pick_pow(internal_carry(p, at, bt, Bool.and(bb, c)), p) : {Nat.add(Nat.add(internal_bv(Bool.xor(bb, c)), Nat.double(Word.to_nat(p, e))), _) == r : Nat}
248 -l = Nat.add(Nat.add(internal_bv(Bool.xor(bb, c)), Nat.double(Word.to_nat(p, e))), Nat.double(Bool.pick(Nat, o, Nat.pow(2n, p), 0n)))
249 %internal_to_nat_con(p, False{}, at) : {l == Nat.add(Nat.add(_, Word.to_nat(1n+p, WCon{bb, bt})), internal_bv(c)) : Nat}
250 %internal_to_nat_con(p, bb, bt) : {l == Nat.add(Nat.add(Nat.add(internal_bv(False{}), Nat.double(Word.to_nat(p, at))), _), internal_bv(c)) : Nat}
251 internal_adc_nat(internal_bv(Bool.xor(bb, c)), internal_bv(Bool.and(bb, c)), internal_bv(False{}), internal_bv(bb), internal_bv(c), Word.to_nat(p, Word.adc(p, at, bt, False{}, Bool.and(bb, c))), Bool.pick(Nat, internal_carry(p, at, bt, Bool.and(bb, c)), Nat.pow(2n, p), 0n), Word.to_nat(p, at), Word.to_nat(p, bt), internal_adc_core(p, at, bt, Bool.and(bb, c)), internal_full_add(False{}, bb, c))
252 case WCon{True{}, +at} WCon{+bb, +bt}:
253 +c = c
254 -e = Word.adc(p, at, bt, False{}, Bool.or(bb, c))
255 -o = internal_carry(p, at, bt, Bool.or(bb, c))
256 -r = Nat.add(Nat.add(Word.to_nat(1n+p, WCon{True{}, at}), Word.to_nat(1n+p, WCon{bb, bt})), internal_bv(c))
257 %internal_to_nat_con(p, Bool.not(Bool.xor(bb, c)), Word.adc(p, at, bt, False{}, Bool.or(bb, c))) : {Nat.add(_, Bool.pick(Nat, o, Nat.pow(2n, 1n+p), 0n)) == r : Nat}
258 %internal_pick_pow(internal_carry(p, at, bt, Bool.or(bb, c)), p) : {Nat.add(Nat.add(internal_bv(Bool.not(Bool.xor(bb, c))), Nat.double(Word.to_nat(p, e))), _) == r : Nat}
259 -l = Nat.add(Nat.add(internal_bv(Bool.not(Bool.xor(bb, c))), Nat.double(Word.to_nat(p, e))), Nat.double(Bool.pick(Nat, o, Nat.pow(2n, p), 0n)))
260 %internal_to_nat_con(p, True{}, at) : {l == Nat.add(Nat.add(_, Word.to_nat(1n+p, WCon{bb, bt})), internal_bv(c)) : Nat}
261 %internal_to_nat_con(p, bb, bt) : {l == Nat.add(Nat.add(Nat.add(internal_bv(True{}), Nat.double(Word.to_nat(p, at))), _), internal_bv(c)) : Nat}
262 internal_adc_nat(internal_bv(Bool.not(Bool.xor(bb, c))), internal_bv(Bool.or(bb, c)), internal_bv(True{}), internal_bv(bb), internal_bv(c), Word.to_nat(p, Word.adc(p, at, bt, False{}, Bool.or(bb, c))), Bool.pick(Nat, internal_carry(p, at, bt, Bool.or(bb, c)), Nat.pow(2n, p), 0n), Word.to_nat(p, at), Word.to_nat(p, bt), internal_adc_core(p, at, bt, Bool.or(bb, c)), internal_full_add(True{}, bb, c))
263
264def internal_lt_congl(-x: Nat, -y: Nat, -m: Nat, e: {x == y : Nat}, h: MNat.lt(x, m)) -> MNat.lt(y, m):
265 %e : MNat.lt(_, m)
266 h
267
268def internal_le_congr(-m: Nat, -x: Nat, -y: Nat, e: {y == x : Nat}, h: MNat.le(m, y)) -> MNat.le(m, x):
269 %e : MNat.le(m, _)
270 h
271
272def internal_fin_exact(+e: Nat, +s: Nat, +m: Nat, o: Bool, eq: {Nat.add(e, Bool.pick(Nat, o, m, 0n)) == s : Nat}, h: MNat.lt(s, m)) -> {e == s : Nat}:
273 match o:
274 case False{}:
275 Equal.trans(Nat, e, Nat.add(e, 0n), s, MNat.add_zero_sym(e), eq)
276 case True{}:
277 +le = MNat.le_of_add_eq(m, e, s, Equal.trans(Nat, Nat.add(m, e), Nat.add(e, m), s, MNat.add_comm(m, e), eq))
278 Empty.absurd({e == s : Nat}, MNat.lt_irrefl(s)(MNat.lt_of_lt_of_le(s, m, s, h, le)))
279
280def internal_fin_wrap(+e: Nat, -s: Nat, +m: Nat, o: Bool, eq: {Nat.add(e, Bool.pick(Nat, o, m, 0n)) == s : Nat}, h: MNat.lt(e, m)) -> {e == Nat.mod(s, m) : Nat}:
281 match o:
282 case False{}:
283 %eq : {e == Nat.mod(_, m) : Nat}
284 %MNat.add_zero_sym(e) : {e == Nat.mod(_, m) : Nat}
285 Equal.sym(Nat, Nat.mod(e, m), e, MNat.mod_eq_of_lt(e, m, h))
286 case True{}:
287 %eq : {e == Nat.mod(_, m) : Nat}
288 %MNat.add_comm(m, e) : {e == Nat.mod(_, m) : Nat}
289 %MNat.add_mod_left_sym(e, m) : {e == _ : Nat}
290 Equal.sym(Nat, Nat.mod(e, m), e, MNat.mod_eq_of_lt(e, m, h))
291
292def internal_fin_over(+e: Nat, +s: Nat, +m: Nat, o: Bool, eq: {Nat.add(e, Bool.pick(Nat, o, m, 0n)) == s : Nat}, h: MNat.lt(e, m), le: MNat.le(m, s)) -> {Nat.add(e, m) == s : Nat}:
293 match o:
294 case False{}:
295 +es = Equal.trans(Nat, e, Nat.add(e, 0n), s, MNat.add_zero_sym(e), eq)
296 Empty.absurd({Nat.add(e, m) == s : Nat}, MNat.lt_irrefl(m)(MNat.lt_of_le_of_lt(m, s, m, le, internal_lt_congl(e, s, m, es, h))))
297 case True{}:
298 eq
299
300# The adder is exact below the overflow: a + b + carry-in < 2^n implies to_nat (adc a b False c) = a + b + carry-in.
301law word_adc_exact:
302 for n: Nat
303 for a: Word(n)
304 for b: Word(n)
305 for c: Bool
306 for h: MNat.lt(Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)), Nat.pow(2n, n))
307 {Word.to_nat(n, Word.adc(n, a, b, False{}, c)) == Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)) : Nat}
308
309def word_adc_exact(n, a, b, c, h):
310 +n = n
311 +a = a
312 +b = b
313 +c = c
314 internal_fin_exact(Word.to_nat(n, Word.adc(n, a, b, False{}, c)), Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)), Nat.pow(2n, n), internal_carry(n, a, b, c), internal_adc_core(n, a, b, c), h)
315
316# The adder drops exactly one 2^n on overflow: 2^n <= a + b + carry-in implies to_nat (adc a b False c) + 2^n = a + b + carry-in.
317law word_adc_overflow:
318 for n: Nat
319 for a: Word(n)
320 for b: Word(n)
321 for c: Bool
322 for h: MNat.le(Nat.pow(2n, n), Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)))
323 {Nat.add(Word.to_nat(n, Word.adc(n, a, b, False{}, c)), Nat.pow(2n, n)) == Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)) : Nat}
324
325def word_adc_overflow(n, a, b, c, h):
326 +n = n
327 +a = a
328 +b = b
329 +c = c
330 internal_fin_over(Word.to_nat(n, Word.adc(n, a, b, False{}, c)), Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)), Nat.pow(2n, n), internal_carry(n, a, b, c), internal_adc_core(n, a, b, c), word_to_nat_lt(n, Word.adc(n, a, b, False{}, c)), h)
331
332# The adder wraps modulo 2^n: to_nat (adc a b False c) = (a + b + carry-in) % 2^n.
333law word_adc_wrap:
334 for n: Nat
335 for a: Word(n)
336 for b: Word(n)
337 for c: Bool
338 {Word.to_nat(n, Word.adc(n, a, b, False{}, c)) == Nat.mod(Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)), Nat.pow(2n, n)) : Nat}
339
340def word_adc_wrap(n, a, b, c):
341 +n = n
342 +a = a
343 +b = b
344 +c = c
345 internal_fin_wrap(Word.to_nat(n, Word.adc(n, a, b, False{}, c)), Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)), Nat.pow(2n, n), internal_carry(n, a, b, c), internal_adc_core(n, a, b, c), word_to_nat_lt(n, Word.adc(n, a, b, False{}, c)))
346
347# Word addition is exact without overflow: a + b < 2^n implies to_nat (add a b) = a + b.
348law word_add_exact:
349 for n: Nat
350 for a: Word(n)
351 for b: Word(n)
352 for h: MNat.lt(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Nat.pow(2n, n))
353 {Word.to_nat(n, Word.add(n, a, b)) == Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}
354
355def word_add_exact(n, a, b, h):
356 +n = n
357 +a = a
358 +b = b
359 %MNat.add_zero(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b))) : {Word.to_nat(n, Word.add(n, a, b)) == _ : Nat}
360 word_adc_exact(n, a, b, False{}, internal_lt_congl(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), 0n), Nat.pow(2n, n), MNat.add_zero_sym(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b))), h))
361
362# Word addition wraps modulo 2^n: to_nat (add a b) = (a + b) % 2^n.
363law word_add_wrap:
364 for n: Nat
365 for a: Word(n)
366 for b: Word(n)
367 {Word.to_nat(n, Word.add(n, a, b)) == Nat.mod(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Nat.pow(2n, n)) : Nat}
368
369def word_add_wrap(n, a, b):
370 +n = n
371 +a = a
372 +b = b
373 %MNat.add_zero(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b))) : {Word.to_nat(n, Word.add(n, a, b)) == Nat.mod(_, Nat.pow(2n, n)) : Nat}
374 word_adc_wrap(n, a, b, False{})
375
376def internal_inc_carry(n: Nat, w: Word(n)) -> Bool:
377 match n:
378 case 0n:
379 True{}
380 case 1n+p:
381 match w:
382 case WCon{False{}, t}:
383 False{}
384 case WCon{True{}, t}:
385 internal_inc_carry(p, t)
386
387def internal_inc_core(n: Nat, w: Word(n)) -> {Nat.add(Word.to_nat(n, Word.inc(n, w)), Bool.pick(Nat, internal_inc_carry(n, w), Nat.pow(2n, n), 0n)) == 1n+Word.to_nat(n, w) : Nat}:
388 match n:
389 case 0n:
390 {==}
391 case 1n++p:
392 match w:
393 case WCon{False{}, t}:
394 MNat.add_zero(1n+Nat.double(Word.to_nat(p, t)))
395 case WCon{True{}, +t}:
396 -x = Word.to_nat(p, t)
397 %internal_pick_pow(internal_inc_carry(p, t), p) : {Nat.add(Nat.double(Word.to_nat(p, Word.inc(p, t))), _) == 2n+Nat.double(x) : Nat}
398 %MNat.double_add(Word.to_nat(p, Word.inc(p, t)), Bool.pick(Nat, internal_inc_carry(p, t), Nat.pow(2n, p), 0n)) : {_ == 2n+Nat.double(x) : Nat}
399 Equal.cong(Nat, Nat, z => Nat.double(z), Nat.add(Word.to_nat(p, Word.inc(p, t)), Bool.pick(Nat, internal_inc_carry(p, t), Nat.pow(2n, p), 0n)), 1n+Word.to_nat(p, t), internal_inc_core(p, t))
400
401# Increment is exact without overflow: 1 + w < 2^n implies to_nat (inc w) = 1 + w.
402law word_inc_exact:
403 for n: Nat
404 for w: Word(n)
405 for h: MNat.lt(1n+Word.to_nat(n, w), Nat.pow(2n, n))
406 {Word.to_nat(n, Word.inc(n, w)) == 1n+Word.to_nat(n, w) : Nat}
407
408def word_inc_exact(n, w, h):
409 +n = n
410 +w = w
411 internal_fin_exact(Word.to_nat(n, Word.inc(n, w)), 1n+Word.to_nat(n, w), Nat.pow(2n, n), internal_inc_carry(n, w), internal_inc_core(n, w), h)
412
413# Increment wraps modulo 2^n: to_nat (inc w) = (1 + w) % 2^n.
414law word_inc_wrap:
415 for n: Nat
416 for w: Word(n)
417 {Word.to_nat(n, Word.inc(n, w)) == Nat.mod(1n+Word.to_nat(n, w), Nat.pow(2n, n)) : Nat}
418
419def word_inc_wrap(n, w):
420 +n = n
421 +w = w
422 internal_fin_wrap(Word.to_nat(n, Word.inc(n, w)), 1n+Word.to_nat(n, w), Nat.pow(2n, n), internal_inc_carry(n, w), internal_inc_core(n, w), word_to_nat_lt(n, Word.inc(n, w)))
423
424def internal_adc_not(n: Nat, a: Word(n), b: Word(n), c: Bool) -> {Word.adc(n, a, b, True{}, c) == Word.adc(n, a, Word.not(n, b), False{}, c) : Word(n)}:
425 match n:
426 case 0n:
427 {==}
428 case 1n++p:
429 match a b:
430 case WCon{False{}, +at} WCon{+bb, +bt}:
431 +c = c
432 Equal.cong(Word(p), Word(1n+p), w => WCon{Bool.xor(Bool.not(bb), c), w}, Word.adc(p, at, bt, True{}, Bool.and(Bool.not(bb), c)), Word.adc(p, at, Word.not(p, bt), False{}, Bool.and(Bool.not(bb), c)), internal_adc_not(p, at, bt, Bool.and(Bool.not(bb), c)))
433 case WCon{True{}, +at} WCon{+bb, +bt}:
434 +c = c
435 Equal.cong(Word(p), Word(1n+p), w => WCon{Bool.not(Bool.xor(Bool.not(bb), c)), w}, Word.adc(p, at, bt, True{}, Bool.or(Bool.not(bb), c)), Word.adc(p, at, Word.not(p, bt), False{}, Bool.or(Bool.not(bb), c)), internal_adc_not(p, at, bt, Bool.or(Bool.not(bb), c)))
436
437def internal_sub_arith(+x: Nat, +y: Nat, +u: Nat, -m: Nat, h: MNat.le(y, x), c: {1n+Nat.add(u, y) == m : Nat}) -> {Nat.add(Nat.add(x, u), 1n) == Nat.add(Nat.sub(x, y), m) : Nat}:
438 -d = Nat.sub(x, y)
439 %c : {Nat.add(Nat.add(x, u), 1n) == Nat.add(d, _) : Nat}
440 %MNat.add_sub_of_le(y, x, h) : {Nat.add(Nat.add(_, u), 1n) == Nat.add(d, 1n+Nat.add(u, y)) : Nat}
441 -l = Nat.add(Nat.add(Nat.add(y, d), u), 1n)
442 %MNat.add_succ_sym(Nat.sub(x, y), Nat.add(u, y)) : {l == _ : Nat}
443 %MNat.add_comm(1n, Nat.add(Nat.add(y, Nat.sub(x, y)), u)) : {_ == 1n+Nat.add(d, Nat.add(u, y)) : Nat}
444 -l2 = Nat.add(1n, Nat.add(Nat.add(y, d), u))
445 %MNat.add_comm(y, u) : {l2 == 1n+Nat.add(d, _) : Nat}
446 %MNat.add_left_comm(y, Nat.sub(x, y), u) : {l2 == 1n+_ : Nat}
447 %MNat.add_assoc(y, Nat.sub(x, y), u) : {l2 == 1n+_ : Nat}
448 {==}
449
450# Word subtraction is exact without underflow: b <= a implies to_nat (sub a b) = a - b.
451law word_sub_exact:
452 for n: Nat
453 for a: Word(n)
454 for b: Word(n)
455 for h: MNat.le(Word.to_nat(n, b), Word.to_nat(n, a))
456 {Word.to_nat(n, Word.sub(n, a, b)) == Nat.sub(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}
457
458def word_sub_exact(n, a, b, h):
459 +n = n
460 +a = a
461 +b = b
462 -x = Word.to_nat(n, a)
463 -y = Word.to_nat(n, b)
464 -nb = Word.not(n, b)
465 -e = Word.to_nat(n, Word.adc(n, a, nb, False{}, True{}))
466 -s = Nat.add(Nat.add(x, Word.to_nat(n, nb)), 1n)
467 -m = Nat.pow(2n, n)
468 %Equal.sym(Word(n), Word.adc(n, a, b, True{}, True{}), Word.adc(n, a, Word.not(n, b), False{}, True{}), internal_adc_not(n, a, b, True{})) : {Word.to_nat(n, _) == Nat.sub(x, y) : Nat}
469 +ar = internal_sub_arith(Word.to_nat(n, a), Word.to_nat(n, b), Word.to_nat(n, Word.not(n, b)), Nat.pow(2n, n), h, word_not_add(n, b))
470 +le = internal_le_congr(Nat.pow(2n, n), Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, Word.not(n, b))), 1n), Nat.add(Nat.sub(Word.to_nat(n, a), Word.to_nat(n, b)), Nat.pow(2n, n)), Equal.sym(Nat, s, Nat.add(Nat.sub(x, y), m), ar), MNat.le_add_left(Nat.pow(2n, n), Nat.sub(Word.to_nat(n, a), Word.to_nat(n, b))))
471 +ov = internal_fin_over(Word.to_nat(n, Word.adc(n, a, Word.not(n, b), False{}, True{})), Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, Word.not(n, b))), 1n), Nat.pow(2n, n), internal_carry(n, a, Word.not(n, b), True{}), internal_adc_core(n, a, Word.not(n, b), True{}), word_to_nat_lt(n, Word.adc(n, a, Word.not(n, b), False{}, True{})), le)
472 MNat.add_right_cancel(Word.to_nat(n, Word.adc(n, a, Word.not(n, b), False{}, True{})), Nat.pow(2n, n), Nat.sub(Word.to_nat(n, a), Word.to_nat(n, b)), Equal.trans(Nat, Nat.add(e, m), s, Nat.add(Nat.sub(x, y), m), ov, ar))
473
474def internal_sub_wrap_arith(+x: Nat, +y: Nat, +u: Nat, -m: Nat, c: {1n+Nat.add(u, y) == m : Nat}) -> {Nat.add(Nat.add(x, u), 1n) == Nat.add(x, Nat.sub(m, y)) : Nat}:
475 %c : {Nat.add(Nat.add(x, u), 1n) == Nat.add(x, Nat.sub(_, y)) : Nat}
476 %MNat.add_sub_cancel_sym(1n+u, y) : {Nat.add(Nat.add(x, u), 1n) == Nat.add(x, _) : Nat}
477 %MNat.add_succ_sym(x, u) : {Nat.add(Nat.add(x, u), 1n) == _ : Nat}
478 MNat.add_comm(Nat.add(x, u), 1n)
479
480# Word subtraction wraps modulo 2^n: to_nat (sub a b) = (a + (2^n - b)) % 2^n.
481law word_sub_wrap:
482 for n: Nat
483 for a: Word(n)
484 for b: Word(n)
485 {Word.to_nat(n, Word.sub(n, a, b)) == Nat.mod(Nat.add(Word.to_nat(n, a), Nat.sub(Nat.pow(2n, n), Word.to_nat(n, b))), Nat.pow(2n, n)) : Nat}
486
487def word_sub_wrap(n, a, b):
488 +n = n
489 +a = a
490 +b = b
491 -x = Word.to_nat(n, a)
492 -y = Word.to_nat(n, b)
493 -u = Word.to_nat(n, Word.not(n, b))
494 -m = Nat.pow(2n, n)
495 %Equal.sym(Word(n), Word.adc(n, a, b, True{}, True{}), Word.adc(n, a, Word.not(n, b), False{}, True{}), internal_adc_not(n, a, b, True{})) : {Word.to_nat(n, _) == Nat.mod(Nat.add(x, Nat.sub(m, y)), m) : Nat}
496 %internal_sub_wrap_arith(Word.to_nat(n, a), Word.to_nat(n, b), Word.to_nat(n, Word.not(n, b)), Nat.pow(2n, n), word_not_add(n, b)) : {Word.to_nat(n, Word.adc(n, a, Word.not(n, b), False{}, True{})) == Nat.mod(_, m) : Nat}
497 word_adc_wrap(n, a, Word.not(n, b), True{})
498
499def internal_bound(-s: Nat, -m: Nat, e: {Nat.pow(2n, 32n) == m : Nat}, h: MNat.lt(s, m)) -> MNat.lt(s, Nat.pow(2n, 32n)):
500 %Equal.sym(Nat, Nat.pow(2n, 32n), m, e) : MNat.lt(s, _)
501 h
502
503def internal_u32_to_nat_lt(-m: Nat, a: U32, e: {Nat.pow(2n, 32n) == m : Nat}) -> MNat.lt(U32.to_nat(a), m):
504 match a:
505 case U32{w}:
506 %e : MNat.lt(Word.to_nat(32n, w), _)
507 word_to_nat_lt(32n, w)
508
509# A U32's value is below 2^32.
510law u32_to_nat_lt:
511 for a: U32
512 MNat.lt(U32.to_nat(a), Nat.pow(2n, 32n))
513
514def u32_to_nat_lt(a):
515 internal_u32_to_nat_lt(Nat.pow(2n, 32n), a, {==})
516
517# Distinct U32s have distinct values: to_nat a = to_nat b implies a = b.
518law u32_to_nat_inj:
519 for a: U32
520 for b: U32
521 for e: {U32.to_nat(a) == U32.to_nat(b) : Nat}
522 {a == b : U32}
523
524def u32_to_nat_inj(a, b, e):
525 match a b:
526 case U32{+x} U32{+y}:
527 Equal.cong(Word(32n), U32, w => U32{w}, x, y, word_to_nat_inj(32n, x, y, e))
528
529# Comparing U32s compares their values: cmp a b = cmp (to_nat a) (to_nat b).
530law u32_cmp_to_nat:
531 for a: U32
532 for b: U32
533 {U32.cmp(a, b) == Nat.cmp(U32.to_nat(a), U32.to_nat(b)) : Cmp}
534
535def u32_cmp_to_nat(a, b):
536 match a b:
537 case U32{x} U32{y}:
538 word_cmp_to_nat(32n, x, y)
539
540# U32 equality tests the values: is_eq a b = is_eq (to_nat a) (to_nat b).
541law u32_is_eq_to_nat:
542 for a: U32
543 for b: U32
544 {U32.is_eq(a, b) == Nat.is_eq(U32.to_nat(a), U32.to_nat(b)) : Bool}
545
546def u32_is_eq_to_nat(a, b):
547 +a = a
548 +b = b
549 Equal.cong(Cmp, Bool, k => Cmp.is_eq(k), U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), u32_cmp_to_nat(a, b))
550
551# U32 disequality tests the values: is_ne a b = is_ne (to_nat a) (to_nat b).
552law u32_is_ne_to_nat:
553 for a: U32
554 for b: U32
555 {U32.is_ne(a, b) == Nat.is_ne(U32.to_nat(a), U32.to_nat(b)) : Bool}
556
557def u32_is_ne_to_nat(a, b):
558 +a = a
559 +b = b
560 Equal.cong(Cmp, Bool, k => Bool.not(Cmp.is_eq(k)), U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), u32_cmp_to_nat(a, b))
561
562# The U32 strict order is the order of the values: is_lt a b = is_lt (to_nat a) (to_nat b).
563law u32_is_lt_to_nat:
564 for a: U32
565 for b: U32
566 {U32.is_lt(a, b) == Nat.is_lt(U32.to_nat(a), U32.to_nat(b)) : Bool}
567
568def u32_is_lt_to_nat(a, b):
569 +a = a
570 +b = b
571 Equal.cong(Cmp, Bool, k => Cmp.is_lt(k), U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), u32_cmp_to_nat(a, b))
572
573# The U32 order is the order of the values: is_le a b = is_le (to_nat a) (to_nat b).
574law u32_is_le_to_nat:
575 for a: U32
576 for b: U32
577 {U32.is_le(a, b) == Nat.is_le(U32.to_nat(a), U32.to_nat(b)) : Bool}
578
579def u32_is_le_to_nat(a, b):
580 +a = a
581 +b = b
582 Equal.cong(Cmp, Bool, k => Cmp.is_le(k), U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), u32_cmp_to_nat(a, b))
583
584# The reverse U32 strict order is that of the values: is_gt a b = is_gt (to_nat a) (to_nat b).
585law u32_is_gt_to_nat:
586 for a: U32
587 for b: U32
588 {U32.is_gt(a, b) == Nat.is_gt(U32.to_nat(a), U32.to_nat(b)) : Bool}
589
590def u32_is_gt_to_nat(a, b):
591 +a = a
592 +b = b
593 Equal.cong(Cmp, Bool, k => Cmp.is_gt(k), U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), u32_cmp_to_nat(a, b))
594
595# The reverse U32 order is that of the values: is_ge a b = is_ge (to_nat a) (to_nat b).
596law u32_is_ge_to_nat:
597 for a: U32
598 for b: U32
599 {U32.is_ge(a, b) == Nat.is_ge(U32.to_nat(a), U32.to_nat(b)) : Bool}
600
601def u32_is_ge_to_nat(a, b):
602 +a = a
603 +b = b
604 Equal.cong(Cmp, Bool, k => Cmp.is_ge(k), U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), u32_cmp_to_nat(a, b))
605
606def internal_u32_add_exact(-m: Nat, a: U32, b: U32, e: {Nat.pow(2n, 32n) == m : Nat}, h: MNat.lt(Nat.add(U32.to_nat(a), U32.to_nat(b)), m)) -> {U32.to_nat(U32.add(a, b)) == Nat.add(U32.to_nat(a), U32.to_nat(b)) : Nat}:
607 match a b:
608 case U32{+x} U32{+y}:
609 word_add_exact(32n, x, y, internal_bound(Nat.add(Word.to_nat(32n, x), Word.to_nat(32n, y)), m, e, h))
610
611# U32 addition is exact without overflow: a + b < 2^32 implies to_nat (a + b) = a + b.
612law u32_add_exact:
613 for a: U32
614 for b: U32
615 for h: MNat.lt(Nat.add(U32.to_nat(a), U32.to_nat(b)), Nat.pow(2n, 32n))
616 {U32.to_nat(U32.add(a, b)) == Nat.add(U32.to_nat(a), U32.to_nat(b)) : Nat}
617
618def u32_add_exact(a, b, h):
619 internal_u32_add_exact(Nat.pow(2n, 32n), a, b, {==}, h)
620
621def internal_u32_add_wrap(-m: Nat, a: U32, b: U32, e: {Nat.pow(2n, 32n) == m : Nat}) -> {U32.to_nat(U32.add(a, b)) == Nat.mod(Nat.add(U32.to_nat(a), U32.to_nat(b)), m) : Nat}:
622 match a b:
623 case U32{+x} U32{+y}:
624 %e : {Word.to_nat(32n, Word.add(32n, x, y)) == Nat.mod(Nat.add(Word.to_nat(32n, x), Word.to_nat(32n, y)), _) : Nat}
625 word_add_wrap(32n, x, y)
626
627# U32 addition wraps modulo 2^32: to_nat (a + b) = (a + b) % 2^32.
628law u32_add_wrap:
629 for a: U32
630 for b: U32
631 {U32.to_nat(U32.add(a, b)) == Nat.mod(Nat.add(U32.to_nat(a), U32.to_nat(b)), Nat.pow(2n, 32n)) : Nat}
632
633def u32_add_wrap(a, b):
634 internal_u32_add_wrap(Nat.pow(2n, 32n), a, b, {==})
635
636# U32 subtraction is exact without underflow: b <= a implies to_nat (a - b) = a - b.
637law u32_sub_exact:
638 for a: U32
639 for b: U32
640 for h: MNat.le(U32.to_nat(b), U32.to_nat(a))
641 {U32.to_nat(U32.sub(a, b)) == Nat.sub(U32.to_nat(a), U32.to_nat(b)) : Nat}
642
643def u32_sub_exact(a, b, h):
644 match a b:
645 case U32{x} U32{y}:
646 word_sub_exact(32n, x, y, h)
647
648def internal_u32_sub_wrap(-m: Nat, a: U32, b: U32, e: {Nat.pow(2n, 32n) == m : Nat}) -> {U32.to_nat(U32.sub(a, b)) == Nat.mod(Nat.add(U32.to_nat(a), Nat.sub(m, U32.to_nat(b))), m) : Nat}:
649 match a b:
650 case U32{+x} U32{+y}:
651 %e : {Word.to_nat(32n, Word.sub(32n, x, y)) == Nat.mod(Nat.add(Word.to_nat(32n, x), Nat.sub(_, Word.to_nat(32n, y))), _) : Nat}
652 word_sub_wrap(32n, x, y)
653
654# U32 subtraction wraps modulo 2^32: to_nat (a - b) = (a + (2^32 - b)) % 2^32.
655law u32_sub_wrap:
656 for a: U32
657 for b: U32
658 {U32.to_nat(U32.sub(a, b)) == Nat.mod(Nat.add(U32.to_nat(a), Nat.sub(Nat.pow(2n, 32n), U32.to_nat(b))), Nat.pow(2n, 32n)) : Nat}
659
660def u32_sub_wrap(a, b):
661 internal_u32_sub_wrap(Nat.pow(2n, 32n), a, b, {==})
662
663def internal_u32_inc_exact(-m: Nat, a: U32, e: {Nat.pow(2n, 32n) == m : Nat}, h: MNat.lt(1n+U32.to_nat(a), m)) -> {U32.to_nat(U32.inc(a)) == 1n+U32.to_nat(a) : Nat}:
664 match a:
665 case U32{+w}:
666 word_inc_exact(32n, w, internal_bound(1n+Word.to_nat(32n, w), m, e, h))
667
668# U32 increment is exact without overflow: 1 + a < 2^32 implies to_nat (inc a) = 1 + a.
669law u32_inc_exact:
670 for a: U32
671 for h: MNat.lt(1n+U32.to_nat(a), Nat.pow(2n, 32n))
672 {U32.to_nat(U32.inc(a)) == 1n+U32.to_nat(a) : Nat}
673
674def u32_inc_exact(a, h):
675 internal_u32_inc_exact(Nat.pow(2n, 32n), a, {==}, h)
676
677def internal_u32_inc_wrap(-m: Nat, a: U32, e: {Nat.pow(2n, 32n) == m : Nat}) -> {U32.to_nat(U32.inc(a)) == Nat.mod(1n+U32.to_nat(a), m) : Nat}:
678 match a:
679 case U32{+w}:
680 %e : {Word.to_nat(32n, Word.inc(32n, w)) == Nat.mod(1n+Word.to_nat(32n, w), _) : Nat}
681 word_inc_wrap(32n, w)
682
683# U32 increment wraps modulo 2^32: to_nat (inc a) = (1 + a) % 2^32.
684law u32_inc_wrap:
685 for a: U32
686 {U32.to_nat(U32.inc(a)) == Nat.mod(1n+U32.to_nat(a), Nat.pow(2n, 32n)) : Nat}
687
688def u32_inc_wrap(a):
689 internal_u32_inc_wrap(Nat.pow(2n, 32n), a, {==})
690
691def internal_u32_to_nat_from_nat(+m: Nat, +e: {Nat.pow(2n, 32n) == m : Nat}, k: Nat, h: MNat.lt(k, m)) -> {U32.to_nat(U32.from_nat(k)) == k : Nat}:
692 match k:
693 case 0n:
694 {==}
695 case 1n++p:
696 +h = h
697 +ih = internal_u32_to_nat_from_nat(m, e, p, MNat.lt_trans(p, 1n+p, m, MNat.lt_succ_self(p), h))
698 +hu = internal_lt_congl(1n+p, 1n+U32.to_nat(U32.from_nat(p)), m, Equal.cong(Nat, Nat, z => 1n+z, p, U32.to_nat(U32.from_nat(p)), Equal.sym(Nat, U32.to_nat(U32.from_nat(p)), p, ih)), h)
699 Equal.trans(Nat, U32.to_nat(U32.inc(U32.from_nat(p))), 1n+U32.to_nat(U32.from_nat(p)), 1n+p, internal_u32_inc_exact(m, U32.from_nat(p), e, hu), Equal.cong(Nat, Nat, z => 1n+z, U32.to_nat(U32.from_nat(p)), p, ih))
700
701# Converting a natural below 2^32 to U32 and back is the identity: k < 2^32 implies to_nat (from_nat k) = k.
702law u32_to_nat_from_nat:
703 for k: Nat
704 for h: MNat.lt(k, Nat.pow(2n, 32n))
705 {U32.to_nat(U32.from_nat(k)) == k : Nat}
706
707def u32_to_nat_from_nat(k, h):
708 internal_u32_to_nat_from_nat(Nat.pow(2n, 32n), {==}, k, h)
709
710# Converting a U32 to a natural and back is the identity: from_nat (to_nat a) = a.
711law u32_from_nat_to_nat:
712 for a: U32
713 {U32.from_nat(U32.to_nat(a)) == a : U32}
714
715def u32_from_nat_to_nat(a):
716 +a = a
717 u32_to_nat_inj(U32.from_nat(U32.to_nat(a)), a, u32_to_nat_from_nat(U32.to_nat(a), u32_to_nat_lt(a)))
718
719def internal_mod_succ_mod(+p: Nat, +m: Nat) -> {Nat.mod(1n+Nat.mod(p, m), m) == Nat.mod(1n+p, m) : Nat}:
720 %MNat.mod_add_div(p, m) : {Nat.mod(1n+Nat.mod(p, m), m) == Nat.mod(1n+_, m) : Nat}
721 Equal.sym(Nat, Nat.mod(Nat.add(1n+Nat.mod(p, m), Nat.mul(m, Nat.div(p, m))), m), Nat.mod(1n+Nat.mod(p, m), m), MNat.add_mul_mod_self_left(1n+Nat.mod(p, m), m, Nat.div(p, m)))
722
723def internal_u32_to_nat_from_nat_mod(+m: Nat, +e: {Nat.pow(2n, 32n) == m : Nat}, k: Nat) -> {U32.to_nat(U32.from_nat(k)) == Nat.mod(k, m) : Nat}:
724 match k:
725 case 0n:
726 Equal.sym(Nat, Nat.mod(0n, m), 0n, MNat.zero_mod(m))
727 case 1n++p:
728 -u = U32.from_nat(p)
729 Equal.trans(Nat, U32.to_nat(U32.inc(u)), Nat.mod(1n+U32.to_nat(u), m), Nat.mod(1n+p, m), internal_u32_inc_wrap(m, U32.from_nat(p), e), Equal.trans(Nat, Nat.mod(1n+U32.to_nat(u), m), Nat.mod(1n+Nat.mod(p, m), m), Nat.mod(1n+p, m), Equal.cong(Nat, Nat, z => Nat.mod(1n+z, m), U32.to_nat(u), Nat.mod(p, m), internal_u32_to_nat_from_nat_mod(m, e, p)), internal_mod_succ_mod(p, m)))
730
731# Converting any natural to U32 and back reduces it modulo 2^32: to_nat (from_nat k) = k % 2^32.
732law u32_to_nat_from_nat_mod:
733 for k: Nat
734 {U32.to_nat(U32.from_nat(k)) == Nat.mod(k, Nat.pow(2n, 32n)) : Nat}
735
736def u32_to_nat_from_nat_mod(k):
737 internal_u32_to_nat_from_nat_mod(Nat.pow(2n, 32n), {==}, k)
738
739def internal_min_fin(+u: U32, +v: U32, c: Bool, e: {Nat.is_lt(U32.to_nat(u), U32.to_nat(v)) == c : Bool}) -> {U32.to_nat(Bool.pick(U32, c, u, v)) == Nat.min(U32.to_nat(u), U32.to_nat(v)) : Nat}:
740 match c:
741 case True{}:
742 Equal.sym(Nat, Nat.min(U32.to_nat(u), U32.to_nat(v)), U32.to_nat(u), MNat.min_eq_left(U32.to_nat(u), U32.to_nat(v), MNat.le_of_lt(U32.to_nat(u), U32.to_nat(v), e)))
743 case False{}:
744 Equal.sym(Nat, Nat.min(U32.to_nat(u), U32.to_nat(v)), U32.to_nat(v), MNat.min_eq_right(U32.to_nat(u), U32.to_nat(v), MNat.le_of_not_lt(U32.to_nat(u), U32.to_nat(v), e)))
745
746# The U32 minimum is the minimum of the values: to_nat (min a b) = min (to_nat a) (to_nat b).
747law u32_min_to_nat:
748 for a: U32
749 for b: U32
750 {U32.to_nat(U32.min(a, b)) == Nat.min(U32.to_nat(a), U32.to_nat(b)) : Nat}
751
752def u32_min_to_nat(a, b):
753 match a b:
754 case U32{+x} U32{+y}:
755 internal_min_fin(U32{x}, U32{y}, U32.is_lt(U32{x}, U32{y}), Equal.sym(Bool, U32.is_lt(U32{x}, U32{y}), Nat.is_lt(U32.to_nat(U32{x}), U32.to_nat(U32{y})), u32_is_lt_to_nat(U32{x}, U32{y})))
756
757def internal_max_fin(+u: U32, +v: U32, c: Bool, e: {Nat.is_lt(U32.to_nat(u), U32.to_nat(v)) == c : Bool}) -> {U32.to_nat(Bool.pick(U32, c, v, u)) == Nat.max(U32.to_nat(u), U32.to_nat(v)) : Nat}:
758 match c:
759 case True{}:
760 Equal.sym(Nat, Nat.max(U32.to_nat(u), U32.to_nat(v)), U32.to_nat(v), MNat.max_eq_right(U32.to_nat(u), U32.to_nat(v), MNat.le_of_lt(U32.to_nat(u), U32.to_nat(v), e)))
761 case False{}:
762 Equal.sym(Nat, Nat.max(U32.to_nat(u), U32.to_nat(v)), U32.to_nat(u), MNat.max_eq_left(U32.to_nat(u), U32.to_nat(v), MNat.le_of_not_lt(U32.to_nat(u), U32.to_nat(v), e)))
763
764# The U32 maximum is the maximum of the values: to_nat (max a b) = max (to_nat a) (to_nat b).
765law u32_max_to_nat:
766 for a: U32
767 for b: U32
768 {U32.to_nat(U32.max(a, b)) == Nat.max(U32.to_nat(a), U32.to_nat(b)) : Nat}
769
770def u32_max_to_nat(a, b):
771 match a b:
772 case U32{+x} U32{+y}:
773 internal_max_fin(U32{x}, U32{y}, U32.is_lt(U32{x}, U32{y}), Equal.sym(Bool, U32.is_lt(U32{x}, U32{y}), Nat.is_lt(U32.to_nat(U32{x}), U32.to_nat(U32{y})), u32_is_lt_to_nat(U32{x}, U32{y})))
774
775# --- generated: _sym twins (tools/mathlib/twins.ts), do not edit ---
776
777# The zero word is the natural zero: to_nat (zero n) = 0, reversed to rewrite toward the simple side.
778law word_to_nat_zero_sym:
779 for n: Nat
780 {0n == Word.to_nat(n, Word.zero(n)) : Nat}
781
782def word_to_nat_zero_sym(n):
783 Equal.sym(Nat, Word.to_nat(n, Word.zero(n)), 0n, word_to_nat_zero(n))
784
785# Comparing words compares their values: cmp a b = cmp (to_nat a) (to_nat b), reversed to rewrite toward the simple side.
786law word_cmp_to_nat_sym:
787 for n: Nat
788 for a: Word(n)
789 for b: Word(n)
790 {Nat.cmp(Word.to_nat(n, a), Word.to_nat(n, b)) == Word.cmp(n, a, b) : Cmp}
791
792def word_cmp_to_nat_sym(n, a, b):
793 Equal.sym(Cmp, Word.cmp(n, a, b), Nat.cmp(Word.to_nat(n, a), Word.to_nat(n, b)), word_cmp_to_nat(n, a, b))
794
795# One plus a word plus its complement is two to the width: 1 + to_nat (not w) + to_nat w = 2^n, reversed to rewrite toward the simple side.
796law word_not_add_sym:
797 for n: Nat
798 for w: Word(n)
799 {Nat.pow(2n, n) == 1n+Nat.add(Word.to_nat(n, Word.not(n, w)), Word.to_nat(n, w)) : Nat}
800
801def word_not_add_sym(n, w):
802 Equal.sym(Nat, 1n+Nat.add(Word.to_nat(n, Word.not(n, w)), Word.to_nat(n, w)), Nat.pow(2n, n), word_not_add(n, w))
803
804# The adder is exact below the overflow: a + b + carry-in < 2^n implies to_nat (adc a b False c) = a + b + carry-in, reversed to rewrite toward the simple side.
805law word_adc_exact_sym:
806 for n: Nat
807 for a: Word(n)
808 for b: Word(n)
809 for c: Bool
810 for h: MNat.lt(Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)), Nat.pow(2n, n))
811 {Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)) == Word.to_nat(n, Word.adc(n, a, b, False{}, c)) : Nat}
812
813def word_adc_exact_sym(n, a, b, c, h):
814 Equal.sym(Nat, Word.to_nat(n, Word.adc(n, a, b, False{}, c)), Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)), word_adc_exact(n, a, b, c, h))
815
816# The adder drops exactly one 2^n on overflow: 2^n <= a + b + carry-in implies to_nat (adc a b False c) + 2^n = a + b + carry-in, reversed to rewrite toward the simple side.
817law word_adc_overflow_sym:
818 for n: Nat
819 for a: Word(n)
820 for b: Word(n)
821 for c: Bool
822 for h: MNat.le(Nat.pow(2n, n), Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)))
823 {Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)) == Nat.add(Word.to_nat(n, Word.adc(n, a, b, False{}, c)), Nat.pow(2n, n)) : Nat}
824
825def word_adc_overflow_sym(n, a, b, c, h):
826 Equal.sym(Nat, Nat.add(Word.to_nat(n, Word.adc(n, a, b, False{}, c)), Nat.pow(2n, n)), Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)), word_adc_overflow(n, a, b, c, h))
827
828# The adder wraps modulo 2^n: to_nat (adc a b False c) = (a + b + carry-in) % 2^n, reversed to rewrite toward the simple side.
829law word_adc_wrap_sym:
830 for n: Nat
831 for a: Word(n)
832 for b: Word(n)
833 for c: Bool
834 {Nat.mod(Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)), Nat.pow(2n, n)) == Word.to_nat(n, Word.adc(n, a, b, False{}, c)) : Nat}
835
836def word_adc_wrap_sym(n, a, b, c):
837 Equal.sym(Nat, Word.to_nat(n, Word.adc(n, a, b, False{}, c)), Nat.mod(Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)), Nat.pow(2n, n)), word_adc_wrap(n, a, b, c))
838
839# Word addition is exact without overflow: a + b < 2^n implies to_nat (add a b) = a + b, reversed to rewrite toward the simple side.
840law word_add_exact_sym:
841 for n: Nat
842 for a: Word(n)
843 for b: Word(n)
844 for h: MNat.lt(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Nat.pow(2n, n))
845 {Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)) == Word.to_nat(n, Word.add(n, a, b)) : Nat}
846
847def word_add_exact_sym(n, a, b, h):
848 Equal.sym(Nat, Word.to_nat(n, Word.add(n, a, b)), Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), word_add_exact(n, a, b, h))
849
850# Word addition wraps modulo 2^n: to_nat (add a b) = (a + b) % 2^n, reversed to rewrite toward the simple side.
851law word_add_wrap_sym:
852 for n: Nat
853 for a: Word(n)
854 for b: Word(n)
855 {Nat.mod(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Nat.pow(2n, n)) == Word.to_nat(n, Word.add(n, a, b)) : Nat}
856
857def word_add_wrap_sym(n, a, b):
858 Equal.sym(Nat, Word.to_nat(n, Word.add(n, a, b)), Nat.mod(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Nat.pow(2n, n)), word_add_wrap(n, a, b))
859
860# Increment is exact without overflow: 1 + w < 2^n implies to_nat (inc w) = 1 + w, reversed to rewrite toward the simple side.
861law word_inc_exact_sym:
862 for n: Nat
863 for w: Word(n)
864 for h: MNat.lt(1n+Word.to_nat(n, w), Nat.pow(2n, n))
865 {1n+Word.to_nat(n, w) == Word.to_nat(n, Word.inc(n, w)) : Nat}
866
867def word_inc_exact_sym(n, w, h):
868 Equal.sym(Nat, Word.to_nat(n, Word.inc(n, w)), 1n+Word.to_nat(n, w), word_inc_exact(n, w, h))
869
870# Increment wraps modulo 2^n: to_nat (inc w) = (1 + w) % 2^n, reversed to rewrite toward the simple side.
871law word_inc_wrap_sym:
872 for n: Nat
873 for w: Word(n)
874 {Nat.mod(1n+Word.to_nat(n, w), Nat.pow(2n, n)) == Word.to_nat(n, Word.inc(n, w)) : Nat}
875
876def word_inc_wrap_sym(n, w):
877 Equal.sym(Nat, Word.to_nat(n, Word.inc(n, w)), Nat.mod(1n+Word.to_nat(n, w), Nat.pow(2n, n)), word_inc_wrap(n, w))
878
879# Word subtraction is exact without underflow: b <= a implies to_nat (sub a b) = a - b, reversed to rewrite toward the simple side.
880law word_sub_exact_sym:
881 for n: Nat
882 for a: Word(n)
883 for b: Word(n)
884 for h: MNat.le(Word.to_nat(n, b), Word.to_nat(n, a))
885 {Nat.sub(Word.to_nat(n, a), Word.to_nat(n, b)) == Word.to_nat(n, Word.sub(n, a, b)) : Nat}
886
887def word_sub_exact_sym(n, a, b, h):
888 Equal.sym(Nat, Word.to_nat(n, Word.sub(n, a, b)), Nat.sub(Word.to_nat(n, a), Word.to_nat(n, b)), word_sub_exact(n, a, b, h))
889
890# Word subtraction wraps modulo 2^n: to_nat (sub a b) = (a + (2^n - b)) % 2^n, reversed to rewrite toward the simple side.
891law word_sub_wrap_sym:
892 for n: Nat
893 for a: Word(n)
894 for b: Word(n)
895 {Nat.mod(Nat.add(Word.to_nat(n, a), Nat.sub(Nat.pow(2n, n), Word.to_nat(n, b))), Nat.pow(2n, n)) == Word.to_nat(n, Word.sub(n, a, b)) : Nat}
896
897def word_sub_wrap_sym(n, a, b):
898 Equal.sym(Nat, Word.to_nat(n, Word.sub(n, a, b)), Nat.mod(Nat.add(Word.to_nat(n, a), Nat.sub(Nat.pow(2n, n), Word.to_nat(n, b))), Nat.pow(2n, n)), word_sub_wrap(n, a, b))
899
900# Comparing U32s compares their values: cmp a b = cmp (to_nat a) (to_nat b), reversed to rewrite toward the simple side.
901law u32_cmp_to_nat_sym:
902 for a: U32
903 for b: U32
904 {Nat.cmp(U32.to_nat(a), U32.to_nat(b)) == U32.cmp(a, b) : Cmp}
905
906def u32_cmp_to_nat_sym(a, b):
907 Equal.sym(Cmp, U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), u32_cmp_to_nat(a, b))
908
909# U32 equality tests the values: is_eq a b = is_eq (to_nat a) (to_nat b), reversed to rewrite toward the simple side.
910law u32_is_eq_to_nat_sym:
911 for a: U32
912 for b: U32
913 {Nat.is_eq(U32.to_nat(a), U32.to_nat(b)) == U32.is_eq(a, b) : Bool}
914
915def u32_is_eq_to_nat_sym(a, b):
916 Equal.sym(Bool, U32.is_eq(a, b), Nat.is_eq(U32.to_nat(a), U32.to_nat(b)), u32_is_eq_to_nat(a, b))
917
918# U32 disequality tests the values: is_ne a b = is_ne (to_nat a) (to_nat b), reversed to rewrite toward the simple side.
919law u32_is_ne_to_nat_sym:
920 for a: U32
921 for b: U32
922 {Nat.is_ne(U32.to_nat(a), U32.to_nat(b)) == U32.is_ne(a, b) : Bool}
923
924def u32_is_ne_to_nat_sym(a, b):
925 Equal.sym(Bool, U32.is_ne(a, b), Nat.is_ne(U32.to_nat(a), U32.to_nat(b)), u32_is_ne_to_nat(a, b))
926
927# The U32 strict order is the order of the values: is_lt a b = is_lt (to_nat a) (to_nat b), reversed to rewrite toward the simple side.
928law u32_is_lt_to_nat_sym:
929 for a: U32
930 for b: U32
931 {Nat.is_lt(U32.to_nat(a), U32.to_nat(b)) == U32.is_lt(a, b) : Bool}
932
933def u32_is_lt_to_nat_sym(a, b):
934 Equal.sym(Bool, U32.is_lt(a, b), Nat.is_lt(U32.to_nat(a), U32.to_nat(b)), u32_is_lt_to_nat(a, b))
935
936# The U32 order is the order of the values: is_le a b = is_le (to_nat a) (to_nat b), reversed to rewrite toward the simple side.
937law u32_is_le_to_nat_sym:
938 for a: U32
939 for b: U32
940 {Nat.is_le(U32.to_nat(a), U32.to_nat(b)) == U32.is_le(a, b) : Bool}
941
942def u32_is_le_to_nat_sym(a, b):
943 Equal.sym(Bool, U32.is_le(a, b), Nat.is_le(U32.to_nat(a), U32.to_nat(b)), u32_is_le_to_nat(a, b))
944
945# The reverse U32 strict order is that of the values: is_gt a b = is_gt (to_nat a) (to_nat b), reversed to rewrite toward the simple side.
946law u32_is_gt_to_nat_sym:
947 for a: U32
948 for b: U32
949 {Nat.is_gt(U32.to_nat(a), U32.to_nat(b)) == U32.is_gt(a, b) : Bool}
950
951def u32_is_gt_to_nat_sym(a, b):
952 Equal.sym(Bool, U32.is_gt(a, b), Nat.is_gt(U32.to_nat(a), U32.to_nat(b)), u32_is_gt_to_nat(a, b))
953
954# The reverse U32 order is that of the values: is_ge a b = is_ge (to_nat a) (to_nat b), reversed to rewrite toward the simple side.
955law u32_is_ge_to_nat_sym:
956 for a: U32
957 for b: U32
958 {Nat.is_ge(U32.to_nat(a), U32.to_nat(b)) == U32.is_ge(a, b) : Bool}
959
960def u32_is_ge_to_nat_sym(a, b):
961 Equal.sym(Bool, U32.is_ge(a, b), Nat.is_ge(U32.to_nat(a), U32.to_nat(b)), u32_is_ge_to_nat(a, b))
962
963# U32 addition is exact without overflow: a + b < 2^32 implies to_nat (a + b) = a + b, reversed to rewrite toward the simple side.
964law u32_add_exact_sym:
965 for a: U32
966 for b: U32
967 for h: MNat.lt(Nat.add(U32.to_nat(a), U32.to_nat(b)), Nat.pow(2n, 32n))
968 {Nat.add(U32.to_nat(a), U32.to_nat(b)) == U32.to_nat(U32.add(a, b)) : Nat}
969
970def u32_add_exact_sym(a, b, h):
971 Equal.sym(Nat, U32.to_nat(U32.add(a, b)), Nat.add(U32.to_nat(a), U32.to_nat(b)), u32_add_exact(a, b, h))
972
973# U32 addition wraps modulo 2^32: to_nat (a + b) = (a + b) % 2^32, reversed to rewrite toward the simple side.
974law u32_add_wrap_sym:
975 for a: U32
976 for b: U32
977 {Nat.mod(Nat.add(U32.to_nat(a), U32.to_nat(b)), Nat.pow(2n, 32n)) == U32.to_nat(U32.add(a, b)) : Nat}
978
979def u32_add_wrap_sym(a, b):
980 Equal.sym(Nat, U32.to_nat(U32.add(a, b)), Nat.mod(Nat.add(U32.to_nat(a), U32.to_nat(b)), Nat.pow(2n, 32n)), u32_add_wrap(a, b))
981
982# U32 subtraction is exact without underflow: b <= a implies to_nat (a - b) = a - b, reversed to rewrite toward the simple side.
983law u32_sub_exact_sym:
984 for a: U32
985 for b: U32
986 for h: MNat.le(U32.to_nat(b), U32.to_nat(a))
987 {Nat.sub(U32.to_nat(a), U32.to_nat(b)) == U32.to_nat(U32.sub(a, b)) : Nat}
988
989def u32_sub_exact_sym(a, b, h):
990 Equal.sym(Nat, U32.to_nat(U32.sub(a, b)), Nat.sub(U32.to_nat(a), U32.to_nat(b)), u32_sub_exact(a, b, h))
991
992# U32 subtraction wraps modulo 2^32: to_nat (a - b) = (a + (2^32 - b)) % 2^32, reversed to rewrite toward the simple side.
993law u32_sub_wrap_sym:
994 for a: U32
995 for b: U32
996 {Nat.mod(Nat.add(U32.to_nat(a), Nat.sub(Nat.pow(2n, 32n), U32.to_nat(b))), Nat.pow(2n, 32n)) == U32.to_nat(U32.sub(a, b)) : Nat}
997
998def u32_sub_wrap_sym(a, b):
999 Equal.sym(Nat, U32.to_nat(U32.sub(a, b)), Nat.mod(Nat.add(U32.to_nat(a), Nat.sub(Nat.pow(2n, 32n), U32.to_nat(b))), Nat.pow(2n, 32n)), u32_sub_wrap(a, b))
1000
1001# U32 increment is exact without overflow: 1 + a < 2^32 implies to_nat (inc a) = 1 + a, reversed to rewrite toward the simple side.
1002law u32_inc_exact_sym:
1003 for a: U32
1004 for h: MNat.lt(1n+U32.to_nat(a), Nat.pow(2n, 32n))
1005 {1n+U32.to_nat(a) == U32.to_nat(U32.inc(a)) : Nat}
1006
1007def u32_inc_exact_sym(a, h):
1008 Equal.sym(Nat, U32.to_nat(U32.inc(a)), 1n+U32.to_nat(a), u32_inc_exact(a, h))
1009
1010# U32 increment wraps modulo 2^32: to_nat (inc a) = (1 + a) % 2^32, reversed to rewrite toward the simple side.
1011law u32_inc_wrap_sym:
1012 for a: U32
1013 {Nat.mod(1n+U32.to_nat(a), Nat.pow(2n, 32n)) == U32.to_nat(U32.inc(a)) : Nat}
1014
1015def u32_inc_wrap_sym(a):
1016 Equal.sym(Nat, U32.to_nat(U32.inc(a)), Nat.mod(1n+U32.to_nat(a), Nat.pow(2n, 32n)), u32_inc_wrap(a))
1017
1018# Converting a natural below 2^32 to U32 and back is the identity: k < 2^32 implies to_nat (from_nat k) = k, reversed to rewrite toward the simple side.
1019law u32_to_nat_from_nat_sym:
1020 for k: Nat
1021 for h: MNat.lt(k, Nat.pow(2n, 32n))
1022 {k == U32.to_nat(U32.from_nat(k)) : Nat}
1023
1024def u32_to_nat_from_nat_sym(k, h):
1025 Equal.sym(Nat, U32.to_nat(U32.from_nat(k)), k, u32_to_nat_from_nat(k, h))
1026
1027# Converting a U32 to a natural and back is the identity: from_nat (to_nat a) = a, reversed to rewrite toward the simple side.
1028law u32_from_nat_to_nat_sym:
1029 for a: U32
1030 {a == U32.from_nat(U32.to_nat(a)) : U32}
1031
1032def u32_from_nat_to_nat_sym(a):
1033 Equal.sym(U32, U32.from_nat(U32.to_nat(a)), a, u32_from_nat_to_nat(a))
1034
1035# Converting any natural to U32 and back reduces it modulo 2^32: to_nat (from_nat k) = k % 2^32, reversed to rewrite toward the simple side.
1036law u32_to_nat_from_nat_mod_sym:
1037 for k: Nat
1038 {Nat.mod(k, Nat.pow(2n, 32n)) == U32.to_nat(U32.from_nat(k)) : Nat}
1039
1040def u32_to_nat_from_nat_mod_sym(k):
1041 Equal.sym(Nat, U32.to_nat(U32.from_nat(k)), Nat.mod(k, Nat.pow(2n, 32n)), u32_to_nat_from_nat_mod(k))
1042
1043# The U32 minimum is the minimum of the values: to_nat (min a b) = min (to_nat a) (to_nat b), reversed to rewrite toward the simple side.
1044law u32_min_to_nat_sym:
1045 for a: U32
1046 for b: U32
1047 {Nat.min(U32.to_nat(a), U32.to_nat(b)) == U32.to_nat(U32.min(a, b)) : Nat}
1048
1049def u32_min_to_nat_sym(a, b):
1050 Equal.sym(Nat, U32.to_nat(U32.min(a, b)), Nat.min(U32.to_nat(a), U32.to_nat(b)), u32_min_to_nat(a, b))
1051
1052# The U32 maximum is the maximum of the values: to_nat (max a b) = max (to_nat a) (to_nat b), reversed to rewrite toward the simple side.
1053law u32_max_to_nat_sym:
1054 for a: U32
1055 for b: U32
1056 {Nat.max(U32.to_nat(a), U32.to_nat(b)) == U32.to_nat(U32.max(a, b)) : Nat}
1057
1058def u32_max_to_nat_sym(a, b):
1059 Equal.sym(Nat, U32.to_nat(U32.max(a, b)), Nat.max(U32.to_nat(a), U32.to_nat(b)), u32_max_to_nat(a, b))