telltale_machine/
coroutine.rs

1//! Coroutine: lightweight execution unit within the ProtocolMachine.
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 ProtocolMachine model.
17pub type RegFile = Vec<Value>;
18
19/// Progress-token representation aligned with the Lean ProtocolMachine 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 ProtocolMachine 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    Recv {
89        /// Edge scope for the receive wait.
90        edge: Edge,
91        /// Progress token associated with the blocked receive.
92        token: ProgressToken,
93    },
94    /// Waiting for buffer space to send.
95    Send {
96        /// Edge awaiting buffer space.
97        edge: Edge,
98    },
99    /// Waiting for an effect handler response.
100    Invoke {
101        /// Effect handler identifier.
102        handler: HandlerId,
103    },
104    /// Waiting for a guard layer to allow acquisition.
105    AcquireDenied {
106        /// Guard layer identifier.
107        layer: String,
108    },
109    /// Waiting for consensus-related condition to resolve.
110    Consensus {
111        /// Consensus wait tag.
112        tag: usize,
113    },
114    /// Waiting for spawn scheduling/activation.
115    Spawn,
116    /// Waiting for a session close to complete.
117    Close {
118        /// The session being closed.
119        sid: SessionId,
120    },
121}
122
123/// Runtime fault.
124#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
125pub enum Fault {
126    /// Instruction violated the session type.
127    TypeViolation {
128        /// Expected runtime value type.
129        expected: ValType,
130        /// Actual runtime value type.
131        actual: ValType,
132        /// Description of the type violation.
133        message: String,
134    },
135    /// Unknown label in offer/choose.
136    UnknownLabel {
137        /// The unrecognized label.
138        label: String,
139    },
140    /// Channel/endpoint closed.
141    ChannelClosed {
142        /// The closed endpoint.
143        endpoint: Endpoint,
144    },
145    /// Signature evidence failed edge validation.
146    InvalidSignature {
147        /// Edge whose signature check failed.
148        edge: Edge,
149    },
150    /// Verification backend rejected a signed payload/proof.
151    VerificationFailed {
152        /// Edge whose verification failed.
153        edge: Edge,
154        /// Failure reason.
155        message: String,
156    },
157    /// Effect handler error.
158    Invoke {
159        /// Typed failure from the handler boundary.
160        failure: crate::effect::EffectFailure,
161    },
162    /// Guard layer failure.
163    Acquire {
164        /// Guard layer identifier.
165        layer: String,
166        /// Typed failure.
167        failure: crate::effect::EffectFailure,
168    },
169    /// Ownership transfer failure.
170    Transfer {
171        /// Error message.
172        message: String,
173    },
174    /// Speculation failure.
175    Speculation {
176        /// Error message.
177        message: String,
178    },
179    /// Session close error.
180    Close {
181        /// Error message from close.
182        message: String,
183    },
184    /// Protocol-level flow invariant violation.
185    FlowViolation {
186        /// Violation detail.
187        message: String,
188    },
189    /// Missing progress token for a required edge action.
190    NoProgressToken {
191        /// Edge missing a valid progress token.
192        edge: Edge,
193    },
194    /// Output-condition commit gate rejected emitted outputs.
195    OutputCondition {
196        /// Predicate reference that failed verification.
197        predicate_ref: String,
198    },
199    /// Register out of bounds.
200    OutOfRegisters,
201    /// PC out of bounds.
202    PcOutOfBounds,
203    /// Buffer full and backpressure policy is error.
204    BufferFull {
205        /// The full endpoint buffer.
206        endpoint: Endpoint,
207    },
208    /// Coroutine exhausted its deterministic execution budget.
209    OutOfCredits,
210}
211
212impl std::fmt::Display for Fault {
213    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
214        match self {
215            Self::TypeViolation {
216                expected,
217                actual,
218                message,
219            } => write!(
220                f,
221                "type violation (expected {expected:?}, actual {actual:?}): {message}"
222            ),
223            Self::UnknownLabel { label } => write!(f, "unknown label: {label}"),
224            Self::ChannelClosed { endpoint } => {
225                write!(f, "channel closed: {}:{}", endpoint.sid, endpoint.role)
226            }
227            Self::InvalidSignature { edge } => write!(
228                f,
229                "invalid signature on edge {}:{}→{}",
230                edge.sid, edge.sender, edge.receiver
231            ),
232            Self::VerificationFailed { edge, message } => write!(
233                f,
234                "verification failed on edge {}:{}→{}: {message}",
235                edge.sid, edge.sender, edge.receiver
236            ),
237            Self::Invoke { failure } => write!(f, "invoke fault: {failure}"),
238            Self::Acquire { layer, failure } => {
239                write!(f, "acquire fault ({layer}): {failure}")
240            }
241            Self::Transfer { message } => write!(f, "transfer fault: {message}"),
242            Self::Speculation { message } => write!(f, "speculation fault: {message}"),
243            Self::Close { message } => write!(f, "close fault: {message}"),
244            Self::FlowViolation { message } => write!(f, "flow violation: {message}"),
245            Self::NoProgressToken { edge } => write!(
246                f,
247                "missing progress token for edge {}:{}→{}",
248                edge.sid, edge.sender, edge.receiver
249            ),
250            Self::OutputCondition { predicate_ref } => {
251                write!(f, "output-condition rejected: {predicate_ref}")
252            }
253            Self::OutOfRegisters => write!(f, "out of registers"),
254            Self::PcOutOfBounds => write!(f, "PC out of bounds"),
255            Self::BufferFull { endpoint } => {
256                write!(f, "buffer full: {}:{}", endpoint.sid, endpoint.role)
257            }
258            Self::OutOfCredits => write!(f, "out of credits"),
259        }
260    }
261}
262
263/// A single coroutine executing a role's local protocol.
264#[derive(Debug, Clone, Serialize, Deserialize)]
265pub struct Coroutine<E = ()> {
266    /// Unique coroutine identifier.
267    pub id: usize,
268    /// Program table index for instruction fetch.
269    pub program_id: usize,
270    /// Program counter.
271    pub pc: PC,
272    /// Register file.
273    pub regs: RegFile,
274    /// Execution status.
275    pub status: CoroStatus,
276    /// Effect execution context.
277    #[serde(default)]
278    pub effect_ctx: EffectCtx<E>,
279    /// Endpoints owned by this coroutine.
280    pub owned_endpoints: Vec<Endpoint>,
281    /// Progress tokens for scheduling.
282    pub progress_tokens: Vec<ProgressToken>,
283    /// Knowledge facts owned by this coroutine.
284    pub knowledge_set: KnowledgeSet,
285    /// Speculation state, if any.
286    pub spec_state: Option<SpeculationState>,
287    /// Session this coroutine participates in.
288    pub session_id: SessionId,
289    /// Role name within the session.
290    pub role: String,
291    /// Remaining instruction budget for deterministic cost accounting.
292    #[serde(default = "default_cost_budget")]
293    pub cost_budget: usize,
294}
295
296/// Lean-aligned coroutine state alias.
297pub type CoroutineState<E = ()> = Coroutine<E>;
298
299/// Knowledge fact for ownership checks.
300#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
301pub struct KnowledgeFact {
302    /// Endpoint that the fact is about.
303    pub endpoint: Endpoint,
304    /// String fact payload.
305    pub fact: String,
306}
307
308/// Lean-aligned knowledge set type.
309pub type KnowledgeSet = Vec<KnowledgeFact>;
310
311/// Speculation state for a coroutine.
312#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
313pub struct SpeculationState {
314    /// Ghost session identifier.
315    pub ghost_sid: usize,
316    /// Speculation depth.
317    pub depth: usize,
318}
319
320impl Coroutine {
321    /// Create a new coroutine.
322    #[must_use]
323    pub fn new(
324        id: usize,
325        program_id: usize,
326        session_id: SessionId,
327        role: String,
328        num_regs: u16,
329        cost_budget: usize,
330    ) -> Self {
331        Self {
332            id,
333            program_id,
334            pc: 0,
335            regs: vec![Value::Unit; usize::from(num_regs)],
336            status: CoroStatus::Ready,
337            effect_ctx: EffectCtx::default(),
338            owned_endpoints: Vec::with_capacity(1),
339            progress_tokens: Vec::with_capacity(1),
340            knowledge_set: Vec::with_capacity(1),
341            spec_state: None,
342            session_id,
343            role,
344            cost_budget,
345        }
346    }
347
348    /// Whether this coroutine is ready to execute.
349    #[must_use]
350    pub fn is_ready(&self) -> bool {
351        self.status == CoroStatus::Ready
352    }
353
354    /// Whether this coroutine has finished (done or faulted).
355    #[must_use]
356    pub fn is_terminal(&self) -> bool {
357        matches!(self.status, CoroStatus::Done | CoroStatus::Faulted(_))
358    }
359}
360
361impl Fault {
362    /// Build a type-violation fault when only a textual diagnostic is available.
363    #[must_use]
364    pub fn type_violation(message: impl Into<String>) -> Self {
365        Self::TypeViolation {
366            expected: ValType::Unit,
367            actual: ValType::Unit,
368            message: message.into(),
369        }
370    }
371}
telltale_machine/coroutine.rs

telltale_machine/
coroutine.rs
