递归 STARK 证明

首个通用计算递归证明上线以太坊主网

原文:Recursive STARKs
作者:StarkWare 核心工程师 Gidi Kaempfer
翻译:「StarkNet 中文」社区

概要

  • 递归证明上线主网,用一个证明来扩展 StarkEx 应用程序和 StarkNet
  • 递归证明提升扩展性,降低成本和延迟(鲜有的扩展性和延迟同步发展,而没有取舍)
  • 递归证明为 L3 和其他妙用创造了条件
  • 来看看递归证明的博文吧,超酷的 😉

倍数扩展!

由 Cairo 通用计算提供支持的递归证明现已投入生产。这标志着 STARK 对 L2 扩展能力的重大提升。单一证明写入以太坊的交易数量可快速成倍增加。

迄今为止,STARK 证明通过将数万甚至数十万个交易「汇总」成单一证明写入以太坊来实现扩展。通过递归,许多这样的证明可以「汇总」成一个单一证明。

这种方法现已应用于众多基于 Cairo 的应用程序:在 StarkWare 的 SaaS 扩展引擎 StarkEx 和无需许可的 Rollup StarkNet 上运行的应用程序 。

迄今发展历程

自 2020 年 3 月主网上线首个证明产生以来,STARK 证明至今经历了不同发展阶段。

STARK 扩展

2020 年 6 月,第一个 STARK 扩展解决方案 StarkEx 在以太坊主网部署。StarkEx 有一个证明器可以在链下执行大型计算,生成一个 STARK 证明表示交易准确性,还有一个验证器在链上验证证明的准确性。第一次部署由 StarkWare 工程师从零开始亲自操刀,因此 StarkEx 的功能极大受限。最终我们决定,需要一种支持证明通用计算的编程语言。这样,Cairo 便应运而生。

Cairo 编程语言

2020 年夏天,Cairo 首次亮相以太坊主网。Cairo 即 CPU 代数中间代码 (CPU Algebraic Intermediate Representation [AIR]),内含一个用于验证相应「CPU」指令集的单一 AIR。Cairo 为更复杂的业务逻辑、任意可计算命题 (computational statements) 打开了编码证明的大门,而且更快、更安全。一个 Cairo 程序可以证明相应应用程序的执行逻辑。但一个 Cairo 程序也可以集合多个此类应用程序,这就是 SHARP。

SHARP

SHARP 即共享证明器 (SHARed Prover),可以聚合几个独立应用程序的交易,并在一个单一的 STARK 证明中证明。应用程序可以组合不同批量交易,更快填满 STARK 证明的容量。交易处理速度和延迟都有所提高。递归证明是下一代前沿技术,不仅适用于一些硬编码逻辑,而且适用于通用计算

要了解递归证明的全部优势,有必要进一步了解 SHARP 迄今为止是如何执行(非递归)证明的。图 1 描绘了一个典型的非递归流程:

图 1:典型非递归证明流程
图 1:典型非递归证明流程

在这个流程中,命题逐渐到达。容量(或时间)达到一定阈值时,会生成一个大型组合命题 (Train)。只有在收到所有单独命题后,才能证明此组合命题。此证明需要很长时间(大约是单独证明每个命题所需的时间总和)。

证明极其庞大的命题最终会受到内存等可用计算资源的限制。在递归之前,这实际上是限制 STARK 证明可扩展性的一大障碍。

什么是递归证明?

通过 STARK 证明,证实命题所花费的时间与执行命题所花费的时间大致呈线性关系。此外,如果证明一个命题需要的时间为 T,那么验证证明所需要的时间大约为 log(T) ,这通常被称为「对数压缩」。换句话说,使用 STARK 让用户在验证命题上的时间要比计算命题的时间少得多。

Cairo 允许表达通用计算命题,这些命题可以经 STARK 证明所证实,再经相应的 STARK 验证器验证。

这就是执行递归的机会所在:就像可以写一个 Cairo 程序来证明成千上万的交易正确性,也可以写一个 Cairo 程序来验证多个 STARK 证明。可以生成一个证明来验证多个「上游」证明的有效性。这就是我们所说的递归证明。

由于对数压缩和证明时间大致呈线性关系,证实 STARK 证明所需的时间相对较短(不久的将来预计只需要几分钟)。

在实现递归时,SHARP 可以一收到命题就可以对其进行验证。证明可以各种模式反复地合并成递归证明,直到在某个点上,产生的证明提交给链上验证者合约。图 2 就是典型的递归证明模式:

图 2:典型递归证明流程
图 2:典型递归证明流程

在本例中,有四个命题发送给 SHARP(可能源自四个不同应用)。这些命题各自平行证明。然后,每一对证明都由一个递归验证器命题(验证 STARK 证明的 Cairo 程序)来验证,由此产生一个证明。这一命题证实有两个证明经过验证。接下来,通过递归验证器命题再次合并这两个证明。这就产生了一个证明,证实所有四个原始命题。此证明最终可以提交到链上,由 Solidity 验证器智能合约进行验证。

递归证明的直接优势

降低链上成本

毫无疑问,我们实现了将多个证明「压缩」成一个,这意味着每笔交易链上验证成本会大幅更低(其中每个命题可能包含许多交易)。

使用递归证明可以消除至今限制证明大小的计算资源障碍(如内存),因为每个命题容量有限,都可以单独证明。因此当使用递归时,递归的有效组合命题 (Train) 的容量几乎是无限,每笔交易成本可以降低好几个数量级。

在实际操作中,降低成本取决于可接受的延迟(以及交易到达的速度)。此外,由于每个证明通常也伴随相应链上数据输出,因此与单个证明一起写入链上的数据量也会有限。尽管如此,将成本降低一个数量级,甚至继续提升性能都可以轻松实现。

降低延迟

递归证明模式可降低证明大型组合命题延迟。有两个因素起到作用:

  1. 接收的命题可以并行证明(而不是证明巨大的组合命题)。
  2. 无需等到 Train 中的最后一个命题到达即可证明。相反,有新命题加入可以随时与证明结合。也就是说,加入 Train 的最后一个命题的延迟,大致上是证明最后一条命题所需的时间加上证明递归验证器命题(证明所有已经「加入」这个特定 Train 的命题)所需的时间。

我们正在积极开发和优化证明递归验证器命题的延迟问题。预计几个月内证明递归验证器命题会达到几分钟的数量级。因此,一个高效的 SHARP 延迟可控制在几分钟到几小时,延迟长短取决于对每笔交易链上成本的取舍。这是对 SHARP 延迟的重大改进。

促进 L3 应用

用 Cairo 开发的递归验证器命题也开启了向 StarkNet 提交证明的可能性,因为该命题可以写入 StarkNet 智能合约。这允许在 StarkNet L2 公共网络上部署 L3

递归模式也适用于来自 L3 的聚合证明,由 L2 上的单个证明验证。因此,L3 也可以实现超大规模扩展。

更多妙用

应用递归

递归为希望进一步扩展其成本和性能的平台和应用程序开辟了更多机会。

每个 STARK 证明证实应用于某些「公开输入」(或 Cairo 术语中的「程序输出」)的命题有效性。从概念上来说,STARK 递归将具有两个输入的两个证明压缩一个具有两个输入的证明。换句话说,虽然证明的数量减少,但输入数量未变。然后,输入通常由应用程序用以更新 L1 上的某些状态(例如,更新状态根或执行链上取款)。

如果递归命题可以在应用层感知,即识别应用程序本身的语义,那么递归命题既可以将两个证明压缩为一个,也可以将两个输入组合为一个。最终的命题证实基于应用程序语义的输入组合的有效性,这就是应用递归(Applicative Recursion,参见图 3 示例)。

图 3:应用递归示例
图 3:应用递归示例

命题 1 证明从 A 到 B 的状态更新,而命题 2 验证从 B 到 C 的进一步更新。命题 1 和命题 2 的证明可以合并为第三个命题,直接证明从 A 到 C 的更新。通过应用类似的递归逻辑,可以非常显着地降低状态更新的成本,达到最终延迟要求。

应用递归的另一个重要示例是压缩来自多个证明的汇总数据。例如,对于像 StarkNet 这样的有效性证明 Rollup,L2 每次存储更新也作为传输数据在 L1 更新,确保数据可用性。但是,不需要为同一个存储单元发送多次更新,因为只有经过证明验证过的交易最终才能满足数据可用性。此优化已在单个 StarkNet 区块中执行。但是,通过为每个区块生成证明,应用递归可以压缩多个 L2 区块汇总数据。这可以显着降低成本,降低 L2 出块时间,而不会牺牲 L1 更新的可扩展性。

值得注意的是:应用递归可以与前面描述的应用通用递归结合使用。但这两种优化互无关联。

降低链上验证器的复杂性

STARK 验证器的复杂性取决于用以验证的命题类型。特别是对于 Cairo 命题,验证器的复杂性取决于 Cairo 语言中允许的特定要素,更具体地说,是支持的内置项(如果把 Cairo 比喻成 CPU,那么内置项相当于 CPU 中的微电路:计算执行太过频繁,所以需要优化自身计算)。

Cairo 语言不断发展并提供越来越多有用的内置项。另一方面,递归验证器只需要使用一小部分内置项。因此,递归 SHARP 可以通过支持递归验证器中的完整语言来成功支持 Cairo 中的任何命题。具体来说,L1 上的 Solidity 验证器只需要验证递归证明,因此验证器可以仅限于验证 Cairo 语言一个更稳定的子集:L1 验证器不需要随最新、最稳定的内置项更新。换句话说,命题不断演化,复杂的验证就交由 L2 处理,L1 验证器只需要验证简单、稳定的命题。

减少计算足迹

在递归之前,聚合多个命题为一个证明受到可用计算实例上可以证明的命题大小(以及生成此类证明所需的时间)的限制。

有了递归,无需再证明如此庞大的命题。因为有了更多又小又便宜的计算实例可供使用(尽管计算实例可能要比使用大型单片证明器时需要的更多)。这使得在更多的物理和虚拟环境中部署证明器实例成为可能。

总结

通用计算的递归证明现已为包括 StarkNet 在内以太坊主网上的多个产品系统服务。

由于可以不断改进,递归的优势会逐步显现。并行计算的潜力得以发挥后,Gas 费降低,延迟改善,超高扩展性终将实现。

递归在成本和延迟方面的优势异常显著,还会催生 L3 和应用递归等新机会。递归验证器持续优化,性能和成本效益也都会逐渐提升。

Subscribe to Starknet 中文
Receive the latest updates directly to your inbox.
Mint this entry as an NFT to add it to your collection.
Verification
This entry has been permanently stored onchain and signed by its creator.