def pack_q

bend-collections-laws-math@1.0.0.0 · proofs/math/random/float.bend:208

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/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
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/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend as FR

208# pack(q, X) is the pattern with exponent field j + 970 and fraction q mod 2^52
209def pack_q(+one: Nat, +h1: {one == 1n : Nat}, +q: Nat, +j: Nat, +hj: {Nat.is_le(j, 52n) == True{} : Bool}, +f53: {C.fits(53n, q) == True{} : Bool}, +n52: {C.fits(52n, q) == False{} : Bool}) -> {SF.pack(False{}, q, Nat.add(j, 2895n)) == SF.encode(False{}, Nat.add(j, 970n), C.low(52n, q)) : F.F64}:
210  +X = Nat.add(j, 2895n)
211  +EF = Nat.add(j, 969n)
212  +E = Nat.add(j, 970n)
213  +l52 = C.low(52n, q)
214  +hEF = N.add_assoc(j, 969n, 1926n)
215  +hq = N.lt_le(q, C.shift(53n, one), WW.lt_one(53n, one, h1, q, f53))
216  +h0 = Equal.cong(Bool, Bool, c => Bool.or(Bool.not(c), Nat.is_eq(EF, 0n)), C.fits(52n, q), False{}, n52)
217  +eA = Equal.trans(Nat, Nat.add(Nat.add(j, 969n), 1n), Nat.add(j, 970n), Nat.add(970n, j), N.add_assoc(j, 969n, 1n), N.add_comm(j, 970n))
218  +ev2 = L.subst(Nat, z => {Nat.is_lt(z, 2047n) == True{} : Bool}, Nat.add(970n, j), Nat.add(Nat.add(j, 969n), 1n), Equal.sym(Nat, Nat.add(Nat.add(j, 969n), 1n), Nat.add(970n, j), eA), N.le_lt_trans(j, 52n, 1077n, hj, {==}))
219  +hov = Equal.trans(Bool, Nat.is_lt(Nat.add(EF, SF.pick(Nat, C.fits(53n, q), 1n, 2n)), 2047n), Nat.is_lt(Nat.add(EF, 1n), 2047n), True{}, Equal.cong(Bool, Bool, c => Nat.is_lt(Nat.add(EF, SF.pick(Nat, c, 1n, 2n)), 2047n), C.fits(53n, q), True{}, f53), ev2)
220  +p1 = FR.pkg(one, h1, False{}, q, X, EF, hEF, hq, h0, hov)
221  +p2 = FR.enc_bits(False{}, E, l52)
222  +eH = FR.hi_one(C.high(52n, q), Equal.trans(Bool, Nat.is_eq(C.half(C.high(52n, q)), 0n), C.fits(53n, q), True{}, Equal.sym(Bool, C.fits(53n, q), Nat.is_eq(C.half(C.high(52n, q)), 0n), FR.f53h(q)), f53), n52)
223  +eHo = Equal.trans(Nat, C.high(52n, q), 1n, one, eH, Equal.sym(Nat, one, 1n, h1))
224  +eq = Equal.trans(Nat, q, Nat.add(l52, C.shift(52n, C.high(52n, q))), Nat.add(l52, C.shift(52n, one)), WW.low_high(52n, q), Equal.cong(Nat, Nat, z => Nat.add(l52, C.shift(52n, z)), C.high(52n, q), one, eHo))
225  +eE = Equal.trans(Nat, E, 1n+EF, Nat.add(one, EF), N.add_succ(j, 969n), Equal.cong(Nat, Nat, z => Nat.add(z, EF), 1n, one, Equal.sym(Nat, one, 1n, h1)))
226  +n1 = Equal.cong(Nat, Nat, z => Nat.add(l52, C.shift(52n, z)), E, Nat.add(one, EF), eE)
227  +n2 = Equal.cong(Nat, Nat, z => Nat.add(l52, z), C.shift(52n, Nat.add(one, EF)), Nat.add(C.shift(52n, one), C.shift(52n, EF)), WW.shift_add(52n, one, EF))
228  +n3 = Equal.sym(Nat, Nat.add(Nat.add(l52, C.shift(52n, one)), C.shift(52n, EF)), Nat.add(l52, Nat.add(C.shift(52n, one), C.shift(52n, EF))), N.add_assoc(l52, C.shift(52n, one), C.shift(52n, EF)))
229  +n4 = Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(52n, EF)), Nat.add(l52, C.shift(52n, one)), q, Equal.sym(Nat, q, Nat.add(l52, C.shift(52n, one)), eq))
230  +nn = Equal.trans(Nat, Nat.add(l52, C.shift(52n, E)), Nat.add(l52, C.shift(52n, Nat.add(one, EF))), Nat.add(q, C.shift(52n, EF)), n1,
231    Equal.trans(Nat, Nat.add(l52, C.shift(52n, Nat.add(one, EF))), Nat.add(l52, Nat.add(C.shift(52n, one), C.shift(52n, EF))), Nat.add(q, C.shift(52n, EF)), n2,
232      Equal.trans(Nat, Nat.add(l52, Nat.add(C.shift(52n, one), C.shift(52n, EF))), Nat.add(Nat.add(l52, C.shift(52n, one)), C.shift(52n, EF)), Nat.add(q, C.shift(52n, EF)), n3, n4)))
233  +p3 = Equal.cong(Nat, F.F64, z => FR.bits(False{}, z), Nat.add(l52, C.shift(52n, E)), Nat.add(q, C.shift(52n, EF)), nn)
234  Equal.trans(F.F64, SF.pack(False{}, q, X), FR.bits(False{}, Nat.add(q, C.shift(52n, EF))), SF.encode(False{}, E, l52), p1,
235    Equal.sym(F.F64, SF.encode(False{}, E, l52), FR.bits(False{}, Nat.add(q, C.shift(52n, EF))), Equal.trans(F.F64, SF.encode(False{}, E, l52), FR.bits(False{}, Nat.add(l52, C.shift(52n, E))), FR.bits(False{}, Nat.add(q, C.shift(52n, EF))), p2, p3)))