~/bend-docscommunity

proofs/math/typed/w64mul.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64mul.bend as W64mul

17 imports
import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/math/w64.bend as SW
import ../../../src/math/w64.bend as X
import ../../../src/math/u64.bend as WU
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/u32div.bend as UD
import ../../lib/word.bend as WD
import ../../lib/arith.bend as AR
import ../../lib/u32alg.bend as A
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../../lib/lemmas/proofs/word_multiplication.bend as WM
import ../../lib/lemmas/spec/numeric.bend as S
import ../u64/u64div.bend as PD
import ../u64/u64.bend as P64
import ./shrn.bend as SR

Definitions

def v source · line 31 · raw

@+x:U32 -> Nat

def le_mul_r source · line 36 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+h:{Nat.is_le(b, c) == True{} : Bool} -> {Nat.is_le(Nat.mul(a, b), Nat.mul(a, c)) == True{} : Bool}

def mul_lt_sq source · line 42 · raw

@+x:Nat -> @+y:Nat -> @+s:Nat -> @+hx:{Nat.is_lt(x, s) == True{} : Bool} -> @+hy:{Nat.is_lt(y, s) == True{} : Bool} -> {Nat.is_lt(Nat.mul(x, y), Nat.mul(s, s)) == True{} : Bool}

x, y < s gives x * y < s * s

def sq_sc source · line 54 · raw

@+k:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, one), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, one)) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(Nat.add(k, k), one) : Nat}

def mul_sc1 source · line 57 · raw

@+k:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:Nat -> {Nat.mul(x, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, one)) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, x) : Nat}

def nz16 source · line 62 · raw

@+c:U32 -> @+pc:{c == U32{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.pw(32n, 16n)} : U32} -> {U32.is_zero(c) == False{} : Bool}

def h16 source · line 65 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+c:U32 -> @+pc:{c == U32{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.pw(32n, 16n)} : U32} -> {v(c) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(16n, one) : Nat}

def lo16 source · line 68 · raw

@+x:U32 -> @+m:U32 -> Nat

def hi16 source · line 71 · raw

@+x:U32 -> @+c:U32 -> Nat

def lo16_lt source · line 74 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:U32 -> @+m:U32 -> @+pm:{m == U32{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.mask(32n, 16n)} : U32} -> {Nat.is_lt(lo16(x, m), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(16n, one)) == True{} : Bool}

def dm16 source · line 78 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:U32 -> @+c:U32 -> @+pc:{c == U32{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.pw(32n, 16n)} : U32} -> {Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(16n, hi16(x, c)), v(U32.mod(x, c))) == v(x) : Nat}

v(x) == 2^16 hi + (x mod 2^16)

def hi16_lt source · line 83 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:U32 -> @+c:U32 -> @+pc:{c == U32{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.pw(32n, 16n)} : U32} -> {Nat.is_lt(hi16(x, c), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(16n, one)) == True{} : Bool}

def split16 source · line 89 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:U32 -> @+c:U32 -> @+pc:{c == U32{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.pw(32n, 16n)} : U32} -> @+m:U32 -> @+pm:{m == U32{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.mask(32n, 16n)} : U32} -> {v(x) == Nat.add(lo16(x, m), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(16n, hi16(x, c))) : Nat}

v(x) == lo + 2^16 hi

def cong_l source · line 100 · raw

@+x:Nat -> @+y:Nat -> @+z:Nat -> @+e:{x == y : Nat} -> {Nat.add(x, z) == Nat.add(y, z) : Nat}

def cong_r source · line 103 · raw

@+z:Nat -> @+x:Nat -> @+y:Nat -> @+e:{x == y : Nat} -> {Nat.add(z, x) == Nat.add(z, y) : Nat}

def cong_sc source · line 106 · raw

@+k:Nat -> @+x:Nat -> @+y:Nat -> @+e:{x == y : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, x) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, y) : Nat}

def mul_sc_r source · line 110 · raw

@+k:Nat -> @+q:Nat -> @+d:Nat -> {Nat.mul(q, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, d)) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, Nat.mul(q, d)) : Nat}

q * 2^k d == 2^k (q d)

def mul_sc_l source · line 114 · raw

@+k:Nat -> @+q:Nat -> @+d:Nat -> {Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, q), d) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, Nat.mul(q, d)) : Nat}

2^k q * d == 2^k (q d)

def sc_sc source · line 118 · raw

@+j:Nat -> @+k:Nat -> @+x:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(j, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, x)) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(Nat.add(j, k), x) : Nat}

2^j (2^k x) == 2^(j+k) x

def sc_add2 source · line 121 · raw

@+k:Nat -> @+x:Nat -> @+y:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, Nat.add(x, y)) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, x), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, y)) : Nat}

def add4 source · line 125 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+d:Nat -> {Nat.add(Nat.add(a, b), Nat.add(c, d)) == Nat.add(Nat.add(a, c), Nat.add(b, d)) : Nat}

(a + b) + (c + d) == (a + c) + (b + d)

def expand16 source · line 131 · raw

@+al:Nat -> @+ah:Nat -> @+bl:Nat -> @+bh:Nat -> {Nat.mul(Nat.add(al, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(16n, ah)), Nat.add(bl, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(16n, bh))) == Nat.add(Nat.add(Nat.mul(al, bl), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(16n, Nat.mul(al, bh))), Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(16n, Nat.mul(ah, bl)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, Nat.mul(ah, bh)))) : Nat}

(al + 2^16 ah)(bl + 2^16 bh) == (al bl + 2^16 al bh) + (2^16 ah bl + 2^32 ah bh)

def mid_eq source · line 149 · raw

@+m:Nat -> @+k:Nat -> @+mlo:Nat -> @+mhi:Nat -> @+lh:Nat -> @+hl:Nat -> @+e3:{Nat.add(m, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, k)) == Nat.add(lh, hl) : Nat} -> @+e5:{m == Nat.add(mlo, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(16n, mhi)) : Nat} -> {Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(16n, mlo), Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, mhi), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(48n, k))) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(16n, lh), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(16n, hl)) : Nat}

2^16 Mlo + (2^32 Mhi + 2^48 K) == 2^16 LH + 2^16 HL, from M == Mlo + 2^16 Mhi and M + 2^32 K == LH + HL

def assemble source · line 166 · raw

@+al:Nat -> @+ah:Nat -> @+bl:Nat -> @+bh:Nat -> @+m:Nat -> @+k:Nat -> @+mlo:Nat -> @+mhi:Nat -> @+vl:Nat -> @+c2:Nat -> @+e3:{Nat.add(m, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, k)) == Nat.add(Nat.mul(al, bh), Nat.mul(ah, bl)) : Nat} -> @+e5:{m == Nat.add(mlo, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(16n, mhi)) : Nat} -> @+e8:{Nat.add(vl, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, c2)) == Nat.add(Nat.mul(al, bl), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(16n, mlo)) : Nat} -> {Nat.add(vl, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, Nat.add(Nat.add(Nat.mul(ah, bh), Nat.add(mhi, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(16n, k))), c2))) == Nat.mul(Nat.add(al, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(16n, ah)), Nat.add(bl, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(16n, bh))) : Nat}

the value equation of the product: low word, carries and high digits

def shift_sc source · line 195 · raw

@+k:Nat -> @+x:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(k, x) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, x) : Nat}

def mex source · line 202 · raw

@x:U32 -> @y:U32 -> Nat

def mul_cons source · line 208 · raw

@+x:U32 -> @+y:U32 -> {Nat.add(v(U32.mul(x, y)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, mex(x, y))) == Nat.mul(v(x), v(y)) : Nat}

a wrapping product and its lost high part

def b32_v source · line 218 · raw

@+c:Bool -> {v(0xa7e654f9780078ca65bf9e187da99d3e/src/math/w64.b32(c)) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.bit_value(c) : Nat}

def bit_le1 source · line 225 · raw

@+c:Bool -> {Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.bit_value(c), 1n) == True{} : Bool}

def one_lt_sc source · line 232 · raw

@+k:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.is_lt(1n, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(1n+k, one)) == True{} : Bool}

def bit_lt16 source · line 236 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+c:Bool -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.bit_value(c), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(16n, one)) == True{} : Bool}

def prod_lt source · line 239 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:Nat -> @+y:Nat -> @+hx:{Nat.is_lt(x, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(16n, one)) == True{} : Bool} -> @+hy:{Nat.is_lt(y, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(16n, one)) == True{} : Bool} -> {Nat.is_lt(Nat.mul(x, y), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, one)) == True{} : Bool}

def sc16_lt source · line 243 · raw

@+one:Nat -> @+x:Nat -> @+hx:{Nat.is_lt(x, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(16n, one)) == True{} : Bool} -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(16n, x), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, one)) == True{} : Bool}

2^16 x < 2^32 for x < 2^16

def fin_g source · line 248 · raw

@+ll:U32 -> @+mid:U32 -> @+hh:U32 -> @mc:Bool -> @+c:U32 -> 0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64

def mid_g source · line 251 · raw

@+ll:U32 -> @+lh:U32 -> @+hl:U32 -> @+hh:U32 -> @+c:U32 -> 0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64

def h_g source · line 254 · raw

@+al:U32 -> @+ah:U32 -> @+bl:U32 -> @+bh:U32 -> @+c:U32 -> 0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64

def mul32g source · line 257 · raw

@+a:U32 -> @+b:U32 -> @+c:U32 -> @+m:U32 -> 0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64

def fin_eq source · line 262 · raw

@+ll:U32 -> @+mid:U32 -> @+hh:U32 -> @+mc:Bool -> {0xa7e654f9780078ca65bf9e187da99d3e/src/math/w64.mul32_fin(ll, mid, hh, mc) == fin_g(ll, mid, hh, mc, 65536) : 0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64}

the implementation splits by U32.shrn(_, 16), a shift; the generalised product by U32.div(_, 65536): the same words (SR.shr16)

def h_eq source · line 266 · raw

@+al:U32 -> @+ah:U32 -> @+bl:U32 -> @+bh:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/src/math/w64.mul32_h(al, ah, bl, bh) == h_g(al, ah, bl, bh, 65536) : 0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64}

def impl source · line 269 · raw

@+a:U32 -> @+b:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/src/math/w64.mul32(a, b) == mul32g(a, b, 65536, 65535) : 0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64}

def mulval source · line 275 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:U32 -> @+b:U32 -> @+c:U32 -> @+pc:{c == U32{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.pw(32n, 16n)} : U32} -> @+m:U32 -> @+pm:{m == U32{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.mask(32n, 16n)} : U32} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/math/w64.value(mul32g(a, b, c, m)) == Nat.mul(v(a), v(b)) : Nat}

the value of the generalised product, constants symbolic

def mul32_value source · line 348 · raw

@+a:U32 -> @+b:U32 -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/w64.Mul32.value(a, b)

Mul32.value: the full product of two U32