1 import Base 2 import ./f64round.bend as FR 3 import ../../../spec/lib/common.bend as C 4 import ../../../spec/math/f64.bend as SF 5 import ../../../src/math/f64.bend as F 6 import ../../../src/math/w64.bend as X 7 import ../../lib/nat.bend as N 8 import ../../lib/logic.bend as L 9 import ./width.bend as WW 10 import ./natcmp.bend as NC 11 import ./f64bits.bend as FB 12 import ./f64addf.bend as AF 13 14 # Add.value and Sub.value of spec/math/f64.bend: SoftFloat's addF64 (the 15 # NaN, infinity and invalid cases of addMagsF64/subMagsF64) is the spec's 16 # add, IEEE 754-2019 §6.2/§7.2 on top of the finite case (f64addf.bend). 17 18 def v(+x: U32) -> Nat: 19 U32.to_nat(x) 20 21 # the spec's add with the classification of both operands as Booleans 22 def spec_g(+a1: Bool, +z1: Bool, +a2: Bool, +z2: Bool, +sx: Bool, +sy: Bool, +x: F.F64, +y: F.F64, +fin: F.F64) -> F.F64: 23 SF.pick(F.F64, Bool.or(Bool.and(a1, Bool.not(z1)), Bool.and(a2, Bool.not(z2))), SF.qnan(), SF.pick(F.F64, Bool.and(a1, z1), SF.pick(F.F64, Bool.and(Bool.and(a2, z2), Bool.not(Bool.not(Bool.xor(sx, sy)))), SF.qnan(), x), SF.pick(F.F64, Bool.and(a2, z2), y, fin))) 24 25 def pick_same(+b: Bool, +r: F.F64) -> {SF.pick(F.F64, b, r, r) == r : F.F64}: 26 match b: 27 case True{}: 28 Equal.trans(F.F64, SF.pick(F.F64, True{}, r, r), r, r, FR.pk_t(F.F64, r, r), {==}) 29 case False{}: 30 Equal.trans(F.F64, SF.pick(F.F64, False{}, r, r), r, r, FR.pk_f(F.F64, r, r), {==}) 31 32 def ff(+z1: Bool, +z2: Bool, +sx: Bool, +sy: Bool, +x: F.F64, +y: F.F64, +fin: F.F64) -> {spec_g(False{}, z1, False{}, z2, sx, sy, x, y, fin) == fin : F.F64}: 33 {==} 34 35 def tf(+z1: Bool, +z2: Bool, +sx: Bool, +sy: Bool, +x: F.F64, +y: F.F64, +fin: F.F64) -> {F.nan_or(x, Bool.not(z1)) == spec_g(True{}, z1, False{}, z2, sx, sy, x, y, fin) : F.F64}: 36 match z1: 37 case True{}: 38 {==} 39 case False{}: 40 {==} 41 42 def ft(+z1: Bool, +z2: Bool, +sx: Bool, +sy: Bool, +x: F.F64, +y: F.F64, +fin: F.F64) -> {F.nan_or(y, Bool.not(z2)) == spec_g(False{}, z1, True{}, z2, sx, sy, x, y, fin) : F.F64}: 43 match z2: 44 case True{}: 45 {==} 46 case False{}: 47 {==} 48 49 def tt(+z1: Bool, +z2: Bool, +sx: Bool, +sy: Bool, +x: F.F64, +y: F.F64, +fin: F.F64) -> {SF.pick(F.F64, Bool.not(Bool.xor(sx, sy)), F.nan_or(x, Bool.or(Bool.not(z1), Bool.not(z2))), F.nan()) == spec_g(True{}, z1, True{}, z2, sx, sy, x, y, fin) : F.F64}: 50 match z1 z2 sx sy: 51 case True{} True{} True{} True{}: 52 {==} 53 case True{} True{} True{} False{}: 54 {==} 55 case True{} True{} False{} True{}: 56 {==} 57 case True{} True{} False{} False{}: 58 {==} 59 case True{} False{} True{} True{}: 60 {==} 61 case True{} False{} True{} False{}: 62 {==} 63 case True{} False{} False{} True{}: 64 {==} 65 case True{} False{} False{} False{}: 66 {==} 67 case False{} True{} True{} True{}: 68 {==} 69 case False{} True{} True{} False{}: 70 {==} 71 case False{} True{} False{} True{}: 72 {==} 73 case False{} True{} False{} False{}: 74 {==} 75 case False{} False{} True{} True{}: 76 {==} 77 case False{} False{} True{} False{}: 78 {==} 79 case False{} False{} False{} True{}: 80 {==} 81 case False{} False{} False{} False{}: 82 {==} 83 84 # the spec's add, classified 85 def spec_c(+xl: U32, +xh: U32, +yl: U32, +yh: U32) -> {SF.add(F.Bits{xl, xh}, F.Bits{yl, yh}) == spec_g(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{yl, yh}), 2047n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})) : F.F64}: 86 {==} 87 88 def lt11(+xl: U32, +xh: U32) -> {Nat.is_lt(SF.efield(F.Bits{xl, xh}), 2047n) == Bool.not(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n)) : Bool}: 89 FB.lt_ne(SF.efield(F.Bits{xl, xh}), 2047n, WW.low_lt(11n, C.high(20n, v(xh)))) 90 91 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}: 92 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{}, lt11(xl, xh), Equal.cong(Bool, Bool, t => Bool.not(t), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), False{}, h)) 93 94 # F.add as the SoftFloat case split on the spec's fields 95 def add_g(+xl: U32, +xh: U32, +yl: U32, +yh: U32) -> {F.add(F.Bits{xl, xh}, F.Bits{yl, yh}) == SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}), Nat.cmp(SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}), Nat.cmp(SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh})))) : F.F64}: 96 +e0 = AF.ap(F.Bits{xl, xh}, F.Bits{yl, yh}, Bool.not(Bool.xor(F.signbit(F.Bits{xl, xh}), F.signbit(F.Bits{yl, yh})))) 97 +c1 = Equal.cong(Bool, F.F64, t => SF.pick(F.F64, Bool.not(Bool.xor(t, F.signbit(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, t, F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, t, F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh})))), F.signbit(F.Bits{xl, xh}), SF.sign(F.Bits{xl, xh}), FB.signbit_value(F.Bits{xl, xh})) 98 +c2 = Equal.cong(Bool, F.F64, t => SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), t)), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh})))), F.signbit(F.Bits{yl, yh}), SF.sign(F.Bits{yl, yh}), FB.signbit_value(F.Bits{yl, yh})) 99 +c3 = Equal.cong(Nat, F.F64, t => SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), t, F.exp_field(F.Bits{yl, yh}), Nat.cmp(t, F.exp_field(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), t, F.exp_field(F.Bits{yl, yh}), Nat.cmp(t, F.exp_field(F.Bits{yl, yh})))), F.exp_field(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), AF.hea(xl, xh)) 100 +c4 = Equal.cong(Nat, F.F64, t => SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), t, Nat.cmp(SF.efield(F.Bits{xl, xh}), t)), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), t, Nat.cmp(SF.efield(F.Bits{xl, xh}), t))), F.exp_field(F.Bits{yl, yh}), SF.efield(F.Bits{yl, yh}), AF.hea(yl, yh)) 101 Equal.trans(F.F64, F.add(F.Bits{xl, xh}, F.Bits{yl, yh}), SF.pick(F.F64, Bool.not(Bool.xor(F.signbit(F.Bits{xl, xh}), F.signbit(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, F.signbit(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, F.signbit(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh})))), SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}), Nat.cmp(SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}), Nat.cmp(SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh})))), e0, Equal.trans(F.F64, SF.pick(F.F64, Bool.not(Bool.xor(F.signbit(F.Bits{xl, xh}), F.signbit(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, F.signbit(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, F.signbit(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh})))), SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), F.signbit(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh})))), SF.pick(F.F64, Bool.not(Boo 102 103 def top_c(+xl: U32, +xh: U32, +yl: U32, +yh: U32, +a1: Bool, +ha1: {Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n) == a1 : Bool}, +a2: Bool, +ha2: {Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n) == a2 : Bool}) -> {F.add(F.Bits{xl, xh}, F.Bits{yl, yh}) == SF.add(F.Bits{xl, xh}, F.Bits{yl, yh}) : F.F64}: 104 match a1 a2: 105 case False{} False{}: 106 +r = AF.afin(xl, xh, yl, yh, ltf(xl, xh, ha1), ltf(yl, yh, ha2)) 107 +s1 = Equal.cong(Bool, F.F64, t => spec_g(t, Nat.is_eq(SF.frac(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), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), False{}, ha1) 108 +s2 = Equal.cong(Bool, F.F64, t => spec_g(False{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), t, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), False{}, ha2) 109 +sp = Equal.trans(F.F64, SF.add(F.Bits{xl, xh}, F.Bits{yl, yh}), spec_g(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{yl, yh}), 2047n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh}), spec_c(xl, xh, yl, yh), Equal.trans(F.F64, spec_g(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{yl, yh}), 2047n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), spec_g(False{}, Nat.is_eq(SF.frac(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), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh}), s1, Equal.trans(F.F64, spec_g(False{}, Nat.is_eq(SF.frac(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), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), spec_g(False{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), False{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh}), s2, ff(Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh}))))) 110 Equal.trans(F.F64, F.add(F.Bits{xl, xh}, F.Bits{yl, yh}), SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh}), SF.add(F.Bits{xl, xh}, F.Bits{yl, yh}), r, Equal.sym(F.F64, SF.add(F.Bits{xl, xh}, F.Bits{yl, yh}), SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh}), sp)) 111 case True{} False{}: 112 +e1 = N.eq_from_is_eq(SF.efield(F.Bits{xl, xh}), 2047n, ha1) 113 +hy = ltf(yl, yh, ha2) 114 +i1 = add_g(xl, xh, yl, yh) 115 +i2 = Equal.cong(Nat, F.F64, t => SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), t, SF.efield(F.Bits{yl, yh}), Nat.cmp(t, SF.efield(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), t, SF.efield(F.Bits{yl, yh}), Nat.cmp(t, SF.efield(F.Bits{yl, yh})))), SF.efield(F.Bits{xl, xh}), 2047n, e1) 116 +i3 = Equal.cong(Cmp, F.F64, t => SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), 2047n, SF.efield(F.Bits{yl, yh}), t), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), 2047n, SF.efield(F.Bits{yl, yh}), t)), Nat.cmp(2047n, SF.efield(F.Bits{yl, yh})), GT{}, NC.cmp_gt(2047n, SF.efield(F.Bits{yl, yh}), hy)) 117 +i4 = pick_same(Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.nan_or(F.Bits{xl, xh}, Bool.not(X.is_zero(F.frac(F.Bits{xl, xh}))))) 118 +i5 = Equal.cong(Bool, F.F64, t => F.nan_or(F.Bits{xl, xh}, Bool.not(t)), 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, {==})) 119 +s1 = Equal.cong(Bool, F.F64, t => spec_g(t, Nat.is_eq(SF.frac(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), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), True{}, ha1) 120 +s2 = Equal.cong(Bool, F.F64, t => spec_g(True{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), t, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), False{}, ha2) 121 +sp = Equal.trans(F.F64, SF.add(F.Bits{xl, xh}, F.Bits{yl, yh}), spec_g(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{yl, yh}), 2047n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), spec_g(True{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), False{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), spec_c(xl, xh, yl, yh), Equal.trans(F.F64, spec_g(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{yl, yh}), 2047n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), spec_g(True{}, Nat.is_eq(SF.frac(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), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), spec_g(True{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), False{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), s1, s2)) 122 +im = Equal.trans(F.F64, F.add(F.Bits{xl, xh}, F.Bits{yl, yh}), SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}), Nat.cmp(SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}), Nat.cmp(SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh})))), spec_g(True{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), False{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), i1, Equal.trans(F.F64, SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}), Nat.cmp(SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}), Nat.cmp(SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh})))), SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), 2047n, SF.efield(F.Bits{yl, yh}), Nat.cmp(2047n, SF.efield(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), 2047n, SF.efield(F.Bits{yl, yh}), Nat.cmp(2047n, SF.efield(F.Bits{yl, yh})))), spec_g(True{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), False{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), i2, Equal.trans(F.F64, SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign 123 Equal.trans(F.F64, F.add(F.Bits{xl, xh}, F.Bits{yl, yh}), spec_g(True{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), False{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), SF.add(F.Bits{xl, xh}, F.Bits{yl, yh}), im, Equal.sym(F.F64, SF.add(F.Bits{xl, xh}, F.Bits{yl, yh}), spec_g(True{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), False{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), sp)) 124 case False{} True{}: 125 +e2 = N.eq_from_is_eq(SF.efield(F.Bits{yl, yh}), 2047n, ha2) 126 +hx = ltf(xl, xh, ha1) 127 +i1 = add_g(xl, xh, yl, yh) 128 +i2 = Equal.cong(Nat, F.F64, t => SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), t, Nat.cmp(SF.efield(F.Bits{xl, xh}), t)), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), t, Nat.cmp(SF.efield(F.Bits{xl, xh}), t))), SF.efield(F.Bits{yl, yh}), 2047n, e2) 129 +i3 = Equal.cong(Cmp, F.F64, t => SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), 2047n, t), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), 2047n, t)), Nat.cmp(SF.efield(F.Bits{xl, xh}), 2047n), LT{}, NC.cmp_lt(SF.efield(F.Bits{xl, xh}), 2047n, hx)) 130 +i4 = pick_same(Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.nan_or(F.Bits{yl, yh}, Bool.not(X.is_zero(F.frac(F.Bits{yl, yh}))))) 131 +i5 = Equal.cong(Bool, F.F64, t => F.nan_or(F.Bits{yl, yh}, Bool.not(t)), 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, {==})) 132 +s1 = Equal.cong(Bool, F.F64, t => spec_g(t, Nat.is_eq(SF.frac(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), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), False{}, ha1) 133 +s2 = Equal.cong(Bool, F.F64, t => spec_g(False{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), t, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), True{}, ha2) 134 +sp = Equal.trans(F.F64, SF.add(F.Bits{xl, xh}, F.Bits{yl, yh}), spec_g(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{yl, yh}), 2047n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), spec_g(False{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), True{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), spec_c(xl, xh, yl, yh), Equal.trans(F.F64, spec_g(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{yl, yh}), 2047n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), spec_g(False{}, Nat.is_eq(SF.frac(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), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), spec_g(False{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), True{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), s1, s2)) 135 +im = Equal.trans(F.F64, F.add(F.Bits{xl, xh}, F.Bits{yl, yh}), SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}), Nat.cmp(SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}), Nat.cmp(SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh})))), spec_g(False{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), True{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), i1, Equal.trans(F.F64, SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}), Nat.cmp(SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}), Nat.cmp(SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh})))), SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), 2047n, Nat.cmp(SF.efield(F.Bits{xl, xh}), 2047n)), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), 2047n, Nat.cmp(SF.efield(F.Bits{xl, xh}), 2047n))), spec_g(False{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), True{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), i2, Equal.trans(F.F64, SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign 136 Equal.trans(F.F64, F.add(F.Bits{xl, xh}, F.Bits{yl, yh}), spec_g(False{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), True{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), SF.add(F.Bits{xl, xh}, F.Bits{yl, yh}), im, Equal.sym(F.F64, SF.add(F.Bits{xl, xh}, F.Bits{yl, yh}), spec_g(False{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), True{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), sp)) 137 case True{} True{}: 138 +e1 = N.eq_from_is_eq(SF.efield(F.Bits{xl, xh}), 2047n, ha1) 139 +e2 = N.eq_from_is_eq(SF.efield(F.Bits{yl, yh}), 2047n, ha2) 140 +i1 = add_g(xl, xh, yl, yh) 141 +i2 = Equal.cong(Nat, F.F64, t => SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), t, SF.efield(F.Bits{yl, yh}), Nat.cmp(t, SF.efield(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), t, SF.efield(F.Bits{yl, yh}), Nat.cmp(t, SF.efield(F.Bits{yl, yh})))), SF.efield(F.Bits{xl, xh}), 2047n, e1) 142 +i3 = Equal.cong(Nat, F.F64, t => SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), 2047n, t, Nat.cmp(2047n, t)), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), 2047n, t, Nat.cmp(2047n, t))), SF.efield(F.Bits{yl, yh}), 2047n, e2) 143 +i4 = Equal.cong(Bool, F.F64, t => SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.nan_or(F.Bits{xl, xh}, Bool.or(Bool.not(t), Bool.not(X.is_zero(F.frac(F.Bits{yl, yh}))))), F.nan()), 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, {==})) 144 +i5 = Equal.cong(Bool, F.F64, t => SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.nan_or(F.Bits{xl, xh}, Bool.or(Bool.not(Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n)), Bool.not(t))), F.nan()), 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, {==})) 145 +s1 = Equal.cong(Bool, F.F64, t => spec_g(t, Nat.is_eq(SF.frac(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), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), True{}, ha1) 146 +s2 = Equal.cong(Bool, F.F64, t => spec_g(True{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), t, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), True{}, ha2) 147 +sp = Equal.trans(F.F64, SF.add(F.Bits{xl, xh}, F.Bits{yl, yh}), spec_g(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{yl, yh}), 2047n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), spec_g(True{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), True{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), spec_c(xl, xh, yl, yh), Equal.trans(F.F64, spec_g(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{yl, yh}), 2047n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), spec_g(True{}, Nat.is_eq(SF.frac(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), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), spec_g(True{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), True{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), s1, s2)) 148 +im = Equal.trans(F.F64, F.add(F.Bits{xl, xh}, F.Bits{yl, yh}), SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}), Nat.cmp(SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}), Nat.cmp(SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh})))), spec_g(True{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), True{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), i1, Equal.trans(F.F64, SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}), Nat.cmp(SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}), Nat.cmp(SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh})))), SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), 2047n, SF.efield(F.Bits{yl, yh}), Nat.cmp(2047n, SF.efield(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), 2047n, SF.efield(F.Bits{yl, yh}), Nat.cmp(2047n, SF.efield(F.Bits{yl, yh})))), spec_g(True{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), True{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), i2, Equal.trans(F.F64, SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F 149 Equal.trans(F.F64, F.add(F.Bits{xl, xh}, F.Bits{yl, yh}), spec_g(True{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), True{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), SF.add(F.Bits{xl, xh}, F.Bits{yl, yh}), im, Equal.sym(F.F64, SF.add(F.Bits{xl, xh}, F.Bits{yl, yh}), spec_g(True{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), True{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), sp)) 150 151 def add_value(+x: F.F64, +y: F.F64) -> SF.Add.value(x, y): 152 match x y: 153 case F.Bits{+xl, +xh} F.Bits{+yl, +yh}: 154 top_c(xl, xh, yl, yh, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), {==}, Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), {==}) 155 156 def sub_value(+x: F.F64, +y: F.F64) -> SF.Sub.value(x, y): 157 Equal.trans(F.F64, F.add(x, F.neg(y)), F.add(x, SF.neg(y)), SF.add(x, SF.neg(y)), Equal.cong(F.F64, F.F64, z => F.add(x, z), F.neg(y), SF.neg(y), FB.neg_value(y)), add_value(x, SF.neg(y)))