1 import Base 2 import ./f64light.bend as FL 3 import ../../../spec/lib/common.bend as C 4 import ../../../spec/math/f64.bend as SF 5 import ../../../spec/math/w64.bend as SW 6 import ../../../src/math/f64.bend as F 7 import ../../../src/math/w64.bend as X 8 import ../../../src/math/u64.bend as WU 9 import ../../lib/nat.bend as N 10 import ../../lib/logic.bend as L 11 import ../../lib/word.bend as WD 12 import ./width.bend as WW 13 import ./natcmp.bend as NC 14 import ./f64bits.bend as FB 15 import ./f64cmp.bend as FC 16 import ./f64round.bend as FR 17 import ./f64norm.bend as NM 18 import ./f64mexp.bend as EX 19 import ./f64divv.bend as DV 20 21 # Div.value of spec/math/f64.bend: SoftFloat's f64_div (NaN, infinity and 22 # zero cases, then the quotient of the normalized significands) is the 23 # spec's div, IEEE 754-2019 §6.2/§7.3 around the exact-then-round quotient. 24 25 def v(+x: U32) -> Nat: 26 U32.to_nat(x) 27 28 def hea(+xl: U32, +xh: U32) -> {F.exp_field(F.Bits{xl, xh}) == SF.efield(F.Bits{xl, xh}) : Nat}: 29 FL.hea(xl, xh) 30 31 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}: 32 FL.fval_g(xl, xh, m, hm) 33 34 def hfr(+xl: U32, +xh: U32) -> {SW.value(F.frac(F.Bits{xl, xh})) == SF.frac(F.Bits{xl, xh}) : Nat}: 35 FL.hfr(xl, xh) 36 37 def ltf(+xl: U32, +xh: U32, +h: {Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n) == False{} : Bool}) -> {Nat.is_lt(SF.efield(F.Bits{xl, xh}), 2047n) == True{} : Bool}: 38 Equal.trans(Bool, Nat.is_lt(SF.efield(F.Bits{xl, xh}), 2047n), Bool.not(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n)), True{}, FB.lt_ne(SF.efield(F.Bits{xl, xh}), 2047n, WW.low_lt(11n, C.high(20n, v(xh)))), Equal.cong(Bool, Bool, t => Bool.not(t), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), False{}, h)) 39 40 def xl_c(+E: Nat, +h: {Nat.is_lt(E, 2047n) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(E, 0n) == c : Bool}) -> {Nat.is_le(SF.pick(Nat, c, Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n)), 3971n) == True{} : Bool}: 41 match c: 42 case True{}: 43 {==} 44 case False{}: 45 L.subst(Nat, z => {Nat.is_le(z, 3971n) == True{} : Bool}, Nat.add(1925n, E), Nat.sub(Nat.add(E, SF.zb()), 1075n), Equal.sym(Nat, Nat.sub(Nat.add(E, SF.zb()), 1075n), Nat.add(1925n, E), FC.esub(E)), N.le_add_left(E, 2046n, 1925n, N.lt_succ_le(E, 2046n, h))) 46 47 def xexp_le(+E: Nat, +h: {Nat.is_lt(E, 2047n) == True{} : Bool}) -> {Nat.is_le(SF.pick(Nat, Nat.is_eq(E, 0n), Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n)), 3971n) == True{} : Bool}: 48 xl_c(E, h, Nat.is_eq(E, 0n), {==}) 49 50 def nzle(+n: Nat, +hz: {Nat.is_eq(n, 0n) == False{} : Bool}) -> {Nat.is_le(1n, n) == True{} : Bool}: 51 match n: 52 case 0n: 53 NC.absurd_tf({Nat.is_le(1n, 0n) == True{} : Bool}, Equal.sym(Bool, True{}, False{}, hz)) 54 case 1n+ +np: 55 N.zero_le(np) 56 57 # a nonzero finite significand is positive 58 def mpos_c(+sy: Nat, +m: Nat, +w: Nat, +hw: {w == C.shift(sy, m) : Nat}, +h52: {C.fits(52n, w) == False{} : Bool}, +z: Bool, +hz: {Nat.is_eq(m, 0n) == z : Bool}) -> {z == False{} : Bool}: 59 match z: 60 case True{}: 61 +e0 = N.eq_from_is_eq(m, 0n, hz) 62 +ew = Equal.trans(Nat, w, C.shift(sy, m), 0n, hw, Equal.trans(Nat, C.shift(sy, m), C.shift(sy, 0n), 0n, Equal.cong(Nat, Nat, t => C.shift(sy, t), m, 0n, e0), WW.shift_zero(sy))) 63 Equal.trans(Bool, True{}, C.fits(52n, w), False{}, Equal.cong(Nat, Bool, t => C.fits(52n, t), 0n, w, Equal.sym(Nat, w, 0n, ew)), h52) 64 case False{}: 65 {==} 66 67 def yp_eq(+yl: U32, +yh: U32, +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}) -> {SF.mant(F.Bits{yl, yh}) == 1n+Nat.sub(SF.mant(F.Bits{yl, yh}), 1n) : Nat}: 68 +n1 = 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), hfr(yl, yh), FC.hF(yl, yh), hzy) 69 +n3 = 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), hfr(yl, yh), FC.hF(yl, yh), hzy) 70 +nz = mpos_c(NM.sa(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), SF.mant(F.Bits{yl, yh}), SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), n1, n3, Nat.is_eq(SF.mant(F.Bits{yl, yh}), 0n), {==}) 71 Equal.sym(Nat, 1n+Nat.sub(SF.mant(F.Bits{yl, yh}), 1n), SF.mant(F.Bits{yl, yh}), N.sub_add(SF.mant(F.Bits{yl, yh}), 1n, nzle(SF.mant(F.Bits{yl, yh}), nz))) 72 73 # the finite nonzero quotient 74 def dfin(+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}, +hax: {Nat.is_lt(SF.efield(F.Bits{xl, xh}), 2047n) == True{} : Bool}, +hay: {Nat.is_lt(SF.efield(F.Bits{yl, yh}), 2047n) == True{} : Bool}) -> {F.div_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.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s) : F.F64}: 75 +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), hfr(xl, xh), FC.hF(xl, xh), hzx) 76 +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), hfr(yl, yh), FC.hF(yl, yh), hzy) 77 +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), hfr(xl, xh), FC.hF(xl, xh), hzx) 78 +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), hfr(yl, yh), FC.hF(yl, yh), hzy) 79 +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), hfr(xl, xh), FC.hF(xl, xh), hzx) 80 +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), hfr(yl, yh), FC.hF(yl, yh), hzy) 81 +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), hfr(xl, xh), FC.hF(xl, xh), hzx) 82 +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), hfr(yl, yh), FC.hF(yl, yh), hzy) 83 +ey = yp_eq(yl, yh, hzy) 84 +hB = Equal.trans(Nat, 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})), C.shift(NM.sa(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), 1n+Nat.sub(SF.mant(F.Bits{yl, yh}), 1n)), n1y, Equal.cong(Nat, Nat, t => C.shift(NM.sa(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), t), SF.mant(F.Bits{yl, yh}), 1n+Nat.sub(SF.mant(F.Bits{yl, yh}), 1n), ey)) 85 +r = DV.dcore(1n, {==}, 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.mant(F.Bits{xl, xh}), Nat.sub(SF.mant(F.Bits{yl, yh}), 1n), 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}), n1x, hB, a53, a52, b53, b52, 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})), xexp_le(SF.efield(F.Bits{yl, yh}), hay)) 86 +sp = Equal.cong(Nat, F.F64, z => SF.round(s, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, SF.mant(F.Bits{xl, xh})), z)), Nat.min(Nat.mod(C.shift(200n, SF.mant(F.Bits{xl, xh})), z), 1n)), Nat.sub(Nat.add(SF.xexp(F.Bits{xl, xh}), SF.zb()), Nat.add(Nat.add(SF.xexp(F.Bits{yl, yh}), SF.kq()), 1n))), SF.mant(F.Bits{yl, yh}), 1n+Nat.sub(SF.mant(F.Bits{yl, yh}), 1n), ey) 87 Equal.trans(F.F64, F.div_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.add(Nat.mul(2n, Nat.div(C.shift(200n, SF.mant(F.Bits{xl, xh})), 1n+Nat.sub(SF.mant(F.Bits{yl, yh}), 1n))), Nat.min(Nat.mod(C.shift(200n, SF.mant(F.Bits{xl, xh})), 1n+Nat.sub(SF.mant(F.Bits{yl, yh}), 1n)), 1n)), Nat.sub(Nat.add(SF.xexp(F.Bits{xl, xh}), 3000n), Nat.add(Nat.add(SF.xexp(F.Bits{yl, yh}), 200n), 1n))), SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s), r, Equal.sym(F.F64, SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s), SF.round(s, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, SF.mant(F.Bits{xl, xh})), 1n+Nat.sub(SF.mant(F.Bits{yl, yh}), 1n))), Nat.min(Nat.mod(C.shift(200n, SF.mant(F.Bits{xl, xh})), 1n+Nat.sub(SF.mant(F.Bits{yl, yh}), 1n)), 1n)), Nat.sub(Nat.add(SF.xexp(F.Bits{xl, xh}), 3000n), Nat.add(Nat.add(SF.xexp(F.Bits{yl, yh}), 200n), 1n))), sp)) 88 89 def mant0(+xl: U32, +xh: U32, +hc: {Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n) == True{} : Bool}, +hb: {Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n) == True{} : Bool}) -> {SF.mant(F.Bits{xl, xh}) == 0n : Nat}: 90 +e1 = Equal.cong(Bool, Nat, t => Nat.add(SF.frac(F.Bits{xl, xh}), C.shift(52n, SF.b2n(Bool.not(t)))), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), True{}, hc) 91 Equal.trans(Nat, SF.mant(F.Bits{xl, xh}), Nat.add(SF.frac(F.Bits{xl, xh}), 0n), 0n, e1, Equal.trans(Nat, Nat.add(SF.frac(F.Bits{xl, xh}), 0n), SF.frac(F.Bits{xl, xh}), 0n, N.add_zero(SF.frac(F.Bits{xl, xh})), N.eq_from_is_eq(SF.frac(F.Bits{xl, xh}), 0n, hb))) 92 93 def zero_v(+s: Bool) -> {F.zero(s) == SF.zero(s) : F.F64}: 94 match s: 95 case True{}: 96 {==} 97 case False{}: 98 {==} 99 100 # zero divided by a nonzero finite double 101 def dz(+s: Bool, +xl: U32, +xh: U32, +yl: U32, +yh: U32, +hc: {Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n) == True{} : Bool}, +hb: {Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n) == True{} : 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.zero(s) == SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s) : F.F64}: 102 +e1 = Equal.cong(Nat, F.F64, z => SF.round(s, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, z), SF.mant(F.Bits{yl, yh}))), Nat.min(Nat.mod(C.shift(200n, z), SF.mant(F.Bits{yl, yh})), 1n)), Nat.sub(Nat.add(SF.xexp(F.Bits{xl, xh}), SF.zb()), Nat.add(Nat.add(SF.xexp(F.Bits{yl, yh}), SF.kq()), 1n))), SF.mant(F.Bits{xl, xh}), 0n, mant0(xl, xh, hc, hb)) 103 +e2 = Equal.cong(Nat, F.F64, z => SF.round(s, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, 0n), z)), Nat.min(Nat.mod(C.shift(200n, 0n), z), 1n)), Nat.sub(Nat.add(SF.xexp(F.Bits{xl, xh}), SF.zb()), Nat.add(Nat.add(SF.xexp(F.Bits{yl, yh}), SF.kq()), 1n))), SF.mant(F.Bits{yl, yh}), 1n+Nat.sub(SF.mant(F.Bits{yl, yh}), 1n), yp_eq(yl, yh, hzy)) 104 Equal.trans(F.F64, F.zero(s), SF.zero(s), SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s), zero_v(s), Equal.sym(F.F64, SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s), SF.zero(s), Equal.trans(F.F64, SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s), SF.round(s, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, 0n), SF.mant(F.Bits{yl, yh}))), Nat.min(Nat.mod(C.shift(200n, 0n), SF.mant(F.Bits{yl, yh})), 1n)), Nat.sub(Nat.add(SF.xexp(F.Bits{xl, xh}), SF.zb()), Nat.add(Nat.add(SF.xexp(F.Bits{yl, yh}), SF.kq()), 1n))), SF.zero(s), e1, e2))) 105 106 def dimpl(+s: Bool, +a1: Bool, +b1: Bool, +c1: Bool, +a2: Bool, +b2: Bool, +c2: Bool, +r: F.F64) -> F.F64: 107 SF.pick(F.F64, a1, SF.pick(F.F64, Bool.or(Bool.not(b1), a2), F.nan(), F.inf(s)), SF.pick(F.F64, a2, SF.pick(F.F64, Bool.not(b2), F.nan(), F.zero(s)), SF.pick(F.F64, Bool.and(c2, b2), SF.pick(F.F64, Bool.and(c1, b1), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.and(c1, b1), F.zero(s), r)))) 108 109 def dspec(+s: Bool, +a1: Bool, +b1: Bool, +c1: Bool, +a2: Bool, +b2: Bool, +c2: Bool, +r: F.F64) -> F.F64: 110 SF.pick(F.F64, Bool.or(Bool.and(a1, Bool.not(b1)), Bool.and(a2, Bool.not(b2))), SF.qnan(), SF.pick(F.F64, Bool.and(a1, b1), SF.pick(F.F64, Bool.and(a2, b2), SF.qnan(), SF.inf(s)), SF.pick(F.F64, Bool.and(a2, b2), SF.zero(s), SF.pick(F.F64, Bool.and(c2, b2), SF.pick(F.F64, Bool.and(c1, b1), SF.qnan(), SF.inf(s)), r)))) 111 112 def ion(+s: Bool, +b: Bool) -> {F.inf_or_nan(s, b) == SF.pick(F.F64, b, F.nan(), F.inf(s)) : F.F64}: 113 match b: 114 case True{}: 115 Equal.trans(F.F64, F.inf_or_nan(s, True{}), F.nan(), SF.pick(F.F64, True{}, F.nan(), F.inf(s)), {==}, Equal.sym(F.F64, SF.pick(F.F64, True{}, F.nan(), F.inf(s)), F.nan(), FR.pk_t(F.F64, F.nan(), F.inf(s)))) 116 case False{}: 117 Equal.trans(F.F64, F.inf_or_nan(s, False{}), F.inf(s), SF.pick(F.F64, False{}, F.nan(), F.inf(s)), {==}, Equal.sym(F.F64, SF.pick(F.F64, False{}, F.nan(), F.inf(s)), F.inf(s), FR.pk_f(F.F64, F.nan(), F.inf(s)))) 118 119 def non(+x: F.F64, +b: Bool) -> {F.nan_or(x, b) == SF.pick(F.F64, b, F.nan(), x) : F.F64}: 120 FL.non(x, b) 121 122 def dsh4(+s: Bool, +ea: Nat, +fa: WU.U64, +eb: Nat, +fb: WU.U64, +z: Bool) -> {F.div_za(s, ea, fa, eb, fb, z) == SF.pick(F.F64, z, F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))) : F.F64}: 123 match z: 124 case True{}: 125 Equal.trans(F.F64, F.div_za(s, ea, fa, eb, fb, True{}), F.zero(s), SF.pick(F.F64, True{}, F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))), {==}, Equal.sym(F.F64, SF.pick(F.F64, True{}, F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))), F.zero(s), FR.pk_t(F.F64, F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))))) 126 case False{}: 127 Equal.trans(F.F64, F.div_za(s, ea, fa, eb, fb, False{}), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb)), SF.pick(F.F64, False{}, F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))), {==}, Equal.sym(F.F64, SF.pick(F.F64, False{}, F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb)), FR.pk_f(F.F64, F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))))) 128 129 def dsh3(+s: Bool, +ea: Nat, +fa: WU.U64, +eb: Nat, +fb: WU.U64, +z: Bool) -> {F.div_z(s, ea, fa, eb, fb, z) == SF.pick(F.F64, z, SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb)))) : F.F64}: 130 match z: 131 case True{}: 132 Equal.trans(F.F64, F.div_z(s, ea, fa, eb, fb, True{}), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.nan(), F.inf(s)), SF.pick(F.F64, True{}, SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb)))), ion(s, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa))), Equal.sym(F.F64, SF.pick(F.F64, True{}, SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb)))), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.nan(), F.inf(s)), FR.pk_t(F.F64, SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb)))))) 133 case False{}: 134 Equal.trans(F.F64, F.div_z(s, ea, fa, eb, fb, False{}), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))), SF.pick(F.F64, False{}, SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb)))), dsh4(s, ea, fa, eb, fb, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa))), Equal.sym(F.F64, SF.pick(F.F64, False{}, SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb)))), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))), FR.pk_f(F.F64, SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb)))))) 135 136 def dsh2(+s: Bool, +ea: Nat, +fa: WU.U64, +eb: Nat, +fb: WU.U64, +t: Bool) -> {F.div_b(s, ea, fa, eb, fb, t) == SF.pick(F.F64, t, SF.pick(F.F64, Bool.not(X.is_zero(fb)), F.nan(), F.zero(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(eb, 0n), X.is_zero(fb)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))))) : F.F64}: 137 match t: 138 case True{}: 139 Equal.trans(F.F64, F.div_b(s, ea, fa, eb, fb, True{}), SF.pick(F.F64, Bool.not(X.is_zero(fb)), F.nan(), F.zero(s)), SF.pick(F.F64, True{}, SF.pick(F.F64, Bool.not(X.is_zero(fb)), F.nan(), F.zero(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(eb, 0n), X.is_zero(fb)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))))), non(F.zero(s), Bool.not(X.is_zero(fb))), Equal.sym(F.F64, SF.pick(F.F64, True{}, SF.pick(F.F64, Bool.not(X.is_zero(fb)), F.nan(), F.zero(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(eb, 0n), X.is_zero(fb)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))))), SF.pick(F.F64, Bool.not(X.is_zero(fb)), F.nan(), F.zero(s)), FR.pk_t(F.F64, SF.pick(F.F64, Bool.not(X.is_zero(fb)), F.nan(), F.zero(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(eb, 0n), X.is_zero(fb)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))))))) 140 case False{}: 141 Equal.trans(F.F64, F.div_b(s, ea, fa, eb, fb, False{}), SF.pick(F.F64, Bool.and(Nat.is_eq(eb, 0n), X.is_zero(fb)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb)))), SF.pick(F.F64, False{}, SF.pick(F.F64, Bool.not(X.is_zero(fb)), F.nan(), F.zero(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(eb, 0n), X.is_zero(fb)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))))), dsh3(s, ea, fa, eb, fb, Bool.and(Nat.is_eq(eb, 0n), X.is_zero(fb))), Equal.sym(F.F64, SF.pick(F.F64, False{}, SF.pick(F.F64, Bool.not(X.is_zero(fb)), F.nan(), F.zero(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(eb, 0n), X.is_zero(fb)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))))), SF.pick(F.F64, Bool.and(Nat.is_eq(eb, 0n), X.is_zero(fb)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb)))), FR.pk_f(F.F64, SF.pick(F.F64, Bool.not(X.is_zero(fb)), F.nan(), F.zero(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(eb, 0n), X.is_zero(fb)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))))))) 142 143 def dsh1(+s: Bool, +ea: Nat, +fa: WU.U64, +eb: Nat, +fb: WU.U64, +t: Bool) -> {F.div_cls(s, ea, fa, eb, fb, t) == dimpl(s, t, X.is_zero(fa), Nat.is_eq(ea, 0n), Nat.is_eq(eb, 2047n), X.is_zero(fb), Nat.is_eq(eb, 0n), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))) : F.F64}: 144 match t: 145 case True{}: 146 ion(s, Bool.or(Bool.not(X.is_zero(fa)), Nat.is_eq(eb, 2047n))) 147 case False{}: 148 dsh2(s, ea, fa, eb, fb, Nat.is_eq(eb, 2047n)) 149 150 def dcase(+s: Bool, +xl: U32, +xh: U32, +yl: U32, +yh: U32, +r1: F.F64, +r2: F.F64, +a1: Bool, +b1: Bool, +c1: Bool, +a2: Bool, +b2: Bool, +c2: Bool, +hR: {SF.pick(F.F64, Bool.or(Bool.or(a1, a2), Bool.or(Bool.and(c1, b1), Bool.and(c2, b2))), r2, r1) == r2 : F.F64}, +hZ: {SF.pick(F.F64, Bool.or(Bool.or(a1, a2), Bool.or(Bool.not(Bool.and(c1, b1)), Bool.and(c2, b2))), r2, F.zero(s)) == r2 : F.F64}) -> {dimpl(s, a1, b1, c1, a2, b2, c2, r1) == dspec(s, a1, b1, c1, a2, b2, c2, r2) : F.F64}: 151 match a1 b1 c1 a2 b2 c2: 152 case True{} True{} True{} True{} True{} True{}: 153 {==} 154 case True{} True{} True{} True{} True{} False{}: 155 {==} 156 case True{} True{} True{} True{} False{} True{}: 157 {==} 158 case True{} True{} True{} True{} False{} False{}: 159 {==} 160 case True{} True{} True{} False{} True{} True{}: 161 FR.inf_v(s) 162 case True{} True{} True{} False{} True{} False{}: 163 FR.inf_v(s) 164 case True{} True{} True{} False{} False{} True{}: 165 FR.inf_v(s) 166 case True{} True{} True{} False{} False{} False{}: 167 FR.inf_v(s) 168 case True{} True{} False{} True{} True{} True{}: 169 {==} 170 case True{} True{} False{} True{} True{} False{}: 171 {==} 172 case True{} True{} False{} True{} False{} True{}: 173 {==} 174 case True{} True{} False{} True{} False{} False{}: 175 {==} 176 case True{} True{} False{} False{} True{} True{}: 177 FR.inf_v(s) 178 case True{} True{} False{} False{} True{} False{}: 179 FR.inf_v(s) 180 case True{} True{} False{} False{} False{} True{}: 181 FR.inf_v(s) 182 case True{} True{} False{} False{} False{} False{}: 183 FR.inf_v(s) 184 case True{} False{} True{} True{} True{} True{}: 185 {==} 186 case True{} False{} True{} True{} True{} False{}: 187 {==} 188 case True{} False{} True{} True{} False{} True{}: 189 {==} 190 case True{} False{} True{} True{} False{} False{}: 191 {==} 192 case True{} False{} True{} False{} True{} True{}: 193 {==} 194 case True{} False{} True{} False{} True{} False{}: 195 {==} 196 case True{} False{} True{} False{} False{} True{}: 197 {==} 198 case True{} False{} True{} False{} False{} False{}: 199 {==} 200 case True{} False{} False{} True{} True{} True{}: 201 {==} 202 case True{} False{} False{} True{} True{} False{}: 203 {==} 204 case True{} False{} False{} True{} False{} True{}: 205 {==} 206 case True{} False{} False{} True{} False{} False{}: 207 {==} 208 case True{} False{} False{} False{} True{} True{}: 209 {==} 210 case True{} False{} False{} False{} True{} False{}: 211 {==} 212 case True{} False{} False{} False{} False{} True{}: 213 {==} 214 case True{} False{} False{} False{} False{} False{}: 215 {==} 216 case False{} True{} True{} True{} True{} True{}: 217 zero_v(s) 218 case False{} True{} True{} True{} True{} False{}: 219 zero_v(s) 220 case False{} True{} True{} True{} False{} True{}: 221 {==} 222 case False{} True{} True{} True{} False{} False{}: 223 {==} 224 case False{} True{} True{} False{} True{} True{}: 225 {==} 226 case False{} True{} True{} False{} True{} False{}: 227 hZ 228 case False{} True{} True{} False{} False{} True{}: 229 hZ 230 case False{} True{} True{} False{} False{} False{}: 231 hZ 232 case False{} True{} False{} True{} True{} True{}: 233 zero_v(s) 234 case False{} True{} False{} True{} True{} False{}: 235 zero_v(s) 236 case False{} True{} False{} True{} False{} True{}: 237 {==} 238 case False{} True{} False{} True{} False{} False{}: 239 {==} 240 case False{} True{} False{} False{} True{} True{}: 241 FR.inf_v(s) 242 case False{} True{} False{} False{} True{} False{}: 243 hR 244 case False{} True{} False{} False{} False{} True{}: 245 hR 246 case False{} True{} False{} False{} False{} False{}: 247 hR 248 case False{} False{} True{} True{} True{} True{}: 249 zero_v(s) 250 case False{} False{} True{} True{} True{} False{}: 251 zero_v(s) 252 case False{} False{} True{} True{} False{} True{}: 253 {==} 254 case False{} False{} True{} True{} False{} False{}: 255 {==} 256 case False{} False{} True{} False{} True{} True{}: 257 FR.inf_v(s) 258 case False{} False{} True{} False{} True{} False{}: 259 hR 260 case False{} False{} True{} False{} False{} True{}: 261 hR 262 case False{} False{} True{} False{} False{} False{}: 263 hR 264 case False{} False{} False{} True{} True{} True{}: 265 zero_v(s) 266 case False{} False{} False{} True{} True{} False{}: 267 zero_v(s) 268 case False{} False{} False{} True{} False{} True{}: 269 {==} 270 case False{} False{} False{} True{} False{} False{}: 271 {==} 272 case False{} False{} False{} False{} True{} True{}: 273 FR.inf_v(s) 274 case False{} False{} False{} False{} True{} False{}: 275 hR 276 case False{} False{} False{} False{} False{} True{}: 277 hR 278 case False{} False{} False{} False{} False{} False{}: 279 hR 280 281 def dswap(+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}) -> {dimpl(s1, p1, p2, p3, p4, p5, p6, r1) == dimpl(s2, q1, q2, q3, q4, q5, q6, r2) : F.F64}: 282 Equal.trans(F.F64, dimpl(s1, p1, p2, p3, p4, p5, p6, r1), dimpl(s2, p1, p2, p3, p4, p5, p6, r1), dimpl(s2, q1, q2, q3, q4, q5, q6, r2), Equal.cong(Bool, F.F64, w => dimpl(w, p1, p2, p3, p4, p5, p6, r1), s1, s2, hs), Equal.trans(F.F64, dimpl(s2, p1, p2, p3, p4, p5, p6, r1), dimpl(s2, p1, p2, p3, p4, p5, p6, r2), dimpl(s2, q1, q2, q3, q4, q5, q6, r2), Equal.cong(F.F64, F.F64, w => dimpl(s2, p1, p2, p3, p4, p5, p6, w), r1, r2, hr), Equal.trans(F.F64, dimpl(s2, p1, p2, p3, p4, p5, p6, r2), dimpl(s2, q1, p2, p3, p4, p5, p6, r2), dimpl(s2, q1, q2, q3, q4, q5, q6, r2), Equal.cong(Bool, F.F64, w => dimpl(s2, w, p2, p3, p4, p5, p6, r2), p1, q1, h0), Equal.trans(F.F64, dimpl(s2, q1, p2, p3, p4, p5, p6, r2), dimpl(s2, q1, q2, p3, p4, p5, p6, r2), dimpl(s2, q1, q2, q3, q4, q5, q6, r2), Equal.cong(Bool, F.F64, w => dimpl(s2, q1, w, p3, p4, p5, p6, r2), p2, q2, h1), Equal.trans(F.F64, dimpl(s2, q1, q2, p3, p4, p5, p6, r2), dimpl(s2, q1, q2, q3, p4, p5, p6, r2), dimpl(s2, q1, q2, q3, q4, q5, q6, r2), Equal.cong(Bool, F.F64, w => dimpl(s2, q1, q2, w, p4, p5, p6, r2), p3, q3, h2), Equal.trans(F.F64, dimpl(s2, q1, q2, q3, p4, p5, p6, r2), dimpl(s2, q1, q2, q3, q4, p5, p6, r2), dimpl(s2, q1, q2, q3, q4, q5, q6, r2), Equal.cong(Bool, F.F64, w => dimpl(s2, q1, q2, q3, w, p5, p6, r2), p4, q4, h3), Equal.trans(F.F64, dimpl(s2, q1, q2, q3, q4, p5, p6, r2), dimpl(s2, q1, q2, q3, q4, q5, p6, r2), dimpl(s2, q1, q2, q3, q4, q5, q6, r2), Equal.cong(Bool, F.F64, w => dimpl(s2, q1, q2, q3, q4, w, p6, r2), p5, q5, h4), Equal.cong(Bool, F.F64, w => dimpl(s2, q1, q2, q3, q4, q5, w, r2), p6, q6, h5)))))))) 283 284 def dkR_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.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s), F.div_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.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s) : F.F64}: 285 match g: 286 case True{}: 287 Equal.trans(F.F64, SF.pick(F.F64, True{}, SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s), F.div_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.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s), SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s), FR.pk_t(F.F64, SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s), F.div_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})))), {==}) 288 case False{}: 289 +ha = FC.or_l(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) 290 +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) 291 Equal.trans(F.F64, SF.pick(F.F64, False{}, SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s), F.div_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.div_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.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s), FR.pk_f(F.F64, SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s), F.div_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})))), dfin(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), ltf(xl, xh, FC.or_l(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), ha)), ltf(yl, yh, FC.or_r(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), ha)))) 292 293 def dkZ_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.not(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.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s), F.zero(s)) == SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s) : F.F64}: 294 match g: 295 case True{}: 296 Equal.trans(F.F64, SF.pick(F.F64, True{}, SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s), F.zero(s)), SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s), SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s), FR.pk_t(F.F64, SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s), F.zero(s)), {==}) 297 case False{}: 298 +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.not(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) 299 +h1 = FR.not_f(Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n)), FC.or_l(Bool.not(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)) 300 Equal.trans(F.F64, SF.pick(F.F64, False{}, SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s), F.zero(s)), F.zero(s), SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s), FR.pk_f(F.F64, SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s), F.zero(s)), dz(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), h1), FC.and_r(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), h1), FC.or_r(Bool.not(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))) 301 302 def div_value(+x: F.F64, +y: F.F64) -> SF.Div.value(x, y): 303 match x y: 304 case F.Bits{+xl, +xh} F.Bits{+yl, +yh}: 305 +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}))) 306 +i1 = dsh1(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)) 307 +i2 = dswap(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.div_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.div_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.div_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}), 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}), 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}), hea(yl, yh)), X.is_zero(F.frac(F.Bits{yl, yh})), Nat.is_eq(SF.frac(F.Bit 308 +i3 = dcase(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh})), xl, xh, yl, yh, F.div_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.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, 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), dkR_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)))), {==}), dkZ_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.not(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)))), {==})) 309 Equal.trans(F.F64, F.div_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)), dimpl(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.div_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})))), dspec(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.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh})))), Equal.trans(F.F64, F.div_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)), dimpl(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.div_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