Skip to content

Trace Schema Reference

Purpose

The exported trace is not just a debug log. It is the structured contract between Python and Lean.

Python writes it. Lean parses it and verifies it.

If the schema drifts, verification will fail.

Current Version

The current schema version is:

  • traceVersion = 3

The Lean verifier rejects mismatched versions.

Top-Level Shape

An EpisodeTrace contains:

  • traceVersion
  • params
  • initialState
  • steps

params

Current fields:

  • batteryCapacity
  • chargeLimit
  • dischargeLimit
  • gridLimit
  • degradationPenalty

initialState

Current fields:

  • soc

Per-Step Shape

Each step contains:

  • state
  • signal
  • proposedAction
  • appliedAction
  • interventionReasons
  • interventionContext
  • nextState

state and nextState

Current fields:

  • soc

nextState must match the transition produced from appliedAction, not proposedAction.

signal

Current fields:

  • solar
  • load
  • buyPrice
  • sellPrice

All current signal values are expected to be non-negative.

proposedAction

Current fields:

  • batteryDelta

This is what the agent wanted to execute.

appliedAction

Current fields:

  • batteryDelta

This is what actually reached the environment after shield filtering.

If the proposed action was already valid, Lean expects proposedAction and appliedAction to match.

interventionReasons

This is a list of reason categories for why the shield intervened or why the action was already acceptable.

Current reason labels:

  • already_valid
  • charge_limit
  • discharge_limit
  • battery_bounds
  • grid_limit
  • unknown_invalid_action

interventionContext

This captures the numeric context for the proposed action.

Current fields:

  • proposedBatteryDelta
  • proposedNextSoc
  • proposedNetGrid
  • chargeLimit
  • dischargeLimit
  • batteryCapacity
  • gridLimit
  • socLowerMargin
  • socUpperMargin
  • gridLowerMargin
  • gridUpperMargin

Margin Semantics

The margin fields are signed distances to limits.

Examples:

  • socLowerMargin < 0 means the proposed next SoC would fall below zero
  • socUpperMargin < 0 means the proposed next SoC would exceed battery capacity
  • gridUpperMargin < 0 means the proposed net grid exchange would exceed the upper grid bound
  • gridLowerMargin < 0 means the proposed net grid exchange would exceed the lower grid bound

Negative margins are expected when the proposed action is invalid.

What Lean Verifies

The Lean verifier checks:

  • the trace version matches the supported schema
  • parameters are valid
  • the initial state is valid
  • each recorded state matches the expected running state
  • each signal is valid
  • the shield audit is consistent
  • intervention reasons match the proposed action
  • intervention context matches the proposed action
  • nextState matches the applied transition

Compatibility Rules

If you change any trace field names or meanings:

  1. update vpp_rl/model.py
  2. update VppLeanRl/Trace.lean
  3. update any related shield logic in VppLeanRl/Shield.lean
  4. update the tests in tests/test_vpp.py

Do not change one side only.

Relevant Files

  • vpp_rl/model.py
  • vpp_rl/env.py
  • vpp_rl/shield.py
  • VppLeanRl/Trace.lean
  • VppLeanRl/Shield.lean
  • tests/test_vpp.py