~/bend-docscommunity

proofs/math/random/fround.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend as Fround

24 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 ../typed/width.bend as WW
import ../typed/u32laws.bend as LW
import ../typed/w64add.bend as WA
import ../typed/f64bits.bend as FB
import ../typed/natcmp.bend as NC
import ../typed/w64sh.bend as SH
import ../../lib/u32.bend as U
import ../../lib/u32half.bend as UH
import ../../lib/u32alg.bend as A
import ../../lib/word.bend as WD
import ../../lib/lemmas/spec/numeric.bend as S
import ../../../src/math/natural.bend as M
import ../natural/bits.bend as BT
import ../typed/f64bl.bend as FO

Definitions

def bits source · line 30 · raw

@+s:Bool -> @+n:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

def enc_bits source · line 33 · raw

@+s:Bool -> @+ef:Nat -> @+f:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.encode(s, ef, f) == bits(s, Nat.add(f, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, ef))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def rne_c source · line 44 · raw

@+q:Nat -> @+c:Cmp -> Nat

def rne_cmp source · line 47 · raw

@+q:Nat -> @+r:Nat -> @+h:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rne_up(q, r, h) == rne_c(q, Nat.cmp(r, h)) : Nat}

def fz source · line 50 · raw

@+d:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(d, 0n) == True{} : Bool}

def fits_add1 source · line 57 · raw

@+k:Nat -> @+a:Nat -> @+b:Nat -> @+ha:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, a) == True{} : Bool} -> @+hb:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, b) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(1n+k, Nat.add(a, b)) == True{} : Bool}

def sub_add_r source · line 65 · raw

@+a:Nat -> @+b:Nat -> @+m:Nat -> @+h:{Nat.is_le(m, a) == True{} : Bool} -> {Nat.sub(Nat.add(a, b), m) == Nat.add(Nat.sub(a, m), b) : Nat}

def parq source · line 69 · raw

@+q:Nat -> {Nat.add(q, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.bit(q), 1n))) == Nat.double(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.half(Nat.add(q, 1n))) : Nat}

def subm source · line 78 · raw

@+n:Nat -> {Nat.sub(n, Nat.mod(n, 2n)) == Nat.double(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.half(n)) : Nat}

def rp_c source · line 81 · raw

@+q0:Nat -> @+r0:Nat -> @+hr:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(10n, r0) == True{} : Bool} -> @+c:Cmp -> @+hc:{Nat.cmp(r0, 512n) == c : Cmp} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, Nat.is_eq(r0, 512n), Nat.sub(Nat.add(q0, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(10n, Nat.add(r0, 512n))), Nat.mod(Nat.add(q0, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(10n, Nat.add(r0, 512n))), 2n)), Nat.add(q0, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(10n, Nat.add(r0, 512n)))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rne_up(q0, r0, 512n) : Nat}

def bl_gt source · line 113 · raw

@+k:Nat -> @+n:Nat -> @+h1:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, n) == False{} : Bool} -> @+h2:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(1n+k, n) == True{} : Bool} -> @+hg:{Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(2n+k), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(n))) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(n) == 1n+k : Nat}

def bl_c source · line 123 · raw

@+k:Nat -> @+n:Nat -> @+h1:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, n) == False{} : Bool} -> @+h2:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(1n+k, n) == True{} : Bool} -> @+c:Cmp -> @+hc:{Nat.cmp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(n), 1n+k) == c : Cmp} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(n) == 1n+k : Nat}

def fits_hc source · line 135 · raw

@+a:Nat -> @+b:Nat -> @+n:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(Nat.add(a, b), n) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(b, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(a, n)) : Bool}

def succ_le source · line 138 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_lt(a, b) == True{} : Bool} -> {Nat.is_le(Nat.add(a, 1n), b) == True{} : Bool}

def nfit_c source · line 141 · raw

@+k:Nat -> @+a:Nat -> @+r:Nat -> @+hle:{Nat.is_le(a, r) == True{} : Bool} -> @+f:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, a) == False{} : Bool} -> @+b:Bool -> @+hb:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, r) == b : Bool} -> {b == False{} : Bool}

def nfit source · line 148 · raw

@+k:Nat -> @+a:Nat -> @+r:Nat -> @+hle:{Nat.is_le(a, r) == True{} : Bool} -> @+f:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, a) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, r) == False{} : Bool}

def lt_fit source · line 151 · raw

@+k:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+n:Nat -> {Nat.is_lt(n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, one)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, n) : Bool}

def efv source · line 155 · raw

@+u:Nat -> @+EF:Nat -> @+hu:{Nat.add(EF, 1926n) == u : Nat} -> {Nat.sub(Nat.add(u, 1075n), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb) == 1n+EF : Nat}

def ef2v source · line 161 · raw

@+u:Nat -> @+EF:Nat -> @+hu:{Nat.add(EF, 1926n) == u : Nat} -> {Nat.sub(Nat.add(1n+u, 1075n), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb) == 2n+EF : Nat}

def hi_one source · line 167 · raw

@+H0:Nat -> @+a:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.half(H0), 0n) == True{} : Bool} -> @+b:{Nat.is_eq(H0, 0n) == False{} : Bool} -> {H0 == 1n : Nat}

def f53h source · line 176 · raw

@+q:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, q) == Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.half(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(52n, q)), 0n) : Bool}

def top_q source · line 179 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+q:Nat -> @+hq:{Nat.is_le(q, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(53n, one)) == True{} : Bool} -> @+hf:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, q) == False{} : Bool} -> {q == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, Nat.double(one)) : Nat}

def pkg_c source · line 184 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Bool -> @+q:Nat -> @+u:Nat -> @+EF:Nat -> @+hEF:{Nat.add(EF, 1926n) == u : Nat} -> @+hq:{Nat.is_le(q, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(53n, one)) == True{} : Bool} -> @+f53:Bool -> @+h53:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, q) == f53 : Bool} -> @+f52:Bool -> @+h52:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, q) == f52 : Bool} -> @+h0:{Bool.or(Bool.not(f52), Nat.is_eq(EF, 0n)) == True{} : Bool} -> @+hov:{Nat.is_lt(Nat.add(EF, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, f53, 1n, 2n)), 2047n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, f53, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, f52, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.encode(s, 0n, q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pack_e(s, Nat.sub(Nat.add(u, 1075n), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(52n, q))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pack_e(s, Nat.sub(Nat.add(1n+u, 1075n), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb), 0n)) == bits(s, Nat.add(q, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, EF))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def pkg source · line 211 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Bool -> @+q:Nat -> @+u:Nat -> @+EF:Nat -> @+hEF:{Nat.add(EF, 1926n) == u : Nat} -> @+hq:{Nat.is_le(q, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(53n, one)) == True{} : Bool} -> @+h0:{Bool.or(Bool.not(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, q)), Nat.is_eq(EF, 0n)) == True{} : Bool} -> @+hov:{Nat.is_lt(Nat.add(EF, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, q), 1n, 2n)), 2047n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pack(s, q, u) == bits(s, Nat.add(q, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, EF))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def hsp source · line 214 · raw

@+m:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(10n, Nat.add(m, 512n)) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(10n, m), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(10n, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(10n, m), 512n))) : Nat}

def mod_sh source · line 217 · raw

@+k:Nat -> @+x:Nat -> {Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(1n+k, x), 2n) == 0n : Nat}

def fsub_c source · line 220 · raw

@+k:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+R0:Nat -> @+hR:{Nat.is_le(R0, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(1n+k, one)) == True{} : Bool} -> @+f:Bool -> @+hf:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(1n+k, R0) == f : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(1n+k, Nat.sub(R0, Nat.mod(R0, 2n))) == f : Bool}

def fpk source · line 231 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+R0:Nat -> @+hR:{Nat.is_le(R0, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(53n, one)) == True{} : Bool} -> @+t:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, t, Nat.sub(R0, Nat.mod(R0, 2n)), R0)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, R0) : Bool}

def le1 source · line 238 · raw

@+t:Nat -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(1n, t) == True{} : Bool} -> {Nat.is_le(t, 1n) == True{} : Bool}

def R_le source · line 247 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+m:Nat -> @+hm:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, m) == True{} : Bool} -> {Nat.is_le(Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(10n, m), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(10n, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(10n, m), 512n))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(53n, one)) == True{} : Bool}

def p2 source · line 253 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+m:Nat -> @+hm:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, m) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rne(m, 10n)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, Nat.add(m, 512n)) : Bool}

def sub_cancel_r source · line 260 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> {Nat.sub(Nat.add(a, c), Nat.add(b, c)) == Nat.sub(a, b) : Nat}

def lt0f source · line 267 · raw

@+h:Nat -> {Nat.is_lt(h, 0n) == False{} : Bool}

def rne_exact source · line 270 · raw

@+k:Nat -> @+m:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rne(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, m), k) == m : Nat}

def rne_shift source · line 287 · raw

@+k:Nat -> @+m:Nat -> @+j:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rne(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, m), Nat.add(j, k)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rne(m, j) : Nat}

def bl_fit source · line 304 · raw

@+n:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(n), n) == True{} : Bool}

def bl_nfit source · line 307 · raw

@+n:Nat -> @+hz:{Nat.is_eq(n, 0n) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(n), 1n), n) == False{} : Bool}

def fits_sh source · line 312 · raw

@+k:Nat -> @+a:Nat -> @+m:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(Nat.add(k, a), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, m)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(a, m) : Bool}

def bl_shift source · line 315 · raw

@+k:Nat -> @+m:Nat -> @+hz:{Nat.is_eq(m, 0n) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, m)) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(m), k) : Nat}

def a1 source · line 327 · raw

@+x:Nat -> @+k:Nat -> @+u:Nat -> @+h:{Nat.is_le(Nat.add(x, k), u) == True{} : Bool} -> {Nat.sub(u, x) == Nat.add(Nat.sub(u, Nat.add(x, k)), k) : Nat}

def qeq_f source · line 332 · raw

@+k:Nat -> @+m:Nat -> @+x:Nat -> @+u:Nat -> @+c1:Bool -> @+hc1:{Nat.is_le(x, u) == c1 : Bool} -> @+hc2:{Nat.is_le(Nat.add(x, k), u) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, c1, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rne(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, m), Nat.sub(u, x)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(x, u), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, m))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(Nat.add(x, k), u), m) : Nat}

def qeq_c source · line 349 · raw

@+k:Nat -> @+m:Nat -> @+x:Nat -> @+u:Nat -> @+c1:Bool -> @+hc1:{Nat.is_le(x, u) == c1 : Bool} -> @+c2:Bool -> @+hc2:{Nat.is_le(Nat.add(x, k), u) == c2 : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, c1, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rne(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, m), Nat.sub(u, x)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(x, u), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, m))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, c2, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rne(m, Nat.sub(u, Nat.add(x, k))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(Nat.add(x, k), u), m)) : Nat}

def rs_c source · line 360 · raw

@+s:Bool -> @+k:Nat -> @+m:Nat -> @+x:Nat -> @+z:Bool -> @+hz:{Nat.is_eq(m, 0n) == z : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, m), x) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, m, Nat.add(x, k)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def round_shift source · line 376 · raw

@+s:Bool -> @+k:Nat -> @+m:Nat -> @+x:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, m), x) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, m, Nat.add(x, k)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}