def est_up

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64est.bend:258

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64dm.bend as DM

258# the estimate is never below the quotient: x < (q_est + 1) b
259def est_up(+one: Nat, +h1: {one == 1n : Nat}, +xl: WU.U64, +xh: U32, +bl: U32, +bh: U32, +hz: {U32.is_zero(bh) == False{} : Bool}, +hX: {Nat.is_lt(DM.X96(xl, xh), Nat.mul(C.shift(32n, one), SW.value(WU.U64{bl, bh}))) == True{} : Bool}) -> {Nat.is_lt(DM.X96(xl, xh), Nat.mul(1n+v(X.q_est(xl, xh, WU.U64{bl, bh}, X.bitlen(bh))), SW.value(WU.U64{bl, bh}))) == True{} : Bool}:
260  est_t(one, h1, xl, xh, bl, bh, hz, hX, X.bitlen(bh), {==})