def main_est

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

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/natural.bend as M
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD

271# from any estimate e, clamped to m == 2^16 - 1
272def main_est(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +e: U32, +m: U32, +pm: {m == U32{WD.mask(32n, 16n)} : U32}) -> {v(up32g(1n+U32.to_nat(U32.sub(m, X.down32(1n+U32.to_nat(U32.min(e, m)), x, U32.min(e, m), U32.is_lt(x, U32.mul(U32.min(e, m), U32.min(e, m)))))), x, X.down32(1n+U32.to_nat(U32.min(e, m)), x, U32.min(e, m), U32.is_lt(x, U32.mul(U32.min(e, m), U32.min(e, m)))), up_okg(x, X.down32(1n+U32.to_nat(U32.min(e, m)), x, U32.min(e, m), U32.is_lt(x, U32.mul(U32.min(e, m), U32.min(e, m)))), m), m)) == M.isqrt(v(x)) : Nat}:
273  main_sqrt(one, h1, x, U32.min(e, m), m, pm, %Equal.sym(U32, U32.min(e, m), Bool.pick(U32, U32.is_lt(e, m), e, m), min_pick(e, m)) : {Nat.is_le(v(_), v(m)) == True{} : Bool} min_le(e, m, U32.is_lt(e, m), {==}))