Verifying Bit-vector Invertibility Conditions in Coq

Results Verified all equivalences for n = 1 to 65 Verified ≈75% of equivalences Verified 18 equivalences • The CVC4 SMT-solver uses invertibility equivalences to solve quantified bit-vector formulas • Proofs of these equivalences for arbitrary bit-widths certify the solver’s results Contributions Previous Work [Niemetz et al., CAV 2018] • generated 162 invertibility equivalences • proved them using SMT-solvers for bitwidths up to 65 [Niemetz et al., CADE 2019] • encoded the equivalences in theories supported by SMT-solvers • verified equivalences for parametric widths • succeeded on ≈75% of the equivalences This work 1. formalized a representative subset of the 162 invertibility equivalences in Coq 2. extended a Coq bit-vector library to support these equivalences 3. proved 18 of them for arbitrary bit-width Results