progress in BTL_SEsimuref

1 files changed, 54 insertions, 31 deletions

diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
index 7f00e46f..557541ce 100644
--- a/scheduling/BTL_SEtheory.v
+++ b/scheduling/BTL_SEtheory.v
@@ -235,16 +235,16 @@ Proof.
     eapply seval_builtin_arg_exact; eauto.
 Qed.
 
-Fixpoint seval_builtin_sval ctx bsv :=
+Fixpoint eval_builtin_sval ctx bsv :=
   match bsv with
   | BA sv => SOME v <- eval_sval ctx sv IN Some (BA v)
   | BA_splitlong sv1 sv2 =>
-      SOME v1 <- seval_builtin_sval ctx sv1 IN
-      SOME v2 <- seval_builtin_sval ctx sv2 IN
+      SOME v1 <- eval_builtin_sval ctx sv1 IN
+      SOME v2 <- eval_builtin_sval ctx sv2 IN
       Some (BA_splitlong v1 v2)
   | BA_addptr sv1 sv2 =>
-      SOME v1 <- seval_builtin_sval ctx sv1 IN
-      SOME v2 <- seval_builtin_sval ctx sv2 IN
+      SOME v1 <- eval_builtin_sval ctx sv1 IN
+      SOME v2 <- eval_builtin_sval ctx sv2 IN
       Some (BA_addptr v1 v2)
   | BA_int i => Some (BA_int i)
   | BA_long l => Some (BA_long l)
@@ -259,7 +259,7 @@ Fixpoint seval_builtin_sval ctx bsv :=
 Fixpoint eval_list_builtin_sval ctx lbsv :=
   match lbsv with
   | nil => Some nil
-  | bsv::lbsv => SOME v <- seval_builtin_sval ctx bsv IN
+  | bsv::lbsv => SOME v <- eval_builtin_sval ctx bsv IN
                  SOME lv <- eval_list_builtin_sval ctx lbsv IN
                  Some (v::lv)
   end.
@@ -271,9 +271,9 @@ Proof.
   destruct lbs2; simpl; repeat autodestruct; congruence.
 Qed.
 
-Lemma seval_builtin_sval_arg ctx bs:
+Lemma eval_builtin_sval_arg ctx bs:
    forall ba m v, 
-   seval_builtin_sval ctx bs = Some ba ->
+   eval_builtin_sval ctx bs = Some ba ->
    eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m ba v ->
    seval_builtin_arg ctx m bs v.
 Proof.
@@ -286,14 +286,14 @@ Proof.
      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.
+     destruct (eval_builtin_sval _ bs1) eqn: SV1; try congruence.
+     destruct (eval_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.
+     destruct (eval_builtin_sval _ bs1) eqn: SV1; try congruence.
+     destruct (eval_builtin_sval _ bs2) eqn: SV2; try congruence.
      intros H; inversion H; subst; clear H.
      intros H; inversion H; subst.
      econstructor; eauto.
@@ -302,7 +302,7 @@ Qed.
 Lemma seval_builtin_arg_sval ctx m v: forall bs,
   seval_builtin_arg ctx m bs v ->
   exists ba,
-    seval_builtin_sval ctx bs = Some ba
+    eval_builtin_sval ctx bs = Some ba
     /\ eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m ba v.
 Proof.
   induction 1.
@@ -323,7 +323,7 @@ Proof.
     + constructor; assumption.
 Qed.
 
-Lemma seval_builtin_sval_args ctx lbs:
+Lemma eval_builtin_sval_args ctx lbs:
    forall lba m v, 
    eval_list_builtin_sval ctx lbs = Some lba ->
    list_forall2 (eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m) lba v ->
@@ -332,12 +332,12 @@ 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 (eval_builtin_sval _ _) eqn:SV; try congruence.
     destruct (eval_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.
+    eapply eval_builtin_sval_arg; eauto.
 Qed.
 
 Lemma seval_builtin_args_sval ctx m lv: forall lbs,
@@ -357,14 +357,14 @@ Proof.
     + constructor; assumption.
 Qed.
 
-Lemma seval_builtin_sval_correct ctx m: forall bs1 v bs2,
+Lemma eval_builtin_sval_correct ctx m: forall bs1 v bs2,
   seval_builtin_arg ctx m bs1 v ->
-  (seval_builtin_sval ctx bs1) = (seval_builtin_sval ctx bs2) ->
+  (eval_builtin_sval ctx bs1) = (eval_builtin_sval ctx bs2) ->
   seval_builtin_arg ctx m bs2 v.
 Proof.
   intros. exploit seval_builtin_arg_sval; eauto.
   intros (ba & X1 & X2).
-  eapply seval_builtin_sval_arg; eauto.
+  eapply eval_builtin_sval_arg; eauto.
   congruence.
 Qed.
 
@@ -375,7 +375,7 @@ Lemma eval_list_builtin_sval_correct ctx m vargs: forall lbs1,
 Proof.
   intros. exploit seval_builtin_args_sval; eauto.
   intros (ba & X1 & X2).
-  eapply seval_builtin_sval_args; eauto.
+  eapply eval_builtin_sval_args; eauto.
   congruence.
 Qed.
 
@@ -1110,19 +1110,19 @@ Definition bctx2 {f1 f2} (ctx: simu_proof_context f1 f2):= Bctx ctx.(sge2) f2 ct
 *)
 
 Inductive optsv_simu {f1 f2: function} (ctx: simu_proof_context f1 f2): (option sval) -> (option sval) -> Prop :=
-  | Ssome_simu sv1 sv2:
-     eval_sval (bctx1 ctx) sv1 = eval_sval (bctx2 ctx) sv2
-     -> optsv_simu ctx (Some sv1) (Some sv2)
+  | Ssome_simu sv1 sv2
+     (SIMU:eval_sval (bctx1 ctx) sv1 = eval_sval (bctx2 ctx) sv2)
+     :optsv_simu ctx (Some sv1) (Some sv2)
   | Snone_simu: optsv_simu ctx None None
   .
 
 Inductive svident_simu {f1 f2: function} (ctx: simu_proof_context f1 f2): (sval + ident) -> (sval + ident) -> Prop :=
-  | Sleft_simu sv1 sv2:
-     eval_sval (bctx1 ctx) sv1 = eval_sval (bctx2 ctx) sv2
-     -> svident_simu ctx (inl sv1) (inl sv2)
-  | Sright_simu id1 id2:
-     id1 = id2
-     -> svident_simu ctx (inr id1) (inr id2)
+  | Sleft_simu sv1 sv2
+     (SIMU:eval_sval (bctx1 ctx) sv1 = eval_sval (bctx2 ctx) sv2)
+     :svident_simu ctx (inl sv1) (inl sv2)
+  | Sright_simu id1 id2
+     (IDSIMU: id1 = id2)
+     :svident_simu ctx (inr id1) (inr id2)
   .
 
 Definition bargs_simu {f1 f2: function} (ctx: simu_proof_context f1 f2) (args1 args2: list (builtin_arg sval)): Prop :=
@@ -1149,9 +1149,14 @@ Inductive sfv_simu {f1 f2} (ctx: simu_proof_context f1 f2): sfval -> sfval -> Pr
       :sfv_simu ctx (Sreturn osv1) (Sreturn osv2)
 .
 
+Definition sistate_simu {f1 f2} (ctx: simu_proof_context f1 f2) (sis1 sis2:sistate): Prop :=
+  forall rs m, sem_sistate (bctx1 ctx) sis1 rs m -> sem_sistate (bctx2 ctx) sis2 rs m.
+
 Definition sstate_simu {f1 f2} (ctx: simu_proof_context f1 f2) (st1 st2:sstate): Prop :=
   forall sis1 sfv1, run_sem_isstate (bctx1 ctx) st1 = Some (sout sis1 sfv1) ->
-  exists sis2 sfv2, run_sem_isstate (bctx2 ctx) st2 = Some (sout sis2 sfv2) /\ sfv_simu ctx sfv1 sfv2
+  exists sis2 sfv2, run_sem_isstate (bctx2 ctx) st2 = Some (sout sis2 sfv2) 
+                   /\ sistate_simu ctx sis1 sis2
+                   /\ sfv_simu ctx sfv1 sfv2
   .
 
 Definition symbolic_simu f1 f2 ib1 ib2: Prop := forall (ctx: simu_proof_context f1 f2), sstate_simu ctx (sexec f1 ib1) (sexec f2 ib2).
@@ -1182,7 +1187,7 @@ Proof.
 Qed.
 *)
 
-(** * Preservation properties *)
+(** * Preservation properties under a [simu_proof_context] *)
 
 Section SymbValPreserved.
 
@@ -1231,6 +1236,23 @@ Proof.
   rewrite eval_sval_preserved; auto.
 Qed.
 
+Lemma eval_builtin_sval_preserved sv:
+   eval_builtin_sval (bctx1 ctx) sv = eval_builtin_sval (bctx2 ctx) sv.
+Proof.
+  induction sv; simpl; auto.
+  all: try (erewrite eval_sval_preserved by eauto); trivial.
+  all: erewrite IHsv1 by eauto; erewrite IHsv2 by eauto; reflexivity.
+Qed.
+
+Lemma eval_list_builtin_sval_preserved lsv:
+   eval_list_builtin_sval (bctx1 ctx) lsv = eval_list_builtin_sval (bctx2 ctx) lsv.
+Proof.
+  induction lsv; simpl; auto.
+  erewrite eval_builtin_sval_preserved by eauto.
+  erewrite IHlsv by eauto.
+  reflexivity.
+Qed.
+
 Lemma seval_condition_preserved cond lsv sm:
   seval_condition (bctx1 ctx) cond lsv sm = seval_condition (bctx2 ctx) cond lsv sm.
 Proof.
@@ -1239,6 +1261,7 @@ Proof.
   rewrite smem_eval_preserved; auto.
 Qed.
 
+(* additional preservation properties under this additional hypothesis *)
 Hypothesis senv_preserved_BTL: Senv.equiv (sge1 ctx) (sge2 ctx).
 
 Lemma senv_find_symbol_preserved id: