Runtime Checked Preconditions → Float32 Semantics Theorems #
NN.Proofs.RL.Floats.IEEE32Exec proves refinement theorems for RL formulas in the executable
ExecFloat.Binary 8 23 float32 semantics, but those theorems are intentionally stated with explicit
isFinite … = true hypotheses for each intermediate.
In the runtime layer, TorchLean typically enforces these hypotheses by checked preconditions:
Runtime.RL.Numerics.Float32.*Checked returns Except String … and fails fast if any
intermediate becomes NaN/Inf.
This file is the glue: it turns “the runtime checker returned .ok” into the proof hypotheses
needed by the refinement theorem, yielding a user-facing statement:
checked boundary ⇒ theorem applies.
References:
- IEEE 754-2019 (binary32 arithmetic): https://doi.org/10.1109/IEEESTD.2019.8766229
- Goldberg, “What Every Computer Scientist Should Know About Floating-Point Arithmetic” (1991): https://doi.org/10.1145/103162.103163
If Runtime.RL.Numerics.Float32.discountedBackupChecked returns .ok, then the decoded real
meaning of the result agrees with the standard “real-op + round-to-float32” model (fp32Round)
at each primitive operation.
This is the direct checked boundary ⇒ semantics theorem applies wrapper.
If Runtime.RL.Numerics.Float32.tdResidualChecked returns .ok, then the decoded real meaning of
the result agrees with the standard “real-op + round-to-float32” model (fp32Round) at each
primitive operation.
This is the checked boundary ⇒ semantics theorem applies wrapper for TD residuals.