一文探讨ZK编程语言

零知识证明（ZKP）是一种强大的密码学工具，它可以在验证计算的正确性的同时，保护输入数据的隐私。作为这一关键基础设施的组成部分，领域特定语言（DSL）发挥了至关重要的作用，简化了 ZKP 电路的开发和验证过程。它们在将抽象概念与证明系统所需的精确电路表示之间扮演了重要的角色，充当了两者之间重要的桥梁。

证明系统面临的关键挑战之一是将抽象的高层概念转化为实际电路。然而，DSL 的出现解决了这一难题，通过促进将这些抽象概念以更具体和可实现的方式结构化表达，从而应对这一挑战。

在过去的十年里，我们目睹了 DSL 在数量和多样性方面都取得了显著增长。这一领域的活跃表现在多种电路语言的发展中，包括 Noir、Leo、Zinc 等。无论您需要通用性的选项，比如 Circom，还是为特定平台定制的解决方案，比如 Cairo，您都可以选择从众多语言和框架中挑选，以编写ZKP 电路。

在本文中，我们将探讨开发者们正在积极利用的主要 ZK编程语言，并分析每种语言的最佳特点。

Cairo，是支持 STARK 证明的通用计算程序的核心语言，在 StarkNet 和 StarkEx 的成功中扮演了关键角色，推动了以太坊主网上应用的可扩展性。值得一提的是，Cairo 在支持各种应用方面发挥了重要作用，包括 dYdX、Sorare、Immutable X 等。"Cairo" 这个名字来源于 "CPU代数中间表示"的缩写。在零知识证明领域，它扮演了类似汇编语言的角色，使熟悉 C、C++ 或 Solidity等低级编程语言的开发人员能够更轻松地上手。

受 Rust 的启发，Cairo 赋予了开发者创建 Starknet 智能合约的能力，着重关注安全性和用户友好的开发。Cairo 具有强大的语法，简化了 ZK 电路的创建，使用户能够在 Cairo 程序中执行各种任务。此外，Cairo 的一个显著优势在于其可扩展性，允许灵活地引入新功能和功能。

在 ZK 系统中，效率和可扩展性是至关重要的因素，而Cairo通过强调这两个方面来满足这一要求。该语言集成了优化策略，包括约束减少和循环消除，以减轻通常与 ZK 电路相关的计算负担。Cairo 对电路设计的优化导致更快的证明生成和验证，使其成为需要高吞吐量和最小延迟的应用的理想选择。

Cairo 的扩张发展是非常的令人瞩目，在过去两年里，全职开发者数量出现了非凡的激增。这一激增凸显了 Cairo 的适应性，因为 Cairo 的用途不仅局限于区块链，而是在任何需要进行计算验证的情境中都具有重要意义。因此，我们可以预见开发者对 Cairo 的采用将进一步迎来显著增长。

2023年9月28日，Starknet 推出了其编程语言 Cairo v2.3.0 的重要升级。这个版本标志着合约更模块化的重大进步，通过引入新功能、存储选项和事件管理，提升了智能合约的潜力。这些组件的整合提供了一种灵活的方式，用于扩展合约功能，使第三方模块能够增强合约的功能性。

Zinc 是一种专为在 zkSync 平台上创建智能合约和 SNARK 电路而设计的编程语言。它采用了Rust 语法，融合了 Solidity 的元素，并提供了独特的功能。

Zinc 的独特之处在于它的用户友好性。您无需深入了解一阶约束系统（R1CS）的所有复杂细节就能编写安全的代码。Zinc 强调不可变性，使其天生具备函数式特性。这意味着它优先考虑不可变数据和函数评估，从而减少副作用，促进编写更干净、更少出错的智能合约代码。

此外，Zinc 还包括安全的数学操作，以防止潜在的溢出，确保所有操作的安全性。尽管它有一些限制，比如没有无限循环和递归，但 Zinc 通过控制台日志跟踪简化了调试过程。这些跟踪可简化在测试网络或主网络上跟踪和解决问题的交易过程，从而提升了调试体验。

Noir 是由 Aztec 开发的开源 DSL，基于 Rust，旨在简化 ZK 电路和 ZK 程序的创建，无需深入了解加密学知识。它被认为是最易入门的语言之一，适用于编写与任何证明系统兼容的 ZK 应用程序。Noir 注重安全性、简洁性和性能。它提供了类似 Rust 的高级语法，将加密安全性抽象化，简化了加密基本原语的使用，同时保持高性能。

Noir 在扩展可以利用 ZKP 提供的隐私保护能力的应用范围方面具有显著优势，从而增强了隐私和验证效率。Noir 编译成一种称为 Abstract Circuit Intermediate Representation（Acer）的中间表示，然后可以进一步编译成 R1CS。将后端证明系统与语言本身分离使 Noir 能够支持各种证明系统，包括 Aztec Brettenberg、Turbo Plonk 以及潜在的未来集成，如 Groth16和Halo2。

该语言提供了一个标准库，包括高效的功能，如 SHA-256（一个生成固定大小输出的加密哈希函数）和 Pedersen-Merkle 检查（一种使用 Pedersen 承诺和 Merkle 树确保数据完整性和一致性的加密验证技术）。Noir 的设计类似于 Rust，包括应用程序开发人员熟悉的特性，如函数、子模块、用户定义类型（结构体）、条件语句、循环和全局常量。此外，还在不断努力开发泛型和一等函数，进一步增强 Noir 的表达能力。

需要注意的是，Noir 仍在不断完善中，可能存在一些限制和潜在的错误。但开发团队致力于持续改进和优化该语言。

o1js，前身为 SnarkyJS，是由 0(1)Labs 开发的 TypeScript 库，用于使用 SNARK 编程语言创建智能合约。它充分利用了已经建立的技术，如 Node.js 和浏览器兼容性，以确保开发者能够轻松获取和方便使用。

o1js 能够与 JavaScript 和 TypeScript 库和工具无缝集成，为开发者提供了强大的生态系统和广泛的社区支持。这种集成简化了开发流程，减少了采用新开发环境所带来的学习曲线。此外，它完全支持 Visual Studio Code（VS Code），这是一款广泛使用的代码编辑器，可让开发者充分利用功能，如代码补全、语法高亮和调试，提升开发体验。

o1js 本质上是一个多功能的 ZK 框架，为您提供了创建zk证明所需的关键工具。它支持创建多样化的ZK程序，涵盖了各种内置的可证明操作，包括基本算术、哈希、签名、布尔操作、比较等等。借助o1js框架，您可以在 Mina Protocol 上构建 zkApps，这些智能合约在客户端执行，具有私有输入。

值得一提的是，在2023年9月初，0(1)Labs 团队宣布将从 SnarkyJS 过渡到 o1js，并强调了他们改进性能的承诺。特别值得注意的是，他们实现了库加载时间的3-4倍减少，这指的是导入 o1js 所需的时间，这个过程可能会阻塞主线程。对于Web应用程序而言，加载时间对 JavaScript 执行时机和整个页面渲染都具有重要意义。此外，该团队还更新了 Mina zkApp CLI，提升了用户界面构建体验，并宣布将进一步改进 Archive Node API，以增强其可靠性和清晰性。

Aleo 区块链在智能合约领域独树一帜，强调隐私保护。其核心是 Leo 编程语言，这是一种受 Rust 启发的静态类型语言。Leo 专为开发私有应用而设计，为那些希望建立安全和保密的分散生态系统的创作者提供了支持。Leo真正独特之处在于，它在引入通用零知识应用的全面工具包方面发挥了开创性作用。这个工具包包括测试框架、包注册表、导入解析器、远程编译器和定理生成器。

Leo 的构想来自一支由 Howard Wu 领导的开发团队，他们设想了一种可以赋予开发人员能力，以构建优先考虑隐私和安全性的分散式应用程序。Leo的设计汲取了Rust的原则，同时融入了一些类似JavaScript的元素，以促进开发过程中的熟悉感和便捷性。此外，Leo旨在通过提供集成的测试平台、包注册表和导入转换器来加速开发，简化开发流程。这种集成使开发人员能够专注于其应用程序的核心逻辑，而不会被基础设施问题拖累。

Leo 的一个引人注目的特点是其编译器，该编译器将程序转换为低级的 R1CS 证明格式。Leo 编译器的独特之处在于其严格的正式验证过程。这种验证至关重要，因为漏洞可能在多个阶段出现，从初始编程到审计和编译。通过进行严格的数学检查，以确保编译器与程序员的意图一致，Leo 旨在降低未被察觉的错误或潜在的漏洞风险，尤其是在 L2 上下文、ZK-rollups 或 Leo 平台上的私有程序中。

Circom，一种专为 ZK 电路开发精心设计的 DSL，是由 Jordi Baylina 和 iden3 团队共同打造的成果。Circom 编译器采用 Rust 编写，其主要任务是编译使用 Circom 语言编写的电路。值得一提的是，Circom 已成为现实世界中杰出的 ZK 应用程序的首选选择，例如 Dark Forest 和 Tornado Cash。它之所以备受欢迎，归功于其出色的性能表现，包括通过优化的 WASM 证明实现快速的浏览器证明时间，通过 rapidsnark 实现高效的服务器端证明，以及高效的链上验证。

然而，需要认识到 Circom 的功能主要专注于 ZK 电路开发，这可能使其在处理更广泛的计算任务时不太适用。寻求更多功能、能够满足更广泛开发需求的开发者可能会觉得 Circom 的能力受到一定限制。在这种情况下，开发者可能需要结合其他编程语言或框架来满足更广泛的开发需求。

图片来自 Circom

Circom 的兼容性主要集中在广泛使用的 ZKP 系统，如 snarkjs 和 libsnark。虽然这种兼容性确保了与这些广泛使用的系统的无缝集成，但也意味着 Circom 电路继承了与这些依赖关系相关的特定功能和限制。那些偏好或需要替代 ZKP 系统的开发者可能会面临兼容性挑战，或需要投入额外的工作来适应和将 Circom 生成的电路集成到他们首选的系统中。

Lurk 是一种受到 Scheme 和 Common Lisp 影响的静态作用域 Lisp 方言，具有独特的特点：它允许使用 zk-SNARKs  直接证明程序执行的正确性，从而实现了紧凑高效的验证。

Lurk 的主要用途包括：

可验证计算：Lurk 允许您在零知识条件下证明其表达式的正确性，增强了对计算结果的信任。

零知识：用户可以证明知识，而无需透露除公共输入之外的具体信息，从而保护隐私。

内容寻址数据：每个 Lurk 程序都配备有一个唯一的内容标识符（CID），使其与 IPFS 和 IPLD 兼容。

图灵完备性：Lurk 支持创建和证明任意计算声明。

高阶函数：Lurk 函数可以接受和返回函数，实现了富有表现力的函数式编程。

处理私有数据的计算：Lurk 使得可以处理私有数据，同时确保可以证明的正确输出，而不会泄露隐私。

在构建通用电路时，Lurk 充分利用了 Lisp 的 “cons” 内存分配器。该分配器合并表达式并生成引用通过散列。关键在于证明两个表达式确实散列成相同的引用。这种验证使得 Lurk 能够在 snark电路内执行计算。

Lurk 的功能非常丰富，包括支持无限递归、循环、条件控制流以及多个后端证明系统，如Groth16 与 SnarkPack+ 和 Nova。这种多功能性为各种应用打开了大门，包括验证计算、私有数据处理，以及在 snark 电路内执行图灵完备程序。

随着 ZK 应用多样性的增加，DSL 在 ZK 领域的发展前景广阔。DSL 成功的关键在于建立蓬勃发展的社群和丰富的库，以丰富开发者的体验。那些将与现有库兼容性置于优先位置的 DSL 可以充分利用更广泛的开发者社群的知识和资源。这种方法有助于更顺畅地集成，加速开发，并在实施ZK应用程序时提供更大的灵活性。这种合作努力对于培育 DSL 周围更为健全的生态系统至关重要，为开发者提供切实的好处，并将进一步推动 ZK 技术的采用和有效性。