Executable IEEE-754 binary32 (IEEE32Exec)

TorchLean uses two complementary ways to talk about "float32":

• NN/Floats/NeuralFloat/* and NN/Floats/FP32/* model rounding-on-ℝ. This is suited to proofs and for compositional "real computation + rounding error" arguments.
• IEEE32Exec (in this file) models bit-level IEEE-754 behavior. This is what you want when you care about corner cases like NaN/Inf payload propagation, signed zero, and exact tie-breaking.

We implement IEEE32Exec as raw UInt32 bits and provide:

• decoders/encoders for the binary32 layout,
• nextUp/nextDown (adjacent representable floats),
• basic arithmetic (+ - * / fma) by decoding to an exact dyadic/rational intermediate and then rounding once (round-to-nearest, ties-to-even),
• comparisons and min/max with IEEE-754 NaN rules,
• sqrt via integer arithmetic on the exact input value, rounded back to binary32.

We also provide a Context IEEE32Exec instance so the spec layer can run modules with an executable scalar. That is why we import NN.Spec.Core.Context here.

About transcendentals

IEEE-754 does not specify implementations for transcendental functions (exp, tanh, ...). In practice those are provided by libm (or vendor math libraries) and vary across platforms.

We provide deterministic implementations for a few transcendentals in Lean so examples can run without delegating to the host runtime. For the remaining ones, we may still delegate to Lean's Float (binary64) and round back to binary32. These functions are executable and stable, but they are not claimed to be correctly rounded or to match any particular hardware/libm.

References

• 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).
• S. Boldo, G. Melquiond, “Flocq: a unified Coq library for proving floating-point algorithms correct” (ARITH 2011). DOI: 10.1109/ARITH.2011.40

structure TorchLean.Floats.IEEE754.IEEE32Exec : Type

Executable IEEE-754 binary32 value, stored as raw bits.

• bits : UInt32

  bits.

def TorchLean.Floats.IEEE754.instDecidableEqIEEE32Exec.decEq (x✝ x✝¹ : IEEE32Exec) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance TorchLean.Floats.IEEE754.instDecidableEqIEEE32Exec : DecidableEq IEEE32Exec

@[implicit_reducible]

instance TorchLean.Floats.IEEE754.instReprIEEE32Exec : Repr IEEE32Exec

def TorchLean.Floats.IEEE754.instReprIEEE32Exec.repr : IEEE32Exec → ℕ → Std.Format

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.ofBits (b : UInt32) : IEEE32Exec

Wrap raw binary32 bits as an IEEE32Exec.

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.toBits (x : IEEE32Exec) : UInt32

Extract the raw binary32 bits of an IEEE32Exec.

@[simp]

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toBits_ofBits (b : UInt32) : (ofBits b).toBits = b

toBits (ofBits b) = b.

@[simp]

theorem TorchLean.Floats.IEEE754.IEEE32Exec.ofBits_toBits (x : IEEE32Exec) : ofBits x.toBits = x

ofBits (toBits x) = x.

@[implicit_reducible]

instance TorchLean.Floats.IEEE754.IEEE32Exec.instInhabited : Inhabited IEEE32Exec

Default inhabitant: all bits zero, i.e. +0.0.

Binary32 bit layout

IEEE-754 binary32 is stored as:

• sign bit s in bit 31,
• exponent field e in bits 30..23 (8 bits, bias 127),
• fraction field f in bits 22..0 (23 bits).

For NaNs, the "quiet" bit is the top fraction bit.

def TorchLean.Floats.IEEE754.IEEE32Exec.signMask : UInt32

Mask selecting the sign bit (bit 31).

def TorchLean.Floats.IEEE754.IEEE32Exec.expMask : UInt32

Mask selecting the 8-bit exponent field (bits 30..23).

def TorchLean.Floats.IEEE754.IEEE32Exec.fracMask : UInt32

Mask selecting the 23-bit fraction field (bits 22..0).

def TorchLean.Floats.IEEE754.IEEE32Exec.quietBit : UInt32

The IEEE-754 "quiet NaN" indicator bit (top fraction bit).

def TorchLean.Floats.IEEE754.IEEE32Exec.expAllOnes : UInt32

8-bit value 0xFF, used to test the “all ones” exponent field.

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.signBit (x : IEEE32Exec) : Bool

True iff the sign bit (bit 31) is set.

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.expField (x : IEEE32Exec) : UInt32

Extract the 8-bit exponent field (bits 30..23).

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.fracField (x : IEEE32Exec) : UInt32

Extract the 23-bit fraction field (bits 22..0).

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.isNaN (x : IEEE32Exec) : Bool

Predicate for NaN: exponent all ones and fraction nonzero.

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.isQNaN (x : IEEE32Exec) : Bool

Predicate for quiet NaN (NaN with the quiet bit set).

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.isSNaN (x : IEEE32Exec) : Bool

Predicate for signaling NaN (NaN with the quiet bit clear).

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.isInf (x : IEEE32Exec) : Bool

Predicate for infinity: exponent all ones and fraction zero.

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.isZero (x : IEEE32Exec) : Bool

Predicate for signed zero (both +0 and -0).

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.isFinite (x : IEEE32Exec) : Bool

Predicate for finiteness: exponent field is not all ones (excludes NaN/Inf).

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.posZero : IEEE32Exec

+0.0 as an executable binary32 constant.

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.negZero : IEEE32Exec

-0.0 as an executable binary32 constant.

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.posOne : IEEE32Exec

+1.0 as an IEEE-754 binary32 constant.

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.negOne : IEEE32Exec

-1.0 as an IEEE-754 binary32 constant.

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.posInf : IEEE32Exec

+∞ as an executable binary32 constant.

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.negInf : IEEE32Exec

-∞ as an executable binary32 constant.

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.canonicalNaN : IEEE32Exec

A canonical quiet NaN payload used by the executable kernel.

NaN selection / payload propagation

IEEE-754 leaves some freedom in how NaNs are "chosen" when multiple NaNs appear. For reproducibility (and nicer debugging), we make the choice deterministic (left-to-right) and we quiet signaling NaNs by setting the quiet bit.

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.quietNaN (x : IEEE32Exec) : IEEE32Exec

Quiet a NaN by setting the quiet bit (and leave non-NaNs unchanged).

def TorchLean.Floats.IEEE754.IEEE32Exec.chooseNaN1 (x : IEEE32Exec) : Option IEEE32Exec

If x is a NaN, return it (quieted).

def TorchLean.Floats.IEEE754.IEEE32Exec.chooseNaN2 (x y : IEEE32Exec) : Option IEEE32Exec

Choose a NaN from two operands.

This is the "NaN propagation" policy used by most binary ops in this file:

• if any operand is a signaling NaN, return that operand (quieted), left-to-right,
• otherwise if any operand is a quiet NaN, return that operand, left-to-right,
• otherwise return none.

def TorchLean.Floats.IEEE754.IEEE32Exec.chooseNaN3 (x y z : IEEE32Exec) : Option IEEE32Exec

Like chooseNaN2, but for ternary ops (used for fma).

Adjacent floats (nextUp/nextDown)

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.posMinSubnormal : IEEE32Exec

Smallest positive subnormal (bit pattern 0x00000001, value 2^-149).

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.negMinSubnormal : IEEE32Exec

Smallest negative subnormal (bit pattern 0x80000001, value -2^-149).

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.posMaxFinite : IEEE32Exec

Largest finite positive float32 (bit pattern 0x7F7FFFFF).

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.negMaxFinite : IEEE32Exec

Largest finite negative float32 (bit pattern 0xFF7FFFFF).

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.nextUp (x : IEEE32Exec) : IEEE32Exec

nextUp x is the next representable float32 strictly greater than x.

IEEE-754 special cases:

• NaN propagates (quieted).
• nextUp (+∞) = +∞.
• nextUp (-0) = +minSubnormal (since +0 is not strictly greater than -0).

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.nextDown (x : IEEE32Exec) : IEEE32Exec

nextDown x is the next representable float32 strictly less than x.

IEEE-754 special cases:

• NaN propagates (quieted).
• nextDown (-∞) = -∞.
• nextDown (+0) = -minSubnormal (since -0 is not strictly less than +0).

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.neg (x : IEEE32Exec) : IEEE32Exec

Flip the sign bit (works for finite/Inf/NaN, and distinguishes ±0).

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.abs (x : IEEE32Exec) : IEEE32Exec

Clear the sign bit.