Tabby：一种用于高性能零知识证明电路的合成辅助编译器

《Proceedings of the ACM on Programming Languages》：Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits

零知识证明应用需要将高级程序转换为高效算术电路，现有方法存在次优电路和手工优化困难的问题。本文提出Tabby编译器，通过领域特定中间表示和基于草图的程序合成技术，自动生成高性能电路，同时保证正确性。实验表明其证明生成时间减少30%以上，电路规模缩小50%以上。

　　

摘要

零知识证明（ZKP）应用需要将高级程序转换为算术电路——这一过程既要求正确性，也要求效率。尽管最近的DSL（领域特定语言）提高了可用性，但它们生成的电路往往不够理想，而手工优化的实现仍然难以构建和验证。我们提出了Tabby，这是一种基于综合技术的编译器，能够自动从高级代码生成高性能的ZKP电路。Tabby引入了一种专为符号推理设计的领域特定中间表示，并应用基于草图的程序综合方法来生成优化的低级实现。通过将程序分解为可重用的组件，并通过基于SMT（符号模型检测）的推理来验证语义等价性，Tabby在确保正确性的同时显著提升了性能。我们在一系列实际ZKP应用中对Tabby进行了评估，发现与主流ZKP编译器相比，其证明生成时间和电路规模都有显著降低。