source: src/joint/lineariseProof.ma @ 2464

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

adapted lineariseProof to new semantics

File size: 19.5 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 good_local_sigma :
21  ∀p:unserialized_params.
22  ∀p':(∀F.sem_unserialized_params p F).
23  ∀globals.
24  joint_closed_internal_function (mk_graph_params p) globals →
25  (label → option ℕ) → Prop ≝
26  λp,p',globals,graph_fun,sigma.
27   let lin_fun ≝ linearise_int_fun … graph_fun in
28   let g ≝ joint_if_code ?? (pi1 … graph_fun) in
29   let c ≝ joint_if_code ?? (pi1 … lin_fun) in
30   ∀entry : (Σl.bool_to_Prop (code_has_label … g l)).
31        code_closed … c ∧
32        sigma entry = Some ? 0 ∧
33        ∀l,n.sigma l = Some ? n →
34          lt n 2^offset_size →
35          ∃s. lookup … g l = Some ? s ∧
36            opt_Exists ?
37              (λls.let 〈lopt, ts〉 ≝ ls in
38                opt_All ? (eq ? l) lopt ∧
39                ts = graph_to_lin_statement … s ∧
40                opt_All ?
41                  (λnext.Or (sigma next = Some ? (S n))
42                  (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉))
43                  (stmt_implicit_label … s)) (nth_opt … n c).
44
45axiom prog_if_of_function :
46  ∀p.∀prog : joint_program p.
47  (Σi.is_internal_function_of_program … prog i) →
48    joint_closed_internal_function p (prog_var_names … prog).
49
50definition if_in_global_env_to_if_in_prog :
51  ∀prog_pars : prog_params.∀f : Σi.is_internal_function … (ev_genv prog_pars) i.
52  Σi.is_internal_function_of_program ? (prog prog_pars) i ≝
53  λprog_pars,f.pi1 ?? f.
54@is_internal_function_of_program_ok @(pi2 … f) qed.
55
56coercion if_in_prog_from_if_in_global_env nocomposites :
57  ∀prog_pars : prog_params.∀f : Σi.is_internal_function … (ev_genv prog_pars) i.
58  Σi.is_internal_function_of_program ? (prog prog_pars) i ≝
59  if_in_global_env_to_if_in_prog
60  on _f : Sig ident (λi.is_internal_function ??? i)
61  to Sig ident (λi.is_internal_function_of_program ?? i).
62
63definition good_sigma :
64  ∀p:unserialized_params.
65  ∀p':(∀F.sem_unserialized_params p F).
66  ∀prog : joint_program (mk_graph_params p).
67  ((Σi.is_internal_function_of_program … prog i) → label → option ℕ) → Prop ≝
68  λp,p',graph_prog,sigma.
69  ∀i.
70  let graph_fun ≝ prog_if_of_function ?? i in
71  let sigma_local ≝ sigma i in
72  good_local_sigma ? p' ? graph_fun sigma_local.
73
74definition graph_prog_params ≝
75λp,p',prog,stack_sizes.
76mk_prog_params (make_sem_graph_params p p') prog stack_sizes.
77
78definition graph_abstract_status:
79 ∀p:unserialized_params.
80  (∀F.sem_unserialized_params p F) →
81    ∀prog : joint_program (mk_graph_params p).
82  ((Σi.is_internal_function_of_program … prog i) → ℕ) →
83     abstract_status
84 ≝
85 λp,p',prog,stack_sizes.
86 joint_abstract_status (graph_prog_params ? p' prog stack_sizes).
87
88definition lin_prog_params ≝
89λp,p',prog,stack_sizes.
90mk_prog_params (make_sem_lin_params p p') prog stack_sizes.
91
92definition lin_abstract_status:
93 ∀p:unserialized_params.
94  (∀F.sem_unserialized_params p F) →
95    ∀prog : joint_program (mk_lin_params p).
96  ((Σi.is_internal_function_of_program … prog i) → ℕ) →
97     abstract_status
98 ≝
99 λp,p',prog,stack_sizes.
100 joint_abstract_status (lin_prog_params ? p' prog stack_sizes).
101
102definition sigma_pc_opt:
103 ∀p,p',graph_prog,stack_sizes.
104  ((Σi.is_internal_function_of_program … graph_prog i) →
105    code_point (mk_graph_params p) → option ℕ) →
106   cpointer → option cpointer
107 ≝
108  λp,p',prog,stack_sizes,sigma,pc.
109  let pars ≝ graph_prog_params p p' prog stack_sizes in
110  let ge ≝ ev_genv pars in
111  ! f ← int_funct_of_block ?? ge (pblock pc) ;
112  ! lin_point ← sigma f (point_of_pointer … pars pc) ;
113  res_to_opt … (pointer_of_point ? (make_sem_lin_params ? p') pc lin_point).
114
115definition well_formed_pc:
116 ∀p,p',graph_prog,stack_sizes.
117  ((Σi.is_internal_function_of_program … graph_prog i) →
118    label → option ℕ) →
119   cpointer → Prop
120 ≝
121 λp,p',prog,stack_sizes,sigma,pc.
122  sigma_pc_opt p p' prog stack_sizes sigma pc
123   ≠ None ….
124
125definition well_formed_status:
126 ∀p,p',graph_prog,stack_sizes.
127  ((Σi.is_internal_function_of_program … graph_prog i) →
128    label → option ℕ) →
129  state_pc (make_sem_graph_params p p') → Prop ≝
130 λp,p',prog,stack_sizes,sigma,st.
131 well_formed_pc p p' prog stack_sizes sigma (pc … st) ∧ ?.
132cases daemon (* TODO *)
133qed.
134
135(*
136lemma prova : ∀p,s,st,prf.sigma_pc_of_status p s st prf = ?.
137[ #p #s #st #prf
138  whd in match sigma_pc_of_status; normalize nodelta
139  @opt_safe_elim
140  #n
141  lapply (refl …  (int_funct_of_block (joint_closed_internal_function p) (globals p)
142        (ev_genv p) (pblock (pc p st))))
143  elim (int_funct_of_block (joint_closed_internal_function p) (globals p)
144        (ev_genv p) (pblock (pc p st))) in ⊢ (???%→%);
145  [ #_ #ABS normalize in ABS; destruct(ABS) ]
146  #f #EQ >m_return_bind
147*)
148
149
150(*
151lemma wf_status_to_wf_pc :
152∀p,p',graph_prog,stack_sizes.
153∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) →
154    code_point (mk_graph_params p) → option ℕ).
155∀st.
156well_formed_status p p' graph_prog stack_sizes sigma st →
157well_formed_pc p p' graph_prog stack_sizes sigma (pc ? st).
158#p #p' #graph_prog #stack_sizes #sigma #st whd in ⊢ (% → ?); * #H #_ @H
159qed.
160
161lemma sigma_pc_of_status_ok:
162  ∀p,p',graph_prog,stack_sizes.
163  ∀sigma.
164   ∀st.
165    ∀prf:well_formed_status p p' graph_prog stack_sizes sigma st.
166    sigma_pc_opt p p' graph_prog stack_sizes sigma (pc ? st) =
167    Some … (sigma_pc_of_status p p' graph_prog stack_sizes sigma st prf).
168    #p #p' #graph_prog #stack_sizes #sigma #st #prf @opt_to_opt_safe qed.
169
170*)
171
172definition sigma_pc :
173∀p,p',graph_prog,stack_sizes.
174∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) →
175    label → option ℕ).
176∀pc.
177∀prf : well_formed_pc p p' graph_prog stack_sizes sigma pc.
178cpointer ≝
179λp,p',graph_prog,stack_sizes,sigma,st.opt_safe ….
180
181definition sigma_state :
182 ∀p.
183 ∀p':∀F.sem_unserialized_params p F.
184 ∀graph_prog,stack_sizes.
185  ∀sigma.
186(*   let lin_prog ≝ linearise ? graph_prog in *)
187    ∀s:state_pc (p' ?). (* = graph_abstract_status p p' graph_prog stack_sizes *)
188     well_formed_status p p' graph_prog stack_sizes sigma s →
189      state_pc (make_sem_lin_params p p') (* = lin_abstract_status p p' lin_prog ? *)
190
191 λp,p',graph_prog,stack_sizes,sigma,s,prf.
192 let pc' ≝ sigma_pc … (proj1 … prf) in
193 mk_state_pc ? ? pc'.
194 cases daemon (* TODO *) qed.
195
196lemma sigma_pc_commute:
197 ∀p,p',graph_prog,stack_sizes,sigma,st.
198 ∀prf : well_formed_status p p' graph_prog stack_sizes sigma st.
199 sigma_pc … (pc ? st) (proj1 … prf) =
200 pc ? (sigma_state … st prf).
201#p #p' #prog #stack_sizes #sigma #st #prf %
202qed.
203
204lemma res_eq_from_opt :
205  ∀A,m,v.res_to_opt A m = return v → m = return v.
206#A * #x #v normalize #EQ destruct % qed.
207
208lemma if_propagate :
209∀pars_in, pars_out : sem_params.
210∀trans : ∀globals.joint_closed_internal_function pars_in globals →
211                  joint_closed_internal_function pars_out globals.
212∀prog_in : program (joint_function pars_in) ℕ.
213let prog_out ≝
214  transform_program … prog_in (λglobals.transf_fundef ?? (trans globals)) in
215∀i.is_internal_function_of_program … prog_in i →
216is_internal_function_of_program … prog_out i.
217cases daemon (* TODO by paolo *) qed.
218
219definition stack_sizes_lift :
220∀pars_in, pars_out : sem_params.
221∀trans : ∀globals.joint_closed_internal_function pars_in globals →
222                  joint_closed_internal_function pars_out globals.
223∀prog_in : program (joint_function pars_in) ℕ.
224let prog_out ≝
225  transform_program … prog_in (λglobals.transf_fundef ?? (trans globals)) in
226((Σi.is_internal_function_of_program … prog_out i) → ℕ) →
227((Σi.is_internal_function_of_program … prog_in i) → ℕ) ≝
228λpars_in,pars_out,prog_in,trans,stack_sizes.
229λi.stack_sizes «i, if_propagate … (pi2 … i)».
230
231axiom ok_is_internal_function_of_program :
232  ∀p.∀prog:joint_program p.∀i.
233  is_internal_function_of_program p prog i →
234  is_internal_function ?? (globalenv_noinit ? prog) i.
235
236
237definition sigma_function_name :
238 ∀p,p',graph_prog.
239 let lin_prog ≝ linearise p graph_prog in
240 ∀lin_stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
241 let graph_stack_sizes ≝
242  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
243    ? graph_prog lin_stack_sizes in
244  (Σf.is_internal_function … (ev_genv (graph_prog_params p p' graph_prog graph_stack_sizes)) f) →
245  (Σf.is_internal_function … (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) f) ≝
246λp,p',graph_prog,lin_stack_sizes,f.pi1 … f.
247@ok_is_internal_function_of_program
248@(if_propagate (make_sem_graph_params p p') (make_sem_lin_params p p'))
249@is_internal_function_of_program_ok
250@(pi2 … f)
251qed.
252
253lemma fetch_function_sigma_commute :
254 ∀p,p',graph_prog.
255 let lin_prog ≝ linearise p graph_prog in
256 ∀lin_stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
257 let graph_stack_sizes ≝
258  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
259    ? graph_prog lin_stack_sizes in
260 ∀sigma,pc,f.
261  ∀prf : well_formed_pc p p' graph_prog graph_stack_sizes sigma pc.
262 fetch_function … (ev_genv (graph_prog_params p p' graph_prog graph_stack_sizes)) pc =
263  return f
264→ fetch_function … (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) (sigma_pc … pc prf) =
265  return sigma_function_name … f.
266 #p #p' #graph_prog #stack_sizes #sigma #pc #f #prf
267(* whd in match fetch_function; normalize nodelta
268whd in match function_of_block; normalize nodelta
269#H elim (bind_inversion ????? H) -H #fn *
270#H lapply (opt_eq_from_res ???? H) -H
271#H >(find_funct_ptr_transf … (λglobals.transf_fundef … (linearise_int_fun … globals)) … H)
272-H #H >m_return_bind cases fn in H; normalize nodelta #arg #EQ whd in EQ:(??%%);
273destruct // *)
274cases daemon
275qed.
276
277lemma if_of_function_commute:
278 ∀p,p',graph_prog,stack_sizes.
279 ∀graph_fun.
280 let graph_fd ≝ if_of_function ??? graph_fun in
281 let lin_fun ≝ sigma_function_name p p' graph_prog stack_sizes graph_fun in
282 let lin_fd ≝ if_of_function … lin_fun in
283 lin_fd = linearise_int_fun … graph_fd.
284(* usare match_opt_prf_elim ? *)
285cases daemon qed.
286
287lemma stmt_at_sigma_commute:
288 ∀p,p',graph_prog,stack_sizes,graph_fun,lbl.
289 let lin_prog ≝ linearise ? graph_prog in
290 let lin_fun ≝ sigma_function_name p p' graph_prog stack_sizes graph_fun in
291 ∀sigma.good_sigma p p' graph_prog sigma →
292 ∀prf:sigma graph_fun lbl ≠ None ….
293 ∃stmt.
294   stmt_at …
295    (joint_if_code ?? (if_of_function ??? graph_fun)) 
296    lbl = Some ? stmt ∧
297   stmt_at …
298    (joint_if_code ?? (if_of_function ??? lin_fun))
299    (opt_safe … (sigma graph_fun lbl) prf) = Some ? (graph_to_lin_statement … stmt). 
300 #p #p' #graph_prog #stack_sizes #graph_fun #lbl #sigma #good #prf
301 @opt_safe_elim -prf #n #prf
302 (*
303 whd in match (stmt_at ????);
304 whd in match (stmt_at ????);
305 cases (linearise_code_spec … p' graph_prog graph_fun
306         (joint_if_entry … graph_fun))
307 * #lin_code_closed #sigma_entry_is_zero #sigma_spec
308 lapply (sigma_spec
309         (point_of_pointer ? (graph_prog_params … p' graph_prog) (pc … s1)))
310 -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @(sigma_pc_of_status_ok … prf) |2: skip ]
311 -sigma_spec #graph_stmt * #graph_lookup_ok >graph_lookup_ok -graph_lookup_ok
312 whd in ⊢ (? → ???%); #sigma_spec whd in sigma_spec;
313 inversion (nth_opt ???) in sigma_spec; [ #H whd in ⊢ (% → ?); #abs cases abs ]
314 * #optlabel #lin_stm #lin_lookup_ok whd in ⊢ (% → ?); ** #_
315 #related_lin_stm_graph_stm #_ <related_lin_stm_graph_stm -related_lin_stm_graph_stm
316 <sigma_pc_commute >lin_lookup_ok // *)
317 cases daemon
318qed.
319
320lemma fetch_statement_sigma_commute:
321  ∀p,p',graph_prog,lin_stack_sizes,pc,fn,stmt.
322  let lin_prog ≝ linearise ? graph_prog in
323  let graph_stack_sizes ≝
324   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
325    ? graph_prog lin_stack_sizes in
326  ∀sigma.good_sigma p p' graph_prog sigma →
327  ∀prf : well_formed_pc p p' graph_prog graph_stack_sizes sigma pc.
328  fetch_statement ? (make_sem_graph_params p p') … (ev_genv (graph_prog_params p p' graph_prog graph_stack_sizes)) pc =
329    return 〈fn,stmt〉 →
330  fetch_statement ? (make_sem_lin_params p p') … (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes))
331   (sigma_pc … pc prf) =
332    return 〈sigma_function_name … fn, graph_to_lin_statement … stmt〉.
333 #p #p' #graph_prog #stack_sizes #pc #fn #stmt #good #prf
334(* @opt_safe_elim -prf #n #prf
335 whd in match fetch_statement; normalize nodelta
336 >fetch_function_sigma_commute
337 cases (fetch_function ????) [2://]
338 #graph_fun whd in ⊢ (??%%);
339 whd in ⊢ (???(match % with [ _ ⇒ ? | _ ⇒ ?]));
340 >stm_at_sigma_commute cases (stmt_at ????) // *)
341cases daemon
342qed.
343
344definition linearise_status_rel:
345 ∀p,p',graph_prog.
346 let lin_prog ≝ linearise p graph_prog in
347 ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
348 let stack_sizes' ≝
349  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
350    ? graph_prog stack_sizes in
351 ∀sigma.
352 good_sigma p p' graph_prog sigma →
353   status_rel
354    (graph_abstract_status p p' graph_prog stack_sizes')
355    (lin_abstract_status p p' lin_prog stack_sizes)
356 ≝ λp,p',graph_prog,stack_sizes,sigma,good.
357   let stack_sizes' ≝
358    stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
359      ? graph_prog ? in
360   mk_status_rel …
361    (* sem_rel ≝ *) (λs1,s2.
362     ∃prf: well_formed_status p p' graph_prog stack_sizes' sigma s1.
363      s2 = sigma_state … s1 prf)
364    (* call_rel ≝ *) (λs1,s2.
365      ∃prf:well_formed_status p p' graph_prog stack_sizes' sigma s1.
366      pc ? s2 = sigma_pc … (pc ? s1) (proj1 … prf))
367    (* sim_final ≝ *) ?.
368#st1 #st2 * #prf #EQ2
369%
370whd in ⊢ (%→%);
371#H lapply (opt_to_opt_safe … H)
372@opt_safe_elim -H
373#res #_
374#H lapply (res_eq_from_opt ??? H) -H
375#H elim (bind_inversion ????? H)
376* #f #stmt *
377whd in ⊢ (??%?→?);
378cases daemon
379qed.
380
381(* To be added to common/Globalenvs, it strenghtens
382   find_funct_ptr_transf *)
383(*   
384lemma
385  find_funct_ptr_transf_eq:
386    ∀A,B,V,iV. ∀p: program A V. ∀transf: (∀vs. A vs → B vs).
387    ∀b: block.
388    find_funct_ptr ? (globalenv … iV (transform_program … p transf)) b =
389     m_map ???
390      (transf …)
391      (find_funct_ptr ? (globalenv … iV p) b).
392 #A #B #V #iV #p #transf #b inversion (find_funct_ptr ???) in ⊢ (???%);
393 [ cases daemon (* TODO in Globalenvs.ma *)
394 | #f #H >(find_funct_ptr_transf A B … H) // ]
395qed.
396*)
397
398
399(*lemma fetch_function_sigma_commute:
400 ∀p,p',graph_prog,sigma,st1.
401 ∀prf:well_formed_status ??? sigma st1.
402 let lin_prog ≝ linearise ? graph_prog in
403  fetch_function               
404   (lin_prog_params p p' lin_prog)
405   (globals (lin_prog_params p p' lin_prog))
406   (ev_genv (lin_prog_params p p' lin_prog))
407   (pc (lin_prog_params p p' lin_prog)
408    (linearise_status_fun p p' graph_prog sigma st1 prf))
409 =
410  m_map …
411   (linearise_int_fun ??)
412   (fetch_function
413    (graph_prog_params p p' graph_prog)
414    (globals (graph_prog_params p p' graph_prog))
415    (ev_genv (graph_prog_params p p' graph_prog))
416    (pc (graph_prog_params p p' graph_prog) st1)).
417#p #p' #prog #sigma #st #prf whd in match fetch_function; normalize nodelta
418whd in match function_of_block; normalize nodelta
419>(find_funct_ptr_transf_eq … (λglobals.transf_fundef … (linearise_int_fun … globals)) …)
420cases (find_funct_ptr ???) // * //
421qed.
422*)
423       
424inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
425    ex1_intro: ∀ x:A. P x →  ex_Type1 A P.
426interpretation "exists in Type[1]" 'exists x = (ex_Type1 ? x).
427
428lemma linearise_ok:
429 ∀p,p',graph_prog.
430  let lin_prog ≝ linearise ? graph_prog in
431 ∀lin_stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
432 let graph_stack_sizes ≝
433  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
434    ? graph_prog lin_stack_sizes in
435   ∃R.
436   status_simulation
437    (graph_abstract_status p p' graph_prog graph_stack_sizes)
438    (lin_abstract_status p p' lin_prog lin_stack_sizes) R.
439 #p #p' #graph_prog
440 cut (∃sigma.good_sigma p p' graph_prog sigma)
441 [ cases daemon (* TODO by Paolo *) ] * #sigma #good
442 #lin_stack_sizes
443 %{(linearise_status_rel p p' graph_prog lin_stack_sizes sigma good)}
444 whd
445#st1 #cl #st1' #st2 #move_st1_st1' #rel_st1_st2 #classified_st1_cl
446cases cl in classified_st1_cl; -cl #classified_st1_cl whd
447[4:
448 cases rel_st1_st2 -rel_st1_st2 #wf_st1 #rel_st1_st2 >rel_st1_st2 -st2
449 whd in move_st1_st1';
450 letin lin_prog ≝ (linearise ? graph_prog)
451
452 cut (joint_closed_internal_function (mk_graph_params p) (globals (graph_prog_params p p' graph_prog))) [cases daemon (*???*)] #graph_fun
453
454 cases (linearise_code_spec … p' graph_prog graph_fun
455         (joint_if_entry … graph_fun))     
456 * #lin_code_closed #sigma_entry_is_zero #sigma_spec
457 lapply (sigma_spec
458         (point_of_pointer ? (graph_prog_params … p' graph_prog) (pc … st1)))
459 -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @(sigma_pc_of_status_ok … wf_st1) |2: skip ]
460 -sigma_spec #graph_stmt * #graph_lookup_ok #sigma_spec whd in sigma_spec;
461 inversion (nth_opt ???) in sigma_spec; [ #H whd in ⊢ (% → ?); #abs cases abs ]
462 * #optlabel #lin_stm #lin_lookup_ok whd in ⊢ (% → ?); ** #labels_preserved
463 #related_lin_stm_graph_stm
464 inversion (stmt_implicit_label ???)
465 [ whd in match (opt_All ???); #stmt_implicit_spec #_
466   letin st2_opt' ≝ (eval_state (globals (lin_prog_params p p' lin_prog)) …
467               (ev_genv (lin_prog_params p p' lin_prog))
468               (linearise_status_fun … sigma st1 wf_st1))
469   check st2_opt'
470   cut (∃st2': lin_abstract_status p p' lin_prog. st2_opt' = return st2')
471   [cases daemon (* TODO, needs lemma? *)] * #st2' #st2_spec'
472   normalize nodelta in st2_spec'; -st2_opt'
473   %{st2'} %{(taaf_step … (taa_base …) …)}
474   [ cases daemon (* TODO, together with the previous one? *)
475   | @st2_spec' ]
476   %[%] [%]
477   [ whd
478     whd in st2_spec':(??%?); >fetch_statement_sigma_commute in st2_spec';
479     whd in move_st1_st1':(??%?);
480     cut (fetch_statement (graph_prog_params p p' graph_prog) (graph_prog_params … graph_prog) … (ev_genv (graph_prog_params … graph_prog)) … (pc … st1) = OK ? 〈graph_fun,graph_stmt〉)
481     [ cases daemon (* TODO once and for all, consequence of graph_lookup_ok *) ]
482     #fetch_statement_ok >fetch_statement_ok in move_st1_st1';
483     whd in ⊢ (??%? → ??%? → ?); normalize nodelta
484     inversion graph_stmt in stmt_implicit_spec; normalize nodelta
485     [ #stmt #lbl #_ #abs @⊥ normalize in abs; destruct(abs) ]
486     XXXXXXXXXX siamo qua, caso GOTO e RETURN
487   | cases daemon (* TODO, after the definition of label_rel, trivial *) ]
488   ]
489 | ....
490qed.
Note: See TracBrowser for help on using the repository browser.