source: src/joint/lineariseProof.ma @ 2528

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

added cases PUSH, C_ADDRESS and COPACCS

File size: 71.9 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "joint/linearise.ma".
16include "common/StatusSimulation.ma".   
17include "joint/Traces.ma".
18include "joint/semanticsUtils.ma".
19
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  ((Σi.is_internal_function_of_program … prog i) → ℕ) →
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  ((Σi.is_internal_function_of_program … prog i) → ℕ) →
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_pc_opt:
100 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
101  ((Σi.is_internal_function_of_program … graph_prog i) →
102    code_point (mk_graph_params p) → option ℕ) →
103   program_counter → option program_counter
104 ≝
105  λp,p',prog,sigma,pc.
106  let pars ≝ make_sem_graph_params p p' in
107  let ge ≝ globalenv_noinit … prog in
108  ! f ← int_funct_of_block ? ge (pc_block pc) ;
109  ! lin_point ← sigma f (point_of_pc ? pars pc) ;
110  return pc_of_point ? (make_sem_lin_params ? p') pc lin_point.
111
112definition well_formed_pc:
113 ∀p,p',graph_prog.
114  ((Σi.is_internal_function_of_program … graph_prog i) →
115    label → option ℕ) →
116   program_counter → Prop
117 ≝
118 λp,p',prog,sigma,pc.
119  sigma_pc_opt p p' prog sigma pc
120   ≠ None ….
121
122definition sigma_beval_opt :
123 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
124  ((Σi.is_internal_function_of_program … graph_prog i) →
125    code_point (mk_graph_params p) → option ℕ) →
126  beval → option beval ≝
127λp,p',graph_prog,sigma,bv.
128match bv with
129[ BVpc pc prt ⇒ ! pc' ← sigma_pc_opt p p' graph_prog sigma pc ; return BVpc pc' prt
130| _ ⇒ return bv
131].
132
133definition sigma_beval :
134 ∀p,p',graph_prog,sigma,bv.
135 sigma_beval_opt p p' graph_prog sigma bv ≠ None ? → beval ≝
136 λp,p',graph_prog,sigma,bv.opt_safe ….
137
138definition sigma_is_opt :
139 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
140  ((Σi.is_internal_function_of_program … graph_prog i) →
141    code_point (mk_graph_params p) → option ℕ) →
142  internal_stack → option internal_stack ≝
143λp,p',graph_prog,sigma,is.
144match is with
145[ empty_is ⇒ return empty_is
146| one_is bv ⇒ ! bv' ← sigma_beval_opt p p' … sigma bv ; return one_is bv'
147| both_is bv1 bv2 ⇒
148  ! bv1' ← sigma_beval_opt p p' … sigma bv1 ;
149  ! bv2' ← sigma_beval_opt p p' … sigma bv2 ;
150  return both_is bv1' bv2'
151].
152
153definition sigma_is :
154 ∀p,p',graph_prog,sigma,is.
155 sigma_is_opt p p' graph_prog sigma is ≠ None ? → internal_stack ≝
156 λp,p',graph_prog,sigma,is.opt_safe ….
157
158lemma sigma_is_pop_commute :
159 ∀p,p',graph_prog,sigma,is,bv,is'.
160 ∀prf : sigma_is_opt p p' graph_prog sigma is ≠ None ?.
161 is_pop is = return 〈bv, is'〉 →
162 ∃prf' : sigma_beval_opt p p' graph_prog sigma bv ≠ None ?.
163 ∃prf'' : sigma_is_opt p p' graph_prog sigma is' ≠ None ?.
164 is_pop (sigma_is … prf) = return 〈sigma_beval … prf', sigma_is … prf''〉.
165cases daemon qed.
166
167definition well_formed_mem :
168 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
169  ((Σi.is_internal_function_of_program … graph_prog i) →
170    code_point (mk_graph_params p) → option ℕ) →
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 : (Σi.is_internal_function_of_program (joint_closed_internal_function (mk_graph_params p))
314    graph_prog i) →
315      label → option ℕ) : Type[0] ≝
316{ well_formed_frames : framesT (make_sem_graph_params p p') → Prop
317; sigma_frames : ∀frms.well_formed_frames frms → framesT (make_sem_lin_params p p')
318; sigma_empty_frames_commute :
319  ∃prf.
320  empty_framesT (make_sem_lin_params p p') =
321  sigma_frames (empty_framesT (make_sem_graph_params p p')) prf
322
323; well_formed_regs : regsT (make_sem_graph_params p p') → Prop
324; sigma_regs : ∀regs.well_formed_regs regs → regsT (make_sem_lin_params p p')
325; sigma_empty_regsT_commute :
326  ∀ptr.∃ prf.
327  empty_regsT (make_sem_lin_params p p') ptr =
328  sigma_regs (empty_regsT (make_sem_graph_params p p') ptr) prf
329; sigma_load_sp_commute :
330  ∀reg,ptr.
331  load_sp (make_sem_graph_params p p') reg = return ptr →
332  ∃prf.
333  load_sp (make_sem_lin_params p p') (sigma_regs reg prf) = return ptr
334; sigma_save_sp_commute :
335  ∀reg,ptr,prf1. ∃prf2.
336  save_sp (make_sem_lin_params p p') (sigma_regs reg prf1) ptr =
337  sigma_regs (save_sp (make_sem_graph_params p p') reg ptr) prf2
338}.
339
340definition well_formed_state :
341 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
342 ∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) →
343    code_point (mk_graph_params p) → option ℕ).
344 good_sem_state_sigma p p' graph_prog sigma →
345 state (make_sem_graph_params p p') → Prop ≝
346λp,p',graph_prog,sigma,gsss,st.
347well_formed_frames … gsss (st_frms … st) ∧
348sigma_is_opt p p' graph_prog sigma (istack … st) ≠ None ? ∧
349well_formed_regs … gsss (regs … st) ∧
350well_formed_mem p p' graph_prog sigma (m … st).
351
352definition sigma_state :
353 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).
354 ∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) →
355    code_point (mk_graph_params p) → option ℕ).
356 ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
357 ∀st : state (make_sem_graph_params p p').
358 well_formed_state … gsss st →
359 state (make_sem_lin_params p p') ≝
360λp,p',graph_prog,sigma,gsss,st,prf.
361mk_state …
362  (sigma_frames p p' graph_prog sigma gsss (st_frms … st) ?)
363  (sigma_is p p' graph_prog sigma (istack … st) ?)
364  (carry … st)
365  (sigma_regs … gsss (regs … st) ?)
366  (sigma_mem p p' graph_prog sigma (m … st) ?).
367@hide_prf
368[ @(proj1 … (proj1 … (proj1 … prf))) | @(proj2 … (proj1 … (proj1 … prf)))
369| @(proj2 … (proj1 … prf)) | @(proj2 … prf)]
370qed.
371
372
373(*
374lemma sigma_is_pop_wf :
375 ∀p,p',graph_prog,sigma,is,bv,is'.
376 is_pop is = return 〈bv, is'〉 →
377 sigma_is_opt p p' graph_prog sigma is ≠ None ? →
378 sigma_beval_opt p p' graph_prog sigma bv ≠ None ? ∧
379 sigma_is_opt p p' graph_prog sigma is' ≠ None ?.
380cases daemon qed.
381*)
382
383(*
384lemma prova : ∀p,s,st,prf.sigma_pc_of_status p s st prf = ?.
385[ #p #s #st #prf
386  whd in match sigma_pc_of_status; normalize nodelta
387  @opt_safe_elim
388  #n
389  lapply (refl …  (int_funct_of_block (joint_closed_internal_function p) (globals p)
390        (ev_genv p) (pblock (pc p st))))
391  elim (int_funct_of_block (joint_closed_internal_function p) (globals p)
392        (ev_genv p) (pblock (pc p st))) in ⊢ (???%→%);
393  [ #_ #ABS normalize in ABS; destruct(ABS) ]
394  #f #EQ >m_return_bind
395*)
396
397
398(*
399lemma wf_status_to_wf_pc :
400∀p,p',graph_prog,stack_sizes.
401∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) →
402    code_point (mk_graph_params p) → option ℕ).
403∀st.
404well_formed_status p p' graph_prog stack_sizes sigma st →
405well_formed_pc p p' graph_prog stack_sizes sigma (pc ? st).
406#p #p' #graph_prog #stack_sizes #sigma #st whd in ⊢ (% → ?); * #H #_ @H
407qed.
408 *)
409definition sigma_pc :
410∀p,p',graph_prog.
411∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) →
412    label → option ℕ).
413∀pc.
414∀prf : well_formed_pc p p' graph_prog sigma pc.
415program_counter ≝
416λp,p',graph_prog,sigma,st.opt_safe ….
417 
418lemma sigma_pc_ok:
419  ∀p,p',graph_prog.
420  ∀sigma.
421   ∀pc.
422    ∀prf:well_formed_pc p p' graph_prog sigma pc.
423    sigma_pc_opt p p' graph_prog sigma pc =
424    Some … (sigma_pc p p' graph_prog sigma pc prf).
425    #p #p' #graph_prog #sigma #st #prf @opt_to_opt_safe qed.
426
427definition well_formed_state_pc :
428 ∀p,p',graph_prog,sigma.
429  good_sem_state_sigma p p' graph_prog sigma →
430  state_pc (make_sem_graph_params p p') → Prop ≝
431 λp,p',prog,sigma,gsss,st.
432 well_formed_pc p p' prog sigma (pc … st) ∧ well_formed_state … gsss st.
433 
434definition sigma_state_pc :
435 ∀p.
436 ∀p':∀F.sem_unserialized_params p F.
437 ∀graph_prog.
438  ∀sigma.
439(*   let lin_prog ≝ linearise ? graph_prog in *)
440  ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
441    ∀s:state_pc (make_sem_graph_params p p'). (* = graph_abstract_status p p' graph_prog stack_sizes *)
442     well_formed_state_pc p p' graph_prog sigma gsss s →
443      state_pc (make_sem_lin_params p p') (* = lin_abstract_status p p' lin_prog ? *)
444
445 λp,p',graph_prog,sigma,gsss,s,prf.
446 let pc' ≝ sigma_pc … (proj1 … prf) in
447 let st' ≝ sigma_state … (proj2 … prf) in
448 mk_state_pc ? st' pc'.
449
450definition sigma_function_name :
451 ∀p,graph_prog.
452 let lin_prog ≝ linearise p graph_prog in
453  (Σf.is_internal_function_of_program … graph_prog f) →
454  (Σf.is_internal_function_of_program … lin_prog f) ≝
455λp,graph_prog,f.«f, if_propagate … (pi2 … f)».
456
457lemma m_list_map_All_ok :
458  ∀M : MonadProps.∀X,Y,f,l.
459  All X (λx.∃y.f x = return y) l → ∃l'.m_list_map M X Y f l = return l'.
460  cases daemon qed.
461
462(*
463inductive isMember (A : Type[0]) (x : A) : list A → Prop ≝
464 | isMemberHead : ∀ tl.isMember A x (x :: tl)
465 | isMemberTail : ∀ y,tl .isMember A x tl → isMember A x (y :: tl).
466(*
467definition lift_f_tail : ∀ A,B : Type[0]. ∀ l ,tl : list A. ∀y : A . l = y ::tl →
468      (∀ x : A. isMember A x l → B) → ∀ x : A. isMember A x tl → B.
469      #A #B #l #tl #y #l_spec #f #x #tl_member @f [//]
470    @(isMemberTail ? x y l tl l_spec tl_member)
471    qed.
472  *)             
473
474let rec ext_map (A,B : Type[0]) (l : list A) (f : ∀ x : A. isMember A x l → B) on l : list B ≝
475match l with [ nil ⇒ λprf : l = nil ?.nil ?
476             | cons x tl ⇒ λprf : l = cons ? x tl.
477              f x ? :: ext_map ?? tl (λy,prf'.f y ?)
478             ] (refl …).
479@hide_prf
480>prf
481[ %1
482| %2 assumption
483] qed.
484              (f x (isMemberHead A x l tl prf)) ::   
485              ext_map A B tl (lift_f_tail A B l tl x prf f) ]
486              (refl ? l).
487*)
488
489definition helper_def_store__commute :
490  ∀p,p',graph_prog,sigma.
491  ∀X : ? → Type[0].
492  ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
493  ∀store : ∀p,F.∀p' : sem_unserialized_params p F.
494    X p → beval → regsT p' →
495    res (regsT p').
496  Prop ≝
497  λp,p',graph_prog,sigma,X,gsss,store.
498  ∀a : X ?.∀bv,r,r',prf1,prf1'.
499  store … a bv r = return r' →
500  ∃prf2.
501  store ??? a
502    (sigma_beval p p' graph_prog sigma bv prf1')
503    (sigma_regs ???? gsss r prf1) = return sigma_regs … gsss r' prf2.
504
505definition helper_def_retrieve__commute :
506  ∀p,p',graph_prog,sigma.
507  ∀X : ? → Type[0].
508  ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
509  ∀retrieve : ∀p,F.∀p' : sem_unserialized_params p F.
510    regsT p' → X p → res beval.
511  Prop ≝
512  λp,p',graph_prog,sigma,X,gsss,retrieve.
513  ∀a : X p.∀r,bv,prf1.
514  retrieve … r a = return bv →
515  ∃prf2.
516  retrieve … (sigma_regs … gsss r prf1) a
517     = return sigma_beval p p' graph_prog sigma bv prf2.
518 
519record good_state_sigma
520  (p : unserialized_params)
521  (p' : ∀F.sem_unserialized_params p F) (graph_prog : ?)
522 (sigma : (Σi.is_internal_function_of_program (joint_closed_internal_function (mk_graph_params p))
523    graph_prog i) →
524      label → option ℕ)
525: Type[0] ≝
526{ gsss :> good_sem_state_sigma p p' graph_prog sigma
527
528; acca_store__commute : helper_def_store__commute … gsss acca_store_
529; acca_retrieve_commute : helper_def_retrieve__commute … gsss acca_retrieve_
530; acca_arg_retrieve_commute : helper_def_retrieve__commute … gsss acca_arg_retrieve_
531; accb_store_commute : helper_def_store__commute … gsss accb_store_
532; accb_retrieve_commute : helper_def_retrieve__commute … gsss accb_retrieve_
533; accb_arg_retrieve_commute : helper_def_retrieve__commute … gsss accb_arg_retrieve_
534; dpl_store_commute : helper_def_store__commute … gsss dpl_store_
535; dpl_retrieve_commute : helper_def_retrieve__commute … gsss dpl_retrieve_
536; dpl_arg_retrieve_commute : helper_def_retrieve__commute … gsss dpl_arg_retrieve_
537; dph_store_commute : helper_def_store__commute … gsss dph_store_
538; dph_retrieve_commute : helper_def_retrieve__commute … gsss dph_retrieve_
539; dph_arg_retrieve_commute : helper_def_retrieve__commute … gsss dph_arg_retrieve_
540; snd_arg_retrieve_commute : helper_def_retrieve__commute … gsss snd_arg_retrieve_
541; pair_reg_move_commute : ∀mv,r1,r2,prf1.
542  pair_reg_move_ ? ? (p' ?) r1 mv = return r2 →
543  ∃prf2 .
544  pair_reg_move_ ? ? (p' ?) (sigma_regs p p' graph_prog sigma gsss r1 prf1) mv =
545    return sigma_regs p p' graph_prog sigma gsss r2 prf2
546; allocate_locals_commute :
547  ∀ loc, r1, prf1. ∃ prf2.
548  allocate_locals_ ? ? (p' ?) loc (sigma_regs p p' graph_prog sigma gsss r1 prf1) =
549  sigma_regs p p' graph_prog sigma gsss (allocate_locals_ ? ? (p' ?) loc r1) prf2
550; save_frame_commute :
551  ∀dest,st1,st2,prf1.
552  save_frame ?? (p' ?) dest st1 = return st2 →
553  let st1' ≝ mk_state_pc … (sigma_state p p' graph_prog sigma gsss st1 (proj2 … prf1))
554    (sigma_pc p p' graph_prog sigma (pc … st1) (proj1 … prf1)) in
555  ∃prf2.
556  save_frame ?? (p' ?) dest st1' = return sigma_state p p' graph_prog sigma gsss st2 prf2
557; eval_ext_seq_commute :
558  let lin_prog ≝ linearise p graph_prog in
559  ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
560  let stack_sizes' ≝
561   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
562     ? graph_prog stack_sizes in
563  ∀ext,fn,st1,st2,prf1.
564  eval_ext_seq ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes'))
565    ext fn st1 = return st2 →
566  ∃prf2.
567  eval_ext_seq ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
568    ext (sigma_function_name … fn) (sigma_state p p' graph_prog sigma gsss st1 prf1) =
569   return sigma_state p p' graph_prog sigma gsss st2 prf2
570; setup_call_commute :
571  ∀ n , parsT, call_args , st1 , st2 , prf1.
572  setup_call ?? (p' ?) n parsT call_args st1 = return st2 →
573  ∃prf2.
574  setup_call ?? (p' ?) n parsT call_args (sigma_state p p' graph_prog sigma gsss st1 prf1) =
575  return (sigma_state p p' graph_prog sigma gsss st2 prf2)
576; fetch_external_args_commute : (* TO BE CHECKED *)
577  ∀ex_fun,st1,prf1,call_args.
578  fetch_external_args ?? (p' ?) ex_fun st1 call_args =
579  fetch_external_args ?? (p' ?) ex_fun (sigma_state p p' graph_prog sigma gsss st1 prf1) call_args
580; set_result_commute :
581  ∀ l , call_dest , st1 , st2 , prf1.
582  set_result ?? (p' ?) l call_dest st1 = return st2 →
583  ∃prf2.
584  set_result ?? (p' ?) l call_dest (sigma_state p p' graph_prog sigma gsss st1 prf1) =
585  return (sigma_state p p' graph_prog sigma gsss st2 prf2) 
586; read_result_commute :
587  let lin_prog ≝ linearise p graph_prog in
588  ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
589  let stack_sizes' ≝
590   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
591     ? graph_prog stack_sizes in
592  ∀call_dest , st1 , prf1, l1.
593  read_result ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes'))
594    call_dest st1 = return l1 →
595  ∃ prf : m_list_map … (sigma_beval_opt p p' graph_prog sigma) l1 ≠ None ?.
596  read_result ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
597    call_dest (sigma_state p p' graph_prog sigma gsss st1 prf1) = return opt_safe … prf 
598; pop_frame_commute :
599  let lin_prog ≝ linearise p graph_prog in
600  ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
601  let stack_sizes' ≝
602   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
603     ? graph_prog stack_sizes in
604  ∀ st1 , prf1, curr_id ,st2.
605  pop_frame ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes'))
606            curr_id st1 = return st2 →
607 ∃prf2.
608 let pc' ≝ sigma_pc p p' graph_prog sigma (pc ? st2) (proj1 … prf2) in
609 let st2' ≝ sigma_state p p' graph_prog sigma gsss (st_no_pc ? st2) (proj2 … prf2) in
610  pop_frame ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes))
611            (sigma_function_name p graph_prog curr_id) (sigma_state p p' graph_prog sigma gsss st1 prf1) =
612            return mk_state_pc ? st2' pc'
613}.
614
615lemma store_commute :
616  ∀p,p',graph_prog,sigma.
617  ∀X : ? → Type[0].
618  ∀store.
619  ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
620  ∀H : helper_def_store__commute … gsss store.
621  ∀a : X p.∀bv,st,st',prf1,prf1'.
622  helper_def_store ? store … a bv st = return st' →
623  ∃prf2.
624  helper_def_store ? store … a
625    (sigma_beval p p' graph_prog sigma bv prf1')
626    (sigma_state … gsss st prf1) = return sigma_state … gsss st' prf2.
627#p #p' #graph_prog #sigma #X #store #gsss #H #a #bv #st #st #prf1 #prf2
628whd in match helper_def_store; normalize nodelta
629#H1 elim(bind_inversion ????? H1) -H1 #graph_reg * #store_spec
630#EQ whd in EQ : (??%%); destruct(EQ)
631elim(H a bv ?? (proj2 … (proj1 … prf1)) prf2 store_spec)
632#wf_graph_reg #store_spec1 %
633[ % [ % ] [%] ]
634[ @(proj1 … (proj1 … (proj1 … prf1)))
635| @(proj2 … (proj1 … (proj1 … prf1)))
636| @wf_graph_reg
637| @(proj2 … prf1)
638] >store_spec1 >m_return_bind %
639qed.
640
641
642
643lemma retrieve_commute :
644 ∀p,p',graph_prog,sigma.
645 ∀X : ? → Type[0].
646 ∀retrieve.
647 ∀gsss : good_sem_state_sigma p p' graph_prog sigma.
648 ∀H : helper_def_retrieve__commute … gsss retrieve.
649 ∀a : X p .∀st,bv,prf1.
650 helper_def_retrieve ? retrieve … st a = return bv →
651 ∃prf2.
652     helper_def_retrieve ? retrieve … (sigma_state … gsss st prf1) a =
653     return sigma_beval p p' graph_prog sigma bv prf2.
654#p #p' #graph_prog #sigma #X #retrieve #gsss #H #a #st #bv #prf1
655whd in match helper_def_retrieve; normalize nodelta
656#retrieve_spec elim(H … (proj2 … (proj1 … prf1)) … retrieve_spec)
657#wf_bv #retrieve_spec1 %{wf_bv} >retrieve_spec1 %
658qed.
659
660(*
661definition acca_store_commute :
662  ∀p,p',graph_prog,sigma.
663  ∀gss : good_state_sigma p p' graph_prog sigma.
664  ∀a : acc_a_reg p.∀bv,st,st',prf1,prf1'.
665  acca_store … a bv st = return st' →
666  ∃prf2.
667  acca_store … a
668    (sigma_beval p p' graph_prog sigma bv prf1')
669    (sigma_state … gss st prf1) = return sigma_state … gss st' prf2
670 ≝
671λp,p',graph_prog,sigma.
672λgss : good_state_sigma p p' graph_prog sigma.
673store_commute … gss (acca_store__commute … gss).
674 
675   
676lemma acca_store_commute :
677  ∀p,p',graph_prog,sigma.
678  ∀gss : good_state_sigma p p' graph_prog sigma.
679  ∀a,bv,st,st',prf1,prf1'.
680  acca_store ?? (p' ?) a bv st = return st' →
681  ∃prf2.
682  acca_store ?? (p' ?) a
683    (sigma_beval p p' graph_prog sigma bv prf1')
684    (sigma_state … gss st prf1) = return sigma_state … gss st' prf2 ≝
685λp,p',graph_prog,sigma,gss,a,bv.?.
686* #frms #is #carry #regs #m
687* #frms' #is' #carry' #regs' #m'
688*** #frms_ok #is_ok #regs_ok #mem_ok
689#bv_ok #EQ1 elim (bind_inversion ????? EQ1)
690#regs'' * -EQ1 #EQ1 whd in ⊢ (??%%→?); #EQ destruct(EQ)
691elim (acca_store__commute … gss … EQ1)
692[ #prf2 #EQ2
693  % [ whd /4 by conj/ ]
694  change with (! r ← ? ; ? = ?) >EQ2
695  whd in match (sigma_state ???????); normalize nodelta
696   >m_return_bind
697
698
699st,st',prf1,prf2,prf3.?.
700
701
702#p #p' #
703*)
704
705(* restano:
706; setup_call : nat → paramsT … uns_pars → call_args uns_pars →
707    state st_pars → res (state st_pars)
708; fetch_external_args: external_function → state st_pars → call_args … uns_pars →
709    res (list val)
710; set_result: list val → call_dest uns_pars → state st_pars → res (state st_pars)
711
712(* from now on, parameters that use the type of functions *)
713; read_result: ∀globals.genv_gen F globals → call_dest uns_pars → state st_pars → res (list beval)
714(* change of pc must be left to *_flow execution *)
715; pop_frame: ∀globals.∀ge : genv_gen F globals.
716  (Σi.is_internal_function … ge i) (* current *) → state st_pars → res (state st_pars)
717*)
718
719(*
720lemma sigma_pc_commute:
721 ∀p,p',graph_prog,sigma,gss,st.
722 ∀prf : well_formed_state_pc p p' graph_prog sigma gss st.
723 sigma_pc … (pc ? st) (proj1 … prf) =
724 pc ? (sigma_state_pc … st prf). // qed.
725*)
726
727lemma res_eq_from_opt :
728  ∀A,m,v.res_to_opt A m = return v → m = return v.
729#A * #x #v normalize #EQ destruct % qed.
730
731lemma if_of_function_commute:
732 ∀p.
733 ∀graph_prog : joint_program (mk_graph_params p).
734 ∀graph_fun : Σi.is_internal_function_of_program … graph_prog i.
735 let graph_fd ≝ if_of_function … graph_fun in
736 let lin_fun ≝ sigma_function_name … graph_fun in
737 let lin_fd ≝ if_of_function … lin_fun in
738 lin_fd = \fst (linearise_int_fun ?? graph_fd).
739 #p #graph_prog #graph_fun whd
740 @prog_if_of_function_transform % qed.
741
742lemma bind_opt_inversion:
743  ∀A,B: Type[0]. ∀f: option A. ∀g: A → option B. ∀y: B.
744  (! x ← f ; g x = Some … y) →
745  ∃x. (f = Some … x) ∧ (g x = Some … y).
746#A #B #f #g #y cases f normalize
747[ #H destruct (H)
748| #a #e %{a} /2 by conj/
749] qed.
750
751lemma sigma_pblock_eq_lemma :
752∀p,p',graph_prog.
753let lin_prog ≝ linearise p graph_prog in
754∀sigma,pc.
755∀prf : well_formed_pc p p' graph_prog sigma pc.
756 pc_block (sigma_pc ? p' graph_prog sigma pc prf) =
757 pc_block pc.
758 #p #p' #graph_prog #sigma #pc #prf
759 whd in match sigma_pc; normalize nodelta
760 @opt_safe_elim #x #x_spec
761 whd in x_spec:(??%?); cases (int_funct_of_block ???) in x_spec;
762 normalize nodelta [#abs destruct] #id #H cases (bind_opt_inversion ????? H) -H
763 #offset * #_ whd in ⊢ (??%? → ?); #EQ destruct //
764qed.
765
766(*
767lemma bind_opt_non_none : ∀A,B : Type[0] . ∀ m : option A . ∀g : A → option B.
768(! x ← m ; g x) ≠ None ? → m ≠ None ?.
769#A #B #m #g #H % #m_eq_none cases m >m_eq_none in H; normalize 
770[ #abs elim abs -abs #abs @abs %
771| #abs elim abs -abs #abs #v @abs %
772]
773qed.
774
775lemma match_option_non_none : ∀A ,B, C : Type[0]. ∀m : option A. ∀ x : A.
776∀ b : B .∀ f : A → B. ∀g : B → option C.
777g (match m with [None  ⇒ b  | Some  x ⇒ f x])≠ None ? →  g b = None ? → m ≠ None ?.
778#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
779qed.
780*)
781
782lemma funct_of_block_transf :
783∀A,B.∀progr : program (λvars .fundef (A vars)) ℕ.
784∀transf : ∀vars. A vars → B vars. ∀bl,f,prf.
785let progr' ≝ transform_program … progr (λvars.transf_fundef … (transf vars)) in
786funct_of_block … (globalenv_noinit … progr) bl = return f →
787funct_of_block … (globalenv_noinit … progr') bl = return «pi1 … f,prf».
788#A #B #progr #transf #bl #f #prf whd
789whd in match funct_of_block in ⊢ (%→?); normalize nodelta
790cut (∀A,B : Type[0].∀Q : option A → Prop.∀P : B → Prop.
791  ∀o.∀prf : Q o.
792  ∀f1,f2.
793  (∀x,prf.P (f1 x prf)) → (∀prf.P(f2 prf)) →
794  P (match o return λx.Q x → B with [ Some x ⇒ f1 x | None ⇒ f2 ] prf))
795  [ #A #B #Q #P * /2/ ] #aux
796@aux [2: #_ change with (?=Some ??→?) #ABS destruct(ABS) ]
797#fd #EQfind whd in ⊢ (??%%→?);
798generalize in ⊢ (??(??(????%))?→?); #e #EQ destruct(EQ)
799whd in match funct_of_block; normalize nodelta
800@aux [ # fd' ]
801[2: >(find_funct_ptr_transf … EQfind) #ABS destruct(ABS) ]
802#prf' cases daemon qed.
803
804lemma description_of_function_transf :
805∀A,B.∀progr : program (λvars .fundef (A vars)) ℕ.
806∀transf : ∀vars. A vars → B vars.
807let progr' ≝ transform_program … progr (λvars.transf_fundef … (transf vars)) in
808∀f_out,prf.
809description_of_function …
810  (globalenv_noinit … progr') f_out =
811transf_fundef … (transf ?) (description_of_function … (globalenv_noinit … progr)
812  «pi1 … f_out, prf»).
813#A #B #progr #transf #f_out #prf
814whd in match description_of_function in ⊢ (???%);
815normalize nodelta
816cut (∀A,B : Type[0].∀Q : option A → Prop.∀P : B → Prop.
817  ∀o.∀prf : Q o.
818  ∀f1,f2.
819  (∀x,prf.o = Some ? x → P (f1 x prf)) → (∀prf.o = None ? → P(f2 prf)) →
820  P (match o return λx.Q x → B with [ Some x ⇒ f1 x | None ⇒ f2 ] prf))
821  [ #A #B #Q #P * /2/ ] #aux
822@aux
823[ #fd' ] * #fd #EQ destruct (EQ)
824inversion (find_symbol ???) [ #_ whd in ⊢ (??%?→?); #ABS destruct(ABS) ]
825#bl #EQfind >m_return_bind #EQfindf
826whd in match description_of_function; normalize nodelta
827@aux
828[ #fdo' ] * #fdo #EQ destruct (EQ)
829>find_symbol_transf >EQfind >m_return_bind
830>(find_funct_ptr_transf … EQfindf) #EQ destruct(EQ) %
831qed.
832
833
834lemma match_int_fun :
835∀A,B : Type[0].∀P : B → Prop.
836∀Q : fundef A → Prop.
837∀m : fundef A.
838∀f1 : ∀fd.Q (Internal \ldots  fd) → B.
839∀f2 : ∀fd.Q (External … fd) → B.
840∀prf : Q m.
841(∀fd,prf.P (f1 fd prf)) →
842(∀fd,prf.P (f2 fd prf)) →
843P (match m
844return λx.Q x → ?
845with
846[ Internal fd ⇒ f1 fd
847| External fd ⇒ f2 fd
848] prf).
849#A #B #P #Q * // qed.
850(*)
851 lemma match_int_fun :
852∀A,B : Type[0].∀P : B → Prop.
853∀m : fundef A.
854∀f1 : ∀fd.m = Internal … fd → B.
855∀f2 : ∀fd.m = External … fd → B.
856(∀fd,prf.P (f1 fd prf)) →
857(∀fd,prf.P (f2 fd prf)) →
858P (match m
859return λx.m = x → ?
860with
861[ Internal fd ⇒ f1 fd
862| External fd ⇒ f2 fd
863] (refl …)).
864#A #B #P * // qed.
865*)
866(*
867lemma prova :
868∀ A.∀progr : program (λvars. fundef (A vars)) ℕ.
869∀ M : fundef (A (prog_var_names (λvars:list ident.fundef (A vars)) ℕ progr)).
870∀ f,g,prf1.
871match M return λx.M = x → option (Σi.is_internal_function_of_program ?? progr i) with
872[Internal fn ⇒ λ prf.return «g,prf1 fn prf» |
873External fn ⇒ λprf.None ? ] (refl ? M) = return f → 
874∃ fn. ∃ prf : M = Internal ? fn . f = «g, prf1 fn prf».
875#H1 #H2 #H3 #H4 #H5 #H6
876@match_int_fun
877#fd #EQ #EQ' whd in EQ' : (??%%); destruct
878%[|%[| % ]] qed.
879*)
880
881lemma int_funct_of_block_transf:
882 ∀A,B.∀progr: program (λvars. fundef (A vars)) ℕ.
883  ∀transf: ∀vars. A vars → B vars. ∀bl,f,prf.
884   let progr' ≝ transform_program … progr (λvars.transf_fundef … (transf vars)) in
885     int_funct_of_block ? (globalenv_noinit … progr) bl = return f →
886     int_funct_of_block ? (globalenv_noinit … progr') bl = return «pi1 … f,prf».
887#A #B #progr #transf #bl #f #prf
888whd whd in match int_funct_of_block in ⊢ (??%?→?); normalize nodelta
889#H
890elim (bind_opt_inversion ??? ?? H) -H #x
891* #x_spec
892@match_int_fun [2: #fd #_ #ABS destruct(ABS) ]
893#fd #EQdescr change with (Some ?? = ? → ?) #EQ destruct(EQ)
894whd in match int_funct_of_block; normalize nodelta
895>(funct_of_block_transf … (internal_function_is_function … prf) … x_spec)
896>m_return_bind
897@match_int_fun #fd' #prf' [ % ]
898@⊥ cases x in prf EQdescr prf'; -x #x #x_prf #prf #EQdescr
899>(description_of_function_transf) [2: @x_prf ]
900>EQdescr whd in ⊢ (??%%→?); #ABS destruct qed.
901
902
903lemma fetch_function_sigma_commute :
904 ∀p,p',graph_prog.
905 let lin_prog ≝ linearise p graph_prog in
906 ∀sigma,pc_st,f.
907  ∀prf : well_formed_pc p p' graph_prog sigma pc_st.
908 fetch_function … (globalenv_noinit … graph_prog) pc_st =
909  return f
910→ fetch_function … (globalenv_noinit … lin_prog) (sigma_pc … pc_st prf) =
911  return sigma_function_name … f.
912 #p #p' #graph_prog #sigma #st #f #prf
913 whd in match fetch_function; normalize nodelta
914 >(sigma_pblock_eq_lemma … prf) #H
915 lapply (opt_eq_from_res ???? H) -H #H
916 >(int_funct_of_block_transf ?? graph_prog (λvars,graph_fun.\fst (linearise_int_fun … graph_fun)) ??? H)
917 //
918qed.
919 
920(*
921#H elim (bind_opt_inversion ????? H) -H
922#x * whd in match funct_of_block in ⊢ (%→?); normalize nodelta
923@match_opt_prf_elim
924 #H #H1  whd in H : (??%?);
925cases (   find_funct_ptr
926   (fundef
927    (joint_closed_internal_function
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     (globals
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   (ev_genv
936    (graph_prog_params p p' graph_prog
937     (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
938      (linearise_int_fun p) graph_prog stack_sizes)))
939   (pblock (pc (make_sem_graph_params p p') st))) in H; [ 2: normalize #abs destruct
940 
941
942normalize nodelta
943#H #H1
944cases (   find_funct_ptr
945   (fundef
946    (joint_closed_internal_function
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     (globals
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   (ev_genv
955    (graph_prog_params p p' graph_prog
956     (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
957      (linearise_int_fun p) graph_prog stack_sizes)))
958   (pblock (pc (make_sem_graph_params p p') st))) in H;
959
960
961check find_funct_ptr_transf
962whd in match int_funct_of_block; normalize nodelta
963#H elim (bind_inversion ????? H)
964
965.. sigma_int_funct_of_block
966
967
968
969whd in match int_funct_of_block; normalize nodelta
970elim (bind_inversion ????? H)
971whd in match int_funct_of_block; normalize nodelta
972#H elim (bind_inversion ????? H) -H #fn *
973#H lapply (opt_eq_from_res ???? H) -H
974#H >(find_funct_ptr_transf … (λglobals.transf_fundef … (linearise_int_fun … globals)) … H)
975-H #H >m_return_bind cases fn in H; normalize nodelta #arg #EQ whd in EQ:(??%%);
976destruct //
977cases daemon
978qed. *)
979
980lemma opt_Exists_elim:
981 ∀A:Type[0].∀P:A → Prop.
982  ∀o:option A.
983   opt_Exists A P o →
984    ∃v:A. o = Some … v ∧ P v.
985 #A #P * normalize /3/ *
986qed.
987
988
989lemma stmt_at_sigma_commute:
990 ∀p,graph_prog,graph_fun,lbl,pt.
991 let lin_prog ≝ linearise ? graph_prog in
992 let lin_fun ≝ sigma_function_name p graph_prog graph_fun in
993 ∀sigma.good_sigma p graph_prog sigma →
994 sigma graph_fun lbl = return pt →
995 ∀stmt.
996   stmt_at …
997    (joint_if_code ?? (if_of_function ?? graph_fun)) 
998    lbl = return stmt →
999   stmt_at ??
1000    (joint_if_code ?? (if_of_function ?? lin_fun))
1001    pt = return (graph_to_lin_statement … stmt). 
1002 #p #graph_prog #graph_fun #lbl #pt #sigma #good #prf #stmt
1003cases (good graph_fun (pi2 … (sigma_function_name p graph_prog graph_fun)))
1004#sigma_entry_is_zero #lin_stmt_spec
1005lapply (lin_stmt_spec lbl pt prf) -lin_stmt_spec * #stmt1 *
1006#EQlookup_stmt1 #H
1007elim (opt_Exists_elim … H) -H * #optlbl_graph_stmt #graph_stmt
1008* #EQnth_opt_graph_stmt normalize nodelta
1009* #optEQlbl_optlbl_graph_stmt #next_spec
1010whd in match (stmt_at ????) in ⊢ (% → ?);
1011normalize nodelta
1012>EQlookup_stmt1 whd in ⊢ ((???%) → ?); #EQ destruct(EQ)
1013whd in match (stmt_at ????); > EQnth_opt_graph_stmt
1014normalize nodelta elim  optEQlbl_optlbl_graph_stmt #_ #EQ >EQ //
1015qed.
1016(*
1017
1018 >(if_of_function_commute … graph_fun)
1019
1020check opt_Exists
1021check linearise_int_fun
1022check
1023 whd in match (stmt_at ????);
1024 whd in match (stmt_at ????);
1025 cases (linearise_code_spec … p' graph_prog graph_fun
1026         (joint_if_entry … graph_fun))
1027 * #lin_code_closed #sigma_entry_is_zero #sigma_spec
1028 lapply (sigma_spec
1029         (point_of_pointer ? (graph_prog_params … p' graph_prog) (pc … s1)))
1030 -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @(sigma_pc_of_status_ok … prf) |2: skip ]
1031 -sigma_spec #graph_stmt * #graph_lookup_ok >graph_lookup_ok -graph_lookup_ok
1032 whd in ⊢ (? → ???%); #sigma_spec whd in sigma_spec;
1033 inversion (nth_opt ???) in sigma_spec; [ #H whd in ⊢ (% → ?); #abs cases abs ]
1034 * #optlabel #lin_stm #lin_lookup_ok whd in ⊢ (% → ?); ** #_
1035 #related_lin_stm_graph_stm #_ <related_lin_stm_graph_stm -related_lin_stm_graph_stm
1036 <sigma_pc_commute >lin_lookup_ok // *)
1037
1038lemma fetch_statement_sigma_commute:
1039  ∀p,p',graph_prog,pc,fn,stmt.
1040  let lin_prog ≝ linearise ? graph_prog in
1041  ∀sigma.good_sigma p graph_prog sigma →
1042  ∀prf : well_formed_pc p p' graph_prog sigma pc.
1043  fetch_statement ? (make_sem_graph_params p p') …
1044    (globalenv_noinit … graph_prog) pc = return 〈fn,stmt〉 →
1045  fetch_statement ? (make_sem_lin_params p p') …
1046    (globalenv_noinit … lin_prog) (sigma_pc … pc prf) =
1047    return 〈sigma_function_name … fn, graph_to_lin_statement … stmt〉.
1048 #p #p' #graph_prog #pc #fn #stmt #sigma #good #wfprf
1049 whd in match fetch_statement; normalize nodelta #H
1050 cases (bind_inversion ????? H) #id * -H #fetchfn
1051 >(fetch_function_sigma_commute … wfprf … fetchfn) >m_return_bind
1052 #H cases (bind_inversion ????? H) #fstmt * -H #H
1053 lapply (opt_eq_from_res ???? H) -H #H #EQ whd in EQ:(??%%); destruct
1054 >(stmt_at_sigma_commute … good … H) [%]
1055 whd in match sigma_pc; normalize nodelta
1056 @opt_safe_elim #pc' #H
1057 cases (bind_opt_inversion ????? H)
1058 #i * #EQ1 -H #H
1059 cases (bind_opt_inversion ????? H)
1060 #pnt * #EQ2 whd in ⊢ (??%?→?); #EQ3 destruct
1061 whd in match point_of_pc in ⊢ (???%); normalize nodelta >point_of_offset_of_point
1062 lapply (opt_eq_from_res ???? fetchfn) >EQ1 #EQ4 destruct @EQ2
1063qed.
1064
1065lemma point_of_pc_sigma_commute :
1066 ∀p,p',graph_prog.
1067 let lin_prog ≝ linearise p graph_prog in
1068 ∀sigma,pc,fn,n.
1069  ∀prf : well_formed_pc p p' graph_prog sigma pc.
1070 int_funct_of_block … (globalenv_noinit … graph_prog) (pc_block pc) = return fn →
1071 sigma fn (point_of_pc ? (make_sem_graph_params p p') pc) = return n →
1072 point_of_pc ? (make_sem_lin_params p p') (sigma_pc … pc prf) = n.
1073#p #p' #graph_prog #sigma #pc #fn #n #prf #EQfetch #EQsigma
1074whd in match sigma_pc; normalize nodelta
1075@opt_safe_elim #pc' whd in match sigma_pc_opt;
1076normalize nodelta >EQfetch >m_return_bind >EQsigma
1077>m_return_bind whd in ⊢ (??%?→?); #EQ destruct(EQ)
1078change with (point_of_offset ??? = ?) @point_of_offset_of_point
1079qed.
1080
1081definition linearise_status_rel:
1082 ∀p,p',graph_prog.
1083 let lin_prog ≝ linearise p graph_prog in
1084 ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
1085 let stack_sizes' ≝
1086  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
1087    ? graph_prog stack_sizes in
1088 ∀sigma,gss.
1089 good_sigma p graph_prog sigma →
1090   status_rel
1091    (graph_abstract_status p p' graph_prog stack_sizes')
1092    (lin_abstract_status p p' lin_prog stack_sizes)
1093 ≝ λp,p',graph_prog,stack_sizes,sigma,gss,good.
1094   mk_status_rel …
1095    (* sem_rel ≝ *) (λs1,s2.
1096     ∃prf: well_formed_state_pc p p' graph_prog sigma gss s1.
1097      s2 = sigma_state_pc … s1 prf)
1098    (* call_rel ≝ *) (λs1,s2.
1099      ∃prf:well_formed_state_pc p p' graph_prog sigma gss s1.
1100      pc ? s2 = sigma_pc … (pc ? s1) (proj1 … prf))
1101    (* sim_final ≝ *) ?.
1102#st1 #st2 * #prf #EQ2
1103%
1104whd in ⊢ (%→%);
1105#H lapply (opt_to_opt_safe … H)
1106@opt_safe_elim -H
1107#res #_
1108#H lapply (res_eq_from_opt ??? H) -H
1109cases daemon
1110(*#H elim (bind_inversion ????? H) in ⊢ ?;
1111* #f #stmt *
1112whd in ⊢ (??%?→?);*)
1113qed.
1114
1115lemma IO_bind_inversion:
1116  ∀O,I,A,B. ∀f: IO O I A. ∀g: A → IO O I B. ∀y: B.
1117  (! x ← f ; g x = return y) →
1118  ∃x. (f = return x) ∧ (g x = return y).
1119#O #I #A #B #f #g #y cases f normalize
1120[ #o #f #H destruct
1121| #a #e %{a} /2 by conj/
1122| #m #H destruct (H)
1123] qed.
1124
1125lemma err_eq_from_io : ∀O,I,X,m,v.
1126  err_to_io O I X m = return v → m = return v.
1127#O #I #X * #x #v normalize #EQ destruct % qed.
1128
1129lemma err_eq_to_io : ∀O,I,X,m,v.
1130   m = return v → err_to_io O I X m = return v.
1131#O #I #X #m #v #H >H //
1132qed.
1133
1134lemma set_istack_sigma_commute :
1135∀p,p',graph_prog,sigma,gss,st,is,sigma_is,prf1,prf2.
1136sigma_is_opt p p' graph_prog sigma is = return sigma_is →
1137set_istack ? sigma_is (sigma_state p p' graph_prog sigma gss st prf1) =
1138sigma_state ???? gss (set_istack ? is st) prf2.
1139#p #p' #graph_prog #sigma #gss #st #is #sigmais #prf1 #prf2 #H
1140whd in match set_istack; normalize nodelta
1141whd in match sigma_state; normalize nodelta
1142whd in match sigma_is; normalize nodelta
1143@opt_safe_elim #x #H1
1144cut(x = sigmais) [>H1 in H; #EQ whd in EQ : (???%); destruct(EQ) %]
1145#EQ >EQ //
1146qed.
1147
1148lemma is_push_sigma_commute :
1149∀ p, p', graph_prog,sigma,gss,st,val,is,prf1,prf2.
1150(is_push (istack … st) val=return is) →
1151∃prf3.
1152is_push (istack … (sigma_state p p' graph_prog sigma gss st prf1))
1153        (sigma_beval p p' graph_prog sigma val prf2) =
1154return sigma_is p p' graph_prog sigma is prf3.
1155#p #p' #graph_prog #sigma #gss #st #val #is #prf1 #prf2 #H
1156%
1157[ @hide_prf
1158whd in match sigma_is_opt; normalize nodelta
1159inversion (istack ? ?) in H;
1160whd in match is_push; normalize nodelta [3: #a #b #_ #ABS whd in ABS : (???%); destruct(ABS)]
1161[2: #a] #a_spec #EQ whd in EQ : (??%%); destruct(EQ) normalize nodelta
1162inversion (sigma_beval_opt ???? val) [1,3: #ABS >ABS in prf2; * #ABS @⊥ @ABS %]
1163[2: #val' #_ >m_return_bind whd in ⊢ (?(??%?)); % #ABS destruct(ABS)]
1164#val' #_
1165inversion(sigma_beval_opt ???? a)
1166  [2: #val'' #_ >m_return_bind >m_return_bind % #EQ whd in EQ : (??%?); destruct(EQ)]
1167#ABS @⊥ lapply(proj2 … (proj1 … (proj1 … prf1))) >a_spec
1168whd in match sigma_is_opt; normalize nodelta >ABS whd in ⊢ ((?(??%?))→ ?); *
1169#EQ @EQ %
1170]
1171whd in match sigma_state; normalize nodelta
1172cut(is_push (istack (make_sem_graph_params p p') st) val=return is)
1173[ assumption] 
1174#H1 whd in match sigma_is; normalize nodelta
1175@opt_safe_elim #is1 #is1_spec
1176whd in match sigma_beval; normalize nodelta
1177@opt_safe_elim #sigma_val #sigma_val_sepc
1178@opt_safe_elim #sigma_is #sigma_is_spec
1179inversion(istack ? st)
1180[2: #val1|3:#val1 #val2]
1181#H2 >H2 in H1;
1182whd in match is_push; normalize nodelta
1183#EQ whd in EQ : (??%%); destruct(EQ)
1184>H2 in is1_spec; whd in match sigma_is_opt; normalize nodelta
1185#EQ whd in EQ : (??%?); destruct(EQ)
1186normalize nodelta
1187whd in match sigma_is_opt in sigma_is_spec;
1188normalize nodelta in sigma_is_spec;
1189>sigma_val_sepc in sigma_is_spec;
1190[ inversion(sigma_beval_opt ???? val1)
1191[ #ABS #EQ1 whd in EQ1 : (??%%); destruct(EQ1) | #sigma_val1 #H3 >m_return_bind]]
1192>m_return_bind
1193#EQ whd in EQ : (??%?); destruct(EQ) [2: %]
1194>H3 in EQ;
1195normalize nodelta
1196#EQ1 whd in EQ1 : (??%%); destruct(EQ1)
1197normalize nodelta //
1198qed.
1199
1200lemma beopaccs_sigma_commute :
1201∀p,p',graph_prog,sigma,op,val1,val2,opaccs1,opaccs2.
1202∀ prf1 : sigma_beval_opt p p' graph_prog sigma val1 ≠ None ?.
1203∀ prf2 : sigma_beval_opt p p' graph_prog sigma val2 ≠ None ?.
1204be_opaccs op val1 val2=return 〈opaccs1,opaccs2〉 →
1205∃ prf1' : sigma_beval_opt p p' graph_prog sigma opaccs1 ≠ None ?.
1206∃ prf2' : sigma_beval_opt p p' graph_prog sigma opaccs2 ≠ None ?.
1207be_opaccs op (sigma_beval … prf1) (sigma_beval … prf2) =
1208return 〈(sigma_beval … prf1'),(sigma_beval … prf2')〉.
1209#p #p' #graph_prog #sigma #op #val1 #val2
1210#opaccs1 #opaccs2 #prf1 #prf2
1211whd in match be_opaccs; normalize nodelta
1212#H elim(bind_inversion ????? H) -H
1213#x * #x_spec
1214#H elim(bind_inversion ????? H) -H
1215#y * #y_spec
1216#H lapply H #H1 normalize in H; elim(opaccs_implementation op x y) in H;
1217#b1 #b2 #EQ normalize in EQ; destruct(EQ)
1218%
1219[whd in match sigma_beval_opt; normalize nodelta % #ABS
1220whd in ABS : (??%?); destruct(ABS)]
1221%
1222[whd in match sigma_beval_opt; normalize nodelta % #ABS
1223whd in ABS : (??%?); destruct(ABS)]
1224whd in match sigma_beval; normalize nodelta
1225@opt_safe_elim #sigma_val1 #sigma_val1_spec
1226@opt_safe_elim #sigma_val2 #sigma_val2_spec
1227@opt_safe_elim #sigma_op1 #sigma_op1_spec
1228@opt_safe_elim #sigma_op2 #sigma_op2_spec
1229lapply x_spec -x_spec lapply sigma_val1_spec -sigma_val1_spec
1230inversion val1 whd in match Byte_of_val; normalize nodelta
1231[ 1,2,5,6,7: [ 1,2: #_ #_] [3: #a #_ #_] [4,5 : #a #b #_ #_] #ABS whd in ABS : (???%); destruct(ABS)]
1232[#pt1 #pt2 #a #_ #_ #ABS whd in ABS : (???%); destruct(ABS)]
1233#bt_val1 #val1_spec whd in match sigma_beval_opt; normalize nodelta
1234whd in ⊢ ((??%?)→ ?); #EQ destruct(EQ)
1235#EQ whd in EQ : (???%); destruct(EQ)
1236lapply y_spec -y_spec lapply sigma_val2_spec -sigma_val2_spec
1237inversion val2 whd in match Byte_of_val; normalize nodelta
1238[ 1,2,5,6,7: [ 1,2: #_ #_] [3: #a #_ #_] [4,5 : #a #b #_ #_] #ABS whd in ABS : (???%); destruct(ABS)]
1239[#pt1 #pt2 #a #_ #_ #ABS whd in ABS : (???%); destruct(ABS)]
1240#bt_val2 #val2_spec whd in match sigma_beval_opt; normalize nodelta
1241whd in ⊢ ((??%?)→ ?); #EQ destruct(EQ) normalize nodelta
1242#EQ whd in EQ : (???%); destruct(EQ)
1243>m_return_bind >m_return_bind
1244whd in match sigma_beval_opt in sigma_op1_spec;
1245normalize nodelta in sigma_op1_spec;
1246whd in sigma_op1_spec : (??%?); destruct(sigma_op1_spec)
1247whd in match sigma_beval_opt in sigma_op2_spec;
1248normalize nodelta in sigma_op2_spec;
1249whd in sigma_op2_spec : (??%?); destruct(sigma_op2_spec)
1250>H1 %
1251qed.
1252
1253lemma eval_seq_no_pc_sigma_commute :
1254 ∀p,p',graph_prog.
1255 let lin_prog ≝ linearise p graph_prog in
1256 ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
1257 let stack_sizes' ≝
1258  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
1259    ? graph_prog stack_sizes in
1260 ∀sigma.∀gss : good_state_sigma … graph_prog sigma.
1261 ∀fn,st,stmt,st'.
1262 ∀prf : well_formed_state … gss st.
1263  eval_seq_no_pc ?? (ev_genv … (graph_prog_params … graph_prog stack_sizes'))
1264   fn st stmt = return st' →
1265  ∃prf'.
1266  eval_seq_no_pc ?? (ev_genv … (lin_prog_params … lin_prog stack_sizes))
1267    (sigma_function_name … fn) (sigma_state … gss st prf) stmt =
1268  return sigma_state … gss st' prf'.
1269  #p #p' #graph_prog #stack_sizes #sigma #gss
1270  #fn #st #stmt
1271  #st' #prf
1272  whd in match eval_seq_no_pc;
1273  cases stmt normalize nodelta
1274  [1,2: (* COMMENT, COST_LABEL *) #_ #EQ whd in EQ : (??%%); destruct(EQ) %{prf} //
1275  | (* MOVE *) #mv_sig #H lapply(err_eq_from_io ????? H) -H #H
1276    change with
1277     (pair_reg_move p (joint_closed_internal_function (make_sem_graph_params p p'))
1278                      (make_sem_graph_params p p') ??) in H : (??%?);
1279    lapply H -H
1280    whd in match pair_reg_move; normalize nodelta #H
1281    elim(bind_inversion ????? H) -H #reg * #reg_spec #EQ whd in EQ : (??%%); destruct(EQ)
1282    elim(pair_reg_move_commute ???????? (proj2 … (proj1 … prf)) reg_spec)
1283    #wf_regs #pm_spec >pm_spec >m_return_bind % [2: %]
1284    % [ 2: @(proj2 … prf)
1285      |    % [2: assumption] %
1286             [ @(proj1 … (proj1 … (proj1 … prf)))
1287             | @(proj2 … (proj1 … (proj1 … prf)))
1288             ]
1289      ]
1290  | (* POP *)
1291    #a #H lapply(err_eq_from_io ????? H) -H #H elim (bind_inversion ????? H) -H
1292    * #val #st1 * #vals_spec #H
1293    change with (acca_store p
1294                          (joint_closed_internal_function (make_sem_graph_params p p'))
1295                          (make_sem_graph_params p p') a val st1 = ?) in H;
1296    change with (pop (make_sem_graph_params p p') ? = ?) in vals_spec;
1297    lapply vals_spec -vals_spec
1298    whd in match pop; normalize nodelta
1299    whd in match is_pop; normalize nodelta
1300    lapply(proj2 … (proj1 … (proj1 … prf))) #wf_is
1301    inversion (istack (make_sem_graph_params p p') st) normalize nodelta
1302    [#_ #ABS normalize in ABS; destruct(ABS)]
1303    [ #Bv | #Bv_not_used #Bv] #is_stack_st_spec >m_return_bind
1304    #EQ whd in EQ : (??%%); destruct(EQ)
1305    elim(store_commute p p' graph_prog sigma ?? gss (acca_store__commute … gss) ?????? H)
1306    [ 2,5: @hide_prf >is_stack_st_spec in wf_is; #wf_is
1307           whd in match sigma_is_opt in wf_is; normalize nodelta in wf_is;
1308           inversion(sigma_beval_opt ?????)
1309           [1,3 : #EQ >EQ in wf_is; whd in ⊢ ((?(??%?)) → ?); * #ABS @⊥ @ABS //
1310                  inversion(sigma_beval_opt ?????) normalize nodelta
1311                  [ #bev %
1312                  | #bev #bev_s >bev_s in ABS; normalize nodelta
1313                    #ABS @⊥ @ABS normalize %
1314                  ]
1315           ]
1316           [#H1 #H2 % #ABS destruct(ABS) | #H1 #H2 % #ABS destruct(ABS)]
1317    ]
1318    [ 2,4: @hide_prf % [2,4 : @(proj2 … prf)] % [2,4 : @(proj2 … (proj1 … prf))]
1319             % [1,3 : @(proj1 … (proj1 … (proj1 … prf)))]
1320             whd in match sigma_is_opt; normalize nodelta
1321             [ whd in ⊢ (? (??%?)); % #ABS destruct(ABS)]
1322             >is_stack_st_spec in wf_is;
1323             whd in match sigma_is_opt; normalize nodelta
1324             cases(sigma_beval_opt ?????)
1325             [ normalize * #ABS @⊥ @ABS %
1326             | #bev #_ normalize % #ABS destruct(ABS)
1327             ]
1328     ] 
1329     #prf' #acca_store_commute %{prf'}     
1330    whd in match sigma_state in ⊢ (??(????(?????(?????%?)?))?);
1331    whd in match sigma_is; normalize nodelta
1332    @opt_safe_elim #int_stack #int_stack_sigma_spec
1333    >is_stack_st_spec in int_stack_sigma_spec;
1334    whd in match sigma_is_opt; normalize nodelta
1335    #IS_SPEC elim(bind_opt_inversion ????? IS_SPEC) -IS_SPEC
1336    [ #sigma_bv * #sigma_bv_spec #EQ whd in EQ : (??%%); destruct(EQ)
1337    | #sigma_bv_not_used * #sigma_bv_not_used_spec #IS_SPEC
1338      elim(bind_opt_inversion ????? IS_SPEC) -IS_SPEC
1339      #sigma_bv * #sigma_bv_spec #EQ whd in EQ : (??%%); destruct(EQ)]
1340      normalize nodelta >m_return_bind
1341      @err_eq_to_io <acca_store_commute
1342      whd in match helper_def_store; normalize nodelta
1343      whd in match acca_store; normalize nodelta
1344      whd in match sigma_beval; normalize nodelta
1345     @opt_safe_elim #xx #xx_spec
1346     [  >xx_spec in sigma_bv_spec; #EQ destruct(EQ) //
1347     | cut(xx =sigma_bv) [>xx_spec in sigma_bv_spec; #EQ destruct(EQ) %]
1348       #EQ >EQ @m_bind_ext_eq #reg
1349       change with (return set_regs (make_sem_lin_params p p') ?
1350                                   (set_istack (make_sem_lin_params p p') ? ?) = ?);
1351       change with (? = return set_regs ? ?
1352                   (sigma_state p p' graph_prog sigma gss
1353                   (set_istack ? (one_is Bv_not_used) st) ?))
1354       >(set_istack_sigma_commute ?????? (one_is Bv_not_used) (one_is sigma_bv_not_used) ???)
1355       [2: whd in match sigma_is_opt; normalize nodelta >sigma_bv_not_used_spec
1356           >m_return_bind whd in ⊢ (??%%); % | % |]
1357     ]
1358  | (* PUSH *)
1359     #a #H lapply(err_eq_from_io ????? H) -H #H elim (bind_inversion ????? H) -H
1360     #val *
1361     change with (((acca_arg_retrieve p
1362                (joint_closed_internal_function (make_sem_graph_params p p'))
1363                 (make_sem_graph_params p p') st a) = ?) → ?)
1364     #graph_ret_spec
1365     change with (((push (make_sem_graph_params p p') ? ?) = ?) → ?)
1366     #graph_push_spec
1367     elim (retrieve_commute p p' graph_prog sigma ?? gss (acca_arg_retrieve_commute … gss)??? prf graph_ret_spec)
1368     #val_wf #acca_arg_retrieve_commute
1369     whd in match push in graph_push_spec; normalize nodelta  in graph_push_spec;
1370     elim(bind_inversion ????? graph_push_spec) -graph_push_spec
1371     #int_stack * #int_stack_spec #EQ whd in EQ : (??%%); destruct(EQ)
1372     %
1373     [ @hide_prf % [% [% [ @(proj1 … (proj1 … (proj1 … prf))) ]]]
1374       [2: @(proj2 … (proj1 … prf))] [2: @(proj2 … prf)]
1375       lapply int_stack_spec -int_stack_spec
1376       cases int_stack
1377       [  whd in match is_push; normalize nodelta 
1378          cases(istack ? ?) normalize nodelta
1379          [2: #x ] [3: #x #y] #EQ whd in EQ : (??%%); destruct(EQ)
1380       |2,3: [#x | #y #x ] whd in match is_push; normalize nodelta
1381        inversion(istack ? ?) normalize nodelta
1382        [ #_ #EQ whd in EQ : (??%%); destruct(EQ)
1383           whd in match sigma_is_opt; normalize nodelta
1384           inversion(sigma_beval_opt ?????)
1385           [  #EQ @⊥ elim val_wf #H @H //
1386           |  #z #_ >m_return_bind % #ABS whd in ABS : (??%?); destruct(ABS)
1387           ]
1388        | #x #_ #ABS whd in ABS : (??%%); destruct(ABS)
1389        | #x #y #_ #ABS whd in ABS : (???%); destruct(ABS)
1390        | #_ #ABS whd in ABS : (??%%); destruct(ABS)
1391        | #z #H #EQ whd in EQ : (??%%); destruct(EQ)
1392          whd in match sigma_is_opt; normalize nodelta
1393          inversion(sigma_beval_opt ???? y)
1394          [ #ABS @⊥ lapply(proj2 … (proj1 … (proj1 … prf)))
1395           whd in match sigma_is_opt; >H normalize nodelta >ABS
1396           whd in ⊢ ((?(??%?))→?); * #h1 @h1 %
1397          | #sigma_y #H >m_return_bind
1398            cases (sigma_beval_opt ? ? ? ? x) in val_wf; [ * #ABS @⊥ @ABS %]
1399            #sigma_y' #_ >m_return_bind whd in ⊢ (?(??%?)); % #H destruct(H)
1400          ]
1401        | #a1 #a2 #_ #EQ whd in EQ : (???%); destruct(EQ)
1402          ]
1403        ]
1404     |
1405        whd in match helper_def_retrieve in acca_arg_retrieve_commute;
1406        normalize nodelta in acca_arg_retrieve_commute;
1407        whd in match acca_arg_retrieve; normalize nodelta
1408        @err_eq_to_io
1409        change with
1410        ((! v ← (acca_arg_retrieve_ p
1411                                      (joint_closed_internal_function (make_sem_lin_params p p'))
1412                                      (make_sem_lin_params p p')
1413                                      (regs (make_sem_lin_params p p')
1414                                         (sigma_state p p' graph_prog sigma gss st prf))
1415                                      a);
1416          ?)=?)
1417          change with ((! v ← ?; push (make_sem_lin_params p p') ? ?) = ?)
1418          cut((acca_arg_retrieve_ p ? ? ? a) = return sigma_beval p ? ? ? ? val_wf)
1419          [4: assumption | | | | ] #H >H >m_return_bind
1420          whd in match push; normalize nodelta
1421          -H elim(is_push_sigma_commute ???????? prf val_wf int_stack_spec)
1422          #wf_is #EQ >EQ >m_return_bind //
1423     ]
1424  | (*C_ADDRESS*)
1425    #sy
1426    change with ((member ? ? (prog_var_names (joint_function (mk_graph_params p)) ℕ graph_prog)) → ?)
1427    #sy_prf
1428    change with ((dpl_reg p) → ?) #dpl 
1429    change with ((dph_reg p) → ?) #dph
1430    #H lapply(err_eq_from_io ????? H) -H
1431    change with ((( ! st1 ← dpl_store p
1432                                     (joint_closed_internal_function (make_sem_graph_params p p'))
1433                                     (make_sem_graph_params p p')
1434                                     ?
1435                                     ?
1436                                     ? ; ? ) = ?) → ?)
1437    change with ((( ! st1 ← dpl_store ????
1438    (BVptr
1439      (mk_pointer
1440         (opt_safe block
1441           (find_symbol
1442              (fundef
1443                 (joint_closed_internal_function
1444                    (make_sem_graph_params p p')
1445                    ?
1446                  )
1447               )
1448               (globalenv_noinit ? graph_prog)
1449               ?
1450           )
1451           ?
1452         )
1453         ?
1454      )
1455      ?
1456    ) ? ; ?) = ?) → ?)
1457    change with ((( ! st1 ← ? ;
1458        dph_store p (joint_closed_internal_function (make_sem_graph_params p p'))
1459                  (make_sem_graph_params p p') ?
1460                  (BVptr
1461      (mk_pointer
1462         (opt_safe block
1463           (find_symbol
1464              (fundef
1465                 (joint_closed_internal_function
1466                    (make_sem_graph_params p p')
1467                    ?
1468                  )
1469               )
1470               (globalenv_noinit ? graph_prog)
1471               ?
1472           )
1473           ?
1474         )
1475         ?
1476      )
1477      ?
1478    ) ?) = ?) → ?)
1479    #H elim(bind_inversion ????? H) -H
1480    #st1 * #dpl_st1
1481    elim(store_commute p p' graph_prog sigma ?? gss (dpl_store_commute … gss) ???? prf ? dpl_st1)
1482    [2: @hide_prf whd in match sigma_beval_opt; normalize nodelta whd in ⊢ (?(??%?)); %
1483        #ABS destruct(ABS)]
1484    #wf_st1 whd in match helper_def_store; normalize nodelta
1485    #H elim(bind_inversion ????? H) -H #reg1 * #reg1_spec #EQ whd in EQ : (??%%);
1486    destruct(EQ) -EQ
1487    #dph_st'
1488    elim(store_commute p p' graph_prog sigma ?? gss (dph_store_commute … gss) ???? wf_st1 ? dph_st')
1489    [2: @hide_prf whd in match sigma_beval_opt; normalize nodelta whd in ⊢ (?(??%?));
1490        % #ABS destruct(ABS)]
1491    #wf_st' whd in match helper_def_store; normalize nodelta
1492    #H elim(bind_inversion ????? H) -H #reg2 * #reg2_spec #EQ whd in EQ : (??%%);
1493    destruct(EQ) -EQ %{wf_st'} <e1
1494    whd in match dpl_store; normalize nodelta
1495    whd in match sigma_beval in reg1_spec; normalize nodelta in reg1_spec;
1496    whd in match sigma_beval_opt in reg1_spec; normalize nodelta in reg1_spec;
1497    lapply reg1_spec -reg1_spec @opt_safe_elim #x #EQ whd in EQ : (??%?);
1498    destruct(EQ) @opt_safe_elim #block_graph #block_graph_spec
1499    #reg1_spec @opt_safe_elim #block_lin #block_lin_spec
1500    cut(find_symbol
1501         (fundef
1502            (joint_closed_internal_function
1503                (make_sem_lin_params p p')
1504                (prog_var_names (joint_function (mk_lin_params p)) ℕ (linearise … graph_prog))
1505            )
1506          )
1507          (globalenv_noinit (joint_function (mk_lin_params p)) (linearise … graph_prog))
1508          sy
1509          =
1510          find_symbol
1511            (fundef
1512               (joint_closed_internal_function
1513                   (make_sem_graph_params p p')
1514                   (prog_var_names (joint_function (mk_graph_params p)) ℕ graph_prog)
1515               )
1516            )
1517            (globalenv_noinit (joint_function (mk_graph_params p)) graph_prog)
1518            sy)   
1519    [ @find_symbol_transf]
1520    #find_sym_EQ >find_sym_EQ in block_lin_spec; >block_graph_spec
1521    #EQ destruct(EQ) >reg1_spec >m_return_bind
1522    whd in match dph_store; normalize nodelta
1523    lapply reg2_spec -reg2_spec
1524    whd in match sigma_beval; normalize nodelta
1525    @opt_safe_elim #y
1526    whd in match sigma_beval_opt; normalize nodelta
1527    whd in ⊢((??%?)→?); #EQ destruct(EQ)
1528    @opt_safe_elim #graph_block >block_graph_spec
1529    #EQ destruct(EQ) #reg2_spec
1530    cut(sigma_state p p' graph_prog sigma gss st1 wf_st1 =
1531    (set_regs (lin_prog_params p p' (linearise p graph_prog) stack_sizes)
1532          reg1 (sigma_state p p' graph_prog sigma gss st prf)))
1533    [whd in match set_regs; normalize nodelta >e0 %]
1534    #sigma_st1_spec <sigma_st1_spec >reg2_spec
1535    >m_return_bind %
1536  | (*C_OPACCS*)
1537    #op #a #b #arg1 #arg2
1538    #H lapply(err_eq_from_io ????? H) -H
1539    #H elim(bind_inversion ????? H) -H
1540    #val1 * #val1_spec
1541    elim (retrieve_commute p p' graph_prog sigma ?? gss (acca_arg_retrieve_commute … gss)??? prf val1_spec)
1542    #wf_val1 #sigma_val1_commute
1543    #H elim(bind_inversion ????? H) -H
1544    #val2 * #val2_spec
1545    elim (retrieve_commute p p' graph_prog sigma ?? gss (accb_arg_retrieve_commute … gss)??? prf val2_spec)
1546    #wf_val2 #sigma_val2_commute
1547    #H elim(bind_inversion ????? H) -H *
1548    #opaccs1 #opaccs2 * #opaccs_spec
1549    elim(beopaccs_sigma_commute p p' graph_prog sigma ????? wf_val1 wf_val2 opaccs_spec)
1550    #wf_opaccs1 * #wf_opaccs2 #be_opaccs_commute
1551    #H elim(bind_inversion ????? H) -H
1552    #st1 * #st1_spec
1553    elim(store_commute p p' graph_prog sigma ?? gss (acca_store__commute … gss) ???? prf wf_opaccs1 st1_spec)
1554    #wf_st1 #sigma_st1_commute #final_spec
1555    elim(store_commute p p' graph_prog sigma ?? gss (accb_store_commute … gss) ???? wf_st1 wf_opaccs2 final_spec)
1556    #wf_st' #sigma_final_commute
1557    %{wf_st'}
1558    whd in match helper_def_retrieve in sigma_val1_commute;
1559    normalize nodelta in sigma_val1_commute;
1560    whd in match acca_arg_retrieve; normalize nodelta
1561    >sigma_val1_commute >m_return_bind
1562    whd in match helper_def_retrieve in sigma_val2_commute;
1563    normalize nodelta in sigma_val2_commute;
1564    whd in match accb_arg_retrieve; normalize nodelta
1565    >sigma_val2_commute >m_return_bind
1566    >be_opaccs_commute >m_return_bind
1567    whd in match helper_def_store in sigma_st1_commute;
1568    normalize nodelta in sigma_st1_commute;
1569    elim(bind_inversion ????? sigma_st1_commute)
1570    #reg1 * #reg1_spec #EQ whd in EQ : (??%%); destruct(EQ)
1571    whd in match acca_store; normalize nodelta
1572    >reg1_spec >m_return_bind
1573    whd in match set_regs; normalize nodelta >e0
1574    whd in match helper_def_store in sigma_final_commute;
1575    normalize nodelta in sigma_final_commute;
1576    elim(bind_inversion ????? sigma_final_commute)
1577    #reg2 * #reg2_spec #EQ whd in EQ : (??%%); destruct(EQ)
1578    whd in match accb_store; normalize nodelta
1579    >reg2_spec >m_return_bind whd in match set_regs; normalize nodelta
1580    >e1 %
1581  | (*C_OP1*)
1582   
1583inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
1584    ex1_intro: ∀ x:A. P x →  ex_Type1 A P.
1585(*interpretation "exists in Type[1]" 'exists x = (ex_Type1 ? x).*)
1586
1587lemma linearise_ok:
1588 ∀p,p',graph_prog.
1589  let lin_prog ≝ linearise ? graph_prog in
1590 ∀lin_stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
1591 let graph_stack_sizes ≝
1592  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
1593    ? graph_prog lin_stack_sizes in
1594 (∀sigma.good_sigma_state p p' graph_prog sigma) →
1595   ex_Type1 … (λR.
1596   status_simulation
1597    (graph_abstract_status p p' graph_prog graph_stack_sizes)
1598    (lin_abstract_status p p' lin_prog lin_stack_sizes) R).
1599 #p #p' #graph_prog
1600 cases (linearise_spec … graph_prog) #sigma #good
1601 #lin_stack_sizes
1602 #gss lapply (gss sigma) -gss #gss
1603 %{(linearise_status_rel p p' graph_prog lin_stack_sizes sigma gss good)}
1604whd in match graph_abstract_status;
1605whd in match lin_abstract_status;
1606whd in match graph_prog_params;
1607whd in match lin_prog_params;
1608normalize nodelta
1609whd
1610whd in ⊢ (%→%→%→?);
1611whd in ⊢ (?(?%)→?(?%)→?(?%)→?);
1612whd in ⊢ (?%→?%→?%→?);
1613#st1 #st1' #st2
1614whd in ⊢ (%→?);
1615change with
1616  (eval_state (make_sem_graph_params p p') (prog_var_names ???) ?? = ? → ?)
1617whd in match eval_state in ⊢ (%→?); normalize nodelta
1618change with (Σi.is_internal_function_of_program ? graph_prog i) in
1619match (Sig ??) in ⊢ (%→?);
1620letin globals ≝ (prog_var_names ?? graph_prog)
1621change with (fetch_statement ??? (globalenv_noinit ? graph_prog) ?) in
1622  match (fetch_statement ?????) in ⊢ (%→?);
1623#ex
1624cases (IO_bind_inversion ??????? ex) in ⊢ ?; * #fn #stmt * -ex
1625#EQfetch lapply (err_eq_from_io ????? EQfetch) -EQfetch
1626#EQfetch
1627cases (bind_inversion ????? EQfetch)
1628#f_id * #H lapply (opt_eq_from_res ???? H) -H
1629#EQfunc_of_block
1630#H elim (bind_inversion ????? H) -H #stmt' *
1631#H lapply (opt_eq_from_res ???? H) -H #EQstmt_at
1632whd in ⊢ (??%%→?); #EQ destruct(EQ)
1633#EQeval
1634cases (good fn (pi2 … (sigma_function_name p graph_prog fn)))
1635letin graph_fun ≝ (if_of_function … fn) in EQstmt_at; #EQstmt_at
1636#entry_0
1637#good_local
1638* * #wf_pc #wf_state #EQst2
1639generalize in match wf_pc in ⊢ ?;
1640whd in ⊢ (%→?);
1641inversion (sigma_pc_opt ?????) in ⊢ (%→?); [ #_ * #ABS elim (ABS ?) % ]
1642#lin_pc
1643whd in match (sigma_pc_opt) in ⊢ (%→?); normalize nodelta
1644>EQfunc_of_block in ⊢ (%→?); >m_return_bind in ⊢ (%→?);
1645#H elim (bind_opt_inversion ????? H) in ⊢ ?; -H #lin_pt *
1646#EQsigma whd in ⊢ (??%?→?); #EQ destruct(EQ) #_
1647elim (good_local … EQsigma) -good_local
1648#stmt' *
1649change with (stmt_at ?? (joint_if_code ?? graph_fun) ? = ? → ?)
1650>EQstmt_at #EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ)
1651#H elim (opt_Exists_elim … H) -H * #lbl_opt #lin_stmt normalize nodelta
1652>(prog_if_of_function_transform … fn) in ⊢ (%→?); [2: % ]
1653change with graph_fun in match (if_of_function ?? fn) in ⊢ (%→?);
1654letin lin_fun ≝ (\fst  (linearise_int_fun p globals graph_fun))
1655change with globals in match (prog_var_names ?? graph_prog) in ⊢ (%→?);
1656*
1657#EQnth_opt ** #opt_lbl_spec #EQ destruct(EQ) #next_spec
1658letin lin_prog ≝ (linearise … graph_prog)
1659lapply (refl … (eval_state ? globals (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) st2))
1660destruct(EQst2)
1661whd in match eval_state in ⊢ (???%→?); normalize nodelta
1662letin st2 ≝ (sigma_state_pc ????? st1 ?)
1663>(fetch_statement_sigma_commute … good … EQfetch) in ⊢ (%→?);
1664>m_return_bind in ⊢ (%→?);
1665#ex'
1666(* resolve classifier *)
1667whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
1668>EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
1669normalize nodelta
1670cases stmt in EQfetch EQeval EQstmt_at EQnth_opt next_spec ex';
1671[ *
1672  [ #stmt #nxt
1673    whd in match eval_statement in ⊢ (?→%→?); normalize nodelta
1674    #EQfetch #EQeval #EQstmt_at #EQnth_opt #next_spec
1675    whd in match (graph_to_lin_statement ???) in ⊢ (%→?);
1676    whd in match eval_statement in ⊢ (%→?); normalize nodelta
1677    elim (IO_bind_inversion ??????? EQeval) #st1_no_pc *
1678    #EQeval_no_pc #EQeval_pc
1679    >(eval_seq_no_pc_sigma_commute … EQeval_no_pc)
1680    [2: (*TODO lemma eval_seq_no_pc_wf *) @hide_prf cases daemon ]
1681        >m_return_bind
1682    cases stmt in EQfetch EQeval_no_pc EQeval_pc EQstmt_at EQnth_opt next_spec;
1683    [14: #f #args #dest
1684    | #c
1685    | #lbl
1686    | #move_sig
1687    | #a
1688    | #a
1689    | #sy #sy_prf #dpl #dph
1690    | #op #a #b #arg1 #arg2
1691    | #op #a #arg
1692    | #op #a #arg1 #arg2
1693    ||
1694    | #a #dpl #dph
1695    | #dpl #dph #a
1696    | #s_ext
1697    ]
1698    [ (* CALL *)
1699    |(*:*)
1700      normalize nodelta
1701      #EQfetch #EQeval_no_pc #EQeval_pc #EQstmt_at #EQnth_opt #next_spec
1702      whd in match eval_seq_pc; normalize nodelta
1703      #ex1
1704      cases next_spec
1705      [ #EQnext_sigma
1706        %[2: %{(taaf_step … (taa_base …) ex1 ?)}
1707         [ cases daemon (* TODO lemma joint_classify_sigma_commute *) ]|]
1708        normalize nodelta
1709        cut (? : Prop) [3: #R' % [ %{I R'} ] |*:]
1710        [ cases daemon (* TODO lemma joint_label_sigma_commute *)
1711        | %
1712          [ (* TODO lemma well_formed_state_pc_preserve? *) @hide_prf cases daemon
1713          | whd in match eval_seq_pc in EQeval_pc;
1714            whd in EQeval_pc : (??%%); whd in EQeval_pc : (??(????%)?);
1715            destruct (EQeval_pc)
1716            whd in ⊢ (??%%);
1717            change with (sigma_pc ??????) in match
1718              (pc ? (sigma_state_pc ???????));
1719            whd in match (succ_pc ????) in ⊢ (??%%);
1720            whd in match (point_of_succ ???) in ⊢ (??%%);
1721            >(point_of_pc_sigma_commute … EQfunc_of_block EQsigma)
1722            whd in match sigma_pc in ⊢ (???%);
1723            whd in match sigma_pc_opt in ⊢ (???%); normalize nodelta
1724            @opt_safe_elim #pc'
1725            >EQfunc_of_block >m_return_bind
1726            whd in match point_of_pc; normalize nodelta
1727            >point_of_offset_of_point
1728            >EQnext_sigma whd in ⊢ (??%?→?);
1729            whd in match pc_of_point; normalize nodelta
1730            #EQ destruct(EQ)
1731            >sigma_pblock_eq_lemma %
1732          ]
1733        ]
1734      | -next_spec #next_spec
1735        %
1736     
1737     
1738        whd in ⊢ (?→???%→?);
1739        generalize in ⊢ (??%? → ???(????%) → ?); |*: skip]  | #a #lbltrue #next
1740  ] #next change with label in next;
1741| *
1742  [ #lbl
1743  |
1744  | #fl #f #args
1745  ]
1746]
1747whd in match eval_statement in ⊢ (?→%→?); normalize nodelta
1748#EQfetch #EQeval #EQstmt_at #EQnth_opt #next_spec
1749normalize nodelta
1750whd in match (graph_to_lin_statement ???) in ⊢ (%→?);
1751whd in match eval_statement in ⊢ (%→?); normalize nodelta
1752[ >m_return_bind in ⊢ (%→?);
1753  >m_return_bind in EQeval;
1754
1755
1756
1757  (* common for all non-call seq *)
1758  >m_return_bind in ⊢ (%→?);
1759  whd in ⊢ (??%%→?); #EQ destruct(EQ)
1760  >m_return_bind in ⊢ (%→?);
1761
1762 
1763  #ex1
1764lapply (refl … (eval_state ? globals (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) st2))
1765
1766whd in match (point_of_pc ???);
1767whd in match (point_of_succ ???);
1768whd in match sigma_pc in ⊢ (???%); normalize nodelta @opt_safe_elim
1769#pc' #H
1770elim (bind_opt_inversion ????? H) #fn * #EQbl
1771-H #H 
1772elim (bind_opt_inversion ????? H) -H #n * #EQsigma whd in ⊢ (??%?→?);
1773#EQ destruct(EQ)
1774whd in match (succ_pc ????);
1775whd in match (point_of_succ ???);
1776change with (point_of_offset ???) in match (point_of_pc ???);
1777>point_of_offset_of_point
1778whd in match sigma_pc; normalize nodelta @opt_safe_elim
1779#pc' whd in match sigma_pc_opt; normalize nodelta
1780
1781 
1782 
1783        whd in match (succ_pc ????);
1784               
1785        change with next in match (offset_of_point ???) in ⊢ (???%);
1786whd in fetch_statement_spec : (??()%);
1787cases cl in classified_st1_cl; -cl #classified_st1_cl whd
1788[4:
1789 >rel_st1_st2 -st2 letin lin_prog ≝ (linearise ? graph_prog)
1790 cases (good (pi1 ?? fn)) [2: cases daemon (* TODO *) ]
1791 #sigma_entry_is_zero #sigma_spec
1792 lapply (sigma_spec (point_of_pc … (make_sem_graph_params … p') (pc … st1)))
1793 -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @opt_to_opt_safe cases daemon (* TO REDO *) |2: skip ]
1794 -sigma_spec #graph_stmt * #graph_lookup_ok #sigma_spec
1795 cases (opt_Exists_elim … sigma_spec) in ⊢ ?;
1796 * #optlabel #lin_stm * #lin_lookup_ok whd in ⊢ (% → ?); ** #labels_preserved
1797 #related_lin_stm_graph_stm
1798 
1799 inversion (stmt_implicit_label ???)
1800 [ whd in match (opt_All ???); #stmt_implicit_spec #_
1801   letin st2_opt' ≝ (eval_state …
1802               (ev_genv (lin_prog_params … lin_prog lin_stack_sizes))
1803               (sigma_state_pc … wf_st1))
1804   cut (∃st2': lin_abstract_status p p' lin_prog lin_stack_sizes. st2_opt' = return st2')
1805   [cases daemon (* TODO, needs lemma? *)] * #st2' #st2_spec'
1806   normalize nodelta in st2_spec'; -st2_opt'
1807   %{st2'} %{(taaf_step … (taa_base …) …)}
1808   [ cases daemon (* TODO, together with the previous one? *)
1809   | @st2_spec' ]
1810   %[%] [%]
1811   [ whd whd in match eval_state in st2_spec'; normalize nodelta in st2_spec';
1812     >(fetch_statement_sigma_commute … good … fetch_statement_spec) in st2_spec';
1813     >m_return_bind
1814     (* Case analysis over the possible statements *)
1815     inversion graph_stmt in stmt_implicit_spec; normalize nodelta
1816     [ #stmt #lbl #_ #abs @⊥ normalize in abs; destruct(abs) ]
1817     XXXXXXXXXX siamo qua, caso GOTO e RETURN
1818   | cases daemon (* TODO, after the definition of label_rel, trivial *) ]
1819   ]
1820 | ....
1821qed.
1822
1823
1824
1825
1826
1827[ *
1828  [ *
1829    [ letin C_COMMENT ≝ 0 in ⊢ ?; #c
1830    | letin C_COST_LABEL ≝ 0 in ⊢ ?; #lbl
1831    | letin C_MOVE       ≝ 0 in ⊢ ?; #move_sig
1832    | letin C_POP        ≝ 0 in ⊢ ?; #a
1833    | letin C_PUSH       ≝ 0 in ⊢ ?; #a
1834    | letin C_ADDRESS    ≝ 0 in ⊢ ?; #sy #sy_prf #dpl #dph
1835    | letin C_OPACCS     ≝ 0 in ⊢ ?; #op #a #b #arg1 #arg2
1836    | letin C_OP1        ≝ 0 in ⊢ ?; #op #a #arg
1837    | letin C_OP2        ≝ 0 in ⊢ ?; #op #a #arg1 #arg2
1838    | letin C_CLEAR_CARRY ≝ 0 in ⊢ ?;
1839    | letin C_SET_CARRY  ≝ 0 in ⊢ ?;
1840    | letin C_LOAD       ≝ 0 in ⊢ ?; #a #dpl #dph
1841    | letin C_STORE      ≝ 0 in ⊢ ?; #dpl #dph #a
1842    | letin C_CALL       ≝ 0 in ⊢ ?; #f #args #dest
1843    | letin C_EXT        ≝ 0 in ⊢ ?; #s_ext
1844    ]
1845  | letin C_COND ≝ 0 in ⊢ ?; #a #lbltrue
1846  ] #next change with label in next;
1847| *
1848  [ letin C_GOTO ≝ 0 in ⊢ ?; #lbl
1849  | letin C_RETURN ≝ 0 in ⊢ ?;
1850  | letin C_TAILCALL ≝ 0 in ⊢ ?; #fl #f #args
1851  ]
1852]
Note: See TracBrowser for help on using the repository browser.