Native binary64 square-root runtime

Positive finite inputs are scaled to a 105- or 106-bit radicand held in two UInt64 limbs. A checked Newton candidate, or a 53-step restoring loop when the check fails, gives the floor root and remainder in native words. The remainder decides the nearest-even result, and the binary64 exponent and fraction are packed without building a generic unpacked-float model.

Sqrt.Proof has the proofs and the Nat.sqrt model.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.shiftedRadicand (mantissa : UInt64) (shift : ℕ) : Numerics.FixedWord.UInt128

Shift a binary64 significand into two limbs. Callers supply a positive shift below 128 and a result that fits in 128 bits.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.digitAt (radicand : Numerics.FixedWord.UInt128) (index : ℕ) : UInt64

Read a base-four digit of a two-limb radicand, for an index below 64.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.rootStep (digit : UInt64) (state : Numerics.FixedWord.RestoringRootState UInt64) : Numerics.FixedWord.RestoringRootState UInt64

Consume one base-four digit in the restoring square-root recurrence.

For the binary64 radicands built above, 53 iterations produce a 53-bit floor root, and the remainder and trial divisor fit in one native word.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.rootLoop (radicand : Numerics.FixedWord.UInt128) : ℕ → Numerics.FixedWord.RestoringRootState UInt64 → Numerics.FixedWord.RestoringRootState UInt64

Consume the given number of radicand digits, most significant first.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.rootAndRemainder (mantissa : UInt64) (shift : ℕ) : Numerics.FixedWord.RestoringRootState UInt64

Compute the floor root and exact remainder of a binary64-sized scaled radicand.

Checked Newton root

The restoring loop takes 53 serial steps. rootAndRemainderChecked takes the candidate and exact square check of CheckedSquareRoot instead. Inputs outside the loop's verified range and rejected candidates still run the loop, so the result is rootAndRemainder on every input (rootAndRemainderChecked_eq in Sqrt.Proof).

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.rootAndRemainderChecked (mantissa : UInt64) (shift : ℕ) : Numerics.FixedWord.RestoringRootState UInt64

rootAndRemainder through a checked Newton candidate where the loop's range conditions hold.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.sqrtPositiveFiniteCore (mantissa scale : UInt64) : UInt64

Positive finite binary64 square root of a decoded significand and scale, as a packed word.

For a nonzero significand below 2^53 and a scale at most 2045, the input value is mantissa * 2^(scale - 1074), with the exponent subtraction in Int. Parity chooses a 105- or 106-bit integer radicand. Its square root cannot be a half-integer, so the result rounds down exactly when remainder ≤ root.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.sqrtPositiveFinite (exponent fraction : UInt64) : UInt64

Decode binary64 fields and run the bounded positive-finite square-root kernel.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.sqrt (x : Value) : Value

Native binary64 square root, including IEEE exceptional-value behavior.