Decimal-to-integer numerical and exception contracts

Successful conversions deliver the specified rounded integer. Failure is characterized by non-finiteness or a rounded value outside the destination range. The integer-grid theorems give error and tie guarantees, and the packing theorems show that the checked result survives fixed-width storage exactly.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertToInteger_inRange (destination : IntegerFormat) (mode : RoundingMode) (signalInexact : Bool) (source : Datum) : Numerics.IntegerFormat.InRange destination (convertToInteger destination mode signalInexact source).value

Every delivered integer, including the invalid default, fits in the chosen destination.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertToInteger_invalid_iff (destination : IntegerFormat) (mode : RoundingMode) (signalInexact : Bool) (source : Datum) : (convertToInteger destination mode signalInexact source).status.invalid = true ↔ ¬∃ (value : ℚ), source.toRat? = some value ∧ Numerics.IntegerFormat.InRange destination (roundInteger mode value)

Range is tested after rounding the exact numerical operand.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertToInteger_of_inRange (destination : IntegerFormat) (mode : RoundingMode) (signalInexact : Bool) (source : Datum) (value : ℚ) (hs : source.toRat? = some value) (hr : Numerics.IntegerFormat.InRange destination (roundInteger mode value)) : convertToInteger destination mode signalInexact source = { value := roundInteger mode value, status := { inexact := signalInexact && decide (↑(roundInteger mode value) ≠ value) } }

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertToInteger_value (destination : IntegerFormat) (mode : RoundingMode) (signalInexact : Bool) (source : Datum) (value : ℚ) (hs : source.toRat? = some value) (hv : (convertToInteger destination mode signalInexact source).status.invalid = false) : (convertToInteger destination mode signalInexact source).value = roundInteger mode value

A successful result denotes the rounded integer exactly.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertToInteger_exact (destination : IntegerFormat) (mode : RoundingMode) (signalInexact : Bool) (source : Datum) (value : ℤ) (hs : source.toRat? = some ↑value) (hr : Numerics.IntegerFormat.InRange destination value) : convertToInteger destination mode signalInexact source = { value := value }

An integer representable in both source and destination is unchanged with no flags.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertToInteger_value_independent (destination : IntegerFormat) (mode : RoundingMode) (signalInexact : Bool) (source : Datum) : (convertToInteger destination mode signalInexact source).value = (convertToInteger destination mode false source).value

Suppression of inexact does not affect the delivered integer.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertToInteger_quiet_inexact (destination : IntegerFormat) (mode : RoundingMode) (source : Datum) : (convertToInteger destination mode false source).status.inexact = false

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertToInteger_inexact_iff (destination : IntegerFormat) (mode : RoundingMode) (source : Datum) (value : ℚ) (hs : source.toRat? = some value) (hv : (convertToInteger destination mode true source).status.invalid = false) : (convertToInteger destination mode true source).status.inexact = true ↔ ↑(convertToInteger destination mode true source).value ≠ value

Inexact is precisely a numerical change on a successful exact-variant conversion.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertToInteger_of_invalid (destination : IntegerFormat) (mode : RoundingMode) (signalInexact : Bool) (source : Datum) (hv : (convertToInteger destination mode signalInexact source).status.invalid = true) : convertToInteger destination mode signalInexact source = invalidOutcome

Invalid integer conversion delivers the documented default, with no simultaneous inexact.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertToInteger_range_flags (destination : IntegerFormat) (mode : RoundingMode) (signalInexact : Bool) (source : Datum) : (convertToInteger destination mode signalInexact source).status.overflow = false ∧ (convertToInteger destination mode signalInexact source).status.underflow = false ∧ (convertToInteger destination mode signalInexact source).status.divideByZero = false

Integer destination conversion never raises floating-point range or division exceptions.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertToInteger_error_le_half (destination : IntegerFormat) (mode : RoundingMode) (hm : mode = RoundingMode.nearestEven ∨ mode = RoundingMode.nearestAway) (signalInexact : Bool) (source : Datum) (value : ℚ) (hs : source.toRat? = some value) (hv : (convertToInteger destination mode signalInexact source).status.invalid = false) : |↑(convertToInteger destination mode signalInexact source).value - value| ≤ 1 / 2

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertToInteger_error_lt_one (destination : IntegerFormat) (mode : RoundingMode) (signalInexact : Bool) (source : Datum) (value : ℚ) (hs : source.toRat? = some value) (hv : (convertToInteger destination mode signalInexact source).status.invalid = false) : |↑(convertToInteger destination mode signalInexact source).value - value| < 1

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.le_convertToInteger_towardPositive (destination : IntegerFormat) (signalInexact : Bool) (source : Datum) (value : ℚ) (hs : source.toRat? = some value) (hv : (convertToInteger destination RoundingMode.towardPositive signalInexact source).status.invalid = false) : value ≤ ↑(convertToInteger destination RoundingMode.towardPositive signalInexact source).value

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertToInteger_towardNegative_le (destination : IntegerFormat) (signalInexact : Bool) (source : Datum) (value : ℚ) (hs : source.toRat? = some value) (hv : (convertToInteger destination RoundingMode.towardNegative signalInexact source).status.invalid = false) : ↑(convertToInteger destination RoundingMode.towardNegative signalInexact source).value ≤ value

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.abs_convertToInteger_towardZero_le (destination : IntegerFormat) (signalInexact : Bool) (source : Datum) (value : ℚ) (hs : source.toRat? = some value) (hv : (convertToInteger destination RoundingMode.towardZero signalInexact source).status.invalid = false) : |↑(convertToInteger destination RoundingMode.towardZero signalInexact source).value| ≤ |value|

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertToFixedInt_toInt (width : ℕ) (mode : RoundingMode) (signalInexact : Bool) (source : Datum) : (convertToFixedInt width mode signalInexact source).1.toInt = (convertToInteger (Numerics.IntegerFormat.signed width) mode signalInexact source).value

Fixed-width packing preserves the checked integer, including invalid delivery.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertToUnsigned_toNat (width : ℕ) (mode : RoundingMode) (signalInexact : Bool) (source : Datum) : ↑(convertToUnsigned width mode signalInexact source).1.toNat = (convertToInteger (Numerics.IntegerFormat.unsigned width) mode signalInexact source).value

Unsigned packing preserves the checked integer exactly, including invalid delivery as zero.