TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Posit.Arithmetic.Spec

Exact reference arithmetic for standardized posits #

These operations are the mathematical specifications for executable posit arithmetic. Every finite operand is decoded to an exact Rat. Rational arithmetic is evaluated exactly before one final rounding by the Posit Standard rule; square root uses the boundary comparisons described below.

NaR is never interpreted as infinity. It propagates through the six core operations. Division by zero and square root of a negative finite value produce NaR. Fused multiply-add computes the exact rational expression left * right + addend and rounds only the final result.

Square root is also exact as a rounding decision: roundSqrtRat compares the rational radicand against squared posit boundaries, so an irrational root never passes through an approximate floating-point value.

Executable backends refine these definitions.

References #

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

Exact addition followed by one standardized posit rounding.

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

    Exact subtraction followed by one standardized posit rounding.

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

      Exact multiplication followed by one standardized posit rounding.

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

        Exact division followed by one standardized posit rounding.

        The standard's real-number interpretation has no result for a zero divisor, so the operation returns NaR in that case.

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

          Correctly rounded square root for the standardized real domain.

          NaR and negative finite inputs produce NaR. Zero and positive inputs use exact rational boundary comparisons.

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

            Exact fused multiply-add with a single final standardized rounding.

            Instances For
              source
              @[simp]
              theorem FloatLib.Floats.Formats.Posit.Model.Spec.add_nar_left {format : Format} (right : Model format) :
              add (nar format) right = nar format

              NaR propagates from the left operand of specified addition.

              source
              @[simp]
              theorem FloatLib.Floats.Formats.Posit.Model.Spec.add_nar_right {format : Format} (left : Model format) :
              add left (nar format) = nar format

              NaR propagates from the right operand of specified addition.

              source
              @[simp]
              theorem FloatLib.Floats.Formats.Posit.Model.Spec.sub_nar_left {format : Format} (right : Model format) :
              sub (nar format) right = nar format

              NaR propagates from the left operand of specified subtraction.

              source
              @[simp]
              theorem FloatLib.Floats.Formats.Posit.Model.Spec.sub_nar_right {format : Format} (left : Model format) :
              sub left (nar format) = nar format

              NaR propagates from the right operand of specified subtraction.

              source
              @[simp]
              theorem FloatLib.Floats.Formats.Posit.Model.Spec.mul_nar_left {format : Format} (right : Model format) :
              mul (nar format) right = nar format

              NaR propagates from the left operand of specified multiplication.

              source
              @[simp]
              theorem FloatLib.Floats.Formats.Posit.Model.Spec.mul_nar_right {format : Format} (left : Model format) :
              mul left (nar format) = nar format

              NaR propagates from the right operand of specified multiplication.

              source
              @[simp]
              theorem FloatLib.Floats.Formats.Posit.Model.Spec.div_nar_left {format : Format} (right : Model format) :
              div (nar format) right = nar format

              NaR propagates from the dividend of specified division.

              source
              @[simp]
              theorem FloatLib.Floats.Formats.Posit.Model.Spec.div_nar_right {format : Format} (left : Model format) :
              div left (nar format) = nar format

              NaR propagates from the divisor of specified division.

              source
              @[simp]
              theorem FloatLib.Floats.Formats.Posit.Model.Spec.div_zero_right {format : Format} (left : Model format) :
              div left (zero format) = nar format

              Specified posit division by zero produces NaR.

              source
              @[simp]
              theorem FloatLib.Floats.Formats.Posit.Model.Spec.sqrt_nar {format : Format} :
              sqrt (nar format) = nar format

              The specified square root of NaR is NaR.

              source
              @[simp]
              theorem FloatLib.Floats.Formats.Posit.Model.Spec.sqrt_zero {format : Format} :
              sqrt (zero format) = zero format

              The specified square root preserves the unique posit zero.

              source
              @[simp]
              theorem FloatLib.Floats.Formats.Posit.Model.Spec.fma_nar_left {format : Format} (right addend : Model format) :
              fma (nar format) right addend = nar format

              NaR propagates from the left multiplicand of specified FMA.

              source
              @[simp]
              theorem FloatLib.Floats.Formats.Posit.Model.Spec.fma_nar_right {format : Format} (left addend : Model format) :
              fma left (nar format) addend = nar format

              NaR propagates from the right multiplicand of specified FMA.

              source
              @[simp]
              theorem FloatLib.Floats.Formats.Posit.Model.Spec.fma_nar_addend {format : Format} (left right : Model format) :
              fma left right (nar format) = nar format

              NaR propagates from the addend of specified FMA.