RL Trust Boundary JSON Loader

This module contains the JSON-lines/interchange side of the RL trust boundary. The contract itself lives in NN.Runtime.RL.Boundary.Core; this file only explains how to parse a small Python-friendly rollout schema and immediately validate it against that contract.

Keeping JSON separate matters because proof files usually need the contract/checker semantics, not the parser or PyTorch import layer. Runtime bridges can import this file when they need external rollout loading.

JSON loading (one simple interchange format)

We provide a small JSON schema that is easy to emit from Python:

{
  "transitions": [
    {
      "obs": <nested arrays matching obsShape>,
      "action": <nat>,
      "reward": <float>,
      "terminated": <bool>,
      "truncated": <bool>,
      "next_obs": <nested arrays matching obsShape>
    },
    ...
  ]
}

This is one supported integration path, using a practical “lowest common denominator” that is easy to diff and validate.

JSON Primitive Parsers

These are small helpers used by the trust-boundary JSON loader and by runtime bridges (e.g. a Gymnasium subprocess client).

They return Except String ... so they can be used from both pure loaders and IO code that wants to convert errors into IO.userError.

def Runtime.RL.Boundary.parseNatStrict (j : Lean.Json) : Except String ℕ

Parse a JSON number as a nonnegative integer.

This is strict: it rejects non-integers (e.g. 1.5) and rejects numbers not exactly representable as an integer when converted through Float.

def Runtime.RL.Boundary.parseBool (field : String) (j : Lean.Json) : Except String Bool

Parse a boolean field from JSON.

def Runtime.RL.Boundary.parseFloat (field : String) (j : Lean.Json) : Except String Float

Parse a numeric field from JSON as a host Float.

def Runtime.RL.Boundary.parseTensorE (field : String) (s : Spec.Shape) (j : Lean.Json) : Except String (Spec.Tensor Float s)

Parse a JSON value as a typed tensor of shape s.

This relies on TorchLean's JSON tensor encoding used by Python bridges.

def Runtime.RL.Boundary.parseTransitionJson {obsShape : Spec.Shape} {nActions : ℕ} (c : Contract obsShape nActions) (j : Lean.Json) : Except String (Transition obsShape nActions)

Parse a single transition object using the schema described above.

def Runtime.RL.Boundary.loadRollout {obsShape : Spec.Shape} {nActions : ℕ} (path : String) (c : Contract obsShape nActions) : IO (Array (Transition obsShape nActions))

Load and validate a rollout file, returning an array of typed transitions.

def Runtime.RL.Boundary.loadRolloutAll {obsShape : Spec.Shape} {nActions : ℕ} (path : String) (c : Contract obsShape nActions) : IO (Array (Except String (Transition obsShape nActions)))

Load a rollout file and validate every transition, returning per-transition results.

Unlike loadRollout, this function does not stop at the first bad transition. Instead it returns an array aligned with the input JSON transitions array:

• ok t means the transition decoded and passed the contract check.
• error msg means decoding or contract checking failed for that transition.

This is useful for widget-style debugging where users want to see a summary of violations rather than only the first failure.