proofs/math/typed/w64dm.bend checks
raw source on the hub · import bend-collections-laws-math@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 -> {0xf86f5f1d9a594d5a5cff999100e01d03/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, 0xf86f5f1d9a594d5a5cff999100e01d03/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(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.fst_q(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul_32_64(q, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.snd_r(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul_32_64(q, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}))))) == Nat.mul(v(q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/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:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(a)) == True{} : Bool}
def ov96 source · line 85 · raw
@+xl:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+xh:U32 -> @+pl:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+ph:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.over96(xl, xh, (pl, ph)) == Nat.is_lt(Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(xl), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, v(xh))), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(pl), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, v(ph)))) : Bool}the 96-bit comparison of over96
def X96 source · line 91 · raw
@+xl:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+xh:U32 -> Nat
def ovq source · line 95 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+xl:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+xh:U32 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+q:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.over96(xl, xh, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul_32_64(q, b)) == Nat.is_lt(X96(xl, xh), Nat.mul(v(q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(b))) : Bool}q b > x
def QB source · line 102 · raw
@+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+q:U32 -> Nat
def qdn source · line 106 · raw
@+fu:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+xl:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+xh:U32 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+q:U32 -> @+cb:Bool -> @+nq:Nat -> @+hf:{Nat.is_lt(v(q), fu) == True{} : Bool} -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.over96(xl, xh, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul_32_64(q, b)) == cb : Bool} -> @+hnq:{v(q) == nq : Nat} -> {Nat.is_le(QB(b, 0xf86f5f1d9a594d5a5cff999100e01d03/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:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+xh:U32 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+q:U32 -> @+cb:Bool -> @+nq:Nat -> @+hf:{Nat.is_lt(v(q), fu) == True{} : Bool} -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.over96(xl, xh, 0xf86f5f1d9a594d5a5cff999100e01d03/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), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(b))) == True{} : Bool} -> {Nat.is_lt(X96(xl, xh), Nat.mul(1n+v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.q_fix(fu, xl, xh, b, q, cb)), 0xf86f5f1d9a594d5a5cff999100e01d03/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:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/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:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+xh:U32 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+q:U32 -> @+m:U32 -> U32
def qs_pair source · line 167 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+xl:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+xh:U32 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+q:U32 -> @+m:U32 -> @+pm:{m == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, 32n)} : U32} -> @+hX:{Nat.is_lt(X96(xl, xh), Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, one), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(b))) == True{} : Bool} -> @+hu:{Nat.is_lt(X96(xl, xh), Nat.mul(1n+v(q), 0xf86f5f1d9a594d5a5cff999100e01d03/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)), 0xf86f5f1d9a594d5a5cff999100e01d03/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:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+xh:U32 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+q:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/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:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, y) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/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, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, t)) == x : Nat} -> @+hr:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, r) == True{} : Bool} -> @+hx:{0xf86f5f1d9a594d5a5cff999100e01d03/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:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {X96(a, 0) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(a) : Nat}
def u32_0 source · line 194 · raw
@+q:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/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(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}, 0), Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, one), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/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(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}, 0), Nat.mul(1n+v(e), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}))) == True{} : Bool} -> @+bp:Nat -> @+hB:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}) == 1n+bp : Nat} -> Pair({Nat.div(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}), 1n+bp) == v(QS(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}, 0, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}, e, 4294967295)) : Nat}, {Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}), 1n+bp) == Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}), Nat.mul(v(QS(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}, 0, 0xf86f5f1d9a594d5a5cff999100e01d03/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(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}, 0), Nat.mul(1n+v(e), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}))) == True{} : Bool} -> {Nat.is_le(Nat.mul(v(QS(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}, 0, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}, e, 4294967295)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh})), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah})) == True{} : Bool}