def pack

bend-collections-laws-crypto@1.0.0.0 · spec/math/f64.bend:168

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/src/math/f64.bend as F

168# the double nearest to (-1)^s * q * 2^(u - Z) for a q of at most 53 bits at
169# the ulp u (subnormal when q < 2^52), carrying a rounded-up q = 2^53 into
170# 2^52 at the ulp 1 + u
171def pack(+s: Bool, +q: Nat, +u: Nat) -> F.F64:
172  pick(F.F64, C.fits(53n, q), pack_n(s, q, u), pack_e(s, Nat.sub(Nat.add(1n+u, 1075n), zb()), 0n))