telltale_machine/
instr.rs

1//! Bytecode instruction set.
2//!
3//! Matches the Lean `Instr γ ε` type from `lean/Runtime/ProtocolMachine/Model/Core.lean`.
4//! Registers are `u16` indices, PC is `usize`.
5
6use serde::{Deserialize, Serialize};
7
8use crate::session::SessionId;
9
10/// Register index.
11pub type Reg = u16;
12
13/// Program counter.
14pub type PC = usize;
15
16/// Effect action descriptor carried by `Invoke`.
17#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
18#[serde(untagged)]
19pub enum InvokeAction {
20    /// Named action descriptor (Lean-aligned shape).
21    Named(String),
22    /// Register-carried action descriptor.
23    Reg(Reg),
24}
25
26/// Structured endpoint: identifies a role within a session.
27///
28/// Matches the Lean `Endpoint` which carries `{ sid, role }`.
29/// The session store uses this as the key for local type state.
30#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)]
31pub struct Endpoint {
32    /// Session this endpoint belongs to.
33    pub sid: SessionId,
34    /// Role name within the session.
35    pub role: String,
36}
37
38/// Bytecode instruction.
39///
40/// The initial instruction set covers communication, session lifecycle,
41/// effects, and control flow. Guard/speculation/ownership instructions
42/// are deferred.
43#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
44pub enum Instr {
45    // -- Communication --
46    /// Send value in `val` register to channel in `chan` register.
47    Send {
48        /// Channel register.
49        chan: Reg,
50        /// Value register to send.
51        val: Reg,
52    },
53    /// Receive from channel in `chan` register, store in `dst` register.
54    Receive {
55        /// Channel register.
56        chan: Reg,
57        /// Destination register for the received value.
58        dst: Reg,
59    },
60    /// Offer a label on channel.
61    Offer {
62        /// Channel register.
63        chan: Reg,
64        /// Label to select.
65        label: String,
66    },
67    /// Choose from a branch table using a received label.
68    Choose {
69        /// Channel register.
70        chan: Reg,
71        /// Label-to-PC jump table.
72        table: Vec<(String, PC)>,
73    },
74
75    // -- Session lifecycle --
76    /// Open a new session with the given roles and endpoint destinations.
77    Open {
78        /// Role names for the session.
79        roles: Vec<String>,
80        /// Role-to-local-type mappings for session initialization.
81        local_types: Vec<(String, telltale_types::LocalTypeR)>,
82        /// Edge-to-handler mappings as `((sender, receiver), handler_id)`.
83        handlers: Vec<((String, String), String)>,
84        /// Role-to-register endpoint mappings.
85        dsts: Vec<(String, Reg)>,
86    },
87    /// Close the session referenced by the register.
88    Close {
89        /// Register holding the session reference.
90        session: Reg,
91    },
92
93    // -- Effects --
94    /// Invoke an effect handler action.
95    Invoke {
96        /// Action descriptor.
97        action: InvokeAction,
98    },
99    /// Acquire a guard layer and store evidence in a register.
100    Acquire {
101        /// Guard layer identifier.
102        layer: String,
103        /// Destination register for evidence.
104        dst: Reg,
105    },
106    /// Release a guard layer using evidence from a register.
107    Release {
108        /// Guard layer identifier.
109        layer: String,
110        /// Register holding evidence.
111        evidence: Reg,
112    },
113
114    // -- Speculation --
115    /// Enter speculation using a ghost session id.
116    Fork {
117        /// Register holding the ghost session id.
118        ghost: Reg,
119    },
120    /// Join speculative execution.
121    Join,
122    /// Abort speculative execution.
123    Abort,
124
125    // -- Ownership and knowledge --
126    /// Transfer an endpoint to another coroutine.
127    Transfer {
128        /// Register holding the endpoint.
129        endpoint: Reg,
130        /// Register holding the target coroutine id.
131        target: Reg,
132        /// Register holding a bundle descriptor.
133        bundle: Reg,
134    },
135    /// Tag a knowledge fact and return success.
136    Tag {
137        /// Register holding the fact.
138        fact: Reg,
139        /// Destination register for the result.
140        dst: Reg,
141    },
142    /// Check a knowledge fact against the flow policy.
143    Check {
144        /// Register holding the knowledge fact.
145        knowledge: Reg,
146        /// Register holding the target role.
147        target: Reg,
148        /// Destination register for the result.
149        dst: Reg,
150    },
151
152    // -- Control --
153    /// Set a register to an immediate value.
154    Set {
155        /// Destination register.
156        dst: Reg,
157        /// Immediate value to load.
158        val: ImmValue,
159    },
160    /// Copy register src to dst.
161    Move {
162        /// Destination register.
163        dst: Reg,
164        /// Source register.
165        src: Reg,
166    },
167    /// Unconditional jump.
168    Jump {
169        /// Target program counter.
170        target: PC,
171    },
172    /// Spawn a new coroutine at target PC with argument registers.
173    Spawn {
174        /// Target program counter for the spawned coroutine.
175        target: PC,
176        /// Registers to copy into the spawned coroutine argument area.
177        args: Vec<Reg>,
178    },
179    /// Yield execution to the scheduler.
180    Yield,
181    /// Halt this coroutine (normal termination).
182    Halt,
183}
184
185/// Immediate values that can be loaded into registers.
186#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
187pub enum ImmValue {
188    /// Unit value.
189    Unit,
190    /// Natural-number value (Lean-compatible).
191    Nat(u64),
192    /// Boolean value.
193    Bool(bool),
194    /// String value.
195    Str(String),
196}
197
198impl Eq for ImmValue {}
telltale_machine/instr.rs

telltale_machine/
instr.rs
