Sound and Complete Solving for Multi-width Parametric Bitvectors via Principled Reductions

Bitvectors are foundational for automated reasoning about programs, and fixed-width bitvector solvers (QF_BV) are fast and ubiquitous. However, the theory of parametric bitvectors (PBV), where widths are symbolic, is much less well understood. The theory of multi-width PBV, where expressions may involve n distinct symbolic widths (PBV_n), is particularly challenging. The only existing complete approach for bounded PBV (where all widths have a concrete upper bound) is exhaustive enumeration, requiring one call to a QF_BV solver for each of the exponentially many possible width assignments. This is a significant bottleneck in tools, such as Alive2 and Hydra, that formally reason about compiler optimizations. To address this problem, we first prove that any PBV_n formula can be reduced to an equisatisfiable mono-width (PBV_1) formula with only a linear increase in formula size. The key idea is to encode symbolic widths as bitmasks. This reduction lets us create two solvers for flavors of multi-width PBV. (1) A sound and complete bounded PBV solver, which instantiates the width variable in the PBV_1 formula to a concrete bound, and therefore requires only a single QF_BV solver call. In practice, this solver proves LLVM rewrites in seconds that enumeration fails to prove in hours. (2) By composing our reduction with existing automata-theoretic decision procedures for PBV_1, we obtain a new sound and complete decision procedure for a fragment of PBV_n with parametric widths. This new decidable fragment subsumes the prior state-of-the-art fragment of linear and bitwise operations, by adding support for zero and sign extension. All our solvers are implemented in Lean, with mechanized proofs of soundness and completeness for the unbounded solver. Empirically, we find that our equisatisfiable reduction from PBV_n to PBV_1 turns exponential enumeration into a single QF_BV query that nearly saturates standard PBV benchmarks (506 of 528 problems across all datasets), while our unbounded solvers solve 1.5x as many problems as the state of the art CVC5-based solver for all bitwidths.