source: src/joint/lineariseProof.ma @ 2476

Last change on this file since 2476 was 2476, checked in by piccolo, 7 years ago

fixed commutation lemmas in lineariseProof
started proof of main theorem in lineariseProof

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