Polygon MidenVM中的recursive STARK verification优化

news2025/4/19 16:13:40

1. 引言

本文主要参考Bobbin Threadbare 2023年9月在ZK Summit 10上的分享 ZK10: Optimizing recursive STARK verification in Polygon Miden VM - Bobbin Threadbare。

本文基本内容框架为：

STARK递归方法
Miden需求及目标
递归verifier开销
Miden VM优化措施
结果及结论

2. STARK递归方法

STARK递归方法：

1）专用电路：以 $N$ 个programs为例，其可以是同一big program切分chunks而来，也可以是完全独立的program。基于STARK的zkVM，会为这 $N$ 个program中的每个都生成proof，然后将各个proofs汇总为单个proof。由于本方案中采用的是专用电路，因此递归证明聚合也是由专用电路实现的。
2）单一相同电路：以 $N$ 个programs为例，与上面的专用电路不同之处在于，采用相同的VM电路来聚合proofs。即执行相同的VM，具有相同的VM逻辑。原因在于VM自身很强大，可执行程序，并生成相应程序执行的proof并验证该proof。因此可使用相同的逻辑，而不需要专用电路。

以上2种STARK递归方法各有优劣：

	专用电路	单一相同电路
灵活性	有限	高
设计复杂度	中等	高
审计	多个电路	单个电路
性能	高	取决于所使用的指令集

在这里插入图片描述

3. Miden需求及目标

Miden rollup的需求为：

Single VM approach：因为聚合证明包含non-trivial additional logic。即，采用相同的VM来执行程序、聚合证明。
proof安全级别为100位：当前的参数为：
- 8倍blowup factor
- 27个queries
- 16 bits of grinding
相对小的计算：大多数“leaf” programs期望的cycle数为 $2^{12}$ 到 $2^{22}$ 。

Miden rollup希望达成的目标为：

在消费级硬件上：生成2-to-1 recursive proof，用时在1到2秒。这里的消费级硬件，是指笔记本，而不是手机。
在定制化硬件上：生成16-to-1 recursive proof，用时在1到2秒。这里的定制化硬件，不是ASIC或FPGA，而是指具有一两个GPU的强处理器。

以 $2^{17}$ 个cycles计算为例，当前Miden VM性能为：
在这里插入图片描述
Miden rollup期望实现的recursive threshold为：

以 $2^{16}$ 个cycles，来验证a Miden VM execution proof。

4. 递归verifier开销

Miden VM架构为：
在这里插入图片描述
上图看起来像Miden VM的trace layout，为基于STARK的系统。
其中最主要的2个元素为：

1）Main processor（Operand stack 19 columns）：相当于会为每条指令添加一行到trace中。
2）Chiplets：
- 处理专用计算
- 每条指令有多行
- 可供main processor并行运行
- Hash chiplet：每个RPO permutation有8行

Miden VM的cost模型为：可将Recursive verifier costs分为2大部分：

1）哈希开销：如Merkle path verification，以及PRF。
2）其它开销：如constraint evaluation、DEEP composition等等。

5. Miden VM优化措施

STARK verifier组件有：

1）Verifying trace and constraint commitments。
2）Loading OOD frame and evaluations。
3）Evaluating AIR constraints at OOD point。
4）Generating random composition coefficients。
5）Computing DEEP composition polynomial。
6）FRI verification。

其中3）5）6）为STARK verifier的主要瓶颈。

5.1 FRI verification优化

在这里插入图片描述
在FRI verification过程中：

1）需验证每层都fold正确：即需确定最优的folding factor是多少？
- 1.1）验证每层folding正确的挑战在于：
  - 大量算术运算是在扩域的。
  - folding factor越高，这种算术运算越复杂，但fold的层数越少。
    【每层folding对应约1万个cycles。】
- 1.2）验证每层folding正确的优化措施有：
  - 为扩域乘法引入新的指令：EXT2MUL
  - 为folding a single point with folding factor $4$ 引入新的指令：FRIE2F4。如原来需要100个cycle，现在只需要一个cycle。
    【优化后，每层folding对应约300个cycles。】
2）需验证remainder为某bounded-degree多项式：即需确定最优的remainder多项式degree是多少？
- 2.1）验证remainder的常规方式为：
  - 采用NTT将remainder插值为某多项式。
  - 检查该多项式的degree。
  在Miden VM中，做以上验证remainder的常规方式是非常昂贵的。
- 2.2）验证remainder的优化方式为：
  - 在Miden VM之外运行NTT。
  - 以non-deterministically方式，将所插值多项式提供给Miden VM。
  - 使用barycentric evaluation，在Miden VM内验证外部所做NTT的正确性。
    【优化后，对于degree $< 8$ 的remainder，可以小于3000个cycles进行验证。】

5.2 DEEP composition优化

计算DEEP composition多项式对应如下公式：
$Y(x)=\sum_{i=0}^{k}(\alpha_i\cdot \frac{T_i(x)-T_i(z)}{x-z}+\beta_i\cdot \frac{T_i(x)-T_i(z\cdot g)}{x-z\cdot g}+\gamma_i\cdot \frac{T_i(x)-T_i(\bar{z})}{x-\bar{z}})+\sum_{j=0}^{m}\delta\cdot \frac{H_j(x)-H_j(z^m)}{x-z^m}$

该计算存在如下调整：

在基域和扩域有大量算术计算。
需跟踪大量遍历
需要大量随机值

DEEP composition多项式计算在Miden VM中非常昂贵。相应的优化策略为：

1）移除对trace polynomials的conjugate（共轭） check。
2）移除对constraint polynomials的degree adjustment factors。
3）减少了所需的随机值数量。
4）为增加linear combination术语，引入2个新指令：RCOMB1和RCOMB2。如原来需20-40 cycle，现在仅需1个cycle。

5.3 AIR constraint evaluation at OOD point优化

当前Miden VM正在对AIR constraint evaluation at OOD point进行优化。

Evaluating AIR constraints at OOD point的挑战在于：

1）constraint evaluation logic需写在Miden assembly中：这不仅充满挑战，且难于维护。
2）constraints仍在进化中。如降低trace columns数量，在Miden assembly中修改约束很难，而跟踪这些修改更难。

相应的解决方案为：【方案正在处理中，未完成】

1）在AirScript中写Miden约束。
2）使用AirScript Miden Assembly backend来输出优化后的constraint evaluation code。

AirScript架构为：
在这里插入图片描述

6. 结果及结论

经以上优化后的结果为：
在这里插入图片描述
即，若想以 $2^{16}$ 个cycles完成proof验证，则当且仅当，constraint valuation $< 30 K$ 个cycles。当前优化后所需的约束cycles数为36.7K，进一步优化是有可能满足要求的。

参考资料

[1] Bobbin Threadbare 2023年9月在ZK Summit 10上的分享 ZK10: Optimizing recursive STARK verification in Polygon Miden VM - Bobbin Threadbare
[2] 2022年8月ethresearch讨论 Miden VM v0.2: new VM architecture for a zk-rollup