OOPSLA

Certified Decision Procedures for Width-Independent Bitvector Predicates

Bitvectors are foundational for automated reasoning. A few interactive theorem provers (ITP), such as Lean, have strong support for deciding fixed-width bitvector predicates by means of bitblasting. However, even these ITPs provide little automation for width-independent bitvector predicates. To fill this gap, we contribute novel, mechanized decision procedures for width-independent bitvector predicates in Lean. Classical algorithms to decide fragments of width-independent bitvector theory can be viewed from the lens of model checking, where the formula corresponds to an automaton and the correctness of the formula is a safety property. However, we cannot currently use this lens in mechanized proofs, as there are no executable, fast, and formally verified model checking algorithms that can be used interactively from within ITPs. To fill this gap, we mechanize key algorithms in the model checking literature: k-induction, automata reachability, automata emptiness checking, and automata minimization. Using these mechanized algorithms, we contribute scalable, mechanized, decision procedures for width-independent bitvector predicates. Furthermore, for controlled fragments of mixtures of arithmetic and bitwise operations which occur in the deobfuscation literature, we mechanize a recent fast algorithm (MBA-Blast), which outperforms the more general procedures on this fragment. Finally, we evaluate our decision procedures on benchmarks from classical compiler problems such as Hacker’s Delight and the LLVM peephole optimizer, as well as on equivalence checking problems for program obfuscation. Our tools solve 100\% of Hacker’s Delight, two of our tools solve 100\% of the deobfuscation dataset, and up to 27\% of peephole rewrites extracted from LLVM’s peephole rewriting test suite. Our new decision procedures provide a push-button experience for width-independent bitvector reasoning in interactive theorem provers, and, more broadly, pave the way for foundational algorithms for fast, formally verified model checking.