Changeset 2949 for src

Timestamp:

Mar 25, 2013, 9:48:01 PM (7 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:

• ERTLptr/ERTLptrToLTLProof.ma (modified) (5 diffs)
• ERTLptr/liveness.ma (modified) (2 diffs)
• utilities/fixpoints.ma (modified) (1 diff)

src/ERTLptr/ERTLptrToLTLProof.ma

@@ -266 +266 @@
 ¬set_member A DEC a y → 
 set_member A DEC a (set_diff … x y).
+axiom set_member_subset_if:
+ ∀A,DEC,S1,S2.
+  set_subset A DEC S1 S2 →
+   ∀x. set_member A DEC x S1 → set_member A DEC x S2.
+axiom set_member_subset_onlyif:
+ ∀A,DEC,S1,S2.
+  (∀x. set_member A DEC x S1 → set_member A DEC x S2) →
+   set_subset A DEC S1 S2.
+
 
 lemma all_used_are_live_before :
@@ -402 +411 @@
  whd in match eliminable; normalize nodelta >Helim %
 qed.
+
+lemma set_subset_to_set_subst_set_union_left:
+ ∀T,eqT,A,B,C. set_subset T eqT A B → set_subset … eqT A (set_union … B C).
+ #T #eqT #A #B #C #H @set_member_subset_onlyif #x #K
+ lapply (set_member_subset_if … H) #H2 /3 by set_member_union1/
+qed.
+
+lemma set_subset_to_set_subst_set_union_right:
+ ∀T,eqT,A,B,C. set_subset T eqT A C → set_subset … eqT A (set_union … B C).
+ #T #eqT #A #B #C #H @set_member_subset_onlyif #x #K
+ lapply (set_member_subset_if … H) #H2 /3 by set_member_union2/
+qed.
+
+lemma rl_included_rl_join_left:
+ ∀A,B,C. rl_included A B → rl_included A (rl_join B C).
+ #A #B #C whd in match rl_included; normalize nodelta #H
+ cases (andb_Prop_true … H) -H #H1 #H2 @andb_Prop
+ /2 by set_subset_to_set_subst_set_union_left/
+qed.
+
+lemma rl_included_rl_join_right:
+ ∀A,B,C. rl_included A C → rl_included A (rl_join B C).
+ #A #B #C whd in match rl_included; normalize nodelta #H
+ cases (andb_Prop_true … H) -H #H1 #H2 @andb_Prop
+ /2 by set_subset_to_set_subst_set_union_right/
+qed.
+
+lemma set_subset_reflexive: ∀A,DEC,x. set_subset A DEC x x.
+ /2/
+qed.
+
+lemma rl_included_reflexive: ∀x. rl_included x x.
+ /2/
+qed.
+
+lemma mem_of_fold_join:
+ ∀F,dom.
+  ∀x. x ∈ dom →
+   rl_included (F x)
+    (fold label (l_property register_lattice) rl_join rl_bottom (λl:label.true)
+      F dom).
+ #F #dom elim dom [ #x * ] #hd #tl #IH #x whd in match (? ∈ ?); @eqb_elim
+ normalize nodelta #Hx #H change with (rl_join ??) in ⊢ (?(??%));
+ destruct /3 by rl_included_rl_join_left,rl_included_rl_join_right/
+qed.
+
+lemma set_subset_transitive:
+ ∀A,DEC,S1,S2,S3.
+  set_subset A DEC S1 S2 → set_subset … DEC S2 S3 → set_subset … DEC S1 S3.
+ #A #DEC #S1 #S2 #S3
+ #H1 lapply (set_member_subset_if … H1) -H1 #H1
+ #H2 lapply (set_member_subset_if … H2) -H2 #H2
+ @set_member_subset_onlyif /3 by/
+qed.
+
+lemma rl_included_transitive:
+ ∀S1,S2,S3. rl_included S1 S2 → rl_included S2 S3 → rl_included S1 S3.
+ #S1 #S2 #S3 whd in match rl_included; normalize nodelta
+ #H cases (andb_Prop_true … H) -H #H1 #H2
+ #H cases (andb_Prop_true … H) -H #H3 #H4
+ /3 by andb_Prop,set_subset_transitive/
+qed.
+
+lemma rl_included_rl_diff_rl_empty:
+ ∀S1. rl_included S1 (rl_diff S1 rl_bottom).
+ #S1 whd in match (rl_included ??);
+ lapply (set_member_subset_onlyif … (eq_identifier …) (\fst S1) (\fst (rl_diff S1 rl_bottom)))
+ cases (set_subset ????)
+ /3 by set_member_diff,set_member_subset_onlyif/
+qed.
+
+lemma included_livebefore_livebeafter_stmt_labels:
+ ∀fix_comp,globals,fn,l,stmt.
+  let after ≝ analyse_liveness fix_comp globals fn in
+   stmt_at … (joint_if_code ERTLptr … fn) l = Some … stmt →
+  ∀nxt.
+   nxt ∈
+    stmt_labels (mk_stmt_params (g_u_pars ERTLptr) label (Some label) false)
+     globals stmt →
+  l_included register_lattice (livebefore … fn after nxt) (after l).
+#fix_comp #globals #fn #l #stmt letin after ≝ (analyse_liveness ???) #EQlookup #nxt
+#Hnxt lapply (fix_correct … after l) #spec @(rl_included_transitive … spec) -spec
+whd in match (liveafter ????); whd in EQlookup:(??%?); >EQlookup -EQlookup normalize nodelta
+/2 by mem_of_fold_join/
+qed.
+
+axiom eq_sigma_state_monotonicity:
+ ∀prog,live,graph,st1,st2,l1,l2.
+  rl_included (live l2) (live l1) →
+  sigma_fb_state prog (to_be_cleared_fb live l1) st1 =
+   sigma_sb_state prog (to_be_cleared_sb live graph l1) st2 →
+  sigma_fb_state prog (to_be_cleared_fb live l2) st1 =
+   sigma_sb_state prog (to_be_cleared_sb live graph l2) st2.
+
+(* True and useless
+axiom to_be_cleared_sb_respects_equal_valuations:
+ ∀live,coloured,l1,l2.
+  live l1 = live l2 →
+   to_be_cleared_sb live coloured l1 = to_be_cleared_sb live coloured l2.
+
+axiom to_be_cleared_fb_respects_equal_valuations:
+ ∀live,l1,l2.
+  live l1 = live l2 →
+   to_be_cleared_fb live l1 = to_be_cleared_fb live l2.
+*)
+
+(*
+lemma sigma_fb_state_insensitive_to_eliminable:
+ ∀fix_comp: fixpoint_computer.
+ ∀prog: ertlptr_program.
+ ∀stackcost.
+ let p_in ≝ mk_prog_params ERTLptr_semantics prog stackcost in
+ ∀f,fn.
+ let after ≝ analyse_liveness fix_comp (prog_var_names … prog) fn in
+ let before ≝ livebefore … fn after in
+ ∀st1 : joint_abstract_status p_in.
+ let pt ≝ point_of_pc ERTLptr_semantics (pc ? st1) in
+ ∀st1_no_pc. ∀stms: joint_seq ERTLptr_semantics (prog_var_names … prog). ∀next.
+ stmt_at p_in … (joint_if_code p_in … fn) pt = return (sequential … stms next) →
+ ∀Heval_seq_no_pc:
+   eval_seq_no_pc ERTLptr_semantics
+   (prog_var_names (joint_function ERTLptr_semantics) ℕ prog)
+   (ev_genv
+    (mk_prog_params ERTLptr_semantics prog stackcost))
+   f stms (st_no_pc … st1)
+   =return st1_no_pc.
+ ∀Heliminable:
+   eliminable_step (globals p_in)
+    (after (point_of_pc ERTLptr_semantics (pc p_in st1))) stms =true.
+ sigma_fb_state prog (to_be_cleared_fb before next) st1_no_pc =
+  sigma_fb_state prog (to_be_cleared_fb before pt) (st_no_pc … st1).
+#fix_comp #prog #stackcost letin p_in ≝ (mk_prog_params ???) #f #fn
+letin after ≝ (analyse_liveness ???)
+#st1 #st1' #stms #next #stmt_at #Heval #Helim
+lapply (eliminable_step_to_eq_livebefore_liveafter … stmt_at … Helim)
+#EQ_livebefore_after
+cases stms in Heval Helim;
+try (#arg1 #arg2 #arg3 #arg4 #arg5 #Heval #Helim)
+try (#arg1 #arg2 #arg3 #arg4 #Heval #Helim)
+try (#arg1 #arg2 #arg3 #Heval #Helim) try (#arg1 #arg2 #Heval #Helim)
+try (#arg1 #Heval #Helim) try (#Heval #Helim)
+whd in Heval:(??%?);
+whd in Helim:(??%?); try (change with (false=true) in Helim; destruct (Helim))
+[7: inversion arg1 in Heval Helim; [ * [3: #arg2 ] |*: #arg2 #arg3 ] #Harg1
+    normalize nodelta ] try #Heval try #Helim whd in Heval:(??%?);
+    try (change with (false=true) in Helim; destruct (Helim))
+    [4,8: cases arg1 in Heval Helim; normalize nodelta
+      [ * normalize nodelta #arg10 #arg11] #Heval #Helim]
+lapply (eq_notb_true_to_eq_false ? Helim) -Helim #Helim
+[1,2: cases arg11 in Heval; [1,3: *] #arg12 whd in ⊢ (??%? → ?);
+  [1,3: whd in match (pair_reg_move_ ?????); normalize nodelta
+        inversion ps_reg_retrieve normalize nodelta
+        [2,4: #error #_ #abs whd in abs:(???%); destruct (abs) ]
+        #bv #EQbv ]
+|3,4,5,6,7,8,13: inversion (acca_arg_retrieve ERTLptr_semantics) in Heval;
+    [2,4,6,8,10,12,14: #error #_ #abs whd in abs:(??%%); destruct (abs) ]
+    #bv normalize nodelta #EQbv #X cases (bind_inversion ????? X) -X
+    #v1 * #Hv1 #X cases (bind_inversion ????? X) -X
+    #vres * #Hvres #X cases (bind_inversion ????? X) -X
+    #st1'' * #Hst1''
+|9: inversion (opt_to_res ???) in Heval;
+    [2: #error #_ #abs whd in abs:(??%%); destruct (abs) ]
+    #bv normalize nodelta #EQbv
+|10,11: inversion (get_pc_from_label ?????) in Heval;
+     [2,4: #error #_ #abs whd in abs:(??%%); destruct (abs) ]
+     #bv normalize nodelta #EQbv
+|12: lapply Heval -Heval
+|14: inversion (acca_retrieve ???) in Heval;
+    [2: #error #_ #abs whd in abs:(??%%); destruct (abs) ]
+    #bv normalize nodelta #EQbv #X cases (bind_inversion ????? X) -X
+    #v1 * #Hv1
+|15: inversion (dph_arg_retrieve ???) in Heval;
+    [2: #error #_ #abs whd in abs:(??%%); destruct (abs) ]
+    #bv normalize nodelta #EQbv #X cases (bind_inversion ????? X) -X
+    #v1 * #Hv1 #X cases (bind_inversion ????? X) -X
+    #vres * #Hvres #X cases (bind_inversion ????? X) -X
+    #v1 * #Hv2 ]
+whd in ⊢ (??%% → ?); #X <(injective_OK ??? X) -X
+try (cases (split_orb_false … Helim) -Helim #Helim1 #Helim2)
+
+XXX
+
+try (@sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption)
+try (@sigma_fb_state_insensitive_to_dead_Reg >EQ_livebefore_after assumption)
+try (@sigma_fb_state_insensitive_to_dead_carry >EQ_livebefore_after assumption)
+[1,2,3,4,5,6,7: <(injective_OK ??? Hst1'') ]
+[1,2,3: 
+  >sigma_fb_state_insensitive_to_dead_carry try (>EQ_livebefore_after assumption)
+  @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption
+|4: whd in Hvres:(??%%); cases Byte_of_val in Hvres; normalize nodelta 
+    [2: #error #abs destruct (abs) ]
+    #by #Hvres; cases (bind_inversion ????? Hvres) #by' * #_ #EQ
+    whd in EQ:(??%%); destruct (EQ) >set_carry_set_regs_commute >eta_set_carry
+    @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption
+|5,6: whd in Hvres:(??%%); cases bv in Hvres; normalize nodelta
+      try (#x1 #x2 #x3 #Hvres) try (#x1 #x2 #Hvres) try (#x1 #Hvres) try #Hvres
+      try (destruct (Hvres) @I) cases v1 in Hvres; normalize nodelta
+      try (#x1' #x2' #x3' #Hvres) try (#x1' #x2' #Hvres) try (#x1' #Hvres) try #Hvres
+      try (destruct (Hvres) @I)
+      [5: cases orb in Hvres; normalize nodelta try (#Hvres destruct(Hvres) @I)
+          cases andb normalize nodelta #Hvres
+      |9,10,11,12: cases cic:/matita/arithmetics/nat/eqb.fix(0,0,1) in Hvres;
+          normalize nodelta try (#abs destruct(abs) @I) #Hvres ]
+      whd in Hvres:(??%%); destruct (Hvres) >set_carry_set_regs_commute >eta_set_carry
+      @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption
+|7: cases (split_orb_false … Helim1) -Helim1 #Helim1 #Helim3
+   >sigma_fb_state_insensitive_to_dead_reg try (>EQ_livebefore_after assumption)
+   @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption
+|8: >sigma_fb_state_insensitive_to_dead_reg try (>EQ_livebefore_after assumption)
+    @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption ]
+qed.
+
 
 lemma sigma_fb_state_insensitive_to_eliminable:
@@ -502 +723 @@
 |8: >sigma_fb_state_insensitive_to_dead_reg try (>EQ_livebefore_after assumption)
     @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption ]
-qed.
-
-axiom to_be_cleared_sb_respects_equal_valuations:
- ∀live,coloured,l1,l2.
-  live l1 = live l2 →
-   to_be_cleared_sb live coloured l1 = to_be_cleared_sb live coloured l2.
-
-axiom to_be_cleared_fb_respects_equal_valuations:
- ∀live,l1,l2.
-  live l1 = live l2 →
-   to_be_cleared_fb live l1 = to_be_cleared_fb live l2.
+qed. *)
 
 lemma make_ERTLptr_To_LTL_good_state_relation :
@@ -588 +799 @@
                      [2,4: @dead_registers_in_dead @acc_is_dead ]
                      whd >point_of_pc_of_point
+                     @(eq_sigma_state_monotonicity … EQst1st2)
                      letin after ≝ (analyse_liveness fix_comp … fn)
-                     letin before ≝ (livebefore … fn after) 
-                     [ cut
-                        (before ltrue =
-                          before (point_of_pc ERTLptr_semantics (pc … st1)))
-                       [ cases daemon (*CSC: Genuine proof obligation! *)
-                       | #Hext ]
-                     |  cut
-                        (before lfalse =
-                          before (point_of_pc ERTLptr_semantics (pc … st1)))
-                       [ cases daemon (*CSC: Genuine proof obligation! *)
-                       | #Hext ]]
-                     >(to_be_cleared_sb_respects_equal_valuations …
-                        (colour … fn …) … Hext) <EQst1st2
-                     >(to_be_cleared_fb_respects_equal_valuations … Hext) %
-                 ]
-            |*: %
-            ]
-       |*: %
-       ]
+                     letin before ≝ (livebefore … fn after)
+                     [2: change with lfalse in match (point_of_succ ???); ]
+                     lapply (included_livebefore_livebeafter_stmt_labels 
+                      fix_comp … EQstmt)
+                     normalize in match (stmt_labels ???);
+                     change with after in match after;
+                     #H [ lapply (H lfalse ?) [ >memb_hd % ]
+                        | lapply (H ltrue ?) [ >memb_cons try % >memb_hd %]]
+                     #K change with (bool_to_Prop (rl_included ??)) in K;
+                     @(rl_included_transitive … K)
+                     whd in match (livebefore ????);
+                     whd in EQstmt; whd in EQstmt:(??%?);
+                     >EQstmt normalize nodelta
+                     @rl_included_rl_join_left
+                     normalize in match (defined ??);
+                     @rl_included_rl_diff_rl_empty ]
+            |*: % ]
+       |*: % ]
   |*: change with (hw_reg_retrieve ??) in match (acca_retrieve ?????);
       >hw_reg_retrieve_write_decision_hit >m_return_bind
@@ -652 +863 @@
     whd in match succ_pc; normalize nodelta >point_of_pc_of_point
     whd in match (point_of_succ ???);
+    lapply(eq_sigma_state_monotonicity … nxt … EQst1st2)
+    [2: #X >X
+
+    
     cut (before nxt = before (point_of_pc ERTLptr_semantics (pc … st1)))
     [ YYY whd in ⊢ (??%%); whd in EQstmt; whd in EQstmt:(??%?); >EQstmt

src/ERTLptr/liveness.ma

@@ -3 +3 @@
 include "utilities/adt/set_adt.ma".
 include "utilities/fixpoints.ma".
+
+definition rl_included ≝
+ λleft,right.
+  set_subset … (eq_identifier RegisterTag) (\fst left) (\fst right) ∧
+  set_subset … eq_Register (\snd left) (\snd right).
 
 definition register_lattice : property_lattice ≝
@@ -12 +17 @@
   set_equal … (eq_identifier ?) (\fst left) (\fst right) ∧
   set_equal … eq_Register (\snd left) (\snd right))
- (λleft.
-  λright.
-  set_subset … (eq_identifier ?) (\fst left) (\fst right) ∧
-  set_subset … eq_Register (\snd left) (\snd right))
+ rl_included
  (λ_.false).
 

src/utilities/fixpoints.ma

@@ -13 +13 @@
 definition equations ≝ λlatt : property_lattice.label → rhs latt.
 
-record fixpoint (latt : property_lattice) : Type[0] ≝
-{ fix_lfp :1> equations latt → valuation latt
+record fixpoint (latt : property_lattice) (eqs: equations latt) : Type[0] ≝
+{ fix_lfp :> valuation latt
 ; fix_correct :
-  ∀eqs : equations latt.
-  let sol ≝ fix_lfp eqs in
   ∀l : label.
-  l_included latt (eqs l sol) (sol l) (* inclusion suffices for correctness *)
+   (* inclusion suffices for correctness *)
+   l_included latt (eqs l fix_lfp) (fix_lfp l)
 }.
 
-definition fixpoint_computer : Type[1] ≝ ∀latt.fixpoint latt.
+definition fixpoint_computer : Type[1] ≝ ∀latt,eqs.fixpoint latt eqs.
+
+coercion apply_fixpoint:
+ ∀latt,eqs.∀f:fixpoint latt eqs. label → latt ≝
+ λlatt,eqs,f,l. fix_lfp … f l
+ on _f: fixpoint ? ? to label → ?.