formalization

Author: osmanyasar05

paper.tex

@@ -123,6 +123,23 @@
 \newacronym{hls}{HLS}{High-level Synthesis}
 \newacronym{asic}{ASIC}{application-specific integrated circuits}
 
+\newcommand{\sem}[1]{\llbracket #1 \rrbracket}
+\newcommand{\Circ}{\mathit{Circuit}}
+\newcommand{\Col}{\mathit{Column}}
+\newcommand{\Heap}{\mathit{BitHeap}}
+\newcommand{\Arith}{\mathit{Arith}}
+\newcommand{\Step}{\mathit{Step}}
+\newcommand{\Chain}{\mathit{Chain}}
+\newcommand{\var}{\mathsf{var}}
+\newcommand{\HA}{\mathsf{HA}}
+\newcommand{\FA}{\mathsf{FA}}
+\newcommand{\maj}{\mathsf{maj}}
+\newcommand{\zext}{\mathsf{zext}}
+\newcommand{\trunc}{\mathsf{trunc}}
+\newcommand{\flatten}[1]{\lfloor #1 \rfloor}
+\newcommand{\lift}[1]{\lceil #1 \rceil}
+\newcommand{\compile}[1]{\langle\!\langle #1 \rangle\!\rangle}
+
 \graphicspath{{./images/}}
 
 % Define macros that are used in this paper
@@ -332,9 +349,10 @@ \section{Background}
 where the term $x_i \cdot y_j$ is the logical AND of the bits, and the weight of the resulting bit is $2^{i+j}$. 
 Therefore, a multiplication can be implemented as a summation of weighted bits, where the bits are generated by logical AND of the bits of the two operands.
 
-A bit heap is a data structure that effectively represents the summation of weighted bits \cite{arithmetic_core_generation_bitheaps}. Bits in a bit heap are organized into columns based on their weights, and the height of each column corresponds to the number of bit values that need to be summed for that particular weight.
+A bit heap is a data structure that effectively represents the summation of weighted  bits \cite{arithmetic_core_generation_bitheaps}. Bits in a bit heap are organized into columns based on their weights, and the height of each column corresponds to the number of bit values that need to be summed for that particular weight.
 
 \subsection{Compression Algorithms}
+\label{comp_algo}
 In arithmetic circuits, a main contributor to delay is carry propagation. In cases where multiple summands must be added, the naive approach chains carry-propagation adders, growing the delay linearly with the number of bits and summands. For example, multiplication is usually implemented as addition of multiple summands. 
 
 Compressor trees are built to address this issue by reducing multiple summands to two using carry-save arithmetic, 
@@ -347,7 +365,7 @@ \subsubsection{Wallace Tree}
 
 \subsubsection{Dadda's Algorithm}
 Dadda's algorithm is a method for reducing the partial products of an $n$-bit multiplier to a two-row representation 
-using \acrfull{fa} and \acrfull{ha}, after which a single \acrfull{cpa} produces the final result \cite{application_specific_arithmetic}.
+using \acrfull{fa} and \acrfull{ha}, after which a single \acrfull{cpa} produces the final result \cite{application_specific_arithmetic} \cite{dadda_tree}.
 
 \begin{figure}[h]
   \centering
@@ -388,18 +406,55 @@ \subsubsection{Dadda's Algorithm}
 \end{tcolorbox}
 
 \section{Formalization}
-In this section, we present the formalization of the bit heap data structure and compression algorithms in Lean 4. 
+In this section, we present the formalization of the bit heap data structure as well as the underlying hardware-level constructs and compression algorithms in Lean 4. 
 We also discuss the correctness of the composition of adders and how we relate bit heaps to bit-vector arithmetic.
 
+\subsection{Circuit}
+The building block of the bit heap data structure is a single bit. 
+In our formalization, the Circuit data structure represent a boolean expression, that is named by a natural-number index.
+
+\[
+\begin{array}{r@{\;}c@{\;}l@{\qquad}l}
+\multicolumn{4}{l}{%
+  \text{indices } \mathbb{N} \ni n,k \qquad
+  \text{width } \mathbb{N}^{+} \ni w \qquad
+  \circledast \in \{\oplus,\wedge,\vee,\barwedge\}}\\[6pt]
+\Circ \ni c &::=& b_n \mid 0 \mid 1 \mid c \circledast c &
+\end{array}
+\]
+
+A \texttt{Circuit} describes a logical expression, that can be a binary variable, constant, or any binary operation over composition Circuit objects.
+The bits represented by \texttt{Circuit} are symbolic and do not hold any value.
+A Circuit is assigned a value under a bit environment $\sigma$,
+which maps the \texttt{Circuit} to Boolean values.
+
+\[
+\begin{array}{r@{\;}c@{\;}l}
+\multicolumn{3}{@{}l@{}}{%
+  \sigma \;=\; \mathbb{N} \to \mathbb{B}} \\[4pt]
+\mathcal{C}\sem{b_n}\sigma &=& \sigma(n)\\
+\mathcal{C}\sem{0}\sigma &=& \mathit{false}\\
+\mathcal{C}\sem{1}\sigma &=& \mathit{true}\\
+\mathcal{C}\sem{c_1 \circledast c_2}\sigma
+  &=& \mathcal{C}\sem{c_0}\sigma \circledast \mathcal{C}\sem{c_1}\sigma
+\end{array}
+\]
+
+We write $\lift{\cdot} : \mathbb{B} \to \{0,1\}$ for the conversion of a
+Boolean into the natural number, so that $\lift{\mathcal{C}\sem{c}\sigma}$ is
+the numeric contribution of circuit $c$.
+
 \subsection{Bit Heap Data Structure}
-A bit heap of width $w$ is a vector of $w$ columns, where the column at index $i$ holds the bits of weight $2^i$. 
-Bits are implemented as an inductive type that we call \texttt{Circuit}. 
-A \texttt{Circuit} describes a logical expression, that can be any binary operation, constant, or a binary variable. 
-The bits represented by \texttt{Circuit} is merely symbolic and does not hold any value, it hold how a bit is computed.
-A value is obtained only under an environment, which assigns Boolean values to the input variables. 
-We use $\bit{c}{\mathit{env}}$ for the value of the \texttt{Circuit} $c$ under the environment $\mathit{env}$.
-A \texttt{Column} is a set of such \texttt{Circuit} elements. 
-The fact that a \texttt{Column} is a set and not a multiset opens up an optimization path that we discuss below.
+A bit heap of width $w$ is a vector of $w$ columns, where the column at index $k$ holds the bits of weight $2^k$. 
+A \texttt{Column} is a set of \texttt{Circuit} elements. 
+
+\[
+\begin{array}{r@{\;}c@{\;}l@{\qquad}l}
+\Col \ni \gamma &::=& \{c_0,\dots,c_n\} \\[2pt]
+\Heap_w \ni h &::=& \{ \gamma_0,\dots,\gamma_{w-1} \} &
+\end{array}
+\]
+
 
 \begin{definition}[Bit heap]
 \label{def:bitheap}
@@ -408,119 +463,164 @@ \subsection{Bit Heap Data Structure}
 \[
   \mathtt{BitHeap}\;w \;\triangleq\; \mathtt{Vector}\;\mathtt{Column}\;w
 \]
-where the component at index $i$ holds the bits of weight $2^{i}$.
 \end{definition}
 
+To compute the value of the bit heap, we compute the weighted sum of the value held by columns, which is the sum of the values of the bits under a certain environment.
+The value of the bit heap is computed in modular arithmetic. Therefore, all correctness statements below are stated as modulo $2^w$.
+
+\[
+\begin{array}{r@{\;}c@{\;}l@{\qquad}l}
+\mathcal{G}\sem{\gamma}\sigma
+  &=& \textstyle\sum_{c \in \gamma} \lift{\mathcal{C}\sem{c}\sigma}
+  & \mathcal{G}\sem{\cdot}\sigma : \Col \to \mathbb{N}\\[6pt]
+\mathcal{H}\sem{h}\sigma
+  &=& \bigl(\textstyle\sum_{k<w} 2^{k}\cdot\mathcal{G}\sem{h_k}\sigma\bigr)
+      \bmod 2^{w}
+  & \mathcal{H}\sem{\cdot}\sigma : \Heap_w \to \mathbb{Z}
+\end{array}
+\]
+
 The value of a bit heap is obtained by summing each column and combining the columns with Horner's method:
 \begin{equation}
-  \sum_{i=0}^{n} a_i x^i = a_0 + x \left( a_1 + x \left( a_2 + \cdots + x \, a_n \right) \right)
+\begin{split}
+  \Bigl( \sum_{k=0}^{w-1} &\mathcal{G}\sem{h_k}\sigma \cdot x^{k} \Bigr) \bmod 2^{w}\\
+    &= \Bigl( \mathcal{G}\sem{h_0}\sigma + x \bigl( \mathcal{G}\sem{h_1}\sigma
+      + x ( \mathcal{G}\sem{h_2}\sigma + \cdots\\
+    &\qquad + x \, \mathcal{G}\sem{h_{w-1}}\sigma ) \bigr) \Bigr) \bmod 2^{w}
+\end{split}
 \end{equation}
 
-By setting $x = 2$, and having $a_i$'s as the value of column at index $i$, we obtain the value of the bit heap.
-The Horner's method has a useful property that it can be implemented as a recursive function:
-
-\begin{lean4}
-def HornersMethod (env : BitEnv) : List Column -> Nat
-  | [] => 0
-  | c :: rest => (c.eval env) + 2 * HornersMethod env rest
-\end{lean4}
+By setting $x = 2$, so that each column at index $k$ contributes its value $\mathcal{G}\sem{h_k}\sigma$ weighted by $2^{k}$, and reducing modulo $2^{w}$, we obtain the value of the bit heap.
+Horner's method is structurally recursive on the list of columns, which makes it convenient for induction in Lean.
 
-This recursive structure makes this definition convenient for our proofs in Lean 4 ITP.
+\begin{table*}[t]
+  \centering
+  \caption{Compression steps. $\maj$ denotes the majority function
+           $(i \wedge j) \vee (i \wedge l) \vee (j \wedge l)$.}
+  \label{tab:steps}
+  \begin{tabular}{@{}lll@{}}
+  \toprule
+  Step & Applicability & Effect \\
+  \midrule
+  $\HA(k,i,j)$
+    & $i,j \in \gamma_k$, $i \neq j$
+    & remove $i,j$ from $\gamma_k$;\;
+      add $i \oplus j$ at $\gamma_k$;\;
+      add $i \wedge j$ at $\gamma_{k{+}1}$ \\[2pt]
+  $\FA(k,i,j,l)$
+    & $i,j,l \in \gamma_k$, pairwise distinct
+    & remove $i,j,l$ from $\gamma_k$;\;
+      add $i \oplus j \oplus l$ at $\gamma_k$;\;
+      add $\maj(i,j,l)$ at $\gamma_{k{+}1}$ \\
+  \bottomrule
+  \end{tabular}
+\end{table*}
 
 Our framework is based on modular arithmetic, so correctness statements for operations on a bit heap hold only modulo $2^w$.
-The reason lies in the fixed nature of hardware, the number of bits is fixed and cannot be changed. 
 That means when a carry is produced on the last column, it is dropped.
 
-Adding a bit to the bit heap requires care for the case where the bit to-be-added is already in the bit heap, since \texttt{Column}s are defined as sets and sets do not allow duplicates of the same values.
-If the bit is already in the column $i$, we remove the existing copy and insert the bit into the next column, which is correct
-because $x + x = 2x$, and repeat if the next column also contains it.
-Effectively this results in building the bit heap in an optimized way by construction.
-Another important operation is the bit removal operation. 
-Introduction of the removal operation forces us to use \texttt{Int} instead of \texttt{Nat}, since in bit removal the value of the bit heap can go to negative temporarily.
-
-Two theorems describe the effect of adding and removing bits from the bit heap.
-Adding a bit $c$ to column $k$ increases the value by $2^k \cdot c$ (Theorem~\ref{thm:addBit}), and removing a bit $c$ from column $k$, provided $c$ is
-actually in that column, decreases it by $2^k \cdot c$ (Theorem~\ref{thm:removeBit}), both modulo $2^w$. 
-The \texttt{evalMod} function is implemented as evaluation using Horner's method modulo $2^w$
+Two theorems describe the primitive operations. Adding a bit $c$ at
+column $k$ increases the value by $2^{k}\lift{\mathcal{C}\sem{c}\sigma}$
+(\ref{thm:addBit}). Removing a bit $c$ from column $k$, provided
+$c$ is present in that column, decreases it by the same amount
+(\ref{thm:removeBit}).
 
 \begin{theorem}[\texttt{evalMod\_heap\_addBit}]
 \label{thm:addBit}
-For all $h : \mathtt{BitHeap}\;w$, $k : \mathbb{N}$, $c : \mathtt{Circuit}$
-and $\mathit{env} : \mathtt{BitEnv}$,
+For all $h : \Heap_w$, $k : \mathbb{N}$, $c : \Circ$ and
+$\sigma : \mathbb{N} \to \mathbb{B}$,
 \[
-  \mathtt{evalMod}\big(\mathtt{addBit}(k, c, h),\, \mathit{env}\big)
+  \mathcal{H}\sem{\mathtt{addBit}(k, c, h)}\sigma
   \;=\;
-  \Big(\mathtt{evalMod}(h, \mathit{env}) + 2^{k}\cdot\bit{c}{\mathit{env}}\Big)
-  \bmod 2^{w}
+  \bigl(\mathcal{H}\sem{h}\sigma
+        + 2^{k}\cdot\lift{\mathcal{C}\sem{c}\sigma}\bigr) \bmod 2^{w}.
 \]
 \end{theorem}
 
 \begin{theorem}[\texttt{evalMod\_heap\_removeBit}]
 \label{thm:removeBit}
-For all $h : \mathtt{BitHeap}\;w$, $k : \mathbb{N}$, $c : \mathtt{Circuit}$
-and $\mathit{env} : \mathtt{BitEnv}$ with $c \in h.\mathtt{get}(k)$,
+For all $h : \Heap_w$, $k : \mathbb{N}$, $c : \Circ$ and
+$\sigma : \mathbb{N} \to \mathbb{B}$ with $c \in h_k$,
 \[
-  \mathtt{evalMod}\big(\mathtt{removeBit}(k, c, h),\, \mathit{env}\big)
+  \mathcal{H}\sem{\mathtt{removeBit}(k, c, h)}\sigma
   \;=\;
-  \Big(\mathtt{evalMod}(h, \mathit{env}) - 2^{k}\cdot\bit{c}{\mathit{env}}\Big)
-  \bmod 2^{w}
+  \bigl(\mathcal{H}\sem{h}\sigma
+        - 2^{k}\cdot\lift{\mathcal{C}\sem{c}\sigma}\bigr) \bmod 2^{w}.
 \]
 \end{theorem}
 
-On top of these theorems, we prove that applying a half adder and a full adder preserves the value of the bit heap. 
-These two adders are the building blocks of our compression algorithms (Section~\ref{sec:compression})
+Since a \texttt{Column} is defined as a set, it cannot contain duplicates.
+Therefore, if the same bit is added to a \texttt{Column} at index k, we propagete the bit to the next column, since $2^{k}c + 2^{k}c = 2^{k+1}c$, and the propagation repeats if the next column already contains the circuit as well.
+Effectively this results in building the bit heap in an optimized way during construction.
+\autoref{thm:addBit} is proved by functional induction on \texttt{addBit}, following the carry propagation described above.
+
+
+\subsection{Compression Algorithms}
+\label{sec:compression}
+Compression reduces the height of a bit heap to two, after which a
+single \acrshort{cpa} produces the result \cite{application_specific_arithmetic}.
+The reduction is carried out by compressors, half adders ($2{:}2$),
+full adders ($3{:}2$), or in general any $N{:}M$ compressor with
+$N \ge M$. We formalize half and full adders, and build compressor trees
+from them. However, our framework can easily be extended for any compressor.
 
-\begin{theorem}[\texttt{halfAdder\_correct\_mod}]
-\label{thm:halfAdder-correct}
-For all $h : \mathtt{BitHeap}\;w$, $k : \mathbb{N}$, $i, j : \mathtt{Circuit}$
-with $i, j \in h.\mathtt{get}(k)$ and $i \neq j$,
 \[
-  \forall\, \mathit{env} : \mathtt{BitEnv},
-  \mathtt{evalMod}\big(\mathtt{halfAdder}(k, i, j, h).\mathtt{heap},\, \mathit{env}\big)
-  \;=\;
-  \mathtt{evalMod}(h, \mathit{env})
+\begin{array}{r@{\;}c@{\;}l@{\qquad}l}
+\Step \ni s &::=& \HA(k,c,c) \mid \FA(k,c,c,c) &\\[2pt]
+\Chain \ni S &::=& [\,] \mid s :: S &
+\end{array}
 \]
-\end{theorem}
 
-\begin{theorem}[\texttt{fullAdder\_correct\_mod}]
-  \label{thm:fullAdder-correct}
-For all $h : \mathtt{BitHeap}\;w$, $k : \mathbb{N}$, $i, j, l : \mathtt{Circuit}$
-with $i, j, l \in h.\mathtt{get}(k)$ pairwise distinct,
+Each compression step records the type of adder, the column it acts on, and the bits it consumes. 
+The effects of a single step on the heap with the applicability conditions are shown in Table~\ref{tab:steps}.
+Both applicability conditions are forced by Theorem~\ref{thm:removeBit}, which requires bits to be present and that they are pairwise distinct.
+Writing $s(h)$ for the heap obtained by applying step $s$ to $h$, we prove that each step preserves the value of the heap.
+
+\begin{theorem}[\texttt{halfAdder\_correct\_mod}, \texttt{fullAdder\_correct\_mod}]
+\label{thm:step-correct}
+For all $h : \Heap_w$, $s : \Step$ and
+$\sigma : \mathbb{N} \to \mathbb{B}$, if $s$ is applicable to $h$ by obeying the conditions stated in \ref{tab:steps}, then
 \[
-  \forall\, \mathit{env} : \mathtt{BitEnv},
-  \mathtt{evalMod}\big(\mathtt{fullAdder}(k, i, j, l, h).\mathtt{heap},\, \mathit{env}\big)
-  \;=\;
-  \mathtt{evalMod}(h, \mathit{env})
+ \mathcal{H}\sem{h}\sigma \;=\; \mathcal{H}\sem{s(h)}\sigma.
 \]
 \end{theorem}
 
-A half adder on column $c$ with bits $i$ and $j$ removes both from the column, inserts $i \oplus j$ into column $c$ and $i \wedge j$ into column $c+1$.
-The correctness theorem for the half adder states that the resulting bit heap has the same value modulo $2^w$, under the hypothesis that $i$ and $j$ belong to column $c$ and that they are distinct.
-The membership hypothesis is required by the remove operation, and the uniqueness is needed to ensure we do not remove the same bit twice from the bit heap.
-We know the latter is already satisfied by our implementation of the bit insertion function, and the way we satisfy the former will be explained in \autoref{sec:compression}.
-To prove Theorem~\ref{thm:halfAdder-correct}), we rewrite insertion and removal theorems and the goal becomes an arithmetic identity on boolean values of $i$ and $j$, after which a case split on the boolean values closes the goal.
-The full adder is proved the same way (Theorem~\ref{thm:fullAdder-correct}), with an extra carry-in bit $k$, the sum becomes $i \oplus j \oplus k$, and a carry $(i \wedge j) \vee (i \wedge k) \vee (j \wedge k)$.
-These few definitions and theorems form the basis of our formalization and they provide all the machinery the compression algorithms require.
+With proofs being similar for both half and full adder cases, the proofs rewrite the Theorems \ref{thm:addBit} and \ref{thm:removeBit} until the
+goal becomes an arithmetic identity over the Boolean values of bits, after which a case split on the boolean values closes the goal.
 
+A compression algorithm produces a chain of compressors. 
+Applicability is a condition on the heap the step is applied to, so it must be checked against the intermediate bit heap, not the original.
 
-\subsection{Compression Algorithms}
-\label{sec:compression}
-We implement Wallace and Dadda trees.
-
+\begin{definition}[Well-formed chain]
+\label{def:wellformed-chain}
+A chain $s :: S$ is well-formed for $h$ if $s$ is applicable to $h$ and $S$ is well-formed for $s(h)$.
+\end{definition}
 
-\subsubsection{Correctness of Composition of Adders}
+\begin{theorem}[\texttt{applyChain\_correct\_mod}]
+\label{thm:chain-correct}
+For all $h : \Heap_w$ and $S: \Chain$ is well-formed for $h$,
+\[
+  \forall \sigma,\quad
+  \mathcal{H}\sem{h}\sigma \;=\; \mathcal{H}\sem{S(h)}\sigma.
+\]
+\end{theorem}
 
+\autoref{thm:chain-correct} is proven by induction on the chain, using Theorem~\ref{thm:step-correct} for the base case and the induction hypothesis for the tail of the chain.
 
-Adder: 
+In our framework, we separate the correctness of the compression from the generation of the chain.
+Theorem~\ref{thm:chain-correct} proves that any well-formed chain preserves the value of the heap.
+Therefore, any algorithm producing a well-formed chain is proven correct.
+That means adding a new algorithm does not require any new proof.
+We use this to implement Wallace and Dadda trees against a single correctness theorem.
 
-ChainPreconditions:
-- applyChainSafe: 
+For chains produced by a compression algorithm, we provide a checked application \texttt{applyChainSafe}, which tests applicability at each step and returns $\mathtt{none}$ on failure. 
 
 \subsection{From Bit Heaps to Bit-Vector Arithmetic}
 At the core of our formalization lies the correctness of Bit heap operations with respect to the semantics of bit-vector arithmetic.
 
 \texttt{ArithCircuit}, \texttt{toBitHeap}, \texttt{denote}, \texttt{toBitHeap\_correct}, \texttt{compressed\_toBitHeap\_correct}
 
+
 \section{Integration}
 
 \subsection{Datapath Synthesis Engine}

references.bib

@@ -26,6 +26,15 @@ @ARTICLE{wallace_tree
   keywords={Adders;Acceleration;Arithmetic;Hardware;Investments;Computer peripherals;Circuits;Power generation economics;Contracts;Physics computing},
   doi={10.1109/PGEC.1964.263830}}
 
+@article{dadda_tree,
+  author={Dadda, Luigi},
+  journal={Alta Frequenza},
+  title={Some Schemes for Parallel Multipliers},
+  year={1965},
+  volume={34},
+  number={5},
+  pages={349-356}}
+
 @article{sca,
 author = {Konrad, Alexander and Scholl, Christoph},
 title = {Symbolic computer algebra for multipliers revisited - demonstrating the significance of order and phase optimization},