proofs/math/typed/f64fmod.bend

bend-collections-laws-math@1.0.0.0 · 783 lines · 81 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/src/math/natural.bend as M
9import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
10import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
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/lib/lemmas/proofs/natural_division.bend as ND
13import bend-collections-laws-math@1.0.0.0/proofs/math/natural/misc.bend as MS
14import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
15import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
16import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH
17import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64dmrem.bend as DR
18import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64dmtop.bend as DQ
19import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB
20import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64light.bend as FL
21import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR
22import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend as RT
23import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64adda.bend as AA
24import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend as FC
25import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bl.bend as BL
26import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64tools.bend as T
27import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64exp.bend as EX
28
29# fmod and remainder (IEEE 754-2019 5.3.1 remainder; C99 7.12.10.1,
30# 7.12.10.2, F.9.7.1, F.9.7.2; python_style_math_stdlib_design.pdf 4.3):
31# Fmod.value, Remainder.value. Both are exact. The implementation divides
32# mant(x) 2^(e(x) - e(y)) by mant(y) ten bits at a time (fm_go); the loop
33# keeps r = N mod B and q = N div B (mod 2) for the dividend N consumed so
34# far (Knuth, TAOCP vol. 2, 4.3.1, long division; the invariant is
35# (N 2^t) mod B = ((N mod B) 2^t) mod B), so it ends with the spec's
36# A mod B and the parity of A div B that rounding to nearest-even needs.
37
38# ---- division on Nat ----
39
40def mod_mul_add(+q: Nat, +bp: Nat, +y: Nat) -> {Nat.mod(Nat.add(Nat.mul(q, 1n+bp), y), 1n+bp) == Nat.mod(y, 1n+bp) : Nat}:
41  +B = Nat.add(1n, bp)
42  +Qy = Nat.div(y, B)
43  +Ry = Nat.mod(y, B)
44  +e1 = Equal.cong(Nat, Nat, t => Nat.add(Nat.mul(q, B), t), y, Nat.add(Nat.mul(Qy, B), Ry), MS.divmod_eq(y, bp))
45  +e2 = Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(q, B), Nat.mul(Qy, B)), Ry), Nat.add(Nat.mul(q, B), Nat.add(Nat.mul(Qy, B), Ry)), NA.add_assoc(Nat.mul(q, B), Nat.mul(Qy, B), Ry))
46  +e3 = Equal.cong(Nat, Nat, t => Nat.add(t, Ry), Nat.add(Nat.mul(q, B), Nat.mul(Qy, B)), Nat.mul(Nat.add(q, Qy), B), Equal.sym(Nat, Nat.mul(Nat.add(q, Qy), B), Nat.add(Nat.mul(q, B), Nat.mul(Qy, B)), NA.mul_add_right(q, Qy, B)))
47  +ee = Equal.trans(Nat, Nat.add(Nat.mul(q, B), y), Nat.add(Nat.mul(q, B), Nat.add(Nat.mul(Qy, B), Ry)), Nat.add(Nat.mul(Nat.add(q, Qy), B), Ry), e1, Equal.trans(Nat, Nat.add(Nat.mul(q, B), Nat.add(Nat.mul(Qy, B), Ry)), Nat.add(Nat.add(Nat.mul(q, B), Nat.mul(Qy, B)), Ry), Nat.add(Nat.mul(Nat.add(q, Qy), B), Ry), e2, e3))
48  +hR = N.lt_succ_le(Ry, bp, MS.divmod_lt(y, bp))
49  Equal.trans(Nat, Nat.mod(Nat.add(Nat.mul(q, B), y), B), Nat.mod(Nat.add(Nat.mul(Nat.add(q, Qy), B), Ry), B), Ry, Equal.cong(Nat, Nat, t => Nat.mod(t, B), Nat.add(Nat.mul(q, B), y), Nat.add(Nat.mul(Nat.add(q, Qy), B), Ry), ee), ND.remainder(Nat.add(q, Qy), bp, Ry, hR))
50
51def div_mul_add(+q: Nat, +bp: Nat, +y: Nat) -> {Nat.div(Nat.add(Nat.mul(q, 1n+bp), y), 1n+bp) == Nat.add(q, Nat.div(y, 1n+bp)) : Nat}:
52  +B = Nat.add(1n, bp)
53  +Qy = Nat.div(y, B)
54  +Ry = Nat.mod(y, B)
55  +e1 = Equal.cong(Nat, Nat, t => Nat.add(Nat.mul(q, B), t), y, Nat.add(Nat.mul(Qy, B), Ry), MS.divmod_eq(y, bp))
56  +e2 = Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(q, B), Nat.mul(Qy, B)), Ry), Nat.add(Nat.mul(q, B), Nat.add(Nat.mul(Qy, B), Ry)), NA.add_assoc(Nat.mul(q, B), Nat.mul(Qy, B), Ry))
57  +e3 = Equal.cong(Nat, Nat, t => Nat.add(t, Ry), Nat.add(Nat.mul(q, B), Nat.mul(Qy, B)), Nat.mul(Nat.add(q, Qy), B), Equal.sym(Nat, Nat.mul(Nat.add(q, Qy), B), Nat.add(Nat.mul(q, B), Nat.mul(Qy, B)), NA.mul_add_right(q, Qy, B)))
58  +ee = Equal.trans(Nat, Nat.add(Nat.mul(q, B), y), Nat.add(Nat.mul(q, B), Nat.add(Nat.mul(Qy, B), Ry)), Nat.add(Nat.mul(Nat.add(q, Qy), B), Ry), e1, Equal.trans(Nat, Nat.add(Nat.mul(q, B), Nat.add(Nat.mul(Qy, B), Ry)), Nat.add(Nat.add(Nat.mul(q, B), Nat.mul(Qy, B)), Ry), Nat.add(Nat.mul(Nat.add(q, Qy), B), Ry), e2, e3))
59  +hR = N.lt_succ_le(Ry, bp, MS.divmod_lt(y, bp))
60  Equal.trans(Nat, Nat.div(Nat.add(Nat.mul(q, B), y), B), Nat.div(Nat.add(Nat.mul(Nat.add(q, Qy), B), Ry), B), Nat.add(q, Qy), Equal.cong(Nat, Nat, t => Nat.div(t, B), Nat.add(Nat.mul(q, B), y), Nat.add(Nat.mul(Nat.add(q, Qy), B), Ry), ee), ND.quotient(Nat.add(q, Qy), bp, Ry, hR))
61
62# N 2^t = (Q 2^t) B + r 2^t for N = Q B + r
63def shq(+N0: Nat, +bp: Nat, +t: Nat) -> {C.shift(t, N0) == Nat.add(Nat.mul(C.shift(t, Nat.div(N0, 1n+bp)), 1n+bp), C.shift(t, Nat.mod(N0, 1n+bp))) : Nat}:
64  +B = Nat.add(1n, bp)
65  +Q = Nat.div(N0, B)
66  +r = Nat.mod(N0, B)
67  +e1 = Equal.cong(Nat, Nat, u => C.shift(t, u), N0, Nat.add(Nat.mul(Q, B), r), MS.divmod_eq(N0, bp))
68  +e2 = WW.shift_add(t, Nat.mul(Q, B), r)
69  +e3 = Equal.cong(Nat, Nat, u => Nat.add(u, C.shift(t, r)), C.shift(t, Nat.mul(Q, B)), Nat.mul(C.shift(t, Q), B), Equal.sym(Nat, Nat.mul(C.shift(t, Q), B), C.shift(t, Nat.mul(Q, B)), WW.shift_mul_l(t, Q, B)))
70  Equal.trans(Nat, C.shift(t, N0), C.shift(t, Nat.add(Nat.mul(Q, B), r)), Nat.add(Nat.mul(C.shift(t, Q), B), C.shift(t, r)), e1, Equal.trans(Nat, C.shift(t, Nat.add(Nat.mul(Q, B), r)), Nat.add(C.shift(t, Nat.mul(Q, B)), C.shift(t, r)), Nat.add(Nat.mul(C.shift(t, Q), B), C.shift(t, r)), e2, e3))
71
72def mod_shift(+N0: Nat, +bp: Nat, +t: Nat) -> {Nat.mod(C.shift(t, Nat.mod(N0, 1n+bp)), 1n+bp) == Nat.mod(C.shift(t, N0), 1n+bp) : Nat}:
73  +B = Nat.add(1n, bp)
74  +e1 = Equal.cong(Nat, Nat, u => Nat.mod(u, B), C.shift(t, N0), Nat.add(Nat.mul(C.shift(t, Nat.div(N0, B)), B), C.shift(t, Nat.mod(N0, B))), shq(N0, bp, t))
75  Equal.sym(Nat, Nat.mod(C.shift(t, N0), B), Nat.mod(C.shift(t, Nat.mod(N0, B)), B), Equal.trans(Nat, Nat.mod(C.shift(t, N0), B), Nat.mod(Nat.add(Nat.mul(C.shift(t, Nat.div(N0, B)), B), C.shift(t, Nat.mod(N0, B))), B), Nat.mod(C.shift(t, Nat.mod(N0, B)), B), e1, mod_mul_add(C.shift(t, Nat.div(N0, B)), bp, C.shift(t, Nat.mod(N0, B)))))
76
77# the quotient's parity after at least one more bit
78def par_shift(+N0: Nat, +bp: Nat, +p: Nat) -> {Nat.mod(Nat.div(C.shift(1n+p, Nat.mod(N0, 1n+bp)), 1n+bp), 2n) == Nat.mod(Nat.div(C.shift(1n+p, N0), 1n+bp), 2n) : Nat}:
79  +B = Nat.add(1n, bp)
80  +t = Nat.add(1n, p)
81  +Q = Nat.div(N0, B)
82  +D = Nat.div(C.shift(t, Nat.mod(N0, B)), B)
83  +e1 = Equal.cong(Nat, Nat, u => Nat.div(u, B), C.shift(t, N0), Nat.add(Nat.mul(C.shift(t, Q), B), C.shift(t, Nat.mod(N0, B))), shq(N0, bp, t))
84  +e2 = div_mul_add(C.shift(t, Q), bp, C.shift(t, Nat.mod(N0, B)))
85  +e3 = NA.add_comm(C.shift(t, Q), D)
86  +ed = Equal.trans(Nat, Nat.div(C.shift(t, N0), B), Nat.div(Nat.add(Nat.mul(C.shift(t, Q), B), C.shift(t, Nat.mod(N0, B))), B), Nat.add(D, C.shift(t, Q)), e1, Equal.trans(Nat, Nat.div(Nat.add(Nat.mul(C.shift(t, Q), B), C.shift(t, Nat.mod(N0, B))), B), Nat.add(C.shift(t, Q), D), Nat.add(D, C.shift(t, Q)), e2, e3))
87  +e4 = Equal.cong(Nat, Nat, u => Nat.mod(u, 2n), Nat.div(C.shift(t, N0), B), Nat.add(D, C.shift(t, Q)), ed)
88  Equal.sym(Nat, Nat.mod(Nat.div(C.shift(t, N0), B), 2n), Nat.mod(D, 2n), Equal.trans(Nat, Nat.mod(Nat.div(C.shift(t, N0), B), 2n), Nat.mod(Nat.add(D, C.shift(t, Q)), 2n), Nat.mod(D, 2n), e4, WW.odd_limb(p, D, Q)))
89
90def min_le_r(+a: Nat, +b: Nat) -> {Nat.is_le(Nat.min(a, b), b) == True{} : Bool}:
91  match a b:
92    case 0n _:
93      N.zero_le(b)
94    case 1n+ +ap 0n:
95      {==}
96    case 1n+ +ap 1n+ +bp:
97      min_le_r(ap, bp)
98
99def min_le_l(+a: Nat, +b: Nat) -> {Nat.is_le(Nat.min(a, b), a) == True{} : Bool}:
100  match a b:
101    case 0n _:
102      {==}
103    case 1n+ +ap 0n:
104      {==}
105    case 1n+ +ap 1n+ +bp:
106      min_le_l(ap, bp)
107
108# ---- one step of the loop ----
109
110def rfit(+bp: Nat, +hB: {C.fits(53n, 1n+bp) == True{} : Bool}, +rw: WU.U64, +N0: Nat, +hr: {SW.value(rw) == Nat.mod(N0, 1n+bp) : Nat}) -> {C.fits(53n, SW.value(rw)) == True{} : Bool}:
111  +f = SH.fits_lek(53n, Nat.mod(N0, 1n+bp), 1n+bp, N.lt_le(Nat.mod(N0, 1n+bp), 1n+bp, MS.divmod_lt(N0, bp)), hB)
112  L.subst(Nat, u => {C.fits(53n, u) == True{} : Bool}, Nat.mod(N0, 1n+bp), SW.value(rw), Equal.sym(Nat, SW.value(rw), Nat.mod(N0, 1n+bp), hr), f)
113
114def shl_t(+rw: WU.U64, +t: Nat, +ht: {Nat.is_le(t, 10n) == True{} : Bool}, +hf: {C.fits(53n, SW.value(rw)) == True{} : Bool}) -> {SW.value(X.shl(rw, t)) == C.shift(t, SW.value(rw)) : Nat}:
115  +hk = N.le_lt_trans(t, 10n, 64n, ht, {==})
116  +hj = N.le_trans(Nat.add(t, 53n), Nat.add(10n, 53n), 64n, Equal.trans(Bool, Nat.is_le(Nat.add(t, 53n), Nat.add(10n, 53n)), Nat.is_le(t, 10n), True{}, FR.le_cancel_r(t, 10n, 53n), ht), {==})
117  FL.shl_v(rw, t, 53n, hk, hj, hf)
118
119def step_r(+b: WU.U64, +bp: Nat, +eB: {SW.value(b) == 1n+bp : Nat}, +hB: {C.fits(53n, 1n+bp) == True{} : Bool}, +hbz: {X.is_zero(b) == False{} : Bool}, +rw: WU.U64, +N0: Nat, +t: Nat, +ht: {Nat.is_le(t, 10n) == True{} : Bool}, +hr: {SW.value(rw) == Nat.mod(N0, 1n+bp) : Nat}) -> {SW.value(X.psnd(X.divmod(X.shl(rw, t), b))) == Nat.mod(C.shift(t, N0), 1n+bp) : Nat}:
120  +A = X.shl(rw, t)
121  +eA = shl_t(rw, t, ht, rfit(bp, hB, rw, N0, hr))
122  +e2 = Equal.cong(Nat, Nat, u => Nat.mod(u, SW.value(b)), SW.value(A), C.shift(t, SW.value(rw)), eA)
123  +e3 = Equal.cong(Nat, Nat, u => Nat.mod(C.shift(t, u), SW.value(b)), SW.value(rw), Nat.mod(N0, 1n+bp), hr)
124  +e4 = Equal.cong(Nat, Nat, u => Nat.mod(C.shift(t, Nat.mod(N0, 1n+bp)), u), SW.value(b), 1n+bp, eB)
125  +m1 = Nat.mod(SW.value(A), SW.value(b))
126  +m2 = Nat.mod(C.shift(t, SW.value(rw)), SW.value(b))
127  +m3 = Nat.mod(C.shift(t, Nat.mod(N0, 1n+bp)), SW.value(b))
128  +m4 = Nat.mod(C.shift(t, Nat.mod(N0, 1n+bp)), 1n+bp)
129  +m5 = Nat.mod(C.shift(t, N0), 1n+bp)
130  Equal.trans(Nat, SW.value(X.rem(A, b)), m1, m5, DR.divmod_rem(A, b, hbz), Equal.trans(Nat, m1, m2, m5, e2, Equal.trans(Nat, m2, m3, m5, e3, Equal.trans(Nat, m3, m4, m5, e4, mod_shift(N0, bp, t)))))
131
132def step_q(+b: WU.U64, +bp: Nat, +eB: {SW.value(b) == 1n+bp : Nat}, +hB: {C.fits(53n, 1n+bp) == True{} : Bool}, +hbz: {X.is_zero(b) == False{} : Bool}, +rw: WU.U64, +N0: Nat, +p: Nat, +ht: {Nat.is_le(1n+p, 10n) == True{} : Bool}, +hr: {SW.value(rw) == Nat.mod(N0, 1n+bp) : Nat}) -> {Nat.mod(SW.value(X.pfst(X.divmod(X.shl(rw, 1n+p), b))), 2n) == Nat.mod(Nat.div(C.shift(1n+p, N0), 1n+bp), 2n) : Nat}:
133  +A = X.shl(rw, 1n+p)
134  +eA = shl_t(rw, 1n+p, ht, rfit(bp, hB, rw, N0, hr))
135  +e2 = Equal.cong(Nat, Nat, u => Nat.div(u, SW.value(b)), SW.value(A), C.shift(1n+p, SW.value(rw)), eA)
136  +e3 = Equal.cong(Nat, Nat, u => Nat.div(C.shift(1n+p, u), SW.value(b)), SW.value(rw), Nat.mod(N0, 1n+bp), hr)
137  +e4 = Equal.cong(Nat, Nat, u => Nat.div(C.shift(1n+p, Nat.mod(N0, 1n+bp)), u), SW.value(b), 1n+bp, eB)
138  +d1 = Nat.div(SW.value(A), SW.value(b))
139  +d2 = Nat.div(C.shift(1n+p, SW.value(rw)), SW.value(b))
140  +d3 = Nat.div(C.shift(1n+p, Nat.mod(N0, 1n+bp)), SW.value(b))
141  +d4 = Nat.div(C.shift(1n+p, Nat.mod(N0, 1n+bp)), 1n+bp)
142  +ed = Equal.trans(Nat, SW.value(X.quot(A, b)), d1, d4, DQ.divmod_quot(A, b, hbz), Equal.trans(Nat, d1, d2, d4, e2, Equal.trans(Nat, d2, d3, d4, e3, e4)))
143  Equal.trans(Nat, Nat.mod(SW.value(X.quot(A, b)), 2n), Nat.mod(d4, 2n), Nat.mod(Nat.div(C.shift(1n+p, N0), 1n+bp), 2n), Equal.cong(Nat, Nat, u => Nat.mod(u, 2n), SW.value(X.quot(A, b)), d4, ed), par_shift(N0, bp, p))
144
145# ---- the loop ----
146
147def shc(+e: Nat, +t: Nat, +N0: Nat, +h: {Nat.is_le(t, 1n+e) == True{} : Bool}) -> {C.shift(Nat.sub(1n+e, t), C.shift(t, N0)) == C.shift(1n+e, N0) : Nat}:
148  +es = Equal.trans(Nat, Nat.add(Nat.sub(1n+e, t), t), Nat.add(t, Nat.sub(1n+e, t)), 1n+e, NA.add_comm(Nat.sub(1n+e, t), t), N.sub_add(1n+e, t, h))
149  Equal.trans(Nat, C.shift(Nat.sub(1n+e, t), C.shift(t, N0)), C.shift(Nat.add(Nat.sub(1n+e, t), t), N0), C.shift(1n+e, N0), Equal.sym(Nat, C.shift(Nat.add(Nat.sub(1n+e, t), t), N0), C.shift(Nat.sub(1n+e, t), C.shift(t, N0)), WW.shift_comp(Nat.sub(1n+e, t), t, N0)), Equal.cong(Nat, Nat, u => C.shift(u, N0), Nat.add(Nat.sub(1n+e, t), t), 1n+e, es))
150
151def eta(p: WU.U64 & WU.U64) -> {p == (X.pfst(p), X.psnd(p)) : WU.U64 & WU.U64}:
152  match p:
153    case (a, b):
154      {==}
155
156def loop_r(fuel: Nat, +b: WU.U64, +bp: Nat, +eB: {SW.value(b) == 1n+bp : Nat}, +hB: {C.fits(53n, 1n+bp) == True{} : Bool}, +hbz: {X.is_zero(b) == False{} : Bool}, +d: Nat, +hd: {Nat.is_le(d, fuel) == True{} : Bool}, +q: WU.U64, +r: WU.U64, +N0: Nat, +hr: {SW.value(r) == Nat.mod(N0, 1n+bp) : Nat}) -> {SW.value(X.psnd(F.fm_go(fuel, b, d, (q, r)))) == Nat.mod(C.shift(d, N0), 1n+bp) : Nat}:
157  match fuel d:
158    case 0n 0n:
159      hr
160    case 0n 1n+ +e:
161      Empty.absurd({SW.value(X.psnd(F.fm_go(0n, b, 1n+e, (q, r)))) == Nat.mod(C.shift(1n+e, N0), 1n+bp) : Nat}, FL.true_ne_false(Equal.sym(Bool, False{}, True{}, hd)))
162    case 1n+ +f 0n:
163      hr
164    case 1n+ +f 1n+ +e:
165      +t = Nat.min(1n+e, 10n)
166      +d2 = Nat.sub(1n+e, t)
167      +hr2 = step_r(b, bp, eB, hB, hbz, r, N0, t, min_le_r(1n+e, 10n), hr)
168      +hd2 = N.le_trans(Nat.sub(e, Nat.min(e, 9n)), e, f, EX.sub_le_self(e, Nat.min(e, 9n)), hd)
169      +ee = Equal.cong(WU.U64 & WU.U64, Nat, u => SW.value(X.psnd(F.fm_go(f, b, d2, u))), X.divmod(X.shl(r, t), b), (X.pfst(X.divmod(X.shl(r, t), b)), X.psnd(X.divmod(X.shl(r, t), b))), eta(X.divmod(X.shl(r, t), b)))
170      +rec = loop_r(f, b, bp, eB, hB, hbz, d2, hd2, X.pfst(X.divmod(X.shl(r, t), b)), X.psnd(X.divmod(X.shl(r, t), b)), C.shift(t, N0), hr2)
171      +es = Equal.cong(Nat, Nat, u => Nat.mod(u, 1n+bp), C.shift(d2, C.shift(t, N0)), C.shift(1n+e, N0), shc(e, t, N0, min_le_l(1n+e, 10n)))
172      Equal.trans(Nat, SW.value(X.psnd(F.fm_go(f, b, d2, X.divmod(X.shl(r, t), b)))), SW.value(X.psnd(F.fm_go(f, b, d2, (X.pfst(X.divmod(X.shl(r, t), b)), X.psnd(X.divmod(X.shl(r, t), b)))))), Nat.mod(C.shift(1n+e, N0), 1n+bp), ee, Equal.trans(Nat, SW.value(X.psnd(F.fm_go(f, b, d2, (X.pfst(X.divmod(X.shl(r, t), b)), X.psnd(X.divmod(X.shl(r, t), b)))))), Nat.mod(C.shift(d2, C.shift(t, N0)), 1n+bp), Nat.mod(C.shift(1n+e, N0), 1n+bp), rec, es))
173
174def loop_q(fuel: Nat, +b: WU.U64, +bp: Nat, +eB: {SW.value(b) == 1n+bp : Nat}, +hB: {C.fits(53n, 1n+bp) == True{} : Bool}, +hbz: {X.is_zero(b) == False{} : Bool}, +d: Nat, +hd: {Nat.is_le(d, fuel) == True{} : Bool}, +q: WU.U64, +r: WU.U64, +N0: Nat, +hr: {SW.value(r) == Nat.mod(N0, 1n+bp) : Nat}, +hq: {Nat.mod(SW.value(q), 2n) == Nat.mod(Nat.div(N0, 1n+bp), 2n) : Nat}) -> {Nat.mod(SW.value(X.pfst(F.fm_go(fuel, b, d, (q, r)))), 2n) == Nat.mod(Nat.div(C.shift(d, N0), 1n+bp), 2n) : Nat}:
175  match fuel d:
176    case 0n 0n:
177      hq
178    case 0n 1n+ +e:
179      Empty.absurd({Nat.mod(SW.value(X.pfst(F.fm_go(0n, b, 1n+e, (q, r)))), 2n) == Nat.mod(Nat.div(C.shift(1n+e, N0), 1n+bp), 2n) : Nat}, FL.true_ne_false(Equal.sym(Bool, False{}, True{}, hd)))
180    case 1n+ +f 0n:
181      hq
182    case 1n+ +f 1n+ +e:
183      +t = Nat.min(1n+e, 10n)
184      +d2 = Nat.sub(1n+e, t)
185      +hr2 = step_r(b, bp, eB, hB, hbz, r, N0, t, min_le_r(1n+e, 10n), hr)
186      +hq2 = step_q(b, bp, eB, hB, hbz, r, N0, Nat.min(e, 9n), min_le_r(e, 9n), hr)
187      +hd2 = N.le_trans(Nat.sub(e, Nat.min(e, 9n)), e, f, EX.sub_le_self(e, Nat.min(e, 9n)), hd)
188      +ee = Equal.cong(WU.U64 & WU.U64, Nat, u => Nat.mod(SW.value(X.pfst(F.fm_go(f, b, d2, u))), 2n), X.divmod(X.shl(r, t), b), (X.pfst(X.divmod(X.shl(r, t), b)), X.psnd(X.divmod(X.shl(r, t), b))), eta(X.divmod(X.shl(r, t), b)))
189      +rec = loop_q(f, b, bp, eB, hB, hbz, d2, hd2, X.pfst(X.divmod(X.shl(r, t), b)), X.psnd(X.divmod(X.shl(r, t), b)), C.shift(t, N0), hr2, hq2)
190      +es = Equal.cong(Nat, Nat, u => Nat.mod(Nat.div(u, 1n+bp), 2n), C.shift(d2, C.shift(t, N0)), C.shift(1n+e, N0), shc(e, t, N0, min_le_l(1n+e, 10n)))
191      Equal.trans(Nat, Nat.mod(SW.value(X.pfst(F.fm_go(f, b, d2, X.divmod(X.shl(r, t), b)))), 2n), Nat.mod(SW.value(X.pfst(F.fm_go(f, b, d2, (X.pfst(X.divmod(X.shl(r, t), b)), X.psnd(X.divmod(X.shl(r, t), b)))))), 2n), Nat.mod(Nat.div(C.shift(1n+e, N0), 1n+bp), 2n), ee, Equal.trans(Nat, Nat.mod(SW.value(X.pfst(F.fm_go(f, b, d2, (X.pfst(X.divmod(X.shl(r, t), b)), X.psnd(X.divmod(X.shl(r, t), b)))))), 2n), Nat.mod(Nat.div(C.shift(d2, C.shift(t, N0)), 1n+bp), 2n), Nat.mod(Nat.div(C.shift(1n+e, N0), 1n+bp), 2n), rec, es))
192
193# ---- a finite double is the round of its own significand and scale ----
194
195def v(+x: U32) -> Nat:
196  U32.to_nat(x)
197
198def dec(+x: F.F64) -> {x == SF.encode(SF.sign(x), SF.efield(x), SF.frac(x)) : F.F64}:
199  match x:
200    case F.Bits{+l, +h}:
201      +H = v(h)
202      +H20 = C.high(20n, H)
203      +e1 = WW.low_high(20n, H)
204      +e2 = Equal.cong(Nat, Nat, t => Nat.add(C.low(20n, H), C.shift(20n, t)), H20, Nat.add(C.low(11n, H20), C.shift(11n, C.high(11n, H20))), WW.low_high(11n, H20))
205      +e3 = Equal.trans(Nat, C.high(11n, H20), C.high(31n, H), SF.b2n(SF.sign(F.Bits{l, h})), Equal.sym(Nat, C.high(Nat.add(20n, 11n), H), C.high(11n, H20), WW.high_comp(11n, 20n, H)), FB.bit_c(C.high(31n, H), FB.half0(h)))
206      +e4 = Equal.cong(Nat, Nat, t => Nat.add(C.low(20n, H), C.shift(20n, Nat.add(C.low(11n, H20), C.shift(11n, t)))), C.high(11n, H20), SF.b2n(SF.sign(F.Bits{l, h})), e3)
207      +a1 = Nat.add(C.low(20n, H), C.shift(20n, H20))
208      +a2 = Nat.add(C.low(20n, H), C.shift(20n, Nat.add(C.low(11n, H20), C.shift(11n, C.high(11n, H20)))))
209      +a3 = Nat.add(C.low(20n, H), C.shift(20n, Nat.add(C.low(11n, H20), C.shift(11n, SF.b2n(SF.sign(F.Bits{l, h}))))))
210      FB.enc_g(l, h, SF.sign(F.Bits{l, h}), h, Equal.trans(Nat, H, a1, a3, e1, Equal.trans(Nat, a1, a2, a3, e2, e4)))
211
212# a significand of at most 52 bits at its own ulp u encodes as a subnormal;
213# u stays abstract, so pack's exponent arithmetic is never evaluated on a
214# literal (rt_sub instantiates u = 1926)
215def ru_self(+s: Bool, +Fr: Nat, +u: Nat, +hF: {C.fits(52n, Fr) == True{} : Bool}) -> {SF.round_u(s, Fr, u, u) == SF.encode(s, 0n, Fr) : F.F64}:
216  +f53 = SH.fits_mono(52n, 53n, Fr, {==}, hF)
217  +l1 = EX.ru(s, Fr, u, u)
218  +l2 = Equal.cong(Bool, F.F64, b => SF.pack(s, SF.pick(Nat, b, SF.rne(Fr, Nat.sub(u, u)), C.shift(Nat.sub(u, u), Fr)), u), Nat.is_le(u, u), True{}, N.le_refl(u))
219  +l3 = Equal.cong(Nat, F.F64, t => SF.pack(s, SF.rne(Fr, t), u), Nat.sub(u, u), 0n, N.sub_self(u))
220  +l4 = Equal.cong(Bool, F.F64, b => SF.pick(F.F64, b, SF.pack_n(s, Fr, u), SF.pack_e(s, Nat.sub(Nat.add(1n+u, 1075n), SF.zb()), 0n)), C.fits(53n, Fr), True{}, f53)
221  +l5 = Equal.cong(Bool, F.F64, b => SF.pick(F.F64, b, SF.encode(s, 0n, Fr), SF.pack_e(s, Nat.sub(Nat.add(u, 1075n), SF.zb()), C.low(52n, Fr))), C.fits(52n, Fr), True{}, hF)
222  +p1 = SF.pack(s, SF.pick(Nat, Nat.is_le(u, u), SF.rne(Fr, Nat.sub(u, u)), C.shift(Nat.sub(u, u), Fr)), u)
223  +p2 = SF.pack(s, SF.rne(Fr, Nat.sub(u, u)), u)
224  +p3 = SF.pack(s, Fr, u)
225  +p4 = SF.pack_n(s, Fr, u)
226  +G = SF.encode(s, 0n, Fr)
227  Equal.trans(F.F64, SF.round_u(s, Fr, u, u), p1, G, l1, Equal.trans(F.F64, p1, p2, G, l2, Equal.trans(F.F64, p2, p3, G, l3, Equal.trans(F.F64, p3, p4, G, l4, l5))))
228
229def rt_sub(+s: Bool, +Fr: Nat, +hF: {C.fits(52n, Fr) == True{} : Bool}, +z: Bool, +hz: {Nat.is_eq(Fr, 0n) == z : Bool}) -> {SF.round(s, Fr, 1926n) == SF.encode(s, 0n, Fr) : F.F64}:
230  match z:
231    case True{}:
232      +e0 = N.eq_from_is_eq(Fr, 0n, hz)
233      +ea = Equal.cong(Nat, F.F64, t => SF.round(s, t, 1926n), Fr, 0n, e0)
234      +eb = Equal.trans(F.F64, SF.encode(s, 0n, 0n), FR.bits(s, 0n), SF.zero(s), FR.enc_bits(s, 0n, 0n), EX.bz(s))
235      +ec = Equal.cong(Nat, F.F64, t => SF.encode(s, 0n, t), 0n, Fr, Equal.sym(Nat, Fr, 0n, N.eq_from_is_eq(Fr, 0n, hz)))
236      Equal.trans(F.F64, SF.round(s, Fr, 1926n), SF.zero(s), SF.encode(s, 0n, Fr), ea, Equal.trans(F.F64, SF.zero(s), SF.encode(s, 0n, 0n), SF.encode(s, 0n, Fr), Equal.sym(F.F64, SF.encode(s, 0n, 0n), SF.zero(s), eb), ec))
237    case False{}:
238      +B = M.bit_length(Fr)
239      +A = Nat.sub(Nat.add(1926n, B), 53n)
240      +hB = BL.bl_le(52n, Fr, hF, Nat.is_le(B, 52n), {==})
241      +emax = EX.max_le(A, 1926n, N.le_trans(B, 52n, 53n, hB, {==}))
242      +e1 = Equal.cong(Bool, F.F64, b => SF.pick(F.F64, b, SF.zero(s), SF.round_u(s, Fr, 1926n, Nat.max(A, Nat.sub(SF.zb(), 1074n)))), Nat.is_eq(Fr, 0n), False{}, hz)
243      +e2 = Equal.cong(Nat, F.F64, u => SF.round_u(s, Fr, 1926n, u), Nat.max(A, 1926n), 1926n, emax)
244      +r1 = SF.round_u(s, Fr, 1926n, Nat.max(A, 1926n))
245      +r2 = SF.round_u(s, Fr, 1926n, 1926n)
246      Equal.trans(F.F64, SF.round(s, Fr, 1926n), r1, SF.encode(s, 0n, Fr), e1, Equal.trans(F.F64, r1, r2, SF.encode(s, 0n, Fr), e2, ru_self(s, Fr, 1926n, hF)))
247
248def rt_norm(+s: Bool, +E: Nat, +Fr: Nat, +one: Nat, +h1: {one == 1n : Nat}, +hE0: {Nat.is_eq(E, 0n) == False{} : Bool}, +hE: {Nat.is_lt(E, 2047n) == True{} : Bool}, +hF: {C.fits(52n, Fr) == True{} : Bool}) -> {SF.round(s, Nat.add(Fr, C.shift(52n, one)), Nat.add(1925n, E)) == SF.encode(s, E, Fr) : F.F64}:
249  +Mn = Nat.add(Fr, C.shift(52n, one))
250  +X0 = Nat.add(1925n, E)
251  +hz0 = Equal.trans(Bool, Nat.is_eq(Mn, 0n), Bool.and(Nat.is_eq(Fr, 0n), Nat.is_eq(one, 0n)), False{}, FB.z2(Fr, 52n, one), Equal.trans(Bool, Bool.and(Nat.is_eq(Fr, 0n), Nat.is_eq(one, 0n)), Bool.and(Nat.is_eq(Fr, 0n), False{}), False{}, Equal.cong(Nat, Bool, t => Bool.and(Nat.is_eq(Fr, 0n), Nat.is_eq(t, 0n)), one, 1n, h1), FR.and_f(Nat.is_eq(Fr, 0n))))
252  +ebl = FR.bl_c(52n, Mn, AA.n52(one, h1, Fr), AA.f53(one, h1, Fr, hF), Nat.cmp(M.bit_length(Mn), 53n), {==})
253  +emx = FR.max_l(X0, 1926n, FL.nz_le(E, hE0))
254  +e1 = Equal.cong(Bool, F.F64, b => SF.pick(F.F64, b, SF.zero(s), SF.round_u(s, Mn, X0, Nat.max(Nat.sub(Nat.add(X0, M.bit_length(Mn)), 53n), Nat.sub(SF.zb(), 1074n)))), Nat.is_eq(Mn, 0n), False{}, hz0)
255  +e2 = Equal.cong(Nat, F.F64, t => SF.round_u(s, Mn, X0, Nat.max(Nat.sub(Nat.add(X0, t), 53n), 1926n)), M.bit_length(Mn), 53n, ebl)
256  +e3 = Equal.cong(Nat, F.F64, t => SF.round_u(s, Mn, X0, Nat.max(t, 1926n)), Nat.sub(Nat.add(X0, 53n), 53n), X0, FR.sub_add_l(X0, 53n))
257  +e4 = Equal.cong(Nat, F.F64, t => SF.round_u(s, Mn, X0, t), Nat.max(X0, 1926n), X0, emx)
258  +e5 = Equal.cong(Bool, F.F64, b => SF.pack(s, SF.pick(Nat, b, SF.rne(Mn, Nat.sub(X0, X0)), C.shift(Nat.sub(X0, X0), Mn)), X0), Nat.is_le(X0, X0), True{}, N.le_refl(X0))
259  +e6 = Equal.cong(Nat, F.F64, t => SF.pack(s, SF.rne(Mn, t), X0), Nat.sub(X0, X0), 0n, N.sub_self(X0))
260  +e7 = Equal.cong(Bool, F.F64, b => SF.pick(F.F64, b, SF.pack_n(s, Mn, X0), SF.pack_e(s, Nat.sub(Nat.add(1n+X0, 1075n), SF.zb()), 0n)), C.fits(53n, Mn), True{}, AA.f53(one, h1, Fr, hF))
261  +e8 = Equal.cong(Bool, F.F64, b => SF.pick(F.F64, b, SF.encode(s, 0n, Mn), SF.pack_e(s, Nat.sub(Nat.add(X0, 1075n), SF.zb()), C.low(52n, Mn))), C.fits(52n, Mn), False{}, AA.n52(one, h1, Fr))
262  +e9 = Equal.cong(Nat, F.F64, t => SF.pack_e(s, t, C.low(52n, Mn)), Nat.sub(Nat.add(X0, 1075n), SF.zb()), E, FR.sub_add_l(E, 1075n))
263  +e10 = Equal.cong(Nat, F.F64, t => SF.pack_e(s, E, t), C.low(52n, Mn), Fr, WW.low_u(52n, Fr, one, hF))
264  +e11 = Equal.cong(Bool, F.F64, b => SF.pick(F.F64, b, SF.inf(s), SF.encode(s, E, Fr)), Nat.is_le(2047n, E), False{}, N.lt_not_le(E, 2047n, hE))
265  +r1 = SF.round_u(s, Mn, X0, Nat.max(Nat.sub(Nat.add(X0, M.bit_length(Mn)), 53n), 1926n))
266  +r2 = SF.round_u(s, Mn, X0, Nat.max(Nat.sub(Nat.add(X0, 53n), 53n), 1926n))
267  +r3 = SF.round_u(s, Mn, X0, Nat.max(X0, 1926n))
268  +r4 = SF.round_u(s, Mn, X0, X0)
269  +r5 = SF.pack(s, SF.rne(Mn, Nat.sub(X0, X0)), X0)
270  +r6 = SF.pack(s, Mn, X0)
271  +r7 = SF.pack_n(s, Mn, X0)
272  +r8 = SF.pack_e(s, Nat.sub(Nat.add(X0, 1075n), SF.zb()), C.low(52n, Mn))
273  +r9 = SF.pack_e(s, E, C.low(52n, Mn))
274  +r10 = SF.pack_e(s, E, Fr)
275  +G = SF.encode(s, E, Fr)
276  Equal.trans(F.F64, SF.round(s, Mn, X0), r1, G, e1, Equal.trans(F.F64, r1, r2, G, e2, Equal.trans(F.F64, r2, r3, G, e3, Equal.trans(F.F64, r3, r4, G, e4, Equal.trans(F.F64, r4, r5, G, e5, Equal.trans(F.F64, r5, r6, G, e6, Equal.trans(F.F64, r6, r7, G, e7, Equal.trans(F.F64, r7, r8, G, e8, Equal.trans(F.F64, r8, r9, G, e9, Equal.trans(F.F64, r9, r10, G, e10, e11))))))))))
277
278def frac52(+x: F.F64) -> {C.fits(52n, SF.frac(x)) == True{} : Bool}:
279  match x:
280    case F.Bits{+xl, +xh}:
281      FL.hF(xl, xh)
282
283def rt_c(+x: F.F64, +hfin: {Nat.is_lt(SF.efield(x), 2047n) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +z: Bool, +hz: {Nat.is_eq(SF.efield(x), 0n) == z : Bool}) -> {SF.round(SF.sign(x), SF.mant(x), SF.xexp(x)) == x : F.F64}:
284  match z:
285    case True{}:
286      +s = SF.sign(x)
287      +E = SF.efield(x)
288      +Fr = SF.frac(x)
289      +e1 = Equal.cong(Bool, F.F64, b => SF.round(s, Nat.add(Fr, C.shift(52n, SF.b2n(Bool.not(b)))), SF.pick(Nat, b, Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n))), Nat.is_eq(E, 0n), True{}, hz)
290      +e2 = Equal.cong(Nat, F.F64, t => SF.round(s, t, 1926n), Nat.add(Fr, 0n), Fr, N.add_zero(Fr))
291      +e3 = rt_sub(s, Fr, frac52(x), Nat.is_eq(Fr, 0n), {==})
292      +e4 = Equal.cong(Nat, F.F64, t => SF.encode(s, t, Fr), 0n, E, Equal.sym(Nat, E, 0n, N.eq_from_is_eq(E, 0n, hz)))
293      +e5 = Equal.sym(F.F64, x, SF.encode(s, E, Fr), dec(x))
294      Equal.trans(F.F64, SF.round(s, SF.mant(x), SF.xexp(x)), SF.round(s, Nat.add(Fr, 0n), 1926n), x, e1, Equal.trans(F.F64, SF.round(s, Nat.add(Fr, 0n), 1926n), SF.round(s, Fr, 1926n), x, e2, Equal.trans(F.F64, SF.round(s, Fr, 1926n), SF.encode(s, 0n, Fr), x, e3, Equal.trans(F.F64, SF.encode(s, 0n, Fr), SF.encode(s, E, Fr), x, e4, e5))))
295    case False{}:
296      +s = SF.sign(x)
297      +E = SF.efield(x)
298      +Fr = SF.frac(x)
299      +eb = Equal.trans(Nat, SF.b2n(Bool.not(Nat.is_eq(E, 0n))), 1n, one, Equal.cong(Bool, Nat, b => SF.b2n(Bool.not(b)), Nat.is_eq(E, 0n), False{}, hz), Equal.sym(Nat, one, 1n, h1))
300      +e1 = Equal.cong(Nat, F.F64, t => SF.round(s, Nat.add(Fr, C.shift(52n, t)), SF.xexp(x)), SF.b2n(Bool.not(Nat.is_eq(E, 0n))), one, eb)
301      +e2 = Equal.cong(Bool, F.F64, b => SF.round(s, Nat.add(Fr, C.shift(52n, one)), SF.pick(Nat, b, Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n))), Nat.is_eq(E, 0n), False{}, hz)
302      +e3 = Equal.cong(Nat, F.F64, t => SF.round(s, Nat.add(Fr, C.shift(52n, one)), t), Nat.sub(Nat.add(E, SF.zb()), 1075n), Nat.add(1925n, E), FC.esub(E))
303      +e4 = rt_norm(s, E, Fr, one, h1, hz, hfin, frac52(x))
304      +e5 = Equal.sym(F.F64, x, SF.encode(s, E, Fr), dec(x))
305      +r1 = SF.round(s, Nat.add(Fr, C.shift(52n, one)), SF.xexp(x))
306      +r2 = SF.round(s, Nat.add(Fr, C.shift(52n, one)), Nat.sub(Nat.add(E, SF.zb()), 1075n))
307      +r3 = SF.round(s, Nat.add(Fr, C.shift(52n, one)), Nat.add(1925n, E))
308      Equal.trans(F.F64, SF.round(s, SF.mant(x), SF.xexp(x)), r1, x, e1, Equal.trans(F.F64, r1, r2, x, e2, Equal.trans(F.F64, r2, r3, x, e3, Equal.trans(F.F64, r3, SF.encode(s, E, Fr), x, e4, e5))))
309
310def rt(+x: F.F64, +hfin: {Nat.is_lt(SF.efield(x), 2047n) == True{} : Bool}) -> {SF.round(SF.sign(x), SF.mant(x), SF.xexp(x)) == x : F.F64}:
311  rt_c(x, hfin, 1n, {==}, Nat.is_eq(SF.efield(x), 0n), {==})
312
313# ---- the pieces of fmod ----
314
315def fin(+x: F.F64, +hn: {SF.is_nan(x) == False{} : Bool}, +hi: {SF.is_inf(x) == False{} : Bool}) -> {Nat.is_lt(SF.efield(x), 2047n) == True{} : Bool}:
316  match x:
317    case F.Bits{+xl, +xh}:
318      FC.lt2047(xl, xh, hi, hn)
319
320def mod_small(+a: Nat, +n: Nat, +h: {Nat.is_lt(a, n) == True{} : Bool}) -> {Nat.mod(a, n) == a : Nat}:
321  match n:
322    case 0n:
323      Empty.absurd({Nat.mod(a, 0n) == a : Nat}, N.lt_zero_absurd(a, h))
324    case 1n+ +np:
325      ND.remainder(0n, np, a, N.lt_succ_le(a, np, h))
326
327def div_small(+a: Nat, +n: Nat, +h: {Nat.is_lt(a, n) == True{} : Bool}) -> {Nat.div(a, n) == 0n : Nat}:
328  match n:
329    case 0n:
330      Empty.absurd({Nat.div(a, 0n) == 0n : Nat}, N.lt_zero_absurd(a, h))
331    case 1n+ +np:
332      ND.quotient(0n, np, a, N.lt_succ_le(a, np, h))
333
334def xge_c(+x: F.F64, +c: Bool, +hc: {Nat.is_eq(SF.efield(x), 0n) == c : Bool}) -> {Nat.is_le(1926n, SF.pick(Nat, c, Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(SF.efield(x), SF.zb()), 1075n))) == True{} : Bool}:
335  match c:
336    case True{}:
337      {==}
338    case False{}:
339      L.subst(Nat, t => {Nat.is_le(1926n, t) == True{} : Bool}, Nat.add(1925n, SF.efield(x)), Nat.sub(Nat.add(SF.efield(x), SF.zb()), 1075n), Equal.sym(Nat, Nat.sub(Nat.add(SF.efield(x), SF.zb()), 1075n), Nat.add(1925n, SF.efield(x)), FC.esub(SF.efield(x))), FL.nz_le(SF.efield(x), hc))
340
341def xge(+x: F.F64) -> {Nat.is_le(1926n, SF.xexp(x)) == True{} : Bool}:
342  xge_c(x, Nat.is_eq(SF.efield(x), 0n), {==})
343
344# a scale above another double's is a normal number's
345def yn_c(+x: F.F64, +y: F.F64, +hlt: {Nat.is_lt(SF.xexp(x), SF.xexp(y)) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(SF.efield(y), 0n) == c : Bool}) -> {c == False{} : Bool}:
346  match c:
347    case True{}:
348      +h1 = L.subst(Bool, b => {Nat.is_lt(SF.xexp(x), SF.pick(Nat, b, Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(SF.efield(y), SF.zb()), 1075n))) == True{} : Bool}, Nat.is_eq(SF.efield(y), 0n), True{}, hc, hlt)
349      +h2 = N.le_not_lt(SF.xexp(x), 1926n, xge(x))
350      Empty.absurd({True{} == False{} : Bool}, FL.true_ne_false(Equal.trans(Bool, True{}, Nat.is_lt(SF.xexp(x), 1926n), False{}, Equal.sym(Bool, Nat.is_lt(SF.xexp(x), 1926n), True{}, h1), h2)))
351    case False{}:
352      {==}
353
354def nf52(+y: F.F64, +hz: {Nat.is_eq(SF.efield(y), 0n) == False{} : Bool}) -> {C.fits(52n, SF.mant(y)) == False{} : Bool}:
355  AA.n52(SF.b2n(Bool.not(Nat.is_eq(SF.efield(y), 0n))), Equal.cong(Bool, Nat, b => SF.b2n(Bool.not(b)), Nat.is_eq(SF.efield(y), 0n), False{}, hz), SF.frac(y))
356
357# y's significand moved up by k >= 1 is at least 2^53 > mant(x)
358def far_lt(+x: F.F64, +y: F.F64, +hlt: {Nat.is_lt(SF.xexp(x), SF.xexp(y)) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_lt(SF.mant(x), C.shift(Nat.sub(SF.xexp(y), SF.xexp(x)), SF.mant(y))) == True{} : Bool}:
359  +k = Nat.sub(SF.xexp(y), SF.xexp(x))
360  +S = C.shift(k, SF.mant(y))
361  +hk = FR.lt_sub_pos(SF.xexp(x), SF.xexp(y), hlt)
362  +hy = yn_c(x, y, hlt, Nat.is_eq(SF.efield(y), 0n), {==})
363  +f1 = Equal.trans(Bool, C.fits(Nat.add(k, 52n), S), C.fits(52n, SF.mant(y)), False{}, RT.fits_sh(k, 52n, SF.mant(y)), nf52(y, hy))
364  +h53 = Equal.trans(Bool, Nat.is_le(Nat.add(1n, 52n), Nat.add(k, 52n)), Nat.is_le(1n, k), True{}, FR.le_cancel_r(1n, k, 52n), hk)
365  +f2 = FL.nfit_mono(53n, Nat.add(k, 52n), S, h53, f1)
366  +l1 = Equal.trans(Bool, Nat.is_lt(SF.mant(x), C.shift(53n, one)), C.fits(53n, SF.mant(x)), True{}, FR.lt_fit(53n, one, h1, SF.mant(x)), T.mant_fits(x))
367  +l2 = Equal.trans(Bool, Nat.is_le(C.shift(53n, one), S), Bool.not(C.fits(53n, S)), True{}, FB.le_fit(53n, one, h1, S), Equal.cong(Bool, Bool, b => Bool.not(b), C.fits(53n, S), False{}, f2))
368  N.lt_le_trans(SF.mant(x), C.shift(53n, one), S, l1, l2)
369
370def FM(+x: F.F64, +y: F.F64) -> F.F64:
371  SF.round(SF.sign(x), Nat.mod(SF.ra(x, y), SF.rb(x, y)), SF.rsc(x, y))
372
373# the spec's operands when x has the smaller scale
374def fm_far(+x: F.F64, +y: F.F64, +hlt: {Nat.is_lt(SF.xexp(x), SF.xexp(y)) == True{} : Bool}, +hfin: {Nat.is_lt(SF.efield(x), 2047n) == True{} : Bool}) -> {FM(x, y) == x : F.F64}:
375  +s = SF.sign(x)
376  +xx = SF.xexp(x)
377  +xy = SF.xexp(y)
378  +mx = SF.mant(x)
379  +my = SF.mant(y)
380  +S = C.shift(Nat.sub(xy, xx), my)
381  +e1 = Equal.cong(Nat, F.F64, t => SF.round(s, Nat.mod(C.shift(Nat.sub(xx, t), mx), C.shift(Nat.sub(xy, t), my)), t), Nat.min(xx, xy), xx, N.min_left(xx, xy, hlt))
382  +e2 = Equal.cong(Nat, F.F64, t => SF.round(s, Nat.mod(C.shift(t, mx), S), xx), Nat.sub(xx, xx), 0n, N.sub_self(xx))
383  +e3 = Equal.cong(Nat, F.F64, t => SF.round(s, t, xx), Nat.mod(mx, S), mx, mod_small(mx, S, far_lt(x, y, hlt, 1n, {==})))
384  +r1 = SF.round(s, Nat.mod(C.shift(Nat.sub(xx, xx), mx), S), xx)
385  +r2 = SF.round(s, Nat.mod(mx, S), xx)
386  Equal.trans(F.F64, FM(x, y), r1, x, e1, Equal.trans(F.F64, r1, r2, x, e2, Equal.trans(F.F64, r2, SF.round(s, mx, xx), x, e3, rt(x, hfin))))
387
388# a zero x
389def fm_zero(+x: F.F64, +y: F.F64, +hzx: {SF.is_zero(x) == True{} : Bool}, +hzy: {SF.is_zero(y) == False{} : Bool}, +hfin: {Nat.is_lt(SF.efield(x), 2047n) == True{} : Bool}) -> {FM(x, y) == x : F.F64}:
390  +s = SF.sign(x)
391  +em = N.eq_from_is_eq(SF.mant(x), 0n, Equal.trans(Bool, Nat.is_eq(SF.mant(x), 0n), SF.is_zero(x), True{}, T.mant_z(x), hzx))
392  +a = Nat.sub(SF.xexp(x), SF.rsc(x, y))
393  +rb = SF.rb(x, y)
394  +hmy = FL.nz_le(SF.mant(y), Equal.trans(Bool, Nat.is_eq(SF.mant(y), 0n), SF.is_zero(y), False{}, T.mant_z(y), hzy))
395  +hrb = N.succ_le_lt(0n, rb, N.le_trans(1n, SF.mant(y), rb, hmy, WW.shift_ge(Nat.sub(SF.xexp(y), SF.rsc(x, y)), SF.mant(y))))
396  +e1 = Equal.cong(Nat, F.F64, t => SF.round(s, Nat.mod(C.shift(a, t), rb), SF.rsc(x, y)), SF.mant(x), 0n, em)
397  +e2 = Equal.cong(Nat, F.F64, t => SF.round(s, Nat.mod(t, rb), SF.rsc(x, y)), C.shift(a, 0n), 0n, WW.shift_zero(a))
398  +e3 = Equal.cong(Nat, F.F64, t => SF.round(s, t, SF.rsc(x, y)), Nat.mod(0n, rb), 0n, mod_small(0n, rb, hrb))
399  +e4 = Equal.cong(Nat, F.F64, t => SF.round(s, t, SF.xexp(x)), 0n, SF.mant(x), Equal.sym(Nat, SF.mant(x), 0n, N.eq_from_is_eq(SF.mant(x), 0n, Equal.trans(Bool, Nat.is_eq(SF.mant(x), 0n), SF.is_zero(x), True{}, T.mant_z(x), hzx))))
400  +r1 = SF.round(s, Nat.mod(C.shift(a, 0n), rb), SF.rsc(x, y))
401  +r2 = SF.round(s, Nat.mod(0n, rb), SF.rsc(x, y))
402  +r3 = SF.round(s, 0n, SF.rsc(x, y))
403  +r4 = SF.round(s, 0n, SF.xexp(x))
404  Equal.trans(F.F64, FM(x, y), r1, x, e1, Equal.trans(F.F64, r1, r2, x, e2, Equal.trans(F.F64, r2, r3, x, e3, Equal.trans(F.F64, r3, r4, x, {==}, Equal.trans(F.F64, r4, SF.round(s, SF.mant(x), SF.xexp(x)), x, e4, rt(x, hfin))))))
405
406# ---- the loop's result for a nonzero y ----
407
408def bpv(+y: F.F64) -> Nat:
409  Nat.sub(SW.value(F.dmant(y)), 1n)
410
411def ynz(+y: F.F64, +hzy: {SF.is_zero(y) == False{} : Bool}) -> {Nat.is_eq(SW.value(F.dmant(y)), 0n) == False{} : Bool}:
412  Equal.trans(Bool, Nat.is_eq(SW.value(F.dmant(y)), 0n), SF.is_zero(y), False{}, T.dmz(y), hzy)
413
414def eBy(+y: F.F64, +hzy: {SF.is_zero(y) == False{} : Bool}) -> {SW.value(F.dmant(y)) == 1n+bpv(y) : Nat}:
415  Equal.sym(Nat, Nat.add(1n, bpv(y)), SW.value(F.dmant(y)), N.sub_add(SW.value(F.dmant(y)), 1n, FL.nz_le(SW.value(F.dmant(y)), ynz(y, hzy))))
416
417def hbzy(+y: F.F64, +hzy: {SF.is_zero(y) == False{} : Bool}) -> {X.is_zero(F.dmant(y)) == False{} : Bool}:
418  Equal.trans(Bool, X.is_zero(F.dmant(y)), Nat.is_eq(SW.value(F.dmant(y)), 0n), False{}, WA.is_zero_value(F.dmant(y)), ynz(y, hzy))
419
420def hBy(+y: F.F64, +hzy: {SF.is_zero(y) == False{} : Bool}) -> {C.fits(53n, 1n+bpv(y)) == True{} : Bool}:
421  L.subst(Nat, t => {C.fits(53n, t) == True{} : Bool}, SW.value(F.dmant(y)), 1n+bpv(y), eBy(y, hzy), T.mw53(y))
422
423def DD(+x: F.F64, +y: F.F64) -> Nat:
424  Nat.sub(F.dexp(x), F.dexp(y))
425
426def qr_r(+x: F.F64, +y: F.F64, +hzy: {SF.is_zero(y) == False{} : Bool}) -> {SW.value(X.psnd(F.fm_qr(x, y))) == Nat.mod(C.shift(DD(x, y), SW.value(F.dmant(x))), SW.value(F.dmant(y))) : Nat}:
427  +xw = F.dmant(x)
428  +yw = F.dmant(y)
429  +D = DD(x, y)
430  +bp = bpv(y)
431  +V = SW.value(yw)
432  +e0 = Equal.cong(WU.U64 & WU.U64, Nat, u => SW.value(X.psnd(F.fm_go(D, yw, D, u))), X.divmod(xw, yw), (X.pfst(X.divmod(xw, yw)), X.psnd(X.divmod(xw, yw))), eta(X.divmod(xw, yw)))
433  +hr0 = Equal.trans(Nat, SW.value(X.rem(xw, yw)), Nat.mod(SW.value(xw), V), Nat.mod(SW.value(xw), 1n+bp), DR.divmod_rem(xw, yw, hbzy(y, hzy)), Equal.cong(Nat, Nat, t => Nat.mod(SW.value(xw), t), V, 1n+bp, eBy(y, hzy)))
434  +e1 = loop_r(D, yw, bp, eBy(y, hzy), hBy(y, hzy), hbzy(y, hzy), D, N.le_refl(D), X.pfst(X.divmod(xw, yw)), X.psnd(X.divmod(xw, yw)), SW.value(xw), hr0)
435  +e2 = Equal.cong(Nat, Nat, t => Nat.mod(C.shift(D, SW.value(xw)), t), 1n+bp, V, Equal.sym(Nat, V, 1n+bp, eBy(y, hzy)))
436  Equal.trans(Nat, SW.value(X.psnd(F.fm_go(D, yw, D, X.divmod(xw, yw)))), SW.value(X.psnd(F.fm_go(D, yw, D, (X.pfst(X.divmod(xw, yw)), X.psnd(X.divmod(xw, yw)))))), Nat.mod(C.shift(D, SW.value(xw)), V), e0, Equal.trans(Nat, SW.value(X.psnd(F.fm_go(D, yw, D, (X.pfst(X.divmod(xw, yw)), X.psnd(X.divmod(xw, yw)))))), Nat.mod(C.shift(D, SW.value(xw)), 1n+bp), Nat.mod(C.shift(D, SW.value(xw)), V), e1, e2))
437
438def qr_q(+x: F.F64, +y: F.F64, +hzy: {SF.is_zero(y) == False{} : Bool}) -> {Nat.mod(SW.value(X.pfst(F.fm_qr(x, y))), 2n) == Nat.mod(Nat.div(C.shift(DD(x, y), SW.value(F.dmant(x))), SW.value(F.dmant(y))), 2n) : Nat}:
439  +xw = F.dmant(x)
440  +yw = F.dmant(y)
441  +D = DD(x, y)
442  +bp = bpv(y)
443  +V = SW.value(yw)
444  +e0 = Equal.cong(WU.U64 & WU.U64, Nat, u => Nat.mod(SW.value(X.pfst(F.fm_go(D, yw, D, u))), 2n), X.divmod(xw, yw), (X.pfst(X.divmod(xw, yw)), X.psnd(X.divmod(xw, yw))), eta(X.divmod(xw, yw)))
445  +hr0 = Equal.trans(Nat, SW.value(X.rem(xw, yw)), Nat.mod(SW.value(xw), V), Nat.mod(SW.value(xw), 1n+bp), DR.divmod_rem(xw, yw, hbzy(y, hzy)), Equal.cong(Nat, Nat, t => Nat.mod(SW.value(xw), t), V, 1n+bp, eBy(y, hzy)))
446  +hq0 = Equal.cong(Nat, Nat, t => Nat.mod(t, 2n), SW.value(X.quot(xw, yw)), Nat.div(SW.value(xw), 1n+bp), Equal.trans(Nat, SW.value(X.quot(xw, yw)), Nat.div(SW.value(xw), V), Nat.div(SW.value(xw), 1n+bp), DQ.divmod_quot(xw, yw, hbzy(y, hzy)), Equal.cong(Nat, Nat, t => Nat.div(SW.value(xw), t), V, 1n+bp, eBy(y, hzy))))
447  +e1 = loop_q(D, yw, bp, eBy(y, hzy), hBy(y, hzy), hbzy(y, hzy), D, N.le_refl(D), X.pfst(X.divmod(xw, yw)), X.psnd(X.divmod(xw, yw)), SW.value(xw), hr0, hq0)
448  +e2 = Equal.cong(Nat, Nat, t => Nat.mod(Nat.div(C.shift(D, SW.value(xw)), t), 2n), 1n+bp, V, Equal.sym(Nat, V, 1n+bp, eBy(y, hzy)))
449  Equal.trans(Nat, Nat.mod(SW.value(X.pfst(F.fm_go(D, yw, D, X.divmod(xw, yw)))), 2n), Nat.mod(SW.value(X.pfst(F.fm_go(D, yw, D, (X.pfst(X.divmod(xw, yw)), X.psnd(X.divmod(xw, yw)))))), 2n), Nat.mod(Nat.div(C.shift(D, SW.value(xw)), V), 2n), e0, Equal.trans(Nat, Nat.mod(SW.value(X.pfst(F.fm_go(D, yw, D, (X.pfst(X.divmod(xw, yw)), X.psnd(X.divmod(xw, yw)))))), 2n), Nat.mod(Nat.div(C.shift(D, SW.value(xw)), 1n+bp), 2n), Nat.mod(Nat.div(C.shift(D, SW.value(xw)), V), 2n), e1, e2))
450
451# ---- fmod ----
452
453def NRd(+s: Bool, +a: Nat, +b: Nat, +m1: Nat, +m2: Nat) -> F.F64:
454  SF.round(s, Nat.mod(C.shift(Nat.sub(a, b), m1), m2), b)
455
456# FM when y has the smaller (or equal) scale
457def fm_spec_near(+x: F.F64, +y: F.F64, +hge: {Nat.is_lt(SF.xexp(x), SF.xexp(y)) == False{} : Bool}) -> {FM(x, y) == NRd(SF.sign(x), SF.xexp(x), SF.xexp(y), SF.mant(x), SF.mant(y)) : F.F64}:
458  +s = SF.sign(x)
459  +xx = SF.xexp(x)
460  +xy = SF.xexp(y)
461  +mx = SF.mant(x)
462  +my = SF.mant(y)
463  +e1 = Equal.cong(Nat, F.F64, t => SF.round(s, Nat.mod(C.shift(Nat.sub(xx, t), mx), C.shift(Nat.sub(xy, t), my)), t), Nat.min(xx, xy), xy, N.min_right(xx, xy, hge))
464  +e2 = Equal.cong(Nat, F.F64, t => SF.round(s, Nat.mod(C.shift(Nat.sub(xx, xy), mx), C.shift(t, my)), xy), Nat.sub(xy, xy), 0n, N.sub_self(xy))
465  Equal.trans(F.F64, FM(x, y), SF.round(s, Nat.mod(C.shift(Nat.sub(xx, xy), mx), C.shift(Nat.sub(xy, xy), my)), xy), NRd(s, xx, xy, mx, my), e1, e2)
466
467def nrd_v(+x: F.F64, +y: F.F64) -> {NRd(F.signbit(x), F.dexp(x), F.dexp(y), SW.value(F.dmant(x)), SW.value(F.dmant(y))) == NRd(SF.sign(x), SF.xexp(x), SF.xexp(y), SF.mant(x), SF.mant(y)) : F.F64}:
468  +e1 = Equal.cong(Bool, F.F64, t => NRd(t, F.dexp(x), F.dexp(y), SW.value(F.dmant(x)), SW.value(F.dmant(y))), F.signbit(x), SF.sign(x), FB.signbit_value(x))
469  +e2 = Equal.cong(Nat, F.F64, t => NRd(SF.sign(x), t, F.dexp(y), SW.value(F.dmant(x)), SW.value(F.dmant(y))), F.dexp(x), SF.xexp(x), T.dexp_value(x))
470  +e3 = Equal.cong(Nat, F.F64, t => NRd(SF.sign(x), SF.xexp(x), t, SW.value(F.dmant(x)), SW.value(F.dmant(y))), F.dexp(y), SF.xexp(y), T.dexp_value(y))
471  +e4 = Equal.cong(Nat, F.F64, t => NRd(SF.sign(x), SF.xexp(x), SF.xexp(y), t, SW.value(F.dmant(y))), SW.value(F.dmant(x)), SF.mant(x), T.dmant_value(x))
472  +e5 = Equal.cong(Nat, F.F64, t => NRd(SF.sign(x), SF.xexp(x), SF.xexp(y), SF.mant(x), t), SW.value(F.dmant(y)), SF.mant(y), T.dmant_value(y))
473  +r1 = NRd(SF.sign(x), F.dexp(x), F.dexp(y), SW.value(F.dmant(x)), SW.value(F.dmant(y)))
474  +r2 = NRd(SF.sign(x), SF.xexp(x), F.dexp(y), SW.value(F.dmant(x)), SW.value(F.dmant(y)))
475  +r3 = NRd(SF.sign(x), SF.xexp(x), SF.xexp(y), SW.value(F.dmant(x)), SW.value(F.dmant(y)))
476  +r4 = NRd(SF.sign(x), SF.xexp(x), SF.xexp(y), SF.mant(x), SW.value(F.dmant(y)))
477  +G = NRd(SF.sign(x), SF.xexp(x), SF.xexp(y), SF.mant(x), SF.mant(y))
478  Equal.trans(F.F64, NRd(F.signbit(x), F.dexp(x), F.dexp(y), SW.value(F.dmant(x)), SW.value(F.dmant(y))), r1, G, e1, Equal.trans(F.F64, r1, r2, G, e2, Equal.trans(F.F64, r2, r3, G, e3, Equal.trans(F.F64, r3, r4, G, e4, e5))))
479
480def xlt(+x: F.F64, +y: F.F64, +b: Bool, +h: {Nat.is_lt(F.dexp(x), F.dexp(y)) == b : Bool}) -> {Nat.is_lt(SF.xexp(x), SF.xexp(y)) == b : Bool}:
481  +h1 = L.subst(Nat, t => {Nat.is_lt(t, F.dexp(y)) == b : Bool}, F.dexp(x), SF.xexp(x), T.dexp_value(x), h)
482  L.subst(Nat, t => {Nat.is_lt(SF.xexp(x), t) == b : Bool}, F.dexp(y), SF.xexp(y), T.dexp_value(y), h1)
483
484def fm_near(+x: F.F64, +y: F.F64, +hzy: {SF.is_zero(y) == False{} : Bool}, +hge: {Nat.is_lt(F.dexp(x), F.dexp(y)) == False{} : Bool}) -> {F.round_w(F.signbit(x), F.dexp(y), X.psnd(F.fm_qr(x, y))) == FM(x, y) : F.F64}:
485  +r = X.psnd(F.fm_qr(x, y))
486  +e1 = T.rw_value(F.signbit(x), F.dexp(y), r, T.dexp_ge(y))
487  +e2 = Equal.cong(Nat, F.F64, t => SF.round(F.signbit(x), t, F.dexp(y)), SW.value(r), Nat.mod(C.shift(DD(x, y), SW.value(F.dmant(x))), SW.value(F.dmant(y))), qr_r(x, y, hzy))
488  +G = NRd(SF.sign(x), SF.xexp(x), SF.xexp(y), SF.mant(x), SF.mant(y))
489  +e3 = nrd_v(x, y)
490  +e4 = Equal.sym(F.F64, FM(x, y), G, fm_spec_near(x, y, xlt(x, y, False{}, hge)))
491  +r1 = SF.round(F.signbit(x), SW.value(r), F.dexp(y))
492  +r2 = NRd(F.signbit(x), F.dexp(x), F.dexp(y), SW.value(F.dmant(x)), SW.value(F.dmant(y)))
493  Equal.trans(F.F64, F.round_w(F.signbit(x), F.dexp(y), r), r1, FM(x, y), e1, Equal.trans(F.F64, r1, r2, FM(x, y), e2, Equal.trans(F.F64, r2, G, FM(x, y), e3, e4)))
494
495def nn(+b: Bool) -> {Bool.not(Bool.not(b)) == b : Bool}:
496  match b:
497    case True{}:
498      {==}
499    case False{}:
500      {==}
501
502def badv(+x: F.F64, +y: F.F64) -> {Bool.or(Bool.or(F.unordered(x, y), F.is_inf(x)), F.is_zero(y)) == SF.rbad(x, y) : Bool}:
503  +e1 = Equal.cong(Bool, Bool, t => Bool.or(Bool.or(Bool.or(t, F.is_nan(y)), F.is_inf(x)), F.is_zero(y)), F.is_nan(x), SF.is_nan(x), FB.is_nan_value(x))
504  +e2 = Equal.cong(Bool, Bool, t => Bool.or(Bool.or(Bool.or(SF.is_nan(x), t), F.is_inf(x)), F.is_zero(y)), F.is_nan(y), SF.is_nan(y), FB.is_nan_value(y))
505  +U = Bool.or(SF.is_nan(x), SF.is_nan(y))
506  +e3 = Equal.cong(Bool, Bool, t => Bool.or(Bool.or(t, F.is_inf(x)), F.is_zero(y)), U, Bool.not(Bool.not(U)), Equal.sym(Bool, Bool.not(Bool.not(U)), U, nn(U)))
507  +e4 = Equal.cong(Bool, Bool, t => Bool.or(Bool.or(Bool.not(Bool.not(U)), t), F.is_zero(y)), F.is_inf(x), SF.is_inf(x), FB.is_inf_value(x))
508  +e5 = Equal.cong(Bool, Bool, t => Bool.or(Bool.or(Bool.not(Bool.not(U)), SF.is_inf(x)), t), F.is_zero(y), SF.is_zero(y), FB.is_zero_value(y))
509  +b1 = Bool.or(Bool.or(Bool.or(SF.is_nan(x), F.is_nan(y)), F.is_inf(x)), F.is_zero(y))
510  +b2 = Bool.or(Bool.or(U, F.is_inf(x)), F.is_zero(y))
511  +b3 = Bool.or(Bool.or(Bool.not(Bool.not(U)), F.is_inf(x)), F.is_zero(y))
512  +b4 = Bool.or(Bool.or(Bool.not(Bool.not(U)), SF.is_inf(x)), F.is_zero(y))
513  Equal.trans(Bool, Bool.or(Bool.or(F.unordered(x, y), F.is_inf(x)), F.is_zero(y)), b1, SF.rbad(x, y), e1, Equal.trans(Bool, b1, b2, SF.rbad(x, y), e2, Equal.trans(Bool, b2, b3, SF.rbad(x, y), e3, Equal.trans(Bool, b3, b4, SF.rbad(x, y), e4, e5))))
514
515# what a false rbad says
516def ok_zy(+x: F.F64, +y: F.F64, +h: {SF.rbad(x, y) == False{} : Bool}) -> {SF.is_zero(y) == False{} : Bool}:
517  FC.or_r(Bool.or(Bool.not(SF.ordered(x, y)), SF.is_inf(x)), SF.is_zero(y), h)
518
519def ok_ix(+x: F.F64, +y: F.F64, +h: {SF.rbad(x, y) == False{} : Bool}) -> {SF.is_inf(x) == False{} : Bool}:
520  FC.or_r(Bool.not(SF.ordered(x, y)), SF.is_inf(x), FC.or_l(Bool.or(Bool.not(SF.ordered(x, y)), SF.is_inf(x)), SF.is_zero(y), h))
521
522def ok_u(+x: F.F64, +y: F.F64, +h: {SF.rbad(x, y) == False{} : Bool}) -> {Bool.or(SF.is_nan(x), SF.is_nan(y)) == False{} : Bool}:
523  +h1 = FC.or_l(Bool.not(SF.ordered(x, y)), SF.is_inf(x), FC.or_l(Bool.or(Bool.not(SF.ordered(x, y)), SF.is_inf(x)), SF.is_zero(y), h))
524  FR.not_t(Bool.or(SF.is_nan(x), SF.is_nan(y)), FR.not_f(SF.ordered(x, y), h1))
525
526def ok_fin(+x: F.F64, +y: F.F64, +h: {SF.rbad(x, y) == False{} : Bool}) -> {Nat.is_lt(SF.efield(x), 2047n) == True{} : Bool}:
527  fin(x, FC.or_l(SF.is_nan(x), SF.is_nan(y), ok_u(x, y, h)), ok_ix(x, y, h))
528
529def ff_c(+x: F.F64, +y: F.F64, +h: {SF.rbad(x, y) == False{} : Bool}, +far: Bool, +hfar: {Nat.is_lt(F.dexp(x), F.dexp(y)) == far : Bool}) -> {F.fmod_fin(x, y, far) == FM(x, y) : F.F64}:
530  match far:
531    case True{}:
532      Equal.sym(F.F64, FM(x, y), x, fm_far(x, y, xlt(x, y, True{}, hfar), ok_fin(x, y, h)))
533    case False{}:
534      fm_near(x, y, ok_zy(x, y, h), hfar)
535
536def fz_c(+x: F.F64, +y: F.F64, +h: {SF.rbad(x, y) == False{} : Bool}, +zx: Bool, +hzx: {SF.is_zero(x) == zx : Bool}) -> {F.fmod_z(x, y, zx) == FM(x, y) : F.F64}:
537  match zx:
538    case True{}:
539      Equal.sym(F.F64, FM(x, y), x, fm_zero(x, y, hzx, ok_zy(x, y, h), ok_fin(x, y, h)))
540    case False{}:
541      ff_c(x, y, h, Nat.is_lt(F.dexp(x), F.dexp(y)), {==})
542
543def fyi_c(+x: F.F64, +y: F.F64, +h: {SF.rbad(x, y) == False{} : Bool}, +yi: Bool) -> {F.fmod_yi(x, y, yi) == SF.pick(F.F64, yi, x, FM(x, y)) : F.F64}:
544  match yi:
545    case True{}:
546      {==}
547    case False{}:
548      Equal.trans(F.F64, F.fmod_z(x, y, F.is_zero(x)), F.fmod_z(x, y, SF.is_zero(x)), FM(x, y), Equal.cong(Bool, F.F64, t => F.fmod_z(x, y, t), F.is_zero(x), SF.is_zero(x), FB.is_zero_value(x)), fz_c(x, y, h, SF.is_zero(x), {==}))
549
550def fb_c(+x: F.F64, +y: F.F64, +bad: Bool, +h: {SF.rbad(x, y) == bad : Bool}) -> {F.fmod_bad(x, y, bad) == SF.pick(F.F64, bad, SF.qnan(), SF.pick(F.F64, SF.is_inf(y), x, FM(x, y))) : F.F64}:
551  match bad:
552    case True{}:
553      {==}
554    case False{}:
555      Equal.trans(F.F64, F.fmod_yi(x, y, F.is_inf(y)), F.fmod_yi(x, y, SF.is_inf(y)), SF.pick(F.F64, SF.is_inf(y), x, FM(x, y)), Equal.cong(Bool, F.F64, t => F.fmod_yi(x, y, t), F.is_inf(y), SF.is_inf(y), FB.is_inf_value(y)), fyi_c(x, y, h, SF.is_inf(y)))
556
557def fmod_value(+x: F.F64, +y: F.F64) -> SF.Fmod.value(x, y):
558  +e1 = Equal.cong(Bool, F.F64, t => F.fmod_bad(x, y, t), Bool.or(Bool.or(F.unordered(x, y), F.is_inf(x)), F.is_zero(y)), SF.rbad(x, y), badv(x, y))
559  Equal.trans(F.F64, F.fmod(x, y), F.fmod_bad(x, y, SF.rbad(x, y)), SF.fmod(x, y), e1, fb_c(x, y, SF.rbad(x, y), {==}))
560
561# ---- remainder ----
562
563def addrr(+r: WU.U64, +Rv: Nat, +er: {SW.value(r) == Rv : Nat}, +hf: {C.fits(53n, Rv) == True{} : Bool}) -> {SW.value(X.add(r, r)) == Nat.add(Rv, Rv) : Nat}:
564  +f64 = SH.fits_mono(54n, 64n, Nat.add(Rv, Rv), {==}, FR.fits_add1(53n, Rv, Rv, hf, hf))
565  e1 = WA.add_value(r, r)
566  +e2 = Equal.cong(Nat, Nat, t => C.low(64n, Nat.add(t, t)), SW.value(r), Rv, er)
567  Equal.trans(Nat, SW.value(X.add(r, r)), C.low(64n, Nat.add(SW.value(r), SW.value(r))), Nat.add(Rv, Rv), e1, Equal.trans(Nat, C.low(64n, Nat.add(SW.value(r), SW.value(r))), C.low(64n, Nat.add(Rv, Rv)), Nat.add(Rv, Rv), e2, WW.low_fit(64n, Nat.add(Rv, Rv), f64)))
568
569def rmp_c(+s: Bool, +u: Nat, +hu: {Nat.is_le(63n, u) == True{} : Bool}, +b: WU.U64, +r: WU.U64, +Bv: Nat, +Rv: Nat, +eb: {SW.value(b) == Bv : Nat}, +er: {SW.value(r) == Rv : Nat}, +hRB: {Nat.is_le(Rv, Bv) == True{} : Bool}, +c: Bool) -> {F.rm_pick(s, u, b, r, c) == SF.pick(F.F64, c, SF.round(Bool.not(s), Nat.sub(Bv, Rv), u), SF.round(s, Rv, u)) : F.F64}:
570  match c:
571    case True{}:
572      +hle = L.subst(Nat, t => {Nat.is_le(t, SW.value(b)) == True{} : Bool}, Rv, SW.value(r), Equal.sym(Nat, SW.value(r), Rv, er), L.subst(Nat, t => {Nat.is_le(Rv, t) == True{} : Bool}, Bv, SW.value(b), Equal.sym(Nat, SW.value(b), Bv, eb), hRB))
573      +es = Equal.trans(Nat, SW.value(X.sub(b, r)), Nat.sub(SW.value(b), SW.value(r)), Nat.sub(Bv, Rv), WA.sub_value(b, r, hle), Equal.trans(Nat, Nat.sub(SW.value(b), SW.value(r)), Nat.sub(Bv, SW.value(r)), Nat.sub(Bv, Rv), Equal.cong(Nat, Nat, t => Nat.sub(t, SW.value(r)), SW.value(b), Bv, eb), Equal.cong(Nat, Nat, t => Nat.sub(Bv, t), SW.value(r), Rv, er)))
574      Equal.trans(F.F64, F.round_w(Bool.not(s), u, X.sub(b, r)), SF.round(Bool.not(s), SW.value(X.sub(b, r)), u), SF.round(Bool.not(s), Nat.sub(Bv, Rv), u), T.rw_value(Bool.not(s), u, X.sub(b, r), hu), Equal.cong(Nat, F.F64, t => SF.round(Bool.not(s), t, u), SW.value(X.sub(b, r)), Nat.sub(Bv, Rv), es))
575    case False{}:
576      Equal.trans(F.F64, F.round_w(s, u, r), SF.round(s, SW.value(r), u), SF.round(s, Rv, u), T.rw_value(s, u, r, hu), Equal.cong(Nat, F.F64, t => SF.round(s, t, u), SW.value(r), Rv, er))
577
578# rm_fix on words is the spec's rnear on their values
579def rmfix_v(+s: Bool, +u: Nat, +hu: {Nat.is_le(63n, u) == True{} : Bool}, +b: WU.U64, +r: WU.U64, +q: WU.U64, +Bv: Nat, +Rv: Nat, +Qv: Nat, +eb: {SW.value(b) == Bv : Nat}, +er: {SW.value(r) == Rv : Nat}, +hq: {Nat.mod(SW.value(q), 2n) == Nat.mod(Qv, 2n) : Nat}, +hRB: {Nat.is_le(Rv, Bv) == True{} : Bool}, +hf: {C.fits(53n, Rv) == True{} : Bool}) -> {F.rm_fix(s, u, b, r, q) == SF.rnear(s, Rv, Bv, Qv, u) : F.F64}:
580  +R2 = Nat.add(Rv, Rv)
581  +ea = addrr(r, Rv, er, hf)
582  +f1 = Equal.trans(Bool, X.lt(b, X.add(r, r)), Nat.is_lt(SW.value(b), SW.value(X.add(r, r))), Nat.is_lt(Bv, R2), WA.lt_value(b, X.add(r, r)), Equal.trans(Bool, Nat.is_lt(SW.value(b), SW.value(X.add(r, r))), Nat.is_lt(Bv, SW.value(X.add(r, r))), Nat.is_lt(Bv, R2), Equal.cong(Nat, Bool, t => Nat.is_lt(t, SW.value(X.add(r, r))), SW.value(b), Bv, eb), Equal.cong(Nat, Bool, t => Nat.is_lt(Bv, t), SW.value(X.add(r, r)), R2, ea)))
583  +f2 = Equal.trans(Bool, X.eq(X.add(r, r), b), Nat.is_eq(SW.value(X.add(r, r)), SW.value(b)), Nat.is_eq(R2, Bv), WA.eq_value(X.add(r, r), b), Equal.trans(Bool, Nat.is_eq(SW.value(X.add(r, r)), SW.value(b)), Nat.is_eq(R2, SW.value(b)), Nat.is_eq(R2, Bv), Equal.cong(Nat, Bool, t => Nat.is_eq(t, SW.value(b)), SW.value(X.add(r, r)), R2, addrr(r, Rv, er, hf)), Equal.cong(Nat, Bool, t => Nat.is_eq(R2, t), SW.value(b), Bv, eb)))
584  +f3 = Equal.trans(Bool, X.odd(q), Nat.is_eq(Nat.mod(SW.value(q), 2n), 1n), Nat.is_eq(Nat.mod(Qv, 2n), 1n), WA.odd_value(q), Equal.cong(Nat, Bool, t => Nat.is_eq(t, 1n), Nat.mod(SW.value(q), 2n), Nat.mod(Qv, 2n), hq))
585  +g1 = Equal.cong(Bool, F.F64, t => F.rm_pick(s, u, b, r, Bool.or(t, Bool.and(X.eq(X.add(r, r), b), X.odd(q)))), X.lt(b, X.add(r, r)), Nat.is_lt(Bv, R2), f1)
586  +g2 = Equal.cong(Bool, F.F64, t => F.rm_pick(s, u, b, r, Bool.or(Nat.is_lt(Bv, R2), Bool.and(t, X.odd(q)))), X.eq(X.add(r, r), b), Nat.is_eq(R2, Bv), f2)
587  +g3 = Equal.cong(Bool, F.F64, t => F.rm_pick(s, u, b, r, Bool.or(Nat.is_lt(Bv, R2), Bool.and(Nat.is_eq(R2, Bv), t))), X.odd(q), Nat.is_eq(Nat.mod(Qv, 2n), 1n), f3)
588  +a1 = F.rm_pick(s, u, b, r, Bool.or(Nat.is_lt(Bv, R2), Bool.and(X.eq(X.add(r, r), b), X.odd(q))))
589  +a2 = F.rm_pick(s, u, b, r, Bool.or(Nat.is_lt(Bv, R2), Bool.and(Nat.is_eq(R2, Bv), X.odd(q))))
590  +a3 = F.rm_pick(s, u, b, r, SF.rflip(Rv, Bv, Qv))
591  Equal.trans(F.F64, F.rm_fix(s, u, b, r, q), a1, SF.rnear(s, Rv, Bv, Qv, u), g1, Equal.trans(F.F64, a1, a2, SF.rnear(s, Rv, Bv, Qv, u), g2, Equal.trans(F.F64, a2, a3, SF.rnear(s, Rv, Bv, Qv, u), g3, rmp_c(s, u, hu, b, r, Bv, Rv, eb, er, hRB, SF.rflip(Rv, Bv, Qv)))))
592
593def RNs(+x: F.F64, +y: F.F64) -> F.F64:
594  SF.rnear(SF.sign(x), Nat.mod(SF.ra(x, y), SF.rb(x, y)), SF.rb(x, y), Nat.div(SF.ra(x, y), SF.rb(x, y)), SF.rsc(x, y))
595
596def RNd(+s: Bool, +a: Nat, +b: Nat, +m1: Nat, +m2: Nat) -> F.F64:
597  SF.rnear(s, Nat.mod(C.shift(Nat.sub(a, b), m1), m2), m2, Nat.div(C.shift(Nat.sub(a, b), m1), m2), b)
598
599def rn_spec_near(+x: F.F64, +y: F.F64, +hge: {Nat.is_lt(SF.xexp(x), SF.xexp(y)) == False{} : Bool}) -> {RNs(x, y) == RNd(SF.sign(x), SF.xexp(x), SF.xexp(y), SF.mant(x), SF.mant(y)) : F.F64}:
600  +s = SF.sign(x)
601  +xx = SF.xexp(x)
602  +xy = SF.xexp(y)
603  +mx = SF.mant(x)
604  +my = SF.mant(y)
605  +e1 = Equal.cong(Nat, F.F64, t => SF.rnear(s, Nat.mod(C.shift(Nat.sub(xx, t), mx), C.shift(Nat.sub(xy, t), my)), C.shift(Nat.sub(xy, t), my), Nat.div(C.shift(Nat.sub(xx, t), mx), C.shift(Nat.sub(xy, t), my)), t), Nat.min(xx, xy), xy, N.min_right(xx, xy, hge))
606  +A = C.shift(Nat.sub(xx, xy), mx)
607  +e2 = Equal.cong(Nat, F.F64, t => SF.rnear(s, Nat.mod(A, C.shift(t, my)), C.shift(t, my), Nat.div(A, C.shift(t, my)), xy), Nat.sub(xy, xy), 0n, N.sub_self(xy))
608  Equal.trans(F.F64, RNs(x, y), SF.rnear(s, Nat.mod(A, C.shift(Nat.sub(xy, xy), my)), C.shift(Nat.sub(xy, xy), my), Nat.div(A, C.shift(Nat.sub(xy, xy), my)), xy), RNd(s, xx, xy, mx, my), e1, e2)
609
610def rnd_v(+x: F.F64, +y: F.F64) -> {RNd(F.signbit(x), F.dexp(x), F.dexp(y), SW.value(F.dmant(x)), SW.value(F.dmant(y))) == RNd(SF.sign(x), SF.xexp(x), SF.xexp(y), SF.mant(x), SF.mant(y)) : F.F64}:
611  +e1 = Equal.cong(Bool, F.F64, t => RNd(t, F.dexp(x), F.dexp(y), SW.value(F.dmant(x)), SW.value(F.dmant(y))), F.signbit(x), SF.sign(x), FB.signbit_value(x))
612  +e2 = Equal.cong(Nat, F.F64, t => RNd(SF.sign(x), t, F.dexp(y), SW.value(F.dmant(x)), SW.value(F.dmant(y))), F.dexp(x), SF.xexp(x), T.dexp_value(x))
613  +e3 = Equal.cong(Nat, F.F64, t => RNd(SF.sign(x), SF.xexp(x), t, SW.value(F.dmant(x)), SW.value(F.dmant(y))), F.dexp(y), SF.xexp(y), T.dexp_value(y))
614  +e4 = Equal.cong(Nat, F.F64, t => RNd(SF.sign(x), SF.xexp(x), SF.xexp(y), t, SW.value(F.dmant(y))), SW.value(F.dmant(x)), SF.mant(x), T.dmant_value(x))
615  +e5 = Equal.cong(Nat, F.F64, t => RNd(SF.sign(x), SF.xexp(x), SF.xexp(y), SF.mant(x), t), SW.value(F.dmant(y)), SF.mant(y), T.dmant_value(y))
616  +r1 = RNd(SF.sign(x), F.dexp(x), F.dexp(y), SW.value(F.dmant(x)), SW.value(F.dmant(y)))
617  +r2 = RNd(SF.sign(x), SF.xexp(x), F.dexp(y), SW.value(F.dmant(x)), SW.value(F.dmant(y)))
618  +r3 = RNd(SF.sign(x), SF.xexp(x), SF.xexp(y), SW.value(F.dmant(x)), SW.value(F.dmant(y)))
619  +r4 = RNd(SF.sign(x), SF.xexp(x), SF.xexp(y), SF.mant(x), SW.value(F.dmant(y)))
620  +G = RNd(SF.sign(x), SF.xexp(x), SF.xexp(y), SF.mant(x), SF.mant(y))
621  Equal.trans(F.F64, RNd(F.signbit(x), F.dexp(x), F.dexp(y), SW.value(F.dmant(x)), SW.value(F.dmant(y))), r1, G, e1, Equal.trans(F.F64, r1, r2, G, e2, Equal.trans(F.F64, r2, r3, G, e3, Equal.trans(F.F64, r3, r4, G, e4, e5))))
622
623def modlt(+n: Nat, +V: Nat, +hne: {Nat.is_eq(V, 0n) == False{} : Bool}) -> {Nat.is_lt(Nat.mod(n, V), V) == True{} : Bool}:
624  match V:
625    case 0n:
626      Empty.absurd({Nat.is_lt(Nat.mod(n, 0n), 0n) == True{} : Bool}, FL.true_ne_false(hne))
627    case 1n+ +vp:
628      MS.divmod_lt(n, vp)
629
630def rm_near_c(+x: F.F64, +y: F.F64, +hzy: {SF.is_zero(y) == False{} : Bool}) -> {F.rm_qr(x, y, F.fm_qr(x, y)) == RNd(F.signbit(x), F.dexp(x), F.dexp(y), SW.value(F.dmant(x)), SW.value(F.dmant(y))) : F.F64}:
631  +Vx = SW.value(F.dmant(x))
632  +Vy = SW.value(F.dmant(y))
633  +Rv = Nat.mod(C.shift(DD(x, y), Vx), Vy)
634  +Qv = Nat.div(C.shift(DD(x, y), Vx), Vy)
635  +e0 = Equal.cong(WU.U64 & WU.U64, F.F64, p => F.rm_qr(x, y, p), F.fm_qr(x, y), (X.pfst(F.fm_qr(x, y)), X.psnd(F.fm_qr(x, y))), eta(F.fm_qr(x, y)))
636  +hRB = N.lt_le(Rv, Vy, modlt(C.shift(DD(x, y), Vx), Vy, ynz(y, hzy)))
637  +hf = SH.fits_lek(53n, Rv, Vy, N.lt_le(Rv, Vy, modlt(C.shift(DD(x, y), Vx), Vy, ynz(y, hzy))), T.mw53(y))
638  +e1 = rmfix_v(F.signbit(x), F.dexp(y), T.dexp_ge(y), F.dmant(y), X.psnd(F.fm_qr(x, y)), X.pfst(F.fm_qr(x, y)), Vy, Rv, Qv, {==}, qr_r(x, y, hzy), qr_q(x, y, hzy), hRB, hf)
639  Equal.trans(F.F64, F.rm_qr(x, y, F.fm_qr(x, y)), F.rm_fix(F.signbit(x), F.dexp(y), F.dmant(y), X.psnd(F.fm_qr(x, y)), X.pfst(F.fm_qr(x, y))), RNd(F.signbit(x), F.dexp(x), F.dexp(y), Vx, Vy), e0, e1)
640
641def rn_spec_far(+x: F.F64, +y: F.F64, +hlt: {Nat.is_lt(SF.xexp(x), SF.xexp(y)) == True{} : Bool}) -> {RNs(x, y) == SF.rnear(SF.sign(x), SF.mant(x), C.shift(Nat.sub(SF.xexp(y), SF.xexp(x)), SF.mant(y)), 0n, SF.xexp(x)) : F.F64}:
642  +s = SF.sign(x)
643  +xx = SF.xexp(x)
644  +xy = SF.xexp(y)
645  +mx = SF.mant(x)
646  +my = SF.mant(y)
647  +S = C.shift(Nat.sub(xy, xx), my)
648  +e1 = Equal.cong(Nat, F.F64, t => SF.rnear(s, Nat.mod(C.shift(Nat.sub(xx, t), mx), C.shift(Nat.sub(xy, t), my)), C.shift(Nat.sub(xy, t), my), Nat.div(C.shift(Nat.sub(xx, t), mx), C.shift(Nat.sub(xy, t), my)), t), Nat.min(xx, xy), xx, N.min_left(xx, xy, hlt))
649  +e2 = Equal.cong(Nat, F.F64, t => SF.rnear(s, Nat.mod(C.shift(t, mx), S), S, Nat.div(C.shift(t, mx), S), xx), Nat.sub(xx, xx), 0n, N.sub_self(xx))
650  +e3 = Equal.cong(Nat, F.F64, t => SF.rnear(s, t, S, Nat.div(mx, S), xx), Nat.mod(mx, S), mx, mod_small(mx, S, far_lt(x, y, hlt, 1n, {==})))
651  +e4 = Equal.cong(Nat, F.F64, t => SF.rnear(s, mx, S, t, xx), Nat.div(mx, S), 0n, div_small(mx, S, far_lt(x, y, hlt, 1n, {==})))
652  +r1 = SF.rnear(s, Nat.mod(C.shift(Nat.sub(xx, xx), mx), S), S, Nat.div(C.shift(Nat.sub(xx, xx), mx), S), xx)
653  +r2 = SF.rnear(s, Nat.mod(mx, S), S, Nat.div(mx, S), xx)
654  +r3 = SF.rnear(s, mx, S, Nat.div(mx, S), xx)
655  +G = SF.rnear(s, mx, S, 0n, xx)
656  Equal.trans(F.F64, RNs(x, y), r1, G, e1, Equal.trans(F.F64, r1, r2, G, e2, Equal.trans(F.F64, r2, r3, G, e3, e4)))
657
658def xsub(+x: F.F64, +y: F.F64) -> {Nat.sub(F.dexp(y), F.dexp(x)) == Nat.sub(SF.xexp(y), SF.xexp(x)) : Nat}:
659  Equal.trans(Nat, Nat.sub(F.dexp(y), F.dexp(x)), Nat.sub(SF.xexp(y), F.dexp(x)), Nat.sub(SF.xexp(y), SF.xexp(x)), Equal.cong(Nat, Nat, t => Nat.sub(t, F.dexp(x)), F.dexp(y), SF.xexp(y), T.dexp_value(y)), Equal.cong(Nat, Nat, t => Nat.sub(SF.xexp(y), t), F.dexp(x), SF.xexp(x), T.dexp_value(x)))
660
661# exactly one scale step below y
662def rm_one(+x: F.F64, +y: F.F64, +hlt: {Nat.is_lt(SF.xexp(x), SF.xexp(y)) == True{} : Bool}, +hk: {Nat.sub(F.dexp(y), F.dexp(x)) == 1n : Nat}) -> {F.rm_fix(F.signbit(x), F.dexp(x), X.add(F.dmant(y), F.dmant(y)), F.dmant(x), WU.U64{0, 0}) == RNs(x, y) : F.F64}:
663  +s = SF.sign(x)
664  +xx = SF.xexp(x)
665  +mx = SF.mant(x)
666  +my = SF.mant(y)
667  +my2 = Nat.add(my, my)
668  +ek = Equal.trans(Nat, Nat.sub(SF.xexp(y), xx), Nat.sub(F.dexp(y), F.dexp(x)), 1n, Equal.sym(Nat, Nat.sub(F.dexp(y), F.dexp(x)), Nat.sub(SF.xexp(y), xx), xsub(x, y)), hk)
669  +h0 = L.subst(Nat, t => {Nat.is_lt(mx, C.shift(t, my)) == True{} : Bool}, Nat.sub(SF.xexp(y), xx), 1n, ek, far_lt(x, y, hlt, 1n, {==}))
670  +h2 = L.subst(Nat, t => {Nat.is_lt(mx, t) == True{} : Bool}, Nat.double(my), my2, NA.double_self(my), h0)
671  +e1 = rmfix_v(F.signbit(x), F.dexp(x), T.dexp_ge(x), X.add(F.dmant(y), F.dmant(y)), F.dmant(x), WU.U64{0, 0}, my2, mx, 0n, addrr(F.dmant(y), my, T.dmant_value(y), T.mant_fits(y)), T.dmant_value(x), {==}, N.lt_le(mx, my2, h2), T.mant_fits(x))
672  +e2 = Equal.cong(Bool, F.F64, t => SF.rnear(t, mx, my2, 0n, F.dexp(x)), F.signbit(x), s, FB.signbit_value(x))
673  +e3 = Equal.cong(Nat, F.F64, t => SF.rnear(s, mx, my2, 0n, t), F.dexp(x), xx, T.dexp_value(x))
674  +S = C.shift(Nat.sub(SF.xexp(y), xx), my)
675  +f1 = rn_spec_far(x, y, hlt)
676  +f2 = Equal.cong(Nat, F.F64, t => SF.rnear(s, mx, C.shift(t, my), 0n, xx), Nat.sub(SF.xexp(y), xx), 1n, ek)
677  +f3 = Equal.cong(Nat, F.F64, t => SF.rnear(s, mx, t, 0n, xx), Nat.double(my), my2, NA.double_self(my))
678  +G = SF.rnear(s, mx, my2, 0n, xx)
679  +eR = Equal.trans(F.F64, RNs(x, y), SF.rnear(s, mx, S, 0n, xx), G, f1, Equal.trans(F.F64, SF.rnear(s, mx, S, 0n, xx), SF.rnear(s, mx, Nat.double(my), 0n, xx), G, f2, f3))
680  +a1 = SF.rnear(F.signbit(x), mx, my2, 0n, F.dexp(x))
681  +a2 = SF.rnear(s, mx, my2, 0n, F.dexp(x))
682  Equal.trans(F.F64, F.rm_fix(F.signbit(x), F.dexp(x), X.add(F.dmant(y), F.dmant(y)), F.dmant(x), WU.U64{0, 0}), a1, RNs(x, y), e1, Equal.trans(F.F64, a1, a2, RNs(x, y), e2, Equal.trans(F.F64, a2, G, RNs(x, y), e3, Equal.sym(F.F64, RNs(x, y), G, eR))))
683
684def two_le(+k: Nat, +h1: {Nat.is_le(1n, k) == True{} : Bool}, +h2: {Nat.is_eq(k, 1n) == False{} : Bool}) -> {Nat.is_le(2n, k) == True{} : Bool}:
685  match k:
686    case 0n:
687      Empty.absurd({Nat.is_le(2n, 0n) == True{} : Bool}, FL.true_ne_false(Equal.sym(Bool, False{}, True{}, h1)))
688    case 1n:
689      Empty.absurd({Nat.is_le(2n, 1n) == True{} : Bool}, FL.true_ne_false(h2))
690    case 2n+ +kp:
691      N.zero_le(kp)
692
693def big54(+x: F.F64, +y: F.F64, +hlt: {Nat.is_lt(SF.xexp(x), SF.xexp(y)) == True{} : Bool}, +hk: {Nat.is_eq(Nat.sub(SF.xexp(y), SF.xexp(x)), 1n) == False{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_lt(C.shift(Nat.sub(SF.xexp(y), SF.xexp(x)), SF.mant(y)), Nat.add(SF.mant(x), SF.mant(x))) == False{} : Bool}:
694  +k = Nat.sub(SF.xexp(y), SF.xexp(x))
695  +S = C.shift(k, SF.mant(y))
696  +m2 = Nat.add(SF.mant(x), SF.mant(x))
697  +hk2 = two_le(k, FR.lt_sub_pos(SF.xexp(x), SF.xexp(y), hlt), hk)
698  +f1 = Equal.trans(Bool, C.fits(Nat.add(k, 52n), S), C.fits(52n, SF.mant(y)), False{}, RT.fits_sh(k, 52n, SF.mant(y)), nf52(y, yn_c(x, y, hlt, Nat.is_eq(SF.efield(y), 0n), {==})))
699  +h54 = Equal.trans(Bool, Nat.is_le(Nat.add(2n, 52n), Nat.add(k, 52n)), Nat.is_le(2n, k), True{}, FR.le_cancel_r(2n, k, 52n), hk2)
700  +f2 = FL.nfit_mono(54n, Nat.add(k, 52n), S, h54, f1)
701  +f3 = FR.fits_add1(53n, SF.mant(x), SF.mant(x), T.mant_fits(x), T.mant_fits(x))
702  +l1 = Equal.trans(Bool, Nat.is_lt(m2, C.shift(54n, one)), C.fits(54n, m2), True{}, FR.lt_fit(54n, one, h1, m2), f3)
703  +l2 = Equal.trans(Bool, Nat.is_le(C.shift(54n, one), S), Bool.not(C.fits(54n, S)), True{}, FB.le_fit(54n, one, h1, S), Equal.cong(Bool, Bool, b => Bool.not(b), C.fits(54n, S), False{}, f2))
704  N.le_not_lt(S, m2, N.lt_le(m2, S, N.lt_le_trans(m2, C.shift(54n, one), S, l1, l2)))
705
706def or_ff(+a: Bool, +b: Bool, +ha: {a == False{} : Bool}, +hb: {b == False{} : Bool}) -> {Bool.or(a, b) == False{} : Bool}:
707  Equal.trans(Bool, Bool.or(a, b), Bool.or(False{}, b), False{}, Equal.cong(Bool, Bool, t => Bool.or(t, b), a, False{}, ha), hb)
708
709# two or more scale steps below y: x itself
710def rm_many(+x: F.F64, +y: F.F64, +hlt: {Nat.is_lt(SF.xexp(x), SF.xexp(y)) == True{} : Bool}, +hk: {Nat.is_eq(Nat.sub(F.dexp(y), F.dexp(x)), 1n) == False{} : Bool}, +hfin: {Nat.is_lt(SF.efield(x), 2047n) == True{} : Bool}) -> {RNs(x, y) == x : F.F64}:
711  +s = SF.sign(x)
712  +xx = SF.xexp(x)
713  +mx = SF.mant(x)
714  +S = C.shift(Nat.sub(SF.xexp(y), xx), SF.mant(y))
715  +hk2 = L.subst(Nat, t => {Nat.is_eq(t, 1n) == False{} : Bool}, Nat.sub(F.dexp(y), F.dexp(x)), Nat.sub(SF.xexp(y), xx), xsub(x, y), hk)
716  +fl = or_ff(Nat.is_lt(S, Nat.add(mx, mx)), Bool.and(Nat.is_eq(Nat.add(mx, mx), S), False{}), big54(x, y, hlt, hk2, 1n, {==}), FR.and_f(Nat.is_eq(Nat.add(mx, mx), S)))
717  +e1 = rn_spec_far(x, y, hlt)
718  +e2 = Equal.cong(Bool, F.F64, b => SF.pick(F.F64, b, SF.round(Bool.not(s), Nat.sub(S, mx), xx), SF.round(s, mx, xx)), SF.rflip(mx, S, 0n), False{}, fl)
719  Equal.trans(F.F64, RNs(x, y), SF.rnear(s, mx, S, 0n, xx), x, e1, Equal.trans(F.F64, SF.rnear(s, mx, S, 0n, xx), SF.round(s, mx, xx), x, e2, rt(x, hfin)))
720
721def rm_zero(+x: F.F64, +y: F.F64, +hzx: {SF.is_zero(x) == True{} : Bool}, +hzy: {SF.is_zero(y) == False{} : Bool}, +hfin: {Nat.is_lt(SF.efield(x), 2047n) == True{} : Bool}) -> {RNs(x, y) == x : F.F64}:
722  +s = SF.sign(x)
723  +em = N.eq_from_is_eq(SF.mant(x), 0n, Equal.trans(Bool, Nat.is_eq(SF.mant(x), 0n), SF.is_zero(x), True{}, T.mant_z(x), hzx))
724  +a = Nat.sub(SF.xexp(x), SF.rsc(x, y))
725  +rb = SF.rb(x, y)
726  +u = SF.rsc(x, y)
727  +hmy = FL.nz_le(SF.mant(y), Equal.trans(Bool, Nat.is_eq(SF.mant(y), 0n), SF.is_zero(y), False{}, T.mant_z(y), hzy))
728  +hrb = N.succ_le_lt(0n, rb, N.le_trans(1n, SF.mant(y), rb, hmy, WW.shift_ge(Nat.sub(SF.xexp(y), SF.rsc(x, y)), SF.mant(y))))
729  +e1 = Equal.cong(Nat, F.F64, t => SF.rnear(s, Nat.mod(C.shift(a, t), rb), rb, Nat.div(C.shift(a, t), rb), u), SF.mant(x), 0n, em)
730  +e2 = Equal.cong(Nat, F.F64, t => SF.rnear(s, Nat.mod(t, rb), rb, Nat.div(t, rb), u), C.shift(a, 0n), 0n, WW.shift_zero(a))
731  +e3 = Equal.cong(Nat, F.F64, t => SF.rnear(s, t, rb, Nat.div(0n, rb), u), Nat.mod(0n, rb), 0n, mod_small(0n, rb, hrb))
732  +e4 = Equal.cong(Nat, F.F64, t => SF.rnear(s, 0n, rb, t, u), Nat.div(0n, rb), 0n, div_small(0n, rb, N.succ_le_lt(0n, rb, N.le_trans(1n, SF.mant(y), rb, FL.nz_le(SF.mant(y), Equal.trans(Bool, Nat.is_eq(SF.mant(y), 0n), SF.is_zero(y), False{}, T.mant_z(y), hzy)), WW.shift_ge(Nat.sub(SF.xexp(y), SF.rsc(x, y)), SF.mant(y))))))
733  +fl = or_ff(Nat.is_lt(rb, 0n), Bool.and(Nat.is_eq(0n, rb), False{}), N.not_lt_zero(rb), FR.and_f(Nat.is_eq(0n, rb)))
734  +e5 = Equal.cong(Bool, F.F64, b => SF.pick(F.F64, b, SF.round(Bool.not(s), Nat.sub(rb, 0n), u), SF.round(s, 0n, u)), SF.rflip(0n, rb, 0n), False{}, fl)
735  +e6 = Equal.cong(Nat, F.F64, t => SF.round(s, t, SF.xexp(x)), 0n, SF.mant(x), Equal.sym(Nat, SF.mant(x), 0n, N.eq_from_is_eq(SF.mant(x), 0n, Equal.trans(Bool, Nat.is_eq(SF.mant(x), 0n), SF.is_zero(x), True{}, T.mant_z(x), hzx))))
736  +r1 = SF.rnear(s, Nat.mod(C.shift(a, 0n), rb), rb, Nat.div(C.shift(a, 0n), rb), u)
737  +r2 = SF.rnear(s, Nat.mod(0n, rb), rb, Nat.div(0n, rb), u)
738  +r3 = SF.rnear(s, 0n, rb, Nat.div(0n, rb), u)
739  +r4 = SF.rnear(s, 0n, rb, 0n, u)
740  +r5 = SF.round(s, 0n, u)
741  +r6 = SF.round(s, 0n, SF.xexp(x))
742  Equal.trans(F.F64, RNs(x, y), r1, x, e1, Equal.trans(F.F64, r1, r2, x, e2, Equal.trans(F.F64, r2, r3, x, e3, Equal.trans(F.F64, r3, r4, x, e4, Equal.trans(F.F64, r4, r5, x, e5, Equal.trans(F.F64, r5, r6, x, {==}, Equal.trans(F.F64, r6, SF.round(s, SF.mant(x), SF.xexp(x)), x, e6, rt(x, hfin))))))))
743
744def rone_c(+x: F.F64, +y: F.F64, +h: {SF.rbad(x, y) == False{} : Bool}, +hlt: {Nat.is_lt(SF.xexp(x), SF.xexp(y)) == True{} : Bool}, +o: Bool, +ho: {Nat.is_eq(Nat.sub(F.dexp(y), F.dexp(x)), 1n) == o : Bool}) -> {F.rm_near(x, y, o) == RNs(x, y) : F.F64}:
745  match o:
746    case True{}:
747      rm_one(x, y, hlt, N.eq_from_is_eq(Nat.sub(F.dexp(y), F.dexp(x)), 1n, ho))
748    case False{}:
749      Equal.sym(F.F64, RNs(x, y), x, rm_many(x, y, hlt, ho, ok_fin(x, y, h)))
750
751def rfar_c(+x: F.F64, +y: F.F64, +h: {SF.rbad(x, y) == False{} : Bool}, +far: Bool, +hfar: {Nat.is_lt(F.dexp(x), F.dexp(y)) == far : Bool}) -> {F.rm_far(x, y, far) == RNs(x, y) : F.F64}:
752  match far:
753    case True{}:
754      rone_c(x, y, h, xlt(x, y, True{}, hfar), Nat.is_eq(Nat.sub(F.dexp(y), F.dexp(x)), 1n), {==})
755    case False{}:
756      +G = RNd(SF.sign(x), SF.xexp(x), SF.xexp(y), SF.mant(x), SF.mant(y))
757      +a1 = RNd(F.signbit(x), F.dexp(x), F.dexp(y), SW.value(F.dmant(x)), SW.value(F.dmant(y)))
758      Equal.trans(F.F64, F.rm_qr(x, y, F.fm_qr(x, y)), a1, RNs(x, y), rm_near_c(x, y, ok_zy(x, y, h)), Equal.trans(F.F64, a1, G, RNs(x, y), rnd_v(x, y), Equal.sym(F.F64, RNs(x, y), G, rn_spec_near(x, y, xlt(x, y, False{}, hfar)))))
759
760def rz_c(+x: F.F64, +y: F.F64, +h: {SF.rbad(x, y) == False{} : Bool}, +zx: Bool, +hzx: {SF.is_zero(x) == zx : Bool}) -> {F.rm_z(x, y, zx) == RNs(x, y) : F.F64}:
761  match zx:
762    case True{}:
763      Equal.sym(F.F64, RNs(x, y), x, rm_zero(x, y, hzx, ok_zy(x, y, h), ok_fin(x, y, h)))
764    case False{}:
765      rfar_c(x, y, h, Nat.is_lt(F.dexp(x), F.dexp(y)), {==})
766
767def ryi_c(+x: F.F64, +y: F.F64, +h: {SF.rbad(x, y) == False{} : Bool}, +yi: Bool) -> {F.rm_yi(x, y, yi) == SF.pick(F.F64, yi, x, RNs(x, y)) : F.F64}:
768  match yi:
769    case True{}:
770      {==}
771    case False{}:
772      Equal.trans(F.F64, F.rm_z(x, y, F.is_zero(x)), F.rm_z(x, y, SF.is_zero(x)), RNs(x, y), Equal.cong(Bool, F.F64, t => F.rm_z(x, y, t), F.is_zero(x), SF.is_zero(x), FB.is_zero_value(x)), rz_c(x, y, h, SF.is_zero(x), {==}))
773
774def rb_c(+x: F.F64, +y: F.F64, +bad: Bool, +h: {SF.rbad(x, y) == bad : Bool}) -> {F.rm_bad(x, y, bad) == SF.pick(F.F64, bad, SF.qnan(), SF.pick(F.F64, SF.is_inf(y), x, RNs(x, y))) : F.F64}:
775  match bad:
776    case True{}:
777      {==}
778    case False{}:
779      Equal.trans(F.F64, F.rm_yi(x, y, F.is_inf(y)), F.rm_yi(x, y, SF.is_inf(y)), SF.pick(F.F64, SF.is_inf(y), x, RNs(x, y)), Equal.cong(Bool, F.F64, t => F.rm_yi(x, y, t), F.is_inf(y), SF.is_inf(y), FB.is_inf_value(y)), ryi_c(x, y, h, SF.is_inf(y)))
780
781def remainder_value(+x: F.F64, +y: F.F64) -> SF.Remainder.value(x, y):
782  +e1 = Equal.cong(Bool, F.F64, t => F.rm_bad(x, y, t), Bool.or(Bool.or(F.unordered(x, y), F.is_inf(x)), F.is_zero(y)), SF.rbad(x, y), badv(x, y))
783  Equal.trans(F.F64, F.remainder(x, y), F.rm_bad(x, y, SF.rbad(x, y)), SF.remainder(x, y), e1, rb_c(x, y, SF.rbad(x, y), {==}))