def cs_g

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

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/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

394def cs_g(+one: Nat, +h1: {one == 1n : Nat}, +l: U32, +h: U32, +l2: U32, +h2: U32, +m31: U32, +hm31: {m31 == U32{WD.mask(32n, 31n)} : U32}, +c: U32, +hc: {c == U32{WD.pw(32n, 31n)} : U32}) -> {F.Bits{l, U32.add(U32.and(h, m31), U32.and(h2, c))} == SF.encode(SF.sign(F.Bits{l2, h2}), SF.efield(F.Bits{l, h}), SF.frac(F.Bits{l, h})) : F.F64}:
395  +H = v(h)
396  +f = C.low(20n, H)
397  +E = C.low(11n, C.high(20n, H))
398  +c2 = C.high(31n, v(h2))
399  +a = U32.and(h, m31)
400  +b = U32.and(h2, c)
401  +ea = andm(h, 31n, m31, hm31)
402  +eb = andv(h2, c, hc)
403  +esum = Equal.trans(Nat, Nat.add(v(a), v(b)), Nat.add(C.low(31n, H), v(b)), Nat.add(C.low(31n, H), C.shift(31n, c2)), Equal.cong(Nat, Nat, z => Nat.add(z, v(b)), v(a), C.low(31n, H), ea), Equal.cong(Nat, Nat, z => Nat.add(C.low(31n, H), z), v(b), C.shift(31n, c2), eb))
404  +hfit = WW.limbs_fit(31n, 1n, C.low(31n, H), c2, WW.low_fits(31n, H), half0(h2))
405  +hlt0 = WW.lt_one(32n, one, h1, Nat.add(C.low(31n, H), C.shift(31n, c2)), hfit)
406  +hlt = L.subst(Nat, z => {Nat.is_lt(z, C.shift(32n, one)) == True{} : Bool}, Nat.add(C.low(31n, H), C.shift(31n, c2)), Nat.add(v(a), v(b)), Equal.sym(Nat, Nat.add(v(a), v(b)), Nat.add(C.low(31n, H), C.shift(31n, c2)), esum), hlt0)
407  +e1 = Equal.trans(Nat, v(U32.add(a, b)), Nat.add(v(a), v(b)), Nat.add(C.low(31n, H), C.shift(31n, c2)), addv(one, h1, a, b, hlt), esum)
408  +e2 = Equal.trans(Nat, v(U32.add(a, b)), Nat.add(C.low(31n, H), C.shift(31n, c2)), Nat.add(Nat.add(f, C.shift(20n, E)), C.shift(31n, c2)), e1, Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(31n, c2)), C.low(31n, H), Nat.add(f, C.shift(20n, E)), low_split(20n, 11n, H)))
409  +e3 = Equal.trans(Nat, v(U32.add(a, b)), Nat.add(Nat.add(f, C.shift(20n, E)), C.shift(31n, c2)), Nat.add(f, C.shift(20n, Nat.add(E, C.shift(11n, c2)))), e2, fold(f, E, c2))
410  +e4 = Equal.cong(Nat, Nat, z => Nat.add(f, C.shift(20n, Nat.add(E, C.shift(11n, z)))), c2, SF.b2n(SF.sign(F.Bits{l2, h2})), bit_c(c2, half0(h2)))
411  enc_g(l, h, SF.sign(F.Bits{l2, h2}), U32.add(a, b), Equal.trans(Nat, v(U32.add(a, b)), Nat.add(f, C.shift(20n, Nat.add(E, C.shift(11n, c2)))), Nat.add(f, C.shift(20n, Nat.add(E, C.shift(11n, SF.b2n(SF.sign(F.Bits{l2, h2})))))), e3, e4))