telltale_vm/vm/
vm_error_and_step_pack.rs

1/// Errors from VM operations.
2#[derive(Debug, thiserror::Error)]
3pub enum VMError {
4    /// A coroutine faulted.
5    #[error("coroutine {coro_id} faulted: {fault}")]
6    Fault {
7        /// Coroutine ID.
8        coro_id: usize,
9        /// The fault.
10        fault: Fault,
11    },
12    /// Session limit exceeded.
13    #[error("max sessions ({max}) exceeded")]
14    TooManySessions {
15        /// Maximum allowed.
16        max: usize,
17    },
18    /// Coroutine limit exceeded.
19    #[error("max coroutines ({max}) exceeded")]
20    TooManyCoroutines {
21        /// Maximum allowed.
22        max: usize,
23    },
24    /// Session not found.
25    #[error("session {0} not found")]
26    SessionNotFound(SessionId),
27    /// Effect handler error.
28    #[error("effect handler error: {0}")]
29    HandlerError(String),
30    /// Persistence model lifecycle error.
31    #[error("persistence error: {0}")]
32    PersistenceError(String),
33    /// Invalid concurrency parameter.
34    #[error("invalid concurrency level: {n}")]
35    InvalidConcurrency {
36        /// Requested concurrency.
37        n: usize,
38    },
39}
40
41// ---- StepPack: atomic instruction result (matches Lean StepPack) ----
42
43/// How to update the coroutine after an instruction.
44pub(crate) enum CoroUpdate {
45    /// Advance PC by 1, status = Ready.
46    AdvancePc,
47    /// Set PC to target (for Jmp), status = Ready.
48    SetPc(PC),
49    /// Block with given reason. PC unchanged.
50    Block(BlockReason),
51    /// Advance PC by 1 and set blocked status.
52    AdvancePcBlock(BlockReason),
53    /// Halt (Done). PC unchanged.
54    Halt,
55    /// Advance PC by 1, write a value to a register, status = Ready.
56    AdvancePcWriteReg { reg: u16, val: Value },
57}
58
59/// Type update action for commit.
60pub(crate) enum TypeUpdate {
61    /// Advance to a new local type.
62    Advance(LocalTypeR),
63    /// Advance to a new local type and update the original (for Mu unfolding).
64    AdvanceWithOriginal(LocalTypeR, LocalTypeR),
65    /// Remove the type entry (endpoint completed).
66    Remove,
67}
68
69/// Resolve a continuation and build the appropriate `TypeUpdate`.
70pub(crate) fn resolve_type_update(
71    cont: &LocalTypeR,
72    original: &LocalTypeR,
73    ep: &Endpoint,
74) -> (LocalTypeR, Option<(Endpoint, TypeUpdate)>) {
75    let (resolved, new_scope) = unfold_if_var_with_scope(cont, original);
76    let update = if let Some(mu) = new_scope {
77        Some((
78            ep.clone(),
79            TypeUpdate::AdvanceWithOriginal(resolved.clone(), mu),
80        ))
81    } else {
82        Some((ep.clone(), TypeUpdate::Advance(resolved.clone())))
83    };
84    (resolved, update)
85}
86
87/// Atomic result of executing one instruction.
88///
89/// Matches the Lean `StepPack` pattern: bundles all mutations so the
90/// caller commits them together via `commit_pack`.
91pub(crate) struct StepPack {
92    /// How to update the coroutine.
93    pub(crate) coro_update: CoroUpdate,
94    /// Type advancement, if any. `None` means no type change (e.g., block, control flow).
95    pub(crate) type_update: Option<(Endpoint, TypeUpdate)>,
96    /// Observable events to emit.
97    pub(crate) events: Vec<ObsEvent>,
98}
99
100#[derive(Clone, Copy)]
101pub(crate) struct GuardAcquireInput<'a> {
102    pub coro_idx: usize,
103    pub endpoint: &'a Endpoint,
104    pub role: &'a str,
105    pub sid: SessionId,
106    pub layer: &'a str,
107    pub dst: u16,
108}
109
110#[derive(Clone, Copy)]
111pub(crate) struct GuardReleaseInput<'a> {
112    pub coro_idx: usize,
113    pub endpoint: &'a Endpoint,
114    pub role: &'a str,
115    pub sid: SessionId,
116    pub layer: &'a str,
117    pub evidence: u16,
118}
119
120/// Internal outcome after committing a `StepPack`.
121pub(crate) enum ExecOutcome {
122    /// Instruction completed, coroutine continues.
123    Continue,
124    /// Coroutine blocked on a resource.
125    Blocked(BlockReason),
126    /// Coroutine halted normally.
127    Halted,
128}
129
130// ---- The VM ----
131
132/// The choreographic VM.
133///
134/// Manages coroutines, sessions (which own type state), and a scheduler.
135/// Multiple choreographies can be loaded into a single VM, each in its
136/// own session namespace — justified by separation logic.
137#[derive(Debug, Serialize, Deserialize)]
138pub struct VM<I = (), G = (), P = NoopPersistence, Nu = DefaultVerificationModel>
139where
140    P: PersistenceModel,
141{
142    config: VMConfig,
143    code: Option<Program>,
144    programs: Vec<Program>,
145    identity_model: PhantomData<I>,
146    guard_model: PhantomData<G>,
147    persistence_model: PhantomData<P>,
148    persistent: P::PState,
149    verification: Nu,
150    coroutines: Vec<Coroutine>,
151    sessions: SessionStore,
152    arena: Arena,
153    resource_states: BTreeMap<ScopeId, ResourceState>,
154    sched: Scheduler,
155    monitor: SessionMonitor,
156    obs_trace: Vec<ObsEvent>,
157    role_symbols: SymbolTable,
158    label_symbols: SymbolTable,
159    clock: SimClock,
160    next_coro_id: usize,
161    next_session_id: SessionId,
162    paused_roles: BTreeSet<String>,
163    guard_layer: InMemoryGuardLayer,
164    effect_trace: Vec<EffectTraceEntry>,
165    next_effect_id: u64,
166    output_condition_checks: Vec<OutputConditionCheck>,
167    crashed_sites: BTreeSet<SiteId>,
168    partitioned_edges: BTreeSet<(SiteId, SiteId)>,
169    corrupted_edges: BTreeMap<(SiteId, SiteId), CorruptionType>,
170    timed_out_sites: BTreeMap<SiteId, u64>,
171    last_sched_step: Option<SchedStepDebug>,
172    handler_identity_anchor: Option<String>,
173}
174
175/// Lean-aligned VM state alias.
176pub type VMState<I = (), G = (), P = NoopPersistence, Nu = DefaultVerificationModel> =
177    VM<I, G, P, Nu>;
178
179impl<I, G, P, Nu> VM<I, G, P, Nu>
180where
181    P: PersistenceModel,
182{
183    /// Create a VM for arbitrary persistence/verification model parameters.
184    #[must_use]
185    pub fn new_with_models(config: VMConfig) -> Self
186    where
187        P::PState: Default,
188        Nu: VerificationModel + Default,
189    {
190        config.assert_invariants();
191        let tick_duration = config.tick_duration;
192        let sched = Scheduler::new(config.sched_policy.clone());
193        let mut guard_resources = BTreeMap::new();
194        for layer in &config.guard_layers {
195            guard_resources.insert(layer.id.clone(), Value::Unit);
196        }
197        Self {
198            config,
199            code: None,
200            programs: Vec::new(),
201            identity_model: PhantomData,
202            guard_model: PhantomData,
203            persistence_model: PhantomData,
204            persistent: P::PState::default(),
205            verification: Nu::default(),
206            coroutines: Vec::new(),
207            sessions: SessionStore::new(),
208            arena: Arena::default(),
209            resource_states: BTreeMap::new(),
210            sched,
211            monitor: SessionMonitor::default(),
212            obs_trace: Vec::new(),
213            role_symbols: SymbolTable::new(),
214            label_symbols: SymbolTable::new(),
215            clock: SimClock::new(tick_duration),
216            next_coro_id: 0,
217            next_session_id: 0,
218            paused_roles: BTreeSet::new(),
219            guard_layer: InMemoryGuardLayer {
220                resources: guard_resources
221                    .into_iter()
222                    .map(|(k, v)| (LayerId(k), v))
223                    .collect(),
224            },
225            effect_trace: Vec::new(),
226            next_effect_id: 0,
227            output_condition_checks: Vec::new(),
228            crashed_sites: BTreeSet::new(),
229            partitioned_edges: BTreeSet::new(),
230            corrupted_edges: BTreeMap::new(),
231            timed_out_sites: BTreeMap::new(),
232            last_sched_step: None,
233            handler_identity_anchor: None,
234        }
235    }
236
237    /// Borrow the persistent state tracked by the configured persistence model.
238    #[must_use]
239    pub fn persistent_state(&self) -> &P::PState {
240        &self.persistent
241    }
242
243    /// Mutably borrow persistent state.
244    pub fn persistent_state_mut(&mut self) -> &mut P::PState {
245        &mut self.persistent
246    }
247
248    fn apply_open_delta(&mut self, sid: SessionId) -> Result<(), String> {
249        let delta = P::open_delta(sid);
250        P::apply(&mut self.persistent, &delta)
251    }
252
253    fn apply_close_delta(&mut self, sid: SessionId) -> Result<(), String> {
254        let delta = P::close_delta(sid);
255        P::apply(&mut self.persistent, &delta)
256    }
257
258    fn apply_invoke_delta(&mut self, sid: SessionId, action: &str) -> Result<(), String> {
259        if let Some(delta) = P::invoke_delta(sid, action) {
260            P::apply(&mut self.persistent, &delta)?;
261        }
262        Ok(())
263    }
264
265    /// Resolve guard-layer capability for a participant via bridge binding.
266    #[must_use]
267    pub fn bridge_guard_layer_for_participant<B>(
268        &self,
269        bridge: &B,
270        participant: &I::ParticipantId,
271    ) -> LayerId
272    where
273        I: IdentityModel,
274        G: GuardLayer,
275        B: IdentityGuardBridge<I, G>,
276    {
277        bridge.guard_layer_for_participant(participant)
278    }
279
280    /// Resolve participant verification key via bridge binding.
281    #[must_use]
282    pub fn bridge_verifying_key_for_participant<B>(
283        &self,
284        bridge: &B,
285        participant: &I::ParticipantId,
286    ) -> Nu::VerifyingKey
287    where
288        I: IdentityModel,
289        Nu: VerificationModel,
290        B: IdentityVerificationBridge<I, Nu>,
291    {
292        bridge.verification_key_for_participant(participant)
293    }
294}
295
telltale_vm/vm/vm_error_and_step_pack.rs

telltale_vm/vm/
vm_error_and_step_pack.rs
