# GKR 引擎

> 远地虚拟机核心的证明引擎。为什么分层 GKR 电路只承诺它的输入，一次由求和校验构成的反向过程如何把整个电路汇聚到单个点上，以及这带来了什么。

远地虚拟机中的每个分片都以同一种方式证明：使用其电路族的电路，这个电路写成一摞层，由 GKR 引擎从电路的输出反向运行到其已承诺列。本页讨论为什么这个引擎位于系统的核心，以及为什么它所属的这一类证明系统，正是证明技术前沿推进的方向。

## 基本思想

证明一项计算的经典做法，是把它排成一张表，承诺每一列（包括中间值），再证明一组约束在整张表上为零。承诺是其中昂贵的部分：每个被承诺的列都要花费一次多标量乘法或一棵 Merkle 树，还要在约束论证问到的每个点上做一次打开。

GKR（得名于 Goldwasser、Kalai 和 Rothblum）改变了必须承诺的内容。计算被表示为一个**分层电路**。只有最底层，也就是输入，才被承诺。其上的每一层都由作用于下一层的门定义，证明者从不承诺它。取而代之的是：关于顶层的断言，经一次求和校验（sumcheck）归约为关于其下一层的断言，再归约到更下一层，直到这些断言全部落在已承诺的输入上，并且都位于同一个随机点。一次打开就能了结它们。

> [!NOTE]
> **这是类比，不是名称。** 传统的证明者像一枚火箭：它把自己产生的每一个中间值都承诺下来、运到目的地，并为这些质量付出代价。GKR 引擎的行为更像科幻作品中的曲速引擎：移动的是飞船周围的空间，而不是飞船本身。真正被运送的是*断言*，它沿着电路一层一层向下移动，而中间层根本不会被运到任何地方。

这给 zkVM 带来的好处：

- **中间值不花费任何承诺。** 电路族的电路可以计算数百个内部列、乘积树和分式树，它们无一被承诺。被承诺的只有执行轨迹列。
- **每个分片一个打开点。** 反向过程结束时，每个已承诺列都在同一个点上有一个断言。无论有多少列，一个分片都恰好只需一次批量打开，704 字节。
- **证明者的工作是域运算。** 每一层的求和校验在 `Fr` 上进行，耗时与该层的大小成线性关系，每层都不需要承诺、变换或哈希。
- **论证在电路内部组合。** 内存论证的大乘积和查找（lookup）的 LogUp 求和，只是同一个电路中更多的层，在同一个过程中归约。

## 电路族的电路，逐层来看

> Figure: 一个电路族的电路。证明者自下而上把每一层计算一次（虚线）。证明则自上而下进行：先吸收输出，然后每次层间转换都是一次求和校验，把关于某一层的断言变成关于其下一层的断言，直到所有断言在已承诺列上汇聚于同一点。

最底层是分片的已承诺列，分为三种，区别在于何时被绑定：**`M`**，内存列，在任何内存挑战产生之前于陈述的全局 transcript 中承诺；**`W`**，见证列，在分片自己的 transcript 中承诺；**`S`**，设置列，由程序身份或仪式绑定。它们旁边是**虚拟表**：诸如行索引或 16 位范围这样的闭式表达式，验证者可以在任意点上对其求值，它们从不被承诺。

在第 0 层之上，每个电路族的电路都有相同的结构：

1. **门列表 0** 逐行计算内存叶子（每个查询的读元组和写元组）、查找分式（每个查找一个 `(numerator, denominator)` 对，另加表本身的一对），以及每个**约束门**：电路族的约束，每一个都是必须在每一行上为零的多项式。
2. **逐行列表**合并兄弟叶子：乘积树把元组相乘，分式树按 `(n_a·d_b + n_b·d_a, d_a·d_b)` 把分式相加，直到每一行的每棵树只剩一个节点。
3. **折半列表**按分片高度的每个变量各有一个，把各行两两合并：前一半与后一半。经过 `n` 个折半列表后，电路到达一个没有变量的顶层：分片的读根、写根，以及每个查找通道最终的分子和分母。

所以一个电路在一个过程中同时证明电路族的约束、计算它对内存论证的贡献，并对它的查找求和。每个门的次数至多为 2，所以每次求和校验的每个轮多项式都是三次多项式。

## 反向过程

证明者自下而上把每一层物化一次。随后证明自上而下进行，它的 transcript 时序对每个电路都相同：

1. **输出首先被吸收**，这样在任何挑战产生之前，证明者就已被这些根绑定。
2. 对于从第 `k + 1` 层到第 `k` 层的每次转换，一个挑战 `λ` 把第 `k + 1` 层上的每个断言，连同该列表的每个约束门，批量合成一个和。一次**求和校验**把这个和归约为在随机点 `ρ` 上的一个求值，每个变量一条三次多项式消息。
3. 证明者给出第 `k` 层各列在 `ρ` 上的值。对于折半列表，它给出两个子节点的值，再由另一个挑战 `τ` 把它们合并为每列一个断言。
4. 到第 0 层时，每个已承诺列都有一个断言，全部位于同一点 `u`。

分片唯一的那次 Mercury 打开，对照各承诺证明这些断言：内存列的承诺取自陈述，见证列的取自分片证明，设置列的取自验证密钥。虚拟表由验证者自己求值。

约束门可以免费搭车。约束门断言自己处处为 0，所以它加入其所在转换的批次；一旦某个门被违反，批量和以压倒性的概率不为零。一个 `LayerInconsistency` 错误同时涵盖错误的下行断言和被违反的门：批量和无法区分二者，证明也不为区分它们花费任何代价。

## 为什么它是可靠的

每个挑战都在它所保护的一切之后抽取：

- 输出点在输出之后抽取，所以证明者无法挑选只在将被检查之处与真实值一致的表；
- `λ` 在断言和点之后抽取，所以虚假的断言或被违反的门，只有当 `λ` 恰为某个非零多项式的根时才能幸存；
- 每个求和校验挑战在其所在轮的三次多项式之后抽取，所以错误的三次多项式与真实的三次多项式一致的概率至多为 `3/|Fr|`；
- `τ` 在两个子节点的值之后抽取。

对注册表中任一电路在其默认高度下的全部转换求和，可靠性误差保持在 `2^14/|Fr|` 以下；这里 Fiat–Shamir 基于 Poseidon2 transcript，并在随机预言机模型中分析。

## 以数据表示的电路

电路不是代码，而是一个 `CircuitArtifact`：按名称列出的已承诺列、虚拟表、使用七种门形状的门列表、同一组关系的扁平列表、查找以及填充行，以规范形式序列化。四条法则让每个制品都保持一致的形式：每个操作数在被读取之处都可读；每个列表的宽度由其门推导而来；顶层恰好就是输出；分层的门与扁平关系是同一个约束集。这些法则只在构建制品或加载密钥时运行一次，从不针对每个证明运行。

对任何评估这个系统的人来说，有两点后果值得关注：

- **验证密钥携带自己的电路，验证者要求它们与自己的注册表一致。** 程序身份绑定程序；注册表绑定证明该程序的电路。
- **电路可以由第二套实现检查。** `checker` crate 在不共享构造器代码的前提下，重新实现了各项法则、查找规则和填充约定，并且只通过双方都视为语义权威的那一个门内核对门求值。

## 代价

这个引擎用内存换掉了承诺。前向过程以域元素的形式持有每一个内部层：最宽的指令电路族的一个 `2^20` 分片约占 8.4 GiB，一个 `2^18` 的 `KECCAK_F` 分片占 42 GiB，其电路要计算 5,490 个内部列。这就是证明受内存限制的原因，也是高度成为调优参数、[流式证明者](https://apogee.gweb3networks.com/docs/architecture/streaming)以同时处理中的分片为内存上界的原因。证明大小只会随每层每个变量增加一轮求和校验而增长：一个 `KECCAK_F` 分片的证明在 `2^18` 时为 381,100 字节，在 `2^16` 时为 373,276 字节，而前者的工作量是后者的四倍。

规范见 [GKR 引擎](https://apogee.gweb3networks.com/docs/auditors/spec/gkr)，以及[审计专区](https://apogee.gweb3networks.com/docs/auditors)下每个电路族各自的页面。