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, and 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

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Directed.cast_eq (src dst : FloatFormat) (x : Model src) (mode : IEEERoundingMode) : cast src dst x mode = Model.cast src dst x mode

The directed cast kernel computes cast in every rounding direction.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Status.cast_eq (src dst : FloatFormat) (x : Model src) (mode : IEEERoundingMode) : cast src dst x mode = Model.cast src dst x mode true

The status cast kernel is cast with status := true.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.value_cast (src dst : FloatFormat) (x : Model src) (mode : IEEERoundingMode) : (cast src dst x mode true).value = cast src dst x mode

A cast with status := true delivers the value of the cast in the same direction.

@[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 the identity, signed zero included.

NaN propagation

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.fracField_or_quietBit {fmt : FloatFormat} (b : fmt.ExecWord) : (ofBits (b ||| fmt.quietBit)).fracField = (ofBits b).fracField ||| 2 ^ (fmt.fracWidth - 1)

Setting the quiet bit of a word sets bit fracWidth - 1 of its fraction field.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.expField_or_quietBit {fmt : FloatFormat} (b : fmt.ExecWord) : (ofBits (b ||| fmt.quietBit)).expField = (ofBits b).expField

Setting the quiet bit of a word leaves its exponent field unchanged.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.signBit_or_quietBit {fmt : FloatFormat} (b : fmt.ExecWord) : (ofBits (b ||| fmt.quietBit)).signBit = (ofBits b).signBit

Setting the quiet bit of a word leaves its sign bit unchanged.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.and_quietBit_eq_zero_iff {fmt : FloatFormat} (x : Model fmt) : (x.bits &&& fmt.quietBit == 0) = !x.fracField.testBit (fmt.fracWidth - 1)

The quiet bit of a word is clear exactly when bit fracWidth - 1 of its fraction is clear.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.propagatedNaN_eq_quietNaN {fmt : FloatFormat} (x : Model fmt) (hnan : x.isNaN = true) : propagatedNaN fmt x.signBit x.nanPayload = x.quietNaN

Rebuilding a NaN from its sign and IEEE payload gives the quieted NaN.

This is the same-descriptor case of IEEE 754-2019 §6.2.3, so cast could use propagatedNaN on every NaN. It keeps quietNaN on the same descriptor because that path avoids field packing.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_propagatedNaN (fmt : FloatFormat) (negative : Bool) (payload : ℕ) (h : fmt.encoding ≠ FloatFormat.Encoding.finite) : (propagatedNaN fmt negative payload).isNaN = true

A propagated NaN is a NaN in every destination that has a NaN encoding.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.cast_of_isNaN {src dst : FloatFormat} (x : Model src) (hnan : x.isNaN = true) (mode : IEEERoundingMode := IEEERoundingMode.nearest) : cast src dst x mode = propagatedNaN dst x.signBit x.nanPayload

On a NaN source, cast in any rounding direction is propagatedNaN on the source sign and IEEE payload, for equal and unequal descriptors alike (IEEE 754-2019 §6.2.3).

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.cast_invalid_of_isNaN_of_encoding_finite {src dst : FloatFormat} (x : Model src) (mode : IEEERoundingMode) (hnan : x.isNaN = true) (hdst : dst.encoding = FloatFormat.Encoding.finite) : (cast src dst x mode true).status.invalid = true

Casting a NaN into a destination with no NaN encoding raises invalid in every rounding mode.

Such a destination has no NaN to deliver, so cast returns positive zero and reports the lost NaN through the invalid flag.

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 stays 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 and 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) (mode : IEEERoundingMode := IEEERoundingMode.nearest) : cast src dst x mode = x.widenExact hexp hbias hencoding hfrac

Compatible finite widening preserves the complete field encoding, including signed zero, in every rounding mode.

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) : toReal (cast src dst x) = 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 : isFinite (cast src dst x) = true) : toReal (cast src dst x) = 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_eq_roundAt_of_isIEEE_destination {src dst : FloatFormat} (hdst : dst.isIEEE = true) (x : Model src) (hx : x.isFinite = true) (hxy : isFinite (cast src dst x) = true) : toReal (cast src dst x) = roundAt dst x.toReal

Casting any finite binary descriptor to an IEEE destination performs one nearest-even real rounding, provided the delivered result is finite. The source may use a custom bias or a finite-only encoding.

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 : isFinite (cast src dst x) = true) : toReal (cast src dst x) = 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.

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

A finer destination grid preserves the real value of every finite source descriptor, including finite-only encodings. It needs a finite result because grid inclusion does not bound the destination's upper exponent range.