source: src/joint/lineariseProof.ma @ 2551

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

completed isFinal and fetchStatementSigmaCommute. Fixed exit definition and sigma_pc in semantics.ma

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