Gymnasium Bridge (Session)

Stepping an external Gymnasium environment yields only the next observation. To validate a full Gym-style transition we need both:

• observation before the action, and
• nextObservation after the action.

Session stores the last observation so stepChecked can return a fully-observed, contract-checked transition (Runtime.RL.Boundary.Transition).

This is the main entry point used by executable RL workflows: it is small, typed, and keeps trust-boundary validation in one place.

References:

• Gymnasium API docs (reset/step, terminated vs truncated): https://gymnasium.farama.org/
• The original Gym API paper (background on the env interface): https://arxiv.org/abs/1606.01540
• Trust-boundary contract definition: NN.Runtime.RL.Boundary.

Stateful session (validated transitions)

structure Runtime.RL.Gymnasium.Session (obsShape : Spec.Shape) (nActions : ℕ) : Type

Stateful Gymnasium session that stores the most recent observation.

This is the state required to emit a fully observed transition on each step.

• client : Client obsShape nActions

  Subprocess client used to communicate with Python Gymnasium.

• observation : Spec.Tensor Float obsShape

  Current observation (the one to be used as observation on the next step).

def Runtime.RL.Gymnasium.Session.start {obsShape : Spec.Shape} {nActions : ℕ} (client : Client obsShape nActions) (seed? : Option ℕ := none) : IO (Session obsShape nActions)

Create a session by resetting the environment once.

def Runtime.RL.Gymnasium.Session.withSession {α : Type} {obsShape : Spec.Shape} {nActions : ℕ} (serverScript envId : String) (contract : Boundary.Contract obsShape nActions) (seed? : Option ℕ := none) (k : Session obsShape nActions → IO α) : IO α

Spawn a client + start a session, ensuring the subprocess is closed after k returns.

def Runtime.RL.Gymnasium.Session.reset {obsShape : Spec.Shape} {nActions : ℕ} (s : Session obsShape nActions) (seed? : Option ℕ := none) : IO (Session obsShape nActions)

Reset and replace the stored observation.

def Runtime.RL.Gymnasium.Session.stepChecked {obsShape : Spec.Shape} {nActions : ℕ} (s : Session obsShape nActions) (action : Fin nActions) (resetOnDone : Bool := true) : IO (Boundary.Transition obsShape nActions × Session obsShape nActions)

Step once, validate against the trust-boundary contract, and optionally auto-reset on done.

resetOnDone=true is convenient for fixed-horizon rollouts where we want to keep collecting even across episode boundaries.

def Runtime.RL.Gymnasium.Session.close {obsShape : Spec.Shape} {nActions : ℕ} (s : Session obsShape nActions) : IO Unit

Close the underlying client/subprocess.