proofs/math/typed/f64divq.bend checks
raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divq.bend as F64divq
22 imports
import Base import ../../../spec/lib/common.bend as C import ../../../spec/math/f64.bend as SF import ../../../spec/math/w64.bend as SW import ../../../src/math/f64.bend as F 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 ./width.bend as WW import ./u32laws.bend as LW import ./w64add.bend as WA import ./w64sh.bend as SH import ./w64dm.bend as DM import ./f64bits.bend as FB import ./f64round.bend as FR import ./f64rtools.bend as RT import ./f64mulp.bend as MP import ./f64addb.bend as AB import ./f64divn.bend as DN
Definitions
def v source · line 27 · raw
@+x:U32 -> Nat
def lowq source · line 31 · raw
@+d1:U32 -> @+d2:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(2n, v(d2)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(2n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{d2, d1})) : Nat}the low two bits of Q come from its low digit
def flag_v source · line 36 · raw
@+d1:U32 -> @+d2:U32 -> @+r2w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {Bool.or(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.nz(r2w), Bool.not(U32.is_zero(U32.and(d2, 3)))) == Bool.or(Bool.not(Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(r2w), 0n)), Bool.not(Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(2n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{d2, d1})), 0n))) : Bool}
def hq62 source · line 42 · raw
@+d1:U32 -> @+d2:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(2n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{d2, d1}))) == True{} : Bool}
def t63 source · line 45 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+d1:U32 -> @+d2:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(62n, one), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(2n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{d2, d1})))) == True{} : Bool}
def t62 source · line 49 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+d1:U32 -> @+d2:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(62n, one), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(2n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{d2, d1})))) == False{} : Bool}
def w1_v source · line 52 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+d1:U32 -> @+d2:U32 -> @+c:U32 -> @+hc:{c == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(32n, 30n)} : U32} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, c}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shr(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{d2, d1}, 2n))) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(62n, one), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(2n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{d2, d1}))) : Nat}
def sig_v source · line 59 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+d1:U32 -> @+d2:U32 -> @+r2w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+c:U32 -> @+hc:{c == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(32n, 30n)} : U32} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.or_bit(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, c}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shr(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{d2, d1}, 2n)), Bool.or(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.nz(r2w), Bool.not(U32.is_zero(U32.and(d2, 3)))))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(62n, one), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(2n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{d2, d1}))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(Bool.or(Bool.not(Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(r2w), 0n)), Bool.not(Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(2n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{d2, d1})), 0n))))) : Nat}
def dq_round source · line 66 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Bool -> @+e:Nat -> @+x:Nat -> @+hx:{Nat.add(x, 2180n) == e : Nat} -> @+d1:U32 -> @+d2:U32 -> @+r2w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+c:U32 -> @+hc:{c == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(32n, 30n)} : U32} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.round_pack(s, e, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.or_bit(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, c}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shr(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{d2, d1}, 2n)), Bool.or(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.nz(r2w), Bool.not(U32.is_zero(U32.and(d2, 3)))))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(62n, one), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(2n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{d2, d1}))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(Bool.or(Bool.not(Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(r2w), 0n)), Bool.not(Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(2n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{d2, d1})), 0n))))), x) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}roundPackToF64 of the quotient significand is the spec's round of its value
def iq_T source · line 75 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bp:Nat -> @+R:Nat -> @+Q:Nat -> @+r2:Nat -> @+hQ:{Nat.add(Nat.mul(Q, 1n+bp), r2) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, R) : Nat} -> {Nat.add(Nat.mul(Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(62n, one), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(2n, Q)), 1n+bp), Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(62n, R), Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(2n, Q), 1n+bp))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(62n, Nat.add(R, 1n+bp)) : Nat}a * 2^62 = T * b + e for a = (a - b) + b