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 remain 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; 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 is NaN (unordered); otherwise some Ordering.

Infinities are handled first by sign; finite values are compared through cmpDyadic.

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

True iff compare x y = some .lt (false when unordered / NaN).

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

True on some .lt or some .eq; false for NaN unordered.

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

IEEE minimum: NaNs via chooseNaN2; minimum(-0,+0) = -0.

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

IEEE maximum: NaNs via chooseNaN2; 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.minimumNumber {fmt : FloatFormat} (x y : Model fmt) : Model fmt

IEEE 754-2019 §9.6 minimumNumber.

If exactly one operand is a NaN, quiet or signaling, the other operand is returned; 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 minimumNumberWithStatus in Operations.Runtime, since the value alone carries no status.

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

IEEE 754-2019 §9.6 maximumNumber.

If exactly one operand is a NaN, quiet or signaling, the other operand is returned; 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 maximumNumberWithStatus in Operations.Runtime.