PROOF_bits.bend

bend-osdev-word64@0.1.1.0 · 196 lines · 22 definitions

1# Generated by gen/proof.py; do not edit by hand. The proofs of LAWS_bits.bend:
2# the bitwise operations and the one-bit shift.
3import Base
4import bend-osdev-u32@0.1.0.0/u32.bend as U
5import bend-osdev-u32@0.1.0.0/LAWS.bend as UL
6import bend-osdev-u32@0.1.0.0/PROOF.bend as UP
7import bend-osdev-word64@0.1.1.0/word64.bend as W
8import bend-osdev-word64@0.1.1.0/LAWS.bend as WB
9import bend-osdev-word64@0.1.1.0/PROOF.bend as WBP
10import bend-osdev-word64@0.1.1.0/proof_value.bend as P
11import bend-osdev-word64@0.1.1.0/proof_shift.bend as PS
12import bend-osdev-word64@0.1.1.0/LAWS_bits.bend as Laws
13
14# Bounds in the exact form a lemma takes them: a U32 value below 2^32, a W64
15# value below 2^64
16
17def wu.ve(+w: Word(32n)) -> {Word.to_nat(32n, w) == U32.to_nat(U32{w}) : Nat}:
18  {==}
19
20def wu.lt(+x: U32) -> {Nat.is_lt(U32.to_nat(x), U.U32Nat.dbl(32n, 1n)) == True{} : Bool}:
21  match x:
22    case U32{+w}:
23      %wu.ve(w) : {Nat.is_lt(_, U.U32Nat.dbl(32n, 1n)) == True{} : Bool}
24      UL.word_value_lt(32n, w)
25
26def wv.g(+n: Nat, +m: Nat, +h: Word(n), +l: Word(n), e: {Nat.add(n, n) == m : Nat}) -> {Nat.is_lt(P.wv.V(n, h, l), U.U32Nat.dbl(m, 1n)) == True{} : Bool}:
27  %e : {Nat.is_lt(P.wv.V(n, h, l), U.U32Nat.dbl(_, 1n)) == True{} : Bool}
28  %UL.dbl_dbl(n, n, 1n) : {Nat.is_lt(P.wv.V(n, h, l), _) == True{} : Bool}
29  P.wv.val_lt2(n, Word.to_nat(n, l), Word.to_nat(n, h), UL.word_value_lt(n, l), UL.word_value_lt(n, h))
30
31def wv.ve(+h: Word(32n), +l: Word(32n)) -> {P.wv.V(32n, h, l) == W.W64.to_nat(W.W64{U32{h}, U32{l}}) : Nat}:
32  {==}
33
34def wv.lt64(+x: W.W64) -> {Nat.is_lt(W.W64.to_nat(x), U.U32Nat.dbl(64n, 1n)) == True{} : Bool}:
35  match x:
36    case W.W64{U32{+h}, U32{+l}}:
37      %wv.ve(h, l) : {Nat.is_lt(_, U.U32Nat.dbl(64n, 1n)) == True{} : Bool}
38      wv.g(32n, 64n, h, l, {==})
39
40def wn.sub0(x: Nat) -> {Nat.sub(x, 0n) == x : Nat}:
41  match x:
42    case 0n:
43      {==}
44    case 1n+ +p:
45      {==}
46
47def wn.le0(x: Nat) -> {Nat.is_le(0n, x) == True{} : Bool}:
48  match x:
49    case 0n:
50      {==}
51    case 1n+ +p:
52      {==}
53
54def wn.ft(e: {False{} == True{} : Bool}) -> Empty:
55  P.wn.ft(e)
56
57def wn.tf(e: {True{} == False{} : Bool}) -> Empty:
58  PS.ns.tf(e)
59
60def wn.ge_lt(c: Cmp) -> {Cmp.is_ge(c) == Bool.not(Cmp.is_lt(c)) : Bool}:
61  match c:
62    case LT{}:
63      {==}
64    case EQ{}:
65      {==}
66    case GT{}:
67      {==}
68
69def wm.fn(+h: Nat, +n: Nat, +x: Nat, +en: {Nat.add(h, h) == n : Nat}) -> {U.U32Nat.dbl(n, x) == U.U32Nat.dbl(h, U.U32Nat.dbl(h, x)) : Nat}:
70  Equal.trans(Nat, U.U32Nat.dbl(n, x), U.U32Nat.dbl(Nat.add(h, h), x), U.U32Nat.dbl(h, U.U32Nat.dbl(h, x)), Equal.cong(Nat, Nat, zz => U.U32Nat.dbl(zz, x), n, Nat.add(h, h), Equal.sym(Nat, Nat.add(h, h), n, en)), Equal.sym(Nat, U.U32Nat.dbl(h, U.U32Nat.dbl(h, x)), U.U32Nat.dbl(Nat.add(h, h), x), UL.dbl_dbl(h, h, x)))
71
72# The bits
73
74def Laws.and_comm(a, b):
75  match a b:
76    case W.W64{+ah, +al} W.W64{+bh, +bl}:
77      %UL.u32_and_comm(al, bl) : {W.W64{U32.and(ah, bh), U32.and(al, bl)} == W.W64{U32.and(bh, ah), _} : W.W64}
78      %UL.u32_and_comm(ah, bh) : {W.W64{U32.and(ah, bh), U32.and(al, bl)} == W.W64{_, U32.and(al, bl)} : W.W64}
79      {==}
80
81def Laws.or_comm(a, b):
82  match a b:
83    case W.W64{+ah, +al} W.W64{+bh, +bl}:
84      %UL.u32_or_comm(al, bl) : {W.W64{U32.or(ah, bh), U32.or(al, bl)} == W.W64{U32.or(bh, ah), _} : W.W64}
85      %UL.u32_or_comm(ah, bh) : {W.W64{U32.or(ah, bh), U32.or(al, bl)} == W.W64{_, U32.or(al, bl)} : W.W64}
86      {==}
87
88def Laws.xor_comm(a, b):
89  match a b:
90    case W.W64{+ah, +al} W.W64{+bh, +bl}:
91      %UL.u32_xor_comm(al, bl) : {W.W64{U32.xor(ah, bh), U32.xor(al, bl)} == W.W64{U32.xor(bh, ah), _} : W.W64}
92      %UL.u32_xor_comm(ah, bh) : {W.W64{U32.xor(ah, bh), U32.xor(al, bl)} == W.W64{_, U32.xor(al, bl)} : W.W64}
93      {==}
94
95def wr.b0(+x0: Nat, +x1: Nat, +x2: Nat, +x3: Nat) -> {Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x1)), Nat.add(x2, U.U32Nat.dbl(32n, x3))) == Nat.add(Nat.add(x0, x2), U.U32Nat.dbl(32n, Nat.add(x1, x3))) : Nat}:
96  %Equal.sym(Nat, Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x1)), Nat.add(x2, U.U32Nat.dbl(32n, x3))), Nat.add(x0, Nat.add(U.U32Nat.dbl(32n, x1), Nat.add(x2, U.U32Nat.dbl(32n, x3)))), UL.nat_add_assoc(x0, U.U32Nat.dbl(32n, x1), Nat.add(x2, U.U32Nat.dbl(32n, x3)))) : {_ == Nat.add(Nat.add(x0, x2), U.U32Nat.dbl(32n, Nat.add(x1, x3))) : Nat}
97  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(32n, x1), Nat.add(x2, U.U32Nat.dbl(32n, x3))), Nat.add(x2, Nat.add(U.U32Nat.dbl(32n, x1), U.U32Nat.dbl(32n, x3))), UL.nat_add_left_comm(U.U32Nat.dbl(32n, x1), x2, U.U32Nat.dbl(32n, x3))) : {Nat.add(x0, _) == Nat.add(Nat.add(x0, x2), U.U32Nat.dbl(32n, Nat.add(x1, x3))) : Nat}
98  %Equal.sym(Nat, Nat.add(x0, Nat.add(x2, Nat.add(U.U32Nat.dbl(32n, x1), U.U32Nat.dbl(32n, x3)))), Nat.add(Nat.add(x0, x2), Nat.add(U.U32Nat.dbl(32n, x1), U.U32Nat.dbl(32n, x3))), Equal.sym(Nat, Nat.add(Nat.add(x0, x2), Nat.add(U.U32Nat.dbl(32n, x1), U.U32Nat.dbl(32n, x3))), Nat.add(x0, Nat.add(x2, Nat.add(U.U32Nat.dbl(32n, x1), U.U32Nat.dbl(32n, x3)))), UL.nat_add_assoc(x0, x2, Nat.add(U.U32Nat.dbl(32n, x1), U.U32Nat.dbl(32n, x3))))) : {_ == Nat.add(Nat.add(x0, x2), U.U32Nat.dbl(32n, Nat.add(x1, x3))) : Nat}
99  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(32n, x1), U.U32Nat.dbl(32n, x3)), U.U32Nat.dbl(32n, Nat.add(x1, x3)), Equal.sym(Nat, U.U32Nat.dbl(32n, Nat.add(x1, x3)), Nat.add(U.U32Nat.dbl(32n, x1), U.U32Nat.dbl(32n, x3)), UL.dbl_add(32n, x1, x3))) : {Nat.add(Nat.add(x0, x2), _) == Nat.add(Nat.add(x0, x2), U.U32Nat.dbl(32n, Nat.add(x1, x3))) : Nat}
100  {==}
101
102def wr.b1(+x0: Nat, +x1: Nat, +x2: Nat, +x3: Nat) -> {Nat.add(Nat.add(x0, x1), U.U32Nat.dbl(32n, Nat.add(x2, x3))) == Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x2)), Nat.add(x1, U.U32Nat.dbl(32n, x3))) : Nat}:
103  %Equal.sym(Nat, U.U32Nat.dbl(32n, Nat.add(x2, x3)), Nat.add(U.U32Nat.dbl(32n, x2), U.U32Nat.dbl(32n, x3)), UL.dbl_add(32n, x2, x3)) : {Nat.add(Nat.add(x0, x1), _) == Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x2)), Nat.add(x1, U.U32Nat.dbl(32n, x3))) : Nat}
104  %Equal.sym(Nat, Nat.add(Nat.add(x0, x1), Nat.add(U.U32Nat.dbl(32n, x2), U.U32Nat.dbl(32n, x3))), Nat.add(x0, Nat.add(x1, Nat.add(U.U32Nat.dbl(32n, x2), U.U32Nat.dbl(32n, x3)))), UL.nat_add_assoc(x0, x1, Nat.add(U.U32Nat.dbl(32n, x2), U.U32Nat.dbl(32n, x3)))) : {_ == Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x2)), Nat.add(x1, U.U32Nat.dbl(32n, x3))) : Nat}
105  %Equal.sym(Nat, Nat.add(x1, Nat.add(U.U32Nat.dbl(32n, x2), U.U32Nat.dbl(32n, x3))), Nat.add(U.U32Nat.dbl(32n, x2), Nat.add(x1, U.U32Nat.dbl(32n, x3))), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(32n, x2), Nat.add(x1, U.U32Nat.dbl(32n, x3))), Nat.add(x1, Nat.add(U.U32Nat.dbl(32n, x2), U.U32Nat.dbl(32n, x3))), UL.nat_add_left_comm(U.U32Nat.dbl(32n, x2), x1, U.U32Nat.dbl(32n, x3)))) : {Nat.add(x0, _) == Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x2)), Nat.add(x1, U.U32Nat.dbl(32n, x3))) : Nat}
106  %Equal.sym(Nat, Nat.add(x0, Nat.add(U.U32Nat.dbl(32n, x2), Nat.add(x1, U.U32Nat.dbl(32n, x3)))), Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x2)), Nat.add(x1, U.U32Nat.dbl(32n, x3))), Equal.sym(Nat, Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x2)), Nat.add(x1, U.U32Nat.dbl(32n, x3))), Nat.add(x0, Nat.add(U.U32Nat.dbl(32n, x2), Nat.add(x1, U.U32Nat.dbl(32n, x3)))), UL.nat_add_assoc(x0, U.U32Nat.dbl(32n, x2), Nat.add(x1, U.U32Nat.dbl(32n, x3))))) : {_ == Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x2)), Nat.add(x1, U.U32Nat.dbl(32n, x3))) : Nat}
107  {==}
108
109def Laws.and_or(a, b):
110  match a b:
111    case W.W64{+ah, +al} W.W64{+bh, +bl}:
112      Equal.trans(Nat, Nat.add(Nat.add(U32.to_nat(U32.and(al, bl)), U.U32Nat.dbl(32n, U32.to_nat(U32.and(ah, bh)))), Nat.add(U32.to_nat(U32.or(al, bl)), U.U32Nat.dbl(32n, U32.to_nat(U32.or(ah, bh))))), Nat.add(Nat.add(U32.to_nat(al), U32.to_nat(bl)), U.U32Nat.dbl(32n, Nat.add(U32.to_nat(ah), U32.to_nat(bh)))), Nat.add(Nat.add(U32.to_nat(al), U.U32Nat.dbl(32n, U32.to_nat(ah))), Nat.add(U32.to_nat(bl), U.U32Nat.dbl(32n, U32.to_nat(bh)))), Equal.trans(Nat, Nat.add(Nat.add(U32.to_nat(U32.and(al, bl)), U.U32Nat.dbl(32n, U32.to_nat(U32.and(ah, bh)))), Nat.add(U32.to_nat(U32.or(al, bl)), U.U32Nat.dbl(32n, U32.to_nat(U32.or(ah, bh))))), Nat.add(Nat.add(U32.to_nat(al), U32.to_nat(bl)), U.U32Nat.dbl(32n, Nat.add(U32.to_nat(U32.and(ah, bh)), U32.to_nat(U32.or(ah, bh))))), Nat.add(Nat.add(U32.to_nat(al), U32.to_nat(bl)), U.U32Nat.dbl(32n, Nat.add(U32.to_nat(ah), U32.to_nat(bh)))), Equal.trans(Nat, Nat.add(Nat.add(U32.to_nat(U32.and(al, bl)), U.U32Nat.dbl(32n, U32.to_nat(U32.and(ah, bh)))), Nat.add(U32.to_nat(U32.or(al, bl)), U.U32Nat.dbl(32n, U32.to_nat(U32.or(ah, bh))))), Nat.add(Nat.add(U32.to_nat(U32.and(al, bl)), U32.to_nat(U32.or(al, bl))), U.U32Nat.dbl(32n, Nat.add(U32.to_nat(U32.and(ah, bh)), U32.to_nat(U32.or(ah, bh))))), Nat.add(Nat.add(U32.to_nat(al), U32.to_nat(bl)), U.U32Nat.dbl(32n, Nat.add(U32.to_nat(U32.and(ah, bh)), U32.to_nat(U32.or(ah, bh))))), wr.b0(U32.to_nat(U32.and(al, bl)), U32.to_nat(U32.and(ah, bh)), U32.to_nat(U32.or(al, bl)), U32.to_nat(U32.or(ah, bh))), Equal.cong(Nat, Nat, zz => Nat.add(zz, U.U32Nat.dbl(32n, Nat.add(U32.to_nat(U32.and(ah, bh)), U32.to_nat(U32.or(ah, bh))))), Nat.add(U32.to_nat(U32.and(al, bl)), U32.to_nat(U32.or(al, bl))), Nat.add(U32.to_nat(al), U32.to_nat(bl)), UL.u32_and_or(al, bl))), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(U32.to_nat(al), U32.to_nat(bl)), U.U32Nat.dbl(32n, zz)), Nat.add(U32.to_nat(U32.and(ah, bh)), U32.to_nat(U32.or(ah, bh))), Nat.add(U32.to_nat(ah), U32.to_nat(bh)), UL.u32_and_or(ah, bh))), wr.b1(U32.to_nat(al), U32.to_nat(bl), U32.to_nat(ah), U32.to_nat(bh)))
113
114def wr.b2(+x0: Nat, +x1: Nat, +x2: Nat, +x3: Nat) -> {Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x1)), Nat.double(Nat.add(x2, U.U32Nat.dbl(32n, x3)))) == Nat.add(Nat.add(x0, Nat.double(x2)), U.U32Nat.dbl(32n, Nat.add(x1, Nat.double(x3)))) : Nat}:
115  %Equal.sym(Nat, Nat.double(Nat.add(x2, U.U32Nat.dbl(32n, x3))), Nat.add(Nat.add(x2, U.U32Nat.dbl(32n, x3)), Nat.add(x2, U.U32Nat.dbl(32n, x3))), UL.nat_double(Nat.add(x2, U.U32Nat.dbl(32n, x3)))) : {Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x1)), _) == Nat.add(Nat.add(x0, Nat.double(x2)), U.U32Nat.dbl(32n, Nat.add(x1, Nat.double(x3)))) : Nat}
116  %Equal.sym(Nat, Nat.add(Nat.add(x2, U.U32Nat.dbl(32n, x3)), Nat.add(x2, U.U32Nat.dbl(32n, x3))), Nat.add(x2, Nat.add(U.U32Nat.dbl(32n, x3), Nat.add(x2, U.U32Nat.dbl(32n, x3)))), UL.nat_add_assoc(x2, U.U32Nat.dbl(32n, x3), Nat.add(x2, U.U32Nat.dbl(32n, x3)))) : {Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x1)), _) == Nat.add(Nat.add(x0, Nat.double(x2)), U.U32Nat.dbl(32n, Nat.add(x1, Nat.double(x3)))) : Nat}
117  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(32n, x3), Nat.add(x2, U.U32Nat.dbl(32n, x3))), Nat.add(x2, Nat.add(U.U32Nat.dbl(32n, x3), U.U32Nat.dbl(32n, x3))), UL.nat_add_left_comm(U.U32Nat.dbl(32n, x3), x2, U.U32Nat.dbl(32n, x3))) : {Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x1)), Nat.add(x2, _)) == Nat.add(Nat.add(x0, Nat.double(x2)), U.U32Nat.dbl(32n, Nat.add(x1, Nat.double(x3)))) : Nat}
118  %Equal.sym(Nat, Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x1)), Nat.add(x2, Nat.add(x2, Nat.add(U.U32Nat.dbl(32n, x3), U.U32Nat.dbl(32n, x3))))), Nat.add(x0, Nat.add(U.U32Nat.dbl(32n, x1), Nat.add(x2, Nat.add(x2, Nat.add(U.U32Nat.dbl(32n, x3), U.U32Nat.dbl(32n, x3)))))), UL.nat_add_assoc(x0, U.U32Nat.dbl(32n, x1), Nat.add(x2, Nat.add(x2, Nat.add(U.U32Nat.dbl(32n, x3), U.U32Nat.dbl(32n, x3)))))) : {_ == Nat.add(Nat.add(x0, Nat.double(x2)), U.U32Nat.dbl(32n, Nat.add(x1, Nat.double(x3)))) : Nat}
119  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(32n, x1), Nat.add(x2, Nat.add(x2, Nat.add(U.U32Nat.dbl(32n, x3), U.U32Nat.dbl(32n, x3))))), Nat.add(x2, Nat.add(U.U32Nat.dbl(32n, x1), Nat.add(x2, Nat.add(U.U32Nat.dbl(32n, x3), U.U32Nat.dbl(32n, x3))))), UL.nat_add_left_comm(U.U32Nat.dbl(32n, x1), x2, Nat.add(x2, Nat.add(U.U32Nat.dbl(32n, x3), U.U32Nat.dbl(32n, x3))))) : {Nat.add(x0, _) == Nat.add(Nat.add(x0, Nat.double(x2)), U.U32Nat.dbl(32n, Nat.add(x1, Nat.double(x3)))) : Nat}
120  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(32n, x1), Nat.add(x2, Nat.add(U.U32Nat.dbl(32n, x3), U.U32Nat.dbl(32n, x3)))), Nat.add(x2, Nat.add(U.U32Nat.dbl(32n, x1), Nat.add(U.U32Nat.dbl(32n, x3), U.U32Nat.dbl(32n, x3)))), UL.nat_add_left_comm(U.U32Nat.dbl(32n, x1), x2, Nat.add(U.U32Nat.dbl(32n, x3), U.U32Nat.dbl(32n, x3)))) : {Nat.add(x0, Nat.add(x2, _)) == Nat.add(Nat.add(x0, Nat.double(x2)), U.U32Nat.dbl(32n, Nat.add(x1, Nat.double(x3)))) : Nat}
121  %Equal.sym(Nat, Nat.add(x2, Nat.add(x2, Nat.add(U.U32Nat.dbl(32n, x1), Nat.add(U.U32Nat.dbl(32n, x3), U.U32Nat.dbl(32n, x3))))), Nat.add(Nat.add(x2, x2), Nat.add(U.U32Nat.dbl(32n, x1), Nat.add(U.U32Nat.dbl(32n, x3), U.U32Nat.dbl(32n, x3)))), Equal.sym(Nat, Nat.add(Nat.add(x2, x2), Nat.add(U.U32Nat.dbl(32n, x1), Nat.add(U.U32Nat.dbl(32n, x3), U.U32Nat.dbl(32n, x3)))), Nat.add(x2, Nat.add(x2, Nat.add(U.U32Nat.dbl(32n, x1), Nat.add(U.U32Nat.dbl(32n, x3), U.U32Nat.dbl(32n, x3))))), UL.nat_add_assoc(x2, x2, Nat.add(U.U32Nat.dbl(32n, x1), Nat.add(U.U32Nat.dbl(32n, x3), U.U32Nat.dbl(32n, x3)))))) : {Nat.add(x0, _) == Nat.add(Nat.add(x0, Nat.double(x2)), U.U32Nat.dbl(32n, Nat.add(x1, Nat.double(x3)))) : Nat}
122  %Equal.sym(Nat, Nat.add(x0, Nat.add(Nat.add(x2, x2), Nat.add(U.U32Nat.dbl(32n, x1), Nat.add(U.U32Nat.dbl(32n, x3), U.U32Nat.dbl(32n, x3))))), Nat.add(Nat.add(x0, Nat.add(x2, x2)), Nat.add(U.U32Nat.dbl(32n, x1), Nat.add(U.U32Nat.dbl(32n, x3), U.U32Nat.dbl(32n, x3)))), Equal.sym(Nat, Nat.add(Nat.add(x0, Nat.add(x2, x2)), Nat.add(U.U32Nat.dbl(32n, x1), Nat.add(U.U32Nat.dbl(32n, x3), U.U32Nat.dbl(32n, x3)))), Nat.add(x0, Nat.add(Nat.add(x2, x2), Nat.add(U.U32Nat.dbl(32n, x1), Nat.add(U.U32Nat.dbl(32n, x3), U.U32Nat.dbl(32n, x3))))), UL.nat_add_assoc(x0, Nat.add(x2, x2), Nat.add(U.U32Nat.dbl(32n, x1), Nat.add(U.U32Nat.dbl(32n, x3), U.U32Nat.dbl(32n, x3)))))) : {_ == Nat.add(Nat.add(x0, Nat.double(x2)), U.U32Nat.dbl(32n, Nat.add(x1, Nat.double(x3)))) : Nat}
123  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(32n, x3), U.U32Nat.dbl(32n, x3)), U.U32Nat.dbl(32n, Nat.add(x3, x3)), Equal.sym(Nat, U.U32Nat.dbl(32n, Nat.add(x3, x3)), Nat.add(U.U32Nat.dbl(32n, x3), U.U32Nat.dbl(32n, x3)), UL.dbl_add(32n, x3, x3))) : {Nat.add(Nat.add(x0, Nat.add(x2, x2)), Nat.add(U.U32Nat.dbl(32n, x1), _)) == Nat.add(Nat.add(x0, Nat.double(x2)), U.U32Nat.dbl(32n, Nat.add(x1, Nat.double(x3)))) : Nat}
124  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(32n, x1), U.U32Nat.dbl(32n, Nat.add(x3, x3))), U.U32Nat.dbl(32n, Nat.add(x1, Nat.add(x3, x3))), Equal.sym(Nat, U.U32Nat.dbl(32n, Nat.add(x1, Nat.add(x3, x3))), Nat.add(U.U32Nat.dbl(32n, x1), U.U32Nat.dbl(32n, Nat.add(x3, x3))), UL.dbl_add(32n, x1, Nat.add(x3, x3)))) : {Nat.add(Nat.add(x0, Nat.add(x2, x2)), _) == Nat.add(Nat.add(x0, Nat.double(x2)), U.U32Nat.dbl(32n, Nat.add(x1, Nat.double(x3)))) : Nat}
125  %Equal.sym(Nat, Nat.add(x3, x3), Nat.double(x3), Equal.sym(Nat, Nat.double(x3), Nat.add(x3, x3), UL.nat_double(x3))) : {Nat.add(Nat.add(x0, Nat.add(x2, x2)), U.U32Nat.dbl(32n, Nat.add(x1, _))) == Nat.add(Nat.add(x0, Nat.double(x2)), U.U32Nat.dbl(32n, Nat.add(x1, Nat.double(x3)))) : Nat}
126  %Equal.sym(Nat, Nat.add(x2, x2), Nat.double(x2), Equal.sym(Nat, Nat.double(x2), Nat.add(x2, x2), UL.nat_double(x2))) : {Nat.add(Nat.add(x0, _), U.U32Nat.dbl(32n, Nat.add(x1, Nat.double(x3)))) == Nat.add(Nat.add(x0, Nat.double(x2)), U.U32Nat.dbl(32n, Nat.add(x1, Nat.double(x3)))) : Nat}
127  {==}
128
129def Laws.xor_and(a, b):
130  match a b:
131    case W.W64{+ah, +al} W.W64{+bh, +bl}:
132      Equal.trans(Nat, Nat.add(Nat.add(U32.to_nat(U32.xor(al, bl)), U.U32Nat.dbl(32n, U32.to_nat(U32.xor(ah, bh)))), Nat.double(Nat.add(U32.to_nat(U32.and(al, bl)), U.U32Nat.dbl(32n, U32.to_nat(U32.and(ah, bh)))))), Nat.add(Nat.add(U32.to_nat(al), U32.to_nat(bl)), U.U32Nat.dbl(32n, Nat.add(U32.to_nat(ah), U32.to_nat(bh)))), Nat.add(Nat.add(U32.to_nat(al), U.U32Nat.dbl(32n, U32.to_nat(ah))), Nat.add(U32.to_nat(bl), U.U32Nat.dbl(32n, U32.to_nat(bh)))), Equal.trans(Nat, Nat.add(Nat.add(U32.to_nat(U32.xor(al, bl)), U.U32Nat.dbl(32n, U32.to_nat(U32.xor(ah, bh)))), Nat.double(Nat.add(U32.to_nat(U32.and(al, bl)), U.U32Nat.dbl(32n, U32.to_nat(U32.and(ah, bh)))))), Nat.add(Nat.add(U32.to_nat(al), U32.to_nat(bl)), U.U32Nat.dbl(32n, Nat.add(U32.to_nat(U32.xor(ah, bh)), Nat.double(U32.to_nat(U32.and(ah, bh)))))), Nat.add(Nat.add(U32.to_nat(al), U32.to_nat(bl)), U.U32Nat.dbl(32n, Nat.add(U32.to_nat(ah), U32.to_nat(bh)))), Equal.trans(Nat, Nat.add(Nat.add(U32.to_nat(U32.xor(al, bl)), U.U32Nat.dbl(32n, U32.to_nat(U32.xor(ah, bh)))), Nat.double(Nat.add(U32.to_nat(U32.and(al, bl)), U.U32Nat.dbl(32n, U32.to_nat(U32.and(ah, bh)))))), Nat.add(Nat.add(U32.to_nat(U32.xor(al, bl)), Nat.double(U32.to_nat(U32.and(al, bl)))), U.U32Nat.dbl(32n, Nat.add(U32.to_nat(U32.xor(ah, bh)), Nat.double(U32.to_nat(U32.and(ah, bh)))))), Nat.add(Nat.add(U32.to_nat(al), U32.to_nat(bl)), U.U32Nat.dbl(32n, Nat.add(U32.to_nat(U32.xor(ah, bh)), Nat.double(U32.to_nat(U32.and(ah, bh)))))), wr.b2(U32.to_nat(U32.xor(al, bl)), U32.to_nat(U32.xor(ah, bh)), U32.to_nat(U32.and(al, bl)), U32.to_nat(U32.and(ah, bh))), Equal.cong(Nat, Nat, zz => Nat.add(zz, U.U32Nat.dbl(32n, Nat.add(U32.to_nat(U32.xor(ah, bh)), Nat.double(U32.to_nat(U32.and(ah, bh)))))), Nat.add(U32.to_nat(U32.xor(al, bl)), Nat.double(U32.to_nat(U32.and(al, bl)))), Nat.add(U32.to_nat(al), U32.to_nat(bl)), UL.u32_xor_and(al, bl))), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(U32.to_nat(al), U32.to_nat(bl)), U.U32Nat.dbl(32n, zz)), Nat.add(U32.to_nat(U32.xor(ah, bh)), Nat.double(U32.to_nat(U32.and(ah, bh)))), Nat.add(U32.to_nat(ah), U32.to_nat(bh)), UL.u32_xor_and(ah, bh))), wr.b1(U32.to_nat(al), U32.to_nat(bl), U32.to_nat(ah), U32.to_nat(bh)))
133
134def Laws.or_disjoint(a, b, h):
135  Equal.trans(Nat, W.W64.to_nat(W.W64.or(a, b)), Nat.add(W.W64.to_nat(W.W64.zero()), W.W64.to_nat(W.W64.or(a, b))), Nat.add(W.W64.to_nat(a), W.W64.to_nat(b)), {==}, Equal.trans(Nat, Nat.add(W.W64.to_nat(W.W64.zero()), W.W64.to_nat(W.W64.or(a, b))), Nat.add(W.W64.to_nat(W.W64.and(a, b)), W.W64.to_nat(W.W64.or(a, b))), Nat.add(W.W64.to_nat(a), W.W64.to_nat(b)), Equal.cong(W.W64, Nat, zz => Nat.add(W.W64.to_nat(zz), W.W64.to_nat(W.W64.or(a, b))), W.W64.zero(), W.W64.and(a, b), Equal.sym(W.W64, W.W64.and(a, b), W.W64.zero(), h)), Laws.and_or(a, b)))
136
137def wb.lts(x: Nat, y: Nat) -> {Nat.is_lt(x, 1n+y) == Nat.is_le(x, y) : Bool}:
138  Equal.sym(Bool, Nat.is_le(1n+x, 1n+y), Nat.is_lt(x, 1n+y), P.wn.le_succ(x, 1n+y))
139
140# nothing is above the mask of all n bits
141def wb.mlt(+n: Nat, +w: Word(n)) -> {Cmp.is_lt(Word.cmp(n, U.U32Word.mask(n, n), w)) == False{} : Bool}:
142  Equal.trans(Bool, Cmp.is_lt(Word.cmp(n, U.U32Word.mask(n, n), w)), Nat.is_lt(Word.to_nat(n, U.U32Word.mask(n, n)), Word.to_nat(n, w)), False{}, Equal.cong(Cmp, Bool, zz => Cmp.is_lt(zz), Word.cmp(n, U.U32Word.mask(n, n), w), Nat.cmp(Word.to_nat(n, U.U32Word.mask(n, n)), Word.to_nat(n, w)), UL.word_cmp_value(n, U.U32Word.mask(n, n), w)), P.wn.le_not_lt(Word.to_nat(n, w), Word.to_nat(n, U.U32Word.mask(n, n)), Equal.trans(Bool, Nat.is_le(Word.to_nat(n, w), Word.to_nat(n, U.U32Word.mask(n, n))), Nat.is_lt(Word.to_nat(n, w), 1n+Word.to_nat(n, U.U32Word.mask(n, n))), True{}, Equal.sym(Bool, Nat.is_lt(Word.to_nat(n, w), 1n+Word.to_nat(n, U.U32Word.mask(n, n))), Nat.is_le(Word.to_nat(n, w), Word.to_nat(n, U.U32Word.mask(n, n))), wb.lts(Word.to_nat(n, w), Word.to_nat(n, U.U32Word.mask(n, n)))), Equal.trans(Bool, Nat.is_lt(Word.to_nat(n, w), 1n+Word.to_nat(n, U.U32Word.mask(n, n))), Nat.is_lt(Word.to_nat(n, w), U.U32Nat.dbl(n, 1n)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(Word.to_nat(n, w), zz), 1n+Word.to_nat(n, U.U32Word.mask(n, n)), U.U32Nat.dbl(n, 1n), UL.word_mask_value(n, n, UL.nat_le_refl(n))), UL.word_value_lt(n, w)))))
143
144def wb.maxlt(+x: U32) -> {U32.is_lt(4294967295, x) == False{} : Bool}:
145  match x:
146    case U32{+w}:
147      wb.mlt(32n, w)
148
149def wb.sub0(+x: U32) -> {U32.sub(x, 0) == x : U32}:
150  UL.u32_value_eq(U32.sub(x, 0), x, Equal.trans(Nat, U32.to_nat(U32.sub(x, 0)), Nat.sub(U32.to_nat(x), 0n), U32.to_nat(x), UL.u32_sub_value(x, 0, wn.le0(U32.to_nat(x))), wn.sub0(U32.to_nat(x))))
151
152def Laws.not_sub(a):
153  match a:
154    case W.W64{+ah, +al}:
155      %Equal.sym(U32, U32.not(ah), U32.sub(4294967295, ah), UL.u32_not_sub(ah)) : {W.W64{_, U32.not(al)} == W.W64.sub(W.W64.max(), W.W64{ah, al}) : W.W64}
156      %Equal.sym(U32, U32.not(al), U32.sub(4294967295, al), UL.u32_not_sub(al)) : {W.W64{U32.sub(4294967295, ah), _} == W.W64.sub(W.W64.max(), W.W64{ah, al}) : W.W64}
157      Equal.sym(W.W64, W.W64.sub(W.W64.max(), W.W64{ah, al}), W.W64{U32.sub(4294967295, ah), U32.sub(4294967295, al)}, Equal.trans(W.W64, W.W64{U32.sub(U32.sub(4294967295, ah), W.W64.bit(U32.is_lt(4294967295, al))), U32.sub(4294967295, al)}, W.W64{U32.sub(U32.sub(4294967295, ah), W.W64.bit(False{})), U32.sub(4294967295, al)}, W.W64{U32.sub(4294967295, ah), U32.sub(4294967295, al)}, Equal.cong(Bool, W.W64, zz => W.W64{U32.sub(U32.sub(4294967295, ah), W.W64.bit(zz)), U32.sub(4294967295, al)}, U32.is_lt(4294967295, al), False{}, wb.maxlt(al)), Equal.cong(U32, W.W64, zz => W.W64{zz, U32.sub(4294967295, al)}, U32.sub(U32.sub(4294967295, ah), 0), U32.sub(4294967295, ah), wb.sub0(U32.sub(4294967295, ah)))))
158
159# A shift left by one bit
160
161def wr.b3(+x0: Nat, +x1: Nat, +x2: Nat, +x3: Nat) -> {Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, Nat.add(x1, x2))), U.U32Nat.dbl(64n, x3)) == Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x2)), U.U32Nat.dbl(32n, Nat.add(x1, U.U32Nat.dbl(32n, x3)))) : Nat}:
162  %Equal.sym(Nat, U.U32Nat.dbl(32n, Nat.add(x1, x2)), Nat.add(U.U32Nat.dbl(32n, x1), U.U32Nat.dbl(32n, x2)), UL.dbl_add(32n, x1, x2)) : {Nat.add(Nat.add(x0, _), U.U32Nat.dbl(64n, x3)) == Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x2)), U.U32Nat.dbl(32n, Nat.add(x1, U.U32Nat.dbl(32n, x3)))) : Nat}
163  %Equal.sym(Nat, Nat.add(Nat.add(x0, Nat.add(U.U32Nat.dbl(32n, x1), U.U32Nat.dbl(32n, x2))), U.U32Nat.dbl(64n, x3)), Nat.add(x0, Nat.add(Nat.add(U.U32Nat.dbl(32n, x1), U.U32Nat.dbl(32n, x2)), U.U32Nat.dbl(64n, x3))), UL.nat_add_assoc(x0, Nat.add(U.U32Nat.dbl(32n, x1), U.U32Nat.dbl(32n, x2)), U.U32Nat.dbl(64n, x3))) : {_ == Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x2)), U.U32Nat.dbl(32n, Nat.add(x1, U.U32Nat.dbl(32n, x3)))) : Nat}
164  %Equal.sym(Nat, Nat.add(Nat.add(U.U32Nat.dbl(32n, x1), U.U32Nat.dbl(32n, x2)), U.U32Nat.dbl(64n, x3)), Nat.add(U.U32Nat.dbl(32n, x1), Nat.add(U.U32Nat.dbl(32n, x2), U.U32Nat.dbl(64n, x3))), UL.nat_add_assoc(U.U32Nat.dbl(32n, x1), U.U32Nat.dbl(32n, x2), U.U32Nat.dbl(64n, x3))) : {Nat.add(x0, _) == Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x2)), U.U32Nat.dbl(32n, Nat.add(x1, U.U32Nat.dbl(32n, x3)))) : Nat}
165  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(32n, x1), Nat.add(U.U32Nat.dbl(32n, x2), U.U32Nat.dbl(64n, x3))), Nat.add(U.U32Nat.dbl(32n, x2), Nat.add(U.U32Nat.dbl(32n, x1), U.U32Nat.dbl(64n, x3))), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(32n, x2), Nat.add(U.U32Nat.dbl(32n, x1), U.U32Nat.dbl(64n, x3))), Nat.add(U.U32Nat.dbl(32n, x1), Nat.add(U.U32Nat.dbl(32n, x2), U.U32Nat.dbl(64n, x3))), UL.nat_add_left_comm(U.U32Nat.dbl(32n, x2), U.U32Nat.dbl(32n, x1), U.U32Nat.dbl(64n, x3)))) : {Nat.add(x0, _) == Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x2)), U.U32Nat.dbl(32n, Nat.add(x1, U.U32Nat.dbl(32n, x3)))) : Nat}
166  %Equal.sym(Nat, Nat.add(x0, Nat.add(U.U32Nat.dbl(32n, x2), Nat.add(U.U32Nat.dbl(32n, x1), U.U32Nat.dbl(64n, x3)))), Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x2)), Nat.add(U.U32Nat.dbl(32n, x1), U.U32Nat.dbl(64n, x3))), Equal.sym(Nat, Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x2)), Nat.add(U.U32Nat.dbl(32n, x1), U.U32Nat.dbl(64n, x3))), Nat.add(x0, Nat.add(U.U32Nat.dbl(32n, x2), Nat.add(U.U32Nat.dbl(32n, x1), U.U32Nat.dbl(64n, x3)))), UL.nat_add_assoc(x0, U.U32Nat.dbl(32n, x2), Nat.add(U.U32Nat.dbl(32n, x1), U.U32Nat.dbl(64n, x3))))) : {_ == Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x2)), U.U32Nat.dbl(32n, Nat.add(x1, U.U32Nat.dbl(32n, x3)))) : Nat}
167  %Equal.sym(Nat, U.U32Nat.dbl(Nat.add(32n, 32n), x3), U.U32Nat.dbl(32n, U.U32Nat.dbl(32n, x3)), Equal.sym(Nat, U.U32Nat.dbl(32n, U.U32Nat.dbl(32n, x3)), U.U32Nat.dbl(Nat.add(32n, 32n), x3), UL.dbl_dbl(32n, 32n, x3))) : {Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x2)), Nat.add(U.U32Nat.dbl(32n, x1), _)) == Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x2)), U.U32Nat.dbl(32n, Nat.add(x1, U.U32Nat.dbl(32n, x3)))) : Nat}
168  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(32n, x1), U.U32Nat.dbl(32n, U.U32Nat.dbl(32n, x3))), U.U32Nat.dbl(32n, Nat.add(x1, U.U32Nat.dbl(32n, x3))), Equal.sym(Nat, U.U32Nat.dbl(32n, Nat.add(x1, U.U32Nat.dbl(32n, x3))), Nat.add(U.U32Nat.dbl(32n, x1), U.U32Nat.dbl(32n, U.U32Nat.dbl(32n, x3))), UL.dbl_add(32n, x1, U.U32Nat.dbl(32n, x3)))) : {Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x2)), _) == Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x2)), U.U32Nat.dbl(32n, Nat.add(x1, U.U32Nat.dbl(32n, x3)))) : Nat}
169  {==}
170
171def wr.b4(+x0: Nat, +x1: Nat) -> {Nat.add(Nat.double(x0), U.U32Nat.dbl(32n, Nat.double(x1))) == Nat.double(Nat.add(x0, U.U32Nat.dbl(32n, x1))) : Nat}:
172  %Equal.sym(Nat, Nat.double(x0), Nat.add(x0, x0), UL.nat_double(x0)) : {Nat.add(_, U.U32Nat.dbl(32n, Nat.double(x1))) == Nat.double(Nat.add(x0, U.U32Nat.dbl(32n, x1))) : Nat}
173  %Equal.sym(Nat, Nat.double(x1), Nat.add(x1, x1), UL.nat_double(x1)) : {Nat.add(Nat.add(x0, x0), U.U32Nat.dbl(32n, _)) == Nat.double(Nat.add(x0, U.U32Nat.dbl(32n, x1))) : Nat}
174  %Equal.sym(Nat, U.U32Nat.dbl(32n, Nat.add(x1, x1)), Nat.add(U.U32Nat.dbl(32n, x1), U.U32Nat.dbl(32n, x1)), UL.dbl_add(32n, x1, x1)) : {Nat.add(Nat.add(x0, x0), _) == Nat.double(Nat.add(x0, U.U32Nat.dbl(32n, x1))) : Nat}
175  %Equal.sym(Nat, Nat.add(Nat.add(x0, x0), Nat.add(U.U32Nat.dbl(32n, x1), U.U32Nat.dbl(32n, x1))), Nat.add(x0, Nat.add(x0, Nat.add(U.U32Nat.dbl(32n, x1), U.U32Nat.dbl(32n, x1)))), UL.nat_add_assoc(x0, x0, Nat.add(U.U32Nat.dbl(32n, x1), U.U32Nat.dbl(32n, x1)))) : {_ == Nat.double(Nat.add(x0, U.U32Nat.dbl(32n, x1))) : Nat}
176  %Equal.sym(Nat, Nat.add(x0, Nat.add(U.U32Nat.dbl(32n, x1), U.U32Nat.dbl(32n, x1))), Nat.add(U.U32Nat.dbl(32n, x1), Nat.add(x0, U.U32Nat.dbl(32n, x1))), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(32n, x1), Nat.add(x0, U.U32Nat.dbl(32n, x1))), Nat.add(x0, Nat.add(U.U32Nat.dbl(32n, x1), U.U32Nat.dbl(32n, x1))), UL.nat_add_left_comm(U.U32Nat.dbl(32n, x1), x0, U.U32Nat.dbl(32n, x1)))) : {Nat.add(x0, _) == Nat.double(Nat.add(x0, U.U32Nat.dbl(32n, x1))) : Nat}
177  %Equal.sym(Nat, Nat.add(x0, Nat.add(U.U32Nat.dbl(32n, x1), Nat.add(x0, U.U32Nat.dbl(32n, x1)))), Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x1)), Nat.add(x0, U.U32Nat.dbl(32n, x1))), Equal.sym(Nat, Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x1)), Nat.add(x0, U.U32Nat.dbl(32n, x1))), Nat.add(x0, Nat.add(U.U32Nat.dbl(32n, x1), Nat.add(x0, U.U32Nat.dbl(32n, x1)))), UL.nat_add_assoc(x0, U.U32Nat.dbl(32n, x1), Nat.add(x0, U.U32Nat.dbl(32n, x1))))) : {_ == Nat.double(Nat.add(x0, U.U32Nat.dbl(32n, x1))) : Nat}
178  %Equal.sym(Nat, Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x1)), Nat.add(x0, U.U32Nat.dbl(32n, x1))), Nat.double(Nat.add(x0, U.U32Nat.dbl(32n, x1))), Equal.sym(Nat, Nat.double(Nat.add(x0, U.U32Nat.dbl(32n, x1))), Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x1)), Nat.add(x0, U.U32Nat.dbl(32n, x1))), UL.nat_double(Nat.add(x0, U.U32Nat.dbl(32n, x1))))) : {_ == Nat.double(Nat.add(x0, U.U32Nat.dbl(32n, x1))) : Nat}
179  {==}
180
181def Laws.shl_one_wrap(a):
182  match a:
183    case W.W64{+h, +l}:
184      Equal.trans(Nat, Nat.add(Nat.add(U32.to_nat(U32.shln(l, 1n)), U.U32Nat.dbl(32n, U32.to_nat(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n))))), U.U32Nat.dbl(64n, U32.to_nat(U32.shrn(h, 31n)))), Nat.add(Nat.double(U32.to_nat(l)), U.U32Nat.dbl(32n, Nat.double(U32.to_nat(h)))), Nat.double(Nat.add(U32.to_nat(l), U.U32Nat.dbl(32n, U32.to_nat(h)))), Equal.trans(Nat, Nat.add(Nat.add(U32.to_nat(U32.shln(l, 1n)), U.U32Nat.dbl(32n, U32.to_nat(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n))))), U.U32Nat.dbl(64n, U32.to_nat(U32.shrn(h, 31n)))), Nat.add(Nat.double(U32.to_nat(l)), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.low(32n, Nat.double(U32.to_nat(h))), U.U32Nat.dbl(32n, U.U32Nat.high(32n, Nat.double(U32.to_nat(h))))))), Nat.add(Nat.double(U32.to_nat(l)), U.U32Nat.dbl(32n, Nat.double(U32.to_nat(h)))), Equal.trans(Nat, Nat.add(Nat.add(U32.to_nat(U32.shln(l, 1n)), U.U32Nat.dbl(32n, U32.to_nat(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n))))), U.U32Nat.dbl(64n, U32.to_nat(U32.shrn(h, 31n)))), Nat.add(Nat.add(U.U32Nat.low(32n, Nat.double(U32.to_nat(l))), U.U32Nat.dbl(32n, U.U32Nat.high(32n, Nat.double(U32.to_nat(l))))), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.low(32n, Nat.double(U32.to_nat(h))), U.U32Nat.dbl(32n, U.U32Nat.high(32n, Nat.double(U32.to_nat(h))))))), Nat.add(Nat.double(U32.to_nat(l)), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.low(32n, Nat.double(U32.to_nat(h))), U.U32Nat.dbl(32n, U.U32Nat.high(32n, Nat.double(U32.to_nat(h))))))), Equal.trans(Nat, Nat.add(Nat.add(U32.to_nat(U32.shln(l, 1n)), U.U32Nat.dbl(32n, U32.to_nat(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n))))), U.U32Nat.dbl(64n, U32.to_nat(U32.shrn(h, 31n)))), Nat.add(Nat.add(U.U32Nat.low(32n, Nat.double(U32.to_nat(l))), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.low(32n, Nat.double(U32.to_nat(h))), U.U32Nat.high(32n, Nat.double(U32.to_nat(l)))))), U.U32Nat.dbl(64n, U.U32Nat.high(32n, Nat.double(U32.to_nat(h))))), Nat.add(Nat.add(U.U32Nat.low(32n, Nat.double(U32.to_nat(l))), U.U32Nat.dbl(32n, U.U32Nat.high(32n, Nat.double(U32.to_nat(l))))), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.low(32n, Nat.double(U32.to_nat(h))), U.U32Nat.dbl(32n, U.U32Nat.high(32n, Nat.double(U32.to_nat(h))))))), Equal.trans(Nat, Nat.add(Nat.add(U32.to_nat(U32.shln(l, 1n)), U.U32Nat.dbl(32n, U32.to_nat(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n))))), U.U32Nat.dbl(64n, U32.to_nat(U32.shrn(h, 31n)))), Nat.add(Nat.add(U.U32Nat.low(32n, Nat.double(U32.to_nat(l))), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.low(32n, Nat.double(U32.to_nat(h))), U.U32Nat.high(32n, Nat.double(U32.to_nat(l)))))), U.U32Nat.dbl(64n, U.U32Nat.high(31n, U32.to_nat(h)))), Nat.add(Nat.add(U.U32Nat.low(32n, Nat.double(U32.to_nat(l))), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.low(32n, Nat.double(U32.to_nat(h))), U.U32Nat.high(32n, Nat.double(U32.to_nat(l)))))), U.U32Nat.dbl(64n, U.U32Nat.high(32n, Nat.double(U32.to_nat(h))))), Equal.trans(Nat, Nat.add(Nat.add(U32.to_nat(U32.shln(l, 1n)), U.U32Nat.dbl(32n, U32.to_nat(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n))))), U.U32Nat.dbl(64n, U32.to_nat(U32.shrn(h, 31n)))), Nat.add(Nat.add(U.U32Nat.low(32n, Nat.double(U32.to_nat(l))), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.low(32n, Nat.double(U32.to_nat(h))), U.U32Nat.high(31n, U32.to_nat(l))))), U.U32Nat.dbl(64n, U.U32Nat.high(31n, U32.to_nat(h)))), Nat.add(Nat.add(U.U32Nat.low(32n, Nat.double(U32.to_nat(l))), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.low(32n, Nat.double(U32.to_nat(h))), U.U32Nat.high(32n, Nat.double(U32.to_nat(l)))))), U.U32Nat.dbl(64n, U.U32Nat.high(31n, U32.to_nat(h)))), Equal.trans(Nat, Nat.add(Nat.add(U32.to_nat(U32.shln(l, 1n)), U.U32Nat.dbl(32n, U32.to_nat(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n))))), U.U32Nat.dbl(64n, U32.to_nat(U32.shrn(h, 31n)))), Nat.add(Nat.add(U.U32Nat.low(32n, Nat.double(U32.to_nat(l))), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.low(32n, Nat.double(U32.to_nat(h))), U.U32Nat.high(31n, U32.to_nat(l))))), U.U32Nat.dbl(64n, U32.to_nat(U32.shrn(h, 31n)))), Nat.add(Nat.add(U.U32Nat.low(32n, Nat.double(U32.to_nat(l))), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.low(32n, Nat.double(U32.to_nat(h))), U.U32Nat.high(31n, U32.to_nat(l))))), U.U32Nat.dbl(64n, U.U32Nat.high(31n, U32.to_nat(h)))), Equal.trans(Nat, Nat.add(Nat.add(U32.to_nat(U32.shln(l, 1n)), U.U32Nat.dbl(32n, U32.to_nat(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n))))), U.U32Nat.dbl(64n, U32.to_nat(U32.shrn(h, 31n)))), Nat.add(Nat.add(U.U32Nat.low(32n, Nat.double(U32.to_nat(l))), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.low(32n, Nat.double(U32.to_nat(h))), U32.to_nat(U32.shrn(l, 31n))))), U.U32Nat.dbl(64n, U32.to_nat(U32.shrn(h, 31n)))), Nat.add(Nat.add(U.U32Nat.low(32n, Nat.double(U32.to_nat(l))), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.low(32n, Nat.double(U32.to_nat(h))), U.U32Nat.high(31n, U32.to_nat(l))))), U.U32Nat.dbl(64n, U32.to_nat(U32.shrn(h, 31n)))), Equal.trans(Nat, Nat.add(Nat.add(U32.to_nat(U32.shln(l, 1n)), U.U32Nat.dbl(32n, U32.to_nat(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n))))), U.U32Nat.dbl(64n, U32.to_nat(U32.shrn(h, 31n)))), Nat.add(Nat.add(U.U32Nat.low(32n, U.U32Nat.dbl(1n, U32.to_nat(l))), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.low(32n, U.U32Nat.dbl(1n, U32.to_nat(h))), U32.to_nat(U32.shrn(l, 31n))))), U.U32Nat.dbl(64n, U32.to_nat(U32.shrn(h, 31n)))), Nat.add(Nat.add(U.U32Nat.low(32n, Nat.double(U32.to_nat(l))), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.low(32n, Nat.double(U32.to_nat(h))), U32.to_nat(U32.shrn(l, 31n))))), U.U32Nat.dbl(64n, U32.to_nat(U32.shrn(h, 31n)))), Equal.trans(Nat, Nat.add(Nat.add(U32.to_nat(U32.shln(l, 1n)), U.U32Nat.dbl(32n, U32.to_nat(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n))))), U.U32Nat.dbl(64n, U32.to_nat(U32.shrn(h, 31n)))), Nat.add(Nat.add(U.U32Nat.low(32n, U.U32Nat.dbl(1n, U32.to_nat(l))), U.U32Nat.dbl(32n, Nat.add(U32.to_nat(U32.shln(h, 1n)), U32.to_nat(U32.shrn(l, 31n))))), U.U32Nat.dbl(64n, U32.to_nat(U32.shrn(h, 31n)))), Nat.add(Nat.add(U.U32Nat.low(32n, U.U32Nat.dbl(1n, U32.to_nat(l))), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.low(32n, U.U32Nat.dbl(1n, U32.to_nat(h))), U32.to_nat(U32.shrn(l, 31n))))), U.U32Nat.dbl(64n, U32.to_nat(U32.shrn(h, 31n)))), Equal.trans(Nat, Nat.add(Nat.add(U32.to_nat(U32.shln(l, 1n)), U.U32Nat.dbl(32n, U32.to_nat(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n))))), U.U32Nat.dbl(64n, U32.to_nat(U32.shrn(h, 31n)))), Nat.add(Nat.add(U32.to_nat(U32.shln(l, 1n)), U.U32Nat.dbl(32n, Nat.add(U32.to_nat(U32.shln(h, 1n)), U32.to_nat(U32.shrn(l, 31n))))), U.U32Nat.dbl(64n, U32.to_nat(U32.shrn(h, 31n)))), Nat.add(Nat.add(U.U32Nat.low(32n, U.U32Nat.dbl(1n, U32.to_nat(l))), U.U32Nat.dbl(32n, Nat.add(U32.to_nat(U32.shln(h, 1n)), U32.to_nat(U32.shrn(l, 31n))))), U.U32Nat.dbl(64n, U32.to_nat(U32.shrn(h, 31n)))), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(U32.to_nat(U32.shln(l, 1n)), U.U32Nat.dbl(32n, zz)), U.U32Nat.dbl(64n, U32.to_nat(U32.shrn(h, 31n)))), U32.to_nat(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n))), Nat.add(U32.to_nat(U32.shln(h, 1n)), U32.to_nat(U32.shrn(l, 31n))), UL.u32_or_split(U32.shln(h, 1n), U32.shrn(l, 31n), 1n, U.U32Nat.low(31n, U32.to_nat(h)), Equal.trans(Nat, U32.to_nat(U32.shln(h, 1n)), Nat.double(U.U32Nat.low(31n, U32.to_nat(h))), U.U32Nat.dbl(1n, U.U32Nat.low(31n, U32.to_nat(h))), Equal.trans(Nat, U32.to_nat(U32.shln(h, 1n)), U.U32Nat.low(32n, Nat.double(U32.to_nat(h))), Nat.double(U.U32Nat.low(31n, U32.to_nat(h))), Equal.trans(Nat, U32.to_nat(U32.shln(h, 1n)), U.U32Nat.low(32n, U.U32Nat.dbl(1n, U32.to_nat(h))), U.U32Nat.low(32n, Nat.double(U32.to_nat(h))), UL.u32_shln_low(h, 1n), {==}), UL.low_double(31n, U32.to_nat(h))), {==}), Equal.trans(Bool, Nat.is_lt(U32.to_nat(U32.shrn(l, 31n)), U.U32Nat.dbl(1n, 1n)), Nat.is_lt(U.U32Nat.high(31n, U32.to_nat(l)), U.U32Nat.dbl(1n, 1n)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(zz, U.U32Nat.dbl(1n, 1n)), U32.to_nat(U32.shrn(l, 31n)), U.U32Nat.high(31n, U32.to_nat(l)), Equal.sym(Nat, U.U32Nat.high(31n, U32.to_nat(l)), U32.to_nat(U32.shrn(l, 31n)), Equal.sym(Nat, U32.to_nat(U32.shrn(l, 31n)), U.U32Nat.high(31n, U32.to_nat(l)), UL.u32_shrn_value(l, 31n)))), UL.high_lt(31n, 1n, 32n, U32.to_nat(l), {==}, wu.lt(l))))), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(zz, U.U32Nat.dbl(32n, Nat.add(U32.to_nat(U32.shln(h, 1n)), U32.to_nat(U32.shrn(l, 31n))))), U.U32Nat.dbl(64n, U32.to_nat(U32.shrn(h, 31n)))), U32.to_nat(U32.shln(l, 1n)), U.U32Nat.low(32n, U.U32Nat.dbl(1n, U32.to_nat(l))), UL.u32_shln_low(l, 1n))), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(U.U32Nat.low(32n, U.U32Nat.dbl(1n, U32.to_nat(l))), U.U32Nat.dbl(32n, Nat.add(zz, U32.to_nat(U32.shrn(l, 31n))))), U.U32Nat.dbl(64n, U32.to_nat(U32.shrn(h, 31n)))), U32.to_nat(U32.shln(h, 1n)), U.U32Nat.low(32n, U.U32Nat.dbl(1n, U32.to_nat(h))), UL.u32_shln_low(h, 1n))), {==}), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(U.U32Nat.low(32n, Nat.double(U32.to_nat(l))), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.low(32n, Nat.double(U32.to_nat(h))), zz))), U.U32Nat.dbl(64n, U32.to_nat(U32.shrn(h, 31n)))), U32.to_nat(U32.shrn(l, 31n)), U.U32Nat.high(31n, U32.to_nat(l)), UL.u32_shrn_value(l, 31n))), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(U.U32Nat.low(32n, Nat.double(U32.to_nat(l))), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.low(32n, Nat.double(U32.to_nat(h))), U.U32Nat.high(31n, U32.to_nat(l))))), U.U32Nat.dbl(64n, zz)), U32.to_nat(U32.shrn(h, 31n)), U.U32Nat.high(31n, U32.to_nat(h)), UL.u32_shrn_value(h, 31n))), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(U.U32Nat.low(32n, Nat.double(U32.to_nat(l))), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.low(32n, Nat.double(U32.to_nat(h))), zz))), U.U32Nat.dbl(64n, U.U32Nat.high(31n, U32.to_nat(h)))), U.U32Nat.high(31n, U32.to_nat(l)), U.U32Nat.high(32n, Nat.double(U32.to_nat(l))), Equal.sym(Nat, U.U32Nat.high(32n, Nat.double(U32.to_nat(l))), U.U32Nat.high(31n, U32.to_nat(l)), UL.high_double(31n, U32.to_nat(l))))), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(U.U32Nat.low(32n, Nat.double(U32.to_nat(l))), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.low(32n, Nat.double(U32.to_nat(h))), U.U32Nat.high(32n, Nat.double(U32.to_nat(l)))))), U.U32Nat.dbl(64n, zz)), U.U32Nat.high(31n, U32.to_nat(h)), U.U32Nat.high(32n, Nat.double(U32.to_nat(h))), Equal.sym(Nat, U.U32Nat.high(32n, Nat.double(U32.to_nat(h))), U.U32Nat.high(31n, U32.to_nat(h)), UL.high_double(31n, U32.to_nat(h))))), wr.b3(U.U32Nat.low(32n, Nat.double(U32.to_nat(l))), U.U32Nat.low(32n, Nat.double(U32.to_nat(h))), U.U32Nat.high(32n, Nat.double(U32.to_nat(l))), U.U32Nat.high(32n, Nat.double(U32.to_nat(h))))), Equal.cong(Nat, Nat, zz => Nat.add(zz, U.U32Nat.dbl(32n, Nat.add(U.U32Nat.low(32n, Nat.double(U32.to_nat(h))), U.U32Nat.dbl(32n, U.U32Nat.high(32n, Nat.double(U32.to_nat(h))))))), Nat.add(U.U32Nat.low(32n, Nat.double(U32.to_nat(l))), U.U32Nat.dbl(32n, U.U32Nat.high(32n, Nat.double(U32.to_nat(l))))), Nat.double(U32.to_nat(l)), UL.low_high(32n, Nat.double(U32.to_nat(l))))), Equal.cong(Nat, Nat, zz => Nat.add(Nat.double(U32.to_nat(l)), U.U32Nat.dbl(32n, zz)), Nat.add(U.U32Nat.low(32n, Nat.double(U32.to_nat(h))), U.U32Nat.dbl(32n, U.U32Nat.high(32n, Nat.double(U32.to_nat(h))))), Nat.double(U32.to_nat(h)), UL.low_high(32n, Nat.double(U32.to_nat(h))))), wr.b4(U32.to_nat(l), U32.to_nat(h)))
185
186def wr.b5(+x0: Nat, +x1: Nat, +x2: Nat) -> {Nat.add(Nat.add(x0, x1), U.U32Nat.dbl(32n, Nat.add(x2, 0n))) == Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x2)), x1) : Nat}:
187  %Equal.sym(Nat, Nat.add(x2, 0n), x2, UL.nat_add_zero(x2)) : {Nat.add(Nat.add(x0, x1), U.U32Nat.dbl(32n, _)) == Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x2)), x1) : Nat}
188  %Equal.sym(Nat, Nat.add(Nat.add(x0, x1), U.U32Nat.dbl(32n, x2)), Nat.add(x0, Nat.add(x1, U.U32Nat.dbl(32n, x2))), UL.nat_add_assoc(x0, x1, U.U32Nat.dbl(32n, x2))) : {_ == Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x2)), x1) : Nat}
189  %Equal.sym(Nat, Nat.add(x1, U.U32Nat.dbl(32n, x2)), Nat.add(U.U32Nat.dbl(32n, x2), x1), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(32n, x2), x1), Nat.add(x1, U.U32Nat.dbl(32n, x2)), UL.nat_add_comm(U.U32Nat.dbl(32n, x2), x1))) : {Nat.add(x0, _) == Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x2)), x1) : Nat}
190  %Equal.sym(Nat, Nat.add(x0, Nat.add(U.U32Nat.dbl(32n, x2), x1)), Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x2)), x1), Equal.sym(Nat, Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x2)), x1), Nat.add(x0, Nat.add(U.U32Nat.dbl(32n, x2), x1)), UL.nat_add_assoc(x0, U.U32Nat.dbl(32n, x2), x1))) : {_ == Nat.add(Nat.add(x0, U.U32Nat.dbl(32n, x2)), x1) : Nat}
191  {==}
192
193def wb.or_bit(+x: W.W64, +c: U32, +hc: {Nat.is_lt(U32.to_nat(c), U.U32Nat.dbl(1n, 1n)) == True{} : Bool}) -> {W.W64.to_nat(W.W64.or(W.W64.shl(x, 1n), W.W64.from_u32(c))) == Nat.add(W.W64.to_nat(W.W64.shl(x, 1n)), U32.to_nat(c)) : Nat}:
194  match x:
195    case W.W64{+h, +l}:
196      Equal.trans(Nat, Nat.add(U32.to_nat(U32.or(U32.shln(l, 1n), c)), U.U32Nat.dbl(32n, U32.to_nat(U32.or(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n)), 0)))), Nat.add(Nat.add(U32.to_nat(U32.shln(l, 1n)), U32.to_nat(c)), U.U32Nat.dbl(32n, Nat.add(U32.to_nat(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n))), 0n))), Nat.add(Nat.add(U32.to_nat(U32.shln(l, 1n)), U.U32Nat.dbl(32n, U32.to_nat(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n))))), U32.to_nat(c)), Equal.trans(Nat, Nat.add(U32.to_nat(U32.or(U32.shln(l, 1n), c)), U.U32Nat.dbl(32n, U32.to_nat(U32.or(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n)), 0)))), Nat.add(Nat.add(U32.to_nat(U32.shln(l, 1n)), U32.to_nat(c)), U.U32Nat.dbl(32n, U32.to_nat(U32.or(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n)), 0)))), Nat.add(Nat.add(U32.to_nat(U32.shln(l, 1n)), U32.to_nat(c)), U.U32Nat.dbl(32n, Nat.add(U32.to_nat(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n))), 0n))), Equal.cong(Nat, Nat, zz => Nat.add(zz, U.U32Nat.dbl(32n, U32.to_nat(U32.or(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n)), 0)))), U32.to_nat(U32.or(U32.shln(l, 1n), c)), Nat.add(U32.to_nat(U32.shln(l, 1n)), U32.to_nat(c)), UL.u32_or_split(U32.shln(l, 1n), c, 1n, U.U32Nat.low(31n, U32.to_nat(l)), Equal.trans(Nat, U32.to_nat(U32.shln(l, 1n)), Nat.double(U.U32Nat.low(31n, U32.to_nat(l))), U.U32Nat.dbl(1n, U.U32Nat.low(31n, U32.to_nat(l))), Equal.trans(Nat, U32.to_nat(U32.shln(l, 1n)), U.U32Nat.low(32n, Nat.double(U32.to_nat(l))), Nat.double(U.U32Nat.low(31n, U32.to_nat(l))), Equal.trans(Nat, U32.to_nat(U32.shln(l, 1n)), U.U32Nat.low(32n, U.U32Nat.dbl(1n, U32.to_nat(l))), U.U32Nat.low(32n, Nat.double(U32.to_nat(l))), UL.u32_shln_low(l, 1n), {==}), UL.low_double(31n, U32.to_nat(l))), {==}), hc)), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(U32.to_nat(U32.shln(l, 1n)), U32.to_nat(c)), U.U32Nat.dbl(32n, zz)), U32.to_nat(U32.or(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n)), 0)), Nat.add(U32.to_nat(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n))), 0n), Equal.trans(Nat, U32.to_nat(U32.or(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n)), 0)), Nat.add(U32.to_nat(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n))), U32.to_nat(0)), Nat.add(U32.to_nat(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n))), 0n), UL.u32_or_split(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n)), 0, 0n, U32.to_nat(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n))), {==}, {==}), {==}))), wr.b5(U32.to_nat(U32.shln(l, 1n)), U32.to_nat(c), U32.to_nat(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n)))))