Two-word square-root runtime #
CheckedSquareRoot.rootAndRemainder, which equals the proved restoring loop, computes the 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.
Shift a normal significand by shift bits into four words.
Instances For
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.
Instances For
sqrtNormal? on the storage words of the operand, returning the storage words of an accepted
root. Two-word carriers call this form, and Sqrt.Proof.sqrtNormal?_of_words relates the two.