STARK证明器对比：Miden和Starknet

介绍

STARKs（可扩展的透明知识论证）由于其帮助扩展以太坊的能力而受到广泛关注。它们允许一方，即证明者，通过提交可以比验证者进行朴素重新执行更快验证的证明，向验证者证明给定的程序执行是正确的。证明大小也更小，数量级为 $O(\log_2(n))$，其中 $n$ 是计算中的步骤数。Starknet 和 Polygon Miden 在其协议中使用 STARKs 来生成这些证明，使用它们自定义的版本。Starknet 使用 Stone Prover，而 Miden 使用 Winterfell。我们的证明器，lambdaworks 中的 STARK Platinum，是一个通用的证明器，我们希望用作任何这些证明器的直接替代品。 如果你想了解 STARKs 的工作原理，你可以看看我们之前关于 STARKs、Stone 证明器 和 FRI 的文章。

一般步骤

简而言之，STARKs 使用执行轨迹（一个包含计算期间寄存器值的大型表）和一个代数中间表示 (AIR) 来表示计算，AIR 是一组应该在轨迹上强制执行的多项式约束。通过利用预处理阶段并从验证者那里获取随机性，STARKs 得到了改进，从而将 AIR 变成了具有预处理的随机 AIR。这样，我们可以使用对内存检查或与协处理器通信有用的附加变量来扩展轨迹。主要步骤是：

1. 插值轨迹列以获得轨迹多项式。
2. 通过在更大的域（低度扩展）上进行评估并将这些评估用作 Merkle 树中的叶子来提交轨迹多项式。
3. 可选：从验证者那里采样随机性并将轨迹扩展到辅助轨迹。插值辅助轨迹列并按照步骤 2 中的策略提交给这些多项式。
4. 从验证者那里采样随机性并使用 AIR 约束和整个轨迹来计算组合多项式。提交给组合多项式。
5. 从验证者那里获取域外点 $z$，在 $z$ 处评估轨迹多项式和组合多项式，并将它们发送给验证者。
6. 构建 DEEP 组合多项式，这将让我们检查点 5 中多项式的评估是否正确。
7. 将 FRI 协议应用于 DEEP 组合多项式并获得证明。

检查约束

我们检查约束的方式如下：让我们将轨迹的行表示为 $x_0, x_1, ... xN$。轨迹的一个元素只是 $x{ij}$，它是一个域元素。AIR 约束是某个多元多项式 $P(u,v,w)$，其中 $u$、$v$ 和 $w$ 可以是来自不同行或列的元素。每个约束也有一个有效范围。以下是一些约束的示例：

• 简单的边界约束：这些约束强制轨迹中的给定位置 $x_{ij}$ 具有规定的值。例如，我们希望第 0 行中的寄存器 $2$ 等于 $5$。约束多项式将是 $P(x) = x_2 - 5$。如果该轨迹有效，当我们把 $x_0$ 插入到 $P$ 中，我们将有 $x_0^2 - 5 = 0$。如果我们使用其他行，则多项式不一定会计算为 $0$。
• 一致性约束：这些约束强制某些寄存器的值满足给定的条件。例如，如果我们希望寄存器 $4$ 是一个布尔变量，我们需要对于所有 $k$， $x{k4}(1 - x{k4}) = 0$。因此，约束多项式是 $P(x) = x_4(1 - x_4)$，这应该适用于所有行。
• 简单的转换约束：表明一行中寄存器的值与前一行中的值兼容，这由计算决定 。例如，如果我们有一个序列 $x{0,n+1} = x{0,n}^2 + x{1n}$，约束多项式是 $P(x{k+1}, xk) = x{0,k+1} - x{0,k}^2 - x{1,k}$。这些约束适用于所有计算，除了最后一行。
• 更复杂的约束：这些约束可能涉及更多行，或者仅在特定点应用，这使得它们的描述更加复杂。

为了强制执行约束，我们需要将轨迹多项式（通过将轨迹解释为对某个集合 $D$ 上多项式的评估获得）与约束多项式组合，从而获得与我们拥有的约束一样多的 $C_i(x)$，并将每个 $C_i(x)$ 除以它们对应的零化器 $Z_i(x)$，这是一个在约束被强制执行的地方为 $0$ 的多项式。一些零化器是：

• 简单的边界约束：$Z(x) = x - g^k$，其中 $g$ 跨越域 $D$ ($D = g^0, g, g^2 ... g^{n-1}$)。
• 一致性约束：$Z(x) = x^n - 1$。
• 简单的转换约束：$Z(x) = (x^n - 1) / (x - g^{n-1})$

STARK 证明器的效率部分取决于能够以快速的方式计算这些零化器。如果一个约束要应用于步骤 $1, 3, 4, 6, 7, 9, 12, 14, ... n-1$，而没有清晰的模式，我们将不得不花费几乎线性的时间来尝试评估该多项式。如果想要拥有最简单的证明器，最好使用最多涉及两个连续行的约束，并且是边界约束、一致性约束或简单的转换约束。这有助于我们减少需要计算的零化器的数量和乘法的数量。

就性能和可用性而言，我们使用的 AIR 以及我们如何组织轨迹非常重要。AIR 中高度的约束将使组合多项式的评估更加昂贵。另一方面，对轨迹的严格组织（轨迹布局）增加了证明通用程序的开销，并且难以对证明器进行更改。Miden 一直在开发 AIRScript，旨在使 AIR 描述和评估简单且高性能。在 Lambdaworks 中，我们也在努力简化 AIR 的定义和约束的评估，从而实现更快的证明器和更容易的维护或更新。

不同的代数中间表示

Miden vm 的 AIR 包含在这里。Stone prover 的 AIR 取决于布局的类型；AIR 的一般性描述在这里。这是 Starknet 中不同布局的列表：

• Plain
• Small
• Dex
• Recursive
• Starknet
• StarknetWithKeccak
• RecursiveLargeOutput
• AllCairo
• AllSolidity
• Dynamic

在这里，我们展示了 Starknet 中普通布局的主轨迹的单个步骤的图，没有辅助轨迹（更多信息，请参见我们的分析）：

Stone Prover 将多个寄存器打包到单个列中，从而创建虚拟列。例如，所有 16 个标志都分组在一个列下。内存的地址和值也以交错的方式分组在另一列中。这减少了轨迹中的列数（我们将 $16$ 列合并为 $1$ 列），但轨迹长度变为原来的 $16$ 倍。当我们想要找到轨迹多项式时，我们执行大小为 $16n$ 的一个快速傅里叶变换 (FFT)，而不是大小为 $n$ 的 $16$ 个 FFT。

如果某些寄存器仅更新几次，那么使用虚拟列可能很有用，因为我们仍然必须将它们填充到完整长度，从而减少轨迹中的内存使用。但是，这有一个很大的缺点：我们必须保留不同的零化器，并且（我们用来有效计算约束的）评估帧变得更加复杂。让我们看看这两种方法之间的区别：

16 列

为了评估每个约束，我们只需要获取一行的元素。轨迹长度为 $n$，因此零化器为 $Z(x) = x^n - 1$。15 个标志具有约束 $x(1 - x) = 0$，而最后一个标志具有 $x = 0$。

单个虚拟列

为了评估每个约束，我们只需要从行中取一个元素。问题在于约束 $x(1 - x)$ 对所有行都有效，除了每第 $16$ 行，而约束 $x = 0$ 仅对每第 $16$ 行有效。这样，我们必须维护两个零化器，每个约束一个：

• $Z(x) = (x^{16n} - 1) / (x^n - g^{15n/16})$
• $Z(x) = x^n - g^{15n/16}$

另一个问题是，如果一个约束涉及多个标志，我们需要传递多行才能评估它。值得注意的是，在这种情况下，$g$ 与前一种情况不同，因为插值现在发生在大小为 $16n$ 的域上。

内置组件和微芯片

拥有用于证明的通用 CPU 会带来成本：虚拟机并未针对某些常用操作进行优化。为了解决这个问题，Cairo vm (Starknet) 和 Miden vm 引入了协处理器来处理这些操作，然后将结果传递给 CPU。

微芯片和 Miden vm

Miden 使用专用组件来加速复杂计算，称为微芯片。每个微芯片处理一个独特的计算，并负责证明计算的正确性及其内部一致性。目前受支持的微芯片有：

• Hash
• Bitwise
• Memory
• Kernel ROM
• Range checker（它作为微芯片工作，但被单独处理）

微芯片的执行轨迹是通过堆叠每个微芯片的执行轨迹来构建的。这是一种优化，因为每个微芯片可能比 vm 的其他组件生成更少的单元格，从而避免了将它们填充到相同长度的显着填充，并减少了列数。它使用与 Stone 中的虚拟列类似的推理，但它不会交错它们。

微芯片由选择器标识。约束的总度数在 $5$ 到 $9$ 之间，每个微芯片占用 $6$ 到 $17$ 列。选择器为：

• $1$：hash
• $1, 0$：bitwise
• $1, 1, 0$：Memory
• $1, 1, 1, 0$：Kernel ROM
• $1, 1, 1, 1$：padding

但是，堆叠微芯片的轨迹存在一些困难，因为一个微芯片的最后一行的 一致性和转换约束可能会与下一个微芯片的第一行冲突。内存和内核 ROM 微芯片就是这种情况，选择器标志可以解决冲突。

微芯片使用总线连接到 VM 的其余部分，总线可以将请求发送到任何微芯片并接收响应。它被实现为一个运行产品列，如果请求和响应匹配，总线将以 $1$ 开始和结束。

这种方法的主要缺点之一是约束具有相当大的度数，这使得约束评估更加昂贵。另一方面，该构造不需要处理多个零化器，并且看起来更易于实现和理解。

内置组件和 Cairo vm

内置组件是特定于应用程序的 AIR，可以减少给定计算的执行轨迹的大小。例如，使用 Cairo 表达 Poseidon 哈希函数需要在轨迹中使用 35k 个单元格，而 Poseidon 内置组件将其减少到大约 600-650 个单元格。在内置组件中，我们有：

• Poseidon
• Pedersen
• Elliptic curve operation
• Keccak
• Bitwise
• ECDSA
• Range check

但是，内置组件的集成需要一些谨慎，因为简单的方法可能会导致浪费单元格，从而降低构造的效率。布局指定分配给每个组件的单元格和位置的数量。根据我们要证明的程序的类型，我们可以从 Starknet 中提供的不同布局中进行选择，以实现最具成本效益的解决方案。但是，正如对 动态布局的讨论中所指出的那样，现有布局可能会为证明我们的程序带来显着的开销。添加新布局需要专家知识和仔细分析；对于需要理解布局之间差异的用户来说，它也可能令人困惑。

每个内置组件都有一个内存段。为了检查内存段中是否存在溢出，有两个指针（开始和停止）通过公共内存机制导出。由于每个内置组件的约束每隔几行应用一次，因此我们被迫计算不同的零化器并处理更复杂的求值帧。

结论

在这篇文章中，我们讨论了 STARK 证明器的特性和一些实现权衡。我们分析了 Miden 和 Cairo VM 如何处理它们的执行轨迹以及 AIR 的描述。我们还讨论了约束的主要类型以及在执行轨迹上强制执行它们的方式。使用虚拟列（将多个寄存器分组在一列中）减少了我们必须执行的 FFT 的数量，但代价是 需要更复杂的评估帧和保留多个零化器。但是，当多个组件的轨迹单元较少且需要填充时，此策略是必需的。Miden 在处理微芯片时使用这种类型的策略，但它选择堆叠轨迹而不是交错它们。这引入了几个选择器变量，这增加了约束的度数，从而为约束评估增加了额外的成本。另一方面，评估帧更简单，我们不必计算多个零化器。使用布局可能会带来更具成本效益的解决方案，尽管代价是证明某些类型的程序需要更大的开销。此外，添加更多布局会增加复杂性并使事情更难维护。我们喜欢分析不同的解决方案及其权衡，因为它们可以带来新的设计，从而帮助我们改进通用证明器。

• 原文链接： blog.lambdaclass.com/com...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～