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来实现该方法。实验表明，AC4在求解率上表现出显著提升，相较于Picus和CIVER提高了29%，相较于专用于halo2电路的检查器halo2-analyzer也有小幅改进。在可求解范围内，检查时间亦展现出明显改善，较先前工作实现了数量级提升。