Runtime Float32 Bridge

External (assumption-based) bridge: Lean's Init.Float32 ↔ IEEE32Exec.

Why assumptions are necessary: Init.Float32 arithmetic in Lean is implemented by external runtime calls. Those calls are opaque to the Lean kernel, so (inside Lean) we cannot prove that the runtime implementation coincides bit-for-bit with any particular float32 specification.

We package the finite-result connection as a typeclass interface. If you (or your trusted runtime) can discharge the assumptions that finite runtime Float32 primitives match the executable kernel IEEE32Exec bit-for-bit, then you can:

1. execute with Float32 (runtime),
2. rewrite the result to IEEE32Exec,
3. reuse NN/Floats/IEEEExec/Bridge/FP32.lean and NN/Floats/IEEEExec/Bridge/Expressions.lean to connect execution to the FP32 rounding-on-ℝ model on finite/no-overflow inputs.

The trust boundary is explicit: the only unproved part is the external/runtime correctness assumption, which is unavoidable in a pure Lean development.

Background:

• IEEE 754-2019 (what it means to “match float32 semantics”): https://doi.org/10.1109/IEEESTD.2019.8766229

@[inline]

def TorchLean.Floats.IEEE754.Float32Bridge.toIEEE32Exec (x : Float32) : IEEE32Exec

Reinterpret a runtime Float32 as the executable bit-level float32 (IEEE32Exec).

@[inline]

def TorchLean.Floats.IEEE754.Float32Bridge.ofIEEE32Exec (x : IEEE32Exec) : Float32

Reinterpret an executable float32 bit-pattern as a runtime Float32.

What this bridge gives us

This file does not prove anything about the runtime semantics of Float32. Instead, it gives a clean interface that you can assume/provide:

• If the runtime Float32 primitives produce the same result bits as IEEE32Exec, then runtime evaluation can be rewritten into IEEE32Exec evaluation.
• Once we are in IEEE32Exec, we can use the internal bridge theorems to connect execution to the FP32 rounding-on-ℝ model on the finite/no-overflow path (NN/Floats/IEEEExec/Bridge/FP32.lean, NN/Floats/IEEEExec/Bridge/FP32Total.lean, and NN/Floats/IEEEExec/Bridge/Expressions.lean).

NaN payloads are deliberately outside the exact-bit contract: Lean runtimes may canonicalize them, whereas IEEE32Exec preserves a deterministic payload. Classification fields below still relate NaN, infinity, and finiteness for every runtime value.

External correctness assumptions

class TorchLean.Floats.IEEE754.Float32Bridge.RuntimeFloat32FiniteMatchesIEEE32Exec : Prop

Assumption package relating the finite-result part of Lean's runtime Float32 primitives to IEEE32Exec. Exact NaN payload agreement is intentionally not required.

• toBits_ofBits_of_isFinite (b : UInt32) : (IEEE32Exec.ofBits b).isFinite = true → (Float32.ofBits b).toBits = b
• add_bits_of_isFinite (a b : Float32) : a.isFinite = true → b.isFinite = true → (a.add b).isFinite = true → (a.add b).toBits = ((toIEEE32Exec a).add (toIEEE32Exec b)).bits
• sub_bits_of_isFinite (a b : Float32) : a.isFinite = true → b.isFinite = true → (a.sub b).isFinite = true → (a.sub b).toBits = ((toIEEE32Exec a).sub (toIEEE32Exec b)).bits
• mul_bits_of_isFinite (a b : Float32) : a.isFinite = true → b.isFinite = true → (a.mul b).isFinite = true → (a.mul b).toBits = ((toIEEE32Exec a).mul (toIEEE32Exec b)).bits
• div_bits_of_isFinite (a b : Float32) : a.isFinite = true → b.isFinite = true → (a.div b).isFinite = true → (a.div b).toBits = ((toIEEE32Exec a).div (toIEEE32Exec b)).bits
• neg_bits_of_isFinite (a : Float32) : a.isFinite = true → a.neg.toBits = (toIEEE32Exec a).neg.bits
• sqrt_bits_of_isFinite (a : Float32) : a.isFinite = true → a.sqrt.isFinite = true → a.sqrt.toBits = (toIEEE32Exec a).sqrt.bits
• isNaN_bits (a : Float32) : a.isNaN = (toIEEE32Exec a).isNaN
• isInf_bits (a : Float32) : a.isInf = (toIEEE32Exec a).isInf
• isFinite_bits (a : Float32) : a.isFinite = (toIEEE32Exec a).isFinite

Derived bit-level refinement lemmas

Derived lemmas (rewriting runtime to executable)

The assumptions above are phrased as bit equalities. In practice we almost always want the more convenient value-level rewriting lemmas below:

toIEEE32Exec (a + b) = IEEE32Exec.add (toIEEE32Exec a) (toIEEE32Exec b), etc.

These are the lemmas you use to “turn a runtime evaluation into an IEEE32Exec evaluation”.

theorem TorchLean.Floats.IEEE754.Float32Bridge.RuntimeFloat32FiniteMatchesIEEE32Exec.toIEEE32Exec_add [RuntimeFloat32FiniteMatchesIEEE32Exec] (a b : Float32) : a.isFinite = true → b.isFinite = true → (a.add b).isFinite = true → toIEEE32Exec (a.add b) = (toIEEE32Exec a).add (toIEEE32Exec b)

Rewrite runtime float32 addition into executable IEEE32Exec.add.

theorem TorchLean.Floats.IEEE754.Float32Bridge.RuntimeFloat32FiniteMatchesIEEE32Exec.toIEEE32Exec_sub [RuntimeFloat32FiniteMatchesIEEE32Exec] (a b : Float32) : a.isFinite = true → b.isFinite = true → (a.sub b).isFinite = true → toIEEE32Exec (a.sub b) = (toIEEE32Exec a).sub (toIEEE32Exec b)

Rewrite runtime float32 subtraction into executable IEEE32Exec.sub (value-level form).

theorem TorchLean.Floats.IEEE754.Float32Bridge.RuntimeFloat32FiniteMatchesIEEE32Exec.toIEEE32Exec_mul [RuntimeFloat32FiniteMatchesIEEE32Exec] (a b : Float32) : a.isFinite = true → b.isFinite = true → (a.mul b).isFinite = true → toIEEE32Exec (a.mul b) = (toIEEE32Exec a).mul (toIEEE32Exec b)

Rewrite runtime float32 multiplication into executable IEEE32Exec.mul (value-level form).

theorem TorchLean.Floats.IEEE754.Float32Bridge.RuntimeFloat32FiniteMatchesIEEE32Exec.toIEEE32Exec_div [RuntimeFloat32FiniteMatchesIEEE32Exec] (a b : Float32) : a.isFinite = true → b.isFinite = true → (a.div b).isFinite = true → toIEEE32Exec (a.div b) = (toIEEE32Exec a).div (toIEEE32Exec b)

Rewrite runtime float32 division into executable IEEE32Exec.div (value-level form).

theorem TorchLean.Floats.IEEE754.Float32Bridge.RuntimeFloat32FiniteMatchesIEEE32Exec.toIEEE32Exec_neg [RuntimeFloat32FiniteMatchesIEEE32Exec] (a : Float32) (ha : a.isFinite = true) : toIEEE32Exec a.neg = (toIEEE32Exec a).neg

Rewrite runtime float32 negation into executable IEEE32Exec.neg (value-level form).

theorem TorchLean.Floats.IEEE754.Float32Bridge.RuntimeFloat32FiniteMatchesIEEE32Exec.toIEEE32Exec_sqrt [RuntimeFloat32FiniteMatchesIEEE32Exec] (a : Float32) : a.isFinite = true → a.sqrt.isFinite = true → toIEEE32Exec a.sqrt = (toIEEE32Exec a).sqrt

Rewrite runtime float32 square root into executable IEEE32Exec.sqrt (value-level form).

theorem TorchLean.Floats.IEEE754.Float32Bridge.RuntimeFloat32FiniteMatchesIEEE32Exec.toIEEE32Exec_ofIEEE32Exec [RuntimeFloat32FiniteMatchesIEEE32Exec] (x : IEEE32Exec) (hx : x.isFinite = true) : toIEEE32Exec (ofIEEE32Exec x) = x

Converting a finite IEEE32Exec value to runtime Float32 and back preserves its bits.