starting to merge with Cyril's proof

1 files changed, 773 insertions, 48 deletions

diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v
index 3b8088d4..50bdd7a6 100644
--- a/kvx/lib/RTLpathSE_impl_junk.v
+++ b/kvx/lib/RTLpathSE_impl_junk.v
@@ -192,7 +192,7 @@ Record hsistate := { hsi_pc: node; hsi_exits: list hsistate_exit; hsi_local: hsi
 (** ** Syntax and Semantics of symbolic state *)
 Record hsstate := { hinternal:> hsistate; hfinal: hsfval }.
 
-(** ** Refinement Definitions: from refinement of symbolic values, memories, local/exit/internal/symbolic. *)
+(** ** Refinement Definitions: from refinement of symbolic values, memories, local/exit/internal/final. *)
 
 Fixpoint hsval_proj hsv :=
   match hsv with
@@ -219,21 +219,6 @@ Local Notation "'seval_list_hsval' ge sp lhv" := (seval_list_sval ge sp (hsval_l
 Local Notation "'seval_hsmem' ge sp hsm" := (seval_smem ge sp (hsmem_proj hsm))
   (only parsing, at level 0, ge at next level, sp at next level, hsm at next level).
 
-Lemma hseval_preserved ge ge' rs0 m0 sp hsv:
-  (forall s, Genv.find_symbol ge' s = Genv.find_symbol ge s) ->
-  seval_hsval ge sp hsv rs0 m0 = seval_hsval ge' sp hsv rs0 m0.
-Proof.
-  intros; eapply seval_preserved; eauto.
-Qed.
-
-Lemma hsmem_eval_preserved ge ge' rs0 m0 sp hsm:
-  (forall s, Genv.find_symbol ge' s = Genv.find_symbol ge s) ->
-  seval_hsmem ge sp hsm rs0 m0 = seval_hsmem ge' sp hsm rs0 m0.
-Proof.
-  intros; eapply smem_eval_preserved; eauto.
-Qed.
-
-
 Local Notation "'sval_refines' ge sp rs0 m0 hv sv" := (seval_hsval ge sp hv rs0 m0 = seval_sval ge sp sv rs0 m0)
   (only parsing, at level 0, ge at next level, sp at next level, rs0 at next level, m0 at next level, hv at next level, sv at next level).
 
@@ -243,12 +228,14 @@ Local Notation "'list_sval_refines' ge sp rs0 m0 lhv lsv" := (seval_list_hsval g
 Local Notation "'smem_refines' ge sp rs0 m0 hm sm" := (seval_hsmem ge sp hm rs0 m0 = seval_smem ge sp sm rs0 m0)
   (only parsing, at level 0, ge at next level, sp at next level, rs0 at next level, m0 at next level, hm at next level, sm at next level).
 
-Definition hsi_sreg_eval ge sp (hst: PTree.t hsval) r rs0 m0: option val :=
+Definition hsi_sreg_proj (hst: PTree.t hsval) r: sval :=
    match PTree.get r hst with
-   | None => Some (Regmap.get r rs0)
-   | Some hsv => seval_sval ge sp (hsval_proj hsv) rs0 m0
+   | None => Sinput r
+   | Some hsv => hsval_proj hsv
    end.
 
+Definition hsi_sreg_eval ge sp hst r := seval_sval ge sp (hsi_sreg_proj hst r).
+
 Definition hsok_local ge sp rs0 m0 (hst: hsistate_local) : Prop :=
      (forall hsv, List.In hsv (hsi_ok_lsval hst) -> seval_hsval ge sp hsv rs0 m0 <> None)
   /\ (seval_hsmem ge sp (hst.(hsi_smem)) rs0 m0 <> None).
@@ -261,22 +248,6 @@ Definition hsilocal_refines ge sp rs0 m0 (hst: hsistate_local) (st: sistate_loca
   /\  (forall m b ofs, seval_smem ge sp st.(si_smem) rs0 m0 = Some m -> Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs)
   .
 
-
-(*
-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 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.
-*)
-
 Lemma hsilocal_refines_sreg ge sp rs0 m0 hst st:
   hsilocal_refines ge sp rs0 m0 hst st -> 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.
 Proof.
@@ -393,7 +364,65 @@ Proof.
 Qed.
 Local Hint Resolve hsistate_refines_dyn_nested: core.
 
+Definition hfinal_proj (hfv: hsfval) : sfval := 
+  match hfv with
+  | HSnone => Snone
+  | HScall s hvi hlv r pc => Scall s (sum_left_map hsval_proj hvi) (hsval_list_proj hlv) r pc
+  | HStailcall s hvi hlv => Stailcall s (sum_left_map hsval_proj hvi) (hsval_list_proj hlv)
+  | HSbuiltin ef lbh br pc => Sbuiltin ef (List.map (builtin_arg_map hsval_proj) lbh) br pc
+  | HSjumptable hv ln => Sjumptable (hsval_proj hv) ln
+  | HSreturn oh => Sreturn (option_map hsval_proj oh)
+  end.
+
+Section HFINAL_REFINES.
+
+Variable ge: RTL.genv.
+Variable sp: val.
+Variable rs0: regset.
+Variable m0: mem.
+
+Definition option_refines (ohsv: option hsval) (osv: option sval) :=
+  match ohsv, osv with
+  | Some hsv, Some sv => sval_refines ge sp rs0 m0 hsv sv
+  | None, None => True
+  | _, _ => False
+  end.
+
+Definition sum_refines (hsi: hsval + ident) (si: sval + ident) :=
+  match hsi, si with
+  | inl hv, inl sv => sval_refines ge sp rs0 m0 hv sv
+  | inr id, inr id' => id = id'
+  | _, _ => False
+  end.
 
+Definition bargs_refines (hargs: list (builtin_arg hsval)) (args: list (builtin_arg sval)): Prop :=
+  seval_list_builtin_sval ge sp (List.map (builtin_arg_map hsval_proj) hargs) rs0 m0 = seval_list_builtin_sval ge sp args rs0 m0.
+
+Inductive hfinal_refines: hsfval -> sfval -> Prop :=
+  | hsnone_ref: hfinal_refines HSnone Snone
+  | hscall_ref: forall hros ros hargs args s r pc,
+      sum_refines hros ros ->
+      list_sval_refines ge sp rs0 m0 hargs args ->
+      hfinal_refines (HScall s hros hargs r pc) (Scall s ros args r pc)
+  | hstailcall_ref: forall hros ros hargs args s,
+      sum_refines hros ros ->
+      list_sval_refines ge sp rs0 m0 hargs args ->
+      hfinal_refines (HStailcall s hros hargs) (Stailcall s ros args)
+  | hsbuiltin_ref: forall ef lbha lba br pc,
+      bargs_refines lbha lba ->
+      hfinal_refines (HSbuiltin ef lbha br pc) (Sbuiltin ef lba br pc)
+  | hsjumptable_ref: forall hsv sv lpc,
+      sval_refines ge sp rs0 m0 hsv sv -> hfinal_refines (HSjumptable hsv lpc) (Sjumptable sv lpc)
+  | hsreturn_ref: forall ohsv osv,
+      option_refines ohsv osv -> hfinal_refines (HSreturn ohsv) (Sreturn osv).
+
+End HFINAL_REFINES.
+
+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 ge sp rs0 m0 (hfinal hst) (final st))
+.
 (** * Implementation of symbolic execution *)
 Section CanonBuilding.
 
@@ -489,8 +518,8 @@ Local Hint Resolve hSload_correct: wlp.
 Definition hSnil (_: unit): ?? list_hsval :=
    hC_list_hsval {| hdata := HSnil unknown_hid; hcodes := nil |}.
 
-Lemma hSnil_correct x:
-  WHEN hSnil x ~> hv THEN forall ge sp rs0 m0,
+Lemma hSnil_correct:
+  WHEN hSnil() ~> hv THEN forall ge sp rs0 m0,
     list_sval_refines ge sp rs0 m0 hv Snil.
 Proof.
   wlp_simplify.
@@ -517,8 +546,8 @@ Local Hint Resolve hScons_correct: wlp.
 Definition hSinit (_: unit): ?? hsmem :=
    hC_hsmem {| hdata := HSinit unknown_hid; hcodes := nil |}.
 
-Lemma hSinit_correct x:
-  WHEN hSinit x ~> hm THEN forall ge sp rs0 m0,
+Lemma hSinit_correct:
+  WHEN hSinit() ~> hm THEN forall ge sp rs0 m0,
     smem_refines ge sp rs0 m0 hm Sinit.
 Proof.
   wlp_simplify.
@@ -561,7 +590,7 @@ Lemma hsi_sreg_get_correct hst r:
     (RR: forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (f r) rs0 m0),
     sval_refines ge sp rs0 m0 hsv (f r).
 Proof.
-  unfold hsi_sreg_eval; wlp_simplify; rewrite <- RR; try_simplify_someHyps.
+  unfold hsi_sreg_eval, hsi_sreg_proj; wlp_simplify; rewrite <- RR; try_simplify_someHyps.
 Qed.
 Global Opaque hsi_sreg_get.
 Local Hint Resolve hsi_sreg_get_correct: wlp.
@@ -834,7 +863,7 @@ Lemma red_PTree_set_correct (r r0:reg) hsv hst ge sp rs0 m0:
 Proof.
   destruct hsv; simpl; auto.
   destruct (Pos.eq_dec r r1); auto.
-  subst; unfold hsi_sreg_eval.
+  subst; unfold hsi_sreg_eval, hsi_sreg_proj.
   destruct (Pos.eq_dec r0 r1); auto.
   - subst; rewrite PTree.grs, PTree.gss; simpl; auto.
   - rewrite PTree.gro, PTree.gso; simpl; auto.
@@ -848,7 +877,7 @@ Lemma red_PTree_set_refines (r r0:reg) hsv hst sv st ge sp rs0 m0:
 Proof.
   intros; rewrite red_PTree_set_correct.
   exploit hsilocal_refines_sreg; eauto.
-  unfold hsi_sreg_eval.
+  unfold hsi_sreg_eval, hsi_sreg_proj.
   destruct (Pos.eq_dec r r0); auto.
   - subst. rewrite PTree.gss; simpl; auto.
   - rewrite PTree.gso; simpl; eauto.
@@ -1031,7 +1060,7 @@ Proof.
   intros (st' & SPATH & PSTAT & PDYN).
   eexists; intuition eauto.
 Qed.
-Global Opaque hsiexec_path_correct.
+Global Opaque hsiexec_path.
 Local Hint Resolve hsiexec_path_correct: wlp.
 
 Fixpoint hbuiltin_arg (hst: PTree.t hsval) (arg : builtin_arg reg): ?? builtin_arg hsval := 
@@ -1057,6 +1086,30 @@ Fixpoint hbuiltin_arg (hst: PTree.t hsval) (arg : builtin_arg reg): ?? builtin_a
     RET (BA_addptr v1 v2)
   end.
 
+Lemma hbuiltin_arg_correct hst arg:
+  WHEN hbuiltin_arg hst arg ~> hargs THEN forall ge sp rs0 m0 (f: reg -> sval) v m
+    (RR: forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (f r) rs0 m0),
+    (seval_builtin_arg ge sp m rs0 m0 (builtin_arg_map hsval_proj hargs) v <-> seval_builtin_arg ge sp m rs0 m0 (builtin_arg_map f arg) v).
+Proof.
+  unfold hbuiltin_arg; induction arg; wlp_simplify.
+  + inversion H0. subst; econstructor. erewrite <- H; eauto.
+  + inversion H0. subst; econstructor. erewrite H; eauto.
+  + inversion H1. subst; econstructor.
+    * erewrite <- H; eauto.
+    * erewrite <- H0; eauto.
+  + inversion H1. subst; econstructor.
+    * erewrite H; eauto.
+    * erewrite H0; eauto.
+  + inversion H1. subst; econstructor.
+    * erewrite <- H; eauto.
+    * erewrite <- H0; eauto.
+  + inversion H1. subst; econstructor.
+    * erewrite H; eauto.
+    * erewrite H0; eauto.
+Qed.
+Global Opaque hbuiltin_arg.
+Local Hint Resolve hbuiltin_arg_correct: wlp.
+
 Fixpoint hbuiltin_args (hst: PTree.t hsval) (args: list (builtin_arg reg)): ?? list (builtin_arg hsval) :=
   match args with
   | nil => RET nil
@@ -1066,12 +1119,41 @@ Fixpoint hbuiltin_args (hst: PTree.t hsval) (args: list (builtin_arg reg)): ?? l
     RET (ha::hl)
     end.
 
+Lemma hbuiltin_args_correct hst args:
+  WHEN hbuiltin_args hst args ~> hargs THEN forall ge sp rs0 m0 (f: reg -> sval)
+    (RR: forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (f r) rs0 m0),
+    bargs_refines ge sp rs0 m0 hargs (List.map (builtin_arg_map f) args).
+Admitted.
+(* A REVOIR
+Proof.
+  unfold hbuiltin_args, bargs_refines, seval_builtin_args; induction args; wlp_simplify.
+  + inversion H1. subst; econstructor.
+    * erewrite <- H; eauto.
+    * erewrite <- H0; eauto.
+  + inversion H1. subst; econstructor.
+    * erewrite H; eauto.
+    * erewrite H0; eauto.
+Qed.
+*)
+Global Opaque hbuiltin_args.
+Local Hint Resolve hbuiltin_args_correct: wlp.
+
 Definition hsum_left (hst: PTree.t hsval) (ros: reg + ident): ?? (hsval + ident) :=
   match ros with
   | inl r => DO hr <~ hsi_sreg_get hst r;; RET (inl hr) 
   | inr s => RET (inr s)
   end.
 
+Lemma hsum_left_correct hst ros:
+  WHEN hsum_left hst ros ~> hsi THEN forall ge sp rs0 m0 (f: reg -> sval)
+    (RR: forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (f r) rs0 m0),
+    sum_refines ge sp rs0 m0 hsi (sum_left_map f ros).
+Proof.
+  unfold sum_refines; destruct ros; wlp_simplify.
+Qed.
+Global Opaque hsum_left.
+Local Hint Resolve hsum_left_correct: wlp.
+
 Definition hsexec_final (i: instruction) (hst: PTree.t hsval): ?? hsfval :=
   match i with
   | Icall sig ros args res pc =>
@@ -1116,9 +1198,573 @@ Definition hsexec (f: function) (pc:node): ?? hsstate :=
             RET {| hinternal := hst; hfinal := hsvf |}
   end.
 
+Lemma hsexec_correct f pc:
+  WHEN hsexec f pc ~> hst THEN
+  exists st, sexec f pc = Some st /\ hsstate_refines hst st.
+Admitted.
+Global Opaque hsexec_correct.
+
 End CanonBuilding.
 
-(** * The simulation test of concrete hash-consed symbolic execution *)
+Local Hint Resolve hsexec_correct: wlp.
+
+(** * Intermediate specifications of the simulation test *)
+
+(** ** Specification of the simulation test on [hsistate_local].
+       It is motivated by [hsilocal_simu_core_correct theorem] below
+*)
+Definition hsilocal_simu_core (oalive: option Regset.t) (hst1 hst2: hsistate_local) :=
+     List.incl (hsi_ok_lsval hst2) (hsi_ok_lsval hst1)
+  /\ (forall r, (match oalive with Some alive => Regset.In r alive | _ => True end) -> PTree.get r hst2 = PTree.get r hst1)
+  /\ hsi_smem hst1 = hsi_smem hst2.
+
+Definition seval_sval_partial ge sp rs0 m0 hsv :=
+  match seval_hsval ge sp hsv rs0 m0 with
+  | Some v => v
+  | None => Vundef
+  end.
+
+Definition select_first (ox oy: option val) :=
+  match ox with
+  | Some v => Some v
+  | None => oy
+  end.
+
+(** If the register was computed by hrs, evaluate the symbolic value from hrs.
+    Else, take the value directly from rs0 *)
+Definition seval_partial_regset ge sp rs0 m0 hrs :=
+  let hrs_eval := PTree.map1 (seval_sval_partial ge sp rs0 m0) hrs in
+  (fst rs0, PTree.combine select_first hrs_eval (snd rs0)).
+
+Lemma seval_partial_regset_get ge sp rs0 m0 hrs r:
+  (seval_partial_regset ge sp rs0 m0 hrs) # r =
+  match (hrs ! r) with Some sv => seval_sval_partial ge sp rs0 m0 sv | None => (rs0 # r) end.
+Proof.
+  unfold seval_partial_regset. unfold Regmap.get. simpl.
+  rewrite PTree.gcombine; [| simpl; reflexivity]. rewrite PTree.gmap1.
+  destruct (hrs ! r); simpl; [reflexivity|].
+  destruct ((snd rs0) ! r); reflexivity.
+Qed.
+
+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 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.
+
+Lemma hsilocal_simu_core_nofail ge1 ge2 of sp rs0 m0 hst1 hst2:
+  hsilocal_simu_core of 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 (RSOK & _ & MEMOK) GFS (OKV & OKM). constructor.
+  - intros sv INS. apply RSOK in INS. apply OKV in INS. erewrite seval_preserved; eauto.
+  - erewrite MEMOK in OKM. erewrite smem_eval_preserved; eauto.
+Qed.
+
+Theorem hsilocal_simu_core_correct hst1 hst2 of ge1 ge2 sp rs0 m0 rs m st1 st2:
+  hsilocal_simu_core of 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 ->
+  match of with
+  | None => ssem_local ge2 sp st2 rs0 m0 rs m
+  | Some alive => 
+      let rs' := seval_partial_regset ge2 sp rs0 m0 (hsi_sreg hst2)
+      in ssem_local ge2 sp st2 rs0 m0 rs' m /\ eqlive_reg (fun r => Regset.In r alive) rs rs'
+  end.
+Proof.
+  intros CORE HREF1 HREF2 GFS SEML.
+  refine (modusponens _ _ (ssem_local_refines_hok _ _ _ _ _ _ _ _ _ _) _); eauto.
+  intro HOK1.
+  refine (modusponens _ _ (hsilocal_simu_core_nofail _ _ _ _ _ _ _ _ _ _ _) _); eauto.
+  intro HOK2.
+  destruct SEML as (PRE & MEMEQ & RSEQ).
+  assert (SIPRE: si_pre st2 ge2 sp rs0 m0). { destruct HREF2 as (OKEQ & _ & _). rewrite <- OKEQ in HOK2. apply HOK2. }
+  assert (SMEMEVAL: seval_smem ge2 sp (si_smem st2) rs0 m0 = Some m). {
+    destruct HREF2 as (_ & MEMEQ2 & _). destruct HREF1 as (_ & MEMEQ1 & _).
+    destruct CORE as (_ & _ & MEMEQ3).
+    rewrite <- MEMEQ2; auto. rewrite <- MEMEQ3.
+    erewrite smem_eval_preserved; [| eapply GFS].
+    rewrite MEMEQ1; auto. }
+  destruct of as [alive |].
+  - constructor.
+    + constructor; [assumption | constructor; [assumption|]].
+      destruct HREF2 as (B & _ & A & _).
+      (** B is used for the auto below. *)
+      assert (forall r : positive, hsi_sreg_eval ge2 sp hst2 r rs0 m0 = seval_sval ge2 sp (si_sreg st2 r) rs0 m0) by auto.
+      intro r. rewrite <- H. clear H. 
+      generalize (A HOK2 r). unfold hsi_sreg_eval.
+      rewrite seval_partial_regset_get.
+      unfold hsi_sreg_proj.
+      destruct (hst2 ! r) eqn:HST2; [| simpl; reflexivity].
+      unfold seval_sval_partial. generalize HOK2; rewrite <- B; intros (_ & _ & C) D.
+      assert (seval_sval ge2 sp (hsval_proj h) rs0 m0 <> None) by congruence.
+      destruct (seval_sval ge2 sp _ rs0 m0); [reflexivity | contradiction].
+    + intros r ALIVE. destruct HREF2 as (_ & _ & A & _). destruct HREF1 as (_ & _ & B & _).
+      destruct CORE as (_ & C & _). rewrite seval_partial_regset_get.
+      assert (OPT: forall (x y: val), Some x = Some y -> x = y) by congruence.
+      destruct (hst2 ! r) eqn:HST2; apply OPT; clear OPT.
+      ++ unfold seval_sval_partial.
+         assert (seval_sval ge2 sp (hsval_proj h) rs0 m0 = hsi_sreg_eval ge2 sp hst2 r rs0 m0). {
+           unfold hsi_sreg_eval, hsi_sreg_proj. rewrite HST2. reflexivity. }
+         rewrite H. clear H. unfold hsi_sreg_eval, hsi_sreg_proj. rewrite C; [|assumption].
+         erewrite seval_preserved; [| eapply GFS].
+         unfold hsi_sreg_eval, hsi_sreg_proj in B; rewrite B; [|assumption]. rewrite RSEQ. reflexivity.
+      ++ rewrite <- RSEQ. rewrite <- B; [|assumption]. unfold hsi_sreg_eval, hsi_sreg_proj.
+         rewrite <- C; [|assumption]. rewrite HST2. reflexivity.
+  - 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 <- MEMEQ3.
+      erewrite smem_eval_preserved; [| eapply GFS].
+      rewrite MEMEQ1; auto.
+    + intro r. destruct HREF2 as (_ & _ & A & _). destruct HREF1 as (_ & _ & B & _).
+      destruct CORE as (_ & C & _). rewrite <- A; auto. unfold hsi_sreg_eval, hsi_sreg_proj.
+      rewrite C; [|auto]. erewrite seval_preserved; [| eapply GFS].
+      unfold hsi_sreg_eval, hsi_sreg_proj in B; rewrite B; auto.
+Qed.
+
+(** ** Specification of the simulation test on [hsistate_exit].
+       It is motivated by [hsiexit_simu_core_correct theorem] below
+*)
+Definition hsiexit_simu_core dm f (hse1 hse2: hsistate_exit) :=
+  (exists path, (fn_path f) ! (hsi_ifso hse1) = Some path
+    /\ hsilocal_simu_core (Some path.(input_regs)) (hsi_elocal hse1) (hsi_elocal hse2))
+  /\ dm ! (hsi_ifso hse2) = Some (hsi_ifso hse1)
+  /\ hsi_cond hse1 = hsi_cond hse2
+  /\ hsi_scondargs hse1 = hsi_scondargs hse2.
+
+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 ((p & _ & 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 st1 st2 HREF1 HREF2 HDYN1 HDYN2.
+  assert (SEVALC:
+   sok_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (si_elocal st1) ->
+    (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 ((OKEQ1 & _) & SCOND1).
+    rewrite OKEQ1; intro OK1. rewrite <- SCOND1 by assumption. clear SCOND1.
+    generalize (genv_match ctx).
+    intro GFS; exploit hsiexit_simu_core_nofail; eauto.
+    destruct HDYN2 as (_ & SCOND2). intro OK2. rewrite <- SCOND2 by assumption. clear OK1 OK2 SCOND2.
+    destruct SIMUC as ((path & _ & LSIMU) & _ & CONDEQ & ARGSEQ). destruct LSIMU as (_ & _ & MEMEQ).
+    rewrite CONDEQ. rewrite ARGSEQ. rewrite MEMEQ. erewrite <- hseval_condition_preserved; eauto.
+  }
+  constructor; [assumption|]. intros is1 ICONT SSEME.
+  assert (OK1: sok_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (si_elocal st1)). {
+    destruct SSEME as (_ & SSEML & _). eapply ssem_local_sok; eauto. }
+  assert (HOK1: hsok_exit (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse1). {
+    unfold hsok_exit. destruct HDYN1 as (LREF & _). destruct LREF as (OKEQ & _ & _). rewrite <- OKEQ. assumption. }
+  exploit hsiexit_simu_core_nofail. 2: eapply ctx. all: eauto. intro HOK2.
+  destruct SSEME as (SCOND & SLOC & PCEQ). destruct SIMUC as ((path & PATH & LSIMU) & REVEQ & _ & _); eauto.
+  destruct HDYN1 as (LREF1 & _). destruct HDYN2 as (LREF2 & _).
+  exploit hsilocal_simu_core_correct; eauto; [apply ctx|]. simpl.
+  intros (SSEML & EQREG).
+  eexists (mk_istate (icontinue is1) (si_ifso st2) _ (imem is1)). simpl. constructor.
+  - constructor; intuition congruence || eauto.
+  - unfold istate_simu. rewrite ICONT.
+    simpl. assert (PCEQ': hsi_ifso hse1 = ipc is1) by congruence.
+    exists path. constructor; [|constructor]; [congruence| |congruence].
+    constructor; [|constructor]; simpl; auto.
+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.
+
+(** ** Specification of the simulation test on [list hsistate_exit].
+       It is motivated by [hsiexit_simu_core_correct theorem] below
+*)
+
+Definition hsiexits_simu dm f (ctx: simu_proof_context f) (lhse1 lhse2: list hsistate_exit): 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.
+
+
+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) ->
+  (forall se1, In se1 lse1 -> sok_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (si_elocal se1)) ->
+  all_fallthrough (the_ge2 ctx) (the_sp ctx) lse2 (the_rs0 ctx) (the_m0 ctx).
+Proof.
+  induction 1; [unfold all_fallthrough; contradiction|]; simpl.
+  intros X OK 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.
+  - intros; intuition.
+Qed.
+
+
+Lemma siexits_simu_all_fallthrough_upto dm f ctx lse1 lse2:
+  siexits_simu dm f lse1 lse2 ctx ->
+  forall ext1 lx1,
+  (forall se1, In se1 lx1 -> sok_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (si_elocal se1)) ->
+  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 ext lx1. intros OK H. destruct H as (ITAIL & ALLFU). eapply is_tail_false in ITAIL. contradiction.
+  - simpl; intros ext lx1 OK 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.
+      * intuition. apply OK. eassumption.
+      * constructor; eauto.
+      * intros (ext2 & lx2 & ALLFUE2 & LENEQ).
+        eexists; eexists. constructor; eauto.
+        eapply all_fallthrough_upto_exit_cons; 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.
+
+
+(** ** Specification of the simulation test on [hsistate].
+       It is motivated by [hsistate_simu_core_correct theorem] below
+*)
+
+Definition hsistate_simu_core dm f (hse1 hse2: hsistate) :=
+     (dm ! (hsi_pc hse2) = Some (hsi_pc hse1))  (* FIXME: issue here ? => see hsistate_simu_check below *)
+  /\ list_forall2 (hsiexit_simu_core dm f) (hsi_exits hse1) (hsi_exits hse2)
+  /\ hsilocal_simu_core None (hsi_local hse1) (hsi_local hse2).
+
+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 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 & NESTED). 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|]. simpl. 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.
+      * eapply nested_sok_prop; eauto.
+        eapply ssem_local_sok; 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.
+    * destruct ALLFU as (ITAIL & ALLF).
+      exploit nested_sok_tail; eauto. intros NESTED2.
+      inv NESTED2. destruct SSEME as (_ & SSEML & _). eapply ssem_local_sok in SSEML.
+      eapply nested_sok_prop; 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; [|assumption]. 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.
+
+
+(** ** Specification of the simulation test on [sfval].
+       It is motivated by [hsistate_simu_core_correct theorem] below
+*)
+
+
+Definition final_simu_core (dm: PTree.t node) (f: RTLpath.function) (pc1 pc2: node) (f1 f2: sfval): Prop :=
+  match f1 with
+  | Scall sig1 svos1 lsv1 res1 pc1 =>
+      match f2 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 f2 with
+      | Sbuiltin ef2 lbs2 br2 pc2 =>
+          dm ! pc2 = Some pc1 /\ ef1 = ef2 /\ lbs1 = lbs2 /\ br1 = br2
+      | _ => False
+      end
+  | Sjumptable sv1 lpc1 =>
+      match f2 with
+      | Sjumptable sv2 lpc2 =>
+          ptree_get_list dm lpc2 = Some lpc1 /\ sv1 = sv2
+      | _ => False
+      end
+  | Snone =>
+      match f2 with
+      | Snone => dm ! pc2 = Some pc1
+      | _ => False
+      end
+  (* Stailcall, Sreturn *)
+  | _ => f1 = f2
+  end.
+
+Definition hfinal_simu_core (dm: PTree.t node) (f: RTLpath.function) (pc1 pc2: node) (hf1 hf2: hsfval): Prop :=
+  final_simu_core dm f pc1 pc2 (hfinal_proj hf1) (hfinal_proj hf2).
+
+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.
+
+Lemma list_proj_refines_eq ge ge' sp rs0 m0 lsv lhsv:
+  (forall s, Genv.find_symbol ge s = Genv.find_symbol ge' s) ->
+  list_sval_refines ge sp rs0 m0 lhsv lsv ->
+  forall lhsv' lsv',
+  list_sval_refines ge' sp rs0 m0 lhsv' lsv' ->
+  hsval_list_proj lhsv = hsval_list_proj lhsv' ->
+  seval_list_sval ge sp lsv rs0 m0 = seval_list_sval ge' sp lsv' rs0 m0.
+Proof.
+  intros GFS H lhsv' lsv' H0 H1.
+  erewrite <- H, H1.
+  erewrite list_sval_eval_preserved; eauto.
+Qed.
+
+(*
+Lemma barg_proj_refines_eq_single ge ge' sp rs0 m0:
+  (forall s, Genv.find_symbol ge s = Genv.find_symbol ge' s) ->
+  forall hsv sv, barg_refines ge sp rs0 m0 hsv sv ->
+  forall hsv' sv', barg_refines ge' sp rs0 m0 hsv' sv' ->
+  builtin_arg_map hsval_proj hsv = builtin_arg_map hsval_proj hsv' ->
+  seval_builtin_sval ge sp sv rs0 m0 = seval_builtin_sval ge' sp sv' rs0 m0.
+Proof.
+  intro GFS hsv sv H hsv' sv' H' H0.
+  
+  all: try (simpl; intros hsv' sv' BREF' BPROJ';
+    destruct hsv'; simpl in BPROJ'; try discriminate;
+    inv BPROJ'; inv BREF'; simpl; try reflexivity;
+    erewrite sval_refines_proj; eauto).
+(* BA_splitlong *)
+  - simpl. intros hsv' sv' BREF' BPROJ'.
+    destruct hsv'; simpl in BPROJ'; try discriminate.
+    inv BPROJ'. inv BREF'. simpl.
+    erewrite IHbarg_refines2; eauto.
+    erewrite IHbarg_refines1. 2: eapply H5.
+    all: eauto.
+(* BA_addptr *)
+  - simpl. intros hsv' sv' BREF' BPROJ'.
+    destruct hsv'; simpl in BPROJ'; try discriminate.
+    inv BPROJ'. inv BREF'. simpl.
+    erewrite IHbarg_refines2; eauto.
+    erewrite IHbarg_refines1. 2: eapply H5.
+    all: eauto.
+Qed.
+
+Lemma barg_proj_refines_eq ge ge' sp rs0 m0: forall lsv lhsv,
+  (forall s, Genv.find_symbol ge s = Genv.find_symbol ge' s) ->
+  list_forall2 (barg_refines ge sp rs0 m0) lhsv lsv ->
+  forall lhsv' lsv',
+  list_forall2 (barg_refines ge' sp rs0 m0) lhsv' lsv' ->
+  barg_list_proj lhsv = barg_list_proj lhsv' ->
+  seval_list_builtin_sval ge sp lsv rs0 m0 = seval_list_builtin_sval ge' sp lsv' rs0 m0.
+Proof.
+  induction 2; rename H into GFS.
+  - simpl. intros. destruct lhsv'; try discriminate. clear H0.
+    inv H. simpl. reflexivity.
+  - simpl. intros. destruct lhsv'; try discriminate.
+    simpl in H2. inv H2. destruct lsv'; [inv H|].
+    inv H. simpl.
+    erewrite barg_proj_refines_eq_single; eauto.
+    erewrite IHlist_forall2; eauto.
+Qed.
+
+
+Theorem hfinal_simu_core_correct dm f ctx opc1 opc2 hf1 hf2 f1 f2:
+  hfinal_simu_core dm f opc1 opc2 hf1 hf2 ->
+  hfinal_refines (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hf1 f1 ->
+  hfinal_refines (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hf2 f2 ->
+  sfval_simu dm f opc1 opc2 ctx f1 f2.
+Proof.
+  assert (GFS: forall s : ident, Genv.find_symbol (the_ge1 ctx) s = Genv.find_symbol (the_ge2 ctx) s) by apply ctx.
+  intros CORE FREF1 FREF2.
+  destruct hf1; inv FREF1.
+  (* Snone *)
+  - destruct hf2; try contradiction. inv FREF2.
+    inv CORE. constructor. assumption.
+  (* Scall *)
+  - rename H5 into SREF1. rename H6 into LREF1.
+    destruct hf2; try contradiction. inv FREF2.
+    rename H5 into SREF2. rename H6 into LREF2.
+    destruct CORE as (PCEQ & ? & ? & ? & ?). subst.
+    rename H0 into SVOSEQ. rename H1 into LSVEQ.
+    constructor; [assumption | |].
+    + destruct svos.
+      * destruct svos0; try discriminate. destruct ros; try contradiction.
+        destruct ros0; try contradiction. constructor.
+        simpl in SVOSEQ. inv SVOSEQ.
+        simpl in SREF1. simpl in SREF2.
+        rewrite <- SREF1. rewrite <- SREF2.
+        erewrite <- seval_preserved; [| eapply GFS]. congruence.
+      * destruct svos0; try discriminate. destruct ros; try contradiction.
+        destruct ros0; try contradiction. constructor.
+        simpl in SVOSEQ. inv SVOSEQ. congruence.
+    + erewrite list_proj_refines_eq; eauto. constructor.
+  (* Stailcall *)
+  - rename H3 into SREF1. rename H4 into LREF1.
+    destruct hf2; try (inv CORE; fail). inv FREF2.
+    rename H4 into LREF2. rename H3 into SREF2.
+    inv CORE. rename H1 into SVOSEQ. rename H2 into LSVEQ.
+    constructor.
+    + destruct svos. (** Copy-paste from Scall *)
+      * destruct svos0; try discriminate. destruct ros; try contradiction.
+        destruct ros0; try contradiction. constructor.
+        simpl in SVOSEQ. inv SVOSEQ.
+        simpl in SREF1. simpl in SREF2.
+        rewrite <- SREF1. rewrite <- SREF2.
+        erewrite <- seval_preserved; [| eapply GFS]. congruence.
+      * destruct svos0; try discriminate. destruct ros; try contradiction.
+        destruct ros0; try contradiction. constructor.
+        simpl in SVOSEQ. inv SVOSEQ. congruence.
+    + erewrite list_proj_refines_eq; eauto. constructor.
+  (* Sbuiltin *)
+  - rename H4 into BREF1. destruct hf2; try (inv CORE; fail). inv FREF2.
+    rename H4 into BREF2. inv CORE. destruct H0 as (? & ? & ?). subst.
+    rename H into PCEQ. rename H1 into ARGSEQ. constructor; [assumption|].
+    erewrite barg_proj_refines_eq; eauto. constructor.
+  (* Sjumptable *)
+  - rename H2 into SREF1. destruct hf2; try contradiction. inv FREF2.
+    rename H2 into SREF2. destruct CORE as (A & B). constructor; [assumption|].
+    erewrite sval_refines_proj; eauto. constructor.
+  (* Sreturn *)
+  - rename H0 into SREF1.
+    destruct hf2; try discriminate. inv CORE.
+    inv FREF2. destruct osv; destruct res; inv SREF1.
+    + destruct res0; try discriminate. destruct osv0; inv H1.
+      constructor. simpl in H0. inv H0. erewrite sval_refines_proj; eauto.
+      constructor.
+    + destruct res0; try discriminate. destruct osv0; inv H1. constructor.
+Qed.
+*)
+
+(** * Implementing the simulation test with concrete hash-consed symbolic execution *)
 
 Definition phys_check {A} (x y:A) (msg: pstring): ?? unit :=
   DO b <~ phys_eq x y;;
@@ -1131,7 +1777,7 @@ Definition struct_check {A} (x y: A) (msg: pstring): ?? unit :=
   RET tt.
 
 Lemma struct_check_correct {A} (a b: A) msg:
-  WHEN struct_check a b msg ~> tt THEN
+  WHEN struct_check a b msg ~> _ THEN
   a = b.
 Proof. wlp_simplify. Qed.
 Global Opaque struct_check.
@@ -1170,6 +1816,7 @@ Proof.
   wlp_simplify. destruct x; simpl; auto.
 Qed.
 Global Opaque PTree_eq_check.
+Local Hint Resolve PTree_eq_check_correct: wlp.
 
 Fixpoint PTree_frame_eq_check {A} (frame: list positive) (d1 d2: PTree.t A): ?? unit :=
   match frame with
@@ -1186,6 +1833,7 @@ Proof.
   subst; auto.
 Qed.
 Global Opaque PTree_frame_eq_check.
+Local Hint Resolve PTree_frame_eq_check_correct: wlp.
 
 Definition hsilocal_simu_check hst1 hst2 : ?? unit :=
   DEBUG("? last check");;
@@ -1194,9 +1842,14 @@ Definition hsilocal_simu_check hst1 hst2 : ?? unit :=
   Sets.assert_list_incl mk_hash_params (hsi_ok_lsval hst2) (hsi_ok_lsval hst1);;
   DEBUG("=> last check: OK").
 
-Definition revmap_check_single (dm: PTree.t node) (n tn: node) : ?? unit :=
-  DO res <~ some_or_fail (dm ! tn) "revmap_check_single: no mapping for tn";;
-  struct_check n res "revmap_check_single: n and res are physically different".
+Lemma hsilocal_simu_check_correct hst1 hst2:
+  WHEN hsilocal_simu_check hst1 hst2 ~> _ THEN
+  hsilocal_simu_core None hst1 hst2.
+Proof.
+  unfold hsilocal_simu_core; wlp_simplify. 
+Qed.
+Hint Resolve hsilocal_simu_check_correct: wlp.
+Global Opaque hsilocal_simu_check.
 
 Definition hsilocal_frame_simu_check frame hst1 hst2 : ?? unit :=
   DEBUG("? frame check");;
@@ -1205,6 +1858,46 @@ Definition hsilocal_frame_simu_check frame hst1 hst2 : ?? unit :=
   Sets.assert_list_incl mk_hash_params (hsi_ok_lsval hst2) (hsi_ok_lsval hst1);;
   DEBUG("=> frame check: OK").
 
+Lemma setoid_in {A: Type} (a: A): forall l,
+  SetoidList.InA (fun x y => x = y) a l ->
+  In a l.
+Proof.
+  induction l; intros; inv H.
+  - constructor. reflexivity.
+  - right. auto.
+Qed.
+
+Lemma regset_elements_in r rs:
+  Regset.In r rs ->
+  In r (Regset.elements rs).
+Proof.
+  intros. exploit Regset.elements_1; eauto. intro SIN.
+  apply setoid_in. assumption.
+Qed.
+Local Hint Resolve regset_elements_in: core.
+
+Lemma hsilocal_frame_simu_check_correct hst1 hst2 alive:
+  WHEN hsilocal_frame_simu_check (Regset.elements alive) hst1 hst2 ~> _ THEN
+  hsilocal_simu_core (Some alive) hst1 hst2.
+Proof.
+  unfold hsilocal_simu_core; wlp_simplify. symmetry; eauto.
+Qed.
+Hint Resolve hsilocal_frame_simu_check_correct: wlp.
+Global Opaque hsilocal_frame_simu_check.
+
+Definition revmap_check_single (dm: PTree.t node) (n tn: node) : ?? unit :=
+  DO res <~ some_or_fail (dm ! tn) "revmap_check_single: no mapping for tn";;
+  struct_check n res "revmap_check_single: n and res are physically different".
+
+Lemma revmap_check_single_correct dm pc1 pc2:
+  WHEN revmap_check_single dm pc1 pc2 ~> _ THEN
+  dm ! pc2 = Some pc1.
+Proof.
+  wlp_simplify. congruence.
+Qed.
+Hint Resolve revmap_check_single_correct: wlp.
+Global Opaque revmap_check_single.
+
 Definition hsiexit_simu_check (dm: PTree.t node) (f: RTLpath.function) (hse1 hse2: hsistate_exit): ?? unit :=
   struct_check (hsi_cond hse1) (hsi_cond hse2) "hsiexit_simu_check: conditions do not match";;
   phys_check (hsi_scondargs hse1) (hsi_scondargs hse2) "hsiexit_simu_check: args do not match";;
@@ -1212,6 +1905,15 @@ Definition hsiexit_simu_check (dm: PTree.t node) (f: RTLpath.function) (hse1 hse
   DO path <~ some_or_fail ((fn_path f) ! (hsi_ifso hse1)) "hsiexit_simu_check: internal error";;
   hsilocal_frame_simu_check (Regset.elements path.(input_regs)) (hsi_elocal hse1) (hsi_elocal hse2).
 
+Lemma hsiexit_simu_check_correct dm f hse1 hse2:
+  WHEN hsiexit_simu_check dm f hse1 hse2 ~> _ THEN
+  hsiexit_simu_core dm f hse1 hse2.
+Proof.
+  unfold hsiexit_simu_core; wlp_simplify.
+Qed.
+Hint Resolve hsiexit_simu_check_correct: wlp.
+Global Opaque hsiexit_simu_check.
+
 Fixpoint hsiexits_simu_check (dm: PTree.t node) (f: RTLpath.function) (lhse1 lhse2: list hsistate_exit) :=
   match lhse1,lhse2 with
   | nil, nil => RET tt
@@ -1221,10 +1923,33 @@ Fixpoint hsiexits_simu_check (dm: PTree.t node) (f: RTLpath.function) (lhse1 lhs
   | _, _ => FAILWITH "siexists_simu_check:  lengths do not match"
   end.
 
+Lemma hsiexits_simu_check_correct dm f: forall le1 le2,
+  WHEN hsiexits_simu_check dm f le1 le2 ~> _ THEN
+  hsiexits_simu_core dm f le1 le2.
+Proof.
+  unfold hsiexits_simu_core; induction le1; simpl; destruct le2; wlp_simplify; constructor; eauto.
+Qed.
+Hint Resolve hsiexits_simu_check_correct: wlp.
+Global Opaque hsiexits_simu_check.
+
+(* FIXME: we got an issue here. 
+   the revmap check may reject any code with a sfval<>None.
+*)
 Definition hsistate_simu_check (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsistate) :=
+  (* revmap_check_single dm (hsi_pc hst1) (hsi_pc hst2);; *)  (* FIXME: too strong ? *)
   hsiexits_simu_check dm f (hsi_exits hst1) (hsi_exits hst2);;
   hsilocal_simu_check (hsi_local hst1) (hsi_local hst2).
 
+Lemma hsistate_simu_check_correct dm f hst1 hst2:
+  WHEN hsistate_simu_check dm f hst1 hst2 ~> _ THEN
+  hsistate_simu_core dm f hst1 hst2.
+Proof.
+  unfold hsistate_simu_core; wlp_simplify.
+Admitted. (* FIXME *)
+Hint Resolve hsistate_simu_check_correct: wlp.
+Global Opaque hsistate_simu_check.
+
+
 Fixpoint revmap_check_list (dm: PTree.t node) (ln ln': list node): ?? unit :=
   match ln, ln' with
   | nil, nil => RET tt