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.

The kernel is selected by intermediate capacity, not by a particular named Posit format. 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 use the two-limb primitives directly. Addition drops the carry out of the second limb and the successor wraps; 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.

          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