def isqrt32_value

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64sqrt.bend:275

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M

275# Isqrt32.value: floor(sqrt(x)) for every U32, whatever the F32 estimate is
276def isqrt32_value(+x: U32) -> SW.Isqrt32.value(x):
277  +r0 = U32.min(F32.to_u32(F32.sqrt(U32.to_f32(x))), 65535)
278  +rd = X.down32(1n+U32.to_nat(r0), x, r0, U32.is_lt(x, U32.mul(r0, r0)))
279  %Equal.sym(U32, X.up32(1n+U32.to_nat(U32.sub(65535, rd)), x, rd, X.up_ok(x, rd)), up32g(1n+U32.to_nat(U32.sub(65535, rd)), x, rd, X.up_ok(x, rd), 65535), impl_up(1n+U32.to_nat(U32.sub(65535, rd)), x, rd, X.up_ok(x, rd))) : {U32.to_nat(_) == M.isqrt(U32.to_nat(x)) : Nat}
280  main_est(1n, {==}, x, F32.to_u32(F32.sqrt(U32.to_f32(x))), 65535, {==})