TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Kernels.FixedWord.Product.Runtime

Fixed-limb product runtime #

Carry-preserving addition and full products operate over one, two, and four native limbs. The explicit UInt256 carrier is large enough for the exact product of two UInt128 values, so the product needs no arbitrary-precision conversion.

Product.Proof shows that each returned value and carry reconstruct the exact natural-number sum or product.

source
structure FloatLib.Numerics.FixedWord.AddResult (α : Type u) :
Type u

A fixed-width addition result together with its unsigned carry.

  • value : α

    Low fixed-width part of the exact sum.

  • carry : UInt64

    Carry above the payload's highest bit, represented as a native word.

Instances For
    source
    def FloatLib.Numerics.FixedWord.instDecidableEqAddResult.decEq {α✝ : Type u_1} [DecidableEq α✝] (x✝ x✝¹ : AddResult α✝) :
    Decidable (x✝ = x✝¹)
    Instances For
      source
      @[instance_reducible]
      instance FloatLib.Numerics.FixedWord.instDecidableEqAddResult {α✝ : Type u_1} [DecidableEq α✝] :
      DecidableEq (AddResult α✝)
      source
      @[instance_reducible]
      instance FloatLib.Numerics.FixedWord.instReprAddResult {α✝ : Type u_1} [Repr α✝] :
      Repr (AddResult α✝)
      source
      def FloatLib.Numerics.FixedWord.instReprAddResult.repr {α✝ : Type u_1} [Repr α✝] :
      AddResult α✝ → ℕ → Std.Format
      Instances For
        source
        @[inline]
        def FloatLib.Numerics.FixedWord.add64 (x y : UInt64) :
        AddResult UInt64

        Add two native words and retain the unsigned carry.

        Instances For
          source
          @[inline]
          def FloatLib.Numerics.FixedWord.addCarry64 (x y carry : UInt64) :
          AddResult UInt64

          Add two words and an incoming carry.

          Instances For
            source
            @[inline]
            def FloatLib.Numerics.FixedWord.add128 (x y : UInt128) :
            AddResult UInt128

            Add two two-word values.

            Instances For
              source
              structure FloatLib.Numerics.FixedWord.UInt256 :
              Type

              A 256-bit unsigned value represented by four native 64-bit limbs.

              • limb3 : UInt64

                Bits 192 through 255.

              • limb2 : UInt64

                Bits 128 through 191.

              • limb1 : UInt64

                Bits 64 through 127.

              • limb0 : UInt64

                Bits 0 through 63.

              Instances For
                source
                def FloatLib.Numerics.FixedWord.instDecidableEqUInt256.decEq (x✝ x✝¹ : UInt256) :
                Decidable (x✝ = x✝¹)
                Instances For
                  source
                  @[instance_reducible]
                  instance FloatLib.Numerics.FixedWord.instDecidableEqUInt256 :
                  DecidableEq UInt256
                  source
                  def FloatLib.Numerics.FixedWord.instReprUInt256.repr :
                  UInt256 → ℕ → Std.Format
                  Instances For
                    source
                    @[instance_reducible]
                    instance FloatLib.Numerics.FixedWord.instReprUInt256 :
                    Repr UInt256
                    source
                    @[inline]
                    def FloatLib.Numerics.FixedWord.UInt256.ofUInt128 (value : UInt128) :
                    UInt256

                    Embed a two-limb unsigned value in the low half of a four-limb carrier.

                    Instances For
                      source
                      @[inline]
                      def FloatLib.Numerics.FixedWord.UInt256.ofUInt128ShiftedLeft (value : UInt128) (shift : ℕ) :
                      UInt256

                      Embed a two-limb value after shifting it left by shift bits, for 64 < shift < 128.

                      The two-word kernels for formats of at most 128 bits align a fracWidth + 1-bit significand by fracWidth or fracWidth + 1 places, so division, fused multiply-add, and square root share this one word shuffle. toNat_ofUInt128ShiftedLeft gives its value under the stated shift bounds; outside them the native shift counts wrap and the result is unspecified.

                      Instances For
                        source
                        @[inline]
                        def FloatLib.Numerics.FixedWord.UInt256.low128 (value : UInt256) :
                        UInt128

                        Return the low two limbs of a four-limb unsigned value.

                        Instances For
                          source
                          def FloatLib.Numerics.FixedWord.UInt256.toNat (value : UInt256) :
                          ℕ

                          Mathematical value of a four-limb unsigned integer.

                          Instances For
                            source
                            @[inline]
                            def FloatLib.Numerics.FixedWord.UInt256.log2 (value : UInt256) :
                            ℕ

                            Position of the most significant set bit, with zero mapped to zero.

                            Instances For
                              source
                              @[inline]
                              def FloatLib.Numerics.FixedWord.add256 (x y : UInt256) :
                              AddResult UInt256

                              Add two four-word values.

                              Instances For
                                source
                                @[inline]
                                def FloatLib.Numerics.FixedWord.mul128 (x y : UInt128) :
                                UInt256

                                Exact native multiplication of two two-limb values.

                                Four mul64 products form the schoolbook product. Each output column is reduced with add64, and the resulting carry count is passed to the next column.

                                Instances For