Changeset 3047
 Timestamp:
 Mar 31, 2013, 10:01:42 PM (4 years ago)
 Location:
 src
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/SwitchAndLabel.ma
r3046 r3047 2 2 include "Clight/labelSimulation.ma". 3 3 4 axiom switch_final_related : ∀ge1,s1,s2.5 switch_state_sim ge1 s1 s2 →6 is_final s1 = is_final s2.7 4 8 5 lemma after_aux_result : ∀avs,n,s,tr,P. … … 90 87 91 88 lemma interactive_switch_step : ∀ge,ge'. 92 switch_removal_globals ?fundef_switch_removal ge ge' →89 related_globals … fundef_switch_removal ge ge' → 93 90 ∀s1,s1',o,k. 94 91 exec_step ge s1 = Interact … o k → … … 144 141 let corec build_exec 145 142 (ge1,ge2,ge3:genv) 146 (SRG: switch_removal_globals ?fundef_switch_removal ge1 ge2)143 (SRG:related_globals … fundef_switch_removal ge1 ge2) 147 144 (RG:related_globals_gen … label_fundef ge2 ge3) 148 145 (s1,s2,s3:state) … … 212 209 ] 213 210 ] qed. 211 212 theorem switch_and_labelling_sim : ∀p. 213 let e1 ≝ exec_inf … clight_fullexec p in 214 let e2 ≝ exec_inf … clight_fullexec (\fst (clight_label (program_switch_removal p))) in 215 not_wrong state e1 → 216 sim_with_labels e1 e2. 217 #p letin p' ≝ (program_switch_removal p) 218 #NW 219 cases (not_wrong_init clight_fullexec p NW) 220 whd in ⊢ (% → ??%? → ?); #s1 #I1 221 cases (initial_state_in_switch_simulation … I1) 222 #s' * * change with p' in match (program_switch_removal p); #I' #RG' #S' 223 cases (initial_state_in_simulation … I') 224 #s2 * #I2 225 226 whd in match (exec_inf ?? clight_fullexec p) in NW ⊢ %; 227 letin ge1 ≝ (make_global ?? clight_fullexec p) in NW ⊢ %; 228 change with (make_initial_state p) in match (make_initial_state ?? clight_fullexec p); 229 >I1 230 231 whd in match (exec_inf ????); 232 letin ge2 ≝ (make_global ?? clight_fullexec (\fst (clight_label p'))) 233 change with (make_initial_state (\fst (clight_label p'))) in match (make_initial_state ?? clight_fullexec (\fst (clight_label p'))); 234 >I2 235 236 whd in ⊢ (??% → ? → ?%%); 237 >exec_inf_aux_unfold 238 >exec_inf_aux_unfold 239 whd in ⊢ (??% → ? → ?%%); 240 whd in match (is_final ?????); 241 >(initial_state_is_not_final … I1) 242 whd in match (is_final ?????); 243 >(initial_state_is_not_final … I2) 244 whd in ⊢ (??% → ? → ?%%); 245 246 #NW #S 247 @(swl_steps E0 E0) 248 [ 2: @steps_step  skip  //  @(build_exec … RG' … S' S) 249 [ whd in match ge2; >unfold_clight_label 250 @transform_program_gen_related 251  inversion NW 252 [ #tr #i #s #E1 #E2 destruct 253  #trX #sX #eX #NWX #E1X #E2X destruct // 254  #H1 #H2 #H3 #H4 #H5 destruct 255 ] 256 ] 257 ] qed. 258 259 
src/Clight/switchRemoval.ma
r3046 r3047 429 429 430 430 let rec program_switch_removal (p : clight_program) : clight_program ≝ 431 let prog_funcs ≝ prog_funct ?? p in 432 let sf_funcs ≝ map ?? (λcl_fundef. 433 let 〈fun_id, fun_def〉 ≝ cl_fundef in 434 〈fun_id, fundef_switch_removal fun_def〉 435 ) prog_funcs in 436 mk_program ?? 437 (prog_vars … p) 438 sf_funcs 439 (prog_main … p). 431 transform_program ??? p (λ_. fundef_switch_removal). 440 432 441 433 (*  … … 1920 1912 (Kcall r (\fst (function_switch_removal f)) en' k'). 1921 1913 1922 record switch_removal_globals (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ {1923 rg_find_symbol: ∀s.1924 find_symbol ? ge s = find_symbol ? ge' s;1925 rg_find_funct_id: ∀v,f,id.1926 find_funct_id ? ge v = Some ? 〈f,id〉 →1927 find_funct_id ? ge' v = Some ? 〈t f,id〉;1928 rg_find_funct_ptr: ∀b,f.1929 find_funct_ptr ? ge b = Some ? f →1930 find_funct_ptr ? ge' b = Some ? (t f)1931 }.1932 1933 1914 inductive switch_state_sim (ge : genv) : state → state → Prop ≝ 1934 1915  sws_state : … … 2214 2195 lemma sim_related_globals : ∀ge,ge',en1,m1,en2,m2,writeable,ext. 2215 2196 ∀Hext:sr_memext m1 m2 writeable. 2216 switch_removal_globals ?fundef_switch_removal ge ge' →2197 related_globals … fundef_switch_removal ge ge' → 2217 2198 disjoint_extension en1 en2 ext → 2218 2199 (* disjoint_extension en1 en2 ext Hext → *) … … 2750 2731 theorem switch_removal_correction : 2751 2732 ∀ge,ge'. 2752 switch_removal_globals ?fundef_switch_removal ge ge' →2733 related_globals … fundef_switch_removal ge ge' → 2753 2734 ∀s1,s1',tr,s2. 2754 2735 switch_state_sim ge s1 s1' → … … 3259 3240  *: @cthulhu ] 3260 3241  *: @cthulhu ] qed. 3242 3243 3244 lemma initial_state_in_switch_simulation : ∀p,s. 3245 make_initial_state p = OK ? s → 3246 ∃s'. 3247 make_initial_state (program_switch_removal p) = OK ? s' ∧ 3248 related_globals … fundef_switch_removal (make_global p) (make_global (program_switch_removal p)) ∧ 3249 switch_state_sim (make_global p) s s'. 3250 * #vars #fns #main #s 3251 whd in ⊢ (??%? → ?); letin ge ≝ (make_global ?) #EX 3252 cases (bind_inversion ????? EX) EX #m * #Em #EX 3253 cases (bind_inversion ????? EX) EX #b * #Emain #EX 3254 cases (bind_inversion ????? EX) EX #fd * #Emain' #EX 3255 whd in EX:(??%%); destruct 3256 whd in match (make_initial_state ?); 3257 letin ge' ≝ (make_global ?) 3258 cut (related_globals … fundef_switch_removal ge ge') 3259 [ // ] #RG 3260 lapply (rg_find_funct_ptr … RG … Emain') #FFP 3261 % [2: % 3262 [ % 3263 [whd in ⊢ (??%?); 3264 change with (transform_program ??? (mk_program …) (λ_.?)) in match (mk_program ??? (transf_program ????) ?); 3265 >(init_mem_transf … (mk_program ?? vars fns main)) >Em in ⊢ (??%?); 3266 whd in ⊢ (??%?); <(rg_find_symbol … RG) >Emain in ⊢ (??%?); 3267 whd in ⊢ (??%?); >FFP in ⊢ (??%?); 3268 whd in ⊢ (??%?); @refl 3269  /3/ 3270 ]  /3/ ]  skip ] 3271 qed. 3272 3273 lemma switch_final_related : ∀ge1,s1,s2. 3274 switch_state_sim ge1 s1 s2 → 3275 is_final s1 = is_final s2. 3276 #Xge #Xs1 #Xs2 * // 3277 qed. 3278 
src/correctness.ma
r3030 r3047 3 3 4 4 include "ASM/Interpret2.ma". 5 6 include "Clight/labelSimulation.ma".7 5 8 6 include "Clight/Clight_classified_system.ma". … … 74 72 include "common/ExtraMonads.ma". 75 73 74 include "Clight/SwitchAndLabel.ma". 75 76 76 theorem correct : 77 77 ∀observe. … … 110 110 111 111 #NOT_WRONG % 112 [ cases daemon (* TODO *) 112 [ whd in EQ_front_end:(??%%); destruct 113 cut (labelled = \fst (clight_label cl_switch_removed)) 114 [ cases (clight_label ?) in CL_LABELLED ⊢ %; // ] 115 #E >E 116 @switch_and_labelling_sim @NOT_WRONG 113 117  #m1 #m2 #m1_m2_meas #c1 #c2 #c1_prf #c2_prf 114 118
Note: See TracChangeset
for help on using the changeset viewer.