一句话：在 Lean 中机械化模型检测与 MBA-Blast 算法，为宽度无关位向量谓词提供可扩展的已验证判定过程。
位向量是自动推理的基础。交互式定理证明器（如 Lean）可用 bitblasting 判定固定宽度位向量谓词，但对宽度无关位向量谓词缺乏自动化。本文从模型检测视角出发，在 Lean 中机械化 k-归纳、自动机可达性、空性检查与最小化，并据此构造可扩展的已验证判定过程；针对去混淆中算术与位运算混合片段，还机械化 MBA-Blast。评估使用 Hacker's Delight、LLVM peephole 重写及混淆等价性基准：求解 100% Hacker's Delight，两个工具求解 100% 去混淆数据集，对 LLVM peephole 重写最高 27%。
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.
@article{paperbot2960,
title = {Certified Decision Procedures for Width-Independent Bitvector Predicates},
author = {Siddharth Bhat and Léo Stefanesco and Chris Hughes and Tobias Grosser},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763148}
}