TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.IEEE754.Native.Model

Packed native floating-point models #

The conversions below connect the descriptor-indexed Model to Lean's packed binary32 and binary64 models. Converting from a native model retains every bit. Converting to one canonicalizes NaN signs and payloads, as required by Lean's packed-value invariant.

Lean 4.33 introduced these logical floating-point models. Lean 4.34 adds public nan and inf constants for Float32, Float, and their packed models, and strengthens the generic format invariant to require at least two exponent bits. These additions let both native widths share the representation and constant proofs below.

The generic representation lemmas imported here separate this normalization from arithmetic refinement. They concern Lean's logical definitions; they add no assumption about native machine instructions and do not select a floating-point backend.

Binary32 #

source
@[inline]
def FloatLib.Floats.Formats.BinaryInterchange.Model.ofFloat32Model (value : Float32.Model) :
Model FloatFormat.binary32

Read the exact canonical word stored by Lean's packed binary32 model.

Instances For
    source
    @[inline]
    def FloatLib.Floats.Formats.BinaryInterchange.Model.toFloat32Model (value : Model FloatFormat.binary32) :
    Float32.Model

    Pack binary32 bits into Lean's model, canonicalizing any NaN sign and payload.

    Instances For
      source
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isModelCanonical_ofFloat32Model (value : Float32.Model) :
      (ofFloat32Model value).IsModelCanonical

      Native packed binary32 always satisfies the generic canonical-word invariant.

      source
      @[simp]
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toModel_ofFloat32Model (value : Float32.Model) :
      (ofFloat32Model value).toModel = value.unpack

      Unpacking the exact native binary32 word agrees with Lean's unpacked interpretation.

      source
      @[simp]
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ofFloat32Model_pack (value : Float.Model.UnpackedFloat) :
      ofFloat32Model (Float32.Model.pack value) = ofModel FloatFormat.binary32 value

      Packing an unpacked value agrees across the binary32 representation boundary.

      source
      @[simp]
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ofFloat32Model_toFloat32Model (value : Model FloatFormat.binary32) :
      ofFloat32Model value.toFloat32Model = value.canonicalizeModel

      Converting to a packed native model and back performs exactly NaN canonicalization.

      source
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ofFloat32Model_injective :
      Function.Injective ofFloat32Model

      Reading the exact binary32 word loses no information from a native packed model.

      source
      @[simp]
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toFloat32Model_ofFloat32Model (value : Float32.Model) :
      (ofFloat32Model value).toFloat32Model = value

      Every native binary32 model round-trips exactly through FloatLib's representation.

      source
      @[simp]
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.unpack_toFloat32Model (value : Model FloatFormat.binary32) :
      value.toFloat32Model.unpack = value.toModel

      Canonicalization does not change the unpacked interpretation of a binary32 conversion.

      source
      @[simp]
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toFloat32Model_ofModel (value : Float.Model.UnpackedFloat) :
      (ofModel FloatFormat.binary32 value).toFloat32Model = Float32.Model.pack value

      Packing already packed model output agrees with the direct binary32 model constructor.

      source
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toFloat32Model_eq_iff (left right : Model FloatFormat.binary32) :
      left.toFloat32Model = right.toFloat32Model ↔ left.toModel = right.toModel

      Equality of packed binary32 conversions is equality of their unpacked interpretations.

      Binary64 #

      source
      @[inline]
      def FloatLib.Floats.Formats.BinaryInterchange.Model.ofFloatModel (value : Float.Model) :
      Model FloatFormat.binary64

      Read the exact canonical word stored by Lean's packed binary64 model.

      Instances For
        source
        @[inline]
        def FloatLib.Floats.Formats.BinaryInterchange.Model.toFloatModel (value : Model FloatFormat.binary64) :
        Float.Model

        Pack binary64 bits into Lean's model, canonicalizing any NaN sign and payload.

        Instances For
          source
          theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isModelCanonical_ofFloatModel (value : Float.Model) :
          (ofFloatModel value).IsModelCanonical

          Native packed binary64 always satisfies the generic canonical-word invariant.

          source
          @[simp]
          theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toModel_ofFloatModel (value : Float.Model) :
          (ofFloatModel value).toModel = value.unpack

          Unpacking the exact native binary64 word agrees with Lean's unpacked interpretation.

          source
          @[simp]
          theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ofFloatModel_pack (value : Float.Model.UnpackedFloat) :
          ofFloatModel (Float.Model.pack value) = ofModel FloatFormat.binary64 value

          Packing an unpacked value agrees across the binary64 representation boundary.

          source
          @[simp]
          theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ofFloatModel_toFloatModel (value : Model FloatFormat.binary64) :
          ofFloatModel value.toFloatModel = value.canonicalizeModel

          Converting to a packed native model and back performs exactly NaN canonicalization.

          source
          theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ofFloatModel_injective :
          Function.Injective ofFloatModel

          Reading the exact binary64 word loses no information from a native packed model.

          source
          @[simp]
          theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toFloatModel_ofFloatModel (value : Float.Model) :
          (ofFloatModel value).toFloatModel = value

          Every native binary64 model round-trips exactly through FloatLib's representation.

          source
          @[simp]
          theorem FloatLib.Floats.Formats.BinaryInterchange.Model.unpack_toFloatModel (value : Model FloatFormat.binary64) :
          value.toFloatModel.unpack = value.toModel

          Canonicalization does not change the unpacked interpretation of a binary64 conversion.

          source
          @[simp]
          theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toFloatModel_ofModel (value : Float.Model.UnpackedFloat) :
          (ofModel FloatFormat.binary64 value).toFloatModel = Float.Model.pack value

          Packing already packed model output agrees with the direct binary64 model constructor.

          source
          theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toFloatModel_eq_iff (left right : Model FloatFormat.binary64) :
          left.toFloatModel = right.toFloatModel ↔ left.toModel = right.toModel

          Equality of packed binary64 conversions is equality of their unpacked interpretations.

          Native constants #

          source
          @[simp]
          theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ofFloat32Model_nan :
          ofFloat32Model Float32.Model.nan = canonicalNaN FloatFormat.binary32

          Lean's binary32 NaN has FloatLib's canonical IEEE quiet-NaN word.

          source
          @[simp]
          theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ofFloatModel_nan :
          ofFloatModel Float.Model.nan = canonicalNaN FloatFormat.binary64

          Lean's binary64 NaN has FloatLib's canonical IEEE quiet-NaN word.

          source
          @[simp]
          theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ofFloat32Model_inf :
          ofFloat32Model Float32.Model.inf = posInf FloatFormat.binary32

          Lean's positive binary32 infinity has the ordinary all-ones-exponent encoding.

          source
          @[simp]
          theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ofFloatModel_inf :
          ofFloatModel Float.Model.inf = posInf FloatFormat.binary64

          Lean's positive binary64 infinity has the ordinary all-ones-exponent encoding.

          source
          @[simp]
          theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toFloat32Model_canonicalNaN :
          (canonicalNaN FloatFormat.binary32).toFloat32Model = Float32.Model.nan

          The binary32 NaN constant converts back to Lean's packed NaN.

          source
          @[simp]
          theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toFloatModel_canonicalNaN :
          (canonicalNaN FloatFormat.binary64).toFloatModel = Float.Model.nan

          The binary64 NaN constant converts back to Lean's packed NaN.

          source
          @[simp]
          theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toFloat32Model_posInf :
          (posInf FloatFormat.binary32).toFloat32Model = Float32.Model.inf

          The binary32 positive-infinity constant converts back to Lean's packed infinity.

          source
          @[simp]
          theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toFloatModel_posInf :
          (posInf FloatFormat.binary64).toFloatModel = Float.Model.inf

          The binary64 positive-infinity constant converts back to Lean's packed infinity.

          source
          theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toModel_ofFloat32Model_nan :
          (ofFloat32Model Float32.nan.toModel).toModel = Float.Model.UnpackedFloat.notANumber

          Lean's native binary32 NaN denotes the unpacked model's single NaN value.

          source
          theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toModel_ofFloatModel_nan :
          (ofFloatModel Float.nan.toModel).toModel = Float.Model.UnpackedFloat.notANumber

          Lean's native binary64 NaN denotes the unpacked model's single NaN value.

          source
          theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toModel_ofFloat32Model_inf :
          (ofFloat32Model Float32.inf.toModel).toModel = Float.Model.UnpackedFloat.infinity Float.Model.UnpackedFloat.Sign.positive

          Lean's native binary32 infinity denotes positive infinity in the unpacked model.

          source
          theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toModel_ofFloatModel_inf :
          (ofFloatModel Float.inf.toModel).toModel = Float.Model.UnpackedFloat.infinity Float.Model.UnpackedFloat.Sign.positive

          Lean's native binary64 infinity denotes positive infinity in the unpacked model.