Native and arbitrary-precision integer square-root runtime

Bounded integer square root uses an overflow-free average and Newton iteration. In compiled code, sqrtChecked replaces it with a floating-point candidate checked by exact squares. Their Nat.sqrt refinements are proved in IntegerSquareRoot.Proof.

Larger inputs use a checked Newton candidate with increasing precision. The refinement follows CPython 3.13's Modules/mathmodule.c, "Integer square root". A final square certificate supplies the root and remainder, and a rejected candidate falls back to full-precision iteration.

The full-precision integer Newton iteration is Algorithm 1.13 (SqrtInt) in Richard P. Brent and Paul Zimmermann, Modern Computer Arithmetic (2010), §1.5.1.

@[inline]

def FloatLib.Numerics.FixedWord.IntegerSquareRoot.average (left right : UInt64) : UInt64

Floor of the average of two native words, without overflowing their sum.

The low-bit conjunction supplies the carry exactly when both operands are odd.

@[irreducible, inline]

def FloatLib.Numerics.FixedWord.IntegerSquareRoot.sqrtIter (value guess : UInt64) : UInt64

Newton iteration starting from an upper bound on the floor square root.

The result is the floor root only when Nat.sqrt value.toNat ≤ guess.toNat. An undersized guess can come back unchanged, as in sqrtIter 16 1 = 1. The sqrt wrapper supplies a valid initial bound.

@[inline]

def FloatLib.Numerics.FixedWord.IntegerSquareRoot.sqrt (value : UInt64) : UInt64

Integer square root of one native word.

@[inline]

def FloatLib.Numerics.FixedWord.IntegerSquareRoot.isFloorRoot (value guess : UInt64) : Bool

Whether guess is the floor square root of value, decided in word arithmetic that cannot overflow.

@[inline]

def FloatLib.Numerics.FixedWord.IntegerSquareRoot.sqrtChecked (value : UInt64) : UInt64

sqrt through a floating-point candidate. The hardware square root of the rounded value proposes the root, and isFloorRoot accepts it or a neighbour only after an exact square check, so no property of floating-point arithmetic is assumed. Rejected candidates run sqrt. IntegerSquareRoot.Compiler installs this as the compiled implementation of sqrt.

@[irreducible]

def FloatLib.Numerics.FixedWord.IntegerSquareRoot.approxRoot (value precision : ℕ) : ℕ

Approximate a square root from a leading native-word seed and increasing-precision refinements.

The intended precision is value.log2 / 2. The recursive call retains approximately half the root bits, and each return performs one division at the next precision. checkRoot? validates the final candidate, so no correctness assumption on the seed or refinement enters sqrtRem.

def FloatLib.Numerics.FixedWord.IntegerSquareRoot.checkRoot? (value guess : ℕ) : Option (ℕ × ℕ)

Check an integer-root candidate, allowing correction by one.

Only one square is computed. In the lower branch the remainder bound is equivalent to value < (guess + 1)², and in the upper branch (guess - 1)² = guess² - (2 * guess - 1). Every accepted pair is the floor square root with its remainder.

def FloatLib.Numerics.FixedWord.IntegerSquareRoot.sqrtRem (value : ℕ) : ℕ × ℕ

Floor square root and exact remainder, with checked increasing-precision Newton as a candidate.

The fallback spells out Nat.sqrt.iter instead of calling Nat.sqrt, which keeps the global compiler replacement of Nat.sqrt by sqrtNat acyclic.

@[inline]

def FloatLib.Numerics.FixedWord.IntegerSquareRoot.sqrtNat (value : ℕ) : ℕ

Use native-word square root below 2^64 and checked increasing-precision Newton above it.

The arbitrary-precision branch computes the remainder anyway while certifying the root, so callers that need both can call sqrtRem.