来源：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结果，同时增加程序计数器，以指向智能合约的下一条指令。
不难看出，这里的正确性属性定义总体上与我们在验证传统字节码VM（比如以太坊L1节点中的EVM解释器）的时候所面对的情况非常相似。它依赖于机器状态（这里指栈内存和执行流）的高级抽象定义，以及关于每条指令预期行为的定义（这里指算术逻辑）。
然而，如我们下面所将要看到的，由于ZKP和zkVM的特殊性，其正确性的验证过程经常与常规VM的验证很不一样。光是验证我们这里的单条指令，就要依赖于zkWASM中很多表的正确性：其中有一张用于限制数值大小的范围表，一张用于二进制位计算中间结果的位表（bit table），一张每行都存储恒定大小的VM状态的执行表（类似物理CPU中的寄存器和锁存器中的数据），以及代表动态可变大小的VM状态（内存、数据栈和调用栈）的内存表和跳转表。
第一步：栈内存
与传统VM类似，我们需要确保指令的两个整数参数可以从堆栈中读取，并且其异或结果值被正确地写回堆栈。堆栈的形式化表述看起来也相当熟悉（还有全局内存和堆内存，但XOR指令不使用它们）。
zkVM使用一种复杂的方案来表示动态数据，这是因为ZK证明器并不能原生支持像堆栈或数组这样的数据结构。相反的，对于压入堆栈的每个数值，内存表用单独的一行来记录，其中的某些列则用于指示该表项的生效时间。当然，这些表的数据可以被攻击者所控制，因此还必须加以一些约束，以确保表项真实对应于合约执行中的实际压栈指令。这是通过精心计算程序执行过程中的压栈次数来实现的。验证每一条指令时，我们需要确保这个计数始终正确。此外，我们还有一系列引理，将单条指令生成的约束与实现堆栈操作的表查找和时间范围检查相关联。从最顶层看，内存操作的计数约束定义如下。
第二步：算术运算
与传统VM类似，我们希望确保位异或的运算正确无误。这看起来很容易，毕竟我们的物理计算机CPU都能够一次性完成这个操作。
但对于zkVM来说，这实际上并不简单。ZK证明器原生支持的唯二算术指令是加法和乘法。为了进行二进制位运算，VM使用了一个相当复杂的方案，其中一张表存放固定的字节级运算结果，另一张表则充当“草稿本”，用以在多个表行上展示如何将64位数字分解为8个字节，然后再重新组合出结果。
zkWasm位表规范的片段
在传统的编程语言中非常简单的异或运算，在这里则需要很多引理来验证这些辅助表的正确性。对于我们的指令，我们有：
第三步：执行流
与传统VM类似，我们需要确保程序计数器的数值正确更新。对于像XOR这样的顺序指令，每次执行步骤后，程序计数器需要加一。
由于zkWasm被设计用来运行Wasm代码，因此也要确保在整个执行过程中，Wasm内存的不变性质始终得到保持。
传统的编程语言对布尔值、8位整数、64位整数等数据类型有原生支持，但在ZK电路中，变量始终是在大素数（≈ 2254）模下的整数范围内变化。由于VM通常以64位数运行，电路开发者需要使用一套约束系统来确保它们具有正确的数值范围，而形式化验证工程师则需要在整个验证过程中追踪关于这些范围的不变性质。对执行流和执行表的推理会涉及到所有的其他辅助表，因此我们需要检查所有表数据的范围是否正确。
类似于内存操作数量管理的情形，zkVM需要一组类似的引理来验证控制流。具体而言，每个调用和返回指令都需要使用调用栈。调用栈使用与数据栈类似的表方案来实现。对于XOR指令，我们并不需要修改调用栈；但验证整条指令时，仍然需要追踪并验证控制流操作计数是否正确。
验证这条指令
让我们将所有步骤整合起来，验证zkWasm XOR指令的端到端正确性定理。以下验证是在交互式证明环境中完成的，其中每一个形式化构造和逻辑推理步骤都经过了最严格的机器检查。
如上所见，形式化验证zkVM电路是可行的。但这是一项艰巨的任务，需要理解和追踪很多复杂的不变性质。这反映了被验证软件本身的复杂性：验证中所涉及的每一条引理都需要得到电路开发者的正确处理。鉴于其中的风险很高，让它们由形式化验证系统进行机器检验，而不是仅仅依靠小心谨慎的人工审查，是非常有价值的。
