Changeset 3254
 Timestamp:
 May 8, 2013, 3:58:29 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTLptr/ERTLptrToLTLProof.ma
r2949 r3254 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 277 268 278 269 lemma all_used_are_live_before : … … 411 402 whd in match eliminable; normalize nodelta >Helim % 412 403 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 #K417 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 #K423 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 #H429 cases (andb_Prop_true … H) H #H1 #H2 @andb_Prop430 /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 #H436 cases (andb_Prop_true … H) H #H1 #H2 @andb_Prop437 /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_elim455 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 #S3463 #H1 lapply (set_member_subset_if … H1) H1 #H1464 #H2 lapply (set_member_subset_if … H2) H2 #H2465 @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 nodelta471 #H cases (andb_Prop_true … H) H #H1 #H2472 #H cases (andb_Prop_true … H) H #H3 #H4473 /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 in487 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 #nxt494 #Hnxt lapply (fix_correct … after l) #spec @(rl_included_transitive … spec) spec495 whd in match (liveafter ????); whd in EQlookup:(??%?); >EQlookup EQlookup normalize nodelta496 /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 useless508 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 in525 ∀f,fn.526 let after ≝ analyse_liveness fix_comp (prog_var_names … prog) fn in527 let before ≝ livebefore … fn after in528 ∀st1 : joint_abstract_status p_in.529 let pt ≝ point_of_pc ERTLptr_semantics (pc ? st1) in530 ∀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_semantics534 (prog_var_names (joint_function ERTLptr_semantics) ℕ prog)535 (ev_genv536 (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 #fn545 letin after ≝ (analyse_liveness ???)546 #st1 #st1' #stms #next #stmt_at #Heval #Helim547 lapply (eliminable_step_to_eq_livebefore_liveafter … stmt_at … Helim)548 #EQ_livebefore_after549 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 ] #Harg1557 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 nodelta560 [ * normalize nodelta #arg10 #arg11] #Heval #Helim]561 lapply (eq_notb_true_to_eq_false ? Helim) Helim #Helim562 [1,2: cases arg11 in Heval; [1,3: *] #arg12 whd in ⊢ (??%? → ?);563 [1,3: whd in match (pair_reg_move_ ?????); normalize nodelta564 inversion ps_reg_retrieve normalize nodelta565 [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) X570 #v1 * #Hv1 #X cases (bind_inversion ????? X) X571 #vres * #Hvres #X cases (bind_inversion ????? X) X572 #st1'' * #Hst1''573 9: inversion (opt_to_res ???) in Heval;574 [2: #error #_ #abs whd in abs:(??%%); destruct (abs) ]575 #bv normalize nodelta #EQbv576 10,11: inversion (get_pc_from_label ?????) in Heval;577 [2,4: #error #_ #abs whd in abs:(??%%); destruct (abs) ]578 #bv normalize nodelta #EQbv579 12: lapply Heval Heval580 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) X583 #v1 * #Hv1584 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) X587 #v1 * #Hv1 #X cases (bind_inversion ????? X) X588 #vres * #Hvres #X cases (bind_inversion ????? X) X589 #v1 * #Hv2 ]590 whd in ⊢ (??%% → ?); #X <(injective_OK ??? X) X591 try (cases (split_orb_false … Helim) Helim #Helim1 #Helim2)592 593 XXX594 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 assumption602 4: whd in Hvres:(??%%); cases Byte_of_val in Hvres; normalize nodelta603 [2: #error #abs destruct (abs) ]604 #by #Hvres; cases (bind_inversion ????? Hvres) #by' * #_ #EQ605 whd in EQ:(??%%); destruct (EQ) >set_carry_set_regs_commute >eta_set_carry606 @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption607 5,6: whd in Hvres:(??%%); cases bv in Hvres; normalize nodelta608 try (#x1 #x2 #x3 #Hvres) try (#x1 #x2 #Hvres) try (#x1 #Hvres) try #Hvres609 try (destruct (Hvres) @I) cases v1 in Hvres; normalize nodelta610 try (#x1' #x2' #x3' #Hvres) try (#x1' #x2' #Hvres) try (#x1' #Hvres) try #Hvres611 try (destruct (Hvres) @I)612 [5: cases orb in Hvres; normalize nodelta try (#Hvres destruct(Hvres) @I)613 cases andb normalize nodelta #Hvres614 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_carry617 @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption618 7: cases (split_orb_false … Helim1) Helim1 #Helim1 #Helim3619 >sigma_fb_state_insensitive_to_dead_reg try (>EQ_livebefore_after assumption)620 @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption621 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 625 404 626 405 lemma sigma_fb_state_insensitive_to_eliminable: … … 723 502 8: >sigma_fb_state_insensitive_to_dead_reg try (>EQ_livebefore_after assumption) 724 503 @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption ] 725 qed. *) 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. 726 515 727 516 lemma make_ERTLptr_To_LTL_good_state_relation : … … 799 588 [2,4: @dead_registers_in_dead @acc_is_dead ] 800 589 whd >point_of_pc_of_point 801 @(eq_sigma_state_monotonicity … EQst1st2)802 590 letin after ≝ (analyse_liveness fix_comp … fn) 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 *: % ] 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 ] 821 610 *: change with (hw_reg_retrieve ??) in match (acca_retrieve ?????); 822 611 >hw_reg_retrieve_write_decision_hit >m_return_bind … … 863 652 whd in match succ_pc; normalize nodelta >point_of_pc_of_point 864 653 whd in match (point_of_succ ???); 865 lapply(eq_sigma_state_monotonicity … nxt … EQst1st2)866 [2: #X >X867 868 869 654 cut (before nxt = before (point_of_pc ERTLptr_semantics (pc … st1))) 870 655 [ YYY whd in ⊢ (??%%); whd in EQstmt; whd in EQstmt:(??%?); >EQstmt
Note: See TracChangeset
for help on using the changeset viewer.