# Changeset 3131

Ignore:
Timestamp:
Apr 12, 2013, 6:10:36 PM (5 years ago)
Message:

 r3128 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} 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.)