source: LTS/Final.ma @ 3540

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

closed some daemons

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