From 11c64b2ea6a8f880513719655d428bd7354d761a Mon Sep 17 00:00:00 2001 From: Hans-Joerg Schurr <commits@schurr.at> Date: Mon, 18 Mar 2024 12:12:42 -0500 Subject: [PATCH] Finish bitblasting function description section --- spec/doc.tex | 67 ++++++++++++++++++++++++++++++++++++---------------- 1 file changed, 46 insertions(+), 21 deletions(-) diff --git a/spec/doc.tex b/spec/doc.tex index b37d7ad..c0b26f1 100644 --- a/spec/doc.tex +++ b/spec/doc.tex @@ -1691,29 +1691,33 @@ is functional congruence, and \proofRule{sko_forall} works like \subsection{Bitvector Reasoning with Bitblasting} -A standard approach to handle bitvector reasoning in SMT solvers is bitblasting. -Bitblasting\index{bitblasting} is the translation of bit-vector\index{bit-vector} -functions to propositional formulas. - -To express bitplasting in the Alethe proof rules, the format uses multiple families -helper functions: $\lsymb{bbT}$, $\lsymb{bitOf}$, $\lsymb{bvsize}$, and $\lsymb{bv}$. -To avoid name clashes with user defined functions, $\lsymb{bbT}$ -is written as \inlineAlethe{@bbT}, $\lsymb{bitOf}$ as \inlineAlethe{@bitOf}, -$\lsymb{bvsize}$ as \inlineAlethe{@bvsize}, and $\lsymb{bv}$ as \inlineAlethe{@bv}. -The SMT-LIB standard specifies +A standard approach to handle bitvector reasoning in SMT solvers +is bitblasting. Bitblasting\index{bitblasting} works by translating +bitvector\index{bitvector} functions to propositional formulas that +model the logical circuit of the bitvector function. + +To express bitblasting in Alethe proof rules, the the Alethe calculus uses +multiple families of helper functions: $\lsymb{bbT}$, $\lsymb{bitOf}_m$, +$\lsymb{bvsize}$, and $\lsymb{bv}_n^i$. Functions in the families are +distinguished either by overloading ($\lsymb{bbT}$ and $\lsymb{bvsize}$) +or by explicit indexing ($\lsymb{bitOf}_m$ and $\lsymb{bv}_n^i$). +To avoid name clashes with user defined +functions, $\lsymb{bbT}$ is written as \inlineAlethe{@bbT}, $\lsymb{bitOf}$ +as \inlineAlethe{@bitOf}, $\lsymb{bvsize}$ as \inlineAlethe{@bvsize}, and +$\lsymb{bv}$ as \inlineAlethe{@bv}. The SMT-LIB standard specifies that simple symbols starting with ``\inlineAlethe{@}'' are reserved for solver generated functions. -The family $\lsymb{bbT}$ consists of one function for each bit-vector sort +The family $\lsymb{bbT}$ consists of one function for each bitvector sort $(\lsymb{BitVec}\;n)$. \[ -\lsymb{bbT} : \underbrace{\lsymb{Bool} \dots \lsymb{Bool}}_n\;(\lsymb{BitVec}\;n). +\lsymb{bbT}\,:\,\underbrace{\lsymb{Bool}\,\dots\,\lsymb{Bool}}_n\;(\lsymb{BitVec}\;n). \] \noindent -Intuitively, the predicate $\lsymb{bbT}$ takes a list of boolean arguments and +Intuitively, the function $\lsymb{bbT}$ takes a list of boolean arguments and packs them into a bitvector. -Let $\langle u_1, \dots, u_n\rangle$ denote a bit-vector of sort $(\lsymb{BitVec}\;n)$ +Let $\langle u_1, \dots, u_n\rangle$ denote a bitvector of sort $(\lsymb{BitVec}\;n)$ where $u_i = \top$ if the bit at position $i$ is $1$, and $u_i = \bot$ otherwise. The bit $u_n$ is the least significant bit. Then @@ -1722,8 +1726,7 @@ The bit $u_n$ is the least significant bit. Then \] \noindent -The addition of the $\lsymb{bbT}$ predicates is a conservative extension. -They could be defined in terms of standard SMT-LIB functions. +The $\lsymb{bbT}$ functions could be defined in terms of standard SMT-LIB functions. \begin{align*} \lsymb{bbT}\;v_1 \dots v_n :=\; &\lsymb{concat}\,(\lsymb{concat}\,(\dots \\ @@ -1734,18 +1737,40 @@ They could be defined in terms of standard SMT-LIB functions. \end{align*} \noindent -The functions $\lsymb{bitOf}$ are the inverse of $\lsymb{bbT}$. They extract +The functions $\lsymb{bitOf}_m$ are the inverse of $\lsymb{bbT}$. They extract a bit of a bitvector as a boolean. Just as the built in $\lsymb{extract}$ -symbol, $\lsymb{bitOf}$ is used as an indexed symbol. Hence, for $n \leq m$, we -write \inlineAlethe{(_ @bitOf} $n$ \inlineAlethe{)}, to denote functions +symbol, $\lsymb{bitOf}_m$ is used as an indexed symbol. Hence, for $m \leq n$, we +write \inlineAlethe{(_ @bitOf} $m$ \inlineAlethe{)}, to denote functions \[ -\lsymb{bitOf}_n : (\lsymb{BitVec}\;m) \to \lsymb{Bool}. +\lsymb{bitOf}_m : (\lsymb{BitVec}\;n) \to \lsymb{Bool}. \] These functions are defined as \[ -\lsymb{bitOf}_n \langle u_1, \dots, u_m \rangle := u_n. +\lsymb{bitOf}_m \langle u_1, \dots, u_n \rangle := u_m. \] + +\noindent +The functions $\lsymb{bvsize}$ return the size of a bitvector. Formally, there +is one $\lsymb{bvsize}$ for for each bitvector sort $(\lsymb{BitVec}\;n)$. Each +$\lsymb{bvsize}$ is a constant function that returns $n$. Using notation: + +\begin{align*} +\lsymb{bvsize}& : (\lsymb{BitVec}\;n) \to \mathbb{N}\\ +\lsymb{bvsize}&\;b := n +\end{align*} + +\noindent +Finally, $\lsymb{bv}_n^i$ is a family of constants indexed by two parameters: +a bitvector length $n$, and a natural number $i$. We +write \inlineAlethe{(_ @bv}$n$ $i$ \inlineAlethe{)} for $\lsymb{bv}_n^i$. +The space before $n$ is omitted for historical reasons. +Each $\lsymb{bv}_n^i$ is the bitvector constant that represents the bitvector +of length $n$ that encodes the integer $i$. Formally, it corresponds +to \inlineAlethe{nat2bv[n](i)}, where \inlineAlethe{nat2bv} is defined +as in the SMT-LIB +standard.\footnote{See \url{https://smt-lib.github.io/theories-FixedSizeBitVectors.shtml}.} + \section{The Alethe Rules} \label{apx:rules} \input{rule_list} -- GitLab