形式化验证 powdr 的自动预编译

liumuhui 4小时前阅读数 1 #区块链

零知识虚拟机（zkVM）让开发者能够证明任意程序正确运行，而证明编写者无需接触证明电路。这种便利是有代价的：客户程序执行的每一条 RISC-V 指令都会增加证明者必须做的工作。通用 zkVM 解释器会为每一条指令重新推导相同的解码和分发簿记工作，即使一整段指令序列只是在做一件概念上简单的事情，比如哈希函数的内层循环。

powdr 是一个构建在 zkVM 之上的开源编译器工具包，主要支持 OpenVM，同时也实验性地支持 SP1，它自动地解决这个问题。Certora 一直在与 powdr 团队合作开发 autoprecompiles：powdr 为热代码自动生成定制电路的机制。更具体地说，我们一直在形式化验证这种优化永远不会改变程序的计算结果。

这篇文章解释了什么是 autoprecompiles，我们如何定义和检查它们的正确性，以及我们的验证器在两个真实工作负载上发现了什么：一个 Keccak 预编译和一个来自 Reth 的执行轨迹。

powdr 做什么

如果 autoprecompiles 的想法听起来很熟悉，那很正常：powdr 运行的是一个相当传统的编译器优化，类似于跨热循环体的指令融合或内联。不同之处在于："指令"是电路约束，它产生的产物是证明电路而不是机器码。

给定一个客户程序，powdr 对其执行进行性能分析，以找到热 基本块：没有分支的直线指令序列。对于每个块，它通过内联块中每条指令的现有电路来构建一个单一的约束系统。powdr 的电路在一个中等大小的有限域上工作，主要是 OpenVM 使用的 BabyBear 域。它们由算术等式以及 总线交互 组成。OpenVM 的电路使用总线来相互通信，用于内存、执行顺序、范围检查、位查找等。这种机制直接来自底层的 zkVM，powdr 只是模仿底层语义以实现忠实的优化。

整个块的组合系统很大且充满冗余：在编译时已经已知的操作码选择器逻辑、仅用于将值从一条指令传递给下一条指令的中间寄存器、立即被覆盖的内存写入。powdr 的优化器流水线反复简化合并后的系统。一旦值已知就进行替换，抵消立即被覆盖的内存写入，删除电路中其他部分不再依赖的变量，等等。它一直持续到系统稳定为止。结果，autoprecompile（APC），被生成为一个单一的固定电路，OpenVM 用它来代替整个原始指令序列运行。

这是通往大多数 zkVM 今天通过手写预编译所达到的相同目标的一条不同路线：针对特定操作（如 Keccak 或配对检查）的定制电路。手写预编译是有效的，但也是有代价的。每一个都必须由电路工程师设计、实现和审计，为每个证明后端重做，并且它大约使团队需要维护的代码翻倍：电路逻辑，以及必须与之完全一致的见证生成逻辑。powdr 的 autoprecompiles 旨在无需那种手动的、每个后端的工作就能达到类似的性能。

回报是证明者只需为一个小型专用电路支付一次，而不是逐条指令地为通用解释器循环支付。powdr 自己的基准测试报告称，在单个工作负载上约束数量减少了 2.5–6 倍，这被认为是预期证明时间的一个不错的代理指标。自动生成的电路已经接近手写预编译所达到的水平。

为什么这需要形式化验证

所有这些简化都是自动发生的，逐块进行，由一个通用重写引擎驱动。这使得它更接近编译器的优化器，而不是一个手工检查的电路。这正是那种容易引入正确性错误且容易遗漏的代码：一个对测试套件恰好覆盖的情况是健全的重写规则，对某些其他指令组合可能仍然是错误的。

要理解为什么这很重要，有必要记住 zkVM 证明是为了什么。像 Reth 的执行逻辑或 Keccak 哈希这样的东西在 zkVM 中运行只有一个原因：让验证者能够接受一个简短的证明，而不是重新执行计算本身。该验证者通常是区块链上的智能合约，例如在 ZK Rollup 的上下文中。它完全信任电路：如果电路愿意接受一个见证，验证者就接受该证明。因此，autoprecompile 电路中的错误不是崩溃，也不是屏幕上的错误输出。它是整个密码学论证本应保证的东西上的一个漏洞，而且这个漏洞可能朝两个方向发展：

电路接受过多（健全性错误）。 如果优化后的电路接受了一个不对应于原始指令任何真实执行的见证，有人可以故意构造该见证。Rollup 将接受不正确的状态转换，这是"凭空铸造代币"类别的错误：证明者说服链上验证者一个无效的交易或区块被正确执行了，因为它某个预编译的加速电路稍微过于宽松。

如果电路用于 ZK，比如在 zkRollup 中，这就更加危险，因为见证是完全隐藏的，所以无效转换在可证明的意义上是无法检测的，即使你对发生了什么无效转换有假设。

电路接受过少（完备性错误）。 如果优化后的电路无法再为原始指令合法允许的某些执行找到满足的见证，那不是安全漏洞，而是活性问题：一个本应可证明的诚实交易突然变得不可证明，链或 Rollup 就会卡在上面。

这两种失败模式都不是你想在预编译发布之后才发现的。因此，我们没有信任优化器，而是构建了一个验证器。它独立地检查每一个优化步骤，验证前后的电路是等价的。

我们的方法

为了验证 autoprecompile，我们单独考虑每个优化步骤，并为每个步骤取两个约束系统：pass 运行之前的一个和刚刚之后的一个。两者都是上述描述的同类对象：代数约束加上总线交互。我们询问两者是否等价。

powdr 的优化器以大约十几个 pass 的流水线运行，执行到不动点，单独应用于每个基本块。例如，一个 pass 合并两个刚刚被融合在一起的指令之间的"下一条指令是什么"的簿记；另一个使用 powdr 自己的内部求解器将某些变量固定为常量并进行替换；第三个抵消在任何人读取之前就被覆盖的内存写入；第四个剪除电路中其他部分不再依赖的变量。这些 pass 反复运行，直到系统停止缩小。我们不是试图一次性验证整个优化器，而是独立地检查每一对连续的中间电路：pass $n$ 的输出电路必须等价于 pass $n+1$ 的输出电路。如果该链中的每个环节都成立，那么根据传递性，最终的 autoprecompile 等价于未优化的块。

"等价"意味着什么。 我们将等价性分为两个方向性的义务，镜像了用于验证编译器和 ZKP 正确性论证的标准健全性/完备性划分：

健全性：优化后电路接受的每一个行为都对应于原始电路的真实行为。
完备性：原始电路接受的每一个行为仍然被优化后电路接受。

两者都是在电路的外部接口上陈述的：在有状态总线（如内存和执行顺序）上发送和接收的值。两者都不看内部信号。两个电路可以使用完全不同的内部变量，只要它们在这些总线上交换相同的值，就仍然是等价的。使用不同的无状态查找表（位运算、范围检查）的两个电路也被视为等价，因为"表接收器"电路可以吸收与这些总线的任何合法交互。这让验证器能够确认优化 pass 的意图（"内存流量不变"），而不会被内部的表面重构分散注意力。

具体来说，健全性是这样一个陈述：对于优化后电路变量的每一个满足赋值，都存在一个原始电路变量的可高效计算的满足赋值，它在有状态总线上产生相同的效果。作为公式：$\forall (\text{optimized-circuit variables}), \text{optimized-constraints} \implies \exists (\text{original-circuit variables}), \text{original-constraints} \land \text{same bus effect}$。完备性是同样的陈述，只是两个电路互换：$\forall (\text{original-circuit variables}), \text{original-constraints} \implies \exists (\text{optimized-circuit variables}), \text{optimized-constraints} \land \text{same bus effect}$。

我们不要求求解器直接证明任何一个蕴含；我们将其否定并检查结果的不可满足性，即通常的"假设 $\land \neg \text{goal}$"形式。对于健全性，我们断言优化后电路的约束为普通（存在性）变量，同时加上一个全称量化的断言，即原始电路变量的任何赋值都不能重现相同的效果：

$$ \text{optimized-constraints} \land \forall (\text{original-circuit variables}) (\neg \text{original-constraints} \lor \neg \text{same bus effect}) $$

如果这个组合公式不可满足，则不存在反例，健全性成立。如果它是可满足的，则满足赋值就是一个具体的反例：一个原始电路无法匹配的优化后电路赋值，这对于调试优化器回归非常宝贵。完备性以同样的方式工作，只是两个电路的角色互换。

因此，我们要检查的公式是全称量化的：在检查健全性时对原始电路的变量进行量化，在检查完备性时对优化后电路的变量进行量化。Z3 是来自微软研究院的成熟开源 SMT 求解器，可以直接求解量化公式，但在实践中，它在这方面的速度远不如求解无量词公式，而无量词公式才是它最初构建的目的。因此，在将任何内容交给求解器之前，我们使用领域特定知识自行消除量词。

这样做的主要工具是 Skolem 化：我们尝试为每个全称量化的变量构建一个显式赋值，一个用其他已经自由的（"ground"）变量表示的具体表达式，该量化变量在给定周围约束的情况下必须等于这个表达式。这个表达式被称为 skolem，一旦我们用这个 skolem 替换目标量化变量，它就被消除了：一个量化变量被移除，取而代之的是一个无量词表达式。幸运的是，对于实践中出现的所有量化变量，这几乎总是可以通过相当简单的技术实现，因此我们最终得到一个完全无量词（QF）的公式。

没有什么能保证我们为量化变量替换的 skolem 是正确的，这一点值得说清楚。如果我们推导出一个错误的 skolem，公式可能会虚假地变得可满足：Z3 返回一个"反例"，但它不是真正的反例，只是一个错误 skolem 的产物。那是误报，不是 powdr 中的健全性错误。幸运的是，我们能够完全避免错误的 skolem，因为我们的 skolem 构建基于 powdr 优化器内部所做的事情，而不是盲目猜测。即使我们犯了错误，错误的 skolem 也永远不会导致一个坏的电路对被验证通过，而只会声称一个好的电路对不等价；人工检查这种情况就会发现 skolem 是不正确的。

Skolem 化加上一些其他标准简化（将模算术表达式重写为规范形式，传播已知的边界和位掩码，以及一些类似的）是我们在任何内容到达求解器之抢跑的流水线。剩下的交给 Z3。我们没有编写自己的求解器；我们应用相当标准的简化，然后驱动一个现成的求解器。我们还偶尔利用析取将大公式拆分成更小的、可独立求解的块。

这大约是八个月的努力，与 powdr 团队联合进行，因为他们的优化器本身在我们脚下不断演进。我们认为验证器是一个研究原型，而不是一个完成、加固的工具。它能够可靠地处理完整的生产规模工作负载（见下文），但尚未打包供外部使用。我们也在继续寻找增加对该方法本身信心的方式：例如，我们已经开始在 Lean 中形式化底层量词消除论证（Skolem 化步骤）的部分内容，作为对我们自身推理的独立、机器检查的交叉验证。

替代编码，以及一些重要的技巧

下面结果背后的大部分实际性能工作并不是发生在电路级等价性定义的层面。它发生在我们首先如何将电路翻译成公式的过程中。其中很大一部分归结为一个反复出现的想法：在任何可能的地方，我们给 Z3 一个它可以通过等式推理（即注意到两个东西相等）来闭合的公式，而不是一个它必须通过真正的、通常是模的或非线性的算术推理来艰难处理的公式。等式推理对 SMT 求解器来说几乎是免费的。在 31 位素域上的算术推理才是它可能卡住的地方。在追求这一目标时，有两件事比其他事情重要得多：我们如何编码内存总线，以及一些将昂贵的算术查询转化为廉价的等式查询的特定重写规则。

编码内存总线。 最重要的一个编码选择是如何表示内存总线。我们经历了三种不同的设计。第一种将内存字面地建模为 SMT 数组：每个数据变量一个数组，按地址空间和指针索引，在每次内存总线交互时通过显式的读/写来更新。这是教科书式的编码，也是最容易陈述的，但它很脆弱，扩展性不好。Z3 的内部数组求解器天真地必须将每个存储与每个可能与其别名的读取关联起来。在我们的电路上，这爆炸到每次查询 70,000–160,000 个可能的关系，求解时间与该数量线性增长。我们最终完全放弃了这个编码。

它的替代品是我们今天的默认方案。它在不使用任何数组理论的情况下编码底层的置换检查：对于每一对可能合理地别名的访问（在我们的定制别名分析剪除明显不可能的配对之后），使用一个布尔"此访问匹配彼访问"变量，每个访问一个"恰好一个匹配"约束，以及每个匹配对上的直接等式。不过，这种两两匹配搜索仍然是实际的工作，至少在我们不能静态地固定所有匹配时是这样。

我们还添加了第三个更便宜的选项，它看起来非常专门化，但实际上适用于 powdr 流水线的大部分。考虑两个电路具有相同数量的内存操作，并且我们的静态预分析可以证明两个电路具有相同指针的情况。在这种情况下，我们完全跳过理解电路内部别名的尝试。相反，我们简单地验证电路中的每个写对具有相等的写入，假设所有先前的读取都是相等的。这是 SMT 擅长的等式推理的一个很好的例子，它完全消除了推理别名的任何需要。而且，它实际上适用于 powdr 中的大多数优化步骤，因为大多数步骤不影响内存访问。

最重要的重写。 在编码层之下，大部分收益来自于在公式到达 Z3 之前应用的一小部分重写规则。有几个不仅仅是簿记工作：

因式分解模多项式。 电路中充满了像 $\mathit{bit} \cdot (\mathit{bit} - 1) = 0$ 这样的表达式，这是将域元素约束为恰好 $0$ 或 $1$ 的标准工具。保持原样的话，这是一个模 31 位素数的非线性方程，它迫使 Z3 进入真正困难的非线性推理。我们转而使用 FLINT（一个现成的数论库）对多项式进行因式分解。我们将其重写为对其根的显式析取以及范围约束，在这个例子中即 $(\mathit{bit} = 0 \lor \mathit{bit} = 1) \land \mathit{bit} < 2$。这个重写将一个困难的算术约束换成了几个简单的等式，Z3 对这些等式进行分支处理，然后用于常量传播，以及一个 Z3 可以用于区间推理的范围约束。对实际 Z3 调用的影响是巨大的。一个曾经超过 70 秒超时的调用，在这个重写和一个附近的配套修复落地后，在 0.06 秒内解决了。另一个从 45–61 秒下降到 1.3–1.5 秒，大约 35 倍的改进。
不进行位展开的位运算。 并非每个技巧都符合等式主题。这个技巧是关于避免另一种类型的爆炸。AND/OR/XOR 在电路中以对字节大小值的不透明操作出现。在 SMT 求解器中推理它们的教科书式方法是逐位展开每个操作数。这在电路规模上是一场组合灾难。我们转而附加一组小的线性算术恒等式，在不展开到位的情况下确定相同的值：例如 $x + y = \operatorname{xor}(x,y) + 2 \cdot \operatorname{and}(x,y)$，以及像 $0 \le \operatorname{and}(x,y) \le \min(x,y)$ 这样的简单边界。这让 Z3 将位运算值当作普通的有限整数来推理。
关闭 Z3 自己的一个默认行为。 Z3 内置的 solve-eqs 策略默认会通过为商引入一个新的见证变量来消除模算术项，从而"帮忙"。在我们的公式上，这适得其反。这些见证变量本身是非线性的，并且它们会在目标的其余部分中倍增。在一个案例中，这把一个 1.5 秒的检查变成了 60 秒的超时。我们禁用了这个特定行为。相反，我们自己做更有针对性的模算术重写：前面提到的同一系列重写，将 $a \cdot x + b \equiv 0 \pmod{p}$ 直接转化为等式 $x = -b/a \pmod{p}$。这样 Z3 就不必通过它自己选择的非线性算术来搜索它。

这些技巧单独来看都不复杂。它们中的大多数归结为同一个动作：将 Z3 必须通过算术推理艰难处理的证明义务，替换为它可以通过等式推理来闭合的证明义务。但是，一个仍然包含几个未简化的较困难情况的公式，可能是几秒和超时之间的区别。

结果：Keccak 和 Reth

我们在两个真实工作负载上运行了验证器：

Keccak 预编译：powdr 的 autoprecompile 选择识别出的 61 个热基本块，每个都经过大约 40 个 pass 到 pass 的步骤优化，总共 2,451 次等价性检查。
Reth 区块执行：取自 Reth 以太坊执行客户端的轨迹，包含 100 个热基本块，总共 4,176 次等价性检查。

在这两种情况下，每个热块中每个优化步骤的绝大多数都被自动证明是等价的。在这两个工作负载的当前状态下，我们没有发现任何反例：每个非超时结果都是等价性的证明，而不是反驳。

剩余的部分是求解器超时：不确定，而不是反驳。它们也没有均匀地分布在各个 pass 中。对于 Keccak，其中 80%（25 个中的 20 个）来自一个单一的基本块，按电路规模计算，它比我们优化的任何其他块都大一个数量级。这是一个超大的离群值，而不是某个特定 pass 系统性困难的证据。Reth 没有这样的单一离群值。它的 53 个超时分布在 100 个块中的 27 个中，也没有任何一个 pass 占主导地位（最差的一个内部求解器步骤也只占 11 个）。但这是同样的底层故事，只是表现为更长的尾部而不是一个尖峰。至少有一个超时的块，平均而言（按电路规模）比没有超时的块大约 9 倍。Reth 的 30 个最大块中有 18 个在其 pass 链的某处有超时。

求解时间在两个工作负载中都与电路规模紧密相关（注意对数/对数刻度）。Keccak 的超时（橙色）由一个超大块主导；Reth 的超时则分布在中等至大型块的更长尾部。

值得把这些数字放在背景中来看。它们是大约六周调整 powdr 优化器和我们自己的编码的产物，而不是一次性的结果。针对同样的 2,451 和 4,176 次检查的第一次端到端运行是在 6 月底。它们只自动完成了 76.5% 的 Keccak 检查和 81.9% 的 Reth 检查，平均每次检查分别耗时 34 秒和 65 秒。

在连续的迭代中，我们做了三种改变。我们让公式更容易通过廉价的等式推理而不是昂贵的算术证明来闭合。我们添加了针对内存总线的专用推理。我们用 Rust 对我们公式重写层进行了彻底的重新实现。（核心编码和预分析仍然在 Python 中，但重写步骤——它承担了大部分简化工作——从重写中获得了很大的加速。）这攀升到了今天的 99.0% / 98.7%。现在平均每次检查分别只需不到 7 秒和 8 秒，每次检查的求解时间大约下降了 5–8.5 倍。完全证明的比例跃升了 17 到 22 个百分点。

在这个过程中，验证器还发现了 powdr 优化器中的一些次要问题。大多数是中间结果表示方式上的表面不一致。一个是关于时间戳溢出处理方式的真实正确性边界情况，是在一个小测试程序的早期发现的。它不可利用，powdr 团队也已经承认并接受了它。这正是独立的等价性检查应该捕获的那种东西。

使用 28 个并行工作进程对工作负载运行完整检查，Keccak 大约需要 12 分钟，Reth 需要 23 分钟。按顺序累加，底层的求解器工作大约为 Keccak 5.4 CPU 小时，Reth 10.5 CPU 小时。这让我们感受到流水线买回了多少自动的、逐 pass 的验证，而每个工作负载的成本是以分钟而不是天来衡量的。

结论

我们着手回答一个相当狭窄的问题：powdr 的 autoprecompile 优化能否在真实生产规模下被独立、自动地检查正确性？答案是是的。

在两个真实工作负载和总共 6,627 次 pass 到 pass 的等价性检查中，这种方法经受住了考验。我们构建了精确的健全性/完备性等价性定义，基于现成求解器的 SMT 编码，以及一个自动证明绝大多数检查的验证器。剩余的一小部分是未确定的超时，而不是关于正确性的悬而未决的问题。六周的调整将最初的端到端运行从 77–82% 的自动化率提升到超过 98%。在这个过程中，验证器做了独立检查该做的事情：它捕获了优化器本身的一些真实的、尽管是次要的问题。