Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Clap: a Semantic-Preserving Optimizing eDSL for Plonkish Proof Systems

Marco Stronati, Denis Firsov, Antonio Locascio, Benjamin Livshits

TL;DR

Clap addresses the fragility and manual complexity of Plonkish circuits used in production ZK systems by providing a Rust eDSL that semantically preserves the translation from circuits and witness generators to Plonkish constraint systems. It introduces a formal framework with an Agda model proving soundness and completeness, plus five automatic optimizations and a flattening-based approach to generate custom gates, enabling back-end flexibility. Experimental evaluation on Poseidon2 and SHA-256 shows Clap yields safer, more readable circuits with up to 10% fewer constraints than hand-optimized baselines and removes historically unsafe patterns. This work offers a principled, modular pathway for evolving Plonkish proofs with strong correctness guarantees and practical performance benefits for high-stakes zk-rollup deployments.

Abstract

Plonkish is a popular circuit format for developing zero-knowledge proof systems that powers a number of major projects in the blockchain space, responsible for holding billions of dollars and processing millions of transactions per day. These projects, including zero-knowledge rollups, rely on highly hand-optimized circuits whose correctness comes at the cost of time-consuming testing and auditing. In this paper, we present Clap, the first Rust eDSL with a proof system agnostic circuit format, facilitating extensibility, automatic optimizations, and formal assurances for the resultant constraint system. Clap casts the problem of producing Plonkish constraint systems and their witness generators as a semantic-preserving compilation problem. Soundness and completeness of the transformation guarantees the absence of subtle bugs caused by under- or over-constraining. Our experimental evaluation shows that its automatic optimizations achieve better performance compared to manual circuit optimization. The optimizer can also be used to automatically derive custom gates from circuit descriptions.

Clap: a Semantic-Preserving Optimizing eDSL for Plonkish Proof Systems

TL;DR

Clap addresses the fragility and manual complexity of Plonkish circuits used in production ZK systems by providing a Rust eDSL that semantically preserves the translation from circuits and witness generators to Plonkish constraint systems. It introduces a formal framework with an Agda model proving soundness and completeness, plus five automatic optimizations and a flattening-based approach to generate custom gates, enabling back-end flexibility. Experimental evaluation on Poseidon2 and SHA-256 shows Clap yields safer, more readable circuits with up to 10% fewer constraints than hand-optimized baselines and removes historically unsafe patterns. This work offers a principled, modular pathway for evolving Plonkish proofs with strong correctness guarantees and practical performance benefits for high-stakes zk-rollup deployments.

Abstract

Plonkish is a popular circuit format for developing zero-knowledge proof systems that powers a number of major projects in the blockchain space, responsible for holding billions of dollars and processing millions of transactions per day. These projects, including zero-knowledge rollups, rely on highly hand-optimized circuits whose correctness comes at the cost of time-consuming testing and auditing. In this paper, we present Clap, the first Rust eDSL with a proof system agnostic circuit format, facilitating extensibility, automatic optimizations, and formal assurances for the resultant constraint system. Clap casts the problem of producing Plonkish constraint systems and their witness generators as a semantic-preserving compilation problem. Soundness and completeness of the transformation guarantees the absence of subtle bugs caused by under- or over-constraining. Our experimental evaluation shows that its automatic optimizations achieve better performance compared to manual circuit optimization. The optimizer can also be used to automatically derive custom gates from circuit descriptions.
Paper Structure (34 sections, 6 equations, 16 figures)

This paper contains 34 sections, 6 equations, 16 figures.

Table of Contents

  1. Introduction
  2. Motivating Example
  3. This Work
  4. Contributions
  5. Paper Organization
  6. From Programs to Proofs
  7. Circuits and Witness Generators
  8. Circuits and Gates
  9. Circuit Semantics
  10. Oracles and Non-Fully-Constrained Traces
  11. Constraint Systems and Their Satisfiability
  12. A Sample of Constrained Vectors
  13. Compilation
  14. Tabulation
  15. Semantic Preservation
  16. ...and 19 more sections

Figures (16)

  • Figure 1: Example: chained gates.
  • Figure 2: From programs to proofs, Clap in orange, proof system in green.
  • Figure 3: Type signatures for Clap's main functions.
  • Figure 4: Circuits and gates.
  • Figure 5: Example tabulation.
  • ...and 11 more figures

Theorems & Definitions (6)

  • Definition 3.1: Gates and circuits
  • Definition 4.1: Constrained vector
  • Definition 4.2: Satisfiability
  • Definition 5.1
  • Definition 5.2
  • Definition 6.1