IEEE32 Executable Arithmetic

This file defines executable binary32 arithmetic for the core operations: addition, subtraction, multiplication, division, square root, and fused multiply-add. The implementation follows IEEE-style case splits for NaN/Inf/zero and delegates finite rounding to the dyadic rounding kernel.

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.