Checked Float32 PPO Objective Helpers

PPO is usually run with ordinary host floats, but these helpers make the scalar objective pieces executable under the explicit ExecFloat.Binary 8 23 model and reject non-finite intermediates. They are useful for regression tests, debugging numerically fragile runs, and connecting runtime checks to proof layer finite hypotheses.

Reference: Schulman et al., "Proximal Policy Optimization Algorithms" (2017).

def Runtime.RL.Numerics.Float32.importanceRatioChecked (newLogProb oldLogProb : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) importanceRatioChecked._proof_1 importanceRatioChecked._proof_2 importanceRatioChecked._proof_3 importanceRatioChecked._proof_4) : Except String (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) importanceRatioChecked._proof_1 importanceRatioChecked._proof_2 importanceRatioChecked._proof_3 importanceRatioChecked._proof_4)

Checked importance ratio exp(newLogProb - oldLogProb), specialized to ExecFloat.Binary 8 23.

This is the float32-semantics variant of Runtime.RL.PolicyGradient.ratio.

def Runtime.RL.Numerics.Float32.ppoClippedObjectiveFromRatioChecked (ratio advantage clipEps : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) importanceRatioChecked._proof_1 importanceRatioChecked._proof_2 importanceRatioChecked._proof_3 importanceRatioChecked._proof_4) : Except String (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) importanceRatioChecked._proof_1 importanceRatioChecked._proof_2 importanceRatioChecked._proof_3 importanceRatioChecked._proof_4)

Checked PPO clipped surrogate objective from a precomputed importance ratio:

min(ratio * A, clip(ratio, 1-ε, 1+ε) * A).

This avoids re-doing the softmax/log-prob computation when you already have ratios.

Reference:

• Schulman et al., "Proximal Policy Optimization Algorithms" (2017): https://arxiv.org/abs/1707.06347