Runtime Checked Preconditions → Float32 Semantics Theorems

NN.Proofs.RL.Floats.IEEE32Exec proves refinement theorems for RL formulas in the executable IEEE32Exec 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

theorem Proofs.RL.Float32Exec.toReal_discountedBackupIEEE32ExecChecked_eq_fp32Round_chain (reward gamma bootstrap : TorchLean.Floats.IEEE754.IEEE32Exec) (done : Bool) (out : TorchLean.Floats.IEEE754.IEEE32Exec) (h : Runtime.RL.Numerics.Float32.discountedBackupIEEE32ExecChecked reward gamma bootstrap done = Except.ok out) : out.toReal = TorchLean.Floats.IEEE754.IEEE32Exec.fp32Round (reward.toReal + TorchLean.Floats.IEEE754.IEEE32Exec.fp32Round (TorchLean.Floats.IEEE754.IEEE32Exec.fp32Round (gamma.toReal * (Spec.RL.continueMask done).toReal) * bootstrap.toReal))

If Runtime.RL.Numerics.Float32.discountedBackupIEEE32ExecChecked 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 most users want.

theorem Proofs.RL.Float32Exec.toReal_tdResidualIEEE32ExecChecked_eq_fp32Round_chain (value reward gamma nextValue : TorchLean.Floats.IEEE754.IEEE32Exec) (done : Bool) (out : TorchLean.Floats.IEEE754.IEEE32Exec) (h : Runtime.RL.Numerics.Float32.tdResidualIEEE32ExecChecked value reward gamma nextValue done = Except.ok out) : out.toReal = TorchLean.Floats.IEEE754.IEEE32Exec.fp32Round (TorchLean.Floats.IEEE754.IEEE32Exec.fp32Round (reward.toReal + TorchLean.Floats.IEEE754.IEEE32Exec.fp32Round (TorchLean.Floats.IEEE754.IEEE32Exec.fp32Round (gamma.toReal * (Spec.RL.continueMask done).toReal) * nextValue.toReal)) - value.toReal)

If Runtime.RL.Numerics.Float32.tdResidualIEEE32ExecChecked 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.