Changeset 2922
 Timestamp:
 Mar 21, 2013, 2:12:59 AM (4 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTLptr/ERTLptrToLTLProof.ma
r2898 r2922 340 340 <associative_append @split_on_last_append_singl 341 341 qed. 342 343 lemma injective_OK: ∀A:Type[0].∀a,b:A. OK … a = OK … b → a=b. 344 #A #a #b #EQ destruct % 345 qed. 346 347 lemma eq_notb_true_to_eq_false: 348 ∀b. (¬b) = true → b = false. 349 * // #abs normalize in abs; destruct 350 qed. 351 352 axiom sigma_fb_state_insensitive_to_dead_reg: 353 ∀fix_comp,colour,prog. 354 let p_in ≝ 355 mk_prog_params ERTLptr_semantics prog 356 (lookup_stack_cost (\snd (\fst (ertlptr_to_ltl fix_comp colour prog)))) in 357 ∀fn,f_lbls,f_regs,bv. 358 ∀st: joint_abstract_status p_in. 359 ∀r: register. 360 let live ≝ 361 analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) fn 362 in 363 set_member (identifier RegisterTag) (eq_identifier RegisterTag) r 364 (\fst (live (point_of_pc ERTLptr_semantics (pc p_in st)))) = false → 365 sigma_fb_state prog f_lbls f_regs 366 (to_be_cleared_fb live) 367 (set_regs ERTLptr_semantics 368 〈reg_store r bv (\fst (regs ERTLptr_semantics (st_no_pc … st))), 369 \snd (regs ERTLptr_semantics (st_no_pc … st))〉 (st_no_pc … st)) 370 = sigma_fb_state prog f_lbls f_regs (to_be_cleared_fb live) (st_no_pc … st). 371 372 axiom sigma_fb_state_insensitive_to_dead_Reg: 373 ∀fix_comp,colour,prog. 374 let p_in ≝ 375 mk_prog_params ERTLptr_semantics prog 376 (lookup_stack_cost (\snd (\fst (ertlptr_to_ltl fix_comp colour prog)))) in 377 ∀fn,f_lbls,f_regs,bv. 378 ∀st: joint_abstract_status p_in. 379 ∀r: Register. 380 let live ≝ 381 analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) fn 382 in 383 set_member Register eq_Register r 384 (\snd (live (point_of_pc ERTLptr_semantics (pc p_in st)))) = false → 385 sigma_fb_state prog f_lbls f_regs 386 (to_be_cleared_fb live) 387 (set_regs ERTLptr_semantics 388 〈\fst (regs ERTLptr_semantics (st_no_pc … st)), 389 hwreg_store r bv (\snd (regs ERTLptr_semantics (st_no_pc … st)))〉 390 (st_no_pc … st)) 391 = sigma_fb_state prog f_lbls f_regs 392 (to_be_cleared_fb live) (st_no_pc … st). 393 394 axiom sigma_fb_state_insensitive_to_dead_carry: 395 ∀fix_comp,colour,prog. 396 let p_in ≝ 397 mk_prog_params ERTLptr_semantics prog 398 (lookup_stack_cost (\snd (\fst (ertlptr_to_ltl fix_comp colour prog)))) in 399 ∀fn,f_lbls,f_regs,bv. 400 ∀st: joint_abstract_status p_in. 401 let live ≝ 402 analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) fn 403 in 404 set_member Register eq_Register RegisterCarry 405 (\snd (live (point_of_pc ERTLptr_semantics (pc p_in st)))) = false → 406 sigma_fb_state prog f_lbls f_regs 407 (to_be_cleared_fb live) 408 (set_carry ERTLptr_semantics bv (st_no_pc … st)) 409 = sigma_fb_state prog f_lbls f_regs (to_be_cleared_fb live) (st_no_pc … st). 410 411 lemma split_orb_false: ∀a,b:bool. orb a b = false → a = false ∧ b = false. 412 ** normalize #abs destruct /2/ 413 qed. 414 415 lemma sigma_fb_state_insensitive_to_eliminable: 416 ∀fix_comp: fixpoint_computer. 417 ∀colour: coloured_graph_computer. 418 ∀prog: ertlptr_program. 419 let p_in ≝ 420 mk_prog_params ERTLptr_semantics prog 421 (lookup_stack_cost (\snd (\fst (ertlptr_to_ltl fix_comp colour prog)))) in 422 ∀f,fn,f_lbls,f_regs. 423 ∀st1 : joint_abstract_status p_in. 424 ∀st1_no_pc,stms. 425 ∀Heval_seq_no_pc: 426 eval_seq_no_pc ERTLptr_semantics 427 (prog_var_names (joint_function ERTLptr_semantics) ℕ prog) 428 (ev_genv 429 (mk_prog_params ERTLptr_semantics prog 430 (lookup_stack_cost (\snd (\fst (ertlptr_to_ltl fix_comp colour prog)))))) 431 f stms (st_no_pc … st1) 432 =return st1_no_pc. 433 ∀Heliminable: 434 eliminable_step (globals p_in) 435 (analyse_liveness fix_comp (globals p_in) fn 436 (point_of_pc ERTLptr_semantics (pc p_in st1))) stms 437 =true. 438 (sigma_fb_state prog f_lbls f_regs 439 (to_be_cleared_fb 440 (analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) 441 fn)) 442 st1_no_pc 443 =sigma_fb_state prog f_lbls f_regs 444 (to_be_cleared_fb 445 (analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) 446 fn)) 447 (st_no_pc … st1)). 448 #fix_comp #colour #prog letin p_in ≝ (mk_prog_params ???) #f #fn #f_lbls #f_regs 449 #st1 #st1' * 450 try (#arg1 #arg2 #arg3 #arg4 #arg5 #Heval #Helim) 451 try (#arg1 #arg2 #arg3 #arg4 #Heval #Helim) 452 try (#arg1 #arg2 #arg3 #Heval #Helim) try (#arg1 #arg2 #Heval #Helim) 453 try (#arg1 #Heval #Helim) try (#Heval #Helim) 454 whd in Heval:(??%?); 455 whd in Helim:(??%?); try (change with (false=true) in Helim; destruct (Helim)) 456 [7: inversion arg1 in Heval Helim; [ * [3: #arg2 ] *: #arg2 #arg3 ] #Harg1 457 normalize nodelta ] try #Heval try #Helim whd in Heval:(??%?); 458 try (change with (false=true) in Helim; destruct (Helim)) 459 [4,8: cases arg1 in Heval Helim; normalize nodelta 460 [ * normalize nodelta #arg10 #arg11] #Heval #Helim] 461 lapply (eq_notb_true_to_eq_false ? Helim) Helim #Helim 462 [1,2: cases arg11 in Heval; [1,3: *] #arg12 whd in ⊢ (??%? → ?); 463 [1,3: whd in match (pair_reg_move_ ?????); normalize nodelta 464 inversion ps_reg_retrieve normalize nodelta 465 [2,4: #error #_ #abs whd in abs:(???%); destruct (abs) ] 466 #bv #EQbv ] 467 3,4,5,6,7,8,13: inversion (acca_arg_retrieve ERTLptr_semantics) in Heval; 468 [2,4,6,8,10,12,14: #error #_ #abs whd in abs:(??%%); destruct (abs) ] 469 #bv normalize nodelta #EQbv #X cases (bind_inversion ????? X) X 470 #v1 * #Hv1 #X cases (bind_inversion ????? X) X 471 #vres * #Hvres #X cases (bind_inversion ????? X) X 472 #st1'' * #Hst1'' 473 9: inversion (opt_to_res ???) in Heval; 474 [2: #error #_ #abs whd in abs:(??%%); destruct (abs) ] 475 #bv normalize nodelta #EQbv 476 10,11: inversion (get_pc_from_label ?????) in Heval; 477 [2,4: #error #_ #abs whd in abs:(??%%); destruct (abs) ] 478 #bv normalize nodelta #EQbv 479 12: lapply Heval Heval 480 14: inversion (acca_retrieve ???) in Heval; 481 [2: #error #_ #abs whd in abs:(??%%); destruct (abs) ] 482 #bv normalize nodelta #EQbv #X cases (bind_inversion ????? X) X 483 #v1 * #Hv1 484 15: inversion (dph_arg_retrieve ???) in Heval; 485 [2: #error #_ #abs whd in abs:(??%%); destruct (abs) ] 486 #bv normalize nodelta #EQbv #X cases (bind_inversion ????? X) X 487 #v1 * #Hv1 #X cases (bind_inversion ????? X) X 488 #vres * #Hvres #X cases (bind_inversion ????? X) X 489 #v1 * #Hv2 ] 490 whd in ⊢ (??%% → ?); #X <(injective_OK ??? X) X 491 try (cases (split_orb_false … Helim) Helim #Helim1 #Helim2) 492 try (@sigma_fb_state_insensitive_to_dead_reg assumption) 493 try (@sigma_fb_state_insensitive_to_dead_Reg assumption) 494 try (@sigma_fb_state_insensitive_to_dead_carry assumption) 495 [ <(injective_OK ??? Hst1'') XXX 496 >sigma_fb_state_insensitive_to_dead_carry assumption 497 @sigma_fb_state_insensitive_to_dead_carry 342 498 343 499 lemma make_ERTLptr_To_LTL_good_state_relation : … … 435 591 >(pc_of_label_eq … EQt_fn1) <(pc_eq_sigma_commute … good … EQfn Rst1st2) % 436 592 ] 437  xxxxxxxxxxxx 438 letin p_in ≝ (mk_prog_params ERTLptr_semantics ??) 439 letin p_out ≝ (mk_prog_params LTL_semantics ??) 593  letin p_in ≝ (mk_prog_params ERTLptr_semantics ??) 594 letin p_out ≝ (mk_prog_params LTL_semantics ??) 440 595 letin trans_prog ≝ (b_graph_transform_program ????) 441 #st1 #st1' #st2 #f #fn * 596 #st1 #st1' #st2 #f #fn 597 #stms #nxt #EQfetch whd in match eval_state in ⊢ (% → ?); 598 normalize nodelta >EQfetch >m_return_bind #H @('bind_inversion H) H 599 #st1_no_pc whd in match eval_statement_no_pc in ⊢ (% → ?); normalize nodelta 600 #Heval_seq_no_pc 601 whd in match eval_statement_advance; normalize nodelta 602 whd in ⊢ (??%% → ?); #EQ destruct(EQ) 603 whd in ⊢ (% → ?); #Rst1st2 #t_fn #EQt_fn 604 whd normalize nodelta 605 change with p_out in match p_out; 606 change with p_in in match p_in; 607 change with trans_prog in match trans_prog; 608 inversion eliminable_step #Heliminable normalize nodelta % 609 [ @([ ]) 610  % [%] % [2: % [%]  skip] whd 611 cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt >EQfn 612 % [2: % [2: % [%]  skip]  skip] 613 (* CSC: BEGIN cut&paste from previous case: make lemma? *) 614 lapply Rst1st2 whd in ⊢ (% → ?); whd in match sigma_fb_state_pc; 615 whd in match sigma_sb_state_pc; normalize nodelta >EQfn 616 <(pc_eq_sigma_commute … good … EQfn Rst1st2) >EQfn 617 normalize nodelta #EQ cases(state_pc_eq … EQ) * 618 #EQst1st2 #_ #_ 619 (* CSC: END *) 620 <EQst1st2 whd in EQst1_no_pc:(??%%); whd in match (st_no_pc ??); 621 622 623 624 625 626 <(injective_OK ??? EQst1_no_pc) 627 change with (set_regs ???) in match (st_no_pc ??); 628 629 630 * 442 631 [7: #op1 #dest #src #nxt #EQfetch whd in match eval_state in ⊢ (% → ?); 443 632 normalize nodelta >EQfetch >m_return_bind #H @('bind_inversion H) H … … 454 643 change with p_in in match p_in; 455 644 change with trans_prog in match trans_prog; 645 inversion eliminable_step #Heliminable normalize nodelta % 646 [ @([ ]) 647  % [%] % [2: % [%]  skip] whd 648 cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt >EQfn 649 % [2: % [2: % [%]  skip]  skip] 650 (* CSC: BEGIN cut&paste from previous case: make lemma? *) 651 lapply Rst1st2 whd in ⊢ (% → ?); whd in match sigma_fb_state_pc; 652 whd in match sigma_sb_state_pc; normalize nodelta >EQfn 653 <(pc_eq_sigma_commute … good … EQfn Rst1st2) >EQfn 654 normalize nodelta #EQ cases(state_pc_eq … EQ) * 655 #EQst1st2 #_ #_ 656 (* CSC: END *) 657 <EQst1st2 whd in EQst1_no_pc:(??%%); <(injective_OK ??? EQst1_no_pc) 658 change with (set_regs ???) in match (st_no_pc ??); 659 660 661 662 663 664 665 666 667 destruct (EQst1_no_pc) 668 669 <(insensitive_to_be_cleared_sb … prog f_lbls f_regs … st2 … 670 (point_of_pc ERTLptr_semantics (pc … st2))) 671 [2,4: @dead_registers_in_dead @acc_is_dead ] 672 assumption 673 674 Rst1st2 675 456 676 % [2: % [ %  ]  skip] 457 677 qed.
Note: See TracChangeset
for help on using the changeset viewer.