Changeset 2938

Timestamp:

Mar 22, 2013, 2:11:59 AM (6 years ago)

Author:

sacerdot

Message:

1. proof of "all eliminable are eliminable" completed
2. the notion of state_rel in the helpers file needs to be generalized to accomodate the dependency on the program counter

File:

• src/ERTLptr/ERTLptrToLTLProof.ma (modified) (9 diffs)

src/ERTLptr/ERTLptrToLTLProof.ma

@@ -102 +102 @@
 
 definition state_rel : fixpoint_computer → coloured_graph_computer → 
-ertlptr_program → (Σb:block.block_region b = Code) → label →
- state ERTL_state → state LTL_LIN_state → Prop ≝ 
+ertlptr_program →
+ (Σb:block.block_region b = Code) → label → state ERTL_state → state LTL_LIN_state → Prop ≝ 
 λfix_comp,build,prog,bl,pc,st1,st2.
 ∃f,fn.fetch_internal_function ? (globalenv_noinit … prog) bl = return 〈f,fn〉 ∧
@@ -349 +349 @@
  ∀fix_comp,prog,fn,bv. ∀st: state ERTLptr_semantics. ∀l:label.
  ∀r: register.
- let live ≝
-  analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) fn in
+ let live ≝ 
+  analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) fn
+ in
   set_member (identifier RegisterTag) (eq_identifier RegisterTag) r
-   (\fst  (live l)) = false →
+   (\fst  (livebefore … fn l live)) = false →
   sigma_fb_state prog
    (to_be_cleared_fb live l)
@@ -363 +364 @@
  ∀fix_comp,prog,fn,bv. ∀st: state ERTLptr_semantics. ∀l:label.
  ∀r: Register.
- let live ≝
+ let live ≝ 
   analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) fn
  in
-  set_member Register eq_Register r (\snd  (live l)) = false →
+  set_member Register eq_Register r (\snd  (livebefore … fn l live)) = false →
   sigma_fb_state prog
    (to_be_cleared_fb live l)
@@ -377 +378 @@
 axiom sigma_fb_state_insensitive_to_dead_carry:
  ∀fix_comp,prog,fn,bv. ∀st: state ERTLptr_semantics. ∀l:label.
- let live ≝
+ let live ≝ 
   analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) fn
  in
-  set_member Register eq_Register RegisterCarry (\snd (live l)) = false →
+  set_member Register eq_Register RegisterCarry (\snd (livebefore … fn l live)) = false →
    sigma_fb_state prog (to_be_cleared_fb live l) (set_carry ERTLptr_semantics bv st) =
    sigma_fb_state prog (to_be_cleared_fb live l) st.
@@ -386 +387 @@
 lemma split_orb_false: ∀a,b:bool. orb a b = false → a = false ∧ b = false.
  ** normalize #abs destruct /2/
+qed.
+
+lemma eta_set_carry:
+ ∀P,st. set_carry P (carry P st) st = st.
+#P * //
+qed.
+
+lemma set_carry_set_regs_commute:
+ ∀P,st,c,v. set_carry P c (set_regs P v st) = set_regs P v (set_carry P c st).
+ #P * //
+qed.
+
+lemma eliminable_step_to_eq_livebefore_liveafter:
+ ∀fix_comp,colour,prog,fn.
+ let p_in ≝
+   mk_prog_params ERTLptr_semantics prog
+   (lookup_stack_cost (\snd  (\fst  (ertlptr_to_ltl fix_comp colour prog)))) in
+ ∀st1: joint_abstract_status p_in.
+ ∀stms: joint_seq ERTLptr_semantics (prog_var_names … prog). ∀next.
+ let pt ≝ point_of_pc ERTLptr_semantics (pc ? st1) in
+ stmt_at p_in ? (joint_if_code p_in … fn) pt = return (sequential … stms next) →
+ let liveafter ≝ analyse_liveness fix_comp (globals p_in) fn in 
+ eliminable_step (globals p_in) (liveafter (point_of_pc ERTLptr_semantics (pc … st1))) stms = true →
+  livebefore … fn pt liveafter = liveafter pt.
+ #fix_comp #colour #prog #fn #st1 #stms #next #stmt_at #Helim
+ whd in ⊢ (??%?); whd in stmt_at:(??%?); cases (lookup ????) in stmt_at;
+ normalize nodelta try (#abs whd in abs:(??%%); destruct (abs) @I)
+ #stms' #EQ whd in EQ:(??%%); destruct (EQ) whd in ⊢ (??%?);
+ whd in match eliminable; normalize nodelta >Helim %
 qed.
 
@@ -398 +428 @@
  ∀st1 : joint_abstract_status p_in.
  let pt ≝ point_of_pc ERTLptr_semantics (pc ? st1) in
- ∀st1_no_pc,stms.
+ ∀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
@@ -423 +454 @@
    (st_no_pc … st1)).
 #fix_comp #colour #prog letin p_in ≝ (mk_prog_params ???) #f #fn
-#st1 #st1' *
+#st1 #st1' #stms #next #stmt_at #Heval #Helim
+lapply (eliminable_step_to_eq_livebefore_liveafter … stmt_at Helim)
+#EQ_livebefore_after -next
+cases stms in Heval Helim;
 try (#arg1 #arg2 #arg3 #arg4 #arg5 #Heval #Helim)
 try (#arg1 #arg2 #arg3 #arg4 #Heval #Helim)
@@ -466 +500 @@
 whd in ⊢ (??%% → ?); #X <(injective_OK ??? X) -X
 try (cases (split_orb_false … Helim) -Helim #Helim1 #Helim2)
-try (@sigma_fb_state_insensitive_to_dead_reg assumption)
-try (@sigma_fb_state_insensitive_to_dead_Reg assumption)
-try (@sigma_fb_state_insensitive_to_dead_carry assumption)
+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 assumption
-  @sigma_fb_state_insensitive_to_dead_reg assumption
-|4,5,6: (* BUG! *)
-|7: >sigma_fb_state_insensitive_to_dead_reg try assumption
+  >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 make_ERTLptr_To_LTL_good_state_relation :
@@ -490 +544 @@
 good_state_relation ERTLptr_semantics LTL_semantics prog stacksizes
  (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)»)
- init_regs f_lbls f_regs good (state_rel fix_comp colour prog f_lbls f_regs)
+ init_regs f_lbls f_regs good (state_rel fix_comp colour prog)
  (sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good)).
 #fix_comp #colour #prog