~/jendhub

proofs/math/typed/f64exp.bend

bend-collections-laws-math@1.0.0.0 · 256 lines · 23 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/natural.bend as M
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/lemmas/proofs/nat_algebra.bend as NA
11import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
12import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH
13import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64clz.bend as CZ
14import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB
15import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR
16import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW
17import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
18import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bl.bend as BL
19import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend as RT
20import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64tools.bend as T
21import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rint.bend as RI
22
23# frexp and ldexp (python_style_math_stdlib_design.pdf 4.4; C99 7.12.6.4,
24# 7.12.6.6 and F.9.3.4, F.9.3.6): Frexp.value, Ldexp.value. frexp rounds
25# the significand at the scale Z - bit_length (exact: f64tools.rw_value with
26# Clz.value for the bit length); ldexp rounds the significand at the moved
27# scale, and a scale below the subnormal range by more than the significand
28# is a zero of x's sign (tiny below: Flocq's round_NE of a value under half
29# the smallest subnormal).
30
31# ---- underflow to zero ----
32
33def sub_le_self(+a: Nat, +b: Nat) -> {Nat.is_le(Nat.sub(a, b), a) == True{} : Bool}:
34  match a b:
35    case 0n 0n:
36      {==}
37    case 0n 1n+ +bp:
38      {==}
39    case 1n+ +ap 0n:
40      N.le_refl(1n+ap)
41    case 1n+ +ap 1n+ +bp:
42      N.le_trans(Nat.sub(ap, bp), ap, 1n+ap, sub_le_self(ap, bp), N.le_succ(ap))
43
44# m < 2^53 divided by 2^(1+j) >= 2^54 rounds to 0
45def rne_zero(+m: Nat, +j: Nat, +hm: {C.fits(53n, m) == True{} : Bool}, +hj: {Nat.is_le(53n, j) == True{} : Bool}) -> {SF.rne(m, 1n+j) == 0n : Nat}:
46  +hj1 = N.le_trans(53n, j, 1n+j, hj, N.le_succ(j))
47  +f1 = SH.fits_mono(53n, 1n+j, m, hj1, hm)
48  +eh = N.eq_from_is_eq(C.high(1n+j, m), 0n, f1)
49  +el = WW.low_fit(1n+j, m, SH.fits_mono(53n, 1n+j, m, N.le_trans(53n, j, 1n+j, hj, N.le_succ(j)), hm))
50  +fj = SH.fits_mono(53n, j, m, hj, hm)
51  +hl = Equal.trans(Bool, Nat.is_lt(m, C.shift(j, 1n)), C.fits(j, m), True{}, FR.lt_fit(j, 1n, {==}, m), fj)
52  +la = RI.nlt(j, 1n, {==}, m, SH.fits_mono(53n, j, m, hj, hm))
53  +le = N.is_eq_lt(m, C.shift(j, 1n), hl)
54  +H = C.shift(j, 1n)
55  +e1 = Equal.cong(Nat, Nat, t => SF.rne_up(t, C.low(1n+j, m), H), C.high(1n+j, m), 0n, eh)
56  +e2 = Equal.cong(Nat, Nat, t => SF.rne_up(0n, t, H), C.low(1n+j, m), m, el)
57  +e3 = Equal.cong(Bool, Nat, b => Nat.add(0n, SF.b2n(Bool.or(b, Bool.and(Nat.is_eq(m, H), False{})))), Nat.is_lt(H, m), False{}, la)
58  +e4 = Equal.cong(Bool, Nat, b => SF.b2n(Bool.and(b, False{})), Nat.is_eq(m, H), False{}, le)
59  Equal.trans(Nat, SF.rne(m, 1n+j), SF.rne_up(0n, C.low(1n+j, m), H), 0n, e1, Equal.trans(Nat, SF.rne_up(0n, C.low(1n+j, m), H), SF.rne_up(0n, m, H), 0n, e2, Equal.trans(Nat, SF.rne_up(0n, m, H), SF.b2n(Bool.and(Nat.is_eq(m, H), False{})), 0n, e3, e4)))
60
61def max_le(+a: Nat, +b: Nat, +h: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.max(a, b) == b : Nat}:
62  match a b:
63    case 0n _:
64      {==}
65    case 1n+ +ap 0n:
66      Empty.absurd({Nat.max(1n+ap, 0n) == 0n : Nat}, LW.true_ne_false(Equal.sym(Bool, False{}, True{}, h)))
67    case 1n+ +ap 1n+ +bp:
68      Equal.cong(Nat, Nat, z => 1n+z, Nat.max(ap, bp), bp, max_le(ap, bp, h))
69
70# a zero pattern with sign s (as f64addc.bz)
71def bz0(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +c: U32, +hc: {c == U32{WD.pw(32n, 31n)} : U32}) -> {F.Bits{0, U32.from_nat(C.shift(31n, SF.pick(Nat, s, one, 0n)))} == SF.pick(F.F64, s, F.Bits{0, c}, F.Bits{0, 0}) : F.F64}:
72  match s:
73    case True{}:
74      Equal.cong(U32, F.F64, z => F.Bits{0, z}, U32.from_nat(C.shift(31n, one)), c, Equal.trans(U32, U32.from_nat(C.shift(31n, one)), U32.from_nat(U32.to_nat(c)), c, Equal.cong(Nat, U32, z => U32.from_nat(z), C.shift(31n, one), U32.to_nat(c), Equal.sym(Nat, U32.to_nat(c), C.shift(31n, one), FB.pwv(31n, {==}, one, h1, c, hc))), LW.rt(c)))
75    case False{}:
76      {==}
77
78def bz(+s: Bool) -> {FR.bits(s, 0n) == SF.zero(s) : F.F64}:
79  Equal.trans(F.F64, F.Bits{0, U32.from_nat(C.shift(31n, SF.b2n(s)))}, F.Bits{0, U32.from_nat(C.shift(31n, SF.pick(Nat, s, 1n, 0n)))}, SF.zero(s), Equal.cong(Nat, F.F64, z => F.Bits{0, U32.from_nat(C.shift(31n, z))}, SF.b2n(s), SF.pick(Nat, s, 1n, 0n), Equal.sym(Nat, SF.pick(Nat, s, 1n, 0n), SF.b2n(s), FR.pb(s, 1n, {==}))), bz0(1n, {==}, s, 2147483648, {==}))
80
81# round_u unfolded at an abstract ulp u: instantiated at a literal u, the
82# checker never evaluates pack's closed exponent arithmetic
83def ru(+s: Bool, +m: Nat, +x: Nat, +u: Nat) -> {SF.round_u(s, m, x, u) == SF.pack(s, SF.pick(Nat, Nat.is_le(x, u), SF.rne(m, Nat.sub(u, x)), C.shift(Nat.sub(x, u), m)), u) : F.F64}:
84  {==}
85
86def tiny_c(+s: Bool, +m: Nat, +x: Nat, +hm: {C.fits(53n, m) == True{} : Bool}, +hx: {Nat.is_lt(x, 63n) == True{} : Bool}, +z: Bool, +hz: {Nat.is_eq(m, 0n) == z : Bool}) -> {SF.round(s, m, x) == SF.zero(s) : F.F64}:
87  match z:
88    case True{}:
89      Equal.cong(Bool, F.F64, b => SF.pick(F.F64, b, SF.zero(s), SF.round_u(s, m, x, Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), 1926n))), Nat.is_eq(m, 0n), True{}, hz)
90    case False{}:
91      +B = M.bit_length(m)
92      +A = Nat.sub(Nat.add(x, B), 53n)
93      +hB = BL.bl_le(53n, m, hm, Nat.is_le(B, 53n), {==})
94      +hx62 = N.lt_succ_le(x, 62n, hx)
95      +h1 = Equal.trans(Bool, Nat.is_le(Nat.add(x, B), Nat.add(62n, B)), Nat.is_le(x, 62n), True{}, FR.le_cancel_r(x, 62n, B), hx62)
96      +h2 = N.le_trans(B, 53n, 1864n, hB, {==})
97      +hA = N.le_trans(A, Nat.add(x, B), 1926n, sub_le_self(Nat.add(x, B), 53n), N.le_trans(Nat.add(x, B), Nat.add(62n, B), 1926n, h1, h2))
98      +emax = max_le(A, 1926n, hA)
99      +hxa = N.le_trans(x, 62n, 1926n, N.lt_succ_le(x, 62n, hx), {==})
100      +hxb = N.le_trans(x, 62n, 1925n, N.lt_succ_le(x, 62n, hx), {==})
101      +j = Nat.sub(1925n, x)
102      +hj = RT.le_sub(53n, x, 1925n, N.le_trans(x, 62n, 1872n, N.lt_succ_le(x, 62n, hx), {==}))
103      +P = SF.pick(Nat, Nat.is_le(x, 1926n), SF.rne(m, Nat.sub(1926n, x)), C.shift(Nat.sub(x, 1926n), m))
104      +e1 = Equal.cong(Bool, F.F64, b => SF.pick(F.F64, b, SF.zero(s), SF.round_u(s, m, x, Nat.max(A, 1926n))), Nat.is_eq(m, 0n), False{}, hz)
105      +e2 = Equal.cong(Nat, F.F64, u => SF.round_u(s, m, x, u), Nat.max(A, 1926n), 1926n, emax)
106      # the pick reduces under pack's argument, so the checker never unfolds pack
107      +e3p = Equal.cong(Bool, Nat, b => SF.pick(Nat, b, SF.rne(m, Nat.sub(1926n, x)), C.shift(Nat.sub(x, 1926n), m)), Nat.is_le(x, 1926n), True{}, hxa)
108      +e3 = Equal.cong(Nat, F.F64, t => SF.pack(s, t, 1926n), SF.pick(Nat, Nat.is_le(x, 1926n), SF.rne(m, Nat.sub(1926n, x)), C.shift(Nat.sub(x, 1926n), m)), SF.rne(m, Nat.sub(1926n, x)), e3p)
109      +e4 = Equal.cong(Nat, F.F64, t => SF.pack(s, SF.rne(m, t), 1926n), Nat.sub(1926n, x), 1n+j, N.sub_succ_left(1925n, x, hxb))
110      +e5 = Equal.cong(Nat, F.F64, t => SF.pack(s, t, 1926n), SF.rne(m, 1n+j), 0n, rne_zero(m, j, hm, hj))
111      +e6 = FR.enc_bits(s, 0n, 0n)
112      +r1 = SF.round_u(s, m, x, Nat.max(A, 1926n))
113      +r2 = SF.round_u(s, m, x, 1926n)
114      +r3 = SF.pack(s, SF.rne(m, Nat.sub(1926n, x)), 1926n)
115      +r4 = SF.pack(s, SF.rne(m, 1n+j), 1926n)
116      +r5 = SF.pack(s, 0n, 1926n)
117      +r6 = FR.bits(s, 0n)
118      +r2p = SF.pack(s, SF.pick(Nat, Nat.is_le(x, 1926n), SF.rne(m, Nat.sub(1926n, x)), C.shift(Nat.sub(x, 1926n), m)), 1926n)
119      Equal.trans(F.F64, SF.round(s, m, x), r1, SF.zero(s), e1, Equal.trans(F.F64, r1, r2, SF.zero(s), e2, Equal.trans(F.F64, r2, r2p, SF.zero(s), ru(s, m, x, 1926n), Equal.trans(F.F64, r2p, r3, SF.zero(s), e3, Equal.trans(F.F64, r3, r4, SF.zero(s), e4, Equal.trans(F.F64, r4, r5, SF.zero(s), e5, Equal.trans(F.F64, r5, r6, SF.zero(s), e6, bz(s))))))))
120
121def tiny(+s: Bool, +m: Nat, +x: Nat, +hm: {C.fits(53n, m) == True{} : Bool}, +hx: {Nat.is_lt(x, 63n) == True{} : Bool}) -> {SF.round(s, m, x) == SF.zero(s) : F.F64}:
122  tiny_c(s, m, x, hm, hx, Nat.is_eq(m, 0n), {==})
123
124# ---- frexp ----
125
126def ee_c(+t: Nat, +c: Bool) -> {F.exp_pick(t, c) == SF.pick(F.Exp, c, F.Exp{False{}, Nat.sub(t, 3000n)}, F.Exp{True{}, Nat.sub(3000n, t)}) : F.Exp}:
127  match c:
128    case True{}:
129      {==}
130    case False{}:
131      {==}
132
133def exp_eq(+t: Nat) -> {F.exp_of(t) == SF.exp_of(t) : F.Exp}:
134  ee_c(t, Nat.is_le(3000n, t))
135
136def FIN(+x: F.F64) -> F.F64 & F.Exp:
137  (SF.round(SF.sign(x), SF.mant(x), Nat.sub(SF.zb(), M.bit_length(SF.mant(x)))), SF.exp_of(Nat.add(SF.xexp(x), M.bit_length(SF.mant(x)))))
138
139def fx_nz(+x: F.F64) -> {F.fx_fin(x, F.dmant(x), Nat.sub(64n, X.clz(F.dmant(x)))) == FIN(x) : F.F64 & F.Exp}:
140  +w = F.dmant(x)
141  +V = SW.value(w)
142  +B = M.bit_length(V)
143  +hB = BL.bl_le(53n, V, T.mw53(x), Nat.is_le(B, 53n), {==})
144  +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)), T.subsub(64n, B, N.le_trans(B, 53n, 64n, hB, {==})))
145  +e0 = Equal.cong(Nat, F.F64 & F.Exp, b => F.fx_fin(x, w, b), Nat.sub(64n, X.clz(w)), B, eb)
146  +hx = RT.le_sub(63n, B, 3000n, N.le_trans(B, 53n, 2937n, BL.bl_le(53n, V, T.mw53(x), Nat.is_le(B, 53n), {==}), {==}))
147  +a1 = T.rw_value(F.signbit(x), Nat.sub(3000n, B), w, hx)
148  +a2 = Equal.cong(Bool, F.F64, t => SF.round(t, V, Nat.sub(3000n, B)), F.signbit(x), SF.sign(x), FB.signbit_value(x))
149  +a3 = Equal.cong(Nat, F.F64, t => SF.round(SF.sign(x), t, Nat.sub(3000n, M.bit_length(t))), V, SF.mant(x), T.dmant_value(x))
150  +A0 = F.round_w(F.signbit(x), Nat.sub(3000n, B), w)
151  +A1 = SF.round(F.signbit(x), V, Nat.sub(3000n, B))
152  +A2 = SF.round(SF.sign(x), V, Nat.sub(3000n, B))
153  +A3 = SF.round(SF.sign(x), SF.mant(x), Nat.sub(SF.zb(), M.bit_length(SF.mant(x))))
154  +ea = Equal.trans(F.F64, A0, A1, A3, a1, Equal.trans(F.F64, A1, A2, A3, a2, a3))
155  +b1 = exp_eq(Nat.add(F.dexp(x), B))
156  +b2 = Equal.cong(Nat, F.Exp, t => SF.exp_of(Nat.add(t, B)), F.dexp(x), SF.xexp(x), T.dexp_value(x))
157  +b3 = Equal.cong(Nat, F.Exp, t => SF.exp_of(Nat.add(SF.xexp(x), M.bit_length(t))), V, SF.mant(x), T.dmant_value(x))
158  +B0 = F.exp_of(Nat.add(F.dexp(x), B))
159  +B1 = SF.exp_of(Nat.add(F.dexp(x), B))
160  +B2 = SF.exp_of(Nat.add(SF.xexp(x), B))
161  +B3 = SF.exp_of(Nat.add(SF.xexp(x), M.bit_length(SF.mant(x))))
162  +eb2 = Equal.trans(F.Exp, B0, B1, B3, b1, Equal.trans(F.Exp, B1, B2, B3, b2, b3))
163  +p1 = Equal.cong(F.F64, F.F64 & F.Exp, t => (t, B0), A0, A3, ea)
164  +p2 = Equal.cong(F.Exp, F.F64 & F.Exp, t => (A3, t), B0, B3, eb2)
165  Equal.trans(F.F64 & F.Exp, F.fx_fin(x, w, Nat.sub(64n, X.clz(w))), F.fx_fin(x, w, B), FIN(x), e0, Equal.trans(F.F64 & F.Exp, (A0, B0), (A3, B0), FIN(x), p1, p2))
166
167def fxz_c(+x: F.F64, +iz: Bool) -> {F.fx_z(x, iz) == SF.pickt(F.F64 & F.Exp, iz, (x, F.Exp{False{}, 0n}), FIN(x)) : F.F64 & F.Exp}:
168  match iz:
169    case True{}:
170      {==}
171    case False{}:
172      fx_nz(x)
173
174def fx_c(+x: F.F64, +t: Bool, +z: Bool, +hz: {X.is_zero(F.frac(x)) == z : Bool}) -> {F.fx_cls(x, t) == SF.pickt(F.F64 & F.Exp, Bool.and(t, Bool.not(z)), (SF.qnan(), F.Exp{False{}, 0n}), SF.pickt(F.F64 & F.Exp, Bool.or(Bool.and(t, z), SF.is_zero(x)), (x, F.Exp{False{}, 0n}), FIN(x))) : F.F64 & F.Exp}:
175  match t z:
176    case True{} True{}:
177      Equal.cong(Bool, F.F64 & F.Exp, b => (F.nan_or(x, Bool.not(b)), F.Exp{False{}, 0n}), X.is_zero(F.frac(x)), True{}, hz)
178    case True{} False{}:
179      Equal.cong(Bool, F.F64 & F.Exp, b => (F.nan_or(x, Bool.not(b)), F.Exp{False{}, 0n}), X.is_zero(F.frac(x)), False{}, hz)
180    case False{} _:
181      +e1 = Equal.cong(Bool, F.F64 & F.Exp, b => F.fx_z(x, b), F.is_zero(x), SF.is_zero(x), FB.is_zero_value(x))
182      Equal.trans(F.F64 & F.Exp, F.fx_z(x, F.is_zero(x)), F.fx_z(x, SF.is_zero(x)), SF.pickt(F.F64 & F.Exp, SF.is_zero(x), (x, F.Exp{False{}, 0n}), FIN(x)), e1, fxz_c(x, SF.is_zero(x)))
183
184def frexp_value(+x: F.F64) -> SF.Frexp.value(x):
185  +e1 = Equal.cong(Nat, F.F64 & F.Exp, u => F.fx_cls(x, Nat.is_eq(u, 2047n)), F.exp_field(x), SF.efield(x), T.ea(x))
186  Equal.trans(F.F64 & F.Exp, F.frexp(x), F.fx_cls(x, Nat.is_eq(SF.efield(x), 2047n)), SF.frexp(x), e1, fx_c(x, Nat.is_eq(SF.efield(x), 2047n), Nat.is_eq(SF.frac(x), 0n), T.fz(x)))
187
188# ---- ldexp ----
189
190def LD(+x: F.F64, +neg: Bool, +k: Nat) -> F.F64:
191  SF.round(SF.sign(x), SF.mant(x), SF.pick(Nat, neg, Nat.sub(SF.xexp(x), k), Nat.add(SF.xexp(x), k)))
192
193# the round_w of the significand at scale u is the spec's round at u
194def rwx(+x: F.F64, +u: Nat, +hu: {Nat.is_le(63n, u) == True{} : Bool}) -> {F.round_w(F.signbit(x), u, F.dmant(x)) == SF.round(SF.sign(x), SF.mant(x), u) : F.F64}:
195  +a1 = T.rw_value(F.signbit(x), u, F.dmant(x), hu)
196  +a2 = Equal.cong(Bool, F.F64, t => SF.round(t, SW.value(F.dmant(x)), u), F.signbit(x), SF.sign(x), FB.signbit_value(x))
197  +a3 = Equal.cong(Nat, F.F64, t => SF.round(SF.sign(x), t, u), SW.value(F.dmant(x)), SF.mant(x), T.dmant_value(x))
198  Equal.trans(F.F64, F.round_w(F.signbit(x), u, F.dmant(x)), SF.round(F.signbit(x), SW.value(F.dmant(x)), u), SF.round(SF.sign(x), SF.mant(x), u), a1, Equal.trans(F.F64, SF.round(F.signbit(x), SW.value(F.dmant(x)), u), SF.round(SF.sign(x), SW.value(F.dmant(x)), u), SF.round(SF.sign(x), SF.mant(x), u), a2, a3))
199
200# a - k < 63 when a < k + 63
201def slt(+a: Nat, +k: Nat, +h: {Nat.is_lt(a, Nat.add(k, 63n)) == True{} : Bool}) -> {Nat.is_lt(Nat.sub(a, k), 63n) == True{} : Bool}:
202  match a k:
203    case 0n 0n:
204      {==}
205    case 0n 1n+ +kp:
206      {==}
207    case 1n+ +ap 0n:
208      h
209    case 1n+ +ap 1n+ +kp:
210      slt(ap, kp, h)
211
212def ldn_c(+x: F.F64, +k: Nat, +c: Bool, +hc: {Nat.is_lt(F.dexp(x), Nat.add(k, 63n)) == c : Bool}) -> {F.ld_neg(x, k, c) == LD(x, True{}, k) : F.F64}:
213  match c:
214    case True{}:
215      +h1 = L.subst(Nat, t => {Nat.is_lt(t, Nat.add(k, 63n)) == True{} : Bool}, F.dexp(x), SF.xexp(x), T.dexp_value(x), hc)
216      +et = tiny(SF.sign(x), SF.mant(x), Nat.sub(SF.xexp(x), k), T.mant_fits(x), slt(SF.xexp(x), k, h1))
217      +ez = Equal.trans(F.F64, F.zero(F.signbit(x)), SF.zero(F.signbit(x)), SF.zero(SF.sign(x)), T.zero_v(F.signbit(x)), Equal.cong(Bool, F.F64, t => SF.zero(t), F.signbit(x), SF.sign(x), FB.signbit_value(x)))
218      Equal.trans(F.F64, F.zero(F.signbit(x)), SF.zero(SF.sign(x)), LD(x, True{}, k), ez, Equal.sym(F.F64, LD(x, True{}, k), SF.zero(SF.sign(x)), et))
219    case False{}:
220      +h0 = N.not_lt_le(F.dexp(x), Nat.add(k, 63n), hc)
221      +h1 = L.subst(Nat, t => {Nat.is_le(t, F.dexp(x)) == True{} : Bool}, Nat.add(k, 63n), Nat.add(63n, k), NA.add_comm(k, 63n), h0)
222      +hu = RT.le_sub(63n, k, F.dexp(x), h1)
223      +e1 = rwx(x, Nat.sub(F.dexp(x), k), hu)
224      +e2 = Equal.cong(Nat, F.F64, t => SF.round(SF.sign(x), SF.mant(x), Nat.sub(t, k)), F.dexp(x), SF.xexp(x), T.dexp_value(x))
225      Equal.trans(F.F64, F.round_w(F.signbit(x), Nat.sub(F.dexp(x), k), F.dmant(x)), SF.round(SF.sign(x), SF.mant(x), Nat.sub(F.dexp(x), k)), LD(x, True{}, k), e1, e2)
226
227def ldf_c(+x: F.F64, +neg: Bool, +k: Nat) -> {F.ld_fin(x, neg, k) == LD(x, neg, k) : F.F64}:
228  match neg:
229    case True{}:
230      ldn_c(x, k, Nat.is_lt(F.dexp(x), Nat.add(k, 63n)), {==})
231    case False{}:
232      +hu = N.le_trans(63n, F.dexp(x), Nat.add(F.dexp(x), k), T.dexp_ge(x), N.le_add_right(F.dexp(x), k))
233      +e1 = rwx(x, Nat.add(F.dexp(x), k), hu)
234      +e2 = Equal.cong(Nat, F.F64, t => SF.round(SF.sign(x), SF.mant(x), Nat.add(t, k)), F.dexp(x), SF.xexp(x), T.dexp_value(x))
235      Equal.trans(F.F64, F.round_w(F.signbit(x), Nat.add(F.dexp(x), k), F.dmant(x)), SF.round(SF.sign(x), SF.mant(x), Nat.add(F.dexp(x), k)), LD(x, False{}, k), e1, e2)
236
237def ldz_c(+x: F.F64, +neg: Bool, +k: Nat, +iz: Bool) -> {F.ld_z(x, F.Exp{neg, k}, iz) == SF.pick(F.F64, iz, x, LD(x, neg, k)) : F.F64}:
238  match iz:
239    case True{}:
240      {==}
241    case False{}:
242      ldf_c(x, neg, k)
243
244def ld_c(+x: F.F64, +neg: Bool, +k: Nat, +t: Bool, +z: Bool, +hz: {X.is_zero(F.frac(x)) == z : Bool}) -> {F.ld_cls(x, F.Exp{neg, k}, t) == SF.pick(F.F64, Bool.and(t, Bool.not(z)), SF.qnan(), SF.pick(F.F64, Bool.or(Bool.and(t, z), SF.is_zero(x)), x, LD(x, neg, k))) : F.F64}:
245  match t z:
246    case True{} True{}:
247      Equal.cong(Bool, F.F64, b => F.nan_or(x, Bool.not(b)), X.is_zero(F.frac(x)), True{}, hz)
248    case True{} False{}:
249      Equal.cong(Bool, F.F64, b => F.nan_or(x, Bool.not(b)), X.is_zero(F.frac(x)), False{}, hz)
250    case False{} _:
251      +e1 = Equal.cong(Bool, F.F64, b => F.ld_z(x, F.Exp{neg, k}, b), F.is_zero(x), SF.is_zero(x), FB.is_zero_value(x))
252      Equal.trans(F.F64, F.ld_z(x, F.Exp{neg, k}, F.is_zero(x)), F.ld_z(x, F.Exp{neg, k}, SF.is_zero(x)), SF.pick(F.F64, SF.is_zero(x), x, LD(x, neg, k)), e1, ldz_c(x, neg, k, SF.is_zero(x)))
253
254def ldexp_value(+x: F.F64, +neg: Bool, +k: Nat) -> SF.Ldexp.value(x, neg, k):
255  +e1 = Equal.cong(Nat, F.F64, u => F.ld_cls(x, F.Exp{neg, k}, Nat.is_eq(u, 2047n)), F.exp_field(x), SF.efield(x), T.ea(x))
256  Equal.trans(F.F64, F.ldexp(x, F.Exp{neg, k}), F.ld_cls(x, F.Exp{neg, k}, Nat.is_eq(SF.efield(x), 2047n)), SF.ldexp(x, neg, k), e1, ld_c(x, neg, k, Nat.is_eq(SF.efield(x), 2047n), Nat.is_eq(SF.frac(x), 0n), T.fz(x)))