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.

Instruction `divine` + `n`

This instruction is fully constrained by its instruction groups

Instruction `pick` + `i`

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

Description

For 0 ⩽ i < 16:

Stack element i is moved to the top.
For 0 ⩽ j < i: stack element j is shifted down by 1.
For j > i: stack element j remains unchanged.

Instruction `place` + `i`

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

Description

For 0 ⩽ i < 16:

Stack element 0 is moved to position i.
For 0 ⩽ j < i: stack element j is shifted up by 1.
For j > i: stack element j remains unchanged.

Instruction `dup` + `i`

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

Description

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

Polynomials

ind_0(hv3, hv2, hv1, hv0)·(st0' - st0)
+ ind_1(hv3, hv2, hv1, hv0)·(st0' - st1)
+ ind_2(hv3, hv2, hv1, hv0)·(st0' - st2)
+ ind_3(hv3, hv2, hv1, hv0)·(st0' - st3)
+ ind_4(hv3, hv2, hv1, hv0)·(st0' - st4)
+ ind_5(hv3, hv2, hv1, hv0)·(st0' - st5)
+ ind_6(hv3, hv2, hv1, hv0)·(st0' - st6)
+ ind_7(hv3, hv2, hv1, hv0)·(st0' - st7)
+ ind_8(hv3, hv2, hv1, hv0)·(st0' - st8)
+ ind_9(hv3, hv2, hv1, hv0)·(st0' - st9)
+ ind_10(hv3, hv2, hv1, hv0)·(st0' - st10)
+ ind_11(hv3, hv2, hv1, hv0)·(st0' - st11)
+ ind_12(hv3, hv2, hv1, hv0)·(st0' - st12)
+ ind_13(hv3, hv2, hv1, hv0)·(st0' - st13)
+ ind_14(hv3, hv2, hv1, hv0)·(st0' - st14)
+ ind_15(hv3, hv2, hv1, hv0)·(st0' - st15)

Instruction `swap` + `i`

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

Description

For 0 ⩽ i < 16:

Stack element i is moved to the top.
The top stack element is moved to position i
For j ≠ i: stack element j remains unchanged.

Instruction `nop`

This instruction is fully constrained by its instruction groups

For the correct behavior of instruction skiz, the instruction pointer ip needs to increment by either 1, or 2, or 3. The concrete value depends on the top of the stack st0 and the next instruction, held in nia.

Helper variable hv0 helps with identifying whether st0 is 0. To this end, it holds the inverse-or-zero of st0, i.e., is 0 if and only if st0 is 0, and is the inverse of st0 otherwise.

Efficient arithmetization of instruction skiz makes use of one of the properties of opcodes. Concretely, the least significant bit of an opcode is 1 if and only if the instruction takes an argument. The arithmetization of skiz can incorporate this simple flag by decomposing nia into helper variable registers hv, similarly to how ci is (always) deconstructed into instruction bit registers ib. Correct decomposition is guaranteed by employing a range check.

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

Description

Helper variable hv1 is the inverse of st0 or 0.
Helper variable hv1 is the inverse of st0 or st0 is 0.
The next instruction nia is decomposed into helper variables hv1 through hv5.
The indicator helper variable hv1 is either 0 or 1. Here, hv1 == 1 means that nia takes an argument.
The helper variable hv2 is either 0 or 1 or 2 or 3.
The helper variable hv3 is either 0 or 1 or 2 or 3.
The helper variable hv4 is either 0 or 1 or 2 or 3.
The helper variable hv5 is either 0 or 1 or 2 or 3.
If st0 is non-zero, register ip is incremented by 1. If st0 is 0 and nia takes no argument, register ip is incremented by 2. If st0 is 0 and nia takes an argument, register ip is incremented by 3.

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

(Register st0 is 0 or ip is incremented by 1), and (st0 has a multiplicative inverse or hv1 is 1 or ip is incremented by 2), and (st0 has a multiplicative inverse or hv1 is 0 or ip is incremented by 3).

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

Polynomials

(st0·hv0 - 1)·hv0
(st0·hv0 - 1)·st0
nia - hv1 - 2·hv2 - 8·hv3 - 32·hv4 - 128·hv5
hv1·(hv1 - 1)
hv2·(hv2 - 1)·(hv2 - 2)·(hv2 - 3)
hv3·(hv3 - 1)·(hv3 - 2)·(hv3 - 3)
hv4·(hv4 - 1)·(hv4 - 2)·(hv4 - 3)
hv5·(hv5 - 1)·(hv5 - 2)·(hv5 - 3)
(ip' - (ip + 1)·st0)
+ ((ip' - (ip + 2))·(st0·hv0 - 1)·(hv1 - 1))
+ ((ip' - (ip + 3))·(st0·hv0 - 1)·hv1)

Helper variable definitions for `skiz`

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

Instruction `call` + `d`

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

Description

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

Polynomials

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

Instruction `return`

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

Description

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

Polynomials

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

Instruction `recurse`

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

Description

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

Polynomials

jsp' - jsp
jso' - jso
jsd' - jsd
ip' - jsd

Instruction `recurse_or_return`

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

Description

If ST5 equals ST6, then ip in the next row equals jso in the current row.
If ST5 equals ST6, then jsp decrements by one.
If ST5 equals ST6, then hv0 in the current row is 0.
If ST5 is unequal to ST6, then hv0 in the current row is the inverse of (ST6 - ST5).
If ST5 is unequal to ST6, then ip in the next row is equal to jsd in the current row.
If ST5 is unequal to ST6, then jsp remains unchanged.
If ST5 is unequal to ST6, then jso remains unchanged.
If ST5 is unequal to ST6, then jsd remains unchanged.

Helper variable definitions for `recurse_or_return`

To help arithmetizing the equality check between ST5 and ST6, helper variable hv0 is the inverse-or-zero of (ST6 - ST5).

Instruction `assert`

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

Description

The current top of the stack st0 is 1.

Polynomials

st0 - 1

Instruction `halt`

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

Description

The instruction executed in the following step is instruction halt.

Polynomials

ci' - ci

Instruction `read_mem` + `n`

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

Description

The RAM pointer st0 is decremented by n.
If n is 1, then st1 is moved into st2
else if n is 2, then st1 is moved into st3
else if n is 3, then st1 is moved into st4
else if n is 4, then st1 is moved into st5
else if n is 5, then st1 is moved into st6.
If n is 1, then st2 is moved into st3
else if n is 2, then st2 is moved into st4
else if n is 3, then st2 is moved into st5
else if n is 4, then st2 is moved into st6
else if n is 5, then st2 is moved into st7.
If n is 1, then st3 is moved into st4
else if n is 2, then st3 is moved into st5
else if n is 3, then st3 is moved into st6
else if n is 4, then st3 is moved into st7
else if n is 5, then st3 is moved into st8.
If n is 1, then st4 is moved into st5
else if n is 2, then st4 is moved into st6
else if n is 3, then st4 is moved into st7
else if n is 4, then st4 is moved into st8
else if n is 5, then st4 is moved into st9.
If n is 1, then st5 is moved into st6
else if n is 2, then st5 is moved into st7
else if n is 3, then st5 is moved into st8
else if n is 4, then st5 is moved into st9
else if n is 5, then st5 is moved into st10.
If n is 1, then st6 is moved into st7
else if n is 2, then st6 is moved into st8
else if n is 3, then st6 is moved into st9
else if n is 4, then st6 is moved into st10
else if n is 5, then st6 is moved into st11.
If n is 1, then st7 is moved into st8
else if n is 2, then st7 is moved into st9
else if n is 3, then st7 is moved into st10
else if n is 4, then st7 is moved into st11
else if n is 5, then st7 is moved into st12.
If n is 1, then st8 is moved into st9
else if n is 2, then st8 is moved into st10
else if n is 3, then st8 is moved into st11
else if n is 4, then st8 is moved into st12
else if n is 5, then st8 is moved into st13.
If n is 1, then st9 is moved into st10
else if n is 2, then st9 is moved into st11
else if n is 3, then st9 is moved into st12
else if n is 4, then st9 is moved into st13
else if n is 5, then st9 is moved into st14.
If n is 1, then st10 is moved into st11
else if n is 2, then st10 is moved into st12
else if n is 3, then st10 is moved into st13
else if n is 4, then st10 is moved into st14
else if n is 5, then st10 is moved into st15.
If n is 1, then st11 is moved into st12
else if n is 2, then st11 is moved into st13
else if n is 3, then st11 is moved into st14
else if n is 4, then st11 is moved into st15
else if n is 5, then the op stack pointer grows by 5.
If n is 1, then st12 is moved into st13
else if n is 2, then st12 is moved into st14
else if n is 3, then st12 is moved into st15
else if n is 4, then the op stack pointer grows by 4
else if n is 5, then with the Op Stack Table accumulates st11 through st15.
If n is 1, then st13 is moved into st14
else if n is 2, then st13 is moved into st15
else if n is 3, then the op stack pointer grows by 3
else if n is 4, then the running product with the Op Stack Table accumulates st12 through st15
else if n is 5, then the running product with the RAM Table accumulates next row's st1 through st5.
If n is 1, then st14 is moved into st15
else if n is 2, then the op stack pointer grows by 2
else if n is 3, then the running product with the Op Stack Table accumulates st13 through st15
else if n is 4, then the running product with the RAM Table accumulates next row's st1 through st4
If n is 1, then the op stack pointer grows by 1
else if n is 2, then the running product with the Op Stack Table accumulates st14 and st15
else if n is 3, then the running product with the RAM Table accumulates next row's st1 through st3.
If n is 1, then the running product with the Op Stack Table accumulates st15
else if n is 2, then the running product with the RAM Table accumulates next row's st1 and st2.
If n is 1, then the running product with the RAM Table accumulates next row's st1.

Instruction `write_mem` + `n`

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

Description

The RAM pointer st0 is incremented by n.
If n is 1, then st2 is moved into st1
else if n is 2, then st3 is moved into st1
else if n is 3, then st4 is moved into st1
else if n is 4, then st5 is moved into st1
else if n is 5, then st6 is moved into st1.
If n is 1, then st3 is moved into st2
else if n is 2, then st4 is moved into st2
else if n is 3, then st5 is moved into st2
else if n is 4, then st6 is moved into st2
else if n is 5, then st7 is moved into st2.
If n is 1, then st4 is moved into st3
else if n is 2, then st5 is moved into st3
else if n is 3, then st6 is moved into st3
else if n is 4, then st7 is moved into st3
else if n is 5, then st8 is moved into st3.
If n is 1, then st5 is moved into st4
else if n is 2, then st6 is moved into st4
else if n is 3, then st7 is moved into st4
else if n is 4, then st8 is moved into st4
else if n is 5, then st9 is moved into st4.
If n is 1, then st6 is moved into st5
else if n is 2, then st7 is moved into st5
else if n is 3, then st8 is moved into st5
else if n is 4, then st9 is moved into st5
else if n is 5, then st10 is moved into st5.
If n is 1, then st7 is moved into st6
else if n is 2, then st8 is moved into st6
else if n is 3, then st9 is moved into st6
else if n is 4, then st10 is moved into st6
else if n is 5, then st11 is moved into st6.
If n is 1, then st8 is moved into st7
else if n is 2, then st9 is moved into st7
else if n is 3, then st10 is moved into st7
else if n is 4, then st11 is moved into st7
else if n is 5, then st12 is moved into st7.
If n is 1, then st9 is moved into st8
else if n is 2, then st10 is moved into st8
else if n is 3, then st11 is moved into st8
else if n is 4, then st12 is moved into st8
else if n is 5, then st13 is moved into st8.
If n is 1, then st10 is moved into st9
else if n is 2, then st11 is moved into st9
else if n is 3, then st12 is moved into st9
else if n is 4, then st13 is moved into st9
else if n is 5, then st14 is moved into st9.
If n is 1, then st11 is moved into st10
else if n is 2, then st12 is moved into st10
else if n is 3, then st13 is moved into st10
else if n is 4, then st14 is moved into st10
else if n is 5, then st15 is moved into st10.
If n is 1, then st12 is moved into st11
else if n is 2, then st13 is moved into st11
else if n is 3, then st14 is moved into st11
else if n is 4, then st15 is moved into st11
else if n is 5, then the op stack pointer shrinks by 5.
If n is 1, then st13 is moved into st12
else if n is 2, then st14 is moved into st12
else if n is 3, then st15 is moved into st12
else if n is 4, then the op stack pointer shrinks by 4
else if n is 5, then the running product with the Op Stack Table accumulates next row's st11 through st15.
If n is 1, then st14 is moved into st13
else if n is 2, then st15 is moved into st13
else if n is 3, then the op stack pointer shrinks by 3
else if n is 4, then the running product with the Op Stack Table accumulates next row's st12 through st15
else if n is 5, then the running product with the RAM Table accumulates st1 through st5.
If n is 1, then st15 is moved into st14
else if n is 2, then the op stack pointer shrinks by 2
else if n is 3, then the running product with the Op Stack Table accumulates next row's st13 through st15
else if n is 4, then the running product with the RAM Table accumulates st1 through st4.
If n is 1, then the op stack pointer shrinks by 1
else if n is 2, then the running product with the Op Stack Table accumulates next row's st14 and st15
else if n is 3, then the running product with the RAM Table accumulates st1 through st2.
If n is 1, then the running product with the Op Stack Table accumulates next row's st15
else if n is 2, then the running product with the RAM Table accumulates st1 and st1.
If n is 1, then the running product with the RAM Table accumulates st1.

Instruction `hash`

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

Description

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

Polynomials

st5' - st10
st6' - st11
st7' - st12
st8' - st13
st9' - st14
st10' - st15
op_stack_pointer' - op_stack_pointer + 5
RunningProductOpStackTable' - RunningProductOpStackTable·(🪤 - 🍋·clk - 🍊 - 🍉·op_stack_pointer' - 🫒·st15')
·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 1) - 🫒·st14')
·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 2) - 🫒·st13')
·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 3) - 🫒·st12')
·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 4) - 🫒·st11')

Instruction `assert_vector`

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

Description

st0 is equal to st5.
st1 is equal to st6.
st2 is equal to st7.
st3 is equal to st8.
st4 is equal to st9.
st10 is moved into st5.
st11 is moved into st6.
st12 is moved into st7.
st13 is moved into st8.
st14 is moved into st9.
st15 is moved into st10.
The op stack pointer shrinks by 5.
The running product with the Op Stack Table accumulates next row's st11 through st15.

Polynomials

st5 - st0
st6 - st1
st7 - st2
st8 - st3
st9 - st4
st5' - st10
st6' - st11
st7' - st12
st8' - st13
st9' - st14
st10' - st15
op_stack_pointer' - op_stack_pointer + 5
RunningProductOpStackTable' - RunningProductOpStackTable·(🪤 - 🍋·clk - 🍊 - 🍉·op_stack_pointer' - 🫒·st15')
·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 1) - 🫒·st14')
·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 2) - 🫒·st13')
·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 3) - 🫒·st12')
·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 4) - 🫒·st11')

Instruction `sponge_init`

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

Instruction `sponge_absorb`

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

Description

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

Polynomials

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

Instruction `sponge_absorb_mem`

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

Description

st0 is incremented by 10.

Instruction `sponge_squeeze`

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

Description

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

Polynomials

st10' - st0
st11' - st1
st12' - st2
st13' - st3
st14' - st4
st15' - st5
op_stack_pointer' - op_stack_pointer - 10
RunningProductOpStackTable' - RunningProductOpStackTable·(🪤 - 🍋·clk - 🍉·op_stack_pointer - 🫒·st15)
·(🪤 - 🍋·clk - 🍉·(op_stack_pointer + 1) - 🫒·st14)
·(🪤 - 🍋·clk - 🍉·(op_stack_pointer + 2) - 🫒·st13)
·(🪤 - 🍋·clk - 🍉·(op_stack_pointer + 3) - 🫒·st12)
·(🪤 - 🍋·clk - 🍉·(op_stack_pointer + 4) - 🫒·st11)
·(🪤 - 🍋·clk - 🍉·(op_stack_pointer + 5) - 🫒·st10)
·(🪤 - 🍋·clk - 🍉·(op_stack_pointer + 6) - 🫒·st9)
·(🪤 - 🍋·clk - 🍉·(op_stack_pointer + 7) - 🫒·st8)
·(🪤 - 🍋·clk - 🍉·(op_stack_pointer + 8) - 🫒·st7)
·(🪤 - 🍋·clk - 🍉·(op_stack_pointer + 9) - 🫒·st6)

Instruction `add`

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

Description

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

Polynomials

st0' - (st0 + st1)

Instruction `mul`

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

Description

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

Polynomials

st0' - st0·st1

Instruction `invert`

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

Description

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

Polynomials

st0'·st0 - 1

Instruction `eq`

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

Description

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

Polynomials

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

Helper variable definitions for `eq`

hv0 = inverse(rhs - lhs) if rhs ≠ lhs.
hv0 = 0 if rhs = lhs.

Instruction `split`

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

Description

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

Polynomials

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

Helper variable definitions for `split`

Given the high 32 bits of st0 as hi = st0 >> 32 and the low 32 bits of st0 as lo = st0 & 0xffff_ffff,

hv0 = (hi - (2^32 - 1)) if lo ≠ 0.
hv0 = 0 if lo = 0.

Instruction `lt`

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

Instruction `and`

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

Instruction `xor`

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

Instruction `log2floor`

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:

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

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

Description

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

Polynomials

st0 - st1·st1' - st0'
st2' - st2

Instruction `pop_count`

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

Instruction `xx_add`

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

Description

The result of adding st0 to st3 is moved into st0.
The result of adding st1 to st4 is moved into st1.
The result of adding st2 to st5 is moved into st2.
st6 is moved into st3.
st7 is moved into st4.
st8 is moved into st5.
st9 is moved into st6.
st10 is moved into st7.
st11 is moved into st8.
st12 is moved into st9.
st13 is moved into st10.
st14 is moved into st11.
st15 is moved into st12.
The op stack pointer shrinks by 3.
The running product with the Op Stack Table accumulates next row's st13 through st15.

Polynomials

st0' - (st0 + st3)
st1' - (st1 + st4)
st2' - (st2 + st5)
st3' - st6
st4' - st7
st5' - st8
st6' - st9
st7' - st10
st8' - st11
st9' - st12
st10' - st13
st11' - st14
st12' - st15
op_stack_pointer' - op_stack_pointer + 3
RunningProductOpStackTable' - RunningProductOpStackTable·(🪤 - 🍋·clk - 🍊 - 🍉·op_stack_pointer' - 🫒·st15')
·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 1) - 🫒·st14')
·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 2) - 🫒·st13')

Instruction `xx_mul`

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

Description

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

Polynomials

st0' - (st0·st3 - st2·st4 - st1·st5)
st1' - (st1·st3 + st0·st4 - st2·st5 + st2·st4 + st1·st5)
st2' - (st2·st3 + st1·st4 + st0·st5 + st2·st5)
st3' - st6
st4' - st7
st5' - st8
st6' - st9
st7' - st10
st8' - st11
st9' - st12
st10' - st13
st11' - st14
st12' - st15
op_stack_pointer' - op_stack_pointer + 3
RunningProductOpStackTable' - RunningProductOpStackTable·(🪤 - 🍋·clk - 🍊 - 🍉·op_stack_pointer' - 🫒·st15')
·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 1) - 🫒·st14')
·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 2) - 🫒·st13')

Instruction `x_invert`

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

Description

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

Polynomials

st0·st0' - st2·st1' - st1·st2' - 1
st1·st0' + st0·st1' - st2·st2' + st2·st1' + st1·st2'
st2·st0' + st1·st1' + st0·st2' + st2·st2'

Instruction `xb_mul`

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

Description

The result of multiplying the top of the stack with the X-Field element's coefficient for x^0 is moved into st0.
The result of multiplying the top of the stack with the X-Field element's coefficient for x^1 is moved into st1.
The result of multiplying the top of the stack with the X-Field element's coefficient for x^2 is moved into st2.
st4 is moved into st3.
st5 is moved into st4.
st6 is moved into st5.
st7 is moved into st6.
st8 is moved into st7.
st9 is moved into st8.
st10 is moved into st9.
st11 is moved into st10.
st12 is moved into st11.
st13 is moved into st12.
st14 is moved into st13.
st15 is moved into st14.
The op stack pointer shrinks by 3.
The running product with the Op Stack Table accumulates next row's st15.

Polynomials

st0' - st0·st1
st1' - st0·st2
st2' - st0·st3
st3' - st4
st4' - st5
st5' - stt
st6' - st7
st7' - st8
st8' - st9
st9' - st10
st10' - st11
st11' - st12
st12' - st13
st13' - st14
st14' - st15
op_stack_pointer' - op_stack_pointer + 1
RunningProductOpStackTable' - RunningProductOpStackTable·(🪤 - 🍋·clk - 🍊 - 🍉·op_stack_pointer' - 🫒·st15')

Instruction `read_io` + `n`

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

Description

If n is 1, the running evaluation for standard input accumulates next row's st0
else if n is 2, the running evaluation for standard input accumulates next row's st0 and st1
else if n is 3, the running evaluation for standard input accumulates next row's st0 through st2
else if n is 4, the running evaluation for standard input accumulates next row's st0 through st3
else if n is 5, the running evaluation for standard input accumulates next row's st0 through st4.

Polynomials

ind_1(hv3, hv2, hv1, hv0)·(RunningEvaluationStandardInput' - 🛏·RunningEvaluationStandardInput - st0')
+ ind_2(hv3, hv2, hv1, hv0)·(RunningEvaluationStandardInput' - 🛏·(🛏·RunningEvaluationStandardInput - st0') - st1')
+ ind_3(hv3, hv2, hv1, hv0)·(RunningEvaluationStandardInput' - 🛏·(🛏·(🛏·RunningEvaluationStandardInput - st0') - st1') - st2')
+ ind_4(hv3, hv2, hv1, hv0)·(RunningEvaluationStandardInput' - 🛏·(🛏·(🛏·(🛏·RunningEvaluationStandardInput - st0') - st1') - st2') - st3')
+ ind_5(hv3, hv2, hv1, hv0)·(RunningEvaluationStandardInput' - 🛏·(🛏·(🛏·(🛏·(🛏·RunningEvaluationStandardInput - st0') - st1') - st2') - st3') - st4')

Instruction `write_io` + `n`

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

Description

If n is 1, the running evaluation for standard output accumulates st0
else if n is 2, the running evaluation for standard output accumulates st0 and st1
else if n is 3, the running evaluation for standard output accumulates st0 through st2
else if n is 4, the running evaluation for standard output accumulates st0 through st3
else if n is 5, the running evaluation for standard output accumulates st0 through st4.

Polynomials

ind_1(hv3, hv2, hv1, hv0)·(RunningEvaluationStandardOutput' - 🧯·RunningEvaluationStandardOutput - st0)
+ ind_2(hv3, hv2, hv1, hv0)·(RunningEvaluationStandardOutput' - 🧯·(🧯·RunningEvaluationStandardOutput - st0) - st1)
+ ind_3(hv3, hv2, hv1, hv0)·(RunningEvaluationStandardOutput' - 🧯·(🧯·(🧯·RunningEvaluationStandardOutput - st0) - st1) - st2)
+ ind_4(hv3, hv2, hv1, hv0)·(RunningEvaluationStandardOutput' - 🧯·(🧯·(🧯·(🧯·RunningEvaluationStandardOutput - st0) - st1) - st2) - st3)
+ ind_5(hv3, hv2, hv1, hv0)·(RunningEvaluationStandardOutput' - 🧯·(🧯·(🧯·(🧯·(🧯·RunningEvaluationStandardOutput - st0) - st1) - st2) - st3) - st4)

Instruction `merkle_step`

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

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

Description

Helper variable hv5 is either 0 or 1.
st5 is shifted by 1 bit to the right. In other words, twice st5 in the next row plus hv5 equals st5 in the current row.

Helper variable definitions for `merkle_step`

hv0 through hv4 hold the sibling digest of the node indicated by st5, as read from the interface for non-deterministic input.
hv5 holds the result of st5 % 2, the Merkle tree node index's least significant bit, indicating whether it is a left or right node.

Instruction `merkle_step_mem`

Description

Stack element st6 does not change.
Stack element st7 is incremented by 5.
Helper variable hv5 is either 0 or 1.
st5 is shifted by 1 bit to the right. In other words, twice st5 in the next row plus hv5 equals st5 in the current row.
The running product with the RAM Table accumulates hv0 through hv4 using the (appropriately adjusted) RAM pointer held in st7.

Helper variable definitions for `merkle_step_mem`

hv0 through hv4 hold the sibling digest of the node indicated by st5, as read from RAM at the address held in st7.
hv5 holds the result of st5 % 2, the Merkle tree node index's least significant bit, indicating whether it is a left or right node.

Instruction `xx_dot_step`

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

Description

Store (RAM[st0], RAM[st0+1], RAM[st0+2]) in (hv0, hv1, hv2).
Store (RAM[st1], RAM[st1+1], RAM[st1+2]) in (hv3, hv4, hv5).
Add (hv0 + hv1·x + hv2·x²) · (hv3 + hv4·x + hv5·x²) into (st2, st3, st4)
Increase the pointers: st0 and st1 by 3 each.

Instruction `xb_dot_step`

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

Description

Store RAM[st0] in hv0.
Store (RAM[st1], RAM[st1+1], RAM[st1+2]) in (hv1, hv2, hv3).
Add hv0 · (hv1 + hv2·x + hv3·x²) into (st1, st2, st3)
Increase the pointers: st0 and st1 by 1 and 3, respectively.

Triton VM