remove history

1 files changed, 111 insertions, 188 deletions

diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v
index 98587b66..2ca36b11 100644
--- a/scheduling/BTL_SEsimuref.v
+++ b/scheduling/BTL_SEsimuref.v
@@ -8,9 +8,6 @@
       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.
-    - introduire "fake" hash-consed values (à renommer en "refined" plutôt que "fake").
-
 *)
 
 Require Import Coqlib Maps Floats.
@@ -18,6 +15,9 @@ Require Import AST Integers Values Events Memory Globalenvs Smallstep.
 Require Import Op Registers.
 Require Import RTL BTL OptionMonad BTL_SEtheory.
 
+
+Local Open Scope option_monad_scope.
+
 (** * Refinement of data-structures and of the specification of the simulation test *)
 
 Local Hint Resolve OK_PRE OK_SMEM OK_SREG: core.
@@ -45,12 +45,20 @@ Definition ris_sreg_get (ris: ristate) r: sval :=
 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 (ok_rsval ris) -> eval_sval ctx sv <> None
+  OK_RMEM: (eval_smem ctx (ris_smem ris)) <> 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.
 
+(* TODO: Is it useful ?
+Definition ris_abs (ris: ristate) : sistate := {|
+  si_pre := fun ctx => ris_ok ctx ris;
+  si_sreg := ris_sreg_get ris;
+  si_smem := ris.(ris_smem)
+|}.
+*)
+
 Record ris_refines ctx (ris: ristate) (sis: sistate): Prop := {
   OK_EQUIV: si_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);
@@ -178,6 +186,21 @@ Inductive rstate :=
   | Rabort
   .
 
+
+Record routcome := rout {
+  _ris: ristate;
+  _rfv: sfval;
+}.
+
+Fixpoint get_routcome ctx (rst:rstate): option routcome :=
+  match rst with
+  | Rfinal ris rfv => Some (rout ris rfv)
+  | Rcond cond args ifso ifnot =>
+     SOME b <- seval_condition ctx cond args IN
+     get_routcome ctx (if b then ifso else ifnot)
+  | Rabort => None
+  end.
+
 Inductive rst_simu: rstate -> rstate -> Prop :=
   | Rfinal_simu ris1 ris2 rfv1 rfv2
       (RIS: ris_simu ris1 ris2)
@@ -196,6 +219,19 @@ Inductive rst_simu: rstate -> rstate -> Prop :=
 *)
   .
 
+Lemma rst_simu_lroutcome rst1 rst2:
+   rst_simu rst1 rst2 ->
+   forall f1 f2 (ctx: simu_proof_context f1 f2) ris1 rfv1,
+   get_routcome (bctx1 ctx) rst1 = Some (rout ris1 rfv1) ->
+   exists ris2 rfv2, get_routcome (bctx2 ctx) rst2 = Some (rout ris2 rfv2) /\ ris_simu ris1 ris2 /\ rfv_simu rfv1 rfv2.
+Proof.
+  induction 1; simpl; intros f1 f2 ctx lris1 lrfv1 ROUT; try_simplify_someHyps.
+  erewrite <- seval_condition_preserved.
+  autodestruct.
+  destruct b; simpl; auto.
+Qed.
+
+
 (* Comment prend on en compte le ris en cours d'execution ??? *)
 
 Inductive rst_refines ctx: rstate -> sstate -> Prop :=
@@ -212,6 +248,30 @@ Inductive rst_refines ctx: rstate -> sstate -> Prop :=
       : rst_refines ctx Rabort Sabort
   .
 
+Lemma rst_refines_outcome_up ctx rst st:
+   rst_refines ctx rst st ->
+   forall ris rfv,
+   get_routcome ctx rst = Some (rout ris rfv) ->
+   exists sis sfv, get_soutcome ctx st = Some (sout sis sfv) /\ ris_refines ctx ris sis /\ (ris_ok ctx ris -> rfv_refines ctx rfv sfv).
+Proof.
+  induction 1; simpl; intros lris lrfv ROUT; try_simplify_someHyps.
+  rewrite RCOND.
+  autodestruct.
+  destruct b; simpl; auto.
+Qed.
+
+Lemma rst_refines_outcome_down ctx rst st:
+   rst_refines ctx rst st ->
+   forall sis sfv,
+   get_soutcome ctx st = Some (sout sis sfv) ->
+   exists ris rfv, get_routcome ctx rst = Some (rout ris rfv) /\ ris_refines ctx ris sis /\ (ris_ok ctx ris -> rfv_refines ctx rfv sfv).
+Proof.
+  induction 1; simpl; intros lris lrfv ROUT; try_simplify_someHyps.
+  rewrite RCOND.
+  autodestruct.
+  destruct b; simpl; auto.
+Qed.
+
 Local Hint Resolve ris_simu_correct rvf_simu_correct: core.
 
 Lemma rst_simu_correct rst1 rst2:
@@ -248,7 +308,7 @@ 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)).
+  eval_list_sval ctx (list_sval_inj (map (si_sreg sis) args)).
 Proof.
   intros REF OK.
   induction args; simpl; eauto.
@@ -565,168 +625,20 @@ Proof.
   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 IN
-      SOME oks <- history ctx (if b then ifso else ifnot) sis k IN 
-      Some (sis::oks)
-  end
-  .
-
-Inductive nested: Prop -> list Prop -> Type :=
-  ns_nil ok: nested ok nil
-| ns_cons (ok1 ok2: Prop) loks:
-   (ok2 -> ok1) ->
-   nested ok2 loks ->
-   nested ok1 (ok2::loks)
-   .
-Local Hint Constructors nested: core.
-
-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 (si_ok ctx sis) (List.map (si_ok ctx) hsis))
-  sis hsis 
-  (RET: history ctx ib sis k = Some hsis),
-  nested (si_ok ctx sis) (List.map (si_ok ctx) 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.
+Lemma si_ok_tr_sis_down ctx fi sis: si_ok ctx (tr_sis (cf ctx) fi sis) -> si_ok ctx sis.
 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 si_ok_op_down ctx op args dest sis: si_ok ctx (sexec_op op args dest sis) -> si_ok ctx sis.
+Admitted.
 
-Lemma is_last_map {A B} (f: A -> B) x l: is_last x l -> is_last (f x) (List.map f l).
-Proof.
-  induction 1; simpl; eauto.
-Qed.
+Lemma si_ok_trap_down ctx chunk addr args dest sis: si_ok ctx (sexec_load TRAP chunk addr args dest sis) -> si_ok ctx sis.
+Admitted.
 
-Lemma run_sem_is_last ctx ib: forall ks kok
-  (CONT: forall sis1 sis2 sfv hsis, run_sem_isstate ctx (ks sis1) = Some (sout sis2 sfv) -> kok sis1 = Some hsis -> is_last sis2 hsis)
-  sis1 sis2 sfv hsis
-  (RUN: run_sem_isstate ctx (sexec_rec (cf ctx) ib sis1 ks) = Some (sout sis2 sfv))
-  (HIST: history ctx ib sis1 kok = Some hsis)
-  ,is_last sis2 hsis.
-Proof.
-  induction ib; simpl; intros; try_simplify_someHyps.
-  + destruct trap; simpl; try_simplify_someHyps.
-  + (* seq *)
-    intros; eapply IHib1. 2-3: eauto.
-    simpl; intros; eapply IHib2; eauto.
-  + (* cond *)
-    autodestruct.
-    destruct (history _ _ _ _) eqn: HIST; try_simplify_someHyps.
-    intros; econstructor.
-    destruct b; eauto.
-Qed.
-
-Lemma run_sem_history_None ctx ib: forall ks kok
-  (CONT: forall sis, kok sis = None -> run_sem_isstate ctx (ks sis) = None)
-  sis
-  (HIST: history ctx ib sis kok = None)
-  ,run_sem_isstate ctx (sexec_rec (cf ctx) ib sis ks) = None.
-Proof.
-  induction ib; simpl; intros; try_simplify_someHyps.
-  + destruct trap; simpl in *; try_simplify_someHyps.
-  + (* seq *)
-    intros; eapply IHib1. 2: eauto.
-    simpl; intros; eapply IHib2; eauto.
-  + (* cond *)
-    simpl in *.
-    autodestruct.
-    destruct (history _ _ _ _) eqn: X; try congruence.
-    intros; destruct b; eauto.
-Qed.
+Lemma si_ok_store_down ctx chunk addr args src sis: si_ok ctx (sexec_store chunk addr args src sis) -> si_ok ctx sis.
+Admitted.
 
-(* TODO:  bof, "historys_spec" un peu lourd pour l'usage qui en est fait ? *)
-Inductive history_spec ctx sis1 sis2: option (list sistate) -> Prop :=
-  history_exist hsis 
-    (NESTED: nested (si_ok ctx sis1) (List.map (si_ok ctx) hsis))
-    (LAST: is_last sis2 hsis)
-    : history_spec ctx sis1 sis2 (Some hsis)
-  .
-Local Hint Resolve history_exist: core.
-
-Lemma run_sem_history ctx ib sis svf
-  (OK: run_sem_isstate ctx (sexec (cf ctx) ib) = Some (sout sis svf))
-  :history_spec ctx sis_init sis (history ctx ib sis_init (fun _ => None)).
-Proof.
-  unfold sexec in *; destruct (history _ _ _ _) eqn: HIST.
-  + econstructor.
-    * eapply history_nested; eauto.
-      simpl; try congruence.
-    * eapply run_sem_is_last. 2-3: eauto.
-      simpl; try congruence.
-  + exploit (run_sem_history_None ctx ib (fun _ => Sabort)); eauto.
-    congruence.
-Qed.
+(* TODO: a revoir: ce n'est pas une bonne idee de mettre ça dans core => ça fait ramer "eauto" !!! *)
+Local Hint Resolve si_ok_tr_sis_down si_ok_op_down si_ok_trap_down si_ok_store_down: core.
 
 (** RAFFINEMENT EXEC SYMBOLIQUE **)
 
@@ -755,50 +667,61 @@ Local Hint Resolve ris_init_correct exec_final_refpreserv tr_ris_correct ok_tr_r
 
 Local Hint Constructors rst_refines: core.
 
+Lemma sexec_rec_down ctx ib: 
+  forall k
+  (CONT: forall sis lsis sfv, get_soutcome ctx (k sis) = Some (sout lsis sfv) ->  si_ok ctx lsis -> si_ok ctx sis)
+  sis lsis sfv
+  (SOUT: get_soutcome ctx (sexec_rec (cf ctx) ib sis k) = Some (sout lsis sfv))
+  (OK: si_ok ctx lsis)
+  ,si_ok ctx sis.
+Proof.
+  induction ib; simpl; try (autodestruct; simpl).
+  1-6: try_simplify_someHyps.
+  - intros. eapply IHib1. 2-3: eauto.
+    eapply IHib2; eauto.
+  - intros k CONT sis lsis sfv.
+    do 2 autodestruct.
+    + intros; eapply IHib1; eauto.
+    + intros; eapply IHib2; eauto.
+Qed.
+
 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 -> (forall sis, List.In sis hsis -> si_ok ctx sis) -> rst_refines ctx (rk ris) (k sis))
-  ris sis hsis st
+  forall rk k
+  (CONTh: forall sis lsis sfv, get_soutcome ctx (k sis) = Some (sout lsis sfv) ->  si_ok ctx lsis -> si_ok ctx sis)
+  (CONT: forall ris sis lsis sfv st, ris_refines ctx ris sis -> k sis = st -> get_soutcome ctx (k sis) = Some (sout lsis sfv) -> si_ok ctx lsis -> rst_refines ctx (rk ris) (k sis))
+  ris sis lsis sfv st
   (REF: ris_refines ctx ris sis)
   (EXEC: sexec_rec (cf ctx) ib sis k = st)
-  (OK1: history ctx ib sis kok = Some hsis)
-  (OK2: forall sis, List.In sis hsis -> si_ok ctx sis)
+  (SOUT: get_soutcome ctx st = Some (sout lsis sfv))
+  (OK: si_ok ctx lsis)
   , 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.
+    eapply IHib1. 3-6: eauto.
+    + simpl. eapply sexec_rec_down; eauto.
+    + intros; subst. eapply IHib2; eauto.
   - (* cond *)
-    intros rk k kok CONT ris sis hsis st REF EXEC. subst.
+    intros rk k CONTh CONT ris sis lsis sfv st REF EXEC OUT OK. subst.
+    assert (rOK: ris_ok ctx ris). {
+      erewrite <- OK_EQUIV. 2: eauto.
+      eapply sexec_rec_down with (ib:=(Bcond cond args ib1 ib2 iinfo)); simpl; eauto.
+    }
+    generalize OUT; clear OUT; simpl.
     autodestruct.
-    intros COND.
-    destruct (history _ _ _ _) eqn: EQl;
-    intros; try_simplify_someHyps; intros.
-    exploit (OK2 sis); auto.
-    assert (rOK: ris_ok ctx ris). { erewrite <- OK_EQUIV; eauto. }
-    generalize COND.
+    intros COND; generalize COND.
     erewrite <- 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 ib sis sfv:
-  run_sem_isstate ctx (sexec (cf ctx) ib) = Some (sout sis sfv) ->
+  get_soutcome ctx (sexec (cf ctx) ib) = Some (sout sis sfv) ->
   (si_ok ctx sis) ->
   rst_refines ctx (rexec (cf ctx) ib) (sexec (cf ctx) ib).
 Proof.
-  intros RUN SIS; exploit run_sem_history; eauto.
-  intros HIST; inv HIST.
-  unfold sexec; intros; eapply rexec_rec_correct; eauto.
-  + simpl; intros; subst; eauto.
-  + intros; eapply nested_last_all.
-    - eapply is_last_map; eauto.
-    - eapply NESTED.
-    - eapply SIS.
-    - eapply List.in_map; eauto.
+  unfold sexec; intros; eapply rexec_rec_correct; eauto; simpl; congruence.
 Qed.