Proving — An Example

In order to illustrate how these different components work together, let us consider an example in which the program counter $pc$ points to memory location $\mathtt{0x00000004}$, containing the binary encoding of the instruction ADDI x10 x8 3. Moreover, for the sake of this example, let us assume the following about the state of the VM.

• Current clock cycle: $256$
• Current trace row: $255$
• Total number of rows: $2^{16}$
• $R[\mathtt{x8}] = \mathtt{0x000000FF}$ was last updated with timestamp $32$
• $R[\mathtt{x10}] = \mathtt{0x00000005}$ was last updated with timestamp $7$
• $Prog[\mathtt{0x00000004}]$ has been accessed $2$ times before the current clock cycle

In the following we describe the relevant trace columns associated with each component, their expected values at row $255$ associated with the current clock cycle $256$, and the associated constraints that they must satisfy.

​

CPU Component Trace Columns and Constraints

In order to verify the correct execution of the ADDI x10 x8 3 instruction at clock cycle $256$, the CPU component will perform the following operations:

• Ensure a correct state transition;
• Fetch the instruction ADDI x10 x8 3 from the program memory component;
• Decode the contents of the instruction and check the correctness of its format;
• Read contents of register $\mathtt{x8}$ from the register memory component;
• Interact with the execution component to execute the instruction ADDI x10 x8 3; and
• Update the contents of register $\mathtt{x10}$ based on the output of the execution component.

Let us now show how each of these operations is performed.

​

Ensuring a Correct State Transition

In this step, the CPU component ensures that the state transition is performed correctly in order to guarantee the correct ordering of instructions during the execution of a program.

In order to do so, the CPU component performs the following checks:

1. It verifies that the program counter in the present row matches the value of the next program counter from the preceding row;
2. It checks that clock values have been updated correctly; and
3. It ensures that padding rows cannot be followed by a non-padding row.

According to the current state of virtual machine, the index $i$ for the current row is $255$, the total number of rows is $2^{16}$, the program counter $pc$ points to memory location $\mathtt{0x00000004}$ containing an instruction ADDI x10 x8 3. Hence, the following holds:

• $i=255$
• $\mathtt{{pc}^{(1)}[255]}$ $=$ $\mathtt{0x04}$
• $\mathtt{{pc}^{(2)}[255]}$ $=$ $\mathtt{0x00}$
• $\mathtt{{pc}^{(3)}[255]}$ $=$ $\mathtt{0x00}$
• $\mathtt{{pc}^{(4)}[255]}$ $=$ $\mathtt{0x00}$
• $\mathtt{{clk}^{(1)}[255]}$ $=$ $\mathtt{0x00}$
• $\mathtt{{clk}^{(2)}[255]}$ $=$ $\mathtt{0x01}$
• $\mathtt{{clk}^{(3)}[255]}$ $=$ $\mathtt{0x00}$
• $\mathtt{{clk}^{(4)}[255]}$ $=$ $\mathtt{0x00}$
• $\mathtt{is\_first}[255]$ $=$ $0$
• $\mathtt{is\_last}[255]$ $=$ $0$
• $\mathtt{is\_add}[255]$ $=$ $1$
• $\mathtt{imm\_c}[255]$ $=$ $1$
• $\mathtt{is\_pad}[255]$ $=$ $0$

From the above description, we note that some values, such as the program counter, are split over multiple limbs. Here, $\mathtt{{pc}^{(1)}[255]}$ is the limb contain the least significant bits of the program counters.

In order to verify that the program counter in the present row matches the value of the next program counter from the preceding row, the following constraint is enforced:

$$\small \begin{array}{l} {/\!\!/\, \texttt{Transition constraints for} \ \mathtt{pc}[i] \ \texttt{for row} \ i > 0 \ \texttt{unless} \ \mathtt{is\_pad}[i]=1} \\[1pt] {/\!\!/\, \texttt{Comparing two limbs at a time}} \\[1pt] \bullet \ (1-\mathtt{is\_first}[i]) \cdot (1-\mathtt{is\_pad}[i]) \ \cdot \\ \ \ \ (\mathtt{pc}^{(1)}[i] + \mathtt{pc}^{(2)}[i] \cdot 2^{8} - \mathtt{pc\_next}^{(1)}[i-1] - \mathtt{pc\_next}^{(2)}[i-1] \cdot 2^{8}) = 0, \\[1pt] \bullet \ (1-\mathtt{is\_first}[i]) \cdot (1-\mathtt{is\_pad}[i]) \ \cdot \\ \ \ \ (\mathtt{pc}^{(3)}[i] + \mathtt{pc}^{(4)}[i] \cdot 2^{8} - \mathtt{pc\_next}^{(3)}[i-1] - \mathtt{pc\_next}^{(4)}[i-1] \cdot 2^{8}) = 0, \\[4pt] \end{array}$$

Since $\mathtt{is\_pad}[255]=0$ and $\mathtt{is\_first}[255]=0$ and since each limb of $\mathtt{pc}$ and $\mathtt{pc\_next}$ is in the range $\{0,\ldots,255\}$, in order for the above constraint to be satisfied, it must be the case that:

• $\mathtt{{pc\_next}^{(1)}}[254]$ $=$ $\mathtt{0x04}$
• $\mathtt{{pc\_next}^{(2)}}[254]$ $=$ $\mathtt{0x00}$
• $\mathtt{{pc\_next}^{(3)}}[254]$ $=$ $\mathtt{0x00}$
• $\mathtt{{pc\_next}^{(4)}}[254]$ $=$ $\mathtt{0x00}$

Likewise, in order to verify that the clock values have been updated correctly, the following transition constraint must be satisfied:

$$\small \begin{array}{l} {/\!\!/\, \texttt{Transition constraints for} \ \mathtt{clk}[i] \ \texttt{for row} \ i > 0} \\[1pt] {/\!\!/\, \mathtt{clk\_carry}^{(j)} \ \texttt{for} \ j = 1,2 \texttt{ used for handling carries}} \\[1pt] {/\!\!/\, \texttt{Adding two limbs at a time}} \\[1pt] \bullet \ \mathtt{clk}^{(1)}[i] + \mathtt{clk}^{(2)}[i] \cdot 2^{8} + \mathtt{clk\_carry}^{(1)}[i] \cdot 2^{16} = \\ \ \ \ \mathtt{clk}^{(1)}[i-1] + \mathtt{clk}^{(2)}[i-1] \cdot 2^{8} + 1 \\[1pt] \bullet \ \mathtt{clk}^{(3)}[i] + \mathtt{clk}^{(4)}[i] \cdot 2^{8} + \mathtt{clk\_carry}^{(2)}[i] \cdot 2^{16} = \\ \ \ \ \mathtt{clk}^{(3)}[i-1] + \mathtt{clk}^{(4)}[i-1] \cdot 2^{8} + \mathtt{clk\_carry}^{(1)}[i] \\[8pt] {/\!\!/\, \texttt{Enforcing} \ \mathtt{clk\_carry}^{(j)} \in \{0,1\} \ \texttt{for} \ j = 1,2} \\[1pt] \bullet \ (\mathtt{clk\_carry}^{(1)}[i]) \cdot (1 - \mathtt{clk\_carry}^{(1)}[i]) = 0, \\[4pt] \bullet \ (\mathtt{clk\_carry}^{(2)}[i]) \cdot (1 - \mathtt{clk\_carry}^{(2)}[i]) = 0, \\[8pt] {/\!\!/\, \texttt{Range check for } \mathtt{clk}^{(j)} \texttt{ for } \ j=1,2,3,4} \\ {/\!\!/\, \texttt{More limbs would be needed if} \ T \geq 2^{32}} \\[1pt] \bullet \ \mathtt{clk}^{(j)} \in \left[0,2^{8}-1\right] \ \texttt{for} \ j=1,2,3,4, \\[4pt] \end{array}$$

For that to happen, it must be the case:

• $\mathtt{{clk}^{(1)}}[254]$ $=$ $\mathtt{0xFF}$
• $\mathtt{{clk}^{(2)}}[254]$ $=$ $\mathtt{0x00}$
• $\mathtt{{clk}^{(3)}}[254]$ $=$ $\mathtt{0x00}$
• $\mathtt{{clk}^{(4)}}[254]$ $=$ $\mathtt{0x00}$
• $\mathtt{{clk\_carry}^{(1)}}[255]$ $=$ $0$
• $\mathtt{{clk\_carry}^{(2)}}[255]$ $=$ $0$

Note that the above constraints introduce additional helper/auxiliary trace variables to account for any carry that may arise while performing the clock update. The prover sets the values for these variables as specified above.

Finally, in order to ensure that padding rows cannot be followed by a non-padding row, the following constraint must be satisfied:

$$\small \begin{array}{l} \hspace{0pt}{/\!\!/\, \texttt{Ensuring that} \ \mathtt{is\_pad} \ \texttt{remains} \ 1 \ \texttt{once it is set to} \ 1 \ \texttt{for row} \ i > 0} \\[1pt] \bullet \ (1 - \mathtt{is\_first}[i]) \cdot (1 - \mathtt{is\_pad}[i]) \cdot (\mathtt{is\_pad}[i-1]) = 0. \\[4pt] \end{array}$$

Since $\mathtt{is\_pad}[255]=0$ and $\mathtt{is\_first}[255]=0$, this implies that:

• $\mathtt{is\_pad}[254]=0$

​

Fetching the Instruction

In order to fecth the instruction being executed at the current clock cycle (ADDI x10 x8 3), the CPU component must interact with the program memory to read the instruction stored at the memory location pointed by the program counter. It must also ensure that the program counter $\mathtt{pc}$ is memory-aligned (i.e., a multiple of $4$).

Remark: Whenever constraints involve trace columns restricted to the same row, we omit the explicit $[i]$ index for readability. For instance, in the description below, we write $\mathtt{{instr\_val}^{(1)}}$ instead of $\mathtt{{instr\_val}^{(1)}}[255]$. All values set in the remainder of this section, unless explicitly specified, apply only to the row indexed by $[255]$ of the corresponding trace column.

In the specification, the CPU interaction with the program memory is captured by a call to the $\mathtt{Read}_{Prog}$ interface with parameters $\mathtt{pc}$ and $\mathtt{clk}$ to obtain $\mathtt{instr\_val}$. Note that the CPU component does not check the consistency of the program memory, which is handled separately by the program memory component.

In the actual implementation, this interface is not explicitly implemented since the trace columns for $\mathtt{pc}$, $\mathtt{clk}$, and $\mathtt{instr\_val}$ are shared between the CPU and program memory components.

As a result of this interaction, the value of these columns will be as follows:

• $\mathtt{{instr\_val}^{(1)}}$ = $Prog[\mathtt{0x00000004}]$ = $\mathtt{0b00010011}$
• $\mathtt{{instr\_val}^{(2)}}$ = $Prog[\mathtt{0x00000005}]$ = $\mathtt{0b00000101}$
• $\mathtt{{instr\_val}^{(3)}}$ = $Prog[\mathtt{0x00000006}]$ = $\mathtt{0b00110100}$
• $\mathtt{{instr\_val}^{(4)}}$ = $Prog[\mathtt{0x00000007}]$ = $\mathtt{0b00000000}$

The values of the 4 limbs of $\mathtt{instr\_val}$ follow from the fact that the binary encoding for the instruction ADDI x10 x8 3 is as follows:

• Bits 0-6: $\mathtt{0b0010011}$ corresponds to a constant associated with ADDI.
• Bits 7-11: $\mathtt{0b01010}$ corresponds to destination register $\mathtt{x10}$. This should match the value of $\mathtt{op\_a}$;
• Bits 12-14: $\mathtt{0b000}$ corresponds to a second constant associated with ADDI;
• Bits 15-19: $\mathtt{0b01000}$ corresponds to the source register $\mathtt{x8}$. This should match the value of $\mathtt{op\_b}$;
• Bits 20-31: $\mathtt{0b000000000011}$ corresponds to the immediate value $3$. This should match the value of $\mathtt{op\_c}$;

In order to ensure the program counter is a multiple of $4$ due to the memory alignment requirement, the following constraint needs to be satisfied:

$$\small \begin{array}{l} {/\!\!/\, \texttt{Ensuring that} \ \mathtt{pc} \ \texttt{is a multiple of 4}} \\[1pt] \bullet \ \mathtt{pc\_aux}^{(1)} \cdot 4 - \mathtt{pc}^{(1)} = 0, \\[4pt] \hspace{0pt}{/\!\!/\, \texttt{Enforcing} \ \mathtt{pc\_aux}^{(1)} \in \left[0,2^{6}-1\right]} \\[1pt] \bullet \ \mathtt{pc\_aux}^{(1)} \in \left[0,2^{6}-1\right]. \\[4pt] \end{array}$$

To show that this is indeed the case, the prover must set the following auxiliary variable to be:

• $\mathtt{pc\_aux}^{(1)}=\mathtt{0x01}$

​

Decoding the Instruction

In this step, the CPU component decodes the instruction ADDI x10 x8 3 that was fetched from the program memory and checks the correctness of the binary encoding.

To achieve this goal, the prover provides several auxiliary values (advices) to help verify the correctness of the binary encoding. More precisely, the prover will provide the following values:

• $\mathtt{op\_a}$: The address of the destination register in the instruction ADDI x10 x8 3. This corresponds to the destination register 10.
• $\mathtt{op\_b}$: The address of the source register in the instruction ADDI x10 x8 3. This corresponds to the destination register 8.
• $\mathtt{op\_c}$: The address of the third operand. This corresponds to the immediate value 3
• $\mathtt{{op\_b\_flag}}$: A flag indicating whether operand $\mathtt{op\_b}$ is used. Should be 1.
• $\mathtt{{imm\_c}}$: A flag indicating whether operand $\mathtt{op\_c}$ is an immediate value, Should be 1.
• $\mathtt{is\_add}$: a selector flag which indicates an ADD or ADDI operation. Should be 1.
• $\mathtt{is\_alu\_imm\_no\_shift}$: a flag which indicates this is an ALU instruction with non-shift immediate values. Should be 1.
• $\mathtt{is\_type\_i}$: a flag which indicates that this is a Type I instruction. Should be 1.
• $\mathtt{is\_pad}$: a selector flag which indicates whether the current row is being used for padding. Should be 0.
• $\mathtt{is\_first}$: a flag which indicates whether the current row is the first row. Should be 0.
• $\mathtt{is\_last}$: a flag which indicates whether the current row is the last row. Should be 0.

Moreover, since the operands are spread over several limbs of $\mathtt{instr\_val}$, the prover additionally provides the following values to help with verification of the binary encoding of the instruction ADDI x10 x8 3:

• $\mathtt{op\_a0}$ = 0 (bit 0 from $\mathtt{op\_a}$)
• $\mathtt{op\_a1\_4}$ = 5 (bits 1—4 from $\mathtt{op\_a}$)
• $\mathtt{op\_b0}$ = 0 (bit 0 from $\mathtt{op\_b}$)
• $\mathtt{op\_b1\_4}$ = 4 (bits 1—4 from $\mathtt{op\_b}$)
• $\mathtt{op\_c0\_3}$ = 3 (bits 0—3 from $\mathtt{op\_c}$)
• $\mathtt{op\_c4\_7}$ = 0 (bits 4—7 from $\mathtt{op\_c}$)
• $\mathtt{op\_c8\_10}$ = 0 (bits 8—10 from $\mathtt{op\_c}$)
• $\mathtt{op\_c11}$ = 0 (bit 11 from $\mathtt{op\_c}$)

In order to check the correctness of the values provided by the prover, the following set of constrains are enforced by the CPU component, where we only include those that are relevant for ALU instructions:

1. Checking that only one instruction or padding flag is set

$$\small \begin{array}{l} {/\!\!/\, \texttt{Enforcing exactly one instruction flag is set to 1}} \\[1pt] \mathtt{is\_lui} + \mathtt{is\_auipc} + \mathtt{is\_jal} + \mathtt{is\_jalr} + \mathtt{is\_ecall} + \mathtt{is\_ebreak} +\\ \mathtt{is\_lui} + \mathtt{is\_auipc} + \mathtt{is\_jal} + \mathtt{is\_jalr} + \mathtt{is\_ecall} + \mathtt{is\_ebreak} +\\ \mathtt{is\_unimp} + \mathtt{is\_beq} + \mathtt{is\_bne} + \mathtt{is\_blt} + \mathtt{is\_bge} + \mathtt{is\_bltu} + \mathtt{is\_bgeu} +\\ \mathtt{is\_lb} + \mathtt{is\_lh} + \mathtt{is\_lw} + \mathtt{is\_lbu} + \mathtt{is\_lhu} + \mathtt{is\_sb} + \mathtt{is\_sh} + \mathtt{is\_sw} + \\ \mathtt{is\_add} + \mathtt{is\_sub} + \mathtt{is\_sll} + \mathtt{is\_slt} + \mathtt{is\_sltu} + \mathtt{is\_xor} + \mathtt{is\_srl} + \mathtt{is\_sra} +\\ \mathtt{is\_or} + \mathtt{is\_and} + \mathtt{is\_pad} = 1 \end{array}$$

Since $\mathtt{is\_add}$ is set to 1, all the other flags in the above constraint are set to 0. Our specification also uses additional constraints to ensure that the flags can only be assigned 0/1 values, ensuring that setting all the other flags to be 0 is the only way to satisfy the above constraint. For simplicity, in this document we do not specify the binary constraint on the flags, and refer the reader to the documentation.

2. Ensuring that the flag $\mathtt{op\_b\_flag}$ for operand $\mathtt{op\_b}$ is set to $1$ for all instructions except LUI, AUIPC, JAL, UNIMP

$$\small \begin{array}{ll} & {/\!\!/\, \texttt{Ensuring that } \mathtt{op\_b\_flag = 1} \texttt{ for all instructions}} \\[1pt] & {/\!\!/\, \texttt{except lui, auipc, jal, unimp}} \\[1pt] &(\mathtt{is\_sb} + \mathtt{is\_sh} + \mathtt{is\_sw} + \mathtt{is\_lb} + \mathtt{is\_lh} + \mathtt{is\_lw} + \mathtt{is\_lbu} + \mathtt{is\_lhu} + \mathtt{is\_jalr} \\ &+\mathtt{is\_add} + \mathtt{is\_sub} + \mathtt{is\_slt} + \mathtt{is\_sltu} + \mathtt{is\_xor} + \mathtt{is\_or} + \mathtt{is\_and} + \mathtt{is\_sll} \\ &+ \mathtt{is\_srl} + \mathtt{is\_sra} + \mathtt{is\_beq} + \mathtt{is\_bne} + \mathtt{is\_blt} + \mathtt{is\_bge} + \mathtt{is\_bltu} + \mathtt{is\_bgeu}\\ &+ \mathtt{is\_ecall} + \mathtt{is\_ebreak} - \mathtt{op\_b\_flag}) = 0 \end{array}$$

Setting $\mathtt{is\_add}=1$, $\mathtt{op\_b\_flag}=1$ and all the other flags to be 0 ensures that the above constraint is satisfied. Note that this assignement of values to the flag is consistent with the prior constraints.

3. Ensuring that $\mathtt{imm\_c}=1$ for all non-ALU instructions

$$\small \begin{array}{ll} & {/\!\!/\, \texttt{Ensuring that } \mathtt{imm\_c=1} \texttt{ for all non-ALU instructions}} \\[1pt] &(\mathtt{is\_lui} + \mathtt{is\_auipc} + \mathtt{is\_jal} + \mathtt{is\_jalr} + \mathtt{is\_ecall} + \mathtt{is\_ebreak} + \mathtt{is\_sb} \\ &+ \mathtt{is\_sh} + \mathtt{is\_sw} + \mathtt{is\_lb} + \mathtt{is\_lh} + \mathtt{is\_lw} + \mathtt{is\_lbu} + \mathtt{is\_lhu} + \mathtt{is\_beq} \\ &+ \mathtt{is\_bne} + \mathtt{is\_blt} + \mathtt{is\_bge} + \mathtt{is\_bltu} + \mathtt{is\_bgeu} )(1 - \mathtt{imm\_c}) = 0 \end{array}$$

4. Matching the instruction flag with the instruction opcode

In the case of the ADD and ADDI instructions, this corresponds to the following constraint:

$$\small (\mathtt{is\_add}) \cdot (\mathtt{opcode} − \mathtt{ADD}) = 0$$

$\mathtt{opcode}$ is set to match the constant corresponding to $\mathtt{ADD}$ as $\mathtt{is\_add}$ is set to 1.

5. Checking ALU flags

$$\small \begin{array}{l} {/\!\!/\, \texttt{ALU instructions}} \\[1pt] \bullet \ \mathtt{is\_alu} = \mathtt{is\_add} + \mathtt{is\_sub} + \mathtt{is\_slt} + \mathtt{is\_sltu} + \mathtt{is\_xor} + \mathtt{is\_or} + \mathtt{is\_and} +\\ \ \ \ \mathtt{is\_sll} + \mathtt{is\_srl} + \mathtt{is\_sra} \\[1pt] \bullet \ \mathtt{is\_alu\_imm\_shift} = \mathtt{imm\_c} \cdot (\mathtt{is\_sll} + \mathtt{is\_srl} + \mathtt{is\_sra}) \\[1pt] \bullet \ \mathtt{is\_alu\_imm\_no\_shift} = \mathtt{imm\_c} \cdot (\mathtt{is\_add} + \mathtt{is\_slt} + \mathtt{is\_sltu} \ +\\[1pt] \ \ \ \mathtt{is\_xor} + \mathtt{is\_or} + \mathtt{is\_and}) \\[4pt] {/\!\!/\, \texttt{Type I instructions with non-shift immediate values}} \\[1pt] \bullet \ \mathtt{is\_type\_i\_no\_shift} = \mathtt{is\_load} + \mathtt{is\_alu\_imm\_no\_shift} + \mathtt{is\_jalr} \\[4pt] {/\!\!/\, \texttt{Type I instructions}} \\[1pt] \bullet \ \mathtt{is\_type\_i} = \mathtt{is\_load} + \mathtt{is\_alu\_imm\_no\_shift} + \mathtt{is\_alu\_imm\_shift} + \mathtt{is\_jalr} \\[1pt] \end{array}$$

The new flags above are used to group instructions so the appropriate constraints are enforced subsequently. Since $\mathtt{is\_add}$ and $\mathtt{imm\_c}$ are set to 1, the new flags are set as below to ensure that the constraints are satisfied.

• $\mathtt{is\_alu}$ = 1
• $\mathtt{is\_alu\_imm\_shift}$ = 0 (all the flags on the right have already been set to 0)
• $\mathtt{is\_alu\_imm\_no\_shift}$ = 1
• $\mathtt{is\_type\_i\_no\_shift}$ = 1
• $\mathtt{is\_type\_i}$ = 1

6. Making sure that the decomposition of each operand is correct

$$\small \begin{array}{l} {/\!\!/\, \texttt{Making sure } \mathtt{op\_a} \texttt{ is consistent with intermediate parts}} \\[1pt] \bullet \ (\mathtt{is\_type\_i\_no\_shift}) \cdot (\mathtt{op\_a0} + \mathtt{op\_a1\_4} \cdot 2 - \mathtt{op\_a}) = 0 \\[4pt] {/\!\!/\, \texttt{Range checking the different } \mathtt{op\_a} \texttt{ parts}} \\[1pt] \bullet \ (\mathtt{is\_type\_i\_no\_shift}) \cdot (\mathtt{op\_a0}) \cdot (1-\mathtt{op\_a0}) = 0 \\[1pt] \bullet \ (\mathtt{is\_type\_i\_no\_shift}) \cdot (\mathtt{op\_a1\_4} \in \left[0, 2^{4} - 1\right]) \\[4pt] {/\!\!/\, \texttt{Making sure } \mathtt{op\_b} \texttt{ is consistent with intermediate parts}} \\[1pt] \bullet \ (\mathtt{is\_type\_i\_no\_shift}) \cdot (\mathtt{op\_b0} + \mathtt{op\_b1\_4} \cdot 2 - \mathtt{op\_b}) = 0 \\[4pt] {/\!\!/\, \texttt{Range checking the different } \mathtt{op\_b} \texttt{ parts}} \\[1pt] \bullet \ (\mathtt{is\_type\_i\_no\_shift}) \cdot (\mathtt{op\_b0}) \cdot (1-\mathtt{op\_b1}) = 0 \\[1pt] \bullet \ (\mathtt{is\_type\_i\_no\_shift}) \cdot (\mathtt{op\_b1\_4} \in \left[0, 2^{4} - 1\right]) \\[4pt] {/\!\!/\, \texttt{Making sure } \mathtt{op\_c} \texttt{ is consistent with intermediate parts}} \\[1pt] \bullet \ (\mathtt{is\_type\_i\_no\_shift}) \cdot (\mathtt{op\_c0\_3} + \mathtt{op\_c4\_7} \cdot 2^{4} + \mathtt{op\_c8\_10} \cdot 2^{8} + \mathtt{op\_c11} \cdot 2^{11} - \mathtt{op\_c}) = 0 \\[4pt] {/\!\!/\, \texttt{Range checking the different } \mathtt{op\_c} \texttt{ parts}} \\[1pt] \bullet \ (\mathtt{is\_type\_i\_no\_shift}) \cdot (\mathtt{op\_c0\_3} \in \left[0,2^{4}-1\right]) \\[1pt] \bullet \ (\mathtt{is\_type\_i\_no\_shift}) \cdot (\mathtt{op\_c4\_7} \in \left[0,2^{4}-1\right]) \\[1pt] \bullet \ (\mathtt{is\_type\_i\_no\_shift}) \cdot (\mathtt{op\_c8\_10} \in \left[0,2^{3}-1\right]) \\[1pt] \bullet \ (\mathtt{is\_type\_i\_no\_shift}) \cdot (\mathtt{op\_c11}) \cdot (1-\mathtt{op\_c11}) = 0 \\[4pt] \end{array}$$

With $\mathtt{is\_type\_i\_no\_shift}$ set to 1, and with the additional values for the operands specified previously, the reader can verify that all of the above constraints are satisfied.

7. Performing sign extension to derive operand $\mathtt{c\_val}$ from $\mathtt{op\_c}$

$$\small \begin{array}{l} {/\!\!/\, \texttt{Performing sign extension to compute } \mathtt{c\_val} \texttt{ from } \mathtt{op\_c}} \\[1pt] \bullet \ (\mathtt{is\_type\_i\_no\_shift}) \cdot (\mathtt{op\_c0\_3} + \mathtt{op\_c4\_7} \cdot 2^{4} - \mathtt{c\_val}^{(1)}) = 0 \\[1pt] \bullet \ (\mathtt{is\_type\_i\_no\_shift}) \cdot (\mathtt{op\_c8\_10} + \mathtt{op\_c11} \cdot (2^{5}-1) \cdot 2^{3} - \mathtt{c\_val}^{(2)}) = 0 \\[1pt] \bullet \ (\mathtt{is\_type\_i\_no\_shift}) \cdot (\mathtt{op\_c11} \cdot (2^{8}-1) - \mathtt{c\_val}^{(3)}) = 0 \\[1pt] \bullet \ (\mathtt{is\_type\_i\_no\_shift}) \cdot (\mathtt{op\_c11} \cdot (2^{8}-1) - \mathtt{c\_val}^{(4)}) = 0 \\[4pt] \end{array}$$

As $\mathtt{op\_c11}$ is set to 0, the sign extension fills in 0 in the higher order bits of $\mathtt{c\_val}$. In particular, the prover sets the values for the limbs for $\mathtt{c\_val}$ as below to ensure that the constraints are satisfied.

• $\mathtt{c\_val}^{(1)} =\mathtt{0x03}$
• $\mathtt{c\_val}^{(2)} =\mathtt{0x00}$
• $\mathtt{c\_val}^{(3)} =\mathtt{0x00}$
• $\mathtt{c\_val}^{(4)} = \mathtt{0x00}$

8. Checking the format of the instruction

$$\small \begin{array}{l} {/\!\!/\, \texttt{Checking instruction format for limb 1}} \\[1pt] \bullet \ (\mathtt{is\_alu\_imm\_no\_shift}) \cdot (\mathtt{0b0010011} + \mathtt{op\_a0} \cdot 2^{7} - \mathtt{instr\_val}^{(1)}) = 0 \\[4pt] {/\!\!/\, \texttt{Checking instruction format for limb 2}} \\[1pt] \bullet \ (\mathtt{is\_add}) \cdot (\mathtt{imm\_c}) \cdot (\mathtt{op\_a1\_4} + \mathtt{0b000} \cdot 2^{4} + \mathtt{op\_b\_0} \cdot 2^{7} - \mathtt{instr\_val}^{(2)}) = 0 \\[4pt] {/\!\!/\, \texttt{Checking instruction format for limb 3}} \\[1pt] \bullet \ (\mathtt{is\_type\_i\_no\_shift}) \cdot (\mathtt{op\_b1\_4} + \mathtt{op\_c0\_3} \cdot 2^{4} - \mathtt{instr\_val}^{(3)}) = 0 \\[4pt] {/\!\!/\, \texttt{Checking instruction format for limb 4}} \\[1pt] \bullet \ (\mathtt{is\_type\_i\_no\_shift}) \cdot (\mathtt{op\_c4\_7} + \mathtt{op\_c8\_10} \cdot 2^{4} + \mathtt{op\_c11} \cdot 2^{7} - \mathtt{instr\_val}^{(4)}) = 0 \\[4pt] \end{array}$$

With $\mathtt{is\_type\_i\_no\_shift}$, $\mathtt{is\_alu\_imm\_no\_shift}$, $\mathtt{is\_add}$ and $\mathtt{imm\_c}$ set to be 1, and all the other values in the constraints already set previously, the reader can verify that the above constraints are satisfied by those values.

​

Reading the Contents of Register $\mathtt{x8}$

In order to read the contents of register $\mathtt{op\_b}=\mathtt{x8}$ at the current clock cycle, the CPU component must interact with the register memory component.

In the specification, the interaction with the register memory is captured by a call to the $\mathtt{Read}_{Reg}$ interface with parameters $(\mathtt{op\_b}, \mathtt{clk},1)$, where $1$ indicates that this is the source register $\mathtt{reg1}$, to obtain the value $\mathtt{b\_val}$. Like in the program memory case, the CPU component does not check the consistency of the register memory, which is handled separately by the register memory component.

In the actual implementation, this interface is not explicitly implemented since the trace columns for $\mathtt{op\_b}$, $\mathtt{clk}$, $\mathtt{b\_val}$, $\mathtt{reg1\_addr}$, and $\mathtt{reg1\_val\_cur}$ are shared between the CPU and the register memory components.

As a result of this interaction, $\mathtt{reg1\_addr}$ will be set to $\mathtt{op\_b}$. Moreover, the value of the limbs for $\mathtt{b\_val}$ will be set to the limbs of $\mathtt{reg1\_val\_cur}$:

• $\mathtt{{b\_val}^{(1)}}$ = $\mathtt{{reg1\_val\_cur}^{(1)}}$ = $\mathtt{0xFF}$
• $\mathtt{{b\_val}^{(2)}}$ = $\mathtt{{reg1\_val\_cur}^{(2)}}$ = $\mathtt{0x00}$
• $\mathtt{{b\_val}^{(3)}}$ = $\mathtt{{reg1\_val\_cur}^{(3)}}$ = $\mathtt{0x00}$
• $\mathtt{{b\_val}^{(4)}}$ = $\mathtt{{reg1\_val\_cur}^{(4)}}$ = $\mathtt{0x00}$

The values of the 4 limbs of $\mathtt{b\_val}$ follow from the fact that, by assumption, register $\mathtt{op\_b}=\mathtt{x8}$ contains $\mathtt{0x00000000FF}$ before the execution of the ADDI instruction.

​

Executing the Instruction

In order to execute the instruction ADDI x10 x8 3 at the current clock cycle, the CPU component must interact with the execution component.

In the specification, the interaction with the execution memory is captured by a call to the $\mathtt{exec}$ interface with parameters $(\mathtt{pc}, \mathtt{opcode},\mathtt{a\_val},\mathtt{b\_val},\mathtt{c\_val})$ to obtain the value $\mathtt{pc\_next}$. Since this is an ADD operation, the execution component also updates the value of $\mathtt{a\_val}$.

In the actual implementation, this interface is not explicitly implemented since the trace columns for $\mathtt{pc}$, $\mathtt{opcode}$, $\mathtt{a\_val}$, $\mathtt{b\_val}$, $\mathtt{c\_val}$, and $\mathtt{pc\_next}$ are shared between the CPU and the execution components.

As a result of this interaction, the values of the limbs for $\mathtt{a\_val}$ $\mathtt{pc\_next}$ will be updated as follows:

• $\mathtt{{a\_val}^{(1)}}$ = $\mathtt{0x02}$
• $\mathtt{{a\_val}^{(2)}}$ = $\mathtt{0x01}$
• $\mathtt{{a\_val}^{(3)}}$ = $\mathtt{0x00}$
• $\mathtt{{a\_val}^{(4)}}$ = $\mathtt{0x00}$
• $\mathtt{{pc\_next}^{(1)}}$ = $\mathtt{0x08}$
• $\mathtt{{pc\_next}^{(2)}}$ = $\mathtt{0x00}$
• $\mathtt{{pc\_next}^{(3)}}$ = $\mathtt{0x00}$
• $\mathtt{{pc\_next}^{(4)}}$ = $\mathtt{0x00}$

The values of the 4 limbs of $\mathtt{a\_val}$ follow from the fact that $\mathtt{b\_val}=\mathtt{0x000000FF}$ and $\mathtt{c\_val}=\mathtt{0x00000003}$. While the value of $\mathtt{b\_val}$ is based on current state of the virtual machine at the current clock cycle, $\mathtt{c\_val}$ follows from the sign extension of $\mathtt{op\_c}=3$.

The values of the 4 limbs of $\mathtt{pc\_next}$ follow from the fact that $\mathtt{pc}=\mathtt{0x00000004}$ gets incremented by $4$ after an ADD instruction.

​

Updating the contents of register $\mathtt{x10}$

In order to update the contents of register $\mathtt{op\_a}=\mathtt{x10}$ at the current clock cycle, the CPU component must interact with the register memory component.

To do so, the CPU first needs to ensure that the value of register $\mathtt{x0}$ remains $0$. For that, the CPU component uses an auxiliary value $\mathtt{a\_val\_effective}$, which is supposed to be equal to $\mathtt{a\_val}$ whenever $\mathtt{op\_a} \not= 0$ and $0$ otherwise. This is enforced via the following set of constraints.

$$\small \begin{array}{l} {/\!\!/\, \texttt{Determining } \mathtt{a\_val\_effective} \texttt{ from } \mathtt{op\_a}} \\[1pt] {/\!\!/\, \mathtt{a\_val\_effective\_flag} \texttt{ is an auxiliary flag}} \\[1pt] {/\!\!/\, \mathtt{a\_val\_effective\_flag\_\{aux,aux\_inv\}} \texttt{ are non-zero auxiliary variables}} \\[1pt] {/\!\!/\, \mathtt{a\_val\_effective\_flag = 1} \texttt{ indicates } \mathtt{op\_a \not= 0}} \\[1pt] {/\!\!/\, \mathtt{a\_val\_effective\_flag = 0} \texttt{ indicates } \mathtt{op\_a = 0}} \\[1pt] \bullet \ \mathtt{op\_a} \cdot \mathtt{a\_val\_effective\_flag\_aux} = \mathtt{a\_val\_effective\_flag} \\[4pt] {/\!\!/\, \texttt{Ensuring } \mathtt{a\_val\_effective\_flag\_aux \not= 0}} \\[1pt] \bullet \ \mathtt{a\_val\_effective\_flag\_aux} \cdot \mathtt{a\_val\_effective\_flag\_aux\_inv} = 1 \\[4pt] {/\!\!/\, \texttt{Enforcing } \mathtt{a\_val\_effective\_flag} \in \{0,1\}} \\[1pt] \bullet \ (\mathtt{a\_val\_effective\_flag}) \cdot (1-\mathtt{a\_val\_effective\_flag}) = 0 \\[4pt] {/\!\!/\, \texttt{Enforcing relation between } \mathtt{a\_val} \texttt{ and } \mathtt{a\_val\_effective}} \\[1pt] \bullet \ \mathtt{a\_val^{(1)}} \cdot \mathtt{a\_val\_effective\_flag} = \mathtt{a\_val\_effective^{(1)}} \\%[4pt] \bullet \ \mathtt{a\_val^{(2)}} \cdot \mathtt{a\_val\_effective\_flag} = \mathtt{a\_val\_effective^{(2)}} \\%[4pt] \bullet \ \mathtt{a\_val^{(3)}} \cdot \mathtt{a\_val\_effective\_flag} = \mathtt{a\_val\_effective^{(3)}} \\%[4pt] \bullet \ \mathtt{a\_val^{(4)}} \cdot \mathtt{a\_val\_effective\_flag} = \mathtt{a\_val\_effective^{(4)}} \\[4pt] \end{array}$$

Since $\mathtt{op\_a} = \mathtt{x10}$, the following must be true:

• $\mathtt{a\_val\_effective\_flag}$ = $1$
• $\mathtt{a\_val\_effective\_flag\_aux}$ = $1/10$
• $\mathtt{a\_val\_effective\_flag\_aux\_inv}$ = $10$
• $\mathtt{{a\_val\_effective}^{(1)}}$ = $\mathtt{{a\_val}^{(1)}}$ = $\mathtt{0x02}$
• $\mathtt{{a\_val\_effective}^{(2)}}$ = $\mathtt{{a\_val}^{(2)}}$ = $\mathtt{0x01}$
• $\mathtt{{a\_val\_effective}^{(3)}}$ = $\mathtt{{a\_val}^{(3)}}$ = $\mathtt{0x00}$
• $\mathtt{{a\_val\_effective}^{(4)}}$ = $\mathtt{{a\_val}^{(4)}}$ = $\mathtt{0x00}$

Next, the CPU component must interact with the register memory component to update the contents of register $\mathtt{op\_a} = \mathtt{x10}$ with the value $\mathtt{a\_val\_effective}$.

In the specification, the interaction with the register memory is captured by a call to the $\mathtt{Write}_{Reg}$ interface with parameters $(\mathtt{op\_a}, \mathtt{a\_val\_effective},\mathtt{clk},3)$, where $3$ indicates that this is the destination register $\mathtt{reg3}$, to write the value $\mathtt{a\_val\_effective}$. As before, the CPU component does not check the consistency of the register memory, which is handled separately by the register memory component.

In the actual implementation, this interface is not explicitly implemented since the trace columns for $\mathtt{op\_a}$, $\mathtt{clk}$, $\mathtt{a\_val\_effective}$, $\mathtt{reg3\_addr}$, and $\mathtt{reg3\_val\_cur}$ are shared between the CPU and the register memory components.

As a result of this interaction, the values of the limbs for $\mathtt{reg3\_val\_cur}$ associated with address $\mathtt{reg3\_addr}=\mathtt{op\_a} = \mathtt{x10}$ will be updated as follows:

• $\mathtt{{reg3\_val\_cur}^{(1)}}$ = $\mathtt{{a\_val\_effective}^{(1)}}$ = $\mathtt{0x02}$
• $\mathtt{{reg3\_val\_cur}^{(2)}}$ = $\mathtt{{a\_val\_effective}^{(2)}}$ = $\mathtt{0x01}$
• $\mathtt{{reg3\_val\_cur}^{(3)}}$ = $\mathtt{{a\_val\_effective}^{(3)}}$ = $\mathtt{0x00}$
• $\mathtt{{reg3\_val\_cur}^{(4)}}$ = $\mathtt{{a\_val\_effective}^{(4)}}$ = $\mathtt{0x00}$

​

Execution Component Trace Columns and Constraints

In order to verify the correct execution of the ADDI x10 x8 3 instruction at clock cycle $256$, the execution component first enforces that the ADD operation is executed via the following set of constraints:

$$\small \begin{array}{l} {/\!\!/\, \texttt{Carry handling for the add instruction}} \\[1pt] \bullet \ (\mathtt{is\_add}) \cdot \left( \mathtt{op\_a\_val}^{(1)} + \mathtt{h\_carry}^{(1)} \cdot 2^{8} - \mathtt{op\_b\_val}^{(1)} - \mathtt{op\_c\_val}^{(1)} \right) = 0 \\[1pt] \bullet \ (\mathtt{is\_add}) \cdot \left( \mathtt{op\_a\_val}^{(2)} + \mathtt{h\_carry}^{(2)} \cdot 2^{8} - \mathtt{op\_b\_val}^{(2)} - \mathtt{op\_c\_val}^{(2)} - \mathtt{h\_carry}^{(1)} \right) = 0 \\[1pt] \bullet \ (\mathtt{is\_add}) \cdot \left( \mathtt{op\_a\_val}^{(3)} + \mathtt{h\_carry}^{(3)} \cdot 2^{8} - \mathtt{op\_b\_val}^{(3)} - \mathtt{op\_c\_val}^{(3)} - \mathtt{h\_carry}^{(2)} \right) = 0 \\[1pt] \bullet \ (\mathtt{is\_add}) \cdot \left( \mathtt{op\_a\_val}^{(4)} + \mathtt{h\_carry}^{(4)} \cdot 2^{8} - \mathtt{op\_b\_val}^{(4)} - \mathtt{op\_c\_val}^{(4)} - \mathtt{h\_carry}^{(3)} \right) = 0 \\[4pt] {/\!\!/\, \texttt{Enforcing that helper carries are binary}} \\[1pt] \bullet \ (\mathtt{is\_add}) \cdot \left( \mathtt{h\_carry}^{(1)} \right) \cdot \left(1 - \mathtt{h\_carry}^{(1)}\right) = 0 \\[1pt] \bullet \ (\mathtt{is\_add}) \cdot \left( \mathtt{h\_carry}^{(2)} \right) \cdot \left(1 - \mathtt{h\_carry}^{(2)}\right) = 0 \\[1pt] \bullet \ (\mathtt{is\_add}) \cdot \left( \mathtt{h\_carry}^{(3)} \right) \cdot \left(1 - \mathtt{h\_carry}^{(3)}\right) = 0 \\[1pt] \bullet \ (\mathtt{is\_add}) \cdot \left( \mathtt{h\_carry}^{(4)} \right) \cdot \left(1 - \mathtt{h\_carry}^{(4)}\right) = 0 \\[4pt] \end{array}$$

Since $\mathtt{b\_val} = \mathtt{0x000000FF}$ and $\mathtt{c\_val} = \mathtt{0x00000003}$, in order to satisfy the set of constraints above, it must be the case that:

• $\mathtt{{a\_val}^{(1)}}$ = $\mathtt{0x02}$
• $\mathtt{{a\_val}^{(2)}}$ = $\mathtt{0x01}$
• $\mathtt{{a\_val}^{(3)}}$ = $\mathtt{0x00}$
• $\mathtt{{a\_val}^{(4)}}$ = $\mathtt{0x00}$
• $\mathtt{{h\_carry}^{(1)}}$ = $1$
• $\mathtt{{h\_carry}^{(2)}}$ = $0$
• $\mathtt{{h\_carry}^{(3)}}$ = $0$
• $\mathtt{{h\_carry}^{(4)}}$ = $0$

Next, the execution component checks whether this instruction is one of those for which $\mathtt{pc}$ gets incremented by $4$ (which is the case for $\texttt{ADDI}$). This is done via the following set of constraints:

$$\small \begin{array}{l} {/\!\!/\, \texttt{Check if instruction is one that pc is incremented}} \\[1pt] \bullet \ (\mathtt{is\_alu} + \mathtt{is\_load} + \mathtt{is\_type\_s} + \mathtt{is\_type\_u} + \\[1pt] \ \ \ \mathtt{is\_type\_sys} \cdot (1 - \mathtt{is\_sys\_halt}) - \mathtt{is\_pc\_inc\_std}) = 0 \\[4pt] {/\!\!/\, \texttt{pc is incremented by 4 handling two limbs at a time}} \\[1pt] {/\!\!/\, \mathtt{pc\_carry} \texttt{ is used to keep track of carries}} \\[1pt] \bullet \ (\mathtt{is\_pc\_inc\_std}) \cdot (\mathtt{pc\_next}^{(1)} + \mathtt{pc\_next}^{(2)} \cdot 2^{8} + \mathtt{pc\_carry}^{(1)} \cdot 2^{16} \\[1pt] \ \ \ - \mathtt{pc}^{(1)} - \mathtt{pc}^{(2)} \cdot 2^{8} - 4) = 0 \\[1pt] \bullet \ (\mathtt{is\_pc\_inc\_std}) \cdot (\mathtt{pc\_next}^{(3)} + \mathtt{pc\_next}^{(4)} \cdot 2^{8} + \mathtt{pc\_carry}^{(2)} \cdot 2^{16} \\[1pt] \ \ \ - \mathtt{pc}^{(3)} - \mathtt{pc}^{(4)} \cdot 2^{8} - \mathtt{pc\_carry}^{(1)}) = 0 \\[4pt] {/\!\!/\, \texttt{Ensuring } \mathtt{pc\_carry} \texttt{ is binary}} \\[1pt] \bullet \ (\mathtt{is\_pc\_inc\_std}) \cdot \left( \mathtt{pc\_carry}^{(1)} \right) \cdot \left(1 - \mathtt{pc\_carry}^{(1)}\right) = 0 \\[1pt] \bullet \ (\mathtt{is\_pc\_inc\_std}) \cdot \left( \mathtt{pc\_carry}^{(2)} \right) \cdot \left(1 - \mathtt{pc\_carry}^{(2)}\right) = 0 \\[4pt] \end{array}$$

Since $\mathtt{pc} = \mathtt{0x00000004}$, it must be the case that carries $\mathtt{pc\_next}$ should be set as follows:

• $\mathtt{{pc\_next}^{(1)}}$ = $\mathtt{0x08}$
• $\mathtt{{pc\_next}^{(2)}}$ = $\mathtt{0x00}$
• $\mathtt{{pc\_next}^{(3)}}$ = $\mathtt{0x00}$
• $\mathtt{{pc\_next}^{(4)}}$ = $\mathtt{0x00}$
• $\mathtt{{pc\_carry}^{(1)}}$ = $0$
• $\mathtt{{pc\_carry}^{(2)}}$ = $0$

​

Program Memory Component Trace Columns and Constraints

As mentioned in the Proving Memory section, the program memory component uses well-known offline memory checking techniques to maintain the consistency of the read accesses to the program memory. Since this is a read-only memory, the program memory component only requires a simplified version of the offline memory checking technique, in which each memory cell is associated with a counter that keeps track of the number of times a particular memory cell has been read.

More precisely, the program memory component defines the following set of trace elements:

• $\mathtt{pc}$: the word-aligned base address associated with a program instruction
• $\mathtt{{instr\_val}^{(1)}}$: bits 0-7 of the instruction word $\mathtt{{instr\_val}}$ stored at address $\mathtt{pc}$
• $\mathtt{{instr\_val}^{(2)}}$: bits 8-15 of the instruction word $\mathtt{{instr\_val}}$ stored at address $\mathtt{pc}+1$
• $\mathtt{{instr\_val}^{(3)}}$: bits 16-23 of the instruction word $\mathtt{{instr\_val}}$ stored at address $\mathtt{pc}+2$
• $\mathtt{{instr\_val}^{(4)}}$: bits 24-31 of the instruction word $\mathtt{{instr\_val}}$ stored at address $\mathtt{pc}+3$
• $\mathtt{prog\_ctr\_prev}$: 4 limbs for the previous counter value associated with base address $\mathtt{pc}$
• $\mathtt{prog\_ctr\_cur}$: 4 limbs for the current counter value associated with base address $\mathtt{pc}$
• $\mathtt{prog\_read\_digest}$: a digest of the read set, used for logups
• $\mathtt{prog\_write\_digest}$: a digest of the write set, used for logups

To enforce the consistency of the read accesses, every time a read operation takes place, the program memory component performs the following actions:

• it checks that the counter associated with the address being accessed is updated correctly; and
• it verifies that the digests of the read and write sets are correctly updated.

​

Enforcing the correct update of access counters

In order to enforce the correct update of access counters, the program memory component verifies that the following set of constraints are satisfied.

$$\small \begin{array}{l} {/\!\!/\, \texttt{Enforcing } \mathtt{prog\_ctr\_cur} = \mathtt{prog\_ctr\_prev} + 1} \\[1pt] {/\!\!/\, \mathtt{prog\_ctr\_carry} \texttt{ used for carry handling}} \\[1pt] \bullet \ \mathtt{{prog\_ctr\_prev}^{(1)}} + 1 - \mathtt{{prog\_ctr\_carry}^{(1)}} \cdot 2^{8} - \mathtt{{prog\_ctr\_cur}^{(1)}} \\%[4pt] \bullet \ \mathtt{{prog\_ctr\_prev}^{(2)}} + \mathtt{{prog\_ctr\_carry}^{(1)}} - \mathtt{{prog\_ctr\_carry}^{(2)}} \cdot 2^{8} - \mathtt{{prog\_ctr\_cur}^{(2)}} \\%[4pt] \bullet \ \mathtt{{prog\_ctr\_prev}^{(3)}} + \mathtt{{prog\_ctr\_carry}^{(2)}} - \mathtt{{prog\_ctr\_carry}^{(3)}} \cdot 2^{8} - \mathtt{{prog\_ctr\_cur}^{(3)}} \\%[4pt] \bullet \ \mathtt{{prog\_ctr\_prev}^{(4)}} + \mathtt{{prog\_ctr\_carry}^{(3)}} - \mathtt{{prog\_ctr\_carry}^{(4)}} \cdot 2^{8} - \mathtt{{prog\_ctr\_cur}^{(4)}} \\[4pt] {/\!\!/\, \texttt{Enforcing } \mathtt{{prog\_ctr\_carry}^{(j)}} \in \{0,1\} \texttt{ for } j=1,2,3,4} \\[1pt] \bullet \ (\mathtt{{prog\_ctr\_carry}^{(1)}}) \cdot (1-\mathtt{{prog\_ctr\_carry}^{(1)}}) = 0 \\%[4pt] \bullet \ (\mathtt{{prog\_ctr\_carry}^{(2)}}) \cdot (1-\mathtt{{prog\_ctr\_carry}^{(2)}}) = 0 \\%[4pt] \bullet \ (\mathtt{{prog\_ctr\_carry}^{(3)}}) \cdot (1-\mathtt{{prog\_ctr\_carry}^{(3)}}) = 0 \\%[4pt] \bullet \ (\mathtt{{prog\_ctr\_carry}^{(4)}}) \cdot (1-\mathtt{{prog\_ctr\_carry}^{(4)}}) = 0 \\[4pt] \end{array}$$

Since $Prog[\mathtt{0x00000004}]$ has been accessed $2$ times before the current clock cycle according to the initial assumption, we have:

• $\mathtt{{prog\_ctr\_prev}^{(1)}}=2$
• $\mathtt{{prog\_ctr\_prev}^{(2)}}=0$
• $\mathtt{{prog\_ctr\_prev}^{(3)}}=0$
• $\mathtt{{prog\_ctr\_prev}^{(4)}}=0$

As a result, in order to satisfy the constraints above, the following must be true:

• $\mathtt{{prog\_ctr\_cur}^{(1)}}=3$
• $\mathtt{{prog\_ctr\_cur}^{(2)}}=0$
• $\mathtt{{prog\_ctr\_cur}^{(3)}}=0$
• $\mathtt{{prog\_ctr\_cur}^{(4)}}=0$
• $\mathtt{{prog\_ctr\_carry}^{(1)}}=0$
• $\mathtt{{prog\_ctr\_carry}^{(2)}}=0$
• $\mathtt{{prog\_ctr\_carry}^{(3)}}=0$
• $\mathtt{{prog\_ctr\_carry}^{(4)}}=0$

​

Enforcing the Correct Update of Read- and Write-Set Digests

Let $\mathtt{fp}(\mathtt{pc},\mathtt{instr\_val}, \mathtt{prog\_ctr})$ denote a fingerprint function which takes as input the tuple $(\mathtt{{pc}^{(1)}}$, $\ldots$, $\mathtt{{pc}^{(4)}}$, $\mathtt{{instr\_val}^{(1)}}$, $\ldots$, $\mathtt{{instr\_val}^{(4)}}$, $\mathtt{{prog\_ctr}^{(1)}}$, $\ldots$, $\mathtt{{prog\_ctr}^{(4)}})$ and returns a field element in the secure extension field used by $\mathtt{Stwo}$ using a random value $\beta$ chosen by the verifier.

In order to ensure that the digests for the read and write sets are updated correctly, one needs to make sure that the logup contribution associated with the entry $(\mathtt{pc}$, $\mathtt{instr\_val}$, $\mathtt{prog\_ctr\_prev})$ gets added to the read set digest and that the logup contribution associated with the entry $(\mathtt{pc}$, $\mathtt{instr\_val}$, $\mathtt{prog\_ctr\_cur})$ gets added to the write set digest.

More precisely, the following set of transition constraints need to be enforced by the program memory component, where $\alpha$ is a random value chosen by the verifier and $i>0$ is the row index:

$$\small \begin{array}{l} \bullet \ \mathtt{prog\_read\_digest}[i] - \mathtt{prog\_read\_digest}[i-1] = \\[1pt] \ \ \ {1} / {(\mathtt{fp}(\mathtt{pc}[i],\mathtt{instr\_val}[i],\mathtt{prog\_ctr\_prev}[i])+\alpha)} \\[1pt] \bullet \ \mathtt{prog\_write\_digest}[i] - \mathtt{prog\_write\_digest}[i-1] = \\[1pt] \ \ \ {1} / {(\mathtt{fp}(\mathtt{pc}[i], \mathtt{instr\_val}[i], \mathtt{prog\_ctr\_cur}[i])+\alpha)}.\\[1pt] \end{array}$$

As stated before,

• $\mathtt{{pc}^{(1)}}[255]=0x04$
• $\mathtt{{pc}^{(2)}}[255]=0x00$
• $\mathtt{{pc}^{(3)}}[255]=0x00$
• $\mathtt{{pc}^{(4)}}[255]=0x00$
• $\mathtt{{instr\_val}^{(1)}}[255]$ = $Prog[\mathtt{0x00000004}]$ = $\mathtt{0b00010011}$
• $\mathtt{{instr\_val}^{(2)}}[255]$ = $Prog[\mathtt{0x00000005}]$ = $\mathtt{0b00000101}$
• $\mathtt{{instr\_val}^{(3)}}[255]$ = $Prog[\mathtt{0x00000006}]$ = $\mathtt{0b00110100}$
• $\mathtt{{instr\_val}^{(4)}}[255]$ = $Prog[\mathtt{0x00000007}]$ = $\mathtt{0b00000000}$

Therefore, the following constraints must be satisfied:

$$\small \begin{array}{l} \bullet \ \mathtt{prog\_read\_digest}[255] - \mathtt{prog\_read\_digest}[254] = \\[1pt] \ \ \ {1} / {(\mathtt{fp}(\mathtt{pc}[255],\mathtt{instr\_val}[255],\mathtt{prog\_ctr\_prev}[255])+\alpha)} \\[1pt] \bullet \ \mathtt{prog\_write\_digest}[255] - \mathtt{prog\_write\_digest}[254] = \\[1pt] \ \ \ {1} / {(\mathtt{fp}(\mathtt{pc}[255], \mathtt{instr\_val}[255], \mathtt{prog\_ctr\_cur}[255])+\alpha)}.\\[1pt] \end{array}$$

Remark: In addition to the above specified constraints, the limbs for $\mathtt{instr\_val}$, $\mathtt{prog\_ctr\_prev}$ and $\mathtt{prog\_ctr\_curv}$ have range checks specified to ensure they encode the correct number of bits. Here we only note that the above set values satisfy the range constraints, and refer the reader to the formal specification for further details.

​

Register Memory Component Trace Columns and Constraints

Like the program memory component, the register memory component uses well-known offline memory checking techniques to maintain the consistency of read and write accesses to the register memory. However, since this is a read-write memory, the register memory component needs to associate a timestamp to each memory cell in order to keep track of the last time a particular memory cell has been accessed.

As in the program memory component, the register memory also makes use of logups to check the consistency between the read and write sets, where each element of the set has the form $(\mathtt{reg\_addr}$, $\mathtt{reg\_val}$, $\mathtt{reg\_ts})$ indicating that the value $\mathtt{reg\_val}$ was written to address $(\mathtt{reg\_addr}$ at time $\mathtt{reg\_ts}$.

Hence, to properly handle an access to a register address, one needs to maintain a set $(\mathtt{reg\_addr}$, $\mathtt{reg\_val\_prev}$, $\mathtt{reg\_val\_cur}$, $\mathtt{reg\_ts\_prev}$, $\mathtt{reg\_ts\_cur})$ consisting of the register address, the previous and current values for that address, and previous and current time stamps. Moreover, since up to three register addresses can be accessed during an execution cycle, the register memory component defines 3 such sets of values.

More precisely, the program memory component defines the following set of trace elements:

• $\mathtt{clk}$: the current execution time
• $\mathtt{reg1\_addr}$, $\mathtt{reg2\_addr}$, $\mathtt{reg3\_addr}$: register addresses
• $\mathtt{reg1\_val\_cur}$, $\mathtt{reg2\_val\_cur}$, $\mathtt{reg3\_val\_cur}$: 32-bit values used to update register contents
• $\mathtt{reg1\_ts\_cur}$, $\mathtt{reg2\_ts\_cur}$, $\mathtt{reg3\_ts\_cur}$: current timestamps for the registers
• $\mathtt{reg1\_val\_prev}$, $\mathtt{reg2\_val\_prev}$, $\mathtt{reg3\_val\_prev}$: previous 32-bit values stored at the registers
• $\mathtt{reg1\_ts\_prev}$, $\mathtt{reg2\_ts\_prev}$, $\mathtt{reg3\_ts\_prev}$: previous timestamps for the registers
• $\mathtt{reg\_read\_digest}$: a digest of the read set, used for logups.
• $\mathtt{reg\_write\_digest}$: a digest of the write set, used for logups.
• $\mathtt{reg1\_accessed}$, $\mathtt{reg2\_accessed}$, $\mathtt{reg3\_accessed}$: flags indicating whether the set of trace elements $(\mathtt{reg}j\mathtt{\_addr}$, $\mathtt{reg}j\mathtt{\_val\_prev}$, $\mathtt{reg}j\mathtt{\_val\_cur}$, $\mathtt{reg}j\mathtt{\_ts\_prev}$, $\mathtt{reg}j\mathtt{\_ts\_cur})$ for $j=1,2,3$ are being used

To enforce the consistency of the read and write accesses to the register memory, the register memory component performs the following actions:

1. it ensures that the current timestamps associated for $\mathtt{reg1\_addr}$, $\mathtt{reg2\_addr}$, $\mathtt{reg3\_addr}$ satisfy the following constraints:

• $\mathtt{reg1\_ts\_cur} = 3 \cdot \mathtt{clk} - 2$
• $\mathtt{reg2\_ts\_cur} = 3 \cdot \mathtt{clk} - 1$
• $\mathtt{reg3\_ts\_cur} = 3 \cdot \mathtt{clk}$

2. it checks that the previous timestamps associated with the addresses being accessed preceed their current timestamps. That is,

• $\mathtt{reg1\_ts\_prev} \in \{0,\ldots,\mathtt{reg1\_ts\_cur-1}\}$
• $\mathtt{reg2\_ts\_prev} \in \{0,\ldots,\mathtt{reg2\_ts\_cur-1}\}$
• $\mathtt{reg3\_ts\_prev} \in \{0,\ldots,\mathtt{reg3\_ts\_cur-1}\}$

3. it verifies that the digests of the read and write sets are correctly updated.

Below, we provide more details about the third step and we refer the reader to the formal specification for further details on the first two checks.

Remark: As stated in the specification, $\mathtt{reg1\_addr}$, $\mathtt{reg2\_addr}$, $\mathtt{reg3\_addr}$ should be accessed in this order and only $\mathtt{reg3\_addr}$ can be modified in a given clock cycle.

​

Enforcing the Correct Update of Read- and Write-Set Digests

Let $\mathtt{fp}(\mathtt{reg\_addr},\mathtt{reg\_val}, \mathtt{reg\_ts})$ denote a fingerprint function which takes as input the tuple $(\mathtt{reg\_addr}$, $\mathtt{{reg\_val}^{(1)}}$, $\ldots$, $\mathtt{{reg\_val}^{(4)}}$, $\mathtt{{reg\_ts}^{(1)}}$, $\ldots$, $\mathtt{{reg\_ts}^{(4)}})$ and returns a field element in the secure extension field used by $\mathtt{Stwo}$ using a random value $\beta$ chosen by the verifier.

In order to ensure that the digests for the read and write sets are updated correctly, one needs to make sure that, whenever a register $\mathtt{reg\_addr}$ is accessed in a clock cycle, the logup contribution associated with the entry $(\mathtt{reg\_addr}$, $\mathtt{reg\_val}$, $\mathtt{reg\_ts\_prev})$ must be added to the read set digest and that the logup contribution associated with the entry $(\mathtt{reg\_addr}$, $\mathtt{reg\_val}$, $\mathtt{reg\_ts\_cur})$ must be added to the write set digest.

More precisely, the following set of transition constraints need to be enforced by the register memory component, where $\alpha$ is a random value chosen by the verifier and $i>0$ is the row index:

$$\small \begin{array}{l} \bullet \ \mathtt{reg\_read\_digest}[i] - \mathtt{reg\_read\_digest}[i-1] = \\ \ \ \ {\mathtt{reg1\_accessed}[i]} / {(\mathtt{fp}(\mathtt{reg1\_addr}[i],\mathtt{reg1\_val}[i],\mathtt{reg1\_ts\_prev}[i])+\alpha)} \ + \\[1pt] \ \ \ {\mathtt{reg2\_accessed}[i]} / {(\mathtt{fp}(\mathtt{reg2\_addr}[i],\mathtt{reg2\_val}[i],\mathtt{reg2\_ts\_prev}[i])+\alpha)} \ + \\[1pt] \ \ \ {\mathtt{reg3\_accessed}[i]} / {(\mathtt{fp}(\mathtt{reg3\_addr}[i],\mathtt{reg3\_val}[i],\mathtt{reg3\_ts\_prev}[i])+\alpha)} \\[1pt] \bullet \ \mathtt{reg\_write\_digest}[i] - \mathtt{reg\_write\_digest}[i-1] = \\ \ \ \ {\mathtt{reg1\_accessed}[i]} / {(\mathtt{fp}(\mathtt{reg1\_addr}[i], \mathtt{reg1\_val}[i], \mathtt{reg1\_ts\_cur}[i])+\alpha)} \ + \\[1pt] \ \ \ {\mathtt{reg2\_accessed}[i]} / {(\mathtt{fp}(\mathtt{reg2\_addr}[i], \mathtt{reg2\_val}[i], \mathtt{reg3\_ts\_cur}[i])+\alpha)} \ + \\[1pt] \ \ \ {\mathtt{reg3\_accessed}[i]} / {(\mathtt{fp}(\mathtt{reg3\_addr}[i], \mathtt{reg3\_val}[i], \mathtt{reg3\_ts\_cur}[i])+\alpha)}. \\[1pt] \end{array}$$

According to the assumptions used for the current example, we have

• $R[\mathtt{x8}] = \mathtt{0x000000FF}$ was last updated with timestamp $32$;and
• $R[\mathtt{x10}] = \mathtt{0x00000005}$ was last updated with timestamp $7$.

Moreover, based on the interactions with the other components and the constraints for the current timestamps, we also know the following:

• $\mathtt{clk}[255] = 256$
• $\mathtt{reg1\_ts\_cur}[255] = 3 \cdot 256 - 2 = 766$
• $\mathtt{reg3\_ts\_cur}[255] = 3 \cdot 256 = 768$
• $\mathtt{reg1\_accessed}[255] = 1$
• $\mathtt{reg2\_accessed}[255] = 0$
• $\mathtt{reg3\_accessed}[255] = 1$
• $R[\mathtt{x10}]$ gets updated to $\mathtt{0x00000102}$ at the current clock cycle

Hence, to satisfy the logup constraints mentioned above for $i=255$, the following must be true for the current clock cycle:

• $\mathtt{{reg1\_ts\_prev}^{(1)}}[255]=32$
• $\mathtt{{reg1\_ts\_prev}^{(2)}}[255]=0$
• $\mathtt{{reg1\_ts\_prev}^{(3)}}[255]=0$
• $\mathtt{{reg1\_ts\_prev}^{(4)}}[255]=0$
• $\mathtt{{reg1\_val\_prev}^{(1)}}[255]=\mathtt{{reg1\_val\_cur}^{(1)}}[255]=\mathtt{0xFF}$
• $\mathtt{{reg1\_val\_prev}^{(2)}}[255]=\mathtt{{reg1\_val\_cur}^{(2)}}[255]=\mathtt{0x00}$
• $\mathtt{{reg1\_val\_prev}^{(3)}}[255]=\mathtt{{reg1\_val\_cur}^{(3)}}[255]=\mathtt{0x00}$
• $\mathtt{{reg1\_val\_prev}^{(4)}}[255]=\mathtt{{reg1\_val\_cur}^{(4)}}[255]=\mathtt{0x00}$
• $\mathtt{{reg1\_ts\_cur}^{(1)}}[255] = 254$
• $\mathtt{{reg1\_ts\_cur}^{(2)}}[255] = 2$
• $\mathtt{{reg1\_ts\_cur}^{(3)}}[255] = 0$
• $\mathtt{{reg1\_ts\_cur}^{(4)}}[255] = 0$
• $\mathtt{{reg3\_ts\_prev}^{(1)}}[255]=7$
• $\mathtt{{reg3\_ts\_prev}^{(2)}}[255]=0$
• $\mathtt{{reg3\_ts\_prev}^{(3)}}[255]=0$
• $\mathtt{{reg3\_ts\_prev}^{(4)}}[255]=0$
• $\mathtt{{reg3\_val\_prev}^{(1)}}[255]=\mathtt{0x05}$
• $\mathtt{{reg3\_val\_prev}^{(2)}}[255]=\mathtt{0x00}$
• $\mathtt{{reg3\_val\_prev}^{(3)}}[255]=\mathtt{0x00}$
• $\mathtt{{reg3\_val\_prev}^{(4)}}[255]=\mathtt{0x00}$
• $\mathtt{{reg3\_ts\_cur}^{(1)}}[255]=0$
• $\mathtt{{reg3\_ts\_cur}^{(2)}}[255]=3$
• $\mathtt{{reg3\_ts\_cur}^{(3)}}[255]=0$
• $\mathtt{{reg3\_ts\_cur}^{(4)}}[255]=0$
• $\mathtt{{reg3\_val\_cur}^{(1)}}[255]=\mathtt{0x02}$
• $\mathtt{{reg3\_val\_cur}^{(2)}}[255]=\mathtt{0x01}$
• $\mathtt{{reg3\_val\_cur}^{(3)}}[255]=\mathtt{0x00}$
• $\mathtt{{reg3\_val\_cur}^{(4)}}[255]=\mathtt{0x00}$