Automating Bitvector and Finite Field Equivalence Proofs in Lean
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2026
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866913129957425152 |
|---|---|
| author | Pertseva, Elizaveta Robert, Valentin Barrett, Clark Parker, James |
| author_facet | Pertseva, Elizaveta Robert, Valentin Barrett, Clark Parker, James |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_15163 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Automating Bitvector and Finite Field Equivalence Proofs in Lean Pertseva, Elizaveta Robert, Valentin Barrett, Clark Parker, James Logic in Computer Science 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. |
| title | Automating Bitvector and Finite Field Equivalence Proofs in Lean |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2605.15163 |