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 (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 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).

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 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

Arithmetic and Boolean operations

Comparison operations

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

Arithmetic operations

Bitwise operations

Comparison operations

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.

Conditional manipulation

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

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

Non-deterministic inputs

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.

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 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}\).

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 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.

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.