Reference arithmetic with exact dyadic intermediates #

Addition, subtraction, multiplication, and fused multiply-add share one specification method: decode finite operands exactly, compute the dyadic intermediate, and round once to nearest with ties to even. Exceptional operands follow the descriptor's NaN, infinity, overflow, and zero policy. In particular, FMA does not round its product before adding the third operand.

These definitions are the stable proof targets for the dispatched arithmetic kernels. Quotients use the rational specification in Spec.Division; roots use Spec.SquareRoot. Explicit rounding directions and exception-status results belong to their separate operation APIs.

These specifications also execute when a backend declines an operand. The rounding refinement must be imported before they are defined: it replaces the logical rounder's repeated one-bit shifts with bulk integer rounding in their compiled code.

Addition and subtraction #

source

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Spec.add {fmt : FloatFormat} (x y : Model fmt) :

Model fmt

Exact dyadic addition followed by nearest-even rounding in the destination descriptor.

Instances For

source

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Spec.sub {fmt : FloatFormat} (x y : Model fmt) :

Model fmt

Subtraction as addition of the negated right operand.

neg toggles the stored sign bit of every word in a signed-zero format, so a NaN propagated from y is returned with its sign bit flipped relative to y. IEEE 754-2019 Section 6.3 leaves the sign of a NaN result unspecified, so this sign choice is allowed. Callers comparing NaN words bit for bit should not expect sub x y to return y's NaN unchanged. In the finite-unsigned-zero encoding neg leaves the NaN word unchanged, so no flip occurs there. The dispatched Model.sub and its backends are proved equal to this definition, so the convention is shared by every format.

Instances For