Restart the proof with cherry-pick from Cyril and commit 0e4186b8f

2 files changed, 433 insertions, 1795 deletions

diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v
index 24da159a..2ea3e1ee 100644
--- a/kvx/lib/RTLpathSE_impl_junk.v
+++ b/kvx/lib/RTLpathSE_impl_junk.v
@@ -20,28 +20,10 @@ Local Open Scope impure.
 Import ListNotations.
 Local Open Scope list_scope.
 
-Ltac wlp_intro vname hname := apply wlp_unfold; intros vname hname.
-Ltac wlp_bind vname hname := apply wlp_bind; intros vname hname.
-Ltac wlp_ret vname := let H := fresh "H" vname in wlp_intro vname H; apply mayRet_ret in H; subst.
-
-Tactic Notation "wlp_intro" ident(v) ident(h) := wlp_intro v h.
-Tactic Notation "wlp_intro" ident(v) := let H := fresh "H" v in wlp_intro v H.
-Tactic Notation "wlp_bind" ident(v) ident(h) := wlp_bind v h.
-Tactic Notation "wlp_bind" ident(v) := let H := fresh "H" v in wlp_bind v H.
-
-Ltac wlp_absurd := match goal with
-  | [ H : FAILWITH ?msg |- _ ] => eapply (_FAILWITH_correct _ _ (fun _ => False)) in H; inv H
-  | [ H : DO r <~ fail ?msg;; RET ?expr ~~> ?exta |- _ ] => eapply (_FAILWITH_correct _ _ (fun _ => False)) in H; inv H
-end.
-
-Ltac wlp_hbind var := match goal with
-  | [ H : DO _ <~ ?expr;; _ ~~> _ |- _ ] => 
-      let Hvar := fresh "H" var in (apply mayRet_bind in H; destruct H as (var & Hvar & H))
-  end.
+Definition XDEBUG {A} (x:A) (k: A -> ?? pstring): ?? unit := RET tt. (* TO REMOVE DEBUG INFO *)
+(* Definition XDEBUG {A} (x:A) (k: A -> ?? pstring): ?? unit := DO s <~ k x;; println ("DEBUG simu_check:" +; s). (* TO INSERT DEBUG INFO *) *)
 
-Ltac wlp_hret := match goal with
-  | [ H : RET _ ~~> _ |- _ ] => apply mayRet_ret in H; subst; clear H
-  end.
+Definition DEBUG (s: pstring): ?? unit := XDEBUG tt (fun _ => RET s).
 
 (** * Implementation of Data-structure use in Hash-consing *)
 
@@ -100,6 +82,7 @@ Definition hsmem_set_hid (hsm: hsmem) (hid: hashcode): hsmem :=
   | HSstore hsm chunk addr lhsv srce _ => HSstore hsm chunk addr lhsv srce hid
   end.
 
+
 (** Now, we build the hash-Cons value from a "hash_eq".
 
   Informal specification: 
@@ -162,7 +145,9 @@ Program Definition mk_hash_params: Dict.hash_params hsval :=
  {|
     Dict.test_eq := phys_eq;
     Dict.hashing := fun (ht: hsval) => RET (hsval_get_hid ht);
-    Dict.log := fun _ => RET () (* NB no log *) |}.
+    Dict.log := fun hv =>
+         DO hv_name <~ string_of_hashcode (hsval_get_hid hv);;
+         println ("unexpected undef behavior of hashcode:" +; (CamlStr hv_name)) |}.
 Obligation 1.
   wlp_simplify.
 Qed.
@@ -207,6 +192,8 @@ 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. *)
+
 Fixpoint hsval_proj hsv :=
   match hsv with
   | HSinput r _ => Sinput r
@@ -224,30 +211,163 @@ with hsmem_proj hm :=
   | HSstore hm chk addr hl hv _ => Sstore (hsmem_proj hm) chk addr (hsval_list_proj hl) (hsval_proj hv)
   end.
 
+(** We use a Notation instead a Definition, in order to get more automation "for free" *)
+Local Notation "'seval_hsval' ge sp hsv" := (seval_sval ge sp (hsval_proj hsv))
+  (only parsing, at level 0, ge at next level, sp at next level, hsv at next level).
+Local Notation "'seval_list_hsval' ge sp lhv" := (seval_list_sval ge sp (hsval_list_proj lhv))
+  (only parsing, at level 0, ge at next level, sp at next level, lhv at next level).
+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).
+
+Local Notation "'list_sval_refines' ge sp rs0 m0 lhv lsv" := (seval_list_hsval ge sp lhv rs0 m0 = seval_list_sval ge sp lsv rs0 m0)
+  (only parsing, at level 0, ge at next level, sp at next level, rs0 at next level, m0 at next level, lhv at next level, lsv at next level).
+
+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 :=
+   match PTree.get r hst with
+   | None => Some (Regmap.get r rs0)
+   | Some hsv => seval_sval ge sp (hsval_proj hsv) rs0 m0
+   end.
+
+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).
+
+(* 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 -> smem_refines ge sp rs0 m0 (hsi_smem hst) (st.(si_smem)))
+  /\  (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)
+  /\  (forall r sv, hst ! r = Some sv -> In sv (hsi_ok_lsval hst)).
+
+(*
+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.
+*)
+
+(** 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_ifso hext = si_ifso ext.
+
+Definition hsok_exit ge sp rs m hse := hsok_local ge sp rs m (hsi_elocal hse).
+
+Definition hseval_condition ge sp cond hcondargs hmem rs0 m0 :=
+  seval_condition ge sp cond (hsval_list_proj hcondargs) (hsmem_proj hmem) rs0 m0.
+
+Lemma hseval_condition_preserved ge ge' sp cond args mem rs0 m0:
+  (forall s : ident, Genv.find_symbol ge' s = Genv.find_symbol ge s) ->
+  hseval_condition ge sp cond args mem rs0 m0 = hseval_condition ge' sp cond args mem rs0 m0.
+Proof.
+  intros. unfold hseval_condition. erewrite seval_condition_preserved; [|eapply H].
+  reflexivity.
+Qed.
+
+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_local ge sp rs0 m0 (hsi_elocal hext) ->
+        hseval_condition ge sp (hsi_cond hext) (hsi_scondargs hext) (hsi_smem (hsi_elocal hext)) rs0 m0
+         = seval_condition ge sp (si_cond ext) (si_scondargs ext) (si_smem (si_elocal ext)) rs0 m0).
+
+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.
+
+
+Inductive nested_sok ge sp rs0 m0: sistate_local -> list sistate_exit -> Prop :=
+    nsok_nil st: nested_sok ge sp rs0 m0 st nil
+  | nsok_cons st se lse:
+     (sok_local ge sp rs0 m0 st -> sok_local ge sp rs0 m0 (si_elocal se)) ->
+     nested_sok ge sp rs0 m0 (si_elocal se) lse ->
+     nested_sok ge sp rs0 m0 st (se::lse).
+
+Lemma nested_sok_prop ge sp st sle rs0 m0:
+  nested_sok ge sp rs0 m0 st sle ->
+  sok_local ge sp rs0 m0 st ->
+  forall se, In se sle -> sok_local ge sp rs0 m0 (si_elocal se).
+Proof.
+  induction 1; simpl; intuition (subst; eauto).
+Qed.
+
+Lemma nested_sok_elocal ge sp rs0 m0 st2 exits:
+  nested_sok ge sp rs0 m0 st2 exits ->
+  forall st1, (sok_local ge sp rs0 m0 st1 -> sok_local ge sp rs0 m0 st2) ->
+  nested_sok ge sp rs0 m0 st1 exits.
+Proof.
+  induction 1; [intros; constructor|].
+  intros. constructor; auto.
+Qed.
+
+Lemma nested_sok_tail ge sp rs0 m0 st lx exits:
+  is_tail lx exits ->
+  nested_sok ge sp rs0 m0 st exits ->
+  nested_sok ge sp rs0 m0 st lx.
+Proof.
+  induction 1; [auto|].
+  intros. inv H0. eapply IHis_tail. eapply nested_sok_elocal; eauto.
+Qed.
+
+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)
+  /\ nested_sok ge sp rs0 m0 (si_local st) (si_exits st).
+
+
 (** * Implementation of symbolic execution *)
 Section CanonBuilding.
 
 Variable hC_hsval: hashinfo hsval -> ?? hsval.
 
-(** FIXME - maybe it's not what we want ? *)
-Hypothesis hC_hsval_correct: forall hs rhsv,
-  hC_hsval hs ~~> rhsv ->
-  (hsval_proj (hdata hs)) = (hsval_proj rhsv).
-Local Hint Resolve hC_hsval_correct: wlp.
+Hypothesis hC_hsval_correct: forall hs,
+  WHEN hC_hsval hs ~> hs' THEN forall ge sp rs0 m0,
+    seval_hsval ge sp (hdata hs) rs0 m0 = seval_hsval ge sp hs' rs0 m0.
 
 Variable hC_list_hsval: hashinfo list_hsval -> ?? list_hsval.
-
-Hypothesis hC_list_hsval_correct: forall hs rhsv,
-  hC_list_hsval hs ~~> rhsv ->
-  (hsval_list_proj (hdata hs)) = (hsval_list_proj rhsv).
-Local Hint Resolve hC_list_hsval_correct: wlp.
+Hypothesis hC_list_hsval_correct: forall lh,
+  WHEN hC_list_hsval lh ~> lh' THEN forall ge sp rs0 m0,
+    seval_list_hsval ge sp (hdata lh) rs0 m0 = seval_list_hsval ge sp lh' rs0 m0.
 
 Variable hC_hsmem: hashinfo hsmem -> ?? hsmem.
-
-Hypothesis hC_hsmem_correct: forall hs rhsv,
-  hC_hsmem hs ~~> rhsv ->
-  (hsmem_proj (hdata hs)) = (hsmem_proj rhsv).
-Local Hint Resolve hC_hsmem_correct: wlp.
+Hypothesis hC_hsmem_correct: forall hm,
+  WHEN hC_hsmem hm ~> hm' THEN forall ge sp rs0 m0,
+    seval_hsmem ge sp (hdata hm) rs0 m0 = seval_hsmem ge sp hm' rs0 m0.
 
 (* First, we wrap constructors for hashed values !*)
 
@@ -265,6 +385,15 @@ Definition hSinput (r:reg): ?? hsval :=
    DO hv <~ hSinput_hcodes r;;
    hC_hsval {| hdata:=HSinput r unknown_hid; hcodes :=hv; |}.
 
+Lemma hSinput_correct r:
+  WHEN hSinput r ~> hv THEN forall ge sp rs0 m0,
+    sval_refines ge sp rs0 m0 hv (Sinput r).
+Proof.
+  wlp_simplify.
+Qed.
+Global Opaque hSinput.
+Local Hint Resolve hSinput_correct: wlp.
+
 Definition hSop_hcodes (op:operation) (lhsv: list_hsval)  (hsm: hsmem) :=
    DO hc <~ hash op_hcode;;
    DO hv <~ hash op;;
@@ -275,6 +404,19 @@ Definition hSop (op:operation) (lhsv: list_hsval)  (hsm: hsmem): ?? hsval :=
    DO hv <~ hSop_hcodes op lhsv hsm;;
    hC_hsval {| hdata:=HSop op lhsv hsm unknown_hid; hcodes :=hv |}.
 
+Lemma hSop_correct op lhsv hsm:
+  WHEN hSop op lhsv hsm ~> hv THEN forall ge sp rs0 m0 lsv sm,
+    list_sval_refines ge sp rs0 m0 lhsv lsv ->
+    smem_refines ge sp rs0 m0 hsm sm ->
+    sval_refines ge sp rs0 m0 hv (Sop op lsv sm).
+Proof.
+  wlp_simplify.
+  rewrite <- H0, <- H1.
+  auto.
+Qed.
+Global Opaque hSop.
+Local Hint Resolve hSop_correct: wlp.
+
 Definition hSload_hcodes (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval):=
    DO hc <~ hash load_hcode;;
    DO hv1 <~ hash trap;;
@@ -287,15 +429,59 @@ Definition hSload (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr
    DO hv <~ hSload_hcodes hsm trap chunk addr lhsv;;
    hC_hsval {| hdata := HSload hsm trap chunk addr lhsv unknown_hid; hcodes := hv |}.
 
+Lemma hSload_correct hsm trap chunk addr lhsv:
+  WHEN hSload hsm trap chunk addr lhsv ~> hv THEN forall ge sp rs0 m0 lsv sm,
+    list_sval_refines ge sp rs0 m0 lhsv lsv ->
+    smem_refines ge sp rs0 m0 hsm sm ->
+    sval_refines ge sp rs0 m0 hv (Sload sm trap chunk addr lsv).
+Proof.
+  wlp_simplify.
+  rewrite <- H0, <- H1.
+  auto.
+Qed.
+Global Opaque hSload.
+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,
+    list_sval_refines ge sp rs0 m0 hv Snil.
+Proof.
+  wlp_simplify.
+Qed.
+Global Opaque hSnil.
+Local Hint Resolve hSnil_correct: wlp.
+
 Definition hScons (hsv: hsval) (lhsv: list_hsval): ?? list_hsval :=
    hC_list_hsval {| hdata := HScons hsv lhsv unknown_hid; hcodes := [hsval_get_hid hsv; list_hsval_get_hid lhsv] |}.
 
+Lemma hScons_correct hsv lhsv:
+  WHEN hScons hsv lhsv ~> lhsv' THEN forall ge sp rs0 m0 sv lsv,
+    sval_refines ge sp rs0 m0 hsv sv ->
+    list_sval_refines ge sp rs0 m0 lhsv lsv ->
+    list_sval_refines ge sp rs0 m0 lhsv' (Scons sv lsv).
+Proof.
+  wlp_simplify.
+  rewrite <- H0, <- H1.
+  auto.
+Qed.
+Global Opaque hScons.
+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,
+    smem_refines ge sp rs0 m0 hm Sinit.
+Proof.
+  wlp_simplify.
+Qed.
+Global Opaque hSinit.
+Local Hint Resolve hSinit_correct: wlp.
+
 Definition hSstore_hcodes (hsm: hsmem) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval) (srce: hsval):=
    DO hv1 <~ hash chunk;;
    DO hv2 <~ hash addr;;
@@ -306,6 +492,19 @@ Definition hSstore (hsm: hsmem) (chunk: memory_chunk) (addr: addressing) (lhsv:
    DO hv <~ hSstore_hcodes hsm chunk addr lhsv srce;;
    hC_hsmem {| hdata := HSstore hsm chunk addr lhsv srce unknown_hid; hcodes := hv |}.
 
+Lemma hSstore_correct hsm chunk addr lhsv hsv:
+  WHEN hSstore hsm chunk addr lhsv hsv ~> hsm' THEN forall ge sp rs0 m0 lsv sm sv,
+    list_sval_refines ge sp rs0 m0 lhsv lsv ->
+    smem_refines ge sp rs0 m0 hsm sm ->
+    sval_refines ge sp rs0 m0 hsv sv ->
+    smem_refines ge sp rs0 m0 hsm' (Sstore sm chunk addr lsv sv).
+Proof.
+  wlp_simplify.
+  rewrite <- H0, <- H1, <- H2.
+  auto.
+Qed.
+Global Opaque hSstore.
+Local Hint Resolve hSstore_correct: wlp.
 
 Definition hsi_sreg_get (hst: PTree.t hsval) r: ?? hsval :=
    match PTree.get r hst with 
@@ -313,6 +512,18 @@ Definition hsi_sreg_get (hst: PTree.t hsval) r: ?? hsval :=
    | Some sv => RET sv
    end.
 
+Lemma hsi_sreg_get_correct hst r:
+  WHEN hsi_sreg_get hst r ~> hsv THEN forall ge sp rs0 m0 (f: reg -> sval),
+    (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 <- H0, H. auto.
+  + rewrite <- H1, H. auto.
+Qed.
+Global Opaque hsi_sreg_get.
+Local Hint Resolve hsi_sreg_get_correct: wlp.
+
 Fixpoint hlist_args (hst: PTree.t hsval) (l: list reg): ?? list_hsval :=
   match l with
   | nil => hSnil()
@@ -322,22 +533,96 @@ Fixpoint hlist_args (hst: PTree.t hsval) (l: list reg): ?? list_hsval :=
     hScons v lhsv
   end.
 
+Lemma hlist_args_correct hst l:
+  WHEN hlist_args hst l ~> lhsv THEN forall ge sp rs0 m0 (f: reg -> sval),
+    (forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (f r) rs0 m0) ->
+    list_sval_refines ge sp rs0 m0 lhsv (list_sval_inj (List.map f l)).
+Proof.
+  induction l; wlp_simplify.
+Qed.
+Global Opaque hlist_args.
+Local Hint Resolve hlist_args_correct: wlp.
+
+
 (** ** Assignment of memory *)
+Definition hslocal_set_smem (hst:hsistate_local) hm :=
+  {| hsi_smem := hm;
+     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 hsm:
+  (seval_hsmem ge sp (hsi_smem hst) rs0 m0 = None -> seval_hsmem ge sp hsm rs0 m0 = None) ->
+  hsok_local ge sp rs0 m0 (hslocal_set_smem hst hsm)
+  <-> (hsok_local ge sp rs0 m0 hst /\ seval_hsmem ge sp hsm rs0 m0 <> None).
+Proof.
+  unfold hslocal_set_smem, hsok_local; simpl; intuition.
+Qed.
+
+Lemma hslocal_set_mem_correct ge sp rs0 m0 hst st hsm sm:
+  (seval_hsmem ge sp (hsi_smem hst) rs0 m0 = None -> seval_hsmem ge sp hsm rs0 m0 = None) ->
+  hsilocal_refines ge sp rs0 m0 hst st ->
+  (hsok_local ge sp rs0 m0 hst -> smem_refines ge sp rs0 m0 hsm sm) ->
+  hsilocal_refines ge sp rs0 m0 (hslocal_set_smem hst hsm) (slocal_set_smem st sm).
+Proof.
+  intros PRESERV (OKEQ & SMEMEQ' & REGEQ) SMEMEQ.
+  split; rewrite! hsok_local_set_mem; eauto; try tauto.
+  rewrite sok_local_set_mem.
+  intuition congruence.
+Qed.
+Local Hint Resolve hslocal_set_mem_correct: wlp.
+
 Definition hslocal_store (hst: hsistate_local) chunk addr args src: ?? hsistate_local :=
    let pt := hst.(hsi_sreg) in
    DO hargs <~ hlist_args pt args;;
    DO hsrc <~ hsi_sreg_get pt src;;
    DO hm <~ hSstore hst chunk addr hargs hsrc;;
-   RET {| hsi_smem := hm;
-         hsi_ok_lsval := hsi_ok_lsval hst;
-         hsi_sreg:= hsi_sreg hst
-       |}.
+   RET (hslocal_set_smem hst hm).
+
+Lemma hslocal_store_correct hst chunk addr args src:
+  WHEN hslocal_store hst chunk addr args src ~> hst' THEN forall ge sp rs0 m0 st,
+    hsilocal_refines ge sp rs0 m0 hst st ->
+    hsilocal_refines ge sp rs0 m0 hst' (slocal_store st chunk addr args src).
+Proof.
+  wlp_simplify.
+  eapply hslocal_set_mem_correct; simpl; eauto.
+  + intros X; erewrite H1; eauto.
+    rewrite X. simplify_SOME z.
+  + unfold hsilocal_refines in * |-; intuition eauto.
+Qed.
+Global Opaque hslocal_store.
+Local Hint Resolve hslocal_store_correct: wlp.
 
 (** ** 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 ->
+  (sok_local ge sp rs0 m0 nxt -> sok_local ge sp rs0 m0 (si_local st)) ->
+  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.
+  intros (EREF & LREF & NESTED) LREFN SOK; intuition.
+  destruct NESTED as [|st0 se lse TOP NEST]; econstructor; simpl; auto.
+Qed.
+
 (** ** Assignment of registers *)
 
 (** locally new symbolic values during symbolic execution *)
@@ -346,10 +631,15 @@ Inductive root_sval: Type :=
 | Rload (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing)
 .
 
+Definition hSop_hSinit (op:operation) (lhsv: list_hsval): ?? hsval :=
+  DO hsi <~ hSinit ();;
+  hSop op lhsv hsi (** magically remove the dependency on sm ! *)
+  .
+
 Definition root_apply (rsv: root_sval) (lr: list reg) (hst: hsistate_local) : ?? hsval :=
   DO lhsv <~ hlist_args hst lr;;
   match rsv with
-  | Rop op => hSop op lhsv hst
+  | Rop op => hSop_hSinit op lhsv
   | Rload trap chunk addr => hSload hst trap chunk addr lhsv
   end.
 
@@ -363,6 +653,23 @@ Definition may_trap (rsv: root_sval) (lr: list reg): bool :=
   | _ => 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.
+
+Lemma seval_list_sval_length ge sp rs0 m0 l:
+  forall l', seval_list_sval ge sp (list_sval_inj l) rs0 m0 = Some l' ->
+  Datatypes.length l = Datatypes.length l'.
+Proof.
+  induction l.
+  - simpl. intros. inv H. reflexivity.
+  - simpl. intros. destruct (seval_sval _ _ _ _ _); [|discriminate].
+    destruct (seval_list_sval _ _ _ _ _) eqn:SLS; [|discriminate]. inv H. simpl.
+    erewrite IHl; eauto.
+Qed.
+
 (** simplify a symbolic value before assignment to a register *)
 Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hsval :=
   match rsv with
@@ -370,9 +677,8 @@ Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hs
      match is_move_operation op lr with
      | Some arg => hsi_sreg_get hst arg (** optimization of Omove *)
      | None =>
-       DO hsi <~ hSinit ();;
        DO lhsv <~ hlist_args hst lr;;
-       hSop op lhsv hsi (** magically remove the dependency on sm ! *)
+       hSop_hSinit op lhsv
      end
   | Rload _ chunk addr => 
        DO lhsv <~ hlist_args hst lr;;
@@ -391,7 +697,9 @@ Definition red_PTree_set (r: reg) (hsv: hsval) (hst: PTree.t hsval): PTree.t hsv
 Definition hslocal_set_sreg (hst: hsistate_local) (r: reg) (rsv: root_sval) (lr: list reg): ?? hsistate_local :=
   DO ok_lhsv <~
    (if may_trap rsv lr
-    then DO hv <~ root_apply rsv lr hst;; RET (hv::(hsi_ok_lsval hst))
+    then DO hv <~ root_apply rsv lr hst;;
+         XDEBUG hv (fun hv => DO hv_name <~ string_of_hashcode (hsval_get_hid hv);; RET ("-- insert undef behavior of hashcode:" +; (CamlStr hv_name))%string);;
+         RET (hv::(hsi_ok_lsval hst))
     else RET (hsi_ok_lsval hst));;
   DO simp <~ simplify rsv lr hst;;
   RET {| hsi_smem := hst;
@@ -431,7 +739,9 @@ Fixpoint hsiexec_path (path:nat) (f: function) (hst: hsistate): ?? hsistate :=
   match path with
   | O => RET hst
   | S p =>
-    DO i <~ some_or_fail ((fn_code f)!(hst.(hsi_pc))) "hsiexec_path.internal_error.1";;
+    let pc := hst.(hsi_pc) in
+    XDEBUG pc (fun pc => DO name_pc <~ string_of_Z (Zpos pc);; RET ("- sym exec node: " +; name_pc)%string);;
+    DO i <~ some_or_fail ((fn_code f)!pc) "hsiexec_path.internal_error.1";;
     DO ohst1 <~ hsiexec_inst i hst;;
     DO hst1 <~ some_or_fail ohst1 "hsiexec_path.internal_error.2";;
     hsiexec_path p f hst1
@@ -475,6 +785,51 @@ Definition hsum_left (hst: PTree.t hsval) (ros: reg + ident): ?? (hsval + ident)
   | inr s => RET (inr s)
   end.
 
+Definition hsexec_final (i: instruction) (hst: PTree.t hsval): ?? hsfval :=
+  match i with
+  | Icall sig ros args res pc =>
+    DO svos <~ hsum_left hst ros;;
+    DO sargs <~ hlist_args hst args;;
+    RET (HScall sig svos sargs res pc)
+  | Itailcall sig ros args =>
+    DO svos <~ hsum_left hst ros;;
+    DO sargs <~ hlist_args hst args;;
+    RET (HStailcall sig svos sargs)
+  | Ibuiltin ef args res pc =>
+    DO sargs <~ hbuiltin_args hst args;;
+    RET (HSbuiltin ef sargs res pc)
+  | Ijumptable reg tbl =>
+    DO sv <~ hsi_sreg_get hst reg;;
+    RET (HSjumptable sv tbl)
+  | Ireturn or =>
+    match or with
+    | Some r => DO hr <~ hsi_sreg_get hst r;; RET (HSreturn (Some hr))
+    | None => RET (HSreturn None)
+    end
+  | _ => RET (HSnone)
+  end.
+
+Definition init_hsistate_local (_:unit): ?? hsistate_local
+  := DO hm <~ hSinit ();;
+     RET {| hsi_smem := hm; hsi_ok_lsval := nil; hsi_sreg := PTree.empty hsval |}.
+
+Definition init_hsistate pc: ?? hsistate
+  := DO hst <~ init_hsistate_local ();;
+     RET {| hsi_pc := pc; hsi_exits := nil; hsi_local := hst |}.
+
+Definition hsexec (f: function) (pc:node): ?? hsstate :=
+  DO path <~ some_or_fail ((fn_path f)!pc) "hsexec.internal_error.1";;
+  DO hinit <~ init_hsistate pc;;
+  DO hst <~ hsiexec_path path.(psize) f hinit;;
+  DO i <~ some_or_fail ((fn_code f)!(hst.(hsi_pc))) "hsexec.internal_error.2";;
+  DO ohst <~ hsiexec_inst i hst;;
+  match ohst with
+  | Some hst' => RET {| hinternal := hst'; hfinal := HSnone |}
+  | None => DO hsvf <~ hsexec_final i hst.(hsi_local);;
+            RET {| hinternal := hst; hfinal := hsvf |}
+  end.
+
+End CanonBuilding.
 
 (** * The simulation test of concrete hash-consed symbolic execution *)
 
@@ -483,15 +838,6 @@ Definition phys_check {A} (x y:A) (msg: pstring): ?? unit :=
   assert_b b msg;;
   RET tt.
 
-Lemma phys_check_correct {A} (a b: A) msg:
-  WHEN phys_check a b msg ~> tt THEN
-  a = b.
-Proof.
-  wlp_simplify.
-Qed.
-Global Opaque phys_check.
-Hint Resolve phys_check_correct: wlp.
-
 Definition struct_check {A} (x y: A) (msg: pstring): ?? unit :=
   DO b <~ struct_eq x y;;
   assert_b b msg;;
@@ -513,7 +859,7 @@ Definition option_eq_check {A} (o1 o2: option A): ?? unit :=
 
 Lemma option_eq_check_correct A (o1 o2: option A): WHEN option_eq_check o1 o2 ~> _ THEN o1=o2.
 Proof.
-  wlp_simplify. congruence.
+  wlp_simplify.
 Qed.
 Global Opaque option_eq_check.
 Hint Resolve option_eq_check_correct:wlp.
@@ -554,383 +900,23 @@ Proof.
 Qed.
 Global Opaque PTree_frame_eq_check.
 
-(** hsilocal_simu_check and properties *)
-
-Definition seval_hsval ge sp hsv rs0 m0 := seval_sval ge sp (hsval_proj hsv) rs0 m0.
-Definition seval_hsmem ge sp hsm rs0 m0 := seval_smem ge sp (hsmem_proj hsm) rs0 m0.
-
-Definition hsi_sreg_eval ge sp (hst: PTree.t hsval) r rs0 m0: option val :=
-   match PTree.get r hst with
-   | None => Some (Regmap.get r rs0)
-   | Some hsv => seval_hsval ge sp hsv rs0 m0
-   end.
-
-Lemma hsi_sreg_eval_correct ge sp hst r rs0 m0:
-  WHEN hsi_sreg_get hst r ~> hv THEN
-  hsi_sreg_eval ge sp hst r rs0 m0 = seval_hsval ge sp hv rs0 m0.
-Proof.
-  wlp_simplify.
-  - unfold hsi_sreg_eval. rewrite H. reflexivity.
-  - unfold hsi_sreg_eval. rewrite H. eapply hC_hsval_correct in Hexta1.
-    simpl in Hexta1. unfold seval_hsval. rewrite <- Hexta1. simpl. reflexivity.
-Qed.
-Hint Resolve hsi_sreg_eval_correct: wlp.
-
-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).
-
-(* 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 -> seval_hsmem ge sp (hsi_smem 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)
-  /\  (forall r sv, hst ! r = Some sv -> In sv (hsi_ok_lsval hst)).
-
-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.
-
-Definition hsilocal_simu_core (oalive: option Regset.t) (hst1 hst2: hsistate_local) :=
-     incl (hsi_ok_lsval hst2) (hsi_ok_lsval hst1)
-  /\ (forall r, (match oalive with Some alive => Regset.In r alive | _ => True end) -> (* hsi_sreg_get hst2 r = hsi_sreg_get hst1 r *)
-              PTree.get r hst2 = PTree.get r hst1)
-  /\ hsi_smem hst1 = hsi_smem hst2.
-
-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. unfold seval_hsval. erewrite 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. unfold seval_hsmem. erewrite smem_eval_preserved; 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 & _ & _) GFS OKV.
-  intros sv INS. apply RSOK in INS. apply OKV in INS. erewrite hseval_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.
-
-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.
-
-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 hsmem_eval_preserved; [| eapply GFS].
-    rewrite MEMEQ1; auto. }
-  destruct of as [alive |].
-  - constructor.
-    + constructor; [assumption | constructor; [assumption|]].
-      destruct HREF2 as (B & _ & A & PT).
-      (** B, A and PT are 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. rewrite seval_partial_regset_get. unfold hsi_sreg_eval.
-      destruct (hst2 ! r) eqn:HST2; [| simpl; reflexivity].
-      unfold seval_sval_partial.
-      assert (seval_hsval ge2 sp h rs0 m0 <> None) by eauto.
-      destruct (seval_hsval ge2 sp h 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_hsval ge2 sp h rs0 m0 = hsi_sreg_eval ge2 sp hst2 r rs0 m0). {
-           unfold hsi_sreg_eval. rewrite HST2. reflexivity. }
-         rewrite H. clear H.
-         unfold hsi_sreg_eval. rewrite HST2.
-         erewrite hseval_preserved; [| eapply GFS].
-         unfold hsi_sreg_eval in B.
-         generalize (B HOK1 r); clear B; intro B.
-         rewrite <- C in B; eauto.
-         rewrite HST2 in B.
-         rewrite B, RSEQ.
-         reflexivity.
-      ++ rewrite <- RSEQ. rewrite <- B; [|assumption].
-         unfold hsi_sreg_eval. 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 hsmem_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. destruct (hst2 ! r) eqn:HST2.
-      ++ assert (seval_hsval ge2 sp h rs0 m0 = hsi_sreg_eval ge2 sp hst2 r rs0 m0). {
-           unfold hsi_sreg_eval. rewrite HST2. reflexivity. }
-         rewrite H. clear H.
-         unfold hsi_sreg_eval. rewrite HST2.
-         erewrite hseval_preserved; [| eapply GFS].
-         unfold hsi_sreg_eval in B.
-         generalize (B HOK1 r); clear B; intro B.
-         rewrite <- C in B; eauto. rewrite HST2 in B. rewrite B, RSEQ. reflexivity.
-      ++ rewrite <- RSEQ. rewrite <- B; [|assumption].
-         unfold hsi_sreg_eval. rewrite <- C; [|auto]. rewrite HST2. reflexivity.
-Qed.
-
 Definition hsilocal_simu_check hst1 hst2 : ?? unit :=
+  DEBUG("? last check");;
   phys_check (hsi_smem hst2) (hsi_smem hst1) "hsilocal_simu_check: hsi_smem sets aren't equiv";;
+  PTree_eq_check (hsi_sreg hst1) (hsi_sreg hst2);;
   Sets.assert_list_incl mk_hash_params (hsi_ok_lsval hst2) (hsi_ok_lsval hst1);;
-  PTree_eq_check (hsi_sreg hst1) (hsi_sreg hst2).
-
-Theorem hsilocal_simu_check_correct hst1 hst2:
-  WHEN hsilocal_simu_check hst1 hst2 ~> tt THEN
-  hsilocal_simu_core None hst1 hst2.
-Proof.
-  wlp_simplify. constructor; [|constructor]; [assumption | | congruence].
-  intros. unfold hsi_sreg_get. rewrite (PTree_eq_check_correct _ hst1 hst2); [|eassumption].
-  reflexivity.
-Qed.
-Hint Resolve hsilocal_simu_check_correct: wlp.
-Global Opaque hsilocal_simu_check.
-
-Definition hsilocal_frame_simu_check frame hst1 hst2 : ?? unit :=
-  phys_check (hsi_smem hst2) (hsi_smem hst1) "hsilocal_frame_simu_check: hsi_smem sets aren't equiv";;
-  Sets.assert_list_incl mk_hash_params (hsi_ok_lsval hst2) (hsi_ok_lsval hst1);;
-  PTree_frame_eq_check frame (hsi_sreg hst1) (hsi_sreg hst2).
-
-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 PTree_frame_eq_check_correct: wlp.
-Local Hint Resolve regset_elements_in: core.
-
-Theorem hsilocal_frame_simu_check_correct hst1 hst2 alive:
-  WHEN hsilocal_frame_simu_check (Regset.elements alive) hst1 hst2 ~> tt THEN
-  hsilocal_simu_core (Some alive) hst1 hst2.
-Proof.
-  wlp_simplify. constructor; [|constructor]; [assumption | | congruence].
-  intros. symmetry. eauto.
-(*   rewrite (PTree_frame_eq_check_correct _ (Regset.elements alive) hst1 hst2); [reflexivity | eassumption | ].
-  apply regset_elements_in. assumption. *)
-Qed.
-Hint Resolve hsilocal_frame_simu_check_correct: wlp.
-Global Opaque hsilocal_frame_simu_check.
-
-Definition init_hsistate_local (_:unit): ?? hsistate_local
-  := DO hm <~ hSinit ();;
-     RET {| hsi_smem := hm; hsi_ok_lsval := nil; hsi_sreg := PTree.empty hsval |}.
-
-Remark hsinit_seval_hsmem ge sp rs0 m0:
-  WHEN hSinit () ~> init THEN
-  seval_hsmem ge sp init rs0 m0 = Some m0.
-Proof.
-  wlp_simplify. unfold hSinit in Hexta. apply hC_hsmem_correct in Hexta. simpl in Hexta.
-  unfold seval_hsmem. rewrite <- Hexta. simpl. reflexivity.
-Qed.
-
-Remark init_hsistate_local_correct ge sp rs0 m0:
-  WHEN init_hsistate_local () ~> hsl THEN
-  hsilocal_refines ge sp rs0 m0 hsl init_sistate_local.
-Proof.
-  wlp_simplify.
-  constructor; constructor; simpl.
-  - intro. destruct H as (_ & SMEM & SVAL). unfold hsok_local. simpl. contradiction.
-  - intro. constructor; [simpl; auto|]. constructor; simpl; discriminate.
-  - unfold hsok_local. simpl. intros; simpl. apply hsinit_seval_hsmem. assumption.
-  - constructor.
-    + intros. simpl. unfold hsi_sreg_eval. rewrite PTree.gempty. reflexivity.
-    + intros r sv. rewrite PTree.gempty. discriminate.
-Qed.
-
-(** Simulation of exits *)
-
-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 (* FIXME - should there be something about okvals ? *).
-
-(** 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_ifso hext = si_ifso ext.
-
-Definition hsok_exit ge sp rs m hse := hsok_local ge sp rs m (hsi_elocal hse).
-
-Definition hseval_condition ge sp cond hcondargs hmem rs0 m0 :=
-  seval_condition ge sp cond (hsval_list_proj hcondargs) (hsmem_proj hmem) rs0 m0.
-
-Lemma hseval_condition_preserved ge ge' sp cond args mem rs0 m0:
-  (forall s : ident, Genv.find_symbol ge' s = Genv.find_symbol ge s) ->
-  hseval_condition ge sp cond args mem rs0 m0 = hseval_condition ge' sp cond args mem rs0 m0.
-Proof.
-  intros. unfold hseval_condition. erewrite seval_condition_preserved; [|eapply H].
-  reflexivity.
-Qed.
-
-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_local ge sp rs0 m0 (hsi_elocal hext) -> 
-        hseval_condition ge sp (hsi_cond hext) (hsi_scondargs hext) (hsi_smem (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 ((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; refine (modusponens _ _ (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. }
-  refine (modusponens _ _ (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.
+  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 revmap_check_single_correct dm pc1 pc2:
-  WHEN revmap_check_single dm pc1 pc2 ~> tt THEN
-  dm ! pc2 = Some pc1.
-Proof.
-  wlp_simplify. congruence.
-Qed.
-Hint Resolve revmap_check_single_correct: wlp.
-Global Opaque revmap_check_single.
+Definition hsilocal_frame_simu_check frame hst1 hst2 : ?? unit :=
+  DEBUG("? frame check");;
+  phys_check (hsi_smem hst2) (hsi_smem hst1) "hsilocal_frame_simu_check: hsi_smem sets aren't equiv";;
+  PTree_frame_eq_check frame (hsi_sreg hst1) (hsi_sreg hst2);;
+  Sets.assert_list_incl mk_hash_params (hsi_ok_lsval hst2) (hsi_ok_lsval hst1);;
+  DEBUG("=> frame check: OK").
 
 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";;
@@ -939,37 +925,6 @@ 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).
 
-Theorem hsiexit_simu_check_correct dm f hse1 hse2:
-  WHEN hsiexit_simu_check dm f hse1 hse2 ~> tt THEN
-  hsiexit_simu_core dm f hse1 hse2.
-Proof.
-  wlp_simplify. constructor; [| constructor; [| constructor]]. 2-4: assumption.
-  exists a. constructor. 1-2: assumption.
-Qed.
-Hint Resolve hsiexit_simu_check_correct: wlp.
-Global Opaque hsiexit_simu_check.
-
-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.
-
 Fixpoint hsiexits_simu_check (dm: PTree.t node) (f: RTLpath.function) (lhse1 lhse2: list hsistate_exit) :=
   match lhse1,lhse2 with
   | nil, nil => RET tt
@@ -979,718 +934,9 @@ Fixpoint hsiexits_simu_check (dm: PTree.t node) (f: RTLpath.function) (lhse1 lhs
   | _, _ => FAILWITH "siexists_simu_check:  lengths do not match"
   end.
 
-Theorem hsiexits_simu_check_correct dm f: forall le1 le2,
-  WHEN hsiexits_simu_check dm f le1 le2 ~> tt THEN
-  hsiexits_simu_core dm f le1 le2.
-Proof.
-  induction le1; simpl.
-  - destruct le2; wlp_simplify. constructor.
-  - destruct le2; wlp_simplify. constructor; [assumption|].
-    eapply IHle1. eassumption.
-Qed.
-Hint Resolve hsiexits_simu_check_correct: wlp.
-Global Opaque hsiexits_simu_check.
-
-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 None (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).
-
-Inductive nested_sok ge sp rs0 m0: sistate_local -> list sistate_exit -> Prop :=
-    nsok_nil st: nested_sok ge sp rs0 m0 st nil
-  | nsok_cons st se lse:
-     (sok_local ge sp rs0 m0 st -> sok_local ge sp rs0 m0 (si_elocal se)) ->
-     nested_sok ge sp rs0 m0 (si_elocal se) lse ->
-     nested_sok ge sp rs0 m0 st (se::lse).
-
-Lemma nested_sok_prop ge sp st sle rs0 m0:
-  nested_sok ge sp rs0 m0 st sle ->
-  sok_local ge sp rs0 m0 st ->
-  forall se, In se sle -> sok_local ge sp rs0 m0 (si_elocal se).
-Proof.
-  induction 1; simpl; intuition (subst; eauto).
-Qed.
-
-Lemma nested_sok_elocal ge sp rs0 m0 st2 exits:
-  nested_sok ge sp rs0 m0 st2 exits ->
-  forall st1, (sok_local ge sp rs0 m0 st1 -> sok_local ge sp rs0 m0 st2) ->
-  nested_sok ge sp rs0 m0 st1 exits.
-Proof.
-  induction 1; [intros; constructor|].
-  intros. constructor; auto.
-Qed.
-
-Lemma nested_sok_tail ge sp rs0 m0 st lx exits:
-  is_tail lx exits ->
-  nested_sok ge sp rs0 m0 st exits ->
-  nested_sok ge sp rs0 m0 st lx.
-Proof.
-  induction 1; [auto|].
-  intros. inv H0. eapply IHis_tail. eapply nested_sok_elocal; eauto.
-Qed.
-
-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)
-  /\ nested_sok ge sp rs0 m0 (si_local st) (si_exits 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 init_hsistate pc: ?? hsistate 
-  := DO hst <~ init_hsistate_local ();;
-     RET {| hsi_pc := pc; hsi_exits := nil; hsi_local := hst |}.
-
-Remark init_hsistate_correct_stat pc:
-  WHEN init_hsistate pc ~> hst THEN
-  hsistate_refines_stat hst (init_sistate pc).
-Proof.
-  wlp_simplify.
-  constructor; constructor; simpl; auto.
-Qed.
-Hint Resolve init_hsistate_correct_stat: wlp.
-
-Remark init_hsistate_correct_dyn ge sp rs0 m0 pc:
-  WHEN init_hsistate pc ~> hst THEN
-  hsistate_refines_dyn ge sp rs0 m0 hst (init_sistate pc).
-Proof.
-  unfold init_hsistate. wlp_bind hst.
-  wlp_simplify.
-  constructor; simpl; auto; [|constructor].
-  - apply list_forall2_nil.
-  - apply init_hsistate_local_correct. assumption.
-  - constructor.
-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 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,
-  (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 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.
-
 Definition hsistate_simu_check (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsistate) :=
-  revmap_check_single dm (hsi_pc hst1) (hsi_pc hst2);;
-  hsilocal_simu_check (hsi_local hst1) (hsi_local hst2);;
-  hsiexits_simu_check dm f (hsi_exits hst1) (hsi_exits hst2).
-
-Theorem hsistate_simu_check_correct dm f hst1 hst2:
-  WHEN hsistate_simu_check dm f hst1 hst2 ~> tt THEN
-  hsistate_simu_core dm f hst1 hst2.
-Proof.
-  wlp_simplify.
-  constructor; [|constructor]. 1-3: assumption.
-Qed.
-Hint Resolve hsistate_simu_check_correct: wlp.
-Global Opaque hsistate_simu_check.
-
-Definition hsi_proj (hsi: hsval + ident) := match hsi with
-  | inl hv => inl (hsval_proj hv)
-  | inr id => inr id
-  end.
-
-Fixpoint barg_proj (bhv: builtin_arg hsval) := match bhv with
-  | BA hv => BA (hsval_proj hv)
-  | BA_splitlong ba1 ba2 => BA_splitlong (barg_proj ba1) (barg_proj ba2)
-  | BA_addptr ba1 ba2 => BA_addptr (barg_proj ba1) (barg_proj ba2)
-  | BA_int i => BA_int i
-  | BA_long i => BA_long i
-  | BA_float f => BA_float f
-  | BA_single f32 => BA_single f32
-  | BA_loadstack m p => BA_loadstack m p
-  | BA_addrstack p => BA_addrstack p
-  | BA_loadglobal c i p => BA_loadglobal c i p
-  | BA_addrglobal i p => BA_addrglobal i p
-  end.
-
-Fixpoint barg_list_proj lbh := match lbh with
-  | [] => []
-  | bh::lbh => (barg_proj bh) :: (barg_list_proj lbh)
-  end.
-
-Definition option_hsval_proj oh := match oh with None => None | Some h => Some (hsval_proj h) end.
-
-Definition hfinal_proj hfv := match hfv with
-  | HSnone => Snone
-  | HScall s hvi hlv r pc => Scall s (hsi_proj hvi) (hsval_list_proj hlv) r pc
-  | HStailcall s hvi hlv => Stailcall s (hsi_proj hvi) (hsval_list_proj hlv)
-  | HSbuiltin ef lbh br pc => Sbuiltin ef (barg_list_proj lbh) br pc
-  | HSjumptable hv ln => Sjumptable (hsval_proj hv) ln
-  | HSreturn oh => Sreturn (option_hsval_proj oh)
-  end.
-
-Section HFINAL_REFINES.
-
-Variable ge: RTL.genv.
-Variable sp: val.
-Variable rs0: regset.
-Variable m0: mem.
-
-Definition sval_refines (hv: hsval) (sv: sval) := seval_hsval ge sp hv rs0 m0 = seval_sval ge sp sv rs0 m0.
-
-Definition sum_refines (hsi: hsval + ident) (si: sval + ident) :=
-  match hsi, si with
-  | inl hv, inl sv => sval_refines hv sv
-  | inr id, inr id' => id = id'
-  | _, _ => False
-  end.
-
-Inductive list_refines: list_hsval -> list_sval -> Prop :=
-  | hsnil_ref: forall h, list_refines (HSnil h) Snil
-  | hscons_ref: forall lhv lsv hv sv h,
-      list_refines lhv lsv ->
-      sval_refines hv sv ->
-      list_refines (HScons hv lhv h) (Scons sv lsv).
-
-Inductive barg_refines: builtin_arg hsval -> builtin_arg sval -> Prop :=
-  | hba_ref: forall hsv sv, sval_refines hsv sv -> barg_refines (BA hsv) (BA sv)
-  | hba_splitlong: forall bha1 bha2 ba1 ba2,
-      barg_refines bha1 ba1 -> barg_refines bha2 ba2 ->
-      barg_refines (BA_splitlong bha1 bha2) (BA_splitlong ba1 ba2)
-  | hba_addptr: forall bha1 bha2 ba1 ba2,
-      barg_refines bha1 ba1 -> barg_refines bha2 ba2 ->
-      barg_refines (BA_addptr bha1 bha2) (BA_addptr ba1 ba2)
-  | hba_int: forall i, barg_refines (BA_int i) (BA_int i)
-  | hba_long: forall l, barg_refines (BA_long l) (BA_long l)
-  | hba_float: forall f, barg_refines (BA_float f) (BA_float f)
-  | hba_single: forall s, barg_refines (BA_single s) (BA_single s)
-  | hba_loadstack: forall chk ptr, barg_refines (BA_loadstack chk ptr) (BA_loadstack chk ptr)
-  | hba_addrstack: forall ptr, barg_refines (BA_addrstack ptr) (BA_addrstack ptr)
-  | hba_loadglobal: forall chk id ptr, barg_refines (BA_loadglobal chk id ptr) (BA_loadglobal chk id ptr)
-  | hba_addrglobal: forall id ptr, barg_refines (BA_addrglobal id ptr) (BA_addrglobal id ptr).
-
-Definition option_refines ohsv osv :=
-  match ohsv, osv with
-  | Some hsv, Some sv => sval_refines hsv sv
-  | None, None => True
-  | _, _ => False
-  end.
-
-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_refines 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_refines hargs args ->
-      hfinal_refines (HStailcall s hros hargs) (Stailcall s ros args)
-  | hsbuiltin_ref: forall ef lbha lba br pc,
-      list_forall2 barg_refines lbha lba ->
-      hfinal_refines (HSbuiltin ef lbha br pc) (Sbuiltin ef lba br pc)
-  | hsjumptable_ref: forall hsv sv lpc,
-      sval_refines 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).
-
-Remark hfinal_refines_snone: hfinal_refines HSnone Snone.
-Proof. constructor. Qed.
-
-End HFINAL_REFINES.
-
-Lemma list_proj_refines_eq ge ge' sp rs0 m0: forall lsv lhsv,
-  (forall s, Genv.find_symbol ge s = Genv.find_symbol ge' s) ->
-  list_refines ge sp rs0 m0 lhsv lsv ->
-  forall lhsv' lsv',
-  list_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.
-  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.
-    assert (SVALEQ: seval_sval ge sp sv rs0 m0 = seval_sval ge' sp sv0 rs0 m0). {
-      rewrite <- H10. rewrite <- H1. unfold seval_hsval. erewrite <- seval_preserved; [| eapply GFS]. congruence.
-    } rewrite SVALEQ.
-    erewrite IHlist_refines; eauto.
-Qed.
-
-Lemma sval_refines_proj ge ge' sp rs m hsv sv hsv' sv':
-  (forall s, Genv.find_symbol ge s = Genv.find_symbol ge' s) ->
-  sval_refines ge sp rs m hsv sv ->
-  sval_refines ge' sp rs m hsv' sv' ->
-  hsval_proj hsv = hsval_proj hsv' ->
-  seval_sval ge sp sv rs m = seval_sval ge' sp sv' rs m.
-Proof.
-  intros GFS REF REF' PROJ.
-  rewrite <- REF. rewrite <- REF'. unfold seval_hsval.
-  erewrite <- seval_preserved; [| eapply GFS].
-  congruence.
-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' ->
-  barg_proj hsv = barg_proj hsv' ->
-  seval_builtin_sval ge sp sv rs0 m0 = seval_builtin_sval ge' sp sv' rs0 m0.
-Proof.
-  intro GFS. induction 1.
-  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.
-
-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.
-
-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. unfold seval_hsval.
-        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. unfold seval_hsval.
-        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.
-
-Definition hsexec_final (i: instruction) (hst: PTree.t hsval): ?? hsfval := 
-  match i with
-  | Icall sig ros args res pc => 
-    DO svos <~ hsum_left hst ros;;
-    DO sargs <~ hlist_args hst args;;
-    RET (HScall sig svos sargs res pc)
-  | Itailcall sig ros args =>
-    DO svos <~ hsum_left hst ros;;
-    DO sargs <~ hlist_args hst args;;
-    RET (HStailcall sig svos sargs)
-  | Ibuiltin ef args res pc =>
-    DO sargs <~ hbuiltin_args hst args;;
-    RET (HSbuiltin ef sargs res pc)
-  | Ijumptable reg tbl =>
-    DO sv <~ hsi_sreg_get hst reg;;
-    RET (HSjumptable sv tbl)
-  | Ireturn or => 
-    match or with
-    | Some r => DO hr <~ hsi_sreg_get hst r;; RET (HSreturn (Some hr))
-    | None => RET (HSreturn None)
-    end
-  | _ => RET (HSnone)
-  end.
-
-Lemma sval_refines_local_get ge sp rs0 m0 hsl sl r:
-  hsok_local ge sp rs0 m0 hsl ->
-  hsilocal_refines ge sp rs0 m0 hsl sl ->
-  WHEN hsi_sreg_get hsl r ~> hsv THEN
-  sval_refines ge sp rs0 m0 hsv (si_sreg sl r).
-Proof.
-  intros HOK HREF. wlp_intro hsv. unfold sval_refines.
-  erewrite <- hsi_sreg_eval_correct; eauto.
-  destruct HREF as (_ & _ & A & _). rewrite <- A; [| assumption].
-  reflexivity.
-Qed.
-
-Lemma hsum_left_correct ge sp rs0 m0 hsl sl ros:
-  hsok_local ge sp rs0 m0 hsl ->
-  hsilocal_refines ge sp rs0 m0 hsl sl ->
-  WHEN hsum_left hsl ros ~> svos THEN
-  sum_refines ge sp rs0 m0 svos (sum_left_map (si_sreg sl) ros).
-Proof.
-  intros HOK HREF. destruct ros; [| wlp_simplify].
-  wlp_bind hr. wlp_simplify. unfold sval_refines.
-  rewrite sval_refines_local_get; eauto.
-Qed.
-
-Lemma hSnil_correct:
-  WHEN hSnil () ~> shv THEN hsval_list_proj shv = Snil.
-Proof.
-  wlp_simplify. unfold hSnil in Hexta. apply hC_list_hsval_correct in Hexta.
-  simpl in *. symmetry. assumption.
-Qed.
-Global Opaque hSnil.
-Hint Resolve hSnil_correct: wlp.
-
-Lemma hScons_correct: forall lhsv hsv,
-  WHEN hScons hsv lhsv ~> lhsv' THEN
-  hsval_list_proj lhsv' = Scons (hsval_proj hsv) (hsval_list_proj lhsv).
-Proof.
-  destruct lhsv; wlp_simplify.
-  - unfold hScons in Hexta. apply hC_list_hsval_correct in Hexta.
-    simpl in *. congruence.
-  - unfold hScons in Hexta. apply hC_list_hsval_correct in Hexta. simpl in *. congruence.
-Qed.
-Global Opaque hScons.
-Hint Resolve hScons_correct: wlp.
-
-Lemma hsi_sreg_get_refines ge sp rs0 m0 hsl sl r:
-  hsok_local ge sp rs0 m0 hsl ->
-  hsilocal_refines ge sp rs0 m0 hsl sl ->
-  WHEN hsi_sreg_get hsl r ~> hsv THEN
-  sval_refines ge sp rs0 m0 hsv (si_sreg sl r).
-Proof.
-  intros HOK HREF. wlp_intro hsv. destruct HREF as (_ & _ & A & _).
-  unfold sval_refines. erewrite <- hsi_sreg_eval_correct by eassumption.
-  rewrite A by assumption. reflexivity.
-Qed.
-
-Lemma hsval_list_proj_correct ge sp rs m lsv: forall lhsv,
-  list_refines ge sp rs m lhsv lsv ->
-  forall lhsv', hsval_list_proj lhsv' = hsval_list_proj lhsv ->
-  list_refines ge sp rs m lhsv' lsv.
-Proof.
-  induction 1.
-  - intro. simpl. intros. destruct lhsv'; try discriminate. constructor.
-  - intros. simpl in H1. destruct lhsv'; try discriminate.
-    simpl in H1. inv H1. apply IHlist_refines in H4.
-    constructor; [assumption|].
-    unfold sval_refines. unfold seval_hsval. rewrite H3. assumption.
-Qed.
-Hint Resolve hsval_list_proj_correct: wlp.
-
-Lemma hsval_proj_correct ge sp rs0 m0 hsl sl hsv r:
-  hsok_local ge sp rs0 m0 hsl ->
-  hsilocal_refines ge sp rs0 m0 hsl sl ->
-  WHEN hsi_sreg_get hsl r ~> hsv' THEN
-  hsval_proj hsv = hsval_proj hsv' ->
-  sval_refines ge sp rs0 m0 hsv (si_sreg sl r).
-Proof.
-  intros HOK HREF. wlp_intro hsv'. intros PROJ.
-  unfold sval_refines. unfold seval_hsval.
-  rewrite PROJ. enough (seval_sval ge sp (hsval_proj hsv') rs0 m0 = seval_hsval ge sp hsv' rs0 m0) as ->; [|reflexivity].
-  erewrite hsi_sreg_get_refines; eauto.
-Qed.
-Hint Resolve hsval_proj_correct: wlp.
-
-Lemma hlist_args_correct ge sp rs0 m0 hsl sl:
-  hsok_local ge sp rs0 m0 hsl ->
-  hsilocal_refines ge sp rs0 m0 hsl sl ->
-  forall lr, WHEN hlist_args hsl lr ~> shv THEN
-  list_refines ge sp rs0 m0 shv (list_sval_inj (List.map (si_sreg sl) lr)).
-Proof.
-  intros HOK HREF. induction lr.
-  - simpl. wlp_simplify. destruct exta; try discriminate. constructor.
-  - simpl. wlp_bind v. wlp_bind lhsv. wlp_simplify.
-    apply IHlr in Hlhsv. clear IHlr.
-    destruct exta; try discriminate. simpl in H. inv H. constructor.
-    + eapply hsval_list_proj_correct; eauto.
-    + eapply hsval_proj_correct; eauto.
-Qed.
-Global Opaque hlist_args.
-Hint Resolve hlist_args_correct: wlp.
-
-Lemma hbuiltin_arg_correct ge sp rs0 m0 hsl sl:
-  hsok_local ge sp rs0 m0 hsl ->
-  hsilocal_refines ge sp rs0 m0 hsl sl ->
-  forall br,
-  WHEN hbuiltin_arg hsl br ~> bhsv THEN
-  barg_refines ge sp rs0 m0 bhsv (builtin_arg_map (si_sreg sl) br).
-Proof.
-  intros HOK HREF.
-  induction br.
-  all: try (wlp_simplify; constructor; auto; fail).
-  (* BA *)
-  - simpl. wlp_bind hsv. wlp_simplify. constructor. eapply hsi_sreg_get_refines; eauto.
-Qed.
-
-Lemma hbuiltin_args_correct ge sp rs0 m0 hsl sl:
-  hsok_local ge sp rs0 m0 hsl ->
-  hsilocal_refines ge sp rs0 m0 hsl sl ->
-  forall lbr,
-  WHEN hbuiltin_args hsl lbr ~> lbhsv THEN
-  list_forall2 (barg_refines ge sp rs0 m0) lbhsv (List.map (builtin_arg_map (si_sreg sl)) lbr).
-Proof.
-  intros HOK HREF.
-  induction lbr; [wlp_simplify; constructor|].
-  simpl. wlp_bind ha. wlp_bind hl. wlp_simplify.
-  constructor; [|auto]. eapply hbuiltin_arg_correct; eauto.
-Qed.
-
-Lemma hsexec_final_correct ge sp rs0 m0 hsl sl i:
-  hsok_local ge sp rs0 m0 hsl ->
-  hsilocal_refines ge sp rs0 m0 hsl sl ->
-  WHEN hsexec_final i hsl ~> hsf THEN
-  hfinal_refines ge sp rs0 m0 hsf (sexec_final i sl).
-Proof.
-  intro HOK.
-  destruct i; simpl; intros HLREF; try (wlp_simplify; apply hfinal_refines_snone).
-  (* Scall *)
-  - wlp_bind svos. wlp_bind sargs. wlp_simplify. constructor.
-    + eapply hsum_left_correct; eauto.
-    + eapply hlist_args_correct; eauto.
-  (* Stailcall *)
-  - wlp_bind svos. wlp_bind sargs. wlp_simplify. constructor.
-    + eapply hsum_left_correct; eauto.
-    + eapply hlist_args_correct; eauto.
-  (* Sbuiltin *)
-  - wlp_simplify. constructor. eapply hbuiltin_args_correct; eauto.
-  (* Sjumptable *)
-  - wlp_bind sv. wlp_simplify. constructor. eapply hsi_sreg_get_refines; eauto.
-  (* Sreturn *)
-  - destruct o.
-    -- wlp_bind sv. wlp_simplify. constructor. simpl.
-       eapply hsi_sreg_get_refines; eauto.
-    -- wlp_simplify. repeat constructor.
-Qed.
+  hsiexits_simu_check dm f (hsi_exits hst1) (hsi_exits hst2);;
+  hsilocal_simu_check (hsi_local hst1) (hsi_local hst2).
 
 Fixpoint revmap_check_list (dm: PTree.t node) (ln ln': list node): ?? unit :=
   match ln, ln' with
@@ -1701,17 +947,6 @@ Fixpoint revmap_check_list (dm: PTree.t node) (ln ln': list node): ?? unit :=
   | _, _ => FAILWITH "revmap_check_list: lists have different lengths"
   end.
 
-Lemma revmap_check_list_correct dm: forall lpc lpc',
-  WHEN revmap_check_list dm lpc lpc' ~> tt THEN
-  ptree_get_list dm lpc' = Some lpc.
-Proof.
-  induction lpc.
-  - destruct lpc'; wlp_simplify.
-  - destruct lpc'; wlp_simplify. rewrite H. rewrite H0. reflexivity.
-Qed.
-Global Opaque revmap_check_list.
-Hint Resolve revmap_check_list_correct: wlp.
-
 Definition svos_simu_check (svos1 svos2: hsval + ident) :=
   match svos1, svos2 with
   | inl sv1, inl sv2 => phys_check sv1 sv2 "svos_simu_check: sval mismatch"
@@ -1719,62 +954,18 @@ Definition svos_simu_check (svos1 svos2: hsval + ident) :=
   | _, _ => FAILWITH "svos_simu_check: type mismatch"
   end.
 
-Lemma svos_simu_check_correct svos1 svos2:
-  WHEN svos_simu_check svos1 svos2 ~> tt THEN
-  svos1 = svos2.
-Proof.
-  destruct svos1; destruct svos2; wlp_simplify; try wlp_absurd.
-  all: congruence.
-Qed.
-Global Opaque svos_simu_check.
-Hint Resolve svos_simu_check_correct: wlp.
-
 Fixpoint builtin_arg_simu_check (bs bs': builtin_arg hsval) :=
-  match bs with
-  | BA sv =>
-    match bs' with
-    | BA sv' => phys_check sv sv' "builtin_arg_simu_check: sval mismatch"
-    | _ => FAILWITH "builtin_arg_simu_check: BA mismatch"
-    end
-  | BA_splitlong lo hi =>
-    match bs' with
-    | BA_splitlong lo' hi' =>
-        builtin_arg_simu_check lo lo';;
-        builtin_arg_simu_check hi hi'
-    | _ => FAILWITH "builtin_arg_simu_check: BA_splitlong mismatch"
-    end
-  | BA_addptr b1 b2 =>
-    match bs' with
-    | BA_addptr b1' b2' =>
-        builtin_arg_simu_check b1 b1';;
-        builtin_arg_simu_check b2 b2'
-    | _ => FAILWITH "builtin_arg_simu_check: BA_addptr mismatch"
-    end
-  | bs => struct_check bs bs' "builtin_arg_simu_check: basic mismatch"
+  match bs, bs' with
+  | BA sv, BA sv' => phys_check sv sv' "builtin_arg_simu_check: sval mismatch"
+  | BA_splitlong lo hi, BA_splitlong lo' hi' => 
+      builtin_arg_simu_check lo lo';;
+      builtin_arg_simu_check hi hi'
+  | BA_addptr b1 b2, BA_addptr b1' b2' => 
+      builtin_arg_simu_check b1 b1';;
+      builtin_arg_simu_check b2 b2'
+  | _, _ => struct_check bs bs' "builtin_arg_simu_check: basic mismatch"
   end.
 
-Lemma builtin_arg_simu_check_correct: forall bs1 bs2,
-  WHEN builtin_arg_simu_check bs1 bs2 ~> tt THEN
-  barg_proj bs1 = barg_proj bs2.
-Proof.
-  induction bs1.
-  all: try (intros; simpl; wlp_simplify; subst; reflexivity).
-  (* BA *)
-  - destruct bs2; wlp_simplify; try wlp_absurd. congruence.
-  (* BA_splitlong *)
-  - destruct bs2; try (wlp_simplify; wlp_absurd). simpl.
-    wlp_bind b1. wlp_intro b2.
-    rewrite IHbs1_1 by eassumption. rewrite IHbs1_2 by eassumption.
-    reflexivity.
-  (* BA_addptr *)
-  - destruct bs2; try (wlp_simplify; wlp_absurd). simpl.
-    wlp_bind b1. wlp_intro b2.
-    rewrite IHbs1_1 by eassumption. rewrite IHbs1_2 by eassumption.
-    reflexivity.
-Qed.
-Global Opaque builtin_arg_simu_check.
-Hint Resolve builtin_arg_simu_check_correct: wlp.
-
 Fixpoint list_builtin_arg_simu_check lbs1 lbs2 :=
   match lbs1, lbs2 with
   | nil, nil => RET tt
@@ -1784,22 +975,9 @@ Fixpoint list_builtin_arg_simu_check lbs1 lbs2 :=
   | _, _ => FAILWITH "list_builtin_arg_simu_check: length mismatch"
   end.
 
-Lemma list_builtin_arg_simu_check_correct: forall lbs1 lbs2,
-  WHEN list_builtin_arg_simu_check lbs1 lbs2 ~> tt THEN
-  barg_list_proj lbs1 = barg_list_proj lbs2.
-Proof.
-  induction lbs1.
-  - wlp_simplify. destruct lbs2; [simpl; reflexivity|].
-    simpl in Hexta. wlp_absurd.
-  - destruct lbs2; wlp_simplify; try wlp_absurd.
-    congruence.
-Qed.
-Global Opaque list_builtin_arg_simu_check.
-Hint Resolve list_builtin_arg_simu_check_correct: wlp.
-
-Definition sfval_simu_check (dm: PTree.t node) (f: RTLpath.function) (opc1 opc2: node) (fv1 fv2: hsfval) :=
+Definition sfval_simu_check (dm: PTree.t node) (f: RTLpath.function) (pc1 pc2: node) (fv1 fv2: hsfval) :=
   match fv1, fv2 with
-  | HSnone, HSnone => revmap_check_single dm opc1 opc2
+  | HSnone, HSnone => revmap_check_single dm pc1 pc2
   | HScall sig1 svos1 lsv1 res1 pc1, HScall sig2 svos2 lsv2 res2 pc2 =>
       revmap_check_single dm pc1 pc2;;
       phys_check sig1 sig2 "sfval_simu_check: Scall different signatures";;
@@ -1823,534 +1001,10 @@ Definition sfval_simu_check (dm: PTree.t node) (f: RTLpath.function) (opc1 opc2:
   | _, _ => FAILWITH "sfval_simu_check: structure mismatch"
   end.
 
-
-Theorem sfval_simu_check_correct dm f opc1 opc2 fv1 fv2:
-  WHEN sfval_simu_check dm f opc1 opc2 fv1 fv2 ~> tt THEN
-  hfinal_simu_core dm f opc1 opc2 fv1 fv2.
-Proof.
-  destruct fv1; destruct fv2; try (wlp_simplify; simpl in Hexta; wlp_absurd).
-  (* HScall *)
-  - simpl. wlp_bind u1 REVMAP. wlp_bind u2 SIG. wlp_bind u3 RES.
-    wlp_bind u4 SVOS. wlp_intro u5 LSV.
-    apply phys_check_correct in SIG. apply phys_check_correct in RES.
-    apply revmap_check_single_correct in REVMAP. apply phys_check_correct in LSV.
-    apply svos_simu_check_correct in SVOS. subst. repeat (constructor; auto).
-  (* HStailcall *)
-  - simpl. wlp_bind u1 SIG. wlp_bind u2 SVOS. wlp_intro u3 LSV.
-    apply phys_check_correct in SIG. apply phys_check_correct in LSV.
-    apply svos_simu_check_correct in SVOS. subst. repeat (constructor; auto).
-  (* HSbuiltin *)
-  - simpl. wlp_bind u1 RMAP. wlp_bind u2 EF. wlp_bind u3 RES.
-    wlp_intro u4 SARGS.
-    apply phys_check_correct in EF. apply phys_check_correct in RES.
-    apply list_builtin_arg_simu_check_correct in SARGS. apply revmap_check_single_correct in RMAP.
-    subst. repeat (constructor; auto).
-  (* HSjumptable *)
-  - simpl. wlp_simplify. subst. constructor; auto.
-  (* HSreturn *)
-  - wlp_simplify. subst. reflexivity.
-Qed.
-Hint Resolve sfval_simu_check_correct: wlp.
-Global Opaque hfinal_simu_core.
-
-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))
-.
-
-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 (hsi_pc (hinternal hst1)) (hsi_pc (hinternal hst2)) (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|]. 1-2: eassumption.
-  destruct SREF1 as (PC1 & _). destruct SREF2 as (PC2 & _). rewrite <- PC1. rewrite <- PC2.
-  eapply FSIMU.
-Qed.
-
 Definition hsstate_simu_check (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsstate) :=
   hsistate_simu_check dm f (hinternal hst1) (hinternal hst2);;
   sfval_simu_check dm f (hsi_pc hst1) (hsi_pc hst2) (hfinal hst1) (hfinal hst2).
 
-Theorem hsstate_simu_check_correct dm f hst1 hst2:
-  WHEN hsstate_simu_check dm f hst1 hst2 ~> tt THEN
-  hsstate_simu_core dm f hst1 hst2.
-Proof.
-  wlp_simplify. constructor. 1-2: assumption.
-Qed.
-Hint Resolve hsstate_simu_check_correct: wlp.
-Global Opaque hsstate_simu_core. 
-
-Definition seval_list_hsval ge sp lhsv rs m := seval_list_sval ge sp (hsval_list_proj lhsv) rs m.
-
-Definition hok_args ge sp rs0 m0 hst lr :=
-  WHEN hlist_args (hsi_sreg hst) lr ~> lhsv THEN
-  hsok_local ge sp rs0 m0 hst -> 
-  (seval_list_hsval ge sp lhsv rs0 m0 <> None).
-
-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 ->
-  (sok_local ge sp rs0 m0 nxt -> sok_local ge sp rs0 m0 (si_local st)) ->
-  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.
-  intros (EREF & LREF & NESTED) LREFN SOK; intuition.
-  destruct NESTED as [|st0 se lse TOP NEST]; econstructor; simpl; auto.
-Qed.
-
-(* Completely lost on that one *)
-(* Lemma hsok_local_set_sreg ge sp rs0 m0 hst r (rsv:root_sval) lr:
-  WHEN hslocal_set_sreg hst r rsv lr ~> hst' THEN
-  hok_args ge sp rs0 m0 hst lr ->
-  hsok_local ge sp rs0 m0 hst'
-  <-> (hsok_local ge sp rs0 m0 hst /\ (WHEN root_apply rsv lr hst ~> hsv THEN seval_hsval ge sp hsv rs0 m0 <> None)).
-Proof.
-  unfold hslocal_set_sreg. wlp_bind lhsvok. wlp_bind hsv. wlp_ret hst'.
-  intros HOK.
-  destruct may_trap eqn: MAYTRAP.
-  - wlp_hbind hv. wlp_hret. constructor.
-    + unfold hsok_local. simpl. intro. constructor.
-      * intros. apply H. right. assumption.
-      * wlp_intro hsv'. apply H.
-
-
-  unfold hok_args, hsok_local. simpl.
-
-  unfold hslocal_set_sreg, ok_args, hsok_local; simpl.
-  destruct may_trap eqn: MAYTRAP; simpl; intuition (subst; eauto).
-  eapply may_trap_correct; eauto.
-Qed. *)
-
-Lemma seval_list_sval_proj ge sp rs0 m0: forall lhsv lsv,
-  list_refines ge sp rs0 m0 lhsv lsv ->
-  seval_list_sval ge sp (hsval_list_proj lhsv) rs0 m0 = seval_list_sval ge sp lsv rs0 m0.
-Proof.
-  induction lhsv.
-  - destruct lsv; simpl; intros H; [reflexivity | inv H].
-  - destruct lsv; [intro H; inv H|].
-    intros. inv H. simpl. erewrite IHlhsv; eauto.
-    rewrite H6. reflexivity.
-Qed.
-
-Lemma hSop_correct ge sp rs0 m0 op lhsv lsv hst st:
-  WHEN hSop op lhsv (hsi_smem hst) ~> hsv THEN
-  hsok_local ge sp rs0 m0 hst ->
-  list_refines ge sp rs0 m0 lhsv lsv ->
-  hsilocal_refines ge sp rs0 m0 hst st ->
-  seval_hsval ge sp hsv rs0 m0 = seval_sval ge sp (Sop op lsv (si_smem st)) rs0 m0.
-Proof.
-  wlp_simplify. apply hC_hsval_correct in Hexta1. simpl in *. unfold seval_hsval.
-  rewrite <- Hexta1. simpl. clear Hexta1.
-  erewrite seval_list_sval_proj; eauto. clear H0.
-  destruct H1 as (A & B & C & D). rewrite <- B; eauto.
-Qed.
-
-(** Version of hSop_correct with weaker hypothesis *)
-Lemma hSop_correct_mem ge sp rs0 m0 op lhsv lsv hsm sm:
-  WHEN hSop op lhsv hsm ~> hsv THEN
-  seval_hsmem ge sp hsm rs0 m0 = seval_smem ge sp sm rs0 m0 ->
-  list_refines ge sp rs0 m0 lhsv lsv ->
-  seval_hsval ge sp hsv rs0 m0 = seval_sval ge sp (Sop op lsv sm) rs0 m0.
-Proof.
-  wlp_simplify. apply hC_hsval_correct in Hexta1. simpl in *. unfold seval_hsval.
-  rewrite <- Hexta1. simpl. clear Hexta1.
-  erewrite seval_list_sval_proj; eauto. clear H0.
-  rewrite <- H. eauto.
-Qed.
-
-Lemma hSload_correct ge sp rs0 m0 lhsv lsv hst st trap addr chunk:
-  WHEN hSload (hsi_smem hst) trap chunk addr lhsv ~> hsv THEN
-  hsok_local ge sp rs0 m0 hst ->
-  list_refines ge sp rs0 m0 lhsv lsv ->
-  hsilocal_refines ge sp rs0 m0 hst st ->
-  seval_hsval ge sp hsv rs0 m0 = seval_sval ge sp (Sload (si_smem st) trap chunk addr lsv) rs0 m0.
-Proof.
-  wlp_simplify. apply hC_hsval_correct in Hexta3. simpl in *. unfold seval_hsval.
-  rewrite <- Hexta3. simpl. clear Hexta3.
-  erewrite seval_list_sval_proj; eauto. clear H0.
-  destruct H1 as (A & B & C & D). rewrite <- B; eauto.
-Qed.
-
-Lemma hsinit_sinit ge sp rs0 m0:
-  WHEN hSinit () ~> init THEN
-  seval_hsmem ge sp init rs0 m0 = seval_smem ge sp Sinit rs0 m0.
-Proof.
-  wlp_intro init. eapply hsinit_seval_hsmem in Hinit; eauto.
-Qed.
-
-Lemma simplify_correct (rsv: root_sval) lr (ge: RTL.genv) (sp: val) rs0 m0 v hst st:
-  WHEN root_apply rsv lr hst ~> hsv THEN
-  hsok_local ge sp rs0 m0 hst ->
-  hsilocal_refines ge sp rs0 m0 hst st ->
-  seval_hsval ge sp hsv rs0 m0 = Some v ->
-  WHEN simplify rsv lr hst ~> hsv' THEN
-  seval_hsval ge sp hsv' rs0 m0 = Some v.
-Proof.
-  wlp_bind lhsv. wlp_intro hsv. intros HOK HREF HEVAL.
-  eapply hlist_args_correct in Hlhsv; eauto.
-  destruct rsv; simpl.
-  (* Rop *)
-  - exploit hSop_correct; eauto. intros EVALMOV. clear Hlhsv. clear Hhsv.
-    destruct (is_move_operation _ _) eqn:IMOVE.
-    + apply is_move_operation_correct in IMOVE. inv IMOVE.
-      rewrite <- HEVAL. rewrite EVALMOV. wlp_intro hsv'.
-      simpl. destruct HREF as (A & B & C & D). rewrite <- C; eauto.
-      rewrite hsi_sreg_eval_correct; eauto.
-      destruct (seval_hsval ge sp hsv' rs0 m0); [|reflexivity].
-      apply A in HOK. destruct HOK as (_ & MOK & _).
-      destruct (seval_smem _ _ _ _ _); [reflexivity|contradiction].
-    + clear IMOVE. wlp_bind hsm. wlp_bind lhsv'. wlp_intro hsv'.
-      eapply hlist_args_correct in Hlhsv'; eauto.
-      rewrite hSop_correct_mem; eauto; [|eapply hsinit_sinit; eauto].
-      clear Hlhsv'. clear Hhsv'. rewrite <- HEVAL. rewrite EVALMOV.
-      admit. (** Voir avec Sylvain - je ne sais plus où on en est sur les dépendances mémoires avec les op *)
-  (* Rload *)
-  - exploit hSload_correct; eauto. intros EVALLOAD.
-    wlp_bind lhsv'. wlp_intro hsv'. eapply hlist_args_correct in Hlhsv'; eauto.
-    rewrite hSload_correct; eauto. rewrite EVALLOAD in HEVAL.
-    destruct trap; simpl; auto. simpl in HEVAL.
-    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.
-    rewrite HEVAL. reflexivity.
-Admitted.
-
-Lemma hSop_preserves_hok ge sp op lhsv rs m hst:
-  seval_list_hsval ge sp lhsv rs m <> None ->
-  hsok_local ge sp rs m hst ->
-  WHEN hSop op lhsv hst ~> hsv THEN
-  seval_hsval ge sp hsv rs m <> None.
-Proof.
-Abort.
-(* FIXME - that theorem is false! *)
-
-Lemma root_apply_preserves_hok ge sp rs m hst lr rsv:
-  hok_args ge sp rs m hst lr ->
-  hsok_local ge sp rs m hst ->
-  WHEN root_apply rsv lr hst ~> hsv THEN
-  seval_hsval ge sp hsv rs m <> None.
-Proof.
-  intros ARGSOK HOKL. unfold root_apply. wlp_bind lhsv. wlp_intro hsv.
-  destruct rsv.
-  - (* eapply hSop_preserves_hok; eauto. *)
-Abort.
-(* FIXME - the theorem is wrong *)
-
-Lemma hsok_local_set_sreg ge sp rs0 m0 hst r (rsv:root_sval) lr:
-  hok_args ge sp rs0 m0 hst lr ->
-  WHEN hslocal_set_sreg hst r rsv lr ~> hst' THEN
-  hsok_local ge sp rs0 m0 hst'
-  <-> (hsok_local ge sp rs0 m0 hst /\ 
-    (WHEN root_apply rsv lr hst ~> hsv' THEN seval_hsval ge sp hsv' rs0 m0 <> None)).
-Proof.
-  intros HOK. unfold hslocal_set_sreg.
-  wlp_bind ok_lhsv. wlp_bind hsv'. wlp_intro hst'. wlp_hret.
-  constructor.
-  - intros HOKL.
-    assert (HOKL': hsok_local ge sp rs0 m0 hst). {
-      destruct may_trap.
-      * wlp_hbind hv. wlp_hret. unfold hsok_local.
-        intros. apply HOKL. simpl. right. assumption.
-      * wlp_hret. unfold hsok_local.
-        intros. apply HOKL. simpl. assumption. } 
-    split; [assumption|].
-    wlp_intro hsv2. admit. (* eapply root_apply_preserves_hok; eauto. FIXME - wrong *)
-  - intros (HOKL & RAPP). destruct (may_trap _ _) eqn:MAYT.
-    + wlp_hbind hv. wlp_hret. unfold hsok_local. simpl. intros. inv H.
-      * admit. (* eapply root_apply_preserves_hok; eauto. FIXME - wrong *)
-      * apply HOKL. assumption.
-    + wlp_hret. apply HOKL.
-Admitted.
-
-Lemma slocal_set_sreg_preserves_sok ge sp rs m st r sv:
-  sok_local ge sp rs m st <-> sok_local ge sp rs m (slocal_set_sreg st r sv).
-Proof.
-Admitted.
-
-Lemma root_apply_none ge sp rsv rs m hst lr:
-  hsok_local ge sp rs m hst ->
-  WHEN root_apply rsv lr hst ~> hsv THEN
-  seval_hsval ge sp hsv rs m <> None.
-Proof.
-Admitted.
-
-Lemma hslocal_set_sreg_preserves_smem ge sp hst rs0 m0 r rsv lr:
-  WHEN hslocal_set_sreg hst r rsv lr ~> hst' THEN
-  seval_hsmem ge sp hst' rs0 m0 = seval_hsmem ge sp hst rs0 m0.
-Proof.
-Admitted.
-
-Lemma hslocal_set_sreg_preserves_hsok ge sp rs m hst r rsv lr:
-  WHEN hslocal_set_sreg hst r rsv lr ~> hst' THEN
-  hsok_local ge sp rs m hst <-> hsok_local ge sp rs m hst'.
-Proof.
-Admitted.
-
-Lemma red_PTree_set_correct (r r0:reg) (hsv: hsval) (hst: PTree.t hsval) ge sp rs0 m0:
-  hsi_sreg_eval ge sp (red_PTree_set r hsv hst) r0 rs0 m0 = hsi_sreg_eval ge sp (PTree.set r hsv hst) r0 rs0 m0.
-Proof.
-  destruct hsv; simpl; auto.
-  destruct (Pos.eq_dec r r1); auto.
-  subst; unfold hsi_sreg_eval.
-  destruct (Pos.eq_dec r0 r1); auto.
-  - subst; rewrite PTree.grs, PTree.gss; simpl; auto.
-  - rewrite PTree.gro, PTree.gso; simpl; auto.
-Qed.
-
-(** TODO - express some lemma about root_apply_correct and simplify_correct
-  * Figure out how to prove this stuff *)
-Lemma hslocal_set_sreg_correct ge sp rs0 m0 hst st r (rsv:root_sval) lr sv':
-  hsilocal_refines ge sp rs0 m0 hst st ->
-  hok_args ge sp rs0 m0 hst lr ->
-  ( hsok_local ge sp rs0 m0 hst ->
-    WHEN root_apply rsv lr hst ~> hsv THEN
-    seval_sval ge sp sv' rs0 m0 = seval_hsval ge sp hsv rs0 m0) ->
-  WHEN hslocal_set_sreg hst r rsv lr ~> hst' THEN
-  hsilocal_refines ge sp rs0 m0 hst' (slocal_set_sreg st r sv').
-Proof.
-  intros HREF HOK REVAL. wlp_intro hst'.
-  unfold hsilocal_refines. split; [|split; [|split]].
-  + symmetry. eapply iff_trans. eapply hsok_local_set_sreg; eauto.
-    constructor.
-    * intros (HOKL & REVAL'). apply slocal_set_sreg_preserves_sok.
-      destruct HREF as (A & _). apply A in HOKL. assumption.
-    * intros SOKL. rewrite <- slocal_set_sreg_preserves_sok in SOKL.
-      destruct HREF as (A & _). apply A in SOKL.
-      split; [assumption|].
-      eapply root_apply_none; eauto.
-  + intros HOKL. simpl. rewrite hslocal_set_sreg_preserves_smem; eauto.
-    destruct HREF as (_ & A & _). rewrite A; auto.
-    eapply hslocal_set_sreg_preserves_hsok; eauto.
-  + intros HOKL. simpl. intro r0. unfold hslocal_set_sreg in Hhst'.
-    wlp_hbind ok_lhsv. wlp_hbind hsv'. wlp_hret. simpl.
-    rewrite red_PTree_set_correct. unfold hsi_sreg_eval.
-    destruct (Pos.eq_dec r r0).
-    * subst. rewrite PTree.gss. (* Something about simplify_correct ? *) admit.
-    * admit.
-  + admit.
-
-(*   intros (ROK & RMEM & RVAL) OKA RSV.
-  unfold hsilocal_refines; simpl. rewrite! hsok_local_set_sreg; eauto. split.
-  + rewrite <- ROK in RSV; rewrite sok_local_set_sreg; eauto.
-    intuition congruence.
-  + split; try tauto.
-    intros (HOKL & RSV2) r0.
-    rewrite red_PTree_set_correct.
-    rewrite hsi_sreg_eval_correct. unfold hsi_sreg_get.
-    destruct (Pos.eq_dec r r0).
-    * subst. rewrite PTree.gss, RSV; auto.
-      destruct (seval_sval ge sp (rsv lsv (hsi_smem hst))) eqn: RSV3; simpl; try congruence.
-      eapply simplify_correct; eauto.
-    * intros; rewrite PTree.gso; auto.
-      rewrite <- RVAL, hsi_sreg_eval_correct; auto. *)
-Admitted.
-
-
-
-
-Lemma seval_list_hsval_refines ge sp rs0 m0 hst st lr:
-  hsok_local ge sp rs0 m0 hst ->
-  hsilocal_refines ge sp rs0 m0 hst st ->
-  WHEN hlist_args hst lr ~> lhsv THEN
-  seval_list_hsval ge sp lhsv rs0 m0 = seval_list_sval ge sp (list_sval_inj (List.map (si_sreg st) lr)) rs0 m0.
-Proof.
-  intros OKL HLREF. wlp_simplify.
-  destruct lr.
-  - simpl in *. inv H. reflexivity.
-  - inv H. simpl. unfold seval_list_hsval. simpl. rewrite H4. erewrite seval_list_sval_proj; eauto.
-Qed.
-
-Lemma seval_list_sval_none ge sp (srs: reg -> sval) rs0 m0: forall lr,
-  (forall r, seval_sval ge sp (srs r) rs0 m0 <> None) ->
-  seval_list_sval ge sp (list_sval_inj (List.map srs lr)) rs0 m0 <> None.
-Proof.
-  induction lr.
-  - simpl. discriminate.
-  - intro SR. simpl. destruct (seval_sval _ _ _ _ _) eqn:V.
-    2: { apply SR in V. inv V. }
-    destruct (seval_list_sval _ _ _ _ _) eqn:LV.
-    2: { apply IHlr in SR. assumption. }
-    discriminate.
-Qed.
-
-Lemma refines_okargs ge sp rs0 m0 hst st lr: 
-  hsistate_refines_dyn ge sp rs0 m0 hst st ->
-  hok_args ge sp rs0 m0 (hsi_local hst) lr.
-Proof.
-  unfold hok_args.
-  intros (_ & HLREF & _). wlp_intro lhsv LHSV. intros OK.
-  exploit hlist_args_correct; eauto. intro LREF.
-  erewrite seval_list_hsval_refines; eauto.
-  destruct HLREF as (OKEQ & _ & _).
-  rewrite <- OKEQ in OK.
-  destruct OK as (_ & _ & OK).
-  apply seval_list_sval_none. assumption.
-Qed.
-
-(* Local Hint Resolve refines_okargs: core. *)
-Lemma hsiexec_inst_correct_dyn ge sp rs0 m0 i hst st hst' st':
-  WHEN hsiexec_inst i hst ~> ohst' THEN
-  ohst' = 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.
-  (* Inop *)
-  - wlp_simplify. inv H. inv H0. auto.
-  (* Iop *)
-  - simpl. wlp_bind next NEXT. wlp_simplify. inv H. inv H0.
-    eapply hsist_set_local_correct_dyn; eauto.
-    + destruct H1 as (A & B & C).
-      eapply hslocal_set_sreg_correct; eauto.
-      { eapply refines_okargs. repeat (econstructor; eauto). }
-      simpl. intro HOK. unfold root_apply. wlp_bind lhsv LHSV. wlp_intro hsv HSV.
-      eapply hlist_args_correct in LHSV; eauto.
-      erewrite hSop_correct; eauto. simpl. reflexivity.
-    + unfold sok_local; simpl; intros (PRE & MEM & REG).
-      intuition.
-      generalize (REG r0); clear REG.
-      destruct (Pos.eq_dec r r0); simpl; intuition (subst; eauto).
-  (* Iload *)
-  - simpl.  wlp_bind next NEXT. wlp_simplify. inv H. inv H0.
-    eapply hsist_set_local_correct_dyn; eauto.
-    + destruct H1 as (A & B & C).
-      eapply hslocal_set_sreg_correct; eauto.
-      { eapply refines_okargs. repeat (econstructor; eauto). }
-      simpl. intro HOK. unfold root_apply. wlp_bind lhsv LHSV. wlp_intro hsv HSV.
-      eapply hlist_args_correct in LHSV; eauto.
-      erewrite hSload_correct; eauto. simpl. reflexivity.
-    + unfold sok_local; simpl; intros (PRE & MEM & REG).
-      intuition.
-      generalize (REG r0); clear REG.
-      destruct (Pos.eq_dec r r0); simpl; intuition (subst; eauto).
-  (* Istore *)
-  - simpl. wlp_bind next NEXT. wlp_simplify. inv H. inv H0.
-    eapply hsist_set_local_correct_dyn; eauto.
-    + admit. (** TODO - port hslocal_set_smem_correct *)
-    + unfold sok_local; simpl; intuition.
-  (* Icall *)
-  - admit.
-  (* Itailcall *)
-  - admit.
-  (* Ibuiltin *)
-  - admit.
-  (* Icond *)
-  - admit.
-  (* Ijumptable *)
-  - admit.
-  (* Ireturn *)
-  - admit.
-Admitted.
-
-
-(* PROOF from RTLpathSE_impl.v
-  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; intros.
-      erewrite seval_list_sval_refines; eauto.
-      erewrite seval_smem_refines; eauto.
-    + unfold sok_local; simpl; intros (PRE & MEM & REG).
-      intuition.
-      generalize (REG r0); clear REG.
-      destruct (Pos.eq_dec r r0); simpl; intuition (subst; eauto).
-  - (* Iload *)
-    eapply hsist_set_local_correct_dyn; eauto.
-    + eapply hslocal_set_sreg_correct; eauto.
-      simpl; intros.
-      erewrite seval_list_sval_refines; eauto.
-      erewrite seval_smem_refines; eauto.
-    + unfold sok_local; simpl; intros (PRE & MEM & REG).
-      intuition.
-      generalize (REG r0); clear REG.
-      destruct (Pos.eq_dec r r0); simpl; intuition (subst; eauto).
-  - (* Istore *)
-    eapply hsist_set_local_correct_dyn; eauto.
-    + eapply hslocal_set_mem_correct; eauto.
-      * simpl. simplify_SOME x.
-      * intros. simpl.
-        erewrite seval_list_sval_refines; eauto.
-        erewrite seval_smem_refines; eauto.
-        erewrite seval_sval_refines; eauto.
-    + unfold sok_local; simpl; intuition.
-  - (* Icond *)
-    destruct REF as (EXREF & LREF & NEST).
-    split.
-    + constructor; simpl; auto.
-      constructor; simpl; auto.
-      intros; erewrite seval_condition_refines; eauto.
-      unfold seval_condition.
-      erewrite seval_list_sval_refines; eauto.
-    + split; simpl; auto.
-      destruct NEST as [|st0 se lse TOP NEST];
-      econstructor; simpl; auto; constructor; auto.
-Qed.  *)
-
-Definition hsexec (f: function) (pc:node): ?? hsstate :=
-  DO path <~ some_or_fail ((fn_path f)!pc) "hsexec.internal_error.1";;
-  DO hinit <~ init_hsistate pc;;
-  DO hst <~ hsiexec_path path.(psize) f hinit;;
-  DO i <~ some_or_fail ((fn_code f)!(hst.(hsi_pc))) "hsexec.internal_error.2";;
-  DO ohst <~ hsiexec_inst i hst;;
-  match ohst with
-  | Some hst' => RET {| hinternal := hst'; hfinal := HSnone |}
-  | None => DO hsvf <~ hsexec_final i hst.(hsi_local);;
-            RET {| hinternal := hst; hfinal := hsvf |}
-  end.
-
-(**
- * init_hsistate_correct_stat : OK
- * init_hsistate_correct_dyn : OK
- * hsexec_final_correct : OK
- * hsiexec_inst_correct_dyn : TODO
- * hsiexec_path_correct_dyn : TODO
- * hfinal_refines_snone : OK
- *)
-
-(* 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:
-  WHEN hsexec f pc ~> hst THEN
-  exists st, sexec f pc = Some st /\ hsstate_refines hst st.
-Proof. Admitted.
-(*   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. *)
-
-End CanonBuilding.
-
 Definition simu_check_single (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) (m: node * node): ?? unit :=
   let (pc2, pc1) := m in
   (* creating the hash-consing tables *)
@@ -2359,7 +1013,9 @@ Definition simu_check_single (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpa
   DO hC_hsmem <~ hCons hSMEM;;
   let hsexec := hsexec hC_sval.(hC) hC_list_hsval.(hC) hC_hsmem.(hC) in
   (* performing the hash-consed executions *)
+  XDEBUG pc1 (fun pc => DO name_pc <~ string_of_Z (Zpos pc);; RET ("entry-point of input superblock: " +; name_pc)%string);;
   DO hst1 <~ hsexec f pc1;;
+  XDEBUG pc2 (fun pc => DO name_pc <~ string_of_Z (Zpos pc);; RET ("entry-point of output superblock: " +; name_pc)%string);;
   DO hst2 <~ hsexec tf pc2;;
   (* comparing the executions *)
   hsstate_simu_check dm f hst1 hst2.
@@ -2367,26 +1023,6 @@ Definition simu_check_single (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpa
 Lemma simu_check_single_correct dm tf f pc1 pc2:
   WHEN simu_check_single dm f tf (pc2, pc1) ~> _ THEN
   sexec_simu dm f tf pc1 pc2.
-Proof.
-  unfold simu_check_single.
-  wlp_bind hC_sval HSVAL. wlp_bind hC_list_hsval HLSVAL.
-  wlp_bind hC_hsmem HSMEM. wlp_bind hst1 HSEXEC1. wlp_bind hst2 HSEXEC2.
-  wlp_intro u HSIMU.
-  unfold sexec_simu. intros st1 SEXEC. explore.
-  assert (TODO1: forall hs rhsv, hC hC_sval hs ~~> rhsv -> hsval_proj (hdata hs) = hsval_proj rhsv)
-    by admit.
-  assert (TODO2: forall hs rhsv, hC hC_list_hsval hs ~~> rhsv -> hsval_list_proj (hdata hs) = hsval_list_proj rhsv)
-    by admit.
-  assert (TODO3: forall hs rhsv, hC hC_hsmem hs ~~> rhsv -> hsmem_proj (hdata hs) = hsmem_proj rhsv)
-    by admit.
-  exploit hsexec_correct; eauto.
-  intros (st2 & SEXEC2 & REF2).
-  exploit hsexec_correct. 4: eapply HSEXEC1. all: eauto.
-  intros (st0 & SEXEC1 & REF1).
-  rewrite SEXEC1 in SEXEC. inv SEXEC.
-  eexists. split; eauto.
-  intros ctx. eapply hsstate_simu_check_correct in HSIMU; eauto.
-  eapply hsstate_simu_core_correct; eauto.
 Admitted.
 Global Opaque simu_check_single.
 Global Hint Resolve simu_check_single_correct: wlp.
@@ -2414,7 +1050,7 @@ Global Hint Resolve simu_check_rec_correct: wlp.
 
 Definition imp_simu_check (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function): ?? unit :=
    simu_check_rec dm f tf (PTree.elements dm);;
-   println("simu_check OK!").
+   DEBUG("simu_check OK!").
 
 Local Hint Resolve PTree.elements_correct: core.
 Lemma imp_simu_check_correct dm f tf:
diff --git a/kvx/lib/RTLpathSE_theory.v b/kvx/lib/RTLpathSE_theory.v
index 22b471fd..dd0b706e 100644
--- a/kvx/lib/RTLpathSE_theory.v
+++ b/kvx/lib/RTLpathSE_theory.v
@@ -469,6 +469,11 @@ Definition slocal_set_smem (st:sistate_local) (sm:smem) :=
 Definition sist_set_local (st: sistate) (pc: node) (nxt: sistate_local): sistate :=
    {| si_pc := pc; si_exits := st.(si_exits); si_local:= nxt |}.
 
+Definition slocal_store st chunk addr args src : sistate_local :=
+   let args := list_sval_inj (List.map (si_sreg st) args) in
+   let src := si_sreg st src in
+   let sm := Sstore (si_smem st) chunk addr args src
+   in slocal_set_smem st sm.
 
 Definition siexec_inst (i: instruction) (st: sistate): option sistate := 
   match i with
@@ -485,9 +490,7 @@ Definition siexec_inst (i: instruction) (st: sistate): option sistate :=
       let next := slocal_set_sreg prev dst (Sload prev.(si_smem) trap chunk addr vargs) in
       Some (sist_set_local st pc' next)
   | Istore chunk addr args src pc' =>
-      let prev := st.(si_local) in
-      let vargs := list_sval_inj (List.map prev.(si_sreg) args) in
-      let next := slocal_set_smem prev (Sstore prev.(si_smem) chunk addr vargs (prev.(si_sreg) src)) in
+      let next := slocal_store st.(si_local) chunk addr args src in
       Some (sist_set_local st pc' next)
    | Icond cond args ifso ifnot _ =>
       let prev := st.(si_local) in
@@ -497,7 +500,6 @@ Definition siexec_inst (i: instruction) (st: sistate): option sistate :=
   | _ => None (* TODO jumptable ? *)
   end.
 
-
 Lemma seval_list_sval_inj ge sp l rs0 m0 (sreg: reg -> sval) rs: 
    (forall r : reg, seval_sval ge sp (sreg r) rs0 m0 = Some (rs # r)) ->
    seval_list_sval ge sp (list_sval_inj (map sreg l)) rs0 m0 = Some (rs ## l).