Hermez zkEVM

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

Hermez zkEVM
Proof of Efficiency: zk-rollups
Polygon zkEVM 状态机设计原理
zkEVM 类型
Polygon zkEM 合约
Polygon zkEVM 整体架构
Polygon zkEVM zkProver设计
zkSync 2.0升级内容
ZK EVM

本文主要对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$ . 下图展示了数值状态机的设计图：

image

扩展主状态机

基于主状态机，可以将其扩展5个寄存器，添加一个arith 标签，将数值状态机边上主状态机。当airth 标签为1的时候，允许检查数值运算。整体的设计图如下所示：

image

下图展示了如何连接两个状态机，关键点在于当 flag 值为1时，需要确何寄存器的值当 $lathch$ 值为1时在数值表中存在，即数值表的约束条件成立。因为，需要保证以下包含关系：

image

[arith \cdot A , arith \cdot B , arith \cdot C , arith \cdot D, arith \cdot op] \subset [latch \cdot \mathcal{A} , latch \cdot \mathcal{B} , latch \cdot \mathcal{C} , latch \cdot \mathcal{D} , latch \cdot \mathcal{E}]

从下图可以看出，我们采用Plookup 连接主状态机和其它具体的状态机。

image

它可以允许以模块化方式设计虚拟状态机，最后采用零知识证明技术验证。

参考

https://docs.hermez.io/zkEVM/architecture/introduction/

https://eprint.iacr.org/2020/315.pdf

Hermez zkEVM
本文主要对Hermez 2.0 zkEVM设计思路进行简单介绍。 Fibonacci 状态机先从Fibonacc...
Proof of Efficiency: zk-rollups
PoE是Polygon Hermez 为zkEVM实现设计的一种新的共识机制，它基于之前的PoD（Proof ...
Polygon zkEVM 状态机设计原理
Polygon zkEVM是兼容EVM的zkRollup Layer 2 方案。zkEVM 证明的第一步是构建交易...
zkEVM 类型
PSE: 第1种类型Polygon Hermez 和 Scroll : 第2或3种类型zkSync和MatterL...
Polygon zkEM 合约
Bridge 合约 Bridge 合约同时部署在Ethereum 和 Polygon Hermez 网络上，用于实...
Polygon zkEVM 整体架构
Polygon zkEVM 是EVM的zkRollup方案，可以提供智能合约支持，用以提升以太坊的可扩展性。架构...
Polygon zkEVM zkProver设计
zkProver主要完成批量交易的证明，是Polygon zkEVM的关键组件。下图展示了zkProver和Nod...
zkSync 2.0升级内容
zkSync2.0 是EVM兼容的zkRollup程序模型，zkEVM将于5月上线测试网，8月上线主网。 Zinc...
ZK EVM
目前zkEVM主要有两种策略：直接支持EVM现有指令集，兼容solidity 指令集，使用这种方案的是主要是He...

Hermez zkEVM

Fibonacci 状态机

状态机证明

简单的状态机

选择条件

管理条件选择

程序执行的证明

证明执行路径的恒等式

模块化设计

分而治之

数值状态机

扩展主状态机

参考

相关文章

Hermez zkEVM

Proof of Efficiency: zk-rollups

Polygon zkEVM 状态机设计原理

zkEVM 类型

Polygon zkEM 合约

Polygon zkEVM 整体架构

Polygon zkEVM zkProver设计

zkSync 2.0升级内容

ZK EVM

网友评论

延伸阅读

深度阅读

栏目导航

热点阅读