telltale_lean_bridge/
sim_reference.rs

1//! Lean reference simulator bridge payloads.
2
3use serde::{Deserialize, Serialize};
4use serde_json::Value;
5use std::collections::BTreeMap;
6
7use crate::vm_runner::VmTraceEvent;
8
9/// Input payload for Lean reference simulation.
10#[derive(Debug, Clone, Serialize, Deserialize)]
11pub struct SimRunInput {
12    /// Schema version for this payload.
13    #[serde(default = "crate::schema::default_schema_version")]
14    pub schema_version: String,
15    /// Scenario configuration payload.
16    pub scenario: Value,
17    /// Global type payload.
18    pub global_type: Value,
19    /// Local type payloads keyed by role.
20    pub local_types: BTreeMap<String, Value>,
21    /// Initial role state payloads keyed by role.
22    #[serde(default)]
23    pub initial_states: BTreeMap<String, Vec<Value>>,
24}
25
26/// Output payload from Lean reference simulation.
27#[derive(Debug, Clone, Serialize, Deserialize)]
28pub struct SimRunOutput {
29    /// Schema version for this payload.
30    #[serde(default = "crate::schema::default_schema_version")]
31    pub schema_version: String,
32    /// Observable trace produced by the simulation.
33    #[serde(default)]
34    pub trace: Vec<VmTraceEvent>,
35    /// Property violations emitted by Lean reference checks.
36    #[serde(default)]
37    pub violations: Vec<Value>,
38    /// Optional operation-specific artifacts.
39    #[serde(default)]
40    pub artifacts: Value,
41}
42
43/// Structured simulation validation error.
44#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq)]
45pub struct SimulationStructuredError {
46    /// Stable Lean-side error code.
47    pub code: String,
48    /// Optional path to the failing payload segment.
49    #[serde(default)]
50    pub path: Option<String>,
51    /// Human-readable diagnostic message.
52    pub message: String,
53}
54
55/// Result payload from `validateSimulationTrace` operation.
56#[derive(Debug, Clone, Serialize, Deserialize)]
57pub struct SimTraceValidation {
58    /// Whether validation succeeded.
59    pub valid: bool,
60    /// Structured errors when validation fails.
61    #[serde(default)]
62    pub errors: Vec<SimulationStructuredError>,
63    /// Optional validation artifacts from Lean.
64    #[serde(default)]
65    pub artifacts: Value,
66}
67
68#[cfg(test)]
69mod tests {
70    use super::*;
71
72    #[test]
73    fn sim_input_legacy_decode_defaults_schema_version() {
74        let legacy = serde_json::json!({
75            "scenario": {"name": "s"},
76            "global_type": {"kind": "end"},
77            "local_types": {},
78            "initial_states": {}
79        });
80
81        let input: SimRunInput = serde_json::from_value(legacy).expect("decode SimRunInput");
82        assert_eq!(
83            input.schema_version,
84            crate::schema::LEAN_BRIDGE_SCHEMA_VERSION
85        );
86    }
87
88    #[test]
89    fn sim_output_legacy_decode_defaults_schema_version() {
90        let legacy = serde_json::json!({
91            "trace": [],
92            "violations": []
93        });
94
95        let output: SimRunOutput = serde_json::from_value(legacy).expect("decode SimRunOutput");
96        assert_eq!(
97            output.schema_version,
98            crate::schema::LEAN_BRIDGE_SCHEMA_VERSION
99        );
100    }
101
102    #[test]
103    fn sim_trace_validation_roundtrip() {
104        let validation = SimTraceValidation {
105            valid: false,
106            errors: vec![SimulationStructuredError {
107                code: "sim.trace.mismatch".to_string(),
108                path: Some("trace[0]".to_string()),
109                message: "event mismatch".to_string(),
110            }],
111            artifacts: serde_json::json!({"kind": "diff"}),
112        };
113
114        let encoded = serde_json::to_value(&validation).expect("encode");
115        let decoded: SimTraceValidation = serde_json::from_value(encoded).expect("decode");
116        assert!(!decoded.valid);
117        assert_eq!(decoded.errors.len(), 1);
118        assert_eq!(decoded.errors[0].code, "sim.trace.mismatch");
119    }
120}
telltale_lean_bridge/sim_reference.rs

telltale_lean_bridge/
sim_reference.rs
