TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Posit.Arithmetic.Limb.Rounding.Runtime

Two-limb posit rounding runtime #

Posit rounding uses the two-limb execution refinement whenever the exact significand fits in UInt128. Wider exact intermediates retain the same field-oriented guard/sticky semantics in the arbitrary-width direct rounder. Selection is by representation capacity rather than named format, and neither branch uses a candidate certificate or search path.

Semantic refinement laws are in Rounding.Proof.

source
@[inline]
def FloatLib.Floats.Formats.Posit.Model.NativeLimbRounding.roundPositiveCode (format : Format) (_heligible : NativeLimb.Eligible format) (target : Numerics.Dyadic) :
ℕ

Round a positive exact dyadic using two limbs when its significand fits.

The outer zero and sign decisions are representation-independent. A significand below 2^128 then stays in two native words through minimum-positive comparison, field packing, guard/sticky inspection, and nearest-even increment. Only a genuinely wider intermediate crosses to the arbitrary-width implementation, which applies the same exact rounding semantics.

Instances For
    source
    @[inline]
    def FloatLib.Floats.Formats.Posit.Model.NativeLimbRounding.roundPositive (format : Format) (heligible : NativeLimb.Eligible format) (target : Numerics.Dyadic) :
    Model format

    Pack the code selected by two-limb positive rounding.

    Instances For
      source
      @[noinline]
      def FloatLib.Floats.Formats.Posit.Model.NativeLimbRounding.round (format : Format) (heligible : NativeLimb.Eligible format) (value : Numerics.Dyadic) :
      Model format

      Round any exact dyadic using unique posit zero and whole-word negative symmetry.

      Instances For
        source
        @[noinline]
        def FloatLib.Floats.Formats.Posit.Model.NativeLimbRounding.roundCodeNat (format : Format) (heligible : NativeLimb.Eligible format) (value : Numerics.Dyadic) :
        ℕ

        Return the complete encoding selected by proved two-limb rounding.

        The result remains a natural number only at the arithmetic boundary. Configured pair storage immediately splits it into two UInt64 limbs, avoiding construction of an exact-width Model.

        Instances For