Directed executable IEEE32 operations.

This file provides lower and upper rounding variants for arithmetic operations, forming the runtime side of the interval-enclosure story.

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

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

fmaDown x y z computes the exact value x * y + z and rounds once toward -∞.

This is a directed fused multiply-add: the product is not rounded before the addition. The special-value cases agree with fma; finite inputs are converted to exact dyadics, and each nonzero exact product-plus-sum is passed once to roundDyadicDown. Exact cancellation bypasses the generic rounder and returns the signed zero required by round-toward-negative.

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

fmaUp x y z computes the exact value x * y + z and rounds once toward +∞.

As with fmaDown, no intermediate product rounding occurs. Keeping both operations in terms of the same exact dyadic expression makes their enclosure theorems share one semantic statement.

Directed square root

For a positive dyadic mant * 2^exp, parity normalization rewrites the radicand as mant' * 2^(2 * expHalf). After scaling mant' by an even power of two, Nat.sqrt gives the lower integer endpoint and its remainder tells us whether the upper endpoint is distinct. The resulting dyadics enclose the exact square root before they are rounded to binary32.

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

Dyadic lower and upper endpoints for a nonnegative square root.

• lower : Dyadic

  Lower endpoint.

• upper : Dyadic

  Upper endpoint.

def TorchLean.Floats.IEEE754.IEEE32Exec.sqrtDyadicBracket (d : Dyadic) : SqrtDyadicBracket

Compute both square-root endpoints from one parity normalization and integer square root.

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

Square root rounded toward -∞; negative finite inputs produce NaN.

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

Square root rounded toward +∞; negative finite inputs produce NaN.

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