source: src/joint/lineariseProof.ma @ 2507

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

finished pop case in commutation eval_Seq_no_pc

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