# Miden Assembly
###### tags: `specs` `assembly` `draft`

Version: v0.2

Miden assembly is a simple, low-level language for writing programs for Miden VM. It stands just above raw Miden VM instruction set, and in fact, many instructions of Miden assembly map directly to raw instructions of Miden VM.

Before Miden assembly can be executed on Miden VM, it needs to be compiled into a [Program MAST](https://hackmd.io/yr-ieh7SSKOzWw7Kdo9gnA) (Merkelized Abstract Syntax Tree) which is a binary tree of code blocks each containing raw Miden VM instructions.


As compared to raw Miden VM instructions, Miden assembly has several advantages:
1. Miden assembly is intended to be a more stable external interface for the VM. That is, while we plan to make signficant changes to the underlying VM to optimize it for stability, performance etc., we intend to make very few breaking changes to Miden assembly.
2. Miden assembly natively supports control flow expressions which the assembler automatically transforms into a program MAST. This greatly simplifies writing programs with complex execution logic.
3. Miden assembly supports *macro instructions*. These instructions expand into short sequences of raw Miden VM instructions making it easier to encode common operations.
4. Miden assembly supports *procedures*. These are stand-alone blocks of code which the assembler inlines into program MAST at compile time. This improves program modularity and code organization.

The last two points also make Miden assembly much more concise as compared to the raw program MAST. This may be important in the blockchain context where pubic programs need to be stored on chain.

### Design goals

The design of Miden assembly tries to achieve the following goals:

1. Miden assembly should be an easy compilation target for high-level languages.
2. Programs written in Miden assembly should be readable, even if the code is generated by a compiler from a high-level language.
3. Control flow should be easy to understand to help in manual inspection, formal verification, and optimization.
4. Compilation of Miden assembly into Miden program MAST should be as straight-forward as possible.
5. Serialization of Miden assembly into a binary representation should be as compact and as straight-forward as possible.

In order to achieve the first goal, Miden assembly exposes a set of native operations over 32-bit integers and supports linear read-write memory. Thus, from the stand-point of a higher-level language compiler, Miden VM can be viewed as a regular 32-bit stack machine with linear read-write memory.

In order to achieve the second and third goals, Miden assembly facilitates flow control via high-level constructs like `while` loops, `if-else` statements, and function calls with statically defined targets. Thus, for example, there are no explicit `jump` instructions.

In order to achieve the fourth goal, Miden assembly retains direct access to the VM stack rather than abstracting it away with higher-level constructs and named variables.

Lastly, in order to achieve the fifth goal, each instruction of Miden assembly can be encoded using a single byte. The resulting byte-code is simply a one-to-one mapping of instructions to their binary values.

## Miden VM overview
Miden VM is a stack machine. The base data type of the MV is a field element in a 64-bit [prime field](https://en.wikipedia.org/wiki/Finite_field) defined by modulus $p = 2^{64} - 2^{32} + 1$. This means that all values that the VM operates with are field elements in this field (i.e., values between $0$ and $2^{64} - 2^{32}$, both inclusive).

Throughout this document, we use lower-case letters to refer to individual field elements (e.g., $a$). Sometimes it is convenient to describe operations over groups of elements. For these purposes we define a *word* to be a group of four elements. We use upper-case letters to refer to words (e.g., $A$). To refer to individual elements within a word, we use numerical subscripts. For example, $a_0$ is the first element of word $A$, $b_3$ is the last element of word $B$, etc.

Miden VM consists of three high-level components as illustrated below.


These components are:
* **Stack** which is a push-down stack where each item is a field element. Most assembly instructions operate with values located on the stack. The stack can grow up to $2^{16}$ items deep, however, only the top 16 items are directly accessible.
* **Memory** which is a linear random-access read-write memory. The memory is word-addressable, meaning, four elements are located at each address, and we can read and write elements to/from memory in batches of four. Memory addresses can be in the range $[0, 2^{32})$.
* **Advice provider** which is a way for the prover to provide non-deterministic inputs to the VM. The advice provider contains a single *advice tape* and unlimited number of *advice sets*. The latter contain structured data which can be interpreted as a set of Merkle paths.

In the future, additional components (e.g., storage, logs) may be added to the VM.

### Terms and notations
In this note we use the following terms and notations:

- $p$ is the modulus of the VM's base field which is equal to $2^{64} - 2^{32} + 1$.
- A *binary* value means a field element which is either $0$ or $1$.
- Inequality comparisons are assumed to be performed on integer representations of field elements in the range $[0, p)$.

## Code organization
A Miden assembly program is just a sequence of instructions each describing a specific directive or an operation. You can use any combination of whitespace characters to separate one instruction from another.

In turn, Miden assembly instructions are just keywords which can be parameterized by zero or more parameters. The notation for specifying parameters is *keyword.param1.param2* - i.e., the parameters are separated by periods. For example, `push.123` instruction denotes a `push` operation which is parameterized by value `123`.

Currently, Miden assembly provides two types of code organization blocks: *scripts* and *procedures*. In the future, additional blocks such as modules and functions will be added.

### Scripts
A *script* block is used to define an executable program. A script must start with a `begin` instruction and terminate with an `end` instruction. For example:

begin
    <instructions>
end

When Miden assembly code is executed, the execution starts at the first instruction following the `begin` instruction of the script. A script block is expected to be the last block in a program and can be followed only by comment blocks.

### Procedures
A *procedure* block is used to define a frequently-used sequence of instructions. A procedure must start with a `proc.<label>.<number of locals>` instruction and terminate with an `end` instruction. For example:

proc.foo.2
    <instructions>
end

A procedure label must start with a letter and can contain any combination of numbers, ASCII letters, and underscores (`_`).

The number of locals specifies the number of memory-based local words a procedure can access (via `load.local`, `store.local`, and other instructions). If a procedure doesn't need any memory-based locals, this parameter can be omitted or set to `0`. The number of locals per procedure is not limited, but the total number of locals available to all procedures at runtime must be smaller than $2^{32}$.

To execute a procedure an `exec.<label>` instruction should be used. For example:

exec.foo

During compilation, procedures are inlined at their call sites. Thus, from the standpoint of the final program, executing procedures is indistinguishable from manually including procedure code in place of the `exec` instruction.

A procedure may execute any other previously defined procedure from the same source, but it cannot execute itself or any of the subsequent procedures. Thus, recursive procedure calls are not possible. For example, the following code block defines a script with two procedures:

proc.foo
    <instructions>
end

proc.bar
    <instructions>
    exec.foo
    <instructions>
end

begin
    <instructions>
    exec.bar
    <instructions>
    exec.foo
end

### Comments
Miden assembly allows annotating code with simple comments. The comments must be placed between two `#` (pound) characters which must be surrounded by whitespace on both sides. For example:

# this is a comment #

Using a pound character within a comment is not allowed.

When Miden assembly is serialized into binary format, comments are not retained.

## Inputs and outputs
External inputs can be provided to Miden VM in two way:

1. Public inputs can be supplied to the VM by initializing the stack with desired values before a program starts executing. Up to 16 stack items can be initialized in this way.
2. Secret (or non-deterministic) inputs can be supplied to the VM via the *advice provider* (described below). There is no limit on how much data the advice provider can hold.

After a program finishes executing up to 16 elements can remain on the stack. These elements then become the outputs of the program.

Having only 16 elements to describe public inputs and outputs of a program may seem limiting, however, just 4 elements are sufficient to represent a root of a Merkle tree which can be expanded into an arbitrary number of values.

For example, if we wanted to provide a thousand public input values to the VM, we could put these values into a Merkle tree, initialize the stack with the root of this tree, initialize the advice provides with the tree itself, and then retrieve values from the tree during program execution using `mtree.get` instruction (described [here](#Hashing-and-Merkle-trees)).

In the future, other ways of providing public inputs and reading public outputs (e.g., storage commitments) may be added to the VM.

### Non-deterministic inputs
The *advice provider* component is responsible for supplying non-deterministic inputs to the VM. These inputs need to be known only to the prover (i.e., they do not need to be shared with the verifier).

The advice provider consists of two components:
* **Advice tape** which is a one-dimensional array of values. The VM can access only the head of the tape. That is the VM can either remove values from the head of the tape or inject new values at the head of the tape. Formally, this means that the advice tape is actually a stack.
* **Advice sets** which contain structured data reduceable to Merkle paths. Some examples of advice sets are: Merkle tree, Sparse Merkle tree, a collection of Merkle paths. Every advice set can be uniquely identified by its root. The VM can request Merkle paths from an advice set, as well as update an advice set by modifying one of its nodes (this will also change the root of the modified advice set).

The prover initializes the advice provider prior to executing a program, and from that point on the advice provider is manipulated solely by executing operations on the VM.

## Flow control
As mentioned above, Miden assembly provides high-level constructs to facilitate flow control. These constructs are:

- *if-else* expressions for conditional execution.
- *repeat* expressions for bounded counter-controlled loops.
- *while* expressions for unbounded condition-controlled loops.

### Conditional execution
Conditional execution in Miden VM can be accomplished with *if-else* statements. These statements look like so:

if.true
    <instructions>
else
    <instructions>
end

where `instructions` can be a sequence of any instructions, including nested control structures; the `else` clause is optional. The above does the following:

1. Pops the top item from the stack.
2. If the value of the item is $1$, instructions in the `if.true` branch are executed.
3. If the value of the item is $0$, instructions in the `else` branch are executed.
4. If the value is not binary, the execution fails.

A note on performance: using *if-else* statements incurs a small, but non-negligible overhead. Thus, for simple conditional statements, it may be more efficient to compute the result of both branches, and then select the result using [conditional drop](#Conditional-manipulation) instructions.

### Counter-controlled loops
Executing a sequence of instructions a predefined number of times can be accomplished with *repeat* statements. These statements look like so:

repeat.<count>
    <instructions>
end

where:

* `instructions` can be a sequence of any instructions, including nested control structures.
* `count` is the number of times the `instructions` sequence should be repeated (e.g. `repeat.10`). `count` must be an integer greater than $0$.

### Condition-controlled loops
Executing a sequence of instructions zero or more times based on some condition can be accomplished with *while loop* expressions. These expressions look like so:

while.true
    <instructions>
end

where `instructions` can be a sequence of any instructions, including nested control structures. The above does the following:

1. Pops the top item from the stack.
2. If the value of the item is $1$, `instructions` in the loop body are executed.
a. After the body is executed, the stack is popped again, and if the popped value is $1$, the body is executed again.
b. If the popped value is $0$, the loop is exited.
c. If the popped value is not binary, the execution fails.
3. If the value of the item is $0$, execution of loop body is skipped.
4. If the value is not binary, the execution fails.

## Field operations
Miden assembly provides a set of instructions which can perform operations with raw field elements. These instructions are described in the tables below.

While most operations place no restrictions on inputs, some operations expect inputs to be binary values, and fail if executed with non-binary inputs.

For instructions where one or more operands can be provided as immediate parameters (e.g., `add` and `add.b`), we provide stack transition diagrams only for the non-immediate version. For the immediate version, it can be assumed that the operand with the specified name is not present on the stack.

### Assertions and tests

| Instruction | Stack_input | Stack_output | Notes |
| ---------------- | ----------- | ------------- | ----------------------------- |
| assert | [a, ...] | [...] | If $a = 1$, removes it from the stack. <br> Fails if $a \ne 1$ |
| assert.eq | [b, a, ...] | [...] | If $a = b$, removes them from the stack. <br> Fails if $a \ne b$ |

### Arithmetic and Boolean operations

| Instruction | Stack_input | Stack_output | Notes |
| ---------------- | ----------- | ------------- | ----------------------------- |
| add <br> add.*b* | [b, a, ...] | [c, ...] | $c \leftarrow (a + b) \mod p$ |
| sub <br> sub.*b* | [b, a, ...] | [c, ...] | $c \leftarrow (a - b) \mod p$ |
| mul <br> mul.*b* | [b, a, ...] | [c, ...] | $c \leftarrow (a \cdot b) \mod p$ |
| div <br> div.*b* | [b, a, ...] | [c, ...] | $c \leftarrow (a \cdot b^{-1}) \mod p$ <br> Fails if $b = 0$ |
| neg | [a, ...] | [b, ...] | $b \leftarrow -a \mod p$ |
| inv | [a, ...] | [b, ...] | $b \leftarrow a^{-1} \mod p$ <br> Fails if $a = 0$ |
| pow2 | [a, ...] | [b, ...] | $b \leftarrow 2^a$ <br> Fails if $a > 63$ |
| not | [a, ...] | [b, ...] | $b \leftarrow 1 - a$ <br> Fails if $a > 1$ |
| and | [b, a, ...] | [c, ...] | $c \leftarrow a \cdot b$ <br> Fails if $max(a, b) > 1$ |
| or | [b, a, ...] | [c, ...] | $c \leftarrow a + b - a \cdot b$ <br> Fails if $max(a, b) > 1$ |
| xor | [b, a, ...] | [c, ...] | $c \leftarrow a + b - 2 \cdot a \cdot b$ <br> Fails if $max(a, b) > 1$ |

### Comparison operations

| Instruction | Stack_input | Stack_output | Notes |
| ---------------- | ----------- | -------------- | ----------------------------- |
| eq <br> eq.*b* | [b, a, ...] | [c, ...] | $c \leftarrow \begin{cases} 1, & \text{if}\ a=b \\ 0, & \text{otherwise}\ \end{cases}$ |
| neq <br> neq.*b* | [b, a, ...] | [c, ...] | $c \leftarrow \begin{cases} 1, & \text{if}\ a \ne b \\ 0, & \text{otherwise}\ \end{cases}$ |
| lt | [b, a, ...] | [c, ...] | $c \leftarrow \begin{cases} 1, & \text{if}\ a < b \\ 0, & \text{otherwise}\ \end{cases}$ |
| lte | [b, a, ...] | [c, ...] | $c \leftarrow \begin{cases} 1, & \text{if}\ a \le b \\ 0, & \text{otherwise}\ \end{cases}$ |
| gt | [b, a, ...] | [c, ...] | $c \leftarrow \begin{cases} 1, & \text{if}\ a > b \\ 0, & \text{otherwise}\ \end{cases}$ |
| gte | [b, a, ...] | [c, ...] | $c \leftarrow \begin{cases} 1, & \text{if}\ a \ge b \\ 0, & \text{otherwise}\ \end{cases}$ |
| eqw | [A, B, ...] | [c, A, B, ...] | $c \leftarrow \begin{cases} 1, & \text{if}\ a_i = b_i \; \forall i \in \{0, 1, 2, 3\} \\ 0, & \text{otherwise}\ \end{cases}$ |

## u32 operations
Miden assembly provides a set of instructions which can perform operations on regular 32-bit integers. These instructions are described in the tables below.

Many instructions have *safe* and *unsafe* versions. The safe versions ensure that input values are 32-bit integers, and fail if that's not the case. The *unsafe* versions do not perform these checks, and thus, should be used only if the inputs are known to be 32-bit integers. Supplying inputs which are greater than or equal to $2^{32}$ to *unsafe* operations results in undefined behavior.

The primary benefit of using *unsafe* operations is performance: they can frequently be executed $2$ or $3$ times faster than their safe counterparts. In general, vast majority of the *unsafe* operations listed below can be executed in a single VM cycle.

For instructions where one or more operands can be provided as immediate parameters (e.g., `u32add` and `u32add.b`), we provide stack transition diagrams only for the non-immediate version. For the immediate version, it can be assumed that the operand with the specified name is not present on the stack.

### Conversions and tests

| Instruction | Stack input | Stack output | Notes |
| ------------- | ----------- | ------------- | ------------------------------------------ |
| u32test | [a, ...] | [b, a, ...] | $b \leftarrow \begin{cases} 1, & \text{if}\ a < 2^{32} \\ 0, & \text{otherwise}\ \end{cases}$ |
| u32testw | [A, ...] | [b, A, ...] | $b \leftarrow \begin{cases} 1, & \text{if}\ \forall\ i \in \{0, 1, 2, 3\}\ a_i < 2^{32} \\ 0, & \text{otherwise}\ \end{cases}$ |
| u32assert | [a, ...] | [a, ...] | Fails if $a \ge 2^{32}$ |
| u32assertw | [A, ...] | [A, ...] | Fails if $\exists\ i \in \{0, 1, 2, 3\} \ni a_i \ge 2^{32}$ |
| u32cast | [a, ...] | [b, ...] | $b \leftarrow a \mod 2^{32}$ |
| u32split | [a, ...] | [c, b, ...] | $b \leftarrow a \mod 2^{32}$, $c \leftarrow \lfloor{a / 2^{32}}\rfloor$ |

### Arithmetic operations

| Instruction | Stack_input | Stack_output | Notes |
| -------------- | -------------- | ------------- | ------------------------------------------ |
| u32add <br> u32add.*b* | [b, a, ...] | [c, ...] | $c \leftarrow a + b$ <br> Fails if $max(a, b, c) \ge 2^{32}$ |
| u32add.full | [b, a, ...] | [d, c, ...] | $c \leftarrow (a + b) \mod 2^{32}$ <br> $d \leftarrow \begin{cases} 1, & \text{if}\ (a + b) \ge 2^{32} \\ 0, & \text{otherwise}\ \end{cases}$ <br> Fails if $max(a, b) \ge 2^{32}$ |
| u32add.unsafe | [b, a, ...] | [d, c, ...] | $c \leftarrow (a + b) \mod 2^{32}$, <br> $d \leftarrow \begin{cases} 1, & \text{if}\ (a + b) \ge 2^{32} \\ 0, & \text{otherwise}\ \end{cases}$ <br> Undefined if $max(a, b) \ge 2^{32}$ |
| u32addc | [b, a, c, ...] | [e, d, ...] | $d \leftarrow (a + b + c) \mod 2^{32}$ <br> $e \leftarrow \begin{cases} 1, & \text{if}\ (a + b + c) \ge 2^{32} \\ 0, & \text{otherwise}\ \end{cases}$ <br> Fails if $max(a, b) \ge 2^{32}$ or $c > 1$ |
| u32addc.unsafe | [b, a, c, ...] | [e, d, ...] | $d \leftarrow (a + b + c) \mod 2^{32}$, <br> $e \leftarrow \begin{cases} 1, & \text{if}\ (a + b + c) \ge 2^{32} \\ 0, & \text{otherwise}\ \end{cases}$ <br> Undefined if $max(a, b) \ge 2^{32}$ <br> Fails if $c > 1$ |
| u32sub <br> u32sub.*b* | [b, a, ...] | [c, ...] | $c \leftarrow (a - b)$ <br> Fails if $max(a, b) \ge 2^{32}$ or $a < b$ |
| u32sub.full | [b, a, ...] | [d, c, ...] | $c \leftarrow (a - b) \mod 2^{32}$ <br> $d \leftarrow \begin{cases} 1, & \text{if}\ a < b \\ 0, & \text{otherwise}\ \end{cases}$ <br> Fails if $max(a, b) \ge 2^{32}$ |
| u32sub.unsafe | [b, a, ...] | [d, c, ...] | $c \leftarrow (a - b) \mod 2^{32}$ <br> $d \leftarrow \begin{cases} 1, & \text{if}\ a < b \\ 0, & \text{otherwise}\ \end{cases}$ <br> Undefined if $max(a, b) \ge 2^{32}$ |
| u32mul <br> u32mul.*b* | [b, a, ...] | [c, ...] | $c \leftarrow a \cdot b$ <br> Fails if $max(a, b, c) \ge 2^{32}$ |
| u32mul.full | [b, a, ...] | [d, c, ...] | $c \leftarrow (a \cdot b) \mod 2^{32}$ <br> $d \leftarrow \lfloor(a \cdot b) / 2^{32}\rfloor$ <br> Fails if $max(a, b) \ge 2^{32}$ |
| u32mul.unsafe | [b, a, ...] | [d, c, ...] | $c \leftarrow (a \cdot b) \mod 2^{32}$ <br> $d \leftarrow \lfloor(a \cdot b) / 2^{32}\rfloor$ <br> Undefined if $max(a, b) \ge 2^{32}$ |
| u32madd | [b, a, c, ...] | [e, d, ...] | $d \leftarrow (a \cdot b + c) \mod 2^{32}$ <br> $e \leftarrow \lfloor(a \cdot b + c) / 2^{32}\rfloor$ <br> Fails if $max(a, b, c) \ge 2^{32}$ |
| u32madd.unsafe | [b, a, c, ...] | [e, d, ...] | $d \leftarrow (a \cdot b + c) \mod 2^{32}$ <br> $e \leftarrow \lfloor(a \cdot b + c) / 2^{32}\rfloor$ <br> Undefined if $max(a, b, c) \ge 2^{32}$ |
| u32div <br> u32div.*b* | [b, a, ...] | [c, ...] | $c \leftarrow \lfloor a / b\rfloor$ <br> Fails if $max(a, b) \ge 2^{32}$ or $b = 0$ |
| u32div.full | [b, a, ...] | [d, c, ...] | $c \leftarrow \lfloor a / b\rfloor$ <br> $d \leftarrow a \mod b$ <br> Fails if $max(a, b) \ge 2^{32}$ or $b = 0$ |
| u32div.unsafe | [b, a, ...] | [d, c, ...] | $c \leftarrow \lfloor a / b\rfloor$ <br> $d \leftarrow a \mod b$ <br> Fails if $b = 0$ <br> Undefined if $max(a, b) \ge 2^{32}$ |
| u32mod <br> u32mod.*b* | [b, a, ...] | [c, ...] | $c \leftarrow a \mod b$ <br> Fails if $max(a, b) \ge 2^{32}$ or $b = 0$ |
| u32mod.unsafe | [b, a, ...] | [c, ...] | $c \leftarrow a \mod b$ <br> Fails if $b = 0$ <br> Undefined if $max(a, b) \ge 2^{32}$ |

### Bitwise operations

| Instruction | Stack_input | Stack_output | Notes |
| -------------- | -------------- | ------------- | ------------------------------------------ |
| u32and | [b, a, ...] | [c, ...] | Computes $c$ as a bitwise `AND` of binary representations of $a$ and $b$. <br> Fails if $max(a,b) \ge 2^{32}$ |
| u32or | [b, a, ...] | [c, ...] | Computes $c$ as a bitwise `OR` of binary representations of $a$ and $b$. <br> Fails if $max(a,b) \ge 2^{32}$ |
| u32xor | [b, a, ...] | [c, ...] | Computes $c$ as a bitwise `XOR` of binary representations of $a$ and $b$. <br> Fails if $max(a,b) \ge 2^{32}$ |
| u32not | [a, ...] | [b, ...] | Computes $b$ as a bitwise `NOT` of binary representation of $a$. <br> Fails if $a \ge 2^{32}$ |
| u32shl <br> u32shl.*b* | [b, a, ...] | [c, ...] | $c \leftarrow (a \cdot 2^b) \mod 2^{32}$ <br> Fails if $a \ge 2^{32}$ or $b > 31$ |
| u32shr <br> u32shr.*b* | [b, a, ...] | [c, ...] | $c \leftarrow \lfloor a/2^b \rfloor$ <br> Fails if $a \ge 2^{32}$ or $b > 31$ |
| u32rotl <br> u32rotl.*b* | [b, a, ...] | [c, ...] | Computes $c$ by rotating a 32-bit representation of $a$ to the left by $b$ bits. <br> Fails if $a \ge 2^{32}$ or $b > 31$ |
| u32rotr <br> u32rotr.*b* | [b, a, ...] | [c, ...] | Computes $c$ by rotating a 32-bit representation of $a$ to the right by $b$ bits. <br> Fails if $a \ge 2^{32}$ or $b > 31$ |

### Comparison operations

| Instruction | Stack_input | Stack_output | Notes |
| -------------- | ------------ | --------------- | ------------------------------------------ |
| u32.eq <br> u32.eq.*b* | [b, a, ...] | [c, ...] | $c \leftarrow \begin{cases} 1, & \text{if}\ a=b \\ 0, & \text{otherwise}\ \end{cases}$ <br> Fails if $max(a, b) \ge 2^{32}$ <br> Note: unsafe version is not provided because it is equivalent to simple `eq`. |
| u32.neq <br> u32.neq.*b* | [b, a, ...] | [c, ...] | $c \leftarrow \begin{cases} 1, & \text{if}\ a \ne b \\ 0, & \text{otherwise}\ \end{cases}$ <br> Fails if $max(a, b) \ge 2^{32}$ <br> Note: unsafe version is not provided because it is equivalent to simple `neq`. |
| u32lt | [b, a, ...] | [c, ...] | $c \leftarrow \begin{cases} 1, & \text{if}\ a < b \\ 0, & \text{otherwise}\ \end{cases}$ <br> Fails if $max(a, b) \ge 2^{32}$ |
| u32lt.unsafe | [b, a, ...] | [c, ...] | $c \leftarrow \begin{cases} 1, & \text{if}\ a < b \\ 0, & \text{otherwise}\ \end{cases}$ <br> Undefined if $max(a, b) \ge 2^{32}$ |
| u32lte | [b, a, ...] | [c, ...] | $c \leftarrow \begin{cases} 1, & \text{if}\ a \le b \\ 0, & \text{otherwise}\ \end{cases}$ <br> Fails if $max(a, b) \ge 2^{32}$ |
| u32lte.unsafe | [b, a, ...] | [c, ...] | $c \leftarrow \begin{cases} 1, & \text{if}\ a \le b \\ 0, & \text{otherwise}\ \end{cases}$ <br> Undefined if $max(a, b) \ge 2^{32}$ |
| u32gt | [b, a, ...] | [c, ...] | $c \leftarrow \begin{cases} 1, & \text{if}\ a > b \\ 0, & \text{otherwise}\ \end{cases}$ <br> Fails if $max(a, b) \ge 2^{32}$ |
| u32gt.unsafe | [b, a, ...] | [c, ...] | $c \leftarrow \begin{cases} 1, & \text{if}\ a > b \\ 0, & \text{otherwise}\ \end{cases}$ <br> Undefined if $max(a, b) \ge 2^{32}$ |
| u32gte | [b, a, ...] | [c, ...] | $c \leftarrow \begin{cases} 1, & \text{if}\ a \ge b \\ 0, & \text{otherwise}\ \end{cases}$ <br> Fails if $max(a, b) \ge 2^{32}$ |
| u32gte.unsafe | [b, a, ...] | [c, ...] | $c \leftarrow \begin{cases} 1, & \text{if}\ a \ge b \\ 0, & \text{otherwise}\ \end{cases}$ <br> Undefined if $max(a, b) \ge 2^{32}$ |
| u32min | [b, a, ...] | [c, ...] | $c \leftarrow \begin{cases} a, & \text{if}\ a < b \\ b, & \text{otherwise}\ \end{cases}$ <br> Fails if $max(a, b) \ge 2^{32}$ |
| u32min.unsafe | [b, a, ...] | [c, ...] | $c \leftarrow \begin{cases} a, & \text{if}\ a < b \\ b, & \text{otherwise}\ \end{cases}$ <br> Undefined if $max(a, b) \ge 2^{32}$ |
| u32max | [b, a, ...] | [c, ...] | $c \leftarrow \begin{cases} a, & \text{if}\ a > b \\ b, & \text{otherwise}\ \end{cases}$ <br> Fails if $max(a, b) \ge 2^{32}$ |
| u32max.unsafe | [b, a, ...] | [c, ...] | $c \leftarrow \begin{cases} a, & \text{if}\ a > b \\ b, & \text{otherwise}\ \end{cases}$ <br> Undefined if $max(a, b) \ge 2^{32}$ |

## Stack manipulation
Miden VM stack is a push-down stack of field elements. The stack has a maximum depth of $2^{16}$, but only the top $16$ elements are directly accessible via the instructions listed below.

In addition to the typical stack manipulation instructions such as `drop`, `dup`, `swap` etc., Miden assembly provides several conditional instructions which can be used to manipulate the stack based on some condition - e.g., conditional swap `cswap` or conditional drop `cdrop`.

| Instruction | Stack_input | Stack_output | Notes |
| ----------- | ----------------- | ------------------ | ------------------------------------------ |
| drop | [a, ... ] | [ ... ] | Deletes the top stack item. |
| dropw | [A, ... ] | [ ... ] | Deletes a word (4 elements) from the top of the stack. |
| padw | [ ... ] | [0, 0, 0, 0, ... ] | Pushes four $0$ values onto the stack. <br> Note: simple `pad` is not provided because `push.0` does the same thing. |
| dup.*n* | [ ..., a, ... ] | [a, ..., a, ... ] | Pushes a copy of the $n$th stack item onto the stack. `dup` and `dup.0` are the same instruction. Valid for $n \in \{0, ..., 15\}$ |
| dupw.*n* | [ ..., A, ... ] | [A, ..., A, ... ] | Pushes a copy of the $n$th stack word onto the stack. `dupw` and `dupw.0` are the same instruction. Valid for $n \in \{0, 1, 2, 3\}$ |
| swap.*n* | [a, ..., b, ... ] | [b, ..., a, ... ] | Swaps the top stack item with the $n$th stack item. `swap` and `swap.1` are the same instruction. Valid for $n \in \{1, ..., 15\}$ |
| swapw.*n* | [A, ..., B, ... ] | [B, ..., A, ... ] | Swaps the top stack word with the $n$th stack word. `swapw` and `swapw.1` are the same instruction. Valid for $n \in \{1, 2, 3\}$ |
| movup.*n* | [ ..., a, ... ] | [a, ... ] | Moves the $n$th stack item to the top of the stack. Valid for $n \in \{2, ..., 15\}$ |
| movupw.*n* | [ ..., A, ... ] | [A, ... ] | Moves the $n$th stack word to the top of the stack. Valid for $n \in \{2, 3\}$ |
| movdn.*n* | [a, ... ] | [ ..., a, ... ] | Moves the top stack item to the $n$th position of the stack. Valid for $n \in \{2, ..., 15\}$ |
| movdnw.*n* | [A, ... ] | [ ..., A, ... ] | Moves the top stack word to the $n$th word position of the stack. Valid for $n \in \{2, 3\}$ |

### Conditional manipulation

| Instruction | Stack_input | Stack_output | Notes |
| ----------- | ----------------- | ------------------ | ------------------------------------------ |
| cswap | [c, b, a, ... ] | [e, d, ... ] | $d = \begin{cases} a, & \text{if}\ c = 0 \\ b, & \text{if}\ c = 1\ \end{cases}$ $e = \begin{cases} b, & \text{if}\ c = 0 \\ a, & \text{if}\ c = 1\ \end{cases}$ <br> Fails if $c > 1$ |
| cswapw | [c, B, A, ... ] | [E, D, ... ] | $D = \begin{cases} A, & \text{if}\ c = 0 \\ B, & \text{if}\ c = 1\ \end{cases}$ $E = \begin{cases} B, & \text{if}\ c = 0 \\ A, & \text{if}\ c = 1\ \end{cases}$ <br> Fails if $c > 1$ |
| cdrop | [c, b, a, ... ] | [d, ... ] | $d = \begin{cases} a, & \text{if}\ c = 0 \\ b, & \text{if}\ c = 1\ \end{cases}$ <br> Fails if $c > 1$ |
| cdropw | [c, B, A, ... ] | [D, ... ] | $D = \begin{cases} A, & \text{if}\ c = 0 \\ B, & \text{if}\ c = 1\ \end{cases}$ <br> Fails if $c > 1$ |

## Input / output operations
Miden assembly provides a set of instructions for moving data between the stack and several other sources. These sources include:

* **Program code**: values to be moved onto the stack can be hard-coded in a program's source code.
* **Environment**: values can be moved onto the stack from environment variables. Currently, the only available environment variable is *stack_depth* which holds the current depth of the stack. In the future, other environment variables may be added.
* **Advice tape**: values can be moved onto the stack from a non-deterministic advice tape contained within the advice provider. Values are always read from the head of the advice tape, and once a value is read, it is removed from the tape. There is no limit on the number of values in the advice tape.
* **Memory**: values can be moved between the stack and random-access memory. The memory is word-addressable, meaning, four elements are located at each address, and we can read and write elements to/from memory in batches of four. Memory can be accessed via absolute memory references (i.e., via memory addresses) as well as via local procedure references (i.e., local index). The latter approach ensures that a procedure does not access locals of another procedure.

In the future several other sources such as *storage* and *logs* may be added.

### Constant inputs

| Instruction | Stack_input | Stack_output | Notes |
| --------------- | ----------- | ------------ | ------------------------------------------ |
| push.*a* <br> push.*a*.*b* <br> push.*a*.*b*.*c*... | [...] | [a, ...] <br> [b, a, ...] <br> [c, b, a, ...] | Pushes values $a$, $b$, $c$ etc. onto the stack. Up to $16$ values can be specified. All values must be valid field elements in decimal (e.g., $123$) or hexadecimal (e.g., $0x7b$) representation. |

When specifying values in hexadecimal format, it is possible to omit the periods between individual values as long as total number of specified bytes is a multiple of $8$. That is, the following are semantically equivalent:

push.0x1234.0xabcd
push.0x0000000000001234000000000000abcd

In both case the values must still encode valid field elements.

### Environment inputs

| Instruction | Stack_input | Stack_output | Notes |
| -------------------- | ----------- | ------------ | ------------------------------------------ |
| push.env.sdepth | [...] | [d, ...] | $d \leftarrow stack.depth()$ <br> Pushes the current depth of the stack onto the stack. |
| push.env.locaddr.*i* | [...] | [a, ...] | $a \leftarrow address\_of(i)$ <br> Pushes the absolute memory address of local memory at index $i$ onto the stack. |

### Non-deterministic inputs

| Instruction | Stack_input_ | Stack_output | Notes |
| -------------- | --------------- | ------------ | ------------------------------------------ |
| push.adv.*n* | [ ... ] | [a, ... ] | $a \leftarrow tape.next()$ <br> Removes the next $n$ values from advice tape and pushes them onto the stack. Valid for $n \in \{1, ..., 16\}$. <br> Fails if the advice tape has fewer than $n$ values. |
| loadw.adv | [0, 0, 0, 0, ... ] | [A, ... ] | $A \leftarrow tape.next\_word()$ <br> Removes the next word (4 elements) from the advice tape and overwrites the top four stack elements with it. <br> Fails if the advice tape has fewer than $4$ values. |

### Random access memory

As mentioned above, there are two ways to access memory in Miden VM. The first way is via memory addresses using the instructions listed below. The addresses are absolute - i.e., they don't depend on the procedure context. Memory addresses can be in the range $[0, 2^{32})$.

Memory is guaranteed to be initialized to zeros. Thus, when reading from memory address which hasn't been written to previously, zero elements will be returned.

| Instruction | Stack_input___ | Stack_output | Notes |
| -------------- | -------------- | ------------ | ------------------------------------------ |
| push.mem <br> push.mem.*a* | [a, ... ] | [v, ... ] | $a \leftarrow mem[a][0]$ <br> Reads a word (4 elements) from memory at address *a*, and pushes the first element of the word onto the stack. If $a$ is provided via the stack, it is removed from the stack first. <br> Fails if $a \ge 2^{32}$ |
| pushw.mem <br> pushw.mem.*a* | [a, ... ] | [A, ... ] | $A \leftarrow mem[a]$ <br> Reads a word from memory at address $a$ and pushes it onto the stack. If $a$ is provided via the stack, it is removed from the stack first. <br> Fails if $a \ge 2^{32}$ |
| loadw.mem <br> loadw.mem.*a* | [a, 0, 0, 0, 0, ...] | [A, ... ] | $A \leftarrow mem[a]$ <br> Reads a word from memory at address $a$ and overwrites top four stack elements with it. If $a$ is provided via the stack, it is removed from the stack first. <br> Fails if $a \ge 2^{32}$ |
| pop.mem <br> pop.mem.*a* | [a, v, ...] | [ ... ] | $[v, 0, 0, 0] \rightarrow mem[a]$ <br> Pops an element off the stack and stores it as the first element of the word in memory at address $a$. All other elements of the word are set to $0$. If $a$ is provided via the stack, it is removed from the stack first. <br> Fails if $a \ge 2^{32}$ |
| popw.mem <br> popw.mem.*a* | [a, A, ...] | [ ... ] | $A \rightarrow mem[a]$ <br> Pops the top four elements off the stack and stores them in memory at address $a$. If $a$ is provided via the stack, it is removed from the stack first. <br> Fails if $a \ge 2^{32}$ |
| storew.mem <br> storew.mem.*a* | [a, A, ...] | [A, ... ] | $A \rightarrow mem[a]$ <br> Stores the top four elements of the stack in memory at address $a$. If $a$ is provided via the stack, it is removed from the stack first. <br> Fails if $a \ge 2^{32}$ |

The second way to access memory is via procedure locals using the instructions listed below. These instructions are available only in procedure context. The number of locals available to a given procedure must be specified at [procedure declaration](#Procedures) time, and trying to access more locals than was declared will result in a compile-time error. The number of locals per procedure is not limited, but the total number of locals available to all procedures at runtime must be smaller than $2^{32}$.

| Instruction | Stack_input_ | Stack_output | Notes |
| -------------- | -------------- | ------------ | ------------------------------------------ |
| push.local.*i* | [ ... ] | [v, ... ] | $v \leftarrow local[i][0]$ <br> Reads a word (4 elements) from local memory at index *i*, and pushes the first element of the word onto the stack. |
| pushw.local.*i* | [...] | [A, ... ] | $A \leftarrow local[i]$ <br> Reads a word from local memory at index $i$ and pushes it onto the stack. |
| loadw.local.*i* | [0, 0, 0, 0, ...] | [A, ... ] | $A \leftarrow local[i]$ <br> Reads a word from local memory at index $i$ and overwrites top four stack elements with it. |
| pop.local.*i* | [v, ...] | [ ... ] | $[v, 0, 0, 0] \rightarrow local[i]$ <br> Pops an element off the stack and stores it as the first element of the word in local memory at index $i$. All other elements of the word are set to $0$. |
| popw.local.*i* | [A, ...] | [ ... ] | $A \rightarrow local[i]$ <br> Pops the top four elements off the stack and stores them in local memory at index $i$. |
| storew.local.*i* | [A, ...] | [A, ... ] | $A \rightarrow local[i]$ <br> Stores the top four elements of the stack in local memory at index $i$. |

Unlike regular memory, procedure locals are not guaranteed to be initialized to zeros. Thus, when working with locals, one must assume that before a local memory address has been written to, it contains "garbage".

Internally in the VM, procedure locals are stored at memory offset stating at $2^{30}$. Thus, every procedure local has an absolute address in regular memory. The `push.env.locaddr` is provided specifically to map an index of a procedure's local to an absolute address so that it can be passed to downstream procedures, when needed.

## Cryptographic operations
Miden assembly provides a set of instructions for performing common cryptographic operations. These instructions are listed in the table below.

### Hashing and Merkle trees
[Rescue Prime](https://eprint.iacr.org/2020/1143) is the native hash function of Miden VM. The parameters of the hash function were chosen to provide 128-bit security level against preimage and collision attacks. The function operates over a state of 12 field elements, and requires 7 rounds for a single permutation. However, due to its special status within the VM, computing Rescue Prime hashes can be done very efficiently. For example, applying a permutation of the hash function can be done in a single VM cycle.

| Instruction | Stack_input | Stack_output | Notes |
| -------------- | --------------- | -------------- | ------------------------------------------ |
| rpperm | [C, B, A, ...] | [F, E, D, ...] | $\{D, E, F\} \leftarrow permute(A, B, C)$ <br> where, $permute()$ computes a Rescue Prime permutation. |
| rphash | [B, A, ...] | [C, ...] | $C \leftarrow hash(A,B)$ <br> where, $hash()$ computes a 2-to-1 Rescue Prime hash. |
| mtree.get | [d, i, R, ...] | [V, R, ...] | Verifies that a Merkle tree with root $R$ opens to node $V$ at depth $d$ and index $i$. Merkle tree with root $R$ must be present in the advice provider, otherwise execution fails. |
| mtree.set | [d, i, V, R, ...] | [V, R', ...] | Updates a node in the Merkle tree with root $R$ at depth $d$ and index $i$ to value $V$. $R'$ is the Merkle root of the resulting tree. Merkle tree with root $R$ must be present in the advice provider, otherwise execution fails. At the end of the operation Merkle tree with root $R$ is removed from the advice provider. |
| mtree.cwm | [d, i, V, R, ...] | [V, R', R, ...] | Copies a Merkle tree with root $R$ and updates a node at depth $d$ and index $i$ in the copied tree to value $V$. $R'$ is the Merkle root of the new tree. Merkle tree with root $R$ must be present in the advice provider, otherwise execution fails. At the end of the operation the advice provider will contain both Merkle trees.

## Debugging
To support basic debugging capabilities, Miden assembly provides `debug` instruction. This instruction prints out the state of the VM at the time when the `debug` instruction is executed. Debug instruction can be parameterized as follows:

- `debug.all` prints out the entire state of the VM (stack and RAM).
- `debug.stack` prints out the entire contents of the stack.
- `debug.stack.<n>` prints out the top $n$ items of the stack. $n$ must be an integer greater than $0$.
- `debug.mem` prints out the entire contents of RAM.
- `debug.mem.<n>` prints out contents of memory at address $n$.
- `debug.mem.<n>.<m>` prints out the contents of memory starting at address $n$ and ending at address $m$ (both inclusive). $m$ must be greater than $n$.
- `debug.local` prints out all locals of the currently executing procedure.
- `debug.local.<n>` prints out contents of the local at index $n$ for the currently executing procedure.

Debug instructions do not affect VM state, do not change program hash, and are omitted when Miden assembly is serialized into binary format.