Hermez zkEVM

作者: 雪落无留痕 | 来源:发表于2022-03-08 15:15 被阅读0次

本文主要对Hermez 2.0 zkEVM设计思路进行简单介绍。

Fibonacci 状态机

先从Fibonacci状态机示例开始，Fibonacci是一个序列，可以通过两个寄存器A和B表示的状态机：

Fibonacci Sequence

初始条件为： $A_1=0, B_1=1$ , 并且寄存器的状态满足以下关系：
$A_{i+1}=B_i \\ B_{i+1}=A_i + B_i$
可以将寄存器的状态表示为多项式 $\mathbb{Z}_p[x]$ , 定义域为 $H=\{\omega, \omega^2, \cdots, w^8=1\}$ 为 $\mathbb{Z}_p^*$ 上的8次单位根。可以得到以下关系：
$A(w^i)=A_i \\ B(w^i)=B_i$
将寄存器状态进一步表示为恒等关系式为：
$A(x\omega)=\vert_HB(X) \\ B(x\omega)=\vert_HA(X) + B(X)$
但是这个恒等关系并不完全成立：

寄存器是非循环的，当在 $w^8$ 估值时：

$A(w^9)=A(w)=0\ne21=B(w^8) \\ B(w^9)=B(w)=1\neq34=A(w^8)+B(w^8)$

可以改变初始条件，例如 $(2,4)$ , 同样满足恒等关系。

为了解决这些问题，可以添加一个辅助寄存器C:

Fibonacci Sequence Aux

C 对应的多项式为：
$C(w^i)=C_i \longrightarrow C=[1,0,0,0,0,0,0,0]$
通过辅助寄存器，新的多项式恒等关系为：
$A(xw)=|_HB(x)(1-C(xw)) \\ B(xw)=|_H(A(x)+B(x))(1-C(xw))+C(xw)$
当 $x=w^8$ 时，恒等关系满足：
$A(w^9)=A(w)=0=B(w^8)(1-C(x)) \\ B(w^9)=B(w)=1=(A(w^8)+B(w^8))(1-C(w))+C(w)$
若初始条件为： $(A_1,B_1)$ ，多项式恒等关系为：
$A(xw)=|_HB(x)(1-C(xw))+A_1C(xw) \\ B(xw)=|_H(A(x)+B(x))(1-C(xw))+B_1C(xw)$
上例中： $(A_1,B_1)=(0,1)$

状态机证明

Polynomial Commitment

多项式关系可以通过多项式承诺证明，例如 Kate 和基于FRI的承诺。

多项式承诺满足 binding 和 hiding的关系。

简单的状态机

状态机可以表示为下图过程：

image

下述汇编指令表示带有两个寄存器 A 和 B, 接受一个外部输入：
$\begin{array}{|l|} \hline \mathbf{Instruction} \\ \hline \mathbf{FREELOAD}~A \\ \hline \mathbf{MOV}~B~3 \\ \hline \mathbf{ADD}~A~B \\ \hline \mathbf{STOP} \\ \hline \end{array}$
其中：

$\mathbf{FREELOAD}\ X$ : 将一个输入的值保存到寄存器 X；
$\mathbf{MOV}\ X\ a$ : 将一个常量移动到寄存器 X ;
$\mathbf{ADD}\ A\ B$ : 将寄存器 A 和 B的值加在一起，将输入保存到寄存器 A 中；

当输入为7的时候，执行的路径为：
$\begin{array}{|l|c|c|c|c|c|} \hline \mathbf{Instruction} & \mathbf{freeIn} & \mathbf{A} & \mathbf{A^{+1}} & \mathbf{B} & \mathbf{B^{+1}} \\ \hline \mathbf{FREELOAD}~~A & 7 & 0 & 7 & 0 & 0 \\ \hline \mathbf{MOV}~~B~3 & 0 & 7 & 7 & 0 & 3 \\ \hline \mathbf{ADD}~~A~B & 0 & 7 & 10 & 3 & 3 \\ \hline \mathbf{STOP} & 0 & 10 & 0 & 3 & 0 \\ \hline \end{array}$
在上述的指令中， $X^{+1}$ 表示寄存器 $X\in\{A,B\}$ 的下一步的状态。

$\mathbf{STOP}$ 指令会重置状态的值。

可以在脱离指令的情况下，通过一系列值推导寄存器的下一个状态。此时，需要添加辅助状态和选择子（selectors）来表示这种关系。寄存器 A 和 B 更新的状态是辅助寄存器和选择子的线性关系，如下图所示：

image

其中：

$\mathbf{inX_i}\in \{0, 1\}$ : 选择子，用以包含寄存器 $X_i$ 是否在线性组合中；
$\mathbf{setX_i}\in \{0,1\}$ : 选择子，以表示是否将线性组合的结果保存到寄存器 $X_{i+1}$ 中；
$\mathbf{freeln}$ : 包含执行程序的输入；
$\mathbf{const}$ : 包含指令的固定值。

通过引入输助变量，可以得到下述的表格：
$\scriptsize \begin{array}{|l|} \hline \mathbf{Instruction} \\ \hline \mathbf{FREELOAD}~~A \\ \hline \mathbf{MOV}~~B~3 \\ \hline \mathbf{ADD}~~A~B \\ \hline \mathbf{STOP} \\ \hline \end{array} \hspace{0.1cm} \begin{array}{|c|c|c|c|c|c|c|c|} \hline \textbf{freeIn} & \textbf{const} & \textbf{setB} & \textbf{setA} & \textbf{inFreeIn} & \textbf{inB} & \textbf{inA} \\ \hline 7 & 0 & 0 & 1 & 1 & 0 & 0 \\ \hline 0 & 3 & 1 & 0 & 0 & 0 & 0 \\ \hline 0 & 0 & 0 & 1 & 0 & 1 & 1 \\ \hline 0 & 0 & 1 & 1 & 0 & 0 & 0 \\ \hline \end{array} \hspace{0.1cm} \begin{array}{|c|c|c|c|} \hline \mathbf{A} & \mathbf{A^{+1}} & \mathbf{B} & \mathbf{B^{+1}} \\ \hline 0 & 7 & 0 & 0\\ \hline 7 & 7 & 0 & 3\\ \hline 7 & 10 & 3 & 3\\ \hline 10 & 0 & 3 & 0\\ \hline \end{array}$
因此寄存器代数表达式的关系为：
$\begin{aligned} &\mathsf{A_{i+1}} = \mathsf{A_i} + \mathsf{setA_i} \cdot (\mathsf{inA_i} \cdot \mathsf{A_i} + \mathsf{inB_i} \cdot \mathsf{B_i} + \mathsf{inFreeIn}_i \cdot \mathsf{freeIn_i} + \mathsf{const_i} - \mathsf{A_i}), \\ &\mathsf{B_{i+1}} = \mathsf{B_i} + \mathsf{setB_i} \cdot (\mathsf{inA_i} \cdot \mathsf{A_i} + \mathsf{inB_i} \cdot \mathsf{B_i} + \mathsf{inFreeIn}_i \cdot \mathsf{freeIn_i} + \mathsf{const_i} - \mathsf{B_i}). \end{aligned}$
可以将寄存器状态表示为四步的多项式 $\mathbb{Z}_p[x]$ , 定义域为： $H=\{w, w^2,w^3,w^4=1\}$ , 可以定义一个循环关系：
$\begin{aligned} &\mathsf{A}(x\omega) = \mathsf{A}(x) + \mathsf{setA}(x) \cdot (\mathsf{inA}(x) \cdot \mathsf{A}(x) + \mathsf{inB}(x) \cdot \mathsf{B}(x) + \mathsf{inFreeIn}(x) \cdot \mathsf{freeIn}(x) + \mathsf{const}(x) - \mathsf{A}(x)), \\ &\mathsf{B}(x\omega) = \mathsf{B}(x) + \mathsf{setB}(x) \cdot (\mathsf{inA}(x) \cdot \mathsf{A}(x) + \mathsf{inB}(x) \cdot \mathsf{B}(x) + \mathsf{inFreeIn}(x) \cdot \mathsf{freeIn}(x) + \mathsf{const}(x) - \mathsf{B}(x)). \end{aligned}$
则程序执行完全由常量（公开）多项式： $\mathsf{inA(x), inB(x), setA(x), setB(x), inFreeIn(x)}$ 和 $\mathsf{const(x)}$ 表示。

多项式 $\mathsf{freeIn(x)}$ 可以公开的承诺的多项式，对于同一个程序，可以在不同的初始条件下进行执行。

在上述程序中，执行结果为 $A(\omega^4)$ 。

选择条件

下面将在汇编程序中添加 $\bf{JMPIZ}$ 指令，若执行操作为0， $\bf{JMPIZ}$ 将会跳到指定的位置。

在下面的程序中， $\bf{JMPIZ}$ 会跳到位置 4 ，若 $\mathbf{Add}\ A\ B$ 为0的话。
$\begin{array}{|c|l|} \hline \textbf{Position} & \mathbf{Instruction} \\ \hline 0 & \mathbf{FREELOAD}~~A \\ \hline 1 & \mathbf{MOV}~~B~-3 \\ \hline 2 & \mathbf{ADD}~~A~B,~\mathbf{JMPIZ}~~4 \\ \hline 3 & \mathbf{ADD}~~A~B \\ \hline 4 & \mathbf{STOP} \\ \hline \end{array}$
当出现条件语句的时候，执行路径的长度不是固定的，依赖于公开输入：
$\scriptsize \begin{array}{|l|c|c|c|c|c|} \hline \mathbf{Instruction} & \mathbf{freeIn} & \mathbf{A} & \mathbf{A^{+1}} & \mathbf{B} & \mathbf{B^{+1}} \\ \hline \mathbf{FREELOAD}~~A & 7 & 0 & 7 & 0 & 0 \\ \hline \mathbf{MOV}~~B~-3 & 0 & 7 & 7 & 0 & -3 \\ \hline \mathbf{ADD}~~A~B,~\mathbf{JMPIZ}~~4 & 0 & 7 & 4 & -3 & -3 \\ \hline \mathbf{ADD}~~A~B & 0 & 4 & 1 & -3 & -3 \\ \hline \mathbf{STOP} & 0 & 1 & 0 & -3 & 0 \\ \hline \end{array}$

$\scriptsize \begin{array}{|l|c|c|c|c|c|} \hline \mathbf{Instruction} & \mathbf{freeIn} & \mathbf{A} & \mathbf{A^{+1}} & \mathbf{B} & \mathbf{B^{+1}} \\ \hline \mathbf{FREELOAD}~~A & 3 & 0 & 3 & 0 & 0 \\ \hline \mathbf{MOV}~~B~-3 & 0 & 3 & 3 & 0 & -3 \\ \hline \mathbf{ADD}~~A~B,~\mathbf{JMPIZ}~~4 & 0 & 3 & 0 & -3 & -3 \\ \hline \mathbf{STOP} & 0 & 0 & 0 & -3 & 0 \\ \hline \end{array}$

第一执行步骤是5步，每二个是4步。

管理条件选择

可以引入一种新的模型，管理条件选择(conditional jump)：

image

上述添加了 $\bf{Program Counter (PC)}$ , PC是一种特别的寄存器，包含程序执行指定的位置。

使用 $op_i$ 表示状态机的线性组合，用以简化约束条件的描述，如下所示：
$\mathsf{op}_i := \mathsf{inA_i} \cdot \mathsf{A_i} + \mathsf{inB_i} \cdot \mathsf{B_i} + \mathsf{inFreeIn}_i \cdot \mathsf{freeIn_i} + \mathsf{const_i}.$

image

若 $op_i$ 为0， $\mathbf{JMPIZ}$ 指令将会跳到地址 $addr_i$ . 下面将介绍如何检查 $op_i$ 是否为0.

为了检查域 $\mathbb{Z}_p$ 的某个元素是否为0，可以通过 $a$ 是否有逆元素判断。若 $a\ne0$ , $a$ 有一个乘法逆元。

因此可以使用下述定义，限制 $\mathbf{isZero}$ 检查。
$\begin{aligned} &\mathsf{isZero}_i := (1 - \mathsf{op}_i \cdot \mathsf{op}_i^{-1}), \\ &\mathsf{isZero}_i \cdot \mathsf{op}_i = 0. \end{aligned}$
可以把这两个方程合成一个约束：
$\mathsf{isZero}_i \cdot \mathsf{op}_i = 0,~~\mathsf{isZero}_i = (1 - \mathsf{op}_i \cdot \mathsf{op}_i^{-1})~~\rightarrow~~(1 - \mathsf{op}_i \cdot \mathsf{op}_i^{-1}) \cdot \mathsf{op}_i = 0.$
可以引入下述机制以引入 jumps:

image

上述添加一个选择子 $\mathbf{selMPIZ_i}\in \{0,1\}$ , 以编码 $\mathbf{JMPIZ}$ 指令，并表述 $\bf{PC}$ 的行为。则约束集合如下所示：
$\begin{aligned} & \mathsf{op_i} := \mathsf{inA_i}\cdot \mathsf{A_i}+\mathsf{inB_i}\cdot B_i+\mathsf{inFreeIn_i}\cdot \mathsf{freeIn_i}+const_i, \\ & PC_{i+1} =PC_i + 1 +selJMPIZ_i\cdot (1 - op_i\cdot op_i^{-1})\cdot(addr_i -PC_i-1), \\ & (1-\mathsf{op_i}\cdot \mathsf{op_i^{-1}})\cdot \mathsf{op_i}=0. \end{aligned}$
由以上可知：

若 $op_i \ne 0$ , 则 $PC_{i+1}=PC_i+ 1$ ;
若 $op_i=0$ , 则 $PC_{i+1}=addr_i$ .

则公开输入为分别为7 和 3的时候，执行路径分别为：
$\tiny \begin{array}{|l|} \hline \mathbf{Instruction} \\ \hline \mathbf{FREELOAD}~~A \\ \hline \mathbf{MOV}~~B~-3 \\ \hline \mathbf{ADD}~~A~B,~\mathbf{JMPIZ}~~4 \\ \hline \mathbf{ADD}~~A~B \\ \hline \mathbf{STOP} \\ \hline \end{array} \hspace{0.1cm} \begin{array}{|c|c|c|c|c|c|c|c|c|c|c|} \hline \textbf{freeIn} & \textbf{const} & \textbf{addr} & \textbf{selJMPIZ} & \textbf{setB} & \textbf{setA} & \textbf{inFreeIn} & \textbf{inB} & \textbf{inA} & \textbf{op} & \textbf{invOp} \\ \hline 7 & 0 & 0 & 0 & 0 & 1 & 1 & 0 & 0 & 7 & 7^{-1} \\ \hline 0 & -3 & 0 & 0 & 1 & 0 & 0 & 0 & 0 & -3 & (-3)^{-1} \\ \hline 0 & 0 & 4 & 1 & 0 & 1 & 0 & 1 & 1 & \mathbf{\color{blue!75!black} 4} & \mathbf{\color{blue!75!black} 4^{-1}} \\ \hline 0 & 0 & 0 & 0 & 0 & 1 & 0 & 1 & 1 & 1 & 1 \\ \hline 0 & 0 & 0 & 1 & 1 & 1 & 0 & 0 & 0 & 0 & 0 \\ \hline \end{array} \hspace{0.1cm} \begin{array}{|c|c|c|c|c|c|} \hline \mathbf{PC} & \mathbf{PC^{+1}} & \mathbf{A} & \mathbf{A^{+1}} & \mathbf{B} & \mathbf{B^{+1}} \\ \hline 0 & 1 & 0 & 7 & 0 & 0\\ \hline 1 & 2 & 7 & 7 & 0 & -3\\ \hline 2 & 3 & 7 & 4 & -3 & -3\\ \hline 3 & 4 & 4 & 1 & -3 & -3\\ \hline 4 & 0 & 1 & 0 & -3 & 0\\ \hline \end{array}$

$\tiny \begin{array}{|l|} \hline \mathbf{Instruction} \\ \hline \mathbf{FREELOAD}~~A \\ \hline \mathbf{MOV}~~B~-3 \\ \hline \mathbf{ADD}~~A~B,~\mathbf{JMPIZ}~~4 \\ \hline \mathbf{STOP} \\ \hline \end{array} \hspace{0.1cm} \begin{array}{|c|c|c|c|c|c|c|c|c|c|c|c|} \hline \textbf{freeIn} & \textbf{const} & \textbf{addr} & \textbf{selJMPIZ} & \textbf{setB} & \textbf{setA} & \textbf{inFreeIn} & \textbf{inB} & \textbf{inA} & \textbf{op} & \textbf{invOp} \\ \hline 3 & 0 & 0 & 0 & 0 & 1 & 1 & 0 & 0 & 3 & 3^{-1} \\ \hline 0 & -3 & 0 & 0 & 1 & 0 & 0 & 0 & 0 & -3 & (-3)^{-1} \\ \hline 0 & 0 & 4 & 1 & 0 & 1 & 0 & 1 & 1 & \mathbf{\color{blue!75!black} 0} & \mathbf{\color{blue!75!black} \alpha} \\ \hline 0 & 0 & 0 & 1 & 1 & 1 & 0 & 0 & 0 & 0 & 0 \\ \hline \end{array} \hspace{0.1cm} \begin{array}{|c|c|c|c|c|c|} \hline \mathbf{PC} & \mathbf{PC^{+1}} & \mathbf{A} & \mathbf{A^{+1}} & \mathbf{B} & \mathbf{B^{+1}} \\ \hline 0 & 1 & 0 & 3 & 0 & 0\\ \hline 1 & 2 & 3 & 3 & 0 & -3\\ \hline 2 & 4 & 3 & 0 & -3 & -3\\ \hline 4 & 0 & 0 & 0 & -3 & 0\\ \hline \end{array}$

其中 $\mathbf{invOp}$ 列表示为 $\mathbf{op}$ 的逆。

并且 $\mathbf{PC}$ 是非常重要的寄存器，因为它可以修改指令序列的执行方式。

目前多项式没有经过预处理，表格的值不仅依赖于程序，还依赖输入的值。因此，需要保证待验证的程序是正确的。

程序执行的证明

目前为止，可以证明每个指令都正确执行，但是怎么证明正确执行了指定的程序指令？需要检查每个执行的指令在我们的程序中，但是如何简洁实现这种证明方式？

为了实现这个目标，我们提供了每个指令的编码方式，并且检查每个执行指令的编码确实在程序的指令中。

首先来展示如何对指令编码，作为一个简单示例，采用4位编码一个指令（实际中可能需要32位编码），4位编码如下所示：
$\begin{array}{|c|c|c|c|c|c|c|c|c|c|c|c|c|} \hline -8 & -7 & -6 & ... & -2 & -1 & 0 & 1 & 2 & ... & 6 & 7 & 8 \\ \hline 1000 & 1001 & 1010 & ... & 1110 & 1111 & 0000 & 0001 & 0010 & ... & 0110 & 0111 & 1000 \\ \hline \end{array}$
去掉数值 $-8=8$ , 采用 -7 到 7的范围，可以编码 $\mathbb{Z}_p$ 的域元素为：
$\begin{array}{|c|c|c|c|c|c|c|c|c|c|c|} \hline -7 & -6 & ... & -2 & -1 & 0 & 1 & 2 & ...& 6 & 7 \\ \hline p-7 & p-6 & ... & p-2 & p-1 & 0 & 1 & 2 & ...& 6 & 7 \\ \hline \end{array}$
因此可以约束 $const(x) \in \{p-7, p-6, \cdots, p-2, p-1,0,1,2,3,\cdots,6,7\}.$

可以约束上述的条件为：
$const(x) + 7 \in \{0,1,2,\cdots,14\}$
直接以2为底表示 $const(x) + 7$ , 以避免sum 运算。

下面将介绍如何编码程序执行的每个一指令。
$\scriptsize \begin{array}{|c|l|} \hline \mathbf{Instruction} \\ \hline \mathbf{FREELOAD}~~A \\ \hline \mathbf{MOV}~~B~-3 \\ \hline \mathbf{ADD}~~A~B,~\mathbf{JMPIZ}~~4 \\ \hline \mathbf{ADD}~~A~B \\ \hline \mathbf{STOP} \\ \hline \end{array} \hspace{0.1cm} \begin{array}{|c|c|c|c|c|c|c|c|c|c|c|} \hline \mathbf{\color{blue!75!black} \textbf{const+7}} & \textbf{addr} & \textbf{selJMPIZ} & \textbf{setB} & \textbf{setA} & \textbf{inFreeIn} & \textbf{inB} & \textbf{inA} & \textbf{instruction code} \\ \hline \mathbf{\color{blue!75!black} 7} & 0 & 0 & 0 & 1 & 1 & 0 & 0 & 0111.0000.001100 \\ \hline \mathbf{\color{blue!75!black} 4} & 0 & 0 & 1 & 0 & 0 & 0 & 0 & 0100.0000.010000 \\ \hline \mathbf{\color{blue!75!black} 7} & 4 & 1 & 0 & 1 & 0 & 1 & 1 & 0111.0100.101011 \\ \hline \mathbf{\color{blue!75!black} 7} & 0 & 0 & 0 & 1 & 0 & 1 & 1 & 0111.0000.001011 \\ \hline \mathbf{\color{blue!75!black} 7} & 0 & 1 & 1 & 1 & 0 & 0 & 0 & 0111.0000.111000 \\ \hline \end{array}$
可以通过下面的规则编码指令：
$\textsf{instruction}_i := 2^{13}\cdot(\textsf{const}_i + 7) + 2^9\cdot \textsf{addr}_i + 2^5\cdot \textsf{selJMPIZ}_i + 2^4 \cdot \textsf{setB}_i + 2^3 \cdot \textsf{setA}_i + 2^2 \cdot \textsf{inFreeIn}_i + 2 \cdot \textsf{inB}_i + \textsf{inA}_i.$
另外，需要检查选择子是二进制的， $\mathbf{addr}$ 由4位组成，即 $addr_i \in \{0,1,\cdots, 15\}$

当 $const_i + 7 =7$ , 其表示 $const_i = 0$ .

为了证明该程序，每个指令通过其代码和位置唯一识别，上例中采用4位来表示位置。

定义 $\mathbf{ROM}$ , 由每个指令和位置来定义表示：
$ROM_i := 2^{17}\cdot position_i +instruction_i.$
因此相应的 $ROM$ 表示为：
$\begin{array}{|c|c|} \hline \textbf{Position} & \mathbf{Instruction} \\ \hline 0 & \mathbf{FREELOAD}~~A \\ \hline 1 & \mathbf{MOV}~~B~-3 \\ \hline 2 & \mathbf{ADD}~~A~B,~\mathbf{JMPIZ}~~4 \\ \hline 3 & \mathbf{ADD}~~A~B \\ \hline 4 & \mathbf{STOP} \\ \hline \end{array} \hspace{0.1cm} \begin{array}{|c|} \hline \textbf{ROM} \\ \hline 0000.0111.0000.001100 \\ \hline 0001.0100.0000.010000 \\ \hline 0010.0111.0100.101011 \\ \hline 0011.0111.0000.001011 \\ \hline 0100.0111.0000.111000 \\ \hline \end{array}$
我们可以采用 $PC$ 来编码程序路径：
$\scriptsize \begin{array}{|c|c|c|c|c|c|} \hline \mathbf{PC} \\ \hline 0 \\ \hline 1 \\ \hline 2 \\ \hline 3 \\ \hline 4 \\ \hline \end{array} \hspace{0.1cm} \begin{array}{|c|c|c|} \hline \mathbf{Instruction} \\ \hline \mathbf{FREELOAD}~~A \\ \hline \mathbf{MOV}~~B~-3 \\ \hline \mathbf{ADD}~~A~B,~\mathbf{JMPIZ}~~4 \\ \hline \mathbf{ADD}~~A~B \\ \hline \mathbf{STOP} \\ \hline \end{array} \hspace{0.1cm} \begin{array}{|c|c|c|c|c|c|c|c|c|} \hline \textbf{const+7} & \textbf{addr} & \textbf{selJMPIZ} & \textbf{setB} & \textbf{setA} & \textbf{inFreeIn} & \textbf{inB} & \textbf{inA} \\ \hline 7 & 0 & 0 & 0 & 1 & 1 & 0 & 0 \\ \hline 4 & 0 & 0 & 1 & 0 & 0 & 0 & 0 \\ \hline 7 & 4 & 1 & 0 & 1 & 0 & 1 & 1 \\ \hline 7 & 0 & 0 & 0 & 1 & 0 & 1 & 1 \\ \hline 7 & 0 & 1 & 1 & 1 & 0 & 0 & 0 \\ \hline \end{array} \hspace{0.1cm} \begin{array}{|c|c|c|c|c|c|} \hline \mathbf{insTrace} \\ \hline 0000.0111.0000.001100 \\ \hline 0001.0100.0000.010000 \\ \hline 0010.0111.0100.101011 \\ \hline 0011.0111.0000.001011 \\ \hline 0100.0111.0000.111000 \\ \hline \end{array}$

$\scriptsize \begin{array}{|c|c|c|c|c|c|} \hline \mathbf{PC} \\ \hline 0 \\ \hline 1 \\ \hline 2 \\ \hline 4 \\ \hline \end{array} \hspace{0.1cm} \begin{array}{|c|c|c|} \hline \mathbf{Instruction} \\ \hline \mathbf{FREELOAD}~~A \\ \hline \mathbf{MOV}~~B~-3 \\ \hline \mathbf{ADD}~~A~B,~\mathbf{JMPIZ}~~4 \\ \hline \mathbf{STOP} \\ \hline \end{array} \hspace{0.1cm} \begin{array}{|c|c|c|c|c|c|c|c|c|c|} \hline \textbf{const+7} & \textbf{addr} & \textbf{selJMPIZ} & \textbf{setB} & \textbf{setA} & \textbf{inFreeIn} & \textbf{inB} & \textbf{inA} \\ \hline 7 & 0 & 0 & 0 & 1 & 1 & 0 & 0 \\ \hline 4 & 0 & 0 & 1 & 0 & 0 & 0 & 0 \\ \hline 7 & 4 & 1 & 0 & 1 & 0 & 1 & 1 \\ \hline 7 & 0 & 1 & 1 & 1 & 0 & 0 & 0 \\ \hline \end{array} \hspace{0.1cm} \begin{array}{|c|c|c|c|c|c|} \hline \mathbf{insTrace} \\ \hline 0000.0111.0000.001100 \\ \hline 0001.0100.0000.010000 \\ \hline 0010.0111.0100.101011 \\ \hline 0100.0111.0000.111000 \\ \hline \end{array}$

其中 $STOP$ 指令设置 $PC$ 值为0，使这个多项式构成循环。

那该如何检查执行了指定的程序了呢？

这时可以采用Plookup协议，检查对应的项目被正确有执行，采用Plookup 检查：
$\mathbf{insTrace(x)\subset \mathbf{ROM}(x)}$
由此表明，若指令的trace 包含在程序的ROM中，则执行的指令是实际的程序。

证明执行路径的恒等式

$\begin{aligned} & A(x\omega) = A(x) + setA(x)\cdot (op(x)-A(x)), \\ & B(x\omega)=B(x)+ setB(x)\cdot(op(x)-B(x)), \\ & PC(x\omega)=P(x) + 1 + selJMPIZ(x)\cdot (1-op(x)\cdot invOp(x))\cdot(addr(x)-PC(x)-1), \\ & (1-op(x)\cdot invOp(x))\cdot op(x)=0. \end{aligned}$

其中：
$op(x) := inA(x)\cdot A(x) + inB(x)\cdot B(x) + inFreeIn(x)\cdot freeIn(x) + const(x).$
并且，我们还需要添加下述的检查：
$$
\begin{aligned}
& const(x) + 7 \subset {0,1,\cdots,14}, \
& addr(x) \subset {0,1,\cdots, 15}, \
& position(x)\subset {0,1,\cdots, 15}, \
& PC(x) \subset {0,1,\cdots, 15}, \
& insTrace(x) \subset \mathsf{ROM}(x).

\end{aligned}
$并且相关的定义如下：$
\begin{aligned}
& \textsf{instruction}(x) := 2^{13}(\textsf{const(x)}+7)+ 2^9 \cdot addr(x) + 2^5\cdot \textsf{selJMPIZ}(x)+ 2^4\cdot \textsf{setB}(x) + 2^3\cdot \textsf{setA}(x)+ 2^2\cdot \textsf{inFreeIn}(x)+ 2\cdot \textsf{inB}(x) + \textsf{inA}(x), \
& \textsf{ROM}(x) := 2^{17} \cdot \textsf{position}(x) + \textsf{instruction}(x), \
& \textsf{insTrace}(x):= 2^{17}\cdot \textsf{PC(x)} + \textsf{instruction}(x).
\end{aligned}
$$

最后，需要检查一系列选择子是二进制的，即：

$\textsf{inA}(x)\cdot(\textsf{inA}(x)-1)=0, \textsf{setA}(x)\cdot(\textsf{setA}(x)-1)=0, \\ \textsf{inB}(x)\cdot (\textsf{inB}(x)-1)=0, \textsf{setB}(x)\cdot(\textsf{setB}(x)-1)=0, \\ \textsf{inFreeIn}(x)\cdot(\textsf{inFreeIn(x)}-1)=0, \textsf{selJMPIZ}(x)\cdot(\textsf{selJMPIZ}(x)-1)=0.$
关于状态机中的多项式：

需要对多项式 $\textsf{inFreeIn}(x), \textsf{inA}(x), \textsf{inB}(x), \textsf{setA}(x), \textsf{setB}(x), \textsf{A}(x), \textsf{B}(x), \textsf{const}(x), \textsf{selJMPIZ(x), \textsf{invOp}(x), \textsf{position}(x)}$ 和 $\textsf{PC}(x)$ 进行承诺；
惟一需要预处理的多项式为： $\textsf{ROM}(x)$

模块化设计

分而治之

对上面的思路进一步扩展，例如要处理乘法运算。

可以通过增加列的方式，来表述这这些运算，但是这将导致设计异常复杂难以处理。但是我们可以采用divide and conquer 策略：

zk-EVM 架构由多个不同的相互连接的状态机构成；
每个状态机证明其相应任务的执行路径；
不同状态机的相关列多项式通过 inclusion proofs 关联在一起（采用plookup）。

下面将通过一个示例展现这个过程：

设计一个状态机执行32位的数值操作；
通过inclusion proof 将该状态机和主状态机连在一起。

数值状态机

数值状态机能够执行32位的 sum, substraction, multiplication, division的运算，采用如下所示的5个寄存器：
$\mathcal{A}_i \cdot \mathcal{B}_i + \mathcal{C}_i = 2^{32} \mathcal{D}_i + \mathcal{E}_i.$
可以将上述关系表示为一个在子群 ${H}$ 上的循环多项式的恒等式，即：
$\mathcal{A}(x)\cdot \mathcal{B}(x)+\mathcal{C}(x)= 2^{32}\mathcal{D}(x)+\mathcal{E}(x)$
注意需要约束 $\mathcal{A}(x),\mathcal{B}(x), \mathcal{C}(x), \mathcal{D}(x), \mathcal{E}(x)$ 在定义域 $H$ 的值为 32 bit.

设计如下状态机检查上述的操作：
$\tiny \begin{array}{|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|} \hline \textbf{set}\mathcal{A} & \textbf{set}\mathcal{B} & \textbf{set}\mathcal{C} & \textbf{set}\mathcal{D} & \textbf{set}\mathcal{E} & \textbf{latch} & \textbf{freeIn} & \mathcal{A} & \mathcal{A'} & \mathcal{B} & \mathcal{B'} & \mathcal{C} & \mathcal{C'} & \mathcal{D} & \mathcal{D'} & \mathcal{E} & \mathcal{E'}\\ \hline 1 & 0 & 0 & 0 & 0 & 0 & 0x0003 & 0 & 0x003 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0\\ \hline 0 & 1 & 0 & 0 & 0 & 0 & 0x0002 & 0x0003 & 0x0003 & 0 & 0x0002 & 0 & 0 & 0 & 0 & 0 & 0\\ \hline 0 & 0 & 1 & 0 & 0 & 0 & 0x0004 & 0x0003 & 0x0003 & 0x0002 & 0x0002 & 0 & 0x0004 & 0 & 0 & 0 & 0\\ \hline 0 & 0 & 0 & 1 & 0 & 0 & 0 & 0x0003 & 0x0003 & 0x0002 & 0x0002 & 0x0004 & 0x0004 & 0 & 0 & 0 & 0\\ \hline 0 & 0 & 0 & 0 & 1 & 0 & 0x000a & 0x0003 & 0x0003 & 0x0002 & 0x0002 & 0x0004 & 0x0004 & 0 & 0 & 0 & 0x000a\\ \hline 1 & 0 & 0 & 0 & 0 & \mathbf{1} & 0x1111 & \mathbf{0x0003} & 0x1111 & \mathbf{0x0002} & 0x0002 & \mathbf{0x0004} & 0x0004 & \mathbf{0} & 0 & \mathbf{0x000a} & 0x000a\\ \hline 0 & 1 & 0 & 0 & 0 & 0 & 0x2222 & {0x1111} & 0x1111 & {0x0002} & 0x2222 & {0x0004} & 0x0004 & {0} & 0 & {0x000a} & 0x000a\\ \hline 0 & 0 & 1 & 0 & 0 & 0 & 0x3333 & {0x1111} & 0x1111 & {0x2222} & 0x2222 & {0x0004} & 0x3333 & {0} & 0 & {0x000a} & 0x000a\\ \hline 0 & 0 & 0 & 1 & 0 & 0 & 0x0246 & {0x1111} & 0x1111 & {0x2222} & 0x2222 & {0x3333} & 0x3333 & {0} & 0x0246 & {0x000a} & 0x000a\\ \hline 0 & 0 & 0 & 0 & 1 & 0 & 0xb975 & {0x1111} & 0x1111 & {0x2222} & 0x2222 & {0x3333} & 0x3333 & {0x0246} & 0x0246 & {0x000a} & 0xb975\\ \hline 1 & 0 & 0 & 0 & 0 & \mathbf{1} & 0x7777 & \mathbf{0x1111} & 0x7777 & \mathbf{0x2222} & 0x2222 & \mathbf{0x3333} & 0x3333 & \mathbf{0x0246} & 0x0246 & \mathbf{0xb975} & 0xb975\\ \hline ... & ... & ... & ... & ... & ... & ... & ... & ... & ... & ... & ... & ... & ... & ... & ... & ...\\ \hline \end{array}$
其中 $X'$ 用于表示寄存器 $X$ 的下一个状态。采用 $\mathbf{latch}$ 表示是否已准备好检查 $\mathcal{A},\mathcal{B},\mathcal{C},\mathcal{D},\mathcal{E}$ 实际的值。

其中 $\mathsf{setA},\mathsf{setB}, \mathsf{C}, \mathcal{D}, \mathcal{E}, \mathbf{latch}$ 并不依赖输入，是不变的。

$\mathbf{freeIn}$ 用于包含数值操作的一些值。

因此，定义数值状态机的多项式恒等式如下所示：
$\begin{aligned} \mathcal{A'} &= \mathbf{sel}\mathcal{A}\cdot (\mathbf{freeIn-\mathcal{A}})+\mathcal{A} \\ \mathcal{B'} &= \mathbf{sel}\mathcal{B}\cdot (\mathbf{freeIn}-\mathcal{B})+\mathcal{B} \\ \mathcal{C'} &= \mathbf{sel} \mathcal{C}\cdot (\mathbf{freeIn}-\mathcal{C}) + \mathcal{C} \\ \mathcal{D'} &= \mathbf{sel} \mathcal{D} \cdot (\mathbf{freeIn} - \mathcal{D}) + \mathcal{D} \\ \mathcal{E'} &= \mathcal{sel} \mathcal{E} \cdot (\mathbf{freeIn}- \mathcal{E})+ \mathcal{E} \\ 0 &= [\mathcal{A}\cdot \mathcal{B}+\mathcal{C} - (2^{32}\mathcal{D} + \mathcal{E})]\cdot \mathbf{latch} \\ &\mathbf{freeIn}\subset byte4 \end{aligned}$
因为 $\mathcal{A}, \mathcal{B}, \mathcal{C}, \mathcal{D}, \mathcal{E}$ 的值都来源于 $\mathbf{freeIn}$ ，所以有检查约束条件： $\mathbf{freeIn}\subset byte4$ . 下图展示了数值状态机的设计图：