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.

    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 !

    TODO: A REVOIR COMPLETEMENT.
    - introduire "fake" hash-consed values (à renommer en "refined" plutôt que "fake").

*)

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.

(** * Refinement of data-structures and of the specification of the simulation test *)

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;
    ok_rsval: 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 (ok_rsval 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.(ok_rsval) -> List.In sv ris1.(ok_rsval);
  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 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_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.
    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
  .

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
*)
  .

(* Comment prend on en compte le ris en cours d'execution ??? *)

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 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
  .

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,
   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;
  inv REF1; inv REF2; simpl in *; inv SEM1; auto.
  - (* final_simu *) 
    do 2 eexists; intuition; eauto.
    exploit sem_sok; eauto.
    erewrite OK_EQUIV; eauto.
    intros ROK1.
    exploit ris_simu_ok_preserv; eauto.
  - (* cond_simu *)
    destruct (seval_condition (bctx1 ctx) cond args sm) eqn: SCOND; try congruence.
    generalize RCOND0.
    erewrite <- seval_condition_preserved, RCOND by eauto.
    intros SCOND0; rewrite <- SCOND0 in RCOND0.
    erewrite <- SCOND0.
    destruct b; simpl.
    * exploit IHrst_simu1; eauto.
    * 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.

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)).
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:= Sinit; 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.
  + 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 :=
  {| ris_smem := rm;
     ris_input_init := ris.(ris_input_init);
     ok_rsval := ris.(ok_rsval);
     ris_sreg:= ris.(ris_sreg)
  |}.

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

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) ->
  (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.
  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 := Sstore 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 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.

(* 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_set_sreg ctx r sv sis:
  sis_ok ctx (set_sreg r sv sis)
  <-> (sis_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 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 (Sop op args Sinit) 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.
  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 :=
   let args := list_sval_inj (List.map ris args) in
   rset_sreg dst (Sload 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 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.
Proof.
  intros; unfold seval_condition.
  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.

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:
  sis_ok ctx (transfer_sis inputs sis)
  <-> (sis_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.

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.
    * erewrite ok_transfer_ris; simpl; unfold ris_sreg_get; simpl; eauto.
      intros; rewrite PTree.gempty. simpl; auto.
  + 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 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.

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 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 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.

(** 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)
  (* 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)
  | Bload NOTRAP chunk addr args dst _ => Rabort
  | 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
  .

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.

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)
  (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 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.
  unfold sexec; intros; eapply rexec_rec_correct; eauto.
  simpl; congruence.
Qed.