(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "Simulation.ma".
include "Vm.ma". 
include "Lang_meas.ma". 

theorem cerco:
 ∀l_p : label_params.
 (* Given the operational semantics of a source program *)
 ∀S1: abstract_status l_p.

 (* Given the compiled assembly program *)
 ∀p,p',prog.
 
 (* Let S2 be the operational semantics of the compiled code  *)
 let S2 ≝ asm_operational_semantics p l_p p' prog in
 
 (* If the simulation conditions between the source and compiled
    code holds (i.e. if the compiler is correct) *)
 ∀rel: relations … S1 S2. simulation_conditions … rel →

 (* Given an abstract interpretation framework for the compiled code *)
 ∀R: asm_abstract_interpretation p p' … prog.
 
 (* If the static analysis does not fail *)
 ∀mT,map1. ∀EQmap : static_analisys … (instr_map … R) mT prog = return map1.

 (* For every source trace whose measurable fragment starts in s1 and ends in s2 or,
   equivalently, whose state after the initial labelled transition is s1 
   and whose state after the final labelled transition is s2  *)
 ∀si,s1,s2,sn. ∀t: raw_trace … S1 … si sn.
 measurable … s1 s2 … t →

 (* For each target non I/O state si' in relation with the source state si *)
 ∀si': S2. as_classify … si' ≠ cl_io → Srel … rel si si' →

 (* There exists a corresponding target trace starting from si' *)
 ∃sn'. ∃t': raw_trace … si' sn'.
  Srel … rel sn sn' ∧
  ∃EQ:get_costlabels_of_trace … t = get_costlabels_of_trace … t'. 
 
 (* that has a measurable fragment starting in s1' and ending in s2' *)
 ∃s1',s2'. measurable … s1' s2' … t' ∧

 (* Let labels be the costlabels observed in the trace (last one excluded) *)
 let labels ≝ chop … (get_costlabels_of_trace …  t) in

(* Let abs_actions be the list of statically computed abstract actions
   associated to each label in labels. *)
 ∀abs_actions.
  abs_actions =
   dependent_map … labels (λlbl,prf.(opt_safe … (get_map … map1 lbl) …)) →

 (* Given an abstract state in relation with the first state of the measurable
    fragment *)
 ∀a1.R s1' a1 →

 (* The final state of the measurable fragment is in relation with the one
   obtained by applying every semantics in abs_trace. *)
 R s2' (〚abs_actions〛 a1).
[2: @hide_prf normalize nodelta in prf; >EQ in prf; #prf
    cases(mem_map ????? (labels_of_trace_are_in_code … (chop_mem … prf))) *
    #lbl' #pc * #Hmem #EQ destruct
    >(proj1 … (static_analisys_ok … EQmap … Hmem))
    @(proj2 … (static_analisys_ok … EQmap … Hmem))]
#l_p #S1 #p #p' #prog letin S2 ≝ (asm_operational_semantics ????) #rel #sim_conds
#R #mT #map #EQmap #si #s1 #s2 #sn #t #Hmeas #si' #Hclass #Rsisi'
cases (simulates_measurable … S1 S2 rel sim_conds … Hmeas … Rsisi') 
[2: #H cases Hclass >H #ABS cases(ABS (refl …)) ]
#sn' * #t' ** #Rsnsn' #EQcostlabs * #s1' * #s2' #Hmeas'
%{sn'} %{t'} %{Rsnsn'} %{EQcostlabs} %{s1'} %{s2'} %{Hmeas'} #acts #EQacts
@(static_dynamic … EQmap … Hmeas') >rewrite_in_dependent_map
[2: <EQcostlabs in ⊢ (??%?); % | // ]
qed.


lemma action_on_permutation : ∀M : abstract_transition_sys.is_abelian (abs_instr M) → 
∀l1,l2 : list (abs_instr M).∀a.is_permutation … l1 l2 → 
(〚l1〛 a) = (〚l2〛 a).
#M #Hab #l1 elim l1 -l1
[ * // #x #xs #a #H lapply(H x) normalize >(\b (refl …)) normalize #EQ destruct]
#x #xs #IH #l #a #H cases(is_permutation_case … H) #l1 * #l2 * #H1 #H2 destruct 
change with ([?]@?) in match (?::?); >big_op_associative >act_op >(IH … H1)
<associative_append
>big_op_associative in ⊢ (???%); >big_op_associative in ⊢ (???%); >(Hab … l1)
>is_associative >act_op in ⊢ (???%); <big_op_associative in ⊢ (???%); %
qed.

theorem final_cerco : 
(* for all programs in the imperative language (possibly with call non post labelled) *)
∀p,p',prog.
no_duplicates_labels … prog → 

(* let t_prog be the same program in which all calls are post-labelled *)
let 〈t_prog,m,keep〉 ≝ trans_prog … prog in

(* Let S1 be the operational semantics of the source code  *)
let S1 ≝ operational_semantics p p' prog in 

(* Let S2 be the operational semantics of the soource code with call post labelled  *)
let S2 ≝ operational_semantics p p' t_prog in

(* for all assmbler programs *)
∀p_asm,p_asm',prog_asm.
(* Let S3 be the operational semantics of the compiled code  *)
let S3 ≝ asm_operational_semantics p_asm p p_asm' prog_asm in

(* If the simulation conditions between the source with call post-labelled and compiled
    code holds (i.e. if the compiler is correct after the first pass) *)
∀rel: relations … S2 S3. simulation_conditions … rel →

(* let REL be semantical relation between the states of the source program and
   the states of compiled code *)
let REL ≝ λsi : S1.λsi' : S3.∃si'' : S2.∃abs_top,abs_tail.state_rel … m keep abs_top abs_tail si si'' ∧
Srel … rel si'' si' in

 (* Given an abstract interpretation framework for the compiled code *)
∀R: asm_abstract_interpretation p_asm p_asm' … prog_asm.

(* If the abstract instructions monoid is abelian *)
is_abelian (abs_instr … (aabs_d … (asm_galois_conn … R))) →  
 
 (* If the static analysis does not fail *)
∀mT,map1. ∀EQmap : static_analisys … (instr_map … R) mT prog_asm = return map1.

 (* For every source trace whose measurable fragment starts in s1 and ends in s2 or,
   equivalently, whose state after the initial labelled transition is s1 
   and whose state after the final labelled transition is s2  *)
 ∀si,s1,s2,sn. ∀t: raw_trace … S1 … si sn.
 measurable … s1 s2 … t →

 (* For each target non I/O state si' in relation with the source state si *)
 ∀si': S3. as_classify … si' ≠ cl_io → REL si si' →

 (* There exists a corresponding target trace starting from si' *)
 ∃sn'. ∃t': raw_trace … si' sn'.
  REL sn sn' ∧ 
  
   (* Let labels be the costlabels observed in the trace of the source with all call post-labelled 
     (last one excluded), that can be computed from the costlabels observed in the trace of
     the source language *)
 let labels ≝ map_labels_on_trace … m … (chop … (get_costlabels_of_trace …  t)) in
  
  (*The labels emitted by the trace of the source with all call post-labelled 
    is a permutation of the labels emitted by the target trace (excluded the last one) *)
  ∃perm:is_permutation … labels (chop … (get_costlabels_of_trace … t')).
 
 (* that has a measurable fragment starting in s1' and ending in s2' *)
 ∃s1',s2'. measurable … s1' s2' … t' ∧

(* Let abs_actions be the list of statically computed abstract actions
   associated to each label in labels. *)
 ∀abs_actions.
  abs_actions =
   dependent_map … labels (λlbl,prf.(opt_safe … (get_map … map1 lbl) …)) →

 (* Given an abstract state in relation with the first state of the measurable
    fragment *)
 ∀a1.R s1' a1 →

 (* The final state of the measurable fragment is in relation with the one
   obtained by applying every semantics in abs_trace. *)
 R s2' (〚abs_actions〛 a1).
[2: @hide_prf normalize nodelta in prf; change with labels in prf : (???%);
    lapply(is_permutation_mem … prf … perm) -prf #prf
    cases(mem_map ????? (labels_of_trace_are_in_code … (chop_mem … prf))) *
    #lbl' #pc * #Hmem #EQ destruct
    >(proj1 … (static_analisys_ok … EQmap … Hmem))
    @(proj2 … (static_analisys_ok … EQmap … Hmem))
]
#p #p' #prog #no_dup @pair_elim * #t_prog #m #keep #EQt_prog normalize nodelta
#p_asm #p_asm' #prog_asm #rel #sim_cond #R #abelian #mT #map #EQmap #si #s1 #s2 #sn
#t #meas_t #si' #Hclass * #si'' * #abs_top * #abs_tail * #Rsi_si'' #Rsi_si'
lapply(correctness_theorem … p' prog no_dup) >EQt_prog normalize nodelta
#H cases(H … meas_t … Rsi_si'') -H #abs_top' * #abs_tail' * #sn'' * #t'' ** #Rsn_sn''
#Hperm * #s1'' * #s2'' #meas_t''
cases(cerco … sim_cond … EQmap … meas_t'' … Rsi_si') //
#sn' * #t' * #Rsn_sn' * #EQcost * #s1' * #s2' * #meas_t' normalize nodelta #Hcerco
%{sn'} %{t'} %
[ %{sn''} %{abs_top'} %{abs_tail'} /2 by conj/ ] %
 [ @(is_permutation_transitive … Hperm) >EQcost // ]
 %{s1'} %{s2'} %{meas_t'} #abs_actions #EQactions #a1 #Rs1_a1
 >(action_on_permutation … abelian)
 [@Hcerco [% | assumption]
 | >EQactions -EQactions @is_permutation_dependent_map //
 |
 ]
qed.

(* TODO:
1. Spostare chop e eliminare suffix.
2. La block cost non fallisce in caso di I/O.
3. Integrare la prima passata di Language nel risultato finale
5. Cambi al control flow: Paolo's trick (label = coppia label-pezzo di stato)
6. Rappresentabilita' di I, [[ ]] e stati astratti =⇒ instrumentazione 
*)

(* TO SAY
1) in una misurabile le silenti prima/dopo l'IO sono già automaticamente vuote (perchè una silente
inizia/termina in un IO solo se vuota
2) non chiediamo di non potere transire in una iniziale/da un finale perchè non ci serve; se uno lo
aggiunge ha automaticamente che le silenti sono vuote come nel caso IO.
*)