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. 3 import Base 4 import bend-osdev-u32@0.1.0.0/u32.bend as U 5 import bend-osdev-u32@0.1.0.0/LAWS.bend as UL 6 import bend-osdev-u32@0.1.0.0/PROOF.bend as UP 7 import ./word64.bend as W 8 import ./LAWS.bend as WB 9 import ./PROOF.bend as WBP 10 import ./proof_value.bend as P 11 import ./proof_shift.bend as PS 12 import ./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 17 def wu.ve(+w: Word(32n)) -> {Word.to_nat(32n, w) == U32.to_nat(U32{w}) : Nat}: 18 {==} 19 20 def 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 26 def 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 31 def 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 34 def 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 40 def wn.sub0(x: Nat) -> {Nat.sub(x, 0n) == x : Nat}: 41 match x: 42 case 0n: 43 {==} 44 case 1n+ +p: 45 {==} 46 47 def wn.le0(x: Nat) -> {Nat.is_le(0n, x) == True{} : Bool}: 48 match x: 49 case 0n: 50 {==} 51 case 1n+ +p: 52 {==} 53 54 def wn.ft(e: {False{} == True{} : Bool}) -> Empty: 55 P.wn.ft(e) 56 57 def wn.tf(e: {True{} == False{} : Bool}) -> Empty: 58 PS.ns.tf(e) 59 60 def 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 69 def 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 74 def 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 81 def 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 88 def 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 95 def 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 102 def 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 109 def 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( 113 114 def 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 129 def 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 133 134 def 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 137 def 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 141 def 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 144 def wb.maxlt(+x: U32) -> {U32.is_lt(4294967295, x) == False{} : Bool}: 145 match x: 146 case U32{+w}: 147 wb.mlt(32n, w) 148 149 def 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 152 def 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 161 def 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 171 def 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 181 def 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.d 185 186 def 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 193 def 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