Special-value rules for IEEE32Exec #
IEEE32Exec is the executable, proof-relevant bit-level IEEE-754 binary32 kernel. The operations
are defined by case splits (chooseNaN2/chooseNaN3, Inf rules, then exact+rounded finite core).
We collect the "special-value" part of those definitions as reusable theorems: how NaNs (including payload selection/quieting) and infinities propagate.
These lemmas are fully proved in Lean because they are consequences of the executable definitions
in NN/Floats/IEEEExec/Exec32.lean.
Why keep these lemmas in a separate file?
- The executable definitions in
Exec32.leanare necessarily a bit long: they split on NaN/Inf/0 cases, decode to exact intermediates, and then round back to float32. - In proofs (and in higher-level specs), we usually want to use those definitions without unfolding them over and over. The lemmas here are the small, reliable rewrite rules we reach for.
Binary32 reminder (math we use repeatedly) #
IEEE-754 binary32 is stored as a 32-bit word split into fields:
- 1 sign bit,
- 8 exponent bits,
- 23 fraction ("mantissa") bits.
If we write e for the exponent field and f for the fraction field, then:
xis finite iffe ≠ 255,xis±∞iffe = 255 ∧ f = 0,xis a NaN iffe = 255 ∧ f ≠ 0.
isFinite, isInf, and isNaN in Exec32.lean are just executable versions of those predicates.
Finally, a signaling NaN is a NaN whose fraction's designated “quiet bit” is not set.
Our quietNaN turns any NaN into a quiet NaN by setting that one bit, leaving the exponent field
unchanged.
References (background) #
- IEEE Standard for Floating-Point Arithmetic, IEEE 754-2019.
- David Goldberg, "What Every Computer Scientist Should Know About Floating-Point Arithmetic", ACM Computing Surveys (1991). DOI: 10.1145/103162.103163
- Jean-Michel Muller et al., Handbook of Floating-Point Arithmetic, 2nd ed. (2018).
NaN selection helpers #
Bitfield facts used by special-case lemmas #
Quieting a NaN does not change the exponent field.
Informal: quietNaN only ORs quietBit into the fraction payload; exponent bits are preserved.
A shorter name for expField_quietNaN_eq (keeps the original name stable).
If x is a NaN, then its exponent field is all ones.
A shorter name for expField_eq_expAllOnes_of_isNaN.
If x is an infinity, then its exponent field is all ones.
A shorter name for expField_eq_expAllOnes_of_isInf.
If the exponent field is all ones, the value is not finite (it is either Inf or NaN).
"Choosing a NaN" always yields a non-finite result #
The chooseNaN* helpers return a NaN operand (quieted). This makes it easy to prove that "once a
NaN is selected, the result is not finite" without redoing bitfield reasoning at every call site.
If chooseNaN1 x = some nan, then nan is not finite.
Mathematically: chooseNaN1 only returns some _ when x is a NaN, and in that case it returns
quietNaN x. Quieting sets a fraction bit but keeps the exponent field equal to all ones, so the
result is not finite.
If chooseNaN2 x y = some nan, then nan is not finite.
This is the core invariant behind the op-level facts like
add_eq_of_chooseNaN2_some / mul_eq_of_chooseNaN2_some: once a NaN is selected, we know it is a
NaN value at the bit level (exponent field is all ones), hence not finite.
If chooseNaN3 x y z = some nan, then nan is not finite.
This is the ternary analogue of isFinite_eq_false_of_chooseNaN2_some, used for fma.
NaN selection rules (chooseNaN2 / chooseNaN3) #
These are "one-step" lemmas for the NaN-selection helpers themselves. They let you prove facts
about chooseNaN2/chooseNaN3 without unfolding their nested if chains.
What chooseNaN* does (informal spec) #
Both helpers implement the NaN-propagation part of IEEE-754-style arithmetic:
- If any operand is a signaling NaN (sNaN), return that operand quieted.
- Otherwise, if any operand is a (quiet) NaN, return one of them quieted.
- Otherwise return
none(meaning: "no NaN special-case, continue with Inf/finite rules").
The order is left-to-right: if two operands are both NaNs, we keep the first one. That is not a deep mathematical choice (IEEE leaves payload selection somewhat implementation-defined), but it is useful for reproducibility and it matches the kind of behavior you typically see when running PyTorch models on IEEE hardware (payloads propagate in a deterministic, operand-order-dependent way).
If the left operand is a signaling NaN, chooseNaN2 returns it (quieted).
If the right operand is a signaling NaN (and the left one is not), chooseNaN2 returns it.
If neither operand is a NaN, chooseNaN2 returns none.
If x is a signaling NaN, chooseNaN3 returns it (quieted), regardless of y and z.
If y is a signaling NaN and x is not, chooseNaN3 returns y (quieted).
This is the same precedence rule as chooseNaN2: signaling NaNs win (and get quieted).
Alias for chooseNaN3_of_isSNaN_x (left operand is a signaling NaN).
Alias for chooseNaN3_of_isSNaN_y (middle operand is a signaling NaN).
Alias for chooseNaN3_of_isSNaN_z (right operand is a signaling NaN).
NaN propagation for ops (short-circuit lemmas) #
Every IEEE32Exec op starts by calling chooseNaN*. If a NaN is selected, the definition returns it
immediately. These lemmas expose that "short-circuit" behavior so higher-level proofs can avoid
unfolding the full op definitions.
NaN short-circuit for addition: add x y returns the NaN chosen by chooseNaN2 x y.
NaN short-circuit for multiplication: mul x y returns the NaN chosen by chooseNaN2 x y.
NaN short-circuit for division: div x y returns the NaN chosen by chooseNaN2 x y.
NaN short-circuit for fused multiply-add: fma x y z returns the NaN chosen by chooseNaN3.
NaN short-circuit for square root: sqrt x returns the NaN chosen by chooseNaN1 x.
NaN short-circuit for minimum: propagate NaNs, like torch.minimum.
NaN short-circuit for maximum: propagate NaNs, like torch.maximum.
Invalid operations (canonical NaN) #
Some combinations of infinities and zeros are specified as invalid in IEEE-754 and return a NaN
(while also raising an invalid-operation flag in hardware). In our executable kernel we model the
return value: after confirming there is no NaN operand (i.e. chooseNaN2 = none), we return the
fixed bit-pattern canonicalNaN.
These lemmas expose those branches directly.
(+∞) + (-∞) (or (-∞) + (+∞)) returns canonicalNaN once we know there is no NaN operand.
∞ / ∞ returns canonicalNaN once we know there is no NaN operand.
∞ * 0 returns canonicalNaN once we know there is no NaN operand.
0 * ∞ returns canonicalNaN once we know there is no NaN operand.
IEEE comparisons are unordered in the presence of NaNs.
Our executable comparator returns Option Ordering:
some ordfor the normal cases, andnonewhen the comparison is unordered (because at least one side is NaN).
This matches what you see in practice in PyTorch/NumPy: e.g. comparisons with NaN are false, and sorting has to pick an explicit policy for NaNs.
Symmetric version of compare_eq_none_of_isNaN_left.
minNum / maxNum (quiet-NaN ignoring) #
IEEE-754 distinguishes two related families of min/max:
minimum/maximum, which propagate NaNs, andminNum/maxNum, which (roughly) ignore quiet NaNs when the other operand is numeric.
Our definitions in Exec32.lean follow this common convention, and the lemmas below let proofs
reason about those branches directly.
In PyTorch terms, minimum/maximum behave like torch.minimum/torch.maximum, while
minNum/maxNum are closer to torch.fmin/torch.fmax (the "ignore NaN when possible" variants).
If the left operand is a signaling NaN, minNum returns it (quieted).
If x is a quiet NaN and y is numeric, minNum x y returns the numeric operand.
This is the defining difference from minimum: minNum tries to return a number when one is
available.
If the left operand is a signaling NaN, maxNum returns it (quieted).