def hw_value

bend-collections-laws-math@1.0.0.0 · proofs/math/random/float.bend:94

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/proofs/lib/nat.bend as N
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/u32.bend as U
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/w64sh.bend as SH
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB

94# its value: 2^20 e + (qh mod 2^20), for e < 2^11
95def hw_value(+one: Nat, +h1: {one == 1n : Nat}, +e: Nat, +qh: U32, +he: {Nat.is_lt(e, 2048n) == True{} : Bool}) -> {v(hw(e, qh)) == Nat.add(C.low(20n, v(qh)), C.shift(20n, e)) : Nat}:
96  +a = U32.mul(U32.from_nat(e), 1048576)
97  +b = U32.and(qh, 1048575)
98  +lq = C.low(20n, v(qh))
99  +se = C.shift(20n, e)
100  +ve = U.to_nat_from_nat(e, 11n, {==}, he)
101  +f32 = fits_shift(20n, 12n, e, f12(e, he))
102  +va = Equal.trans(Nat, v(a), C.low(32n, C.shift(20n, v(U32.from_nat(e)))), se, SH.mul_p2(U32.from_nat(e), 20n, {==}),
103    Equal.trans(Nat, C.low(32n, C.shift(20n, v(U32.from_nat(e)))), C.low(32n, se), se, Equal.cong(Nat, Nat, z => C.low(32n, C.shift(20n, z)), v(U32.from_nat(e)), e, ve), WW.low_fit(32n, se, f32)))
104  +vb = FB.andm(qh, 20n, 1048575, {==})
105  +e12 = Equal.trans(Nat, Nat.add(v(a), v(b)), Nat.add(se, v(b)), Nat.add(se, lq), Equal.cong(Nat, Nat, z => Nat.add(z, v(b)), v(a), se, va), Equal.cong(Nat, Nat, z => Nat.add(se, z), v(b), lq, vb))
106  +e13 = Equal.trans(Nat, Nat.add(v(a), v(b)), Nat.add(se, lq), Nat.add(lq, se), e12, N.add_comm(se, lq))
107  +fs3 = WW.limbs_fit(20n, 12n, lq, e, WW.low_fits(20n, v(qh)), f12(e, he))
108  +fs1 = L.subst(Nat, z => {C.fits(32n, z) == True{} : Bool}, Nat.add(lq, se), Nat.add(v(a), v(b)), Equal.sym(Nat, Nat.add(v(a), v(b)), Nat.add(lq, se), e13), fs3)
109  Equal.trans(Nat, v(U32.add(a, b)), Nat.add(v(a), v(b)), Nat.add(lq, se), FB.addv(one, h1, a, b, WW.lt_one(32n, one, h1, Nat.add(v(a), v(b)), fs1)), e13)