From c847d71d28d2da76f129b6ceb5b885a6c1f0a02f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9ophile=20Bastian?= <contact@tobast.fr>
Date: Sun, 19 Aug 2018 17:09:42 +0200
Subject: [PATCH] Add remarks regarding correctness

---
 report/report.tex | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)

diff --git a/report/report.tex b/report/report.tex
index da95d3f..52741a3 100644
--- a/report/report.tex
+++ b/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}