W64.isqrt32_est: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as W64
Lines 455-460 of bend-collections-laws-math@1.0.0.0/src/math/w64.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&start_line=455&end_line=460

import Base

# floor(sqrt(x)) from any estimate r <= 65535: down while r^2 > x, then up
# while (r + 1)^2 <= x. The F32 square root lands within 1, so both loops
# take at most a step or two; the fuel covers any estimate, so the result
# never depends on F32's accuracy.
def isqrt32_est(+x: U32, +r: U32) -> U32:
  isqrt32_fix(x, down32(1n+U32.to_nat(r), x, r, U32.is_lt(x, U32.mul(r, r))))

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=down32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=isqrt32_fix