~/bend-docscommunity

proofs/math/typed/w64dmrem.bend checks

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

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/u32.bend as U
import ./w64div.bend as W64D
import ./w64add.bend as WA
import ./width.bend as WW
import ./u32laws.bend as LW
import ./w64dm.bend as DM
import ./w64est.bend as W64E

Definitions

def hd_small source · line 19 · raw

@+bl:U32 -> @+bh:U32 -> @+hb:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}) == False{} : Bool} -> @+hz:{U32.is_zero(bh) == True{} : Bool} -> {U32.is_zero(bl) == False{} : Bool}

def vb_small source · line 22 · raw

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

def vb_pos source · line 26 · raw

@+bl:U32 -> @+bh:U32 -> @+hz:{U32.is_zero(bh) == False{} : Bool} -> {Nat.is_le(1n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh})) == True{} : Bool}

def dmr_s source · line 30 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+al:U32 -> @+ah:U32 -> @+bl:U32 -> @+bh:U32 -> @+hb:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}) == False{} : Bool} -> @+hz:{U32.is_zero(bh) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.psnd(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.dm_pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}, True{}))) == Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh})) : Nat}

def rem_core source · line 33 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+al:U32 -> @+ah:U32 -> @+bl:U32 -> @+bh:U32 -> @+q:U32 -> @+hle:{Nat.is_le(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64dm.v(q), 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} -> @+hm:{Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh})) == Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}), Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64dm.v(q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}))) : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.fst_q(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul_32_64(q, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh})))) == Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh})) : Nat}

def le_qs source · line 41 · 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(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64dm.X96(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}, 0), Nat.mul(1n+0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64dm.v(e), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}))) == True{} : Bool} -> {Nat.is_le(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64dm.v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.q_start(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}, 0, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}, e)), 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}

def mod_qs source · line 44 · 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(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64dm.X96(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}, 0), Nat.mul(1n+0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64dm.v(e), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}))) == True{} : Bool} -> {Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh})) == Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}), Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64dm.v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.q_start(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}, 0, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}, e)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}))) : Nat}

def dmr_b source · line 52 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+al:U32 -> @+ah:U32 -> @+bl:U32 -> @+bh:U32 -> @+hb:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}) == False{} : Bool} -> @+hz:{U32.is_zero(bh) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.psnd(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.dm_pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}, False{}))) == Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh})) : Nat}

def dmr source · line 55 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+al:U32 -> @+ah:U32 -> @+bl:U32 -> @+bh:U32 -> @+hb:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}) == False{} : Bool} -> @+z:Bool -> @+hz:{U32.is_zero(bh) == z : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.psnd(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.dm_pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}, z))) == Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh})) : Nat}

def divmod_rem source · line 62 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hb:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(b) == False{} : Bool} -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.DivMod.rem(a, b, hb)