简介
领域特定语言（DSL）在零知识（ZK）证明[4]领域中起着至关重要的作用。在核心上，ZK 证明解决了在不透露任何附加信息的情况下证明秘密数据中某些属性存在的挑战。然而，将高层次的想法转化为具体的证明可能会很复杂。这就是 DSL 发挥作用的地方，它们将抽象概念与证明系统所需的电路表示桥接起来。
证明系统[5]是一种允许一方向另一方证明某个陈述或主张的有效性而不透露任何敏感信息的方法或协议。它涉及一组规则和程序，使证明者能够说服验证者某个陈述的真实性，例如计算的正确性或某些知识的拥有，而不透露任何底层的秘密或数据。
然而，证明系统不能直接处理高层次的概念。相反，它们需要被转化为表示所需属性的电路。从高层次概念到电路的这种转变带来了挑战。这就是电路语言发挥作用的地方。电路语言通过提供一种结构化和形式化的方式来表达高层次的想法来解决这个问题。
在过去的十年中，电路语言的数量和多样性有了显著增长。许多电路语言的发展，如 Noir、Cairo[6]和 Leo，表明了该领域的活跃程度。这种语言的增多使得我们可以比较和对比它们的特性、相似之处和差异。通过对这些语言进行综合考察，可以更深入地了解整个电路语言的格局。
TLDR;
– Noir – 由 Aztec 开发，抽象了密码学的复杂性，使得任何背景的开发人员都可以编写 ZK 电路。
– o1js – 由 O(1) Labs 开发的 TypeScript 库。允许开发人员编写智能合约。与现有的 JavaScript 和 TypeScript 库和工具很好地集成。
– **Circom**[7] – 专为 ZKP 电路开发而设计。提供精确性和清晰性，其功能主要集中在这个特定领域。
– Leo – 为开发人员提供了一个用户友好的环境。采用了经过形式验证的编译器架构，重点是早期错误检测和预防。
– **Cairo**[8] – 强调效率和可扩展性。通过标准接口支持互操作性，可以与区块链平台、智能合约和链下系统集成。
– Lurk – 通过利用 Lisp 实现通用电路，解决了传统 SNARK 的局限性。
术语表
由于我们将涉及技术概念，以下是一些可能在后续文本中遇到的复杂术语的术语表：
• 抽象电路中间表示（Acer：Abstract Circuit Intermediate Representation）： Noir 使用的 ZK 电路的中间表示，可以编译成一阶约束系统（R1CS）。
• 自定义门（Custom gates）： 专为在 ZK 电路中高效且安全地执行密码操作而设计的专用逻辑门。
• SHA-256： 一种密码哈希函数，接受一个输入并产生固定大小的输出。
• Pedersen-Merkle 检查： 使用 Pedersen 承诺和默克尔树的密码验证技术，可以验证数据的完整性和一致性。
• 图灵完备性：计算系统的属性，可以模拟图灵机，在足够的时间和资源下能够解决任何可计算问题。
• 过程传递风格（CPS：Continuation Passing Style）：一种编程技术，将评估过程分解为可管理的步骤，实现统一且高效的执行。
• 域元素（Field elements）：有限数学域中的元素，常用于密码学方案和计算中。
Noir
Noir[9] 是 Aztec 设计的一种领域特定语言（DSL），旨在简化 ZK 电路和 ZK 程序的创建，无需广泛的密码学知识或成为密码学家。其主要目标是使来自任何背景的开发人员能够编写 ZK（零知识）电路。Noir 优先考虑安全性、简单性和性能。它提供了一种高级的、类似于 Rust 的语法，抽象了密码学安全性并简化了密码学原语的使用，同时保持高性能。
通过 ZK 证明扩展可能性
Noir 的一个优点是它有潜力扩展可以利用 ZK 证明提供的保护隐私特性的应用范围。这些证明增强了隐私并提供了高效的验证。Noir 编译成一种中间表示称为抽象电路中间表示（Acer），可以进一步编译成一种称为 R1CS（rank one constraint system）的约束系统。这种后端证明系统与语言的解耦使得 Noir 可以支持各种证明系统，包括 Aztec Brettenberg、Turbo Plonk 以及潜在的未来集成，如 Groth16 和 Halo 2。
优化和标准库
开发人员可以在证明系统层面上优化电路，利用自定义门，一种专门设计用于高效和安全执行密码操作的逻辑门类型，提高速度、安全性和各种应用功能。该语言提供了一个标准库，其中包含了优化的函数，如 SHA-256 和 Pedersen-Merkle 检查，这些密码验证技术使用 Pedersen 承诺和默克尔树，能够验证数据的完整性和一致性。
代码组织和表达能力
Noir 通过模块和外部 crate 支持代码组织，便于创建 Noir 程序的库。它提供了数组、元组和结构等复合数据类型，允许开发人员对数据进行分组并实现公共函数。该语言还支持控制流结构，如 for 循环、if 语句以及逻辑和位运算符。泛型和一级函数正在积极开发中，进一步增强了 Noir 的表达能力。
需要注意的是，Noir 仍然在不断发展中。它可能存在一些限制和潜在的错误。开发团队持续迭代语言，并致力于不断改进。
o1js
o1js[10] 是 (0)1Labs 设计的一种 TypeScript 库，用于使用 Snark 编程语言编写智能合约。它利用现有的开放技术，如 Node.js 和浏览器，使其对开发人员来说更加易于访问和方便。通过构建在 TypeScript 上，o1js 允许开发人员利用他们对 JavaScript 和 TypeScript 库和工具的现有知识。
集成
o1js 与 JavaScript 和 TypeScript 库和工具无缝集成，为开发人员提供了强大的功能和广泛的社区支持。这种集成提高了生产力，并减少了采用新开发环境的学习曲线。
VS Code 支持
它提供对 Visual Studio Code (VS Code) 的支持，这是一款流行的代码编辑器。开发人员可以利用诸如代码补全、语法高亮和调试等功能，增强整体的开发体验。
标准库
o1js 提供了一个全面的标准库，包括域元素、un-64、un-32、公钥、私钥和签名等基本类型。这些类型带有内置方法，简化了加密方案、可选数据、布尔值和椭圆曲线的处理过程。
Circom
Circom 是 Circuit Compiler 的缩写，是一种专为零知识证明 (ZKP) 电路开发而设计的强大领域特定语言 (DSL)，由 Jordi Balyna 和 iden3 团队创建。
表达性电路定义
凭借其表达性的语法，Circom 允许开发人员以精确和清晰的方式定义用于 ZKP 应用的电路。然而，对于 Circom 的新手和对 DSL 或 ZKP 概念不熟悉的人来说，其语法和语义可能难以理解。对于新手电路开发者或具有通用编程语言背景的开发者来说，可能需要额外的努力和时间。
范围限制
虽然 Circom 在 ZKP 电路开发方面表现出色，但需要注意的是，它的功能主要集中在这个特定领域。因此，寻求处理各种计算任务的更通用语言的开发人员可能会发现 Circom 有所限制。为了满足更广泛的开发需求，可能需要将 Circom 与其他编程语言或框架结合使用。
工具和生态系统限制
Circom 受到各种开发工具的支持，并拥有不断发展的生态系统，尽管与更成熟的编程语言和框架相比，其工具和资源的可用性可能仍然相对有限。开发人员可能在寻找特定用例或高级功能的全面文档、库和社区支持方面遇到挑战。这种限制可能会对 Circom 的开发速度和社区采用产生影响。
兼容性考虑
Circom 的兼容性主要集中在像 snarkjs 和 libsnark 这样的流行零知识证明系统上。虽然这使得它可以与这些系统无缝集成，但也引入了对它们特定功能和限制的依赖。偏好或需要其他 ZKP 系统的开发人员可能会遇到兼容性问题，或需要额外的努力来适应和集成 Circom 生成的电路到他们首选的系统中。
Leo
Leo[11] 是一种专门设计用于开发零知识证明应用程序的编程语言。它旨在为开发人员提供一个用户友好的环境，特别是那些在区块链生态系统中具有先前经验的开发人员。LEO 类似于 Rust，并具有一些类似 JavaScript 的元素，旨在在应用程序开发中创建熟悉感和便利性。
Leo 的一个显著特点是其编译器，它将程序转换为一种称为 R1CS 的低级证明格式。Leo 编译器的区别在于它经历的严格形式验证过程。这种验证是必要的，因为错误可能在各个阶段出现，包括编程、审计和编译。通过数学上确保编译器遵循程序员的意图，Leo 旨在最大程度地减少错误被忽视或被利用的风险，特别是在 L2 上下文、ZK-rollups 或 LEO 平台中的私有程序中。
认识到尽管尽力而为，错误是不可避免的，Leo 团队强调了早期错误预防和检测的重要性，特别是在处理重要价值转移的系统中。为了解决这个问题，Leo 的经过正式验证的编译器架构注入了额外的信心，降低了意外偏离预期程序行为的可能性。
除了语言和编译器之外，Leo 还提供了各种开发者体验工具和功能。这些组件旨在增强开发过程，简化任务，提高效率。借鉴了七年的经验，并观察了以太坊生态系统的发展，Leo 团队旨在提供一个用户友好的环境，类似于诸如 explorers、部署框架（如Truffle和Ganache）以及简化应用程序开发和测试的其他资源的工具演变。
Cairo
Cairo[12]提供了一种简化构建 ZKP 电路过程的语法。借鉴传统编程语言的灵感，Cairo允许开发人员在设计 ZK 系统时利用他们现有的编程技能。通过其声明性方法，Cairo使得可以规范逻辑语句和计算，更容易地在零知识证明的背景下表示现实世界的场景。
效率和可扩展性
性能是 ZK 系统的关键因素。Cairo通过关注效率和可扩展性来解决这个问题。该语言采用了优化技术，如约束减少和循环消除，以最小化与 ZKP 电路相关的计算开销。通过优化电路设计，Cairo实现了更快的证明生成和验证，适用于需要高吞吐量和低延迟的应用程序。
互操作性和集成性
Cairo 被设计为与现有软件基础设施集成，使开发人员能够将 ZKP 的能力与其他技术相结合。该语言通过标准接口支持互操作性，允许与区块链平台、智能合约和离链系统进行集成。这种灵活性为在去中心化应用、金融系统和数据验证协议中实现增强隐私功能的可能性打开了大门。
社区和生态系统
Cairo项目培育了一个由开发人员、研究人员和爱好者组成的社区，他们为其发展做出了贡献。文档、教程和示例代码的可用性有助于入门过程，使开发人员能够掌握概念并开始构建 ZK 系统。此外，Cairo还受益于 StarkWare 更广泛的生态系统，该生态系统提供支持、工具和研究进展，以增强该语言及其功能。
Lurk
Lurk[13]旨在通过利用 Lisp（一种函数式编程语言）实现通用电路，解决传统 SNARK 和电路的局限性。使用 Lisp，Lurk 引入了一个名为“eval”的通用函数，可以在 snark 电路中评估任何数据表达式。
代码即数据，数据即代码
Lurk 的一个基本原则是将程序表示为内容可寻址的数据。这种方法可以高效地评估和验证 Lurk 程序。内容可寻址性简化了解析过程，并且生成的数据可以直接在 snark 证明者中使用，而无需单独的编译步骤。
在 SNARK 中实现 Lisp
为了创建一个通用电路，Lurk 利用了 Lisp 的内存分配器“cons”。该分配器将两个表达式组合起来，并通过哈希生成对结果表达式的引用。通过证明两个表达式哈希到相同的引用，Lurk 可以在 snark 电路中执行计算。
延续传递风格
Lurk 采用了延续传递风格（CPS）将评估过程分解为可管理的步骤。每个评估步骤都变成了可处理的计算，实现了统一且高效的执行。在 SNARK 电路中包含显式的延续，有助于逐步进行评估过程。
赋予图灵完备性和递归能力
通过采用 Lisp，Lurk 实现了图灵完备性，并支持 SNARK 电路中的无限递归。这一重要能力允许证明复杂计算，并实现能够执行任意计算的通用电路。
影响和应用
Lurk 的能力具有广泛的影响。通过支持无限递归、循环和条件控制流，Lurk 使得在 SNARK 电路中可以进行复杂计算。这为验证计算、私有数据处理和执行图灵完备程序开辟了各种应用。
结论
领域特定语言（DSL）的选择是多样的，并且随着零知识证明（ZK）在各个区块链生态系统中的应用案例不断扩展，预计将继续增长。目前，建立用于构建 ZK 应用程序的主导语言的竞争仍处于早期阶段，这表明我们可以预期在这个领域会有进一步的改进。
然而，大多数 DSL 的一个共同限制是缺乏来自庞大社区和强大库的网络效应。拥有充满活力的社区和全面的库可以极大地提升开发者的体验。尽管这个不足可能会随着时间的推移得到解决，但对于参与 DSL 开发的团队来说，优先考虑与其他库的兼容性非常重要，可以借鉴 o1js 所采用的方法。
通过确保与现有库的兼容性，DSL 可以利用更广泛的开发者社区的集体知识和资源，实现更容易的集成、更快的开发，并在实现 ZK 应用程序时具有更大的灵活性。这种协作的方式将促进围绕 DSL 的更强大的生态系统的发展，使开发者受益，并最终推动 ZK 技术的采用和效果的提升。
