def round_pack

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64round.bend:917

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/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

917# SoftFloat's roundPackToF64(s, e, sig), sig with its top bit at 62 and e the
918# biased exponent minus one plus OFF, is Flocq's round_NE of s * sig * 2^(e - 2180 - Z)
919def round_pack(+s: Bool, +e: Nat, +sig: WU.U64, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +h62: {C.fits(62n, SW.value(sig)) == False{} : Bool}, +h63: {C.fits(63n, SW.value(sig)) == True{} : Bool}) -> {F.round_pack(s, e, sig) == SF.round(s, SW.value(sig), x) : F.F64}:
920  +elt = Equal.trans(Bool, Nat.is_lt(e, F.off()), Nat.is_lt(Nat.add(x, 2180n), F.off()), Nat.is_lt(x, 1916n), Equal.cong(Nat, Bool, z => Nat.is_lt(z, F.off()), e, Nat.add(x, 2180n), Equal.sym(Nat, Nat.add(x, 2180n), e, hx)), WW.lt_cancel_r(x, 1916n, 2180n))
921  +i1 = Equal.cong(Bool, F.F64, t => F.rp_neg(s, e, sig, t), Nat.is_lt(e, F.off()), Nat.is_lt(x, 1916n), elt)
922  +i2 = rp_c2(1n, {==}, s, e, sig, x, hx, h62, h63, Nat.is_lt(x, 1916n), {==}, Nat.max(Nat.add(10n, x), 1926n), {==})
923  +s0 = sr(s, SW.value(sig), x, h62, h63)
924  Equal.trans(F.F64, F.rp_neg(s, e, sig, Nat.is_lt(e, F.off())), SF.round_u(s, SW.value(sig), x, Nat.max(Nat.add(10n, x), 1926n)), SF.round(s, SW.value(sig), x), Equal.trans(F.F64, F.rp_neg(s, e, sig, Nat.is_lt(e, F.off())), F.rp_neg(s, e, sig, Nat.is_lt(x, 1916n)), SF.round_u(s, SW.value(sig), x, Nat.max(Nat.add(10n, x), 1926n)), i1, i2), Equal.sym(F.F64, SF.round(s, SW.value(sig), x), SF.round_u(s, SW.value(sig), x, Nat.max(Nat.add(10n, x), 1926n)), s0))