Formalizing The Theory of Bit-vectors for Integration of SMT Solvers and Theorem Provers

Lean-SMT is a tactic to integrate the Lean Theorem Prover with cvc5, a Satisfiability Modulo Theory (SMT) solver. To increase automation in Lean, the tactic will reconstruct a proof of unsatisfiability produced by cvc5 in Lean step by step. For successful proof reconstruction in Lean, every cvc5 proof rule and rewrite rule must already be a term in Lean’s library. Consequently, for cvc5’s bit-vector solver, we formalize a theory of bit-vectors in Lean. This includes formalizing a novel bit-vector representation, bit-blasting theorems, and bit-vector rewrite rules. We discuss the formalization primarily and some challenges we faced.