 Timestamp:
 Nov 15, 2012, 4:43:18 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/lineariseProof.ma
r2464 r2467 158 158 #p #p' #graph_prog #stack_sizes #sigma #st whd in ⊢ (% → ?); * #H #_ @H 159 159 qed. 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 : 173 162 ∀p,p',graph_prog,stack_sizes. 174 163 ∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) → … … 178 167 cpointer ≝ 179 168 λp,p',graph_prog,stack_sizes,sigma,st.opt_safe …. 169 170 lemma 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 180 179 181 180 definition sigma_state : … … 251 250 qed. 252 251 253 lemma fetch_function_sigma_commute :254 ∀p,p',graph_prog.255 let lin_prog ≝ linearise p graph_prog in256 ∀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 in260 ∀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 f264 → 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 #prf267 (* whd in match fetch_function; normalize nodelta268 whd in match function_of_block; normalize nodelta269 #H elim (bind_inversion ????? H) H #fn *270 #H lapply (opt_eq_from_res ???? H) H271 #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 daemon275 qed.276 252 277 253 lemma if_of_function_commute: … … 284 260 (* usare match_opt_prf_elim ? *) 285 261 cases daemon qed. 262 263 lemma 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 272 lemma sigma_pblock_eq_lemma : 273 ∀p,p',graph_prog. 274 let lin_prog ≝ linearise p graph_prog in 275 ∀lin_stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. 276 let 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 // 291 qed. 292 293 lemma 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) 309 whd in match fetch_function; normalize nodelta 310 >(sigma_pblock_eq_lemma … prf) #H 311 lapply (opt_eq_from_res ???? H) H 312 whd in match int_funct_of_block in ⊢ (%→?); normalize nodelta 313 314 XXXX 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 : (??%?); 320 cases ( 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 337 normalize nodelta 338 #H #H1 339 cases ( 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 356 check find_funct_ptr_transf 357 whd in match int_funct_of_block; normalize nodelta 358 #H elim (bind_inversion ????? H) 359 360 .. sigma_int_funct_of_block 361 362 363 364 whd in match int_funct_of_block; normalize nodelta 365 elim (bind_inversion ????? H) 366 whd 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:(??%%); 371 destruct // *) 372 cases daemon 373 qed. 286 374 287 375 lemma stmt_at_sigma_commute:
Note: See TracChangeset
for help on using the changeset viewer.