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/// The choreographic VM.
151///
152/// Manages coroutines, sessions (which own type state), and a scheduler.
153/// Multiple choreographies can be loaded into a single VM, each in its
154/// own session namespace — justified by separation logic.
155#[derive(Debug, Serialize, Deserialize)]
156pub struct VM<I = (), G = (), P = NoopPersistence, Nu = DefaultVerificationModel>
157where
158    P: PersistenceModel,
159{
160    config: VMConfig,
161    code: Option<Program>,
162    programs: Vec<Program>,
163    identity_model: PhantomData<I>,
164    guard_model: PhantomData<G>,
165    persistence_model: PhantomData<P>,
166    persistent: P::PState,
167    verification: Nu,
168    #[serde(default)]
169    communication_consumption: DefaultCommunicationConsumption,
170    #[serde(default)]
171    communication_consumption_artifacts: Vec<CommunicationConsumptionArtifact>,
172    coroutines: Vec<Coroutine>,
173    sessions: SessionStore,
174    arena: Arena,
175    resource_states: BTreeMap<ScopeId, ResourceState>,
176    sched: Scheduler,
177    monitor: SessionMonitor,
178    obs_trace: Vec<ObsEvent>,
179    role_symbols: SymbolTable,
180    label_symbols: SymbolTable,
181    clock: SimClock,
182    next_coro_id: usize,
183    next_session_id: SessionId,
184    paused_roles: BTreeSet<String>,
185    guard_layer: InMemoryGuardLayer,
186    effect_trace: Vec<EffectTraceEntry>,
187    next_effect_id: u64,
188    output_condition_checks: Vec<OutputConditionCheck>,
189    crashed_sites: BTreeSet<SiteId>,
190    partitioned_edges: BTreeSet<(SiteId, SiteId)>,
191    corrupted_edges: BTreeMap<(SiteId, SiteId), CorruptionType>,
192    timed_out_sites: BTreeMap<SiteId, u64>,
193    last_sched_step: Option<SchedStepDebug>,
194    handler_identity_anchor: Option<String>,
195}
196
197/// Lean-aligned VM state alias.
198pub type VMState<I = (), G = (), P = NoopPersistence, Nu = DefaultVerificationModel> =
199    VM<I, G, P, Nu>;
200
201impl<I, G, P, Nu> VM<I, G, P, Nu>
202where
203    P: PersistenceModel,
204{
205    /// Create a VM for arbitrary persistence/verification model parameters.
206    #[must_use]
207    pub fn new_with_models(config: VMConfig) -> Self
208    where
209        P::PState: Default,
210        Nu: VerificationModel + Default,
211    {
212        config.assert_invariants();
213        let tick_duration = config.tick_duration;
214        let communication_replay_mode = config.communication_replay_mode;
215        let sched = Scheduler::new(config.sched_policy.clone());
216        let mut guard_resources = BTreeMap::new();
217        for layer in &config.guard_layers {
218            guard_resources.insert(layer.id.clone(), Value::Unit);
219        }
220        Self {
221            config,
222            code: None,
223            programs: Vec::new(),
224            identity_model: PhantomData,
225            guard_model: PhantomData,
226            persistence_model: PhantomData,
227            persistent: P::PState::default(),
228            verification: Nu::default(),
229            communication_consumption: DefaultCommunicationConsumption::new(
230                communication_replay_mode,
231            ),
232            communication_consumption_artifacts: Vec::new(),
233            coroutines: Vec::new(),
234            sessions: SessionStore::new(),
235            arena: Arena::default(),
236            resource_states: BTreeMap::new(),
237            sched,
238            monitor: SessionMonitor::default(),
239            obs_trace: Vec::new(),
240            role_symbols: SymbolTable::new(),
241            label_symbols: SymbolTable::new(),
242            clock: SimClock::new(tick_duration),
243            next_coro_id: 0,
244            next_session_id: 0,
245            paused_roles: BTreeSet::new(),
246            guard_layer: InMemoryGuardLayer {
247                resources: guard_resources
248                    .into_iter()
249                    .map(|(k, v)| (LayerId(k), v))
250                    .collect(),
251            },
252            effect_trace: Vec::new(),
253            next_effect_id: 0,
254            output_condition_checks: Vec::new(),
255            crashed_sites: BTreeSet::new(),
256            partitioned_edges: BTreeSet::new(),
257            corrupted_edges: BTreeMap::new(),
258            timed_out_sites: BTreeMap::new(),
259            last_sched_step: None,
260            handler_identity_anchor: None,
261        }
262    }
263
264    /// Borrow the persistent state tracked by the configured persistence model.
265    #[must_use]
266    pub fn persistent_state(&self) -> &P::PState {
267        &self.persistent
268    }
269
270    /// Mutably borrow persistent state.
271    pub fn persistent_state_mut(&mut self) -> &mut P::PState {
272        &mut self.persistent
273    }
274
275    fn apply_open_delta(&mut self, sid: SessionId) -> Result<(), String> {
276        let delta = P::open_delta(sid);
277        P::apply(&mut self.persistent, &delta)
278    }
279
280    fn apply_close_delta(&mut self, sid: SessionId) -> Result<(), String> {
281        let delta = P::close_delta(sid);
282        P::apply(&mut self.persistent, &delta)
283    }
284
285    fn apply_invoke_delta(&mut self, sid: SessionId, action: &str) -> Result<(), String> {
286        if let Some(delta) = P::invoke_delta(sid, action) {
287            P::apply(&mut self.persistent, &delta)?;
288        }
289        Ok(())
290    }
291
292    /// Resolve guard-layer capability for a participant via bridge binding.
293    #[must_use]
294    pub fn bridge_guard_layer_for_participant<B>(
295        &self,
296        bridge: &B,
297        participant: &I::ParticipantId,
298    ) -> LayerId
299    where
300        I: IdentityModel,
301        G: GuardLayer,
302        B: IdentityGuardBridge<I, G>,
303    {
304        bridge.guard_layer_for_participant(participant)
305    }
306
307    /// Resolve participant verification key via bridge binding.
308    #[must_use]
309    pub fn bridge_verifying_key_for_participant<B>(
310        &self,
311        bridge: &B,
312        participant: &I::ParticipantId,
313    ) -> Nu::VerifyingKey
314    where
315        I: IdentityModel,
316        Nu: VerificationModel,
317        B: IdentityVerificationBridge<I, Nu>,
318    {
319        bridge.verification_key_for_participant(participant)
320    }
321}
telltale_vm/vm/vm_error_and_step_pack.rs

telltale_vm/vm/
vm_error_and_step_pack.rs
