Index: /Deliverables/D4.4/mauro.tex
===================================================================
 /Deliverables/D4.4/mauro.tex (revision 3221)
+++ /Deliverables/D4.4/mauro.tex (revision 3222)
@@ 7,13 +7,13 @@
An instance of the record \verb=sem_graph_params= contains all common information about
programs of a jointlanguage whose source code can be logically organized as a graph.
Thus, every program of this kind will be an ihabitant of the type \verb=joint_program p=,
where \verb=p= is an istance of \verb=sem_graph_params=. We want to stress that such a record
+Thus, every program of this kind will be an inhabitant of the type \verb=joint_program p=,
+where \verb=p= is an instance of \verb=sem_graph_params=. We want to stress that such a record
is in a subtype relation with the record \verb=params=, which was explained in Deliverable 4.3.
In order to establish the correctness of our costmodel in each compiler's backend pass, where
both source and target programs are jointgraphprograms, i.e. the source program \verb=src=
(resp. the target program \verb=out=) is such that there is a \verb=p_in=
(resp. \verb=p_out=) of type \verb=sem_graph_params= such that
\verb=src : joint_program p_in= (resp. \verb=out : joint_program p_out=), we would like to
+In order to establish the correctness of our costmodel in each compiler's backend pass, where
+both source and target programs are jointgraphprograms, i.e.\ the source program \verb=src=
+(resp.\ the target program \verb=out=) is such that there is a \verb=p_in=
+(resp.\ \verb=p_out=) of type \verb=sem_graph_params= such that
+\verb=src : joint_program p_in= (resp.\ \verb=out : joint_program p_out=), we would like to
prove a statement similar to this shape.
\begin{lstlisting}
@@ 44,28 +44,28 @@
Since traces carry both extensional and intensional information, the main disadvantage
with this approach is that the extensional part of the proof (for example
the preservation the semantical relation between states of the program under evaluation)
and the intensional part (for example, all proof obbligation dealing with
+the preservation the semantic relation between states of the program under evaluation)
+and the intensional part (for example, all proof obligation dealing with
the presence of a cost label in some point of the code) are mixed together in a not very clear way.
Furthermore, some proof obbligations concerning the relation among program counters
+Furthermore, some proof obligations concerning the relation among program counters
(for example, the call relation between states which is one of the field of
\verb=status_rel= record) depend only on the way the translation from source to target program is done.
In particular if the translation satisfies some suitable properties, then it is possible
to define some ``standard relations'' that automatically satisfy these proof obbligations,
+to define some ``standard relations'' that automatically satisfy these proof obligations,
in an independent way from the specific source and target languages.
So our question is wether there is a way to use these observation in order to factorize all common
+So our question is whether there is a way to use these observation in order to factorize all common
aspects of all correctness proofs of each pass involving joint languages.
The aim is having a layer on top of the one talking about traces, that ask the user wishing to prove
the correctness of a single pass involving two jointlanguages, to provide some semnatical state relation that
+the correctness of a single pass involving two jointlanguages, to provide some semantic state relation that
satisfies some conditions. These conditions never speak about traces and they are mostly
extensional, with the intesional part being limited to some additional requirred properties of
the translation. This layer will use the trace machineary in order to deliver the desired correctness
+extensional, with the intensional part being limited to some additional required properties of
+the translation. This layer will use the trace machinery in order to deliver the desired correctness
proof of the pass.
In order to reach this goal, we have to analyze first whether there is a common way to perform language
translation for each pass. After having defined and specified the translation machienary, we will
explain how it is possibile to use it in order to build such a layer. So this section is organized as follows:
in the first part we explain the translation machienary while in the second part we explain such a layer.
+In order to reach this goal, we have to analyse first whether there is a common way to perform language
+translation for each pass. After having defined and specified the translation machinery, we will
+explain how it is possible to use it in order to build such a layer. So this section is organized as follows:
+in the first part we explain the translation machinery while in the second part we explain such a layer.
\subsection{Graph translation}
@@ 73,5 +73,5 @@
translation of a program in terms of the way we translate each internal function. Thus, if we let
\verb=src_g_pars= and \verb=dst_g_pars= being the graph parameters of respectively the source and
the target program, the aim is writing a Matita's function that takes as input an object of type
+the target program, the aim is writing a \s{matita}'s function that takes as input an object of type
\verb=joint_closed_internal_function src_g_pars= together with additional information
(that we will explain better later) and gives as output an object of type
@@ 89,5 +89,4 @@
bind_new_instantiates ?? data' data regs ∧
b_graph_translate_props … data' def_in def_out f_lbls f_regs.
........
\end{lstlisting}
@@ 97,6 +96,7 @@
\subsubsection{Input requested by the translation process}
Clearly, \verb=b_graph_translate= takes as input the internal function of the source language we want to translate.
But it also takes in input some useful infomrmation which will be used in order to dictate the translation process.
These information are all contained in an instance of the following record.
+But it also takes in input some useful information which will be used in order to dictate the translation process.
+These informations are all contained in an instance of the following record,
+where we skip some technical details.
\begin{lstlisting}
@@ 111,29 +111,6 @@
; f_step : label → joint_step src globals → bind_step_block dst globals
; f_fin : label → joint_fin_step src → bind_fin_block dst globals
; good_f_step :
 ∀l,s.bind_new_P' ??
 (λlocal_new_regs,block.let 〈 pref, op, post 〉 ≝ block in
 ∀l.
 let allowed_labels ≝ l :: step_labels … s in
 let allowed_registers ≝ new_regs @ local_new_regs @ step_registers … s in
 All (label → joint_seq ??)
 (λs'.step_labels_and_registers_in … allowed_labels allowed_registers
 (step_seq dst globals (s' l)))
 pref ∧
 step_labels_and_registers_in … allowed_labels allowed_registers (op l) ∧
 All (joint_seq ??)
 (step_labels_and_registers_in … allowed_labels allowed_registers)
 post)
 (f_step l s)
; good_f_fin :
 ∀l,s.bind_new_P' ??
 (λlocal_new_regs,block.let 〈 pref, op 〉 ≝ block in
 let allowed_labels ≝ l :: fin_step_labels … s in
 let allowed_registers ≝ new_regs @ local_new_regs @ fin_step_registers … s in
 All (joint_seq ??)
 (λs.step_labels_and_registers_in … allowed_labels allowed_registers s)
 pref ∧
 fin_step_labels_and_registers_in … allowed_labels allowed_registers op)
 (f_fin l s)
+; good_f_step : …
+; good_f_fin : …
; f_step_on_cost :
∀l,c.f_step l (COST_LABEL … c) =
@@ 146,22 +123,28 @@
}
\end{lstlisting}
We will now summarize what each field means and how it is used in the translation process. We will say that an identifier of
a pseudoregister (resp. a code point) is {\em fresh} when it never appears in the code of the source function.
\begin{center}
\begin{tabular*}{\textwidth}{p{4cm}p{11cm}}
Field & Explanation \\
+\autoref{tab:translate_data} summarizes what each field means and how it is used in the translation process. We will say that an identifier of
+a pseudoregister (resp.\ a code label) is {\em fresh} when it never appears in the code of the source function.
+\begin{table}
+ \centering
+\begin{tabular*}{\textwidth}{@{}p{.25\linewidth}@{}p{.75\linewidth}@{}}
+Field & Explanation \\[5pt]
\hline
\texttt{init\_ret} & It tells how to fill the field \texttt{joint\_if\_result}, i.e. it tells what is the translation of the result for the translated function.\\
\texttt{init\_params} & It tells how to fill the field \texttt{joint\_if\_params}, i.e. it tells what is the translation of the formal parameters of the translated function.\\
\texttt{init\_stack\_size} & It tells how to fill the field \texttt{joint\_if\_stacksize} of the translated function, which is used in orderto deal with cost model of stack usage. \\
\texttt{added\_prologue} & It is a list of sequential statements of the target language which is always added at the beginning of the translated function. \\
\texttt{new\_regs} & It is a list of identifiers for fresh pseudoregisters that are used by statements in \texttt{added\_prologue}. \\
\texttt{f\_step} & It is a function that tells how to translate all {\em step statements} i.e. statements admitting a syntactical successor. Statements of this kind are all sequential statements, a cost emission statement, a call statement and a conditional statement: in the two latter cases the syntactical successors are respectively the returning address (at the end of a function call) and the codepoint of the instruction the execution flow will jump in case the guard of the conditional is evaluated to false. \\
\texttt{f\_fin} & It is a function that tells how to translate all {\em final statements} i.e. statements do not admitting a syntactical successor. Statements of this kind are return statements, unconditioned jump statements and tailcalls.\\
\texttt{good\_f\_step} & It tells that the translation function of all step statement is well formed in the sense that all identifier (pseudoregisters or code points) used by the block of step statements being the translation of a step statement either come from the statement being translated or they are fresh and generated by the universe field of the translated function (\verb=joint_if_luniverse= in case of code point identifier or \verb=joint_if_runiverse= in case of pseudoregister identifier). \\
\texttt{good\_f\_fin} & It tells that the translation function of all final statements is well formed. Such a condition is similar to the one given for step statements.\\
\texttt{f\_step\_on\_cost} and \texttt{cost\_in\_f\_step}& It gives a particular restriction on the translation of a costemission statement: it tells that the translation of a costemission has to be the identity, i.e. it should be translated as the same costemission statement. Furthermore, the translation never introduce new costemission statements which do not correspond to a cost emission in the source.
+\texttt{init\_ret} & It tells where the result for the translated function is stored.\\[5pt]
+\texttt{init\_params} & It tells what is the translation of the formal parameters.\\[5pt]
+\texttt{init\_stack\_size} & It tells how to fill the field \texttt{joint\_if\_stacksize} of the translated function, which tells how much stack is required by the function at the given stage of compilation. \\[5pt]
+\texttt{added\_prologue} & It is a list of sequential statements of the target language which is always added at the beginning of the translated function. \\[5pt]
+\texttt{new\_regs} & It is a list of identifiers for fresh pseudoregisters that are generated when instantiating
+this record. They are typically used to store data that must be saved across the call (e.g.\ the return address
+popped from the internal stack).\\[5pt]
+\texttt{f\_step} & It is a function that tells how to translate all {\em step statements} i.e.\ statements admitting a syntactical successor. Statements of this kind are sequential statements, a cost emission statement, a call statement or a conditional statement: in the two latter cases the syntactical successors are respectively the returning address (at the end of a function call) and the point where the flow will continue in case the guard is false. \\[5pt]
+\texttt{f\_fin} & As above, but for {\em final statements} i.e.\ statements do not admitting a syntactical successor. Statements of this kind are return and unconditioned jump statements.\\[5pt]
+\texttt{good\_f\_step} & It tells that the translation function of all step statement is well formed in the sense that
+the block \verb=f_step I= for a step \verb=I= only uses code labels and register appearing in \verb=I=, \verb=new_regs= or generated by the appropriate identifier universe fields of the translated function. \\[5pt]
+\texttt{good\_f\_fin} & As above, but for \verb=f_fin=.\\[5pt]
+\texttt{f\_step\_on\_cost}, \texttt{cost\_in\_f\_step}& They give a particular restriction on the translation of a costemission statement: it tells that the translation of a costemission has to be the identity, i.e.\ it should be translated as the same costemission statement. Furthermore, the translation never introduce new costemission statements which do not correspond to a cost emission in the source.\\[5pt]
\end{tabular*}
\end{center}
+\caption{The explanation of the various fields of the \verb=b_graph_translate_data= record.}
+\label{tab:translate_data}
+\end{table}
\subsubsection{Output given the translation process}
@@ 184,5 +167,5 @@
instruction of the block has $l$ as code point identifier and all succeeding instructions of the block have
fresh code points identifiers. Furthermore statements of this block may use fresh identifiers of pseudoregisters or
(even worste) they may use some fresh codepoint identifiers being generated by the translation (we will see later
+(even worse) they may use some fresh codepoint identifiers being generated by the translation (we will see later
that this will be important when translating a call statement). We will use the above mentioned functions
to retrieve this information. \verb=f_lbls= takes in input an identifier $l$ for a code point in the
@@ 213,13 +196,13 @@
; freshness_lbls :
(∀l.All …
 (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧
 fresh_for_univ … lbl (joint_if_luniverse … def_out)) (f_lbls l))
+ (λlbl.¬in_universe … lbl (joint_if_luniverse … def_in) ∧
+ in_universe … lbl (joint_if_luniverse … def_out)) (f_lbls l))
; freshness_regs :
(∀l.All …
 (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧
 fresh_for_univ … reg (joint_if_runiverse … def_out)) (f_regs l))
+ (λreg.¬in_universe … reg (joint_if_runiverse … def_in) ∧
+ in_universe … reg (joint_if_runiverse … def_out)) (f_regs l))
; freshness_data_regs :
 All … (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧
 fresh_for_univ … reg (joint_if_runiverse … def_out))
+ All … (λreg.¬in_universe … reg (joint_if_runiverse … def_in) ∧
+ in_universe … reg (joint_if_runiverse … def_out))
(new_regs … data)
; data_regs_disjoint : ∀l,r.r ∈ f_regs l → r ∈ new_regs … data → False
@@ 242,5 +225,5 @@
; prologue_ok :
if not_emptyb … (added_prologue … data) then
 ∃lbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧
+ ∃lbl.¬in_universe … lbl (joint_if_luniverse … def_in) ∧
joint_if_entry … def_out
( 〈 [ ],λ_.COST_LABEL … (get_first_costlabel … def_in),
@@ 250,41 +233,45 @@
}.
\end{lstlisting}

We will now summarize the meaning of each field of the record using the same approach followed
in the previous subsection.
\begin{center}
\begin{tabular*}{\textwidth}{p{4cm}p{11cm}}
Field & Explanation \\
+\autoref{tab:translate_props} summarizes the meaning of each field of the record.
+\begin{table}
+\centering
+\begin{tabular*}{\textwidth}{@{}p{.25\linewidth}@{}p{.75\linewidth}@{}}
+Field & Explanation \\[5pt]
\hline
\texttt{res\_def\_out\_eq} & It tells that the result of the translated function is the one specified in the suitable field of the record of type \verb=b_graph_translate_data= provided in input. \\
\texttt{pars\_def\_out\_eq} & It tells that the formal parameters of the translated function are the one specified in the suitable field of the record of type \verb=b_graph_translate_data= provided in input. \\
\texttt{ss\_def\_out\_eq} & It tells that the \verb=joint_if_stacksize= field of the translated function is the one specified in the suitable field of the record of type \verb=b_graph_translate_data= provided in input. \\
\texttt{partition\_lbls} & All lists of codepoint identifiers generated by distinct code point identifiers of the code of the source internal function are pairwise disjoint and every fresh identifier of the list appears at most once, without any repetition. \\
\texttt{partition\_regs} & All lists of pseudoregister identifiers generated by distinct code point identifiers of the code of the source internal function are pairwise disjoint and every fresh identifier of the list appears at most once, without any repetion. \\
\texttt{freshness\_lbls} & All lists of codepoint identifiers generated by a codepoint of the code of the source internal function are fresh. \\
\texttt{freshness\_regs} & All lists of pseudoregister identifiers generated by a codepoint of the code of the source internal function are fresh. \\
\texttt{freshness\_data\_regs} & All identifiers of pseudoregister being element of the field \texttt{new\_regs} of the record of type \verb=b_graph_translate_data= provided in input are fresh. \\
\texttt{data\_regs\_disjoint} & All identifiers of pseudoregister being element of the field \texttt{new\_regs} of the record of type \verb=b_graph_translate_data= provided in input never appear in any list of pseudoregister identifiers generated by a codepoint of the code of the source internal function. \\
+\texttt{res\_def\_out\_eq}, \texttt{pars\_def\_out\_eq}, \texttt{ss\_def\_out\_eq}&
+The return value location, the formal parameters and the syntactic stack size are
+all as dictated by the corresponding \verb=b_graph_translate_data= fields.\\[5pt]
+\texttt{partition\_lbls}, \texttt{partition\_regs}&
+\verb=f_lbls= and \verb=f_regs= are partial partitions, i.e.\ all lists in their
+image are repetitionfree and disjoint for different input values. \\[5pt]
+\texttt{freshness\_lbls}, \texttt{freshness\_regs}, \texttt{freshness\_data\_regs}&
+All lists of codepoint identifiers and register generated at a source codepoint, and the registers in
+\verb=new_regs= are fresh:
+they were not in the former source universe and they are in the new one.\\[5pt]
+ & All identifiers of pseudoregister being element of the field \texttt{new\_regs} of the record of type \verb=b_graph_translate_data= provided in input are fresh. \\[5pt]
+\texttt{data\_regs\_disjoint} & All pseudoregister in \texttt{new\_regs} never appear in \verb=f_regs=. \\[5pt]
\texttt{multi\_fetch\_ok} & Given a statement $I$ and a codepoint identifier $l$ of the source internal function such that $I$ is located in $l$, if the translation process translate $I$ into a statement block $\langle I_1,\ldots ,I_n\rangle$ then
$f\_lbls(l) = [l_1,\ldots,l_{n1}]$ in the translated source code we have that $I_1$ is located in $l$ with $l1$ as syntactical
successor, $I_2$ is located in $l_1$ with $l_2$ as syntactical successor, and so on with the last statement $I_n$ located in $l_{n1}$
and it may have a syntactical successor depending wether $I$ is a stepstatement or not: in the former case we have that the
syntactical successor of $I_n$ is the syntactical successor of $I$, in the latter case, $I_n$ is a final statement.\\
\texttt{prologue\_ok} & If the field \texttt{added\_prologue} of the record of type \verb=b_graph_translate_data= provided in input is empty, then the codepoint identifier of the first instruction of the translated function is the same of the one of the source internal function. Otherwise the two code points are different, with the first instruction of the translated function being a costemission statement followed by the instructions of \texttt{added\_prologue}; the last instruction of \texttt{added\_prologue} has an identifier $l$ as syntactical successor and $l$ is the same identifier as the one of the first instruction of the source internal function and in $l$ we fetch a NOOP instruction.
+and it may have a syntactical successor depending whether $I$ is a stepstatement or not: in the former case we have that the
+syntactical successor of $I_n$ is the syntactical successor of $I$, in the latter case, $I_n$ is a final statement.\\[5pt]
+\texttt{prologue\_ok} & If the field \texttt{added\_prologue} of the record of type \verb=b_graph_translate_data= provided in input is empty, then the codepoint identifier of the first instruction of the translated function is the same of the one of the source internal function. Otherwise the two code points are different, with the first instruction of the translated function being a costemission statement followed by the instructions of \texttt{added\_prologue}; the last instruction of \texttt{added\_prologue} has an identifier $l$ as syntactical successor and $l$ is the same identifier as the one of the first instruction of the source internal function and in $l$ we fetch a \s{NOP} instruction.
\end{tabular*}
\end{center}
+\caption{The explanation of the various fields of the \verb=b_graph_translate_props= record.}
+\label{tab:translate_props}
+\end{table}
\subsection{A general correctness proof}
In order to prove our general result, we need to define the usual semantical (data) relation among states of the source and target language and call relation between states. We remind that two states are in call relation whenever a call statement is fetched at state's current program counter. These two relations have to satify some condition, already explained at the beginning of this deliverable (see Section ??). In this section we will give some general conditions that these two relations have to satisfy in order to obtain the desired simulation result. We begin our analysis from the latter relation (the call one) and then we show how to relate it with a semantical relation satisfying some conditions that allow us to prove our general result.
+In order to prove our general result, we need to define the usual semantic (data) relation among states of the source and target language and call relation between states. We remind that two states are in call relation whenever a call statement is fetched at state's current program counter. These two relations have to satisfy some condition, already explained at the beginning of this deliverable (see Section ??). In this section we will give some general conditions that these two relations have to satisfy in order to obtain the desired simulation result. We begin our analysis from the latter relation (the call one) and then we show how to relate it with a semantic relation satisfying some conditions that allow us to prove our general result.
\subsubsection{A standard calling relation}
Two states are in call relation whenever it is possible to fetch a call statement at the program counter given by the two states. We will explot the properties of the translation explained in previous subsection in order to define a standard calling relation. We remind that the translation of a given statement $I$ is a block of statements $b= \langle I_1,\ldots I_n\rangle$ with $n \geq 1$. When $I$ is a call, then we will require that there is a unique $k \in [1,n]$ such $I_k$ has to be a call statement (we will see the formalization of this condition in the following subsection when we relate the calling relation with the semantical one). The idea of defining a standard calling relation is to compute the codepoint identifier of this $I_k$, starting from the codepoint identifier of the statement $I$ in the code of the source internal function. We will see how to use the information provided by the translation process (in particular the function \verb=f_lbls=) in order to obtain this result. We will see that, for technical reason, we will compute the code point of $I$ starting from the code point of $I_k$.

In order to explain how this machienary work. we need to enter more in the detail of the translation process. Given a stepstatement
+Two states are in call relation whenever it is possible to fetch a call statement at the program counter given by the two states. We will exploit the properties of the translation explained in previous subsection in order to define a standard calling relation. We remind that the translation of a given statement $I$ is a block of statements $b= \langle I_1,\ldots I_n\rangle$ with $n \geq 1$. When $I$ is a call, then we will require that there is a unique $k \in [1,n]$ such $I_k$ has to be a call statement (we will see the formalization of this condition in the following subsection when we relate the calling relation with the semantic one). The idea of defining a standard calling relation is to compute the codepoint identifier of this $I_k$, starting from the codepoint identifier of the statement $I$ in the code of the source internal function. We will see how to use the information provided by the translation process (in particular the function \verb=f_lbls=) in order to obtain this result. We will see that, for technical reason, we will compute the code point of $I$ starting from the code point of $I_k$.
+
+In order to explain how this machinery work. we need to enter more in the detail of the translation process. Given a stepstatement
$I$, formally its translation is a triple $f\_step(s) = \langle pre,p,post \rangle$ such that $pre$ is a list of sequential
statements called {\em preamble}, $p$ is a stepstatement (we call it {\em pivot}) and $post$ is again a list of sequential statements
called {\em postamble}. When $pre = [s_1,\ldots,s_n]$ and $post = [s_1',\ldots,s_m']$, the corresponding block being the translation
of $I$ is $\langle s_1,\ldots,s_n,p,s_1',\ldots,s_m'\rangle$. In case $I$ is a final statement, than its translation does not have
postable, i.e. it is a pair $f\_fin(s) = \langle pre,p\rangle$ where the pivot $p$ is a final statement.
+postamble, i.e.\ it is a pair $f\_fin(s) = \langle pre,p\rangle$ where the pivot $p$ is a final statement.
Given a statement $I$ at a given code point $l$ in the source internal function and given the pivot statement $p$ of the translation
@@ 292,5 +279,5 @@
in case the preamble is empty, for the property of the translation process we have then $l = l'$, while if the preamble is nonempty.
then $l'$ is $n1$th element of $f\_lbls(l)$, where $n \geq 0$ is the length of the preamble.
The Matita's definition computing the code points according to the above mentioned specification is the following one.
+The \s{matita}'s definition computing the code points according to the above mentioned specification is the following one.
\begin{lstlisting}
definition sigma_label : ∀p_in,p_out : sem_graph_params.
@@ 304,7 +291,7 @@
! ← res_to_opt … (fetch_internal_function …
(joint_globalenv p_in prog stack_size) bl);
! ←
 find ?? (joint_if_code ?? fn)
 (λlbl.λ_.match preamble_length … prog stack_size init init_regs f_regs bl lbl with
+! ← find ?? (joint_if_code ?? fn)
+ (λlbl.λ_.
+ match preamble_length … prog stack_size init init_regs f_regs bl lbl with
[ None ⇒ false
 Some n ⇒ match nth_opt ? n (lbl::(f_lbls bl lbl)) with
@@ 316,5 +303,5 @@
\end{lstlisting}
This function takes in input all the information provided by the translation process (in particular the function $f\_lbls$), a
function location and a codepoint identifier $l$; it fetches the internal function of the source language in the correponding location.
+function location and a codepoint identifier $l$; it fetches the internal function of the source language in the corresponding location.
Then it unfolds the code of the fetched function looking for a label $l'$ and a statement $I$ located in $l'$, such that,
either $l = l'$ in case the preamble of the translation of $I$ is empty or $l'$ is the $n 1$th where $n \geq 0$ is the length
@@ 325,11 +312,10 @@
We can prove that, starting from a code point identifier of the translated internal function,
whenever there exists a codepoint identifier in the source internal function satifying the above condition, then it is always unique.
+whenever there exists a codepoint identifier in the source internal function satisfying the above condition, then it is always unique.
The properties \verb=partition_lbls= and \verb=freshness_lbls= provided by the translation process are crucial in the proof
of this statement.

We can wrap this function inside the definition of the desired relation among program counter states in the following way
+We can wrap this function inside the definition of the desired relation between program counter states in the following way
The conditional at the beginning is put to deal with the premain case, which is translated without following the standard
translation process we explain in previous section.
+translation process we explained in previous section.
\begin{lstlisting}
definition sigma_pc_opt :
@@ 357,6 +343,6 @@
The main result about the program counter relation we have defined is the following. If we fetch a statement $I$ in
at a given program counter $pc$ in the source program, then there is a program counter $pc'$ in the target program
which is in relation with $pc$ (i.e. $sigma\_stored\_pc pc' = pc$) and the fetched statement at $pc'$ is the pivot
statement of the tranlation. The formalization of this statement in Matita is given in the following.
+which is in relation with $pc$ (i.e.\ $sigma\_stored\_pc pc' = pc$) and the fetched statement at $pc'$ is the pivot
+statement of the translation. The formalization of this statement in \s{matita} is given in the following.
\begin{lstlisting}
@@ 404,6 +390,6 @@
(λs1:Σs: (joint_abstract_status (mk_prog_params p_in ??)).as_classifier ? s cl_call.
λs2:Σs:(joint_abstract_status (mk_prog_params p_out ??)).as_classifier ? s cl_call.
pc ? s1 =
 sigma_stored_pc p_in p_out prog stack_sizes init init_regs f_lbls f_regs (pc ? s2)).
+pc ? s1 = sigma_stored_pc
+ p_in p_out prog stack_sizes init init_regs f_lbls f_regs (pc ? s2)).
\end{lstlisting}
@@ 412,7 +398,7 @@
use the translation process we explain in the previous section.
\subsubsection{The semantical relation}
The semantical relation between states is the classical relation used in forward simulation proofs.
It correlates the data of the status (e.g. register, memory, etc.). We remind that the notion of state
+\subsubsection{The semantic relation}
+The semantic relation between states is the classical relation used in forward simulation proofs.
+It correlates the data of the status (e.g. register, memory, \emph{etc}). We remind that the notion of state
in joint language is summarized in the following record.
\begin{lstlisting}
@@ 428,5 +414,5 @@
when executing a return instruction.
The type of the semantical relation between state is the following.
+The type of the semantic relation between state is the following.
\begin{lstlisting}
@@ 435,8 +421,8 @@
\end{lstlisting}
We would like to state some conditions the semantical relation between states have to satisfy in order
+We would like to state some conditions the semantic relation between states have to satisfy in order
to get our simulation result. We would like that this relation have some flavour of compositionality.
In particular we would like that it depends strictly on the contents of the field \verb=st_no_pc=, i.e.
the field that really contains data information of the state. So we need also a data relation, i.e.
+the field that really contains data information of the state. So we need also a data relation, i.e.\
a relation of this type.
@@ 447,6 +433,6 @@
Notice that the data relation cab depend on a specific program counter of the source. This is done
to capture complex data relations like the ones in the ERTL to LTL pass, in which you need to know
where data in pseudoregisters of ERTL are stored by the translation (either in hardware register or
+to capture complex data relations like the ones in the \s{ERTL} to \s{LTL} pass, in which you need to know
+where data in pseudoregisters of \s{ERTL} are stored by the translation (either in hardware register or
in memory) and this information depends on the code point on the statement being translated.
@@ 484,14 +470,14 @@
% \end{lstlisting}
%
Condition \texttt{fetch\_ok\_sigma\_state\_ok} postulates that two state that are in semantical
+Condition \texttt{fetch\_ok\_sigma\_state\_ok} postulates that two state that are in semantic
relation should have their data field also in relation. Condition \texttt{fetch\_ok\_pc\_ok} postulates
that two states that are in semantical relation should have the same program counter. This is due
+that two states that are in semantic relation should have the same program counter. This is due
to the way the translation is performed. In fact a statement $I$ at a code point $l$ in the source
internal function is translated with a block of instructions in the translated internal function
whose initial statement is at the same code point $l$. Condition \texttt{fetch\_ok\_sigma\_last\_pop\_ok}
postulates that two states that are in semantical relation have the last popped calling address
+whose initial statement is at the same code point $l$. The condition \texttt{fetch\_ok\_sigma\_last\_pop\_ok}
+postulates that two states that are in semantic relation have the last popped calling address
in call relation. Finally \texttt{st\_rel\_def} postulates that given two states having the same
program counter, the last pop fields in call relation and the data fields also in data relation, then
they are in semantical relation.
+they are in semantic relation.
Another important condition is that the pivot statement of the translation of a call statement is
@@ 513,5 +499,5 @@
% \end{lstlisting}
The conditions we are going to present now are standard semantical commutation lemmas that are commonly
+The conditions we are going to present now are standard semantic commutation lemmas that are commonly
used when proving the correctness of the operational semantics of many imperative languages. We introduce some notation.
We will use $I,J\ldots$ to range over by statements. We will use $l_1,\ldots,l_n$ to range over by code point identifiers.
@@ 519,5 +505,5 @@
over by states of programs of the source language. We will use $s_2,s_2',s_2'',\ldots$ to range over by
states of programs of the target language. We denote respectively with $\simeq_{S}$, $\simeq_C$ and $\simeq_L$
the semantical relation, the call relation and the costlabel relation between states. These relations have
+the semantic relation, the call relation and the costlabel relation between states. These relations have
been introduced at the beginning of this Deliverable (see Section ??). If $instr = [I_1,\ldots,I_n]$ is a list
of instructions, then we write $s_i \stackrel{instr}{\longrightarrow} s_i'$ ($i \in [1,2]$) when $s_i'$ is
@@ 547,5 +533,5 @@
In order to get the commutation of premain instructions (states whose function location of program counter is 1), we have
to prove the following condition: for all $s_1,s_1',s_2$ such that $s_1 \stackrel{I}{\longrightarrow} s_1'$ and $s_1 \simeq_S s_2$,
then there exists an $s_2'$ such that $s_2 \stackrel{J}{\longrightarrow} s_2'$ and $s_1 \simeq_S s_2'$ i.e. such that the following
+then there exists an $s_2'$ such that $s_2 \stackrel{J}{\longrightarrow} s_2'$ and $s_1 \simeq_S s_2'$ i.e.\ such that the following
diagram commutes.
$$
@@ 578,5 +564,5 @@
\begin{itemize}
\item there are $s_2^{fin}$ and $s_2'$ such that $s_2 \stackrel{\pi_1(f\_step(COND \ r \ l))}{\longrightarrow} s_2^{fin}$,
$s_2^{fin} \stackrel{\pi_2(f\_step(COND \ r \ l))} s_2'$ and $s_1' \simeq_S s_2'$, i.e. the following diagram commutes
+$s_2^{fin} \stackrel{\pi_2(f\_step(COND \ r \ l))} s_2'$ and $s_1' \simeq_S s_2'$, i.e.\ the following diagram commutes
$$
\xymatrix{
@@ 632,5 +618,5 @@
into a list of sequential statements $pre$ \verb=@= $[J]$ \verb=@= $post$. Then we can state the condition in the
following way. For all $s_1,s_1',s_2$ such that $s_1 \stackrel{I}{\longrightarrow} s_1'$ and $s_1 \simeq_S s_2$ then
there is $s_2'$ such that $s_2 \stackrel{f\_step(I)}{\longrightarrow} s_s'$ and $s_1' \simeq_S s_2'$, i.e. such that
+there is $s_2'$ such that $s_2 \stackrel{f\_step(I)}{\longrightarrow} s_s'$ and $s_1' \simeq_S s_2'$, i.e.\ such that
the following diagram commutes.
$$
@@ 673,7 +659,7 @@
\paragraph{Commutation of call statement (\verb=call_commutation=).}
For all $s_1,s_1',s_2$ such that $s_1 \stackrel{CALL \ id \ arg \ dst}{\longrightarrow} s_1'$, $s_1 \simeq_S s_2$ and
the statement fetched in the translated language at the program counter being in call relation
with the program counter of $s_1$ is $\pi_2(f\_step(CALL \ id \ arg \ dst)) = CALL id' \ arg' \ dst'$
+For all $s_1,s_1',s_2$ such that we have $s_1 \stackrel{CALL \ id \ arg \ dst}{\longrightarrow} s_1'$, $s_1 \simeq_S s_2$ and
+the statement fetched in the target function at the program counter in call relation
+with the program counter of $s_1$ is $\pi_2(f\_step(CALL \ id \ arg \ dst)) = CALL \ id' \ arg' \ dst'$
for some $id',ags',dst'$, then there are $s_2^{pre},s_2^{after},s_2'$ such that
\begin{itemize}
@@ 752,5 +738,5 @@
\paragraph{Commutation of return statement (\verb=return_commutation=).}
For all $s_1,s_1',s_2$ such that $s_1 \stackrel{RETURN}{\longrightarrow} s_1'$, $s_1 \simeq_S s_2$, if $CALL \ id \ arg \ dst$
is the call statement that caused the function call ened by the current return (i.e. it is the statement whose code point identifier
+is the call statement that caused the function call ened by the current return (i.e.\ it is the statement whose code point identifier
is the syntactical predecessor of the program counter of $s_1'$), then $\pi_2(f\_fin(RETURN)) = RETURN$, there are
$s_2^{pre},s_2^{after},s_2'$ such that $s_2 \stackrel{\pi_1(f\_fin(RETURN))}{\longrightarrow} s_2^{pre}$,
@@ 818,5 +804,5 @@
\subsubsection{Conclusion}
After having provided a semantic relation among states that satifies some conditions that correspond to
+After having provided a semantic relation among states that satisfies some conditions that correspond to
commutation lemmas that are commonly proved in a forward simulation proof, it is possible to prove the
general theorem. All these condition are summarized in a propositional record called \verb=good_state_relation=.
@@ 843,5 +829,5 @@
R init_in init_out.
\end{lstlisting}
The module formalizing the formal machienary we described in this document consists of about 3000 lines of
Matita code. We stress the fact that this machienary proves general properties that do not depend on the
specific backend graph compiler pass.
+The module formalizing the formal machinery we described in this document consists of about 3000 lines of
+\s{matita} code. We stress the fact that this machinery proves general properties that do not depend on the
+specific backend graph compiler pass.
Index: /Deliverables/D4.4/paolo.tex
===================================================================
 /Deliverables/D4.4/paolo.tex (revision 3221)
+++ /Deliverables/D4.4/paolo.tex (revision 3222)
@@ 11,4 +11,5 @@
\usepackage{listings}
\usepackage[all]{xy}
+% \usepackage{supertabular}
\newcommand{\clap}[1]{\hbox to 0pt{\hss#1\hss}}
@@ 66,5 +67,5 @@
\small Department of Computer Science and Engineering, University of Bologna\\
\small \verb\{Mauro.Piccolo, Claudio.SacerdotiCoen, Paolo.Tranquilli\}@unibo.it}
\title{Certifying the back end pass of the CerCo annotating compiler}
+\title{Certifying the backend pass of the CerCo annotating compiler}
\date{}
@@ 72,9 +73,9 @@
\maketitle
\begin{abstract}
We present the certifying effort of the back end of the CerCo annotating
compiler to 8051 assembly. Apart from the usual effort needed in propagating
+We present the certifying effort of the backend of the CerCo annotating
+compiler to 8051 assembly. Apart from the proofs needed for propagating
the extensional part of execution traces, additional care must be taken in
order to ensure a form of intensional correctness of the pass, necessary to
prove the lifting of computational costs correct. We concentrate here on two
+prove that the lifting of computational costs is correct. We concentrate here on two
aspects of the proof: how stack is dealt with during the pass, and how generic graph
language passes can be proven correct from an extensional and intensional point
@@ 210,5 +211,5 @@
Care must be taken in dealing with the stack. The backend pass produces a
\emph{stack model}: the amount of stack needed by each function (\verb+stack_m+),
together with the maximal usable stack (\verb+max_stack+, $2^{16}$ minus the size occupied by globals).
+together with the maximal usable stack (\verb+max_stack+, $2^{16}$ minus the size occupied by global variables).
While programs in the front end do not fail for stack overflow, the stack
information is lifted to source much in the same ways as time consumption information,
@@ 364,5 +365,5 @@
\label{subfig:stacksame}
\end{subfigure}
\caption{Comparison between using tight stack sizes across langauges, i.e.\
+\caption{Comparison between using tight stack sizes across languages, i.e.\
reading how much stack is required from the function, and using the same
stack sizes provided as a parameter to the semantics. We suppose the call stack
@@ 382,5 +383,5 @@
\subsection{From an unbounded to a bounded stack}
The way the \verb+ft_and_tlr+ is propagated is almost everwhere by means of
+The way the \verb+ft_and_tlr+ is propagated is almost everywhere by means of
the proof of existence of a special relation between states that is a simulation
with respect to execution. There are more details involved than in a usual
@@ 418,5 +419,5 @@
The third one, defined as \verb+RTL_semantics_unique+, switches to a semantics with
a single, bounded stack space, where moreover memory has already been granted to
globals too. From this semantics down to \s{LIN}, all data in memory excluding
+global variables too. From this semantics down to \s{LIN}, all data in memory excluding
pieces of program counters remain the same, as specified in \autoref{subsec:evolvingstack}.
However in order to show a
Index: /Deliverables/D4.4/report.tex
===================================================================
 /Deliverables/D4.4/report.tex (revision 3221)
+++ /Deliverables/D4.4/report.tex (revision 3222)
@@ 1,3 +1,3 @@
\documentclass[11pt, epsf, a4wide]{article}
+\documentclass[12pt]{article}
\usepackage{../style/cerco}
@@ 47,5 +47,5 @@
\begin{document}

+\pagenumbering{roman}
\thispagestyle{empty}
@@ 96,6 +96,5 @@
\newpage

\vspace*{7cm}
+\addcontentsline{toc}{section}{Summary}
\paragraph{Summary}
The deliverable D4.4 is composed of the following parts:
@@ 177,8 +176,8 @@
whole assembler.
\includepdf[pages={}]{itp2013.pdf}
\includepdf[pages={}]{paolo.pdf}
\includepdf[pages={}]{cpp2012asm.pdf}
\includepdf[pages={}]{cpp2012policy.pdf}
+\includepdf[pages={},addtotoc={1,section,1,Certification of the preservation of structure by a compiler's backend pass,simulation}]{itp2013.pdf}
+\includepdf[pages={},addtotoc={1,section,1,Certifying the backend pass of the CerCo annotating compiler,backend}]{paolo.pdf}
+\includepdf[pages={},addtotoc={1,section,1,On the correctness of an optimising assembler for the Intel MCS51 microprocessor,asm}]{cpp2012asm.pdf}
+\includepdf[pages={},addtotoc={1,section,1,On the correctness of a branch displacement algorithm,policy}]{cpp2012policy.pdf}
\end{document}
Index: /Papers/cppasm2012/cpp2012asm.tex
===================================================================
 /Papers/cppasm2012/cpp2012asm.tex (revision 3221)
+++ /Papers/cppasm2012/cpp2012asm.tex (revision 3222)
@@ 42,4 +42,5 @@
\begin{document}
+\pagestyle{plain}
\maketitle
Index: /Papers/itp2013/ccexec.tex
===================================================================
 /Papers/itp2013/ccexec.tex (revision 3221)
+++ /Papers/itp2013/ccexec.tex (revision 3222)
@@ 31,4 +31,5 @@
\begin{document}
+\pagestyle{plain}
\title{Certification of the Preservation of Structure by a Compiler's Backend Pass\thanks{The project CerCo acknowledges the financial support of the Future and