Changeset 3213


Ignore:
Timestamp:
Apr 29, 2013, 6:14:15 PM (4 years ago)
Author:
tranquil
Message:

summary for D4.4, and other modifications

Files:
1 added
4 edited

Legend:

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

    r3194 r3213  
    1 \section{A modular approach to the correctness of the graph passes}
     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.
    26
    37An instance of the record \verb=sem_graph_params= contains all common information about
     
    2832    R init_in init_out.
    2933\end{lstlisting}
    30 When proving this statement (for each concrete istance of language),
     34When proving this statement (for each concrete instance of language),
    3135we need to proceed by cases according the classification of
    3236each state in the source program (\verb=cl_jmp=, \verb=cl_other=, \verb=cl_call= and
    33 \verb=cl_return=) and then proving the suitable conditions explained in
    34 previous Section, according to the case we are currently considering (Condition 1 for
     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
    3539\verb=cl_other= and \verb=cl_jump= case, Condition 2 for \verb=cl_call= or
    36 Condition 3 for \verb=cl_return= case). Roughtly speaking, proving these condition
     40Condition 3 for \verb=cl_return= case). Roughly speaking, proving these conditions
    3741means producing traces of some kind in the target language that are in a suitable
    3842correspondence with an execution step in the source language.
     
    4246the preservation the semantical relation between states of the program under evaluation)
    4347and the intensional part (for example, all proof obbligation dealing with
    44 the presence of a cost label in some point of the code) are mixed together in a not so clear way.
     48the presence of a cost label in some point of the code) are mixed together in a not very clear way.
    4549
    4650Furthermore, some proof obbligations concerning the relation among program counters
     
    109113; good_f_step :
    110114  ∀l,s.bind_new_P' ??
    111     (λlocal_new_regs,block.let 〈pref, op, post〉 ≝ block in
     115    (λlocal_new_regs,block.let 〈 pref, op, post 〉 ≝ block in
    112116       ∀l.
    113117       let allowed_labels ≝ l :: step_labels … s in
     
    124128; good_f_fin :
    125129  ∀l,s.bind_new_P' ??
    126     (λlocal_new_regs,block.let 〈pref, op〉 ≝ block in
     130    (λlocal_new_regs,block.let 〈 pref, op 〉 ≝ block in
    127131       let allowed_labels ≝ l :: fin_step_labels … s in
    128132       let allowed_registers ≝ new_regs @ local_new_regs @ fin_step_registers … s in
     
    134138; f_step_on_cost :
    135139  ∀l,c.f_step l (COST_LABEL … c) =
    136     bret ? (step_block ??) 〈[ ], λ_.COST_LABEL dst globals c, [ ]
     140    bret ? (step_block ??) 〈 [ ], λ_.COST_LABEL dst globals c, [ ]
    137141; cost_in_f_step :
    138142  ∀l,s,c.
     
    240244    ∃lbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧
    241245    joint_if_entry … def_out
    242       -(〈[ ],λ_.COST_LABEL … (get_first_costlabel … def_in), added_prologue … data〉,
     246      -( 〈 [ ],λ_.COST_LABEL … (get_first_costlabel … def_in),
     247           added_prologue … data 〉,
    243248        f_lbls … lbl)-> joint_if_entry … def_in in joint_if_code … def_out
    244249  else (joint_if_entry … def_out = joint_if_entry … def_in)
     
    364369let trans_prog ≝ b_graph_transform_program p_in p_out init prog in
    365370fetch_statement p_in … (joint_globalenv p_in prog stack_sizes) pc =
    366 return 〈f,fn,stmt〉 →
     371return 〈 f,fn,stmt 〉 →
    367372∃data.bind_instantiate ?? (init … fn) (init_regs (pc_block pc)) = return data ∧
    368373match stmt with
     
    387392    ∃fn'.fetch_statement p_out …
    388393       (joint_globalenv p_out trans_prog stack_sizes) pc'
    389        = return 〈f,fn',final ?? (\snd fin_block)〉           
     394       = return 〈 f,fn',final ?? (\snd fin_block) 〉
    390395| FCOND abs _ _ _ ⇒ Ⓧabs
    391396].
     
    446451in memory) and this information depends on the code point on the statement being translated.
    447452
    448 The compositionality requirement is expressed by the following conditions (which are part of a bigger
    449 record, that we are going to introduce later).
    450 
    451 \begin{lstlisting}
    452 ; fetch_ok_sigma_state_ok :
    453    ∀st1,st2,f,fn. st_rel st1 st2 →
    454     fetch_internal_function …
    455      (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 
    456      = return <f,fn> →
    457      st_no_pc_rel (pc … st1) (st_no_pc … st1) (st_no_pc … st2)
    458 ; fetch_ok_pc_ok :
    459   ∀st1,st2,f,fn.st_rel st1 st2 →
    460    fetch_internal_function …
    461      (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 
    462      = return <f,fn> →
    463    pc … st1 = pc … st2
    464 ; fetch_ok_sigma_last_pop_ok :
    465   ∀st1,st2,f,fn.st_rel st1 st2 →
    466    fetch_internal_function …
    467      (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 
    468      = return <f,fn> →
    469    (last_pop … st1) = sigma_stored_pc P_in P_out prog stack_sizes init init_regs
    470                        f_lbls f_regs (last_pop … st2)
    471 ; st_rel_def :
    472   ∀st1,st2,pc,lp1,lp2,f,fn.
    473   fetch_internal_function …
    474      (joint_globalenv P_in prog stack_sizes) (pc_block pc) = return <f,fn> →
    475    st_no_pc_rel pc st1 st2 →
    476    lp1 = sigma_stored_pc P_in P_out prog stack_sizes init init_regs
    477           f_lbls f_regs lp2 →
    478   st_rel (mk_state_pc ? st1 pc lp1) (mk_state_pc ? st2 pc lp2)
    479 \end{lstlisting}
    480 
     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%
    481486Condition \texttt{fetch\_ok\_sigma\_state\_ok} postulates that two state that are in semantical
    482487relation should have their data field also in relation. Condition \texttt{fetch\_ok\_pc\_ok} postulates
     
    490495they are in semantical relation.
    491496
    492 An other important condition is that the pivot statement of the translation of a call statement is
     497Another important condition is that the pivot statement of the translation of a call statement is
    493498always a call statement. This is important in order to obtain the correctness of the call relation
    494 and return relation between state. This condition is formalized by the following Matita's code, and
    495 we call it \texttt{call\_is\_call}.
    496 
    497 \begin{lstlisting}
    498 ;  call_is_call :∀f,fn,bl.
    499   fetch_internal_function …
    500      (joint_globalenv P_in prog stack_sizes) bl = return <f,fn> →
    501    ∀id,args,dest,lbl.
    502     bind_new_P' ??
    503      (λregs1.λdata.bind_new_P' ??
    504       (λregs2.λblp.
    505         ∀lbl.∃id',args',dest'.((\snd (\fst blp)) lbl) = CALL P_out ? id' args' dest')
    506       (f_step … data lbl (CALL P_in ? id args dest)))
    507      (init ? fn)
    508 \end{lstlisting}
     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}
    509514
    510515The conditions we are going to present now are standard semantical commutation lemmas that are commonly
     
    539544$s_1 \simeq_S s_2$ and $s_1' \simeq_S s_2'$.
    540545
    541 \paragraph{Commutation of pre-main instructions.}
     546\paragraph{Commutation of pre-main instructions (\verb=pre_main_ok=).}
    542547In order to get the commutation of pre-main instructions (states whose function location of program counter is -1), we have
    543548to 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$,
     
    550555}
    551556$$
    552 The formalization of this statement in Matita is the following one.
    553 \begin{lstlisting}
    554 ; pre_main_ok :
    555   let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
    556     ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
    557     ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
    558     block_id … (pc_block (pc … st1)) = -1 →
    559     st_rel st1 st2 →
    560     as_label (joint_status P_in prog stack_sizes) st1 =
    561     as_label (joint_status P_out trans_prog stack_sizes) st2 ∧
    562     joint_classify … (mk_prog_params P_in prog stack_sizes) st1 =
    563     joint_classify … (mk_prog_params P_out trans_prog stack_sizes) st2 ∧
    564     (eval_state P_in … (joint_globalenv P_in prog stack_sizes)
    565       st1 = return st1' →
    566     ∃st2'. st_rel st1' st2' ∧
    567     eval_state P_out …
    568      (joint_globalenv P_out trans_prog stack_sizes) st2 = return st2')
    569 \end{lstlisting}
    570 
    571 \paragraph{Commutation of conditional jump.}
     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=).}
    572577For 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
    573578\begin{itemize}
     
    583588      such that $l = l'$.
    584589\end{itemize}
    585 This condition is formalized in Matita in the following way.
    586 \begin{lstlisting}
    587 ; cond_commutation :
    588     let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
    589     ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
    590     ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
    591     ∀f,fn,a,ltrue,lfalse,bv,b.
    592     block_id … (pc_block (pc … st1)) ≠ -1 →
    593     let cond ≝ (COND P_in ? a ltrue) in
    594     fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
    595     return <f, fn,  sequential … cond lfalse> → 
    596     acca_retrieve … P_in (st_no_pc … st1) a = return bv →
    597     bool_of_beval … bv = return b →
    598     st_rel st1 st2 →
    599     ∀t_fn.
    600     fetch_internal_function …
    601      (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) =
    602      return 〈f,t_fn〉 →
    603     bind_new_P' ??
    604      (λregs1.λdata.bind_new_P' ??
    605      (λregs2.λblp.(\snd blp) = [ ] ∧
    606         ∀mid.
    607           stmt_at P_out … (joint_if_code ?? t_fn) mid
    608           = return sequential P_out ? ((\snd (\fst blp)) mid) lfalse→
    609          ∃st2_pre_mid_no_pc.
    610             repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f
    611              (map_eval ?? (\fst (\fst blp)) mid) (st_no_pc ? st2)
    612             = return st2_pre_mid_no_pc ∧
    613             let new_pc ≝ if b then
    614                            (pc_of_point P_in (pc_block (pc … st1)) ltrue)
    615                          else
    616                            (pc_of_point P_in (pc_block (pc … st1)) lfalse) in
    617             st_no_pc_rel new_pc (st_no_pc … st1) (st2_pre_mid_no_pc) ∧
    618             ∃a'. ((\snd (\fst blp)) mid)  = COND P_out ? a' ltrue ∧
    619             ∃bv'. acca_retrieve … P_out st2_pre_mid_no_pc a' = return bv' ∧
    620                   bool_of_beval … bv' = return b
    621    )  (f_step … data (point_of_pc P_in (pc … st1)) cond)   
    622   ) (init ? fn)
    623 \end{lstlisting}
    624 
    625 \paragraph{Commutation of sequential statements.}
     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=).}
    626631In case of a sequential statement $I$, its translation $f\_step(I) = \langle pre , J , post \rangle$ is coerced
    627632into a list of sequential statements $pre$ \verb=@= $[J]$ \verb=@= $post$. Then we can state the condition in the
     
    635640}
    636641$$
    637 The formalization in Matita of the above statement is as follows.
    638 \begin{lstlisting}
    639 ; seq_commutation :
    640   let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
    641   ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
    642   ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
    643   ∀f,fn,stmt,nxt.
    644   block_id … (pc_block (pc … st1)) ≠ -1 →
    645   let seq ≝ (step_seq P_in ? stmt) in
    646   fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
    647   return <f, fn,  sequential … seq nxt> → 
    648   eval_state P_in … (joint_globalenv P_in prog stack_sizes)
    649   st1 = return st1' →
    650   st_rel st1 st2 →
    651   ∀t_fn.
    652   fetch_internal_function …
    653      (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) =
    654   return <f,t_fn> →
    655   bind_new_P' ??
    656      (λregs1.λdata.bind_new_P' ??
    657       (λregs2.λblp.
    658        ∃l : list (joint_seq P_out
    659                   (globals ? (mk_prog_params P_out trans_prog stack_sizes))).
    660                             blp = (ensure_step_block ?? l) ∧
    661        ∃st2_fin_no_pc.
    662            repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f
    663               l  (st_no_pc … st2)= return st2_fin_no_pc ∧
    664            st_no_pc_rel (pc … st1') (st_no_pc … st1') st2_fin_no_pc
    665       ) (f_step … data (point_of_pc P_in (pc … st1)) seq)
    666      ) (init ? fn)
    667 \end{lstlisting}
    668 
    669 \paragraph{Commutation of call statement}
     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=).}
    670675For 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
    671676the statement fetched in the translated language at the program counter being in call relation
     
    685690}
    686691$$
    687 The statement is formalized in Matita in the following way.
    688 \begin{lstlisting}
    689 ; call_commutation :
    690   let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
    691   ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
    692   ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
    693   ∀f,fn,id,arg,dest,nxt.
    694   block_id … (pc_block (pc … st1)) ≠ -1 →
    695   fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
    696   return 〈f, fn,  sequential P_in ? (CALL P_in ? id arg dest) nxt〉 →
    697   ∀bl.
    698    block_of_call P_in … (joint_globalenv P_in prog stack_sizes) id (st_no_pc … st1)
    699       = return bl →
    700   ∀f1,fn1.
    701    fetch_internal_function …
    702     (joint_globalenv P_in prog stack_sizes) bl =  return 〈f1,fn1〉 →
    703   ∀st1_pre.
    704   save_frame … P_in (kind_of_call P_in id) dest st1 = return st1_pre →
    705   ∀n.stack_sizes f1 = return n → 
    706   ∀st1'.
    707   setup_call ?? P_in n (joint_if_params … fn1) arg st1_pre = return st1' →
    708   st_rel st1 st2 → 
    709   ∀t_fn1.
    710   fetch_internal_function … (joint_globalenv P_out trans_prog stack_sizes) bl =
    711   return 〈f1,t_fn1〉 →
    712   bind_new_P' ??
    713     (λregs1.λdata.
    714      bind_new_P' ??
    715       (λregs2.λblp.
    716         ∀pc',t_fn,id',arg',dest',nxt1.
    717           sigma_stored_pc P_in P_out prog stack_sizes init init_regs
    718            f_lbls f_regs pc' = (pc … st1) →
    719           fetch_statement P_out … (joint_globalenv P_out trans_prog stack_sizes) pc'
    720           = return 〈f,t_fn,
    721                     sequential P_out ? ((\snd (\fst blp)) (point_of_pc P_out pc')) nxt1〉→
    722           ((\snd (\fst blp)) (point_of_pc P_out pc')) = (CALL P_out ? id' arg' dest') → 
    723        ∃st2_pre_call.
    724         repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f
    725           (map_eval ?? (\fst (\fst blp)) (point_of_pc P_out pc')) (st_no_pc ? st2) = return st2_pre_call ∧
    726        block_of_call P_out … (joint_globalenv P_out trans_prog stack_sizes) id'
    727         st2_pre_call = return bl ∧
    728        ∃st2_pre.
    729         save_frame … P_out (kind_of_call P_out id') dest'
    730          (mk_state_pc ? st2_pre_call pc' (last_pop … st2)) = return st2_pre ∧
    731        ∃st2_after_call.
    732          setup_call ?? P_out n (joint_if_params … t_fn1) arg' st2_pre
    733           = return st2_after_call ∧
    734        bind_new_P' ??
    735          (λregs11.λdata1.
    736           ∃st2'.
    737            repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f1
    738            (added_prologue … data1) (increment_stack_usage P_out n st2_after_call) =
    739            return st2' ∧
    740            st_no_pc_rel (pc_of_point P_in bl (joint_if_entry … fn1))
    741             (increment_stack_usage P_in n st1') st2'               
    742          ) (init ? fn1)
    743      )
    744      (f_step … data (point_of_pc P_in (pc … st1)) (CALL P_in ? id arg dest))
    745     ) (init ? fn)
    746 \end{lstlisting}
    747 \paragraph{Commutation of return statement}
     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=).}
    748753For 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$
    749754is the call statement that caused the function call ened by the current return (i.e. it is the statement whose code point identifier
     
    759764}
    760765$$
    761 The statement is formalized in Matita in the following way.
    762 \begin{lstlisting}
    763 ; return_commutation :
    764   let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
    765   ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
    766   ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
    767   ∀f,fn.
    768   block_id … (pc_block (pc … st1)) ≠ -1 →
    769   fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
    770   return 〈f, fn,  final P_in ? (RETURN …)〉 → 
    771   ∀n. stack_sizes f = return n →
    772   let curr_ret ≝ joint_if_result … fn in
    773   ∀st_pop,pc_pop.
    774   pop_frame ?? P_in ? (joint_globalenv P_in prog stack_sizes) f curr_ret
    775    (st_no_pc … st1) = return 〈st_pop,pc_pop〉 →
    776   ∀nxt.∀f1,fn1,id,args,dest.
    777     fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) pc_pop  =
    778     return 〈f1,fn1,sequential P_in … (CALL P_in ? id args dest) nxt〉 →
    779   st_rel st1 st2 →
    780   ∀t_fn.
    781   fetch_internal_function …
    782      (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) =
    783   return 〈f,t_fn〉 →
    784   bind_new_P' ??
    785      (λregs1.λdata.
    786       bind_new_P' ??
    787       (λregs2.λblp.
    788        \snd blp = (RETURN …) ∧
    789        ∃st_fin. repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f
    790               (\fst blp)  (st_no_pc … st2)= return st_fin ∧
    791         ∃t_st_pop,t_pc_pop.
    792         pop_frame ?? P_out ? (joint_globalenv P_out trans_prog stack_sizes) f
    793          (joint_if_result … t_fn) st_fin = return 〈t_st_pop,t_pc_pop〉 ∧
    794         sigma_stored_pc P_in P_out prog stack_sizes init init_regs f_lbls f_regs
    795          t_pc_pop = pc_pop ∧
    796         if eqZb (block_id (pc_block pc_pop)) (-1) then
    797             st_no_pc_rel (pc_of_point P_in (pc_block pc_pop) nxt)
    798              (decrement_stack_usage ? n st_pop) (decrement_stack_usage ? n t_st_pop) (*pre_main*)
    799         else
    800             bind_new_P' ??
    801             (λregs4.λdata1.
    802                bind_new_P' ??
    803                (λregs3.λblp1.
    804                  ∃st2'. repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f1
    805                       (\snd blp1) (decrement_stack_usage ? n t_st_pop) = return st2' ∧
    806                       st_no_pc_rel (pc_of_point P_in (pc_block pc_pop) nxt)
    807                        (decrement_stack_usage ? n st_pop) st2'
    808                ) (f_step … data1 (point_of_pc P_in pc_pop) (CALL P_in ? id args dest))
    809             ) (init ? fn1)
    810           ) (f_fin … data (point_of_pc P_in (pc … st1)) (RETURN …))
    811      ) (init ? fn)
    812 \end{lstlisting}
     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}
    813818
    814819\subsubsection{Conclusion}
     
    828833 f_lbls f_regs st_no_pc_rel st_rel →
    829834let trans_prog ≝ b_graph_transform_program … init prog in
    830 ∀init_in.make_initial_state (mk_prog_params p_in prog stack_size) = OK ? init_in →
    831 ∃init_out.make_initial_state (mk_prog_params p_out trans_prog stack_size) = OK ? init_out ∧
     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 ∧
    832839∃[1] R.
    833840  status_simulation_with_init
  • Deliverables/D4.4/paolo.tex

    r3194 r3213  
    5858\lstset{extendedchars=false}
    5959\lstset{inputencoding=utf8x}
    60 \DeclareUnicodeCharacter{8797}{:=}
     60\DeclareUnicodeCharacter{8797}{:=\ }
    6161\DeclareUnicodeCharacter{10746}{++}
    6262\DeclareUnicodeCharacter{9001}{\ensuremath{\langle}}
    6363\DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}}
    64 
     64\DeclareUnicodeCharacter{8230}{.\!\!.\!\!.\@\ }
     65\author{Mauro Piccolo, Claudio Sacerdoti Coen and Paolo Tranquilli\\[15pt]
     66\small Department of Computer Science and Engineering, University of Bologna\\
     67\small \verb|\{Mauro.Piccolo, Claudio.SacerdotiCoen, Paolo.Tranquilli\}@unibo.it|}
     68\title{Certifying the back end pass of the CerCo annotating compiler}
    6569\date{}
    66 \author{}
    6770
    6871\begin{document}
    69 
    70 \thispagestyle{empty}
    71 
    72 \vspace*{-1cm}
    73 \begin{center}
    74 \includegraphics[width=0.6\textwidth]{../style/cerco_logo.png}
    75 \end{center}
    76 
    77 \begin{minipage}{\textwidth}
    7872\maketitle
    79 \end{minipage}
    80 
    81 \vspace*{0.5cm}
    82 \begin{center}
    83 \begin{LARGE}
    84 \textbf{
    85 Report n. D4.4\\
    86 ??????????????
    87 }
    88 \end{LARGE}
    89 \end{center}
    90 
    91 \vspace*{2cm}
    92 \begin{center}
    93 \begin{large}
    94 Version 1.1
    95 \end{large}
    96 \end{center}
    97 
    98 \vspace*{0.5cm}
    99 \begin{center}
    100 \begin{large}
    101 Main Authors:\\
    102 ????????????
    103 \end{large}
    104 \end{center}
    105 
    106 \vspace*{\fill}
    107 
    108 \noindent
    109 Project Acronym: \cerco{}\\
    110 Project full title: Certified Complexity\\
    111 Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\
    112 
    113 \clearpage
    114 \pagestyle{myheadings}
    115 \markright{\cerco{}, FP7-ICT-2009-C-243881}
    116 
    117 \newpage
    118 
    119 \vspace*{7cm}
    120 \paragraph{Abstract}
    121 BLA BLA BLA
    122 \newpage
    123 
    124 \tableofcontents
    125 
    126 \newpage
     73\begin{abstract}
     74We present the certifying effort of the back end of the CerCo annotating
     75compiler to 8051 assembly. Apart from the usual effort needed in propagating
     76the extensional part of execution traces, additional care must be taken in
     77order to ensure a form of intensional correctness of the pass, necessary to
     78prove the lifting of computational costs correct. We concentrate here on two
     79aspects of the proof: how stack is dealt with during the pass, and how generic graph
     80language passes can be proven correct from an extensional and intensional point
     81of view.
     82\end{abstract}
    12783
    12884\section{The Back-End Correctness Proof at a Glance}
     85\label{sec:glance}
    12986
    13087The back-end part of the compiler takes an \s{RTLabs} program together with
    13188an initialising cost label and gives the assembly code to be fed to the
    13289assembler. From the semantic point of view, at this stage of the compiler,
    133 we are interested in propagating structured traces, as explained in \cite{?}.
     90we are interested in propagating structured traces, as explained in \cite{simulation}.
    13491
    13592A schema with all the back-end passes and the salient and common points of each one is the following:
     
    156113The next two passes live in the graph part of \verb+joint+, and can benefit from
    157114a generic approach to graph translation and its proof of correctness, as described
    158 in~\cite{mauro}.
     115in~\autoref{modular}.
    159116
    160117Next, a generic \verb+joint+ linearisation pass is performed to go from
     
    171128to relate the states in the two languages.
    172129
    173 \subsection{A common invariant} This block of traces with properties is recurrent enough to merit the
     130\subsection{A common invariant}
     131This block of traces with properties is recurrent enough to merit the
    174132\s{matita} definition in \autoref{fig:ft_and_tlr}. We rely on the fact
    175133that all semantics from \s{RTLabs} down to object code can be expressed
     
    201159The additional property \verb+tlr_unrpt+
    202160tells that program counters do not repeat locally (i.e.\ between two labels)
    203 in \verb+tlr+, a property needed for the soundness of the cost static analysis
    204 (cf.~\cite{?}).
     161in \verb+tlr+, a property needed for the soundness of the cost static analysis.
    205162
    206163\subsection{The statement}
     
    212169only with respect to the \s{ASM} to object code correctness
    213170\footnote{\verb+sigma+ and \verb+pol+ are what allows to maps instructions
    214 between \s{ASM} and the produced object code. This information isgained during
    215 the jump expansion pass, cf.~\cite{?}.}.
     171between \s{ASM} and the produced object code. This information is gained during
     172the jump expansion pass, cf.~\cite{policy}.}.
    216173
    217174\begin{figure}
     
    261218front-end traces, and we put it to use during the back-end pass,
    262219where we pass to a unique bounded stack space for all functions. More details
    263 will be presented in \autoref{sec:?}.
     220will be presented in \autoref{sec:stack}.
    264221
    265222The above explanation is why the back-end correctness results requires some additional preconditions
     
    270227actually the initial state).
    271228
    272 \section{Dealing with the stack}
     229\section{Dealing with the Stack}
     230\label{sec:stack}
    273231Setting apart the extensional details of the proofs, a delicate point is how
    274232we deal with stack.
     
    428386with respect to execution. There are more details involved than in a usual
    429387extensional proof, regarding the intensional preservation. The details are
    430 contained in~\cite{?}.
     388contained in~\cite{simulation}.
    431389
    432390Here we concentrate on a particular aspect that eludes the generic treatment:
     
    467425as it is integrated in the fact that the execution step does not fail.
    468426
    469 \include{mauro}
     427\input{mauro.tex}
     428
     429\bibliographystyle{plain}
     430\bibliography{report}
    470431\end{document}
  • Deliverables/D4.4/report.tex

    r3194 r3213  
    7979\begin{large}
    8080Main Authors:\\
    81 XXXX %Dominic P. Mulligan and Claudio Sacerdoti Coen
     81Jaap Boender, Dominic P. Mulligan, Mauro Piccolo,\\ Claudio Sacerdoti Coen and
     82Paolo Tranquilli
    8283\end{large}
    8384\end{center}
     
    9798
    9899\vspace*{7cm}
    99 \paragraph{Abstract}
    100 xxx
     100\paragraph{Summary}
     101The deliverable D4.4 is composed of the following parts:
     102
     103\begin{enumerate}
     104
     105\item This summary.
     106
     107\item The paper \cite{simulation}.
     108
     109\item The paper \cite{backend}.
     110
     111\item The paper \cite{asm}.
     112
     113\item The paper \cite{policy}.
     114
     115\end{enumerate}
     116
     117This document and all the related \textsf{matita} developments can be downloaded at the
     118page:
     119\begin{center}
     120{\tt http://cerco.cs.unibo.it/}
     121\end{center}
     122
     123\bibliographystyle{unsrt}
     124{\scriptsize\bibliography{report}}
    101125
    102126\newpage
    103127
    104 \tableofcontents
     128\paragraph{Aim}
     129The aim of WP4 is is to build the trusted version of the compiler back-end,
     130from the intermediate \textsf{RTLabs} language down to assembly. The development
     131is made in \textsf{matita}, and it allows the trsuted compiler to be extracted
     132to \textsf{OCaml}.
    105133
    106 \newpage
     134The main planned contributions of deliverable D4.4 are formally checked proof
     135of the semantics correspondence between the intermediate code and the target
     136code, and of the preservation/modification of the control flow for complexity
     137analysis.
    107138
    108 \section{Task}
    109 \label{sect.task}
     139\paragraph{Preservation of structure}
     140In \cite{simulation} we present a genric approach to proving a forward
     141simulation preserving the intensional structure of traces.
    110142
    111 The Grant Agreement describes deliverable D4.4 as follows:
    112 \begin{quotation}
    113 \textbf{Back-end correctness proof}: Formally checked proof of the semantics correspondence between the intermediate code and the target code, and of the preservation/modification of the control flow for complexity analysis. An extensive validation of implementation of the Untrusted Cerco Prototype D5.1 is achieved and reported in the deliverable, possibly triggering updates of the Untrusted CerCo Compiler sources and CIC encoding (D2.2, D5.1 and D4.2).
    114 \end{quotation}
     143When a language
     144starts to be able to meddle with return addresses that live in memory, the call structure
     145is no more guaranteed to be preserved after the high-level, structured
     146languages. This is has little meaning as far as pure extensional semantic
     147preservation is required---after all, if the source language meddles with the
     148call structure there is no problem as long as the target language will follow.
     149However in our approach we have cost labels spanning multiple calls, so that
     150the cost of what follows a call is ``paid'' in advance. This has no hope of
     151being correct if there is no guarantee that upon return from a call we land
     152after the call itself.
    115153
    116 \newpage
     154In this part of the deliverable we will present our approach to this problem,
     155which goes by including in semantic traces structural conditions, and giving
     156generic proof obligations that enrich the classic step-by-step extensional
     157preservation proof with the necessary hypotheses to ensure the preservation
     158of the call and label structures. This approach can be applied on all passes
     159starting from the \textsf{RTLabs} to \textsf{RTL} down to the assembly one.
     160
     161\paragraph{The back-end correctness proof}
     162In \cite{backend}, we give an outline of the actual correctness proof for the
     163passes from \textsf{RTLabs} down to assembly. We skip the details of the
     164extensional parts of each pass and we concentrate on two main aspects:
     165how we deal with stack and how we ensure the conditions explained in
     166\cite{simulation} in the passes involving graph languages.
     167
     168\paragraph{The assembler correctness proof}
     169In \cite{asm}, we present a proof of correctness of our assembler to object
     170code, given a correct policy for branch expansion (see next paragraph).
     171
     172\paragraph{A branch expansion policy maker}
     173In \cite{policy} we finally present our algorithm for branch expansion, that is
     174how generic assembly jumps are expanded to the different type of jumps
     175available in the 8051 architecture (short, absolute and long). The correctness
     176of this algorithm is proved, and is what required by the correctness of the
     177whole assembler.
    117178
    118179\includepdf[pages={-}]{itp2013.pdf}
  • Papers/itp-2013/ccexec.tex

    r2637 r3213  
    12641264\bibliography{ccexec}
    12651265
    1266 \appendix
    1267 \section{Notes for the reviewers}
    1268 
    1269 The results described in the paper are part of a larger formalization
    1270 (the certification of the CerCo compiler). At the moment of the submission
    1271 we need to single out from the CerCo formalization the results presented here.
    1272 Before the 16-th of February we will submit an attachment that contains the
    1273 minimal subset of the CerCo formalization that allows to prove those results.
    1274 At that time it will also be possible to measure exactly the size of the
    1275 formalization described here. At the moment a rough approximation suggests
    1276 about 2700 lines of Matita code.
    1277 
    1278 We will also attach the development version of the interactive theorem
    1279 prover Matita that compiles the submitted formalization. Another possibility
    1280 is to backport the development to the last released version of the system
    1281 to avoid having to re-compile Matita from scratch.
    1282 
    1283 The programming and certification style used in the formalization heavily
    1284 exploit dependent types. Dependent types are used: 1) to impose invariants
    1285 by construction on the data types and operations (e.g. a traces from a state
    1286 $s_1$ to a state $s_2$ can be concatenad to a trace from a state
    1287 $s_2'$ to a state $s_3$ only if $s_2$ is convertible with $s_2'$); 2)
    1288 to state and prove the theorems by using the Russell methodology of
    1289 Matthieu Sozeau\footnote{Subset Coercions in Coq in TYPES'06. Matthieu Sozeau. Thorsten Altenkirch and Conor McBride (Eds). Volume 4502 of Lecture Notes in Computer Science. Springer, 2007, pp.237-252.
    1290 }, better known in the Coq world as ``\texttt{Program}'' and reimplemented in a simpler way in Matita using coercion propagations\footnote{Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi: A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions. Logical Methods in Computer Science 8(1) (2012)}. However, no result presented depends
    1291 mandatorily on dependent types: it should be easy to adapt the technique
    1292 and results presented in the paper to HOL.
    1293 
    1294 Finally, Matita and Coq are based on minor variations of the Calculus of
    1295 (Co)Inductive Constructions. These variations do not affect the CerCo
    1296 formalization. Therefore a porting of the proofs and ideas to Coq would be
    1297 rather straightforward.
     1266% \appendix
     1267% \section{Notes for the reviewers}
     1268%
     1269% The results described in the paper are part of a larger formalization
     1270% (the certification of the CerCo compiler). At the moment of the submission
     1271% we need to single out from the CerCo formalization the results presented here.
     1272% Before the 16-th of February we will submit an attachment that contains the
     1273% minimal subset of the CerCo formalization that allows to prove those results.
     1274% At that time it will also be possible to measure exactly the size of the
     1275% formalization described here. At the moment a rough approximation suggests
     1276% about 2700 lines of Matita code.
     1277%
     1278% We will also attach the development version of the interactive theorem
     1279% prover Matita that compiles the submitted formalization. Another possibility
     1280% is to backport the development to the last released version of the system
     1281% to avoid having to re-compile Matita from scratch.
     1282%
     1283% The programming and certification style used in the formalization heavily
     1284% exploit dependent types. Dependent types are used: 1) to impose invariants
     1285% by construction on the data types and operations (e.g. a traces from a state
     1286% $s_1$ to a state $s_2$ can be concatenad to a trace from a state
     1287% $s_2'$ to a state $s_3$ only if $s_2$ is convertible with $s_2'$); 2)
     1288% to state and prove the theorems by using the Russell methodology of
     1289% Matthieu Sozeau\footnote{Subset Coercions in Coq in TYPES'06. Matthieu Sozeau. Thorsten Altenkirch and Conor McBride (Eds). Volume 4502 of Lecture Notes in Computer Science. Springer, 2007, pp.237-252.
     1290% }, better known in the Coq world as ``\texttt{Program}'' and reimplemented in a simpler way in Matita using coercion propagations\footnote{Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi: A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions. Logical Methods in Computer Science 8(1) (2012)}. However, no result presented depends
     1291% mandatorily on dependent types: it should be easy to adapt the technique
     1292% and results presented in the paper to HOL.
     1293%
     1294% Finally, Matita and Coq are based on minor variations of the Calculus of
     1295% (Co)Inductive Constructions. These variations do not affect the CerCo
     1296% formalization. Therefore a porting of the proofs and ideas to Coq would be
     1297% rather straightforward.
    12981298
    12991299\end{document}
Note: See TracChangeset for help on using the changeset viewer.