Expand description
Per-macrostep trace records.
Every crate::session::start and crate::session::step call returns one
MacrostepTrace: the input it processed, each event it consumed with the transitions that
event (or an eventless selection) fired, the configuration afterwards and the effects it
emitted. Rust and the Lean oracle produce these records independently and the differential
tests compare them for equality. See crate::tape for the JSON Lines exchange format.
Structs§
- Macrostep
Trace - The record of one macrostep (one
startorstepcall). - Microstep
Trace - One selection round inside a macrostep.
- Transition
Ref - A declared transition, identified by its source state and its index in that state’s transition list in the IR.
Enums§
- Trace
Input - What a macrostep was started by.