def ws_o

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64next.bend:251

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR

251# a word of value n < 2^63 with the sign bit added is bits(s, n)
252# 2^32 stays `one` shifted: the checker never builds the closed 2^32
253def ws_o(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +w: WU.U64, +h63: {C.fits(63n, SW.value(w)) == True{} : Bool}) -> {F.with_sign(s, w) == FR.bits(s, SW.value(w)) : F.F64}:
254  +lo = X.lo(w)
255  +hi = X.hi(w)
256  +V = SW.value(w)
257  +b = SF.b2n(s)
258  +T31 = C.shift(31n, b)
259  +eta = WA.val_eta(w)
260  +eh = Equal.trans(Nat, C.high(32n, V), C.high(32n, Nat.add(v(lo), C.shift(32n, v(hi)))), v(hi), Equal.cong(Nat, Nat, t => C.high(32n, t), V, Nat.add(v(lo), C.shift(32n, v(hi))), WA.val_eta(w)), WW.high_u(32n, v(lo), v(hi), LW.vb(lo)))
261  +f31 = L.subst(Nat, t => {C.fits(31n, t) == True{} : Bool}, C.high(32n, V), v(hi), eh, SH.fits_high(32n, 31n, V, h63))
262  +esg = Equal.trans(Nat, v(F.sgn(s)), v(SF.pick(U32, s, 2147483648, 0)), T31, Equal.cong(U32, Nat, t => v(t), F.sgn(s), SF.pick(U32, s, 2147483648, 0), FR.sgn_pick(s)), FR.sgv(1n, {==}, s, 2147483648, {==}))
263  +fs = WW.limbs_fit(31n, 1n, v(hi), b, f31, FR.b2n_le(s))
264  +hs0 = WW.lt_one(32n, one, h1, Nat.add(v(hi), T31), fs)
265  +hs = L.subst(Nat, t => {Nat.is_lt(Nat.add(v(hi), t), C.shift(32n, one)) == True{} : Bool}, T31, v(F.sgn(s)), Equal.sym(Nat, v(F.sgn(s)), T31, esg), hs0)
266  +eadd = Equal.trans(Nat, v(U32.add(hi, F.sgn(s))), Nat.add(v(hi), v(F.sgn(s))), Nat.add(v(hi), T31), FB.addv(one, h1, hi, F.sgn(s), hs), Equal.cong(Nat, Nat, t => Nat.add(v(hi), t), v(F.sgn(s)), T31, esg))
267  +q1 = Nat.add(v(lo), C.shift(32n, v(U32.add(hi, F.sgn(s)))))
268  +q2 = Nat.add(v(lo), C.shift(32n, Nat.add(v(hi), T31)))
269  +q3 = Nat.add(v(lo), Nat.add(C.shift(32n, v(hi)), C.shift(32n, T31)))
270  +q4 = Nat.add(v(lo), Nat.add(C.shift(32n, v(hi)), C.shift(63n, b)))
271  +q5 = Nat.add(Nat.add(v(lo), C.shift(32n, v(hi))), C.shift(63n, b))
272  +q6 = Nat.add(V, C.shift(63n, b))
273  +g1 = Equal.cong(Nat, Nat, t => Nat.add(v(lo), C.shift(32n, t)), v(U32.add(hi, F.sgn(s))), Nat.add(v(hi), T31), eadd)
274  +g2 = Equal.cong(Nat, Nat, t => Nat.add(v(lo), t), C.shift(32n, Nat.add(v(hi), T31)), Nat.add(C.shift(32n, v(hi)), C.shift(32n, T31)), WW.shift_add(32n, v(hi), T31))
275  +g3 = Equal.cong(Nat, Nat, t => Nat.add(v(lo), Nat.add(C.shift(32n, v(hi)), t)), C.shift(32n, T31), C.shift(63n, b), Equal.sym(Nat, C.shift(63n, b), C.shift(32n, T31), WW.shift_comp(32n, 31n, b)))
276  +g4 = Equal.sym(Nat, q5, q4, NA.add_assoc(v(lo), C.shift(32n, v(hi)), C.shift(63n, b)))
277  +g5 = Equal.cong(Nat, Nat, t => Nat.add(t, C.shift(63n, b)), Nat.add(v(lo), C.shift(32n, v(hi))), V, Equal.sym(Nat, V, Nat.add(v(lo), C.shift(32n, v(hi))), eta))
278  +hw = Equal.trans(Nat, q1, q2, q6, g1, Equal.trans(Nat, q2, q3, q6, g2, Equal.trans(Nat, q3, q4, q6, g3, Equal.trans(Nat, q4, q5, q6, g4, g5))))
279  FR.bits_of(s, V, WU.U64{lo, U32.add(hi, F.sgn(s))}, hw)