1 import Base 2 import ../../../spec/lib/common.bend as C 3 import ../../../spec/math/f64.bend as SF 4 import ../../../spec/math/w64.bend as SW 5 import ../../../src/math/f64.bend as F 6 import ../../../src/math/w64.bend as X 7 import ../../../src/math/u64.bend as WU 8 import ../../lib/nat.bend as N 9 import ../../lib/logic.bend as L 10 import ../../lib/word.bend as WD 11 import ../../lib/lemmas/proofs/nat_algebra.bend as NA 12 import ./width.bend as WW 13 import ./w64add.bend as WA 14 import ./w64sh.bend as SH 15 import ./f64bits.bend as FB 16 import ./f64light.bend as FL 17 import ./f64round.bend as FR 18 import ./f64tools.bend as T 19 20 # Rounding to an integral value (IEEE 754-2019 5.3.1 roundToIntegral, C99 21 # F.10.6): Trunc.value, Floor.value, Ceil.value and Round.value. A finite x 22 # below 2^52 in magnitude is m 2^-k (k = Z - xexp(x) >= 1); the 23 # implementation splits m into q = m >> k, r = m - (q << k) and the half unit 24 # h = 2^(k-1) (for k >= 64: q = 0, r = m, h = 2^63), moves q up one by the 25 # direction's rule, and rounds q at the scale Z with round_w (exact: q has at 26 # most 53 bits). Each piece is the spec's integral(): high(k, m), low(k, m) 27 # and rne's h, read through the W64 clauses (Shr, Shl, Sub, Lt, Eq, Odd, 28 # IsZero, Add) and f64tools.rw_value. 29 30 # ---- the direction's rule on values ---- 31 32 def upn(+m: F.RMode, +s: Bool, +q: Nat, +r: Nat, +h: Nat) -> Bool: 33 match m: 34 case F.Trunc{}: 35 False{} 36 case F.Floor{}: 37 Bool.and(s, Bool.not(Nat.is_eq(r, 0n))) 38 case F.Ceil{}: 39 Bool.and(Bool.not(s), Bool.not(Nat.is_eq(r, 0n))) 40 case F.Even{}: 41 Bool.or(Nat.is_lt(h, r), Bool.and(Nat.is_eq(r, h), Nat.is_eq(Nat.mod(q, 2n), 1n))) 42 43 def up_v(+m: F.RMode, +s: Bool, +q: WU.U64, +r: WU.U64, +h: WU.U64) -> {F.ri_up(m, s, q, r, h) == upn(m, s, SW.value(q), SW.value(r), SW.value(h)) : Bool}: 44 match m: 45 case F.Trunc{}: 46 {==} 47 case F.Floor{}: 48 Equal.cong(Bool, Bool, b => Bool.and(s, Bool.not(b)), X.is_zero(r), Nat.is_eq(SW.value(r), 0n), WA.is_zero_value(r)) 49 case F.Ceil{}: 50 Equal.cong(Bool, Bool, b => Bool.and(Bool.not(s), Bool.not(b)), X.is_zero(r), Nat.is_eq(SW.value(r), 0n), WA.is_zero_value(r)) 51 case F.Even{}: 52 +e1 = Equal.cong(Bool, Bool, b => Bool.or(b, Bool.and(X.eq(r, h), X.odd(q))), X.lt(h, r), Nat.is_lt(SW.value(h), SW.value(r)), WA.lt_value(h, r)) 53 +e2 = Equal.cong(Bool, Bool, b => Bool.or(Nat.is_lt(SW.value(h), SW.value(r)), Bool.and(b, X.odd(q))), X.eq(r, h), Nat.is_eq(SW.value(r), SW.value(h)), WA.eq_value(r, h)) 54 +e3 = Equal.cong(Bool, Bool, b => Bool.or(Nat.is_lt(SW.value(h), SW.value(r)), Bool.and(Nat.is_eq(SW.value(r), SW.value(h)), b)), X.odd(q), Nat.is_eq(Nat.mod(SW.value(q), 2n), 1n), WA.odd_value(q)) 55 +b1 = Bool.or(Nat.is_lt(SW.value(h), SW.value(r)), Bool.and(X.eq(r, h), X.odd(q))) 56 +b2 = Bool.or(Nat.is_lt(SW.value(h), SW.value(r)), Bool.and(Nat.is_eq(SW.value(r), SW.value(h)), X.odd(q))) 57 +b3 = Bool.or(Nat.is_lt(SW.value(h), SW.value(r)), Bool.and(Nat.is_eq(SW.value(r), SW.value(h)), Nat.is_eq(Nat.mod(SW.value(q), 2n), 1n))) 58 Equal.trans(Bool, F.ri_up(F.Even{}, s, q, r, h), b1, b3, e1, Equal.trans(Bool, b1, b2, b3, e2, e3)) 59 60 # ---- q + up, rounded at the scale Z ---- 61 62 def b64v(+b: Bool) -> {SW.value(F.b64(b)) == SF.b2n(b) : Nat}: 63 match b: 64 case True{}: 65 {==} 66 case False{}: 67 {==} 68 69 def b2n63(+b: Bool) -> {C.fits(63n, SF.b2n(b)) == True{} : Bool}: 70 match b: 71 case True{}: 72 {==} 73 case False{}: 74 {==} 75 76 def addb(+q: WU.U64, +b: Bool, +hq: {C.fits(63n, SW.value(q)) == True{} : Bool}) -> {SW.value(X.add(q, F.b64(b))) == Nat.add(SW.value(q), SF.b2n(b)) : Nat}: 77 +Q = SW.value(q) 78 e1 = WA.add_value(q, F.b64(b)) 79 +e2 = Equal.cong(Nat, Nat, n => C.low(64n, Nat.add(Q, n)), SW.value(F.b64(b)), SF.b2n(b), b64v(b)) 80 +hf = FR.fits_add1(63n, Q, SF.b2n(b), hq, b2n63(b)) 81 +e3 = WW.low_fit(64n, Nat.add(Q, SF.b2n(b)), hf) 82 Equal.trans(Nat, SW.value(X.add(q, F.b64(b))), C.low(64n, Nat.add(Q, SW.value(F.b64(b)))), Nat.add(Q, SF.b2n(b)), e1, Equal.trans(Nat, C.low(64n, Nat.add(Q, SW.value(F.b64(b)))), C.low(64n, Nat.add(Q, SF.b2n(b))), Nat.add(Q, SF.b2n(b)), e2, e3)) 83 84 def G(+m: F.RMode, +s: Bool, +a: Nat, +b: Nat, +c: Nat) -> F.F64: 85 SF.round(s, Nat.add(a, SF.b2n(upn(m, s, a, b, c))), 3000n) 86 87 def riq(+m: F.RMode, +s: Bool, +q: WU.U64, +r: WU.U64, +h: WU.U64, +hq: {C.fits(63n, SW.value(q)) == True{} : Bool}) -> {F.ri_q(m, s, q, r, h) == G(m, s, SW.value(q), SW.value(r), SW.value(h)) : F.F64}: 88 +u = F.ri_up(m, s, q, r, h) 89 +Q = SW.value(q) 90 +e1 = T.rw_value(s, 3000n, X.add(q, F.b64(u)), {==}) 91 +e2 = Equal.cong(Nat, F.F64, n => SF.round(s, n, 3000n), SW.value(X.add(q, F.b64(u))), Nat.add(Q, SF.b2n(u)), addb(q, u, hq)) 92 +e3 = Equal.cong(Bool, F.F64, b => SF.round(s, Nat.add(Q, SF.b2n(b)), 3000n), u, upn(m, s, Q, SW.value(r), SW.value(h)), up_v(m, s, q, r, h)) 93 Equal.trans(F.F64, F.ri_q(m, s, q, r, h), SF.round(s, SW.value(X.add(q, F.b64(u))), 3000n), G(m, s, Q, SW.value(r), SW.value(h)), e1, Equal.trans(F.F64, SF.round(s, SW.value(X.add(q, F.b64(u))), 3000n), SF.round(s, Nat.add(Q, SF.b2n(u)), 3000n), G(m, s, Q, SW.value(r), SW.value(h)), e2, e3)) 94 95 def g3(+m: F.RMode, +s: Bool, +a: Nat, +a2: Nat, +ha: {a == a2 : Nat}, +b: Nat, +b2: Nat, +hb: {b == b2 : Nat}, +c: Nat, +c2: Nat, +hc: {c == c2 : Nat}) -> {G(m, s, a, b, c) == G(m, s, a2, b2, c2) : F.F64}: 96 +e1 = Equal.cong(Nat, F.F64, t => G(m, s, t, b, c), a, a2, ha) 97 +e2 = Equal.cong(Nat, F.F64, t => G(m, s, a2, t, c), b, b2, hb) 98 +e3 = Equal.cong(Nat, F.F64, t => G(m, s, a2, b2, t), c, c2, hc) 99 Equal.trans(F.F64, G(m, s, a, b, c), G(m, s, a2, b, c), G(m, s, a2, b2, c2), e1, Equal.trans(F.F64, G(m, s, a2, b, c), G(m, s, a2, b2, c), G(m, s, a2, b2, c2), e2, e3)) 100 101 # the spec's integral at k = 1 + j, in the same shape 102 def integ(+m: F.RMode, +s: Bool, +n: Nat, +j: Nat) -> {SF.round(s, SF.integral(m, s, n, 1n+j), 3000n) == G(m, s, C.high(1n+j, n), C.low(1n+j, n), C.shift(j, 1n)) : F.F64}: 103 match m: 104 case F.Trunc{}: 105 Equal.cong(Nat, F.F64, t => SF.round(s, t, 3000n), C.high(1n+j, n), Nat.add(C.high(1n+j, n), 0n), Equal.sym(Nat, Nat.add(C.high(1n+j, n), 0n), C.high(1n+j, n), N.add_zero(C.high(1n+j, n)))) 106 case F.Floor{}: 107 {==} 108 case F.Ceil{}: 109 {==} 110 case F.Even{}: 111 {==} 112 113 # ---- fewer than 64 fractional bits ---- 114 115 def le64(+j: Nat) -> {Nat.is_le(64n, Nat.add(1n+j, 63n)) == True{} : Bool}: 116 L.subst(Nat, t => {Nat.is_le(63n, t) == True{} : Bool}, Nat.add(63n, j), Nat.add(j, 63n), NA.add_comm(63n, j), N.le_add_right(63n, j)) 117 118 def hfit(+j: Nat, +V: Nat, +hv: {C.fits(64n, V) == True{} : Bool}) -> {C.fits(63n, C.high(1n+j, V)) == True{} : Bool}: 119 +f = SH.fits_mono(64n, Nat.add(1n+j, 63n), V, le64(j), hv) 120 Equal.trans(Bool, C.fits(63n, C.high(1n+j, V)), C.fits(Nat.add(1n+j, 63n), V), True{}, Equal.sym(Bool, C.fits(Nat.add(1n+j, 63n), V), C.fits(63n, C.high(1n+j, V)), FR.fits_hc(1n+j, 63n, V)), f) 121 122 # 2^(k-1) as a word 123 def half_v(+j: Nat, +hb: {Nat.is_lt(1n+j, 64n) == True{} : Bool}) -> {SW.value(X.shl(WU.U64{1, 0}, Nat.sub(1n+j, 1n))) == C.shift(j, 1n) : Nat}: 124 +hj = N.lt_trans(j, 1n+j, 64n, N.lt_succ(j), hb) 125 +hl = N.lt_le(1n+j, 64n, hb) 126 +hj1 = L.subst(Nat, t => {Nat.is_le(t, 64n) == True{} : Bool}, 1n+j, Nat.add(j, 1n), Equal.sym(Nat, Nat.add(j, 1n), 1n+j, Equal.trans(Nat, Nat.add(j, 1n), 1n+Nat.add(j, 0n), 1n+j, N.add_succ(j, 0n), Equal.cong(Nat, Nat, t => 1n+t, Nat.add(j, 0n), j, N.add_zero(j)))), hl) 127 +e = FL.shl_v(WU.U64{1, 0}, j, 1n, hj, hj1, {==}) 128 L.subst(Nat, t => {SW.value(X.shl(WU.U64{1, 0}, t)) == C.shift(j, 1n) : Nat}, j, Nat.sub(j, 0n), Equal.sym(Nat, Nat.sub(j, 0n), j, N.sub_zero(j)), e) 129 130 def small_case(+m: F.RMode, +s: Bool, +w: WU.U64, +j: Nat, +hb: {Nat.is_lt(1n+j, 64n) == True{} : Bool}) -> {F.ri_k(m, s, w, 1n+j, True{}) == G(m, s, C.high(1n+j, SW.value(w)), C.low(1n+j, SW.value(w)), C.shift(j, 1n)) : F.F64}: 131 +V = SW.value(w) 132 +q = X.shr(w, 1n+j) 133 +sq = X.shl(q, 1n+j) 134 +r = X.sub(w, sq) 135 +h = X.shl(WU.U64{1, 0}, Nat.sub(1n+j, 1n)) 136 +Hq = C.high(1n+j, V) 137 +Lq = C.low(1n+j, V) 138 +S = C.shift(1n+j, Hq) 139 eq1 = SH.shr_value(w, 1n+j) 140 eq2 = SH.shr_value(w, 1n+j) 141 eq3 = SH.shr_value(w, 1n+j) 142 +hQ = L.subst(Nat, t => {C.fits(63n, t) == True{} : Bool}, Hq, SW.value(q), Equal.sym(Nat, SW.value(q), Hq, eq1), hfit(j, V, FL.vb64(w))) 143 esl0 = SH.shl_value(q, 1n+j, hb) 144 +esl1 = Equal.cong(Nat, Nat, t => C.low(64n, C.shift(1n+j, t)), SW.value(q), Hq, eq2) 145 +eV = WW.low_high(1n+j, V) 146 +eV2 = WW.low_high(1n+j, V) 147 +hSV0 = L.subst(Nat, t => {Nat.is_le(S, t) == True{} : Bool}, Nat.add(S, Lq), Nat.add(Lq, S), NA.add_comm(S, Lq), N.le_add_right(S, Lq)) 148 +hSV = L.subst(Nat, t => {Nat.is_le(S, t) == True{} : Bool}, Nat.add(Lq, S), V, Equal.sym(Nat, V, Nat.add(Lq, S), eV), hSV0) 149 +hSf = SH.fits_lek(64n, S, V, hSV, FL.vb64(w)) 150 +esl = Equal.trans(Nat, SW.value(sq), C.low(64n, S), S, Equal.trans(Nat, SW.value(sq), C.low(64n, C.shift(1n+j, SW.value(q))), C.low(64n, S), esl0, esl1), WW.low_fit(64n, S, hSf)) 151 +esl2 = Equal.trans(Nat, SW.value(sq), C.low(64n, S), S, Equal.trans(Nat, SW.value(sq), C.low(64n, C.shift(1n+j, SW.value(q))), C.low(64n, S), SH.shl_value(q, 1n+j, hb), Equal.cong(Nat, Nat, t => C.low(64n, C.shift(1n+j, t)), SW.value(q), Hq, eq3)), WW.low_fit(64n, S, SH.fits_lek(64n, S, V, L.subst(Nat, t => {Nat.is_le(S, t) == True{} : Bool}, Nat.add(Lq, S), V, Equal.sym(Nat, V, Nat.add(Lq, S), eV2), L.subst(Nat, t => {Nat.is_le(S, t) == True{} : Bool}, Nat.add(S, Lq), Nat.add(Lq, S), NA.add_comm(S, Lq), N.le_add_right(S, Lq))), FL.vb64(w)))) 152 +hle = L.subst(Nat, t => {Nat.is_le(t, V) == True{} : Bool}, S, SW.value(sq), Equal.sym(Nat, SW.value(sq), S, esl), hSV) 153 er0 = WA.sub_value(w, sq, hle) 154 +er1 = Equal.cong(Nat, Nat, t => Nat.sub(V, t), SW.value(sq), S, esl2) 155 +eV3 = WW.low_high(1n+j, V) 156 +er2 = Equal.cong(Nat, Nat, t => Nat.sub(t, S), V, Nat.add(Lq, S), eV3) 157 +er3 = FR.sub_add_l(Lq, S) 158 +er = Equal.trans(Nat, SW.value(r), Nat.sub(V, SW.value(sq)), Lq, er0, Equal.trans(Nat, Nat.sub(V, SW.value(sq)), Nat.sub(V, S), Lq, er1, Equal.trans(Nat, Nat.sub(V, S), Nat.sub(Nat.add(Lq, S), S), Lq, er2, er3))) 159 +ehv = half_v(j, hb) 160 +e0 = riq(m, s, q, r, h, hQ) 161 e4 = SH.shr_value(w, 1n+j) 162 Equal.trans(F.F64, F.ri_q(m, s, q, r, h), G(m, s, SW.value(q), SW.value(r), SW.value(h)), G(m, s, Hq, Lq, C.shift(j, 1n)), e0, g3(m, s, SW.value(q), Hq, e4, SW.value(r), Lq, er, SW.value(h), C.shift(j, 1n), ehv)) 163 164 # ---- 64 or more fractional bits: the integer part is 0 ---- 165 166 def c63(+one: Nat, +h1: {one == 1n : Nat}, +c: U32, +hc: {c == U32{WD.pw(32n, 31n)} : U32}) -> {SW.value(WU.U64{0, c}) == C.shift(63n, one) : Nat}: 167 Equal.trans(Nat, C.shift(32n, U32.to_nat(c)), C.shift(32n, C.shift(31n, one)), C.shift(63n, one), Equal.cong(Nat, Nat, z => C.shift(32n, z), U32.to_nat(c), C.shift(31n, one), FB.pwv(31n, {==}, one, h1, c, hc)), Equal.sym(Nat, C.shift(63n, one), C.shift(32n, C.shift(31n, one)), WW.shift_comp(32n, 31n, one))) 168 169 # V < 2^k is not above 2^k 170 def nlt(+k: Nat, +one: Nat, +h1: {one == 1n : Nat}, +V: Nat, +hf: {C.fits(k, V) == True{} : Bool}) -> {Nat.is_lt(C.shift(k, one), V) == False{} : Bool}: 171 +hl = Equal.trans(Bool, Nat.is_lt(V, C.shift(k, one)), C.fits(k, V), True{}, FR.lt_fit(k, one, h1, V), hf) 172 N.le_not_lt(C.shift(k, one), V, N.lt_le(V, C.shift(k, one), hl)) 173 174 def upn_big(+m: F.RMode, +s: Bool, +V: Nat, +a: Nat, +b: Nat, +la: {Nat.is_lt(a, V) == False{} : Bool}, +lb: {Nat.is_lt(b, V) == False{} : Bool}) -> {upn(m, s, 0n, V, a) == upn(m, s, 0n, V, b) : Bool}: 175 match m: 176 case F.Trunc{}: 177 {==} 178 case F.Floor{}: 179 {==} 180 case F.Ceil{}: 181 {==} 182 case F.Even{}: 183 +ea = Equal.trans(Bool, upn(F.Even{}, s, 0n, V, a), Bool.and(Nat.is_eq(V, a), False{}), False{}, Equal.cong(Bool, Bool, t => Bool.or(t, Bool.and(Nat.is_eq(V, a), False{})), Nat.is_lt(a, V), False{}, la), FR.and_f(Nat.is_eq(V, a))) 184 +eb = Equal.trans(Bool, upn(F.Even{}, s, 0n, V, b), Bool.and(Nat.is_eq(V, b), False{}), False{}, Equal.cong(Bool, Bool, t => Bool.or(t, Bool.and(Nat.is_eq(V, b), False{})), Nat.is_lt(b, V), False{}, lb), FR.and_f(Nat.is_eq(V, b))) 185 Equal.trans(Bool, upn(F.Even{}, s, 0n, V, a), False{}, upn(F.Even{}, s, 0n, V, b), ea, Equal.sym(Bool, upn(F.Even{}, s, 0n, V, b), False{}, eb)) 186 187 def large_case(+m: F.RMode, +s: Bool, +w: WU.U64, +j: Nat, +hb: {Nat.is_le(64n, 1n+j) == True{} : Bool}, +hw: {C.fits(53n, SW.value(w)) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +c: U32, +hc: {c == U32{WD.pw(32n, 31n)} : U32}) -> {F.ri_q(m, s, WU.U64{0, 0}, w, WU.U64{0, c}) == SF.round(s, SF.integral(m, s, SW.value(w), 1n+j), 3000n) : F.F64}: 188 +V = SW.value(w) 189 +vc = SW.value(WU.U64{0, c}) 190 +h53 = N.le_trans(53n, 64n, 1n+j, {==}, hb) 191 +f = SH.fits_mono(53n, 1n+j, V, h53, hw) 192 +eh = N.eq_from_is_eq(C.high(1n+j, V), 0n, f) 193 +el = WW.low_fit(1n+j, V, SH.fits_mono(53n, 1n+j, V, N.le_trans(53n, 64n, 1n+j, {==}, hb), hw)) 194 +fj = SH.fits_mono(53n, j, V, N.le_trans(53n, 63n, j, {==}, hb), hw) 195 +la = nlt(j, 1n, {==}, V, fj) 196 +lb0 = nlt(63n, one, h1, V, SH.fits_mono(53n, 63n, V, {==}, hw)) 197 +lb = L.subst(Nat, t => {Nat.is_lt(t, V) == False{} : Bool}, C.shift(63n, one), vc, Equal.sym(Nat, vc, C.shift(63n, one), c63(one, h1, c, hc)), lb0) 198 +eu = upn_big(m, s, V, C.shift(j, 1n), vc, la, lb) 199 +e0 = riq(m, s, WU.U64{0, 0}, w, WU.U64{0, c}, {==}) 200 +e1 = Equal.sym(F.F64, SF.round(s, SF.integral(m, s, V, 1n+j), 3000n), G(m, s, C.high(1n+j, V), C.low(1n+j, V), C.shift(j, 1n)), integ(m, s, V, j)) 201 +e2 = Equal.sym(F.F64, G(m, s, C.high(1n+j, V), C.low(1n+j, V), C.shift(j, 1n)), G(m, s, 0n, V, C.shift(j, 1n)), g3(m, s, C.high(1n+j, V), 0n, eh, C.low(1n+j, V), V, el, C.shift(j, 1n), C.shift(j, 1n), {==})) 202 +e3 = Equal.cong(Bool, F.F64, t => SF.round(s, SF.b2n(t), 3000n), upn(m, s, 0n, V, vc), upn(m, s, 0n, V, C.shift(j, 1n)), Equal.sym(Bool, upn(m, s, 0n, V, C.shift(j, 1n)), upn(m, s, 0n, V, vc), eu)) 203 Equal.trans(F.F64, F.ri_q(m, s, WU.U64{0, 0}, w, WU.U64{0, c}), G(m, s, 0n, V, vc), SF.round(s, SF.integral(m, s, V, 1n+j), 3000n), e0, Equal.trans(F.F64, G(m, s, 0n, V, vc), G(m, s, 0n, V, C.shift(j, 1n)), SF.round(s, SF.integral(m, s, V, 1n+j), 3000n), e3, Equal.trans(F.F64, G(m, s, 0n, V, C.shift(j, 1n)), G(m, s, C.high(1n+j, V), C.low(1n+j, V), C.shift(j, 1n)), SF.round(s, SF.integral(m, s, V, 1n+j), 3000n), e2, e1))) 204 205 def rik_c(+m: F.RMode, +s: Bool, +w: WU.U64, +j: Nat, +hw: {C.fits(53n, SW.value(w)) == True{} : Bool}, +b: Bool, +hb: {Nat.is_lt(1n+j, 64n) == b : Bool}) -> {F.ri_k(m, s, w, 1n+j, b) == SF.round(s, SF.integral(m, s, SW.value(w), 1n+j), 3000n) : F.F64}: 206 match b: 207 case True{}: 208 +V = SW.value(w) 209 Equal.trans(F.F64, F.ri_k(m, s, w, 1n+j, True{}), G(m, s, C.high(1n+j, V), C.low(1n+j, V), C.shift(j, 1n)), SF.round(s, SF.integral(m, s, V, 1n+j), 3000n), small_case(m, s, w, j, hb), Equal.sym(F.F64, SF.round(s, SF.integral(m, s, V, 1n+j), 3000n), G(m, s, C.high(1n+j, V), C.low(1n+j, V), C.shift(j, 1n)), integ(m, s, V, j))) 210 case False{}: 211 large_case(m, s, w, j, N.not_lt_le(1n+j, 64n, hb), hw, 1n, {==}, 2147483648, {==}) 212 213 def rik(+m: F.RMode, +s: Bool, +w: WU.U64, +k: Nat, +hk: {Nat.is_le(1n, k) == True{} : Bool}, +hw: {C.fits(53n, SW.value(w)) == True{} : Bool}) -> {F.ri_k(m, s, w, k, Nat.is_lt(k, 64n)) == SF.round(s, SF.integral(m, s, SW.value(w), k), 3000n) : F.F64}: 214 match k: 215 case 0n: 216 Empty.absurd({F.ri_k(m, s, w, 0n, Nat.is_lt(0n, 64n)) == SF.round(s, SF.integral(m, s, SW.value(w), 0n), 3000n) : F.F64}, FL.true_ne_false(Equal.sym(Bool, False{}, True{}, hk))) 217 case 1n+ +j: 218 rik_c(m, s, w, j, hw, Nat.is_lt(1n+j, 64n), {==}) 219 220 # ---- the finite case and the special values ---- 221 222 def RI(+m: F.RMode, +x: F.F64) -> F.F64: 223 SF.round(SF.sign(x), SF.integral(m, SF.sign(x), SF.mant(x), Nat.sub(SF.zb(), SF.xexp(x))), SF.zb()) 224 225 def ti_fin(+m: F.RMode, +x: F.F64, +c: Bool, +hc: {Nat.is_le(3000n, F.dexp(x)) == c : Bool}) -> {F.ri_fin(m, x, c) == SF.pick(F.F64, c, x, RI(m, x)) : F.F64}: 226 match c: 227 case True{}: 228 {==} 229 case False{}: 230 +k = Nat.sub(3000n, F.dexp(x)) 231 +hk = FR.lt_sub_pos(F.dexp(x), 3000n, N.not_le_lt(3000n, F.dexp(x), hc)) 232 +hw = L.subst(Nat, t => {C.fits(53n, t) == True{} : Bool}, SF.mant(x), SW.value(F.dmant(x)), Equal.sym(Nat, SW.value(F.dmant(x)), SF.mant(x), T.dmant_value(x)), T.mant_fits(x)) 233 +e0 = rik(m, F.signbit(x), F.dmant(x), k, hk, hw) 234 +e1 = Equal.cong(Bool, F.F64, t => SF.round(t, SF.integral(m, t, SW.value(F.dmant(x)), k), 3000n), F.signbit(x), SF.sign(x), FB.signbit_value(x)) 235 +e2 = Equal.cong(Nat, F.F64, t => SF.round(SF.sign(x), SF.integral(m, SF.sign(x), t, k), 3000n), SW.value(F.dmant(x)), SF.mant(x), T.dmant_value(x)) 236 +e3 = Equal.cong(Nat, F.F64, t => SF.round(SF.sign(x), SF.integral(m, SF.sign(x), SF.mant(x), Nat.sub(3000n, t)), 3000n), F.dexp(x), SF.xexp(x), T.dexp_value(x)) 237 +r0 = SF.round(F.signbit(x), SF.integral(m, F.signbit(x), SW.value(F.dmant(x)), k), 3000n) 238 +r1 = SF.round(SF.sign(x), SF.integral(m, SF.sign(x), SW.value(F.dmant(x)), k), 3000n) 239 +r2 = SF.round(SF.sign(x), SF.integral(m, SF.sign(x), SF.mant(x), k), 3000n) 240 Equal.trans(F.F64, F.ri_fin(m, x, False{}), r0, RI(m, x), e0, Equal.trans(F.F64, r0, r1, RI(m, x), e1, Equal.trans(F.F64, r1, r2, RI(m, x), e2, e3))) 241 242 def ti_c(+m: F.RMode, +x: F.F64, +t: Bool, +z: Bool, +hz: {X.is_zero(F.frac(x)) == z : Bool}) -> {F.ri_cls(m, x, t) == SF.pick(F.F64, Bool.and(t, Bool.not(z)), SF.qnan(), SF.pick(F.F64, Bool.or(Bool.and(t, z), Nat.is_le(SF.zb(), SF.xexp(x))), x, RI(m, x))) : F.F64}: 243 match t z: 244 case True{} True{}: 245 Equal.cong(Bool, F.F64, b => F.nan_or(x, Bool.not(b)), X.is_zero(F.frac(x)), True{}, hz) 246 case True{} False{}: 247 Equal.cong(Bool, F.F64, b => F.nan_or(x, Bool.not(b)), X.is_zero(F.frac(x)), False{}, hz) 248 case False{} _: 249 +e1 = ti_fin(m, x, Nat.is_le(3000n, F.dexp(x)), {==}) 250 +e2 = Equal.cong(Nat, F.F64, u => SF.pick(F.F64, Nat.is_le(3000n, u), x, RI(m, x)), F.dexp(x), SF.xexp(x), T.dexp_value(x)) 251 Equal.trans(F.F64, F.ri_fin(m, x, Nat.is_le(3000n, F.dexp(x))), SF.pick(F.F64, Nat.is_le(3000n, F.dexp(x)), x, RI(m, x)), SF.pick(F.F64, Nat.is_le(3000n, SF.xexp(x)), x, RI(m, x)), e1, e2) 252 253 def ti_value(+m: F.RMode, +x: F.F64) -> {F.to_integral(m, x) == SF.to_integral(m, x) : F.F64}: 254 +e1 = Equal.cong(Nat, F.F64, u => F.ri_cls(m, x, Nat.is_eq(u, 2047n)), F.exp_field(x), SF.efield(x), T.ea(x)) 255 Equal.trans(F.F64, F.to_integral(m, x), F.ri_cls(m, x, Nat.is_eq(SF.efield(x), 2047n)), SF.to_integral(m, x), e1, ti_c(m, x, Nat.is_eq(SF.efield(x), 2047n), Nat.is_eq(SF.frac(x), 0n), T.fz(x))) 256 257 def trunc_value(+x: F.F64) -> SF.Trunc.value(x): 258 ti_value(F.Trunc{}, x) 259 260 def floor_value(+x: F.F64) -> SF.Floor.value(x): 261 ti_value(F.Floor{}, x) 262 263 def ceil_value(+x: F.F64) -> SF.Ceil.value(x): 264 ti_value(F.Ceil{}, x) 265 266 def round_value(+x: F.F64) -> SF.Round.value(x): 267 ti_value(F.Even{}, x)