Miden VM decoder AIR constraints

In this section we describe AIR constraints for Miden VM program decoder. These constraints enforce that the execution trace generated by the prover when executing a particular program complies with the rules described in the previous section.

To refer to decoder execution trace columns, we use the names shown on the diagram below (these are the same names as in the previous section). Additionally, we denote the register containing the value at the top of the stack as $s_0$.

We assume that the VM exposes a flag per operation which is set to $1$ when the operation is executed, and to $0$ otherwise. The notation for such flags is $f_{opname}$. For example, when the VM executes a PUSH operation, flag $f_{push} = 1$. All flags are mutually exclusive - i.e., when one flag is set to $1$ all other flags are set to $0$. The flags are computed based on values in op_bits columns.

AIR constraints for the decoder involve operations listed in the table below. For each operation we also provide the degree of the corresponding flag and the effect that the operation has on the operand stack (however, in this section we do not cover the constraints needed to enforce the correct transition of the operand stack).

Operation	Flag	Degree	Effect on stack
JOIN	$f_{join}$	5	Stack remains unchanged.
SPLIT	$f_{split}$	5	Top stack element is dropped.
LOOP	$f_{loop}$	5	Top stack element is dropped.
REPEAT	$f_{repeat}$	4	Top stack element is dropped.
SPAN	$f_{span}$	5	Stack remains unchanged.
RESPAN	$f_{respan}$	4	Stack remains unchanged.
DYN	$f_{dyn}$	5	Top stack element is dropped.
DYNCALL	$f_{dyncall}$	5	Top stack element is dropped.
CALL	$f_{call}$	4	Stack remains unchanged.
SYSCALL	$f_{syscall}$	4	Stack remains unchanged.
END	$f_{end}$	4	When exiting a loop block, top stack element is dropped; otherwise, the stack remains unchanged.
HALT	$f_{halt}$	4	Stack remains unchanged.
PUSH	$f_{push}$	5	An immediate value is pushed onto the stack.
EMIT	$f_{emit}$	7	Stack remains unchanged.

We also use the control flow flag $f_{ctrl}$ exposed by the VM, which is set to $1$ for the control-flow operations SPAN, JOIN, SPLIT, LOOP, END, REPEAT, RESPAN, HALT, DYN, DYNCALL, CALL, and SYSCALL (and $0$ otherwise). It has degree $5$.

As described previously, the general idea of the decoder is that the prover provides the program to the VM by populating some of cells in the trace non-deterministically. Values in these are then used to update virtual tables (represented via multiset checks) such as block hash table, block stack table etc. Transition constraints are used to ensure that the tables are updates correctly, and we also apply boundary constraints to enforce the correct initial and final states of these tables. One of these boundary constraints binds the execution trace to the hash of the program being executed. Thus, if the virtual tables were updated correctly and boundary constraints hold, we can be convinced that the prover executed the claimed program on the VM.

In the sections below, we describe constraints according to their logical grouping. However, we start out with a set of general constraints which are applicable to multiple parts of the decoder.

General constraints

When SPLIT or LOOP operation is executed, the top of the operand stack must contain a binary value:

$$(f_{split} + f_{loop}) \cdot (s_0^2 - s_0) = 0 \text{ | degree} = 7$$

When a DYN operation is executed, the second half of the hasher registers ($h_4,\dots,h_7$) must be set to $0$ (the first half holds the callee digest):

$$f_{dyn} \cdot h_i = 0 \text { for } i \in [4, 8) \text{ | degree} = 6$$

When REPEAT operation is executed, the value at the top of the operand stack must be $1$:

$$f_{repeat} \cdot (1 - s_0) = 0 \text{ | degree} = 5$$

Also, when REPEAT operation is executed, the value in $h_4$ column (the is_loop_body flag), must be set to $1$. This ensures that REPEAT operation can be executed only inside a loop:

$$f_{repeat} \cdot (1 - h_4) = 0 \text{ | degree} = 5$$

When RESPAN operation is executed, we need to make sure that the block ID is incremented by $32$:

$$f_{respan} \cdot (a' - a - 32) = 0 \text{ | degree} = 5$$

When END operation is executed and we are exiting a loop block (i.e., is_loop, value which is stored in $h_5$, is $1$), the value at the top of the operand stack must be $0$:

$$f_{end} \cdot h_5 \cdot s_0 = 0 \text{ | degree} = 6$$

Also, when END operation is executed and the next operation is REPEAT, values in $h_0, ..., h_4$ (the hash of the current block and the is_loop_body flag) must be copied to the next row:

$$f_{end} \cdot f_{repeat}' \cdot (h_i' - h_i) = 0 \text { for } i \in [0, 5) \text{ | degree} = 9$$

A HALT instruction can be followed only by another HALT instruction:

$$f_{halt} \cdot (1 - f_{halt}') = 0 \text{ | degree} = 8$$

When a HALT operation is executed, block address column must be $0$:

$$f_{halt} \cdot a = 0 \text{ | degree} = 5$$

Values in op_bits columns must be binary (i.e., either $1$ or $0$):

$$b_i^2 - b_i = 0 \text{ for } i \in [0, 7) \text{ | degree} = 2$$

We also use two extra columns ($e_0$, $e_1$) for degree reduction in the operation flag computation:

$$e_0 - b_6 \cdot (1 - b_5) \cdot b_4 = 0 \text{ | degree} = 4$$

$$e_1 - b_6 \cdot b_5 = 0 \text{ | degree} = 3$$

Finally, we enforce opcode-prefix constraints needed for flag construction. These eliminate unused opcode prefixes so that only valid op-code prefixes are allowed:

$$b_6 \cdot (1 - b_5) \cdot (1 - b_4) \cdot b_0 = 0 \text{ | degree} = 4$$

$$b_6 \cdot b_5 \cdot b_0 = 0 \text{ | degree} = 3$$

$$b_6 \cdot b_5 \cdot b_1 = 0 \text{ | degree} = 3$$

When the value in in_span column is set to $1$, control flow operations cannot be executed on the VM, but when in_span flag is $0$, only control flow operations can be executed on the VM:

$$1 - sp - f_{ctrl} = 0 \text{ | degree} = 5$$

Block hash computation constraints

As described previously, when the VM starts executing a new block, it also initiates computation of the block's hash. There are two separate methodologies for computing block hashes.

For join and split blocks, the hash is computed directly from the hashes of the block's children. The prover provides these child hashes non-deterministically by populating registers $h_0,..., h_7$. For loop blocks, only the loop body hash is provided in $h_0..h_3$ and the remaining registers $h_4..h_7$ are set to $0$ (padding to a full 8-element rate). For dyn, only the second half of the hasher registers ($h_4,\dots,h_7$) are forced to $0$, while the first half holds the callee digest read from memory; thus the input is not all zeros. The hasher is initialized using the hash chiplet, and we use the address of the hasher as the block's ID. The result of the hash is available $31$ rows down in the hasher table (i.e., at row with index equal to block ID plus $31$). We read the result from the hasher table at the time the END operation is executed for a given block.

For basic blocks, the hash is computed by absorbing a linear sequence of instructions (organized into operation groups and batches) into the hasher and then returning the result. The prover provides operation batches non-deterministically by populating registers $h_0, ..., h_7$. Similarly to other blocks, the hasher is initialized using the hash chiplet at the start of the block, and we use the address of the hasher as the ID of the first operation batch in the block. As we absorb additional operation batches into the hasher (by executing RESPAN operation), the batch address is incremented by $32$. This moves the "pointer" into the hasher table $32$ rows down with every new batch. We read the result from the hasher table at the time the END operation is executed for a given block.

Chiplets bus constraints

The decoder communicates with the hash chiplet via the chiplets bus. This works by dividing values of the multiset check column $b_{chip}$ by the values of operations providing inputs to or reading outputs from the hash chiplet. A constraint to enforce this would look as $b_{chip}' \cdot u = b_{chip}$, where $u$ is the value which defines the operation.

In constructing values for decoder bus requests, we use the hasher message format described in the hasher chiplet. For decoder requests, the node index is always $0$, so the message reduces to:

$$H(label, addr, state) = \alpha_0 + \alpha_1 \cdot label + \alpha_2 \cdot addr + \sum_{i=0}^{11} \alpha_{4+i} \cdot state_i$$

We use the following labels:

• $L_{init} = \text{LINEAR\_HASH\_LABEL} + 16$
• $L_{respan} = \text{LINEAR\_HASH\_LABEL} + 32$
• $L_{end} = \text{RETURN\_HASH\_LABEL} + 32$

Let $d = \sum_{i=0}^6(b_i \cdot 2^i)$ denote the opcode value, which is placed in the capacity domain lane (state index $9$).

To simplify constraint description, we define the following values:

$$h_{ctrl} = \alpha_0 + \alpha_1 \cdot L_{init} + \alpha_2 \cdot a' + \sum_{i=0}^7(\alpha_{4+i} \cdot h_i) + \alpha_{13} \cdot d$$ $$h_{span} = \alpha_0 + \alpha_1 \cdot L_{init} + \alpha_2 \cdot a' + \sum_{i=0}^7(\alpha_{4+i} \cdot h_i)$$ $$h_{respan} = \alpha_0 + \alpha_1 \cdot L_{respan} + \alpha_2 \cdot (a' - 1) + \sum_{i=0}^7(\alpha_{4+i} \cdot h_i)$$ $$h_{end} = \alpha_0 + \alpha_1 \cdot L_{end} + \alpha_2 \cdot (a + 31) + \sum_{i=0}^3(\alpha_{4+i} \cdot h_i)$$ $$h_{dyn} = \alpha_0 + \alpha_1 \cdot L_{init} + \alpha_2 \cdot a' + \alpha_{13} \cdot d$$ $$f_{ctrli} = f_{join} + f_{split} + f_{loop} \text{ | degree} = 5$$

In the above, $f_{ctrli}$ is set to $1$ when a control flow operation that signifies the initialization of a control block is being executed on the VM (only those control blocks that don't do any concurrent requests to the chiplets bus). Otherwise, it is set to $0$. An exception is made for the DYN, DYNCALL, CALL and SYSCALL operations, since although they initialize a control block, they also run another concurrent bus request, and so are handled separately.

Using the above variables, we define operation values as described below.

When a control block initializer operation (JOIN, SPLIT, LOOP) is executed, a new hasher is initialized and the contents of $h_0, ..., h_7$ are absorbed into the hasher, with the opcode value $d$ placed in the capacity domain lane.

$$u_{ctrli} = f_{ctrli} \cdot h_{ctrl} \text{ | degree} = 6$$

As mentioned previously, the value sent by the SYSCALL operation is defined separately, since in addition to communicating with the hash chiplet it must also send a kernel procedure access request to the kernel ROM chiplet. This value of this kernel procedure request is described by $k_{proc}$.

$$k_{proc} = \alpha_0 + \alpha_1 \cdot op_{krom} + \sum_{i=0}^3 (\alpha_{i + 2} \cdot h_i)$$

In the above, $op_{krom}$ is the unique operation label of the kernel procedure call operation. The values $h_0, h_1, h_2, h_3$ contain the root hash of the procedure being called, which is the procedure that must be requested from the kernel ROM chiplet.

$$u_{syscall} = f_{syscall} \cdot h_{ctrl} \cdot k_{proc} \text{ | degree} = 6$$

The above value sends both the hash initialization request and the kernel procedure access request to the chiplets bus when the SYSCALL operation is executed.

Similar to SYSCALL, CALL is handled separately, since in addition to communicating with the hash chiplet, it must also initialize the frame memory pointer (stored in memory at constant address fmpaddr with constant value fmpinit):

$$m_{fmpwrite} = \alpha_0 + \alpha_1 \cdot m_{writeele} + \alpha_2 \cdot ctx' + \alpha_3 \cdot fmpaddr + \alpha_4 \cdot clk + \alpha_5 \cdot fmpinit$$

In the above, $m_{fmpwrite}$ represents a "write element" memory request equivalent to mem[fmpaddr] = fmpinit (in pseudo-code) in the new memory context (i.e. the memory context of the callee). Currently $fmpaddr = 2^{32} - 1$, and $fmpinit = 2^{31}$.

$$u_{call} = f_{call} \cdot h_{ctrl} \cdot m_{fmpwrite} \text{ | degree} = 6$$

Similar to SYSCALL and CALL, DYN and DYNCALL are handled separately, since in addition to communicating with the hash chiplet they must also issue a memory read operation for the hash of the procedure being called.

$$h_{dynordyncall} = h_{dyn}$$ $$m_{dynordyncall} = \alpha_0 + \alpha_1 \cdot m_{readword} + \alpha_2 \cdot ctx + \alpha_3 \cdot s_0 + \alpha_4 \cdot clk + \sum_{i=0}^3(\alpha_{i + 5} \cdot h_i)$$ $$u_{dyn} = f_{dyn} \cdot h_{dynordyncall} \cdot m_{dynordyncall} \text{ | degree} = 7$$ $$u_{dyncall} = f_{dyncall} \cdot h_{dynordyncall} \cdot m_{dynordyncall} \cdot m_{fmpwrite} \text{ | degree} = 8$$

In the above, $h_{dynordyncall}$ is the control-block request with a zeroed hasher state, and $m_{dynordyncall}$ represents a memory word read request from address $s_0$, where the result is placed in the first half of the decoder hasher trace. Note that similar to CALL, DYNCALL also creates a new memory context, and hence must also initialize the fmp.

When SPAN operation is executed, a new hasher is initialized and contents of $h_0, ..., h_7$ are absorbed into the hasher. The chiplets-bus message uses only the rate lanes; capacity lanes (state indices $8..11$) are zeroed for this request:

$$u_{span} = f_{span} \cdot h_{span} \text{ | degree} = 6$$

When RESPAN operation is executed, contents of $h_0, ..., h_7$ (which contain the new operation batch) are absorbed into the hasher:

$$u_{respan} = f_{respan} \cdot h_{respan} \text{ | degree} = 5$$

When END operation is executed, the hash result is copied into registers $h_0, .., h_3$:

$$u_{end} = f_{end} \cdot h_{end} \text{ | degree} = 5$$

Using the above definitions, we can describe the constraint for computing block hashes as follows:

$$b_{chip}' \cdot (u_{ctrli} + u_{call} + u_{syscall} + u_{dyn} + u_{dyncall} + u_{span} + u_{respan} + u_{end} + \\ 1 - (f_{ctrli} + f_{call} + f_{syscall} + f_{dyn} + f_{dyncall} + f_{span} + f_{respan} + f_{end})) = b_{chip}$$

We need to add $1$ and subtract the sum of the relevant operation flags to ensure that when none of the flags is set to $1$, the above constraint reduces to $b_{chip}' = b_{chip}$.

The degree of this constraint is $9$.

Block stack table constraints

As described previously, block stack table keeps track of program blocks currently executing on the VM. Thus, whenever the VM starts executing a new block, an entry for this block is added to the block stack table. And when execution of a block completes, it is removed from the block stack table.

Adding and removing entries to/from the block stack table is accomplished as follows:

• To add an entry, we multiply the value in column $p_1$ by a value representing a tuple (blk, prnt, is_loop, ctx_next, b0_next, b1_next, fn_hash_next) . A constraint to enforce this would look as $p_1' = p_1 \cdot v$, where $v$ is the value representing the row to be added.
• To remove an entry, we divide the value in column $p_1$ by a value representing a tuple (blk, prnt, is_loop, ctx_next, b0_next, b1_next, fn_hash_next). A constraint to enforce this would look as $p_1' \cdot u = p_1$, where $u$ is the value representing the row to be removed.

Recall that the columns ctx_next, b0_next, b1_next, fn_hash_next are only set on CALL, SYSCALL, and their corresponding END block. Therefore, for simplicity, we will ignore them when documenting all other block types (such that their values are set to 0).

Before describing the constraints for the block stack table, we first describe how we compute the values to be added and removed from the table for each operation. In the below, for block start operations (JOIN, SPLIT, LOOP, SPAN) $a$ refers to the ID of the parent block, and $a'$ refers to the ID of the starting block. For END operation, the situation is reversed: $a$ is the ID of the ending block, and $a'$ is the ID of the parent block. For RESPAN operation, $a$ refers to the ID of the current operation batch, $a'$ refers to the ID of the next batch, and the parent ID for both batches is set by the prover non-deterministically in register $h_1$.

When JOIN operation is executed, row $(a', a, 0)$ is added to the block stack table:

$$v_{join} = f_{join} \cdot (\alpha_0 + \alpha_1 \cdot a' + \alpha_2 \cdot a + \alpha_3 \cdot 0) \text{ | degree} = 6$$

When SPLIT operation is executed, row $(a', a, 0)$ is added to the block stack table:

$$v_{split} = f_{split} \cdot (\alpha_0 + \alpha_1 \cdot a' + \alpha_2 \cdot a + \alpha_3 \cdot 0) \text{ | degree} = 6$$

When LOOP operation is executed, row $(a', a, 1)$ is added to the block stack table if the value at the top of the operand stack is $1$, and row $(a', a, 0)$ is added to the block stack table if the value at the top of the operand stack is $0$:

$$v_{loop} = f_{loop} \cdot (\alpha_0 + \alpha_1 \cdot a' + \alpha_2 \cdot a + \alpha_3 \cdot s_0) \text{ | degree} = 6$$

When SPAN operation is executed, row $(a', a, 0)$ is added to the block stack table:

$$v_{span} = f_{span} \cdot (\alpha_0 + \alpha_1 \cdot a' + \alpha_2 \cdot a + \alpha_3 \cdot 0) \text{ | degree} = 6$$

When RESPAN operation is executed, row $(a, h_1', 0)$ is removed from the block stack table, and row $(a', h_1', 0)$ is added to the table. The prover sets the value of register $h_1$ at the next row to the ID of the parent block:

$$u_{respan} = f_{respan} \cdot (\alpha_0 + \alpha_1 \cdot a + \alpha_2 \cdot h_1' + \alpha_3 \cdot 0) \text{ | degree} = 5 v_{respan} = f_{respan} \cdot (\alpha_0 + \alpha_1 \cdot a' + \alpha_2 \cdot h_1' + \alpha_3 \cdot 0) \text{ | degree} = 5$$

When a DYN operation is executed, row $(a', a, 0)$ is added to the block stack table:

$$v_{dyn} = f_{dyn} \cdot (\alpha_0 + \alpha_1 \cdot a' + \alpha_2 \cdot a + \alpha_3 \cdot 0) \text{ | degree} = 6$$

When a DYNCALL operation is executed, row $(a', a, 0, ctx, h_4, h_5, \mathrm{fnhash}[0..3])$ is added to the block stack table (here $h_4, h_5$ hold the post-shift stack depth and overflow address):

$$\begin{align*} v_{dyncall} &= f_{dyncall} \cdot (\alpha_0 + \alpha_1 \cdot a' + \alpha_2 \cdot a + \alpha_3 \cdot 0 + \alpha_4 \cdot ctx + \alpha_5 \cdot h_4 + \alpha_6 \cdot h_5 \\ &\quad + \alpha_7 \cdot \mathrm{fnhash}_0 + \alpha_8 \cdot \mathrm{fnhash}_1 + \alpha_9 \cdot \mathrm{fnhash}_2 + \alpha_{10} \cdot \mathrm{fnhash}_3) \text{ | degree} = 6 \end{align*}$$

When a CALL or SYSCALL operation is executed, row $(a', a, 0, ctx, b_0, b_1, \mathrm{fnhash}[0..3])$ is added to the block stack table:

$$\begin{align*} v_{callorsyscall} &= (f_{call} + f_{syscall}) \cdot (\alpha_0 + \alpha_1 \cdot a' + \alpha_2 \cdot a + \alpha_3 \cdot 0 + \alpha_4 \cdot ctx + \alpha_5 \cdot b_0 + \alpha_6 \cdot b_1 \\ &\quad + \alpha_7 \cdot \mathrm{fnhash}_0 + \alpha_8 \cdot \mathrm{fnhash}_1 + \alpha_9 \cdot \mathrm{fnhash}_2 + \alpha_{10} \cdot \mathrm{fnhash}_3) \text{ | degree} = 5 \end{align*}$$

When END operation is executed, how we construct the row will depend on whether the IS_CALL or IS_SYSCALL values are set (stored in registers $h_6$ and $h_7$ respectively). If they are not set, then row $(a, a', h_5)$ is removed from the block span table (where $h_5$ contains the is_loop flag); otherwise, row $(a ,a', 0, ctx', b_0', b_1', \mathrm{fnhash}'[0..3])$.

$$\begin{align*} u_{endnocall} &= \alpha_0 + \alpha_1 \cdot a + \alpha_2 \cdot a' + \alpha_3 \cdot h_5 \\ u_{endcall} &= u_{endnocall} + \alpha_4 \cdot ctx' + \alpha_5 \cdot b_0' + \alpha_6 \cdot b_1' \\ &\quad + \alpha_7 \cdot \mathrm{fnhash}_0' + \alpha_8 \cdot \mathrm{fnhash}_1' + \alpha_9 \cdot \mathrm{fnhash}_2' + \alpha_{10} \cdot \mathrm{fnhash}_3' \\ u_{end} &= f_{end} \cdot ((1 - h_6 - h_7) \cdot u_{endnocall} + (h_6 + h_7) \cdot u_{endcall} ) \text{ | degree} = 6 \end{align*}$$

Using the above definitions, we can describe the constraint for updating the block stack table as follows:

$$p_1' \cdot (u_{end} + u_{respan} + 1 - (f_{end} + f_{respan})) = p_1 \cdot (v_{join} + v_{split} + v_{loop} + v_{span} + v_{respan} + v_{dyn} + v_{dyncall} + v_{callorsyscall} + 1 - (f_{join} + f_{split} + f_{loop} + f_{span} + f_{respan} + f_{dyn} + f_{dyncall} + f_{call} + f_{syscall}))$$

We need to add $1$ and subtract the sum of the relevant operation flags from each side to ensure that when none of the flags is set to $1$, the above constraint reduces to $p_1' = p_1$.

The degree of this constraint is $9$.

In addition to the above transition constraint, we also need to impose boundary constraints against the $p_1$ column to make sure the first and the last values in the column are set to $1$. This enforces that the block stack table starts and ends in an empty state.

Block hash table constraints

As described previously, when the VM starts executing a new program block, it adds hashes of the block's children to the block hash table. And when the VM finishes executing a block, it removes the block's hash from the block hash table. This means that the block hash table gets updated when we execute the JOIN, SPLIT, LOOP, REPEAT, DYN, and END operations (executing SPAN operation does not affect the block hash table because a basic block has no children).

Adding and removing entries to/from the block hash table is accomplished as follows:

• To add an entry, we multiply the value in column $p_2$ by a value representing a tuple (prnt_id, block_hash, is_first_child, is_loop_body). A constraint to enforce this would look as $p_2' = p_2 \cdot v$, where $v$ is the value representing the row to be added.
• To remove an entry, we divide the value in column $p_2$ by a value representing a tuple (prnt_id, block_hash, is_first_child, is_loop_body). A constraint to enforce this would look as $p_2' \cdot u = p_2$, where $u$ is the value representing the row to be removed.

To simplify constraint descriptions, we define a generic message for a block hash entry:

$$m(parent, h_0..h_3, is\_first, is\_loop\_body) = \alpha_0 + \alpha_1 \cdot parent + \sum_{i=0}^3(\alpha_{i+2} \cdot h_i) + \alpha_6 \cdot is\_first + \alpha_7 \cdot is\_loop\_body$$

Using this, we define the left and right child messages for a JOIN as:

$$ch_1 = m(a', h_0..h_3, 1, 0) \qquad ch_2 = m(a', h_4..h_7, 0, 0)$$

Graphically, this looks like so:

Using the above variables, we define row values to be added to and removed from the block hash table as follows.

When JOIN operation is executed, hashes of both child nodes are added to the block hash table:

$$v_{join} = f_{join} \cdot ch_1 \cdot ch_2 \text{ | degree} = 7$$

When SPLIT operation is executed and the top of the stack is $1$, hash of the true branch is added to the block hash table; when the top of the stack is $0$, hash of the false branch is added:

$$v_{split} = f_{split} \cdot (s_0 \cdot ch_1 + (1 - s_0) \cdot ch_2) \text{ | degree} = 7$$

When LOOP operation is executed and the top of the stack is $1$, hash of the loop body is added to the block hash table (with is_loop_body = 1). When the top of the stack is $0$, no insertion is made:

$$v_{loop} = f_{loop} \cdot (s_0 \cdot m(a', h_0..h_3, 0, 1) + (1 - s_0)) \text{ | degree} = 7$$

When REPEAT operation is executed, hash of the loop body is added to the block hash table:

$v_{repeat} = f_{repeat} \cdot m(a', h_0..h_3, 0, 1) \text{ | } \text{degree} = 5$

When DYN, DYNCALL, CALL or SYSCALL operation is executed, the hash of the child is added to the block hash table. In all cases, this child is found in the first half of the decoder hasher state.

$$v_{allcalls} = (f_{dyn} + f_{dyncall} + f_{call} + f_{syscall}) \cdot m(a', h_0..h_3, 0, 0) \text{ | degree} = 6$$

When END operation is executed, the hash of the completed block is removed from the block hash table. We differentiate between the first and second child of a JOIN by looking at the next opcode: if the next operation is not END, REPEAT, or HALT, then this block is the first child and is_first_child = 1. The is_loop_body flag is read from $h_4$.

$$u_{end} = f_{end} \cdot m(a', h_0..h_3, 1 - (f_{end}' + f_{repeat}' + f_{halt}'), h_4) \text{ | } \text{degree} = 8$$

Using the above definitions, we can describe the constraint for updating the block hash table as follows:

$$p_2' \cdot (u_{end} + 1 - f_{end}) = p_2 \cdot (v_{join} + v_{split} + v_{loop} + v_{repeat} + v_{allcalls} + 1 - (f_{join} + f_{split} + f_{loop} + f_{repeat} + f_{dyn} + f_{dyncall} + f_{call} + f_{syscall}))$$

We need to add $1$ and subtract the sum of the relevant operation flags from each side to ensure that when none of the flags is set to $1$, the above constraint reduces to $p_2' = p_2$.

The degree of this constraint is $9$.

In addition to the above transition constraint, the last value in the column is $1$ (i.e., the block hash table is empty). The initial program-hash boundary constraint is planned but not enforced yet.

Basic block

Basic block constraints ensure proper decoding of basic blocks. In addition to the block stack table constraints and block hash table constraints described previously, decoding of basic blocks requires constraints described below.

In-span column constraints

The in_span column (denoted as $sp$) marks rows which execute non-control flow operations. This is enforced by the control-flow constraint $1 - sp - f_{ctrl} = 0$, so $sp = 1$ for non-control flow operations and $sp = 0$ otherwise. Semantically, this means $sp$ is 1 throughout basic blocks and 0 on control-flow rows. We do not separately constrain $sp' = sp$; the control-flow constraint pins $sp$ on every row, and the SPAN/RESPAN constraints below ensure the next row enters a basic block. Here $f_{ctrl}$ includes SPAN, JOIN, SPLIT, LOOP, END, REPEAT, RESPAN, HALT, DYN, DYNCALL, CALL, and SYSCALL. The op-group table and group_count constraints enforce that non-control rows can only appear inside spans, so $sp$ cannot switch to $1$ without a preceding SPAN/RESPAN.

We require that the VM starts outside a basic block. Since $sp = 1 - f_{ctrl}$ and $f_{ctrl}$ is binary, $sp$ is also binary.

$$sp = 0 \text{ on the first row}$$

When executing SPAN or RESPAN, the next value of $sp$ must be set to $1$:

$$f_{span} \cdot (1 - sp') = 0 \text{ | degree} = 6$$

$$f_{respan} \cdot (1 - sp') = 0 \text{ | degree} = 5$$

Since these flags are mutually exclusive, we can also merge them into one constraint:

$$(f_{span} + f_{respan}) \cdot (1 - sp') = 0 \text{ | degree} = 6$$

Block address constraints

When we are inside a basic block, values in block address columns (denoted as $a$) must remain the same. This can be enforced with the following constraint:

$$sp \cdot (a' - a) = 0 \text{ | degree} = 2$$

Notice that this constraint does not apply when we execute any of the control flow operations. For such operations, the prover sets the value of the $a$ column non-deterministically, except for the RESPAN operation. For the RESPAN operation the value in the $a$ column is incremented by $32$, which is enforced by a constraint described previously.

Notice also that this constraint implies that when the next operation is the END operation, the value in the $a$ column must also be copied over to the next row. This is exactly the behavior we want to enforce so that when the END operation is executed, the block address is set to the address of the current span batch.

Group count constraints

The group_count column (denoted as $gc$) is used to keep track of the number of operation groups which remains to be executed in a basic block.

In the beginning of a basic block (i.e., when SPAN operation is executed), the prover sets the value of $gc$ non-deterministically. This value is subsequently decremented according to the rules described below. By the time we exit the basic block (i.e., when END operation is executed), the value in $gc$ must be $0$.

The rules for decrementing values in the $gc$ column are as follows:

• The count cannot be decremented by more than $1$ in a single row.
• When an operation group is fully executed (which happens when $h_0 = 0$ inside a basic block), the count is decremented by $1$.
• When SPAN, RESPAN, or PUSH operations are executed, the count is decremented by $1$.

Note that these rules imply that the PUSH operation (or any operation with an immediate value) cannot be the last operation in an operation group (otherwise the count would have to be decremented by $2$).

To simplify the description of the constraints, we will define the following variable:

$$\Delta gc = gc - gc'$$

Using this variable, we can describe the constraints against the $gc$ column as follows:

Inside a basic block, group count can either stay the same or decrease by one:

$$sp \cdot \Delta gc \cdot (\Delta gc - 1) = 0 \text{ | degree} = 3$$

When group count is decremented inside a basic block, either $h_0$ must be $0$ (we consumed all operations in a group) or we must be executing an operation with an immediate value:

$$sp \cdot \Delta gc \cdot (1 - f_{imm})\cdot h_0 = 0 \text{ | degree} = 8$$

Notice that the above constraint does not preclude $f_{imm} = 1$ and $h_0 = 0$ from being true at the same time. If this happens, op group decoding constraints (described here) will force that the operation following the operation with an immediate value is a NOOP.

When executing a SPAN, a RESPAN, or an operation with an immediate value, group count must be decremented by $1$:

$$(f_{span} + f_{respan} + f_{imm}) \cdot (\Delta gc - 1) = 0 \text{ | degree} = 6$$

If the next operation is either an END or a RESPAN, group count must remain the same:

$$\Delta gc \cdot (f_{end}' + f_{respan}') = 0 \text{ | degree} = 5$$

When an END operation is executed, group count must be $0$:

$$f_{end} \cdot gc = 0 \text{ | degree} = 5$$

Op group decoding constraints

Inside a basic block, register $h_0$ is used to keep track of operations to be executed in the current operation group. The value of this register is set by the prover non-deterministically at the time when the prover executes a SPAN or a RESPAN operation, or when processing of a new operation group within a batch starts. The picture below illustrates this.

In the above:

• The prover sets the value of $h_0$ non-deterministically at row $0$. The value is set to an operation group containing operations op0 through op8.
• As we start executing the group, at every row we "remove" the least significant operation from the group. This can be done by subtracting opcode of the operation from the group, and then dividing the result by $2^7$.
• By row $9$ the group is fully executed. This decrements the group count and set op_index to $0$ (constraints against op_index column are described in the next section).
• At row $10$ we start executing the next group with operations op9 through op11. In this case, the prover populates $h_0$ with the group having its first operation (op9) already removed, and sets the op_bits registers to the value encoding op9.
• By row $12$ this group is also fully executed.

To simplify the description of the constraints, we define the following variables:

$$op = \sum_{i=0}^6 (b_i \cdot 2^i) f_{sgc} = sp \cdot sp' \cdot (1 - \Delta gc)$$

$op$ is just an opcode value implied by the values in op_bits registers. $f_{sgc}$ is a flag which is set to $1$ when the group count within a basic block does not change. We multiply it by $sp'$ to make sure the flag is $0$ when we are about to end decoding of an operation batch. Note that $f_{sgc}$ flag is mutually exclusive with $f_{span}$, $f_{respan}$, and $f_{imm}$ flags as these three operations decrement the group count.

Using these variables, we can describe operation group decoding constraints as follows:

When a SPAN, a RESPAN, or an operation with an immediate value is executed or when the group count does not change, the value in $h_0$ should be decremented by the value of the opcode in the next row.

$$(f_{span} + f_{respan} + f_{imm} + f_{sgc}) \cdot (h_0 - h_0' \cdot 2^7 - op') = 0 \text{ | degree} = 6$$

Notice that when the group count does change, and we are not executing $f_{span}$, $f_{respan}$, or $f_{imm}$ operations, no constraints are placed against $h_0$, and thus, the prover can populate this register non-deterministically.

When we are in a basic block and the next operation is END or RESPAN, the current value in $h_0$ column must be $0$.

$$sp \cdot (f_{end}' + f_{respan}') \cdot h_0 = 0 \text{ | degree} = 6$$

Op index constraints

The op_index column (denoted as $ox$) tracks index of an operation within its operation group. It is used to ensure that the number of operations executed per group never exceeds $9$. The index is zero-based, and thus, the possible set of values for $ox$ is between $0$ and $8$ (both inclusive).

To simplify the description of the constraints, we will define the following variables:

$$ng = \Delta gc - f_{imm} \Delta ox = ox' - ox$$

The value of $ng$ is set to $1$ when we are about to start executing a new operation group (i.e., group count is decremented but we did not execute an operation with an immediate value). Using these variables, we can describe the constraints against the $ox$ column as follows.

When executing SPAN or RESPAN operations the next value of op_index must be set to $0$:

$$(f_{span} + f_{respan}) \cdot ox' = 0 \text{ | degree} = 6$$

When starting a new operation group inside a basic block, the next value of op_index must be set to $0$. Note that we multiply by $sp$ to exclude the cases when the group count is decremented because of SPAN or RESPAN operations:

$$sp \cdot ng \cdot ox' = 0 \text{ | degree} = 6$$

When inside a basic block but not starting a new operation group, op_index must be incremented by $1$. Note that we multiply by $sp'$ to exclude the cases when we are about to exit processing of an operation batch (i.e., the next operation is either END or RESPAN):

$$sp \cdot sp' \cdot (1 - ng) \cdot (\Delta ox - 1) = 0 \text{ | degree} = 7$$

Values of op_index must be in the range $[0, 8]$.

$$\prod_{i=0}^{8}(ox - i) = 0 \text{ | degree} = 9$$

Op batch flags constraints

Operation batch flag columns (denoted $bc_0$, $bc_1$, and $bc_2$) are used to specify how many operation groups are present in an operation batch. This is relevant for the last batch in a basic block (or the first batch if there is only one batch in a block) as all other batches should be completely full (i.e., contain 8 operation groups).

These columns are used to define the following 4 flags:

• $f_{g8} = bc_0$: there are 8 operation groups in the batch.
• $f_{g4} = (1 - bc_0) \cdot bc_1 \cdot (1 - bc_2)$: there are 4 operation groups in the batch.
• $f_{g2} = (1 - bc_0) \cdot (1 - bc_1) \cdot bc_2$: there are 2 operation groups in the batch.
• $f_{g1} = (1 - bc_0) \cdot bc_1 \cdot bc_2$: there is only 1 operation groups in the batch.

Notice that the degree of $f_{g8}$ is $1$, while the degree of the remaining flags is $3$.

These flags can be set to $1$ only when we are executing SPAN or RESPAN operations as this is when the VM starts processing new operation batches. Also, for a given flag we need to ensure that only the specified number of operations groups are present in a batch. This can be done with the following constraints.

All batch flags must be binary:

$$bc_i^2 - bc_i = 0 \text{ for } i \in [0, 3) \text{ | degree} = 2$$

When SPAN or RESPAN operations is executed, one of the batch flags must be set to $1$.

$$(f_{span} + f_{respan}) - (f_{g1} + f_{g2} + f_{g4} + f_{g8}) = 0 \text{ | degree} = 5$$

When neither SPAN nor RESPAN is executed, all batch flags must be set to $0$.

$$(1 - (f_{span} + f_{respan})) \cdot (bc_0 + bc_1 + bc_2) = 0 \text{ | degree} = 6$$

When we have at most 4 groups in a batch, registers $h_4, ..., h_7$ should be set to $0$'s.

$$(f_{g1} + f_{g2} + f_{g4}) \cdot h_i = 0 \text{ for } i \in [4, 8) \text{ | degree} = 4$$

When we have at most 2 groups in a batch, registers $h_2$ and $h_3$ should also be set to $0$'s.

$$(f_{g1} + f_{g2}) \cdot h_i = 0 \text{ for } i \in 2, 3 \text{ | degree} = 4$$

When we have at most 1 groups in a batch, register $h_1$ should also be set to $0$.

$$f_{g1} \cdot h_1 = 0 \text{ | degree} = 4$$

Op group table constraints

Op group table is used to ensure that all operation groups in a given batch are consumed before a new batch is started (i.e., via a RESPAN operation) or the execution of a basic block is complete (i.e., via an END operation). The op group table is updated according to the following rules:

• When a new operation batch is started, we add groups from this batch to the table. To add a group to the table, we multiply the value in column $p_3$ by a value representing a tuple (batch_id, group_pos, group). A constraint to enforce this would look as $p_3' = p_3 \cdot v$, where $v$ is the value representing the row to be added. Depending on the batch, we may need to add multiple groups to the table (i.e., $p_3' = p_3 \cdot v_1 \cdot v_2 \cdot v_3 ...$). Flags $f_{g1}$, $f_{g2}$, $f_{g4}$, and $f_{g8}$ are used to define how many groups to add.
• When a new operation group starts executing or when an immediate value is consumed, we remove the corresponding group from the table. To do this, we divide the value in column $p_3$ by a value representing a tuple (batch_id, group_pos, group). A constraint to enforce this would look as $p_3' \cdot u = p_3$, where $u$ is the value representing the row to be removed.

To simplify constraint descriptions, we first define variables representing the rows to be added to and removed from the op group table.

When a SPAN or a RESPAN operation is executed, we compute the values of the rows to be added to the op group table as follows:

$$v_i = \alpha_0 + \alpha_1 \cdot a' + \alpha_2 \cdot (gc - i) + \alpha_3 \cdot h_{i} \text{ | degree} = 1$$

Where $i \in [1, 8)$. Thus, $v_1$ defines row value for group in $h_1$, $v_2$ defines row value for group $h_2$ etc. Note that batch address column comes from the next row of the block address column ($a'$).

We compute the value of the row to be removed from the op group table as follows:

$$u = \alpha_0 + \alpha_1 \cdot a + \alpha_2 \cdot gc + \alpha_3 \cdot ((h_0' \cdot 2^7 + op') \cdot (1 - f_{imm}) + s_0' \cdot f_{push}) \text{ | degree} = 7$$

In the above, the value of the group is computed as $(h_0' \cdot 2^7 + op') \cdot (1 - f_{imm}) + s_0' \cdot f_{push}$. This basically says that when we execute a PUSH operation we need to remove the immediate value from the table. This value is at the top of the stack (column $s_0$) in the next row. However, when we are not executing a PUSH operation, the value to be removed is an op group value which is a combination of values in $h_0$ and op_bits columns (also in the next row). Note also that value for batch address comes from the current value in the block address column ($a$), and the group position comes from the current value of the group count column ($gc$).

We also define a flag which is set to $1$ when a group needs to be removed from the op group table.

$$f_{dg} = sp \cdot \Delta gc \text{ | degree} = 2$$

The above says that we remove groups from the op group table whenever group count is decremented. We multiply by $sp$ to exclude the cases when the group count is decremented due to SPAN or RESPAN operations.

Using the above variables together with flags $f_{g1}$, $f_{g2}$, $f_{g4}$, $f_{g8}$ defined in the previous section, we describe the constraint for updating op group table as follows:

$$p_3' \cdot (f_{dg} \cdot u + 1 - f_{dg}) = p_3 \cdot (f_{g1} + f_{g2} \cdot v_1 + f_{g4} \cdot \prod_{i=1}^3 v_i + f_{g8} \cdot (\prod_{i=1}^7 v_i) + 1 - (f_{span} + f_{respan}))$$

The above constraint specifies that:

• When SPAN or RESPAN operations are executed, we add between $0$ and $7$ groups to the op group table; else, leave $p3$ untouched.
• When group count is decremented inside a basic block, we remove a group from the op group table; else, leave $p3'$ untouched.

The degree of this constraint is $9$.

In addition to the above transition constraint, we also need to impose boundary constraints against the $p_3$ column to make sure the first and the last value in the column is set to $1$. This enforces that the op group table table starts and ends in an empty state.