prepass scheduling proof finished !

proof of the two remaining lemmas

1 files changed, 56 insertions, 24 deletions

diff --git a/scheduling/RTLpathSE_theory.v b/scheduling/RTLpathSE_theory.v
index c43c530e..4c492ecd 100644
--- a/scheduling/RTLpathSE_theory.v
+++ b/scheduling/RTLpathSE_theory.v
@@ -1727,6 +1727,7 @@ Fixpoint seval_builtin_sval ge sp bsv rs0 m0 :=
   | BA_addrglobal id ptr => Some (BA_addrglobal id ptr)
   end.
 
+
 Fixpoint seval_list_builtin_sval ge sp lbsv rs0 m0 :=
   match lbsv with
   | nil => Some nil
@@ -1744,6 +1745,34 @@ Proof.
     try destruct (seval_list_builtin_sval _ _ _ _ _); discriminate.
 Qed.
 
+Lemma seval_builtin_sval_arg (ge:RTL.genv) sp rs0 m0 bs:
+   forall ba m v, 
+   seval_builtin_sval ge sp bs rs0 m0 = Some ba ->
+   eval_builtin_arg ge (fun id => id) sp m ba v ->
+   seval_builtin_arg ge sp m rs0 m0 bs v.
+Proof.
+   induction bs; simpl; 
+   try (intros ba m v H; inversion H; subst; clear H;
+        intros H; inversion H; subst;
+        econstructor; auto; fail).
+   - intros ba m v; destruct (seval_sval _ _ _ _ _) eqn: SV;
+     intros H; inversion H; subst; clear H.
+     intros H; inversion H; subst.
+     econstructor; auto.
+   - intros ba m v. 
+     destruct (seval_builtin_sval _ _ bs1 _ _) eqn: SV1; try congruence.
+     destruct (seval_builtin_sval _ _ bs2 _ _) eqn: SV2; try congruence.
+     intros H; inversion H; subst; clear H.
+     intros H; inversion H; subst.
+     econstructor; eauto.
+   - intros ba m v. 
+     destruct (seval_builtin_sval _ _ bs1 _ _) eqn: SV1; try congruence.
+     destruct (seval_builtin_sval _ _ bs2 _ _) eqn: SV2; try congruence.
+     intros H; inversion H; subst; clear H.
+     intros H; inversion H; subst.
+     econstructor; eauto.
+Qed.
+
 Lemma seval_builtin_arg_sval ge sp m rs0 m0 v: forall bs,
   seval_builtin_arg ge sp m rs0 m0 bs v ->
   exists ba,
@@ -1768,6 +1797,23 @@ Proof.
     + constructor; assumption.
 Qed.
 
+Lemma seval_builtin_sval_args (ge:RTL.genv) sp rs0 m0 lbs:
+   forall lba m v, 
+   seval_list_builtin_sval ge sp lbs rs0 m0 = Some lba ->
+   list_forall2 (eval_builtin_arg ge (fun id => id) sp m) lba v ->
+   seval_builtin_args ge sp m rs0 m0 lbs v.
+Proof.
+  unfold seval_builtin_args; induction lbs; simpl; intros lba m v.
+  - intros H; inversion H; subst; clear H.
+    intros H; inversion H. econstructor.
+  - destruct (seval_builtin_sval _ _ _ _ _) eqn:SV; try congruence.
+    destruct (seval_list_builtin_sval _ _ _ _ _) eqn: SVL; try congruence.
+    intros H; inversion H; subst; clear H.
+    intros H; inversion H; subst; clear H. 
+    econstructor; eauto.
+    eapply seval_builtin_sval_arg; eauto.
+Qed.
+
 Lemma seval_builtin_args_sval ge sp m rs0 m0 lv: forall lbs,
   seval_builtin_args ge sp m rs0 m0 lbs lv ->
   exists lba,
@@ -1790,36 +1836,22 @@ Lemma seval_builtin_sval_correct ge sp m rs0 m0: forall bs1 v bs2,
   (seval_builtin_sval ge sp bs1 rs0 m0) = (seval_builtin_sval ge sp bs2 rs0 m0) ->
   seval_builtin_arg ge sp m rs0 m0 bs2 v.
 Proof.
-  induction bs1.
-  all: try(destruct bs2;
-    intros Hinv Hrew;
-    inv Hinv;
-    cbn in *;
-    try constructor;
-    repeat (destruct seval_sval; [idtac | discriminate]);
-    repeat (destruct seval_builtin_sval; [idtac | discriminate]);
-    try congruence;
-    inv Hrew;
-    constructor).
-  - admit.
-  - admit.
-Admitted.
+  intros. exploit seval_builtin_arg_sval; eauto.
+  intros (ba & X1 & X2).
+  eapply seval_builtin_sval_arg; eauto.
+  congruence.
+Qed.
 
 Lemma seval_list_builtin_sval_correct ge sp m rs0 m0 vargs: forall lbs1,
   seval_builtin_args ge sp m rs0 m0 lbs1 vargs ->
   forall lbs2, (seval_list_builtin_sval ge sp lbs1 rs0 m0) = (seval_list_builtin_sval ge sp lbs2 rs0 m0) ->
   seval_builtin_args ge sp m rs0 m0 lbs2 vargs.
 Proof.
-  induction 1.
-  - simpl. intros.
-    exploit seval_list_builtin_sval_nil; eauto. intro. subst. constructor.
-  - eapply seval_builtin_arg_sval in H. destruct H as (ba & A & B).
-    eapply seval_builtin_args_sval in H0. destruct H0 as (lba & A' & B').
-    intros. destruct lbs2.
-    + simpl in H. rewrite A in H. rewrite A' in H.
-      discriminate.
-    + constructor. 2: apply IHlist_forall2. 2: admit.
-Admitted.
+  intros. exploit seval_builtin_args_sval; eauto.
+  intros (ba & X1 & X2).
+  eapply seval_builtin_sval_args; eauto.
+  congruence.
+Qed.
 
 (* NOTE: we need to mix semantical simulation and syntactic definition on [sfval] in order to abstract the [match_states] *)
 Inductive sfval_simu (dm: PTree.t node) (f: RTLpath.function) (opc1 opc2: node) (ctx: simu_proof_context f): sfval -> sfval -> Prop :=