Index: /Deliverables/D3.4/Report/report.tex
===================================================================
--- /Deliverables/D3.4/Report/report.tex (revision 3130)
+++ /Deliverables/D3.4/Report/report.tex (revision 3131)
@@ -304,5 +304,31 @@
to \textsf{Clight} programs.
-TODO: rest of correctness; discuss full functional correctness
+There is a second part to the statement, which says that the initial
+processing of the input program to produce the cost labelled version
+does not affect the semantics of the program:
+% Yes, I'm paraphrasing the result a tiny bit to remove the observe non-function
+\begin{lstlisting}[language=matita]
+ $\forall$input_program,output.
+ compile input_program = return output $\rightarrow$
+ not_wrong … (exec_inf … clight_fullexec input_program) $\rightarrow$
+ sim_with_labels
+ (exec_inf … clight_fullexec input_program)
+ (exec_inf … clight_fullexec (c_labelled_clight … output))
+\end{lstlisting}
+That is, any successful compilation produces a labelled program that
+has identical behaviour to the original, so long as there is no
+`undefined behaviour'.
+
+Note that this provides full functional correctness, including
+preservation of (non-)termination. The intensional result above does
+not do this directly --- it does not guarantee the same result or same
+termination. There are two mitigating factors, however: first, to
+prove the intensional property you need local simulation results that
+can be pieced together to form full behavioural equivalence, only time
+constraints have prevented us from doing so. Second, if we wish to
+confirm a result, termination, or non-termination we could add an
+observable witness, such as a function that is only called if the
+correct result is given. The intensional result guarantees that the
+observable witness is preserved, so the program must behave correctly.
\section{Intermediate goals for the front-end}
@@ -374,9 +400,9 @@
subtrace.
\item An additional property about the structured trace that no
- `program counter' is repeated between cost labels. Together with
+ `program counter' is \textbf{repeated} between cost labels. Together with
the structure in the trace, this takes over from showing that
cost labelling is sound and precise.
-\item A proof that the observables have been preserved.
-\item A proof that the stack limit is still observed by the prefix and
+\item A proof that the \textbf{observables} have been preserved.
+\item A proof that the \textbf{stack limit} is still observed by the prefix and
the structure trace. (This is largely a consequence of the
preservation of observables.)