Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into BTL

2 files changed, 112 insertions, 109 deletions

diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v
index e9ae11e0..c322a9a5 100644
--- a/scheduling/BTL_SEsimuref.v
+++ b/scheduling/BTL_SEsimuref.v
@@ -89,14 +89,13 @@ Proof.
   - intros; erewrite <- eval_sval_preserved; eauto.
 Qed.
 
-Lemma ris_simu_correct f1 f2 ris1 ris2 (ctx:simu_proof_context f1 f2) sis1 sis2 rs m: 
+Lemma ris_simu_correct f1 f2 ris1 ris2 (ctx:simu_proof_context f1 f2) sis1 sis2: 
   ris_simu ris1 ris2 ->
   ris_refines (bctx1 ctx) ris1 sis1 ->
   ris_refines (bctx2 ctx) ris2 sis2 ->
-  sem_sistate (bctx1 ctx) sis1 rs m ->
-  sem_sistate (bctx2 ctx) sis2 rs m.
+  sistate_simu ctx sis1 sis2.
 Proof.
-  intros RIS REF1 REF2 SEM.
+  intros RIS REF1 REF2 rs m SEM.
   exploit sem_sok; eauto.
   erewrite OK_EQUIV; eauto.
   intros ROK1.
@@ -113,62 +112,76 @@ Proof.
     erewrite REG_EQ; eauto.
 Qed.
 
-(* TODO:
-
-Definition option_refines ctx (orsv: option sval) (osv: option sval) :=
-  match orsv, osv with
-  | Some rsv, Some sv => eval_sval ctx rsv = eval_sval ctx sv
-  | None, None => True
-  | _, _ => False
-  end.
+Inductive optrsv_refines ctx: (option sval) -> (option sval) -> Prop :=
+  | RefSome rsv sv
+     (REF:eval_sval ctx rsv = eval_sval ctx sv)
+     :optrsv_refines ctx (Some rsv) (Some sv)
+  | RefNone: optrsv_refines ctx None None
+  .
 
-Definition sum_refines ctx (rsi: sval + ident) (si: sval + ident) :=
-  match rsi, si with
-  | inl rsv, inl sv => eval_sval ctx rsv = eval_sval ctx sv
-  | inr id, inr id' => id = id'
-  | _, _ => False
-  end.
+Inductive rsvident_refines ctx: (sval + ident) -> (sval + ident) -> Prop :=
+  | RefLeft rsv sv
+     (REF:eval_sval ctx rsv = eval_sval ctx sv)
+     :rsvident_refines ctx (inl rsv) (inl sv)
+  | RefRight id1 id2
+     (IDSIMU: id1 = id2)
+     :rsvident_refines ctx (inr id1) (inr id2)
+  .
 
 Definition bargs_refines ctx (rargs: list (builtin_arg sval)) (args: list (builtin_arg sval)): Prop :=
   eval_list_builtin_sval ctx rargs = eval_list_builtin_sval ctx args.
 
 Inductive rfv_refines ctx: sfval -> sfval -> Prop :=
-  | refines_Sgoto pc: rfv_refines ctx (Sgoto pc) (Sgoto pc)
-  | refines_Scall: forall sig rvos ros rargs args r pc
-      (SUM:sum_refines ctx rvos ros)
+  | RefGoto pc: rfv_refines ctx (Sgoto pc) (Sgoto pc)
+  | RefCall sig rvos ros rargs args r pc
+      (SV:rsvident_refines ctx rvos ros)
       (LIST:eval_list_sval ctx rargs = eval_list_sval ctx args)
-      ,rfv_refines ctx (Scall sig rvos rargs r pc) (Scall sig ros args r pc)
-  | refines_Stailcall: forall sig rvos ros rargs args
-      (SUM:sum_refines ctx rvos ros)
+      :rfv_refines ctx (Scall sig rvos rargs r pc) (Scall sig ros args r pc)
+  | RefTailcall sig rvos ros rargs args
+      (SV:rsvident_refines ctx rvos ros)
       (LIST:eval_list_sval ctx rargs = eval_list_sval ctx args)
-      ,rfv_refines ctx (Stailcall sig rvos rargs) (Stailcall sig ros args)
-  | refines_Sbuiltin: forall ef lbra lba br pc
+      :rfv_refines ctx (Stailcall sig rvos rargs) (Stailcall sig ros args)
+  | RefBuiltin ef lbra lba br pc
       (BARGS: bargs_refines ctx lbra lba)
-      ,rfv_refines ctx (Sbuiltin ef lbra br pc) (Sbuiltin ef lba br pc)
-  | refines_Sjumptable: forall rsv sv lpc
+      :rfv_refines ctx (Sbuiltin ef lbra br pc) (Sbuiltin ef lba br pc)
+  | RefJumptable rsv sv lpc
       (VAL: eval_sval ctx rsv = eval_sval ctx sv)
-      ,rfv_refines ctx (Sjumptable rsv lpc) (Sjumptable sv lpc)
-  | refines_Sreturn: forall orsv osv
-      (OPT:option_refines ctx orsv osv)
-      ,rfv_refines ctx (Sreturn orsv) (Sreturn osv)
+      :rfv_refines ctx (Sjumptable rsv lpc) (Sjumptable sv lpc)
+  | RefReturn orsv osv
+      (OPT:optrsv_refines ctx orsv osv)
+      :rfv_refines ctx (Sreturn orsv) (Sreturn osv)
 .
 
 Definition rfv_simu (rfv1 rfv2: sfval): Prop := rfv1 = rfv2.
 
-Local Hint Constructors sem_sfval equiv_state: core.
+Local Hint Resolve eval_sval_preserved list_sval_eval_preserved smem_eval_preserved eval_list_builtin_sval_preserved: core.
 
-Lemma rvf_simu_correct f1 f2 rfv1 rfv2 (ctx: simu_proof_context f1 f2) sfv1 sfv2 rs m t s: 
+Lemma rvf_simu_correct f1 f2 rfv1 rfv2 (ctx: simu_proof_context f1 f2) sfv1 sfv2: 
   rfv_simu rfv1 rfv2 ->
   rfv_refines (bctx1 ctx) rfv1 sfv1 ->
   rfv_refines (bctx2 ctx) rfv2 sfv2 ->
-  sem_sfval (bctx1 ctx) sfv1 rs m t s ->
-  exists s', sem_sfval (bctx2 ctx) sfv2 rs m t s' /\ equiv_state s s'.
+  sfv_simu ctx sfv1 sfv2.
 Proof.
-  unfold rfv_simu; intros X REF1 REF2 SEM. subst.
-  unfold bctx2; destruct REF1; inv REF2; inv SEM; simpl.
-  - eexists; split; eauto; simpl.
-    (* eapply State_equiv; eauto. NE MARCHE PAS ! *)
-Admitted.
+  unfold rfv_simu; intros X REF1 REF2. subst.
+  unfold bctx2; destruct REF1; inv REF2; simpl; econstructor; eauto.
+  - (* call svid *)
+    inv SV; inv SV0; econstructor; eauto.
+    rewrite <- REF, <- REF0; eauto.
+  - (* call args *)
+    rewrite <- LIST, <- LIST0; eauto.
+  - (* taillcall svid *)
+    inv SV; inv SV0; econstructor; eauto.
+    rewrite <- REF, <- REF0; eauto.
+  - (* tailcall args *)
+    rewrite <- LIST, <- LIST0; eauto.
+  - (* builtin args *)
+    unfold bargs_refines, bargs_simu in *.
+    rewrite <- BARGS, <- BARGS0; eauto.
+  - rewrite <- VAL, <- VAL0; eauto.
+  - (* return *)
+    inv OPT; inv OPT0; econstructor; eauto.
+    rewrite <- REF, <- REF0; eauto.
+Qed.
 
 (* refinement of (symbolic) state *)
 Inductive rstate :=
@@ -197,18 +210,18 @@ Inductive rst_simu: rstate -> rstate -> Prop :=
 
 (* Comment prend on en compte le ris en cours d'execution ??? *)
 Inductive rst_refines ctx: (* Prop -> *) rstate -> sstate -> Prop :=
-  | refines_Sfinal ris sis rfv sfv (*ok: Prop*)
+  | Reffinal ris sis rfv sfv (*ok: Prop*)
       (*OK: ris_ok ctx ris -> ok*)
       (RIS: ris_refines ctx ris sis)
       (RFV: ris_ok ctx ris -> rfv_refines ctx rfv sfv)
       : rst_refines ctx (*ok*) (Rfinal ris rfv) (Sfinal sis sfv)
-  | refines_Scond cond rargs args sm rifso rifnot ifso ifnot (*ok1 ok2: Prop*)
+  | Refcond cond rargs args sm rifso rifnot ifso ifnot (*ok1 ok2: Prop*)
       (*OK1: ok2 -> ok1*)
       (RCOND: (* ok2 -> *) seval_condition ctx cond rargs Sinit = seval_condition ctx cond args sm)
       (REFso: seval_condition ctx cond rargs Sinit = Some true -> rst_refines ctx (*ok2*) rifso ifso)
       (REFnot: seval_condition ctx cond rargs Sinit = Some false -> rst_refines ctx (*ok2*) rifnot ifnot)
       : rst_refines ctx (*ok1*) (Rcond cond rargs rifso rifnot) (Scond cond args sm ifso ifnot)
-  | refines_Sabort
+  | Refabort
       : rst_refines ctx Rabort Sabort
   .
 
@@ -223,37 +236,4 @@ Proof.
   induction 1; simpl; auto.
   - (* final *) intros f1 f2 ctx st1 st2 REF1 REF2 t s1 SEM1.
     inv REF1. inv REF2. inv SEM1.
-    exploit sem_sok; eauto.
-    rewrite OK_EQUIV; eauto.
-    intros RIS_OK1.
-    exploit (ris_simu_ok_preserv f1 f2); eauto.
-    intros RIS_OK2. intuition.
-    exploit ris_simu_correct; eauto.
-    exploit rvf_simu_correct; eauto.
-    simpl. (*
-    eexists; split.
-    + econstructor; eauto.
-      simpl.
-      clear SIS.
-      admit. (* TODO: condition sur les tr_inputs du simu_proof_context ! *)
-      (* TODO: le rfv_refines est trop sémantique ! *)
-    + admit.
-  - (* cond *) intros f1 f2 ctx st1 st2 REF1 REF2 t s1 SEM1.
-    inv REF1. inv REF2. inv SEM1.
-    destruct b; simpl.
-    + assert (TODO1: rst_refines (bctx1 ctx) rifso1 ifso). admit.
-      assert (TODO2: rst_refines (bctx2 ctx) rifso2 ifso0). admit.
-      exploit IHrst_simu1; eauto.
-      intros (s2 & X1 & X2).
-      exists s2; split; eauto.
-      econstructor; eauto.
-      * assert (TODO3: seval_condition (bctx2 ctx) cond args0 sm0 = Some true). admit.
-        eauto.
-      * simpl; eauto.
-   + admit.
-  - (* abort *) intros f1 f2 ctx st1 st2 REF1 REF2 t s1 SEM1.
-    inv REF1. inv SEM1.
-*)
-
-Admitted.
-*)
\ No newline at end of file
+Admitted.
\ No newline at end of file
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: