Square-root specification

The reference operation is descriptor-aware for every validated FloatFormat. The model bridge below is intentionally restricted to conventional IEEE descriptors.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Spec.sqrt {fmt : FloatFormat} (x : Model fmt) : Model fmt

Descriptor-aware square root rounded to nearest with ties to even.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Spec.sqrt_eq_model {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (x : Model fmt) (hfinite : x.isFinite = true) (hnonzero : x.isZero = false) (hnonnegative : x.signBit = false) : sqrt x = ofModel fmt (Float.Model.UnpackedFloat.sqrt fmt.toModel x.toModel)

For a positive finite conventional-IEEE value, the descriptor-aware square root agrees with the established unpacked-model result used by the binary32 and binary64 refinements.