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
keep_ramRAM does not change, i.e.,registers ramp and ramv do not change
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
stack_grows_and_top_2_unconstrainedoperational stack elements starting from st1 are shifted down by one position, highest two elements of the resulting stack are unconstrained
grow_stackoperational stack elements are shifted down by one position, top element of the resulting stack is unconstrained
stack_remains_and_top_11_unconstrainedoperational stack's top 11 elements are unconstrained, rest of stack remains unchanged
stack_remains_and_top_10_unconstrainedoperational stack's top 10 elements are unconstrained, rest of stack remains unchanged
stack_remains_and_top_3_unconstrainedoperational stack's top 3 elements are unconstrained, rest of stack remains unchanged
unary_operationoperational stack's top-most element is unconstrained, rest of stack remains unchanged
keep_stackoperational stack remains unchanged
stack_shrinks_and_top_3_unconstrainedoperational stack elements starting from st3 are shifted up by one position, highest three elements of the resulting stack are unconstrained. Needs hv0
binary_operationoperational stack elements starting from st2 are shifted up by one position, highest two elements of the resulting stack are unconstrained. Needs hv0
shrink_stackoperational stack elements starting from st1 are shifted up by one position. Needs hv0

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_argkeep_ramkeep_jump_stackstep_1step_2stack_grows_and_top_2_unconstrainedgrow_stackstack_remains_and_top_11_unconstrainedstack_remains_and_top_10_unconstrainedstack_remains_and_top_3_unconstrainedunary_operationkeep_stackstack_shrinks_and_top_3_unconstrainedbinary_operationshrink_stack
popxxx
push + axxx
divinexxx
dup + ixxxx
swap + ixxx
nopxxx
skizxxx
call + dxx
returnxx
recursexxx
assertxxx
haltxxx
read_memxx
write_memxx
hashxxx
divine_siblingxxx
assert_vectorxxx
absorb_initxxx
absorbxxx
squeezexxx
addxxx
mulxxx
invertxxx
eqxxx
splitxxx
ltxxx
andxxx
xorxxx
log_2_floorxxx
powxxx
divxxx
pop_countxxx
xxaddxxx
xxmulxxx
xinvertxxx
xbmulxxx
read_ioxxx
write_ioxxx

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 dup and swap, it is beneficial to have polynomials that evaluate to 1 if the instruction's argument i is a specific value, and to 0 otherwise. This allows indicating which registers are constraint, and in which way they are, depending on i. 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 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.

Below, you can find a list of all 16 indicator polynomials.

  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 are the 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 keep_ram

Description

  1. The RAM pointer ramp does not change.
  2. The RAM value ramv does not change.

Polynomials

  1. ramp' - ramp
  2. ramv' - ramv

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 stack_grows_and_top_2_unconstrained

Description

  1. The stack element in st1 is moved into st2.
  2. The stack element in st2 is moved into st3.
  3. The stack element in st3 is moved into st4.
  4. The stack element in st4 is moved into st5.
  5. The stack element in st5 is moved into st6.
  6. The stack element in st6 is moved into st7.
  7. The stack element in st7 is moved into st8.
  8. The stack element in st8 is moved into st9.
  9. The stack element in st9 is moved into st10.
  10. The stack element in st10 is moved into st11.
  11. The stack element in st11 is moved into st12.
  12. The stack element in st12 is moved into st13.
  13. The stack element in st13 is moved into st14.
  14. The stack element in st14 is moved into st15.
  15. The stack element in st15 is moved to the top of OpStack underflow, i.e., osv.
  16. The OpStack pointer is incremented by 1.

Polynomials

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

Group grow_stack

Contains all constraints from instruction group stack_grows_and_top_2_unconstrained, and additionally:

Description

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

Polynomials

  1. st1' - st0

Group stack_remains_and_top_11_unconstrained

Description

  1. The stack element in st11 does not change.
  2. The stack element in st12 does not change.
  3. The stack element in st13 does not change.
  4. The stack element in st14 does not change.
  5. The stack element in st15 does not change.
  6. The top of the OpStack underflow, i.e., osv, does not change.
  7. The OpStack pointer does not change.

Polynomials

  1. st11' - st11
  2. st12' - st12
  3. st13' - st13
  4. st14' - st14
  5. st15' - st15
  6. osv' - osv
  7. osp' - osp

Group stack_remains_and_top_10_unconstrained

Contains all constraints from instruction group stack_remains_and_top_11_unconstrained, and additionally:

Description

  1. The stack element in st10 does not change.

Polynomials

  1. st10' - st10

Group stack_remains_and_top_3_unconstrained

Contains all constraints from instruction group stack_remains_and_top_10_unconstrained, and additionally:

Description

  1. The stack element in st3 does not change.
  2. The stack element in st4 does not change.
  3. The stack element in st5 does not change.
  4. The stack element in st6 does not change.
  5. The stack element in st7 does not change.
  6. The stack element in st8 does not change.
  7. The stack element in st9 does not change.

Polynomials

  1. st3' - st3
  2. st4' - st4
  3. st5' - st5
  4. st6' - st6
  5. st7' - st7
  6. st8' - st8
  7. st9' - st9

Group unary_operation

Contains all constraints from instruction group stack_remains_and_top_3_unconstrained, and additionally:

Description

  1. The stack element in st1 does not change.
  2. The stack element in st2 does not change.

Polynomials

  1. st1' - st1
  2. st2' - st2

Group keep_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 stack_shrinks_and_top_3_unconstrained

This instruction group requires helper variable hv0 to hold the multiplicative inverse of (osp - 16). In effect, this means that the OpStack pointer can only be decremented if it is not 16, i.e., if OpStack Underflow Memory is not empty. Since the stack can only change by one element at a time, this prevents stack underflow.

Description

  1. The stack element in st4 is moved into st3.
  2. The stack element in st5 is moved into st4.
  3. The stack element in st6 is moved into st5.
  4. The stack element in st7 is moved into st6.
  5. The stack element in st8 is moved into st7.
  6. The stack element in st9 is moved into st8.
  7. The stack element in st10 is moved into st9.
  8. The stack element in st11 is moved into st10.
  9. The stack element in st12 is moved into st11.
  10. The stack element in st13 is moved into st12.
  11. The stack element in st14 is moved into st13.
  12. The stack element in st15 is moved into st14.
  13. The stack element at the top of OpStack underflow, i.e., osv, is moved into st15.
  14. The OpStack pointer is decremented by 1.
  15. The helper variable register hv0 holds the inverse of (osp - 16).

Polynomials

  1. st3' - st4
  2. st4' - st5
  3. st5' - st6
  4. st6' - st7
  5. st7' - st8
  6. st8' - st9
  7. st9' - st10
  8. st10' - st11
  9. st11' - st12
  10. st12' - st13
  11. st13' - st14
  12. st14' - st15
  13. st15' - osv
  14. osp' - (osp - 1)
  15. (osp - 16)·hv0 - 1

Group binary_operation

Contains all constraints from instruction group stack_shrinks_and_top_3_unconstrained, and additionally:

Description

  1. The stack element in st2 is moved into st1.
  2. The stack element in st3 is moved into st2.

Polynomials

  1. st1' - st2
  2. st2' - st3

Group shrink_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