Direct packed-pair posit square-root runtime #
The packed-pair square-root kernel returns posit codes for configured values stored in two
native limbs. Range and semantic refinement proofs live in Sqrt.Proof.
@[noinline]
def
FloatLib.Floats.Formats.Posit.Model.NativeLimbPacked.sqrtCode
{format : Format}
(value : Numerics.FixedWord.UInt128)
:
Decode one packed operand, take its exact rounded square root, and return the result code.