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 (IEEE32Exec)

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

Require that an IEEE32Exec value is finite, producing a tagged error on failure.

Checked IEEE32Exec primitives

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

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

Checked IEEE32Exec addition.

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

Checked IEEE32Exec subtraction.

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

Checked IEEE32Exec multiplication.

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

Checked IEEE32Exec division.

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

Checked IEEE32Exec exponentiation (base-e).

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

Checked IEEE32Exec logarithm (natural log).

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

Checked IEEE32Exec square root.

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

Checked IEEE32Exec min using IEEE-754 minimum.

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

Checked IEEE32Exec max using IEEE-754 maximum.

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

Checked version of the one-step discounted backup

reward + γ * (1-done) * bootstrap

specialized to IEEE32Exec.

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 IEEE32Exec 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.discountedBackupIEEE32ExecChecked_eq_ok (reward gamma bootstrap : Float32Exec) (done : Bool) (out : Float32Exec) (h : discountedBackupIEEE32ExecChecked reward gamma bootstrap done = Except.ok out) : (TorchLean.Floats.IEEE754.IEEE32Exec.mul gamma (Spec.RL.continueMask done)).isFinite = true ∧ ((TorchLean.Floats.IEEE754.IEEE32Exec.mul gamma (Spec.RL.continueMask done)).mul bootstrap).isFinite = true ∧ (TorchLean.Floats.IEEE754.IEEE32Exec.add reward ((TorchLean.Floats.IEEE754.IEEE32Exec.mul gamma (Spec.RL.continueMask done)).mul bootstrap)).isFinite = true ∧ out = Spec.RL.discountedBackup reward gamma bootstrap done

If discountedBackupIEEE32ExecChecked returns .ok out, then:

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

def Runtime.RL.Numerics.Float32.discountedReturnsVecFromIEEE32ExecChecked {n : ℕ} (gamma : Float32Exec) (rewards : Spec.Tensor Float32Exec (Spec.Shape.dim n Spec.Shape.scalar)) (bootstrap : Float32Exec := 0) : Except String (Spec.Tensor Float32Exec (Spec.Shape.dim n Spec.Shape.scalar))

Checked fixed-horizon discounted returns (no done flags), specialized to IEEE32Exec.

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