Changeset 2949


Ignore:
Timestamp:
Mar 25, 2013, 9:48:01 PM (4 years ago)
Author:
sacerdot
Message:

Some advance/repairing in ERTLptrToLTLProof. In particular, we know take in
account that the fixpoint computation only returns a pre-fixpoint.

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptrToLTLProof.ma

    r2944 r2949  
    266266¬set_member A DEC a y →
    267267set_member A DEC a (set_diff … x y).
     268axiom 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.
     272axiom 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
    268277
    269278lemma all_used_are_live_before :
     
    402411 whd in match eliminable; normalize nodelta >Helim %
    403412qed.
     413
     414lemma 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/
     418qed.
     419
     420lemma 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/
     424qed.
     425
     426lemma 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/
     431qed.
     432
     433lemma 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/
     438qed.
     439
     440lemma set_subset_reflexive: ∀A,DEC,x. set_subset A DEC x x.
     441 /2/
     442qed.
     443
     444lemma rl_included_reflexive: ∀x. rl_included x x.
     445 /2/
     446qed.
     447
     448lemma 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/
     457qed.
     458
     459lemma 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/
     466qed.
     467
     468lemma 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/
     474qed.
     475
     476lemma 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/
     482qed.
     483
     484lemma 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
     495whd in match (liveafter ????); whd in EQlookup:(??%?); >EQlookup -EQlookup normalize nodelta
     496/2 by mem_of_fold_join/
     497qed.
     498
     499axiom 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
     508axiom 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
     513axiom 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(*
     520lemma 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
     545letin after ≝ (analyse_liveness ???)
     546#st1 #st1' #stms #next #stmt_at #Heval #Helim
     547lapply (eliminable_step_to_eq_livebefore_liveafter … stmt_at … Helim)
     548#EQ_livebefore_after
     549cases stms in Heval Helim;
     550try (#arg1 #arg2 #arg3 #arg4 #arg5 #Heval #Helim)
     551try (#arg1 #arg2 #arg3 #arg4 #Heval #Helim)
     552try (#arg1 #arg2 #arg3 #Heval #Helim) try (#arg1 #arg2 #Heval #Helim)
     553try (#arg1 #Heval #Helim) try (#Heval #Helim)
     554whd in Heval:(??%?);
     555whd 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]
     561lapply (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 ]
     590whd in ⊢ (??%% → ?); #X <(injective_OK ??? X) -X
     591try (cases (split_orb_false … Helim) -Helim #Helim1 #Helim2)
     592
     593XXX
     594
     595try (@sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption)
     596try (@sigma_fb_state_insensitive_to_dead_Reg >EQ_livebefore_after assumption)
     597try (@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 ]
     623qed.
     624
    404625
    405626lemma sigma_fb_state_insensitive_to_eliminable:
     
    502723|8: >sigma_fb_state_insensitive_to_dead_reg try (>EQ_livebefore_after assumption)
    503724    @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.
     725qed. *)
    515726
    516727lemma make_ERTLptr_To_LTL_good_state_relation :
     
    588799                     [2,4: @dead_registers_in_dead @acc_is_dead ]
    589800                     whd >point_of_pc_of_point
     801                     @(eq_sigma_state_monotonicity … EQst1st2)
    590802                     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       |*: % ]
    610821  |*: change with (hw_reg_retrieve ??) in match (acca_retrieve ?????);
    611822      >hw_reg_retrieve_write_decision_hit >m_return_bind
     
    652863    whd in match succ_pc; normalize nodelta >point_of_pc_of_point
    653864    whd in match (point_of_succ ???);
     865    lapply(eq_sigma_state_monotonicity … nxt … EQst1st2)
     866    [2: #X >X
     867
     868   
    654869    cut (before nxt = before (point_of_pc ERTLptr_semantics (pc … st1)))
    655870    [ YYY whd in ⊢ (??%%); whd in EQstmt; whd in EQstmt:(??%?); >EQstmt
  • src/ERTLptr/liveness.ma

    r2942 r2949  
    33include "utilities/adt/set_adt.ma".
    44include "utilities/fixpoints.ma".
     5
     6definition rl_included ≝
     7 λleft,right.
     8  set_subset … (eq_identifier RegisterTag) (\fst left) (\fst right) ∧
     9  set_subset … eq_Register (\snd left) (\snd right).
    510
    611definition register_lattice : property_lattice ≝
     
    1217  set_equal … (eq_identifier ?) (\fst left) (\fst right) ∧
    1318  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
    1820 (λ_.false).
    1921
  • src/utilities/fixpoints.ma

    r2700 r2949  
    1313definition equations ≝ λlatt : property_lattice.label → rhs latt.
    1414
    15 record fixpoint (latt : property_lattice) : Type[0] ≝
    16 { fix_lfp :1> equations latt → valuation latt
     15record fixpoint (latt : property_lattice) (eqs: equations latt) : Type[0] ≝
     16{ fix_lfp :> valuation latt
    1717; fix_correct :
    18   ∀eqs : equations latt.
    19   let sol ≝ fix_lfp eqs in
    2018  ∀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)
    2221}.
    2322
    24 definition fixpoint_computer : Type[1] ≝ ∀latt.fixpoint latt.
     23definition fixpoint_computer : Type[1] ≝ ∀latt,eqs.fixpoint latt eqs.
     24
     25coercion 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.