Instruction Groups

Some transition constraints are shared across some, or even many instructions. For example, most instructions must not change the jump stack. Likewise, most instructions must not change RAM. To simplify presentation of the instruction-specific transition constraints, these common constraints are grouped together and aliased. Continuing above example, instruction group keep_jump_stack contains all transition constraints to ensure that the jump stack remains unchanged.

The next section treats each instruction group in detail. The following table lists and briefly explains all instruction groups.

group namedescription
decompose_arginstruction's argument held in nia is binary decomposed into helper registers hv0 through hv3
prohibit_illegal_num_wordsconstrain the instruction's argument n to 1 ⩽ n ⩽ 5
no_iothe running evaluations for public input & output remain unchanged
keep_ramRAM does not change, i.e., the running product of the Permutation Argument with the RAM Table remains unchanged
keep_jump_stackjump stack does not change, i.e., registers jsp, jso, and jsd do not change
step_1jump stack does not change and instruction pointer ip increases by 1
step_2jump stack does not change and instruction pointer ip increases by 2
grow_op_stackop stack elements are shifted down by one position, top element of the resulting stack is unconstrained
grow_op_stack_by_any_ofop stack elements are shifted down by n positions, top n elements of the resulting stack are unconstrained, where n is the instruction's argument
unary_operationop stack's top-most element is unconstrained, rest of stack remains unchanged
keep_op_stackop stack remains unchanged, i.e., the running product of the Permutation Argument with the Op Stack Table remains unchanged
binary_operationop stack elements starting from st2 are shifted up by one position, highest two elements of the resulting stack are unconstrained
shrink_op_stackop stack elements starting from st1 are shifted up by one position
shrink_op_stack_by_any_ofop stack elements starting from stn are shifted up by one position, where n is the instruction's argument

Below figure gives a comprehensive overview over the subset relation between all instruction groups.

A summary of all instructions and which groups they are part of is given in the following table.

instructiondecompose_argprohibit_illegal_num_wordsno_iokeep_ramkeep_jump_stackstep_1step_2grow_op_stackgrow_op_stack_by_any_ofunary_operationkeep_op_stackbinary_operationshrink_op_stackshrink_op_stack_by_any_of
pop + nxxxxxx
push + axxxx
divine + nxxxxxx
dup + ixxxxx
swap + ixxxx
nopxxxx
skizxxxx
call + dxxx
returnxxx
recursexxxx
assertxxxx
haltxxxx
read_mem + nxxxx
write_mem + nxxxx
hashxxx
divine_siblingxxx
assert_vectorxxx
sponge_initxxx
sponge_absorbxxx
sponge_squeezexxx
addxxxx
mulxxxx
invertxxxx
eqxxxx
splitxxx
ltxxxx
andxxxx
xorxxxx
log_2_floorxxxx
powxxxx
div_modxxx
pop_countxxxx
xxaddxxx
xxmulxxx
xinvertxxx
xbmulxxx
read_io + nxxxxx
write_io + nxxxxx

Indicator Polynomials ind_i(hv3, hv2, hv1, hv0)

In this and the following sections, a register marked with a ' refers to the next state of that register. For example, st0' = st0 + 2 means that stack register st0 is incremented by 2. An alternative view for the same concept is that registers marked with ' are those of the next row in the table.

For instructions like dup i, swap i, pop n, et cetera, it is beneficial to have polynomials that evaluate to 1 if the instruction's argument is a specific value, and to 0 otherwise. This allows indicating which registers are constraint, and in which way they are, depending on the argument. This is the purpose of the indicator polynomials ind_i. Evaluated on the binary decomposition of i, they show the behavior described above.

For example, take i = 13. The corresponding binary decomposition is (hv3, hv2, hv1, hv0) = (1, 1, 0, 1). Indicator polynomial ind_13(hv3, hv2, hv1, hv0) is defined as hv3·hv2·(1 - hv1)·hv0. It evaluates to 1 on (1, 1, 0, 1), i.e., ind_13(1, 1, 0, 1) = 1. Any other indicator polynomial, like ind_7, evaluates to 0 on (1, 1, 0, 1). Likewise, the indicator polynomial for 13 evaluates to 0 for any other argument.

The list of all 16 indicator polynomials is:

  1. ind_0(hv3, hv2, hv1, hv0) = (1 - hv3)·(1 - hv2)·(1 - hv1)·(1 - hv0)
  2. ind_1(hv3, hv2, hv1, hv0) = (1 - hv3)·(1 - hv2)·(1 - hv1)·hv0
  3. ind_2(hv3, hv2, hv1, hv0) = (1 - hv3)·(1 - hv2)·hv1·(1 - hv0)
  4. ind_3(hv3, hv2, hv1, hv0) = (1 - hv3)·(1 - hv2)·hv1·hv0
  5. ind_4(hv3, hv2, hv1, hv0) = (1 - hv3)·hv2·(1 - hv1)·(1 - hv0)
  6. ind_5(hv3, hv2, hv1, hv0) = (1 - hv3)·hv2·(1 - hv1)·hv0
  7. ind_6(hv3, hv2, hv1, hv0) = (1 - hv3)·hv2·hv1·(1 - hv0)
  8. ind_7(hv3, hv2, hv1, hv0) = (1 - hv3)·hv2·hv1·hv0
  9. ind_8(hv3, hv2, hv1, hv0) = hv3·(1 - hv2)·(1 - hv1)·(1 - hv0)
  10. ind_9(hv3, hv2, hv1, hv0) = hv3·(1 - hv2)·(1 - hv1)·hv0
  11. ind_10(hv3, hv2, hv1, hv0) = hv3·(1 - hv2)·hv1·(1 - hv0)
  12. ind_11(hv3, hv2, hv1, hv0) = hv3·(1 - hv2)·hv1·hv0
  13. ind_12(hv3, hv2, hv1, hv0) = hv3·hv2·(1 - hv1)·(1 - hv0)
  14. ind_13(hv3, hv2, hv1, hv0) = hv3·hv2·(1 - hv1)·hv0
  15. ind_14(hv3, hv2, hv1, hv0) = hv3·hv2·hv1·(1 - hv0)
  16. ind_15(hv3, hv2, hv1, hv0) = hv3·hv2·hv1·hv0

Group decompose_arg

Description

  1. The helper variables hv0 through hv3 are the binary decomposition of the instruction's argument, which is held in register nia.
  2. The helper variable hv0 is either 0 or 1.
  3. The helper variable hv1 is either 0 or 1.
  4. The helper variable hv2 is either 0 or 1.
  5. The helper variable hv3 is either 0 or 1.

Polynomials

  1. nia - (8·hv3 + 4·hv2 + 2·hv1 + hv0)
  2. hv0·(hv0 - 1)
  3. hv1·(hv1 - 1)
  4. hv2·(hv2 - 1)
  5. hv3·(hv3 - 1)

Group prohibit_illegal_num_words

Is only ever used in combination with instruction group decompose_arg. Therefore, the instruction argument's correct binary decomposition is known to be in helper variables hv0 through hv3.

Description

  1. The argument is not 0.
  2. The argument is not 6.
  3. The argument is not 7.
  4. The argument is not 8.
  5. The argument is not 9.
  6. The argument is not 10.
  7. The argument is not 11.
  8. The argument is not 12.
  9. The argument is not 13.
  10. The argument is not 14.
  11. The argument is not 15.

Polynomials

  1. ind_0(hv3, hv2, hv1, hv0)
  2. ind_6(hv3, hv2, hv1, hv0)
  3. ind_7(hv3, hv2, hv1, hv0)
  4. ind_8(hv3, hv2, hv1, hv0)
  5. ind_9(hv3, hv2, hv1, hv0)
  6. ind_10(hv3, hv2, hv1, hv0)
  7. ind_11(hv3, hv2, hv1, hv0)
  8. ind_12(hv3, hv2, hv1, hv0)
  9. ind_13(hv3, hv2, hv1, hv0)
  10. ind_14(hv3, hv2, hv1, hv0)
  11. ind_15(hv3, hv2, hv1, hv0)

Group no_io

Description

  1. The running evaluation for standard input remains unchanged.
  2. The running evaluation for standard output remains unchanged.

Polynomials

  1. RunningEvaluationStandardInput' - RunningEvaluationStandardInput
  2. RunningEvaluationStandardOutput' - RunningEvaluationStandardOutput

Group keep_ram

Description

  1. The running product for the Permutation Argument with the RAM table does not change.

Polynomials

  1. RunningProductRamTable' - RunningProductRamTable

Group keep_jump_stack

Description

  1. The jump stack pointer jsp does not change.
  2. The jump stack origin jso does not change.
  3. The jump stack destination jsd does not change.

Polynomials

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

Group step_1

Contains all constraints from instruction group keep_jump_stack, and additionally:

Description

  1. The instruction pointer increments by 1.

Polynomials

  1. ip' - (ip + 1)

Group step_2

Contains all constraints from instruction group keep_jump_stack, and additionally:

Description

  1. The instruction pointer increments by 2.

Polynomials

  1. ip' - (ip + 2)

Group grow_op_stack

Description

  1. The stack element in st0 is moved into st1.
  2. The stack element in st1 is moved into st2.
  3. The stack element in st2 is moved into st3.
  4. The stack element in st3 is moved into st4.
  5. The stack element in st4 is moved into st5.
  6. The stack element in st5 is moved into st6.
  7. The stack element in st6 is moved into st7.
  8. The stack element in st7 is moved into st8.
  9. The stack element in st8 is moved into st9.
  10. The stack element in st9 is moved into st10.
  11. The stack element in st10 is moved into st11.
  12. The stack element in st11 is moved into st12.
  13. The stack element in st12 is moved into st13.
  14. The stack element in st13 is moved into st14.
  15. The stack element in st14 is moved into st15.
  16. The op stack pointer is incremented by 1.
  17. The running product for the Op Stack Table absorbs the current row with respect to challenges 🍋, 🍊, 🍉, and 🫒 and indeterminate 🪤.

Polynomials

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

Group grow_op_stack_by_any_of

Is only ever used in combination with instruction group decompose_arg. Therefore, the instruction's argument n correct binary decomposition is known to be in helper variables hv0 through hv3.

Description

  1. If n is 1, then st0 is moved into st1
    else if n is 2, then st0 is moved into st2
    else if n is 3, then st0 is moved into st3
    else if n is 4, then st0 is moved into st4
    else if n is 5, then st0 is moved into st5.
  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 the running product 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.
  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.
  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.
  17. If n is 1, then the running product with the Op Stack Table accumulates st15.

Group unary_operation

Description

  1. The stack element in st1 does not change.
  2. The stack element in st2 does not change.
  3. The stack element in st3 does not change.
  4. The stack element in st4 does not change.
  5. The stack element in st5 does not change.
  6. The stack element in st6 does not change.
  7. The stack element in st7 does not change.
  8. The stack element in st8 does not change.
  9. The stack element in st9 does not change.
  10. The stack element in st10 does not change.
  11. The stack element in st11 does not change.
  12. The stack element in st12 does not change.
  13. The stack element in st13 does not change.
  14. The stack element in st14 does not change.
  15. The stack element in st15 does not change.
  16. The op stack pointer does not change.
  17. The running product for the Op Stack Table remains unchanged.

Polynomials

  1. st1' - st1
  2. st2' - st2
  3. st3' - st3
  4. st4' - st4
  5. st5' - st5
  6. st6' - st6
  7. st7' - st7
  8. st8' - st8
  9. st9' - st9
  10. st10' - st10
  11. st11' - st11
  12. st12' - st12
  13. st13' - st13
  14. st14' - st14
  15. st15' - st15
  16. op_stack_pointer' - op_stack_pointer
  17. RunningProductOpStackTable' - RunningProductOpStackTable

Group keep_op_stack

Contains all constraints from instruction group unary_operation, and additionally:

Description

  1. The stack element in st0 does not change.

Polynomials

  1. st0' - st0

Group binary_operation

Description

  1. The stack element in st2 is moved into st1.
  2. The stack element in st3 is moved into st2.
  3. The stack element in st4 is moved into st3.
  4. The stack element in st5 is moved into st4.
  5. The stack element in st6 is moved into st5.
  6. The stack element in st7 is moved into st6.
  7. The stack element in st8 is moved into st7.
  8. The stack element in st9 is moved into st8.
  9. The stack element in st10 is moved into st9.
  10. The stack element in st11 is moved into st10.
  11. The stack element in st12 is moved into st11.
  12. The stack element in st13 is moved into st12.
  13. The stack element in st14 is moved into st13.
  14. The stack element in st15 is moved into st14.
  15. The op stack pointer is decremented by 1.
  16. The running product for the Op Stack Table absorbs clock cycle and instruction bit 1 from the current row as well as op stack pointer and stack element 15 from the next row with respect to challenges 🍋, 🍊, 🍉, and 🫒 and indeterminate 🪤.

Polynomials

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

Group shrink_op_stack

Contains all constraints from instruction group binary_operation, and additionally:

Description

  1. The stack element in st1 is moved into st0.

Polynomials

  1. st0' - st1

Group shrink_op_stack_by_any_of

Is only ever used in combination with instruction group decompose_arg. Therefore, the instruction's argument n correct binary decomposition is known to be in helper variables hv0 through hv3.

Description

  1. If n is 1, then st1 is moved into st0
    else if n is 2, then st2 is moved into st0
    else if n is 3, then st3 is moved into st0
    else if n is 4, then st4 is moved into st0
    else if n is 5, then st5 is moved into st0.
  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.
  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.
  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.
  17. If n is 1, then the running product with the Op Stack Table accumulates next row's st15.