Changeset 3131 for Deliverables

Timestamp:

Apr 12, 2013, 6:10:36 PM (8 years ago)

Author:

campbell

Message:

Add rest of correctness.

File:

• Deliverables/D3.4/Report/report.tex (modified) (2 diffs)

Deliverables/D3.4/Report/report.tex

@@ -304 +304 @@
 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 +400 @@
   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.)