Native one-word square root for small IEEE formats

A positive finite input is mantissa * 2 ^ (scale - (bias + fracWidth - 1)). Scaling the mantissa to a radicand of 2 * fracWidth + 1 or 2 * fracWidth + 2 bits gives a floor square root with exactly fracWidth + 1 bits, so the root and its remainder fit one machine word. Since a square root is never a midpoint, comparing the remainder with the root decides nearest rounding. This is the binary32 kernel with the format's bias and fraction width as parameters.

Formats whose radicand exceeds one word, or whose bias is too small for every square root to be normal, use the descriptor-generic kernel. Sqrt.Proof has the proofs.

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordSqrt.Eligible (fmt : FloatFormat) : Prop

Formats served by the one-word kernel: one-word IEEE storage, a radicand below 2 ^ 64, and a bias for which the square root of every finite value is normal.

@[instance_reducible, inline]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordSqrt.instDecidableEligible (fmt : FloatFormat) : Decidable (Eligible fmt)

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordSqrt.sqrtPositiveCore (fmt : FloatFormat) (mantissa scale : UInt64) : UInt64

Square root of mantissa * 2 ^ (scale - (bias + fracWidth - 1)) for a nonzero mantissa below 2 ^ (fracWidth + 1) and a scale of a finite value, packed as storage bits.

numerator / 2 is the biased exponent of the root before rounding, and the shift makes the radicand's leading-bit position 2 * fracWidth or 2 * fracWidth + 1, matching its parity.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordSqrt.sqrtPositive {fmt : FloatFormat} (heligible : NativeSmallWord.StorageEligible fmt) (x : Model fmt) (hfinite : x.isFinite = true) (hnonzero : x.isZero = false) (hpositive : x.signBit = false) : Model fmt

Square root of a positive, finite, nonzero value: the one-word kernel for eligible formats and the shared finite kernel otherwise. The evidence is erased by compilation.