starting refinement of symbolic execution

1 files changed, 106 insertions, 3 deletions

diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v
index a4da4291..6d74ccf9 100644
--- a/scheduling/BTL_SEsimuref.v
+++ b/scheduling/BTL_SEsimuref.v
@@ -1,13 +1,18 @@
 (** Refinement of BTL_SEtheory data-structures
     in order to introduce (and prove correct) a lower-level specification of the simulation test.
 
-    Ceci est un "bac à sable". TODO: A REVOIR COMPLETEMENT. Introduire "fake" hash-consing
+    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 !
 
+    TODO: A REVOIR COMPLETEMENT.
+    - essayer de découper chaque relation de raffinement en une fonction "projection/abstraction" (à la "hsval_proj" à renommer en "hsval_abstract") 
+      et une équivalence sur la représentation abstraite.
+    - introduire "fake" hash-consed values (à renommer en "refined" plutôt que "fake").
+
 *)
 
 Require Import Coqlib Maps Floats.
@@ -15,7 +20,7 @@ Require Import AST Integers Values Events Memory Globalenvs Smallstep.
 Require Import Op Registers.
 Require Import RTL BTL OptionMonad BTL_SEtheory.
 
-(** * ... *)
+(** * Refinement of data-structures and of the specification of the simulation test *)
 
 Record sis_ok ctx (sis: sistate): Prop := {
   OK_PRE: (sis.(si_pre) ctx);
@@ -254,6 +259,103 @@ Proof.
     * exploit IHrst_simu2; eauto.
 Qed.
 
+(** * Refinement of the symbolic execution *)
+
+Local Hint Constructors rfv_refines optrsv_refines rsvident_refines rsvident_refines: core.
+
+Lemma eval_list_sval_refpreserv ctx args ris sis:
+  ris_refines ctx ris sis ->
+  ris_ok ctx ris ->
+  eval_list_sval ctx (list_sval_inj (map ris args)) =
+  eval_list_sval ctx (list_sval_inj (map sis args)).
+Proof.
+  intros REF OK.
+  induction args; simpl; eauto.
+  intros; erewrite REG_EQ, IHargs; eauto.
+Qed.
+
+Local Hint Resolve eval_list_sval_refpreserv: core.
+
+Lemma eval_builtin_sval_refpreserv ctx arg ris sis:
+  ris_refines ctx ris sis ->
+  ris_ok ctx ris ->
+  eval_builtin_sval ctx (builtin_arg_map ris arg) = eval_builtin_sval ctx (builtin_arg_map sis arg).
+Proof.
+  intros REF OK; induction arg; simpl; eauto.
+  + erewrite REG_EQ; eauto.
+  + erewrite IHarg1, IHarg2; eauto.
+  + erewrite IHarg1, IHarg2; eauto.
+Qed.
+
+Lemma bargs_refpreserv ctx args ris sis:
+  ris_refines ctx ris sis ->
+  ris_ok ctx ris ->
+  bargs_refines ctx (map (builtin_arg_map ris) args) (map (builtin_arg_map sis) args).
+Proof.
+  unfold bargs_refines. intros REF OK.
+  induction args; simpl; eauto.
+  erewrite eval_builtin_sval_refpreserv, IHargs; eauto.
+Qed.
+
+Local Hint Resolve bargs_refpreserv: core.
+
+Lemma exec_final_refpreserv ctx i ris sis:
+  ris_refines ctx ris sis ->
+  ris_ok ctx ris ->
+  rfv_refines ctx (sexec_final_sfv i ris) (sexec_final_sfv i sis).
+Proof.
+  destruct i; simpl; unfold sum_left_map; try autodestruct; eauto.
+Qed.
+
+Definition ris_init: ristate := {| ris_smem:= Sinit; ris_input_init:=true; ris_ok_sval := nil; ris_sreg := PTree.empty _ |}.
+
+Lemma ris_init_correct ctx:
+  ris_refines ctx ris_init sis_init.
+Proof.
+  unfold ris_init, sis_init; econstructor; simpl in *; eauto.
+  + split; destruct 1; econstructor; simpl in *; eauto.
+    congruence.
+  + destruct 1; simpl in *. unfold ris_sreg_get; simpl.
+    intros; rewrite PTree.gempty; eauto.
+  + try_simplify_someHyps.
+Qed.
+
+Definition rset_smem rm (ris:ristate): ristate :=
+  {| ris_smem := rm;
+     ris_input_init := ris.(ris_input_init);
+     ris_ok_sval := ris.(ris_ok_sval);
+     ris_sreg:= ris.(ris_sreg)
+  |}.
+
+Lemma sis_ok_set_mem ctx sm sis:
+  sis_ok ctx (set_smem sm sis)
+  <-> (sis_ok ctx sis /\ eval_smem ctx sm <> None).
+Proof.
+  split; destruct 1; econstructor; simpl in *; eauto.
+  intuition eauto.
+Qed.
+
+Lemma ris_ok_set_mem ctx rm (ris: ristate):
+  (eval_smem ctx ris.(ris_smem) = None -> eval_smem ctx rm = None) ->
+  ris_ok ctx (rset_smem rm ris)
+  <-> (ris_ok ctx ris /\ eval_smem ctx rm <> None).
+Proof.
+   split; destruct 1; econstructor; simpl in *; eauto.
+Qed.
+
+Lemma rset_mem_refpreserv ctx rm sm ris sis:
+  (eval_smem ctx ris.(ris_smem) = None -> eval_smem ctx rm = None) ->
+  (forall m b ofs, eval_smem ctx sm = Some m -> Mem.valid_pointer m b ofs = Mem.valid_pointer (cm0 ctx) b ofs) ->
+  ris_refines ctx ris sis ->
+  (ris_ok ctx ris -> eval_smem ctx rm = eval_smem ctx sm) ->
+  ris_refines ctx (rset_smem rm ris) (set_smem sm sis).
+Proof.
+  destruct 3; intros.
+  econstructor; eauto.
+  + rewrite sis_ok_set_mem, ris_ok_set_mem; intuition congruence.
+  + rewrite ris_ok_set_mem; intuition eauto.
+  + rewrite ris_ok_set_mem; intuition eauto.
+Qed.
 
 (** TODO: could be useful ?
 Lemma seval_condition_valid_preserv ctx cond args sm b
@@ -268,4 +370,5 @@ Proof.
   eapply cond_valid_pointer_eq; intros.
   exploit VALID_PRESERV; eauto.
 Qed.
-*)
\ No newline at end of file
+*)
+