零知识证明的先进形式化验证：如何验证一条ZK指令

来源：CertiK中文社区

为了深入理解形式化验证技术是如何应用于zkVM（零知识虚拟机）之上的，本文将聚焦于单条指令的验证。关于ZKP（零知识证明）先进形式化验证的总体情况，请查阅我们同期发布的“零知识证明区块链的先进形式化验证”文章。

什么是ZK指令的验证？

zkVM（零知识虚拟机）能够创建简短的证明对象，以作为证据来证明特定程序可以在某些输入上运行、并成功终止。在Web3.0领域，zkVM的应用使得吞吐量变高，这是因为L1节点只需要验证智能合约从输入态到输出态转变过程的简短证明，而实际的合约代码执行则可以在链下完成。

zkVM证明器首先会运行程序以生成每一步的执行记录，然后将执行记录的数据转换为一组数字表格（该过程被称为“算术化”）。这些数之间必须满足一组约束（即电路），其中包括了具体表单元格之间的联系方程、固定的常数、表间的数据库查找约束，以及每对相邻表行间所需要满足的多项式方程（亦即“门”）。链上验证可以由此确认的确存在某张能满足所有约束的表，同时又保证不会看到表中的具体数字。

每条VM指令的执行都面临很多这样的约束，这里我们将VM指令的这组约束简称为它的“ZK指令”。下面是用Rust语言编写的一个zkWasm内存加载指令约束的示例。

ZK指令的形式化验证是通过对这些代码进行形式化推理来完成的，我们首先将其翻译成形式化语言。

即便只有单个约束包含错误，攻击者都因此而有可能提交恶意的ZK证明。恶意证明所对应的数据表格并不对应智能合约的合法运行。与以太坊等非ZK链不同，后者有许多节点运行不同的EVM（以太坊虚拟机）实现，从而不太可能在同时同地出现相同的错误，一个zkVM链则只有单一的VM实现。单就这个角度而言，ZK链比传统的Web3.0系统更为脆弱。

更糟糕的是，和非ZK链不一样，由于zkVM交易的计算细节并没有被提交并存储在链上，在攻击发生后，不仅是要发现攻击的具体细节非常困难，甚至要识别攻击本身也会变得极具挑战性。

zkVM系统需要极为严格的检视，不幸的是，zkVM电路的正确性很难保证。

ZK指令的验证为何很难？

VM（虚拟机）是Web3.0系统架构中最为复杂的部分之一。智能合约的强大功能是支撑Web3.0能力的核心，其力量源自于底层的VM，它们既灵活又复杂：为了完成通用计算和存储任务，这些VM必须能够支持众多的指令和状态。比如，EVM的geth实现需要超过7500行Go语言代码。类似的，约束这些指令执行的ZK电路也同样庞大而复杂。像在zkWasm项目中，ZK电路的实现需要超过6000行Rust代码。

zkWasm 电路架构

与专为特定应用（如私人支付）设计的ZK系统中使用的专用ZK电路相比，zkVM电路的规模要大得多：其约束规则的数量可能比前者多出一到两个数量级，而其算术化表格则可能包括数百列、含有数以百万计的数字单元格。

ZK指令的验证意味着什么？

我们在这里想要去验证zkWasm中的XOR指令的正确性。从技术上讲，zkWasm的执行表对应一个合法的Wasm VM执行序列。所以宏观来看，我们想要验证的是：每次执行这条指令总是会产生一个新的合法的zkVM状态：表中的每一行都对应VM的一个合法状态，而紧接着的一行则总是要通过执行相应的VM指令来生成。下图为XOR指令正确性的形式化定理。

这里“state_rel i st”表明状态“st”是步骤“i”中智能合约的合法zkVM状态。 正如你可能猜测的那样，要证明“state_rel (i+1) …”不是轻而易举的。

如何验证ZK指令？

尽管XOR指令的计算语义很简单，就是计算两个整数的按位异或（bitwise xor）并返回整数结果，但它所涉及的方面却比较多：首先，它需要从栈内存中取出两个整数，进行异或计算，然后将这个计算得出的新整数存回同一个栈。此外，该指令的执行步骤应融入于整个智能合约的执行流程中，并且其执行顺序及时机必须正确。

因此，XOR指令的执行效果应该是从数据堆栈中弹出两个数，压入它们的XOR结果，同时增加程序计数器，以指向智能合约的下一条指令。