Executable exact-intermediate finite arithmetic

Storage and accumulation may use different precisions. For example, mulAddFinite? can read FP8 operands and accumulate their product in FP32. These operations separate the exact intermediate calculation from destination rounding:

• inputs are decoded to exact dyadics;
• addition and multiplication occur in the exact integer intermediate;
• the result is rounded once into the selected destination format and policy.

The checked operations return Option. none means that an input was NaN or infinity, or that division encountered a zero denominator. A successful result can still overflow according to the selected output policy. This avoids inventing arithmetic rules for storage formats whose standards specify encodings and conversions but no standalone arithmetic. A hardware-specific layer can add its documented exceptional-value behavior and prove refinement to these finite paths.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.mulDyadic (x y : Numerics.Dyadic) : Numerics.Dyadic

Exact dyadic product used before destination-format rounding.

def FloatLib.Floats.Formats.BinaryInterchange.Model.addFinite? (fmt : FloatFormat) (policy : Numerics.QuantizationPolicy) (entropy : ℕ) (x y : Model fmt) : Option (Model fmt)

Add two finite values exactly and round once into their common format.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.subFinite? (fmt : FloatFormat) (policy : Numerics.QuantizationPolicy) (entropy : ℕ) (x y : Model fmt) : Option (Model fmt)

Subtract two finite values exactly and round once into their common format.

def FloatLib.Floats.Formats.BinaryInterchange.Model.mulFiniteSpec? (fmt : FloatFormat) (policy : Numerics.QuantizationPolicy) (entropy : ℕ) (x y : Model fmt) : Option (Model fmt)

Logical specification of finite multiplication.

Compiled format-specific dispatchers may replace the public entry point, but tables and proofs use this definition directly so their initialization cannot recurse through the compiled dispatcher.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.mulFiniteImpl? (fmt : FloatFormat) (policy : Numerics.QuantizationPolicy) (entropy : ℕ) (x y : Model fmt) : Option (Model fmt)

Compiled finite multiplication.

Nearest-even finite multiplication reuses the canonical Model.mul, including its native word and exhaustive tiny-table backends. Every other policy retains the generic exact dyadic implementation.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.mulFinite? (fmt : FloatFormat) (policy : Numerics.QuantizationPolicy) (entropy : ℕ) (x y : Model fmt) : Option (Model fmt)

Multiply two finite values exactly and round once into their common format.

@[csimp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.mulFinite_eq_mulFiniteImpl : mulFinite? = mulFiniteImpl?

The compiled nearest-even finite path is extensionally equal to generic exact multiplication.

This theorem installs the canonical operation in generated code while proofs continue to unfold mulFinite? to the format-independent policy specification.

def FloatLib.Floats.Formats.BinaryInterchange.Model.fmaFinite? (fmt : FloatFormat) (policy : Numerics.QuantizationPolicy) (entropy : ℕ) (x y z : Model fmt) : Option (Model fmt)

Exact finite x * y + z, followed by one rounding step.

def FloatLib.Floats.Formats.BinaryInterchange.Model.divFinite? (fmt : FloatFormat) (policy : Numerics.QuantizationPolicy) (entropy : ℕ) (x y : Model fmt) : Option (Model fmt)

Divide two finite values and round the exact rational quotient once.

def FloatLib.Floats.Formats.BinaryInterchange.Model.mulAddFinite? (storage accumulator : FloatFormat) (policy : Numerics.QuantizationPolicy) (entropy : ℕ) (x y : Model storage) (acc : Model accumulator) : Option (Model accumulator)

Fused multiply-add from one storage format into a potentially wider accumulator format.

For example, x and y may be FP8 while acc is BF16, FP16, FP32, or a custom wider format. There is no intermediate rounding of the product.