Skip to main content

Design

In the following sections, we provide in-depth descriptions of Miden VM internals, including all AIR constraints for the proving system. We also provide rationale for making specific design choices.

Throughout these sections we adopt the following notations and assumptions:

  • All arithmetic operations, unless noted otherwise, are assumed to be in a prime field with modulus p=264232+1p = 2^{64} - 2^{32} + 1.
  • A binary value means a field element which is either 00 or 11.
  • We use lowercase letters to refer to individual field elements (e.g., aa), and uppercase letters to refer to groups of 44 elements, also referred to as words (e.g., AA). To refer to individual elements within a word, we use numerical subscripts. For example, a0a_0 is the first element of word AA, b3b_3 is the last element of word BB, etc.
  • When describing AIR constraints:
    • For a column xx, we denote the value in the current row simply as xx, and the value in the next row of the column as xx'. Thus, all transition constraints for Miden VM work with two consecutive rows of the execution trace.
    • For multiset equality constraints, we denote random values sent by the verifier after the prover commits to the main execution trace as α0,α1,α2\alpha_0, \alpha_1, \alpha_2 etc.
    • To differentiate constraints from other formulas, we frequently use the following format for constraint equations.
x(x+y)=0 | degree=1x' - (x + y) = 0 \text{ | degree} = 1

In the formula above, the constraint equation is followed by the implied algebraic degree of the constraint. This degree is determined by the number of multiplications between trace columns. If a constraint does not involve any multiplications between columns, its degree is 11. If a constraint involves multiplication between two columns, its degree is 22. If we need to multiply three columns together, the degree is 33 ect.

The maximum allowed constraint degree in Miden VM is 99. If a constraint degree grows beyond that, we frequently need to introduce additional columns to reduce the degree.

VM components

Miden VM consists of several interconnected components, each providing a specific set of functionalities. These components are:

  • Program decoder, which is responsible for computing a commitment to the executing program and converting the program into a sequence of operations executed by the VM.
  • Operand stack, which is a push-down stack which provides operands for all operations executed by the VM.
  • Range checker, which is responsible for providing 16-bit range checks needed by other components.
  • Chiplets, which is a set of specialized circuits used to accelerate commonly-used complex computations. Currently, the VM relies on 3 chiplets:
    • Hash chiplet, used to compute Rescue Prime hashes both for sequential hashing and for Merkle tree hashing.
    • Bitwise chiplet, used to compute bitwise operations (e.g., AND, XOR) over 32-bit integers.
    • Memory chiplet, used to support random-access memory in the VM.

The above components are connected via buses, which are implemented using multiset checks. We also use multiset checks internally within components to describe virtual tables.

VM execution trace

Execution trace of Miden VM consists of 6666 main trace columns, 22 buses, and 66 virtual tables as shown in the diagram below.

vm_trace.png

As can be seen from the image above, decoder, stack, and range checker components use dedicated sets of columns, while all chiplets share the same 1818 columns. To differentiate between chiplets, we use a set of binary selector columns, a combination of which uniquely identifies each chiplet.

In addition to the components described previously, execution trace also contains 22 system columns:

  • clk which is used to keep track of the current VM cycle. Values in this column start out at 00 and are incremented by 11 with each cycle.
  • fmp which contains the value of the free memory pointer used for specifying the region of memory available to procedure locals.

AIR constraints for the fmp column are described in system operations section. For the clk column, the constraints are straightforward:

clk(clk+1)=0 | degree=1clk' - (clk + 1) = 0 \text{ | degree} = 1