AC⁴: Algebraic Computation Checker for Circuit Constraints in Zero-Knowledge Proofs

The construction of arithmetic circuits is plagued by two critical challenges: overconstrained and underconstrained circuits. Programmer-authored circuits, even from seasoned ZKP developers, often bear inadvertently miscalibrated constraints, leading to these issues. While completely eradicating these issues remains a persistent hurdle, current approaches fall short of effectiveness. This subsection tackles this double-edged sword head-on, proposing a novel approach to ensure the construction of robust and reliable arithmetic circuits.

In our method, categorization is essential to account for the different types of variables in arithmetic circuits. Variables can be classified based on their source: some are determined by external inputs, while others depend on internal variables. It is also important to categorize variables according to their degree. Due to the computational complexity of verifying certain circuits, we can only provide coarse-grained results. This limitation underscores the importance of categorizing the outcomes as well.

The three types of constraints to consider are precise linear equations, $K$-coefficient linear constraints, and higher constraints. A precise linear constraint is defined by having linear generator variables with constant coefficients. Conversely, a $K$-coefficient linear equation includes at least one generator variable with a coefficient represented by the known variables $K$, and none of the generator variables’ coefficients are represented by the unknown variables $U$. Lastly, a higher equation is distinguished by containing at least one generator variable with a coefficient represented by the unknown variables $U$.

The system of constraints, namely circuits, can be categorized into three types based on the constraints outlined above: precise linear circuits, $K$-coefficient circuits, and higher-order circuits. A precise linear circuit consists solely of precise linear constraints, while a $K$-coefficient circuit must contain at least one $K$-coefficient linear constraint and no higher-order constraints. Finally, a higher-order circuit should include at least one higher-order constraint.

This section demonstrates the reduction of the under/overconstrained problems of a circuit to the number of solutions of the corresponding polynomial equations.

To reduce the circuit constraint problems to the number of solutions of polynomials, we have the following proposition:

A bijection can be constructed between the formal variables of polynomials and the variables of a circuit because their domain is the same finite field $\mathbb{F}$. The meta operator set $O_{c}$ of polynomial circuits is $\{+,\times,\sim\}$ ¹¹1$\sim$ is the complementary operation on finite fields and the meta operator set $O_{p}$ of a polynomials are $\{+,\times,\sim\}$, so $O_{c}=O_{p}$. Because the additive group over finite fields is an Abelian group under ‘+’, the operation of shifting the terms does not change the properties of the original variables and constraints. However, a constraint of a polynomial circuit can only be constant, linear, or higher, while polynomials exceed the limit of the degree of variables. Consequently, the constraints of a polynomial circuit are a subset of polynomials.

Based on the argument above, completely checking the constraint status of circuits can be achieved by solving polynomials. More concretely, the constraint problem corresponds to figuring out the number of solutions for polynomials.

Fig. 1 illustrates the overall workflow of our proposed tool, $\text{AC}^{4}$, which receives a Circom program file as the input, and compiles the program in debug mode into an R1CS format file along with a sym file. To retrieve the variables and constraints from the compiled files, a task-specific parser is implemented to handle those compiled files, focusing on unknown variables within constraints. After that, the extracted constraints are then simplified into equations. A categorizing mechanism is leveraged in Section 3.2 to determine the specific category of the circuit according to its simplified equation system. Based on the category result of circuits, three types of solvers is employed to address them respectively.

In the context of a precisely pure linear circuit, the system of linear equations can be represented in matrix form. While it may seem natural to rely on rank to determine the number of solutions, it is more important to prioritize verifying the uniqueness of the output variable set. Therefore, solving the system demands a suitable method for linear equations. Specifically, in $\text{AC}^{4}$, the Gauss-Jordan method[51] is utilized to obtain the solution of the circuits as well as to ascertain the uniqueness of the set of output variables.

The system of $K$-coefficient linear equations corresponding to an algebraically linear circuit can be represented in matrix form. However, it is imperative to note that algebraic computation does not inherently account for the division by zero problem. Consequently, for certain specific inputs $I$, the rank of the matrix may decrease, potentially altering the outcome of $\text{AC}^{4}$. Rank reduction risks are mitigated by strategically identifying and treating special input cases. Our approach addresses this challenge through heuristic approaches to improve the efficiency and accuracy.

For higher-order circuits, we solve the coefficients and verify if the circuit will be underconstrained with specific inputs. Then, we use $\text{AC}^{4}$ to directly solve the systems of polynomial equations with Gröebner basis[18] and check the uniqueness of the output variables.

Here, an example will be used to demonstrate our workflow and enhance readers’ comprehension. The template in Fig. 2 refers to the Circom circuit Decoder, which converts a w-ary number into a one-hot encoded format.

Upon setting $w=2$, the Decoder(2) emerges as a 2-bit decoder. This circuit is then transformed into a format denoted as $C(K,U,O,E$, where the sets are defined as follows: $K=\{inp\}$, $U=\{out_{1},out_{2},success\}$, $O=\{out_{1},out_{2},success\}$, and $E=\{out_{0}\times inp=0,out_{1}\times(inp-1)=0,success\times(success-1)=0\}$.

Based on the classification of circuits mentioned above, it is evident that this circuit is not linear. To analyze this, we begin by treating the variable $inp$ as a coefficient and proceed to solve for the undetermined coefficients of each equation. This process yields the solutions $[\{inp=0\},\{inp=1\}]$. When substituting $\{inp=0\}$ into $E$, the resulting equations are $E=\{0=0,out_{1}\times(inp-1)=0,success\times(success-1)=0\}$. Notably, $out_{0}$ can take on any value over the finite field, indicating that the circuit is underconstrained.

AC⁴ is designed to provide precise results when analyzing circuits. However, when dealing with large or complex circuits, it might produce an “unknown” outcome due to the scalability. To handle these situations, AC⁴ relaxes its strict checking conditions and instead returns partial, but still meaningful, results.

In certain cases, the input coefficients in circuit equations can be difficult to determine as zero or non-zero. To simplify, AC⁴ treats all combinations of input and constant values as non-zero, allowing for a more straightforward algebraic result. For example, in an equation like $(\text{input coefficients})\times\text{out}=1$, AC⁴ assumes the input coefficients are non-zero, so the output becomes $\frac{1}{\text{input coefficients}}$. This yields a workable solution, even if not fully precise. Under this assumption, the overconstrained and exact-constrained results may not align with the actual situation of the circuits. We name the former as algebraic results. In contrast, by precisely, we mean that the result are directed obtained without the above assumption. Hence, as depicted in Fig. 3, AC⁴ generates five practical categories of results: algebraic overconstrained, precisely overconstrained, algebraic exact-constrained, precisely exact-constrained, and precisely underconstrained.

While its primary objective is to provide precise results during circuit analysis, AC⁴ recognizes the challenges posed by large circuits with numerous parameters. In such scenarios, where a precise result may be unattainable, AC⁴ adjusts its approach by relaxing the strictness of its checking conditions. This adaptability enables AC⁴ to yield a meaningful partial result, ensuring that even with complex circuits, users can still gain valuable insights into the circuit’s behavior.

To provide more detailed feedback on unsolvable circuits, AC⁴ refines its result classification. It introduces two intermediate categories, algebraic exact-constrained and algebraic overconstrained, which offer additional insights. These categories help analysts understand whether a circuit may be underconstrained (too flexible) or overconstrained (no valid solutions) by examining the algebraic structure of the equation matrix.

The relationship between AC⁴’s results and the actual circuit behavior is also cross-referenced with ground truth. Three categories—precisely underconstrained, precisely exact-constrained, and precisely overconstrained-directly correspond to whether a circuit is under, exact or overconstrained. However, the algebraic categories offer more nuanced information. For example, an algebraically exact-constrained circuit might be either underconstrained or exact-constrained in reality, while algebraic overconstrained cases could actually be exact-constrained or overconstrained.

Unknown results may stem from circuit size, computational complexity, or the inherent NP-hardness of solving polynomial equations over finite fields.

By relaxing the strict checking conditions, AC⁴ can filter out cases that are definitely under or overconstrained, providing more efficient and useful results even when a full solution isn’t possible.

From above, we divide the overall circuit verification problem space into three types: precisely linear, $k$-coefficient linear, and higher-order separately. In this section, we introduce those algorithms in detail.

Although in nature, these equations are considered linear due to their higher-order terms containing one or more known variables, Hence, they are treated as linear circuits and represented in matrix form to enhance verification efficiency. For these circuits, we still use the previous heuristic approach given in Algorithm 2, to determine if there are special inputs that can cause the underconstrained condition, aiming to enhance efficiency. Afterwards, a $k$-coefficient linear circuit can be succinctly represented by a coefficient matrix $A$ and a constant vector $b$, and checked as a linear case. The pseudo-code of checking $k$-coefficient circuits is given in Algorithm4.

This section examines the time complexity associated with each category of circuits. For linear circuits, including those characterized by $K$-coefficient linear circuits, the Gauss-Jordan elimination method has a time complexity of $O(n^{3})$ [3]. Our statistical analysis of Circomlib [32] indicates that the majority of cases involve linear circuits. Consequently, we anticipate that our algebraic-based method will significantly enhance performance compared to SMT solvers. In the case of higher-order circuits, we employed the $F_{5}$ algorithm, which is designed for computing Gröbner bases.[23] This algorithm typically exhibits $O(2^{n})$ or $O(2^{2^{n}})$ time complexity in the worst-case scenarios. However, the $F_{5}$ algorithm demonstrates substantial improvements over its predecessors, such as Buchberger’s algorithm[18] and the $F_{4}$ algorithm.

Furthermore, we established a benchmark to evaluate the effectiveness and accuracy of AC⁴ and the halo2-analyzer[31], as implemented in the study by Soureshjani et al. (2023) [52]. This benchmark was constructed using a dataset of classical halo2 circuits, which were collected from various GitHub projects.

The primary benchmark focuses on circom datasets, while our results also demonstrate improvements on halo2 datasets compared to other tools.

On the other hand, we propose a more relaxed metric, $AS$ (Algebraic Solved), by remapping cases that failed to obtain precise results into two new categories: algebraic exact-constrained and algebraic overconstrained, to reject overconstrained and underconstrained respectively. Note that $\text{AC}^{4}$ still returns unknown for extremely computationally exhausting cases.

We categorize circuits based on their constraint numbers in Table 2, considering those with a constraint number less than 100 as “small” circuits, those with a constraint number in the range $[100,1000)$ as “medium” circuits, and those with a constraint number in the range $[1000,\infty)$ as “large” circuits. This classification, which may be rudimentary, does not consider output signals. It is evident that small circuits can be solved directly, whereas other circuits may require specific restrictions to be solved within an acceptable time frame.

Fortunately, the majority of practical Circom circuits are of the precisely linear type. This characteristic is advantageous because medium or large circuits that are not precisely linear cannot be solved directly due to unknown outcomes. Therefore, alternative methods must be utilized to bypass the direct solution of non-linear circuits. Additionally, providing a more accurate range to determine whether to solve the circuits can help avoid obtaining algebraically solved results. This approach is crucial for maintaining clarity and precision in circuit analysis.

Heuristic algorithms initially assess potential underconstraint in quadratic circuits. We then apply classic algorithms for solving quadratic equations over finite fields to obtain direct solutions. Moreover, in the case of specific binary circuits such as BinSum and Num2Bits, a detection method is utilized to verify the boolean nature of unknown variables. Upon confirmation, a specialized method for solving binary circuits is employed in lieu of arithmetic-based approaches. Most circuits are thoroughly verified before processing.

In the paper [46], Picus, an implementation of the tool $\textbf{QED}^{2}$, is utilized for verifying the uniqueness property (under-constrained signals) of ZKP circuits. This implementation employs static program analysis and SMT solvers checking to achieve the verification of the uniqueness of ZKP circuits. Subsequently, we benchmarked the Picus program using the same benchmark set.

The completed Picus ratio for the utils benchmark set is 80.33%, for the core benchmark set it is 62.61%, and for both sets it is 69.36%. Additionally, the average solving time for the Picus solver is 425.73 seconds for the utils benchmark set, 317.88 seconds for the core benchmark set, and 365.52 seconds for both sets.

The comparison of the two tools based on the solved ratio can be found in Fig. 4b. Our advantage lies in precisely linear cases as well as some heuristic methods for $k-$coefficient and binary cases.Fig. 4b shows the solving time comparison of the two tools.

Given the current dearth of comprehensive research on halo2 circuits and the absence of template circuits provided by the official Zcash organization, we undertook the task of extracting 10 of the most frequently utilized halo2 circuit types from GitHub repositories dedicated to halo2 projects. These extractions were subsequently employed to construct a relevant dataset. Utilizing this custom-curated dataset, we conducted benchmark analyses in conjunction with the halo2-analyzer.

As shown in figure 5, AC⁴ demonstrates a enhancement in efficiency and accuracy compared to halo2-analyzer, exhibiting a 26.73% improvement in the verification time and 10% improvement in the checked ratio for halo2 circuits.

Table 3 illustrates a significant correlation between the size of the circuit and the time required for checking. Despite their size, large circuits keep checking times low due to two critical factors. Firstly, the predominance of linear circuits, efficiently addressed by the Gauss-Jordan solver, contributes to the efficiency in solving a majority of cases. Additionally, optimizations targeting binary cases within k-coefficient and higher-order circuits serve to further reduce the solving time despite their slightly larger size.

The checked ratio is high for precisely linear cases; however, there are some cases for which we cannot provide precisely checked results due to the lack of an algebraic solution. Special input scenarios can reduce the augmented matrix’s rank, yielding a solution. In contrast, for the $K$-coefficient cases, the checked ratio is relatively low, even when a mixed solver is employed. This is because we did not implement certain static analysis methods to elaborate the benchmark set, which would have facilitated the checking of circuits. Conversely, the checked ratio is relatively high for quadratic cases, as most of these cases are in binary form. The detection method and optimization for binary quadratic circuits have significantly enhanced efficiency in checking these cases.

In the context of quadratic cases, Picus and halo2-analyzer employ the cvc5-ff-range solver. This solver first implements finite field theory and then utilizes Buchberger’s algorithm along with triangular decomposition to simplify polynomial equations. To address the problem, it further applies Collins’ cylindrical algebraic decomposition (CAD) [22] [43]. It is important to note that the time complexity of CAD is $O(2^{2^{n}})$, which can be prohibitive in many scenarios involving large quadratic cases. Additionally, the $F_{5}$ algorithm demonstrates superior performance over modular integers in various cryptographic challenges.