source: src/joint/lineariseProof.ma @ 2555

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

lemma eval_call_ok finished

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