telltale_vm/instr.rs
1//! Bytecode instruction set.
2//!
3//! Matches the Lean `Instr γ ε` type from `lean/Runtime/VM/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 /// Legacy 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 /// Legacy compatibility field for register-result encoding.
99 #[serde(default)]
100 dst: Option<Reg>,
101 },
102 /// Acquire a guard layer and store evidence in a register.
103 Acquire {
104 /// Guard layer identifier.
105 layer: String,
106 /// Destination register for evidence.
107 dst: Reg,
108 },
109 /// Release a guard layer using evidence from a register.
110 Release {
111 /// Guard layer identifier.
112 layer: String,
113 /// Register holding evidence.
114 evidence: Reg,
115 },
116
117 // -- Speculation --
118 /// Enter speculation using a ghost session id.
119 Fork {
120 /// Register holding the ghost session id.
121 ghost: Reg,
122 },
123 /// Join speculative execution.
124 Join,
125 /// Abort speculative execution.
126 Abort,
127
128 // -- Ownership and knowledge --
129 /// Transfer an endpoint to another coroutine.
130 Transfer {
131 /// Register holding the endpoint.
132 endpoint: Reg,
133 /// Register holding the target coroutine id.
134 target: Reg,
135 /// Register holding a bundle descriptor.
136 bundle: Reg,
137 },
138 /// Tag a knowledge fact and return success.
139 Tag {
140 /// Register holding the fact.
141 fact: Reg,
142 /// Destination register for the result.
143 dst: Reg,
144 },
145 /// Check a knowledge fact against the flow policy.
146 Check {
147 /// Register holding the knowledge fact.
148 knowledge: Reg,
149 /// Register holding the target role.
150 target: Reg,
151 /// Destination register for the result.
152 dst: Reg,
153 },
154
155 // -- Control --
156 /// Set a register to an immediate value.
157 Set {
158 /// Destination register.
159 dst: Reg,
160 /// Immediate value to load.
161 val: ImmValue,
162 },
163 /// Copy register src to dst.
164 Move {
165 /// Destination register.
166 dst: Reg,
167 /// Source register.
168 src: Reg,
169 },
170 /// Unconditional jump.
171 Jump {
172 /// Target program counter.
173 target: PC,
174 },
175 /// Spawn a new coroutine at target PC with argument registers.
176 Spawn {
177 /// Target program counter for the spawned coroutine.
178 target: PC,
179 /// Registers to copy into the spawned coroutine argument area.
180 args: Vec<Reg>,
181 },
182 /// Yield execution to the scheduler.
183 Yield,
184 /// Halt this coroutine (normal termination).
185 Halt,
186}
187
188/// Immediate values that can be loaded into registers.
189#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
190pub enum ImmValue {
191 /// Unit value.
192 Unit,
193 /// Natural-number value (Lean-compatible).
194 Nat(u64),
195 /// Boolean value.
196 Bool(bool),
197 /// String value.
198 Str(String),
199}
200
201impl Eq for ImmValue {}