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 following names (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$.

Columns	Registers
$0$	$a$
$1$--$7$	$b_0, \ldots, b_6$
$8$--$15$	$h_0, \ldots, h_7$
$16$	$sp$
$17$	$gc$
$18$	$ox$
$19$	full_batch
$20$	batch_size_code
$21$--$22$	$e_0, e_1$

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 prover supplies parts of the program by populating trace cells non-deterministically. Typed LogUp messages bind those values to the block hash, block stack, and op-group virtual tables. Local transition constraints select the required insertions and removals, while lookup closure and the program-hash boundary contribution bind the execution trace to the claimed program.

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 $1$:

$$f_{respan} \cdot (a' - a - 1) = 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 block). For dyn, the first half holds the callee digest read from memory and the second half of the hasher registers ($h_4,\dots,h_7$) is constrained to $0$; the digest itself may be the zero word. The callee digest participates in the memory and block-hash messages, while the domain-separated DYN hash request uses an all-zero input block. The hasher is initialized using the hash controller, and we use the controller-row address as the block's ID. A controller row overlays both the compression input and its output chaining value; for these framed block-hash operations, that value is the block digest read by END at the same address.

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 controller at the start of the block, and we use the address of the first controller 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 uses the next controller row, so the batch address is incremented by $1$. We read the result from that final controller row when the END operation is executed for the block.

Chiplets bus constraints

The decoder communicates with the hash, memory, and kernel-ROM chiplets through typed LogUp messages. Each decoder request has multiplicity $-1$; the owning chiplet supplies the matching message with positive multiplicity. The shared LogUp recurrence and cross-AIR closure are described in the linked overview.

In constructing values for decoder bus requests, we use the typed hasher message format described in the hasher chiplet. Let $P_k$ be the domain-separated prefix for message kind $k$. A message is reduced as

$$H_k(addr, node, payload) = P_k + addr + \beta \cdot node + \sum_{i=0}^{|payload|-1} \beta^{i+2} \cdot payload_i.$$

The message kind selects a distinct prefix for a full-state initialization, next-block absorption, or four-Felt result/CV return. Decoder block-hash messages use node index zero. Let $d = \sum_{i=0}^6(b_i \cdot 2^i)$ denote the opcode value. Let $CV(d)$ denote the Eidos two-to-one chaining word derived from that opcode, and let $CV_{span}(gc)$ denote the basic-block chaining word derived from its logical operation-group count.

To simplify constraint description, we define the following values:

$$h_{ctrl} = H_{init}(a', 0, [h_0,\ldots,h_7,CV(d)])$$ $$h_{span} = H_{init}(a', 0, [h_0,\ldots,h_7,CV_{span}(gc)])$$ $$h_{respan} = H_{absorb}(a', 0, [h_0,\ldots,h_7])$$ $$h_{end} = H_{return}(a, 0, [h_0,\ldots,h_3])$$ $$h_{dyn} = H_{init}(a', 0, [0,\ldots,0,CV(d)])$$

For the other typed chiplet messages below, write

$$K_{call}(q) = P_{kernel\_call} + \sum_{i=0}^{3}\beta^i q_i$$

and

$$M_k(ctx, addr, clk, p) = P_k + ctx + \beta addr + \beta^2 clk + \sum_{i=0}^{|p|-1}\beta^{i+3}p_i.$$ $$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.

When a control block initializer (JOIN, SPLIT, or LOOP) is executed, the decoder removes $h_{ctrl}$. The opcode-derived Eidos chaining word domain-separates the new hash.

SYSCALL removes both $h_{ctrl}$ and the following kernel-ROM request:

$$k_{proc} = K_{call}([h_0,\ldots,h_3])$$

The values $h_0, h_1, h_2, h_3$ contain the root hash of the procedure being called.

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} = M_{write\_element}(ctx', fmpaddr, clk, [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). The VM uses $fmpaddr = 2^{32} - 2$ and $fmpinit = 2^{31}$.

CALL removes $h_{ctrl}$ and $m_{fmpwrite}$ as two separate interactions.

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.

$$m_{dynordyncall} = M_{read\_word}(ctx, s_0, clk, [h_0,\ldots,h_3])$$

DYN removes $h_{dyn}$ and $m_{dynordyncall}$; DYNCALL additionally removes $m_{fmpwrite}$. The hash request carries an all-zero block and the opcode-derived chaining word, while $m_{dynordyncall}$ binds the callee digest in $h_0,\ldots,h_3$ to the memory word at $s_0$. $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 is executed, a new hasher is initialized and the contents of $h_0, ..., h_7$ are absorbed into it. The input CV is $CV_{span}(gc)$, which binds the logical operation-group count. The decoder removes $h_{span}$ on that row.

When RESPAN is executed, the contents of $h_0, ..., h_7$ (which contain the new operation batch) are absorbed into the hasher. The decoder removes $h_{respan}$ on that row.

When END is executed, the hash result is copied into registers $h_0, .., h_3$. The decoder removes $h_{end}$ on that row. Together, these operation-gated negative contributions require the hasher, memory, and kernel-ROM traces to provide every requested typed message.

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.

The BlockStackTable message has two tagged variants. A continuation is $S_c(block,parent,is\_loop)$; a caller frame is $S_f(block,parent,ctx,b_0,b_1,fn\_hash)$. The caller-frame tag prevents its encoding from colliding with a continuation whose saved payload is zero. Operation flags gate these signed interactions:

• JOIN, SPLIT, SPAN, and DYN add $S_c(a',a,0)$.
• LOOP adds $S_c(a',a,1)$. Its do-while semantics make is_loop unconditionally one.
• CALL and SYSCALL add $S_f(a',a,ctx,b_0,b_1,fn\_hash)$, saving the caller state.
• DYNCALL adds $S_f(a',a,ctx,h_4,h_5,fn\_hash)$; $h_4$ and $h_5$ hold the post-shift stack depth and overflow address.
• RESPAN removes $S_c(a,h'_1,0)$ and adds $S_c(a',h'_1,0)$, replacing the current batch ID while preserving its parent.
• END removes a continuation or a caller frame according to its entry-kind selectors.

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 $S_c(a,a',\ell)$. If $t=1$, it removes $S_f(a,a',ctx',b'_0,b'_1,fn\_hash')$, binding the restored caller state to the saved entry.

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

Adds have multiplicity $+1$ and removals have multiplicity $-1$. LogUp closure requires every completed block to cancel the entry created when that block began.

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. When the VM finishes executing a block, it removes the block's hash from the table. The table is therefore updated by JOIN, SPLIT, LOOP, DYN, DYNCALL, CALL, SYSCALL, and END. SPAN does not affect the table because a basic block has no children.

Define the typed BlockHashTable message

$$B(hash,parent,is\_first,is\_loop\_body),$$

whose encoded payload is [hash[0..4], parent, is_first, is_loop_body]. The two JOIN children are

$$B([h_0,\ldots,h_3],a',1,0) \quad\text{and}\quad B([h_4,\ldots,h_7],a',0,0).$$

Graphically, this looks like so:

Operation flags gate the following positive contributions:

• JOIN adds both messages above.
• SPLIT adds the first message when $s_0=1$ and the second when $s_0=0$.
• LOOP adds $B([h_0,\ldots,h_3],a',0,1)$ with multiplicity group_count, the number of body executions. Its do-while semantics require at least one body execution. REPEAT adds no block-hash entry; each body END must remove a copy of the hash committed by LOOP.
• DYN, DYNCALL, CALL, and SYSCALL add $B([h_0,\ldots,h_3],a',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$.

Thus, END removes

$$B([h_0,\ldots,h_3],a',1-(f'_{end}+f'_{repeat}+f'_{respan}+f'_{halt}),h_4).$$

Adds have multiplicity $+1$ and the END removal has multiplicity $-1$. The verifier also adds $B(program\_hash,0,0,0)$ as a boundary contribution. At the root END, the local constraints reduce the removal to that same message, binding the decoded execution to the public 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$$

This preservation constraint covers in-span rows and REPEAT. For the remaining control-flow operations, the prover supplies the next block address subject to their operation-specific constraints. In particular, RESPAN increments $a$ by $1$, as specified above.

When an in-span row is followed by END, this constraint copies $a$ into the END row, keeping 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 encoding constraints

The full_batch and batch_size_code columns specify how many operation groups are present in an operation batch. Let $f$ denote full_batch, let $t$ denote batch_size_code, and let $A = f_{span} + f_{respan}$. The valid encodings are:

Encoding $(f, t)$	Meaning
$(1, 0)$	8 groups
$(0, 1)$	4 groups
$(0, -1)$	2 groups
$(0, 0)$ with $A = 1$	1 group
$(0, 0)$ with $A = 0$	Inactive row

The following constraints restrict the pair to these encodings. The two inactive-row constraints directly pin each committed value to zero when the encoding is inactive.

$$f(f - 1) = 0 \text{ | degree} = 2$$

$$t(t - 1)(t + 1) = 0 \text{ | degree} = 3$$

$$f \cdot t = 0 \text{ | degree} = 2$$

$$(1 - A) \cdot f = 0 \text{ | degree} = 6$$

$$(1 - A) \cdot t = 0 \text{ | degree} = 6$$

The four batch-size selectors are derived as follows:

• $f_{g8} = f$.
• $f_{g4} = (t^2 + t) / 2$.
• $f_{g2} = (t^2 - t) / 2$.
• $f_{g1} = A - f - t^2$.

Their degrees are $1$, $2$, $2$, and $5$, respectively. They sum to $A$, so the shared $(0, 0)$ encoding selects one group on SPAN and RESPAN rows and selects no group on inactive rows.

Design rationale

The value $-1$ is simply the field value assigned to the 2-group case; this encoding does not use signed integer arithmetic. The values $-1$, $0$, and $1$ are distinct in the trace field, and the constraint $t(t - 1)(t + 1) = 0$ permits exactly those values.

The 8-group case gets its own Boolean flag because it controls the largest op-group lookup. The remaining three active sizes share the short-batch code. The product constraint $f \cdot t = 0$ excludes mixed encodings, while the two separate inactive-row constraints ensure that neither value can be non-zero when the encoding is inactive.

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

$$(A - f) \cdot h_i = 0 \text{ for } i \in [4, 8) \text{ | degree} = 6$$

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

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

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

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:

An entry is the typed message

$$G(batch\_id,group\_pos,group\_value) = P_{op\_group} + batch\_id + \beta group\_pos + \beta^2 group\_value.$$

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:

$$G(a',gc-i,h_i), \qquad i \in [1,8).$$

The batch-size flags select the required prefix of these messages: zero for a one-group batch, one for a two-group batch, three for a four-group batch, or seven for an eight-group batch. Each selected message is added with multiplicity $+1$. The batch address comes from the next row's block address $a'$.

When a deferred group or immediate is consumed, the decoder removes

$$G(a,gc,f_{push}s'_0+(1-f_{push})(2^7h'_0+op')).$$

For PUSH, the group value is the immediate at $s'_0$. Otherwise it combines $h'_0$ with the next opcode. The batch address and group position come from the current $a$ and $gc$ values.

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

Thus, a group is removed with multiplicity $-1$ exactly when its count is decremented inside a basic block. Multiplying by $sp$ excludes the decrements performed by SPAN and RESPAN. LogUp closure requires every deferred group added at batch setup to be consumed.