~/bend-docscommunity

proofs/math/typed/w64mm.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mm.bend as W64mm

14 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 ../natural/arith.bend as NR
import ./w64dm.bend as DM
import ./w64est.bend as W64E
import ./w64m128.bend as M128
import ./width.bend as WW
import ./u32laws.bend as LW

Definitions

def v source · line 21 · raw

@+x:U32 -> Nat

def red_alg source · line 24 · raw

@+vs:Nat -> @+vf:Nat -> @+vxl:Nat -> @+y1:Nat -> @+qs:Nat -> @+t:Nat -> @+mq:Nat -> @+r:Nat -> @+es:{Nat.add(vs, vf) == Nat.add(vxl, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, qs)) : Nat} -> @+e1:{Nat.add(vf, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, t)) == mq : Nat} -> @+er:{Nat.add(mq, r) == Nat.add(vxl, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, y1)) : Nat} -> {Nat.add(vf, Nat.add(vs, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, y1))) == Nat.add(vf, Nat.add(r, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, Nat.add(t, qs)))) : Nat}

def red_core source · line 28 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x0:U32 -> @+y0:U32 -> @+y1:U32 -> @+ml:U32 -> @+mh:U32 -> @+q:U32 -> @+bp:Nat -> @+hB:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh}) == 1n+bp : Nat} -> @+hle:{Nat.is_le(Nat.mul(v(q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh})), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64dm.X96(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{x0, y0}, y1)) == True{} : Bool} -> @+hlt:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64dm.X96(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{x0, y0}, y1), Nat.mul(1n+v(q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh}))) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{x0, y0}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.fst_q(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul_32_64(q, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh})))) == Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64dm.X96(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{x0, y0}, y1), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh})) : Nat}

x - q m for q m <= x < (q + 1) m is x mod m

def red_q source · line 42 · raw

@+x0:U32 -> @+y0:U32 -> @+ml:U32 -> @+mh:U32 -> @+q1:U32 -> @+q2:U32 -> @+e:{q1 == q2 : U32} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{x0, y0}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.fst_q(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul_32_64(q1, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh})))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{x0, y0}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.fst_q(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul_32_64(q2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh})))) : Nat}

def red_fin source · line 45 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x0:U32 -> @+y0:U32 -> @+y1:U32 -> @+ml:U32 -> @+mh:U32 -> @+q:U32 -> @+bp:Nat -> @+hB:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh}) == 1n+bp : Nat} -> @p:Pair({Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64dm.QB(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh}, q), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64dm.X96(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{x0, y0}, y1)) == True{} : Bool}, {Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64dm.X96(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{x0, y0}, y1), Nat.mul(1n+v(q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh}))) == True{} : Bool}) -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{x0, y0}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.fst_q(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul_32_64(q, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh})))) == Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64dm.X96(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{x0, y0}, y1), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh})) : Nat}

def x96_eq source · line 49 · raw

@+x0:U32 -> @+y0:U32 -> @+y1:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64dm.X96(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{x0, y0}, y1) == Nat.add(v(x0), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{y0, y1}))) : Nat}

def red_hx source · line 53 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x0:U32 -> @+y0:U32 -> @+y1:U32 -> @+ml:U32 -> @+mh:U32 -> @+hx:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{y0, y1}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh})) == True{} : Bool} -> {Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64dm.X96(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{x0, y0}, y1), Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, one), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh}))) == True{} : Bool}

x0 + 2^32 xh < 2^32 m

def red_ve source · line 64 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x0:U32 -> @+y0:U32 -> @+y1:U32 -> @+ml:U32 -> @+mh:U32 -> @+e:U32 -> @+hx:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{y0, y1}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh})) == True{} : Bool} -> @+hz:{U32.is_zero(mh) == False{} : Bool} -> @+he:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64dm.X96(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{x0, y0}, y1), Nat.mul(1n+v(e), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh}))) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{x0, y0}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.fst_q(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul_32_64(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.q_start(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{x0, y0}, y1, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh}, e), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh})))) == Nat.mod(Nat.add(v(x0), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{y0, y1}))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh})) : Nat}

red96(xh, x0, m) == (x0 + 2^32 xh) mod m for xh < m, m >= 2^32

def red_v source · line 74 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x0:U32 -> @+y0:U32 -> @+y1:U32 -> @+ml:U32 -> @+mh:U32 -> @+hx:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{y0, y1}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh})) == True{} : Bool} -> @+hz:{U32.is_zero(mh) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.red96(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{y0, y1}, x0, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh})) == Nat.mod(Nat.add(v(x0), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{y0, y1}))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh})) : Nat}

def red_vg source · line 77 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x0:U32 -> @+xh:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+ml:U32 -> @+mh:U32 -> @+hx:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(xh), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh})) == True{} : Bool} -> @+hz:{U32.is_zero(mh) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.red96(xh, x0, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh})) == Nat.mod(Nat.add(v(x0), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(xh))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh})) : Nat}

def hi0 source · line 83 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+al:U32 -> @+ah:U32 -> @+ml:U32 -> @+h:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}), v(ml)) == True{} : Bool} -> @+c:Nat -> @+hc:{v(ah) == c : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}) == v(al) : Nat}

the high limb of a value below 2^32 is 0