Scalar expression refinement #

toReal_evalRuntime_eq_evalSpec composes FloatLib's arithmetic refinement results along an Expr tree. evalRuntime uses encoded binary32 operations; evalSpec rounds each real operation with Model.roundAt FloatFormat.binary32. Fused multiply-add rounds once, not after its product.

The theorem requires a FiniteEval witness for every intermediate result, including finite leaves and a nonzero divisor. Subnormals and underflow to zero are allowed. The decoded real equality does not distinguish signed zeros or establish native CPU/GPU kernel correspondence.

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.

source

inductive TorchLean.Floats.IEEE754.IEEE32Exec.Expr :

Type

A compact AST for scalar float32 expressions evaluated using ExecFloat.Binary 8 23.

var : ℕ → Expr
const : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) _proof_1 _proof_2 _proof_3 _proof_4 → 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

Instances For

source

def TorchLean.Floats.IEEE754.IEEE32Exec.instReprExpr.repr :

Expr → ℕ → Std.Format

Instances For

source

@[instance_reducible]

instance TorchLean.Floats.IEEE754.IEEE32Exec.instReprExpr :

Repr Expr

source

def TorchLean.Floats.IEEE754.IEEE32Exec.evalRuntime (env : ℕ → FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) Expr._proof_1 Expr._proof_2 Expr._proof_3 Expr._proof_4) :

Expr → FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) Expr._proof_1 Expr._proof_2 Expr._proof_3 Expr._proof_4

Evaluate an Expr using the executable float32 kernel (ExecFloat.Binary 8 23).

Instances For

source

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

Expr → ℝ

Real semantics for the compact scalar expression language.

Instances For

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

The arithmetic adapter bridges finite ExecFloat.Binary 8 23 behavior to binary32 rounding on the reals. For expression-level statements, every intermediate evaluation must remain finite.

FiniteEval env e d records the result's decoded dyadic d and finite-evaluation witnesses for every subtree. A successful toDyadic? observation rules out NaN and infinity.

source