source: LTS/Final.ma @ 3549

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

added paolo's trick

File size: 13.4 KB
Line 
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".
16include "Vm.ma".
17include "Lang_meas.ma".
18
19theorem cerco:
20 ∀l_p : label_params.
21 (* Given the operational semantics of a source program *)
22 ∀S1: abstract_status l_p.
23
24 (* Given the compiled assembly program *)
25 ∀p,p',prog.
26 
27 (* Let S2 be the operational semantics of the compiled code  *)
28 let S2 ≝ asm_operational_semantics p l_p p' prog in
29 
30 (* If the simulation conditions between the source and compiled
31    code holds (i.e. if the compiler is correct) *)
32 ∀rel: relations … S1 S2. simulation_conditions … rel →
33
34 (* Given an abstract interpretation framework for the compiled code *)
35 ∀R: asm_abstract_interpretation p p' … prog.
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  *)
43 ∀si,s1,s2,sn. ∀t: raw_trace … S1 … si sn.
44 measurable … s1 s2 … t →
45
46 (* For each target non I/O state si' in relation with the source state si *)
47 ∀si': S2. as_classify … si' ≠ cl_io → Srel … rel si si' →
48
49 (* There exists a corresponding target trace starting from si' *)
50 ∃sn'. ∃t': raw_trace … si' sn'.
51  Srel … rel sn sn' ∧
52  ∃EQ:get_costlabels_of_trace … t = get_costlabels_of_trace … t'.
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).
73[2: @hide_prf normalize nodelta in prf; >EQ in prf; #prf
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))
77    @(proj2 … (static_analisys_ok … EQmap … Hmem))]
78#l_p #S1 #p #p' #prog letin S2 ≝ (asm_operational_semantics ????) #rel #sim_conds
79#R #mT #map #EQmap #si #s1 #s2 #sn #t #Hmeas #si' #Hclass #Rsisi'
80cases (simulates_measurable … S1 S2 rel sim_conds … Hmeas … Rsisi')
81[2: #H cases Hclass >H #ABS cases(ABS (refl …)) ]
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 ⊢ (??%?); % | // ]
86qed.
87
88lemma is_multiset_mem_neq_zero : ∀A : DeqSet.
89∀l : list A.∀x.mem … x l → mult … (list_to_multiset … l) x ≠ O.
90#A #l elim l [ #x *] #x #xs #IH #y *
91[ #EQ destruct % normalize >(\b (refl …)) normalize nodelta normalize #EQ destruct
92| #H normalize cases(?==?) normalize [ % #EQ destruct] @IH //
93]
94qed.
95
96lemma mem_neq_zero_is_multiset : ∀A : DeqSet.
97∀l: list A.∀x.mult … (list_to_multiset … l) x ≠ O → mem … x l.
98#A #l elim l [ #x * #H cases H % ]
99#x #xs #IH #y normalize inversion(y==x) normalize nodelta
100#H normalize [#_ % >(\P H) % ] #H1 %2 @IH assumption
101qed.
102
103lemma is_permutation_mem : ∀A :DeqSet.
104∀l1,l2 : list A.∀x : A.mem … x l1 →
105is_permutation A l1 l2 → mem … x l2.
106#A #l1 #l2 #x #Hmem normalize #H @mem_neq_zero_is_multiset <H @is_multiset_mem_neq_zero assumption
107qed.
108
109lemma mem_list : ∀A : Type[0].
110∀l : list A.∀x : A.mem … x l →
111∃l1,l2.l=l1 @ [x] @ l2.
112#A #l elim l
113[ #x *]
114#x #xs #IH #y *
115[ #EQ destruct %{[]} %{xs} %
116| #H cases(IH … H) #l1 * #l2 #EQ destruct
117  %{(x :: l1)} %{l2} %
118]
119qed.
120
121lemma is_permutation_case : ∀A : DeqSet.
122∀x : A.∀xs : list A.∀l : list A.is_permutation … (x::xs) l →
123∃l1,l2 : list A.is_permutation A xs (l1@l2) ∧ l = l1 @ [x] @ l2.
124#A #x #xs #l #H cases(mem_list … x (is_permutation_mem … H)) [2: %%]
125#l1 * #l2 #EQ destruct %{l1} %{l2} % //
126@(permute_equal_right … [x]) @permute_append_all
127@(is_permutation_transitive … H)
128/4 by is_permutation_append_left_cancellable, permute_append_l1, permute_append_all/
129qed.
130
131lemma action_on_permutation : ∀M : abstract_transition_sys.is_abelian (abs_instr M) →
132∀l1,l2 : list (abs_instr M).∀a.is_permutation … l1 l2 →
133(〚l1〛 a) = (〚l2〛 a).
134#M #Hab #l1 elim l1 -l1
135[ * // #x #xs #a #H lapply(H x) normalize >(\b (refl …)) normalize #EQ destruct]
136#x #xs #IH #l #a #H cases(is_permutation_case … H) #l1 * #l2 * #H1 #H2 destruct
137change with ([?]@?) in match (?::?); >big_op_associative >act_op >(IH … H1)
138<associative_append
139>big_op_associative in ⊢ (???%); >big_op_associative in ⊢ (???%); >(Hab … l1)
140>is_associative >act_op in ⊢ (???%); <big_op_associative in ⊢ (???%); %
141qed.
142
143definition applica : ∀A,B : Type[0].∀ l : list A.(∀a : A.mem … a l → B) → ∀a : A.mem … a l → B ≝
144λA,B,l,f,x,prf.f x prf.
145
146lemma proof_irrelevance_temp :  ∀A,B : Type[0].∀l : list A.
147∀f : (∀a : A.mem … a l → B).∀x.∀prf1,prf2.
148applica … f x prf1 = applica … f x prf2.
149//
150qed.
151
152lemma proof_irrelevance_all : ∀A,B : Type[0].∀l : list A.
153∀f : (∀a : A.mem … a l → B).∀x.∀prf1,prf2.
154f x prf1 = f x prf2.
155#A #B #l #f #x #prf1 #prf2 @proof_irrelevance_temp
156qed.
157
158lemma dependent_map_extensional : ∀A,B : Type[0].∀l : list A.
159∀f,g : (∀a.mem … a l → B).(∀a,prf1,prf2.f a prf1 = g a prf2) →
160dependent_map … l f = dependent_map … l g.
161#A #B #l elim l // #x #xs #IH #f #g #H whd in ⊢ (??%%);
162@eq_f2 // @IH //
163qed.
164
165lemma is_permutation_dependent_map : ∀A,B : DeqSet.∀l1,l2 : list A.
166∀f : (∀a : A.mem … a l1 → B).∀g : (∀a : A.mem … a l2 → B).
167∀perm : is_permutation A l1 l2.
168(∀a : A.
169 ∀prf : mem … a l1.f a prf = g a ?) →
170is_permutation B (dependent_map … l1 (λa,prf.f a prf)) (dependent_map … l2 (λa,prf.g a prf)).
171[2: @(is_permutation_mem … perm) //]
172#A #B #l1 elim l1 -l1
173[ * // #x #xs #f #g #H @⊥ lapply(H … x) normalize >(\b (refl …)) normalize #EQ destruct ]
174#x #xs #IH #l2 #f #g #H #H1 cases(is_permutation_case … H) #l3 * #l4 * #H2 #EQ destruct
175>dependent_map_append >dependent_map_append @permute_append_l1 >associative_append
176whd in match (dependent_map ????); whd in match (dependent_map ????) in ⊢ (???%);
177whd in match(append ???); >H1 generalize in ⊢ (??(??(??%)?)?);
178generalize in ⊢ (? → ???(??(??%)?));
179#prf1 #prf2
180>(proof_irrelevance_all … g x prf1 prf2)
181@is_permutation_cons whd in match (dependent_map ?? [ ] ?) in ⊢ (???%);
182whd in match (append ? [ ] ?) in ⊢ (???%); @permute_append_l1
183@(is_permutation_transitive …(IH … (l3@l4) …) )
184[2: assumption
185|3: #a #prf @(g a) cases(mem_append ???? prf) [ /3 by mem_append_l1/ | #H6 @mem_append_l2 @mem_append_l2 //]
186| @hide_prf #a #prf generalize in ⊢ (??(??%)?); #prf' >H1 //
187]
188>dependent_map_append @is_permutation_append
189[ >dependent_map_extensional [ @is_permutation_eq | // |]
190| >dependent_map_extensional [ @is_permutation_eq | // |]
191]
192qed.
193
194theorem final_cerco :
195(* for all programs in the imperative language (possibly with call non post labelled) *)
196∀p,p',prog.
197no_duplicates_labels … prog →
198
199(* let t_prog be the same program in which all calls are post-labelled *)
200let 〈t_prog,m,keep〉 ≝ trans_prog … prog in
201
202(* Let S1 be the operational semantics of the source code  *)
203let S1 ≝ operational_semantics p p' prog in
204
205(* Let S2 be the operational semantics of the soource code with call post labelled  *)
206let S2 ≝ operational_semantics p p' t_prog in
207
208(* for all assmbler programs *)
209∀p_asm,p_asm',prog_asm.
210(* Let S3 be the operational semantics of the compiled code  *)
211let S3 ≝ asm_operational_semantics p_asm p p_asm' prog_asm in
212
213(* If the simulation conditions between the source with call post-labelled and compiled
214    code holds (i.e. if the compiler is correct after the first pass) *)
215∀rel: relations … S2 S3. simulation_conditions … rel →
216
217(* let REL be semantical relation between the states of the source program and
218   the states of compiled code *)
219let REL ≝ λsi : S1.λsi' : S3.∃si'' : S2.∃abs_top,abs_tail.state_rel … m keep abs_top abs_tail si si'' ∧
220Srel … rel si'' si' in
221
222 (* Given an abstract interpretation framework for the compiled code *)
223∀R: asm_abstract_interpretation p_asm p_asm' … prog_asm.
224
225(* If the abstract instructions monoid is abelian *)
226is_abelian (abs_instr … (aabs_d … (asm_galois_conn … R))) → 
227 
228 (* If the static analysis does not fail *)
229∀mT,map1. ∀EQmap : static_analisys … (instr_map … R) mT prog_asm = return map1.
230
231 (* For every source trace whose measurable fragment starts in s1 and ends in s2 or,
232   equivalently, whose state after the initial labelled transition is s1
233   and whose state after the final labelled transition is s2  *)
234 ∀si,s1,s2,sn. ∀t: raw_trace … S1 … si sn.
235 measurable … s1 s2 … t →
236
237 (* For each target non I/O state si' in relation with the source state si *)
238 ∀si': S3. as_classify … si' ≠ cl_io → REL si si' →
239
240 (* There exists a corresponding target trace starting from si' *)
241 ∃sn'. ∃t': raw_trace … si' sn'.
242  REL sn sn' ∧
243 
244   (* Let labels be the costlabels observed in the trace of the source with all call post-labelled
245     (last one excluded), that can be computed from the costlabels observed in the trace of
246     the source language *)
247 let labels ≝ map_labels_on_trace … m … (chop … (get_costlabels_of_trace …  t)) in
248 
249  (*The labels emitted by the trace of the source with all call post-labelled
250    is a permutation of the labels emitted by the target trace (excluded the last one) *)
251  ∃perm:is_permutation … labels (chop … (get_costlabels_of_trace … t')).
252 
253 (* that has a measurable fragment starting in s1' and ending in s2' *)
254 ∃s1',s2'. measurable … s1' s2' … t' ∧
255
256(* Let abs_actions be the list of statically computed abstract actions
257   associated to each label in labels. *)
258 ∀abs_actions.
259  abs_actions =
260   dependent_map … labels (λlbl,prf.(opt_safe … (get_map … map1 lbl) …)) →
261
262 (* Given an abstract state in relation with the first state of the measurable
263    fragment *)
264 ∀a1.R s1' a1 →
265
266 (* The final state of the measurable fragment is in relation with the one
267   obtained by applying every semantics in abs_trace. *)
268 R s2' (〚abs_actions〛 a1).
269[2: @hide_prf normalize nodelta in prf; change with labels in prf : (???%);
270    lapply(is_permutation_mem … prf … perm) -prf #prf
271    cases(mem_map ????? (labels_of_trace_are_in_code … (chop_mem … prf))) *
272    #lbl' #pc * #Hmem #EQ destruct
273    >(proj1 … (static_analisys_ok … EQmap … Hmem))
274    @(proj2 … (static_analisys_ok … EQmap … Hmem))
275]
276#p #p' #prog #no_dup @pair_elim * #t_prog #m #keep #EQt_prog normalize nodelta
277#p_asm #p_asm' #prog_asm #rel #sim_cond #R #abelian #mT #map #EQmap #si #s1 #s2 #sn
278#t #meas_t #si' #Hclass * #si'' * #abs_top * #abs_tail * #Rsi_si'' #Rsi_si'
279lapply(correctness_theorem … p' prog no_dup) >EQt_prog normalize nodelta
280#H cases(H … meas_t … Rsi_si'') -H #abs_top' * #abs_tail' * #sn'' * #t'' ** #Rsn_sn''
281#Hperm * #s1'' * #s2'' #meas_t''
282cases(cerco … sim_cond … EQmap … meas_t'' … Rsi_si') //
283#sn' * #t' * #Rsn_sn' * #EQcost * #s1' * #s2' * #meas_t' normalize nodelta #Hcerco
284%{sn'} %{t'} %
285[ %{sn''} %{abs_top'} %{abs_tail'} /2 by conj/ ] %
286 [ @(is_permutation_transitive … Hperm) >EQcost // ]
287 %{s1'} %{s2'} %{meas_t'} #abs_actions #EQactions #a1 #Rs1_a1
288 >(action_on_permutation … abelian)
289 [@Hcerco [% | assumption]
290 | >EQactions -EQactions @is_permutation_dependent_map //
291 |
292 ]
293qed.
294
295(* TODO:
2961. Spostare chop e eliminare suffix.
2972. La block cost non fallisce in caso di I/O.
2983. Integrare la prima passata di Language nel risultato finale
2995. Cambi al control flow: Paolo's trick (label = coppia label-pezzo di stato)
3006. Rappresentabilita' di I, [[ ]] e stati astratti =⇒ instrumentazione
301*)
302
303(* TO SAY
3041) in una misurabile le silenti prima/dopo l'IO sono già automaticamente vuote (perchè una silente
305inizia/termina in un IO solo se vuota
3062) non chiediamo di non potere transire in una iniziale/da un finale perchè non ci serve; se uno lo
307aggiunge ha automaticamente che le silenti sono vuote come nel caso IO.
308*)
Note: See TracBrowser for help on using the repository browser.