Skip to content

Stack manipulation

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

PAD

The PAD operation pushes a \(0\) onto the stack. The diagram below illustrates this graphically.

pad

Stack transition for this operation must satisfy the following constraints:

\[ s_{0}' = 0 \text{ | degree} = 1 \]

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

  • Right shift starting from position \(0\).

DROP

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

drop

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

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

  • Left shift starting from position \(1\).

DUP(n)

The DUP(n) operations push a copy of the \(n\)-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 \(6\)-th stack element onto the stack. This operation is valid for \(n \in \{0, ..., 7, 9, 11, 13, 15\}\). The diagram below illustrates this graphically.

dupn

Stack transition for this operation must satisfy the following constraints:

\[ s_{0}' - s_{n} = 0 \text{ for } n \in \{0, ..., 7, 9, 11, 13, 15\} \text{ | degree} = 1 \]

where \(n\) 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 \(0\).

SWAP

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

swap

Stack transition for this operation must satisfy the following constraints:

\[ s_{0}' - s_{1} = 0 \text{ | degree} = 1 \]
\[ s_{1}' - s_{0} = 0 \text{ | degree} = 1 \]

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

  • No change starting from position \(2\).

SWAPW

The SWAPW operation swaps stack elements \(0, 1, 2, 3\) with elements \(4, 5, 6, 7\). The diagram below illustrates this graphically.

swapw

Stack transition for this operation must satisfy the following constraints:

\[ s_{i}' - s_{i+4} = 0 \text{ for } i \in \{0, 1, 2, 3\} \text{ | degree} = 1 \]
\[ s_{i + 4}' - s_i = 0 \text{ for } i \in \{0, 1, 2, 3\} \text{ | degree} = 1 \]

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

  • No change starting from position \(8\).

SWAPW2

The SWAPW2 operation swaps stack elements \(0, 1, 2, 3\) with elements \(8, 9, 10, 11\). The diagram below illustrates this graphically.

swapw2

Stack transition for this operation must satisfy the following constraints:

\[ s_i' - s_{i+8} = 0 \text{ for } i \in \{0, 1, 2, 3\} \text{ | degree} = 1 \]
\[ s_{i + 8}' - s_i = 0 \text{ for } i \in \{0, 1, 2, 3\} \text{ | degree} = 1 \]

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

  • No change for elements \(4, 5, 6, 7\).
  • No change starting from position \(12\).

SWAPW3

The SWAPW3 operation swaps stack elements \(0, 1, 2, 3\) with elements \(12, 13, 14, 15\). The diagram below illustrates this graphically.

swapw3

Stack transition for this operation must satisfy the following constraints:

\[ s_i' - s_{i+12} = 0 \text{ for } i \in \{0, 1, 2, 3\} \text{ | degree} = 1 \]
\[ s_{i+12}' - s_i = 0 \text{ for } i \in \{0, 1, 2, 3\} \text{ | degree} = 1 \]

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

  • No change for elements \(4, 5, 6, 7, 8, 9, 10, 11\).
  • No change starting from position \(16\).

SWAPDW

The SWAPDW operation swaps stack elements \([0, 8)\) with elements \([8, 16)\). The diagram below illustrates this graphically.

swapdw

Stack transition for this operation must satisfy the following constraints:

\[ s_i' - s_{i+8} = 0 \text{ for } i \in [0, 8) \text{ | degree} = 1 \]
\[ s_{i+8}' - s_i = 0 \text{ for } i \in [0, 8) \text{ | degree} = 1 \]

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

  • No change starting from position \(16\).

MOVUP(n)

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

movup

Stack transition for this operation must satisfy the following constraints:

\[ s_0' - s_n = 0 \text{ for } n \in [2, 9) \text{ | degree} = 1 \]

where \(n\) 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 \(0\) and \(n-1\).
  • No change starting from position \(n+1\).

MOVDN(n)

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

movdn

Stack transition for this operation must satisfy the following constraints:

\[ s_n' - s_0 = 0 \text{ for } n \in [2, 9) \text{ | degree} = 1 \]

where \(n\) 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 \(1\) and \(n\).
  • No change starting from position \(n+1\).

CSWAP

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

cswap

In the above:

\[ d = \begin{cases} a, & \text{if}\ c = 0 \\ b, & \text{if}\ c = 1\ \end{cases} e = \begin{cases} b, & \text{if}\ c = 0 \\ a, & \text{if}\ c = 1\ \end{cases} \]

Stack transition for this operation must satisfy the following constraints:

\[ s_0' - s_{0} \cdot s_{2} - (1-s_0) \cdot s_1 = 0 \text{ | degree} = 2 \]
\[ s_1' - s_0 \cdot s_{1} - (1-s_0) \cdot s_2 = 0 \text{ | degree} = 2 \]

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

\[ s_0^2 - s_0 = 0 \text{ | degree} = 2 \]

The effect of this operation on the rest of the stack is: * Left shift starting from position \(3\).

CSWAPW

The CSWAPW operation pops an element off the stack and if the element is \(1\), swaps elements \(1, 2, 3, 4\) with elements \(5, 6, 7, 8\). If the popped element is \(0\), the rest of the stack remains unchanged. The diagram below illustrates this graphically.

cswapw

In the above:

\[ D = \begin{cases} A, & \text{if}\ c = 0 \\ B, & \text{if}\ c = 1\ \end{cases} E = \begin{cases} B, & \text{if}\ c = 0 \\ A, & \text{if}\ c = 1\ \end{cases} \]

Stack transition for this operation must satisfy the following constraints:

\[ s_i' - s_0 \cdot s_{i+5} - (1-s_0) \cdot s_{i+1} = 0 \text{ for } i \in [0, 4) \text{ | degree} = 2 \]
\[ s_{i+4}' - s_0 \cdot s_{i+1} - (1-s_0) \cdot s_{i+5} = 0 \text{ for } i \in [0, 4) \text{ | degree} = 2 \]

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

\[ s_0^2 - s_0 = 0 \text{ | degree} = 2 \]

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

  • Left shift starting from position \(9\).

Last update: December 21, 2023
Authors: kmurphypolygon