proofs/math/typed/f64round.bend

bend-collections-laws-math@1.0.0.0 · 924 lines · 105 definitions

1import Base
2import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
4import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
5import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
6import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
7import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
8import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
9import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
10import bend-collections-laws-math@1.0.0.0/proofs/lib/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/u32laws.bend as LW
13import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
14import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB
15import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as NC
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/lib/u32.bend as U
18import bend-collections-laws-math@1.0.0.0/proofs/lib/u32half.bend as UH
19import bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend as A
20import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
21import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
22import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
23import bend-collections-laws-math@1.0.0.0/proofs/math/natural/bits.bend as BT
24
25# Rounding to nearest, ties to even, on binary64: the lemmas behind
26# SoftFloat's roundPackToF64. A rounding by k bits depends only on the
27# quotient and on how the remainder compares with half the divisor, so
28# jamming the bits below the rounding point into one sticky bit keeps the
29# result (the sticky-bit argument of Flocq's Round_NE / inbetween theory,
30# Boldo and Melquiond; Goldberg, "What every computer scientist should know
31# about floating-point arithmetic", 1991). The pattern of a finite double
32# is (s * 2^11 + field) * 2^52 + fraction, one integer N below 2^63 with
33# the sign on top: bits(s, N).
34
35# SF.pick on a known Bool, as lemmas: rewriting with these keeps a conversion
36# syntactic instead of unfolding (and normalizing) both branches
37def pk_t(-T: Data, +a: T, +b: T) -> {SF.pick(T, True{}, a, b) == a : T}:
38  {==}
39
40def pk_f(-T: Data, +a: T, +b: T) -> {SF.pick(T, False{}, a, b) == b : T}:
41  {==}
42
43def v(+x: U32) -> Nat:
44  U32.to_nat(x)
45
46# ---- a double as sign and a 63-bit integer ----
47
48def bits(+s: Bool, +n: Nat) -> F.F64:
49  F.Bits{U32.from_nat(C.low(32n, n)), U32.from_nat(Nat.add(C.high(32n, n), C.shift(31n, SF.b2n(s))))}
50
51def enc_bits(+s: Bool, +ef: Nat, +f: Nat) -> {SF.encode(s, ef, f) == bits(s, Nat.add(f, C.shift(52n, ef))) : F.F64}:
52  +t = C.shift(20n, ef)
53  +n = Nat.add(f, C.shift(52n, ef))
54  +b = C.shift(31n, SF.b2n(s))
55  +e52 = WW.shift_comp(32n, 20n, ef)
56  +el = Equal.trans(Nat, C.low(32n, n), C.low(32n, Nat.add(f, C.shift(32n, t))), C.low(32n, f), Equal.cong(Nat, Nat, z => C.low(32n, Nat.add(f, z)), C.shift(52n, ef), C.shift(32n, t), e52), WW.low_add_shift(32n, f, t))
57  +eh0 = Equal.trans(Nat, C.high(32n, n), C.high(32n, Nat.add(f, C.shift(32n, t))), Nat.add(C.high(32n, f), t), Equal.cong(Nat, Nat, z => C.high(32n, Nat.add(f, z)), C.shift(52n, ef), C.shift(32n, t), e52), WW.high_add_shift(32n, f, t))
58  +eh = Equal.trans(Nat, Nat.add(C.high(32n, n), b), Nat.add(Nat.add(C.high(32n, f), t), b), Nat.add(C.high(32n, f), C.shift(20n, Nat.add(ef, C.shift(11n, SF.b2n(s))))), Equal.cong(Nat, Nat, z => Nat.add(z, b), C.high(32n, n), Nat.add(C.high(32n, f), t), eh0), FB.fold(C.high(32n, f), ef, SF.b2n(s)))
59  +e = Equal.trans(F.F64, bits(s, n), F.Bits{U32.from_nat(C.low(32n, f)), U32.from_nat(Nat.add(C.high(32n, n), b))}, SF.encode(s, ef, f), Equal.cong(Nat, F.F64, z => F.Bits{U32.from_nat(z), U32.from_nat(Nat.add(C.high(32n, n), b))}, C.low(32n, n), C.low(32n, f), el), Equal.cong(Nat, F.F64, z => F.Bits{U32.from_nat(C.low(32n, f)), U32.from_nat(z)}, Nat.add(C.high(32n, n), b), Nat.add(C.high(32n, f), C.shift(20n, Nat.add(ef, C.shift(11n, SF.b2n(s))))), eh))
60  Equal.sym(F.F64, bits(s, n), SF.encode(s, ef, f), e)
61
62# ---- rounding by k bits depends on the quotient and a comparison ----
63
64def rne_c(+q: Nat, +c: Cmp) -> Nat:
65  Nat.add(q, SF.b2n(Bool.or(Cmp.is_lt(SF.flip(c)), Bool.and(Cmp.is_eq(c), Nat.is_eq(Nat.mod(q, 2n), 1n)))))
66
67def rne_cmp(+q: Nat, +r: Nat, +h: Nat) -> {SF.rne_up(q, r, h) == rne_c(q, Nat.cmp(r, h)) : Nat}:
68  Equal.cong(Cmp, Nat, t => Nat.add(q, SF.b2n(Bool.or(Cmp.is_lt(t), Bool.and(Cmp.is_eq(Nat.cmp(r, h)), Nat.is_eq(Nat.mod(q, 2n), 1n))))), Nat.cmp(h, r), SF.flip(Nat.cmp(r, h)), Equal.sym(Cmp, SF.flip(Nat.cmp(r, h)), Nat.cmp(h, r), NC.cmp_flip(r, h)))
69
70def lex_assoc(+x: Cmp, +y: Cmp, +z: Cmp) -> {NC.lex(NC.lex(x, y), z) == NC.lex(x, NC.lex(y, z)) : Cmp}:
71  match x:
72    case LT{}:
73      {==}
74    case EQ{}:
75      {==}
76    case GT{}:
77      {==}
78
79def fz(+d: Nat) -> {C.fits(d, 0n) == True{} : Bool}:
80  match d:
81    case 0n:
82      {==}
83    case 1n+ +p:
84      fz(p)
85
86def small(+t: Nat, +ht: {Nat.is_le(t, 1n) == True{} : Bool}) -> {C.fits(1n, t) == True{} : Bool}:
87  match t:
88    case 0n:
89      {==}
90    case 1n:
91      {==}
92    case 2n+ +q:
93      NC.absurd_tf({C.fits(1n, 2n+q) == True{} : Bool}, ht)
94
95def bit_small(+t: Nat, +ht: {Nat.is_le(t, 1n) == True{} : Bool}) -> {C.bit(t) == t : Nat}:
96  match t:
97    case 0n:
98      {==}
99    case 1n:
100      {==}
101    case 2n+ +q:
102      NC.absurd_tf({C.bit(2n+q) == 2n+q : Nat}, ht)
103
104def half_small(+t: Nat, +ht: {Nat.is_le(t, 1n) == True{} : Bool}) -> {C.half(t) == 0n : Nat}:
105  match t:
106    case 0n:
107      {==}
108    case 1n:
109      {==}
110    case 2n+ +q:
111      NC.absurd_tf({C.half(2n+q) == 0n : Nat}, ht)
112
113def max_le1(+b: Nat, +l: Nat, +hb: {Nat.is_le(b, 1n) == True{} : Bool}) -> {Nat.is_le(Nat.max(b, Nat.min(l, 1n)), 1n) == True{} : Bool}:
114  match b l:
115    case 0n 0n:
116      {==}
117    case 0n 1n+ +lp:
118      match lp:
119        case 0n:
120          {==}
121        case 1n+ +lq:
122          {==}
123    case 1n 0n:
124      {==}
125    case 1n 1n+ +lp:
126      match lp:
127        case 0n:
128          {==}
129        case 1n+ +lq:
130          {==}
131    case 2n+ +q _:
132      NC.absurd_tf({Nat.is_le(Nat.max(2n+q, Nat.min(l, 1n)), 1n) == True{} : Bool}, hb)
133
134# the sticky bit merges the parity bit with "some lower bit is set"
135def tl(+b: Nat, +l: Nat, +hb: {Nat.is_le(b, 1n) == True{} : Bool}) -> {NC.lex(Nat.cmp(b, 0n), Nat.cmp(l, 0n)) == Nat.cmp(Nat.max(b, Nat.min(l, 1n)), 0n) : Cmp}:
136  match b l:
137    case 0n 0n:
138      {==}
139    case 0n 1n+ +lp:
140      {==}
141    case 1n 0n:
142      {==}
143    case 1n 1n+ +lp:
144      {==}
145    case 2n+ +q _:
146      NC.absurd_tf({NC.lex(Nat.cmp(2n+q, 0n), Nat.cmp(l, 0n)) == Nat.cmp(Nat.max(2n+q, Nat.min(l, 1n)), 0n) : Cmp}, hb)
147
148# jam(H, L) is H with bit 0 replaced by t = max(bit H, [L > 0])
149def jam_form(+h: Nat, +l: Nat) -> {SW.jam(h, l) == Nat.add(Nat.max(C.bit(h), Nat.min(l, 1n)), Nat.double(C.half(h))) : Nat}:
150  +t = Nat.max(C.bit(h), Nat.min(l, 1n))
151  +e1 = Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(2n, z), Nat.max(Nat.mod(h, 2n), Nat.min(l, 1n))), Nat.div(h, 2n), C.half(h), Equal.sym(Nat, C.half(h), Nat.div(h, 2n), WA.half_div(h)))
152  +e2 = Equal.cong(Nat, Nat, z => Nat.add(z, Nat.max(Nat.mod(h, 2n), Nat.min(l, 1n))), Nat.mul(2n, C.half(h)), Nat.double(C.half(h)), Equal.sym(Nat, Nat.double(C.half(h)), Nat.mul(2n, C.half(h)), NA.double_mul(C.half(h))))
153  +e3 = Equal.cong(Nat, Nat, z => Nat.add(Nat.double(C.half(h)), Nat.max(z, Nat.min(l, 1n))), Nat.mod(h, 2n), C.bit(h), Equal.sym(Nat, C.bit(h), Nat.mod(h, 2n), WW.bit_mod(h)))
154  +e4 = NA.add_comm(Nat.double(C.half(h)), t)
155  Equal.trans(Nat, SW.jam(h, l), Nat.add(Nat.mul(2n, C.half(h)), Nat.max(Nat.mod(h, 2n), Nat.min(l, 1n))), Nat.add(t, Nat.double(C.half(h))), e1, Equal.trans(Nat, Nat.add(Nat.mul(2n, C.half(h)), Nat.max(Nat.mod(h, 2n), Nat.min(l, 1n))), Nat.add(Nat.double(C.half(h)), Nat.max(Nat.mod(h, 2n), Nat.min(l, 1n))), Nat.add(t, Nat.double(C.half(h))), e2, Equal.trans(Nat, Nat.add(Nat.double(C.half(h)), Nat.max(Nat.mod(h, 2n), Nat.min(l, 1n))), Nat.add(Nat.double(C.half(h)), t), Nat.add(t, Nat.double(C.half(h))), e3, e4)))
156
157# rounding m by K + D bits is rounding jam(m >> D, m mod 2^D) by K bits, K >= 2
158def sticky(+i: Nat, +D: Nat, +m: Nat) -> {SF.rne(m, Nat.add(2n+i, D)) == SF.rne(SW.jam(C.high(D, m), C.low(D, m)), 2n+i) : Nat}:
159  +eA = NA.add_comm(D, 2n+i)
160  +qm = Equal.trans(Nat, C.high(Nat.add(2n+i, D), m), C.high(Nat.add(D, 2n+i), m), C.high(2n+i, C.high(D, m)), Equal.cong(Nat, Nat, z => C.high(z, m), Nat.add(2n+i, D), Nat.add(D, 2n+i), Equal.sym(Nat, Nat.add(D, 2n+i), Nat.add(2n+i, D), eA)), WW.high_comp(2n+i, D, m))
161  +rm = Equal.trans(Nat, C.low(Nat.add(2n+i, D), m), C.low(Nat.add(D, 2n+i), m), Nat.add(C.low(D, m), C.shift(D, C.low(2n+i, C.high(D, m)))), Equal.cong(Nat, Nat, z => C.low(z, m), Nat.add(2n+i, D), Nat.add(D, 2n+i), Equal.sym(Nat, Nat.add(D, 2n+i), Nat.add(2n+i, D), eA)), FB.low_split(D, 2n+i, m))
162  +hm = Equal.trans(Nat, C.shift(Nat.add(1n+i, D), 1n), C.shift(Nat.add(D, 1n+i), 1n), C.shift(D, C.shift(1n+i, 1n)), Equal.cong(Nat, Nat, z => C.shift(z, 1n), Nat.add(1n+i, D), Nat.add(D, 1n+i), NA.add_comm(1n+i, D)), WW.shift_comp(D, 1n+i, 1n))
163  +c1 = Equal.trans(Cmp, Nat.cmp(C.low(Nat.add(2n+i, D), m), C.shift(Nat.add(1n+i, D), 1n)), Nat.cmp(Nat.add(C.low(D, m), C.shift(D, C.low(2n+i, C.high(D, m)))), C.shift(Nat.add(1n+i, D), 1n)), Nat.cmp(Nat.add(C.low(D, m), C.shift(D, C.low(2n+i, C.high(D, m)))), C.shift(D, C.shift(1n+i, 1n))), Equal.cong(Nat, Cmp, z => Nat.cmp(z, C.shift(Nat.add(1n+i, D), 1n)), C.low(Nat.add(2n+i, D), m), Nat.add(C.low(D, m), C.shift(D, C.low(2n+i, C.high(D, m)))), rm), Equal.cong(Nat, Cmp, z => Nat.cmp(Nat.add(C.low(D, m), C.shift(D, C.low(2n+i, C.high(D, m)))), z), C.shift(Nat.add(1n+i, D), 1n), C.shift(D, C.shift(1n+i, 1n)), hm))
164  +c2 = NC.cmp_limbs(D, C.low(D, m), C.low(2n+i, C.high(D, m)), 0n, C.shift(1n+i, 1n), WW.low_fits(D, m), fz(D))
165  +c3 = Equal.cong(Cmp, Cmp, z => NC.lex(z, Nat.cmp(C.low(D, m), 0n)), Nat.cmp(C.low(2n+i, C.high(D, m)), C.shift(1n+i, 1n)), NC.lex(Nat.cmp(C.low(1n+i, C.half(C.high(D, m))), C.shift(i, 1n)), Nat.cmp(C.bit(C.high(D, m)), 0n)), NC.cmp_limbs(1n, C.bit(C.high(D, m)), C.low(1n+i, C.half(C.high(D, m))), 0n, C.shift(i, 1n), small(C.bit(C.high(D, m)), WW.bit_le1(C.high(D, m))), fz(1n)))
166  +c4 = lex_assoc(Nat.cmp(C.low(1n+i, C.half(C.high(D, m))), C.shift(i, 1n)), Nat.cmp(C.bit(C.high(D, m)), 0n), Nat.cmp(C.low(D, m), 0n))
167  +c5 = Equal.cong(Cmp, Cmp, z => NC.lex(Nat.cmp(C.low(1n+i, C.half(C.high(D, m))), C.shift(i, 1n)), z), NC.lex(Nat.cmp(C.bit(C.high(D, m)), 0n), Nat.cmp(C.low(D, m), 0n)), Nat.cmp(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), 0n), tl(C.bit(C.high(D, m)), C.low(D, m), WW.bit_le1(C.high(D, m))))
168  +cm = Equal.trans(Cmp, Nat.cmp(C.low(Nat.add(2n+i, D), m), C.shift(Nat.add(1n+i, D), 1n)), Nat.cmp(Nat.add(C.low(D, m), C.shift(D, C.low(2n+i, C.high(D, m)))), C.shift(D, C.shift(1n+i, 1n))), NC.lex(Nat.cmp(C.low(1n+i, C.half(C.high(D, m))), C.shift(i, 1n)), Nat.cmp(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), 0n)), c1, Equal.trans(Cmp, Nat.cmp(Nat.add(C.low(D, m), C.shift(D, C.low(2n+i, C.high(D, m)))), C.shift(D, C.shift(1n+i, 1n))), NC.lex(Nat.cmp(C.low(2n+i, C.high(D, m)), C.shift(1n+i, 1n)), Nat.cmp(C.low(D, m), 0n)), NC.lex(Nat.cmp(C.low(1n+i, C.half(C.high(D, m))), C.shift(i, 1n)), Nat.cmp(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), 0n)), c2, Equal.trans(Cmp, NC.lex(Nat.cmp(C.low(2n+i, C.high(D, m)), C.shift(1n+i, 1n)), Nat.cmp(C.low(D, m), 0n)), NC.lex(NC.lex(Nat.cmp(C.low(1n+i, C.half(C.high(D, m))), C.shift(i, 1n)), Nat.cmp(C.bit(C.high(D, m)), 0n)), Nat.cmp(C.low(D, m), 0n)), NC.lex(Nat.cmp(C.low(1n+i, C.half(C.high(D, m))), C.shift(i, 1n)), Nat.cmp(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), 0n)), c3, Equal.trans(Cmp, NC.lex(NC.lex(Nat.cmp(C.low(1n+i, C.half(C.high(D, m))), C.shift(i, 1n)), Nat.cmp(C.bit(C.high(D, m)), 0n)), Nat.cmp(C.low(D, m), 0n)), NC.lex(Nat.cmp(C.low(1n+i, C.half(C.high(D, m))), C.shift(i, 1n)), NC.lex(Nat.cmp(C.bit(C.high(D, m)), 0n), Nat.cmp(C.low(D, m), 0n))), NC.lex(Nat.cmp(C.low(1n+i, C.half(C.high(D, m))), C.shift(i, 1n)), Nat.cmp(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), 0n)), c4, c5))))
169  +lhs = Equal.trans(Nat, SF.rne_up(C.high(Nat.add(2n+i, D), m), C.low(Nat.add(2n+i, D), m), C.shift(Nat.add(1n+i, D), 1n)), rne_c(C.high(Nat.add(2n+i, D), m), Nat.cmp(C.low(Nat.add(2n+i, D), m), C.shift(Nat.add(1n+i, D), 1n))), rne_c(C.high(2n+i, C.high(D, m)), NC.lex(Nat.cmp(C.low(1n+i, C.half(C.high(D, m))), C.shift(i, 1n)), Nat.cmp(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), 0n))), rne_cmp(C.high(Nat.add(2n+i, D), m), C.low(Nat.add(2n+i, D), m), C.shift(Nat.add(1n+i, D), 1n)), Equal.trans(Nat, rne_c(C.high(Nat.add(2n+i, D), m), Nat.cmp(C.low(Nat.add(2n+i, D), m), C.shift(Nat.add(1n+i, D), 1n))), rne_c(C.high(2n+i, C.high(D, m)), Nat.cmp(C.low(Nat.add(2n+i, D), m), C.shift(Nat.add(1n+i, D), 1n))), rne_c(C.high(2n+i, C.high(D, m)), NC.lex(Nat.cmp(C.low(1n+i, C.half(C.high(D, m))), C.shift(i, 1n)), Nat.cmp(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), 0n))), Equal.cong(Nat, Nat, z => rne_c(z, Nat.cmp(C.low(Nat.add(2n+i, D), m), C.shift(Nat.add(1n+i, D), 1n))), C.high(Nat.add(2n+i, D), m), C.high(2n+i, C.high(D, m)), qm), Equal.cong(Cmp, Nat, z => rne_c(C.high(2n+i, C.high(D, m)), z), Nat.cmp(C.low(Nat.add(2n+i, D), m), C.shift(Nat.add(1n+i, D), 1n)), NC.lex(Nat.cmp(C.low(1n+i, C.half(C.high(D, m))), C.shift(i, 1n)), Nat.cmp(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), 0n)), cm)))
170  +jf = jam_form(C.high(D, m), C.low(D, m))
171  +hbt = max_le1(C.bit(C.high(D, m)), C.low(D, m), WW.bit_le1(C.high(D, m)))
172  +hJ = Equal.trans(Nat, C.half(SW.jam(C.high(D, m), C.low(D, m))), C.half(Nat.add(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), Nat.double(C.half(C.high(D, m))))), C.half(C.high(D, m)), Equal.cong(Nat, Nat, z => C.half(z), SW.jam(C.high(D, m), C.low(D, m)), Nat.add(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), Nat.double(C.half(C.high(D, m)))), jf), Equal.trans(Nat, C.half(Nat.add(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), Nat.double(C.half(C.high(D, m))))), Nat.add(C.half(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n))), C.half(C.high(D, m))), C.half(C.high(D, m)), WW.half_dbl(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), C.half(C.high(D, m))), Equal.cong(Nat, Nat, z => Nat.add(z, C.half(C.high(D, m))), C.half(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n))), 0n, half_small(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), hbt))))
173  +bJ = Equal.trans(Nat, C.bit(SW.jam(C.high(D, m), C.low(D, m))), C.bit(Nat.add(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), Nat.double(C.half(C.high(D, m))))), Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), Equal.cong(Nat, Nat, z => C.bit(z), SW.jam(C.high(D, m), C.low(D, m)), Nat.add(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), Nat.double(C.half(C.high(D, m)))), jf), Equal.trans(Nat, C.bit(Nat.add(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), Nat.double(C.half(C.high(D, m))))), C.bit(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n))), Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), WW.bit_dbl(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), C.half(C.high(D, m))), bit_small(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), hbt)))
174  +qJ = Equal.cong(Nat, Nat, z => C.high(1n+i, z), C.half(SW.jam(C.high(D, m), C.low(D, m))), C.half(C.high(D, m)), hJ)
175  +lJ = Equal.trans(Nat, Nat.add(C.bit(SW.jam(C.high(D, m), C.low(D, m))), Nat.double(C.low(1n+i, C.half(SW.jam(C.high(D, m), C.low(D, m)))))), Nat.add(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), Nat.double(C.low(1n+i, C.half(SW.jam(C.high(D, m), C.low(D, m)))))), Nat.add(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), Nat.double(C.low(1n+i, C.half(C.high(D, m))))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.double(C.low(1n+i, C.half(SW.jam(C.high(D, m), C.low(D, m)))))), C.bit(SW.jam(C.high(D, m), C.low(D, m))), Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), bJ), Equal.cong(Nat, Nat, z => Nat.add(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), Nat.double(C.low(1n+i, z))), C.half(SW.jam(C.high(D, m), C.low(D, m))), C.half(C.high(D, m)), hJ))
176  +cJ = Equal.trans(Cmp, Nat.cmp(C.low(2n+i, SW.jam(C.high(D, m), C.low(D, m))), C.shift(1n+i, 1n)), Nat.cmp(Nat.add(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), Nat.double(C.low(1n+i, C.half(C.high(D, m))))), C.shift(1n+i, 1n)), NC.lex(Nat.cmp(C.low(1n+i, C.half(C.high(D, m))), C.shift(i, 1n)), Nat.cmp(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), 0n)), Equal.cong(Nat, Cmp, z => Nat.cmp(z, C.shift(1n+i, 1n)), C.low(2n+i, SW.jam(C.high(D, m), C.low(D, m))), Nat.add(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), Nat.double(C.low(1n+i, C.half(C.high(D, m))))), lJ), NC.cmp_limbs(1n, Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), C.low(1n+i, C.half(C.high(D, m))), 0n, C.shift(i, 1n), small(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), hbt), fz(1n)))
177  +rhs = Equal.trans(Nat, SF.rne_up(C.high(2n+i, SW.jam(C.high(D, m), C.low(D, m))), C.low(2n+i, SW.jam(C.high(D, m), C.low(D, m))), C.shift(1n+i, 1n)), rne_c(C.high(2n+i, SW.jam(C.high(D, m), C.low(D, m))), Nat.cmp(C.low(2n+i, SW.jam(C.high(D, m), C.low(D, m))), C.shift(1n+i, 1n))), rne_c(C.high(2n+i, C.high(D, m)), NC.lex(Nat.cmp(C.low(1n+i, C.half(C.high(D, m))), C.shift(i, 1n)), Nat.cmp(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), 0n))), rne_cmp(C.high(2n+i, SW.jam(C.high(D, m), C.low(D, m))), C.low(2n+i, SW.jam(C.high(D, m), C.low(D, m))), C.shift(1n+i, 1n)), Equal.trans(Nat, rne_c(C.high(2n+i, SW.jam(C.high(D, m), C.low(D, m))), Nat.cmp(C.low(2n+i, SW.jam(C.high(D, m), C.low(D, m))), C.shift(1n+i, 1n))), rne_c(C.high(2n+i, C.high(D, m)), Nat.cmp(C.low(2n+i, SW.jam(C.high(D, m), C.low(D, m))), C.shift(1n+i, 1n))), rne_c(C.high(2n+i, C.high(D, m)), NC.lex(Nat.cmp(C.low(1n+i, C.half(C.high(D, m))), C.shift(i, 1n)), Nat.cmp(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), 0n))), Equal.cong(Nat, Nat, z => rne_c(z, Nat.cmp(C.low(2n+i, SW.jam(C.high(D, m), C.low(D, m))), C.shift(1n+i, 1n))), C.high(2n+i, SW.jam(C.high(D, m), C.low(D, m))), C.high(2n+i, C.high(D, m)), qJ), Equal.cong(Cmp, Nat, z => rne_c(C.high(2n+i, C.high(D, m)), z), Nat.cmp(C.low(2n+i, SW.jam(C.high(D, m), C.low(D, m))), C.shift(1n+i, 1n)), NC.lex(Nat.cmp(C.low(1n+i, C.half(C.high(D, m))), C.shift(i, 1n)), Nat.cmp(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), 0n)), cJ)))
178  Equal.trans(Nat, SF.rne_up(C.high(Nat.add(2n+i, D), m), C.low(Nat.add(2n+i, D), m), C.shift(Nat.add(1n+i, D), 1n)), rne_c(C.high(2n+i, C.high(D, m)), NC.lex(Nat.cmp(C.low(1n+i, C.half(C.high(D, m))), C.shift(i, 1n)), Nat.cmp(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), 0n))), SF.rne_up(C.high(2n+i, SW.jam(C.high(D, m), C.low(D, m))), C.low(2n+i, SW.jam(C.high(D, m), C.low(D, m))), C.shift(1n+i, 1n)), lhs, Equal.sym(Nat, SF.rne_up(C.high(2n+i, SW.jam(C.high(D, m), C.low(D, m))), C.low(2n+i, SW.jam(C.high(D, m), C.low(D, m))), C.shift(1n+i, 1n)), rne_c(C.high(2n+i, C.high(D, m)), NC.lex(Nat.cmp(C.low(1n+i, C.half(C.high(D, m))), C.shift(i, 1n)), Nat.cmp(Nat.max(C.bit(C.high(D, m)), Nat.min(C.low(D, m), 1n)), 0n))), rhs))
179
180# ---- SoftFloat's rounding increment: add half an ulp, shift, clear bit 0 on a tie ----
181
182def fits_add1(+k: Nat, +a: Nat, +b: Nat, +ha: {C.fits(k, a) == True{} : Bool}, +hb: {C.fits(k, b) == True{} : Bool}) -> {C.fits(1n+k, Nat.add(a, b)) == True{} : Bool}:
183  +P = C.pow2(k)
184  +h1 = N.lt_add_r2(a, P, b, WW.lt_of_fits(k, a, ha))
185  +h2 = N.lt_add_left(b, P, P, WW.lt_of_fits(k, b, hb))
186  +h3 = N.lt_trans(Nat.add(a, b), Nat.add(P, b), Nat.add(P, P), h1, h2)
187  +h4 = L.subst(Nat, z => {Nat.is_lt(Nat.add(a, b), z) == True{} : Bool}, Nat.add(P, P), Nat.double(P), Equal.sym(Nat, Nat.double(P), Nat.add(P, P), NA.double_self(P)), h3)
188  WW.fits_of_lt(1n+k, Nat.add(a, b), h4)
189
190def bit_le_self(+n: Nat) -> {Nat.is_le(C.bit(n), n) == True{} : Bool}:
191  match n:
192    case 0n:
193      {==}
194    case 1n:
195      {==}
196    case 2n+ +q:
197      N.le_trans(C.bit(q), q, 2n+q, bit_le_self(q), N.le_trans(q, 1n+q, 2n+q, N.le_succ(q), N.le_succ(1n+q)))
198
199def sub_add_r(+a: Nat, +b: Nat, +m: Nat, +h: {Nat.is_le(m, a) == True{} : Bool}) -> {Nat.sub(Nat.add(a, b), m) == Nat.add(Nat.sub(a, m), b) : Nat}:
200  +d = Nat.sub(a, m)
201  Equal.trans(Nat, Nat.sub(Nat.add(a, b), m), Nat.sub(Nat.add(Nat.add(m, d), b), m), Nat.add(d, b), Equal.cong(Nat, Nat, z => Nat.sub(Nat.add(z, b), m), a, Nat.add(m, d), Equal.sym(Nat, Nat.add(m, d), a, N.sub_add(a, m, h))), Equal.trans(Nat, Nat.sub(Nat.add(Nat.add(m, d), b), m), Nat.sub(Nat.add(m, Nat.add(d, b)), m), Nat.add(d, b), Equal.cong(Nat, Nat, z => Nat.sub(z, m), Nat.add(Nat.add(m, d), b), Nat.add(m, Nat.add(d, b)), NA.add_assoc(m, d, b)), N.add_sub_cancel(m, Nat.add(d, b))))
202
203# the value of clear0(r, b): r, or r with bit 0 cleared
204def cvb(+l: U32, +h: U32, +b: Bool) -> {SW.value(X.clear0(WU.U64{l, h}, b)) == SF.pick(Nat, b, Nat.sub(SW.value(WU.U64{l, h}), Nat.mod(SW.value(WU.U64{l, h}), 2n)), SW.value(WU.U64{l, h})) : Nat}:
205  match b:
206    case True{}:
207      +vl = v(l)
208      +S32 = C.shift(32n, v(h))
209      +m = Nat.mod(vl, 2n)
210      +em = LW.odd_val(l)
211      +hle = L.subst(Nat, z => {Nat.is_le(z, vl) == True{} : Bool}, C.bit(vl), m, WW.bit_mod(vl), bit_le_self(vl))
212      +hle2 = L.subst(Nat, z => {Nat.is_le(z, vl) == True{} : Bool}, m, v(U32.and(l, 1)), Equal.sym(Nat, v(U32.and(l, 1)), m, em), hle)
213      +es2 = Equal.trans(Nat, v(U32.sub(l, U32.and(l, 1))), Nat.sub(vl, v(U32.and(l, 1))), Nat.sub(vl, m), U.sub_nat(l, U32.and(l, 1), hle2), Equal.cong(Nat, Nat, z => Nat.sub(vl, z), v(U32.and(l, 1)), m, em))
214      +e1 = Equal.cong(Nat, Nat, z => Nat.add(z, S32), v(U32.sub(l, U32.and(l, 1))), Nat.sub(vl, m), es2)
215      +eo = WW.odd_limb(31n, vl, v(h))
216      +e2 = Equal.trans(Nat, Nat.sub(Nat.add(vl, S32), Nat.mod(Nat.add(vl, S32), 2n)), Nat.sub(Nat.add(vl, S32), m), Nat.add(Nat.sub(vl, m), S32), Equal.cong(Nat, Nat, z => Nat.sub(Nat.add(vl, S32), z), Nat.mod(Nat.add(vl, S32), 2n), m, eo), sub_add_r(vl, S32, m, hle))
217      Equal.trans(Nat, SW.value(X.clear0(WU.U64{l, h}, True{})), Nat.sub(SW.value(WU.U64{l, h}), Nat.mod(SW.value(WU.U64{l, h}), 2n)), SF.pick(Nat, True{}, Nat.sub(SW.value(WU.U64{l, h}), Nat.mod(SW.value(WU.U64{l, h}), 2n)), SW.value(WU.U64{l, h})), Equal.trans(Nat, Nat.add(v(U32.sub(l, U32.and(l, 1))), S32), Nat.add(Nat.sub(vl, m), S32), Nat.sub(Nat.add(vl, S32), Nat.mod(Nat.add(vl, S32), 2n)), e1, Equal.sym(Nat, Nat.sub(Nat.add(vl, S32), Nat.mod(Nat.add(vl, S32), 2n)), Nat.add(Nat.sub(vl, m), S32), e2)), Equal.sym(Nat, SF.pick(Nat, True{}, Nat.sub(SW.value(WU.U64{l, h}), Nat.mod(SW.value(WU.U64{l, h}), 2n)), SW.value(WU.U64{l, h})), Nat.sub(SW.value(WU.U64{l, h}), Nat.mod(SW.value(WU.U64{l, h}), 2n)), pk_t(Nat, Nat.sub(SW.value(WU.U64{l, h}), Nat.mod(SW.value(WU.U64{l, h}), 2n)), SW.value(WU.U64{l, h}))))
218    case False{}:
219      +vl = v(l)
220      +e0 = FB.andm(l, 0n, 0, {==})
221      +hle = L.subst(Nat, z => {Nat.is_le(z, vl) == True{} : Bool}, 0n, v(U32.and(l, 0)), Equal.sym(Nat, v(U32.and(l, 0)), 0n, e0), N.zero_le(vl))
222      +es2 = Equal.trans(Nat, v(U32.sub(l, U32.and(l, 0))), Nat.sub(vl, v(U32.and(l, 0))), vl, U.sub_nat(l, U32.and(l, 0), hle), Equal.trans(Nat, Nat.sub(vl, v(U32.and(l, 0))), Nat.sub(vl, 0n), vl, Equal.cong(Nat, Nat, z => Nat.sub(vl, z), v(U32.and(l, 0)), 0n, e0), N.sub_zero(vl)))
223      Equal.trans(Nat, SW.value(X.clear0(WU.U64{l, h}, False{})), SW.value(WU.U64{l, h}), SF.pick(Nat, False{}, Nat.sub(SW.value(WU.U64{l, h}), Nat.mod(SW.value(WU.U64{l, h}), 2n)), SW.value(WU.U64{l, h})), Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(32n, v(h))), v(U32.sub(l, U32.and(l, 0))), vl, es2), Equal.sym(Nat, SF.pick(Nat, False{}, Nat.sub(SW.value(WU.U64{l, h}), Nat.mod(SW.value(WU.U64{l, h}), 2n)), SW.value(WU.U64{l, h})), SW.value(WU.U64{l, h}), pk_f(Nat, Nat.sub(SW.value(WU.U64{l, h}), Nat.mod(SW.value(WU.U64{l, h}), 2n)), SW.value(WU.U64{l, h}))))
224
225def cv(+r: WU.U64, +b: Bool) -> {SW.value(X.clear0(r, b)) == SF.pick(Nat, b, Nat.sub(SW.value(r), Nat.mod(SW.value(r), 2n)), SW.value(r)) : Nat}:
226  match r:
227    case WU.U64{+l, +h}:
228      cvb(l, h, b)
229
230# the tie test reads the low 10 bits
231def tie_v(+l: U32, +h: U32) -> {U32.is_eq(U32.and(l, 1023), 512) == Nat.is_eq(C.low(10n, SW.value(WU.U64{l, h})), 512n) : Bool}:
232  +e1 = LW.eq_nat(U32.and(l, 1023), 512)
233  +e2 = Equal.cong(Nat, Bool, z => Nat.is_eq(z, 512n), v(U32.and(l, 1023)), C.low(10n, v(l)), FB.andm(l, 10n, 1023, {==}))
234  +e3 = Equal.trans(Nat, C.low(10n, Nat.add(v(l), C.shift(32n, v(h)))), C.low(10n, Nat.add(v(l), C.shift(10n, C.shift(22n, v(h))))), C.low(10n, v(l)), Equal.cong(Nat, Nat, z => C.low(10n, Nat.add(v(l), z)), C.shift(32n, v(h)), C.shift(10n, C.shift(22n, v(h))), WW.shift_comp(10n, 22n, v(h))), WW.low_add_shift(10n, v(l), C.shift(22n, v(h))))
235  Equal.trans(Bool, U32.is_eq(U32.and(l, 1023), 512), Nat.is_eq(C.low(10n, v(l)), 512n), Nat.is_eq(C.low(10n, SW.value(WU.U64{l, h})), 512n), Equal.trans(Bool, U32.is_eq(U32.and(l, 1023), 512), Nat.is_eq(v(U32.and(l, 1023)), 512n), Nat.is_eq(C.low(10n, v(l)), 512n), e1, e2), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 512n), C.low(10n, v(l)), C.low(10n, SW.value(WU.U64{l, h})), Equal.sym(Nat, C.low(10n, SW.value(WU.U64{l, h})), C.low(10n, v(l)), e3)))
236
237def parq(+q: Nat) -> {Nat.add(q, SF.b2n(Nat.is_eq(C.bit(q), 1n))) == Nat.double(C.half(Nat.add(q, 1n))) : Nat}:
238  match q:
239    case 0n:
240      {==}
241    case 1n:
242      {==}
243    case 2n+ +p:
244      Equal.cong(Nat, Nat, z => 2n+z, Nat.add(p, SF.b2n(Nat.is_eq(C.bit(p), 1n))), Nat.double(C.half(Nat.add(p, 1n))), parq(p))
245
246def subm(+n: Nat) -> {Nat.sub(n, Nat.mod(n, 2n)) == Nat.double(C.half(n)) : Nat}:
247  Equal.trans(Nat, Nat.sub(n, Nat.mod(n, 2n)), Nat.sub(n, C.bit(n)), Nat.double(C.half(n)), Equal.cong(Nat, Nat, z => Nat.sub(n, z), Nat.mod(n, 2n), C.bit(n), Equal.sym(Nat, C.bit(n), Nat.mod(n, 2n), WW.bit_mod(n))), Equal.trans(Nat, Nat.sub(n, C.bit(n)), Nat.sub(Nat.add(C.bit(n), Nat.double(C.half(n))), C.bit(n)), Nat.double(C.half(n)), Equal.cong(Nat, Nat, z => Nat.sub(z, C.bit(n)), n, Nat.add(C.bit(n), Nat.double(C.half(n))), WW.hb(n)), N.add_sub_cancel(C.bit(n), Nat.double(C.half(n)))))
248
249def rp_c(+q0: Nat, +r0: Nat, +hr: {C.fits(10n, r0) == True{} : Bool}, +c: Cmp, +hc: {Nat.cmp(r0, 512n) == c : Cmp}) -> {SF.pick(Nat, Nat.is_eq(r0, 512n), Nat.sub(Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), Nat.mod(Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), 2n)), Nat.add(q0, C.high(10n, Nat.add(r0, 512n)))) == SF.rne_up(q0, r0, 512n) : Nat}:
250  match c:
251    case LT{}:
252      +hlt = NC.lt_of_cmp(r0, 512n, hc)
253      +he = Equal.cong(Cmp, Bool, t => Cmp.is_eq(t), Nat.cmp(r0, 512n), LT{}, hc)
254      +hg = Equal.cong(Cmp, Bool, t => Cmp.is_lt(t), Nat.cmp(512n, r0), GT{}, Equal.trans(Cmp, Nat.cmp(512n, r0), SF.flip(Nat.cmp(r0, 512n)), GT{}, Equal.sym(Cmp, SF.flip(Nat.cmp(r0, 512n)), Nat.cmp(512n, r0), NC.cmp_flip(r0, 512n)), Equal.cong(Cmp, Cmp, t => SF.flip(t), Nat.cmp(r0, 512n), LT{}, hc)))
255      +f = WW.fits_of_lt(10n, Nat.add(r0, 512n), N.lt_add_r2(r0, 512n, 512n, hlt))
256      +h0 = N.eq_from_is_eq(C.high(10n, Nat.add(r0, 512n)), 0n, f)
257      +l1 = Equal.cong(Bool, Nat, t => SF.pick(Nat, t, Nat.sub(Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), Nat.mod(Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), 2n)), Nat.add(q0, C.high(10n, Nat.add(r0, 512n)))), Nat.is_eq(r0, 512n), False{}, he)
258      +l2 = Equal.cong(Nat, Nat, z => Nat.add(q0, z), C.high(10n, Nat.add(r0, 512n)), 0n, h0)
259      +r1 = Equal.cong(Bool, Nat, t => Nat.add(q0, SF.b2n(Bool.or(t, Bool.and(Nat.is_eq(r0, 512n), Nat.is_eq(Nat.mod(q0, 2n), 1n))))), Nat.is_lt(512n, r0), False{}, hg)
260      +r2 = Equal.cong(Bool, Nat, t => Nat.add(q0, SF.b2n(Bool.or(False{}, Bool.and(t, Nat.is_eq(Nat.mod(q0, 2n), 1n))))), Nat.is_eq(r0, 512n), False{}, he)
261      Equal.trans(Nat, SF.pick(Nat, Nat.is_eq(r0, 512n), Nat.sub(Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), Nat.mod(Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), 2n)), Nat.add(q0, C.high(10n, Nat.add(r0, 512n)))), Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), SF.rne_up(q0, r0, 512n), l1, Equal.trans(Nat, Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), Nat.add(q0, 0n), SF.rne_up(q0, r0, 512n), l2, Equal.sym(Nat, SF.rne_up(q0, r0, 512n), Nat.add(q0, 0n), Equal.trans(Nat, SF.rne_up(q0, r0, 512n), Nat.add(q0, SF.b2n(Bool.or(False{}, Bool.and(Nat.is_eq(r0, 512n), Nat.is_eq(Nat.mod(q0, 2n), 1n))))), Nat.add(q0, 0n), r1, r2))))
262    case GT{}:
263      +hgt = NC.lt_of_gt(r0, 512n, hc)
264      +he = Equal.cong(Cmp, Bool, t => Cmp.is_eq(t), Nat.cmp(r0, 512n), GT{}, hc)
265      +d = Nat.sub(r0, 512n)
266      +ed = N.sub_add(r0, 512n, N.lt_le(512n, r0, hgt))
267      +ex = Equal.trans(Nat, Nat.add(r0, 512n), Nat.add(Nat.add(512n, d), 512n), Nat.add(d, C.shift(10n, 1n)), Equal.cong(Nat, Nat, z => Nat.add(z, 512n), r0, Nat.add(512n, d), Equal.sym(Nat, Nat.add(512n, d), r0, ed)), Equal.trans(Nat, Nat.add(Nat.add(512n, d), 512n), Nat.add(512n, Nat.add(d, 512n)), Nat.add(d, C.shift(10n, 1n)), NA.add_assoc(512n, d, 512n), Equal.trans(Nat, Nat.add(512n, Nat.add(d, 512n)), Nat.add(1024n, d), Nat.add(d, C.shift(10n, 1n)), Equal.cong(Nat, Nat, z => Nat.add(512n, z), Nat.add(d, 512n), Nat.add(512n, d), NA.add_comm(d, 512n)), NA.add_comm(1024n, d))))
268      +hd = SH.fits_lek(10n, d, r0, UH.sub_le(r0, 512n), hr)
269      +h1 = Equal.trans(Nat, C.high(10n, Nat.add(r0, 512n)), C.high(10n, Nat.add(d, C.shift(10n, 1n))), 1n, Equal.cong(Nat, Nat, z => C.high(10n, z), Nat.add(r0, 512n), Nat.add(d, C.shift(10n, 1n)), ex), WW.high_u(10n, d, 1n, hd))
270      +l1 = Equal.cong(Bool, Nat, t => SF.pick(Nat, t, Nat.sub(Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), Nat.mod(Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), 2n)), Nat.add(q0, C.high(10n, Nat.add(r0, 512n)))), Nat.is_eq(r0, 512n), False{}, he)
271      +l2 = Equal.cong(Nat, Nat, z => Nat.add(q0, z), C.high(10n, Nat.add(r0, 512n)), 1n, h1)
272      +r1 = Equal.cong(Bool, Nat, t => Nat.add(q0, SF.b2n(Bool.or(t, Bool.and(Nat.is_eq(r0, 512n), Nat.is_eq(Nat.mod(q0, 2n), 1n))))), Nat.is_lt(512n, r0), True{}, hgt)
273      Equal.trans(Nat, SF.pick(Nat, Nat.is_eq(r0, 512n), Nat.sub(Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), Nat.mod(Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), 2n)), Nat.add(q0, C.high(10n, Nat.add(r0, 512n)))), Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), SF.rne_up(q0, r0, 512n), l1, Equal.trans(Nat, Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), Nat.add(q0, 1n), SF.rne_up(q0, r0, 512n), l2, Equal.sym(Nat, SF.rne_up(q0, r0, 512n), Nat.add(q0, 1n), r1)))
274    case EQ{}:
275      +er = NC.eq_of_cmp(r0, 512n, hc)
276      +b1 = subm(Nat.add(q0, 1n))
277      +b2 = Equal.trans(Nat, Nat.add(q0, SF.b2n(Nat.is_eq(Nat.mod(q0, 2n), 1n))), Nat.add(q0, SF.b2n(Nat.is_eq(C.bit(q0), 1n))), Nat.double(C.half(Nat.add(q0, 1n))), Equal.cong(Nat, Nat, z => Nat.add(q0, SF.b2n(Nat.is_eq(z, 1n))), Nat.mod(q0, 2n), C.bit(q0), Equal.sym(Nat, C.bit(q0), Nat.mod(q0, 2n), WW.bit_mod(q0))), parq(q0))
278      +base = Equal.trans(Nat, Nat.sub(Nat.add(q0, 1n), Nat.mod(Nat.add(q0, 1n), 2n)), Nat.double(C.half(Nat.add(q0, 1n))), Nat.add(q0, SF.b2n(Nat.is_eq(Nat.mod(q0, 2n), 1n))), b1, Equal.sym(Nat, Nat.add(q0, SF.b2n(Nat.is_eq(Nat.mod(q0, 2n), 1n))), Nat.double(C.half(Nat.add(q0, 1n))), b2))
279      L.subst(Nat, z => {SF.pick(Nat, Nat.is_eq(z, 512n), Nat.sub(Nat.add(q0, C.high(10n, Nat.add(z, 512n))), Nat.mod(Nat.add(q0, C.high(10n, Nat.add(z, 512n))), 2n)), Nat.add(q0, C.high(10n, Nat.add(z, 512n)))) == SF.rne_up(q0, z, 512n) : Nat}, 512n, r0, Equal.sym(Nat, r0, 512n, er), base)
280
281# the rounded significand of roundPackToF64 is rne(sig, 10)
282def rpv(+l: U32, +h: U32, +hS: {C.fits(63n, SW.value(WU.U64{l, h})) == True{} : Bool}) -> {SW.value(X.clear0(X.shr(X.add(WU.U64{l, h}, WU.U64{512, 0}), 10n), U32.is_eq(U32.and(l, 1023), 512))) == SF.rne(SW.value(WU.U64{l, h}), 10n) : Nat}:
283  a1 = WA.add_value(WU.U64{l, h}, WU.U64{512, 0})
284  +ev1 = Equal.trans(Nat, SW.value(X.add(WU.U64{l, h}, WU.U64{512, 0})), C.low(64n, Nat.add(SW.value(WU.U64{l, h}), 512n)), Nat.add(SW.value(WU.U64{l, h}), 512n), a1, WW.low_fit(64n, Nat.add(SW.value(WU.U64{l, h}), 512n), fits_add1(63n, SW.value(WU.U64{l, h}), 512n, hS, {==})))
285  s1 = SH.shr_value(X.add(WU.U64{l, h}, WU.U64{512, 0}), 10n)
286  +ev2 = Equal.trans(Nat, SW.value(X.shr(X.add(WU.U64{l, h}, WU.U64{512, 0}), 10n)), C.high(10n, SW.value(X.add(WU.U64{l, h}, WU.U64{512, 0}))), C.high(10n, Nat.add(SW.value(WU.U64{l, h}), 512n)), s1, Equal.cong(Nat, Nat, z => C.high(10n, z), SW.value(X.add(WU.U64{l, h}, WU.U64{512, 0})), Nat.add(SW.value(WU.U64{l, h}), 512n), ev1))
287  +sp = Equal.trans(Nat, C.high(10n, Nat.add(SW.value(WU.U64{l, h}), 512n)), C.high(10n, Nat.add(Nat.add(C.low(10n, SW.value(WU.U64{l, h})), C.shift(10n, C.high(10n, SW.value(WU.U64{l, h})))), 512n)), Nat.add(C.high(10n, SW.value(WU.U64{l, h})), C.high(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n))), Equal.cong(Nat, Nat, z => C.high(10n, Nat.add(z, 512n)), SW.value(WU.U64{l, h}), Nat.add(C.low(10n, SW.value(WU.U64{l, h})), C.shift(10n, C.high(10n, SW.value(WU.U64{l, h})))), WW.low_high(10n, SW.value(WU.U64{l, h}))), Equal.trans(Nat, C.high(10n, Nat.add(Nat.add(C.low(10n, SW.value(WU.U64{l, h})), C.shift(10n, C.high(10n, SW.value(WU.U64{l, h})))), 512n)), C.high(10n, Nat.add(Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n), C.shift(10n, C.high(10n, SW.value(WU.U64{l, h}))))), Nat.add(C.high(10n, SW.value(WU.U64{l, h})), C.high(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n))), Equal.cong(Nat, Nat, z => C.high(10n, z), Nat.add(Nat.add(C.low(10n, SW.value(WU.U64{l, h})), C.shift(10n, C.high(10n, SW.value(WU.U64{l, h})))), 512n), Nat.add(Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n), C.shift(10n, C.high(10n, SW.value(WU.U64{l, h})))), A.add_rot(C.low(10n, SW.value(WU.U64{l, h})), C.shift(10n, C.high(10n, SW.value(WU.U64{l, h}))), 512n)), Equal.trans(Nat, C.high(10n, Nat.add(Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n), C.shift(10n, C.high(10n, SW.value(WU.U64{l, h}))))), Nat.add(C.high(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n)), C.high(10n, SW.value(WU.U64{l, h}))), Nat.add(C.high(10n, SW.value(WU.U64{l, h})), C.high(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n))), WW.high_add_shift(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n), C.high(10n, SW.value(WU.U64{l, h}))), NA.add_comm(C.high(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n)), C.high(10n, SW.value(WU.U64{l, h}))))))
288  +ev3 = Equal.trans(Nat, SW.value(X.shr(X.add(WU.U64{l, h}, WU.U64{512, 0}), 10n)), C.high(10n, Nat.add(SW.value(WU.U64{l, h}), 512n)), Nat.add(C.high(10n, SW.value(WU.U64{l, h})), C.high(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n))), ev2, sp)
289  +ec = cv(X.shr(X.add(WU.U64{l, h}, WU.U64{512, 0}), 10n), U32.is_eq(U32.and(l, 1023), 512))
290  +e4 = Equal.cong(Nat, Nat, z => SF.pick(Nat, U32.is_eq(U32.and(l, 1023), 512), Nat.sub(z, Nat.mod(z, 2n)), z), SW.value(X.shr(X.add(WU.U64{l, h}, WU.U64{512, 0}), 10n)), Nat.add(C.high(10n, SW.value(WU.U64{l, h})), C.high(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n))), ev3)
291  +e5 = Equal.cong(Bool, Nat, t => SF.pick(Nat, t, Nat.sub(Nat.add(C.high(10n, SW.value(WU.U64{l, h})), C.high(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n))), Nat.mod(Nat.add(C.high(10n, SW.value(WU.U64{l, h})), C.high(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n))), 2n)), Nat.add(C.high(10n, SW.value(WU.U64{l, h})), C.high(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n)))), U32.is_eq(U32.and(l, 1023), 512), Nat.is_eq(C.low(10n, SW.value(WU.U64{l, h})), 512n), tie_v(l, h))
292  Equal.trans(Nat, SW.value(X.clear0(X.shr(X.add(WU.U64{l, h}, WU.U64{512, 0}), 10n), U32.is_eq(U32.and(l, 1023), 512))), SF.pick(Nat, U32.is_eq(U32.and(l, 1023), 512), Nat.sub(SW.value(X.shr(X.add(WU.U64{l, h}, WU.U64{512, 0}), 10n)), Nat.mod(SW.value(X.shr(X.add(WU.U64{l, h}, WU.U64{512, 0}), 10n)), 2n)), SW.value(X.shr(X.add(WU.U64{l, h}, WU.U64{512, 0}), 10n))), SF.rne_up(C.high(10n, SW.value(WU.U64{l, h})), C.low(10n, SW.value(WU.U64{l, h})), 512n), ec, Equal.trans(Nat, SF.pick(Nat, U32.is_eq(U32.and(l, 1023), 512), Nat.sub(SW.value(X.shr(X.add(WU.U64{l, h}, WU.U64{512, 0}), 10n)), Nat.mod(SW.value(X.shr(X.add(WU.U64{l, h}, WU.U64{512, 0}), 10n)), 2n)), SW.value(X.shr(X.add(WU.U64{l, h}, WU.U64{512, 0}), 10n))), SF.pick(Nat, U32.is_eq(U32.and(l, 1023), 512), Nat.sub(Nat.add(C.high(10n, SW.value(WU.U64{l, h})), C.high(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n))), Nat.mod(Nat.add(C.high(10n, SW.value(WU.U64{l, h})), C.high(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n))), 2n)), Nat.add(C.high(10n, SW.value(WU.U64{l, h})), C.high(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n)))), SF.rne_up(C.high(10n, SW.value(WU.U64{l, h})), C.low(10n, SW.value(WU.U64{l, h})), 512n), e4, Equal.trans(Nat, SF.pick(Nat, U32.is_eq(U32.and(l, 1023), 512), Nat.sub(Nat.add(C.high(10n, SW.value(WU.U64{l, h})), C.high(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n))), Nat.mod(Nat.add(C.high(10n, SW.value(WU.U64{l, h})), C.high(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n))), 2n)), Nat.add(C.high(10n, SW.value(WU.U64{l, h})), C.high(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n)))), SF.pick(Nat, Nat.is_eq(C.low(10n, SW.value(WU.U64{l, h})), 512n), Nat.sub(Nat.add(C.high(10n, SW.value(WU.U64{l, h})), C.high(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n))), Nat.mod(Nat.add(C.high(10n, SW.value(WU.U64{l, h})), C.high(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n))), 2n)), Nat.add(C.high(10n, SW.value(WU.U64{l, h})), C.high(10n, Nat.add(C.low(10n, SW.value(WU.U64{l, h})), 512n)))), SF.rne_up(C.high(10n, SW.value(WU.U64{l, h})), C.low(10n, SW.value(WU.U64{l, h})), 512n), e5, rp_c(C.high(10n, SW.value(WU.U64{l, h})), C.low(10n, SW.value(WU.U64{l, h})), WW.low_fits(10n, SW.value(WU.U64{l, h})), Nat.cmp(C.low(10n, SW.value(WU.U64{l, h})), 512n), {==}))))
293
294# ---- packing: a 64-bit word whose value is n + 2^63 s is bits(s, n) ----
295
296def bits_of(+s: Bool, +n: Nat, +w: WU.U64, +hw: {SW.value(w) == Nat.add(n, C.shift(63n, SF.b2n(s))) : Nat}) -> {F.pack64(w) == bits(s, n) : F.F64}:
297  +lo = X.lo(w)
298  +hi = X.hi(w)
299  +t = C.shift(31n, SF.b2n(s))
300  +e63 = WW.shift_comp(32n, 31n, SF.b2n(s))
301  +ew = Equal.trans(Nat, Nat.add(v(lo), C.shift(32n, v(hi))), SW.value(w), Nat.add(n, C.shift(32n, t)), Equal.sym(Nat, SW.value(w), Nat.add(v(lo), C.shift(32n, v(hi))), WA.val_eta(w)), Equal.trans(Nat, SW.value(w), Nat.add(n, C.shift(63n, SF.b2n(s))), Nat.add(n, C.shift(32n, t)), hw, Equal.cong(Nat, Nat, z => Nat.add(n, z), C.shift(63n, SF.b2n(s)), C.shift(32n, t), e63)))
302  +el = Equal.trans(Nat, C.low(32n, n), C.low(32n, Nat.add(n, C.shift(32n, t))), v(lo), Equal.sym(Nat, C.low(32n, Nat.add(n, C.shift(32n, t))), C.low(32n, n), WW.low_add_shift(32n, n, t)), Equal.trans(Nat, C.low(32n, Nat.add(n, C.shift(32n, t))), C.low(32n, Nat.add(v(lo), C.shift(32n, v(hi)))), v(lo), Equal.cong(Nat, Nat, z => C.low(32n, z), Nat.add(n, C.shift(32n, t)), Nat.add(v(lo), C.shift(32n, v(hi))), Equal.sym(Nat, Nat.add(v(lo), C.shift(32n, v(hi))), Nat.add(n, C.shift(32n, t)), ew)), WW.low_u(32n, v(lo), v(hi), LW.vb(lo))))
303  +eh = Equal.trans(Nat, Nat.add(C.high(32n, n), t), C.high(32n, Nat.add(n, C.shift(32n, t))), v(hi), Equal.sym(Nat, C.high(32n, Nat.add(n, C.shift(32n, t))), Nat.add(C.high(32n, n), t), WW.high_add_shift(32n, n, t)), Equal.trans(Nat, C.high(32n, Nat.add(n, C.shift(32n, t))), C.high(32n, Nat.add(v(lo), C.shift(32n, v(hi)))), v(hi), Equal.cong(Nat, Nat, z => C.high(32n, z), Nat.add(n, C.shift(32n, t)), Nat.add(v(lo), C.shift(32n, v(hi))), Equal.sym(Nat, Nat.add(v(lo), C.shift(32n, v(hi))), Nat.add(n, C.shift(32n, t)), ew)), WW.high_u(32n, v(lo), v(hi), LW.vb(lo))))
304  +ul = Equal.trans(U32, U32.from_nat(C.low(32n, n)), U32.from_nat(v(lo)), lo, Equal.cong(Nat, U32, z => U32.from_nat(z), C.low(32n, n), v(lo), el), LW.rt(lo))
305  +uh = Equal.trans(U32, U32.from_nat(Nat.add(C.high(32n, n), t)), U32.from_nat(v(hi)), hi, Equal.cong(Nat, U32, z => U32.from_nat(z), Nat.add(C.high(32n, n), t), v(hi), eh), LW.rt(hi))
306  +e = Equal.trans(F.F64, bits(s, n), F.Bits{lo, U32.from_nat(Nat.add(C.high(32n, n), t))}, F.Bits{lo, hi}, Equal.cong(U32, F.F64, z => F.Bits{z, U32.from_nat(Nat.add(C.high(32n, n), t))}, U32.from_nat(C.low(32n, n)), lo, ul), Equal.cong(U32, F.F64, z => F.Bits{lo, z}, U32.from_nat(Nat.add(C.high(32n, n), t)), hi, uh))
307  Equal.sym(F.F64, bits(s, n), F.Bits{lo, hi}, e)
308
309def sgn_pick(+s: Bool) -> {F.sgn(s) == SF.pick(U32, s, 2147483648, 0) : U32}:
310  match s:
311    case True{}:
312      Equal.trans(U32, F.sgn(True{}), 2147483648, SF.pick(U32, True{}, 2147483648, 0), {==}, Equal.sym(U32, SF.pick(U32, True{}, 2147483648, 0), 2147483648, pk_t(U32, 2147483648, 0)))
313    case False{}:
314      Equal.trans(U32, F.sgn(False{}), 0, SF.pick(U32, False{}, 2147483648, 0), {==}, Equal.sym(U32, SF.pick(U32, False{}, 2147483648, 0), 0, pk_f(U32, 2147483648, 0)))
315
316def pb(+s: Bool, +one: Nat, +h1: {one == 1n : Nat}) -> {SF.pick(Nat, s, one, 0n) == SF.b2n(s) : Nat}:
317  match s:
318    case True{}:
319      Equal.trans(Nat, SF.pick(Nat, True{}, one, 0n), one, SF.b2n(True{}), pk_t(Nat, one, 0n), h1)
320    case False{}:
321      Equal.trans(Nat, SF.pick(Nat, False{}, one, 0n), 0n, SF.b2n(False{}), pk_f(Nat, one, 0n), {==})
322
323def sgv0(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +c: U32, +hc: {c == U32{WD.pw(32n, 31n)} : U32}) -> {v(SF.pick(U32, s, c, 0)) == C.shift(31n, SF.pick(Nat, s, one, 0n)) : Nat}:
324  match s:
325    case True{}:
326      FB.pwv(31n, {==}, one, h1, c, hc)
327    case False{}:
328      {==}
329
330def sgv(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +c: U32, +hc: {c == U32{WD.pw(32n, 31n)} : U32}) -> {v(SF.pick(U32, s, c, 0)) == C.shift(31n, SF.b2n(s)) : Nat}:
331  Equal.trans(Nat, v(SF.pick(U32, s, c, 0)), C.shift(31n, SF.pick(Nat, s, one, 0n)), C.shift(31n, SF.b2n(s)), sgv0(one, h1, s, c, hc), Equal.cong(Nat, Nat, z => C.shift(31n, z), SF.pick(Nat, s, one, 0n), SF.b2n(s), pb(s, one, h1)))
332
333def b2n_le(+s: Bool) -> {C.fits(1n, SF.b2n(s)) == True{} : Bool}:
334  match s:
335    case True{}:
336      {==}
337    case False{}:
338      {==}
339
340# a product below 2^32 is exact
341def mulv(+one: Nat, +h1: {one == 1n : Nat}, +a: U32, +c: U32, +h: {Nat.is_lt(Nat.mul(v(a), v(c)), C.shift(32n, one)) == True{} : Bool}) -> {v(U32.mul(a, c)) == Nat.mul(v(a), v(c)) : Nat}:
342  match a c:
343    case U32{+x} U32{+y}:
344      +ex = U.to_nat_word(x)
345      +ey = U.to_nat_word(y)
346      +es = Equal.trans(Nat, Nat.mul(v(U32{x}), v(U32{y})), Nat.mul(S.unsigned(32n, x), v(U32{y})), Nat.mul(S.unsigned(32n, x), S.unsigned(32n, y)), Equal.cong(Nat, Nat, z => Nat.mul(z, v(U32{y})), v(U32{x}), S.unsigned(32n, x), ex), Equal.cong(Nat, Nat, z => Nat.mul(S.unsigned(32n, x), z), v(U32{y}), S.unsigned(32n, y), ey))
347      +h2 = L.subst(Nat, z => {Nat.is_lt(z, C.shift(32n, one)) == True{} : Bool}, Nat.mul(v(U32{x}), v(U32{y})), Nat.mul(S.unsigned(32n, x), S.unsigned(32n, y)), es, h)
348      +h3 = L.subst(Nat, z => {Nat.is_lt(Nat.mul(S.unsigned(32n, x), S.unsigned(32n, y)), z) == True{} : Bool}, C.shift(32n, one), S.scale_binary(32n, one), Equal.sym(Nat, S.scale_binary(32n, one), C.shift(32n, one), FB.sb(32n, one)), h2)
349      +m = Word.mul(32n, x, y)
350      Equal.trans(Nat, U32.to_nat(U32{m}), S.unsigned(32n, m), Nat.mul(v(U32{x}), v(U32{y})), U.to_nat_word(m), Equal.trans(Nat, S.unsigned(32n, m), Nat.mul(S.unsigned(32n, x), S.unsigned(32n, y)), Nat.mul(v(U32{x}), v(U32{y})), WD.mul_exact(32n, one, h1, x, y, h3), Equal.sym(Nat, Nat.mul(v(U32{x}), v(U32{y})), Nat.mul(S.unsigned(32n, x), S.unsigned(32n, y)), es)))
351
352# the high word of packToF64's addend: 2^31 s + 2^20 e
353def hwv(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +e: Nat, +he: {C.fits(11n, e) == True{} : Bool}, +c31: U32, +hc31: {c31 == U32{WD.pw(32n, 31n)} : U32}, +c20: U32, +hc20: {c20 == U32{WD.pw(32n, 20n)} : U32}) -> {v(U32.add(SF.pick(U32, s, c31, 0), U32.mul(U32.from_nat(e), c20))) == Nat.add(C.shift(31n, SF.b2n(s)), C.shift(20n, e)) : Nat}:
354  +efe = LW.vo(e, SH.fits_mono(11n, 32n, e, {==}, he))
355  +ec = FB.pwv(20n, {==}, one, h1, c20, hc20)
356  +ep = Equal.trans(Nat, Nat.mul(v(U32.from_nat(e)), v(c20)), Nat.mul(e, v(c20)), C.shift(20n, e), Equal.cong(Nat, Nat, z => Nat.mul(z, v(c20)), v(U32.from_nat(e)), e, efe), Equal.trans(Nat, Nat.mul(e, v(c20)), Nat.mul(e, C.shift(20n, one)), C.shift(20n, e), Equal.cong(Nat, Nat, z => Nat.mul(e, z), v(c20), C.shift(20n, one), ec), Equal.sym(Nat, C.shift(20n, e), Nat.mul(e, C.shift(20n, one)), WW.shift_mul_one(20n, one, h1, e))))
357  +f31 = L.subst(Nat, z => {C.fits(31n, z) == True{} : Bool}, Nat.add(0n, C.shift(20n, e)), C.shift(20n, e), {==}, WW.limbs_fit(20n, 11n, 0n, e, fz(20n), he))
358  +f32 = SH.fits_mono(31n, 32n, C.shift(20n, e), {==}, f31)
359  +hl = L.subst(Nat, z => {Nat.is_lt(z, C.shift(32n, one)) == True{} : Bool}, C.shift(20n, e), Nat.mul(v(U32.from_nat(e)), v(c20)), Equal.sym(Nat, Nat.mul(v(U32.from_nat(e)), v(c20)), C.shift(20n, e), ep), WW.lt_one(32n, one, h1, C.shift(20n, e), f32))
360  +emm = Equal.trans(Nat, v(U32.mul(U32.from_nat(e), c20)), Nat.mul(v(U32.from_nat(e)), v(c20)), C.shift(20n, e), mulv(one, h1, U32.from_nat(e), c20, hl), ep)
361  +esg = sgv(one, h1, s, c31, hc31)
362  +esum = Equal.trans(Nat, Nat.add(v(SF.pick(U32, s, c31, 0)), v(U32.mul(U32.from_nat(e), c20))), Nat.add(C.shift(31n, SF.b2n(s)), v(U32.mul(U32.from_nat(e), c20))), Nat.add(C.shift(31n, SF.b2n(s)), C.shift(20n, e)), Equal.cong(Nat, Nat, z => Nat.add(z, v(U32.mul(U32.from_nat(e), c20))), v(SF.pick(U32, s, c31, 0)), C.shift(31n, SF.b2n(s)), esg), Equal.cong(Nat, Nat, z => Nat.add(C.shift(31n, SF.b2n(s)), z), v(U32.mul(U32.from_nat(e), c20)), C.shift(20n, e), emm))
363  +f2 = WW.limbs_fit(31n, 1n, C.shift(20n, e), SF.b2n(s), f31, b2n_le(s))
364  +f3 = L.subst(Nat, z => {C.fits(32n, z) == True{} : Bool}, Nat.add(C.shift(20n, e), C.shift(31n, SF.b2n(s))), Nat.add(C.shift(31n, SF.b2n(s)), C.shift(20n, e)), NA.add_comm(C.shift(20n, e), C.shift(31n, SF.b2n(s))), f2)
365  +hl2 = L.subst(Nat, z => {Nat.is_lt(z, C.shift(32n, one)) == True{} : Bool}, Nat.add(C.shift(31n, SF.b2n(s)), C.shift(20n, e)), Nat.add(v(SF.pick(U32, s, c31, 0)), v(U32.mul(U32.from_nat(e), c20))), Equal.sym(Nat, Nat.add(v(SF.pick(U32, s, c31, 0)), v(U32.mul(U32.from_nat(e), c20))), Nat.add(C.shift(31n, SF.b2n(s)), C.shift(20n, e)), esum), WW.lt_one(32n, one, h1, Nat.add(C.shift(31n, SF.b2n(s)), C.shift(20n, e)), f3))
366  Equal.trans(Nat, v(U32.add(SF.pick(U32, s, c31, 0), U32.mul(U32.from_nat(e), c20))), Nat.add(v(SF.pick(U32, s, c31, 0)), v(U32.mul(U32.from_nat(e), c20))), Nat.add(C.shift(31n, SF.b2n(s)), C.shift(20n, e)), FB.addv(one, h1, SF.pick(U32, s, c31, 0), U32.mul(U32.from_nat(e), c20), hl2), esum)
367
368# SoftFloat's packToF64: the pattern of (s, e, m) is bits(s, m + 2^52 e)
369def pack_g(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +e: Nat, +he: {C.fits(11n, e) == True{} : Bool}, +m: WU.U64, +hn: {C.fits(63n, Nat.add(SW.value(m), C.shift(52n, e))) == True{} : Bool}, +c31: U32, +hc31: {c31 == U32{WD.pw(32n, 31n)} : U32}, +c20: U32, +hc20: {c20 == U32{WD.pw(32n, 20n)} : U32}) -> {F.pack64(X.add(WU.U64{0, U32.add(SF.pick(U32, s, c31, 0), U32.mul(U32.from_nat(e), c20))}, m)) == bits(s, Nat.add(SW.value(m), C.shift(52n, e))) : F.F64}:
370  +ep = Equal.trans(Nat, SW.value(WU.U64{0, U32.add(SF.pick(U32, s, c31, 0), U32.mul(U32.from_nat(e), c20))}), C.shift(32n, Nat.add(C.shift(31n, SF.b2n(s)), C.shift(20n, e))), Nat.add(C.shift(63n, SF.b2n(s)), C.shift(52n, e)), Equal.cong(Nat, Nat, z => C.shift(32n, z), v(U32.add(SF.pick(U32, s, c31, 0), U32.mul(U32.from_nat(e), c20))), Nat.add(C.shift(31n, SF.b2n(s)), C.shift(20n, e)), hwv(one, h1, s, e, he, c31, hc31, c20, hc20)), Equal.trans(Nat, C.shift(32n, Nat.add(C.shift(31n, SF.b2n(s)), C.shift(20n, e))), Nat.add(C.shift(32n, C.shift(31n, SF.b2n(s))), C.shift(32n, C.shift(20n, e))), Nat.add(C.shift(63n, SF.b2n(s)), C.shift(52n, e)), WW.shift_add(32n, C.shift(31n, SF.b2n(s)), C.shift(20n, e)), Equal.trans(Nat, Nat.add(C.shift(32n, C.shift(31n, SF.b2n(s))), C.shift(32n, C.shift(20n, e))), Nat.add(C.shift(63n, SF.b2n(s)), C.shift(32n, C.shift(20n, e))), Nat.add(C.shift(63n, SF.b2n(s)), C.shift(52n, e)), Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(32n, C.shift(20n, e))), C.shift(32n, C.shift(31n, SF.b2n(s))), C.shift(63n, SF.b2n(s)), Equal.sym(Nat, C.shift(63n, SF.b2n(s)), C.shift(32n, C.shift(31n, SF.b2n(s))), WW.shift_comp(32n, 31n, SF.b2n(s)))), Equal.cong(Nat, Nat, z => Nat.add(C.shift(63n, SF.b2n(s)), z), C.shift(32n, C.shift(20n, e)), C.shift(52n, e), Equal.sym(Nat, C.shift(52n, e), C.shift(32n, C.shift(20n, e)), WW.shift_comp(32n, 20n, e))))))
371  +es = Equal.trans(Nat, Nat.add(SW.value(WU.U64{0, U32.add(SF.pick(U32, s, c31, 0), U32.mul(U32.from_nat(e), c20))}), SW.value(m)), Nat.add(Nat.add(C.shift(63n, SF.b2n(s)), C.shift(52n, e)), SW.value(m)), Nat.add(Nat.add(SW.value(m), C.shift(52n, e)), C.shift(63n, SF.b2n(s))), Equal.cong(Nat, Nat, z => Nat.add(z, SW.value(m)), SW.value(WU.U64{0, U32.add(SF.pick(U32, s, c31, 0), U32.mul(U32.from_nat(e), c20))}), Nat.add(C.shift(63n, SF.b2n(s)), C.shift(52n, e)), ep), Equal.trans(Nat, Nat.add(Nat.add(C.shift(63n, SF.b2n(s)), C.shift(52n, e)), SW.value(m)), Nat.add(C.shift(63n, SF.b2n(s)), Nat.add(C.shift(52n, e), SW.value(m))), Nat.add(Nat.add(SW.value(m), C.shift(52n, e)), C.shift(63n, SF.b2n(s))), NA.add_assoc(C.shift(63n, SF.b2n(s)), C.shift(52n, e), SW.value(m)), Equal.trans(Nat, Nat.add(C.shift(63n, SF.b2n(s)), Nat.add(C.shift(52n, e), SW.value(m))), Nat.add(C.shift(63n, SF.b2n(s)), Nat.add(SW.value(m), C.shift(52n, e))), Nat.add(Nat.add(SW.value(m), C.shift(52n, e)), C.shift(63n, SF.b2n(s))), Equal.cong(Nat, Nat, z => Nat.add(C.shift(63n, SF.b2n(s)), z), Nat.add(C.shift(52n, e), SW.value(m)), Nat.add(SW.value(m), C.shift(52n, e)), NA.add_comm(C.shift(52n, e), SW.value(m))), NA.add_comm(C.shift(63n, SF.b2n(s)), Nat.add(SW.value(m), C.shift(52n, e))))))
372  +f64 = WW.limbs_fit(63n, 1n, Nat.add(SW.value(m), C.shift(52n, e)), SF.b2n(s), hn, b2n_le(s))
373  a1 = WA.add_value(WU.U64{0, U32.add(SF.pick(U32, s, c31, 0), U32.mul(U32.from_nat(e), c20))}, m)
374  +ev = Equal.trans(Nat, SW.value(X.add(WU.U64{0, U32.add(SF.pick(U32, s, c31, 0), U32.mul(U32.from_nat(e), c20))}, m)), C.low(64n, Nat.add(SW.value(WU.U64{0, U32.add(SF.pick(U32, s, c31, 0), U32.mul(U32.from_nat(e), c20))}), SW.value(m))), Nat.add(Nat.add(SW.value(m), C.shift(52n, e)), C.shift(63n, SF.b2n(s))), a1, Equal.trans(Nat, C.low(64n, Nat.add(SW.value(WU.U64{0, U32.add(SF.pick(U32, s, c31, 0), U32.mul(U32.from_nat(e), c20))}), SW.value(m))), C.low(64n, Nat.add(Nat.add(SW.value(m), C.shift(52n, e)), C.shift(63n, SF.b2n(s)))), Nat.add(Nat.add(SW.value(m), C.shift(52n, e)), C.shift(63n, SF.b2n(s))), Equal.cong(Nat, Nat, z => C.low(64n, z), Nat.add(SW.value(WU.U64{0, U32.add(SF.pick(U32, s, c31, 0), U32.mul(U32.from_nat(e), c20))}), SW.value(m)), Nat.add(Nat.add(SW.value(m), C.shift(52n, e)), C.shift(63n, SF.b2n(s))), es), WW.low_fit(64n, Nat.add(Nat.add(SW.value(m), C.shift(52n, e)), C.shift(63n, SF.b2n(s))), f64)))
375  bits_of(s, Nat.add(SW.value(m), C.shift(52n, e)), X.add(WU.U64{0, U32.add(SF.pick(U32, s, c31, 0), U32.mul(U32.from_nat(e), c20))}, m), ev)
376
377def pack_v(+s: Bool, +e: Nat, +he: {C.fits(11n, e) == True{} : Bool}, +m: WU.U64, +hn: {C.fits(63n, Nat.add(SW.value(m), C.shift(52n, e))) == True{} : Bool}) -> {F.pack(s, e, m) == bits(s, Nat.add(SW.value(m), C.shift(52n, e))) : F.F64}:
378  +e0 = Equal.cong(U32, F.F64, z => F.pack64(X.add(WU.U64{0, U32.add(z, U32.mul(U32.from_nat(e), 1048576))}, m)), F.sgn(s), SF.pick(U32, s, 2147483648, 0), sgn_pick(s))
379  Equal.trans(F.F64, F.pack(s, e, m), F.pack64(X.add(WU.U64{0, U32.add(SF.pick(U32, s, 2147483648, 0), U32.mul(U32.from_nat(e), 1048576))}, m)), bits(s, Nat.add(SW.value(m), C.shift(52n, e))), e0, pack_g(1n, {==}, s, e, he, m, hn, 2147483648, {==}, 1048576, {==}))
380
381def inf_v(+s: Bool) -> {F.inf(s) == SF.inf(s) : F.F64}:
382  match s:
383    case True{}:
384      {==}
385    case False{}:
386      {==}
387
388# ---- bit lengths and the bounds of the rounded significand ----
389
390def bl_gt(+k: Nat, +n: Nat, +h1: {C.fits(k, n) == False{} : Bool}, +h2: {C.fits(1n+k, n) == True{} : Bool}, +hg: {Nat.is_le(C.pow2(2n+k), C.pow2(M.bit_length(n))) == True{} : Bool}) -> {M.bit_length(n) == 1n+k : Nat}:
391  match n:
392    case 0n:
393      NC.absurd_tf({M.bit_length(0n) == 1n+k : Nat}, Equal.trans(Bool, False{}, C.fits(k, 0n), True{}, Equal.sym(Bool, C.fits(k, 0n), False{}, h1), fz(k)))
394    case 1n+ +np:
395      +P = C.pow2(2n+k)
396      +hd = N.double_lt(1n+np, C.pow2(1n+k), WW.lt_of_fits(1n+k, 1n+np, h2))
397      +hle = N.le_trans(P, C.pow2(M.bit_length(1n+np)), Nat.double(1n+np), hg, BT.bit_length_le(np))
398      NC.absurd_tf({M.bit_length(1n+np) == 1n+k : Nat}, Equal.trans(Bool, False{}, Nat.is_lt(P, P), True{}, Equal.sym(Bool, Nat.is_lt(P, P), False{}, N.lt_irrefl(P)), N.le_lt_trans(P, Nat.double(1n+np), P, hle, hd)))
399
400def bl_c(+k: Nat, +n: Nat, +h1: {C.fits(k, n) == False{} : Bool}, +h2: {C.fits(1n+k, n) == True{} : Bool}, +c: Cmp, +hc: {Nat.cmp(M.bit_length(n), 1n+k) == c : Cmp}) -> {M.bit_length(n) == 1n+k : Nat}:
401  match c:
402    case EQ{}:
403      NC.eq_of_cmp(M.bit_length(n), 1n+k, hc)
404    case LT{}:
405      +hl = N.lt_succ_le(M.bit_length(n), k, NC.lt_of_cmp(M.bit_length(n), 1n+k, hc))
406      +hn = N.lt_le_trans(n, C.pow2(M.bit_length(n)), C.pow2(k), BT.bit_length_lt(n), N.pow2_mono(M.bit_length(n), k, hl))
407      NC.absurd_tf({M.bit_length(n) == 1n+k : Nat}, Equal.trans(Bool, False{}, C.fits(k, n), True{}, Equal.sym(Bool, C.fits(k, n), False{}, h1), WW.fits_of_lt(k, n, hn)))
408    case GT{}:
409      +hg = N.pow2_mono(2n+k, M.bit_length(n), N.lt_succ_le_succ(1n+k, M.bit_length(n), NC.lt_of_gt(M.bit_length(n), 1n+k, hc)))
410      bl_gt(k, n, h1, h2, hg)
411
412def bl63(+m: Nat, +h1: {C.fits(62n, m) == False{} : Bool}, +h2: {C.fits(63n, m) == True{} : Bool}) -> {M.bit_length(m) == 63n : Nat}:
413  bl_c(62n, m, h1, h2, Nat.cmp(M.bit_length(m), 63n), {==})
414
415def nz_of(+k: Nat, +m: Nat, +h1: {C.fits(k, m) == False{} : Bool}) -> {Nat.is_eq(m, 0n) == False{} : Bool}:
416  match m:
417    case 0n:
418      NC.absurd_tf({Nat.is_eq(0n, 0n) == False{} : Bool}, Equal.trans(Bool, False{}, C.fits(k, 0n), True{}, Equal.sym(Bool, C.fits(k, 0n), False{}, h1), fz(k)))
419    case 1n+ +mp:
420      {==}
421
422# fits(a + b, n) is fits(b, n >> a)
423def fits_hc(+a: Nat, +b: Nat, +n: Nat) -> {C.fits(Nat.add(a, b), n) == C.fits(b, C.high(a, n)) : Bool}:
424  Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), C.high(Nat.add(a, b), n), C.high(b, C.high(a, n)), WW.high_comp(b, a, n))
425
426def b2n_le1(+c: Bool) -> {Nat.is_le(SF.b2n(c), 1n) == True{} : Bool}:
427  match c:
428    case True{}:
429      {==}
430    case False{}:
431      {==}
432
433def rne_lb(+m: Nat) -> {Nat.is_le(C.high(10n, m), SF.rne(m, 10n)) == True{} : Bool}:
434  N.le_add_right(C.high(10n, m), SF.b2n(Bool.or(Nat.is_lt(512n, C.low(10n, m)), Bool.and(Nat.is_eq(C.low(10n, m), 512n), Nat.is_eq(Nat.mod(C.high(10n, m), 2n), 1n)))))
435
436def rne_ub(+m: Nat) -> {Nat.is_le(SF.rne(m, 10n), Nat.add(C.high(10n, m), 1n)) == True{} : Bool}:
437  N.le_add_left(SF.b2n(Bool.or(Nat.is_lt(512n, C.low(10n, m)), Bool.and(Nat.is_eq(C.low(10n, m), 512n), Nat.is_eq(Nat.mod(C.high(10n, m), 2n), 1n)))), 1n, C.high(10n, m), b2n_le1(Bool.or(Nat.is_lt(512n, C.low(10n, m)), Bool.and(Nat.is_eq(C.low(10n, m), 512n), Nat.is_eq(Nat.mod(C.high(10n, m), 2n), 1n)))))
438
439def succ_le(+a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_le(Nat.add(a, 1n), b) == True{} : Bool}:
440  L.subst(Nat, z => {Nat.is_le(z, b) == True{} : Bool}, 1n+a, Nat.add(a, 1n), Equal.sym(Nat, Nat.add(a, 1n), 1n+a, Equal.trans(Nat, Nat.add(a, 1n), Nat.add(1n, a), 1n+a, NA.add_comm(a, 1n), {==})), N.lt_succ_le_succ(a, b, h))
441
442# a 63-bit m rounds to at most 2^53
443def rne_top(+one: Nat, +h1: {one == 1n : Nat}, +m: Nat, +hm: {C.fits(63n, m) == True{} : Bool}) -> {Nat.is_le(SF.rne(m, 10n), C.shift(53n, one)) == True{} : Bool}:
444  +f = SH.fits_high(10n, 53n, m, hm)
445  N.le_trans(SF.rne(m, 10n), Nat.add(C.high(10n, m), 1n), C.shift(53n, one), rne_ub(m), succ_le(C.high(10n, m), C.shift(53n, one), WW.lt_one(53n, one, h1, C.high(10n, m), f)))
446
447def nfit_c(+k: Nat, +a: Nat, +r: Nat, +hle: {Nat.is_le(a, r) == True{} : Bool}, +f: {C.fits(k, a) == False{} : Bool}, +b: Bool, +hb: {C.fits(k, r) == b : Bool}) -> {b == False{} : Bool}:
448  match b:
449    case True{}:
450      NC.absurd_tf({True{} == False{} : Bool}, Equal.trans(Bool, False{}, C.fits(k, a), True{}, Equal.sym(Bool, C.fits(k, a), False{}, f), SH.fits_lek(k, a, r, hle, hb)))
451    case False{}:
452      {==}
453
454def nfit(+k: Nat, +a: Nat, +r: Nat, +hle: {Nat.is_le(a, r) == True{} : Bool}, +f: {C.fits(k, a) == False{} : Bool}) -> {C.fits(k, r) == False{} : Bool}:
455  nfit_c(k, a, r, hle, f, C.fits(k, r), {==})
456
457# a normalized m (bit 62 set) rounds to a normal significand
458def rne_norm(+m: Nat, +hm: {C.fits(62n, m) == False{} : Bool}) -> {C.fits(52n, SF.rne(m, 10n)) == False{} : Bool}:
459  +f = Equal.trans(Bool, C.fits(52n, C.high(10n, m)), C.fits(62n, m), False{}, Equal.sym(Bool, C.fits(62n, m), C.fits(52n, C.high(10n, m)), fits_hc(10n, 52n, m)), hm)
460  nfit(52n, C.high(10n, m), SF.rne(m, 10n), rne_lb(m), f)
461
462
463# n < 2^k as fits
464def lt_fit(+k: Nat, +one: Nat, +h1: {one == 1n : Nat}, +n: Nat) -> {Nat.is_lt(n, C.shift(k, one)) == C.fits(k, n) : Bool}:
465  +e2a = Equal.trans(Bool, Nat.is_lt(n, C.shift(k, 1n)), Nat.is_lt(n, C.pow2(k)), C.fits(k, n), Equal.cong(Nat, Bool, z => Nat.is_lt(n, z), C.shift(k, 1n), C.pow2(k), WW.shift_one(k)), Equal.sym(Bool, C.fits(k, n), Nat.is_lt(n, C.pow2(k)), WW.fits_lt(k, n)))
466  L.subst(Nat, o => {Nat.is_lt(n, C.shift(k, o)) == C.fits(k, n) : Bool}, 1n, one, Equal.sym(Nat, one, 1n, h1), e2a)
467
468
469
470# ---- the spec's pack on a rounded significand q <= 2^53 at ulp u = 1926 + EF ----
471
472def efv(+u: Nat, +EF: Nat, +hu: {Nat.add(EF, 1926n) == u : Nat}) -> {Nat.sub(Nat.add(u, 1075n), SF.zb()) == 1n+EF : Nat}:
473  +e1 = Equal.cong(Nat, Nat, z => Nat.sub(Nat.add(z, 1075n), SF.zb()), u, Nat.add(EF, 1926n), Equal.sym(Nat, Nat.add(EF, 1926n), u, hu))
474  +e2 = Equal.cong(Nat, Nat, z => Nat.sub(z, SF.zb()), Nat.add(Nat.add(EF, 1926n), 1075n), Nat.add(EF, 3001n), NA.add_assoc(EF, 1926n, 1075n))
475  +e3 = Equal.cong(Nat, Nat, z => Nat.sub(z, SF.zb()), Nat.add(EF, 3001n), Nat.add(3001n, EF), NA.add_comm(EF, 3001n))
476  Equal.trans(Nat, Nat.sub(Nat.add(u, 1075n), SF.zb()), Nat.sub(Nat.add(Nat.add(EF, 1926n), 1075n), SF.zb()), 1n+EF, e1, Equal.trans(Nat, Nat.sub(Nat.add(Nat.add(EF, 1926n), 1075n), SF.zb()), Nat.sub(Nat.add(EF, 3001n), SF.zb()), 1n+EF, e2, e3))
477
478def ef2v(+u: Nat, +EF: Nat, +hu: {Nat.add(EF, 1926n) == u : Nat}) -> {Nat.sub(Nat.add(1n+u, 1075n), SF.zb()) == 2n+EF : Nat}:
479  +e1 = Equal.cong(Nat, Nat, z => Nat.sub(Nat.add(1n+z, 1075n), SF.zb()), u, Nat.add(EF, 1926n), Equal.sym(Nat, Nat.add(EF, 1926n), u, hu))
480  +e2 = Equal.cong(Nat, Nat, z => Nat.sub(z, SF.zb()), Nat.add(Nat.add(1n+EF, 1926n), 1075n), Nat.add(1n+EF, 3001n), NA.add_assoc(1n+EF, 1926n, 1075n))
481  +e3 = Equal.cong(Nat, Nat, z => Nat.sub(z, SF.zb()), Nat.add(1n+EF, 3001n), Nat.add(3001n, 1n+EF), NA.add_comm(1n+EF, 3001n))
482  Equal.trans(Nat, Nat.sub(Nat.add(1n+u, 1075n), SF.zb()), Nat.sub(Nat.add(Nat.add(1n+EF, 1926n), 1075n), SF.zb()), 2n+EF, e1, Equal.trans(Nat, Nat.sub(Nat.add(Nat.add(1n+EF, 1926n), 1075n), SF.zb()), Nat.sub(Nat.add(1n+EF, 3001n), SF.zb()), 2n+EF, e2, e3))
483
484def add1c(+a: Nat, +k: Nat) -> {Nat.add(a, k) == Nat.add(k, a) : Nat}:
485  NA.add_comm(a, k)
486
487# the high part of a q in [2^52, 2^53) is 1
488def hi_one(+H0: Nat, +a: {Nat.is_eq(C.half(H0), 0n) == True{} : Bool}, +b: {Nat.is_eq(H0, 0n) == False{} : Bool}) -> {H0 == 1n : Nat}:
489  match H0:
490    case 0n:
491      Empty.absurd({0n == 1n : Nat}, LW.true_ne_false(b))
492    case 1n:
493      {==}
494    case 2n+ +p:
495      NC.absurd_tf({2n+p == 1n : Nat}, a)
496
497def f53h(+q: Nat) -> {C.fits(53n, q) == Nat.is_eq(C.half(C.high(52n, q)), 0n) : Bool}:
498  fits_hc(52n, 1n, q)
499
500def top_q(+one: Nat, +h1: {one == 1n : Nat}, +q: Nat, +hq: {Nat.is_le(q, C.shift(53n, one)) == True{} : Bool}, +hf: {C.fits(53n, q) == False{} : Bool}) -> {q == C.shift(52n, Nat.double(one)) : Nat}:
501  +hlt = Equal.trans(Bool, Nat.is_lt(q, C.shift(53n, one)), C.fits(53n, q), False{}, lt_fit(53n, one, h1, q), hf)
502  +hge = N.not_lt_le(q, C.shift(53n, one), hlt)
503  Equal.trans(Nat, q, C.shift(53n, one), C.shift(52n, Nat.double(one)), N.le_antisym(q, C.shift(53n, one), hq, hge), Equal.sym(Nat, C.shift(52n, Nat.double(one)), C.shift(53n, one), WW.shift_dbl(52n, one)))
504
505def pkg_c(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +q: Nat, +u: Nat, +EF: Nat, +hEF: {Nat.add(EF, 1926n) == u : Nat}, +hq: {Nat.is_le(q, C.shift(53n, one)) == True{} : Bool}, +f53: Bool, +h53: {C.fits(53n, q) == f53 : Bool}, +f52: Bool, +h52: {C.fits(52n, q) == f52 : Bool}, +h0: {Bool.or(Bool.not(f52), Nat.is_eq(EF, 0n)) == True{} : Bool}, +hov: {Nat.is_lt(Nat.add(EF, SF.pick(Nat, f53, 1n, 2n)), 2047n) == True{} : Bool}) -> {SF.pick(F.F64, f53, SF.pick(F.F64, f52, SF.encode(s, 0n, q), SF.pack_e(s, Nat.sub(Nat.add(u, 1075n), SF.zb()), C.low(52n, q))), SF.pack_e(s, Nat.sub(Nat.add(1n+u, 1075n), SF.zb()), 0n)) == bits(s, Nat.add(q, C.shift(52n, EF))) : F.F64}:
506  match f53 f52:
507    case True{} True{}:
508      +e0 = N.eq_from_is_eq(EF, 0n, h0)
509      Equal.trans(F.F64, SF.encode(s, 0n, q), bits(s, Nat.add(q, C.shift(52n, 0n))), bits(s, Nat.add(q, C.shift(52n, EF))), enc_bits(s, 0n, q), Equal.cong(Nat, F.F64, z => bits(s, Nat.add(q, C.shift(52n, z))), 0n, EF, Equal.sym(Nat, EF, 0n, e0)))
510    case True{} False{}:
511      +eH = 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), f53h(q)), h53), h52)
512      +e1 = efv(u, EF, hEF)
513      +eE = Equal.trans(Nat, Nat.sub(Nat.add(u, 1075n), SF.zb()), 1n+EF, Nat.add(C.high(52n, q), EF), e1, Equal.cong(Nat, Nat, z => Nat.add(z, EF), 1n, C.high(52n, q), Equal.sym(Nat, C.high(52n, q), 1n, eH)))
514      +hle = Equal.trans(Bool, Nat.is_le(2047n, Nat.sub(Nat.add(u, 1075n), SF.zb())), Nat.is_le(2047n, 1n+EF), False{}, Equal.cong(Nat, Bool, z => Nat.is_le(2047n, z), Nat.sub(Nat.add(u, 1075n), SF.zb()), 1n+EF, e1), Equal.trans(Bool, Nat.is_le(2047n, 1n+EF), Bool.not(Nat.is_lt(1n+EF, 2047n)), False{}, FB.le_nlt(2047n, 1n+EF), Equal.cong(Bool, Bool, t => Bool.not(t), Nat.is_lt(1n+EF, 2047n), True{}, L.subst(Nat, z => {Nat.is_lt(z, 2047n) == True{} : Bool}, Nat.add(EF, 1n), 1n+EF, Equal.trans(Nat, Nat.add(EF, 1n), Nat.add(1n, EF), 1n+EF, NA.add_comm(EF, 1n), {==}), hov))))
515      +p1 = Equal.cong(Bool, F.F64, t => SF.pick(F.F64, t, SF.inf(s), SF.encode(s, Nat.sub(Nat.add(u, 1075n), SF.zb()), C.low(52n, q))), Nat.is_le(2047n, Nat.sub(Nat.add(u, 1075n), SF.zb())), False{}, hle)
516      +p2 = enc_bits(s, Nat.sub(Nat.add(u, 1075n), SF.zb()), C.low(52n, q))
517      +v1 = Equal.trans(Nat, Nat.add(C.low(52n, q), C.shift(52n, Nat.sub(Nat.add(u, 1075n), SF.zb()))), Nat.add(C.low(52n, q), C.shift(52n, Nat.add(C.high(52n, q), EF))), Nat.add(q, C.shift(52n, EF)), Equal.cong(Nat, Nat, z => Nat.add(C.low(52n, q), C.shift(52n, z)), Nat.sub(Nat.add(u, 1075n), SF.zb()), Nat.add(C.high(52n, q), EF), eE), Equal.trans(Nat, Nat.add(C.low(52n, q), C.shift(52n, Nat.add(C.high(52n, q), EF))), Nat.add(C.low(52n, q), Nat.add(C.shift(52n, C.high(52n, q)), C.shift(52n, EF))), Nat.add(q, C.shift(52n, EF)), Equal.cong(Nat, Nat, z => Nat.add(C.low(52n, q), z), C.shift(52n, Nat.add(C.high(52n, q), EF)), Nat.add(C.shift(52n, C.high(52n, q)), C.shift(52n, EF)), WW.shift_add(52n, C.high(52n, q), EF)), Equal.trans(Nat, Nat.add(C.low(52n, q), Nat.add(C.shift(52n, C.high(52n, q)), C.shift(52n, EF))), Nat.add(Nat.add(C.low(52n, q), C.shift(52n, C.high(52n, q))), C.shift(52n, EF)), Nat.add(q, C.shift(52n, EF)), Equal.sym(Nat, Nat.add(Nat.add(C.low(52n, q), C.shift(52n, C.high(52n, q))), C.shift(52n, EF)), Nat.add(C.low(52n, q), Nat.add(C.shift(52n, C.high(52n, q)), C.shift(52n, EF))), NA.add_assoc(C.low(52n, q), C.shift(52n, C.high(52n, q)), C.shift(52n, EF))), Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(52n, EF)), Nat.add(C.low(52n, q), C.shift(52n, C.high(52n, q))), q, Equal.sym(Nat, q, Nat.add(C.low(52n, q), C.shift(52n, C.high(52n, q))), WW.low_high(52n, q))))))
518      +p3 = Equal.cong(Nat, F.F64, z => bits(s, z), Nat.add(C.low(52n, q), C.shift(52n, Nat.sub(Nat.add(u, 1075n), SF.zb()))), Nat.add(q, C.shift(52n, EF)), v1)
519      Equal.trans(F.F64, SF.pack_e(s, Nat.sub(Nat.add(u, 1075n), SF.zb()), C.low(52n, q)), SF.encode(s, Nat.sub(Nat.add(u, 1075n), SF.zb()), C.low(52n, q)), bits(s, Nat.add(q, C.shift(52n, EF))), p1, Equal.trans(F.F64, SF.encode(s, Nat.sub(Nat.add(u, 1075n), SF.zb()), C.low(52n, q)), bits(s, Nat.add(C.low(52n, q), C.shift(52n, Nat.sub(Nat.add(u, 1075n), SF.zb())))), bits(s, Nat.add(q, C.shift(52n, EF))), p2, p3))
520    case False{} _:
521      +e1 = ef2v(u, EF, hEF)
522      +eq = top_q(one, h1, q, hq, h53)
523      +two = Nat.double(one)
524      +eE = Equal.trans(Nat, Nat.sub(Nat.add(1n+u, 1075n), SF.zb()), 2n+EF, Nat.add(two, EF), e1, Equal.cong(Nat, Nat, z => Nat.add(Nat.double(z), EF), 1n, one, Equal.sym(Nat, one, 1n, h1)))
525      +hle = Equal.trans(Bool, Nat.is_le(2047n, Nat.sub(Nat.add(1n+u, 1075n), SF.zb())), Nat.is_le(2047n, 2n+EF), False{}, Equal.cong(Nat, Bool, z => Nat.is_le(2047n, z), Nat.sub(Nat.add(1n+u, 1075n), SF.zb()), 2n+EF, e1), Equal.trans(Bool, Nat.is_le(2047n, 2n+EF), Bool.not(Nat.is_lt(2n+EF, 2047n)), False{}, FB.le_nlt(2047n, 2n+EF), Equal.cong(Bool, Bool, t => Bool.not(t), Nat.is_lt(2n+EF, 2047n), True{}, L.subst(Nat, z => {Nat.is_lt(z, 2047n) == True{} : Bool}, Nat.add(EF, 2n), 2n+EF, Equal.trans(Nat, Nat.add(EF, 2n), Nat.add(2n, EF), 2n+EF, NA.add_comm(EF, 2n), {==}), hov))))
526      +p1 = Equal.cong(Bool, F.F64, t => SF.pick(F.F64, t, SF.inf(s), SF.encode(s, Nat.sub(Nat.add(1n+u, 1075n), SF.zb()), 0n)), Nat.is_le(2047n, Nat.sub(Nat.add(1n+u, 1075n), SF.zb())), False{}, hle)
527      +p2 = enc_bits(s, Nat.sub(Nat.add(1n+u, 1075n), SF.zb()), 0n)
528      +v1 = Equal.trans(Nat, C.shift(52n, Nat.sub(Nat.add(1n+u, 1075n), SF.zb())), C.shift(52n, Nat.add(two, EF)), Nat.add(q, C.shift(52n, EF)), Equal.cong(Nat, Nat, z => C.shift(52n, z), Nat.sub(Nat.add(1n+u, 1075n), SF.zb()), Nat.add(two, EF), eE), Equal.trans(Nat, C.shift(52n, Nat.add(two, EF)), Nat.add(C.shift(52n, two), C.shift(52n, EF)), Nat.add(q, C.shift(52n, EF)), WW.shift_add(52n, two, EF), Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(52n, EF)), C.shift(52n, two), q, Equal.sym(Nat, q, C.shift(52n, two), eq))))
529      +p3 = Equal.cong(Nat, F.F64, z => bits(s, z), C.shift(52n, Nat.sub(Nat.add(1n+u, 1075n), SF.zb())), Nat.add(q, C.shift(52n, EF)), v1)
530      Equal.trans(F.F64, SF.pack_e(s, Nat.sub(Nat.add(1n+u, 1075n), SF.zb()), 0n), SF.encode(s, Nat.sub(Nat.add(1n+u, 1075n), SF.zb()), 0n), bits(s, Nat.add(q, C.shift(52n, EF))), p1, Equal.trans(F.F64, SF.encode(s, Nat.sub(Nat.add(1n+u, 1075n), SF.zb()), 0n), bits(s, Nat.add(0n, C.shift(52n, Nat.sub(Nat.add(1n+u, 1075n), SF.zb())))), bits(s, Nat.add(q, C.shift(52n, EF))), p2, p3))
531
532def pkg(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +q: Nat, +u: Nat, +EF: Nat, +hEF: {Nat.add(EF, 1926n) == u : Nat}, +hq: {Nat.is_le(q, C.shift(53n, one)) == True{} : Bool}, +h0: {Bool.or(Bool.not(C.fits(52n, q)), Nat.is_eq(EF, 0n)) == True{} : Bool}, +hov: {Nat.is_lt(Nat.add(EF, SF.pick(Nat, C.fits(53n, q), 1n, 2n)), 2047n) == True{} : Bool}) -> {SF.pack(s, q, u) == bits(s, Nat.add(q, C.shift(52n, EF))) : F.F64}:
533  pkg_c(one, h1, s, q, u, EF, hEF, hq, C.fits(53n, q), {==}, C.fits(52n, q), {==}, h0, hov)
534
535def pko_c(+s: Bool, +q: Nat, +u: Nat, +EF: Nat, +hEF: {Nat.add(EF, 1926n) == u : Nat}, +f53: Bool, +h52: {C.fits(52n, q) == False{} : Bool}, +hov: {Nat.is_lt(Nat.add(EF, SF.pick(Nat, f53, 1n, 2n)), 2047n) == False{} : Bool}) -> {SF.pick(F.F64, f53, SF.pick(F.F64, C.fits(52n, q), SF.encode(s, 0n, q), SF.pack_e(s, Nat.sub(Nat.add(u, 1075n), SF.zb()), C.low(52n, q))), SF.pack_e(s, Nat.sub(Nat.add(1n+u, 1075n), SF.zb()), 0n)) == SF.inf(s) : F.F64}:
536  match f53:
537    case True{}:
538      +e1 = efv(u, EF, hEF)
539      +hle = Equal.trans(Bool, Nat.is_le(2047n, Nat.sub(Nat.add(u, 1075n), SF.zb())), Nat.is_le(2047n, 1n+EF), True{}, Equal.cong(Nat, Bool, z => Nat.is_le(2047n, z), Nat.sub(Nat.add(u, 1075n), SF.zb()), 1n+EF, e1), Equal.trans(Bool, Nat.is_le(2047n, 1n+EF), Bool.not(Nat.is_lt(1n+EF, 2047n)), True{}, FB.le_nlt(2047n, 1n+EF), Equal.cong(Bool, Bool, t => Bool.not(t), Nat.is_lt(1n+EF, 2047n), False{}, L.subst(Nat, z => {Nat.is_lt(z, 2047n) == False{} : Bool}, Nat.add(EF, 1n), 1n+EF, Equal.trans(Nat, Nat.add(EF, 1n), Nat.add(1n, EF), 1n+EF, NA.add_comm(EF, 1n), {==}), hov))))
540      +p0 = Equal.cong(Bool, F.F64, t => SF.pick(F.F64, t, SF.encode(s, 0n, q), SF.pack_e(s, Nat.sub(Nat.add(u, 1075n), SF.zb()), C.low(52n, q))), C.fits(52n, q), False{}, h52)
541      Equal.trans(F.F64, SF.pick(F.F64, True{}, SF.pick(F.F64, C.fits(52n, q), SF.encode(s, 0n, q), SF.pack_e(s, Nat.sub(Nat.add(u, 1075n), SF.zb()), C.low(52n, q))), SF.pack_e(s, Nat.sub(Nat.add(1n+u, 1075n), SF.zb()), 0n)), SF.pick(F.F64, C.fits(52n, q), SF.encode(s, 0n, q), SF.pack_e(s, Nat.sub(Nat.add(u, 1075n), SF.zb()), C.low(52n, q))), SF.inf(s), pk_t(F.F64, SF.pick(F.F64, C.fits(52n, q), SF.encode(s, 0n, q), SF.pack_e(s, Nat.sub(Nat.add(u, 1075n), SF.zb()), C.low(52n, q))), SF.pack_e(s, Nat.sub(Nat.add(1n+u, 1075n), SF.zb()), 0n)), Equal.trans(F.F64, SF.pick(F.F64, C.fits(52n, q), SF.encode(s, 0n, q), SF.pack_e(s, Nat.sub(Nat.add(u, 1075n), SF.zb()), C.low(52n, q))), SF.pack_e(s, Nat.sub(Nat.add(u, 1075n), SF.zb()), C.low(52n, q)), SF.inf(s), p0, Equal.cong(Bool, F.F64, t => SF.pick(F.F64, t, SF.inf(s), SF.encode(s, Nat.sub(Nat.add(u, 1075n), SF.zb()), C.low(52n, q))), Nat.is_le(2047n, Nat.sub(Nat.add(u, 1075n), SF.zb())), True{}, hle)))
542    case False{}:
543      +e1 = ef2v(u, EF, hEF)
544      +hle = Equal.trans(Bool, Nat.is_le(2047n, Nat.sub(Nat.add(1n+u, 1075n), SF.zb())), Nat.is_le(2047n, 2n+EF), True{}, Equal.cong(Nat, Bool, z => Nat.is_le(2047n, z), Nat.sub(Nat.add(1n+u, 1075n), SF.zb()), 2n+EF, e1), Equal.trans(Bool, Nat.is_le(2047n, 2n+EF), Bool.not(Nat.is_lt(2n+EF, 2047n)), True{}, FB.le_nlt(2047n, 2n+EF), Equal.cong(Bool, Bool, t => Bool.not(t), Nat.is_lt(2n+EF, 2047n), False{}, L.subst(Nat, z => {Nat.is_lt(z, 2047n) == False{} : Bool}, Nat.add(EF, 2n), 2n+EF, Equal.trans(Nat, Nat.add(EF, 2n), Nat.add(2n, EF), 2n+EF, NA.add_comm(EF, 2n), {==}), hov))))
545      Equal.trans(F.F64, SF.pick(F.F64, False{}, SF.pick(F.F64, C.fits(52n, q), SF.encode(s, 0n, q), SF.pack_e(s, Nat.sub(Nat.add(u, 1075n), SF.zb()), C.low(52n, q))), SF.pack_e(s, Nat.sub(Nat.add(1n+u, 1075n), SF.zb()), 0n)), SF.pack_e(s, Nat.sub(Nat.add(1n+u, 1075n), SF.zb()), 0n), SF.inf(s), pk_f(F.F64, SF.pick(F.F64, C.fits(52n, q), SF.encode(s, 0n, q), SF.pack_e(s, Nat.sub(Nat.add(u, 1075n), SF.zb()), C.low(52n, q))), SF.pack_e(s, Nat.sub(Nat.add(1n+u, 1075n), SF.zb()), 0n)), Equal.cong(Bool, F.F64, t => SF.pick(F.F64, t, SF.inf(s), SF.encode(s, Nat.sub(Nat.add(1n+u, 1075n), SF.zb()), 0n)), Nat.is_le(2047n, Nat.sub(Nat.add(1n+u, 1075n), SF.zb())), True{}, hle))
546
547def pko(+s: Bool, +q: Nat, +u: Nat, +EF: Nat, +hEF: {Nat.add(EF, 1926n) == u : Nat}, +h52: {C.fits(52n, q) == False{} : Bool}, +hov: {Nat.is_lt(Nat.add(EF, SF.pick(Nat, C.fits(53n, q), 1n, 2n)), 2047n) == False{} : Bool}) -> {SF.pack(s, q, u) == SF.inf(s) : F.F64}:
548  pko_c(s, q, u, EF, hEF, C.fits(53n, q), h52, hov)
549
550# ---- when the rounded significand reaches 2^53 ----
551
552def hsp(+m: Nat) -> {C.high(10n, Nat.add(m, 512n)) == Nat.add(C.high(10n, m), C.high(10n, Nat.add(C.low(10n, m), 512n))) : Nat}:
553  Equal.trans(Nat, C.high(10n, Nat.add(m, 512n)), C.high(10n, Nat.add(Nat.add(C.low(10n, m), C.shift(10n, C.high(10n, m))), 512n)), Nat.add(C.high(10n, m), C.high(10n, Nat.add(C.low(10n, m), 512n))), Equal.cong(Nat, Nat, z => C.high(10n, Nat.add(z, 512n)), m, Nat.add(C.low(10n, m), C.shift(10n, C.high(10n, m))), WW.low_high(10n, m)), Equal.trans(Nat, C.high(10n, Nat.add(Nat.add(C.low(10n, m), C.shift(10n, C.high(10n, m))), 512n)), C.high(10n, Nat.add(Nat.add(C.low(10n, m), 512n), C.shift(10n, C.high(10n, m)))), Nat.add(C.high(10n, m), C.high(10n, Nat.add(C.low(10n, m), 512n))), Equal.cong(Nat, Nat, z => C.high(10n, z), Nat.add(Nat.add(C.low(10n, m), C.shift(10n, C.high(10n, m))), 512n), Nat.add(Nat.add(C.low(10n, m), 512n), C.shift(10n, C.high(10n, m))), A.add_rot(C.low(10n, m), C.shift(10n, C.high(10n, m)), 512n)), Equal.trans(Nat, C.high(10n, Nat.add(Nat.add(C.low(10n, m), 512n), C.shift(10n, C.high(10n, m)))), Nat.add(C.high(10n, Nat.add(C.low(10n, m), 512n)), C.high(10n, m)), Nat.add(C.high(10n, m), C.high(10n, Nat.add(C.low(10n, m), 512n))), WW.high_add_shift(10n, Nat.add(C.low(10n, m), 512n), C.high(10n, m)), NA.add_comm(C.high(10n, Nat.add(C.low(10n, m), 512n)), C.high(10n, m)))))
554
555def mod_sh(+k: Nat, +x: Nat) -> {Nat.mod(C.shift(1n+k, x), 2n) == 0n : Nat}:
556  WW.odd_limb(k, 0n, x)
557
558def fsub_c(+k: Nat, +one: Nat, +h1: {one == 1n : Nat}, +R0: Nat, +hR: {Nat.is_le(R0, C.shift(1n+k, one)) == True{} : Bool}, +f: Bool, +hf: {C.fits(1n+k, R0) == f : Bool}) -> {C.fits(1n+k, Nat.sub(R0, Nat.mod(R0, 2n))) == f : Bool}:
559  match f:
560    case True{}:
561      SH.fits_lek(1n+k, Nat.sub(R0, Nat.mod(R0, 2n)), R0, UH.sub_le(R0, Nat.mod(R0, 2n)), hf)
562    case False{}:
563      +hlt = Equal.trans(Bool, Nat.is_lt(R0, C.shift(1n+k, one)), C.fits(1n+k, R0), False{}, lt_fit(1n+k, one, h1, R0), hf)
564      +eR = N.le_antisym(R0, C.shift(1n+k, one), hR, N.not_lt_le(R0, C.shift(1n+k, one), hlt))
565      +em = Equal.trans(Nat, Nat.mod(R0, 2n), Nat.mod(C.shift(1n+k, one), 2n), 0n, Equal.cong(Nat, Nat, z => Nat.mod(z, 2n), R0, C.shift(1n+k, one), eR), mod_sh(k, one))
566      +es = Equal.trans(Nat, Nat.sub(R0, Nat.mod(R0, 2n)), Nat.sub(R0, 0n), R0, Equal.cong(Nat, Nat, z => Nat.sub(R0, z), Nat.mod(R0, 2n), 0n, em), N.sub_zero(R0))
567      Equal.trans(Bool, C.fits(1n+k, Nat.sub(R0, Nat.mod(R0, 2n))), C.fits(1n+k, R0), False{}, Equal.cong(Nat, Bool, z => C.fits(1n+k, z), Nat.sub(R0, Nat.mod(R0, 2n)), R0, es), hf)
568
569def fpk(+one: Nat, +h1: {one == 1n : Nat}, +R0: Nat, +hR: {Nat.is_le(R0, C.shift(53n, one)) == True{} : Bool}, +t: Bool) -> {C.fits(53n, SF.pick(Nat, t, Nat.sub(R0, Nat.mod(R0, 2n)), R0)) == C.fits(53n, R0) : Bool}:
570  match t:
571    case True{}:
572      fsub_c(52n, one, h1, R0, hR, C.fits(53n, R0), {==})
573    case False{}:
574      {==}
575
576def le1(+t: Nat, +h: {C.fits(1n, t) == True{} : Bool}) -> {Nat.is_le(t, 1n) == True{} : Bool}:
577  match t:
578    case 0n:
579      {==}
580    case 1n:
581      {==}
582    case 2n+ +p:
583      NC.absurd_tf({Nat.is_le(2n+p, 1n) == True{} : Bool}, h)
584
585def R_le(+one: Nat, +h1: {one == 1n : Nat}, +m: Nat, +hm: {C.fits(63n, m) == True{} : Bool}) -> {Nat.is_le(Nat.add(C.high(10n, m), C.high(10n, Nat.add(C.low(10n, m), 512n))), C.shift(53n, one)) == True{} : Bool}:
586  +t = C.high(10n, Nat.add(C.low(10n, m), 512n))
587  +ht = le1(t, SH.fits_high(10n, 1n, Nat.add(C.low(10n, m), 512n), fits_add1(10n, C.low(10n, m), 512n, WW.low_fits(10n, m), {==})))
588  +hq = WW.lt_one(53n, one, h1, C.high(10n, m), SH.fits_high(10n, 53n, m, hm))
589  N.le_trans(Nat.add(C.high(10n, m), C.high(10n, Nat.add(C.low(10n, m), 512n))), Nat.add(C.high(10n, m), 1n), C.shift(53n, one), N.le_add_left(t, 1n, C.high(10n, m), ht), succ_le(C.high(10n, m), C.shift(53n, one), hq))
590
591# the rounded significand overflows 53 bits exactly when m + 2^9 overflows 63
592def p2(+one: Nat, +h1: {one == 1n : Nat}, +m: Nat, +hm: {C.fits(63n, m) == True{} : Bool}) -> {C.fits(53n, SF.rne(m, 10n)) == C.fits(63n, Nat.add(m, 512n)) : Bool}:
593  +e1 = Equal.cong(Nat, Bool, z => C.fits(53n, z), SF.rne(m, 10n), SF.pick(Nat, Nat.is_eq(C.low(10n, m), 512n), Nat.sub(Nat.add(C.high(10n, m), C.high(10n, Nat.add(C.low(10n, m), 512n))), Nat.mod(Nat.add(C.high(10n, m), C.high(10n, Nat.add(C.low(10n, m), 512n))), 2n)), Nat.add(C.high(10n, m), C.high(10n, Nat.add(C.low(10n, m), 512n)))), Equal.sym(Nat, SF.pick(Nat, Nat.is_eq(C.low(10n, m), 512n), Nat.sub(Nat.add(C.high(10n, m), C.high(10n, Nat.add(C.low(10n, m), 512n))), Nat.mod(Nat.add(C.high(10n, m), C.high(10n, Nat.add(C.low(10n, m), 512n))), 2n)), Nat.add(C.high(10n, m), C.high(10n, Nat.add(C.low(10n, m), 512n)))), SF.rne(m, 10n), rp_c(C.high(10n, m), C.low(10n, m), WW.low_fits(10n, m), Nat.cmp(C.low(10n, m), 512n), {==})))
594  +e2 = fpk(one, h1, Nat.add(C.high(10n, m), C.high(10n, Nat.add(C.low(10n, m), 512n))), R_le(one, h1, m, hm), Nat.is_eq(C.low(10n, m), 512n))
595  +e3 = Equal.cong(Nat, Bool, z => C.fits(53n, z), Nat.add(C.high(10n, m), C.high(10n, Nat.add(C.low(10n, m), 512n))), C.high(10n, Nat.add(m, 512n)), Equal.sym(Nat, C.high(10n, Nat.add(m, 512n)), Nat.add(C.high(10n, m), C.high(10n, Nat.add(C.low(10n, m), 512n))), hsp(m)))
596  +e4 = Equal.sym(Bool, C.fits(63n, Nat.add(m, 512n)), C.fits(53n, C.high(10n, Nat.add(m, 512n))), fits_hc(10n, 53n, Nat.add(m, 512n)))
597  Equal.trans(Bool, C.fits(53n, SF.rne(m, 10n)), C.fits(53n, SF.pick(Nat, Nat.is_eq(C.low(10n, m), 512n), Nat.sub(Nat.add(C.high(10n, m), C.high(10n, Nat.add(C.low(10n, m), 512n))), Nat.mod(Nat.add(C.high(10n, m), C.high(10n, Nat.add(C.low(10n, m), 512n))), 2n)), Nat.add(C.high(10n, m), C.high(10n, Nat.add(C.low(10n, m), 512n))))), C.fits(63n, Nat.add(m, 512n)), e1, Equal.trans(Bool, C.fits(53n, SF.pick(Nat, Nat.is_eq(C.low(10n, m), 512n), Nat.sub(Nat.add(C.high(10n, m), C.high(10n, Nat.add(C.low(10n, m), 512n))), Nat.mod(Nat.add(C.high(10n, m), C.high(10n, Nat.add(C.low(10n, m), 512n))), 2n)), Nat.add(C.high(10n, m), C.high(10n, Nat.add(C.low(10n, m), 512n))))), C.fits(53n, Nat.add(C.high(10n, m), C.high(10n, Nat.add(C.low(10n, m), 512n)))), C.fits(63n, Nat.add(m, 512n)), e2, Equal.trans(Bool, C.fits(53n, Nat.add(C.high(10n, m), C.high(10n, Nat.add(C.low(10n, m), 512n)))), C.fits(53n, C.high(10n, Nat.add(m, 512n))), C.fits(63n, Nat.add(m, 512n)), e3, e4)))
598
599# SoftFloat's carry test: 2^63 <= sig + 2^9
600def ovle(+one: Nat, +h1: {one == 1n : Nat}, +sig: WU.U64, +hS: {C.fits(63n, SW.value(sig)) == True{} : Bool}, +c: U32, +hc: {c == U32{WD.pw(32n, 31n)} : U32}) -> {X.le(WU.U64{0, c}, X.add(sig, WU.U64{512, 0})) == Bool.not(C.fits(63n, Nat.add(SW.value(sig), 512n))) : Bool}:
601  a1 = WA.add_value(sig, WU.U64{512, 0})
602  +ev1 = Equal.trans(Nat, SW.value(X.add(sig, WU.U64{512, 0})), C.low(64n, Nat.add(SW.value(sig), 512n)), Nat.add(SW.value(sig), 512n), a1, WW.low_fit(64n, Nat.add(SW.value(sig), 512n), fits_add1(63n, SW.value(sig), 512n, hS, {==})))
603  +ec = Equal.trans(Nat, C.shift(32n, v(c)), C.shift(32n, C.shift(31n, one)), C.shift(63n, one), Equal.cong(Nat, Nat, z => C.shift(32n, z), v(c), C.shift(31n, one), FB.pwv(31n, {==}, one, h1, c, hc)), Equal.sym(Nat, C.shift(63n, one), C.shift(32n, C.shift(31n, one)), WW.shift_comp(32n, 31n, one)))
604  l1 = WA.lt_value(X.add(sig, WU.U64{512, 0}), WU.U64{0, c})
605  +e2 = Equal.trans(Bool, Nat.is_lt(SW.value(X.add(sig, WU.U64{512, 0})), C.shift(32n, v(c))), Nat.is_lt(Nat.add(SW.value(sig), 512n), C.shift(32n, v(c))), Nat.is_lt(Nat.add(SW.value(sig), 512n), C.shift(63n, one)), Equal.cong(Nat, Bool, z => Nat.is_lt(z, C.shift(32n, v(c))), SW.value(X.add(sig, WU.U64{512, 0})), Nat.add(SW.value(sig), 512n), ev1), Equal.cong(Nat, Bool, z => Nat.is_lt(Nat.add(SW.value(sig), 512n), z), C.shift(32n, v(c)), C.shift(63n, one), ec))
606  +e3 = Equal.trans(Bool, X.lt(X.add(sig, WU.U64{512, 0}), WU.U64{0, c}), Nat.is_lt(Nat.add(SW.value(sig), 512n), C.shift(63n, one)), C.fits(63n, Nat.add(SW.value(sig), 512n)), Equal.trans(Bool, X.lt(X.add(sig, WU.U64{512, 0}), WU.U64{0, c}), Nat.is_lt(SW.value(X.add(sig, WU.U64{512, 0})), C.shift(32n, v(c))), Nat.is_lt(Nat.add(SW.value(sig), 512n), C.shift(63n, one)), l1, e2), lt_fit(63n, one, h1, Nat.add(SW.value(sig), 512n)))
607  Equal.cong(Bool, Bool, t => Bool.not(t), X.lt(X.add(sig, WU.U64{512, 0}), WU.U64{0, c}), C.fits(63n, Nat.add(SW.value(sig), 512n)), e3)
608
609
610# ---- small facts for roundPackToF64 ----
611
612def ze0(+z: Bool) -> {F.zero_e(0n, z) == 0n : Nat}:
613  match z:
614    case True{}:
615      {==}
616    case False{}:
617      {==}
618
619def rpw(+w: WU.U64, +hS: {C.fits(63n, SW.value(w)) == True{} : Bool}) -> {SW.value(X.clear0(X.shr(X.add(w, WU.U64{512, 0}), 10n), U32.is_eq(U32.and(X.lo(w), 1023), 512))) == SF.rne(SW.value(w), 10n) : Nat}:
620  match w:
621    case WU.U64{+l, +h}:
622      rpv(l, h, hS)
623
624def max_r(+a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.max(a, b) == b : Nat}:
625  match a b:
626    case 0n _:
627      {==}
628    case 1n+ +ap 0n:
629      NC.absurd_tf({Nat.max(1n+ap, 0n) == 0n : Nat}, h)
630    case 1n+ +ap 1n+ +bp:
631      Equal.cong(Nat, Nat, z => 1n+z, Nat.max(ap, bp), bp, max_r(ap, bp, h))
632
633def max_l(+a: Nat, +b: Nat, +h: {Nat.is_le(b, a) == True{} : Bool}) -> {Nat.max(a, b) == a : Nat}:
634  match a b:
635    case 0n 0n:
636      {==}
637    case 0n 1n+ +bp:
638      NC.absurd_tf({Nat.max(0n, 1n+bp) == 0n : Nat}, h)
639    case 1n+ +ap 0n:
640      {==}
641    case 1n+ +ap 1n+ +bp:
642      Equal.cong(Nat, Nat, z => 1n+z, Nat.max(ap, bp), ap, max_l(ap, bp, h))
643
644def ge_or(+c: Nat, +n: Nat) -> {Bool.or(Nat.is_lt(c, n), Nat.is_eq(n, c)) == Nat.is_le(c, n) : Bool}:
645  match c n:
646    case 0n 0n:
647      {==}
648    case 0n 1n+ +np:
649      {==}
650    case 1n+ +cp 0n:
651      {==}
652    case 1n+ +cp 1n+ +np:
653      ge_or(cp, np)
654
655def le_succ_lt(+a: Nat, +b: Nat) -> {Nat.is_le(1n+a, b) == Nat.is_lt(a, b) : Bool}:
656  match a b:
657    case 0n 0n:
658      {==}
659    case 0n 1n+ +bp:
660      match bp:
661        case 0n:
662          {==}
663        case 1n+ +bq:
664          {==}
665    case 1n+ +ap 0n:
666      {==}
667    case 1n+ +ap 1n+ +bp:
668      le_succ_lt(ap, bp)
669
670def and_f(+b: Bool) -> {Bool.and(b, False{}) == False{} : Bool}:
671  match b:
672    case True{}:
673      {==}
674    case False{}:
675      {==}
676
677def or_f(+b: Bool) -> {Bool.or(b, False{}) == b : Bool}:
678  match b:
679    case True{}:
680      {==}
681    case False{}:
682      {==}
683
684def or_t(+b: Bool) -> {Bool.or(b, True{}) == True{} : Bool}:
685  match b:
686    case True{}:
687      {==}
688    case False{}:
689      {==}
690
691def not_t(+b: Bool, +h: {Bool.not(b) == True{} : Bool}) -> {b == False{} : Bool}:
692  match b:
693    case True{}:
694      Empty.absurd({True{} == False{} : Bool}, LW.true_ne_false(Equal.sym(Bool, False{}, True{}, h)))
695    case False{}:
696      {==}
697
698def not_f(+b: Bool, +h: {Bool.not(b) == False{} : Bool}) -> {b == True{} : Bool}:
699  match b:
700    case True{}:
701      {==}
702    case False{}:
703      Empty.absurd({False{} == True{} : Bool}, LW.true_ne_false(h))
704
705def pick_lt(+c: Bool) -> {Nat.is_lt(SF.pick(Nat, c, 1n, 2n), 2047n) == True{} : Bool}:
706  match c:
707    case True{}:
708      {==}
709    case False{}:
710      {==}
711
712# the overflow test of roundPackToF64 against the spec's exponent field
713def ov_c(+EF: Nat, +f: Bool) -> {Bool.or(Nat.is_lt(2045n, EF), Bool.and(Nat.is_eq(EF, 2045n), Bool.not(f))) == Bool.not(Nat.is_lt(Nat.add(EF, SF.pick(Nat, f, 1n, 2n)), 2047n)) : Bool}:
714  match f:
715    case True{}:
716      +l1 = Equal.trans(Bool, Bool.or(Nat.is_lt(2045n, EF), Bool.and(Nat.is_eq(EF, 2045n), False{})), Bool.or(Nat.is_lt(2045n, EF), False{}), Nat.is_lt(2045n, EF), Equal.cong(Bool, Bool, t => Bool.or(Nat.is_lt(2045n, EF), t), Bool.and(Nat.is_eq(EF, 2045n), False{}), False{}, and_f(Nat.is_eq(EF, 2045n))), or_f(Nat.is_lt(2045n, EF)))
717      +r1 = Equal.trans(Bool, Bool.not(Nat.is_lt(Nat.add(EF, 1n), 2047n)), Bool.not(Nat.is_lt(EF, 2046n)), Nat.is_lt(2045n, EF), Equal.cong(Bool, Bool, t => Bool.not(t), Nat.is_lt(Nat.add(EF, 1n), 2047n), Nat.is_lt(EF, 2046n), WW.lt_cancel_r(EF, 2046n, 1n)), Equal.trans(Bool, Bool.not(Nat.is_lt(EF, 2046n)), Nat.is_le(2046n, EF), Nat.is_lt(2045n, EF), Equal.sym(Bool, Nat.is_le(2046n, EF), Bool.not(Nat.is_lt(EF, 2046n)), FB.le_nlt(2046n, EF)), le_succ_lt(2045n, EF)))
718      Equal.trans(Bool, Bool.or(Nat.is_lt(2045n, EF), Bool.and(Nat.is_eq(EF, 2045n), False{})), Nat.is_lt(2045n, EF), Bool.not(Nat.is_lt(Nat.add(EF, 1n), 2047n)), l1, Equal.sym(Bool, Bool.not(Nat.is_lt(Nat.add(EF, 1n), 2047n)), Nat.is_lt(2045n, EF), r1))
719    case False{}:
720      +l1 = Equal.trans(Bool, Bool.or(Nat.is_lt(2045n, EF), Bool.and(Nat.is_eq(EF, 2045n), True{})), Bool.or(Nat.is_lt(2045n, EF), Nat.is_eq(EF, 2045n)), Nat.is_le(2045n, EF), Equal.cong(Bool, Bool, t => Bool.or(Nat.is_lt(2045n, EF), t), Bool.and(Nat.is_eq(EF, 2045n), True{}), Nat.is_eq(EF, 2045n), U.and_true(Nat.is_eq(EF, 2045n))), ge_or(2045n, EF))
721      +r1 = Equal.trans(Bool, Bool.not(Nat.is_lt(Nat.add(EF, 2n), 2047n)), Bool.not(Nat.is_lt(EF, 2045n)), Nat.is_le(2045n, EF), Equal.cong(Bool, Bool, t => Bool.not(t), Nat.is_lt(Nat.add(EF, 2n), 2047n), Nat.is_lt(EF, 2045n), WW.lt_cancel_r(EF, 2045n, 2n)), Equal.sym(Bool, Nat.is_le(2045n, EF), Bool.not(Nat.is_lt(EF, 2045n)), FB.le_nlt(2045n, EF)))
722      Equal.trans(Bool, Bool.or(Nat.is_lt(2045n, EF), Bool.and(Nat.is_eq(EF, 2045n), True{})), Nat.is_le(2045n, EF), Bool.not(Nat.is_lt(Nat.add(EF, 2n), 2047n)), l1, Equal.sym(Bool, Bool.not(Nat.is_lt(Nat.add(EF, 2n), 2047n)), Nat.is_le(2045n, EF), r1))
723
724def eq_cancel_r(+a: Nat, +b: Nat, +c: Nat) -> {Nat.is_eq(Nat.add(a, c), Nat.add(b, c)) == Nat.is_eq(a, b) : Bool}:
725  Equal.cong(Cmp, Bool, t => Cmp.is_eq(t), Nat.cmp(Nat.add(a, c), Nat.add(b, c)), Nat.cmp(a, b), NC.cmp_addr(a, b, c))
726
727def sub_cancel_r(+a: Nat, +b: Nat, +c: Nat) -> {Nat.sub(Nat.add(a, c), Nat.add(b, c)) == Nat.sub(a, b) : Nat}:
728  match c:
729    case 0n:
730      Equal.trans(Nat, Nat.sub(Nat.add(a, 0n), Nat.add(b, 0n)), Nat.sub(a, Nat.add(b, 0n)), Nat.sub(a, b), Equal.cong(Nat, Nat, z => Nat.sub(z, Nat.add(b, 0n)), Nat.add(a, 0n), a, N.add_zero(a)), Equal.cong(Nat, Nat, z => Nat.sub(a, z), Nat.add(b, 0n), b, N.add_zero(b)))
731    case 1n+ +cp:
732      Equal.trans(Nat, Nat.sub(Nat.add(a, 1n+cp), Nat.add(b, 1n+cp)), Nat.sub(1n+Nat.add(a, cp), Nat.add(b, 1n+cp)), Nat.sub(a, b), Equal.cong(Nat, Nat, z => Nat.sub(z, Nat.add(b, 1n+cp)), Nat.add(a, 1n+cp), 1n+Nat.add(a, cp), N.add_succ(a, cp)), Equal.trans(Nat, Nat.sub(1n+Nat.add(a, cp), Nat.add(b, 1n+cp)), Nat.sub(1n+Nat.add(a, cp), 1n+Nat.add(b, cp)), Nat.sub(a, b), Equal.cong(Nat, Nat, z => Nat.sub(1n+Nat.add(a, cp), z), Nat.add(b, 1n+cp), 1n+Nat.add(b, cp), N.add_succ(b, cp)), sub_cancel_r(a, b, cp)))
733
734def sub_add_l(+a: Nat, +x: Nat) -> {Nat.sub(Nat.add(a, x), x) == a : Nat}:
735  Equal.trans(Nat, Nat.sub(Nat.add(a, x), x), Nat.sub(Nat.add(x, a), x), a, Equal.cong(Nat, Nat, z => Nat.sub(z, x), Nat.add(a, x), Nat.add(x, a), NA.add_comm(a, x)), N.add_sub_cancel(x, a))
736
737def half_le(+n: Nat) -> {Nat.is_le(C.half(n), n) == True{} : Bool}:
738  match n:
739    case 0n:
740      {==}
741    case 1n:
742      {==}
743    case 2n+ +p:
744      N.le_trans(1n+C.half(p), 1n+p, 2n+p, half_le(p), N.le_succ(1n+p))
745
746# q < 2^53 + 1 fits 54 bits
747def fit54(+one: Nat, +h1: {one == 1n : Nat}, +q: Nat, +hq: {Nat.is_le(q, C.shift(53n, one)) == True{} : Bool}) -> {C.fits(54n, q) == True{} : Bool}:
748  +h0 = L.subst(Nat, o => {Nat.is_lt(o, Nat.double(o)) == True{} : Bool}, 1n, one, Equal.sym(Nat, one, 1n, h1), {==})
749  +h2 = WW.shift_lt(53n, one, Nat.double(one), h0)
750  +h3 = L.subst(Nat, z => {Nat.is_lt(C.shift(53n, one), z) == True{} : Bool}, C.shift(53n, Nat.double(one)), C.shift(54n, one), WW.shift_dbl(53n, one), h2)
751  Equal.trans(Bool, C.fits(54n, q), Nat.is_lt(q, C.shift(54n, one)), True{}, Equal.sym(Bool, Nat.is_lt(q, C.shift(54n, one)), C.fits(54n, q), lt_fit(54n, one, h1, q)), N.le_lt_trans(q, C.shift(53n, one), C.shift(54n, one), hq, h3))
752
753# the high part of a normal q <= 2^53 is the spec's 1 or 2
754def hpick_c(+one: Nat, +h1: {one == 1n : Nat}, +q: Nat, +hq: {Nat.is_le(q, C.shift(53n, one)) == True{} : Bool}, +h52: {C.fits(52n, q) == False{} : Bool}, +f: Bool, +hf: {C.fits(53n, q) == f : Bool}) -> {C.high(52n, q) == SF.pick(Nat, f, 1n, 2n) : Nat}:
755  match f:
756    case True{}:
757      Equal.trans(Nat, C.high(52n, q), 1n, SF.pick(Nat, True{}, 1n, 2n), 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), f53h(q)), hf), h52), Equal.sym(Nat, SF.pick(Nat, True{}, 1n, 2n), 1n, pk_t(Nat, 1n, 2n)))
758    case False{}:
759      +eq = top_q(one, h1, q, hq, hf)
760      +e1 = Equal.trans(Nat, C.high(52n, q), C.high(52n, C.shift(52n, Nat.double(one))), Nat.double(one), Equal.cong(Nat, Nat, z => C.high(52n, z), q, C.shift(52n, Nat.double(one)), eq), WW.high_u(52n, 0n, Nat.double(one), fz(52n)))
761      Equal.trans(Nat, C.high(52n, q), 2n, SF.pick(Nat, False{}, 1n, 2n), Equal.trans(Nat, C.high(52n, q), Nat.double(one), 2n, e1, Equal.cong(Nat, Nat, z => Nat.double(z), one, 1n, h1)), Equal.sym(Nat, SF.pick(Nat, False{}, 1n, 2n), 2n, pk_f(Nat, 1n, 2n)))
762
763def qsplit(+q: Nat, +EF: Nat) -> {Nat.add(C.low(52n, q), C.shift(52n, Nat.add(C.high(52n, q), EF))) == Nat.add(q, C.shift(52n, EF)) : Nat}:
764  Equal.trans(Nat, Nat.add(C.low(52n, q), C.shift(52n, Nat.add(C.high(52n, q), EF))), Nat.add(C.low(52n, q), Nat.add(C.shift(52n, C.high(52n, q)), C.shift(52n, EF))), Nat.add(q, C.shift(52n, EF)), Equal.cong(Nat, Nat, z => Nat.add(C.low(52n, q), z), C.shift(52n, Nat.add(C.high(52n, q), EF)), Nat.add(C.shift(52n, C.high(52n, q)), C.shift(52n, EF)), WW.shift_add(52n, C.high(52n, q), EF)), Equal.trans(Nat, Nat.add(C.low(52n, q), Nat.add(C.shift(52n, C.high(52n, q)), C.shift(52n, EF))), Nat.add(Nat.add(C.low(52n, q), C.shift(52n, C.high(52n, q))), C.shift(52n, EF)), Nat.add(q, C.shift(52n, EF)), Equal.sym(Nat, Nat.add(Nat.add(C.low(52n, q), C.shift(52n, C.high(52n, q))), C.shift(52n, EF)), Nat.add(C.low(52n, q), Nat.add(C.shift(52n, C.high(52n, q)), C.shift(52n, EF))), NA.add_assoc(C.low(52n, q), C.shift(52n, C.high(52n, q)), C.shift(52n, EF))), Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(52n, EF)), Nat.add(C.low(52n, q), C.shift(52n, C.high(52n, q))), q, Equal.sym(Nat, q, Nat.add(C.low(52n, q), C.shift(52n, C.high(52n, q))), WW.low_high(52n, q)))))
765
766# a normal q with its exponent field below 2047 fits the 63-bit pattern
767def qfit(+one: Nat, +h1: {one == 1n : Nat}, +q: Nat, +EF: Nat, +hq: {Nat.is_le(q, C.shift(53n, one)) == True{} : Bool}, +h52: {C.fits(52n, q) == False{} : Bool}, +hov: {Nat.is_lt(Nat.add(EF, SF.pick(Nat, C.fits(53n, q), 1n, 2n)), 2047n) == True{} : Bool}) -> {C.fits(63n, Nat.add(q, C.shift(52n, EF))) == True{} : Bool}:
768  +eH = hpick_c(one, h1, q, hq, h52, C.fits(53n, q), {==})
769  +h2 = L.subst(Nat, z => {Nat.is_lt(Nat.add(EF, z), 2047n) == True{} : Bool}, SF.pick(Nat, C.fits(53n, q), 1n, 2n), C.high(52n, q), Equal.sym(Nat, C.high(52n, q), SF.pick(Nat, C.fits(53n, q), 1n, 2n), eH), hov)
770  +h3 = L.subst(Nat, z => {Nat.is_lt(z, 2047n) == True{} : Bool}, Nat.add(EF, C.high(52n, q)), Nat.add(C.high(52n, q), EF), NA.add_comm(EF, C.high(52n, q)), h2)
771  +f11 = WW.fits_of_lt(11n, Nat.add(C.high(52n, q), EF), N.lt_trans(Nat.add(C.high(52n, q), EF), 2047n, 2048n, h3, {==}))
772  +f = WW.limbs_fit(52n, 11n, C.low(52n, q), Nat.add(C.high(52n, q), EF), WW.low_fits(52n, q), f11)
773  L.subst(Nat, z => {C.fits(63n, z) == True{} : Bool}, Nat.add(C.low(52n, q), C.shift(52n, Nat.add(C.high(52n, q), EF))), Nat.add(q, C.shift(52n, EF)), qsplit(q, EF), f)
774
775def ef11(+EF: Nat, +c: Nat, +hov: {Nat.is_lt(Nat.add(EF, c), 2047n) == True{} : Bool}) -> {C.fits(11n, EF) == True{} : Bool}:
776  WW.fits_of_lt(11n, EF, N.le_lt_trans(EF, Nat.add(EF, c), 2048n, N.le_add_right(EF, c), N.lt_trans(Nat.add(EF, c), 2047n, 2048n, hov, {==})))
777
778# ---- roundPackToF64's last step ----
779
780def rpfE(+s: Bool, +E: Nat, +w: WU.U64, +hS: {C.fits(63n, SW.value(w)) == True{} : Bool}, +hE: {C.fits(11n, E) == True{} : Bool}, +hz: {C.fits(52n, SF.rne(SW.value(w), 10n)) == False{} : Bool}, +hq: {C.fits(63n, Nat.add(SF.rne(SW.value(w), 10n), C.shift(52n, E))) == True{} : Bool}) -> {F.rp_fin(s, E, w) == bits(s, Nat.add(SF.rne(SW.value(w), 10n), C.shift(52n, E))) : F.F64}:
781  +r = X.clear0(X.shr(X.add(w, WU.U64{512, 0}), 10n), U32.is_eq(U32.and(X.lo(w), 1023), 512))
782  +q = SF.rne(SW.value(w), 10n)
783  +ev = rpw(w, hS)
784  z0 = WA.is_zero_value(r)
785  +hzr = Equal.trans(Bool, X.is_zero(r), Nat.is_eq(SW.value(r), 0n), False{}, z0, Equal.trans(Bool, Nat.is_eq(SW.value(r), 0n), Nat.is_eq(q, 0n), False{}, Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), SW.value(r), q, ev), nz_of(52n, q, hz)))
786  +e1 = Equal.cong(Bool, F.F64, t => F.pack(s, F.zero_e(E, t), r), X.is_zero(r), False{}, hzr)
787  +hn = L.subst(Nat, z => {C.fits(63n, Nat.add(z, C.shift(52n, E))) == True{} : Bool}, q, SW.value(r), Equal.sym(Nat, SW.value(r), q, ev), hq)
788  +e2 = pack_v(s, E, hE, r, hn)
789  +e3 = Equal.cong(Nat, F.F64, z => bits(s, Nat.add(z, C.shift(52n, E))), SW.value(r), q, ev)
790  Equal.trans(F.F64, F.pack(s, F.zero_e(E, X.is_zero(r)), r), F.pack(s, E, r), bits(s, Nat.add(q, C.shift(52n, E))), e1, Equal.trans(F.F64, F.pack(s, E, r), bits(s, Nat.add(SW.value(r), C.shift(52n, E))), bits(s, Nat.add(q, C.shift(52n, E))), e2, e3))
791
792def rpf0(+s: Bool, +w: WU.U64, +hS: {C.fits(63n, SW.value(w)) == True{} : Bool}, +hq: {C.fits(63n, Nat.add(SF.rne(SW.value(w), 10n), C.shift(52n, 0n))) == True{} : Bool}) -> {F.rp_fin(s, 0n, w) == bits(s, Nat.add(SF.rne(SW.value(w), 10n), C.shift(52n, 0n))) : F.F64}:
793  +r = X.clear0(X.shr(X.add(w, WU.U64{512, 0}), 10n), U32.is_eq(U32.and(X.lo(w), 1023), 512))
794  +q = SF.rne(SW.value(w), 10n)
795  +ev = rpw(w, hS)
796  +e1 = Equal.cong(Nat, F.F64, t => F.pack(s, t, r), F.zero_e(0n, X.is_zero(r)), 0n, ze0(X.is_zero(r)))
797  +hn = L.subst(Nat, z => {C.fits(63n, Nat.add(z, C.shift(52n, 0n))) == True{} : Bool}, q, SW.value(r), Equal.sym(Nat, SW.value(r), q, ev), hq)
798  +e2 = pack_v(s, 0n, {==}, r, hn)
799  +e3 = Equal.cong(Nat, F.F64, z => bits(s, Nat.add(z, C.shift(52n, 0n))), SW.value(r), q, ev)
800  Equal.trans(F.F64, F.pack(s, F.zero_e(0n, X.is_zero(r)), r), F.pack(s, 0n, r), bits(s, Nat.add(q, C.shift(52n, 0n))), e1, Equal.trans(F.F64, F.pack(s, 0n, r), bits(s, Nat.add(SW.value(r), C.shift(52n, 0n))), bits(s, Nat.add(q, C.shift(52n, 0n))), e2, e3))
801
802
803# ---- roundPackToF64 is the spec's round ----
804
805def esub63(+x: Nat) -> {Nat.sub(Nat.add(x, 63n), 53n) == Nat.add(10n, x) : Nat}:
806  Equal.trans(Nat, Nat.sub(Nat.add(x, 63n), 53n), Nat.sub(Nat.add(63n, x), 53n), Nat.add(10n, x), Equal.cong(Nat, Nat, z => Nat.sub(z, 53n), Nat.add(x, 63n), Nat.add(63n, x), NA.add_comm(x, 63n)), {==})
807
808def sr(+s: Bool, +m: Nat, +x: Nat, +h62: {C.fits(62n, m) == False{} : Bool}, +h63: {C.fits(63n, m) == True{} : Bool}) -> {SF.round(s, m, x) == SF.round_u(s, m, x, Nat.max(Nat.add(10n, x), 1926n)) : F.F64}:
809  +e1 = Equal.cong(Bool, F.F64, t => SF.pick(F.F64, t, SF.zero(s), SF.round_u(s, m, x, Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)))), Nat.is_eq(m, 0n), False{}, nz_of(62n, m, h62))
810  +e2 = Equal.cong(Nat, F.F64, z => SF.round_u(s, m, x, Nat.max(Nat.sub(Nat.add(x, z), 53n), Nat.sub(SF.zb(), 1074n))), M.bit_length(m), 63n, bl63(m, h62, h63))
811  +e3 = Equal.cong(Nat, F.F64, z => SF.round_u(s, m, x, Nat.max(z, Nat.sub(SF.zb(), 1074n))), Nat.sub(Nat.add(x, 63n), 53n), Nat.add(10n, x), esub63(x))
812  Equal.trans(F.F64, SF.round(s, m, x), SF.round_u(s, m, x, Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SF.round_u(s, m, x, Nat.max(Nat.add(10n, x), 1926n)), e1, Equal.trans(F.F64, SF.round_u(s, m, x, Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SF.round_u(s, m, x, Nat.max(Nat.sub(Nat.add(x, 63n), 53n), Nat.sub(SF.zb(), 1074n))), SF.round_u(s, m, x, Nat.max(Nat.add(10n, x), 1926n)), e2, e3))
813
814def lt_sub_pos(+x: Nat, +n: Nat, +h: {Nat.is_lt(x, n) == True{} : Bool}) -> {Nat.is_le(1n, Nat.sub(n, x)) == True{} : Bool}:
815  match x n:
816    case 0n 0n:
817      NC.absurd_tf({Nat.is_le(1n, 0n) == True{} : Bool}, h)
818    case 0n 1n+ +np:
819      N.zero_le(np)
820    case 1n+ +xp 0n:
821      NC.absurd_tf({Nat.is_le(1n, 0n) == True{} : Bool}, h)
822    case 1n+ +xp 1n+ +np:
823      lt_sub_pos(xp, np, h)
824
825def sub_add_a(+a: Nat, +n: Nat, +x: Nat, +h: {Nat.is_le(x, n) == True{} : Bool}) -> {Nat.sub(Nat.add(a, n), x) == Nat.add(a, Nat.sub(n, x)) : Nat}:
826  Equal.trans(Nat, Nat.sub(Nat.add(a, n), x), Nat.sub(Nat.add(n, a), x), Nat.add(a, Nat.sub(n, x)), Equal.cong(Nat, Nat, z => Nat.sub(z, x), Nat.add(a, n), Nat.add(n, a), NA.add_comm(a, n)), Equal.trans(Nat, Nat.sub(Nat.add(n, a), x), Nat.add(Nat.sub(n, x), a), Nat.add(a, Nat.sub(n, x)), sub_add_r(n, a, x, h), NA.add_comm(Nat.sub(n, x), a)))
827
828def le_cancel_r(+a: Nat, +b: Nat, +c: Nat) -> {Nat.is_le(Nat.add(a, c), Nat.add(b, c)) == Nat.is_le(a, b) : Bool}:
829  Equal.cong(Cmp, Bool, t => Cmp.is_le(t), Nat.cmp(Nat.add(a, c), Nat.add(b, c)), Nat.cmp(a, b), NC.cmp_addr(a, b, c))
830
831def jfit(+d: Nat, +m: Nat, +hd: {Nat.is_le(1n, d) == True{} : Bool}, +h63: {C.fits(63n, m) == True{} : Bool}) -> {C.fits(63n, SW.jam(C.high(d, m), C.low(d, m))) == True{} : Bool}:
832  +h = C.high(d, m)
833  +t = Nat.max(C.bit(h), Nat.min(C.low(d, m), 1n))
834  +hle = L.subst(Nat, z => {Nat.is_le(63n, z) == True{} : Bool}, Nat.add(62n, d), Nat.add(d, 62n), NA.add_comm(62n, d), hd)
835  +fh = Equal.trans(Bool, C.fits(62n, h), C.fits(Nat.add(d, 62n), m), True{}, Equal.sym(Bool, C.fits(Nat.add(d, 62n), m), C.fits(62n, h), fits_hc(d, 62n, m)), SH.fits_mono(63n, Nat.add(d, 62n), m, hle, h63))
836  +fhh = SH.fits_lek(62n, C.half(h), h, half_le(h), fh)
837  +ft = small(t, max_le1(C.bit(h), C.low(d, m), WW.bit_le1(h)))
838  +f = WW.limbs_fit(1n, 62n, t, C.half(h), ft, fhh)
839  L.subst(Nat, z => {C.fits(63n, z) == True{} : Bool}, Nat.add(t, Nat.double(C.half(h))), SW.jam(h, C.low(d, m)), Equal.sym(Nat, SW.jam(h, C.low(d, m)), Nat.add(t, Nat.double(C.half(h))), jam_form(h, C.low(d, m))), f)
840
841def rp_sub(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +e: Nat, +sig: WU.U64, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +h62: {C.fits(62n, SW.value(sig)) == False{} : Bool}, +h63: {C.fits(63n, SW.value(sig)) == True{} : Bool}, +hb: {Nat.is_lt(x, 1916n) == True{} : Bool}, +u: Nat, +hu: {Nat.max(Nat.add(10n, x), 1926n) == u : Nat}) -> {F.rp_neg(s, e, sig, True{}) == SF.round_u(s, SW.value(sig), x, u) : F.F64}:
842  +hu1 = Equal.trans(Nat, u, Nat.max(Nat.add(10n, x), 1926n), 1926n, Equal.sym(Nat, Nat.max(Nat.add(10n, x), 1926n), u, hu), max_r(Nat.add(10n, x), 1926n, hb))
843  +d = Nat.sub(F.off(), e)
844  +ed = Equal.trans(Nat, d, Nat.sub(F.off(), Nat.add(x, 2180n)), Nat.sub(1916n, x), Equal.cong(Nat, Nat, z => Nat.sub(F.off(), z), e, Nat.add(x, 2180n), Equal.sym(Nat, Nat.add(x, 2180n), e, hx)), sub_cancel_r(1916n, x, 2180n))
845  +hd1 = L.subst(Nat, z => {Nat.is_le(1n, z) == True{} : Bool}, Nat.sub(1916n, x), d, Equal.sym(Nat, d, Nat.sub(1916n, x), ed), lt_sub_pos(x, 1916n, hb))
846  +ku = Equal.trans(Nat, Nat.sub(u, x), Nat.sub(1926n, x), Nat.add(10n, d), Equal.cong(Nat, Nat, z => Nat.sub(z, x), u, 1926n, hu1), Equal.trans(Nat, Nat.sub(1926n, x), Nat.add(10n, Nat.sub(1916n, x)), Nat.add(10n, d), sub_add_a(10n, 1916n, x, N.lt_le(x, 1916n, hb)), Equal.cong(Nat, Nat, z => Nat.add(10n, z), Nat.sub(1916n, x), d, Equal.sym(Nat, d, Nat.sub(1916n, x), ed))))
847  +hle = L.subst(Nat, z => {Nat.is_le(x, z) == True{} : Bool}, 1926n, u, Equal.sym(Nat, u, 1926n, hu1), N.le_trans(x, 1916n, 1926n, N.lt_le(x, 1916n, hb), {==}))
848  sj = SH.shr_jam_value(sig, d)
849  sj2 = SH.shr_jam_value(sig, d)
850  +est = sticky(8n, d, SW.value(sig))
851  +eq = Equal.trans(Nat, SF.rne(SW.value(sig), Nat.add(10n, d)), SF.rne(SW.jam(C.high(d, SW.value(sig)), C.low(d, SW.value(sig))), 10n), SF.rne(SW.value(X.shr_jam(sig, d)), 10n), est, Equal.cong(Nat, Nat, z => SF.rne(z, 10n), SW.jam(C.high(d, SW.value(sig)), C.low(d, SW.value(sig))), SW.value(X.shr_jam(sig, d)), Equal.sym(Nat, SW.value(X.shr_jam(sig, d)), SW.jam(C.high(d, SW.value(sig)), C.low(d, SW.value(sig))), sj)))
852  +hJ = L.subst(Nat, z => {C.fits(63n, z) == True{} : Bool}, SW.jam(C.high(d, SW.value(sig)), C.low(d, SW.value(sig))), SW.value(X.shr_jam(sig, d)), Equal.sym(Nat, SW.value(X.shr_jam(sig, d)), SW.jam(C.high(d, SW.value(sig)), C.low(d, SW.value(sig))), sj2), jfit(d, SW.value(sig), hd1, h63))
853  +hqJ = rne_top(one, h1, SW.value(X.shr_jam(sig, d)), hJ)
854  +hq = L.subst(Nat, z => {Nat.is_le(z, C.shift(53n, one)) == True{} : Bool}, SF.rne(SW.value(X.shr_jam(sig, d)), 10n), SF.rne(SW.value(sig), Nat.add(10n, d)), Equal.sym(Nat, SF.rne(SW.value(sig), Nat.add(10n, d)), SF.rne(SW.value(X.shr_jam(sig, d)), 10n), eq), hqJ)
855  +h0 = or_t(Bool.not(C.fits(52n, SF.rne(SW.value(sig), Nat.add(10n, d)))))
856  +hov = pick_lt(C.fits(53n, SF.rne(SW.value(sig), Nat.add(10n, d))))
857  +s1 = Equal.cong(Bool, F.F64, t => SF.pack(s, SF.pick(Nat, t, SF.rne(SW.value(sig), Nat.sub(u, x)), C.shift(Nat.sub(x, u), SW.value(sig))), u), Nat.is_le(x, u), True{}, hle)
858  +s2 = Equal.cong(Nat, F.F64, z => SF.pack(s, SF.rne(SW.value(sig), z), u), Nat.sub(u, x), Nat.add(10n, d), ku)
859  +s3 = pkg(one, h1, s, SF.rne(SW.value(sig), Nat.add(10n, d)), u, 0n, Equal.sym(Nat, u, 1926n, hu1), hq, h0, hov)
860  +sp = Equal.trans(F.F64, SF.round_u(s, SW.value(sig), x, u), SF.pack(s, SF.rne(SW.value(sig), Nat.sub(u, x)), u), bits(s, Nat.add(SF.rne(SW.value(sig), Nat.add(10n, d)), C.shift(52n, 0n))), s1, Equal.trans(F.F64, SF.pack(s, SF.rne(SW.value(sig), Nat.sub(u, x)), u), SF.pack(s, SF.rne(SW.value(sig), Nat.add(10n, d)), u), bits(s, Nat.add(SF.rne(SW.value(sig), Nat.add(10n, d)), C.shift(52n, 0n))), s2, s3))
861  +f54 = SH.fits_mono(54n, 63n, SF.rne(SW.value(X.shr_jam(sig, d)), 10n), {==}, fit54(one, h1, SF.rne(SW.value(X.shr_jam(sig, d)), 10n), hqJ))
862  +hq0 = L.subst(Nat, z => {C.fits(63n, z) == True{} : Bool}, SF.rne(SW.value(X.shr_jam(sig, d)), 10n), Nat.add(SF.rne(SW.value(X.shr_jam(sig, d)), 10n), 0n), Equal.sym(Nat, Nat.add(SF.rne(SW.value(X.shr_jam(sig, d)), 10n), 0n), SF.rne(SW.value(X.shr_jam(sig, d)), 10n), N.add_zero(SF.rne(SW.value(X.shr_jam(sig, d)), 10n))), f54)
863  +i1 = rpf0(s, X.shr_jam(sig, d), hJ, hq0)
864  +i2 = Equal.cong(Nat, F.F64, z => bits(s, Nat.add(z, C.shift(52n, 0n))), SF.rne(SW.value(X.shr_jam(sig, d)), 10n), SF.rne(SW.value(sig), Nat.add(10n, d)), Equal.sym(Nat, SF.rne(SW.value(sig), Nat.add(10n, d)), SF.rne(SW.value(X.shr_jam(sig, d)), 10n), eq))
865  Equal.trans(F.F64, F.rp_fin(s, 0n, X.shr_jam(sig, d)), bits(s, Nat.add(SF.rne(SW.value(sig), Nat.add(10n, d)), C.shift(52n, 0n))), SF.round_u(s, SW.value(sig), x, u), Equal.trans(F.F64, F.rp_fin(s, 0n, X.shr_jam(sig, d)), bits(s, Nat.add(SF.rne(SW.value(X.shr_jam(sig, d)), 10n), C.shift(52n, 0n))), bits(s, Nat.add(SF.rne(SW.value(sig), Nat.add(10n, d)), C.shift(52n, 0n))), i1, i2), Equal.sym(F.F64, SF.round_u(s, SW.value(sig), x, u), bits(s, Nat.add(SF.rne(SW.value(sig), Nat.add(10n, d)), C.shift(52n, 0n))), sp))
866
867def ov_eq(+one: Nat, +h1: {one == 1n : Nat}, +e: Nat, +sig: WU.U64, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +hge: {Nat.is_le(1916n, x) == True{} : Bool}, +h63: {C.fits(63n, SW.value(sig)) == True{} : Bool}) -> {Bool.or(Nat.is_lt(Nat.add(F.off(), 2045n), e), Bool.and(Nat.is_eq(e, Nat.add(F.off(), 2045n)), X.le(WU.U64{0, 2147483648}, X.add(sig, WU.U64{512, 0})))) == Bool.not(Nat.is_lt(Nat.add(Nat.sub(e, F.off()), SF.pick(Nat, C.fits(53n, SF.rne(SW.value(sig), 10n)), 1n, 2n)), 2047n)) : Bool}:
868  +he = L.subst(Nat, z => {Nat.is_le(F.off(), z) == True{} : Bool}, Nat.add(x, 2180n), e, hx, Equal.trans(Bool, Nat.is_le(Nat.add(1916n, 2180n), Nat.add(x, 2180n)), Nat.is_le(1916n, x), True{}, le_cancel_r(1916n, x, 2180n), hge))
869  +ee = Equal.trans(Nat, e, Nat.add(4096n, Nat.sub(e, F.off())), Nat.add(Nat.sub(e, F.off()), 4096n), Equal.sym(Nat, Nat.add(4096n, Nat.sub(e, F.off())), e, N.sub_add(e, 4096n, he)), NA.add_comm(4096n, Nat.sub(e, F.off())))
870  +a1 = Equal.trans(Bool, Nat.is_lt(6141n, e), Nat.is_lt(6141n, Nat.add(Nat.sub(e, F.off()), 4096n)), Nat.is_lt(2045n, Nat.sub(e, F.off())), Equal.cong(Nat, Bool, z => Nat.is_lt(6141n, z), e, Nat.add(Nat.sub(e, F.off()), 4096n), ee), WW.lt_cancel_r(2045n, Nat.sub(e, F.off()), 4096n))
871  +a2 = Equal.trans(Bool, Nat.is_eq(e, 6141n), Nat.is_eq(Nat.add(Nat.sub(e, F.off()), 4096n), 6141n), Nat.is_eq(Nat.sub(e, F.off()), 2045n), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 6141n), e, Nat.add(Nat.sub(e, F.off()), 4096n), ee), eq_cancel_r(Nat.sub(e, F.off()), 2045n, 4096n))
872  +a3 = Equal.trans(Bool, X.le(WU.U64{0, 2147483648}, X.add(sig, WU.U64{512, 0})), Bool.not(C.fits(63n, Nat.add(SW.value(sig), 512n))), Bool.not(C.fits(53n, SF.rne(SW.value(sig), 10n))), ovle(one, h1, sig, h63, 2147483648, {==}), Equal.cong(Bool, Bool, t => Bool.not(t), C.fits(63n, Nat.add(SW.value(sig), 512n)), C.fits(53n, SF.rne(SW.value(sig), 10n)), Equal.sym(Bool, C.fits(53n, SF.rne(SW.value(sig), 10n)), C.fits(63n, Nat.add(SW.value(sig), 512n)), p2(one, h1, SW.value(sig), h63))))
873  +LE = X.le(WU.U64{0, 2147483648}, X.add(sig, WU.U64{512, 0}))
874  +c1 = Equal.cong(Bool, Bool, t => Bool.or(t, Bool.and(Nat.is_eq(e, 6141n), LE)), Nat.is_lt(6141n, e), Nat.is_lt(2045n, Nat.sub(e, F.off())), a1)
875  +c2 = Equal.cong(Bool, Bool, t => Bool.or(Nat.is_lt(2045n, Nat.sub(e, F.off())), Bool.and(t, LE)), Nat.is_eq(e, 6141n), Nat.is_eq(Nat.sub(e, F.off()), 2045n), a2)
876  +c3 = Equal.cong(Bool, Bool, t => Bool.or(Nat.is_lt(2045n, Nat.sub(e, F.off())), Bool.and(Nat.is_eq(Nat.sub(e, F.off()), 2045n), t)), LE, Bool.not(C.fits(53n, SF.rne(SW.value(sig), 10n))), a3)
877  Equal.trans(Bool, Bool.or(Nat.is_lt(6141n, e), Bool.and(Nat.is_eq(e, 6141n), LE)), Bool.or(Nat.is_lt(2045n, Nat.sub(e, F.off())), Bool.and(Nat.is_eq(e, 6141n), LE)), Bool.not(Nat.is_lt(Nat.add(Nat.sub(e, F.off()), SF.pick(Nat, C.fits(53n, SF.rne(SW.value(sig), 10n)), 1n, 2n)), 2047n)), c1, Equal.trans(Bool, Bool.or(Nat.is_lt(2045n, Nat.sub(e, F.off())), Bool.and(Nat.is_eq(e, 6141n), LE)), Bool.or(Nat.is_lt(2045n, Nat.sub(e, F.off())), Bool.and(Nat.is_eq(Nat.sub(e, F.off()), 2045n), LE)), Bool.not(Nat.is_lt(Nat.add(Nat.sub(e, F.off()), SF.pick(Nat, C.fits(53n, SF.rne(SW.value(sig), 10n)), 1n, 2n)), 2047n)), c2, Equal.trans(Bool, Bool.or(Nat.is_lt(2045n, Nat.sub(e, F.off())), Bool.and(Nat.is_eq(Nat.sub(e, F.off()), 2045n), LE)), Bool.or(Nat.is_lt(2045n, Nat.sub(e, F.off())), Bool.and(Nat.is_eq(Nat.sub(e, F.off()), 2045n), Bool.not(C.fits(53n, SF.rne(SW.value(sig), 10n))))), Bool.not(Nat.is_lt(Nat.add(Nat.sub(e, F.off()), SF.pick(Nat, C.fits(53n, SF.rne(SW.value(sig), 10n)), 1n, 2n)), 2047n)), c3, ov_c(Nat.sub(e, F.off()), C.fits(53n, SF.rne(SW.value(sig), 10n))))))
878
879def rp_nc(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +e: Nat, +sig: WU.U64, +x: Nat, +h62: {C.fits(62n, SW.value(sig)) == False{} : Bool}, +h63: {C.fits(63n, SW.value(sig)) == True{} : Bool}, +u: Nat, +hEF: {Nat.add(Nat.sub(e, F.off()), 1926n) == u : Nat}, +o: Bool, +ho: {Bool.not(Nat.is_lt(Nat.add(Nat.sub(e, F.off()), SF.pick(Nat, C.fits(53n, SF.rne(SW.value(sig), 10n)), 1n, 2n)), 2047n)) == o : Bool}) -> {F.rp_over(s, e, sig, o) == SF.pack(s, SF.rne(SW.value(sig), 10n), u) : F.F64}:
880  match o:
881    case True{}:
882      +hovF = not_t(Nat.is_lt(Nat.add(Nat.sub(e, F.off()), SF.pick(Nat, C.fits(53n, SF.rne(SW.value(sig), 10n)), 1n, 2n)), 2047n), ho)
883      Equal.trans(F.F64, F.inf(s), SF.inf(s), SF.pack(s, SF.rne(SW.value(sig), 10n), u), inf_v(s), Equal.sym(F.F64, SF.pack(s, SF.rne(SW.value(sig), 10n), u), SF.inf(s), pko(s, SF.rne(SW.value(sig), 10n), u, Nat.sub(e, F.off()), hEF, rne_norm(SW.value(sig), h62), hovF)))
884    case False{}:
885      +hovT = not_f(Nat.is_lt(Nat.add(Nat.sub(e, F.off()), SF.pick(Nat, C.fits(53n, SF.rne(SW.value(sig), 10n)), 1n, 2n)), 2047n), ho)
886      +hz = rne_norm(SW.value(sig), h62)
887      +hq = rne_top(one, h1, SW.value(sig), h63)
888      +i1 = rpfE(s, Nat.sub(e, F.off()), sig, h63, ef11(Nat.sub(e, F.off()), SF.pick(Nat, C.fits(53n, SF.rne(SW.value(sig), 10n)), 1n, 2n), hovT), hz, qfit(one, h1, SF.rne(SW.value(sig), 10n), Nat.sub(e, F.off()), hq, hz, hovT))
889      +h0 = Equal.cong(Bool, Bool, t => Bool.or(Bool.not(t), Nat.is_eq(Nat.sub(e, F.off()), 0n)), C.fits(52n, SF.rne(SW.value(sig), 10n)), False{}, hz)
890      +sp = pkg(one, h1, s, SF.rne(SW.value(sig), 10n), u, Nat.sub(e, F.off()), hEF, hq, h0, hovT)
891      Equal.trans(F.F64, F.rp_fin(s, Nat.sub(e, F.off()), sig), bits(s, Nat.add(SF.rne(SW.value(sig), 10n), C.shift(52n, Nat.sub(e, F.off())))), SF.pack(s, SF.rne(SW.value(sig), 10n), u), i1, Equal.sym(F.F64, SF.pack(s, SF.rne(SW.value(sig), 10n), u), bits(s, Nat.add(SF.rne(SW.value(sig), 10n), C.shift(52n, Nat.sub(e, F.off())))), sp))
892
893def rp_norm(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +e: Nat, +sig: WU.U64, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +h62: {C.fits(62n, SW.value(sig)) == False{} : Bool}, +h63: {C.fits(63n, SW.value(sig)) == True{} : Bool}, +hb: {Nat.is_lt(x, 1916n) == False{} : Bool}, +u: Nat, +hu: {Nat.max(Nat.add(10n, x), 1926n) == u : Nat}) -> {F.rp_neg(s, e, sig, False{}) == SF.round_u(s, SW.value(sig), x, u) : F.F64}:
894  +hge = N.not_lt_le(x, 1916n, hb)
895  +hu1 = Equal.trans(Nat, u, Nat.max(Nat.add(10n, x), 1926n), Nat.add(10n, x), Equal.sym(Nat, Nat.max(Nat.add(10n, x), 1926n), u, hu), max_l(Nat.add(10n, x), 1926n, hge))
896  +eEF = Equal.trans(Nat, Nat.sub(e, F.off()), Nat.sub(Nat.add(x, 2180n), F.off()), Nat.sub(x, 1916n), Equal.cong(Nat, Nat, z => Nat.sub(z, F.off()), e, Nat.add(x, 2180n), Equal.sym(Nat, Nat.add(x, 2180n), e, hx)), sub_cancel_r(x, 1916n, 2180n))
897  +y = Nat.sub(x, 1916n)
898  +ex = Equal.trans(Nat, Nat.add(y, 1926n), Nat.add(Nat.add(y, 1916n), 10n), u, Equal.sym(Nat, Nat.add(Nat.add(y, 1916n), 10n), Nat.add(y, 1926n), NA.add_assoc(y, 1916n, 10n)), Equal.trans(Nat, Nat.add(Nat.add(y, 1916n), 10n), Nat.add(x, 10n), u, Equal.cong(Nat, Nat, z => Nat.add(z, 10n), Nat.add(y, 1916n), x, Equal.trans(Nat, Nat.add(y, 1916n), Nat.add(1916n, y), x, NA.add_comm(y, 1916n), N.sub_add(x, 1916n, hge))), Equal.trans(Nat, Nat.add(x, 10n), Nat.add(10n, x), u, NA.add_comm(x, 10n), Equal.sym(Nat, u, Nat.add(10n, x), hu1))))
899  +hEF = Equal.trans(Nat, Nat.add(Nat.sub(e, F.off()), 1926n), Nat.add(y, 1926n), u, Equal.cong(Nat, Nat, z => Nat.add(z, 1926n), Nat.sub(e, F.off()), y, eEF), ex)
900  +hle = L.subst(Nat, z => {Nat.is_le(x, z) == True{} : Bool}, Nat.add(10n, x), u, Equal.sym(Nat, u, Nat.add(10n, x), hu1), L.subst(Nat, z => {Nat.is_le(x, z) == True{} : Bool}, Nat.add(x, 10n), Nat.add(10n, x), NA.add_comm(x, 10n), N.le_add_right(x, 10n)))
901  +ku = Equal.trans(Nat, Nat.sub(u, x), Nat.sub(Nat.add(10n, x), x), 10n, Equal.cong(Nat, Nat, z => Nat.sub(z, x), u, Nat.add(10n, x), hu1), sub_add_l(10n, x))
902  +s1 = Equal.cong(Bool, F.F64, t => SF.pack(s, SF.pick(Nat, t, SF.rne(SW.value(sig), Nat.sub(u, x)), C.shift(Nat.sub(x, u), SW.value(sig))), u), Nat.is_le(x, u), True{}, hle)
903  +s2 = Equal.cong(Nat, F.F64, z => SF.pack(s, SF.rne(SW.value(sig), z), u), Nat.sub(u, x), 10n, ku)
904  +sp = Equal.trans(F.F64, SF.round_u(s, SW.value(sig), x, u), SF.pack(s, SF.rne(SW.value(sig), Nat.sub(u, x)), u), SF.pack(s, SF.rne(SW.value(sig), 10n), u), s1, s2)
905  +eo = ov_eq(one, h1, e, sig, x, hx, hge, h63)
906  +i1 = Equal.cong(Bool, F.F64, t => F.rp_over(s, e, sig, t), Bool.or(Nat.is_lt(Nat.add(F.off(), 2045n), e), Bool.and(Nat.is_eq(e, Nat.add(F.off(), 2045n)), X.le(WU.U64{0, 2147483648}, X.add(sig, WU.U64{512, 0})))), Bool.not(Nat.is_lt(Nat.add(Nat.sub(e, F.off()), SF.pick(Nat, C.fits(53n, SF.rne(SW.value(sig), 10n)), 1n, 2n)), 2047n)), eo)
907  +i2 = rp_nc(one, h1, s, e, sig, x, h62, h63, u, hEF, Bool.not(Nat.is_lt(Nat.add(Nat.sub(e, F.off()), SF.pick(Nat, C.fits(53n, SF.rne(SW.value(sig), 10n)), 1n, 2n)), 2047n)), {==})
908  Equal.trans(F.F64, F.rp_over(s, e, sig, Bool.or(Nat.is_lt(Nat.add(F.off(), 2045n), e), Bool.and(Nat.is_eq(e, Nat.add(F.off(), 2045n)), X.le(WU.U64{0, 2147483648}, X.add(sig, WU.U64{512, 0}))))), SF.pack(s, SF.rne(SW.value(sig), 10n), u), SF.round_u(s, SW.value(sig), x, u), Equal.trans(F.F64, F.rp_over(s, e, sig, Bool.or(Nat.is_lt(Nat.add(F.off(), 2045n), e), Bool.and(Nat.is_eq(e, Nat.add(F.off(), 2045n)), X.le(WU.U64{0, 2147483648}, X.add(sig, WU.U64{512, 0}))))), F.rp_over(s, e, sig, Bool.not(Nat.is_lt(Nat.add(Nat.sub(e, F.off()), SF.pick(Nat, C.fits(53n, SF.rne(SW.value(sig), 10n)), 1n, 2n)), 2047n))), SF.pack(s, SF.rne(SW.value(sig), 10n), u), i1, i2), Equal.sym(F.F64, SF.round_u(s, SW.value(sig), x, u), SF.pack(s, SF.rne(SW.value(sig), 10n), u), sp))
909
910def rp_c2(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +e: Nat, +sig: WU.U64, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +h62: {C.fits(62n, SW.value(sig)) == False{} : Bool}, +h63: {C.fits(63n, SW.value(sig)) == True{} : Bool}, +b: Bool, +hb: {Nat.is_lt(x, 1916n) == b : Bool}, +u: Nat, +hu: {Nat.max(Nat.add(10n, x), 1926n) == u : Nat}) -> {F.rp_neg(s, e, sig, b) == SF.round_u(s, SW.value(sig), x, u) : F.F64}:
911  match b:
912    case True{}:
913      rp_sub(one, h1, s, e, sig, x, hx, h62, h63, hb, u, hu)
914    case False{}:
915      rp_norm(one, h1, s, e, sig, x, hx, h62, h63, hb, u, hu)
916
917# SoftFloat's roundPackToF64(s, e, sig), sig with its top bit at 62 and e the
918# biased exponent minus one plus OFF, is Flocq's round_NE of s * sig * 2^(e - 2180 - Z)
919def round_pack(+s: Bool, +e: Nat, +sig: WU.U64, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +h62: {C.fits(62n, SW.value(sig)) == False{} : Bool}, +h63: {C.fits(63n, SW.value(sig)) == True{} : Bool}) -> {F.round_pack(s, e, sig) == SF.round(s, SW.value(sig), x) : F.F64}:
920  +elt = Equal.trans(Bool, Nat.is_lt(e, F.off()), Nat.is_lt(Nat.add(x, 2180n), F.off()), Nat.is_lt(x, 1916n), Equal.cong(Nat, Bool, z => Nat.is_lt(z, F.off()), e, Nat.add(x, 2180n), Equal.sym(Nat, Nat.add(x, 2180n), e, hx)), WW.lt_cancel_r(x, 1916n, 2180n))
921  +i1 = Equal.cong(Bool, F.F64, t => F.rp_neg(s, e, sig, t), Nat.is_lt(e, F.off()), Nat.is_lt(x, 1916n), elt)
922  +i2 = rp_c2(1n, {==}, s, e, sig, x, hx, h62, h63, Nat.is_lt(x, 1916n), {==}, Nat.max(Nat.add(10n, x), 1926n), {==})
923  +s0 = sr(s, SW.value(sig), x, h62, h63)
924  Equal.trans(F.F64, F.rp_neg(s, e, sig, Nat.is_lt(e, F.off())), SF.round_u(s, SW.value(sig), x, Nat.max(Nat.add(10n, x), 1926n)), SF.round(s, SW.value(sig), x), Equal.trans(F.F64, F.rp_neg(s, e, sig, Nat.is_lt(e, F.off())), F.rp_neg(s, e, sig, Nat.is_lt(x, 1916n)), SF.round_u(s, SW.value(sig), x, Nat.max(Nat.add(10n, x), 1926n)), i1, i2), Equal.sym(F.F64, SF.round(s, SW.value(sig), x), SF.round_u(s, SW.value(sig), x, Nat.max(Nat.add(10n, x), 1926n)), s0))