Add remarks regarding correctness

report/report.tex

@@ -410,6 +410,14 @@ pointer. The C function representing it will thus take as parameters an array
 of the registers' values as well as an IP, and will return another array of
 registers values, which will represent the evaluated DWARF row.
 
+\subsection{Concerning correctness}\label{ssec:sem_correctness}
+
+The semantics described in this section are designed in a concern of
+\emph{formalization} of the original DWARF standard. This standard, sadly, only
+devises a plain English description of each instruction's action and result,
+which cannot be used as a basis to \emph{prove} anything correct without
+relying on informal interpretations.
+
 \subsection{Original language: DWARF instructions}
 
 These are the DWARF instructions used for CFI description, that is, the
@@ -897,6 +905,24 @@ DWARF data could be efficiently compressed in this way.
                      {src/fib7/fib7.eh_elf_outline.c}
 \end{minipage}
 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Implementation correctness}
+
+The core part of the code, the \texttt{if}/\texttt{else if} bodies, are in
+substance strictly equivalent to what was devised in the semantics in
+Section~\ref{sec:semantics}. Indeed, the semantics were designed \wrt{} C code
+to be able to export them directly to the C code generated by the compiler. As
+a result, this part's proof is limited to checking that no errors were made
+when copying the code snippets.
+
+The only things that remain to be proved are thus code optimisations, namely
+the binary search transformation of the \texttt{switch} statement and the
+outlining. The binary search part proof is a common proof, which in substance
+requires proving that binary search is equivalent to iterative, exhaustive
+search. The outlining only consists in proving that the program flow remains
+unchanged, which is easy to prove.
+
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \section{Benchmarking}\label{sec:benchmarking}