Changeset 3127


Ignore:
Timestamp:
Apr 12, 2013, 4:03:35 PM (4 years ago)
Author:
piccolo
Message:

report on general proof

Location:
Deliverables/D4.4
Files:
1 added
1 moved

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.4/mauro.tex

    r3126 r3127  
    1010\usepackage[utf8x]{inputenc}
    1111\usepackage{listings}
     12\usepackage[all]{xy}
     13
     14\newcommand{\unif}{\ensuremath{\stackrel{\scriptscriptstyle ?}{\equiv}}}
     15\newcommand{\founif}{\ensuremath{\stackrel{\scriptscriptstyle ?}{=}}}
     16\newcommand{\vect}[1]{\ensuremath{\stackrel{\to}{#1}}}
     17\newcommand{\sem}[1]{\ensuremath{[\![#1]\!]}}
     18\newcommand{\bsem}[2]{\ensuremath{[\![#1;\;#2]\!]}}
     19
     20\renewcommand{\verb}{\lstinline}
     21\def\lstlanguagefiles{lst-grafite.tex}
     22\lstset{language=Grafite}
     23
    1224\usepackage{lscape}
    1325\usepackage{stmaryrd}
     
    119131\verb=src : joint_program p_in= (resp. \verb=out : joint_program p_out=), we would like to
    120132prove a statement similar to this shape.
    121 \begin{verbatim}
     133\begin{lstlisting}
    122134theorem joint_correctness : ∀p_in,p_out : sem_graph_params.
    123135∀prog : joint_program p_in.∀stack_size.
     
    133145    (joint_abstract_status (mk_prog_params p_out trans_prog stack_size))
    134146    R init_in init_out.
    135 \end{verbatim}
     147\end{lstlisting}
    136148When proving this statement (for each concrete istance of language),
    137149we need to proceed by cases according the classification of
     
    168180In order to reach this goal, we have to analyze first whether there is a common way to perform language
    169181translation for each pass. After having defined and specified the translation machienary, we will
    170 explain how it is possibile to use it in order to build such a layer.
     182explain how it is possibile to use it in order to build such a layer. So this section is organized as follows:
     183in the first part we explain the translation machienary while in the second part we explain such a layer.
     184
     185\subsection{Graph translation}
     186Since a program is just a collection of functions, the compositional approach suggests us to define the
     187translation of a program in terms of the way we translate each internal function. Thus, if we let
     188\verb=src_g_pars= and \verb=dst_g_pars= being the graph parameters of respectively the source and
     189the target program, the aim is writing a Matita's function that takes as input an object of type
     190\verb=joint_closed_internal_function src_g_pars= together with additional information
     191(that we will explain better later) and gives as output an object of type
     192\verb=joint_closed_internal_function dst_g_pars= with some properties, that corresponds
     193to the result of the translation (for the definition of \verb=joint_closed_internal_function=, see
     194Deliverable 4.2 and 4.3) . The signature of the definition is the following one.
     195\begin{lstlisting}
     196definition b_graph_translate :
     197  ∀src_g_pars,dst_g_pars : graph_params.
     198  ∀globals: list ident.
     199  ∀data : bound_b_graph_translate_data src_g_pars dst_g_pars globals.
     200  ∀def_in : joint_closed_internal_function src_g_pars globals.
     201  Σdef_out : joint_closed_internal_function dst_g_pars globals.
     202  ∃data',regs,f_lbls,f_regs.
     203    bind_new_instantiates ?? data' data regs ∧
     204    b_graph_translate_props … data' def_in def_out f_lbls f_regs.
     205........
     206\end{lstlisting}
     207
     208Let us now discuss in detail what are the parameter to be provide in input and what is the output of the
     209translation process.
     210
     211\subsubsection{Input requested by the translation process}
     212Clearly, \verb=b_graph_translate= takes as input the internal function of the source language we want to translate.
     213But it also takes in input some useful infomrmation which will be used in order to dictate the translation process.
     214These information are all contained in an instance of the following record.
     215
     216\begin{lstlisting}
     217record b_graph_translate_data
     218  (src, dst : graph_params)
     219  (globals : list ident) : Type[0] ≝
     220{ init_ret : call_dest dst
     221; init_params : paramsT dst
     222; init_stack_size : ℕ
     223; added_prologue : list (joint_seq dst globals)
     224; new_regs : list register
     225; f_step : label → joint_step src globals → bind_step_block dst globals
     226; f_fin : label → joint_fin_step src → bind_fin_block dst globals
     227; good_f_step :
     228  ∀l,s.bind_new_P' ??
     229    (λlocal_new_regs,block.let 〈pref, op, post〉 ≝ block in
     230       ∀l.
     231       let allowed_labels ≝ l :: step_labels … s in
     232       let allowed_registers ≝ new_regs @ local_new_regs @ step_registers … s in
     233       All (label → joint_seq ??)
     234         (λs'.step_labels_and_registers_in … allowed_labels allowed_registers
     235              (step_seq dst globals (s' l)))
     236         pref ∧
     237       step_labels_and_registers_in … allowed_labels allowed_registers (op l) ∧
     238       All (joint_seq ??)
     239         (step_labels_and_registers_in … allowed_labels allowed_registers)
     240         post)
     241    (f_step l s)
     242; good_f_fin :
     243  ∀l,s.bind_new_P' ??
     244    (λlocal_new_regs,block.let 〈pref, op〉 ≝ block in
     245       let allowed_labels ≝ l :: fin_step_labels … s in
     246       let allowed_registers ≝ new_regs @ local_new_regs @ fin_step_registers … s in
     247       All (joint_seq ??)
     248         (λs.step_labels_and_registers_in … allowed_labels allowed_registers s)
     249         pref ∧
     250       fin_step_labels_and_registers_in … allowed_labels allowed_registers op)
     251    (f_fin l s)
     252; f_step_on_cost :
     253  ∀l,c.f_step l (COST_LABEL … c) =
     254    bret ? (step_block ??) 〈[ ], λ_.COST_LABEL dst globals c, [ ]〉
     255; cost_in_f_step :
     256  ∀l,s,c.
     257  bind_new_P ??
     258    (λblock.∀l'.\snd (\fst block) l' = COST_LABEL dst globals c →
     259       s = COST_LABEL … c) (f_step l s)
     260}
     261\end{lstlisting}
     262We will now summarize what each field means and how it is used in the translation process. We will say that an identifier of
     263a pseudo-register (resp. a code point) is {\em fresh} when it never appears in the code of the source function.
     264\begin{center}
     265\begin{tabular*}{\textwidth}{p{4cm}p{11cm}}
     266Field & Explanation \\
     267\hline
     268\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.\\
     269\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.\\
     270\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. \\
     271\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. \\
     272\texttt{new\_regs} & It is a list of identifiers for fresh pseudo-registers that are used by statements in \texttt{added\_prologue}. \\
     273\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. \\
     274\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.\\
     275\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).  \\
     276\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.\\
     277\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.
     278\end{tabular*}
     279\end{center}
     280
     281\subsubsection{Output given the translation process}
     282Clearly \verb=g_graph_translate= gives in output the translated internal function. Unfortunately,
     283for what we are going to develop later, this information is insufficient because we need some information
     284about the correspondence between the source internal function and the translated one. Such an information
     285is given by the second component of the $\Sigma$-type returned by the translation process.
     286We remind that the return type of \verb=b_graph_translate= is the following.
     287\begin{lstlisting}
     288 Σdef_out : joint_closed_internal_function dst_g_pars globals.
     289  ∃data',regs,f_lbls,f_regs.
     290    bind_new_instantiates ?? data' data regs ∧
     291    b_graph_translate_props … data' def_in def_out f_lbls f_regs.
     292\end{lstlisting}
     293The correspondence between the source internal function and the translated one is made explicit by two functions:
     294\verb=f_lbls : code_point src_g_pars → list (code_point dst_g_pars)= and
     295\verb=f_regs :  code_point src_g_pars → list (register)=. To understand their meaning, we need to stress the
     296fact that the translation process translates every statement appearing in the code of the source internal function
     297in a given code point $l$ into a block of statements in the code of the translated function where the first
     298instruction of the block has $l$ as code point identifier and all succeeding instructions of the block have
     299fresh code points identifiers. Furthermore statements of this block may use fresh identifiers of pseudo-registers or
     300(even worste) they may use some fresh code-point identifiers being generated by the translation (we will see later
     301that this will be important when translating a call statement). We will use the above mentioned functions
     302to retrieve this information. \verb=f_lbls= takes in input an identifier $l$ for a code point in the
     303source code and it gives back the list of all fresh code point identifiers generated by the translation process
     304of the statement in the source located in $l$. \verb=f_regs= takes in input an identifier $l$ for a code point
     305in the source code and it gives back the list of all fresh register identifiers generated by the translation process
     306of the statement in the source located in $l$.
     307
     308The above mentioned properties about the functions \verb=f_lbls= and \verb=f_regs=, together with some other
     309ones, are expressed and formalized by the following propositional record.
     310\begin{lstlisting}
     311record b_graph_translate_props
     312  (src_g_pars, dst_g_pars : graph_params)
     313  (globals: list ident)
     314  (data : b_graph_translate_data src_g_pars dst_g_pars globals)
     315  (def_in : joint_closed_internal_function src_g_pars globals)
     316  (def_out : joint_closed_internal_function dst_g_pars globals)
     317  (f_lbls : label → list label)
     318  (f_regs : label → list register) : Prop ≝
     319{ res_def_out_eq :
     320           joint_if_result … def_out = init_ret … data
     321; pars_def_out_eq :
     322           joint_if_params … def_out = init_params … data
     323; ss_def_out_eq :
     324           joint_if_stacksize … def_out = init_stack_size … data
     325; partition_lbls : partial_partition … f_lbls
     326; partition_regs : partial_partition … f_regs
     327; freshness_lbls :
     328  (∀l.All …
     329    (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧
     330           fresh_for_univ … lbl (joint_if_luniverse … def_out)) (f_lbls l))
     331; freshness_regs :
     332  (∀l.All …
     333    (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧
     334           fresh_for_univ … reg (joint_if_runiverse … def_out)) (f_regs l))
     335; freshness_data_regs :
     336  All … (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧
     337               fresh_for_univ … reg (joint_if_runiverse … def_out))
     338        (new_regs … data)
     339; data_regs_disjoint : ∀l,r.r ∈ f_regs l → r ∈ new_regs … data → False
     340; multi_fetch_ok :
     341  ∀l,s.stmt_at … (joint_if_code … def_in) l = Some ? s →
     342  let lbls ≝ f_lbls l in let regs ≝ f_regs l in
     343  match s with
     344  [ sequential s' nxt ⇒
     345    let block ≝
     346      if not_emptyb … (added_prologue … data) ∧
     347         eq_identifier … (joint_if_entry … def_in) l then
     348        bret … [ ]
     349      else
     350        f_step … data l s' in
     351    l -(block, l::lbls, regs)-> nxt in joint_if_code … def_out
     352  | final s' ⇒
     353    l -(f_fin … data l s', l::lbls, regs)-> it in joint_if_code … def_out
     354  | FCOND abs _ _ _ ⇒ Ⓧabs
     355  ]
     356; prologue_ok :
     357  if not_emptyb … (added_prologue … data) then
     358    ∃lbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧
     359    joint_if_entry … def_out
     360      -(〈[ ],λ_.COST_LABEL … (get_first_costlabel … def_in), added_prologue … data〉,
     361        f_lbls … lbl)-> joint_if_entry … def_in in joint_if_code … def_out
     362  else (joint_if_entry … def_out = joint_if_entry … def_in)
     363}.
     364\end{lstlisting}
     365
     366We will now summarize the meaning of each field of the record using the same approach followed
     367in the previous subsection.
     368\begin{center}
     369\begin{tabular*}{\textwidth}{p{4cm}p{11cm}}
     370Field & Explanation \\
     371\hline
     372\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. \\
     373\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. \\
     374\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. \\
     375\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. \\
     376\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. \\
     377\texttt{freshness\_lbls} & All lists of code-point identifiers generated by a code-point of the code of the source internal function are fresh.  \\
     378\texttt{freshness\_regs} & All lists of pseudo-register identifiers generated by a code-point of the code of the source internal function are fresh.  \\
     379\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. \\
     380\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. \\
     381\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
     382$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
     383successor, $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}$
     384and it may have a syntactical successor depending wether $I$ is a step-statement or not: in the former case we have that the
     385syntactical successor of $I_n$ is the syntactical successor of $I$, in the latter case, $I_n$ is a final statement.\\
     386\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.
     387\end{tabular*}
     388\end{center}
     389
     390\subsection{A general correctness proof}
     391In 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.
     392
     393\subsubsection{A standard calling relation}
     394Two 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$.
     395
     396In order to explain how this machienary work. we need to enter more in the detail of the translation process. Given a step-statement
     397$I$, formally its translation is a triple $f\_step(s) = \langle pre,p,post \rangle$ such that $pre$ is a list of sequential
     398statements called {\em preamble}, $p$ is a step-statement (we call it {\em pivot}) and $post$ is again a list of sequential statements
     399called {\em postamble}. When $pre = [s_1,\ldots,s_n]$ and $post = [s_1',\ldots,s_m']$, the corresponding block being the translation
     400of $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
     401postable, i.e. it is a pair $f\_fin(s) = \langle pre,p\rangle$ where the pivot $p$ is a final statement.
     402
     403Given a statement $I$ at a given code point $l$ in the source internal function and given the pivot statement $p$ of the translation
     404of $I$ staying at code-point $l'$ in the translated internal function, there is an easy way to relate $l$ and $l'$. Notice that,
     405in case the preamble is empty, for the property of the translation process we have then $l = l'$, while if the preamble is non-empty.
     406then $l'$ is $n-1$-th element of $f\_lbls(l)$, where $n \geq 0$ is the length of the preamble.
     407The Matita's definition computing the code points according to the above mentioned specification is the following one.
     408\begin{lstlisting}
     409definition sigma_label : ∀p_in,p_out : sem_graph_params.
     410joint_program p_in → (ident → option ℕ) →
     411(∀globals.joint_closed_internal_function p_in globals
     412         →bound_b_graph_translate_data p_in p_out globals) →
     413(block → list register) → lbl_funct_type → regs_funct_type →
     414block → label → option label ≝
     415λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,bl,searched.
     416! bl ← code_block_of_block bl ;
     417! <id,fn> ← res_to_opt … (fetch_internal_function …
     418                           (joint_globalenv p_in prog stack_size) bl);
     419! <res,s> ←
     420 find ?? (joint_if_code ?? fn)
     421  (λlbl.λ_.match preamble_length … prog stack_size init init_regs f_regs bl lbl with
     422             [ None ⇒ false
     423             | Some n ⇒ match nth_opt ? n (lbl::(f_lbls bl lbl)) with
     424                         [ None ⇒ false
     425                         | Some x ⇒ eq_identifier … searched x
     426                         ]
     427             ]);
     428return res.
     429\end{lstlisting}
     430This function takes in input all the information provided by the translation process (in particular the function $f\_lbls$), a
     431function location and a code-point identifier $l$; it fetches the internal function of the source language in the correponding location.
     432Then it unfolds the code of the fetched function looking for a label $l'$ and a statement $I$ located in $l'$, such that,
     433either $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
     434of the preamble of $I$. The function $find$ is the procedure realizing this search. If $preamble\_length$ is the function giving in
     435output the length of the preamble and if $nth\_opt$ is the function giving the $n$-th element of a list, then this condition can
     436be 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)$,
     437where $n$ is the length of the preamble.
     438
     439We can prove that, starting from a code point identifier of the translated internal function,
     440whenever there exists a code-point identifier in the source internal function satifying the above condition, then it is always unique.
     441The properties \verb=partition_lbls= and \verb=freshness_lbls= provided by the translation process are crucial in the proof
     442of this statement.
     443
     444We can wrap this function inside the definition of the desired relation among program counter states in the following way
     445The conditional at the beginning is put to deal with the pre-main case, which is translated without following the standard
     446translation process we explain in previous section.
     447\begin{lstlisting}
     448definition sigma_pc_opt : 
     449∀p_in,p_out : sem_graph_params.
     450joint_program p_in → (ident → option ℕ) →
     451(∀globals.joint_closed_internal_function p_in globals
     452         →bound_b_graph_translate_data p_in p_out globals) →
     453(block → list register) → lbl_funct_type → regs_funct_type →
     454program_counter → option program_counter ≝
     455λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc.
     456let target_point ≝ point_of_pc p_out pc in
     457if eqZb (block_id (pc_block pc)) (-1) then
     458 return pc
     459else
     460 ! source_point ← sigma_label p_in p_out prog stack_size init init_regs
     461                   f_lbls f_regs (pc_block pc) target_point;
     462 return pc_of_point p_in (pc_block pc) source_point.
     463
     464definition sigma_stored_pc ≝
     465λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc.
     466match sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc with
     467      [None ⇒ null_pc (pc_offset … pc) | Some x ⇒ x].
     468\end{lstlisting}
     469
     470The main result about the program counter relation we have defined is the following. If we fetch a statement $I$ in
     471at a given program counter $pc$ in the source program, then there is a program counter $pc'$ in the target program
     472which is in relation with $pc$ (i.e. $sigma\_stored\_pc pc' = pc$) and the fetched statement at $pc'$ is the pivot
     473statement of the tranlation. The formalization of this statement in Matita is given in the following.
     474
     475\begin{lstlisting}
     476lemma fetch_statement_sigma_stored_pc :
     477∀p_in,p_out,prog,stack_sizes,
     478init,init_regs,f_lbls,f_regs,pc,f,fn,stmt.
     479b_graph_transform_program_props p_in p_out stack_sizes
     480  init prog init_regs f_lbls f_regs →
     481block_id … (pc_block pc) ≠ -1 →
     482let trans_prog ≝ b_graph_transform_program p_in p_out init prog in
     483fetch_statement p_in … (joint_globalenv p_in prog stack_sizes) pc =
     484return 〈f,fn,stmt〉 →
     485∃data.bind_instantiate ?? (init … fn) (init_regs (pc_block pc)) = return data ∧
     486match stmt with
     487[ sequential step nxt ⇒
     488   ∃step_block : step_block p_out (prog_names … trans_prog).
     489   bind_instantiate ?? (f_step … data (point_of_pc p_in pc) step)
     490                 (f_regs (pc_block pc) (point_of_pc p_in pc)) = return step_block ∧
     491   ∃pc'.sigma_stored_pc p_in p_out prog stack_sizes init
     492                                           init_regs f_lbls f_regs pc' = pc ∧
     493   ∃fn',nxt'.
     494   fetch_statement p_out … (joint_globalenv p_out trans_prog stack_sizes) pc' =
     495   if not_emptyb … (added_prologue … data) ∧
     496      eq_identifier … (point_of_pc p_in pc) (joint_if_entry … fn)
     497   then OK ? <f,fn',sequential ?? (NOOP …) nxt'>
     498   else OK ? <f,fn',
     499             sequential ?? ((\snd(\fst step_block)) (point_of_pc p_in pc')) nxt'>
     500| final fin ⇒
     501    ∃fin_block.bind_instantiate ?? (f_fin … data (point_of_pc p_in pc) fin)
     502                  (f_regs (pc_block pc) (point_of_pc p_in pc)) = return fin_block ∧
     503    ∃pc'.sigma_stored_pc p_in p_out prog stack_sizes init
     504                                           init_regs f_lbls f_regs pc' = pc ∧
     505    ∃fn'.fetch_statement p_out …
     506       (joint_globalenv p_out trans_prog stack_sizes) pc'
     507       = return 〈f,fn',final ?? (\snd fin_block)〉           
     508| FCOND abs _ _ _ ⇒ Ⓧabs
     509].
     510\end{lstlisting}
     511
     512If we combine the statement above with the fact that the pivot statement of the translation
     513of a call statement is always a call statement (which we will formalize better in the
     514following section), then we can define our standard calling relation in the following way.
     515
     516\begin{lstlisting}
     517(λs1:Σs: (joint_abstract_status (mk_prog_params p_in ??)).as_classifier ? s cl_call.
     518 λs2:Σs:(joint_abstract_status (mk_prog_params p_out ??)).as_classifier ? s cl_call.
     519pc ? s1 =
     520 sigma_stored_pc p_in p_out prog stack_sizes init init_regs f_lbls f_regs (pc ? s2)).
     521\end{lstlisting}
     522
     523We stress the fact that such a call relation will be always defined in this way for all joint-languages,
     524in an independent way from the specific pass. The only condition we will ask is that the pass should
     525use the translation process we explain in the previous section.
     526
     527\subsubsection{The semantical relation}
     528The semantical relation between states is the classical relation used in forward simulation proofs.
     529It correlates the data of the status (e.g. register, memory, etc.). We remind that the notion of state
     530in joint language is summarized in the following record.
     531\begin{lstlisting}
     532record state_pc (semp : sem_state_params) : Type[0] ≝
     533  { st_no_pc :> state semp
     534  ; pc : program_counter
     535  ; last_pop : program_counter
     536  }.
     537\end{lstlisting}
     538It consists of three fields: the field \verb=st_no_pc= contains all data information of the state
     539(the content of the registers, of the memory and so on), the field \verb=pc= contains the current
     540program counter, while the field \verb=last_pop= is the address of the last popped calling address
     541when executing a return instruction.
     542
     543The type of the semantical relation between state is the following.
     544
     545\begin{lstlisting}
     546definition joint_state_pc_relation ≝
     547λP_in,P_out : sem_graph_params.state_pc P_in → state_pc P_out → Prop.
     548\end{lstlisting}
     549
     550We would like to state some conditions the semantical relation between states have to satisfy in order
     551to get our simulation result. We would like that this relation have some flavour of compositionality.
     552In particular we would like that it depends strictly on the contents of the field \verb=st_no_pc=, i.e.
     553the field that really contains data information of the state. So we need also a data relation, i.e.
     554a relation of this type.
     555
     556\begin{lstlisting}
     557definition joint_state_relation ≝
     558λP_in,P_out.program_counter → state P_in → state P_out → Prop.
     559\end{lstlisting}
     560
     561Notice that the data relation cab depend on a specific program counter of the source. This is done
     562to capture complex data relations like the ones in the ERTL to LTL pass, in which you need to know
     563where data in pseudoregisters of ERTL are stored by the translation (either in hardware register or
     564in memory) and this information depends on the code point on the statement being translated.
     565
     566The compositionality requirement is expressed by the following conditions (which are part of a bigger
     567record, that we are going to introduce later).
     568
     569\begin{lstlisting}
     570; fetch_ok_sigma_state_ok :
     571   ∀st1,st2,f,fn. st_rel st1 st2 →
     572    fetch_internal_function …
     573     (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 
     574     = return <f,fn> →
     575     st_no_pc_rel (pc … st1) (st_no_pc … st1) (st_no_pc … st2)
     576; fetch_ok_pc_ok :
     577  ∀st1,st2,f,fn.st_rel st1 st2 →
     578   fetch_internal_function …
     579     (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 
     580     = return <f,fn> →
     581   pc … st1 = pc … st2
     582; fetch_ok_sigma_last_pop_ok :
     583  ∀st1,st2,f,fn.st_rel st1 st2 →
     584   fetch_internal_function …
     585     (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 
     586     = return <f,fn> →
     587   (last_pop … st1) = sigma_stored_pc P_in P_out prog stack_sizes init init_regs
     588                       f_lbls f_regs (last_pop … st2)
     589; st_rel_def :
     590  ∀st1,st2,pc,lp1,lp2,f,fn.
     591  fetch_internal_function …
     592     (joint_globalenv P_in prog stack_sizes) (pc_block pc) = return <f,fn> →
     593   st_no_pc_rel pc st1 st2 →
     594   lp1 = sigma_stored_pc P_in P_out prog stack_sizes init init_regs
     595          f_lbls f_regs lp2 →
     596  st_rel (mk_state_pc ? st1 pc lp1) (mk_state_pc ? st2 pc lp2)
     597\end{lstlisting}
     598
     599Condition \texttt{fetch\_ok\_sigma\_state\_ok} postulates that two state that are in semantical
     600relation should have their data field also in relation. Condition \texttt{fetch\_ok\_pc\_ok} postulates
     601that two states that are in semantical relation should have the same program counter. This is due
     602to the way the translation is performed. In fact a statement $I$ at a code point $l$ in the source
     603internal function is translated with a block of instructions in the translated internal function
     604whose initial statement is at the same code point $l$. Condition \texttt{fetch\_ok\_sigma\_last\_pop\_ok}
     605postulates that two states that are in semantical relation have the last popped calling address
     606in call relation. Finally \texttt{st\_rel\_def} postulates that given two states having the same
     607program counter, the last pop fields in call relation and the data fields also in data relation, then
     608they are in semantical relation.
     609
     610An other important condition is that the pivot statement of the translation of a call statement is
     611always a call statement. This is important in order to obtain the correctness of the call relation
     612and return relation between state. This condition is formalized by the following Matita's code, and
     613we call it \texttt{call\_is\_call}.
     614
     615\begin{lstlisting}
     616;  call_is_call :∀f,fn,bl.
     617  fetch_internal_function …
     618     (joint_globalenv P_in prog stack_sizes) bl = return <f,fn> →
     619   ∀id,args,dest,lbl.
     620    bind_new_P' ??
     621     (λregs1.λdata.bind_new_P' ??
     622      (λregs2.λblp.
     623        ∀lbl.∃id',args',dest'.((\snd (\fst blp)) lbl) = CALL P_out ? id' args' dest')
     624      (f_step … data lbl (CALL P_in ? id args dest)))
     625     (init ? fn)
     626\end{lstlisting}
     627
     628The conditions we are going to present now are standard semantical commutation lemmas that are commonly
     629used when proving the correctness of the operational semantics of many imperative languages. We introduce some notation.
     630We 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.
     631We 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
     632over by states of programs of the source language. We will use $s_2,s_2',s_2'',\ldots$ to range over by
     633states of programs of the target language. We denote respectively with $\simeq_{S}$, $\simeq_C$ and $\simeq_L$
     634the semantical relation, the call relation and the cost-label relation between states. These relations have
     635been introduced at the beginning of this Deliverable (see Section ??). If $instr = [I_1,\ldots,I_n]$ is a list
     636of instructions, then we write $s_i \stackrel{instr}{\longrightarrow} s_i'$ ($i \in [1,2]$) when $s_i'$ is
     637the state being the result of the evaluation of the sequence of instructions $instr$ (performed in the order
     638they appear in the list) starting from the initial state $s_i$. When $instr = [I]$ is a singleton, we use
     639to omit square brackets and we write $s_i \stackrel{I}{\longrightarrow} s_i'$.
     640We will denote with $\pi_i$ ($i \in [1,t]$) the projecting functions of $t$-uples. We will denote with $f\_step$ and $f\_fin$
     641the translating functions of respectively step-statements and final statements. We remind that $f\_step$ gives
     642a triple as output (a list of instruction called preamble,an instruction called pivot and a list of instructions
     643called postamble) while $f\_fin$ gives a pair as output (a list of instruction called preamble and an instruction
     644called pivot). Furthermore, we denote with $prologue$ the content of the field \texttt{added\_prologue} of the record
     645provided in input to the translation process.
     646
     647Many commutation conditions can be depicted using diagrams. We will use them to give a pictorial flavour of the conditions
     648we will ask in order to obtain the final correctness statement. Given the states $s_1,s_1',s_2,s_2'$ and the instructions
     649$I,J_1,\ldots,J_k$, the following diagram
     650$$
     651\xymatrix{
     652s_1 \ar@{->}[rr]^{I} \ar@{-}[d]^{\simeq_S} && s_1' \ar@{-}[d]^{\simeq_S}\\
     653s_2 \ar[rr]^{[J_1,\ldots,J_k]} && s_2'
     654}
     655$$
     656depicts a situation in which the state $s_1 \stackrel{I}{\longrightarrow} s_1'$, $s_2 \stackrel{I}{\longrightarrow} s_2'$,
     657$s_1 \simeq_S s_2$ and $s_1' \simeq_S s_2'$.
     658
     659\paragraph{Commutation of pre-main instructions.}
     660In order to get the commutation of pre-main instructions (states whose function location of program counter is -1), we have
     661to 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$,
     662then 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
     663diagram commutes.
     664$$
     665\xymatrix{
     666s_1 \ar@{->}[rr]^{I} \ar@{-}[d]^{\simeq_S} && s_1' \ar@{-}[d]^{\simeq_S}\\
     667s_2 \ar[rr]^{J} && s_2'
     668}
     669$$
     670The formalization of this statement in Matita is the following one.
     671\begin{lstlisting}
     672; pre_main_ok :
     673  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
     674    ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
     675    ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
     676    block_id … (pc_block (pc … st1)) = -1 →
     677    st_rel st1 st2 →
     678    as_label (joint_status P_in prog stack_sizes) st1 =
     679    as_label (joint_status P_out trans_prog stack_sizes) st2 ∧
     680    joint_classify … (mk_prog_params P_in prog stack_sizes) st1 =
     681    joint_classify … (mk_prog_params P_out trans_prog stack_sizes) st2 ∧
     682    (eval_state P_in … (joint_globalenv P_in prog stack_sizes)
     683      st1 = return st1' →
     684    ∃st2'. st_rel st1' st2' ∧
     685    eval_state P_out …
     686     (joint_globalenv P_out trans_prog stack_sizes) st2 = return st2')
     687\end{lstlisting}
     688
     689\paragraph{Commutation of conditional jump.}
     690For 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
     691\begin{itemize}
     692\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}$,
     693$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
     694$$
     695\xymatrix{
     696s_1 \ar@{->}[rrrrrr]^{COND \ l \ r} \ar@{-}[d]^{\simeq_S} &&&&&& s_1' \ar@{-}[d]^{\simeq_S}\\
     697s_2 \ar[rrr]^{\pi_1(f\_step(COND \ r \ l))} &&& s_2^{fin} \ar[rrr]^{\pi_2(f\_step(COND \ r \ l))} &&& s_2'
     698}
     699$$
     700\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
     701      such that $l = l'$.
     702\end{itemize}
     703This condition is formalized in Matita in the following way.
     704\begin{lstlisting}
     705; cond_commutation :
     706    let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
     707    ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
     708    ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
     709    ∀f,fn,a,ltrue,lfalse,bv,b.
     710    block_id … (pc_block (pc … st1)) ≠ -1 →
     711    let cond ≝ (COND P_in ? a ltrue) in
     712    fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
     713    return <f, fn,  sequential … cond lfalse> → 
     714    acca_retrieve … P_in (st_no_pc … st1) a = return bv →
     715    bool_of_beval … bv = return b →
     716    st_rel st1 st2 →
     717    ∀t_fn.
     718    fetch_internal_function …
     719     (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) =
     720     return 〈f,t_fn〉 →
     721    bind_new_P' ??
     722     (λregs1.λdata.bind_new_P' ??
     723     (λregs2.λblp.(\snd blp) = [ ] ∧
     724        ∀mid.
     725          stmt_at P_out … (joint_if_code ?? t_fn) mid
     726          = return sequential P_out ? ((\snd (\fst blp)) mid) lfalse→
     727         ∃st2_pre_mid_no_pc.
     728            repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f
     729             (map_eval ?? (\fst (\fst blp)) mid) (st_no_pc ? st2)
     730            = return st2_pre_mid_no_pc ∧
     731            let new_pc ≝ if b then
     732                           (pc_of_point P_in (pc_block (pc … st1)) ltrue)
     733                         else
     734                           (pc_of_point P_in (pc_block (pc … st1)) lfalse) in
     735            st_no_pc_rel new_pc (st_no_pc … st1) (st2_pre_mid_no_pc) ∧
     736            ∃a'. ((\snd (\fst blp)) mid)  = COND P_out ? a' ltrue ∧
     737            ∃bv'. acca_retrieve … P_out st2_pre_mid_no_pc a' = return bv' ∧
     738                  bool_of_beval … bv' = return b
     739   )  (f_step … data (point_of_pc P_in (pc … st1)) cond)   
     740  ) (init ? fn)
     741\end{lstlisting}
     742
     743\paragraph{Commutation of sequential statements.}
     744In case of a sequential statement $I$, its translation $f\_step(I) = \langle pre , J , post \rangle$ is coerced
     745into a list of sequential statements $pre$ \verb=@= $[J]$ \verb=@= $post$. Then we can state the condition in the
     746following 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
     747there 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
     748the following diagram commutes.
     749$$
     750\xymatrix{
     751s_1 \ar@{->}[rr]^{I} \ar@{-}[d]^{\simeq_S}  && s_1' \ar@{-}[d]^{\simeq_S}\\
     752s_2 \ar[rr]^{f\_step(I)} && s_2'
     753}
     754$$
     755The formalization in Matita of the above statement is as follows.
     756\begin{lstlisting}
     757; seq_commutation :
     758  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
     759  ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
     760  ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
     761  ∀f,fn,stmt,nxt.
     762  block_id … (pc_block (pc … st1)) ≠ -1 →
     763  let seq ≝ (step_seq P_in ? stmt) in
     764  fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
     765  return <f, fn,  sequential … seq nxt> → 
     766  eval_state P_in … (joint_globalenv P_in prog stack_sizes)
     767  st1 = return st1' →
     768  st_rel st1 st2 →
     769  ∀t_fn.
     770  fetch_internal_function …
     771     (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) =
     772  return <f,t_fn> →
     773  bind_new_P' ??
     774     (λregs1.λdata.bind_new_P' ??
     775      (λregs2.λblp.
     776       ∃l : list (joint_seq P_out
     777                  (globals ? (mk_prog_params P_out trans_prog stack_sizes))).
     778                            blp = (ensure_step_block ?? l) ∧
     779       ∃st2_fin_no_pc.
     780           repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f
     781              l  (st_no_pc … st2)= return st2_fin_no_pc ∧
     782           st_no_pc_rel (pc … st1') (st_no_pc … st1') st2_fin_no_pc
     783      ) (f_step … data (point_of_pc P_in (pc … st1)) seq)
     784     ) (init ? fn)
     785\end{lstlisting}
     786
     787\paragraph{Commutation of call statement}
     788For 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
     789the statement fetched in the translated language at the program counter being in call relation
     790with the program counter of $s_1$ is $\pi_2(f\_step(CALL \ id \ arg \ dst)) = CALL id' \ arg' \ dst'$
     791for some $id',ags',dst'$, then there are $s_2^{pre},s_2^{after},s_2'$ such that
     792\begin{itemize}
     793\item $s_2 \stackrel{\pi_1(f\_step(CALL \ id \ arg \ dst))}{\longrightarrow} s_2^{pre}$,
     794\item $s_2^{pre} \stackrel{CALL \ id' \arg' \ dst'}{\longrightarrow} s_2^{after}$,
     795\item $s_2^{after} \stackrel{prologue}{\longrightarrow} s_2'$,
     796\item $s_1' \simeq_L s_2^{after}$ and $s_1' \simeq_S s_2'$.
     797\end{itemize}
     798The situation is depicted by the following diagram.
     799$$
     800\xymatrix{
     801s_1 \ar@{-}[d]^{\simeq_S} \ar@{-}[d]^{\simeq_S} \ar[rrrrrrrrrr]^{CALL \ id \ arg \ dst}  &&&&&&&&&&  s_1' \ar@{-}[d]^{\simeq_S} \\
     802s_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'
     803}
     804$$
     805The statement is formalized in Matita in the following way.
     806\begin{lstlisting}
     807; call_commutation :
     808  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
     809  ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
     810  ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
     811  ∀f,fn,id,arg,dest,nxt.
     812  block_id … (pc_block (pc … st1)) ≠ -1 →
     813  fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
     814  return 〈f, fn,  sequential P_in ? (CALL P_in ? id arg dest) nxt〉 →
     815  ∀bl.
     816   block_of_call P_in … (joint_globalenv P_in prog stack_sizes) id (st_no_pc … st1)
     817      = return bl →
     818  ∀f1,fn1.
     819   fetch_internal_function …
     820    (joint_globalenv P_in prog stack_sizes) bl =  return 〈f1,fn1〉 →
     821  ∀st1_pre.
     822  save_frame … P_in (kind_of_call P_in id) dest st1 = return st1_pre →
     823  ∀n.stack_sizes f1 = return n → 
     824  ∀st1'.
     825  setup_call ?? P_in n (joint_if_params … fn1) arg st1_pre = return st1' →
     826  st_rel st1 st2 → 
     827  ∀t_fn1.
     828  fetch_internal_function … (joint_globalenv P_out trans_prog stack_sizes) bl =
     829  return 〈f1,t_fn1〉 →
     830  bind_new_P' ??
     831    (λregs1.λdata.
     832     bind_new_P' ??
     833      (λregs2.λblp.
     834        ∀pc',t_fn,id',arg',dest',nxt1.
     835          sigma_stored_pc P_in P_out prog stack_sizes init init_regs
     836           f_lbls f_regs pc' = (pc … st1) →
     837          fetch_statement P_out … (joint_globalenv P_out trans_prog stack_sizes) pc'
     838          = return 〈f,t_fn,
     839                    sequential P_out ? ((\snd (\fst blp)) (point_of_pc P_out pc')) nxt1〉→
     840          ((\snd (\fst blp)) (point_of_pc P_out pc')) = (CALL P_out ? id' arg' dest') → 
     841       ∃st2_pre_call.
     842        repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f
     843          (map_eval ?? (\fst (\fst blp)) (point_of_pc P_out pc')) (st_no_pc ? st2) = return st2_pre_call ∧
     844       block_of_call P_out … (joint_globalenv P_out trans_prog stack_sizes) id'
     845        st2_pre_call = return bl ∧
     846       ∃st2_pre.
     847        save_frame … P_out (kind_of_call P_out id') dest'
     848         (mk_state_pc ? st2_pre_call pc' (last_pop … st2)) = return st2_pre ∧
     849       ∃st2_after_call.
     850         setup_call ?? P_out n (joint_if_params … t_fn1) arg' st2_pre
     851          = return st2_after_call ∧
     852       bind_new_P' ??
     853         (λregs11.λdata1.
     854          ∃st2'.
     855           repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f1
     856           (added_prologue … data1) (increment_stack_usage P_out n st2_after_call) =
     857           return st2' ∧
     858           st_no_pc_rel (pc_of_point P_in bl (joint_if_entry … fn1))
     859            (increment_stack_usage P_in n st1') st2'               
     860         ) (init ? fn1)
     861     )
     862     (f_step … data (point_of_pc P_in (pc … st1)) (CALL P_in ? id arg dest))
     863    ) (init ? fn)
     864\end{lstlisting}
     865\paragraph{Commutation of return statement}
     866For 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$
     867is the call statement that caused the function call ened by the current return (i.e. it is the statement whose code point identifier
     868is the syntactical predecessor of the program counter of $s_1'$), then $\pi_2(f\_fin(RETURN)) = RETURN$, there are
     869$s_2^{pre},s_2^{after},s_2'$ such that $s_2 \stackrel{\pi_1(f\_fin(RETURN))}{\longrightarrow} s_2^{pre}$,
     870$s_2^{pre} \stackrel{RETURN}{\longrightarrow} s_2^{after}$,
     871$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
     872depicts the above described requested situation.
     873$$
     874\xymatrix{
     875s_1 \ar@{-}[d]^{\simeq_S} \ar@{-}[d]^{\simeq_S} \ar[rrrrrrrrrrr]^{RETURN}  &&&&&&&&&&&  s_1' \ar@{-}[d]^{\simeq_S} \\\
     876s_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'
     877}
     878$$
     879The statement is formalized in Matita in the following way.
     880\begin{lstlisting}
     881; return_commutation :
     882  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
     883  ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
     884  ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
     885  ∀f,fn.
     886  block_id … (pc_block (pc … st1)) ≠ -1 →
     887  fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
     888  return 〈f, fn,  final P_in ? (RETURN …)〉 → 
     889  ∀n. stack_sizes f = return n →
     890  let curr_ret ≝ joint_if_result … fn in
     891  ∀st_pop,pc_pop.
     892  pop_frame ?? P_in ? (joint_globalenv P_in prog stack_sizes) f curr_ret
     893   (st_no_pc … st1) = return 〈st_pop,pc_pop〉 →
     894  ∀nxt.∀f1,fn1,id,args,dest.
     895    fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) pc_pop  =
     896    return 〈f1,fn1,sequential P_in … (CALL P_in ? id args dest) nxt〉 →
     897  st_rel st1 st2 →
     898  ∀t_fn.
     899  fetch_internal_function …
     900     (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) =
     901  return 〈f,t_fn〉 →
     902  bind_new_P' ??
     903     (λregs1.λdata.
     904      bind_new_P' ??
     905      (λregs2.λblp.
     906       \snd blp = (RETURN …) ∧
     907       ∃st_fin. repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f
     908              (\fst blp)  (st_no_pc … st2)= return st_fin ∧
     909        ∃t_st_pop,t_pc_pop.
     910        pop_frame ?? P_out ? (joint_globalenv P_out trans_prog stack_sizes) f
     911         (joint_if_result … t_fn) st_fin = return 〈t_st_pop,t_pc_pop〉 ∧
     912        sigma_stored_pc P_in P_out prog stack_sizes init init_regs f_lbls f_regs
     913         t_pc_pop = pc_pop ∧
     914        if eqZb (block_id (pc_block pc_pop)) (-1) then
     915            st_no_pc_rel (pc_of_point P_in (pc_block pc_pop) nxt)
     916             (decrement_stack_usage ? n st_pop) (decrement_stack_usage ? n t_st_pop) (*pre_main*)
     917        else
     918            bind_new_P' ??
     919            (λregs4.λdata1.
     920               bind_new_P' ??
     921               (λregs3.λblp1.
     922                 ∃st2'. repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f1
     923                      (\snd blp1) (decrement_stack_usage ? n t_st_pop) = return st2' ∧
     924                      st_no_pc_rel (pc_of_point P_in (pc_block pc_pop) nxt)
     925                       (decrement_stack_usage ? n st_pop) st2'
     926               ) (f_step … data1 (point_of_pc P_in pc_pop) (CALL P_in ? id args dest))
     927            ) (init ? fn1)
     928          ) (f_fin … data (point_of_pc P_in (pc … st1)) (RETURN …))
     929     ) (init ? fn)
     930\end{lstlisting}
     931
     932\subsubsection{Conclusion}
     933After having provided a semantic relation among states that satifies some conditions that correspond to
     934commutation lemmas that are commonly proved in a forward simulation proof, it is possible to prove the
     935general theorem. All these condition are summarized in a propositional record called \verb=good_state_relation=.
     936The statement we are able to prove have the following shape.
     937\begin{lstlisting}
     938theorem joint_correctness : ∀p_in,p_out : sem_graph_params.
     939∀prog : joint_program p_in.∀stack_size : ident → option ℕ.
     940∀init : (∀globals.joint_closed_internal_function p_in globals →
     941         bound_b_graph_translate_data p_in p_out globals).
     942∀init_regs : block → list register.∀f_lbls : lbl_funct_type.
     943∀f_regs : regs_funct_type.∀st_no_pc_rel : joint_state_relation p_in p_out.
     944∀st_rel : joint_state_pc_relation p_in p_out.
     945good_state_relation p_in p_out prog stack_size init init_regs
     946 f_lbls f_regs st_no_pc_rel st_rel →
     947let trans_prog ≝ b_graph_transform_program … init prog in
     948∀init_in.make_initial_state (mk_prog_params p_in prog stack_size) = OK ? init_in →
     949∃init_out.make_initial_state (mk_prog_params p_out trans_prog stack_size) = OK ? init_out ∧
     950∃[1] R.
     951  status_simulation_with_init
     952    (joint_abstract_status (mk_prog_params p_in prog stack_size))
     953    (joint_abstract_status (mk_prog_params p_out trans_prog stack_size))
     954    R init_in init_out.
     955\end{lstlisting}
     956The module formalizing the formal machienary we described in this document consists of about 3000 lines of
     957Matita code. We stress the fact that this machienary proves general properties that do not depend on the
     958specific backend compiler pass. Without this layer one would have to prove these properties each specific
     959pass multiplying the number of Matita's lines by $n$ where $n$ is the number of backend pass.
     960
     961
     962
    171963
    172964
Note: See TracChangeset for help on using the changeset viewer.