Two-word square-root runtime

The proved restoring loop computes the exact floor square root and remainder for a positive normal input of any eligible two-word layout whose fraction has at most 124 bits and whose bias exceeds the fraction width. Correctness proofs live in Sqrt.Proof.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.alignSqrtRadicand (mantissa : Numerics.FixedWord.UInt128) (shift : ℕ) : Numerics.FixedWord.UInt256

Shift a normal significand by shift bits into four words.

@[specialize #[0]]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.sqrtNormal? {fmt : FloatFormat} (x : Model fmt) : Option (Model fmt)

Try the fixed-word square root for one positive normal value.

The radicand is the significand shifted by fracWidth or fracWidth + 1 bits, chosen so that the result exponent is integral, and the root is extracted with fracWidth + 1 base-four digits. The kernel declines formats whose fraction exceeds 124 bits, outside the proved bound on the two-word remainder state, and formats whose bias is at most the fraction width, outside the hypotheses of the exponent lemmas in SqrtArithmetic. The dispatcher handles these cases. Descriptor specialization follows the pattern described in Dispatch.Add.Runtime.