From f081142f871f0a05f62b5c28c9d8daef09d42a2c Mon Sep 17 00:00:00 2001
From: Hans-Joerg Schurr <commits@schurr.at>
Date: Mon, 18 Mar 2024 19:47:17 -0500
Subject: [PATCH] Bitblasting: adapt notation

---
 spec/rule_list.tex | 92 +++++++++++++++++++++++++---------------------
 1 file changed, 50 insertions(+), 42 deletions(-)

diff --git a/spec/rule_list.tex b/spec/rule_list.tex
index d91a206..868f23f 100644
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
@@ -1532,58 +1532,58 @@ form and the reordering of equalities.
 
 \begin{RuleDescription}{bitblast_extract}
 \begin{AletheX}
-$i$. & \ctxsep & $((\_\ \mathrm{extract}\ j\ i)\ x) \simeq (\mathrm{bbterm}\ x[i]\ \ldots\ x[j])$ & (\currule) \\
+$i$. & \ctxsep & $((\lsymb{extract}\ j\ i)\ x) ≈ (\lsymb{bbT}\ \varphi_i\ \ldots\ \varphi_j)$ & (\currule) \\
 \end{AletheX}
 
-Each term $x[i]$ corresponds to whether the $i$-th bit of $x$ is true or not, which
-will be represented via an application of the operator ``bit\_of'', i.e.,
-$((\_\ bit\_of\ i)\ x)$, which has a Boolean return type.
-%
-The ``bbterm'' operator takes $n$ Booleans and yields a bit-vector of size $n$
-where the least significant bit is 1 if the first argument 1 is true, 0
-otherwise, and so on.
-%
+\noindent
+where the formulas $\varphi_k$ are $(\lsymb{bitOf}_k\ x)$ for $i \leq k \leq j$.
+
 Alternatively, the rule may also be phrased as a ``short-circuiting'' of the
-above when $x$ is a ``bbterm'' application:
+above when $x$ is a $\lsymb{bbT}$ application:
 
 \medskip
 \begin{AletheX}
-$i$. & \ctxsep & $((\_\ \mathrm{extract}\ j\ i)\ (\mathrm{bbterm}\ x_0\ \ldots\
-x_i\ \ldots \ x_j\ \ldots\ x_n)) \simeq (\mathrm{bbterm}\ x_i\ \ldots\ x_j)$ & (\currule) \\
+$i$. & \ctxsep & $((\lsymb{extract}\ j\ i)\ (\lsymb{bbT}\ x_0\ \ldots\
+x_i\ \ldots \ x_j\ \ldots\ x_n)) ≈ (\lsymb{bbT}\ x_i\ \ldots\ x_j)$ & (\currule) \\
 \end{AletheX}
 
+\noindent
 This alternative is based on the validity of the equality
-$$(\mathrm{bbterm}\ x_0\ \ldots\ x_i\ \ldots \ x_j\ \ldots\ x_n)[i]\simeq x_i$$
-for any bit-vector $x$ of size $n+1$, where $0\leq i\leq n$.
+\[
+\lsymb{bitOf}_k\ (\lsymb{bbT}\ x_0\ \ldots\ x_i\ \ldots \ x_j\ \ldots\ x_n) ≈ x_k
+\]
+for any bit-vector $x$ of size $n+1$, where $0\leq k\leq n$.
 
 \end{RuleDescription}
 
 \begin{RuleDescription}{bitblast_ult}
 \begin{AletheX}
-$i$. & \ctxsep & $(\mathrm{bvult}\ x\ y) \simeq res_{n-1}$ & (\currule) \\
+$i$. & \ctxsep & $(\lsymb{bvult}\ x\ y) ≈ \mathrm{res}_{n-1}$ & (\currule) \\
 \end{AletheX}
-in which both $x$ and $y$ must have the same type $(\_\ \mathrm{BitVec}\ n)$ and, for
-$i\geq 0$:
+in which both $x$ and $y$ must have the same type $(\lsymb{BitVec}\ n)$ and, for
+$i\geq 0$
 \[
   \begin{array}{lcl}
-    \mathrm{res}_0&=&\neg x[0] \wedge y[0]\\
-    \mathrm{res}_{i+1}&=&((x[i+1]\simeq y[i+1])\wedge
-                          \mathrm{res}_i)\vee (\neg x[i+1]\wedge y[i+1])
+    \mathrm{res}_0&=&\neg (\lsymb{bitOf}_0\ x) \wedge (\lsymb{bitOf}_0\ y)\\
+    \mathrm{res}_{i+1}&=&(((\lsymb{bitOf}_{i+1}\ x) ≈ (\lsymb{bitOf}_{i+1}\ y))\wedge \mathrm{res}_i)\vee
+                       (\neg (\lsymb{bitOf}_{i+1}\ x) \wedge (\lsymb{bitOf}_{i+1}\ y))
   \end{array}
 \]
+
+\noindent
 Alternatively, the rule may also be phrased as a ``short-circuiting'' of the
-above when $x$ and $y$ are ``bbterm'' applications. So given that
+above when $x$ and $y$ are ``$\lsymb{bbT}$'' applications. So given that
 \[
   \begin{array}{lcl}
-    x&=&(\mathrm{bbterm}\ x_0\ \ldots\ x_i\ \ldots \ x_j\ \ldots\ x_n)\\
-    y&=&(\mathrm{bbterm}\ y_0\ \ldots\ y_i\ \ldots \ y_j\ \ldots\ y_n)\\
+    x&=&(\lsymb{bbT}\ x_0\ \ldots\ x_i\ \ldots \ x_j\ \ldots\ x_n)\\
+    y&=&(\lsymb{bbT}\ y_0\ \ldots\ y_i\ \ldots \ y_j\ \ldots\ y_n)\\
   \end{array}
 \]
-then ``res'' can be defined, for $i \geq 0$, as 
+then ``$\mathrm{res}$'' can be defined, for $i \geq 0$, as 
 \[
   \begin{array}{lcl}
     \mathrm{res}_0&=&\neg x_0 \wedge y_0\\
-    \mathrm{res}_{i+1}&=&((x_{i+1}\simeq y_{i+1})\wedge
+    \mathrm{res}_{i+1}&=&((x_{i+1} ≈ y_{i+1})\wedge
                           \mathrm{res}_i)\vee (\neg x_{i+1}\wedge y_{i+1})
   \end{array}
 \]
@@ -1592,37 +1592,45 @@ then ``res'' can be defined, for $i \geq 0$, as
 
 \begin{RuleDescription}{bitblast_add}
 \begin{AletheX}
-$i$. & \ctxsep & $(\mathrm{bvadd}\ x\ y) \simeq (\mathrm{bbterm}\ (x[0] \oplus y[0])\oplus\mathrm{carry}_0\ \ldots\ (x[n-1]
-        \oplus y[n-1])\oplus\mathrm{carry}_{n-1})$ & (\currule) \\
+$i$. & \ctxsep & $(\lsymb{bvadd}\ x\ y) ≈ A_1$ & (\currule) \\
 \end{AletheX}
-in which both $x$ and $y$ must have the same type $(\_\ \mathrm{BitVec}\ n)$ and, for
-$i\geq 0$:
-    \[
-      \begin{array}{lcl}
-        \mathrm{carry}_0&=&\bot\\
-        \mathrm{carry}_{i+1}&=&(x[i]\wedge y[i])\vee((x[i]\oplus y[i])\wedge \mathrm{carry}_i)
-      \end{array}
-    \]
+in which both $x$ and $y$ must have the same type $(\lsymb{BitVec}\ n)$.
+The term ``$A_1$'' is
+\begin{align*}
+(\lsymb{bbT}\;& (((\lsymb{bitOf}_{0}\ x) \,\lsymb{xor}\,(\lsymb{bitOf}_{0}\ y))\,\lsymb{xor}\,\mathrm{carry}_0) \\
+              & (((\lsymb{bitOf}_{1}\ x) \,\lsymb{xor}\,(\lsymb{bitOf}_{1}\ y))\,\lsymb{xor}\,\mathrm{carry}_1) \\
+              & \ldots \\
+              & (((\lsymb{bitOf}_{n-1}\ x) \,\lsymb{xor}\, (\lsymb{bitOf}_{n-1}\ y))\,\lsymb{xor}\,\mathrm{carry}_{n-1}))
+\end{align*}
+and for $i\geq 0$
+\[
+  \begin{array}{lcl}
+    \mathrm{carry}_0&=&\bot\\
+    \mathrm{carry}_{i+1}&=&((\lsymb{bitOf}_{i}\ x) \wedge (\lsymb{bitOf}_{i}\ y))\vee(((\lsymb{bitOf}_{i}\ x)\,\lsymb{xor}\, (\lsymb{bitOf}_{i}\ y))\wedge \mathrm{carry}_i)
+  \end{array}
+\]
 
+\noindent
 Alternatively, the rule may also be phrased as a ``short-circuiting'' of the
-above when $x$ and $y$ are ``bbterm'' applications. So given that
+above when $x$ and $y$ are ``$\lsymb{bbT}$'' applications. So given that
 \[
   \begin{array}{lcl}
-    x&=&(\mathrm{bbterm}\ x_0\ \ldots\ x_i\ \ldots \ x_j\ \ldots\ x_n)\\
-    y&=&(\mathrm{bbterm}\ y_0\ \ldots\ y_i\ \ldots \ y_j\ \ldots\ y_n)\\
+    x&=&(\lsymb{bbT}\ x_0\ \ldots\ x_i\ \ldots \ x_j\ \ldots\ x_n)\\
+    y&=&(\lsymb{bbT}\ y_0\ \ldots\ y_i\ \ldots \ y_j\ \ldots\ y_n)\\
   \end{array}
 \]
 then the rule can be alternatively phrased as
 
 \begin{AletheX}
-$i$. & \ctxsep & $(\mathrm{bvadd}\ x\ y) \simeq (\mathrm{bbterm}\ (x_0 \oplus y_0)\oplus\mathrm{carry}_0\ \ldots\ (x_{n-1}
-        \oplus y_{n-1})\oplus\mathrm{carry}_{n-1})$ & (\currule) \\
+$i$. & \ctxsep & $(\mathrm{bvadd}\ x\ y) ≈ A_2$ & (\currule) \\
 \end{AletheX}
-with ``carry'' being defined, for $i \geq 0$, as 
+with $A_2 := (\lsymb{bbT}\ (x_0 \,\lsymb{xor}\, y_0)\,\lsymb{xor}\,\mathrm{carry}_0\ \ldots\ (x_{n-1}
+        \,\lsymb{xor}\, y_{n-1})\,\lsymb{xor}\,\mathrm{carry}_{n-1})$ and
+``$\mathrm{carry}$'' being defined, for $i \geq 0$, as 
 \[
   \begin{array}{lcl}
     \mathrm{carry}_0&=&\bot\\
-    \mathrm{carry}_{i+1}&=&(x_i\wedge y_i)\vee((x_i\oplus y_i)\wedge \mathrm{carry}_i)
+    \mathrm{carry}_{i+1}&=&(x_i\wedge y_i)\vee((x_i\,\lsymb{xor}\, y_i)\wedge \mathrm{carry}_i)
   \end{array}
 \]
 
-- 
GitLab