Changeset 2484 for src/joint/lineariseProof.ma
- Timestamp:
- Nov 22, 2012, 6:40:31 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/joint/lineariseProof.ma
r2481 r2484 120 120 ≠ None …. 121 121 122 definition well_formed_status:123 ∀p,p' ,graph_prog.122 definition sigma_beval_opt : 123 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p). 124 124 ((Σi.is_internal_function_of_program … graph_prog i) → 125 label → option ℕ) → 126 state_pc (make_sem_graph_params p p') → Prop ≝ 127 λp,p',prog,sigma,st. 128 well_formed_pc p p' prog sigma (pc … st) ∧ ?. 129 cases daemon (* TODO *) 130 qed. 125 code_point (mk_graph_params p) → option ℕ) → 126 beval → option beval ≝ 127 λp,p',graph_prog,sigma,bv. 128 match bv with 129 [ BVpc pc prt ⇒ ! pc' ← sigma_pc_opt p p' graph_prog sigma pc ; return BVpc pc' prt 130 | _ ⇒ return bv 131 ]. 132 133 definition sigma_beval : 134 ∀p,p',graph_prog,sigma,bv. 135 sigma_beval_opt p p' graph_prog sigma bv ≠ None ? → beval ≝ 136 λp,p',graph_prog,sigma,bv.opt_safe …. 131 137 132 138 (* … … 165 171 λp,p',graph_prog,sigma,st.opt_safe …. 166 172 167 lemma sigma_pc_o f_status_ok:173 lemma sigma_pc_ok: 168 174 ∀p,p',graph_prog. 169 175 ∀sigma. … … 174 180 #p #p' #graph_prog #sigma #st #prf @opt_to_opt_safe qed. 175 181 176 definition sigma_state :177 ∀p.178 ∀p':∀F.sem_unserialized_params p F.179 ∀graph_prog.180 ∀sigma.181 (* let lin_prog ≝ linearise ? graph_prog in *)182 ∀s:state_pc (make_sem_graph_params p p'). (* = graph_abstract_status p p' graph_prog stack_sizes *)183 well_formed_status p p' graph_prog sigma s →184 state_pc (make_sem_lin_params p p') (* = lin_abstract_status p p' lin_prog ? *)185 ≝186 λp,p',graph_prog,sigma,s,prf.187 let pc' ≝ sigma_pc … (proj1 … prf) in188 mk_state_pc ? ? pc'.189 cases daemon (* TODO *) qed.190 191 lemma sigma_pc_commute:192 ∀p,p',graph_prog,sigma,st.193 ∀prf : well_formed_status p p' graph_prog sigma st.194 sigma_pc … (pc ? st) (proj1 … prf) =195 pc ? (sigma_state … st prf).196 #p #p' #prog #sigma #st #prf %197 qed.198 199 lemma res_eq_from_opt :200 ∀A,m,v.res_to_opt A m = return v → m = return v.201 #A * #x #v normalize #EQ destruct % qed.202 203 182 definition sigma_function_name : 204 183 ∀p,graph_prog. … … 207 186 (Σf.is_internal_function_of_program … lin_prog f) ≝ 208 187 λp,graph_prog,f.«f, if_propagate … (pi2 … f)». 188 189 record good_sigma_state (p : unserialized_params) 190 (p' : ∀F.sem_unserialized_params p F) (graph_prog : ?) 191 (sigma : (Σi.is_internal_function_of_program (joint_closed_internal_function (mk_graph_params p)) 192 graph_prog i) → 193 label → option ℕ) 194 : Type[0] ≝ 195 { well_formed_state : state (make_sem_graph_params p p') → Prop 196 ; sigma_state : ∀st.well_formed_state st → state (make_sem_lin_params p p') 197 198 ; acca_store_ok : 199 ∀a,bv,bv',st,st',prf1,prf2. 200 sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' → 201 acca_store ?? (p' ?) a bv st = return st' → 202 acca_store … (p' ?) a bv' (sigma_state st prf1) = return sigma_state st' prf2 203 ; acca_store_wf : ∀a,bv,bv',st,st'. 204 sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' → 205 acca_store ?? (p' ?) a bv st = return st' → 206 well_formed_state st → well_formed_state st' 207 208 ; acca_retrieve_ok : 209 ∀a,st,bv,prf1,prf2. 210 acca_retrieve ?? (p' ?) st a = return bv → 211 acca_retrieve ?? (p' ?) (sigma_state st prf1) a = 212 return sigma_beval p p' graph_prog sigma bv prf2 213 ; acca_retrieve_wf : ∀a,st,bv. 214 acca_retrieve ?? (p' ?) st a = return bv → 215 well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ? 216 217 ; acca_arg_retrieve_ok : 218 ∀a,st,bv,prf1,prf2. 219 acca_arg_retrieve ?? (p' ?) st a = return bv → 220 acca_arg_retrieve ?? (p' ?) (sigma_state st prf1) a = 221 return sigma_beval p p' graph_prog sigma bv prf2 222 ; acca_arg_retrieve_wf : ∀a,st,bv. 223 acca_arg_retrieve ?? (p' ?) st a = return bv → 224 well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ? 225 226 ; accb_store_ok : 227 ∀a,bv,bv',st,st',prf1,prf2. 228 sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' → 229 accb_store ?? (p' ?) a bv st = return st' → 230 accb_store … (p' ?) a bv' (sigma_state st prf1) = return sigma_state st' prf2 231 ; accb_store_wf : ∀a,bv,bv',st,st'. 232 sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' → 233 accb_store ?? (p' ?) a bv st = return st' → 234 well_formed_state st → well_formed_state st' 235 236 ; accb_retrieve_ok : 237 ∀a,st,bv,prf1,prf2. 238 accb_retrieve ?? (p' ?) st a = return bv → 239 accb_retrieve ?? (p' ?) (sigma_state st prf1) a = 240 return sigma_beval p p' graph_prog sigma bv prf2 241 ; accb_retrieve_wf : ∀a,st,bv. 242 accb_retrieve ?? (p' ?) st a = return bv → 243 well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ? 244 245 ; accb_arg_retrieve_ok : 246 ∀a,st,bv,prf1,prf2. 247 acca_arg_retrieve ?? (p' ?) st a = return bv → 248 acca_arg_retrieve ?? (p' ?) (sigma_state st prf1) a = 249 return sigma_beval p p' graph_prog sigma bv prf2 250 ; accb_arg_retrieve_wf : ∀a,st,bv. 251 accb_arg_retrieve ?? (p' ?) st a = return bv → 252 well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ? 253 254 255 ; dpl_store_ok : 256 ∀a,bv,bv',st,st',prf1,prf2. 257 sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' → 258 dpl_store ?? (p' ?) a bv st = return st' → 259 dpl_store … (p' ?) a bv' (sigma_state st prf1) = return sigma_state st' prf2 260 ; dpl_store_wf : ∀a,bv,bv',st,st'. 261 sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' → 262 dpl_store ?? (p' ?) a bv st = return st' → 263 well_formed_state st → well_formed_state st' 264 265 ; dpl_retrieve_ok : 266 ∀a,st,bv,prf1,prf2. 267 dpl_retrieve ?? (p' ?) st a = return bv → 268 dpl_retrieve ?? (p' ?) (sigma_state st prf1) a = 269 return sigma_beval p p' graph_prog sigma bv prf2 270 ; dpl_retrieve_wf : ∀a,st,bv. 271 dpl_retrieve ?? (p' ?) st a = return bv → 272 well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ? 273 274 ; dpl_arg_retrieve_ok : 275 ∀a,st,bv,prf1,prf2. 276 acca_arg_retrieve ?? (p' ?) st a = return bv → 277 acca_arg_retrieve ?? (p' ?) (sigma_state st prf1) a = 278 return sigma_beval p p' graph_prog sigma bv prf2 279 ; dpl_arg_retrieve_wf : ∀a,st,bv. 280 dpl_arg_retrieve ?? (p' ?) st a = return bv → 281 well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ? 282 283 284 ; dph_store_ok : 285 ∀a,bv,bv',st,st',prf1,prf2. 286 sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' → 287 dph_store ?? (p' ?) a bv st = return st' → 288 dph_store … (p' ?) a bv' (sigma_state st prf1) = return sigma_state st' prf2 289 ; dph_store_wf : ∀a,bv,bv',st,st'. 290 sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' → 291 dph_store ?? (p' ?) a bv st = return st' → 292 well_formed_state st → well_formed_state st' 293 294 ; dph_retrieve_ok : 295 ∀a,st,bv,prf1,prf2. 296 dph_retrieve ?? (p' ?) st a = return bv → 297 dph_retrieve ?? (p' ?) (sigma_state st prf1) a = 298 return sigma_beval p p' graph_prog sigma bv prf2 299 ; dph_retrieve_wf : ∀a,st,bv. 300 dph_retrieve ?? (p' ?) st a = return bv → 301 well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ? 302 303 ; dph_arg_retrieve_ok : 304 ∀a,st,bv,prf1,prf2. 305 acca_arg_retrieve ?? (p' ?) st a = return bv → 306 acca_arg_retrieve ?? (p' ?) (sigma_state st prf1) a = 307 return sigma_beval p p' graph_prog sigma bv prf2 308 ; dph_arg_retrieve_wf : ∀a,st,bv. 309 dph_arg_retrieve ?? (p' ?) st a = return bv → 310 well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ? 311 312 313 ; snd_arg_retrieve_ok : 314 ∀a,st,bv,prf1,prf2. 315 snd_arg_retrieve ?? (p' ?) st a = return bv → 316 snd_arg_retrieve ?? (p' ?) (sigma_state st prf1) a = 317 return sigma_beval p p' graph_prog sigma bv prf2 318 ; snd_arg_retrieve_wf : ∀a,st,bv. 319 snd_arg_retrieve ?? (p' ?) st a = return bv → 320 well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ? 321 322 ; pair_reg_move_ok : 323 ∀mv,st1,st2,prf1,prf2. 324 pair_reg_move ?? (p' ?) st1 mv = return st2 → 325 pair_reg_move ?? (p' ?) (sigma_state st1 prf1) mv = 326 return sigma_state st2 prf2 327 ; pair_reg_move_wf : 328 ∀mv,st1,st2. 329 pair_reg_move ?? (p' ?) st1 mv = return st2 → 330 well_formed_state st1 → well_formed_state st2 331 332 ; allocate_locals_ok : 333 ∀l,st1,prf1,prf2. 334 allocate_locals ?? (p' ?) l (sigma_state st1 prf1) = 335 sigma_state (allocate_locals ?? (p' ?) l st1) prf2 336 ; allocate_locals_wf : 337 ∀l,st1. 338 well_formed_state st1 → 339 well_formed_state (allocate_locals ?? (p' ?) l st1) 340 341 ; save_frame_ok : 342 ∀dest,st1,st2,prf1,prf2. 343 save_frame ?? (p' ?) dest st1 = return st2 → 344 let st1' ≝ mk_state_pc … (sigma_state st1 (proj2 … prf1)) 345 (sigma_pc p p' graph_prog sigma (pc … st1) (proj1 … prf1)) in 346 save_frame ?? (p' ?) dest st1' = return sigma_state st2 prf2 347 ; save_frame_wf : 348 ∀dest,st1,st2. 349 save_frame ?? (p' ?) dest st1 = return st2 → 350 (well_formed_pc p p' graph_prog sigma (pc … st1) ∧ 351 well_formed_state st1) → well_formed_state st2 352 353 ; eval_ext_seq_ok : 354 let lin_prog ≝ linearise p graph_prog in 355 ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. 356 let stack_sizes' ≝ 357 stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') 358 ? graph_prog stack_sizes in 359 ∀ext,fn,st1,st2,prf1,prf2. 360 eval_ext_seq ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes')) 361 ext fn st1 = return st2 → 362 eval_ext_seq ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes)) 363 ext (sigma_function_name … fn) (sigma_state st1 prf1) = return sigma_state st2 prf2 364 ; eval_ext_seq_wf : 365 let lin_prog ≝ linearise p graph_prog in 366 ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. 367 let stack_sizes' ≝ 368 stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') 369 ? graph_prog stack_sizes in 370 ∀ext,fn,st1,st2. 371 eval_ext_seq ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes')) 372 ext fn st1 = return st2 → 373 well_formed_state st1 → well_formed_state st2 374 375 }. 376 377 (* restano: 378 ; setup_call : nat → paramsT … uns_pars → call_args uns_pars → 379 state st_pars → res (state st_pars) 380 ; fetch_external_args: external_function → state st_pars → call_args … uns_pars → 381 res (list val) 382 ; set_result: list val → call_dest uns_pars → state st_pars → res (state st_pars) 383 384 (* from now on, parameters that use the type of functions *) 385 ; read_result: ∀globals.genv_gen F globals → call_dest uns_pars → state st_pars → res (list beval) 386 (* change of pc must be left to *_flow execution *) 387 ; pop_frame: ∀globals.∀ge : genv_gen F globals. 388 (Σi.is_internal_function … ge i) (* current *) → state st_pars → res (state st_pars) 389 *) 390 391 definition well_formed_state_pc : 392 ∀p,p',graph_prog,sigma. 393 good_sigma_state p p' graph_prog sigma → 394 state_pc (make_sem_graph_params p p') → Prop ≝ 395 λp,p',prog,sigma,gss,st. 396 well_formed_pc p p' prog sigma (pc … st) ∧ well_formed_state … gss st. 397 398 definition sigma_state_pc : 399 ∀p. 400 ∀p':∀F.sem_unserialized_params p F. 401 ∀graph_prog. 402 ∀sigma. 403 (* let lin_prog ≝ linearise ? graph_prog in *) 404 ∀gss : good_sigma_state p p' graph_prog sigma. 405 ∀s:state_pc (make_sem_graph_params p p'). (* = graph_abstract_status p p' graph_prog stack_sizes *) 406 well_formed_state_pc p p' graph_prog sigma gss s → 407 state_pc (make_sem_lin_params p p') (* = lin_abstract_status p p' lin_prog ? *) 408 ≝ 409 λp,p',graph_prog,sigma,gss,s,prf. 410 let pc' ≝ sigma_pc … (proj1 … prf) in 411 let st' ≝ sigma_state … (proj2 … prf) in 412 mk_state_pc ? st' pc'. 413 414 (* 415 lemma sigma_pc_commute: 416 ∀p,p',graph_prog,sigma,gss,st. 417 ∀prf : well_formed_state_pc p p' graph_prog sigma gss st. 418 sigma_pc … (pc ? st) (proj1 … prf) = 419 pc ? (sigma_state_pc … st prf). // qed. 420 *) 421 422 lemma res_eq_from_opt : 423 ∀A,m,v.res_to_opt A m = return v → m = return v. 424 #A * #x #v normalize #EQ destruct % qed. 209 425 210 426 lemma if_of_function_commute: … … 358 574 *) 359 575 360 lemma int_funct_of_block_transf _commute:576 lemma int_funct_of_block_transf: 361 577 ∀A,B.∀progr: program (λvars. fundef (A vars)) ℕ. 362 578 ∀transf: ∀vars. A vars → B vars. ∀bl,f,prf. … … 393 609 >(sigma_pblock_eq_lemma … prf) #H 394 610 lapply (opt_eq_from_res ???? H) -H #H 395 >(int_funct_of_block_transf _commute?? graph_prog (λvars,graph_fun.\fst (linearise_int_fun … graph_fun)) ??? H)611 >(int_funct_of_block_transf ?? graph_prog (λvars,graph_fun.\fst (linearise_int_fun … graph_fun)) ??? H) 396 612 // 397 613 qed. … … 457 673 qed. *) 458 674 675 lemma opt_Exists_elim: 676 ∀A:Type[0].∀P:A → Prop. 677 ∀o:option A. 678 opt_Exists A P o → 679 ∃v:A. o = Some … v ∧ P v. 680 #A #P * normalize /3/ * 681 qed. 682 683 459 684 lemma stmt_at_sigma_commute: 460 685 ∀p,graph_prog,graph_fun,lbl,pt. … … 470 695 (joint_if_code ?? (if_of_function ?? lin_fun)) 471 696 pt = return (graph_to_lin_statement … stmt). 472 #p #graph_prog #graph_fun #lbl #pt #sigma #good #prf 473 (* 697 #p #graph_prog #graph_fun #lbl #pt #sigma #good #prf #stmt 698 cases (good graph_fun (pi2 … (sigma_function_name p graph_prog graph_fun))) 699 #sigma_entry_is_zero #lin_stmt_spec 700 lapply (lin_stmt_spec lbl pt prf) -lin_stmt_spec * #stmt1 * 701 #EQlookup_stmt1 #H 702 elim (opt_Exists_elim … H) -H * #optlbl_graph_stmt #graph_stmt 703 * #EQnth_opt_graph_stmt normalize nodelta 704 * #optEQlbl_optlbl_graph_stmt #next_spec 705 whd in match (stmt_at ????) in ⊢ (% → ?); 706 normalize nodelta 707 >EQlookup_stmt1 whd in ⊢ ((???%) → ?); #EQ destruct(EQ) 708 whd in match (stmt_at ????); > EQnth_opt_graph_stmt 709 normalize nodelta elim optEQlbl_optlbl_graph_stmt #_ #EQ >EQ // 710 qed. 711 (* 712 713 >(if_of_function_commute … graph_fun) 714 715 check opt_Exists 716 check linearise_int_fun 717 check 474 718 whd in match (stmt_at ????); 475 719 whd in match (stmt_at ????); … … 486 730 #related_lin_stm_graph_stm #_ <related_lin_stm_graph_stm -related_lin_stm_graph_stm 487 731 <sigma_pc_commute >lin_lookup_ok // *) 488 cases daemon489 qed.490 732 491 733 lemma fetch_statement_sigma_commute: … … 516 758 qed. 517 759 760 lemma point_of_pc_sigma_commute : 761 ∀p,p',graph_prog. 762 let lin_prog ≝ linearise p graph_prog in 763 ∀sigma,pc,fn,n. 764 ∀prf : well_formed_pc p p' graph_prog sigma pc. 765 int_funct_of_block … (globalenv_noinit … graph_prog) (pc_block pc) = return fn → 766 sigma fn (point_of_pc ? (make_sem_graph_params p p') pc) = return n → 767 point_of_pc ? (make_sem_lin_params p p') (sigma_pc … pc prf) = n. 768 #p #p' #graph_prog #sigma #pc #fn #n #prf #EQfetch #EQsigma 769 whd in match sigma_pc; normalize nodelta 770 @opt_safe_elim #pc' whd in match sigma_pc_opt; 771 normalize nodelta >EQfetch >m_return_bind >EQsigma 772 >m_return_bind whd in ⊢ (??%?→?); #EQ destruct(EQ) 773 change with (point_of_offset ??? = ?) @point_of_offset_of_point 774 qed. 775 518 776 definition linearise_status_rel: 519 777 ∀p,p',graph_prog. … … 523 781 stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') 524 782 ? graph_prog stack_sizes in 525 ∀sigma .783 ∀sigma,gss. 526 784 good_sigma p graph_prog sigma → 527 785 status_rel 528 786 (graph_abstract_status p p' graph_prog stack_sizes') 529 787 (lin_abstract_status p p' lin_prog stack_sizes) 530 ≝ λp,p',graph_prog,stack_sizes,sigma,g ood.788 ≝ λp,p',graph_prog,stack_sizes,sigma,gss,good. 531 789 mk_status_rel … 532 790 (* sem_rel ≝ *) (λs1,s2. 533 ∃prf: well_formed_stat us p p' graph_prog sigmas1.534 s2 = sigma_state … s1 prf)791 ∃prf: well_formed_state_pc p p' graph_prog sigma gss s1. 792 s2 = sigma_state_pc … s1 prf) 535 793 (* call_rel ≝ *) (λs1,s2. 536 ∃prf:well_formed_stat us p p' graph_prog sigmas1.794 ∃prf:well_formed_state_pc p p' graph_prog sigma gss s1. 537 795 pc ? s2 = sigma_pc … (pc ? s1) (proj1 … prf)) 538 796 (* sim_final ≝ *) ?. … … 544 802 #res #_ 545 803 #H lapply (res_eq_from_opt ??? H) -H 546 #H elim (bind_inversion ????? H) 804 cases daemon 805 (*#H elim (bind_inversion ????? H) in ⊢ ?; 547 806 * #f #stmt * 548 whd in ⊢ (??%?→?); 549 cases daemon 807 whd in ⊢ (??%?→?);*) 550 808 qed. 551 552 (* To be added to common/Globalenvs, it strenghtens553 find_funct_ptr_transf *)554 (*555 lemma556 find_funct_ptr_transf_eq:557 ∀A,B,V,iV. ∀p: program A V. ∀transf: (∀vs. A vs → B vs).558 ∀b: block.559 find_funct_ptr ? (globalenv … iV (transform_program … p transf)) b =560 m_map ???561 (transf …)562 (find_funct_ptr ? (globalenv … iV p) b).563 #A #B #V #iV #p #transf #b inversion (find_funct_ptr ???) in ⊢ (???%);564 [ cases daemon (* TODO in Globalenvs.ma *)565 | #f #H >(find_funct_ptr_transf A B … H) // ]566 qed.567 *)568 569 570 (*lemma fetch_function_sigma_commute:571 ∀p,p',graph_prog,sigma,st1.572 ∀prf:well_formed_status ??? sigma st1.573 let lin_prog ≝ linearise ? graph_prog in574 fetch_function575 (lin_prog_params p p' lin_prog)576 (globals (lin_prog_params p p' lin_prog))577 (ev_genv (lin_prog_params p p' lin_prog))578 (pc (lin_prog_params p p' lin_prog)579 (linearise_status_fun p p' graph_prog sigma st1 prf))580 =581 m_map …582 (linearise_int_fun ??)583 (fetch_function584 (graph_prog_params p p' graph_prog)585 (globals (graph_prog_params p p' graph_prog))586 (ev_genv (graph_prog_params p p' graph_prog))587 (pc (graph_prog_params p p' graph_prog) st1)).588 #p #p' #prog #sigma #st #prf whd in match fetch_function; normalize nodelta589 whd in match function_of_block; normalize nodelta590 >(find_funct_ptr_transf_eq … (λglobals.transf_fundef … (linearise_int_fun … globals)) …)591 cases (find_funct_ptr ???) // * //592 qed.593 *)594 809 595 810 lemma IO_bind_inversion: … … 603 818 ] qed. 604 819 605 lemma opt_Exists_elim: 606 ∀A:Type[0].∀P:A → Prop. 607 ∀o:option A. 608 opt_Exists A P o → 609 ∃v:A. o = Some … v ∧ P v. 610 #A #P * normalize /3/ * 611 qed. 820 lemma err_eq_from_io : ∀O,I,X,m,v. 821 err_to_io O I X m = return v → m = return v. 822 #O #I #X * #x #v normalize #EQ destruct % qed. 823 824 lemma eval_seq_no_pc_sigma_commute : 825 ∀p,p',graph_prog. 826 let lin_prog ≝ linearise p graph_prog in 827 ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. 828 let stack_sizes' ≝ 829 stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') 830 ? graph_prog stack_sizes in 831 ∀sigma.∀gss : good_sigma_state … graph_prog sigma. 832 ∀fn,st,stmt,st'. 833 ∀prf : well_formed_state … gss st.∀prf'. 834 eval_seq_no_pc ?? (ev_genv … (graph_prog_params … graph_prog stack_sizes')) 835 fn st stmt = return st' → 836 eval_seq_no_pc ?? (ev_genv … (lin_prog_params … lin_prog stack_sizes)) 837 (sigma_function_name … fn) (sigma_state … gss st prf) stmt = 838 return sigma_state … gss st' prf'. 839 #p #p' #graph_prog #stack_sizes #sigma #gss 840 #fn #st #stmt 841 #st' #prf #prf' 842 cases daemon (* 843 whd in match eval_seq_no_pc; 844 cases stmt normalize nodelta 845 [1,2: #_ #EQ whd in EQ : (??%%); destruct(EQ) // 846 | #mv_sig whd in match pair_reg_move in ⊢ (%→?); normalize nodelta 847 #H 848 ] *) 849 qed. 612 850 613 851 inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝ 614 852 ex1_intro: ∀ x:A. P x → ex_Type1 A P. 615 853 (*interpretation "exists in Type[1]" 'exists x = (ex_Type1 ? x).*) 616 617 lemma err_eq_from_io : ∀O,I,X,m,v.618 err_to_io O I X m = return v → m = return v.619 #O #I #X * #x #v normalize #EQ destruct % qed.620 854 621 855 lemma linearise_ok: … … 626 860 stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') 627 861 ? graph_prog lin_stack_sizes in 862 (∀sigma.good_sigma_state p p' graph_prog sigma) → 628 863 ex_Type1 … (λR. 629 864 status_simulation … … 633 868 cases (linearise_spec … graph_prog) #sigma #good 634 869 #lin_stack_sizes 635 %{(linearise_status_rel p p' graph_prog lin_stack_sizes sigma good)} 636 whd whd in ⊢ (%→%→?); 637 change with (∀st1 : state_pc (p' (joint_closed_internal_function (mk_graph_params ?))).?) 638 #st1 639 change with (∀st1 : state_pc (p' (joint_closed_internal_function (mk_graph_params ?))).?) 640 #st1' 641 change with (∀st : state_pc (p' (joint_closed_internal_function (mk_lin_params ?))).?) 642 #st2 643 #ex * #wfprf #rel_st1_st2 644 whd in ex; 645 change with 646 (eval_state 647 (make_sem_graph_params p p') 648 (prog_var_names ?? graph_prog) 649 ? 650 st1 = ?) in ex; 651 whd in match eval_state in ex; 652 normalize nodelta in ex; 653 cases (IO_bind_inversion ??????? ex) in ⊢ ?; * #fn #stmt 654 change with (Σi.is_internal_function_of_program … graph_prog i) in fn; * 655 change with (globalenv_noinit ? graph_prog) in 656 ⊢ (??(???%?)?→?); 657 match (ge ?? (ev_genv ?)) in ⊢ (%→?); 658 st1' 870 #gss lapply (gss sigma) -gss #gss 871 %{(linearise_status_rel p p' graph_prog lin_stack_sizes sigma gss good)} 872 whd in match graph_abstract_status; 873 whd in match lin_abstract_status; 874 whd in match graph_prog_params; 875 whd in match lin_prog_params; 876 normalize nodelta 877 whd 878 whd in ⊢ (%→%→%→?); 879 whd in ⊢ (?(?%)→?(?%)→?(?%)→?); 880 whd in ⊢ (?%→?%→?%→?); 881 #st1 #st1' #st2 882 whd in ⊢ (%→?); 883 change with 884 (eval_state (make_sem_graph_params p p') (prog_var_names ???) ?? = ? → ?) 885 whd in match eval_state in ⊢ (%→?); normalize nodelta 886 change with (Σi.is_internal_function_of_program ? graph_prog i) in 887 match (Sig ??) in ⊢ (%→?); 888 letin globals ≝ (prog_var_names ?? graph_prog) 889 change with (fetch_statement ??? (globalenv_noinit ? graph_prog) ?) in 890 match (fetch_statement ?????) in ⊢ (%→?); 891 #ex 892 cases (IO_bind_inversion ??????? ex) in ⊢ ?; * #fn #stmt * -ex 893 #EQfetch lapply (err_eq_from_io ????? EQfetch) -EQfetch 894 #EQfetch 895 cases (bind_inversion ????? EQfetch) 896 #f_id * #H lapply (opt_eq_from_res ???? H) -H 897 #EQfunc_of_block 898 #H elim (bind_inversion ????? H) -H #stmt' * 899 #H lapply (opt_eq_from_res ???? H) -H #EQstmt_at 900 whd in ⊢ (??%%→?); #EQ destruct(EQ) 901 #EQeval 902 cases (good fn (pi2 … (sigma_function_name p graph_prog fn))) 903 letin graph_fun ≝ (if_of_function … fn) in EQstmt_at; #EQstmt_at 904 #entry_0 905 #good_local 906 * * #wf_pc #wf_state #EQst2 907 generalize in match wf_pc in ⊢ ?; 908 whd in ⊢ (%→?); 909 inversion (sigma_pc_opt ?????) in ⊢ (%→?); [ #_ * #ABS elim (ABS ?) % ] 910 #lin_pc 911 whd in match (sigma_pc_opt) in ⊢ (%→?); normalize nodelta 912 >EQfunc_of_block in ⊢ (%→?); >m_return_bind in ⊢ (%→?); 913 #H elim (bind_opt_inversion ????? H) in ⊢ ?; -H #lin_pt * 914 #EQsigma whd in ⊢ (??%?→?); #EQ destruct(EQ) #_ 915 elim (good_local … EQsigma) -good_local 916 #stmt' * 917 change with (stmt_at ?? (joint_if_code ?? graph_fun) ? = ? → ?) 918 >EQstmt_at #EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ) 919 #H elim (opt_Exists_elim … H) -H * #lbl_opt #lin_stmt normalize nodelta 920 >(prog_if_of_function_transform … fn) in ⊢ (%→?); [2: % ] 921 change with graph_fun in match (if_of_function ?? fn) in ⊢ (%→?); 922 letin lin_fun ≝ (\fst (linearise_int_fun p globals graph_fun)) 923 change with globals in match (prog_var_names ?? graph_prog) in ⊢ (%→?); 924 * 925 #EQnth_opt ** #opt_lbl_spec #EQ destruct(EQ) #next_spec 926 letin lin_prog ≝ (linearise … graph_prog) 927 lapply (refl … (eval_state ? globals (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) st2)) 928 destruct(EQst2) 929 whd in match eval_state in ⊢ (???%→?); normalize nodelta 930 letin st2 ≝ (sigma_state_pc ????? st1 ?) 931 >(fetch_statement_sigma_commute … good … EQfetch) in ⊢ (%→?); 932 >m_return_bind in ⊢ (%→?); 933 #ex' 934 (* resolve classifier *) 659 935 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]); 660 >fetch_statement_spec in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]); 936 >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]); 937 normalize nodelta 938 cases stmt in EQfetch EQeval EQstmt_at EQnth_opt next_spec ex'; 939 [ * 940 [ #stmt #nxt 941 whd in match eval_statement in ⊢ (?→%→?); normalize nodelta 942 #EQfetch #EQeval #EQstmt_at #EQnth_opt #next_spec 943 whd in match (graph_to_lin_statement ???) in ⊢ (%→?); 944 whd in match eval_statement in ⊢ (%→?); normalize nodelta 945 elim (IO_bind_inversion ??????? EQeval) #st1_no_pc * 946 #EQeval_no_pc #EQeval_pc 947 >(eval_seq_no_pc_sigma_commute … EQeval_no_pc) 948 [2: (*TODO lemma eval_seq_no_pc_wf *) @hide_prf cases daemon ] 949 >m_return_bind 950 cases stmt in EQfetch EQeval_no_pc EQeval_pc EQstmt_at EQnth_opt next_spec; 951 [14: #f #args #dest 952 | #c 953 | #lbl 954 | #move_sig 955 | #a 956 | #a 957 | #sy #sy_prf #dpl #dph 958 | #op #a #b #arg1 #arg2 959 | #op #a #arg 960 | #op #a #arg1 #arg2 961 || 962 | #a #dpl #dph 963 | #dpl #dph #a 964 | #s_ext 965 ] 966 [ (* CALL *) 967 |(*:*) 968 normalize nodelta 969 #EQfetch #EQeval_no_pc #EQeval_pc #EQstmt_at #EQnth_opt #next_spec 970 whd in match eval_seq_pc; normalize nodelta 971 #ex1 972 cases next_spec 973 [ #EQnext_sigma 974 %[2: %{(taaf_step … (taa_base …) ex1 ?)} 975 [ cases daemon (* TODO lemma joint_classify_sigma_commute *) ]|] 976 normalize nodelta 977 cut (? : Prop) [3: #R' % [ %{I R'} ] |*:] 978 [ cases daemon (* TODO lemma joint_label_sigma_commute *) 979 | % 980 [ (* TODO lemma well_formed_state_pc_preserve? *) @hide_prf cases daemon 981 | whd in match eval_seq_pc in EQeval_pc; 982 whd in EQeval_pc : (??%%); whd in EQeval_pc : (??(????%)?); 983 destruct (EQeval_pc) 984 whd in ⊢ (??%%); 985 change with (sigma_pc ??????) in match 986 (pc ? (sigma_state_pc ???????)); 987 whd in match (succ_pc ????) in ⊢ (??%%); 988 whd in match (point_of_succ ???) in ⊢ (??%%); 989 >(point_of_pc_sigma_commute … EQfunc_of_block EQsigma) 990 whd in match sigma_pc in ⊢ (???%); 991 whd in match sigma_pc_opt in ⊢ (???%); normalize nodelta 992 @opt_safe_elim #pc' 993 >EQfunc_of_block >m_return_bind 994 whd in match point_of_pc; normalize nodelta 995 >point_of_offset_of_point 996 >EQnext_sigma whd in ⊢ (??%?→?); 997 whd in match pc_of_point; normalize nodelta 998 #EQ destruct(EQ) 999 >sigma_pblock_eq_lemma % 1000 ] 1001 ] 1002 | -next_spec #next_spec 1003 % 1004 1005 1006 whd in ⊢ (?→???%→?); 1007 generalize in ⊢ (??%? → ???(????%) → ?); |*: skip] | #a #lbltrue #next 1008 ] #next change with label in next; 1009 | * 1010 [ #lbl 1011 | 1012 | #fl #f #args 1013 ] 1014 ] 1015 whd in match eval_statement in ⊢ (?→%→?); normalize nodelta 1016 #EQfetch #EQeval #EQstmt_at #EQnth_opt #next_spec 1017 normalize nodelta 1018 whd in match (graph_to_lin_statement ???) in ⊢ (%→?); 1019 whd in match eval_statement in ⊢ (%→?); normalize nodelta 1020 [ >m_return_bind in ⊢ (%→?); 1021 >m_return_bind in EQeval; 1022 1023 1024 1025 (* common for all non-call seq *) 1026 >m_return_bind in ⊢ (%→?); 1027 whd in ⊢ (??%%→?); #EQ destruct(EQ) 1028 >m_return_bind in ⊢ (%→?); 1029 1030 1031 #ex1 1032 lapply (refl … (eval_state ? globals (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) st2)) 1033 1034 whd in match (point_of_pc ???); 1035 whd in match (point_of_succ ???); 1036 whd in match sigma_pc in ⊢ (???%); normalize nodelta @opt_safe_elim 1037 #pc' #H 1038 elim (bind_opt_inversion ????? H) #fn * #EQbl 1039 -H #H 1040 elim (bind_opt_inversion ????? H) -H #n * #EQsigma whd in ⊢ (??%?→?); 1041 #EQ destruct(EQ) 1042 whd in match (succ_pc ????); 1043 whd in match (point_of_succ ???); 1044 change with (point_of_offset ???) in match (point_of_pc ???); 1045 >point_of_offset_of_point 1046 whd in match sigma_pc; normalize nodelta @opt_safe_elim 1047 #pc' whd in match sigma_pc_opt; normalize nodelta 1048 1049 1050 1051 whd in match (succ_pc ????); 1052 1053 change with next in match (offset_of_point ???) in ⊢ (???%); 661 1054 whd in fetch_statement_spec : (??()%); 662 1055 cases cl in classified_st1_cl; -cl #classified_st1_cl whd … … 676 1069 letin st2_opt' ≝ (eval_state … 677 1070 (ev_genv (lin_prog_params … lin_prog lin_stack_sizes)) 678 (sigma_state … wf_st1))1071 (sigma_state_pc … wf_st1)) 679 1072 cut (∃st2': lin_abstract_status p p' lin_prog lin_stack_sizes. st2_opt' = return st2') 680 1073 [cases daemon (* TODO, needs lemma? *)] * #st2' #st2_spec' … … 695 1088 | .... 696 1089 qed. 1090 1091 1092 1093 1094 1095 [ * 1096 [ * 1097 [ letin C_COMMENT ≝ 0 in ⊢ ?; #c 1098 | letin C_COST_LABEL ≝ 0 in ⊢ ?; #lbl 1099 | letin C_MOVE ≝ 0 in ⊢ ?; #move_sig 1100 | letin C_POP ≝ 0 in ⊢ ?; #a 1101 | letin C_PUSH ≝ 0 in ⊢ ?; #a 1102 | letin C_ADDRESS ≝ 0 in ⊢ ?; #sy #sy_prf #dpl #dph 1103 | letin C_OPACCS ≝ 0 in ⊢ ?; #op #a #b #arg1 #arg2 1104 | letin C_OP1 ≝ 0 in ⊢ ?; #op #a #arg 1105 | letin C_OP2 ≝ 0 in ⊢ ?; #op #a #arg1 #arg2 1106 | letin C_CLEAR_CARRY ≝ 0 in ⊢ ?; 1107 | letin C_SET_CARRY ≝ 0 in ⊢ ?; 1108 | letin C_LOAD ≝ 0 in ⊢ ?; #a #dpl #dph 1109 | letin C_STORE ≝ 0 in ⊢ ?; #dpl #dph #a 1110 | letin C_CALL ≝ 0 in ⊢ ?; #f #args #dest 1111 | letin C_EXT ≝ 0 in ⊢ ?; #s_ext 1112 ] 1113 | letin C_COND ≝ 0 in ⊢ ?; #a #lbltrue 1114 ] #next change with label in next; 1115 | * 1116 [ letin C_GOTO ≝ 0 in ⊢ ?; #lbl 1117 | letin C_RETURN ≝ 0 in ⊢ ?; 1118 | letin C_TAILCALL ≝ 0 in ⊢ ?; #fl #f #args 1119 ] 1120 ]
Note: See TracChangeset
for help on using the changeset viewer.