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

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.


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.
Local Hint Constructors si_ok: core.

(* 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
        See [ris_sreg_get] below.
     *)
    ris_input_init: bool;
    ok_rsval: list sval;
    ris_sreg:> PTree.t sval
  }.

Definition ris_sreg_get (ris: ristate) r: sval :=
   match PTree.get r (ris_sreg ris) with
   | None => if ris_input_init ris then fSinput r else fSundef
   | Some sv => sv
   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 |}.

Lemma ris_sreg_set_access (ris: ristate) (sreg: PTree.t sval) r smem rsval:
  {| ris_smem := smem;
     ris_input_init := ris_input_init ris;
     ok_rsval := rsval;
     ris_sreg := sreg |} r =
  ris_sreg_set ris sreg r.
Proof.
  unfold ris_sreg_set, ris_sreg_get; simpl.
  reflexivity.
Qed.

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
}.
Local Hint Resolve OK_RMEM OK_RREG: core.
Local Hint Constructors ris_ok: core.

(**
   NOTE that this refinement relation *cannot* be decomposed into a abstraction function of type 
   ristate -> sistate & an equivalence relation on istate.

   Indeed, any [sis] satisfies [forall ctx r, si_ok ctx sis -> eval_sval ctx (sis r) <> None].
   whereas this is generally not true for [ris] that [forall ctx r, ris_ok ctx ris -> eval_sval ctx (ris r) <> None], 
   except when, precisely, [ris_refines ris sis].

   An alternative design enabling to define ris_refines as the composition of an equivalence on sistate 
   and a abstraction function would consist in constraining sistate with an additional [wf] field:

   Record sistate := 
    { si_pre: iblock_exec_context -> Prop; 
      si_sreg:> reg -> sval;
      si_smem: smem;
      si_wf: forall ctx, si_pre ctx -> si_smem <> None /\ forall r, si_sreg r <> None 
   }.

  Such a constraint should also appear in [ristate]. This is not clear whether this alternative design 
  would be really simpler.

*)
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);
  REG_EQ: ris_ok ctx ris -> forall r, eval_sval ctx (ris r) = eval_sval ctx (sis r)
}.
Local Hint Resolve OK_EQUIV MEM_EQ REG_EQ: core.
Local Hint Constructors ris_refines: core.

Record ris_simu ris1 ris2: Prop := {
  SIMU_FAILS: forall sv, List.In sv ris2.(ok_rsval) -> List.In sv ris1.(ok_rsval);
  SIMU_MEM: ris1.(ris_smem) = ris2.(ris_smem);
  SIMU_REG: forall r, ris1 r = 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 f1 f2):
  ris_simu ris1 ris2 -> ris_ok (bctx1 ctx) ris1 -> ris_ok (bctx2 ctx) ris2.
Proof.
  intros SIMU OK; econstructor; eauto.
  - erewrite <- SIMU_MEM; eauto.
    erewrite <- smem_eval_preserved; eauto.
  - intros; erewrite <- eval_sval_preserved; eauto.
Qed.

Lemma ris_simu_correct f1 f2 ris1 ris2 (ctx:simu_proof_context f1 f2) sis1 sis2: 
  ris_simu ris1 ris2 ->
  ris_refines (bctx1 ctx) ris1 sis1 ->
  ris_refines (bctx2 ctx) ris2 sis2 ->
  sistate_simu ctx sis1 sis2.
Proof.
  intros RIS REF1 REF2 rs m SEM.
  exploit sem_si_ok; 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.
    erewrite <- smem_eval_preserved; eauto.
    erewrite MEM_EQ; eauto.
  + erewrite <- REG_EQ, <- SIMU_REG; eauto.
    erewrite <- eval_sval_preserved; eauto.
    erewrite REG_EQ; eauto.
Qed.

Inductive optrsv_refines ctx: (option sval) -> (option sval) -> Prop :=
  | RefSome rsv sv
     (REF:eval_sval ctx rsv = eval_sval ctx sv)
     :optrsv_refines ctx (Some rsv) (Some sv)
  | RefNone: optrsv_refines ctx None None
  .

Inductive rsvident_refines ctx: (sval + ident) -> (sval + ident) -> Prop :=
  | RefLeft rsv sv
     (REF:eval_sval ctx rsv = eval_sval ctx sv)
     :rsvident_refines ctx (inl rsv) (inl sv)
  | RefRight id1 id2
     (IDSIMU: id1 = id2)
     :rsvident_refines ctx (inr id1) (inr id2)
  .

Definition bargs_refines ctx (rargs: list (builtin_arg sval)) (args: list (builtin_arg sval)): Prop :=
  eval_list_builtin_sval ctx rargs = eval_list_builtin_sval ctx args.

Inductive rfv_refines ctx: sfval -> sfval -> Prop :=
  | RefGoto pc: rfv_refines ctx (Sgoto pc) (Sgoto pc)
  | RefCall sig rvos ros rargs args r pc
      (SV:rsvident_refines ctx rvos ros)
      (LIST:eval_list_sval ctx rargs = eval_list_sval ctx args)
      :rfv_refines ctx (Scall sig rvos rargs r pc) (Scall sig ros args r pc)
  | RefTailcall sig rvos ros rargs args
      (SV:rsvident_refines ctx rvos ros)
      (LIST:eval_list_sval ctx rargs = eval_list_sval ctx args)
      :rfv_refines ctx (Stailcall sig rvos rargs) (Stailcall sig ros args)
  | RefBuiltin ef lbra lba br pc
      (BARGS: bargs_refines ctx lbra lba)
      :rfv_refines ctx (Sbuiltin ef lbra br pc) (Sbuiltin ef lba br pc)
  | RefJumptable rsv sv lpc
      (VAL: eval_sval ctx rsv = eval_sval ctx sv)
      :rfv_refines ctx (Sjumptable rsv lpc) (Sjumptable sv lpc)
  | RefReturn orsv osv
      (OPT:optrsv_refines ctx orsv osv)
      :rfv_refines ctx (Sreturn orsv) (Sreturn osv)
.

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

Local Hint Resolve eval_sval_preserved list_sval_eval_preserved smem_eval_preserved eval_list_builtin_sval_preserved: core.

Lemma rvf_simu_correct f1 f2 rfv1 rfv2 (ctx: simu_proof_context f1 f2) sfv1 sfv2: 
  rfv_simu rfv1 rfv2 ->
  rfv_refines (bctx1 ctx) rfv1 sfv1 ->
  rfv_refines (bctx2 ctx) rfv2 sfv2 ->
  sfv_simu ctx sfv1 sfv2.
Proof.
  unfold rfv_simu; intros X REF1 REF2. subst.
  unfold bctx2; destruct REF1; inv REF2; simpl; econstructor; eauto.
  - (* call svid *)
    inv SV; inv SV0; econstructor; eauto.
    rewrite <- REF, <- REF0; eauto.
  - (* call args *)
    rewrite <- LIST, <- LIST0; eauto.
  - (* taillcall svid *)
    inv SV; inv SV0; econstructor; eauto.
    rewrite <- REF, <- REF0; eauto.
  - (* tailcall args *)
    rewrite <- LIST, <- LIST0; eauto.
  - (* builtin args *)
    unfold bargs_refines, bargs_simu in *.
    rewrite <- BARGS, <- BARGS0; eauto.
  - rewrite <- VAL, <- VAL0; eauto.
  - (* return *)
    inv OPT; inv OPT0; econstructor; eauto.
    rewrite <- REF, <- REF0; eauto.
Qed.

(* refinement of (symbolic) state *)
Inductive rstate :=
  | Rfinal (ris: ristate) (rfv: sfval)
  | Rcond (cond: condition) (rargs: list_sval) (rifso rifnot: 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 <- eval_scondition 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)
      (RFV: rfv_simu rfv1 rfv2)
      : rst_simu (Rfinal ris1 rfv1) (Rfinal ris2 rfv2)
  | Rcond_simu cond rargs rifso1 rifnot1 rifso2 rifnot2
      (IFSO: rst_simu rifso1 rifso2)
      (IFNOT: 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
*)
  .

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 <- eval_scondition_preserved.
  autodestruct.
  destruct b; simpl; auto.
Qed.

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 (Rfinal ris rfv) (Sfinal sis sfv)
  | Refcond rcond cond rargs args rifso rifnot ifso ifnot
      (RCOND: eval_scondition ctx rcond rargs = eval_scondition ctx cond args)
      (REFso: eval_scondition ctx rcond rargs = Some true -> rst_refines ctx rifso ifso)
      (REFnot: eval_scondition ctx rcond rargs = Some false -> rst_refines ctx rifnot ifnot)
      : rst_refines ctx (Rcond rcond rargs rifso rifnot) (Scond cond args ifso ifnot)
  | Refabort
      : 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_okpreserv 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 f1 f2 (ctx: simu_proof_context f1 f2) rst1 rst2 st1 st2
   (SIMU: rst_simu rst1 rst2) 
   (REF1: forall sis sfv, get_soutcome (bctx1 ctx) st1 = Some (sout sis sfv) -> si_ok (bctx1 ctx) sis -> rst_refines (bctx1 ctx) rst1 st1)
   (REF2: forall ris rfv, get_routcome (bctx2 ctx) rst2 = Some (rout ris rfv) -> ris_ok (bctx2 ctx) ris -> rst_refines (bctx2 ctx) rst2 st2)
   :sstate_simu ctx st1 st2.
Proof.
  intros sis1 sfv1 SOUT OK1.
  exploit REF1; eauto.
  clear REF1; intros REF1.
  exploit rst_refines_outcome_okpreserv; eauto. clear REF1 SOUT.
  intros (ris1 & rfv1 & ROUT1 & REFI1 & REFF1).
  rewrite OK_EQUIV in OK1; eauto. 
  exploit REFF1; eauto. clear REFF1; intros REFF1.
  exploit rst_simu_lroutcome; eauto.
  intros (ris2 & rfv2 & ROUT2 & SIMUI & SIMUF). clear ROUT1.
  exploit ris_simu_ok_preserv; eauto.
  clear OK1. intros OK2.
  exploit REF2; eauto. clear REF2; intros REF2.
  exploit rst_refines_outcome_up; eauto.
  intros (sis2 & sfv2 & SOUT & REFI2 & REFF2).
  do 2 eexists; split; eauto.
Qed.


(** * Properties of the (abstract) operators involved in symbolic execution *)

Lemma ok_set_mem ctx sm sis:
  si_ok ctx (set_smem sm sis)
  <-> (si_ok ctx sis /\ eval_smem ctx sm <> None).
Proof.
  split; destruct 1; econstructor; simpl in *; eauto.
  intuition eauto.
Qed.

Lemma ok_set_sreg ctx r sv sis:
  si_ok ctx (set_sreg r sv sis)
  <-> (si_ok ctx sis /\ eval_sval ctx sv <> None).
Proof.
  unfold set_sreg; split.
  + intros [(SVAL & PRE) SMEM SREG]; simpl in *; split.
    - econstructor; eauto.
      intros r0; generalize (SREG r0); destruct (Pos.eq_dec r r0); try congruence.
    - generalize (SREG r); destruct (Pos.eq_dec r r); try congruence.
  + intros ([PRE SMEM SREG] & SVAL).
    econstructor; simpl; eauto.
    intros r0;  destruct (Pos.eq_dec r r0); try congruence.
Qed.

Lemma si_ok_op_okpreserv ctx op args dest sis: si_ok ctx (sexec_op op args dest sis) -> si_ok ctx sis.
Proof.
  unfold sexec_op. rewrite ok_set_sreg. intuition.
Qed.

Lemma si_ok_load_okpreserv ctx chunk addr args dest sis trap: si_ok ctx (sexec_load trap chunk addr args dest sis) -> si_ok ctx sis.
Proof.
  unfold sexec_load. rewrite ok_set_sreg. intuition.
Qed.

Lemma si_ok_store_okpreserv ctx chunk addr args src sis: si_ok ctx (sexec_store chunk addr args src sis) -> si_ok ctx sis.
Proof.
  unfold sexec_store. rewrite ok_set_mem. intuition.
Qed.

Lemma si_ok_tr_okpreserv ctx fi sis: si_ok ctx (tr_sis (cf ctx) fi sis) -> si_ok ctx sis.
Proof.
  unfold tr_sis. intros OK; inv OK. simpl in *. intuition.
Qed.

(* These lemmas are very bad for eauto: we put them into a dedicated basis. *)
Local Hint Resolve si_ok_tr_okpreserv si_ok_op_okpreserv si_ok_load_okpreserv si_ok_store_okpreserv: sis_ok.

Lemma sexec_rec_okpreserv 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; eauto with sis_ok.
  - intros. eapply IHib1. 2-3: eauto.
    eapply IHib2; eauto.
  - intros k CONT sis lsis sfv.
    do 2 autodestruct; eauto.
Qed.

(* an alternative tr_sis *)

Definition transfer_sis (inputs: list reg) (sis:sistate): sistate :=
   {| si_pre := fun ctx => (sis.(si_pre) ctx /\ forall r, eval_sval ctx (sis.(si_sreg) r) <> None);
      si_sreg := transfer_sreg inputs sis;
      si_smem := sis.(si_smem) |}.

Lemma ok_transfer_sis ctx inputs sis:
  si_ok ctx (transfer_sis inputs sis)
  <-> (si_ok ctx sis).
Proof.
  unfold transfer_sis. induction inputs as [|r l]; simpl.
  + split; destruct 1; econstructor; simpl in *; intuition eauto. congruence.
  + split.
    * destruct 1; econstructor; simpl in *; intuition eauto.
    * intros X; generalize X. rewrite <- IHl in X; clear IHl.
      intros [PRE SMEM SREG].
      econstructor; simpl; eauto.
      intros r0;  destruct (Pos.eq_dec r r0); try congruence.
      intros H; eapply OK_SREG; eauto.
Qed.

Definition alt_tr_sis := poly_tr (fun f tbl or => transfer_sis (Regset.elements (pre_inputs f tbl or))).

Lemma tr_sis_alt_def f fi sis:
  alt_tr_sis f fi sis = tr_sis f fi sis.
Proof.
  unfold tr_sis, str_inputs. destruct fi; simpl; auto.
Qed.


(** * Refinement of the symbolic execution (e.g. refinement of [sexec] into [rexec]).

TODO: Est-ce qu'on garde cette vision purement fonctionnelle de l'implementation ?
=> ça pourrait être pratique quand on va compliquer encore le vérificateur !

Du coup, on introduirait une version avec hash-consing qui serait en correspondance 
pour une relation d'equivalence sur les ristate ?

Attention toutefois, il est possible que certaines parties de l'execution soient pénibles à formuler 
en programmation fonctionnelle pure (exemple: usage de l'égalité de pointeur comme test d'égalité rapide!)


*)

Local Hint Constructors rfv_refines optrsv_refines rsvident_refines rsvident_refines: core.

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 (si_sreg sis) args)).
Proof.
  intros REF OK.
  induction args; simpl; eauto.
  intros; erewrite REG_EQ, IHargs; eauto.
Qed.

Local Hint Resolve eval_list_sval_refpreserv: core.

Lemma eval_builtin_sval_refpreserv ctx arg ris sis:
  ris_refines ctx ris sis ->
  ris_ok ctx ris ->
  eval_builtin_sval ctx (builtin_arg_map ris arg) = eval_builtin_sval ctx (builtin_arg_map sis arg).
Proof.
  intros REF OK; induction arg; simpl; eauto.
  + erewrite REG_EQ; eauto.
  + erewrite IHarg1, IHarg2; eauto.
  + erewrite IHarg1, IHarg2; eauto.
Qed.

Lemma bargs_refpreserv ctx args ris sis:
  ris_refines ctx ris sis ->
  ris_ok ctx ris ->
  bargs_refines ctx (map (builtin_arg_map ris) args) (map (builtin_arg_map sis) args).
Proof.
  unfold bargs_refines. intros REF OK.
  induction args; simpl; eauto.
  erewrite eval_builtin_sval_refpreserv, IHargs; eauto.
Qed.

Local Hint Resolve bargs_refpreserv: core.

Lemma exec_final_refpreserv ctx i ris sis:
  ris_refines ctx ris sis ->
  ris_ok ctx ris ->
  rfv_refines ctx (sexec_final_sfv i ris) (sexec_final_sfv i sis).
Proof.
  destruct i; simpl; unfold sum_left_map; try autodestruct; eauto.
Qed.

Definition ris_init: ristate := {| ris_smem:= fSinit; ris_input_init:=true; ok_rsval := nil; ris_sreg := PTree.empty _ |}.

Lemma ris_init_correct ctx:
  ris_refines ctx ris_init sis_init.
Proof.
  unfold ris_init, sis_init; econstructor; simpl in *; eauto.
  split; destruct 1; econstructor; simpl in *; eauto.
    congruence.
Qed.

Definition rset_smem rm (ris:ristate): ristate :=
  {| ris_smem := rm;
     ris_input_init := ris.(ris_input_init);
     ok_rsval := ris.(ok_rsval);
     ris_sreg:= ris.(ris_sreg)
  |}.

Lemma ok_rset_mem ctx rm (ris: ristate):
  (eval_smem ctx ris.(ris_smem) = None -> eval_smem ctx rm = None) ->
  ris_ok ctx (rset_smem rm ris)
  <-> (ris_ok ctx ris /\ eval_smem ctx rm <> None).
Proof.
   split; destruct 1; econstructor; simpl in *; eauto.
Qed.

Lemma rset_mem_correct ctx rm sm ris sis:
  (eval_smem ctx ris.(ris_smem) = None -> eval_smem ctx rm = None) ->
  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 2; intros.
  econstructor; eauto.
  + rewrite ok_set_mem, ok_rset_mem; intuition congruence.
  + rewrite ok_rset_mem; intuition eauto.
  + rewrite ok_rset_mem; intuition eauto.
Qed.

Definition rexec_store chunk addr args src ris: ristate :=
   let args := list_sval_inj (List.map (ris_sreg_get ris) args) in
   let src := ris_sreg_get ris src in
   let rm := fSstore ris.(ris_smem) chunk addr args src in
   rset_smem rm ris.

Lemma rexec_store_correct ctx chunk addr args src ris sis:
  ris_refines ctx ris sis ->
  ris_refines ctx (rexec_store chunk addr args src ris) (sexec_store chunk addr args src sis).
Proof.
  intros REF; eapply rset_mem_correct; simpl; eauto.
  + intros X; rewrite X. repeat autodestruct; eauto.
  + intros OK; erewrite eval_list_sval_refpreserv, MEM_EQ, REG_EQ; eauto.
Qed.

(* TODO: reintroduire le "root_apply" ? *)

Definition rset_sreg r rsv (ris:ristate): ristate :=
  {| ris_smem := ris.(ris_smem);
     ris_input_init := ris.(ris_input_init);
     ok_rsval := rsv::ris.(ok_rsval); (* TODO: A CHANGER ? *)
     ris_sreg:= PTree.set r rsv ris.(ris_sreg) (* TODO: A CHANGER *)
  |}.

Lemma ok_rset_sreg ctx r rsv ris:
  ris_ok ctx (rset_sreg r rsv ris)
  <-> (ris_ok ctx ris /\ eval_sval ctx rsv <> None).
Proof.
   split; destruct 1; econstructor; simpl in *; eauto.
   intuition subst; eauto.
   exploit OK_RREG; eauto.
Qed.

Lemma rset_reg_correct ctx r rsv sv ris sis:
  ris_refines ctx ris sis ->
  (ris_ok ctx ris -> eval_sval ctx rsv = eval_sval ctx sv) ->
  ris_refines ctx (rset_sreg r rsv ris) (set_sreg r sv sis).
Proof.
  destruct 1; intros.
  econstructor; eauto.
  + rewrite ok_set_sreg, ok_rset_sreg; intuition congruence.
  + rewrite ok_rset_sreg; intuition eauto.
  + rewrite ok_rset_sreg. intros; unfold rset_sreg, set_sreg, ris_sreg_get; simpl. intuition eauto.
    destruct (Pos.eq_dec _ _).
    * subst; rewrite PTree.gss; eauto.
    * rewrite PTree.gso; eauto.
Qed.

Definition rexec_op op args dst (ris:ristate): ristate :=
   let args := list_sval_inj (List.map ris args) in
   rset_sreg dst (fSop op args) ris.

Lemma rexec_op_correct ctx op args dst ris sis:
  ris_refines ctx ris sis ->
  ris_refines ctx (rexec_op op args dst ris) (sexec_op op args dst sis).
Proof.
  intros REF; eapply rset_reg_correct; simpl; eauto.
  intros OK; erewrite eval_list_sval_refpreserv; eauto.
Qed.

Definition rexec_load trap chunk addr args dst (ris:ristate): ristate :=
   let args := list_sval_inj (List.map ris args) in
   rset_sreg dst (fSload ris.(ris_smem) trap chunk addr args) ris.

Lemma rexec_load_correct ctx trap chunk addr args dst ris sis:
  ris_refines ctx ris sis ->
  ris_refines ctx (rexec_load trap chunk addr args dst ris) (sexec_load trap chunk addr args dst sis).
Proof.
  intros REF; eapply rset_reg_correct; simpl; eauto.
  intros OK; erewrite eval_list_sval_refpreserv, MEM_EQ; eauto.
Qed.

Lemma eval_scondition_refpreserv ctx cond args ris sis:
  ris_refines ctx ris sis ->
  ris_ok ctx ris ->
  eval_scondition ctx cond (list_sval_inj (map ris args)) = eval_scondition ctx cond (list_sval_inj (map sis args)).
Proof.
  intros; unfold eval_scondition.
  erewrite eval_list_sval_refpreserv; eauto.
Qed.


(* transfer *)

Definition rseto_sreg r rsv (ris:ristate): ristate :=
  {| ris_smem := ris.(ris_smem);
     ris_input_init := ris.(ris_input_init);
     ok_rsval := ris.(ok_rsval);
     ris_sreg:= PTree.set r rsv ris.(ris_sreg) (* TODO: A CHANGER *)
  |}.

Lemma ok_rseto_sreg ctx r rsv ris:
  ris_ok ctx (rseto_sreg r rsv ris)
  <-> (ris_ok ctx ris).
Proof.
   split; destruct 1; econstructor; simpl in *; eauto.
Qed.

Lemma rseto_reg_correct ctx r rsv sv ris sis:
  ris_refines ctx ris sis ->
  (ris_ok ctx ris -> eval_sval ctx rsv <> None) ->
  (ris_ok ctx ris -> eval_sval ctx rsv = eval_sval ctx sv) ->
  ris_refines ctx (rseto_sreg r rsv ris) (set_sreg r sv sis).
Proof.
  destruct 1; intros.
  econstructor; eauto.
  + rewrite ok_set_sreg, ok_rseto_sreg; intuition congruence.
  + rewrite ok_rseto_sreg; intuition eauto.
  + rewrite ok_rseto_sreg. intros; unfold rseto_sreg, set_sreg, ris_sreg_get; simpl. intuition eauto.
    destruct (Pos.eq_dec _ _).
    * subst; rewrite PTree.gss; eauto.
    * rewrite PTree.gso; eauto.
Qed.

Fixpoint transfer_ris (inputs: list reg) (ris:ristate): ristate :=
  match inputs with
  | nil =>   {| ris_smem := ris.(ris_smem);
                ris_input_init := false;
                ok_rsval := ris.(ok_rsval);
                ris_sreg:= PTree.empty _
             |}
  | r::l => rseto_sreg r (ris_sreg_get ris r) (transfer_ris l ris)
  end.

Lemma ok_transfer_ris ctx inputs ris:
  ris_ok ctx (transfer_ris inputs ris)
  <-> (ris_ok ctx ris).
Proof.
  induction inputs as [|r l]; simpl.
  + split; destruct 1; econstructor; simpl in *; intuition eauto.
  + rewrite ok_rseto_sreg. auto.
Qed.

Lemma transfer_ris_correct ctx inputs ris sis:
  ris_refines ctx ris sis ->
  ris_refines ctx (transfer_ris inputs ris) (transfer_sis inputs sis).
Proof.
  destruct 1; intros.
  induction inputs as [|r l].
  + econstructor; eauto.
    * erewrite ok_transfer_sis, ok_transfer_ris; eauto.
    * erewrite ok_transfer_ris; eauto.
  + econstructor; eauto.
    * erewrite ok_transfer_sis, ok_transfer_ris; eauto.
    * erewrite ok_transfer_ris; simpl.
      intros; erewrite MEM_EQ. 2: eauto.
      - unfold transfer_sis; simpl; eauto.
      - rewrite ok_transfer_ris; simpl; eauto.
    * erewrite ok_transfer_ris; simpl.
      intros H r0.
      erewrite REG_EQ. 2: eapply rseto_reg_correct; eauto.
      - unfold set_sreg; simpl; auto.
        destruct (Pos.eq_dec _ _); simpl; auto.
      - intros. rewrite REG_EQ0; auto. apply OK_SREG; tauto.
      - rewrite ok_rseto_sreg, ok_transfer_ris. auto.
Qed.

Definition tr_ris := poly_tr (fun f tbl or => transfer_ris (Regset.elements (pre_inputs f tbl or))).

Local Hint Resolve transfer_ris_correct ok_transfer_ris: core.
Local Opaque transfer_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 ris_ok_tr_okpreserv 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 fi ris sis:
  ris_refines ctx ris 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.

(** 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)
  (* basic instructions *)
  | Bnop _ => k ris
  | Bop op args res _ => k (rexec_op op args res ris)
  | Bload trap chunk addr args dst _ => k (rexec_load trap chunk addr args dst ris)
  | 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
  end
  .

Definition rexec f ib := rexec_rec f ib ris_init (fun _ => Rabort).


Local Hint Resolve ris_init_correct exec_final_refpreserv tr_ris_correct ris_ok_tr_okpreserv
  rexec_op_correct rexec_load_correct rexec_store_correct: core.

Local Hint Constructors rst_refines: core.

Lemma rexec_rec_correct1 ctx ib: 
  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)
  (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).
  - (* seq *)
    intros; subst.
    eapply IHib1. 3-6: eauto.
    + simpl. eapply sexec_rec_okpreserv; eauto.
    + intros; subst. eapply IHib2; eauto.
  - (* cond *)
    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_okpreserv with (ib:=(Bcond cond args ib1 ib2 iinfo)); simpl; eauto.
    }
    generalize OUT; clear OUT; simpl.
    autodestruct.
    intros COND; generalize COND.
    erewrite <- eval_scondition_refpreserv; eauto.
    econstructor; try_simplify_someHyps.
Qed.

Lemma rexec_correct1 ctx ib 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.
  unfold sexec; intros; eapply rexec_rec_correct1; eauto; simpl; congruence.
Qed.


(** COPIER-COLLER ... Y a-t-il moyen de l'eviter ? **)

Lemma ris_ok_op_okpreserv ctx op args dest ris: ris_ok ctx (rexec_op op args dest ris) -> ris_ok ctx ris.
Proof.
  unfold rexec_op. rewrite ok_rset_sreg. intuition.
Qed.

Lemma ris_ok_load_okpreserv ctx chunk addr args dest ris trap: ris_ok ctx (rexec_load trap chunk addr args dest ris) -> ris_ok ctx ris.
Proof.
  unfold rexec_load. rewrite ok_rset_sreg. intuition.
Qed.

Lemma ris_ok_store_okpreserv ctx chunk addr args src ris: ris_ok ctx (rexec_store chunk addr args src ris) -> ris_ok ctx ris.
Proof.
  unfold rexec_store. rewrite ok_rset_mem; simpl. 
  + intuition.
  + intros X; rewrite X; simpl.
    repeat autodestruct.
Qed.

(* These lemmas are very bad for eauto: we put them into a dedicated basis. *)
Local Hint Resolve ris_ok_store_okpreserv ris_ok_op_okpreserv ris_ok_load_okpreserv: ris_ok.

Lemma rexec_rec_okpreserv ctx ib: 
  forall k
  (CONT: forall ris lris rfv, get_routcome ctx (k ris) = Some (rout lris rfv) ->  ris_ok ctx lris -> ris_ok ctx ris)
  ris lris rfv
  (ROUT: get_routcome ctx (rexec_rec (cf ctx) ib ris k) = Some (rout lris rfv))
  (OK: ris_ok ctx lris)
  ,ris_ok ctx ris.
Proof.
  induction ib; simpl; try (autodestruct; simpl).
  1-6: try_simplify_someHyps; eauto with ris_ok.
  - intros. eapply IHib1. 2-3: eauto.
    eapply IHib2; eauto.
  - intros k CONT sis lsis sfv.
    do 2 autodestruct; eauto.
Qed.

Lemma rexec_rec_correct2 ctx ib: 
  forall rk k
  (CONTh: forall ris lris rfv, get_routcome ctx (rk ris) = Some (rout lris rfv) ->  ris_ok ctx lris -> ris_ok ctx ris)
  (CONT: forall ris sis lris rfv st, ris_refines ctx ris sis -> rk ris = st -> get_routcome ctx (rk ris) = Some (rout lris rfv) -> ris_ok ctx lris -> rst_refines ctx (rk ris) (k sis))
  ris sis lris rfv st
  (REF: ris_refines ctx ris sis)
  (EXEC: rexec_rec (cf ctx) ib ris rk = st)
  (SOUT: get_routcome ctx st = Some (rout lris rfv))
  (OK: ris_ok ctx lris)
  , rst_refines ctx st (sexec_rec (cf ctx) ib sis k).
Proof.
  induction ib; simpl; try (intros; subst; eauto; fail).
  - (* seq *)
    intros; subst.
    eapply IHib1. 3-6: eauto.
    + simpl. eapply rexec_rec_okpreserv; eauto.
    + intros; subst. eapply IHib2; eauto.
  - (* cond *)
    intros rk k CONTh CONT ris sis lsis sfv st REF EXEC OUT OK. subst.
    assert (OK0: ris_ok ctx ris). {
      eapply rexec_rec_okpreserv with (ib:=(Bcond cond args ib1 ib2 iinfo)); simpl; eauto.
    }
    generalize OUT; clear OUT; simpl.
    autodestruct.
    intros COND; generalize COND.
    erewrite eval_scondition_refpreserv; eauto.
    econstructor; try_simplify_someHyps.
Qed.

Lemma rexec_correct2 ctx ib ris rfv:
  get_routcome ctx (rexec (cf ctx) ib) = Some (rout ris rfv) ->
  (ris_ok ctx ris) ->
  rst_refines ctx (rexec (cf ctx) ib) (sexec (cf ctx) ib).
Proof.
  unfold rexec; intros; eapply rexec_rec_correct2; eauto; simpl; congruence.
Qed.

Theorem rexec_simu_correct f1 f2 ib1 ib2:
  rst_simu (rexec f1 ib1) (rexec f2 ib2) ->
  symbolic_simu f1 f2 ib1 ib2.
Proof.
  intros SIMU ctx.
  eapply rst_simu_correct; eauto.
  + intros; eapply rexec_correct1; eauto.
  + intros; eapply rexec_correct2; eauto.
Qed.