Cryptographic operations

In this section we describe the AIR constraints for Miden VM cryptographic operations.

Cryptographic operations in Miden VM are performed by the Hash chiplet. Communication between the stack and the hash chiplet is accomplished via the chiplet bus . To make requests to and to read results from the chiplet bus we need to divide its current value by the value representing the request.

Thus, to describe AIR constraints for the cryptographic operations, we need to define how to compute these input and output values within the stack. We do this in the following sections.

HPERM

The HPERM operation applies Rescue Prime Optimized permutation to the top elements of the stack. The stack is assumed to be arranged so that the elements of the rate are at the top of the stack. The capacity word follows, with the number of elements to be hashed at the deepest position in stack. The diagram below illustrates this graphically.

hperm

In the above, (located in the helper register ) is the row address from the hash chiplet set by the prover non-deterministically.

For the HPERM operation, we define input and output values as follows:

In the above, and are the unique operation labels for initiating a linear hash and reading the full state of the hasher respectively. Also note that the term for is missing from the above expressions because for Rescue Prime Optimized permutation computation the index column is expected to be set to .

Using the above values, we can describe the constraint for the chiplet bus column as follows:

The above constraint enforces that the specified input and output rows must be present in the trace of the hash chiplet, and that they must be exactly rows apart.

The effect of this operation on the rest of the stack is:

  • No change starting from position .

MPVERIFY

The MPVERIFY operation verifies that a Merkle path from the specified node resolves to the specified root. This operation can be used to prove that the prover knows a path in the specified Merkle tree which starts with the specified node.

Prior to the operation, the stack is expected to be arranged as follows (from the top):

  • Value of the node, 4 elements ( in the below image)
  • Depth of the path, 1 element ( in the below image)
  • Index of the node, 1 element ( in the below image)
  • Root of the tree, 4 elements ( in the below image)

The Merkle path itself is expected to be provided by the prover non-deterministically (via the advice provider). If the prover is not able to provide the required path, the operation fails. Otherwise, the state of the stack does not change. The diagram below illustrates this graphically.

mpverify

In the above, (located in the helper register ) is the row address from the hash chiplet set by the prover non-deterministically.

For the MPVERIFY operation, we define input and output values as follows:

In the above, and are the unique operation labels for initiating a Merkle path verification computation and reading the hash result respectively. The sum expression for inputs computes the value of the leaf node, while the sum expression for the output computes the value of the tree root.

Using the above values, we can describe the constraint for the chiplet bus column as follows:

The above constraint enforces that the specified input and output rows must be present in the trace of the hash chiplet, and that they must be exactly rows apart, where is the depth of the node.

The effect of this operation on the rest of the stack is:

  • No change starting from position .

MRUPDATE

The MRUPDATE operation computes a new root of a Merkle tree where a node at the specified position is updated to the specified value.

The stack is expected to be arranged as follows (from the top):

  • old value of the node, 4 element ( in the below image)
  • depth of the node, 1 element ( in the below image)
  • index of the node, 1 element ( in the below image)
  • current root of the tree, 4 elements ( in the below image)
  • new value of the node, 4 element ( in the below image)

The Merkle path for the node is expected to be provided by the prover non-deterministically (via merkle sets). At the end of the operation, the old node value is replaced with the new root value computed based on the provided path. Everything else on the stack remains the same. The diagram below illustrates this graphically.

mrupdate

In the above, (located in the helper register ) is the row address from the hash chiplet set by the prover non-deterministically.

For the MRUPDATE operation, we define input and output values as follows:

In the above, the first two expressions correspond to inputs and outputs for verifying the Merkle path between the old node value and the old tree root, while the last two expressions correspond to inputs and outputs for verifying the Merkle path between the new node value and the new tree root. The hash chiplet ensures the same set of sibling nodes are uses in both of these computations.

The , , and are the unique operation labels used by the above computations.

The above constraint enforces that the specified input and output rows for both, the old and the new node/root combinations, must be present in the trace of the hash chiplet, and that they must be exactly rows apart, where is the depth of the node. It also ensures that the computation for the old node/root combination is immediately followed by the computation for the new node/root combination.

The effect of this operation on the rest of the stack is:

  • No change for positions starting from .

FRIE2F4

The FRIE2F4 operation performs FRI layer folding by a factor of 4 for FRI protocol executed in a degree 2 extension of the base field. It also performs several computations needed for checking correctness of the folding from the previous layer as well as simplifying folding of the next FRI layer.

The stack for the operation is expected to be arranged as follows:

  • The first stack elements contain query points to be folded. Each point is represented by two field elements because points to be folded are in the extension field. We denote these points as , , , .
  • The next element is the query position in the folded domain. It can be computed as , where is the position in the source domain, and is size of the folded domain.
  • The next element is a value indicating domain segment from which the position in the original domain was folded. It can be computed as . Since the size of the source domain is always times bigger than the size of the folded domain, possible domain segment values can be , , , or .
  • The next element is a power of initial domain generator which aid in a computation of the domain point .
  • The next two elements contain the result of the previous layer folding - a single element in the extension field denoted as .
  • The next two elements specify a random verifier challenge for the current layer defined as .
  • The last element on the top of the stack () is expected to be a memory address of the layer currently being folded.

The diagram below illustrates stack transition for FRIE2F4 operation.

frie2f4

At the high-level, the operation does the following:

  • Computes the domain value based on values of and .
  • Using and , folds the query values into a single value .
  • Compares the previously folded value to the appropriate value of to verify that the folding of the previous layer was done correctly.
  • Computes the new value of as (this is done in two steps to keep the constraint degree low).
  • Increments the layer address pointer by .
  • Shifts the stack by to the left. This moves an element from the stack overflow table into the last position on the stack top.

To keep the degree of the constraints low, a number of intermediate values are used. Specifically, the operation relies on all helper registers, and also uses the first elements of the stack at the next state for degree reduction purposes. Thus, once the operation has been executed, the top elements of the stack can be considered to be "garbage".

TODO: add detailed constraint descriptions. See discussion here.

The effect on the rest of the stack is:

  • Left shift starting from position .

RCOMBBASE

The RCOMBBASE operation performs a single step in the computation of the random linear combination defining the DEEP composition polynomial i.e., the input to the FRI protocol. More precisely, the sum in question is: where is the current query to the DEEP composition polynomial for which we are computing the above random linear combination. The RCOMBBASE instruction computes the numerators and and stores the values in two accumulators and , respectively. This instruction is specialized to main trace columns i.e. the values are base field elements. The instruction works in combination with the mem_stream instruction where it is called 8 times in a row for each call to mem_stream.

The stack for the operation is expected to be arranged as follows:

  • The first stack elements contain base field elements representing the values of for the current query and the current batch of column values of the main trace for query .
  • The next elements contain the current value of the accumulator as a quadratic extension field element.
  • The next elements contain the current value of the accumulator as a quadratic extension field element.
  • The next element contains the value of the memory pointer x_ptr to the next batch of column values for query .
  • The next element contains the value of the memory pointer z_ptr to the -th OOD evaluations at z and gz i.e. and .
  • The next element contains the value of the memory pointer a_ptr to the -th random value . The remaining elements of the word are expected to be empty.

The diagram below illustrates the stack transition for RCOMBBASE operation.

rcomb_base

After calling the mem_stream with x_ptr, the operation does the following:

  • Populates the helper registers with using the pointers z_ptr and a_ptr.
  • Updates the accumulators and
  • Increments the pointers z_ptr and a_ptr by .
  • The top base field elements are circularly shifted so that T_0 becomes the element at the top of the operand stack.

TODO: add detailed constraint descriptions. See discussion here.

The effect on the rest of the stack is:

  • No change.

The RCOMBBASE makes two memory access request. To simplify the description of these, we first define the following variables :

Using the above variables, we define the values representing the memory access request as follows: