source: src/joint/lineariseProof.ma @ 2559

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

lineariseProof finished

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