source: src/joint/lineariseProof.ma @ 2536

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

finished eval_seq_no_pc_sigma_commute lemma

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