深入理解ZK虚拟机

Cyfrin 发布于 2026-04-04 阅读 13

本文深入解析了ZK虚拟机的原理与实现。前半部分构建概念基础:零知识证明、算术电路、将计算转化为代数方程,以及从证明特定计算转向证明虚拟机执行。后半部分用Rust实现了一个基于STARK的最小ZKVM,包含6条指令、4个寄存器,逐步展示了执行、轨迹生成、代数约束(AIR)、证明生成与验证的完整流程。文章最后讨论了真实ZKVM缺失的特性(内存、零知识、边界约束等),并提供了丰富的学习资源和生产级ZKVM列表。

Farouk Elalem

理解 ZK 虚拟机

深入探讨 ZKVM 的工作原理——从 ZK 证明和电路,通过算术化,到在 Rust 中构建一个基于 STARK 的可工作的 ZKVM。

关于 ZKVMs 的高层次解释有很多,充满形式化数学的研究论文也很多。但更难找到的是中间地带:既有足够的理论来理解为什么这个工作流程会如此运作,又有足够的代码来看到如何将所有部分组合在一起。本文旨在填补这一空白。前半部分构建概念基础:ZK 证明、电路、算术化,以及从证明计算到证明机器的转变。后半部分通过用 Rust 构建一个基于 STARK 的可工作的 ZKVM 使其具体化,逐步讲解执行、迹生成、代数约束和证明验证。


1. 零知识证明

你可以证明一个计算被正确执行,而无需透露它是如何完成的。不是通过模糊细节或加密输出,而是通过构建一个数学论证,该论证能说服验证者,同时不透露中间步骤的任何信息。这个性质以及其背后的机制,使得本文中的所有内容成为可能。

在我们这里关心的系统中,证明者运行一个计算并产生一个小的证明。验证者无需重新执行任何操作即可检查它。证明相对于计算来说非常小,验证相对于执行来说非常快。

形式化框架依赖于三个性质:

  • 完备性: 如果证明者是诚实的(计算确实产生了声称的结果),验证者将始终接受。诚实的证明者永远不会被拒绝。
  • 可靠性: 如果证明者是不诚实的(声称的结果是错误的),验证者将以压倒性的概率拒绝。不诚实的证明者被拒绝的概率可以忽略不计。
  • 零知识: 证明除了陈述的真实性之外不透露任何信息。验证者得知结果是正确的,但不会获得关于中间步骤或私有输入的任何信息。

在许多区块链可扩展性背景下,零知识属性是次要的。最重要的是简洁性:证明很小且检查速度快,即使原始计算非常庞大。因此,这些系统通常被描述为有效性证明而非零知识证明。主要目标是压缩验证,而不是隐藏信息。一个典型的 ZK rollup 并不特别关心向 L1 验证者隐藏交易数据;它关心的是不让 L1 重新执行每笔交易。

许多证明系统遵循相同的基本模式:证明者首先承诺数据,然后回答验证者的挑战,这些答案之间的一致性说服了验证者。在实践中,验证者挑战是使用哈希函数从证明者的承诺中确定性地推导出来的(一种称为 Fiat-Shamir 变换的技术),因此整个协议变得非交互式。证明者产生一个单一的证明对象,验证者离线检查它。无需来回通信。

这是其他一切的基础。问题是:证明者究竟在证明什么?

2. ZK 电路如何工作

要证明一个计算,你首先需要将其表达为证明系统可以推理的形式。在与本文相关的证明系统中,计算必须被表达为有限域上的代数方程。不同的系统以不同的方式做到这一点。最广为人知的表示是算术电路:一个由加法和乘法门组成的有向无环图(DAG)。

一个有限域是一组数字,你可以在其中进行加法、减法、乘法和除法(除零外),并且每个操作都保持在集合内。最简单的例子是素数 $p$ 的整数模。如果 $p = 7$,那么 $5 + 4 = 2$(因为 $9 \bmod 7 = 2$),并且每个非零元素都有一个乘法逆元($3 \times 5 = 1 \bmod 7$,所以 $3^{-1} = 5$)。现代 SNARKs 和 STARKs 使用大得多的有限域,但算术遵循相同的规则。

要理解计算如何变成代数,算术电路是最清晰的起点。在算术电路中,计算通过导线流动。每条导线携带一个域元素。门取输入导线,执行一个操作(加法或乘法),并产生一个输出导线。一个计算 $x^2 + x + 5$ 的电路可能看起来像:

算术电路:$x^2 + x + 5$

该电路中的每个门产生一个代数约束,一个必须成立的方程。乘法门说 $a \times b = c$,其中 $a$ 和 $b$ 是输入导线,$c$ 是输出导线。加法门说 $a + b = c$。整个电路是一个在域上的多项式方程组。

见证是所有导线值(输入、中间值和输出)的集合,这些值同时满足每个约束。证明者知道见证;验证者不知道。证明意味着展示你知道一个可满足的赋值,一组使每个门方程成立的导线值。在零知识设置中,这可以在不透露这些导线值的情况下完成。

不同的证明系统对这些约束进行不同的编码。Groth16 使用一种称为 R1CS(Rank-1 约束系统)的格式,其中每个约束被写为两个线性组合的乘积等于第三个。Plonk 使用基于门的表述,并带有额外的约束,这些约束将导线连接起来跨越电路。但底层思想在所有系统中都是相同的:计算变成一个多项式方程组,而证明就是展示你知道一个解。

这是一个具体的例子。假设你想证明你知道一个 $x$ 使得 $x^3 + x + 5 = 35$。该电路将有:

  1. 一个乘法门: $v_1 = x \times x$(计算 $x^2$)
  2. 一个乘法门: $v_2 = v_1 \times x$(计算 $x^3$)
  3. 一个加法门: $v_3 = v_2 + x$(计算 $x^3 + x$)
  4. 一个加法门: $out = v_3 + 5$(计算 $x^3 + x + 5$)
  5. 一个约束: $out = 35$(公共输出)

这里,$35$ 是公共输出(所证明陈述的一部分),而 $x$ 是私有见证。证明者知道 $x = 3$(因为 $27 + 3 + 5 = 35$)以及所有中间值。在零知识设置中,证明者可以令验证者确信存在这样一个 $x$,而无需透露 $x = 3$。

ZK 电路浏览器

算术电路并不是为证明而表示计算的唯一方式。基于 STARK 的系统,包括我们将在本文后面构建的系统,使用不同的表示:它们记录逐步执行的迹,并将正确性规则表示为该迹上的多项式约束(这种方法称为 AIR,我们在第 11 节中详细介绍)。底层原理是相同的:将计算简化为多项式方程。但这些方程的结构以及构建它们的方式有所不同。我们在这里从电路开始,因为它们使核心思想具体化。我们接下来描述的局限性同样适用于任何为每次计算手工制作约束的方法。

3. 自定义约束系统的局限性

无论你使用算术电路、AIR 约束还是任何其他代数表示,传统模型都需要一个针对每类计算定制的约束系统。

如果你想证明一个斐波那契计算,你要构建一个斐波那契约束系统。如果你想证明一个 Merkle 树包含,你要构建一个 Merkle 约束系统。如果你想证明一个签名是有效的,你要构建一个签名约束系统。每一个都成为它自己的工程项目:设计约束、审计系统、测试可靠性漏洞,即允许无效证人通过的约束系统中的错误。

这些约束在实践中甚至更具限制性。这些约束系统是静态且固定大小的。没有传统意义上的循环和分支:

  • 一个迭代 $n$ 次的“循环”通常必须在编译时被展开为循环体的 $n$ 个副本。一个迭代 1000 次的循环会产生大约大 1000 倍的约束系统。而且迭代次数必须是固定的。你不能有一个循环“直到满足某个条件”的系统。
  • 一个“if-else”分支通常通过评估两个候选结果并使用一个选择器来选择正确的一个来编码。换句话说,条件逻辑被编译成算术,而不是作为运行时分支执行。即使只有一个分支在逻辑上被采用,两个分支都会消耗计算。

结果,编写约束系统的感觉完全不像编写普通程序。开发者通常依赖专门的语言和工具链,如 CircomNoir课程)。调试很困难:当一个约束不满足时,错误信息是“约束 4,372 失败”,而不是“第 42 行:索引越界”。审计很难,因为约束系统与原始计算意图相去甚远。而且开发者群体很小,因为约束工程需要同时在密码学、代数和证明系统的特定格式方面有专业知识。

对于简单、范围明确的应用程序,如证明 Merkle 包含或验证单个签名,这个模型是实用的。但随着你需要证明的计算复杂度增长,为每个新应用程序手工制作全新的约束系统变得越来越不切实际。

这不仅是一个理论问题。一旦人们开始尝试证明像以太坊执行那样庞大且不规则的系统,自定义约束系统的局限性就变得显而易见了。ZK rollups 使这个局限性具体化。

4. 为什么 ZK Rollups 需要更好的方法

Rollups 成为以太坊的主要扩展策略。这个想法很直接:在链下批量执行交易,将生成的承诺发布回 L1(以太坊),并包含某种形式的正确性保证,这样 L1 就不必重新执行所有操作。对于 ZK rollups,这个保证是一个有效性证明:一个简洁的证明,证明该批次被正确执行。

困难在于以太坊不是一个单一用途的计算平台。它是一个通用的智能合约平台。用户部署任意合约(DeFi 协议、NFT 市场、治理系统、游戏),每笔交易都是不同合约的调用,具有不同的逻辑。一个希望与 EVM 兼容的 ZK rollup 不能为每个可能的合约执行手工制作单独的约束系统。没有办法预先知道用户将部署什么合约,而且可能的计算空间是无限的。

要获得通用的 EVM 兼容性,你必须证明 EVM 执行本身的正确性,而不是为每个合约手工制作单独的约束系统。换句话说,你需要一个针对虚拟机本身的约束系统。

这就是 zkEVM 方法,它在技术上要求非常高。EVM 有大约 140 个操作码、复杂的 gas 计量、可以在运行时增长的动态内存、具有冷/热访问模式的持久存储模型、用于加密操作的预编译合约,以及多年来通过 EIP 积累的许多边缘情况。

每个操作码都需要捕捉其行为的代数约束。Gas 计费也必须通过代数方式强制执行。必须跟踪内存扩展成本。结果系统非常庞大,即使是中等规模的批次也会导致大的迹和沉重的证明工作负载。

zkSyncScrollPolygon zkEVM 这样的项目需要多年的工作和大型工程团队来构建这些系统。困难是结构性的:EVM 是为确定性执行而设计的,而不是为可证明性。其不规则的指令集、基于栈的执行模型、动态内存和存储行为以及许多边缘情况,并不自然映射到证明系统所需的规则代数结构。

这种模式并不限于 rollups。一个最近的以太坊 L1 zkEVM 路线图 提议让验证者通过简洁证明来验证区块,而不是重新执行每笔交易。该方法不是构建一个单体的 zkEVM 电路,而是将 EVM 验证逻辑编译为在通用 ZKVM 内运行的程序。zkEVM 变成了“只是一个程序”。

这指向了 zkEVM 工作使之不可避免的更广泛的洞察。一旦你承诺证明一个虚拟机而不是一个特定的计算,你就做了一个概念上的飞跃。约束系统不再编码“这个特定的业务逻辑”。它编码“这台机器的规则”。如果机器是通用的,那么任何在其上运行的程序都自动是可证明的。

这就是 ZKVMs 背后的想法,而且它不一定非得是 EVM。

5. ZKVM 概念:证明机器,而不是计算

ZKVM 是一种证明系统,其中被证明的陈述是:“这个程序,在这个虚拟机上执行,产生这些输出”。约束系统编码 VM 的执行规则(程序计数器如何前进、指令如何修改寄存器、内存读写如何工作),而不是任何特定的计算。

ZKVM 流水线在高层的工作方式如下:

  1. 编译 你的程序为 VM 可以执行的形式。你用高级语言(如 Rust 或 C)编写,编译器将其翻译成 VM 的低级指令。
  2. 执行 程序在 VM 内部,记录每一步作为执行迹:一个表格,其中每一行是一个时钟周期,列跟踪机器的状态(程序计数器、寄存器、内存等)。
  3. 算术化 迹。将 VM 的转换规则编码为迹上的代数约束。“程序计数器增加 1”变成一个多项式方程。“寄存器 r0 被更新为 r1 和 r2 的和”变成另一个多项式方程。
  4. 证明 迹满足所有约束,使用证明系统(SNARK、STARK 等)生成一个简洁的证明。
  5. 验证 证明比重新执行完整计算快得多。

ZKVM 流水线ZKVM 流水线📝编译高级代码 → VM 指令⚙执行在 VM 上运行,记录执行迹𝑓算术化VM 规则变成多项式约束🔒证明承诺、FRI、生成简洁的 STARK 证明✓验证检查证明,永不重新执行程序program.rstrace 表C(x), Q(x)STARK 证明✓ / ✗

关键点在于工程努力的去向。在每计算一模型下,每个新应用程序都需要新的约束工程。在 ZKVM 模型下,工程努力投入到构建 VM 的约束系统一次,然后任何编译到该 VM 的程序都自动是可证明的。一次性成本很高(构建 ZKVM 是一个重大的工程项目),但每个新程序的边际约束工程成本急剧下降。

这就是使 ZKVMs 对 rollups、协同处理器、桥以及任何需要证明任意计算的应用程序实用的原因。你不需要为每个新用例配备一个约束工程师团队。你需要一个编译器工具链和一个 ZKVM。

在本文的下一部分,我们将使所有这些具体化。我们将逐步完成一个完整的 ZKVM 实现,一个用 Rust 编写的极小但功能完整的基于 STARK 的系统,并追溯流水线的每一步:从定义指令集,到执行程序,再到生成和验证证明。代码故意简单:6 条指令、4 个寄存器、无内存。但它仍然捕捉了与大规模系统(如 RISC ZeroSP1)相同的底层 STARK 流水线。

在我们编写任何代码之前,我们需要理解我们实际上在证明什么。ZKVM 证明一台机器正确执行。这从机器在底层如何实际工作开始:指令是什么、状态如何逐步变化,以及需要什么将这些规则表达为证明系统可以检查的方程。

6. 什么是指令集架构?

CPU 如何执行指令

剥离操作系统、浏览器和编程语言。在栈的底部,CPU 在一个循环中做一件事:获取下一条指令、解码它、执行它、重复。你曾经运行过的每个程序都归结为这个每秒执行数十亿次的循环。

指令集架构 (ISA) 是精确定义这个循环的契约。它指定了存在哪些指令(CPU 知道的操作)、它们操作什么状态(寄存器、内存、程序计数器)以及它们如何在二进制中编码。ISA 形成了软件和硬件之间的边界。编译器将高级代码转换为 ISA 指令,硬件执行它们,双方都不需要知道对方的内部结构。

几乎每个 ISA 中都会出现三个概念:

寄存器 是 CPU 的便签本,一个小的快速存储槽,指令从中读取和写入。一个典型的 CPU 可能有 32 个通用寄存器,每个保存一个单字(32 或 64 位)。算术指令从寄存器获取输入,并将结果写回寄存器。

操作码 命名操作。每条指令都有一个操作码,告诉 CPU 要做什么ADD 意味着将两个值相加,MUL 意味着相乘,LOAD 意味着从内存中获取一个值到寄存器,BEQ 意味着如果两个值相等则分支(跳转)。操作码通常是指令二进制编码的前几位。

程序计数器 (PC) 跟踪我们在程序中的位置。它保存当前指令的地址。执行指令后,PC 通常前进到下一条,除非该指令是分支或跳转,在这种情况下 PC 被设置为不同的地址。

这些一起给了我们取指-译码-执行循环:

取指-译码-执行循环

取指-译码-执行循环

程序

▸0LOADr0 = 10

1LOADr1 = 3

2ADDr2 = r0 + r1

3ADDr0 = r2 + r1

4HALT停止

寄存器

r00

r10

r20

r30

PC0

取指›译码›执行›写回

步进重置

在执行的每一步,机器的状态可能会改变:寄存器获得新值,PC 向前移动,也许内存位置被更新。这些状态变化的完整序列就是我们稍后称之为执行迹的东西,并且这正是 ZKVM 需要证明正确的东西。

为什么 ISA 设计对可证明性重要

回想一下,ZKVM 通过将 VM 的规则编码为代数约束(每个有效执行步骤必须满足的多项式方程)来工作。这就是 ISA 设计直接影响到可证明性的地方。

更少的指令意味着更少的约束。 每个操作码都需要捕捉其行为的约束:ADD 需要一个目的寄存器保存和的约束,MUL 需要一个乘积的约束,等等。像 x86 这样具有非常庞大且历史积累的指令集的 ISA,将需要大量的约束集。像 RISC-V 这样只有 47 个基础整数指令的最小 ISA,则更容易处理。

统一的指令格式意味着规则的约束结构。 当每条指令具有相同的位布局(操作码在这里,目的寄存器在那里,源寄存器在那里)时,你可以编写一个处理译码的通用约束模板,并为每个操作码专门化它。具有可变长度指令的 ISA(如 x86,其中一条指令可以是从 1 到 15 字节的任何长度)将需要仅仅为了弄清楚一条指令在哪里结束、下一条在哪里开始而设置约束。RISC-V 标准的固定宽度基本编码完全避免了这一点。

简单的操作意味着更低次数的约束。 每个约束都是一个多项式方程,多项式次数很重要。更高次数的约束会使证明更大且更昂贵。一个简单的“加两个寄存器”指令产生一个低次数的约束。一个更复杂的指令要么导致更复杂的约束,要么必须被分解成几个更简单的约束步骤。

这就是为什么 RISC-V 已成为通用 ZKVMs 的主流选择。它是一个现代的、开源的 ISA,设计具有证明系统所奖励的那种规律性:较少的指令、固定宽度的编码、简单的操作。像 RISC Zero、SP1 和 zkSync 的 Airbender 这样的系统使用 RISC-V 作为编译目标,并证明结果迹的执行。你用 Rust 编写程序,Rust 编译器发出 RISC-V 指令,ZKVM 证明这些指令被正确执行。

有些项目走得更远,专门为可证明性设计 ISA:

  • Cairo (StarkWare) 使用自定义 ISA,其中指令几乎直接映射到低次数的 AIR 约束。VM 有一个单只读内存、一个程序计数器和一个分配指针。每条指令都被设计成易于约束。
  • Miden VM (Polygon) 是一个基于栈的 VM。值保存在一个栈上,而不是命名的寄存器。栈操作自然映射到简单的转换约束。

这些自定义 ISA 可以实现比 RISC-V 更好的证明性能(因为每条指令都考虑到了证明系统),但它们牺牲了工具链兼容性。你不能仅仅将现有的 Rust 代码编译为 Cairo 程序而不需要专门的编译器。

权衡很清楚:RISC-V 给你编程生态系统;自定义 ISA 给你证明效率。 两种方法都在生产环境中积极使用。

有了这个基础,我们理解了机器是什么:一个状态(寄存器、PC)根据 ISA 的规则随时间演化。ZKVM 需要证明这种演化是正确的,每一步都遵循了规则。下一节看“证明正确执行”实际上意味着什么,然后再引入任何特定的证明机制。


7. 证明执行正确性

在深入任何特定的数学或密码学之前,让我们从概念层面理解证明一台机器被正确执行的策略。

执行迹

当 CPU 执行一个程序时,其状态在每个执行步骤中都会改变:程序计数器移动,寄存器获得新值,当前指令从一个步骤变化到另一个步骤。如果你在每一步记录该状态的快照,并将每个快照写为表中的一行,你就能得到机器所做一切的完整记录。

这个表就是执行迹。每一行是一个完整的快照。迹是确定性的。给定相同的程序和相同的输入,你总是得到相同的表。当我们在第 9 节构建我们的 VM 时,我们将看到确切的列布局,但这个想法很简单:每个执行步骤一行,每块机器状态一列。

迹是整个 ZKVM 流水线中的核心对象。接下来的一切(多项式、约束、证明)都是为了回答一个问题:这个迹有效吗?

“正确执行”意味着什么

一个有效的迹不仅仅是任意数字表。每对连续的行必须与 ISA 的规则一致。如果某行的操作码是 ADD,那么下一行的状态必须反映该加法的结果。

具体来说,对于从行 $i$ 到行 $i+1$ 的每个转换,ISA 施加了如下规则:

  • 时钟前进: $cycle[i+1] = cycle[i] + 1$
  • PC 正确更新: 对于大多数指令,$pc[i+1] = pc[i] + 1$。对于 HALT,PC 保持不变。
  • 正确的寄存器改变: 如果操作码是 $ADD\ rd, rs1, rs2$,那么行 $i+1$ 中寄存器 $rd$ 的值必须等于行 $i$ 中寄存器 $rs1$ 和 $rs2$ 值的和。
  • 其他寄存器不变: 每个不是目的寄存器的寄存器必须在行 $i+1$ 中与行 $i$ 中具有相同的值。

如果每一对连续的行都满足所有这些规则,那么迹代表一个有效的执行。如果甚至一个转换违反了一条规则,迹就是无效的。某些事情出错了(或是被伪造了)。

这给了我们一个清晰的定义:证明正确执行 = 证明迹中每一个行到行的转换都满足 ISA 的规则。

算术化思想

这是关键步骤。我们刚刚用英语描述的那些规则(“时钟前进”、“正确的寄存器改变”)可以被写成方程。每个规则变成一个当规则满足时等于零的表达式:

规则(英文) 方程(代数)
“时钟前进 1” $cycle[i+1] - cycle[i] - 1 = 0$
“当指令不写入 r0 时,寄存器 r0 保持不变” $(r0[i+1] - r0[i]) \times s = 0$,其中 $s = 0$ 当 r0 是目的寄存器时
“PC 增加 1” $pc[i+1] - pc[i] - 1 = 0$

如果我们将所有规则都写成这样的方程,那么一个有效的迹就是每个方程在每一行都等于零的迹。

这被称为算术化:将计算规则转化为算术,或者更准确地说,转化为代数方程。它是弥合“计算机执行了程序”和“一组数学方程被满足”之间差距的关键步骤。

为什么这有用?因为多项式方程的世界有强大的工具。一旦我们的规则是方程,我们可以:

  1. 将迹编码为多项式(每列一个多项式,通过该列中的所有值)
  2. 将规则表达为多项式恒等式(必须在迹的所有点上都成立的方程)
  3. 使用证明系统有效地验证这些恒等式

关键性质:多项式方程可以被高效检查。证明系统不是单独验证迹的每一行,而是可以将所有这些检查压缩成一个单一的多项式关系,验证者在少数几个随机点上对其进行评估。我们将在第 10 节中看到这具体是如何工作的。

证明流水线

综合起来,这里是 ZKVM 遵循的完整流水线,我们将在接下来的章节中逐步构建:

证明流水线

1

在 VM 上执行程序

运行取指-译码-执行循环

2

记录执行迹

机器状态表,每周期一行

3

将每列编码为多项式

对迹域进行拉格朗日插值

4

将 VM 规则表达为多项式约束

必须在每一行等于零的方程


5

证明所有约束成立

承诺、商、FRI → 简洁的 STARK 证明

6

验证者检查少数几个抽查点

永不重新执行程序

步骤 1–4:详细构建 ZKVM 特定工程

步骤 5–6:通用 STARK 基础设施在所有系统间共享

步骤 1–4 是“VM 侧”:定义计算并将其规则编码为代数。步骤 5–6 是“证明侧”:数学和密码学。我们将详细构建 VM 侧。对于证明侧,我们将涵盖足够的内容以理解每一步做什么以及为什么。证明机制是所有 STARK 系统共享的通用基础设施。

该流水线中的每一步都映射到我们代码库中的一个模块。让我们从我们自己的玩具指令集和 VM 开始。


8. 我们的玩具 ZKVM:指令集

机器

是时候打开代码库了。以下是我们的玩具 ZKVM 的规范:

  • 4 个寄存器 (r0-r3)
  • 6 条指令 (NOP, IMM, ADD, MUL, SUB, HALT)
  • 没有内存,所有数据都存在于寄存器中
  • 所有算术在有限域中进行(Goldilocks 域,我们将在第 10 节中介绍)

这是一个最小的 VM,围绕与生产级 ZKVMs(如 RISC Zero 或 SP1)相同的核心思想构建。我们在这里学到的一切都直接映射到这些系统的工作方式。

6 个操作码

这是完整的指令集,全部六个操作码:

操作码 操作 描述
NOP 0 (无) 无操作。用于填充迹。
IMM 1 $rd = imm$ 将立即数加载到寄存器。
ADD 2 $rd = rs1 + rs2$ 加两个寄存器,存储结果。
MUL 3 $rd = rs1 * rs2$ 乘两个寄存器,存储结果。
SUB 4 $rd = rs1 - rs2$ 减两个寄存器,存储结果。
HALT 5 (停止) 结束执行。

有几点值得注意:

每个算术操作都是域操作,而不是常规整数操作。当我们说 $rd = rs1 + rs2$ 时,我们指的是模 Goldilocks 素数加法。算术直接模 Goldilocks 素数定义,因此没有单独的溢出行为需要考虑。域算术就是语义。这很重要,因为证明系统在这个域上工作,VM 必须匹配。

NOP 用于填充。 证明系统要求迹长度为 2 的幂,因此短程序用 NOP 行填充(第 9 节)。

没有分支或跳转。 执行严格顺序:普通指令上 PC 增加 1,HALT 终止执行。这是一个主要的简化。真实的 ISA 有条件分支、函数调用和循环。我们省略它们,因为它们会增加约束复杂性而不会教授新概念。

在 Rust 中,操作码是一个带有整数值的简单枚举:

#[derive(Debug, Clone, Copy, PartialEq, Eq)]
#[repr(u8)]
pub enum Opcode {
    Nop  = 0,  // 无操作(用于迹填充)
    Imm  = 1,  // rd = imm
    Add  = 2,  // rd = rs1 + rs2
    Mul  = 3,  // rd = rs1 * rs2
    Sub  = 4,  // rd = rs1 - rs2
    Halt = 5,  // 停止执行
}

#[repr(u8)] 属性确保每个操作码映射到一个特定的整数。这很重要,因为迹将操作码存储为数值域元素,稍后约束系统将使用这些值来选择正确的指令行为。

指令编码

每条指令使用相同的统一格式,五个字段,总是存在:

pub struct Instruction {
    pub opcode: Opcode,  // 哪个操作(0–5)
    pub rd: u8,          // 目的寄存器索引(0–3)
    pub rs1: u8,         // 第一个源寄存器索引(0–3)
    pub rs2: u8,         // 第二个源寄存器索引(0–3)
    pub imm: u64,        // 立即值(由 IMM 指令使用)
}

不是每条指令都使用每个字段。ADD 使用 $rd$、$rs1$ 和 $rs2$,但忽略 $imm$。IMM 使用 $rd$ 和 $imm$,但忽略 $rs1$ 和 $rs2$。HALT 忽略所有字段。但格式总是相同的。每条指令在迹中占据完全相同的“形状”。

这种统一性是故意的,并且对证明系统很重要。 如果不同的指令有不同数量的字段,迹表将有一个不规则的结构,这更难约束。通过统一的格式,迹的每一行具有相同的 13 列,约束系统可以将相同的多项式模板应用于每一行。

为了使程序可读,构建器函数让你自然地编写指令:

impl Instruction {
    pub fn nop() -> Self {
        Instruction { opcode: Opcode::Nop, rd: 0, rs1: 0, rs2: 0, imm: 0 }
    }

    pub fn imm(rd: u8, value: u64) -> Self {
        assert!(rd < 4, "寄存器索引必须为 0–3");
        Instruction { opcode: Opcode::Imm, rd, rs1: 0, rs2: 0, imm: value }
    }

    pub fn add(rd: u8, rs1: u8, rs2: u8) -> Self {
        assert!(rd < 4 && rs1 < 4 && rs2 < 4);
        Instruction { opcode: Opcode::Add, rd, rs1, rs2, imm: 0 }
    }

    pub fn mul(rd: u8, rs1: u8, rs2: u8) -> Self {
        assert!(rd < 4 && rs1 < 4 && rs2 < 4);
        Instruction { opcode: Opcode::Mul, rd, rs1, rs2, imm: 0 }
    }

    pub fn sub(rd: u8, rs1: u8, rs2: u8) -> Self {
        assert!(rd < 4 && rs1 < 4 && rs2 < 4);
        Instruction { opcode: Opcode::Sub, rd, rs1, rs2, imm: 0 }
    }

    pub fn halt() -> Self {
        Instruction { opcode: Opcode::Halt, rd: 0, rs1: 0, rs2: 0, imm: 0 }
    }
}

注意寄存器索引上的 assert! 守卫。只有 4 个寄存器(0–3),所以任何超出该范围的索引都是错误。未使用的字段被清零,而不是未定义。这很重要:当这些值进入迹时,它们成为输入到约束的域元素。让它们为垃圾会导致约束违反。注意这些是程序构造时的 Rust 级别检查。它们不会在证明中产生代数约束,因此直接构造迹的恶意证明者可以绕过它们。为了简单起见,我们省略了相应的代数范围检查,并在第 14 节中回到这一点。

为什么是这个 ISA?

你可能想知道:为什么不加更多指令?为什么没有内存?为什么只有 4 个寄存器?

正如第 6 节所解释的,更少的指令意味着更少的约束,更简单的操作通常导致更简单、更低次数的约束系统。这个 ISA 捕捉了每个 ZKVM 必须处理的三个基本关注点:操作码分发(选择器)、寄存器读/写(寄存器选择器)和算术正确性,而无需真实 ISA 的偶然复杂性。像 RISC Zero 这样的生产系统在更大、更丰富的 ISA 上运行,具有更大的寄存器文件和更多的指令,但底层的约束模式是相似的。通过从小处着手,我们可以清楚地看到它们。


9. 执行程序并生成迹

取指-译码-执行循环

定义了我们的指令集后,VM 遵循第 6 节中确定的取指-译码-执行循环:

pub fn execute(program: &[Instruction]) -> ExecutionTrace {
    let mut regs: [Fp; 4] = [Fp::ZERO; 4];
    let mut pc: usize = 0;
    let mut rows: Vec<TraceRow> = Vec::new();

    loop {
        let inst = &program[pc];
        let clk = rows.len() as u64;

        // 查找源寄存器值
        let rs1_val = regs[inst.rs1 as usize];
        let rs2_val = regs[inst.rs2 as usize];

        // 在执行此指令之前记录状态
        rows.push(TraceRow {
            clk: Fp::new(clk),
            pc: Fp::new(pc as u64),
            opcode: Fp::new(inst.opcode as u64),
            rd: Fp::new(inst.rd as u64),
            rs1: Fp::new(inst.rs1 as u64),
            rs2: Fp::new(inst.rs2 as u64),
            imm: Fp::new(inst.imm),
            r0: regs[0],
            r1: regs[1],
            r2: regs[2],
            r3: regs[3],
            rs1_val,
            rs2_val,
        });

        // 执行指令
        match inst.opcode {
            Opcode::Nop  => {}
            Opcode::Imm  => { regs[inst.rd as usize] = Fp::new(inst.imm); }
            Opcode::Add  => { regs[inst.rd as usize] = rs1_val + rs2_val; }
            Opcode::Mul  => { regs[inst.rd as usize] = rs1_val * rs2_val; }
            Opcode::Sub  => { regs[inst.rd as usize] = rs1_val - rs2_val; }
            Opcode::Halt => { break; }
        }

        pc += 1;
    }

    ExecutionTrace::new(rows)
}

初始状态为零:所有寄存器都是 Fp::ZERO,PC 为 0。每次迭代获取 program[pc] 处的指令,将当前状态记录为迹行,执行指令,对于非 HALT 指令,增加 PC。HALT 终止循环。

这里有一个微妙但关键的细节:迹记录的是每条指令执行之前的状态,而不是之后。 看顺序:我们先推送 TraceRow然后执行 match。这意味着迹中的第 $i$ 行显示了第 $i$ 条指令即将运行时机器状态。该指令的效果出现在第 $i+1$ 行。

为什么?因为转换约束关联连续的行:它们说“给定第 $i$ 行的状态和第 $i$ 行的操作码,第 $i+1$ 行的状态必须是如此这般”。如果我们在执行之后记录状态,我们需要往回看一行才能找到引起变化的操作码,这会使约束结构复杂化。

执行迹表

每个迹行在 13 个字段中捕获完整的 VM 状态:

pub struct TraceRow {
    pub clk: Fp,      // 时钟周期 (0, 1, 2, ...)
    pub pc: Fp,       // 程序计数器
    pub opcode: Fp,   // 当前指令的操作码 (0–5)
    pub rd: Fp,       // 目的寄存器索引
    pub rs1: Fp,      // 第一个源寄存器索引
    pub rs2: Fp,      // 第二个源寄存器索引
    pub imm: Fp,      // 立即值
    pub r0: Fp,       // 寄存器 0 的值
    pub r1: Fp,       // 寄存器 1 的值
    pub r2: Fp,       // 寄存器 2 的值
    pub r3: Fp,       // 寄存器 3 的值
    pub rs1_val: Fp,  // 寄存器 rs1 的值
    pub rs2_val: Fp,  // 寄存器 rs2 的值
}

前 7 列(clkimm)描述正在发生什么:哪条指令正在执行以及它的操作数是什么。接下来的 4 列(r0r3)捕获机器状态,每个寄存器的值。最后 2 列(rs1_valrs2_val)是从源寄存器读取的实际值。

rs1_valrs2_val 列可能看起来多余。我们在行中已经有 r0r3,而 rs1 告诉我们要读取哪个寄存器。但是约束系统处理的是列值上的多项式方程。它没有办法说“查找索引为 $rs1$ 的寄存器”,因为那需要数组索引,而多项式不能做到这一点。相反,我们显式地存储查找出的值,并使用额外的约束来验证它们匹配正确的寄存器。第 11 节将详细介绍如何做到这一点。

运行示例:$(3 + 4)^2 - (3 + 4) = 42$

让我们追踪一个具体的程序。这是来自 main.rs 的程序。它计算 $(3 + 4)^2 - (3 + 4) = 49 - 7 = 42$:

let program = vec![
    Instruction::imm(0, 3),       // r0 = 3
    Instruction::imm(1, 4),       // r1 = 4
    Instruction::add(2, 0, 1),    // r2 = r0 + r1 = 7
    Instruction::mul(3, 2, 2),    // r3 = r2 * r2 = 49
    Instruction::sub(0, 3, 2),    // r0 = r3 - r2 = 42
    Instruction::halt(),          // 停止
];

六条指令。让我们逐步执行并看看迹是什么样的。记住,每一行记录的是指令执行之前的状态:

第 0 行, IMM r0, 3 所有寄存器从 0 开始。迹记录 $clk=0, pc=0, opcode=1(IMM), rd=0, imm=3, r0=0, r1=0, r2=0, r3=0$。执行后,$r0$ 变为 3。

第 1 行, IMM r1, 4 现在 $r0=3$ 来自上一步。迹记录 $clk=1, pc=1, opcode=1(IMM), rd=1, imm=4, r0=3, r1=0, r2=0, r3=0$。执行后,$r1$ 变为 4。

第 2 行, ADD r2, r0, r1 寄存器为 $r0=3, r1=4$。迹记录 $clk=2, pc=2, opcode=2(ADD), rd=2, rs1=0, rs2=1, r0=3, r1=4, r2=0, r3=0, rs1_val=3, rs2_val=4$。执行后,$r2$ 变为 7。

第 3 行, MUL r3, r2, r2 寄存器为 $r0=3, r1=4, r2=7$。迹记录 $clk=3, pc=3, opcode=3(MUL), rd=3, rs1=2, rs2=2, r0=3, r1=4, r2=7, r3=0, rs1_val=7, rs2_val=7$。执行后,$r3$ 变为 49。

第 4 行, SUB r0, r3, r2 寄存器为 $r0=3, r1=4, r2=7, r3=49$。迹记录 $clk=4, pc=4, opcode=4(SUB), rd=0, rs1=3, rs2=2, r0=3, r1=4, r2=7, r3=49, rs1_val=49, rs2_val=7$。执行后,$r0$ 变为 42。

第 5 行, HALT 寄存器为 $r0=42, r1=4, r2=7, r3=49$。迹记录 $clk=5, pc=5, opcode=5(HALT), r0=42, r1=4, r2=7, r3=49$。执行停止。

这里是完整的迹表:

clk pc op rd rs1 rs2 imm r0 r1 r2 r3 rs1_val rs2_val
0 0 1 0 0 0 3 0 0 0 0 0 0
1 1 1 1 0 0 4 3 0 0 0 3 3
2 2 2 2 0 1 0 3 4 0 0 3 4
3 3 3 3 2 2 0 3 4 7 0 7 7
4 4 4 0 3 2 0 3 4 7 49 49 7
5 5 5 0 0 0 0 42 4 7 49 42 42

VM 执行迹查看器

注意相邻行如何编码 ISA 规则。在第 2 行和第 3 行之间:操作码是 2 (ADD),$rd=2$,$rs1_val=3$,$rs2_val=4$,在第 3 行中 $r2$ 从 0 变为 7 $(= 3 + 4)$。每个其他寄存器都保持不变。这正是转换约束将验证的内容,但通过代数方式,而不是通过检查。

填充到 2 的幂

我们的程序产生了 6 个迹行。但证明系统需要迹长度是 2 的幂(我们将在第 10 节中看到原因)。所以 6 行必须变成 8 行。

填充行是什么都不做的 NOP 指令。寄存器冻结在它们的最后一个值:

pub fn pad_to_power_of_two(&mut self) {
    let target = self.rows.len().next_power_of_two();
    while self.rows.len() < target {
        let clk = self.rows.len() as u64;
        let prev = *self.rows.last().unwrap();
        self.rows.push(TraceRow::padding(clk, &prev));
    }
}

每个填充行从前一行构建:

pub fn padding(clk: u64, prev: &TraceRow) -> Self {
    TraceRow {
        clk: Fp::new(clk),
        pc: prev.pc,                        // PC 保持不变
        opcode: Fp::new(Opcode::Nop as u64), // NOP 指令
        rd: Fp::ZERO,
        rs1: Fp::ZERO,
        rs2: Fp::ZERO,
        imm: Fp::ZERO,
        r0: prev.r0,    // 所有寄存器从前一行复制
        r1: prev.r1,
        r2: prev.r2,
        r3: prev.r3,
        rs1_val: prev.r0,  // rs1=0,所以 rs1_val = r0
        rs2_val: prev.r0,  // rs2=0,所以 rs2_val = r0
    }
}

有几点需要注意:

  • 时钟继续增加。 约束系统将检查 一行 $clk[i+1] = clk[i] + 1$,包括填充行。
  • PC 冻结。 在迹的填充尾部,NOP 行被视为停止状态:PC 和寄存器保持不变。这是对 AIR 的一个建模选择,而不是关于运行时 NOP 通常如何行为的声明。我们将 HALT 和填充都折叠为“没有进一步状态变化”的情况,以保持约束简单。
  • 寄存器值被复制 从前一行。由于 NOP 不修改任何寄存器,“下一行具有相同的寄存器值”约束被平凡地满足。
  • $rs1_val$ $rs2_val$ 必须是一致的,因为填充行中 $rs1=0$ 且 $rs2=0$,两个查找值必须等于 $r0$。填充函数正确设置了这一点。

最后一点很重要。你不能只用零填充行。它们仍然必须满足每个转换约束。一个声称 $rs1=0$ 但 $rs1_val=999$ 的填充行将无法通过寄存器查找约束。填充在约束系统下必须是有效的,而不仅仅是空的空间。

填充后,我们的 6 行迹变成 8 行,填充后的迹现在满足证明流水线的结构要求。


10. STARK 证明工具箱

我们已经构建了一个 VM,执行了一个程序,并产生了一个迹。现在我们需要证明迹是有效的,而无需验证者重新执行程序。这就是证明机制发挥作用的地方。

流水线的其余部分使用几个数学和密码学构建块:有限域、多项式、求值域、Merkle 树、基于哈希的挑战协议以及称为 FRI 的低次测试协议。这些是通用的 STARK 基础设施。这些成分的变体出现在现代基于 STARK 的系统中,通常以更优化的形式出现。

本节为你提供足够关于每个构建块的直觉,以便理解约束系统(第 11 节)和证明者/验证者流水线(第 12 节)。我们不会深入实现细节或代码。目标是理解每个部分做什么以及为什么需要它。如果数学第一次没有完全理解,那也没关系。一旦你看到了这些部分在行动中,后面的章节会更有意义。

对于想要完整实现故事的读者:请参见 StarkWare 的 STARK 101Vitalik 的 STARKs 系列源代码src/field.rssrc/polynomial.rssrc/domain.rssrc/merkle.rssrc/channel.rssrc/fri.rs)。

有限域算术

我们在第 2 节中已经介绍了有限域:一组数字,其中算术模素数定义,每个非零元素都有一个乘法逆元,并且所有操作都在域内。证明流水线需要所有这些属性:固定大小的元素、精确算术(多项式恒等式必须精确成立)以及通用除法(使多项式除法和插值定义良好)。

我们使用的特定域围绕 Goldilocks 素数 构建:$p = 2^{64} - 2^{32} + 1$。选择它是因为它适合单个 64 位字(快速算术)并支持证明系统所需的 2 的幂域大小(正如我们将在本节稍后看到的)。你在代码中看到的每个类型为 Fp 的值都是 mod 这个素数的数字。

迹列变成多项式

迹是一个数字表。证明系统处理多项式。所以第一步是将迹的每一列转换为一个多项式。这意味着什么?

以我们 8 行迹中的 clk 列为例:它包含值 $[0, 1, 2, 3, 4, 5, 6, 7]$(时钟每一行都递增,即使在填充期间)。我们想要一个多项式 $P(x)$,使得当我们在 8 个特定点上求值时,我们得到完全这 8 个值。即:

P(d₀) = 0,  P(d₁) = 1,  P(d₂) = 2,  ...,  P(d₇) = 7

其中 $d_0, d_1, \ldots, d_7$ 是迹域中的点(一组 8 个特殊的域元素,我们将在本节稍后定义)。多项式编码了这一列:它在域点处的值正好是列中的条目。

给定 $n$ 个不同的点和 $n$ 个值,恰好有一个次数小于 $n$ 的多项式通过它们所有。找到它被称为拉格朗日插值。对于我们的 8 行迹,每一列变成一个 7 次多项式。我们对所有 13 列这样做,产生 13 个完全编码迹的多项式。

为什么费这个劲?因为一旦迹被编码为多项式,我们可以将 VM 的转换规则表达为多项式方程(第 11 节),然后使用一个强大的事实来高效地检查它们。

这是关键洞察:如果你选择一个随机点,并且两个低次多项式在那里给出相同的值,那么它们几乎肯定在所有地方都是相同的多项式。这被称为 Schwartz-Zippel 引理。为什么?一个 $d$ 次多项式最多可以在 $d$ 个点为零。所以如果两个 $d$ 次多项式不同,它们只能在 $\sim 2^{64}$ 个域元素中的 $d$ 个点上“偶然”一致,这对于随机检查来说可能性微乎其微。

这就是为什么在随机点检查多项式恒等式给出了它处处成立的压倒性证据。这就是“验证迹的每一行”如何压缩为“验证少数几个随机求值”的核心。

求值域

在本节前面,我们说迹列在“8 个特殊的域元素”处求值。这些元素是什么,为什么它们特殊?

迹域是迹多项式取实际迹值的点的集合。我们需要 8 个点(每行一个),并且我们选择它们具有非常特定的结构。

选择一个域元素 $\omega$,使得 $\omega^8 = 1$ 但 $\omega$ 的任何更小次幂都不等于 1。那么幂 ${1, \omega, \omega^2, \omega^3, \omega^4, \omega^5, \omega^6, \omega^7}$ 是 8 个不同的元素,循环回到 1。这个集合被称为“8 次单位根”,因为每个元素提升到 8 次方都等于 1。

为了使这具体化,让我们在一个小的域中工作:模 17 的整数。这里 $\omega = 9$ 是一个 8 次单位根,因为 $9^8 \bmod 17 = 1$。8 个域点是 ${1, 9, 13, 15, 16, 8, 4, 2}$。乘以 9 循环遍历它们:$1 \rightarrow 9 \rightarrow 13 \rightarrow 15 \rightarrow 16 \rightarrow 8 \rightarrow 4 \rightarrow 2 \rightarrow 1$。每次乘法只是 $\times 9 \bmod 17$。

我们将迹行分配给这些点:第 0 行在 $1$,第 1 行在 $9$,第 2 行在 $13$,依此类推。其优点是“下一行”总是“乘以 $\omega$”。为了比较第 $i$ 行与第 $i+1$ 行,约束系统只需比较 $P(x)$ 与 $P(\omega x)$。选择一个下面的迹列并逐步查看以看到这个动作:

单位根浏览器

真正的系统使用 Goldilocks 域($p \approx 2^{64}$),它具有直至 $2^{32}$ 的任何 2 的幂大小的单位根。数学是相同的,只是数字更大。我们将在第 11 节中看到这种结构如何使约束检查变得自然。关于有限域中单位根的更深入处理,请参见 RareSkills 的这篇文章

消失多项式与商技巧

在第 11 节中,我们将构建一个约束多项式 $C(x)$,它将我们 VM 的所有 8 个转换规则打包成一个多项式表达式。它如何构建的细节可以等。目前,唯一重要的是一个性质:如果迹是有效的, $C(x)$ 在迹域的每一点处都求值为零。

每个转换规则(“时钟增加 1”、“正确的寄存器更新”等)贡献一个当规则满足时等于零的项。如果所有规则在每一行都成立,整个多项式在每个迹域点处为零。

那么,我们如何证明 $C(x)$ 在所有 8 个迹点处为零而不逐个检查它们?这就是关于多项式的一个基本事实有帮助的地方。如果一个多项式在某个点 $r$ 处为零,那么 $(x - r)$ 能整除它。例如,如果 $f(x)$ 在 $x = 2$、$x = 3$ 和 $x = 5$ 处为零,那么 $(x - 2)(x - 3)(x - 5)$ 能整除 $f(x)$ 且没有余数。这只是代数中的因子定理。

消失多项式 $Z_H(x)$ 是恰好等于零在迹域点处的多项式。写出来就是 $Z_H(x) = (x - 1)(x - \omega)(x - \omega^2)\cdots(x - \omega^{n-1})$。但有一个简化。每个迹域点都是一个 $n$ 次单位根:$(\omega^k)^n = (\omega^n)^k = 1^k = 1$。这意味着每个迹点满足 $x^n = 1$,或等价地 $x^n - 1 = 0$。由于 $x^n - 1$ 是一个 $n$ 次多项式,恰好有 $n$ 个根,并且这些根恰好是我们的迹域点,它一定是同一个多项式:$Z_H(x) = x^n - 1$。这种紧凑形式比将所有 $n$ 个因子乘出来要便宜得多。

如果 $C(x)$ 真的在所有那些点为零,那么 $Z_H(x)$ 必须整除 $C(x)$ 而没有任何余数。

证明者通过计算来证明这一点:$Q(x) = C(x) / Z_H(x)$。如果除法是精确的(没有余数),$Q(x)$ 是一个有效的低次多项式。如果迹是无效的并且 $C(x)$ 在某个迹点不为零,那么除法将不干净,并且 $Q(x)$ 将不是一个合适的低次多项式。证明系统会捕获这一点(通过 FRI,稍后在本节介绍)。

证明者需要在许多点上计算这个商以承诺它(通过 Merkle 树,接下来介绍)。但它不能在迹域点上求值 $C(x) / Z_H(x)$,因为 $Z_H(x) = 0$ 那里,除以零是未定义的。所以证明者在一个单独的、更大的点集上求值,称为 LDE(低次扩展)域。在我们的构造中,这个域比迹域大 8 倍(对于我们的 8 行迹是 64 个点),并且被移位,使得其点都不与迹域重合。移位保证 $Z_H(x) \neq 0$ 在每个 LDE 点,使得除法是安全的。

验证者在随机点 $z$ 处的检查就是:是否 $C(z) = Q(z) \cdot Z_H(z)$?根据 Schwartz-Zippel,如果这在随机点成立,那么它几乎肯定处处成立。

承诺与挑战

两个基础设施部分将代数与真实的证明联系起来:

Merkle 树让证明者承诺多项式的求值。一个单一的 32 字节哈希(树根)锁定了所有数据。之后,证明者可以用一个短的证明路径(从叶子到根的一串兄弟哈希值)揭示任何单个值。验证者检查揭示的值是否与承诺的根匹配。这防止了证明者在事后更改其数据。

Fiat-Shamir 变换将交互式验证者的随机性替换为证明者承诺的确定性哈希值。在交互式证明中,验证者会在证明者每一步之后发送随机挑战。在非交互式证明中,证明者哈希自己的承诺来导出这些挑战。证明者和验证者维护相同的基于哈希的“通道”,输入相同的承诺并挤出相同的挑战。这使得证明成为从证明者到验证者的单一消息,同时确保证明者不能“寻找”有利的随机性。有关可视化演练,请参见 KoalateeCtrl 的这个视频

FRI:低次测试

商技巧只有在 $Q(x)$ 实际上是一个低次多项式时才有效。一个作弊的证明者可以承诺(通过 Merkle 树)不来自任何低次多项式的求值,但仍然在少数采样点通过商检查。我们需要一种方法来验证承诺的求值实际上来自一个低次多项式。

FRI(快速 Reed-Solomon 近邻性交互式谕言)做到了这一点。核心思想是重复压缩:证明者使用通过 Fiat-Shamir 导出的随机挑战,将多项式的求值逐步折叠起来。每一阶段将值的数量减半。如果原始求值来自一个真正的低次多项式,每个阶段保持一致。如果不是,就会出现不一致。经过足够多的折叠轮次后,剩余的对象应该是非常低次的;在我们的玩具设置中,最终只是一个常数。

验证者通过抽查这个过程:它选择随机的查询点,通过 Merkle 证明在每个折叠阶段打开值,并检查每个折叠是否被正确计算。在我们的参数化中,30 个查询给出大约 90 位的可靠性。关于 FRI 的更深入探讨,请参见 StarkWare 的这个视频


11. 从 VM 规则到代数约束

这是 ZKVM 的概念核心。我们有一个迹表和一组 ISA 规则。代数中间表示 (AIR) 将这些规则表达为相邻迹行上的多项式方程。如果所有方程在每一行都等于零,迹就是有效的。

本节是 ZKVM 特定逻辑与第 10 节中证明机制相遇的地方。这里的选择器和约束使得这个特定的 VM 可以证明。不同的 VM(RISC-V、Cairo、Miden)有不同的 AIR,但它们都遵循相同的模式。

选择器多项式取代分支

在 VM 的 execute 函数中,我们使用了 match 语句:

match inst.opcode {
    Opcode::Add => { regs[inst.rd as usize] = rs1_val + rs2_val; }
    Opcode::Mul => { regs[inst.rd as usize] = rs1_val * rs2_val; }
    ...
}

在 AIR 中,我们不能分支。一切必须是一个多项式表达式。那么我们如何处理“对不同操作码做不同事情”?

选择器多项式。 对于每个操作码值 $t$,我们需要一个函数,当 $opcode == t$ 时等于 1,并且对于每个其他有效操作码等于 0。这里有一个简单的方法来构建一个。

从乘积 $(opcode - 0)(opcode - 1)(opcode - 2)(opcode - 3)(opcode - 4)(opcode - 5)$ 开始。对于每个有效操作码,这个乘积等于零,因为其中一个因子总是零。现在删除我们要选择的那个操作码的因子。对于 ADD(操作码 2),删除 $(opcode - 2)$ 因子,剩下 $(opcode - 0)(opcode - 1)(opcode - 3)(opcode - 4)(opcode - 5)$。这个表达式对于除了 2 之外的每个操作码都是零。当 $opcode = 2$ 时,所有剩余的因子都是非零的,给出某个非一的值。除以那个值(我们可以预计算的一个常数)将结果归一化为正好 1。

结果:一个在有效操作码值 0 到 5 上像独热选择器的函数。对于 ADD 返回 1,对于其他所有返回 0。

opcode 0 1 2 3 4 5
sel 0 0 1 0 0 0

这被称为拉格朗日基多项式。在代码中:

pub fn opcode_selector(opcode: Fp, target: u64) -> Fp {
    let mut num = Fp::ONE;
    let mut den = Fp::ONE;
    let t = Fp::new(target);
    for v in 0..NUM_OPCODES {
        if v == target { continue; }
        let fv = Fp::new(v);
        num = num * (opcode - fv);
        den = den * (t - fv);
    }
    num * den.inv()
}

选择器多项式可视化器

这个选择器次数为 5(5 个线性项的乘积)。我们需要对寄存器使用相同的技巧。当一个约束需要检查寄存器 $r2$ 是否是目的寄存器时,它使用一个以相同方式构建的寄存器选择器,但在集合 ${0, 1, 2, 3}$(我们的 4 个寄存器索引)上而不是 ${0, 1, 2, 3, 4, 5}$。这些选择器的次数为 3:

pub fn register_selector(idx: Fp, target: u64) -> Fp {
    let mut num = Fp::ONE;
    let mut den = Fp::ONE;
    let t = Fp::new(target);
    for v in 0..NUM_REGS {
        if v == target { continue; }
        let fv = Fp::new(v);
        num = num * (idx - fv);
        den = den * (t - fv);
    }
    num * den.inv()
}

有了选择器,我们可以将分支转化为算术。我们不写“如果 ADD 做这个,如果 MUL 做那个”,而是计算每个情况,将每个乘以其选择器,然后将它们加起来:

result = sel_add * (rs1_val + rs2_val) + sel_mul * (rs1_val * rs2_val) + ...

这个假设是关键的,但没有通过代数方式强制执行。 如果操作码列包含一个有效值(0–5),那么在任意给定行,恰好一个选择器为 1,其余为 0。除了匹配的那个项之外,每个项都被乘以零而消失。只有正确操作的结果幸存。但如果一个恶意证明者在迹中放置了一个超出范围的值,比如 $opcode = 6$,每个选择器都会求值为某个非零值,约束就会看到所有操作的加权混合,而不是与单个指令的干净匹配。同样的道理适用于 $register_selector$ 中使用的寄存器索引。为了简单起见,我们省略了防止这种情况的代数范围检查,并在第 14 节中讨论其影响。

分支 → 算术

8 个转换约束

现在让我们逐一浏览所有 8 个约束。每一个都是当前行和下一行上的多项式表达式。一个有效的迹使每个约束在每行都求值为零。

首先,一些被多个约束使用的设置值:

let op = current[2];     // opcode
let rd = current[3];     // 目的寄存器索引
let imm = current[6];    // 立即值
let rs1_val = current[11];
let rs2_val = current[12];

// 操作码选择器
let s_nop  = opcode_selector(op, 0);
let s_imm  = opcode_selector(op, 1);
let s_add  = opcode_selector(op, 2);
let s_mul  = opcode_selector(op, 3);
let s_sub  = opcode_selector(op, 4);
let s_halt = opcode_selector(op, 5);

// 这是一个写指令吗? (IMM, ADD, MUL, SUB)
let is_write = s_imm + s_add + s_mul + s_sub;

// 什么值被写入目的寄存器?
let write_val = s_imm * imm
    + s_add * (rs1_val + rs2_val)
    + s_mul * (rs1_val * rs2_val)
    + s_sub * (rs1_val - rs2_val);

$is_write$ 对于任何修改寄存器的指令等于 1,对于 NOP 和 HALT 为 0。$write_val$ 使用选择器技巧为活动的操作码计算正确的结果。只有一个选择器为 1,所以只有匹配的项有贡献。

C0,时钟增加 1:

let c0 = next[0] - current[0] - Fp::ONE;

这是最简单的约束。$clk[i+1] - clk[i] - 1 = 0$ 在每一行,包括填充行。

C1,PC 更新:

let c1 = (s_nop + s_halt) * (next[1] - current[1])
    + (s_imm + s_add + s_mul + s_sub) * (next[1] - current[1] - Fp::ONE);

两种情况:NOP 和 HALT 保持 PC 不变 ($next_pc - cur_pc = 0$),而写指令使其增加 ($next_pc - cur_pc - 1 = 0$)。从第 9 节回顾,在这个 AIR 中,填充的 NOP 行被视为停止状态,所以 NOP 和 HALT 都使 PC 不变。选择器选择正确的情况。由于恰好一个操作码选择器是活动的,恰好一个项是非零的。如果该项为零,约束通过。

C2–C5,寄存器更新(每个寄存器一个约束):

for i in 0..4 {
    let sel_i = register_selector(rd, i as u64);
    let cur_ri = current[7 + i];
    let next_ri = next[7 + i];
    reg_constraints[i] = next_ri - cur_ri - sel_i * is_write * (write_val - cur_ri);
}

这个约束紧凑地处理所有寄存器更新情况。让我们解开它:

  • $register_selector(rd, i)$ 如果 $rd == i$(这个寄存器是目的寄存器)则为 1,否则为 0
  • $is_write$ 如果指令写入则为 1,否则为 0(NOP、HALT)
  • $write_val - cur_ri$ 是将会被应用的变化

表达式 $next_ri - cur_ri - sel_i \cdot is_write \cdot (write_val - cur_ri) = 0$ 意味着:

  • 如果这个寄存器是目的寄存器且指令写入: $sel_i = 1$, $is_write = 1$,所以 $next_ri = cur_ri + (write_val - cur_ri) = write_val$。寄存器获得新值。
  • 如果这个寄存器不是目的寄存器: $sel_i = 0$,所以 $next_ri = cur_ri$。寄存器被保留。
  • 如果指令不写入(NOP/HALT): $is_write = 0$,所以 $next_ri = cur_ri$。所有寄存器被保留。

一个表达式,没有分支,处理所有情况。

C6–C7,寄存器查找一致性:

// C6: rs1_val 必须等于索引 rs1 处的寄存器
let rs1_idx = current[4];
let mut rs1_expected = Fp::ZERO;
for i in 0..4 {
    rs1_expected = rs1_expected
        + register_selector(rs1_idx, i as u64) * current[7 + i];
}
let c6 = current[11] - rs1_expected;

// C7: rs2_val 必须等于索引 rs2 处的寄存器
let rs2_idx = current[5];
let mut rs2_expected = Fp::ZERO;
for i in 0..4 {
    rs2_expected = rs2_expected
        + register_selector(rs2_idx, i as u64) * current[7 + i];
}
let c7 = current[12] - rs2_expected;

从第 9 节回顾:AIR 不能做数组索引。这些约束验证 $rs1_val$ 和 $rs2_val$ 实际上匹配正确的寄存器。对于有效的寄存器索引,选择器 $register_selector(rs1_idx, i)$ 当 $rs1 == i$ 时为 1,所以和 $\sum sel(rs1, i) \cdot r_i$ 精确地挑选出索引为 $rs1$ 的寄存器值。约束检查 $rs1_val$ 等于这个和。

约束求值器

组合多项式

我们有 8 个约束,我们需要检查它们全部。而不是通过整个证明流水线单独处理它们,我们使用一个随机线性组合将它们组合成一个单一的组合多项式:

pub fn evaluate_composition(
    current: &[Fp; NUM_COLUMNS],
    next: &[Fp; NUM_COLUMNS],
    alpha: Fp,
) -> Fp {
    let constraints = evaluate_transition_constraints(current, next);
    let mut result = Fp::ZERO;
    let mut alpha_power = Fp::ONE;
    for c in &constraints {
        result = result + alpha_power * *c;
        alpha_power = alpha_power * alpha;
    }
    result
}

组合是 $C(x) = c_0 + \alpha\cdot c_1 + \alpha^2 \cdot c_2 + \cdots + \alpha^7 \cdot c_7$,其中 $\alpha$ 是从 Fiat-Shamir 转录本(第 10 节)导出的随机挑战。

为什么随机组合是安全的?如果任何单个约束 $c_i$ 在某个点非零,那么组合 $C$ 在那个点以压倒性概率非零,因为 $\alpha$ 是随机的,并且约束之间的偶然抵消可能性极小。因此,在 $\alpha$ 的选择上以压倒性概率,检查 $C(x) = 0$ 足以同时强制执行所有 8 个约束。

这减少了证明者的工作,从“证明 8 个多项式在迹域上为零”到“证明 1 个多项式在迹域上为零”。

约束次数分析

组合多项式的次数很重要,因为它决定了商多项式的次数,进而决定了证明者和验证者做多少工作。

操作码选择器的次数为 5(5 个线性项的乘积)。寄存器选择器的次数为 3。在寄存器更新约束(C2–C5)中,我们将一个寄存器选择器(次数 3)乘以 $is_write$(操作码选择器的和,次数 5)再乘以 $write_val$(其本身涉及操作码选择器乘以迹值)。得到的约束多项式具有高次数。

更具体地说,迹多项式的次数 $< n$(迹长度)。在这个玩具构造中,一个粗略的上界将组合次数置于大约 $12n$,而商 $Q(x) = C(x) / Z_H(x)$ 大约为 $11n$。这就是为什么 LDE 域需要比迹域大得多。我们在求值一个高次多项式,需要足够的点来安全地承诺它。


12. STARK 证明者和验证者

所有构建块都已就位:VM 产生迹,AIR 将 VM 规则编码为代数约束,证明工具箱(第 10 节)提供数学和密码学基础设施。证明者将所有东西组装成一个证明;验证者廉价地检查它。

证明者流水线

以下是证明者如何接收执行迹并生成紧凑证明的逐步过程:

1. 插值: 迹是一个数字表,但证明系统处理多项式。所以第一步是将 13 列中的每一列转换成一个通过该列所有值的多项式(使用第 10 节中的拉格朗日插值)。 对于我们的 8 行迹,每一列变成一个 7 次多项式。这一步之后,迹被完全编码为 13 个多项式。

2. 扩展: 在 LDE 域(比迹域多 8 倍的点)上求值那 13 个多项式。额外的求值完全由多项式决定,因此没有添加新信息。但它们给了验证者更多稍后可以抽查的点。

3. 承诺: 在 LDE 求值上构建一棵 Merkle 树。每个叶子打包一个 LDE 点上的所有 13 列值。Merkle 根,一个单一的 32 字节哈希,锁定了整个迹。这是证明的第一部分。

4. 挑战: 将程序(公共输入)和迹根输入 Fiat-Shamir 通道,然后挤出 $\alpha$,用于将 8 个约束组合成组合多项式的随机挑战(第 11 节)。 为什么吸收程序?因为 $\alpha$,以及每一个后续挑战,现在都依赖于声明的程序。如果我们跳过这个,一个证明者可以取程序 A 的有效证明,并将其重新标记为程序 B 的证明,因为挑战将是相同的。吸收程序防止了这种事后重新标记的技巧。 为什么吸收迹根?因为证明者必须在看到 $\alpha$ 之前承诺迹。如果 $\alpha$ 不依赖于迹承诺,证明者可以试图将迹定制为一个方便的挑战,而不是回答一个随机的挑战。 警告: 吸收程序将挑战绑定到声明的程序,但 AIR 中没有任何内容检查承诺的迹实际上匹配那个程序。一个恶意证明者仍然可以产生一个源自不同程序的迹,或直接伪造一个迹,并声明你的。第 14 节解释了这个差距。

5. 约束: 在每个 LDE 点求值组合多项式 $C(x) = \sum \alpha^i \cdot C_i(x)$,使用第 11 节的 AIR。每次求值使用来自两个相邻行(当前和下一个)的迹值来检查该点的所有 8 个约束。

6. 商: 在每个 LDE 点进行除法:$Q(x) = C(x) / Z_H(x)$。如果迹是有效的,$C(x)$ 在迹域的处处为零,所以这个除法是精确的,并且 $Q(x)$ 是一个有效的低次多项式。 如果迹是无效的,得到的商求值将无法通过低次测试。

7. 承诺商: 构建另一棵 Merkle 树,这次是在商求值上。将其根输入 Fiat-Shamir 通道。

8. FRI: 证明 $Q(x)$ 实际上是低次的,而不是无法对应任何低次多项式的求值数据。这是第 10 节中重复的折叠协议:每一轮将求值折叠成更小的表示,减少次数界限并将域大小减半,然后承诺结果并导出下一个挑战。

9. 打开查询: 从通道导出随机查询索引。在每个查询处,证明者揭示迹值、商值以及验证所有这些的 Merkle 证明。这些是验证者将检查的特定点。

证明对象

证明捆绑了验证者需要的所有东西:

pub struct StarkProof {
    pub trace_root: [u8; 32],         // 对迹 LDE 的承诺
    pub quotient_root: [u8; 32],      // 对商 LDE 的承诺
    pub fri_proof: FriProof,          // FRI 证明 Q(x) 是低次的
    pub query_responses: Vec&lt;QueryResponse>,  // 打开的值 + Merkle 证明
    pub query_indices: Vec&lt;usize>,    // 哪个 LDE 点被查询(为了方便;验证者会重新导出自己的)
    pub program: Vec&lt;Instruction>,    // 程序(公共输入)
    pub outputs: [Fp; 4],            // 声称的寄存器输出
    pub trace_length: usize,         // 填充后的迹长度
    pub real_trace_length: usize,    // 实际执行长度
}

两个 Merkle 根,一个 FRI 证明,以及少量打开的值及其认证路径。验证者接收这个证明并检查它,而从未看到完整的迹或完整的多项式求值。

验证者流水线

验证者从未看到迹。它只接收证明对象并检查它,而无需重新执行完整程序:

1. 重新导出挑战: 验证者重建证明者使用过的同一个 Fiat-Shamir 通道:它输入程序、迹根、商根以及 FRI 层根,在每个阶段挤出挑战。 因为双方以相同顺序哈希相同的数据,他们得到相同的随机挑战。这就是验证者如何在没有通信的情况下“重放”证明者的随机性。

2. 导出 FRI 挑战: 通过吸收每一层根并挤出折叠挑战(betas)来重放 FRI 承诺阶段。这将转录本推进到证明者在 FRI 承诺之后达到的相同状态。

3. 导出查询索引: 从通道中挤出查询索引。这些是验证者将检查的随机位置。因为它们是在所有承诺之后导出的,证明者无法预料它们。 至关重要地,验证者导出自己的查询索引,而不是信任证明中的那些。否则恶意证明者可以选择有利的查询点或完全省略查询。

4. 验证 FRI: 检查商多项式 $Q(x)$ 实际上是低次的。对于每个查询点,在每个折叠层打开 Merkle 证明,并检查每个折叠是否使用步骤 2 中的 betas 被正确计算。 如果 FRI 通过,验证者确信 $Q(x)$ 是一个真正的低次多项式。

5. 对于每个查询点:

  • 验证 Merkle 证明 用于迹值和商值。这确认了证明者使用的是它实际承诺的值,而不是在看到挑战后伪造的值。
  • 从打开的迹值重新求值组合多项式 $C(x)$ 使用 AIR(第 11 节)。验证者从零开始在这个单一点上计算,不信任证明者的任何东西。
  • 检查商方程: 在这个查询点是否 $C(z) = Q(z) \cdot Z_H(z)$?如果 $C(x)$ 确实在迹域上为零,并且 $Q(x)$ 是干净的商,这个方程成立。如果任何东西被篡改,它就会失败。

6. 边界约束: 作为教学上的简化,边界条件在多项式机制之外被检查。验证者确认程序以 HALT 结束,但它根本不验证 $proof.outputs$ 是否与承诺的迹匹配;声称的输出被信任。 在生产系统中,边界约束是在特定迹点(而不是所有相邻对)上求值的多项式方程,带有它们自己的消失项,并折叠到同一个组合多项式中。例如,“寄存器 r0 在最后一个真正行等于声称的输出”变成一个约束 $P_{r0}(\omega^k) - claimed_r0 = 0$,除以 $(x - \omega^k)$ 并与转换约束组合。这使得输出正确性与转换正确性成为同一个密码学保证的一部分。 我们的简化方法意味着恶意证明者可以声称任意输出,而验证者会接受它们。商检查不会捕获它,因为边界约束不参与组合,并且验证者从未在输出所存在的特定行打开迹。

验证者学到了什么

当验证通过时,验证者建立了一个保证链:

  • $Q(x)$ 是低次的 (FRI) $\rightarrow$ $C(x)$ 能被 $Z_H(x)$ 整除 $\rightarrow$ 约束在所有迹行成立
  • 打开的值是真实的 (Merkle 证明) $\rightarrow$ 证明者使用了它承诺的数据
  • 挑战不能被预料 (Fiat-Shamir) $\rightarrow$ 证明者不能操纵随机性

因此,一个承诺的迹满足所有转换约束。 验证者确信某个执行迹通过了 AIR 检查,而无需重新执行单条指令。但要注意在我们的简化系统中这没有证明什么:迹没有被限制为匹配声明的程序(没有程序一致性约束),声称的输出没有被验证是否与迹匹配(组合中没有边界约束),并且初始状态未被检查。第 14 节详细说明了每个差距。

非对称性

证明者执行的计算量要大得多:多项式插值(在我们的朴素实现中为 O($n^2$),使用 NTT 为 O($n \log n$))、多点求值、Merkle 树构建和 FRI 折叠。验证者检查少量 Merkle 证明(每个 O($\log n$) 个哈希)并在那些点求值约束方程。这种定性上的不对称随着程序长度增长而持续。一个有百万条指令的程序会产生更长的迹和更大的证明,但验证者的工作只缓慢增长,通常是对数或亚对数级别的迹长度。

这种证明者-验证者不对称性是使 STARKs 有用的核心性质。


13. 运行完整演示

每个模块都已构建。让我们把它们放在一起,观察整个流水线从程序定义到验证证明的运行。main.rs 中的演示很短,但它演练了我们讨论的每个阶段。

程序

与第 9 节相同的程序,用六条指令计算 $(3 + 4)^2 - (3 + 4) = 42$。结果(寄存器 $r0$ 中的 42)是证明者将声称的输出。如第 14 节所讨论的,验证者不会独立验证这些声称的输出是否与承诺的迹匹配。

执行并生成迹

let mut trace = vm::execute(&program);
trace.pad_to_power_of_two();

VM 产生第 9 节中的 6 行迹,然后填充将其扩展到 8 行(下一个 2 的幂),使用冻结寄存器状态的 NOP 指令。两个填充行(行 6–7)有 $opcode=NOP$,PC 冻结在 5,所有寄存器保持它们的最终值,时钟仍然递增(如约束系统所要求的)。

约束验证(直接)

在生成证明之前,演示直接验证约束,作为一个健全性检查,确保我们的迹是有效的:

match air::verify_trace_constraints(&trace.rows) {
    Ok(()) => println!("  所有转换约束已满足!"),
    Err((row, constraint)) => {
        println!("  行 {} 处约束违反,约束编号 {}", row, constraint);
        return;
    }
}

这个函数遍历每对相邻行并求值所有 8 个转换约束。如果任何约束在任何行返回非零值,执行停止。这是“诚实”的检查方式:直接求值所有东西,不涉及密码学。它是 O($n$) 的,需要完整的迹。STARK 证明的存在是为了用一个验证者无需迹即可检查的东西来替换这个。

证明生成与验证

let proof = prover::prove(&trace, &program);

这一行代码触发了第 12 节中整个证明者流水线:插值 13 列,在 LDE 域上求值,通过 Merkle 树承诺,导出挑战,求值约束,计算商,运行 FRI,并打开查询点。

match verifier::verify(&proof) {
    Ok(()) => {
        println!("  *** 证明已验证 ***");
        println!("  验证者确信:");
        println!("    - 一个有效程序被正确执行");
        println!("    - 执行迹满足所有 {} 个转换约束",
            air::NUM_CONSTRAINTS);
        println!("    - 商多项式是低次的(FRI 已验证)");
        println!("    - 输出: r0={}, r1={}, r2={}, r3={}",
            proof.outputs[0], proof.outputs[1], proof.outputs[2], proof.outputs[3]);
    }
    Err(e) => {
        println!("  证明被拒绝: {}", e);
    }
}

打印的摘要夸大了证明实际保证的内容。转换约束和 FRI 检查是密码学验证的,但声称的程序和输出并未对照承诺的迹进行检查。验证者确认声明的程序以 HALT 结束并打印 $proof.outputs$,但两者都基于信任。请参阅第 14 节以获取简化列表。

在从未看到完整迹的情况下,验证者重新导出 Fiat-Shamir 挑战,验证 FRI,检查每个查询点的 Merkle 证明和商方程,并检查声明的程序以 HALT 结束。当输出显示 *** PROOF VERIFIED *** 时,每个检查都已通过。

在这个玩具参数化中,验证者被密码学方式说服,具有大约 90 位的可靠性,认为某个有效执行迹满足所有转换约束,并且与一个低次商多项式一致。声明的程序被吸收到 Fiat-Shamir 挑战中,声称的输出被携带在证明中并由验证者打印,但两者都没有独立地对照承诺的迹进行检查(有关这对可靠性意味着什么的详细信息,请参阅第 14 节)。


14. 这个 ZKVM 省略了什么

我们已经在大约 2,500 行 Rust 代码中构建了一个完整的流水线(执行、迹、算术化、证明、验证)。这个流水线是完整的,并产生有效的证明。但它省略了许多使生产级 ZKVMs 更加复杂的功能。理解这些差距与理解流水线本身同样重要,因为它们定义了真正的工程挑战所在。

没有内存。 我们的 VM 有 4 个寄存器,没有别的。真正的程序需要 RAM:数组、栈、堆。在 ZKVM 中,内存很难,因为迹记录顺序执行,但内存访问可以是随机的(任何地址,任何时间)。你不能仅仅添加一个“内存”列并逐行约束它,因为对地址 1000 的存储可能在周期 5 发生,而在周期 500,000 才被读取。生产系统使用内存检查论证来处理:它们按地址对内存访问进行排序,并使用置换论证或查找表(如 LogUpPlookup)检查一致性。这增加了主要的辅助子系统的约束和迹列,并且是真实 ZKVMs 中复杂性的主要来源之一。

没有零知识。 我们的证明不是零知识的:它通过打开的求值揭示迹信息。通过 Merkle 树承诺并在查询点打开的 LDE 值暴露了实际的迹数据。一个验证者(或任何看到证明的人)可以学习寄存器值、操作码和中间状态。生产级 STARKs 添加掩蔽多项式,添加到迹多项式的随机低次多项式,以随机化求值而不影响约束满足。这就是将“ZK”放在 ZKVM 中的东西。我们跳过了它,因为它与理解证明流水线是正交的。

边界约束没有被折叠进组合。 我们的验证者只执行一个最小的边界检查:它确认声明的程序以 HALT 结束。它验证 $proof.outputs$ 是否与 HALT 行处的承诺迹匹配。声称的输出基于信任。在真实系统中,边界约束是在特定迹点(而不是所有相邻对)上求值的多项式方程,带有它们自己的消失项,并折叠到同一个组合多项式中。例如,“寄存器 r0 在最后一个真正行等于声称的输出”变成一个约束 $P_{r0}(\omega^k) - claimed_r0 = 0$,除以 $(x - \omega^k)$ 并与转换约束组合。这使得它们成为同一个密码学保证的一部分。我们的简化方法意味着恶意证明者可以声称任意输出。

没有对迹列的范围约束。 第 11 节中的选择器多项式假设 $opcode \in {0,1,2,3,4,5}$ 且 $rd, rs1, rs2 \in {0,1,2,3}$。但 AIR 中没有约束强制执行这些范围。在 ${0,1,2,3,4,5}$ 上的拉格朗日基多项式在恰好一个点求值为 1,在其他点求值为 0,但仅限于该集合内。给它一个集合外的值(比如 $opcode = 6$),每个选择器都会返回一个非零值。约束变成所有操作的加权混合,而不是与单个指令的干净匹配。在我们的系统中,Instruction 构建器上的 Rust 级别 assert! 守卫在诚实执行期间防止了这种情况,但它们不是代数约束。直接构造迹的恶意证明者可以绕过它们。修复方法是直截了当的:添加消失多项式约束,如 $opcode \cdot (opcode - 1) \cdot (opcode - 2) \cdot (opcode - 3) \cdot (opcode - 4) \cdot (opcode - 5) = 0$ 和 $rd \cdot (rd - 1) \cdot (rd - 2) \cdot (rd - 3) = 0$(对 $rs1$、$rs2$ 类似)。当值在有效集合内时,这些恰好为零,否则非零。我们将约束数保持在 8 个而省略了它们,但任何生产系统都需要它们。

没有程序一致性约束。 证明将程序作为公共输入包含,并将其吸收到 Fiat-Shamir 转录本中,这将所有挑战绑定到声明的程序,并防止证明在事后被重新标记。但 AIR 从不约束迹的指令列($opcode$、$rd$、$rs1$、$rs2$、$imm$)以匹配从该公共程序在当前 PC 处取出的指令。在生产级 ZKVM 中,这是通过一个程序内存表强制执行的:证明者将程序承诺为一个映射 $(pc \rightarrow opcode, rd, rs1, rs2, imm)$ 的查找表,并且一个跨表查找参数(例如 LogUp)约束每个迹行从该表中取出其指令。没有这个,验证者实际上并没有证明“这个确切的公共程序被执行了”,而只是证明某个承诺的迹在从声明的程序导出的挑战下满足了转换约束。一个恶意证明者可以从程序 A 生成一个有效迹,声明程序 B,而验证者会接受它。

没有初始状态约束。 VM 以 $pc = 0$ 和所有寄存器为零开始执行,但验证者从不检查承诺的迹是否从该状态开始。像输出声明一样,初始状态是一个需要被折叠到组合多项式中的边界条件(例如 $P_{r0}(\omega^0) - 0 = 0$,除以 $(x - \omega^0)$),或通过第一个迹行的专用 Merkle 打开来验证。如果没有这两种机制,恶意证明者可以从任意寄存器值开始迹,而验证者不会检测到。

没有递归或聚合。 生产级 ZKVMs 通常需要证明非常长的计算,数百万或数十亿个周期。单次 STARK 证明会是巨大的。解决方案是递归证明:将执行分成多个段,分别证明每个段,然后证明段证明是有效的。验证者本身成为一个在 ZKVM 内运行的程序,生成一个“证明的证明”。这种技术(被 RISC Zero、SP1 和其他系统使用)将非常长的计算压缩成更简洁的证明。它要求 ZKVM 能够有效地验证自己的证明,这是一个重大的工程挑战。

朴素的多项式算术。 我们的拉格朗日插值是 O($n^2$) 的。对于 $n$ 个基多项式中的每一个,我们做 O($n$) 的工作。我们的多项式乘法也是 O($n^2$) 的。生产系统使用数论变换 (NTT),FFT 的有限域类比,以 O($n \log n$) 的时间进行插值和乘法。对于 $2^{20}$ 行(约 100 万)的迹,这相当于 $\sim 10^{12}$ 次操作和 $\sim 2 \times 10^7$ 次操作之间的差异。NTT 是为什么生产级证明者足够快到实用的原因,也是为什么 Goldilocks 素数的大 2 的幂子群很重要的原因。这里使用的基 2 NTT 需要一个 2 的幂乘法子群。

6 条指令 vs 数百条。 我们的 ISA 没有分支、跳转、内存加载/存储、比较操作、函数调用。真正的 RISC-V 有 47 条基本指令 (RV32I) 加上乘法、原子操作等的扩展。每条额外的指令意味着更多的选择器多项式、更多的约束情况以及更高的约束次数。一个完整的 RISC-V ZKVM,如 RISC Zero 或 SP1,有数千个约束,跨越数十种约束类型,组织成多个通过跨表查找参数交互的 AIR 表。仅约束工程本身就是一个专家团队多年的努力。

上述每一个省略都代表了生产系统中的大量工作。但流水线(执行、迹、算术化、证明、验证)是相同的。六指令版本和生产级 RISC-V 系统遵循相同的高层流水线。差异在于规模、优化和工程深度,而不是架构。

15. 结论

我们已经走过了使 ZKVM 模式工作的流水线的每个阶段。证明机器一次,任何编译到其 ISA 的程序都自动是可证明的:

  • ISA(第 8 节)定义了机器能做什么:6 个操作码、4 个寄存器、统一的指令格式。
  • VM(第 9 节)执行程序并记录执行迹,一个在每一步包含机器状态的完整表格。
  • 证明工具箱(第 10 节)提供了数学底层:有限域、多项式、求值域、Merkle 承诺、Fiat-Shamir 挑战和 FRI。
  • AIR(第 11 节)将 VM 的规则翻译成代数。选择器多项式取代了分支;8 个转换约束编码了整个 ISA。这就是 ZKVM 特定工程存在的地方。
  • 证明者和验证者(第 12 节)组装流水线:插值、求值、承诺、组合、除法、证明;然后使用少量 Merkle 证明和每个查询一个方程来验证。

这是用于生产级基于 STARK 的 ZKVMs 的相同概念流水线:SP1、ZisK、Ceno、Pico、ZKsync Airbender 以及其他在 ethproofs.org/zkvms 上追踪的系统。差异在于 ISA(RISC-V rv32/rv64 vs. Cairo vs. MIPS vs. 自定义)、规模(数百万个约束 vs. 我们的 8 个)以及优化(NTT、递归、GPU 加速)。但底层概念架构(执行、迹、算术化、证明、验证)是相同的。

这两个层(ZKVM 特定的 AIR 和通用证明基础设施(域、多项式、FRI、Merkle 树))之间的边界,是区分“知道 STARKs 如何工作”和“理解如何构建 ZKVM”的东西。

以太坊的 L1 正积极朝这个方向前进。通过 Ethproofs 倡议,协议正致力于让验证者通过简洁证明来验证区块,而不是重新执行每笔交易。该方法遵循相同的模式:EVM 验证逻辑编译为通用 RISC-V ZKVM 内的客程序。构建 ZKVM 证明者的团队,包括 SP1 和其他由 Ethproofs 追踪的团队,正在推动实时以太坊区块证明。你刚刚构建的流水线(执行、迹、算术化、证明、验证)正是这些团队正在将其扩展到生产环境的同一流水线。

代码 可供直接运行、修改和实验。更改程序并观察迹的变化。添加一个新的操作码,看看它需要什么约束。破坏一个约束,观察证明失败。理解证明系统的最佳方式就是构建一个,而现在你已经有了。


资源

学习

生产级 ZKVMs(参见 ethproofs.org/zkvms 获取实时数据)

以太坊 L1 集成

论文

  • 原文链接: cyfrin.io/blog/making-se...
  • 登链社区 AI 助手,为大家转译优秀英文文章,如有翻译不通的地方,还请包涵~

相关文章

0 条评论