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	Stack remains unchanged.
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 operation is executed, the top of the operand stack must contain a binary value:

$$f_{split} \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$$

A REPEAT operation requires $1$ at the top of the operand stack:

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

On each transition, REPEAT must follow an END whose $h_4$ marks the completed node as a loop body. The block-hash relation authenticates this flag on the END row:

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

LOOP cannot transition directly to END; that would skip the body if its body-hash multiplicity were zero:

$$f_{loop} \cdot f_{end}' = 0 \text{ | degree} = 9$$

The first row has no predecessor, so it cannot be a REPEAT operation:

$$f_{repeat} = 0 \text{ on the first row}$$

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

$$f_{respan} \cdot (a' - a - 2) = 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$$

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} = 3$$

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

Since $e_0$ selects prefix 101, $b_6 - e_0$ selects prefixes 100 and 11. The two terms below select disjoint opcode groups: the first forces $b_0 = 0$ for prefixes 100 and 11, and the second rejects opcode $95$ under prefix 101:

$$(b_6 - e_0 + e_0 \cdot b_3 \cdot b_2 \cdot b_1) \cdot b_0 = 0 \text{ | degree} = 5$$

Prefix 11 also requires $b_1 = 0$:

$$e_1 \cdot b_1 = 0 \text{ | degree} = 2$$

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 controller input row as the block's ID. The result of the hash is then available in the paired controller output row at block ID plus $1$, and we read that result when the END operation is executed for the 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 first controller input row as the ID of the first operation batch in the block. As we absorb additional operation batches into the hasher (by executing RESPAN), the next batch starts at the next controller input row, so the batch address is incremented by $2$. We read the result from the controller output row corresponding to the final batch when the END operation is executed for the 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' + \sum_{i=0}^7(\alpha_{4+i} \cdot h_i)$$ $$h_{end} = \alpha_0 + \alpha_1 \cdot L_{end} + \alpha_2 \cdot (a + 1) + \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 uses one logical block-stack relation with two authenticated entry kinds:

• A continuation carries (blk, prnt, is_loop).
• A caller frame carries (blk, prnt, caller_ctx, caller_stack_depth, caller_overflow_addr, caller_fn_hash). In the common encoded layout its loop-marker slot is a constant zero; a caller frame cannot also be a LOOP continuation.

Both kinds use the same block-stack bus prefix $\alpha_B$. Payload slot $i$ contributes $\beta^i t_i$. Slot 10 is an explicit entry-kind tag: zero for a continuation and one for a caller frame, contributing $\beta^{10}$ only to the latter. Thus a continuation is not a zero-padded caller frame, and the two cannot collide when all saved caller-state fields are zero. JOIN, SPLIT, LOOP, SPAN, RESPAN, and DYN use continuation entries. CALL, DYNCALL, and SYSCALL use caller-frame entries. The matching END must consume the same authenticated kind.

Before describing the constraints, we describe the messages added to and removed from the relation. For compactness, throughout this block-stack section we write $\alpha_i = \beta^{i-1}$ for $i \ge 1$. The formulas display each opcode gate multiplied by its encoded denominator to make polynomial degrees visible. The lookup argument supplies the gate and denominator separately and contributes $f/d$ for an addition or $-f/d$ for a removal.

For block-start operations (JOIN, SPLIT, LOOP, SPAN), $a$ is the parent block ID and $a'$ is the starting block ID. For END, $a$ is the ending block ID and $a'$ is its parent. For RESPAN, $a$ is the current operation-batch ID, $a'$ is the next batch ID, and $h_1'$ supplies their common parent ID.

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

$$v_{join} = f_{join} \cdot (\alpha_B + \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_B + \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. Because LOOP has do-while semantics, the body is always entered, so the is_loop slot is unconditionally $1$:

$$v_{loop} = f_{loop} \cdot (\alpha_B + \alpha_1 \cdot a' + \alpha_2 \cdot a + \alpha_3) \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_B + \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_B + \alpha_1 \cdot a + \alpha_2 \cdot h_1' + \alpha_3 \cdot 0) \text{ | degree} = 5 v_{respan} = f_{respan} \cdot (\alpha_B + \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_B + \alpha_1 \cdot a' + \alpha_2 \cdot a + \alpha_3 \cdot 0) \text{ | degree} = 6$$

When a DYNCALL operation is executed, caller frame $(a', a, 0, ctx, h_4, h_5, \mathrm{fnhash}[0..3])$ is added to the block stack table. Here $h_4$ is constrained to the caller's post-shift stack depth $b_0 - f_{ov}$. The overflow relation pins $h_5$ to the post-shift overflow address when overflow is non-empty, and a direct constraint pins it to zero when overflow is empty:

$$\begin{align*} v_{dyncall} &= f_{dyncall} \cdot (\alpha_B + \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 + \alpha_{11}) \text{ | degree} = 6 \end{align*}$$

When a CALL or SYSCALL operation is executed, caller frame $(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_B + \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 + \alpha_{11}) \text{ | degree} = 5 \end{align*}$$

When END executes, $\ell = h_5$ indicates a LOOP continuation and $t = h_6$ indicates that the operation restores a caller frame. Both selectors are constrained to be boolean and mutually exclusive, while $h_7$ is fixed to zero. If $t=0$, the operation removes continuation $(a, a', \ell)$. If $t=1$, it removes caller frame $(a, a', 0, ctx', b_0', b_1', \mathrm{fnhash}'[0..3])$.

$$f_{end} \cdot \ell \cdot (\ell - 1) = 0, \qquad f_{end} \cdot t \cdot (t - 1) = 0, \qquad f_{end} \cdot h_7 = 0, \qquad f_{end} \cdot \ell \cdot t = 0$$

The booleanity and mutual-exclusion constraints have degree $6$; the $h_7$ zeroing constraint has degree $5$.

$$\begin{align*} u_{continuation} &= \alpha_B + \alpha_1 \cdot a + \alpha_2 \cdot a' + \alpha_3 \cdot \ell \\ u_{caller\_frame} &= \alpha_B + \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' + \alpha_{11} \\ u_{end} &= f_{end} \cdot ((1 - t) \cdot u_{continuation} + t \cdot u_{caller\_frame} ) \text{ | degree} = 6 \end{align*}$$

The lookup argument contributes $f/d$ for every add and $-f/d$ for every remove. It groups the mutually exclusive opcode branches and cross-multiplies their denominators. Summed across the trace, the block-stack contributions must be zero, proving multiset equality between inserted and removed tagged messages. The compiled constraint has degree $9$.

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, DYN, DYNCALL, CALL, SYSCALL, and END operations (executing SPAN operation does not affect the block hash table because a basic block has no children). REPEAT re-enters a loop body that the LOOP operation already accounted for, so it does not add an entry of its own.

The block-hash relation is part of a LogUp lookup column. Each insertion contributes $f/d$ and each removal contributes $-f/d$, where $f$ is the operation flag and $d$ encodes the entry. Define the denominator for one block-hash entry as:

$$d(parent, h_0..h_3, is\_first, is\_loop\_body) = \alpha_{block\_hash} + \sum_{i=0}^3 \beta^i h_i + \beta^4 parent + \beta^5 is\_first + \beta^6 is\_loop\_body.$$

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

$$d_{left} = d(a', h_0..h_3, 1, 0) \qquad d_{right} = d(a', h_4..h_7, 0, 0)$$

Graphically, this looks like so:

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

$$L_{join} = f_{join}\left(\frac{1}{d_{left}} + \frac{1}{d_{right}}\right).$$

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:

$$L_{split} = \frac{f_{split}}{d\left( a',\; s_0 h_0 + (1-s_0)h_4,\ldots,s_0 h_3 + (1-s_0)h_7,\; 0,\; 0 \right)}.$$

When LOOP operation is executed, its row contributes the loop-body hash with is_loop_body = 1 and multiplicity $gc$, the value of the group_count column. The lookup balance equates $gc$ with the number of body END rows that return to this loop instance. For an honestly executed do-while loop this count is at least one; the LOOP-to-END adjacency constraint prevents a malicious trace from skipping the body with a zero count. A single LOOP row therefore accounts for every iteration:

$$L_{loop} = \frac{gc \cdot f_{loop}}{d(a', h_0..h_3, 0, 1)}.$$

REPEAT does not add anything to the block hash table. Were it to add the digest supplied on its own row, a forged body END could be cancelled by the REPEAT that follows it, and the loop body executed by an iteration would no longer have to be the body that LOOP committed to.

Note that group_count is reused here: on LOOP rows it carries this multiplicity rather than a number of operation groups. The op group table is unaffected because control-flow rows have in_span = 0.

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.

$$L_{allcalls} = \frac{f_{dyn} + f_{dyncall} + f_{call} + f_{syscall}} {d(a', h_0..h_3, 0, 0)}.$$

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, RESPAN, or HALT, then this block is the first child and is_first_child = 1. RESPAN is included defensively — no single constraint forbids END → RESPAN, so excluding it would let an adversarial trace inject a false-positive is_first_child = 1. The is_loop_body flag is read from $h_4$.

$$L_{end} = -\frac{f_{end}} {d(a', h_0..h_3, 1 - (f_{end}' + f_{repeat}' + f_{respan}' + f_{halt}'), h_4)}.$$

The lookup builder combines these terms with the op-group interactions that share the column and cross-multiplies the active denominators. The resulting transition constraint has degree $9$. A boundary contribution inserts $(parent=0, child\_hash=program\_hash, 0, 0)$, which balances the root block's END removal and binds the relation to the claimed program hash.

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. The transition constraints below enforce the legal state transitions into and out of basic blocks. Here $f_{ctrl}$ includes SPAN, JOIN, SPLIT, LOOP, END, REPEAT, RESPAN, HALT, DYN, DYNCALL, CALL, and SYSCALL.

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}$$

On each transition, SPAN and RESPAN are followed by an in-span row. An in-span row remains inside unless the next operation is END or RESPAN:

$$sp' = f_{span} + f_{respan} + sp \cdot (1 - f_{end}' - f_{respan}')$$

The first-row constraint above handles the start of the trace separately from this transition rule.

Block address constraints

When we are inside a basic block, values in block address columns (denoted as $a$) must remain the same. The same is true when executing REPEAT, which re-enters the same loop parent for another body iteration. This can be enforced with the following constraint:

$$(sp + f_{repeat}) \cdot (a' - a) = 0 \text{ | degree} = 5$$

Notice that this constraint does not apply when we execute most control flow operations. For such operations, the prover sets the value of the $a$ column non-deterministically, except for the RESPAN and REPEAT operations. For the RESPAN operation the value in the $a$ column is incremented by $2$, 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.