Automating Bitvector and Finite Field Equivalence Proofs in Lean
For researchers verifying Zero-Knowledge Proof circuit encodings, this work provides a more automated and scalable verification method.
The paper presents a Lean tactic, BitModEq, that automates equivalence proofs combining bitvector and finite field operations, solving 19% more ZKP arithmetization benchmarks than state-of-the-art SMT solvers.
Efforts to verify Zero-Knowledge Proof circuit encodings have highlighted the challenge of proving the correctness of quantifier-free statements that make use of both bitvector and finite field operations. Existing verification workflows are either manual or rely on SMT solvers, which scale poorly on some classes of problems for reasons that include difficulties with conversion operators and challenges reasoning about inequalities. To address these limitations, we present a novel Lean tactic BitModEq that leverages range lemmas and case analysis to produce verified translations from finite fields to bitvectors. Our approach, combined with bit-blasting, outperforms state-of-the-art SMT solvers, solving 19% more ZKP arithmetization benchmarks.