Formal Verification of Bit-Vector Invertibility Conditions in Coq
Citation
Ekici, B., Viswanathan, A., Zohar, Y., Tinelli, C., & Barrett, C. (2023, September). Formal Verification of Bit-Vector Invertibility Conditions in Coq. In International Symposium on Frontiers of Combining Systems (pp. 41-59). Cham: Springer Nature Switzerland.Abstract
We prove the correctness of invertibility conditions for the theory of fixed-width bit-vectors—used to solve quantified bit-vector formulas in the Satisfiability Modulo Theories (SMT) solver cvc5— in the Coq proof assistant. Previous work proved many of these in a completely automatic fashion for arbitrary bit-width; however, some were only proved for bit-widths up to 65, even though they are being used to solve formulas over larger bit-widths. In this paper we describe the process of proving a representative subset of these invertibility conditions in Coq. In particular, we describe the BVList library for bit-vectors in Coq, our extensions to it, and proofs of the invertibility conditions.
