telltale-bridge 11.0.0

Lean verification bridge for Telltale session types
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90

//! Lean reference simulator bridge payloads.

use serde::{Deserialize, Serialize};
use serde_json::Value;
use std::collections::BTreeMap;

use crate::protocol_machine_runner::ProtocolMachineTraceEvent;

/// Input payload for Lean reference simulation.
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct SimRunInput {
    /// Schema version for this payload.
    #[serde(deserialize_with = "crate::schema::deserialize_schema_version")]
    pub schema_version: String,
    /// Scenario configuration payload.
    pub scenario: Value,
    /// Global type payload.
    pub global_type: Value,
    /// Local type payloads keyed by role.
    pub local_types: BTreeMap<String, Value>,
    /// Initial role state payloads keyed by role.
    #[serde(default)]
    pub initial_states: BTreeMap<String, Vec<Value>>,
}

/// Output payload from Lean reference simulation.
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct SimRunOutput {
    /// Schema version for this payload.
    #[serde(deserialize_with = "crate::schema::deserialize_schema_version")]
    pub schema_version: String,
    /// Observable trace produced by the simulation.
    #[serde(default)]
    pub trace: Vec<ProtocolMachineTraceEvent>,
    /// Property violations emitted by Lean reference checks.
    #[serde(default)]
    pub violations: Vec<Value>,
    /// Optional operation-specific artifacts.
    #[serde(default)]
    pub artifacts: Value,
}

/// Structured simulation validation error.
#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq)]
pub struct SimulationStructuredError {
    /// Stable Lean-side error code.
    pub code: String,
    /// Optional path to the failing payload segment.
    #[serde(default)]
    pub path: Option<String>,
    /// Human-readable diagnostic message.
    pub message: String,
}

/// Result payload from `validateSimulationTrace` operation.
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct SimTraceValidation {
    /// Whether validation succeeded.
    pub valid: bool,
    /// Structured errors when validation fails.
    #[serde(default)]
    pub errors: Vec<SimulationStructuredError>,
    /// Optional validation artifacts from Lean.
    #[serde(default)]
    pub artifacts: Value,
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn sim_trace_validation_roundtrip() {
        let validation = SimTraceValidation {
            valid: false,
            errors: vec![SimulationStructuredError {
                code: "sim.trace.mismatch".to_string(),
                path: Some("trace[0]".to_string()),
                message: "event mismatch".to_string(),
            }],
            artifacts: serde_json::json!({"kind": "diff"}),
        };

        let encoded = serde_json::to_value(&validation).expect("encode");
        let decoded: SimTraceValidation = serde_json::from_value(encoded).expect("decode");
        assert!(!decoded.valid);
        assert_eq!(decoded.errors.len(), 1);
        assert_eq!(decoded.errors[0].code, "sim.trace.mismatch");
    }
}