def main_sqrt
bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64sqrt.bend:268
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64sqrt.bend as W64sqrt
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/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
268def main_sqrt(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +r0: U32, +m: U32, +pm: {m == U32{WD.mask(32n, 16n)} : U32}, +hr0: {Nat.is_le(v(r0), v(m)) == True{} : Bool}) -> {v(up32g(1n+U32.to_nat(U32.sub(m, X.down32(1n+U32.to_nat(r0), x, r0, U32.is_lt(x, U32.mul(r0, r0))))), x, X.down32(1n+U32.to_nat(r0), x, r0, U32.is_lt(x, U32.mul(r0, r0))), up_okg(x, X.down32(1n+U32.to_nat(r0), x, r0, U32.is_lt(x, U32.mul(r0, r0))), m), m)) == M.isqrt(v(x)) : Nat}:
269 main_up(one, h1, x, X.down32(1n+U32.to_nat(r0), x, r0, U32.is_lt(x, U32.mul(r0, r0))), m, pm, dn(1n+v(r0), one, h1, x, r0, N.lt_succ(v(r0)), lt16(one, h1, r0, m, pm, hr0), U32.is_lt(x, U32.mul(r0, r0)), {==}, v(r0), {==}))