- Timestamp:
- Mar 25, 2013, 9:48:01 PM (8 years ago)
- Location:
- src
- Files:
-
- 3 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ERTLptr/ERTLptrToLTLProof.ma
r2944 r2949 266 266 ¬set_member A DEC a y → 267 267 set_member A DEC a (set_diff … x y). 268 axiom set_member_subset_if: 269 ∀A,DEC,S1,S2. 270 set_subset A DEC S1 S2 → 271 ∀x. set_member A DEC x S1 → set_member A DEC x S2. 272 axiom set_member_subset_onlyif: 273 ∀A,DEC,S1,S2. 274 (∀x. set_member A DEC x S1 → set_member A DEC x S2) → 275 set_subset A DEC S1 S2. 276 268 277 269 278 lemma all_used_are_live_before : … … 402 411 whd in match eliminable; normalize nodelta >Helim % 403 412 qed. 413 414 lemma set_subset_to_set_subst_set_union_left: 415 ∀T,eqT,A,B,C. set_subset T eqT A B → set_subset … eqT A (set_union … B C). 416 #T #eqT #A #B #C #H @set_member_subset_onlyif #x #K 417 lapply (set_member_subset_if … H) #H2 /3 by set_member_union1/ 418 qed. 419 420 lemma set_subset_to_set_subst_set_union_right: 421 ∀T,eqT,A,B,C. set_subset T eqT A C → set_subset … eqT A (set_union … B C). 422 #T #eqT #A #B #C #H @set_member_subset_onlyif #x #K 423 lapply (set_member_subset_if … H) #H2 /3 by set_member_union2/ 424 qed. 425 426 lemma rl_included_rl_join_left: 427 ∀A,B,C. rl_included A B → rl_included A (rl_join B C). 428 #A #B #C whd in match rl_included; normalize nodelta #H 429 cases (andb_Prop_true … H) -H #H1 #H2 @andb_Prop 430 /2 by set_subset_to_set_subst_set_union_left/ 431 qed. 432 433 lemma rl_included_rl_join_right: 434 ∀A,B,C. rl_included A C → rl_included A (rl_join B C). 435 #A #B #C whd in match rl_included; normalize nodelta #H 436 cases (andb_Prop_true … H) -H #H1 #H2 @andb_Prop 437 /2 by set_subset_to_set_subst_set_union_right/ 438 qed. 439 440 lemma set_subset_reflexive: ∀A,DEC,x. set_subset A DEC x x. 441 /2/ 442 qed. 443 444 lemma rl_included_reflexive: ∀x. rl_included x x. 445 /2/ 446 qed. 447 448 lemma mem_of_fold_join: 449 ∀F,dom. 450 ∀x. x ∈ dom → 451 rl_included (F x) 452 (fold label (l_property register_lattice) rl_join rl_bottom (λl:label.true) 453 F dom). 454 #F #dom elim dom [ #x * ] #hd #tl #IH #x whd in match (? ∈ ?); @eqb_elim 455 normalize nodelta #Hx #H change with (rl_join ??) in ⊢ (?(??%)); 456 destruct /3 by rl_included_rl_join_left,rl_included_rl_join_right/ 457 qed. 458 459 lemma set_subset_transitive: 460 ∀A,DEC,S1,S2,S3. 461 set_subset A DEC S1 S2 → set_subset … DEC S2 S3 → set_subset … DEC S1 S3. 462 #A #DEC #S1 #S2 #S3 463 #H1 lapply (set_member_subset_if … H1) -H1 #H1 464 #H2 lapply (set_member_subset_if … H2) -H2 #H2 465 @set_member_subset_onlyif /3 by/ 466 qed. 467 468 lemma rl_included_transitive: 469 ∀S1,S2,S3. rl_included S1 S2 → rl_included S2 S3 → rl_included S1 S3. 470 #S1 #S2 #S3 whd in match rl_included; normalize nodelta 471 #H cases (andb_Prop_true … H) -H #H1 #H2 472 #H cases (andb_Prop_true … H) -H #H3 #H4 473 /3 by andb_Prop,set_subset_transitive/ 474 qed. 475 476 lemma rl_included_rl_diff_rl_empty: 477 ∀S1. rl_included S1 (rl_diff S1 rl_bottom). 478 #S1 whd in match (rl_included ??); 479 lapply (set_member_subset_onlyif … (eq_identifier …) (\fst S1) (\fst (rl_diff S1 rl_bottom))) 480 cases (set_subset ????) 481 /3 by set_member_diff,set_member_subset_onlyif/ 482 qed. 483 484 lemma included_livebefore_livebeafter_stmt_labels: 485 ∀fix_comp,globals,fn,l,stmt. 486 let after ≝ analyse_liveness fix_comp globals fn in 487 stmt_at … (joint_if_code ERTLptr … fn) l = Some … stmt → 488 ∀nxt. 489 nxt ∈ 490 stmt_labels (mk_stmt_params (g_u_pars ERTLptr) label (Some label) false) 491 globals stmt → 492 l_included register_lattice (livebefore … fn after nxt) (after l). 493 #fix_comp #globals #fn #l #stmt letin after ≝ (analyse_liveness ???) #EQlookup #nxt 494 #Hnxt lapply (fix_correct … after l) #spec @(rl_included_transitive … spec) -spec 495 whd in match (liveafter ????); whd in EQlookup:(??%?); >EQlookup -EQlookup normalize nodelta 496 /2 by mem_of_fold_join/ 497 qed. 498 499 axiom eq_sigma_state_monotonicity: 500 ∀prog,live,graph,st1,st2,l1,l2. 501 rl_included (live l2) (live l1) → 502 sigma_fb_state prog (to_be_cleared_fb live l1) st1 = 503 sigma_sb_state prog (to_be_cleared_sb live graph l1) st2 → 504 sigma_fb_state prog (to_be_cleared_fb live l2) st1 = 505 sigma_sb_state prog (to_be_cleared_sb live graph l2) st2. 506 507 (* True and useless 508 axiom to_be_cleared_sb_respects_equal_valuations: 509 ∀live,coloured,l1,l2. 510 live l1 = live l2 → 511 to_be_cleared_sb live coloured l1 = to_be_cleared_sb live coloured l2. 512 513 axiom to_be_cleared_fb_respects_equal_valuations: 514 ∀live,l1,l2. 515 live l1 = live l2 → 516 to_be_cleared_fb live l1 = to_be_cleared_fb live l2. 517 *) 518 519 (* 520 lemma sigma_fb_state_insensitive_to_eliminable: 521 ∀fix_comp: fixpoint_computer. 522 ∀prog: ertlptr_program. 523 ∀stackcost. 524 let p_in ≝ mk_prog_params ERTLptr_semantics prog stackcost in 525 ∀f,fn. 526 let after ≝ analyse_liveness fix_comp (prog_var_names … prog) fn in 527 let before ≝ livebefore … fn after in 528 ∀st1 : joint_abstract_status p_in. 529 let pt ≝ point_of_pc ERTLptr_semantics (pc ? st1) in 530 ∀st1_no_pc. ∀stms: joint_seq ERTLptr_semantics (prog_var_names … prog). ∀next. 531 stmt_at p_in … (joint_if_code p_in … fn) pt = return (sequential … stms next) → 532 ∀Heval_seq_no_pc: 533 eval_seq_no_pc ERTLptr_semantics 534 (prog_var_names (joint_function ERTLptr_semantics) ℕ prog) 535 (ev_genv 536 (mk_prog_params ERTLptr_semantics prog stackcost)) 537 f stms (st_no_pc … st1) 538 =return st1_no_pc. 539 ∀Heliminable: 540 eliminable_step (globals p_in) 541 (after (point_of_pc ERTLptr_semantics (pc p_in st1))) stms =true. 542 sigma_fb_state prog (to_be_cleared_fb before next) st1_no_pc = 543 sigma_fb_state prog (to_be_cleared_fb before pt) (st_no_pc … st1). 544 #fix_comp #prog #stackcost letin p_in ≝ (mk_prog_params ???) #f #fn 545 letin after ≝ (analyse_liveness ???) 546 #st1 #st1' #stms #next #stmt_at #Heval #Helim 547 lapply (eliminable_step_to_eq_livebefore_liveafter … stmt_at … Helim) 548 #EQ_livebefore_after 549 cases stms in Heval Helim; 550 try (#arg1 #arg2 #arg3 #arg4 #arg5 #Heval #Helim) 551 try (#arg1 #arg2 #arg3 #arg4 #Heval #Helim) 552 try (#arg1 #arg2 #arg3 #Heval #Helim) try (#arg1 #arg2 #Heval #Helim) 553 try (#arg1 #Heval #Helim) try (#Heval #Helim) 554 whd in Heval:(??%?); 555 whd in Helim:(??%?); try (change with (false=true) in Helim; destruct (Helim)) 556 [7: inversion arg1 in Heval Helim; [ * [3: #arg2 ] |*: #arg2 #arg3 ] #Harg1 557 normalize nodelta ] try #Heval try #Helim whd in Heval:(??%?); 558 try (change with (false=true) in Helim; destruct (Helim)) 559 [4,8: cases arg1 in Heval Helim; normalize nodelta 560 [ * normalize nodelta #arg10 #arg11] #Heval #Helim] 561 lapply (eq_notb_true_to_eq_false ? Helim) -Helim #Helim 562 [1,2: cases arg11 in Heval; [1,3: *] #arg12 whd in ⊢ (??%? → ?); 563 [1,3: whd in match (pair_reg_move_ ?????); normalize nodelta 564 inversion ps_reg_retrieve normalize nodelta 565 [2,4: #error #_ #abs whd in abs:(???%); destruct (abs) ] 566 #bv #EQbv ] 567 |3,4,5,6,7,8,13: inversion (acca_arg_retrieve ERTLptr_semantics) in Heval; 568 [2,4,6,8,10,12,14: #error #_ #abs whd in abs:(??%%); destruct (abs) ] 569 #bv normalize nodelta #EQbv #X cases (bind_inversion ????? X) -X 570 #v1 * #Hv1 #X cases (bind_inversion ????? X) -X 571 #vres * #Hvres #X cases (bind_inversion ????? X) -X 572 #st1'' * #Hst1'' 573 |9: inversion (opt_to_res ???) in Heval; 574 [2: #error #_ #abs whd in abs:(??%%); destruct (abs) ] 575 #bv normalize nodelta #EQbv 576 |10,11: inversion (get_pc_from_label ?????) in Heval; 577 [2,4: #error #_ #abs whd in abs:(??%%); destruct (abs) ] 578 #bv normalize nodelta #EQbv 579 |12: lapply Heval -Heval 580 |14: inversion (acca_retrieve ???) in Heval; 581 [2: #error #_ #abs whd in abs:(??%%); destruct (abs) ] 582 #bv normalize nodelta #EQbv #X cases (bind_inversion ????? X) -X 583 #v1 * #Hv1 584 |15: inversion (dph_arg_retrieve ???) in Heval; 585 [2: #error #_ #abs whd in abs:(??%%); destruct (abs) ] 586 #bv normalize nodelta #EQbv #X cases (bind_inversion ????? X) -X 587 #v1 * #Hv1 #X cases (bind_inversion ????? X) -X 588 #vres * #Hvres #X cases (bind_inversion ????? X) -X 589 #v1 * #Hv2 ] 590 whd in ⊢ (??%% → ?); #X <(injective_OK ??? X) -X 591 try (cases (split_orb_false … Helim) -Helim #Helim1 #Helim2) 592 593 XXX 594 595 try (@sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption) 596 try (@sigma_fb_state_insensitive_to_dead_Reg >EQ_livebefore_after assumption) 597 try (@sigma_fb_state_insensitive_to_dead_carry >EQ_livebefore_after assumption) 598 [1,2,3,4,5,6,7: <(injective_OK ??? Hst1'') ] 599 [1,2,3: 600 >sigma_fb_state_insensitive_to_dead_carry try (>EQ_livebefore_after assumption) 601 @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption 602 |4: whd in Hvres:(??%%); cases Byte_of_val in Hvres; normalize nodelta 603 [2: #error #abs destruct (abs) ] 604 #by #Hvres; cases (bind_inversion ????? Hvres) #by' * #_ #EQ 605 whd in EQ:(??%%); destruct (EQ) >set_carry_set_regs_commute >eta_set_carry 606 @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption 607 |5,6: whd in Hvres:(??%%); cases bv in Hvres; normalize nodelta 608 try (#x1 #x2 #x3 #Hvres) try (#x1 #x2 #Hvres) try (#x1 #Hvres) try #Hvres 609 try (destruct (Hvres) @I) cases v1 in Hvres; normalize nodelta 610 try (#x1' #x2' #x3' #Hvres) try (#x1' #x2' #Hvres) try (#x1' #Hvres) try #Hvres 611 try (destruct (Hvres) @I) 612 [5: cases orb in Hvres; normalize nodelta try (#Hvres destruct(Hvres) @I) 613 cases andb normalize nodelta #Hvres 614 |9,10,11,12: cases cic:/matita/arithmetics/nat/eqb.fix(0,0,1) in Hvres; 615 normalize nodelta try (#abs destruct(abs) @I) #Hvres ] 616 whd in Hvres:(??%%); destruct (Hvres) >set_carry_set_regs_commute >eta_set_carry 617 @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption 618 |7: cases (split_orb_false … Helim1) -Helim1 #Helim1 #Helim3 619 >sigma_fb_state_insensitive_to_dead_reg try (>EQ_livebefore_after assumption) 620 @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption 621 |8: >sigma_fb_state_insensitive_to_dead_reg try (>EQ_livebefore_after assumption) 622 @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption ] 623 qed. 624 404 625 405 626 lemma sigma_fb_state_insensitive_to_eliminable: … … 502 723 |8: >sigma_fb_state_insensitive_to_dead_reg try (>EQ_livebefore_after assumption) 503 724 @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption ] 504 qed. 505 506 axiom to_be_cleared_sb_respects_equal_valuations: 507 ∀live,coloured,l1,l2. 508 live l1 = live l2 → 509 to_be_cleared_sb live coloured l1 = to_be_cleared_sb live coloured l2. 510 511 axiom to_be_cleared_fb_respects_equal_valuations: 512 ∀live,l1,l2. 513 live l1 = live l2 → 514 to_be_cleared_fb live l1 = to_be_cleared_fb live l2. 725 qed. *) 515 726 516 727 lemma make_ERTLptr_To_LTL_good_state_relation : … … 588 799 [2,4: @dead_registers_in_dead @acc_is_dead ] 589 800 whd >point_of_pc_of_point 801 @(eq_sigma_state_monotonicity … EQst1st2) 590 802 letin after ≝ (analyse_liveness fix_comp … fn) 591 letin before ≝ (livebefore … fn after) 592 [ cut 593 (before ltrue = 594 before (point_of_pc ERTLptr_semantics (pc … st1))) 595 [ cases daemon (*CSC: Genuine proof obligation! *) 596 | #Hext ] 597 | cut 598 (before lfalse = 599 before (point_of_pc ERTLptr_semantics (pc … st1))) 600 [ cases daemon (*CSC: Genuine proof obligation! *) 601 | #Hext ]] 602 >(to_be_cleared_sb_respects_equal_valuations … 603 (colour … fn …) … Hext) <EQst1st2 604 >(to_be_cleared_fb_respects_equal_valuations … Hext) % 605 ] 606 |*: % 607 ] 608 |*: % 609 ] 803 letin before ≝ (livebefore … fn after) 804 [2: change with lfalse in match (point_of_succ ???); ] 805 lapply (included_livebefore_livebeafter_stmt_labels 806 fix_comp … EQstmt) 807 normalize in match (stmt_labels ???); 808 change with after in match after; 809 #H [ lapply (H lfalse ?) [ >memb_hd % ] 810 | lapply (H ltrue ?) [ >memb_cons try % >memb_hd %]] 811 #K change with (bool_to_Prop (rl_included ??)) in K; 812 @(rl_included_transitive … K) 813 whd in match (livebefore ????); 814 whd in EQstmt; whd in EQstmt:(??%?); 815 >EQstmt normalize nodelta 816 @rl_included_rl_join_left 817 normalize in match (defined ??); 818 @rl_included_rl_diff_rl_empty ] 819 |*: % ] 820 |*: % ] 610 821 |*: change with (hw_reg_retrieve ??) in match (acca_retrieve ?????); 611 822 >hw_reg_retrieve_write_decision_hit >m_return_bind … … 652 863 whd in match succ_pc; normalize nodelta >point_of_pc_of_point 653 864 whd in match (point_of_succ ???); 865 lapply(eq_sigma_state_monotonicity … nxt … EQst1st2) 866 [2: #X >X 867 868 654 869 cut (before nxt = before (point_of_pc ERTLptr_semantics (pc … st1))) 655 870 [ YYY whd in ⊢ (??%%); whd in EQstmt; whd in EQstmt:(??%?); >EQstmt -
src/ERTLptr/liveness.ma
r2942 r2949 3 3 include "utilities/adt/set_adt.ma". 4 4 include "utilities/fixpoints.ma". 5 6 definition rl_included ≝ 7 λleft,right. 8 set_subset … (eq_identifier RegisterTag) (\fst left) (\fst right) ∧ 9 set_subset … eq_Register (\snd left) (\snd right). 5 10 6 11 definition register_lattice : property_lattice ≝ … … 12 17 set_equal … (eq_identifier ?) (\fst left) (\fst right) ∧ 13 18 set_equal … eq_Register (\snd left) (\snd right)) 14 (λleft. 15 λright. 16 set_subset … (eq_identifier ?) (\fst left) (\fst right) ∧ 17 set_subset … eq_Register (\snd left) (\snd right)) 19 rl_included 18 20 (λ_.false). 19 21 -
src/utilities/fixpoints.ma
r2700 r2949 13 13 definition equations ≝ λlatt : property_lattice.label → rhs latt. 14 14 15 record fixpoint (latt : property_lattice) : Type[0] ≝16 { fix_lfp : 1> equations latt →valuation latt15 record fixpoint (latt : property_lattice) (eqs: equations latt) : Type[0] ≝ 16 { fix_lfp :> valuation latt 17 17 ; fix_correct : 18 ∀eqs : equations latt.19 let sol ≝ fix_lfp eqs in20 18 ∀l : label. 21 l_included latt (eqs l sol) (sol l) (* inclusion suffices for correctness *) 19 (* inclusion suffices for correctness *) 20 l_included latt (eqs l fix_lfp) (fix_lfp l) 22 21 }. 23 22 24 definition fixpoint_computer : Type[1] ≝ ∀latt.fixpoint latt. 23 definition fixpoint_computer : Type[1] ≝ ∀latt,eqs.fixpoint latt eqs. 24 25 coercion apply_fixpoint: 26 ∀latt,eqs.∀f:fixpoint latt eqs. label → latt ≝ 27 λlatt,eqs,f,l. fix_lfp … f l 28 on _f: fixpoint ? ? to label → ?.
Note: See TracChangeset
for help on using the changeset viewer.