proofs/math/typed/f64rint.bend

bend-collections-laws-math@1.0.0.0 · 267 lines · 27 definitions

1import Base
2import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
4import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
5import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
6import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
7import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
8import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
9import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
10import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
11import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
12import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
13import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
14import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH
15import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB
16import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64light.bend as FL
17import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR
18import bend-collections-laws-math@1.0.0.0/proofs/math/typed/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
32def 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
43def 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
62def b64v(+b: Bool) -> {SW.value(F.b64(b)) == SF.b2n(b) : Nat}:
63  match b:
64    case True{}:
65      {==}
66    case False{}:
67      {==}
68
69def b2n63(+b: Bool) -> {C.fits(63n, SF.b2n(b)) == True{} : Bool}:
70  match b:
71    case True{}:
72      {==}
73    case False{}:
74      {==}
75
76def 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
84def 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
87def 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
95def 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
102def 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
115def 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
118def 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
123def 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
130def 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
166def 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
170def 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
174def 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
187def 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
205def 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
213def 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
222def 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
225def 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
242def 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
253def 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
257def trunc_value(+x: F.F64) -> SF.Trunc.value(x):
258  ti_value(F.Trunc{}, x)
259
260def floor_value(+x: F.F64) -> SF.Floor.value(x):
261  ti_value(F.Floor{}, x)
262
263def ceil_value(+x: F.F64) -> SF.Ceil.value(x):
264  ti_value(F.Ceil{}, x)
265
266def round_value(+x: F.F64) -> SF.Round.value(x):
267  ti_value(F.Even{}, x)