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