Exact-dyadic posit arithmetic

Finite posit values are dyadic. These kernels therefore perform their exact intermediate work on integer significands and binary exponents rather than constructing normalized rational operands. Addition, subtraction, multiplication, division, square root, and fused multiply-add all round once according to the Posit Standard (2022).

The equality proofs against the independent rational specification live in Dyadic.Proof.

@[noinline]

def FloatLib.Floats.Formats.Posit.Model.DyadicArithmetic.add {format : Format} (left right : Model format) : Model format

Exact integer addition followed by standardized posit rounding.

The dyadic operands are aligned at their smaller exponent and added as signed integers. Final threshold comparisons remain in the exact dyadic domain.

@[noinline]

def FloatLib.Floats.Formats.Posit.Model.DyadicArithmetic.sub {format : Format} (left right : Model format) : Model format

Exact integer subtraction followed by standardized posit rounding.

Subtraction shares the exact dyadic alignment kernel with addition and performs no host floating-point computation.

@[noinline]

def FloatLib.Floats.Formats.Posit.Model.DyadicArithmetic.mul {format : Format} (left right : Model format) : Model format

Exact integer multiplication followed by standardized posit rounding.

Compared with Model.Spec.mul, this forms one integer product and converts only that exact result directly with the certified dyadic rounder; it allocates no rational operands.

@[noinline]

def FloatLib.Floats.Formats.Posit.Model.DyadicArithmetic.div {format : Format} (left right : Model format) : Model format

Correctly rounded division through exact dyadic cross-multiplication.

The kernel never constructs a rational quotient. Candidate values and rounding thresholds are multiplied by the positive divisor magnitude and compared directly with the dividend magnitude. Division by zero and every NaR case retain the specification's NaR result.

@[noinline]

def FloatLib.Floats.Formats.Posit.Model.DyadicArithmetic.sqrt {format : Format} (value : Model format) : Model format

Correctly rounded square root through exact dyadic squared comparisons.

The result itself may be irrational, so this kernel never constructs it. Candidate and threshold squares are compared directly with the decoded dyadic radicand.

@[noinline]

def FloatLib.Floats.Formats.Posit.Model.DyadicArithmetic.fma {format : Format} (left right addend : Model format) : Model format

Exact fused multiply-add with one final standardized rounding.

Both multiplication and addition stay in the shared dyadic carrier. The exact result is converted directly after accumulating the addend, preserving the specification's single-rounding semantics.