correctness

Author: osmanyasar05

paper.tex

@@ -774,12 +774,22 @@ \subsection{Compression Algorithms For Fast Arithmetic}
 proven above (\autoref{thm:step-correct}),
 and the induction hypothesis is used to prove that the other steps preserve the value of the heap.
 
-This therefore shows that \emph{any chain} of well-formed compression steps preserves the value of the bit heap.
-We then use this to trivially prove the correctness of the Dadda algorithm.
-It is easy to prove that the Dadda algorithm produces a well-formed chain of compression steps.
-\osman{we need to explain why this is the case, and this part might be connected to the Integration section.}
-However, see that our framework is general,
-and can be used to prove the correctness of any compression algorithm that produces a well-formed chain of compression steps.
+This shows that \emph{any} well-formed chain preserves the value of the bit heap.
+It should we noted that we do not verify compression algorithms themselves.
+But instead we verify that the chain of compressors generated by a compressor algorithm preserves the value at the run-time..
+So we define $\mathsf{applyChainSafe}$, which applies a chain step by step, checks the conditions of each step against the bit heap it
+has reached, and returns $\mathsf{none}$ if a step does not apply.
+We then prove that a successful run preserves the value:
+\[
+  \mathsf{applyChainSafe}(S, h) = \mathsf{some}\ h'
+  \quad\Longrightarrow\quad
+  \forall \sigma,\; \hsem{h'} = \hsem{h}.
+\]
+
+Dadda's algorithm is a plain Lean function with no correctness theorem of its own.
+It proposes a chain, and the check decides whether that chain is used.
+Any other compression algorithm can take its place without further proof, since only the chain it produces is checked.
+This is the check the CIRCT pass of \autoref{sec:integration} runs.
 
 \begin{theorem}[Bit Heap Compression]
 \label{thm:tobitheap-compression}
@@ -799,6 +809,7 @@ \subsection{Compression Algorithms For Fast Arithmetic}
 The next sections will explain the integration into CIRCT and the results of the verified synthesis of multipliers.
 
 \section{Integration}
+\label{sec:integration}
 
 We integrate our verified synthesizer into the CIRCT compiler framework, and make our contributions open-source.
 CIRCT's \texttt{circt-synth} flow lowers the word-level \texttt{comb} dialect to an