proofs/lib/lemmas/proofs/word_comparison.bend
bend-collections-laws-containers@1.0.0.0 · 55 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/numeric.bend as N
4
5# Base compares high bits first. Mathematical interpretation preserves that
6# exact comparison, including equality, at every width.
7def digits(a: Nat, b: Nat, x: Bool, y: Bool) -> {Nat.cmp(Nat.add(S.bit_value(x), Nat.double(a)), Nat.add(S.bit_value(y), Nat.double(b))) == Word.cmp.fin(x, y, Nat.cmp(a, b)) : Cmp}:
8 match a b:
9 case 0n 0n:
10 match x y:
11 case False{} False{}: {==}
12 case False{} True{}: {==}
13 case True{} False{}: {==}
14 case True{} True{}: {==}
15 case 0n 1n+p:
16 match x y:
17 case False{} False{}: {==}
18 case False{} True{}: {==}
19 case True{} False{}: {==}
20 case True{} True{}: {==}
21 case 1n+p 0n:
22 match x y:
23 case False{} False{}: {==}
24 case False{} True{}: {==}
25 case True{} False{}: {==}
26 case True{} True{}: {==}
27 case 1n+p 1n+q:
28 match x y:
29 case False{} False{}: digits(p, q, False{}, False{})
30 case False{} True{}: digits(p, q, False{}, True{})
31 case True{} False{}: digits(p, q, True{}, False{})
32 case True{} True{}: digits(p, q, True{}, True{})
33
34def refines(+n: Nat, a: Word(n), b: Word(n)) -> {Word.cmp(n, a, b) == Nat.cmp(S.unsigned(n, a), S.unsigned(n, b)) : Cmp}:
35 match n:
36 case 0n:
37 match a b:
38 case WNil{} WNil{}: {==}
39 case 1n+ +p:
40 match a b:
41 case WCon{+x, +at} WCon{+y, +bt}:
42 Equal.trans(Cmp, Word.cmp.fin(x, y, Word.cmp(p, at, bt)), Word.cmp.fin(x, y, Nat.cmp(S.unsigned(p, at), S.unsigned(p, bt))), Nat.cmp(Nat.add(S.bit_value(x), Nat.double(S.unsigned(p, at))), Nat.add(S.bit_value(y), Nat.double(S.unsigned(p, bt)))), Equal.cong(Cmp, Cmp, c => Word.cmp.fin(x, y, c), Word.cmp(p, at, bt), Nat.cmp(S.unsigned(p, at), S.unsigned(p, bt)), refines(p, at, bt)), Equal.sym(Cmp, Nat.cmp(Nat.add(S.bit_value(x), Nat.double(S.unsigned(p, at))), Nat.add(S.bit_value(y), Nat.double(S.unsigned(p, bt)))), Word.cmp.fin(x, y, Nat.cmp(S.unsigned(p, at), S.unsigned(p, bt))), digits(S.unsigned(p, at), S.unsigned(p, bt), x, y)))
43
44def u32_refines(a: U32, b: U32) -> {U32.cmp(a, b) == Nat.cmp(U32.to_nat(a), U32.to_nat(b)) : Cmp}:
45 match a b:
46 case U32{+x} U32{+y}:
47 %Equal.sym(Nat, Word.to_nat(32n, x), S.unsigned(32n, x), N.primitive_word_interpretation(32n, x)) : {U32.cmp(U32{x}, U32{y}) == Nat.cmp(_, Word.to_nat(32n, y)) : Cmp}
48 %Equal.sym(Nat, Word.to_nat(32n, y), S.unsigned(32n, y), N.primitive_word_interpretation(32n, y)) : {U32.cmp(U32{x}, U32{y}) == Nat.cmp(S.unsigned(32n, x), _) : Cmp}
49 refines(32n, x, y)
50
51def u32_ge(+a: U32, +b: U32) -> {U32.is_ge(a, b) == Nat.is_ge(U32.to_nat(a), U32.to_nat(b)) : Bool}:
52 Equal.cong(Cmp, Bool, Cmp.is_ge, U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), u32_refines(a, b))
53
54def u32_lt(+a: U32, +b: U32) -> {U32.is_lt(a, b) == Nat.is_lt(U32.to_nat(a), U32.to_nat(b)) : Bool}:
55 Equal.cong(Cmp, Bool, Cmp.is_lt, U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), u32_refines(a, b))