Automating Bitvector and Finite Field Equivalence Proofs in Lean
The work
| Authors | Elizaveta Pertseva; Valentin Robert; Clark Barrett; James Parker |
|---|---|
| Editors | |
| Type | misc |
| Year | 2026 |
| Citekey | pertseva2026automating |
Identifiers
| arXiv | 2605.15163 from its landing_page_url |
|---|
Access
| Landing page | https://arxiv.org/abs/2605.15163 |
|---|
Related
| Distinct from | dai2026guarded |
|---|---|
| Distinct from | smith2024scaling |
From bibtex.
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 percent more ZKP arithmetization benchmarks.
A copy is held
pdf, 809.5 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-09-17 17:03 UTC |
| Approved by | a person 2026-09-17 17:03 UTC |
Filed under
Cite it as
@misc{pertseva2026automating,
title = {Automating Bitvector and Finite Field Equivalence Proofs in Lean},
author = {Elizaveta Pertseva and Valentin Robert and Clark Barrett and James Parker},
year = {2026},
}
This record lives at https://refs.drheap.org/pertseva2026automating/ and will keep doing so.