# Miden VM program decoder
###### tags: `decoder`
In this note we describe how Miden VM decoder works. The decoder is responsible for two things:

1. Decoding a sequence of field elements supplied by the prover into individual operation codes (or *opcodes* for short).
2. Computing hash of the program according to the methodology described [here](https://hackmd.io/yr-ieh7SSKOzWw7Kdo9gnA). Program hash binds the sequence of opcodes executed by the VM to a program the prover claims to have executed on the VM.

The last point means that the verifier can be convinced that a program executed by the VM matches the program hash that the VM outputs.

### Assumptions and notations
In this note we make the following assumptions:
1. An opcode requires $7$ bits to represent.
2. An immediate value requires one full field element to represent.
3. A `NOOP` operation has a numeric value of $0$, and thus, can be encoded as seven zeros. Executing a `NOOP` operation does not change the state of the VM, but it does advance operation counter, and may affect program hash.

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

When describing AIR constraints, we adopt the following notation: for a register $x$, we denote the current state of the register simply as $x$, and the next state of the register as $x'$. Thus, all transition constraints described in this note work with two consecutive rows of an execution trace.

Throughout the note, we denote random values sent by the verifier to the prover as $\alpha$ and $\beta$. These values are used for [permutation checks](https://hackmd.io/@arielg/ByFgSDA7D). The verifier sends these values after the prover has committed to the main execution trace, but before the prover has committed to permutation columns.

We refer to the register representing the top of the stack as $s_0$.

## Hash function
We assume that the hash function used to compute a program's hash is [Rescue Prime](https://eprint.iacr.org/2020/1143) instantiated over a state of $12$ field elements in a $64$-bit prime field. This also means that the hash function can absorb up to $8$ field elements in a single permutation.

Hashing is performed using an auxiliary table similar to the methodology described [here](https://hackmd.io/bOM0GTU6S7eklNQdU6xiLA). Denoting the lookup column as $p_0$, to compute a hash of $8$ field elements $v_1, ..., v_8$, we would first need to update $p_0$ like so:

$$
p_0' = p_0 \cdot (\beta + \alpha \cdot k_s + \alpha^2 \cdot a + \sum_{i=1}^8(\alpha^{i + 2} \cdot v_i) + \alpha^{11} \cdot 8)
$$

where $k_s$ is a constant used to identify table rows at which the hashing starts, and $a$ is the address of the row at which the hashing starts. Address $a$ is provided by the prover non-deterministically.

Then, to read the result of the hashing, we'd need to update $p_0$ like so:

$$
p_0' = p_0 \cdot (\beta + \alpha \cdot k_r + \alpha^2 \cdot (a + 7) + \sum_{i=1}^4(\alpha^{i + 2} \cdot r_i))
$$

where $k_r$ is a constant used to identify rows at which hashing result is available, $r_1, ..., r_4$ are the results of the hash provided non-deterministically by the prover.

The above does two lookups in the table: one at the row when the hashing starts, and another $7$ rows down, when the result of hashing is available. This works because hashing $8$ field elements can be done in a single permutation. If we need to hash more than $8$ field elements, we can do the following:

First, when we initiate hashing, we need to specify the total number of elements to be hashed. Denoting the elements to be hashed as $v_1, ..., v_n$, we'll need to update $p_0$ as follows:

$$
p_0' = p_0 \cdot (\beta + \alpha \cdot k_s + \alpha^2 \cdot a + \sum_{i=1}^8(\alpha^{i + 2} \cdot v_i) + \alpha^{11} \cdot n)
$$

The above will have the effect of absorbing first $8$ elements into hasher state. To absorb the next $8$ elements, we'd need to update $p_0$ as follows:

$$
p_0' = p_0 \cdot (\beta + \alpha \cdot k_a + \alpha^2 \cdot (a + 8) + \sum_{i=1}^8(\alpha^{i + 2} \cdot v_{i + 8}))
$$

where $k_a$ is a constant value used to identify rows at which we absorb addition field elements into the hasher state. For each subsequent absorption step, we'd need to keep incrementing $a$ by $8$. For example, absorbing $v_{17}, ... v_{24}$ would require updating $p_0$ like so:

$$
p_0' = p_0 \cdot (\beta + \alpha \cdot k_a + \alpha^2 \cdot (a + 16) + \sum_{i=1}^8(\alpha^{i + 2} \cdot v_{i + 16}))
$$

Then, finally, we can read the result of the hash by incrementing $a$ by $7$. For example, reading the result of hashing $v_1, ..., v_{24}$ can be done by updating $p_0$ as follows:

$$
p_0' = p_0 \cdot (\beta + \alpha \cdot k_r + \alpha^2 \cdot (a + 23) + \sum_{i=1}^4(\alpha^{i + 2} \cdot r_i))
$$

Thus, to hash $24$ field elements, we "used up" $24$ rows from the auxiliary hashing table.

## Operation decoding
To decode an operation we use $7$ registers, each contain a single bit of the operation's *opcode* as illustrated below.


In the above diagram, $b_0$ is the least significant bit of the opcode and $b_6$ is the most significant bit of the opcode.

### Operation group decoding
As described [here](https://hackmd.io/yr-ieh7SSKOzWw7Kdo9gnA#Span-block), an operation group is a sequence of operations which can be encoded into a single field element. For a field element of $64$ bits, we can fit up to $9$ operations into a group. We do this by concatenating binary representations of opcodes together with the first operation located in the least significant position.

We can read opcodes from the group by simply subtracting them from the op group value and then dividing the resulting value by $2^7$. Once the value of the op group reaches $0$, we know that all opcodes have been read. Graphically, this can be illustrated like so:


Notice that despite their appearance, `op bits` is actually $7$ separate registers, while `op group` is just a single register.

## Decoder structure
The decoder consists of several components as described below:


1. Block address register $a$. This register contains address of the hasher for the current block (row index from the auxiliary hashing table). It also serves the role of unique block identifiers. This is convenient, because hasher addresses are guaranteed to be unique.
2. $7$ registers encoding an opcode for an operation to be executed by the VM. We denote these registers $b_0, ..., b_6$. Each of these registers can contain a single binary value (either $1$ or $0$). And together these values describe a single opcode.
3. Register $sn$ which contains a binary flag indicating whether the VM is currently executing a *span* block. The flag is set to $1$ when a span block is being executed, and to $0$ otherwise.
4. $8$ hasher registers $h_0, ..., h_7$. When control flow operations are executed, these registers facilitate computation of program block hashes. However, when regular operations are executed, two of these registers are used to hold help with op group decoding, and the remaining $6$ can be used to hold operation-specific helper variables.
5. Register $gc$ used to keep track of unprocessed operation groups in a given *span* block.
6. A small number of additional registers (not shown) used primarily for constraint degree reduction.

### Control flow operations
Managing control flow in the VM is accomplished by executing control flow operations listed in the table below. These operations also dictate how the program hash is computed by the VM.

| Operation | Description |
| --------- | ----------- |
| `JOIN` | Initiates processing of a new [Join block](https://hackmd.io/yr-ieh7SSKOzWw7Kdo9gnA#Join-block). |
| `SPLIT` | Initiates processing of a new [Split block](https://hackmd.io/yr-ieh7SSKOzWw7Kdo9gnA#Split-block). |
| `LOOP` | Initiates processing of a new [Loop block](https://hackmd.io/yr-ieh7SSKOzWw7Kdo9gnA#Loop-block). |
| `REPEAT` | Initiates a new iteration of an executing loop. |
| `CALL` | Initiates processing of a new [Call block](https://hackmd.io/yr-ieh7SSKOzWw7Kdo9gnA#Call-block). |
| `SPAN` | Initiates processing of a new [Span block](https://hackmd.io/yr-ieh7SSKOzWw7Kdo9gnA#Span-block). |
| `RESPAN` | Initiates processing of a new operation batch within a span block. |
| `END` | Marks the end of a program block. |

### Control flow tables
Besides the auxiliary hasher table, control flow operations rely on $3$ virtual tables: *block stack* table, *block hash* table, and *op group* table. These tables are virtual in that they don't require separate trace columns. Their state is described solely by permutation columns: $p_1$, $p_2$, and $p_3$. The tables are described in the following sections.

#### Block stack table
When the VM starts executing a new program block, it adds its block ID together with the ID of its parent block (and some additional info) to the *block stack* table. When a program block is fully executed, it is removed from the table. In this way, the table represents a stack of blocks which are currently executing on the VM.

The table can be thought of as consisting of $3$ columns as shown below:


where:
* Column $t_0$ contains the ID of the block.
* Column $t_1$ contains the ID of the parent block. If the block has no parent (i.e., it is a root block of the program), parent ID is 0.
* Column $t_2$ contains a binary value which is set to $1$ is the block is a *loop* block, and to $0$ otherwise.

Permutation column $p_1$ is used to keep track of the state of the table. At any step of the computation, the current value of $p_1$ defines which rows are present in the table.

#### Block hash table
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 its hash from the block hash table.

The table can be thought of as consisting of $7$ columns as shown below:


where:
* Column $t_0$ contains the ID of the block. For program root, block ID is $0$.
* Columns $t_1, ..., t_4$ contain a hash (4 elements) of a child block for the block specified in $t_0$.
* Column $t_5$ contains a binary value which is set to $1$ if the block is the first child of a *join* block, and to $0$ otherwise.
* Column $t_6$ contains a binary value which is set to $1$ if the block is a body of a loop, and to $0$ otherwise.

Permutation column $p_2$ is used to keep track of the state of the table. At any step of the computation, the current value of $p_2$ defines which rows are present in the table.

#### Op group table
*Op group* table is used in decoding *span* blocks, which are leaves in a program's MAST. As described [here](https://hackmd.io/yr-ieh7SSKOzWw7Kdo9gnA#Span-block), a *span* block can contain one or more operation batches, each batch containing up to $8$ operation groups.

When the VM starts executing a new batch of operations, it adds all operation groups within a batch, except for the first one, to the *op group* table. Then, as the VM start executing an operation group, it removes the group from the table. Thus, by the time all operation groups in a batch have been executed, the *op group* table should be empty.

The table can be thought of as consisting of $3$ columns as shown below:


The meaning of the columns is as follows:

* Column $t_0$ contains operation batch ID. During the execution of the program, each operation batch is assigned a unique ID.
* Column $t_1$ contains the index of an op group within a batch. The indexes can be in the range $[1, 9)$ as the first group of a batch (group with index $0$) is not added to the table.
* Column $t_2$ contains the actual values of operation groups.

A tuple of $(t_0, t_1)$ uniquely identifies a row in the table.

Permutation column $p_3$ is used to keep track of the state of the table. At any step of the computation, the current value of $p_3$ defines which rows are present in the table.

## Program decoding
The basic idea of how decoding of a program works is described below.

We start at the root block of the program. We can compute the hash of the root block directly from hashes of its children. The prover provides hashes of the child blocks non-deterministically, and we use them to compute the program's hash (here we rely on the auxiliary hasher table). We then verify the program hash via boundary constraints. Thus, if the prover provided valid hashes for the child blocks, we will get the expected program hash.

Now, we need to verify that the VM executed the child blocks correctly. We do this recursively similar to what is described above: for each of the blocks, the prover provides hashes of its children non-deterministically and we verify that the hash has been computed correctly. We do this until we get to the leaf nodes (i.e., *span* blocks). Hashes of *span* blocks are computed linearly from the instructions executed by the VM.

A sample transition diagram of a control flow operation is shown below.


Here, we are executing a *join* block. The ID of this block is $blk_1$, and the ID of its parent is $blk_0$. Value of $blk_0$ is enforced via transition constraints, but $blk_1$ is provided by the prover non-deterministically.

Values $a_0, ..., a_3$ represent hash of the $blk_1$'s left child, and values $b_0, ..., b_3$ represent hash of the right child. Both of these hashes are provided by the prover non-deterministically.

When the VM executes a `JOIN` operation, it enforces that values $a_0, ..., a_3, b_0, ..., b_3$ are copied to the auxiliary hasher table into row with address $blk_1$. And when the VM executed `END` operation, it enforces that values $r_1, ..., r_3$ are copied from the auxiliary hasher table from the row with address $blk_1 + 7$. This enforces that $\{r_0, .., r_3\} \leftarrow hash(\{a_0, ..., a_3\}, \{b_0, ..., b_3\})$.

The `END` operation also removes a row with hash $r_0, .., r_3$ from the block hash table. This row would have been added to the table when $blk_0$ started executing. Thus, if $r_0, .., r_3$ does not match expected hash of $blk_0$'s child, the execution fails.

Lastly, the `END` operation sets block ID value for the next operation (i.e., changes it from $blk_1$ to $blk_0$). For this, it relies on the block stack table.

### Control flow operation semantics
In the following sections we describe high-level semantics of executing all control flow operations. The descriptions are not meant to be complete and omit some low-level details. However, they provide good intuition on how these operations work.

#### JOIN operation
Before a `JOIN` operation is executed by the VM, the prover populates $h_0, ..., h_7$ registers with hashes of left and right child of the *join* program block as shown in the diagram below.


In the above diagram, $blk$ is the ID of the *join* block which is about to be executed. $blk$ is also the address of the hasher row in the auxiliary hasher table. $prnt$ is the ID of the block's parent.

When the VM executes a `JOIN` operation, it does the following:
1. Adds a tuple $(blk, prnt, 0)$ to the block stack table.
2. Adds tuples $(blk, hash(left\_child), 1, 0)$ and $(blk, hash(right\_child), 0, 0)$ to the block hash table.
3. Performs a lookup into the hasher table to make sure the row with $(blk, hash(left\_child), hash(right\_child))$ exists there and is a starting row for a new hasher.

#### SPLIT operation
Before a `SPLIT` operation is executed by the VM, the prover populates $h_0, ..., h_7$ registers with hashes of true and false branches of the *split* program block as shown in the diagram below.


In the above diagram, $blk$ is the ID of the *split* block which is about to be executed. $blk$ is also the address of the hasher row in the auxiliary hasher table. $prnt$ is the ID of the block's parent.

When the VM executes a `SPLIT` operation, it does the following:
1. Adds a tuple $(blk, prnt, 0)$ to the block stack table.
2. Pops the stack and if the popped element is $1$, adds a tuple $(blk, hash(true\_branch), 0, 0)$ to the block hash table. If the element is $0$, adds a tuple $(blk, hash(false\_branch), 0, 0)$ to the block hash table. If the element is neither $1$ nor $0$, the execution fails.
3. Performs a lookup into the hasher table to make sure the row with $(blk, hash(true\_branch), hash(false\_branch))$ exists there and is a starting row for a new hasher.

#### LOOP operation
Before a `LOOP` operation is executed by the VM, the prover populates $h_0, ..., h_3$ registers with hash of the loop's body as shown in the diagram below.


In the above diagram, $blk$ is the ID of the *loop* block which is about to be executed. $blk$ is also the address of the hasher row in the auxiliary hasher table. $prnt$ is the ID of the block's parent.

When the VM executes a `LOOP` operation, it does the following:
1. Adds a tuple $(blk, prnt, 1)$ to the block stack table. The `2` indicates that this is a *loop* block.
2. Pops the stack and if the popped element is $1$, adds a tuples $(blk, hash(loop\_body), 0, 1)$ to the block hash table. If the element is $0$, nothing is added to the block hash table. If the element is neither $1$ nor $0$, the execution fails.
3. Performs a lookup into the hasher table to make sure the row with $(blk, hash(loop\_body)$ exists there and is a starting row for a new hasher.

#### CALL operation
Before a `CALL` operation is executed by the VM, the prover populates $h_0, ..., h_3$ registers with hash of the function's body as shown in the diagram below.


In the above diagram, $blk$ is the ID of the *call* block which is about to be executed. $blk$ is also the address of the hasher row in the auxiliary hasher table. $prnt$ is the ID of the block's parent.

When the VM executes a `CALL` operation, it does the following:
1. Adds a tuple $(blk, prnt, 0)$ to the block stack table.
2. Adds $(blk, hash(function\_body), 0, 0)$ to the block hash table.
3. Performs a lookup into the hasher table to make sure the row with $(blk, hash(function\_body)$ exists there and is a starting row for a new hasher.

#### SPAN operation
Before a `SPAN` operation is executed by the VM, the prover populates $h_0, ..., h_7$ registers with contents of the first operation batch of the span block as shown in the diagram below. The prover also sets the group count register $gc$ to the total number of operation groups in the span block.


In the above diagram, $blk$ is the ID of the *span* block which is about to be executed. $blk$ is also the address of the hasher row in the auxiliary hasher table. $prnt$ is the ID of the block's parent. $g_0\_op_0$ is the first operation of the batch, and $g_0$ is the first operation group of the batch with the first operation removed.

When the VM executes a `SPAN` operation, it does the following:
1. Adds a tuple $(blk, prnt, 0)$ to the block stack table.
2. Adds all groups of the operation batch, except for the first one, to the *op group* table.
3. Performs a lookup into the hasher table to make sure the row with $(blk, operation\_batch)$ exists there and is a starting row for a new hasher.
4. Sets the `in_span` register to $1$.

#### END operation
Before an `END` operation is executed by the VM, the prover populates $h_0, ..., h_3$ registers with the hash of the block which is about to end. The prover also sets $f_0$ and $f_1$ values as follows:
* $f_0$ is set to $1$ if the block is a body of a *loop* block.
* $f_1$ is set to $1$ if the block is a *loop* block.


In the above diagram, $blk$ is the ID of the block which is about to finish executing. $prnt$ is the ID of the block's parent.

When the VM executes an `END` operation, it does the following:
1. Removes a tuple $(blk, prnt, f_1)$ from the block stack table.
2. Removes a tuple $(prnt, hash(current\_block), nxt, f_0)$ from the block hash table, where $nxt=0$ if the next operation is either `END` or `REPEAT`, and $1$ otherwise.
3. Verifies that hash of the current block is present in the auxiliary hasher table at address $blk + 7$.

#### REPEAT operation
Before a `REPEAT` operation is executed by the VM, the VM copies values in registers $h_0, ..., h_4$ to the next row.


In the above diagram, $blk$ is the ID of the loop's body and $prnt$ is the ID of the loop.

When the VM executes a `REPEAT` operation, it does the following:
1. Checks whether register $h_4$ is set to $1$. If it isn't (i.e., we are not in a loop), the execution fails.
2. Pops the stack and if the popped element is $1$, adds a tuple $(prnt, hash(loop\_body), 0, 1)$ to the block hash table. If the element is not $1$, the execution fails.

The effect of the above is that the VM needs to execute the loop's body again to clear the block hash table.

#### RESPAN operation
Before a `RESPAN` operation is executed by the VM, the VM copies the ID of the current block $blk$ and the number of remaining operation groups in the span $n$ to the next row. The prover also sets teh value of $h_1$ register for the next row to the ID of the current block parent $prnt$.


In the above diagram, `g0_op0` is the first operation of the batch, and `g0'` is the first operation group of the batch.

When the VM executes a `RESPAN` operation, it does the following:
1. Removes the tuple $(blk, prnt, 0)$ from the block stack table.
2. Adds the tuple $(blk+8, prnt, 0)$ to the block stack table.
3. Performs a lookup into the hasher table to make sure the row with $(blk+8, operation\_batch)$ exists there and is an absorption row for a hasher.
4. Adds all groups of the operation batch, except for the first one, to the *op group* table using $blk+8$ as batch ID.

The net result of the above is that we incremented the ID of the current block by $8$ and added the next set of operation groups to the op group table.

### Program decoding example
Let's consider a simple program below:

<operations1>
if.true
    <operations2>
else
    <operations3>
end

Block structure of this program is shown below.

b0: JOIN
    b1: SPAN
        <operations1>
    b1: END
    b2: SPLIT
        b3: SPAN
            <operations2>
        b3: END
        b4: SPAN
            <operations3>
        b4: END
    b2: END
b0: END

The root of the program is a *join* block $b_0$. This block contains two children: a *span* bock $b_1$ and a *split* block $b_2$. In turn, the *split* block $b_2$ contains two children: a *span* block $b_3$ and a *span* block $b_4$.

When this program is executed on the VM, the following happens:

1. First, the hash of $b_0$ is added to the block hash table.
2. Then, `JOIN` operation for $b_0$ is executed. It adds hashes of $b_1$ and $b_2$ to the block hash table. It also adds an entry to the block stack table. States of both tables after this step are illustrated below.
3. Then, *span* $b_1$ is executed and a liner hash of its instructions is computed. Also, when `SPAN` for $b_1$ is executed, $b_1$ is added to the block stack table. At the end of $b_1$ (when `END` is executed), $b_1$ is removed from both the block hash and block stack tables.
4. Then, `SPLIT` operation for $b_2$ is executed. It adds an entry fro $b_2$ to the block stack table. Also, Depending on whether the top of the stack is $1$ or $0$, either, either hash of $b_3$ or hash of $b_4$ is added to the block hash table. Let's say the top of the stack is $1$. Then, at this point, the block hash and block stack table will look like in the second picture below.
5. Then, *span* $b_3$ is executed and a liner hash of its instructions is computed. Also, when `SPAN` for $b_3$ is executed, $b_3$ is added to the block stack table. At the end of $b_3$ (when `END` is executed), $b_3$ is removed from both the block hash and block stack tables.
6. Then, `END` operation for $b_2$ is executed. It removes the hash of $b_2$ from the block hash table, and also removes $b_2$ from the block stack table.
7. Finally, `END` for $b_0$ is executed, which removes hash of $b_0$ from the block hash table and also removes $b_0$ entry from the block stack table. At this point both tables are empty.

State of block hash and block stack tables after step 2:

State of block hash and block stack tables after step 4:

### Handling loops
TODO

## Span block decoding
As described [here](https://hackmd.io/yr-ieh7SSKOzWw7Kdo9gnA#Span-block), a *span* block can contain one or more operation batches, each batch containing up to $8$ operation groups. At the high level, decoding of a span block is done as follows:

1. At the beginning of the block, we initialize Rescue Prime hasher.
2. For each operation batch, we absorb the batch (i.e., $8$ field elements) into the hasher, and at the same time, add all of the groups contained in the batch (except for the first one) into the *op group* table.
3. We then remove operation groups from the op group table in the FIFO order one by one, and decode them in the manner similar to the one described [here](#Operation-group-decoding).
4. Once all operation groups in a batch have been decoded, we absorb the next batch into the hasher and repeat the process described above.
5. Once all batches have been decoded, we return the hash of the span block from the hasher.

Overall, three control flow operations are used when decoding a *span* block:
1. `SPAN` operation is used to initialize a hasher and absorbs the first operation batch into it.
2. `RESPAN` operation is used to absorb any additional batches in the span block.
3. `END` operation is used to end the decoding of a span block and retrieve it hash from the haser table.

### Single-batch span
The example below illustrates decoding of a span which contains a single operation batch. In turn, the batch contains $8$ operation groups: $g_0, ..., g_7$.


Decoding of this block proceeds as follows:

Before the VM starts processing this *span* block, the prover populates `hasher` registers $h_0, ..., h_7$ with operation groups $g_0, ..., g_7$. The prover also puts the total number of groups into the `group count` register $gc$. In this case, the total number of groups is $8$.

When the VM executes a `SPAN` operation, it does the following:
1. Sets the `is span` register $sn$ to $1$.
2. Performs a lookup into the hasher table to make sure the row with $(blk_1, g_0, ..., g_7)$ exists there and is a starting row for a new hasher.
3. Decrements $gc$ register by $1$.
4. Sets `op bits` registers at the next step to the first operation of $g_0$, and also copies $g_0$ with the first operation removed to the next row.
5. Adds groups $g_1, ..., g_7$ to the op group table. Thus, after the `SPAN` operation is executed, op group table looks as shown below.


Then, with every step the next operation is removed from $g_0$, and by step $9$, value of $g_0$ is $0$. Once this happens, the VM does the following:
1. Decrements register $gc$ by $1$.
2. Sets `op bits` registers at the next step to the first operation of $g_1$.
3. Sets `hasher` register $h_0$ to the value of $g_1$ with the first operation removed.
4. Removes row $(blk_1, 7, g_1)$ from the op group table (this row can be obtained by taking values from registers: $a$, $gc$, and $h_0' + \sum_{i=0}^6(2^i \cdot b_i')$).

Then, again with every subsequent step the next operation is removed from $g_1$ until its value reaches $0$, at which point, decoding of group $g_2$ begins.

The above steps are executed until value of $gc$ reaches $0$. Once $gc$ reaches $0$ and the last operation group $g_7$ is executed, the VM executed the `END` operation. Semantics of the `END` operation are described [here](#END-operation).

### Multi-batch span


### Handling immediate values

TODO

## Decoder constraints

### Computing block hash
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**, **split**, **loop**, and **call** 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$. The hasher is initialized using the auxiliary hasher table (as described [here](#Hash-function)), and we use the address of the hasher as the block's ID. The result of the hash is available $7$ rows down in the hasher table (i.e., at row with index equal to block ID plus $7$). We read the result from the hasher table at the time `END` operation is executed for a given block.

For **span** 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 auxiliary hasher table 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 $8$. This moves the "pointer" into the hasher table $8$ rows down with every new batch. We read the result from the hasher table at the time `END` operation is executed for a given block.

To simplify constraint description, we define define the following variables:

$h_{init}$ and $h_{init2}$, which correspond to rows in hasher table which initializes a new hasher:

$$
h_{init} = \beta + \alpha \cdot k_s + \alpha^2 \cdot a' + \sum_{i=0}^3(\alpha^{i + 3} \cdot h_i) \\
h_{init2} = \beta + \alpha \cdot k_s + \alpha^2 \cdot a' + \sum_{i=0}^7(\alpha^{i + 3} \cdot h_i)
$$

In the above, $a'$ is the address of the hasher (and also the ID of the block for which the hasher is instantiated).

$h_{absr}$, which corresponds to a row in the hasher table which absorbs a new operation batch:

$$
h_{absr} = \beta + \alpha \cdot k_a + \alpha^2 \cdot a' + \sum_{i=0}^7(\alpha^{i + 3} \cdot h_i)
$$

In the above, we assume that $a' = a + 8$, which is enforced by separate constraints.

$h_{res}$, which corresponds to a row in the hasher table which contains the result of hashing:

$$
h_{res} = \beta + \alpha \cdot k_r + \alpha^2 \cdot (a + 7) + \sum_{i=0}^3(\alpha^{i + 3} \cdot h_i)
$$

Armed with the above notation, we describe the constraints for each operation as follows:

| Condition | Constraint | Comments |
| -------------- | --------------------------- | -------- |
| $f_{join}=1$ | $p_0' = p_0 \cdot h_{init2} + \alpha^{11} \cdot 8$ | When `JOIN` operation is executed, a new hasher is initialized and contents of $h_0, ..., h_7$ are absorbed into the hasher. We also indicate the that number of elements to be hashed is $8$. |
| $f_{split}=1$ | $p_0' = p_0 \cdot h_{init2} + \alpha^{11} \cdot 8$ | When `SPLIT` operation is executed, a new hasher is initialized and contents of $h_0, ..., h_7$ are absorbed into the hasher. We also indicate the that number of elements to be hashed is $8$. |
| $f_{loop}=1$ | $p_0' = p_0 \cdot h_{init} + \alpha^{11} \cdot 4$ | When `LOOP` operation is executed, a new hasher is initialized and contents of $h_0, ..., h_3$ are absorbed into the hasher. We also indicate the that number of elements to be hashed is $4$. |
| $f_{call}=1$ | $p_0' = p_0 \cdot h_{init} + \alpha^{11} \cdot 4$ | When `CALL` operation is executed, a new hasher is initialized and contents of $h_0, ..., h_3$ are absorbed into the hasher. We also indicate the that number of elements to be hashed is $4$. |
| $f_{span}=1$ | $p_0' = p_0 \cdot h_{init2} + \alpha^{11} \cdot gc$ | When `SPAN` operation is executed, a new hasher is initialized and contents of $h_0, ..., h_7$ are absorbed into the hasher. We also indicate the that number of operation groups to be hashed is located in register $gc$. |
| $f_{respan}=1$ | $p_0' = p_0 \cdot h_{absr}$ | When `RESPAN` operation is executed, contents of $h_0, ..., h_7$ (which contain a batch of operations) are absorbed into the hasher.
| $f_{end}=1$ | $p_0' = p_0 \cdot h_{res}$ | When `END` operation is executed, we hash result is copied into registers $h_0, .., h_3$.
| otherwise | $p_0' = p_0$ | Hasher table is not affected. |

We can combine the above constraints into a single constraint as follows:

$$
p_0' = p_0 \cdot \left(\left[(h_{join} + h_{split}) \cdot (f_{init2} + \alpha^{11} \cdot 8)\right] + \\
\left[(h_{loop} + h_{call}) \cdot (f_{init} + \alpha^{11} \cdot 4)\right] + \\
\left[f_{span} \cdot (h_{init2} + \alpha^{11} \cdot gc) \right] + \\
h_{absr} \cdot f_{respan} + h_{res} \cdot f_{end} + \\
1 - (f_{join} + f_{split} + f_{loop} + f_{call} + f_{span} + f_{respan} + f_{end})\right)
$$

Notice that the degree of the above constraint is $9$ or smaller as long as degrees of operation flags are $6$ or smaller.

### Updating block stack table
As described [earlier](#Block-stack-table), block stack table keeps track of program blocks currently executing on the VM. Thus, whenever the VM starts executing a new block, the block, together with its parent, is added to the block stack table. And when execution of a block completes, it is removed from the block stack table.

The table below describes constraints for each of the operations which can affect the block stack table. In this table, for block start operations (`JOIN`, `SPLIT`, `LOOP`, `CALL`, `SPAN`) $a$ refers to the ID of the parent block, and $a'$ refers to the ID 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$.

| Condition | Constraint | Comments |
| -------------- | ---------------------------------- | -------- |
| $f_{join}=1$ | $p_1' = p_1 \cdot (\beta + \alpha \cdot a' + \alpha^2 \cdot a)$ | When `JOIN` operation is executed, row $(a', a, 0)$ is added to the block stack table. |
| $f_{split}=1$ | $p_1' = p_1 \cdot (\beta + \alpha \cdot a' + \alpha^2 \cdot a)$ | When `SPLIT` operation is executed, row $(a', a, 0)$ added to the block stack table. |
| $f_{loop}=1$ | $p_1' = p_1 \cdot (\beta + \alpha \cdot a' + \alpha^2 \cdot a + \alpha^3)$ | When `LOOP` operation is executed, row $(a', a, 1)$ is added to the block stack table. |
| $f_{call}=1$ | $p_1' = p_1 \cdot (\beta + \alpha \cdot a' + \alpha^2 \cdot a)$ | When `CALL` operation is executed, row $(a', a, 0)$ is added to the block stack table. |
| $f_{span}=1$ | $p_1' = p_1 \cdot (\beta + \alpha \cdot a' + \alpha^2 \cdot a)$ | When `SPAN` operation is executed, row $(a', a, 0)$ is added to the block stack table. |
| $f_{respan}=1$ | $p_1' \cdot (\beta + \alpha \cdot a + \alpha^2 \cdot h_1') =$ <br> $p_1 \cdot (\beta + \alpha \cdot a' + \alpha^2 \cdot h_1')$ | 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.
| $f_{end}=1$ | $p_1' \cdot (\beta + \alpha \cdot a + \alpha^2 \cdot a' + \alpha^3 \cdot h_5)$ <br> $=p_1$ | When `END` operation is executed, row $(a, a', h_5)$ is removed from the block span table. Register $h_5$ contains the `is_loop` flag. |

We can combine the above constraints into a single constraint as follows:

$$
p_1' \cdot \left(\left[(\beta + \alpha \cdot a + \alpha^2 \cdot a' + \alpha^3 \cdot h_5) \cdot f_{end}\right] + \\
\left[(\beta + \alpha \cdot a + \alpha^2 \cdot h_1') \cdot f_{respan} \right] + \\
1 - (f_{end} + f_{respan})\right) = \\
p_1 \cdot \left(
\left[(\beta + \alpha \cdot a' + \alpha^2 \cdot a) \cdot (f_{join} + f_{split} + f_{call} + f_{span}) \right] + \\
\left[(\beta + \alpha \cdot a' + \alpha^2 \cdot a + \alpha^3) \cdot f_{loop}\right] + \\
\left[(\beta + \alpha \cdot a' + \alpha^2 \cdot h_1') \cdot f_{respan} \right] + \\
1 - (f_{join} + f_{split} + f_{loop} + f_{call} + f_{span} + f_{respan}) \right)
$$

Notice that the degree of the above constraint is $9$ or smaller as long as degrees of operation flags are $6$ or smaller.

### Updating block hash table
As described [earlier](#Block-hash-table), 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 tables gets updated when we execute `JOIN`, `SPLIT`, `LOOP`, `CALL`, and `END` operations (executing `SPAN` operation does not affect the block hash table because a *span* block has no children).

To simplify constraint description, we define rows representing left and right children of a block as follows:

$$
ch_1 = \beta + \alpha \cdot a' + \sum_{i=0}^3(a^{i+2} \cdot h_i) \\
ch_2 = \beta + \alpha \cdot a' + \sum_{i=0}^3(a^{i+2} \cdot h_{i+4})
$$

Graphically, this looks like so:


In a similar manner, we define a value representing a row in the block hash table as follows:

$$
bhr = \beta + \alpha \cdot a + \sum_{i=0}^3(a^{i+2} \cdot h_i) + \alpha^7 \cdot h_4
$$

Note that in the above we use $a$ (block address from the current row) rather than $a'$ (block address from the next row) as we did for for values of $ch_1$ and $ch_2$. Also, note that we are not adding a flag indicating whether the block is the first child of a join block (i.e., $\alpha^6$ is missing). It will be added later on.

We also define a flag which is set $1$ when the next operation is neither `END` nor `REPEAT`, and to $0$ otherwise. We will use this flag to identify blocks which are the first child of a *join* block. The flag can be computed as follows.

$$
f_{first} = 1 - (f_{end}' + f_{repeat}')
$$

Armed with the above notation, we can express the constraints needed to ensure that block hash table is updated correctly as follows (recall that $s_0$ is the register at the top of the stack):

| Condition | Constraint | Comments |
| -------------- | ---------------------------------- | -------- |
| $f_{join}=1$ | $p_1' = p_1 \cdot (ch_1 + \alpha^6) \cdot ch_2$ | When `JOIN` operation is executed, hashes of both child nodes are added to the block hash table. We add $\alpha^6$ to the first child to differentiate it from the second child. |
| $f_{split}=1$ <br> $s_0 = 1$ | $p_1' = p_1 \cdot ch_1$ | 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. |
| $f_{split}=1$ <br> $s_0 = 0$ | $p_1' = p_1 \cdot ch_2$ | When `SPLIT` operation is executed and the top of the stack is $0$, hash of the *false* branch is added to the block hash table. |
| $f_{loop}=1$ <br> $s_0 = 1$ | $p_1' = p_1 \cdot (ch_1 + \alpha^7)$ | When `LOOP` operation is executed and the top of the stack is $1$, hash of loop body is added to the block hash table. We add $\alpha^7$ to indicate that the child is a body of a loop. |
| $f_{loop}=1$ <br> $s_0 = 0$ | $p_1' = p_1$ | When `LOOP` operation is executed and the top of the stack is $0$, block hash table does not change. |
| $f_{repeat}=1$ | $p_1'= p_1 \cdot (ch_1 + \alpha^7)$ | When `REPEAT` operation is executed, hash of loop body is added to the block hash table. We add $\alpha^7$ to indicate that the child is a body of a loop. |
| $f_{call}=1$ | $p_1' = p_1 \cdot ch_1$ | When `CALL` operation is executed, hash of the called function is added to the block hash table. |
| $f_{end}=1$ <br> $f_{first}=0$ | $p_1' \cdot bhr = p_1$ | When `END` operation is executed and the next operation is either `END` or `REPEAT` (i.e., the outer bock execution is also finished or we are about to execute another iteration of a loop), hash of the current block is removed from the block hash table. |
| $f_{end}=1$ <br> $f_{first}=1$ | $p_1' \cdot (bhr + \alpha^6) = p_1$ | When `END` operation is executed but the next operation is neither `END` nor `REPEAT` (i.e., we are about to start executing second child of a `JOIN` block), we need to add $\alpha^6$ to the current block hash row before removing it from the block hash table. |
| otherwise | $p_1' = p_1$ | Block hash table does not change. |

We can combine the above constraints into a single constraint as follows:

$$
p_1' \cdot ((bh + \alpha^6 \cdot f_{first}) \cdot f_{end} + 1 - f_{end}) = p_1 \cdot \left(
\Bigl[(ch_1 + \alpha^6) \cdot ch_2 \cdot f_{join}\Bigr] + \\
\Bigl[(ch_1 \cdot f_{split} + (ch_1 + \alpha^7) \cdot f_{loop}) \cdot s_0\Bigr] +
\Bigl[ch_2 \cdot f_{split} \cdot (1 - s_0)\Bigr] + \\
\Bigl[(ch_1 + \alpha^7) \cdot f_{repeat}\Bigr] + \Bigl[ch_1 \cdot f_{call} \Bigr] + 1 - (f_{join} + f_{split} + f_{loop} + f_{repeat} + f_{call}) \right)
$$

Notice that the degree of the above constraint is $9$ or smaller as long as degrees of all operation flags, except for $f_{end}$, are $5$ or smaller, and the degree of $f_{end}$ is $2$ or smaller.

### Group count register constraints

| Condition | Constraint | Comments |
| -------------- | ---------------------------------- | -------- |
| $f_{span}=1$ | $gc' - gc - 1 = 0$ | When `SPAN` operation is executed, group count should be decremented by $1$. |
| $f_{respan}=1$ | $gc' - gc - 1 = 0$ | When `RESPAN` operation is executed, group count should be decremented by $1$. |
| $f_{end}=1$ <br> $sn=1$ | $gc = 0$ | When *span* block is ending, group count should be $0$.
| $sn'=1$ <br> $f_{end}' + f_{respan}'=1$ | $gc' - gc = 0$ | When we are in a *span* block and the next operation is either `END` or `RESPAN`, group count should remain the same. |
| $sn' = 1$ <br> $f_{end}'=0$ <br> $f_{respan}'=0$ | $(gc' - gc) \cdot (gc' - gc -1) = 0$ | When we are in a *span* block and the next operation is neither `END` nor `RESPAN`, group count can either stay the same or decrease by $1$. |

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

### Other constraints

We need to make user that operation bit registers $b_0, ..., b_6$ are binary. This can be done with the following constraints for values of $i \in \{0, ..., 6\}$:

$$
b_i^2 - b_i = 0
$$

When executing `SLPIT` or `LOOP` operation, we need to make sure that top of the stack contains a binary value. This can be done with the following constraint:

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

When executing a `REPEAT` operation, we need to make sure that the top of the stack is set to $1$. This can be done with the following constraint:

$$
f_{repeat} \cdot (1 - s_0) = 0
$$

When executing `END` operation for a loop block, we need to make sure that top of the stack is set to $0$ (i.e., we can't exit the loop unless top of the stack is $0$). This can be done with the following constraint:

$$
f_{end} \cdot h_5 \cdot s_0 = 0
$$

Recall, that when we execute `END` operation for a *loop* block, register $h_5$ is set to $1$.

When executing `END` operation and the next operation is `REPEAT`, the first four registers of the hasher should be copied over:

$$
f_{end} \cdot f_{repeat}' \cdot (h_i' - h_i) = 0
$$

## Span block decoding 2
As described [here](https://hackmd.io/yr-ieh7SSKOzWw7Kdo9gnA#Span-block), a *span* block can contain one or more operation batches, each batch containing up to $8$ operation groups. At the high level, decoding of a span block is done as follows:

1. At the beginning of the block, we initialize Rescue Prime hasher.
2. For each operation batch, we absorb the batch (i.e., $8$ field elements) into the hasher, and at the same time, add each of the groups contained in the batch into a virtual table (op group table).
3. We than remove operation groups from the table in the FIFO order one by one, and decode them in the manner similar to the one described [above](#Operation-group-decoding).
4. Once all operation groups in a batch have been decoded, we absorb the next batch into the hasher and repeat the process described above.
5. Once all batches have been decoded, we return the hash of the span block from the hasher.

### Op group table
The virtual table we use to hold un-processed operation groups has the following form:


The meaning of the columns is as follows:

* Column $t_0$ contains IDs of operation batches to which a group belongs. During the execution of the program, each operation batch is assigned a unique ID.
* Column $t_1$ contains the index of an op group within a batch. The indexes can be in the range $[1, 9)$ as the first group of a batch (group with index $0$) is not added to the table.
* Column $t_2$ contains the actual values of the operation groups.

A tuple of $(t_0, t_1)$ must uniquely identify a row in the table.

To represent this table, we'll use a single permutation column $p_1$. This column keeps track of rows inserted into and removed from the table. Thus, at any step of the computation, $p_1$ contains a product of rows currently in the table.

To compute a product of rows, we first need to reduce each row to a single value. This is done as follows. Assume $\alpha$ is a random value the verifier sends to the prover. The prover reduces row $i$ in the table to a single value $v_i$ as:

$$
v_i = \alpha \cdot t_{0, i} + \alpha^2 \cdot t_{1, i} + \alpha^3 \cdot t_{2, i}
$$

Then, when row $i$ is added to the table, we update the value in the $p_0$ column like so ($\beta$ is another random value sent by the verifier):

$$
p'_1 = p_1 \cdot (\beta + v_i)
$$

And when row $i$ is removed from the table, we update the value in $p_0$ column like so:

$$
p'_1 = \frac{p_1}{\beta + v_i}
$$

Thus, if the initial value of $p_1 = 1$, the value of $p_1$ will be $1$ at the end of program execution, if and only if we added and then removed exactly the same set of rows.

The structure of the table itself does not enforce the sequence in which the rows are added and removed. Thus, adding a row and then removing is equivalent to removing a row and then adding it. To make sure the latter doesn't happen, we'll need to impose additional constraints outside of the table.

### Starting a span block
At the beginning of each span block, we must execute a `SPAN` operation on the VM. This operation does the following:

1. Initializes the hasher and absorbs the first operation batch (i.e., $8$ operation groups) into the hasher.
2. Adds $7$ out of the $8$ groups to the op group table (the first group is skipped).
3. Initiates decoding of the first op group.

For example, if a span block contains a single batch, executing a `SPAN` operation would look like so:


In the above, `hash addr` register (denoted as $a$) contains the row address of the hasher in the hashing table, `group count` registers (denoted as $c$) contains the total number of groups in the span block, and `op sponge` registers (denoted as $g_0, ..., g_7$) contain the operation groups to be absorbed.

Thus, to absorb operation groups in $g_0, ..., g_7$ into the hasher, we'll need to enforce the following constraints:

$$
p_0' = p_0 \cdot ((\beta + \alpha \cdot k_s + \alpha^2 \cdot a + \sum_{i=0}^7(\alpha^{i + 3} \cdot g_i) + \alpha^{11} \cdot c) \cdot f_{span} - f_{span} + 1)
$$

where $p_0$ is a lookup column for the hashing table as described [here](#Hash-function). The above constraint affects value of $p_0$ only when $f_{span} = 1$, otherwise the value of $p_0$, remains the same.

We also want to make sure that the value of hasher address and group count does not change in the next step. This can be done with the following constraints:

$$
(a' - a) \cdot f_{span} = 0 \\
(c' - c) \cdot f_{span} = 0
$$

To add operation groups in $g_1, ..., g_7$ into the op group table, we will enforce the following constraints:

$$
p_1' = p_1 \cdot ((\prod_{i=1}^7 (\beta + \alpha \cdot a + \alpha^2 \cdot (c - i) + \alpha^3 \cdot g_i)) \cdot f_{span} - f_{span} + 1)
$$

Above, we are using `hash addr` as the operation batch ID. If the above constraints hold, after executing `SPAN` operation, the op group table would look as follows:


The reason we don't add group $g_0$ to the table is that we can start decoding this group immediately. To do this, we enforce the following constraints:

$$
i_{op}' \cdot f_{span} = 0 \\
(g_0' \cdot 2^7 - g_0 + \sum_{i=0}^6 (2^i \cdot b_i)) \cdot f_{span} = 0
$$

The above ensures that we set the operation index to $0$ just as we populate op bits registers $b_0, .., b_6$ with the first operation of $g_0$. Values for $b_0, ..., b_6$ are provided by the prover non-deterministically.

We then proceed to decode $g_0$ in a manner similar to the one described [here](#Operation-group-decoding).

### Decoding span operation groups
While decoding of the first operation group in a span can begin immediately, decoding subsequent groups requires removing them one by one from the op group table. To facilitate this, we'll impose the following constraint against `group count` register:

$$
(1 - f_{ctrl}) \cdot (c - c') \cdot (c - c' - 1) = 0
$$

This constraint specifies that whenever we execute regular operations, the value in the `group count` register can either remain the same or decrease by one. Thus, when the value does decrease by one, we assume that decoding of a new group is starting. Graphically, this would look like so:


In the picture above, decoding of operations in the first group completes by step $9$, and decoding of the second operation group starts on step $10$. Thus, the value of `group count` register decreases from $8$ to $7$ between these two steps.

To simplify description of the constraints, we'll define a binary flag $f_{ng}$. The value of this flag can be computed like so:

$$
f_{ng} = (1 - f_{ctrl}) \cdot (c - c')
$$

Thus, when decoding of a new group is about to start $f_{ng}$ will be set to $1$; otherwise, it will be set to $0$. For the example illustrated above, $f_{ng} = 1$ at step $9$, thus the constraints described below refer to step $9$ as the current step, and step $10$ as the next step.

To make sure that decoding of a new group starts only after decoding of a previous group has finished, we'll impose the following constraint:

$$
f_{ng} \cdot g_0 = 0
$$

We also need to make sure that `op index` is reset to zero for the new group. This can be done with the following constraint:

$$
f_{ng} \cdot i_{op}' = 0
$$

Next, we'll need to make sure a row containing $g_1$ group is removed from the op group table. Batch ID of this row is contained in register $a$ and group index is contained in register $c$ at step $10$. Thus, the value of the row which needs to be removed from the op group table can be computed as:

$$
v = \beta + \alpha \cdot a + \alpha^2 \cdot c' + \alpha^3 \cdot (g_0' \cdot 2^7 + \sum_{i=0}^6(2^i \cdot b_i'))
$$

The above requires that the prover set `op bits` registers at step $10$ to the binary decomposition of the first operation of $g_1$ group, and the remaining value of the group goes into register $g_0$ (also at step $10$).

To make sure that this row is removed from the op group table, we'll need to impose the following constraint:

$$
p_1' \cdot (v \cdot f_{ng} - f_{ng} + 1)= p_1
$$

We can combine this constraint with the constraint from the previous section which we used to enforce addition of operation groups to op group table when `SPAN` instruction is executed. First, we'll define a row that is to be added to the op group table as:

$$
u_i = \beta + \alpha \cdot a + \alpha^2 \cdot (c - i) + \alpha^3 \cdot g_i
$$

Then, the full constraint against $p_1$ column becomes:
$$
p_1' \cdot (v \cdot f_{ng} - f_{ng} + 1)= p_1 \cdot ((\prod_{i=1}^7 u_i) \cdot f_{span} - f_{span} + 1)
$$

The table below shows what the above constraint reduces to for various values of $f_{span}$ and $f_{ng}$. Note that, combination $f_{span}=1$ and $f_{ng}=1$ is not possible because $f_{ng}$ can be set to $1$ only when we are executing regular operations.

| $f_{span}$ | $f_{ng}$ | Constraint | Comments |
| ---------- | ---------- | ---------------------- | -------- |
| 0 | 0 | $p_1' = p_1$ | Value of $p_1$ does not change |
| 1 | 0 | $p_1' = p_1 \cdot \prod_{i=1}^7 u_i$ | Rows $u_1, ..., u_7$ are added to the table |
| 0 | 1 | $p_1' \cdot v = p_1$ | Row $v$ is removed from the table |

### Ending a span block

### Handling immediate values

$$
g = g_0' + \sum_{i=0}^6(2^i \cdot b_i') \\
v = \beta + \alpha \cdot a + \alpha^2 \cdot c' + \alpha^3 \cdot (g \cdot (1 - f_{push}) + s_0 \cdot f_{push})
$$
test
$$
f_{ng} = (1 - f_c) \cdot (c - c')
$$

$$
p_1' \cdot (v \cdot f_{ng} + f_{ng} - 1)= p_1
$$

### Decoding multiple batches

### Span decoding constraints

Value in register $a$ (`hash addr`) is unconstrained when `SPAN` operation is executed. Otherwise, it either remains the same, or is decremented by $8$ when `RESPAN` operation is executed.

$$
(1 - f_{span}) \cdot (a' - a - 8 \cdot f_{respan}) = 0
$$

When a regular operation is executed, the value in register $c$ (`group count`) either remains the same, or is decremented by $1$. When a `RESPAN` operation is executed, value of $c$ is decremented by $1$. Otherwise, register $c$ is unconstrained.

$$
(1 - f_{ctrl}) \cdot (c - c') \cdot (c - c' - 1) + f_{respan} \cdot (c - c' - 1)= 0
$$

Register $i_{op}$

$$
(f_{span} + f_{respan} + f_{ng}) \cdot i_{op}' = 0
$$

$$
(1 - f_{ctrl}) \cdot ((c - c') \cdot i_{op} + (1 - c + c') \cdot (i_{op}' - i_{op} - 1)) = 0 \\
\prod_{i=0}^8 (i - i_{op}) = 0
$$

### Span decoding optimizations