TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Format.Storage

Exact-width binary format storage #

Exact-width BitVec representations of layout masks derived from a validated FloatFormat.

The definitions centralize sign, exponent, significand, and payload masks so packing code does not reconstruct them with ad hoc shifts. They describe logical layout only; selection of UInt8, UInt16, UInt32, UInt64, or arbitrary-width storage belongs to the configured execution layer.

source
@[inline]
def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.ofWordNat (fmt : FloatFormat) (n : Nat) :
fmt.ExecWord

Pack a Nat pattern into the format's exact-width storage word.

Instances For
    source
    @[inline]
    def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.expAllOnes (fmt : FloatFormat) :
    fmt.ExecWord

    Exponent all-ones as storage word.

    Instances For
      source
      @[inline]
      def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.fracMask (fmt : FloatFormat) :
      fmt.ExecWord

      Fraction mask as storage word.

      Instances For
        source
        @[inline]
        def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.expMask (fmt : FloatFormat) :
        fmt.ExecWord

        Shifted exponent mask as storage word.

        Instances For
          source
          @[inline]
          def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.signMask (fmt : FloatFormat) :
          fmt.ExecWord

          Sign-bit mask as storage word.

          Instances For
            source
            @[simp]
            theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.signMask_toNat (fmt : FloatFormat) :
            BitVec.toNat fmt.signMask = 2 ^ (fmt.bitWidth - 1)

            The exact-width sign mask decodes to its unique top-bit power of two.

            source
            @[simp]
            theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.signMask_ne_zero (fmt : FloatFormat) :
            fmt.signMask ≠ 0#fmt.bitWidth

            The sign-bit mask is nonzero for every valid format descriptor.

            source
            @[inline]
            def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.quietBit (fmt : FloatFormat) :
            fmt.ExecWord

            Quiet-NaN bit as storage word.

            Instances For