def pack_g

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64round.bend:368

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/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/lib/word.bend as WD

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)