Correctness of native binary32 square root

For positive finite binary32 inputs, including subnormals, exponent parity determines an exact integer radicand. Its floor square root and remainder determine the rounded significand. The proof relates this calculation and final packing to the generic Model square-root kernel.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.sqrt_eq_generic_of_positive_finite (x : Value) (hexponent : Model.expField x ≠ FloatFormat.binary32.expAllOnesNat) (hnonzero : isZero x = false) (hsign : Model.signBit x = false) : ofUInt32 (sqrtPositiveFinite (expField (toUInt32 x)) (fracField (toUInt32 x))) = ofModel FloatFormat.binary32 (Float.Model.UnpackedFloat.sqrt FloatFormat.binary32.toModel (toModel x))

For a positive, finite, nonzero binary32 input the fast square root agrees with the generic kernel.