miden_core/
sys_events.rs

1use core::fmt;
2
3// SYSTEM EVENTS
4// ================================================================================================
5
6// Randomly generated constant values for the VM's system events. All values were sampled
7// between 0 and 2^32.
8pub use constants::*;
9
10#[rustfmt::skip]
11mod constants {
12    pub const EVENT_MERKLE_NODE_MERGE: u32            = 276124218;
13    pub const EVENT_MERKLE_NODE_TO_STACK: u32         = 361943238;
14    pub const EVENT_MAP_VALUE_TO_STACK: u32           = 574478993;
15    pub const EVENT_MAP_VALUE_TO_STACK_N: u32         = 630847990;
16    pub const EVENT_U64_DIV: u32                      = 678156251;
17    pub const EVENT_EXT2_INV: u32                     = 1251967401;
18    pub const EVENT_EXT2_INTT: u32                    = 1347499010;
19    pub const EVENT_SMT_PEEK: u32                     = 1889584556;
20    pub const EVENT_U32_CLZ: u32                      = 1951932030;
21    pub const EVENT_U32_CTZ: u32                      = 2008979519;
22    pub const EVENT_U32_CLO: u32                      = 2032895094;
23    pub const EVENT_U32_CTO: u32                      = 2083700134;
24    pub const EVENT_ILOG2: u32                        = 2297972669;
25    pub const EVENT_MEM_TO_MAP: u32                   = 2389394361;
26    pub const EVENT_HDWORD_TO_MAP: u32                = 2391452729;
27    pub const EVENT_HDWORD_TO_MAP_WITH_DOMAIN: u32    = 2822590340;
28    pub const EVENT_HPERM_TO_MAP: u32                 = 3297060969;
29    pub const EVENT_FALCON_DIV: u32                   = 3419226155;
30}
31
32/// Defines a set of actions which can be initiated from the VM to inject new data into the advice
33/// provider.
34///
35/// These actions can affect all 3 components of the advice provider: Merkle store, advice stack,
36/// and advice map.
37///
38/// All actions, except for `MerkleNodeMerge`, `Ext2Inv` and `UpdateMerkleNode` can be invoked
39/// directly from Miden assembly via dedicated instructions.
40#[derive(Copy, Clone, Debug, Eq, PartialEq)]
41pub enum SystemEvent {
42    // MERKLE STORE EVENTS
43    // --------------------------------------------------------------------------------------------
44    /// Creates a new Merkle tree in the advice provider by combining Merkle trees with the
45    /// specified roots. The root of the new tree is defined as `Hash(LEFT_ROOT, RIGHT_ROOT)`.
46    ///
47    /// Inputs:
48    ///   Operand stack: [RIGHT_ROOT, LEFT_ROOT, ...]
49    ///   Merkle store: {RIGHT_ROOT, LEFT_ROOT}
50    ///
51    /// Outputs:
52    ///   Operand stack: [RIGHT_ROOT, LEFT_ROOT, ...]
53    ///   Merkle store: {RIGHT_ROOT, LEFT_ROOT, hash(LEFT_ROOT, RIGHT_ROOT)}
54    ///
55    /// After the operation, both the original trees and the new tree remains in the advice
56    /// provider (i.e., the input trees are not removed).
57    MerkleNodeMerge,
58
59    // ADVICE STACK SYSTEM EVENTS
60    // --------------------------------------------------------------------------------------------
61    /// Pushes a node of the Merkle tree specified by the values on the top of the operand stack
62    /// onto the advice stack.
63    ///
64    /// Inputs:
65    ///   Operand stack: [depth, index, TREE_ROOT, ...]
66    ///   Advice stack: [...]
67    ///   Merkle store: {TREE_ROOT<-NODE}
68    ///
69    /// Outputs:
70    ///   Operand stack: [depth, index, TREE_ROOT, ...]
71    ///   Advice stack: [NODE, ...]
72    ///   Merkle store: {TREE_ROOT<-NODE}
73    MerkleNodeToStack,
74
75    /// Pushes a list of field elements onto the advice stack. The list is looked up in the advice
76    /// map using the specified word from the operand stack as the key.
77    ///
78    /// Inputs:
79    ///   Operand stack: [KEY, ...]
80    ///   Advice stack: [...]
81    ///   Advice map: {KEY: values}
82    ///
83    /// Outputs:
84    ///   Operand stack: [KEY, ...]
85    ///   Advice stack: [values, ...]
86    ///   Advice map: {KEY: values}
87    MapValueToStack,
88
89    /// Pushes a list of field elements onto the advice stack, and then the number of elements
90    /// pushed. The list is looked up in the advice map using the specified word from the operand
91    /// stack as the key.
92    ///
93    /// Inputs:
94    ///   Operand stack: [KEY, ...]
95    ///   Advice stack: [...]
96    ///   Advice map: {KEY: values}
97    ///
98    /// Outputs:
99    ///   Operand stack: [KEY, ...]
100    ///   Advice stack: [num_values, values, ...]
101    ///   Advice map: {KEY: values}
102    MapValueToStackN,
103
104    /// Pushes the result of [u64] division (both the quotient and the remainder) onto the advice
105    /// stack.
106    ///
107    /// Inputs:
108    ///   Operand stack: [b1, b0, a1, a0, ...]
109    ///   Advice stack: [...]
110    ///
111    /// Outputs:
112    ///   Operand stack: [b1, b0, a1, a0, ...]
113    ///   Advice stack: [q0, q1, r0, r1, ...]
114    ///
115    /// Where (a0, a1) and (b0, b1) are the 32-bit limbs of the dividend and the divisor
116    /// respectively (with a0 representing the 32 lest significant bits and a1 representing the
117    /// 32 most significant bits). Similarly, (q0, q1) and (r0, r1) represent the quotient and
118    /// the remainder respectively.
119    U64Div,
120
121    /// Pushes the result of divison (both the quotient and the remainder) of a [u64] by the Falcon
122    /// prime (M = 12289) onto the advice stack.
123    ///
124    /// Inputs:
125    ///   Operand stack: [a1, a0, ...]
126    ///   Advice stack: [...]
127    ///
128    /// Outputs:
129    ///   Operand stack: [a1, a0, ...]
130    ///   Advice stack: [q0, q1, r, ...]
131    ///
132    /// Where (a0, a1) are the 32-bit limbs of the dividend (with a0 representing the 32 least
133    /// significant bits and a1 representing the 32 most significant bits).
134    /// Similarly, (q0, q1) represent the quotient and r the remainder.
135    FalconDiv,
136
137    /// Given an element in a quadratic extension field on the top of the stack (i.e., a0, b1),
138    /// computes its multiplicative inverse and push the result onto the advice stack.
139    ///
140    /// Inputs:
141    ///   Operand stack: [a1, a0, ...]
142    ///   Advice stack: [...]
143    ///
144    /// Outputs:
145    ///   Operand stack: [a1, a0, ...]
146    ///   Advice stack: [b0, b1...]
147    ///
148    /// Where (b0, b1) is the multiplicative inverse of the extension field element (a0, a1) at the
149    /// top of the stack.
150    Ext2Inv,
151
152    /// Given evaluations of a polynomial over some specified domain, interpolates the evaluations
153    ///  into a polynomial in coefficient form and pushes the result into the advice stack.
154    ///
155    /// The interpolation is performed using the iNTT algorithm. The evaluations are expected to be
156    /// in the quadratic extension.
157    ///
158    /// Inputs:
159    ///   Operand stack: [output_size, input_size, input_start_ptr, ...]
160    ///   Advice stack: [...]
161    ///
162    /// Outputs:
163    ///   Operand stack: [output_size, input_size, input_start_ptr, ...]
164    ///   Advice stack: [coefficients...]
165    ///
166    /// - `input_size` is the number of evaluations (each evaluation is 2 base field elements). Must
167    ///   be a power of 2 and greater 1.
168    /// - `output_size` is the number of coefficients in the interpolated polynomial (each
169    ///   coefficient is 2 base field elements). Must be smaller than or equal to the number of
170    ///   input evaluations.
171    /// - `input_start_ptr` is the memory address of the first evaluation.
172    /// - `coefficients` are the coefficients of the interpolated polynomial such that lowest degree
173    ///   coefficients are located at the top of the advice stack.
174    Ext2Intt,
175
176    /// Pushes onto the advice stack the value associated with the specified key in a Sparse
177    /// Merkle Tree defined by the specified root.
178    ///
179    /// If no value was previously associated with the specified key, [ZERO; 4] is pushed onto
180    /// the advice stack.
181    ///
182    /// Inputs:
183    ///   Operand stack: [KEY, ROOT, ...]
184    ///   Advice stack: [...]
185    ///
186    /// Outputs:
187    ///   Operand stack: [KEY, ROOT, ...]
188    ///   Advice stack: [VALUE, ...]
189    SmtPeek,
190
191    /// Pushes the number of the leading zeros of the top stack element onto the advice stack.
192    ///
193    /// Inputs:
194    ///   Operand stack: [n, ...]
195    ///   Advice stack: [...]
196    ///
197    /// Outputs:
198    ///   Operand stack: [n, ...]
199    ///   Advice stack: [leading_zeros, ...]
200    U32Clz,
201
202    /// Pushes the number of the trailing zeros of the top stack element onto the advice stack.
203    ///
204    /// Inputs:
205    ///   Operand stack: [n, ...]
206    ///   Advice stack: [...]
207    ///
208    /// Outputs:
209    ///   Operand stack: [n, ...]
210    ///   Advice stack: [trailing_zeros, ...]
211    U32Ctz,
212
213    /// Pushes the number of the leading ones of the top stack element onto the advice stack.
214    ///
215    /// Inputs:
216    ///   Operand stack: [n, ...]
217    ///   Advice stack: [...]
218    ///
219    /// Outputs:
220    ///   Operand stack: [n, ...]
221    ///   Advice stack: [leading_ones, ...]
222    U32Clo,
223
224    /// Pushes the number of the trailing ones of the top stack element onto the advice stack.
225    ///
226    /// Inputs:
227    ///   Operand stack: [n, ...]
228    ///   Advice stack: [...]
229    ///
230    /// Outputs:
231    ///   Operand stack: [n, ...]
232    ///   Advice stack: [trailing_ones, ...]
233    U32Cto,
234
235    /// Pushes the base 2 logarithm of the top stack element, rounded down.
236    /// Inputs:
237    ///   Operand stack: [n, ...]
238    ///   Advice stack: [...]
239    ///
240    /// Outputs:
241    ///   Operand stack: [n, ...]
242    ///   Advice stack: [ilog2(n), ...]
243    ILog2,
244
245    // ADVICE MAP SYSTEM EVENTS
246    // --------------------------------------------------------------------------------------------
247    /// Reads words from memory at the specified range and inserts them into the advice map under
248    /// the key `KEY` located at the top of the stack.
249    ///
250    /// Inputs:
251    ///   Operand stack: [KEY, start_addr, end_addr, ...]
252    ///   Advice map: {...}
253    ///
254    /// Outputs:
255    ///   Operand stack: [KEY, start_addr, end_addr, ...]
256    ///   Advice map: {KEY: values}
257    ///
258    /// Where `values` are the elements located in memory[start_addr..end_addr].
259    MemToMap,
260
261    /// Reads two word from the operand stack and inserts them into the advice map under the key
262    /// defined by the hash of these words.
263    ///
264    /// Inputs:
265    ///   Operand stack: [B, A, ...]
266    ///   Advice map: {...}
267    ///
268    /// Outputs:
269    ///   Operand stack: [B, A, ...]
270    ///   Advice map: {KEY: [a0, a1, a2, a3, b0, b1, b2, b3]}
271    ///
272    /// Where KEY is computed as hash(A || B, domain=0)
273    HdwordToMap,
274
275    /// Reads two word from the operand stack and inserts them into the advice map under the key
276    /// defined by the hash of these words (using `d` as the domain).
277    ///
278    /// Inputs:
279    ///   Operand stack: [B, A, d, ...]
280    ///   Advice map: {...}
281    ///
282    /// Outputs:
283    ///   Operand stack: [B, A, d, ...]
284    ///   Advice map: {KEY: [a0, a1, a2, a3, b0, b1, b2, b3]}
285    ///
286    /// Where KEY is computed as hash(A || B, d).
287    HdwordToMapWithDomain,
288
289    /// Reads three words from the operand stack and inserts the top two words into the advice map
290    /// under the key defined by applying an RPO permutation to all three words.
291    ///
292    /// Inputs:
293    ///   Operand stack: [B, A, C, ...]
294    ///   Advice map: {...}
295    ///
296    /// Outputs:
297    ///   Operand stack: [B, A, C, ...]
298    ///   Advice map: {KEY: [a0, a1, a2, a3, b0, b1, b2, b3]}
299    ///
300    /// Where KEY is computed by extracting the digest elements from hperm([C, A, B]). For example,
301    /// if C is [0, d, 0, 0], KEY will be set as hash(A || B, d).
302    HpermToMap,
303}
304
305impl SystemEvent {
306    pub fn into_event_id(self) -> u32 {
307        match self {
308            SystemEvent::MerkleNodeMerge => EVENT_MERKLE_NODE_MERGE,
309            SystemEvent::MerkleNodeToStack => EVENT_MERKLE_NODE_TO_STACK,
310            SystemEvent::MapValueToStack => EVENT_MAP_VALUE_TO_STACK,
311            SystemEvent::MapValueToStackN => EVENT_MAP_VALUE_TO_STACK_N,
312            SystemEvent::U64Div => EVENT_U64_DIV,
313            SystemEvent::FalconDiv => EVENT_FALCON_DIV,
314            SystemEvent::Ext2Inv => EVENT_EXT2_INV,
315            SystemEvent::Ext2Intt => EVENT_EXT2_INTT,
316            SystemEvent::SmtPeek => EVENT_SMT_PEEK,
317            SystemEvent::U32Clz => EVENT_U32_CLZ,
318            SystemEvent::U32Ctz => EVENT_U32_CTZ,
319            SystemEvent::U32Clo => EVENT_U32_CLO,
320            SystemEvent::U32Cto => EVENT_U32_CTO,
321            SystemEvent::ILog2 => EVENT_ILOG2,
322            SystemEvent::MemToMap => EVENT_MEM_TO_MAP,
323            SystemEvent::HdwordToMap => EVENT_HDWORD_TO_MAP,
324            SystemEvent::HdwordToMapWithDomain => EVENT_HDWORD_TO_MAP_WITH_DOMAIN,
325            SystemEvent::HpermToMap => EVENT_HPERM_TO_MAP,
326        }
327    }
328
329    /// Returns a system event corresponding to the specified event ID, or `None` if the event
330    /// ID is not recognized.
331    pub fn from_event_id(event_id: u32) -> Option<Self> {
332        match event_id {
333            EVENT_MERKLE_NODE_MERGE => Some(SystemEvent::MerkleNodeMerge),
334            EVENT_MERKLE_NODE_TO_STACK => Some(SystemEvent::MerkleNodeToStack),
335            EVENT_MAP_VALUE_TO_STACK => Some(SystemEvent::MapValueToStack),
336            EVENT_MAP_VALUE_TO_STACK_N => Some(SystemEvent::MapValueToStackN),
337            EVENT_U64_DIV => Some(SystemEvent::U64Div),
338            EVENT_FALCON_DIV => Some(SystemEvent::FalconDiv),
339            EVENT_EXT2_INV => Some(SystemEvent::Ext2Inv),
340            EVENT_EXT2_INTT => Some(SystemEvent::Ext2Intt),
341            EVENT_SMT_PEEK => Some(SystemEvent::SmtPeek),
342            EVENT_U32_CLZ => Some(SystemEvent::U32Clz),
343            EVENT_U32_CTZ => Some(SystemEvent::U32Ctz),
344            EVENT_U32_CLO => Some(SystemEvent::U32Clo),
345            EVENT_U32_CTO => Some(SystemEvent::U32Cto),
346            EVENT_ILOG2 => Some(SystemEvent::ILog2),
347            EVENT_MEM_TO_MAP => Some(SystemEvent::MemToMap),
348            EVENT_HDWORD_TO_MAP => Some(SystemEvent::HdwordToMap),
349            EVENT_HDWORD_TO_MAP_WITH_DOMAIN => Some(SystemEvent::HdwordToMapWithDomain),
350            EVENT_HPERM_TO_MAP => Some(SystemEvent::HpermToMap),
351            _ => None,
352        }
353    }
354}
355
356impl crate::prettier::PrettyPrint for SystemEvent {
357    fn render(&self) -> crate::prettier::Document {
358        crate::prettier::display(self)
359    }
360}
361
362impl fmt::Display for SystemEvent {
363    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
364        match self {
365            Self::MerkleNodeMerge => write!(f, "merkle_node_merge"),
366            Self::MerkleNodeToStack => write!(f, "merkle_node_to_stack"),
367            Self::MapValueToStack => write!(f, "map_value_to_stack"),
368            Self::MapValueToStackN => write!(f, "map_value_to_stack_with_len"),
369            Self::U64Div => write!(f, "div_u64"),
370            Self::FalconDiv => write!(f, "falcon_div"),
371            Self::Ext2Inv => write!(f, "ext2_inv"),
372            Self::Ext2Intt => write!(f, "ext2_intt"),
373            Self::SmtPeek => write!(f, "smt_peek"),
374            Self::U32Clz => write!(f, "u32clz"),
375            Self::U32Ctz => write!(f, "u32ctz"),
376            Self::U32Clo => write!(f, "u32clo"),
377            Self::U32Cto => write!(f, "u32cto"),
378            Self::ILog2 => write!(f, "ilog2"),
379            Self::MemToMap => write!(f, "mem_to_map"),
380            Self::HdwordToMap => write!(f, "hdword_to_map"),
381            Self::HdwordToMapWithDomain => write!(f, "hdword_to_map_with_domain"),
382            Self::HpermToMap => write!(f, "hperm_to_map"),
383        }
384    }
385}