telltale_lean_bridge/
vm_trace.rs

1//! VM trace normalization helpers for cross-VM comparison.
2
3use serde::{Deserialize, Serialize};
4use serde_json::Value;
5use std::collections::{BTreeMap, HashMap};
6
7/// Normalized event for cross-VM comparison.
8/// Drops absolute session IDs (may differ), normalizes to session index.
9#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq)]
10pub struct NormalizedEvent {
11    pub kind: String,
12    pub session_index: usize,
13    pub sender: String,
14    pub receiver: String,
15    pub label: Option<String>,
16}
17
18/// Per-session trace: the subsequence of events for one session.
19pub type SessionTrace = Vec<NormalizedEvent>;
20
21/// Topology perturbation kinds recorded in effect traces.
22#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq)]
23pub enum TopologyPerturbationKind {
24    Crash,
25    Partition,
26    Heal,
27}
28
29/// Optional topology perturbation payload associated with an effect.
30#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq)]
31pub struct TopologyPerturbationEvent {
32    pub kind: TopologyPerturbationKind,
33    #[serde(default)]
34    pub site: Option<String>,
35    #[serde(default)]
36    pub from: Option<String>,
37    #[serde(default)]
38    pub to: Option<String>,
39}
40
41/// Effect-trace record used for replay and determinism checks.
42#[derive(Debug, Clone, Serialize, Deserialize, PartialEq)]
43pub struct EffectTraceEvent {
44    pub effect_id: u64,
45    pub effect_kind: String,
46    pub inputs: Value,
47    pub outputs: Value,
48    pub handler_identity: String,
49    pub ordering_key: u64,
50    #[serde(default)]
51    pub topology: Option<TopologyPerturbationEvent>,
52}
53
54/// Output-condition verification record in replay traces.
55#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq)]
56pub struct OutputConditionTraceEvent {
57    pub predicate_ref: String,
58    #[serde(default)]
59    pub witness_ref: Option<String>,
60    pub output_digest: String,
61    pub passed: bool,
62}
63
64/// Replay bundle combining VM events with effect/output-condition traces.
65#[derive(Debug, Clone, Serialize, Deserialize, PartialEq)]
66pub struct ReplayTraceBundle {
67    /// Schema version for this payload.
68    #[serde(default = "crate::schema::default_schema_version")]
69    pub schema_version: String,
70    pub vm_trace: Vec<NormalizedEvent>,
71    #[serde(default)]
72    pub effect_trace: Vec<EffectTraceEvent>,
73    #[serde(default)]
74    pub output_condition_trace: Vec<OutputConditionTraceEvent>,
75}
76
77/// Try to extract a session identifier from an event payload.
78///
79/// Supports common shapes used by VM traces:
80/// - `{ "session": <usize>, ... }`
81/// - `{ "sid": <usize>, ... }`
82/// - nested `{ "edge": { "sid": <usize> } }`
83/// - nested `{ "endpoint": { "sid": <usize> } }`
84#[must_use]
85pub fn event_session<E>(event: &E) -> Option<usize>
86where
87    E: Serialize,
88{
89    let value = serde_json::to_value(event).ok()?;
90    event_session_from_value(&value)
91}
92
93fn event_session_from_value(value: &Value) -> Option<usize> {
94    match value {
95        Value::Object(map) => {
96            if let Some(sid) = map.get("session").and_then(Value::as_u64) {
97                return usize::try_from(sid).ok();
98            }
99            if let Some(sid) = map.get("sid").and_then(Value::as_u64) {
100                return usize::try_from(sid).ok();
101            }
102            if let Some(edge_sid) = map
103                .get("edge")
104                .and_then(Value::as_object)
105                .and_then(|edge| edge.get("sid"))
106                .and_then(Value::as_u64)
107            {
108                return usize::try_from(edge_sid).ok();
109            }
110            if let Some(endpoint_sid) = map
111                .get("endpoint")
112                .and_then(Value::as_object)
113                .and_then(|endpoint| endpoint.get("sid"))
114                .and_then(Value::as_u64)
115            {
116                return usize::try_from(endpoint_sid).ok();
117            }
118
119            for nested in map.values() {
120                if let Some(sid) = event_session_from_value(nested) {
121                    return Some(sid);
122                }
123            }
124            None
125        }
126        Value::Array(items) => {
127            for nested in items {
128                if let Some(sid) = event_session_from_value(nested) {
129                    return Some(sid);
130                }
131            }
132            None
133        }
134        _ => None,
135    }
136}
137
138/// Normalize tick values per session so traces can be compared independent of
139/// cross-session scheduling interleavings.
140#[must_use]
141pub fn normalize_vm_trace<E>(
142    trace: &[crate::vm_export::TickedObsEvent<E>],
143) -> Vec<crate::vm_export::TickedObsEvent<E>>
144where
145    E: Serialize + Clone,
146{
147    let mut counters: HashMap<usize, u64> = HashMap::new();
148    let mut out = Vec::with_capacity(trace.len());
149
150    for ev in trace {
151        if let Some(sid) = event_session(&ev.event) {
152            let counter = counters.entry(sid).or_insert(0);
153            out.push(crate::vm_export::TickedObsEvent {
154                tick: *counter,
155                event: ev.event.clone(),
156            });
157            *counter += 1;
158        } else {
159            out.push(ev.clone());
160        }
161    }
162
163    out
164}
165
166/// Compare two traces after per-session normalization.
167#[must_use]
168pub fn traces_equivalent<E>(
169    rust_trace: &[crate::vm_export::TickedObsEvent<E>],
170    lean_trace: &[crate::vm_export::TickedObsEvent<E>],
171) -> bool
172where
173    E: Serialize + Clone + PartialEq,
174{
175    normalize_vm_trace(rust_trace) == normalize_vm_trace(lean_trace)
176}
177
178/// Minimal shared observational equivalence relation for Lean/Rust VM traces.
179///
180/// Equivalence is defined as equality after per-session tick normalization.
181#[must_use]
182pub fn observationally_equivalent<E>(
183    left: &[crate::vm_export::TickedObsEvent<E>],
184    right: &[crate::vm_export::TickedObsEvent<E>],
185) -> bool
186where
187    E: Serialize + Clone + PartialEq,
188{
189    traces_equivalent(left, right)
190}
191
192/// Extract per-session traces from a flat event list.
193#[must_use]
194pub fn partition_by_session(events: &[NormalizedEvent]) -> BTreeMap<usize, SessionTrace> {
195    let mut map: BTreeMap<usize, SessionTrace> = BTreeMap::new();
196    for ev in events {
197        map.entry(ev.session_index).or_default().push(ev.clone());
198    }
199    map
200}
201
202#[cfg(test)]
203mod tests {
204    use super::*;
205    use crate::vm_export::TickedObsEvent;
206    use serde_json::json;
207
208    #[test]
209    fn event_session_extracts_common_shapes() {
210        assert_eq!(
211            event_session(&json!({"session": 3, "kind": "sent"})),
212            Some(3)
213        );
214        assert_eq!(event_session(&json!({"sid": 4, "kind": "opened"})), Some(4));
215        assert_eq!(
216            event_session(&json!({"edge": {"sid": 5, "from": "A", "to": "B"}})),
217            Some(5)
218        );
219        assert_eq!(
220            event_session(&json!({"event": {"endpoint": {"sid": 6, "role": "A"}}})),
221            Some(6)
222        );
223        assert_eq!(event_session(&json!({"kind": "halted"})), None);
224    }
225
226    #[test]
227    fn normalize_vm_trace_rewrites_ticks_per_session() {
228        let trace = vec![
229            TickedObsEvent {
230                tick: 10,
231                event: json!({"session": 1, "kind": "sent"}),
232            },
233            TickedObsEvent {
234                tick: 11,
235                event: json!({"session": 2, "kind": "sent"}),
236            },
237            TickedObsEvent {
238                tick: 12,
239                event: json!({"session": 1, "kind": "received"}),
240            },
241        ];
242
243        let normalized = normalize_vm_trace(&trace);
244        assert_eq!(normalized[0].tick, 0);
245        assert_eq!(normalized[1].tick, 0);
246        assert_eq!(normalized[2].tick, 1);
247    }
248
249    #[test]
250    fn traces_equivalent_compares_normalized_ticks() {
251        let rust_trace = vec![
252            TickedObsEvent {
253                tick: 50,
254                event: json!({"session": 1, "kind": "sent"}),
255            },
256            TickedObsEvent {
257                tick: 99,
258                event: json!({"session": 1, "kind": "received"}),
259            },
260        ];
261        let lean_trace = vec![
262            TickedObsEvent {
263                tick: 1,
264                event: json!({"session": 1, "kind": "sent"}),
265            },
266            TickedObsEvent {
267                tick: 2,
268                event: json!({"session": 1, "kind": "received"}),
269            },
270        ];
271        assert!(traces_equivalent(&rust_trace, &lean_trace));
272    }
273}
telltale_lean_bridge/vm_trace.rs

telltale_lean_bridge/
vm_trace.rs
