source: src/joint/lineariseProof.ma @ 3371

Last change on this file since 3371 was 3371, checked in by piccolo, 6 years ago

Modified RTLsemantics and ERTLsemantics. Now the pop frame will set
to undef the carry bit and all RegisterCallerSaved? exept those used to
pass the return value of a function.

Added an overflow check in ERTL_semantics

File size: 99.8 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".
19include "common/ExtraMonads.ma".
20
21check mk_sem_graph_params
22
23definition graph_prog_params ≝
24λp,p',pre_main,prog,stack_sizes.
25mk_prog_params (mk_sem_graph_params p p' pre_main) prog stack_sizes.
26
27check mk_sem_graph_params
28
29definition graph_abstract_status:
30 ∀p:uns_params.
31  (∀F.sem_unserialized_params p F) →
32   (∀prog : joint_program (mk_graph_params p).
33    joint_closed_internal_function (mk_graph_params p) (prog_names … prog)) →
34    ∀prog : joint_program (mk_graph_params p).
35  (ident → option ℕ) →
36     abstract_status
37 ≝
38 λp,p',pre_main,prog,stack_sizes.
39 joint_abstract_status (graph_prog_params ? p' pre_main prog stack_sizes).
40
41definition lin_prog_params ≝
42λp,p',pre_main,prog,stack_sizes.
43mk_prog_params (mk_sem_lin_params p p' pre_main) prog stack_sizes.
44
45definition lin_abstract_status:
46 ∀p:uns_params.
47  (∀F.sem_unserialized_params p F) →
48  (∀prog : joint_program (mk_lin_params p).
49    joint_closed_internal_function (mk_lin_params p) (prog_names … prog)) →
50    ∀prog : joint_program (mk_lin_params p).
51  (ident → option ℕ) →
52     abstract_status
53 ≝
54 λp,p',pre_main,prog,stack_sizes.
55 joint_abstract_status (lin_prog_params ? p' pre_main prog stack_sizes).
56
57(*
58axiom P :
59  ∀A,B,prog.A (prog_var_names (λvars.fundef (A vars)) B prog) → Prop.
60
61check (λpars.let pars' ≝ make_global pars in λx :joint_closed_internal_function pars' (globals pars'). P … x)
62(*
63unification hint 0 ≔ p, prog, stack_sizes ;
64pars ≟ mk_prog_params p prog stack_sizes ,
65pars' ≟ make_global pars,
66A ≟ λvars.joint_closed_internal_function p vars,
67B ≟ ℕ
68
69A (prog_var_names (λvars.fundef (A vars)) B prog) ≡
70joint_closed_internal_function pars' (globals pars').
71*)
72axiom T : ∀A,B,prog.genv_t (fundef (A (prog_var_names (λvars:list ident.fundef (A vars)) B prog))) → Prop.
73(*axiom Q : ∀A,B,init,prog.
74 T … (globalenv (λvars:list ident.fundef (A vars)) B
75  init prog) → Prop.
76
77lemma pippo :
78  ∀p,p',prog,stack_sizes.
79  let pars ≝ graph_prog_params p p' prog stack_sizes in
80  let ge ≝ ev_genv pars in T ?? prog ge → Prop.
81 
82  #H1 #H2 #H3 #H4
83   #H5
84  whd in match (ev_genv ?) in H5;               
85  whd in match (globalenv_noinit) in H5; normalize nodelta in H5;
86  whd in match (prog ?) in H5;
87  whd in match (joint_function ?) in H5;
88  @(Q … H5)
89 λx:T ??? ge.Q ???? x)
90*)
91axiom Q : ∀A,B,init,prog,i.
92is_internal_function
93 (A
94  (prog_var_names (λvars:list ident.fundef (A vars)) B
95   prog))
96 (globalenv (λvars:list ident.fundef (A vars)) B
97  init prog)
98 i → Prop.
99
100check
101  (λp,p',prog,stack_sizes,i.
102  let pars ≝ graph_prog_params p p' prog stack_sizes in
103  let ge ≝ ev_genv pars in
104 λx:is_internal_function (joint_closed_internal_function pars (globals pars))
105  ge i.Q ??? prog ? x)
106*)
107
108definition sigma_map ≝ λp.λgraph_prog : joint_program (mk_graph_params p).
109  joint_closed_internal_function (mk_graph_params p) (prog_var_names … graph_prog) →
110    label → option ℕ.
111
112definition sigma_pc_opt:
113 ∀p,p'.∀graph_prog.
114  sigma_map p graph_prog →
115   program_counter → option program_counter
116 ≝
117  λp,p',prog,sigma,pc.
118  let pars ≝ mk_sem_graph_params p p' in
119  let ge ≝ globalenv_noinit … prog in
120  if eqZb       (block_id (pc_block pc)) (-1) then (* check for dummy exit pc *)
121    return pc
122  else
123    ! 〈i, fd〉 ← res_to_opt … (fetch_internal_function … ge (pc_block pc)) ;
124    ! lin_point ← sigma fd (point_of_pc pars pc) ;
125    return pc_of_point
126    (mk_sem_lin_params ? p') (pc_block pc) lin_point.
127
128definition well_formed_pc:
129 ∀p,p',graph_prog.
130  sigma_map p graph_prog →
131   program_counter → Prop
132 ≝
133 λp,p',prog,sigma,pc.
134  sigma_pc_opt p p' prog sigma pc
135   ≠ None ….
136
137definition sigma_beval_opt :
138 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
139  sigma_map p graph_prog →
140  beval → option beval ≝
141λp,p',graph_prog,sigma,bv.
142match bv with
143[ BVpc pc prt ⇒ ! pc' ← sigma_pc_opt p p' graph_prog sigma pc ; return BVpc pc' prt
144| _ ⇒ return bv
145].
146
147definition sigma_beval :
148 ∀p,p',graph_prog,sigma,bv.
149 sigma_beval_opt p p' graph_prog sigma bv ≠ None ? → beval ≝
150 λp,p',graph_prog,sigma,bv.opt_safe ….
151
152definition sigma_is_opt :
153 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
154  sigma_map p graph_prog →
155  internal_stack → option internal_stack ≝
156λp,p',graph_prog,sigma,is.
157match is with
158[ empty_is ⇒ return empty_is
159| one_is bv ⇒ ! bv' ← sigma_beval_opt p p' … sigma bv ; return one_is bv'
160| both_is bv1 bv2 ⇒
161  ! bv1' ← sigma_beval_opt p p' … sigma bv1 ;
162  ! bv2' ← sigma_beval_opt p p' … sigma bv2 ;
163  return both_is bv1' bv2'
164].
165
166definition sigma_is :
167 ∀p,p',graph_prog,sigma,is.
168 sigma_is_opt p p' graph_prog sigma is ≠ None ? → internal_stack ≝
169 λp,p',graph_prog,sigma,is.opt_safe ….
170 
171lemma sigma_is_empty : ∀p,p',graph_prog,sigma.
172  ∀prf.sigma_is p p' graph_prog sigma empty_is prf = empty_is.
173#p #p' #graph_prog #sigma #prf whd in match sigma_is; normalize nodelta
174@opt_safe_elim #is' whd in ⊢ (??%%→?); #EQ destruct(EQ) % qed.
175
176(* spostato in ExtraMonads.ma
177
178lemma res_preserve_error : ∀X,Y,P,F,e,n.res_preserve X Y P F (Error … e) n.
179#X #Y #P #F #e #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed.
180
181lemma mfr_return_eq : ∀M1,M2.∀FR : MonadFunctRel M1 M2.
182∀X,Y,P,F,v,n.
183∀prf.n = return F v prf →
184FR X Y P F (return v) n.
185#M1 #M2 #FR #X #Y #P #F #v #n #prf #EQ >EQ @mfr_return qed.
186
187lemma opt_safe_eq : ∀A,m,x,prf.m = Some A x → opt_safe A m prf = x.
188#A #m #x #prf @opt_safe_elim #x' #EQ >EQ #EQ' destruct % qed.
189*)
190
191lemma sigma_is_pop_commute :
192 ∀p,p',graph_prog,sigma,is.
193 ∀prf : sigma_is_opt p p' graph_prog sigma is ≠ None ?.
194 res_preserve …
195  (λpr.sigma_beval_opt p p' graph_prog sigma (\fst pr) ≠ None ? ∧
196       sigma_is_opt p p' graph_prog sigma (\snd pr) ≠ None ?)
197  (λpr,prf.〈sigma_beval … (proj1 … prf), sigma_is … (proj2 … prf)〉)
198  (is_pop is) (is_pop (sigma_is … prf)).
199#p #p' #graph_prog #sigma * [|#bv1|#bv1 #bv2] #prf
200[ @res_preserve_error
201|*:
202 whd in match sigma_is in ⊢ (?????????%); normalize nodelta
203 @opt_safe_elim #is'
204  #H @('bind_inversion H) -H #bv1' #EQ1
205  [2: #H @('bind_inversion H) -H #bv2' #EQ2 ]
206 whd in ⊢ (??%%→?); #EQ destruct(EQ)
207 @mfr_return_eq
208 [1,3: @hide_prf %%
209 |*: whd in match sigma_beval; whd in match sigma_is;
210  normalize nodelta @opt_safe_elim #bv1'' @opt_safe_elim #is''
211 ]
212 [2,4,5,6: whd in match sigma_is_opt; normalize nodelta [1,3: >EQ1 ]
213  whd in ⊢ (??%%→?); #EQ destruct(EQ) ]
214 [1,3: >EQ2 |*: >EQ1 ] #EQ' destruct(EQ') %
215]
216qed.
217
218(* lemma opt_to_res_preserve : ∀X,Y.∀P : X → Y → Prop.∀e,u,v.
219  opt_preserve P u v → res_preserve P (opt_to_res … e u) (opt_to_res … e v).
220#X #Y #P #e #u #v #H #x #EQ lapply (opt_eq_from_res ???? EQ) -EQ #EQ
221lapply (H … EQ) cases v [ * ] #y #K @K qed.
222
223lemma err_eq_from_io : ∀O,I,X,m,v.
224  err_to_io O I X m = return v → m = return v.
225#O #I #X * #x #v normalize #EQ destruct % qed.
226
227lemma res_to_io_preserve : ∀X,Y.∀P : X → Y → Prop.∀O,I,u,v.
228  res_preserve P u v → IO_preserve O I P u v.
229#X #Y #P #O #I #u #v #H #x #EQ lapply (err_eq_from_io ????? EQ) -EQ #EQ
230lapply (H … EQ) cases v [2: #e * ] #y #K @K qed.
231
232lemma preserve_opt_to_res : ∀X,Y.∀P : X → Y → Prop.∀e,u,v.
233  res_preserve P (opt_to_res … e u) (opt_to_res … e v) → opt_preserve P u v.
234#X #Y #P #e #u #v #H #x #EQ
235lapply (H x) >EQ -H #H lapply (H (refl …)) cases v [ * ]
236#y #K @K qed.
237
238lemma preserve_res_to_io : ∀X,Y.∀P : X → Y → Prop.∀O,I,u,v.
239  IO_preserve O I P (err_to_io … u) (err_to_io … v) → res_preserve P u v.
240#X #Y #P #O #I #u #v #H #x #EQ
241lapply (H x) >EQ -H #H lapply (H (refl …)) cases v [2: #e * ]
242#y #K @K qed. *)
243
244definition well_formed_mem :
245 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
246  sigma_map p graph_prog →
247 bemem → Prop ≝
248λp,p',graph_prog,sigma,m.
249∀b,z.block_id b < nextblock m → low_bound m b ≤ z → z < high_bound m b →
250  sigma_beval_opt p p' graph_prog sigma (contents (blocks m b) z) ≠ None ?.
251
252definition sigma_mem :
253 ∀p,p',graph_prog,sigma,m.
254 well_formed_mem p p' graph_prog sigma m →
255 bemem ≝
256 λp,p',graph_prog,sigma,m,prf.
257 mk_mem
258  (λb.
259    If Zltb (block_id b) (nextblock m) then with prf' do   
260      let l ≝ low_bound m b in
261      let h ≝ high_bound m b in
262      mk_block_contents l h
263      (λz.If Zleb l z ∧ Zltb z h then with prf'' do
264        sigma_beval p p' graph_prog sigma (contents (blocks m b) z) ?
265      else BVundef)
266    else empty_block OZ OZ)
267  (nextblock m)
268  (nextblock_pos m).
269@hide_prf
270lapply prf'' lapply prf' -prf' -prf''
271@Zltb_elim_Type0 [2: #_ * ]
272#bid_ok *
273@Zleb_elim_Type0 [2: #_ * ]
274@Zltb_elim_Type0 [2: #_ #_ * ]
275#zh #zl * @(prf … bid_ok zl zh)
276qed.
277
278lemma andb_false : ∀b1,b2.andb b1 b2 = false → b1 = false ∨ b2 = false.
279** /2 by or_introl, or_intror/ normalize #ABS destruct(ABS) qed.
280
281axiom mem_ext_eq :
282  ∀m1,m2 : mem.
283  (∀b.let bc1 ≝ blocks m1 b in
284      let bc2 ≝ blocks m2 b in
285      low bc1 = low bc2 ∧ high bc1 = high bc2 ∧
286      ∀z.contents bc1 z = contents bc2 z) →
287  nextblock m1 = nextblock m2 → m1 = m2.
288(* spostato in ExtraMonads.ma
289
290lemma opt_preserve_none : ∀X,Y,P,F,n.opt_preserve X Y P F (None ?) n.
291#X #Y #P #F #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed.
292*)
293
294lemma beloadv_sigma_commute:
295∀p,p',graph_prog,sigma,ptr.
296preserving … opt_preserve …
297 (sigma_mem p p' graph_prog sigma)
298 (sigma_beval p p' graph_prog sigma)
299 (λm.beloadv m ptr)
300 (λm.beloadv m ptr).
301#p #p' #graph_prog  #sigma #ptr #m #prf #bv
302whd in match beloadv;
303whd in match do_if_in_bounds;
304whd in match sigma_mem;
305normalize nodelta
306@If_elim #block_ok >block_ok normalize nodelta
307[2: whd in ⊢ (???%→?); #ABS destruct(ABS) ]
308@If_elim #H
309[ elim (andb_true … H)
310  #H1 #H2
311  whd in match sigma_beval; normalize nodelta
312  @opt_safe_elim #bv' #EQ_bv' >H1 >H2 normalize nodelta
313  whd in ⊢ (???%→?); #EQ' destruct
314  >EQ_bv' % [ % #ABS destruct(ABS) ] @opt_to_opt_safe
315| elim (andb_false … H) -H #H >H
316  [2: >commutative_andb ] normalize nodelta
317  whd in ⊢ (???%→?); #ABS destruct(ABS)
318]
319qed.
320
321include alias "common/GenMem.ma".
322
323lemma bestorev_sigma_commute :
324∀p,p',graph_prog,sigma,ptr.
325preserving2 ?? opt_preserve …
326  (sigma_mem p p' graph_prog sigma)
327  (sigma_beval p p' graph_prog sigma)
328  (sigma_mem p p' graph_prog sigma)
329  (λm.bestorev m ptr)
330  (λm.bestorev m ptr).
331#p #p' #graph_prog #sigma #ptr #m #bv #prf1 #prf2 #m'
332whd in match bestorev;
333whd in match do_if_in_bounds;
334whd in match sigma_mem;
335whd in match update_block;
336 normalize nodelta
337@If_elim #block_ok >block_ok normalize nodelta
338[2: whd in ⊢ ((???%) → ?); #ABS destruct(ABS)]
339@Zleb_elim_Type0 #H1
340[ @Zltb_elim_Type0 #H2 ]
341[2,3: #ABS normalize in ABS; destruct(ABS) ]
342normalize nodelta whd in ⊢ (???%→?); #EQ destruct(EQ)
343%
344[2: whd in ⊢ (???%);
345  @eq_f
346  @mem_ext_eq [2: % ]
347  #b @if_elim
348  [2: #B
349    @If_elim #prf1 @If_elim #prf2
350    [2,3: @⊥ >prf1 in prf2; * /2 by I/ ] [2: % [%%] #z % ]
351    whd in match low_bound; whd in match high_bound;
352    normalize nodelta
353    cut (Not (bool_to_Prop (eq_block b (pblock ptr))))
354    [ % #ABS >ABS in B; * ]
355    -B #B % [ >B %% ] #z
356    @If_elim #prf3 
357    @If_elim #prf4
358    [2,3: @⊥ >B in prf4; normalize nodelta >prf3 * /2 by I/ |4: % ]
359    whd in match sigma_beval in ⊢ (??%%); normalize nodelta
360    @opt_safe_elim @opt_safe_elim #bv1 #EQ1 #bv2 #EQ2 >B in EQ1;
361    >EQ2 #EQ destruct(EQ) %
362  | #B cut (b = pblock ptr) [ lapply B @eq_block_elim // #_ * ]
363    #EQ destruct(EQ)
364    @If_elim whd in match low_bound; whd in match high_bound;
365    normalize nodelta
366    [2: >block_ok * #ABS elim (ABS I) ]
367    #prf3 % [ >B %% ]
368    #z whd in match update; normalize nodelta
369    @eqZb_elim normalize nodelta #prf4
370    [2: @If_elim #prf5 @If_elim #prf6
371      [2,3: @⊥ >B in prf6; >prf5 * /2 by I/ |4: % ]
372      whd in match sigma_beval in ⊢ (??%%); normalize nodelta
373      @opt_safe_elim @opt_safe_elim #bv1 #EQ1 #bv2 #EQ2 >B in EQ1;
374      normalize nodelta >(eqZb_false … prf4) >EQ2
375      #EQ destruct(EQ) %
376    | @If_elim #prf5
377      [2: >B in prf5; normalize nodelta
378        >prf4 >(Zle_to_Zleb_true … H1) >(Zlt_to_Zltb_true … H2) * #ABS elim (ABS I) ]
379      whd in match sigma_beval in ⊢ (??%%); normalize nodelta
380      @opt_safe_elim @opt_safe_elim #bv1 #EQ1 #bv2 #EQ2 >B in EQ1;
381      normalize nodelta >prf4 >eqZb_z_z >EQ2 #EQ destruct(EQ) %
382    ]
383  ]
384| whd #b #z #h1 whd in match low_bound; whd in match high_bound; normalize nodelta
385  @eq_block_elim #H normalize nodelta destruct
386  #h2 #h3 whd in match update; normalize nodelta
387  [ @eqZb_elim #H destruct normalize nodelta [ assumption ]]
388  @prf1 assumption
389]
390qed.
391
392record good_sem_state_sigma
393  (p : unserialized_params)
394  (p' : ∀F.sem_unserialized_params p F) (graph_prog : ?)
395  (sigma : sigma_map p graph_prog) : Type[0] ≝
396{ well_formed_frames : framesT (mk_sem_graph_params p p') → Prop
397; sigma_frames : ∀frms.well_formed_frames frms → framesT (mk_sem_lin_params p p')
398; sigma_empty_frames_commute :
399  ∃prf.
400  empty_framesT (mk_sem_lin_params p p') =
401  sigma_frames (empty_framesT (mk_sem_graph_params p p')) prf
402
403; well_formed_regs : regsT (mk_sem_graph_params p p') → Prop
404; sigma_regs : ∀regs.well_formed_regs regs → regsT (mk_sem_lin_params p p')
405; sigma_empty_regsT_commute :
406  ∀ptr.∃ prf.
407  empty_regsT (mk_sem_lin_params p p') ptr =
408  sigma_regs (empty_regsT (mk_sem_graph_params p p') ptr) prf
409; sigma_load_sp_commute :
410  preserving … res_preserve …
411    (λ_.True)
412    …
413    sigma_regs
414    (λx.λ_.x)
415    (load_sp (mk_sem_graph_params p p'))
416    (load_sp (mk_sem_lin_params p p'))
417; sigma_save_sp_commute :
418  ∀reg,ptr,prf1. ∃prf2.
419  save_sp (mk_sem_lin_params p p') (sigma_regs reg prf1) ptr =
420  sigma_regs (save_sp (mk_sem_graph_params p p') reg ptr) prf2
421}.
422
423definition well_formed_state :
424 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
425 ∀sigma.
426 good_sem_state_sigma p p' graph_prog sigma →
427 state (mk_sem_graph_params p p') → Prop ≝
428λp,p',graph_prog,sigma,gsss,st.
429well_formed_frames … gsss (st_frms … st) ∧
430sigma_is_opt p p' graph_prog sigma (istack … st) ≠ None ? ∧
431well_formed_regs … gsss (regs … st) ∧
432well_formed_mem p p' graph_prog sigma (m … st).
433
434definition sigma_state :
435 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
436 ∀sigma.
437 ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
438 ∀st : state (mk_sem_graph_params p p').
439 well_formed_state … gsss st →
440 state (mk_sem_lin_params p p') ≝
441λp,p',graph_prog,sigma,gsss,st,prf.
442mk_state …
443  (sigma_frames p p' graph_prog sigma gsss (st_frms … st) ?)
444  (sigma_is p p' graph_prog sigma (istack … st) ?)
445  (carry … st)
446  (sigma_regs … gsss (regs … st) ?)
447  (sigma_mem p p' graph_prog sigma (m … st) ?).
448@hide_prf cases prf ** //
449qed.
450
451
452(*
453lemma sigma_is_pop_wf :
454 ∀p,p',graph_prog,sigma,is,bv,is'.
455 is_pop is = return 〈bv, is'〉 →
456 sigma_is_opt p p' graph_prog sigma is ≠ None ? →
457 sigma_beval_opt p p' graph_prog sigma bv ≠ None ? ∧
458 sigma_is_opt p p' graph_prog sigma is' ≠ None ?.
459cases daemon qed.
460*)
461
462(*
463lemma prova : ∀p,s,st,prf.sigma_pc_of_status p s st prf = ?.
464[ #p #s #st #prf
465  whd in match sigma_pc_of_status; normalize nodelta
466  @opt_safe_elim
467  #n
468  lapply (refl …  (int_funct_of_block (joint_closed_internal_function p) (globals p)
469        (ev_genv p) (pblock (pc p st))))
470  elim (int_funct_of_block (joint_closed_internal_function p) (globals p)
471        (ev_genv p) (pblock (pc p st))) in ⊢ (???%→%);
472  [ #_ #ABS normalize in ABS; destruct(ABS) ]
473  #f #EQ >m_return_bind
474*)
475
476
477(*
478lemma wf_status_to_wf_pc :
479∀p,p',graph_prog,stack_sizes.
480∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) →
481    code_point (mk_graph_params p) → option ℕ).
482∀st.
483well_formed_status p p' graph_prog stack_sizes sigma st →
484well_formed_pc p p' graph_prog stack_sizes sigma (pc ? st).
485#p #p' #graph_prog #stack_sizes #sigma #st whd in ⊢ (% → ?); * #H #_ @H
486qed.
487 *)
488definition sigma_pc :
489∀p,p',graph_prog.
490∀sigma.
491∀pc.
492∀prf : well_formed_pc p p' graph_prog sigma pc.
493program_counter ≝
494λp,p',graph_prog,sigma,st.opt_safe ….
495 
496lemma sigma_pc_ok:
497  ∀p,p',graph_prog.
498  ∀sigma.
499   ∀pc.
500    ∀prf:well_formed_pc p p' graph_prog sigma pc.
501    sigma_pc_opt p p' graph_prog sigma pc =
502    Some … (sigma_pc p p' graph_prog sigma pc prf).
503    #p #p' #graph_prog #sigma #st #prf @opt_to_opt_safe qed.
504
505lemma sigma_pc_irr :
506  ∀p,p',graph_prog,sigma,pc1,pc2,prf1,prf2.
507  pc1 = pc2 →
508  sigma_pc p p' graph_prog sigma pc1 prf1 =
509  sigma_pc p p' graph_prog sigma pc2 prf2.
510#p #p' #graph_prog #sigma #pc1 #pc2 #prf1 #prf2
511#EQ destruct(EQ) % qed.
512
513definition well_formed_state_pc :
514 ∀p,p',graph_prog,sigma.
515  good_sem_state_sigma p p' graph_prog sigma →
516  state_pc (mk_sem_graph_params p p') → Prop ≝
517 λp,p',prog,sigma,gsss,st.
518 well_formed_pc p p' prog sigma (last_pop … st) ∧
519 well_formed_pc p p' prog sigma (pc … st) ∧
520 well_formed_state … gsss st.
521 
522definition sigma_state_pc :
523 ∀p.
524 ∀p':∀F.sem_unserialized_params p F.
525 ∀graph_prog.
526  ∀sigma.
527(*   let lin_prog ≝ linearise ? graph_prog in *)
528  ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
529    ∀s:state_pc (mk_sem_graph_params p p'). (* = graph_abstract_status p p' graph_prog stack_sizes *)
530     well_formed_state_pc p p' graph_prog sigma gsss s →
531      state_pc (mk_sem_lin_params p p') (* = lin_abstract_status p p' lin_prog ? *)
532
533 λp,p',graph_prog,sigma,gsss,s,prf.
534 let last_pop' ≝ sigma_pc … (proj1 … (proj1 … prf)) in
535 let pc' ≝ sigma_pc … (proj2 … (proj1 … prf)) in
536 let st' ≝ sigma_state … (proj2 … prf) in
537 mk_state_pc ? st' pc' last_pop'.
538(*
539definition sigma_function_name :
540 ∀p,graph_prog.
541 let lin_prog ≝ linearise p graph_prog in
542  (Σf.is_internal_function_of_program … graph_prog f) →
543  (Σf.is_internal_function_of_program … lin_prog f) ≝
544λp,graph_prog,f.«f, if_propagate … (pi2 … f)».
545*)
546
547(* spostato in ExtraMonads.ma
548
549lemma m_list_map_All_ok :
550  ∀M : MonadProps.∀X,Y,f,l.
551  All X (λx.∃y.f x = return y) l → ∃l'.m_list_map M X Y f l = return l'.
552  #M #X #Y #f #l elim l -l
553  [ * %{[ ]} %
554  | #hd #tl #IH * * #y #EQ #H cases (IH H) #ys #EQ'
555    %{(y :: ys)}
556    change with (! y ← ? ;  ? = ?)
557    >EQ >m_return_bind
558    change with (! acc ← m_list_map ????? ; ? = ?) >EQ'
559    @m_return_bind
560qed.
561*)
562
563definition helper_def_store__commute :
564  ∀p,p',graph_prog,sigma.
565  ∀X : ? → Type[0].
566  ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
567  ∀store : ∀p,F.∀p' : sem_unserialized_params p F.
568    X p → beval → regsT p' →
569    res (regsT p').
570  Prop ≝
571  λp,p',graph_prog,sigma,X,gsss,store.
572  ∀a : X p.preserving2 … res_preserve …
573    (sigma_beval p p' graph_prog sigma)
574    (sigma_regs … gsss)
575    (sigma_regs … gsss)
576    (store … a)
577    (store … a).
578 
579definition helper_def_retrieve__commute :
580  ∀p,p',graph_prog,sigma.
581  ∀X : ? → Type[0].
582  ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
583  ∀retrieve : ∀p,F.∀p' : sem_unserialized_params p F.
584    regsT p' → X p → res beval.
585  Prop ≝
586  λp,p',graph_prog,sigma,X,gsss,retrieve.
587  ∀a : X p.
588  preserving … res_preserve …
589    (sigma_regs … gsss)
590    (sigma_beval p p' graph_prog sigma)
591    (λr.retrieve … r a)
592    (λr.retrieve … r a).
593
594record good_state_sigma
595  (p : unserialized_params)
596  (p' : ∀F.sem_unserialized_params p F) (graph_prog : ?)
597  (sigma : sigma_map p graph_prog)
598: Type[0] ≝
599{ gsss :> good_sem_state_sigma p p' graph_prog sigma
600
601; acca_store__commute : helper_def_store__commute … gsss acca_store_
602; acca_retrieve_commute : helper_def_retrieve__commute … gsss acca_retrieve_
603; acca_arg_retrieve_commute : helper_def_retrieve__commute … gsss acca_arg_retrieve_
604; accb_store_commute : helper_def_store__commute … gsss accb_store_
605; accb_retrieve_commute : helper_def_retrieve__commute … gsss accb_retrieve_
606; accb_arg_retrieve_commute : helper_def_retrieve__commute … gsss accb_arg_retrieve_
607; dpl_store_commute : helper_def_store__commute … gsss dpl_store_
608; dpl_retrieve_commute : helper_def_retrieve__commute … gsss dpl_retrieve_
609; dpl_arg_retrieve_commute : helper_def_retrieve__commute … gsss dpl_arg_retrieve_
610; dph_store_commute : helper_def_store__commute … gsss dph_store_
611; dph_retrieve_commute : helper_def_retrieve__commute … gsss dph_retrieve_
612; dph_arg_retrieve_commute : helper_def_retrieve__commute … gsss dph_arg_retrieve_
613; snd_arg_retrieve_commute : helper_def_retrieve__commute … gsss snd_arg_retrieve_
614; pair_reg_move_commute : ∀mv.
615  preserving … res_preserve … (sigma_regs … gsss) (sigma_regs … gsss)
616    (λr.pair_reg_move_ ? ? (p' ?) r mv)
617    (λr.pair_reg_move_ ? ? (p' ?) r mv)
618; save_frame_commute :
619  ∀dest,fl.
620  preserving … res_preserve …
621    (sigma_state_pc … gsss)
622    (sigma_state … gsss)
623    (save_frame ?? (p' ?) fl dest)
624    (save_frame ?? (p' ?) fl dest)
625; eval_ext_seq_commute :
626  let lin_prog ≝ linearise p graph_prog in
627  ∀ stack_sizes.
628  ∀ext,i,fn.
629  preserving … res_preserve …
630    (sigma_state … gsss)
631    (sigma_state … gsss)
632    (eval_ext_seq ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes))
633      ext i fn)
634    (eval_ext_seq ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
635      ext i (\fst (linearise_int_fun … fn)))
636; setup_call_commute :
637  ∀ n , parsT, call_args.
638  preserving … res_preserve …
639    (sigma_state … gsss)
640    (sigma_state … gsss)
641    (setup_call ?? (p' ?) n parsT call_args)
642    (setup_call ?? (p' ?) n parsT call_args)
643; fetch_external_args_commute : (* TO BE CHECKED *)
644  ∀ex_fun,st1,prf1,call_args.
645  fetch_external_args ?? (p' ?) ex_fun st1 call_args =
646  fetch_external_args ?? (p' ?) ex_fun (sigma_state p p' graph_prog sigma gsss st1 prf1) call_args
647; set_result_commute :
648  ∀ l , call_dest.
649  preserving … res_preserve …
650    (sigma_state … gsss)
651    (sigma_state … gsss)
652    (set_result ?? (p' ?) l call_dest)
653    (set_result ?? (p' ?) l call_dest) 
654; read_result_commute :
655  let lin_prog ≝ linearise p graph_prog in
656  ∀stack_sizes.
657  ∀call_dest.
658  preserving … res_preserve …
659    (sigma_state … gsss)
660    (λl,prf.opt_safe ? (m_list_map … (sigma_beval_opt p p' graph_prog sigma) l) prf)
661    (read_result ?? (p' ?) ? (ev_genv (graph_prog_params … graph_prog stack_sizes))
662     call_dest)
663    (read_result ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
664     call_dest)
665; pop_frame_commute :
666  let lin_prog ≝ linearise p graph_prog in
667  ∀stack_sizes, curr_id , curr_fn.
668  preserving … res_preserve …
669    (sigma_state … gsss)
670    (sigma_state_pc … gsss)
671  (pop_frame ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes))
672            curr_id curr_fn)
673  (pop_frame ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
674            curr_id (\fst (linearise_int_fun … curr_fn)))
675}.
676
677lemma wf_set_regs : ∀p,p',graph_prog,sigma,gss,st,r.
678well_formed_state p p' graph_prog sigma gss st →
679well_formed_regs … gss r →
680well_formed_state … gss (set_regs … r st).
681#p #p' #graph_prog #sigma #gss #st #r
682*** #H1 #H2 #_ #H4 #H3
683%{H4} %{H3} %{H2} @H1
684qed.
685
686lemma allocate_locals_def :
687  ∀p,F,p',loc,locs,st.
688  allocate_locals p F p' (loc::locs) st =
689  (let st' ≝ allocate_locals p F p' locs st in
690   set_regs … (allocate_locals_ p F p' loc (regs … st')) st').
691#p #F #p' #loc #locs #st % qed.
692
693lemma allocate_locals_commute :
694  ∀p,p',graph_prog,sigma.
695  ∀gss : good_state_sigma p p' graph_prog sigma.
696  ∀locs, st1, prf1. ∃ prf2.
697  allocate_locals ? ? (p' ?) locs (sigma_state … gss st1 prf1) =
698  sigma_state … gss (allocate_locals ? ? (p' ?) locs st1) prf2.
699#p #p' #gp #sigma #gss #locs elim locs -locs
700[ #st1 #prf1 %{prf1} % ]
701#loc #tl #IH #st1 #prf1
702letin st2 ≝ (sigma_state … st1 prf1)
703cases (IH st1 prf1)
704letin st1' ≝ (allocate_locals ??? tl st1)
705letin st2' ≝ (allocate_locals ??? tl st2)
706#prf' #EQ'
707cases (allocate_locals__commute … gss loc (regs … st1') ?)
708[2: @hide_prf cases prf' ** // ]
709#prf'' #EQ''
710% [ @hide_prf @wf_set_regs assumption ]
711change with (set_regs ? (allocate_locals_ ??? loc (regs ? st1')) st1')
712  in match (allocate_locals ??? (loc::tl) st1);
713change with (set_regs ? (allocate_locals_ ??? loc (regs ? st2')) st2')
714  in match (allocate_locals ??? (loc::tl) st2);
715>EQ' >EQ'' %
716qed.
717
718lemma store_commute :
719  ∀p,p',graph_prog,sigma.
720  ∀X : ? → Type[0].
721  ∀store.
722  ∀gsss : good_state_sigma p p' graph_prog sigma.
723  ∀H : helper_def_store__commute … gsss store.
724  ∀a : X p.
725  preserving2 … res_preserve …
726    (sigma_beval p p' graph_prog sigma)
727    (sigma_state … gsss)
728    (sigma_state … gsss)
729    (helper_def_store ? store … a)
730    (helper_def_store ? store … a).
731#p #p' #graph_prog #sigma #X #store #gsss #H #a
732#bv #st #prf1 #prf2
733@(mfr_bind … (sigma_regs … gsss)) [@H]
734#r #prf3 @mfr_return cases st in prf2;
735#frms #is #carry #r' #m *** #H1 #H2 #H3 #H4 %{H4} % [%{H1 H2}] assumption
736qed.
737
738lemma retrieve_commute :
739 ∀p,p',graph_prog,sigma.
740 ∀X : ? → Type[0].
741 ∀retrieve.
742 ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
743 ∀H : helper_def_retrieve__commute … gsss retrieve.
744 ∀a : X p .
745 preserving … res_preserve …
746    (sigma_state … gsss)
747    (sigma_beval p p' graph_prog sigma)
748    (λst.helper_def_retrieve ? retrieve … st a)
749    (λst.helper_def_retrieve ? retrieve … st a).
750#p #p' #graph_prog #sigma #X #retrieve #gsss #H #a #st #prf @H qed.
751
752(*
753definition acca_store_commute :
754  ∀p,p',graph_prog,sigma.
755  ∀gss : good_state_sigma p p' graph_prog sigma.
756  ∀a : acc_a_reg p.∀bv,st,st',prf1,prf1'.
757  acca_store … a bv st = return st' →
758  ∃prf2.
759  acca_store … a
760    (sigma_beval p p' graph_prog sigma bv prf1')
761    (sigma_state … gss st prf1) = return sigma_state … gss st' prf2
762 ≝
763λp,p',graph_prog,sigma.
764λgss : good_state_sigma p p' graph_prog sigma.
765store_commute … gss (acca_store__commute … gss).
766
767*)
768
769(* restano:
770; setup_call : nat → paramsT … uns_pars → call_args uns_pars →
771    state st_pars → res (state st_pars)
772; fetch_external_args: external_function → state st_pars → call_args … uns_pars →
773    res (list val)
774; set_result: list val → call_dest uns_pars → state st_pars → res (state st_pars)
775
776(* from now on, parameters that use the type of functions *)
777; read_result: ∀globals.genv_gen F globals → call_dest uns_pars → state st_pars → res (list beval)
778(* change of pc must be left to *_flow execution *)
779; pop_frame: ∀globals.∀ge : genv_gen F globals.
780  (Σi.is_internal_function … ge i) (* current *) → state st_pars → res (state st_pars)
781*)
782
783(*
784lemma sigma_pc_commute:
785 ∀p,p',graph_prog,sigma,gss,st.
786 ∀prf : well_formed_state_pc p p' graph_prog sigma gss st.
787 sigma_pc … (pc ? st) (proj1 … prf) =
788 pc ? (sigma_state_pc … st prf). // qed.
789*)
790
791(*
792lemma if_of_function_commute:
793 ∀p.
794 ∀graph_prog : joint_program (mk_graph_params p).
795 ∀graph_fun : Σi.is_internal_function_of_program … graph_prog i.
796 let graph_fd ≝ if_of_function … graph_fun in
797 let lin_fun ≝ sigma_function_name … graph_fun in
798 let lin_fd ≝ if_of_function … lin_fun in
799 lin_fd = \fst (linearise_int_fun ?? graph_fd).
800 #p #graph_prog #graph_fun whd
801 @prog_if_of_function_transform % qed.
802*)
803lemma pc_block_sigma_commute :
804∀p,p',graph_prog.
805let lin_prog ≝ linearise p graph_prog in
806∀sigma,pc.
807∀prf : well_formed_pc p p' graph_prog sigma pc.
808 pc_block (sigma_pc ? p' graph_prog sigma pc prf) =
809 pc_block pc.
810 #p #p' #graph_prog #sigma #pc #prf
811 whd in match sigma_pc; whd in match sigma_pc_opt; normalize nodelta
812 @opt_safe_elim #x
813 @if_elim #_
814 [2: #H @('bind_inversion H) -H * #i #fn #_
815   #H @('bind_inversion H) -H #n #_ ]
816 whd in ⊢ (??%?→?);
817 #EQ destruct %
818qed.
819
820(*
821lemma bind_opt_non_none : ∀A,B : Type[0] . ∀ m : option A . ∀g : A → option B.
822(! x ← m ; g x) ≠ None ? → m ≠ None ?.
823#A #B #m #g #H % #m_eq_none cases m >m_eq_none in H; normalize 
824[ #abs elim abs -abs #abs @abs %
825| #abs elim abs -abs #abs #v @abs %
826]
827qed.
828
829lemma match_option_non_none : ∀A ,B, C : Type[0]. ∀m : option A. ∀ x : A.
830∀ b : B .∀ f : A → B. ∀g : B → option C.
831g (match m with [None  ⇒ b  | Some  x ⇒ f x])≠ None ? →  g b = None ? → m ≠ None ?.
832#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
833qed.
834*)
835
836(*
837lemma funct_of_block_transf :
838∀A,B.∀progr : program (λvars .fundef (A vars)) ℕ.
839∀transf : ∀vars. A vars → B vars. ∀bl,f,prf.
840let progr' ≝ transform_program … progr (λvars.transf_fundef … (transf vars)) in
841funct_of_block … (globalenv_noinit … progr) bl = return f →
842funct_of_block … (globalenv_noinit … progr') bl = return «pi1 … f,prf».
843#A #B #progr #transf #bl #f #prf whd
844whd in match funct_of_block in ⊢ (%→?); normalize nodelta
845cut (∀A,B : Type[0].∀Q : option A → Prop.∀P : B → Prop.
846  ∀o.∀prf : Q o.
847  ∀f1,f2.
848  (∀x,prf.P (f1 x prf)) → (∀prf.P(f2 prf)) →
849  P (match o return λx.Q x → B with [ Some x ⇒ f1 x | None ⇒ f2 ] prf))
850  [ #A #B #Q #P * /2/ ] #aux
851@aux [2: #_ change with (?=Some ??→?) #ABS destruct(ABS) ]
852#fd #EQfind whd in ⊢ (??%%→?);
853generalize in ⊢ (??(??(????%))?→?); #e #EQ destruct(EQ)
854whd in match funct_of_block; normalize nodelta
855@aux [ # fd' ]
856[2: >(find_funct_ptr_transf … EQfind) #ABS destruct(ABS) ]
857#prf' cases daemon qed.
858
859lemma description_of_function_transf :
860∀A,B.∀progr : program (λvars .fundef (A vars)) ℕ.
861∀transf : ∀vars. A vars → B vars.
862let progr' ≝ transform_program … progr (λvars.transf_fundef … (transf vars)) in
863∀f_out,prf.
864description_of_function …
865  (globalenv_noinit … progr') f_out =
866transf_fundef … (transf ?) (description_of_function … (globalenv_noinit … progr)
867  «pi1 … f_out, prf»).
868#A #B #progr #transf #f_out #prf
869whd in match description_of_function in ⊢ (???%);
870normalize nodelta
871cut (∀A,B : Type[0].∀Q : option A → Prop.∀P : B → Prop.
872  ∀o.∀prf : Q o.
873  ∀f1,f2.
874  (∀x,prf.o = Some ? x → P (f1 x prf)) → (∀prf.o = None ? → P(f2 prf)) →
875  P (match o return λx.Q x → B with [ Some x ⇒ f1 x | None ⇒ f2 ] prf))
876  [ #A #B #Q #P * /2/ ] #aux
877@aux
878[ #fd' ] * #fd #EQ destruct (EQ)
879inversion (find_symbol ???) [ #_ whd in ⊢ (??%?→?); #ABS destruct(ABS) ]
880#bl #EQfind >m_return_bind #EQfindf
881whd in match description_of_function; normalize nodelta
882@aux
883[ #fdo' ] * #fdo #EQ destruct (EQ)
884>find_symbol_transf >EQfind >m_return_bind
885>(find_funct_ptr_transf … EQfindf) #EQ destruct(EQ) %
886qed.
887
888
889lemma match_int_fun :
890∀A,B : Type[0].∀P : B → Prop.
891∀Q : fundef A → Prop.
892∀m : fundef A.
893∀f1 : ∀fd.Q (Internal \ldots  fd) → B.
894∀f2 : ∀fd.Q (External … fd) → B.
895∀prf : Q m.
896(∀fd,prf.P (f1 fd prf)) →
897(∀fd,prf.P (f2 fd prf)) →
898P (match m
899return λx.Q x → ?
900with
901[ Internal fd ⇒ f1 fd
902| External fd ⇒ f2 fd
903] prf).
904#A #B #P #Q * // qed.
905(*)
906 lemma match_int_fun :
907∀A,B : Type[0].∀P : B → Prop.
908∀m : fundef A.
909∀f1 : ∀fd.m = Internal … fd → B.
910∀f2 : ∀fd.m = External … fd → B.
911(∀fd,prf.P (f1 fd prf)) →
912(∀fd,prf.P (f2 fd prf)) →
913P (match m
914return λx.m = x → ?
915with
916[ Internal fd ⇒ f1 fd
917| External fd ⇒ f2 fd
918] (refl …)).
919#A #B #P * // qed.
920*)
921(*
922lemma prova :
923∀ A.∀progr : program (λvars. fundef (A vars)) ℕ.
924∀ M : fundef (A (prog_var_names (λvars:list ident.fundef (A vars)) ℕ progr)).
925∀ f,g,prf1.
926match M return λx.M = x → option (Σi.is_internal_function_of_program ?? progr i) with
927[Internal fn ⇒ λ prf.return «g,prf1 fn prf» |
928External fn ⇒ λprf.None ? ] (refl ? M) = return f → 
929∃ fn. ∃ prf : M = Internal ? fn . f = «g, prf1 fn prf».
930#H1 #H2 #H3 #H4 #H5 #H6
931@match_int_fun
932#fd #EQ #EQ' whd in EQ' : (??%%); destruct
933%[|%[| % ]] qed.
934*)
935
936lemma int_funct_of_block_transf:
937 ∀A,B.∀progr: program (λvars. fundef (A vars)) ℕ.
938  ∀transf: ∀vars. A vars → B vars. ∀bl,f,prf.
939   let progr' ≝ transform_program … progr (λvars.transf_fundef … (transf vars)) in
940     int_funct_of_block ? (globalenv_noinit … progr) bl = return f →
941     int_funct_of_block ? (globalenv_noinit … progr') bl = return «pi1 … f,prf».
942#A #B #progr #transf #bl #f #prf
943whd whd in match int_funct_of_block in ⊢ (??%?→?); normalize nodelta
944@'bind_inversion #x #x_spec
945@match_int_fun [2: #fd #_ #ABS destruct(ABS) ]
946#fd #EQdescr change with (Some ?? = ? → ?) #EQ destruct(EQ)
947whd in match int_funct_of_block; normalize nodelta
948>(funct_of_block_transf … (internal_function_is_function … prf) … x_spec)
949>m_return_bind
950@match_int_fun #fd' #prf' [ % ]
951@⊥ cases x in prf EQdescr prf'; -x #x #x_prf #prf #EQdescr
952>(description_of_function_transf) [2: @x_prf ]
953>EQdescr whd in ⊢ (??%%→?); #ABS destruct qed.
954*)
955
956lemma symbol_for_block_match:
957    ∀M:matching.∀initV,initW.
958     (∀v,w. match_var_entry M v w →
959      size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) →
960    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
961    ∀MATCH:match_program … M p p'.
962    ∀b: block.
963    symbol_for_block … (globalenv … initW p') b =
964    symbol_for_block … (globalenv … initV p) b.
965* #A #B #V #W #match_fn #match_var #initV #initW #H
966#p #p' * #Mvars #Mfn #Mmain
967#b
968whd in match symbol_for_block; normalize nodelta
969whd in match globalenv in ⊢ (???%); normalize nodelta
970whd in match (globalenv_allocmem ????);
971change with (add_globals ?????) in match (foldl ?????);
972>(proj1 … (add_globals_match … initW … Mvars))
973[ % |*:]
974[ * #idr #v * #idr' #w #MVE %
975  [ inversion MVE
976    #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct %
977  | @(H … MVE)
978  ]
979| @(matching_fns_get_same_blocks … Mfn)
980  #f #g @match_funct_entry_id
981]
982qed.
983
984lemma symbol_for_block_transf :
985 ∀A,B,V,init.∀prog_in : program A V.
986 ∀trans : ∀vars.A vars → B vars.
987 let prog_out ≝ transform_program … prog_in trans in
988 ∀bl.
989 symbol_for_block … (globalenv … init prog_out) bl =
990 symbol_for_block … (globalenv … init prog_in) bl.
991#A #B #V #iV #p #tf @(symbol_for_block_match … (transform_program_match … tf ?))
992#v0 #w0 * //
993qed.
994
995lemma fetch_function_transf :
996 ∀A,B,V,init.∀prog_in : program A V.
997 ∀trans : ∀vars.A vars → B vars.
998 let prog_out ≝ transform_program … prog_in trans in
999 ∀bl,i,f.
1000 fetch_function … (globalenv … init prog_in) bl =
1001  return 〈i, f〉
1002→ fetch_function … (globalenv … init prog_out) bl =
1003  return 〈i, trans … f〉.
1004#A #B #V #init #prog_in #trans #bl #i #f
1005 whd in match fetch_function; normalize nodelta
1006 #H lapply (opt_eq_from_res ???? H) -H
1007 #H @('bind_inversion H) -H #id #eq_symbol_for_block
1008 #H @('bind_inversion H) -H #fd #eq_find_funct
1009 whd in ⊢ (??%?→?); #EQ destruct(EQ)
1010 >(symbol_for_block_transf … trans) >eq_symbol_for_block >m_return_bind
1011 >(find_funct_ptr_transf A B …  eq_find_funct) %
1012qed.
1013
1014lemma fetch_internal_function_transf :
1015 ∀A,B.∀prog_in : program (λvars.fundef (A vars)) ℕ.
1016 ∀trans : ∀vars.A vars → B vars.
1017 let prog_out ≝ transform_program … prog_in (λvars.transf_fundef … (trans vars)) in
1018 ∀bl,i,f.
1019 fetch_internal_function … (globalenv_noinit … prog_in) bl =
1020  return 〈i, f〉
1021→ fetch_internal_function … (globalenv_noinit … prog_out) bl =
1022  return 〈i, trans … f〉.
1023#A #B #prog #trans #bl #i #f
1024 whd in match fetch_internal_function; normalize nodelta
1025 #H @('bind_inversion H) * #id * #fd normalize nodelta #EQfetch
1026 whd in ⊢ (??%%→?); #EQ destruct(EQ)
1027 >(fetch_function_transf … EQfetch) %
1028qed.
1029 
1030(*
1031#H elim (bind_opt_inversion ????? H) -H
1032#x * whd in match funct_of_block in ⊢ (%→?); normalize nodelta
1033@match_opt_prf_elim
1034 #H #H1  whd in H : (??%?);
1035cases (   find_funct_ptr
1036   (fundef
1037    (joint_closed_internal_function
1038     (graph_prog_params p p' graph_prog
1039      (stack_sizes_lift (mk_sem_graph_params p p') (mk_sem_lin_params p p')
1040       (linearise_int_fun p) graph_prog stack_sizes))
1041     (globals
1042      (graph_prog_params p p' graph_prog
1043       (stack_sizes_lift (mk_sem_graph_params p p') (mk_sem_lin_params p p')
1044        (linearise_int_fun p) graph_prog stack_sizes)))))
1045   (ev_genv
1046    (graph_prog_params p p' graph_prog
1047     (stack_sizes_lift (mk_sem_graph_params p p') (mk_sem_lin_params p p')
1048      (linearise_int_fun p) graph_prog stack_sizes)))
1049   (pblock (pc (mk_sem_graph_params p p') st))) in H; [ 2: normalize #abs destruct
1050 
1051
1052normalize nodelta
1053#H #H1
1054cases (   find_funct_ptr
1055   (fundef
1056    (joint_closed_internal_function
1057     (graph_prog_params p p' graph_prog
1058      (stack_sizes_lift (mk_sem_graph_params p p') (mk_sem_lin_params p p')
1059       (linearise_int_fun p) graph_prog stack_sizes))
1060     (globals
1061      (graph_prog_params p p' graph_prog
1062       (stack_sizes_lift (mk_sem_graph_params p p') (mk_sem_lin_params p p')
1063        (linearise_int_fun p) graph_prog stack_sizes)))))
1064   (ev_genv
1065    (graph_prog_params p p' graph_prog
1066     (stack_sizes_lift (mk_sem_graph_params p p') (mk_sem_lin_params p p')
1067      (linearise_int_fun p) graph_prog stack_sizes)))
1068   (pblock (pc (mk_sem_graph_params p p') st))) in H;
1069
1070
1071check find_funct_ptr_transf
1072whd in match int_funct_of_block; normalize nodelta
1073#H elim (bind_inversion ????? H)
1074
1075.. sigma_int_funct_of_block
1076
1077
1078
1079whd in match int_funct_of_block; normalize nodelta
1080elim (bind_inversion ????? H)
1081whd in match int_funct_of_block; normalize nodelta
1082#H elim (bind_inversion ????? H) -H #fn *
1083#H lapply (opt_eq_from_res ???? H) -H
1084#H >(find_funct_ptr_transf … (λglobals.transf_fundef … (linearise_int_fun … globals)) … H)
1085-H #H >m_return_bind cases fn in H; normalize nodelta #arg #EQ whd in EQ:(??%%);
1086destruct //
1087cases daemon
1088qed. *)
1089
1090lemma stmt_at_sigma_commute:
1091 ∀p,globals,graph_code,entry,lin_code,lbl,pt,sigma.
1092 good_local_sigma p globals graph_code entry lin_code sigma →
1093 code_closed … lin_code →
1094 sigma lbl = return pt →
1095 ∀stmt.
1096   stmt_at … graph_code
1097    lbl = return stmt →
1098  All … (λl.sigma l ≠ None ?) (stmt_labels … stmt) ∧
1099 match stmt with
1100 [ final s' ⇒ stmt_at … lin_code pt = Some ? (final … s')
1101 | sequential s' nxt ⇒
1102             match s' with
1103             [ step_seq _ ⇒
1104               (stmt_at … lin_code pt = Some ? (sequential … s' it)) ∧
1105                  ((sigma nxt = Some ? (S pt)) ∨
1106                   (stmt_at … lin_code (S pt) = Some ? (GOTO … nxt) ∧
1107                    point_of_label … lin_code nxt = sigma nxt) )
1108             | COND a ltrue ⇒
1109               (stmt_at … lin_code pt = Some ? (sequential … s' it) ∧
1110               sigma nxt = Some ? (S pt)) ∨
1111               (stmt_at … lin_code pt = Some ? (FCOND … I a ltrue nxt) ∧
1112                point_of_label … lin_code nxt = sigma nxt)
1113             ]
1114 | FCOND abs _ _ _ ⇒ Ⓧabs   
1115 ]. 
1116 #p #globals #graph_code #entry #lin_code #lbl #pt #sigma
1117 ** #_ #all_labels_in #lin_stmt_spec #lin_code_closed #prf
1118elim (lin_stmt_spec … prf) -lin_stmt_spec #stmt1 ** #stmt1_spec
1119#All_succs_in #next_spec
1120#stmt >stmt1_spec #EQ whd in EQ : (???%); destruct(EQ)
1121% [assumption]
1122cases stmt in next_spec; -stmt
1123[ * [ #s | #a #lbl ] #nxt | #s | * ]
1124normalize nodelta
1125[ * #H #G %{H}
1126  cases G -G #G
1127  [ %1{G} ]
1128| * [ #H %1{H} ] #G
1129| //
1130] %2 %{G}
1131  lapply (refl …  (point_of_label … lin_code nxt))
1132  change with (If ? then with prf do ? else ?) in ⊢ (???%→?);
1133  @If_elim <(lin_code_has_label … (mk_lin_params p))
1134  [1,3: #_ #EQ >EQ >(all_labels_in … EQ) % ]
1135  * #H cases (H ?) -H
1136  lapply (lin_code_closed … G) ** [2: #_ * ] //
1137qed.
1138 
1139(*
1140
1141 >(if_of_function_commute … graph_fun)
1142
1143check opt_Exists
1144check linearise_int_fun
1145check
1146 whd in match (stmt_at ????);
1147 whd in match (stmt_at ????);
1148 cases (linearise_code_spec … p' graph_prog graph_fun
1149         (joint_if_entry … graph_fun))
1150 * #lin_code_closed #sigma_entry_is_zero #sigma_spec
1151 lapply (sigma_spec
1152         (point_of_pointer ? (graph_prog_params … p' graph_prog) (pc … s1)))
1153 -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @(sigma_pc_of_status_ok … prf) |2: skip ]
1154 -sigma_spec #graph_stmt * #graph_lookup_ok >graph_lookup_ok -graph_lookup_ok
1155 whd in ⊢ (? → ???%); #sigma_spec whd in sigma_spec;
1156 inversion (nth_opt ???) in sigma_spec; [ #H whd in ⊢ (% → ?); #abs cases abs ]
1157 * #optlabel #lin_stm #lin_lookup_ok whd in ⊢ (% → ?); ** #_
1158 #related_lin_stm_graph_stm #_ <related_lin_stm_graph_stm -related_lin_stm_graph_stm
1159 <sigma_pc_commute >lin_lookup_ok // *)
1160
1161definition good_sigma :
1162  ∀p.∀graph_prog : joint_program (mk_graph_params p).
1163  (joint_closed_internal_function ? (prog_var_names … graph_prog) →
1164    label → option ℕ) → Prop ≝
1165  λp,graph_prog,sigma.
1166  ∀fn : joint_closed_internal_function (mk_graph_params p) ?.
1167  good_local_sigma ?? (joint_if_code … fn) (joint_if_entry … fn)
1168    (joint_if_code … (\fst (linearise_int_fun … fn))) (sigma fn).
1169
1170lemma pc_of_label_sigma_commute :
1171  ∀p,p',graph_prog,bl,lbl,i,fn.
1172  let lin_prog ≝ linearise ? graph_prog in
1173  ∀sigma.good_sigma p graph_prog sigma →
1174  fetch_internal_function …
1175    (globalenv_noinit … graph_prog) bl = return 〈i, fn〉 →
1176  let pc' ≝ pc_of_point (mk_sem_graph_params p p') … bl lbl in
1177  code_has_label … (joint_if_code … (\fst (linearise_int_fun … fn))) lbl →
1178  ∃prf'.pc_of_label (mk_sem_lin_params p p') … (globalenv_noinit … lin_prog)
1179    bl lbl =
1180        return sigma_pc p p' graph_prog sigma pc' prf'.
1181#p #p' #graph_prog #bl #lbl #i #fn
1182#sigma #good cases (good fn) -good * #_ #all_labels_in
1183#good #fetchfn >lin_code_has_label #lbl_in
1184whd in match pc_of_label; normalize nodelta
1185> (fetch_internal_function_transf … fetchfn) >m_return_bind
1186inversion (point_of_label ????)
1187[ (*
1188  change with (If ? then with prf do ? else ? = ? → ?)
1189  @If_elim [ #prf' whd in ⊢ (??%?→?); #ABS destruct(ABS) | #ABS >ABS in lbl_in; * ]
1190  *) whd in ⊢ (??%?→?); >lbl_in whd in ⊢ (??%?→?); #ABS destruct(ABS)
1191| #pt #H lapply (all_labels_in … H) #EQsigma >m_return_bind
1192  %
1193  [ @hide_prf whd %
1194  | whd in match sigma_pc; normalize nodelta
1195    @opt_safe_elim #pc'
1196  ]
1197  whd in match sigma_pc_opt; normalize nodelta
1198  @eqZb_elim #Hbl normalize nodelta
1199  [1,3: >(fetch_internal_function_no_minus_one … Hbl) in fetchfn;
1200  |*: >fetchfn >m_return_bind
1201    >point_of_pc_of_point
1202    >EQsigma
1203  ] whd in ⊢ (??%%→?); #EQ destruct(EQ) %
1204]
1205qed.
1206
1207lemma graph_pc_of_label :
1208  ∀p,p'.let pars ≝ make_sem_graph_params p p' in
1209  ∀globals,ge,bl,i_fn,lbl.
1210  fetch_internal_function ? ge bl = return i_fn →
1211  pc_of_label pars globals ge bl lbl =
1212    OK ? (pc_of_point pars bl lbl).
1213#p #p' #globals #ge #bl #fn #lbl #fetchfn
1214whd in match pc_of_label; normalize nodelta
1215>fetchfn %
1216qed.
1217
1218lemma point_of_pc_sigma_commute :
1219 ∀p,p',graph_prog.
1220 let lin_prog ≝ linearise p graph_prog in
1221 ∀sigma,pc,f,fn,n.
1222  ∀prf : well_formed_pc p p' graph_prog sigma pc.
1223 fetch_internal_function … (globalenv_noinit … graph_prog) (pc_block pc) = return 〈f, fn〉 →
1224 sigma fn (point_of_pc (mk_sem_graph_params p p') pc) = return n →
1225 point_of_pc (mk_sem_lin_params p p') (sigma_pc … pc prf) = n.
1226#p #p' #graph_prog #sigma #pc #f #fn #n #prf #EQfetch #EQsigma
1227whd in match sigma_pc; normalize nodelta
1228@opt_safe_elim #pc' whd in match sigma_pc_opt;
1229normalize nodelta @eqZb_elim #Hbl
1230[ >(fetch_internal_function_no_minus_one … Hbl) in EQfetch;
1231  whd in ⊢ (???%→?); #ABS destruct(ABS) ]
1232>EQfetch >m_return_bind >EQsigma
1233whd in ⊢ (??%%→?); #EQ destruct(EQ)
1234@point_of_offset_of_point 
1235qed.
1236
1237lemma graph_succ_pc :
1238  ∀p,p'.let pars ≝ make_sem_graph_params p p' in
1239  ∀pc,lbl.
1240  succ_pc pars pc lbl = pc_of_point pars (pc_block pc) lbl.
1241normalize //
1242qed.
1243
1244lemma fetch_statement_sigma_commute:
1245  ∀p,p',graph_prog,pc,f,fn,stmt.
1246  let lin_prog ≝ linearise ? graph_prog in
1247  ∀sigma.good_sigma p graph_prog sigma →
1248  ∀prf : well_formed_pc p p' graph_prog sigma pc.
1249  fetch_statement (mk_sem_graph_params p p') …
1250    (globalenv_noinit ? graph_prog) pc = return 〈f, fn,stmt〉 →
1251  All ? (λlbl.∃prf:well_formed_pc p p' graph_prog sigma
1252      (pc_of_point (mk_sem_graph_params p p') (pc_block pc) lbl).
1253      pc_of_label (mk_sem_lin_params p p') …
1254          (globalenv_noinit … lin_prog)
1255          (pc_block pc)
1256          lbl = return sigma_pc … prf)
1257    (stmt_explicit_labels … stmt) ∧
1258  match stmt with
1259  [  sequential s nxt ⇒
1260        match s with
1261        [ step_seq x ⇒
1262          fetch_statement (mk_sem_lin_params p p') …
1263          (globalenv_noinit … lin_prog) (sigma_pc … pc prf) =
1264              return 〈f, \fst (linearise_int_fun … fn),
1265                      sequential (mk_lin_params p) … (step_seq … x ) it〉 ∧
1266          ∃prf'.
1267            let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (mk_sem_graph_params p p') pc nxt) prf' in
1268            let nxt_pc ≝ succ_pc (mk_sem_lin_params p p') (sigma_pc … pc prf) it in
1269            (nxt_pc = sigma_nxt ∨
1270              (fetch_statement (mk_sem_lin_params p p') …
1271                (globalenv_noinit … lin_prog) nxt_pc =
1272                return 〈f, \fst (linearise_int_fun … fn),
1273                         final (mk_lin_params p) … (GOTO … nxt)〉 ∧
1274              (pc_of_label (mk_sem_lin_params p p') …
1275                (globalenv_noinit … lin_prog)
1276                (pc_block pc)
1277                nxt = return sigma_nxt)))
1278        | COND a ltrue ⇒
1279            ∃prf'.
1280            let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (mk_sem_graph_params p p') pc nxt) prf' in
1281            (let nxt_pc ≝ succ_pc (make_sem_lin_params p p') (sigma_pc … pc prf) it in
1282            (fetch_statement (mk_sem_lin_params p p') …
1283            (globalenv_noinit … lin_prog) (sigma_pc … pc prf) =
1284              return 〈f, \fst (linearise_int_fun … fn),
1285                      sequential (mk_lin_params p) … (COND … a ltrue) it〉 ∧
1286             nxt_pc = sigma_nxt)) ∨
1287            (fetch_statement (mk_sem_lin_params p p') … (globalenv_noinit … lin_prog) (sigma_pc … pc prf) 
1288             =
1289             return 〈f, \fst (linearise_int_fun … fn), FCOND (mk_lin_params p) … I a ltrue nxt〉 ∧
1290            pc_of_label (mk_sem_lin_params p p') …
1291                (globalenv_noinit … lin_prog)
1292                (pc_block pc)
1293                nxt = return sigma_nxt)
1294         ]
1295    | final z ⇒   fetch_statement (mk_sem_lin_params p p') …
1296                   (globalenv_noinit … lin_prog) (sigma_pc … pc prf) =
1297                   return 〈f, \fst (linearise_int_fun … fn), final  (mk_lin_params p) … z〉
1298    | FCOND abs _ _ _ ⇒ Ⓧabs
1299  ].
1300#p #p' #graph_prog #pc #f #fn #stmt #sigma
1301#good elim (good fn) * #_ #all_labels_in #good_local #wfprf
1302#H elim (fetch_statement_inv … H) #fetchfn #graph_stmt
1303whd in match well_formed_pc in wfprf; normalize nodelta in wfprf;
1304inversion(sigma_pc_opt p p' graph_prog sigma pc)
1305[#ABS @⊥ >ABS in wfprf; * #H @H %]
1306#lin_pc
1307whd in match sigma_pc_opt in ⊢ (%→?); normalize nodelta  in ⊢ (%→?);
1308@eqZb_elim #Hbl
1309[ >(fetch_internal_function_no_minus_one … Hbl) in fetchfn; #ABS destruct(ABS) ]
1310normalize nodelta >fetchfn >m_return_bind
1311#H @('bind_inversion H) -H
1312#lin_pt #lin_pt_spec #EQ whd in EQ : (??%?); destruct(EQ)
1313lapply(stmt_at_sigma_commute ???????? (good fn) ??? graph_stmt)
1314[@lin_pt_spec|@(pi2 … (\fst (linearise_int_fun … fn)))|] * #H1 #H2 %
1315[ cases stmt in H2;
1316  [ * [#s|#a#lbl]#nxt | #s | *]
1317  normalize nodelta
1318  [ * #stmt_at_EQ #_ | ** #stmt_at_EQ #_ | #stmt_at_EQ ]
1319  cases (pi2 … (\fst (linearise_int_fun … fn)) … stmt_at_EQ)
1320  #H #_
1321  [1,2,4: @(All_mp … H) #lbl @(pc_of_label_sigma_commute … good … fetchfn)
1322  |3: cases H -H #H #_ %{I} @(pc_of_label_sigma_commute … good … fetchfn) @H
1323  ]
1324]
1325cases (stmt) in H1 H2; [ * [ #s | #a #ltrue ] #nxt | #s | * ] normalize nodelta
1326#all_labels_spec #H3 whd in match fetch_statement; normalize nodelta
1327>pc_block_sigma_commute
1328>(fetch_internal_function_transf … fetchfn) >m_return_bind
1329>(point_of_pc_sigma_commute … fetchfn lin_pt_spec)
1330[ %
1331   [ >(proj1 … H3) %
1332   | % [ @hide_prf %
1333     | change with (opt_safe ???) in match (sigma_pc ???? (succ_pc ???) ?);
1334       @opt_safe_elim #pc1
1335     ] whd in match sigma_pc_opt;
1336        normalize nodelta >(eqZb_false … Hbl) >fetchfn
1337        >m_return_bind
1338        >graph_succ_pc >point_of_pc_of_point
1339        cases(proj2 … H3)
1340        [1,3: #EQ >EQ
1341        |*: * cases all_labels_spec #Z #_ #sn
1342          >(opt_to_opt_safe … Z) #EQpoint_of_label
1343        ] whd in ⊢ (??%?→?); #EQ destruct(EQ)
1344        [ %1
1345          whd in match (point_of_succ ???) ;
1346          whd in match point_of_pc; normalize nodelta
1347          whd in match sigma_pc; whd in match sigma_pc_opt; normalize nodelta
1348          @opt_safe_elim >(eqZb_false … Hbl) >fetchfn >m_return_bind
1349          >lin_pt_spec #pc' whd in ⊢ (??%%→?); #EQ destruct(EQ)
1350          whd in match succ_pc; whd in match point_of_pc; normalize nodelta
1351          >point_of_offset_of_point %
1352        | %2 whd in match (pc_block ?); >pc_block_sigma_commute
1353          >(fetch_internal_function_transf … fetchfn) >m_return_bind
1354          whd in match sigma_pc; whd in match sigma_pc_opt; normalize nodelta
1355          @opt_safe_elim >(eqZb_false … Hbl) normalize nodelta
1356          #pc_lin >fetchfn >m_return_bind >lin_pt_spec >m_return_bind
1357          whd in match pc_of_point; normalize nodelta #EQ whd in EQ : (??%?); destruct
1358          whd in match point_of_pc; whd in match succ_pc; normalize nodelta
1359          whd in match point_of_pc; normalize nodelta >point_of_offset_of_point
1360          whd in match pc_of_point; normalize nodelta >point_of_offset_of_point
1361          >sn >m_return_bind % [%] whd in match pc_of_label; normalize nodelta
1362           >(fetch_internal_function_transf … fetchfn) >m_return_bind
1363           >EQpoint_of_label %
1364        ]
1365   ]
1366 | % [ @hide_prf % whd in match sigma_pc_opt; normalize nodelta
1367      >(eqZb_false … Hbl) normalize nodelta whd in match (pc_block ?); >fetchfn
1368      >m_return_bind whd in match point_of_pc; whd in match succ_pc; normalize nodelta
1369      whd in match pc_of_point; whd in match point_of_pc; normalize nodelta
1370      >point_of_offset_of_point cases all_labels_spec #H >(opt_to_opt_safe … H) #_
1371      >m_return_bind #ABS whd in ABS : (??%?); destruct(ABS)]
1372   cases H3 * #nxt_spec #point_of_lab_spec >nxt_spec >m_return_bind
1373      [%1 % [%] whd in match sigma_pc; whd in match sigma_pc_opt; normalize nodelta
1374       @opt_safe_elim #lin_pc1 @opt_safe_elim #lin_pc2
1375       >(eqZb_false … Hbl) normalize nodelta >fetchfn >m_return_bind
1376       >m_return_bind in ⊢ (? → % → ?); whd in match point_of_pc; whd in match succ_pc;
1377       normalize nodelta whd in match pc_of_point; whd in match point_of_pc; normalize nodelta
1378       >point_of_offset_of_point >point_of_lab_spec >m_return_bind #EQ
1379       whd in EQ : (??%?); destruct(EQ) >lin_pt_spec >m_return_bind #EQ
1380       whd in EQ : (??%?); destruct(EQ) >point_of_offset_of_point %
1381      |%2 >m_return_bind >nxt_spec >m_return_bind %[%] whd in match pc_of_label;
1382       normalize nodelta >(fetch_internal_function_transf … fetchfn)
1383       >m_return_bind >point_of_lab_spec cases all_labels_spec #H #INUTILE
1384       >(opt_to_opt_safe … H) in ⊢ (??%?); >m_return_bind
1385       normalize in ⊢ (??%?);
1386       whd in match sigma_pc; whd in match sigma_pc_opt; normalize nodelta
1387       @opt_safe_elim >(eqZb_false … Hbl) normalize nodelta whd in match (pc_block ?);
1388       >fetchfn >m_return_bind whd in match point_of_pc; whd in match succ_pc;
1389       normalize nodelta whd in match point_of_pc; whd in match pc_of_point;
1390       normalize nodelta >point_of_offset_of_point cases (sigma fn nxt) in H;
1391       [ * #ABS @⊥ @ABS %] #linear_point * #INUTILE1 #linear_pc >m_return_bind
1392       #EQ whd in EQ : (??%?); destruct(EQ) normalize nodelta %
1393      ]
1394  | >H3 >m_return_bind %
1395]
1396qed.
1397
1398(*
1399spostato in ExtraMonads.ma
1400
1401lemma res_eq_from_opt : ∀A,m,a.
1402res_to_opt A m = return a → m = return a.
1403#A #m #a  cases m #x normalize #EQ destruct(EQ) %
1404qed.
1405
1406lemma res_to_opt_preserve : ∀X,Y,P,F,m,n.
1407  res_preserve X Y P F m n → opt_preserve X Y P F (res_to_opt … m) (res_to_opt … n).
1408#X #Y #P #F #m #n #H #x #EQ
1409cases (H x ?)
1410[ #prf #EQ' %{prf} >EQ' %
1411| cases m in EQ; normalize #x #EQ destruct %
1412]
1413qed.
1414*)
1415lemma sigma_pc_exit :
1416  ∀p,p',graph_prog,sigma,pc,prf.
1417  let exit ≝ mk_program_counter «mk_block Code (-1), refl …» one in
1418  pc = exit →
1419  sigma_pc p p' graph_prog sigma pc prf = exit.
1420#p #p' #graph_prog #sigma #pc #prf
1421whd in match sigma_pc; normalize nodelta @opt_safe_elim #pc'
1422#EQ1 #EQ2 destruct
1423whd in match sigma_pc_opt in EQ1; whd in EQ1 : (??%?);
1424destruct %
1425qed.
1426
1427(* this should make things easier for ops using memory (where pc cant happen) *)
1428definition bv_no_pc : beval → Prop ≝
1429λbv.match bv with [ BVpc _ _ ⇒ False | _ ⇒ True ].
1430
1431lemma bv_pc_other :
1432  ∀P : beval → Prop.
1433  (∀pc,p.P (BVpc pc p)) →
1434  (∀bv.bv_no_pc bv → P bv) →
1435  ∀bv.P bv.
1436#P #H1 #H2 * /2/ qed.
1437
1438lemma sigma_bv_no_pc : ∀p,p',graph_prog,sigma,bv,prf.
1439  bv_no_pc bv →
1440  sigma_beval p p' graph_prog sigma bv prf = bv.
1441#p #p' #graph_prog #sigma *
1442[|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p ]
1443#prf * whd in match sigma_beval; normalize nodelta
1444@opt_safe_elim #bv' normalize #EQ destruct(EQ) %
1445qed.
1446
1447lemma bv_no_pc_wf : ∀p,p',graph_prog,sigma,bv.
1448bv_no_pc bv → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?.
1449#p #p' #graph_prog #sigma *
1450[|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p ] *
1451% whd in ⊢ (??%?→?); #ABS destruct(ABS) qed.
1452
1453lemma Byte_of_val_inv : ∀bv,e,by.Byte_of_val e bv = return by → bv = BVByte by.
1454* [|| #a #b #c |#p | #p | #p #pa | #p #pa ] #e #by
1455  whd in ⊢ (??%%→?); #EQ destruct(EQ) % qed.
1456
1457lemma sigma_pc_no_exit :
1458  ∀p,p',graph_prog,sigma,pc,prf.
1459  let exit ≝ mk_program_counter «mk_block Code (-1), refl …» one in
1460  pc ≠ exit →
1461  sigma_pc p p' graph_prog sigma pc prf ≠ exit.
1462#p #p' #graph_prog #sigma #pc #prf
1463@(eqZb_elim (block_id (pc_block pc)) (-1))
1464[ #Hbl
1465  whd in match sigma_pc; normalize nodelta @opt_safe_elim #pc'
1466  whd in match sigma_pc_opt; normalize nodelta
1467  >Hbl whd in ⊢ (??%?→?); #EQ destruct(EQ) // ]
1468#NEQ #_ inversion (sigma_pc ??????)
1469** #r #id #EQr #off #EQ
1470lapply (pc_block_sigma_commute …prf) >EQ #EQ' >EQ'
1471% #ABS destruct(ABS) cases NEQ #H @H -H
1472cases (pc_block ?) in e0; * #r #id' #EQ'' >EQ'' #EQ''' destruct(EQ''') %
1473qed.
1474
1475definition linearise_status_rel:
1476 ∀p,p',graph_prog.
1477 let lin_prog ≝ linearise p graph_prog in
1478 ∀stack_sizes.
1479 ∀sigma. ∀ gss : good_state_sigma p p' graph_prog sigma.
1480 good_sigma p graph_prog sigma →
1481   status_rel
1482    (graph_abstract_status p p' graph_prog stack_sizes)
1483    (lin_abstract_status p p' lin_prog stack_sizes)
1484 ≝ λp,p',graph_prog,stack_sizes,sigma,gss,good.
1485   mk_status_rel …
1486    (* sem_rel ≝ *) (λs1,s2.
1487     ∃prf: well_formed_state_pc p p' graph_prog sigma gss s1.
1488      s2 = sigma_state_pc … s1 prf)
1489    (* call_rel ≝ *) (λs1,s2.
1490      ∃prf:well_formed_state_pc p p' graph_prog sigma gss s1.
1491      pc ? s2 = sigma_pc … (pc ? s1) (proj2 … (proj1 … prf)))
1492    (* sim_final ≝ *) ?.
1493#st1 #st2 * #prf #EQ2
1494% [2: cases daemon]
1495>EQ2
1496whd in ⊢ (%→%);
1497#H lapply (opt_to_opt_safe … H)
1498@opt_safe_elim -H #res #_ whd in match is_final; normalize nodelta
1499#H lapply(res_eq_from_opt ??? H) -H
1500#H  @('bind_inversion H) -H
1501** #id #int_f #stmt
1502#stmt_spec cases (fetch_statement_sigma_commute ???????? good (proj2 … (proj1 … prf)) stmt_spec)
1503cases stmt in stmt_spec; -stmt normalize nodelta
1504[1,3: [ #a #b #_| #a #b #c #d #e] #_ #_ #ABS whd in ABS : (???%); destruct(ABS)]
1505* normalize nodelta
1506[1,3: [#l| #a #b #c] #_ #_ #_ #ABS whd in ABS: (???%); destruct(ABS)]
1507#fetch_graph_spec #_ #fetch_lin_spec
1508#H >fetch_lin_spec >m_return_bind normalize nodelta
1509letin graph_ge ≝ (ev_genv (graph_prog_params p p' graph_prog stack_sizes))
1510letin lin_ge ≝ (ev_genv (lin_prog_params p p' (linearise p graph_prog) stack_sizes))
1511cut (preserving … res_preserve …
1512       (sigma_state … gss)
1513       (λl.λ_ : True.l)
1514       (λst.
1515          do st' ← pop_frame … graph_ge id int_f st;
1516          if eq_program_counter (pc … st') exit_pc then
1517          do vals ← read_result … graph_ge (joint_if_result … int_f) st ;
1518            Word_of_list_beval vals
1519          else
1520            Error ? [ ])
1521       (λst.
1522          do st' ← pop_frame … lin_ge id (\fst (linearise_int_fun … int_f)) st;
1523          if eq_program_counter (pc … st') exit_pc then
1524          do vals ← read_result … lin_ge (joint_if_result … (\fst (linearise_int_fun … int_f))) st ;
1525            Word_of_list_beval vals
1526          else
1527            Error ? [ ]))
1528[ #st #prf @mfr_bind [3: @pop_frame_commute |*:]
1529  #st' #prf' @eq_program_counter_elim 
1530  [ #EQ_pc normalize nodelta
1531    change with (sigma_pc ??????) in match (pc ??);
1532    >(sigma_pc_exit … EQ_pc) normalize nodelta
1533    @mfr_bind [3: @read_result_commute |*:]
1534    #lbv #prf_lbv @opt_safe_elim #lbv' #EQ_lbv'
1535    @(mfr_bind … (λpr,prf.〈\fst pr, opt_safe …
1536        (m_list_map … (sigma_beval_opt p p' graph_prog sigma) (\snd pr)) prf〉))
1537    [
1538    | * -lbv -lbv' #by1 #lbv #lbv_prf
1539      @(mfr_bind … (λpr,prf.〈\fst pr, opt_safe …
1540        (m_list_map … (sigma_beval_opt p p' graph_prog sigma) (\snd pr)) prf〉))
1541    [ @opt_safe_elim #lbv' #EQ_lbv'
1542    |* -lbv #by2 #lbv #lbv_prf
1543      @(mfr_bind … (λpr,prf.〈\fst pr, opt_safe …
1544        (m_list_map … (sigma_beval_opt p p' graph_prog sigma) (\snd pr)) prf〉))
1545    [ @opt_safe_elim #lbv' #EQ_lbv'
1546    |* -lbv #by3 #lbv #lbv_prf
1547      @(mfr_bind … (λpr,prf.〈\fst pr, opt_safe …
1548        (m_list_map … (sigma_beval_opt p p' graph_prog sigma) (\snd pr)) prf〉))
1549    [ @opt_safe_elim #lbv' #EQ_lbv'
1550    |* -lbv #by4 * [2: #by5 #tl #lbv_prf @res_preserve_error ]
1551      #lbv_prf @mfr_return %
1552    ]]]]
1553    cases lbv in EQ_lbv';
1554    try (#H @res_preserve_error)
1555    -lbv #by1 #lbv #H @('bind_inversion H) -H #by1' #EQby1'
1556    #H @('bind_inversion H) -H #tl' #EQtl'
1557    whd in ⊢ (??%?→?); #EQ destruct(EQ)
1558    @(mfr_bind … (λby.λ_:True.by))
1559    [1,3,5,7: #by #EQ %{I} >(Byte_of_val_inv … EQ) in EQby1';
1560      whd in ⊢ (??%%→?); #EQ destruct(EQ) %
1561    |*: #by1 * @mfr_return_eq
1562      change with (m_list_map ????? = ?) in EQtl';
1563      [1,3,5,7: %
1564      |*: @opt_safe_elim #lbv''
1565      ] >EQtl' #EQ destruct %
1566    ]
1567  | #_ @res_preserve_error
1568  ]
1569]
1570#PRESERVE
1571cases (PRESERVE … (proj2 … prf) … H) *
1572#EQ >EQ % whd in ⊢ (??%?→?); #ABS destruct(ABS)
1573qed.
1574
1575lemma as_label_sigma_commute :
1576  ∀p,p',graph_prog,stack_sizes,sigma,gss.good_sigma p graph_prog sigma →
1577  ∀st,prf.
1578  as_label (lin_abstract_status p p' (linearise … graph_prog) stack_sizes)
1579    (sigma_state_pc p p' graph_prog sigma gss st prf) =
1580  as_label (graph_abstract_status p p' graph_prog stack_sizes) st.
1581#p #p' #graph_prog #stack_sizes #sigma #gss #good * #st #pc #popped
1582** #prf1 #prf2 #prf3
1583change with (as_label_of_pc ?? = as_label_of_pc ??)
1584change with (sigma_pc ??????) in match (as_pc_of ??);
1585change with pc in match (as_pc_of ??);
1586whd in match sigma_pc; normalize nodelta
1587@opt_safe_elim #pc'
1588whd in match sigma_pc_opt; normalize nodelta
1589@eqZb_elim #Hbl normalize nodelta
1590[ whd in ⊢ (??%%→??%%); #EQ destruct(EQ)
1591  whd in match fetch_statement; normalize nodelta
1592  >(fetch_internal_function_no_minus_one … graph_prog … Hbl)
1593  >(fetch_internal_function_no_minus_one … (linearise … graph_prog) … Hbl) %
1594| #H @('bind_inversion H) * #i #f -H
1595  inversion (fetch_internal_function … (pc_block pc))
1596  [2: #e #_ whd in ⊢ (??%%→?); #ABS destruct(ABS) ]
1597  * #i' #f' #EQfetch whd in ⊢ (??%%→?); #EQ destruct(EQ)
1598  #H @('bind_inversion H) #n #EQsigma whd in ⊢ (??%%→?); #EQ destruct(EQ)
1599  whd in ⊢ (??%%);
1600  whd in match fetch_statement; normalize nodelta >EQfetch
1601  >(fetch_internal_function_transf … graph_prog
1602    (λvars,fn.\fst (linearise_int_fun … fn)) … EQfetch)
1603  >m_return_bind >m_return_bind
1604  cases (good f) * #_ #all_labels_in #spec
1605  cases (spec … EQsigma) #s ** cases s -s
1606  [ * [#s|#a#lbl]#nxt|#s|*] normalize nodelta #EQstmt_at #_
1607  [ * #EQstmt_at' #_ | * [ * #EQstmt_at' #_ | #EQstmt_at' ] | #EQstmt_at' ]
1608  whd in match point_of_pc; normalize nodelta >point_of_offset_of_point
1609  >EQstmt_at >EQstmt_at' normalize nodelta %
1610qed.
1611 
1612lemma set_istack_sigma_commute :
1613∀p,p',graph_prog,sigma,gss,st,is,prf1,prf2,prf3.
1614set_istack ? (sigma_is p p' graph_prog sigma is prf1) (sigma_state p p' graph_prog sigma gss st prf2) =
1615sigma_state ???? gss (set_istack ? is st) prf3.
1616#p #p' #graph_prog #sigma #gss *
1617#frms #is' #carry #r #m #is #prf1 #prf2 #prf3 % qed.
1618(* #st #is #sigmais #prf1 #prf2 #H
1619whd in match set_istack; normalize nodelta
1620whd in match sigma_state; normalize nodelta
1621whd in match sigma_is; normalize nodelta
1622@opt_safe_elim #x #H1
1623cut(x = sigmais) [>H1 in H; #EQ whd in EQ : (???%); destruct(EQ) %]
1624#EQ >EQ //
1625qed.*)
1626
1627lemma is_push_sigma_commute :
1628∀ p, p', graph_prog,sigma.
1629preserving2 … res_preserve …
1630  (sigma_is p p' graph_prog sigma)
1631  (sigma_beval p p' graph_prog sigma) 
1632  (sigma_is p p' graph_prog sigma)
1633  is_push is_push.
1634#p #p' #graph_prog #sigma *
1635[ | #bv1 | #bv1 #bv2 ] #val #prf1 #prf2 #is'
1636whd in ⊢ (??%%→?); #EQ destruct(EQ)
1637whd in match sigma_beval; normalize nodelta
1638@opt_safe_elim #val' #EQsigma_val
1639%
1640[1,3: @hide_prf %
1641|*: whd in match sigma_is in ⊢ (???%); normalize nodelta
1642  @opt_safe_elim #is''
1643] whd in match sigma_is_opt; normalize nodelta
1644[2,4:
1645  inversion (sigma_beval_opt ?????)
1646  [1,3: #EQ whd in prf1 : (?(??%?)); @⊥ >EQ in prf1;
1647    normalize nodelta * #H @H % ]
1648  #bv1' #EQ_bv1' >m_return_bind ]
1649>EQsigma_val
1650whd in ⊢ (??%%→?); #EQ destruct(EQ)
1651whd in match sigma_is; normalize nodelta
1652@opt_safe_elim #is1
1653whd in match sigma_is_opt; normalize nodelta
1654[ #H @('bind_inversion H) #bv1''
1655  >EQ_bv1' #EQ destruct(EQ) ]
1656whd in ⊢ (??%%→?); #EQ destruct(EQ) %
1657qed.
1658
1659lemma Bit_of_val_inv :
1660  ∀e,bb,v.Bit_of_val e bb = return v → bb = BBbit v.
1661#e *
1662[ #b || #b #ptr #p #o ] #v
1663whd in ⊢ (??%%→?); #EQ destruct(EQ) % qed.
1664
1665lemma beopaccs_sigma_commute :
1666∀p,p',graph_prog,sigma,op.
1667preserving2 … res_preserve …
1668  (sigma_beval p p' graph_prog sigma)
1669  (sigma_beval p p' graph_prog sigma)
1670  (λpr,prf.〈sigma_beval p p' graph_prog sigma (\fst pr) (proj1 ?? prf),
1671            sigma_beval p p' graph_prog sigma (\snd pr) (proj2 ?? prf)〉)
1672  (be_opaccs op) (be_opaccs op).
1673#p #p' #graph_prog #sigma #op
1674#bv1 #bv2 #prf1 #prf2
1675@mfr_bind [ @(λ_.True) | @(λx.λ_.x) ]
1676[2: #by1 * @mfr_bind [ @(λ_.True) | @(λx.λ_.x) ]
1677  [2: #by2 * cases (opaccs ????) #by1' #by2'
1678    @mfr_return %% whd in ⊢ (??%%→?); #EQ destruct(EQ)
1679  ]
1680]
1681#v #EQ %{I}
1682>sigma_bv_no_pc try assumption
1683>(Byte_of_val_inv … EQ) %
1684qed.
1685
1686lemma beop1_sigma_commute :
1687∀p,p',graph_prog,sigma,op.
1688preserving … res_preserve …
1689  (sigma_beval p p' graph_prog sigma)
1690  (sigma_beval p p' graph_prog sigma)
1691  (be_op1 op) (be_op1 op).
1692#p #p' #graph_prog #sigma #op
1693#bv #prf
1694@mfr_bind [ @(λ_.True) | @(λx.λ_.x) ]
1695[2: #by * @mfr_return % whd in ⊢ (??%%→?); #EQ destruct(EQ) ]
1696#v #EQ %{I} >sigma_bv_no_pc try assumption
1697>(Byte_of_val_inv … EQ) %
1698qed.
1699
1700
1701lemma sigma_ptr_commute :
1702∀ p, p', graph_prog , sigma.
1703preserving … res_preserve …
1704  (λpr,prf.〈sigma_beval p p' graph_prog sigma (\fst pr) (proj1 ?? prf),
1705            sigma_beval p p' graph_prog sigma (\snd pr) (proj2 ?? prf)〉)
1706  (λx.λ_ : True.x)
1707  pointer_of_address pointer_of_address.
1708#p #p' #graph_prog #sigma * #val1 #val2 * #prf1 #prf2
1709#ptr whd in ⊢ (??%?→?);
1710cases val1 in prf1;
1711[|| #ptr1 #ptr2 #p | #by | #p | #ptr1 #p1 | #pc #p ]
1712#prf1 whd in ⊢ (??%%→?); #EQ destruct(EQ)
1713cases val2 in prf2 EQ;
1714[|| #ptr1 #ptr2 #p | #by | #p | #ptr2 #p2 | #pc #p ]
1715#prf2 normalize nodelta #EQ destruct(EQ)
1716%{I}
1717>sigma_bv_no_pc [2: %]
1718>sigma_bv_no_pc [2: %] @EQ
1719qed.
1720
1721lemma beop2_sigma_commute :
1722∀p,p',graph_prog,sigma,carry,op.
1723preserving2 … res_preserve …
1724  (sigma_beval p p' graph_prog sigma)
1725  (sigma_beval p p' graph_prog sigma)
1726  (λpr,prf.〈sigma_beval p p' graph_prog sigma (\fst pr) prf, \snd pr〉)
1727  (be_op2 carry op) (be_op2 carry op).
1728#p #p' #graph_prog #sigma #carry #op
1729@bv_pc_other
1730[ #pc1 #p1 #bv2
1731| #bv1 #bv1_no_pc
1732  @bv_pc_other
1733  [ #pc2 #p2
1734  | #bv2 #bv2_no_pc
1735  ]
1736] #prf1 #prf2
1737* #res #carry'
1738[1,2:
1739  [2: cases bv1 in prf1;
1740    [|| #ptr11 #ptr12 #p1 | #by1 | #p1 | #ptr1 #p1 | #pc1 #p1 ] #prf1 ]
1741   whd in ⊢ (??%%→?);
1742  #EQ destruct(EQ) ]
1743#EQ
1744cut (bv_no_pc res)
1745[ -prf1 -prf2
1746  cases bv1 in bv1_no_pc EQ;
1747  [|| #ptr11 #ptr12 #p1 | #by1 | #p1 | #ptr1 #p1 | #pc1 #p1 ] *
1748  cases bv2 in bv2_no_pc;
1749  [3,10,17,24,31,38: #ptr21 #ptr22 #p2
1750  |4,11,18,25,32,39: #by2
1751  |5,12,19,26,33,40: #p2
1752  |6,13,20,27,34,41: #ptr2 #p2
1753  |7,14,21,28,35,42: #pc2 #p2
1754  ] *
1755  cases op
1756  whd in match be_op2; whd in ⊢ (???%→?);
1757  normalize nodelta
1758  #EQ destruct(EQ) try %
1759  try (whd in EQ : (??%?); destruct(EQ) %)
1760  lapply EQ -EQ
1761  [ @if_elim #_ [ @if_elim #_ ] whd in ⊢ (??%%→?); #EQ destruct(EQ) %
1762  |2,12,13,16,18: @if_elim #_  whd in ⊢ (??%%→?); #EQ destruct(EQ) %
1763  |3,4,5,6,7,8: #H @('bind_inversion H) #bit #EQ
1764    cases (op2 eval bit ???) #res' #bit'
1765    whd in ⊢ (??%%→?); #EQ destruct(EQ) %
1766  |17: cases (ptype ptr1) normalize nodelta
1767    [ @if_elim #_
1768      [ #H @('bind_inversion H) #bit #EQbit
1769      cases (op2 eval bit ???) #res' #bit'
1770      ]
1771    ]
1772    whd in ⊢ (??%%→?); #EQ destruct(EQ) %
1773  |*: whd in ⊢ (??%?→?);
1774    cases (ptype ?) normalize nodelta
1775    try (#EQ destruct(EQ) @I)
1776    cases (part_no ?) normalize nodelta
1777    try (#n lapply (refl ℕ n) #_)
1778    try (#EQ destruct(EQ) @I)
1779    try (#H @('bind_inversion H) -H * #EQbit
1780         whd in ⊢ (??%%→?);)
1781    try (#EQ destruct(EQ) @I)
1782    [1,2,4,6,7: cases (op2 eval ????) #res' #bit' whd in ⊢ (??%%→?);
1783         #EQ destruct(EQ) @I
1784    |*: cases carry normalize nodelta
1785      try (#b lapply (refl bool b) #_)
1786      try (#ptr lapply (refl pointer ptr) #_ #p #o)
1787      try (#EQ destruct(EQ) @I)
1788      @if_elim #_
1789      try (#EQ destruct(EQ) @I)
1790      @If_elim #prf
1791      try (#EQ destruct(EQ) @I)
1792      cases (op2_bytes ?????)
1793      #res' #bit' whd in ⊢ (??%%→?);
1794      #EQ destruct(EQ) @I
1795    ]
1796  ]
1797] #res_no_pc
1798%{(bv_no_pc_wf … res_no_pc)}
1799>(sigma_bv_no_pc … bv1_no_pc)
1800>(sigma_bv_no_pc … bv2_no_pc)
1801>(sigma_bv_no_pc … res_no_pc)
1802assumption
1803qed.
1804
1805definition combine_strong :
1806  ∀A,B,C,D : Type[0].
1807  ∀P : A → Prop.∀Q : C → Prop.
1808  (∀x.P x → B) → (∀x.Q x → D) →
1809  (∀pr.(P (\fst pr) ∧ Q (\snd pr)) → B × D) ≝
1810λA,B,C,D,P,Q,f,g,pr,prf.〈f ? (proj1 … prf), g ? (proj2 … prf)〉.
1811
1812lemma wf_set_is : ∀p,p',graph_prog,sigma,gss,st,is.
1813well_formed_state p p' graph_prog sigma gss st →
1814sigma_is_opt p p' graph_prog sigma is ≠ None ? →
1815well_formed_state … gss (set_istack … is st).
1816#p #p' #graph_prog #sigma #gss #st #is
1817*** #H1 #H2 #H3 #H4 #H5
1818%{H4} %{H3} %{H5} @H1
1819qed.
1820
1821lemma wf_set_m : ∀p,p',graph_prog,sigma,gss,st,m.
1822well_formed_state p p' graph_prog sigma gss st →
1823well_formed_mem p p' graph_prog sigma m →
1824well_formed_state … gss (set_m … m st).
1825#p #p' #graph_prog #sigma #gss #st #m
1826*** #H1 #H2 #H3 #H4 #H5
1827%{H5} %{H3} %{H2} @H1
1828qed.
1829(* spostato in ExtraMonads.ma
1830lemma opt_to_res_preserve : ∀X,Y,P,F,m,n,e1,e2.
1831       opt_preserve X Y P F m n →
1832       res_preserve X Y P F (opt_to_res … e1 m) (opt_to_res … e2 n).
1833#X #Y #P #F #m #n #e1 #e2 #H #v #prf
1834cases (H … (opt_eq_from_res ???? prf)) #prf' #EQ %{prf'}
1835>EQ %
1836qed.
1837
1838lemma err_eq_from_io : ∀O,I,X,m,v.
1839  err_to_io O I X m = return v → m = return v.
1840#O #I #X * #x #v normalize #EQ destruct % qed.
1841
1842lemma res_to_io_preserve : ∀O,I,X,Y,P,F,m,n.
1843       res_preserve X Y P F m n →
1844       io_preserve O I X Y P F m n.
1845#O #I #X #Y #P #F #m #n #H #v #prf
1846cases (H … (err_eq_from_io ????? prf)) #prf' #EQ %{prf'}
1847>EQ %
1848qed.
1849*)
1850lemma eval_seq_no_pc_sigma_commute :
1851 ∀p,p',graph_prog.
1852 let lin_prog ≝ linearise p graph_prog in
1853 ∀stack_sizes.
1854 ∀sigma.∀gss : good_state_sigma p p' graph_prog sigma.
1855 ∀f,fn,stmt.
1856 preserving … res_preserve …
1857   (sigma_state … gss)
1858   (sigma_state … gss)
1859   (eval_seq_no_pc … (ev_genv … (graph_prog_params … graph_prog stack_sizes))
1860      f fn stmt)
1861   (eval_seq_no_pc … (ev_genv … (lin_prog_params … lin_prog stack_sizes))
1862      f (\fst (linearise_int_fun … fn)) stmt).
1863  #p #p' #graph_prog #stack_sizes #sigma #gss #f
1864  #fn #stmt
1865  whd in match eval_seq_no_pc;
1866  cases stmt normalize nodelta
1867  [1,2: (* COMMENT, COST_LABEL *) #_ @mfr_return
1868  | (* MOVE *) #mv_sig #st #prf'
1869    @mfr_bind [3: @pair_reg_move_commute |*:]
1870    #r #prf @mfr_return @wf_set_regs assumption
1871  | (* POP *)
1872    #a #st #prf
1873    @(mfr_bind … (combine_strong … (sigma_beval p p' graph_prog sigma) (sigma_state … gss)))
1874    [ @(mfr_bind … (sigma_is_pop_commute …)) * #bv #is' * #prf1' #prf2'
1875      @mfr_return %{prf1'} @wf_set_is assumption
1876    | * #bv #st' * #prf1' #prf2'
1877      @mfr_bind [3: @acca_store__commute |*:]
1878      #r #prf3' @mfr_return @wf_set_regs assumption
1879    ]
1880  | (* PUSH *)
1881     #a #st #prf
1882     @mfr_bind [3: @acca_arg_retrieve_commute |*:]
1883     #bv #prf_bv
1884     @mfr_bind [3: @is_push_sigma_commute |*:]
1885     #is #prf_is @mfr_return @wf_set_is assumption
1886  | (*C_ADDRESS*)
1887    #sy
1888    change with ((member ? ? ? (prog_var_names (joint_function (mk_graph_params p)) ℕ graph_prog)) → ?)
1889    #sy_prf
1890    change with ((dpl_reg p) → ?) #dpl 
1891    change with ((dph_reg p) → ?) #dph
1892    #st #prf
1893    @(mfr_bind … (sigma_state … gss))
1894    [ @(mfr_bind … (sigma_regs … gss))
1895      [2: #r #prf' @mfr_return @wf_set_regs assumption ]
1896    ]
1897    @opt_safe_elim #bl #EQbl
1898    @opt_safe_elim #bl'
1899    >(find_symbol_transf …
1900          (λvars.transf_fundef … (λfn.\fst (linearise_int_fun … fn))) graph_prog sy) in ⊢ (%→?);
1901    >EQbl in ⊢ (%→?); #EQ destruct(EQ)
1902    [ @dpl_store_commute
1903    | #st' #st_prf'
1904      @mfr_bind [3: @dph_store_commute |*:]
1905      [2: #r #prf' @mfr_return @wf_set_regs assumption
1906      ]
1907    ] @bv_no_pc_wf %
1908  | (*C_OPACCS*)
1909    #op #a #b #arg1 #arg2 #st #prf
1910    @mfr_bind [3: @acca_arg_retrieve_commute |*: ]
1911    #bv1 #bv1_prf
1912    @mfr_bind [3: @accb_arg_retrieve_commute |*: ]
1913    #bv2 #bv2_prf
1914    @mfr_bind [3: @beopaccs_sigma_commute |*: ]
1915    * #res1 #res2 * #res1_prf #res2_prf
1916    @(mfr_bind … (sigma_state … gss))
1917    [ @mfr_bind [3: @acca_store__commute |*: ]
1918      #r #r_prf @mfr_return @wf_set_regs assumption
1919    ]
1920    #st' #st_prf'
1921    @mfr_bind [3: @accb_store_commute |*: ]
1922    #r #r_prf @mfr_return @wf_set_regs assumption
1923  | (*C_OP1*)
1924    #op #a #arg #st #prf
1925    @mfr_bind [3: @acca_retrieve_commute |*: ]
1926    #bv #bv_prf
1927    @mfr_bind [3: @beop1_sigma_commute |*: ]
1928    #res #res_prf
1929    @mfr_bind [3: @acca_store__commute |*: ]
1930    #r #r_prf @mfr_return @wf_set_regs assumption
1931  | (*C_OP2*)
1932    #op #a #arg1 #arg2 #st #prf
1933    @mfr_bind [3: @acca_arg_retrieve_commute |*: ]
1934    #bv1 #bv1_prf
1935    @mfr_bind [3: @snd_arg_retrieve_commute |*: ]
1936    #bv2 #bv2_prf
1937    @mfr_bind [3: @beop2_sigma_commute |*: ]
1938    * #res1 #carry' #res1_prf
1939    @(mfr_bind … (sigma_state … gss))
1940    [ @mfr_bind [3: @acca_store__commute |*: ]
1941      #r #r_prf @mfr_return @wf_set_regs assumption
1942    ]
1943    #st' #st_prf' @mfr_return
1944  | (*C_CLEAR_CARRY*)
1945     #st #prf @mfr_return
1946  | (*C_SET_CARRY*)
1947    #st #prf @mfr_return
1948  | (*C_LOAD*)
1949    #a #dpl #dph #st #prf
1950    @mfr_bind [3: @dph_arg_retrieve_commute |*:]
1951    #bv1 #bv1_prf
1952    @mfr_bind [3: @dpl_arg_retrieve_commute |*:]
1953    #bv2 #bv2_prf
1954    @mfr_bind [3: @sigma_ptr_commute |*:]
1955    [ % assumption ]
1956    #ptr *
1957    @mfr_bind
1958    [3:
1959     @opt_to_res_preserve @beloadv_sigma_commute
1960   |*:]
1961   #res #res_prf
1962   @mfr_bind [3: @acca_store__commute |*: ]
1963   #r #r_prf @mfr_return @wf_set_regs assumption
1964 | (*C_STORE*)
1965    #dpl #dph #a #st #prf
1966    @mfr_bind [3: @dph_arg_retrieve_commute |*:]
1967    #bv1 #bv1_prf
1968    @mfr_bind [3: @dpl_arg_retrieve_commute |*:]
1969    #bv2 #bv2_prf
1970    @mfr_bind [3: @sigma_ptr_commute |*:]
1971    [ % assumption ]
1972    #ptr *
1973    @mfr_bind
1974    [3: @acca_arg_retrieve_commute |*:]
1975    #res #res_prf
1976    @mfr_bind
1977    [3:
1978     @opt_to_res_preserve @bestorev_sigma_commute
1979    |*:]
1980    #mem #wf_mem
1981    @mfr_return
1982    @wf_set_m assumption
1983 | (*CALL*)
1984     #f #args #dest #st #prf @mfr_return
1985 |  (*C_EXT*)
1986    #s_ext #st #prf @eval_ext_seq_commute
1987 ]
1988 qed.
1989
1990lemma eval_seq_no_call_ok :
1991 ∀p,p',graph_prog.
1992 let lin_prog ≝ linearise p graph_prog in
1993 ∀stack_sizes.
1994 ∀sigma.good_sigma p graph_prog sigma →
1995 ∀gss : good_state_sigma p p' graph_prog sigma.
1996 ∀st,st',f,fn,stmt,nxt.no_call ?? stmt →
1997 ∀prf : well_formed_state_pc … gss st.
1998   fetch_statement (mk_sem_graph_params p p') …
1999    (globalenv_noinit ? graph_prog) (pc … st) =
2000      return 〈f, fn,  sequential … (step_seq (mk_graph_params p) … stmt) nxt〉 →
2001   eval_state … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) st =
2002    return st' →
2003 ∃prf'.
2004 ∃taf : trace_any_any_free (lin_abstract_status p p' lin_prog stack_sizes)
2005  (sigma_state_pc … gss st prf)
2006  (sigma_state_pc … gss st' prf').
2007 bool_to_Prop (taaf_non_empty … taf).
2008#p #p' #graph_prog #stack_sizes #sigma #good #gss #st #st' #f #fn #stmt #nxt #stmt_no_call
2009#prf #EQfetch
2010whd in match eval_state; normalize nodelta >EQfetch
2011>m_return_bind whd in match eval_statement_no_pc;
2012whd in match eval_statement_advance; normalize nodelta
2013@'bind_inversion #st_no_pc' #EQeval
2014>no_call_advance [2: assumption]
2015whd in ⊢ (??%%→?); #EQ destruct(EQ)
2016cases (fetch_statement_sigma_commute … good … (proj2 … (proj1 … prf)) … EQfetch)
2017normalize nodelta #_ * #EQfetch' *
2018#prf_nxt #nxt_spec
2019lapply (err_eq_from_io ????? EQeval) -EQeval #EQeval
2020cases (eval_seq_no_pc_sigma_commute … gss … (proj2 … prf) … EQeval)
2021#st_no_pc_prf
2022#EQeval'
2023%{(hide_prf …)} [ %{st_no_pc_prf} %{prf_nxt} cases st in prf; -st #st #pc #popped ** // ]
2024cases nxt_spec -nxt_spec
2025[ #nxt_spec %{(taaf_step … (taa_base …) …) I}
2026| * #nxt_spec #pc_of_label_spec %{(taaf_step … (taa_step … (taa_base …))…) I}
2027]
2028[1,6:
2029  whd whd in ⊢ (??%?); >EQfetch' normalize nodelta
2030  whd in match joint_classify_step; normalize nodelta
2031  >no_call_other try % assumption
2032|2,5:
2033  whd whd in match eval_state; normalize nodelta
2034  change with (sigma_pc ??????) in match (pc ??);
2035  try >EQfetch' in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
2036  whd in match eval_statement_no_pc; normalize nodelta
2037  try >EQeval' in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
2038  whd in match eval_statement_advance; normalize nodelta
2039  >no_call_advance try assumption
2040  whd in match (next ???) in ⊢ (??%?);
2041  [ >nxt_spec %
2042  | %
2043  ]
2044|3:
2045  whd whd in ⊢ (??%?); >nxt_spec normalize nodelta %
2046|4:
2047  whd whd in match eval_state; normalize nodelta
2048  >nxt_spec >m_return_bind >m_return_bind
2049  whd in match eval_statement_advance; normalize nodelta
2050  whd in match goto; normalize nodelta
2051  whd in match (pc_block ?); >pc_block_sigma_commute
2052  >pc_of_label_spec %
2053|7: %* #H @H -H
2054  whd in ⊢ (??%?); >nxt_spec %
2055|8:
2056]
2057qed.
2058
2059lemma block_of_call_sigma_commute :
2060∀p,p',graph_prog,sigma.
2061∀gss : good_state_sigma p p' graph_prog sigma.∀cl.
2062 preserving … res_preserve …
2063   (sigma_state p p' graph_prog sigma gss)
2064   (λx.λ_ : True .x)
2065   (block_of_call (mk_sem_graph_params p p') …
2066      (globalenv_noinit ? graph_prog) cl)   
2067   (block_of_call (mk_sem_lin_params p p') …
2068      (globalenv_noinit ? (linearise ? graph_prog)) cl).
2069#p #p' #graph_prog #sigma #gss #cl #st #prf
2070@mfr_bind
2071[3: cases cl
2072  [ #id normalize nodelta @opt_to_res_preserve
2073    >(find_symbol_transf …
2074          (λvars.transf_fundef … (λfn.\fst (linearise_int_fun … fn))) graph_prog id)
2075   #s #EQs %{I} >EQs in ⊢ (??%?); %
2076  | * #dpl #dph normalize nodelta
2077    @mfr_bind [3: @dpl_arg_retrieve_commute |*:]
2078    #bv1 #bv1_prf
2079    @mfr_bind [3: @dph_arg_retrieve_commute |*:]
2080    #bv2 #bv2_prf
2081    @(mfr_bind … (λptr.λ_:True.ptr))
2082    [ change with (pointer_of_address 〈?,?〉) in
2083      match (pointer_of_bevals ?);
2084      change with (pointer_of_address 〈?,?〉) in
2085      match (pointer_of_bevals [sigma_beval ??????;?]);
2086      @sigma_ptr_commute % assumption
2087    ] #ptr *
2088    @if_elim #_ [ @mfr_return | @res_preserve_error ] %
2089 ]
2090|4: #bl * @opt_to_res_preserve #x #EQ %{I} @EQ
2091|*:
2092]
2093qed.
2094
2095lemma fetch_function_no_minus_one :
2096  ∀F,V,i,p,bl.
2097  block_id (pi1 … bl) = -1 →
2098  fetch_function … (globalenv (λvars.fundef (F vars)) V i p)
2099    bl = Error … [MSG BadFunction].
2100 #F#V#i#p ** #r #id #EQ1 #EQ2 destruct
2101  whd in match fetch_function; normalize nodelta
2102  >globalenv_no_minus_one
2103  cases (symbol_for_block ???) normalize //
2104qed.
2105
2106lemma entry_sigma_commute:
2107∀ p,p',graph_prog,sigma.good_sigma p graph_prog sigma →
2108∀bl,f1,fn1.
2109(fetch_function ? (globalenv_noinit … graph_prog) bl =
2110return 〈f1,Internal ? fn1〉) →
2111∃prf.
2112sigma_pc p p' graph_prog sigma
2113   (pc_of_point (mk_sem_graph_params p p') bl (joint_if_entry ?? fn1)) prf =
2114      pc_of_point (mk_sem_lin_params p p') bl 0.
2115#p #p' #graph_prog #sigma #good #bl #f1 #fn1 #fn1_spec
2116cases (good fn1) * #entry_in #_ #_
2117       % [ @hide_prf % | whd in match sigma_pc; normalize nodelta @opt_safe_elim #pc ]
2118       whd in match sigma_pc_opt; normalize nodelta
2119       >eqZb_false whd in match (pc_block ?);
2120       [2,4: % #EQbl
2121        >(fetch_function_no_minus_one … graph_prog … EQbl) in fn1_spec;
2122        whd in ⊢ (???%→?); #ABS destruct(ABS) ]
2123       normalize nodelta whd in match fetch_internal_function;
2124       normalize nodelta >fn1_spec >m_return_bind >point_of_pc_of_point
2125       >entry_in whd in ⊢ (??%%→?); #EQ destruct(EQ) %
2126qed.
2127
2128lemma eval_call_ok :
2129 ∀p,p',graph_prog.
2130 let lin_prog ≝ linearise p graph_prog in
2131 ∀stack_sizes.
2132 ∀sigma. good_sigma p graph_prog sigma →
2133 ∀gss : good_state_sigma p p' graph_prog sigma.
2134 ∀st,st',f,fn,called,args,dest,nxt.
2135 ∀prf : well_formed_state_pc … gss st.
2136  fetch_statement (mk_sem_graph_params p p') …
2137    (globalenv_noinit ? graph_prog) (pc … st) =
2138      return 〈f, fn,
2139        sequential … (CALL (mk_graph_params p) … called args dest ) nxt〉 →
2140   eval_state … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) st =
2141    return st' →
2142(* let st_pc' ≝ mk_state_pc ? st'
2143  (succ_pc (mk_sem_graph_params p p') …
2144    (pc … st) nxt) in
2145 ∀prf'.
2146 fetch_statement (mk_sem_lin_params p p') …
2147   (globalenv_noinit … lin_prog)
2148     (succ_pc (mk_sem_lin_params p p') (sigma_pc … (pc … st) (proj1 … prf)) it) =
2149   return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉 →
2150 pc_of_label (mk_sem_lin_params p p') ?
2151                (globalenv_noinit ? (linearise p … graph_prog))
2152                (pc_block (pc … st))
2153                nxt = return sigma_pc p p' graph_prog sigma
2154    (succ_pc (mk_sem_graph_params p p') (pc … st) nxt) prf' →*)
2155  let st2_pre_call ≝ sigma_state_pc … gss st prf in
2156  ∃is_call, is_call'.
2157  ∃prf'.
2158  let st2_after_call ≝ sigma_state_pc … gss st' prf' in
2159  joint_call_ident (lin_prog_params … (linearise … graph_prog) stack_sizes) «st2_pre_call, is_call'» =
2160  joint_call_ident (graph_prog_params … graph_prog stack_sizes) «st, is_call» ∧
2161  eval_state … (ev_genv … (lin_prog_params … (linearise … graph_prog) stack_sizes))
2162    st2_pre_call = return st2_after_call.
2163#p #p' #graph_prog #stack_sizes #sigma #good #gss #st #st1 #f #fn
2164#called #args #dest #nxt #prf #fetch_spec
2165cases(fetch_statement_sigma_commute … good (proj2 … (proj1 … prf)) … fetch_spec) #_
2166normalize nodelta * #lin_fetch_spec #_
2167whd in match eval_state in ⊢ (%→?); normalize nodelta >fetch_spec
2168>m_return_bind >m_return_bind whd in match eval_statement_advance;
2169whd in match eval_seq_advance; whd in match eval_seq_call; normalize nodelta
2170@('bind_inversion) #bl #H lapply (err_eq_from_io ????? H) -H #bl_spec
2171@('bind_inversion) * #id #int_f #H lapply (err_eq_from_io ????? H) -H
2172cases int_f -int_f [ #fn | #ext_f] #int_f_spec normalize nodelta
2173[2:#H @('bind_inversion H) -H #st' #H #_ @('bind_inversion H) -H #vals #_
2174  @'bind_inversion #vals' #_ whd in ⊢ (??%%→?); #ABS destruct(ABS) ]
2175#H lapply (err_eq_from_io ????? H) -H
2176#H @('bind_inversion H) -H #st_no_pc #save_frame_spec
2177>m_bind_bind
2178#H @('bind_inversion H) -H #stack_size #H lapply (opt_eq_from_res ???? H) -H
2179whd in match (stack_sizes ?);
2180#stack_size_spec
2181>m_bind_bind
2182#H @('bind_inversion H) -H #st_no_pc' #set_call_spec
2183>m_return_bind whd in ⊢ (??%%→?);
2184whd in match set_no_pc; normalize nodelta #EQ destruct(EQ)
2185%
2186[  @hide_prf
2187  whd in match joint_classify; normalize nodelta >fetch_spec >m_return_bind
2188  normalize nodelta whd in match joint_classify_step;
2189  whd in match joint_classify_seq; normalize nodelta
2190  >bl_spec >m_return_bind >int_f_spec normalize nodelta %
2191| cases(block_of_call_sigma_commute p p' graph_prog sigma gss ?? (proj2 … prf) ?
2192            bl_spec)
2193  * #lin_bl_spec
2194  generalize in match (fetch_function_transf … graph_prog …
2195      (λvars.transf_fundef … (λf_in.\fst(linearise_int_fun ?? f_in)))
2196      … int_f_spec : fetch_function … (globalenv_noinit … (linearise … graph_prog)) bl = ?) in ⊢ ?;
2197  #lin_int_f_spec
2198  %
2199  [ @hide_prf whd in match joint_classify; normalize nodelta >lin_fetch_spec
2200    >m_return_bind normalize nodelta whd in match joint_classify_step;
2201    whd in match joint_classify_seq; normalize nodelta
2202    >lin_bl_spec >m_return_bind
2203    >lin_int_f_spec %
2204   | cases (save_frame_commute … gss … save_frame_spec) in ⊢ ?;
2205    [2: @hide_prf cases st in prf; // ]
2206    #st_no_pc_wf #lin_save_frame_spec
2207     cases (setup_call_commute … gss … st_no_pc_wf … set_call_spec) in ⊢ ?;
2208     #st_no_pc_wf' #lin_set_call_spec
2209     cases (allocate_locals_commute … gss … (joint_if_locals … fn) … st_no_pc_wf')
2210     #st_no_pc_wf'' #lin_allocate_locals_spec
2211     cases(entry_sigma_commute p p' graph_prog sigma good … int_f_spec)
2212     #entry_prf #entry_spec
2213      % [ @hide_prf %{st_no_pc_wf''} %{entry_prf} @(proj1 … (proj1 … prf)) ]
2214      % [ whd in match joint_call_ident; normalize nodelta
2215          >lin_fetch_spec in ⊢ (??match % with [ _ ⇒ ? | _ ⇒ ?]?);
2216          >fetch_spec in ⊢ (???match % with [ _ ⇒ ? | _ ⇒ ?]);
2217          normalize nodelta
2218          >lin_bl_spec >bl_spec >m_return_bind >m_return_bind
2219          whd in match fetch_internal_function; normalize nodelta
2220          >lin_int_f_spec >int_f_spec %
2221        | whd in match eval_state; normalize nodelta
2222          >lin_fetch_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
2223           whd in match eval_statement_no_pc; normalize nodelta
2224           whd in match eval_seq_no_pc; normalize nodelta
2225           >m_return_bind in ⊢ (??%?);
2226           whd in match eval_statement_advance; whd in match eval_seq_advance;
2227           whd in match eval_seq_call; normalize nodelta
2228           >lin_bl_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
2229           >lin_int_f_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
2230           normalize nodelta
2231           >lin_save_frame_spec >m_return_bind
2232           >m_bind_bind whd in match (stack_sizes ?);
2233           >stack_size_spec >m_return_bind
2234           >lin_set_call_spec >m_return_bind
2235           >lin_allocate_locals_spec
2236           <entry_spec %
2237         ]
2238       ]
2239     ]
2240qed.         
2241               
2242lemma eval_goto_ok :
2243 ∀p,p',graph_prog.
2244 let lin_prog ≝ linearise p graph_prog in
2245 ∀stack_sizes.
2246 ∀sigma.good_sigma p graph_prog sigma →
2247 ∀gss : good_state_sigma p p' graph_prog sigma.
2248 ∀st,st',f,fn,nxt.
2249 ∀prf : well_formed_state_pc … gss st.
2250   fetch_statement (mk_sem_graph_params p p') …
2251    (globalenv_noinit ? graph_prog) (pc … st) =
2252      return 〈f, fn,  final … (GOTO (mk_graph_params p) … nxt)〉 →
2253   eval_state … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) st =
2254    return st' →
2255 ∃prf'.
2256 ∃taf : trace_any_any_free (lin_abstract_status p p' lin_prog stack_sizes)
2257  (sigma_state_pc … gss st prf)
2258  (sigma_state_pc … gss st' prf').
2259 bool_to_Prop (taaf_non_empty … taf).
2260#p #p' #graph_prog #stack_sizes #sigma #good #gss #st #st' #f #fn
2261#nxt #prf #EQfetch
2262whd in match eval_state; normalize nodelta >EQfetch
2263>m_return_bind >m_return_bind
2264whd in match eval_statement_advance; normalize nodelta
2265whd in match goto; normalize nodelta
2266#H lapply (err_eq_from_io ????? H) -H
2267#H @('bind_inversion H) #pc'
2268@('bind_inversion EQfetch) * #curr_i #curr_fn #EQfetchfn
2269#H @('bind_inversion H) -H #stmt' #_ whd in ⊢ (??%%→?);
2270#EQ destruct(EQ)
2271>(graph_pc_of_label … EQfetchfn) whd in ⊢ (??%%→??%%→?);
2272#EQ1 #EQ2 destruct
2273cases (fetch_statement_sigma_commute … good … (proj2 … (proj1 … prf)) … EQfetch)
2274normalize nodelta ** #prf' #EQpc_of_label' *
2275#EQfetch'
2276-H
2277%
2278[ @hide_prf cases st in prf prf'; -st #st #pc #popped ** #H1 #H2 #H3
2279  #H4 %{H3} %{H1 H4} ]
2280%{(taaf_step … (taa_base …) …) I}
2281[ whd whd in ⊢ (??%?); >EQfetch' %
2282| whd whd in match eval_state; normalize nodelta
2283  >EQfetch' >m_return_bind >m_return_bind
2284  whd in match eval_statement_advance; whd in match goto;
2285  normalize nodelta >pc_block_sigma_commute >EQpc_of_label'
2286  >m_return_bind %
2287]
2288qed.
2289
2290lemma eval_cond_ok :
2291∀p,p',graph_prog.
2292let lin_prog ≝ linearise p graph_prog in
2293∀stack_sizes.
2294∀sigma.good_sigma p graph_prog sigma →
2295∀gss : good_state_sigma p p' graph_prog sigma.
2296∀st,st',f,fn,a,ltrue,lfalse.
2297∀prf : well_formed_state_pc … gss st.
2298 fetch_statement (mk_sem_graph_params p p') …
2299  (globalenv_noinit ? graph_prog) (pc … st) =
2300    return 〈f, fn,  sequential … (COND (mk_graph_params p) … a ltrue) lfalse〉 →
2301 eval_state … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) st =
2302  return st' →
2303as_costed (joint_abstract_status (graph_prog_params p p' graph_prog stack_sizes))
2304  st' →
2305∃prf'.
2306∃taf : trace_any_any_free (lin_abstract_status p p' lin_prog stack_sizes)
2307(sigma_state_pc … gss st prf)
2308(sigma_state_pc … gss st' prf').
2309bool_to_Prop (taaf_non_empty … taf).
2310#p #p' #graph_prog #stack_sizes #sigma #good #gss #st #st' #f #fn
2311#a #ltrue #lfalse #prf #EQfetch
2312whd in match eval_state; normalize nodelta >EQfetch
2313>m_return_bind >m_return_bind
2314whd in match eval_statement_advance; normalize nodelta
2315#H @('bind_inversion (err_eq_from_io ????? H))
2316@bv_pc_other [ #pc' #p #_ whd in ⊢ (??%%→?); #ABS destruct(ABS) ]
2317#bv #bv_no_pc #EQretrieve
2318cut
2319  (∃prf'.acca_retrieve ?? (p' ?) (sigma_state_pc p p' graph_prog sigma gss st prf) a =
2320    return sigma_beval p p' graph_prog sigma bv prf')
2321[ @acca_retrieve_commute assumption ]
2322* #bv_prf >(sigma_bv_no_pc … bv_no_pc) #EQretrieve'
2323-H #H @('bind_inversion H) *
2324#EQbool normalize nodelta -H
2325[ whd in match goto; normalize nodelta
2326  #H @('bind_inversion H) -H #pc'
2327  @('bind_inversion EQfetch) * #curr_i #curr_fn #EQfetchfn
2328  #H @('bind_inversion H) -H #stmt' #_ whd in ⊢ (??%%→?);
2329  #EQ destruct(EQ)
2330  >(graph_pc_of_label … EQfetchfn) whd in ⊢ (??%%→??%%→?);
2331  #EQ1 #EQ2 destruct
2332| whd in ⊢ (??%%→?);
2333  #EQ destruct(EQ)
2334]
2335#ncost
2336cases (fetch_statement_sigma_commute … good … (proj2 … (proj1 … prf)) … EQfetch)
2337normalize nodelta ** #prf' #EQpc_of_label' ** #prf'' **
2338#EQfetch' #nxt_spec
2339% [1,3,5,7: @hide_prf
2340  cases st in prf prf' prf'';
2341  -st #st #pc #popped ** #H1 #H2 #H3 #H4 #H5
2342  %{H3} %{H1} assumption ]
2343%{(taaf_step_jump … (taa_base …) …) I}
2344[1,4,7,10: whd
2345  >(as_label_sigma_commute … good) assumption
2346|2,5,8,11: whd whd in ⊢ (??%?);
2347  >EQfetch' %
2348|*: whd whd in match eval_state; normalize nodelta >EQfetch'
2349  >m_return_bind >m_return_bind
2350  whd in match eval_statement_advance; normalize nodelta >EQretrieve'
2351  >m_return_bind >EQbool >m_return_bind normalize nodelta
2352  [1,2: whd in match goto; normalize nodelta
2353    >pc_block_sigma_commute >EQpc_of_label' %
2354  |3: whd in match next; normalize nodelta >nxt_spec %
2355  |4: whd in match goto; normalize nodelta
2356    >pc_block_sigma_commute >nxt_spec %
2357  ]
2358]
2359qed.
2360
2361lemma eval_return_ok :
2362∀p,p',graph_prog.
2363let lin_prog ≝ linearise p graph_prog in
2364∀stack_sizes.
2365∀sigma.∀good : good_sigma p graph_prog sigma.
2366∀gss : good_state_sigma p p' graph_prog sigma.
2367∀st,st',f,fn.
2368∀prf : well_formed_state_pc … gss st.
2369 fetch_statement (mk_sem_graph_params p p') …
2370  (globalenv_noinit ? graph_prog) (pc … st) =
2371    return 〈f, fn,  final … (RETURN (mk_graph_params p) … )〉 →
2372 eval_state … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) st =
2373  return st' →
2374joint_classify (lin_prog_params … (linearise … graph_prog) stack_sizes)
2375  (sigma_state_pc … st prf) = Some ? cl_return ∧
2376∃prf'.
2377∃st2_after_ret.
2378∃taf : trace_any_any_free (lin_abstract_status p p' lin_prog stack_sizes)
2379st2_after_ret
2380(sigma_state_pc … gss st' prf').
2381(if taaf_non_empty … taf then
2382  ¬as_costed (joint_abstract_status (lin_prog_params p p' (linearise … graph_prog) stack_sizes))
2383    st2_after_ret
2384 else True) ∧
2385eval_state … (ev_genv …  (lin_prog_params … (linearise … graph_prog) stack_sizes))
2386  (sigma_state_pc … st prf) =
2387return st2_after_ret ∧
2388ret_rel … (linearise_status_rel … gss good) st' st2_after_ret.
2389#p #p' #graph_prog #stack_sizes #sigma #good #gss #st #st' #f #fn
2390#prf #EQfetch
2391whd in match eval_state; normalize nodelta >EQfetch
2392>m_return_bind >m_return_bind
2393whd in match eval_statement_advance; normalize nodelta
2394#H lapply (err_eq_from_io ????? H) -H
2395#H @('bind_inversion H) -H #st1' #EQpop
2396cut (∃prf'.
2397  (pop_frame … (ev_genv (lin_prog_params ? p' (linearise ? graph_prog) stack_sizes))
2398    f (\fst (pi1 ?? (linearise_int_fun ?? fn))) (sigma_state … gss st (proj2 … prf)))
2399   = return sigma_state_pc … gss st1' prf')
2400[ @pop_frame_commute assumption ]
2401* #prf' #EQpop' >m_bind_bind
2402#H @('bind_inversion H) ** #call_i #call_fn
2403* [ * [ #s | #a #lbl ] #nxt | #s | * ] normalize nodelta
2404#EQfetch_ret -H
2405whd in ⊢ (??%%→?); #EQ destruct(EQ) whd in match (next ???); >graph_succ_pc
2406cases (fetch_statement_sigma_commute … good … (proj2 … (proj1 … prf)) … EQfetch)
2407#_ normalize nodelta #EQfetch'
2408cases (fetch_statement_sigma_commute … good … (proj2 … (proj1 … prf')) … EQfetch_ret)
2409normalize nodelta
2410#all_labels_in
2411* #EQfetch_ret' * #prf'' * [2: * ] #nxt_spec [2:| #EQpc_of_label']
2412% [1,3: whd in match joint_classify; normalize nodelta
2413  >EQfetch' >m_return_bind % ]
2414% [1,3: @hide_prf cases prf' * #_ #H1 #H2 %{H2} %{H1 prf''} ]
2415[ % [2: %{(taaf_base …)} |]
2416  % [ %{I} ]
2417  [ >EQfetch' >m_return_bind >m_return_bind normalize nodelta
2418    whd in match eval_return; normalize nodelta
2419    >EQpop' >m_return_bind
2420    whd in match next_of_pc; normalize nodelta
2421    >EQfetch_ret' >m_return_bind whd in match next; normalize nodelta
2422    >nxt_spec %
2423  | * #s1_pre #s1_call
2424    cases (joint_classify_call … s1_call)
2425    * #calling_i #calling * #call_spec * #arg * #dest * #nxt * #bl
2426    * #called_i * #called ** #EQfetch_call #EQbl #EQfetch_called
2427    * #s2_pre #s2_call
2428    whd in ⊢ (%→?); >EQfetch_call * #EQ #_
2429    * #s1_pre_prf #EQpc_s2_pre
2430    whd >EQpc_s2_pre
2431    <(sigma_pc_irr … EQ) [2: @hide_prf @(proj2 … (proj1 … prf')) ]
2432    >EQfetch_ret' % [ % | >nxt_spec % ]
2433  ]
2434| % [2: %{(taaf_step … (taa_base …) …)} |*:]
2435  [3: % [ % normalize nodelta ]
2436    [2: >EQfetch' in ⊢ (??%?);
2437      >m_return_bind in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
2438      normalize nodelta
2439      whd in match eval_return; normalize nodelta
2440      >EQpop' in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
2441      whd in match next_of_pc; normalize nodelta
2442      >EQfetch_ret' in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
2443      whd in match next; normalize nodelta %
2444    |1: normalize nodelta %* #H @H -H
2445      whd in ⊢ (??%?); >nxt_spec %
2446    |3: * #s1_pre #s1_call
2447      cases (joint_classify_call … s1_call)
2448      * #calling_i #calling * #call_spec * #arg * #dest * #nxt' * #bl
2449      * #called_i * #called ** #EQfetch_call #EQbl #EQfetch_called
2450      * #s2_pre #s2_call
2451      whd in ⊢ (%→?); >EQfetch_call * #EQ #_
2452      * #s1_pre_prf #EQpc_s2_pre
2453      whd >EQpc_s2_pre
2454      <(sigma_pc_irr … EQ) [2: @hide_prf @(proj2 … (proj1 … prf')) ]
2455      >EQfetch_ret' %%
2456    ]
2457  |1: whd whd in ⊢ (??%?); >nxt_spec %
2458  |2: whd whd in match eval_state; normalize nodelta
2459    >nxt_spec >m_return_bind >m_return_bind
2460    whd in match eval_statement_advance; whd in match goto; normalize nodelta
2461    whd in match (pc_block ?); >pc_block_sigma_commute
2462    >EQpc_of_label' >m_return_bind % whd in match (set_pc ???); %
2463  |*:
2464  ]
2465]
2466qed.
2467
2468 
2469lemma eval_tailcall_ok :
2470∀p,p',graph_prog.
2471let lin_prog ≝ linearise p graph_prog in
2472∀stack_sizes.
2473∀sigma.good_sigma p graph_prog sigma →
2474∀gss : good_state_sigma p p' graph_prog sigma.
2475∀st,st',f,fn,fl,called,args.
2476∀prf : well_formed_state_pc … gss st.
2477 fetch_statement (mk_sem_graph_params p p') …
2478  (globalenv_noinit ? graph_prog) (pc … st) =
2479    return 〈f, fn,  final … (TAILCALL (mk_graph_params p) … fl called args)〉 →
2480 eval_state … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) st =
2481  return st' →
2482  let st2_pre_call ≝ sigma_state_pc … gss st prf in
2483  ∃is_tailcall, is_tailcall'.
2484  ∃prf'.
2485  let st2_after_call ≝ sigma_state_pc … gss st' prf' in
2486  joint_tailcall_ident (lin_prog_params … (linearise … graph_prog) stack_sizes) «st2_pre_call, is_tailcall'» =
2487  joint_tailcall_ident (graph_prog_params … graph_prog stack_sizes) «st, is_tailcall» ∧
2488  eval_state … (ev_genv … (lin_prog_params … (linearise … graph_prog) stack_sizes))
2489    st2_pre_call = return st2_after_call.
2490#p #p' #graph_prog #stack_sizes #sigma #good #gss #st #st' #f #fn #fl #called #args
2491#prf #fetch_spec
2492cases(fetch_statement_sigma_commute … good (proj2 … (proj1 … prf)) … fetch_spec) *
2493normalize nodelta #lin_fetch_spec
2494whd in match eval_state; normalize nodelta >fetch_spec
2495>m_return_bind whd in match eval_statement_no_pc; normalize nodelta
2496>m_return_bind whd in match eval_statement_advance; whd in match eval_tailcall;
2497normalize nodelta @('bind_inversion) #bl #bl_spec
2498lapply (err_eq_from_io ????? bl_spec) -bl_spec
2499whd in match set_no_pc; normalize nodelta #bl_spec
2500cases(block_of_call_sigma_commute p p' graph_prog sigma gss ?? (proj2 … prf) ?
2501            bl_spec) * #lin_bl_spec @('bind_inversion)
2502* #f1 #fn1 cases fn1 normalize nodelta -fn1
2503[2: #ext_f #_ whd in match eval_external_call; normalize nodelta @('bind_inversion)
2504    #st @('bind_inversion) #list_val #_ @('bind_inversion) #le #_
2505    whd in ⊢ (??%% → ?); #ABS destruct(ABS)]
2506#fn1 #fn1_spec lapply(err_eq_from_io ????? fn1_spec) -fn1_spec #fn1_spec
2507generalize in match (fetch_function_transf … graph_prog …
2508      (λvars.transf_fundef … (λf_in.\fst(linearise_int_fun ?? f_in)))
2509      … fn1_spec : fetch_function … (globalenv_noinit … (linearise … graph_prog)) bl = ?) in ⊢ ?;
2510      #lin_fn1_spec
2511whd in match eval_internal_call; normalize nodelta
2512#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
2513#st1 #H @('bind_inversion H) -H #dim_s #dim_s_spec
2514#H @('bind_inversion H) -H #st2 #st2_spec whd in ⊢ (??%% → ??%% → ?);
2515#EQ1 #EQ2 destruct %
2516[ @hide_prf | % [@hide_prf]]
2517[1,2: whd in match joint_classify; normalize nodelta [>fetch_spec | >lin_fetch_spec]
2518      >m_return_bind normalize nodelta whd in match joint_classify_final;
2519      normalize nodelta [>bl_spec|>lin_bl_spec] >m_return_bind
2520      [>fn1_spec|>lin_fn1_spec] %
2521| cases (setup_call_commute … gss … (proj2 … prf) … st2_spec) #wf_st2 #lin_st2_spec
2522  cases (allocate_locals_commute … gss … (joint_if_locals … fn1) ? wf_st2)
2523  #wf_all_st2 #all_st2_spec
2524  cases(entry_sigma_commute p p' graph_prog sigma good … fn1_spec) #wf_pc
2525  #pc_spec
2526  %
2527  [ @hide_prf %
2528    [ % [@(proj1 … (proj1 … prf)) | @(wf_pc)]
2529    | @(wf_all_st2)
2530    ]
2531  | %
2532    [ whd in match joint_tailcall_ident; normalize nodelta
2533      >lin_fetch_spec in ⊢ (??match % with [ _ ⇒ ? | _ ⇒ ?]?);
2534      >fetch_spec in ⊢ (???match % with [ _ ⇒ ? | _ ⇒ ?]);
2535      normalize nodelta >lin_bl_spec >bl_spec >m_return_bind >m_return_bind
2536      whd in match fetch_internal_function; normalize nodelta
2537      >fn1_spec >lin_fn1_spec %
2538    | >lin_fetch_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
2539      normalize nodelta >m_return_bind in ⊢ (??%?);
2540      >lin_bl_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
2541      >lin_fn1_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
2542      normalize nodelta >dim_s_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
2543      >lin_st2_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
2544      >all_st2_spec in ⊢ (??%?); whd in ⊢ (??%%); @eq_f @eq_f2 [2: %]
2545      >pc_spec %
2546    ]
2547  ]
2548]
2549qed.
2550   
2551
2552lemma linearise_ok:
2553 ∀p,p',graph_prog.
2554  let lin_prog ≝ linearise ? graph_prog in
2555 ∀stack_sizes.
2556 (∀sigma.good_state_sigma p p' graph_prog sigma) →
2557   ∃[1] R.
2558   status_simulation
2559    (graph_abstract_status p p' graph_prog stack_sizes)
2560    (lin_abstract_status p p' lin_prog stack_sizes) R).
2561 #p #p' #graph_prog
2562 letin sigma ≝ (λfn.\snd (linearise_int_fun … fn) : sigma_map … graph_prog)
2563 cut (∀fn.good_local_sigma … (sigma fn))
2564  [6: #fn @(pi2 … (linearise_int_fun … fn)) |*:]
2565 #good
2566 #stack_sizes
2567 #gss lapply (gss sigma) -gss #gss
2568 %{(linearise_status_rel p p' graph_prog stack_sizes sigma gss good)}
2569whd in match graph_abstract_status;
2570whd in match lin_abstract_status;
2571whd in match graph_prog_params;
2572whd in match lin_prog_params;
2573normalize nodelta
2574whd
2575whd in ⊢ (%→%→%→?);
2576whd in ⊢ (?(?%)→?(?%)→?(?%)→?);
2577whd in ⊢ (?%→?%→?%→?);
2578#st1 #st1' #st2
2579whd in ⊢ (%→?);
2580change with
2581  (eval_state (mk_sem_graph_params p p') (prog_var_names ???) ?? = ? → ?)
2582#EQeval
2583@('bind_inversion EQeval)
2584** #curr_f #curr_fn #stmt #H lapply (err_eq_from_io ????? H) -H #EQfetch
2585#_ * #prf #EQst2
2586cases stmt in EQfetch; -stmt
2587[ @cond_call_other
2588  [ #a #ltrue | #f #args #dest | #s #s_no_call ] #nxt | #s | * ]
2589normalize nodelta
2590#EQfetch
2591change with (joint_classify ??) in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
2592[ (* COND *)
2593  whd in match joint_classify; normalize nodelta;
2594  >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
2595  normalize nodelta
2596  #ncost
2597  cases (eval_cond_ok … good … prf EQfetch EQeval ncost)
2598  #prf' * #taf #taf_ne
2599  destruct(EQst2)
2600  % [2: %{taf} |*:]
2601  >taf_ne normalize nodelta
2602  % [ %{I} %{prf'} % ]
2603  whd >(as_label_sigma_commute … good) %
2604|  (* CALL *)
2605  cases (eval_call_ok … good … prf EQfetch EQeval)
2606  #is_call * #is_call' *
2607  #prf' * #eq_call #EQeval'
2608  destruct(EQst2)
2609  >is_call in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
2610  #ignore %{«?, is_call'»}
2611  % [ %{eq_call} %{prf} % ]
2612  % [2: % [2: %{(taa_base …)} %{(taa_base …)} % [ %{EQeval'} %{prf'} % ]] |*:]
2613  whd >(as_label_sigma_commute … good) %
2614| (* SEQ *)
2615  whd in match joint_classify; normalize nodelta;
2616  >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
2617  normalize nodelta
2618  whd in match joint_classify_step; normalize nodelta
2619  >no_call_other [2: assumption ] normalize nodelta
2620  cases (eval_seq_no_call_ok … good … prf EQfetch EQeval) [2: assumption ]
2621  #prf' * #taf #taf_ne
2622  destruct(EQst2)
2623  % [2: %{taf} |*:]
2624  >taf_ne normalize nodelta % [ %{I} ]
2625  [ %{prf'} % | whd >(as_label_sigma_commute … good) % ]
2626| (* FIN *) cases s in EQfetch;
2627  [ (* GOTO *) #lbl #EQfetch
2628    whd in match joint_classify; normalize nodelta;
2629    >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
2630    normalize nodelta
2631    cases (eval_goto_ok … good … prf EQfetch EQeval)
2632    #prf' * #taf #taf_ne
2633    destruct(EQst2)
2634    % [2: %{taf} |*:]
2635    >taf_ne normalize nodelta % [ %{I} ]
2636    [ %{prf'} % | whd >(as_label_sigma_commute … good) % ]
2637  | (* RETURN *) #EQfetch
2638    whd in match joint_classify; normalize nodelta;
2639    >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
2640    normalize nodelta
2641    cases (eval_return_ok … good … prf EQfetch EQeval)
2642    #is_ret' *
2643    #prf' * #after_ret * #taf ** #taf_prf #EQeval' #ret_prf
2644    destruct(EQst2)
2645    % [2: % [2: % [2: %{(taa_base …)} %{taf} ]] |*:]
2646    % [2: whd >(as_label_sigma_commute … good) % ]
2647    %{ret_prf}
2648    % [2: %{prf'} % ]
2649    %{EQeval'}
2650    %{taf_prf is_ret'}
2651  | (* TAILCALL *) #fl #called #args #EQfetch
2652    cases (eval_tailcall_ok … good … prf EQfetch EQeval)
2653    #is_tailcall * #is_tailcall' *
2654    #prf' * #eq_call #EQeval'
2655    destruct(EQst2)
2656    >is_tailcall in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
2657    #ignore %{«?, is_tailcall'»}
2658    %{eq_call}
2659    % [2: % [2: %{(taa_base …)} %{(taa_base …)} % [ %{EQeval'} %{prf'} % ]] |*:]
2660    whd >(as_label_sigma_commute … good) %
2661  ]
2662]
2663qed.
Note: See TracBrowser for help on using the repository browser.