source: LTS/Final.ma @ 3535

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

final statement of cerco with the first pass integrated in place

File size: 9.8 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_permutation_mem : ∀A :DeqSet.
88∀l1,l2 : list A.∀x : A.mem … x l1 →
89is_permutation A l1 l2 → mem … x l2.
90cases daemon
91qed.
92
93definition is_abelian ≝ λM : monoid.
94∀x,y : M.op … M x y = op … M y x.
95
96lemma action_on_permutation : ∀M : abstract_transition_sys.is_abelian (abs_instr M) →
97∀l1,l2 : list (abs_instr M).∀a.is_permutation … l1 l2 →
98(〚l1〛 a) = (〚l2〛 a).
99cases daemon
100qed.
101
102lemma is_permutation_dependent_map : ∀A,B : DeqSet.∀l1,l2 : list A.
103∀f : (∀a : A.mem … a l1 → B).∀g : (∀a : A.mem … a l2 → B).
104∀perm : is_permutation A l1 l2.
105(∀a : A.
106 ∀prf : mem … a l1.f a prf = g a ?) →
107is_permutation B (dependent_map … l1 f) (dependent_map … l2 g).
108[2: @(is_permutation_mem … perm) //]
109cases daemon
110qed.
111
112theorem final_cerco :
113(* for all programs in the imperative language (possibly with call non post labelled) *)
114∀p,p',prog.
115no_duplicates_labels … prog →
116
117(* let t_prog be the same program in which all calls are post-labelled *)
118let 〈t_prog,m,keep〉 ≝ trans_prog … prog in
119
120(* Let S1 be the operational semantics of the source code  *)
121let S1 ≝ operational_semantics p p' prog in
122
123(* Let S2 be the operational semantics of the soource code with call post labelled  *)
124let S2 ≝ operational_semantics p p' t_prog in
125
126(* for all assmbler programs *)
127∀p_asm,p_asm',prog_asm.
128(* Let S3 be the operational semantics of the compiled code  *)
129let S3 ≝ asm_operational_semantics p_asm p_asm' prog_asm in
130
131(* If the simulation conditions between the source with call post-labelled and compiled
132    code holds (i.e. if the compiler is correct after the first pass) *)
133∀rel: relations S2 S3. simulation_conditions … rel →
134
135(* let REL be semantical relation between the states of the source program and
136   the states of compiled code *)
137let REL ≝ λsi : S1.λsi' : S3.∃si'' : S2.∃abs_top,abs_tail.state_rel … m keep abs_top abs_tail si si'' ∧
138Srel … rel si'' si' in
139
140 (* Given an abstract interpretation framework for the compiled code *)
141∀R: asm_abstract_interpretation p_asm p_asm' prog_asm.
142
143(* If the abstract instructions monoid is abelian *)
144is_abelian (abs_instr … (aabs_d … (asm_galois_conn … R))) → 
145 
146 (* If the static analysis does not fail *)
147∀mT,map1. ∀EQmap : static_analisys … (instr_map … R) mT prog_asm = return map1.
148
149 (* For every source trace whose measurable fragment starts in s1 and ends in s2 or,
150   equivalently, whose state after the initial labelled transition is s1
151   and whose state after the final labelled transition is s2  *)
152 ∀si,s1,s2,sn. ∀t: raw_trace S1 … si sn.
153 measurable … s1 s2 … t →
154
155 (* For each target non I/O state si' in relation with the source state si *)
156 ∀si': S3. as_classify … si' ≠ cl_io → REL si si' →
157
158 (* There exists a corresponding target trace starting from si' *)
159 ∃sn'. ∃t': raw_trace … si' sn'.
160  REL sn sn' ∧
161 
162   (* Let labels be the costlabels observed in the trace of the source with all call post-labelled
163     (last one excluded), that can be computed from the costlabels observed in the trace of
164     the source language *)
165 let labels ≝ map_labels_on_trace … m … (chop … (get_costlabels_of_trace …  t)) in
166 
167  (*The labels emitted by the trace of the source with all call post-labelled
168    is a permutation of the labels emitted by the target trace (excluded the last one) *)
169  ∃perm:is_permutation … labels (chop … (get_costlabels_of_trace … t')).
170 
171 (* that has a measurable fragment starting in s1' and ending in s2' *)
172 ∃s1',s2'. measurable … s1' s2' … t' ∧
173
174(* Let abs_actions be the list of statically computed abstract actions
175   associated to each label in labels. *)
176 ∀abs_actions.
177  abs_actions =
178   dependent_map … labels (λlbl,prf.(opt_safe … (get_map … map1 lbl) …)) →
179
180 (* Given an abstract state in relation with the first state of the measurable
181    fragment *)
182 ∀a1.R s1' a1 →
183
184 (* The final state of the measurable fragment is in relation with the one
185   obtained by applying every semantics in abs_trace. *)
186 R s2' (〚abs_actions〛 a1).
187[2: @hide_prf normalize nodelta in prf; change with labels in prf : (???%);
188    lapply(is_permutation_mem … prf … perm) -prf #prf
189    cases(mem_map ????? (labels_of_trace_are_in_code … (chop_mem … prf))) *
190    #lbl' #pc * #Hmem #EQ destruct
191    >(proj1 … (static_analisys_ok … EQmap … Hmem))
192    @(proj2 … (static_analisys_ok … EQmap … Hmem))
193]
194#p #p' #prog #no_dup @pair_elim * #t_prog #m #keep #EQt_prog normalize nodelta
195#p_asm #p_asm' #prog_asm #rel #sim_cond #R #abelian #mT #map #EQmap #si #s1 #s2 #sn
196#t #meas_t #si' #Hclass * #si'' * #abs_top * #abs_tail * #Rsi_si'' #Rsi_si'
197lapply(correctness_theorem … p' prog no_dup) >EQt_prog normalize nodelta
198#H cases(H … meas_t … Rsi_si'') -H #abs_top' * #abs_tail' * #sn'' * #t'' ** #Rsn_sn''
199#Hperm * #s1'' * #s2'' #meas_t''
200cases(cerco … sim_cond … EQmap … meas_t'' … Rsi_si') //
201#sn' * #t' * #Rsn_sn' * #EQcost * #s1' * #s2' * #meas_t' normalize nodelta #Hcerco
202%{sn'} %{t'} %
203[ %{sn''} %{abs_top'} %{abs_tail'} /2 by conj/ ] %
204 [ @(is_permutation_transitive … Hperm) >EQcost // ]
205 %{s1'} %{s2'} %{meas_t'} #abs_actions #EQactions #a1 #Rs1_a1
206 >(action_on_permutation … abelian)
207 [@Hcerco [% | assumption]
208 | >EQactions -EQactions @is_permutation_dependent_map //
209 |
210 ]
211qed.
212
213(* TODO:
2141. Spostare chop e eliminare suffix.
2152. La block cost non fallisce in caso di I/O.
2163. Integrare la prima passata di Language nel risultato finale
2175. Cambi al control flow: Paolo's trick (label = coppia label-pezzo di stato)
2186. Rappresentabilita' di I, [[ ]] e stati astratti =⇒ instrumentazione
219*)
220
221(* TO SAY
2221) in una misurabile le silenti prima/dopo l'IO sono già automaticamente vuote (perchè una silente
223inizia/termina in un IO solo se vuota
2242) non chiediamo di non potere transire in una iniziale/da un finale perchè non ci serve; se uno lo
225aggiunge ha automaticamente che le silenti sono vuote come nel caso IO.
226*)
Note: See TracBrowser for help on using the repository browser.