def est_eq

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

import Base
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

210# the estimate est32 of q_est is min(floor(y / d), 2^32 - 1), the clamped
211# div32 quotient
212def est_eq(+y: WU.U64, +d: U32, +hd: {U32.is_zero(d) == False{} : Bool}) -> {X.est32(y, d) == X.q_clamp(X.fst_q(X.div32(y, d))) : U32}:
213  est_eq_n(y, d, hd, v(d), {==})