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 ../../../src/math/natural.bend as M
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ./width.bend as WW
import ../../lib/word.bend as WD
import ./w64sh.bend as SH
import ./natcmp.bend as NC
import ./f64bits.bend as FB
import ./f64cmp.bend as FC
import ./f64rtools.bend as RT
import ./f64norm.bend as NM
import ./f64mexp.bend as EX
import ./f64mul.bend as MU

# Mul.value of spec/math/f64.bend: the finite nonzero product.

def v(+x: U32) -> Nat:
  U32.to_nat(x)

# ---- fields of the operands ----

def hea(+xl: U32, +xh: U32) -> {F.exp_field(F.Bits{xl, xh}) == SF.efield(F.Bits{xl, xh}) : Nat}:
  FB.ef_g(1n, {==}, xh, 1048576, {==}, 2047, {==})

def 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}:
  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))

def hfa(+xl: U32, +xh: U32) -> {SW.value(F.frac(F.Bits{xl, xh})) == SF.frac(F.Bits{xl, xh}) : Nat}:
  fval_g(xl, xh, 1048575, {==})

def 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}:
  match c:
    case True{}:
      {==}
    case False{}:
      +h1 = N.lt_succ_le(M.bit_length(m), k, N.not_le_lt(1n+k, M.bit_length(m), hc))
      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))))

def nfit_bl(+k: Nat, +m: Nat, +hk: {C.fits(k, m) == False{} : Bool}) -> {Nat.is_le(1n+k, M.bit_length(m)) == True{} : Bool}:
  nlb(False{}, k, m, 0n, hk, Nat.is_le(1n+k, M.bit_length(m)), {==})

def 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}:
  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)))))

# ---- two finite nonzero operands ----

def 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}:
  +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)
  +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)
  +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)
  +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)
  +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)
  +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)
  +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)
  +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)
  +eA = MU.shl_v(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 10n, 53n, {==}, {==}, a53)
  +eB = MU.shl_v(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), 11n, 53n, {==}, {==}, b53)
  +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)))
  +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}))))
  +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)
  +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)
  +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))
  +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))
  +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})))
  +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}))))
  +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)
  +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})))
  +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))
  +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))
  +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))
  +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)
  +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))
  +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))
  +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})))
  +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)
  +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))
  +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}))))
  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)))))))

# ---- the special values: f64_mul's branches and the spec's picks ----