Correctness of binary format casts

A finite cast decodes the source exactly and applies one nearest-even rounding step in the destination format. The real-valued rounding bridge assumes conventional IEEE descriptors and a finite result; it does not assign a real value to an infinity or NaN.

References

• IEEE Standard for Floating-Point Arithmetic, IEEE 754-2019, Section 5.4.2. https://doi.org/10.1109/IEEESTD.2019.8766229
• S. Boldo and G. Melquiond, "Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq," 2011. https://doi.org/10.1109/ARITH.2011.40

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.castWithRounding_nearestEven (src dst : FloatFormat) (x : Model src) : castWithRounding src dst x = cast src dst x

The ordinary cast is the nearest-even specialization of the directed cast.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.castWithStatus_value (src dst : FloatFormat) (x : Model src) (mode : IEEERoundingMode) : (castWithStatus src dst x mode).value = castWithRounding src dst x mode

Status-bearing conversion preserves the value selected by the directed cast.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.cast_self_of_finite {fmt : FloatFormat} (x : Model fmt) (hx : x.isFinite = true) : cast fmt fmt x = x

Casting a finite value to its own format is an exact identity, including signed zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.signBit_widenExact {src dst : FloatFormat} (x : Model src) (hexp : src.expWidth = dst.expWidth) (hbias : src.exponentBias = dst.exponentBias) (hencoding : src.encoding = dst.encoding) (hfrac : src.fracWidth ≤ dst.fracWidth) : (x.widenExact hexp hbias hencoding hfrac).signBit = x.signBit

Exact widening preserves the sign bit.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.expField_widenExact {src dst : FloatFormat} (x : Model src) (hexp : src.expWidth = dst.expWidth) (hbias : src.exponentBias = dst.exponentBias) (hencoding : src.encoding = dst.encoding) (hfrac : src.fracWidth ≤ dst.fracWidth) : (x.widenExact hexp hbias hencoding hfrac).expField = x.expField

Exact widening preserves the biased exponent field.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.fracField_widenExact {src dst : FloatFormat} (x : Model src) (hexp : src.expWidth = dst.expWidth) (hbias : src.exponentBias = dst.exponentBias) (hencoding : src.encoding = dst.encoding) (hfrac : src.fracWidth ≤ dst.fracWidth) : (x.widenExact hexp hbias hencoding hfrac).fracField = x.fracField.shiftLeft (dst.fracWidth - src.fracWidth)

Exact widening shifts the stored fraction into the high end of the destination field.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_widenExact {src dst : FloatFormat} (x : Model src) (hexp : src.expWidth = dst.expWidth) (hbias : src.exponentBias = dst.exponentBias) (hencoding : src.encoding = dst.encoding) (hfrac : src.fracWidth ≤ dst.fracWidth) (hx : x.isFinite = true) : (x.widenExact hexp hbias hencoding hfrac).isFinite = true

A finite value remains finite under exact widening.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_widenExact {src dst : FloatFormat} (x : Model src) (hexp : src.expWidth = dst.expWidth) (hbias : src.exponentBias = dst.exponentBias) (hencoding : src.encoding = dst.encoding) (hfrac : src.fracWidth ≤ dst.fracWidth) (hx : x.isFinite = true) : (x.widenExact hexp hbias hencoding hfrac).toReal = x.toReal

Exact same-exponent widening preserves the decoded real value.

For a nonzero finite value, widening left-shifts the integer significand by dst.fracWidth - src.fracWidth; the destination scale loses the same number of powers of two, so the represented real number is unchanged.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.fexpOf_le_of_gridExtension {src dst : FloatFormat} (hfrac : src.fracWidth ≤ dst.fracWidth) (hmin : dst.minSubnormalExponent ≤ src.minSubnormalExponent) (e : ℤ) : fexpOf dst e ≤ fexpOf src e

A destination with at least as many fraction bits and no larger minimum subnormal exponent has a finer dyadic grid. This grid has no upper exponent bound.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.genericFormat_of_gridExtension {src dst : FloatFormat} {r : ℝ} (hfrac : src.fracWidth ≤ dst.fracWidth) (hmin : dst.minSubnormalExponent ≤ src.minSubnormalExponent) (hr : Flocq.genericFormat Numerics.binaryRadix (fexpOf src) r) : Flocq.genericFormat Numerics.binaryRadix (fexpOf dst) r

Representability is preserved by extension to a finer dyadic grid.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.genericFormat_of_compatibleWidening {src dst : FloatFormat} (hbias : src.exponentBias = dst.exponentBias) (hfrac : src.fracWidth ≤ dst.fracWidth) {r : ℝ} (hr : Flocq.genericFormat Numerics.binaryRadix (fexpOf src) r) : Flocq.genericFormat Numerics.binaryRadix (fexpOf dst) r

Equal biases and increased precision preserve the entire rounded-real grid.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.cast_eq_widenExact_of_compatibleWidening {src dst : FloatFormat} (x : Model src) (hexp : src.expWidth = dst.expWidth) (hbias : src.exponentBias = dst.exponentBias) (hencoding : src.encoding = dst.encoding) (hfrac : src.fracWidth ≤ dst.fracWidth) (hx : x.isFinite = true) : cast src dst x = x.widenExact hexp hbias hencoding hfrac

Compatible finite widening preserves the complete field encoding, including signed zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.castWithRounding_eq_widenExact_of_compatibleWidening {src dst : FloatFormat} (x : Model src) (mode : IEEERoundingMode) (hexp : src.expWidth = dst.expWidth) (hbias : src.exponentBias = dst.exponentBias) (hencoding : src.encoding = dst.encoding) (hfrac : src.fracWidth ≤ dst.fracWidth) (hx : x.isFinite = true) : castWithRounding src dst x mode = x.widenExact hexp hbias hencoding hfrac

Every rounding mode uses the same bit-exact compatible finite widening.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.cast_exact_of_compatibleWidening {src dst : FloatFormat} (x : Model src) (hexp : src.expWidth = dst.expWidth) (hbias : src.exponentBias = dst.exponentBias) (hencoding : src.encoding = dst.encoding) (hfrac : src.fracWidth ≤ dst.fracWidth) (hx : x.isFinite = true) : (cast src dst x).toReal = x.toReal

Casting across compatible exponent semantics with at least as much precision is exact.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.cast_eq_roundAt {src dst : FloatFormat} (hsrc : src.isIEEE = true) (hdst : dst.isIEEE = true) (x : Model src) (hx : x.isFinite = true) (hxy : (cast src dst x).isFinite = true) : (cast src dst x).toReal = roundAt dst x.toReal

For conventional IEEE source and destination formats, executable casting refines one nearest-even rounding step in the destination's real-valued model.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.cast_exact_of_gridExtension {src dst : FloatFormat} (x : Model src) (hsrc : src.isIEEE = true) (hdst : dst.isIEEE = true) (hfrac : src.fracWidth ≤ dst.fracWidth) (hmin : dst.minSubnormalExponent ≤ src.minSubnormalExponent) (hx : x.isFinite = true) (hxy : (cast src dst x).isFinite = true) : (cast src dst x).toReal = x.toReal

Conventional IEEE casting into a finer dyadic grid is exact whenever the executable result is finite. This permits a wider exponent field and covers the usual exact standard-format widening conversions.