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.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 established unpacked model applied to the original 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 preserves the exact-dyadic specification.

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

The scalar-field square-root entry point preserves 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 its positive finite contract, the optional scalar decoder returns the direct runtime result.

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

The proof-guided runtime entry point computes square root from the exact dyadic represented by its finite input.

@[csimp]

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

Compile positive square root through the scalar decoder.