Field Operations
In this section we describe the AIR constraints for Miden VM field operations (i.e., arithmetic operations over field elements).
ADD
Assume and are the elements at the top of the stack. The ADD
operation computes . The diagram below illustrates this graphically.
Stack transition for this operation must satisfy the following constraints:
The effect on the rest of the stack is:
- Left shift starting from position .
NEG
Assume is the element at the top of the stack. The NEG
operation computes . The diagram below illustrates this graphically.
Stack transition for this operation must satisfy the following constraints:
The effect on the rest of the stack is:
- No change starting from position .
MUL
Assume and are the elements at the top of the stack. The MUL
operation computes . The diagram below illustrates this graphically.
Stack transition for this operation must satisfy the following constraints:
The effect on the rest of the stack is:
- Left shift starting from position .
INV
Assume is the element at the top of the stack. The INV
operation computes . The diagram below illustrates this graphically.
Stack transition for this operation must satisfy the following constraints:
Note that the above constraint can be satisfied only if the value in .
The effect on the rest of the stack is:
- No change starting from position .
INCR
Assume is the element at the top of the stack. The INCR
operation computes . The diagram below illustrates this graphically.
Stack transition for this operation must satisfy the following constraints:
The effect on the rest of the stack is:
- No change starting from position .
NOT
Assume is a binary value at the top of the stack. The NOT
operation computes . The diagram below illustrates this graphically.
Stack transition for this operation must satisfy the following constraints:
The first constraint ensures that the value in is binary, and the second constraint ensures the correctness of the boolean NOT
operation.
The effect on the rest of the stack is:
- No change starting from position .
AND
Assume and are binary values at the top of the stack. The AND
operation computes . The diagram below illustrates this graphically.
Stack transition for this operation must satisfy the following constraints:
The first two constraints ensure that the value in and are binary, and the third constraint ensures the correctness of the boolean AND
operation.
The effect on the rest of the stack is:
- Left shift starting from position .
OR
Assume and are binary values at the top of the stack. The OR
operation computes The diagram below illustrates this graphically.
Stack transition for this operation must satisfy the following constraints:
The first two constraints ensure that the value in and are binary, and the third constraint ensures the correctness of the boolean OR
operation.
The effect on the rest of the stack is:
- Left shift starting from position .
EQ
Assume and are the elements at the top of the stack. The EQ
operation computes such that if , and otherwise. The diagram below illustrates this graphically.
Stack transition for this operation must satisfy the following constraints:
To satisfy the above constraints, the prover must populate the value of helper register as follows:
- If , set .
- Otherwise, set to any value (e.g., ).
The effect on the rest of the stack is:
- Left shift starting from position .
EQZ
Assume is the element at the top of the stack. The EQZ
operation computes such that if , and otherwise. The diagram below illustrates this graphically.
Stack transition for this operation must satisfy the following constraints:
To satisfy the above constraints, the prover must populate the value of helper register as follows:
- If , set .
- Otherwise, set to any value (e.g., ).
The effect on the rest of the stack is:
- No change starting from position .
EXPACC
The EXPACC
operation computes one round of the expression . It is expected that Expacc
is called at least num_exp_bits
times, where num_exp_bits
is the number of bits required to represent exp
.
It pops elements from the top of the stack, performs a single round of exponent aggregation, and pushes the resulting values onto the stack. The diagram below illustrates this graphically.
Expacc is based on the observation that the exponentiation of a number can be computed by repeatedly squaring the base and multiplying those powers of the base by the accumulator, for the powers of the base which correspond to the exponent's bits which are set to 1.
For example, take . Over the course of 3 iterations ( is in binary), the algorithm will compute , and (placed in base_acc
). Hence, we want to multiply base_acc
in acc
when and when , which occurs on the first and third iterations (corresponding to the bits in the binary representation of 5).
Stack transition for this operation must satisfy the following constraints:
bit'
should be a binary.
The base
in the next frame should be the square of the base
in the current frame.
The value val
in the helper register is computed correctly using the bit
and exp
in next and current frame respectively.
The acc
in the next frame is the product of val
and acc
in the current frame.
exp
in the next frame is half of exp
in the current frame (accounting for even/odd).
The effect on the rest of the stack is:
- No change starting from position .
EXT2MUL
The EXT2MUL
operation pops top values from the top of the stack, performs multiplication between the two extension field elements, and pushes the resulting values onto the stack. The diagram below illustrates this graphically.
Stack transition for this operation must satisfy the following constraints:
The first stack element should be unchanged in the next frame.
The second stack element should be unchanged in the next frame.
The third stack element should satisfy the following constraint.
The fourth stack element should satisfy the following constraint.
The effect on the rest of the stack is:
- No change starting from position .