path: root/scheduling/BTL_SEsimuref.v

(** Refinement of BTL_SEtheory data-structures
    in order to introduce (and prove correct) a lower-level specification of the simulation test.

    TODO: not yet with hash-consing ? Or "fake" hash-consing only ?

    Ceci est un "bac à sable".

    - On introduit une représentation plus concrète pour les types d'état symbolique [sistate] et [sstate].
    - Etant donné une spécification intuitive "*_simu" pour tester la simulation sur cette représentation des états symboliques,
      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 !

*)

Require Import Coqlib Maps Floats.
Require Import AST Integers Values Events Memory Globalenvs Smallstep.
Require Import Op Registers.
Require Import RTL BTL OptionMonad BTL_SEtheory.

(** * Preservation properties *)

(* TODO: inherited from RTLpath. Use simu_proof_context + bctx2 + bctx1 instead of all the hypotheses/variables below ? *)
 
Section SymbValPreserved.

Variable ge ge': BTL.genv.

Hypothesis symbols_preserved_BTL: forall s, Genv.find_symbol ge' s = Genv.find_symbol ge s.

Hypothesis senv_preserved_BTL: Senv.equiv ge ge'.

Lemma senv_find_symbol_preserved id:
  Senv.find_symbol ge id = Senv.find_symbol ge' id.
Proof.
  destruct senv_preserved_BTL as (A & B & C). congruence.
Qed.

Lemma senv_symbol_address_preserved id ofs:
  Senv.symbol_address ge id ofs = Senv.symbol_address ge' id ofs.
Proof.
  unfold Senv.symbol_address. rewrite senv_find_symbol_preserved.
  reflexivity.
Qed.

Variable stk stk': list stackframe.
Variable f f': function.
Variable sp: val.
Variable rs0: regset.
Variable m0: mem.

Lemma eval_sval_preserved sv:
  eval_sval (Bctx ge stk f sp rs0 m0) sv = eval_sval (Bctx ge' stk' f' sp rs0 m0) sv.
Proof.
  induction sv using sval_mut with (P0 := fun lsv => eval_list_sval (Bctx ge stk f sp rs0 m0) lsv = eval_list_sval (Bctx ge' stk' f' sp rs0 m0) lsv)
                                   (P1 := fun sm => eval_smem (Bctx ge stk f sp rs0 m0) sm = eval_smem (Bctx ge' stk' f' sp rs0 m0) 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.
    destruct (eval_addressing _ sp _ _); auto.
    rewrite IHsv; auto.
  + rewrite IHsv; clear IHsv. destruct (eval_sval _ _); auto.
    rewrite IHsv0; auto.
  + rewrite IHsv0; clear IHsv0. destruct (eval_list_sval _ _); auto.
    erewrite <- eval_addressing_preserved; eauto.
    destruct (eval_addressing _ sp _ _); auto.
    rewrite IHsv; clear IHsv. destruct (eval_smem _ _); auto.
    rewrite IHsv1; auto.
Qed.

Lemma seval_builtin_arg_preserved m: forall bs varg,
  seval_builtin_arg (Bctx ge stk f sp rs0 m0) m bs varg ->
  seval_builtin_arg (Bctx ge' stk' f' sp rs0 m0) m bs varg.
Proof.
  induction 1; simpl.
  all: try (constructor; auto).
  - rewrite <- eval_sval_preserved. assumption.
  - rewrite <- senv_symbol_address_preserved. assumption.
  - rewrite senv_symbol_address_preserved. eapply seval_BA_addrglobal.
Qed.

Lemma seval_builtin_args_preserved m lbs vargs:
  seval_builtin_args (Bctx ge stk f sp rs0 m0) m lbs vargs ->
  seval_builtin_args (Bctx ge' stk' f' sp rs0 m0) m lbs vargs.
Proof.
  induction 1; constructor; eauto.
  eapply seval_builtin_arg_preserved; auto.
Qed.

Lemma list_sval_eval_preserved lsv: 
  eval_list_sval (Bctx ge stk f sp rs0 m0) lsv = eval_list_sval (Bctx ge' stk' f' sp rs0 m0) lsv.
Proof.
  induction lsv; simpl; auto.
  rewrite eval_sval_preserved. destruct (eval_sval _ _); auto.
  rewrite IHlsv; auto.
Qed.

Lemma smem_eval_preserved sm: 
  eval_smem (Bctx ge stk f sp rs0 m0) sm = eval_smem (Bctx ge' stk' f' sp rs0 m0) sm.
Proof.
  induction sm; simpl; auto.
  rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto.
  erewrite <- eval_addressing_preserved; eauto.
  destruct (eval_addressing _ sp _ _); auto.
  rewrite IHsm; clear IHsm. destruct (eval_smem _ _); auto.
  rewrite eval_sval_preserved; auto.
Qed.

Lemma seval_condition_preserved cond lsv sm:
  seval_condition (Bctx ge stk f sp rs0 m0) cond lsv sm = seval_condition (Bctx ge' stk' f' sp rs0 m0) cond lsv sm.
Proof.
  unfold seval_condition.
  rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto.
  rewrite smem_eval_preserved; auto.
Qed.

End SymbValPreserved.

(** * ... *)

Record sis_ok ctx (sis: sistate): Prop := {
  OK_PRE: (sis.(si_pre) ctx);
  OK_SMEM: eval_smem ctx sis.(si_smem) <> None;
  OK_SREG: forall (r: reg), eval_sval ctx (si_sreg sis r) <> None
}.
Local Hint Resolve OK_PRE OK_SMEM OK_SREG: core.
Local Hint Constructors sis_ok: core.

Lemma sem_sok ctx sis rs m:
  sem_sistate ctx sis rs m ->  sis_ok ctx sis.
Proof.
  unfold sem_sistate;
  econstructor;
  intuition congruence.
Qed.

(* NB: refinement of (symbolic) internal state *)
Record ristate := 
  { 
    (** [ris_smem] represents the current smem symbolic evaluations.
        (we also recover the history of smem in ris_smem)  *)
    ris_smem: smem;
    (** For the values in registers:
        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;
    ris_sreg:> PTree.t sval
  }.

Definition ris_sreg_get (ris: ristate) r: sval :=
   match PTree.get r ris with
   | None => if ris_input_init ris then Sinput r else Sundef
   | Some sv => sv
   end.
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
}.
Local Hint Resolve OK_RMEM OK_RREG: core.
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
}.
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_MEM: ris1.(ris_smem) = ris2.(ris_smem);
  SIMU_REG: forall r, ris_sreg_get ris1 r = ris_sreg_get ris2 r
}.
Local Hint Resolve SIMU_FAILS SIMU_MEM SIMU_REG: core.
Local Hint Constructors ris_simu: core.
Local Hint Resolve sge_match: core.

Lemma ris_simu_ok_preserv f1 f2 ris1 ris2 (ctx:simu_proof_context):
  ris_simu ris1 ris2 -> ris_ok (bctx1 f1 ctx) ris1 -> ris_ok (bctx2 f2 ctx) ris2.
Proof.
  intros SIMU OK; econstructor; eauto.
  - erewrite <- SIMU_MEM; eauto.
    unfold bctx2; erewrite smem_eval_preserved; eauto.
  - unfold bctx2; intros; erewrite eval_sval_preserved; eauto.
Qed.

Lemma ris_simu_correct f1 f2 ris1 ris2 (ctx:simu_proof_context) sis1 sis2 rs m: 
  ris_simu ris1 ris2 ->
  ris_refines (bctx1 f1 ctx) ris1 sis1 ->
  ris_refines (bctx2 f2 ctx) ris2 sis2 ->
  sem_sistate (bctx1 f1 ctx) sis1 rs m ->
  sem_sistate (bctx2 f2 ctx) sis2 rs m.
Proof.
  intros RIS REF1 REF2 SEM.
  (* destruct REF1. destruct REF2. *)
  exploit sem_sok; eauto.
  erewrite OK_EQUIV; eauto.
  intros ROK1.
  exploit ris_simu_ok_preserv; eauto.
  intros ROK2. generalize ROK2; erewrite <- OK_EQUIV; eauto.
  intros SOK2.
  destruct SEM as (PRE & SMEM & SREG).
  unfold sem_sistate; intuition eauto.
  + erewrite <- MEM_EQ, <- SIMU_MEM; eauto.
    unfold bctx2; erewrite smem_eval_preserved; eauto.
    erewrite MEM_EQ; eauto.
  + erewrite <- REG_EQ, <- SIMU_REG; eauto.
    unfold bctx2; erewrite eval_sval_preserved; eauto.
    erewrite REG_EQ; eauto.
Qed.

Definition rfv_refines ctx (rfv sfv: sfval): Prop :=
  forall rs m t s, sem_sfval ctx rfv rs m t s <-> sem_sfval ctx sfv rs m t s.

Definition rfv_simu (rfv1 rfv2: sfval): Prop := rfv1 = rfv2.

Lemma rvf_simu_correct f1 f2 rfv1 rfv2 (ctx: simu_proof_context) sfv1 sfv2 rs m t s: 
  rfv_simu rfv1 rfv2 ->
  rfv_refines (bctx1 f1 ctx) rfv1 sfv1 ->
  rfv_refines (bctx2 f2 ctx) rfv2 sfv2 ->
  sem_sfval (bctx1 f1 ctx) sfv1 rs m t s ->
  sem_sfval (bctx2 f2 ctx) sfv2 rs m t s.
Proof.
  unfold rfv_simu, rfv_refines; intros X REF1 REF2 SEM. subst.
  rewrite <- REF2.
  assert (sem_sfval (bctx1 f1 ctx) rfv2 rs m t s). { rewrite REF1; auto. }
Admitted.

(* refinement of (symbolic) state *)
Inductive rstate :=
  | Rfinal (ris: ristate) (rfv: sfval)
  | Rcond (cond: condition) (rargs: list_sval) (rifso rifnot: rstate)
  | Rabort
  .

Inductive rst_simu: rstate -> rstate -> Prop :=
  | Rfinal_simu ris1 ris2 rfv1 rfv2:
      ris_simu ris1 ris2 ->
      rfv_simu rfv1 rfv2 ->
      rst_simu (Rfinal ris1 rfv1) (Rfinal ris2 rfv2)
  | Rcond_simu cond rargs rifso1 rifnot1 rifso2 rifnot2:
      rst_simu rifso1 rifso2 ->
      rst_simu rifnot1 rifnot2 ->
      rst_simu (Rcond cond rargs rifso1 rifnot1) (Rcond cond rargs rifso2 rifnot2)
  | Rabort_simu: rst_simu Rabort Rabort
(* TODO: extension à voir dans un second temps !
  | Rcond_skip cond rargs rifso1 rifnot1 rst:
      rst_simu rifso1 rst ->
      rst_simu rifnot1 rst ->
      rst_simu (Rcond cond rargs rifso1 rifnot1) rst
*)
  .

(* Comment prend on en compte le ris en cours d'execution ??? *)
Inductive rst_refines ctx: (* Prop -> *) rstate -> sstate -> Prop :=
  | refines_Sfinal ris sis rfv sfv (*ok: Prop*)
      (*OK: ris_ok ctx ris -> ok*)
      (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)
  | refines_Scond 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)
  | refines_Sabort
      : rst_refines ctx Rabort Sabort
  .

Lemma rst_simu_correct rst1 rst2:
   rst_simu rst1 rst2 ->
   forall f1 f2 ctx st1 st2 (*ok1 ok2*),
   rst_refines (*ok1*) (bctx1 f1 ctx) rst1 st1 ->
   rst_refines (*ok2*) (bctx2 f2 ctx) rst2 st2 ->
   (* ok1 -> ok2 -> *)
   sstate_simu f1 f2 ctx st1 st2.
Proof.
  induction 1; simpl; auto.
  - (* final *) intros f1 f2 ctx st1 st2 REF1 REF2 t s1 SEM1.
    inv REF1. inv REF2. inv SEM1.
    exploit sem_sok; eauto.
    rewrite OK_EQUIV; eauto.
    intros RIS_OK1.
    exploit (ris_simu_ok_preserv f1 f2); eauto.
    intros RIS_OK2. intuition.
    exploit ris_simu_correct; eauto.
    exploit rvf_simu_correct; eauto.
    simpl.
    eexists; split.
    + econstructor; eauto.
      simpl.
      admit. (* TODO: condition sur les tr_inputs: à ajouter plutôt dans le simu_proof_context ! *)
    + admit.
  - (* cond *) intros f1 f2 ctx st1 st2 REF1 REF2 t s1 SEM1.
    inv REF1. inv REF2. inv SEM1.
    destruct b; simpl.
    + assert (TODO1: rst_refines (bctx1 f1 ctx) rifso1 ifso). admit.
      assert (TODO2: rst_refines (bctx2 f2 ctx) rifso2 ifso0). admit.
      exploit IHrst_simu1; eauto.
      intros (s2 & X1 & X2).
      exists s2; split; eauto.
      econstructor; eauto.
      * assert (TODO3: seval_condition (bctx2 f2 ctx) cond args0 sm0 = Some true). admit.
        eauto.
      * simpl; eauto.
   + admit.
  - (* abort *) intros f1 f2 ctx st1 st2 REF1 REF2 t s1 SEM1.
    inv REF1. inv SEM1.
Admitted.