Clap: a Rust eDSL for PlonKish Proof Systems with a Semantics-preserving Optimizing Compiler

手动编写 Plonkish 约束系统是繁琐且容易出错的，因此多年来出现了几个库和 DSL 来简化此任务，以及直接分析约束系统的技术。然而，独立语言需要开发人员使用外部工具链，并在应用程序和电路之间留下空白。另一方面，像 Halo2 或 Boojum 这样的 Rust 嵌入式 DSL 缺乏模块化；此外，通常无法将电路与证明系统分开，这使得重用电路甚至比较不同证明系统在相同电路上的性能都很困难。 在本文中，我们介绍了 Clap，这是第一个 Rust eDSL，提出了一个证明器无关的电路格式，实现了可扩展性、自动优化和对生成的约束系统的形式保证。Clap 生成的 Plonkish 约束系统和见证生成器彼此之间是完备和正确的，不会因为过度或不足的约束而出现微妙的错误。我们在 Agda 证明助手中证明了该等价模型，用于 Clap 的 Rust 实现子集，该子集足以捕获我们格式的组合属性。为了增加电路的重用性，自动执行了许多优化，使开发人员无需在电路描述中过度指定低级约束系统细节。我们在 Poseidon2 哈希函数的实现上测试了 Clap 的表达能力和效率，生成的约束系统在大小方面与手动优化的 Boojum 电路相当。

介绍了一种名为Clap的Rust eDSL，旨在解决手动编写Plonkish约束系统的繁琐和容易出错的问题，同时具有可扩展性、自动优化和形式保证等特点。

Clap提供了一种与证明系统无关的电路格式，可以自动生成Plonkish约束系统和证人生成器，从而实现了电路的复用和不同证明系统性能的比较。

Clap在Agda证明助手中证明了其Rust实现的等价性模型，具有自动优化电路描述的功能，以及在实现Poseidon2哈希函数时生成了与手动优化的Boojum电路具有竞争力的约束系统。

最近的相关研究包括Halo2和Boojum等Rust嵌入式DSL，以及Plonk等其他Plonkish约束系统。