def enc_g

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64bits.bend:354

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/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW

354# a pattern with the fraction and exponent of x and sign s is encode(s, ...)
355def enc_g(+l: U32, +h: U32, +s: Bool, +y: U32, +hy: {v(y) == Nat.add(C.low(20n, v(h)), C.shift(20n, Nat.add(C.low(11n, C.high(20n, v(h))), C.shift(11n, SF.b2n(s))))) : Nat}) -> {F.Bits{l, y} == SF.encode(s, SF.efield(F.Bits{l, h}), SF.frac(F.Bits{l, h})) : F.F64}:
356  +f = C.low(20n, v(h))
357  +T = C.shift(20n, Nat.add(C.low(11n, C.high(20n, v(h))), C.shift(11n, SF.b2n(s))))
358  +fr = Nat.add(v(l), C.shift(32n, f))
359  +elo = Equal.trans(U32, U32.from_nat(C.low(32n, fr)), U32.from_nat(v(l)), l, Equal.cong(Nat, U32, z => U32.from_nat(z), C.low(32n, fr), v(l), WW.low_u(32n, v(l), f, LW.vb(l))), LW.rt(l))
360  +ehi0 = Equal.trans(Nat, Nat.add(C.high(32n, fr), T), Nat.add(f, T), v(y), Equal.cong(Nat, Nat, z => Nat.add(z, T), C.high(32n, fr), f, WW.high_u(32n, v(l), f, LW.vb(l))), Equal.sym(Nat, v(y), Nat.add(f, T), hy))
361  +ehi = Equal.trans(U32, U32.from_nat(Nat.add(C.high(32n, fr), T)), U32.from_nat(v(y)), y, Equal.cong(Nat, U32, z => U32.from_nat(z), Nat.add(C.high(32n, fr), T), v(y), ehi0), LW.rt(y))
362  +e = Equal.trans(F.F64, F.Bits{U32.from_nat(C.low(32n, fr)), U32.from_nat(Nat.add(C.high(32n, fr), T))}, F.Bits{l, U32.from_nat(Nat.add(C.high(32n, fr), T))}, F.Bits{l, y}, Equal.cong(U32, F.F64, z => F.Bits{z, U32.from_nat(Nat.add(C.high(32n, fr), T))}, U32.from_nat(C.low(32n, fr)), l, elo), Equal.cong(U32, F.F64, z => F.Bits{l, z}, U32.from_nat(Nat.add(C.high(32n, fr), T)), y, ehi))
363  Equal.sym(F.F64, F.Bits{U32.from_nat(C.low(32n, fr)), U32.from_nat(Nat.add(C.high(32n, fr), T))}, F.Bits{l, y}, e)