TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Posit.Arithmetic.Word.Packed.Quotient.Runtime

Packed native-word Posit division #

Packed operands are decoded directly to sign, significand, and exponent fields. Quotient rounding normalizes them in one word, generates the destination-width quotient prefix with the shared two-limb restoring recurrence, and feeds that exact prefix to the common guard/sticky packer.

The two-limb state is selected by intermediate capacity: a normalized one-word ratio can require one additional quotient digit, while its doubled remainder must never wrap. Significands and restoring-loop state stay in fixed-width carriers; exponents and digit counts use Int and Nat.

source
structure FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedQuotient.NormalizedWords :
Type

One-word significands normalized to a common leading position.

  • numerator : UInt64

    Numerator shifted so its leading bit reaches the common position.

  • denominator : UInt64

    Denominator shifted so its leading bit reaches the common position.

  • numeratorLeading : ℕ

    Leading-bit position of the original numerator.

  • denominatorLeading : ℕ

    Leading-bit position of the original denominator.

Instances For
    source
    @[inline]
    def FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedQuotient.normalizeWords (numerator denominator : UInt64) :
    NormalizedWords

    Normalize two nonzero one-word significands to a common leading position.

    Each shift raises the smaller leading position to the larger one. The result therefore still fits in one word. The original leading positions are retained so the quotient exponent can compensate for the different shifts.

    Instances For
      source
      structure FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedQuotient.Prefix :
      Type

      Exact two-limb quotient prefix consumed by direct Posit rounding.

      • significand : Numerics.FixedWord.UInt128

        Generated quotient bits with every omitted nonzero bit jammed into the low bit.

      • exponent : ℤ

        Dyadic exponent associated with the generated quotient prefix.

      Instances For
        source
        @[inline]
        def FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedQuotient.jamState (state : Numerics.FixedWord.RestoringQuotient.QuotientState Numerics.FixedWord.UInt128) :
        Numerics.FixedWord.UInt128

        Jam a nonzero restoring remainder into the quotient prefix's low bit.

        Instances For
          source
          @[inline]
          def FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedQuotient.quotientPrefixWord (format : Format) (numeratorSignificand : UInt64) (numeratorExponent : ℤ) (denominatorSignificand : UInt64) (denominatorExponent : ℤ) :
          Prefix

          Generate the normalized quotient prefix needed by the destination format.

          Ratios below one consume one extra digit; ratios at least one begin with their known leading one. The policy is identical for every one-word-eligible format and depends only on destination precision.

          Instances For
            source
            @[inline]
            def FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedQuotient.roundPositiveCodeWord (format : Format) (numeratorSignificand : UInt64) (numeratorExponent : ℤ) (denominatorSignificand : UInt64) (denominatorExponent : ℤ) :
            UInt64

            Round a positive quotient directly from native decoded fields.

            Instances For
              source
              @[inline]
              def FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedQuotient.roundPositiveCode (format : Format) (numeratorSignificand : UInt64) (numeratorExponent : ℤ) (denominatorSignificand : UInt64) (denominatorExponent : ℤ) :
              ℕ

              Natural-number view of the native positive quotient code.

              Instances For
                source
                @[inline]
                def FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedQuotient.roundFieldsWord (format : Format) (numeratorNegative : Bool) (numeratorSignificand : UInt64) (numeratorExponent : ℤ) (denominatorNegative : Bool) (denominatorSignificand : UInt64) (denominatorExponent : ℤ) :
                UInt64

                Word-valued signed quotient encoding.

                Instances For
                  source
                  @[inline]
                  def FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedQuotient.roundFields (format : Format) (numeratorNegative : Bool) (numeratorSignificand : UInt64) (numeratorExponent : ℤ) (denominatorNegative : Bool) (denominatorSignificand : UInt64) (denominatorExponent : ℤ) :
                  ℕ

                  Natural-number view of signed decoded-field division.

                  Division by zero emits NaR, zero divided by a finite nonzero value emits zero, and finite signs are handled by the same direct guard/sticky call as the word-valued API.

                  Instances For
                    source
                    @[inline]
                    def FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedQuotient.divWordsCodeValid {format : Format} (heligible : NativeWord.Eligible format) (left right : UInt64) (hleft : left.toNat < format.modulus) (hright : right.toNat < format.modulus) :
                    ℕ

                    Divide two proved-valid packed Posit words.

                    Instances For
                      source
                      @[inline]
                      def FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedQuotient.divWordsCodeWordValid {format : Format} (heligible : NativeWord.Eligible format) (left right : UInt64) (hleft : left.toNat < format.modulus) (hright : right.toNat < format.modulus) :
                      UInt64

                      Divide two proved-valid packed Posit words and retain the result in UInt64.

                      Instances For