preuve de rexec_rec_correct via les notions history/histOK

1 files changed, 251 insertions, 41 deletions

diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v
index fdefe205..4f472e3e 100644
--- a/scheduling/BTL_SEsimuref.v
+++ b/scheduling/BTL_SEsimuref.v
@@ -212,18 +212,17 @@ Inductive rst_simu: rstate -> rstate -> Prop :=
   .
 
 (* Comment prend on en compte le ris en cours d'execution ??? *)
-Inductive rst_refines ctx: (* Prop -> *) rstate -> sstate -> Prop :=
-  | Reffinal ris sis rfv sfv (*ok: Prop*)
-      (*OK: ris_ok ctx ris -> ok*)
+
+Inductive rst_refines ctx: rstate -> sstate -> Prop :=
+  | Reffinal ris sis rfv sfv
       (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)
-  | Refcond 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)
+      : 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)
   | Refabort
       : rst_refines ctx Rabort Sabort
   .
@@ -232,10 +231,9 @@ Local Hint Resolve ris_simu_correct rvf_simu_correct: core.
 
 Lemma rst_simu_correct rst1 rst2:
    rst_simu rst1 rst2 ->
-   forall f1 f2 (ctx: simu_proof_context f1 f2) st1 st2 (*ok1 ok2*),
-   rst_refines (*ok1*) (bctx1 ctx) rst1 st1 ->
-   rst_refines (*ok2*) (bctx2 ctx) rst2 st2 ->
-   (* ok1 -> ok2 -> *)
+   forall f1 f2 (ctx: simu_proof_context f1 f2) st1 st2,
+   rst_refines (bctx1 ctx) rst1 st1 ->
+   rst_refines (bctx2 ctx) rst2 st2 ->
    sstate_simu ctx st1 st2.
 Proof.
   induction 1; simpl; intros f1 f2 ctx st1 st2 REF1 REF2 sis1 svf1 SEM1;
@@ -257,6 +255,34 @@ 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.
@@ -582,29 +608,197 @@ Definition tr_ris := poly_tr (fun f tbl or => transfer_ris (Regset.elements (pre
 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)
+Lemma ok_tr_ris ctx fi ris:
+  ris_ok ctx (tr_ris (cf ctx) 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)
+Lemma ok_tr_ris_imp ctx fi ris:
+  ris_ok ctx (tr_ris (cf ctx) fi ris)
   -> (ris_ok ctx ris).
 Proof.
   rewrite ok_tr_ris; auto.
 Qed.
 
 
-Lemma tr_ris_correct ctx f fi ris sis:
+Lemma tr_ris_correct ctx fi ris sis:
   ris_refines ctx ris sis ->
-  ris_refines ctx (tr_ris f fi ris) (tr_sis f fi sis).
+  ris_refines ctx (tr_ris (cf ctx) fi ris) (tr_sis (cf ctx) fi sis).
 Proof.
   intros REF. rewrite <- tr_sis_alt_def.
   destruct fi; simpl; eauto.
 Qed.
 
+(** TODO: CHANTIER **)
+
+Local Open Scope option_monad_scope.
+
+(* TODO: est-ce qu'un type inductif serait plus simple ? Pas sûr à cause des raisonnements par continuation ? 
+
+Un avantage du fixpoint, c'est que ça pourrait permettre de prouver les propriétés de history de façon plus incrémentale/modulaire.
+*)
+
+Fixpoint history ctx ib sis (k:sistate -> option (list sistate)): option (list sistate) := 
+  match ib with
+  | BF fin _ => Some (tr_sis (cf ctx) fin sis::nil)
+  (* basic instructions *)
+  | Bnop _ => k sis
+  | Bop op args res _ => k (sexec_op op args res sis)
+  | Bload TRAP chunk addr args dst _ => k (sexec_load TRAP chunk addr args dst sis)
+  | Bload NOTRAP chunk addr args dst _ => None
+  | Bstore chunk addr args src _ => k (sexec_store chunk addr args src sis)
+ (* composed instructions *)
+  | Bseq ib1 ib2 =>
+      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 oks <- history ctx (if b then ifso else ifnot) sis k IN 
+      Some (sis::oks)
+  end
+  .
+
+Inductive nested ctx: sistate -> list sistate -> Type :=
+  ns_nil sis: nested ctx sis nil
+| ns_cons sis1 sis2 lsis:
+   (sis_ok ctx sis2 -> sis_ok ctx sis1) ->
+   nested ctx sis2 lsis ->
+   nested ctx sis1 (sis2::lsis)
+   .
+Local Hint Constructors nested: core.
+
+(* TODO: A REVOIR !
+Lemma nested_monotonic ok1 oks: 
+  nested ok1 oks ->
+  forall (ok2: Prop), (ok1 -> ok2) ->
+  nested ok2 oks.
+Proof.
+  induction 1; simpl; eauto.
+Qed.
+
+Lemma history_nested ctx ib:
+  forall k
+  (CONT: forall sis hsis, (k sis) = Some hsis -> nested (sis_ok ctx sis) hsis)
+  sis hsis 
+  (RET: history ctx ib sis k = Some hsis),
+  nested (sis_ok ctx sis) hsis.
+Proof.
+  induction ib; simpl; intros; try_simplify_someHyps.
+  + econstructor; eauto. admit.
+  + intros; eapply nested_monotonic; eauto.
+    admit.
+  + destruct trap; try_simplify_someHyps.
+    intros;  eapply nested_monotonic; eauto.
+    admit.
+  + intros; eapply nested_monotonic; eauto.
+    admit.
+  + intros; eapply nested_monotonic. 2: eauto.
+    eapply IHib1. 2: eauto.
+    simpl; intros; eapply nested_monotonic; eauto.
+  + repeat autodestruct; intros; try_simplify_someHyps.
+Admitted.
+
+Inductive is_last {A} (x:A): list A -> Prop :=
+   is_last_refl: is_last x (x::nil)
+ | is_last_cons a l (NXT: is_last x l): is_last x (a::l)
+ .
+
+Lemma nested_last_1 P oks (LAST: is_last P oks): forall ok
+  (N: nested ok oks),
+  P -> ok.
+Proof.
+  induction LAST; simpl; intros.
+  + inv N; auto.
+  + inv N; eauto.
+    eapply IHLAST; eauto.
+    eapply nested_monotonic; eauto.
+Qed.
+
+Lemma nested_last_all P oks (LAST: is_last P oks): forall ok
+  (N: nested ok oks),
+  P -> forall Q, List.In Q oks -> Q.
+Proof.
+  induction LAST; simpl; intros.
+  + intuition subst. inv N; auto.
+  + inv N.
+    intuition subst.
+    * eapply nested_last_1; eauto.
+    * eapply IHLAST; eauto.
+Qed.
+Local Hint Constructors is_last: core.
+
+Lemma run_sem_isstate_okcnd_last ctx ib: forall ks kok
+  (CONT: forall sis1 sis2 sfv, run_sem_isstate ctx (ks sis1) = Some (sout sis2 sfv) -> exists hsis, kok sis1 = Some hsis /\ is_last (sis_ok ctx sis2) hsis)
+  sis1 sis2 sfv
+  (RUN: run_sem_isstate ctx (sexec_rec (cf ctx) ib sis1 ks) = Some (sout sis2 sfv))
+  ,exists hsis, history ctx ib sis1 kok = Some hsis /\ is_last (sis_ok ctx sis2) hsis.
+Proof.
+  induction ib; simpl; intros; try_simplify_someHyps.
+  + destruct trap; simpl; try_simplify_someHyps.
+  + (* seq *)
+    intros; eapply IHib1; eauto.
+    simpl; intros; eapply IHib2; eauto.
+  + (* cond *)
+    autodestruct. intros; destruct b.
+    - exploit IHib1; eauto.
+      intros (hsis & OK & LAST).
+      rewrite OK; simpl.
+      eexists; split; eauto.
+    - exploit IHib2; eauto.
+      intros (hsis & OK & LAST).
+      rewrite OK; simpl.
+      eexists; split; eauto.
+Qed.
+*)
+
+Inductive histOK ctx: list sistate -> sstate -> Prop :=
+  | Final_ok sis sfv
+      : histOK ctx (sis::nil) (Sfinal sis sfv)
+  | Cond_ok b sis hsis cond args ifso ifnot
+      (OK: (sis_ok ctx sis))
+      (EVAL: seval_condition ctx cond args sis.(si_smem) = Some b)
+      (REC: histOK ctx hsis (if b then ifso else ifnot))
+      : histOK ctx (sis::hsis) (Scond cond args sis.(si_smem) ifso ifnot)
+  .
+Local Hint Constructors histOK: core.
+
+(* TODO: pour prouver ça, faut généraliser avec nested + is_last en hypothèse ?  
+
+Lemma run_sem_isstate_okentails ctx ib: forall ks kok
+  (CONT: forall sis st, ks sis = st -> run_sem_isstate ctx st <> None -> exists hsis, kok sis = Some hsis /\ histOK ctx hsis st)
+  sis st
+  (EXEC: sexec_rec (cf ctx) ib sis ks = st)
+  (OK: run_sem_isstate ctx st <> None)
+  ,exists hsis, history ctx ib sis kok = Some hsis /\ histOK ctx hsis st.
+Proof.
+  induction ib; simpl; intros; subst; try_simplify_someHyps.
+  + destruct trap; simpl in *; try_simplify_someHyps. congruence.
+  + (* seq *)
+    intros; eapply IHib1; eauto.
+    simpl; intros; eapply IHib2; eauto.
+  + (* cond *)
+    simpl in *.
+    autodestruct.
+    intros; destruct b.
+    - exploit IHib1; eauto.
+      intros (hsis & OK1 & X).
+      rewrite OK1; simpl.
+      eexists; split; eauto.
+      econstructor; eauto.
+      admit.
+    - exploit IHib2; eauto.
+      intros (hsis & OK2 & LAST).
+      rewrite OK2; simpl.
+      eexists; split; eauto.
+      econstructor; eauto.
+      admit.
+Admitted.
+*)
+
+(** RAFFINEMENT EXEC SYMBOLIQUE **)
+
 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)
@@ -625,33 +819,49 @@ Fixpoint rexec_rec f ib ris (k: ristate -> rstate): rstate :=
   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))
+Local Hint Constructors rst_refines: core.
+
+Lemma rexec_rec_correct ctx ib: 
+  forall kok rk k
+  (CONT: forall ris sis hsis st, ris_refines ctx ris sis -> k sis = st -> kok sis = Some hsis -> histOK ctx hsis st -> rst_refines ctx (rk ris) (k sis))
+  ris sis hsis st
   (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.
+  (EXEC: sexec_rec (cf ctx) ib sis k = st)
+  (OK1: history ctx ib sis kok = Some hsis)
+  (OK2: histOK ctx hsis st)
+  , rst_refines ctx (rexec_rec (cf ctx) ib ris rk) st.
+Proof.
+  induction ib; simpl; try (intros; subst; eauto; fail).
+  - (* load *) intros; subst; autodestruct; simpl in *; subst; eauto.
+  - (* seq *)
+    intros; subst.
+    eapply IHib1; eauto.
+    simpl. intros; subst. eapply IHib2; eauto.
+  - (* cond *)
+    intros rk k kok CONT ris sis hsis st REF EXEC. subst.
+    autodestruct.
+    intros EQb.
+    destruct (history _ _ _ _) eqn: EQl;
+    intros; try_simplify_someHyps; intros.
+    inv OK2.
+    assert (rOK: ris_ok ctx ris). { erewrite <- OK_EQUIV; eauto. }
+    try_simplify_someHyps; intros.
+    generalize EVAL.
+    erewrite seval_condition_valid_preserv, <- seval_condition_refpreserv; eauto.
+    intros;
+    econstructor; try_simplify_someHyps.
+Qed.
 
 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).
+Lemma rexec_correct ctx ib hsis:
+  history ctx ib sis_init (fun _ : sistate => None) = Some hsis ->
+  histOK ctx hsis (sexec_rec (cf ctx) ib sis_init (fun _ : sistate => Sabort)) ->
+  rst_refines ctx (rexec (cf ctx) ib) (sexec (cf ctx) ib).
 Proof.
-  eapply rexec_rec_correct; eauto.
-  (* econstructor; simpl; auto. congruence. *)
+  unfold sexec; intros; eapply rexec_rec_correct; eauto.
+  simpl; congruence.
 Qed.
-
-
-