Changeset 2559 for src/joint/lineariseProof.ma
 Timestamp:
 Dec 18, 2012, 1:56:07 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/lineariseProof.ma
r2556 r2559 1 (**************************************************************************)1 (**************************************************************************) 2 2 (* ___ *) 3 3 (* M *) … … 18 18 include "joint/semanticsUtils.ma". 19 19 20 axiom globalenv_no_minus_one : 20 include alias "common/PositiveMap.ma". 21 22 lemma add_functs_functions_miss : ∀F. ∀ge : genv_t F.∀ l.∀ id. 23 id < (nextfunction ? ge) → 24 lookup_opt … id (functions ? ge) = None ? → 25 lookup_opt … id (functions … (add_functs F ge l)) = None ?. 26 #F #ge #l #id whd in match add_functs; normalize nodelta 27 elim l l [ #_ normalize //] 28 * #id1 #f1 #tl #IND #H #H1 whd in match (foldr ?????); 29 >lookup_opt_insert_miss [ inversion(lookup_opt ? ? ?) [ #_ %] 30 #f1 #H3 <(drop_fn_lfn … f1 H3) @(IND H H1) 31  cut(nextfunction F ge ≤ nextfunction F (foldr … (add_funct F) ge tl)) 32 [elim tl [normalize //] 33 #x #tl2 whd in match (foldr ?????) in ⊢ (? → %); #H %2{H} ] 34 #H2 lapply(transitive_le … H H2) @lt_to_not_eq 35 qed. 36 37 lemma add_globals_functions_miss : ∀F,V,init. ∀gem : genv_t F × mem.∀ id,l. 38 lookup_opt … id (functions ? (\fst gem)) = None ? → 39 lookup_opt … id (functions … (\fst (add_globals F V init gem l))) = None ?. 40 #F #V #init * #ge #m #id #l lapply ge ge lapply m m elim l [ #ge #m #H @H] 41 ** #x1 #x2 #x3 #tl whd in match add_globals; 42 normalize nodelta #IND #m #ge #H whd in match (foldl ?????); normalize nodelta 43 cases(alloc m ? ? x2) #m1 #bl1 normalize nodelta @IND whd in match add_symbol; 44 normalize nodelta inversion(lookup_opt ? ? ?) [ #_ %] 45 #f1 #H3 <(drop_fn_lfn … f1 H3) assumption 46 qed. 47 48 49 lemma globalenv_no_minus_one : 21 50 ∀F,V,i,p. 22 find_funct_ptr … (globalenv F V i p) (mk_block Code (1)) = None ?. 51 find_funct_ptr … (globalenv F V i p) (mk_block Code (1)) = None ?. 52 #F #V #i #p 53 whd in match find_funct_ptr; normalize nodelta 54 whd in match globalenv; 55 whd in match globalenv_allocmem; normalize nodelta 56 @add_globals_functions_miss @add_functs_functions_miss normalize // 57 qed. 23 58 24 59 lemma fetch_internal_function_no_minus_one : … … 444 479 ] 445 480 qed. 481 482 include alias "common/GenMem.ma". 446 483 447 484 lemma bestorev_sigma_commute : … … 2226 2263 qed. 2227 2264 2265 lemma entry_sigma_commute: 2266 ∀ p,p',graph_prog,sigma.good_sigma p graph_prog sigma → 2267 ∀bl,f1,fn1. 2268 (fetch_function ? (globalenv_noinit … graph_prog) bl = 2269 return 〈f1,Internal ? fn1〉) → 2270 ∃prf. 2271 sigma_pc p p' graph_prog sigma 2272 (pc_of_point (make_sem_graph_params p p') bl (joint_if_entry ?? fn1)) prf = 2273 pc_of_point (make_sem_lin_params p p') bl 0. 2274 #p #p' #graph_prog #sigma #good #bl #f1 #fn1 #fn1_spec 2275 cases (good fn1) * #entry_in #_ #_ 2276 % [ @hide_prf %  whd in match sigma_pc; normalize nodelta @opt_safe_elim #pc ] 2277 whd in match sigma_pc_opt; normalize nodelta 2278 >eqZb_false whd in match (pc_block ?); 2279 [2,4: % #EQbl 2280 >(fetch_function_no_minus_one … graph_prog … EQbl) in fn1_spec; 2281 whd in ⊢ (???%→?); #ABS destruct(ABS) ] 2282 normalize nodelta whd in match fetch_internal_function; 2283 normalize nodelta >fn1_spec >m_return_bind >point_of_pc_of_point 2284 >entry_in whd in ⊢ (??%%→?); #EQ destruct(EQ) % 2285 qed. 2286 2228 2287 lemma eval_call_ok : 2229 2288 ∀p,p',graph_prog. … … 2309 2368 cases (allocate_locals_commute … gss … (joint_if_locals … fn) … st_no_pc_wf') 2310 2369 #st_no_pc_wf'' #lin_allocate_locals_spec 2311 cut 2312 (∃prf.sigma_pc p p' graph_prog sigma (pc_of_point (make_sem_graph_params p p') bl (joint_if_entry ?? fn)) prf = 2313 pc_of_point (make_sem_lin_params p p') bl 0) 2314 [ cases (good fn) * #entry_in #_ #_ 2315 % [ @hide_prf %  whd in match sigma_pc; normalize nodelta @opt_safe_elim #pc ] 2316 whd in match sigma_pc_opt; normalize nodelta 2317 >eqZb_false whd in match (pc_block ?); 2318 [2,4: % #EQbl 2319 >(fetch_function_no_minus_one … graph_prog … EQbl) in int_f_spec; 2320 whd in ⊢ (???%→?); #ABS destruct(ABS) ] 2321 normalize nodelta whd in match fetch_internal_function; 2322 normalize nodelta >int_f_spec >m_return_bind >point_of_pc_of_point 2323 >entry_in whd in ⊢ (??%%→?); #EQ destruct(EQ) % 2324 ] * #entry_prf #entry_spec 2370 cases(entry_sigma_commute p p' graph_prog sigma good … int_f_spec) 2371 #entry_prf #entry_spec 2325 2372 % [ @hide_prf %{st_no_pc_wf''} %{entry_prf} @(proj1 … (proj1 … prf)) ] 2326 2373 % [ whd in match joint_call_ident; normalize nodelta … … 2578 2625 qed. 2579 2626 2580 (* TODO *) 2581 axiomeval_tailcall_ok :2627 2628 lemma eval_tailcall_ok : 2582 2629 ∀p,p',graph_prog. 2583 2630 let lin_prog ≝ linearise p graph_prog in … … 2600 2647 eval_state … (ev_genv … (lin_prog_params … (linearise … graph_prog) stack_sizes)) 2601 2648 st2_pre_call = return st2_after_call. 2602 2603 2649 #p #p' #graph_prog #stack_sizes #sigma #good #gss #st #st' #f #fn #fl #called #args 2650 #prf #fetch_spec 2651 cases(fetch_statement_sigma_commute … good (proj2 … (proj1 … prf)) … fetch_spec) * 2652 normalize nodelta #lin_fetch_spec 2653 whd in match eval_state; normalize nodelta >fetch_spec 2654 >m_return_bind whd in match eval_statement_no_pc; normalize nodelta 2655 >m_return_bind whd in match eval_statement_advance; whd in match eval_tailcall; 2656 normalize nodelta @('bind_inversion) #bl #bl_spec 2657 lapply (err_eq_from_io ????? bl_spec) bl_spec 2658 whd in match set_no_pc; normalize nodelta #bl_spec 2659 cases(block_of_call_sigma_commute p p' graph_prog sigma gss ?? (proj2 … prf) ? 2660 bl_spec) * #lin_bl_spec @('bind_inversion) 2661 * #f1 #fn1 cases fn1 normalize nodelta fn1 2662 [2: #ext_f #_ whd in match eval_external_call; normalize nodelta @('bind_inversion) 2663 #st @('bind_inversion) #list_val #_ @('bind_inversion) #le #_ 2664 whd in ⊢ (??%% → ?); #ABS destruct(ABS)] 2665 #fn1 #fn1_spec lapply(err_eq_from_io ????? fn1_spec) fn1_spec #fn1_spec 2666 generalize in match (fetch_function_transf … graph_prog … 2667 (λvars.transf_fundef … (λf_in.\fst(linearise_int_fun ?? f_in))) 2668 … fn1_spec : fetch_function … (globalenv_noinit … (linearise … graph_prog)) bl = ?) in ⊢ ?; 2669 #lin_fn1_spec 2670 whd in match eval_internal_call; normalize nodelta 2671 #H lapply(err_eq_from_io ????? H) H #H @('bind_inversion H) H 2672 #st1 #H @('bind_inversion H) H #dim_s #dim_s_spec 2673 #H @('bind_inversion H) H #st2 #st2_spec whd in ⊢ (??%% → ??%% → ?); 2674 #EQ1 #EQ2 destruct % 2675 [ @hide_prf  % [@hide_prf]] 2676 [1,2: whd in match joint_classify; normalize nodelta [>fetch_spec  >lin_fetch_spec] 2677 >m_return_bind normalize nodelta whd in match joint_classify_final; 2678 normalize nodelta [>bl_spec>lin_bl_spec] >m_return_bind 2679 [>fn1_spec>lin_fn1_spec] % 2680  cases (setup_call_commute … gss … (proj2 … prf) … st2_spec) #wf_st2 #lin_st2_spec 2681 cases (allocate_locals_commute … gss … (joint_if_locals … fn1) ? wf_st2) 2682 #wf_all_st2 #all_st2_spec 2683 cases(entry_sigma_commute p p' graph_prog sigma good … fn1_spec) #wf_pc 2684 #pc_spec 2685 % 2686 [ @hide_prf % 2687 [ % [@(proj1 … (proj1 … prf))  @(wf_pc)] 2688  @(wf_all_st2) 2689 ] 2690  % 2691 [ whd in match joint_tailcall_ident; normalize nodelta 2692 >lin_fetch_spec in ⊢ (??match % with [ _ ⇒ ?  _ ⇒ ?]?); 2693 >fetch_spec in ⊢ (???match % with [ _ ⇒ ?  _ ⇒ ?]); 2694 normalize nodelta >lin_bl_spec >bl_spec >m_return_bind >m_return_bind 2695 whd in match fetch_internal_function; normalize nodelta 2696 >fn1_spec >lin_fn1_spec % 2697  >lin_fetch_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?); 2698 normalize nodelta >m_return_bind in ⊢ (??%?); 2699 >lin_bl_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?); 2700 >lin_fn1_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?); 2701 normalize nodelta >dim_s_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?); 2702 >lin_st2_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?); 2703 >all_st2_spec in ⊢ (??%?); whd in ⊢ (??%%); @eq_f @eq_f2 [2: %] 2704 >pc_spec % 2705 ] 2706 ] 2707 ] 2708 qed. 2709 2710 2711 2604 2712 inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝ 2605 2713 ex1_intro: ∀ x:A. P x → ex_Type1 A P.
Note: See TracChangeset
for help on using the changeset viewer.