Polygon zkEVM zkProver设计

作者: 雪落无留痕 | 来源:发表于2022-10-06 00:31 被阅读0次

zkProver主要完成批量交易的证明，是Polygon zkEVM的关键组件。下图展示了zkProver和Node, Database交互的过程。

Node 会发送以太坊状态内容和EVM Merkle 树到DB 中，存储起来；
Node 将批量交易作为zkProver的输入；
zkProver 访问DB, 获取用于生成交易可验证证明数据；
zkProver 生成交易的证明，然后返回给Node.

zkProver 概览

zkProver主要有几个组件：

Executor: 主要负责主状态机执行；
STARK 递归组件：生成STARK 证明；
CIRCOM 库：主要成生成STARK验证电路；
zk-SNARK Prover: 主要生成验证STARK 的SNARK 证明。

zkProver 数据处理流程

Executor

Excutor 是主状态机的执行者，它的输入包括：交易，旧的状态根，新的状态根，ChainID等。另外，executor 需要zkEVM当前状态的值用以构建证明。

Executor 还需要：

ROM: 存储了执行的指令；
PIL: 一系列寄存器的多项式，定义了它们的约束关系；

Executor 实现是汇编语言（zkASM）的解释器，zkASM 用来构建称为zkEVM-ROM的程序，然后由Executor 执行生成合适的执行路径。在zkEVM-ROM程序中，每个EVM opcode 通过一系统zkASM 指令实现。每个指令使用执行路径矩阵的一行，也称为zkEVM的一步。

STARK 递归组件

当Executor 执行完成后，会生成一系列多项式，STARK递归组件将其作为输入，主要包含：

承诺多项式；
常量多项式；
一系列指令的脚本；

STARK递归组件采用FRI (Fast Reed-Solomon Interactive Oracle Proof of Proximity, FRS-IOPP) 生成zk-STARK 证明。

采用递归的原因为：

实际上是生成多个zk-STARK 证明；
将其分成多组 zk-STARK 证明；
对于每个组，合并成一个zk-STARK 证明；
对于所有的组，最终合并成一个zk-STARK 证明。

因此，最终将几百个zk-STARK 证明合并成一个zk-STARK 证明。

CIRCOM 库

CIRCOM 组件将生成的zk-STARK 证明作为输入，生成witness，以R1CS（Rank-1 Constraints System）形式表示约束。

zk-SNARK Prover

zk-SNARK Prover 采用Rapid SNARK方案，根据CIRMCOM生成的约束系统，最终生成zk-SNARK 证明。

zk-STARK 具有较快的证明者速度，不需要可信设置，但是生成的证明比较大；采用zk-SNRK来验证zk-STARK证明，可以大幅减少证明大小，大幅减少gas花费（从 5M 到 350 K），实现简洁性目标。

两种新的语言

Polygon Hermez 创建了两种新的语言： zkASM（Zero-knowledge Assembly）和 PIL (Polynomial Identities Language) 。

zkASM: 主要将主状态机的指令映射到其它状态机，作为固件的解释器，由Executor 执行，生成执行路径；
PIL：将计算转变为多项式约束关系，描述这些多项式的恒等关系，然后用于生成证明。

zkASM

zkASM（zero-knowledge Assembly）以更加抽象的方式，描述处理器的ROM, 告诉Executor 如何解释输入的各种交易，然后由Executor 生成多项式。

基本语法

zkASM 的每个指令顺序执行（除了jump），指令被一行一行地描述。

注释和模块

注释用 ";" 表示, 目前只支持单行注释：

; This a totally useful comment

zkASM 代码划分为多个文件，通过INCLUDE 导入，实现zkASM 的模块化：

; File: main.zkasm

INCLUDE "utils.zkasm"
INCLUDE "constants.zkasm"
; -- code --

寄存器赋值

有多种寄存器赋值方式：

采用 "=>" 将常量赋给1个或多个寄存器：
```
0 => A, B
```
将一个寄存器值赋给其它寄存器：

A => B, C

也可以将函数值存在寄存器中：

f(A,B) => C,D

将全局变量值存入寄存器：
```
%GLOBAL_VAR => A,B
```
将 executor 执行结果存入1个或多个寄存器中，使用 $ 符号。

${ExecutorMethod(params)} => A,B

若一个方法独自执行，主要是用来生成日志信息：

${ExecutorMethod(params)}

除了executor 方法，还可以使用内联函数.

${A >> 2} => B
${A & 0x03} => C

引入操作码

之前每个指令主要和寄存器交互，下面将和ROM的其它部分交互。

使用下面的语法将zkEVM的操作码存入某些寄存器中：

$ => A,B    :OPCODE(param)

其中一个简单的例子是从内存中载入操作码：

$ => A,B    :MLOAD(param)

当寄存器出现在操作码的一边，表示寄存器A 是内存存储操作码的输入。

A   :MSTORE(param)

类似地，可以将自由输入存到寄存器，然后执行一些zkEVM 操作码：

${ExecutorMethod(params)} => A      :OPCODE1
                                    :OPCODE2
                                    :OPCODE3
                                    ...

当 executor 方法和一个寄存器存储结果，可以和 jump 操作码结合，用来处理一些意外的情形，例如gas 不足：

${ExecutorMethod(params)} => A :JMP(param)

有时也会遇到反方向的跳转，用来执行即将发生的操作：

SP - 2  :JMPN(stackUnderflow)

代码注入

内联javascript 指令可以用 $$ 表示：

$${CODE}

断言

下面的断言比较寄存 B 和寄存器A 中的值。

B    :ASSERT

示例

下面将EVM ADD 作为第一个介绍性的示例：

opADD:
    SP - 2          :JMPN(stackUnderflow)
    SP - 1 => SP
    $ => A          :MLOAD(SP--)
    $ => C          :MLOAD(SP)

    ; Add operation with Arith
    A               :MSTORE(arithA)
    C               :MSTORE(arithB)
                    :CALL(addARITH)
    $ => E          :MLOAD(arithRes1)
    E               :MSTORE(SP++)
    1024 - SP       :JMPN(stackOverflow)
    GAS-3 => GAS    :JMPN(outOfGas)
                    :JMP(readCode)

首先检查stack 是否适合 ADD 操作。 ADD 操作码两个元素，它会检查这两个元素确实在stack 上。
```
SP - 2          :JMPN(stackUnderflow)
```

若少于两个元素，则 stackUnderflow 函数执行。

然后分别移动stack 指针，分别将值存入寄存器 A 和 C中：

SP - 1 => SP
$ => A          :MLOAD(SP--)
$ => C          :MLOAD(SP)

分别将寄存器 A 和 C 存入变量 arithA 和 arithB 中，然后调用addARITH , 执行实际的加法运算：

A               :MSTORE(arithA)
C               :MSTORE(arithB)
                :CALL(addARITH)
$ => E          :MLOAD(arithRes1)
E               :MSTORE(SP++)

最后，将加法结果移入寄存器 E 中，将对应的值放到stack指针位置。

执行多个检查，如stack 没有满，gas 未耗尽。

1024 - SP       :JMPN(stackOverflow)
GAS-3 => GAS    :JMPN(outOfGas)
                :JMP(readCode)

最后，还有一个指令用来指示移动下一个指令中。

PIL

PIL (Polynomial Identity Language) 是一种用来定义状态机的域相关的语言。创建PIL 的目的是为开发者提供一种构建状态机的友好框架，将证明机制的复杂性抽象出来。PIL 的一个主要特别是模块化，允许开发者定义参数化的状态机：namespaces。通过构建模块化状态机，更容易测试、审计和形式化验证复杂的状态机。PIL 的关键特点有：

提供 $\mathtt{namespaces}$ ，对状态机必要的部分进行命名；
表示多项式是承诺的，还是不变的；
表达多项式的有关系，可能是恒等，或 $\mathtt{lookup arguments}$ ;
指定多项式的类型，例如 bool 或 u32.

Hello World 示例

对于一个状态机，输入为两个数 $x$ 和 $y$ ，作乘法运算，也称为 Multiplier，通过下面的函数表示：
$f(x, y) = x \cdot y$
下表展示了不同输入的计算路径，有两个自由输入多项式 $\mathtt{ freeIn_1}$ 和 $\mathtt{freeIn_2}$ , 输出多项式为 $\mathtt{out}$ ，为输入多项式的乘积。

由此可以将多项式分为两类：

$\textbf{Free Input Polynomials}$ ：主要用来在计算中引入更多输入, 值不依赖之前的输入；
$\textbf{State Variables}$ : 组成状态机的状态，代表状态机输出的每一步，若是最后一步，则表示整个计算的输出。

Multiplier 状态机的约束条件为：
$out = freeIn_1 \cdot freeIn_2$

PIL 组件

本节深入讲解PIL 的组件。

Namespaces

[图片上传失败...(image-f2d442-1664987363581)]

状态机在PIL以namespaces方式组织，用作一个命名空间，将状态机所有的多项式和恒等关系包含在内，也包含了状态机的组件。命名空间不允许重名。

Polynomials

[图片上传失败...(image-7dbcd2-1664987363581)]

常量多项式，是预处理的多项式，在状态机执行前就已经确定，并且在执行过程中保持不变，例如selectors， latches, sequencers。

承诺多项式只有证明者知道，在执行过程中会改变。承诺多项式分两类：输入多项式和状态变量。

Free Input Polynomials：用来引入状态机的输入数据。

State Variables: 状态变量可以认为是状态机的的状态。

多项式元素类型

[图片上传失败...(image-1963c3-1664987363582)]

可以通过关键字表明多项式类型，例如 bool, u16, field, 以实现元素域的约束条件。

约束是PIL 代码最关键的部分，用来定义多项式之间的关系，实现条件约束。

[图片上传失败...(image-f498eb-1664987363582)]

约束条件一般有以下几种类型：

                      Main Polynomial Constraints

循环结构

状态机需要有循环性质，尤其是从最后一行到第一行的状态转换，在设计状态机约束条件时候需要特别注意。

[图片上传失败...(image-bf1aec-1664987363582)]

                                                                      状态机循环性质

若最后一次状态转换约束未满足，可以通过人工添加值的方式解决。

使如对于如下的状态机和对应的计算路径：

[图片上传失败...(image-b1981f-1664987363582)]

明显，约束条件 $b'=b+a$ 在最后一个转换中不满足： $(a,b)=(1,2)$ 到 $(a,b)=(1,1)$

可以通过添加额外两行方式解决，即：

另外一种办法是引入选择子，即：

[图片上传失败...(image-89eab7-1664987363582)]

第三种办法是利用现有的选择子进行处理。

模块化

虽然一些多项式可以添加到状态机中用以表述更多操作，但这种设计很难测试，审计和验证。

为了避免这些复杂性，PIL 采取分而治之的策略：

不是仅开发一个大的状态机，而是采用由不同状态机组成的架构；
每个状态机证明一项指定的任务，有一系列约束条件；
不同状态机的相关多项式通过lookup tables和 permutation arguments 关联在一起；
保证一致性，就像仅有一个单一的状态机。

PIL 因此非常适合状态机的模块化设计。下图描述了多项式 $[a,b,c]和[d,e,f]$ 之间的连接关系。

                                               跨状态机之间的多项式连接

为了说明这个过程：

首先设计一个状态机，管理2字节元素的算术化操作；
通过lookup argument 连接两个状态机。

算术状态机

算术状态机用来检查一些算术操作，例如加法和乘法，在2字节元素上正确执行，对于多项式 $\mathtt{a,b,c,d,e}$ ，需要满足下面的恒等关系：
$a(x)\cdot b(x)+c(x)=2^{16}\cdot d(x)+e(x)$
需要注意的是：

（a） $a$ 和 $b$ 之间乘法操作，可以通过 $e$ 和 $d$ 描述，它们都是2字节的元素；

（b）约束 $a, b,c,d,e$ 的值都是2字节的值。

                                                                        算术状态机的架构

上图展示了算术状态机的设计架构，下表显示计算的执行路径：

[图片上传失败...(image-5633e4-1664987363582)]

                                                       算术状态机的计算路径

算术状态机工作方式如下： $\mathtt{LATCH}$ 来用标记运算是否准备好。 $\mathtt{SET[A]}, \mathtt{SET[B]}, \mathtt{SET[C]}, \mathtt{SET[E]}$ 和 $\mathtt{LATCH}$ 为常量多项式， $\mathtt{freeIn}$ 为承诺多项式， $a,b,c,d,e$ 为状态变量，

算术状态机多项式的约束为：
$\begin{aligned} &\texttt{freeIn} \subset [0,2^{16} - 1], \\ \texttt{a}' &= \texttt{SET}[A]\cdot(\texttt{freeIn} - \texttt{a}) + \texttt{a}, \\ \texttt{b}' &= \texttt{SET}[B]\cdot(\texttt{freeIn} - \texttt{b}) + \texttt{b}, \\ \texttt{c}' &= \texttt{SET}[C]\cdot(\texttt{freeIn} - \texttt{c}) + \texttt{c}, \\ \texttt{d}' &= \texttt{SET}[D]\cdot(\texttt{freeIn} - \texttt{d}) + \texttt{d}, \\ \texttt{e}' &= \texttt{SET}[E]\cdot(\texttt{freeIn} - \texttt{e}) + \texttt{e}, \\ 0 &= [ \texttt{a} \cdot \texttt{b} + \texttt{c} - (2^{16} \cdot \texttt{d} + \texttt{e}) ] \cdot \texttt{LATCH}. \end{aligned}$
在PIL 代码中可以如下描述：

[图片上传失败...(image-681699-1664987363582)]

主状态机

主状态机主要负责主要的一些任务，但会指定使用算术状态机当需要的时候。

                                                             主状态机架构

PIL 的第一任务是引入大量的多项式，如下所示：
[图片上传失败...(image-3ce6aa-1664987363582)]

现在可以添加主状态机变量 $a,b,c,d,e$ 的大量约束，下图展示了所需要的行为：

在PIL中，表示如下：

[图片上传失败...(image-22f9e6-1664987363582)]

最后，主状态机和算术状态机之间的约束关系可以用下面的约束表示：

[图片上传失败...(image-f16ff3-1664987363582)]

这种连接关系可以下面的表描述，即：

[图片上传失败...(image-def9bc-1664987363582)]

一方面， $\mathtt{arith}$ 选择子用来标记主状态机中的在算术状态机中的lookup，另一方面， $\mathtt{LATCH}$ 也是一个选择子，哪些行需要添加到lookup证明，即最后需要证明：
$\begin{array}{c} \texttt{Main.arith} \cdot [\texttt{Main.a} , \texttt{Main.b} , \texttt{Main.c} , \texttt{Main.d}, \texttt{Main.e}] \\ \subset \\ \texttt{Arith.LATCH} \cdot [\texttt{Arith.a}, \texttt{Arith.b}, \texttt{Arith.c}, \texttt{Arith.d}, \texttt{Arith.e}]. \end{array}$

高级特性

公开输入

公开输入是多项式的值，在状态机执行前已知。在下面的示例中， $\mathtt{publicInput}$ 被设为多项式 $a$ 的第一个值，分号 ":" 用来向编译器注明：

[图片上传失败...(image-906e91-1664987363582)]

这里使用Lagrage 多项式 $L_1$ 用来创建一个约束条件：
$L_1 \cdot (\texttt{a} - :\texttt{publicInput}) = 0.$
Permutation check

下面的例子中， $\mathtt{is}$ 关键字用来表示 $[\mathtt{sm1.a}, \mathtt{sm1.b},\mathtt{sm1.c}]$ 和 $\mathtt{sm2.a}, \mathtt{sm2.b}, \mathtt{sm2.c}$ 是置换关系，

[图片上传失败...(image-c62cd3-1664987363582)]

这个约束可以用连接不同的状态机，约束不同状态机的多项式是相同的。

两个特殊的功能

$\mathtt{in}$ 和 $\mathtt{is}$ 主要用于以下设计：
$\begin{array}{ccc} (3,2) & \text{in} & (1,2,3,4)\\ (1,5,5,5,8,1,1,2) & \text{in} & (1,2,4,5,8)\\ (3,2,3,1) & \text{is} & (1,2,3,3)\\ (5,5,6,9,0) & \text{is} & (6,5,9,0,5). \end{array}$
Connect关键字