以太坊拨款支持的LLZK：一种新的中间表示（IR）……

LLZK：一种新的 ZK 语言中间表示 (IR)

Veridise 获得以太坊基金会的资助，以开发LLZK

在解决零知识领域的碎片化问题方面，Veridise 获得了以太坊基金会的资助，以构建一种开源的 ZK 电路语言的中间表示 (IR)。

我们称之为 LLZK —— 一个灵活的框架，受 LLVM 启发，旨在统一多种前端语言和后端架构，消除重新发明解决方案的必要。该框架旨在统一和简化电路编译，提升整个 ZK 领域的可维护性和安全性。

使用 LLZK 编译电路的整体工作流。它由三个主要组成部分：前端、转换/优化过程、后端。

解决 ZK 生态系统中的碎片化

zkSNARKs 和 zkSTARKs 是区块链行业的基石，以回滚和隐私保护区块链/应用的形式确保数十亿美元的安全。与此同时，这两者都是相对较新的技术，我们看到底层方法和相关工具的快速发展。例如，ZK 生态系统充满了各种电路 DSL/框架，包括 Circom、Halo2、Arkworks、Gnark、Zirken 等，新的工具或自定义语言频繁被创建，以利用底层 SNARK 算法的进步。

尽管这种快速发展令人振奋，但生态系统中有很大的碎片化程度。与主流语言不同，每种 ZK 语言都有一个端到端的编译器，将电路/程序转换为特定的约束集。我们将这种碎片化视为有两个负面后果：可维护性差和安全工具有限。

可维护性差

如果研究社区引入了一种新的证明系统，那么语言开发人员需要修改他们的编译器以支持该系统。事实上，如果语言没有快速添加支持，开发人员可能会创建自己的 DSL 或分叉现有语言以支持该系统，进一步碎片化开发生态系统。此外，添加新的译码阶段以支持新类型的算术化也可能引入错误。然而，我们相信，为新算术化添加支持的工作可以在不同语言之间共享。

例如，为了支持新算术化，开发人员需要将约束转换为特定的算术化方案，这需要 1) 添加提取约束的逻辑，2) 将其重写为标准形式（例如，R1CS），3) 添加优化使约束变得简单。

安全工具有限

ZK 被用于滚动或隐私保护区块链等安全关键应用，但可用于帮助 ZK 开发人员检查电路程序正确性的工具非常有限。我们认为这在一定程度上与电路语言的碎片化有关。现有 ZK 安全工具（ Picus、ZKAP、CIVER、CODA、Circomspect、Halo2-analyzer) 仅支持 Circom、R1CS 或 Halo2 之一。

支持新框架往往是项不平凡的任务，因为工具开发人员要么需要修改其底层工具，要么编写翻译器，将用一种语言编写的电路转换为其工具可以接受的语言。这类工作通常繁琐且容易出错。

在 Veridise，我们开发了 工具 用于 ZK 电路验证（Picus、ZK Vanguard）并 发布了有关零知识安全的学术研究。

Veridise LLZK 的设计目标

为了应对关键挑战，我们的 IR 将包含以下关键特性：

• 模块化。 为了编译和分析大电路，IR 必须保留现有语言中存在的模块化特性。特别是，IR 应具有声明子电路/模块的能力。在高层次上，这些组件应该相当于 Circom 组件。
• 域与余域。 电路的输入和输出是被过载的术语，通常在不同框架中有不同的含义。这会影响诸如 Picus、ECNE、Civer 等工具对电路确定性的推理。因此，IR 应包括在 IR 中定义的模块的域/余域的概念。
• 后端的灵活性。 IR（连同周围基础设施）应设计为支持不同的后端。特别是，我们希望用 IR 表达的电路能够编译为不同算术化格式的约束，如 R1CS、AIR 或 Plonk。此外，Picus 等不同安全工具可以轻松编写提取器，将 ZKIR 约束转换为其内部表示。
• 形式验证。 理想情况下，IR 应设计为可以对不同方面进行形式验证——尤其是对电路施加的优化。因此，我们希望选择一个对形式验证支持不断增长的技术栈。
• 见证生成与约束。 我们希望能够定义见证生成逻辑和约束。此外，我们希望能够将二者“拆分”为不同的模块。
• 我们还计划包括其他特性，如： 简洁电路表示、高效代码生成、参数化电路、诊断信息，和转换 & 分析友好

此外，我们希望在一个对大部分开发人员可访问的技术栈中设计 LLZK 及其周边基础设施，以便他们可以根据自己的需要对 IR 进行贡献和扩展。

LLZK： ZK 语言统一的 IR

为了解决这些挑战，Veridise 正在开发 LLZK，一种统一电路编译和安全分析的中间表示，适用于 ZK 语言。这种方法提供了两个关键好处：整合编译和统一电路分析。

整合编译

一旦 ZK 电路被编译为 IR，IR 编译器处理约束提取、重写、优化以及生成证明者和验证者的过程。因此，任何编译为 IR 的电路语言都可以免费获得这些步骤。

统一电路分析

一个设计良好的 IR 简化了可以在多个语言间重用的程序分析的开发，帮助在编译时进行错误检测和电路优化。这些分析可以被任何编译为 IR 的编程语言所访问。此外，先进的错误查找和验证工具可以利用 IR 来确保电路的正确性。在 IR 之上编写安全工具允许它们具有广泛适用性，因为它们可以针对任何编译为 IR 的程序免费。

架构

LLZK 的架构由三个部分组成：前端组件、转换和后端。让我们重新查看相同的图。

前端组件 接收用电路语言/框架编写的电路程序，并发出 LLZK AST（ 抽象语法树）。它们将使用一个提供了构建和操纵 LLZK AST 以及序列化 LLZK AST 到文件中 LLZK 的中间表示语言的库。

转换 组件定义了诸如优化、模块扁平化、约束重写等转换过程。

后端 组件接收生成的 IR 程序，并为目标后端发出程序，例如，将 IR 代码转换为特定算术化格式的约束或其他后端工具（如静态分析器或验证引擎）所需的 IR。

技术方法和实施概览

Veridise 将使用 **MLIR**（多级中间表示）框架开发 LLZK，该框架是一种广泛采用的编译器基础设施。MLIR 的结构化方法将实现高效的电路转换、分析和优化。

我们将首先开发 LLZK 库，定义核心 IR 结构，并提供电路编译和优化的工具。接下来，我们将与现有的 ZK 语言进行集成，并建立前端来支持关键的电路 DSL。最后，我们将开发一个安全分析后端，并将 LLZK 转换为与 Picus 等验证工具兼容的格式，以实现自动化安全检查。

开源 LLZK 和未来的道路

我们感谢以太坊基金会对 LLZK 开发的资金支持。在他们的支持下，我们激动地加快我们的努力，使 LLZK 成为 ZK 电路开发人员的基础工具。

通过减少碎片化并启用更广泛的安全工具，LLZK 将帮助加强 ZK 生态系统，并使零知识应用更安全、更容易维护。

我们将开源 LLZK，并积极与更广泛的 ZK 和以太坊社区互动。我们邀请开发人员、研究人员和安全分析师在 LLZK 成形的过程中贡献和提供反馈。

请关注我们的 GitHub 更新，并关注我们的最新进展！

LLZK 演示

在 ZK Accelerate 会议上，Jon Stephens 的演示中了解有关 LLZK 的更多信息。

https://www.youtube.com/watch?v=MHtSOV7JZ1c

作者：

Shankara Pailoor，Veridise 的 ZK 安全主管

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