 Timestamp:
 Apr 1, 2013, 7:04:57 PM (7 years ago)
 Location:
 src/Clight
 Files:

 1 added
 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/toCminorCorrectness.ma
r3054 r3055 3049 3049 3050 3050 3051 3052 3053 3054 (* TODO: adapt the following to the new goal shape. *) 3055 (* 3056 3057 axiom clight_cminor_cost : 3058 ∀INV:clight_cminor_inv. 3059 ∀s1,s1',s2,tr. 3060 clight_cminor_rel INV s1 s1' → 3061 Clight_labelled s1 → 3062 after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) → 3063 after_n_steps 1 … Cminor_exec (ge_cm INV) s1' (λs.true) (λtr',s2'. 3064 tr = tr' ∧ 3065 clight_cminor_rel INV s2 s2' 3066 ). 3067 3068 axiom clight_cminor_init : ∀cl_program,cm_program,s,s'. 3069 clight_to_cminor cl_program = OK ? cm_program → 3070 make_initial_state ?? clight_fullexec cl_program = OK ? s → 3071 make_initial_state ?? Cminor_fullexec cm_program = OK ? s' → 3072 ∃INV. clight_cminor_rel INV s 3051 (* TODO: move to globalenvs *) 3052 lemma find_funct_match: 3053 ∀M:matching.∀initV,initW. 3054 ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M). 3055 ∀MATCH:match_program … M p p'. 3056 ∀v. ∀f: m_A M (prog_var_names … p). 3057 find_funct … (globalenv … initV p) v = Some ? f → 3058 ∃tf : m_B M (prog_var_names … p'). 3059 find_funct … (globalenv … initW p') v = Some ? tf ∧ match_fundef M ? f (tf⌈m_B M ? ↦ m_B M (prog_var_names … p)⌉). 3060 [ 2: >(matching_vars … (mp_vars … MATCH)) % ] 3061 #M #initV #initW #p #p' #MP * [  #sz #i   #p ] #f 3062 [ 1,2,3: #FF whd in FF:(??%?); destruct ] 3063 whd in ⊢ (??%? → ?); @eq_offset_elim #OFF #FFP 3064 [2: whd in FFP:(??%?); destruct ] 3065 cases (find_funct_ptr_match M initV initW … MP (pblock p) f FFP) 3066 #f' * #FFP' #MF %{f'} % 3067 [ whd in ⊢ (??%?); >OFF >reflexive_eq_offset @FFP' 3068  @MF 3069 ] qed. 3070 3071 lemma clight_cminor_inv_exists : ∀p,p'. 3072 clight_to_cminor p = OK … p' → 3073 clight_cminor_inv (make_global … clight_fullexec p) (make_global … Cminor_fullexec p'). 3074 #p #p' #COMPILE 3075 lapply (clight_to_cminor_matches … COMPILE) #MATCHES COMPILE 3076 % 3077 [2: #sym lapply (find_symbol_match (clight_cminor_matching p) ????? MATCHES) 3078 [4: #H @sym_eq @H  #X #Y * #id #r #v1 #v2 * %  skip  skip ] 3079 3: #v #f #FF cases (find_funct_match … MATCHES … FF) 3080 [ #f' * #FF' whd in ⊢ (% → ?); * #H1 * #H2 #Efd 3081 % [2: %{f'} %{H1} %{H2} % [ >Efd 3082 Efd H1 H2 FF' FF 3083 generalize in ⊢ (??(??(match % with [_⇒?]))?); 3084 >(matching_vars … (mp_vars … MATCHES)) MATCHES 3085 #E @(streicherK ???? E) % 3086  @FF' 3087 ] 3088  skip 3089 ] 3090  skip 3091 ] 3092  skip 3093 ] qed. 3094 3095 3096 lemma init_clight_cminor : ∀p,p',s. 3097 make_initial_state … clight_fullexec p = OK … s → 3098 clight_to_cminor p = OK … p' → 3099 ∃INV:clight_cminor_inv (make_global … clight_fullexec p) (make_global … Cminor_fullexec p'). 3100 ∃s'. 3101 make_initial_state … Cminor_fullexec p' = OK … s' ∧ 3102 clight_cminor_rel (make_global … clight_fullexec p) (make_global … Cminor_fullexec p') INV s s'. 3103 #p #p' #s #INIT #COMPILE 3104 lapply (clight_to_cminor_matches … COMPILE) #MATCHES 3105 3106 %{(clight_cminor_inv_exists … COMPILE)} 3107 3108 lapply (find_funct_ptr_match (clight_cminor_matching p) (fst ??) (λx.x) … MATCHES) 3109 lapply (find_symbol_match (clight_cminor_matching p) (fst ??) (λx.x) … MATCHES) 3110 [ #v #w * // ] 3111 lapply (init_mem_match (clight_cminor_matching p) (fst ??) (λx.x) … MATCHES) 3112 [ #v #w * // ] 3113 cases p in INIT COMPILE MATCHES ⊢ %; #vars #fns #main #INIT #COMPILE #MATCHES 3114 cases (bind_inversion ????? INIT) INIT #m * #INITMEM #INIT 3115 cases (bind_inversion ????? INIT) INIT #b * #FINDSYM #INIT 3116 cases (bind_inversion ????? INIT) INIT #fd * #FFP #INIT 3117 whd in INIT:(??%%); destruct 3118 whd in match (m_A ??); whd in match (m_B ??); whd in match (m_V ?); whd in match (m_W ?); 3119 #M_initmem #M_findsym #M_ffp 3120 cases (M_ffp … FFP) M_ffp #f' * #FFP' #Mf' 3121 %{(Callstate main f' [ ] m SStop)} % 3122 [ whd in ⊢ (??%?); normalize in M_initmem:(??(?%%%?)(?%%%?)); >M_initmem >INITMEM 3123 whd in ⊢ (??%?); lapply (M_findsym main) <(mp_main … MATCHES) 3124 whd in match (m_A ??); whd in match (m_B ??); 3125 change with (make_global p') in match (globalenv ????); #E >E 3126 >FINDSYM 3127 whd in ⊢ (??%?); >FFP' 3128 whd in ⊢ (??%?); % 3129  (* Axiomatised  we don't have the simulation step out of Callstate yet anyway. *) 3130 cases daemon 3131 ] qed. 3132
Note: See TracChangeset
for help on using the changeset viewer.