TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

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

Flattened packed-word exact-dyadic posit arithmetic #

Addition, subtraction, multiplication, and fused multiply-add decode finite posits to exact dyadic fields before one direct rounding step. The logical definitions use Option Dyadic; these kernels pass the decoded fields through continuations instead.

The kernels in this module pass signs, significands, and exponents directly to the format-independent exact field operations, avoiding intermediate input options and dyadic records. Their semantic and compiler-refinement proofs live in FloatLib.Floats.Formats.Posit.Arithmetic.Word.Packed.Dyadic.Proof.

Addition #

source
@[inline]
def FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.addWordsCodeFlat {format : Format} (heligible : NativeWord.Eligible format) (left right : UInt64) :
ℕ

Add packed posit words after eliminating decoded input records.

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

    Add two words whose packed carrier has already proved both encodings valid.

    Instances For

      Subtraction #

      source
      @[inline]
      def FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.subWordsCodeFlat {format : Format} (heligible : NativeWord.Eligible format) (left right : UInt64) :
      ℕ

      Subtract packed posit words after eliminating decoded input records.

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

        Subtract two words whose packed carrier has already proved both encodings valid.

        Instances For

          Multiplication #

          source
          @[inline]
          def FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.mulWordsCodeFlat {format : Format} (heligible : NativeWord.Eligible format) (left right : UInt64) :
          ℕ

          Multiply packed posit words after scalar-field elimination.

          The product is computed with natural-number significands. The fixed-carrier multiplier in Packed.Product is proved equal to this definition.

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

            Multiply two words whose packed carrier has already proved both encodings valid.

            Instances For

              Fused multiply-add #

              source
              @[inline]
              def FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.fmaWordsCodeFlat {format : Format} (heligible : NativeWord.Eligible format) (left right addend : UInt64) :
              ℕ

              Fuse a packed-word product and addend through scalar exact fields.

              Dyadic.fmaFields forms the exact product and sum before the sole call to the posit rounder.

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

                FMA for three words whose packed carrier has proved every encoding valid.

                Instances For