source: src/joint/lineariseProof.ma @ 2757

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

ERTLtoERTLptr in place

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