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
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
In the above,
For the HPERM
operation, we define input and output values as follows:
In the above,
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
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.
In the above,
For the MPVERIFY
operation, we define input and output values as follows:
In the above,
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
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.
In the above,
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
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
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.
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
The effect on the rest of the stack is:
- Left shift starting from position
.