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