(** Implementation and refinement of the symbolic execution
 *)

Require Import Coqlib Maps Floats.
Require Import AST Integers Values Events Memory Globalenvs Smallstep.
Require Import Op Registers.
Require Import RTL RTLpath.
Require Import Errors Duplicate.
Require Import RTLpathSE_theory.
Require Import Axioms.

Local Open Scope error_monad_scope.
Local Open Scope option_monad_scope.

(** * TODO: refine symbolic values/symbolic memories with hash-consed symbolic values *)

(** * Implementation of local symbolic internal states - definitions and core simulation properties *)

(** name : Hash-consed Symbolic Internal state local. Later on we will use the
    refinement to introduce hash consing *)
Record hsistate_local := 
  { 
    (** [hsi_lsmem] represents the list of smem symbolic evaluations.
        The first one of the list is the current smem *)
    hsi_lsmem:> list smem;
    (** For the values in registers:
        1) we store a list of sval evaluations
        2) we encode the symbolic regset by a PTree *)
    hsi_ok_lsval: list sval;
    hsi_sreg:> PTree.t sval
  }.

Definition hsi_sreg_get (hst: PTree.t sval) r: sval :=
   match PTree.get r hst with 
   | None => Sinput r
   | Some sv => sv
   end.

(* NB: short cut *)
Definition hsi_sreg_eval ge sp (hst: PTree.t sval) r rs0 m0: option val :=
   match PTree.get r hst with 
   | None => Some (Regmap.get r rs0)
   | Some sv => seval_sval ge sp sv rs0 m0
   end.

Lemma hsi_sreg_eval_correct ge sp hst r rs0 m0:
  hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (hsi_sreg_get hst r) rs0 m0.
Proof.
  unfold hsi_sreg_eval, hsi_sreg_get; destruct (PTree.get r hst); simpl; auto.
Qed.

Definition hsi_smem_get (hst: list smem): smem :=
   match hst with 
   | nil => Sinit
   | sm::_ => sm
   end.

(* NB: short cut *)
Definition hsi_smem_eval ge sp (hst: list smem) rs0 m0 : option mem :=
   match hst with 
   | nil => Some m0
   | sm::_ => seval_smem ge sp sm rs0 m0
   end.

Lemma hsi_smem_eval_correct ge sp hst rs0 m0:
  hsi_smem_eval ge sp hst rs0 m0 = seval_smem ge sp (hsi_smem_get hst) rs0 m0.
Proof.
  unfold hsi_smem_eval, hsi_smem_get; destruct hst; simpl; auto.
Qed.


(* negation of sabort_local *)
Definition sok_local (ge: RTL.genv) (sp:val) (rs0: regset) (m0: mem) (st: sistate_local): Prop :=
  (st.(si_pre) ge sp rs0 m0)
  /\ seval_smem ge sp st.(si_smem) rs0 m0 <> None
  /\ forall (r: reg), seval_sval ge sp (si_sreg st r) rs0 m0 <> None.

Lemma ssem_local_sok ge sp rs0 m0 st rs m:
  ssem_local ge sp st rs0 m0 rs m -> sok_local ge sp rs0 m0 st.
Proof.
  unfold sok_local, ssem_local. 
  intuition congruence.
Qed.

Definition hsok_local ge sp rs0 m0 (hst: hsistate_local) : Prop :=
     (forall sv, List.In sv (hsi_ok_lsval hst) -> seval_sval ge sp sv rs0 m0 <> None)
  /\ (forall sm, List.In sm (hsi_lsmem hst) -> seval_smem ge sp sm rs0 m0 <> None).

(* refinement link between a (st: sistate_local) and (hst: hsistate_local) *)
Definition hsilocal_refines ge sp rs0 m0 (hst: hsistate_local) (st: sistate_local) :=
      (sok_local ge sp rs0 m0 st <-> hsok_local ge sp rs0 m0 hst) 
  /\  (hsok_local ge sp rs0 m0 hst -> hsi_smem_eval ge sp hst rs0 m0 = seval_smem ge sp st.(si_smem) rs0 m0)
  /\  (hsok_local ge sp rs0 m0 hst -> forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (si_sreg st r) rs0 m0).

Lemma ssem_local_refines_hok ge sp rs0 m0 hst st rs m:
  ssem_local ge sp st rs0 m0 rs m -> hsilocal_refines ge sp rs0 m0 hst st -> hsok_local ge sp rs0 m0 hst.
Proof.
  intros H0 (H1 & _ & _). apply H1. eapply ssem_local_sok. eauto.
Qed.

Definition is_subset {A: Type} (lv2 lv1: list A) := forall v, In v lv2 -> In v lv1.

Definition hsilocal_simu_core (hst1 hst2: hsistate_local) :=
     is_subset (hsi_lsmem hst2) (hsi_lsmem hst1)
  /\ is_subset (hsi_ok_lsval hst2) (hsi_ok_lsval hst1)
  /\ (forall r, hsi_sreg_get hst2 r = hsi_sreg_get hst1 r)
  /\ hsi_smem_get hst1 = hsi_smem_get hst2.

Lemma hsilocal_simu_core_nofail ge1 ge2 sp rs0 m0 hst1 hst2:
  hsilocal_simu_core hst1 hst2 ->
  (forall s, Genv.find_symbol ge1 s = Genv.find_symbol ge2 s) ->
  hsok_local ge1 sp rs0 m0 hst1 ->
  hsok_local ge2 sp rs0 m0 hst2.
Proof.
  intros (MEMOK & RSOK & _ & _) GFS (OKV & OKM). constructor.
  - intros sv INS. apply RSOK in INS. apply OKV in INS. erewrite seval_preserved; eauto.
  - intros sm INS. apply MEMOK in INS. apply OKM in INS. erewrite smem_eval_preserved; eauto.
Qed.

Remark istate_simulive_reflexive dm is: istate_simulive  (fun _ : Regset.elt => True) dm is is.
Proof.
  unfold istate_simulive. 
  repeat (constructor; auto).
Qed.

Theorem hsilocal_simu_core_correct hst1 hst2 ge1 ge2 sp rs0 m0 rs m st1 st2:
  hsilocal_simu_core hst1 hst2 ->
  hsilocal_refines ge1 sp rs0 m0 hst1 st1 ->
  hsilocal_refines ge2 sp rs0 m0 hst2 st2 ->
  (forall s, Genv.find_symbol ge1 s = Genv.find_symbol ge2 s) ->
  ssem_local ge1 sp st1 rs0 m0 rs m ->
  ssem_local ge2 sp st2 rs0 m0 rs m.
Proof.
  intros CORE HREF1 HREF2 GFS SEML.
  exploit ssem_local_refines_hok; eauto. intro HOK1.
  exploit hsilocal_simu_core_nofail; eauto. intro HOK2.
  destruct SEML as (PRE & MEMEQ & RSEQ).
  constructor; [|constructor].
  + destruct HREF2 as (OKEQ & _ & _). rewrite <- OKEQ in HOK2. apply HOK2.
  + destruct HREF2 as (_ & MEMEQ2 & _). destruct HREF1 as (_ & MEMEQ1 & _).
    destruct CORE as (_ & _ & _ & MEMEQ3).
    rewrite <- MEMEQ2; auto. rewrite hsi_smem_eval_correct. rewrite <- MEMEQ3.
    erewrite smem_eval_preserved; [| eapply GFS].
    rewrite <- hsi_smem_eval_correct. rewrite MEMEQ1; auto.
  + intro r. destruct HREF2 as (_ & _ & A). destruct HREF1 as (_ & _ & B).
    destruct CORE as (_ & _ & C & _). rewrite <- A; auto. rewrite hsi_sreg_eval_correct.
    rewrite C. erewrite seval_preserved; [| eapply GFS]. rewrite <- hsi_sreg_eval_correct.
    rewrite B; auto.
Qed.

(* Syntax and semantics of symbolic exit states *)
(* TODO: add hash-consing *)
Record hsistate_exit := mk_hsistate_exit
  { hsi_cond: condition; hsi_scondargs: list_sval; hsi_elocal: hsistate_local; hsi_ifso: node }.

Definition hsiexit_simu_core dm f (hse1 hse2: hsistate_exit) :=
  (exists path, (fn_path f) ! (hsi_ifso hse1) = Some path)
  /\ dm ! (hsi_ifso hse2) = Some (hsi_ifso hse1)
  /\ hsi_cond hse1 = hsi_cond hse2
  /\ hsi_scondargs hse1 = hsi_scondargs hse2 (* FIXME - should there be something about okvals ? *)
  /\ hsilocal_simu_core (hsi_elocal hse1) (hsi_elocal hse2).

Definition hsiexit_simu_coreb (dm: PTree.t node) (f: RTLpath.function) (hse1 hse2: hsistate_exit) := OK tt (* TODO *).

Theorem hsiexit_simu_coreb_correct hse1 hse2 dm f:
  hsiexit_simu_coreb dm f hse1 hse2 = OK tt ->
  hsiexit_simu_core dm f hse1 hse2.
Proof.
Admitted.

(** NB: we split the refinement relation between a "static" part -- independendent of the initial context
   and a "dynamic" part -- that depends on it
*)
Definition hsiexit_refines_stat (hext: hsistate_exit) (ext: sistate_exit): Prop :=
     hsi_cond hext = si_cond ext
  /\ hsi_ifso hext = si_ifso ext.

Definition hsok_exit ge sp rs m hse := hsok_local ge sp rs m (hsi_elocal hse).

Definition hsiexit_refines_dyn ge sp rs0 m0 (hext: hsistate_exit) (ext: sistate_exit): Prop :=
   hsilocal_refines ge sp rs0 m0 (hsi_elocal hext) (si_elocal ext)
   /\ seval_condition ge sp (hsi_cond hext) (hsi_scondargs hext) (hsi_smem_get (hsi_elocal hext)) rs0 m0
         = seval_condition ge sp (si_cond ext) (si_scondargs ext) (si_smem (si_elocal ext)) rs0 m0.

Definition hsiexit_simu dm f (ctx: simu_proof_context f) hse1 hse2: Prop := forall se1 se2,
  hsiexit_refines_stat hse1 se1 ->
  hsiexit_refines_stat hse2 se2 ->
  hsiexit_refines_dyn (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse1 se1 ->
  hsiexit_refines_dyn (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse2 se2 ->
  siexit_simu dm f ctx se1 se2.

Lemma hsiexit_simu_core_nofail dm f hse1 hse2 ge1 ge2 sp rs m:
  hsiexit_simu_core dm f hse1 hse2 ->
  (forall s, Genv.find_symbol ge1 s = Genv.find_symbol ge2 s) ->
  hsok_exit ge1 sp rs m hse1 ->
  hsok_exit ge2 sp rs m hse2.
Proof.
  intros CORE GFS HOK1.
  destruct CORE as (_ & _ & _ & _ & CORE).
  eapply hsilocal_simu_core_nofail; eauto.
Qed.

Theorem hsiexit_simu_core_correct dm f hse1 hse2 ctx:
  hsiexit_simu_core dm f hse1 hse2 ->
  hsiexit_simu dm f ctx hse1 hse2.
Proof.
  intros SIMUC (* HOK1 *) st1 st2 HREF1 HREF2 HDYN1 HDYN2.
  assert (SEVALC:
    seval_condition (the_ge1 ctx) (the_sp ctx) (si_cond st1) (si_scondargs st1) (si_smem (si_elocal st1)) 
  (the_rs0 ctx) (the_m0 ctx) =
    seval_condition (the_ge2 ctx) (the_sp ctx) (si_cond st2) (si_scondargs st2) (si_smem (si_elocal st2)) 
  (the_rs0 ctx) (the_m0 ctx)).
  { destruct HDYN1 as (_ & SCOND1). rewrite <- SCOND1 by assumption. clear SCOND1.
    destruct HDYN2 as (_ & SCOND2). rewrite <- SCOND2 by assumption. clear SCOND2.
    destruct SIMUC as (_ & _ & CONDEQ & ARGSEQ & LSIMU). destruct LSIMU as (_ & _ & _ & MEMEQ).
    rewrite CONDEQ. rewrite ARGSEQ. rewrite MEMEQ. erewrite <- seval_condition_preserved; eauto.
    eapply ctx. }
  constructor; [assumption|]. intros is1 SSEME.
  assert (HOK1: hsok_exit (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse1). {
    unfold hsok_exit. destruct SSEME as (_ & SSEML & _). apply ssem_local_sok in SSEML.
    destruct HDYN1 as (LREF & _). destruct LREF as (OKEQ & _ & _). rewrite <- OKEQ. assumption. }
  exploit hsiexit_simu_core_nofail. 2: eapply ctx. all: eauto. intro HOK2.
  exists (mk_istate (icontinue is1) (si_ifso st2) (irs is1) (imem is1)). simpl. constructor.
  - constructor; [|constructor].
    + rewrite <- SEVALC. destruct SSEME as (SCOND & _ & _). assumption.
    + destruct SSEME as (_ & SLOC & _). destruct SIMUC as (_ & _ & _ & _ & LSIMU).
      destruct HDYN1 as (LREF1 & _). destruct HDYN2 as (LREF2 & _).
      eapply hsilocal_simu_core_correct; eauto. apply ctx.
    + reflexivity.
  - unfold istate_simu. destruct (icontinue is1) eqn:ICONT.
    * constructor; [|constructor]; simpl; auto.
      constructor; auto.
    * simpl. destruct SIMUC as ((path & PATH) & REVEQ & _ & _ & _ & _).
      assert (PCEQ: hsi_ifso hse1 = ipc is1). { destruct SSEME as (_ & _ & PCEQ). destruct HREF1 as (_ & IFSO). congruence. }
      exists path. constructor; [|constructor].
      + congruence.
      + constructor; [|constructor]; simpl; auto.
        constructor; auto.
      + destruct HREF2 as (_ & IFSO). congruence.
Qed.

Remark hsiexit_simu_siexit dm f ctx hse1 hse2 se1 se2:
  hsiexit_simu dm f ctx hse1 hse2 ->
  hsiexit_refines_stat hse1 se1 ->
  hsiexit_refines_stat hse2 se2 ->
  hsiexit_refines_dyn (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse1 se1 ->
  hsiexit_refines_dyn (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse2 se2 ->
  siexit_simu dm f ctx se1 se2.
Proof.
  auto.
Qed.

Definition hsiexits_simu dm f (ctx: simu_proof_context f) lhse1 lhse2: Prop :=
  list_forall2 (hsiexit_simu dm f ctx) lhse1 lhse2.

Definition hsiexits_simu_core dm f lhse1 lhse2: Prop :=
  list_forall2 (hsiexit_simu_core dm f) lhse1 lhse2.

Theorem hsiexits_simu_core_correct dm f lhse1 lhse2 ctx:
  hsiexits_simu_core dm f lhse1 lhse2 ->
  hsiexits_simu dm f ctx lhse1 lhse2.
Proof.
  induction 1; [constructor|].
  constructor; [|apply IHlist_forall2; assumption].
  apply hsiexit_simu_core_correct; assumption.
Qed.

Definition hsiexits_refines_stat lhse lse :=
  list_forall2 hsiexit_refines_stat lhse lse.

Definition hsiexits_refines_dyn ge sp rs0 m0 lhse se :=
  list_forall2 (hsiexit_refines_dyn ge sp rs0 m0) lhse se.

(** * Syntax and Semantics of symbolic internal state *)
Record hsistate := { hsi_pc: node; hsi_exits: list hsistate_exit; hsi_local: hsistate_local }.

Definition hsistate_simu_core dm f (hse1 hse2: hsistate) :=
     dm ! (hsi_pc hse2) = Some (hsi_pc hse1)
  /\ list_forall2 (hsiexit_simu_core dm f) (hsi_exits hse1) (hsi_exits hse2)
  /\ hsilocal_simu_core (hsi_local hse1) (hsi_local hse2).

Definition hsistate_refines_stat (hst: hsistate) (st:sistate): Prop :=
  hsi_pc hst = si_pc st
  /\ hsiexits_refines_stat (hsi_exits hst) (si_exits st).

Definition hsistate_refines_dyn ge sp rs0 m0 (hst: hsistate) (st:sistate): Prop :=
     hsiexits_refines_dyn ge sp rs0 m0 (hsi_exits hst) (si_exits st)
  /\ hsilocal_refines ge sp rs0 m0 (hsi_local hst) (si_local st).

Definition hsistate_simu dm f (hst1 hst2: hsistate) (ctx: simu_proof_context f): Prop := forall st1 st2,
  hsistate_refines_stat hst1 st1 ->
  hsistate_refines_stat hst2 st2 ->
  hsistate_refines_dyn (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hst1 st1 ->
  hsistate_refines_dyn (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hst2 st2 ->
  sistate_simu dm f st1 st2 ctx.

Lemma siexits_simu_all_fallthrough dm f ctx: forall lse1 lse2,
  siexits_simu dm f lse1 lse2 ctx ->
  all_fallthrough (the_ge1 ctx) (the_sp ctx) lse1 (the_rs0 ctx) (the_m0 ctx) ->
  all_fallthrough (the_ge2 ctx) (the_sp ctx) lse2 (the_rs0 ctx) (the_m0 ctx).
Proof.
  induction 1; [unfold all_fallthrough; contradiction|].
  intros X ext INEXT. eapply all_fallthrough_revcons in X. destruct X as (SEVAL & ALLFU).
  apply IHlist_forall2 in ALLFU.
  destruct H as (CONDSIMU & _).
  inv INEXT; [|eauto].
  erewrite <- CONDSIMU; eauto.
Qed.

Lemma hsiexits_simu_siexits dm f ctx lhse1 lhse2:
  hsiexits_simu dm f ctx lhse1 lhse2 ->
  forall lse1 lse2,
  hsiexits_refines_stat lhse1 lse1 ->
  hsiexits_refines_stat lhse2 lse2 ->
  hsiexits_refines_dyn (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) lhse1 lse1 ->
  hsiexits_refines_dyn (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) lhse2 lse2 ->
  siexits_simu dm f lse1 lse2 ctx.
Proof.
  induction 1.
  - intros. inv H. inv H0. constructor.
  - intros lse1 lse2 SREF1 SREF2 DREF1 DREF2. inv SREF1. inv SREF2. inv DREF1. inv DREF2.
    constructor; [| eapply IHlist_forall2; eauto].
    eapply hsiexit_simu_siexit; eauto.
Qed.

Lemma siexits_simu_all_fallthrough_upto dm f ctx lse1 lse2:
  siexits_simu dm f lse1 lse2 ctx -> forall ext1 lx1,
  all_fallthrough_upto_exit (the_ge1 ctx) (the_sp ctx) ext1 lx1 lse1 (the_rs0 ctx) (the_m0 ctx) ->
  exists ext2 lx2,
    all_fallthrough_upto_exit (the_ge2 ctx) (the_sp ctx) ext2 lx2 lse2 (the_rs0 ctx) (the_m0 ctx)
  /\ length lx1 = length lx2.
Proof.
  induction 1.
  - intros. destruct H as (ITAIL & ALLFU). eapply is_tail_false in ITAIL. contradiction.
  - intros ext1 lx1 ALLFUE.
    destruct ALLFUE as (ITAIL & ALLFU). inv ITAIL.
    + eexists; eexists.
      constructor; [| eapply list_forall2_length; eauto].
      constructor; [econstructor | eapply siexits_simu_all_fallthrough; eauto].
    + exploit IHlist_forall2; [constructor; eauto|].
      intros (ext2 & lx2 & ALLFUE2 & LENEQ).
      eexists; eexists. constructor; eauto.
      eapply all_fallthrough_upto_exit_cons; eauto.
Qed.

Lemma list_forall2_nth_error {A} (l1 l2: list A) P:
  list_forall2 P l1 l2 ->
  forall x1 x2 n,
  nth_error l1 n = Some x1 ->
  nth_error l2 n = Some x2 ->
  P x1 x2.
Proof.
  induction 1.
  - intros. rewrite nth_error_nil in H. discriminate.
  - intros x1 x2 n. destruct n as [|n]; simpl.
    + intros. inv H1. inv H2. assumption.
    + apply IHlist_forall2.
Qed.

Lemma is_tail_length {A} (l1 l2: list A):
  is_tail l1 l2 ->
  (length l1 <= length l2)%nat.
Proof.
  induction l2.
  - intro. destruct l1; auto. apply is_tail_false in H. contradiction.
  - intros ITAIL. inv ITAIL; auto.
    apply IHl2 in H1. clear IHl2. simpl. omega.
Qed.

Lemma is_tail_nth_error {A} (l1 l2: list A) x:
  is_tail (x::l1) l2 ->
  nth_error l2 ((length l2) - length l1 - 1) = Some x.
Proof.
  induction l2.
  - intro ITAIL. apply is_tail_false in ITAIL. contradiction.
  - intros ITAIL. assert (length (a::l2) = S (length l2)) by auto. rewrite H. clear H.
    assert (forall n n', ((S n) - n' - 1)%nat = (n - n')%nat) by (intros; omega). rewrite H. clear H.
    inv ITAIL.
    + assert (forall n, (n - n)%nat = 0%nat) by (intro; omega). rewrite H.
      simpl. reflexivity.
    + exploit IHl2; eauto. intros. clear IHl2.
      assert (forall n n', (n > n')%nat -> (n - n')%nat = S (n - n' - 1)%nat) by (intros; omega).
      exploit (is_tail_length (x::l1)); eauto. intro. simpl in H2.
      assert ((length l2 > length l1)%nat) by omega. clear H2.
      rewrite H0; auto.
Qed.

Theorem hsistate_simu_core_correct dm f hst1 hst2 ctx:
  hsistate_simu_core dm f hst1 hst2 ->
  hsistate_simu dm f hst1 hst2 ctx.
Proof.
  intros SIMUC st1 st2 HREF1 HREF2 DREF1 DREF2 is1 SEMI.
  destruct HREF1 as (PCREF1 & EREF1). destruct HREF2 as (PCREF2 & EREF2).
  destruct DREF1 as (DEREF1 & LREF1). destruct DREF2 as (DEREF2 & LREF2).
  destruct SIMUC as (PCSIMU & ESIMU & LSIMU).
  exploit hsiexits_simu_core_correct; eauto. intro HESIMU.
  unfold ssem_internal in SEMI. destruct (icontinue _) eqn:ICONT.
  - destruct SEMI as (SSEML & PCEQ & ALLFU).
    exploit hsilocal_simu_core_correct; eauto; [apply ctx|]. intro SSEML2.
    exists (mk_istate (icontinue is1) (si_pc st2) (irs is1) (imem is1)). constructor.
    + unfold ssem_internal. simpl. rewrite ICONT. constructor; [assumption | constructor; [reflexivity |]].
      eapply siexits_simu_all_fallthrough; eauto. eapply hsiexits_simu_siexits; eauto.
    + unfold istate_simu. rewrite ICONT. constructor; [simpl; assumption | constructor; [| reflexivity]].
      constructor.
  - destruct SEMI as (ext & lx & SSEME & ALLFU).
    assert (SESIMU: siexits_simu dm f (si_exits st1) (si_exits st2) ctx) by (eapply hsiexits_simu_siexits; eauto).
    exploit siexits_simu_all_fallthrough_upto; eauto. intros (ext2 & lx2 & ALLFU2 & LENEQ).
    assert (EXTSIMU: siexit_simu dm f ctx ext ext2). {
      eapply list_forall2_nth_error; eauto.
      - destruct ALLFU as (ITAIL & _). eapply is_tail_nth_error; eauto.
      - destruct ALLFU2 as (ITAIL & _). eapply is_tail_nth_error in ITAIL.
        assert (LENEQ': length (si_exits st1) = length (si_exits st2)) by (eapply list_forall2_length; eauto).
        congruence. }
    destruct EXTSIMU as (CONDEVAL & EXTSIMU).
    apply EXTSIMU in SSEME. clear EXTSIMU. destruct SSEME as (is2 & SSEME2 & ISIMU).
    exists (mk_istate (icontinue is1) (ipc is2) (irs is2) (imem is2)). constructor.
    + unfold ssem_internal. simpl. rewrite ICONT. exists ext2, lx2. constructor; assumption.
    + unfold istate_simu in *. rewrite ICONT in *. destruct ISIMU as (path & PATHEQ & ISIMULIVE & DMEQ).
      destruct ISIMULIVE as (CONTEQ & REGEQ & MEMEQ).
      exists path. repeat (constructor; auto).
Qed.

(* Definition hfinal_refines hfv fv := forall pge ge sp npc stk f rs0 m0 rs' m' t s',
  ssem_final pge ge sp npc stk f rs0 m0 hfv rs' m' t s' <-> ssem_final pge ge sp npc stk f rs0 m0 fv rs' m' t s'. *)

(* FIXME - might be too strong, let's change it later.. *)
Definition hfinal_refines (hfv fv: sfval) := hfv = fv.

Remark hfinal_refines_snone: hfinal_refines Snone Snone.
Proof.
  reflexivity.
Qed.

Definition hfinal_simu_core (dm: PTree.t node) (f: RTLpath.function) (hf1 hf2: sfval): Prop :=
  match hf1 with
  | Scall sig1 svos1 lsv1 res1 pc1 =>
      match hf2 with
      | Scall sig2 svos2 lsv2 res2 pc2 =>
          dm ! pc2 = Some pc1 /\ sig1 = sig2 /\ svos1 = svos2 /\ lsv1 = lsv2 /\ res1 = res2
      | _ => False
      end
  | Sbuiltin ef1 lbs1 br1 pc1 =>
      match hf2 with
      | Sbuiltin ef2 lbs2 br2 pc2 =>
          dm ! pc2 = Some pc1 /\ ef1 = ef2 /\ lbs1 = lbs2 /\ br1 = br2
      | _ => False
      end
  | Sjumptable sv1 lpc1 =>
      match hf2 with
      | Sjumptable sv2 lpc2 =>
          ptree_get_list dm lpc2 = Some lpc1 /\ sv1 = sv2
      | _ => False
      end
  (* Snone, Stailcall, Sreturn *)
  | _ => hf1 = hf2
  end.

Lemma svident_simu_refl f ctx s:
  svident_simu f ctx s s.
Proof.
  destruct s; constructor; [| reflexivity].
  erewrite <- seval_preserved; [| eapply ctx]. constructor.
Qed.

Theorem hfinal_simu_core_correct dm f ctx opc1 opc2 hf1 hf2 f1 f2:
  hfinal_simu_core dm f hf1 hf2 ->
  hfinal_refines hf1 f1 ->
  hfinal_refines hf2 f2 ->
  dm ! opc2 = Some opc1 ->
  sfval_simu dm f opc1 opc2 ctx f1 f2.
Proof.
  intros CORE FREF1 FREF2 OPCEQ.
  rewrite <- FREF1. rewrite <- FREF2. clear FREF1. clear FREF2. (* FIXME - to change when the refinement is more complex *)
  destruct hf1.
  (* Snone *)
  - simpl in CORE. rewrite <- CORE. constructor. assumption.
  (* Scall *)
  - simpl in CORE. destruct hf2; try contradiction. destruct CORE as (PCEQ & ? & ? & ? & ?). subst.
    constructor; [assumption | apply svident_simu_refl|].
    erewrite <- list_sval_eval_preserved; [| eapply ctx]. constructor.
  (* Stailcall *)
  - simpl in CORE. rewrite <- CORE. constructor; [apply svident_simu_refl|].
    erewrite <- list_sval_eval_preserved; [| eapply ctx]. constructor.
  (* Sbuiltin *)
  - simpl in CORE. destruct hf2; try contradiction. destruct CORE as (PCEQ & ? & ? & ?). subst.
    constructor; [assumption | reflexivity].
  (* Sjumptable *)
  - simpl in CORE. destruct hf2; try contradiction. destruct CORE as (PCEQ & ?). subst.
    constructor; [assumption|].
    erewrite <- seval_preserved; [| eapply ctx]. constructor.
  (* Sreturn *)
  - simpl in CORE. subst. constructor.
Qed.

Record hsstate := { hinternal:> hsistate; hfinal: sfval }.

Definition hsstate_refines (hst: hsstate) (st:sstate): Prop :=
   hsistate_refines_stat (hinternal hst) (internal st)
  /\ (forall ge sp rs0 m0, hsistate_refines_dyn ge sp rs0 m0 (hinternal hst) (internal st))
  /\ hfinal_refines (hfinal hst) (final st).

Definition hsstate_simu_core (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsstate) :=
     hsistate_simu_core dm f (hinternal hst1) (hinternal hst2)
  /\ hfinal_simu_core dm f (hfinal hst1) (hfinal hst2).

Definition hsstate_simu dm f (hst1 hst2: hsstate) ctx: Prop :=
  forall st1 st2,
  hsstate_refines hst1 st1 ->
  hsstate_refines hst2 st2 -> sstate_simu dm f st1 st2 ctx.

Theorem hsstate_simu_core_correct dm f ctx hst1 hst2:
  hsstate_simu_core dm f hst1 hst2 ->
  hsstate_simu dm f hst1 hst2 ctx.
Proof.
  intros (SCORE & FSIMU). intros st1 st2 HREF1 HREF2.
  destruct HREF1 as (SREF1 & DREF1 & FREF1). destruct HREF2 as (SREF2 & DREF2 & FREF2).
  assert (PCEQ: dm ! (hsi_pc hst2) = Some (hsi_pc hst1)) by apply SCORE.
  eapply hsistate_simu_core_correct in SCORE.
  eapply hfinal_simu_core_correct in FSIMU; eauto.
  constructor; [apply SCORE; auto|].
  destruct SREF1 as (PC1 & _). destruct SREF2 as (PC2 & _). rewrite <- PC1. rewrite <- PC2.
  eapply FSIMU.
Qed.

(** * Verificators of *_simu_core properties *)

(* WARNING: ce code va bouger pas mal quand on aura le hash-consing ! *)
Fixpoint sval_simub (sv1 sv2: sval) :=
  match sv1 with
  | Sinput r =>
      match sv2 with
      | Sinput r' => if (Pos.eq_dec r r') then OK tt else Error (msg "sval_simub: Sinput different registers")
      | _ => Error (msg "sval_simub: Sinput expected")
      end
  | Sop op lsv sm =>
      match sv2 with
      | Sop op' lsv' sm' =>
          if (eq_operation op op') then
            do _ <- list_sval_simub lsv lsv';
            smem_simub sm sm'
          else Error (msg "sval_simub: different operations in Sop")
      | _ => Error (msg "sval_simub: Sop expected")
      end
  | Sload sm trap chk addr lsv =>
      match sv2 with
      | Sload sm' trap' chk' addr' lsv' =>
          if (trapping_mode_eq trap trap') then
            if (chunk_eq chk chk') then
              if (eq_addressing addr addr') then
                do _ <- smem_simub sm sm';
                list_sval_simub lsv lsv'
              else Error (msg "sval_simub: addressings do not match")
            else Error (msg "sval_simub: chunks do not match")
          else Error (msg "sval_simub: trapping modes do not match")
          (* FIXME - should be refined once we introduce non trapping loads *)
      | _ => Error (msg "sval_simub: Sload expected")
      end
  end
with list_sval_simub (lsv1 lsv2: list_sval) :=
  match lsv1 with
  | Snil =>
      match lsv2 with
      | Snil => OK tt
      | _ => Error (msg "list_sval_simub: lists of different lengths (lsv2 is bigger)")
      end
  | Scons sv1 lsv1 =>
      match lsv2 with
      | Snil => Error (msg "list_sval_simub: lists of different lengths (lsv1 is bigger)")
      | Scons sv2 lsv2 =>
          do _ <- sval_simub sv1 sv2;
          list_sval_simub lsv1 lsv2
      end
  end
with smem_simub (sm1 sm2: smem) :=
  match sm1 with
  | Sinit =>
      match sm2 with
      | Sinit => OK tt
      | _ => Error (msg "smem_simub: Sinit expected")
      end
  | Sstore sm chk addr lsv sv =>
      match sm2 with
      | Sstore sm' chk' addr' lsv' sv' =>
          if (chunk_eq chk chk') then
            if (eq_addressing addr addr') then
              do _ <- smem_simub sm sm';
              do _ <- list_sval_simub lsv lsv';
              sval_simub sv sv'
            else Error (msg "smem_simub: addressings do not match")
          else Error (msg "smem_simub: chunks not match")
      | _ => Error (msg "smem_simub: Sstore expected")
      end
  end.

Lemma sval_simub_correct sv1: forall sv2,
  sval_simub sv1 sv2 = OK tt -> sv1 = sv2.
Proof.
  induction sv1 using sval_mut with
    (P0 := fun lsv1 => forall lsv2, list_sval_simub lsv1 lsv2 = OK tt -> lsv1 = lsv2)
    (P1 := fun sm1 => forall sm2, smem_simub sm1 sm2 = OK tt -> sm1 = sm2); simpl; auto.
  (* Sinput *)
  - destruct sv2; try discriminate.
    destruct (Pos.eq_dec r r0); [congruence|discriminate].
  (* Sop *)
  - destruct sv2; try discriminate.
    destruct (eq_operation _ _); [|discriminate]. subst.
    intro. explore. apply IHsv1 in EQ. apply IHsv0 in EQ0. congruence.
  (* Sload *)
  - destruct sv2; try discriminate.
    destruct (trapping_mode_eq _ _); [|discriminate].
    destruct (chunk_eq _ _); [|discriminate].
    destruct (eq_addressing _ _); [|discriminate].
    intro. explore. assert (sm = sm0) by auto. assert (lsv = lsv0) by auto.
    congruence.
  (* Snil *)
  - destruct lsv2; [|discriminate]. congruence.
  (* Scons *)
  - destruct lsv2; [discriminate|]. intro. explore.
    apply IHsv1 in EQ. apply IHsv0 in EQ0. congruence.
  (* Sinit *)
  - destruct sm2; [|discriminate]. congruence.
  (* Sstore *)
  - destruct sm2; [discriminate|].
    destruct (chunk_eq _ _); [|discriminate].
    destruct (eq_addressing _ _); [|discriminate].
    intro. explore.
    assert (sm = sm2) by auto. assert (lsv = lsv0) by auto. assert (sv1 = srce) by auto.
    congruence.
Qed.

Lemma list_sval_simub_correct lsv1: forall lsv2,
  list_sval_simub lsv1 lsv2 = OK tt -> lsv1 = lsv2.
Proof.
  induction lsv1; simpl; auto.
  - destruct lsv2; try discriminate. reflexivity.
  - destruct lsv2; try discriminate. intro. explore.
    apply sval_simub_correct in EQ. assert (lsv1 = lsv2) by auto.
    congruence.
Qed.

Lemma smem_simub_correct sm1: forall sm2,
  smem_simub sm1 sm2 = OK tt -> sm1 = sm2.
Proof.
  induction sm1; simpl; auto.
  - destruct sm2; try discriminate. reflexivity.
  - destruct sm2; try discriminate.
    destruct (chunk_eq _ _); [|discriminate].
    destruct (eq_addressing _ _); [|discriminate]. intro. explore.
    apply sval_simub_correct in EQ2. apply list_sval_simub_correct in EQ1.
    apply IHsm1 in EQ. congruence.
Qed.

Definition is_structural {A: Type} (cmp: A -> A -> bool) :=
  forall x y, cmp x y = true -> x = y.

Fixpoint is_part_of {A: Type} (cmp: A -> A -> bool) (elt: A) (lv: list A): bool :=
  match lv with
  | nil => false
  | v::lv => if (cmp elt v) then true else is_part_of cmp elt lv
  end.

Lemma is_part_of_correct {A: Type} cmp lv (e: A):
  is_structural cmp ->
  is_part_of cmp e lv = true ->
  In e lv.
Proof.
  induction lv.
  - intros. simpl in H0. discriminate.
  - intros. simpl in H0. destruct (cmp e a) eqn:CMP.
    + apply H in CMP. subst. constructor; auto.
    + right. apply IHlv; assumption.
Qed.

(* Checks if lv2 is a subset of lv1 *)
Fixpoint is_subsetb {A: Type} (cmp: A -> A -> bool) (lv2 lv1: list A): bool :=
  match lv2 with
  | nil => true
  | v2 :: lv2 => if (is_part_of cmp v2 lv1) then is_subsetb cmp lv2 lv1
                 else false
  end.

Lemma is_subset_cons {A: Type} (x: A) lv lx:
  In x lv /\ is_subset lx lv -> is_subset (x::lx) lv.
Proof.
  intros (ISIN & ISSUB). unfold is_subset.
  intros. inv H.
  - assumption.
  - apply ISSUB. assumption.
Qed.

Lemma is_subset_correct {A: Type} cmp (lv2 lv1: list A):
  is_structural cmp ->
  is_subsetb cmp lv2 lv1 = true ->
  is_subset lv2 lv1.
Proof.
  induction lv2.
  - simpl. intros. intro. intro. apply in_nil in H1. contradiction.
  - intros. simpl in H0. apply is_subset_cons.
    explore. apply is_part_of_correct in EQ; [|assumption].
    apply IHlv2 in H0; [|assumption]. constructor; assumption.
Qed.

Definition simub_bool {A: Type} (simub: A -> A -> res unit) (sv1 sv2: A) :=
  match simub sv1 sv2 with
  | OK tt => true
  | _ => false
  end.

Lemma simub_bool_correct {A: Type} simub (sv1 sv2: A):
  (forall x y, simub x y = OK tt -> x = y) ->
  simub_bool simub sv1 sv2 = true -> sv1 = sv2.
Proof.
  intros. unfold simub_bool in H0. destruct (simub sv1 sv2) eqn:SIMU; explore.
  - apply H. assumption.
  - discriminate.
Qed.

Definition hsilocal_simu_coreb hst1 hst2 :=
  if (is_subsetb (simub_bool smem_simub) (hsi_lsmem hst2) (hsi_lsmem hst1)) then
    if (is_subsetb (simub_bool sval_simub) (hsi_ok_lsval hst2) (hsi_ok_lsval hst1)) then
      (* TODO - compare on the whole ptree *) OK tt
    else Error (msg "hsi_ok_lsval sets aren't included")
  else Error (msg "hsi_lsmem sets aren't included").

Theorem hsilocal_simu_coreb_correct hst1 hst2:
  hsilocal_simu_coreb hst1 hst2 = OK tt ->
  hsilocal_simu_core hst1 hst2.
Proof.
Admitted.

(* Definition hsiexit_simub (dm: PTree.t node) (f: RTLpath.function) (hse1 hse2: hsistate_exit) :=
  if (eq_condition (hsi_cond hse1) (hsi_cond hse2)) then
    do _ <- list_sval_simub (hsi_scondargs hse1) (hsi_scondargs hse2);
    do _ <- hsilocal_simub dm f (hsi_elocal hse1) (hsi_elocal hse2);
    revmap_check_single dm (hsi_ifso hse1) (hsi_ifso hse2)
  else Error (msg "siexit_simub: conditions do not match")
. *)

(* Fixpoint hsiexits_simub (dm: PTree.t node) (f: RTLpath.function) (lhse1 lhse2: list hsistate_exit) :=
  match lhse1 with
  | nil =>
      match lhse2 with
      | nil => OK tt
      | _ => Error (msg "siexists_simub: sle1 and sle2 lengths do not match")
      end
  | hse1 :: lhse1 =>
      match lhse2 with
      | nil => Error (msg "siexits_simub: sle1 and sle2 lengths do not match")
      | hse2 :: lhse2 =>
          do _ <- hsiexit_simub dm f hse1 hse2;
          do _ <- hsiexits_simub dm f lhse1 lhse2;
          OK tt
      end
  end. *)

(* Lemma hsiexits_simub_correct dm f ctx lhse1: forall lhse2,
  hsiexits_simub dm f lhse1 lhse2 = OK tt ->
  hsiexits_simu dm f ctx lhse1 lhse2.
Proof.
(*   induction lhse1.
  - simpl. intros. destruct lhse2; try discriminate. intros se1 se2 HEREFS1 HEREFS2 _ _.
    inv HEREFS1. inv HEREFS2. constructor.
  - (* simpl. *) unfold hsiexits_simub. intros. destruct lhse2; try discriminate. explore.
    fold hsiexits_simub in EQ1.
    eapply hsiexit_simub_correct in EQ. apply IHlhse1 in EQ1.
    intros se1 se2 HEREFS1 HEREFS2 HEREFD1 HEREFD2. inv HEREFS1. inv HEREFS2. inv HEREFD1. inv HEREFD2. constructor; auto.
    apply EQ1; assumption. *)
Admitted.
 *)

(* TODO *)
Definition hsiexits_simu_coreb (dm: PTree.t node) (f: RTLpath.function) (lhse1 lhse2: list hsistate_exit) := OK tt.

Theorem hsiexits_simu_coreb_correct dm f lhse1 lhse2:
  hsiexits_simu_coreb dm f lhse1 lhse2 = OK tt ->
  hsiexits_simu_core dm f lhse1 lhse2.
Proof.
Admitted.

Definition hsistate_simu_coreb (dm: PTree.t node) (f: RTLpath.function) (hse1 hse2: hsistate) := OK tt. (* TODO *)

Theorem hsistate_simu_coreb_correct dm f hse1 hse2:
  hsistate_simu_coreb dm f hse1 hse2 = OK tt ->
  hsistate_simu_core dm f hse1 hse2.
Proof.
Admitted.

Definition hsstate_simu_coreb (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsstate) := OK tt. (* TODO *)

Theorem hsstate_simu_coreb_correct dm f hst1 hst2:
  hsstate_simu_coreb dm f hst1 hst2 = OK tt ->
  hsstate_simu_core dm f hst1 hst2.
Proof.
Admitted.

Definition hfinal_simu_coreb (dm: PTree.t node) (f: RTLpath.function) (hf1 hf2: sfval) := OK tt. (* TODO *)

Theorem hfinal_simu_coreb_correct dm f hf1 hf2:
  hfinal_simu_coreb dm f hf1 hf2 = OK tt ->
  hfinal_simu_core dm f hf1 hf2.
Proof.
Admitted.

Lemma hsistate_refines_stat_pceq st hst:
  hsistate_refines_stat hst st ->
  (hsi_pc hst) = (si_pc st).
Proof.
  unfold hsistate_refines_stat; intuition.
Qed.

Lemma hsistate_refines_dyn_local_refines ge sp rs0 m0 hst st:
   hsistate_refines_dyn ge sp rs0 m0 hst st ->
   hsilocal_refines ge sp rs0 m0 (hsi_local hst) (si_local st).
Proof.
  unfold hsistate_refines_dyn; intuition.
Qed.



Local Hint Resolve hsistate_refines_dyn_local_refines: core.



(** * Symbolic execution of one internal step 
  TODO: to refine symbolic values/symbolic memories with hash-consed symbolic values
*)

(** ** Assignment of memory *)
Definition hslocal_set_smem (hst:hsistate_local) (sm:smem) :=
  {| hsi_lsmem := sm::hsi_lsmem hst;
     hsi_ok_lsval := hsi_ok_lsval hst;
     hsi_sreg:= hsi_sreg hst
  |}.

Lemma sok_local_set_mem ge sp rs0 m0 st sm:
  sok_local ge sp rs0 m0 (slocal_set_smem st sm) 
  <-> (sok_local ge sp rs0 m0 st /\ seval_smem ge sp sm rs0 m0 <> None).
Proof.
  unfold slocal_set_smem, sok_local; simpl; intuition (subst; eauto).
Qed.

Lemma hsok_local_set_mem ge sp rs0 m0 hst sm:
  hsok_local ge sp rs0 m0 (hslocal_set_smem hst sm)
  <-> (hsok_local ge sp rs0 m0 hst /\ seval_smem ge sp sm rs0 m0 <> None).
Proof.
  unfold hslocal_set_smem, hsok_local; simpl; intuition (subst; eauto).
Qed.

Lemma hslocal_set_mem_correct ge sp rs0 m0 hst st hsm sm:
  hsilocal_refines ge sp rs0 m0 hst st ->
  (hsok_local ge sp rs0 m0 hst -> seval_smem ge sp hsm rs0 m0 = seval_smem ge sp sm rs0 m0) ->
  hsilocal_refines ge sp rs0 m0 (hslocal_set_smem hst hsm) (slocal_set_smem st sm).
Proof.
  intros LOCREF. intros SMEMEQ.
  destruct LOCREF as (OKEQ & SMEMEQ' & REGEQ). constructor; [| constructor ].
  - rewrite hsok_local_set_mem.
    rewrite sok_local_set_mem.
    constructor.
    + intros (OKL & SMEMN). constructor. 2: rewrite SMEMEQ; auto.
      all: rewrite <- OKEQ; assumption.
    + intros (HOKL & HSMEM). rewrite OKEQ. constructor; auto.
      rewrite <- SMEMEQ; auto.
  - rewrite! hsok_local_set_mem. intros (HOKL & HSMEM).
    simpl. apply SMEMEQ; assumption.
  - rewrite hsok_local_set_mem. intros (HOKL & HSMEM).
    simpl. intuition congruence.
Qed.

(** ** Assignment of local state *)

Definition hsist_set_local (hst: hsistate) (pc: node) (hnxt: hsistate_local): hsistate :=
   {| hsi_pc := pc; hsi_exits := hst.(hsi_exits); hsi_local:= hnxt |}.

Lemma hsist_set_local_correct_stat hst st pc hnxt nxt:
  hsistate_refines_stat hst st ->
  hsistate_refines_stat (hsist_set_local hst pc hnxt) (sist_set_local st pc nxt).
Proof.
  unfold hsistate_refines_stat; simpl; intuition.
Qed.

Lemma hsist_set_local_correct_dyn ge sp rs0 m0 hst st pc hnxt nxt:
  hsistate_refines_dyn ge sp rs0 m0 hst st ->
  hsilocal_refines ge sp rs0 m0 hnxt nxt ->
  hsistate_refines_dyn ge sp rs0 m0 (hsist_set_local hst pc hnxt) (sist_set_local st pc nxt).
Proof.
  unfold hsistate_refines_dyn; simpl; intuition.
Qed.

(** ** Assignment of registers *)

(* locally new symbolic values during symbolic execution *)
Inductive root_sval: Type :=
| Rop (op:operation)
| Rload (trap: trapping_mode) (chunk:memory_chunk) (addr:addressing)
.

Definition root_apply (rsv: root_sval) (lsv: list sval) (sm: smem): sval :=
  match rsv with
  | Rop op => Sop op (list_sval_inj lsv) sm
  | Rload trap chunk addr => Sload sm trap chunk addr (list_sval_inj lsv)
  end.
Coercion root_apply: root_sval >-> Funclass.

Local Open Scope lazy_bool_scope.

(* NB: return [false] if the rsv cannot fail *)
Definition may_trap (rsv: root_sval) (lsv: list sval) (sm: smem): bool :=
  match rsv with 
  | Rop op => is_trapping_op op ||| negb (Nat.eqb (length lsv) (args_of_operation op))  (* cf. lemma is_trapping_op_sound *)
  | Rload TRAP _ _  => true
  | _ => false
  end.

Lemma lazy_orb_negb_false (b1 b2:bool):
  (b1 ||| negb b2) = false <-> (b1 = false /\ b2 = true).
Proof.
  unfold negb; explore; simpl; intuition (try congruence).
Qed.

(* not used yet *)
Lemma may_trap_correct (ge: RTL.genv) (sp:val) (rsv: root_sval) (rs0: regset) (m0: mem) (lsv: list sval) (sm: smem):
  may_trap rsv lsv sm = false -> 
  seval_list_sval ge sp (list_sval_inj lsv) rs0 m0 <> None ->
  seval_smem ge sp sm rs0 m0 <> None ->
  seval_sval ge sp (rsv lsv sm) rs0 m0 <> None.
Proof.
  destruct rsv; simpl; try congruence.
  - rewrite lazy_orb_negb_false. intros (TRAP1 & TRAP2) OK1 OK2.
    explore; try congruence.
    eapply is_trapping_op_sound; eauto.
    admit. (* TODO *)
  - intros X OK1 OK2.
    explore; try congruence.
Admitted.

(* simplify a symbolic value before assignment to a register *)
Definition simplify (rsv: root_sval) lsv sm: sval :=
  match rsv with
  | Rload TRAP chunk addr => Sload sm NOTRAP chunk addr (list_sval_inj lsv)
  | Rop op =>
     match is_move_operation op lsv with
     | Some arg => arg  (* optimization of Omove *)
     | None => 
       if op_depends_on_memory op then
          rsv lsv sm
       else
          Sop op (list_sval_inj lsv) Sinit (* magically remove the dependency on sm ! *)
     end
  | _ => rsv lsv sm
  end.

Lemma simplify_correct (rsv: root_sval) lsv sm (ge: RTL.genv) (sp:val) (rs0: regset) (m0: mem) v:
  seval_sval ge sp (rsv lsv sm) rs0 m0 = Some v ->
  seval_sval ge sp (simplify rsv lsv sm) rs0 m0 = Some v.
Proof.
  destruct rsv; simpl; auto.
  - (* Rop *)
    destruct (seval_list_sval _ _ _ _) as [args|] eqn: Hargs; try congruence.
    destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
    intros Hv.
    destruct (is_move_operation _ _) eqn: Hmove.
    + exploit is_move_operation_correct; eauto.
      intros (Hop & Hlsv); subst; simpl in *.
      explore. auto.
    + clear Hmove; destruct (op_depends_on_memory op) eqn: Hop; simpl; explore; try congruence.
      inversion Hargs; subst.
      erewrite op_depends_on_memory_correct; eauto.
  - (* Rload *)
    destruct trap; simpl; auto.
    destruct (seval_list_sval _ _ _ _) as [args|] eqn: Hargs; try congruence.
    destruct (eval_addressing _ _ _ _) as [a|] eqn: Ha; try congruence.
    destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
    intros H; rewrite H; auto.
Qed.

Definition red_PTree_set (r:reg) (sv: sval) (hst: PTree.t sval): PTree.t sval :=
  match sv with
  | Sinput r' =>
     if Pos.eq_dec r r' 
     then PTree.remove r' hst
     else PTree.set r sv hst
  | _ => PTree.set r sv hst
  end.

Lemma red_PTree_set_correct (r:reg) (sv: sval) (hst: PTree.t sval) ge sp rs0 m0:
  hsi_sreg_eval ge sp (red_PTree_set r sv hst) r rs0 m0 = hsi_sreg_eval ge sp (PTree.set r sv hst) r rs0 m0.
Proof.
  destruct sv; simpl; auto.
  destruct (Pos.eq_dec r r0); auto.
  subst; unfold hsi_sreg_eval.
  rewrite PTree.grs, PTree.gss; simpl; auto.
Qed.

(* naive version:
@Cyril: éventuellement, tu peux utiliser la version naive dans un premier temps pour simplifier les preuves...

Definition naive_hslocal_set_sreg (hst:hsistate_local) (r:reg) (rsv:root_sval) lsv sm :=
  let sv := rsv lsv sm in
  {| hsi_lsmem := hsi_lsmem hst;
     hsi_ok_lsval := sv::(hsi_ok_lsval hst);
     hsi_sreg:= PTree.set r sv (hsi_sreg hst) |}.
*)

Definition hslocal_set_sreg (hst:hsistate_local) (r:reg) (rsv:root_sval) lsv sm :=
  {| hsi_lsmem := hsi_lsmem hst;
     hsi_ok_lsval := if may_trap rsv lsv sm then (rsv lsv sm)::(hsi_ok_lsval hst) else hsi_ok_lsval hst;
     hsi_sreg := red_PTree_set r (simplify rsv lsv sm) (hsi_sreg hst) |}.

Definition ok_args ge sp rs0 m0 hst lsv sm :=
  hsok_local ge sp rs0 m0 hst -> 
  (seval_list_sval ge sp (list_sval_inj lsv) rs0 m0 <> None /\ seval_smem ge sp sm rs0 m0 <> None).

Lemma hslocal_set_sreg_correct ge sp rs0 m0 hst st r (rsv:root_sval) lsv sm sv':
  hsilocal_refines ge sp rs0 m0 hst st ->
  (forall ge sp rs0 m0,
  ok_args ge sp rs0 m0 hst lsv sm ->
  (hsok_local ge sp rs0 m0 hst -> seval_sval ge sp sv' rs0 m0 = seval_sval ge sp (rsv lsv sm) rs0 m0) ) ->
  hsilocal_refines ge sp rs0 m0 (hslocal_set_sreg hst r rsv lsv sm) (slocal_set_sreg st r sv').
Admitted.

(** ** Execution of one instruction *)

Definition hsiexec_inst (i: instruction) (hst: hsistate): option hsistate := 
  match i with
  | Inop pc' => 
      Some (hsist_set_local hst pc' hst.(hsi_local))
  | Iop op args dst pc' =>
      let prev := hst.(hsi_local) in
      let vargs := List.map (hsi_sreg_get prev) args in
      let next := hslocal_set_sreg prev dst (Rop op) vargs (hsi_smem_get prev) in
      Some (hsist_set_local hst pc' next)
  | Iload trap chunk addr args dst pc' =>
      let prev := hst.(hsi_local) in
      let vargs := List.map (hsi_sreg_get prev) args in
      let next := hslocal_set_sreg prev dst (Rload trap chunk addr) vargs (hsi_smem_get prev) in
      Some (hsist_set_local hst pc' next)
  | Istore chunk addr args src pc' =>
      let prev := hst.(hsi_local) in
      let vargs := list_sval_inj (List.map (hsi_sreg_get prev) args) in
      let next := hslocal_set_smem prev (Sstore (hsi_smem_get prev) chunk addr vargs (hsi_sreg_get prev src)) in
      Some (hsist_set_local hst pc' next)
   | Icond cond args ifso ifnot _ =>
      let prev := hst.(hsi_local) in
      let vargs := list_sval_inj (List.map (hsi_sreg_get prev) args) in
      let ex := {| hsi_cond:=cond; hsi_scondargs:=vargs; hsi_elocal := prev; hsi_ifso := ifso |} in
      Some {| hsi_pc := ifnot; hsi_exits := ex::hst.(hsi_exits); hsi_local := prev |}
  | _ => None (* TODO jumptable ? *)
  end.

Local Hint Resolve hsist_set_local_correct_stat
  hsist_set_local_correct_dyn hslocal_set_mem_correct: core.

Lemma seval_sval_refines ge sp rs0 m0 hst st p:
  hsok_local ge sp rs0 m0 hst ->
  hsilocal_refines ge sp rs0 m0 hst st ->
  seval_sval ge sp (hsi_sreg_get hst p) rs0 m0 = seval_sval ge sp (si_sreg st p) rs0 m0.
Proof.
  intros OKL HREF. destruct HREF as (_ & _ & RSEQ).
  rewrite <- hsi_sreg_eval_correct; eauto.
Qed.

Lemma seval_list_sval_refines ge sp rs0 m0 hst st l:
  hsok_local ge sp rs0 m0 hst ->
  hsilocal_refines ge sp rs0 m0 hst st ->
  seval_list_sval ge sp (list_sval_inj (map (hsi_sreg_get hst) l)) rs0 m0 =
  seval_list_sval ge sp (list_sval_inj (map (si_sreg st) l)) rs0 m0.
Proof.
  intros OKL HLREF. destruct HLREF as (_ & _ & RSEQ).
  induction l; simpl; auto.
  erewrite <- RSEQ; auto.
  rewrite IHl. 
  rewrite <- hsi_sreg_eval_correct.
  reflexivity.
Qed.

Lemma seval_smem_refines ge sp rs0 m0 hst st :
  hsok_local ge sp rs0 m0 hst ->
  hsilocal_refines ge sp rs0 m0 hst st ->
  seval_smem ge sp (hsi_smem_get hst) rs0 m0 = seval_smem ge sp (si_smem st) rs0 m0.
Proof.
  intros OKL HLREF. destruct HLREF as (_ & MSEQ & _).
  rewrite <- hsi_smem_eval_correct.
  auto.
Qed.

Lemma seval_condition_refines hst st ge sp cond args rs m:
  hsok_local ge sp rs m hst ->
  hsilocal_refines ge sp rs m hst st ->
  seval_condition ge sp cond args (hsi_smem_get hst) rs m
  = seval_condition ge sp cond args (si_smem st) rs m.
 Proof.
  intros HOK (OKEQ & MEMEQ & RSEQ). unfold seval_condition.
  rewrite <- MEMEQ; auto. rewrite hsi_smem_eval_correct. reflexivity.
Qed.

Lemma hsiexec_inst_correct_None i hst st:
  hsiexec_inst i hst = None -> siexec_inst i st = None.
Proof.
  destruct i; simpl; congruence.
Qed.


Lemma hsiexec_inst_correct_stat i hst hst' st:
  hsiexec_inst i hst = Some hst' ->
  exists st', siexec_inst i st = Some st'
  /\ (hsistate_refines_stat hst st -> hsistate_refines_stat hst' st').
Proof.
 destruct i; simpl; intros STEPI; inversion_clear STEPI; discriminate || eexists; split; eauto.
 (* TODO *)
Admitted.

Lemma hsiexec_inst_correct_dyn ge sp rs0 m0 i hst st hst' st':
  hsiexec_inst i hst = Some hst' ->
  siexec_inst i st = Some st' ->
  hsistate_refines_dyn ge sp rs0 m0 hst st -> hsistate_refines_dyn ge sp rs0 m0 hst' st'.
Proof.
  destruct i; simpl; intros STEP1 STEP2; inversion_clear STEP1;
    inversion_clear STEP2; discriminate || (intro REF; eauto).
  - (* Iop *)
    eapply hsist_set_local_correct_dyn; eauto.
    eapply hslocal_set_sreg_correct; eauto.
    + simpl. admit. (* TODO *)
  - (* Iload *)
    eapply hsist_set_local_correct_dyn; eauto.
    eapply hslocal_set_sreg_correct; eauto.
    + simpl. admit. (* TODO *)
  - (* Istore *)
    eapply hsist_set_local_correct_dyn; eauto.
    eapply hslocal_set_mem_correct; eauto.
    intros. simpl.
    erewrite seval_list_sval_refines; eauto.
    erewrite seval_smem_refines; eauto.
    erewrite seval_sval_refines; eauto.
  - (* Icond *)
    admit. (* TODO *)
Admitted.


Fixpoint hsiexec_path (path:nat) (f: function) (hst: hsistate): option hsistate :=
  match path with
  | O => Some hst
  | S p =>
    SOME i <- (fn_code f)!(hst.(hsi_pc)) IN
    SOME hst1 <- hsiexec_inst i hst IN
    hsiexec_path p f hst1
  end.

Lemma hsiexec_path_correct_stat ps f hst hst' st:
  hsiexec_path ps f hst = Some hst' -> 
  hsistate_refines_stat hst st ->
  exists st', siexec_path ps f st = Some st' /\ hsistate_refines_stat hst' st'.
Proof.
Admitted.

Lemma hsiexec_path_correct_dyn ge sp rs0 m0 ps f hst hst' st st':
  hsiexec_path ps f hst = Some hst' -> 
  siexec_path ps f st = Some st' ->
  hsistate_refines_stat hst st ->
  hsistate_refines_stat hst' st' ->
  hsistate_refines_dyn ge sp rs0 m0 hst st 
  -> hsistate_refines_dyn ge sp rs0 m0 hst' st'.
Proof.
Admitted.


Definition hsexec_final (i: instruction) (prev: hsistate_local): sfval := 
  match i with
  | Icall sig ros args res pc => 
    let svos := sum_left_map (hsi_sreg_get prev) ros in
    let sargs := list_sval_inj (List.map (hsi_sreg_get prev) args) in
    Scall sig svos sargs res pc
  | Itailcall sig ros args =>
    let svos := sum_left_map (hsi_sreg_get prev) ros in
    let sargs := list_sval_inj (List.map (hsi_sreg_get prev) args) in
    Stailcall sig svos sargs
  | Ibuiltin ef args res pc =>
    let sargs := List.map (builtin_arg_map (hsi_sreg_get prev)) args in
    Sbuiltin ef sargs res pc
  | Ireturn or => 
    let sor := SOME r <- or IN Some (hsi_sreg_get prev r) in
    Sreturn sor
  | Ijumptable reg tbl =>
    let sv := hsi_sreg_get prev reg in
    Sjumptable sv tbl
  | _ => Snone
  end.

(* Lemma local_refines_sreg_get hsl sl ge sp rs0 m0:
  hsistate_local_refines hsl sl ->
  sok_local ge sp sl rs0 m0 ->
  hsi_sreg_get hsl = si_sreg sl.
Proof.
  intros HREF SOKL. apply functional_extensionality. intro r.
  destruct (HREF ge sp rs0 m0) as (OKEQ & MEMEQ & RSEQ).
  apply OKEQ in SOKL. pose (RSEQ SOKL r) as EQ.
  unfold hsi_sreg_get. 
Admitted. *)

Lemma sfind_function_conserves hsl sl pge ge sp s rs0 m0:
  hsilocal_refines ge sp rs0 m0 hsl sl ->
  sfind_function pge ge sp (sum_left_map (hsi_sreg_get hsl) s) rs0 m0 =
  sfind_function pge ge sp (sum_left_map (si_sreg sl) s) rs0 m0.
Admitted.

Lemma hsexec_final_correct hsl sl i:
  (forall ge sp rs0 m0, hsilocal_refines ge sp rs0 m0 hsl sl) ->
  hsexec_final i hsl = sexec_final i sl.
Proof.
(*   destruct i; simpl; intros HLREF; try (apply hfinal_refines_snone).
  (* Scall *)
  - constructor.
    + intro. inv H. constructor; auto.
      ++ erewrite <- sfind_function_conserves; eauto.
      ++ erewrite <- seval_list_sval_refines; eauto.
    + intro. inv H. constructor; auto.
      ++ erewrite sfind_function_conserves; eauto.
      ++ erewrite seval_list_sval_refines; eauto.
  (* Stailcall *)
  - admit.
  (* Sbuiltin *)
  - admit.
  (* Sjumptable *)
  - admit.
  (* Sreturn *)
  - admit. *)
Admitted.


Definition init_hsistate_local := {| hsi_lsmem := Sinit::nil;
    hsi_ok_lsval := nil; hsi_sreg := PTree.empty sval |}.

Remark init_hsistate_local_correct ge sp rs0 m0:
  hsilocal_refines ge sp rs0 m0 init_hsistate_local init_sistate_local.
Proof.
  constructor; constructor; simpl.
  - intro. destruct H as (_ & SMEM & SVAL). constructor; [contradiction|].
    intros. destruct H; [|contradiction]. subst. discriminate. 
  - intro. destruct H as (SVAL & SMEM). constructor; [simpl; auto|].
    constructor; simpl; discriminate.
  - intros; simpl; reflexivity.
  - intros. simpl. unfold hsi_sreg_eval. rewrite PTree.gempty. reflexivity.
Qed.

Definition init_hsistate pc := {| hsi_pc := pc; hsi_exits := nil; hsi_local := init_hsistate_local |}.

Remark init_hsistate_correct_stat pc:
  hsistate_refines_stat (init_hsistate pc) (init_sistate pc).
Proof.
  constructor; constructor; simpl; auto.
Qed.

Remark init_hsistate_correct_dyn ge sp rs0 m0 pc:
  hsistate_refines_dyn ge sp rs0 m0 (init_hsistate pc) (init_sistate pc).
Proof.
  constructor; simpl; auto.
  - apply list_forall2_nil.
  - apply init_hsistate_local_correct.
Qed.

Definition hsexec (f: function) (pc:node): option hsstate :=
  SOME path <- (fn_path f)!pc IN
  SOME hst <- hsiexec_path path.(psize) f (init_hsistate pc) IN
  SOME i <- (fn_code f)!(hst.(hsi_pc)) IN
  Some (match hsiexec_inst i hst with
       | Some hst' => {| hinternal := hst'; hfinal := Snone |}
       | None => {| hinternal := hst; hfinal := hsexec_final i hst.(hsi_local) |}
       end).

Local Hint Resolve init_hsistate_correct_stat init_hsistate_correct_dyn hsexec_final_correct
  hsiexec_inst_correct_dyn hsiexec_path_correct_dyn hfinal_refines_snone: core.

Lemma hsexec_correct f pc hst:
  hsexec f pc = Some hst ->
  exists st, sexec f pc = Some st /\ hsstate_refines hst st.
Proof.
  unfold hsexec. intro. explore_hyp.
  unfold sexec. 
  rewrite EQ.
  exploit hsiexec_path_correct_stat; eauto.
  intros (st0 & SPATH & REF0).
  generalize REF0; intros (PC0 & XREF0). rewrite SPATH.
  erewrite <- PC0. rewrite EQ1.
  destruct (hsiexec_inst i h) eqn:HINST.
  + exploit hsiexec_inst_correct_stat; eauto.
    intros (st1 & EQ2 & PC2 & REF2).
    - split; eauto. 
    - rewrite EQ2.
      repeat (econstructor; simpl; eauto).
  + erewrite hsiexec_inst_correct_None; eauto.
    repeat (econstructor; simpl; eauto).
    unfold hfinal_refines. simpl; eauto.
Qed.

(** * The simulation test of concrete symbolic execution *)

Definition revmap_check_single (dm: PTree.t node) (n tn: node) : res unit :=
  match dm ! tn with
  | None => Error (msg "revmap_check_single: no mapping for tn")
  | Some res => if (Pos.eq_dec n res) then OK tt
                else Error (msg "revmap_check_single: n and res do not match")
  end.

Lemma revmap_check_single_correct dm n tn:
  revmap_check_single dm n tn = OK tt ->
  dm ! tn = Some n.
Proof.
  unfold revmap_check_single. explore; try discriminate. congruence.
Qed.


Local Hint Resolve genv_match ssem_local_refines_hok: core.

Fixpoint revmap_check_list (dm: PTree.t node) (ln ln': list node): res unit :=
  match ln with
  | nil =>
      match ln' with
      | nil => OK tt
      | _ => Error (msg "revmap_check_list: lists have different lengths")
      end
  | n::ln =>
      match ln' with
      | nil => Error (msg "revmap_check_list: lists have different lengths")
      | n'::ln' => do _ <- revmap_check_single dm n n'; revmap_check_list dm ln ln'
      end
  end.

Lemma revmap_check_list_correct dm ln: forall ln',
  revmap_check_list dm ln ln' = OK tt ->
  ptree_get_list dm ln' = Some ln.
Proof.
  induction ln.
  - simpl. intros. destruct ln'; try discriminate. constructor; auto.
  - simpl. intros; destruct ln'; try discriminate. explore.
    apply IHln in EQ0. apply revmap_check_single_correct in EQ.
    simpl. rewrite EQ. rewrite EQ0. reflexivity.
Qed.

Definition svos_simub (svos1 svos2: sval + ident) :=
  match svos1 with
  | inl sv1 =>
      match svos2 with
      | inl sv2 => sval_simub sv1 sv2
      | _ => Error (msg "svos_simub: expected sval")
      end
  | inr id1 =>
      match svos2 with
      | inr id2 =>
          if (ident_eq id1 id2) then OK tt
          else Error (msg "svos_simub: ids do not match")
      | _ => Error (msg "svos_simub: expected id")
      end
  end.

Lemma svos_simub_correct svos1 svos2:
  svos_simub svos1 svos2 = OK tt ->
  svos1 = svos2.
Proof.
  destruct svos1.
  - simpl. destruct svos2; [|discriminate].
    intro. exploit sval_simub_correct; eauto. congruence.
  - simpl. destruct svos2; [discriminate|].
    intro. explore. reflexivity.
Qed.

Fixpoint builtin_arg_simub (bs bs': builtin_arg sval) :=
  match bs with
  | BA sv =>
      match bs' with
      | BA sv' => sval_simub sv sv'
      | _ => Error (msg "builtin_arg_simub: BA expected")
      end
  | BA_int n =>
      match bs' with
      | BA_int n' => if (Integers.int_eq n n') then OK tt else Error (msg "builtin_arg_simub: integers do not match")
      | _ => Error (msg "buitin_arg_simub: BA_int expected")
      end
  | BA_long n =>
      match bs' with
      | BA_long n' => if (int64_eq n n') then OK tt else Error (msg "builtin_arg_simub: integers do not match")
      | _ => Error (msg "buitin_arg_simub: BA_long expected")
      end
  | BA_float f =>
      match bs' with
      | BA_float f' => if (float_eq f f') then OK tt else Error (msg "builtin_arg_simub: floats do not match")
      | _ => Error (msg "builtin_arg_simub: BA_float expected")
      end
  | BA_single f =>
      match bs' with
      | BA_single f' => if (float32_eq f f') then OK tt else Error (msg "builtin_arg_simub: floats do not match")
      | _ => Error (msg "builtin_arg_simub: BA_single expected")
      end
  | BA_loadstack chk ptr =>
      match bs' with
      | BA_loadstack chk' ptr' =>
          if (chunk_eq chk chk') then
            if (ptrofs_eq ptr ptr') then OK tt
            else Error (msg "builtin_arg_simub: ptr do not match")
          else Error (msg "builtin_arg_simub: chunks do not match")
      | _ => Error (msg "builtin_arg_simub: BA_loadstack expected")
      end
  | BA_addrstack ptr =>
      match bs' with
      | BA_addrstack ptr' => if (ptrofs_eq ptr ptr') then OK tt else Error (msg "builtin_arg_simub: ptr do not match")
      | _ => Error (msg "builtin_arg_simub: BA_addrstack expected")
      end
  | BA_loadglobal chk id ofs =>
      match bs' with
      | BA_loadglobal chk' id' ofs' =>
          if (chunk_eq chk chk') then
            if (ident_eq id id') then
              if (ptrofs_eq ofs ofs') then OK tt
              else Error (msg "builtin_arg_simub: offsets do not match")
            else Error (msg "builtin_arg_simub: identifiers do not match")
          else Error (msg "builtin_arg_simub: chunks do not match")
      | _ => Error (msg "builtin_arg_simub: BA_loadglobal expected")
      end
  | BA_addrglobal id ofs =>
      match bs' with
      | BA_addrglobal id' ofs' =>
          if (ident_eq id id') then
            if (ptrofs_eq ofs ofs') then OK tt
            else Error (msg "builtin_arg_simub: offsets do not match")
          else Error (msg "builtin_arg_simub: identifiers do not match")
      | _ => Error (msg "builtin_arg_simub: BA_addrglobal expected")
      end
  | BA_splitlong lo hi =>
      match bs' with
      | BA_splitlong lo' hi' => do _ <- builtin_arg_simub lo lo'; builtin_arg_simub hi hi'
      | _ => Error (msg "builtin_arg_simub: BA_splitlong expected")
      end
  | BA_addptr b1 b2 =>
      match bs' with
      | BA_addptr b1' b2' => do _ <- builtin_arg_simub b1 b1'; builtin_arg_simub b2 b2'
      | _ => Error (msg "builtin_arg_simub: BA_addptr expected")
      end
  end.

Lemma builtin_arg_simub_correct b1: forall b2,
  builtin_arg_simub b1 b2 = OK tt -> b1 = b2.
Proof.
  induction b1; simpl; destruct b2; try discriminate; auto; intros; try (explore; congruence).
  - apply sval_simub_correct in H. congruence.
  - explore. assert (b1_1 = b2_1) by auto. assert (b1_2 = b2_2) by auto. congruence.
  - explore. assert (b1_1 = b2_1) by auto. assert (b1_2 = b2_2) by auto. congruence.
Qed.

Fixpoint list_builtin_arg_simub lbs1 lbs2 :=
  match lbs1 with
  | nil =>
      match lbs2 with
      | nil => OK tt
      | _ => Error (msg "list_builtin_arg_simub: lists of different lengths (lbs2 is bigger)")
      end
  | bs1::lbs1 =>
      match lbs2 with
      | nil => Error (msg "list_builtin_arg_simub: lists of different lengths (lbs1 is bigger)")
      | bs2::lbs2 =>
          do _ <- builtin_arg_simub bs1 bs2;
          list_builtin_arg_simub lbs1 lbs2
      end
  end.

Lemma list_builtin_arg_simub_correct lsb1: forall lsb2,
  list_builtin_arg_simub lsb1 lsb2 = OK tt -> lsb1 = lsb2.
Proof.
  induction lsb1; intros; simpl; destruct lsb2; try discriminate; auto.
  simpl in H. explore. apply builtin_arg_simub_correct in EQ.
  assert (lsb1 = lsb2) by auto. congruence.
Qed.

(* WARNING: ce code va bouger pas mal quand on aura le hash-consing ! *)
Definition sfval_simub (dm: PTree.t node) (f: RTLpath.function) (pc1 pc2: node) (fv1 fv2: sfval) :=
  match fv1 with
  | Snone =>
      match fv2 with
      | Snone => revmap_check_single dm pc1 pc2
      | _ => Error (msg "sfval_simub: Snone expected")
      end
  | Scall sig svos lsv res pc1 =>
      match fv2 with
      | Scall sig2 svos2 lsv2 res2 pc2 =>
          do _ <- revmap_check_single dm pc1 pc2;
          if (signature_eq sig sig2) then
            if (Pos.eq_dec res res2) then
              do _ <- svos_simub svos svos2;
              list_sval_simub lsv lsv2
            else Error (msg "sfval_simub: Scall res do not match")
          else Error (msg "sfval_simub: Scall different signatures")
      | _ => Error (msg "sfval_simub: Scall expected")
      end
  | Stailcall sig svos lsv =>
      match fv2 with
      | Stailcall sig' svos' lsv' =>
          if (signature_eq sig sig') then
            do _ <- svos_simub svos svos';
            list_sval_simub lsv lsv'
          else Error (msg "sfval_simub: signatures do not match")
      | _ => Error (msg "sfval_simub: Stailcall expected")
      end
  | Sbuiltin ef lbs br pc =>
      match fv2 with
      | Sbuiltin ef' lbs' br' pc' =>
          if (external_function_eq ef ef') then
            if (builtin_res_eq_pos br br') then
              do _ <- revmap_check_single dm pc pc';
              list_builtin_arg_simub lbs lbs'
            else Error (msg "sfval_simub: builtin res do not match")
          else Error (msg "sfval_simub: external functions do not match")
      | _ => Error (msg "sfval_simub: Sbuiltin expected")
      end
  | Sjumptable sv ln =>
      match fv2 with
      | Sjumptable sv' ln' =>
          do _ <- revmap_check_list dm ln ln'; sval_simub sv sv'
      | _ => Error (msg "sfval_simub: Sjumptable expected")
      end
  | Sreturn osv =>
      match fv2 with
      | Sreturn osv' =>
          match osv with
          | Some sv =>
              match osv' with
              | Some sv' => sval_simub sv sv'
              | None => Error (msg "sfval_simub sv' expected")
              end
          | None =>
              match osv' with
              | Some sv' => Error (msg "None expected")
              | None => OK tt
              end
          end
      | _ => Error (msg "sfval_simub: Sreturn expected")
      end
  end.

Lemma sfval_simub_correct dm f pc1 pc2 fv1 fv2 ctx:
  sfval_simub dm f pc1 pc2 fv1 fv2 = OK tt ->
  sfval_simu dm f pc1 pc2 ctx fv1 fv2.
Proof.
  unfold sfval_simub. destruct fv1.
  (* Snone *)
  - destruct fv2; try discriminate. intro.
    apply revmap_check_single_correct in H. constructor; auto.
  (* Scall *)
  - destruct fv2; try discriminate. intro. explore.
    apply svos_simub_correct in EQ3. apply list_sval_simub_correct in EQ4.
    subst. apply revmap_check_single_correct in EQ. constructor; auto.
    + admit.
    + admit.
  (* Stailcall *)
  - destruct fv2; try discriminate. intro. explore.
    apply svos_simub_correct in EQ0. apply list_sval_simub_correct in EQ1.
    subst. constructor; auto.
    + admit.
    + admit.
  (* Sbuiltin *)
  - destruct fv2; try discriminate. intro. explore.
    apply revmap_check_single_correct in EQ1. apply list_builtin_arg_simub_correct in EQ2.
    subst. constructor; auto.
  (* Sjumptable *)
  - destruct fv2; try discriminate. intro. explore.
    apply revmap_check_list_correct in EQ. apply sval_simub_correct in EQ0. subst.
    constructor; auto.
    admit.
  (* Sreturn *)
  - destruct fv2; try discriminate. destruct o; destruct o0; try discriminate.
    + intro. apply sval_simub_correct in H. subst. constructor; auto.
    + constructor; auto.
Admitted.

Definition simu_check_single (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) (m: node * node) :=
  let (pc2, pc1) := m in
  match (hsexec f pc1) with
  | None => Error (msg "simu_check_single: hsexec f pc1 failed")
  | Some hst1 =>
      match (hsexec tf pc2) with
      | None => Error (msg "simu_check_single: hsexec tf pc2 failed")
      | Some hst2 => hsstate_simu_coreb dm f hst1 hst2
      end
  end.

Lemma simu_check_single_correct dm tf f pc1 pc2:
  simu_check_single dm f tf (pc2, pc1) = OK tt ->
  sexec_simu dm f tf pc1 pc2.
Proof.
  unfold simu_check_single. intro.
  unfold sexec_simu.
  intros st1 SEXEC.
  explore.
  exploit hsexec_correct; eauto.
  intros (st2 & SEXEC2 & REF2).
  clear EQ0. (* now, useless in principle and harmful for the next [exploit] *)
  exploit hsexec_correct; eauto.
  intros (st0 & SEXEC1 & REF1).
  rewrite SEXEC1 in SEXEC; inversion SEXEC; subst.
  eexists; split; eauto.
  intros ctx. eapply hsstate_simu_coreb_correct in H.
  eapply hsstate_simu_core_correct; eauto.
Qed.

Fixpoint simu_check_rec (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) lm :=
  match lm with
  | nil => OK tt
  | m :: lm => do u1 <- simu_check_single dm f tf m;
               do u2 <- simu_check_rec dm f tf lm;
               OK tt
  end.

Lemma simu_check_rec_correct dm f tf pc1 pc2: forall lm,
  simu_check_rec dm f tf lm = OK tt ->
  In (pc2, pc1) lm ->
  sexec_simu dm f tf pc1 pc2.
Proof.
  induction lm.
  - simpl. intuition.
  - simpl. intros. explore. destruct H0.
    + subst. eapply simu_check_single_correct; eauto.
    + eapply IHlm; assumption.
Qed.

Definition simu_check (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) := 
   simu_check_rec dm f tf (PTree.elements dm).

Lemma simu_check_correct dm f tf:
  simu_check dm f tf = OK tt ->
  forall pc1 pc2, dm ! pc2 = Some pc1 ->
  sexec_simu dm f tf pc1 pc2.
Proof.
  unfold simu_check. intros. eapply PTree.elements_correct in H0.
  eapply simu_check_rec_correct; eassumption.
Qed.