def below_one

bend-collections-laws-math@1.0.0.0 · proofs/math/random/float.bend:391

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB

391# a double Bits{l, hw(E, qh)} with E < k <= 2047 is below Bits{0, H} whose
392# high word (without sign) is k * 2^20
393def below_one(+l: U32, +qh: U32, +E: Nat, +H: U32, +K: U32, +k: Nat, +hE: {Nat.is_lt(E, k) == True{} : Bool}, +hk: {C.fits(11n, k) == True{} : Bool}, +hn: {F.is_nan(F.Bits{0, H}) == False{} : Bool}, +hz: {F.is_zero(F.Bits{0, H}) == False{} : Bool}, +hs: {F.signbit(F.Bits{0, H}) == False{} : Bool}, +hH: {U32.and(H, 2147483647) == U32.mul(K, X.pow2(20n)) : U32}, +hK: {U32.to_nat(K) == k : Nat}) -> {F.lt(F.Bits{l, hw(E, qh)}, F.Bits{0, H}) == True{} : Bool}:
394  +h = hw(E, qh)
395  +x = {F.Bits{l, h} : F.F64}
396  +y = {F.Bits{0, H} : F.F64}
397  +lq = C.low(20n, v(qh))
398  +hk2 = WW.lt_of_fits(11n, k, hk)
399  +he = N.lt_trans(E, k, 2048n, hE, hk2)
400  +hk12 = SH.fits_mono(11n, 12n, k, {==}, hk)
401  +vh = hw_value(1n, {==}, E, qh, he)
402  +f11 = fits_lt11(E, he)
403  +f31 = Equal.trans(Bool, C.fits(31n, v(h)), C.fits(31n, Nat.add(lq, C.shift(20n, E))), True{}, Equal.cong(Nat, Bool, z => C.fits(31n, z), v(h), Nat.add(lq, C.shift(20n, E)), vh), WW.limbs_fit(20n, 11n, lq, E, WW.low_fits(20n, v(qh)), f11))
404  +ef = Equal.trans(Nat, v(U32.and(U32.div(h, 1048576), 2047)), C.low(11n, C.high(20n, v(h))), E, FB.ef_g(1n, {==}, h, 1048576, {==}, 2047, {==}),
405    Equal.trans(Nat, C.low(11n, C.high(20n, v(h))), C.low(11n, E), E,
406      Equal.cong(Nat, Nat, z => C.low(11n, z), C.high(20n, v(h)), E, Equal.trans(Nat, C.high(20n, v(h)), C.high(20n, Nat.add(lq, C.shift(20n, E))), E, Equal.cong(Nat, Nat, z => C.high(20n, z), v(h), Nat.add(lq, C.shift(20n, E)), vh), WW.high_u(20n, lq, E, WW.low_fits(20n, v(qh))))),
407      WW.low_fit(11n, E, f11)))
408  +hne = N.is_eq_lt(E, 2047n, N.lt_le_trans(E, k, 2047n, hE, N.lt_succ_le(k, 2047n, hk2)))
409  +nanx = Equal.trans(Bool, F.is_nan(x), Bool.and(Nat.is_eq(E, 2047n), F.nz(F.frac(x))), False{},
410    Equal.cong(Nat, Bool, z => Bool.and(Nat.is_eq(z, 2047n), F.nz(F.frac(x))), v(U32.and(U32.div(h, 1048576), 2047)), E, ef),
411    Equal.cong(Bool, Bool, z => Bool.and(z, F.nz(F.frac(x))), Nat.is_eq(E, 2047n), False{}, hne))
412  +uo = Equal.trans(Bool, F.unordered(x, y), Bool.or(False{}, F.is_nan(y)), False{}, Equal.cong(Bool, Bool, z => Bool.or(z, F.is_nan(y)), F.is_nan(x), False{}, nanx), hn)
413  +zs = Equal.trans(Bool, F.zeros(x, y), Bool.and(F.is_zero(x), False{}), False{}, Equal.cong(Bool, Bool, z => Bool.and(F.is_zero(x), z), F.is_zero(y), False{}, hz), and_f(F.is_zero(x)))
414  +sx = Equal.trans(Bool, F.signbit(x), SF.sign(x), False{}, FB.signbit_g(1n, {==}, l, h, 2147483648, {==}),
415    Equal.cong(Bool, Bool, z => Bool.not(z), C.fits(31n, v(h)), True{}, f31))
416  +vmx = Equal.trans(Nat, SW.value(F.mag(x)), Nat.add(v(l), C.shift(32n, C.low(31n, v(h)))), Nat.add(v(l), C.shift(32n, v(h))),
417    Equal.cong(Nat, Nat, z => Nat.add(v(l), C.shift(32n, z)), v(U32.and(h, 2147483647)), C.low(31n, v(h)), FB.andm(h, 31n, 2147483647, {==})),
418    Equal.cong(Nat, Nat, z => Nat.add(v(l), C.shift(32n, z)), C.low(31n, v(h)), v(h), WW.low_fit(31n, v(h), f31)))
419  +vmy = Equal.cong(Nat, Nat, z => C.shift(32n, z), v(U32.and(H, 2147483647)), C.shift(20n, k), hv_one(H, K, k, hk12, hH, hK))
420  +hvh = Equal.trans(Bool, Nat.is_lt(v(h), C.shift(20n, k)), Nat.is_lt(Nat.add(lq, C.shift(20n, E)), C.shift(20n, k)), True{}, Equal.cong(Nat, Bool, z => Nat.is_lt(z, C.shift(20n, k)), v(h), Nat.add(lq, C.shift(20n, E)), vh), WW.lt_hi(20n, lq, E, 0n, k, WW.low_fits(20n, v(qh)), hE))
421  +hlt = WW.lt_hi(32n, v(l), v(h), 0n, C.shift(20n, k), LW.vb(l), hvh)
422  +cmp = Equal.trans(Bool, X.lt(F.mag(x), F.mag(y)), Nat.is_lt(SW.value(F.mag(x)), SW.value(F.mag(y))), True{}, WA.lt_value(F.mag(x), F.mag(y)),
423    Equal.trans(Bool, Nat.is_lt(SW.value(F.mag(x)), SW.value(F.mag(y))), Nat.is_lt(Nat.add(v(l), C.shift(32n, v(h))), C.shift(32n, C.shift(20n, k))), True{},
424      Equal.trans(Bool, Nat.is_lt(SW.value(F.mag(x)), SW.value(F.mag(y))), Nat.is_lt(Nat.add(v(l), C.shift(32n, v(h))), SW.value(F.mag(y))), Nat.is_lt(Nat.add(v(l), C.shift(32n, v(h))), C.shift(32n, C.shift(20n, k))),
425        Equal.cong(Nat, Bool, z => Nat.is_lt(z, SW.value(F.mag(y))), SW.value(F.mag(x)), Nat.add(v(l), C.shift(32n, v(h))), vmx),
426        Equal.cong(Nat, Bool, z => Nat.is_lt(Nat.add(v(l), C.shift(32n, v(h))), z), SW.value(F.mag(y)), C.shift(32n, C.shift(20n, k)), vmy)),
427      hlt))
428  +c1 = Equal.cong(Bool, Bool, z => F.lt_z(x, y, z, F.zeros(x, y)), F.unordered(x, y), False{}, uo)
429  +c2 = Equal.cong(Bool, Bool, z => F.lt_z(x, y, False{}, z), F.zeros(x, y), False{}, zs)
430  +c3 = Equal.cong(Bool, Bool, z => F.lt_s(x, y, z, F.signbit(y)), F.signbit(x), False{}, sx)
431  +c4 = Equal.cong(Bool, Bool, z => F.lt_s(x, y, False{}, z), F.signbit(y), False{}, hs)
432  Equal.trans(Bool, F.lt(x, y), F.lt_z(x, y, False{}, F.zeros(x, y)), True{}, c1,
433    Equal.trans(Bool, F.lt_z(x, y, False{}, F.zeros(x, y)), F.lt_z(x, y, False{}, False{}), True{}, c2,
434      Equal.trans(Bool, F.lt_s(x, y, F.signbit(x), F.signbit(y)), F.lt_s(x, y, False{}, F.signbit(y)), True{}, c3,
435        Equal.trans(Bool, F.lt_s(x, y, False{}, F.signbit(y)), F.lt_s(x, y, False{}, False{}), True{}, c4, cmp))))