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 | |
---|
15 | include "joint/linearise.ma". |
---|
16 | include "common/StatusSimulation.ma". |
---|
17 | include "joint/Traces.ma". |
---|
18 | include "joint/semanticsUtils.ma". |
---|
19 | |
---|
20 | definition good_local_sigma : |
---|
21 | ∀p:unserialized_params. |
---|
22 | ∀p':(∀F.sem_unserialized_params p F). |
---|
23 | ∀globals. |
---|
24 | joint_closed_internal_function (mk_graph_params p) globals → |
---|
25 | (label → option ℕ) → Prop ≝ |
---|
26 | λp,p',globals,graph_fun,sigma. |
---|
27 | let lin_fun ≝ linearise_int_fun … graph_fun in |
---|
28 | let g ≝ joint_if_code ?? (pi1 … graph_fun) in |
---|
29 | let c ≝ joint_if_code ?? (pi1 … lin_fun) in |
---|
30 | ∀entry : (Σl.bool_to_Prop (code_has_label … g l)). |
---|
31 | code_closed … c ∧ |
---|
32 | sigma entry = Some ? 0 ∧ |
---|
33 | ∀l,n.sigma l = Some ? n → |
---|
34 | lt n 2^offset_size → |
---|
35 | ∃s. lookup … g l = Some ? s ∧ |
---|
36 | opt_Exists ? |
---|
37 | (λls.let 〈lopt, ts〉 ≝ ls in |
---|
38 | opt_All ? (eq ? l) lopt ∧ |
---|
39 | ts = graph_to_lin_statement … s ∧ |
---|
40 | opt_All ? |
---|
41 | (λnext.Or (sigma next = Some ? (S n)) |
---|
42 | (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉)) |
---|
43 | (stmt_implicit_label … s)) (nth_opt … n c). |
---|
44 | |
---|
45 | axiom prog_if_of_function : |
---|
46 | ∀p.∀prog : joint_program p. |
---|
47 | (Σi.is_internal_function_of_program … prog i) → |
---|
48 | joint_closed_internal_function p (prog_var_names … prog). |
---|
49 | |
---|
50 | definition if_in_global_env_to_if_in_prog : |
---|
51 | ∀prog_pars : prog_params.∀f : Σi.is_internal_function … (ev_genv prog_pars) i. |
---|
52 | Σi.is_internal_function_of_program ? (prog prog_pars) i ≝ |
---|
53 | λprog_pars,f.pi1 ?? f. |
---|
54 | @is_internal_function_of_program_ok @(pi2 … f) qed. |
---|
55 | |
---|
56 | coercion if_in_prog_from_if_in_global_env nocomposites : |
---|
57 | ∀prog_pars : prog_params.∀f : Σi.is_internal_function … (ev_genv prog_pars) i. |
---|
58 | Σi.is_internal_function_of_program ? (prog prog_pars) i ≝ |
---|
59 | if_in_global_env_to_if_in_prog |
---|
60 | on _f : Sig ident (λi.is_internal_function ??? i) |
---|
61 | to Sig ident (λi.is_internal_function_of_program ?? i). |
---|
62 | |
---|
63 | definition good_sigma : |
---|
64 | ∀p:unserialized_params. |
---|
65 | ∀p':(∀F.sem_unserialized_params p F). |
---|
66 | ∀prog : joint_program (mk_graph_params p). |
---|
67 | ((Σi.is_internal_function_of_program … prog i) → label → option ℕ) → Prop ≝ |
---|
68 | λp,p',graph_prog,sigma. |
---|
69 | ∀i. |
---|
70 | let graph_fun ≝ prog_if_of_function ?? i in |
---|
71 | let sigma_local ≝ sigma i in |
---|
72 | good_local_sigma ? p' ? graph_fun sigma_local. |
---|
73 | |
---|
74 | definition graph_prog_params ≝ |
---|
75 | λp,p',prog,stack_sizes. |
---|
76 | mk_prog_params (make_sem_graph_params p p') prog stack_sizes. |
---|
77 | |
---|
78 | definition graph_abstract_status: |
---|
79 | ∀p:unserialized_params. |
---|
80 | (∀F.sem_unserialized_params p F) → |
---|
81 | ∀prog : joint_program (mk_graph_params p). |
---|
82 | ((Σi.is_internal_function_of_program … prog i) → ℕ) → |
---|
83 | abstract_status |
---|
84 | ≝ |
---|
85 | λp,p',prog,stack_sizes. |
---|
86 | joint_abstract_status (graph_prog_params ? p' prog stack_sizes). |
---|
87 | |
---|
88 | definition lin_prog_params ≝ |
---|
89 | λp,p',prog,stack_sizes. |
---|
90 | mk_prog_params (make_sem_lin_params p p') prog stack_sizes. |
---|
91 | |
---|
92 | definition lin_abstract_status: |
---|
93 | ∀p:unserialized_params. |
---|
94 | (∀F.sem_unserialized_params p F) → |
---|
95 | ∀prog : joint_program (mk_lin_params p). |
---|
96 | ((Σi.is_internal_function_of_program … prog i) → ℕ) → |
---|
97 | abstract_status |
---|
98 | ≝ |
---|
99 | λp,p',prog,stack_sizes. |
---|
100 | joint_abstract_status (lin_prog_params ? p' prog stack_sizes). |
---|
101 | |
---|
102 | definition sigma_pc_opt: |
---|
103 | ∀p,p',graph_prog,stack_sizes. |
---|
104 | ((Σi.is_internal_function_of_program … graph_prog i) → |
---|
105 | code_point (mk_graph_params p) → option ℕ) → |
---|
106 | cpointer → option cpointer |
---|
107 | ≝ |
---|
108 | λp,p',prog,stack_sizes,sigma,pc. |
---|
109 | let pars ≝ graph_prog_params p p' prog stack_sizes in |
---|
110 | let ge ≝ ev_genv pars in |
---|
111 | ! f ← int_funct_of_block ?? ge (pblock pc) ; |
---|
112 | ! lin_point ← sigma f (point_of_pointer … pars pc) ; |
---|
113 | res_to_opt … (pointer_of_point ? (make_sem_lin_params ? p') pc lin_point). |
---|
114 | |
---|
115 | definition well_formed_pc: |
---|
116 | ∀p,p',graph_prog,stack_sizes. |
---|
117 | ((Σi.is_internal_function_of_program … graph_prog i) → |
---|
118 | label → option ℕ) → |
---|
119 | cpointer → Prop |
---|
120 | ≝ |
---|
121 | λp,p',prog,stack_sizes,sigma,pc. |
---|
122 | sigma_pc_opt p p' prog stack_sizes sigma pc |
---|
123 | ≠ None …. |
---|
124 | |
---|
125 | definition well_formed_status: |
---|
126 | ∀p,p',graph_prog,stack_sizes. |
---|
127 | ((Σi.is_internal_function_of_program … graph_prog i) → |
---|
128 | label → option ℕ) → |
---|
129 | state_pc (make_sem_graph_params p p') → Prop ≝ |
---|
130 | λp,p',prog,stack_sizes,sigma,st. |
---|
131 | well_formed_pc p p' prog stack_sizes sigma (pc … st) ∧ ?. |
---|
132 | cases daemon (* TODO *) |
---|
133 | qed. |
---|
134 | |
---|
135 | (* |
---|
136 | lemma prova : ∀p,s,st,prf.sigma_pc_of_status p s st prf = ?. |
---|
137 | [ #p #s #st #prf |
---|
138 | whd in match sigma_pc_of_status; normalize nodelta |
---|
139 | @opt_safe_elim |
---|
140 | #n |
---|
141 | lapply (refl … (int_funct_of_block (joint_closed_internal_function p) (globals p) |
---|
142 | (ev_genv p) (pblock (pc p st)))) |
---|
143 | elim (int_funct_of_block (joint_closed_internal_function p) (globals p) |
---|
144 | (ev_genv p) (pblock (pc p st))) in ⊢ (???%→%); |
---|
145 | [ #_ #ABS normalize in ABS; destruct(ABS) ] |
---|
146 | #f #EQ >m_return_bind |
---|
147 | *) |
---|
148 | |
---|
149 | |
---|
150 | (* |
---|
151 | lemma wf_status_to_wf_pc : |
---|
152 | ∀p,p',graph_prog,stack_sizes. |
---|
153 | ∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) → |
---|
154 | code_point (mk_graph_params p) → option ℕ). |
---|
155 | ∀st. |
---|
156 | well_formed_status p p' graph_prog stack_sizes sigma st → |
---|
157 | well_formed_pc p p' graph_prog stack_sizes sigma (pc ? st). |
---|
158 | #p #p' #graph_prog #stack_sizes #sigma #st whd in ⊢ (% → ?); * #H #_ @H |
---|
159 | qed. |
---|
160 | *) |
---|
161 | definition sigma_pc : |
---|
162 | ∀p,p',graph_prog,stack_sizes. |
---|
163 | ∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) → |
---|
164 | label → option ℕ). |
---|
165 | ∀pc. |
---|
166 | ∀prf : well_formed_pc p p' graph_prog stack_sizes sigma pc. |
---|
167 | cpointer ≝ |
---|
168 | λp,p',graph_prog,stack_sizes,sigma,st.opt_safe …. |
---|
169 | |
---|
170 | lemma sigma_pc_of_status_ok: |
---|
171 | ∀p,p',graph_prog,stack_sizes. |
---|
172 | ∀sigma. |
---|
173 | ∀pc. |
---|
174 | ∀prf:well_formed_pc p p' graph_prog stack_sizes sigma pc. |
---|
175 | sigma_pc_opt p p' graph_prog stack_sizes sigma pc = |
---|
176 | Some … (sigma_pc p p' graph_prog stack_sizes sigma pc prf). |
---|
177 | #p #p' #graph_prog #stack_sizes #sigma #st #prf @opt_to_opt_safe qed. |
---|
178 | |
---|
179 | |
---|
180 | definition sigma_state : |
---|
181 | ∀p. |
---|
182 | ∀p':∀F.sem_unserialized_params p F. |
---|
183 | ∀graph_prog,stack_sizes. |
---|
184 | ∀sigma. |
---|
185 | (* let lin_prog ≝ linearise ? graph_prog in *) |
---|
186 | ∀s:state_pc (p' ?). (* = graph_abstract_status p p' graph_prog stack_sizes *) |
---|
187 | well_formed_status p p' graph_prog stack_sizes sigma s → |
---|
188 | state_pc (make_sem_lin_params p p') (* = lin_abstract_status p p' lin_prog ? *) |
---|
189 | ≝ |
---|
190 | λp,p',graph_prog,stack_sizes,sigma,s,prf. |
---|
191 | let pc' ≝ sigma_pc … (proj1 … prf) in |
---|
192 | mk_state_pc ? ? pc'. |
---|
193 | cases daemon (* TODO *) qed. |
---|
194 | |
---|
195 | lemma sigma_pc_commute: |
---|
196 | ∀p,p',graph_prog,stack_sizes,sigma,st. |
---|
197 | ∀prf : well_formed_status p p' graph_prog stack_sizes sigma st. |
---|
198 | sigma_pc … (pc ? st) (proj1 … prf) = |
---|
199 | pc ? (sigma_state … st prf). |
---|
200 | #p #p' #prog #stack_sizes #sigma #st #prf % |
---|
201 | qed. |
---|
202 | |
---|
203 | lemma res_eq_from_opt : |
---|
204 | ∀A,m,v.res_to_opt A m = return v → m = return v. |
---|
205 | #A * #x #v normalize #EQ destruct % qed. |
---|
206 | |
---|
207 | lemma if_propagate : |
---|
208 | ∀pars_in, pars_out : sem_params. |
---|
209 | ∀trans : ∀globals.joint_closed_internal_function pars_in globals → |
---|
210 | joint_closed_internal_function pars_out globals. |
---|
211 | ∀prog_in : program (joint_function pars_in) ℕ. |
---|
212 | let prog_out ≝ |
---|
213 | transform_program … prog_in (λglobals.transf_fundef ?? (trans globals)) in |
---|
214 | ∀i.is_internal_function_of_program … prog_in i → |
---|
215 | is_internal_function_of_program … prog_out i. |
---|
216 | cases daemon (* TODO by paolo *) qed. |
---|
217 | |
---|
218 | definition stack_sizes_lift : |
---|
219 | ∀pars_in, pars_out : sem_params. |
---|
220 | ∀trans : ∀globals.joint_closed_internal_function pars_in globals → |
---|
221 | joint_closed_internal_function pars_out globals. |
---|
222 | ∀prog_in : program (joint_function pars_in) ℕ. |
---|
223 | let prog_out ≝ |
---|
224 | transform_program … prog_in (λglobals.transf_fundef ?? (trans globals)) in |
---|
225 | ((Σi.is_internal_function_of_program … prog_out i) → ℕ) → |
---|
226 | ((Σi.is_internal_function_of_program … prog_in i) → ℕ) ≝ |
---|
227 | λpars_in,pars_out,prog_in,trans,stack_sizes. |
---|
228 | λi.stack_sizes «i, if_propagate … (pi2 … i)». |
---|
229 | |
---|
230 | axiom ok_is_internal_function_of_program : |
---|
231 | ∀p.∀prog:joint_program p.∀i. |
---|
232 | is_internal_function_of_program p prog i → |
---|
233 | is_internal_function ?? (globalenv_noinit ? prog) i. |
---|
234 | |
---|
235 | |
---|
236 | definition sigma_function_name : |
---|
237 | ∀p,p',graph_prog. |
---|
238 | let lin_prog ≝ linearise p graph_prog in |
---|
239 | ∀lin_stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. |
---|
240 | let graph_stack_sizes ≝ |
---|
241 | stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') |
---|
242 | ? graph_prog lin_stack_sizes in |
---|
243 | (Σf.is_internal_function … (ev_genv (graph_prog_params p p' graph_prog graph_stack_sizes)) f) → |
---|
244 | (Σf.is_internal_function … (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) f) ≝ |
---|
245 | λp,p',graph_prog,lin_stack_sizes,f.pi1 … f. |
---|
246 | @ok_is_internal_function_of_program |
---|
247 | @(if_propagate (make_sem_graph_params p p') (make_sem_lin_params p p')) |
---|
248 | @is_internal_function_of_program_ok |
---|
249 | @(pi2 … f) |
---|
250 | qed. |
---|
251 | |
---|
252 | |
---|
253 | lemma if_of_function_commute: |
---|
254 | ∀p,p',graph_prog,stack_sizes. |
---|
255 | ∀graph_fun. |
---|
256 | let graph_fd ≝ if_of_function ??? graph_fun in |
---|
257 | let lin_fun ≝ sigma_function_name p p' graph_prog stack_sizes graph_fun in |
---|
258 | let lin_fd ≝ if_of_function … lin_fun in |
---|
259 | lin_fd = linearise_int_fun … graph_fd. |
---|
260 | (* usare match_opt_prf_elim ? *) |
---|
261 | cases daemon qed. |
---|
262 | |
---|
263 | lemma bind_opt_inversion: |
---|
264 | ∀A,B: Type[0]. ∀f: option A. ∀g: A → option B. ∀y: B. |
---|
265 | (! x ← f ; g x = Some … y) → |
---|
266 | ∃x. (f = Some … x) ∧ (g x = Some … y). |
---|
267 | #A #B #f #g #y cases f normalize |
---|
268 | [ #H destruct (H) |
---|
269 | | #a #e %{a} /2 by conj/ |
---|
270 | ] qed. |
---|
271 | |
---|
272 | lemma sigma_pblock_eq_lemma : |
---|
273 | ∀p,p',graph_prog. |
---|
274 | let lin_prog ≝ linearise p graph_prog in |
---|
275 | ∀lin_stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. |
---|
276 | let graph_stack_sizes ≝ |
---|
277 | stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') |
---|
278 | ? graph_prog lin_stack_sizes in |
---|
279 | ∀sigma,st. |
---|
280 | ∀prf : well_formed_status p p' graph_prog graph_stack_sizes sigma st. |
---|
281 | pblock (sigma_pc ? p' graph_prog graph_stack_sizes sigma (pc ? st) (proj1 … prf)) = |
---|
282 | pblock (pc ? st). |
---|
283 | #p #p' #graph_prog #stack_sizes #sigma #st #prf |
---|
284 | whd in match sigma_pc; normalize nodelta |
---|
285 | @opt_safe_elim #x #x_spec |
---|
286 | whd in x_spec:(??%?); cases (int_funct_of_block ????) in x_spec; |
---|
287 | normalize nodelta [#abs destruct] #id #H cases (bind_opt_inversion ????? H) -H |
---|
288 | #offset * #_ whd in ⊢ (??%? → ?); whd in match pointer_of_point; normalize nodelta |
---|
289 | cases (opt_to_res ???) [2: #msg #abs normalize in abs; destruct] |
---|
290 | #offset_lin whd in ⊢ (??%? → ?); #EQ destruct // |
---|
291 | qed. |
---|
292 | |
---|
293 | lemma fetch_function_sigma_commute : |
---|
294 | ∀p,p',graph_prog. |
---|
295 | let lin_prog ≝ linearise p graph_prog in |
---|
296 | ∀lin_stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. |
---|
297 | let graph_stack_sizes ≝ |
---|
298 | stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') |
---|
299 | ? graph_prog lin_stack_sizes in |
---|
300 | ∀sigma,st,f. |
---|
301 | ∀prf : well_formed_status p p' graph_prog graph_stack_sizes sigma st. |
---|
302 | let pc_st ≝ pc ? st in |
---|
303 | fetch_function … (ev_genv (graph_prog_params p p' graph_prog graph_stack_sizes)) pc_st = |
---|
304 | return f |
---|
305 | → fetch_function … (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) (sigma_pc … pc_st (proj1 … prf)) = |
---|
306 | return sigma_function_name … f. |
---|
307 | #p #p' #graph_prog #stack_sizes #sigma #st #f #prf |
---|
308 | >(sigma_pc_commute … prf) |
---|
309 | whd in match fetch_function; normalize nodelta |
---|
310 | >(sigma_pblock_eq_lemma … prf) #H |
---|
311 | lapply (opt_eq_from_res ???? H) -H |
---|
312 | whd in match int_funct_of_block in ⊢ (%→?); normalize nodelta |
---|
313 | |
---|
314 | XXXX ENTRARE IN PRF CHE C'E' FUNCT OF BLOCK XXXX |
---|
315 | |
---|
316 | #H elim (bind_opt_inversion ????? H) -H |
---|
317 | #x * whd in match funct_of_block in ⊢ (%→?); normalize nodelta |
---|
318 | @match_opt_prf_elim |
---|
319 | #H #H1 whd in H : (??%?); |
---|
320 | cases ( find_funct_ptr |
---|
321 | (fundef |
---|
322 | (joint_closed_internal_function |
---|
323 | (graph_prog_params p p' graph_prog |
---|
324 | (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') |
---|
325 | (linearise_int_fun p) graph_prog stack_sizes)) |
---|
326 | (globals |
---|
327 | (graph_prog_params p p' graph_prog |
---|
328 | (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') |
---|
329 | (linearise_int_fun p) graph_prog stack_sizes))))) |
---|
330 | (ev_genv |
---|
331 | (graph_prog_params p p' graph_prog |
---|
332 | (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') |
---|
333 | (linearise_int_fun p) graph_prog stack_sizes))) |
---|
334 | (pblock (pc (make_sem_graph_params p p') st))) in H; [ 2: normalize #abs destruct |
---|
335 | |
---|
336 | |
---|
337 | normalize nodelta |
---|
338 | #H #H1 |
---|
339 | cases ( find_funct_ptr |
---|
340 | (fundef |
---|
341 | (joint_closed_internal_function |
---|
342 | (graph_prog_params p p' graph_prog |
---|
343 | (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') |
---|
344 | (linearise_int_fun p) graph_prog stack_sizes)) |
---|
345 | (globals |
---|
346 | (graph_prog_params p p' graph_prog |
---|
347 | (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') |
---|
348 | (linearise_int_fun p) graph_prog stack_sizes))))) |
---|
349 | (ev_genv |
---|
350 | (graph_prog_params p p' graph_prog |
---|
351 | (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') |
---|
352 | (linearise_int_fun p) graph_prog stack_sizes))) |
---|
353 | (pblock (pc (make_sem_graph_params p p') st))) in H; |
---|
354 | |
---|
355 | |
---|
356 | check find_funct_ptr_transf |
---|
357 | whd in match int_funct_of_block; normalize nodelta |
---|
358 | #H elim (bind_inversion ????? H) |
---|
359 | |
---|
360 | .. sigma_int_funct_of_block |
---|
361 | |
---|
362 | |
---|
363 | |
---|
364 | whd in match int_funct_of_block; normalize nodelta |
---|
365 | elim (bind_inversion ????? H) |
---|
366 | whd in match int_funct_of_block; normalize nodelta |
---|
367 | #H elim (bind_inversion ????? H) -H #fn * |
---|
368 | #H lapply (opt_eq_from_res ???? H) -H |
---|
369 | #H >(find_funct_ptr_transf … (λglobals.transf_fundef … (linearise_int_fun … globals)) … H) |
---|
370 | -H #H >m_return_bind cases fn in H; normalize nodelta #arg #EQ whd in EQ:(??%%); |
---|
371 | destruct // *) |
---|
372 | cases daemon |
---|
373 | qed. |
---|
374 | |
---|
375 | lemma stmt_at_sigma_commute: |
---|
376 | ∀p,p',graph_prog,stack_sizes,graph_fun,lbl. |
---|
377 | let lin_prog ≝ linearise ? graph_prog in |
---|
378 | let lin_fun ≝ sigma_function_name p p' graph_prog stack_sizes graph_fun in |
---|
379 | ∀sigma.good_sigma p p' graph_prog sigma → |
---|
380 | ∀prf:sigma graph_fun lbl ≠ None …. |
---|
381 | ∃stmt. |
---|
382 | stmt_at … |
---|
383 | (joint_if_code ?? (if_of_function ??? graph_fun)) |
---|
384 | lbl = Some ? stmt ∧ |
---|
385 | stmt_at … |
---|
386 | (joint_if_code ?? (if_of_function ??? lin_fun)) |
---|
387 | (opt_safe … (sigma graph_fun lbl) prf) = Some ? (graph_to_lin_statement … stmt). |
---|
388 | #p #p' #graph_prog #stack_sizes #graph_fun #lbl #sigma #good #prf |
---|
389 | @opt_safe_elim -prf #n #prf |
---|
390 | (* |
---|
391 | whd in match (stmt_at ????); |
---|
392 | whd in match (stmt_at ????); |
---|
393 | cases (linearise_code_spec … p' graph_prog graph_fun |
---|
394 | (joint_if_entry … graph_fun)) |
---|
395 | * #lin_code_closed #sigma_entry_is_zero #sigma_spec |
---|
396 | lapply (sigma_spec |
---|
397 | (point_of_pointer ? (graph_prog_params … p' graph_prog) (pc … s1))) |
---|
398 | -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @(sigma_pc_of_status_ok … prf) |2: skip ] |
---|
399 | -sigma_spec #graph_stmt * #graph_lookup_ok >graph_lookup_ok -graph_lookup_ok |
---|
400 | whd in ⊢ (? → ???%); #sigma_spec whd in sigma_spec; |
---|
401 | inversion (nth_opt ???) in sigma_spec; [ #H whd in ⊢ (% → ?); #abs cases abs ] |
---|
402 | * #optlabel #lin_stm #lin_lookup_ok whd in ⊢ (% → ?); ** #_ |
---|
403 | #related_lin_stm_graph_stm #_ <related_lin_stm_graph_stm -related_lin_stm_graph_stm |
---|
404 | <sigma_pc_commute >lin_lookup_ok // *) |
---|
405 | cases daemon |
---|
406 | qed. |
---|
407 | |
---|
408 | lemma fetch_statement_sigma_commute: |
---|
409 | ∀p,p',graph_prog,lin_stack_sizes,pc,fn,stmt. |
---|
410 | let lin_prog ≝ linearise ? graph_prog in |
---|
411 | let graph_stack_sizes ≝ |
---|
412 | stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') |
---|
413 | ? graph_prog lin_stack_sizes in |
---|
414 | ∀sigma.good_sigma p p' graph_prog sigma → |
---|
415 | ∀prf : well_formed_pc p p' graph_prog graph_stack_sizes sigma pc. |
---|
416 | fetch_statement ? (make_sem_graph_params p p') … (ev_genv (graph_prog_params p p' graph_prog graph_stack_sizes)) pc = |
---|
417 | return 〈fn,stmt〉 → |
---|
418 | fetch_statement ? (make_sem_lin_params p p') … (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) |
---|
419 | (sigma_pc … pc prf) = |
---|
420 | return 〈sigma_function_name … fn, graph_to_lin_statement … stmt〉. |
---|
421 | #p #p' #graph_prog #stack_sizes #pc #fn #stmt #good #prf |
---|
422 | (* @opt_safe_elim -prf #n #prf |
---|
423 | whd in match fetch_statement; normalize nodelta |
---|
424 | >fetch_function_sigma_commute |
---|
425 | cases (fetch_function ????) [2://] |
---|
426 | #graph_fun whd in ⊢ (??%%); |
---|
427 | whd in ⊢ (???(match % with [ _ ⇒ ? | _ ⇒ ?])); |
---|
428 | >stm_at_sigma_commute cases (stmt_at ????) // *) |
---|
429 | cases daemon |
---|
430 | qed. |
---|
431 | |
---|
432 | definition linearise_status_rel: |
---|
433 | ∀p,p',graph_prog. |
---|
434 | let lin_prog ≝ linearise p graph_prog in |
---|
435 | ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. |
---|
436 | let stack_sizes' ≝ |
---|
437 | stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') |
---|
438 | ? graph_prog stack_sizes in |
---|
439 | ∀sigma. |
---|
440 | good_sigma p p' graph_prog sigma → |
---|
441 | status_rel |
---|
442 | (graph_abstract_status p p' graph_prog stack_sizes') |
---|
443 | (lin_abstract_status p p' lin_prog stack_sizes) |
---|
444 | ≝ λp,p',graph_prog,stack_sizes,sigma,good. |
---|
445 | let stack_sizes' ≝ |
---|
446 | stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') |
---|
447 | ? graph_prog ? in |
---|
448 | mk_status_rel … |
---|
449 | (* sem_rel ≝ *) (λs1,s2. |
---|
450 | ∃prf: well_formed_status p p' graph_prog stack_sizes' sigma s1. |
---|
451 | s2 = sigma_state … s1 prf) |
---|
452 | (* call_rel ≝ *) (λs1,s2. |
---|
453 | ∃prf:well_formed_status p p' graph_prog stack_sizes' sigma s1. |
---|
454 | pc ? s2 = sigma_pc … (pc ? s1) (proj1 … prf)) |
---|
455 | (* sim_final ≝ *) ?. |
---|
456 | #st1 #st2 * #prf #EQ2 |
---|
457 | % |
---|
458 | whd in ⊢ (%→%); |
---|
459 | #H lapply (opt_to_opt_safe … H) |
---|
460 | @opt_safe_elim -H |
---|
461 | #res #_ |
---|
462 | #H lapply (res_eq_from_opt ??? H) -H |
---|
463 | #H elim (bind_inversion ????? H) |
---|
464 | * #f #stmt * |
---|
465 | whd in ⊢ (??%?→?); |
---|
466 | cases daemon |
---|
467 | qed. |
---|
468 | |
---|
469 | (* To be added to common/Globalenvs, it strenghtens |
---|
470 | find_funct_ptr_transf *) |
---|
471 | (* |
---|
472 | lemma |
---|
473 | find_funct_ptr_transf_eq: |
---|
474 | ∀A,B,V,iV. ∀p: program A V. ∀transf: (∀vs. A vs → B vs). |
---|
475 | ∀b: block. |
---|
476 | find_funct_ptr ? (globalenv … iV (transform_program … p transf)) b = |
---|
477 | m_map ??? |
---|
478 | (transf …) |
---|
479 | (find_funct_ptr ? (globalenv … iV p) b). |
---|
480 | #A #B #V #iV #p #transf #b inversion (find_funct_ptr ???) in ⊢ (???%); |
---|
481 | [ cases daemon (* TODO in Globalenvs.ma *) |
---|
482 | | #f #H >(find_funct_ptr_transf A B … H) // ] |
---|
483 | qed. |
---|
484 | *) |
---|
485 | |
---|
486 | |
---|
487 | (*lemma fetch_function_sigma_commute: |
---|
488 | ∀p,p',graph_prog,sigma,st1. |
---|
489 | ∀prf:well_formed_status ??? sigma st1. |
---|
490 | let lin_prog ≝ linearise ? graph_prog in |
---|
491 | fetch_function |
---|
492 | (lin_prog_params p p' lin_prog) |
---|
493 | (globals (lin_prog_params p p' lin_prog)) |
---|
494 | (ev_genv (lin_prog_params p p' lin_prog)) |
---|
495 | (pc (lin_prog_params p p' lin_prog) |
---|
496 | (linearise_status_fun p p' graph_prog sigma st1 prf)) |
---|
497 | = |
---|
498 | m_map … |
---|
499 | (linearise_int_fun ??) |
---|
500 | (fetch_function |
---|
501 | (graph_prog_params p p' graph_prog) |
---|
502 | (globals (graph_prog_params p p' graph_prog)) |
---|
503 | (ev_genv (graph_prog_params p p' graph_prog)) |
---|
504 | (pc (graph_prog_params p p' graph_prog) st1)). |
---|
505 | #p #p' #prog #sigma #st #prf whd in match fetch_function; normalize nodelta |
---|
506 | whd in match function_of_block; normalize nodelta |
---|
507 | >(find_funct_ptr_transf_eq … (λglobals.transf_fundef … (linearise_int_fun … globals)) …) |
---|
508 | cases (find_funct_ptr ???) // * // |
---|
509 | qed. |
---|
510 | *) |
---|
511 | |
---|
512 | inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝ |
---|
513 | ex1_intro: ∀ x:A. P x → ex_Type1 A P. |
---|
514 | interpretation "exists in Type[1]" 'exists x = (ex_Type1 ? x). |
---|
515 | |
---|
516 | lemma linearise_ok: |
---|
517 | ∀p,p',graph_prog. |
---|
518 | let lin_prog ≝ linearise ? graph_prog in |
---|
519 | ∀lin_stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. |
---|
520 | let graph_stack_sizes ≝ |
---|
521 | stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') |
---|
522 | ? graph_prog lin_stack_sizes in |
---|
523 | ∃R. |
---|
524 | status_simulation |
---|
525 | (graph_abstract_status p p' graph_prog graph_stack_sizes) |
---|
526 | (lin_abstract_status p p' lin_prog lin_stack_sizes) R. |
---|
527 | #p #p' #graph_prog |
---|
528 | cut (∃sigma.good_sigma p p' graph_prog sigma) |
---|
529 | [ cases daemon (* TODO by Paolo *) ] * #sigma #good |
---|
530 | #lin_stack_sizes |
---|
531 | %{(linearise_status_rel p p' graph_prog lin_stack_sizes sigma good)} |
---|
532 | whd |
---|
533 | #st1 #cl #st1' #st2 #move_st1_st1' #rel_st1_st2 #classified_st1_cl |
---|
534 | cases cl in classified_st1_cl; -cl #classified_st1_cl whd |
---|
535 | [4: |
---|
536 | cases rel_st1_st2 -rel_st1_st2 #wf_st1 #rel_st1_st2 >rel_st1_st2 -st2 |
---|
537 | whd in move_st1_st1'; |
---|
538 | letin lin_prog ≝ (linearise ? graph_prog) |
---|
539 | |
---|
540 | cut (joint_closed_internal_function (mk_graph_params p) (globals (graph_prog_params p p' graph_prog))) [cases daemon (*???*)] #graph_fun |
---|
541 | |
---|
542 | cases (linearise_code_spec … p' graph_prog graph_fun |
---|
543 | (joint_if_entry … graph_fun)) |
---|
544 | * #lin_code_closed #sigma_entry_is_zero #sigma_spec |
---|
545 | lapply (sigma_spec |
---|
546 | (point_of_pointer ? (graph_prog_params … p' graph_prog) (pc … st1))) |
---|
547 | -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @(sigma_pc_of_status_ok … wf_st1) |2: skip ] |
---|
548 | -sigma_spec #graph_stmt * #graph_lookup_ok #sigma_spec whd in sigma_spec; |
---|
549 | inversion (nth_opt ???) in sigma_spec; [ #H whd in ⊢ (% → ?); #abs cases abs ] |
---|
550 | * #optlabel #lin_stm #lin_lookup_ok whd in ⊢ (% → ?); ** #labels_preserved |
---|
551 | #related_lin_stm_graph_stm |
---|
552 | inversion (stmt_implicit_label ???) |
---|
553 | [ whd in match (opt_All ???); #stmt_implicit_spec #_ |
---|
554 | letin st2_opt' ≝ (eval_state (globals (lin_prog_params p p' lin_prog)) … |
---|
555 | (ev_genv (lin_prog_params p p' lin_prog)) |
---|
556 | (linearise_status_fun … sigma st1 wf_st1)) |
---|
557 | check st2_opt' |
---|
558 | cut (∃st2': lin_abstract_status p p' lin_prog. st2_opt' = return st2') |
---|
559 | [cases daemon (* TODO, needs lemma? *)] * #st2' #st2_spec' |
---|
560 | normalize nodelta in st2_spec'; -st2_opt' |
---|
561 | %{st2'} %{(taaf_step … (taa_base …) …)} |
---|
562 | [ cases daemon (* TODO, together with the previous one? *) |
---|
563 | | @st2_spec' ] |
---|
564 | %[%] [%] |
---|
565 | [ whd |
---|
566 | whd in st2_spec':(??%?); >fetch_statement_sigma_commute in st2_spec'; |
---|
567 | whd in move_st1_st1':(??%?); |
---|
568 | cut (fetch_statement (graph_prog_params p p' graph_prog) (graph_prog_params … graph_prog) … (ev_genv (graph_prog_params … graph_prog)) … (pc … st1) = OK ? 〈graph_fun,graph_stmt〉) |
---|
569 | [ cases daemon (* TODO once and for all, consequence of graph_lookup_ok *) ] |
---|
570 | #fetch_statement_ok >fetch_statement_ok in move_st1_st1'; |
---|
571 | whd in ⊢ (??%? → ??%? → ?); normalize nodelta |
---|
572 | inversion graph_stmt in stmt_implicit_spec; normalize nodelta |
---|
573 | [ #stmt #lbl #_ #abs @⊥ normalize in abs; destruct(abs) ] |
---|
574 | XXXXXXXXXX siamo qua, caso GOTO e RETURN |
---|
575 | | cases daemon (* TODO, after the definition of label_rel, trivial *) ] |
---|
576 | ] |
---|
577 | | .... |
---|
578 | qed. |
---|