1 import Base 2 import ../../../spec/lib/common.bend as C 3 import ../../../spec/math/instances.bend as SI 4 import ../../../spec/math/generic.bend as SG 5 import ../../../src/math/instances.bend as I 6 import ../../../src/math/num.bend as NM 7 import ../../lib/nat.bend as N 8 import ../../lib/u32.bend as U 9 import ../../lib/u32div.bend as UD 10 import ../../lib/u32half.bend as UH 11 import ../../lib/u32alg.bend as A 12 import ../../lib/word.bend as WD 13 import ../../lib/logic.bend as L 14 import ../../lib/lemmas/spec/numeric.bend as S 15 import ../u64/u64.bend as P64 16 import ./u32.bend as U32P 17 import ./width.bend as WW 18 import ../u64/u64div.bend as PD 19 import ../natural/arith.bend as NA 20 import ../../lib/arith.bend as AR 21 import ./w64mul.bend as W64M 22 import ./w64div.bend as W64D 23 import ./w64sqrt.bend as W64S 24 import ../../../src/math/w64.bend as X 25 import ../../../spec/math/w64.bend as SW 26 27 # The U32 instance (src/math/instances.bend) against spec/math/instances.bend: 28 # the model (value below 2^32, round trip) and the laws of every operation 29 # and test that do not go through w64.bend (those are in u32w64.bend). 30 # Width 32 stays symbolic (k with k == 32) inside the proofs: the checker 31 # cannot expand 2^32. 32 33 def v(+x: U32) -> Nat: 34 U32.to_nat(x) 35 36 # ---- the model ---- 37 38 def vb_k(+k: Nat, +hk: {k == 32n : Nat}, +x: U32) -> {C.fits(k, v(x)) == True{} : Bool}: 39 %Equal.sym(Bool, C.fits(k, v(x)), Nat.is_lt(v(x), C.pow2(k)), WW.fits_lt(k, v(x))) : {_ == True{} : Bool} 40 U32P.val_lt(1n, {==}, k, hk, x) 41 42 # every U32 value fits 32 bits 43 def vb(+x: U32) -> {C.fits(32n, v(x)) == True{} : Bool}: 44 vb_k(32n, {==}, x) 45 46 def lt_k(+k: Nat, +n: Nat, +h: {C.fits(k, n) == True{} : Bool}) -> {Nat.is_lt(n, C.pow2(k)) == True{} : Bool}: 47 %WW.fits_lt(k, n) : {_ == True{} : Bool} 48 h 49 50 def vo_k(+k: Nat, +hk: {k == 32n : Nat}, +n: Nat, +h: {C.fits(k, n) == True{} : Bool}) -> {v(U32.from_nat(n)) == n : Nat}: 51 U.to_nat_from_nat(n, k, U32P.le_k(k, hk), lt_k(k, n, h)) 52 53 # a value that fits is the value of its U32 54 def vo(+n: Nat, +h: {C.fits(32n, n) == True{} : Bool}) -> {v(U32.from_nat(n)) == n : Nat}: 55 vo_k(32n, {==}, n, h) 56 57 def rt(+x: U32) -> {U32.from_nat(v(x)) == x : U32}: 58 U32P.round_trip(x) 59 60 # ---- tests ---- 61 62 def true_ne_false(+h: {True{} == False{} : Bool}) -> Empty: 63 U32P.true_ne_false(h) 64 65 def is_zero_c(+a: U32, +c: Bool, +hc: {U32.is_zero(a) == c : Bool}, +n: Nat, +hn: {v(a) == n : Nat}) -> {c == Nat.is_eq(v(a), 0n) : Bool}: 66 match c: 67 case True{}: 68 %Equal.sym(U32, a, 0, A.eq_of(a, 0, hc)) : {True{} == Nat.is_eq(v(_), 0n) : Bool} 69 {==} 70 case False{}: 71 match n: 72 case 0n: 73 +hz = L.subst(U32, z => {U32.is_zero(z) == True{} : Bool}, 0, a, Equal.sym(U32, a, 0, U.injective(a, 0, hn)), {==}) 74 Empty.absurd({False{} == Nat.is_eq(v(a), 0n) : Bool}, true_ne_false(Equal.trans(Bool, True{}, U32.is_zero(a), False{}, Equal.sym(Bool, U32.is_zero(a), True{}, hz), hc))) 75 case 1n+ +p: 76 %Equal.sym(Nat, v(a), 1n+p, hn) : {False{} == Nat.is_eq(_, 0n) : Bool} 77 {==} 78 79 # U32.is_zero is the zero test on the value 80 def zero_nat(+a: U32) -> {U32.is_zero(a) == Nat.is_eq(v(a), 0n) : Bool}: 81 is_zero_c(a, U32.is_zero(a), {==}, v(a), {==}) 82 83 # U32 equality is equality of the values 84 def eq_c(+x: U32, +y: U32, +c: Bool, +hc: {U32.is_eq(x, y) == c : Bool}, +d: Bool, +hd: {Nat.is_eq(v(x), v(y)) == d : Bool}) -> {c == d : Bool}: 85 match c d: 86 case True{} True{}: 87 {==} 88 case False{} False{}: 89 {==} 90 case True{} False{}: 91 +e = A.eq_of(x, y, hc) 92 +hd2 = L.subst(U32, z => {Nat.is_eq(v(x), v(z)) == False{} : Bool}, y, x, Equal.sym(U32, x, y, e), hd) 93 Empty.absurd({True{} == False{} : Bool}, true_ne_false(Equal.trans(Bool, True{}, Nat.is_eq(v(x), v(x)), False{}, Equal.sym(Bool, Nat.is_eq(v(x), v(x)), True{}, N.is_eq_refl(v(x))), hd2))) 94 case False{} True{}: 95 +e = U.injective(x, y, N.eq_from_is_eq(v(x), v(y), hd)) 96 +hc2 = L.subst(U32, z => {U32.is_eq(x, z) == False{} : Bool}, y, x, Equal.sym(U32, x, y, e), hc) 97 Empty.absurd({False{} == True{} : Bool}, true_ne_false(Equal.trans(Bool, True{}, U32.is_eq(x, x), False{}, Equal.sym(Bool, U32.is_eq(x, x), True{}, A.eq_refl(x)), hc2))) 98 99 def eq_nat(+x: U32, +y: U32) -> {U32.is_eq(x, y) == Nat.is_eq(v(x), v(y)) : Bool}: 100 eq_c(x, y, U32.is_eq(x, y), {==}, Nat.is_eq(v(x), v(y)), {==}) 101 102 # the carry of an addition is "the sum does not fit" 103 def carry_fits(+k: Nat, +s: Nat, +n: Nat, +c: Bool, +e: {Nat.add(s, WD.sc(k, S.bit_value(c))) == n : Nat}, +hs: {Nat.is_lt(s, C.pow2(k)) == True{} : Bool}) -> {c == Bool.not(C.fits(k, n)) : Bool}: 104 match c: 105 case False{}: 106 %Equal.sym(Bool, C.fits(k, n), Nat.is_lt(n, C.pow2(k)), WW.fits_lt(k, n)) : {False{} == Bool.not(_) : Bool} 107 %e : {False{} == Bool.not(Nat.is_lt(_, C.pow2(k))) : Bool} 108 %Equal.sym(Nat, WD.sc(k, 0n), 0n, A.sc_zero(k)) : {False{} == Bool.not(Nat.is_lt(Nat.add(s, _), C.pow2(k))) : Bool} 109 %Equal.sym(Nat, Nat.add(s, 0n), s, N.add_zero(s)) : {False{} == Bool.not(Nat.is_lt(_, C.pow2(k))) : Bool} 110 %Equal.sym(Bool, Nat.is_lt(s, C.pow2(k)), True{}, hs) : {False{} == Bool.not(_) : Bool} 111 {==} 112 case True{}: 113 %Equal.sym(Bool, C.fits(k, n), Nat.is_lt(n, C.pow2(k)), WW.fits_lt(k, n)) : {True{} == Bool.not(_) : Bool} 114 %e : {True{} == Bool.not(Nat.is_lt(_, C.pow2(k))) : Bool} 115 %U.pow2_scale(k) : {True{} == Bool.not(Nat.is_lt(Nat.add(s, _), C.pow2(k))) : Bool} 116 +le = L.subst(Nat, z => {Nat.is_le(C.pow2(k), z) == True{} : Bool}, Nat.add(C.pow2(k), s), Nat.add(s, C.pow2(k)), N.add_comm(C.pow2(k), s), N.le_add_right(C.pow2(k), s)) 117 %Equal.sym(Bool, Nat.is_lt(Nat.add(s, C.pow2(k)), C.pow2(k)), False{}, N.le_not_lt(Nat.add(s, C.pow2(k)), C.pow2(k), le)) : {True{} == Bool.not(_) : Bool} 118 {==} 119 120 # ---- the instance laws of spec/math/instances.bend at U32 ---- 121 122 def ops_zero() -> SI.Ops.zero(~U32, ~I.u32_op, ~SG.u32_val): 123 {==} 124 125 def ops_one() -> SI.Ops.one(~U32, ~I.u32_op, ~SG.u32_val): 126 {==} 127 128 def ops_abs(+a: U32) -> SI.Ops.abs(~U32, ~I.u32_op, a): 129 {==} 130 131 def tests_lt(+a: U32, +b: U32) -> SI.Tests.lt(~U32, ~I.u32_is, ~SG.u32_val, a, b): 132 U.is_lt_nat(a, b) 133 134 def tests_is_zero(+a: U32) -> SI.Tests.is_zero(~U32, ~I.u32_is, ~SG.u32_val, a): 135 zero_nat(a) 136 137 def ops_sub(+a: U32, +b: U32, +h: {Nat.is_le(SG.u32_val(b), SG.u32_val(a)) == True{} : Bool}) -> SI.Ops.sub(~U32, ~I.u32_op, ~SG.u32_val, a, b, h): 138 U.sub_nat(a, b, h) 139 140 def nz(+b: U32, +h: {Nat.is_eq(SG.u32_val(b), 0n) == False{} : Bool}) -> {U32.is_zero(b) == False{} : Bool}: 141 Equal.trans(Bool, U32.is_zero(b), Nat.is_eq(v(b), 0n), False{}, zero_nat(b), h) 142 143 def ops_quot(+a: U32, +b: U32, +h: {Nat.is_eq(SG.u32_val(b), 0n) == False{} : Bool}) -> SI.Ops.quot(~U32, ~I.u32_op, ~SG.u32_val, a, b, h): 144 UD.div_nat(a, b, nz(b, h)) 145 146 def ops_rem(+a: U32, +b: U32, +h: {Nat.is_eq(SG.u32_val(b), 0n) == False{} : Bool}) -> SI.Ops.rem(~U32, ~I.u32_op, ~SG.u32_val, a, b, h): 147 UD.mod_nat(a, b, nz(b, h)) 148 149 def hlf_div2(+n: Nat) -> {UH.hlf(n) == Nat.div(n, 2n) : Nat}: 150 match n: 151 case 0n: 152 {==} 153 case 1n: 154 {==} 155 case 2n+ +q: 156 %Equal.sym(Nat, Nat.div(Nat.add(2n, q), 2n), 1n+Nat.div(q, 2n), N.div2_step(q)) : {1n+UH.hlf(q) == _ : Nat} 157 N.succ_cong(UH.hlf(q), Nat.div(q, 2n), hlf_div2(q)) 158 159 def ops_half(+a: U32) -> SI.Ops.half(~U32, ~I.u32_op, ~SG.u32_val, a): 160 Equal.trans(Nat, v(U32.shr(a)), UH.hlf(v(a)), Nat.div(v(a), 2n), UH.shr_value(a), hlf_div2(v(a))) 161 162 def carry_of(+a: U32, +b: U32, +h: {I.u32_is(NM.AddOver{a, b}) == False{} : Bool}) -> {P64.carry32(a, b) == False{} : Bool}: 163 Equal.trans(Bool, P64.carry32(a, b), U32.is_lt(U32.add(a, b), a), False{}, Equal.sym(Bool, U32.is_lt(U32.add(a, b), a), P64.carry32(a, b), P64.add_lt(a, b)), h) 164 165 def ops_add(+a: U32, +b: U32, +h: {I.u32_is(NM.AddOver{a, b}) == False{} : Bool}) -> SI.Ops.add(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, a, b, h): 166 +e = L.subst(Bool, c => {Nat.add(UD.v(U32.add(a, b)), WD.sc(32n, S.bit_value(c))) == Nat.add(UD.v(a), UD.v(b)) : Nat}, P64.carry32(a, b), False{}, carry_of(a, b, h), P64.add_cons(a, b)) 167 Equal.trans(Nat, v(U32.add(a, b)), Nat.add(v(U32.add(a, b)), 0n), Nat.add(v(a), v(b)), Equal.sym(Nat, Nat.add(v(U32.add(a, b)), 0n), v(U32.add(a, b)), N.add_zero(v(U32.add(a, b)))), e) 168 169 def add_over_k(+k: Nat, +hk: {k == 32n : Nat}, +a: U32, +b: U32) -> {P64.carry32(a, b) == Bool.not(C.fits(k, Nat.add(v(a), v(b)))) : Bool}: 170 +e = L.subst(Nat, z => {Nat.add(UD.v(U32.add(a, b)), WD.sc(z, S.bit_value(P64.carry32(a, b)))) == Nat.add(UD.v(a), UD.v(b)) : Nat}, 32n, k, Equal.sym(Nat, k, 32n, hk), P64.add_cons(a, b)) 171 carry_fits(k, v(U32.add(a, b)), Nat.add(v(a), v(b)), P64.carry32(a, b), e, U32P.val_lt(1n, {==}, k, hk, U32.add(a, b))) 172 173 def tests_add_over(+a: U32, +b: U32) -> SI.Tests.add_over(~U32, ~I.u32_is, ~SG.u32_val, 32n, a, b): 174 %Equal.sym(Bool, U32.is_lt(U32.add(a, b), a), P64.carry32(a, b), P64.add_lt(a, b)) : {_ == Bool.not(C.fits(32n, Nat.add(v(a), v(b)))) : Bool} 175 add_over_k(32n, {==}, a, b) 176 177 # ---- odd: the low bit ---- 178 179 def dbl(+h: Nat) -> {Nat.mul(h, 2n) == Nat.double(h) : Nat}: 180 match h: 181 case 0n: 182 {==} 183 case 1n+ +p: 184 %Equal.sym(Nat, Nat.mul(p, 2n), Nat.double(p), dbl(p)) : {Nat.add(2n, _) == Nat.double(1n+p) : Nat} 185 {==} 186 187 # r + 2h mod 2 is the bit r 188 def mod2_bit(+r: Nat, +h: Nat, +hr: {Nat.is_lt(r, 2n) == True{} : Bool}) -> {r == Nat.mod(Nat.add(r, Nat.double(h)), 2n) : Nat}: 189 match r: 190 case 0n: 191 %dbl(h) : {0n == Nat.mod(_, 2n) : Nat} 192 %N.add_zero(Nat.mul(h, 2n)) : {0n == Nat.mod(_, 2n) : Nat} 193 Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(h, 2n), 0n), 2n), 0n, NA.absorb(1n, h, 0n)) 194 case 1n: 195 %dbl(h) : {1n == Nat.mod(1n+_, 2n) : Nat} 196 %N.add_zero(Nat.mul(h, 2n)) : {1n == Nat.mod(1n+_, 2n) : Nat} 197 %N.add_succ(Nat.mul(h, 2n), 0n) : {1n == Nat.mod(_, 2n) : Nat} 198 Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(h, 2n), 1n), 2n), 1n, NA.absorb(1n, h, 1n)) 199 case 2n+ +q: 200 Empty.absurd({2n+q == Nat.mod(Nat.add(2n+q, Nat.double(h)), 2n) : Nat}, N.lt_zero_absurd(q, hr)) 201 202 def odd_val(+a: U32) -> {v(U32.and(a, 1)) == Nat.mod(v(a), 2n) : Nat}: 203 +e = PD.and32(1n, a, 1, {==}) 204 %Equal.sym(Nat, v(a), Nat.add(v(U32.and(a, 1)), Nat.double(PD.hp32(1n, a))), e) : {v(U32.and(a, 1)) == Nat.mod(_, 2n) : Nat} 205 mod2_bit(v(U32.and(a, 1)), PD.hp32(1n, a), PD.and32_lt(1n, 1n, {==}, a, 1, {==})) 206 207 def tests_odd(+a: U32) -> SI.Tests.odd(~U32, ~I.u32_is, ~SG.u32_val, a): 208 %Equal.sym(Bool, U32.is_eq(U32.and(a, 1), 1), Nat.is_eq(v(U32.and(a, 1)), v(1)), eq_nat(U32.and(a, 1), 1)) : {_ == Nat.is_eq(Nat.mod(v(a), 2n), 1n) : Bool} 209 %Equal.sym(Nat, v(U32.and(a, 1)), Nat.mod(v(a), 2n), odd_val(a)) : {Nat.is_eq(_, 1n) == Nat.is_eq(Nat.mod(v(a), 2n), 1n) : Bool} 210 {==} 211 212 # ---- multiplication through the full product ---- 213 214 def not_false(+b: Bool, +h: {Bool.not(b) == False{} : Bool}) -> {b == True{} : Bool}: 215 match b: 216 case True{}: 217 {==} 218 case False{}: 219 Empty.absurd({False{} == True{} : Bool}, true_ne_false(h)) 220 221 # fits(k, lo + 2^k hi) exactly when hi == 0 (lo < 2^k) 222 def fits_split(+k: Nat, +lo: Nat, +hi: Nat, +hl: {Nat.is_lt(lo, C.pow2(k)) == True{} : Bool}) -> {C.fits(k, Nat.add(lo, WD.sc(k, hi))) == Nat.is_eq(hi, 0n) : Bool}: 223 match hi: 224 case 0n: 225 %Equal.sym(Nat, WD.sc(k, 0n), 0n, A.sc_zero(k)) : {C.fits(k, Nat.add(lo, _)) == True{} : Bool} 226 %Equal.sym(Nat, Nat.add(lo, 0n), lo, N.add_zero(lo)) : {C.fits(k, _) == True{} : Bool} 227 %Equal.sym(Bool, C.fits(k, lo), Nat.is_lt(lo, C.pow2(k)), WW.fits_lt(k, lo)) : {_ == True{} : Bool} 228 hl 229 case 1n+ +h: 230 %Equal.sym(Bool, C.fits(k, Nat.add(lo, WD.sc(k, 1n+h))), Nat.is_lt(Nat.add(lo, WD.sc(k, 1n+h)), C.pow2(k)), WW.fits_lt(k, Nat.add(lo, WD.sc(k, 1n+h)))) : {_ == False{} : Bool} 231 +p1 = L.subst(Nat, z => {Nat.is_le(z, WD.sc(k, 1n+h)) == True{} : Bool}, WD.sc(k, 1n), C.pow2(k), Equal.sym(Nat, C.pow2(k), WD.sc(k, 1n), U.pow2_scale(k)), AR.sc_le(k, 1n, 1n+h, N.zero_le(h))) 232 +p2 = L.subst(Nat, z => {Nat.is_le(WD.sc(k, 1n+h), z) == True{} : Bool}, Nat.add(WD.sc(k, 1n+h), lo), Nat.add(lo, WD.sc(k, 1n+h)), N.add_comm(WD.sc(k, 1n+h), lo), N.le_add_right(WD.sc(k, 1n+h), lo)) 233 N.le_not_lt(Nat.add(lo, WD.sc(k, 1n+h)), C.pow2(k), N.le_trans(C.pow2(k), WD.sc(k, 1n+h), Nat.add(lo, WD.sc(k, 1n+h)), p1, p2)) 234 235 def hi_zero(+a: U32, +b: U32, +h: {I.u32_is(NM.MulOver{a, b}) == False{} : Bool}) -> {v(X.hi(X.mul32(a, b))) == 0n : Nat}: 236 +z = not_false(U32.is_zero(X.hi(X.mul32(a, b))), h) 237 N.eq_from_is_eq(v(X.hi(X.mul32(a, b))), 0n, Equal.trans(Bool, Nat.is_eq(v(X.hi(X.mul32(a, b))), 0n), U32.is_zero(X.hi(X.mul32(a, b))), True{}, Equal.sym(Bool, U32.is_zero(X.hi(X.mul32(a, b))), Nat.is_eq(v(X.hi(X.mul32(a, b))), 0n), zero_nat(X.hi(X.mul32(a, b)))), z)) 238 239 # the product value as the two limbs of the full product 240 def prod_limbs(+a: U32, +b: U32) -> {Nat.add(v(X.lo(X.mul32(a, b))), WD.sc(32n, v(X.hi(X.mul32(a, b))))) == Nat.mul(v(a), v(b)) : Nat}: 241 e = W64M.mul32_value(a, b) 242 +lo = X.lo(X.mul32(a, b)) 243 +hi = X.hi(X.mul32(a, b)) 244 Equal.trans(Nat, Nat.add(v(lo), WD.sc(32n, v(hi))), Nat.add(v(lo), C.shift(32n, v(hi))), Nat.mul(v(a), v(b)), W64M.cong_r(v(lo), WD.sc(32n, v(hi)), C.shift(32n, v(hi)), Equal.sym(Nat, C.shift(32n, v(hi)), WD.sc(32n, v(hi)), W64M.shift_sc(32n, v(hi)))), e) 245 246 def ops_mul_one(+one: Nat, +h1: {one == 1n : Nat}, +a: U32, +b: U32, +h: {I.u32_is(NM.MulOver{a, b}) == False{} : Bool}) -> {v(U32.mul(a, b)) == Nat.mul(v(a), v(b)) : Nat}: 247 +lo = X.lo(X.mul32(a, b)) 248 +hi = X.hi(X.mul32(a, b)) 249 +e0 = Equal.trans(Nat, v(lo), Nat.add(v(lo), 0n), Nat.add(v(lo), WD.sc(32n, v(hi))), Equal.sym(Nat, Nat.add(v(lo), 0n), v(lo), N.add_zero(v(lo))), W64M.cong_r(v(lo), 0n, WD.sc(32n, v(hi)), Equal.trans(Nat, 0n, WD.sc(32n, 0n), WD.sc(32n, v(hi)), Equal.sym(Nat, WD.sc(32n, 0n), 0n, A.sc_zero(32n)), W64M.cong_sc(32n, 0n, v(hi), Equal.sym(Nat, v(hi), 0n, hi_zero(a, b, h)))))) 250 +ep = Equal.trans(Nat, v(lo), Nat.add(v(lo), WD.sc(32n, v(hi))), Nat.mul(v(a), v(b)), e0, prod_limbs(a, b)) 251 +lt = L.subst(Nat, z => {Nat.is_lt(z, WD.sc(32n, one)) == True{} : Bool}, v(lo), Nat.mul(v(a), v(b)), ep, UD.vb(one, h1, lo)) 252 PD.mul32(one, h1, a, b, lt) 253 254 def ops_mul(+a: U32, +b: U32, +h: {I.u32_is(NM.MulOver{a, b}) == False{} : Bool}) -> SI.Ops.mul(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, a, b, h): 255 ops_mul_one(1n, {==}, a, b, h) 256 257 def mul_over_k(+k: Nat, +hk: {k == 32n : Nat}, +a: U32, +b: U32) -> {U32.is_zero(X.hi(X.mul32(a, b))) == C.fits(k, Nat.mul(v(a), v(b))) : Bool}: 258 +lo = X.lo(X.mul32(a, b)) 259 +hi = X.hi(X.mul32(a, b)) 260 +ek = L.subst(Nat, z => {Nat.add(v(lo), WD.sc(z, v(hi))) == Nat.mul(v(a), v(b)) : Nat}, 32n, k, Equal.sym(Nat, k, 32n, hk), prod_limbs(a, b)) 261 %ek : {U32.is_zero(hi) == C.fits(k, _) : Bool} 262 %Equal.sym(Bool, C.fits(k, Nat.add(v(lo), WD.sc(k, v(hi)))), Nat.is_eq(v(hi), 0n), fits_split(k, v(lo), v(hi), U32P.val_lt(1n, {==}, k, hk, lo))) : {U32.is_zero(hi) == _ : Bool} 263 zero_nat(hi) 264 265 def tests_mul_over(+a: U32, +b: U32) -> SI.Tests.mul_over(~U32, ~I.u32_is, ~SG.u32_val, 32n, a, b): 266 Equal.cong(Bool, Bool, t => Bool.not(t), U32.is_zero(X.hi(X.mul32(a, b))), C.fits(32n, Nat.mul(v(a), v(b))), mul_over_k(32n, {==}, a, b)) 267 268 # ---- mulmod: the product reduced by the 64 / 32 remainder ---- 269 270 def pos_nz(+x: Nat, +y: Nat, +h: {Nat.is_lt(x, y) == True{} : Bool}) -> {Nat.is_eq(y, 0n) == False{} : Bool}: 271 match y: 272 case 0n: 273 Empty.absurd({Nat.is_eq(0n, 0n) == False{} : Bool}, N.lt_zero_absurd(x, h)) 274 case 1n+yp: 275 {==} 276 277 def ops_mulmod(+a: U32, +b: U32, +m: U32, +ha: {Nat.is_lt(SG.u32_val(a), SG.u32_val(m)) == True{} : Bool}, +hb: {Nat.is_lt(SG.u32_val(b), SG.u32_val(m)) == True{} : Bool}) -> SI.Ops.mulmod(~U32, ~I.u32_op, ~SG.u32_val, a, b, m, ha, hb): 278 e1 = W64D.mod32_value(X.mul32(a, b), m, nz(m, pos_nz(v(a), v(m), ha))) 279 e2 = W64M.mul32_value(a, b) 280 Equal.trans(Nat, v(X.mod32(X.mul32(a, b), m)), Nat.mod(SW.value(X.mul32(a, b)), v(m)), Nat.mod(Nat.mul(v(a), v(b)), v(m)), e1, Equal.cong(Nat, Nat, t => Nat.mod(t, v(m)), SW.value(X.mul32(a, b)), Nat.mul(v(a), v(b)), e2)) 281 282 # ---- pow2: the table is the words with one bit set ---- 283 284 def pw_table(+k: Nat, +hk: {Nat.is_lt(k, 32n) == True{} : Bool}) -> {X.pow2(k) == U32{WD.pw(32n, k)} : U32}: 285 match k: 286 case 0n: 287 {==} 288 case 1n: 289 {==} 290 case 2n: 291 {==} 292 case 3n: 293 {==} 294 case 4n: 295 {==} 296 case 5n: 297 {==} 298 case 6n: 299 {==} 300 case 7n: 301 {==} 302 case 8n: 303 {==} 304 case 9n: 305 {==} 306 case 10n: 307 {==} 308 case 11n: 309 {==} 310 case 12n: 311 {==} 312 case 13n: 313 {==} 314 case 14n: 315 {==} 316 case 15n: 317 {==} 318 case 16n: 319 {==} 320 case 17n: 321 {==} 322 case 18n: 323 {==} 324 case 19n: 325 {==} 326 case 20n: 327 {==} 328 case 21n: 329 {==} 330 case 22n: 331 {==} 332 case 23n: 333 {==} 334 case 24n: 335 {==} 336 case 25n: 337 {==} 338 case 26n: 339 {==} 340 case 27n: 341 {==} 342 case 28n: 343 {==} 344 case 29n: 345 {==} 346 case 30n: 347 {==} 348 case 31n: 349 {==} 350 case 32n+ +j: 351 Empty.absurd({X.pow2(32n+j) == U32{WD.pw(32n, 32n+j)} : U32}, N.lt_zero_absurd(j, hk)) 352 353 def ops_pow2(+k: Nat, +hk: {Nat.is_lt(k, 32n) == True{} : Bool}) -> SI.Ops.pow2(~U32, ~I.u32_op, ~SG.u32_val, 32n, k, hk): 354 %Equal.sym(U32, X.pow2(k), U32{WD.pw(32n, k)}, pw_table(k, hk)) : {v(_) == C.pow2(k) : Nat} 355 %Equal.sym(Nat, C.pow2(k), WD.sc(k, 1n), U.pow2_scale(k)) : {v(U32{WD.pw(32n, k)}) == _ : Nat} 356 PD.pow32(k, hk, 1n, {==}, U32{WD.pw(32n, k)}, {==}) 357 358 # ---- sqrt: the exact integer square root from any F32 estimate ---- 359 360 def ops_sqrt(+a: U32) -> SI.Ops.sqrt(~U32, ~I.u32_op, ~SG.u32_val, a): 361 W64S.isqrt32_value(a)