# Instruction-Specific Transition Constraints

## Instruction `pop`

+ `n`

This instruction is fully constrained by its instruction groups

## Instruction `push`

+ `a`

In addition to its instruction groups, this instruction has the following constraints.

### Description

- The instruction's argument
`a`

is moved onto the stack.

### Polynomials

`st0' - nia`

## Instruction `divine`

+ `n`

This instruction is fully constrained by its instruction groups

## Instruction `pick`

+ `i`

This instruction makes use of indicator polynomials. In addition to its instruction groups, this instruction has the following constraints.

### Description

For 0 ⩽ `i`

< 16:

- Stack element
`i`

is moved to the top. - For 0 ⩽
`j`

<`i`

: stack element`j`

is shifted down by 1. - For
`j`

>`i`

: stack element`j`

remains unchanged.

## Instruction `place`

+ `i`

This instruction makes use of indicator polynomials. In addition to its instruction groups, this instruction has the following constraints.

### Description

For 0 ⩽ `i`

< 16:

- Stack element 0 is moved to position
`i`

. - For 0 ⩽
`j`

<`i`

: stack element`j`

is shifted up by 1. - For
`j`

>`i`

: stack element`j`

remains unchanged.

## Instruction `dup`

+ `i`

This instruction makes use of indicator polynomials. In addition to its instruction groups, this instruction has the following constraints.

### Description

- If
`i`

is 0, then`st0`

is put on top of the stack and

if`i`

is 1, then`st1`

is put on top of the stack and

if`i`

is 2, then`st2`

is put on top of the stack and

if`i`

is 3, then`st3`

is put on top of the stack and

if`i`

is 4, then`st4`

is put on top of the stack and

if`i`

is 5, then`st5`

is put on top of the stack and

if`i`

is 6, then`st6`

is put on top of the stack and

if`i`

is 7, then`st7`

is put on top of the stack and

if`i`

is 8, then`st8`

is put on top of the stack and

if`i`

is 9, then`st9`

is put on top of the stack and

if`i`

is 10, then`st10`

is put on top of the stack and

if`i`

is 11, then`st11`

is put on top of the stack and

if`i`

is 12, then`st12`

is put on top of the stack and

if`i`

is 13, then`st13`

is put on top of the stack and

if`i`

is 14, then`st14`

is put on top of the stack and

if`i`

is 15, then`st15`

is put on top of the stack.

### Polynomials

`ind_0(hv3, hv2, hv1, hv0)·(st0' - st0)`

`+ ind_1(hv3, hv2, hv1, hv0)·(st0' - st1)`

`+ ind_2(hv3, hv2, hv1, hv0)·(st0' - st2)`

`+ ind_3(hv3, hv2, hv1, hv0)·(st0' - st3)`

`+ ind_4(hv3, hv2, hv1, hv0)·(st0' - st4)`

`+ ind_5(hv3, hv2, hv1, hv0)·(st0' - st5)`

`+ ind_6(hv3, hv2, hv1, hv0)·(st0' - st6)`

`+ ind_7(hv3, hv2, hv1, hv0)·(st0' - st7)`

`+ ind_8(hv3, hv2, hv1, hv0)·(st0' - st8)`

`+ ind_9(hv3, hv2, hv1, hv0)·(st0' - st9)`

`+ ind_10(hv3, hv2, hv1, hv0)·(st0' - st10)`

`+ ind_11(hv3, hv2, hv1, hv0)·(st0' - st11)`

`+ ind_12(hv3, hv2, hv1, hv0)·(st0' - st12)`

`+ ind_13(hv3, hv2, hv1, hv0)·(st0' - st13)`

`+ ind_14(hv3, hv2, hv1, hv0)·(st0' - st14)`

`+ ind_15(hv3, hv2, hv1, hv0)·(st0' - st15)`

## Instruction `swap`

+ `i`

### Description

For 0 ⩽ `i`

< 16:

- Stack element
`i`

is moved to the top. - The top stack element is moved to position
`i`

- For
`j`

≠`i`

: stack element`j`

remains unchanged.

## Instruction `nop`

This instruction is fully constrained by its instruction groups

## Instruction `skiz`

For the correct behavior of instruction `skiz`

, the instruction pointer `ip`

needs to increment by either 1, or 2, or 3.
The concrete value depends on the top of the stack `st0`

and the next instruction, held in `nia`

.

Helper variable `hv0`

helps with identifying whether `st0`

is 0.
To this end, it holds the inverse-or-zero of `st0`

, *i.e.*, is 0 if and only if `st0`

is 0, and is the inverse of `st0`

otherwise.

Efficient arithmetization of instruction `skiz`

makes use of one of the properties of opcodes.
Concretely, the least significant bit of an opcode is 1 if and only if the instruction takes an argument.
The arithmetization of `skiz`

can incorporate this simple flag by decomposing `nia`

into helper variable registers `hv`

,
similarly to how `ci`

is (always) deconstructed into instruction bit registers `ib`

.
Correct decomposition is guaranteed by employing a range check.

In addition to its instruction groups, this instruction has the following constraints.

### Description

- Helper variable
`hv1`

is the inverse of`st0`

or 0. - Helper variable
`hv1`

is the inverse of`st0`

or`st0`

is 0. - The next instruction
`nia`

is decomposed into helper variables`hv1`

through`hv5`

. - The indicator helper variable
`hv1`

is either 0 or 1. Here,`hv1 == 1`

means that`nia`

takes an argument. - The helper variable
`hv2`

is either 0 or 1 or 2 or 3. - The helper variable
`hv3`

is either 0 or 1 or 2 or 3. - The helper variable
`hv4`

is either 0 or 1 or 2 or 3. - The helper variable
`hv5`

is either 0 or 1 or 2 or 3. - If
`st0`

is non-zero, register`ip`

is incremented by 1. If`st0`

is 0 and`nia`

takes no argument, register`ip`

is incremented by 2. If`st0`

is 0 and`nia`

takes an argument, register`ip`

is incremented by 3.

Written as Disjunctive Normal Form, the last constraint can be expressed as:

- (Register
`st0`

is 0 or`ip`

is incremented by 1), and (`st0`

has a multiplicative inverse or`hv1`

is 1 or`ip`

is incremented by 2), and (`st0`

has a multiplicative inverse or`hv1`

is 0 or`ip`

is incremented by 3).

Since the three cases are mutually exclusive, the three respective polynomials can be summed up into one.

### Polynomials

`(st0·hv0 - 1)·hv0`

`(st0·hv0 - 1)·st0`

`nia - hv1 - 2·hv2 - 8·hv3 - 32·hv4 - 128·hv5`

`hv1·(hv1 - 1)`

`hv2·(hv2 - 1)·(hv2 - 2)·(hv2 - 3)`

`hv3·(hv3 - 1)·(hv3 - 2)·(hv3 - 3)`

`hv4·(hv4 - 1)·(hv4 - 2)·(hv4 - 3)`

`hv5·(hv5 - 1)·(hv5 - 2)·(hv5 - 3)`

`(ip' - (ip + 1)·st0)`

`+ ((ip' - (ip + 2))·(st0·hv0 - 1)·(hv1 - 1))`

`+ ((ip' - (ip + 3))·(st0·hv0 - 1)·hv1)`

### Helper variable definitions for `skiz`

`hv0 = inverse(st0)`

(if`st0 ≠ 0`

)`hv1 = nia mod 2`

`hv2 = (nia >> 1) mod 4`

`hv3 = (nia >> 3) mod 4`

`hv4 = (nia >> 5) mod 4`

`hv5 = nia >> 7`

## Instruction `call`

+ `d`

In addition to its instruction groups, this instruction has the following constraints.

### Description

- The jump stack pointer
`jsp`

is incremented by 1. - The jump's origin
`jso`

is set to the current instruction pointer`ip`

plus 2. - The jump's destination
`jsd`

is set to the instruction's argument`d`

. - The instruction pointer
`ip`

is set to the instruction's argument`d`

.

### Polynomials

`jsp' - (jsp + 1)`

`jso' - (ip + 2)`

`jsd' - nia`

`ip' - nia`

## Instruction `return`

In addition to its instruction groups, this instruction has the following constraints.

### Description

- The jump stack pointer
`jsp`

is decremented by 1. - The instruction pointer
`ip`

is set to the last call's origin`jso`

.

### Polynomials

`jsp' - (jsp - 1)`

`ip' - jso`

## Instruction `recurse`

In addition to its instruction groups, this instruction has the following constraints.

### Description

- The jump stack pointer
`jsp`

does not change. - The last jump's origin
`jso`

does not change. - The last jump's destination
`jsd`

does not change. - The instruction pointer
`ip`

is set to the last jump's destination`jsd`

.

### Polynomials

`jsp' - jsp`

`jso' - jso`

`jsd' - jsd`

`ip' - jsd`

## Instruction `recurse_or_return`

In addition to its instruction groups, this instruction has the following constraints.

### Description

- If
`ST5`

equals`ST6`

, then`ip`

in the next row equals`jso`

in the current row. - If
`ST5`

equals`ST6`

, then`jsp`

decrements by one. - If
`ST5`

equals`ST6`

, then`hv0`

in the current row is 0. - If
`ST5`

is unequal to`ST6`

, then`hv0`

in the current row is the inverse of`(ST6 - ST5)`

. - If
`ST5`

is unequal to`ST6`

, then`ip`

in the next row is equal to`jsd`

in the current row. - If
`ST5`

is unequal to`ST6`

, then`jsp`

remains unchanged. - If
`ST5`

is unequal to`ST6`

, then`jso`

remains unchanged. - If
`ST5`

is unequal to`ST6`

, then`jsd`

remains unchanged.

### Helper variable definitions for `recurse_or_return`

To help arithmetizing the equality check between `ST5`

and `ST6`

, helper variable `hv0`

is the inverse-or-zero of `(ST6 - ST5)`

.

## Instruction `assert`

In addition to its instruction groups, this instruction has the following constraints.

### Description

- The current top of the stack
`st0`

is 1.

### Polynomials

`st0 - 1`

## Instruction `halt`

In addition to its instruction groups, this instruction has the following constraints.

### Description

- The instruction executed in the following step is instruction
`halt`

.

### Polynomials

`ci' - ci`

## Instruction `read_mem`

+ `n`

In addition to its instruction groups, this instruction has the following constraints.

### Description

- The RAM pointer
`st0`

is decremented by`n`

. - If
`n`

is 1, then`st1`

is moved into`st2`

else if`n`

is 2, then`st1`

is moved into`st3`

else if`n`

is 3, then`st1`

is moved into`st4`

else if`n`

is 4, then`st1`

is moved into`st5`

else if`n`

is 5, then`st1`

is moved into`st6`

. - If
`n`

is 1, then`st2`

is moved into`st3`

else if`n`

is 2, then`st2`

is moved into`st4`

else if`n`

is 3, then`st2`

is moved into`st5`

else if`n`

is 4, then`st2`

is moved into`st6`

else if`n`

is 5, then`st2`

is moved into`st7`

. - If
`n`

is 1, then`st3`

is moved into`st4`

else if`n`

is 2, then`st3`

is moved into`st5`

else if`n`

is 3, then`st3`

is moved into`st6`

else if`n`

is 4, then`st3`

is moved into`st7`

else if`n`

is 5, then`st3`

is moved into`st8`

. - If
`n`

is 1, then`st4`

is moved into`st5`

else if`n`

is 2, then`st4`

is moved into`st6`

else if`n`

is 3, then`st4`

is moved into`st7`

else if`n`

is 4, then`st4`

is moved into`st8`

else if`n`

is 5, then`st4`

is moved into`st9`

. - If
`n`

is 1, then`st5`

is moved into`st6`

else if`n`

is 2, then`st5`

is moved into`st7`

else if`n`

is 3, then`st5`

is moved into`st8`

else if`n`

is 4, then`st5`

is moved into`st9`

else if`n`

is 5, then`st5`

is moved into`st10`

. - If
`n`

is 1, then`st6`

is moved into`st7`

else if`n`

is 2, then`st6`

is moved into`st8`

else if`n`

is 3, then`st6`

is moved into`st9`

else if`n`

is 4, then`st6`

is moved into`st10`

else if`n`

is 5, then`st6`

is moved into`st11`

. - If
`n`

is 1, then`st7`

is moved into`st8`

else if`n`

is 2, then`st7`

is moved into`st9`

else if`n`

is 3, then`st7`

is moved into`st10`

else if`n`

is 4, then`st7`

is moved into`st11`

else if`n`

is 5, then`st7`

is moved into`st12`

. - If
`n`

is 1, then`st8`

is moved into`st9`

else if`n`

is 2, then`st8`

is moved into`st10`

else if`n`

is 3, then`st8`

is moved into`st11`

else if`n`

is 4, then`st8`

is moved into`st12`

else if`n`

is 5, then`st8`

is moved into`st13`

. - If
`n`

is 1, then`st9`

is moved into`st10`

else if`n`

is 2, then`st9`

is moved into`st11`

else if`n`

is 3, then`st9`

is moved into`st12`

else if`n`

is 4, then`st9`

is moved into`st13`

else if`n`

is 5, then`st9`

is moved into`st14`

. - If
`n`

is 1, then`st10`

is moved into`st11`

else if`n`

is 2, then`st10`

is moved into`st12`

else if`n`

is 3, then`st10`

is moved into`st13`

else if`n`

is 4, then`st10`

is moved into`st14`

else if`n`

is 5, then`st10`

is moved into`st15`

. - If
`n`

is 1, then`st11`

is moved into`st12`

else if`n`

is 2, then`st11`

is moved into`st13`

else if`n`

is 3, then`st11`

is moved into`st14`

else if`n`

is 4, then`st11`

is moved into`st15`

else if`n`

is 5, then the op stack pointer grows by 5. - If
`n`

is 1, then`st12`

is moved into`st13`

else if`n`

is 2, then`st12`

is moved into`st14`

else if`n`

is 3, then`st12`

is moved into`st15`

else if`n`

is 4, then the op stack pointer grows by 4

else if`n`

is 5, then with the Op Stack Table accumulates`st11`

through`st15`

. - If
`n`

is 1, then`st13`

is moved into`st14`

else if`n`

is 2, then`st13`

is moved into`st15`

else if`n`

is 3, then the op stack pointer grows by 3

else if`n`

is 4, then the running product with the Op Stack Table accumulates`st12`

through`st15`

else if`n`

is 5, then the running product with the RAM Table accumulates next row's`st1`

through`st5`

. - If
`n`

is 1, then`st14`

is moved into`st15`

else if`n`

is 2, then the op stack pointer grows by 2

else if`n`

is 3, then the running product with the Op Stack Table accumulates`st13`

through`st15`

else if`n`

is 4, then the running product with the RAM Table accumulates next row's`st1`

through`st4`

- If
`n`

is 1, then the op stack pointer grows by 1

else if`n`

is 2, then the running product with the Op Stack Table accumulates`st14`

and`st15`

else if`n`

is 3, then the running product with the RAM Table accumulates next row's`st1`

through`st3`

. - If
`n`

is 1, then the running product with the Op Stack Table accumulates`st15`

else if`n`

is 2, then the running product with the RAM Table accumulates next row's`st1`

and`st2`

. - If
`n`

is 1, then the running product with the RAM Table accumulates next row's`st1`

.

## Instruction `write_mem`

+ `n`

In addition to its instruction groups, this instruction has the following constraints.

### Description

- The RAM pointer
`st0`

is incremented by`n`

. - If
`n`

is 1, then`st2`

is moved into`st1`

else if`n`

is 2, then`st3`

is moved into`st1`

else if`n`

is 3, then`st4`

is moved into`st1`

else if`n`

is 4, then`st5`

is moved into`st1`

else if`n`

is 5, then`st6`

is moved into`st1`

. - If
`n`

is 1, then`st3`

is moved into`st2`

else if`n`

is 2, then`st4`

is moved into`st2`

else if`n`

is 3, then`st5`

is moved into`st2`

else if`n`

is 4, then`st6`

is moved into`st2`

else if`n`

is 5, then`st7`

is moved into`st2`

. - If
`n`

is 1, then`st4`

is moved into`st3`

else if`n`

is 2, then`st5`

is moved into`st3`

else if`n`

is 3, then`st6`

is moved into`st3`

else if`n`

is 4, then`st7`

is moved into`st3`

else if`n`

is 5, then`st8`

is moved into`st3`

. - If
`n`

is 1, then`st5`

is moved into`st4`

else if`n`

is 2, then`st6`

is moved into`st4`

else if`n`

is 3, then`st7`

is moved into`st4`

else if`n`

is 4, then`st8`

is moved into`st4`

else if`n`

is 5, then`st9`

is moved into`st4`

. - If
`n`

is 1, then`st6`

is moved into`st5`

else if`n`

is 2, then`st7`

is moved into`st5`

else if`n`

is 3, then`st8`

is moved into`st5`

else if`n`

is 4, then`st9`

is moved into`st5`

else if`n`

is 5, then`st10`

is moved into`st5`

. - If
`n`

is 1, then`st7`

is moved into`st6`

else if`n`

is 2, then`st8`

is moved into`st6`

else if`n`

is 3, then`st9`

is moved into`st6`

else if`n`

is 4, then`st10`

is moved into`st6`

else if`n`

is 5, then`st11`

is moved into`st6`

. - If
`n`

is 1, then`st8`

is moved into`st7`

else if`n`

is 2, then`st9`

is moved into`st7`

else if`n`

is 3, then`st10`

is moved into`st7`

else if`n`

is 4, then`st11`

is moved into`st7`

else if`n`

is 5, then`st12`

is moved into`st7`

. - If
`n`

is 1, then`st9`

is moved into`st8`

else if`n`

is 2, then`st10`

is moved into`st8`

else if`n`

is 3, then`st11`

is moved into`st8`

else if`n`

is 4, then`st12`

is moved into`st8`

else if`n`

is 5, then`st13`

is moved into`st8`

. - If
`n`

is 1, then`st10`

is moved into`st9`

else if`n`

is 2, then`st11`

is moved into`st9`

else if`n`

is 3, then`st12`

is moved into`st9`

else if`n`

is 4, then`st13`

is moved into`st9`

else if`n`

is 5, then`st14`

is moved into`st9`

. - If
`n`

is 1, then`st11`

is moved into`st10`

else if`n`

is 2, then`st12`

is moved into`st10`

else if`n`

is 3, then`st13`

is moved into`st10`

else if`n`

is 4, then`st14`

is moved into`st10`

else if`n`

is 5, then`st15`

is moved into`st10`

. - If
`n`

is 1, then`st12`

is moved into`st11`

else if`n`

is 2, then`st13`

is moved into`st11`

else if`n`

is 3, then`st14`

is moved into`st11`

else if`n`

is 4, then`st15`

is moved into`st11`

else if`n`

is 5, then the op stack pointer shrinks by 5. - If
`n`

is 1, then`st13`

is moved into`st12`

else if`n`

is 2, then`st14`

is moved into`st12`

else if`n`

is 3, then`st15`

is moved into`st12`

else if`n`

is 4, then the op stack pointer shrinks by 4

else if`n`

is 5, then the running product with the Op Stack Table accumulates next row's`st11`

through`st15`

. - If
`n`

is 1, then`st14`

is moved into`st13`

else if`n`

is 2, then`st15`

is moved into`st13`

else if`n`

is 3, then the op stack pointer shrinks by 3

else if`n`

is 4, then the running product with the Op Stack Table accumulates next row's`st12`

through`st15`

else if`n`

is 5, then the running product with the RAM Table accumulates`st1`

through`st5`

. - If
`n`

is 1, then`st15`

is moved into`st14`

else if`n`

is 2, then the op stack pointer shrinks by 2

else if`n`

is 3, then the running product with the Op Stack Table accumulates next row's`st13`

through`st15`

else if`n`

is 4, then the running product with the RAM Table accumulates`st1`

through`st4`

. - If
`n`

is 1, then the op stack pointer shrinks by 1

else if`n`

is 2, then the running product with the Op Stack Table accumulates next row's`st14`

and`st15`

else if`n`

is 3, then the running product with the RAM Table accumulates`st1`

through`st2`

. - If
`n`

is 1, then the running product with the Op Stack Table accumulates next row's`st15`

else if`n`

is 2, then the running product with the RAM Table accumulates`st1`

and`st1`

. - If
`n`

is 1, then the running product with the RAM Table accumulates`st1`

.

## Instruction `hash`

In addition to its instruction groups, this instruction has the following constraints.

### Description

`st10`

is moved into`st5`

.`st11`

is moved into`st6`

.`st12`

is moved into`st7`

.`st13`

is moved into`st8`

.`st14`

is moved into`st9`

.`st15`

is moved into`st10`

.- The op stack pointer shrinks by 5.
- The running product with the Op Stack Table accumulates next row's
`st11`

through`st15`

.

### Polynomials

`st5' - st10`

`st6' - st11`

`st7' - st12`

`st8' - st13`

`st9' - st14`

`st10' - st15`

`op_stack_pointer' - op_stack_pointer + 5`

`RunningProductOpStackTable' - RunningProductOpStackTable·(🪤 - 🍋·clk - 🍊 - 🍉·op_stack_pointer' - 🫒·st15')`

`·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 1) - 🫒·st14')`

`·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 2) - 🫒·st13')`

`·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 3) - 🫒·st12')`

`·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 4) - 🫒·st11')`

## Instruction `assert_vector`

In addition to its instruction groups, this instruction has the following constraints.

### Description

`st0`

is equal to`st5`

.`st1`

is equal to`st6`

.`st2`

is equal to`st7`

.`st3`

is equal to`st8`

.`st4`

is equal to`st9`

.`st10`

is moved into`st5`

.`st11`

is moved into`st6`

.`st12`

is moved into`st7`

.`st13`

is moved into`st8`

.`st14`

is moved into`st9`

.`st15`

is moved into`st10`

.- The op stack pointer shrinks by 5.
- The running product with the Op Stack Table accumulates next row's
`st11`

through`st15`

.

### Polynomials

`st5 - st0`

`st6 - st1`

`st7 - st2`

`st8 - st3`

`st9 - st4`

`st5' - st10`

`st6' - st11`

`st7' - st12`

`st8' - st13`

`st9' - st14`

`st10' - st15`

`op_stack_pointer' - op_stack_pointer + 5`

`RunningProductOpStackTable' - RunningProductOpStackTable·(🪤 - 🍋·clk - 🍊 - 🍉·op_stack_pointer' - 🫒·st15')`

`·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 1) - 🫒·st14')`

`·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 2) - 🫒·st13')`

`·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 3) - 🫒·st12')`

`·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 4) - 🫒·st11')`

## Instruction `sponge_init`

This instruction is fully constrained by its instruction groups Beyond that, correct transition is guaranteed by the Hash Table.

## Instruction `sponge_absorb`

In addition to its instruction groups, this instruction has the following constraints. Beyond that, correct transition is guaranteed by the Hash Table.

### Description

`st10`

is moved into`st0`

.`st11`

is moved into`st1`

.`st12`

is moved into`st2`

.`st13`

is moved into`st3`

.`st14`

is moved into`st4`

.`st15`

is moved into`st5`

.- The op stack pointer shrinks by 10.
- The running product with the Op Stack Table accumulates next row's
`st6`

through`st15`

.

### Polynomials

`st0' - st10`

`st1' - st11`

`st2' - st12`

`st3' - st13`

`st4' - st14`

`st5' - st15`

`op_stack_pointer' - op_stack_pointer + 10`

`RunningProductOpStackTable' - RunningProductOpStackTable·(🪤 - 🍋·clk - 🍊 - 🍉·op_stack_pointer' - 🫒·st15')`

`·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 1) - 🫒·st14')`

`·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 2) - 🫒·st13')`

`·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 3) - 🫒·st12')`

`·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 4) - 🫒·st11')`

`·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 5) - 🫒·st10')`

`·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 6) - 🫒·st9')`

`·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 7) - 🫒·st8')`

`·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 8) - 🫒·st7')`

`·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 9) - 🫒·st6')`

## Instruction `sponge_absorb_mem`

In addition to its instruction groups, this instruction has the following constraints. Beyond that, correct transition is guaranteed by the Hash Table and the RAM Table.

### Description

`st0`

is incremented by 10.

## Instruction `sponge_squeeze`

In addition to its instruction groups, this instruction has the following constraints. Beyond that, correct transition is guaranteed by the Hash Table.

### Description

`st0`

is moved into`st10`

.`st1`

is moved into`st11`

.`st2`

is moved into`st12`

.`st3`

is moved into`st13`

.`st4`

is moved into`st14`

.`st5`

is moved into`st15`

.- The op stack pointer grows by 10.
- The running product with the Op Stack Table accumulates
`st6`

through`st15`

.

### Polynomials

`st10' - st0`

`st11' - st1`

`st12' - st2`

`st13' - st3`

`st14' - st4`

`st15' - st5`

`op_stack_pointer' - op_stack_pointer - 10`

`RunningProductOpStackTable' - RunningProductOpStackTable·(🪤 - 🍋·clk - 🍉·op_stack_pointer - 🫒·st15)`

`·(🪤 - 🍋·clk - 🍉·(op_stack_pointer + 1) - 🫒·st14)`

`·(🪤 - 🍋·clk - 🍉·(op_stack_pointer + 2) - 🫒·st13)`

`·(🪤 - 🍋·clk - 🍉·(op_stack_pointer + 3) - 🫒·st12)`

`·(🪤 - 🍋·clk - 🍉·(op_stack_pointer + 4) - 🫒·st11)`

`·(🪤 - 🍋·clk - 🍉·(op_stack_pointer + 5) - 🫒·st10)`

`·(🪤 - 🍋·clk - 🍉·(op_stack_pointer + 6) - 🫒·st9)`

`·(🪤 - 🍋·clk - 🍉·(op_stack_pointer + 7) - 🫒·st8)`

`·(🪤 - 🍋·clk - 🍉·(op_stack_pointer + 8) - 🫒·st7)`

`·(🪤 - 🍋·clk - 🍉·(op_stack_pointer + 9) - 🫒·st6)`

## Instruction `add`

In addition to its instruction groups, this instruction has the following constraints.

### Description

- The sum of the top two stack elements is moved into the top of the stack.

### Polynomials

`st0' - (st0 + st1)`

## Instruction `mul`

In addition to its instruction groups, this instruction has the following constraints.

### Description

- The product of the top two stack elements is moved into the top of the stack.

### Polynomials

`st0' - st0·st1`

## Instruction `invert`

In addition to its instruction groups, this instruction has the following constraints.

### Description

- The top of the stack's inverse is moved into the top of the stack.

### Polynomials

`st0'·st0 - 1`

## Instruction `eq`

In addition to its instruction groups, this instruction has the following constraints.

### Description

- Helper variable
`hv0`

is the inverse of the difference of the stack's two top-most elements or 0. - Helper variable
`hv0`

is the inverse of the difference of the stack's two top-most elements or the difference is 0. - The new top of the stack is 1 if the difference between the stack's two top-most elements is not invertible, 0 otherwise.

### Polynomials

`hv0·(hv0·(st1 - st0) - 1)`

`(st1 - st0)·(hv0·(st1 - st0) - 1)`

`st0' - (1 - hv0·(st1 - st0))`

### Helper variable definitions for `eq`

`hv0 = inverse(rhs - lhs)`

if`rhs ≠ lhs`

.`hv0 = 0`

if`rhs = lhs`

.

## Instruction `split`

In addition to its instruction groups, this instruction has the following constraints. Part of the correct transition, namely the range check on the instruction's result, is guaranteed by the U32 Table.

### Description

- The top of the stack is decomposed as 32-bit chunks into the stack's top-most two elements.
- Helper variable
`hv0`

holds the inverse of $2_{32}−1$ subtracted from the high 32 bits or the low 32 bits are 0.

### Polynomials

`st0 - (2^32·st1' + st0')`

`st0'·(hv0·(st1' - (2^32 - 1)) - 1)`

### Helper variable definitions for `split`

Given the high 32 bits of `st0`

as `hi = st0 >> 32`

and the low 32 bits of `st0`

as `lo = st0 & 0xffff_ffff`

,

`hv0 = (hi - (2^32 - 1))`

if`lo ≠ 0`

.`hv0 = 0`

if`lo = 0`

.

## Instruction `lt`

This instruction is fully constrained by its instruction groups Beyond that, correct transition is guaranteed by the U32 Table.

## Instruction `and`

This instruction is fully constrained by its instruction groups Beyond that, correct transition is guaranteed by the U32 Table.

## Instruction `xor`

This instruction is fully constrained by its instruction groups Beyond that, correct transition is guaranteed by the U32 Table.

## Instruction `log2floor`

## Instruction `pow`

## Instruction `div_mod`

Recall that instruction `div_mod`

takes stack `_ d n`

and computes `_ q r`

where `n`

is the numerator, `d`

is the denominator, `r`

is the remainder, and `q`

is the quotient.
The following two properties are guaranteed by the U32 Table:

- The remainder
`r`

is smaller than the denominator`d`

, and - all four of
`n`

,`d`

,`q`

, and`r`

are u32s.

In addition to its instruction groups, this instruction has the following constraints.

### Description

- Numerator is quotient times denominator plus remainder:
`n == q·d + r`

.

### Polynomials

`st0 - st1·st1' - st0'`

`st2' - st2`

## Instruction `pop_count`

## Instruction `xx_add`

In addition to its instruction groups, this instruction has the following constraints.

### Description

- The result of adding
`st0`

to`st3`

is moved into`st0`

. - The result of adding
`st1`

to`st4`

is moved into`st1`

. - The result of adding
`st2`

to`st5`

is moved into`st2`

. `st6`

is moved into`st3`

.`st7`

is moved into`st4`

.`st8`

is moved into`st5`

.`st9`

is moved into`st6`

.`st10`

is moved into`st7`

.`st11`

is moved into`st8`

.`st12`

is moved into`st9`

.`st13`

is moved into`st10`

.`st14`

is moved into`st11`

.`st15`

is moved into`st12`

.- The op stack pointer shrinks by 3.
- The running product with the Op Stack Table accumulates next row's
`st13`

through`st15`

.

### Polynomials

`st0' - (st0 + st3)`

`st1' - (st1 + st4)`

`st2' - (st2 + st5)`

`st3' - st6`

`st4' - st7`

`st5' - st8`

`st6' - st9`

`st7' - st10`

`st8' - st11`

`st9' - st12`

`st10' - st13`

`st11' - st14`

`st12' - st15`

`op_stack_pointer' - op_stack_pointer + 3`

`·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 1) - 🫒·st14')`

`·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 2) - 🫒·st13')`

## Instruction `xx_mul`

In addition to its instruction groups, this instruction has the following constraints.

### Description

- The coefficient of x^0 of multiplying the two X-Field elements on the stack is moved into
`st0`

. - The coefficient of x^1 of multiplying the two X-Field elements on the stack is moved into
`st1`

. - The coefficient of x^2 of multiplying the two X-Field elements on the stack is moved into
`st2`

. `st6`

is moved into`st3`

.`st7`

is moved into`st4`

.`st8`

is moved into`st5`

.`st9`

is moved into`st6`

.`st10`

is moved into`st7`

.`st11`

is moved into`st8`

.`st12`

is moved into`st9`

.`st13`

is moved into`st10`

.`st14`

is moved into`st11`

.`st15`

is moved into`st12`

.- The op stack pointer shrinks by 3.
- The running product with the Op Stack Table accumulates next row's
`st13`

through`st15`

.

### Polynomials

`st0' - (st0·st3 - st2·st4 - st1·st5)`

`st1' - (st1·st3 + st0·st4 - st2·st5 + st2·st4 + st1·st5)`

`st2' - (st2·st3 + st1·st4 + st0·st5 + st2·st5)`

`st3' - st6`

`st4' - st7`

`st5' - st8`

`st6' - st9`

`st7' - st10`

`st8' - st11`

`st9' - st12`

`st10' - st13`

`st11' - st14`

`st12' - st15`

`op_stack_pointer' - op_stack_pointer + 3`

`·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 1) - 🫒·st14')`

`·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 2) - 🫒·st13')`

## Instruction `x_invert`

In addition to its instruction groups, this instruction has the following constraints.

### Description

- The coefficient of x^0 of multiplying X-Field element on top of the current stack and on top of the next stack is 1.
- The coefficient of x^1 of multiplying X-Field element on top of the current stack and on top of the next stack is 0.
- The coefficient of x^2 of multiplying X-Field element on top of the current stack and on top of the next stack is 0.

### Polynomials

`st0·st0' - st2·st1' - st1·st2' - 1`

`st1·st0' + st0·st1' - st2·st2' + st2·st1' + st1·st2'`

`st2·st0' + st1·st1' + st0·st2' + st2·st2'`

## Instruction `xb_mul`

In addition to its instruction groups, this instruction has the following constraints.

### Description

- The result of multiplying the top of the stack with the X-Field element's coefficient for x^0 is moved into
`st0`

. - The result of multiplying the top of the stack with the X-Field element's coefficient for x^1 is moved into
`st1`

. - The result of multiplying the top of the stack with the X-Field element's coefficient for x^2 is moved into
`st2`

. `st4`

is moved into`st3`

.`st5`

is moved into`st4`

.`st6`

is moved into`st5`

.`st7`

is moved into`st6`

.`st8`

is moved into`st7`

.`st9`

is moved into`st8`

.`st10`

is moved into`st9`

.`st11`

is moved into`st10`

.`st12`

is moved into`st11`

.`st13`

is moved into`st12`

.`st14`

is moved into`st13`

.`st15`

is moved into`st14`

.- The op stack pointer shrinks by 3.
- The running product with the Op Stack Table accumulates next row's
`st15`

.

### Polynomials

`st0' - st0·st1`

`st1' - st0·st2`

`st2' - st0·st3`

`st3' - st4`

`st4' - st5`

`st5' - stt`

`st6' - st7`

`st7' - st8`

`st8' - st9`

`st9' - st10`

`st10' - st11`

`st11' - st12`

`st12' - st13`

`st13' - st14`

`st14' - st15`

`op_stack_pointer' - op_stack_pointer + 1`

## Instruction `read_io`

+ `n`

In addition to its instruction groups, this instruction has the following constraints.

### Description

- If
`n`

is 1, the running evaluation for standard input accumulates next row's`st0`

else if`n`

is 2, the running evaluation for standard input accumulates next row's`st0`

and`st1`

else if`n`

is 3, the running evaluation for standard input accumulates next row's`st0`

through`st2`

else if`n`

is 4, the running evaluation for standard input accumulates next row's`st0`

through`st3`

else if`n`

is 5, the running evaluation for standard input accumulates next row's`st0`

through`st4`

.

### Polynomials

`ind_1(hv3, hv2, hv1, hv0)·(RunningEvaluationStandardInput' - 🛏·RunningEvaluationStandardInput - st0')`

`+ ind_2(hv3, hv2, hv1, hv0)·(RunningEvaluationStandardInput' - 🛏·(🛏·RunningEvaluationStandardInput - st0') - st1')`

`+ ind_3(hv3, hv2, hv1, hv0)·(RunningEvaluationStandardInput' - 🛏·(🛏·(🛏·RunningEvaluationStandardInput - st0') - st1') - st2')`

`+ ind_4(hv3, hv2, hv1, hv0)·(RunningEvaluationStandardInput' - 🛏·(🛏·(🛏·(🛏·RunningEvaluationStandardInput - st0') - st1') - st2') - st3')`

`+ ind_5(hv3, hv2, hv1, hv0)·(RunningEvaluationStandardInput' - 🛏·(🛏·(🛏·(🛏·(🛏·RunningEvaluationStandardInput - st0') - st1') - st2') - st3') - st4')`

## Instruction `write_io`

+ `n`

In addition to its instruction groups, this instruction has the following constraints.

### Description

- If
`n`

is 1, the running evaluation for standard output accumulates`st0`

else if`n`

is 2, the running evaluation for standard output accumulates`st0`

and`st1`

else if`n`

is 3, the running evaluation for standard output accumulates`st0`

through`st2`

else if`n`

is 4, the running evaluation for standard output accumulates`st0`

through`st3`

else if`n`

is 5, the running evaluation for standard output accumulates`st0`

through`st4`

.

### Polynomials

`ind_1(hv3, hv2, hv1, hv0)·(RunningEvaluationStandardOutput' - 🧯·RunningEvaluationStandardOutput - st0)`

`+ ind_2(hv3, hv2, hv1, hv0)·(RunningEvaluationStandardOutput' - 🧯·(🧯·RunningEvaluationStandardOutput - st0) - st1)`

`+ ind_3(hv3, hv2, hv1, hv0)·(RunningEvaluationStandardOutput' - 🧯·(🧯·(🧯·RunningEvaluationStandardOutput - st0) - st1) - st2)`

`+ ind_4(hv3, hv2, hv1, hv0)·(RunningEvaluationStandardOutput' - 🧯·(🧯·(🧯·(🧯·RunningEvaluationStandardOutput - st0) - st1) - st2) - st3)`

`+ ind_5(hv3, hv2, hv1, hv0)·(RunningEvaluationStandardOutput' - 🧯·(🧯·(🧯·(🧯·(🧯·RunningEvaluationStandardOutput - st0) - st1) - st2) - st3) - st4)`

## Instruction `merkle_step`

Recall that in a Merkle tree, the indices of left (respectively right) leaves have 0 (respectively 1) as their least significant bit. This motivates the use of a helper variable to hold that least significant bit.

In addition to its instruction groups, this instruction has the following constraints. The two Evaluation Arguments also used for instruction hash guarantee correct transition of the top of the stack.

### Description

- Helper variable
`hv5`

is either 0 or 1. `st5`

is shifted by 1 bit to the right. In other words, twice`st5`

in the next row plus`hv5`

equals`st5`

in the current row.

### Helper variable definitions for `merkle_step`

`hv0`

through`hv4`

hold the sibling digest of the node indicated by`st5`

, as read from the interface for non-deterministic input.`hv5`

holds the result of`st5 % 2`

, the Merkle tree node index's least significant bit, indicating whether it is a left or right node.

## Instruction `merkle_step_mem`

In addition to its instruction groups, this instruction has the following constraints.
The two Evaluation Arguments also used for instruction hash guarantee correct transition of the top of the stack.
See also `merkle_step`

.

### Description

- Stack element
`st6`

does not change. - Stack element
`st7`

is incremented by 5. - Helper variable
`hv5`

is either 0 or 1. `st5`

is shifted by 1 bit to the right. In other words, twice`st5`

in the next row plus`hv5`

equals`st5`

in the current row.- The running product with the RAM Table accumulates
`hv0`

through`hv4`

using the (appropriately adjusted) RAM pointer held in`st7`

.

### Helper variable definitions for `merkle_step_mem`

`hv0`

through`hv4`

hold the sibling digest of the node indicated by`st5`

, as read from RAM at the address held in`st7`

.`hv5`

holds the result of`st5 % 2`

, the Merkle tree node index's least significant bit, indicating whether it is a left or right node.

## Instruction `xx_dot_step`

In addition to its instruction groups, this instruction has the following constraints.

### Description

- Store
`(RAM[st0], RAM[st0+1], RAM[st0+2])`

in`(hv0, hv1, hv2)`

. - Store
`(RAM[st1], RAM[st1+1], RAM[st1+2])`

in`(hv3, hv4, hv5)`

. - Add
`(hv0 + hv1·x + hv2·x²) · (hv3 + hv4·x + hv5·x²)`

into`(st2, st3, st4)`

- Increase the pointers:
`st0`

and`st1`

by 3 each.

## Instruction `xb_dot_step`

In addition to its instruction groups, this instruction has the following constraints.

### Description

- Store
`RAM[st0]`

in`hv0`

. - Store
`(RAM[st1], RAM[st1+1], RAM[st1+2])`

in`(hv1, hv2, hv3)`

. - Add
`hv0 · (hv1 + hv2·x + hv3·x²)`

into`(st1, st2, st3)`

- Increase the pointers:
`st0`

and`st1`

by 1 and 3, respectively.