BridgeFP32Expr

Compositional refinement lemmas on top of NN/Floats/IEEEExec/BridgeFP32.lean.

In BridgeFP32.lean we prove refinement theorems one op at a time (add/mul/div/sqrt, etc.). In practice, though, we often want to talk about a whole scalar expression and not re-run the same “op-level” proof script at every node.

This file provides:

• a compact scalar expression language Expr, and
• an “all intermediates are finite” witness FiniteEval,

so we can state and prove a single theorem that looks like:

toReal (evalRuntime env e) = evalSpec (toReal ∘ env) e

where:

• evalRuntime evaluates the AST using the executable IEEE-754 kernel IEEE32Exec, and
• evalSpec evaluates the AST in ℝ, rounding after every operation using fp32Round.

This mirrors the standard mathematical model of float32 evaluation: compute the real operation, then round-to-float32 at each node, provided we stay on the finite path (no NaNs/Infs, no division by zero, no overflow).

References / background (for the rounding model itself, not this AST wrapper):

• IEEE 754-2019: https://doi.org/10.1109/IEEESTD.2019.8766229
• Goldberg (1991): https://doi.org/10.1145/103162.103163
• Flocq (Boldo–Melquiond, 2011): https://doi.org/10.1109/ARITH.2011.40

A small scalar expression language

Expr is a small, scalar-only AST. TorchLean's main IRs live elsewhere; this wrapper exists to state expression-level refinement theorems for straight-line float32 computations.

inductive TorchLean.Floats.IEEE754.IEEE32Exec.Expr : Type

A compact AST for scalar float32 expressions evaluated using IEEE32Exec.

• var : ℕ → Expr
• const : IEEE32Exec → Expr
• add : Expr → Expr → Expr
• sub : Expr → Expr → Expr
• mul : Expr → Expr → Expr
• div : Expr → Expr → Expr
• fma : Expr → Expr → Expr → Expr
• sqrt : Expr → Expr

@[implicit_reducible]

instance TorchLean.Floats.IEEE754.IEEE32Exec.instReprExpr : Repr Expr

def TorchLean.Floats.IEEE754.IEEE32Exec.instReprExpr.repr : Expr → ℕ → Std.Format

def TorchLean.Floats.IEEE754.IEEE32Exec.evalRuntime (env : ℕ → IEEE32Exec) : Expr → IEEE32Exec

Evaluate an Expr using the executable float32 kernel (IEEE32Exec).

def TorchLean.Floats.IEEE754.IEEE32Exec.evalSpec (env : ℕ → ℝ) : Expr → ℝ

Real semantics for the compact scalar expression language.

"Finite evaluation" witnesses (finite at every intermediate node)

BridgeFP32.lean is explicit about the trust boundary: it bridges only the finite behavior of IEEE32Exec to FP32. For expression-level statements, we therefore need an assumption that every intermediate evaluation remains finite.

FiniteEval env e d is a proof object that says:

• evaluating e under env is finite, and
• its decoded dyadic value is d.

We store the dyadic because it gives us a convenient “finiteness certificate”: toDyadic? x = some d immediately rules out NaN/Inf and unlocks the op-level bridge lemmas.

inductive TorchLean.Floats.IEEE754.IEEE32Exec.FiniteEval (env : ℕ → IEEE32Exec) : Expr → Dyadic → Prop

Finite-evaluation witness for the compact scalar expression language.

• var {env : ℕ → IEEE32Exec} (i : ℕ) (d : Dyadic) (h : (env i).toDyadic? = some d) : FiniteEval env (Expr.var i) d
• const {env : ℕ → IEEE32Exec} (x : IEEE32Exec) (d : Dyadic) (h : x.toDyadic? = some d) : FiniteEval env (Expr.const x) d
• add {env : ℕ → IEEE32Exec} {a b : Expr} {da db dout : Dyadic} (ha : FiniteEval env a da) (hb : FiniteEval env b db) (hout : ((evalRuntime env a).add (evalRuntime env b)).toDyadic? = some dout) : FiniteEval env (a.add b) dout
• sub {env : ℕ → IEEE32Exec} {a b : Expr} {da db dout : Dyadic} (ha : FiniteEval env a da) (hb : FiniteEval env b db) (hout : ((evalRuntime env a).sub (evalRuntime env b)).toDyadic? = some dout) : FiniteEval env (a.sub b) dout
• mul {env : ℕ → IEEE32Exec} {a b : Expr} {da db dout : Dyadic} (ha : FiniteEval env a da) (hb : FiniteEval env b db) (hout : ((evalRuntime env a).mul (evalRuntime env b)).toDyadic? = some dout) : FiniteEval env (a.mul b) dout
• div {env : ℕ → IEEE32Exec} {a b : Expr} {da db dout : Dyadic} (ha : FiniteEval env a da) (hb : FiniteEval env b db) (hden : db.mant ≠ 0) (hout : ((evalRuntime env a).div (evalRuntime env b)).toDyadic? = some dout) : FiniteEval env (a.div b) dout
• fma {env : ℕ → IEEE32Exec} {a b c : Expr} {da db dc dout : Dyadic} (ha : FiniteEval env a da) (hb : FiniteEval env b db) (hc : FiniteEval env c dc) (hout : ((evalRuntime env a).fma (evalRuntime env b) (evalRuntime env c)).toDyadic? = some dout) : FiniteEval env (a.fma b c) dout
• sqrt {env : ℕ → IEEE32Exec} {a : Expr} {da dout : Dyadic} (ha : FiniteEval env a da) (hout : (evalRuntime env a).sqrt.toDyadic? = some dout) : FiniteEval env a.sqrt dout

theorem TorchLean.Floats.IEEE754.IEEE32Exec.FiniteEval.toDyadic? {env : ℕ → IEEE32Exec} {e : Expr} {d : Dyadic} : FiniteEval env e d → (evalRuntime env e).toDyadic? = some d

Extract the decoded dyadic of the runtime evaluation from a FiniteEval witness.

Whole-expression refinement

This is the main result of the file: a compositional refinement theorem that follows the AST AST shape and invokes the corresponding op-level bridge theorem at each node.

If you are thinking in PyTorch terms: Expr is a compact “forward graph”, and the result says that the executable float32 evaluation agrees with the standard float32 mathematical model (real arithmetic + rounding) on the finite path.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_evalRuntime_eq_evalSpec (env : ℕ → IEEE32Exec) {e : Expr} {d : Dyadic} : FiniteEval env e d → (evalRuntime env e).toReal = evalSpec (fun (i : ℕ) => (env i).toReal) e

Main expression-level refinement theorem for IEEEExec.