Skip to content

instruction_reference.md

Latest commit

 

History

History
399 lines (322 loc) · 44.1 KB

instruction_reference.md

File metadata and controls

399 lines (322 loc) · 44.1 KB
Raw
title Miden VM Instruction Reference
sidebar_position 12

Miden VM Instruction Reference

This page provides a comprehensive reference for Miden Assembly instructions.

Field Operations

Comparison Operations

Instruction Stack Input Stack Output Cycles Notes
lte
lte.b 		[b, a, ...] [c, ...] 18
19		 $$c = \begin{cases} 1, & \text{if } a \leq b 0, & \text{otherwise} \end{cases}$$
lt
lt.b 		[b, a, ...] [c, ...] 17
18		 $$c = \begin{cases} 1, & \text{if } a < b 0, & \text{otherwise} \end{cases}$$
gte
gte.b 		[b, a, ...] [c, ...] 17
18		 $$c = \begin{cases} 1, & \text{if } a \geq b 0, & \text{otherwise} \end{cases}$$
gt
gt.b 		[b, a, ...] [c, ...] 16
17		 $$c = \begin{cases} 1, & \text{if } a > b 0, & \text{otherwise} \end{cases}$$
eq
eq.b 		[b, a, ...] [c, ...] 1
1-2		 $$c = \begin{cases} 1, & \text{if } a = b 0, & \text{otherwise} \end{cases}$$
neq
neq.b 		[b, a, ...] [c, ...] 2
2-3		 $$c = \begin{cases} 1, & \text{if } a \neq b 0, & \text{otherwise} \end{cases}$$
eqw [A, B, ...] [c, A, B, ...] 15 $$c = \begin{cases} 1, & \text{if } a_i = b_i\ \forall i \in {0,1,2,3} 0, & \text{otherwise} \end{cases}$$
is_odd [a, ...] [b, ...] 6 $$b = \begin{cases} 1, & \text{if $a$ is odd} 0, & \text{otherwise} \end{cases}$$

Assertions and Tests

Instruction Stack Input Stack Output Cycles Notes
assert [a, ...] [...] 1 Removes $a$ if $a = 1$. Fails if $a \neq 1$.
assertz [a, ...] [...] 2 Removes $a$ if $a = 0$. Fails if $a \neq 0$.
assert_eq [b, a, ...] [...] 2 Removes $a, b$ if $a = b$. Fails if $a \neq b$.
assert_eqw [B, A, ...] [...] 11 Removes $A, B$ if $A = B$. Fails if $A \neq B$.

Note: Assertions can be parameterized with an error message (e.g., assert.err="Division by 0").

Arithmetic and Boolean Operations

Instruction Stack Input Stack Output Cycles Notes
add
add.b 		[b, a, ...] [c, ...] 1
1-2		 $c = (a + b) \bmod p$
sub
sub.b 		[b, a, ...] [c, ...] 2
2		 $c = (a - b) \bmod p$
mul
mul.b 		[b, a, ...] [c, ...] 1
2		 $c = (a \cdot b) \bmod p$
div
div.b 		[b, a, ...] [c, ...] 2
2		 $c = (a \cdot b^{-1}) \bmod p$. Fails if $b = 0$. Field division — not integer floor division. Use u32div for floor division.
neg [a, ...] [b, ...] 1 $b = -a \bmod p$
inv [a, ...] [b, ...] 1 $b = a^{-1} \bmod p$. Fails if $a = 0$.
pow2 [a, ...] [b, ...] 16 $b = 2^a$. Fails if $a &gt; 63$.
exp.uxx
exp.b 		[b, a, ...] [c, ...] 9+xx
9+log2(b)		 $c = a^b$. Fails if $xx$ is outside $[0, 63)$. exp is exp.u64 (73 cycles).
ilog2 [a, ...] [b, ...] 66 $b = \lfloor \log_2(a) \rfloor$. Fails if $a = 0$.
not [a, ...] [b, ...] 1 $b = 1 - a$. Fails if $a &gt; 1$.
and [b, a, ...] [c, ...] 1 $c = a \cdot b$. Fails if $\max(a, b) &gt; 1$.
or [b, a, ...] [c, ...] 1 $c = a + b - a \cdot b$. Fails if $\max(a, b) &gt; 1$.
xor [b, a, ...] [c, ...] 7 $c = a + b - 2 \cdot a \cdot b$. Fails if $\max(a, b) &gt; 1$.

Extension Field Operations

All operations in this section are defined over the quadratic extension field $\mathbb{F}_p[x] / (x^2 - 7)$, with modulus $p = 2^{64} - 2^{32} + 1$.

Instruction Stack Input Stack Output Cycles Notes
ext2add [b0, b1, a0, a1, ...] [c0, c1, ...] 5 $c0 = (a0 + b0) \bmod p$
$c1 = (a1 + b1) \bmod p$
ext2sub [b0, b1, a0, a1, ...] [c0, c1, ...] 7 $c0 = (a0 - b0) \bmod p$
$c1 = (a1 - b1) \bmod p$
ext2mul [b0, b1, a0, a1, ...] [c0, c1, ...] 3 $c0 = a0b0 + 7a1b1 \bmod p$
$c1 = a0b1 + a1b0 \bmod p$
ext2neg [a0, a1, ...] [a0', a1', ...] 4 $a0' = -a0$
$a1' = -a1$
ext2inv [a0, a1, ...] [a0', a1', ...] 8 $a' = a^{-1}$ in $\mathbb{F}_p[x]/(x^2 - 7)$. Fails if $a = 0$.
ext2div [b0, b1, a0, a1, ...] [c0, c1, ...] 11 $c = a \cdot b^{-1}$ in $\mathbb{F}_p[x]/(x^2 - 7)$. Fails if $b = 0$.

U32 Operations

Operations on 32-bit integers. Most instructions will fail or have undefined behavior if inputs are not valid u32 values.

Conversions and Tests

Instruction Stack Input Stack Output Cycles Notes
u32test [a, ...] [b, a, ...] 5 $$b = \begin{cases} 1, & \text{if } a < 2^{32} 0, & \text{otherwise} \end{cases}$$
u32testw [A, ...] [b, A, ...] 23 $$b = \begin{cases} 1, & \text{if } \forall i \in {0,1,2,3}, a_i < 2^{32} 0, & \text{otherwise} \end{cases}$$
u32assert [a, ...] [a, ...] 3 Fails if $a \geq 2^{32}$.
u32assert2 [b, a,...] [b, a,...] 1 Fails if $a \geq 2^{32}$ or $b \geq 2^{32}$.
u32assertw [A, ...] [A, ...] 6 Fails if any element of $A$ is $\geq 2^{32}$.
u32cast [a, ...] [b, ...] 2 $b = a \bmod 2^{32}$
u32split [a, ...] [b, c, ...] 1 $b = a \bmod 2^{32}$, $c = \lfloor a / 2^{32} \rfloor$

Note: Assertions can be parameterized with an error message (e.g., assert.err="Division by 0").

Arithmetic Operations

Instruction Stack Input Stack Output Cycles Notes
u32widening_add
u32widening_add.b 		[b, a, ...] [c, d, ...] 1
2-3		 $c = (a + b) \bmod 2^{32}$, $$d = \begin{cases} 1, & \text{if } (a + b) \geq 2^{32} 0, & \text{otherwise} \end{cases}$$. The pair $[c, d]$ forms the 64-bit sum with $c$ as the low limb. Undefined if $\max(a,b) \geq 2^{32}$.
u32overflowing_add
u32overflowing_add.b 		[b, a, ...] [d, c, ...] 2
3-4		 $c = (a + b) \bmod 2^{32}$, $$d = \begin{cases} 1, & \text{if } (a + b) \geq 2^{32} 0, & \text{otherwise} \end{cases}$$. The pair $[c, d]$ forms the 64-bit sum with $c$ as the low limb. Undefined if $\max(a,b) \geq 2^{32}$.
u32wrapping_add
u32wrapping_add.b 		[b, a, ...] [c, ...] 3
4-5		 $c = (a + b) \bmod 2^{32}$. Undefined if $\max(a,b) \geq 2^{32}$.
u32widening_add3 [c, b, a, ...] [d, e, ...] 1 $d = (a+b+c) \bmod 2^{32}$, $e = \lfloor (a+b+c)/2^{32} \rfloor$. The pair $[d, e]$ forms the 64-bit sum with $d$ as the low limb. Undefined if $\max(a,b,c) \geq 2^{32}$.
u32overflowing_add3 [c, b, a, ...] [e, d, ...] 2 $d = (a+b+c) \bmod 2^{32}$, $e = \lfloor (a+b+c)/2^{32} \rfloor$. The pair $[d, e]$ forms the 64-bit sum with $d$ as the low limb. Undefined if $\max(a,b,c) \geq 2^{32}$.
u32wrapping_add3 [c, b, a, ...] [d, ...] 3 $d = (a+b+c) \bmod 2^{32}$. Undefined if $\max(a,b,c) \geq 2^{32}$.
u32overflowing_sub
u32overflowing_sub.b 		[b, a, ...] [d, c, ...] 1
2-3		 $c = (a - b) \bmod 2^{32}$, $$d = \begin{cases} 1, & \text{if } a < b 0, & \text{otherwise} \end{cases}$$. Undefined if $\max(a,b) \geq 2^{32}$.
u32wrapping_sub
u32wrapping_sub.b 		[b, a, ...] [c, ...] 2
3-4		 $c = (a - b) \bmod 2^{32}$. Undefined if $\max(a,b) \geq 2^{32}$.
u32widening_mul
u32widening_mul.b 		[b, a, ...] [c, d, ...] 1
2-3		 $c = (a \cdot b) \bmod 2^{32}$, $d = \lfloor(a \cdot b) / 2^{32}\rfloor$. Undefined if $\max(a,b) \geq 2^{32}$.
u32wrapping_mul
u32wrapping_mul.b 		[b, a, ...] [c, ...] 2
3-4		 $c = (a \cdot b) \bmod 2^{32}$. Undefined if $\max(a,b) \geq 2^{32}$.
u32widening_madd [b, a, c, ...] [d, e, ...] 1 $d = (a \cdot b+c) \bmod 2^{32}$, $e = \lfloor(a \cdot b+c) / 2^{32}\rfloor$. Undefined if $\max(a,b,c) \geq 2^{32}$.
u32wrapping_madd [b, a, c, ...] [d, ...] 3 $d = (a \cdot b+c) \bmod 2^{32}$. Undefined if $\max(a,b,c) \geq 2^{32}$.
u32div
u32div.b 		[b, a, ...] [c, ...] 2
3-4		 $c = \lfloor a/b \rfloor$. Fails if $b=0$. Undefined if $\max(a,b) \geq 2^{32}$.
u32mod
u32mod.b 		[b, a, ...] [c, ...] 3
4-5		 $c = a \bmod b$. Fails if $b=0$. Undefined if $\max(a,b) \geq 2^{32}$.
u32divmod
u32divmod.b 		[b, a, ...] [d, c, ...] 1
2-3		 $c = \lfloor a/b \rfloor$, $d = a \bmod b$. Fails if $b=0$. Undefined if $\max(a,b) \geq 2^{32}$.

Bitwise Operations

Instruction Stack Input Stack Output Cycles Notes
u32and
u32and.b 		[b, a, ...] [c, ...] 1
2		 Bitwise AND. Fails if $\max(a,b) \geq 2^{32}$.
u32or
u32or.b 		[b, a, ...] [c, ...] 6
7		 Bitwise OR. Fails if $\max(a,b) \geq 2^{32}$.
u32xor
u32xor.b 		[b, a, ...] [c, ...] 1
2		 Bitwise XOR. Fails if $\max(a,b) \geq 2^{32}$.
u32not
u32not.a 		[a, ...] [b, ...] 5
6		 Bitwise NOT. Fails if $a \geq 2^{32}$.
u32shl
u32shl.b 		[b, a, ...] [c, ...] 19
4		 $c = (a \cdot 2^b) \bmod 2^{32}$. Undefined if $a \geq 2^{32}$ or $b &gt; 31$.
u32shr
u32shr.b 		[b, a, ...] [c, ...] 20
5		 $c = \lfloor a / 2^b \rfloor$. Undefined if $a \geq 2^{32}$ or $b &gt; 31$.
u32rotl
u32rotl.b 		[b, a, ...] [c, ...] 18
3		 Rotate left. Undefined if $a \geq 2^{32}$ or $b &gt; 31$.
u32rotr
u32rotr.b 		[b, a, ...] [c, ...] 22
3		 Rotate right. Undefined if $a \geq 2^{32}$ or $b &gt; 31$.
u32popcnt [a, ...] [b, ...] 32 Population count (Hamming weight). Undefined if $a \geq 2^{32}$.
u32clz [a, ...] [b, ...] 48 Count leading zeros. Undefined if $a \geq 2^{32}$.
u32ctz [a, ...] [b, ...] 34 Count trailing zeros. Undefined if $a \geq 2^{32}$.
u32clo [a, ...] [b, ...] 40 Count leading ones. Undefined if $a \geq 2^{32}$.
u32cto [a, ...] [b, ...] 33 Count trailing ones. Undefined if $a \geq 2^{32}$.

Comparison Operations

Instruction Stack Input Stack Output Cycles Notes
u32lt
u32lt.b 		[b, a, ...] [c, ...] 3
4		 $$c = \begin{cases} 1, & \text{if } a < b 0, & \text{otherwise} \end{cases}$$. Undefined if $\max(a,b) \geq 2^{32}$.
u32lte
u32lte.b 		[b, a, ...] [c, ...] 5
6		 $$c = \begin{cases} 1, & \text{if } a \leq b 0, & \text{otherwise} \end{cases}$$. Undefined if $\max(a,b) \geq 2^{32}$.
u32gt
u32gt.b 		[b, a, ...] [c, ...] 4
5		 $$c = \begin{cases} 1, & \text{if } a > b 0, & \text{otherwise} \end{cases}$$. Undefined if $\max(a,b) \geq 2^{32}$.
u32gte
u32gte.b 		[b, a, ...] [c, ...] 4
5		 $$c = \begin{cases} 1, & \text{if } a \geq b 0, & \text{otherwise} \end{cases}$$. Undefined if $\max(a,b) \geq 2^{32}$.
u32min
u32min.b 		[b, a, ...] [c, ...] 8
9		 $c = \min(a,b)$. Undefined if $\max(a,b) \geq 2^{32}$.
u32max
u32max.b 		[b, a, ...] [c, ...] 9
10		 $c = \max(a,b)$. Undefined if $\max(a,b) \geq 2^{32}$.

Stack Manipulation

Instructions for directly manipulating the operand stack. Only the top 16 elements are directly accessible.

Instruction Stack Input Stack Output Cycles Notes
drop [a, ... ] [ ... ] 1 Deletes the top stack item.
dropw [A, ... ] [ ... ] 4 Deletes a word (4 elements) from the top of the stack.
padw [ ... ] [0,0,0,0, ... ] 4 Pushes four 0 values onto the stack.
dup.n [ ..., a, ... ] [a, ..., a, ... ] 1-3 Pushes a copy of the nth stack item (0-indexed) onto the stack. dup is dup.0. Valid for n in 0..=15.
dupw.n [ ..., A, ... ] [A, ..., A, ... ] 4 Pushes a copy of the nth stack word (0-indexed) onto the stack. dupw is dupw.0. Valid for n in 0..=3.
swap.n [a, ..., b, ... ] [b, ..., a, ... ] 1-6 Swaps the top stack item with the nth stack item (1-indexed). swap is swap.1. Valid for n in 1..=15.
swapw.n [A, ..., B, ... ] [B, ..., A, ... ] 1 Swaps the top stack word with the nth stack word (1-indexed). swapw is swapw.1. Valid for n in 1..=3.
swapdw [D,C,B,A, ... ] [B,A,D,C ... ] 1 Swaps words: 1st with 3rd, 2nd with 4th.
movup.n [ ..., a, ... ] [a, ... ] 1-4 Moves the nth stack item (2-indexed) to the top. Valid for n in 2..=15.
movupw.n [ ..., A, ... ] [A, ... ] 2-3 Moves the nth stack word (2-indexed) to the top. Valid for n in 2..=3.
movdn.n [a, ... ] [ ..., a, ... ] 1-4 Moves the top stack item to the nth position (2-indexed). Valid for n in 2..=15.
movdnw.n [A, ... ] [ ..., A, ... ] 2-3 Moves the top stack word to the nth word position (2-indexed). Valid for n in 2..=3.

Conditional Manipulation

Instruction Stack Input Stack Output Cycles Notes
cswap [c, b, a, ... ] [e, d, ... ] 1 If c = 1, d=b, e=a. If c = 0, d=a, e=b. Fails if c > 1.
cswapw [c, B, A, ... ] [E, D, ... ] 1 If c = 1, D=B, E=A. If c = 0, D=A, E=B. Fails if c > 1.
cdrop [c, b, a, ... ] [d, ... ] 2 If c = 1, d=b. If c = 0, d=a. Fails if c > 1.
cdropw [c, B, A, ... ] [D, ... ] 5 If c = 1, D=B. If c = 0, D=A. Fails if c > 1.

Input/Output Operations

Instructions for moving data between the stack and other sources like program code, environment, advice provider, and memory.

Constant Inputs

Instruction Stack Input Stack Output Cycles Notes
push.a... [ ... ] [c, b, a, ...] 1-2 Pushes up to 16 field elements (decimal or hex) onto the stack. Hex words (32 bytes) are little-endian; short hex values are big-endian. Example: push.0x1234.0x5678 or push.0x34120000...78560000...
push.[a,b,c,d] [ ... ] [a, b, c, d, ...] 4 Pushes a word (4 field elements) onto the stack. Element a ends up on top. Example: push.[1,2,3,4] results in [1, 2, 3, 4, ...].

Environment Inputs

Instruction Stack Input Stack Output Cycles Notes
clk [ ... ] [t, ... ] 1 Pushes current clock cycle t.
sdepth [ ... ] [d, ... ] 1 Pushes current stack depth d.
caller [A, ...] [H, ...] 1 In context 0, overwrites the top 4 stack items with hash H of the function that syscall'd into the current context, or [0, 0, 0, 0] when not servicing a SYSCALL. In any other context, H corresponds to the hash of the function that entered the current context.
locaddr.i [ ... ] [a, ... ] 2 Pushes absolute memory address a of local memory at index i.
procref.name [ ... ] [A, ... ] 4 Pushes MAST root A of procedure name.

Nondeterministic Inputs (Advice Provider)

Reading from Advice Stack

Instruction Stack Input Stack Output Cycles Notes
adv_push [ ... ] [a, ...] 1 Pops 1 value from advice stack and pushes onto operand stack. Fails if advice stack is empty.
adv_pushw [ ... ] [A, ...] 5 Equivalent to padw adv_loadw. Pushes a word from advice onto the stack (grows by 4). Fails if advice stack has < 4 values.
adv_loadw [0,0,0,0, ...] [A, ...] 1 Pops word A (4 elements) from advice stack, overwrites top word of operand stack. Fails if advice stack has < 4 values.
adv_pipe [A,B,C,a,...] [A',B',C,a+8,...] 1 Pops 2 words from advice stack, overwrites top 2 words (positions 0-7). C (positions 8-11) unchanged. Writes both words to memory at a and a+4. a' = a+8. Fails if advice stack has < 8 values.

Advice Provider and Deferred-State System Events (3 cycles)

Push to Advice Stack:

Instruction Stack Input Stack Output Notes
adv.push_mapval [K, ... ] [K, ... ] Pushes values from advice_map[K] to advice stack.
adv.push_mapval_count [K, ... ] [K, ... ] Pushes number of elements in advice_map[K] to advice stack.
adv.push_mapvaln [K, ... ] [K, ... ] Pushes [n, ele1, ele2, ...] from advice_map[K] to advice stack, where n is element count.
adv.push_mtnode [d, i, R, ... ] [d, i, R, ... ] Pushes Merkle tree node (root R, depth d, index i) from Merkle store to advice stack.
adv.evaluate_deferred [NODE_DIGEST, ...] [NODE_DIGEST, ...] Evaluates a registered deferred node and pushes its canonical tag and payload felts to the advice stack. See deferred DAG details below.
adv.evaluate_deferred_tag [NODE_DIGEST, ...] [NODE_DIGEST, ...] Evaluates a registered deferred node and pushes only its canonical tag to the advice stack.
adv.evaluate_deferred_payload [NODE_DIGEST, ...] [NODE_DIGEST, ...] Evaluates a registered deferred node and pushes only its canonical payload felts to the advice stack.

Deferred DAG (host-side registration; no advice output):

Instruction Stack Input Stack Output Notes
adv.register_deferred [PAYLOAD_LO, PAYLOAD_HI, TAG, ...] [PAYLOAD_LO, PAYLOAD_HI, TAG, ...] Registers and eagerly evaluates an operand-stack deferred node. Produces no advice output. See deferred DAG details below.
adv.register_deferred_data [TAG, ptr, n_chunks, ...] [TAG, ptr, n_chunks, ...] Registers and eagerly evaluates a memory-backed deferred node. Produces no advice output. See deferred DAG details below.

Deferred DAG details:

  • TAG and every digest are one word (4 field elements). One deferred data chunk is 8 field elements, i.e. two words.

  • adv.register_deferred accepts exactly one stack-resident payload block: PAYLOAD_LO || PAYLOAD_HI (8 field elements).

    • Data tags interpret those eight felts as a one-chunk data payload.
    • Join tags interpret them as lhs_digest || rhs_digest.
    • Pair-list tags interpret them as one lhs_digest || rhs_digest pair.

    TRUE is not accepted by this instruction. Tags that semantically require more data chunks or pairs fail during precompile evaluation. Code that later uses the node digest must compute it inside the VM from the same PAYLOAD_LO, PAYLOAD_HI, and TAG values, for example with hperm.

  • adv.register_deferred_data accepts data, pair-list, and join tags. Its stack-supplied TAG, ptr, and n_chunks are visible in the VM execution trace, but the event does not AIR-bind the host-read contents to memory.

    • Data tags read exactly n_chunks 8-felt chunks from word-aligned ptr.
    • Pair-list tags interpret those chunks as lhs_digest || rhs_digest pairs.
    • Join tags require n_chunks == 1 and interpret the chunk as lhs_digest || rhs_digest.

    TRUE is not accepted. Code that later relies on the node must compute its digest with VM instructions from the same TAG and ordered chunk sequence. The register_mem wrapper does this by hashing the exact range [ptr, ptr + 8 * n_chunks) with one absorption per chunk.

  • adv.evaluate_deferred requires NODE_DIGEST to be already registered. It pushes the canonical tag followed by the canonical payload in advice-pop order. For a single 8-felt payload, adv_pushw adv_pushw adv_pushw leaves [PAYLOAD_LO, PAYLOAD_HI, TAG, ...] on the operand stack. TRUE emits only Tag::TRUE.

  • adv.evaluate_deferred_tag pushes only the canonical tag. TRUE emits Tag::TRUE.

  • adv.evaluate_deferred_payload is the payload-only compatibility event. It pushes only the canonical payload to the advice stack.

    • Data payloads are arranged per 8-felt chunk as HIGH then LOW in advice-pop order, so adv_pushw adv_pushw leaves LOW above HIGH on the operand stack. Chunks preserve canonical chunk order.
    • Join payloads use the same two-word LIFO convention, leaving lhs_digest above rhs_digest after two adv_pushws.
    • TRUE emits no advice.

  • All adv.evaluate_deferred* outputs, including tag-only output, are host-provided hints. Before proof-relevant use, code must relate them with VM instructions to values established independently of that advice.

Insert into Advice Map:

Instruction Stack Input Stack Output Notes
adv.insert_mem [K, a, b, ... ] [K, a, b, ... ] advice_map[K] ← mem[a..b].
adv.insert_hdword [A, B, ... ] [A, B, ... ] K ← hash(A || B) (top first). advice_map[K] ← [A,B]. MASM: hmerge.
adv.insert_hdword_d [A, B, d, ... ] [A, B, d, ... ] K ← hash(A || B, domain=d) (top first). advice_map[K] ← [A,B].
adv.insert_hqword [A, B, C, D, ... ] [A, B, C, D, ... ] K ← hash_elements([A,B,C,D]). advice_map[K] ← [A,B,C,D].
adv.insert_hperm [R0, R1, C, ...] [R0, R1, C, ...] K ← permute(R0,R1,C).digest. advice_map[K] ← [R0,R1].

Random Access Memory

Memory is 0-initialized. Addresses are absolute [0, 2^32). Locals are stored at offset 2^30.

Absolute Addressing

Instruction Stack Input Stack Output Cycles Notes
mem_load
mem_load.a		 [a, ... ] [v, ... ] 1
2		 v ← mem[a]. Pushes element from mem[a]. If a on stack, it's popped. Fails if a >= 2^32.
mem_loadw_be
mem_loadw_be.a		 [a, 0,0,0,0,...] [A, ... ] 4
5		 A ← mem[a..a+3] (word, big-endian). Overwrites top 4 stack elements (mem[a+3] is top). Equivalent to mem_loadw_le reversew. If a on stack, it's popped. Fails if a >= 2^32 or a not multiple of 4.
mem_loadw_le
mem_loadw_le.a		 [a, 0,0,0,0,...] [A, ... ] 1
2		 A ← mem[a..a+3] (word, little-endian). Overwrites top 4 stack elements (mem[a] is top). If a on stack, it's popped. Fails if a >= 2^32 or a not multiple of 4.
mem_store
mem_store.a		 [a, v, ... ] [ ... ] 2
3-4		 mem[a] ← v. Pops v to mem[a]. If a on stack, it's popped. Fails if a >= 2^32.
mem_storew_be
mem_storew_be.a		 [a, A, ... ] [A, ... ] 9
8-9		 mem[a..a+3] ← A. Stores word A in big-endian order (top stack element at mem[a+3]). Equivalent to reversew mem_storew_le reversew. If a on stack, it's popped. Fails if a >= 2^32 or a not multiple of 4.
mem_storew_le
mem_storew_le.a		 [a, A, ... ] [A, ... ] 1
2-3		 mem[a..a+3] ← A. Stores word A in little-endian order (top stack element at mem[a]). If a on stack, it's popped. Fails if a >= 2^32 or a not multiple of 4.
mem_stream [R0, R1, C, a, ...] [D, E, C, a', ...] 1 [D, E] ← [mem[a..a+3], mem[a+4..a+7]]. a' ← a+8. Reads 2 sequential words from memory, replacing R0 and R1 of the sponge state.

Procedure Locals (Context-Specific)

Locals are not 0-initialized. Max $2^{16}$ locals per procedure, $2^{31} - 1$ total. Rounded up to multiple of 4.

Instruction Stack Input Stack Output Cycles Notes
loc_load.i [ ... ] [v, ... ] 5-6 v ← local[i]. Pushes element from local memory at index i.
loc_loadw_be.i [0,0,0,0, ...] [A, ... ] 6-7 A ← local[i..i+3]. Reads word in big-endian order, local[i+3] is top of stack. Equivalent to loc_loadw_le reversew. Fails if i not multiple of 4.
loc_loadw_le.i [0,0,0,0, ...] [A, ... ] 3-4 A ← local[i..i+3]. Reads word in little-endian order, local[i] is top of stack. Fails if i not multiple of 4.
loc_store.i [v, ... ] [ ... ] 6-7 local[i] ← v. Pops v to local memory at index i.
loc_storew_be.i [A, ... ] [A, ... ] 9-10 local[i..i+3] ← A. Stores word in big-endian order, top stack element at local[i+3]. Equivalent to reversew loc_storew_le reversew.
loc_storew_le.i [A, ... ] [A, ... ] 3-4 local[i..i+3] ← A. Stores word in little-endian order, top stack element at local[i].

Cryptographic Operations

Common cryptographic operations, including hashing and Merkle tree manipulations using Poseidon2.

Hashing and Merkle Trees

Instruction Stack Input Stack Output Cycles Notes
hash [A, ...] [B, ...] 19 B ← hash(A). 1-to-1 Poseidon2 hash.
hperm [R0, R1, C, ...] [R0', R1', C', ...] 1 Poseidon2 permutation. R0,R1=rate (R0 on top), C=capacity, R0'=digest.
hmerge [A, B, ...] [C, ...] 16 C ← hash(A,B). 2-to-1 Poseidon2 hash.
mtree_get [d, i, R, ...] [V, R, ...] 10 Verifies Merkle path for node V at depth d, index i for tree R (from advice provider), returns V.
mtree_set [d, i, R, V', ...] [V, R', ...] 30 Updates node in tree R at d,i to V'. Returns old value V and new root R'. Both trees in advice provider.
mtree_merge [L, R, ...] [M, ...] 16 Merges Merkle trees with roots L (left) and R (right) into new tree M. Input trees retained.
mtree_verify [V, d, i, R, ...] [V,d,i,R,...] 1 Verifies Merkle path for node V at depth d, index i for tree R (from advice provider).
Can be parameterized with err code (e.g., mtree_verify.err=123). Default error code is 0.
crypto_stream [rate(8), cap(4), src_ptr, dst_ptr, ...] [ciphertext(8), cap(4), src_ptr+8, dst_ptr+8, ...] 1 Poseidon2-sponge keystream step against memory: loads two words from src_ptr, adds the rate (top 8 stack elements) element-wise to produce ciphertext, writes ciphertext to dst_ptr, replaces rate on stack with ciphertext, preserves capacity, increments both pointers by 8. Primitive used by miden::core::crypto::aead.

Flow Control Operations

High-level constructs for controlling the execution flow.

Conditional Execution: if.true ... else ... end / if.false ... else ... end

  • Syntax: 
    if.true
  # instructions for true branch
else
  # instructions for false branch
end
    Or with if.false (condition inverted). The else block is optional.
  • Stack Input: [cond, ...] (where cond is 0 or 1)
  • Cycles: Incurs a small overhead. For simple conditionals, cdrop might be more efficient if side-effects can be managed.
  • Notes:
    • Pops cond from the stack. Fails if not boolean.
    • if.true: Executes first block if cond = 1, second (else) block if cond = 0.
    • if.false: Executes first block if cond = 0, second (else) block if cond = 1.
    • Empty or elided branches are treated as a nop.
    • Ensure stack consistency at join points if modifications persist beyond a branch.

Counter-Controlled Loops: repeat.count ... end

  • Syntax: 
    repeat.COUNT
  # instructions to repeat
end
  • Cycles: No additional cost for counting; the block is unrolled COUNT times during compilation.
  • Notes:
  • COUNT must be an integer or a named constant in the range 1..=1,000,000.
    • Instructions inside can include nested control structures.

Condition-Controlled Loops: while.true ... end

  • Syntax: 
    while.true
  # instructions for loop body
end
  • Stack Input (for each iteration check): [cond, ...] (where cond is 0 or 1)
  • Cycles: Overhead per iteration for condition check.
  • Notes:
    1. Pops cond from the stack. If 0, skips loop. Fails if not boolean.
    2. If cond = 1, executes loop body.
    3. After body execution, pops a new cond. If 1, repeats body. If 0, exits loop. Fails if not boolean.

No-Operation: nop

  • Syntax: nop
  • Cycles: 1
  • Notes:
    • Increments the cycle counter with no other effects.
    • Useful for empty blocks or explicitly advancing cycles.
    • Assembler automatically inserts nop for empty/elided branches in if statements.

Events

Instructions for communicating with the host through events.

Instruction Stack Input Stack Output Cycles Notes
emit.<event_id> [...] [...] 3 Emits an event with the specified event_id to the host. The net effect on the operand stack is no change (internally expands to push.<event_id> emit drop). Immediate event_id must be defined via const.ID=event("...") or inlined as emit.event("..."). Events allow programs to communicate contextual information to the host for triggering appropriate actions. Example: emit.event("foo") or emit.MY_EVENT
emit [event_id, ...] [event_id, ...] 1 Emits an event using the event_id from the top of the stack. The stack remains unchanged as the event_id is read without consuming it. This instruction reads the event ID from the stack but does not modify the stack depth. Example: with push.1230 on stack, emit reads the event ID 1230 and executes the corresponding event handler. Note that event IDs in the range 0..256 are reserved for system events.
log_deferred [_, STMNT, _, ...] [ROOT_NEW, OUT_RATE1, OUT_CAP, ...] 1 Folds STMNT from stack[4..8] into the VM's rolling deferred root via ROOT_NEW = rate0(Poseidon2([ROOT_PREV, STMNT, [1,0,0,0]])), using the internally maintained previous root and the Tag::AND capacity word [1, 0, 0, 0]. STMNT must be a registered statement for a precompile claim that evaluates to TRUE. Writes three output words, normally dropped by wrappers. Core-library facades and internal support code normally wrap this low-level opcode when precompile claims need to be logged.

Debugging Operations

Procedures for inspecting VM state during execution. These are ordinary miden::core::debug procedure calls that emit events, so adding them changes the program being executed. Procedures with stack inputs also change VM state by consuming those inputs. Remove these calls from production programs.

miden::core::debug

  • Procedures:
    • print_stack: Prints the entire operand stack. Inputs: [...]. Outputs: [...]. Cycles: 3.
    • print_mem: Prints memory in the range [start, end) of the current context. Inputs: [start, end, ...]. Outputs: [...]. Cycles: 5.
    • print_mem_all: Prints the full memory of the current context. Inputs: [...]. Outputs: [...]. Cycles: 3.
    • print_adv_stack: Prints the advice stack in the range [start, end). Inputs: [start, end, ...]. Outputs: [...]. Cycles: 5.
    • print_adv_stack_all: Prints the full advice stack. Inputs: [...]. Outputs: [...]. Cycles: 7.
    • print_adv_map_all: Prints the full advice map. Inputs: [...]. Outputs: [...]. Cycles: 3.
    • print_adv_map_item: Looks up a WORD key in the advice map and prints the associated list of field elements. Inputs: [KEY, ...]. Outputs: [...]. Cycles: 7.
  • Notes:
    • Range-based procedures consume start and end.
    • Advice-map item procedures consume the WORD key.
    • Always active regardless of debug mode.