Native signed integers to binary floating point

The shared theorem connects Lean's integer constructor to the complete binary conversion specification, including the selected word and rounding status. Fixed-width native conversions then agree with the existing ExecDType.intToFloat operation at nearest-even rounding.

Lean 4.33 introduced the logical floating-point models. Lean 4.34 connects the signed native casts to those models and exposes ofNat, ofInt, Int.toFloat, Int.toFloat32, and named floating-point constants. The proofs here use the new signed-cast definitions.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ofModel_ofInt_eq_roundRat (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (n : ℤ) : ofModel fmt (Float.Model.UnpackedFloat.ofInt fmt.toModel n) = roundRat fmt (Numerics.SignedRat.ofRat ↑n).negative (↑n).num.natAbs (↑n).den

Lean's integer constructor selects exactly the rational conversion result.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ofInt_conversion_spec {Destination : Type u} (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (pack : Model fmt → Destination) (n : ℤ) : ExecFloat.Binary.Conversion.specWith pack ExecFloat.Binary.Conversion.Context.default (Numerics.NumericalValue.finite (Numerics.SignedRat.ofRat ↑n)) (ExecFloat.ConversionOutcome.success (pack (ofModel fmt (Float.Model.UnpackedFloat.ofInt fmt.toModel n))) (ExecFloat.Binary.Conversion.finiteStatus ExecFloat.Binary.Conversion.Context.default (↑n) (ofModel fmt (Float.Model.UnpackedFloat.ofInt fmt.toModel n))))

Lean's shared integer conversion satisfies the existing complete nearest-even conversion spec. The destination adapter may expose the model word or pack it into a configured carrier.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ofModel_ofInt_eq_intToFloat {width : ℕ} (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (n : Numerics.Representations.FixedInt width) : ofModel fmt (Float.Model.UnpackedFloat.ofInt fmt.toModel n.toInt) = ExecDType.intToFloat fmt n IEEERoundingMode.nearestEven

The core integer constructor agrees with the existing fixed-width conversion operation.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat_int8ToFloat (n : Int8) : toModel (ofFloat n.toFloat) = Formats.BinaryInterchange.ExecDType.intToFloat Formats.BinaryInterchange.FloatFormat.binary64 { bits := n.toBitVec } Formats.BinaryInterchange.Model.IEEERoundingMode.nearestEven

Int8.toFloat is the existing binary64 nearest-even integer conversion.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat_int16ToFloat (n : Int16) : toModel (ofFloat n.toFloat) = Formats.BinaryInterchange.ExecDType.intToFloat Formats.BinaryInterchange.FloatFormat.binary64 { bits := n.toBitVec } Formats.BinaryInterchange.Model.IEEERoundingMode.nearestEven

Int16.toFloat is the existing binary64 nearest-even integer conversion.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat_int32ToFloat (n : Int32) : toModel (ofFloat n.toFloat) = Formats.BinaryInterchange.ExecDType.intToFloat Formats.BinaryInterchange.FloatFormat.binary64 { bits := n.toBitVec } Formats.BinaryInterchange.Model.IEEERoundingMode.nearestEven

Int32.toFloat is the existing binary64 nearest-even integer conversion.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat_int64ToFloat (n : Int64) : toModel (ofFloat n.toFloat) = Formats.BinaryInterchange.ExecDType.intToFloat Formats.BinaryInterchange.FloatFormat.binary64 { bits := n.toBitVec } Formats.BinaryInterchange.Model.IEEERoundingMode.nearestEven

Int64.toFloat is the existing binary64 nearest-even integer conversion.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat_iSizeToFloat (n : ISize) : toModel (ofFloat n.toFloat) = Formats.BinaryInterchange.ExecDType.intToFloat Formats.BinaryInterchange.FloatFormat.binary64 { bits := n.toBitVec } Formats.BinaryInterchange.Model.IEEERoundingMode.nearestEven

ISize.toFloat uses the platform's signed width and binary64 nearest-even rounding.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat32_int8ToFloat32 (n : Int8) : toModel (ofFloat32 n.toFloat32) = Formats.BinaryInterchange.ExecDType.intToFloat Formats.BinaryInterchange.FloatFormat.binary32 { bits := n.toBitVec } Formats.BinaryInterchange.Model.IEEERoundingMode.nearestEven

Int8.toFloat32 is the existing binary32 nearest-even integer conversion.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat32_int16ToFloat32 (n : Int16) : toModel (ofFloat32 n.toFloat32) = Formats.BinaryInterchange.ExecDType.intToFloat Formats.BinaryInterchange.FloatFormat.binary32 { bits := n.toBitVec } Formats.BinaryInterchange.Model.IEEERoundingMode.nearestEven

Int16.toFloat32 is the existing binary32 nearest-even integer conversion.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat32_int32ToFloat32 (n : Int32) : toModel (ofFloat32 n.toFloat32) = Formats.BinaryInterchange.ExecDType.intToFloat Formats.BinaryInterchange.FloatFormat.binary32 { bits := n.toBitVec } Formats.BinaryInterchange.Model.IEEERoundingMode.nearestEven

Int32.toFloat32 is the existing binary32 nearest-even integer conversion.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat32_int64ToFloat32 (n : Int64) : toModel (ofFloat32 n.toFloat32) = Formats.BinaryInterchange.ExecDType.intToFloat Formats.BinaryInterchange.FloatFormat.binary32 { bits := n.toBitVec } Formats.BinaryInterchange.Model.IEEERoundingMode.nearestEven

Int64.toFloat32 is the existing binary32 nearest-even integer conversion.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat32_iSizeToFloat32 (n : ISize) : toModel (ofFloat32 n.toFloat32) = Formats.BinaryInterchange.ExecDType.intToFloat Formats.BinaryInterchange.FloatFormat.binary32 { bits := n.toBitVec } Formats.BinaryInterchange.Model.IEEERoundingMode.nearestEven

ISize.toFloat32 uses the platform's signed width and binary32 nearest-even rounding.