~/bend-docscommunity

proofs/math/typed/f64mulf.bend source

proofs/math/typed/f64mulf.bend on the hub · documented module

import Baseimport ../../../spec/lib/common.bend as Cimport ../../../spec/math/f64.bend as SFimport ../../../spec/math/w64.bend as SWimport ../../../src/math/f64.bend as Fimport ../../../src/math/w64.bend as Ximport ../../../src/math/u64.bend as WUimport ../../../src/math/natural.bend as Mimport ../../lib/nat.bend as Nimport ../../lib/logic.bend as Limport ./width.bend as WWimport ../../lib/word.bend as WDimport ./w64sh.bend as SHimport ./natcmp.bend as NCimport ./f64bits.bend as FBimport ./f64cmp.bend as FCimport ./f64rtools.bend as RTimport ./f64norm.bend as NMimport ./f64mexp.bend as EXimport ./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 ----