Checked Float32 Discounted Returns

This module contains the value-learning recurrences that need explicit finite-intermediate checks: discounted backups and fixed-horizon discounted returns. The public names stay in Runtime.RL.Numerics.Float32; this file only separates the implementation so the runtime tree is easier to audit.

Reference: Sutton and Barto, Reinforcement Learning: An Introduction.

Checked RL core transforms (configured binary32)

def Runtime.RL.Numerics.Float32.requireFinite (label : String) (x : Float32Exec) : Except String Unit

Require that an ExecFloat.Binary 8 23 value is finite, producing a tagged error on failure.

Checked configured binary32 primitives

The checked RL helpers below are intentionally written in terms of a few small “checked primitive” combinators (checkedAdd, checkedMul, …). Larger routines (GAE, PPO objectives, …) remain readable while still producing precise error locations when non-finite values occur.

Exponential and logarithm use FloatLib's configured deterministic approximations. Their checks reject nonfinite results; they do not certify correct rounding or a real-error bound.

def Runtime.RL.Numerics.Float32.checkedAdd (label : String) (x y : Float32Exec) : Except String Float32Exec

Checked configured binary32 addition.

def Runtime.RL.Numerics.Float32.checkedSub (label : String) (x y : Float32Exec) : Except String Float32Exec

Checked configured binary32 subtraction.

def Runtime.RL.Numerics.Float32.checkedMul (label : String) (x y : Float32Exec) : Except String Float32Exec

Checked configured binary32 multiplication.

def Runtime.RL.Numerics.Float32.checkedDiv (label : String) (x y : Float32Exec) : Except String Float32Exec

Checked configured binary32 division.

def Runtime.RL.Numerics.Float32.checkedExp (label : String) (x : Float32Exec) : Except String Float32Exec

Approximate eˣ in binary32 and reject a nonfinite result.

def Runtime.RL.Numerics.Float32.checkedLog (label : String) (x : Float32Exec) : Except String Float32Exec

Approximate the natural logarithm in binary32 and reject a nonfinite result.

def Runtime.RL.Numerics.Float32.checkedSqrt (label : String) (x : Float32Exec) : Except String Float32Exec

Checked configured binary32 square root.

def Runtime.RL.Numerics.Float32.checkedMin (label : String) (x y : Float32Exec) : Except String Float32Exec

Checked configured binary32 min using IEEE-754 minimum.

def Runtime.RL.Numerics.Float32.checkedMax (label : String) (x y : Float32Exec) : Except String Float32Exec

Checked configured binary32 max using IEEE-754 maximum.

def Runtime.RL.Numerics.Float32.discountedBackupChecked (reward gamma bootstrap : Float32Exec) (done : Bool) : Except String Float32Exec

Checked version of the one-step discounted backup

reward + γ * (1-done) * bootstrap

specialized to ExecFloat.Binary 8 23.

The runtime return type is Except String … so training code can choose to:

• fail fast, or
• fall back to a safer scalar backend (interval/oracle), or
• log and skip a bad sample.

Checked preconditions → proof hypotheses

The NN/Proofs/RL/Floats/* bridge theorems for ExecFloat.Binary 8 23 are usually stated with explicit isFinite … = true hypotheses for each intermediate.

The lemma below is the glue between runtime safety checks and those proof hypotheses:

If the checked routine returns .ok, then all the finiteness side-conditions needed by the semantic bridge theorems hold automatically.

theorem Runtime.RL.Numerics.Float32.discountedBackup_eq_ok (reward gamma bootstrap : Float32Exec) (done : Bool) (out : Float32Exec) (h : discountedBackupChecked reward gamma bootstrap done = Except.ok out) : FloatLib.Floats.ExecFloat.Binary.isFinite (FloatLib.Floats.ExecFloat.mul gamma (Spec.RL.continueMask done)) = true ∧ FloatLib.Floats.ExecFloat.Binary.isFinite ((FloatLib.Floats.ExecFloat.mul gamma (Spec.RL.continueMask done)).mul bootstrap) = true ∧ FloatLib.Floats.ExecFloat.Binary.isFinite (FloatLib.Floats.ExecFloat.add reward ((FloatLib.Floats.ExecFloat.mul gamma (Spec.RL.continueMask done)).mul bootstrap)) = true ∧ out = Spec.RL.discountedBackup reward gamma bootstrap done

If discountedBackupChecked returns .ok out, then:

• every configured binary32 intermediate used by the refinement theorem is finite, and
• out agrees with the spec-layer discountedBackup formula.

def Runtime.RL.Numerics.Float32.discountedReturnsChecked {n : ℕ} (gamma : Float32Exec) (rewards : TorchLean.Tensor Float32Exec [n]) (bootstrap : Float32Exec := 0) : Except String (TorchLean.Tensor Float32Exec [n])

Checked fixed-horizon discounted returns (no done flags), specialized to ExecFloat.Binary 8 23.

This is the checked/finite counterpart to Runtime.RL.Core.discountedReturnsFrom.