source: Deliverables/D4.4/mauro.tex @ 3213

Last change on this file since 3213 was 3213, checked in by tranquil, 8 years ago

summary for D4.4, and other modifications

File size: 52.6 KB
Line 
1\section{A Modular Approach to the Correctness of the Graph Passes}
2\label{modular}
3
4We will now outline how the proof can be carried out generally in the
5graph passes of the back-end that share the \verb+joint+ language interface.
6
7An instance of the record \verb=sem_graph_params= contains all common information about
8programs of a joint-language whose source code can be logically organized as a graph.
9Thus, every program of this kind will be an ihabitant of the type \verb=joint_program p=,
10where \verb=p= is an istance of \verb=sem_graph_params=. We want to stress that such a record
11is in a sub-type relation with the record \verb=params=, which was explained in  Deliverable 4.3.
12
13In order to establish the correctness of our cost-model in each compiler's backend pass, where
14both source and target programs are joint-graph-programs, i.e. the source program \verb=src=
15(resp. the target program \verb=out=) is such that there is a \verb=p_in=
16(resp. \verb=p_out=) of type \verb=sem_graph_params= such that
17\verb=src : joint_program p_in= (resp. \verb=out : joint_program p_out=), we would like to
18prove a statement similar to this shape.
19\begin{lstlisting}
20theorem joint_correctness : ∀p_in,p_out : sem_graph_params.
21∀prog : joint_program p_in.∀stack_size.
22let trans_prog ≝ transform_program … prog in
23∀init_in.
24make_initial_state (mk_prog_params p_in prog stack_size) = OK ? init_in →
25∃init_out.
26make_initial_state (mk_prog_params p_out trans_prog stack_size) = OK ? init_out ∧
27∃[1] R : status_rel (joint_abstract_status (mk_prog_params p_in prog stack_size))
28          (joint_abstract_status (mk_prog_params p_out trans_prog stack_size)).
29  status_simulation_with_init
30    (joint_abstract_status (mk_prog_params p_in prog stack_size))
31    (joint_abstract_status (mk_prog_params p_out trans_prog stack_size))
32    R init_in init_out.
33\end{lstlisting}
34When proving this statement (for each concrete instance of language),
35we need to proceed by cases according the classification of
36each state in the source program (\verb=cl_jmp=, \verb=cl_other=, \verb=cl_call= and
37\verb=cl_return=) and then prove the suitable conditions explained in
38\cite{simulation}, according to the case we are currently considering (Condition 1 for
39\verb=cl_other= and \verb=cl_jump= case, Condition 2 for \verb=cl_call= or
40Condition 3 for \verb=cl_return= case). Roughly speaking, proving these conditions
41means producing traces of some kind in the target language that are in a suitable
42correspondence with an execution step in the source language.
43
44Since traces carry both extensional and intensional information, the main disadvantage
45with this approach is that the extensional part of the proof (for example
46the preservation the semantical relation between states of the program under evaluation)
47and the intensional part (for example, all proof obbligation dealing with
48the presence of a cost label in some point of the code) are mixed together in a not very clear way.
49
50Furthermore, some proof obbligations concerning the relation among program counters
51(for example, the call relation between states which is one of the field of
52\verb=status_rel= record) depend only on the way the translation from source to target program is done.
53In particular if the translation satisfies some suitable properties, then it is possible
54to define some ``standard relations'' that automatically satisfy these proof obbligations,
55in an independent way from the specific source and target languages.
56
57So our question is wether there is a way to use these observation in order to factorize all common
58aspects of all correctness proofs of each pass involving joint languages.
59The aim is having a layer on top of the one talking about traces, that ask the user wishing to prove
60the correctness of a single pass involving two joint-languages, to provide some semnatical state relation that
61satisfies some conditions. These conditions never speak about traces and they are mostly
62extensional, with the intesional part being limited to some additional requirred properties of
63the translation. This layer will use the trace machineary in order to deliver the desired correctness
64proof of the pass.
65
66In order to reach this goal, we have to analyze first whether there is a common way to perform language
67translation for each pass. After having defined and specified the translation machienary, we will
68explain how it is possibile to use it in order to build such a layer. So this section is organized as follows:
69in the first part we explain the translation machienary while in the second part we explain such a layer.
70
71\subsection{Graph translation}
72Since a program is just a collection of functions, the compositional approach suggests us to define the
73translation of a program in terms of the way we translate each internal function. Thus, if we let
74\verb=src_g_pars= and \verb=dst_g_pars= being the graph parameters of respectively the source and
75the target program, the aim is writing a Matita's function that takes as input an object of type
76\verb=joint_closed_internal_function src_g_pars= together with additional information
77(that we will explain better later) and gives as output an object of type
78\verb=joint_closed_internal_function dst_g_pars= with some properties, that corresponds
79to the result of the translation (for the definition of \verb=joint_closed_internal_function=, see
80Deliverable 4.2 and 4.3) . The signature of the definition is the following one.
81\begin{lstlisting}
82definition b_graph_translate :
83  ∀src_g_pars,dst_g_pars : graph_params.
84  ∀globals: list ident.
85  ∀data : bound_b_graph_translate_data src_g_pars dst_g_pars globals.
86  ∀def_in : joint_closed_internal_function src_g_pars globals.
87  Σdef_out : joint_closed_internal_function dst_g_pars globals.
88  ∃data',regs,f_lbls,f_regs.
89    bind_new_instantiates ?? data' data regs ∧
90    b_graph_translate_props … data' def_in def_out f_lbls f_regs.
91........
92\end{lstlisting}
93
94Let us now discuss in detail what are the parameter to be provide in input and what is the output of the
95translation process.
96
97\subsubsection{Input requested by the translation process}
98Clearly, \verb=b_graph_translate= takes as input the internal function of the source language we want to translate.
99But it also takes in input some useful infomrmation which will be used in order to dictate the translation process.
100These information are all contained in an instance of the following record.
101
102\begin{lstlisting}
103record b_graph_translate_data
104  (src, dst : graph_params)
105  (globals : list ident) : Type[0] ≝
106{ init_ret : call_dest dst
107; init_params : paramsT dst
108; init_stack_size : ℕ
109; added_prologue : list (joint_seq dst globals)
110; new_regs : list register
111; f_step : label → joint_step src globals → bind_step_block dst globals
112; f_fin : label → joint_fin_step src → bind_fin_block dst globals
113; good_f_step :
114  ∀l,s.bind_new_P' ??
115    (λlocal_new_regs,block.let 〈 pref, op, post 〉 ≝ block in
116       ∀l.
117       let allowed_labels ≝ l :: step_labels … s in
118       let allowed_registers ≝ new_regs @ local_new_regs @ step_registers … s in
119       All (label → joint_seq ??)
120         (λs'.step_labels_and_registers_in … allowed_labels allowed_registers
121              (step_seq dst globals (s' l)))
122         pref ∧
123       step_labels_and_registers_in … allowed_labels allowed_registers (op l) ∧
124       All (joint_seq ??)
125         (step_labels_and_registers_in … allowed_labels allowed_registers)
126         post)
127    (f_step l s)
128; good_f_fin :
129  ∀l,s.bind_new_P' ??
130    (λlocal_new_regs,block.let 〈 pref, op 〉 ≝ block in
131       let allowed_labels ≝ l :: fin_step_labels … s in
132       let allowed_registers ≝ new_regs @ local_new_regs @ fin_step_registers … s in
133       All (joint_seq ??)
134         (λs.step_labels_and_registers_in … allowed_labels allowed_registers s)
135         pref ∧
136       fin_step_labels_and_registers_in … allowed_labels allowed_registers op)
137    (f_fin l s)
138; f_step_on_cost :
139  ∀l,c.f_step l (COST_LABEL … c) =
140    bret ? (step_block ??) 〈 [ ], λ_.COST_LABEL dst globals c, [ ] 〉
141; cost_in_f_step :
142  ∀l,s,c.
143  bind_new_P ??
144    (λblock.∀l'.\snd (\fst block) l' = COST_LABEL dst globals c →
145       s = COST_LABEL … c) (f_step l s)
146}
147\end{lstlisting}
148We will now summarize what each field means and how it is used in the translation process. We will say that an identifier of
149a pseudo-register (resp. a code point) is {\em fresh} when it never appears in the code of the source function.
150\begin{center}
151\begin{tabular*}{\textwidth}{p{4cm}p{11cm}}
152Field & Explanation \\
153\hline
154\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.\\
155\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.\\
156\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. \\
157\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. \\
158\texttt{new\_regs} & It is a list of identifiers for fresh pseudo-registers that are used by statements in \texttt{added\_prologue}. \\
159\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 code-point of the instruction the execution flow will jump in case the guard of the conditional is evaluated to false. \\
160\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.\\
161\texttt{good\_f\_step} & It tells that the translation function of all step statement is well formed in the sense that all identifier (pseudo-registers 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 pseudo-register identifier).  \\
162\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.\\
163\texttt{f\_step\_on\_cost} and \texttt{cost\_in\_f\_step}& It gives a particular restriction on the translation of a cost-emission statement: it tells that the translation of a cost-emission has to be the identity, i.e. it should be translated as the same cost-emission statement. Furthermore, the translation never introduce new cost-emission statements which do not correspond to a cost emission in the source.
164\end{tabular*}
165\end{center}
166
167\subsubsection{Output given the translation process}
168Clearly \verb=g_graph_translate= gives in output the translated internal function. Unfortunately,
169for what we are going to develop later, this information is insufficient because we need some information
170about the correspondence between the source internal function and the translated one. Such an information
171is given by the second component of the $\Sigma$-type returned by the translation process.
172We remind that the return type of \verb=b_graph_translate= is the following.
173\begin{lstlisting}
174 Σdef_out : joint_closed_internal_function dst_g_pars globals.
175  ∃data',regs,f_lbls,f_regs.
176    bind_new_instantiates ?? data' data regs ∧
177    b_graph_translate_props … data' def_in def_out f_lbls f_regs.
178\end{lstlisting}
179The correspondence between the source internal function and the translated one is made explicit by two functions:
180\verb=f_lbls : code_point src_g_pars → list (code_point dst_g_pars)= and
181\verb=f_regs :  code_point src_g_pars → list (register)=. To understand their meaning, we need to stress the
182fact that the translation process translates every statement appearing in the code of the source internal function
183in a given code point $l$ into a block of statements in the code of the translated function where the first
184instruction of the block has $l$ as code point identifier and all succeeding instructions of the block have
185fresh code points identifiers. Furthermore statements of this block may use fresh identifiers of pseudo-registers or
186(even worste) they may use some fresh code-point identifiers being generated by the translation (we will see later
187that this will be important when translating a call statement). We will use the above mentioned functions
188to retrieve this information. \verb=f_lbls= takes in input an identifier $l$ for a code point in the
189source code and it gives back the list of all fresh code point identifiers generated by the translation process
190of the statement in the source located in $l$. \verb=f_regs= takes in input an identifier $l$ for a code point
191in the source code and it gives back the list of all fresh register identifiers generated by the translation process
192of the statement in the source located in $l$.
193
194The above mentioned properties about the functions \verb=f_lbls= and \verb=f_regs=, together with some other
195ones, are expressed and formalized by the following propositional record.
196\begin{lstlisting}
197record b_graph_translate_props
198  (src_g_pars, dst_g_pars : graph_params)
199  (globals: list ident)
200  (data : b_graph_translate_data src_g_pars dst_g_pars globals)
201  (def_in : joint_closed_internal_function src_g_pars globals)
202  (def_out : joint_closed_internal_function dst_g_pars globals)
203  (f_lbls : label → list label)
204  (f_regs : label → list register) : Prop ≝
205{ res_def_out_eq :
206           joint_if_result … def_out = init_ret … data
207; pars_def_out_eq :
208           joint_if_params … def_out = init_params … data
209; ss_def_out_eq :
210           joint_if_stacksize … def_out = init_stack_size … data
211; partition_lbls : partial_partition … f_lbls
212; partition_regs : partial_partition … f_regs
213; freshness_lbls :
214  (∀l.All …
215    (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧
216           fresh_for_univ … lbl (joint_if_luniverse … def_out)) (f_lbls l))
217; freshness_regs :
218  (∀l.All …
219    (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧
220           fresh_for_univ … reg (joint_if_runiverse … def_out)) (f_regs l))
221; freshness_data_regs :
222  All … (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧
223               fresh_for_univ … reg (joint_if_runiverse … def_out))
224        (new_regs … data)
225; data_regs_disjoint : ∀l,r.r ∈ f_regs l → r ∈ new_regs … data → False
226; multi_fetch_ok :
227  ∀l,s.stmt_at … (joint_if_code … def_in) l = Some ? s →
228  let lbls ≝ f_lbls l in let regs ≝ f_regs l in
229  match s with
230  [ sequential s' nxt ⇒
231    let block ≝
232      if not_emptyb … (added_prologue … data) ∧
233         eq_identifier … (joint_if_entry … def_in) l then
234        bret … [ ]
235      else
236        f_step … data l s' in
237    l -(block, l::lbls, regs)-> nxt in joint_if_code … def_out
238  | final s' ⇒
239    l -(f_fin … data l s', l::lbls, regs)-> it in joint_if_code … def_out
240  | FCOND abs _ _ _ ⇒ Ⓧabs
241  ]
242; prologue_ok :
243  if not_emptyb … (added_prologue … data) then
244    ∃lbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧
245    joint_if_entry … def_out
246      -( 〈 [ ],λ_.COST_LABEL … (get_first_costlabel … def_in),
247           added_prologue … data 〉,
248        f_lbls … lbl)-> joint_if_entry … def_in in joint_if_code … def_out
249  else (joint_if_entry … def_out = joint_if_entry … def_in)
250}.
251\end{lstlisting}
252
253We will now summarize the meaning of each field of the record using the same approach followed
254in the previous subsection.
255\begin{center}
256\begin{tabular*}{\textwidth}{p{4cm}p{11cm}}
257Field & Explanation \\
258\hline
259\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. \\
260\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. \\
261\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. \\
262\texttt{partition\_lbls} & All lists of code-point 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. \\
263\texttt{partition\_regs} & All lists of pseudo-register 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. \\
264\texttt{freshness\_lbls} & All lists of code-point identifiers generated by a code-point of the code of the source internal function are fresh.  \\
265\texttt{freshness\_regs} & All lists of pseudo-register identifiers generated by a code-point of the code of the source internal function are fresh.  \\
266\texttt{freshness\_data\_regs} & All identifiers of pseudo-register being element of the field \texttt{new\_regs} of the record of type \verb=b_graph_translate_data= provided in input are fresh. \\
267\texttt{data\_regs\_disjoint} &  All identifiers of pseudo-register 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 pseudo-register identifiers generated by a code-point of the code of the source internal function. \\
268\texttt{multi\_fetch\_ok} & Given a statement $I$ and a code-point 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
269$f\_lbls(l) = [l_1,\ldots,l_{n-1}]$ in the translated source code we have that $I_1$ is located in $l$ with $l1$ as syntactical
270successor, $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_{n-1}$
271and it may have a syntactical successor depending wether $I$ is a step-statement or not: in the former case we have that the
272syntactical successor of $I_n$ is the syntactical successor of $I$, in the latter case, $I_n$ is a final statement.\\ 
273\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 code-point 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 cost-emission 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.
274\end{tabular*}
275\end{center}
276
277\subsection{A general correctness proof}
278In 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.
279
280\subsubsection{A standard calling relation}
281Two 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 code-point identifier of this $I_k$, starting from the code-point 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$.
282
283In order to explain how this machienary work. we need to enter more in the detail of the translation process. Given a step-statement
284$I$, formally its translation is a triple $f\_step(s) = \langle pre,p,post \rangle$ such that $pre$ is a list of sequential
285statements called {\em preamble}, $p$ is a step-statement (we call it {\em pivot}) and $post$ is again a list of sequential statements
286called {\em postamble}. When $pre = [s_1,\ldots,s_n]$ and $post = [s_1',\ldots,s_m']$, the corresponding block being the translation
287of $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
288postable, i.e. it is a pair $f\_fin(s) = \langle pre,p\rangle$ where the pivot $p$ is a final statement.
289
290Given a statement $I$ at a given code point $l$ in the source internal function and given the pivot statement $p$ of the translation
291of $I$ staying at code-point $l'$ in the translated internal function, there is an easy way to relate $l$ and $l'$. Notice that,
292in case the preamble is empty, for the property of the translation process we have then $l = l'$, while if the preamble is non-empty.
293then $l'$ is $n-1$-th element of $f\_lbls(l)$, where $n \geq 0$ is the length of the preamble.
294The Matita's definition computing the code points according to the above mentioned specification is the following one.
295\begin{lstlisting}
296definition sigma_label : ∀p_in,p_out : sem_graph_params.
297joint_program p_in → (ident → option ℕ) →
298(∀globals.joint_closed_internal_function p_in globals
299         →bound_b_graph_translate_data p_in p_out globals) →
300(block → list register) → lbl_funct_type → regs_funct_type →
301block → label → option label ≝
302λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,bl,searched.
303! bl ← code_block_of_block bl ;
304! <id,fn> ← res_to_opt … (fetch_internal_function …
305                           (joint_globalenv p_in prog stack_size) bl);
306! <res,s> ←
307 find ?? (joint_if_code ?? fn)
308  (λlbl.λ_.match preamble_length … prog stack_size init init_regs f_regs bl lbl with
309             [ None ⇒ false
310             | Some n ⇒ match nth_opt ? n (lbl::(f_lbls bl lbl)) with
311                         [ None ⇒ false
312                         | Some x ⇒ eq_identifier … searched x
313                         ]
314             ]);
315return res.
316\end{lstlisting}
317This function takes in input all the information provided by the translation process (in particular the function $f\_lbls$), a
318function location and a code-point identifier $l$; it fetches the internal function of the source language in the correponding location.
319Then it unfolds the code of the fetched function looking for a label $l'$ and a statement $I$ located in $l'$, such that,
320either $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
321of the preamble of $I$. The function $find$ is the procedure realizing this search. If $preamble\_length$ is the function giving in
322output the length of the preamble and if $nth\_opt$ is the function giving the $n$-th element of a list, then this condition can
323be summarized as following: we are looking for a label $l'$ such that $l$ is the $n$-th element of the list $l :: f\_lbls (l)$,
324where $n$ is the length of the preamble.
325
326We can prove that, starting from a code point identifier of the translated internal function,
327whenever there exists a code-point identifier in the source internal function satifying the above condition, then it is always unique.
328The properties \verb=partition_lbls= and \verb=freshness_lbls= provided by the translation process are crucial in the proof
329of this statement.
330
331We can wrap this function inside the definition of the desired relation among program counter states in the following way
332The conditional at the beginning is put to deal with the pre-main case, which is translated without following the standard
333translation process we explain in previous section.
334\begin{lstlisting}
335definition sigma_pc_opt : 
336∀p_in,p_out : sem_graph_params.
337joint_program p_in → (ident → option ℕ) →
338(∀globals.joint_closed_internal_function p_in globals
339         →bound_b_graph_translate_data p_in p_out globals) →
340(block → list register) → lbl_funct_type → regs_funct_type →
341program_counter → option program_counter ≝
342λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc.
343let target_point ≝ point_of_pc p_out pc in
344if eqZb (block_id (pc_block pc)) (-1) then
345 return pc
346else
347 ! source_point ← sigma_label p_in p_out prog stack_size init init_regs
348                   f_lbls f_regs (pc_block pc) target_point;
349 return pc_of_point p_in (pc_block pc) source_point.
350
351definition sigma_stored_pc ≝
352λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc.
353match sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc with
354      [None ⇒ null_pc (pc_offset … pc) | Some x ⇒ x].
355\end{lstlisting}
356
357The main result about the program counter relation we have defined is the following. If we fetch a statement $I$ in
358at a given program counter $pc$ in the source program, then there is a program counter $pc'$ in the target program
359which is in relation with $pc$ (i.e. $sigma\_stored\_pc pc' = pc$) and the fetched statement at $pc'$ is the pivot
360statement of the tranlation. The formalization of this statement in Matita is given in the following.
361
362\begin{lstlisting}
363lemma fetch_statement_sigma_stored_pc :
364∀p_in,p_out,prog,stack_sizes,
365init,init_regs,f_lbls,f_regs,pc,f,fn,stmt.
366b_graph_transform_program_props p_in p_out stack_sizes
367  init prog init_regs f_lbls f_regs →
368block_id … (pc_block pc) ≠ -1 →
369let trans_prog ≝ b_graph_transform_program p_in p_out init prog in
370fetch_statement p_in … (joint_globalenv p_in prog stack_sizes) pc =
371return 〈 f,fn,stmt 〉 →
372∃data.bind_instantiate ?? (init … fn) (init_regs (pc_block pc)) = return data ∧
373match stmt with
374[ sequential step nxt ⇒
375   ∃step_block : step_block p_out (prog_names … trans_prog).
376   bind_instantiate ?? (f_step … data (point_of_pc p_in pc) step)
377                 (f_regs (pc_block pc) (point_of_pc p_in pc)) = return step_block ∧
378   ∃pc'.sigma_stored_pc p_in p_out prog stack_sizes init
379                                           init_regs f_lbls f_regs pc' = pc ∧
380   ∃fn',nxt'.
381   fetch_statement p_out … (joint_globalenv p_out trans_prog stack_sizes) pc' =
382   if not_emptyb … (added_prologue … data) ∧
383      eq_identifier … (point_of_pc p_in pc) (joint_if_entry … fn)
384   then OK ? <f,fn',sequential ?? (NOOP …) nxt'>
385   else OK ? <f,fn',
386             sequential ?? ((\snd(\fst step_block)) (point_of_pc p_in pc')) nxt'>
387| final fin ⇒
388    ∃fin_block.bind_instantiate ?? (f_fin … data (point_of_pc p_in pc) fin)
389                  (f_regs (pc_block pc) (point_of_pc p_in pc)) = return fin_block ∧
390    ∃pc'.sigma_stored_pc p_in p_out prog stack_sizes init
391                                           init_regs f_lbls f_regs pc' = pc ∧
392    ∃fn'.fetch_statement p_out …
393       (joint_globalenv p_out trans_prog stack_sizes) pc'
394       = return 〈 f,fn',final ?? (\snd fin_block) 〉
395| FCOND abs _ _ _ ⇒ Ⓧabs
396].
397\end{lstlisting}
398
399If we combine the statement above with the fact that the pivot statement of the translation
400of a call statement is always a call statement (which we will formalize better in the
401following section), then we can define our standard calling relation in the following way.
402
403\begin{lstlisting}
404(λs1:Σs: (joint_abstract_status (mk_prog_params p_in ??)).as_classifier ? s cl_call.
405 λs2:Σs:(joint_abstract_status (mk_prog_params p_out ??)).as_classifier ? s cl_call.
406pc ? s1 =
407 sigma_stored_pc p_in p_out prog stack_sizes init init_regs f_lbls f_regs (pc ? s2)).
408\end{lstlisting}
409
410We stress the fact that such a call relation will be always defined in this way for all joint-languages,
411in an independent way from the specific pass. The only condition we will ask is that the pass should
412use the translation process we explain in the previous section.
413
414\subsubsection{The semantical relation}
415The semantical relation between states is the classical relation used in forward simulation proofs.
416It correlates the data of the status (e.g. register, memory, etc.). We remind that the notion of state
417in joint language is summarized in the following record.
418\begin{lstlisting}
419record state_pc (semp : sem_state_params) : Type[0] ≝
420  { st_no_pc :> state semp
421  ; pc : program_counter
422  ; last_pop : program_counter
423  }.
424\end{lstlisting}
425It consists of three fields: the field \verb=st_no_pc= contains all data information of the state
426(the content of the registers, of the memory and so on), the field \verb=pc= contains the current
427program counter, while the field \verb=last_pop= is the address of the last popped calling address
428when executing a return instruction.
429
430The type of the semantical relation between state is the following.
431
432\begin{lstlisting}
433definition joint_state_pc_relation ≝
434λP_in,P_out : sem_graph_params.state_pc P_in → state_pc P_out → Prop.
435\end{lstlisting}
436
437We would like to state some conditions the semantical relation between states have to satisfy in order
438to get our simulation result. We would like that this relation have some flavour of compositionality.
439In particular we would like that it depends strictly on the contents of the field \verb=st_no_pc=, i.e.
440the field that really contains data information of the state. So we need also a data relation, i.e.
441a relation of this type.
442
443\begin{lstlisting}
444definition joint_state_relation ≝
445λP_in,P_out.program_counter → state P_in → state P_out → Prop.
446\end{lstlisting}
447
448Notice that the data relation cab depend on a specific program counter of the source. This is done
449to capture complex data relations like the ones in the ERTL to LTL pass, in which you need to know
450where data in pseudoregisters of ERTL are stored by the translation (either in hardware register or
451in memory) and this information depends on the code point on the statement being translated.
452
453The compositionality requirement is expressed by several conditions (which are part of a bigger
454record).
455%
456% \begin{lstlisting}
457% ; fetch_ok_sigma_state_ok :
458%    ∀st1,st2,f,fn. st_rel st1 st2 →
459%     fetch_internal_function …
460%      (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 
461%      = return <f,fn> →
462%      st_no_pc_rel (pc … st1) (st_no_pc … st1) (st_no_pc … st2)
463% ; fetch_ok_pc_ok :
464%   ∀st1,st2,f,fn.st_rel st1 st2 →
465%    fetch_internal_function …
466%      (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 
467%      = return <f,fn> →
468%    pc … st1 = pc … st2
469% ; fetch_ok_sigma_last_pop_ok :
470%   ∀st1,st2,f,fn.st_rel st1 st2 →
471%    fetch_internal_function …
472%      (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 
473%      = return <f,fn> →
474%    (last_pop … st1) = sigma_stored_pc P_in P_out prog stack_sizes init init_regs
475%                        f_lbls f_regs (last_pop … st2)
476% ; st_rel_def :
477%   ∀st1,st2,pc,lp1,lp2,f,fn.
478%   fetch_internal_function …
479%      (joint_globalenv P_in prog stack_sizes) (pc_block pc) = return <f,fn> →
480%    st_no_pc_rel pc st1 st2 →
481%    lp1 = sigma_stored_pc P_in P_out prog stack_sizes init init_regs
482%           f_lbls f_regs lp2 →
483%   st_rel (mk_state_pc ? st1 pc lp1) (mk_state_pc ? st2 pc lp2)
484% \end{lstlisting}
485%
486Condition \texttt{fetch\_ok\_sigma\_state\_ok} postulates that two state that are in semantical
487relation should have their data field also in relation. Condition \texttt{fetch\_ok\_pc\_ok} postulates
488that two states that are in semantical relation should have the same program counter. This is due
489to the way the translation is performed. In fact a statement $I$ at a code point $l$ in the source
490internal function is translated with a block of instructions in the translated internal function
491whose initial statement is at the same code point $l$. Condition \texttt{fetch\_ok\_sigma\_last\_pop\_ok} 
492postulates that two states that are in semantical relation have the last popped calling address
493in call relation. Finally \texttt{st\_rel\_def} postulates that given two states having the same
494program counter, the last pop fields in call relation and the data fields also in data relation, then
495they are in semantical relation.
496
497Another important condition is that the pivot statement of the translation of a call statement is
498always a call statement. This is important in order to obtain the correctness of the call relation
499and return relation between state. % This condition is formalized by the following Matita's code, and
500We call this condition \texttt{call\_is\_call}.
501
502% \begin{lstlisting}
503% ;  call_is_call :∀f,fn,bl.
504%   fetch_internal_function …
505%      (joint_globalenv P_in prog stack_sizes) bl = return <f,fn> →
506%    ∀id,args,dest,lbl.
507%     bind_new_P' ??
508%      (λregs1.λdata.bind_new_P' ??
509%       (λregs2.λblp.
510%         ∀lbl.∃id',args',dest'.((\snd (\fst blp)) lbl) = CALL P_out ? id' args' dest')
511%       (f_step … data lbl (CALL P_in ? id args dest)))
512%      (init ? fn)
513% \end{lstlisting}
514
515The conditions we are going to present now are standard semantical commutation lemmas that are commonly
516used when proving the correctness of the operational semantics of many imperative languages. We introduce some notation.
517We 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.
518We will use $r_1,\ldots,r_n$ to range over by register identifiers. We will use $s_1,s_1',s_1'',\ldots$ to range
519over by states of programs of the source language. We will use $s_2,s_2',s_2'',\ldots$ to range over by
520states of programs of the target language. We denote respectively with $\simeq_{S}$, $\simeq_C$ and $\simeq_L$ 
521the semantical relation, the call relation and the cost-label relation between states. These relations have
522been introduced at the beginning of this Deliverable (see Section ??). If $instr = [I_1,\ldots,I_n]$ is a list
523of instructions, then we write $s_i \stackrel{instr}{\longrightarrow} s_i'$ ($i \in [1,2]$) when $s_i'$ is
524the state being the result of the evaluation of the sequence of instructions $instr$ (performed in the order
525they appear in the list) starting from the initial state $s_i$. When $instr = [I]$ is a singleton, we use
526to omit square brackets and we write $s_i \stackrel{I}{\longrightarrow} s_i'$.
527We will denote with $\pi_i$ ($i \in [1,t]$) the projecting functions of $t$-uples. We will denote with $f\_step$ and $f\_fin$
528the translating functions of respectively step-statements and final statements. We remind that $f\_step$ gives
529a triple as output (a list of instruction called preamble,an instruction called pivot and a list of instructions
530called postamble) while $f\_fin$ gives a pair as output (a list of instruction called preamble and an instruction
531called pivot). Furthermore, we denote with $prologue$ the content of the field \texttt{added\_prologue} of the record
532provided in input to the translation process.
533
534Many commutation conditions can be depicted using diagrams. We will use them to give a pictorial flavour of the conditions
535we will ask in order to obtain the final correctness statement. Given the states $s_1,s_1',s_2,s_2'$ and the instructions
536$I,J_1,\ldots,J_k$, the following diagram
537$$
538\xymatrix{
539s_1 \ar@{->}[rr]^{I} \ar@{-}[d]^{\simeq_S} && s_1' \ar@{-}[d]^{\simeq_S}\\
540s_2 \ar[rr]^{[J_1,\ldots,J_k]} && s_2'
541}
542$$
543depicts a situation in which the state $s_1 \stackrel{I}{\longrightarrow} s_1'$, $s_2 \stackrel{I}{\longrightarrow} s_2'$,
544$s_1 \simeq_S s_2$ and $s_1' \simeq_S s_2'$.
545
546\paragraph{Commutation of pre-main instructions (\verb=pre_main_ok=).}
547In order to get the commutation of pre-main instructions (states whose function location of program counter is -1), we have
548to 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$,
549then 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
550diagram commutes.
551$$
552\xymatrix{
553s_1 \ar@{->}[rr]^{I} \ar@{-}[d]^{\simeq_S} && s_1' \ar@{-}[d]^{\simeq_S}\\
554s_2 \ar[rr]^{J} && s_2'
555}
556$$
557% The formalization of this statement in Matita is the following one.
558% \begin{lstlisting}
559% ; pre_main_ok :
560%   let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
561%     ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
562%     ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
563%     block_id … (pc_block (pc … st1)) = -1 →
564%     st_rel st1 st2 →
565%     as_label (joint_status P_in prog stack_sizes) st1 =
566%     as_label (joint_status P_out trans_prog stack_sizes) st2 ∧
567%     joint_classify … (mk_prog_params P_in prog stack_sizes) st1 =
568%     joint_classify … (mk_prog_params P_out trans_prog stack_sizes) st2 ∧
569%     (eval_state P_in … (joint_globalenv P_in prog stack_sizes)
570%       st1 = return st1' →
571%     ∃st2'. st_rel st1' st2' ∧
572%     eval_state P_out …
573%      (joint_globalenv P_out trans_prog stack_sizes) st2 = return st2')
574% \end{lstlisting}
575
576\paragraph{Commutation of conditional jump (\verb=cond_commutation=).}
577For all $s_1,s_1'$ and $s_2$ such that $s_1 \stackrel{COND \ r \ l}{\longrightarrow} s_1'$ and $s_1 \simeq_S s_2$ then
578\begin{itemize}
579\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}$,
580$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
581$$
582\xymatrix{
583s_1 \ar@{->}[rrrrrr]^{COND \ l \ r} \ar@{-}[d]^{\simeq_S} &&&&&& s_1' \ar@{-}[d]^{\simeq_S}\\
584s_2 \ar[rrr]^{\pi_1(f\_step(COND \ r \ l))} &&& s_2^{fin} \ar[rrr]^{\pi_2(f\_step(COND \ r \ l))} &&& s_2'
585}
586$$
587\item $\pi_3(f\_step(COND \ r \ l))$ is empty, while $\pi_2(f\_step(COND \ r \ l)) = COND \ r' \ l'$ is a conditional jump
588      such that $l = l'$.
589\end{itemize}
590% This condition is formalized in Matita in the following way.
591% \begin{lstlisting}
592% ; cond_commutation :
593%     let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
594%     ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
595%     ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
596%     ∀f,fn,a,ltrue,lfalse,bv,b.
597%     block_id … (pc_block (pc … st1)) ≠ -1 →
598%     let cond ≝ (COND P_in ? a ltrue) in
599%     fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
600%     return <f, fn,  sequential … cond lfalse> → 
601%     acca_retrieve … P_in (st_no_pc … st1) a = return bv →
602%     bool_of_beval … bv = return b →
603%     st_rel st1 st2 →
604%     ∀t_fn.
605%     fetch_internal_function …
606%      (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) =
607%      return 〈 f,t_fn 〉 →
608%     bind_new_P' ??
609%      (λregs1.λdata.bind_new_P' ??
610%      (λregs2.λblp.(\snd blp) = [ ] ∧
611%         ∀mid.
612%           stmt_at P_out … (joint_if_code ?? t_fn) mid
613%           = return sequential P_out ? ((\snd (\fst blp)) mid) lfalse→
614%          ∃st2_pre_mid_no_pc.
615%             repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f
616%              (map_eval ?? (\fst (\fst blp)) mid) (st_no_pc ? st2)
617%             = return st2_pre_mid_no_pc ∧
618%             let new_pc ≝ if b then
619%                            (pc_of_point P_in (pc_block (pc … st1)) ltrue)
620%                          else
621%                            (pc_of_point P_in (pc_block (pc … st1)) lfalse) in
622%             st_no_pc_rel new_pc (st_no_pc … st1) (st2_pre_mid_no_pc) ∧
623%             ∃a'. ((\snd (\fst blp)) mid)  = COND P_out ? a' ltrue ∧
624%             ∃bv'. acca_retrieve … P_out st2_pre_mid_no_pc a' = return bv' ∧
625%                   bool_of_beval … bv' = return b
626%    )  (f_step … data (point_of_pc P_in (pc … st1)) cond)   
627%   ) (init ? fn)
628% \end{lstlisting}
629
630\paragraph{Commutation of sequential statements (\verb=seq_commutation=).}
631In case of a sequential statement $I$, its translation $f\_step(I) = \langle pre , J , post \rangle$ is coerced
632into a list of sequential statements $pre$ \verb=@= $[J]$ \verb=@= $post$. Then we can state the condition in the
633following 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
634there 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
635the following diagram commutes.
636$$
637\xymatrix{
638s_1 \ar@{->}[rr]^{I} \ar@{-}[d]^{\simeq_S}  && s_1' \ar@{-}[d]^{\simeq_S}\\
639s_2 \ar[rr]^{f\_step(I)} && s_2'
640}
641$$
642% The formalization in Matita of the above statement is as follows.
643% \begin{lstlisting}
644% ; seq_commutation :
645%   let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
646%   ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
647%   ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
648%   ∀f,fn,stmt,nxt.
649%   block_id … (pc_block (pc … st1)) ≠ -1 →
650%   let seq ≝ (step_seq P_in ? stmt) in
651%   fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
652%   return <f, fn,  sequential … seq nxt> → 
653%   eval_state P_in … (joint_globalenv P_in prog stack_sizes)
654%   st1 = return st1' →
655%   st_rel st1 st2 →
656%   ∀t_fn.
657%   fetch_internal_function …
658%      (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) =
659%   return <f,t_fn> →
660%   bind_new_P' ??
661%      (λregs1.λdata.bind_new_P' ??
662%       (λregs2.λblp.
663%        ∃l : list (joint_seq P_out
664%                   (globals ? (mk_prog_params P_out trans_prog stack_sizes))).
665%                             blp = (ensure_step_block ?? l) ∧
666%        ∃st2_fin_no_pc.
667%            repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f
668%               l  (st_no_pc … st2)= return st2_fin_no_pc ∧
669%            st_no_pc_rel (pc … st1') (st_no_pc … st1') st2_fin_no_pc
670%       ) (f_step … data (point_of_pc P_in (pc … st1)) seq)
671%      ) (init ? fn)
672% \end{lstlisting}
673
674\paragraph{Commutation of call statement (\verb=call_commutation=).}
675For 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
676the statement fetched in the translated language at the program counter being in call relation
677with the program counter of $s_1$ is $\pi_2(f\_step(CALL \ id \ arg \ dst)) = CALL id' \ arg' \ dst'$ 
678for some $id',ags',dst'$, then there are $s_2^{pre},s_2^{after},s_2'$ such that
679\begin{itemize}
680\item $s_2 \stackrel{\pi_1(f\_step(CALL \ id \ arg \ dst))}{\longrightarrow} s_2^{pre}$,
681\item $s_2^{pre} \stackrel{CALL \ id' \arg' \ dst'}{\longrightarrow} s_2^{after}$,
682\item $s_2^{after} \stackrel{prologue}{\longrightarrow} s_2'$,
683\item $s_1' \simeq_L s_2^{after}$ and $s_1' \simeq_S s_2'$.
684\end{itemize}
685The situation is depicted by the following diagram.
686$$
687\xymatrix{
688s_1 \ar@{-}[d]^{\simeq_S} \ar@{-}[d]^{\simeq_S} \ar[rrrrrrrrrr]^{CALL \ id \ arg \ dst}  &&&&&&&&&&  s_1' \ar@{-}[d]^{\simeq_S} \\
689s_2 \ar[rrrr]^{\pi_1(f\_step(CALL \ id \ arg \ dst))} &&&& s_2^{pre} \ar[rrr]^{CALL \ id' \ arg' \ dst'} &&& s_2^{after} \ar[rrr]^{prologue} &&& s_2'
690}
691$$
692% The statement is formalized in Matita in the following way.
693% \begin{lstlisting}
694% ; call_commutation :
695%   let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
696%   ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
697%   ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
698%   ∀f,fn,id,arg,dest,nxt.
699%   block_id … (pc_block (pc … st1)) ≠ -1 →
700%   fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
701%   return 〈 f, fn,  sequential P_in ? (CALL P_in ? id arg dest) nxt 〉 →
702%   ∀bl.
703%    block_of_call P_in … (joint_globalenv P_in prog stack_sizes) id (st_no_pc … st1)
704%       = return bl →
705%   ∀f1,fn1.
706%    fetch_internal_function …
707%     (joint_globalenv P_in prog stack_sizes) bl =  return 〈 f1,fn1 〉 →
708%   ∀st1_pre.
709%   save_frame … P_in (kind_of_call P_in id) dest st1 = return st1_pre →
710%   ∀n.stack_sizes f1 = return n → 
711%   ∀st1'.
712%   setup_call ?? P_in n (joint_if_params … fn1) arg st1_pre = return st1' →
713%   st_rel st1 st2 → 
714%   ∀t_fn1.
715%   fetch_internal_function … (joint_globalenv P_out trans_prog stack_sizes) bl =
716%   return 〈 f1,t_fn1 〉 →
717%   bind_new_P' ??
718%     (λregs1.λdata.
719%      bind_new_P' ??
720%       (λregs2.λblp.
721%         ∀pc',t_fn,id',arg',dest',nxt1.
722%           sigma_stored_pc P_in P_out prog stack_sizes init init_regs
723%            f_lbls f_regs pc' = (pc … st1) →
724%           fetch_statement P_out … (joint_globalenv P_out trans_prog stack_sizes) pc'
725%           = return 〈 f,t_fn,
726%                     sequential P_out ? ((\snd (\fst blp)) (point_of_pc P_out pc')) nxt1 〉→
727%           ((\snd (\fst blp)) (point_of_pc P_out pc')) = (CALL P_out ? id' arg' dest') → 
728%        ∃st2_pre_call.
729%         repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f
730%           (map_eval ?? (\fst (\fst blp)) (point_of_pc P_out pc')) (st_no_pc ? st2) = return st2_pre_call ∧
731%        block_of_call P_out … (joint_globalenv P_out trans_prog stack_sizes) id'
732%         st2_pre_call = return bl ∧
733%        ∃st2_pre.
734%         save_frame … P_out (kind_of_call P_out id') dest'
735%          (mk_state_pc ? st2_pre_call pc' (last_pop … st2)) = return st2_pre ∧
736%        ∃st2_after_call.
737%          setup_call ?? P_out n (joint_if_params … t_fn1) arg' st2_pre
738%           = return st2_after_call ∧
739%        bind_new_P' ??
740%          (λregs11.λdata1.
741%           ∃st2'.
742%            repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f1
743%            (added_prologue … data1) (increment_stack_usage P_out n st2_after_call) =
744%            return st2' ∧
745%            st_no_pc_rel (pc_of_point P_in bl (joint_if_entry … fn1))
746%             (increment_stack_usage P_in n st1') st2'               
747%          ) (init ? fn1)
748%      )
749%      (f_step … data (point_of_pc P_in (pc … st1)) (CALL P_in ? id arg dest))
750%     ) (init ? fn)
751% \end{lstlisting}
752\paragraph{Commutation of return statement (\verb=return_commutation=).}
753For 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$
754is the call statement that caused the function call ened by the current return (i.e. it is the statement whose code point identifier
755is the syntactical predecessor of the program counter of $s_1'$), then $\pi_2(f\_fin(RETURN)) = RETURN$, there are
756$s_2^{pre},s_2^{after},s_2'$ such that $s_2 \stackrel{\pi_1(f\_fin(RETURN))}{\longrightarrow} s_2^{pre}$,
757$s_2^{pre} \stackrel{RETURN}{\longrightarrow} s_2^{after}$,
758$s_2^{after} \stackrel{\pi_3(f\_step(CALL \ id \ arg \ dst))}{\longrightarrow} s_2'$ and $s_1' \simeq_S s_2'$. The following diagram
759depicts the above described requested situation.
760$$
761\xymatrix{
762s_1 \ar@{-}[d]^{\simeq_S} \ar@{-}[d]^{\simeq_S} \ar[rrrrrrrrrrr]^{RETURN}  &&&&&&&&&&&  s_1' \ar@{-}[d]^{\simeq_S} \\\
763s_2 \ar[rrrr]^{\pi_1(f\_fin(RETURN))} &&&& s_2^{pre} \ar[rrr]^{RETURN} &&& s_2^{after} \ar[rrrr]^{\pi_3(f\_step(CALL \ id \ arg \ dst))} &&&& s_2'
764}
765$$
766% The statement is formalized in Matita in the following way.
767% \begin{lstlisting}
768% ; return_commutation :
769%   let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
770%   ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
771%   ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
772%   ∀f,fn.
773%   block_id … (pc_block (pc … st1)) ≠ -1 →
774%   fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
775%   return 〈 f, fn,  final P_in ? (RETURN …) 〉 →
776%   ∀n. stack_sizes f = return n →
777%   let curr_ret ≝ joint_if_result … fn in
778%   ∀st_pop,pc_pop.
779%   pop_frame ?? P_in ? (joint_globalenv P_in prog stack_sizes) f curr_ret
780%    (st_no_pc … st1) = return 〈 st_pop,pc_pop 〉 →
781%   ∀nxt.∀f1,fn1,id,args,dest.
782%     fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) pc_pop  =
783%     return 〈 f1,fn1,sequential P_in … (CALL P_in ? id args dest) nxt 〉 →
784%   st_rel st1 st2 →
785%   ∀t_fn.
786%   fetch_internal_function …
787%      (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) =
788%   return 〈 f,t_fn 〉 →
789%   bind_new_P' ??
790%      (λregs1.λdata.
791%       bind_new_P' ??
792%       (λregs2.λblp.
793%        \snd blp = (RETURN …) ∧
794%        ∃st_fin. repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f
795%               (\fst blp)  (st_no_pc … st2)= return st_fin ∧
796%         ∃t_st_pop,t_pc_pop.
797%         pop_frame ?? P_out ? (joint_globalenv P_out trans_prog stack_sizes) f
798%          (joint_if_result … t_fn) st_fin = return 〈 t_st_pop,t_pc_pop 〉 ∧
799%         sigma_stored_pc P_in P_out prog stack_sizes init init_regs f_lbls f_regs
800%          t_pc_pop = pc_pop ∧
801%         if eqZb (block_id (pc_block pc_pop)) (-1) then
802%             st_no_pc_rel (pc_of_point P_in (pc_block pc_pop) nxt)
803%              (decrement_stack_usage ? n st_pop) (decrement_stack_usage ? n t_st_pop) (*pre_main*)
804%         else
805%             bind_new_P' ??
806%             (λregs4.λdata1.
807%                bind_new_P' ??
808%                (λregs3.λblp1.
809%                  ∃st2'. repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f1
810%                       (\snd blp1) (decrement_stack_usage ? n t_st_pop) = return st2' ∧
811%                       st_no_pc_rel (pc_of_point P_in (pc_block pc_pop) nxt)
812%                        (decrement_stack_usage ? n st_pop) st2'
813%                ) (f_step … data1 (point_of_pc P_in pc_pop) (CALL P_in ? id args dest))
814%             ) (init ? fn1)
815%           ) (f_fin … data (point_of_pc P_in (pc … st1)) (RETURN …))
816%      ) (init ? fn)
817% \end{lstlisting}
818
819\subsubsection{Conclusion}
820After having provided a semantic relation among states that satifies some conditions that correspond to
821commutation lemmas that are commonly proved in a forward simulation proof, it is possible to prove the
822general theorem. All these condition are summarized in a propositional record called \verb=good_state_relation=.
823The statement we are able to prove have the following shape.
824\begin{lstlisting}
825theorem joint_correctness : ∀p_in,p_out : sem_graph_params.
826∀prog : joint_program p_in.∀stack_size : ident → option ℕ.
827∀init : (∀globals.joint_closed_internal_function p_in globals →
828         bound_b_graph_translate_data p_in p_out globals).
829∀init_regs : block → list register.∀f_lbls : lbl_funct_type.
830∀f_regs : regs_funct_type.∀st_no_pc_rel : joint_state_relation p_in p_out.
831∀st_rel : joint_state_pc_relation p_in p_out.
832good_state_relation p_in p_out prog stack_size init init_regs
833 f_lbls f_regs st_no_pc_rel st_rel →
834let trans_prog ≝ b_graph_transform_program … init prog in
835∀init_in.
836make_initial_state (mk_prog_params p_in prog stack_size) = OK ? init_in →
837∃init_out.
838make_initial_state (mk_prog_params p_out trans_prog stack_size) = OK ? init_out ∧
839∃[1] R.
840  status_simulation_with_init
841    (joint_abstract_status (mk_prog_params p_in prog stack_size))
842    (joint_abstract_status (mk_prog_params p_out trans_prog stack_size))
843    R init_in init_out.
844\end{lstlisting}
845The module formalizing the formal machienary we described in this document consists of about 3000 lines of
846Matita code. We stress the fact that this machienary proves general properties that do not depend on the
847specific backend graph compiler pass.
Note: See TracBrowser for help on using the repository browser.