def isqrt
import bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend as Naturalimport Base
import bend-collections-laws-crypto@1.0.0.0/src/math/pow2.bend as P2
232def isqrt(+n: Nat) -> Nat:
233 isqrt_from(n, P2.pow2t(1n+Nat.div(bit_length(n), 2n)))
Uses (5)
Used by (15)
- bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/sqrtn:isqrt_le
- bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/sqrtn:lt_succ_isqrt
- bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64sqrt:is_isqrt
- bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64sqrt:isqrt32_value
- bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64sqrt:main_est
- …