VPP Lean RL User Manual¶

Related entry points:

Who This Manual Is For¶

This manual is written for three groups:

Beginners who want to run the project and understand the main workflow
Engineers who want to modify, extend, and debug the codebase
Research scientists who want a reproducible scaffold for RL + formal methods experiments

If you only want the shortest onboarding path, start with:

1. What This Project Is¶

VPP Lean RL is a lightweight research scaffold that integrates:

Lean 4 for formal constraints and trace verification
Python for RL training and simulation
a simplified virtual power plant model with battery, solar, load, and grid exchange

The current codebase is intentionally small and deterministic. The goal is not to ship a production-grade VPP controller. The goal is to provide a runnable, inspectable, and extensible foundation for experiments in safe RL and formal verification.

2. What You Can Use It For¶

Train tabular RL baselines on deterministic VPP scenarios
Compare different algorithms and operating scenarios
Apply an online safety shield before actions hit the environment
Export Lean-derived shield rule tables for Python to consume
Generate auditable rollout traces
Verify those traces in Lean against state, action, grid, and shield-audit constraints

3. What It Does Not Try To Be¶

This project is not:

a production EMS or DERMS platform
a deep RL framework
a multi-site market bidding engine
a proof system for policy optimality

Treat it as a research and engineering scaffold, not as an operational control system.

4. Requirements¶

4.1 Required Tooling¶

Lean 4
Lake
Python >= 3.11

Declared in:

lean-toolchain
pyproject.toml

4.2 First Commands To Run¶

lake build
python3 -m unittest discover -s tests

If both commands pass, the Lean and Python sides are wired correctly.

5. Quick Start¶

5.1 Inspect Supported Options¶

python3 -m vpp_rl.train --list-scenarios
python3 -m vpp_rl.train --list-algorithms

Current scenarios:

default
peak_shaving
solar_export
stress_test

Current algorithms:

q_learning
sarsa
double_q

5.2 Run the Full Demo¶

./scripts/run_demo.sh 180 double_q peak_shaving table_project

This script will:

train an agent
export a trace
verify the trace in Lean

5.3 Run the Workflow Step by Step¶

Export a Lean rule table:

python3 -m vpp_rl.rule_table \
  --scenario peak_shaving \
  --output artifacts/peak_shaving_shield_table.json

Train and export a trace:

python3 -m vpp_rl.train \
  --episodes 180 \
  --algorithm double_q \
  --scenario peak_shaving \
  --shield-mode table_project \
  --shield-table artifacts/peak_shaving_shield_table.json \
  --output artifacts/peak_shaving_double_q_table_project_trace.json

Verify the trace in Lean:

lake env lean --run VppLeanRl/Cli.lean -- \
  artifacts/peak_shaving_double_q_table_project_trace.json

6. Repository Map¶

6.1 Lean Modules¶

VppLeanRl/Domain.lean: formal definitions of parameters, states, signals, actions, transitions, and validity
VppLeanRl/Parameters.lean: parameter well-formedness lemmas
VppLeanRl/Safety.lean: safety lemmas derived from action validity and state preservation
VppLeanRl/SignalFacts.lean: non-negativity lemmas for signal values
VppLeanRl/Shield.lean: online shield contract and audit consistency checks
VppLeanRl/RuleTable.lean: Lean-side rule-table generator
VppLeanRl/RuleTableCli.lean: CLI for exporting rule tables
VppLeanRl/Trace.lean: trace verifier
VppLeanRl/Cli.lean: verifier CLI entry point

6.2 Python Modules¶

vpp_rl/model.py: shared domain model and trace schema
vpp_rl/env.py: environment, scenario factory, reward logic, trace recording
vpp_rl/agent.py: tabular RL algorithms
vpp_rl/shield.py: online safety filter
vpp_rl/rule_table.py: Python-side rule-table export and loading helpers
vpp_rl/train.py: training and evaluation entry point

6.3 Tests and Scripts¶

tests/test_vpp.py: unit and integration tests
scripts/run_demo.sh: one-command demo workflow

7. Core Concepts¶

7.1 Scenario¶

A scenario defines:

battery parameters
24 hourly signal curves
initial state of charge

All built-in scenarios are deterministic by design so behavior is easier to compare and verification is easier to reproduce.

7.2 Action¶

The current action space is a discrete battery power action represented by batteryDelta.

In most scenarios the available deltas are:

-control_step
0
+control_step

7.3 Observation¶

The current agent uses a tabular observation key:

(time_index, soc)

7.4 Reward¶

The environment computes a cost, then returns:

reward = -cost

The cost includes:

grid import cost
grid export revenue
battery degradation penalty

7.5 Algorithm¶

Current built-in algorithms:

q_learning
sarsa
double_q

If you want the most useful baseline out of the box, start with double_q.

7.6 Shield Mode¶

Current shield modes:

none
project
table_project

table_project is the most complete integration path because it uses a Lean-derived rule table at runtime.

7.7 Rule Table¶

A rule table is a JSON artifact generated by Lean. For each (timeIndex, soc) pair it stores:

the valid action indices
the projected action index for each proposed action

This lets Python use Lean-derived constraints without recomputing them online.

7.8 Trace¶

The environment exports an EpisodeTrace that serves two roles:

a runtime artifact
the input contract for the Lean verifier

The current schema is versioned:

traceVersion = 3

Each step records:

state
signal
proposedAction
appliedAction
interventionReasons
interventionContext
nextState

7.9 Proposed vs Applied Actions¶

proposedAction: what the policy wanted to execute
appliedAction: what actually reached the environment after shielding

If the proposed action was already valid, Lean expects both actions to match.

7.10 Intervention Reasons and Context¶

interventionReasons explains why a proposed action was changed.

Examples:

already_valid
charge_limit
discharge_limit
battery_bounds
grid_limit

interventionContext stores the numeric context behind that decision, including:

proposed battery delta
proposed next SoC
proposed net grid exchange
active limits
boundary margins

Margin values may be negative. That is intentional: negative values indicate a proposed action would violate a boundary.

8. For Beginners¶

Use this path:

run ./scripts/run_demo.sh 180 double_q peak_shaving table_project
inspect the generated JSON trace in artifacts/
run the Lean verifier manually once
switch one variable at a time: scenario, algorithm, or shield mode

At this stage you do not need to understand Lean proof details or RL tuning internals. The main thing to understand is the end-to-end chain:

train -> trace -> Lean verification

9. For Engineers¶

9.1 Main Execution Path¶

The main runtime path lives in vpp_rl/train.py:

build an environment from scenario
build an agent from algorithm
build a shield from shield_mode
train the agent
run a greedy rollout
export a trace
verify the trace in Lean

9.2 Where To Extend¶

Add a new scenario in vpp_rl/env.py:

create a new ScenarioDefinition
register it in SCENARIOS
expose it through available_scenarios()

Add a new algorithm in vpp_rl/agent.py:

create a new TabularAgent subclass
implement policy_values()
implement update()
register it in build_agent()

Add a new shield mode in vpp_rl/shield.py:

keep ShieldDecision intact
preserve proposedAction, appliedAction, interventionReasons, and interventionContext

If you break that contract, the Lean-side audit path will break.

9.3 Trace Schema Discipline¶

The trace is not just a debug log. It is a cross-language contract between Python and Lean.

If you change the schema:

update Python export logic
update Lean JSON parsing
update verification logic
update tests

The relevant files are:

vpp_rl/model.py
VppLeanRl/Trace.lean

9.4 Recommended Debugging Order¶

When something breaks, debug in this order:

python3 -m unittest discover -s tests
lake build
python3 -m vpp_rl.train ...
lake env lean --run VppLeanRl/Cli.lean -- <trace>
inspect the trace JSON directly

10. For Research Scientists¶

10.1 Useful Research Questions¶

This scaffold is a good fit for:

RL with formal constraints
online safety filtering for control
auditable safe-action pipelines
Lean-assisted safety verification of learned controllers
controlled comparisons across scenarios and algorithms

10.2 Suggested Experiment Matrix¶

Compare at least these axes:

scenarios: default, peak_shaving, solar_export, stress_test
algorithms: q_learning, sarsa, double_q
shield modes: none, project, table_project

10.3 Metrics To Track¶

Already available from the current codebase:

training_reward
greedy_reward
idle_reward
improvement
shield_interventions
trace length
intervention reasons
violation margins from interventionContext

For more rigorous studies, also track:

mean and variance across seeds
convergence behavior
intervention frequency ratio
intervention category distribution
reward deltas with and without shielding

10.4 Reproducibility Advice¶

For reproducible experiments, fix:

scenario
algorithm
episodes
seed
shield_mode
shield_table
traceVersion

If you change battery parameters, actions, or signal curves, regenerate the rule table instead of reusing an old one.

10.5 Current Research Boundaries¶

Be explicit about these limits:

deterministic environments
tabular algorithms only
simplified single-site VPP model
safety and audit verification, not policy-optimality proofs

11. Command Reference¶

Build and test:

lake build
python3 -m unittest discover -s tests

List scenarios and algorithms:

python3 -m vpp_rl.train --list-scenarios
python3 -m vpp_rl.train --list-algorithms

Generate a rule table:

python3 -m vpp_rl.rule_table \
  --scenario peak_shaving \
  --output artifacts/peak_shaving_shield_table.json