def hwv

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

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/proofs/lib/logic.bend as L
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/u32laws.bend as LW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD

352# the high word of packToF64's addend: 2^31 s + 2^20 e
353def hwv(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +e: Nat, +he: {C.fits(11n, e) == True{} : Bool}, +c31: U32, +hc31: {c31 == U32{WD.pw(32n, 31n)} : U32}, +c20: U32, +hc20: {c20 == U32{WD.pw(32n, 20n)} : U32}) -> {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)) : Nat}:
354  +efe = LW.vo(e, SH.fits_mono(11n, 32n, e, {==}, he))
355  +ec = FB.pwv(20n, {==}, one, h1, c20, hc20)
356  +ep = Equal.trans(Nat, Nat.mul(v(U32.from_nat(e)), v(c20)), Nat.mul(e, v(c20)), C.shift(20n, e), Equal.cong(Nat, Nat, z => Nat.mul(z, v(c20)), v(U32.from_nat(e)), e, efe), Equal.trans(Nat, Nat.mul(e, v(c20)), Nat.mul(e, C.shift(20n, one)), C.shift(20n, e), Equal.cong(Nat, Nat, z => Nat.mul(e, z), v(c20), C.shift(20n, one), ec), Equal.sym(Nat, C.shift(20n, e), Nat.mul(e, C.shift(20n, one)), WW.shift_mul_one(20n, one, h1, e))))
357  +f31 = L.subst(Nat, z => {C.fits(31n, z) == True{} : Bool}, Nat.add(0n, C.shift(20n, e)), C.shift(20n, e), {==}, WW.limbs_fit(20n, 11n, 0n, e, fz(20n), he))
358  +f32 = SH.fits_mono(31n, 32n, C.shift(20n, e), {==}, f31)
359  +hl = L.subst(Nat, z => {Nat.is_lt(z, C.shift(32n, one)) == True{} : Bool}, C.shift(20n, e), Nat.mul(v(U32.from_nat(e)), v(c20)), Equal.sym(Nat, Nat.mul(v(U32.from_nat(e)), v(c20)), C.shift(20n, e), ep), WW.lt_one(32n, one, h1, C.shift(20n, e), f32))
360  +emm = Equal.trans(Nat, v(U32.mul(U32.from_nat(e), c20)), Nat.mul(v(U32.from_nat(e)), v(c20)), C.shift(20n, e), mulv(one, h1, U32.from_nat(e), c20, hl), ep)
361  +esg = sgv(one, h1, s, c31, hc31)
362  +esum = Equal.trans(Nat, Nat.add(v(SF.pick(U32, s, c31, 0)), v(U32.mul(U32.from_nat(e), c20))), Nat.add(C.shift(31n, SF.b2n(s)), v(U32.mul(U32.from_nat(e), c20))), Nat.add(C.shift(31n, SF.b2n(s)), C.shift(20n, e)), Equal.cong(Nat, Nat, z => Nat.add(z, v(U32.mul(U32.from_nat(e), c20))), v(SF.pick(U32, s, c31, 0)), C.shift(31n, SF.b2n(s)), esg), Equal.cong(Nat, Nat, z => Nat.add(C.shift(31n, SF.b2n(s)), z), v(U32.mul(U32.from_nat(e), c20)), C.shift(20n, e), emm))
363  +f2 = WW.limbs_fit(31n, 1n, C.shift(20n, e), SF.b2n(s), f31, b2n_le(s))
364  +f3 = L.subst(Nat, z => {C.fits(32n, z) == True{} : Bool}, Nat.add(C.shift(20n, e), C.shift(31n, SF.b2n(s))), Nat.add(C.shift(31n, SF.b2n(s)), C.shift(20n, e)), NA.add_comm(C.shift(20n, e), C.shift(31n, SF.b2n(s))), f2)
365  +hl2 = L.subst(Nat, z => {Nat.is_lt(z, C.shift(32n, one)) == True{} : Bool}, Nat.add(C.shift(31n, SF.b2n(s)), C.shift(20n, e)), Nat.add(v(SF.pick(U32, s, c31, 0)), v(U32.mul(U32.from_nat(e), c20))), Equal.sym(Nat, Nat.add(v(SF.pick(U32, s, c31, 0)), v(U32.mul(U32.from_nat(e), c20))), Nat.add(C.shift(31n, SF.b2n(s)), C.shift(20n, e)), esum), WW.lt_one(32n, one, h1, Nat.add(C.shift(31n, SF.b2n(s)), C.shift(20n, e)), f3))
366  Equal.trans(Nat, v(U32.add(SF.pick(U32, s, c31, 0), U32.mul(U32.from_nat(e), c20))), Nat.add(v(SF.pick(U32, s, c31, 0)), v(U32.mul(U32.from_nat(e), c20))), Nat.add(C.shift(31n, SF.b2n(s)), C.shift(20n, e)), FB.addv(one, h1, SF.pick(U32, s, c31, 0), U32.mul(U32.from_nat(e), c20), hl2), esum)