avancement ref de l'exe symbolique

2 files changed, 306 insertions, 26 deletions

diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v
index 6d74ccf9..fdefe205 100644
--- a/scheduling/BTL_SEsimuref.v
+++ b/scheduling/BTL_SEsimuref.v
@@ -9,8 +9,6 @@
     - 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").
 
 *)
@@ -48,7 +46,7 @@ Record ristate :=
         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;
+    ok_rsval: list sval;
     ris_sreg:> PTree.t sval
   }.
 
@@ -61,7 +59,7 @@ 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
+   OK_RREG: forall sv, List.In sv (ok_rsval ris) -> eval_sval ctx sv <> None
 }.
 Local Hint Resolve OK_RMEM OK_RREG: core.
 Local Hint Constructors ris_ok: core.
@@ -77,7 +75,7 @@ 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_FAILS: forall sv, List.In sv ris2.(ok_rsval) -> List.In sv ris1.(ok_rsval);
   SIMU_MEM: ris1.(ris_smem) = ris2.(ris_smem);
   SIMU_REG: forall r, ris_sreg_get ris1 r = ris_sreg_get ris2 r
 }.
@@ -307,7 +305,7 @@ 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 _ |}.
+Definition ris_init: ristate := {| ris_smem:= Sinit; ris_input_init:=true; ok_rsval := nil; ris_sreg := PTree.empty _ |}.
 
 Lemma ris_init_correct ctx:
   ris_refines ctx ris_init sis_init.
@@ -323,11 +321,11 @@ 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);
+     ok_rsval := ris.(ok_rsval);
      ris_sreg:= ris.(ris_sreg)
   |}.
 
-Lemma sis_ok_set_mem ctx sm sis:
+Lemma ok_set_mem ctx sm sis:
   sis_ok ctx (set_smem sm sis)
   <-> (sis_ok ctx sis /\ eval_smem ctx sm <> None).
 Proof.
@@ -335,7 +333,7 @@ Proof.
   intuition eauto.
 Qed.
 
-Lemma ris_ok_set_mem ctx rm (ris: ristate):
+Lemma ok_rset_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).
@@ -343,7 +341,7 @@ Proof.
    split; destruct 1; econstructor; simpl in *; eauto.
 Qed.
 
-Lemma rset_mem_refpreserv ctx rm sm ris sis:
+Lemma rset_mem_correct 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 ->
@@ -352,23 +350,308 @@ Lemma rset_mem_refpreserv ctx rm sm ris 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.
+  + rewrite ok_set_mem, ok_rset_mem; intuition congruence.
+  + rewrite ok_rset_mem; intuition eauto.
+  + rewrite ok_rset_mem; intuition eauto.
 Qed.
 
-(** TODO: could be useful ?
-Lemma seval_condition_valid_preserv ctx cond args sm b
+Definition rexec_store chunk addr args src ris: ristate :=
+   let args := list_sval_inj (List.map (ris_sreg_get ris) args) in
+   let src := ris_sreg_get ris src in
+   let rm := Sstore ris.(ris_smem) chunk addr args src in
+   rset_smem rm ris.
+
+Lemma rexec_store_correct ctx chunk addr args src ris sis:
+  ris_refines ctx ris sis ->
+  ris_refines ctx (rexec_store chunk addr args src ris) (sexec_store chunk addr args src sis).
+Proof.
+  intros REF; eapply rset_mem_correct; simpl; eauto.
+  + intros X; rewrite X. repeat autodestruct; eauto.
+  + intros m b ofs; repeat autodestruct.
+    intros; erewrite <- Mem.storev_preserv_valid; [| eauto].
+    eauto.
+  + intros OK; erewrite eval_list_sval_refpreserv, MEM_EQ, REG_EQ; eauto.
+Qed.
+
+(* TODO: reintroduire le "root_apply" ? *)
+
+Definition rset_sreg r rsv (ris:ristate): ristate :=
+  {| ris_smem := ris.(ris_smem);
+     ris_input_init := ris.(ris_input_init);
+     ok_rsval := rsv::ris.(ok_rsval); (* TODO: A CHANGER ? *)
+     ris_sreg:= PTree.set r rsv ris.(ris_sreg) (* TODO: A CHANGER *)
+  |}.
+
+Lemma ok_set_sreg ctx r sv sis:
+  sis_ok ctx (set_sreg r sv sis)
+  <-> (sis_ok ctx sis /\ eval_sval ctx sv <> None).
+Proof.
+  unfold set_sreg; split.
+  + intros [(SVAL & PRE) SMEM SREG]; simpl in *; split.
+    - econstructor; eauto.
+      intros r0; generalize (SREG r0); destruct (Pos.eq_dec r r0); try congruence.
+    - generalize (SREG r); destruct (Pos.eq_dec r r); try congruence.
+  + intros ([PRE SMEM SREG] & SVAL).
+    econstructor; simpl; eauto.
+    intros r0;  destruct (Pos.eq_dec r r0); try congruence.
+Qed.
+
+Lemma ok_rset_sreg ctx r rsv ris:
+  ris_ok ctx (rset_sreg r rsv ris)
+  <-> (ris_ok ctx ris /\ eval_sval ctx rsv <> None).
+Proof.
+   split; destruct 1; econstructor; simpl in *; eauto.
+   intuition subst; eauto.
+   exploit OK_RREG; eauto.
+Qed.
+
+Lemma rset_reg_correct ctx r rsv sv ris sis:
+  ris_refines ctx ris sis ->
+  (ris_ok ctx ris -> eval_sval ctx rsv = eval_sval ctx sv) ->
+  ris_refines ctx (rset_sreg r rsv ris) (set_sreg r sv sis).
+Proof.
+  destruct 1; intros.
+  econstructor; eauto.
+  + rewrite ok_set_sreg, ok_rset_sreg; intuition congruence.
+  + rewrite ok_rset_sreg; intuition eauto.
+  + rewrite ok_rset_sreg. intros; unfold rset_sreg, set_sreg, ris_sreg_get; simpl. intuition eauto.
+    destruct (Pos.eq_dec _ _).
+    * subst; rewrite PTree.gss; eauto.
+    * rewrite PTree.gso; eauto.
+Qed.
+
+Definition rexec_op op args dst (ris:ristate): ristate :=
+   let args := list_sval_inj (List.map ris args) in
+   rset_sreg dst (Sop op args Sinit) ris.
+
+Lemma rexec_op_correct ctx op args dst ris sis:
+  ris_refines ctx ris sis ->
+  ris_refines ctx (rexec_op op args dst ris) (sexec_op op args dst sis).
+Proof.
+  intros REF; eapply rset_reg_correct; simpl; eauto.
+  intros OK; erewrite eval_list_sval_refpreserv; eauto.
+  do 2 autodestruct; auto.
+  + intros. erewrite <- op_valid_pointer_eq; eauto.
+  + erewrite <- MEM_EQ; eauto.
+    intros; exploit OK_RMEM; eauto. destruct 1.
+Qed.
+
+Definition rexec_load trap chunk addr args dst (ris:ristate): ristate :=
+   let args := list_sval_inj (List.map ris args) in
+   rset_sreg dst (Sload ris.(ris_smem) trap chunk addr args) ris.
+
+Lemma rexec_load_correct ctx trap chunk addr args dst ris sis:
+  ris_refines ctx ris sis ->
+  ris_refines ctx (rexec_load trap chunk addr args dst ris) (sexec_load trap chunk addr args dst sis).
+Proof.
+  intros REF; eapply rset_reg_correct; simpl; eauto.
+  intros OK; erewrite eval_list_sval_refpreserv, MEM_EQ; eauto.
+Qed.
+
+Lemma seval_condition_valid_preserv ctx cond args sm
+  (OK: eval_smem ctx sm <> None)
   (VALID_PRESERV: forall m b ofs, eval_smem ctx sm = Some m -> Mem.valid_pointer m b ofs = Mem.valid_pointer (cm0 ctx) b ofs)
-  :seval_condition ctx cond args sm = Some b ->
-   seval_condition ctx cond args Sinit = Some b.
+  :seval_condition ctx cond args sm = seval_condition ctx cond args Sinit.
 Proof.
   unfold seval_condition; autodestruct; simpl; try congruence.
   intros EVAL_LIST.
   autodestruct; try congruence.
-  intros MEM COND. rewrite <- COND.
+  intros.
   eapply cond_valid_pointer_eq; intros.
   exploit VALID_PRESERV; eauto.
 Qed.
-*)
+
+Lemma seval_condition_refpreserv ctx cond args ris sis:
+  ris_refines ctx ris sis ->
+  ris_ok ctx ris ->
+  seval_condition ctx cond (list_sval_inj (map ris args)) Sinit =
+  seval_condition ctx cond (list_sval_inj (map sis args)) Sinit.
+Proof.
+  intros; unfold seval_condition.
+  erewrite eval_list_sval_refpreserv; eauto.
+Qed.
+
+
+(* transfer *)
+
+Definition rseto_sreg r rsv (ris:ristate): ristate :=
+  {| ris_smem := ris.(ris_smem);
+     ris_input_init := ris.(ris_input_init);
+     ok_rsval := ris.(ok_rsval);
+     ris_sreg:= PTree.set r rsv ris.(ris_sreg) (* TODO: A CHANGER *)
+  |}.
+
+Lemma ok_rseto_sreg ctx r rsv ris:
+  ris_ok ctx (rseto_sreg r rsv ris)
+  <-> (ris_ok ctx ris).
+Proof.
+   split; destruct 1; econstructor; simpl in *; eauto.
+Qed.
+
+Lemma rseto_reg_correct ctx r rsv sv ris sis:
+  ris_refines ctx ris sis ->
+  (ris_ok ctx ris -> eval_sval ctx rsv <> None) ->
+  (ris_ok ctx ris -> eval_sval ctx rsv = eval_sval ctx sv) ->
+  ris_refines ctx (rseto_sreg r rsv ris) (set_sreg r sv sis).
+Proof.
+  destruct 1; intros.
+  econstructor; eauto.
+  + rewrite ok_set_sreg, ok_rseto_sreg; intuition congruence.
+  + rewrite ok_rseto_sreg; intuition eauto.
+  + rewrite ok_rseto_sreg. intros; unfold rseto_sreg, set_sreg, ris_sreg_get; simpl. intuition eauto.
+    destruct (Pos.eq_dec _ _).
+    * subst; rewrite PTree.gss; eauto.
+    * rewrite PTree.gso; eauto.
+Qed.
+
+Fixpoint transfer_ris (inputs: list reg) (ris:ristate): ristate :=
+  match inputs with
+  | nil =>   {| ris_smem := ris.(ris_smem);
+                ris_input_init := false;
+                ok_rsval := ris.(ok_rsval);
+                ris_sreg:= PTree.empty _
+             |}
+  | r::l => rseto_sreg r (ris_sreg_get ris r) (transfer_ris l ris)
+  end.
+
+Definition transfer_sis (inputs: list reg) (sis:sistate): sistate :=
+   {| si_pre := fun ctx => (sis.(si_pre) ctx /\ forall r, eval_sval ctx (sis.(si_sreg) r) <> None);
+      si_sreg := transfer_sreg inputs sis;
+      si_smem := sis.(si_smem) |}.
+
+Lemma ok_transfer_sis ctx inputs sis:
+  sis_ok ctx (transfer_sis inputs sis)
+  <-> (sis_ok ctx sis).
+Proof.
+  unfold transfer_sis. induction inputs as [|r l]; simpl.
+  + split; destruct 1; econstructor; simpl in *; intuition eauto. congruence.
+  + split.
+    * destruct 1; econstructor; simpl in *; intuition eauto.
+    * intros X; generalize X. rewrite <- IHl in X; clear IHl.
+      intros [PRE SMEM SREG].
+      econstructor; simpl; eauto.
+      intros r0;  destruct (Pos.eq_dec r r0); try congruence.
+      intros H; eapply OK_SREG; eauto.
+Qed.
+
+Lemma ok_transfer_ris ctx inputs ris:
+  ris_ok ctx (transfer_ris inputs ris)
+  <-> (ris_ok ctx ris).
+Proof.
+  induction inputs as [|r l]; simpl.
+  + split; destruct 1; econstructor; simpl in *; intuition eauto.
+  + rewrite ok_rseto_sreg. auto.
+Qed.
+
+Lemma transfer_ris_correct ctx inputs ris sis:
+  ris_refines ctx ris sis ->
+  ris_refines ctx (transfer_ris inputs ris) (transfer_sis inputs sis).
+Proof.
+  destruct 1; intros.
+  induction inputs as [|r l].
+  + econstructor; eauto.
+    * erewrite ok_transfer_sis, ok_transfer_ris; eauto.
+    * erewrite ok_transfer_ris; eauto.
+    * erewrite ok_transfer_ris; simpl; unfold ris_sreg_get; simpl; eauto.
+      intros; rewrite PTree.gempty. simpl; auto.
+  + econstructor; eauto.
+    * erewrite ok_transfer_sis, ok_transfer_ris; eauto.
+    * erewrite ok_transfer_ris; simpl.
+      intros; erewrite MEM_EQ. 2: eauto.
+      - unfold transfer_sis; simpl; eauto.
+      - rewrite ok_transfer_ris; simpl; eauto.
+    * erewrite ok_transfer_ris; simpl.
+      intros H r0.
+      erewrite REG_EQ. 2: eapply rseto_reg_correct; eauto.
+      - unfold set_sreg; simpl; auto.
+        destruct (Pos.eq_dec _ _); simpl; auto.
+      - intros. rewrite REG_EQ0; auto. apply OK_SREG; tauto.
+      - rewrite ok_rseto_sreg, ok_transfer_ris. auto.
+Qed.
+
+Definition alt_tr_sis := poly_tr (fun f tbl or => transfer_sis (Regset.elements (pre_inputs f tbl or))).
+
+Lemma tr_sis_alt_def f fi sis:
+  alt_tr_sis f fi sis = tr_sis f fi sis.
+Proof.
+  unfold tr_sis, str_inputs. destruct fi; simpl; auto.
+Qed.
+
+Definition tr_ris := poly_tr (fun f tbl or => transfer_ris (Regset.elements (pre_inputs f tbl or))).
+
+Local Hint Resolve transfer_ris_correct ok_transfer_ris: core.
+Local Opaque transfer_ris.
+
+Lemma ok_tr_ris ctx f fi ris:
+  ris_ok ctx (tr_ris f fi ris)
+  <-> (ris_ok ctx ris).
+Proof.
+   destruct fi; simpl; eauto.
+Qed.
+
+Lemma ok_tr_ris_imp ctx f fi ris:
+  ris_ok ctx (tr_ris f fi ris)
+  -> (ris_ok ctx ris).
+Proof.
+  rewrite ok_tr_ris; auto.
+Qed.
+
+
+Lemma tr_ris_correct ctx f fi ris sis:
+  ris_refines ctx ris sis ->
+  ris_refines ctx (tr_ris f fi ris) (tr_sis f fi sis).
+Proof.
+  intros REF. rewrite <- tr_sis_alt_def.
+  destruct fi; simpl; eauto.
+Qed.
+
+Fixpoint rexec_rec f ib ris (k: ristate -> rstate): rstate := 
+  match ib with
+  | BF fin _ => Rfinal (tr_ris f fin ris) (sexec_final_sfv fin ris)
+  (* basic instructions *)
+  | Bnop _ => k ris
+  | Bop op args res _ => k (rexec_op op args res ris)
+  | Bload TRAP chunk addr args dst _ => k (rexec_load TRAP chunk addr args dst ris)
+  | Bload NOTRAP chunk addr args dst _ => Rabort
+  | Bstore chunk addr args src _ => k (rexec_store chunk addr args src ris)
+ (* composed instructions *)
+  | Bseq ib1 ib2 =>
+      rexec_rec f ib1 ris (fun ris2 => rexec_rec f ib2 ris2 k)
+  | Bcond cond args ifso ifnot _ =>
+      let args := list_sval_inj (List.map ris args) in
+      let ifso := rexec_rec f ifso ris k in
+      let ifnot := rexec_rec f ifnot ris k in
+      Rcond cond args ifso ifnot
+  end
+  .
+
+Local Hint Constructors rst_refines: core.
+Local Hint Resolve ris_init_correct exec_final_refpreserv tr_ris_correct ok_tr_ris_imp 
+  rexec_op_correct rexec_load_correct rexec_store_correct: core.
+
+Lemma rexec_rec_correct ctx f ib: 
+  forall ris sis rk k
+  (CONT: forall rs ss, ris_refines ctx rs ss -> rst_refines ctx (rk rs) (k ss))
+  (REF: ris_refines ctx ris sis)
+  (*OK: ris_ok ctx ris*)
+  , rst_refines ctx (rexec_rec f ib ris rk) (sexec_rec f ib sis k).
+Proof.
+  induction ib; simpl; eauto.
+  - (* load *) autodestruct; eauto.
+  - intros.
+    econstructor; eauto.
+    symmetry.
+    erewrite seval_condition_valid_preserv; eauto.
+Admitted.
+
+Definition rexec f ib := rexec_rec f ib ris_init (fun _ => Rabort).
+
+Lemma rexec_correct ctx f ib:
+  rst_refines ctx (rexec f ib) (sexec f ib).
+Proof.
+  eapply rexec_rec_correct; eauto.
+  (* econstructor; simpl; auto. congruence. *)
+Qed.
+
+
 
diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
index 4b4571e4..464bb0f0 100644
--- a/scheduling/BTL_SEtheory.v
+++ b/scheduling/BTL_SEtheory.v
@@ -630,7 +630,7 @@ Qed.
 Fixpoint transfer_sreg (inputs: list reg) (sreg: reg -> sval): reg -> sval :=
   match inputs with
   | nil => fun r => Sundef 
-  | r1::l => fun r => if Pos.eq_dec r r1 then sreg r1 else transfer_sreg l sreg r
+  | r1::l => fun r => if Pos.eq_dec r1 r then sreg r1 else transfer_sreg l sreg r
   end.
 
 Definition str_inputs (f:function) (tbl: list exit) (or:option reg) := transfer_sreg (Regset.elements (pre_inputs f tbl or)).
@@ -655,15 +655,12 @@ Definition tr_sis f (fi: final) (sis: sistate) :=
      si_sreg := poly_tr str_inputs f fi sis.(si_sreg); 
      si_smem := sis.(si_smem) |}.
 
-Definition sreg_eval ctx (sis: sistate) (r: reg): option val :=
-  eval_sval ctx (sis.(si_sreg) r).
-
 Lemma tr_sis_regs_correct_aux ctx fin sis rs m:
   sem_sistate ctx sis rs m ->
-  (forall r, sreg_eval ctx (tr_sis (cf ctx) fin sis) r = Some (tr_regs (cf ctx) fin rs) # r).
+  (forall r, eval_sval ctx (tr_sis (cf ctx) fin sis r) = Some (tr_regs (cf ctx) fin rs) # r).
 Proof.
   Local Opaque str_inputs.
-  unfold sreg_eval; simpl. destruct 1 as (_ & _ & REG).
+  simpl. destruct 1 as (_ & _ & REG).
   destruct fin; simpl; eauto.
 Qed.
 
@@ -842,7 +839,7 @@ Lemma sem_sistate_tr_sis_determ ctx sis rs1 m1 fi rs2 m2:
 Proof.
   intros H1 H2.
   lapply (tr_sis_regs_correct_aux ctx fi sis rs1 m1); eauto.
-  unfold sreg_eval; intros X.
+  intros X.
   destruct H1 as (_&MEM1&REG1).
   destruct H2 as (_&MEM2&REG2); simpl in *.
   intuition try congruence.