Native floating point to signed integers

Lean 4.34 gives the signed native casts logical definitions using the floating-point models introduced in Lean 4.33. They truncate toward zero, saturate overflow and infinities, and send NaN to zero. FloatLib's checked conversion reports those exceptional cases as errors.

The shared policy below uses the same exact decoder and integral rounder as the checked conversion. In-range means that the truncated integer is in range: for example, 127.75 converts successfully to the signed eight-bit integer 127.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toInt_toModel_eq {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (x : Model fmt) (lower upper : ℤ) : Float.Model.UnpackedFloat.toInt lower upper x.toModel = match x.exactValue with | ExactValue.finite d => roundDyadicToInt IEEERoundingMode.towardZero d | ExactValue.infinity negative => if negative = true then lower else upper | ExactValue.nan sign signaling payload => 0

Lean's integer conversion reads FloatLib's exact interpretation and truncates its finite dyadic. Infinity endpoints are supplied by the destination; NaN maps to zero before saturation.

def FloatLib.Floats.Formats.BinaryInterchange.ExecDType.floatToIntSaturating {fmt : FloatFormat} (width : ℕ) (x : Model fmt) : Numerics.Representations.FixedInt width

Toward-zero signed conversion with Lean's native exceptional-value policy.

This uses the checked conversion's exact decoder and integral rounder, then saturates finite overflow. Infinities select their signed endpoint and NaN selects zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.ExecDType.floatToIntSaturating_eq_ofIntSaturating_toModel {fmt : FloatFormat} {width : ℕ} (hfmt : fmt.isIEEE = true) (hwidth : 0 < width) (x : Model fmt) : floatToIntSaturating width x = Numerics.Representations.FixedInt.ofIntSaturating (Float.Model.UnpackedFloat.toInt (Numerics.Representations.FixedInt.minValue width) (Numerics.Representations.FixedInt.maxValue width) x.toModel)

The native policy is the existing saturating integer encoder applied to Lean's model result.

theorem FloatLib.Floats.Formats.BinaryInterchange.ExecDType.floatToIntSaturating_of_exactValue_eq_finite_of_inRange {fmt : FloatFormat} {width : ℕ} (x : Model fmt) (d : Numerics.Dyadic) (hvalue : x.exactValue = Model.ExactValue.finite d) (hrange : Numerics.Representations.FixedInt.InRange width (Model.roundDyadicToInt Model.IEEERoundingMode.towardZero d)) : floatToInt x Model.IEEERoundingMode.towardZero = ExecFloat.ConversionOutcome.success (floatToIntSaturating width x) { inexact := !Model.dyadicIsIntegral d }

Checked conversion agrees with native saturation whenever its rounded integer is in range.

theorem FloatLib.Floats.Formats.BinaryInterchange.ExecDType.floatToIntSaturating_of_exactValue_eq_finite_of_real_inRange {fmt : FloatFormat} {width : ℕ} (x : Model fmt) (d : Numerics.Dyadic) (hvalue : x.exactValue = Model.ExactValue.finite d) (hrange : Numerics.Representations.FixedInt.InRange width (if 0 ≤ d.toReal then ⌊d.toReal⌋ else ⌈d.toReal⌉)) : floatToInt x Model.IEEERoundingMode.towardZero = ExecFloat.ConversionOutcome.success (floatToIntSaturating width x) { inexact := !Model.dyadicIsIntegral d }

On an in-range truncated integer, native saturation and the checked API return the same code.

theorem FloatLib.Floats.Formats.BinaryInterchange.ExecDType.floatToIntSaturating_of_exactValue_eq_finite_of_not_inRange {fmt : FloatFormat} {width : ℕ} (x : Model fmt) (d : Numerics.Dyadic) (hvalue : x.exactValue = Model.ExactValue.finite d) (hrange : ¬Numerics.Representations.FixedInt.InRange width (Model.roundDyadicToInt Model.IEEERoundingMode.towardZero d)) : floatToIntSaturating width x = Numerics.Representations.FixedInt.ofIntSaturating (Model.roundDyadicToInt Model.IEEERoundingMode.towardZero d) ∧ floatToInt x Model.IEEERoundingMode.towardZero = ExecFloat.ConversionOutcome.failure ExecFloat.ConversionFailure.outOfRange

Out-of-range finite values saturate natively but are rejected by the checked conversion.

theorem FloatLib.Floats.Formats.BinaryInterchange.ExecDType.floatToIntSaturating_of_exactValue_eq_infinity {fmt : FloatFormat} (width : ℕ) (x : Model fmt) (negative : Bool) (hvalue : x.exactValue = Model.ExactValue.infinity negative) : (floatToIntSaturating width x = if negative = true then Numerics.Representations.FixedInt.minCode width else Numerics.Representations.FixedInt.maxCode width) ∧ floatToInt x Model.IEEERoundingMode.towardZero = ExecFloat.ConversionOutcome.failure (ExecFloat.ConversionFailure.infinity ExecFloat.InputPosition.source negative)

Infinity saturates to its signed endpoint while the checked API reports signed infinity.

theorem FloatLib.Floats.Formats.BinaryInterchange.ExecDType.floatToIntSaturating_of_exactValue_eq_nan {fmt : FloatFormat} (width : ℕ) (x : Model fmt) (negative signaling : Bool) (payload : ℕ) (hvalue : x.exactValue = Model.ExactValue.nan negative signaling payload) : floatToIntSaturating width x = Numerics.Representations.FixedInt.ofInt 0 ∧ floatToInt x Model.IEEERoundingMode.towardZero = ExecFloat.ConversionOutcome.failure (ExecFloat.ConversionFailure.exceptional ExecFloat.InputPosition.source (Numerics.ExceptionalValue.nan (some payload)))

NaN maps to zero natively while the checked API reports its payload.

theorem FloatLib.Floats.ExecFloat.Binary.floatToInt8_eq_floatToIntSaturating (x : Float) : { bits := x.toInt8.toBitVec } = Formats.BinaryInterchange.ExecDType.floatToIntSaturating 8 (toModel (ofFloat x))

Native binary64 to Int8 uses the shared toward-zero, saturation, and NaN-to-zero policy.

theorem FloatLib.Floats.ExecFloat.Binary.floatToInt16_eq_floatToIntSaturating (x : Float) : { bits := x.toInt16.toBitVec } = Formats.BinaryInterchange.ExecDType.floatToIntSaturating 16 (toModel (ofFloat x))

Native binary64 to Int16 uses the shared signed conversion policy.

theorem FloatLib.Floats.ExecFloat.Binary.floatToInt32_eq_floatToIntSaturating (x : Float) : { bits := x.toInt32.toBitVec } = Formats.BinaryInterchange.ExecDType.floatToIntSaturating 32 (toModel (ofFloat x))

Native binary64 to Int32 uses the shared signed conversion policy.

theorem FloatLib.Floats.ExecFloat.Binary.floatToInt64_eq_floatToIntSaturating (x : Float) : { bits := x.toInt64.toBitVec } = Formats.BinaryInterchange.ExecDType.floatToIntSaturating 64 (toModel (ofFloat x))

Native binary64 to Int64 uses the shared signed conversion policy.

theorem FloatLib.Floats.ExecFloat.Binary.floatToISize_eq_floatToIntSaturating (x : Float) : { bits := x.toISize.toBitVec } = Formats.BinaryInterchange.ExecDType.floatToIntSaturating System.Platform.numBits (toModel (ofFloat x))

Native binary64 to ISize saturates to the platform's signed interval.

theorem FloatLib.Floats.ExecFloat.Binary.float32ToInt8_eq_floatToIntSaturating (x : Float32) : { bits := x.toInt8.toBitVec } = Formats.BinaryInterchange.ExecDType.floatToIntSaturating 8 (toModel (ofFloat32 x))

Native binary32 to Int8 uses the shared toward-zero, saturation, and NaN-to-zero policy.

theorem FloatLib.Floats.ExecFloat.Binary.float32ToInt16_eq_floatToIntSaturating (x : Float32) : { bits := x.toInt16.toBitVec } = Formats.BinaryInterchange.ExecDType.floatToIntSaturating 16 (toModel (ofFloat32 x))

Native binary32 to Int16 uses the shared signed conversion policy.

theorem FloatLib.Floats.ExecFloat.Binary.float32ToInt32_eq_floatToIntSaturating (x : Float32) : { bits := x.toInt32.toBitVec } = Formats.BinaryInterchange.ExecDType.floatToIntSaturating 32 (toModel (ofFloat32 x))

Native binary32 to Int32 uses the shared signed conversion policy.

theorem FloatLib.Floats.ExecFloat.Binary.float32ToInt64_eq_floatToIntSaturating (x : Float32) : { bits := x.toInt64.toBitVec } = Formats.BinaryInterchange.ExecDType.floatToIntSaturating 64 (toModel (ofFloat32 x))

Native binary32 to Int64 uses the shared signed conversion policy.

theorem FloatLib.Floats.ExecFloat.Binary.float32ToISize_eq_floatToIntSaturating (x : Float32) : { bits := x.toISize.toBitVec } = Formats.BinaryInterchange.ExecDType.floatToIntSaturating System.Platform.numBits (toModel (ofFloat32 x))

Native binary32 to ISize saturates to the platform's signed interval.