Executable binary comparisons

Comparison first handles NaNs and signed infinities, then compares finite values through their exact dyadic denotations. This gives every FloatFormat one numerical order without assuming a particular storage width or relying on host floating-point comparison.

NaNs are unordered. The minimum and maximum operations apply their NaN-selection and signed-zero rules around the same comparator. Both the deprecated IEEE 754-2008 minNum/maxNum and the IEEE 754-2019 minimumNumber/maximumNumber operations are provided, and they differ only in how a signaling NaN operand is treated.

def FloatLib.Floats.Formats.BinaryInterchange.Model.compareNonNaN {fmt : FloatFormat} (x y : Model fmt) (hxNaN : x.isNaN = false) (hyNaN : y.isNaN = false) : Ordering

Numerical ordering once both operands are known not to be NaNs.

Infinity is ordered by sign. Every remaining bit pattern is finite, so comparison uses the exact dyadics extracted from those classification proofs.

def FloatLib.Floats.Formats.BinaryInterchange.Model.compare {fmt : FloatFormat} (x y : Model fmt) : Option Ordering

IEEE numerical comparison: none if either operand is a NaN (unordered), otherwise the ordering.

Infinities are ordered first by sign, and finite values are compared through cmpDyadic.

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

Strict IEEE order, compare x y = some .lt. It fails when either operand is a NaN.

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

Weak IEEE order, compare x y is some .lt or some .eq. It fails for a NaN operand.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instDecidableLe {fmt : FloatFormat} (x y : Model fmt) : Decidable (x.le y)

le is decided by the executable comparison.

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

IEEE minimum, with NaNs selected by chooseNaN2 and minimum(-0,+0) = -0.

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

IEEE maximum, with NaNs selected by chooseNaN2 and maximum(-0,+0) = +0.

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

IEEE 754-2008 minNum, deprecated by IEEE 754-2019 in favor of minimumNumber.

A signaling NaN takes priority and propagates as a quiet NaN. Otherwise, a lone quiet NaN is ignored, two quiet NaNs select the left operand after quieting, and two numbers use minimum, including its minNum(-0, +0) = -0 rule.

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

IEEE 754-2008 maxNum, deprecated by IEEE 754-2019 in favor of maximumNumber.

A signaling NaN takes priority and propagates as a quiet NaN. Otherwise, a lone quiet NaN is ignored, two quiet NaNs select the left operand after quieting, and two numbers use maximum, including its maxNum(-0, +0) = +0 rule.

@[inline]

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

Quiet NaN delivered when both operands of minimumNumber or maximumNumber are NaNs.

The signaling operand is preferred, then the left operand, matching chooseNaN2.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Value.minimumNumber {fmt : FloatFormat} (x y : Model fmt) : Model fmt

IEEE 754-2019 §9.6 minimumNumber, the kernel of Model.minimumNumber x y.

If exactly one operand is a NaN, quiet or signaling, the other operand is returned, so a signaling NaN is not propagated. When both operands are NaNs the result is a quiet NaN chosen by bothNaNNumber. On two numbers this is minimum, so minimumNumber(-0, +0) = -0. The invalid signal owed to a signaling operand is reported by Model.minimumNumber x y (status := true) in Operations.Runtime, since the value alone carries no status.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Value.maximumNumber {fmt : FloatFormat} (x y : Model fmt) : Model fmt

IEEE 754-2019 §9.6 maximumNumber, the kernel of Model.maximumNumber x y.

If exactly one operand is a NaN, quiet or signaling, the other operand is returned, so a signaling NaN is not propagated. When both operands are NaNs the result is a quiet NaN chosen by bothNaNNumber. On two numbers this is maximum, so maximumNumber(-0, +0) = +0. The invalid signal owed to a signaling operand is reported by Model.maximumNumber x y (status := true) in Operations.Runtime.