proofs/math/typed/f64divf.bend checks

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

25 imports

import Base
import ./f64light.bend as FL
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 ../../../src/math/natural.bend as M
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 ./w64add.bend as WA
import ./w64sh.bend as SH
import ./f64round.bend as FR
import ./f64rtools.bend as RT
import ./f64mulp.bend as MP
import ./f64adda.bend as AA
import ./f64divd.bend as DD
import ./w64mm.bend as MM
import ./w64est.bend as W64E
import ./f64divn.bend as DN
import ./f64divq.bend as DQ

Definitions

def v source · line 31 · raw

@+x:U32 -> Nat

def e0 source · line 34 · raw

@+rl:U32 -> @+rh:U32 -> @+ml:U32 -> @+mh:U32 -> @+t:Nat -> U32

def dq96q source · line 37 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+r:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+t:Nat -> @+hx:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(r), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(b)) == True{} : Bool} -> @+hz:{U32.is_zero(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.hi(b)) == False{} : Bool} -> @+ht:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.bitlen(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.hi(b)) == t : Nat} -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.q96(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(r)}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.hi(r), b, t)) == Nat.div(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(r)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(b)) : Nat}

def dq96r source · line 42 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+r:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+t:Nat -> @+hx:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(r), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(b)) == True{} : Bool} -> @+hz:{U32.is_zero(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.hi(b)) == False{} : Bool} -> @+ht:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.bitlen(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.hi(b)) == t : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(r)}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.fst_q(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul_32_64(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.q96(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(r)}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.hi(r), b, t), b)))) == Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(r)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(b)) : Nat}

def dm2 source · line 47 · raw

@+l:Bool -> @+r:Bool -> {Bool.or(Bool.not(r), Bool.not(l)) == Bool.not(Bool.and(l, r)) : Bool}

def nfit_mono_c source · line 50 · raw

@+a:Nat -> @+b:Nat -> @+x:Nat -> @+hab:{Nat.is_le(a, b) == True{} : Bool} -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(b, x) == False{} : Bool} -> @+c:Bool -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(a, x) == c : Bool} -> {c == False{} : Bool}

def nfit_mono source · line 53 · raw

@+a:Nat -> @+b:Nat -> @+x:Nat -> @+hab:{Nat.is_le(a, b) == True{} : Bool} -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(b, x) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(a, x) == False{} : Bool}

def dgen source · line 57 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Bool -> @+e:Nat -> @+x:Nat -> @+hx:{Nat.add(x, 2180n) == e : Nat} -> @+aw:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+bw:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+bp:Nat -> @+hBp:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(bw) == 1n+bp : Nat} -> @+MX:Nat -> @+yp:Nat -> @+u:Nat -> @+w:Nat -> @+P:Nat -> @+dp:Nat -> @+ha:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(aw) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(u, MX) : Nat} -> @+hb:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(bw) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(w, 1n+yp) : Nat} -> @+hP:{Nat.add(62n, u) == Nat.add(w, P) : Nat} -> @+hdp:{Nat.add(dp, P) == 200n : Nat} -> @+hle:{Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(bw), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(aw)) == True{} : Bool} -> @+hRlt:{Nat.is_lt(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(aw), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(bw)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(bw)) == True{} : Bool} -> @+hhi:{U32.is_zero(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.hi(bw)) == False{} : Bool} -> @+E:Nat -> @+hEx:{Nat.add(E, 1n+dp) == x : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.div_q(s, e, aw, bw) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, Nat.add(Nat.mul(2n, Nat.div(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(200n, MX), 1n+yp), 1n)), E) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

the quotient step, for a in [b, 2b), a = MX * 2^u, b = MY * 2^w, 62 + u = w + P, P + dp = 200