# 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

1. The instruction's argument a is moved onto the stack.

### Polynomials

1. 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

1. If i is 0, then st0 is put on top of the stack.
2. If i is 1, then st1 is put on top of the stack.
3. If i is 2, then st2 is put on top of the stack.
4. If i is 3, then st3 is put on top of the stack.
5. If i is 4, then st4 is put on top of the stack.
6. If i is 5, then st5 is put on top of the stack.
7. If i is 6, then st6 is put on top of the stack.
8. If i is 7, then st7 is put on top of the stack.
9. If i is 8, then st8 is put on top of the stack.
10. If i is 9, then st9 is put on top of the stack.
11. If i is 10, then st10 is put on top of the stack.
12. If i is 11, then st11 is put on top of the stack.
13. If i is 12, then st12 is put on top of the stack.
14. If i is 13, then st13 is put on top of the stack.
15. If i is 14, then st14 is put on top of the stack.
16. If i is 15, then st15 is put on top of the stack.

### Polynomials

1. ind_0(hv3, hv2, hv1, hv0)·(st0' - st0)
2. ind_1(hv3, hv2, hv1, hv0)·(st0' - st1)
3. ind_2(hv3, hv2, hv1, hv0)·(st0' - st2)
4. ind_3(hv3, hv2, hv1, hv0)·(st0' - st3)
5. ind_4(hv3, hv2, hv1, hv0)·(st0' - st4)
6. ind_5(hv3, hv2, hv1, hv0)·(st0' - st5)
7. ind_6(hv3, hv2, hv1, hv0)·(st0' - st6)
8. ind_7(hv3, hv2, hv1, hv0)·(st0' - st7)
9. ind_8(hv3, hv2, hv1, hv0)·(st0' - st8)
10. ind_9(hv3, hv2, hv1, hv0)·(st0' - st9)
11. ind_10(hv3, hv2, hv1, hv0)·(st0' - st10)
12. ind_11(hv3, hv2, hv1, hv0)·(st0' - st11)
13. ind_12(hv3, hv2, hv1, hv0)·(st0' - st12)
14. ind_13(hv3, hv2, hv1, hv0)·(st0' - st13)
15. ind_14(hv3, hv2, hv1, hv0)·(st0' - st14)
16. 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

1. Argument i is not 0.
2. If i is 1, then st0 is moved into st1.
3. If i is 2, then st0 is moved into st2.
4. If i is 3, then st0 is moved into st3.
5. If i is 4, then st0 is moved into st4.
6. If i is 5, then st0 is moved into st5.
7. If i is 6, then st0 is moved into st6.
8. If i is 7, then st0 is moved into st7.
9. If i is 8, then st0 is moved into st8.
10. If i is 9, then st0 is moved into st9.
11. If i is 10, then st0 is moved into st10.
12. If i is 11, then st0 is moved into st11.
13. If i is 12, then st0 is moved into st12.
14. If i is 13, then st0 is moved into st13.
15. If i is 14, then st0 is moved into st14.
16. If i is 15, then st0 is moved into st15.
17. If i is 1, then st1 is moved into st0.
18. If i is 2, then st2 is moved into st0.
19. If i is 3, then st3 is moved into st0.
20. If i is 4, then st4 is moved into st0.
21. If i is 5, then st5 is moved into st0.
22. If i is 6, then st6 is moved into st0.
23. If i is 7, then st7 is moved into st0.
24. If i is 8, then st8 is moved into st0.
25. If i is 9, then st9 is moved into st0.
26. If i is 10, then st10 is moved into st0.
27. If i is 11, then st11 is moved into st0.
28. If i is 12, then st12 is moved into st0.
29. If i is 13, then st13 is moved into st0.
30. If i is 14, then st14 is moved into st0.
31. If i is 15, then st15 is moved into st0.
32. If i is not 1, then st1 does not change.
33. If i is not 2, then st2 does not change.
34. If i is not 3, then st3 does not change.
35. If i is not 4, then st4 does not change.
36. If i is not 5, then st5 does not change.
37. If i is not 6, then st6 does not change.
38. If i is not 7, then st7 does not change.
39. If i is not 8, then st8 does not change.
40. If i is not 9, then st9 does not change.
41. If i is not 10, then st10 does not change.
42. If i is not 11, then st11 does not change.
43. If i is not 12, then st12 does not change.
44. If i is not 13, then st13 does not change.
45. If i is not 14, then st14 does not change.
46. If i is not 15, then st15 does not change.
47. The op stack pointer does not change.
48. The running product for the Op Stack Table remains unchanged.

### Polynomials

1. ind_0(hv3, hv2, hv1, hv0)
2. ind_1(hv3, hv2, hv1, hv0)·(st1' - st0)
3. ind_2(hv3, hv2, hv1, hv0)·(st2' - st0)
4. ind_3(hv3, hv2, hv1, hv0)·(st3' - st0)
5. ind_4(hv3, hv2, hv1, hv0)·(st4' - st0)
6. ind_5(hv3, hv2, hv1, hv0)·(st5' - st0)
7. ind_6(hv3, hv2, hv1, hv0)·(st6' - st0)
8. ind_7(hv3, hv2, hv1, hv0)·(st7' - st0)
9. ind_8(hv3, hv2, hv1, hv0)·(st8' - st0)
10. ind_9(hv3, hv2, hv1, hv0)·(st9' - st0)
11. ind_10(hv3, hv2, hv1, hv0)·(st10' - st0)
12. ind_11(hv3, hv2, hv1, hv0)·(st11' - st0)
13. ind_12(hv3, hv2, hv1, hv0)·(st12' - st0)
14. ind_13(hv3, hv2, hv1, hv0)·(st13' - st0)
15. ind_14(hv3, hv2, hv1, hv0)·(st14' - st0)
16. ind_15(hv3, hv2, hv1, hv0)·(st15' - st0)
17. ind_1(hv3, hv2, hv1, hv0)·(st0' - st1)
18. ind_2(hv3, hv2, hv1, hv0)·(st0' - st2)
19. ind_3(hv3, hv2, hv1, hv0)·(st0' - st3)
20. ind_4(hv3, hv2, hv1, hv0)·(st0' - st4)
21. ind_5(hv3, hv2, hv1, hv0)·(st0' - st5)
22. ind_6(hv3, hv2, hv1, hv0)·(st0' - st6)
23. ind_7(hv3, hv2, hv1, hv0)·(st0' - st7)
24. ind_8(hv3, hv2, hv1, hv0)·(st0' - st8)
25. ind_9(hv3, hv2, hv1, hv0)·(st0' - st9)
26. ind_10(hv3, hv2, hv1, hv0)·(st0' - st10)
27. ind_11(hv3, hv2, hv1, hv0)·(st0' - st11)
28. ind_12(hv3, hv2, hv1, hv0)·(st0' - st12)
29. ind_13(hv3, hv2, hv1, hv0)·(st0' - st13)
30. ind_14(hv3, hv2, hv1, hv0)·(st0' - st14)
31. ind_15(hv3, hv2, hv1, hv0)·(st0' - st15)
32. (1 - ind_1(hv3, hv2, hv1, hv0))·(st1' - st1)
33. (1 - ind_2(hv3, hv2, hv1, hv0))·(st2' - st2)
34. (1 - ind_3(hv3, hv2, hv1, hv0))·(st3' - st3)
35. (1 - ind_4(hv3, hv2, hv1, hv0))·(st4' - st4)
36. (1 - ind_5(hv3, hv2, hv1, hv0))·(st5' - st5)
37. (1 - ind_6(hv3, hv2, hv1, hv0))·(st6' - st6)
38. (1 - ind_7(hv3, hv2, hv1, hv0))·(st7' - st7)
39. (1 - ind_8(hv3, hv2, hv1, hv0))·(st8' - st8)
40. (1 - ind_9(hv3, hv2, hv1, hv0))·(st9' - st9)
41. (1 - ind_10(hv3, hv2, hv1, hv0))·(st10' - st10)
42. (1 - ind_11(hv3, hv2, hv1, hv0))·(st11' - st11)
43. (1 - ind_12(hv3, hv2, hv1, hv0))·(st12' - st12)
44. (1 - ind_13(hv3, hv2, hv1, hv0))·(st13' - st13)
45. (1 - ind_14(hv3, hv2, hv1, hv0))·(st14' - st14)
46. (1 - ind_15(hv3, hv2, hv1, hv0))·(st15' - st15)
47. op_stack_pointer' - op_stack_pointer
48. 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

1. Helper variable hv1 is the inverse of st0 or 0.
2. Helper variable hv1 is the inverse of st0 or st0 is 0.
3. The next instruction nia is decomposed into helper variables hv1 through hv5.
4. The indicator helper variable hv1 is either 0 or 1. Here, hv1 == 1 means that nia takes an argument.
5. The helper variable hv2 is either 0 or 1 or 2 or 3.
6. The helper variable hv3 is either 0 or 1 or 2 or 3.
7. The helper variable hv4 is either 0 or 1 or 2 or 3.
8. The helper variable hv5 is either 0 or 1 or 2 or 3.
9. 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:

1. (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

1. (st0·hv0 - 1)·hv0
2. (st0·hv0 - 1)·st0
3. nia - hv1 - 2·hv2 - 8·hv3 - 32·hv4 - 128·hv5
4. hv1·(hv1 - 1)
5. hv2·(hv2 - 1)·(hv2 - 2)·(hv2 - 3)
6. hv3·(hv3 - 1)·(hv3 - 2)·(hv3 - 3)
7. hv4·(hv4 - 1)·(hv4 - 2)·(hv4 - 3)
8. hv5·(hv5 - 1)·(hv5 - 2)·(hv5 - 3)
9. (ip' - (ip + 1)·st0)
 + ((ip' - (ip + 2))·(st0·hv0 - 1)·(hv1 - 1))
 + ((ip' - (ip + 3))·(st0·hv0 - 1)·hv1)

### Helper variable definitions for skiz

1. hv0 = inverse(st0) (if st0 ≠ 0)
2. hv1 = nia mod 2
3. hv2 = (nia >> 1) mod 4
4. hv3 = (nia >> 3) mod 4
5. hv4 = (nia >> 5) mod 4
6. hv5 = nia >> 7

## Instruction call + d

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

### Description

1. The jump stack pointer jsp is incremented by 1.
2. The jump's origin jso is set to the current instruction pointer ip plus 2.
3. The jump's destination jsd is set to the instruction's argument d.
4. The instruction pointer ip is set to the instruction's argument d.

### Polynomials

1. jsp' - (jsp + 1)
2. jso' - (ip + 2)
3. jsd' - nia
4. ip' - nia

## Instruction return

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

### Description

1. The jump stack pointer jsp is decremented by 1.
2. The instruction pointer ip is set to the last call's origin jso.

### Polynomials

1. jsp' - (jsp - 1)
2. ip' - jso

## Instruction recurse

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

### Description

1. The jump stack pointer jsp does not change.
2. The last jump's origin jso does not change.
3. The last jump's destination jsd does not change.
4. The instruction pointer ip is set to the last jump's destination jsd.

### Polynomials

1. jsp' - jsp
2. jso' - jso
3. jsd' - jsd
4. ip' - jsd

## Instruction assert

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

### Description

1. The current top of the stack st0 is 1.

### Polynomials

1. st0 - 1

## Instruction halt

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

### Description

1. The instruction executed in the following step is instruction halt.

### Polynomials

1. ci' - ci

## Instruction read_mem + n

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

### Description

1. The RAM pointer st0 is decremented by n.
2. 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.
3. 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.
4. 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.
5. 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.
6. 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.
7. 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.
8. 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.
9. 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.
10. 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.
11. 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.
12. 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.
13. 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.
14. 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.
15. 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
16. 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.
17. 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.
18. 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

1. The RAM pointer st0 is incremented by n.
2. 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.
3. 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.
4. 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.
5. 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.
6. 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.
7. 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.
8. 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.
9. 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.
10. 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.
11. 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.
12. 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.
13. 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.
14. 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.
15. 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.
16. 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.
17. 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.
18. 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

1. st10 is moved into st5.
2. st11 is moved into st6.
3. st12 is moved into st7.
4. st13 is moved into st8.
5. st14 is moved into st9.
6. st15 is moved into st10.
7. The op stack pointer shrinks by 5.
8. The running product with the Op Stack Table accumulates next row's st11 through st15.

### Polynomials

1. st5' - st10
2. st6' - st11
3. st7' - st12
4. st8' - st13
5. st9' - st14
6. st10' - st15
7. op_stack_pointer' - op_stack_pointer + 5
8. 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

1. Helper variable hv0 is either 0 or 1.
2. If hv0 is 0, then st0 does not change.
3. If hv0 is 0, then st1 does not change.
4. If hv0 is 0, then st2 does not change.
5. If hv0 is 0, then st3 does not change.
6. If hv0 is 0, then st4 does not change.
7. If hv0 is 1, then st0 is moved to st5.
8. If hv0 is 1, then st1 is moved to st6.
9. If hv0 is 1, then st2 is moved to st7.
10. If hv0 is 1, then st3 is moved to st8.
11. If hv0 is 1, then st4 is moved to st9.
12. st5 is shifted by 1 bit to the right and moved into st10.
13. st6 is moved into st11
14. st7 is moved into st12
15. st8 is moved into st13
16. st9 is moved into st14
17. st10 is moved into st15
18. The op stack pointer grows by 5.
19. The running product with the Op Stack Table accumulates st11 through st15.

### Polynomials

1. hv0·(hv0 - 1)
2. (1 - hv0)·(st0' - st0) + hv0·(st5' - st0)
3. (1 - hv0)·(st1' - st1) + hv0·(st6' - st1)
4. (1 - hv0)·(st2' - st2) + hv0·(st7' - st2)
5. (1 - hv0)·(st3' - st3) + hv0·(st8' - st3)
6. (1 - hv0)·(st4' - st4) + hv0·(st9' - st4)
7. st10'·2 + hv0 - st5
8. st11' - st6
9. st12' - st7
10. st13' - st8
11. st14' - st9
12. st15' - st10
13. op_stack_pointer' - op_stack_pointer - 5
14. 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,

1. 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

1. st0 is equal to st5.
2. st1 is equal to st6.
3. st2 is equal to st7.
4. st3 is equal to st8.
5. st4 is equal to st9.
6. st10 is moved into st5.
7. st11 is moved into st6.
8. st12 is moved into st7.
9. st13 is moved into st8.
10. st14 is moved into st9.
11. st15 is moved into st10.
12. The op stack pointer shrinks by 5.
13. The running product with the Op Stack Table accumulates next row's st11 through st15.

### Polynomials

1. st5 - st0
2. st6 - st1
3. st7 - st2
4. st8 - st3
5. st9 - st4
6. st5' - st10
7. st6' - st11
8. st7' - st12
9. st8' - st13
10. st9' - st14
11. st10' - st15
12. op_stack_pointer' - op_stack_pointer + 5
13. 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

1. st10 is moved into st0.
2. st11 is moved into st1.
3. st12 is moved into st2.
4. st13 is moved into st3.
5. st14 is moved into st4.
6. st15 is moved into st5.
7. The op stack pointer shrinks by 10.
8. The running product with the Op Stack Table accumulates next row's st6 through st15.

### Polynomials

1. st0' - st10
2. st1' - st11
3. st2' - st12
4. st3' - st13
5. st4' - st14
6. st5' - st15
7. op_stack_pointer' - op_stack_pointer + 10
8. 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

1. st0 is moved into st10.
2. st1 is moved into st11.
3. st2 is moved into st12.
4. st3 is moved into st13.
5. st4 is moved into st14.
6. st5 is moved into st15.
7. The op stack pointer grows by 10.
8. The running product with the Op Stack Table accumulates st6 through st15.

### Polynomials

1. st10' - st0
2. st11' - st1
3. st12' - st2
4. st13' - st3
5. st14' - st4
6. st15' - st5
7. op_stack_pointer' - op_stack_pointer - 10
8. 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

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

### Polynomials

1. st0' - (st0 + st1)

## Instruction mul

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

### Description

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

### Polynomials

1. st0' - st0·st1

## Instruction invert

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

### Description

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

### Polynomials

1. st0'·st0 - 1

## Instruction eq

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

### Description

1. Helper variable hv0 is the inverse of the difference of the stack's two top-most elements or 0.
2. Helper variable hv0 is the inverse of the difference of the stack's two top-most elements or the difference is 0.
3. 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

1. hv0·(hv0·(st1 - st0) - 1)
2. (st1 - st0)·(hv0·(st1 - st0) - 1)
3. st0' - (1 - hv0·(st1 - st0))

### Helper variable definitions for eq

1. hv0 = inverse(rhs - lhs) if rhs ≠ lhs.
2. 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

1. The top of the stack is decomposed as 32-bit chunks into the stack's top-most two elements.
2. Helper variable hv0 holds the inverse of subtracted from the high 32 bits or the low 32 bits are 0.

### Polynomials

1. st0 - (2^32·st1' + st0')
2. 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,

1. hv0 = (hi - (2^32 - 1)) if lo ≠ 0.
2. 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

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

## Instruction pow

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

## 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:

1. The remainder r is smaller than the denominator d, and
2. all four of n, d, q, and r are u32s.

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

### Description

1. Numerator is quotient times denominator plus remainder: n == q·d + r.
2. Stack element st2 does not change.

### Polynomials

1. st0 - st1·st1' - st0'
2. st2' - st2

## Instruction pop_count

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

## Instruction xxadd

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

### Description

1. The result of adding st0 to st3 is moved into st0.
2. The result of adding st1 to st4 is moved into st1.
3. The result of adding st2 to st5 is moved into st2.
4. st6 is moved into st3.
5. st7 is moved into st4.
6. st8 is moved into st5.
7. st9 is moved into st6.
8. st10 is moved into st7.
9. st11 is moved into st8.
10. st12 is moved into st9.
11. st13 is moved into st10.
12. st14 is moved into st11.
13. st15 is moved into st12.
14. The op stack pointer shrinks by 3.
15. The running product with the Op Stack Table accumulates next row's st13 through st15.

### Polynomials

1. st0' - (st0 + st3)
2. st1' - (st1 + st4)
3. st2' - (st2 + st5)
4. st3' - st6
5. st4' - st7
6. st5' - st8
7. st6' - st9
8. st7' - st10
9. st8' - st11
10. st9' - st12
11. st10' - st13
12. st11' - st14
13. st12' - st15
14. op_stack_pointer' - op_stack_pointer + 3
15. RunningProductOpStackTable' - RunningProductOpStackTable·(🪤 - 🍋·clk - 🍊 - 🍉·op_stack_pointer' - 🫒·st15')
·(🪤 - 🍋·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

1. The coefficient of x^0 of multiplying the two X-Field elements on the stack is moved into st0.
2. The coefficient of x^1 of multiplying the two X-Field elements on the stack is moved into st1.
3. The coefficient of x^2 of multiplying the two X-Field elements on the stack is moved into st2.
4. st6 is moved into st3.
5. st7 is moved into st4.
6. st8 is moved into st5.
7. st9 is moved into st6.
8. st10 is moved into st7.
9. st11 is moved into st8.
10. st12 is moved into st9.
11. st13 is moved into st10.
12. st14 is moved into st11.
13. st15 is moved into st12.
14. The op stack pointer shrinks by 3.
15. The running product with the Op Stack Table accumulates next row's st13 through st15.

### Polynomials

1. st0' - (st0·st3 - st2·st4 - st1·st5)
2. st1' - (st1·st3 + st0·st4 - st2·st5 + st2·st4 + st1·st5)
3. st2' - (st2·st3 + st1·st4 + st0·st5 + st2·st5)
4. st3' - st6
5. st4' - st7
6. st5' - st8
7. st6' - st9
8. st7' - st10
9. st8' - st11
10. st9' - st12
11. st10' - st13
12. st11' - st14
13. st12' - st15
14. op_stack_pointer' - op_stack_pointer + 3
15. RunningProductOpStackTable' - RunningProductOpStackTable·(🪤 - 🍋·clk - 🍊 - 🍉·op_stack_pointer' - 🫒·st15')
·(🪤 - 🍋·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

1. 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.
2. 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.
3. 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

1. st0·st0' - st2·st1' - st1·st2' - 1
2. st1·st0' + st0·st1' - st2·st2' + st2·st1' + st1·st2'
3. st2·st0' + st1·st1' + st0·st2' + st2·st2'

## Instruction xbmul

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

### Description

1. The result of multiplying the top of the stack with the X-Field element's coefficient for x^0 is moved into st0.
2. The result of multiplying the top of the stack with the X-Field element's coefficient for x^1 is moved into st1.
3. The result of multiplying the top of the stack with the X-Field element's coefficient for x^2 is moved into st2.
4. st4 is moved into st3.
5. st5 is moved into st4.
6. st6 is moved into st5.
7. st7 is moved into st6.
8. st8 is moved into st7.
9. st9 is moved into st8.
10. st10 is moved into st9.
11. st11 is moved into st10.
12. st12 is moved into st11.
13. st13 is moved into st12.
14. st14 is moved into st13.
15. st15 is moved into st14.
16. The op stack pointer shrinks by 3.
17. The running product with the Op Stack Table accumulates next row's st15.

### Polynomials

1. st0' - st0·st1
2. st1' - st0·st2
3. st2' - st0·st3
4. st3' - st4
5. st4' - st5
6. st5' - stt
7. st6' - st7
8. st7' - st8
9. st8' - st9
10. st9' - st10
11. st10' - st11
12. st11' - st12
13. st12' - st13
14. st13' - st14
15. st14' - st15
16. op_stack_pointer' - op_stack_pointer + 1
17. RunningProductOpStackTable' - RunningProductOpStackTable·(🪤 - 🍋·clk - 🍊 - 🍉·op_stack_pointer' - 🫒·st15')

## Instruction read_io + n

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

### Description

1. 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

1. 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

1. 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

1. 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)