Automating Bitvector and Finite Field Equivalence Proofs in Lean

TL;DR

This paper introduces a new Lean tactic, BitModEq, which improves the verification of Zero-Knowledge Proof circuit encodings involving bitvector and finite field operations, outperforming SMT solvers.

Contribution

The paper presents a novel Lean tactic that automates finite field to bitvector translations, enhancing verification efficiency for ZKP circuits.

Findings

Outperforms SMT solvers on 19% more benchmarks

Leverages range lemmas and case analysis for verification

Enables verified translations from finite fields to bitvectors

Abstract

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.