red_PTree lemmas

2 files changed, 77 insertions, 10 deletions

diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v
index df8cc47f..b007a07e 100644
--- a/scheduling/BTL_SEimpl.v
+++ b/scheduling/BTL_SEimpl.v
@@ -258,21 +258,18 @@ Qed.
 Global Opaque hSstore.
 Local Hint Resolve hSstore_correct: wlp.
 
-Definition hrs_sreg_eval ctx hrs r := eval_sval ctx (ris_sreg_get hrs r).
-
 Definition hrs_sreg_get (hrs: ristate) r: ?? sval :=
    match PTree.get r hrs with
    | None => if ris_input_init hrs then hSinput r else hSundef
    | Some sv => RET sv
    end.
-Coercion hrs_sreg_get: ristate >-> Funclass.
 
 Lemma hrs_sreg_get_correct hrs r:
   WHEN hrs_sreg_get hrs r ~> sv THEN forall ctx (f: reg -> sval)
-  (RR: forall r, hrs_sreg_eval ctx hrs r = eval_sval ctx (f r)),
+  (RR: forall r, sval_refines ctx (hrs r) (f r)),
   sval_refines ctx sv (f r).
 Proof.
-  unfold hrs_sreg_eval, ris_sreg_get. wlp_simplify; rewrite <- RR; rewrite H; auto;
+  unfold ris_sreg_get; wlp_simplify; rewrite <- RR; rewrite H; auto;
   rewrite H0, H1; simpl; auto.
 Qed.
 Global Opaque hrs_sreg_get.
@@ -289,7 +286,7 @@ Fixpoint hlist_args (hrs: ristate) (l: list reg): ?? list_sval :=
 
 Lemma hlist_args_correct hrs l:
   WHEN hlist_args hrs l ~> lsv THEN forall ctx (f: reg -> sval)
-    (RR: forall r, hrs_sreg_eval ctx hrs r = eval_sval ctx (f r)),
+    (RR: forall r, sval_refines ctx (hrs r) (f r)),
     list_sval_refines ctx lsv (list_sval_inj (List.map f l)).
 Proof.
   induction l; wlp_simplify.
@@ -333,7 +330,7 @@ with fsval_list_proj sl: ?? list_sval :=
 
 Lemma fsval_proj_correct sv:
   WHEN fsval_proj sv ~> sv' THEN forall ctx,
-  eval_sval ctx sv = eval_sval ctx sv'.
+  sval_refines ctx sv sv'.
 Proof.
  induction sv using sval_mut 
  with (P0 := fun lsv => 
@@ -349,7 +346,7 @@ Local Hint Resolve fsval_proj_correct: wlp.
 
 Lemma fsval_list_proj_correct lsv:
   WHEN fsval_list_proj lsv ~> lsv' THEN forall ctx,
-  eval_list_sval ctx lsv = eval_list_sval ctx lsv'.
+  list_sval_refines ctx lsv lsv'.
 Proof.
   induction lsv; wlp_simplify.
   erewrite H0, H1; eauto.
@@ -495,13 +492,53 @@ Proof.
     wlp_simplify; inv REF. erewrite H0; eauto.
   - (* Rload *)
     destruct trap; wlp_simplify; inv REF.
-    + erewrite H0, H, MEM_EQ; eauto.
+    + erewrite H0; eauto.
+      erewrite H; [|eapply REG_EQ; eauto].
+      erewrite MEM_EQ; eauto.
       repeat simplify_SOME z.
       * destruct (Memory.Mem.loadv _ _ _); try congruence.
       * rewrite H1 in OK1; congruence.
     + erewrite H0; eauto.
 Qed.
 
+Definition red_PTree_set (r: reg) (sv: sval) (hrs: ristate): ristate :=
+  let sreg :=
+    match (ris_input_init hrs), sv with
+    | true, Sinput r' _ =>
+        if Pos.eq_dec r r' 
+        then PTree.remove r' hrs
+        else PTree.set r sv hrs
+    | false, Sundef _ =>
+        PTree.remove r hrs
+    | _, _ => PTree.set r sv hrs
+    end in
+  ris_sreg_set hrs sreg.
+
+Lemma red_PTree_set_correct (r r0:reg) sv hrs ctx:
+  sval_refines ctx ((red_PTree_set r sv hrs) r0) ((ris_sreg_set hrs (PTree.set r sv hrs)) r0).
+Proof.
+  unfold red_PTree_set, ris_sreg_set, ris_sreg_get; simpl.
+  destruct (ris_input_init hrs) eqn:Hinit, sv; simpl; auto.
+  1: destruct (Pos.eq_dec r r1); auto; subst;
+     rename r1 into r.
+  all: destruct (Pos.eq_dec r r0); auto;
+       [ subst; rewrite PTree.grs, PTree.gss; simpl; auto |
+         rewrite PTree.gro, PTree.gso; simpl; auto].
+Qed.
+
+Lemma red_PTree_set_refines (r r0:reg) ctx hrs st sv1 sv2:
+ ris_refines ctx hrs st ->
+ sval_refines ctx sv1 sv2 ->
+ ris_ok ctx hrs ->
+ sval_refines ctx ((red_PTree_set r sv1 hrs) r0) (if Pos.eq_dec r r0 then sv2 else si_sreg st r0).
+Proof.
+  intros REF SREF OK; rewrite red_PTree_set_correct.
+  unfold ris_sreg_set, ris_sreg_get.
+  destruct (Pos.eq_dec r r0).
+  - subst; simpl. rewrite PTree.gss; simpl; auto.
+  - inv REF; simpl. rewrite PTree.gso; simpl; eauto.
+Qed.
+
 Definition cbranch_expanse (prev: ristate) (cond: condition) (args: list reg): ?? (condition * list_sval) :=
   (* TODO gourdinl  
   match target_cbranch_expanse prev cond args with
@@ -549,7 +586,31 @@ Proof.
     intros; rewrite PTree.gempty; eauto.
 Qed.
 
-(*
+Fixpoint hrexec_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 _ => RET (k ris)
+  | Bop op args res _ =>
+      DO next <~ ris_sreg_set hrs 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
+
+  (* TODO to remove *)
+  | _ => RET (k ris)
+  end
+  .
+
 Definition hrexec f ib := hrexec_rec f ib hris_init (fun _ => Rabort).
 
 Definition hsexec (f: function) (pc:node): ?? ristate :=
diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v
index 66abe6e1..60c49e04 100644
--- a/scheduling/BTL_SEsimuref.v
+++ b/scheduling/BTL_SEsimuref.v
@@ -38,6 +38,12 @@ Definition ris_sreg_get (ris: ristate) r: sval :=
    end.
 Coercion ris_sreg_get: ristate >-> Funclass.
 
+Definition ris_sreg_set (ris: ristate) (sreg: PTree.t sval): ristate :=
+  {| ris_smem := ris_smem ris;
+     ris_input_init := ris_input_init ris;
+     ok_rsval := ok_rsval ris;
+     ris_sreg := sreg |}.
+
 Record ris_ok ctx (ris: ristate) : Prop := {
   OK_RMEM: (eval_smem ctx (ris_smem ris)) <> None;
   OK_RREG: forall sv, List.In sv (ok_rsval ris) -> eval_sval ctx sv <> None