~/jendhub

proofs/math/typed/f64conv.bend

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