Gymnasium Trust-Boundary Wrappers (Proof Layer) #
NN.Runtime.RL.Gymnasium.Session.stepChecked returns a contract-validated transition, but the
runtime layer intentionally does not carry the Prop-level proof object in its return type.
This file provides a proof-layer wrapper that returns the same transition bundled with a proof
that it satisfies the Lean-side trust-boundary contract (Runtime.RL.Boundary.ContractHolds).
This is useful when you want a “checked preconditions” API: instead of assuming numeric/shape safety of externally collected rollouts, you explicitly check and obtain a usable hypothesis.
References:
- Gymnasium API docs (reset/step, terminated vs truncated): https://gymnasium.farama.org/
def
Runtime.RL.Gymnasium.Session.stepCheckedWithProof
{obsShape : Spec.Shape}
{nActions : ℕ}
(s : Session obsShape nActions)
(action : Fin nActions)
(resetOnDone : Bool := true)
:
Like stepChecked, but returns the transition bundled with a Prop-level proof that it satisfies
the client’s trust-boundary contract.