Wide-limb square-root runtime

Positive normal inputs are decoded from their stored limbs. Their significands are scaled by fracWidth or fracWidth + 1 bits and passed to a checked increasing-precision integer square root. The exact remainder determines rounding, including carry into the exponent.

The normal path has no fraction-width bound and does not require the bias to exceed the precision. Zero, subnormal, negative, and exceptional inputs use the reference operation. Sqrt.Proof proves equality with that operation on every eligible stored value.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.sqrtMantissa {fmt : FloatFormat} (x : Value fmt) : ℕ

Read the normal significand without allocating a separate array of fraction limbs.

def FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.sqrtNormalValue (fmt : FloatFormat) (exponent mantissa : ℕ) : Value fmt

Square root of normal scalar fields, with remainder rounding and a possible exponent carry.

For the normal-input contract, the scaled radicand has either 2 * fracWidth + 1 or 2 * fracWidth + 2 bits. Its square root therefore needs no discarded integer bits, and the exact remainder is below the rounding midpoint exactly when it is at most the integer root.

def FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.sqrtNormal? (fmt : FloatFormat) (x : Value fmt) : Option (Value fmt)

Try the checked square-root candidate on a positive normal stored value.

def FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.sqrt (fmt : FloatFormat) (x : Value fmt) : Value fmt

Wide-limb square root, with the exact reference operation for declined inputs.