vertep_core/lib.rs
1//! Chart IR, validation and the pure SCXML step kernel for Vertep.
2//!
3//! `vertep-core` is `no_std` with `alloc` and has no I/O, no async and no clock: every
4//! interaction with the outside world is an effect returned by the step function.
5//!
6//! The pipeline is: build or read a [`ir::Chart`], give anonymous states identifiers with
7//! [`identity::assign_generated_ids`], compile it with [`compile::CompiledChart::new`] (which runs
8//! [`validate::validate`]), pick the datamodel with [`null::create_datamodel`], then call
9//! [`session::start`] once and [`session::step`] for every input. Wrap the datamodel in a
10//! [`tape::TapeDatamodel`] to record the answer tape for the Lean oracle.
11//!
12//! @tg: implements:: [[decisions#IR is the hub]]
13//! @tg: implements:: [[decisions#SCXML semantics are normative]]
14//! @tg: implements:: [[decisions#No-std core and tokio shell]]
15//! @tg: implements:: [[decisions#Pluggable datamodel]]
16
17#![cfg_attr(not(feature = "std"), no_std)]
18
19extern crate alloc;
20
21pub mod bitset;
22pub mod compile;
23pub mod datamodel;
24pub mod identity;
25pub mod ir;
26pub mod kernel;
27pub mod null;
28pub mod order;
29pub mod session;
30pub mod tape;
31pub mod trace;
32pub mod types;
33pub mod validate;
34
35#[cfg(test)]
36mod tests;