starting BTL_SEsimuref

2 files changed, 318 insertions, 99 deletions

diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v
new file mode 100644
index 00000000..af2159cb
--- /dev/null
+++ b/scheduling/BTL_SEsimuref.v
@@ -0,0 +1,317 @@
+(** Refinement of BTL_SEtheory data-structures
+    in order to introduce (and prove correct) a lower-level specification of the simulation test.
+
+    TODO: not yet with hash-consing ? Or "fake" hash-consing only ?
+
+    Ceci est un "bac à sable".
+
+    - On introduit une représentation plus concrète pour les types d'état symbolique [sistate] et [sstate].
+    - Etant donné une spécification intuitive "*_simu" pour tester la simulation sur cette représentation des états symboliques,
+      on essaye déjà de trouver les bonnes notions de raffinement "*_refines" qui permette de prouver les lemmes "*_simu_correct".
+    - Il faudra ensuite vérifier que l'exécution symbolique préserve ces relations de raffinement !
+
+*)
+
+Require Import Coqlib Maps Floats.
+Require Import AST Integers Values Events Memory Globalenvs Smallstep.
+Require Import Op Registers.
+Require Import RTL BTL OptionMonad BTL_SEtheory.
+
+(** * Preservation properties *)
+
+(* TODO: inherited from RTLpath. Use simu_proof_context + bctx2 + bctx1 instead of all the hypotheses/variables below ? *)
+ 
+Section SymbValPreserved.
+
+Variable ge ge': BTL.genv.
+
+Hypothesis symbols_preserved_BTL: forall s, Genv.find_symbol ge' s = Genv.find_symbol ge s.
+
+Hypothesis senv_preserved_BTL: Senv.equiv ge ge'.
+
+Lemma senv_find_symbol_preserved id:
+  Senv.find_symbol ge id = Senv.find_symbol ge' id.
+Proof.
+  destruct senv_preserved_BTL as (A & B & C). congruence.
+Qed.
+
+Lemma senv_symbol_address_preserved id ofs:
+  Senv.symbol_address ge id ofs = Senv.symbol_address ge' id ofs.
+Proof.
+  unfold Senv.symbol_address. rewrite senv_find_symbol_preserved.
+  reflexivity.
+Qed.
+
+Variable stk stk': list stackframe.
+Variable f f': function.
+Variable sp: val.
+Variable rs0: regset.
+Variable m0: mem.
+
+Lemma eval_sval_preserved sv:
+  eval_sval (Bctx ge stk f sp rs0 m0) sv = eval_sval (Bctx ge' stk' f' sp rs0 m0) sv.
+Proof.
+  induction sv using sval_mut with (P0 := fun lsv => eval_list_sval (Bctx ge stk f sp rs0 m0) lsv = eval_list_sval (Bctx ge' stk' f' sp rs0 m0) lsv)
+                                   (P1 := fun sm => eval_smem (Bctx ge stk f sp rs0 m0) sm = eval_smem (Bctx ge' stk' f' sp rs0 m0) sm); simpl; auto.
+  + rewrite IHsv; clear IHsv. destruct (eval_list_sval _ _); auto.
+    rewrite IHsv0; clear IHsv0. destruct (eval_smem _ _); auto.
+    erewrite eval_operation_preserved; eauto.
+  + rewrite IHsv0; clear IHsv0. destruct (eval_list_sval _ _); auto.
+    erewrite <- eval_addressing_preserved; eauto.
+    destruct (eval_addressing _ sp _ _); auto.
+    rewrite IHsv; auto.
+  + rewrite IHsv; clear IHsv. destruct (eval_sval _ _); auto.
+    rewrite IHsv0; auto.
+  + rewrite IHsv0; clear IHsv0. destruct (eval_list_sval _ _); auto.
+    erewrite <- eval_addressing_preserved; eauto.
+    destruct (eval_addressing _ sp _ _); auto.
+    rewrite IHsv; clear IHsv. destruct (eval_smem _ _); auto.
+    rewrite IHsv1; auto.
+Qed.
+
+Lemma seval_builtin_arg_preserved m: forall bs varg,
+  seval_builtin_arg (Bctx ge stk f sp rs0 m0) m bs varg ->
+  seval_builtin_arg (Bctx ge' stk' f' sp rs0 m0) m bs varg.
+Proof.
+  induction 1; simpl.
+  all: try (constructor; auto).
+  - rewrite <- eval_sval_preserved. assumption.
+  - rewrite <- senv_symbol_address_preserved. assumption.
+  - rewrite senv_symbol_address_preserved. eapply seval_BA_addrglobal.
+Qed.
+
+Lemma seval_builtin_args_preserved m lbs vargs:
+  seval_builtin_args (Bctx ge stk f sp rs0 m0) m lbs vargs ->
+  seval_builtin_args (Bctx ge' stk' f' sp rs0 m0) m lbs vargs.
+Proof.
+  induction 1; constructor; eauto.
+  eapply seval_builtin_arg_preserved; auto.
+Qed.
+
+Lemma list_sval_eval_preserved lsv: 
+  eval_list_sval (Bctx ge stk f sp rs0 m0) lsv = eval_list_sval (Bctx ge' stk' f' sp rs0 m0) lsv.
+Proof.
+  induction lsv; simpl; auto.
+  rewrite eval_sval_preserved. destruct (eval_sval _ _); auto.
+  rewrite IHlsv; auto.
+Qed.
+
+Lemma smem_eval_preserved sm: 
+  eval_smem (Bctx ge stk f sp rs0 m0) sm = eval_smem (Bctx ge' stk' f' sp rs0 m0) sm.
+Proof.
+  induction sm; simpl; auto.
+  rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto.
+  erewrite <- eval_addressing_preserved; eauto.
+  destruct (eval_addressing _ sp _ _); auto.
+  rewrite IHsm; clear IHsm. destruct (eval_smem _ _); auto.
+  rewrite eval_sval_preserved; auto.
+Qed.
+
+Lemma seval_condition_preserved cond lsv sm:
+  seval_condition (Bctx ge stk f sp rs0 m0) cond lsv sm = seval_condition (Bctx ge' stk' f' sp rs0 m0) cond lsv sm.
+Proof.
+  unfold seval_condition.
+  rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto.
+  rewrite smem_eval_preserved; auto.
+Qed.
+
+End SymbValPreserved.
+
+(** * ... *)
+
+Record sis_ok ctx (sis: sistate): Prop := {
+  OK_PRE: (sis.(si_pre) ctx);
+  OK_SMEM: eval_smem ctx sis.(si_smem) <> None;
+  OK_SREG: forall (r: reg), eval_sval ctx (si_sreg sis r) <> None
+}.
+Local Hint Resolve OK_PRE OK_SMEM OK_SREG: core.
+Local Hint Constructors sis_ok: core.
+
+Lemma sem_sok ctx sis rs m:
+  sem_sistate ctx sis rs m ->  sis_ok ctx sis.
+Proof.
+  unfold sem_sistate;
+  econstructor;
+  intuition congruence.
+Qed.
+
+(* NB: refinement of (symbolic) internal state *)
+Record ristate := 
+  { 
+    (** [ris_smem] represents the current smem symbolic evaluations.
+        (we also recover the history of smem in ris_smem)  *)
+    ris_smem: smem;
+    (** For the values in registers:
+        1) we store a list of sval evaluations
+        2) we encode the symbolic regset by a PTree + a boolean indicating the default sval *)
+    ris_input_init: bool;
+    ris_ok_sval: list sval;
+    ris_sreg:> PTree.t sval
+  }.
+
+Definition ris_sreg_get (ris: ristate) r: sval :=
+   match PTree.get r ris with
+   | None => if ris_input_init ris then Sinput r else Sundef
+   | Some sv => sv
+   end.
+Coercion ris_sreg_get: ristate >-> Funclass.
+
+Record ris_ok ctx (ris: ristate) : Prop := {
+   OK_RMEM: (eval_smem ctx (ris_smem ris)) <> None;
+   OK_RREG: forall sv, List.In sv (ris_ok_sval ris) -> eval_sval ctx sv <> None
+}.
+Local Hint Resolve OK_RMEM OK_RREG: core.
+Local Hint Constructors ris_ok: core.
+
+Record ris_refines ctx (ris: ristate) (sis: sistate): Prop := {
+  OK_EQUIV: sis_ok ctx sis <-> ris_ok ctx ris;
+  MEM_EQ: ris_ok ctx ris ->  eval_smem ctx ris.(ris_smem) = eval_smem ctx sis.(si_smem);
+  REG_EQ: ris_ok ctx ris -> forall r, eval_sval ctx (ris_sreg_get ris r) = eval_sval ctx (si_sreg sis r);
+      (* the below invariant allows to evaluate operations in the initial memory of the path instead of the current memory *)
+  VALID_PRESERV: forall m b ofs, eval_smem ctx sis.(si_smem) = Some m -> Mem.valid_pointer m b ofs = Mem.valid_pointer (cm0 ctx) b ofs
+}.
+Local Hint Resolve OK_EQUIV MEM_EQ REG_EQ VALID_PRESERV: core.
+Local Hint Constructors ris_refines: core.
+
+Record ris_simu ris1 ris2: Prop := {
+  SIMU_FAILS: forall sv, List.In sv ris2.(ris_ok_sval) -> List.In sv ris1.(ris_ok_sval);
+  SIMU_MEM: ris1.(ris_smem) = ris2.(ris_smem);
+  SIMU_REG: forall r, ris_sreg_get ris1 r = ris_sreg_get ris2 r
+}.
+Local Hint Resolve SIMU_FAILS SIMU_MEM SIMU_REG: core.
+Local Hint Constructors ris_simu: core.
+Local Hint Resolve sge_match: core.
+
+Lemma ris_simu_ok_preserv f1 f2 ris1 ris2 (ctx:simu_proof_context):
+  ris_simu ris1 ris2 -> ris_ok (bctx1 f1 ctx) ris1 -> ris_ok (bctx2 f2 ctx) ris2.
+Proof.
+  intros SIMU OK; econstructor; eauto.
+  - erewrite <- SIMU_MEM; eauto.
+    unfold bctx2; erewrite smem_eval_preserved; eauto.
+  - unfold bctx2; intros; erewrite eval_sval_preserved; eauto.
+Qed.
+
+Lemma ris_simu_correct f1 f2 ris1 ris2 (ctx:simu_proof_context) sis1 sis2 rs m: 
+  ris_simu ris1 ris2 ->
+  ris_refines (bctx1 f1 ctx) ris1 sis1 ->
+  ris_refines (bctx2 f2 ctx) ris2 sis2 ->
+  sem_sistate (bctx1 f1 ctx) sis1 rs m ->
+  sem_sistate (bctx2 f2 ctx) sis2 rs m.
+Proof.
+  intros RIS REF1 REF2 SEM.
+  (* destruct REF1. destruct REF2. *)
+  exploit sem_sok; eauto.
+  erewrite OK_EQUIV; eauto.
+  intros ROK1.
+  exploit ris_simu_ok_preserv; eauto.
+  intros ROK2. generalize ROK2; erewrite <- OK_EQUIV; eauto.
+  intros SOK2.
+  destruct SEM as (PRE & SMEM & SREG).
+  unfold sem_sistate; intuition eauto.
+  + erewrite <- MEM_EQ, <- SIMU_MEM; eauto.
+    unfold bctx2; erewrite smem_eval_preserved; eauto.
+    erewrite MEM_EQ; eauto.
+  + erewrite <- REG_EQ, <- SIMU_REG; eauto.
+    unfold bctx2; erewrite eval_sval_preserved; eauto.
+    erewrite REG_EQ; eauto.
+Qed.
+
+Definition rfv_refines ctx (rfv sfv: sfval): Prop :=
+  forall rs m t s, sem_sfval ctx rfv rs m t s <-> sem_sfval ctx sfv rs m t s.
+
+Definition rfv_simu (rfv1 rfv2: sfval): Prop := rfv1 = rfv2.
+
+Lemma rvf_simu_correct f1 f2 rfv1 rfv2 (ctx: simu_proof_context) sfv1 sfv2 rs m t s: 
+  rfv_simu rfv1 rfv2 ->
+  rfv_refines (bctx1 f1 ctx) rfv1 sfv1 ->
+  rfv_refines (bctx2 f2 ctx) rfv2 sfv2 ->
+  sem_sfval (bctx1 f1 ctx) sfv1 rs m t s ->
+  sem_sfval (bctx2 f2 ctx) sfv2 rs m t s.
+Proof.
+  unfold rfv_simu, rfv_refines; intros X REF1 REF2 SEM. subst.
+  rewrite <- REF2.
+  assert (sem_sfval (bctx1 f1 ctx) rfv2 rs m t s). { rewrite REF1; auto. }
+Admitted.
+
+(* refinement of (symbolic) state *)
+Inductive rstate :=
+  | Rfinal (ris: ristate) (rfv: sfval)
+  | Rcond (cond: condition) (rargs: list_sval) (rifso rifnot: rstate)
+  | Rabort
+  .
+
+Inductive rst_simu: rstate -> rstate -> Prop :=
+  | Rfinal_simu ris1 ris2 rfv1 rfv2:
+      ris_simu ris1 ris2 ->
+      rfv_simu rfv1 rfv2 ->
+      rst_simu (Rfinal ris1 rfv1) (Rfinal ris2 rfv2)
+  | Rcond_simu cond rargs rifso1 rifnot1 rifso2 rifnot2:
+      rst_simu rifso1 rifso2 ->
+      rst_simu rifnot1 rifnot2 ->
+      rst_simu (Rcond cond rargs rifso1 rifnot1) (Rcond cond rargs rifso2 rifnot2)
+  | Rabort_simu: rst_simu Rabort Rabort
+(* TODO: extension à voir dans un second temps !
+  | Rcond_skip cond rargs rifso1 rifnot1 rst:
+      rst_simu rifso1 rst ->
+      rst_simu rifnot1 rst ->
+      rst_simu (Rcond cond rargs rifso1 rifnot1) rst
+*)
+  .
+
+(* 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*)
+      (*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*)
+      (*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
+      : rst_refines ctx Rabort Sabort
+  .
+
+Lemma rst_simu_correct rst1 rst2:
+   rst_simu rst1 rst2 ->
+   forall f1 f2 ctx st1 st2 (*ok1 ok2*),
+   rst_refines (*ok1*) (bctx1 f1 ctx) rst1 st1 ->
+   rst_refines (*ok2*) (bctx2 f2 ctx) rst2 st2 ->
+   (* ok1 -> ok2 -> *)
+   sstate_simu f1 f2 ctx st1 st2.
+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.
+      admit. (* TODO: condition sur les tr_inputs: à ajouter plutôt dans le simu_proof_context ! *)
+    + 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 f1 ctx) rifso1 ifso). admit.
+      assert (TODO2: rst_refines (bctx2 f2 ctx) rifso2 ifso0). admit.
+      exploit IHrst_simu1; eauto.
+      intros (s2 & X1 & X2).
+      exists s2; split; eauto.
+      econstructor; eauto.
+      * assert (TODO3: seval_condition (bctx2 f2 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.
diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
index 3083ca71..c7a44153 100644
--- a/scheduling/BTL_SEtheory.v
+++ b/scheduling/BTL_SEtheory.v
@@ -1057,102 +1057,4 @@ Proof.
   intros (s3 & STEP2 & EQ2).
   clear STEP1; eexists; split; eauto.
   eapply equiv_state_trans; eauto.
-Qed.
-
-(** * Preservation properties *)
-
-Section SymbValPreserved.
-
-Variable ge ge': BTL.genv.
-
-Hypothesis symbols_preserved_BTL: forall s, Genv.find_symbol ge' s = Genv.find_symbol ge s.
-
-Hypothesis senv_preserved_BTL: Senv.equiv ge ge'.
-
-Lemma senv_find_symbol_preserved id:
-  Senv.find_symbol ge id = Senv.find_symbol ge' id.
-Proof.
-  destruct senv_preserved_BTL as (A & B & C). congruence.
-Qed.
-
-Lemma senv_symbol_address_preserved id ofs:
-  Senv.symbol_address ge id ofs = Senv.symbol_address ge' id ofs.
-Proof.
-  unfold Senv.symbol_address. rewrite senv_find_symbol_preserved.
-  reflexivity.
-Qed.
-
-Variable stk stk': list stackframe.
-Variable f f': function.
-Variable sp: val.
-Variable rs0: regset.
-Variable m0: mem.
-
-Lemma eval_sval_preserved sv:
-  eval_sval (Bctx ge stk f sp rs0 m0) sv = eval_sval (Bctx ge' stk' f' sp rs0 m0) sv.
-Proof.
-  induction sv using sval_mut with (P0 := fun lsv => eval_list_sval (Bctx ge stk f sp rs0 m0) lsv = eval_list_sval (Bctx ge' stk' f' sp rs0 m0) lsv)
-                                   (P1 := fun sm => eval_smem (Bctx ge stk f sp rs0 m0) sm = eval_smem (Bctx ge' stk' f' sp rs0 m0) sm); simpl; auto.
-  + rewrite IHsv; clear IHsv. destruct (eval_list_sval _ _); auto.
-    rewrite IHsv0; clear IHsv0. destruct (eval_smem _ _); auto.
-    erewrite eval_operation_preserved; eauto.
-  + rewrite IHsv0; clear IHsv0. destruct (eval_list_sval _ _); auto.
-    erewrite <- eval_addressing_preserved; eauto.
-    destruct (eval_addressing _ sp _ _); auto.
-    rewrite IHsv; auto.
-  + rewrite IHsv; clear IHsv. destruct (eval_sval _ _); auto.
-    rewrite IHsv0; auto.
-  + rewrite IHsv0; clear IHsv0. destruct (eval_list_sval _ _); auto.
-    erewrite <- eval_addressing_preserved; eauto.
-    destruct (eval_addressing _ sp _ _); auto.
-    rewrite IHsv; clear IHsv. destruct (eval_smem _ _); auto.
-    rewrite IHsv1; auto.
-Qed.
-
-Lemma seval_builtin_arg_preserved m: forall bs varg,
-  seval_builtin_arg (Bctx ge stk f sp rs0 m0) m bs varg ->
-  seval_builtin_arg (Bctx ge' stk' f' sp rs0 m0) m bs varg.
-Proof.
-  induction 1; simpl.
-  all: try (constructor; auto).
-  - rewrite <- eval_sval_preserved. assumption.
-  - rewrite <- senv_symbol_address_preserved. assumption.
-  - rewrite senv_symbol_address_preserved. eapply seval_BA_addrglobal.
-Qed.
-
-Lemma seval_builtin_args_preserved m lbs vargs:
-  seval_builtin_args (Bctx ge stk f sp rs0 m0) m lbs vargs ->
-  seval_builtin_args (Bctx ge' stk' f' sp rs0 m0) m lbs vargs.
-Proof.
-  induction 1; constructor; eauto.
-  eapply seval_builtin_arg_preserved; auto.
-Qed.
-
-Lemma list_sval_eval_preserved lsv: 
-  eval_list_sval (Bctx ge stk f sp rs0 m0) lsv = eval_list_sval (Bctx ge' stk' f' sp rs0 m0) lsv.
-Proof.
-  induction lsv; simpl; auto.
-  rewrite eval_sval_preserved. destruct (eval_sval _ _); auto.
-  rewrite IHlsv; auto.
-Qed.
-
-Lemma smem_eval_preserved sm: 
-  eval_smem (Bctx ge stk f sp rs0 m0) sm = eval_smem (Bctx ge' stk' f' sp rs0 m0) sm.
-Proof.
-  induction sm; simpl; auto.
-  rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto.
-  erewrite <- eval_addressing_preserved; eauto.
-  destruct (eval_addressing _ sp _ _); auto.
-  rewrite IHsm; clear IHsm. destruct (eval_smem _ _); auto.
-  rewrite eval_sval_preserved; auto.
-Qed.
-
-Lemma seval_condition_preserved cond lsv sm:
-  seval_condition (Bctx ge stk f sp rs0 m0) cond lsv sm = seval_condition (Bctx ge' stk' f' sp rs0 m0) cond lsv sm.
-Proof.
-  unfold seval_condition.
-  rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto.
-  rewrite smem_eval_preserved; auto.
-Qed.
-
-End SymbValPreserved.
+Qed.
\ No newline at end of file