# 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 `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. - If
`i`

is 1, then`st1`

is put on top of the stack. - If
`i`

is 2, then`st2`

is put on top of the stack. - If
`i`

is 3, then`st3`

is put on top of the stack. - If
`i`

is 4, then`st4`

is put on top of the stack. - If
`i`

is 5, then`st5`

is put on top of the stack. - If
`i`

is 6, then`st6`

is put on top of the stack. - If
`i`

is 7, then`st7`

is put on top of the stack. - If
`i`

is 8, then`st8`

is put on top of the stack. - If
`i`

is 9, then`st9`

is put on top of the stack. - If
`i`

is 10, then`st10`

is put on top of the stack. - If
`i`

is 11, then`st11`

is put on top of the stack. - If
`i`

is 12, then`st12`

is put on top of the stack. - If
`i`

is 13, then`st13`

is put on top of the stack. - If
`i`

is 14, then`st14`

is put on top of the stack. - 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`

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

### Description

- Argument
`i`

is not 0. - If
`i`

is 1, then`st0`

is moved into`st1`

. - If
`i`

is 2, then`st0`

is moved into`st2`

. - If
`i`

is 3, then`st0`

is moved into`st3`

. - If
`i`

is 4, then`st0`

is moved into`st4`

. - If
`i`

is 5, then`st0`

is moved into`st5`

. - If
`i`

is 6, then`st0`

is moved into`st6`

. - If
`i`

is 7, then`st0`

is moved into`st7`

. - If
`i`

is 8, then`st0`

is moved into`st8`

. - If
`i`

is 9, then`st0`

is moved into`st9`

. - If
`i`

is 10, then`st0`

is moved into`st10`

. - If
`i`

is 11, then`st0`

is moved into`st11`

. - If
`i`

is 12, then`st0`

is moved into`st12`

. - If
`i`

is 13, then`st0`

is moved into`st13`

. - If
`i`

is 14, then`st0`

is moved into`st14`

. - If
`i`

is 15, then`st0`

is moved into`st15`

. - If
`i`

is 1, then`st1`

is moved into`st0`

. - If
`i`

is 2, then`st2`

is moved into`st0`

. - If
`i`

is 3, then`st3`

is moved into`st0`

. - If
`i`

is 4, then`st4`

is moved into`st0`

. - If
`i`

is 5, then`st5`

is moved into`st0`

. - If
`i`

is 6, then`st6`

is moved into`st0`

. - If
`i`

is 7, then`st7`

is moved into`st0`

. - If
`i`

is 8, then`st8`

is moved into`st0`

. - If
`i`

is 9, then`st9`

is moved into`st0`

. - If
`i`

is 10, then`st10`

is moved into`st0`

. - If
`i`

is 11, then`st11`

is moved into`st0`

. - If
`i`

is 12, then`st12`

is moved into`st0`

. - If
`i`

is 13, then`st13`

is moved into`st0`

. - If
`i`

is 14, then`st14`

is moved into`st0`

. - If
`i`

is 15, then`st15`

is moved into`st0`

. - If
`i`

is not 1, then`st1`

does not change. - If
`i`

is not 2, then`st2`

does not change. - If
`i`

is not 3, then`st3`

does not change. - If
`i`

is not 4, then`st4`

does not change. - If
`i`

is not 5, then`st5`

does not change. - If
`i`

is not 6, then`st6`

does not change. - If
`i`

is not 7, then`st7`

does not change. - If
`i`

is not 8, then`st8`

does not change. - If
`i`

is not 9, then`st9`

does not change. - If
`i`

is not 10, then`st10`

does not change. - If
`i`

is not 11, then`st11`

does not change. - If
`i`

is not 12, then`st12`

does not change. - If
`i`

is not 13, then`st13`

does not change. - If
`i`

is not 14, then`st14`

does not change. - If
`i`

is not 15, then`st15`

does not change. - The op stack pointer does not change.
- The running product for the Op Stack Table remains unchanged.

### Polynomials

`ind_0(hv3, hv2, hv1, hv0)`

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

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

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

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

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

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

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

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

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

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

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

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

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

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

`ind_15(hv3, hv2, hv1, hv0)·(st15' - 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)`

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

`op_stack_pointer' - op_stack_pointer`

`RunningProductOpStackTable' - RunningProductOpStackTable`

## 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 `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 `divine_sibling`

Recall that in a Merkle tree, the indices of left (respectively right) leafs have 0 (respectively 1) as their least significant bit.
The first two polynomials achieve that helper variable `hv0`

holds the result of `st10 mod 2`

.
The third polynomial sets the new value of `st10`

to `st10 div 2`

.

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

### Description

- Helper variable
`hv0`

is either 0 or 1. - If
`hv0`

is 0, then`st0`

does not change. - If
`hv0`

is 0, then`st1`

does not change. - If
`hv0`

is 0, then`st2`

does not change. - If
`hv0`

is 0, then`st3`

does not change. - If
`hv0`

is 0, then`st4`

does not change. - If
`hv0`

is 1, then`st0`

is moved to`st5`

. - If
`hv0`

is 1, then`st1`

is moved to`st6`

. - If
`hv0`

is 1, then`st2`

is moved to`st7`

. - If
`hv0`

is 1, then`st3`

is moved to`st8`

. - If
`hv0`

is 1, then`st4`

is moved to`st9`

. `st5`

is shifted by 1 bit to the right and moved into`st10`

.`st6`

is moved into`st11`

`st7`

is moved into`st12`

`st8`

is moved into`st13`

`st9`

is moved into`st14`

`st10`

is moved into`st15`

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

through`st15`

.

### Polynomials

`hv0·(hv0 - 1)`

`(1 - hv0)·(st0' - st0) + hv0·(st5' - st0)`

`(1 - hv0)·(st1' - st1) + hv0·(st6' - st1)`

`(1 - hv0)·(st2' - st2) + hv0·(st7' - st2)`

`(1 - hv0)·(st3' - st3) + hv0·(st8' - st3)`

`(1 - hv0)·(st4' - st4) + hv0·(st9' - st4)`

`st10'·2 + hv0 - st5`

`st11' - st6`

`st12' - st7`

`st13' - st8`

`st14' - st9`

`st15' - st10`

`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)`

### Helper variable definitions for `divine_sibling`

Since `st10`

contains the Merkle tree node index,

`hv0`

holds the result of`st10 % 2`

(the node index's least significant bit, indicating whether it is a left/right node).

## 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_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`

. - Stack element
`st2`

does not change.

### Polynomials

`st0 - st1·st1' - st0'`

`st2' - st2`

## Instruction `pop_count`

## Instruction `xxadd`

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 `xxmul`

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 `xinvert`

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 `xbmul`

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)`