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    /// VM configuration violates required runtime invariants.
40    #[error("invalid VM config: {reason}")]
41    InvalidConfig {
42        /// Validation failure details.
43        reason: String,
44    },
45    /// Thread-pool initialization failed.
46    #[error("thread pool build failed: {message}")]
47    ThreadPoolBuild {
48        /// Build error details.
49        message: String,
50    },
51    /// Code image failed runtime validation checks.
52    #[error("invalid code image: {reason}")]
53    InvalidCodeImage {
54        /// Validation failure details.
55        reason: String,
56    },
57}
58
59// ---- StepPack: atomic instruction result (matches Lean StepPack) ----
60
61/// How to update the coroutine after an instruction.
62pub(crate) enum CoroUpdate {
63    /// Advance PC by 1, status = Ready.
64    AdvancePc,
65    /// Set PC to target (for Jmp), status = Ready.
66    SetPc(PC),
67    /// Block with given reason. PC unchanged.
68    Block(BlockReason),
69    /// Advance PC by 1 and set blocked status.
70    AdvancePcBlock(BlockReason),
71    /// Halt (Done). PC unchanged.
72    Halt,
73    /// Advance PC by 1, write a value to a register, status = Ready.
74    AdvancePcWriteReg { reg: u16, val: Value },
75}
76
77/// Type update action for commit.
78pub(crate) enum TypeUpdate {
79    /// Advance to a new local type.
80    Advance(LocalTypeR),
81    /// Advance to a new local type and update the original (for Mu unfolding).
82    AdvanceWithOriginal(LocalTypeR, LocalTypeR),
83    /// Remove the type entry (endpoint completed).
84    Remove,
85}
86
87/// Resolve a continuation and build the appropriate `TypeUpdate`.
88pub(crate) fn resolve_type_update(
89    cont: &LocalTypeR,
90    original: &LocalTypeR,
91    ep: &Endpoint,
92) -> (LocalTypeR, Option<(Endpoint, TypeUpdate)>) {
93    let (resolved, new_scope) = unfold_if_var_with_scope(cont, original);
94    let update = if let Some(mu) = new_scope {
95        Some((
96            ep.clone(),
97            TypeUpdate::AdvanceWithOriginal(resolved.clone(), mu),
98        ))
99    } else {
100        Some((ep.clone(), TypeUpdate::Advance(resolved.clone())))
101    };
102    (resolved, update)
103}
104
105/// Atomic result of executing one instruction.
106///
107/// Matches the Lean `StepPack` pattern: bundles all mutations so the
108/// caller commits them together via `commit_pack`.
109pub(crate) struct StepPack {
110    /// How to update the coroutine.
111    pub(crate) coro_update: CoroUpdate,
112    /// Type advancement, if any. `None` means no type change (e.g., block, control flow).
113    pub(crate) type_update: Option<(Endpoint, TypeUpdate)>,
114    /// Observable events to emit.
115    pub(crate) events: Vec<ObsEvent>,
116}
117
118#[derive(Clone, Copy)]
119pub(crate) struct GuardAcquireInput<'a> {
120    pub coro_idx: usize,
121    pub endpoint: &'a Endpoint,
122    pub role: &'a str,
123    pub sid: SessionId,
124    pub layer: &'a str,
125    pub dst: u16,
126}
127
128#[derive(Clone, Copy)]
129pub(crate) struct GuardReleaseInput<'a> {
130    pub coro_idx: usize,
131    pub endpoint: &'a Endpoint,
132    pub role: &'a str,
133    pub sid: SessionId,
134    pub layer: &'a str,
135    pub evidence: u16,
136}
137
138/// Internal outcome after committing a `StepPack`.
139pub(crate) enum ExecOutcome {
140    /// Instruction completed, coroutine continues.
141    Continue,
142    /// Coroutine blocked on a resource.
143    Blocked(BlockReason),
144    /// Coroutine halted normally.
145    Halted,
146}
147
148// ---- The VM ----
149
150/// Retained observability artifacts with optional bounded storage.
151#[derive(Debug, Clone, Serialize, Deserialize)]
152#[serde(transparent)]
153pub(crate) struct RetainedLog<T>(Vec<T>);
154
155fn default_true() -> bool {
156    true
157}
158
159impl<T> Default for RetainedLog<T> {
160    fn default() -> Self {
161        Self(Vec::new())
162    }
163}
164
165impl<T> RetainedLog<T> {
166    fn push(&mut self, item: T, config: &ObservabilityRetentionConfig) {
167        match config.mode {
168            ObservabilityRetentionMode::Disabled => {}
169            ObservabilityRetentionMode::Full => self.0.push(item),
170            ObservabilityRetentionMode::Capped => {
171                self.0.push(item);
172                self.trim_to_capacity(config.capacity);
173            }
174        }
175    }
176
177    fn extend<I>(&mut self, iter: I, config: &ObservabilityRetentionConfig)
178    where
179        I: IntoIterator<Item = T>,
180    {
181        match config.mode {
182            ObservabilityRetentionMode::Disabled => {}
183            ObservabilityRetentionMode::Full => self.0.extend(iter),
184            ObservabilityRetentionMode::Capped => {
185                self.0.extend(iter);
186                self.trim_to_capacity(config.capacity);
187            }
188        }
189    }
190
191    fn as_slice(&self) -> &[T] {
192        &self.0
193    }
194
195    fn len(&self) -> usize {
196        self.0.len()
197    }
198
199    fn drain(&mut self) -> Vec<T> {
200        self.0.drain(..).collect()
201    }
202
203    fn trim_to_capacity(&mut self, capacity: usize) {
204        if self.0.len() > capacity {
205            let overflow = self.0.len() - capacity;
206            self.0.drain(0..overflow);
207        }
208    }
209}
210
211impl<T> std::ops::Deref for RetainedLog<T> {
212    type Target = [T];
213
214    fn deref(&self) -> &Self::Target {
215        self.as_slice()
216    }
217}
218
219/// The choreographic VM.
220///
221/// Manages coroutines, sessions (which own type state), and a scheduler.
222/// Multiple choreographies can be loaded into a single VM, each in its
223/// own session namespace — justified by separation logic.
224#[derive(Debug, Serialize, Deserialize)]
225pub struct VM<I = (), G = (), P = NoopPersistence, Nu = DefaultVerificationModel>
226where
227    P: PersistenceModel,
228{
229    config: VMConfig,
230    code: Option<Program>,
231    programs: ProgramStore,
232    identity_model: PhantomData<I>,
233    guard_model: PhantomData<G>,
234    persistence_model: PhantomData<P>,
235    persistent: P::PState,
236    verification: Nu,
237    #[serde(default)]
238    communication_consumption: DefaultCommunicationConsumption,
239    #[serde(default)]
240    communication_consumption_artifacts: RetainedLog<CommunicationConsumptionArtifact>,
241    coroutines: Vec<Coroutine>,
242    sessions: SessionStore,
243    arena: Arena,
244    resource_states: BTreeMap<ScopeId, ResourceState>,
245    sched: Scheduler,
246    monitor: SessionMonitor,
247    obs_trace: RetainedLog<ObsEvent>,
248    role_symbols: SymbolTable,
249    label_symbols: SymbolTable,
250    handler_symbols: SymbolTable,
251    edge_symbols: EdgeSymbolTable,
252    clock: SimClock,
253    next_coro_id: usize,
254    next_session_id: SessionId,
255    paused_roles: BTreeSet<String>,
256    #[serde(skip, default)]
257    coro_slots: BTreeMap<usize, usize>,
258    #[serde(skip, default)]
259    role_coroutines: BTreeMap<String, Vec<usize>>,
260    #[serde(skip, default)]
261    paused_coro_ids: BTreeSet<usize>,
262    #[serde(skip, default)]
263    timed_out_coro_ids: BTreeSet<usize>,
264    #[serde(skip, default)]
265    session_open_plans: BTreeMap<String, crate::session::SessionOpenPlan>,
266    #[serde(skip, default)]
267    eligible_ready: BTreeSet<usize>,
268    #[serde(skip, default = "default_true")]
269    eligibility_dirty: bool,
270    guard_layer: InMemoryGuardLayer,
271    effect_trace: RetainedLog<EffectTraceEntry>,
272    next_effect_id: u64,
273    output_condition_checks: RetainedLog<OutputConditionCheck>,
274    crashed_sites: BTreeSet<SiteId>,
275    partitioned_edges: BTreeSet<(SiteId, SiteId)>,
276    corrupted_edges: BTreeMap<(SiteId, SiteId), CorruptionType>,
277    timed_out_sites: BTreeMap<SiteId, u64>,
278    last_sched_step: Option<SchedStepDebug>,
279    handler_identity_anchor: Option<String>,
280}
281
282/// Lean-aligned VM state alias.
283pub type VMState<I = (), G = (), P = NoopPersistence, Nu = DefaultVerificationModel> =
284    VM<I, G, P, Nu>;
285
286impl<I, G, P, Nu> VM<I, G, P, Nu>
287where
288    P: PersistenceModel,
289{
290    /// Create a VM for arbitrary persistence/verification model parameters.
291    #[must_use]
292    pub fn new_with_models(config: VMConfig) -> Self
293    where
294        P::PState: Default,
295        Nu: VerificationModel + Default,
296    {
297        config.assert_invariants();
298        let tick_duration = config.tick_duration;
299        let communication_replay_mode = config.communication_replay_mode;
300        let sched = Scheduler::new(config.sched_policy.clone());
301        let mut guard_resources = BTreeMap::new();
302        for layer in &config.guard_layers {
303            guard_resources.insert(layer.id.clone(), Value::Unit);
304        }
305        Self {
306            config,
307            code: None,
308            programs: ProgramStore::new(),
309            identity_model: PhantomData,
310            guard_model: PhantomData,
311            persistence_model: PhantomData,
312            persistent: P::PState::default(),
313            verification: Nu::default(),
314            communication_consumption: DefaultCommunicationConsumption::new(
315                communication_replay_mode,
316            ),
317            communication_consumption_artifacts: RetainedLog::default(),
318            coroutines: Vec::new(),
319            sessions: SessionStore::new(),
320            arena: Arena::default(),
321            resource_states: BTreeMap::new(),
322            sched,
323            monitor: SessionMonitor::default(),
324            obs_trace: RetainedLog::default(),
325            role_symbols: SymbolTable::new(),
326            label_symbols: SymbolTable::new(),
327            handler_symbols: SymbolTable::new(),
328            edge_symbols: EdgeSymbolTable::new(),
329            clock: SimClock::new(tick_duration),
330            next_coro_id: 0,
331            next_session_id: 0,
332            paused_roles: BTreeSet::new(),
333            coro_slots: BTreeMap::new(),
334            role_coroutines: BTreeMap::new(),
335            paused_coro_ids: BTreeSet::new(),
336            timed_out_coro_ids: BTreeSet::new(),
337            session_open_plans: BTreeMap::new(),
338            eligible_ready: BTreeSet::new(),
339            eligibility_dirty: true,
340            guard_layer: InMemoryGuardLayer {
341                resources: guard_resources
342                    .into_iter()
343                    .map(|(k, v)| (LayerId(k), v))
344                    .collect(),
345            },
346            effect_trace: RetainedLog::default(),
347            next_effect_id: 0,
348            output_condition_checks: RetainedLog::default(),
349            crashed_sites: BTreeSet::new(),
350            partitioned_edges: BTreeSet::new(),
351            corrupted_edges: BTreeMap::new(),
352            timed_out_sites: BTreeMap::new(),
353            last_sched_step: None,
354            handler_identity_anchor: None,
355        }
356    }
357
358    /// Borrow the persistent state tracked by the configured persistence model.
359    #[must_use]
360    pub fn persistent_state(&self) -> &P::PState {
361        &self.persistent
362    }
363
364    /// Mutably borrow persistent state.
365    pub fn persistent_state_mut(&mut self) -> &mut P::PState {
366        &mut self.persistent
367    }
368
369    fn apply_open_delta(&mut self, sid: SessionId) -> Result<(), String> {
370        let delta = P::open_delta(sid);
371        P::apply(&mut self.persistent, &delta)
372    }
373
374    fn apply_close_delta(&mut self, sid: SessionId) -> Result<(), String> {
375        let delta = P::close_delta(sid);
376        P::apply(&mut self.persistent, &delta)
377    }
378
379    fn apply_invoke_delta(&mut self, sid: SessionId, action: &str) -> Result<(), String> {
380        if let Some(delta) = P::invoke_delta(sid, action) {
381            P::apply(&mut self.persistent, &delta)?;
382        }
383        Ok(())
384    }
385
386    /// Resolve guard-layer capability for a participant via bridge binding.
387    #[must_use]
388    pub fn bridge_guard_layer_for_participant<B>(
389        &self,
390        bridge: &B,
391        participant: &I::ParticipantId,
392    ) -> LayerId
393    where
394        I: IdentityModel,
395        G: GuardLayer,
396        B: IdentityGuardBridge<I, G>,
397    {
398        bridge.guard_layer_for_participant(participant)
399    }
400
401    /// Resolve participant verification key via bridge binding.
402    #[must_use]
403    pub fn bridge_verifying_key_for_participant<B>(
404        &self,
405        bridge: &B,
406        participant: &I::ParticipantId,
407    ) -> Nu::VerifyingKey
408    where
409        I: IdentityModel,
410        Nu: VerificationModel,
411        B: IdentityVerificationBridge<I, Nu>,
412    {
413        bridge.verification_key_for_participant(participant)
414    }
415}
telltale_vm/vm/vm_error_and_step_pack.rs

telltale_vm/vm/
vm_error_and_step_pack.rs
