~/bend-docscommunity

proofs/math/typed/f64mulv.bend source

proofs/math/typed/f64mulv.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 ../../lib/lemmas/proofs/nat_algebra.bend as NAimport ./width.bend as WWimport ../../lib/word.bend as WDimport ./w64sh.bend as SHimport ./u32laws.bend as LWimport ./natcmp.bend as NCimport ./f64bits.bend as FBimport ./f64cmp.bend as FCimport ./f64round.bend as FRimport ./f64rtools.bend as RTimport ./f64norm.bend as NMimport ./f64mexp.bend as EXimport ./f64mul.bend as MUimport ./f64mulf.bend as MFimport ./f64mulc.bend as MC# Mul.value of spec/math/f64.bend.def v(+x: U32) -> Nat:  U32.to_nat(x)# ---- fields of the operands ----def mswap(+s1: Bool, +s2: Bool, +hs: {s1 == s2 : Bool}, +r1: F.F64, +r2: F.F64, +hr: {r1 == r2 : F.F64}, +p1: Bool, +q1: Bool, +h0: {p1 == q1 : Bool}, +p2: Bool, +q2: Bool, +h1: {p2 == q2 : Bool}, +p3: Bool, +q3: Bool, +h2: {p3 == q3 : Bool}, +p4: Bool, +q4: Bool, +h3: {p4 == q4 : Bool}, +p5: Bool, +q5: Bool, +h4: {p5 == q5 : Bool}, +p6: Bool, +q6: Bool, +h5: {p6 == q6 : Bool}) -> {MC.mimpl(s1, p1, p2, p3, p4, p5, p6, r1) == MC.mimpl(s2, q1, q2, q3, q4, q5, q6, r2) : F.F64}:  Equal.trans(F.F64, MC.mimpl(s1, p1, p2, p3, p4, p5, p6, r1), MC.mimpl(s2, p1, p2, p3, p4, p5, p6, r1), MC.mimpl(s2, q1, q2, q3, q4, q5, q6, r2), Equal.cong(Bool, F.F64, w => MC.mimpl(w, p1, p2, p3, p4, p5, p6, r1), s1, s2, hs), Equal.trans(F.F64, MC.mimpl(s2, p1, p2, p3, p4, p5, p6, r1), MC.mimpl(s2, p1, p2, p3, p4, p5, p6, r2), MC.mimpl(s2, q1, q2, q3, q4, q5, q6, r2), Equal.cong(F.F64, F.F64, w => MC.mimpl(s2, p1, p2, p3, p4, p5, p6, w), r1, r2, hr), Equal.trans(F.F64, MC.mimpl(s2, p1, p2, p3, p4, p5, p6, r2), MC.mimpl(s2, q1, p2, p3, p4, p5, p6, r2), MC.mimpl(s2, q1, q2, q3, q4, q5, q6, r2), Equal.cong(Bool, F.F64, w => MC.mimpl(s2, w, p2, p3, p4, p5, p6, r2), p1, q1, h0), Equal.trans(F.F64, MC.mimpl(s2, q1, p2, p3, p4, p5, p6, r2), MC.mimpl(s2, q1, q2, p3, p4, p5, p6, r2), MC.mimpl(s2, q1, q2, q3, q4, q5, q6, r2), Equal.cong(Bool, F.F64, w => MC.mimpl(s2, q1, w, p3, p4, p5, p6, r2), p2, q2, h1), Equal.trans(F.F64, MC.mimpl(s2, q1, q2, p3, p4, p5, p6, r2), MC.mimpl(s2, q1, q2, q3, p4, p5, p6, r2), MC.mimpl(s2, q1, q2, q3, q4, q5, q6, r2), Equal.cong(Bool, F.F64, w => MC.mimpl(s2, q1, q2, w, p4, p5, p6, r2), p3, q3, h2), Equal.trans(F.F64, MC.mimpl(s2, q1, q2, q3, p4, p5, p6, r2), MC.mimpl(s2, q1, q2, q3, q4, p5, p6, r2), MC.mimpl(s2, q1, q2, q3, q4, q5, q6, r2), Equal.cong(Bool, F.F64, w => MC.mimpl(s2, q1, q2, q3, w, p5, p6, r2), p4, q4, h3), Equal.trans(F.F64, MC.mimpl(s2, q1, q2, q3, q4, p5, p6, r2), MC.mimpl(s2, q1, q2, q3, q4, q5, p6, r2), MC.mimpl(s2, q1, q2, q3, q4, q5, q6, r2), Equal.cong(Bool, F.F64, w => MC.mimpl(s2, q1, q2, q3, q4, w, p6, r2), p5, q5, h4), Equal.cong(Bool, F.F64, w => MC.mimpl(s2, q1, q2, q3, q4, q5, w, r2), p6, q6, h5))))))))def mkR_c(+s: Bool, +xl: U32, +xh: U32, +yl: U32, +yh: U32, +g: Bool, +hg: {Bool.or(Bool.or(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n)), Bool.or(Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n)), Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n)))) == g : Bool}) -> {SF.pick(F.F64, g, 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.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}:  match g:    case True{}:      Equal.trans(F.F64, SF.pick(F.F64, True{}, 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.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())), 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())), FR.pk_t(F.F64, 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.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})))), {==})    case False{}:      +hz = FC.or_r(Bool.or(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n)), Bool.or(Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n)), Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n))), hg)      Equal.trans(F.F64, SF.pick(F.F64, False{}, 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.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})))), 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())), FR.pk_f(F.F64, 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.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})))), MF.mfin(s, xl, xh, yl, yh, FC.or_l(Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n)), Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n)), hz), FC.or_r(Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n)), Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n)), hz)))def mkZ_z(+s: Bool, +xl: U32, +xh: U32, +yl: U32, +yh: U32, +z1: Bool, +hz1: {Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n)) == z1 : Bool}, +h: {Bool.or(z1, Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n))) == True{} : Bool}) -> {F.zero(s) == 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}:  match z1:    case True{}:      MC.zx(s, xl, xh, yl, yh, FC.and_l(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), hz1), FC.and_r(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), hz1))    case False{}:      MC.zy(s, xl, xh, yl, yh, FC.and_l(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), h), FC.and_r(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), h))def mkZ_c(+s: Bool, +xl: U32, +xh: U32, +yl: U32, +yh: U32, +g: Bool, +hg: {Bool.or(Bool.or(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n)), Bool.not(Bool.or(Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n)), Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n))))) == g : Bool}) -> {SF.pick(F.F64, g, 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.zero(s)) == 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}:  match g:    case True{}:      Equal.trans(F.F64, SF.pick(F.F64, True{}, 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.zero(s)), 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())), 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())), FR.pk_t(F.F64, 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.zero(s)), {==})    case False{}:      +hn = FC.or_r(Bool.or(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n)), Bool.not(Bool.or(Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n)), Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n)))), hg)      Equal.trans(F.F64, SF.pick(F.F64, False{}, 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.zero(s)), F.zero(s), 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())), FR.pk_f(F.F64, 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.zero(s)), mkZ_z(s, xl, xh, yl, yh, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n)), {==}, FR.not_f(Bool.or(Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n)), Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n))), hn)))def mul_value(+x: F.F64, +y: F.F64) -> SF.Mul.value(x, y):  match x y:    case F.Bits{+xl, +xh} F.Bits{+yl, +yh}:      +hs = Equal.trans(Bool, Bool.xor(F.signbit(F.Bits{xl, xh}), F.signbit(F.Bits{yl, yh})), Bool.xor(SF.sign(F.Bits{xl, xh}), F.signbit(F.Bits{yl, yh})), Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh})), Equal.cong(Bool, Bool, z => Bool.xor(z, F.signbit(F.Bits{yl, yh})), F.signbit(F.Bits{xl, xh}), SF.sign(F.Bits{xl, xh}), FB.signbit_value(F.Bits{xl, xh})), Equal.cong(Bool, Bool, z => Bool.xor(SF.sign(F.Bits{xl, xh}), z), F.signbit(F.Bits{yl, yh}), SF.sign(F.Bits{yl, yh}), FB.signbit_value(F.Bits{yl, yh})))      +i1 = MC.sh1(Bool.xor(F.signbit(F.Bits{xl, xh}), F.signbit(F.Bits{yl, yh})), F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}), Nat.is_eq(F.exp_field(F.Bits{xl, xh}), 2047n))      +i2 = mswap(Bool.xor(F.signbit(F.Bits{xl, xh}), F.signbit(F.Bits{yl, yh})), Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh})), hs, F.mul_n(Bool.xor(F.signbit(F.Bits{xl, xh}), F.signbit(F.Bits{yl, yh})), 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}))), F.mul_n(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh})), 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}))), Equal.cong(Bool, F.F64, z => F.mul_n(z, 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}))), Bool.xor(F.signbit(F.Bits{xl, xh}), F.signbit(F.Bits{yl, yh})), Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh})), hs), Nat.is_eq(F.exp_field(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 2047n), F.exp_field(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), MF.hea(xl, xh)), X.is_zero(F.frac(F.Bits{xl, xh})), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), FB.fz_g(xl, xh, 1048575, {==}), Nat.is_eq(F.exp_field(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), F.exp_field(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), MF.hea(xl, xh)), Nat.is_eq(F.exp_field(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 2047n), F.exp_field(F.Bits{yl, yh}), SF.efield(F.Bits{yl, yh}), MF.hea(yl, yh)), X.is_zero(F.frac(F.Bits{yl, yh})), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), FB.fz_g(yl, yh, 1048575, {==}), Nat.is_eq(F.exp_field(F.Bits{yl, yh}), 0n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), F.exp_field(F.Bits{yl, yh}), SF.efield(F.Bits{yl, yh}), MF.hea(yl, yh)))      +i3 = MC.mcase(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh})), xl, xh, yl, yh, F.mul_n(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh})), 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(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh})), 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())), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), {==}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), {==}, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), {==}, Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), {==}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), {==}, Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n), {==}, mkR_c(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh})), xl, xh, yl, yh, Bool.or(Bool.or(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n)), Bool.or(Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n)), Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n)))), {==}), mkZ_c(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh})), xl, xh, yl, yh, Bool.or(Bool.or(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n)), Bool.not(Bool.or(Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n)), Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n))))), {==}))      Equal.trans(F.F64, F.mul_cls(Bool.xor(F.signbit(F.Bits{xl, xh}), F.signbit(F.Bits{yl, yh})), F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}), Nat.is_eq(F.exp_field(F.Bits{xl, xh}), 2047n)), MC.mimpl(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh})), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n), F.mul_n(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh})), 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})))), MC.mspec(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh})), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n), SF.round(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh})), 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()))), Equal.trans(F.F64, F.mul_cls(Bool.xor(F.signbit(F.Bits{xl, xh}), F.signbit(F.Bits{yl, yh})), F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}), Nat.is_eq(F.exp_field(F.Bits{xl, xh}), 2047n)), MC.mimpl(Bool.xor(F.signbit(F.Bits{xl, xh}), F.signbit(F.Bits{yl, yh})), Nat.is_eq(F.exp_field(F.Bits{xl, xh}), 2047n), X.is_zero(F.frac(F.Bits{xl, xh})), Nat.is_eq(F.exp_field(F.Bits{xl, xh}), 0n), Nat.is_eq(F.exp_field(F.Bits{yl, yh}), 2047n), X.is_zero(F.frac(F.Bits{yl, yh})), Nat.is_eq(F.exp_field(F.Bits{yl, yh}), 0n), F.mul_n(Bool.xor(F.signbit(F.Bits{xl, xh}), F.signbit(F.Bits{yl, yh})), 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})))), MC.mimpl(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh})), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n), F.mul_n(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh})), 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})))), i1, i2), i3)