Stack Manipulation

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

The PAD operation pushes a onto the stack. The diagram below illustrates this graphically.

Stack transition for this operation must satisfy the following constraints:

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

• Right shift starting from position .

DROP

The DROP operation removes an element from the top of the stack. The diagram below illustrates this graphically.

The DROP operation shifts the stack by element to the left, but does not impose any additional constraints. The degree of left shift constraints is .

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

• Left shift starting from position .

DUP(n)

The DUP(n) operations push a copy of the -th stack element onto the stack. Eg. DUP (same as DUP0) pushes a copy of the top stack element onto the stack. Similarly, DUP5 pushes a copy of the -th stack element onto the stack. This operation is valid for . The diagram below illustrates this graphically.

Stack transition for this operation must satisfy the following constraints:

where is the depth of the stack from where the element has been copied.

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

• Right shift starting from position .

SWAP

The SWAP operations swaps the top two elements of the stack. The diagram below illustrates this graphically.

Stack transition for this operation must satisfy the following constraints:

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

• No change starting from position .

SWAPW

The SWAPW operation swaps stack elements with elements . The diagram below illustrates this graphically.

Stack transition for this operation must satisfy the following constraints:

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

• No change starting from position .

SWAPW2

The SWAPW2 operation swaps stack elements with elements . The diagram below illustrates this graphically.

Stack transition for this operation must satisfy the following constraints:

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

• No change for elements .
• No change starting from position .

SWAPW3

The SWAPW3 operation swaps stack elements with elements . The diagram below illustrates this graphically.

Stack transition for this operation must satisfy the following constraints:

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

• No change for elements .
• No change starting from position .

SWAPDW

The SWAPDW operation swaps stack elements with elements . The diagram below illustrates this graphically.

Stack transition for this operation must satisfy the following constraints:

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

• No change starting from position .

MOVUP(n)

The MOVUP(n) operation moves the -th element of the stack to the top of the stack. For example, MOVUP2 moves element at depth to the top of the stack. All elements with depth less than are shifted to the right by one, while elements with depth greater than remain in place, and the depth of the stack does not change. This operation is valid for . The diagram below illustrates this graphically.

Stack transition for this operation must satisfy the following constraints:

where is the depth of the element which is moved moved to the top of the stack.

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

• Right shift for elements between and .
• No change starting from position .

MOVDN(n)

The MOVDN(n) operation moves the top element of the stack to the -th position. For example, MOVDN2 moves the top element of the stack to depth . All the elements with depth less than are shifted to the left by one, while elements with depth greater than remain in place, and the depth of the stack does not change. This operation is valid for . The diagram below illustrates this graphically.

Stack transition for this operation must satisfy the following constraints:

where is the depth to which the top stack element is moved.

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

• Left shift for elements between and .
• No change starting from position .

CSWAP

The CSWAP operation pops an element off the stack and if the element is , swaps the top two remaining elements. If the popped element is , the rest of the stack remains unchanged. The diagram below illustrates this graphically.

In the above:

Stack transition for this operation must satisfy the following constraints:

We also need to enforce that the value in is binary. This can be done with the following constraint:

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

• Left shift starting from position .

CSWAPW

The CSWAPW operation pops an element off the stack and if the element is , swaps elements with elements . If the popped element is , the rest of the stack remains unchanged. The diagram below illustrates this graphically.

In the above:

Stack transition for this operation must satisfy the following constraints:

We also need to enforce that the value in is binary. This can be done with the following constraint:

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

• Left shift starting from position .