miden_core/sys_events.rs
1use core::fmt;
2
3use crate::{EventId, EventName};
4
5// SYSTEM EVENTS
6// ================================================================================================
7
8/// Defines a set of actions which can be initiated from the VM to inject new data into the advice
9/// provider.
10///
11/// These actions can affect all 3 components of the advice provider: Merkle store, advice stack,
12/// and advice map.
13///
14/// All actions, except for `MerkleNodeMerge`, `Ext2Inv` and `UpdateMerkleNode` can be invoked
15/// directly from Miden assembly via dedicated instructions.
16///
17/// System event IDs are derived from blake3-hashing their names (prefixed with "sys::").
18///
19/// The enum variant order matches the indices in SYSTEM_EVENT_LOOKUP, allowing efficient const
20/// lookup via `to_event_id()`. The discriminants are implicitly 0, 1, 2, ... 15.
21#[derive(Copy, Clone, Debug, Eq, PartialEq)]
22#[repr(u8)]
23pub enum SystemEvent {
24 // MERKLE STORE EVENTS
25 // --------------------------------------------------------------------------------------------
26 /// Creates a new Merkle tree in the advice provider by combining Merkle trees with the
27 /// specified roots. The root of the new tree is defined as `Hash(LEFT_ROOT, RIGHT_ROOT)`.
28 ///
29 /// Inputs:
30 /// Operand stack: [RIGHT_ROOT, LEFT_ROOT, ...]
31 /// Merkle store: {RIGHT_ROOT, LEFT_ROOT}
32 ///
33 /// Outputs:
34 /// Operand stack: [RIGHT_ROOT, LEFT_ROOT, ...]
35 /// Merkle store: {RIGHT_ROOT, LEFT_ROOT, hash(LEFT_ROOT, RIGHT_ROOT)}
36 ///
37 /// After the operation, both the original trees and the new tree remains in the advice
38 /// provider (i.e., the input trees are not removed).
39 MerkleNodeMerge,
40
41 // ADVICE STACK SYSTEM EVENTS
42 // --------------------------------------------------------------------------------------------
43 /// Pushes a node of the Merkle tree specified by the values on the top of the operand stack
44 /// onto the advice stack.
45 ///
46 /// Inputs:
47 /// Operand stack: [depth, index, TREE_ROOT, ...]
48 /// Advice stack: [...]
49 /// Merkle store: {TREE_ROOT<-NODE}
50 ///
51 /// Outputs:
52 /// Operand stack: [depth, index, TREE_ROOT, ...]
53 /// Advice stack: [NODE, ...]
54 /// Merkle store: {TREE_ROOT<-NODE}
55 MerkleNodeToStack,
56
57 /// Pushes a list of field elements onto the advice stack. The list is looked up in the advice
58 /// map using the specified word from the operand stack as the key.
59 ///
60 /// Inputs:
61 /// Operand stack: [KEY, ...]
62 /// Advice stack: [...]
63 /// Advice map: {KEY: values}
64 ///
65 /// Outputs:
66 /// Operand stack: [KEY, ...]
67 /// Advice stack: [values, ...]
68 /// Advice map: {KEY: values}
69 MapValueToStack,
70
71 /// Pushes the number of elements in a list of field elements onto the advice stack. The list is
72 /// looked up in the advice map using the specified word from the operand stack as the key.
73 ///
74 /// Inputs:
75 /// Operand stack: [KEY, ...]
76 /// Advice stack: [...]
77 /// Advice map: {KEY: values}
78 ///
79 /// Outputs:
80 /// Operand stack: [KEY, ...]
81 /// Advice stack: [values.len(), ...]
82 /// Advice map: {KEY: values}
83 MapValueCountToStack,
84
85 /// Pushes a list of field elements onto the advice stack, along with the number of elements in
86 /// that list. The list is looked up in the advice map using the word at the top of the operand
87 /// stack as the key.
88 ///
89 /// Notice that the resulting elements list is not padded.
90 ///
91 /// Inputs:
92 /// Operand stack: [KEY, ...]
93 /// Advice stack: [...]
94 /// Advice map: {KEY: values}
95 ///
96 /// Outputs:
97 /// Operand stack: [KEY, ...]
98 /// Advice stack: [num_values, values, ...]
99 /// Advice map: {KEY: values}
100 MapValueToStackN0,
101
102 /// Pushes a padded list of field elements onto the advice stack, along with the number of
103 /// elements in that list. The list is looked up in the advice map using the word at the top of
104 /// the operand stack as the key.
105 ///
106 /// Notice that the elements list obtained from the advice map will be padded with zeros,
107 /// increasing its length to the next multiple of 4.
108 ///
109 /// Inputs:
110 /// Operand stack: [KEY, ...]
111 /// Advice stack: [...]
112 /// Advice map: {KEY: values}
113 ///
114 /// Outputs:
115 /// Operand stack: [KEY, ...]
116 /// Advice stack: [num_values, values, padding, ...]
117 /// Advice map: {KEY: values}
118 MapValueToStackN4,
119
120 /// Pushes a padded list of field elements onto the advice stack, along with the number of
121 /// elements in that list. The list is looked up in the advice map using the word at the top of
122 /// the operand stack as the key.
123 ///
124 /// Notice that the elements list obtained from the advice map will be padded with zeros,
125 /// increasing its length to the next multiple of 8.
126 ///
127 /// Inputs:
128 /// Operand stack: [KEY, ...]
129 /// Advice stack: [...]
130 /// Advice map: {KEY: values}
131 ///
132 /// Outputs:
133 /// Operand stack: [KEY, ...]
134 /// Advice stack: [num_values, values, padding, ...]
135 /// Advice map: {KEY: values}
136 MapValueToStackN8,
137
138 /// Pushes a flag onto the advice stack whether advice map has an entry with specified key.
139 ///
140 /// If the advice map has the entry with the key equal to the key placed at the top of the
141 /// operand stack, `1` will be pushed to the advice stack and `0` otherwise.
142 ///
143 /// Inputs:
144 /// Operand stack: [KEY, ...]
145 /// Advice stack: [...]
146 ///
147 /// Outputs:
148 /// Operand stack: [KEY, ...]
149 /// Advice stack: [has_mapkey, ...]
150 HasMapKey,
151
152 /// Given an element in a quadratic extension field on the top of the stack (i.e., a0, b1),
153 /// computes its multiplicative inverse and push the result onto the advice stack.
154 ///
155 /// Inputs:
156 /// Operand stack: [a1, a0, ...]
157 /// Advice stack: [...]
158 ///
159 /// Outputs:
160 /// Operand stack: [a1, a0, ...]
161 /// Advice stack: [b0, b1...]
162 ///
163 /// Where (b0, b1) is the multiplicative inverse of the extension field element (a0, a1) at the
164 /// top of the stack.
165 Ext2Inv,
166
167 /// Pushes the number of the leading zeros of the top stack element onto the advice stack.
168 ///
169 /// Inputs:
170 /// Operand stack: [n, ...]
171 /// Advice stack: [...]
172 ///
173 /// Outputs:
174 /// Operand stack: [n, ...]
175 /// Advice stack: [leading_zeros, ...]
176 U32Clz,
177
178 /// Pushes the number of the trailing zeros of the top stack element onto the advice stack.
179 ///
180 /// Inputs:
181 /// Operand stack: [n, ...]
182 /// Advice stack: [...]
183 ///
184 /// Outputs:
185 /// Operand stack: [n, ...]
186 /// Advice stack: [trailing_zeros, ...]
187 U32Ctz,
188
189 /// Pushes the number of the leading ones of the top stack element onto the advice stack.
190 ///
191 /// Inputs:
192 /// Operand stack: [n, ...]
193 /// Advice stack: [...]
194 ///
195 /// Outputs:
196 /// Operand stack: [n, ...]
197 /// Advice stack: [leading_ones, ...]
198 U32Clo,
199
200 /// Pushes the number of the trailing ones of the top stack element onto the advice stack.
201 ///
202 /// Inputs:
203 /// Operand stack: [n, ...]
204 /// Advice stack: [...]
205 ///
206 /// Outputs:
207 /// Operand stack: [n, ...]
208 /// Advice stack: [trailing_ones, ...]
209 U32Cto,
210
211 /// Pushes the base 2 logarithm of the top stack element, rounded down.
212 /// Inputs:
213 /// Operand stack: [n, ...]
214 /// Advice stack: [...]
215 ///
216 /// Outputs:
217 /// Operand stack: [n, ...]
218 /// Advice stack: [ilog2(n), ...]
219 ILog2,
220
221 // ADVICE MAP SYSTEM EVENTS
222 // --------------------------------------------------------------------------------------------
223 /// Reads words from memory at the specified range and inserts them into the advice map under
224 /// the key `KEY` located at the top of the stack.
225 ///
226 /// Inputs:
227 /// Operand stack: [KEY, start_addr, end_addr, ...]
228 /// Advice map: {...}
229 ///
230 /// Outputs:
231 /// Operand stack: [KEY, start_addr, end_addr, ...]
232 /// Advice map: {KEY: values}
233 ///
234 /// Where `values` are the elements located in memory[start_addr..end_addr].
235 MemToMap,
236
237 /// Reads two word from the operand stack and inserts them into the advice map under the key
238 /// defined by the hash of these words.
239 ///
240 /// Inputs:
241 /// Operand stack: [B, A, ...]
242 /// Advice map: {...}
243 ///
244 /// Outputs:
245 /// Operand stack: [B, A, ...]
246 /// Advice map: {KEY: [a0, a1, a2, a3, b0, b1, b2, b3]}
247 ///
248 /// Where KEY is computed as hash(A || B, domain=0)
249 HdwordToMap,
250
251 /// Reads two words from the operand stack and inserts them into the advice map under the key
252 /// defined by the hash of these words (using `d` as the domain).
253 ///
254 /// Inputs:
255 /// Operand stack: [B, A, d, ...]
256 /// Advice map: {...}
257 ///
258 /// Outputs:
259 /// Operand stack: [B, A, d, ...]
260 /// Advice map: {KEY: [a0, a1, a2, a3, b0, b1, b2, b3]}
261 ///
262 /// Where KEY is computed as hash(A || B, d).
263 HdwordToMapWithDomain,
264
265 /// Reads four words from the operand stack and inserts them into the advice map under the key
266 /// defined by the hash of these words.
267 ///
268 /// Inputs:
269 /// Operand stack: [D, C, B, A, ...]
270 /// Advice map: {...}
271 ///
272 /// Outputs:
273 /// Operand stack: [D, C, B, A, ...]
274 /// Advice map: {KEY: [A', B', C', D'])}
275 ///
276 /// Where:
277 /// - KEY is the hash computed as hash(hash(hash(A || B) || C) || D) with domain=0.
278 /// - A' (and other words with `'`) is the A word with the reversed element order: A = [a3, a2,
279 /// a1, a0], A' = [a0, a1, a2, a3].
280 HqwordToMap,
281
282 /// Reads three words from the operand stack and inserts the top two words into the advice map
283 /// under the key defined by applying an RPO permutation to all three words.
284 ///
285 /// Inputs:
286 /// Operand stack: [B, A, C, ...]
287 /// Advice map: {...}
288 ///
289 /// Outputs:
290 /// Operand stack: [B, A, C, ...]
291 /// Advice map: {KEY: [a0, a1, a2, a3, b0, b1, b2, b3]}
292 ///
293 /// Where KEY is computed by extracting the digest elements from hperm([C, A, B]). For example,
294 /// if C is [0, d, 0, 0], KEY will be set as hash(A || B, d).
295 HpermToMap,
296}
297
298impl SystemEvent {
299 /// Attempts to convert an EventId into a SystemEvent by looking it up in the const table.
300 ///
301 /// Returns `Some(SystemEvent)` if the ID matches a known system event, `None` otherwise.
302 /// This uses a const lookup table with hardcoded EventIds, avoiding runtime hash computation.
303 pub const fn from_event_id(event_id: EventId) -> Option<Self> {
304 let lookup = Self::LOOKUP;
305 let mut i = 0;
306 while i < lookup.len() {
307 if lookup[i].id.as_u64() == event_id.as_u64() {
308 return Some(lookup[i].event);
309 }
310 i += 1;
311 }
312 None
313 }
314
315 /// Attempts to convert a name into a SystemEvent by looking it up in the const table.
316 ///
317 /// Returns `Some(SystemEvent)` if the name matches a known system event, `None` otherwise.
318 /// This uses const string comparison against the lookup table.
319 pub const fn from_name(name: &str) -> Option<Self> {
320 let lookup = Self::LOOKUP;
321 let mut i = 0;
322 while i < lookup.len() {
323 if str_eq(name, lookup[i].name) {
324 return Some(lookup[i].event);
325 }
326 i += 1;
327 }
328 None
329 }
330
331 /// Returns the human-readable name of this system event as an [`EventName`].
332 ///
333 /// System event names are prefixed with `sys::` to distinguish them from user-defined events.
334 pub const fn event_name(&self) -> EventName {
335 EventName::new(Self::LOOKUP[*self as usize].name)
336 }
337
338 /// Returns the [`EventId`] for this system event.
339 ///
340 /// The ID is looked up from the const LOOKUP table using the enum's discriminant
341 /// as the index. The discriminants are explicitly set to match the array indices.
342 pub const fn event_id(&self) -> EventId {
343 Self::LOOKUP[*self as usize].id
344 }
345
346 /// Returns an array of all system event variants.
347 pub const fn all() -> [Self; Self::COUNT] {
348 [
349 Self::MerkleNodeMerge,
350 Self::MerkleNodeToStack,
351 Self::MapValueToStack,
352 Self::MapValueCountToStack,
353 Self::MapValueToStackN0,
354 Self::MapValueToStackN4,
355 Self::MapValueToStackN8,
356 Self::HasMapKey,
357 Self::Ext2Inv,
358 Self::U32Clz,
359 Self::U32Ctz,
360 Self::U32Clo,
361 Self::U32Cto,
362 Self::ILog2,
363 Self::MemToMap,
364 Self::HdwordToMap,
365 Self::HdwordToMapWithDomain,
366 Self::HqwordToMap,
367 Self::HpermToMap,
368 ]
369 }
370}
371
372impl From<SystemEvent> for EventName {
373 fn from(system_event: SystemEvent) -> Self {
374 system_event.event_name()
375 }
376}
377
378impl crate::prettier::PrettyPrint for SystemEvent {
379 fn render(&self) -> crate::prettier::Document {
380 crate::prettier::display(self)
381 }
382}
383
384impl fmt::Display for SystemEvent {
385 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
386 const PREFIX_LEN: usize = "sys::".len();
387
388 let (_prefix, rest) = Self::LOOKUP[*self as usize].name.split_at(PREFIX_LEN);
389 write!(f, "{rest}")
390 }
391}
392
393// LOOKUP TABLE
394// ================================================================================================
395
396/// An entry in the system event lookup table, containing all metadata for a system event.
397#[derive(Copy, Clone, Debug)]
398pub(crate) struct SystemEventEntry {
399 /// The unique event ID (hash of the name)
400 pub id: EventId,
401 /// The system event variant
402 pub event: SystemEvent,
403 /// The full event name string (e.g., "sys::merkle_node_merge")
404 pub name: &'static str,
405}
406
407impl SystemEvent {
408 /// The total number of system events.
409 pub const COUNT: usize = 19;
410
411 /// Lookup table mapping system events to their metadata.
412 ///
413 /// The enum variant order matches the indices in this table, allowing efficient const
414 /// lookup via array indexing using discriminants.
415 const LOOKUP: [SystemEventEntry; Self::COUNT] = [
416 SystemEventEntry {
417 id: EventId::from_u64(7243907139105902342),
418 event: SystemEvent::MerkleNodeMerge,
419 name: "sys::merkle_node_merge",
420 },
421 SystemEventEntry {
422 id: EventId::from_u64(6873007751276594108),
423 event: SystemEvent::MerkleNodeToStack,
424 name: "sys::merkle_node_to_stack",
425 },
426 SystemEventEntry {
427 id: EventId::from_u64(17843484659000820118),
428 event: SystemEvent::MapValueToStack,
429 name: "sys::map_value_to_stack",
430 },
431 SystemEventEntry {
432 id: EventId::from_u64(3470274154276391308),
433 event: SystemEvent::MapValueCountToStack,
434 name: "sys::map_value_count_to_stack",
435 },
436 SystemEventEntry {
437 id: EventId::from_u64(11775886982554463322),
438 event: SystemEvent::MapValueToStackN0,
439 name: "sys::map_value_to_stack_n_0",
440 },
441 SystemEventEntry {
442 id: EventId::from_u64(3443305460233942990),
443 event: SystemEvent::MapValueToStackN4,
444 name: "sys::map_value_to_stack_n_4",
445 },
446 SystemEventEntry {
447 id: EventId::from_u64(1741586542981559489),
448 event: SystemEvent::MapValueToStackN8,
449 name: "sys::map_value_to_stack_n_8",
450 },
451 SystemEventEntry {
452 id: EventId::from_u64(5642583036089175977),
453 event: SystemEvent::HasMapKey,
454 name: "sys::has_map_key",
455 },
456 SystemEventEntry {
457 id: EventId::from_u64(9660728691489438960),
458 event: SystemEvent::Ext2Inv,
459 name: "sys::ext2_inv",
460 },
461 SystemEventEntry {
462 id: EventId::from_u64(1503707361178382932),
463 event: SystemEvent::U32Clz,
464 name: "sys::u32_clz",
465 },
466 SystemEventEntry {
467 id: EventId::from_u64(10656887096526143429),
468 event: SystemEvent::U32Ctz,
469 name: "sys::u32_ctz",
470 },
471 SystemEventEntry {
472 id: EventId::from_u64(12846584985739176048),
473 event: SystemEvent::U32Clo,
474 name: "sys::u32_clo",
475 },
476 SystemEventEntry {
477 id: EventId::from_u64(6773574803673468616),
478 event: SystemEvent::U32Cto,
479 name: "sys::u32_cto",
480 },
481 SystemEventEntry {
482 id: EventId::from_u64(7444351342957461231),
483 event: SystemEvent::ILog2,
484 name: "sys::ilog2",
485 },
486 SystemEventEntry {
487 id: EventId::from_u64(5768534446586058686),
488 event: SystemEvent::MemToMap,
489 name: "sys::mem_to_map",
490 },
491 SystemEventEntry {
492 id: EventId::from_u64(5988159172915333521),
493 event: SystemEvent::HdwordToMap,
494 name: "sys::hdword_to_map",
495 },
496 SystemEventEntry {
497 id: EventId::from_u64(6143777601072385586),
498 event: SystemEvent::HdwordToMapWithDomain,
499 name: "sys::hdword_to_map_with_domain",
500 },
501 SystemEventEntry {
502 id: EventId::from_u64(11723176702659679401),
503 event: SystemEvent::HqwordToMap,
504 name: "sys::hqword_to_map",
505 },
506 SystemEventEntry {
507 id: EventId::from_u64(6190830263511605775),
508 event: SystemEvent::HpermToMap,
509 name: "sys::hperm_to_map",
510 },
511 ];
512}
513
514// HELPERS
515// ================================================================================================
516
517/// Const-compatible string equality check.
518const fn str_eq(a: &str, b: &str) -> bool {
519 let a_bytes = a.as_bytes();
520 let b_bytes = b.as_bytes();
521
522 if a_bytes.len() != b_bytes.len() {
523 return false;
524 }
525
526 let mut i = 0;
527 while i < a_bytes.len() {
528 if a_bytes[i] != b_bytes[i] {
529 return false;
530 }
531 i += 1;
532 }
533 true
534}
535
536#[cfg(test)]
537mod test {
538 use super::*;
539
540 #[test]
541 fn test_system_events() {
542 // Comprehensive test verifying consistency between SystemEvent::all() and
543 // SystemEvent::LOOKUP. This ensures all() and LOOKUP are in sync, lookup table has
544 // correct IDs/names, and all variants are covered.
545
546 // Verify lengths match COUNT
547 assert_eq!(SystemEvent::all().len(), SystemEvent::COUNT);
548 assert_eq!(SystemEvent::LOOKUP.len(), SystemEvent::COUNT);
549
550 // Iterate through both all() and LOOKUP together, checking all invariants
551 for (i, (event, entry)) in
552 SystemEvent::all().iter().zip(SystemEvent::LOOKUP.iter()).enumerate()
553 {
554 // Verify LOOKUP entry matches the event at the same index
555 assert_eq!(
556 entry.event, *event,
557 "LOOKUP[{}].event ({:?}) doesn't match all()[{}] ({:?})",
558 i, entry.event, i, event
559 );
560
561 // Verify LOOKUP entry ID matches the computed ID
562 let computed_id = event.event_id();
563 assert_eq!(
564 entry.id,
565 computed_id,
566 "LOOKUP[{}].id is EventId::from_u64({}), but {:?}.to_event_id() returns EventId::from_u64({})",
567 i,
568 entry.id.as_u64(),
569 event,
570 computed_id.as_u64()
571 );
572
573 // Verify name has correct "sys::" prefix
574 assert!(
575 entry.name.starts_with("sys::"),
576 "SystemEvent name should start with 'sys::': {}",
577 entry.name
578 );
579
580 // Verify from_event_id lookup works
581 let looked_up =
582 SystemEvent::from_event_id(entry.id).expect("SystemEvent should be found by ID");
583 assert_eq!(looked_up, *event);
584
585 // Verify from_name lookup works
586 let looked_up_by_name =
587 SystemEvent::from_name(entry.name).expect("SystemEvent should be found by name");
588 assert_eq!(looked_up_by_name, *event);
589
590 // Verify EventName conversion works
591 let event_name = event.event_name();
592 assert_eq!(event_name.as_str(), entry.name);
593 assert!(SystemEvent::from_name(event_name.as_str()).is_some());
594 let event_name_from_into: EventName = (*event).into();
595 assert_eq!(event_name_from_into.as_str(), entry.name);
596 assert!(SystemEvent::from_name(event_name_from_into.as_str()).is_some());
597
598 // Exhaustive match to ensure compile-time error when adding new variants
599 match event {
600 SystemEvent::MerkleNodeMerge
601 | SystemEvent::MerkleNodeToStack
602 | SystemEvent::MapValueToStack
603 | SystemEvent::MapValueCountToStack
604 | SystemEvent::MapValueToStackN0
605 | SystemEvent::MapValueToStackN4
606 | SystemEvent::MapValueToStackN8
607 | SystemEvent::HasMapKey
608 | SystemEvent::Ext2Inv
609 | SystemEvent::U32Clz
610 | SystemEvent::U32Ctz
611 | SystemEvent::U32Clo
612 | SystemEvent::U32Cto
613 | SystemEvent::ILog2
614 | SystemEvent::MemToMap
615 | SystemEvent::HdwordToMap
616 | SystemEvent::HdwordToMapWithDomain
617 | SystemEvent::HqwordToMap
618 | SystemEvent::HpermToMap => {},
619 }
620 }
621 }
622}