proofs/math/random/float.bend

bend-collections-laws-math@1.0.0.0 · 460 lines · 48 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/w64.bend as SW
4import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
5import bend-collections-laws-math@1.0.0.0/spec/math/random.bend as SR
6import bend-collections-laws-math@1.0.0.0/src/math/random/rand.bend as R
7import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
8import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
9import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
10import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
11import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
12import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
13import bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend as U
14import bend-collections-laws-math@1.0.0.0/proofs/math/natural/bits.bend as NB
15import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
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/math/typed/w64sh.bend as SH
18import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64clz.bend as WC
19import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
20import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB
21import bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend as FR
22
23# Float64.value and Float64.lt_one of spec/math/random.bend: Go's Float64,
24# float64(x << 11 >> 11) / 2^53, built by src/math/random/rand.bend's
25# to_float as the bit pattern of m * 2^-53 (m the low 53 bits of x), is the
26# double spec/math/f64.bend's round gives for m * 2^-53, and is below 1.
27# For m > 0 with bit length 1 + j (j <= 52), the significand is
28# q = m * 2^(52 - j) in [2^52, 2^53) and the exponent field 970 + j <= 1022.
29# No constant 2^k is ever expanded: widths stay symbolic (C.fits, C.low,
30# C.high, C.shift) and U32 constants are read through their words.
31
32def v(+x: U32) -> Nat:
33  U32.to_nat(x)
34
35# ---- natural-number arithmetic ----
36
37# 63 - j = 11 + (52 - j)
38def sub63(+j: Nat, +hj: {Nat.is_le(j, 52n) == True{} : Bool}) -> {Nat.sub(63n, j) == Nat.add(11n, Nat.sub(52n, j)) : Nat}:
39  +r = Nat.sub(52n, j)
40  +e1 = N.sub_add(52n, j, hj)
41  +e2 = Equal.trans(Nat, Nat.add(j, Nat.add(11n, r)), Nat.add(Nat.add(11n, r), j), 63n, N.add_comm(j, Nat.add(11n, r)), Equal.cong(Nat, Nat, z => Nat.add(11n, z), Nat.add(r, j), 52n, Equal.trans(Nat, Nat.add(r, j), Nat.add(j, r), 52n, N.add_comm(r, j), e1)))
42  %e2 : {Nat.sub(_, j) == Nat.add(11n, r) : Nat}
43  N.add_sub_cancel(j, Nat.add(11n, r))
44
45# the shift of the implementation: clz - 11 = 52 - j
46def shift_amt(+j: Nat, +hj: {Nat.is_le(j, 52n) == True{} : Bool}) -> {Nat.sub(Nat.sub(63n, j), 11n) == Nat.sub(52n, j) : Nat}:
47  %Equal.sym(Nat, Nat.sub(63n, j), Nat.add(11n, Nat.sub(52n, j)), sub63(j, hj)) : {Nat.sub(_, 11n) == Nat.sub(52n, j) : Nat}
48  N.sub_zero(Nat.sub(52n, j))
49
50# the exponent field of the implementation: 1033 - clz = 970 + j
51def exp_amt0(+j: Nat, +hj: {Nat.is_le(j, 52n) == True{} : Bool}) -> {Nat.sub(1033n, Nat.sub(63n, j)) == Nat.add(970n, j) : Nat}:
52  +r = Nat.sub(52n, j)
53  +e1 = N.sub_add(52n, j, hj)
54  +e3 = Equal.trans(Nat, Nat.add(r, Nat.add(970n, j)), Nat.add(Nat.add(970n, j), r), 1022n, N.add_comm(r, Nat.add(970n, j)), Equal.cong(Nat, Nat, z => Nat.add(970n, z), Nat.add(j, r), 52n, e1))
55  %Equal.sym(Nat, Nat.sub(63n, j), Nat.add(11n, r), sub63(j, hj)) : {Nat.sub(1033n, _) == Nat.add(970n, j) : Nat}
56  %e3 : {Nat.sub(_, r) == Nat.add(970n, j) : Nat}
57  N.add_sub_cancel(r, Nat.add(970n, j))
58
59def exp_amt(+j: Nat, +hj: {Nat.is_le(j, 52n) == True{} : Bool}) -> {Nat.sub(1033n, Nat.sub(63n, j)) == Nat.add(j, 970n) : Nat}:
60  Equal.trans(Nat, Nat.sub(1033n, Nat.sub(63n, j)), Nat.add(970n, j), Nat.add(j, 970n), exp_amt0(j, hj), N.add_comm(970n, j))
61
62# ---- widths ----
63
64def fits0(+a: Nat) -> {C.fits(a, 0n) == True{} : Bool}:
65  %Equal.sym(Nat, C.high(a, 0n), 0n, WC.high0(a)) : {Nat.is_eq(_, 0n) == True{} : Bool}
66  {==}
67
68def fits_up(+a: Nat, +d: Nat, +x: Nat, +h: {C.fits(a, x) == True{} : Bool}) -> {C.fits(Nat.add(a, d), x) == True{} : Bool}:
69  +e = N.eq_from_is_eq(C.high(a, x), 0n, h)
70  %Equal.sym(Nat, C.high(Nat.add(a, d), x), C.high(d, C.high(a, x)), WW.high_comp(d, a, x)) : {Nat.is_eq(_, 0n) == True{} : Bool}
71  %Equal.sym(Nat, C.high(a, x), 0n, e) : {Nat.is_eq(C.high(d, _), 0n) == True{} : Bool}
72  fits0(d)
73
74# x < 2^k gives x 2^a < 2^(a + k)
75def fits_shift(+a: Nat, +k: Nat, +x: Nat, +h: {C.fits(k, x) == True{} : Bool}) -> {C.fits(Nat.add(a, k), C.shift(a, x)) == True{} : Bool}:
76  WW.limbs_fit(a, k, 0n, x, fits0(a), h)
77
78def fits_lt11(+e: Nat, +h: {Nat.is_lt(e, 2048n) == True{} : Bool}) -> {C.fits(11n, e) == True{} : Bool}:
79  WW.fits_of_lt(11n, e, h)
80
81# ---- the high word ----
82
83# the high word the implementation builds: exponent field e, and the top 20
84# fraction bits of qh
85def hw(+e: Nat, +qh: U32) -> U32:
86  U32.add(U32.mul(U32.from_nat(e), 1048576), U32.and(qh, 1048575))
87
88def bits(+q: WU.U64, +e: Nat) -> F.F64:
89  F.Bits{X.lo(q), hw(e, X.hi(q))}
90
91def f12(+e: Nat, +he: {Nat.is_lt(e, 2048n) == True{} : Bool}) -> {C.fits(12n, e) == True{} : Bool}:
92  fits_up(11n, 1n, e, fits_lt11(e, he))
93
94# its value: 2^20 e + (qh mod 2^20), for e < 2^11
95def hw_value(+one: Nat, +h1: {one == 1n : Nat}, +e: Nat, +qh: U32, +he: {Nat.is_lt(e, 2048n) == True{} : Bool}) -> {v(hw(e, qh)) == Nat.add(C.low(20n, v(qh)), C.shift(20n, e)) : Nat}:
96  +a = U32.mul(U32.from_nat(e), 1048576)
97  +b = U32.and(qh, 1048575)
98  +lq = C.low(20n, v(qh))
99  +se = C.shift(20n, e)
100  +ve = U.to_nat_from_nat(e, 11n, {==}, he)
101  +f32 = fits_shift(20n, 12n, e, f12(e, he))
102  +va = Equal.trans(Nat, v(a), C.low(32n, C.shift(20n, v(U32.from_nat(e)))), se, SH.mul_p2(U32.from_nat(e), 20n, {==}),
103    Equal.trans(Nat, C.low(32n, C.shift(20n, v(U32.from_nat(e)))), C.low(32n, se), se, Equal.cong(Nat, Nat, z => C.low(32n, C.shift(20n, z)), v(U32.from_nat(e)), e, ve), WW.low_fit(32n, se, f32)))
104  +vb = FB.andm(qh, 20n, 1048575, {==})
105  +e12 = Equal.trans(Nat, Nat.add(v(a), v(b)), Nat.add(se, v(b)), Nat.add(se, lq), Equal.cong(Nat, Nat, z => Nat.add(z, v(b)), v(a), se, va), Equal.cong(Nat, Nat, z => Nat.add(se, z), v(b), lq, vb))
106  +e13 = Equal.trans(Nat, Nat.add(v(a), v(b)), Nat.add(se, lq), Nat.add(lq, se), e12, N.add_comm(se, lq))
107  +fs3 = WW.limbs_fit(20n, 12n, lq, e, WW.low_fits(20n, v(qh)), f12(e, he))
108  +fs1 = L.subst(Nat, z => {C.fits(32n, z) == True{} : Bool}, Nat.add(lq, se), Nat.add(v(a), v(b)), Equal.sym(Nat, Nat.add(v(a), v(b)), Nat.add(lq, se), e13), fs3)
109  Equal.trans(Nat, v(U32.add(a, b)), Nat.add(v(a), v(b)), Nat.add(lq, se), FB.addv(one, h1, a, b, WW.lt_one(32n, one, h1, Nat.add(v(a), v(b)), fs1)), e13)
110
111def value_eta(+q: WU.U64) -> {SW.value(q) == Nat.add(v(X.lo(q)), C.shift(32n, v(X.hi(q)))) : Nat}:
112  match q:
113    case WU.U64{l, h}:
114      {==}
115
116# the implementation's bits are encode(False, e, q mod 2^52) for the value
117# q < 2^53 of the shifted significand
118def enc(+one: Nat, +h1: {one == 1n : Nat}, +Q: WU.U64, +e: Nat, +he: {Nat.is_lt(e, 2048n) == True{} : Bool}, +q: Nat, +hq: {SW.value(Q) == q : Nat}, +f53: {C.fits(53n, q) == True{} : Bool}) -> {bits(Q, e) == SF.encode(False{}, e, C.low(52n, q)) : F.F64}:
119  +ql = X.lo(Q)
120  +qh = X.hi(Q)
121  +lq = C.low(20n, v(qh))
122  +hq2 = Equal.trans(Nat, q, SW.value(Q), Nat.add(v(ql), C.shift(32n, v(qh))), Equal.sym(Nat, SW.value(Q), q, hq), value_eta(Q))
123  +f = C.low(52n, q)
124  +F1 = Nat.add(v(ql), C.shift(32n, lq))
125  +s1 = FB.low_split(32n, 20n, q)
126  +el = Equal.trans(Nat, C.low(32n, q), C.low(32n, Nat.add(v(ql), C.shift(32n, v(qh)))), v(ql), Equal.cong(Nat, Nat, z => C.low(32n, z), q, Nat.add(v(ql), C.shift(32n, v(qh))), hq2), WW.low_u(32n, v(ql), v(qh), LW.vb(ql)))
127  +eh = Equal.trans(Nat, C.high(32n, q), C.high(32n, Nat.add(v(ql), C.shift(32n, v(qh)))), v(qh), Equal.cong(Nat, Nat, z => C.high(32n, z), q, Nat.add(v(ql), C.shift(32n, v(qh))), hq2), WW.high_u(32n, v(ql), v(qh), LW.vb(ql)))
128  +ef1 = Equal.trans(Nat, f, Nat.add(C.low(32n, q), C.shift(32n, C.low(20n, C.high(32n, q)))), F1, s1,
129    Equal.trans(Nat, Nat.add(C.low(32n, q), C.shift(32n, C.low(20n, C.high(32n, q)))), Nat.add(v(ql), C.shift(32n, C.low(20n, C.high(32n, q)))), F1, Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(32n, C.low(20n, C.high(32n, q)))), C.low(32n, q), v(ql), el),
130      Equal.cong(Nat, Nat, z => Nat.add(v(ql), C.shift(32n, C.low(20n, z))), C.high(32n, q), v(qh), eh)))
131  +elo = Equal.trans(Nat, C.low(32n, f), C.low(32n, F1), v(ql), Equal.cong(Nat, Nat, z => C.low(32n, z), f, F1, ef1), WW.low_u(32n, v(ql), lq, LW.vb(ql)))
132  +ehi0 = Equal.trans(Nat, C.high(32n, f), C.high(32n, F1), lq, Equal.cong(Nat, Nat, z => C.high(32n, z), f, F1, ef1), WW.high_u(32n, v(ql), lq, LW.vb(ql)))
133  +T = Nat.add(e, C.shift(11n, SF.b2n(False{})))
134  +ehi1 = Equal.trans(Nat, Nat.add(C.high(32n, f), C.shift(20n, T)), Nat.add(lq, C.shift(20n, T)), Nat.add(lq, C.shift(20n, e)), Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(20n, T)), C.high(32n, f), lq, ehi0), Equal.cong(Nat, Nat, z => Nat.add(lq, C.shift(20n, z)), T, e, N.add_zero(e)))
135  +ehi2 = Equal.trans(Nat, Nat.add(C.high(32n, f), C.shift(20n, T)), Nat.add(lq, C.shift(20n, e)), v(hw(e, qh)), ehi1, Equal.sym(Nat, v(hw(e, qh)), Nat.add(lq, C.shift(20n, e)), hw_value(one, h1, e, qh, he)))
136  +wlo = Equal.trans(U32, U32.from_nat(C.low(32n, f)), U32.from_nat(v(ql)), ql, Equal.cong(Nat, U32, z => U32.from_nat(z), C.low(32n, f), v(ql), elo), LW.rt(ql))
137  +whi = Equal.trans(U32, U32.from_nat(Nat.add(C.high(32n, f), C.shift(20n, T))), U32.from_nat(v(hw(e, qh))), hw(e, qh), Equal.cong(Nat, U32, z => U32.from_nat(z), Nat.add(C.high(32n, f), C.shift(20n, T)), v(hw(e, qh)), ehi2), LW.rt(hw(e, qh)))
138  +lo_s = U32.from_nat(C.low(32n, f))
139  +hi_s = U32.from_nat(Nat.add(C.high(32n, f), C.shift(20n, T)))
140  Equal.sym(F.F64, F.Bits{lo_s, hi_s}, F.Bits{ql, hw(e, qh)}, Equal.trans(F.F64, F.Bits{lo_s, hi_s}, F.Bits{ql, hi_s}, F.Bits{ql, hw(e, qh)}, Equal.cong(U32, F.F64, z => F.Bits{z, hi_s}, lo_s, ql, wlo), Equal.cong(U32, F.F64, z => F.Bits{ql, z}, hi_s, hw(e, qh), whi)))
141
142# ---- bit lengths ----
143
144def bl_le(+k: Nat, +n: Nat, +h: {C.fits(k, n) == True{} : Bool}) -> {Nat.is_le(M.bit_length(n), k) == True{} : Bool}:
145  match k:
146    case 0n:
147      +en = N.eq_from_is_eq(n, 0n, h)
148      %Equal.sym(Nat, n, 0n, en) : {Nat.is_le(M.bit_length(_), 0n) == True{} : Bool}
149      {==}
150    case 1n+ +kp:
151      match n:
152        case 0n:
153          {==}
154        case 1n+ +np:
155          %Equal.sym(Nat, M.bit_length(1n+np), 1n+M.bit_length(C.half(1n+np)), WC.bl_succ(np)) : {Nat.is_le(_, 1n+kp) == True{} : Bool}
156          bl_le(kp, C.half(1n+np), h)
157
158
159# ---- the rounding of spec/math/f64.bend ----
160# Exponents are kept as j + c (the variable first), so the checker never
161# unfolds them into long successor chains.
162
163def x0() -> Nat:
164  Nat.sub(SF.zb(), 53n)
165
166def max_l(+a: Nat, +b: Nat, +h: {Nat.is_le(b, a) == True{} : Bool}) -> {Nat.max(a, b) == a : Nat}:
167  match a b:
168    case 0n 0n:
169      {==}
170    case 0n 1n+bp:
171      Empty.absurd({Nat.max(0n, 1n+bp) == 0n : Nat}, L.false_true(h))
172    case 1n+ap 0n:
173      {==}
174    case 1n+ap 1n+bp:
175      Equal.cong(Nat, Nat, z => 1n+z, Nat.max(ap, bp), ap, max_l(ap, bp, h))
176
177def sub_add53(+X: Nat) -> {Nat.sub(Nat.add(X, 53n), 53n) == X : Nat}:
178  %Equal.sym(Nat, Nat.add(X, 53n), Nat.add(53n, X), N.add_comm(X, 53n)) : {Nat.sub(_, 53n) == X : Nat}
179  N.sub_zero(X)
180
181# X + r = 2947 for X = j + 2895, r = 52 - j
182def ex(+j: Nat, +hj: {Nat.is_le(j, 52n) == True{} : Bool}) -> {Nat.add(Nat.add(j, 2895n), Nat.sub(52n, j)) == x0() : Nat}:
183  +r = Nat.sub(52n, j)
184  +e1 = N.sub_add(52n, j, hj)
185  +a1 = N.add_assoc(j, 2895n, r)
186  +a2 = Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(2895n, r), Nat.add(r, 2895n), N.add_comm(2895n, r))
187  +a3 = Equal.sym(Nat, Nat.add(Nat.add(j, r), 2895n), Nat.add(j, Nat.add(r, 2895n)), N.add_assoc(j, r, 2895n))
188  +a4 = Equal.cong(Nat, Nat, z => Nat.add(z, 2895n), Nat.add(j, r), 52n, e1)
189  Equal.trans(Nat, Nat.add(Nat.add(j, 2895n), r), Nat.add(j, Nat.add(2895n, r)), x0(), a1,
190    Equal.trans(Nat, Nat.add(j, Nat.add(2895n, r)), Nat.add(j, Nat.add(r, 2895n)), x0(), a2,
191      Equal.trans(Nat, Nat.add(j, Nat.add(r, 2895n)), Nat.add(Nat.add(j, r), 2895n), x0(), a3, a4)))
192
193# round(q, X) for 2^52 <= q < 2^53 at the scale X = j + 2895 is pack(q, X)
194def round_q(+q: Nat, +j: Nat, +bq: {M.bit_length(q) == 53n : Nat}, +hz: {Nat.is_eq(q, 0n) == False{} : Bool}) -> {SF.round(False{}, q, Nat.add(j, 2895n)) == SF.pack(False{}, q, Nat.add(j, 2895n)) : F.F64}:
195  +X = Nat.add(j, 2895n)
196  +U = Nat.max(Nat.sub(Nat.add(X, M.bit_length(q)), 53n), Nat.sub(SF.zb(), 1074n))
197  +hle = Equal.trans(Bool, Nat.is_le(1926n, X), Nat.is_le(1926n, Nat.add(2895n, j)), True{}, Equal.cong(Nat, Bool, z => Nat.is_le(1926n, z), X, Nat.add(2895n, j), N.add_comm(j, 2895n)), {==})
198  +eU = Equal.trans(Nat, U, Nat.max(Nat.sub(Nat.add(X, 53n), 53n), 1926n), X, Equal.cong(Nat, Nat, z => Nat.max(Nat.sub(Nat.add(X, z), 53n), Nat.sub(SF.zb(), 1074n)), M.bit_length(q), 53n, bq),
199    Equal.trans(Nat, Nat.max(Nat.sub(Nat.add(X, 53n), 53n), 1926n), Nat.max(X, 1926n), X, Equal.cong(Nat, Nat, z => Nat.max(z, 1926n), Nat.sub(Nat.add(X, 53n), 53n), X, sub_add53(X)), max_l(X, 1926n, hle)))
200  +r1 = Equal.cong(Bool, F.F64, c => SF.pick(F.F64, c, SF.zero(False{}), SF.round_u(False{}, q, X, U)), Nat.is_eq(q, 0n), False{}, hz)
201  +r2 = Equal.cong(Nat, F.F64, z => SF.round_u(False{}, q, X, z), U, X, eU)
202  +r3 = Equal.cong(Bool, F.F64, c => SF.pack(False{}, SF.pick(Nat, c, SF.rne(q, Nat.sub(X, X)), C.shift(Nat.sub(X, X), q)), X), Nat.is_le(X, X), True{}, N.le_refl(X))
203  +r4 = Equal.cong(Nat, F.F64, z => SF.pack(False{}, SF.rne(q, z), X), Nat.sub(X, X), 0n, N.sub_self(X))
204  Equal.trans(F.F64, SF.round(False{}, q, X), SF.round_u(False{}, q, X, U), SF.pack(False{}, q, X), r1,
205    Equal.trans(F.F64, SF.round_u(False{}, q, X, U), SF.round_u(False{}, q, X, X), SF.pack(False{}, q, X), r2,
206      Equal.trans(F.F64, SF.round_u(False{}, q, X, X), SF.pack(False{}, SF.rne(q, Nat.sub(X, X)), X), SF.pack(False{}, q, X), r3, r4)))
207
208# pack(q, X) is the pattern with exponent field j + 970 and fraction q mod 2^52
209def pack_q(+one: Nat, +h1: {one == 1n : Nat}, +q: Nat, +j: Nat, +hj: {Nat.is_le(j, 52n) == True{} : Bool}, +f53: {C.fits(53n, q) == True{} : Bool}, +n52: {C.fits(52n, q) == False{} : Bool}) -> {SF.pack(False{}, q, Nat.add(j, 2895n)) == SF.encode(False{}, Nat.add(j, 970n), C.low(52n, q)) : F.F64}:
210  +X = Nat.add(j, 2895n)
211  +EF = Nat.add(j, 969n)
212  +E = Nat.add(j, 970n)
213  +l52 = C.low(52n, q)
214  +hEF = N.add_assoc(j, 969n, 1926n)
215  +hq = N.lt_le(q, C.shift(53n, one), WW.lt_one(53n, one, h1, q, f53))
216  +h0 = Equal.cong(Bool, Bool, c => Bool.or(Bool.not(c), Nat.is_eq(EF, 0n)), C.fits(52n, q), False{}, n52)
217  +eA = Equal.trans(Nat, Nat.add(Nat.add(j, 969n), 1n), Nat.add(j, 970n), Nat.add(970n, j), N.add_assoc(j, 969n, 1n), N.add_comm(j, 970n))
218  +ev2 = L.subst(Nat, z => {Nat.is_lt(z, 2047n) == True{} : Bool}, Nat.add(970n, j), Nat.add(Nat.add(j, 969n), 1n), Equal.sym(Nat, Nat.add(Nat.add(j, 969n), 1n), Nat.add(970n, j), eA), N.le_lt_trans(j, 52n, 1077n, hj, {==}))
219  +hov = Equal.trans(Bool, Nat.is_lt(Nat.add(EF, SF.pick(Nat, C.fits(53n, q), 1n, 2n)), 2047n), Nat.is_lt(Nat.add(EF, 1n), 2047n), True{}, Equal.cong(Bool, Bool, c => Nat.is_lt(Nat.add(EF, SF.pick(Nat, c, 1n, 2n)), 2047n), C.fits(53n, q), True{}, f53), ev2)
220  +p1 = FR.pkg(one, h1, False{}, q, X, EF, hEF, hq, h0, hov)
221  +p2 = FR.enc_bits(False{}, E, l52)
222  +eH = FR.hi_one(C.high(52n, q), Equal.trans(Bool, Nat.is_eq(C.half(C.high(52n, q)), 0n), C.fits(53n, q), True{}, Equal.sym(Bool, C.fits(53n, q), Nat.is_eq(C.half(C.high(52n, q)), 0n), FR.f53h(q)), f53), n52)
223  +eHo = Equal.trans(Nat, C.high(52n, q), 1n, one, eH, Equal.sym(Nat, one, 1n, h1))
224  +eq = Equal.trans(Nat, q, Nat.add(l52, C.shift(52n, C.high(52n, q))), Nat.add(l52, C.shift(52n, one)), WW.low_high(52n, q), Equal.cong(Nat, Nat, z => Nat.add(l52, C.shift(52n, z)), C.high(52n, q), one, eHo))
225  +eE = Equal.trans(Nat, E, 1n+EF, Nat.add(one, EF), N.add_succ(j, 969n), Equal.cong(Nat, Nat, z => Nat.add(z, EF), 1n, one, Equal.sym(Nat, one, 1n, h1)))
226  +n1 = Equal.cong(Nat, Nat, z => Nat.add(l52, C.shift(52n, z)), E, Nat.add(one, EF), eE)
227  +n2 = Equal.cong(Nat, Nat, z => Nat.add(l52, z), C.shift(52n, Nat.add(one, EF)), Nat.add(C.shift(52n, one), C.shift(52n, EF)), WW.shift_add(52n, one, EF))
228  +n3 = Equal.sym(Nat, Nat.add(Nat.add(l52, C.shift(52n, one)), C.shift(52n, EF)), Nat.add(l52, Nat.add(C.shift(52n, one), C.shift(52n, EF))), N.add_assoc(l52, C.shift(52n, one), C.shift(52n, EF)))
229  +n4 = Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(52n, EF)), Nat.add(l52, C.shift(52n, one)), q, Equal.sym(Nat, q, Nat.add(l52, C.shift(52n, one)), eq))
230  +nn = Equal.trans(Nat, Nat.add(l52, C.shift(52n, E)), Nat.add(l52, C.shift(52n, Nat.add(one, EF))), Nat.add(q, C.shift(52n, EF)), n1,
231    Equal.trans(Nat, Nat.add(l52, C.shift(52n, Nat.add(one, EF))), Nat.add(l52, Nat.add(C.shift(52n, one), C.shift(52n, EF))), Nat.add(q, C.shift(52n, EF)), n2,
232      Equal.trans(Nat, Nat.add(l52, Nat.add(C.shift(52n, one), C.shift(52n, EF))), Nat.add(Nat.add(l52, C.shift(52n, one)), C.shift(52n, EF)), Nat.add(q, C.shift(52n, EF)), n3, n4)))
233  +p3 = Equal.cong(Nat, F.F64, z => FR.bits(False{}, z), Nat.add(l52, C.shift(52n, E)), Nat.add(q, C.shift(52n, EF)), nn)
234  Equal.trans(F.F64, SF.pack(False{}, q, X), FR.bits(False{}, Nat.add(q, C.shift(52n, EF))), SF.encode(False{}, E, l52), p1,
235    Equal.sym(F.F64, SF.encode(False{}, E, l52), FR.bits(False{}, Nat.add(q, C.shift(52n, EF))), Equal.trans(F.F64, SF.encode(False{}, E, l52), FR.bits(False{}, Nat.add(l52, C.shift(52n, E))), FR.bits(False{}, Nat.add(q, C.shift(52n, EF))), p2, p3)))
236
237# ---- the value: m * 2^-53 for 0 < m < 2^53 ----
238
239# the bit length of 1 + np is 1 + J(np)
240def J(+np: Nat) -> Nat:
241  M.bit_length(C.half(1n+np))
242
243def j52(+np: Nat, +hf: {C.fits(53n, 1n+np) == True{} : Bool}) -> {Nat.is_le(J(np), 52n) == True{} : Bool}:
244  L.subst(Nat, z => {Nat.is_le(z, 53n) == True{} : Bool}, M.bit_length(1n+np), 1n+J(np), WC.bl_succ(np), bl_le(53n, 1n+np, hf))
245
246def r52(+j: Nat, +hj: {Nat.is_le(j, 52n) == True{} : Bool}) -> {Nat.is_lt(Nat.sub(52n, j), 64n) == True{} : Bool}:
247  +r = Nat.sub(52n, j)
248  +e = Equal.trans(Nat, Nat.add(r, j), Nat.add(j, r), 52n, N.add_comm(r, j), N.sub_add(52n, j, hj))
249  N.le_lt_trans(r, 52n, 64n, L.subst(Nat, z => {Nat.is_le(r, z) == True{} : Bool}, Nat.add(r, j), 52n, e, N.le_add_right(r, j)), {==})
250
251# the implementation: shift by 52 - j, exponent field j + 970, for the bit
252# length 1 + j of the significand (j a variable, so no bit length is ever
253# evaluated inside a comparison)
254def impl_eq(+m: WU.U64, +np: Nat, +hM: {SW.value(m) == 1n+np : Nat}, +j: Nat, +hj: {Nat.is_le(j, 52n) == True{} : Bool}, +hbl: {M.bit_length(1n+np) == 1n+j : Nat}) -> {R.f53(m, X.clz(m)) == bits(X.shl(m, Nat.sub(52n, j)), Nat.add(j, 970n)) : F.F64}:
255  +r = Nat.sub(52n, j)
256  +E = Nat.add(j, 970n)
257  +c = X.clz(m)
258  +hclz = Equal.trans(Nat, c, Nat.sub(64n, M.bit_length(SW.value(m))), Nat.sub(63n, j), WC.clz_value(m),
259    Equal.trans(Nat, Nat.sub(64n, M.bit_length(SW.value(m))), Nat.sub(64n, M.bit_length(1n+np)), Nat.sub(63n, j), Equal.cong(Nat, Nat, z => Nat.sub(64n, M.bit_length(z)), SW.value(m), 1n+np, hM), Equal.cong(Nat, Nat, z => Nat.sub(64n, z), M.bit_length(1n+np), 1n+j, hbl)))
260  +es = Equal.trans(Nat, Nat.sub(c, 11n), Nat.sub(Nat.sub(63n, j), 11n), r, Equal.cong(Nat, Nat, z => Nat.sub(z, 11n), c, Nat.sub(63n, j), hclz), shift_amt(j, hj))
261  +ee = Equal.trans(Nat, Nat.sub(1033n, c), Nat.sub(1033n, Nat.sub(63n, j)), E, Equal.cong(Nat, Nat, z => Nat.sub(1033n, z), c, Nat.sub(63n, j), hclz), exp_amt(j, hj))
262  +i2 = Equal.cong(Nat, F.F64, z => bits(X.shl(m, z), Nat.sub(1033n, c)), Nat.sub(c, 11n), r, es)
263  +i3 = Equal.cong(Nat, F.F64, z => bits(X.shl(m, r), z), Nat.sub(1033n, c), E, ee)
264  Equal.trans(F.F64, R.f53(m, c), bits(X.shl(m, Nat.sub(c, 11n)), Nat.sub(1033n, c)), bits(X.shl(m, r), E), {==},
265    Equal.trans(F.F64, bits(X.shl(m, Nat.sub(c, 11n)), Nat.sub(1033n, c)), bits(X.shl(m, r), Nat.sub(1033n, c)), bits(X.shl(m, r), E), i2, i3))
266
267# j <= 52 from the bit length 1 + j <= 53
268def hj_of(+np: Nat, +j: Nat, +hf: {C.fits(53n, 1n+np) == True{} : Bool}, +hbl: {M.bit_length(1n+np) == 1n+j : Nat}) -> {Nat.is_le(j, 52n) == True{} : Bool}:
269  L.subst(Nat, z => {Nat.is_le(z, 53n) == True{} : Bool}, M.bit_length(1n+np), 1n+j, hbl, bl_le(53n, 1n+np, hf))
270
271def main_g(+one: Nat, +h1: {one == 1n : Nat}, +xv: Nat, +hx: {Nat.sub(SF.zb(), 53n) == xv : Nat}, +m: WU.U64, +np: Nat, +hM: {SW.value(m) == 1n+np : Nat}, +j: Nat, +hj: {Nat.is_le(j, 52n) == True{} : Bool}, +hbl: {M.bit_length(1n+np) == 1n+j : Nat}) -> {bits(X.shl(m, Nat.sub(52n, j)), Nat.add(j, 970n)) == SF.round(False{}, 1n+np, xv) : F.F64}:
272  +r = Nat.sub(52n, j)
273  +q = C.shift(r, 1n+np)
274  +e1 = N.sub_add(52n, j, hj)
275  +bq = Equal.trans(Nat, M.bit_length(q), Nat.add(M.bit_length(1n+np), r), 53n, FR.bl_shift(r, 1n+np, {==}),
276    Equal.trans(Nat, Nat.add(M.bit_length(1n+np), r), Nat.add(1n+j, r), 53n, Equal.cong(Nat, Nat, z => Nat.add(z, r), M.bit_length(1n+np), 1n+j, hbl), Equal.cong(Nat, Nat, z => 1n+z, Nat.add(j, r), 52n, e1)))
277  +hzq = WW.shift_eq0(r, 1n+np)
278  +f53 = L.subst(Nat, z => {C.fits(z, q) == True{} : Bool}, M.bit_length(q), 53n, bq, FR.bl_fit(q))
279  +n52 = L.subst(Nat, z => {C.fits(z, q) == False{} : Bool}, Nat.sub(M.bit_length(q), 1n), 52n, Equal.cong(Nat, Nat, z => Nat.sub(z, 1n), M.bit_length(q), 53n, bq), FR.bl_nfit(q, hzq))
280  sv = SH.shl_value(m, r, r52(j, hj))
281  +hq = Equal.trans(Nat, SW.value(X.shl(m, r)), C.low(64n, C.shift(r, SW.value(m))), q, sv,
282    Equal.trans(Nat, C.low(64n, C.shift(r, SW.value(m))), C.low(64n, q), q, Equal.cong(Nat, Nat, z => C.low(64n, C.shift(r, z)), SW.value(m), 1n+np, hM), WW.low_fit(64n, q, fits_up(53n, 11n, q, f53))))
283  +he = L.subst(Nat, z => {Nat.is_lt(z, 2048n) == True{} : Bool}, Nat.add(970n, j), Nat.add(j, 970n), N.add_comm(970n, j), N.le_lt_trans(j, 52n, 1078n, hj, {==}))
284  +l52 = C.low(52n, q)
285  +c1 = enc(one, h1, X.shl(m, r), Nat.add(j, 970n), he, q, hq, f53)
286  +c2 = pack_q(one, h1, q, j, hj, f53, n52)
287  +c3 = round_q(q, j, bq, hzq)
288  +c4 = FR.round_shift(False{}, r, 1n+np, Nat.add(j, 2895n))
289  +c5 = Equal.cong(Nat, F.F64, z => SF.round(False{}, 1n+np, z), Nat.add(Nat.add(j, 2895n), r), xv, Equal.trans(Nat, Nat.add(Nat.add(j, 2895n), r), x0(), xv, ex(j, hj), hx))
290  +s3 = Equal.trans(F.F64, SF.round(False{}, q, Nat.add(j, 2895n)), SF.pack(False{}, q, Nat.add(j, 2895n)), SF.encode(False{}, Nat.add(j, 970n), l52), c3, c2)
291  +s4 = Equal.trans(F.F64, SF.round(False{}, 1n+np, Nat.add(Nat.add(j, 2895n), r)), SF.round(False{}, q, Nat.add(j, 2895n)), SF.encode(False{}, Nat.add(j, 970n), l52), Equal.sym(F.F64, SF.round(False{}, q, Nat.add(j, 2895n)), SF.round(False{}, 1n+np, Nat.add(Nat.add(j, 2895n), r)), c4), s3)
292  +sp = Equal.trans(F.F64, SF.round(False{}, 1n+np, xv), SF.round(False{}, 1n+np, Nat.add(Nat.add(j, 2895n), r)), SF.encode(False{}, Nat.add(j, 970n), l52), Equal.sym(F.F64, SF.round(False{}, 1n+np, Nat.add(Nat.add(j, 2895n), r)), SF.round(False{}, 1n+np, xv), c5), s4)
293  Equal.trans(F.F64, bits(X.shl(m, r), Nat.add(j, 970n)), SF.encode(False{}, Nat.add(j, 970n), l52), SF.round(False{}, 1n+np, xv), c1, Equal.sym(F.F64, SF.round(False{}, 1n+np, xv), SF.encode(False{}, Nat.add(j, 970n), l52), sp))
294
295def main_j(+one: Nat, +h1: {one == 1n : Nat}, +xv: Nat, +hx: {Nat.sub(SF.zb(), 53n) == xv : Nat}, +m: WU.U64, +np: Nat, +hM: {SW.value(m) == 1n+np : Nat}, +hf: {C.fits(53n, 1n+np) == True{} : Bool}, +j: Nat, +hbl: {M.bit_length(1n+np) == 1n+j : Nat}) -> {R.f53(m, X.clz(m)) == SF.round(False{}, 1n+np, xv) : F.F64}:
296  +hj = hj_of(np, j, hf, hbl)
297  Equal.trans(F.F64, R.f53(m, X.clz(m)), bits(X.shl(m, Nat.sub(52n, j)), Nat.add(j, 970n)), SF.round(False{}, 1n+np, xv),
298    impl_eq(m, np, hM, j, hj, hbl),
299    main_g(one, h1, xv, hx, m, np, hM, j, hj, hbl))
300
301def bl_nz(+np: Nat, +h: {M.bit_length(1n+np) == 0n : Nat}) -> Empty:
302  N.succ_zero(M.bit_length(C.half(1n+np)), Equal.trans(Nat, 1n+M.bit_length(C.half(1n+np)), M.bit_length(1n+np), 0n, Equal.sym(Nat, M.bit_length(1n+np), 1n+M.bit_length(C.half(1n+np)), WC.bl_succ(np)), h))
303
304def main_b(+one: Nat, +h1: {one == 1n : Nat}, +xv: Nat, +hx: {Nat.sub(SF.zb(), 53n) == xv : Nat}, +m: WU.U64, +np: Nat, +hM: {SW.value(m) == 1n+np : Nat}, +hf: {C.fits(53n, 1n+np) == True{} : Bool}, +b: Nat, +hb: {M.bit_length(1n+np) == b : Nat}) -> {R.f53(m, X.clz(m)) == SF.round(False{}, 1n+np, xv) : F.F64}:
305  match b:
306    case 0n:
307      Empty.absurd({R.f53(m, X.clz(m)) == SF.round(False{}, 1n+np, xv) : F.F64}, bl_nz(np, hb))
308    case 1n+j:
309      main_j(one, h1, xv, hx, m, np, hM, hf, j, hb)
310
311def main_v(+one: Nat, +h1: {one == 1n : Nat}, +xv: Nat, +hx: {Nat.sub(SF.zb(), 53n) == xv : Nat}, +m: WU.U64, +np: Nat, +hM: {SW.value(m) == 1n+np : Nat}, +hf: {C.fits(53n, 1n+np) == True{} : Bool}) -> {R.f53(m, X.clz(m)) == SF.round(False{}, 1n+np, xv) : F.F64}:
312  main_b(one, h1, xv, hx, m, np, hM, hf, M.bit_length(1n+np), {==})
313
314# ---- Float64.value ----
315
316# the low 53 bits of the source output
317def mm(+x: WU.U64) -> WU.U64:
318  WU.U64{X.lo(x), U32.and(X.hi(x), 2097151)}
319
320def m_val(+x: WU.U64) -> {SW.value(mm(x)) == C.low(53n, SW.value(x)) : Nat}:
321  match x:
322    case WU.U64{+l, +h}:
323      +n = Nat.add(v(l), C.shift(32n, v(h)))
324      Equal.trans(Nat, Nat.add(v(l), C.shift(32n, v(U32.and(h, 2097151)))), Nat.add(v(l), C.shift(32n, C.low(21n, v(h)))), C.low(53n, n),
325        Equal.cong(Nat, Nat, z => Nat.add(v(l), C.shift(32n, z)), v(U32.and(h, 2097151)), C.low(21n, v(h)), FB.andm(h, 21n, 2097151, {==})),
326        Equal.sym(Nat, C.low(53n, n), Nat.add(v(l), C.shift(32n, C.low(21n, v(h)))),
327          Equal.trans(Nat, C.low(53n, n), Nat.add(C.low(32n, n), C.shift(32n, C.low(21n, C.high(32n, n)))), Nat.add(v(l), C.shift(32n, C.low(21n, v(h)))),
328            FB.low_split(32n, 21n, n),
329            Equal.trans(Nat, Nat.add(C.low(32n, n), C.shift(32n, C.low(21n, C.high(32n, n)))), Nat.add(v(l), C.shift(32n, C.low(21n, C.high(32n, n)))), Nat.add(v(l), C.shift(32n, C.low(21n, v(h)))),
330              Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(32n, C.low(21n, C.high(32n, n)))), C.low(32n, n), v(l), WW.low_u(32n, v(l), v(h), LW.vb(l))),
331              Equal.cong(Nat, Nat, z => Nat.add(v(l), C.shift(32n, C.low(21n, z))), C.high(32n, n), v(h), WW.high_u(32n, v(l), v(h), LW.vb(l)))))))
332
333def iz(+m: WU.U64, +vm: Nat, +hv: {SW.value(m) == vm : Nat}) -> {X.is_zero(m) == Nat.is_eq(vm, 0n) : Bool}:
334  Equal.trans(Bool, X.is_zero(m), Nat.is_eq(SW.value(m), 0n), Nat.is_eq(vm, 0n), WA.is_zero_value(m), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), SW.value(m), vm, hv))
335
336def hl_of(+x: WU.U64, +vm: Nat, +hv: {SW.value(mm(x)) == vm : Nat}) -> {C.low(53n, SW.value(x)) == vm : Nat}:
337  Equal.trans(Nat, C.low(53n, SW.value(x)), SW.value(mm(x)), vm, Equal.sym(Nat, SW.value(mm(x)), C.low(53n, SW.value(x)), m_val(x)), hv)
338
339def round0(+xv: Nat) -> {SF.round(False{}, 0n, xv) == SF.zero(False{}) : F.F64}:
340  {==}
341
342def value_z(+x: WU.U64, +n: Nat, +hn: {C.low(53n, SW.value(x)) == n : Nat}, +xv: Nat, +hv: {SW.value(mm(x)) == 0n : Nat}) -> {R.to_float(x) == SF.round(False{}, n, xv) : F.F64}:
343  +h0 = Equal.trans(Nat, n, C.low(53n, SW.value(x)), 0n, Equal.sym(Nat, C.low(53n, SW.value(x)), n, hn), hl_of(x, 0n, hv))
344  %Equal.sym(Nat, n, 0n, h0) : {R.to_float(x) == SF.round(False{}, _, xv) : F.F64}
345  %Equal.sym(Bool, X.is_zero(mm(x)), Nat.is_eq(0n, 0n), iz(mm(x), 0n, hv)) : {R.f53_z(mm(x), _) == SF.round(False{}, 0n, xv) : F.F64}
346  Equal.trans(F.F64, R.f53_z(mm(x), Nat.is_eq(0n, 0n)), SF.zero(False{}), SF.round(False{}, 0n, xv), {==}, Equal.sym(F.F64, SF.round(False{}, 0n, xv), SF.zero(False{}), round0(xv)))
347
348def value_s(+x: WU.U64, +n: Nat, +hn: {C.low(53n, SW.value(x)) == n : Nat}, +np: Nat, +xv: Nat, +hx: {Nat.sub(SF.zb(), 53n) == xv : Nat}, +hv: {SW.value(mm(x)) == 1n+np : Nat}) -> {R.to_float(x) == SF.round(False{}, n, xv) : F.F64}:
349  +hl = hl_of(x, 1n+np, hv)
350  +h1 = Equal.trans(Nat, n, C.low(53n, SW.value(x)), 1n+np, Equal.sym(Nat, C.low(53n, SW.value(x)), n, hn), hl)
351  +hf = Equal.trans(Bool, C.fits(53n, 1n+np), C.fits(53n, C.low(53n, SW.value(x))), True{}, Equal.cong(Nat, Bool, z => C.fits(53n, z), 1n+np, C.low(53n, SW.value(x)), Equal.sym(Nat, C.low(53n, SW.value(x)), 1n+np, hl)), WW.low_fits(53n, SW.value(x)))
352  %Equal.sym(Nat, n, 1n+np, h1) : {R.to_float(x) == SF.round(False{}, _, xv) : F.F64}
353  %Equal.sym(Bool, X.is_zero(mm(x)), Nat.is_eq(1n+np, 0n), iz(mm(x), 1n+np, hv)) : {R.f53_z(mm(x), _) == SF.round(False{}, 1n+np, xv) : F.F64}
354  Equal.trans(F.F64, R.f53_z(mm(x), Nat.is_eq(1n+np, 0n)), R.f53(mm(x), X.clz(mm(x))), SF.round(False{}, 1n+np, xv), {==}, main_v(1n, {==}, xv, hx, mm(x), np, hv, hf))
355
356def value_c(+vm: Nat, +x: WU.U64, +n: Nat, +hn: {C.low(53n, SW.value(x)) == n : Nat}, +xv: Nat, +hx: {Nat.sub(SF.zb(), 53n) == xv : Nat}, +hv: {SW.value(mm(x)) == vm : Nat}) -> {R.to_float(x) == SF.round(False{}, n, xv) : F.F64}:
357  match vm:
358    case 0n:
359      value_z(x, n, hn, xv, hv)
360    case 1n+np:
361      value_s(x, n, hn, np, xv, hx, hv)
362
363# THEOREM (Float64.value)
364def value(+x: WU.U64, +n: Nat, +hn: {C.low(53n, SW.value(x)) == n : Nat}, +xv: Nat, +hx: {Nat.sub(SF.zb(), 53n) == xv : Nat}) -> SR.Float64.value(x, n, hn, xv, hx):
365  value_c(SW.value(mm(x)), x, n, hn, xv, hx, {==})
366
367# ---- Float64.lt_one ----
368# The comparison is F.lt itself (Go's <): the checker evaluates what it can
369# on 1.0 = Bits{0, H} (H = 0x3FF00000) at the word level, and every value
370# fact about H comes from word equations (hH, hK), so no 30-bit constant is
371# ever unfolded into a natural number.
372
373def and_f(+b: Bool) -> {Bool.and(b, False{}) == False{} : Bool}:
374  match b:
375    case True{}:
376      {==}
377    case False{}:
378      {==}
379
380# the value of the high word of 1.0 without its sign bit: k * 2^20 (k = 1023,
381# kept a variable so no 30-bit constant is ever expanded)
382def hv_one(+H: U32, +K: U32, +k: Nat, +hk: {C.fits(12n, k) == True{} : Bool}, +hH: {U32.and(H, 2147483647) == U32.mul(K, X.pow2(20n)) : U32}, +hK: {U32.to_nat(K) == k : Nat}) -> {v(U32.and(H, 2147483647)) == C.shift(20n, k) : Nat}:
383  Equal.trans(Nat, v(U32.and(H, 2147483647)), v(U32.mul(K, X.pow2(20n))), C.shift(20n, k),
384    Equal.cong(U32, Nat, z => v(z), U32.and(H, 2147483647), U32.mul(K, X.pow2(20n)), hH),
385    Equal.trans(Nat, v(U32.mul(K, X.pow2(20n))), C.low(32n, C.shift(20n, v(K))), C.shift(20n, k),
386      SH.mul_p2(K, 20n, {==}),
387      Equal.trans(Nat, C.low(32n, C.shift(20n, v(K))), C.low(32n, C.shift(20n, k)), C.shift(20n, k),
388        Equal.cong(Nat, Nat, z => C.low(32n, C.shift(20n, z)), v(K), k, hK),
389        WW.low_fit(32n, C.shift(20n, k), fits_shift(20n, 12n, k, hk)))))
390
391# a double Bits{l, hw(E, qh)} with E < k <= 2047 is below Bits{0, H} whose
392# high word (without sign) is k * 2^20
393def below_one(+l: U32, +qh: U32, +E: Nat, +H: U32, +K: U32, +k: Nat, +hE: {Nat.is_lt(E, k) == True{} : Bool}, +hk: {C.fits(11n, k) == True{} : Bool}, +hn: {F.is_nan(F.Bits{0, H}) == False{} : Bool}, +hz: {F.is_zero(F.Bits{0, H}) == False{} : Bool}, +hs: {F.signbit(F.Bits{0, H}) == False{} : Bool}, +hH: {U32.and(H, 2147483647) == U32.mul(K, X.pow2(20n)) : U32}, +hK: {U32.to_nat(K) == k : Nat}) -> {F.lt(F.Bits{l, hw(E, qh)}, F.Bits{0, H}) == True{} : Bool}:
394  +h = hw(E, qh)
395  +x = {F.Bits{l, h} : F.F64}
396  +y = {F.Bits{0, H} : F.F64}
397  +lq = C.low(20n, v(qh))
398  +hk2 = WW.lt_of_fits(11n, k, hk)
399  +he = N.lt_trans(E, k, 2048n, hE, hk2)
400  +hk12 = SH.fits_mono(11n, 12n, k, {==}, hk)
401  +vh = hw_value(1n, {==}, E, qh, he)
402  +f11 = fits_lt11(E, he)
403  +f31 = Equal.trans(Bool, C.fits(31n, v(h)), C.fits(31n, Nat.add(lq, C.shift(20n, E))), True{}, Equal.cong(Nat, Bool, z => C.fits(31n, z), v(h), Nat.add(lq, C.shift(20n, E)), vh), WW.limbs_fit(20n, 11n, lq, E, WW.low_fits(20n, v(qh)), f11))
404  +ef = Equal.trans(Nat, v(U32.and(U32.div(h, 1048576), 2047)), C.low(11n, C.high(20n, v(h))), E, FB.ef_g(1n, {==}, h, 1048576, {==}, 2047, {==}),
405    Equal.trans(Nat, C.low(11n, C.high(20n, v(h))), C.low(11n, E), E,
406      Equal.cong(Nat, Nat, z => C.low(11n, z), C.high(20n, v(h)), E, Equal.trans(Nat, C.high(20n, v(h)), C.high(20n, Nat.add(lq, C.shift(20n, E))), E, Equal.cong(Nat, Nat, z => C.high(20n, z), v(h), Nat.add(lq, C.shift(20n, E)), vh), WW.high_u(20n, lq, E, WW.low_fits(20n, v(qh))))),
407      WW.low_fit(11n, E, f11)))
408  +hne = N.is_eq_lt(E, 2047n, N.lt_le_trans(E, k, 2047n, hE, N.lt_succ_le(k, 2047n, hk2)))
409  +nanx = Equal.trans(Bool, F.is_nan(x), Bool.and(Nat.is_eq(E, 2047n), F.nz(F.frac(x))), False{},
410    Equal.cong(Nat, Bool, z => Bool.and(Nat.is_eq(z, 2047n), F.nz(F.frac(x))), v(U32.and(U32.div(h, 1048576), 2047)), E, ef),
411    Equal.cong(Bool, Bool, z => Bool.and(z, F.nz(F.frac(x))), Nat.is_eq(E, 2047n), False{}, hne))
412  +uo = Equal.trans(Bool, F.unordered(x, y), Bool.or(False{}, F.is_nan(y)), False{}, Equal.cong(Bool, Bool, z => Bool.or(z, F.is_nan(y)), F.is_nan(x), False{}, nanx), hn)
413  +zs = Equal.trans(Bool, F.zeros(x, y), Bool.and(F.is_zero(x), False{}), False{}, Equal.cong(Bool, Bool, z => Bool.and(F.is_zero(x), z), F.is_zero(y), False{}, hz), and_f(F.is_zero(x)))
414  +sx = Equal.trans(Bool, F.signbit(x), SF.sign(x), False{}, FB.signbit_g(1n, {==}, l, h, 2147483648, {==}),
415    Equal.cong(Bool, Bool, z => Bool.not(z), C.fits(31n, v(h)), True{}, f31))
416  +vmx = Equal.trans(Nat, SW.value(F.mag(x)), Nat.add(v(l), C.shift(32n, C.low(31n, v(h)))), Nat.add(v(l), C.shift(32n, v(h))),
417    Equal.cong(Nat, Nat, z => Nat.add(v(l), C.shift(32n, z)), v(U32.and(h, 2147483647)), C.low(31n, v(h)), FB.andm(h, 31n, 2147483647, {==})),
418    Equal.cong(Nat, Nat, z => Nat.add(v(l), C.shift(32n, z)), C.low(31n, v(h)), v(h), WW.low_fit(31n, v(h), f31)))
419  +vmy = Equal.cong(Nat, Nat, z => C.shift(32n, z), v(U32.and(H, 2147483647)), C.shift(20n, k), hv_one(H, K, k, hk12, hH, hK))
420  +hvh = Equal.trans(Bool, Nat.is_lt(v(h), C.shift(20n, k)), Nat.is_lt(Nat.add(lq, C.shift(20n, E)), C.shift(20n, k)), True{}, Equal.cong(Nat, Bool, z => Nat.is_lt(z, C.shift(20n, k)), v(h), Nat.add(lq, C.shift(20n, E)), vh), WW.lt_hi(20n, lq, E, 0n, k, WW.low_fits(20n, v(qh)), hE))
421  +hlt = WW.lt_hi(32n, v(l), v(h), 0n, C.shift(20n, k), LW.vb(l), hvh)
422  +cmp = Equal.trans(Bool, X.lt(F.mag(x), F.mag(y)), Nat.is_lt(SW.value(F.mag(x)), SW.value(F.mag(y))), True{}, WA.lt_value(F.mag(x), F.mag(y)),
423    Equal.trans(Bool, Nat.is_lt(SW.value(F.mag(x)), SW.value(F.mag(y))), Nat.is_lt(Nat.add(v(l), C.shift(32n, v(h))), C.shift(32n, C.shift(20n, k))), True{},
424      Equal.trans(Bool, Nat.is_lt(SW.value(F.mag(x)), SW.value(F.mag(y))), Nat.is_lt(Nat.add(v(l), C.shift(32n, v(h))), SW.value(F.mag(y))), Nat.is_lt(Nat.add(v(l), C.shift(32n, v(h))), C.shift(32n, C.shift(20n, k))),
425        Equal.cong(Nat, Bool, z => Nat.is_lt(z, SW.value(F.mag(y))), SW.value(F.mag(x)), Nat.add(v(l), C.shift(32n, v(h))), vmx),
426        Equal.cong(Nat, Bool, z => Nat.is_lt(Nat.add(v(l), C.shift(32n, v(h))), z), SW.value(F.mag(y)), C.shift(32n, C.shift(20n, k)), vmy)),
427      hlt))
428  +c1 = Equal.cong(Bool, Bool, z => F.lt_z(x, y, z, F.zeros(x, y)), F.unordered(x, y), False{}, uo)
429  +c2 = Equal.cong(Bool, Bool, z => F.lt_z(x, y, False{}, z), F.zeros(x, y), False{}, zs)
430  +c3 = Equal.cong(Bool, Bool, z => F.lt_s(x, y, z, F.signbit(y)), F.signbit(x), False{}, sx)
431  +c4 = Equal.cong(Bool, Bool, z => F.lt_s(x, y, False{}, z), F.signbit(y), False{}, hs)
432  Equal.trans(Bool, F.lt(x, y), F.lt_z(x, y, False{}, F.zeros(x, y)), True{}, c1,
433    Equal.trans(Bool, F.lt_z(x, y, False{}, F.zeros(x, y)), F.lt_z(x, y, False{}, False{}), True{}, c2,
434      Equal.trans(Bool, F.lt_s(x, y, F.signbit(x), F.signbit(y)), F.lt_s(x, y, False{}, F.signbit(y)), True{}, c3,
435        Equal.trans(Bool, F.lt_s(x, y, False{}, F.signbit(y)), F.lt_s(x, y, False{}, False{}), True{}, c4, cmp))))
436
437def lt_z_case(+x: WU.U64, +hv: {SW.value(mm(x)) == 0n : Nat}) -> {F.lt(R.to_float(x), F.one()) == True{} : Bool}:
438  %Equal.sym(Bool, X.is_zero(mm(x)), Nat.is_eq(0n, 0n), iz(mm(x), 0n, hv)) : {F.lt(R.f53_z(mm(x), _), F.one()) == True{} : Bool}
439  {==}
440
441def lt_s_case(+x: WU.U64, +np: Nat, +hv: {SW.value(mm(x)) == 1n+np : Nat}) -> {F.lt(R.to_float(x), F.one()) == True{} : Bool}:
442  +hl = hl_of(x, 1n+np, hv)
443  +hf = Equal.trans(Bool, C.fits(53n, 1n+np), C.fits(53n, C.low(53n, SW.value(x))), True{}, Equal.cong(Nat, Bool, z => C.fits(53n, z), 1n+np, C.low(53n, SW.value(x)), Equal.sym(Nat, C.low(53n, SW.value(x)), 1n+np, hl)), WW.low_fits(53n, SW.value(x)))
444  +j = J(np)
445  +Q = X.shl(mm(x), Nat.sub(52n, j))
446  +hE = Equal.trans(Bool, Nat.is_lt(Nat.add(j, 970n), 1023n), Nat.is_lt(j, 53n), True{}, WW.lt_cancel_r(j, 53n, 970n), N.le_lt_succ(j, 52n, j52(np, hf)))
447  %Equal.sym(Bool, X.is_zero(mm(x)), Nat.is_eq(1n+np, 0n), iz(mm(x), 1n+np, hv)) : {F.lt(R.f53_z(mm(x), _), F.one()) == True{} : Bool}
448  %Equal.sym(F.F64, R.f53(mm(x), X.clz(mm(x))), bits(Q, Nat.add(j, 970n)), impl_eq(mm(x), np, hv, j, j52(np, hf), WC.bl_succ(np))) : {F.lt(_, F.one()) == True{} : Bool}
449  below_one(X.lo(Q), X.hi(Q), Nat.add(j, 970n), 1072693248, 1023, 1023n, hE, {==}, {==}, {==}, {==}, {==}, {==})
450
451def lt_c(+vm: Nat, +x: WU.U64, +hv: {SW.value(mm(x)) == vm : Nat}) -> {F.lt(R.to_float(x), F.one()) == True{} : Bool}:
452  match vm:
453    case 0n:
454      lt_z_case(x, hv)
455    case 1n+np:
456      lt_s_case(x, np, hv)
457
458# THEOREM (Float64.lt_one)
459def lt_one(+x: WU.U64) -> SR.Float64.lt_one(x):
460  lt_c(SW.value(mm(x)), x, {==})