Changeset 3254


Ignore:
Timestamp:
May 8, 2013, 3:58:29 PM (4 years ago)
Author:
sacerdot
Message:

Code I always forgot to commit.
To be ported to ERTLtoLTLProof.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptrToLTLProof.ma

    r2949 r3254  
    266266¬set_member A DEC a y →
    267267set_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 
    277268
    278269lemma all_used_are_live_before :
     
    411402 whd in match eliminable; normalize nodelta >Helim %
    412403qed.
    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 
    625404
    626405lemma sigma_fb_state_insensitive_to_eliminable:
     
    723502|8: >sigma_fb_state_insensitive_to_dead_reg try (>EQ_livebefore_after assumption)
    724503    @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption ]
    725 qed. *)
     504qed.
     505
     506axiom 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
     511axiom 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.
    726515
    727516lemma make_ERTLptr_To_LTL_good_state_relation :
     
    799588                     [2,4: @dead_registers_in_dead @acc_is_dead ]
    800589                     whd >point_of_pc_of_point
    801                      @(eq_sigma_state_monotonicity … EQst1st2)
    802590                     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       ]
    821610  |*: change with (hw_reg_retrieve ??) in match (acca_retrieve ?????);
    822611      >hw_reg_retrieve_write_decision_hit >m_return_bind
     
    863652    whd in match succ_pc; normalize nodelta >point_of_pc_of_point
    864653    whd in match (point_of_succ ???);
    865     lapply(eq_sigma_state_monotonicity … nxt … EQst1st2)
    866     [2: #X >X
    867 
    868    
    869654    cut (before nxt = before (point_of_pc ERTLptr_semantics (pc … st1)))
    870655    [ YYY whd in ⊢ (??%%); whd in EQstmt; whd in EQstmt:(??%?); >EQstmt
Note: See TracChangeset for help on using the changeset viewer.