Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

AC4: Algebraic Computation Checker for Circuit Constraints in ZKPs

Qizhe Yang, Boxuan Liang, Hao Chen, Guoqiang Li

TL;DR

The paper tackles the reliability of zk-SNARK arithmetic circuits by addressing underconstrained and overconstrained constraints. It introduces AC4, which encodes circuit constraints as polynomial systems over finite fields and solves them with computer algebra, coupled with category-based adaptive checking. Key contributions include a formal reduction of circuit verification to polynomial solution counting, a practical AC4 framework with five result categories, and extensive evaluations on Circom and halo2 benchmarks showing improved solved-rate and competitive checking times. This approach demonstrates the viability of algebraic computation for robust ZK circuit verification and outlines future work in static analysis, larger datasets, and specialized solvers.

Abstract

Zero-knowledge proof (ZKP) systems have surged attention and held a fundamental role in contemporary cryptography. Zero-knowledge succinct non-interactive argument of knowledge (zk-SNARK) protocols dominate the ZKP usage, implemented through arithmetic circuit programming paradigm. However, underconstrained or overconstrained circuits may lead to bugs. The former refers to circuits that lack the necessary constraints, resulting in unexpected solutions and causing the verifier to accept a bogus witness, and the latter refers to circuits that are constrained excessively, resulting in lacking necessary solutions and causing the verifier to accept no witness. This paper introduces a novel approach for pinpointing two distinct types of bugs in ZKP circuits. The method involves encoding the arithmetic circuit constraints to polynomial equation systems and solving them over finite fields by the computer algebra system. The classification of verification results is refined, greatly enhancing the expressive power of the system. A tool, AC4, is proposed to represent the implementation of the method. Experiments show that AC4 demonstrates a increase in the solved rate, showing a 29% improvement over Picus and CIVER, and a slight improvement over halo2-analyzer, a checker for halo2 circuits. Within a solvable range, the checking time has also exhibited noticeable improvement, demonstrating a magnitude increase compared to previous efforts.

AC4: Algebraic Computation Checker for Circuit Constraints in ZKPs

TL;DR

The paper tackles the reliability of zk-SNARK arithmetic circuits by addressing underconstrained and overconstrained constraints. It introduces AC4, which encodes circuit constraints as polynomial systems over finite fields and solves them with computer algebra, coupled with category-based adaptive checking. Key contributions include a formal reduction of circuit verification to polynomial solution counting, a practical AC4 framework with five result categories, and extensive evaluations on Circom and halo2 benchmarks showing improved solved-rate and competitive checking times. This approach demonstrates the viability of algebraic computation for robust ZK circuit verification and outlines future work in static analysis, larger datasets, and specialized solvers.

Abstract

Zero-knowledge proof (ZKP) systems have surged attention and held a fundamental role in contemporary cryptography. Zero-knowledge succinct non-interactive argument of knowledge (zk-SNARK) protocols dominate the ZKP usage, implemented through arithmetic circuit programming paradigm. However, underconstrained or overconstrained circuits may lead to bugs. The former refers to circuits that lack the necessary constraints, resulting in unexpected solutions and causing the verifier to accept a bogus witness, and the latter refers to circuits that are constrained excessively, resulting in lacking necessary solutions and causing the verifier to accept no witness. This paper introduces a novel approach for pinpointing two distinct types of bugs in ZKP circuits. The method involves encoding the arithmetic circuit constraints to polynomial equation systems and solving them over finite fields by the computer algebra system. The classification of verification results is refined, greatly enhancing the expressive power of the system. A tool, AC4, is proposed to represent the implementation of the method. Experiments show that AC4 demonstrates a increase in the solved rate, showing a 29% improvement over Picus and CIVER, and a slight improvement over halo2-analyzer, a checker for halo2 circuits. Within a solvable range, the checking time has also exhibited noticeable improvement, demonstrating a magnitude increase compared to previous efforts.
Paper Structure (18 sections, 1 theorem, 2 equations, 5 figures, 3 tables, 4 algorithms)

This paper contains 18 sections, 1 theorem, 2 equations, 5 figures, 3 tables, 4 algorithms.

Table of Contents

  1. Introduction
  2. Background
  3. Problem Statements
  4. Constraint Problems
  5. Categories of Elements
  6. Problem Reduction
  7. Methodology
  8. AC4 Framework
  9. Adaptive Checking with Relaxation and Partial Results
  10. Checking Circuits: Category-Based Algorithms
  11. Complexity Analysis
  12. Evaluations
  13. Environment Setting and Metrics
  14. Detailed Evaluation over Circom Circuits
  15. Evaluation over Halo2 Circuits
  16. ...and 3 more sections

Key Result

proposition thmcounterproposition

For each circuit $A = \langle C(X), e \rangle \in \langle C(\mathcal{X}), E \rangle$, there exists $A^{\prime} \in \mathbb{F}[X_1, \ldots, X_k]$, such that $A^{\prime} = \mathbb{M}(A)$ , where $\mathbb{M}$ is a bijection function from a circuit to polynomial equations over finite fields.

Figures (5)

  • Figure 1: The framework of AC4.
  • Figure 2: Binary to One-Hot Decoder Circuit
  • Figure 3: The category of results from AC4
  • Figure 4: The checking time and solved rate comparisons between $\text{AC}^4$, Picus and Civer
  • Figure 5: The checking time and solved rate comparisons between $\text{AC}^4$ and halo2-analyzer

Theorems & Definitions (7)

  • definition thmcounterdefinition: Arithmetic circuit pmlr-v49-volkovich16
  • definition thmcounterdefinition: Constraint in Circom
  • definition thmcounterdefinition: Constraint in halo2
  • remark thmcounterremark
  • definition thmcounterdefinition: Arithmetic circuit with constraints
  • definition thmcounterdefinition: Polynomials over finite fields
  • proposition thmcounterproposition: Circuit-Poly Reduction