Zero-Knowledge (ZK) proof systems are cryptographic protocols that can (with overwhelming probability) demonstrate that the pair $(X, W)$ is in a relation $R$ without revealing information about the private input $W$. This membership checking is captured by a complex arithmetic circuit: a set of polynomial equations over a finite field. ZK programming languages, like Noir, have been proposed to simplify the description of these circuits. A developer can write a Noir program using traditional high-level constructs that can be compiled into a lower-level ACIR (Abstract Circuit Intermediate Representation), which is essentially a high-level description of an arithmetic circuit. In this paper, we formalise some of the ACIR language using SMT-LIB and its extended theory of finite fields. We use this formalisation to create an open-source formal verifier for the Noir language using the SMT solver cvc5. Our verifier can be used to check whether Noir programs behave appropriately. For instance, it can be used to check whether a Noir program has been properly constrained, that is, the finite-field polynomial equations generated truly capture the intended relation. We evaluate our verifier over 4 distinct sets of Noir programs, demonstrating its practical applicability and identifying a hard-to-check constraint type that charts an improvement path for our verification framework.

翻译：零知识（ZK）证明系统是一种密码学协议，能够（以压倒性概率）证明配对$(X, W)$属于关系$R$，同时不泄露关于私有输入$W$的信息。这种成员关系检查通过复杂的算术电路实现：即有限域上的一组多项式方程。为简化此类电路的描述，人们提出了如Noir等ZK编程语言。开发者可使用传统高级编程结构编写Noir程序，这些程序可被编译为底层的ACIR（抽象电路中间表示），其本质上是算术电路的高级描述。本文利用SMT-LIB及其扩展的有限域理论，对部分ACIR语言进行了形式化建模。基于此形式化模型，我们借助SMT求解器cvc5构建了面向Noir语言的开源形式化验证器。该验证器可用于检查Noir程序的行为是否符合预期，例如验证Noir程序是否受到适当约束——即生成的有限域多项式方程是否准确捕获了预期关系。我们在4组不同的Noir程序集上评估了验证器的性能，证明了其实际适用性，并发现了一类难以检测的约束类型，这为验证框架的改进指明了方向。