[Broken version] Intermediate local commit: proof of inst_checker_eqlive OK

2 files changed, 131 insertions, 54 deletions

diff --git a/scheduling/RTLpathLivegen.v b/scheduling/RTLpathLivegen.v
index 7449dcc6..91c8e790 100644
--- a/scheduling/RTLpathLivegen.v
+++ b/scheduling/RTLpathLivegen.v
@@ -152,7 +152,7 @@ Qed.
 
 Local Hint Resolve exit_list_checker_correct: core.
 
-Definition final_inst_checker (pm: path_map) (alive: Regset.t) (i: instruction): option unit :=
+(* TODO REMOVE (REPLACED) Definition final_inst_checker (pm: path_map) (alive: Regset.t) (i: instruction): option unit :=
    match i with
    | Icall sig ros args res pc' =>
       ASSERT list_mem args alive IN
@@ -173,47 +173,7 @@ Definition final_inst_checker (pm: path_map) (alive: Regset.t) (i: instruction):
       ASSERT (reg_option_mem optarg) alive IN
       Some tt
    | _ => None
-   end.
-
-Lemma final_inst_checker_wellformed (c:code) pc (pm: path_map) (alive: Regset.t) (i: instruction):
-  final_inst_checker pm alive i = Some tt ->
-  c!pc = Some i -> wellformed_path c pm 0 pc.
-Proof.
-  intros CHECK PC. eapply wf_last_node; eauto.
-  clear c pc PC. intros pc PC.
-  destruct i; simpl in * |- *; intuition (subst; eauto);
-  try (generalize CHECK; clear CHECK; try (inversion_SOME path); repeat inversion_ASSERT; try_simplify_someHyps).
-Qed.
-
-Definition inst_checker (pm: path_map) (alive: Regset.t) (i: instruction): option unit :=
-   match iinst_checker pm alive i with
-   | Some res =>
-      exit_checker pm (fst res) (snd res) tt
-   | _ => 
-      final_inst_checker pm alive i
-   end.
-
-Lemma inst_checker_wellformed (c:code) pc (pm: path_map) (alive: Regset.t) (i: instruction):
-  inst_checker pm alive i = Some tt ->
-  c!pc = Some i -> wellformed_path c pm 0 pc.
-Proof.
-  unfold inst_checker.
-  destruct (iinst_checker pm alive i) as [[alive0 pc0]|] eqn: CHECK1; simpl.
-  - simpl; intros CHECK2 PC. eapply wf_last_node; eauto.
-    destruct i; simpl in * |- *; intuition (subst; eauto);
-    try (generalize CHECK2 CHECK1; clear CHECK1 CHECK2; try (inversion_SOME path); repeat inversion_ASSERT; try_simplify_someHyps).
-    intros PC CHECK1 CHECK2. 
-    intros; exploit exit_checker_res; eauto.
-    intros X; inversion X. intros; subst; eauto.
-  - eapply final_inst_checker_wellformed.
-Qed.
-
-Definition path_checker (f: RTL.function) pm (pc: node) (path:path_info): option unit :=
-   SOME res <- ipath_checker (path.(psize)) f pm (path.(input_regs)) pc  IN
-   SOME i <- f.(fn_code)!(snd res) IN
-   inst_checker pm (fst res) i.
-
-(* TODO: replace the implementation of [path_checker] above by this one in order to check [path.(pre_output_regs)]
+   end.*)
 
 Definition final_inst_checker (pm: path_map) (alive por: Regset.t) (i: instruction): option unit :=
    match i with
@@ -238,6 +198,24 @@ Definition final_inst_checker (pm: path_map) (alive por: Regset.t) (i: instructi
    | _ => None
    end.
 
+Lemma final_inst_checker_wellformed (c:code) pc (pm: path_map) (alive por: Regset.t) (i: instruction):
+  final_inst_checker pm alive por i = Some tt ->
+  c!pc = Some i -> wellformed_path c pm 0 pc.
+Proof.
+  intros CHECK PC. eapply wf_last_node; eauto.
+  clear c pc PC. intros pc PC.
+  destruct i; simpl in * |- *; intuition (subst; eauto);
+  try (generalize CHECK; clear CHECK; try (inversion_SOME path); repeat inversion_ASSERT; try_simplify_someHyps).
+Qed.
+
+(* TODO (REPLACED) Definition inst_checker (pm: path_map) (alive: Regset.t) (i: instruction): option unit :=
+   match iinst_checker pm alive i with
+   | Some res =>
+      exit_checker pm (fst res) (snd res) tt
+   | _ => 
+      final_inst_checker pm alive i
+   end.*)
+
 Definition inst_checker (pm: path_map) (alive por: Regset.t) (i: instruction): option unit :=
    match iinst_checker pm alive i with
    | Some res =>
@@ -248,11 +226,31 @@ Definition inst_checker (pm: path_map) (alive por: Regset.t) (i: instruction): o
       final_inst_checker pm alive por i
    end.
 
+Lemma inst_checker_wellformed (c:code) pc (pm: path_map) (alive por: Regset.t) (i: instruction):
+  inst_checker pm alive por i = Some tt ->
+  c!pc = Some i -> wellformed_path c pm 0 pc.
+Proof.
+  unfold inst_checker.
+  destruct (iinst_checker pm alive i) as [[alive0 pc0]|] eqn: CHECK1; simpl.
+  - simpl; intros CHECK2 PC. eapply wf_last_node; eauto.
+    destruct i; simpl in * |- *; intuition (subst; eauto);
+    try (generalize CHECK2 CHECK1; clear CHECK1 CHECK2; try (inversion_SOME path); repeat inversion_ASSERT; try_simplify_someHyps).
+    intros PC CHECK1 CHECK2. 
+    intros; exploit exit_checker_res; eauto.
+    intros X; inversion X. intros; subst; eauto.
+  - simpl; intros CHECK2 PC. eapply final_inst_checker_wellformed; eauto.
+    generalize CHECK2. clear CHECK2. inversion_ASSERT. try_simplify_someHyps.
+Qed.
+
+(* TODO (REPLACED) Definition path_checker (f: RTL.function) pm (pc: node) (path:path_info): option unit :=
+   SOME res <- ipath_checker (path.(psize)) f pm (path.(input_regs)) pc  IN
+   SOME i <- f.(fn_code)!(snd res) IN
+   inst_checker pm (fst res) i. *)
+
 Definition path_checker (f: RTL.function) pm (pc: node) (path:path_info): option unit :=
    SOME res <- ipath_checker (path.(psize)) f pm (path.(input_regs)) pc  IN
    SOME i <- f.(fn_code)!(snd res) IN
    inst_checker pm (fst res) (path.(pre_output_regs)) i.
-*)
 
 Lemma path_checker_wellformed f pm pc path:
    path_checker f pm pc path = Some tt -> wellformed_path (f.(fn_code)) pm (path.(psize)) pc.
diff --git a/scheduling/RTLpathLivegenproof.v b/scheduling/RTLpathLivegenproof.v
index 26a1a50a..968077a9 100644
--- a/scheduling/RTLpathLivegenproof.v
+++ b/scheduling/RTLpathLivegenproof.v
@@ -501,9 +501,9 @@ Proof.
   intros H; erewrite (EQLIVE r); eauto.
 Qed.
 
-Lemma final_inst_checker_from_iinst_checker i sp rs m st pm alive:
+Lemma final_inst_checker_from_iinst_checker i sp rs m st pm alive por:
   istep ge i sp rs m = Some st -> 
-  final_inst_checker pm alive i = None.
+  final_inst_checker pm alive por i = None.
 Proof.
   destruct i; simpl; try congruence.
 Qed.
@@ -597,15 +597,16 @@ Proof.
     * intuition. eapply IHtbl; eauto.
 Qed.
 
-Lemma final_inst_checker_eqlive (f: function) sp alive pc i rs1 rs2 m stk1 stk2 t s1:
+Lemma final_inst_checker_eqlive (f: function) sp alive por pc i rs1 rs2 m stk1 stk2 t s1:
   list_forall2 eqlive_stackframes stk1 stk2 ->
   eqlive_reg (ext alive) rs1 rs2 -> 
+  eqlive_reg (ext por) rs1 rs2 -> 
   liveness_ok_function f ->
   (fn_code f) ! pc = Some i ->
   path_last_step ge pge stk1 f sp pc rs1 m t s1 ->
-  final_inst_checker (fn_path f) alive i = Some tt -> 
+  final_inst_checker (fn_path f) alive por i = Some tt -> 
   exists s2, path_last_step ge pge stk2 f sp pc rs2 m t s2 /\ eqlive_states s1 s2.
-Proof.
+Proof. Admitted. (*
   intros STACKS EQLIVE LIVENESS PC; 
   destruct 1 as [i' sp pc rs1 m st1|
                  sp pc rs1 m sig ros args res pc' fd|
@@ -661,15 +662,89 @@ Proof.
       * erewrite (EQLIVE r); eauto.
         eapply eqlive_states_return; eauto.
       * eapply eqlive_states_return; eauto.
-Qed.
-
-Lemma inst_checker_eqlive (f: function) sp alive pc i rs1 rs2 m stk1 stk2 t s1:
+     Qed.*)
+
+Lemma subset_contra: forall por alive inputs,
+  Regset.Subset por alive ->
+  Regset.subset inputs alive = false ->
+  Regset.subset inputs por = true ->
+  False.
+Proof.
+  intros por alive inputs SUB CONTRA H.
+  assert (INV: Regset.Subset inputs alive).
+  { 
+    apply Regset.subset_2 in H.
+    unfold Regset.Subset in *; intros.
+    auto. }
+  apply Regset.subset_1 in INV. congruence.
+Qed.
+
+Lemma add_subset_contra: forall r por alive inputs,
+  Regset.Subset por alive ->
+  Regset.subset inputs (Regset.add r alive) = false ->
+  Regset.subset inputs (Regset.add r por) = true ->
+  False.
+Proof.
+  intros r por alive inputs SUB CONTRA H.
+  assert (INV: Regset.Subset inputs (Regset.add r alive)).
+  { 
+    apply Regset.subset_2 in H.
+    unfold Regset.Subset in *; intros.
+    destruct (Pos.eq_dec r a); subst.
+    * apply Regset.add_1; auto.
+    * specialize H with a.
+      apply Regset.add_2. 
+      apply SUB. apply Regset.add_3 in H; auto. }
+  apply Regset.subset_1 in INV. congruence.
+Qed.
+
+Lemma exit_list_checker_subset_contra: forall por alive f l,
+  Regset.Subset por alive ->
+  exit_list_checker (fn_path f) alive l = false ->
+  exit_list_checker (fn_path f) por l = true ->
+  False.
+Proof.
+  induction l.
+  - simpl in *; intuition.
+  - simpl in *. unfold exit_checker.
+    simplify_SOME path. generalize H2, H3. 
+    repeat inversion_ASSERT.
+    + intuition.
+    + intuition.
+      exploit (subset_contra por alive (input_regs path0)); eauto;
+      intros CONTRA; inv CONTRA.
+Qed.
+
+Lemma final_inst_checker_trans: forall alive por i f,
+  Regset.subset por alive = true ->
+  final_inst_checker (fn_path f) alive por i = Some () ->
+  final_inst_checker (fn_path f) alive alive i = Some ().
+Proof.
+  intros.
+  destruct i; simpl in *; try congruence;
+  generalize H0; clear H0; unfold exit_checker;
+  repeat inversion_ASSERT; simplify_SOME path;
+  repeat inversion_ASSERT; intuition.
+  - exploit (add_subset_contra r por alive (input_regs path0)); eauto;
+    intros CONTRA; inv CONTRA.
+  - destruct b; simpl in *.
+    + exploit (add_subset_contra x por alive (input_regs path0)); eauto;
+      intros CONTRA; inv CONTRA.
+    + exploit (subset_contra por alive (input_regs path0)); eauto;
+      intros CONTRA; inv CONTRA.
+    + exploit (subset_contra por alive (input_regs path0)); eauto;
+      intros CONTRA; inv CONTRA.
+  - exploit (exit_list_checker_subset_contra por alive f l); eauto;
+    intros CONTRA; inv CONTRA.
+Qed.
+
+Lemma inst_checker_eqlive (f: function) sp alive por pc i rs1 rs2 m stk1 stk2 t s1:
   list_forall2 eqlive_stackframes stk1 stk2 ->
   eqlive_reg (ext alive) rs1 rs2 -> 
   liveness_ok_function f ->
   (fn_code f) ! pc = Some i ->
   path_last_step ge pge stk1 f sp pc rs1 m t s1 ->
-  inst_checker (fn_path f) alive i = Some tt -> 
+  inst_checker (fn_path f) alive por i = Some tt -> 
   exists s2, path_last_step ge pge stk2 f sp pc rs2 m t s2 /\ eqlive_states s1 s2.
 Proof.
   unfold inst_checker;
@@ -677,7 +752,7 @@ Proof.
   destruct (iinst_checker (fn_path f) alive i) as [res|] eqn: IICHECKER.
   + destruct 1 as [i' sp pc rs1 m st1| | | | | ];
     try_simplify_someHyps.
-    intros PC ISTEP.
+    intros IICHECKER PC ISTEP. inversion_ASSERT.
     intros.
     destruct (icontinue st1) eqn: CONT.
     - (* CONT => true *)
@@ -685,7 +760,9 @@ Proof.
       destruct 1 as (st2 & ISTEP2 & [CONT' PC2 RS MEM]).
       repeat (econstructor; simpl; eauto).
       rewrite <- MEM, <- PC2.
+      apply Regset.subset_2 in H.
       exploit exit_checker_eqlive; eauto.
+      eapply eqlive_reg_monotonic; eauto.
       intros (path & PATH & EQLIVE2).
       eapply eqlive_states_intro; eauto.
       erewrite <- iinst_checker_istep_continue; eauto.
@@ -695,7 +772,9 @@ Proof.
       repeat (econstructor; simpl; eauto).
       rewrite <- MEM, <- PC2.
       eapply eqlive_states_intro; eauto.
-  + intros; exploit final_inst_checker_eqlive; eauto.
+  + inversion_ASSERT.
+    intros; exploit final_inst_checker_eqlive; eauto.
+    eapply final_inst_checker_trans; eauto.
 Qed.
 
 Lemma path_step_eqlive path stk1 f sp rs1 m pc t s1 stk2 rs2: