Merge branch 'mppa-RTLpathSE-verif' into mppa-RTLpathSE-verif-hash-junk

2 files changed, 528 insertions, 224 deletions

diff --git a/kvx/lib/RTLpathSE_impl.v b/kvx/lib/RTLpathSE_impl.v
index 294867c0..965f8578 100644
--- a/kvx/lib/RTLpathSE_impl.v
+++ b/kvx/lib/RTLpathSE_impl.v
@@ -14,9 +14,7 @@ Local Open Scope option_monad_scope.
 
 (** * TODO: refine symbolic values/symbolic memories with hash-consed symbolic values *)
 
-(** * Implementation of local symbolic internal states 
-TODO: use refined symbolic values instead of those from RTLpathSE_theory.
-*)
+(** * Implementation of local symbolic internal states *)
 
 (** name : Hash-consed Symbolic Internal state local. Later on we will use the
     refinement to introduce hash consing *)
@@ -77,43 +75,448 @@ Definition sok_local (ge: RTL.genv) (sp:val) (rs0: regset) (m0: mem) (st: sistat
   /\ 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.
+
+(*
+Lemma sok_local_no_abort ge sp rs0 m0 st:
+  sok_local ge sp rs0 m0 st -> sabort_local ge sp st rs0 m0 -> False.
+Proof.
+  unfold sok_local, sabort_local. 
+  intros (H1 & H2 & H3) [A1 | [A2 | (r & A3)]]; intuition eauto.
+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 hsistate_local_refines ge sp rs0 m0 (hst: hsistate_local) (st: sistate_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 hsilocal_simu_core (hst1 hst2: hsistate_local) :=
+     (forall sm, List.In sm (hsi_lsmem hst2) -> List.In sm (hsi_lsmem hst1))
+  /\ (forall sv, List.In sv (hsi_ok_lsval hst2) -> List.In sv (hsi_ok_lsval hst1))
+  /\ (forall r, hsi_sreg_get hst2 r = hsi_sreg_get hst1 r)
+  /\ hsi_smem_get hst1 = hsi_smem_get hst2.
+
+Definition hsilocal_simu_coreb (hst1 hst2: hsistate_local) := OK tt.
+
+Theorem hsilocal_simu_coreb_correct hst1 hst2:
+  hsilocal_simu_coreb hst1 hst2 = OK tt ->
+  hsilocal_simu_core hst1 hst2.
+Proof.
+Admitted.
+
+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 hsistate_exit_refines_stat (hext: hsistate_exit) (ext: sistate_exit): Prop :=
-  hsi_cond hext = si_cond ext
-  /\ hsi_scondargs hext = si_scondargs ext
+Definition hsiexit_refines_stat (hext: hsistate_exit) (ext: sistate_exit): Prop :=
+     hsi_cond hext = si_cond ext
   /\ hsi_ifso hext = si_ifso ext.
 
-Definition hsistate_exit_refines_dyn ge sp rs0 m0 (hext: hsistate_exit) (ext: sistate_exit): Prop :=
-   hsistate_local_refines ge sp rs0 m0 (hsi_elocal hext) (si_elocal 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)
+   /\ (hsok_exit ge sp rs0 m0 hext -> 
+        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 ->
+  hsok_exit (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse1 ->
+  hsiexit_simu dm f ctx hse1 hse2.
+Proof.
+  intros SIMUC HOK1 st1 st2 HREF1 HREF2 HDYN1 HDYN2.
+  exploit hsiexit_simu_core_nofail. 2: eapply ctx. all: eauto. intro HOK2.
+  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.
+  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.
+
+Inductive hsok_exits ge sp rs m: list hsistate_exit -> Prop :=
+  | hsok_exits_nil: hsok_exits ge sp rs m nil
+  | hsok_exits_cons: forall he lhe,
+      hsok_exits ge sp rs m lhe ->
+      hsok_exit ge sp rs m he ->
+      hsok_exits ge sp rs m (he::lhe).
+
+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.
+
+(* 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.
+
+Theorem hsiexits_simu_core_correct dm f lhse1 lhse2 ctx:
+  hsiexits_simu_core dm f lhse1 lhse2 ->
+  hsok_exits (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) lhse1 ->
+  hsiexits_simu dm f ctx lhse1 lhse2.
+Proof.
+  induction 1; [constructor|].
+  intros HOKS. inv HOKS. 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_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 hsistate_refines_stat (hst: hsistate) (st:sistate): Prop :=
   hsi_pc hst = si_pc st
-  /\ list_forall2 hsistate_exit_refines_stat (hsi_exits hst) (si_exits st).
+  /\ hsiexits_refines_stat (hsi_exits hst) (si_exits st).
 
 Definition hsistate_refines_dyn ge sp rs0 m0 (hst: hsistate) (st:sistate): Prop :=
-     list_forall2 (hsistate_exit_refines_dyn ge sp rs0 m0) (hsi_exits hst) (si_exits st)
-  /\ hsistate_local_refines ge sp rs0 m0 (hsi_local hst) (si_local st).
+     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.
+
+Definition hsok ge sp rs m hst := 
+     hsok_exits ge sp rs m (hsi_exits hst)
+  /\ hsok_local ge sp rs m (hsi_local hst).
+
+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 ->
+  hsok (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hst1 ->
+  hsistate_simu dm f hst1 hst2 ctx.
+Proof.
+  intros SIMUC HOK 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). destruct HOK as (EOK1 & LOK1).
+  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 - 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.
+
+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 hst1 = hfinal hst2.
+
+Definition hok ge sp rs m hst := hsok ge sp rs m (hinternal hst).
+
+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.
+
+Remark sfval_simu_reflexive dm f ctx pc1 pc2 hf:
+  dm ! pc2 = Some pc1 ->
+  sfval_simu dm f pc1 pc2 ctx hf hf.
+Proof.
+  intro DMEQ. destruct hf.
+  - constructor; auto.
+  - constructor; auto.
+Abort. (* theorem not true !! *)
+
+Theorem hsstate_simu_core_correct dm f ctx hst1 hst2:
+  hsstate_simu_core dm f hst1 hst2 ->
+  hok (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hst1 ->
+  hsstate_simu dm f hst1 hst2 ctx.
+Proof.
+  intros (SCORE & FSIMU) HOK1. 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; [|eassumption].
+  constructor; [apply SCORE; auto|].
+(*   rewrite <- FREF1. rewrite <- FREF2. rewrite FSIMU. (* FIXME - not that simple *)
+  apply sfval_simu_reflexive.
+  destruct SREF1 as (PC1 & _). destruct SREF2 as (PC2 & _). congruence. *)
+Admitted.
 
 Lemma hsistate_refines_stat_pceq st hst:
   hsistate_refines_stat hst st ->
@@ -124,13 +527,15 @@ Qed.
 
 Lemma hsistate_refines_dyn_local_refines ge sp rs0 m0 hst st:
    hsistate_refines_dyn ge sp rs0 m0 hst st ->
-   hsistate_local_refines ge sp rs0 m0 (hsi_local hst) (si_local 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
 *)
@@ -157,9 +562,9 @@ Proof.
 Qed.
 
 Lemma hslocal_set_mem_correct ge sp rs0 m0 hst st hsm sm:
-  hsistate_local_refines ge sp rs0 m0 hst st ->
+  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) ->
-  hsistate_local_refines ge sp rs0 m0 (hslocal_set_smem hst hsm) (slocal_set_smem st sm).
+  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 ].
@@ -190,7 +595,7 @@ 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 ->
-  hsistate_local_refines ge sp rs0 m0 hnxt nxt ->
+  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.
@@ -260,7 +665,8 @@ Definition simplify (rsv: root_sval) lsv sm: sval :=
   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.
+  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 *)
@@ -320,11 +726,11 @@ Definition ok_args ge sp rs0 m0 hst lsv sm :=
   (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':
-  hsistate_local_refines ge sp rs0 m0 hst st ->
+  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) ) ->
-  hsistate_local_refines ge sp rs0 m0 (hslocal_set_sreg hst r rsv lsv sm) (slocal_set_sreg st r sv').
+  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 *)
@@ -356,11 +762,12 @@ Definition hsiexec_inst (i: instruction) (hst: hsistate): option hsistate :=
   | _ => None (* TODO jumptable ? *)
   end.
 
-Local Hint Resolve hsist_set_local_correct_stat hsist_set_local_correct_dyn hslocal_set_mem_correct: core.
+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 ->
-  hsistate_local_refines ge sp rs0 m0 hst st ->
+  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).
@@ -369,7 +776,7 @@ Qed.
 
 Lemma seval_list_sval_refines ge sp rs0 m0 hst st l:
   hsok_local ge sp rs0 m0 hst ->
-  hsistate_local_refines ge sp rs0 m0 hst st ->
+  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.
@@ -383,7 +790,7 @@ Qed.
 
 Lemma seval_smem_refines ge sp rs0 m0 hst st :
   hsok_local ge sp rs0 m0 hst ->
-  hsistate_local_refines ge sp rs0 m0 hst st ->
+  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 & _).
@@ -391,6 +798,16 @@ Proof.
   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.
@@ -400,7 +817,8 @@ 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').
+  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 *)
@@ -411,7 +829,8 @@ Lemma hsiexec_inst_correct_dyn ge sp rs0 m0 i hst st hst' st':
   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).
+  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.
@@ -458,22 +877,6 @@ Lemma hsiexec_path_correct_dyn ge sp rs0 m0 ps f hst hst' st st':
 Proof.
 Admitted.
 
-(* 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 - too strong let's change it later.. *)
-Definition hfinal_refines (hfv fv: sfval) := hfv = fv.
-
-Remark hfinal_refines_snone: hfinal_refines Snone Snone.
-Proof.
-Admitted.
-
-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 hsexec_final (i: instruction) (prev: hsistate_local): sfval := 
   match i with
@@ -509,13 +912,13 @@ Proof.
 Admitted. *)
 
 Lemma sfind_function_conserves hsl sl pge ge sp s rs0 m0:
-  hsistate_local_refines ge sp rs0 m0 hsl sl ->
+  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, hsistate_local_refines ge sp rs0 m0 hsl sl) ->
+  (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).
@@ -538,10 +941,11 @@ Proof.
 Admitted.
 
 
-Definition init_hsistate_local := {| hsi_lsmem := Sinit::nil; hsi_ok_lsval := nil; hsi_sreg := PTree.empty sval |}.
+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:
-  hsistate_local_refines ge sp rs0 m0 init_hsistate_local init_sistate_local.
+  hsilocal_refines ge sp rs0 m0 init_hsistate_local init_sistate_local.
 Proof.
   constructor; constructor; simpl.
   - intro. destruct H as (_ & SMEM & SVAL). constructor; [contradiction|].
@@ -577,7 +981,8 @@ Definition hsexec (f: function) (pc:node): option hsstate :=
        | 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.
+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 ->
@@ -606,10 +1011,18 @@ Qed.
 (* TODO - generalize it with a list of registers to test ? *)
 Definition hsilocal_simub (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsistate_local) := OK tt.
 
+(* (* TODO: voilà les conditions que hsilocal_simub doit garantir *)
+Definition hsilocal_simu_core (hst1 hst2: hsistate_local):=
+    forall sm, List.In sm (hsi_lsmem hst2) -> List.In sm (hsi_lsmem hst1)
+ /\ forall sv, List.In sv (hsi_ok_lsval hst2) -> List.In sv (hsi_ok_lsval hst1)
+ /\ forall r, hsi_sreg_get hst2 r = hsi_sreg_get hst1 r.
+
+*)
+
 Definition hsilocal_simu dm f (hst1 hst2: hsistate_local) (ctx: simu_proof_context f): Prop := forall st1 st2,
-  hsistate_local_refines (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hst1 st1 ->
-  hsistate_local_refines (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hst2 st2 ->
-  silocal_simu dm f st1 st2 ctx.
+  hsilocal_refines (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hst1 st1 ->
+  hsilocal_refines (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hst2 st2 ->
+  silocal_simu dm f st1 st2 ctx. 
 
 Lemma hsilocal_simub_correct dm f hst1 hst2:
   hsilocal_simub dm f hst1 hst2 = OK tt ->
@@ -760,62 +1173,51 @@ Definition hsiexit_simub (dm: PTree.t node) (f: RTLpath.function) (hse1 hse2: hs
   else Error (msg "siexit_simub: conditions do not match")
 .
 
-Definition hsok_exit ge sp rs m hse := hsok_local ge sp rs m (hsi_elocal hse).
+(* Definition hsiexit_simu dm f hse1 hse2 (ctx: simu_proof_context f): 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. *)
 
-Definition hsiexit_simu dm f hse1 hse2 (ctx: simu_proof_context f): Prop := forall se1 se2,
-  hsistate_exit_refines_stat hse1 se1 ->
-  hsistate_exit_refines_stat hse2 se2 ->
-  hsistate_exit_refines_dyn (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse1 se1 ->
-  hsistate_exit_refines_dyn (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse2 se2 ->
-  hsok_exit (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse1 ->
-  hsok_exit (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse2 ->
-  siexit_simu dm f ctx se1 se2.
-
-Lemma seval_condition_refines hst st ge sp cond args rs m:
-  hsok_local ge sp rs m hst ->
-  hsistate_local_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.
-
-Local Hint Resolve genv_match: core.
+Local Hint Resolve genv_match ssem_local_refines_hok: core.
 
 Lemma hsiexit_simub_correct dm f hse1 hse2:
   hsiexit_simub dm f hse1 hse2 = OK tt ->
-  forall ctx, hsiexit_simu dm f hse1 hse2 ctx.
+  forall ctx, hsiexit_simu dm f ctx hse1 hse2.
 Proof.
-  unfold hsiexit_simub. intro. explore.
+(*   unfold hsiexit_simub. intro. explore.
   apply list_sval_simub_correct in EQ0. exploit hsilocal_simub_eq; eauto.
   intros (SREGEQ & SMEMEQ) ctx.
   eapply hsilocal_simub_correct in EQ2.
   apply revmap_check_single_correct in EQ3.
-  intros se1 se2 (HCOND1 & HARGS1 & HIFSO1) (HCOND2 & HARGS2 & HIFSO2) HLREF1 HLREF2 HOK1 HOK2.
-  unfold hsistate_exit_refines_dyn in *.
+  intros se1 se2 HIFSO1 HIFSO2 (HLREF1 & HCOND1) (HLREF2 & HCOND2).
+  unfold hsiexit_refines_stat in *.
+  intros is1 (SCOND & SLOCAL & SIFSO).
   constructor.
-  - unfold siexit_simu_ssem. intros is SEMEXIT.
-    destruct SEMEXIT as (SCOND & SLOCAL & SIFSO).
-    let H0 := fresh "SLOCAL" in assert (H0 := SLOCAL).
+  - rewrite <- HCOND1; eauto.
+    rewrite <- HCOND2; eauto.
+    rewrite SMEMEQ, EQ0, e. 
+    eapply seval_condition_preserved; eauto.
+    assert (X: hsok_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (hsi_elocal hse1) -> 
+                 hsok_local (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (hsi_elocal hse2)).
+    + admit. (* TODO: on doit savoir ça du fait que l'état symbolique de hse2 simule celui de hse1 *)
+    + eauto.
+  - let H0 := fresh "SLOCAL" in assert (H0 := SLOCAL).
     eapply EQ2 in SLOCAL0; eauto. destruct SLOCAL0 as (is2 & SLOCAL' & ISIMU).
     destruct is2 as [icont ipc irs imem]. simpl in *.
     exists (mk_istate icont (si_ifso se2) irs imem). simpl.
     constructor; auto.
     + repeat (constructor; auto).
-      rewrite <- HARGS2. rewrite <- EQ0.
-      rewrite <- HCOND2. rewrite <- e.
-      erewrite <- seval_condition_refines; eauto. rewrite <- SMEMEQ.
+      rewrite <- HCOND2; eauto.
+      rewrite <- e, <- EQ0, <- SMEMEQ.
       erewrite seval_condition_preserved; eauto.
-      rewrite HARGS1. rewrite HCOND1. erewrite seval_condition_refines; eauto.
-    + unfold istate_simu in *. destruct (icontinue is) eqn:ICONT.
+      rewrite HCOND1; eauto.
+    + unfold istate_simu in *. destruct (icontinue is1) eqn:ICONT.
       * destruct ISIMU as (A & B & C). constructor; auto.
       * destruct ISIMU as (path & PATHEQ & ISIMU & REVEQ). exists path.
-        repeat (constructor; auto). simpl in *. congruence.
-  - rewrite <- HARGS2. rewrite <- HCOND2. erewrite <- seval_condition_refines; eauto.
-    rewrite <- HARGS1. rewrite <- HCOND1. erewrite <- seval_condition_refines; eauto.
-    rewrite SMEMEQ, EQ0, e. 
-    eapply seval_condition_preserved; eauto.
-Qed.
+        repeat (constructor; auto). simpl in *. congruence. *)
+Admitted.
 
 Fixpoint hsiexits_simub (dm: PTree.t node) (f: RTLpath.function) (lhse1 lhse2: list hsistate_exit) :=
   match lhse1 with
@@ -834,135 +1236,47 @@ Fixpoint hsiexits_simub (dm: PTree.t node) (f: RTLpath.function) (lhse1 lhse2: l
       end
   end.
 
-Inductive hsok_exits ge sp rs m: list hsistate_exit -> Prop :=
-  | hsok_exits_nil: hsok_exits ge sp rs m nil
-  | hsok_exits_cons: forall l ex, hsok_exits ge sp rs m l -> hsok_exit ge sp rs m ex -> hsok_exits ge sp rs m (ex::l)
-  .
-
-Definition hsiexits_simu dm f (hse1 hse2: list hsistate_exit) (ctx: simu_proof_context f): Prop := forall se1 se2,
-  list_forall2 hsistate_exit_refines_stat hse1 se1 ->
-  list_forall2 hsistate_exit_refines_stat hse2 se2 ->
-  list_forall2 (hsistate_exit_refines_dyn (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx)) hse1 se1 ->
-  list_forall2 (hsistate_exit_refines_dyn (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx)) hse2 se2 ->
-  hsok_exits (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse1 ->
-  hsok_exits (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse2 ->
-  siexits_simu dm f se1 se2 ctx.
-
 Lemma hsiexits_simub_correct dm f ctx lhse1: forall lhse2,
   hsiexits_simub dm f lhse1 lhse2 = OK tt ->
-  hsiexits_simu dm f lhse1 lhse2 ctx.
+  hsiexits_simu dm f ctx lhse1 lhse2.
 Proof.
-  induction lhse1.
-  - simpl. intros. destruct lhse2; try discriminate. intros se1 se2 HEREFS1 HEREFS2 _ _ _ _.
+(*   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 HOK1 HOK2.
-    inv HEREFS1. inv HEREFS2. inv HEREFD1. inv HEREFD2. inv HOK1. inv HOK2. constructor; auto.
-    apply EQ1; assumption.
-Qed.
+    intros se1 se2 HEREFS1 HEREFS2 HEREFD1 HEREFD2. inv HEREFS1. inv HEREFS2. inv HEREFD1. inv HEREFD2. constructor; auto.
+    apply EQ1; assumption. *)
+Admitted.
 
 Definition hsistate_simub (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsistate) :=
   do _ <- hsilocal_simub dm f (hsi_local hst1) (hsi_local hst2);
   do _ <- hsiexits_simub dm f (hsi_exits hst1) (hsi_exits hst2);
   OK tt.
 
-Definition hsok_internal ge sp rs m hst :=
-  hsok_exits ge sp rs m (hsi_exits hst) /\ hsok_local ge sp rs m (hsi_local hst).
-
-Definition hsistate_simu dm f (hst1 hst2: hsistate) (ctx: simu_proof_context f): Prop := forall st1 st2,
+(* 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 ->
-  hsok_internal (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hst1 ->
-  hsok_internal (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hst2 ->
-  sistate_simu dm f st1 st2 ctx.
+  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 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.
 
 (* Very adapted from sistate_simub_correct ---> should delete sistate_simub_correct after *)
 Lemma hsistate_simub_correct dm f hst1 hst2:
   hsistate_simub dm f hst1 hst2 = OK tt ->
   forall ctx, hsistate_simu dm f hst1 hst2 ctx.
 Proof.
-  unfold hsistate_simub. intro. explore. unfold hsistate_simu.
-  intros ctx st1 st2 (PCEQ1 & HEREFD1) (PCEQ2 & HEREFD2)
-    (HREF1 & HLREF1) (HREF2 & HLREF2) (HOKE1 & HOKL1) (HOKE2 & HOKL2) is1 SEMI.
+(*   unfold hsistate_simub. intro. explore. unfold hsistate_simu.
+  intros ctx st1 st2 (PCEQ1 & HEREFD1) (PCEQ2 & HEREFD2) (HREF1 & HLREF1) (HREF2 & HLREF2) is1 SEMI.
   exploit hsiexits_simub_correct; eauto. intro ESIMU.
   unfold ssem_internal in SEMI. destruct (icontinue _) eqn:ICONT.
   - destruct SEMI as (SSEML & PCEQ & ALLFU).
@@ -982,29 +1296,22 @@ Proof.
       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. }
+        assert (LENEQ': length (si_exits st1) = length (si_exits st2)) by (eapply list_forall2_length; eauto).
+        congruence. } *)
+Admitted.
+(*
     destruct EXTSIMU as (SEMSIMU & _). eapply SEMSIMU in SSEME; eauto.
     destruct SSEME as (is2 & SSEME2 & ISIMU).
-    unfold istate_simu in ISIMU. rewrite ICONT in ISIMU.
-    destruct ISIMU as (path & PATHEQ & SIMULIVE & REVBIND).
+    unfold istate_simu in ISIMU. rewrite ICONT in ISIMU. destruct ISIMU as (path & PATHEQ & SIMULIVE & REVBIND).
     destruct SIMULIVE as (CONTEQ & REGLIVE & MEMEQ).
     unfold ssem_internal. exists is2.
     rewrite <- CONTEQ. rewrite ICONT. constructor; auto.
     + eexists; eexists; constructor; eauto.
     + unfold istate_simu. rewrite ICONT. eexists. repeat (constructor; eauto).
 Qed.
+*)
 
-Definition hsok ge sp rs m hst := hsok_internal ge sp rs m (hinternal hst).
 
-Definition hsstate_simu dm f (hst1 hst2: hsstate) ctx: Prop :=
-  forall st1 st2,
-  hsstate_refines hst1 st1 ->
-  hsstate_refines hst2 st2 ->
-  hsok (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hst1 ->
-  hsok (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hst2 ->
-  sstate_simu f dm st1 st2 ctx.
 
 Fixpoint revmap_check_list (dm: PTree.t node) (ln ln': list node): res unit :=
   match ln with
@@ -1241,16 +1548,14 @@ Proof.
   - 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.
-    + destruct svos0; constructor; [| reflexivity ].
-      erewrite <- seval_preserved; eauto. constructor.
-    + erewrite <- list_sval_eval_preserved; eauto. constructor.
+    + 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.
-    + destruct s2; constructor; [| reflexivity].
-      erewrite <- seval_preserved; eauto. constructor.
-    + erewrite <- list_sval_eval_preserved; eauto. constructor.
+    + admit.
+    + admit.
   (* Sbuiltin *)
   - destruct fv2; try discriminate. intro. explore.
     apply revmap_check_single_correct in EQ1. apply list_builtin_arg_simub_correct in EQ2.
@@ -1258,12 +1563,13 @@ Proof.
   (* Sjumptable *)
   - destruct fv2; try discriminate. intro. explore.
     apply revmap_check_list_correct in EQ. apply sval_simub_correct in EQ0. subst.
-    constructor; auto. erewrite <- seval_preserved; eauto. constructor.
+    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.
-Qed.
+Admitted.
 
 Definition hsstate_simub (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsstate) :=
   do u1 <- hsistate_simub dm f (hinternal hst1) (hinternal hst2);
@@ -1272,11 +1578,11 @@ Definition hsstate_simub (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hs
 
 Lemma hsstate_simub_correct dm f hst1 hst2 ctx:
   hsstate_simub dm f hst1 hst2 = OK tt ->
-  hsstate_simu f dm hst1 hst2 ctx.
+  hsstate_simu dm f hst1 hst2 ctx.
 Proof.
   unfold hsstate_simub. intro. explore.
   eapply sfval_simub_correct in EQ1. eapply hsistate_simub_correct in EQ.
-  intros st1 st2 (SREF1 & LREF1 & FREF1) (SREF2 & LREF2 & FREF2) HOK1 HOK2.
+  intros st1 st2 (SREF1 & LREF1 & FREF1) (SREF2 & LREF2 & FREF2).
   constructor; [eauto |].
   destruct SREF1 as (PCEQ1 & _ ). destruct SREF2 as (PCEQ2 & _ ).
   rewrite <- PCEQ1. rewrite <- PCEQ2. rewrite <- FREF1. rewrite <- FREF2.
@@ -1311,8 +1617,7 @@ Proof.
   rewrite SEXEC1 in SEXEC; inversion SEXEC; subst.
   eexists; split; eauto.
   intros; eapply hsstate_simub_correct; eauto.
-  all: admit. (* FIXME - le raffinement n'est prouvé correct que dans le cas où on ne fail pas *)
-Admitted.
+Qed.
 
 Fixpoint simu_check_rec (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) lm :=
   match lm with
diff --git a/kvx/lib/RTLpathSE_theory.v b/kvx/lib/RTLpathSE_theory.v
index e81a107e..81351f6a 100644
--- a/kvx/lib/RTLpathSE_theory.v
+++ b/kvx/lib/RTLpathSE_theory.v
@@ -1757,21 +1757,20 @@ Here are intermediate definitions.
 *)
 
 Definition silocal_simu (dm: PTree.t node) (f: RTLpath.function) (sl1 sl2: sistate_local) (ctx: simu_proof_context f): Prop :=
-    forall is1, ssem_local (the_ge1 ctx) (the_sp ctx) sl1 (the_rs0 ctx) (the_m0 ctx) (irs is1) (imem is1) -> 
+    forall is1, ssem_local (the_ge1 ctx) (the_sp ctx) sl1 (the_rs0 ctx) (the_m0 ctx) (irs is1) (imem is1) ->
     exists is2, ssem_local (the_ge2 ctx) (the_sp ctx) sl2 (the_rs0 ctx) (the_m0 ctx) (irs is2) (imem is2)
                 /\ istate_simu f dm is1 is2.
 
-Definition siexit_simu_ssem (dm: PTree.t node) (f: RTLpath.function) (se1 se2: sistate_exit) (ctx: simu_proof_context f):=
-  forall is1, ssem_exit (the_ge1 ctx) (the_sp ctx) se1 (the_rs0 ctx) (the_m0 ctx) (irs is1) (imem is1) (ipc is1) ->
-  exists is2,
-     ssem_exit (the_ge2 ctx) (the_sp ctx) se2 (the_rs0 ctx) (the_m0 ctx) (irs is2) (imem is2) (ipc is2)
-  /\ istate_simu f dm is1 is2.
-
 Definition siexit_simu (dm: PTree.t node) (f: RTLpath.function) (ctx: simu_proof_context f) (se1 se2: sistate_exit) :=
-  siexit_simu_ssem dm f se1 se2 ctx 
-  /\
-  seval_condition (the_ge1 ctx) (the_sp ctx) (si_cond se1) (si_scondargs se1) (si_smem (si_elocal se1)) (the_rs0 ctx) (the_m0 ctx) 
-   = seval_condition (the_ge2 ctx) (the_sp ctx) (si_cond se2) (si_scondargs se2) (si_smem (si_elocal se2)) (the_rs0 ctx) (the_m0 ctx).
+    (seval_condition (the_ge1 ctx) (the_sp ctx) (si_cond se1) (si_scondargs se1) 
+      (si_smem (si_elocal se1)) (the_rs0 ctx) (the_m0 ctx)) 
+  = (seval_condition (the_ge2 ctx) (the_sp ctx) (si_cond se2) (si_scondargs se2)
+      (si_smem (si_elocal se2)) (the_rs0 ctx) (the_m0 ctx))
+  /\ forall is1,
+      ssem_exit (the_ge1 ctx) (the_sp ctx) se1 (the_rs0 ctx) (the_m0 ctx) (irs is1) (imem is1) (ipc is1) ->
+      exists is2,
+          ssem_exit (the_ge2 ctx) (the_sp ctx) se2 (the_rs0 ctx) (the_m0 ctx) (irs is2) (imem is2) (ipc is2)
+      /\  istate_simu f dm is1 is2.
 
 Definition siexits_simu (dm: PTree.t node) (f: RTLpath.function) (lse1 lse2: list sistate_exit) (ctx: simu_proof_context f) :=
   list_forall2 (siexit_simu dm f ctx) lse1 lse2.