Trace Schema 参考

作用

trace 不是普通日志，而是 Python 和 Lean 之间的结构化契约。

• Python 负责导出
• Lean 负责解析和验证

如果 schema 漂移，Lean verifier 会直接失败。

当前版本

• traceVersion = 3

顶层结构

EpisodeTrace 当前包含：

• traceVersion
• params
• initialState
• steps

每一步包含什么

每个 step 当前包含：

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

proposedAction 和 appliedAction

• proposedAction：agent 原本想执行的动作
• appliedAction：shield 处理后真正进入环境的动作

如果 proposed action 本身合法，Lean 会要求两者一致。

interventionReasons

当前可能包括：

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

interventionContext

当前字段包括：

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

margin 字段怎么理解

• 正值：还没碰到边界
• 负值：已经越界

例如：

• socLowerMargin < 0：proposed next SoC 会低于 0
• gridUpperMargin < 0：proposed net grid 会超过上边界

Lean 当前会检查什么

• trace version 是否匹配
• 参数是否合法
• 初始状态是否合法
• 每一步状态是否和运行中的期望状态一致
• 信号是否合法
• shield 审计是否一致
• intervention reasons 是否一致
• intervention context 是否一致
• nextState 是否由 appliedAction 推导

相关文件

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