TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.ExecFloat.Backends.Word.Narrow.Base.Runtime

Native binary32 storage and rounding primitives #

Model FloatFormat.binary32 remains the theorem-facing representation. Narrow-word kernels share a UInt32 view, direct field operations, exact finite decoding, and rounding primitives defined here.

Operation-specific kernels and their refinements live in sibling modules. Keeping this base small prevents representation-only clients from importing the much larger addition and fused-operation proof developments.

References #

source
@[reducible, inline]
abbrev FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.Value :
Type

The generic binary32 carrier.

Instances For
    source
    @[inline]
    def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.toUInt32 (x : Value) :
    UInt32

    View generic binary32 storage as a native word.

    Instances For
      source
      @[inline]
      def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.ofUInt32 (bits : UInt32) :
      Value

      Rewrap a native binary32 word in the generic carrier.

      Instances For

        Native storage operations

        source
        @[inline]
        def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.negate (x : Value) :
        Value

        Toggle the binary32 sign bit without passing through generic BitVec arithmetic.

        Instances For
          source
          @[inline]
          def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.signBit (bits : UInt32) :
          Bool

          Extract the binary32 sign from a native word.

          Instances For
            source
            @[inline]
            def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.expField (bits : UInt32) :
            UInt32

            Extract the binary32 biased exponent from a native word.

            Instances For
              source
              @[inline]
              def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.fracField (bits : UInt32) :
              UInt32

              Extract the binary32 fraction from a native word.

              Instances For
                source
                @[inline]
                def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.toDyadic? (bits : UInt32) :
                Option Numerics.Dyadic

                Decode a finite binary32 native word to the generic exact dyadic representation.

                Instances For
                  source
                  @[inline]
                  def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.mkBits (sign : Bool) (exponent fraction : ℕ) :
                  UInt32

                  Convert natural-number fields to native words, then mask and pack the binary32 fields.

                  Instances For
                    source
                    @[inline]
                    def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.roundDyadic (value : Numerics.Dyadic) :
                    UInt32

                    Round an exact dyadic to a native binary32 word, using nearest-even rounding.

                    Instances For
                      source
                      @[inline]
                      def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.roundRatScaled (sign : Bool) (num den : ℕ) (exponent : ℤ) :
                      UInt32

                      Round the signed magnitude (num / den) * 2^exponent to a native binary32 word; a zero denominator produces canonical NaN.

                      The exact quotient calculations remain format-independent natural-number arithmetic. Only the binary32 thresholds and final field packing are specialized.

                      Instances For