source: LTS/Final.ma

Last change on this file was 3552, checked in by piccolo, 5 years ago

closed all daemons

File size: 9.7 KB
RevLine 
[3507]1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "Simulation.ma".
[3535]16include "Vm.ma".
17include "Lang_meas.ma".
[3507]18
[3509]19theorem cerco:
[3549]20 ∀l_p : label_params.
[3507]21 (* Given the operational semantics of a source program *)
[3549]22 ∀S1: abstract_status l_p.
[3507]23
24 (* Given the compiled assembly program *)
25 ∀p,p',prog.
26 
27 (* Let S2 be the operational semantics of the compiled code  *)
[3549]28 let S2 ≝ asm_operational_semantics p l_p p' prog in
[3507]29 
30 (* If the simulation conditions between the source and compiled
31    code holds (i.e. if the compiler is correct) *)
[3549]32 ∀rel: relations … S1 S2. simulation_conditions … rel →
[3507]33
34 (* Given an abstract interpretation framework for the compiled code *)
[3549]35 ∀R: asm_abstract_interpretation p p' … prog.
[3507]36 
37 (* If the static analysis does not fail *)
38 ∀mT,map1. ∀EQmap : static_analisys … (instr_map … R) mT prog = return map1.
39
40 (* For every source trace whose measurable fragment starts in s1 and ends in s2 or,
41   equivalently, whose state after the initial labelled transition is s1
42   and whose state after the final labelled transition is s2  *)
[3549]43 ∀si,s1,s2,sn. ∀t: raw_trace … S1 … si sn.
[3507]44 measurable … s1 s2 … t →
45
46 (* For each target non I/O state si' in relation with the source state si *)
[3549]47 ∀si': S2. as_classify … si' ≠ cl_io → Srel … rel si si' →
[3507]48
49 (* There exists a corresponding target trace starting from si' *)
50 ∃sn'. ∃t': raw_trace … si' sn'.
[3509]51  Srel … rel sn sn' ∧
52  ∃EQ:get_costlabels_of_trace … t = get_costlabels_of_trace … t'.
[3507]53 
54 (* that has a measurable fragment starting in s1' and ending in s2' *)
55 ∃s1',s2'. measurable … s1' s2' … t' ∧
56
57 (* Let labels be the costlabels observed in the trace (last one excluded) *)
58 let labels ≝ chop … (get_costlabels_of_trace …  t) in
59
60(* Let abs_actions be the list of statically computed abstract actions
61   associated to each label in labels. *)
62 ∀abs_actions.
63  abs_actions =
64   dependent_map … labels (λlbl,prf.(opt_safe … (get_map … map1 lbl) …)) →
65
66 (* Given an abstract state in relation with the first state of the measurable
67    fragment *)
68 ∀a1.R s1' a1 →
69
70 (* The final state of the measurable fragment is in relation with the one
71   obtained by applying every semantics in abs_trace. *)
72 R s2' (〚abs_actions〛 a1).
[3509]73[2: @hide_prf normalize nodelta in prf; >EQ in prf; #prf
[3507]74    cases(mem_map ????? (labels_of_trace_are_in_code … (chop_mem … prf))) *
75    #lbl' #pc * #Hmem #EQ destruct
76    >(proj1 … (static_analisys_ok … EQmap … Hmem))
[3510]77    @(proj2 … (static_analisys_ok … EQmap … Hmem))]
[3549]78#l_p #S1 #p #p' #prog letin S2 ≝ (asm_operational_semantics ????) #rel #sim_conds
[3510]79#R #mT #map #EQmap #si #s1 #s2 #sn #t #Hmeas #si' #Hclass #Rsisi'
[3549]80cases (simulates_measurable … S1 S2 rel sim_conds … Hmeas … Rsisi')
[3535]81[2: #H cases Hclass >H #ABS cases(ABS (refl …)) ]
[3510]82#sn' * #t' ** #Rsnsn' #EQcostlabs * #s1' * #s2' #Hmeas'
83%{sn'} %{t'} %{Rsnsn'} %{EQcostlabs} %{s1'} %{s2'} %{Hmeas'} #acts #EQacts
84@(static_dynamic … EQmap … Hmeas') >rewrite_in_dependent_map
85[2: <EQcostlabs in ⊢ (??%?); % | // ]
[3540]86qed.
[3511]87
[3540]88
[3535]89lemma action_on_permutation : ∀M : abstract_transition_sys.is_abelian (abs_instr M) →
90∀l1,l2 : list (abs_instr M).∀a.is_permutation … l1 l2 →
91(〚l1〛 a) = (〚l2〛 a).
[3540]92#M #Hab #l1 elim l1 -l1
93[ * // #x #xs #a #H lapply(H x) normalize >(\b (refl …)) normalize #EQ destruct]
94#x #xs #IH #l #a #H cases(is_permutation_case … H) #l1 * #l2 * #H1 #H2 destruct
95change with ([?]@?) in match (?::?); >big_op_associative >act_op >(IH … H1)
96<associative_append
97>big_op_associative in ⊢ (???%); >big_op_associative in ⊢ (???%); >(Hab … l1)
98>is_associative >act_op in ⊢ (???%); <big_op_associative in ⊢ (???%); %
[3535]99qed.
100
101theorem final_cerco :
102(* for all programs in the imperative language (possibly with call non post labelled) *)
103∀p,p',prog.
104no_duplicates_labels … prog →
105
106(* let t_prog be the same program in which all calls are post-labelled *)
107let 〈t_prog,m,keep〉 ≝ trans_prog … prog in
108
109(* Let S1 be the operational semantics of the source code  *)
110let S1 ≝ operational_semantics p p' prog in
111
112(* Let S2 be the operational semantics of the soource code with call post labelled  *)
113let S2 ≝ operational_semantics p p' t_prog in
114
115(* for all assmbler programs *)
116∀p_asm,p_asm',prog_asm.
117(* Let S3 be the operational semantics of the compiled code  *)
[3549]118let S3 ≝ asm_operational_semantics p_asm p p_asm' prog_asm in
[3535]119
120(* If the simulation conditions between the source with call post-labelled and compiled
121    code holds (i.e. if the compiler is correct after the first pass) *)
[3549]122∀rel: relations … S2 S3. simulation_conditions … rel →
[3535]123
124(* let REL be semantical relation between the states of the source program and
125   the states of compiled code *)
126let REL ≝ λsi : S1.λsi' : S3.∃si'' : S2.∃abs_top,abs_tail.state_rel … m keep abs_top abs_tail si si'' ∧
127Srel … rel si'' si' in
128
129 (* Given an abstract interpretation framework for the compiled code *)
[3549]130∀R: asm_abstract_interpretation p_asm p_asm' … prog_asm.
[3535]131
132(* If the abstract instructions monoid is abelian *)
133is_abelian (abs_instr … (aabs_d … (asm_galois_conn … R))) → 
134 
135 (* If the static analysis does not fail *)
136∀mT,map1. ∀EQmap : static_analisys … (instr_map … R) mT prog_asm = return map1.
137
138 (* For every source trace whose measurable fragment starts in s1 and ends in s2 or,
139   equivalently, whose state after the initial labelled transition is s1
140   and whose state after the final labelled transition is s2  *)
[3549]141 ∀si,s1,s2,sn. ∀t: raw_trace … S1 … si sn.
[3535]142 measurable … s1 s2 … t →
143
144 (* For each target non I/O state si' in relation with the source state si *)
145 ∀si': S3. as_classify … si' ≠ cl_io → REL si si' →
146
147 (* There exists a corresponding target trace starting from si' *)
148 ∃sn'. ∃t': raw_trace … si' sn'.
149  REL sn sn' ∧
150 
151   (* Let labels be the costlabels observed in the trace of the source with all call post-labelled
152     (last one excluded), that can be computed from the costlabels observed in the trace of
153     the source language *)
154 let labels ≝ map_labels_on_trace … m … (chop … (get_costlabels_of_trace …  t)) in
155 
156  (*The labels emitted by the trace of the source with all call post-labelled
157    is a permutation of the labels emitted by the target trace (excluded the last one) *)
158  ∃perm:is_permutation … labels (chop … (get_costlabels_of_trace … t')).
159 
160 (* that has a measurable fragment starting in s1' and ending in s2' *)
161 ∃s1',s2'. measurable … s1' s2' … t' ∧
162
163(* Let abs_actions be the list of statically computed abstract actions
164   associated to each label in labels. *)
165 ∀abs_actions.
166  abs_actions =
167   dependent_map … labels (λlbl,prf.(opt_safe … (get_map … map1 lbl) …)) →
168
169 (* Given an abstract state in relation with the first state of the measurable
170    fragment *)
171 ∀a1.R s1' a1 →
172
173 (* The final state of the measurable fragment is in relation with the one
174   obtained by applying every semantics in abs_trace. *)
175 R s2' (〚abs_actions〛 a1).
176[2: @hide_prf normalize nodelta in prf; change with labels in prf : (???%);
177    lapply(is_permutation_mem … prf … perm) -prf #prf
178    cases(mem_map ????? (labels_of_trace_are_in_code … (chop_mem … prf))) *
179    #lbl' #pc * #Hmem #EQ destruct
180    >(proj1 … (static_analisys_ok … EQmap … Hmem))
181    @(proj2 … (static_analisys_ok … EQmap … Hmem))
182]
183#p #p' #prog #no_dup @pair_elim * #t_prog #m #keep #EQt_prog normalize nodelta
184#p_asm #p_asm' #prog_asm #rel #sim_cond #R #abelian #mT #map #EQmap #si #s1 #s2 #sn
185#t #meas_t #si' #Hclass * #si'' * #abs_top * #abs_tail * #Rsi_si'' #Rsi_si'
186lapply(correctness_theorem … p' prog no_dup) >EQt_prog normalize nodelta
187#H cases(H … meas_t … Rsi_si'') -H #abs_top' * #abs_tail' * #sn'' * #t'' ** #Rsn_sn''
188#Hperm * #s1'' * #s2'' #meas_t''
189cases(cerco … sim_cond … EQmap … meas_t'' … Rsi_si') //
190#sn' * #t' * #Rsn_sn' * #EQcost * #s1' * #s2' * #meas_t' normalize nodelta #Hcerco
191%{sn'} %{t'} %
192[ %{sn''} %{abs_top'} %{abs_tail'} /2 by conj/ ] %
193 [ @(is_permutation_transitive … Hperm) >EQcost // ]
194 %{s1'} %{s2'} %{meas_t'} #abs_actions #EQactions #a1 #Rs1_a1
195 >(action_on_permutation … abelian)
196 [@Hcerco [% | assumption]
197 | >EQactions -EQactions @is_permutation_dependent_map //
198 |
199 ]
200qed.
201
[3511]202(* TODO:
[3535]2031. Spostare chop e eliminare suffix.
2042. La block cost non fallisce in caso di I/O.
[3511]2053. Integrare la prima passata di Language nel risultato finale
2065. Cambi al control flow: Paolo's trick (label = coppia label-pezzo di stato)
2076. Rappresentabilita' di I, [[ ]] e stati astratti =⇒ instrumentazione
[3531]208*)
209
210(* TO SAY
2111) in una misurabile le silenti prima/dopo l'IO sono già automaticamente vuote (perchè una silente
212inizia/termina in un IO solo se vuota
2132) non chiediamo di non potere transire in una iniziale/da un finale perchè non ci serve; se uno lo
214aggiunge ha automaticamente che le silenti sono vuote come nel caso IO.
215*)
Note: See TracBrowser for help on using the repository browser.