source: src/joint/lineariseProof.ma @ 2556

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

in joint semantics and traces: added a last popped calling address to state_pc, in order to have a strong enough as_after_return in joint (due to graph languages having one-to-many predecessors)
in lineariseProof: one axiom left (tailcall case)

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