source: src/joint/lineariseProof.ma @ 2481

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

corrected some inconsistencies
fixed some of lineariseProof

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