TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.IEEE754.Native.Integer.FromInt

Native signed integers to binary floating point #

ofInt_conversion_spec 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 ExecDType.intToFloat at nearest-even rounding.

Lean defines the signed native casts through its logical floating-point models and exposes ofNat, ofInt, Int.toFloat, Int.toFloat32, and named floating-point constants. The proofs here use those signed-cast definitions.

source
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 gives the roundRat result for the integer as a rational.

source
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 complete nearest-even conversion specification. The pack adapter may return the model word or store it in a configured carrier.

source
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

Lean's integer constructor agrees with fixed-width ExecDType.intToFloat at nearest-even.

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

Int8.toFloat agrees with nearest-even ExecDType.intToFloat into binary64.

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

Int16.toFloat agrees with nearest-even ExecDType.intToFloat into binary64.

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

Int32.toFloat agrees with nearest-even ExecDType.intToFloat into binary64.

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

Int64.toFloat agrees with nearest-even ExecDType.intToFloat into binary64.

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

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

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

Int8.toFloat32 agrees with nearest-even ExecDType.intToFloat into binary32.

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

Int16.toFloat32 agrees with nearest-even ExecDType.intToFloat into binary32.

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

Int32.toFloat32 agrees with nearest-even ExecDType.intToFloat into binary32.

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

Int64.toFloat32 agrees with nearest-even ExecDType.intToFloat into binary32.

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

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