目录
核心问题 一般约束
DSL 方法 ISA/VM 方法 直接方法
要点
防御性 ZKP 编译器管道设计的核心问题是:
如果有关 ZKP 的大多数通用应用需要通用的可编程隐私，那么，什么样的编译器堆栈能够让开发人员既能安全地编写程序，也能产生高效的输出呢？
由于很多东西都是程序，所以这是一个核心的问题。最终我们会得到一些证明系统，也许还会有一些不同的编译器堆栈，但这些编译器堆栈里可能有 bug，我们需要消除这些 bug 并正规地验证它们。不过，庆幸的是，与实际程序相比，证明系统和编译器堆栈的数量相对较少。
思考一下如以太坊虚拟机（EVM）和 Solidity 编译器这样类似的例子。在 EVM 和 Solidity 的早期历史中，EVM 和 Solidity 编译器都有很多 bug。通常情况下，在这个时期程序中的 bug 虽说不完全是由编译器或 EVM 中的 bug 引起，但也有相当一部分是由此引起的。彼时这些 bug 的产生并非是因为开发人员没有考虑到他们的模型，或是因没有正确编写 Solidity 代码而引起的。
但是，随着时间的推移，随着 EVM 和 Solidity 的模式开始固化，随着它们被更好的理解并且以不同的方式进行了更正式的建模，这些 bug 的出现频率已经大大下降 —— 甚至不会在 EVM 中出现，与此同时，在 Solidity 中出现的 bug 数量也非常少且大多是非常微小的 bug。
如果你到 Rekt 去看看，你就会发现：发展到现在，大多数的 bug，并非来自 Solidity 编译器或是 EVM 中的 bug，而是来自开发人员编写的代码中的 bug ——（1）有时它们是因程序本身的模型不清晰或错误（可能是开发者故意的）引起的；（2）有时它们是在使用 Solidity 语言来表达程序模型时产生的 —— 这两种情况都是开发人员层面的问题，开发人员的水平是不一致的。如果你对预防 bug 感兴趣，那么就必须关注到这一层面，因为大多数 bug 正是因开发人员的编写而导致的。
这一问题，对于涉及零知识证明系统（ZKPs）和隐私的程序来说，更是如此。因为大多数开发人员，对 ZKPs 系统的实现细节并没有全面而精细的了解。如果编译栈要求他们了解这些实现细节，以便能够安全地编写程序，那么他们编写的程序可能会有很多 bug。这是因为，密码学是非常难以理解的。如果你没有深厚的密码学背景，却同时又在写一个会涉及到密码学的复杂应用程序时，尤其如此。
显而易见的是，即使你的编译器堆栈非常安全，但它的速度不够快，且性能成本对实际的应用程序来说又太高，那么就不会有人使用它。那么，相应地，它也就无法为人们带来更安全的编译服务。
因此，文字开篇那个问题——什么样的编译器能够让开发人员既能安全地编写程序，也能产生高效的输出？可以被表达为——什么样的编译器栈能够在保证效率的同时，为开发者提供最大的编写安全保护，以便这些编译器栈能够被实际采用？
电路 /ZKP 编译器设计中存在一些不同于常规编译器设计的约束。首先，有一些非常独特的 "阈值延迟约束" —— 即，如果程序的执行时间超过了几秒钟，很多应用就变成不可接受的了。在大多数情况下，至少在用户想要隐私的情况下，用户就必须创建证明，而创建证明时的延迟是 3 秒还是 9 秒会造成非常大的用户体验差异，尽管这里相差的时间只是 3 倍。
在使用常规编译器时，为了让程序编写（见：Javascript）更加容易，你也许能够容忍这种小的差异 —— 例如，如果你正在运行一个电子表格税务计算程序，3 倍的差异的确并不是多么重要 —— 只要不过于频繁地运行该程序，用户就可以在程序运行时做其他事情。
通常，我们往往会关心常规编译器的用户交互延迟，而用户交互延迟对编译器的设计有重大影响。例如，具有自动内存管理的语言倾向于做增量内存垃圾回收，这削弱了垃圾回收的延迟；然而，较简单的垃圾回收算法则会导致不可预测的延迟峰值。
但在编写用于 ZKP 系统的电路时，这一点并不成立，因为所有的交互对于一个单独的程序来说都是非交互式的。相反，这种时候应该优化编译器，以使 Prover 总执行时间尽可能短。
另一类可能会写 bug 的人员，是我们这样的电路编译器开发人员。所以生态系统有必要至少提出一些可供重复使用的编译器组件，这些组件可以被多方共享且共同验证。为此，本文的后续部分对当前的电路编译方法进行了高层次的分类，并描述了选择它们的权衡。
这个分类法将编译方法分为三大类型，依次按以下顺序进行定义和分析。
DSL 方法
ISA/VM 方法
直接方法
DSL 方法
“DSL 方法”是生态系统开始时使用的方法。DSL 是“领域专用语言（domain-specific language）”的缩写，DSL 采用 R1CS、PLONK、AIR 之类的东西，并基于它们构建了一种语言，这种语言可以创建迭代抽象，以简化程序员的工作。这类系统中的 DSL 指令通常表现得像约束编写宏 —— 可以跟踪某些变量，进行某种简化编译，但没有中间指令集或抽象机，以及 DSL 中的指令能够直接转换为约束。
使用 DSL 方法的例子包括:
Zokrates
Circom
Snarky
Leo
Noir
Juvix Circuits
可能还有很多其他的。
注意，Noir 是后端不可知的。它会被编译为抽象的 IR，然后 IR 再被编译为 R1CS 或 Plonk 之类的语言。同样，Leo 会被编译成一个名为 Aleo 指令的 IR，这是一种类似于 Assembly 的语言，可以直接用于对约束进行细颗粒度的控制。
虽然这些语言是由不同的语法编写而来，针对不同的证明系统，但它们都遵循同样的一般方法——从一个低级约束系统开始，并在上面不断迭代抽象。
DSL 方法的优点：
编写 DSL 是相对容易的，因为可以基于约束反复构建抽象。这意味着编写 DSL 无需一个完整的单独定义的指令集或架构。
有了这种低级的控制，你可以将 DSL 作为一种更为简单方式来手动编写电路优化。这是因为，当开发者充分理解到每条指令被翻译成为怎样的约束时，他们就能轻松地对系统的性能进行估算。
DSL 方法的劣势：
DSL 不具备高级抽象的能力，至少在没有更复杂的编译器通道以及与底层约束系统分离的语义设计的的情况下是如此。
如果有许多不同的 DSL 用于不同的证明系统，那么开发者就总是需要一些证明系统专用语言的语义来编写电路，而这些 DSL 的语义与大多数开发者已知的语言的语义大为不同。
如果开发者编写的程序包括一些电路组件和一些非电路组件——它们是两种不同的语义和语言，这两者间的转换之处很可能就是引入 bug 之处。
大多数 DSL 并没有构建类型系统以对行为进行推理。因此，对于那些希望能够验证他们的程序是否符合某些正确性标准的开发者来说，需要使用外部工具来做到这一点。
学习将 DSL 编译为固定大小的电路，对于熟悉通用编程语言的开发者来说是一件相当困难的事情。因为，这要求所有计算在编译阶段都有已知的界限（例如，没有运行时可变循环条件的循环）。
DSL 方法的一个难点在于，每个 DSL 都需要一个编译器，但这个编译器是很难构建的。仅仅为了测试一个 DSL 的新想法，就需要从头构建一个新的编译器，这种负担使得探索大量的 DSL 设计变得不可行。
设计编译器基础设施来将 DSL 编译为电路，是降低构建这种编译器成本的想法之一。这些基础设施可以实现常见的优化、转换算法和抽象，它们是作为一个库来提供，使得通过基础设施来构建新编译器变得非常简单。CirC 是一个用于已存量化电路的编译器基础设施，它捕获了 ZKP/MPC/FHE/SMT/ILP 的计算模型。
ISA/VM 方法
ISA/VM（指令集架构 / 虚拟机：Instruction Set Architecture / Vritual Machine）编译方法较为复杂。ISA/VM 编译需要明确定义一个中间虚拟机和指令集架构，它位于开发者编写程序的高级语言和用于生成证明的低级 ZKP 系统之间的编译管道中。尽管可以直接编写虚拟机指令，但在一般来说开发者不会这样做（而且这些虚拟机也没有针对开发者的优化）。
编写虚拟机指令，可以用现有的指令集来完成。例如，Risc0 团队已经用 RISC-V 微架构做到了这一点。RISC-V 微架构最初是为 CPU 设计的，并没有考虑到 ZKP 系统，但 Risc0 现在已经编写出了一个与 RISC-V ISA 现有规范相兼容的适用于 RISC-V 的 STARK Prover 和 Verifier（https://github.com/risc0/risc0）。
编写虚拟机指令，也可通过定制的 VM 和专为特定证明系统而设计的高效指令集来完成。并且，有可能在虚拟机中或其它你想要有效支持的特定应用程序中，进行递归验证。例如，Cairo VM 和 Miden VM 在 STARK 中比 在 RISC-V 这样的体系结构中，能够更有效地进行证明和验证；而 Triton VM 被专门设计为使虚拟机中的递归证明验证相对便宜。
所有这些方法都对所有程序使用同一个电路，并且都支持许多高级语言（高级语言只需编译到指定的指令集），而且这些方法大多都是基于冯 - 诺伊曼架构式的机器——有堆栈、堆栈上的操作、某种形式的内存、存储、I/O，可能还有一些协同处理器或内置运算。注意，RISC-V 和 Cairo 不是基于栈的虚拟机 ——RISC-V 是寄存器机，而 Cairo 是内存机，而 Miden VM 也不是冯 - 诺依曼架构。
ISA/VM 方法的优点：
开发人员可以使用他们已经熟悉的或者比低级电路 DSL 更容易学习高级语言。
使用现有微架构，你可以重复使用任何可以编译到 RISC-V 的现有工具 —— 也就是任何可以编译到 LLVM 的东西，这几乎就是你所要关心的一切——它们都可以与 Risc0 电路、Prover 和 Verifier 一起使用。
即使是在像 Miden VM 和 Triton VM 这样的新指令集架构中，这些基于堆栈的虚拟机编译技术对于命令语言和函数语言来说都是非常知名的。编译器作者可以重复使用很多现有工作，这些工作并非是针对 ZKPs 或电路的。
开发人员在编写编译到虚拟机的代码时，可以采用与通用编程语言相似的方法，这是因为无边界的计算可以用程序来表达（程序在 Runtime 中仍必须是有界的，但在编译阶段则不然）。
ISA/VM 方法的劣势：
当把高级程序编译到一些中间指令集时，可能会有一些抽象成本，虽然还不清楚这个成本到底是什么。例如，在任何特定程序的专用电路中，当你在做堆栈运算时，这些运算都可以被更直接地检查。我们有理由预计这是非常有可能的；并且有理由预计，如若指令集架构并非专门为 ZKPs 而建立（如 RISC-V），那么就会有更高的性能惩罚。
可以说，ISA/VM 方法所提供的功能，比应用程序实际需要的功能强大得多。相应地，也正因为它的更强大，所以更加难以验证其正确性。有很多关于图灵完备性的争论，但事实上，没有人真的想要运行不会终止的 ZKP 计算。因为，在实践中，是不可能创建出这样一个证明的。这与交互世界不同 —— 大多数交互程序永远不会终止，如电子表格，因为电子表格在一个环路中接收用户的输入，并根据用户的输入采取行动，然后等待更多的输入，直到用户（或操作系统）告诉程序退出。但是，电路执行终究是会终止的。
如果你想验证 ISA/VM 方法中编译器的正确性，你必须验证从高级语言语义到中间指令的转译的正确性，以及验证实现中间 ISA/VM 的电路的正确性。另外，即使使用现有的或更强大的高级语言来进行验证，也有大量的现有工作是可供利用。
直接方法
由于缺乏更好词语，所以我们在这里把第三种方法称为直接方法。直接方法的基本想法是以某种方式直接将高级程序编译成电路。这些高级程序可以是基于 λ 算子的函数程序，也可以是某种命令语言。但无论如何，直接方法都涉及在无需中间指令集的情况下，将这种高级语言直接转化为电路。
至少对于函数式语言来说，这种转化的最佳候选项是基于 Conal Elliot 的一篇名为 《编译到类型（ “Compiling to Categories” ） 》的论文（见：http://conal.net/papers/compiling-to-categories/）。其工作原理是采取简单 λ 算子 —— 可由函数语言翻译而来，将 λ 算子操作的语义翻译成类型的语义，再将类型的语义翻译成多项式操作类型，然后将多项式操作翻译成特定的电路。
与 DSL 方法类似，直接方法使得每个程序都能生成一个独特的电路。其他类型的直接编译也是有可能的——事实上，有一种 DSL 的连续体，它们采用越来越高级的语义，越来越于这种直接编译相似。
直接编译的优点:
原则上，开发者使用高级的语言就能获得非常高的性能。这是因为，这种编译方式使得你在编译时不会丢失任何信息（例如，你无需中间堆栈操作来表示什么）。
这种方法类似于在硬件电路综合方面所做的一些现有工作，这些工作是在 ZKP 系统的背景之外的，但依然属于摩尔定律和编译器流水线的范畴，以期产生物理电路和极度并行化程序。
至少在 《编译到类型 》一文中，编译有一个非常清晰的数学模型，并且这个模型是非常易于推理和验证的。
直接编译的劣势：
至少与简单的 DSL 方法相比，编译器管道中的复杂性更高。
不能重复使用大多数的现有工具，因为核心和编译技术是新的和非标准的。
与任何涉及更高程度抽象的方法类似，开发人员可能会更加难以推理他们程序的性能。
如此多的编译器选项让人眼花缭乱。这也引发了一个问题：将会发生什么，以及相应地，现在最好往那个方向努力？
这里概述的三种方法有着不同的权衡，特别是在潜在性能、低级控制、抽象程度和创建适当工具的难度方面。也正是因为这些权衡，我们可能会看到各种方法的组合使用：其中关键的函数和小工具（例如哈希函数、Merkle 证明验证、签名检查、递归验证、其他密码学）会被直接写在低级（1）DSL 中，甚至写在原始约束中，这些会在标准库中提供；然后将它们与开发人员用（2）ISA/VM 或（3）直接编译法编译的高级语言编写的 "业务逻辑 "联系在一起。
各种方法的组合使用是非常有可能发生的，因为这是一种两全其美的方式 —— 你可以把你的 "优化了的时间"（手工优化电路的时间）用在真正需要优化的代码的关键点上（ "hot spots "上），以及用在那些其性能能够很大程度地决定程序整体性能的地方，并使用效率较低但更通用的编译管道来处理由普通开发人员编写的自定义型的"业务逻辑"。
这也类似于今天的加密系统结构 —— 实现加密协议的时候，通常（在标准化之后）有硬件支持特定的优化原语（哈希函数，加密算法），这些原语在用高级语言编写的协议中被联系在一起，而这些高级
最后，我的一个小提示是：特定标准原语和中间接口的一致和趋同，有助于促进整个生态系统摆脱重复建设工作，并可以为开发人员提供更容易的学习环境。IBC 协议就是一个很好的例子，它在这个领域的标准化工作已经取得了一定的成功，现在正被许多不同的产业链和生态系统采用
就与零知识相关的标准工作而言，zkInterface 是一个零知识互操作性标准工具，作用于不同的 ZK DSL、小工具库和证明系统之间。Anoma 正试图用 VampIR 证明系统不可知的中间多项式表示法，来为这个方向提供一点帮助，Delendum 也在探索实用的方法以完成不同证明系统之间的组合和转换。我们非常乐意了解其他标准工作，并与之合作。
【免责声明】市场有风险，投资需谨慎。本文不构成投资建议，用户应考虑本文中的任何意见、观点或结论是否符合其特定状况。据此投资，责任自负。
推荐专栏
