source: src/joint/lineariseProof.ma @ 2529

Last change on this file since 2529 was 2529, checked in by tranquil, 7 years ago

rewritten function handling in joint
swapped call_rel with ret_rel in the definition of status_rel, and parameterised status_simulation on status_rel
renamed SemanticUtils?

File size: 80.5 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  (ident → option ℕ) →
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  (ident → option ℕ) →
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_map ≝ λp.λgraph_prog : joint_program (mk_graph_params p).
100  joint_closed_internal_function (mk_graph_params p) (prog_var_names … graph_prog) →
101    label → option ℕ.
102   
103definition sigma_pc_opt:
104 ∀p,p'.∀graph_prog.
105  sigma_map p graph_prog →
106   program_counter → option program_counter
107 ≝
108  λp,p',prog,sigma,pc.
109  let pars ≝ make_sem_graph_params p p' in
110  let ge ≝ globalenv_noinit … prog in
111  ! 〈i, fd〉 ← res_to_opt … (fetch_internal_function … ge (pc_block pc)) ;
112  ! lin_point ← sigma fd (point_of_pc pars pc) ;
113  return pc_of_point
114  (make_sem_lin_params ? p') (pc_block pc) lin_point.
115
116definition well_formed_pc:
117 ∀p,p',graph_prog.
118  sigma_map p graph_prog →
119   program_counter → Prop
120 ≝
121 λp,p',prog,sigma,pc.
122  sigma_pc_opt p p' prog sigma pc
123   ≠ None ….
124
125definition sigma_beval_opt :
126 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
127  sigma_map p graph_prog →
128  beval → option beval ≝
129λp,p',graph_prog,sigma,bv.
130match bv with
131[ BVpc pc prt ⇒ ! pc' ← sigma_pc_opt p p' graph_prog sigma pc ; return BVpc pc' prt
132| _ ⇒ return bv
133].
134
135definition sigma_beval :
136 ∀p,p',graph_prog,sigma,bv.
137 sigma_beval_opt p p' graph_prog sigma bv ≠ None ? → beval ≝
138 λp,p',graph_prog,sigma,bv.opt_safe ….
139
140definition sigma_is_opt :
141 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
142  sigma_map p graph_prog →
143  internal_stack → option internal_stack ≝
144λp,p',graph_prog,sigma,is.
145match is with
146[ empty_is ⇒ return empty_is
147| one_is bv ⇒ ! bv' ← sigma_beval_opt p p' … sigma bv ; return one_is bv'
148| both_is bv1 bv2 ⇒
149  ! bv1' ← sigma_beval_opt p p' … sigma bv1 ;
150  ! bv2' ← sigma_beval_opt p p' … sigma bv2 ;
151  return both_is bv1' bv2'
152].
153
154definition sigma_is :
155 ∀p,p',graph_prog,sigma,is.
156 sigma_is_opt p p' graph_prog sigma is ≠ None ? → internal_stack ≝
157 λp,p',graph_prog,sigma,is.opt_safe ….
158
159lemma sigma_is_pop_commute :
160 ∀p,p',graph_prog,sigma,is,bv,is'.
161 ∀prf : sigma_is_opt p p' graph_prog sigma is ≠ None ?.
162 is_pop is = return 〈bv, is'〉 →
163 ∃prf' : sigma_beval_opt p p' graph_prog sigma bv ≠ None ?.
164 ∃prf'' : sigma_is_opt p p' graph_prog sigma is' ≠ None ?.
165 is_pop (sigma_is … prf) = return 〈sigma_beval … prf', sigma_is … prf''〉.
166cases daemon qed.
167
168definition well_formed_mem :
169 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
170  sigma_map p graph_prog →
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 : sigma_map p graph_prog) : Type[0] ≝
314{ well_formed_frames : framesT (make_sem_graph_params p p') → Prop
315; sigma_frames : ∀frms.well_formed_frames frms → framesT (make_sem_lin_params p p')
316; sigma_empty_frames_commute :
317  ∃prf.
318  empty_framesT (make_sem_lin_params p p') =
319  sigma_frames (empty_framesT (make_sem_graph_params p p')) prf
320
321; well_formed_regs : regsT (make_sem_graph_params p p') → Prop
322; sigma_regs : ∀regs.well_formed_regs regs → regsT (make_sem_lin_params p p')
323; sigma_empty_regsT_commute :
324  ∀ptr.∃ prf.
325  empty_regsT (make_sem_lin_params p p') ptr =
326  sigma_regs (empty_regsT (make_sem_graph_params p p') ptr) prf
327; sigma_load_sp_commute :
328  ∀reg,ptr.
329  load_sp (make_sem_graph_params p p') reg = return ptr →
330  ∃prf.
331  load_sp (make_sem_lin_params p p') (sigma_regs reg prf) = return ptr
332; sigma_save_sp_commute :
333  ∀reg,ptr,prf1. ∃prf2.
334  save_sp (make_sem_lin_params p p') (sigma_regs reg prf1) ptr =
335  sigma_regs (save_sp (make_sem_graph_params p p') reg ptr) prf2
336}.
337
338definition well_formed_state :
339 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
340 ∀sigma.
341 good_sem_state_sigma p p' graph_prog sigma →
342 state (make_sem_graph_params p p') → Prop ≝
343λp,p',graph_prog,sigma,gsss,st.
344well_formed_frames … gsss (st_frms … st) ∧
345sigma_is_opt p p' graph_prog sigma (istack … st) ≠ None ? ∧
346well_formed_regs … gsss (regs … st) ∧
347well_formed_mem p p' graph_prog sigma (m … st).
348
349definition sigma_state :
350 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
351 ∀sigma.
352 ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
353 ∀st : state (make_sem_graph_params p p').
354 well_formed_state … gsss st →
355 state (make_sem_lin_params p p') ≝
356λp,p',graph_prog,sigma,gsss,st,prf.
357mk_state …
358  (sigma_frames p p' graph_prog sigma gsss (st_frms … st) ?)
359  (sigma_is p p' graph_prog sigma (istack … st) ?)
360  (carry … st)
361  (sigma_regs … gsss (regs … st) ?)
362  (sigma_mem p p' graph_prog sigma (m … st) ?).
363@hide_prf
364[ @(proj1 … (proj1 … (proj1 … prf))) | @(proj2 … (proj1 … (proj1 … prf)))
365| @(proj2 … (proj1 … prf)) | @(proj2 … prf)]
366qed.
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.
408∀pc.
409∀prf : well_formed_pc p p' graph_prog sigma pc.
410program_counter ≝
411λp,p',graph_prog,sigma,st.opt_safe ….
412 
413lemma sigma_pc_ok:
414  ∀p,p',graph_prog.
415  ∀sigma.
416   ∀pc.
417    ∀prf:well_formed_pc p p' graph_prog sigma pc.
418    sigma_pc_opt p p' graph_prog sigma pc =
419    Some … (sigma_pc p p' graph_prog sigma pc prf).
420    #p #p' #graph_prog #sigma #st #prf @opt_to_opt_safe qed.
421
422definition well_formed_state_pc :
423 ∀p,p',graph_prog,sigma.
424  good_sem_state_sigma p p' graph_prog sigma →
425  state_pc (make_sem_graph_params p p') → Prop ≝
426 λp,p',prog,sigma,gsss,st.
427 well_formed_pc p p' prog sigma (pc … st) ∧ well_formed_state … gsss st.
428 
429definition sigma_state_pc :
430 ∀p.
431 ∀p':∀F.sem_unserialized_params p F.
432 ∀graph_prog.
433  ∀sigma.
434(*   let lin_prog ≝ linearise ? graph_prog in *)
435  ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
436    ∀s:state_pc (make_sem_graph_params p p'). (* = graph_abstract_status p p' graph_prog stack_sizes *)
437     well_formed_state_pc p p' graph_prog sigma gsss s →
438      state_pc (make_sem_lin_params p p') (* = lin_abstract_status p p' lin_prog ? *)
439
440 λp,p',graph_prog,sigma,gsss,s,prf.
441 let pc' ≝ sigma_pc … (proj1 … prf) in
442 let st' ≝ sigma_state … (proj2 … prf) in
443 mk_state_pc ? st' pc'.
444(*
445definition sigma_function_name :
446 ∀p,graph_prog.
447 let lin_prog ≝ linearise p graph_prog in
448  (Σf.is_internal_function_of_program … graph_prog f) →
449  (Σf.is_internal_function_of_program … lin_prog f) ≝
450λp,graph_prog,f.«f, if_propagate … (pi2 … f)».
451*)
452lemma m_list_map_All_ok :
453  ∀M : MonadProps.∀X,Y,f,l.
454  All X (λx.∃y.f x = return y) l → ∃l'.m_list_map M X Y f l = return l'.
455  cases daemon qed.
456
457(*
458inductive isMember (A : Type[0]) (x : A) : list A → Prop ≝
459 | isMemberHead : ∀ tl.isMember A x (x :: tl)
460 | isMemberTail : ∀ y,tl .isMember A x tl → isMember A x (y :: tl).
461(*
462definition lift_f_tail : ∀ A,B : Type[0]. ∀ l ,tl : list A. ∀y : A . l = y ::tl →
463      (∀ x : A. isMember A x l → B) → ∀ x : A. isMember A x tl → B.
464      #A #B #l #tl #y #l_spec #f #x #tl_member @f [//]
465    @(isMemberTail ? x y l tl l_spec tl_member)
466    qed.
467  *)             
468
469let rec ext_map (A,B : Type[0]) (l : list A) (f : ∀ x : A. isMember A x l → B) on l : list B ≝
470match l with [ nil ⇒ λprf : l = nil ?.nil ?
471             | cons x tl ⇒ λprf : l = cons ? x tl.
472              f x ? :: ext_map ?? tl (λy,prf'.f y ?)
473             ] (refl …).
474@hide_prf
475>prf
476[ %1
477| %2 assumption
478] qed.
479              (f x (isMemberHead A x l tl prf)) ::   
480              ext_map A B tl (lift_f_tail A B l tl x prf f) ]
481              (refl ? l).
482*)
483
484definition helper_def_store__commute :
485  ∀p,p',graph_prog,sigma.
486  ∀X : ? → Type[0].
487  ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
488  ∀store : ∀p,F.∀p' : sem_unserialized_params p F.
489    X p → beval → regsT p' →
490    res (regsT p').
491  Prop ≝
492  λp,p',graph_prog,sigma,X,gsss,store.
493  ∀a : X ?.∀bv,r,r',prf1,prf1'.
494  store … a bv r = return r' →
495  ∃prf2.
496  store ??? a
497    (sigma_beval p p' graph_prog sigma bv prf1')
498    (sigma_regs ???? gsss r prf1) = return sigma_regs … gsss r' prf2.
499
500definition helper_def_retrieve__commute :
501  ∀p,p',graph_prog,sigma.
502  ∀X : ? → Type[0].
503  ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
504  ∀retrieve : ∀p,F.∀p' : sem_unserialized_params p F.
505    regsT p' → X p → res beval.
506  Prop ≝
507  λp,p',graph_prog,sigma,X,gsss,retrieve.
508  ∀a : X p.∀r,bv,prf1.
509  retrieve … r a = return bv →
510  ∃prf2.
511  retrieve … (sigma_regs … gsss r prf1) a
512     = return sigma_beval p p' graph_prog sigma bv prf2.
513 
514record good_state_sigma
515  (p : unserialized_params)
516  (p' : ∀F.sem_unserialized_params p F) (graph_prog : ?)
517  (sigma : sigma_map p graph_prog)
518: Type[0] ≝
519{ gsss :> good_sem_state_sigma p p' graph_prog sigma
520
521; acca_store__commute : helper_def_store__commute … gsss acca_store_
522; acca_retrieve_commute : helper_def_retrieve__commute … gsss acca_retrieve_
523; acca_arg_retrieve_commute : helper_def_retrieve__commute … gsss acca_arg_retrieve_
524; accb_store_commute : helper_def_store__commute … gsss accb_store_
525; accb_retrieve_commute : helper_def_retrieve__commute … gsss accb_retrieve_
526; accb_arg_retrieve_commute : helper_def_retrieve__commute … gsss accb_arg_retrieve_
527; dpl_store_commute : helper_def_store__commute … gsss dpl_store_
528; dpl_retrieve_commute : helper_def_retrieve__commute … gsss dpl_retrieve_
529; dpl_arg_retrieve_commute : helper_def_retrieve__commute … gsss dpl_arg_retrieve_
530; dph_store_commute : helper_def_store__commute … gsss dph_store_
531; dph_retrieve_commute : helper_def_retrieve__commute … gsss dph_retrieve_
532; dph_arg_retrieve_commute : helper_def_retrieve__commute … gsss dph_arg_retrieve_
533; snd_arg_retrieve_commute : helper_def_retrieve__commute … gsss snd_arg_retrieve_
534; pair_reg_move_commute : ∀mv,r1,r2,prf1.
535  pair_reg_move_ ? ? (p' ?) r1 mv = return r2 →
536  ∃prf2 .
537  pair_reg_move_ ? ? (p' ?) (sigma_regs p p' graph_prog sigma gsss r1 prf1) mv =
538    return sigma_regs p p' graph_prog sigma gsss r2 prf2
539; allocate_locals_commute :
540  ∀ loc, r1, prf1. ∃ prf2.
541  allocate_locals_ ? ? (p' ?) loc (sigma_regs p p' graph_prog sigma gsss r1 prf1) =
542  sigma_regs p p' graph_prog sigma gsss (allocate_locals_ ? ? (p' ?) loc r1) prf2
543; save_frame_commute :
544  ∀dest,st1,st2,prf1.
545  save_frame ?? (p' ?) dest st1 = return st2 →
546  let st1' ≝ mk_state_pc … (sigma_state p p' graph_prog sigma gsss st1 (proj2 … prf1))
547    (sigma_pc p p' graph_prog sigma (pc … st1) (proj1 … prf1)) in
548  ∃prf2.
549  save_frame ?? (p' ?) dest st1' = return sigma_state p p' graph_prog sigma gsss st2 prf2
550; eval_ext_seq_commute :
551  let lin_prog ≝ linearise p graph_prog in
552  ∀stack_sizes.
553  ∀ext,i,fn,st1,st2,prf1.
554  eval_ext_seq ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes))
555    ext i fn st1 = return st2 →
556  ∃prf2.
557  eval_ext_seq ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
558    ext i (\fst (linearise_int_fun … fn)) (sigma_state p p' graph_prog sigma gsss st1 prf1) =
559   return sigma_state p p' graph_prog sigma gsss st2 prf2
560; setup_call_commute :
561  ∀ n , parsT, call_args , st1 , st2 , prf1.
562  setup_call ?? (p' ?) n parsT call_args st1 = return st2 →
563  ∃prf2.
564  setup_call ?? (p' ?) n parsT call_args (sigma_state p p' graph_prog sigma gsss st1 prf1) =
565  return (sigma_state p p' graph_prog sigma gsss st2 prf2)
566; fetch_external_args_commute : (* TO BE CHECKED *)
567  ∀ex_fun,st1,prf1,call_args.
568  fetch_external_args ?? (p' ?) ex_fun st1 call_args =
569  fetch_external_args ?? (p' ?) ex_fun (sigma_state p p' graph_prog sigma gsss st1 prf1) call_args
570; set_result_commute :
571  ∀ l , call_dest , st1 , st2 , prf1.
572  set_result ?? (p' ?) l call_dest st1 = return st2 →
573  ∃prf2.
574  set_result ?? (p' ?) l call_dest (sigma_state p p' graph_prog sigma gsss st1 prf1) =
575  return (sigma_state p p' graph_prog sigma gsss st2 prf2) 
576; read_result_commute :
577  let lin_prog ≝ linearise p graph_prog in
578  ∀stack_sizes.
579  ∀call_dest , st1 , prf1, l1.
580  read_result ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes))
581    call_dest st1 = return l1 →
582  ∃ prf : m_list_map … (sigma_beval_opt p p' graph_prog sigma) l1 ≠ None ?.
583  read_result ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
584    call_dest (sigma_state p p' graph_prog sigma gsss st1 prf1) = return opt_safe … prf 
585; pop_frame_commute :
586  let lin_prog ≝ linearise p graph_prog in
587  ∀stack_sizes.
588  ∀ st1 , prf1, curr_id , curr_fn ,st2.
589  pop_frame ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes))
590            curr_id curr_fn st1 = return st2 →
591 ∃prf2.
592 let pc' ≝ sigma_pc p p' graph_prog sigma (pc ? st2) (proj1 … prf2) in
593 let st2' ≝ sigma_state p p' graph_prog sigma gsss (st_no_pc ? st2) (proj2 … prf2) in
594  pop_frame ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
595            curr_id (\fst (linearise_int_fun … curr_fn)) (sigma_state p p' graph_prog sigma gsss st1 prf1) =
596            return mk_state_pc ? st2' pc'
597}.
598
599lemma store_commute :
600  ∀p,p',graph_prog,sigma.
601  ∀X : ? → Type[0].
602  ∀store.
603  ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
604  ∀H : helper_def_store__commute … gsss store.
605  ∀a : X p.∀bv,st,st',prf1,prf1'.
606  helper_def_store ? store … a bv st = return st' →
607  ∃prf2.
608  helper_def_store ? store … a
609    (sigma_beval p p' graph_prog sigma bv prf1')
610    (sigma_state … gsss st prf1) = return sigma_state … gsss st' prf2.
611#p #p' #graph_prog #sigma #X #store #gsss #H #a #bv #st #st #prf1 #prf2
612whd in match helper_def_store; normalize nodelta
613#H1 elim(bind_inversion ????? H1) -H1 #graph_reg * #store_spec
614#EQ whd in EQ : (??%%); destruct(EQ)
615elim(H a bv ?? (proj2 … (proj1 … prf1)) prf2 store_spec)
616#wf_graph_reg #store_spec1 %
617[ % [ % ] [%] ]
618[ @(proj1 … (proj1 … (proj1 … prf1)))
619| @(proj2 … (proj1 … (proj1 … prf1)))
620| @wf_graph_reg
621| @(proj2 … prf1)
622] >store_spec1 >m_return_bind %
623qed.
624
625
626
627lemma retrieve_commute :
628 ∀p,p',graph_prog,sigma.
629 ∀X : ? → Type[0].
630 ∀retrieve.
631 ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
632 ∀H : helper_def_retrieve__commute … gsss retrieve.
633 ∀a : X p .∀st,bv,prf1.
634 helper_def_retrieve ? retrieve … st a = return bv →
635 ∃prf2.
636     helper_def_retrieve ? retrieve … (sigma_state … gsss st prf1) a =
637     return sigma_beval p p' graph_prog sigma bv prf2.
638#p #p' #graph_prog #sigma #X #retrieve #gsss #H #a #st #bv #prf1
639whd in match helper_def_retrieve; normalize nodelta
640#retrieve_spec elim(H … (proj2 … (proj1 … prf1)) … retrieve_spec)
641#wf_bv #retrieve_spec1 %{wf_bv} >retrieve_spec1 %
642qed.
643
644(*
645definition acca_store_commute :
646  ∀p,p',graph_prog,sigma.
647  ∀gss : good_state_sigma p p' graph_prog sigma.
648  ∀a : acc_a_reg p.∀bv,st,st',prf1,prf1'.
649  acca_store … a bv st = return st' →
650  ∃prf2.
651  acca_store … a
652    (sigma_beval p p' graph_prog sigma bv prf1')
653    (sigma_state … gss st prf1) = return sigma_state … gss st' prf2
654 ≝
655λp,p',graph_prog,sigma.
656λgss : good_state_sigma p p' graph_prog sigma.
657store_commute … gss (acca_store__commute … gss).
658
659*)
660
661(* restano:
662; setup_call : nat → paramsT … uns_pars → call_args uns_pars →
663    state st_pars → res (state st_pars)
664; fetch_external_args: external_function → state st_pars → call_args … uns_pars →
665    res (list val)
666; set_result: list val → call_dest uns_pars → state st_pars → res (state st_pars)
667
668(* from now on, parameters that use the type of functions *)
669; read_result: ∀globals.genv_gen F globals → call_dest uns_pars → state st_pars → res (list beval)
670(* change of pc must be left to *_flow execution *)
671; pop_frame: ∀globals.∀ge : genv_gen F globals.
672  (Σi.is_internal_function … ge i) (* current *) → state st_pars → res (state st_pars)
673*)
674
675(*
676lemma sigma_pc_commute:
677 ∀p,p',graph_prog,sigma,gss,st.
678 ∀prf : well_formed_state_pc p p' graph_prog sigma gss st.
679 sigma_pc … (pc ? st) (proj1 … prf) =
680 pc ? (sigma_state_pc … st prf). // qed.
681*)
682
683lemma res_eq_from_opt :
684  ∀A,m,v.res_to_opt A m = return v → m = return v.
685#A * #x #v normalize #EQ destruct % qed.
686
687(*
688lemma if_of_function_commute:
689 ∀p.
690 ∀graph_prog : joint_program (mk_graph_params p).
691 ∀graph_fun : Σi.is_internal_function_of_program … graph_prog i.
692 let graph_fd ≝ if_of_function … graph_fun in
693 let lin_fun ≝ sigma_function_name … graph_fun in
694 let lin_fd ≝ if_of_function … lin_fun in
695 lin_fd = \fst (linearise_int_fun ?? graph_fd).
696 #p #graph_prog #graph_fun whd
697 @prog_if_of_function_transform % qed.
698*)
699lemma bind_option_inversion_star:
700  ∀A,B: Type[0].∀P : Prop.∀f: option A. ∀g: A → option B. ∀y: B.
701  (∀x.f = Some … x → g x = Some … y → P) →
702  (! x ← f ; g x = Some … y) → P.
703#A #B #P #f #g #y #H #G elim (option_bind_inverse ????? G) #x * @H qed.
704
705interpretation "option bind inversion" 'bind_inversion =
706  (bind_option_inversion_star ???????).
707
708lemma sigma_pblock_eq_lemma :
709∀p,p',graph_prog.
710let lin_prog ≝ linearise p graph_prog in
711∀sigma,pc.
712∀prf : well_formed_pc p p' graph_prog sigma pc.
713 pc_block (sigma_pc ? p' graph_prog sigma pc prf) =
714 pc_block pc.
715 #p #p' #graph_prog #sigma #pc #prf
716 whd in match sigma_pc; normalize nodelta
717 @opt_safe_elim #x @'bind_inversion * #i #fn #_
718 @'bind_inversion #n #_ whd in ⊢ (??%?→?);
719 #EQ destruct %
720qed.
721
722(*
723lemma bind_opt_non_none : ∀A,B : Type[0] . ∀ m : option A . ∀g : A → option B.
724(! x ← m ; g x) ≠ None ? → m ≠ None ?.
725#A #B #m #g #H % #m_eq_none cases m >m_eq_none in H; normalize 
726[ #abs elim abs -abs #abs @abs %
727| #abs elim abs -abs #abs #v @abs %
728]
729qed.
730
731lemma match_option_non_none : ∀A ,B, C : Type[0]. ∀m : option A. ∀ x : A.
732∀ b : B .∀ f : A → B. ∀g : B → option C.
733g (match m with [None  ⇒ b  | Some  x ⇒ f x])≠ None ? →  g b = None ? → m ≠ None ?.
734#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
735qed.
736*)
737
738(*
739lemma funct_of_block_transf :
740∀A,B.∀progr : program (λvars .fundef (A vars)) ℕ.
741∀transf : ∀vars. A vars → B vars. ∀bl,f,prf.
742let progr' ≝ transform_program … progr (λvars.transf_fundef … (transf vars)) in
743funct_of_block … (globalenv_noinit … progr) bl = return f →
744funct_of_block … (globalenv_noinit … progr') bl = return «pi1 … f,prf».
745#A #B #progr #transf #bl #f #prf whd
746whd in match funct_of_block in ⊢ (%→?); normalize nodelta
747cut (∀A,B : Type[0].∀Q : option A → Prop.∀P : B → Prop.
748  ∀o.∀prf : Q o.
749  ∀f1,f2.
750  (∀x,prf.P (f1 x prf)) → (∀prf.P(f2 prf)) →
751  P (match o return λx.Q x → B with [ Some x ⇒ f1 x | None ⇒ f2 ] prf))
752  [ #A #B #Q #P * /2/ ] #aux
753@aux [2: #_ change with (?=Some ??→?) #ABS destruct(ABS) ]
754#fd #EQfind whd in ⊢ (??%%→?);
755generalize in ⊢ (??(??(????%))?→?); #e #EQ destruct(EQ)
756whd in match funct_of_block; normalize nodelta
757@aux [ # fd' ]
758[2: >(find_funct_ptr_transf … EQfind) #ABS destruct(ABS) ]
759#prf' cases daemon qed.
760
761lemma description_of_function_transf :
762∀A,B.∀progr : program (λvars .fundef (A vars)) ℕ.
763∀transf : ∀vars. A vars → B vars.
764let progr' ≝ transform_program … progr (λvars.transf_fundef … (transf vars)) in
765∀f_out,prf.
766description_of_function …
767  (globalenv_noinit … progr') f_out =
768transf_fundef … (transf ?) (description_of_function … (globalenv_noinit … progr)
769  «pi1 … f_out, prf»).
770#A #B #progr #transf #f_out #prf
771whd in match description_of_function in ⊢ (???%);
772normalize nodelta
773cut (∀A,B : Type[0].∀Q : option A → Prop.∀P : B → Prop.
774  ∀o.∀prf : Q o.
775  ∀f1,f2.
776  (∀x,prf.o = Some ? x → P (f1 x prf)) → (∀prf.o = None ? → P(f2 prf)) →
777  P (match o return λx.Q x → B with [ Some x ⇒ f1 x | None ⇒ f2 ] prf))
778  [ #A #B #Q #P * /2/ ] #aux
779@aux
780[ #fd' ] * #fd #EQ destruct (EQ)
781inversion (find_symbol ???) [ #_ whd in ⊢ (??%?→?); #ABS destruct(ABS) ]
782#bl #EQfind >m_return_bind #EQfindf
783whd in match description_of_function; normalize nodelta
784@aux
785[ #fdo' ] * #fdo #EQ destruct (EQ)
786>find_symbol_transf >EQfind >m_return_bind
787>(find_funct_ptr_transf … EQfindf) #EQ destruct(EQ) %
788qed.
789
790
791lemma match_int_fun :
792∀A,B : Type[0].∀P : B → Prop.
793∀Q : fundef A → Prop.
794∀m : fundef A.
795∀f1 : ∀fd.Q (Internal \ldots  fd) → B.
796∀f2 : ∀fd.Q (External … fd) → B.
797∀prf : Q m.
798(∀fd,prf.P (f1 fd prf)) →
799(∀fd,prf.P (f2 fd prf)) →
800P (match m
801return λx.Q x → ?
802with
803[ Internal fd ⇒ f1 fd
804| External fd ⇒ f2 fd
805] prf).
806#A #B #P #Q * // qed.
807(*)
808 lemma match_int_fun :
809∀A,B : Type[0].∀P : B → Prop.
810∀m : fundef A.
811∀f1 : ∀fd.m = Internal … fd → B.
812∀f2 : ∀fd.m = External … fd → B.
813(∀fd,prf.P (f1 fd prf)) →
814(∀fd,prf.P (f2 fd prf)) →
815P (match m
816return λx.m = x → ?
817with
818[ Internal fd ⇒ f1 fd
819| External fd ⇒ f2 fd
820] (refl …)).
821#A #B #P * // qed.
822*)
823(*
824lemma prova :
825∀ A.∀progr : program (λvars. fundef (A vars)) ℕ.
826∀ M : fundef (A (prog_var_names (λvars:list ident.fundef (A vars)) ℕ progr)).
827∀ f,g,prf1.
828match M return λx.M = x → option (Σi.is_internal_function_of_program ?? progr i) with
829[Internal fn ⇒ λ prf.return «g,prf1 fn prf» |
830External fn ⇒ λprf.None ? ] (refl ? M) = return f → 
831∃ fn. ∃ prf : M = Internal ? fn . f = «g, prf1 fn prf».
832#H1 #H2 #H3 #H4 #H5 #H6
833@match_int_fun
834#fd #EQ #EQ' whd in EQ' : (??%%); destruct
835%[|%[| % ]] qed.
836*)
837
838lemma int_funct_of_block_transf:
839 ∀A,B.∀progr: program (λvars. fundef (A vars)) ℕ.
840  ∀transf: ∀vars. A vars → B vars. ∀bl,f,prf.
841   let progr' ≝ transform_program … progr (λvars.transf_fundef … (transf vars)) in
842     int_funct_of_block ? (globalenv_noinit … progr) bl = return f →
843     int_funct_of_block ? (globalenv_noinit … progr') bl = return «pi1 … f,prf».
844#A #B #progr #transf #bl #f #prf
845whd whd in match int_funct_of_block in ⊢ (??%?→?); normalize nodelta
846@'bind_inversion #x #x_spec
847@match_int_fun [2: #fd #_ #ABS destruct(ABS) ]
848#fd #EQdescr change with (Some ?? = ? → ?) #EQ destruct(EQ)
849whd in match int_funct_of_block; normalize nodelta
850>(funct_of_block_transf … (internal_function_is_function … prf) … x_spec)
851>m_return_bind
852@match_int_fun #fd' #prf' [ % ]
853@⊥ cases x in prf EQdescr prf'; -x #x #x_prf #prf #EQdescr
854>(description_of_function_transf) [2: @x_prf ]
855>EQdescr whd in ⊢ (??%%→?); #ABS destruct qed.
856*)
857
858axiom symbol_for_block_transf :
859 ∀A,B,V,init.∀prog_in : program A V.
860 ∀trans : ∀vars.A vars → B vars.
861 let prog_out ≝ transform_program … prog_in trans in
862 ∀bl, i.
863 symbol_for_block … (globalenv … init prog_in) bl = Some ? i →
864 symbol_for_block … (globalenv … init prog_out) bl = Some ? i.
865
866lemma fetch_function_transf :
867 ∀A,B,V,init.∀prog_in : program A V.
868 ∀trans : ∀vars.A vars → B vars.
869 let prog_out ≝ transform_program … prog_in trans in
870 ∀bl,i,f.
871 fetch_function … (globalenv … init prog_in) bl =
872  return 〈i, f〉
873→ fetch_function … (globalenv … init prog_out) bl =
874  return 〈i, trans … f〉.
875#A #B #V #init #prog_in #trans #bl #i #f
876 whd in match fetch_function; normalize nodelta
877 #H lapply (opt_eq_from_res ???? H) -H
878 @'bind_inversion #id #eq_symbol_for_block
879 @'bind_inversion #fd #eq_find_funct
880 whd in ⊢ (??%?→?); #EQ destruct(EQ)
881 >(symbol_for_block_transf A B … eq_symbol_for_block) >m_return_bind
882 >(find_funct_ptr_transf A B …  eq_find_funct) >m_return_bind %
883qed.
884
885lemma bind_inversion_star : ∀X,Y.∀P : Prop.
886∀m : res X.∀f : X → res Y.∀v : Y.
887(∀x. m = return x → f x = return v → P) →
888! x ← m ; f x = return v → P.
889#X #Y #P #m #f #v #H #G
890elim (bind_inversion ????? G) #x * @H qed.
891
892interpretation "res bind inversion" 'bind_inversion =
893  (bind_inversion_star ???????).
894
895lemma fetch_internal_function_transf :
896 ∀A,B.∀prog_in : program (λvars.fundef (A vars)) ℕ.
897 ∀trans : ∀vars.A vars → B vars.
898 let prog_out ≝ transform_program … prog_in (λvars.transf_fundef … (trans vars)) in
899 ∀bl,i,f.
900 fetch_internal_function … (globalenv_noinit … prog_in) bl =
901  return 〈i, f〉
902→ fetch_internal_function … (globalenv_noinit … prog_out) bl =
903  return 〈i, trans … f〉.
904#A #B #prog #trans #bl #i #f
905 whd in match fetch_internal_function; normalize nodelta
906 @'bind_inversion * #id * #fd normalize nodelta #EQfetch
907 whd in ⊢ (??%%→?); #EQ destruct(EQ)
908 >(fetch_function_transf … EQfetch) %
909qed.
910 
911(*
912#H elim (bind_opt_inversion ????? H) -H
913#x * whd in match funct_of_block in ⊢ (%→?); normalize nodelta
914@match_opt_prf_elim
915 #H #H1  whd in H : (??%?);
916cases (   find_funct_ptr
917   (fundef
918    (joint_closed_internal_function
919     (graph_prog_params p p' graph_prog
920      (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
921       (linearise_int_fun p) graph_prog stack_sizes))
922     (globals
923      (graph_prog_params p p' graph_prog
924       (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
925        (linearise_int_fun p) graph_prog stack_sizes)))))
926   (ev_genv
927    (graph_prog_params p p' graph_prog
928     (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
929      (linearise_int_fun p) graph_prog stack_sizes)))
930   (pblock (pc (make_sem_graph_params p p') st))) in H; [ 2: normalize #abs destruct
931 
932
933normalize nodelta
934#H #H1
935cases (   find_funct_ptr
936   (fundef
937    (joint_closed_internal_function
938     (graph_prog_params p p' graph_prog
939      (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
940       (linearise_int_fun p) graph_prog stack_sizes))
941     (globals
942      (graph_prog_params p p' graph_prog
943       (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
944        (linearise_int_fun p) graph_prog stack_sizes)))))
945   (ev_genv
946    (graph_prog_params p p' graph_prog
947     (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
948      (linearise_int_fun p) graph_prog stack_sizes)))
949   (pblock (pc (make_sem_graph_params p p') st))) in H;
950
951
952check find_funct_ptr_transf
953whd in match int_funct_of_block; normalize nodelta
954#H elim (bind_inversion ????? H)
955
956.. sigma_int_funct_of_block
957
958
959
960whd in match int_funct_of_block; normalize nodelta
961elim (bind_inversion ????? H)
962whd in match int_funct_of_block; normalize nodelta
963#H elim (bind_inversion ????? H) -H #fn *
964#H lapply (opt_eq_from_res ???? H) -H
965#H >(find_funct_ptr_transf … (λglobals.transf_fundef … (linearise_int_fun … globals)) … H)
966-H #H >m_return_bind cases fn in H; normalize nodelta #arg #EQ whd in EQ:(??%%);
967destruct //
968cases daemon
969qed. *)
970
971lemma stmt_at_sigma_commute:
972 ∀p,globals,graph_code,entry,lin_code,lbl,pt,sigma.
973 good_local_sigma p globals graph_code entry lin_code sigma →
974 sigma lbl = return pt →
975 ∀stmt.
976   stmt_at … graph_code
977    lbl = return stmt →
978 stmt_at ?? lin_code
979  pt = return graph_to_lin_statement … stmt ∧
980  All … (λl.sigma l ≠ None ?) (stmt_labels … stmt) ∧
981 match stmt with
982 [ final stmt ⇒ True
983 | sequential stmt nxt ⇒
984   (sigma nxt = Some ? (S pt) ∨
985    (stmt_at ?? lin_code
986     (S pt) = return final (mk_lin_params p) … (GOTO … nxt)))
987 ]. 
988 #p #globals #graph_code #entry #lin_code #lbl #pt #sigma
989 * #_ #lin_stmt_spec #prf
990elim (lin_stmt_spec … prf) -lin_stmt_spec #stmt1 *** #EQstmt_at
991#All_succs_in #next_spec
992#EQstmt_at_graph_stmt
993#stmt >EQstmt_at
994whd in ⊢ (??%%→?); #EQ destruct(EQ)
995% [ % assumption ]
996cases stmt in next_spec; -stmt normalize nodelta [2: // ]
997#stmt #nxt
998whd in match opt_All;
999whd in match stmt_implicit_label;
1000normalize nodelta //
1001qed.
1002 
1003(*
1004
1005 >(if_of_function_commute … graph_fun)
1006
1007check opt_Exists
1008check linearise_int_fun
1009check
1010 whd in match (stmt_at ????);
1011 whd in match (stmt_at ????);
1012 cases (linearise_code_spec … p' graph_prog graph_fun
1013         (joint_if_entry … graph_fun))
1014 * #lin_code_closed #sigma_entry_is_zero #sigma_spec
1015 lapply (sigma_spec
1016         (point_of_pointer ? (graph_prog_params … p' graph_prog) (pc … s1)))
1017 -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @(sigma_pc_of_status_ok … prf) |2: skip ]
1018 -sigma_spec #graph_stmt * #graph_lookup_ok >graph_lookup_ok -graph_lookup_ok
1019 whd in ⊢ (? → ???%); #sigma_spec whd in sigma_spec;
1020 inversion (nth_opt ???) in sigma_spec; [ #H whd in ⊢ (% → ?); #abs cases abs ]
1021 * #optlabel #lin_stm #lin_lookup_ok whd in ⊢ (% → ?); ** #_
1022 #related_lin_stm_graph_stm #_ <related_lin_stm_graph_stm -related_lin_stm_graph_stm
1023 <sigma_pc_commute >lin_lookup_ok // *)
1024
1025definition good_sigma :
1026  ∀p.∀graph_prog : joint_program (mk_graph_params p).
1027  (joint_closed_internal_function ? (prog_var_names … graph_prog) →
1028    label → option ℕ) → Prop ≝
1029  λp,graph_prog,sigma.
1030  ∀fn : joint_closed_internal_function (mk_graph_params p) ?.
1031  good_local_sigma ?? (joint_if_code … fn) (joint_if_entry … fn)
1032    (joint_if_code … (\fst (linearise_int_fun … fn))) (sigma fn).
1033
1034lemma pc_of_label_sigma_commute :
1035  ∀p,p',graph_prog,pc,lbl,i,fn.
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_internal_function …
1040    (globalenv_noinit … graph_prog) (pc_block pc) = return 〈i, fn〉 →
1041  let pc' ≝ pc_of_point (make_sem_graph_params p p') … (pc_block pc) lbl in
1042  code_has_label … (joint_if_code … (\fst (linearise_int_fun … fn))) lbl →
1043  ∃prf'.pc_of_label (make_sem_lin_params p p') … (globalenv_noinit … lin_prog)
1044    (pc_block (sigma_pc … pc prf)) lbl =
1045        return sigma_pc p p' graph_prog sigma pc' prf'.
1046#p #p' #graph_prog #pc #lbl #i #fn
1047#sigma #good cases (good fn) -good * #_ #all_labels_in
1048#good #prf #fetchfn >lin_code_has_label #lbl_in
1049whd in match pc_of_label; normalize nodelta
1050>sigma_pblock_eq_lemma
1051> (fetch_internal_function_transf … fetchfn) >m_return_bind
1052inversion (point_of_label ????)
1053[ (*
1054  change with (If ? then with prf do ? else ? = ? → ?)
1055  @If_elim [ #prf' whd in ⊢ (??%?→?); #ABS destruct(ABS) | #ABS >ABS in lbl_in; * ]
1056  *) whd in ⊢ (??%?→?); >lbl_in whd in ⊢ (??%?→?); #ABS destruct(ABS)
1057| #pt #H lapply (all_labels_in … H) #EQsigma >m_return_bind
1058  %
1059  [ @hide_prf whd %
1060  | whd in match sigma_pc; normalize nodelta
1061    @opt_safe_elim #pc'
1062  ]
1063  whd in match sigma_pc_opt; normalize nodelta >fetchfn >m_return_bind
1064  >point_of_pc_of_point
1065  >EQsigma whd in ⊢ (??%?→?); #EQ destruct(EQ) %
1066]
1067qed.
1068
1069lemma graph_pc_of_label :
1070  ∀p,p'.let pars ≝ make_sem_graph_params p p' in
1071  ∀globals,ge,bl,i_fn,lbl.
1072  fetch_internal_function ? ge bl = return i_fn →
1073  pc_of_label pars globals ge bl lbl =
1074    OK ? (pc_of_point pars bl lbl).
1075#p #p' #globals #ge #bl #fn #lbl #fetchfn
1076whd in match pc_of_label; normalize nodelta
1077>fetchfn %
1078qed.
1079
1080lemma graph_succ_pc :
1081  ∀p,p'.let pars ≝ make_sem_graph_params p p' in
1082  ∀pc,lbl.
1083  succ_pc pars pc lbl = pc_of_point pars (pc_block pc) lbl.
1084normalize //
1085qed.
1086
1087lemma fetch_statement_sigma_commute:
1088  ∀p,p',graph_prog,pc,f,fn,stmt.
1089  let lin_prog ≝ linearise ? graph_prog in
1090  ∀sigma.good_sigma p graph_prog sigma →
1091  ∀prf : well_formed_pc p p' graph_prog sigma pc.
1092  fetch_statement (make_sem_graph_params p p') …
1093    (globalenv_noinit ? graph_prog) pc = return 〈f, fn,stmt〉 →
1094  fetch_statement (make_sem_lin_params p p') …
1095    (globalenv_noinit … lin_prog) (sigma_pc … pc prf) =
1096  return 〈f, \fst (linearise_int_fun … fn), graph_to_lin_statement … stmt〉 ∧
1097  All ? (λlbl.well_formed_pc p p' graph_prog sigma
1098      (pc_of_point (make_sem_graph_params p p') (pc_block pc) lbl))
1099    (stmt_explicit_labels … stmt) ∧
1100  match stmt with
1101  [ sequential stmt nxt ⇒
1102    ∃prf'.
1103    let nxt_pc ≝ succ_pc (make_sem_lin_params p p') (sigma_pc … pc prf) it in
1104    let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (make_sem_graph_params p p') pc nxt) prf' in
1105    (nxt_pc = sigma_nxt ∨
1106     fetch_statement (make_sem_lin_params p p') …
1107      (globalenv_noinit … lin_prog) nxt_pc =
1108      return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉)
1109  | final stmt ⇒ True
1110  ].
1111#p #p' #graph_prog #pc #f #fn #stmt #sigma #good
1112elim (good fn) * #_ #all_labels_in #good_local #wfprf
1113#H
1114elim (fetch_statement_inv … H)
1115#fetchfn #graph_stmt
1116whd in match fetch_statement; normalize nodelta
1117>sigma_pblock_eq_lemma
1118>(fetch_internal_function_transf … fetchfn) >m_return_bind
1119whd in match sigma_pc; normalize nodelta @opt_safe_elim
1120#lin_pc whd in match sigma_pc_opt in ⊢ (%→?); normalize nodelta
1121>fetchfn in ⊢ (%→?); >m_return_bind
1122inversion (sigma ??)
1123[ #_ normalize in ⊢ (%→?); #ABS destruct(ABS) ]
1124#lin_pt #EQsigma whd in ⊢ (??%%→?); #EQ destruct(EQ)
1125cases (stmt_at_sigma_commute … (good fn) … EQsigma … graph_stmt) *
1126#H1 #H2 #H3 % [ % ]
1127[ whd in match point_of_pc; normalize nodelta >point_of_offset_of_point
1128  >H1 %
1129| @(All_mp … (All_append_r … H2)) #lbl #prf'
1130 whd whd in match sigma_pc_opt; normalize nodelta
1131 >fetchfn >m_return_bind >point_of_pc_of_point
1132 >(opt_to_opt_safe … prf') % normalize
1133 #ABS destruct(ABS)
1134| cases stmt in H2 H3; normalize nodelta [2: // ]
1135  -stmt #stmt #nxt * #next_in #_ #nxt_spec
1136  % 
1137  [ @hide_prf whd %
1138  | @opt_safe_elim #pc'
1139  ]
1140  >graph_succ_pc whd in ⊢ (??%?→?);
1141  >fetchfn normalize nodelta >point_of_pc_of_point
1142  >(opt_to_opt_safe … next_in) whd in ⊢ (??%?→?); #EQ destruct(EQ)
1143  cases nxt_spec
1144  [ #EQsigma_nxt %1
1145    whd in match (succ_pc ???); whd in match point_of_pc; normalize nodelta
1146    >point_of_offset_of_point lapply next_in >EQsigma_nxt #N %
1147  | #EQstmt_at_nxt %2
1148    whd in match (succ_pc ???);
1149    >(fetch_internal_function_transf … fetchfn) >m_return_bind
1150    whd in match point_of_pc;
1151    normalize nodelta >point_of_offset_of_point >point_of_offset_of_point
1152    whd in match (point_of_succ ???);
1153    >EQstmt_at_nxt %
1154  ]
1155]
1156qed. 
1157
1158lemma point_of_pc_sigma_commute :
1159 ∀p,p',graph_prog.
1160 let lin_prog ≝ linearise p graph_prog in
1161 ∀sigma,pc,f,fn,n.
1162  ∀prf : well_formed_pc p p' graph_prog sigma pc.
1163 fetch_internal_function … (globalenv_noinit … graph_prog) (pc_block pc) = return 〈f, fn〉 →
1164 sigma fn (point_of_pc (make_sem_graph_params p p') pc) = return n →
1165 point_of_pc (make_sem_lin_params p p') (sigma_pc … pc prf) = n.
1166#p #p' #graph_prog #sigma #pc #f #fn #n #prf #EQfetch #EQsigma
1167whd in match sigma_pc; normalize nodelta
1168@opt_safe_elim #pc' whd in match sigma_pc_opt;
1169normalize nodelta >EQfetch >m_return_bind >EQsigma
1170whd in ⊢ (??%?→?); #EQ destruct(EQ)
1171@point_of_offset_of_point
1172qed.
1173
1174definition linearise_status_rel:
1175 ∀p,p',graph_prog.
1176 let lin_prog ≝ linearise p graph_prog in
1177 ∀stack_sizes.
1178 ∀sigma,gss.
1179 good_sigma p graph_prog sigma →
1180   status_rel
1181    (graph_abstract_status p p' graph_prog stack_sizes)
1182    (lin_abstract_status p p' lin_prog stack_sizes)
1183 ≝ λp,p',graph_prog,stack_sizes,sigma,gss,good.
1184   mk_status_rel …
1185    (* sem_rel ≝ *) (λs1,s2.
1186     ∃prf: well_formed_state_pc p p' graph_prog sigma gss s1.
1187      s2 = sigma_state_pc … s1 prf)
1188    (* call_rel ≝ *) (λs1,s2.
1189      ∃prf:well_formed_state_pc p p' graph_prog sigma gss s1.
1190      pc ? s2 = sigma_pc … (pc ? s1) (proj1 … prf))
1191    (* sim_final ≝ *) ?.
1192#st1 #st2 * #prf #EQ2
1193%
1194whd in ⊢ (%→%);
1195#H lapply (opt_to_opt_safe … H)
1196@opt_safe_elim -H
1197#res #_
1198#H lapply (res_eq_from_opt ??? H) -H
1199cases daemon
1200(*#H elim (bind_inversion ????? H) in ⊢ ?;
1201* #f #stmt *
1202whd in ⊢ (??%?→?);*)
1203qed.
1204
1205lemma IO_bind_inversion:
1206  ∀O,I,A,B.∀P : Prop.∀f: IO O I A. ∀g: A → IO O I B. ∀y: B.
1207  (∀x.f = return x → g x = return y → P) →
1208  (! x ← f ; g x = return y) → P.
1209#O #I #A #B #P #f #g #y cases f normalize
1210[ #o #f #_ #H destruct
1211| #a #G #H @(G ? (refl …) H)
1212| #e #_ #H destruct
1213] qed.
1214
1215interpretation "IO bind inversion" 'bind_inversion =
1216  (IO_bind_inversion ?????????).
1217
1218lemma err_eq_from_io : ∀O,I,X,m,v.
1219  err_to_io O I X m = return v → m = return v.
1220#O #I #X * #x #v normalize #EQ destruct % qed.
1221
1222lemma err_eq_to_io : ∀O,I,X,m,v.
1223   m = return v → err_to_io O I X m = return v.
1224#O #I #X #m #v #H >H //
1225qed.
1226
1227lemma set_istack_sigma_commute :
1228∀p,p',graph_prog,sigma,gss,st,is,sigma_is,prf1,prf2.
1229sigma_is_opt p p' graph_prog sigma is = return sigma_is →
1230set_istack ? sigma_is (sigma_state p p' graph_prog sigma gss st prf1) =
1231sigma_state ???? gss (set_istack ? is st) prf2.
1232#p #p' #graph_prog #sigma #gss #st #is #sigmais #prf1 #prf2 #H
1233whd in match set_istack; normalize nodelta
1234whd in match sigma_state; normalize nodelta
1235whd in match sigma_is; normalize nodelta
1236@opt_safe_elim #x #H1
1237cut(x = sigmais) [>H1 in H; #EQ whd in EQ : (???%); destruct(EQ) %]
1238#EQ >EQ //
1239qed.
1240
1241(* this should make things easier for ops using memory (where pc cant happen) *)
1242definition bv_no_pc : beval → Prop ≝
1243λbv.match bv with [ BVpc _ _ ⇒ False | _ ⇒ True ].
1244
1245lemma bv_pc_other :
1246  ∀P : beval → Prop.
1247  (∀pc,p.P (BVpc pc p)) →
1248  (∀bv.bv_no_pc bv → P bv) →
1249  ∀bv.P bv.
1250#P #H1 #H2 * /2/ qed.
1251
1252lemma sigma_bv_no_pc : ∀p,p',graph_prog,sigma,bv,prf.
1253  bv_no_pc bv →
1254  sigma_beval p p' graph_prog sigma bv prf = bv.
1255#p #p' #graph_prog #sigma *
1256[|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p ]
1257#prf * whd in match sigma_beval; normalize nodelta
1258@opt_safe_elim #bv' normalize #EQ destruct(EQ) %
1259qed.
1260
1261lemma is_push_sigma_commute :
1262∀ p, p', graph_prog,sigma,gss,st,val,is,prf1,prf2.
1263(is_push (istack … st) val=return is) →
1264∃prf3.
1265is_push (istack … (sigma_state p p' graph_prog sigma gss st prf1))
1266        (sigma_beval p p' graph_prog sigma val prf2) =
1267return sigma_is p p' graph_prog sigma is prf3.
1268#p #p' #graph_prog #sigma #gss #st #val #is #prf1 #prf2 #H
1269%
1270[ @hide_prf
1271whd in match sigma_is_opt; normalize nodelta
1272inversion (istack ? ?) in H;
1273whd in match is_push; normalize nodelta [3: #a #b #_ #ABS whd in ABS : (???%); destruct(ABS)]
1274[2: #a] #a_spec #EQ whd in EQ : (??%%); destruct(EQ) normalize nodelta
1275inversion (sigma_beval_opt ???? val) [1,3: #ABS >ABS in prf2; * #ABS @⊥ @ABS %]
1276[2: #val' #_ >m_return_bind whd in ⊢ (?(??%?)); % #ABS destruct(ABS)]
1277#val' #_
1278inversion(sigma_beval_opt ???? a)
1279  [2: #val'' #_ >m_return_bind >m_return_bind % #EQ whd in EQ : (??%?); destruct(EQ)]
1280#ABS @⊥ lapply(proj2 … (proj1 … (proj1 … prf1))) >a_spec
1281whd in match sigma_is_opt; normalize nodelta >ABS whd in ⊢ ((?(??%?))→ ?); *
1282#EQ @EQ %
1283]
1284whd in match sigma_state; normalize nodelta
1285cut(is_push (istack (make_sem_graph_params p p') st) val=return is)
1286[ assumption] 
1287#H1 whd in match sigma_is; normalize nodelta
1288@opt_safe_elim #is1 #is1_spec
1289whd in match sigma_beval; normalize nodelta
1290@opt_safe_elim #sigma_val #sigma_val_sepc
1291@opt_safe_elim #sigma_is #sigma_is_spec
1292inversion(istack ? st)
1293[2: #val1|3:#val1 #val2]
1294#H2 >H2 in H1;
1295whd in match is_push; normalize nodelta
1296#EQ whd in EQ : (??%%); destruct(EQ)
1297>H2 in is1_spec; whd in match sigma_is_opt; normalize nodelta
1298#EQ whd in EQ : (??%?); destruct(EQ)
1299normalize nodelta
1300whd in match sigma_is_opt in sigma_is_spec;
1301normalize nodelta in sigma_is_spec;
1302>sigma_val_sepc in sigma_is_spec;
1303[ inversion(sigma_beval_opt ???? val1)
1304[ #ABS #EQ1 whd in EQ1 : (??%%); destruct(EQ1) | #sigma_val1 #H3 >m_return_bind]]
1305>m_return_bind
1306#EQ whd in EQ : (??%?); destruct(EQ) [2: %]
1307>H3 in EQ;
1308normalize nodelta
1309#EQ1 whd in EQ1 : (??%%); destruct(EQ1)
1310normalize nodelta //
1311qed.
1312
1313lemma beopaccs_sigma_commute :
1314∀p,p',graph_prog,sigma,op,val1,val2,opaccs1,opaccs2.
1315∀ prf1 : sigma_beval_opt p p' graph_prog sigma val1 ≠ None ?.
1316∀ prf2 : sigma_beval_opt p p' graph_prog sigma val2 ≠ None ?.
1317be_opaccs op val1 val2=return 〈opaccs1,opaccs2〉 →
1318∃ prf1' : sigma_beval_opt p p' graph_prog sigma opaccs1 ≠ None ?.
1319∃ prf2' : sigma_beval_opt p p' graph_prog sigma opaccs2 ≠ None ?.
1320be_opaccs op (sigma_beval … prf1) (sigma_beval … prf2) =
1321return 〈(sigma_beval … prf1'),(sigma_beval … prf2')〉.
1322#p #p' #graph_prog #sigma #op #val1 #val2
1323#opaccs1 #opaccs2 #prf1 #prf2
1324whd in match be_opaccs; normalize nodelta
1325#H elim(bind_inversion ????? H) -H
1326#x * #x_spec
1327#H elim(bind_inversion ????? H) -H
1328#y * #y_spec
1329#H lapply H #H1 normalize in H; elim(opaccs_implementation op x y) in H;
1330#b1 #b2 #EQ normalize in EQ; destruct(EQ)
1331%
1332[whd in match sigma_beval_opt; normalize nodelta % #ABS
1333whd in ABS : (??%?); destruct(ABS)]
1334%
1335[whd in match sigma_beval_opt; normalize nodelta % #ABS
1336whd in ABS : (??%?); destruct(ABS)]
1337whd in match sigma_beval; normalize nodelta
1338@opt_safe_elim #sigma_val1 #sigma_val1_spec
1339@opt_safe_elim #sigma_val2 #sigma_val2_spec
1340@opt_safe_elim #sigma_op1 #sigma_op1_spec
1341@opt_safe_elim #sigma_op2 #sigma_op2_spec
1342lapply x_spec -x_spec lapply sigma_val1_spec -sigma_val1_spec
1343inversion val1 whd in match Byte_of_val; normalize nodelta
1344[ 1,2,5,6,7: [ 1,2: #_ #_] [3: #a #_ #_] [4,5 : #a #b #_ #_] #ABS whd in ABS : (???%); destruct(ABS)]
1345[#pt1 #pt2 #a #_ #_ #ABS whd in ABS : (???%); destruct(ABS)]
1346#bt_val1 #val1_spec whd in match sigma_beval_opt; normalize nodelta
1347whd in ⊢ ((??%?)→ ?); #EQ destruct(EQ)
1348#EQ whd in EQ : (???%); destruct(EQ)
1349lapply y_spec -y_spec lapply sigma_val2_spec -sigma_val2_spec
1350inversion val2 whd in match Byte_of_val; normalize nodelta
1351[ 1,2,5,6,7: [ 1,2: #_ #_] [3: #a #_ #_] [4,5 : #a #b #_ #_] #ABS whd in ABS : (???%); destruct(ABS)]
1352[#pt1 #pt2 #a #_ #_ #ABS whd in ABS : (???%); destruct(ABS)]
1353#bt_val2 #val2_spec whd in match sigma_beval_opt; normalize nodelta
1354whd in ⊢ ((??%?)→ ?); #EQ destruct(EQ) normalize nodelta
1355#EQ whd in EQ : (???%); destruct(EQ)
1356>m_return_bind >m_return_bind
1357whd in match sigma_beval_opt in sigma_op1_spec;
1358normalize nodelta in sigma_op1_spec;
1359whd in sigma_op1_spec : (??%?); destruct(sigma_op1_spec)
1360whd in match sigma_beval_opt in sigma_op2_spec;
1361normalize nodelta in sigma_op2_spec;
1362whd in sigma_op2_spec : (??%?); destruct(sigma_op2_spec)
1363>H1 %
1364qed.
1365
1366lemma eval_seq_no_pc_sigma_commute :
1367 ∀p,p',graph_prog.
1368 let lin_prog ≝ linearise p graph_prog in
1369 ∀stack_sizes.
1370 ∀sigma.∀gss : good_state_sigma p p' graph_prog sigma.
1371 ∀f,fn,st,stmt,st'.
1372 ∀prf : well_formed_state … gss st.
1373  eval_seq_no_pc … (ev_genv … (graph_prog_params … graph_prog stack_sizes))
1374   f fn stmt st = return st' →
1375  ∃prf'.
1376  eval_seq_no_pc … (ev_genv … (lin_prog_params … lin_prog stack_sizes))
1377    f (\fst (linearise_int_fun … fn)) stmt (sigma_state … gss st prf) =
1378  return sigma_state … gss st' prf'.
1379  #p #p' #graph_prog #stack_sizes #sigma #gss
1380  #fn #st #stmt
1381  #st' #prf
1382  whd in match eval_seq_no_pc;
1383  cases stmt normalize nodelta
1384  [1,2: (* COMMENT, COST_LABEL *) #_ #EQ whd in EQ : (??%%); destruct(EQ) %{prf} //
1385  | (* MOVE *) #mv_sig #H lapply(err_eq_from_io ????? H) -H #H
1386    change with
1387     (pair_reg_move p (joint_closed_internal_function (make_sem_graph_params p p'))
1388                      (make_sem_graph_params p p') ??) in H : (??%?);
1389    lapply H -H
1390    whd in match pair_reg_move; normalize nodelta #H
1391    elim(bind_inversion ????? H) -H #reg * #reg_spec #EQ whd in EQ : (??%%); destruct(EQ)
1392    elim(pair_reg_move_commute ???????? (proj2 … (proj1 … prf)) reg_spec)
1393    #wf_regs #pm_spec >pm_spec >m_return_bind % [2: %]
1394    % [ 2: @(proj2 … prf)
1395      |    % [2: assumption] %
1396             [ @(proj1 … (proj1 … (proj1 … prf)))
1397             | @(proj2 … (proj1 … (proj1 … prf)))
1398             ]
1399      ]
1400  | (* POP *)
1401    #a #H lapply(err_eq_from_io ????? H) -H #H elim (bind_inversion ????? H) -H
1402    * #val #st1 * #vals_spec #H
1403    change with (acca_store p
1404                          (joint_closed_internal_function (make_sem_graph_params p p'))
1405                          (make_sem_graph_params p p') a val st1 = ?) in H;
1406    change with (pop (make_sem_graph_params p p') ? = ?) in vals_spec;
1407    lapply vals_spec -vals_spec
1408    whd in match pop; normalize nodelta
1409    whd in match is_pop; normalize nodelta
1410    lapply(proj2 … (proj1 … (proj1 … prf))) #wf_is
1411    inversion (istack (make_sem_graph_params p p') st) normalize nodelta
1412    [#_ #ABS normalize in ABS; destruct(ABS)]
1413    [ #Bv | #Bv_not_used #Bv] #is_stack_st_spec >m_return_bind
1414    #EQ whd in EQ : (??%%); destruct(EQ)
1415    elim(store_commute p p' graph_prog sigma ?? gss (acca_store__commute … gss) ?????? H)
1416    [ 2,5: @hide_prf >is_stack_st_spec in wf_is; #wf_is
1417           whd in match sigma_is_opt in wf_is; normalize nodelta in wf_is;
1418           inversion(sigma_beval_opt ?????)
1419           [1,3 : #EQ >EQ in wf_is; whd in ⊢ ((?(??%?)) → ?); * #ABS @⊥ @ABS //
1420                  inversion(sigma_beval_opt ?????) normalize nodelta
1421                  [ #bev %
1422                  | #bev #bev_s >bev_s in ABS; normalize nodelta
1423                    #ABS @⊥ @ABS normalize %
1424                  ]
1425           ]
1426           [#H1 #H2 % #ABS destruct(ABS) | #H1 #H2 % #ABS destruct(ABS)]
1427    ]
1428    [ 2,4: @hide_prf % [2,4 : @(proj2 … prf)] % [2,4 : @(proj2 … (proj1 … prf))]
1429             % [1,3 : @(proj1 … (proj1 … (proj1 … prf)))]
1430             whd in match sigma_is_opt; normalize nodelta
1431             [ whd in ⊢ (? (??%?)); % #ABS destruct(ABS)]
1432             >is_stack_st_spec in wf_is;
1433             whd in match sigma_is_opt; normalize nodelta
1434             cases(sigma_beval_opt ?????)
1435             [ normalize * #ABS @⊥ @ABS %
1436             | #bev #_ normalize % #ABS destruct(ABS)
1437             ]
1438     ] 
1439     #prf' #acca_store_commute %{prf'}     
1440    whd in match sigma_state in ⊢ (??(????(?????(?????%?)?))?);
1441    whd in match sigma_is; normalize nodelta
1442    @opt_safe_elim #int_stack #int_stack_sigma_spec
1443    >is_stack_st_spec in int_stack_sigma_spec;
1444    whd in match sigma_is_opt; normalize nodelta
1445    #IS_SPEC elim(bind_opt_inversion ????? IS_SPEC) -IS_SPEC
1446    [ #sigma_bv * #sigma_bv_spec #EQ whd in EQ : (??%%); destruct(EQ)
1447    | #sigma_bv_not_used * #sigma_bv_not_used_spec #IS_SPEC
1448      elim(bind_opt_inversion ????? IS_SPEC) -IS_SPEC
1449      #sigma_bv * #sigma_bv_spec #EQ whd in EQ : (??%%); destruct(EQ)]
1450      normalize nodelta >m_return_bind
1451      @err_eq_to_io <acca_store_commute
1452      whd in match helper_def_store; normalize nodelta
1453      whd in match acca_store; normalize nodelta
1454      whd in match sigma_beval; normalize nodelta
1455     @opt_safe_elim #xx #xx_spec
1456     [  >xx_spec in sigma_bv_spec; #EQ destruct(EQ) //
1457     | cut(xx =sigma_bv) [>xx_spec in sigma_bv_spec; #EQ destruct(EQ) %]
1458       #EQ >EQ @m_bind_ext_eq #reg
1459       change with (return set_regs (make_sem_lin_params p p') ?
1460                                   (set_istack (make_sem_lin_params p p') ? ?) = ?);
1461       change with (? = return set_regs ? ?
1462                   (sigma_state p p' graph_prog sigma gss
1463                   (set_istack ? (one_is Bv_not_used) st) ?))
1464       >(set_istack_sigma_commute ?????? (one_is Bv_not_used) (one_is sigma_bv_not_used) ???)
1465       [2: whd in match sigma_is_opt; normalize nodelta >sigma_bv_not_used_spec
1466           >m_return_bind whd in ⊢ (??%%); % | % |]
1467     ]
1468  | (* PUSH *)
1469     #a #H lapply(err_eq_from_io ????? H) -H #H elim (bind_inversion ????? H) -H
1470     #val *
1471     change with (((acca_arg_retrieve p
1472                (joint_closed_internal_function (make_sem_graph_params p p'))
1473                 (make_sem_graph_params p p') st a) = ?) → ?)
1474     #graph_ret_spec
1475     change with (((push (make_sem_graph_params p p') ? ?) = ?) → ?)
1476     #graph_push_spec
1477     elim (retrieve_commute p p' graph_prog sigma ?? gss (acca_arg_retrieve_commute … gss)??? prf graph_ret_spec)
1478     #val_wf #acca_arg_retrieve_commute
1479     whd in match push in graph_push_spec; normalize nodelta  in graph_push_spec;
1480     elim(bind_inversion ????? graph_push_spec) -graph_push_spec
1481     #int_stack * #int_stack_spec #EQ whd in EQ : (??%%); destruct(EQ)
1482     %
1483     [ @hide_prf % [% [% [ @(proj1 … (proj1 … (proj1 … prf))) ]]]
1484       [2: @(proj2 … (proj1 … prf))] [2: @(proj2 … prf)]
1485       lapply int_stack_spec -int_stack_spec
1486       cases int_stack
1487       [  whd in match is_push; normalize nodelta 
1488          cases(istack ? ?) normalize nodelta
1489          [2: #x ] [3: #x #y] #EQ whd in EQ : (??%%); destruct(EQ)
1490       |2,3: [#x | #y #x ] whd in match is_push; normalize nodelta
1491        inversion(istack ? ?) normalize nodelta
1492        [ #_ #EQ whd in EQ : (??%%); destruct(EQ)
1493           whd in match sigma_is_opt; normalize nodelta
1494           inversion(sigma_beval_opt ?????)
1495           [  #EQ @⊥ elim val_wf #H @H //
1496           |  #z #_ >m_return_bind % #ABS whd in ABS : (??%?); destruct(ABS)
1497           ]
1498        | #x #_ #ABS whd in ABS : (??%%); destruct(ABS)
1499        | #x #y #_ #ABS whd in ABS : (???%); destruct(ABS)
1500        | #_ #ABS whd in ABS : (??%%); destruct(ABS)
1501        | #z #H #EQ whd in EQ : (??%%); destruct(EQ)
1502          whd in match sigma_is_opt; normalize nodelta
1503          inversion(sigma_beval_opt ???? y)
1504          [ #ABS @⊥ lapply(proj2 … (proj1 … (proj1 … prf)))
1505         xxxxxxxxxxxxxxxxxx
1506       
1507 qed.       
1508
1509lemma eval_statement_no_pc_sigma_commute :
1510 ∀p,p',graph_prog.
1511 let lin_prog ≝ linearise p graph_prog in
1512 ∀stack_sizes.
1513 ∀sigma.∀gss : good_state_sigma p p' graph_prog sigma.
1514 ∀f,fn,st,stmt,st'.
1515 ∀prf : well_formed_state … gss st.
1516  eval_statement_no_pc … (ev_genv … (graph_prog_params … graph_prog stack_sizes))
1517   f fn stmt st = return st' →
1518  ∃prf'.
1519  eval_statement_no_pc … (ev_genv … (lin_prog_params … lin_prog stack_sizes))
1520    f (\fst (linearise_int_fun … fn)) (graph_to_lin_statement … stmt)
1521       (sigma_state … gss st prf) =
1522  return sigma_state … gss st' prf'.
1523  #p #p' #graph_prog #stack_sizes #sigma #gss
1524  #f #fn #st * [* [ #stmt | #a #lbl ] #nxt | * [ #lbl | | #fl #called #args ]]
1525  #st' #prf
1526  whd in match eval_statement_no_pc; normalize nodelta
1527  [ @eval_seq_no_pc_sigma_commute
1528  |2,3,4: whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} %
1529  | (* tailcall, follow proof of CALL in previous lemma *)
1530    cases daemon
1531  ]
1532qed.
1533
1534=======
1535           whd in match sigma_is_opt; >H normalize nodelta >ABS
1536           whd in ⊢ ((?(??%?))→?); * #h1 @h1 %
1537          | #sigma_y #H >m_return_bind
1538            cases (sigma_beval_opt ? ? ? ? x) in val_wf; [ * #ABS @⊥ @ABS %]
1539            #sigma_y' #_ >m_return_bind whd in ⊢ (?(??%?)); % #H destruct(H)
1540          ]
1541        | #a1 #a2 #_ #EQ whd in EQ : (???%); destruct(EQ)
1542          ]
1543        ]
1544     |
1545        whd in match helper_def_retrieve in acca_arg_retrieve_commute;
1546        normalize nodelta in acca_arg_retrieve_commute;
1547        whd in match acca_arg_retrieve; normalize nodelta
1548        @err_eq_to_io
1549        change with
1550        ((! v ← (acca_arg_retrieve_ p
1551                                      (joint_closed_internal_function (make_sem_lin_params p p'))
1552                                      (make_sem_lin_params p p')
1553                                      (regs (make_sem_lin_params p p')
1554                                         (sigma_state p p' graph_prog sigma gss st prf))
1555                                      a);
1556          ?)=?)
1557          change with ((! v ← ?; push (make_sem_lin_params p p') ? ?) = ?)
1558          cut((acca_arg_retrieve_ p ? ? ? a) = return sigma_beval p ? ? ? ? val_wf)
1559          [4: assumption | | | | ] #H >H >m_return_bind
1560          whd in match push; normalize nodelta
1561          -H elim(is_push_sigma_commute ???????? prf val_wf int_stack_spec)
1562          #wf_is #EQ >EQ >m_return_bind //
1563     ]
1564  | (*C_ADDRESS*)
1565    #sy
1566    change with ((member ? ? (prog_var_names (joint_function (mk_graph_params p)) ℕ graph_prog)) → ?)
1567    #sy_prf
1568    change with ((dpl_reg p) → ?) #dpl 
1569    change with ((dph_reg p) → ?) #dph
1570    #H lapply(err_eq_from_io ????? H) -H
1571    change with ((( ! st1 ← dpl_store p
1572                                     (joint_closed_internal_function (make_sem_graph_params p p'))
1573                                     (make_sem_graph_params p p')
1574                                     ?
1575                                     ?
1576                                     ? ; ? ) = ?) → ?)
1577    change with ((( ! st1 ← dpl_store ????
1578    (BVptr
1579      (mk_pointer
1580         (opt_safe block
1581           (find_symbol
1582              (fundef
1583                 (joint_closed_internal_function
1584                    (make_sem_graph_params p p')
1585                    ?
1586                  )
1587               )
1588               (globalenv_noinit ? graph_prog)
1589               ?
1590           )
1591           ?
1592         )
1593         ?
1594      )
1595      ?
1596    ) ? ; ?) = ?) → ?)
1597    change with ((( ! st1 ← ? ;
1598        dph_store p (joint_closed_internal_function (make_sem_graph_params p p'))
1599                  (make_sem_graph_params p p') ?
1600                  (BVptr
1601      (mk_pointer
1602         (opt_safe block
1603           (find_symbol
1604              (fundef
1605                 (joint_closed_internal_function
1606                    (make_sem_graph_params p p')
1607                    ?
1608                  )
1609               )
1610               (globalenv_noinit ? graph_prog)
1611               ?
1612           )
1613           ?
1614         )
1615         ?
1616      )
1617      ?
1618    ) ?) = ?) → ?)
1619    #H elim(bind_inversion ????? H) -H
1620    #st1 * #dpl_st1
1621    elim(store_commute p p' graph_prog sigma ?? gss (dpl_store_commute … gss) ???? prf ? dpl_st1)
1622    [2: @hide_prf whd in match sigma_beval_opt; normalize nodelta whd in ⊢ (?(??%?)); %
1623        #ABS destruct(ABS)]
1624    #wf_st1 whd in match helper_def_store; normalize nodelta
1625    #H elim(bind_inversion ????? H) -H #reg1 * #reg1_spec #EQ whd in EQ : (??%%);
1626    destruct(EQ) -EQ
1627    #dph_st'
1628    elim(store_commute p p' graph_prog sigma ?? gss (dph_store_commute … gss) ???? wf_st1 ? dph_st')
1629    [2: @hide_prf whd in match sigma_beval_opt; normalize nodelta whd in ⊢ (?(??%?));
1630        % #ABS destruct(ABS)]
1631    #wf_st' whd in match helper_def_store; normalize nodelta
1632    #H elim(bind_inversion ????? H) -H #reg2 * #reg2_spec #EQ whd in EQ : (??%%);
1633    destruct(EQ) -EQ %{wf_st'} <e1
1634    whd in match dpl_store; normalize nodelta
1635    whd in match sigma_beval in reg1_spec; normalize nodelta in reg1_spec;
1636    whd in match sigma_beval_opt in reg1_spec; normalize nodelta in reg1_spec;
1637    lapply reg1_spec -reg1_spec @opt_safe_elim #x #EQ whd in EQ : (??%?);
1638    destruct(EQ) @opt_safe_elim #block_graph #block_graph_spec
1639    #reg1_spec @opt_safe_elim #block_lin #block_lin_spec
1640    cut(find_symbol
1641         (fundef
1642            (joint_closed_internal_function
1643                (make_sem_lin_params p p')
1644                (prog_var_names (joint_function (mk_lin_params p)) ℕ (linearise … graph_prog))
1645            )
1646          )
1647          (globalenv_noinit (joint_function (mk_lin_params p)) (linearise … graph_prog))
1648          sy
1649          =
1650          find_symbol
1651            (fundef
1652               (joint_closed_internal_function
1653                   (make_sem_graph_params p p')
1654                   (prog_var_names (joint_function (mk_graph_params p)) ℕ graph_prog)
1655               )
1656            )
1657            (globalenv_noinit (joint_function (mk_graph_params p)) graph_prog)
1658            sy)   
1659    [ @find_symbol_transf]
1660    #find_sym_EQ >find_sym_EQ in block_lin_spec; >block_graph_spec
1661    #EQ destruct(EQ) >reg1_spec >m_return_bind
1662    whd in match dph_store; normalize nodelta
1663    lapply reg2_spec -reg2_spec
1664    whd in match sigma_beval; normalize nodelta
1665    @opt_safe_elim #y
1666    whd in match sigma_beval_opt; normalize nodelta
1667    whd in ⊢((??%?)→?); #EQ destruct(EQ)
1668    @opt_safe_elim #graph_block >block_graph_spec
1669    #EQ destruct(EQ) #reg2_spec
1670    cut(sigma_state p p' graph_prog sigma gss st1 wf_st1 =
1671    (set_regs (lin_prog_params p p' (linearise p graph_prog) stack_sizes)
1672          reg1 (sigma_state p p' graph_prog sigma gss st prf)))
1673    [whd in match set_regs; normalize nodelta >e0 %]
1674    #sigma_st1_spec <sigma_st1_spec >reg2_spec
1675    >m_return_bind %
1676  | (*C_OPACCS*)
1677    #op #a #b #arg1 #arg2
1678    #H lapply(err_eq_from_io ????? H) -H
1679    #H elim(bind_inversion ????? H) -H
1680    #val1 * #val1_spec
1681    elim (retrieve_commute p p' graph_prog sigma ?? gss (acca_arg_retrieve_commute … gss)??? prf val1_spec)
1682    #wf_val1 #sigma_val1_commute
1683    #H elim(bind_inversion ????? H) -H
1684    #val2 * #val2_spec
1685    elim (retrieve_commute p p' graph_prog sigma ?? gss (accb_arg_retrieve_commute … gss)??? prf val2_spec)
1686    #wf_val2 #sigma_val2_commute
1687    #H elim(bind_inversion ????? H) -H *
1688    #opaccs1 #opaccs2 * #opaccs_spec
1689    elim(beopaccs_sigma_commute p p' graph_prog sigma ????? wf_val1 wf_val2 opaccs_spec)
1690    #wf_opaccs1 * #wf_opaccs2 #be_opaccs_commute
1691    #H elim(bind_inversion ????? H) -H
1692    #st1 * #st1_spec
1693    elim(store_commute p p' graph_prog sigma ?? gss (acca_store__commute … gss) ???? prf wf_opaccs1 st1_spec)
1694    #wf_st1 #sigma_st1_commute #final_spec
1695    elim(store_commute p p' graph_prog sigma ?? gss (accb_store_commute … gss) ???? wf_st1 wf_opaccs2 final_spec)
1696    #wf_st' #sigma_final_commute
1697    %{wf_st'}
1698    whd in match helper_def_retrieve in sigma_val1_commute;
1699    normalize nodelta in sigma_val1_commute;
1700    whd in match acca_arg_retrieve; normalize nodelta
1701    >sigma_val1_commute >m_return_bind
1702    whd in match helper_def_retrieve in sigma_val2_commute;
1703    normalize nodelta in sigma_val2_commute;
1704    whd in match accb_arg_retrieve; normalize nodelta
1705    >sigma_val2_commute >m_return_bind
1706    >be_opaccs_commute >m_return_bind
1707    whd in match helper_def_store in sigma_st1_commute;
1708    normalize nodelta in sigma_st1_commute;
1709    elim(bind_inversion ????? sigma_st1_commute)
1710    #reg1 * #reg1_spec #EQ whd in EQ : (??%%); destruct(EQ)
1711    whd in match acca_store; normalize nodelta
1712    >reg1_spec >m_return_bind
1713    whd in match set_regs; normalize nodelta >e0
1714    whd in match helper_def_store in sigma_final_commute;
1715    normalize nodelta in sigma_final_commute;
1716    elim(bind_inversion ????? sigma_final_commute)
1717    #reg2 * #reg2_spec #EQ whd in EQ : (??%%); destruct(EQ)
1718    whd in match accb_store; normalize nodelta
1719    >reg2_spec >m_return_bind whd in match set_regs; normalize nodelta
1720    >e1 %
1721  | (*C_OP1*)
1722   
1723>>>>>>> .r2528
1724inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
1725    ex1_intro: ∀ x:A. P x →  ex_Type1 A P.
1726(*interpretation "exists in Type[1]" 'exists x = (ex_Type1 ? x).*)
1727
1728lemma linearise_ok:
1729 ∀p,p',graph_prog.
1730  let lin_prog ≝ linearise ? graph_prog in
1731 ∀stack_sizes.
1732 (∀sigma.good_state_sigma p p' graph_prog sigma) →
1733   ex_Type1 … (λR.
1734   status_simulation
1735    (graph_abstract_status p p' graph_prog stack_sizes)
1736    (lin_abstract_status p p' lin_prog stack_sizes) R).
1737 #p #p' #graph_prog
1738 letin sigma ≝ (λfn.\snd (linearise_int_fun … fn) : sigma_map … graph_prog)
1739 cut (∀fn.good_local_sigma … (sigma fn))
1740  [6: #fn @(pi2 … (linearise_int_fun … fn)) |*:]
1741 #good
1742 #stack_sizes
1743 #gss lapply (gss sigma) -gss #gss
1744 %{(linearise_status_rel p p' graph_prog stack_sizes sigma gss good)}
1745whd in match graph_abstract_status;
1746whd in match lin_abstract_status;
1747whd in match graph_prog_params;
1748whd in match lin_prog_params;
1749normalize nodelta
1750whd
1751whd in ⊢ (%→%→%→?);
1752whd in ⊢ (?(?%)→?(?%)→?(?%)→?);
1753whd in ⊢ (?%→?%→?%→?);
1754#st1 #st1' #st2
1755whd in ⊢ (%→?);
1756change with
1757  (eval_state (make_sem_graph_params p p') (prog_var_names ???) ?? = ? → ?)
1758whd in match eval_state in ⊢ (%→?); normalize nodelta
1759@'bind_inversion
1760** #curr_f #curr_fn #stmt #H lapply (err_eq_from_io ????? H) -H #EQfetch_stmt
1761cases (fetch_statement_inv … EQfetch_stmt) #EQfetchfn #_
1762@'bind_inversion
1763#st1_no_pc' #ex lapply (err_eq_from_io ????? ex) -ex #ex #ex_advance
1764* #wf_prf #st2_EQ
1765
1766cases (fetch_statement_sigma_commute … good … (hide_prf … (proj1 … wf_prf)) EQfetch_stmt)
1767* #EQfetch_stmt' #all_labels_in
1768
1769letin lin_prog ≝ (linearise … graph_prog)
1770lapply (refl … (eval_state …  (ev_genv (mk_prog_params (make_sem_lin_params p p') lin_prog stack_sizes)) st2))
1771whd in match eval_state in ⊢ (???%→?);
1772>st2_EQ in ⊢ (???%→?); normalize nodelta
1773>EQfetch_stmt' in ⊢ (%→?); >m_return_bind in ⊢ (???%→?);
1774cases (eval_statement_no_pc_sigma_commute … gss … (hide_prf … (proj2 … wf_prf)) ex) in ⊢ ?;
1775#wf_st1_no_pc_prf #ex' >ex' in ⊢ (???%→?); >m_return_bind in ⊢ (???%→?);
1776
1777whd in match (as_classify ??) in ⊢ (?→?→match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
1778>EQfetch_stmt in ⊢ (?→?→match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
1779normalize nodelta
1780
1781cases stmt in ex ex_advance; -stmt whd in match graph_to_lin_statement;
1782normalize nodelta
1783[ whd in match joint_classify_step; @cond_call_other
1784  [ (* COND *) #a #lbltrue #nxt
1785    #ex whd in match eval_statement_advance in ⊢ (%→%→?); normalize nodelta
1786    #H @('bind_inversion (err_eq_from_io ????? H)) -H @bv_pc_other
1787    [ #bv_pc #p #bv whd in ⊢ (??%%→?); #ABS destruct(ABS) ]
1788    #bv #bv_no_pc #EQretrieve
1789    cases (retrieve_commute … (acca_retrieve_commute … gss) … wf_st1_no_pc_prf … EQretrieve)
1790    #ignore >(sigma_bv_no_pc … bv_no_pc)
1791    change with (acca_retrieve ?? (make_sem_lin_params p p') ?? = ? → ?)
1792    #EQretrieve' >EQretrieve' in ⊢ (?→%→?); >m_return_bind in ⊢ (?→%→?);
1793    #H @('bind_inversion H) -H * normalize nodelta #EQbool_of_bv
1794    >EQbool_of_bv in ⊢ (?→%→?); >m_return_bind in ⊢ (?→%→?); normalize nodelta
1795    [ whd in match goto; normalize nodelta
1796      >(graph_pc_of_label … EQfetchfn) whd in ⊢ (??%%→?);
1797      #EQ destruct(EQ) #ex_advance #ex_advance'
1798      % [2: %{(tal_base_not_return …)} [3: @ex_advance'
1799  | (* CALL *) #f #args #dest #nxt
1800  | (* other *) #stmt #no_call #nxt
1801  ] normalize nodelta
1802  [ #ex
1803    #ex_advance #ex_advance'
1804  | whd in ⊢ (??%%→?); #EQ destruct(EQ)
1805    #H @('bind_inversion H) -H #called_block
1806    #H lapply (err_eq_from_io ????? H) -H #EQcalled_block
1807    #H @('bind_inversion H) -H * #called * #called_fn
1808    #H lapply (err_eq_from_io ????? H) -H #EQcalled
1809    normalize nodelta
1810    [ #H lapply (err_eq_from_io ????? H) -H ]
1811    #H @('bind_inversion H) -H
1812     | @('bind_inversion H) ] -H #st1_no_pc'' #save_frame_EQ ]
1813    #ex_advance #ex_advance'
1814    whd in match joint_classify_seq; normalize nodelta
1815    >EQcalled_block in ⊢ (?→match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
1816   
1817    cut (∀p,p',graph_prog,sigma,gss,st,f,bl.
1818        ∀prf : well_formed_state p p' graph_prog sigma gss st.
1819        block_of_call (make_sem_graph_params p p') ?
1820          (globalenv_noinit ? graph_prog) st f = return bl →
1821        block_of_call (make_sem_lin_params p p') ?
1822          (globalenv_noinit ? (linearise … graph_prog))
1823          (sigma_state … st prf) f = return bl)
1824      [1,3: (*TODO lemma *) cases daemon ] #block_of_call_sigma_commute
1825      whd in match eval_seq_advance; normalize nodelta
1826      >(block_of_call_sigma_commute … EQcalled_block) in ⊢ (???%→?);
1827      >m_return_bind in ⊢ (???%→?);
1828      >(fetch_function_transf … EQcalled :
1829        fetch_function … (globalenv_noinit … lin_prog) called_block = ?) in ⊢ (???%→?);
1830      >m_return_bind in ⊢ (???%→?);
1831      whd in match (transf_fundef); normalize nodelta
1832       
1833       
1834      #block_of_call_sigma_commute
1835    @match_int_fun #called_descr #EQcalled_descr
1836    [ #H @('bind_inversion H) -H #st1_frame_saved #EQ_frame_saved ]
1837    #ex_advance
1838    cut
1839      (∀A,B.∀prog : program (λvars.fundef (A vars)) ℕ.
1840      ∀trans : ∀vars.A vars → B vars.
1841      let prog_out : program (λvars.fundef (B vars)) ℕ ≝
1842        transform_program ??? prog (λvars.transf_fundef … (trans vars)) in
1843      ∀i.is_function … (globalenv_noinit … prog) i →
1844       is_function … (globalenv_noinit … prog_out) i) [1,3: (* TODO lemma *) cases daemon ]
1845    #f_propagate
1846    letin sigma_function ≝ (λA,B,prog,trans.
1847      λf : Σi.is_function ? (globalenv_noinit ? prog) i.
1848      «pi1 ?? f, f_propagate A B prog trans ? (pi2 ?? f)») in ⊢ ?; (* TODO def *)
1849    cut (∀p,p',graph_prog.
1850      let lin_prog ≝ linearise ? graph_prog in
1851      ∀sigma.∀gss : good_state_sigma … graph_prog sigma.
1852      ∀f,st,fn.
1853      ∀prf : well_formed_state … gss st.
1854      function_of_call (make_sem_graph_params p p') … (globalenv_noinit … graph_prog)
1855        st f = return fn →
1856      function_of_call (make_sem_lin_params p p') … (globalenv_noinit … lin_prog)
1857        (sigma_state … gss st prf) f = return sigma_function … fn)
1858        [1,3: (* TODO lemma *) cases daemon ]
1859    #function_of_call_sigma_commute
1860    whd in match joint_classify_step; whd in match joint_classify_seq;
1861    normalize nodelta #next_spec
1862    >(function_of_call_sigma_commute … EQcalled) in ⊢ (%→?);
1863    >m_return_bind in ⊢ (%→?);
1864    @match_int_fun
1865    [2,3: #EQdescr' lapply EQdescr'
1866      >description_of_function_transf in EQdescr';
1867     
1868   
1869    whd in match sigma_beval; normalize nodelta
1870    cases bv
1871    [|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #bv_pc #p ]
1872    whd in match (sigma_beval_opt ?????) in ⊢ (%→%→?);
1873    [7: #ignore #_
1874    #ignore whd in match (opt_safe ???) in ⊢ (%→?); #EQretrieve
1875    whd in match (bool_of_beval ?) in ⊢ (% → ?);
1876    3: >no_call_advance [2: @no_call]
1877 
1878
1879
1880generalize in match wf_pc in ⊢ ?;
1881whd in ⊢ (%→?);
1882inversion (sigma_pc_opt ?????) in ⊢ (%→?); [ #_ * #ABS elim (ABS ?) % ]
1883#lin_pc
1884whd in match (sigma_pc_opt) in ⊢ (%→?); normalize nodelta
1885>EQfunc_of_block in ⊢ (%→?); >m_return_bind in ⊢ (%→?);
1886#H elim (bind_opt_inversion ????? H) in ⊢ ?; -H #lin_pt *
1887#EQsigma whd in ⊢ (??%?→?); #EQ destruct(EQ) #_
1888elim (good_local … EQsigma) -good_local
1889#stmt' *
1890change with (stmt_at ?? (joint_if_code ?? graph_fun) ? = ? → ?)
1891>EQstmt_at #EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ)
1892#H elim (opt_Exists_elim … H) -H * #lbl_opt #lin_stmt normalize nodelta
1893>(prog_if_of_function_transform … fn) in ⊢ (%→?); [2: % ]
1894change with graph_fun in match (if_of_function ?? fn) in ⊢ (%→?);
1895letin lin_fun ≝ (\fst  (linearise_int_fun p globals graph_fun))
1896change with globals in match (prog_var_names ?? graph_prog) in ⊢ (%→?);
1897*
1898#EQnth_opt ** #opt_lbl_spec #EQ destruct(EQ) #next_spec
1899destruct(EQst2)
1900whd in match eval_state in ⊢ (???%→?); normalize nodelta
1901(* resolve classifier *)
1902[ *
1903  [ #stmt #nxt
1904    whd in match eval_statement in ⊢ (?→%→?); normalize nodelta
1905    #EQfetch #EQeval #EQstmt_at #EQnth_opt #next_spec
1906    whd in match (graph_to_lin_statement ???) in ⊢ (%→?);
1907    whd in match eval_statement in ⊢ (%→?); normalize nodelta
1908    elim (IO_bind_inversion ??????? EQeval) #st1_no_pc *
1909    #EQeval_no_pc #EQeval_pc
1910    >(eval_seq_no_pc_sigma_commute … EQeval_no_pc)
1911    [2: (*TODO lemma eval_seq_no_pc_wf *) @hide_prf cases daemon ]
1912        >m_return_bind
1913    cases stmt in EQfetch EQeval_no_pc EQeval_pc EQstmt_at EQnth_opt next_spec;
1914    [14: #f #args #dest
1915    | #c
1916    | #lbl
1917    | #move_sig
1918    | #a
1919    | #a
1920    | #sy #sy_prf #dpl #dph
1921    | #op #a #b #arg1 #arg2
1922    | #op #a #arg
1923    | #op #a #arg1 #arg2
1924    ||
1925    | #a #dpl #dph
1926    | #dpl #dph #a
1927    | #s_ext
1928    ]
1929    [ (* CALL *)
1930    |(*:*)
1931      normalize nodelta
1932      #EQfetch #EQeval_no_pc #EQeval_pc #EQstmt_at #EQnth_opt #next_spec
1933      whd in match eval_seq_pc; normalize nodelta
1934      #ex1
1935      cases next_spec
1936      [ #EQnext_sigma
1937        %[2: %{(taaf_step … (taa_base …) ex1 ?)}
1938         [ cases daemon (* TODO lemma joint_classify_sigma_commute *) ]|]
1939        normalize nodelta
1940        cut (? : Prop) [3: #R' % [ %{I R'} ] |*:]
1941        [ cases daemon (* TODO lemma joint_label_sigma_commute *)
1942        | %
1943          [ (* TODO lemma well_formed_state_pc_preserve? *) @hide_prf cases daemon
1944          | whd in match eval_seq_pc in EQeval_pc;
1945            whd in EQeval_pc : (??%%); whd in EQeval_pc : (??(????%)?);
1946            destruct (EQeval_pc)
1947            whd in ⊢ (??%%);
1948            change with (sigma_pc ??????) in match
1949              (pc ? (sigma_state_pc ???????));
1950            whd in match (succ_pc ????) in ⊢ (??%%);
1951            whd in match (point_of_succ ???) in ⊢ (??%%);
1952            >(point_of_pc_sigma_commute … EQfunc_of_block EQsigma)
1953            whd in match sigma_pc in ⊢ (???%);
1954            whd in match sigma_pc_opt in ⊢ (???%); normalize nodelta
1955            @opt_safe_elim #pc'
1956            >EQfunc_of_block >m_return_bind
1957            whd in match point_of_pc; normalize nodelta
1958            >point_of_offset_of_point
1959            >EQnext_sigma whd in ⊢ (??%?→?);
1960            whd in match pc_of_point; normalize nodelta
1961            #EQ destruct(EQ)
1962            >sigma_pblock_eq_lemma %
1963          ]
1964        ]
1965      | -next_spec #next_spec
1966        %
1967     
1968     
1969        whd in ⊢ (?→???%→?);
1970        generalize in ⊢ (??%? → ???(????%) → ?); |*: skip]  | #a #lbltrue #next
1971  ] #next change with label in next;
1972| *
1973  [ #lbl
1974  |
1975  | #fl #f #args
1976  ]
1977]
1978whd in match eval_statement in ⊢ (?→%→?); normalize nodelta
1979#EQfetch #EQeval #EQstmt_at #EQnth_opt #next_spec
1980normalize nodelta
1981whd in match (graph_to_lin_statement ???) in ⊢ (%→?);
1982whd in match eval_statement in ⊢ (%→?); normalize nodelta
1983[ >m_return_bind in ⊢ (%→?);
1984  >m_return_bind in EQeval;
1985
1986
1987
1988  (* common for all non-call seq *)
1989  >m_return_bind in ⊢ (%→?);
1990  whd in ⊢ (??%%→?); #EQ destruct(EQ)
1991  >m_return_bind in ⊢ (%→?);
1992
1993 
1994  #ex1
1995lapply (refl … (eval_state ? globals (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) st2))
1996
1997whd in match (point_of_pc ???);
1998whd in match (point_of_succ ???);
1999whd in match sigma_pc in ⊢ (???%); normalize nodelta @opt_safe_elim
2000#pc' #H
2001elim (bind_opt_inversion ????? H) #fn * #EQbl
2002-H #H 
2003elim (bind_opt_inversion ????? H) -H #n * #EQsigma whd in ⊢ (??%?→?);
2004#EQ destruct(EQ)
2005whd in match (succ_pc ????);
2006whd in match (point_of_succ ???);
2007change with (point_of_offset ???) in match (point_of_pc ???);
2008>point_of_offset_of_point
2009whd in match sigma_pc; normalize nodelta @opt_safe_elim
2010#pc' whd in match sigma_pc_opt; normalize nodelta
2011
2012 
2013 
2014        whd in match (succ_pc ????);
2015               
2016        change with next in match (offset_of_point ???) in ⊢ (???%);
2017whd in fetch_statement_spec : (??()%);
2018cases cl in classified_st1_cl; -cl #classified_st1_cl whd
2019[4:
2020 >rel_st1_st2 -st2 letin lin_prog ≝ (linearise ? graph_prog)
2021 cases (good (pi1 ?? fn)) [2: cases daemon (* TODO *) ]
2022 #sigma_entry_is_zero #sigma_spec
2023 lapply (sigma_spec (point_of_pc … (make_sem_graph_params … p') (pc … st1)))
2024 -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @opt_to_opt_safe cases daemon (* TO REDO *) |2: skip ]
2025 -sigma_spec #graph_stmt * #graph_lookup_ok #sigma_spec
2026 cases (opt_Exists_elim … sigma_spec) in ⊢ ?;
2027 * #optlabel #lin_stm * #lin_lookup_ok whd in ⊢ (% → ?); ** #labels_preserved
2028 #related_lin_stm_graph_stm
2029 
2030 inversion (stmt_implicit_label ???)
2031 [ whd in match (opt_All ???); #stmt_implicit_spec #_
2032   letin st2_opt' ≝ (eval_state …
2033               (ev_genv (lin_prog_params … lin_prog lin_stack_sizes))
2034               (sigma_state_pc … wf_st1))
2035   cut (∃st2': lin_abstract_status p p' lin_prog lin_stack_sizes. st2_opt' = return st2')
2036   [cases daemon (* TODO, needs lemma? *)] * #st2' #st2_spec'
2037   normalize nodelta in st2_spec'; -st2_opt'
2038   %{st2'} %{(taaf_step … (taa_base …) …)}
2039   [ cases daemon (* TODO, together with the previous one? *)
2040   | @st2_spec' ]
2041   %[%] [%]
2042   [ whd whd in match eval_state in st2_spec'; normalize nodelta in st2_spec';
2043     >(fetch_statement_sigma_commute … good … fetch_statement_spec) in st2_spec';
2044     >m_return_bind
2045     (* Case analysis over the possible statements *)
2046     inversion graph_stmt in stmt_implicit_spec; normalize nodelta
2047     [ #stmt #lbl #_ #abs @⊥ normalize in abs; destruct(abs) ]
2048     XXXXXXXXXX siamo qua, caso GOTO e RETURN
2049   | cases daemon (* TODO, after the definition of label_rel, trivial *) ]
2050   ]
2051 | ....
2052qed.
2053
2054
2055
2056
2057
2058[ *
2059  [ *
2060    [ letin C_COMMENT ≝ 0 in ⊢ ?; #c
2061    | letin C_COST_LABEL ≝ 0 in ⊢ ?; #lbl
2062    | letin C_MOVE       ≝ 0 in ⊢ ?; #move_sig
2063    | letin C_POP        ≝ 0 in ⊢ ?; #a
2064    | letin C_PUSH       ≝ 0 in ⊢ ?; #a
2065    | letin C_ADDRESS    ≝ 0 in ⊢ ?; #sy #sy_prf #dpl #dph
2066    | letin C_OPACCS     ≝ 0 in ⊢ ?; #op #a #b #arg1 #arg2
2067    | letin C_OP1        ≝ 0 in ⊢ ?; #op #a #arg
2068    | letin C_OP2        ≝ 0 in ⊢ ?; #op #a #arg1 #arg2
2069    | letin C_CLEAR_CARRY ≝ 0 in ⊢ ?;
2070    | letin C_SET_CARRY  ≝ 0 in ⊢ ?;
2071    | letin C_LOAD       ≝ 0 in ⊢ ?; #a #dpl #dph
2072    | letin C_STORE      ≝ 0 in ⊢ ?; #dpl #dph #a
2073    | letin C_CALL       ≝ 0 in ⊢ ?; #f #args #dest
2074    | letin C_EXT        ≝ 0 in ⊢ ?; #s_ext
2075    ]
2076  | letin C_COND ≝ 0 in ⊢ ?; #a #lbltrue
2077  ] #next change with label in next;
2078| *
2079  [ letin C_GOTO ≝ 0 in ⊢ ?; #lbl
2080  | letin C_RETURN ≝ 0 in ⊢ ?;
2081  | letin C_TAILCALL ≝ 0 in ⊢ ?; #fl #f #args
2082  ]
2083]
Note: See TracBrowser for help on using the repository browser.