main.tex

\documentclass[10pt,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}
\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{hyperref}
\usepackage{cleveref}

\BeforeBeginEnvironment{minted}{\begin{tcolorbox}}%
	\AfterEndEnvironment{minted}{\end{tcolorbox}}%
	
%\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}

%%CT The \thanks command was causing the extrapage
%\thanks{Identify applicable funding agency here. If none, delete this.}

%%CT See Section IV.B of 
% http://mirrors.ibiblio.org/CTAN/macros/latex/contrib/IEEEtran/IEEEtran_HOWTO.pdf
% for how to add more than three authors
\author{\IEEEauthorblockN{
Arjun Viswanathan\IEEEauthorrefmark{2},
Burak Ekici\IEEEauthorrefmark{3},
Yoni Zohar\IEEEauthorrefmark{4},
Clark Barrett\IEEEauthorrefmark{4} and
Cesare Tinelli\IEEEauthorrefmark{2}}
\\
\IEEEauthorblockA{
\IEEEauthorrefmark{2}\textit{Department of Computer Science},
\textit{University of Iowa},
Iowa City, USA
%arjun-viswanathan@uiowa.edu
}
\IEEEauthorblockA{
\IEEEauthorrefmark{3}\textit{Department of Computer Science},
\textit{University of Innsbruck},
Innsbruck, Austria
%burak.ekici@uibk.ac.at
}
\IEEEauthorblockA{
\IEEEauthorrefmark{4}\textit{Department of Computer Science},
\textit{Stanford University},
Stanford, USA
%yoniz@cs.stanford.edu
}
%\IEEEauthorblockA{\textit{Department of Computer Science} \\
%\textit{Stanford University}\\
%Stanford, USA \\
%barrett@cs.stanford.edu}
%\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, 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~\cite{Gupta:1993:RSM:259794.259827}, 
bounded model checking~\cite{Armando2008BoundedMC}, and symbolic execution~\cite{Cadar:2006:EAG:1180405.1180445}. 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 \emph{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$, or true. This is represented by the equivalence 
$\equal{\bvadd{x}{s}}{t} \iff \true$. 
A more interesting case is that 
of bit-wise conjunction (\bvand{}{}), 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~\cite{DBLP:conf/cav/EkiciMTKKRB17}, and proved 18 invertibility equivalences.

\section{Invertibility Equivalence Proofs}
\label{ieproofs}
We assume the usual terminology of many-sorted 
first-order logic with equality
(see, e.g.,~\cite{ENDERTON200167} for more details),
and consider the \smtlib~\cite{SMTLib2010} 
\footnote{The \smtlib theory is defined at \url{http://www.smt-lib.org/theories.shtml}}
theory of bit-vectors, $\sigbv$.
In general, we write
$\psi[x_0, ..., x_n]$ to denote a formula whose free variables are 
from the set $\{x_0, ..., x_n\}$.
An \emph{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. 
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).

Reference \cite{b1} defines 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.
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}$.
Thus, 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} proves 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}.
There, \coqp means that the invertibility 
equivalence was successfully verified in \coq
but not in~\cite{b2}, while \cadep means the 
opposite; \both means that the invertibility 
equivalence was verified using both approaches, 
and \none that it was verified with neither.
Meta-symbol $\bowtie$ ranges over the operators 
in the table's top row.

\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 over $\coqsig$. 
	}\label{icresults} 
\end{table} 


\section{Library and Proof Details}
\label{proofs}
We used a library originally developed for the
\smtcoq tool~\cite{DBLP:conf/cav/EkiciMTKKRB17},
a \coq plugin 
that dispatches proof goals to \smt-solvers.
Although there are other libraries such as 
\coq's bit-vector library~\cite{coqbvlib}, 
the Bedrock Bit Vectors Library~\cite{bbvlib}, and the SSRBit library~\cite{ssrbit},
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
\footnote{Both the library and the proofs of invertibility equivalences can be found at \url{https://github.com/ekiciburak/bitvector/tree/pxtp2019}}.

We were also assisted by CoqHammer, a tool that 
solves proof goals by learning from previous proofs, 
and by outsourcing proofs of certain subgoals 
to external automated provers.
 
\section{Conclusion}
\label{conc}
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. 

\section{Future Work}
\label{future}
This work was accepted and is to be presented at PxTP 
2019~\cite{b3} as an extended abstract.
In the future, we plan to expand this library 
with operators such as division and 
modulus, and prove a larger set of 
invertibility conditions. The next goal would be 
to extend SMTCoq so it can certify proofs 
over the newly added operators of the Coq library. 
Another potential 
direction of future work is to recreate the library 
in the Lean Theorem Prover \cite{conf/cade/MouraKADR15}.

%\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}.

\bibliographystyle{IEEEtran}
\bibliography{generic}

\end{document}