main.tex

\documentclass[conference]{IEEEtran}
\IEEEoverridecommandlockouts
% The preceding line is only needed to identify funding in the first footnote. If that is unneeded, please comment it out.
\usepackage{cite}
\usepackage{amsmath,amssymb,amsfonts}
\usepackage{graphicx}
\usepackage{textcomp}
\usepackage{xcolor}
\usepackage{tcolorbox}
\usepackage{etoolbox}
\BeforeBeginEnvironment{minted}{\begin{tcolorbox}}%
	\AfterEndEnvironment{minted}{\end{tcolorbox}}%
\usepackage{mdframed}
\usepackage{colortbl}
%\usepackage{breakurl}             % Not needed if you use pdflatex only.
\usepackage{mdframed}
\usepackage{underscore}           % Only needed if you use pdflatex.
\usepackage{xspace}
\usepackage{pifont}
\usepackage{comment}
\usepackage{listings}
\usepackage{wrapfig}
\usepackage{semantic}
\usepackage{tikz}
\usepackage{wasysym}
\usepackage{cleveref}
\def\BibTeX{{\rm B\kern-.05em{\sc i\kern-.025em b}\kern-.08em
    T\kern-.1667em\lower.7ex\hbox{E}\kern-.125emX}}
\begin{document}

\title{Verifying Bit-vector Invertibility Conditions in Coq}
\thanks{Identify applicable funding agency here. If none, delete this.}

\author
{\IEEEauthorblockN{Burak Ekici}
\IEEEauthorblockA{\textit{Computational Logic Group} \\
\textit{University of Innsbruck}\\
Innsbruck, Austria \\
burak.ekici@uibk.ac.at}
\and
\IEEEauthorblockN{Arjun Viswanathan}
\IEEEauthorblockA{\textit{Department of Computer Science} \\
\textit{University of Iowa}\\
Iowa City, USA \\
arjun-viswanathan@uiowa.edu}
\and
\IEEEauthorblockN{Yoni Zohar}
\IEEEauthorblockA{\textit{Department of Computer Science} \\
\textit{Stanford University}\\
Stanford, USA \\
yoniz@cs.stanford.edu}
\and
\IEEEauthorblockN{Clark Barrett}
\IEEEauthorblockA{\textit{Department of Computer Science} \\
\textit{Stanford University}\\
Stanford, USA \\
barrett@cs.stanford.edu}
\and
\IEEEauthorblockN{Cesare Tinelli}
\IEEEauthorblockA{\textit{Department of Computer Science} \\
\textit{University of Iowa}\\
Iowa City, USA \\
cesare-tinelli@uiowa.edu}
}

\maketitle

\input{macros.tex}

\begin{abstract}
This report describes ongoing work of verifying invertibility 
conditions for the theory of fixed-width bit-vectors, 
that are used 
to solve quantified bit-vector formulas in the 
Satisfiability Modulo Theories (SMT) solver CVC4. 
This work complements the verification 
efforts of previous work by proving a subset of these
invertibility conditions in the \coq proof assistant. 

\end{abstract}

\begin{IEEEkeywords}
bit-vectors, \coq, proof assistant, invertibility conditions
\end{IEEEkeywords}

\section{Introduction}
\label{sec:intro}
The theory of bit-vectors can be used to model problems 
in various applications such as hardware circuit analysis, 
bounded model checking, and symbolic execution. Most of 
these applications require reasoning about quantified 
formulas over bit-vectors. Few SMT solvers can deal 
with this fragment, one of which is \cvcfour. \cvcfour 
uses a quantifier 
instantiation technique to reason about quantified formulas. 
As presented in \cite{b1}, a quantifier instantiation 
method using invertibility conditions benefits from a smaller 
number of instantiations, resulting in a more efficient 
solver. An invertibility condition for a literal specifies 
the conditions under which that literal is solvable. For 
instance, $\equal{\bvadd{x}{s}}{t}$ is unconditionally solvable 
for $x$, where $x$, $s$, and $t$ are bit-vectors of the 
same sort and $\bvaddf$ is bit-vector addition. 
A general solution or inverse for $x$ is $\bvsub{t}{s}$, and 
since $x$ is always invertible, the invertibility condition 
for the literal $\equal{\bvadd{x}{s}}{t}$ is 
simply $\true$. This is represented by the equivalence 
$\equal{\bvadd{x}{s}}{t} \iff \true$. 
A more interesting case is that 
of bit-wise conjunction, which is represented by the 
equivalence 
$\equal{\bvand{x}{s}}{t} \iff \equal{\bvand{t}{s}}{t}$.
Reference \cite{b1} found 
160 of these invertibility equivalences for a 
representative set of operators and predicates from the 
bit-vector theory of the \smtlib standard 
(in the previous two examples, the operators are 
$\bvaddf$ and $\bvandf$, 
and the predicate is equality, or $\teq$) and verified them 
using SMT solvers, for bit-widths up to 65. The correctness of the quantifier 
instantiation technique that uses these equivalences,
however, assumes the equivalences to be valid in the 
theory of bit-vectors for any bit-width $n$.
The challenge of verifying these equivalences for 
bit-vectors of arbitrary bit-widths comes from 
SMT-solvers' inability to express bit-vectors over
arbitrary bit-widths. Reference \cite{b2} encoded 
these problems over the theory of non-linear arithmetic 
with uninterpreted functions. The corresponding verification 
attempt was still unable to prove over a quarter of the 
equivalences. We complement these works by proving a 
representative subset of invertibility equivalences in 
the \coq proof assistant. We extended a bit-vector 
library in Coq (\rem{cite SMTCoq}), and proved 18 invertibility equivalences.


\section{Preliminaries}
\label{prelim}
We assume the usual terminology of many-sorted 
first-order logic with equality
(see, e.g.,\rem{cite} for more details).  
We denote equality 
by $=$, and use $x\neq y$ as an abbreviation for $\neg(x=y)$.  
The signature $\sigbv$ of the \smtlib theory of fixed-width bit-vectors
includes a unique sort for each positive integer $n$,
which we denote by $\sortbv{n}$.  
For every positive integer $n$ and a bit-vector of
width $n$, the signature includes a constant of sort $\sortbv{n}$ 
in $\sigbv$ representing that
bit-vector, which we denote as a binary string of length $n$.
The function and predicate symbols of $\sigbv$ are as
described in the \smtlib standard.

Formulas of
$\sigbv$ are built from variables (sorted by the sorts $\sortbv{n}$),
bit-vector constants, and the function and predicate symbols of $\sigbv$,
along with the usual logical connectives and quantifiers.  
%We write
%$\psi[x_{1}\til x_{n}]$ to represent a formula whose free %variables are
%from $\{x_{1}\til x_{n}\}$. 

The semantics of $\sigbv$-formulas is given by interpretations that extend a
single many-sorted first-order structure so that the domain of every sort
$\sortbv{n}$ is the set of bit-vectors of bit-width $n$, and the function and
predicate symbols are interpreted as specified by the \smtlib standard.  A
$\sigbv$-formula is said to be \emph{valid} in the theory of fixed-width bit-vectors
if it evaluates to true in every such interpretation.

In what follows, we denote by $\coqsig$ the sub-signature of $\sigbv$
containing the predicate symbols 
$\bvultf$, $\bvugtf$, $\bvulef$, $\bvugef$ 
(corresponding to strong and weak unsigned comparisons
between bit-vectors, respectively), as
well as the function symbols $\bvaddf$ (bit-vector addition), $\bvandf$, $\bvorf$, $\bvnot$ (bit-wise conjunction,
disjunction and negation), 
$\bvnegf$ (2's complement unary negation), 
and $\bvshl$, $\bvlshrf$ and
$\bvashrf$ (left shift, and logical and 
arithmetical right shifts).  
%
We also
denote by $\cavsig$ the extension of $\coqsig$ with the predicate symbols
$\bvsltf$, $\bvsgtf$, $\bvslef$, and $\bvsgef$ 
(corresponding to strong and weak signed comparisons
between bit-vectors, respectively), as 
well as the function symbols $\bvsubf$,
$\bvmulf$, $\bvudivf$, $\bvuremf$ (corresponding to subtraction,
multiplication, division and remainder), 
and $\bvconcatf$ (concatenation).  
%We use $0$ to represent the bit-vectors composed of all $0$-bits.
%Its numerical or bit-vector interpretation should be clear from context.  
%Using bit-wise negation $\bvnotf$, we can express the bitvectors composed
%of all $1$-bits by $\bvnot{0}$.
 

\section{Invertibility Equivalence Proofs}
\label{ieproofs}
An invertibility condition for a variable $x$ in a $\sigbv$-literal $\ell[x,s,t]$ is
a formula $IC[s,t]$ such that
$\forall s.\,\forall t.\,IC[s,t] \Leftrightarrow \exists x.\ell[x,s,t]$ is valid in the theory of fixed-width bit-vectors.

Reference \cite{b1} define invertibility conditions for 
a representative set of literals $\ell$ having a single occurrence of $x$,
that involve the bit-vector operators of $\cavsig$.
The soundness of the technique proposed in that work 
relies on the correctness of the invertibility conditions.
Every literal $\ell[x,s,t]$ and its corresponding invertibility condition $IC[s,t]$
induce the \emph{invertibility equivalence}
\[
\forall s:\sortbv{n}.\,\forall t:\sortbv{n}.\,IC[s,t] \Leftrightarrow \exists x:\sortbv{n}.\ell[x,s,t] \ .
\]
which one needs to prove valid for \emph{all} $n >0$.
Reference \cite{b1} was able to prove these 
equivalences for values of $n$ from $1$ to $65$.

Reference \cite{b2} proved over half of the 160 
equivalences for arbitrary bit-widths 
using \smt-solvers by encoding the equivalences 
into theories which the solvers could deal with.

We focused mainly on proving those equivalences 
that \cite{b2} failed to prove. We chose $\coqsig$ as a 
representative subset of $\cavsig$, and proved 18 of the 
equivalences, 11 of which were unproved by \cite{b2}. Our 
results are summarized in \Cref{icresults}.

\begin{table}
	\begin{center}
		{%
			\renewcommand{\arraystretch}{1.2}%
			\begin{tabular}{r@{\hspace{2.0em}}c@{\hspace{1.0em}}c@{\hspace{1.5em}}c@{\hspace{1.0em}}c@{\hspace{1.5em}}c@{\hspace{1.0em}}c}
				\hline
				\\[-2.5ex]
				$\ell[x]$ & \teq & \tneq & \bvultf & \bvugtf & \bvulef &
				\bvugef
				\\[.5ex]
				\hline
				\\[-2.5ex]
				$\bvneg{x}  \rel t$ & \both & \cadep & \cadep & \cadep  
				& \cadep & \cadep \\
				$\bvnot{x}  \rel t$ & \both & \cadep & \cadep & \cadep  
				& \cadep & \cadep  \\
				$\bvand{x}{s}  \rel t$ & \coqp & \cadep & \cadep & \cadep  
				& \cadep & \cadep \\
				$\bvor{x}{s}   \rel t$ & \coqp & \cadep & \cadep & \cadep 
				& \cadep & \cadep \\
				$\bvshl{x}{s}  \rel t$ & \coqp & \coqp & \cadep & \coqp   
				& \cadep & \coqp \\
				$\bvshl{s}{x}  \rel t$ & \both & \cadep & \cadep & \cadep 
				& \cadep & \cadep \\
				$\bvlshr{x}{s} \rel t$ & \both & \cadep & \cadep & \none 
				& \cadep & \cadep \\
				$\bvlshr{s}{x} \rel t$ & \both & \cadep & \cadep & \cadep 
				& \cadep & \cadep \\
				$\bvashr{x}{s} \rel t$ & \coqp & \cadep & \cadep & \cadep 
				& \cadep & \cadep \\
				$\bvashr{s}{x} \rel t$ & \both & \cadep & \coqp & \coqp  
				& \coqp & \coqp \\
				$\bvadd{x}{s}  \rel t$ & \both & \cadep & \cadep & \cadep 
				& \cadep & \cadep \\
			\end{tabular}%
		}
	\end{center}
	\caption{Results of proving invertibility equivalences 
		for literals in $\coqsig$.
	}\label{icresults} 
\end{table} 


\section{Library and Proof Details}
\label{proofs}
We used a library originally developed for the
\smtcoq tool \rem{cite} - a \coq plugin 
that dispatches proof goals to \smt-solvers.
Although there are other libraries such as 
\rem{cite Bedrock, SSRBit and the Coq library here},
we choose this library because it was developed 
for \smtlib bit-vectors, and as a result, had many 
relevant lemmas for our proofs already available.
We extended this library with the $\bvashrf$
operator, and the predicates $\bvulef$ and $\bvugef$.
In using the library for our proofs, we also enriched 
it with various additional lemmas.

The bit-vector library represents bit-vectors as 
lists of Booleans, dependent on a natural number, 
representing their size. This dependent bit-vector 
type is constructed from an underlying non-dependent 
representation. This separation makes it easier to 
expand the library - one can represent operators 
and lemmas in the non-dependent representation, 
before using the library's functor to transform it 
into the required dependent type. \rem{citations}

We were also assisted by CoqHammer - a tool that 
solves proof goals by learning from previous proofs, 
and by deploying proofs to external automated provers
 - in solving subgoals.
 
\section{Conclusion}
\label{conc}
\rem{Is this a good place to mention that we submitted this 
	work to PxTP?} We present here our work in an ongoing 
project of using invertibility conditions to facilitate a 
quantifier instantiation technique that is deployed in 
the \cvcfour SMT solver. Our contribution was to 
prove a subset of these invertibility conditions in the 
\coq proof assistant for a general bit-width. We plan 
to extend this library with operators such as division and 
modulus in the future, and prove a bigger set of invertibility conditions. 


\section*{References}

Please number citations consecutively within brackets \cite{b1}. The 
sentence punctuation follows the bracket \cite{b2}. Refer simply to the reference 
number, as in \cite{b3}---do not use ``Ref. \cite{b3}'' or ``reference \cite{b3}'' except at 
the beginning of a sentence: ``Reference \cite{b3} was the first $\ldots$''

Number footnotes separately in superscripts. Place the actual footnote at 
the bottom of the column in which it was cited. Do not put footnotes in the 
abstract or reference list. Use letters for table footnotes.

Unless there are six authors or more give all authors' names; do not use 
``et al.''. Papers that have not been published, even if they have been 
submitted for publication, should be cited as ``unpublished'' \cite{b4}. Papers 
that have been accepted for publication should be cited as ``in press'' \cite{b5}. 
Capitalize only the first word in a paper title, except for proper nouns and 
element symbols.

For papers published in translation journals, please give the English 
citation first, followed by the original foreign-language citation \cite{b6}.

\begin{thebibliography}{00}
\bibitem{b1} A. Niemetz, M. Preiner, A. Reynolds, 
C. Barrett and C. Tinelli, ``Solving Quantified Bit-Vectors 
Using Invertibility Conditions,'' Computer Aided Verification 2018, pp.236-255.
\bibitem{b2} A. Niemetz, M. Preiner, A. Reynolds, 
Y. Zohar, C. Barrett and C. Tinelli, ``Towards Bit-Width-Independent Proofs in SMT Solvers,'' 
To appear in the proceedings of 
Conference on Automated Deduction 2019.
\bibitem{b3} I. S. Jacobs and C. P. Bean, ``Fine particles, thin films and exchange anisotropy,'' in Magnetism, vol. III, G. T. Rado and H. Suhl, Eds. New York: Academic, 1963, pp. 271--350.
\bibitem{b4} K. Elissa, ``Title of paper if known,'' unpublished.
\bibitem{b5} R. Nicole, ``Title of paper with only first word capitalized,'' J. Name Stand. Abbrev., in press.
\bibitem{b6} Y. Yorozu, M. Hirano, K. Oka, and Y. Tagawa, ``Electron spectroscopy studies on magneto-optical media and plastic substrate interface,'' IEEE Transl. J. Magn. Japan, vol. 2, pp. 740--741, August 1987 [Digests 9th Annual Conf. Magnetics Japan, p. 301, 1982].
\bibitem{b7} M. Young, The Technical Writer's Handbook. Mill Valley, CA: University Science, 1989.
\end{thebibliography}
\end{document}