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 ../../../src/math/num.bend as NE 9 import ../../../src/math/natural.bend as M 10 import ../../lib/nat.bend as N 11 import ../../lib/logic.bend as L 12 import ../../lib/lemmas/proofs/nat_algebra.bend as NA 13 import ./width.bend as WW 14 import ./w64add.bend as WA 15 import ./w64sh.bend as SH 16 import ./w64clz.bend as CZ 17 import ./u32laws.bend as LW 18 import ./f64bits.bend as FB 19 import ./f64light.bend as FL 20 import ./f64round.bend as FR 21 import ./f64rtools.bend as RT 22 import ./f64nrp.bend as NR 23 import ./f64bl.bend as BL 24 import ./f64tools.bend as T 25 import ./f64rint.bend as RI 26 27 # The conversions to unsigned integers (python_style_math_stdlib_design.pdf 28 # 3.1: int(x) truncates toward zero; 2.6: a fixed width raises instead of 29 # wrapping; IEEE 754-2019 5.8 convertToInteger with the invalid exception 30 # as an error value): ToU64.value, ToU32.value, FloorU64.value, 31 # CeilU64.value and RoundU64.value. A finite x is m 2^(xexp - Z): below 2^52 32 # its integer part is m >> (Z - xexp) (Shr.value), above it m << (xexp - Z), 33 # which fits 64 bits exactly when (xexp - Z) + bit_length(m) <= 64 34 # (Clz.value, f64nrp.tbf / tbn). 35 36 def v(+x: U32) -> Nat: 37 U32.to_nat(x) 38 39 # the spec's verdict on a nonnegative-or-zero integer part n with sign s 40 def TN(+s: Bool, +n: Nat) -> Result<&2, &2, NE.NumError, Nat>: 41 SF.pick(Result<&2, &2, NE.NumError, Nat>, Bool.or(Bool.and(s, Bool.not(Nat.is_eq(n, 0n))), Bool.not(C.fits(64n, n))), Fail{NE.Overflow{}}, Done{n}) 42 43 def TS(+s: Bool, +n: Nat) -> Result<&2, &2, NE.NumError, Nat>: 44 SF.pick(Result<&2, &2, NE.NumError, Nat>, Bool.and(s, Bool.not(Nat.is_eq(n, 0n))), Fail{NE.Overflow{}}, Done{n}) 45 46 def tn(+w: WU.U64, +b: Bool) -> {SF.rv64(F.tu_neg(w, b)) == SF.pick(Result<&2, &2, NE.NumError, Nat>, b, Fail{NE.Overflow{}}, Done{SW.value(w)}) : Result<&2, &2, NE.NumError, Nat>}: 47 match b: 48 case True{}: 49 {==} 50 case False{}: 51 {==} 52 53 def tuint_v(+s: Bool, +w: WU.U64) -> {SF.rv64(F.tu_int(s, w)) == TS(s, SW.value(w)) : Result<&2, &2, NE.NumError, Nat>}: 54 +e1 = Equal.cong(Bool, Result<&2, &2, NE.NumError, Nat>, b => SF.rv64(F.tu_neg(w, Bool.and(s, Bool.not(b)))), X.is_zero(w), Nat.is_eq(SW.value(w), 0n), WA.is_zero_value(w)) 55 Equal.trans(Result<&2, &2, NE.NumError, Nat>, SF.rv64(F.tu_int(s, w)), SF.rv64(F.tu_neg(w, Bool.and(s, Bool.not(Nat.is_eq(SW.value(w), 0n))))), TS(s, SW.value(w)), e1, tn(w, Bool.and(s, Bool.not(Nat.is_eq(SW.value(w), 0n))))) 56 57 # TN is TS when n fits 64 bits 58 def tn_fit(+s: Bool, +n: Nat, +hf: {C.fits(64n, n) == True{} : Bool}) -> {TS(s, n) == TN(s, n) : Result<&2, &2, NE.NumError, Nat>}: 59 +A = Bool.and(s, Bool.not(Nat.is_eq(n, 0n))) 60 +e1 = Equal.cong(Bool, Result<&2, &2, NE.NumError, Nat>, b => SF.pick(Result<&2, &2, NE.NumError, Nat>, Bool.or(A, Bool.not(b)), Fail{NE.Overflow{}}, Done{n}), C.fits(64n, n), True{}, hf) 61 +e2 = Equal.cong(Bool, Result<&2, &2, NE.NumError, Nat>, b => SF.pick(Result<&2, &2, NE.NumError, Nat>, b, Fail{NE.Overflow{}}, Done{n}), Bool.or(A, False{}), A, FR.or_f(A)) 62 Equal.sym(Result<&2, &2, NE.NumError, Nat>, TN(s, n), TS(s, n), Equal.trans(Result<&2, &2, NE.NumError, Nat>, TN(s, n), SF.pick(Result<&2, &2, NE.NumError, Nat>, Bool.or(A, False{}), Fail{NE.Overflow{}}, Done{n}), TS(s, n), e1, e2)) 63 64 # ---- below 2^52: a right shift ---- 65 66 def le_k64(+k: Nat) -> {Nat.is_le(64n, Nat.add(k, 64n)) == True{} : Bool}: 67 L.subst(Nat, t => {Nat.is_le(64n, t) == True{} : Bool}, Nat.add(64n, k), Nat.add(k, 64n), NA.add_comm(64n, k), N.le_add_right(64n, k)) 68 69 def small_nat(+s: Bool, +w: WU.U64, +k: Nat) -> {SF.rv64(F.tu_int(s, X.shr(w, k))) == TN(s, C.high(k, SW.value(w))) : Result<&2, &2, NE.NumError, Nat>}: 70 +V = SW.value(w) 71 +H = C.high(k, V) 72 +e1 = tuint_v(s, X.shr(w, k)) 73 +e2 = Equal.cong(Nat, Result<&2, &2, NE.NumError, Nat>, n => TS(s, n), SW.value(X.shr(w, k)), H, SH.shr_value(w, k)) 74 +hf = Equal.trans(Bool, C.fits(64n, H), C.fits(Nat.add(k, 64n), V), True{}, Equal.sym(Bool, C.fits(Nat.add(k, 64n), V), C.fits(64n, H), FR.fits_hc(k, 64n, V)), SH.fits_mono(64n, Nat.add(k, 64n), V, le_k64(k), FL.vb64(w))) 75 Equal.trans(Result<&2, &2, NE.NumError, Nat>, SF.rv64(F.tu_int(s, X.shr(w, k))), TS(s, SW.value(X.shr(w, k))), TN(s, H), e1, Equal.trans(Result<&2, &2, NE.NumError, Nat>, TS(s, SW.value(X.shr(w, k))), TS(s, H), TN(s, H), e2, tn_fit(s, H, hf))) 76 77 # ---- at least 2^52: a left shift that must fit ---- 78 79 def subsub(+a: Nat, +b: Nat, +h: {Nat.is_le(b, a) == True{} : Bool}) -> {Nat.sub(a, Nat.sub(a, b)) == b : Nat}: 80 +d = Nat.sub(a, b) 81 L.subst(Nat, t => {Nat.sub(t, d) == b : Nat}, Nat.add(b, d), a, N.sub_add(a, b, h), FR.sub_add_l(b, d)) 82 83 def big_c(+s: Bool, +w: WU.U64, +k: Nat, +hz: {Nat.is_eq(SW.value(w), 0n) == False{} : Bool}, +c: Bool, +hc: {Nat.is_le(Nat.add(k, M.bit_length(SW.value(w))), 64n) == c : Bool}) -> {SF.rv64(F.tu_big(s, w, k, c)) == TN(s, C.shift(k, SW.value(w))) : Result<&2, &2, NE.NumError, Nat>}: 84 match c: 85 case True{}: 86 +V = SW.value(w) 87 +B = M.bit_length(V) 88 +S = C.shift(k, V) 89 +hb1 = BL.bl_pos(V, hz, B, {==}) 90 +hkl = Equal.trans(Bool, Nat.is_lt(k, Nat.add(k, B)), Nat.is_lt(Nat.add(k, 0n), Nat.add(k, B)), True{}, Equal.cong(Nat, Bool, t => Nat.is_lt(t, Nat.add(k, B)), k, Nat.add(k, 0n), Equal.sym(Nat, Nat.add(k, 0n), k, N.add_zero(k))), N.lt_add_left(0n, B, k, N.succ_le_lt(0n, B, hb1))) 91 +hk = N.lt_le_trans(k, Nat.add(k, B), 64n, hkl, hc) 92 +ev = FL.shl_v(w, k, B, hk, hc, RT.bl_fit(V)) 93 +e1 = tuint_v(s, X.shl(w, k)) 94 +e2 = Equal.cong(Nat, Result<&2, &2, NE.NumError, Nat>, n => TS(s, n), SW.value(X.shl(w, k)), S, ev) 95 +hf = SH.fits_mono(Nat.add(k, B), 64n, S, hc, NR.tbf(k, V, Nat.add(k, B), {==})) 96 Equal.trans(Result<&2, &2, NE.NumError, Nat>, SF.rv64(F.tu_int(s, X.shl(w, k))), TS(s, SW.value(X.shl(w, k))), TN(s, S), e1, Equal.trans(Result<&2, &2, NE.NumError, Nat>, TS(s, SW.value(X.shl(w, k))), TS(s, S), TN(s, S), e2, tn_fit(s, S, hf))) 97 case False{}: 98 +V = SW.value(w) 99 +B = M.bit_length(V) 100 +S = C.shift(k, V) 101 +A = Bool.and(s, Bool.not(Nat.is_eq(S, 0n))) 102 +J = Nat.add(k, B) 103 +K = Nat.sub(J, 1n) 104 +hJ = N.not_le_lt(J, 64n, hc) 105 +hJ1 = N.le_trans(1n, 65n, J, {==}, N.lt_succ_le_succ(64n, J, hJ)) 106 +ek = Equal.sym(Nat, Nat.add(1n, K), J, N.sub_add(J, 1n, hJ1)) 107 +hK = N.lt_succ_le(64n, K, L.subst(Nat, t => {Nat.is_lt(64n, t) == True{} : Bool}, J, 1n+K, ek, hJ)) 108 +nf = FL.nfit_mono(64n, K, S, hK, NR.tbn(k, V, K, hz, ek)) 109 +e1 = Equal.cong(Bool, Result<&2, &2, NE.NumError, Nat>, b => SF.pick(Result<&2, &2, NE.NumError, Nat>, Bool.or(A, Bool.not(b)), Fail{NE.Overflow{}}, Done{S}), C.fits(64n, S), False{}, nf) 110 +e2 = Equal.cong(Bool, Result<&2, &2, NE.NumError, Nat>, b => SF.pick(Result<&2, &2, NE.NumError, Nat>, b, Fail{NE.Overflow{}}, Done{S}), Bool.or(A, True{}), True{}, FR.or_t(A)) 111 Equal.sym(Result<&2, &2, NE.NumError, Nat>, TN(s, S), Fail{NE.Overflow{}}, Equal.trans(Result<&2, &2, NE.NumError, Nat>, TN(s, S), SF.pick(Result<&2, &2, NE.NumError, Nat>, Bool.or(A, True{}), Fail{NE.Overflow{}}, Done{S}), Fail{NE.Overflow{}}, e1, e2)) 112 113 def big_nat(+s: Bool, +w: WU.U64, +k: Nat, +hz: {Nat.is_eq(SW.value(w), 0n) == False{} : Bool}, +hw: {C.fits(53n, SW.value(w)) == True{} : Bool}) -> {SF.rv64(F.tu_big(s, w, k, Nat.is_le(Nat.add(k, Nat.sub(64n, X.clz(w))), 64n))) == TN(s, C.shift(k, SW.value(w))) : Result<&2, &2, NE.NumError, Nat>}: 114 +V = SW.value(w) 115 +B = M.bit_length(V) 116 +hB = N.le_trans(B, 53n, 64n, BL.bl_le(53n, V, hw, Nat.is_le(B, 53n), {==}), {==}) 117 +eb = Equal.trans(Nat, Nat.sub(64n, X.clz(w)), Nat.sub(64n, Nat.sub(64n, B)), B, Equal.cong(Nat, Nat, t => Nat.sub(64n, t), X.clz(w), Nat.sub(64n, B), CZ.clz_value(w)), subsub(64n, B, hB)) 118 +e1 = Equal.cong(Nat, Result<&2, &2, NE.NumError, Nat>, t => SF.rv64(F.tu_big(s, w, k, Nat.is_le(Nat.add(k, t), 64n))), Nat.sub(64n, X.clz(w)), B, eb) 119 Equal.trans(Result<&2, &2, NE.NumError, Nat>, SF.rv64(F.tu_big(s, w, k, Nat.is_le(Nat.add(k, Nat.sub(64n, X.clz(w))), 64n))), SF.rv64(F.tu_big(s, w, k, Nat.is_le(Nat.add(k, B), 64n))), TN(s, C.shift(k, V)), e1, big_c(s, w, k, hz, Nat.is_le(Nat.add(k, B), 64n), {==})) 120 121 # ---- the finite case ---- 122 123 # a double with scale at least Z is normal, so its significand is not zero 124 # the significand at an abstract exponent-is-zero bit b: instantiated at 125 # False, the hidden bit 2^52 is never evaluated 126 def mz(+x: F.F64, +b: Bool, +hb: {Nat.is_eq(SF.efield(x), 0n) == b : Bool}) -> {Nat.is_eq(SF.mant(x), 0n) == Nat.is_eq(Nat.add(SF.frac(x), C.shift(52n, SF.b2n(Bool.not(b)))), 0n) : Bool}: 127 Equal.cong(Bool, Bool, t => Nat.is_eq(Nat.add(SF.frac(x), C.shift(52n, SF.b2n(Bool.not(t)))), 0n), Nat.is_eq(SF.efield(x), 0n), b, hb) 128 129 def bnz_c(+x: F.F64, +z: Bool, +hz: {Nat.is_eq(F.exp_field(x), 0n) == z : Bool}, +h: {Nat.is_le(3000n, F.dexp_z(F.exp_field(x), z)) == True{} : Bool}) -> {Nat.is_eq(SF.mant(x), 0n) == False{} : Bool}: 130 match z: 131 case True{}: 132 Empty.absurd({Nat.is_eq(SF.mant(x), 0n) == False{} : Bool}, FL.true_ne_false(Equal.sym(Bool, False{}, True{}, h))) 133 case False{}: 134 +hz2 = L.subst(Nat, t => {Nat.is_eq(t, 0n) == False{} : Bool}, F.exp_field(x), SF.efield(x), T.ea(x), hz) 135 +Fr = SF.frac(x) 136 +e1 = mz(x, False{}, hz2) 137 # the hidden bit stays b2n(not False): no closed 2^52 138 +H = SF.b2n(Bool.not(False{})) 139 +e2 = FB.z2(Fr, 52n, H) 140 +e3 = Equal.cong(Bool, Bool, t => Bool.and(Nat.is_eq(Fr, 0n), t), Nat.is_eq(H, 0n), False{}, {==}) 141 Equal.trans(Bool, Nat.is_eq(SF.mant(x), 0n), Nat.is_eq(Nat.add(Fr, C.shift(52n, H)), 0n), False{}, e1, Equal.trans(Bool, Nat.is_eq(Nat.add(Fr, C.shift(52n, H)), 0n), Bool.and(Nat.is_eq(Fr, 0n), Nat.is_eq(H, 0n)), False{}, e2, Equal.trans(Bool, Bool.and(Nat.is_eq(Fr, 0n), Nat.is_eq(H, 0n)), Bool.and(Nat.is_eq(Fr, 0n), False{}), False{}, e3, FR.and_f(Nat.is_eq(Fr, 0n))))) 142 143 def big_nz(+x: F.F64, +h: {Nat.is_le(3000n, F.dexp(x)) == True{} : Bool}) -> {Nat.is_eq(SW.value(F.dmant(x)), 0n) == False{} : Bool}: 144 L.subst(Nat, t => {Nat.is_eq(t, 0n) == False{} : Bool}, SF.mant(x), SW.value(F.dmant(x)), Equal.sym(Nat, SW.value(F.dmant(x)), SF.mant(x), T.dmant_value(x)), bnz_c(x, Nat.is_eq(F.exp_field(x), 0n), {==}, h)) 145 146 def hw53(+x: F.F64) -> {C.fits(53n, SW.value(F.dmant(x))) == True{} : Bool}: 147 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)) 148 149 def IPc(+x: F.F64, +c: Bool) -> Nat: 150 SF.pick(Nat, c, C.shift(Nat.sub(SF.xexp(x), SF.zb()), SF.mant(x)), C.high(Nat.sub(SF.zb(), SF.xexp(x)), SF.mant(x))) 151 152 def tu_fin_c(+x: F.F64, +c: Bool, +hc: {Nat.is_le(3000n, F.dexp(x)) == c : Bool}) -> {SF.rv64(F.tu_fin(x, c)) == TN(SF.sign(x), IPc(x, c)) : Result<&2, &2, NE.NumError, Nat>}: 153 match c: 154 case True{}: 155 +k = Nat.sub(F.dexp(x), 3000n) 156 +e0 = big_nat(F.signbit(x), F.dmant(x), k, big_nz(x, hc), hw53(x)) 157 +e1 = Equal.cong(Bool, Result<&2, &2, NE.NumError, Nat>, t => TN(t, C.shift(k, SW.value(F.dmant(x)))), F.signbit(x), SF.sign(x), FB.signbit_value(x)) 158 +e2 = Equal.cong(Nat, Result<&2, &2, NE.NumError, Nat>, t => TN(SF.sign(x), C.shift(k, t)), SW.value(F.dmant(x)), SF.mant(x), T.dmant_value(x)) 159 +e3 = Equal.cong(Nat, Result<&2, &2, NE.NumError, Nat>, t => TN(SF.sign(x), C.shift(Nat.sub(t, 3000n), SF.mant(x))), F.dexp(x), SF.xexp(x), T.dexp_value(x)) 160 +r0 = TN(F.signbit(x), C.shift(k, SW.value(F.dmant(x)))) 161 +r1 = TN(SF.sign(x), C.shift(k, SW.value(F.dmant(x)))) 162 +r2 = TN(SF.sign(x), C.shift(k, SF.mant(x))) 163 Equal.trans(Result<&2, &2, NE.NumError, Nat>, SF.rv64(F.tu_fin(x, True{})), r0, TN(SF.sign(x), IPc(x, True{})), e0, Equal.trans(Result<&2, &2, NE.NumError, Nat>, r0, r1, TN(SF.sign(x), IPc(x, True{})), e1, Equal.trans(Result<&2, &2, NE.NumError, Nat>, r1, r2, TN(SF.sign(x), IPc(x, True{})), e2, e3))) 164 case False{}: 165 +k = Nat.sub(3000n, F.dexp(x)) 166 +e0 = small_nat(F.signbit(x), F.dmant(x), k) 167 +e1 = Equal.cong(Bool, Result<&2, &2, NE.NumError, Nat>, t => TN(t, C.high(k, SW.value(F.dmant(x)))), F.signbit(x), SF.sign(x), FB.signbit_value(x)) 168 +e2 = Equal.cong(Nat, Result<&2, &2, NE.NumError, Nat>, t => TN(SF.sign(x), C.high(k, t)), SW.value(F.dmant(x)), SF.mant(x), T.dmant_value(x)) 169 +e3 = Equal.cong(Nat, Result<&2, &2, NE.NumError, Nat>, t => TN(SF.sign(x), C.high(Nat.sub(3000n, t), SF.mant(x))), F.dexp(x), SF.xexp(x), T.dexp_value(x)) 170 +r0 = TN(F.signbit(x), C.high(k, SW.value(F.dmant(x)))) 171 +r1 = TN(SF.sign(x), C.high(k, SW.value(F.dmant(x)))) 172 +r2 = TN(SF.sign(x), C.high(k, SF.mant(x))) 173 Equal.trans(Result<&2, &2, NE.NumError, Nat>, SF.rv64(F.tu_fin(x, False{})), r0, TN(SF.sign(x), IPc(x, False{})), e0, Equal.trans(Result<&2, &2, NE.NumError, Nat>, r0, r1, TN(SF.sign(x), IPc(x, False{})), e1, Equal.trans(Result<&2, &2, NE.NumError, Nat>, r1, r2, TN(SF.sign(x), IPc(x, False{})), e2, e3))) 174 175 def TNR(+a: Bool, +b: Bool, +c: Bool, +n: Nat, +f: Bool) -> Result<&2, &2, NE.NumError, Nat>: 176 SF.pick(Result<&2, &2, NE.NumError, Nat>, a, Fail{NE.BadDomain{}}, SF.pick(Result<&2, &2, NE.NumError, Nat>, Bool.or(b, Bool.or(c, Bool.not(f))), Fail{NE.Overflow{}}, Done{n})) 177 178 def tu_c(+x: F.F64, +t: Bool, +z: Bool, +hz: {X.is_zero(F.frac(x)) == z : Bool}) -> {SF.rv64(F.tu_cls(x, t)) == TNR(Bool.and(t, Bool.not(z)), Bool.and(t, z), Bool.and(SF.sign(x), Bool.not(Nat.is_eq(SF.int_part(x), 0n))), SF.int_part(x), C.fits(64n, SF.int_part(x))) : Result<&2, &2, NE.NumError, Nat>}: 179 match t z: 180 case True{} True{}: 181 Equal.cong(Bool, Result<&2, &2, NE.NumError, Nat>, b => SF.rv64(F.tu_top(Bool.not(b))), X.is_zero(F.frac(x)), True{}, hz) 182 case True{} False{}: 183 Equal.cong(Bool, Result<&2, &2, NE.NumError, Nat>, b => SF.rv64(F.tu_top(Bool.not(b))), X.is_zero(F.frac(x)), False{}, hz) 184 case False{} _: 185 +e1 = tu_fin_c(x, Nat.is_le(3000n, F.dexp(x)), {==}) 186 +e2 = Equal.cong(Nat, Result<&2, &2, NE.NumError, Nat>, u => TN(SF.sign(x), IPc(x, Nat.is_le(3000n, u))), F.dexp(x), SF.xexp(x), T.dexp_value(x)) 187 Equal.trans(Result<&2, &2, NE.NumError, Nat>, SF.rv64(F.tu_fin(x, Nat.is_le(3000n, F.dexp(x)))), TN(SF.sign(x), IPc(x, Nat.is_le(3000n, F.dexp(x)))), TN(SF.sign(x), SF.int_part(x)), e1, e2) 188 189 def to_u64_value(+x: F.F64) -> SF.ToU64.value(x): 190 +e1 = Equal.cong(Nat, Result<&2, &2, NE.NumError, Nat>, u => SF.rv64(F.tu_cls(x, Nat.is_eq(u, 2047n))), F.exp_field(x), SF.efield(x), T.ea(x)) 191 Equal.trans(Result<&2, &2, NE.NumError, Nat>, SF.rv64(F.to_u64(x)), SF.rv64(F.tu_cls(x, Nat.is_eq(SF.efield(x), 2047n))), SF.to_nat(x, 64n), e1, tu_c(x, Nat.is_eq(SF.efield(x), 2047n), Nat.is_eq(SF.frac(x), 0n), T.fz(x))) 192 193 # ---- 32 bits: the 64-bit result, when its high word is zero ---- 194 195 def f32r(r: Result<&2, &2, NE.NumError, Nat>) -> Result<&2, &2, NE.NumError, Nat>: 196 match r: 197 case Fail{e}: 198 Fail{e} 199 case Done{+n}: 200 SF.pick(Result<&2, &2, NE.NumError, Nat>, C.fits(32n, n), Done{n}, Fail{NE.Overflow{}}) 201 202 def t32_c(+l: U32, +h: U32, +c: Bool, +hc: {U32.is_zero(h) == c : Bool}) -> {SF.rv32(F.tu32_w(WU.U64{l, h}, c)) == SF.pick(Result<&2, &2, NE.NumError, Nat>, c, Done{SW.value(WU.U64{l, h})}, Fail{NE.Overflow{}}) : Result<&2, &2, NE.NumError, Nat>}: 203 match c: 204 case True{}: 205 +h0 = N.eq_from_is_eq(v(h), 0n, Equal.trans(Bool, Nat.is_eq(v(h), 0n), U32.is_zero(h), True{}, Equal.sym(Bool, U32.is_zero(h), Nat.is_eq(v(h), 0n), LW.zero_nat(h)), hc)) 206 +e1 = Equal.cong(Nat, Nat, t => Nat.add(v(l), C.shift(32n, t)), v(h), 0n, h0) 207 +e2 = Equal.trans(Nat, SW.value(WU.U64{l, h}), Nat.add(v(l), 0n), v(l), Equal.trans(Nat, SW.value(WU.U64{l, h}), Nat.add(v(l), C.shift(32n, 0n)), Nat.add(v(l), 0n), e1, {==}), N.add_zero(v(l))) 208 Equal.cong(Nat, Result<&2, &2, NE.NumError, Nat>, t => Done{t}, v(l), SW.value(WU.U64{l, h}), Equal.sym(Nat, SW.value(WU.U64{l, h}), v(l), e2)) 209 case False{}: 210 {==} 211 212 def t32w(+w: WU.U64) -> {SF.rv32(F.tu32_w(w, U32.is_zero(X.hi(w)))) == SF.pick(Result<&2, &2, NE.NumError, Nat>, C.fits(32n, SW.value(w)), Done{SW.value(w)}, Fail{NE.Overflow{}}) : Result<&2, &2, NE.NumError, Nat>}: 213 match w: 214 case WU.U64{+l, +h}: 215 +ef = Equal.trans(Bool, U32.is_zero(h), Nat.is_eq(v(h), 0n), C.fits(32n, SW.value(WU.U64{l, h})), LW.zero_nat(h), Equal.cong(Nat, Bool, t => Nat.is_eq(t, 0n), v(h), C.high(32n, SW.value(WU.U64{l, h})), Equal.sym(Nat, C.high(32n, SW.value(WU.U64{l, h})), v(h), WW.high_u(32n, v(l), v(h), LW.vb(l))))) 216 +e1 = t32_c(l, h, U32.is_zero(h), {==}) 217 +e2 = Equal.cong(Bool, Result<&2, &2, NE.NumError, Nat>, b => SF.pick(Result<&2, &2, NE.NumError, Nat>, b, Done{SW.value(WU.U64{l, h})}, Fail{NE.Overflow{}}), U32.is_zero(h), C.fits(32n, SW.value(WU.U64{l, h})), ef) 218 Equal.trans(Result<&2, &2, NE.NumError, Nat>, SF.rv32(F.tu32_w(WU.U64{l, h}, U32.is_zero(h))), SF.pick(Result<&2, &2, NE.NumError, Nat>, U32.is_zero(h), Done{SW.value(WU.U64{l, h})}, Fail{NE.Overflow{}}), SF.pick(Result<&2, &2, NE.NumError, Nat>, C.fits(32n, SW.value(WU.U64{l, h})), Done{SW.value(WU.U64{l, h})}, Fail{NE.Overflow{}}), e1, e2) 219 220 def t32(r: Result<&2, &2, NE.NumError, WU.U64>) -> {SF.rv32(F.tu32(r)) == f32r(SF.rv64(r)) : Result<&2, &2, NE.NumError, Nat>}: 221 match r: 222 case Fail{e}: 223 {==} 224 case Done{+w}: 225 t32w(w) 226 227 def pn(+b: Bool, +n: Nat) -> {SF.pick(Result<&2, &2, NE.NumError, Nat>, b, Done{n}, Fail{NE.Overflow{}}) == SF.pick(Result<&2, &2, NE.NumError, Nat>, Bool.not(b), Fail{NE.Overflow{}}, Done{n}) : Result<&2, &2, NE.NumError, Nat>}: 228 match b: 229 case True{}: 230 {==} 231 case False{}: 232 {==} 233 234 def s32_c(+a: Bool, +b: Bool, +c: Bool, +n: Nat, +f: Bool, +hf: {C.fits(64n, n) == f : Bool}) -> {f32r(TNR(a, b, c, n, f)) == TNR(a, b, c, n, C.fits(32n, n)) : Result<&2, &2, NE.NumError, Nat>}: 235 match a b c f: 236 case True{} _ _ _: 237 {==} 238 case False{} True{} _ _: 239 {==} 240 case False{} False{} True{} _: 241 {==} 242 case False{} False{} False{} True{}: 243 pn(C.fits(32n, n), n) 244 case False{} False{} False{} False{}: 245 +g = FL.nfit_mono(32n, 64n, n, {==}, hf) 246 Equal.cong(Bool, Result<&2, &2, NE.NumError, Nat>, t => TNR(False{}, False{}, False{}, n, t), False{}, C.fits(32n, n), Equal.sym(Bool, C.fits(32n, n), False{}, g)) 247 248 def to_u32_value(+x: F.F64) -> SF.ToU32.value(x): 249 +R64 = SF.rv64(F.to_u64(x)) 250 +e1 = t32(F.to_u64(x)) 251 +e2 = Equal.cong(Result<&2, &2, NE.NumError, Nat>, Result<&2, &2, NE.NumError, Nat>, r => f32r(r), R64, SF.to_nat(x, 64n), to_u64_value(x)) 252 +IP = SF.int_part(x) 253 +e3 = s32_c(SF.is_nan(x), SF.is_inf(x), Bool.and(SF.sign(x), Bool.not(Nat.is_eq(IP, 0n))), IP, C.fits(64n, IP), {==}) 254 Equal.trans(Result<&2, &2, NE.NumError, Nat>, SF.rv32(F.to_u32(x)), f32r(R64), SF.to_nat(x, 32n), e1, Equal.trans(Result<&2, &2, NE.NumError, Nat>, f32r(R64), f32r(SF.to_nat(x, 64n)), SF.to_nat(x, 32n), e2, e3)) 255 256 # ---- floor, ceil, round, then the conversion ---- 257 258 def floor_u64_value(+x: F.F64) -> SF.FloorU64.value(x): 259 Equal.trans(Result<&2, &2, NE.NumError, Nat>, SF.rv64(F.to_u64(F.floor(x))), SF.to_nat(F.floor(x), 64n), SF.to_nat(SF.to_integral(F.Floor{}, x), 64n), to_u64_value(F.floor(x)), Equal.cong(F.F64, Result<&2, &2, NE.NumError, Nat>, y => SF.to_nat(y, 64n), F.floor(x), SF.to_integral(F.Floor{}, x), RI.floor_value(x))) 260 261 def ceil_u64_value(+x: F.F64) -> SF.CeilU64.value(x): 262 Equal.trans(Result<&2, &2, NE.NumError, Nat>, SF.rv64(F.to_u64(F.ceil(x))), SF.to_nat(F.ceil(x), 64n), SF.to_nat(SF.to_integral(F.Ceil{}, x), 64n), to_u64_value(F.ceil(x)), Equal.cong(F.F64, Result<&2, &2, NE.NumError, Nat>, y => SF.to_nat(y, 64n), F.ceil(x), SF.to_integral(F.Ceil{}, x), RI.ceil_value(x))) 263 264 def round_u64_value(+x: F.F64) -> SF.RoundU64.value(x): 265 Equal.trans(Result<&2, &2, NE.NumError, Nat>, SF.rv64(F.to_u64(F.round(x))), SF.to_nat(F.round(x), 64n), SF.to_nat(SF.to_integral(F.Even{}, x), 64n), to_u64_value(F.round(x)), Equal.cong(F.F64, Result<&2, &2, NE.NumError, Nat>, y => SF.to_nat(y, 64n), F.round(x), SF.to_integral(F.Even{}, x), RI.round_value(x)))