~/bend-docscommunity

proofs/math/typed/f64divd.bend checks

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

13 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 ./width.bend as WW
import ./u32laws.bend as LW
import ./w64dm.bend as DM
import ./w64mm.bend as MM

Definitions

def v source · line 19 · raw

@+x:U32 -> Nat

def dig_r source · line 23 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+rl:U32 -> @+rh:U32 -> @+ml:U32 -> @+mh:U32 -> @+e:U32 -> @+hx:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{rl, rh}), 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{0, rl}, rh), 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{0, rl}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.fst_q(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul_32_64(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.q_start(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, rl}, rh, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh}, e), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh})))) == Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{rl, rh})), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh})) : Nat}

the remainder digit

def dig_q source · line 27 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+rl:U32 -> @+rh:U32 -> @+ml:U32 -> @+mh:U32 -> @+e:U32 -> @+hx:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{rl, rh}), 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{0, rl}, rh), Nat.mul(1n+v(e), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh}))) == True{} : Bool} -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.q_start(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, rl}, rh, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh}, e)) == Nat.div(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{rl, rh})), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh})) : Nat}

the quotient digit

def sh_mul source · line 46 · raw

@+k:Nat -> @+q:Nat -> @+b:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, Nat.mul(q, b)) == Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, q), b) : Nat}

shifting a product shifts one factor

def two source · line 59 · raw

@+bp:Nat -> @+R:Nat -> @+q1:Nat -> @+r1:Nat -> @+q2:Nat -> @+r2:Nat -> @+e1:{q1 == Nat.div(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, R), 1n+bp) : Nat} -> @+f1:{r1 == Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, R), 1n+bp) : Nat} -> @+e2:{q2 == Nat.div(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, r1), 1n+bp) : Nat} -> @+f2:{r2 == Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, r1), 1n+bp) : Nat} -> {Nat.add(Nat.mul(Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, q1), q2), 1n+bp), r2) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, R) : Nat}

two digits: r * 2^64 = (q1 * 2^32 + q2) * b + r2