Native floating point to signed integers

Lean defines the signed native casts through its logical floating-point models. 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 truncates FloatLib's exact finite value toward zero. Infinities map to the caller's lower and upper endpoints, and NaN maps to zero.

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.

It 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 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 (Model.payloadOfNaNField signaling payload fmt.encoding)) negative signaling))

NaN maps to zero natively. The checked failure keeps its sign, signaling class, and diagnostic payload without the quiet bit.

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

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 (ofFloat x).toModel

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 (ofFloat x).toModel

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 (ofFloat x).toModel

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 (ofFloat x).toModel

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 (ofFloat32 x).toModel

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 (ofFloat32 x).toModel

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 (ofFloat32 x).toModel

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 (ofFloat32 x).toModel

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 (ofFloat32 x).toModel

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