Writing Plonkish constraint systems by hand is tedious and error-prone; as a result, several libraries and DSL's have emerged over the years to facilitate this task as well as techniques to directly analyze constraint systems. However, standalone languages require developers to use a foreign toolchain and leave gaps between the application and its circuits. On the other hand, Rust-embedded DSL like Halo2 or Boojum lack in modularity; furthermore, it is usually impossible to tease apart the circuit from the proof system, making it hard to reuse circuits and even to compare performance of different proof systems on the same circuits. In this paper we introduce Clap, the first Rust eDSL to propose a prover-agnostic circuit format that enables extensibility, automatic optimizations, and formal guarantees for the resulting constraint system. Clap generates Plonkish constraint systems and witness generators that are sound and complete with respect to each other, leaving no room for subtle bugs due to under- or over-constraining. A model of this equivalence is proved in the Agda proof assistant for a subset of Clap's Rust implementation that is expressive enough to capture the compositional properties of our format. In order to increase the reuse of circuits, a number of optimizations are carried out automatically, sparing the developer from over-specifying low-level constraint system details in their circuit descriptions. We test the expressivity and efficiency of Clap on an implementation of the Poseidon2 hash function that produces a constraint system that is competitive in terms of size with hand-optimized Boojum circuits.

翻译：手动编写PlonKish约束系统繁琐且易出错；为此，近年来涌现出多种库和领域特定语言（DSL）以简化此任务，并开发了直接分析约束系统的技术。然而，独立语言要求开发者使用外部工具链，并在应用与其电路之间留下鸿沟。另一方面，Halo2或Boojum等Rust嵌入式DSL缺乏模块化，且通常无法将电路与证明系统分离，导致电路难以复用，甚至难以在同一电路上比较不同证明系统的性能。本文提出Clap——首个提出与证明器无关的电路格式的Rust eDSL，该格式支持可扩展性、自动优化以及为最终约束系统提供形式化保证。Clap生成的Plonkish约束系统与见证生成器相互间具有可靠性和完备性，从而避免了因约束不足或过度约束导致的细微错误。我们在Agda证明辅助工具中为Clap的Rust实现子集验证了这种等价性的模型，该子集具有足够的表达能力以捕获我们格式的组合性质。为提升电路复用性，多项优化被自动执行，开发者无需在电路描述中过度指定底层约束系统的细节。我们通过在Poseidon2哈希函数实现上测试Clap的表现力与效率，其生成的约束系统在规模上与手工优化的Boojum电路不相上下。