TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Posit.Arithmetic.Dyadic.Direct.Runtime

Direct arbitrary-width exact-dyadic posit arithmetic #

Direct posit arithmetic combines shared exact-dyadic operand decoding and integer arithmetic with construction of the standard regime/exponent/fraction stream. It is the width-generic executable tier used after fixed packed storage ends.

Division uses a destination-width quotient prefix, one exact remainder test, and direct guard/sticky packing. Square root uses one destination-width integer-root prefix and one exact square-remainder sticky bit. Refinement theorems live in Direct.Proof.

source
@[noinline]
def FloatLib.Floats.Formats.Posit.Model.DirectDyadicArithmetic.add {format : Format} (left right : Model format) :
Model format

Exact dyadic addition followed by certified direct result packing.

Instances For
    source
    @[noinline]
    def FloatLib.Floats.Formats.Posit.Model.DirectDyadicArithmetic.sub {format : Format} (left right : Model format) :
    Model format

    Exact dyadic subtraction followed by certified direct result packing.

    Instances For
      source
      @[noinline]
      def FloatLib.Floats.Formats.Posit.Model.DirectDyadicArithmetic.mul {format : Format} (left right : Model format) :
      Model format

      Exact integer multiplication followed by certified direct result packing.

      Instances For
        source
        @[inline]
        def FloatLib.Floats.Formats.Posit.Model.DirectDyadicArithmetic.divDecoded (format : Format) (numerator denominator : Option Numerics.Dyadic) :
        Model format

        Apply the shared quotient-prefix kernel to two already-decoded operands.

        Keeping exceptional-value dispatch at this boundary lets every storage representation reuse the same division implementation after supplying its proved decoder.

        Instances For
          source
          @[noinline]
          def FloatLib.Floats.Formats.Posit.Model.DirectDyadicArithmetic.div {format : Format} (left right : Model format) :
          Model format

          Correctly rounded division using one destination-width quotient prefix and exact remainder rounding.

          Instances For
            source
            @[noinline]
            def FloatLib.Floats.Formats.Posit.Model.DirectDyadicArithmetic.sqrt {format : Format} (value : Model format) :
            Model format

            Correctly rounded square root using one integer-root prefix and exact sticky bit.

            Instances For
              source
              @[noinline]
              def FloatLib.Floats.Formats.Posit.Model.DirectDyadicArithmetic.fma {format : Format} (left right addend : Model format) :
              Model format

              Exact fused multiply-add with one certified direct final packing step.

              Instances For