source: src/joint/lineariseProof.ma @ 2548

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

in BackEndOps?, cleaner def of be_op2
new statement of fetch_statement_sigma_commute and first part of further lemmas

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