Executable exact-dyadic posit rounding

Finite posit inputs and the exact results of addition, subtraction, multiplication, and fused multiply-add are dyadic. This module runs the standardized code search using aligned integer comparisons instead of repeatedly materializing normalized rational values.

The search interval, (n + 1)-bit threshold rule, saturation behavior, tie-breaking rule, and whole-word negative symmetry are identical to Model.roundRat. Refinement theorems live in Dyadic.Proof.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.DyadicRounding.nonnegativeDyadicAt (format : Format) (code : ℕ) : Numerics.Dyadic

Exact dyadic value of the posit word with unsigned code code.

For code < format.signMaskNat, the value is nonnegative and finite. In general, ofNatBits first reduces the code modulo the format's modulus. Zero and NaR map to Dyadic.zero; other words decode with their sign.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.DyadicRounding.minPositive (format : Format) : Numerics.Dyadic

Exact smallest positive value in the dyadic comparison domain.

Code 1 has a unit significand and an all-zero regime prefix. Writing that value directly avoids running the width-linear generic decoder for the same format constant on every rounding call.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.DyadicRounding.roundingThreshold (format : Format) (lowerCode : ℕ) : Numerics.Dyadic

Exact (n + 1)-bit standard boundary above a retained n-bit code.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.DyadicRounding.lowerCodeForPositive (format : Format) (target : Numerics.Dyadic) : ℕ

Greatest positive code accepted by exact dyadic comparison.

The shared bisection routine guarantees that the optimized and reference searches have identical control flow once their comparison predicates are related.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.DyadicRounding.chooseNearestCode (target threshold : Numerics.Dyadic) (lower upper : ℕ) : ℕ

Select a retained code by comparing the target with the exact appended-bit threshold.

A three-way comparison aligns the dyadic significands once. Equality selects the even retained code, as required by the standard's tie rule.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.DyadicRounding.roundPositiveCode (format : Format) (target : Numerics.Dyadic) : ℕ

Round a positive exact dyadic value to a nonnegative posit code.

Zero and negative inputs map to zero, making the positive-rounding helper total. Arithmetic callers pass a nonzero magnitude with negative = false.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.DyadicRounding.roundPositive (format : Format) (target : Numerics.Dyadic) : Model format

Pack the nonnegative code selected by roundPositiveCode.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.DyadicRounding.magnitude (value : Numerics.Dyadic) : Numerics.Dyadic

Clear the sign while preserving the exact dyadic magnitude fields.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.DyadicRounding.restoreSignCode (format : Format) (negative : Bool) (positiveCode : ℕ) : ℕ

Restore a result sign directly on a complete posit encoding.

Every nonzero negative posit is the whole-word two's complement of its positive encoding. The explicit zero branch preserves the standard's unique zero. This operation is independent of the runtime carrier and is therefore shared by native-word and fixed-limb backends.

@[noinline]

def FloatLib.Floats.Formats.Posit.Model.DyadicRounding.round (format : Format) (value : Numerics.Dyadic) : Model format

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

The sign stored on an exact dyadic zero is forgotten because the Posit Standard (2022) has one zero encoding.