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.

@[inline]

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).

@[inline]

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

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

@[inline]

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

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

@[inline]

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.

IEEE exception status

The value-only operations above remain the basic executable API. The wrappers below return the same value together with the five exception indicators defined by IEEE 754. Tininess is detected after rounding, and underflow is reported only when the rounded result is both tiny and inexact.

The status is computed from the exact dyadic or rational intermediate already used by each operation. No host floating-point operation or numerical tolerance enters this classification.

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

The five exception indicators associated with an IEEE-754 operation.

• invalid : Bool
• divideByZero : Bool
• overflow : Bool
• underflow : Bool
• inexact : Bool

@[implicit_reducible]

instance TorchLean.Floats.IEEE754.IEEE32Exec.instReprIEEEStatus : Repr IEEEStatus

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

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

@[implicit_reducible]

instance TorchLean.Floats.IEEE754.IEEE32Exec.instDecidableEqIEEEStatus : DecidableEq IEEEStatus

@[implicit_reducible]

instance TorchLean.Floats.IEEE754.IEEE32Exec.instInhabitedIEEEStatus : Inhabited IEEEStatus

def TorchLean.Floats.IEEE754.IEEE32Exec.IEEEStatus.clear : IEEEStatus

No exception was raised.

def TorchLean.Floats.IEEE754.IEEE32Exec.IEEEStatus.union (a b : IEEEStatus) : IEEEStatus

Accumulate exception indicators from two operations.

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

An executable binary32 value paired with the exception status produced while computing it.

• value : IEEE32Exec
• status : IEEEStatus

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

@[implicit_reducible]

instance TorchLean.Floats.IEEE754.IEEE32Exec.instReprIEEEOutcome : Repr IEEEOutcome

@[implicit_reducible]

instance TorchLean.Floats.IEEE754.IEEE32Exec.instDecidableEqIEEEOutcome : DecidableEq IEEEOutcome

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

@[implicit_reducible]

instance TorchLean.Floats.IEEE754.IEEE32Exec.instInhabitedIEEEOutcome : Inhabited IEEEOutcome

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

Whether a finite binary32 result is zero or subnormal.

def TorchLean.Floats.IEEE754.IEEE32Exec.dyadicRoundingStatus (exact : Dyadic) (rounded : IEEE32Exec) : IEEEStatus

Classify rounding an exact dyadic to the supplied binary32 result.

def TorchLean.Floats.IEEE754.IEEE32Exec.rationalEqualsDyadic (sign : Bool) (num den : ℕ) (d : Dyadic) : Bool

Exact equality between num / den and a dyadic magnitude, including the result sign.

def TorchLean.Floats.IEEE754.IEEE32Exec.rationalRoundingStatus (sign : Bool) (num den : ℕ) (rounded : IEEE32Exec) : IEEEStatus

Classify rounding an exact signed rational to the supplied binary32 result.

def TorchLean.Floats.IEEE754.IEEE32Exec.addWithStatus (x y : IEEE32Exec) : IEEEOutcome

Binary32 addition with IEEE exception status.

def TorchLean.Floats.IEEE754.IEEE32Exec.subWithStatus (x y : IEEE32Exec) : IEEEOutcome

Binary32 subtraction with IEEE exception status.

def TorchLean.Floats.IEEE754.IEEE32Exec.mulWithStatus (x y : IEEE32Exec) : IEEEOutcome

Binary32 multiplication with IEEE exception status.

def TorchLean.Floats.IEEE754.IEEE32Exec.divWithStatus (x y : IEEE32Exec) : IEEEOutcome

Binary32 division with IEEE exception status.

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

Fused multiply-add with IEEE exception status.

def TorchLean.Floats.IEEE754.IEEE32Exec.sqrtWithStatus (x : IEEE32Exec) : IEEEOutcome

Binary32 square root with IEEE exception status.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.dyadicRoundingStatus_inexact_of_underflow {exact : Dyadic} {rounded : IEEE32Exec} (h : (dyadicRoundingStatus exact rounded).underflow = true) : (dyadicRoundingStatus exact rounded).inexact = true

After-rounding dyadic underflow is reported only for an inexact result.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.rationalRoundingStatus_inexact_of_underflow {sign : Bool} {num den : ℕ} {rounded : IEEE32Exec} (h : (rationalRoundingStatus sign num den rounded).underflow = true) : (rationalRoundingStatus sign num den rounded).inexact = true

After-rounding rational underflow is reported only for an inexact result.