Float.pack_q: def of bend-collections-laws-math@1.0.0.0 Import: import bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend as Float Lines 208-235 of bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend&start_line=208&end_line=235 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 # pack(q, X) is the pattern with exponent field j + 970 and fraction q mod 2^52 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}: +X = Nat.add(j, 2895n) +EF = Nat.add(j, 969n) +E = Nat.add(j, 970n) +l52 = C.low(52n, q) +hEF = N.add_assoc(j, 969n, 1926n) +hq = N.lt_le(q, C.shift(53n, one), WW.lt_one(53n, one, h1, q, f53)) +h0 = Equal.cong(Bool, Bool, c => Bool.or(Bool.not(c), Nat.is_eq(EF, 0n)), C.fits(52n, q), False{}, n52) +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)) +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, {==})) +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) +p1 = FR.pkg(one, h1, False{}, q, X, EF, hEF, hq, h0, hov) +p2 = FR.enc_bits(False{}, E, l52) +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) +eHo = Equal.trans(Nat, C.high(52n, q), 1n, one, eH, Equal.sym(Nat, one, 1n, h1)) +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)) +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))) +n1 = Equal.cong(Nat, Nat, z => Nat.add(l52, C.shift(52n, z)), E, Nat.add(one, EF), eE) +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)) +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))) +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)) +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, 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, 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))) +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) 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, 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))) Uses (34): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend&name=subst https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=add_assoc https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=add_comm https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=add_succ https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=le_lt_trans https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=lt_le https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend&name=bits https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend&name=enc_bits https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend&name=f53h https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend&name=hi_one https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend&name=pkg https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=low_high https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=lt_one https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=shift_add https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=fits https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=half https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=high https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=low https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=shift https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=encode https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=pack https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=pick https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=F64