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.

structure TorchLean.Floats.IEEE754.IEEE32Exec.Dyadic : Type

Exact dyadic value (-1)^sign * mant * 2^exp used as an intermediate for finite ops.

• sign : Bool

  sign.

• mant : ℕ

  mant.

• exp : ℤ

  exp.

@[implicit_reducible]

instance TorchLean.Floats.IEEE754.IEEE32Exec.instReprDyadic : Repr Dyadic

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

@[implicit_reducible]

instance TorchLean.Floats.IEEE754.IEEE32Exec.instDecidableEqDyadic : DecidableEq Dyadic

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

def TorchLean.Floats.IEEE754.IEEE32Exec.pow2 (k : ℕ) : ℕ

2^k as a natural number.

def TorchLean.Floats.IEEE754.IEEE32Exec.roundShiftRightEven (n shift : ℕ) : ℕ

Round n / 2^shift to nearest, ties-to-even.

This is the primitive "shift + rounding" operation we use when shrinking a mantissa back down to a fixed bit width. It is the same tie-breaking policy as IEEE round-to-nearest-even.

def TorchLean.Floats.IEEE754.IEEE32Exec.mkBits (sign : Bool) (exp frac : ℕ) : UInt32

Construct a raw binary32 bit-pattern from fields.

mkBits sign exp frac places:

• sign in bit 31,
• exp in bits 30..23 (8 bits),
• frac in bits 22..0 (masked to 23 bits).

def TorchLean.Floats.IEEE754.IEEE32Exec.toDyadic? (x : IEEE32Exec) : Option Dyadic

Decode a finite binary32 into an exact dyadic value.

Returns none for NaN/Inf.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.isNaN_eq_false_of_toDyadic?_some {x : IEEE32Exec} {d : Dyadic} (hx : x.toDyadic? = some d) : x.isNaN = false

If toDyadic? x = some d then x is not a NaN.

Informal: toDyadic? only returns some _ for finite floats; NaNs map to none.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.isInf_eq_false_of_toDyadic?_some {x : IEEE32Exec} {d : Dyadic} (hx : x.toDyadic? = some d) : x.isInf = false

If toDyadic? x = some d then x is not an infinity.

Informal: toDyadic? only returns some _ for finite floats; infinities map to none.

Rounding back to binary32

The general pattern for the finite ops in this file is:

1. decode float32(s) to an exact intermediate representation (Dyadic for + - * fma sqrt, rationals for /),
2. compute the exact result in that intermediate representation,
3. round once to float32 using round-to-nearest, ties-to-even.

def TorchLean.Floats.IEEE754.IEEE32Exec.roundDyadicToIEEE32 (d : Dyadic) : IEEE32Exec

Round an exact dyadic value to binary32 (ties-to-even).

This function implements:

• overflow to ±Inf,
• gradual underflow into subnormals (down to exponent -149),
• underflow-to-zero below 2^-150 (half the minimum subnormal, where ties-to-even chooses 0),
• mantissa rounding to the 24-bit precision of binary32 normal numbers.

Exact dyadic arithmetic (finite core)

Dyadic is closed under + and * (at the exact level). We use these helpers before rounding back to float32.

def TorchLean.Floats.IEEE754.IEEE32Exec.addDyadic (a b : Dyadic) : Dyadic

Exact dyadic addition.

We align exponents by shifting the mantissa of the operand with the larger exponent, add signed integers, and then return an exact dyadic (no rounding yet).

Exact rationals for division

For division we compute an exact rational num/den (with den > 0) and then round it to binary32 using round-to-nearest, ties-to-even.

def TorchLean.Floats.IEEE754.IEEE32Exec.roundQuotEven (num den : ℕ) : ℕ

Round num/den to nearest, ties-to-even (assumes den > 0).

def TorchLean.Floats.IEEE754.IEEE32Exec.ratLtPow2 (num den : ℕ) (k : ℤ) : Bool

Test whether num/den < 2^k without converting to reals.

def TorchLean.Floats.IEEE754.IEEE32Exec.ratGePow2 (num den : ℕ) (k : ℤ) : Bool

Test whether num/den ≥ 2^k without converting to reals.

def TorchLean.Floats.IEEE754.IEEE32Exec.floorLog2Rat (num den : ℕ) : ℤ

Compute ⌊log₂(num/den)⌋ as an Int (assumes num > 0 and den > 0).

We start from the rough estimate log2(num) - log2(den) and then adjust by checking against powers of two.

def TorchLean.Floats.IEEE754.IEEE32Exec.roundRatToIEEE32 (sign : Bool) (num den : ℕ) : IEEE32Exec

Round an exact rational num/den to binary32 (ties-to-even).

This is the division analogue of roundDyadicToIEEE32: it uses the same exponent thresholds and the same final mantissa rounding policy.

def TorchLean.Floats.IEEE754.IEEE32Exec.add (x y : IEEE32Exec) : IEEE32Exec

IEEE754 addition (round-to-nearest, ties-to-even), with NaN/Inf rules.

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.sub (x y : IEEE32Exec) : IEEE32Exec

IEEE754 subtraction (defined as addition with sign-flip).

def TorchLean.Floats.IEEE754.IEEE32Exec.mul (x y : IEEE32Exec) : IEEE32Exec

IEEE754 multiplication (round-to-nearest, ties-to-even), with NaN/Inf rules.

def TorchLean.Floats.IEEE754.IEEE32Exec.div (x y : IEEE32Exec) : IEEE32Exec

IEEE754 division (round-to-nearest, ties-to-even), with NaN/Inf rules.

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

IEEE754 fused multiply-add: compute x*y+z and round once (ties-to-even).

theorem TorchLean.Floats.IEEE754.IEEE32Exec.add_eq_roundDyadicToIEEE32_of_toDyadic? {x y : IEEE32Exec} {dx dy : Dyadic} (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) : x.add y = roundDyadicToIEEE32 (addDyadic dx dy)

If both inputs decode to dyadics, add is “exact dyadic add, then round once”.

Informal: for finite x,y, we compute the exact dyadic value dx + dy and apply IEEE round-to-nearest-even.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.mul_eq_roundDyadicToIEEE32_of_toDyadic? {x y : IEEE32Exec} {dx dy : Dyadic} (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) : x.mul y = roundDyadicToIEEE32 { sign := dx.sign ^^ dy.sign, mant := dx.mant * dy.mant, exp := dx.exp + dy.exp }

If both inputs decode to dyadics, mul is “exact dyadic multiply, then round once”.

Informal: for finite x,y, the exact product is a dyadic with mantissa dx.mant * dy.mant and exponent dx.exp + dy.exp, and we round that back to binary32.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.fma_eq_roundDyadicToIEEE32_of_toDyadic? {x y z : IEEE32Exec} {dx dy dz : Dyadic} (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) (hz : z.toDyadic? = some dz) : x.fma y z = roundDyadicToIEEE32 (addDyadic { sign := dx.sign ^^ dy.sign, mant := dx.mant * dy.mant, exp := dx.exp + dy.exp } dz)

If all inputs decode to dyadics, fma x y z is “exact dyadic (x*y) + z, then round once”.

Informal: for finite inputs, we compute the exact dyadic product dx*dy, add dz, and finally apply IEEE round-to-nearest-even.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.div_eq_roundRatToIEEE32_of_toDyadic? {x y : IEEE32Exec} {dx dy : Dyadic} (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) (hy0 : dy.mant ≠ 0) : x.div y = have sign := dx.sign ^^ dy.sign; have eDiff := dx.exp - dy.exp; match match eDiff with | Int.ofNat sh => (dx.mant.shiftLeft sh, dy.mant) | Int.negSucc sh => (dx.mant, dy.mant.shiftLeft (sh + 1)) with | (num, den) => roundRatToIEEE32 sign num den

If x and y decode to dyadics and the denominator mantissa is nonzero, div x y is obtained by forming the exact rational quotient and rounding once.

Informal: for finite nonzero y, we compute the exact value (dx.mant * 2^dx.exp) / (dy.mant * 2^dy.exp) as a rational num/den with an exponent adjustment, then apply IEEE round-to-nearest-even.

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

IEEE754 square root (ties-to-even).

def TorchLean.Floats.IEEE754.IEEE32Exec.cmpDyadic (a b : Dyadic) : Ordering

Compare two exact dyadics by exact integer comparison.

This is used internally by executable rounding and special-case logic. The implementation normalizes the exponents to a common minimum exponent and compares the scaled integer mantissas.

def TorchLean.Floats.IEEE754.IEEE32Exec.shiftRightCeilPow2 (n shift : ℕ) : ℕ

ceil(n / 2^shift) for naturals, implemented via shifts (used for directed rounding).

def TorchLean.Floats.IEEE754.IEEE32Exec.roundDyadicPosDown (mant : ℕ) (exp : ℤ) : IEEE32Exec

Directed rounding down (toward -∞) for a positive dyadic mant * 2^exp.

def TorchLean.Floats.IEEE754.IEEE32Exec.roundDyadicPosUp (mant : ℕ) (exp : ℤ) : IEEE32Exec

Directed rounding up (toward +∞) for a positive dyadic mant * 2^exp.

def TorchLean.Floats.IEEE754.IEEE32Exec.roundDyadicDown (d : Dyadic) : IEEE32Exec

Directed rounding down (toward -∞) of an exact dyadic to float32.

def TorchLean.Floats.IEEE754.IEEE32Exec.roundDyadicUp (d : Dyadic) : IEEE32Exec

Directed rounding up (toward +∞) of an exact dyadic to float32.

def TorchLean.Floats.IEEE754.IEEE32Exec.addDown (x y : IEEE32Exec) : IEEE32Exec

addDown x y is a float32 lower bound for the exact real sum (when finite).

def TorchLean.Floats.IEEE754.IEEE32Exec.addUp (x y : IEEE32Exec) : IEEE32Exec

addUp x y is a float32 upper bound for the exact real sum (when finite).

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.subDown (x y : IEEE32Exec) : IEEE32Exec

subDown x y is a float32 lower bound for the exact real difference (when finite).

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.subUp (x y : IEEE32Exec) : IEEE32Exec

subUp x y is a float32 upper bound for the exact real difference (when finite).

def TorchLean.Floats.IEEE754.IEEE32Exec.mulDown (x y : IEEE32Exec) : IEEE32Exec

mulDown x y is a float32 lower bound for the exact real product (when finite).

def TorchLean.Floats.IEEE754.IEEE32Exec.mulUp (x y : IEEE32Exec) : IEEE32Exec

mulUp x y is a float32 upper bound for the exact real product (when finite).

Directed rounding for exact rationals (division-friendly)

For divDown/divUp we need outward rounding of an exact rational num/den to the float32 grid. Our dyadic-directed rounders (roundDyadicDown/roundDyadicUp) already have a clean soundness proof, so we reduce rational rounding to dyadic rounding by building a dyadic enclosure of num/den:

• lower dyadic: ⌊(num/den) * 2^K⌋ * 2^{-K},
• upper dyadic: ⌈(num/den) * 2^K⌉ * 2^{-K}.

We then apply roundDyadicDown/roundDyadicUp to these dyadics.

This is sound (it produces outward-rounded endpoints), but it is not necessarily optimally tight; a larger ratApproxShift improves tightness at some computational cost.

def TorchLean.Floats.IEEE754.IEEE32Exec.ratApproxShift : ℕ

Number of extra bits used when turning num/den into a dyadic enclosure.

def TorchLean.Floats.IEEE754.IEEE32Exec.quotCeil (num den : ℕ) : ℕ

ceil(num/den) for naturals, totalized (returns 0 when den = 0).

def TorchLean.Floats.IEEE754.IEEE32Exec.ratLowerMant (num den : ℕ) : ℕ

Lower dyadic mantissa for num/den at scale 2^ratApproxShift.

def TorchLean.Floats.IEEE754.IEEE32Exec.ratUpperMant (num den : ℕ) : ℕ

Upper dyadic mantissa for num/den at scale 2^ratApproxShift.

def TorchLean.Floats.IEEE754.IEEE32Exec.roundRatDown (sign : Bool) (num den : ℕ) : IEEE32Exec

Directed rounding down (toward -∞) for a rational ±(num/den) with den > 0.

We do not attempt to be "correctly rounded" in the IEEE-754 sense; we only need a sound lower bound.

def TorchLean.Floats.IEEE754.IEEE32Exec.roundRatUp (sign : Bool) (num den : ℕ) : IEEE32Exec

Directed rounding up (toward +∞) for a rational ±(num/den) with den > 0.

def TorchLean.Floats.IEEE754.IEEE32Exec.divDown (x y : IEEE32Exec) : IEEE32Exec

divDown x y is a float32 lower bound for the exact real quotient (when finite and y ≠ 0).

def TorchLean.Floats.IEEE754.IEEE32Exec.divUp (x y : IEEE32Exec) : IEEE32Exec

divUp x y is a float32 upper bound for the exact real quotient (when finite and y ≠ 0).

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

IEEE754 numerical comparison.

Returns none (unordered) if either operand is NaN; otherwise returns an Ordering.

def TorchLean.Floats.IEEE754.IEEE32Exec.lt (x y : IEEE32Exec) : Prop

Strict order induced by IEEE-754 comparison.

lt x y is true exactly when compare x y = some .lt. In particular, if either side is NaN then lt x y is false (because compare returns none).

def TorchLean.Floats.IEEE754.IEEE32Exec.le (x y : IEEE32Exec) : Prop

Non-strict order induced by IEEE-754 comparison.

le x y is true when compare x y returns .lt or .eq, and false otherwise (including the NaN unordered case).

Order lemmas

IEEE-754 comparisons treat NaNs as unordered, so in particular le x x is not true for NaNs. For the interval layer, we mainly need the basic fact that le is reflexive on finite values.

@[simp]

theorem TorchLean.Floats.IEEE754.IEEE32Exec.le_self_of_isFinite_eq_true (x : IEEE32Exec) (hx : x.isFinite = true) : x.le x

IEEE32Exec.le is reflexive on finite values.

Informally: if x is a finite float32, then x ≤ x. (NaNs are excluded by the isFinite premise: for NaN, isFinite x = false and x ≤ x is false because compare returns none.)

This lemma is used by the executable interval layer to show that the "point interval" [x, x] is valid whenever x is finite.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.le_self_of_isFinite_eq_true_imp (x : IEEE32Exec) : x.isFinite = true → x.le x

Curried form of le_self_of_isFinite_eq_true (useful for simp).

@[simp]

theorem TorchLean.Floats.IEEE754.IEEE32Exec.isFinite_imp_le_self_iff_true (x : IEEE32Exec) : x.isFinite = true → x.le x ↔ True

isFinite x = true → x ≤ x is always true.

This looks a bit odd, but it's exactly the side-goal produced by simp [Valid, point] in the executable interval module (NN/Floats/Interval/IEEEExec32.lean). Registering this as a simp lemma lets that file stay a one-liner.

def TorchLean.Floats.IEEE754.IEEE32Exec.minimum (x y : IEEE32Exec) : IEEE32Exec

IEEE754 minimum: NaNs propagate; minimum(-0,+0) = -0.

def TorchLean.Floats.IEEE754.IEEE32Exec.maximum (x y : IEEE32Exec) : IEEE32Exec

IEEE754 maximum: NaNs propagate; maximum(-0,+0) = +0.

def TorchLean.Floats.IEEE754.IEEE32Exec.minNum (x y : IEEE32Exec) : IEEE32Exec

IEEE754 minNum: if exactly one operand is a quiet NaN, return the other operand.

Signaling NaNs still propagate (quieted).

def TorchLean.Floats.IEEE754.IEEE32Exec.maxNum (x y : IEEE32Exec) : IEEE32Exec

IEEE754 maxNum: if exactly one operand is a quiet NaN, return the other operand.

Signaling NaNs still propagate (quieted).

def TorchLean.Floats.IEEE754.IEEE32Exec.toFloat (x : IEEE32Exec) : Float

Convert to an exact Float (binary64); finite float32 values embed exactly in binary64.

def TorchLean.Floats.IEEE754.IEEE32Exec.ofFloat (x : Float) : IEEE32Exec

Convert/round an IEEE binary64 Float to float32 (ties-to-even).

def TorchLean.Floats.IEEE754.IEEE32Exec.Transcendentals.fixedScale : ℕ

Fixed-point scale (in bits) used by the integer-only exp/log approximations.

def TorchLean.Floats.IEEE754.IEEE32Exec.Transcendentals.fixedScaleInt : ℤ

fixedScale as an Int.

def TorchLean.Floats.IEEE754.IEEE32Exec.Transcendentals.fixedOne : ℤ

Fixed-point encoding of 1 at scale fixedScale (i.e. 2^fixedScale).

def TorchLean.Floats.IEEE754.IEEE32Exec.Transcendentals.pow2Int (k : ℕ) : ℤ

Integer power of two: pow2Int k = 2^k as an Int.

def TorchLean.Floats.IEEE754.IEEE32Exec.Transcendentals.roundQuotEvenInt (num den : ℤ) : ℤ

Round an integer quotient num/den to the nearest integer, ties-to-even.

Assumes den > 0.

def TorchLean.Floats.IEEE754.IEEE32Exec.Transcendentals.roundDivPow2EvenInt (n : ℤ) (shift : ℕ) : ℤ

Divide by 2^shift, rounding to nearest with ties-to-even.

def TorchLean.Floats.IEEE754.IEEE32Exec.Transcendentals.shiftPow2EvenInt (n k : ℤ) : ℤ

Shift by a power of two: multiply when k ≥ 0, divide when k < 0.

Division uses ties-to-even rounding.

def TorchLean.Floats.IEEE754.IEEE32Exec.Transcendentals.fixedMul (a b : ℤ) : ℤ

Fixed-point multiplication at scale fixedScale (ties-to-even).

def TorchLean.Floats.IEEE754.IEEE32Exec.Transcendentals.fixedDiv (a b : ℤ) : ℤ

Fixed-point division at scale fixedScale (ties-to-even).

If a and b are fixed-point at scale fixedScale, the result is at the same scale.

def TorchLean.Floats.IEEE754.IEEE32Exec.Transcendentals.fixedDivByNat (a : ℤ) (n : ℕ) : ℤ

Divide by a natural number, rounding to nearest with ties-to-even.

def TorchLean.Floats.IEEE754.IEEE32Exec.Transcendentals.fixedOfDyadic (d : Dyadic) : ℤ

Convert a dyadic number to a signed fixed-point integer at scale fixedScale.

def TorchLean.Floats.IEEE754.IEEE32Exec.Transcendentals.fixedToDyadic (x : ℤ) : Dyadic

Convert a signed fixed-point integer at scale fixedScale to a dyadic number.

def TorchLean.Floats.IEEE754.IEEE32Exec.Transcendentals.fixedLn2 : ℤ

Fixed-point approximation to ln 2 at scale fixedScale.

def TorchLean.Floats.IEEE754.IEEE32Exec.Transcendentals.fixedInvLn2 : ℤ

Fixed-point approximation to 1/ln 2 at scale fixedScale.

def TorchLean.Floats.IEEE754.IEEE32Exec.Transcendentals.exp2PolyCoeffsDesc : List ℤ

Fixed-point Taylor coefficients (highest degree first) for 2^x on [-1/2, 1/2].

def TorchLean.Floats.IEEE754.IEEE32Exec.Transcendentals.evalExp2Poly (xFixed : ℤ) : ℤ

Evaluate the fixed-point 2^x polynomial approximation using Horner’s method.

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

Deterministic exp (no delegation to Float): range-reduced 2^(x/ln2) with a fixedpoint polynomial.

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

Deterministic log (no delegation to Float): normalize x = m*2^k and use an atanh-series for log m.

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

Deterministic sinh (no delegation to Float): defined via exp.

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

Deterministic cosh (no delegation to Float): defined via exp.

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

Deterministic tanh (no delegation to Float): stable form tanh x = s*(1 - 2/(exp(2*|x|)+1)).

Deterministic sin/cos

Unlike exp/log, sin and cos are used by the runtime FFT layer (NN.Runtime.*.Fft) to build twiddle factors. Delegating to the host Float implementation makes results platform-dependent.

We implement sin/cos purely inside Lean:

1. scale the input down by a power of two so |y| < 1/2,
2. approximate sin y and cos y by exact Taylor partial sums (degree 13 / 12),
3. scale back up using m applications of the double-angle formulas.

This is deterministic and uses only the IEEE32Exec kernel ops (roundRatToIEEE32, add/mul/sub, etc.). We do not claim correctly-rounded libm behavior; the goal is reproducible execution.

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.Trig.mulDyadic (a b : Dyadic) : Dyadic

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.Trig.oneDyadic : Dyadic

Dyadic 1.

def TorchLean.Floats.IEEE754.IEEE32Exec.Trig.roundDyadicDivNat (d : Dyadic) (den : ℕ) : IEEE32Exec

Round the exact rational d / den to binary32, where d is an exact dyadic mant * 2^exp.

We package the dyadic exponent into a rational numerator/denominator and call roundRatToIEEE32.

Taylor partial sums on |y| < 1/2

We encode the partial sums using a common factorial denominator so the coefficients are exact integers, not approximations.

For z = y^2:

• sin y = ∑_{i=0}^6 (-1)^i y^(2i+1)/(2i+1)! + R₇(y) where the polynomial part can be written as y * (∑_{i=0}^6 (-1)^i (13!/(2i+1)!) z^i) / 13!.

• cos y = ∑_{i=0}^6 (-1)^i y^(2i)/(2i)! + R₇'(y) i.e. (∑_{i=0}^6 (-1)^i (12!/(2i)!) z^i) / 12!.

def TorchLean.Floats.IEEE754.IEEE32Exec.Trig.sinDen : ℕ

def TorchLean.Floats.IEEE754.IEEE32Exec.Trig.cosDen : ℕ

def TorchLean.Floats.IEEE754.IEEE32Exec.Trig.sinCoeff (i : ℕ) : ℤ

def TorchLean.Floats.IEEE754.IEEE32Exec.Trig.cosCoeff (i : ℕ) : ℤ

def TorchLean.Floats.IEEE754.IEEE32Exec.Trig.coeffToDyadic (c : ℤ) : Dyadic

def TorchLean.Floats.IEEE754.IEEE32Exec.Trig.evalPolyNumerator (coeff : ℕ → ℤ) (z : Dyadic) : Dyadic

def TorchLean.Floats.IEEE754.IEEE32Exec.Trig.sinCosTaylorSmall (y : Dyadic) : IEEE32Exec × IEEE32Exec

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.Trig.doubleAngle (sc : IEEE32Exec × IEEE32Exec) : IEEE32Exec × IEEE32Exec

def TorchLean.Floats.IEEE754.IEEE32Exec.Trig.iterDoubleAngle : ℕ → IEEE32Exec × IEEE32Exec → IEEE32Exec × IEEE32Exec

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.Trig.sinCosPow2 (y : Dyadic) (m : ℕ) : IEEE32Exec × IEEE32Exec

def TorchLean.Floats.IEEE754.IEEE32Exec.Trig.sinCosScaled (dx : Dyadic) : IEEE32Exec × IEEE32Exec

def TorchLean.Floats.IEEE754.IEEE32Exec.Trig.sinCos (x : IEEE32Exec) : IEEE32Exec × IEEE32Exec

Joint deterministic sin/cos computation for IEEE32Exec.

def TorchLean.Floats.IEEE754.IEEE32Exec.Trig.sin (x : IEEE32Exec) : IEEE32Exec

Deterministic sin implementation (shared core via sinCos).

def TorchLean.Floats.IEEE754.IEEE32Exec.Trig.cos (x : IEEE32Exec) : IEEE32Exec

Deterministic cos implementation (shared core via sinCos).

Public sin / cos

We expose sin/cos as executable ops on IEEE32Exec using the deterministic implementation above, together with standard IEEE special-case conventions.

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

Deterministic sin for IEEE32Exec.

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

Deterministic cos for IEEE32Exec.

@[implicit_reducible]

instance TorchLean.Floats.IEEE754.IEEE32Exec.instToString : ToString IEEE32Exec

Pretty-print using Lean's Float printer (via toFloat).

@[implicit_reducible]

instance TorchLean.Floats.IEEE754.IEEE32Exec.instCoeNat : Coe ℕ IEEE32Exec

Coerce naturals to binary32 by converting through Lean's Float and re-encoding.

@[implicit_reducible]

instance TorchLean.Floats.IEEE754.IEEE32Exec.instOfNat (n : ℕ) : OfNat IEEE32Exec n

Numeral literals for IEEE32Exec.

This allows writing:

• (1 : IEEE32Exec)
• (42 : IEEE32Exec)

The interpretation is Nat → Float (binary64) → IEEE32Exec via ofFloat, i.e. it rounds the exact integer to the nearest representable float32 (which is exact for small enough integers).

@[implicit_reducible]

instance TorchLean.Floats.IEEE754.IEEE32Exec.instZero : Zero IEEE32Exec

0.0 as an executable binary32 value (chosen as +0.0).

@[implicit_reducible]

instance TorchLean.Floats.IEEE754.IEEE32Exec.instOne : One IEEE32Exec

1.0 as an executable binary32 value.

@[implicit_reducible]

instance TorchLean.Floats.IEEE754.IEEE32Exec.instNeg : Neg IEEE32Exec

Unary negation (IEEE-754 sign flip, with NaN payload rules).

@[implicit_reducible]

instance TorchLean.Floats.IEEE754.IEEE32Exec.instAdd : Add IEEE32Exec

IEEE-754 addition (with NaN/Inf rules).

@[implicit_reducible]

instance TorchLean.Floats.IEEE754.IEEE32Exec.instSub : Sub IEEE32Exec

IEEE-754 subtraction (with NaN/Inf rules).

@[implicit_reducible]

instance TorchLean.Floats.IEEE754.IEEE32Exec.instMul : Mul IEEE32Exec

IEEE-754 multiplication (with NaN/Inf rules).

@[implicit_reducible]

instance TorchLean.Floats.IEEE754.IEEE32Exec.instDiv : Div IEEE32Exec

IEEE-754 division (with NaN/Inf rules).

@[implicit_reducible]

instance TorchLean.Floats.IEEE754.IEEE32Exec.instPow : Pow IEEE32Exec IEEE32Exec

Exponentiation instance.

This is a deterministic executable choice, not a claim about correctly-rounded pow: we implement a small set of IEEE-like special cases and handle integer exponents exactly enough to avoid the most common footguns (negative bases, 0^0, 1^∞, etc.). For general non-integer exponents we fall back to exp (b * log a) on positive bases.

def TorchLean.Floats.IEEE754.IEEE32Exec.instPow.powNatLinear (a : IEEE32Exec) : ℕ → IEEE32Exec

@[implicit_reducible]

instance TorchLean.Floats.IEEE754.IEEE32Exec.instBEq : BEq IEEE32Exec

Boolean equality with IEEE-754 NaN/zero conventions.

• If either side is NaN, we return false.
• If both are zeros (either sign), we return true.
• Otherwise we compare raw bits.

@[implicit_reducible]

instance TorchLean.Floats.IEEE754.IEEE32Exec.instLT : LT IEEE32Exec

Strict order instance, defined via IEEE32Exec.lt.

@[implicit_reducible]

instance TorchLean.Floats.IEEE754.IEEE32Exec.instLE : LE IEEE32Exec

Non-strict order instance, defined via IEEE32Exec.le.

@[implicit_reducible]

instance TorchLean.Floats.IEEE754.IEEE32Exec.instDecidableRelLt : DecidableRel fun (x1 x2 : IEEE32Exec) => x1 < x2

Decidable < inherited from the compare-based definition.

@[implicit_reducible]

instance TorchLean.Floats.IEEE754.IEEE32Exec.instDecidableRelLe : DecidableRel fun (x1 x2 : IEEE32Exec) => x1 ≤ x2

Decidable ≤ inherited from the compare-based definition.

@[implicit_reducible]

instance TorchLean.Floats.IEEE754.IEEE32Exec.instMin : Min IEEE32Exec

min operator, implemented by IEEE-754 minimum.

@[implicit_reducible]

instance TorchLean.Floats.IEEE754.IEEE32Exec.instMax : Max IEEE32Exec

max operator, implemented by IEEE-754 maximum.

@[implicit_reducible]

instance TorchLean.Floats.IEEE754.IEEE32Exec.instMathFunctions : MathFunctions IEEE32Exec

Provide the MathFunctions interface using the deterministic implementations in this file.

@[implicit_reducible]

instance TorchLean.Floats.IEEE754.IEEE32Exec.instNumbers : Numbers IEEE32Exec

Numeric constants used by the spec library, instantiated at binary32.

@[implicit_reducible]

instance TorchLean.Floats.IEEE754.IEEE32Exec.instContext : Context IEEE32Exec

Context instance so the spec layer can execute with IEEE32Exec scalars.