Exact rational arithmetic for P3109

The closed operations in Arithmetic evaluate finite operands in Rat, retaining infinities and the report's single NaN. In particular, division by zero returns NaN, including infinity divided by zero. FMA and fused add-add form the complete exact expression before projection.

Each ExecFloat.P3109 operation projects into (target := ...), by default the format of its operands, with (mode := ...) and (saturation := ...) options that default to nearest-even rounding and no saturation request. unary, binary, and ternary apply any exact closed operation to operands of independent descriptors. No IEEE exception flags or floating-point environment are used.

Exact rational intermediates can require large integers when the descriptor has a wide exponent range. This implementation does not promise a fixed workspace bound for arbitrary descriptors.

Reference

IEEE Working Group P3109, Interim Report on Arithmetic Formats for Machine Learning, version 4.0.3 (1 September 2026), §§4.10.1–4.10.8, revision 34f5964. This is an unapproved working-group report, not an approved IEEE standard. https://github.com/P3109/Public/tree/34f5964d9bb2382b2665d15467fc3517b990b308.

def FloatLib.Floats.Formats.P3109.Arithmetic.nan : Numerics.NumericalValue ℚ

The report's single exceptional datum.

def FloatLib.Floats.Formats.P3109.Arithmetic.toRat : Numerics.NumericalValue Numerics.Dyadic → Numerics.NumericalValue ℚ

Exact rational observation of a decoded binary datum.

def FloatLib.Floats.Formats.P3109.Arithmetic.neg : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ

Negation in the report's closed extended domain.

def FloatLib.Floats.Formats.P3109.Arithmetic.abs : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ

Absolute value in the report's closed extended domain.

def FloatLib.Floats.Formats.P3109.Arithmetic.copySign (value sign : Numerics.NumericalValue ℚ) : Numerics.NumericalValue ℚ

Copying a sign treats zero as nonnegative and propagates either NaN operand.

def FloatLib.Floats.Formats.P3109.Arithmetic.add : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ

Exact addition, with the indeterminate result NaN for opposite infinities.

def FloatLib.Floats.Formats.P3109.Arithmetic.sub (left right : Numerics.NumericalValue ℚ) : Numerics.NumericalValue ℚ

Exact subtraction, with no projection of the negated operand.

def FloatLib.Floats.Formats.P3109.Arithmetic.mul : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ

Exact multiplication, with NaN for zero times infinity.

def FloatLib.Floats.Formats.P3109.Arithmetic.div : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ

Exact division, with NaN for every zero denominator and for infinity over infinity.

def FloatLib.Floats.Formats.P3109.Arithmetic.recip (value : Numerics.NumericalValue ℚ) : Numerics.NumericalValue ℚ

Exact reciprocal, before the sole destination projection.

def FloatLib.Floats.Formats.P3109.Arithmetic.fma (left right addend : Numerics.NumericalValue ℚ) : Numerics.NumericalValue ℚ

Exact fused multiply-add, with no intermediate rounding or saturation.

def FloatLib.Floats.Formats.P3109.Arithmetic.faa (left middle right : Numerics.NumericalValue ℚ) : Numerics.NumericalValue ℚ

Exact fused add-add, with no intermediate rounding or saturation.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.toClosedRat {source : Formats.P3109.Format} (value : P3109 source) : Numerics.NumericalValue ℚ

Exact closed rational value of a P3109 operand.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.unary {source : Formats.P3109.Format} (operation : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ) (value : P3109 source) (target : Formats.P3109.Format := source) (mode : Formats.P3109.RoundingMode := Formats.P3109.RoundingMode.nearest) (saturation : Formats.P3109.SaturationMode := Formats.P3109.SaturationMode.none) : P3109 target

Apply an exact unary closed operation and project the result once into target, by default the operand's format, rounding in mode before saturation applies.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.binary {leftFormat rightFormat : Formats.P3109.Format} (operation : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ) (left : P3109 leftFormat) (right : P3109 rightFormat) (target : Formats.P3109.Format := leftFormat) (mode : Formats.P3109.RoundingMode := Formats.P3109.RoundingMode.nearest) (saturation : Formats.P3109.SaturationMode := Formats.P3109.SaturationMode.none) : P3109 target

Apply an exact binary closed operation to both decoded operands, then project once into target, by default the left operand's format.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.ternary {leftFormat rightFormat thirdFormat : Formats.P3109.Format} (operation : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ) (left : P3109 leftFormat) (right : P3109 rightFormat) (third : P3109 thirdFormat) (target : Formats.P3109.Format := leftFormat) (mode : Formats.P3109.RoundingMode := Formats.P3109.RoundingMode.nearest) (saturation : Formats.P3109.SaturationMode := Formats.P3109.SaturationMode.none) : P3109 target

Evaluate a complete exact ternary closed expression, then project once into target, by default the first operand's format.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.neg {format : Formats.P3109.Format} (value : P3109 format) (target : Formats.P3109.Format := format) (mode : Formats.P3109.RoundingMode := Formats.P3109.RoundingMode.nearest) (saturation : Formats.P3109.SaturationMode := Formats.P3109.SaturationMode.none) : P3109 target

Negation followed by one projection, which also covers negative results in unsigned targets.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.abs {format : Formats.P3109.Format} (value : P3109 format) (target : Formats.P3109.Format := format) (mode : Formats.P3109.RoundingMode := Formats.P3109.RoundingMode.nearest) (saturation : Formats.P3109.SaturationMode := Formats.P3109.SaturationMode.none) : P3109 target

Absolute value followed by one projection.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.copySign {format : Formats.P3109.Format} (value sign : P3109 format) (target : Formats.P3109.Format := format) (mode : Formats.P3109.RoundingMode := Formats.P3109.RoundingMode.nearest) (saturation : Formats.P3109.SaturationMode := Formats.P3109.SaturationMode.none) : P3109 target

Copy the sign of sign, propagating either NaN, and project once.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.add {format : Formats.P3109.Format} (left right : P3109 format) (target : Formats.P3109.Format := format) (mode : Formats.P3109.RoundingMode := Formats.P3109.RoundingMode.nearest) (saturation : Formats.P3109.SaturationMode := Formats.P3109.SaturationMode.none) : P3109 target

Add the exact decoded operands and project once.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.sub {format : Formats.P3109.Format} (left right : P3109 format) (target : Formats.P3109.Format := format) (mode : Formats.P3109.RoundingMode := Formats.P3109.RoundingMode.nearest) (saturation : Formats.P3109.SaturationMode := Formats.P3109.SaturationMode.none) : P3109 target

Subtract the exact decoded operands and project once.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.mul {format : Formats.P3109.Format} (left right : P3109 format) (target : Formats.P3109.Format := format) (mode : Formats.P3109.RoundingMode := Formats.P3109.RoundingMode.nearest) (saturation : Formats.P3109.SaturationMode := Formats.P3109.SaturationMode.none) : P3109 target

Multiply the exact decoded operands and project once.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.div {format : Formats.P3109.Format} (left right : P3109 format) (target : Formats.P3109.Format := format) (mode : Formats.P3109.RoundingMode := Formats.P3109.RoundingMode.nearest) (saturation : Formats.P3109.SaturationMode := Formats.P3109.SaturationMode.none) : P3109 target

Divide the exact decoded operands and project once. A zero denominator gives NaN.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.recip {format : Formats.P3109.Format} (value : P3109 format) (target : Formats.P3109.Format := format) (mode : Formats.P3109.RoundingMode := Formats.P3109.RoundingMode.nearest) (saturation : Formats.P3109.SaturationMode := Formats.P3109.SaturationMode.none) : P3109 target

Take the exact reciprocal and project once. Zero gives NaN.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.fma {format : Formats.P3109.Format} (left right addend : P3109 format) (target : Formats.P3109.Format := format) (mode : Formats.P3109.RoundingMode := Formats.P3109.RoundingMode.nearest) (saturation : Formats.P3109.SaturationMode := Formats.P3109.SaturationMode.none) : P3109 target

Fused multiply-add: the exact left * right + addend, projected once.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.faa {format : Formats.P3109.Format} (left middle right : P3109 format) (target : Formats.P3109.Format := format) (mode : Formats.P3109.RoundingMode := Formats.P3109.RoundingMode.nearest) (saturation : Formats.P3109.SaturationMode := Formats.P3109.SaturationMode.none) : P3109 target

Fused add-add: the exact left + middle + right, projected once.