valid_pointer_preserv dans BTL_SEtheory => opportunites de *grosses* simplifications (à venir )

2 files changed, 42 insertions, 87 deletions

diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v
index 5098659d..40c28934 100644
--- a/scheduling/BTL_SEsimuref.v
+++ b/scheduling/BTL_SEsimuref.v
@@ -67,11 +67,9 @@ 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
+  REG_EQ: ris_ok ctx ris -> forall r, eval_sval ctx (ris_sreg_get ris r) = eval_sval ctx (si_sreg sis r)
 }.
-Local Hint Resolve OK_EQUIV MEM_EQ REG_EQ VALID_PRESERV: core.
+Local Hint Resolve OK_EQUIV MEM_EQ REG_EQ: core.
 Local Hint Constructors ris_refines: core.
 
 Record ris_simu ris1 ris2: Prop := {
@@ -218,11 +216,11 @@ Inductive rst_refines ctx: rstate -> sstate -> Prop :=
       (RIS: ris_refines ctx ris sis)
       (RFV: ris_ok ctx ris -> rfv_refines ctx rfv sfv)
       : rst_refines ctx (Rfinal ris rfv) (Sfinal sis sfv)
-  | Refcond cond rargs args sm rifso rifnot ifso ifnot
-      (RCOND: seval_condition ctx cond rargs Sinit = seval_condition ctx cond args sm)
-      (REFso: seval_condition ctx cond rargs Sinit = Some true -> rst_refines ctx rifso ifso)
-      (REFnot: seval_condition ctx cond rargs Sinit = Some false -> rst_refines ctx rifnot ifnot)
-      : rst_refines ctx (Rcond cond rargs rifso rifnot) (Scond cond args sm ifso ifnot)
+  | Refcond cond rargs args rifso rifnot ifso ifnot
+      (RCOND: seval_condition ctx cond rargs = seval_condition ctx cond args)
+      (REFso: seval_condition ctx cond rargs = Some true -> rst_refines ctx rifso ifso)
+      (REFnot: seval_condition ctx cond rargs = Some false -> rst_refines ctx rifnot ifnot)
+      : rst_refines ctx (Rcond cond rargs rifso rifnot) (Scond cond args ifso ifnot)
   | Refabort
       : rst_refines ctx Rabort Sabort
   .
@@ -245,7 +243,7 @@ Proof.
     intros ROK1.
     exploit ris_simu_ok_preserv; eauto.
   - (* cond_simu *)
-    destruct (seval_condition (bctx1 ctx) cond args sm) eqn: SCOND; try congruence.
+    destruct (seval_condition (bctx1 ctx) cond args) eqn: SCOND; try congruence.
     generalize RCOND0.
     erewrite <- seval_condition_preserved, RCOND by eauto.
     intros SCOND0; rewrite <- SCOND0 in RCOND0.
@@ -255,34 +253,6 @@ Proof.
     * exploit IHrst_simu2; eauto.
 Qed.
 
-
-(* TODO: useless ?
-Record routcome := rout {
-   r_sis: ristate;
-   r_sfv: sfval;
-}.
-
-Local Open Scope option_monad_scope.
-
-Fixpoint run_sem_irstate ctx (rst:rstate): option routcome :=
-  match rst with
-  | Rfinal ris sfv => Some (rout ris sfv)
-  | Rcond cond args ifso ifnot =>
-     SOME b <- seval_condition ctx cond args Sinit IN
-     run_sem_irstate ctx (if b then ifso else ifnot)
-  | Rabort => None
-  end.
-
-(* Non: pas assez de "matching" syntaxique entre rst et st pour rst_simu_correct
-Definition rst_refines ctx rst st:=
-    (run_sem_isstate ctx st=None <-> run_sem_irstate ctx rst=None)
- /\ (forall ris rfv sis sfv, run_sem_irstate ctx rst = Some (rout ris rfv) -> run_sem_isstate ctx st = Some (sout sis sfv) ->
-       (ris_refines ctx ris sis) /\ (ris_ok ctx ris -> rfv_refines ctx rfv sfv)).
-
-*)
-*)
-
-
 (** * Refinement of the symbolic execution *)
 
 Local Hint Constructors rfv_refines optrsv_refines rsvident_refines rsvident_refines: core.
@@ -341,7 +311,6 @@ Proof.
     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 :=
@@ -369,12 +338,11 @@ Qed.
 
 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 ->
   (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.
+  destruct 2; intros.
   econstructor; eauto.
   + rewrite ok_set_mem, ok_rset_mem; intuition congruence.
   + rewrite ok_rset_mem; intuition eauto.
@@ -393,9 +361,6 @@ Lemma rexec_store_correct ctx chunk addr args src ris 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.
 
@@ -448,7 +413,7 @@ 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.
+   rset_sreg dst (Sop op args) ris.
 
 Lemma rexec_op_correct ctx op args dst ris sis:
   ris_refines ctx ris sis ->
@@ -456,10 +421,6 @@ Lemma rexec_op_correct ctx op args dst ris 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 :=
@@ -474,24 +435,10 @@ Proof.
   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 = seval_condition ctx cond args Sinit.
-Proof.
-  unfold seval_condition; autodestruct; simpl; try congruence.
-  intros EVAL_LIST.
-  autodestruct; try congruence.
-  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.
+  seval_condition ctx cond (list_sval_inj (map ris args)) = seval_condition ctx cond (list_sval_inj (map sis args)).
 Proof.
   intros; unfold seval_condition.
   erewrite eval_list_sval_refpreserv; eauto.
@@ -654,7 +601,7 @@ Fixpoint history ctx ib sis (k:sistate -> option (list sistate)): option (list s
       history ctx ib1 sis (fun sis2 => history ctx ib2 sis2 k)
   | Bcond cond args ifso ifnot _ =>
       let args := list_sval_inj (List.map sis args) in
-      SOME b <- seval_condition ctx cond args sis.(si_smem) IN
+      SOME b <- seval_condition ctx cond args IN
       SOME oks <- history ctx (if b then ifso else ifnot) sis k IN 
       Some (sis::oks)
   end
@@ -846,7 +793,7 @@ Proof.
     exploit (OK2 sis); auto.
     assert (rOK: ris_ok ctx ris). { erewrite <- OK_EQUIV; eauto. }
     generalize COND.
-    erewrite seval_condition_valid_preserv, <- seval_condition_refpreserv; eauto.
+    erewrite <- seval_condition_refpreserv; eauto.
     intros;
     econstructor; try_simplify_someHyps.
 Qed.
diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
index 464bb0f0..97dc7fc8 100644
--- a/scheduling/BTL_SEtheory.v
+++ b/scheduling/BTL_SEtheory.v
@@ -29,7 +29,7 @@ Record iblock_exec_context := Bctx {
 Inductive sval :=
   | Sundef
   | Sinput (r: reg)
-  | Sop (op:operation) (lsv: list_sval)  (sm: smem)
+  | Sop (op:operation) (lsv: list_sval)
   | Sload (sm: smem) (trap: trapping_mode) (chunk:memory_chunk) (addr:addressing) (lsv:list_sval) 
 with list_sval := 
   | Snil
@@ -55,10 +55,9 @@ Fixpoint eval_sval ctx (sv: sval): option val :=
   match sv with
   | Sundef => Some Vundef
   | Sinput r => Some ((crs0 ctx)#r)
-  | Sop op l sm =>
+  | Sop op l =>
      SOME args <- eval_list_sval ctx l IN
-     SOME m <- eval_smem ctx sm IN
-     eval_operation (cge ctx) (csp ctx) op args m
+     eval_operation (cge ctx) (csp ctx) op args (cm0 ctx)
   | Sload sm trap chunk addr lsv =>
       match trap with
       | TRAP =>
@@ -98,6 +97,16 @@ with eval_smem ctx (sm: smem): option mem :=
      Mem.storev chunk m a sv
   end.
 
+
+Lemma valid_pointer_preserv ctx sm:
+  forall m b ofs, eval_smem ctx sm = Some m -> Mem.valid_pointer (cm0 ctx) b ofs = Mem.valid_pointer m b ofs.
+Proof.
+  induction sm; simpl; intros; try_simplify_someHyps; auto.
+  repeat autodestruct; intros; erewrite IHsm by reflexivity.
+  eapply Mem.storev_preserv_valid; eauto.
+Qed.
+Local Hint Resolve valid_pointer_preserv: core.
+
 Lemma eval_list_sval_inj ctx l (sreg: reg -> sval) rs: 
   (forall r : reg, eval_sval ctx (sreg r) = Some (rs # r)) ->
   eval_list_sval ctx (list_sval_inj (map sreg l)) = Some (rs ## l).
@@ -105,10 +114,9 @@ Proof.
   intros H; induction l as [|r l]; simpl; repeat autodestruct; auto.
 Qed.
 
-Definition seval_condition ctx (cond: condition) (lsv: list_sval) (sm: smem) : option bool :=
+Definition seval_condition ctx (cond: condition) (lsv: list_sval): option bool :=
   SOME args <- eval_list_sval ctx lsv IN
-  SOME m <- eval_smem ctx sm IN
-  eval_condition cond args m.
+  eval_condition cond args (cm0 ctx).
 
 
 (** * Auxiliary definitions on Builtins *)
@@ -565,7 +573,7 @@ Qed.
 
 Definition sexec_op op args dst sis: sistate :=
    let args := list_sval_inj (List.map sis.(si_sreg) args) in
-   set_sreg dst (Sop op args sis.(si_smem)) sis.
+   set_sreg dst (Sop op args) sis.
 
 Lemma sexec_op_correct ctx op args dst sis rs m v
  (EVAL: eval_operation (cge ctx) (csp ctx) op rs ## args m = Some v)
@@ -577,6 +585,7 @@ Proof.
     rewrite Regmap.gss; simpl; auto.
     erewrite eval_list_sval_inj; simpl; auto.
     try_simplify_someHyps.
+    intros; erewrite op_valid_pointer_eq; eauto.
   - intros; rewrite Regmap.gso; auto.
 Qed.
 
@@ -619,11 +628,11 @@ Qed.
 
 Lemma seval_condition_eq ctx cond args sis rs m
   (SIS : sem_sistate ctx sis rs m)
-  :seval_condition ctx cond (list_sval_inj (map (si_sreg sis) args)) (si_smem sis) = eval_condition cond rs ## args m.
+  :seval_condition ctx cond (list_sval_inj (map (si_sreg sis) args)) = eval_condition cond rs ## args m.
 Proof.
   destruct SIS as (PRE&MEM&REG); unfold seval_condition; simpl.
   erewrite eval_list_sval_inj; simpl; auto.
-  erewrite MEM; auto.
+  eapply cond_valid_pointer_eq; eauto.
 Qed.
 
 (** * Compute sistate associated to final values *)
@@ -698,7 +707,7 @@ Qed.
 (* symbolic state *)
 Inductive sstate :=
   | Sfinal (sis: sistate) (sfv: sfval)
-  | Scond (cond: condition) (args: list_sval) (sm: smem) (ifso ifnot: sstate)
+  | Scond (cond: condition) (args: list_sval) (ifso ifnot: sstate)
   | Sabort
  .
 
@@ -711,8 +720,8 @@ Record soutcome := sout {
 Fixpoint run_sem_isstate ctx (st:sstate): option soutcome :=
   match st with
   | Sfinal sis sfv => Some (sout sis sfv)
-  | Scond cond args sm ifso ifnot =>
-     SOME b <- seval_condition ctx cond args sm IN
+  | Scond cond args ifso ifnot =>
+     SOME b <- seval_condition ctx cond args IN
      run_sem_isstate ctx (if b then ifso else ifnot)
   | Sabort => None
   end.
@@ -723,10 +732,10 @@ Inductive sem_sstate ctx stk t s: sstate -> Prop :=
      (SIS: sem_sistate ctx sis (str_regs (cf ctx) sfv rs) m)
      (SFV: sem_sfval ctx stk sfv rs m t s)
      : sem_sstate ctx stk t s (Sfinal sis sfv)
-  | sem_Scond b cond args sm ifso ifnot
-     (SEVAL: seval_condition ctx cond args sm = Some b)
+  | sem_Scond b cond args ifso ifnot
+     (SEVAL: seval_condition ctx cond args = Some b)
      (SELECT: sem_sstate ctx stk t s (if b then ifso else ifnot))
-     : sem_sstate ctx stk t s (Scond cond args sm ifso ifnot)
+     : sem_sstate ctx stk t s (Scond cond args ifso ifnot)
   (* NB: Sabort: fails to produce a transition *) 
   .
 
@@ -784,7 +793,7 @@ Fixpoint sexec_rec f ib sis (k: sistate -> sstate): sstate :=
       let args := list_sval_inj (List.map sis.(si_sreg) args) in
       let ifso := sexec_rec f ifso sis k in
       let ifnot := sexec_rec f ifnot sis k in
-      Scond cond args sis.(si_smem) ifso ifnot
+      Scond cond args ifso ifnot
   end
   .
 
@@ -954,6 +963,7 @@ Proof.
   simpl. destruct SIS as (PRE&MEM&REG).
   erewrite eval_list_sval_inj; simpl; auto.
   try_simplify_someHyps.
+  intros; erewrite op_valid_pointer_eq; eauto.
 Qed.
 
 Lemma sexec_load_TRAP_abort ctx chunk addr args dst sis rs m
@@ -1177,7 +1187,6 @@ Proof.
   induction sv using sval_mut with (P0 := fun lsv => eval_list_sval (bctx1 ctx) lsv = eval_list_sval (bctx2 ctx) lsv)
                                    (P1 := fun sm => eval_smem (bctx1 ctx) sm = eval_smem (bctx2 ctx) 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.
@@ -1228,12 +1237,11 @@ Proof.
   reflexivity.
 Qed.
 
-Lemma seval_condition_preserved cond lsv sm:
-  seval_condition (bctx1 ctx) cond lsv sm = seval_condition (bctx2 ctx) cond lsv sm.
+Lemma seval_condition_preserved cond lsv:
+  seval_condition (bctx1 ctx) cond lsv = seval_condition (bctx2 ctx) cond lsv.
 Proof.
   unfold seval_condition.
   rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto.
-  rewrite smem_eval_preserved; auto.
 Qed.
 
 (* TODO: useless ?