BridgeInitFloat32

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 intended connection as a typeclass interface. If you (or your trusted runtime) can discharge the assumptions that the 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 the internal refinement theorems (BridgeFP32.lean / BridgeFP32Expr.lean) to connect execution to the FP32 rounding-on-ℝ model on finite/no-overflow inputs.

This keeps the trust boundary 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

@[reducible, inline]

abbrev TorchLean.Floats.IEEE754.Float32Bridge.F32 : Type

Local alias for Lean's runtime Float32 type.

@[inline]

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

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

@[inline]

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

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 (BridgeFP32.lean, BridgeFP32Total.lean, BridgeFP32Expr.lean).

We keep this separation because it makes the trust boundary explicit: the only “axioms” are the bit-level runtime correctness assumptions below.

External correctness assumptions

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

Assumption package relating Lean's runtime Float32 primitives to IEEE32Exec.

• toBits_ofBits (b : UInt32) : (Float32.ofBits b).toBits = b
• ofBits_toBits (x : F32) : Float32.ofBits (Float32.toBits x) = x
• add_bits (a b : F32) : (Float32.add a b).toBits = ((toIEEE32Exec a).add (toIEEE32Exec b)).bits
• sub_bits (a b : F32) : (Float32.sub a b).toBits = ((toIEEE32Exec a).sub (toIEEE32Exec b)).bits
• mul_bits (a b : F32) : (Float32.mul a b).toBits = ((toIEEE32Exec a).mul (toIEEE32Exec b)).bits
• div_bits (a b : F32) : (Float32.div a b).toBits = ((toIEEE32Exec a).div (toIEEE32Exec b)).bits
• neg_bits (a : F32) : (Float32.neg a).toBits = (toIEEE32Exec a).neg.bits
• sqrt_bits (a : F32) : (Float32.sqrt a).toBits = (toIEEE32Exec a).sqrt.bits
• isNaN_bits (a : F32) : Float32.isNaN a = (toIEEE32Exec a).isNaN
• isInf_bits (a : F32) : Float32.isInf a = (toIEEE32Exec a).isInf
• isFinite_bits (a : F32) : Float32.isFinite a = (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.RuntimeFloat32MatchesIEEE32Exec.toIEEE32Exec_add [RuntimeFloat32MatchesIEEE32Exec] (a b : F32) : toIEEE32Exec (a + b) = (toIEEE32Exec a).add (toIEEE32Exec b)

Rewrite runtime float32 addition into executable IEEE32Exec.add.

theorem TorchLean.Floats.IEEE754.Float32Bridge.RuntimeFloat32MatchesIEEE32Exec.toIEEE32Exec_sub [RuntimeFloat32MatchesIEEE32Exec] (a b : F32) : toIEEE32Exec (a - b) = (toIEEE32Exec a).sub (toIEEE32Exec b)

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

theorem TorchLean.Floats.IEEE754.Float32Bridge.RuntimeFloat32MatchesIEEE32Exec.toIEEE32Exec_mul [RuntimeFloat32MatchesIEEE32Exec] (a b : F32) : toIEEE32Exec (a * b) = (toIEEE32Exec a).mul (toIEEE32Exec b)

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

theorem TorchLean.Floats.IEEE754.Float32Bridge.RuntimeFloat32MatchesIEEE32Exec.toIEEE32Exec_div [RuntimeFloat32MatchesIEEE32Exec] (a b : F32) : toIEEE32Exec (a / b) = (toIEEE32Exec a).div (toIEEE32Exec b)

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

theorem TorchLean.Floats.IEEE754.Float32Bridge.RuntimeFloat32MatchesIEEE32Exec.toIEEE32Exec_neg [RuntimeFloat32MatchesIEEE32Exec] (a : F32) : toIEEE32Exec (-a) = (toIEEE32Exec a).neg

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

theorem TorchLean.Floats.IEEE754.Float32Bridge.RuntimeFloat32MatchesIEEE32Exec.toIEEE32Exec_sqrt [RuntimeFloat32MatchesIEEE32Exec] (a : F32) : toIEEE32Exec (Float32.sqrt a) = (toIEEE32Exec a).sqrt

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

theorem TorchLean.Floats.IEEE754.Float32Bridge.RuntimeFloat32MatchesIEEE32Exec.toIEEE32Exec_ofIEEE32Exec [RuntimeFloat32MatchesIEEE32Exec] (x : IEEE32Exec) : toIEEE32Exec (ofIEEE32Exec x) = x

Converting an IEEE32Exec value to runtime Float32 and back returns the original bits.