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

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

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), 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:

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 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\).

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, 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):

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

\[ (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, 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.
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. 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.

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.

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