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.

add

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.

neg

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.

mul

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.

inv

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.

incr

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.

not

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.

and

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.

or

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.

eq

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.

eqz

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

Stack transition for this operation must satisfy the following constraints:

bit should be a binary.

The exp in the next frame should be the square of the exp 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.

b in the next frame is the right shift of b in the current frame.

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.

ext2mul

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 .