An Effective Orchestral Approach to Satisfiability Modulo Prime Fields

TL;DR

This paper introduces a new SMT solver approach for polynomial satisfiability over prime fields, improving verification of zero-knowledge proof systems and arithmetic circuits.

Contribution

It presents a novel DPLL(T)-based method with a modular theory solver, demonstrating better performance than existing tools on relevant benchmarks.

Findings

Prototype outperforms state-of-the-art tools on ZKP verification benchmarks

New approach effectively handles polynomial constraints over prime fields

Improves formal verification techniques for zero-knowledge proof systems

Abstract

Zero-knowledge proofs (ZKPs) are an emerging technology that has become the solution to efficiently provide security and privacy along with the transparency requirement of blockchains. ZKPs are usually expressed by means of arithmetic circuits and, more generally, systems of polynomial equations in a large prime field (commonly ranging from 64-bit to 256-bit values). An increasing interest to apply formal verification techniques to ensure soundness and completeness properties of ZKP protocols has shown the need of developing powerful SMT solvers able to handle such constraint systems. In this paper we consider the problem of deciding the satisfiability of existentially quantified first-order formulas defined over polynomial equations on a prime field. We present a new DPLL($T$)-based approach in which the theory solver orchestrates several modules with different trade-offs between completeness and efficiency. We have implemented the proposed techniques in a prototype that already shows better results than existing state-of-the-art tools on both benchmarks from the domain of ZKP compiler correctness and new benchmarks coming from the verification of arithmetic circuits for ZKPs. \keywords{SMT \and Finite field \and Polynomials \and Zero-Knowledge Proofs.