vertep_core/
tape.rs

1//! The datamodel answer tape for the Lean oracle (decision D5).
2//!
3//! [`TapeDatamodel`] wraps any datamodel and records every request the interpreter makes and the
4//! answer it got, in order. The Lean `step` treats the datamodel as an oracle: it replays the
5//! tape and must issue exactly the same requests in the same order, so the Rust and Lean runs can
6//! be compared on charts whose expressions Lean cannot evaluate. `snapshot` takes `&self` and is
7//! never called by the interpreter, so it is not recorded; `name` is not recorded either.
8//!
9//! # Exchange format
10//!
11//! With the `serde` feature the tape, the trace and the inputs serialize with serde's default
12//! (externally tagged) representation. The exchange with the oracle is JSON Lines: one
13//! [`OracleRecord`] per line, one line per macrostep, in order:
14//!
15//! ```text
16//! {"input": <OracleInput>, "tape": [<TapeEntry>, ...], "trace": <MacrostepTrace>}
17//! ```
18//!
19//! - `input` is `{"Start": <StartInput>}` for the first line and `{"Step": <Input>}` afterwards.
20//! - `tape` lists the datamodel requests of that macrostep as
21//!   `{"request": <Request>, "answer": <Answer>}`, for example
22//!   `{"request": {"EvalCond": {"expr": "In('b')"}}, "answer": {"Bool": true}}` or
23//!   `{"request": {"EvalValue": {"expr": "x"}}, "answer": {"Error": {"message": "..."}}}`.
24//!   Unit requests (`SetEvent`, `SetEnvironment`, successful `Declare`, ...) answer `"Unit"`.
25//! - `trace` is the [`MacrostepTrace`]: `index`, `input` (`{"Start": {"sessionid": ...}}`,
26//!   `{"Event": <Event>}` or `"Cancel"`), `microsteps` (each `{"event": name or null,
27//!   "transitions": [{"source": id, "index": n}, ...]}`), `configuration` (state identifiers in
28//!   document order), `effects` (each an externally tagged [`crate::session::Effect`]) and
29//!   `terminated`.
30//!
31//! [`Value`]s serialize as `"Undefined"`, `"Null"`, `{"Bool": b}`, `{"Number": n}`,
32//! `{"String": s}`, `{"Array": [...]}` and `{"Object": [[key, value], ...]}` (keys in insertion
33//! order).
34
35use alloc::string::String;
36use alloc::vec::Vec;
37
38use crate::datamodel::{Datamodel, Environment, EvalError, Event, SessionInfo, StateQuery, Value};
39use crate::session::{Input, StartInput};
40use crate::trace::MacrostepTrace;
41
42/// A datamodel request.
43#[derive(Clone, Debug, PartialEq)]
44#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
45pub enum Request {
46    /// `init_session`.
47    InitSession(SessionInfo),
48    /// `set_environment`.
49    SetEnvironment(Environment),
50    /// `declare`.
51    Declare {
52        /// Data item id.
53        id: String,
54    },
55    /// `set_event`.
56    SetEvent(Event),
57    /// `eval_cond`.
58    EvalCond {
59        /// Expression.
60        expr: String,
61    },
62    /// `eval_value`.
63    EvalValue {
64        /// Expression.
65        expr: String,
66    },
67    /// `eval_content`.
68    EvalContent {
69        /// Inline content.
70        content: String,
71    },
72    /// `assign_expr`.
73    AssignExpr {
74        /// Location.
75        location: String,
76        /// Expression.
77        expr: String,
78    },
79    /// `assign_value`.
80    AssignValue {
81        /// Location.
82        location: String,
83        /// Value.
84        value: Value,
85    },
86    /// `bind_var`.
87    BindVar {
88        /// Variable name.
89        name: String,
90        /// Value.
91        value: Value,
92    },
93    /// `is_location`.
94    IsLocation {
95        /// Location.
96        location: String,
97    },
98    /// `exec_script`.
99    ExecScript {
100        /// Script text.
101        script: String,
102    },
103    /// `foreach_items`.
104    ForeachItems {
105        /// Array expression.
106        array: String,
107    },
108    /// `restore`.
109    Restore(Value),
110}
111
112/// A datamodel answer.
113#[derive(Clone, Debug, PartialEq)]
114#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
115pub enum Answer {
116    /// Success without a value.
117    Unit,
118    /// A boolean (conditions, `is_location`).
119    Bool(bool),
120    /// A value.
121    Value(Value),
122    /// A list of values (`foreach_items`).
123    Values(Vec<Value>),
124    /// An evaluation error.
125    Error(EvalError),
126}
127
128/// One request and its answer.
129#[derive(Clone, Debug, PartialEq)]
130#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
131pub struct TapeEntry {
132    /// The request.
133    pub request: Request,
134    /// The answer.
135    pub answer: Answer,
136}
137
138/// The input of one macrostep in an oracle record.
139#[derive(Clone, Debug, PartialEq)]
140#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
141pub enum OracleInput {
142    /// The start macrostep.
143    Start(StartInput),
144    /// A later macrostep.
145    Step(Input),
146}
147
148/// One JSON Lines record exchanged with the Lean oracle: a macrostep's input, its datamodel
149/// tape and its trace.
150#[derive(Clone, Debug, PartialEq)]
151#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
152pub struct OracleRecord {
153    /// The input.
154    pub input: OracleInput,
155    /// Datamodel requests and answers, in order.
156    pub tape: Vec<TapeEntry>,
157    /// The macrostep trace.
158    pub trace: MacrostepTrace,
159}
160
161/// A datamodel wrapper that records every request and answer.
162pub struct TapeDatamodel<'a> {
163    inner: &'a mut dyn Datamodel,
164    entries: Vec<TapeEntry>,
165}
166
167impl<'a> TapeDatamodel<'a> {
168    /// Record the requests made to `inner`.
169    pub fn new(inner: &'a mut dyn Datamodel) -> Self {
170        TapeDatamodel {
171            inner,
172            entries: Vec::new(),
173        }
174    }
175
176    /// The entries recorded so far.
177    pub fn entries(&self) -> &[TapeEntry] {
178        &self.entries
179    }
180
181    /// Take the entries recorded so far, leaving the tape empty (call after each macrostep).
182    pub fn take(&mut self) -> Vec<TapeEntry> {
183        core::mem::take(&mut self.entries)
184    }
185
186    fn log(&mut self, request: Request, answer: Answer) {
187        self.entries.push(TapeEntry { request, answer });
188    }
189}
190
191fn unit(r: &Result<(), EvalError>) -> Answer {
192    match r {
193        Ok(()) => Answer::Unit,
194        Err(e) => Answer::Error(e.clone()),
195    }
196}
197
198impl Datamodel for TapeDatamodel<'_> {
199    fn name(&self) -> &str {
200        self.inner.name()
201    }
202
203    fn init_session(&mut self, info: &SessionInfo) -> Result<(), EvalError> {
204        let r = self.inner.init_session(info);
205        self.log(Request::InitSession(info.clone()), unit(&r));
206        r
207    }
208
209    fn set_environment(&mut self, env: &Environment) {
210        self.inner.set_environment(env);
211        self.log(Request::SetEnvironment(*env), Answer::Unit);
212    }
213
214    fn declare(&mut self, id: &str) -> Result<(), EvalError> {
215        let r = self.inner.declare(id);
216        self.log(Request::Declare { id: id.into() }, unit(&r));
217        r
218    }
219
220    fn set_event(&mut self, event: &Event) {
221        self.inner.set_event(event);
222        self.log(Request::SetEvent(event.clone()), Answer::Unit);
223    }
224
225    /// Not an interpreter request (hosts call it before stepping), so it is not recorded.
226    fn check_event(&self, event: &Event) -> Result<(), EvalError> {
227        self.inner.check_event(event)
228    }
229
230    fn eval_cond(&mut self, expr: &str, states: &dyn StateQuery) -> Result<bool, EvalError> {
231        let r = self.inner.eval_cond(expr, states);
232        let a = match &r {
233            Ok(b) => Answer::Bool(*b),
234            Err(e) => Answer::Error(e.clone()),
235        };
236        self.log(Request::EvalCond { expr: expr.into() }, a);
237        r
238    }
239
240    fn eval_value(&mut self, expr: &str, states: &dyn StateQuery) -> Result<Value, EvalError> {
241        let r = self.inner.eval_value(expr, states);
242        let a = match &r {
243            Ok(v) => Answer::Value(v.clone()),
244            Err(e) => Answer::Error(e.clone()),
245        };
246        self.log(Request::EvalValue { expr: expr.into() }, a);
247        r
248    }
249
250    fn eval_content(&mut self, content: &str) -> Result<Value, EvalError> {
251        let r = self.inner.eval_content(content);
252        let a = match &r {
253            Ok(v) => Answer::Value(v.clone()),
254            Err(e) => Answer::Error(e.clone()),
255        };
256        self.log(
257            Request::EvalContent {
258                content: content.into(),
259            },
260            a,
261        );
262        r
263    }
264
265    fn assign_expr(
266        &mut self,
267        location: &str,
268        expr: &str,
269        states: &dyn StateQuery,
270    ) -> Result<(), EvalError> {
271        let r = self.inner.assign_expr(location, expr, states);
272        self.log(
273            Request::AssignExpr {
274                location: location.into(),
275                expr: expr.into(),
276            },
277            unit(&r),
278        );
279        r
280    }
281
282    fn assign_value(&mut self, location: &str, value: Value) -> Result<(), EvalError> {
283        let req = Request::AssignValue {
284            location: location.into(),
285            value: value.clone(),
286        };
287        let r = self.inner.assign_value(location, value);
288        self.log(req, unit(&r));
289        r
290    }
291
292    fn bind_var(&mut self, name: &str, value: Value) -> Result<(), EvalError> {
293        let req = Request::BindVar {
294            name: name.into(),
295            value: value.clone(),
296        };
297        let r = self.inner.bind_var(name, value);
298        self.log(req, unit(&r));
299        r
300    }
301
302    fn is_location(&mut self, location: &str) -> bool {
303        let r = self.inner.is_location(location);
304        self.log(
305            Request::IsLocation {
306                location: location.into(),
307            },
308            Answer::Bool(r),
309        );
310        r
311    }
312
313    fn exec_script(&mut self, script: &str, states: &dyn StateQuery) -> Result<(), EvalError> {
314        let r = self.inner.exec_script(script, states);
315        self.log(
316            Request::ExecScript {
317                script: script.into(),
318            },
319            unit(&r),
320        );
321        r
322    }
323
324    fn foreach_items(
325        &mut self,
326        array: &str,
327        states: &dyn StateQuery,
328    ) -> Result<Vec<Value>, EvalError> {
329        let r = self.inner.foreach_items(array, states);
330        let a = match &r {
331            Ok(v) => Answer::Values(v.clone()),
332            Err(e) => Answer::Error(e.clone()),
333        };
334        self.log(
335            Request::ForeachItems {
336                array: array.into(),
337            },
338            a,
339        );
340        r
341    }
342
343    fn snapshot(&self) -> Value {
344        self.inner.snapshot()
345    }
346
347    fn restore(&mut self, snapshot: &Value) -> Result<(), EvalError> {
348        let r = self.inner.restore(snapshot);
349        self.log(Request::Restore(snapshot.clone()), unit(&r));
350        r
351    }
352}
vertep_core/tape.rs

vertep_core/
tape.rs
