lemmas.bend
bend-kit-lemmas@0.1.0.0 · 746 lines · 0 definitions
1# Proved laws that relate Word and U32 arithmetic to Nat. Source: https://github.com/paymog/bend-kit/tree/main/lemmas
2import Base
3import bend-mathlib@0.7.2.0/nat.bend as MNat
4
5# 2^n, by the doubling that Word.to_nat uses.
6def pow2(n: Nat) -> Nat:
7 match n:
8 case 0n:
9 1n
10 case 1n+p:
11 Nat.double(pow2(p))
12
13# The value of a word whose low bit is x and whose upper bits have value t.
14def bit(x: Bool, t: Nat) -> Nat:
15 match x:
16 case False{}:
17 Nat.double(t)
18 case True{}:
19 1n+Nat.double(t)
20
21law to_nat_con:
22 for -p: Nat
23 for x: Bool
24 for -t: Word(p)
25 {bit(x, Word.to_nat(p, t)) == Word.to_nat(1n+p, WCon{x, t}) : Nat}
26
27def to_nat_con(p, x, t):
28 match x:
29 case False{}:
30 {==}
31 case True{}:
32 {==}
33
34law cmp_bit:
35 for a: Nat
36 for b: Nat
37 for x: Bool
38 for y: Bool
39 {Word.cmp.fin(x, y, Nat.cmp(a, b)) == Nat.cmp(bit(x, a), bit(y, b)) : Cmp}
40
41def cmp_bit(a, b, x, y):
42 match a b:
43 case 0n 0n:
44 match x y:
45 case False{} False{}:
46 {==}
47 case False{} True{}:
48 {==}
49 case True{} False{}:
50 {==}
51 case True{} True{}:
52 {==}
53 case 0n 1n+q:
54 match x y:
55 case False{} False{}:
56 {==}
57 case False{} True{}:
58 {==}
59 case True{} False{}:
60 {==}
61 case True{} True{}:
62 {==}
63 case 1n+p 0n:
64 match x y:
65 case False{} False{}:
66 {==}
67 case False{} True{}:
68 {==}
69 case True{} False{}:
70 {==}
71 case True{} True{}:
72 {==}
73 case 1n+p 1n+q:
74 match x y:
75 case False{} False{}:
76 cmp_bit(p, q, False{}, False{})
77 case False{} True{}:
78 cmp_bit(p, q, False{}, True{})
79 case True{} False{}:
80 cmp_bit(p, q, True{}, False{})
81 case True{} True{}:
82 cmp_bit(p, q, True{}, True{})
83
84# Comparing two words compares their values.
85law word_cmp_nat:
86 for n: Nat
87 for a: Word(n)
88 for b: Word(n)
89 {Word.cmp(n, a, b) == Nat.cmp(Word.to_nat(n, a), Word.to_nat(n, b)) : Cmp}
90
91def word_cmp_nat(n, a, b):
92 match n:
93 case 0n:
94 {==}
95 case 1n+ +p:
96 match a b:
97 case WCon{+x, +at} WCon{+y, +bt}:
98 %to_nat_con(p, x, at) : {Word.cmp.fin(x, y, Word.cmp(p, at, bt)) ==
99 Nat.cmp(_, Word.to_nat(1n+p, WCon{y, bt})) : Cmp}
100 %to_nat_con(p, y, bt) : {Word.cmp.fin(x, y, Word.cmp(p, at, bt)) ==
101 Nat.cmp(bit(x, Word.to_nat(p, at)), _) : Cmp}
102 %cmp_bit(Word.to_nat(p, at), Word.to_nat(p, bt), x, y) :
103 {Word.cmp.fin(x, y, Word.cmp(p, at, bt)) == _ : Cmp}
104 %word_cmp_nat(p, at, bt) : {Word.cmp.fin(x, y, Word.cmp(p, at, bt)) ==
105 Word.cmp.fin(x, y, _) : Cmp}
106 {==}
107
108law u32_cmp_nat:
109 for a: U32
110 for b: U32
111 {U32.cmp(a, b) == Nat.cmp(U32.to_nat(a), U32.to_nat(b)) : Cmp}
112
113def u32_cmp_nat(a, b):
114 match a b:
115 case U32{x} U32{y}:
116 word_cmp_nat(32n, x, y)
117
118law u32_is_lt_nat:
119 for a: U32
120 for b: U32
121 {U32.is_lt(a, b) == Nat.is_lt(U32.to_nat(a), U32.to_nat(b)) : Bool}
122
123def u32_is_lt_nat(a, b):
124 Equal.cong(Cmp, Bool, c => Cmp.is_lt(c), U32.cmp(a, b),
125 Nat.cmp(U32.to_nat(a), U32.to_nat(b)), u32_cmp_nat(a, b))
126
127law u32_is_le_nat:
128 for a: U32
129 for b: U32
130 {U32.is_le(a, b) == Nat.is_le(U32.to_nat(a), U32.to_nat(b)) : Bool}
131
132def u32_is_le_nat(a, b):
133 Equal.cong(Cmp, Bool, c => Cmp.is_le(c), U32.cmp(a, b),
134 Nat.cmp(U32.to_nat(a), U32.to_nat(b)), u32_cmp_nat(a, b))
135
136law u32_is_eq_nat:
137 for a: U32
138 for b: U32
139 {U32.is_eq(a, b) == Nat.is_eq(U32.to_nat(a), U32.to_nat(b)) : Bool}
140
141def u32_is_eq_nat(a, b):
142 Equal.cong(Cmp, Bool, c => Cmp.is_eq(c), U32.cmp(a, b),
143 Nat.cmp(U32.to_nat(a), U32.to_nat(b)), u32_cmp_nat(a, b))
144
145law odd_lt_double:
146 for a: Nat
147 for b: Nat
148 for h: MNat.lt(a, b)
149 MNat.lt(1n+Nat.double(a), Nat.double(b))
150
151def odd_lt_double(a, b, h):
152 match a b:
153 case 0n 0n:
154 Empty.absurd(MNat.lt(1n, 0n), MNat.lt_zero(0n)(h))
155 case 0n 1n+q:
156 {==}
157 case 1n+p 0n:
158 Empty.absurd(MNat.lt(1n+Nat.double(1n+p), 0n), MNat.lt_zero(1n+p)(h))
159 case 1n+p 1n+q:
160 odd_lt_double(p, q, h)
161
162# A word of n bits has a value below 2^n.
163law word_to_nat_lt:
164 for n: Nat
165 for w: Word(n)
166 MNat.lt(Word.to_nat(n, w), pow2(n))
167
168def word_to_nat_lt(n, w):
169 match n:
170 case 0n:
171 {==}
172 case 1n+ +p:
173 match w:
174 case WCon{False{}, +t}:
175 MNat.double_lt_double(Word.to_nat(p, t), pow2(p), word_to_nat_lt(p, t))
176 case WCon{True{}, +t}:
177 odd_lt_double(Word.to_nat(p, t), pow2(p), word_to_nat_lt(p, t))
178
179law u32_to_nat_word:
180 for -x: Word(32n)
181 {Word.to_nat(32n, x) == U32.to_nat(U32{x}) : Nat}
182
183def u32_to_nat_word(x):
184 {==}
185
186law u32_to_nat_lt:
187 for a: U32
188 MNat.lt(U32.to_nat(a), pow2(32n))
189
190def u32_to_nat_lt(a):
191 match a:
192 case U32{+x}:
193 # A conversion here expands pow2(32n) and overflows the checker stack (bendlang/bend#1071).
194 %u32_to_nat_word(x) : MNat.lt(_, pow2(32n))
195 word_to_nat_lt(32n, x)
196
197law double_inj:
198 for a: Nat
199 for b: Nat
200 for h: {Nat.double(a) == Nat.double(b) : Nat}
201 {a == b : Nat}
202
203def double_inj(a, b, h):
204 match a b:
205 case 0n 0n:
206 {==}
207 case 0n 1n+q:
208 Empty.absurd({0n == 1n+q : Nat}, MNat.zero_ne_succ(1n+Nat.double(q))(h))
209 case 1n+p 0n:
210 Empty.absurd({1n+p == 0n : Nat}, MNat.succ_ne_zero(1n+Nat.double(p))(h))
211 case 1n+p 1n+q:
212 Equal.cong(Nat, Nat, k => 1n+k, p, q,
213 double_inj(p, q, MNat.succ_inj(Nat.double(p), Nat.double(q),
214 MNat.succ_inj(1n+Nat.double(p), 1n+Nat.double(q), h))))
215
216law double_ne_odd:
217 for a: Nat
218 for b: Nat
219 for h: {Nat.double(a) == 1n+Nat.double(b) : Nat}
220 Empty
221
222def double_ne_odd(a, b, h):
223 match a b:
224 case 0n 0n:
225 MNat.zero_ne_succ(0n)(h)
226 case 0n 1n+q:
227 MNat.zero_ne_succ(2n+Nat.double(q))(h)
228 case 1n+p 0n:
229 MNat.succ_ne_zero(Nat.double(p))(MNat.succ_inj(1n+Nat.double(p), 0n, h))
230 case 1n+p 1n+q:
231 double_ne_odd(p, q, MNat.succ_inj(Nat.double(p), 1n+Nat.double(q),
232 MNat.succ_inj(1n+Nat.double(p), 2n+Nat.double(q), h)))
233
234# Two words with the same value are the same word.
235law word_to_nat_inj:
236 for n: Nat
237 for a: Word(n)
238 for b: Word(n)
239 for h: {Word.to_nat(n, a) == Word.to_nat(n, b) : Nat}
240 {a == b : Word(n)}
241
242def word_to_nat_inj(n, a, b, h):
243 match n:
244 case 0n:
245 match a b:
246 case WNil{} WNil{}:
247 {==}
248 case 1n+ +p:
249 match a b:
250 case WCon{False{}, +at} WCon{False{}, +bt}:
251 Equal.cong(Word(p), Word(1n+p), t => WCon{False{}, t}, at, bt,
252 word_to_nat_inj(p, at, bt, double_inj(Word.to_nat(p, at), Word.to_nat(p, bt), h)))
253 case WCon{True{}, +at} WCon{True{}, +bt}:
254 Equal.cong(Word(p), Word(1n+p), t => WCon{True{}, t}, at, bt,
255 word_to_nat_inj(p, at, bt, double_inj(Word.to_nat(p, at), Word.to_nat(p, bt),
256 MNat.succ_inj(Nat.double(Word.to_nat(p, at)), Nat.double(Word.to_nat(p, bt)), h))))
257 case WCon{False{}, +at} WCon{True{}, +bt}:
258 Empty.absurd({WCon{False{}, at} == WCon{True{}, bt} : Word(1n+p)},
259 double_ne_odd(Word.to_nat(p, at), Word.to_nat(p, bt), h))
260 case WCon{True{}, +at} WCon{False{}, +bt}:
261 Empty.absurd({WCon{True{}, at} == WCon{False{}, bt} : Word(1n+p)},
262 double_ne_odd(Word.to_nat(p, bt), Word.to_nat(p, at),
263 Equal.sym(Nat, 1n+Nat.double(Word.to_nat(p, at)), Nat.double(Word.to_nat(p, bt)), h)))
264
265law u32_to_nat_inj:
266 for a: U32
267 for b: U32
268 for h: {U32.to_nat(a) == U32.to_nat(b) : Nat}
269 {a == b : U32}
270
271def u32_to_nat_inj(a, b, h):
272 match a b:
273 case U32{+x} U32{+y}:
274 Equal.cong(Word(32n), U32, w => U32{w}, x, y, word_to_nat_inj(32n, x, y, h))
275
276def b2n(b: Bool) -> Nat:
277 match b:
278 case False{}:
279 0n
280 case True{}:
281 1n
282
283# m when q is set, else 0.
284def scale(q: Bool, m: Nat) -> Nat:
285 match q:
286 case False{}:
287 0n
288 case True{}:
289 m
290
291# The carry out of a full adder: set when two or three of the bits are set.
292def maj(x: Bool, y: Bool, c: Bool) -> Bool:
293 match x y:
294 case False{} False{}:
295 False{}
296 case True{} True{}:
297 True{}
298 case False{} True{}:
299 c
300 case True{} False{}:
301 c
302
303# The carry out of Word.adc(n, a, b, False{}, c): the bit that a + b + c overflows into.
304def carry(n: Nat, a: Word(n), b: Word(n), c: Bool) -> Bool:
305 match n:
306 case 0n:
307 c
308 case 1n+p:
309 match a b:
310 case WCon{x, at} WCon{y, bt}:
311 carry(p, at, bt, maj(x, y, c))
312
313law scale_double:
314 for q: Bool
315 for -m: Nat
316 {Nat.double(scale(q, m)) == scale(q, Nat.double(m)) : Nat}
317
318def scale_double(q, m):
319 match q:
320 case False{}:
321 {==}
322 case True{}:
323 {==}
324
325# One bit of the adder: s + 2k is the sum c + x + y of the three input bits.
326law adc_step:
327 for +s: Nat
328 for +x: Nat
329 for +y: Nat
330 for +c: Nat
331 for +k: Nat
332 for +r: Nat
333 for +q: Bool
334 for +m: Nat
335 for +a: Nat
336 for +b: Nat
337 for ih: {Nat.add(r, scale(q, m)) == Nat.add(k, Nat.add(a, b)) : Nat}
338 for fa: {Nat.add(c, Nat.add(x, y)) == Nat.add(s, Nat.double(k)) : Nat}
339 {Nat.add(Nat.add(s, Nat.double(r)), scale(q, Nat.double(m))) == Nat.add(c, Nat.add(Nat.add(x, Nat.double(a)), Nat.add(y, Nat.double(b)))) : Nat}
340
341def adc_step(s, x, y, c, k, r, q, m, a, b, ih, fa):
342 %scale_double(q, m) : {Nat.add(Nat.add(s, Nat.double(r)), _) == Nat.add(c, Nat.add(Nat.add(x, Nat.double(a)), Nat.add(y, Nat.double(b)))) : Nat}
343 %MNat.add_assoc_sym(s, Nat.double(r), Nat.double(scale(q, m))) : {_ == Nat.add(c, Nat.add(Nat.add(x, Nat.double(a)), Nat.add(y, Nat.double(b)))) : Nat}
344 %MNat.double_add(r, scale(q, m)) : {Nat.add(s, _) == Nat.add(c, Nat.add(Nat.add(x, Nat.double(a)), Nat.add(y, Nat.double(b)))) : Nat}
345 %Equal.sym(Nat, Nat.add(r, scale(q, m)), Nat.add(k, Nat.add(a, b)), ih) :
346 {Nat.add(s, Nat.double(_)) == Nat.add(c, Nat.add(Nat.add(x, Nat.double(a)), Nat.add(y, Nat.double(b)))) : Nat}
347 %MNat.double_add_sym(k, Nat.add(a, b)) : {Nat.add(s, _) == Nat.add(c, Nat.add(Nat.add(x, Nat.double(a)), Nat.add(y, Nat.double(b)))) : Nat}
348 %MNat.double_add_sym(a, b) : {Nat.add(s, Nat.add(Nat.double(k), _)) == Nat.add(c, Nat.add(Nat.add(x, Nat.double(a)), Nat.add(y, Nat.double(b)))) : Nat}
349 %MNat.add_assoc(s, Nat.double(k), Nat.add(Nat.double(a), Nat.double(b))) : {_ == Nat.add(c, Nat.add(Nat.add(x, Nat.double(a)), Nat.add(y, Nat.double(b)))) : Nat}
350 %fa : {Nat.add(_, Nat.add(Nat.double(a), Nat.double(b))) == Nat.add(c, Nat.add(Nat.add(x, Nat.double(a)), Nat.add(y, Nat.double(b)))) : Nat}
351 %MNat.add_add_add_comm(x, y, Nat.double(a), Nat.double(b)) : {Nat.add(Nat.add(c, Nat.add(x, y)), Nat.add(Nat.double(a), Nat.double(b))) == Nat.add(c, _) : Nat}
352 %MNat.add_assoc(c, Nat.add(x, y), Nat.add(Nat.double(a), Nat.double(b))) : {Nat.add(Nat.add(c, Nat.add(x, y)), Nat.add(Nat.double(a), Nat.double(b))) == _ : Nat}
353 {==}
354
355# The adder is exact: the word sum plus the carry-out weight 2^n is c + a + b.
356law word_adc_nat:
357 for n: Nat
358 for a: Word(n)
359 for b: Word(n)
360 for c: Bool
361 {Nat.add(Word.to_nat(n, Word.adc(n, a, b, False{}, c)),
362 scale(carry(n, a, b, c), pow2(n))) ==
363 Nat.add(b2n(c), Nat.add(Word.to_nat(n, a), Word.to_nat(n, b))) : Nat}
364
365def word_adc_nat(n, a, b, c):
366 match n:
367 case 0n:
368 match c:
369 case False{}:
370 {==}
371 case True{}:
372 {==}
373 case 1n+ +p:
374 match a b c:
375 case WCon{False{}, +at} WCon{False{}, +bt} False{}:
376 adc_step(0n, 0n, 0n, 0n, 0n,
377 Word.to_nat(p, Word.adc(p, at, bt, False{}, False{})), carry(p, at, bt, False{}), pow2(p),
378 Word.to_nat(p, at), Word.to_nat(p, bt), word_adc_nat(p, at, bt, False{}), {==})
379 case WCon{False{}, +at} WCon{False{}, +bt} True{}:
380 adc_step(1n, 0n, 0n, 1n, 0n,
381 Word.to_nat(p, Word.adc(p, at, bt, False{}, False{})), carry(p, at, bt, False{}), pow2(p),
382 Word.to_nat(p, at), Word.to_nat(p, bt), word_adc_nat(p, at, bt, False{}), {==})
383 case WCon{False{}, +at} WCon{True{}, +bt} False{}:
384 adc_step(1n, 0n, 1n, 0n, 0n,
385 Word.to_nat(p, Word.adc(p, at, bt, False{}, False{})), carry(p, at, bt, False{}), pow2(p),
386 Word.to_nat(p, at), Word.to_nat(p, bt), word_adc_nat(p, at, bt, False{}), {==})
387 case WCon{False{}, +at} WCon{True{}, +bt} True{}:
388 adc_step(0n, 0n, 1n, 1n, 1n,
389 Word.to_nat(p, Word.adc(p, at, bt, False{}, True{})), carry(p, at, bt, True{}), pow2(p),
390 Word.to_nat(p, at), Word.to_nat(p, bt), word_adc_nat(p, at, bt, True{}), {==})
391 case WCon{True{}, +at} WCon{False{}, +bt} False{}:
392 adc_step(1n, 1n, 0n, 0n, 0n,
393 Word.to_nat(p, Word.adc(p, at, bt, False{}, False{})), carry(p, at, bt, False{}), pow2(p),
394 Word.to_nat(p, at), Word.to_nat(p, bt), word_adc_nat(p, at, bt, False{}), {==})
395 case WCon{True{}, +at} WCon{False{}, +bt} True{}:
396 adc_step(0n, 1n, 0n, 1n, 1n,
397 Word.to_nat(p, Word.adc(p, at, bt, False{}, True{})), carry(p, at, bt, True{}), pow2(p),
398 Word.to_nat(p, at), Word.to_nat(p, bt), word_adc_nat(p, at, bt, True{}), {==})
399 case WCon{True{}, +at} WCon{True{}, +bt} False{}:
400 adc_step(0n, 1n, 1n, 0n, 1n,
401 Word.to_nat(p, Word.adc(p, at, bt, False{}, True{})), carry(p, at, bt, True{}), pow2(p),
402 Word.to_nat(p, at), Word.to_nat(p, bt), word_adc_nat(p, at, bt, True{}), {==})
403 case WCon{True{}, +at} WCon{True{}, +bt} True{}:
404 adc_step(1n, 1n, 1n, 1n, 1n,
405 Word.to_nat(p, Word.adc(p, at, bt, False{}, True{})), carry(p, at, bt, True{}), pow2(p),
406 Word.to_nat(p, at), Word.to_nat(p, bt), word_adc_nat(p, at, bt, True{}), {==})
407
408# Moves a strict upper bound across an equation without a conversion check.
409law lt_rw:
410 for -a: Nat
411 for -b: Nat
412 for -c: Nat
413 for e: {a == b : Nat}
414 for h: MNat.lt(b, c)
415 MNat.lt(a, c)
416
417def lt_rw(a, b, c, e, h):
418 %Equal.sym(Nat, a, b, e) : MNat.lt(_, c)
419 h
420
421law add_no_carry:
422 for q: Bool
423 for +r: Nat
424 for +m: Nat
425 for +s: Nat
426 for e: {Nat.add(r, scale(q, m)) == s : Nat}
427 for h: MNat.lt(s, m)
428 {r == s : Nat}
429
430def add_no_carry(q, r, m, s, e, h):
431 match q:
432 case False{}:
433 Equal.trans(Nat, r, Nat.add(r, 0n), s, MNat.add_zero_sym(r), e)
434 case True{}:
435 Empty.absurd({r == s : Nat}, MNat.lt_irrefl(m)(MNat.lt_of_le_of_lt(m, Nat.add(r, m), m,
436 MNat.le_add_left(m, r), lt_rw(Nat.add(r, m), s, m, e, h))))
437
438law add_mod_carry:
439 for q: Bool
440 for +r: Nat
441 for +m: Nat
442 for +s: Nat
443 for e: {Nat.add(r, scale(q, m)) == s : Nat}
444 for h: MNat.lt(r, m)
445 {r == Nat.mod(s, m) : Nat}
446
447def add_mod_carry(q, r, m, s, e, h):
448 match q:
449 case False{}:
450 %e : {r == Nat.mod(_, m) : Nat}
451 %MNat.add_zero_sym(r) : {r == Nat.mod(_, m) : Nat}
452 Equal.sym(Nat, Nat.mod(r, m), r, MNat.mod_eq_of_lt(r, m, h))
453 case True{}:
454 %e : {r == Nat.mod(_, m) : Nat}
455 %MNat.add_comm(m, r) : {r == Nat.mod(_, m) : Nat}
456 %MNat.add_mod_left_sym(r, m) : {r == _ : Nat}
457 Equal.sym(Nat, Nat.mod(r, m), r, MNat.mod_eq_of_lt(r, m, h))
458
459# Addition without overflow is exact.
460law word_add_nat:
461 for +n: Nat
462 for +a: Word(n)
463 for +b: Word(n)
464 for h: MNat.lt(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), pow2(n))
465 {Word.to_nat(n, Word.add(n, a, b)) == Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}
466
467def word_add_nat(n, a, b, h):
468 add_no_carry(carry(n, a, b, False{}), Word.to_nat(n, Word.adc(n, a, b, False{}, False{})), pow2(n),
469 Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), word_adc_nat(n, a, b, False{}), h)
470
471# Addition wraps modulo 2^n.
472law word_add_mod:
473 for +n: Nat
474 for +a: Word(n)
475 for +b: Word(n)
476 {Word.to_nat(n, Word.add(n, a, b)) ==
477 Nat.mod(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), pow2(n)) : Nat}
478
479def word_add_mod(n, a, b):
480 add_mod_carry(carry(n, a, b, False{}), Word.to_nat(n, Word.adc(n, a, b, False{}, False{})), pow2(n),
481 Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), word_adc_nat(n, a, b, False{}),
482 word_to_nat_lt(n, Word.adc(n, a, b, False{}, False{})))
483
484law u32_add_word:
485 for -x: Word(32n)
486 for -y: Word(32n)
487 {Word.to_nat(32n, Word.add(32n, x, y)) == U32.to_nat(U32.add(U32{x}, U32{y})) : Nat}
488
489def u32_add_word(x, y):
490 {==}
491
492law u32_add_nat:
493 for a: U32
494 for b: U32
495 for h: MNat.lt(Nat.add(U32.to_nat(a), U32.to_nat(b)), pow2(32n))
496 {U32.to_nat(U32.add(a, b)) == Nat.add(U32.to_nat(a), U32.to_nat(b)) : Nat}
497
498def u32_add_nat(a, b, h):
499 match a b:
500 case U32{+x} U32{+y}:
501 word_add_nat(32n, x, y, lt_rw(Nat.add(Word.to_nat(32n, x), Word.to_nat(32n, y)),
502 Nat.add(U32.to_nat(U32{x}), U32.to_nat(U32{y})), pow2(32n), {==}, h))
503
504law u32_add_mod:
505 for a: U32
506 for b: U32
507 {U32.to_nat(U32.add(a, b)) == Nat.mod(Nat.add(U32.to_nat(a), U32.to_nat(b)), pow2(32n)) : Nat}
508
509def u32_add_mod(a, b):
510 match a b:
511 case U32{+x} U32{+y}:
512 %u32_add_word(x, y) :
513 {_ == Nat.mod(Nat.add(U32.to_nat(U32{x}), U32.to_nat(U32{y})), pow2(32n)) : Nat}
514 %u32_to_nat_word(x) : {Word.to_nat(32n, Word.add(32n, x, y)) ==
515 Nat.mod(Nat.add(_, U32.to_nat(U32{y})), pow2(32n)) : Nat}
516 %u32_to_nat_word(y) : {Word.to_nat(32n, Word.add(32n, x, y)) ==
517 Nat.mod(Nat.add(Word.to_nat(32n, x), _), pow2(32n)) : Nat}
518 word_add_mod(32n, x, y)
519
520# The bitwise complement of w has value 2^n - 1 - w.
521law word_not_nat:
522 for n: Nat
523 for w: Word(n)
524 {1n+Nat.add(Word.to_nat(n, Word.not(n, w)), Word.to_nat(n, w)) == pow2(n) : Nat}
525
526def word_not_nat(n, w):
527 match n:
528 case 0n:
529 {==}
530 case 1n+ +p:
531 match w:
532 case WCon{False{}, +t}:
533 %word_not_nat(p, t) : {2n+Nat.add(Nat.double(Word.to_nat(p, Word.not(p, t))), Nat.double(Word.to_nat(p, t))) == Nat.double(_) : Nat}
534 %MNat.double_add_sym(Word.to_nat(p, Word.not(p, t)), Word.to_nat(p, t)) : {2n+Nat.add(Nat.double(Word.to_nat(p, Word.not(p, t))), Nat.double(Word.to_nat(p, t))) == 2n+_ : Nat}
535 {==}
536 case WCon{True{}, +t}:
537 %MNat.add_succ_sym(Nat.double(Word.to_nat(p, Word.not(p, t))), Nat.double(Word.to_nat(p, t))) : {1n+_ == pow2(1n+p) : Nat}
538 %word_not_nat(p, t) : {2n+Nat.add(Nat.double(Word.to_nat(p, Word.not(p, t))), Nat.double(Word.to_nat(p, t))) == Nat.double(_) : Nat}
539 %MNat.double_add_sym(Word.to_nat(p, Word.not(p, t)), Word.to_nat(p, t)) : {2n+Nat.add(Nat.double(Word.to_nat(p, Word.not(p, t))), Nat.double(Word.to_nat(p, t))) == 2n+_ : Nat}
540 {==}
541
542# Subtraction is addition of the complement with a carry in.
543law word_sub_not:
544 for n: Nat
545 for a: Word(n)
546 for b: Word(n)
547 for +c: Bool
548 {Word.adc(n, a, b, True{}, c) == Word.adc(n, a, Word.not(n, b), False{}, c) : Word(n)}
549
550def word_sub_not(n, a, b, c):
551 match n:
552 case 0n:
553 {==}
554 case 1n+ +p:
555 match a b:
556 case WCon{False{}, +at} WCon{+y, +bt}:
557 Equal.cong(Word(p), Word(1n+p), w => WCon{Bool.xor(Bool.not(y), c), w},
558 Word.adc(p, at, bt, True{}, Bool.and(Bool.not(y), c)),
559 Word.adc(p, at, Word.not(p, bt), False{}, Bool.and(Bool.not(y), c)),
560 word_sub_not(p, at, bt, Bool.and(Bool.not(y), c)))
561 case WCon{True{}, +at} WCon{+y, +bt}:
562 Equal.cong(Word(p), Word(1n+p), w => WCon{Bool.not(Bool.xor(Bool.not(y), c)), w},
563 Word.adc(p, at, bt, True{}, Bool.or(Bool.not(y), c)),
564 Word.adc(p, at, Word.not(p, bt), False{}, Bool.or(Bool.not(y), c)),
565 word_sub_not(p, at, bt, Bool.or(Bool.not(y), c)))
566
567law sub_arith:
568 for +a: Nat
569 for +b: Nat
570 for +nb: Nat
571 for +m: Nat
572 for h: MNat.le(b, a)
573 for hn: {1n+Nat.add(nb, b) == m : Nat}
574 {1n+Nat.add(a, nb) == Nat.add(Nat.sub(a, b), m) : Nat}
575
576def sub_arith(a, b, nb, m, h, hn):
577 %hn : {1n+Nat.add(a, nb) == Nat.add(Nat.sub(a, b), _) : Nat}
578 %MNat.add_succ_sym(Nat.sub(a, b), Nat.add(nb, b)) : {1n+Nat.add(a, nb) == _ : Nat}
579 %MNat.sub_add_cancel(a, b, h) : {1n+Nat.add(_, nb) == 1n+Nat.add(Nat.sub(a, b), Nat.add(nb, b)) : Nat}
580 %MNat.add_assoc_sym(Nat.sub(a, b), b, nb) : {1n+_ == 1n+Nat.add(Nat.sub(a, b), Nat.add(nb, b)) : Nat}
581 %MNat.add_comm(nb, b) : {1n+Nat.add(Nat.sub(a, b), _) == 1n+Nat.add(Nat.sub(a, b), Nat.add(nb, b)) : Nat}
582 {==}
583
584law sub_fin:
585 for q: Bool
586 for +r: Nat
587 for +d: Nat
588 for +m: Nat
589 for e: {Nat.add(r, scale(q, m)) == Nat.add(d, m) : Nat}
590 for h: MNat.lt(r, m)
591 {r == d : Nat}
592
593def sub_fin(q, r, d, m, e, h):
594 match q:
595 case False{}:
596 Empty.absurd({r == d : Nat}, MNat.lt_irrefl(m)(MNat.lt_of_le_of_lt(m, Nat.add(d, m), m,
597 MNat.le_add_left(m, d), lt_rw(Nat.add(d, m), r, m,
598 Equal.sym(Nat, r, Nat.add(d, m),
599 Equal.trans(Nat, r, Nat.add(r, 0n), Nat.add(d, m), MNat.add_zero_sym(r), e)), h))))
600 case True{}:
601 MNat.add_right_cancel(r, m, d, e)
602
603# Subtraction without wrap is exact.
604law word_sub_nat:
605 for +n: Nat
606 for +a: Word(n)
607 for +b: Word(n)
608 for h: MNat.le(Word.to_nat(n, b), Word.to_nat(n, a))
609 {Word.to_nat(n, Word.sub(n, a, b)) == Nat.sub(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}
610
611def word_sub_nat(n, a, b, h):
612 %Equal.sym(Word(n), Word.adc(n, a, b, True{}, True{}),
613 Word.adc(n, a, Word.not(n, b), False{}, True{}), word_sub_not(n, a, b, True{})) :
614 {Word.to_nat(n, _) == Nat.sub(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}
615 sub_fin(carry(n, a, Word.not(n, b), True{}),
616 Word.to_nat(n, Word.adc(n, a, Word.not(n, b), False{}, True{})),
617 Nat.sub(Word.to_nat(n, a), Word.to_nat(n, b)), pow2(n),
618 Equal.trans(Nat,
619 Nat.add(Word.to_nat(n, Word.adc(n, a, Word.not(n, b), False{}, True{})),
620 scale(carry(n, a, Word.not(n, b), True{}), pow2(n))),
621 1n+Nat.add(Word.to_nat(n, a), Word.to_nat(n, Word.not(n, b))),
622 Nat.add(Nat.sub(Word.to_nat(n, a), Word.to_nat(n, b)), pow2(n)),
623 word_adc_nat(n, a, Word.not(n, b), True{}),
624 sub_arith(Word.to_nat(n, a), Word.to_nat(n, b), Word.to_nat(n, Word.not(n, b)), pow2(n), h,
625 word_not_nat(n, b))),
626 word_to_nat_lt(n, Word.adc(n, a, Word.not(n, b), False{}, True{})))
627
628law u32_sub_nat:
629 for a: U32
630 for b: U32
631 for h: MNat.le(U32.to_nat(b), U32.to_nat(a))
632 {U32.to_nat(U32.sub(a, b)) == Nat.sub(U32.to_nat(a), U32.to_nat(b)) : Nat}
633
634def u32_sub_nat(a, b, h):
635 match a b:
636 case U32{x} U32{y}:
637 word_sub_nat(32n, x, y, h)
638
639law lt_of_double_lt:
640 for a: Nat
641 for b: Nat
642 for h: MNat.lt(Nat.double(a), Nat.double(b))
643 MNat.lt(a, b)
644
645def lt_of_double_lt(a, b, h):
646 match a b:
647 case 0n 0n:
648 Empty.absurd(MNat.lt(0n, 0n), MNat.lt_zero(0n)(h))
649 case 1n+p 0n:
650 Empty.absurd(MNat.lt(1n+p, 0n), MNat.lt_zero(2n+Nat.double(p))(h))
651 case 0n 1n+q:
652 {==}
653 case 1n+p 1n+q:
654 lt_of_double_lt(p, q, h)
655
656# Incrementing without overflow adds one.
657law word_inc_nat:
658 for n: Nat
659 for w: Word(n)
660 for h: MNat.lt(1n+Word.to_nat(n, w), pow2(n))
661 {Word.to_nat(n, Word.inc(n, w)) == 1n+Word.to_nat(n, w) : Nat}
662
663def word_inc_nat(n, w, h):
664 match n:
665 case 0n:
666 Empty.absurd({0n == 1n : Nat}, MNat.lt_irrefl(1n)(h))
667 case 1n+ +p:
668 match w:
669 case WCon{False{}, t}:
670 {==}
671 case WCon{True{}, +t}:
672 Equal.cong(Nat, Nat, v => Nat.double(v), Word.to_nat(p, Word.inc(p, t)),
673 1n+Word.to_nat(p, t),
674 word_inc_nat(p, t, lt_of_double_lt(1n+Word.to_nat(p, t), pow2(p), h)))
675
676law u32_inc_nat:
677 for a: U32
678 for h: MNat.lt(1n+U32.to_nat(a), pow2(32n))
679 {U32.to_nat(U32.inc(a)) == 1n+U32.to_nat(a) : Nat}
680
681def u32_inc_nat(a, h):
682 match a:
683 case U32{+x}:
684 word_inc_nat(32n, x, lt_rw(1n+Word.to_nat(32n, x), 1n+U32.to_nat(U32{x}), pow2(32n), {==}, h))
685
686law u32_to_from_nat:
687 for k: Nat
688 for +h: MNat.lt(k, pow2(32n))
689 {U32.to_nat(U32.from_nat(k)) == k : Nat}
690
691def u32_to_from_nat(k, h):
692 match k:
693 case 0n:
694 {==}
695 case 1n+ +j:
696 +ih = u32_to_from_nat(j, MNat.lt_trans(j, 1n+j, pow2(32n), MNat.lt_succ_self(j), h))
697 Equal.trans(Nat, U32.to_nat(U32.inc(U32.from_nat(j))), 1n+U32.to_nat(U32.from_nat(j)), 1n+j,
698 u32_inc_nat(U32.from_nat(j), lt_rw(1n+U32.to_nat(U32.from_nat(j)), 1n+j, pow2(32n),
699 Equal.cong(Nat, Nat, v => 1n+v, U32.to_nat(U32.from_nat(j)), j, ih), h)),
700 Equal.cong(Nat, Nat, v => 1n+v, U32.to_nat(U32.from_nat(j)), j, ih))
701
702law u32_from_to_nat:
703 for +a: U32
704 {U32.from_nat(U32.to_nat(a)) == a : U32}
705
706def u32_from_to_nat(a):
707 u32_to_nat_inj(U32.from_nat(U32.to_nat(a)), a, u32_to_from_nat(U32.to_nat(a), u32_to_nat_lt(a)))
708
709law and_le_sub:
710 for c: Bool
711 for +a: Nat
712 for +b: Nat
713 for +l: Nat
714 for -s: Nat
715 for +hc: {Nat.is_le(a, l) == c : Bool}
716 for hs: MNat.le(a, l) -> {s == Nat.sub(l, a) : Nat}
717 {Bool.and(c, Nat.is_le(b, s)) == Nat.is_le(Nat.add(a, b), l) : Bool}
718
719def and_le_sub(c, a, b, l, s, hc, hs):
720 match c:
721 case True{}:
722 %Equal.sym(Nat, s, Nat.sub(l, a), hs(hc)) :
723 {Bool.and(True{}, Nat.is_le(b, _)) == Nat.is_le(Nat.add(a, b), l) : Bool}
724 %hc : {Bool.and(_, Nat.is_le(b, Nat.sub(l, a))) == Nat.is_le(Nat.add(a, b), l) : Bool}
725 MNat.le_and_le_sub_iff_add_le(a, b, l)
726 case False{}:
727 %MNat.le_and_le_sub_iff_add_le(a, b, l) : {Bool.and(False{}, Nat.is_le(b, s)) == _ : Bool}
728 %Equal.sym(Bool, Nat.is_le(a, l), False{}, hc) :
729 {Bool.and(False{}, Nat.is_le(b, s)) == Bool.and(_, Nat.is_le(b, Nat.sub(l, a))) : Bool}
730 {==}
731
732# The overflow-safe bounds check n <= len and i <= len - n holds exactly when i + n <= len.
733law u32_fits_nat:
734 for +len: U32
735 for +i: U32
736 for +n: U32
737 {Bool.and(U32.is_le(n, len), U32.is_le(i, U32.sub(len, n))) == Nat.is_le(Nat.add(U32.to_nat(i), U32.to_nat(n)), U32.to_nat(len)) : Bool}
738
739def u32_fits_nat(len, i, n):
740 %Equal.sym(Bool, U32.is_le(n, len), Nat.is_le(U32.to_nat(n), U32.to_nat(len)), u32_is_le_nat(n, len)) :
741 {Bool.and(_, U32.is_le(i, U32.sub(len, n))) == Nat.is_le(Nat.add(U32.to_nat(i), U32.to_nat(n)), U32.to_nat(len)) : Bool}
742 %Equal.sym(Bool, U32.is_le(i, U32.sub(len, n)), Nat.is_le(U32.to_nat(i), U32.to_nat(U32.sub(len, n))), u32_is_le_nat(i, U32.sub(len, n))) :
743 {Bool.and(Nat.is_le(U32.to_nat(n), U32.to_nat(len)), _) == Nat.is_le(Nat.add(U32.to_nat(i), U32.to_nat(n)), U32.to_nat(len)) : Bool}
744 %MNat.add_comm(U32.to_nat(n), U32.to_nat(i)) :
745 {Bool.and(Nat.is_le(U32.to_nat(n), U32.to_nat(len)), Nat.is_le(U32.to_nat(i), U32.to_nat(U32.sub(len, n)))) == Nat.is_le(_, U32.to_nat(len)) : Bool}
746 and_le_sub(Nat.is_le(U32.to_nat(n), U32.to_nat(len)), U32.to_nat(n), U32.to_nat(i), U32.to_nat(len), U32.to_nat(U32.sub(len, n)), {==}, h => u32_sub_nat(len, n, h))