Checked square roots of two-word radicands

approxRoot proposes the floor root of a two-word radicand from a native-word root of its leading bits and one Newton step, the refinement of IntegerSquareRoot.approxRoot. checkRoot? accepts the candidate, or its predecessor, only after an exact two-word square check, so no correctness argument depends on the candidate. rootAndRemainder replaces the restoring loop for radicands below 2 ^ 128 and keeps the loop otherwise. CheckedSqrt.Proof shows it equals the loop on every input.

@[inline]

def FloatLib.Numerics.FixedWord.CheckedSquareRoot.Internal.divTwoStep (value : UInt128) (divisor : UInt64) : UInt64

Quotient of a two-word value by a native divisor, from two native divisions. It is the exact quotient for a value below 2 ^ 96 and a nonzero divisor below 2 ^ 32.

@[inline]

def FloatLib.Numerics.FixedWord.CheckedSquareRoot.approxRoot (radicand : UInt128) : UInt64

Candidate floor root: a native root of the leading 62 or 63 bits and one Newton step, or the native root alone for a one-word radicand.

@[inline]

def FloatLib.Numerics.FixedWord.CheckedSquareRoot.checkRoot? (radicand : UInt128) (guess : UInt64) : Option (RestoringRootState UInt64)

Accept guess, or guess - 1 when guess is one too large, exactly when it is the floor root of radicand, together with the remainder.

@[inline]

def FloatLib.Numerics.FixedWord.CheckedSquareRoot.rootAndRemainder (radicand : UInt256) (steps : ℕ) : RestoringRootState UInt128

RestoringSquareRoot.rootAndRemainder with the checked candidate for radicands below 2 ^ 128. The loop runs for larger radicands, digit counts outside its verified range, and rejected candidates.

Four-word radicands

@[inline]

def FloatLib.Numerics.FixedWord.CheckedSquareRoot.Internal.approxFloat (value : UInt256) : Float

A floating-point approximation of a four-word value from its leading 64 bits.

@[inline]

def FloatLib.Numerics.FixedWord.CheckedSquareRoot.Internal.newtonStepWide (radicand : UInt256) (root : UInt128) : UInt128

One Newton correction r ± |radicand - r^2| / (2 r) with a floating-point quotient.

@[inline]

def FloatLib.Numerics.FixedWord.CheckedSquareRoot.approxRootWide (radicand : UInt256) : UInt128

Candidate floor root of a four-word radicand of at least 2 ^ 128: the floating-point root of the leading 54 or 55 bits, two Newton corrections, and a final unit adjustment with exact squares. The candidate is only a proposal, which acceptRootWide? checks.

@[inline]

def FloatLib.Numerics.FixedWord.CheckedSquareRoot.acceptRootWide? (radicand : UInt256) (guess : UInt128) : Option (RestoringRootState UInt128)

Accept guess exactly when it is the floor root of radicand, together with the remainder: the square is at most the radicand and the remainder is at most twice the root.

@[inline]

def FloatLib.Numerics.FixedWord.CheckedSquareRoot.Internal.rootAndRemainder (radicand : UInt256) (steps : ℕ) : RestoringRootState UInt128

rootAndRemainder with the checked candidate also for radicands of at least 2 ^ 128. It equals rootAndRemainder on every input (Internal.rootAndRemainder_eq), and CheckedSqrt.Compiler installs it in compiled code.