def bits_of

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

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/math/typed/width.bend as WW
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/w64add.bend as WA

296def bits_of(+s: Bool, +n: Nat, +w: WU.U64, +hw: {SW.value(w) == Nat.add(n, C.shift(63n, SF.b2n(s))) : Nat}) -> {F.pack64(w) == bits(s, n) : F.F64}:
297  +lo = X.lo(w)
298  +hi = X.hi(w)
299  +t = C.shift(31n, SF.b2n(s))
300  +e63 = WW.shift_comp(32n, 31n, SF.b2n(s))
301  +ew = Equal.trans(Nat, Nat.add(v(lo), C.shift(32n, v(hi))), SW.value(w), Nat.add(n, C.shift(32n, t)), Equal.sym(Nat, SW.value(w), Nat.add(v(lo), C.shift(32n, v(hi))), WA.val_eta(w)), Equal.trans(Nat, SW.value(w), Nat.add(n, C.shift(63n, SF.b2n(s))), Nat.add(n, C.shift(32n, t)), hw, Equal.cong(Nat, Nat, z => Nat.add(n, z), C.shift(63n, SF.b2n(s)), C.shift(32n, t), e63)))
302  +el = Equal.trans(Nat, C.low(32n, n), C.low(32n, Nat.add(n, C.shift(32n, t))), v(lo), Equal.sym(Nat, C.low(32n, Nat.add(n, C.shift(32n, t))), C.low(32n, n), WW.low_add_shift(32n, n, t)), Equal.trans(Nat, C.low(32n, Nat.add(n, C.shift(32n, t))), C.low(32n, Nat.add(v(lo), C.shift(32n, v(hi)))), v(lo), Equal.cong(Nat, Nat, z => C.low(32n, z), Nat.add(n, C.shift(32n, t)), Nat.add(v(lo), C.shift(32n, v(hi))), Equal.sym(Nat, Nat.add(v(lo), C.shift(32n, v(hi))), Nat.add(n, C.shift(32n, t)), ew)), WW.low_u(32n, v(lo), v(hi), LW.vb(lo))))
303  +eh = Equal.trans(Nat, Nat.add(C.high(32n, n), t), C.high(32n, Nat.add(n, C.shift(32n, t))), v(hi), Equal.sym(Nat, C.high(32n, Nat.add(n, C.shift(32n, t))), Nat.add(C.high(32n, n), t), WW.high_add_shift(32n, n, t)), Equal.trans(Nat, C.high(32n, Nat.add(n, C.shift(32n, t))), C.high(32n, Nat.add(v(lo), C.shift(32n, v(hi)))), v(hi), Equal.cong(Nat, Nat, z => C.high(32n, z), Nat.add(n, C.shift(32n, t)), Nat.add(v(lo), C.shift(32n, v(hi))), Equal.sym(Nat, Nat.add(v(lo), C.shift(32n, v(hi))), Nat.add(n, C.shift(32n, t)), ew)), WW.high_u(32n, v(lo), v(hi), LW.vb(lo))))
304  +ul = Equal.trans(U32, U32.from_nat(C.low(32n, n)), U32.from_nat(v(lo)), lo, Equal.cong(Nat, U32, z => U32.from_nat(z), C.low(32n, n), v(lo), el), LW.rt(lo))
305  +uh = Equal.trans(U32, U32.from_nat(Nat.add(C.high(32n, n), t)), U32.from_nat(v(hi)), hi, Equal.cong(Nat, U32, z => U32.from_nat(z), Nat.add(C.high(32n, n), t), v(hi), eh), LW.rt(hi))
306  +e = Equal.trans(F.F64, bits(s, n), F.Bits{lo, U32.from_nat(Nat.add(C.high(32n, n), t))}, F.Bits{lo, hi}, Equal.cong(U32, F.F64, z => F.Bits{z, U32.from_nat(Nat.add(C.high(32n, n), t))}, U32.from_nat(C.low(32n, n)), lo, ul), Equal.cong(U32, F.F64, z => F.Bits{lo, z}, U32.from_nat(Nat.add(C.high(32n, n), t)), hi, uh))
307  Equal.sym(F.F64, bits(s, n), F.Bits{lo, hi}, e)