proofs/math/typed/f64mulf.bend

bend-collections-laws-math@1.0.0.0 · 88 lines · 8 definitions

1import Base
2import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
4import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
5import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
6import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
7import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
8import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
9import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
10import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
11import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
12import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
13import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH
14import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as NC
15import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB
16import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend as FC
17import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend as RT
18import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64norm.bend as NM
19import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mexp.bend as EX
20import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mul.bend as MU
21
22# Mul.value of spec/math/f64.bend: the finite nonzero product.
23
24def v(+x: U32) -> Nat:
25  U32.to_nat(x)
26
27# ---- fields of the operands ----
28
29def hea(+xl: U32, +xh: U32) -> {F.exp_field(F.Bits{xl, xh}) == SF.efield(F.Bits{xl, xh}) : Nat}:
30  FB.ef_g(1n, {==}, xh, 1048576, {==}, 2047, {==})
31
32def fval_g(+xl: U32, +xh: U32, +m: U32, +hm: {m == U32{WD.mask(32n, 20n)} : U32}) -> {SW.value(WU.U64{xl, U32.and(xh, m)}) == SF.frac(F.Bits{xl, xh}) : Nat}:
33  Equal.cong(Nat, Nat, z => Nat.add(v(xl), C.shift(32n, z)), v(U32.and(xh, m)), C.low(20n, v(xh)), FB.andm(xh, 20n, m, hm))
34
35def hfa(+xl: U32, +xh: U32) -> {SW.value(F.frac(F.Bits{xl, xh})) == SF.frac(F.Bits{xl, xh}) : Nat}:
36  fval_g(xl, xh, 1048575, {==})
37
38def nlb(+s: Bool, +k: Nat, +m: Nat, +x: Nat, +hk: {C.fits(k, m) == False{} : Bool}, +c: Bool, +hc: {Nat.is_le(1n+k, M.bit_length(m)) == c : Bool}) -> {c == True{} : Bool}:
39  match c:
40    case True{}:
41      {==}
42    case False{}:
43      +h1 = N.lt_succ_le(M.bit_length(m), k, N.not_le_lt(1n+k, M.bit_length(m), hc))
44      NC.absurd_tf({False{} == True{} : Bool}, Equal.trans(Bool, False{}, C.fits(k, m), True{}, Equal.sym(Bool, C.fits(k, m), False{}, hk), SH.fits_mono(M.bit_length(m), k, m, h1, RT.bl_fit(m))))
45
46def nfit_bl(+k: Nat, +m: Nat, +hk: {C.fits(k, m) == False{} : Bool}) -> {Nat.is_le(1n+k, M.bit_length(m)) == True{} : Bool}:
47  nlb(False{}, k, m, 0n, hk, Nat.is_le(1n+k, M.bit_length(m)), {==})
48
49def smul(+k: Nat, +j: Nat, +x: Nat, +y: Nat) -> {Nat.mul(C.shift(k, x), C.shift(j, y)) == C.shift(Nat.add(k, j), Nat.mul(x, y)) : Nat}:
50  Equal.trans(Nat, Nat.mul(C.shift(k, x), C.shift(j, y)), C.shift(k, Nat.mul(x, C.shift(j, y))), C.shift(Nat.add(k, j), Nat.mul(x, y)), WW.shift_mul_l(k, x, C.shift(j, y)), Equal.trans(Nat, C.shift(k, Nat.mul(x, C.shift(j, y))), C.shift(k, C.shift(j, Nat.mul(x, y))), C.shift(Nat.add(k, j), Nat.mul(x, y)), Equal.cong(Nat, Nat, z => C.shift(k, z), Nat.mul(x, C.shift(j, y)), C.shift(j, Nat.mul(x, y)), WW.shift_mul_r(j, x, y)), Equal.sym(Nat, C.shift(Nat.add(k, j), Nat.mul(x, y)), C.shift(k, C.shift(j, Nat.mul(x, y))), WW.shift_comp(k, j, Nat.mul(x, y)))))
51
52# ---- two finite nonzero operands ----
53
54def mfin(+s: Bool, +xl: U32, +xh: U32, +yl: U32, +yh: U32, +hzx: {Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n)) == False{} : Bool}, +hzy: {Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n)) == False{} : Bool}) -> {F.mul_n(s, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_e(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))) == SF.round(s, Nat.mul(SF.mant(F.Bits{xl, xh}), SF.mant(F.Bits{yl, yh})), Nat.sub(Nat.add(SF.xexp(F.Bits{xl, xh}), SF.xexp(F.Bits{yl, yh})), SF.zb())) : F.F64}:
55  +n1x = NM.n1(1n, {==}, F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), hea(xl, xh), hfa(xl, xh), FC.hF(xl, xh), hzx)
56  +n1y = NM.n1(1n, {==}, F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}), SF.efield(F.Bits{yl, yh}), SF.frac(F.Bits{yl, yh}), hea(yl, yh), hfa(yl, yh), FC.hF(yl, yh), hzy)
57  +n2x = NM.n2(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), hea(xl, xh), hfa(xl, xh), FC.hF(xl, xh), hzx)
58  +n2y = NM.n2(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}), SF.efield(F.Bits{yl, yh}), SF.frac(F.Bits{yl, yh}), hea(yl, yh), hfa(yl, yh), FC.hF(yl, yh), hzy)
59  +a53 = NM.n3a(1n, {==}, F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), hea(xl, xh), hfa(xl, xh), FC.hF(xl, xh), hzx)
60  +b53 = NM.n3a(1n, {==}, F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}), SF.efield(F.Bits{yl, yh}), SF.frac(F.Bits{yl, yh}), hea(yl, yh), hfa(yl, yh), FC.hF(yl, yh), hzy)
61  +a52 = NM.n3b(1n, {==}, F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), hea(xl, xh), hfa(xl, xh), FC.hF(xl, xh), hzx)
62  +b52 = NM.n3b(1n, {==}, F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}), SF.efield(F.Bits{yl, yh}), SF.frac(F.Bits{yl, yh}), hea(yl, yh), hfa(yl, yh), FC.hF(yl, yh), hzy)
63  +eA = MU.shl_v(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 10n, 53n, {==}, {==}, a53)
64  +eB = MU.shl_v(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), 11n, 53n, {==}, {==}, b53)
65  +hp = Equal.trans(Nat, Nat.add(SW.value(X.pfst(X.mul128(X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 10n), X.shl(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), 11n)))), C.shift(64n, SW.value(X.psnd(X.mul128(X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 10n), X.shl(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), 11n)))))), Nat.mul(SW.value(X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 10n)), SW.value(X.shl(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), 11n))), Nat.mul(C.shift(10n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(11n, SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))))), MU.m128g(X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 10n), X.shl(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), 11n)), Equal.trans(Nat, Nat.mul(SW.value(X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 10n)), SW.value(X.shl(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), 11n))), Nat.mul(C.shift(10n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), SW.value(X.shl(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), 11n))), Nat.mul(C.shift(10n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(11n, SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))))), Equal.cong(Nat, Nat, z => Nat.mul(z, SW.value(X.shl(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), 11n))), SW.value(X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 10n)), C.shift(10n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), eA), Equal.cong(Nat, Nat, z => Nat.mul(C.shift(10n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), z), SW.value(X.shl(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), 11n)), C.shift(11n, SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})))), eB)))
66  +eP = smul(10n, 11n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))))
67  +f106 = MU.fits_mul(53n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), a53, b53)
68  +n104 = MU.nfits_mul(52n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), a52, b52)
69  +h127 = L.subst(Nat, z => {C.fits(127n, z) == True{} : Bool}, C.shift(21n, Nat.mul(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))))), Nat.mul(C.shift(10n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(11n, SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))))), Equal.sym(Nat, Nat.mul(C.shift(10n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(11n, SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))))), C.shift(21n, Nat.mul(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))))), eP), Equal.trans(Bool, C.fits(Nat.add(21n, 106n), C.shift(21n, Nat.mul(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})))))), C.fits(106n, Nat.mul(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))))), True{}, RT.fits_sh(21n, 106n, Nat.mul(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))))), f106))
70  +h125 = L.subst(Nat, z => {C.fits(125n, z) == False{} : Bool}, C.shift(21n, Nat.mul(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))))), Nat.mul(C.shift(10n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(11n, SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))))), Equal.sym(Nat, Nat.mul(C.shift(10n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(11n, SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))))), C.shift(21n, Nat.mul(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))))), eP), Equal.trans(Bool, C.fits(Nat.add(21n, 104n), C.shift(21n, Nat.mul(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})))))), C.fits(104n, Nat.mul(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))))), False{}, RT.fits_sh(21n, 104n, Nat.mul(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))))), n104))
71  +hx = EX.x_eq(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_e(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), NM.sa(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), SF.xexp(F.Bits{xl, xh}), SF.xexp(F.Bits{yl, yh}), n2x, n2y, EX.sa_le(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), EX.sa_le(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), EX.xexp_ge(SF.efield(F.Bits{xl, xh})), EX.xexp_ge(SF.efield(F.Bits{yl, yh})))
72  +hx1 = N.le_trans(1n, 64n, Nat.sub(Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_e(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), Nat.add(F.off(), 1023n)), 2180n), {==}, EX.x_ge(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_e(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), NM.sa(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), SF.xexp(F.Bits{xl, xh}), SF.xexp(F.Bits{yl, yh}), n2x, n2y, EX.sa_le(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), EX.sa_le(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), EX.xexp_ge(SF.efield(F.Bits{xl, xh})), EX.xexp_ge(SF.efield(F.Bits{yl, yh}))))
73  +r1 = MU.mcore(s, Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_e(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), Nat.add(F.off(), 1023n)), X.mul128(X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 10n), X.shl(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), 11n)), Nat.mul(C.shift(10n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(11n, SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))))), hp, Nat.sub(Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_e(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), Nat.add(F.off(), 1023n)), 2180n), hx, hx1, h127, h125)
74  +ex0 = EX.x0_eq(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_e(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), NM.sa(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), SF.xexp(F.Bits{xl, xh}), SF.xexp(F.Bits{yl, yh}), n2x, n2y, EX.sa_le(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), EX.sa_le(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), EX.xexp_ge(SF.efield(F.Bits{xl, xh})), EX.xexp_ge(SF.efield(F.Bits{yl, yh})))
75  +r2 = Equal.cong(Nat, F.F64, z => SF.round(s, SW.jam(C.high(64n, Nat.mul(C.shift(10n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(11n, SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})))))), C.low(64n, Nat.mul(C.shift(10n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(11n, SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))))))), z), Nat.sub(Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_e(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), Nat.add(F.off(), 1023n)), 2180n), Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_e(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), Nat.add(F.off(), 1023n)), 2180n), 64n), 64n), Equal.sym(Nat, Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_e(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), Nat.add(F.off(), 1023n)), 2180n), 64n), 64n), Nat.sub(Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_e(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), Nat.add(F.off(), 1023n)), 2180n), ex0))
76  +hb = N.le_trans(Nat.add(64n, 55n), 126n, M.bit_length(Nat.mul(C.shift(10n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(11n, SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})))))), {==}, nfit_bl(125n, Nat.mul(C.shift(10n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(11n, SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))))), h125))
77  +r3 = Equal.sym(F.F64, SF.round(s, Nat.mul(C.shift(10n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(11n, SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))))), Nat.sub(Nat.sub(Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_e(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), Nat.add(F.off(), 1023n)), 2180n), 64n)), SF.round(s, SW.jam(C.high(64n, Nat.mul(C.shift(10n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(11n, SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})))))), C.low(64n, Nat.mul(C.shift(10n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(11n, SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))))))), Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_e(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), Nat.add(F.off(), 1023n)), 2180n), 64n), 64n)), RT.round_jam(s, 64n, Nat.mul(C.shift(10n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(11n, SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))))), Nat.sub(Nat.sub(Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_e(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), Nat.add(F.off(), 1023n)), 2180n), 64n), hb))
78  +r4 = Equal.cong(Nat, F.F64, z => SF.round(s, z, Nat.sub(Nat.sub(Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_e(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), Nat.add(F.off(), 1023n)), 2180n), 64n)), Nat.mul(C.shift(10n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(11n, SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))))), C.shift(21n, Nat.mul(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))))), eP)
79  +r5 = RT.round_shift(s, 21n, Nat.mul(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})))), Nat.sub(Nat.sub(Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_e(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), Nat.add(F.off(), 1023n)), 2180n), 64n))
80  +eM = Equal.trans(Nat, Nat.mul(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})))), Nat.mul(C.shift(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh})), SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})))), Nat.mul(C.shift(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh})), C.shift(NM.sa(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), SF.mant(F.Bits{yl, yh}))), Equal.cong(Nat, Nat, z => Nat.mul(z, SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), C.shift(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh})), n1x), Equal.cong(Nat, Nat, z => Nat.mul(C.shift(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh})), z), SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), C.shift(NM.sa(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), SF.mant(F.Bits{yl, yh})), n1y))
81  +eM2 = Equal.trans(Nat, Nat.mul(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})))), Nat.mul(C.shift(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh})), C.shift(NM.sa(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), SF.mant(F.Bits{yl, yh}))), C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), NM.sa(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), Nat.mul(SF.mant(F.Bits{xl, xh}), SF.mant(F.Bits{yl, yh}))), eM, smul(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), NM.sa(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), SF.mant(F.Bits{xl, xh}), SF.mant(F.Bits{yl, yh})))
82  +r6 = Equal.cong(Nat, F.F64, z => SF.round(s, z, Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_e(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n)), Nat.mul(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})))), C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), NM.sa(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), Nat.mul(SF.mant(F.Bits{xl, xh}), SF.mant(F.Bits{yl, yh}))), eM2)
83  +r7 = RT.round_shift(s, Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), NM.sa(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), Nat.mul(SF.mant(F.Bits{xl, xh}), SF.mant(F.Bits{yl, yh})), Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_e(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n))
84  +r8 = Equal.cong(Nat, F.F64, z => SF.round(s, Nat.mul(SF.mant(F.Bits{xl, xh}), SF.mant(F.Bits{yl, yh})), z), Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_e(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), NM.sa(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})))), Nat.sub(Nat.add(SF.xexp(F.Bits{xl, xh}), SF.xexp(F.Bits{yl, yh})), SF.zb()), EX.mexp(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_e(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), NM.sa(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), SF.xexp(F.Bits{xl, xh}), SF.xexp(F.Bits{yl, yh}), n2x, n2y, EX.sa_le(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), EX.sa_le(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), EX.xexp_ge(SF.efield(F.Bits{xl, xh})), EX.xexp_ge(SF.efield(F.Bits{yl, yh}))))
85  Equal.trans(F.F64, F.mul_n(s, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_e(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), SF.round(s, SW.jam(C.high(64n, Nat.mul(C.shift(10n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(11n, SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})))))), C.low(64n, Nat.mul(C.shift(10n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(11n, SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))))))), Nat.sub(Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_e(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), Nat.add(F.off(), 1023n)), 2180n)), SF.round(s, Nat.mul(SF.mant(F.Bits{xl, xh}), SF.mant(F.Bits{yl, yh})), Nat.sub(Nat.add(SF.xexp(F.Bits{xl, xh}), SF.xexp(F.Bits{yl, yh})), SF.zb())), r1, Equal.trans(F.F64, SF.round(s, SW.jam(C.high(64n, Nat.mul(C.shift(10n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(11n, SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})))))), C.low(64n, Nat.mul(C.shift(10n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(11n, SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))))))), Nat.sub(Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_e(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), Nat.add(F.off(), 1023n)), 2180n)), SF.round(s, SW.jam(C.high(64n, Nat.mul(C.shift(10n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(11n, SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})))))), C.low(64n, Nat.mul(C.shift(10n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(11n, SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))))))), Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_e(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), Nat.add(F.off(), 1023n)), 2180n), 64n), 64n)), SF.round(s, Nat.mul(SF.mant(F.Bits{xl, xh}), SF.mant(F.Bits{yl, yh})), Nat.sub(Nat.add(SF.xexp(F.Bits{xl, xh}), SF.xexp(F.Bits{yl, yh})), SF.zb())), r2, Equal.trans(F.F64, SF.round(s, SW.jam(C.high(64n, Nat.mul(C.shift(10n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(11n, SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})))))), C.low(64n, Nat.mul(C.shift(10n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(11n, SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))))))), Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_e(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), Nat.add(F.off(), 1023n)), 2180n), 64n), 64n)), SF.round(s, Nat.mul(C.shift(10n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(11n, SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))))), Nat.sub(Nat.sub(Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_e(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), Nat.add(F.off(), 1023n)), 2180n), 64n)), SF.round(s, Nat.mul(SF.mant(F.Bits{xl, xh}), SF.mant(F.Bits{yl, yh})), Nat.sub(Nat.add(SF.xexp(F.Bits{xl, xh}), SF.xexp(F.Bits{yl, yh})), SF.zb())), r3, Equal.trans(F.F64, SF.round(s, Nat.mul(C.shift(10n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(11n, SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))))), Nat.sub(Nat.sub(Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_e(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), Nat.add(F.off(), 1023n)), 2180n), 64n)), SF.round(s, C.shift(21n, Nat.mul(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))))), Nat.sub(Nat.sub(Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_e(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), Nat.add(F.off(), 1023n)), 2180n), 64n)), SF.round(s, Nat.mul(SF.mant(F.Bits{xl, xh}), SF.mant(F.Bits{yl, yh})), Nat.sub(Nat.add(SF.xexp(F.Bits{xl, xh}), SF.xexp(F.Bits{yl, yh})), SF.zb())), r4, Equal.trans(F.F64, SF.round(s, C.shift(21n, Nat.mul(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))))), Nat.sub(Nat.sub(Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_e(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), Nat.add(F.off(), 1023n)), 2180n), 64n)), SF.round(s, Nat.mul(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})))), Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_e(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n)), SF.round(s, Nat.mul(SF.mant(F.Bits{xl, xh}), SF.mant(F.Bits{yl, yh})), Nat.sub(Nat.add(SF.xexp(F.Bits{xl, xh}), SF.xexp(F.Bits{yl, yh})), SF.zb())), r5, Equal.trans(F.F64, SF.round(s, Nat.mul(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})))), Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_e(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n)), SF.round(s, C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), NM.sa(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), Nat.mul(SF.mant(F.Bits{xl, xh}), SF.mant(F.Bits{yl, yh}))), Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_e(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n)), SF.round(s, Nat.mul(SF.mant(F.Bits{xl, xh}), SF.mant(F.Bits{yl, yh})), Nat.sub(Nat.add(SF.xexp(F.Bits{xl, xh}), SF.xexp(F.Bits{yl, yh})), SF.zb())), r6, Equal.trans(F.F64, SF.round(s, C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), NM.sa(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), Nat.mul(SF.mant(F.Bits{xl, xh}), SF.mant(F.Bits{yl, yh}))), Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_e(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n)), SF.round(s, Nat.mul(SF.mant(F.Bits{xl, xh}), SF.mant(F.Bits{yl, yh})), Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_e(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), NM.sa(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))))), SF.round(s, Nat.mul(SF.mant(F.Bits{xl, xh}), SF.mant(F.Bits{yl, yh})), Nat.sub(Nat.add(SF.xexp(F.Bits{xl, xh}), SF.xexp(F.Bits{yl, yh})), SF.zb())), r7, r8)))))))
86
87# ---- the special values: f64_mul's branches and the spec's picks ----
88