TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Posit.Arithmetic.Limb.Rounding.GuardSticky.Runtime

Direct guard-and-sticky two-limb Posit rounding #

The shared field-oriented posit rounder is instantiated with the UInt128 carrier. candidateCarrier maps every shared operation to a two-limb primitive, and the generic kernel in GuardStickyCarrier keeps significands and codes in UInt128. Exponents and bit counts use Int and Nat. Only the steps with carrier-specific contracts live here: the exact minimum-positive comparison, the zero test, and exact-width sign restoration.

Intermediate capacity selects the kernel, and no named Posit format is special. Every format whose storage fits two words may use it whenever the exact significand is below 2^128. Wider exact intermediates retain the same field semantics through the arbitrary-width rounder.

source
@[inline]
def FloatLib.Floats.Formats.Posit.Model.NativeLimbRounding.GuardSticky.shiftLeft (value : Numerics.FixedWord.UInt128) (shift : ℕ) :
Numerics.FixedWord.UInt128

Shift left in the two-word bitstream, returning zero at and beyond 128 positions.

Instances For
    source
    @[always_inline]
    def FloatLib.Floats.Formats.Posit.Model.NativeLimbRounding.GuardSticky.hasLowBits (value : Numerics.FixedWord.UInt128) (width : ℕ) :
    Bool

    Whether the discarded low-bit suffix is nonzero.

    Instances For
      source
      @[always_inline]
      def FloatLib.Floats.Formats.Posit.Model.NativeLimbRounding.GuardSticky.isOdd (value : Numerics.FixedWord.UInt128) :
      Bool

      Parity of the packed candidate used to break a midpoint tie.

      Instances For
        source
        @[reducible, inline]
        abbrev FloatLib.Floats.Formats.Posit.Model.NativeLimbRounding.GuardSticky.candidateCarrier :
        GuardStickyCarrier.CandidateCarrier Numerics.FixedWord.UInt128

        Two-limb implementation of the shared candidate carrier.

        The transparent record lets inlined helpers specialize to the two-limb primitives. Addition drops the carry out of the second limb and the successor wraps, but the shared rounder applies both only to values it has bounded.

        Instances For
          source
          @[inline]
          def FloatLib.Floats.Formats.Posit.Model.NativeLimbRounding.GuardSticky.isLessMinPositive (format : Format) (significand : Numerics.FixedWord.UInt128) (exponent : ℤ) :
          Bool

          Test a positive two-limb target against the format's exact minimum-positive value, a power of two, by comparing the exponent of its leading bit.

          Instances For
            source
            @[inline]
            def FloatLib.Floats.Formats.Posit.Model.NativeLimbRounding.GuardSticky.roundPositiveCodeWord (format : Format) (significand : Numerics.FixedWord.UInt128) (exponent : ℤ) :
            Numerics.FixedWord.UInt128

            Round the nonnegative value significand * 2 ^ exponent to its complete unsigned code in two limbs.

            Zero maps to code zero and targets below minPos to code one. Every other target uses the shared normalized rounder at the UInt128 carrier.

            Instances For
              source
              @[inline]
              def FloatLib.Floats.Formats.Posit.Model.NativeLimbRounding.GuardSticky.restoreSignWord (format : Format) (negative : Bool) (positiveCode : Numerics.FixedWord.UInt128) :
              Numerics.FixedWord.UInt128

              Restore a posit sign by exact-width two's complement inside the two-limb carrier.

              Instances For
                source
                @[inline]
                def FloatLib.Floats.Formats.Posit.Model.NativeLimbRounding.GuardSticky.roundCodeWord (format : Format) (negative : Bool) (significand : Numerics.FixedWord.UInt128) (exponent : ℤ) :
                Numerics.FixedWord.UInt128

                Round signed dyadic fields while keeping the significand and result code in two limbs.

                Instances For