source: src/joint/lineariseProof.ma @ 2495

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

continuing lineariseProof

File size: 56.6 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
138definition sigma_is_opt :
139 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
140  ((Σi.is_internal_function_of_program … graph_prog i) →
141    code_point (mk_graph_params p) → option ℕ) →
142  internal_stack → option internal_stack ≝
143λp,p',graph_prog,sigma,is.
144match is with
145[ empty_is ⇒ return empty_is
146| one_is bv ⇒ ! bv' ← sigma_beval_opt p p' … sigma bv ; return one_is bv'
147| both_is bv1 bv2 ⇒
148  ! bv1' ← sigma_beval_opt p p' … sigma bv1 ;
149  ! bv2' ← sigma_beval_opt p p' … sigma bv2 ;
150  return both_is bv1' bv2'
151].
152
153definition sigma_is :
154 ∀p,p',graph_prog,sigma,is.
155 sigma_is_opt p p' graph_prog sigma is ≠ None ? → internal_stack ≝
156 λp,p',graph_prog,sigma,is.opt_safe ….
157
158lemma sigma_is_pop_commute :
159 ∀p,p',graph_prog,sigma,is,bv,is'.
160 ∀prf : sigma_is_opt p p' graph_prog sigma is ≠ None ?.
161 is_pop is = return 〈bv, is'〉 →
162 ∃prf' : sigma_beval_opt p p' graph_prog sigma bv ≠ None ?.
163 ∃prf'' : sigma_is_opt p p' graph_prog sigma is' ≠ None ?.
164 is_pop (sigma_is … prf) = return 〈sigma_beval … prf', sigma_is … prf''〉.
165cases daemon qed.
166
167definition well_formed_mem :
168 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
169  ((Σi.is_internal_function_of_program … graph_prog i) →
170    code_point (mk_graph_params p) → option ℕ) →
171 bemem → Prop ≝
172λp,p',graph_prog,sigma,m.
173∀b,z.block_id b < nextblock m → low_bound m b ≤ z → z < high_bound m b →
174  sigma_beval_opt p p' graph_prog sigma (contents (blocks m b) z) ≠ None ?.
175
176definition sigma_mem :
177 ∀p,p',graph_prog,sigma,m.
178 well_formed_mem p p' graph_prog sigma m →
179 bemem ≝
180 λp,p',graph_prog,sigma,m,prf.
181 mk_mem
182  (λb.
183    If Zltb (block_id b) (nextblock m) then with prf' do   
184      let l ≝ low_bound m b in
185      let h ≝ high_bound m b in
186      mk_block_contents l h
187      (λz.If Zleb l z ∧ Zltb z h then with prf'' do
188        sigma_beval p p' graph_prog sigma (contents (blocks m b) z) ?
189      else BVundef)
190    else empty_block OZ OZ)
191  (nextblock m)
192  (nextblock_pos m).
193@hide_prf
194lapply prf'' lapply prf' -prf' -prf''
195@Zltb_elim_Type0 [2: #_ * ]
196#bid_ok *
197@Zleb_elim_Type0 [2: #_ * ]
198@Zltb_elim_Type0 [2: #_ #_ * ]
199#zh #zl * @(prf … bid_ok zl zh)
200qed.
201
202lemma beloadv_sigma_commute:
203∀p,p',graph_prog,sigma,m,ptr,bv,prf1.
204beloadv m ptr = return bv →
205∃ prf2.
206beloadv (sigma_mem p p' graph_prog sigma m prf1) ptr =
207               return sigma_beval p p' graph_prog sigma bv prf2.
208#p #p' #graph_prog #sigma #m #ptr #bv #prf1
209whd in match beloadv in ⊢ (%→?); normalize nodelta
210whd in match do_if_in_bounds in ⊢ (%→?); normalize nodelta
211@Zltb_elim_Type0 normalize nodelta [2: #_ #EQ whd in EQ : (??%%); destruct(EQ)]
212#block_id_ok
213@Zleb_elim_Type0 normalize nodelta [2: #_ #EQ whd in EQ : (??%%); destruct(EQ)]
214#zh
215@Zltb_elim_Type0 normalize nodelta [2: #_ #EQ whd in EQ : (??%%); destruct(EQ)]
216#zl #EQ whd in EQ : (???%); destruct(EQ)
217% [ @(prf1 ?? block_id_ok zh zl) ]
218whd in match beloadv; normalize nodelta
219whd in match do_if_in_bounds; normalize nodelta
220@Zltb_elim_Type0 normalize nodelta [2: * #ABS @⊥ @ABS assumption]
221#block_id_lin_ok
222@Zleb_elim_Type0 normalize nodelta
223[
224| * #ABS @⊥ @ABS whd in match sigma_mem; normalize nodelta
225
226lemma bestorev_sigma_commute :
227∀p,p',graph_prog,sigma,m,ptr,bv,m',prf1,prf2.
228bestorev m ptr bv = return m' →
229∃prf3.
230bestorev (sigma_mem p p' graph_prog sigma m prf1)
231          ptr
232          (sigma_beval p p' graph_prog sigma bv prf2)
233=
234return (sigma_mem p p' graph_prog sigma m' prf3).
235cases daemon qed.
236
237record good_sem_state_sigma
238  (p : unserialized_params)
239  (p' : ∀F.sem_unserialized_params p F) (graph_prog : ?)
240 (sigma : (Σi.is_internal_function_of_program (joint_closed_internal_function (mk_graph_params p))
241    graph_prog i) →
242      label → option ℕ) : Type[0] ≝
243{ well_formed_frames : framesT (make_sem_graph_params p p') → Prop
244; sigma_frames : ∀frms.well_formed_frames frms → framesT (make_sem_lin_params p p')
245; sigma_empty_frames_commute :
246  ∃prf.
247  empty_framesT (make_sem_lin_params p p') =
248  sigma_frames (empty_framesT (make_sem_graph_params p p')) prf
249
250; well_formed_regs : regsT (make_sem_graph_params p p') → Prop
251; sigma_regs : ∀regs.well_formed_regs regs → regsT (make_sem_lin_params p p')
252; sigma_empty_regsT_commute :
253  ∀ptr.∃ prf.
254  empty_regsT (make_sem_lin_params p p') ptr =
255  sigma_regs (empty_regsT (make_sem_graph_params p p') ptr) prf
256; sigma_load_sp_commute :
257  ∀reg,ptr.
258  load_sp (make_sem_graph_params p p') reg = return ptr →
259  ∃prf.
260  load_sp (make_sem_lin_params p p') (sigma_regs reg prf) = return ptr
261; sigma_save_sp_commute :
262  ∀reg,ptr,prf1. ∃prf2.
263  save_sp (make_sem_lin_params p p') (sigma_regs reg prf1) ptr =
264  sigma_regs (save_sp (make_sem_graph_params p p') reg ptr) prf2
265}.
266
267definition well_formed_state :
268 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
269 ∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) →
270    code_point (mk_graph_params p) → option ℕ).
271 good_sem_state_sigma p p' graph_prog sigma →
272 state (make_sem_graph_params p p') → Prop ≝
273λp,p',graph_prog,sigma,gsss,st.
274well_formed_frames … gsss (st_frms … st) ∧
275sigma_is_opt p p' graph_prog sigma (istack … st) ≠ None ? ∧
276well_formed_regs … gsss (regs … st) ∧
277well_formed_mem p p' graph_prog sigma (m … st).
278
279definition sigma_state :
280 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
281 ∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) →
282    code_point (mk_graph_params p) → option ℕ).
283 ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
284 ∀st : state (make_sem_graph_params p p').
285 well_formed_state … gsss st →
286 state (make_sem_lin_params p p') ≝
287λp,p',graph_prog,sigma,gsss,st,prf.
288mk_state …
289  (sigma_frames … gsss (st_frms … st) (proj1 … (proj1 … (proj1 … prf))))
290  (sigma_is p p' graph_prog sigma (istack … st) (proj2 … (proj1 … (proj1 … prf))))
291  (carry … st)
292  (sigma_regs … gsss (regs … st) (proj2 … (proj1 … prf)))
293  (sigma_mem p p' graph_prog sigma (m … st) (proj2 … prf)).
294
295
296(*
297lemma sigma_is_pop_wf :
298 ∀p,p',graph_prog,sigma,is,bv,is'.
299 is_pop is = return 〈bv, is'〉 →
300 sigma_is_opt p p' graph_prog sigma is ≠ None ? →
301 sigma_beval_opt p p' graph_prog sigma bv ≠ None ? ∧
302 sigma_is_opt p p' graph_prog sigma is' ≠ None ?.
303cases daemon qed.
304*)
305
306(*
307lemma prova : ∀p,s,st,prf.sigma_pc_of_status p s st prf = ?.
308[ #p #s #st #prf
309  whd in match sigma_pc_of_status; normalize nodelta
310  @opt_safe_elim
311  #n
312  lapply (refl …  (int_funct_of_block (joint_closed_internal_function p) (globals p)
313        (ev_genv p) (pblock (pc p st))))
314  elim (int_funct_of_block (joint_closed_internal_function p) (globals p)
315        (ev_genv p) (pblock (pc p st))) in ⊢ (???%→%);
316  [ #_ #ABS normalize in ABS; destruct(ABS) ]
317  #f #EQ >m_return_bind
318*)
319
320
321(*
322lemma wf_status_to_wf_pc :
323∀p,p',graph_prog,stack_sizes.
324∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) →
325    code_point (mk_graph_params p) → option ℕ).
326∀st.
327well_formed_status p p' graph_prog stack_sizes sigma st →
328well_formed_pc p p' graph_prog stack_sizes sigma (pc ? st).
329#p #p' #graph_prog #stack_sizes #sigma #st whd in ⊢ (% → ?); * #H #_ @H
330qed.
331 *)
332 definition sigma_pc :
333∀p,p',graph_prog.
334∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) →
335    label → option ℕ).
336∀pc.
337∀prf : well_formed_pc p p' graph_prog sigma pc.
338program_counter ≝
339λp,p',graph_prog,sigma,st.opt_safe ….
340 
341lemma sigma_pc_ok:
342  ∀p,p',graph_prog.
343  ∀sigma.
344   ∀pc.
345    ∀prf:well_formed_pc p p' graph_prog sigma pc.
346    sigma_pc_opt p p' graph_prog sigma pc =
347    Some … (sigma_pc p p' graph_prog sigma pc prf).
348    #p #p' #graph_prog #sigma #st #prf @opt_to_opt_safe qed.
349
350definition well_formed_state_pc :
351 ∀p,p',graph_prog,sigma.
352  good_sem_state_sigma p p' graph_prog sigma →
353  state_pc (make_sem_graph_params p p') → Prop ≝
354 λp,p',prog,sigma,gsss,st.
355 well_formed_pc p p' prog sigma (pc … st) ∧ well_formed_state … gsss st.
356 
357definition sigma_state_pc :
358 ∀p.
359 ∀p':∀F.sem_unserialized_params p F.
360 ∀graph_prog.
361  ∀sigma.
362(*   let lin_prog ≝ linearise ? graph_prog in *)
363  ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
364    ∀s:state_pc (make_sem_graph_params p p'). (* = graph_abstract_status p p' graph_prog stack_sizes *)
365     well_formed_state_pc p p' graph_prog sigma gsss s →
366      state_pc (make_sem_lin_params p p') (* = lin_abstract_status p p' lin_prog ? *)
367
368 λp,p',graph_prog,sigma,gsss,s,prf.
369 let pc' ≝ sigma_pc … (proj1 … prf) in
370 let st' ≝ sigma_state … (proj2 … prf) in
371 mk_state_pc ? st' pc'.
372
373definition sigma_function_name :
374 ∀p,graph_prog.
375 let lin_prog ≝ linearise p graph_prog in
376  (Σf.is_internal_function_of_program … graph_prog f) →
377  (Σf.is_internal_function_of_program … lin_prog f) ≝
378λp,graph_prog,f.«f, if_propagate … (pi2 … f)».
379
380lemma m_list_map_All_ok :
381  ∀M : MonadProps.∀X,Y,f,l.
382  All X (λx.∃y.f x = return y) l → ∃l'.m_list_map M X Y f l = return l'.
383  cases daemon qed.
384
385(*
386inductive isMember (A : Type[0]) (x : A) : list A → Prop ≝
387 | isMemberHead : ∀ tl.isMember A x (x :: tl)
388 | isMemberTail : ∀ y,tl .isMember A x tl → isMember A x (y :: tl).
389(*
390definition lift_f_tail : ∀ A,B : Type[0]. ∀ l ,tl : list A. ∀y : A . l = y ::tl →
391      (∀ x : A. isMember A x l → B) → ∀ x : A. isMember A x tl → B.
392      #A #B #l #tl #y #l_spec #f #x #tl_member @f [//]
393    @(isMemberTail ? x y l tl l_spec tl_member)
394    qed.
395  *)             
396
397let rec ext_map (A,B : Type[0]) (l : list A) (f : ∀ x : A. isMember A x l → B) on l : list B ≝
398match l with [ nil ⇒ λprf : l = nil ?.nil ?
399             | cons x tl ⇒ λprf : l = cons ? x tl.
400              f x ? :: ext_map ?? tl (λy,prf'.f y ?)
401             ] (refl …).
402@hide_prf
403>prf
404[ %1
405| %2 assumption
406] qed.
407              (f x (isMemberHead A x l tl prf)) ::   
408              ext_map A B tl (lift_f_tail A B l tl x prf f) ]
409              (refl ? l).
410*)
411
412definition helper_def_store__commute :
413  ∀p,p',graph_prog,sigma.
414  ∀X : ? → Type[0].
415  ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
416  ∀store : ∀p,F.∀p' : sem_unserialized_params p F.
417    X p → beval → regsT p' →
418    res (regsT p').
419  Prop ≝
420  λp,p',graph_prog,sigma,X,gsss,store.
421  ∀a : X ?.∀bv,r,r',prf1,prf1'.
422  store … a bv r = return r' →
423  ∃prf2.
424  store ??? a
425    (sigma_beval p p' graph_prog sigma bv prf1')
426    (sigma_regs ???? gsss r prf1) = return sigma_regs … gsss r' prf2.
427
428definition helper_def_retrieve__commute :
429  ∀p,p',graph_prog,sigma.
430  ∀X : ? → Type[0].
431  ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
432  ∀retrieve : ∀p,F.∀p' : sem_unserialized_params p F.
433    regsT p' → X p → res beval.
434  Prop ≝
435  λp,p',graph_prog,sigma,X,gsss,retrieve.
436  ∀a : X p.∀r,bv,prf1.
437  retrieve … r a = return bv →
438  ∃prf2.
439  retrieve … (sigma_regs … gsss r prf1) a
440     = return sigma_beval p p' graph_prog sigma bv prf2.
441 
442record good_state_sigma
443  (p : unserialized_params)
444  (p' : ∀F.sem_unserialized_params p F) (graph_prog : ?)
445 (sigma : (Σi.is_internal_function_of_program (joint_closed_internal_function (mk_graph_params p))
446    graph_prog i) →
447      label → option ℕ)
448: Type[0] ≝
449{ gsss :> good_sem_state_sigma p p' graph_prog sigma
450
451; acca_store__commute : helper_def_store__commute … gsss acca_store_
452
453; acca_retrieve_commute : helper_def_retrieve__commute … gsss acca_retrieve_
454
455}.
456
457lemma store_commute :
458  ∀p,p',graph_prog,sigma.
459  ∀X : ? → Type[0].
460  ∀store.
461  ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
462  ∀H : helper_def_store__commute … gsss store.
463  ∀a : X p.∀bv,st,st',prf1,prf1'.
464  helper_def_store ? store … a bv st = return st' →
465  ∃prf2.
466  helper_def_store ? store … a
467    (sigma_beval p p' graph_prog sigma bv prf1')
468    (sigma_state … gsss st prf1) = return sigma_state … gsss st' prf2.
469cases daemon qed.
470
471lemma retrieve_commute :
472 ∀p,p',graph_prog,sigma.
473 ∀X : ? → Type[0].
474 ∀retrieve.
475 ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
476 ∀H : helper_def_retrieve__commute … gsss retrieve.
477 ∀a : X p .∀st,bv,prf1.
478 helper_def_retrieve ? retrieve … st a = return bv →
479 ∃prf2.
480     helper_def_retrieve ? retrieve … (sigma_state … gsss st prf1) a =
481     return sigma_beval p p' graph_prog sigma bv prf2.
482cases daemon qed.
483
484(*
485definition acca_store_commute :
486  ∀p,p',graph_prog,sigma.
487  ∀gss : good_state_sigma p p' graph_prog sigma.
488  ∀a : acc_a_reg p.∀bv,st,st',prf1,prf1'.
489  acca_store … a bv st = return st' →
490  ∃prf2.
491  acca_store … a
492    (sigma_beval p p' graph_prog sigma bv prf1')
493    (sigma_state … gss st prf1) = return sigma_state … gss st' prf2
494 ≝
495λp,p',graph_prog,sigma.
496λgss : good_state_sigma p p' graph_prog sigma.
497store_commute … gss (acca_store__commute … gss).*)
498 
499   
500lemma acca_store_commute :
501  ∀p,p',graph_prog,sigma.
502  ∀gss : good_state_sigma p p' graph_prog sigma.
503  ∀a,bv,st,st',prf1,prf1'.
504  acca_store ?? (p' ?) a bv st = return st' →
505  ∃prf2.
506  acca_store ?? (p' ?) a
507    (sigma_beval p p' graph_prog sigma bv prf1')
508    (sigma_state … gss st prf1) = return sigma_state … gss st' prf2 ≝
509λp,p',graph_prog,sigma,gss,a,bv.?.
510* #frms #is #carry #regs #m
511* #frms' #is' #carry' #regs' #m'
512*** #frms_ok #is_ok #regs_ok #mem_ok
513#bv_ok #EQ1 elim (bind_inversion ????? EQ1)
514#regs'' * -EQ1 #EQ1 whd in ⊢ (??%%→?); #EQ destruct(EQ)
515elim (acca_store__commute … gss … EQ1)
516[ #prf2 #EQ2
517  % [ whd /4 by conj/ ]
518  change with (! r ← ? ; ? = ?) >EQ2
519  whd in match (sigma_state ???????); normalize nodelta
520   >m_return_bind
521
522
523st,st',prf1,prf2,prf3.?.
524
525
526#p #p' #
527(*
528; acca_store_wf :  ∀a,bv,st,st'.
529  sigma_beval_opt p p' graph_prog sigma bv ≠ None ? →
530  acca_store ?? (p' ?) a bv st = return st' →
531  well_formed_state st → well_formed_state st'
532
533; acca_retrieve_wf :  ∀a,st,bv.
534  acca_retrieve ?? (p' ?) st a = return bv →
535  well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?
536
537; acca_arg_retrieve_ok :
538  ∀a,st,bv,prf1,prf2.
539  acca_arg_retrieve ?? (p' ?) st a = return bv →
540  acca_arg_retrieve ?? (p' ?) (sigma_state st prf1) a =
541  return sigma_beval p p' graph_prog sigma bv prf2
542; acca_arg_retrieve_wf :  ∀a,st,bv.
543  acca_arg_retrieve ?? (p' ?) st a = return bv →
544  well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?
545
546; accb_store_ok :
547  ∀a,bv,bv',st,st',prf1,prf2.
548  sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
549  accb_store ?? (p' ?) a bv st = return st' →
550  accb_store … (p' ?) a bv' (sigma_state st prf1) = return sigma_state st' prf2
551; accb_store_wf :  ∀a,bv,bv',st,st'.
552  sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
553  accb_store ?? (p' ?) a bv st = return st' →
554  well_formed_state st → well_formed_state st'
555
556; accb_retrieve_ok :
557  ∀a,st,bv,prf1,prf2.
558  accb_retrieve ?? (p' ?) st a = return bv →
559  accb_retrieve ?? (p' ?) (sigma_state st prf1) a =
560  return sigma_beval p p' graph_prog sigma bv prf2
561; accb_retrieve_wf :  ∀a,st,bv.
562  accb_retrieve ?? (p' ?) st a = return bv →
563  well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?
564
565; accb_arg_retrieve_ok :
566  ∀a,st,bv,prf1,prf2.
567  acca_arg_retrieve ?? (p' ?) st a = return bv →
568  acca_arg_retrieve ?? (p' ?) (sigma_state st prf1) a =
569  return sigma_beval p p' graph_prog sigma bv prf2
570; accb_arg_retrieve_wf :  ∀a,st,bv.
571  accb_arg_retrieve ?? (p' ?) st a = return bv →
572  well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?
573
574
575; dpl_store_ok :
576  ∀a,bv,bv',st,st',prf1,prf2.
577  sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
578  dpl_store ?? (p' ?) a bv st = return st' →
579  dpl_store … (p' ?) a bv' (sigma_state st prf1) = return sigma_state st' prf2
580; dpl_store_wf :  ∀a,bv,bv',st,st'.
581  sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
582  dpl_store ?? (p' ?) a bv st = return st' →
583  well_formed_state st → well_formed_state st'
584
585; dpl_retrieve_ok :
586  ∀a,st,bv,prf1,prf2.
587  dpl_retrieve ?? (p' ?) st a = return bv →
588  dpl_retrieve ?? (p' ?) (sigma_state st prf1) a =
589  return sigma_beval p p' graph_prog sigma bv prf2
590; dpl_retrieve_wf :  ∀a,st,bv.
591  dpl_retrieve ?? (p' ?) st a = return bv →
592  well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?
593
594; dpl_arg_retrieve_ok :
595  ∀a,st,bv,prf1,prf2.
596  acca_arg_retrieve ?? (p' ?) st a = return bv →
597  acca_arg_retrieve ?? (p' ?) (sigma_state st prf1) a =
598  return sigma_beval p p' graph_prog sigma bv prf2
599; dpl_arg_retrieve_wf :  ∀a,st,bv.
600  dpl_arg_retrieve ?? (p' ?) st a = return bv →
601  well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?
602
603
604; dph_store_ok :
605  ∀a,bv,bv',st,st',prf1,prf2.
606  sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
607  dph_store ?? (p' ?) a bv st = return st' →
608  dph_store … (p' ?) a bv' (sigma_state st prf1) = return sigma_state st' prf2
609; dph_store_wf :  ∀a,bv,bv',st,st'.
610  sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' →
611  dph_store ?? (p' ?) a bv st = return st' →
612  well_formed_state st → well_formed_state st'
613
614; dph_retrieve_ok :
615  ∀a,st,bv,prf1,prf2.
616  dph_retrieve ?? (p' ?) st a = return bv →
617  dph_retrieve ?? (p' ?) (sigma_state st prf1) a =
618  return sigma_beval p p' graph_prog sigma bv prf2
619; dph_retrieve_wf :  ∀a,st,bv.
620  dph_retrieve ?? (p' ?) st a = return bv →
621  well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?
622
623; dph_arg_retrieve_ok :
624  ∀a,st,bv,prf1,prf2.
625  acca_arg_retrieve ?? (p' ?) st a = return bv →
626  acca_arg_retrieve ?? (p' ?) (sigma_state st prf1) a =
627  return sigma_beval p p' graph_prog sigma bv prf2
628; dph_arg_retrieve_wf :  ∀a,st,bv.
629  dph_arg_retrieve ?? (p' ?) st a = return bv →
630  well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?
631
632
633; snd_arg_retrieve_ok :
634  ∀a,st,bv,prf1,prf2.
635  snd_arg_retrieve ?? (p' ?) st a = return bv →
636  snd_arg_retrieve ?? (p' ?) (sigma_state st prf1) a =
637  return sigma_beval p p' graph_prog sigma bv prf2
638; snd_arg_retrieve_wf :  ∀a,st,bv.
639  snd_arg_retrieve ?? (p' ?) st a = return bv →
640  well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?
641
642; pair_reg_move_ok :
643  ∀mv,st1,st2,prf1,prf2.
644  pair_reg_move ?? (p' ?) st1 mv = return st2 →
645  pair_reg_move ?? (p' ?) (sigma_state st1 prf1) mv =
646    return sigma_state st2 prf2
647; pair_reg_move_wf :
648  ∀mv,st1,st2.
649  pair_reg_move ?? (p' ?) st1 mv = return st2 →
650  well_formed_state st1 → well_formed_state st2
651
652; allocate_locals_ok :
653  ∀l,st1,prf1,prf2.
654  allocate_locals ?? (p' ?) l (sigma_state st1 prf1) =
655    sigma_state (allocate_locals ?? (p' ?) l st1) prf2
656; allocate_locals_wf :
657  ∀l,st1.
658  well_formed_state st1 →
659    well_formed_state (allocate_locals ?? (p' ?) l st1)
660
661; save_frame_ok :
662  ∀dest,st1,st2,prf1,prf2.
663  save_frame ?? (p' ?) dest st1 = return st2 →
664  let st1' ≝ mk_state_pc … (sigma_state st1 (proj2 … prf1))
665    (sigma_pc p p' graph_prog sigma (pc … st1) (proj1 … prf1)) in
666  save_frame ?? (p' ?) dest st1' = return sigma_state st2 prf2
667; save_frame_wf :
668  ∀dest,st1,st2.
669  save_frame ?? (p' ?) dest st1 = return st2 →
670  (well_formed_pc p p' graph_prog sigma (pc … st1) ∧
671   well_formed_state st1) → well_formed_state st2
672
673; eval_ext_seq_ok :
674  let lin_prog ≝ linearise p graph_prog in
675  ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
676  let stack_sizes' ≝
677   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
678     ? graph_prog stack_sizes in
679  ∀ext,fn,st1,st2,prf1,prf2.
680  eval_ext_seq ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes'))
681    ext fn st1 = return st2 →
682  eval_ext_seq ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
683    ext (sigma_function_name … fn) (sigma_state st1 prf1) = return sigma_state st2 prf2
684; eval_ext_seq_wf :
685  let lin_prog ≝ linearise p graph_prog in
686  ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
687  let stack_sizes' ≝
688   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
689     ? graph_prog stack_sizes in
690  ∀ext,fn,st1,st2.
691  eval_ext_seq ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes'))
692    ext fn st1 = return st2 →
693  well_formed_state st1 → well_formed_state st2
694
695; setup_call_ok :
696  ∀ n , parsT, call_args , st1 , st2 , prf1, prf2.
697  setup_call ?? (p' ?) n parsT call_args st1 = return st2 →
698  setup_call ?? (p' ?) n parsT call_args (sigma_state st1 prf1) =
699  return (sigma_state st2 prf2)
700; setup_call_wf :
701  ∀ n , parsT, call_args , st1 , st2.
702  setup_call ?? (p' ?) n parsT call_args st1 = return st2 →
703  well_formed_state st1 → well_formed_state st2
704 
705; fetch_external_args_ok : (* TO BE CHECKED *)
706  ∀ex_fun,st1,prf1,call_args.
707  fetch_external_args ?? (p' ?) ex_fun st1 call_args =
708  fetch_external_args ?? (p' ?) ex_fun (sigma_state st1 prf1) call_args
709; fetch_external_args_wf :
710  ∀ex_fun,st1,call_args.
711  well_formed_state st1 → ∃ l.
712  fetch_external_args ?? (p' ?) ex_fun st1 call_args = OK ? l
713 
714; set_result_ok :
715  ∀ l , call_dest , st1 , st2 , prf1 , prf2 .
716  set_result ?? (p' ?) l call_dest st1 = return st2 →
717  set_result ?? (p' ?) l call_dest (sigma_state st1 prf1) =
718  return (sigma_state st2 prf2)
719; set_result_wf :
720  ∀ l , call_dest , st1 , st2  .
721  set_result ?? (p' ?) l call_dest st1 = return st2 →
722  well_formed_state st1 → well_formed_state st2 
723 
724; read_result_ok :
725  let lin_prog ≝ linearise p graph_prog in
726  ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
727  let stack_sizes' ≝
728   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
729     ? graph_prog stack_sizes in
730  ∀call_dest , st1 , prf1, l1.
731  read_result ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes'))
732    call_dest st1 = return l1 →
733  ∀prf : m_list_map … (sigma_beval_opt p p' graph_prog sigma) l1 ≠ None ?.
734  read_result ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
735    call_dest (sigma_state st1 prf1) = return opt_safe … prf
736; read_result_wf :
737  let lin_prog ≝ linearise p graph_prog in
738  ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
739  let stack_sizes' ≝
740   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
741     ? graph_prog stack_sizes in
742  ∀call_dest , st1 , l1.
743  read_result ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes'))
744    call_dest st1 = return l1 →
745  well_formed_state st1 →
746  m_list_map … (sigma_beval_opt p p' graph_prog sigma) l1 ≠ None ?
747 
748; pop_frame_ok :
749  let lin_prog ≝ linearise p graph_prog in
750  ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
751  let stack_sizes' ≝
752   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
753     ? graph_prog stack_sizes in
754  ∀ st1 , prf1, curr_id ,st2, prf2.
755  pop_frame ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes'))
756            curr_id st1 = return st2 →
757 let pc' ≝ sigma_pc p p' graph_prog sigma (pc ? st2) (proj1 … prf2) in
758 let st2' ≝ sigma_state (st_no_pc ? st2) (proj2 … prf2) in
759  pop_frame ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
760            (sigma_function_name p graph_prog curr_id) (sigma_state st1 prf1) =
761            return mk_state_pc ? st2' pc'
762; pop_frame_wf :
763  let lin_prog ≝ linearise p graph_prog in
764  ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
765  let stack_sizes' ≝
766   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
767     ? graph_prog stack_sizes in
768  ∀ st1, curr_id ,st2.
769  pop_frame ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes'))
770            curr_id st1 = return st2 →
771  well_formed_state st1 → well_formed_pc p p' graph_prog sigma (pc ? st2) ∧
772      well_formed_state (st_no_pc ? st2)
773}.
774
775(* restano:
776; setup_call : nat → paramsT … uns_pars → call_args uns_pars →
777    state st_pars → res (state st_pars)
778; fetch_external_args: external_function → state st_pars → call_args … uns_pars →
779    res (list val)
780; set_result: list val → call_dest uns_pars → state st_pars → res (state st_pars)
781
782(* from now on, parameters that use the type of functions *)
783; read_result: ∀globals.genv_gen F globals → call_dest uns_pars → state st_pars → res (list beval)
784(* change of pc must be left to *_flow execution *)
785; pop_frame: ∀globals.∀ge : genv_gen F globals.
786  (Σi.is_internal_function … ge i) (* current *) → state st_pars → res (state st_pars)
787*)
788*)
789
790(*
791lemma sigma_pc_commute:
792 ∀p,p',graph_prog,sigma,gss,st.
793 ∀prf : well_formed_state_pc p p' graph_prog sigma gss st.
794 sigma_pc … (pc ? st) (proj1 … prf) =
795 pc ? (sigma_state_pc … st prf). // qed.
796*)
797
798lemma res_eq_from_opt :
799  ∀A,m,v.res_to_opt A m = return v → m = return v.
800#A * #x #v normalize #EQ destruct % qed.
801
802lemma if_of_function_commute:
803 ∀p.
804 ∀graph_prog : joint_program (mk_graph_params p).
805 ∀graph_fun : Σi.is_internal_function_of_program … graph_prog i.
806 let graph_fd ≝ if_of_function … graph_fun in
807 let lin_fun ≝ sigma_function_name … graph_fun in
808 let lin_fd ≝ if_of_function … lin_fun in
809 lin_fd = \fst (linearise_int_fun ?? graph_fd).
810 #p #graph_prog #graph_fun whd
811 @prog_if_of_function_transform % qed.
812
813lemma bind_opt_inversion:
814  ∀A,B: Type[0]. ∀f: option A. ∀g: A → option B. ∀y: B.
815  (! x ← f ; g x = Some … y) →
816  ∃x. (f = Some … x) ∧ (g x = Some … y).
817#A #B #f #g #y cases f normalize
818[ #H destruct (H)
819| #a #e %{a} /2 by conj/
820] qed.
821
822lemma sigma_pblock_eq_lemma :
823∀p,p',graph_prog.
824let lin_prog ≝ linearise p graph_prog in
825∀sigma,pc.
826∀prf : well_formed_pc p p' graph_prog sigma pc.
827 pc_block (sigma_pc ? p' graph_prog sigma pc prf) =
828 pc_block pc.
829 #p #p' #graph_prog #sigma #pc #prf
830 whd in match sigma_pc; normalize nodelta
831 @opt_safe_elim #x #x_spec
832 whd in x_spec:(??%?); cases (int_funct_of_block ???) in x_spec;
833 normalize nodelta [#abs destruct] #id #H cases (bind_opt_inversion ????? H) -H
834 #offset * #_ whd in ⊢ (??%? → ?); #EQ destruct //
835qed.
836
837(*
838lemma bind_opt_non_none : ∀A,B : Type[0] . ∀ m : option A . ∀g : A → option B.
839(! x ← m ; g x) ≠ None ? → m ≠ None ?.
840#A #B #m #g #H % #m_eq_none cases m >m_eq_none in H; normalize 
841[ #abs elim abs -abs #abs @abs %
842| #abs elim abs -abs #abs #v @abs %
843]
844qed.
845
846lemma match_option_non_none : ∀A ,B, C : Type[0]. ∀m : option A. ∀ x : A.
847∀ b : B .∀ f : A → B. ∀g : B → option C.
848g (match m with [None  ⇒ b  | Some  x ⇒ f x])≠ None ? →  g b = None ? → m ≠ None ?.
849#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
850qed.
851*)
852
853lemma funct_of_block_transf :
854∀A,B.∀progr : program (λvars .fundef (A vars)) ℕ.
855∀transf : ∀vars. A vars → B vars. ∀bl,f,prf.
856let progr' ≝ transform_program … progr (λvars.transf_fundef … (transf vars)) in
857funct_of_block … (globalenv_noinit … progr) bl = return f →
858funct_of_block … (globalenv_noinit … progr') bl = return «pi1 … f,prf».
859#A #B #progr #transf #bl #f #prf whd
860whd in match funct_of_block in ⊢ (%→?); normalize nodelta
861cut (∀A,B : Type[0].∀Q : option A → Prop.∀P : B → Prop.
862  ∀o.∀prf : Q o.
863  ∀f1,f2.
864  (∀x,prf.P (f1 x prf)) → (∀prf.P(f2 prf)) →
865  P (match o return λx.Q x → B with [ Some x ⇒ f1 x | None ⇒ f2 ] prf))
866  [ #A #B #Q #P * /2/ ] #aux
867@aux [2: #_ change with (?=Some ??→?) #ABS destruct(ABS) ]
868#fd #EQfind whd in ⊢ (??%%→?);
869generalize in ⊢ (??(??(????%))?→?); #e #EQ destruct(EQ)
870whd in match funct_of_block; normalize nodelta
871@aux [ # fd' ]
872[2: >(find_funct_ptr_transf … EQfind) #ABS destruct(ABS) ]
873#prf' cases daemon qed.
874
875lemma description_of_function_transf :
876∀A,B.∀progr : program (λvars .fundef (A vars)) ℕ.
877∀transf : ∀vars. A vars → B vars.
878let progr' ≝ transform_program … progr (λvars.transf_fundef … (transf vars)) in
879∀f_out,prf.
880description_of_function …
881  (globalenv_noinit … progr') f_out =
882transf_fundef … (transf ?) (description_of_function … (globalenv_noinit … progr)
883  «pi1 … f_out, prf»).
884#A #B #progr #transf #f_out #prf
885whd in match description_of_function in ⊢ (???%);
886normalize nodelta
887cut (∀A,B : Type[0].∀Q : option A → Prop.∀P : B → Prop.
888  ∀o.∀prf : Q o.
889  ∀f1,f2.
890  (∀x,prf.o = Some ? x → P (f1 x prf)) → (∀prf.o = None ? → P(f2 prf)) →
891  P (match o return λx.Q x → B with [ Some x ⇒ f1 x | None ⇒ f2 ] prf))
892  [ #A #B #Q #P * /2/ ] #aux
893@aux
894[ #fd' ] * #fd #EQ destruct (EQ)
895inversion (find_symbol ???) [ #_ whd in ⊢ (??%?→?); #ABS destruct(ABS) ]
896#bl #EQfind >m_return_bind #EQfindf
897whd in match description_of_function; normalize nodelta
898@aux
899[ #fdo' ] * #fdo #EQ destruct (EQ)
900>find_symbol_transf >EQfind >m_return_bind
901>(find_funct_ptr_transf … EQfindf) #EQ destruct(EQ) %
902qed.
903
904
905lemma match_int_fun :
906∀A,B : Type[0].∀P : B → Prop.
907∀Q : fundef A → Prop.
908∀m : fundef A.
909∀f1 : ∀fd.Q (Internal \ldots  fd) → B.
910∀f2 : ∀fd.Q (External … fd) → B.
911∀prf : Q m.
912(∀fd,prf.P (f1 fd prf)) →
913(∀fd,prf.P (f2 fd prf)) →
914P (match m
915return λx.Q x → ?
916with
917[ Internal fd ⇒ f1 fd
918| External fd ⇒ f2 fd
919] prf).
920#A #B #P #Q * // qed.
921(*)
922 lemma match_int_fun :
923∀A,B : Type[0].∀P : B → Prop.
924∀m : fundef A.
925∀f1 : ∀fd.m = Internal … fd → B.
926∀f2 : ∀fd.m = External … fd → B.
927(∀fd,prf.P (f1 fd prf)) →
928(∀fd,prf.P (f2 fd prf)) →
929P (match m
930return λx.m = x → ?
931with
932[ Internal fd ⇒ f1 fd
933| External fd ⇒ f2 fd
934] (refl …)).
935#A #B #P * // qed.
936*)
937(*
938lemma prova :
939∀ A.∀progr : program (λvars. fundef (A vars)) ℕ.
940∀ M : fundef (A (prog_var_names (λvars:list ident.fundef (A vars)) ℕ progr)).
941∀ f,g,prf1.
942match M return λx.M = x → option (Σi.is_internal_function_of_program ?? progr i) with
943[Internal fn ⇒ λ prf.return «g,prf1 fn prf» |
944External fn ⇒ λprf.None ? ] (refl ? M) = return f → 
945∃ fn. ∃ prf : M = Internal ? fn . f = «g, prf1 fn prf».
946#H1 #H2 #H3 #H4 #H5 #H6
947@match_int_fun
948#fd #EQ #EQ' whd in EQ' : (??%%); destruct
949%[|%[| % ]] qed.
950*)
951
952lemma int_funct_of_block_transf:
953 ∀A,B.∀progr: program (λvars. fundef (A vars)) ℕ.
954  ∀transf: ∀vars. A vars → B vars. ∀bl,f,prf.
955   let progr' ≝ transform_program … progr (λvars.transf_fundef … (transf vars)) in
956     int_funct_of_block ? (globalenv_noinit … progr) bl = return f →
957     int_funct_of_block ? (globalenv_noinit … progr') bl = return «pi1 … f,prf».
958#A #B #progr #transf #bl #f #prf
959whd whd in match int_funct_of_block in ⊢ (??%?→?); normalize nodelta
960#H
961elim (bind_opt_inversion ??? ?? H) -H #x
962* #x_spec
963@match_int_fun [2: #fd #_ #ABS destruct(ABS) ]
964#fd #EQdescr change with (Some ?? = ? → ?) #EQ destruct(EQ)
965whd in match int_funct_of_block; normalize nodelta
966>(funct_of_block_transf … (internal_function_is_function … prf) … x_spec)
967>m_return_bind
968@match_int_fun #fd' #prf' [ % ]
969@⊥ cases x in prf EQdescr prf'; -x #x #x_prf #prf #EQdescr
970>(description_of_function_transf) [2: @x_prf ]
971>EQdescr whd in ⊢ (??%%→?); #ABS destruct qed.
972
973
974lemma fetch_function_sigma_commute :
975 ∀p,p',graph_prog.
976 let lin_prog ≝ linearise p graph_prog in
977 ∀sigma,pc_st,f.
978  ∀prf : well_formed_pc p p' graph_prog sigma pc_st.
979 fetch_function … (globalenv_noinit … graph_prog) pc_st =
980  return f
981→ fetch_function … (globalenv_noinit … lin_prog) (sigma_pc … pc_st prf) =
982  return sigma_function_name … f.
983 #p #p' #graph_prog #sigma #st #f #prf
984 whd in match fetch_function; normalize nodelta
985 >(sigma_pblock_eq_lemma … prf) #H
986 lapply (opt_eq_from_res ???? H) -H #H
987 >(int_funct_of_block_transf ?? graph_prog (λvars,graph_fun.\fst (linearise_int_fun … graph_fun)) ??? H)
988 //
989qed.
990 
991(*
992#H elim (bind_opt_inversion ????? H) -H
993#x * whd in match funct_of_block in ⊢ (%→?); normalize nodelta
994@match_opt_prf_elim
995 #H #H1  whd in H : (??%?);
996cases (   find_funct_ptr
997   (fundef
998    (joint_closed_internal_function
999     (graph_prog_params p p' graph_prog
1000      (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
1001       (linearise_int_fun p) graph_prog stack_sizes))
1002     (globals
1003      (graph_prog_params p p' graph_prog
1004       (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
1005        (linearise_int_fun p) graph_prog stack_sizes)))))
1006   (ev_genv
1007    (graph_prog_params p p' graph_prog
1008     (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
1009      (linearise_int_fun p) graph_prog stack_sizes)))
1010   (pblock (pc (make_sem_graph_params p p') st))) in H; [ 2: normalize #abs destruct
1011 
1012
1013normalize nodelta
1014#H #H1
1015cases (   find_funct_ptr
1016   (fundef
1017    (joint_closed_internal_function
1018     (graph_prog_params p p' graph_prog
1019      (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
1020       (linearise_int_fun p) graph_prog stack_sizes))
1021     (globals
1022      (graph_prog_params p p' graph_prog
1023       (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
1024        (linearise_int_fun p) graph_prog stack_sizes)))))
1025   (ev_genv
1026    (graph_prog_params p p' graph_prog
1027     (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
1028      (linearise_int_fun p) graph_prog stack_sizes)))
1029   (pblock (pc (make_sem_graph_params p p') st))) in H;
1030
1031
1032check find_funct_ptr_transf
1033whd in match int_funct_of_block; normalize nodelta
1034#H elim (bind_inversion ????? H)
1035
1036.. sigma_int_funct_of_block
1037
1038
1039
1040whd in match int_funct_of_block; normalize nodelta
1041elim (bind_inversion ????? H)
1042whd in match int_funct_of_block; normalize nodelta
1043#H elim (bind_inversion ????? H) -H #fn *
1044#H lapply (opt_eq_from_res ???? H) -H
1045#H >(find_funct_ptr_transf … (λglobals.transf_fundef … (linearise_int_fun … globals)) … H)
1046-H #H >m_return_bind cases fn in H; normalize nodelta #arg #EQ whd in EQ:(??%%);
1047destruct //
1048cases daemon
1049qed. *)
1050
1051lemma opt_Exists_elim:
1052 ∀A:Type[0].∀P:A → Prop.
1053  ∀o:option A.
1054   opt_Exists A P o →
1055    ∃v:A. o = Some … v ∧ P v.
1056 #A #P * normalize /3/ *
1057qed.
1058
1059
1060lemma stmt_at_sigma_commute:
1061 ∀p,graph_prog,graph_fun,lbl,pt.
1062 let lin_prog ≝ linearise ? graph_prog in
1063 let lin_fun ≝ sigma_function_name p graph_prog graph_fun in
1064 ∀sigma.good_sigma p graph_prog sigma →
1065 sigma graph_fun lbl = return pt →
1066 ∀stmt.
1067   stmt_at …
1068    (joint_if_code ?? (if_of_function ?? graph_fun)) 
1069    lbl = return stmt →
1070   stmt_at ??
1071    (joint_if_code ?? (if_of_function ?? lin_fun))
1072    pt = return (graph_to_lin_statement … stmt). 
1073 #p #graph_prog #graph_fun #lbl #pt #sigma #good #prf #stmt
1074cases (good graph_fun (pi2 … (sigma_function_name p graph_prog graph_fun)))
1075#sigma_entry_is_zero #lin_stmt_spec
1076lapply (lin_stmt_spec lbl pt prf) -lin_stmt_spec * #stmt1 *
1077#EQlookup_stmt1 #H
1078elim (opt_Exists_elim … H) -H * #optlbl_graph_stmt #graph_stmt
1079* #EQnth_opt_graph_stmt normalize nodelta
1080* #optEQlbl_optlbl_graph_stmt #next_spec
1081whd in match (stmt_at ????) in ⊢ (% → ?);
1082normalize nodelta
1083>EQlookup_stmt1 whd in ⊢ ((???%) → ?); #EQ destruct(EQ)
1084whd in match (stmt_at ????); > EQnth_opt_graph_stmt
1085normalize nodelta elim  optEQlbl_optlbl_graph_stmt #_ #EQ >EQ //
1086qed.
1087(*
1088
1089 >(if_of_function_commute … graph_fun)
1090
1091check opt_Exists
1092check linearise_int_fun
1093check
1094 whd in match (stmt_at ????);
1095 whd in match (stmt_at ????);
1096 cases (linearise_code_spec … p' graph_prog graph_fun
1097         (joint_if_entry … graph_fun))
1098 * #lin_code_closed #sigma_entry_is_zero #sigma_spec
1099 lapply (sigma_spec
1100         (point_of_pointer ? (graph_prog_params … p' graph_prog) (pc … s1)))
1101 -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @(sigma_pc_of_status_ok … prf) |2: skip ]
1102 -sigma_spec #graph_stmt * #graph_lookup_ok >graph_lookup_ok -graph_lookup_ok
1103 whd in ⊢ (? → ???%); #sigma_spec whd in sigma_spec;
1104 inversion (nth_opt ???) in sigma_spec; [ #H whd in ⊢ (% → ?); #abs cases abs ]
1105 * #optlabel #lin_stm #lin_lookup_ok whd in ⊢ (% → ?); ** #_
1106 #related_lin_stm_graph_stm #_ <related_lin_stm_graph_stm -related_lin_stm_graph_stm
1107 <sigma_pc_commute >lin_lookup_ok // *)
1108
1109lemma fetch_statement_sigma_commute:
1110  ∀p,p',graph_prog,pc,fn,stmt.
1111  let lin_prog ≝ linearise ? graph_prog in
1112  ∀sigma.good_sigma p graph_prog sigma →
1113  ∀prf : well_formed_pc p p' graph_prog sigma pc.
1114  fetch_statement ? (make_sem_graph_params p p') …
1115    (globalenv_noinit … graph_prog) pc = return 〈fn,stmt〉 →
1116  fetch_statement ? (make_sem_lin_params p p') …
1117    (globalenv_noinit … lin_prog) (sigma_pc … pc prf) =
1118    return 〈sigma_function_name … fn, graph_to_lin_statement … stmt〉.
1119 #p #p' #graph_prog #pc #fn #stmt #sigma #good #wfprf
1120 whd in match fetch_statement; normalize nodelta #H
1121 cases (bind_inversion ????? H) #id * -H #fetchfn
1122 >(fetch_function_sigma_commute … wfprf … fetchfn) >m_return_bind
1123 #H cases (bind_inversion ????? H) #fstmt * -H #H
1124 lapply (opt_eq_from_res ???? H) -H #H #EQ whd in EQ:(??%%); destruct
1125 >(stmt_at_sigma_commute … good … H) [%]
1126 whd in match sigma_pc; normalize nodelta
1127 @opt_safe_elim #pc' #H
1128 cases (bind_opt_inversion ????? H)
1129 #i * #EQ1 -H #H
1130 cases (bind_opt_inversion ????? H)
1131 #pnt * #EQ2 whd in ⊢ (??%?→?); #EQ3 destruct
1132 whd in match point_of_pc in ⊢ (???%); normalize nodelta >point_of_offset_of_point
1133 lapply (opt_eq_from_res ???? fetchfn) >EQ1 #EQ4 destruct @EQ2
1134qed.
1135
1136lemma point_of_pc_sigma_commute :
1137 ∀p,p',graph_prog.
1138 let lin_prog ≝ linearise p graph_prog in
1139 ∀sigma,pc,fn,n.
1140  ∀prf : well_formed_pc p p' graph_prog sigma pc.
1141 int_funct_of_block … (globalenv_noinit … graph_prog) (pc_block pc) = return fn →
1142 sigma fn (point_of_pc ? (make_sem_graph_params p p') pc) = return n →
1143 point_of_pc ? (make_sem_lin_params p p') (sigma_pc … pc prf) = n.
1144#p #p' #graph_prog #sigma #pc #fn #n #prf #EQfetch #EQsigma
1145whd in match sigma_pc; normalize nodelta
1146@opt_safe_elim #pc' whd in match sigma_pc_opt;
1147normalize nodelta >EQfetch >m_return_bind >EQsigma
1148>m_return_bind whd in ⊢ (??%?→?); #EQ destruct(EQ)
1149change with (point_of_offset ??? = ?) @point_of_offset_of_point
1150qed.
1151
1152definition linearise_status_rel:
1153 ∀p,p',graph_prog.
1154 let lin_prog ≝ linearise p graph_prog in
1155 ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
1156 let stack_sizes' ≝
1157  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
1158    ? graph_prog stack_sizes in
1159 ∀sigma,gss.
1160 good_sigma p graph_prog sigma →
1161   status_rel
1162    (graph_abstract_status p p' graph_prog stack_sizes')
1163    (lin_abstract_status p p' lin_prog stack_sizes)
1164 ≝ λp,p',graph_prog,stack_sizes,sigma,gss,good.
1165   mk_status_rel …
1166    (* sem_rel ≝ *) (λs1,s2.
1167     ∃prf: well_formed_state_pc p p' graph_prog sigma gss s1.
1168      s2 = sigma_state_pc … s1 prf)
1169    (* call_rel ≝ *) (λs1,s2.
1170      ∃prf:well_formed_state_pc p p' graph_prog sigma gss s1.
1171      pc ? s2 = sigma_pc … (pc ? s1) (proj1 … prf))
1172    (* sim_final ≝ *) ?.
1173#st1 #st2 * #prf #EQ2
1174%
1175whd in ⊢ (%→%);
1176#H lapply (opt_to_opt_safe … H)
1177@opt_safe_elim -H
1178#res #_
1179#H lapply (res_eq_from_opt ??? H) -H
1180cases daemon
1181(*#H elim (bind_inversion ????? H) in ⊢ ?;
1182* #f #stmt *
1183whd in ⊢ (??%?→?);*)
1184qed.
1185
1186lemma IO_bind_inversion:
1187  ∀O,I,A,B. ∀f: IO O I A. ∀g: A → IO O I B. ∀y: B.
1188  (! x ← f ; g x = return y) →
1189  ∃x. (f = return x) ∧ (g x = return y).
1190#O #I #A #B #f #g #y cases f normalize
1191[ #o #f #H destruct
1192| #a #e %{a} /2 by conj/
1193| #m #H destruct (H)
1194] qed.
1195
1196lemma err_eq_from_io : ∀O,I,X,m,v.
1197  err_to_io O I X m = return v → m = return v.
1198#O #I #X * #x #v normalize #EQ destruct % qed.
1199
1200lemma eval_seq_no_pc_sigma_commute :
1201 ∀p,p',graph_prog.
1202 let lin_prog ≝ linearise p graph_prog in
1203 ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
1204 let stack_sizes' ≝
1205  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
1206    ? graph_prog stack_sizes in
1207 ∀sigma.∀gss : good_state_sigma … graph_prog sigma.
1208 ∀fn,st,stmt,st'.
1209 ∀prf : well_formed_state … gss st.∀prf'.
1210  eval_seq_no_pc ?? (ev_genv … (graph_prog_params … graph_prog stack_sizes'))
1211   fn st stmt = return st' →
1212  eval_seq_no_pc ?? (ev_genv … (lin_prog_params … lin_prog stack_sizes))
1213    (sigma_function_name … fn) (sigma_state … gss st prf) stmt =
1214  return sigma_state … gss st' prf'.
1215  #p #p' #graph_prog #stack_sizes #sigma #gss
1216  #fn #st #stmt
1217  #st' #prf #prf'
1218  whd in match eval_seq_no_pc;
1219  cases stmt normalize nodelta
1220  [1,2: (* COMMENT, COST_LABEL *) #_ #EQ whd in EQ : (??%%); destruct(EQ) //
1221  | (* MOVE *) #mv_sig #H lapply(err_eq_from_io ????? H) -H #H
1222    >(pair_reg_move_ok ?????????? H) [% | skip]
1223  | (* POP *)
1224    #a #H lapply(err_eq_from_io ????? H) -H #H elim (bind_inversion ????? H) -H
1225    * #val #st1 * #vals_spec #H
1226    cut(well_formed_state … gss st1) [ cases daemon (* to be added to gss *) ]
1227    #wf_st1
1228    lapply(acca_store_wf ????????? H wf_st1)
1229    * #_ #sigma_val_spec
1230    lapply vals_spec -vals_spec
1231    whd in match pop; normalize nodelta
1232    #H1 elim (bind_inversion ????? H1) -H1 * #g_bev #g_is * #ispop_spec
1233    whd in ⊢ ((??%%) → ?); #EQ (*to be destructed*)
1234    lapply ispop_spec -ispop_spec
1235    whd in match is_pop; normalize nodelta
1236    cases (istack ? st) normalize nodelta
1237    [ #ABS whd in ABS : (???%); destruct(ABS)
1238    | #one whd in ⊢ ((??%%) → ?); #EQ1 destruct(EQ1)
1239      cases (istack ? (sigma_state … st prf)) normalize nodelta
1240   
1241    lapply (acca_store_ok ?????????????? H)
1242
1243   
1244     -val_spec * #bv #is * #bv_is_spec
1245    #EQ whd in EQ : (??%%); destruct(EQ)
1246    whd in match is_pop in bv_is_spec; normalize nodelta in bv_is_spec;
1247    inversion (istack ? st) in bv_is_spec;
1248    [ #_ normalize nodelta whd in ⊢ ((???%) → ?); #ABS destruct(ABS)
1249    | #bv1 #bv1_spec normalize nodelta whd in ⊢ ((??%%) → ?); #EQ destruct(EQ)
1250    lapply(acca_store_wf ????????? H prf) check acca_store_ok check(acca_store_ok ?????????????? H)
1251 
1252  @(pair_reg_move_ok ? ? ? ? gss mv_sig st st' ? ?) whd in match pair_reg_move in ⊢ (%→?); normalize nodelta     
1253    #H
1254qed.       
1255       
1256inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
1257    ex1_intro: ∀ x:A. P x →  ex_Type1 A P.
1258(*interpretation "exists in Type[1]" 'exists x = (ex_Type1 ? x).*)
1259
1260lemma linearise_ok:
1261 ∀p,p',graph_prog.
1262  let lin_prog ≝ linearise ? graph_prog in
1263 ∀lin_stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
1264 let graph_stack_sizes ≝
1265  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
1266    ? graph_prog lin_stack_sizes in
1267 (∀sigma.good_sigma_state p p' graph_prog sigma) →
1268   ex_Type1 … (λR.
1269   status_simulation
1270    (graph_abstract_status p p' graph_prog graph_stack_sizes)
1271    (lin_abstract_status p p' lin_prog lin_stack_sizes) R).
1272 #p #p' #graph_prog
1273 cases (linearise_spec … graph_prog) #sigma #good
1274 #lin_stack_sizes
1275 #gss lapply (gss sigma) -gss #gss
1276 %{(linearise_status_rel p p' graph_prog lin_stack_sizes sigma gss good)}
1277whd in match graph_abstract_status;
1278whd in match lin_abstract_status;
1279whd in match graph_prog_params;
1280whd in match lin_prog_params;
1281normalize nodelta
1282whd
1283whd in ⊢ (%→%→%→?);
1284whd in ⊢ (?(?%)→?(?%)→?(?%)→?);
1285whd in ⊢ (?%→?%→?%→?);
1286#st1 #st1' #st2
1287whd in ⊢ (%→?);
1288change with
1289  (eval_state (make_sem_graph_params p p') (prog_var_names ???) ?? = ? → ?)
1290whd in match eval_state in ⊢ (%→?); normalize nodelta
1291change with (Σi.is_internal_function_of_program ? graph_prog i) in
1292match (Sig ??) in ⊢ (%→?);
1293letin globals ≝ (prog_var_names ?? graph_prog)
1294change with (fetch_statement ??? (globalenv_noinit ? graph_prog) ?) in
1295  match (fetch_statement ?????) in ⊢ (%→?);
1296#ex
1297cases (IO_bind_inversion ??????? ex) in ⊢ ?; * #fn #stmt * -ex
1298#EQfetch lapply (err_eq_from_io ????? EQfetch) -EQfetch
1299#EQfetch
1300cases (bind_inversion ????? EQfetch)
1301#f_id * #H lapply (opt_eq_from_res ???? H) -H
1302#EQfunc_of_block
1303#H elim (bind_inversion ????? H) -H #stmt' *
1304#H lapply (opt_eq_from_res ???? H) -H #EQstmt_at
1305whd in ⊢ (??%%→?); #EQ destruct(EQ)
1306#EQeval
1307cases (good fn (pi2 … (sigma_function_name p graph_prog fn)))
1308letin graph_fun ≝ (if_of_function … fn) in EQstmt_at; #EQstmt_at
1309#entry_0
1310#good_local
1311* * #wf_pc #wf_state #EQst2
1312generalize in match wf_pc in ⊢ ?;
1313whd in ⊢ (%→?);
1314inversion (sigma_pc_opt ?????) in ⊢ (%→?); [ #_ * #ABS elim (ABS ?) % ]
1315#lin_pc
1316whd in match (sigma_pc_opt) in ⊢ (%→?); normalize nodelta
1317>EQfunc_of_block in ⊢ (%→?); >m_return_bind in ⊢ (%→?);
1318#H elim (bind_opt_inversion ????? H) in ⊢ ?; -H #lin_pt *
1319#EQsigma whd in ⊢ (??%?→?); #EQ destruct(EQ) #_
1320elim (good_local … EQsigma) -good_local
1321#stmt' *
1322change with (stmt_at ?? (joint_if_code ?? graph_fun) ? = ? → ?)
1323>EQstmt_at #EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ)
1324#H elim (opt_Exists_elim … H) -H * #lbl_opt #lin_stmt normalize nodelta
1325>(prog_if_of_function_transform … fn) in ⊢ (%→?); [2: % ]
1326change with graph_fun in match (if_of_function ?? fn) in ⊢ (%→?);
1327letin lin_fun ≝ (\fst  (linearise_int_fun p globals graph_fun))
1328change with globals in match (prog_var_names ?? graph_prog) in ⊢ (%→?);
1329*
1330#EQnth_opt ** #opt_lbl_spec #EQ destruct(EQ) #next_spec
1331letin lin_prog ≝ (linearise … graph_prog)
1332lapply (refl … (eval_state ? globals (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) st2))
1333destruct(EQst2)
1334whd in match eval_state in ⊢ (???%→?); normalize nodelta
1335letin st2 ≝ (sigma_state_pc ????? st1 ?)
1336>(fetch_statement_sigma_commute … good … EQfetch) in ⊢ (%→?);
1337>m_return_bind in ⊢ (%→?);
1338#ex'
1339(* resolve classifier *)
1340whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
1341>EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
1342normalize nodelta
1343cases stmt in EQfetch EQeval EQstmt_at EQnth_opt next_spec ex';
1344[ *
1345  [ #stmt #nxt
1346    whd in match eval_statement in ⊢ (?→%→?); normalize nodelta
1347    #EQfetch #EQeval #EQstmt_at #EQnth_opt #next_spec
1348    whd in match (graph_to_lin_statement ???) in ⊢ (%→?);
1349    whd in match eval_statement in ⊢ (%→?); normalize nodelta
1350    elim (IO_bind_inversion ??????? EQeval) #st1_no_pc *
1351    #EQeval_no_pc #EQeval_pc
1352    >(eval_seq_no_pc_sigma_commute … EQeval_no_pc)
1353    [2: (*TODO lemma eval_seq_no_pc_wf *) @hide_prf cases daemon ]
1354        >m_return_bind
1355    cases stmt in EQfetch EQeval_no_pc EQeval_pc EQstmt_at EQnth_opt next_spec;
1356    [14: #f #args #dest
1357    | #c
1358    | #lbl
1359    | #move_sig
1360    | #a
1361    | #a
1362    | #sy #sy_prf #dpl #dph
1363    | #op #a #b #arg1 #arg2
1364    | #op #a #arg
1365    | #op #a #arg1 #arg2
1366    ||
1367    | #a #dpl #dph
1368    | #dpl #dph #a
1369    | #s_ext
1370    ]
1371    [ (* CALL *)
1372    |(*:*)
1373      normalize nodelta
1374      #EQfetch #EQeval_no_pc #EQeval_pc #EQstmt_at #EQnth_opt #next_spec
1375      whd in match eval_seq_pc; normalize nodelta
1376      #ex1
1377      cases next_spec
1378      [ #EQnext_sigma
1379        %[2: %{(taaf_step … (taa_base …) ex1 ?)}
1380         [ cases daemon (* TODO lemma joint_classify_sigma_commute *) ]|]
1381        normalize nodelta
1382        cut (? : Prop) [3: #R' % [ %{I R'} ] |*:]
1383        [ cases daemon (* TODO lemma joint_label_sigma_commute *)
1384        | %
1385          [ (* TODO lemma well_formed_state_pc_preserve? *) @hide_prf cases daemon
1386          | whd in match eval_seq_pc in EQeval_pc;
1387            whd in EQeval_pc : (??%%); whd in EQeval_pc : (??(????%)?);
1388            destruct (EQeval_pc)
1389            whd in ⊢ (??%%);
1390            change with (sigma_pc ??????) in match
1391              (pc ? (sigma_state_pc ???????));
1392            whd in match (succ_pc ????) in ⊢ (??%%);
1393            whd in match (point_of_succ ???) in ⊢ (??%%);
1394            >(point_of_pc_sigma_commute … EQfunc_of_block EQsigma)
1395            whd in match sigma_pc in ⊢ (???%);
1396            whd in match sigma_pc_opt in ⊢ (???%); normalize nodelta
1397            @opt_safe_elim #pc'
1398            >EQfunc_of_block >m_return_bind
1399            whd in match point_of_pc; normalize nodelta
1400            >point_of_offset_of_point
1401            >EQnext_sigma whd in ⊢ (??%?→?);
1402            whd in match pc_of_point; normalize nodelta
1403            #EQ destruct(EQ)
1404            >sigma_pblock_eq_lemma %
1405          ]
1406        ]
1407      | -next_spec #next_spec
1408        %
1409     
1410     
1411        whd in ⊢ (?→???%→?);
1412        generalize in ⊢ (??%? → ???(????%) → ?); |*: skip]  | #a #lbltrue #next
1413  ] #next change with label in next;
1414| *
1415  [ #lbl
1416  |
1417  | #fl #f #args
1418  ]
1419]
1420whd in match eval_statement in ⊢ (?→%→?); normalize nodelta
1421#EQfetch #EQeval #EQstmt_at #EQnth_opt #next_spec
1422normalize nodelta
1423whd in match (graph_to_lin_statement ???) in ⊢ (%→?);
1424whd in match eval_statement in ⊢ (%→?); normalize nodelta
1425[ >m_return_bind in ⊢ (%→?);
1426  >m_return_bind in EQeval;
1427
1428
1429
1430  (* common for all non-call seq *)
1431  >m_return_bind in ⊢ (%→?);
1432  whd in ⊢ (??%%→?); #EQ destruct(EQ)
1433  >m_return_bind in ⊢ (%→?);
1434
1435 
1436  #ex1
1437lapply (refl … (eval_state ? globals (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) st2))
1438
1439whd in match (point_of_pc ???);
1440whd in match (point_of_succ ???);
1441whd in match sigma_pc in ⊢ (???%); normalize nodelta @opt_safe_elim
1442#pc' #H
1443elim (bind_opt_inversion ????? H) #fn * #EQbl
1444-H #H 
1445elim (bind_opt_inversion ????? H) -H #n * #EQsigma whd in ⊢ (??%?→?);
1446#EQ destruct(EQ)
1447whd in match (succ_pc ????);
1448whd in match (point_of_succ ???);
1449change with (point_of_offset ???) in match (point_of_pc ???);
1450>point_of_offset_of_point
1451whd in match sigma_pc; normalize nodelta @opt_safe_elim
1452#pc' whd in match sigma_pc_opt; normalize nodelta
1453
1454 
1455 
1456        whd in match (succ_pc ????);
1457               
1458        change with next in match (offset_of_point ???) in ⊢ (???%);
1459whd in fetch_statement_spec : (??()%);
1460cases cl in classified_st1_cl; -cl #classified_st1_cl whd
1461[4:
1462 >rel_st1_st2 -st2 letin lin_prog ≝ (linearise ? graph_prog)
1463 cases (good (pi1 ?? fn)) [2: cases daemon (* TODO *) ]
1464 #sigma_entry_is_zero #sigma_spec
1465 lapply (sigma_spec (point_of_pc … (make_sem_graph_params … p') (pc … st1)))
1466 -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @opt_to_opt_safe cases daemon (* TO REDO *) |2: skip ]
1467 -sigma_spec #graph_stmt * #graph_lookup_ok #sigma_spec
1468 cases (opt_Exists_elim … sigma_spec) in ⊢ ?;
1469 * #optlabel #lin_stm * #lin_lookup_ok whd in ⊢ (% → ?); ** #labels_preserved
1470 #related_lin_stm_graph_stm
1471 
1472 inversion (stmt_implicit_label ???)
1473 [ whd in match (opt_All ???); #stmt_implicit_spec #_
1474   letin st2_opt' ≝ (eval_state …
1475               (ev_genv (lin_prog_params … lin_prog lin_stack_sizes))
1476               (sigma_state_pc … wf_st1))
1477   cut (∃st2': lin_abstract_status p p' lin_prog lin_stack_sizes. st2_opt' = return st2')
1478   [cases daemon (* TODO, needs lemma? *)] * #st2' #st2_spec'
1479   normalize nodelta in st2_spec'; -st2_opt'
1480   %{st2'} %{(taaf_step … (taa_base …) …)}
1481   [ cases daemon (* TODO, together with the previous one? *)
1482   | @st2_spec' ]
1483   %[%] [%]
1484   [ whd whd in match eval_state in st2_spec'; normalize nodelta in st2_spec';
1485     >(fetch_statement_sigma_commute … good … fetch_statement_spec) in st2_spec';
1486     >m_return_bind
1487     (* Case analysis over the possible statements *)
1488     inversion graph_stmt in stmt_implicit_spec; normalize nodelta
1489     [ #stmt #lbl #_ #abs @⊥ normalize in abs; destruct(abs) ]
1490     XXXXXXXXXX siamo qua, caso GOTO e RETURN
1491   | cases daemon (* TODO, after the definition of label_rel, trivial *) ]
1492   ]
1493 | ....
1494qed.
1495
1496
1497
1498
1499
1500[ *
1501  [ *
1502    [ letin C_COMMENT ≝ 0 in ⊢ ?; #c
1503    | letin C_COST_LABEL ≝ 0 in ⊢ ?; #lbl
1504    | letin C_MOVE       ≝ 0 in ⊢ ?; #move_sig
1505    | letin C_POP        ≝ 0 in ⊢ ?; #a
1506    | letin C_PUSH       ≝ 0 in ⊢ ?; #a
1507    | letin C_ADDRESS    ≝ 0 in ⊢ ?; #sy #sy_prf #dpl #dph
1508    | letin C_OPACCS     ≝ 0 in ⊢ ?; #op #a #b #arg1 #arg2
1509    | letin C_OP1        ≝ 0 in ⊢ ?; #op #a #arg
1510    | letin C_OP2        ≝ 0 in ⊢ ?; #op #a #arg1 #arg2
1511    | letin C_CLEAR_CARRY ≝ 0 in ⊢ ?;
1512    | letin C_SET_CARRY  ≝ 0 in ⊢ ?;
1513    | letin C_LOAD       ≝ 0 in ⊢ ?; #a #dpl #dph
1514    | letin C_STORE      ≝ 0 in ⊢ ?; #dpl #dph #a
1515    | letin C_CALL       ≝ 0 in ⊢ ?; #f #args #dest
1516    | letin C_EXT        ≝ 0 in ⊢ ?; #s_ext
1517    ]
1518  | letin C_COND ≝ 0 in ⊢ ?; #a #lbltrue
1519  ] #next change with label in next;
1520| *
1521  [ letin C_GOTO ≝ 0 in ⊢ ?; #lbl
1522  | letin C_RETURN ≝ 0 in ⊢ ?;
1523  | letin C_TAILCALL ≝ 0 in ⊢ ?; #fl #f #args
1524  ]
1525]
Note: See TracBrowser for help on using the repository browser.