~/bend-docscommunity

proofs/math/typed/w64dm.bend checks

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

20 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/lemmas/proofs/nat_algebra.bend as NA
import ../../lib/word.bend as WD
import ../../lib/u32.bend as U
import ../../lib/arith.bend as AR2
import ../../lib/lemmas/spec/numeric.bend as S
import ../natural/arith.bend as NR
import ../u64/u64.bend as P64
import ./w64mul.bend as W64M
import ./w64div.bend as W64D
import ./w64add.bend as WA
import ./width.bend as WW
import ./u32laws.bend as LW
import ./natfuel.bend as NF

Definitions

def v source · line 31 · raw

@+x:U32 -> Nat

def true_ne_false source · line 34 · raw

@+h:{True{} == False{} : Bool} -> Empty

def vb source · line 37 · raw

@+x:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(32n, v(x)) == True{} : Bool}

def lt_add_pos source · line 40 · raw

@+a:Nat -> @+c:Nat -> @+h:{Nat.is_lt(0n, c) == True{} : Bool} -> {Nat.is_lt(a, Nat.add(a, c)) == True{} : Bool}

def hi_lt source · line 45 · raw

@+p:Nat -> @+q:Nat -> @+bh:Nat -> @+lo:Nat -> @+hi:Nat -> @+hq:{Nat.is_lt(q, 1n+p) == True{} : Bool} -> @+hb:{Nat.is_lt(bh, 1n+p) == True{} : Bool} -> @+hp:{Nat.is_le(1n, p) == True{} : Bool} -> @+e:{Nat.add(lo, Nat.mul(hi, 1n+p)) == Nat.mul(q, bh) : Nat} -> {Nat.is_lt(Nat.add(hi, 1n), 1n+p) == True{} : Bool}

q, bh < 1 + p, p >= 1, lo + hi (1 + p) == q bh: hi + 1 < 1 + p

def P2 source · line 52 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.is_le(2n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(32n, one)) == True{} : Bool}

def mul3264 source · line 57 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+q:U32 -> @+bl:U32 -> @+bh:U32 -> {Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/math/w64.value(0xa7e654f9780078ca65bf9e187da99d3e/src/math/w64.fst_q(0xa7e654f9780078ca65bf9e187da99d3e/src/math/w64.mul_32_64(q, 0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64{bl, bh}))), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(64n, v(0xa7e654f9780078ca65bf9e187da99d3e/src/math/w64.snd_r(0xa7e654f9780078ca65bf9e187da99d3e/src/math/w64.mul_32_64(q, 0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64{bl, bh}))))) == Nat.mul(v(q), 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/w64.value(0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64{bl, bh})) : Nat}

the 96-bit product q b of mul_32_64: low 64 bits + 2^64 * top 32 bits

def fit64 source · line 79 · raw

@+a:0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64 -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(64n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/w64.value(a)) == True{} : Bool}

def ov96 source · line 85 · raw

@+xl:0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64 -> @+xh:U32 -> @+pl:0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64 -> @+ph:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/src/math/w64.over96(xl, xh, (pl, ph)) == Nat.is_lt(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/math/w64.value(xl), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(64n, v(xh))), Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/math/w64.value(pl), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(64n, v(ph)))) : Bool}

the 96-bit comparison of over96

def X96 source · line 91 · raw

@+xl:0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64 -> @+xh:U32 -> Nat

def ovq source · line 95 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+xl:0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64 -> @+xh:U32 -> @+b:0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64 -> @+q:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/src/math/w64.over96(xl, xh, 0xa7e654f9780078ca65bf9e187da99d3e/src/math/w64.mul_32_64(q, b)) == Nat.is_lt(X96(xl, xh), Nat.mul(v(q), 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/w64.value(b))) : Bool}

q b > x

def QB source · line 102 · raw

@+b:0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64 -> @+q:U32 -> Nat

def qdn source · line 106 · raw

@+fu:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+xl:0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64 -> @+xh:U32 -> @+b:0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64 -> @+q:U32 -> @+cb:Bool -> @+nq:Nat -> @+hf:{Nat.is_lt(v(q), fu) == True{} : Bool} -> @+hc:{0xa7e654f9780078ca65bf9e187da99d3e/src/math/w64.over96(xl, xh, 0xa7e654f9780078ca65bf9e187da99d3e/src/math/w64.mul_32_64(q, b)) == cb : Bool} -> @+hnq:{v(q) == nq : Nat} -> {Nat.is_le(QB(b, 0xa7e654f9780078ca65bf9e187da99d3e/src/math/w64.q_fix(fu, xl, xh, b, q, cb)), X96(xl, xh)) == True{} : Bool}

down: q - 1 while q b > x; ends with q b <= x

def qup2 source · line 123 · raw

@+fu:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+xl:0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64 -> @+xh:U32 -> @+b:0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64 -> @+q:U32 -> @+cb:Bool -> @+nq:Nat -> @+hf:{Nat.is_lt(v(q), fu) == True{} : Bool} -> @+hc:{0xa7e654f9780078ca65bf9e187da99d3e/src/math/w64.over96(xl, xh, 0xa7e654f9780078ca65bf9e187da99d3e/src/math/w64.mul_32_64(q, b)) == cb : Bool} -> @+hnq:{v(q) == nq : Nat} -> @+hu:{Nat.is_lt(X96(xl, xh), Nat.mul(1n+v(q), 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/w64.value(b))) == True{} : Bool} -> {Nat.is_lt(X96(xl, xh), Nat.mul(1n+v(0xa7e654f9780078ca65bf9e187da99d3e/src/math/w64.q_fix(fu, xl, xh, b, q, cb)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/w64.value(b))) == True{} : Bool}

down keeps x < (q + 1) b: a step is taken only when x < q b

def div_uniq source · line 143 · raw

@+x:Nat -> @+r:Nat -> @+bp:Nat -> @+h1:{Nat.is_le(Nat.mul(r, 1n+bp), x) == True{} : Bool} -> @+h2:{Nat.is_lt(x, Nat.mul(1n+r, 1n+bp)) == True{} : Bool} -> Pair({Nat.div(x, 1n+bp) == r : Nat}, {Nat.mod(x, 1n+bp) == Nat.sub(x, Nat.mul(r, 1n+bp)) : Nat})

r b <= x < (r + 1) b: r == x / b and x - r b == x mod b

def qs_fin source · line 151 · raw

@+x:Nat -> @+r:Nat -> @+bp:Nat -> @+hB:{0xa7e654f9780078ca65bf9e187da99d3e/spec/math/w64.value(0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64{0, 0}) == 0n : Nat} -> @p:Pair({Nat.is_le(Nat.mul(r, 1n+bp), x) == True{} : Bool}, {Nat.is_lt(x, Nat.mul(1n+r, 1n+bp)) == True{} : Bool}) -> Pair({Nat.div(x, 1n+bp) == r : Nat}, {Nat.mod(x, 1n+bp) == Nat.sub(x, Nat.mul(r, 1n+bp)) : Nat})

def qs_fin2 source · line 155 · raw

@+x:Nat -> @+r:Nat -> @+B:Nat -> @+bp:Nat -> @+hB:{B == 1n+bp : Nat} -> @p:Pair({Nat.is_le(Nat.mul(r, B), x) == True{} : Bool}, {Nat.is_lt(x, Nat.mul(1n+r, B)) == True{} : Bool}) -> Pair({Nat.div(x, 1n+bp) == r : Nat}, {Nat.mod(x, 1n+bp) == Nat.sub(x, Nat.mul(r, 1n+bp)) : Nat})

def qle_fin source · line 159 · raw

@+x:Nat -> @+r:Nat -> @+B:Nat -> @p:Pair({Nat.is_le(Nat.mul(r, B), x) == True{} : Bool}, {Nat.is_lt(x, Nat.mul(1n+r, B)) == True{} : Bool}) -> {Nat.is_le(Nat.mul(r, B), x) == True{} : Bool}

def QS source · line 163 · raw

@+xl:0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64 -> @+xh:U32 -> @+b:0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64 -> @+q:U32 -> @+m:U32 -> U32

def qs_pair source · line 167 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+xl:0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64 -> @+xh:U32 -> @+b:0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64 -> @+q:U32 -> @+m:U32 -> @+pm:{m == U32{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.mask(32n, 32n)} : U32} -> @+hX:{Nat.is_lt(X96(xl, xh), Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(32n, one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/w64.value(b))) == True{} : Bool} -> @+hu:{Nat.is_lt(X96(xl, xh), Nat.mul(1n+v(q), 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/w64.value(b))) == True{} : Bool} -> Pair({Nat.is_le(QB(b, QS(xl, xh, b, q, m)), X96(xl, xh)) == True{} : Bool}, {Nat.is_lt(X96(xl, xh), Nat.mul(1n+v(QS(xl, xh, b, q, m)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/w64.value(b))) == True{} : Bool})

the down loop from an estimate q with x < (q + 1) b: q' b <= x < (q' + 1) b

def impl_qs source · line 170 · raw

@+xl:0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64 -> @+xh:U32 -> @+b:0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64 -> @+q:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/src/math/w64.q_start(xl, xh, b, q) == QS(xl, xh, b, q, 4294967295) : U32}

def fits_le source · line 175 · raw

@+k:Nat -> @+x:Nat -> @+y:Nat -> @+h:{Nat.is_le(x, y) == True{} : Bool} -> @+hy:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(k, y) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(k, x) == True{} : Bool}

def low_exact source · line 179 · raw

@+r:Nat -> @+t:Nat -> @+x:Nat -> @+e:{Nat.add(r, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(64n, t)) == x : Nat} -> @+hr:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(64n, r) == True{} : Bool} -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(64n, x) == True{} : Bool} -> {r == x : Nat}

a 96-bit value below 2^64 has top word 0: its low 64 bits are the value

def pr1 source · line 183 · raw

@-P:Type -> @-Q:Type -> @p:Pair(P, Q) -> P

def pr2 source · line 187 · raw

@-P:Type -> @-Q:Type -> @p:Pair(P, Q) -> Q

def x96_0 source · line 191 · raw

@+a:0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64 -> {X96(a, 0) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/w64.value(a) : Nat}

def u32_0 source · line 194 · raw

@+q:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/math/w64.value(0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64{q, 0}) == v(q) : Nat}

def dm_hx source · line 198 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+al:U32 -> @+ah:U32 -> @+bl:U32 -> @+bh:U32 -> @+hz:{U32.is_zero(bh) == False{} : Bool} -> {Nat.is_lt(X96(0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64{al, ah}, 0), Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(32n, one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/w64.value(0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64{bl, bh}))) == True{} : Bool}

a < 2^32 b for b >= 2^32

def dm_pair source · line 209 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+al:U32 -> @+ah:U32 -> @+bl:U32 -> @+bh:U32 -> @+e:U32 -> @+hz:{U32.is_zero(bh) == False{} : Bool} -> @+he:{Nat.is_lt(X96(0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64{al, ah}, 0), Nat.mul(1n+v(e), 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/w64.value(0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64{bl, bh}))) == True{} : Bool} -> @+bp:Nat -> @+hB:{0xa7e654f9780078ca65bf9e187da99d3e/spec/math/w64.value(0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64{bl, bh}) == 1n+bp : Nat} -> Pair({Nat.div(0xa7e654f9780078ca65bf9e187da99d3e/spec/math/w64.value(0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64{al, ah}), 1n+bp) == v(QS(0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64{al, ah}, 0, 0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64{bl, bh}, e, 4294967295)) : Nat}, {Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/spec/math/w64.value(0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64{al, ah}), 1n+bp) == Nat.sub(0xa7e654f9780078ca65bf9e187da99d3e/spec/math/w64.value(0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64{al, ah}), Nat.mul(v(QS(0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64{al, ah}, 0, 0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64{bl, bh}, e, 4294967295)), 1n+bp)) : Nat})

the big-divisor quotient: q b <= a < (q + 1) b

def dm_le source · line 216 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+al:U32 -> @+ah:U32 -> @+bl:U32 -> @+bh:U32 -> @+e:U32 -> @+hz:{U32.is_zero(bh) == False{} : Bool} -> @+he:{Nat.is_lt(X96(0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64{al, ah}, 0), Nat.mul(1n+v(e), 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/w64.value(0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64{bl, bh}))) == True{} : Bool} -> {Nat.is_le(Nat.mul(v(QS(0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64{al, ah}, 0, 0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64{bl, bh}, e, 4294967295)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/w64.value(0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64{bl, bh})), 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/w64.value(0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64{al, ah})) == True{} : Bool}