从理论到代码理解Lasso和Jolt

本文介绍了两项新技术——Lasso和Jolt,它们为SNARK设计带来了根本性的新方法,显著提升了性能并改善了开发者体验。Lasso提供了更快的查找论证,支持大型表格的高效查找,而Jolt则为零知识虚拟机(zkVM)设计带来了简化,使开发者可以更容易地编写高效的SNARK应用。文章深入探讨了这些技术的背景、实现及其在区块链开发中的潜在影响。

编辑备注:在本系列中,我们分享了两项新创新,这些创新可以显著加速 web3 中应用程序的扩展和构建:Lasso 和 Jolt。它们代表了一种从根本上新颖的 SNARK 设计方法,提高了广泛部署的工具链的性能,提升幅度达到一个数量级或更高;提供了更好、更易于访问的开发者体验;并使审计变得更加容易。

有关这些技术的深入介绍,以及它们技术演变的见解,请见 这篇文章 ,作者是 a16z crypto 研究合作伙伴 Justin Thaler。或者查找有关 Lasso Jolt 的研究论文。你还可以观看有关查找奇点和 SNARK 设计的新思考方式的 解释视频

在过去的几年中,广泛的研究致力于提高 可验证计算 的效率和可用性,以实现无信任的分布式系统的承诺,并解决当前 web3 中的一个关键障碍:帮助区块链扩展。尽管提出了许多理论应用,但它们在实践中受限于现有技术的效率。

特别是 SNARKs (简洁的非交互式知识论证)已经取得了很大进展。但关于它们的 性能、安全性和需要专业且通常是高强度的工程工作仍然存在一些误解和不确定性,这些威胁着这一重要技术的长期采用。因为对于 web3 建设者来说,SNARKs 可以解锁计算密集型应用程序,使得可以构建的应用类型比现在更多。

为了解决这些问题并加速该领域的进展,两个新的创新, Lasso 和 Jolt,提出了一种根本不同的 SNARK 设计方法——这种方法不仅更快,而且为开发者提供了可能更易于理解和构建的基础。Lasso 和 Jolt 论文中描述的技术代表了与之前工作的显著演变。但是,具体它们是什么呢?

  • Lasso 是一种新的查找论证(下面将详细介绍),具有显著更快的证明者。我们初步实现的查找论证相较于流行且经过良好工程设计的 halo2 工具链的查找论证实现了大约 10 倍的加速;我们预计在完成优化时能实现约 40 倍的改进。为了展示这一点,我们发布了用 Rust 编写的 开源实现。我们邀请社区帮助我们使 Lasso 尽可能快速和稳健。
  • 陪伴 Lasso 的第二项创新是 Jolt,一种基于 Lasso 的 zkVM(零知识虚拟机)设计新方法。Jolt 实现了“查找奇点”——这是以太坊基金会的 Barry Whitehat 提出的愿景,旨在实现更简单的工具和轻量级的以查找为中心的电路(关于这为什么重要,请下文详细说明)。相较于现有的 zkVM,我们预计 Jolt 能够达到类似或更好的性能——更重要的是,提供更流畅和更易得到的开发者体验。有了 Jolt,开发者可以更轻松地用他们选择的高级语言编写快速的 SNARK。

简而言之:Lasso 介绍了一种流线化的 zkVM 方法,通过对大规模结构化表进行查找而避免了繁琐的手工优化电路,减少了浪费;以 Jolt 为基础的 VM 简单、快速且易于审计。这两个创新使得现有流行的编程语言的 SNARK 成为可能——不仅限于那些为此任务而设计的语言。

因此,在这篇文章中,我们分享了关于 SNARK 和 zkVM 重要性、以及 Lasso 和 Jolt 背后的动机和概念的简要介绍,还有关键改进和性能基准。接着,我们深入探讨 Lasso 的 实现——这展示了区块链工程师和其他开发者如何使用和构建这一工具。

为什么 SNARK 和 zkVM 重要,关键概念和当今挑战

由于许多区块链节点验证和记录每一笔交易,因此在区块链上运行计算成本可能非常高。为了避免更高的交易成本,开发者通常在链上的计算上做最少的工作,以启用他们的应用。因此,SNARK 在通过使应用能够在链外创建昂贵计算的收据,并仅在链上承担验证这些收据的成本方面,具有中心地位。这是因为“简洁性”方面(SNARK 中的“s”)意味着这些收据很短,并且可以通过显著少的工作来验证,而无需重新计算每一笔交易。

尽管最近取得了进展,但 SNARK 仍然计算代价高昂、审计困难,并对多数区块链工程师来说难以获取(例如,当前的方法需要一个即使是对经验丰富的开发者来说也不熟悉的编程模型)。有关当前 SNARK 设计范式的更多挑战,请参见 这篇文章

当前状态:为了使用 SNARK,开发者通常首先应用一个 前端,将计算机程序转换为 电路 这是一个由概率证明系统(后端)可用的 多项式约束 系统。在此方法中,前端和后端都会引入 显著的开销 ,无论访问多少条目。出于性能原因,许多 SNARK 开发者仍然手动编写这些电路/多项式约束。其他项目采取不同的方法,开发了一个模拟现代计算机设计的工具链,这些计算机执行简单的指令集,如 ARM、x86 和 RISC-V。用 Java、C++ 和 Rust 等高级语言编写的程序被编译为这些指令集,以便让硅片能够直接理解。

但现代计算机不向程序员暴露 CPU 指令有充分的理由。当以高级语言编写时,程序员可以使用抽象——如数组、结构和类——确保代码相对易于阅读和编写。相反,CPU 指令集仅提供像 ADD、MUL、OR 和 JMP 这样的原始操作。这些操作的长序列容易被硅片执行,但对人类而言,理解和执行时易出错。人类实际上在逻辑方面表现不佳;能够由计算机产生更多逻辑将是更好的。

这将我们引向 zkVM:SNARK 可以证明在特定 CPU 的汇编语言中执行任意计算机程序是正确的。一个支持现有指令集架构的 zkVM——例如 RISC-VEVM——可以利用现有编译器基础设施将高级语言编译为 VM 的汇编代码。这导致了一种友好的开发者工具链,不需要开发者从零开始构建所有基础设施。开发者可以用自己选择的语言编写程序,而不用担心 SNARK 的内部机制,也不必为自定义手工编码的电路感到担忧。

为了进一步理解 SNARK 的挑战和机遇,以及这项工作的影响,了解查找论证的意义也很重要。

理解查找

针对 CPU 的编译器常常利用在硅片上廉价的操作。但不幸的是,这些操作在 SNARK 中可能非常昂贵:

例如,位运算——将指令的输入视为一系列二进制数字而不是单个整数——在 CPU 上几乎是 免费,但在当前的 SNARK 中却是 极其昂贵

位与操作的图示,使用两个 4 位操作数 | 来源:a16z crypto

为了解决这个问题,研究人员常常使用一种称为“查找论证”的技术。与其通过加法和乘法直接计算位运算指令,不如利用查找论证 预计算 所有可能输入的位运算指令的输出。然后,zkVM 采用相对廉价的 SNARK 操作——也称为“查找”——来验证当前指令是否存在于预计算表中。这样做能够降低指令的成本。

4 位(16 行)位或表的物化说明 | 来源:a16z crypto

问题在于,像 OR 这样的指令有两个 64 位输入和一个 64 位输出(见上图)。这意味着在预计算表中有 2128 个条目[编辑者的注:那是多少340,282,366,920,938,463,463,374,607,431,768,211,456条目]。简单地物化这样的表中的所有可能组合是完全不切实际的,即使将已知宇宙中所有的硬盘连接到你的机器上。

目前,查找论证通常应用于最大为 216 的表大小,并且表的大小通常被 “分块” 结合。但分块策略通过以下方式引入了显著的开销:

  • 将一个整数分解为多个块
  • 每块都需要查找一次
  • 从分块查找中重构一个整数。

额外的复杂性也在很大程度上增加了开发者和审计者的认知开销。

将一个 32 位位或表示例转换为 8 位表的分块减少策略的说明 | 来源:a16z crypto

使用查找论证的另一个挑战——这导致了 Lasso 的关键洞察——是这些巨大表中的大多数条目是 未使用的。但是,证明者必须仍然为所有未访问的表条目 “支付” 费用。即使查找表可能是不可实现的巨大(假设有 2128 个条目),仅有其条目的一小部分实际上会被查找,这不必要地增加了成本。

这就是 Lasso 和 Jolt 发挥作用的地方。

Lasso 和 Jolt 如何改变现有的 SNARK 范式

Lasso 使得在非常大表上进行高效查找的新策略成为可能(如在 64 位位运算中涉及的 2128 大小的表)。与现有的查找方案不同,成本不会随着查找表的大小而线性增长,无论访问了多少条目。相反,成本主要随查找次数的增长而增长:Lasso 高效地证明对这个表的查找,而无需在任何时候物化整个表。

Lasso 对所有 CPU 指令具有类似的低成本,而不仅仅是位运算子集。将 CPU 指令转换为 Lasso 查找的技术在 Jolt 中有所描述。

与此同时,Jolt 将 Lasso 应用到 整个指令集,例如 RISC-V 或 WebAssembly。关键的洞察是大多数指令可以通过组合少量小型表的查找来计算。例如,针对 64 位操作数的位与指令可以通过将查找索引分割为“块”并对包含 8 位操作数位与结果的较小“子表”进行查找来重构。事实证明,所有 RISC-V 指令有类似的结构,因此它们的查找可以使用 Lasso 进行证明。

结果是一种 zkVM 实现的新范式,这在以前是无法实现的,因为先前的查找论证要求 (超)线性预处理或证明者时间。

更快速、更友好的 SNARK 设计的好处

在过去,上述挑战——特别是计算针对整个查找表的承诺和打开证明的成本——一直是查找方案中的关键瓶颈。因此,它使开发者无法建设更多计算密集型的 web3 应用,而这些应用只有在具有非常高性能的 SNARK 时才能得以实现。

但 Lasso 和 Jolt 的创新带来了许多好处,包括: (1) 更快的性能, (2) 更好、更易获取的开发者体验,及 (3) 更容易审计。以下简要阐述这些内容。

1. 更快的性能

Lasso 并不是第一个查找论证实现,但我们预计它将是最快的。

我们的初步基准测试验证了 Lasso 理论性能,最容易理解的是与现有实现进行比较。我们使用 halo2,它是最广泛使用的支持查找的 SNARK 工具链。以下是关于 2022 年款 Apple M1 Pro(16GB RAM)上 16 位查找表与 halo2 后端 的性能比较的基准。

_基准测试日期:2023年7月1日 | source_

然而,Lasso 的主要优势在于更大的查找表——因相应查找表的巨大计算成本而在其他框架中无法使用的查找。在 2 操作数 64 位位与表的 1k 到 1M 的查找的基准测试结果如下:

基准测试日期:2023年7月1日 | source

如果我们直接使用 halo2 或其他现有查找方案,那么我们就必须物化一张包含 2128 行的表,这是不可能的(因此上面描述的分块策略)。但使用 Lasso,我们现在可以 直接 查找 CPU 指令。每个 CPU 指令直接映射到一个 Lasso 查找。

干净、简单、高效。

(2) 更易获取的开发者体验

Lasso 提供了更友好的开发者途径,以实现 zkVM,优势于现有方法。

以前的 SNARK 设计方法涉及将 CPU 指令构形成电路并进行手动优化——这是一项低级且安全至关重要的任务,需要在特定领域语言中的专业知识。相比之下,来自不同语言生态系统的开发者应该可以相对轻松地上手 Lasso。

这是因为在 Lasso 中,指令通过其子表分解进行定义:其“大”查找表可以从少数较小的“子表”组成。更重要的是,这种分解可以用高级编程语言简单明了地描述。例如,在 我们的实现 中,指令可以在少至 50 行 Rust 代码中实现(例如 位与)。此外,不同指令集之间的许多指令在概念上是相同的,允许显著的代码重用——例如,WASM、EVM 和 RISC-V 都指定相同的基本算数、位运算和比较操作。

(3) 更容易审计

Lasso 简化的开发者体验也使其比以前的方法更易于审计。zkVM 的可审计性尤其有价值,因为如今许多 SNARK 已在区块链上保证了重大的经济价值。由于 Lasso 在 Rust 中实现指令逻辑——而不是在自定义电路中——同时鼓励跨指令集的代码重用,因此它将待审计的代码表面面积集中到一个相对较小且易读的代码库中。

现在我们已分享了当前 SNARK 的状态,以及 Lasso 和 Jolt 的加入情况,接下来我们将分享更多关于如何将 Lasso 从研究论文翻译成实践,通过开源实现。对于希望在此基础上构建的人员,这里有我们进展的总结——以及一些技术细节、挑战和机遇——还有一些为建设者提供的建议方向。

实现 Lasso 的说明

在实现 Lasso 和 Jolt 所设定的整体愿景之前,还有很多工作要做。但截至今天,Lasso 可以用于高性能独立查找表。近期,它还将用于构建完整的 zkVM(这就是 Jolt 的愿景)。

为了展示潜力,我们发布了 Lasso 的开源 实现。在工程领域还有很多改进和扩展 Lasso 的工作,我们欢迎更多对 SNARK 未来感兴趣的开源贡献者加入。

从 Spartan 到 Lasso

正如在前面的章节中提到的,Lasso 利用查找的“稀疏性”来实现次线性证明者运行时间,这是在 Setty 的 Spartan 论文 中概述的。更准确地说,Spark 将任意的多线性多项式承诺方案转变成专门针对 稀疏 多线性多项式优化的方案。

为了利用它们的共同基础,我们将 Lasso 构建为 Spartan 代码库的分支。更具体地说,我们在 Spartan 的 Arkworks 分支 的基础上进行构建,以便 Lasso 可以受益于不断扩张的 Arkworks 生态系统,反之亦然。

MSM 优化

我们的实现性能在很大程度上取决于多标量乘法(MSM),该操作是多项式承诺方案所需。MSM 是一个涉及群体指数运算的操作,通常用于多项式承诺方案和 SNARK 中。与以前的查找论证相比,Lasso 通常只需要对小的域元素进行承诺。

我们对 Arkworks 的 MSM 算法进行了 修改,以利用这一点并实现约 30% 的证明者加速。请注意,尽管我们的实现目前使用 Hyrax 承诺,但 Lasso 也可以通过非 MSM 基础的承诺方案来实例化。

朝向 Jolt

我们目前正与 Lasso 一起努力实现 Jolt。为了达到完整的实施效果,我们需要将指令集中的每个指令(例如 32 位 RISC-V 基本整数指令集的 40 个指令——另外还有八个整数乘法和除法扩展)实现为子表的组合。这样的实现过程就简单得多,例如使用 SubtableStrategy 特性

截至目前,我们已实现了 AND、OR、XOR、SLTU(无符号小于)、以及范围检查等示例。有关新指令实现过程的进一步详细描述,请见 该 repo

未来工作

除了实现 Jolt 所需的工作外,还有许多任务正在进行中,或可由其他开发者接手,包括:

  • 实现/集成不同的多项式承诺方案,例如多线性变体的 KZGPSTZeromorph、等)、DoryLigeroBrakedown 和在 Lasso 论文中介绍的 Sona
  • 实现 Quarks 论文 第 6 节中所述的宏观积论证优化
  • 更全面的基准测试、测试和错误处理
  • 使用 SNARK 递归实现高效的链上证明验证

这只是我们看到的一些方向,但还有许多 其他机会 可供贡献!或者欢迎随时与我们联系,提出问题、想法和反馈: @samrags_ @moodlezoup

\\*\

  • 原文链接: a16zcrypto.com/posts/art...
  • 登链社区 AI 助手,为大家转译优秀英文文章,如有翻译不通的地方,还请包涵~
点赞 0
收藏 0
分享
本文参与登链社区写作激励计划 ,好文好收益,欢迎正在阅读的你也加入。

0 条评论

请先 登录 后评论
a16z Crypto
a16z Crypto
https://a16zcrypto.com/