Correctness of compact finite square root

The executable descriptor-aware square-root kernels live in Sqrt.Runtime. This module proves their agreement with the exact dyadic and unpacked-model specifications and installs the verified compiler substitution.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteSqrt.sqrtGeneral_eq_unscaled (fmt : FloatFormat) (mantissa : ℕ) (exponent : ℤ) : sqrtGeneral fmt mantissa exponent = if (mantissa == 0) = true then posZero fmt else have finalExponent := targetExponent fmt mantissa exponent; have rootExponent := min (exponent.ediv 2) finalExponent; have scaledMantissa := mantissa <<< (exponent - 2 * rootExponent).toNat; have root := scaledMantissa.sqrt; have remainder := scaledMantissa - root * root; Internal.roundDyadic fmt { negative := false, significand := roundRoot root remainder (finalExponent - rootExponent).toNat, exponent := finalExponent }

The scaled kernel sqrtGeneral equals the full-radicand algorithm.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteSqrt.sqrtPositiveDyadic_eq_model_of_ieee {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (x : Model fmt) (value : Numerics.Dyadic) (hdecode : x.toDyadic? = some value) (hsign : value.negative = false) (hmantissa : value.significand ≠ 0) : sqrtPositiveDyadic fmt value.significand value.exponent = ofModel fmt (Float.Model.UnpackedFloat.sqrt fmt.toModel x.toModel)

For a conventional IEEE descriptor, exact-dyadic square root agrees with the unpacked model UnpackedFloat.sqrt applied to the encoded value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteSqrt.sqrtPositive_eq_spec {fmt : FloatFormat} (x : Model fmt) : sqrtPositive? x = match x.toDyadic? with | none => none | some value => if value.negative = true then none else if (value.significand == 0) = true then none else some (sqrtPositiveDyadic fmt value.significand value.exponent)

Compact positive square root agrees with the exact-dyadic specification.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteSqrt.sqrtPositiveRuntime_eq {fmt : FloatFormat} (x : Model fmt) : sqrtPositiveRuntime? x = sqrtPositive? x

Scalar-field square root sqrtPositiveRuntime? agrees with sqrtPositive?.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteSqrt.sqrtPositiveRuntime_eq_some {fmt : FloatFormat} (x : Model fmt) (hfinite : x.isFinite = true) (hnonzero : x.isZero = false) (hpositive : x.signBit = false) : sqrtPositiveRuntime? x = some (sqrtPositiveRuntime x hfinite hnonzero hpositive)

On a positive finite nonzero input, the optional scalar decoder returns sqrtPositiveRuntime.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteSqrt.sqrtPositiveRuntime_eq_finiteDyadic {fmt : FloatFormat} (x : Model fmt) (hfinite : x.isFinite = true) (hnonzero : x.isZero = false) (hpositive : x.signBit = false) : sqrtPositiveRuntime x hfinite hnonzero hpositive = have value := x.finiteDyadic hfinite; sqrtPositiveDyadic fmt value.significand value.exponent

sqrtPositiveRuntime takes the square root of the exact dyadic that its finite input represents.

@[csimp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteSqrt.sqrtPositive_eq_sqrtPositiveRuntime : @sqrtPositive? = @sqrtPositiveRuntime?

Compile positive square root through the scalar decoder.