~/bend-docscommunity

proofs/math/typed/w64mmtop.bend checks

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

16 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 ./w64mul.bend as W64M
import ./w64div.bend as W64D
import ./w64add.bend as WA
import ./w64m128.bend as M128
import ./w64mm.bend as MM
import ./width.bend as WW
import ./u32laws.bend as LW

Definitions

def v source · line 20 · raw

@+x:U32 -> Nat

def val0 source · line 23 · raw

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

def vm_small source · line 26 · raw

@+ml:U32 -> @+mh:U32 -> @+hz:{U32.is_zero(mh) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh}) == v(ml) : Nat}

def mm_small source · line 30 · raw

@+al:U32 -> @+ah:U32 -> @+bl:U32 -> @+bh:U32 -> @+ml:U32 -> @+mh:U32 -> @+ha:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh})) == True{} : Bool} -> @+hb:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh})) == True{} : Bool} -> @+hz:{U32.is_zero(mh) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mm_pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh}, True{})) == Nat.mod(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh})), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh})) : Nat}

def mm_bg source · line 41 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pl:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+ph:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+pr:Nat -> @+em:{Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(pl), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(ph))) == pr : Nat} -> @+ml:U32 -> @+mh:U32 -> @+hsq:{Nat.is_lt(pr, Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh}), 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/w64.red96(ph, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.hi(pl), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(pl), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh})) == Nat.mod(pr, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh})) : Nat}

def mm_big source · line 62 · raw

@+al:U32 -> @+ah:U32 -> @+bl:U32 -> @+bh:U32 -> @+ml:U32 -> @+mh:U32 -> @+ha:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh})) == True{} : Bool} -> @+hb:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}), 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/w64.red96(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.psnd(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul128(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh})), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.hi(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pfst(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul128(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}))), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pfst(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul128(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}))), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh})) == Nat.mod(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh})), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh})) : Nat}

def mm_c source · line 65 · raw

@+al:U32 -> @+ah:U32 -> @+bl:U32 -> @+bh:U32 -> @+ml:U32 -> @+mh:U32 -> @+ha:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh})) == True{} : Bool} -> @+hb:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh})) == True{} : Bool} -> @+z:Bool -> @+hz:{U32.is_zero(mh) == z : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mm_pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh}, z)) == Nat.mod(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh})), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh})) : Nat}

def mulmod_value source · line 72 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+ha:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(a), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(m)) == True{} : Bool} -> @+hb:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(b), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(m)) == True{} : Bool} -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.MulMod.value(a, b, m, ha, hb)