telltale_vm/
coroutine.rs

1//! Coroutine: lightweight execution unit within the VM.
2//!
3//! Each role in a choreography runs as a coroutine with its own PC,
4//! register file, and status. Matches the Lean `Coroutine` structure.
5
6use serde::{Deserialize, Serialize};
7use telltale_types::ValType;
8
9use crate::instr::{Endpoint, PC};
10use crate::session::{Edge, HandlerId, SessionId};
11
12fn default_cost_budget() -> usize {
13    usize::MAX
14}
15
16/// Register-file representation aligned with the Lean VM model.
17pub type RegFile = Vec<Value>;
18
19/// Progress-token representation aligned with the Lean VM model.
20#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
21pub struct ProgressToken {
22    /// Session this token is scoped to.
23    pub sid: SessionId,
24    /// Endpoint this token authorizes progress for.
25    pub endpoint: Endpoint,
26}
27
28impl ProgressToken {
29    /// Construct a token from an endpoint.
30    #[must_use]
31    pub fn for_endpoint(endpoint: Endpoint) -> Self {
32        Self {
33            sid: endpoint.sid,
34            endpoint,
35        }
36    }
37}
38
39/// Effect context for coroutine execution, aligned with the Lean VM model.
40#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
41pub struct EffectCtx<E = ()> {
42    /// Optional effect metadata captured for replay/introspection.
43    pub last_effect: Option<E>,
44}
45
46impl<E> Default for EffectCtx<E> {
47    fn default() -> Self {
48        Self { last_effect: None }
49    }
50}
51
52/// Runtime value stored in registers and buffers.
53#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
54pub enum Value {
55    /// Unit / no value.
56    Unit,
57    /// Natural number (Lean-compatible).
58    Nat(u64),
59    /// Boolean.
60    Bool(bool),
61    /// String.
62    Str(String),
63    /// Product pair value (Lean-compatible).
64    Prod(Box<Value>, Box<Value>),
65    /// Endpoint reference for ownership and guard operations.
66    Endpoint(Endpoint),
67}
68
69/// Coroutine execution status.
70#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
71pub enum CoroStatus {
72    /// Ready to execute.
73    Ready,
74    /// Blocked waiting on something.
75    Blocked(BlockReason),
76    /// Completed normally.
77    Done,
78    /// Faulted with an error.
79    Faulted(Fault),
80    /// Running under speculative execution mode.
81    Speculating,
82}
83
84/// Why a coroutine is blocked.
85#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
86pub enum BlockReason {
87    /// Waiting to receive on an edge.
88    #[serde(alias = "RecvWait")]
89    Recv {
90        /// Edge scope for the receive wait.
91        edge: Edge,
92        /// Progress token associated with the blocked receive.
93        token: ProgressToken,
94    },
95    /// Waiting for buffer space to send.
96    #[serde(alias = "SendWait")]
97    Send {
98        /// Edge awaiting buffer space.
99        edge: Edge,
100    },
101    /// Waiting for an effect handler response.
102    #[serde(alias = "InvokeWait")]
103    Invoke {
104        /// Effect handler identifier.
105        handler: HandlerId,
106    },
107    /// Waiting for a guard layer to allow acquisition.
108    AcquireDenied {
109        /// Guard layer identifier.
110        layer: String,
111    },
112    /// Waiting for consensus-related condition to resolve.
113    #[serde(alias = "ConsensusWait")]
114    Consensus {
115        /// Consensus wait tag.
116        tag: usize,
117    },
118    /// Waiting for spawn scheduling/activation.
119    #[serde(alias = "SpawnWait")]
120    Spawn,
121    /// Waiting for a session close to complete.
122    #[serde(alias = "CloseWait")]
123    Close {
124        /// The session being closed.
125        sid: SessionId,
126    },
127}
128
129/// Runtime fault.
130#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
131pub enum Fault {
132    /// Instruction violated the session type.
133    TypeViolation {
134        /// Expected runtime value type.
135        expected: ValType,
136        /// Actual runtime value type.
137        actual: ValType,
138        /// Description of the type violation.
139        message: String,
140    },
141    /// Unknown label in offer/choose.
142    UnknownLabel {
143        /// The unrecognized label.
144        label: String,
145    },
146    /// Channel/endpoint closed.
147    ChannelClosed {
148        /// The closed endpoint.
149        endpoint: Endpoint,
150    },
151    /// Signature evidence failed edge validation.
152    InvalidSignature {
153        /// Edge whose signature check failed.
154        edge: Edge,
155    },
156    /// Verification backend rejected a signed payload/proof.
157    VerificationFailed {
158        /// Edge whose verification failed.
159        edge: Edge,
160        /// Failure reason.
161        message: String,
162    },
163    /// Effect handler error.
164    #[serde(alias = "InvokeFault")]
165    Invoke {
166        /// Error message from the handler.
167        message: String,
168    },
169    /// Guard layer failure.
170    #[serde(alias = "AcquireFault")]
171    Acquire {
172        /// Guard layer identifier.
173        layer: String,
174        /// Error message.
175        message: String,
176    },
177    /// Ownership transfer failure.
178    #[serde(alias = "TransferFault")]
179    Transfer {
180        /// Error message.
181        message: String,
182    },
183    /// Speculation failure.
184    #[serde(alias = "SpecFault")]
185    Speculation {
186        /// Error message.
187        message: String,
188    },
189    /// Session close error.
190    #[serde(alias = "CloseFault")]
191    Close {
192        /// Error message from close.
193        message: String,
194    },
195    /// Protocol-level flow invariant violation.
196    FlowViolation {
197        /// Violation detail.
198        message: String,
199    },
200    /// Missing progress token for a required edge action.
201    NoProgressToken {
202        /// Edge missing a valid progress token.
203        edge: Edge,
204    },
205    /// Output-condition commit gate rejected emitted outputs.
206    #[serde(alias = "OutputConditionFault")]
207    OutputCondition {
208        /// Predicate reference that failed verification.
209        predicate_ref: String,
210    },
211    /// Register out of bounds.
212    OutOfRegisters,
213    /// PC out of bounds.
214    PcOutOfBounds,
215    /// Buffer full and backpressure policy is error.
216    BufferFull {
217        /// The full endpoint buffer.
218        endpoint: Endpoint,
219    },
220    /// Coroutine exhausted its deterministic execution budget.
221    OutOfCredits,
222}
223
224impl std::fmt::Display for Fault {
225    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
226        match self {
227            Self::TypeViolation {
228                expected,
229                actual,
230                message,
231            } => write!(
232                f,
233                "type violation (expected {expected:?}, actual {actual:?}): {message}"
234            ),
235            Self::UnknownLabel { label } => write!(f, "unknown label: {label}"),
236            Self::ChannelClosed { endpoint } => {
237                write!(f, "channel closed: {}:{}", endpoint.sid, endpoint.role)
238            }
239            Self::InvalidSignature { edge } => write!(
240                f,
241                "invalid signature on edge {}:{}→{}",
242                edge.sid, edge.sender, edge.receiver
243            ),
244            Self::VerificationFailed { edge, message } => write!(
245                f,
246                "verification failed on edge {}:{}→{}: {message}",
247                edge.sid, edge.sender, edge.receiver
248            ),
249            Self::Invoke { message } => write!(f, "invoke fault: {message}"),
250            Self::Acquire { layer, message } => {
251                write!(f, "acquire fault ({layer}): {message}")
252            }
253            Self::Transfer { message } => write!(f, "transfer fault: {message}"),
254            Self::Speculation { message } => write!(f, "speculation fault: {message}"),
255            Self::Close { message } => write!(f, "close fault: {message}"),
256            Self::FlowViolation { message } => write!(f, "flow violation: {message}"),
257            Self::NoProgressToken { edge } => write!(
258                f,
259                "missing progress token for edge {}:{}→{}",
260                edge.sid, edge.sender, edge.receiver
261            ),
262            Self::OutputCondition { predicate_ref } => {
263                write!(f, "output-condition rejected: {predicate_ref}")
264            }
265            Self::OutOfRegisters => write!(f, "out of registers"),
266            Self::PcOutOfBounds => write!(f, "PC out of bounds"),
267            Self::BufferFull { endpoint } => {
268                write!(f, "buffer full: {}:{}", endpoint.sid, endpoint.role)
269            }
270            Self::OutOfCredits => write!(f, "out of credits"),
271        }
272    }
273}
274
275/// A single coroutine executing a role's local protocol.
276#[derive(Debug, Clone, Serialize, Deserialize)]
277pub struct Coroutine<E = ()> {
278    /// Unique coroutine identifier.
279    pub id: usize,
280    /// Program table index for instruction fetch.
281    pub program_id: usize,
282    /// Program counter.
283    pub pc: PC,
284    /// Register file.
285    pub regs: RegFile,
286    /// Execution status.
287    pub status: CoroStatus,
288    /// Effect execution context.
289    #[serde(default)]
290    pub effect_ctx: EffectCtx<E>,
291    /// Endpoints owned by this coroutine.
292    pub owned_endpoints: Vec<Endpoint>,
293    /// Progress tokens for scheduling.
294    pub progress_tokens: Vec<ProgressToken>,
295    /// Knowledge facts owned by this coroutine.
296    pub knowledge_set: KnowledgeSet,
297    /// Speculation state, if any.
298    pub spec_state: Option<SpeculationState>,
299    /// Session this coroutine participates in.
300    pub session_id: SessionId,
301    /// Role name within the session.
302    pub role: String,
303    /// Remaining instruction budget for deterministic cost accounting.
304    #[serde(default = "default_cost_budget")]
305    pub cost_budget: usize,
306}
307
308/// Lean-aligned coroutine state alias.
309pub type CoroutineState<E = ()> = Coroutine<E>;
310
311/// Knowledge fact for ownership checks.
312#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
313pub struct KnowledgeFact {
314    /// Endpoint that the fact is about.
315    pub endpoint: Endpoint,
316    /// String fact payload.
317    pub fact: String,
318}
319
320/// Lean-aligned knowledge set type.
321pub type KnowledgeSet = Vec<KnowledgeFact>;
322
323/// Speculation state for a coroutine.
324#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
325pub struct SpeculationState {
326    /// Ghost session identifier.
327    pub ghost_sid: usize,
328    /// Speculation depth.
329    pub depth: usize,
330}
331
332impl Coroutine {
333    /// Create a new coroutine.
334    #[must_use]
335    pub fn new(
336        id: usize,
337        program_id: usize,
338        session_id: SessionId,
339        role: String,
340        num_regs: u16,
341        cost_budget: usize,
342    ) -> Self {
343        Self {
344            id,
345            program_id,
346            pc: 0,
347            regs: vec![Value::Unit; usize::from(num_regs)],
348            status: CoroStatus::Ready,
349            effect_ctx: EffectCtx::default(),
350            owned_endpoints: Vec::with_capacity(1),
351            progress_tokens: Vec::with_capacity(1),
352            knowledge_set: Vec::with_capacity(1),
353            spec_state: None,
354            session_id,
355            role,
356            cost_budget,
357        }
358    }
359
360    /// Whether this coroutine is ready to execute.
361    #[must_use]
362    pub fn is_ready(&self) -> bool {
363        self.status == CoroStatus::Ready
364    }
365
366    /// Whether this coroutine has finished (done or faulted).
367    #[must_use]
368    pub fn is_terminal(&self) -> bool {
369        matches!(self.status, CoroStatus::Done | CoroStatus::Faulted(_))
370    }
371}
372
373impl Fault {
374    /// Build a type-violation fault when only a textual diagnostic is available.
375    #[must_use]
376    pub fn type_violation(message: impl Into<String>) -> Self {
377        Self::TypeViolation {
378            expected: ValType::Unit,
379            actual: ValType::Unit,
380            message: message.into(),
381        }
382    }
383}
telltale_vm/coroutine.rs

telltale_vm/
coroutine.rs
