Changeset 2467 for src/joint


Ignore:
Timestamp:
Nov 15, 2012, 4:43:18 PM (7 years ago)
Author:
piccolo
Message:

LINEARISE PROOF MODIFIED NOT YED FIXED

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/lineariseProof.ma

    r2464 r2467  
    158158#p #p' #graph_prog #stack_sizes #sigma #st whd in ⊢ (% → ?); * #H #_ @H
    159159qed.
    160 
    161 lemma 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 
    172 definition sigma_pc :
     160 *)
     161 definition sigma_pc :
    173162∀p,p',graph_prog,stack_sizes.
    174163∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) →
     
    178167cpointer ≝
    179168λ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
    180179
    181180definition sigma_state :
     
    251250qed.
    252251
    253 lemma 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
    268 whd 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:(??%%);
    273 destruct // *)
    274 cases daemon
    275 qed.
    276252
    277253lemma if_of_function_commute:
     
    284260(* usare match_opt_prf_elim ? *)
    285261cases 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.
    286374
    287375lemma stmt_at_sigma_commute:
Note: See TracChangeset for help on using the changeset viewer.