source: src/joint/lineariseProof.ma @ 2467

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

LINEARISE PROOF MODIFIED NOT YED FIXED
File size: 22.7 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 *)
161 definition sigma_pc :
162∀p,p',graph_prog,stack_sizes.
163∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) →
164    label → option ℕ).
165∀pc.
166∀prf : well_formed_pc p p' graph_prog stack_sizes sigma pc.
167cpointer ≝
168λp,p',graph_prog,stack_sizes,sigma,st.opt_safe ….
169 
170lemma sigma_pc_of_status_ok:
171  ∀p,p',graph_prog,stack_sizes.
172  ∀sigma.
173   ∀pc.
174    ∀prf:well_formed_pc p p' graph_prog stack_sizes sigma pc.
175    sigma_pc_opt p p' graph_prog stack_sizes sigma pc =
176    Some … (sigma_pc p p' graph_prog stack_sizes sigma pc prf).
177    #p #p' #graph_prog #stack_sizes #sigma #st #prf @opt_to_opt_safe qed.
178
179
180definition sigma_state :
181 ∀p.
182 ∀p':∀F.sem_unserialized_params p F.
183 ∀graph_prog,stack_sizes.
184  ∀sigma.
185(*   let lin_prog ≝ linearise ? graph_prog in *)
186    ∀s:state_pc (p' ?). (* = graph_abstract_status p p' graph_prog stack_sizes *)
187     well_formed_status p p' graph_prog stack_sizes sigma s →
188      state_pc (make_sem_lin_params p p') (* = lin_abstract_status p p' lin_prog ? *)
189≝
190 λp,p',graph_prog,stack_sizes,sigma,s,prf.
191 let pc' ≝ sigma_pc … (proj1 … prf) in
192 mk_state_pc ? ? pc'.
193 cases daemon (* TODO *) qed.
194
195lemma sigma_pc_commute:
196 ∀p,p',graph_prog,stack_sizes,sigma,st.
197 ∀prf : well_formed_status p p' graph_prog stack_sizes sigma st.
198 sigma_pc … (pc ? st) (proj1 … prf) =
199 pc ? (sigma_state … st prf).
200#p #p' #prog #stack_sizes #sigma #st #prf %
201qed.
202
203lemma res_eq_from_opt :
204  ∀A,m,v.res_to_opt A m = return v → m = return v.
205#A * #x #v normalize #EQ destruct % qed.
206
207lemma if_propagate :
208∀pars_in, pars_out : sem_params.
209∀trans : ∀globals.joint_closed_internal_function pars_in globals →
210                  joint_closed_internal_function pars_out globals.
211∀prog_in : program (joint_function pars_in) ℕ.
212let prog_out ≝
213  transform_program … prog_in (λglobals.transf_fundef ?? (trans globals)) in
214∀i.is_internal_function_of_program … prog_in i →
215is_internal_function_of_program … prog_out i.
216cases daemon (* TODO by paolo *) qed.
217
218definition stack_sizes_lift :
219∀pars_in, pars_out : sem_params.
220∀trans : ∀globals.joint_closed_internal_function pars_in globals →
221                  joint_closed_internal_function pars_out globals.
222∀prog_in : program (joint_function pars_in) ℕ.
223let prog_out ≝
224  transform_program … prog_in (λglobals.transf_fundef ?? (trans globals)) in
225((Σi.is_internal_function_of_program … prog_out i) → ℕ) →
226((Σi.is_internal_function_of_program … prog_in i) → ℕ) ≝
227λpars_in,pars_out,prog_in,trans,stack_sizes.
228λi.stack_sizes «i, if_propagate … (pi2 … i)».
229
230axiom ok_is_internal_function_of_program :
231  ∀p.∀prog:joint_program p.∀i.
232  is_internal_function_of_program p prog i →
233  is_internal_function ?? (globalenv_noinit ? prog) i.
234
235
236definition sigma_function_name :
237 ∀p,p',graph_prog.
238 let lin_prog ≝ linearise p graph_prog in
239 ∀lin_stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
240 let graph_stack_sizes ≝
241  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
242    ? graph_prog lin_stack_sizes in
243  (Σf.is_internal_function … (ev_genv (graph_prog_params p p' graph_prog graph_stack_sizes)) f) →
244  (Σf.is_internal_function … (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) f) ≝
245λp,p',graph_prog,lin_stack_sizes,f.pi1 … f.
246@ok_is_internal_function_of_program
247@(if_propagate (make_sem_graph_params p p') (make_sem_lin_params p p'))
248@is_internal_function_of_program_ok
249@(pi2 … f)
250qed.
251
252
253lemma if_of_function_commute:
254 ∀p,p',graph_prog,stack_sizes.
255 ∀graph_fun.
256 let graph_fd ≝ if_of_function ??? graph_fun in
257 let lin_fun ≝ sigma_function_name p p' graph_prog stack_sizes graph_fun in
258 let lin_fd ≝ if_of_function … lin_fun in
259 lin_fd = linearise_int_fun … graph_fd.
260(* usare match_opt_prf_elim ? *)
261cases daemon qed.
262
263lemma bind_opt_inversion:
264  ∀A,B: Type[0]. ∀f: option A. ∀g: A → option B. ∀y: B.
265  (! x ← f ; g x = Some … y) →
266  ∃x. (f = Some … x) ∧ (g x = Some … y).
267#A #B #f #g #y cases f normalize
268[ #H destruct (H)
269| #a #e %{a} /2 by conj/
270] qed.
271
272lemma sigma_pblock_eq_lemma :
273∀p,p',graph_prog.
274let lin_prog ≝ linearise p graph_prog in
275∀lin_stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
276let graph_stack_sizes ≝
277 stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
278    ? graph_prog lin_stack_sizes in
279∀sigma,st.
280∀prf : well_formed_status p p' graph_prog graph_stack_sizes sigma st.
281 pblock (sigma_pc ? p' graph_prog graph_stack_sizes sigma (pc ? st) (proj1 … prf)) =
282 pblock (pc ? st).
283 #p #p' #graph_prog #stack_sizes #sigma #st #prf
284 whd in match sigma_pc; normalize nodelta
285 @opt_safe_elim #x #x_spec
286 whd in x_spec:(??%?); cases (int_funct_of_block ????) in x_spec;
287 normalize nodelta [#abs destruct] #id #H cases (bind_opt_inversion ????? H) -H
288 #offset * #_ whd in ⊢ (??%? → ?); whd in match pointer_of_point; normalize nodelta
289 cases (opt_to_res ???) [2: #msg #abs normalize in abs; destruct]
290 #offset_lin whd in ⊢ (??%? → ?); #EQ destruct //
291qed.
292
293lemma fetch_function_sigma_commute :
294 ∀p,p',graph_prog.
295 let lin_prog ≝ linearise p graph_prog in
296 ∀lin_stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
297 let graph_stack_sizes ≝
298  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
299    ? graph_prog lin_stack_sizes in
300 ∀sigma,st,f.
301  ∀prf : well_formed_status p p' graph_prog graph_stack_sizes sigma st.
302  let pc_st ≝ pc ? st in
303 fetch_function … (ev_genv (graph_prog_params p p' graph_prog graph_stack_sizes)) pc_st =
304  return f
305→ fetch_function … (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) (sigma_pc … pc_st (proj1 … prf)) =
306  return sigma_function_name … f.
307 #p #p' #graph_prog #stack_sizes #sigma #st #f #prf
308 >(sigma_pc_commute … prf)
309whd in match fetch_function; normalize nodelta
310>(sigma_pblock_eq_lemma … prf) #H
311lapply (opt_eq_from_res ???? H) -H
312whd in match int_funct_of_block in ⊢ (%→?); normalize nodelta
313
314XXXX ENTRARE IN PRF CHE C'E' FUNCT OF BLOCK XXXX
315
316#H elim (bind_opt_inversion ????? H) -H
317#x * whd in match funct_of_block in ⊢ (%→?); normalize nodelta
318@match_opt_prf_elim
319 #H #H1  whd in H : (??%?);
320cases (   find_funct_ptr
321   (fundef
322    (joint_closed_internal_function
323     (graph_prog_params p p' graph_prog
324      (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
325       (linearise_int_fun p) graph_prog stack_sizes))
326     (globals
327      (graph_prog_params p p' graph_prog
328       (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
329        (linearise_int_fun p) graph_prog stack_sizes)))))
330   (ev_genv
331    (graph_prog_params p p' graph_prog
332     (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
333      (linearise_int_fun p) graph_prog stack_sizes)))
334   (pblock (pc (make_sem_graph_params p p') st))) in H; [ 2: normalize #abs destruct
335 
336
337normalize nodelta
338#H #H1
339cases (   find_funct_ptr
340   (fundef
341    (joint_closed_internal_function
342     (graph_prog_params p p' graph_prog
343      (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
344       (linearise_int_fun p) graph_prog stack_sizes))
345     (globals
346      (graph_prog_params p p' graph_prog
347       (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
348        (linearise_int_fun p) graph_prog stack_sizes)))))
349   (ev_genv
350    (graph_prog_params p p' graph_prog
351     (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
352      (linearise_int_fun p) graph_prog stack_sizes)))
353   (pblock (pc (make_sem_graph_params p p') st))) in H;
354
355
356check find_funct_ptr_transf
357whd in match int_funct_of_block; normalize nodelta
358#H elim (bind_inversion ????? H)
359
360.. sigma_int_funct_of_block
361
362
363
364whd in match int_funct_of_block; normalize nodelta
365elim (bind_inversion ????? H)
366whd in match int_funct_of_block; normalize nodelta
367#H elim (bind_inversion ????? H) -H #fn *
368#H lapply (opt_eq_from_res ???? H) -H
369#H >(find_funct_ptr_transf … (λglobals.transf_fundef … (linearise_int_fun … globals)) … H)
370-H #H >m_return_bind cases fn in H; normalize nodelta #arg #EQ whd in EQ:(??%%);
371destruct // *)
372cases daemon
373qed.
374
375lemma stmt_at_sigma_commute:
376 ∀p,p',graph_prog,stack_sizes,graph_fun,lbl.
377 let lin_prog ≝ linearise ? graph_prog in
378 let lin_fun ≝ sigma_function_name p p' graph_prog stack_sizes graph_fun in
379 ∀sigma.good_sigma p p' graph_prog sigma →
380 ∀prf:sigma graph_fun lbl ≠ None ….
381 ∃stmt.
382   stmt_at …
383    (joint_if_code ?? (if_of_function ??? graph_fun)) 
384    lbl = Some ? stmt ∧
385   stmt_at …
386    (joint_if_code ?? (if_of_function ??? lin_fun))
387    (opt_safe … (sigma graph_fun lbl) prf) = Some ? (graph_to_lin_statement … stmt). 
388 #p #p' #graph_prog #stack_sizes #graph_fun #lbl #sigma #good #prf
389 @opt_safe_elim -prf #n #prf
390 (*
391 whd in match (stmt_at ????);
392 whd in match (stmt_at ????);
393 cases (linearise_code_spec … p' graph_prog graph_fun
394         (joint_if_entry … graph_fun))
395 * #lin_code_closed #sigma_entry_is_zero #sigma_spec
396 lapply (sigma_spec
397         (point_of_pointer ? (graph_prog_params … p' graph_prog) (pc … s1)))
398 -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @(sigma_pc_of_status_ok … prf) |2: skip ]
399 -sigma_spec #graph_stmt * #graph_lookup_ok >graph_lookup_ok -graph_lookup_ok
400 whd in ⊢ (? → ???%); #sigma_spec whd in sigma_spec;
401 inversion (nth_opt ???) in sigma_spec; [ #H whd in ⊢ (% → ?); #abs cases abs ]
402 * #optlabel #lin_stm #lin_lookup_ok whd in ⊢ (% → ?); ** #_
403 #related_lin_stm_graph_stm #_ <related_lin_stm_graph_stm -related_lin_stm_graph_stm
404 <sigma_pc_commute >lin_lookup_ok // *)
405 cases daemon
406qed.
407
408lemma fetch_statement_sigma_commute:
409  ∀p,p',graph_prog,lin_stack_sizes,pc,fn,stmt.
410  let lin_prog ≝ linearise ? graph_prog in
411  let graph_stack_sizes ≝
412   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
413    ? graph_prog lin_stack_sizes in
414  ∀sigma.good_sigma p p' graph_prog sigma →
415  ∀prf : well_formed_pc p p' graph_prog graph_stack_sizes sigma pc.
416  fetch_statement ? (make_sem_graph_params p p') … (ev_genv (graph_prog_params p p' graph_prog graph_stack_sizes)) pc =
417    return 〈fn,stmt〉 →
418  fetch_statement ? (make_sem_lin_params p p') … (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes))
419   (sigma_pc … pc prf) =
420    return 〈sigma_function_name … fn, graph_to_lin_statement … stmt〉.
421 #p #p' #graph_prog #stack_sizes #pc #fn #stmt #good #prf
422(* @opt_safe_elim -prf #n #prf
423 whd in match fetch_statement; normalize nodelta
424 >fetch_function_sigma_commute
425 cases (fetch_function ????) [2://]
426 #graph_fun whd in ⊢ (??%%);
427 whd in ⊢ (???(match % with [ _ ⇒ ? | _ ⇒ ?]));
428 >stm_at_sigma_commute cases (stmt_at ????) // *)
429cases daemon
430qed.
431
432definition linearise_status_rel:
433 ∀p,p',graph_prog.
434 let lin_prog ≝ linearise p graph_prog in
435 ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
436 let stack_sizes' ≝
437  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
438    ? graph_prog stack_sizes in
439 ∀sigma.
440 good_sigma p p' graph_prog sigma →
441   status_rel
442    (graph_abstract_status p p' graph_prog stack_sizes')
443    (lin_abstract_status p p' lin_prog stack_sizes)
444 ≝ λp,p',graph_prog,stack_sizes,sigma,good.
445   let stack_sizes' ≝
446    stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
447      ? graph_prog ? in
448   mk_status_rel …
449    (* sem_rel ≝ *) (λs1,s2.
450     ∃prf: well_formed_status p p' graph_prog stack_sizes' sigma s1.
451      s2 = sigma_state … s1 prf)
452    (* call_rel ≝ *) (λs1,s2.
453      ∃prf:well_formed_status p p' graph_prog stack_sizes' sigma s1.
454      pc ? s2 = sigma_pc … (pc ? s1) (proj1 … prf))
455    (* sim_final ≝ *) ?.
456#st1 #st2 * #prf #EQ2
457%
458whd in ⊢ (%→%);
459#H lapply (opt_to_opt_safe … H)
460@opt_safe_elim -H
461#res #_
462#H lapply (res_eq_from_opt ??? H) -H
463#H elim (bind_inversion ????? H)
464* #f #stmt *
465whd in ⊢ (??%?→?);
466cases daemon
467qed.
468
469(* To be added to common/Globalenvs, it strenghtens
470   find_funct_ptr_transf *)
471(*   
472lemma
473  find_funct_ptr_transf_eq:
474    ∀A,B,V,iV. ∀p: program A V. ∀transf: (∀vs. A vs → B vs).
475    ∀b: block.
476    find_funct_ptr ? (globalenv … iV (transform_program … p transf)) b =
477     m_map ???
478      (transf …)
479      (find_funct_ptr ? (globalenv … iV p) b).
480 #A #B #V #iV #p #transf #b inversion (find_funct_ptr ???) in ⊢ (???%);
481 [ cases daemon (* TODO in Globalenvs.ma *)
482 | #f #H >(find_funct_ptr_transf A B … H) // ]
483qed.
484*)
485
486
487(*lemma fetch_function_sigma_commute:
488 ∀p,p',graph_prog,sigma,st1.
489 ∀prf:well_formed_status ??? sigma st1.
490 let lin_prog ≝ linearise ? graph_prog in
491  fetch_function               
492   (lin_prog_params p p' lin_prog)
493   (globals (lin_prog_params p p' lin_prog))
494   (ev_genv (lin_prog_params p p' lin_prog))
495   (pc (lin_prog_params p p' lin_prog)
496    (linearise_status_fun p p' graph_prog sigma st1 prf))
497 =
498  m_map …
499   (linearise_int_fun ??)
500   (fetch_function
501    (graph_prog_params p p' graph_prog)
502    (globals (graph_prog_params p p' graph_prog))
503    (ev_genv (graph_prog_params p p' graph_prog))
504    (pc (graph_prog_params p p' graph_prog) st1)).
505#p #p' #prog #sigma #st #prf whd in match fetch_function; normalize nodelta
506whd in match function_of_block; normalize nodelta
507>(find_funct_ptr_transf_eq … (λglobals.transf_fundef … (linearise_int_fun … globals)) …)
508cases (find_funct_ptr ???) // * //
509qed.
510*)
511       
512inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
513    ex1_intro: ∀ x:A. P x →  ex_Type1 A P.
514interpretation "exists in Type[1]" 'exists x = (ex_Type1 ? x).
515
516lemma linearise_ok:
517 ∀p,p',graph_prog.
518  let lin_prog ≝ linearise ? graph_prog in
519 ∀lin_stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
520 let graph_stack_sizes ≝
521  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
522    ? graph_prog lin_stack_sizes in
523   ∃R.
524   status_simulation
525    (graph_abstract_status p p' graph_prog graph_stack_sizes)
526    (lin_abstract_status p p' lin_prog lin_stack_sizes) R.
527 #p #p' #graph_prog
528 cut (∃sigma.good_sigma p p' graph_prog sigma)
529 [ cases daemon (* TODO by Paolo *) ] * #sigma #good
530 #lin_stack_sizes
531 %{(linearise_status_rel p p' graph_prog lin_stack_sizes sigma good)}
532 whd
533#st1 #cl #st1' #st2 #move_st1_st1' #rel_st1_st2 #classified_st1_cl
534cases cl in classified_st1_cl; -cl #classified_st1_cl whd
535[4:
536 cases rel_st1_st2 -rel_st1_st2 #wf_st1 #rel_st1_st2 >rel_st1_st2 -st2
537 whd in move_st1_st1';
538 letin lin_prog ≝ (linearise ? graph_prog)
539
540 cut (joint_closed_internal_function (mk_graph_params p) (globals (graph_prog_params p p' graph_prog))) [cases daemon (*???*)] #graph_fun
541
542 cases (linearise_code_spec … p' graph_prog graph_fun
543         (joint_if_entry … graph_fun))     
544 * #lin_code_closed #sigma_entry_is_zero #sigma_spec
545 lapply (sigma_spec
546         (point_of_pointer ? (graph_prog_params … p' graph_prog) (pc … st1)))
547 -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @(sigma_pc_of_status_ok … wf_st1) |2: skip ]
548 -sigma_spec #graph_stmt * #graph_lookup_ok #sigma_spec whd in sigma_spec;
549 inversion (nth_opt ???) in sigma_spec; [ #H whd in ⊢ (% → ?); #abs cases abs ]
550 * #optlabel #lin_stm #lin_lookup_ok whd in ⊢ (% → ?); ** #labels_preserved
551 #related_lin_stm_graph_stm
552 inversion (stmt_implicit_label ???)
553 [ whd in match (opt_All ???); #stmt_implicit_spec #_
554   letin st2_opt' ≝ (eval_state (globals (lin_prog_params p p' lin_prog)) …
555               (ev_genv (lin_prog_params p p' lin_prog))
556               (linearise_status_fun … sigma st1 wf_st1))
557   check st2_opt'
558   cut (∃st2': lin_abstract_status p p' lin_prog. st2_opt' = return st2')
559   [cases daemon (* TODO, needs lemma? *)] * #st2' #st2_spec'
560   normalize nodelta in st2_spec'; -st2_opt'
561   %{st2'} %{(taaf_step … (taa_base …) …)}
562   [ cases daemon (* TODO, together with the previous one? *)
563   | @st2_spec' ]
564   %[%] [%]
565   [ whd
566     whd in st2_spec':(??%?); >fetch_statement_sigma_commute in st2_spec';
567     whd in move_st1_st1':(??%?);
568     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〉)
569     [ cases daemon (* TODO once and for all, consequence of graph_lookup_ok *) ]
570     #fetch_statement_ok >fetch_statement_ok in move_st1_st1';
571     whd in ⊢ (??%? → ??%? → ?); normalize nodelta
572     inversion graph_stmt in stmt_implicit_spec; normalize nodelta
573     [ #stmt #lbl #_ #abs @⊥ normalize in abs; destruct(abs) ]
574     XXXXXXXXXX siamo qua, caso GOTO e RETURN
575   | cases daemon (* TODO, after the definition of label_rel, trivial *) ]
576   ]
577 | ....
578qed.
Note: See TracBrowser for help on using the repository browser.