source: src/joint/lineariseProof.ma @ 2484

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

fixed Traces and semantics
added commutation record (not yet finished) and proofs in lineariseProof

File size: 41.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 "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 sigma_beval_opt :
123 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
124  ((Σi.is_internal_function_of_program … graph_prog i) →
125    code_point (mk_graph_params p) → option ℕ) →
126  beval → option beval ≝
127λp,p',graph_prog,sigma,bv.
128match bv with
129[ BVpc pc prt ⇒ ! pc' ← sigma_pc_opt p p' graph_prog sigma pc ; return BVpc pc' prt
130| _ ⇒ return bv
131].
132
133definition sigma_beval :
134 ∀p,p',graph_prog,sigma,bv.
135 sigma_beval_opt p p' graph_prog sigma bv ≠ None ? → beval ≝
136 λp,p',graph_prog,sigma,bv.opt_safe ….
137
138(*
139lemma prova : ∀p,s,st,prf.sigma_pc_of_status p s st prf = ?.
140[ #p #s #st #prf
141  whd in match sigma_pc_of_status; normalize nodelta
142  @opt_safe_elim
143  #n
144  lapply (refl …  (int_funct_of_block (joint_closed_internal_function p) (globals p)
145        (ev_genv p) (pblock (pc p st))))
146  elim (int_funct_of_block (joint_closed_internal_function p) (globals p)
147        (ev_genv p) (pblock (pc p st))) in ⊢ (???%→%);
148  [ #_ #ABS normalize in ABS; destruct(ABS) ]
149  #f #EQ >m_return_bind
150*)
151
152
153(*
154lemma wf_status_to_wf_pc :
155∀p,p',graph_prog,stack_sizes.
156∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) →
157    code_point (mk_graph_params p) → option ℕ).
158∀st.
159well_formed_status p p' graph_prog stack_sizes sigma st →
160well_formed_pc p p' graph_prog stack_sizes sigma (pc ? st).
161#p #p' #graph_prog #stack_sizes #sigma #st whd in ⊢ (% → ?); * #H #_ @H
162qed.
163 *)
164 definition sigma_pc :
165∀p,p',graph_prog.
166∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) →
167    label → option ℕ).
168∀pc.
169∀prf : well_formed_pc p p' graph_prog sigma pc.
170program_counter ≝
171λp,p',graph_prog,sigma,st.opt_safe ….
172 
173lemma sigma_pc_ok:
174  ∀p,p',graph_prog.
175  ∀sigma.
176   ∀pc.
177    ∀prf:well_formed_pc p p' graph_prog sigma pc.
178    sigma_pc_opt p p' graph_prog sigma pc =
179    Some … (sigma_pc p p' graph_prog sigma pc prf).
180    #p #p' #graph_prog #sigma #st #prf @opt_to_opt_safe qed.
181
182definition sigma_function_name :
183 ∀p,graph_prog.
184 let lin_prog ≝ linearise p graph_prog in
185  (Σf.is_internal_function_of_program … graph_prog f) →
186  (Σf.is_internal_function_of_program … lin_prog f) ≝
187λp,graph_prog,f.«f, if_propagate … (pi2 … f)».
188
189record good_sigma_state (p : unserialized_params)
190  (p' : ∀F.sem_unserialized_params p F) (graph_prog : ?)
191 (sigma : (Σi.is_internal_function_of_program (joint_closed_internal_function (mk_graph_params p))
192    graph_prog i) →
193      label → option ℕ)
194: Type[0] ≝
195{ well_formed_state : state (make_sem_graph_params p p') → Prop
196; sigma_state : ∀st.well_formed_state st → state (make_sem_lin_params p p')
197
198; acca_store_ok :
199  ∀a,bv,bv',st,st',prf1,prf2.
200  sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
201  acca_store ?? (p' ?) a bv st = return st' →
202  acca_store … (p' ?) a bv' (sigma_state st prf1) = return sigma_state st' prf2
203; acca_store_wf :  ∀a,bv,bv',st,st'.
204  sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
205  acca_store ?? (p' ?) a bv st = return st' →
206  well_formed_state st → well_formed_state st'
207
208; acca_retrieve_ok :
209  ∀a,st,bv,prf1,prf2.
210  acca_retrieve ?? (p' ?) st a = return bv →
211  acca_retrieve ?? (p' ?) (sigma_state st prf1) a =
212  return sigma_beval p p' graph_prog sigma bv prf2
213; acca_retrieve_wf :  ∀a,st,bv.
214  acca_retrieve ?? (p' ?) st a = return bv →
215  well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?
216
217; acca_arg_retrieve_ok :
218  ∀a,st,bv,prf1,prf2.
219  acca_arg_retrieve ?? (p' ?) st a = return bv →
220  acca_arg_retrieve ?? (p' ?) (sigma_state st prf1) a =
221  return sigma_beval p p' graph_prog sigma bv prf2
222; acca_arg_retrieve_wf :  ∀a,st,bv.
223  acca_arg_retrieve ?? (p' ?) st a = return bv →
224  well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?
225
226; accb_store_ok :
227  ∀a,bv,bv',st,st',prf1,prf2.
228  sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
229  accb_store ?? (p' ?) a bv st = return st' →
230  accb_store … (p' ?) a bv' (sigma_state st prf1) = return sigma_state st' prf2
231; accb_store_wf :  ∀a,bv,bv',st,st'.
232  sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
233  accb_store ?? (p' ?) a bv st = return st' →
234  well_formed_state st → well_formed_state st'
235
236; accb_retrieve_ok :
237  ∀a,st,bv,prf1,prf2.
238  accb_retrieve ?? (p' ?) st a = return bv →
239  accb_retrieve ?? (p' ?) (sigma_state st prf1) a =
240  return sigma_beval p p' graph_prog sigma bv prf2
241; accb_retrieve_wf :  ∀a,st,bv.
242  accb_retrieve ?? (p' ?) st a = return bv →
243  well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?
244
245; accb_arg_retrieve_ok :
246  ∀a,st,bv,prf1,prf2.
247  acca_arg_retrieve ?? (p' ?) st a = return bv →
248  acca_arg_retrieve ?? (p' ?) (sigma_state st prf1) a =
249  return sigma_beval p p' graph_prog sigma bv prf2
250; accb_arg_retrieve_wf :  ∀a,st,bv.
251  accb_arg_retrieve ?? (p' ?) st a = return bv →
252  well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?
253
254
255; dpl_store_ok :
256  ∀a,bv,bv',st,st',prf1,prf2.
257  sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
258  dpl_store ?? (p' ?) a bv st = return st' →
259  dpl_store … (p' ?) a bv' (sigma_state st prf1) = return sigma_state st' prf2
260; dpl_store_wf :  ∀a,bv,bv',st,st'.
261  sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
262  dpl_store ?? (p' ?) a bv st = return st' →
263  well_formed_state st → well_formed_state st'
264
265; dpl_retrieve_ok :
266  ∀a,st,bv,prf1,prf2.
267  dpl_retrieve ?? (p' ?) st a = return bv →
268  dpl_retrieve ?? (p' ?) (sigma_state st prf1) a =
269  return sigma_beval p p' graph_prog sigma bv prf2
270; dpl_retrieve_wf :  ∀a,st,bv.
271  dpl_retrieve ?? (p' ?) st a = return bv →
272  well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?
273
274; dpl_arg_retrieve_ok :
275  ∀a,st,bv,prf1,prf2.
276  acca_arg_retrieve ?? (p' ?) st a = return bv →
277  acca_arg_retrieve ?? (p' ?) (sigma_state st prf1) a =
278  return sigma_beval p p' graph_prog sigma bv prf2
279; dpl_arg_retrieve_wf :  ∀a,st,bv.
280  dpl_arg_retrieve ?? (p' ?) st a = return bv →
281  well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?
282
283
284; dph_store_ok :
285  ∀a,bv,bv',st,st',prf1,prf2.
286  sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
287  dph_store ?? (p' ?) a bv st = return st' →
288  dph_store … (p' ?) a bv' (sigma_state st prf1) = return sigma_state st' prf2
289; dph_store_wf :  ∀a,bv,bv',st,st'.
290  sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
291  dph_store ?? (p' ?) a bv st = return st' →
292  well_formed_state st → well_formed_state st'
293
294; dph_retrieve_ok :
295  ∀a,st,bv,prf1,prf2.
296  dph_retrieve ?? (p' ?) st a = return bv →
297  dph_retrieve ?? (p' ?) (sigma_state st prf1) a =
298  return sigma_beval p p' graph_prog sigma bv prf2
299; dph_retrieve_wf :  ∀a,st,bv.
300  dph_retrieve ?? (p' ?) st a = return bv →
301  well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?
302
303; dph_arg_retrieve_ok :
304  ∀a,st,bv,prf1,prf2.
305  acca_arg_retrieve ?? (p' ?) st a = return bv →
306  acca_arg_retrieve ?? (p' ?) (sigma_state st prf1) a =
307  return sigma_beval p p' graph_prog sigma bv prf2
308; dph_arg_retrieve_wf :  ∀a,st,bv.
309  dph_arg_retrieve ?? (p' ?) st a = return bv →
310  well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?
311
312
313; snd_arg_retrieve_ok :
314  ∀a,st,bv,prf1,prf2.
315  snd_arg_retrieve ?? (p' ?) st a = return bv →
316  snd_arg_retrieve ?? (p' ?) (sigma_state st prf1) a =
317  return sigma_beval p p' graph_prog sigma bv prf2
318; snd_arg_retrieve_wf :  ∀a,st,bv.
319  snd_arg_retrieve ?? (p' ?) st a = return bv →
320  well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?
321
322; pair_reg_move_ok :
323  ∀mv,st1,st2,prf1,prf2.
324  pair_reg_move ?? (p' ?) st1 mv = return st2 →
325  pair_reg_move ?? (p' ?) (sigma_state st1 prf1) mv =
326    return sigma_state st2 prf2
327; pair_reg_move_wf :
328  ∀mv,st1,st2.
329  pair_reg_move ?? (p' ?) st1 mv = return st2 →
330  well_formed_state st1 → well_formed_state st2
331
332; allocate_locals_ok :
333  ∀l,st1,prf1,prf2.
334  allocate_locals ?? (p' ?) l (sigma_state st1 prf1) =
335    sigma_state (allocate_locals ?? (p' ?) l st1) prf2
336; allocate_locals_wf :
337  ∀l,st1.
338  well_formed_state st1 →
339    well_formed_state (allocate_locals ?? (p' ?) l st1)
340
341; save_frame_ok :
342  ∀dest,st1,st2,prf1,prf2.
343  save_frame ?? (p' ?) dest st1 = return st2 →
344  let st1' ≝ mk_state_pc … (sigma_state st1 (proj2 … prf1))
345    (sigma_pc p p' graph_prog sigma (pc … st1) (proj1 … prf1)) in
346  save_frame ?? (p' ?) dest st1' = return sigma_state st2 prf2
347; save_frame_wf :
348  ∀dest,st1,st2.
349  save_frame ?? (p' ?) dest st1 = return st2 →
350  (well_formed_pc p p' graph_prog sigma (pc … st1) ∧
351   well_formed_state st1) → well_formed_state st2
352
353; eval_ext_seq_ok :
354  let lin_prog ≝ linearise p graph_prog in
355  ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
356  let stack_sizes' ≝
357   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
358     ? graph_prog stack_sizes in
359  ∀ext,fn,st1,st2,prf1,prf2.
360  eval_ext_seq ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes'))
361    ext fn st1 = return st2 →
362  eval_ext_seq ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
363    ext (sigma_function_name … fn) (sigma_state st1 prf1) = return sigma_state st2 prf2
364; eval_ext_seq_wf :
365  let lin_prog ≝ linearise p graph_prog in
366  ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
367  let stack_sizes' ≝
368   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
369     ? graph_prog stack_sizes in
370  ∀ext,fn,st1,st2.
371  eval_ext_seq ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes'))
372    ext fn st1 = return st2 →
373  well_formed_state st1 → well_formed_state st2
374
375}.
376
377(* restano:
378; setup_call : nat → paramsT … uns_pars → call_args uns_pars →
379    state st_pars → res (state st_pars)
380; fetch_external_args: external_function → state st_pars → call_args … uns_pars →
381    res (list val)
382; set_result: list val → call_dest uns_pars → state st_pars → res (state st_pars)
383
384(* from now on, parameters that use the type of functions *)
385; read_result: ∀globals.genv_gen F globals → call_dest uns_pars → state st_pars → res (list beval)
386(* change of pc must be left to *_flow execution *)
387; pop_frame: ∀globals.∀ge : genv_gen F globals.
388  (Σi.is_internal_function … ge i) (* current *) → state st_pars → res (state st_pars)
389*)
390
391definition well_formed_state_pc :
392 ∀p,p',graph_prog,sigma.
393  good_sigma_state p p' graph_prog sigma →
394  state_pc (make_sem_graph_params p p') → Prop ≝
395 λp,p',prog,sigma,gss,st.
396 well_formed_pc p p' prog sigma (pc … st) ∧ well_formed_state … gss st.
397 
398definition sigma_state_pc :
399 ∀p.
400 ∀p':∀F.sem_unserialized_params p F.
401 ∀graph_prog.
402  ∀sigma.
403(*   let lin_prog ≝ linearise ? graph_prog in *)
404  ∀gss : good_sigma_state p p' graph_prog sigma.
405    ∀s:state_pc (make_sem_graph_params p p'). (* = graph_abstract_status p p' graph_prog stack_sizes *)
406     well_formed_state_pc p p' graph_prog sigma gss s →
407      state_pc (make_sem_lin_params p p') (* = lin_abstract_status p p' lin_prog ? *)
408
409 λp,p',graph_prog,sigma,gss,s,prf.
410 let pc' ≝ sigma_pc … (proj1 … prf) in
411 let st' ≝ sigma_state … (proj2 … prf) in
412 mk_state_pc ? st' pc'.
413
414(*
415lemma sigma_pc_commute:
416 ∀p,p',graph_prog,sigma,gss,st.
417 ∀prf : well_formed_state_pc p p' graph_prog sigma gss st.
418 sigma_pc … (pc ? st) (proj1 … prf) =
419 pc ? (sigma_state_pc … st prf). // qed.
420*)
421
422lemma res_eq_from_opt :
423  ∀A,m,v.res_to_opt A m = return v → m = return v.
424#A * #x #v normalize #EQ destruct % qed.
425
426lemma if_of_function_commute:
427 ∀p.
428 ∀graph_prog : joint_program (mk_graph_params p).
429 ∀graph_fun : Σi.is_internal_function_of_program … graph_prog i.
430 let graph_fd ≝ if_of_function … graph_fun in
431 let lin_fun ≝ sigma_function_name … graph_fun in
432 let lin_fd ≝ if_of_function … lin_fun in
433 lin_fd = \fst (linearise_int_fun ?? graph_fd).
434 #p #graph_prog #graph_fun whd
435 @prog_if_of_function_transform % qed.
436
437lemma bind_opt_inversion:
438  ∀A,B: Type[0]. ∀f: option A. ∀g: A → option B. ∀y: B.
439  (! x ← f ; g x = Some … y) →
440  ∃x. (f = Some … x) ∧ (g x = Some … y).
441#A #B #f #g #y cases f normalize
442[ #H destruct (H)
443| #a #e %{a} /2 by conj/
444] qed.
445
446lemma sigma_pblock_eq_lemma :
447∀p,p',graph_prog.
448let lin_prog ≝ linearise p graph_prog in
449∀sigma,pc.
450∀prf : well_formed_pc p p' graph_prog sigma pc.
451 pc_block (sigma_pc ? p' graph_prog sigma pc prf) =
452 pc_block pc.
453 #p #p' #graph_prog #sigma #pc #prf
454 whd in match sigma_pc; normalize nodelta
455 @opt_safe_elim #x #x_spec
456 whd in x_spec:(??%?); cases (int_funct_of_block ???) in x_spec;
457 normalize nodelta [#abs destruct] #id #H cases (bind_opt_inversion ????? H) -H
458 #offset * #_ whd in ⊢ (??%? → ?); #EQ destruct //
459qed.
460
461(*
462lemma bind_opt_non_none : ∀A,B : Type[0] . ∀ m : option A . ∀g : A → option B.
463(! x ← m ; g x) ≠ None ? → m ≠ None ?.
464#A #B #m #g #H % #m_eq_none cases m >m_eq_none in H; normalize 
465[ #abs elim abs -abs #abs @abs %
466| #abs elim abs -abs #abs #v @abs %
467]
468qed.
469
470lemma match_option_non_none : ∀A ,B, C : Type[0]. ∀m : option A. ∀ x : A.
471∀ b : B .∀ f : A → B. ∀g : B → option C.
472g (match m with [None  ⇒ b  | Some  x ⇒ f x])≠ None ? →  g b = None ? → m ≠ None ?.
473#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
474qed.
475*)
476
477lemma funct_of_block_transf :
478∀A,B.∀progr : program (λvars .fundef (A vars)) ℕ.
479∀transf : ∀vars. A vars → B vars. ∀bl,f,prf.
480let progr' ≝ transform_program … progr (λvars.transf_fundef … (transf vars)) in
481funct_of_block … (globalenv_noinit … progr) bl = return f →
482funct_of_block … (globalenv_noinit … progr') bl = return «pi1 … f,prf».
483#A #B #progr #transf #bl #f #prf whd
484whd in match funct_of_block in ⊢ (%→?); normalize nodelta
485cut (∀A,B : Type[0].∀Q : option A → Prop.∀P : B → Prop.
486  ∀o.∀prf : Q o.
487  ∀f1,f2.
488  (∀x,prf.P (f1 x prf)) → (∀prf.P(f2 prf)) →
489  P (match o return λx.Q x → B with [ Some x ⇒ f1 x | None ⇒ f2 ] prf))
490  [ #A #B #Q #P * /2/ ] #aux
491@aux [2: #_ change with (?=Some ??→?) #ABS destruct(ABS) ]
492#fd #EQfind whd in ⊢ (??%%→?);
493generalize in ⊢ (??(??(????%))?→?); #e #EQ destruct(EQ)
494whd in match funct_of_block; normalize nodelta
495@aux [ # fd' ]
496[2: >(find_funct_ptr_transf … EQfind) #ABS destruct(ABS) ]
497#prf' cases daemon qed.
498
499lemma description_of_function_transf :
500∀A,B.∀progr : program (λvars .fundef (A vars)) ℕ.
501∀transf : ∀vars. A vars → B vars.
502let progr' ≝ transform_program … progr (λvars.transf_fundef … (transf vars)) in
503∀f_out,prf.
504description_of_function …
505  (globalenv_noinit … progr') f_out =
506transf_fundef … (transf ?) (description_of_function … (globalenv_noinit … progr)
507  «pi1 … f_out, prf»).
508#A #B #progr #transf #f_out #prf
509whd in match description_of_function in ⊢ (???%);
510normalize nodelta
511cut (∀A,B : Type[0].∀Q : option A → Prop.∀P : B → Prop.
512  ∀o.∀prf : Q o.
513  ∀f1,f2.
514  (∀x,prf.o = Some ? x → P (f1 x prf)) → (∀prf.o = None ? → P(f2 prf)) →
515  P (match o return λx.Q x → B with [ Some x ⇒ f1 x | None ⇒ f2 ] prf))
516  [ #A #B #Q #P * /2/ ] #aux
517@aux
518[ #fd' ] * #fd #EQ destruct (EQ)
519inversion (find_symbol ???) [ #_ whd in ⊢ (??%?→?); #ABS destruct(ABS) ]
520#bl #EQfind >m_return_bind #EQfindf
521whd in match description_of_function; normalize nodelta
522@aux
523[ #fdo' ] * #fdo #EQ destruct (EQ)
524>find_symbol_transf >EQfind >m_return_bind
525>(find_funct_ptr_transf … EQfindf) #EQ destruct(EQ) %
526qed.
527
528
529lemma match_int_fun :
530∀A,B : Type[0].∀P : B → Prop.
531∀Q : fundef A → Prop.
532∀m : fundef A.
533∀f1 : ∀fd.Q (Internal \ldots  fd) → B.
534∀f2 : ∀fd.Q (External … fd) → B.
535∀prf : Q m.
536(∀fd,prf.P (f1 fd prf)) →
537(∀fd,prf.P (f2 fd prf)) →
538P (match m
539return λx.Q x → ?
540with
541[ Internal fd ⇒ f1 fd
542| External fd ⇒ f2 fd
543] prf).
544#A #B #P #Q * // qed.
545(*)
546 lemma match_int_fun :
547∀A,B : Type[0].∀P : B → Prop.
548∀m : fundef A.
549∀f1 : ∀fd.m = Internal … fd → B.
550∀f2 : ∀fd.m = External … fd → B.
551(∀fd,prf.P (f1 fd prf)) →
552(∀fd,prf.P (f2 fd prf)) →
553P (match m
554return λx.m = x → ?
555with
556[ Internal fd ⇒ f1 fd
557| External fd ⇒ f2 fd
558] (refl …)).
559#A #B #P * // qed.
560*)
561(*
562lemma prova :
563∀ A.∀progr : program (λvars. fundef (A vars)) ℕ.
564∀ M : fundef (A (prog_var_names (λvars:list ident.fundef (A vars)) ℕ progr)).
565∀ f,g,prf1.
566match M return λx.M = x → option (Σi.is_internal_function_of_program ?? progr i) with
567[Internal fn ⇒ λ prf.return «g,prf1 fn prf» |
568External fn ⇒ λprf.None ? ] (refl ? M) = return f → 
569∃ fn. ∃ prf : M = Internal ? fn . f = «g, prf1 fn prf».
570#H1 #H2 #H3 #H4 #H5 #H6
571@match_int_fun
572#fd #EQ #EQ' whd in EQ' : (??%%); destruct
573%[|%[| % ]] qed.
574*)
575
576lemma int_funct_of_block_transf:
577 ∀A,B.∀progr: program (λvars. fundef (A vars)) ℕ.
578  ∀transf: ∀vars. A vars → B vars. ∀bl,f,prf.
579   let progr' ≝ transform_program … progr (λvars.transf_fundef … (transf vars)) in
580     int_funct_of_block ? (globalenv_noinit … progr) bl = return f →
581     int_funct_of_block ? (globalenv_noinit … progr') bl = return «pi1 … f,prf».
582#A #B #progr #transf #bl #f #prf
583whd whd in match int_funct_of_block in ⊢ (??%?→?); normalize nodelta
584#H
585elim (bind_opt_inversion ??? ?? H) -H #x
586* #x_spec
587@match_int_fun [2: #fd #_ #ABS destruct(ABS) ]
588#fd #EQdescr change with (Some ?? = ? → ?) #EQ destruct(EQ)
589whd in match int_funct_of_block; normalize nodelta
590>(funct_of_block_transf … (internal_function_is_function … prf) … x_spec)
591>m_return_bind
592@match_int_fun #fd' #prf' [ % ]
593@⊥ cases x in prf EQdescr prf'; -x #x #x_prf #prf #EQdescr
594>(description_of_function_transf) [2: @x_prf ]
595>EQdescr whd in ⊢ (??%%→?); #ABS destruct qed.
596
597
598lemma fetch_function_sigma_commute :
599 ∀p,p',graph_prog.
600 let lin_prog ≝ linearise p graph_prog in
601 ∀sigma,pc_st,f.
602  ∀prf : well_formed_pc p p' graph_prog sigma pc_st.
603 fetch_function … (globalenv_noinit … graph_prog) pc_st =
604  return f
605→ fetch_function … (globalenv_noinit … lin_prog) (sigma_pc … pc_st prf) =
606  return sigma_function_name … f.
607 #p #p' #graph_prog #sigma #st #f #prf
608 whd in match fetch_function; normalize nodelta
609 >(sigma_pblock_eq_lemma … prf) #H
610 lapply (opt_eq_from_res ???? H) -H #H
611 >(int_funct_of_block_transf ?? graph_prog (λvars,graph_fun.\fst (linearise_int_fun … graph_fun)) ??? H)
612 //
613qed.
614 
615(*
616#H elim (bind_opt_inversion ????? H) -H
617#x * whd in match funct_of_block in ⊢ (%→?); normalize nodelta
618@match_opt_prf_elim
619 #H #H1  whd in H : (??%?);
620cases (   find_funct_ptr
621   (fundef
622    (joint_closed_internal_function
623     (graph_prog_params p p' graph_prog
624      (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
625       (linearise_int_fun p) graph_prog stack_sizes))
626     (globals
627      (graph_prog_params p p' graph_prog
628       (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
629        (linearise_int_fun p) graph_prog stack_sizes)))))
630   (ev_genv
631    (graph_prog_params p p' graph_prog
632     (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
633      (linearise_int_fun p) graph_prog stack_sizes)))
634   (pblock (pc (make_sem_graph_params p p') st))) in H; [ 2: normalize #abs destruct
635 
636
637normalize nodelta
638#H #H1
639cases (   find_funct_ptr
640   (fundef
641    (joint_closed_internal_function
642     (graph_prog_params p p' graph_prog
643      (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
644       (linearise_int_fun p) graph_prog stack_sizes))
645     (globals
646      (graph_prog_params p p' graph_prog
647       (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
648        (linearise_int_fun p) graph_prog stack_sizes)))))
649   (ev_genv
650    (graph_prog_params p p' graph_prog
651     (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
652      (linearise_int_fun p) graph_prog stack_sizes)))
653   (pblock (pc (make_sem_graph_params p p') st))) in H;
654
655
656check find_funct_ptr_transf
657whd in match int_funct_of_block; normalize nodelta
658#H elim (bind_inversion ????? H)
659
660.. sigma_int_funct_of_block
661
662
663
664whd in match int_funct_of_block; normalize nodelta
665elim (bind_inversion ????? H)
666whd in match int_funct_of_block; normalize nodelta
667#H elim (bind_inversion ????? H) -H #fn *
668#H lapply (opt_eq_from_res ???? H) -H
669#H >(find_funct_ptr_transf … (λglobals.transf_fundef … (linearise_int_fun … globals)) … H)
670-H #H >m_return_bind cases fn in H; normalize nodelta #arg #EQ whd in EQ:(??%%);
671destruct //
672cases daemon
673qed. *)
674
675lemma opt_Exists_elim:
676 ∀A:Type[0].∀P:A → Prop.
677  ∀o:option A.
678   opt_Exists A P o →
679    ∃v:A. o = Some … v ∧ P v.
680 #A #P * normalize /3/ *
681qed.
682
683
684lemma stmt_at_sigma_commute:
685 ∀p,graph_prog,graph_fun,lbl,pt.
686 let lin_prog ≝ linearise ? graph_prog in
687 let lin_fun ≝ sigma_function_name p graph_prog graph_fun in
688 ∀sigma.good_sigma p graph_prog sigma →
689 sigma graph_fun lbl = return pt →
690 ∀stmt.
691   stmt_at …
692    (joint_if_code ?? (if_of_function ?? graph_fun)) 
693    lbl = return stmt →
694   stmt_at ??
695    (joint_if_code ?? (if_of_function ?? lin_fun))
696    pt = return (graph_to_lin_statement … stmt). 
697 #p #graph_prog #graph_fun #lbl #pt #sigma #good #prf #stmt
698cases (good graph_fun (pi2 … (sigma_function_name p graph_prog graph_fun)))
699#sigma_entry_is_zero #lin_stmt_spec
700lapply (lin_stmt_spec lbl pt prf) -lin_stmt_spec * #stmt1 *
701#EQlookup_stmt1 #H
702elim (opt_Exists_elim … H) -H * #optlbl_graph_stmt #graph_stmt
703* #EQnth_opt_graph_stmt normalize nodelta
704* #optEQlbl_optlbl_graph_stmt #next_spec
705whd in match (stmt_at ????) in ⊢ (% → ?);
706normalize nodelta
707>EQlookup_stmt1 whd in ⊢ ((???%) → ?); #EQ destruct(EQ)
708whd in match (stmt_at ????); > EQnth_opt_graph_stmt
709normalize nodelta elim  optEQlbl_optlbl_graph_stmt #_ #EQ >EQ //
710qed.
711(*
712
713 >(if_of_function_commute … graph_fun)
714
715check opt_Exists
716check linearise_int_fun
717check
718 whd in match (stmt_at ????);
719 whd in match (stmt_at ????);
720 cases (linearise_code_spec … p' graph_prog graph_fun
721         (joint_if_entry … graph_fun))
722 * #lin_code_closed #sigma_entry_is_zero #sigma_spec
723 lapply (sigma_spec
724         (point_of_pointer ? (graph_prog_params … p' graph_prog) (pc … s1)))
725 -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @(sigma_pc_of_status_ok … prf) |2: skip ]
726 -sigma_spec #graph_stmt * #graph_lookup_ok >graph_lookup_ok -graph_lookup_ok
727 whd in ⊢ (? → ???%); #sigma_spec whd in sigma_spec;
728 inversion (nth_opt ???) in sigma_spec; [ #H whd in ⊢ (% → ?); #abs cases abs ]
729 * #optlabel #lin_stm #lin_lookup_ok whd in ⊢ (% → ?); ** #_
730 #related_lin_stm_graph_stm #_ <related_lin_stm_graph_stm -related_lin_stm_graph_stm
731 <sigma_pc_commute >lin_lookup_ok // *)
732
733lemma fetch_statement_sigma_commute:
734  ∀p,p',graph_prog,pc,fn,stmt.
735  let lin_prog ≝ linearise ? graph_prog in
736  ∀sigma.good_sigma p graph_prog sigma →
737  ∀prf : well_formed_pc p p' graph_prog sigma pc.
738  fetch_statement ? (make_sem_graph_params p p') …
739    (globalenv_noinit … graph_prog) pc = return 〈fn,stmt〉 →
740  fetch_statement ? (make_sem_lin_params p p') …
741    (globalenv_noinit … lin_prog) (sigma_pc … pc prf) =
742    return 〈sigma_function_name … fn, graph_to_lin_statement … stmt〉.
743 #p #p' #graph_prog #pc #fn #stmt #sigma #good #wfprf
744 whd in match fetch_statement; normalize nodelta #H
745 cases (bind_inversion ????? H) #id * -H #fetchfn
746 >(fetch_function_sigma_commute … wfprf … fetchfn) >m_return_bind
747 #H cases (bind_inversion ????? H) #fstmt * -H #H
748 lapply (opt_eq_from_res ???? H) -H #H #EQ whd in EQ:(??%%); destruct
749 >(stmt_at_sigma_commute … good … H) [%]
750 whd in match sigma_pc; normalize nodelta
751 @opt_safe_elim #pc' #H
752 cases (bind_opt_inversion ????? H)
753 #i * #EQ1 -H #H
754 cases (bind_opt_inversion ????? H)
755 #pnt * #EQ2 whd in ⊢ (??%?→?); #EQ3 destruct
756 whd in match point_of_pc in ⊢ (???%); normalize nodelta >point_of_offset_of_point
757 lapply (opt_eq_from_res ???? fetchfn) >EQ1 #EQ4 destruct @EQ2
758qed.
759
760lemma point_of_pc_sigma_commute :
761 ∀p,p',graph_prog.
762 let lin_prog ≝ linearise p graph_prog in
763 ∀sigma,pc,fn,n.
764  ∀prf : well_formed_pc p p' graph_prog sigma pc.
765 int_funct_of_block … (globalenv_noinit … graph_prog) (pc_block pc) = return fn →
766 sigma fn (point_of_pc ? (make_sem_graph_params p p') pc) = return n →
767 point_of_pc ? (make_sem_lin_params p p') (sigma_pc … pc prf) = n.
768#p #p' #graph_prog #sigma #pc #fn #n #prf #EQfetch #EQsigma
769whd in match sigma_pc; normalize nodelta
770@opt_safe_elim #pc' whd in match sigma_pc_opt;
771normalize nodelta >EQfetch >m_return_bind >EQsigma
772>m_return_bind whd in ⊢ (??%?→?); #EQ destruct(EQ)
773change with (point_of_offset ??? = ?) @point_of_offset_of_point
774qed.
775
776definition linearise_status_rel:
777 ∀p,p',graph_prog.
778 let lin_prog ≝ linearise p graph_prog in
779 ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
780 let stack_sizes' ≝
781  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
782    ? graph_prog stack_sizes in
783 ∀sigma,gss.
784 good_sigma p graph_prog sigma →
785   status_rel
786    (graph_abstract_status p p' graph_prog stack_sizes')
787    (lin_abstract_status p p' lin_prog stack_sizes)
788 ≝ λp,p',graph_prog,stack_sizes,sigma,gss,good.
789   mk_status_rel …
790    (* sem_rel ≝ *) (λs1,s2.
791     ∃prf: well_formed_state_pc p p' graph_prog sigma gss s1.
792      s2 = sigma_state_pc … s1 prf)
793    (* call_rel ≝ *) (λs1,s2.
794      ∃prf:well_formed_state_pc p p' graph_prog sigma gss s1.
795      pc ? s2 = sigma_pc … (pc ? s1) (proj1 … prf))
796    (* sim_final ≝ *) ?.
797#st1 #st2 * #prf #EQ2
798%
799whd in ⊢ (%→%);
800#H lapply (opt_to_opt_safe … H)
801@opt_safe_elim -H
802#res #_
803#H lapply (res_eq_from_opt ??? H) -H
804cases daemon
805(*#H elim (bind_inversion ????? H) in ⊢ ?;
806* #f #stmt *
807whd in ⊢ (??%?→?);*)
808qed.
809
810lemma IO_bind_inversion:
811  ∀O,I,A,B. ∀f: IO O I A. ∀g: A → IO O I B. ∀y: B.
812  (! x ← f ; g x = return y) →
813  ∃x. (f = return x) ∧ (g x = return y).
814#O #I #A #B #f #g #y cases f normalize
815[ #o #f #H destruct
816| #a #e %{a} /2 by conj/
817| #m #H destruct (H)
818] qed.
819
820lemma err_eq_from_io : ∀O,I,X,m,v.
821  err_to_io O I X m = return v → m = return v.
822#O #I #X * #x #v normalize #EQ destruct % qed.
823
824lemma eval_seq_no_pc_sigma_commute :
825 ∀p,p',graph_prog.
826 let lin_prog ≝ linearise p graph_prog in
827 ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
828 let stack_sizes' ≝
829  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
830    ? graph_prog stack_sizes in
831 ∀sigma.∀gss : good_sigma_state … graph_prog sigma.
832 ∀fn,st,stmt,st'.
833 ∀prf : well_formed_state … gss st.∀prf'.
834  eval_seq_no_pc ?? (ev_genv … (graph_prog_params … graph_prog stack_sizes'))
835   fn st stmt = return st' →
836  eval_seq_no_pc ?? (ev_genv … (lin_prog_params … lin_prog stack_sizes))
837    (sigma_function_name … fn) (sigma_state … gss st prf) stmt =
838  return sigma_state … gss st' prf'.
839  #p #p' #graph_prog #stack_sizes #sigma #gss
840  #fn #st #stmt
841  #st' #prf #prf'
842  cases daemon (*
843  whd in match eval_seq_no_pc;
844  cases stmt normalize nodelta
845  [1,2: #_ #EQ whd in EQ : (??%%); destruct(EQ) //
846  | #mv_sig whd in match pair_reg_move in ⊢ (%→?); normalize nodelta     
847    #H
848  ] *)
849qed.       
850       
851inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
852    ex1_intro: ∀ x:A. P x →  ex_Type1 A P.
853(*interpretation "exists in Type[1]" 'exists x = (ex_Type1 ? x).*)
854
855lemma linearise_ok:
856 ∀p,p',graph_prog.
857  let lin_prog ≝ linearise ? graph_prog in
858 ∀lin_stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
859 let graph_stack_sizes ≝
860  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
861    ? graph_prog lin_stack_sizes in
862 (∀sigma.good_sigma_state p p' graph_prog sigma) →
863   ex_Type1 … (λR.
864   status_simulation
865    (graph_abstract_status p p' graph_prog graph_stack_sizes)
866    (lin_abstract_status p p' lin_prog lin_stack_sizes) R).
867 #p #p' #graph_prog
868 cases (linearise_spec … graph_prog) #sigma #good
869 #lin_stack_sizes
870 #gss lapply (gss sigma) -gss #gss
871 %{(linearise_status_rel p p' graph_prog lin_stack_sizes sigma gss good)}
872whd in match graph_abstract_status;
873whd in match lin_abstract_status;
874whd in match graph_prog_params;
875whd in match lin_prog_params;
876normalize nodelta
877whd
878whd in ⊢ (%→%→%→?);
879whd in ⊢ (?(?%)→?(?%)→?(?%)→?);
880whd in ⊢ (?%→?%→?%→?);
881#st1 #st1' #st2
882whd in ⊢ (%→?);
883change with
884  (eval_state (make_sem_graph_params p p') (prog_var_names ???) ?? = ? → ?)
885whd in match eval_state in ⊢ (%→?); normalize nodelta
886change with (Σi.is_internal_function_of_program ? graph_prog i) in
887match (Sig ??) in ⊢ (%→?);
888letin globals ≝ (prog_var_names ?? graph_prog)
889change with (fetch_statement ??? (globalenv_noinit ? graph_prog) ?) in
890  match (fetch_statement ?????) in ⊢ (%→?);
891#ex
892cases (IO_bind_inversion ??????? ex) in ⊢ ?; * #fn #stmt * -ex
893#EQfetch lapply (err_eq_from_io ????? EQfetch) -EQfetch
894#EQfetch
895cases (bind_inversion ????? EQfetch)
896#f_id * #H lapply (opt_eq_from_res ???? H) -H
897#EQfunc_of_block
898#H elim (bind_inversion ????? H) -H #stmt' *
899#H lapply (opt_eq_from_res ???? H) -H #EQstmt_at
900whd in ⊢ (??%%→?); #EQ destruct(EQ)
901#EQeval
902cases (good fn (pi2 … (sigma_function_name p graph_prog fn)))
903letin graph_fun ≝ (if_of_function … fn) in EQstmt_at; #EQstmt_at
904#entry_0
905#good_local
906* * #wf_pc #wf_state #EQst2
907generalize in match wf_pc in ⊢ ?;
908whd in ⊢ (%→?);
909inversion (sigma_pc_opt ?????) in ⊢ (%→?); [ #_ * #ABS elim (ABS ?) % ]
910#lin_pc
911whd in match (sigma_pc_opt) in ⊢ (%→?); normalize nodelta
912>EQfunc_of_block in ⊢ (%→?); >m_return_bind in ⊢ (%→?);
913#H elim (bind_opt_inversion ????? H) in ⊢ ?; -H #lin_pt *
914#EQsigma whd in ⊢ (??%?→?); #EQ destruct(EQ) #_
915elim (good_local … EQsigma) -good_local
916#stmt' *
917change with (stmt_at ?? (joint_if_code ?? graph_fun) ? = ? → ?)
918>EQstmt_at #EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ)
919#H elim (opt_Exists_elim … H) -H * #lbl_opt #lin_stmt normalize nodelta
920>(prog_if_of_function_transform … fn) in ⊢ (%→?); [2: % ]
921change with graph_fun in match (if_of_function ?? fn) in ⊢ (%→?);
922letin lin_fun ≝ (\fst  (linearise_int_fun p globals graph_fun))
923change with globals in match (prog_var_names ?? graph_prog) in ⊢ (%→?);
924*
925#EQnth_opt ** #opt_lbl_spec #EQ destruct(EQ) #next_spec
926letin lin_prog ≝ (linearise … graph_prog)
927lapply (refl … (eval_state ? globals (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) st2))
928destruct(EQst2)
929whd in match eval_state in ⊢ (???%→?); normalize nodelta
930letin st2 ≝ (sigma_state_pc ????? st1 ?)
931>(fetch_statement_sigma_commute … good … EQfetch) in ⊢ (%→?);
932>m_return_bind in ⊢ (%→?);
933#ex'
934(* resolve classifier *)
935whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
936>EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
937normalize nodelta
938cases stmt in EQfetch EQeval EQstmt_at EQnth_opt next_spec ex';
939[ *
940  [ #stmt #nxt
941    whd in match eval_statement in ⊢ (?→%→?); normalize nodelta
942    #EQfetch #EQeval #EQstmt_at #EQnth_opt #next_spec
943    whd in match (graph_to_lin_statement ???) in ⊢ (%→?);
944    whd in match eval_statement in ⊢ (%→?); normalize nodelta
945    elim (IO_bind_inversion ??????? EQeval) #st1_no_pc *
946    #EQeval_no_pc #EQeval_pc
947    >(eval_seq_no_pc_sigma_commute … EQeval_no_pc)
948    [2: (*TODO lemma eval_seq_no_pc_wf *) @hide_prf cases daemon ]
949        >m_return_bind
950    cases stmt in EQfetch EQeval_no_pc EQeval_pc EQstmt_at EQnth_opt next_spec;
951    [14: #f #args #dest
952    | #c
953    | #lbl
954    | #move_sig
955    | #a
956    | #a
957    | #sy #sy_prf #dpl #dph
958    | #op #a #b #arg1 #arg2
959    | #op #a #arg
960    | #op #a #arg1 #arg2
961    ||
962    | #a #dpl #dph
963    | #dpl #dph #a
964    | #s_ext
965    ]
966    [ (* CALL *)
967    |(*:*)
968      normalize nodelta
969      #EQfetch #EQeval_no_pc #EQeval_pc #EQstmt_at #EQnth_opt #next_spec
970      whd in match eval_seq_pc; normalize nodelta
971      #ex1
972      cases next_spec
973      [ #EQnext_sigma
974        %[2: %{(taaf_step … (taa_base …) ex1 ?)}
975         [ cases daemon (* TODO lemma joint_classify_sigma_commute *) ]|]
976        normalize nodelta
977        cut (? : Prop) [3: #R' % [ %{I R'} ] |*:]
978        [ cases daemon (* TODO lemma joint_label_sigma_commute *)
979        | %
980          [ (* TODO lemma well_formed_state_pc_preserve? *) @hide_prf cases daemon
981          | whd in match eval_seq_pc in EQeval_pc;
982            whd in EQeval_pc : (??%%); whd in EQeval_pc : (??(????%)?);
983            destruct (EQeval_pc)
984            whd in ⊢ (??%%);
985            change with (sigma_pc ??????) in match
986              (pc ? (sigma_state_pc ???????));
987            whd in match (succ_pc ????) in ⊢ (??%%);
988            whd in match (point_of_succ ???) in ⊢ (??%%);
989            >(point_of_pc_sigma_commute … EQfunc_of_block EQsigma)
990            whd in match sigma_pc in ⊢ (???%);
991            whd in match sigma_pc_opt in ⊢ (???%); normalize nodelta
992            @opt_safe_elim #pc'
993            >EQfunc_of_block >m_return_bind
994            whd in match point_of_pc; normalize nodelta
995            >point_of_offset_of_point
996            >EQnext_sigma whd in ⊢ (??%?→?);
997            whd in match pc_of_point; normalize nodelta
998            #EQ destruct(EQ)
999            >sigma_pblock_eq_lemma %
1000          ]
1001        ]
1002      | -next_spec #next_spec
1003        %
1004     
1005     
1006        whd in ⊢ (?→???%→?);
1007        generalize in ⊢ (??%? → ???(????%) → ?); |*: skip]  | #a #lbltrue #next
1008  ] #next change with label in next;
1009| *
1010  [ #lbl
1011  |
1012  | #fl #f #args
1013  ]
1014]
1015whd in match eval_statement in ⊢ (?→%→?); normalize nodelta
1016#EQfetch #EQeval #EQstmt_at #EQnth_opt #next_spec
1017normalize nodelta
1018whd in match (graph_to_lin_statement ???) in ⊢ (%→?);
1019whd in match eval_statement in ⊢ (%→?); normalize nodelta
1020[ >m_return_bind in ⊢ (%→?);
1021  >m_return_bind in EQeval;
1022
1023
1024
1025  (* common for all non-call seq *)
1026  >m_return_bind in ⊢ (%→?);
1027  whd in ⊢ (??%%→?); #EQ destruct(EQ)
1028  >m_return_bind in ⊢ (%→?);
1029
1030 
1031  #ex1
1032lapply (refl … (eval_state ? globals (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) st2))
1033
1034whd in match (point_of_pc ???);
1035whd in match (point_of_succ ???);
1036whd in match sigma_pc in ⊢ (???%); normalize nodelta @opt_safe_elim
1037#pc' #H
1038elim (bind_opt_inversion ????? H) #fn * #EQbl
1039-H #H 
1040elim (bind_opt_inversion ????? H) -H #n * #EQsigma whd in ⊢ (??%?→?);
1041#EQ destruct(EQ)
1042whd in match (succ_pc ????);
1043whd in match (point_of_succ ???);
1044change with (point_of_offset ???) in match (point_of_pc ???);
1045>point_of_offset_of_point
1046whd in match sigma_pc; normalize nodelta @opt_safe_elim
1047#pc' whd in match sigma_pc_opt; normalize nodelta
1048
1049 
1050 
1051        whd in match (succ_pc ????);
1052               
1053        change with next in match (offset_of_point ???) in ⊢ (???%);
1054whd in fetch_statement_spec : (??()%);
1055cases cl in classified_st1_cl; -cl #classified_st1_cl whd
1056[4:
1057 >rel_st1_st2 -st2 letin lin_prog ≝ (linearise ? graph_prog)
1058 cases (good (pi1 ?? fn)) [2: cases daemon (* TODO *) ]
1059 #sigma_entry_is_zero #sigma_spec
1060 lapply (sigma_spec (point_of_pc … (make_sem_graph_params … p') (pc … st1)))
1061 -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @opt_to_opt_safe cases daemon (* TO REDO *) |2: skip ]
1062 -sigma_spec #graph_stmt * #graph_lookup_ok #sigma_spec
1063 cases (opt_Exists_elim … sigma_spec) in ⊢ ?;
1064 * #optlabel #lin_stm * #lin_lookup_ok whd in ⊢ (% → ?); ** #labels_preserved
1065 #related_lin_stm_graph_stm
1066 
1067 inversion (stmt_implicit_label ???)
1068 [ whd in match (opt_All ???); #stmt_implicit_spec #_
1069   letin st2_opt' ≝ (eval_state …
1070               (ev_genv (lin_prog_params … lin_prog lin_stack_sizes))
1071               (sigma_state_pc … wf_st1))
1072   cut (∃st2': lin_abstract_status p p' lin_prog lin_stack_sizes. st2_opt' = return st2')
1073   [cases daemon (* TODO, needs lemma? *)] * #st2' #st2_spec'
1074   normalize nodelta in st2_spec'; -st2_opt'
1075   %{st2'} %{(taaf_step … (taa_base …) …)}
1076   [ cases daemon (* TODO, together with the previous one? *)
1077   | @st2_spec' ]
1078   %[%] [%]
1079   [ whd whd in match eval_state in st2_spec'; normalize nodelta in st2_spec';
1080     >(fetch_statement_sigma_commute … good … fetch_statement_spec) in st2_spec';
1081     >m_return_bind
1082     (* Case analysis over the possible statements *)
1083     inversion graph_stmt in stmt_implicit_spec; normalize nodelta
1084     [ #stmt #lbl #_ #abs @⊥ normalize in abs; destruct(abs) ]
1085     XXXXXXXXXX siamo qua, caso GOTO e RETURN
1086   | cases daemon (* TODO, after the definition of label_rel, trivial *) ]
1087   ]
1088 | ....
1089qed.
1090
1091
1092
1093
1094
1095[ *
1096  [ *
1097    [ letin C_COMMENT ≝ 0 in ⊢ ?; #c
1098    | letin C_COST_LABEL ≝ 0 in ⊢ ?; #lbl
1099    | letin C_MOVE       ≝ 0 in ⊢ ?; #move_sig
1100    | letin C_POP        ≝ 0 in ⊢ ?; #a
1101    | letin C_PUSH       ≝ 0 in ⊢ ?; #a
1102    | letin C_ADDRESS    ≝ 0 in ⊢ ?; #sy #sy_prf #dpl #dph
1103    | letin C_OPACCS     ≝ 0 in ⊢ ?; #op #a #b #arg1 #arg2
1104    | letin C_OP1        ≝ 0 in ⊢ ?; #op #a #arg
1105    | letin C_OP2        ≝ 0 in ⊢ ?; #op #a #arg1 #arg2
1106    | letin C_CLEAR_CARRY ≝ 0 in ⊢ ?;
1107    | letin C_SET_CARRY  ≝ 0 in ⊢ ?;
1108    | letin C_LOAD       ≝ 0 in ⊢ ?; #a #dpl #dph
1109    | letin C_STORE      ≝ 0 in ⊢ ?; #dpl #dph #a
1110    | letin C_CALL       ≝ 0 in ⊢ ?; #f #args #dest
1111    | letin C_EXT        ≝ 0 in ⊢ ?; #s_ext
1112    ]
1113  | letin C_COND ≝ 0 in ⊢ ?; #a #lbltrue
1114  ] #next change with label in next;
1115| *
1116  [ letin C_GOTO ≝ 0 in ⊢ ?; #lbl
1117  | letin C_RETURN ≝ 0 in ⊢ ?;
1118  | letin C_TAILCALL ≝ 0 in ⊢ ?; #fl #f #args
1119  ]
1120]
Note: See TracBrowser for help on using the repository browser.