path: root/kvx/lib/RTLpathSE_impl_junk.v

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

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

Local Open Scope error_monad_scope.
Local Open Scope option_monad_scope.

Require Export Impure.ImpHCons.
Export Notations.
Import HConsing.

Local Open Scope impure.

Import ListNotations.
Local Open Scope list_scope.

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

Definition DEBUG (s: pstring): ?? unit := XDEBUG tt (fun _ => RET s).

(** * Implementation of Data-structure use in Hash-consing *)

(** ** Implementation of symbolic values/symbolic memories with hash-consing data *)

Inductive hsval :=
  | HSinput (r: reg) (hid: hashcode)
  | HSop (op: operation) (lhsv: list_hsval)  (hsm: hsmem) (hid: hashcode)
  | HSload (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval) (hid: hashcode)
with list_hsval :=
  | HSnil (hid: hashcode)
  | HScons (hsv: hsval) (lhsv: list_hsval) (hid: hashcode)
with hsmem :=
  | HSinit (hid: hashcode)
  | HSstore (hsm: hsmem) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval) (srce: hsval) (hid:hashcode).

Scheme hsval_mut := Induction for hsval Sort Prop
with list_hsval_mut := Induction for list_hsval Sort Prop
with hsmem_mut := Induction for hsmem Sort Prop.

Definition hsval_get_hid (hsv: hsval): hashcode :=
  match hsv with
  | HSinput _ hid => hid
  | HSop _ _ _ hid => hid
  | HSload _ _ _ _ _ hid => hid
  end.

Definition list_hsval_get_hid (lhsv: list_hsval): hashcode :=
  match lhsv with
  | HSnil hid => hid
  | HScons _ _ hid => hid
  end.

Definition hsmem_get_hid (hsm: hsmem): hashcode :=
  match hsm with
  | HSinit hid => hid
  | HSstore _ _ _ _ _ hid => hid
  end.

Definition hsval_set_hid (hsv: hsval) (hid: hashcode): hsval :=
  match hsv with
  | HSinput r _ => HSinput r hid
  | HSop o lhsv hsm _ => HSop o lhsv hsm hid
  | HSload hsm trap chunk addr lhsv _ => HSload hsm trap chunk addr lhsv hid
  end.

Definition list_hsval_set_hid (lhsv: list_hsval) (hid: hashcode): list_hsval :=
  match lhsv with
  | HSnil _ => HSnil hid
  | HScons hsv lhsv _ => HScons hsv lhsv hid
  end.

Definition hsmem_set_hid (hsm: hsmem) (hid: hashcode): hsmem :=
  match hsm with
  | HSinit _ => HSinit hid
  | 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: 
    [hash_eq] must be consistent with the "hashed" constructors defined above.

  We expect that hashinfo values in the code of these "hashed" constructors verify:
    (hash_eq (hdata x) (hdata y) ~> true) <-> (hcodes x)=(hcodes y)
*)


Definition hsval_hash_eq (sv1 sv2: hsval): ?? bool :=
  match sv1, sv2 with
  | HSinput r1 _, HSinput r2 _ => struct_eq r1 r2 (* NB: really need a struct_eq here ? *)
  | HSop op1 lsv1 sm1 _, HSop op2 lsv2 sm2 _  =>
     DO b1 <~ phys_eq lsv1 lsv2;;
     DO b2 <~ phys_eq sm1 sm2;;
     if b1 && b2 
     then struct_eq op1 op2 (* NB: really need a struct_eq here ? *)
     else RET false
  | HSload sm1 trap1 chk1 addr1 lsv1 _, HSload sm2 trap2 chk2 addr2 lsv2 _ =>
     DO b1 <~ phys_eq lsv1 lsv2;;
     DO b2 <~ phys_eq sm1 sm2;;
     DO b3 <~ struct_eq trap1 trap2;;
     DO b4 <~ struct_eq chk1 chk2;;
     if b1 && b2 && b3 && b4
     then struct_eq addr1 addr2
     else RET false
  | _,_ => RET false
  end.


Lemma and_true_split a b: a && b = true <-> a = true /\ b = true.
Proof.
  destruct a; simpl; intuition.
Qed.

Lemma hsval_hash_eq_correct x y:
  WHEN hsval_hash_eq x y ~> b THEN 
   b = true -> hsval_set_hid x unknown_hid = hsval_set_hid y unknown_hid.
Proof.
  destruct x, y; wlp_simplify; try (rewrite !and_true_split in *); intuition; subst; try congruence.
Qed.
Global Opaque hsval_hash_eq.
Local Hint Resolve hsval_hash_eq_correct: wlp.

Definition list_hsval_hash_eq (lsv1 lsv2: list_hsval): ?? bool :=
  match lsv1, lsv2 with
  | HSnil _, HSnil _ => RET true
  | HScons sv1 lsv1' _, HScons sv2 lsv2' _  =>
     DO b <~ phys_eq lsv1' lsv2';;
     if b 
     then phys_eq sv1 sv2
     else RET false
  | _,_ => RET false
  end.

Lemma list_hsval_hash_eq_correct x y:
  WHEN list_hsval_hash_eq x y ~> b THEN 
   b = true -> list_hsval_set_hid x unknown_hid = list_hsval_set_hid y unknown_hid.
Proof.
  destruct x, y; wlp_simplify; try (rewrite !and_true_split in *); intuition; subst; try congruence.
Qed.
Global Opaque list_hsval_hash_eq.
Local Hint Resolve list_hsval_hash_eq_correct: wlp.

Definition hsmem_hash_eq (sm1 sm2: hsmem): ?? bool :=
  match sm1, sm2 with
  | HSinit _, HSinit _ => RET true
  | HSstore sm1 chk1 addr1 lsv1 sv1 _, HSstore sm2 chk2 addr2 lsv2 sv2 _ =>
     DO b1 <~ phys_eq lsv1 lsv2;;
     DO b2 <~ phys_eq sm1 sm2;;
     DO b3 <~ phys_eq sv1 sv2;;
     DO b4 <~ struct_eq chk1 chk2;;
     if b1 && b2 && b3 && b4
     then struct_eq addr1 addr2
     else RET false
  | _,_ => RET false
  end.

Lemma hsmem_hash_eq_correct x y:
  WHEN hsmem_hash_eq x y ~> b THEN 
   b = true -> hsmem_set_hid x unknown_hid = hsmem_set_hid y unknown_hid.
Proof.
  destruct x, y; wlp_simplify; try (rewrite !and_true_split in *); intuition; subst; try congruence.
Qed.
Global Opaque hsmem_hash_eq.
Local Hint Resolve hsmem_hash_eq_correct: wlp.


Definition hSVAL: hashP hsval := {| hash_eq := hsval_hash_eq; get_hid:=hsval_get_hid; set_hid:=hsval_set_hid |}. 
Definition hLSVAL: hashP list_hsval := {| hash_eq := list_hsval_hash_eq; get_hid:= list_hsval_get_hid; set_hid:= list_hsval_set_hid |}.
Definition hSMEM: hashP hsmem := {| hash_eq := hsmem_hash_eq; get_hid:= hsmem_get_hid; set_hid:= hsmem_set_hid |}.

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


(** Symbolic final value -- from hash-consed values
  It does not seem useful to hash-consed these final values (because they are final).
*)
Inductive hsfval :=
  | HSnone
  | HScall (sig: signature) (svos: hsval + ident) (lsv: list_hsval) (res: reg) (pc: node)
  | HStailcall (sig: signature) (svos: hsval + ident) (lsv: list_hsval)
  | HSbuiltin (ef: external_function) (sargs: list (builtin_arg hsval)) (res: builtin_res reg) (pc: node)
  | HSjumptable (sv: hsval) (tbl: list node)
  | HSreturn (res: option hsval)
.

(** ** Implementation of symbolic states 
*)

(** name : Hash-consed Symbolic Internal state local.  *)
Record hsistate_local := 
  { 
    (** [hsi_smem] represents the current smem symbolic evaluations.
        (we can recover the previous one from smem)  *)
    hsi_smem:> hsmem;
    (** For the values in registers:
        1) we store a list of sval evaluations
        2) we encode the symbolic regset by a PTree *)
    hsi_ok_lsval: list hsval;
    hsi_sreg:> PTree.t hsval
  }.

(* Syntax and semantics of symbolic exit states *)
Record hsistate_exit := mk_hsistate_exit
  { hsi_cond: condition; hsi_scondargs: list_hsval; hsi_elocal: hsistate_local; hsi_ifso: node }.


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

(** ** Syntax and Semantics of symbolic state *)
Record hsstate := { hinternal:> hsistate; hfinal: hsfval }.

(** ** Refinement Definitions: from refinement of symbolic values, memories, local/exit/internal/final. *)

Fixpoint hsval_proj hsv :=
  match hsv with
  | HSinput r _ => Sinput r
  | HSop op hl hm _ => Sop op (hsval_list_proj hl) (hsmem_proj hm)
  | HSload hm t chk addr hl _ => Sload (hsmem_proj hm) t chk addr (hsval_list_proj hl)
  end
with hsval_list_proj hl :=
  match hl with
  | HSnil _ => Snil
  | HScons hv hl _ => Scons (hsval_proj hv) (hsval_list_proj hl)
  end
with hsmem_proj hm :=
  match hm with
  | HSinit _ => Sinit
  | 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).

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

Lemma hsval_set_hid_correct x y ge sp rs0 m0:
  hsval_set_hid x unknown_hid = hsval_set_hid y unknown_hid ->
  seval_hsval ge sp x rs0 m0 = seval_hsval ge sp y rs0 m0.
Proof.
  destruct x, y; intro H; inversion H; subst; simpl; auto.
Qed.
Local Hint Resolve hsval_set_hid_correct: core.

Lemma list_hsval_set_hid_correct x y ge sp rs0 m0:
  list_hsval_set_hid x unknown_hid = list_hsval_set_hid y unknown_hid ->
  seval_list_hsval ge sp x rs0 m0 = seval_list_hsval ge sp y rs0 m0.
Proof.
  destruct x, y; intro H; inversion H; subst; simpl; auto.
Qed.
Local Hint Resolve list_hsval_set_hid_correct: core.

Lemma hsmem_set_hid_correct x y ge sp rs0 m0:
  hsmem_set_hid x unknown_hid = hsmem_set_hid y unknown_hid ->
  seval_hsmem ge sp x rs0 m0 = seval_hsmem ge sp y rs0 m0.
Proof.
  destruct x, y; intro H; inversion H; subst; simpl; auto.
Qed.
Local Hint Resolve hsmem_set_hid_correct: core.

Definition hsi_sreg_proj (hst: PTree.t hsval) r: sval :=
   match PTree.get r hst with
   | None => Sinput r
   | Some hsv => hsval_proj hsv
   end.

Definition hsi_sreg_eval ge sp hst r := seval_sval ge sp (hsi_sreg_proj hst r).

Definition hsok_local ge sp rs0 m0 (hst: hsistate_local) : Prop :=
     (forall hsv, List.In hsv (hsi_ok_lsval hst) -> seval_hsval ge sp hsv rs0 m0 <> None)
  /\ (seval_hsmem ge sp (hst.(hsi_smem)) rs0 m0 <> None).

(* 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 m b ofs, seval_smem ge sp st.(si_smem) rs0 m0 = Some m -> Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs)
  .

Lemma hsilocal_refines_sreg ge sp rs0 m0 hst st:
  hsilocal_refines ge sp rs0 m0 hst st -> hsok_local ge sp rs0 m0 hst -> forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (si_sreg st r) rs0 m0.
Proof.
  unfold hsilocal_refines; intuition.
Qed.
Local Hint Resolve hsilocal_refines_sreg: core.

Lemma hsilocal_refines_valid_pointer ge sp rs0 m0 hst st:
  hsilocal_refines ge sp rs0 m0 hst st -> forall m b ofs, seval_smem ge sp st.(si_smem) rs0 m0 = Some m -> Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs.
Proof.
  unfold hsilocal_refines; intuition.
Qed.
Local Hint Resolve hsilocal_refines_valid_pointer: core.

Lemma hsilocal_refines_smem_refines ge sp rs0 m0 hst st:
  hsilocal_refines ge sp rs0 m0 hst st -> hsok_local ge sp rs0 m0 hst -> smem_refines ge sp rs0 m0 (hsi_smem hst) (st.(si_smem)).
Proof.
  unfold hsilocal_refines; intuition.
Qed.
Local Hint Resolve hsilocal_refines_smem_refines: core.

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

Lemma hsistate_refines_dyn_exits ge sp rs0 m0 hst st:
  hsistate_refines_dyn ge sp rs0 m0 hst st -> hsiexits_refines_dyn ge sp rs0 m0 (hsi_exits hst) (si_exits st).
Proof.
  unfold hsistate_refines_dyn; intuition.
Qed.
Local Hint Resolve hsistate_refines_dyn_exits: core.

Lemma hsistate_refines_dyn_local ge sp rs0 m0 hst st:
  hsistate_refines_dyn ge sp rs0 m0 hst st -> hsilocal_refines ge sp rs0 m0 (hsi_local hst) (si_local st).
Proof.
  unfold hsistate_refines_dyn; intuition.
Qed.
Local Hint Resolve hsistate_refines_dyn_local: core.

Lemma hsistate_refines_dyn_nested ge sp rs0 m0 hst st:
  hsistate_refines_dyn ge sp rs0 m0 hst st -> nested_sok ge sp rs0 m0 (si_local st) (si_exits st).
Proof.
  unfold hsistate_refines_dyn; intuition.
Qed.
Local Hint Resolve hsistate_refines_dyn_nested: core.

Definition hfinal_proj (hfv: hsfval) : sfval := 
  match hfv with
  | HSnone => Snone
  | HScall s hvi hlv r pc => Scall s (sum_left_map hsval_proj hvi) (hsval_list_proj hlv) r pc
  | HStailcall s hvi hlv => Stailcall s (sum_left_map hsval_proj hvi) (hsval_list_proj hlv)
  | HSbuiltin ef lbh br pc => Sbuiltin ef (List.map (builtin_arg_map hsval_proj) lbh) br pc
  | HSjumptable hv ln => Sjumptable (hsval_proj hv) ln
  | HSreturn oh => Sreturn (option_map hsval_proj oh)
  end.

Section HFINAL_REFINES.

Variable ge: RTL.genv.
Variable sp: val.
Variable rs0: regset.
Variable m0: mem.

Definition option_refines (ohsv: option hsval) (osv: option sval) :=
  match ohsv, osv with
  | Some hsv, Some sv => sval_refines ge sp rs0 m0 hsv sv
  | None, None => True
  | _, _ => False
  end.

Definition sum_refines (hsi: hsval + ident) (si: sval + ident) :=
  match hsi, si with
  | inl hv, inl sv => sval_refines ge sp rs0 m0 hv sv
  | inr id, inr id' => id = id'
  | _, _ => False
  end.

Definition bargs_refines (hargs: list (builtin_arg hsval)) (args: list (builtin_arg sval)): Prop :=
  seval_list_builtin_sval ge sp (List.map (builtin_arg_map hsval_proj) hargs) rs0 m0 = seval_list_builtin_sval ge sp args rs0 m0.

Inductive hfinal_refines: hsfval -> sfval -> Prop :=
  | hsnone_ref: hfinal_refines HSnone Snone
  | hscall_ref: forall hros ros hargs args s r pc,
      sum_refines hros ros ->
      list_sval_refines ge sp rs0 m0 hargs args ->
      hfinal_refines (HScall s hros hargs r pc) (Scall s ros args r pc)
  | hstailcall_ref: forall hros ros hargs args s,
      sum_refines hros ros ->
      list_sval_refines ge sp rs0 m0 hargs args ->
      hfinal_refines (HStailcall s hros hargs) (Stailcall s ros args)
  | hsbuiltin_ref: forall ef lbha lba br pc,
      bargs_refines lbha lba ->
      hfinal_refines (HSbuiltin ef lbha br pc) (Sbuiltin ef lba br pc)
  | hsjumptable_ref: forall hsv sv lpc,
      sval_refines ge sp rs0 m0 hsv sv -> hfinal_refines (HSjumptable hsv lpc) (Sjumptable sv lpc)
  | hsreturn_ref: forall ohsv osv,
      option_refines ohsv osv -> hfinal_refines (HSreturn ohsv) (Sreturn osv).

End HFINAL_REFINES.

Definition hsstate_refines (hst: hsstate) (st:sstate): Prop :=
   hsistate_refines_stat (hinternal hst) (internal st)
  /\ (forall ge sp rs0 m0, hsistate_refines_dyn ge sp rs0 m0 (hinternal hst) (internal st))
  /\ forall ge sp rs0 m0, 
      hsok_local ge sp rs0 m0 (hsi_local (hinternal hst)) (* hypothesis added by Sylvain, because needed to prove hsexec_correct ! *) 
      -> hfinal_refines ge sp rs0 m0 (hfinal hst) (final st).

(** * Implementation of symbolic execution *)
Section CanonBuilding.

Variable hC_hsval: hashinfo hsval -> ?? hsval.

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

Definition reg_hcode := 1.
Definition op_hcode := 2.
Definition load_hcode := 3.

Definition hSinput_hcodes (r: reg) :=
   DO hc <~ hash reg_hcode;;
   DO hv <~ hash r;;
   RET [hc;hv].
Extraction Inline hSinput_hcodes.

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;;
   RET [hc;hv;list_hsval_get_hid lhsv; hsmem_get_hid hsm].
Extraction Inline hSop_hcodes.

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
    (LR: list_sval_refines ge sp rs0 m0 lhsv lsv)
    (MR: smem_refines ge sp rs0 m0 hsm sm),
    sval_refines ge sp rs0 m0 hv (Sop op lsv sm).
Proof.
  wlp_simplify.
  rewrite <- LR, <- MR.
  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;;
   DO hv2 <~ hash chunk;;
   DO hv3 <~ hash addr;;
   RET [hc; hsmem_get_hid hsm; hv1; hv2; hv3; list_hsval_get_hid lhsv].
Extraction Inline hSload_hcodes.

Definition hSload (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval): ?? hsval :=
   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
    (LR: list_sval_refines ge sp rs0 m0 lhsv lsv)
    (MR: 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 <- LR, <- MR.
  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:
  WHEN hSnil() ~> 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
    (VR: sval_refines ge sp rs0 m0 hsv sv)
    (LR: list_sval_refines ge sp rs0 m0 lhsv lsv),
    list_sval_refines ge sp rs0 m0 lhsv' (Scons sv lsv).
Proof.
  wlp_simplify.
  rewrite <- VR, <- LR.
  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:
  WHEN hSinit() ~> 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;;
   RET [hsmem_get_hid hsm; hv1; hv2; list_hsval_get_hid lhsv; hsval_get_hid srce].
Extraction Inline hSstore_hcodes.

Definition hSstore (hsm: hsmem) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval) (srce: hsval): ?? hsmem :=
   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
    (LR: list_sval_refines ge sp rs0 m0 lhsv lsv)
    (MR: smem_refines ge sp rs0 m0 hsm sm)
    (VR: 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 <- LR, <- MR, <- VR.
  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 
   | None => hSinput r
   | 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)
    (RR: forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (f r) rs0 m0),
    sval_refines ge sp rs0 m0 hsv (f r).
Proof.
  unfold hsi_sreg_eval, hsi_sreg_proj; wlp_simplify; rewrite <- RR; try_simplify_someHyps.
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()
  | r::l =>
    DO v <~ hsi_sreg_get hst r;;
    DO lhsv <~ hlist_args hst l;;
    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)
    (RR: 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) ->
  (forall m b ofs, seval_smem ge sp sm rs0 m0 = Some m -> Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs) ->
  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 SMVALID (OKEQ & SMEMEQ' & REGEQ & MVALID) SMEMEQ.
  split; rewrite! hsok_local_set_mem; simpl; eauto; try tauto.
  rewrite sok_local_set_mem.
  intuition congruence.
Qed.

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 (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
    (REF: 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 *; 
    simplify_SOME z; intuition. 
    erewrite <- Mem.storev_preserv_valid; [| eauto].
    eauto.
  + 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 *)
Inductive root_sval: Type :=
| Rop (op: operation)
| Rload (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing)
.

Definition root_apply (rsv: root_sval) (lr: list reg) (st: sistate_local): sval :=
  let lsv := list_sval_inj (List.map (si_sreg st) lr) in
  let sm := si_smem st in
  match rsv with
  | Rop op => Sop op lsv sm
  | Rload trap chunk addr => Sload sm trap chunk addr lsv
  end.
Coercion root_apply: root_sval >-> Funclass.

Definition hSop_hSinit (op:operation) (lhsv: list_hsval): ?? hsval :=
  DO hsi <~ hSinit ();;
  hSop op lhsv hsi (** magically remove the dependency on sm ! *)
  .

Lemma hSop_hSinit_correct op lhsv:
  WHEN hSop_hSinit op lhsv ~> hv THEN forall ge sp rs0 m0 lsv sm m
   (MEM: seval_smem ge sp sm rs0 m0 = Some m)
   (MVALID: forall b ofs, Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs)
   (LR: list_sval_refines ge sp rs0 m0 lhsv lsv),
   sval_refines ge sp rs0 m0 hv (Sop op lsv sm).
Proof.
  wlp_simplify.
  erewrite H0; [ idtac | eauto | eauto ].
  rewrite H, MEM.
  destruct (seval_list_sval _ _ lsv _); try congruence.
  eapply op_valid_pointer_eq; eauto.
Qed.
Global Opaque hSop_hSinit.
Local Hint Resolve hSop_hSinit_correct: wlp.

Definition root_happly (rsv: root_sval) (lr: list reg) (hst: hsistate_local) : ?? hsval :=
  DO lhsv <~ hlist_args hst lr;;
  match rsv with
  | Rop op => hSop_hSinit op lhsv
  | Rload trap chunk addr => hSload hst trap chunk addr lhsv
  end.

Lemma root_happly_correct (rsv: root_sval) lr hst:
  WHEN root_happly rsv lr hst ~> hv' THEN forall ge sp rs0 m0 st
    (REF:hsilocal_refines ge sp rs0 m0 hst st)
    (OK:hsok_local ge sp rs0 m0 hst),
    sval_refines ge sp rs0 m0 hv' (rsv lr st).
Proof.
   unfold hsilocal_refines, root_apply, root_happly; destruct rsv; wlp_simplify.
   unfold sok_local in *.
   generalize (H0 ge sp rs0 m0 (list_sval_inj (map (si_sreg st) lr)) (si_smem st)); clear H0.
   destruct (seval_smem ge sp (si_smem st) rs0 m0) as [m|] eqn:X; eauto.
   intuition congruence.
Qed.
Global Opaque root_happly.
Hint Resolve root_happly_correct: wlp.

Local Open Scope lazy_bool_scope.

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

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

Lemma seval_list_sval_length ge sp rs0 m0 (f: reg -> sval) (l:list reg):
  forall l', seval_list_sval ge sp (list_sval_inj (List.map f 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.

Lemma may_trap_correct (ge: RTL.genv) (sp:val) (rsv: root_sval) (rs0: regset) (m0: mem) (lr: list reg) st:
  may_trap rsv lr = false -> 
  seval_list_sval ge sp (list_sval_inj (List.map (si_sreg st) lr)) rs0 m0 <> None ->
  seval_smem ge sp (si_smem st) rs0 m0 <> None ->
  seval_sval ge sp (rsv lr st) rs0 m0 <> None.
Proof.
  destruct rsv; simpl; try congruence.
  - rewrite lazy_orb_negb_false. intros (TRAP1 & TRAP2) OK1 OK2.
    explore; try congruence.
    eapply is_trapping_op_sound; eauto.
    erewrite <- seval_list_sval_length; eauto.
    apply Nat.eqb_eq in TRAP2.
    assumption.
  - intros X OK1 OK2.
    explore; try congruence.
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
  | Rop op =>
     match is_move_operation op lr with
     | Some arg => hsi_sreg_get hst arg (** optimization of Omove *)
     | None =>
       DO lhsv <~ hlist_args hst lr;;
       hSop_hSinit op lhsv
     end
  | Rload _ chunk addr => 
       DO lhsv <~ hlist_args hst lr;;
       hSload hst NOTRAP chunk addr lhsv
  end.

Lemma simplify_correct rsv lr hst:
  WHEN simplify rsv lr hst ~> hv THEN forall ge sp rs0 m0 st
    (REF: hsilocal_refines ge sp rs0 m0 hst st)
    (OK0: hsok_local ge sp rs0 m0 hst)
    (OK1: seval_sval ge sp (rsv lr st) rs0 m0 <> None),
    sval_refines ge sp rs0 m0 hv (rsv lr st).
Proof.
  destruct rsv; simpl; auto.
  - (* Rop *)
    destruct (is_move_operation _ _) eqn: Hmove; wlp_simplify.
    + exploit is_move_operation_correct; eauto.
      intros (Hop & Hlsv); subst; simpl in *.
      simplify_SOME z.
      * erewrite H; eauto.
      * try_simplify_someHyps; congruence.
      * congruence.
    + clear Hmove.
      generalize (H0 ge sp rs0 m0 (list_sval_inj (map (si_sreg st) lr)) (si_smem st)); clear H0.
      destruct (seval_smem ge sp (si_smem st) rs0 m0) as [m|] eqn:X; eauto.
      intro H0; clear H0; simplify_SOME z; congruence. (* absurd case *)
  - (* Rload *)
    destruct trap; wlp_simplify.
    erewrite H0; eauto.
    erewrite H; eauto.
    erewrite hsilocal_refines_smem_refines; eauto.
    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.
    destruct (Mem.loadv _ _ _); try congruence.
Qed.
Global Opaque simplify.
Local Hint Resolve simplify_correct: wlp.

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

Lemma red_PTree_set_correct (r r0:reg) hsv hst 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, hsi_sreg_proj.
  destruct (Pos.eq_dec r0 r1); auto.
  - subst; rewrite PTree.grs, PTree.gss; simpl; auto.
  - rewrite PTree.gro, PTree.gso; simpl; auto.
Qed.

Lemma red_PTree_set_refines (r r0:reg) hsv hst sv st ge sp rs0 m0:
 hsilocal_refines ge sp rs0 m0 hst st ->
 sval_refines ge sp rs0 m0 hsv sv ->
 hsok_local ge sp rs0 m0 hst ->
 hsi_sreg_eval ge sp (red_PTree_set r hsv hst) r0 rs0 m0 = seval_sval ge sp (if Pos.eq_dec r r0 then sv else si_sreg st r0) rs0 m0.
Proof.
  intros; rewrite red_PTree_set_correct.
  exploit hsilocal_refines_sreg; eauto.
  unfold hsi_sreg_eval, hsi_sreg_proj.
  destruct (Pos.eq_dec r r0); auto.
  - subst. rewrite PTree.gss; simpl; auto.
  - rewrite PTree.gso; simpl; eauto.
Qed.

Lemma sok_local_set_sreg (rsv:root_sval) ge sp rs0 m0 st r lr:
  sok_local ge sp rs0 m0 (slocal_set_sreg st r (rsv lr st))
  <-> (sok_local ge sp rs0 m0 st /\ seval_sval ge sp (rsv lr st) rs0 m0 <> None).
Proof.
  unfold slocal_set_sreg, sok_local; simpl; split.
  + intros ((SVAL0 & PRE) & SMEM & SVAL).
    repeat (split; try tauto).
    - intros r0; generalize (SVAL r0); clear SVAL; destruct (Pos.eq_dec r r0); try congruence.
    - generalize (SVAL r); clear SVAL; destruct (Pos.eq_dec r r); try congruence.
  + intros ((PRE & SMEM & SVAL0) & SVAL).
    repeat (split; try tauto; eauto).
    intros r0;  destruct (Pos.eq_dec r r0); try congruence.
Qed.

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_happly 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;
         hsi_ok_lsval := ok_lhsv;
         hsi_sreg := red_PTree_set r simp (hsi_sreg hst) |}.

Lemma hslocal_set_sreg_correct hst r rsv lr:
  WHEN hslocal_set_sreg hst r rsv lr ~> hst' THEN forall ge sp rs0 m0 st
    (REF: hsilocal_refines ge sp rs0 m0 hst st),
    hsilocal_refines ge sp rs0 m0 hst' (slocal_set_sreg st r (rsv lr st)).
Proof.
  wlp_simplify.
  + (* may_trap ~> true *)
    assert (X: sok_local ge sp rs0 m0 (slocal_set_sreg st r (rsv lr st)) <->
               hsok_local ge sp rs0 m0 {| hsi_smem := hst; hsi_ok_lsval := exta :: hsi_ok_lsval hst; hsi_sreg := red_PTree_set r exta0 hst |}).
    { rewrite sok_local_set_sreg; generalize REF.
      intros (OKeq & MEM & REG & MVALID); rewrite OKeq; clear OKeq.
      unfold hsok_local; simpl; intuition (subst; eauto);
      erewrite <- H0 in *; eauto; unfold hsok_local; simpl; intuition eauto.
    }
    unfold hsilocal_refines; simpl; split; auto.
    rewrite <- X, sok_local_set_sreg. intuition eauto.
    - destruct REF; intuition eauto.
    - generalize REF; intros (OKEQ & _). rewrite OKEQ in * |-; erewrite red_PTree_set_refines; eauto.
  + (* may_trap ~> false *)
    assert (X: sok_local ge sp rs0 m0 (slocal_set_sreg st r (rsv lr st)) <->
               hsok_local ge sp rs0 m0 {| hsi_smem := hst; hsi_ok_lsval := hsi_ok_lsval hst; hsi_sreg := red_PTree_set r exta hst |}).
    { 
      rewrite sok_local_set_sreg; generalize REF.
      intros (OKeq & MEM & REG & MVALID); rewrite OKeq.
      unfold hsok_local; simpl; intuition (subst; eauto).
      assert (X0:hsok_local ge sp rs0 m0 hst). { unfold hsok_local; intuition. }
      exploit may_trap_correct; eauto.
      * intro X1; eapply seval_list_sval_inj_not_none; eauto.
        assert (X2: sok_local ge sp rs0 m0 st). { intuition. }
        unfold sok_local in X2; intuition eauto.
      * rewrite <- MEM; eauto.
    }
    unfold hsilocal_refines; simpl; split; auto.
    rewrite <- X, sok_local_set_sreg. intuition eauto.
    - destruct REF; intuition eauto.
    - generalize REF; intros (OKEQ & _). rewrite OKEQ in * |-; erewrite red_PTree_set_refines; eauto.
Qed.
Global Opaque hslocal_set_sreg.
Local Hint Resolve hslocal_set_sreg_correct: wlp.

(** ** Execution of one instruction *)

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


Remark hsiexec_inst_None_correct i hst:
  WHEN hsiexec_inst i hst ~> o THEN forall st, o = None -> siexec_inst i st = None.
Proof.
  destruct i; wlp_simplify; congruence.
Qed.

Lemma seval_condition_refines hst st ge sp cond hargs args rs m:
  hsok_local ge sp rs m hst -> 
  hsilocal_refines ge sp rs m hst st ->
  list_sval_refines ge sp rs m hargs args ->
  hseval_condition ge sp cond hargs (hsi_smem hst) rs m
  = seval_condition ge sp cond args (si_smem st) rs m.
 Proof.
  intros HOK (_ & MEMEQ & _) LR. unfold hseval_condition, seval_condition.
  rewrite LR, <- MEMEQ; auto.
Qed.

Lemma sok_local_set_sreg_simp (rsv:root_sval) ge sp rs0 m0 st r lr:
  sok_local ge sp rs0 m0 (slocal_set_sreg st r (rsv lr st))
  -> sok_local ge sp rs0 m0 st.
Proof.
  rewrite sok_local_set_sreg; intuition.
Qed.

Local Hint Resolve hsist_set_local_correct_stat: core.

Lemma hsiexec_inst_correct i hst:
  WHEN hsiexec_inst i hst ~> o THEN forall hst' st,
   o = Some hst' ->
   exists st', siexec_inst i st = Some st'
    /\ (forall (REF:hsistate_refines_stat hst st), hsistate_refines_stat hst' st')
    /\ (forall ge sp rs0 m0 (REF:hsistate_refines_dyn ge sp rs0 m0 hst st), hsistate_refines_dyn ge sp rs0 m0 hst' st').
Proof.
  destruct i; simpl; wlp_simplify; try_simplify_someHyps; eexists; intuition eauto.
  - (* refines_dyn Iop *)
    eapply hsist_set_local_correct_dyn; eauto.
    generalize (sok_local_set_sreg_simp (Rop o)); simpl; eauto.
  - (* refines_dyn Iload *)
    eapply hsist_set_local_correct_dyn; eauto.
    generalize (sok_local_set_sreg_simp (Rload t0 m a)); simpl; eauto.
  - (* refines_dyn Istore *)
    eapply hsist_set_local_correct_dyn; eauto.
    unfold sok_local; simpl; intuition.
  - (* refines_stat Icond *)
    unfold hsistate_refines_stat, hsiexits_refines_stat in *; simpl; intuition.
    constructor; simpl; eauto.
    constructor.
  - (* refines_dyn Icond *)
    destruct REF as (EXREF & LREF & NEST).
    split.
    + constructor; simpl; auto.
      constructor; simpl; auto.
      intros; erewrite seval_condition_refines; eauto.
    + split; simpl; auto.
      destruct NEST as [|st0 se lse TOP NEST];
      econstructor; simpl; auto; constructor; auto.
Qed.
Global Opaque hsiexec_inst.
Local Hint Resolve hsiexec_inst_correct: wlp.


Definition some_or_fail {A} (o: option A) (msg: pstring): ?? A :=
  match o with
  | Some x => RET x
  | None => FAILWITH msg
  end.

Fixpoint hsiexec_path (path:nat) (f: function) (hst: hsistate): ?? hsistate :=
  match path with
  | O => RET hst
  | S p =>
    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
  end.

Lemma hsiexec_path_correct path f: forall hst,
  WHEN hsiexec_path path f hst ~> hst' THEN forall st
  (RSTAT:hsistate_refines_stat hst st),
  exists st', siexec_path path f st = Some st'
    /\ hsistate_refines_stat hst' st'
    /\ (forall ge sp rs0 m0 (REF:hsistate_refines_dyn ge sp rs0 m0 hst st), hsistate_refines_dyn ge sp rs0 m0 hst' st').
Proof.
  induction path; wlp_simplify; try_simplify_someHyps. clear IHpath.
  generalize RSTAT; intros (PCEQ & _) INSTEQ.
  rewrite <- PCEQ, INSTEQ; simpl.
  exploit H0; eauto. clear H0.
  intros (st0 & SINST & ISTAT & IDYN); erewrite SINST.
  exploit H1; eauto. clear H1.
  intros (st' & SPATH & PSTAT & PDYN).
  eexists; intuition eauto.
Qed.
Global Opaque hsiexec_path.
Local Hint Resolve hsiexec_path_correct: wlp.

Fixpoint hbuiltin_arg (hst: PTree.t hsval) (arg : builtin_arg reg): ?? builtin_arg hsval := 
  match arg with
  | BA r => 
         DO v <~ hsi_sreg_get hst r;;
         RET (BA v)
  | BA_int n => RET (BA_int n)
  | BA_long n => RET (BA_long n)
  | BA_float f0 => RET (BA_float f0)
  | BA_single s => RET (BA_single s)
  | BA_loadstack chunk ptr => RET (BA_loadstack chunk ptr)
  | BA_addrstack ptr => RET (BA_addrstack ptr)
  | BA_loadglobal chunk id ptr => RET (BA_loadglobal chunk id ptr)
  | BA_addrglobal id ptr => RET (BA_addrglobal id ptr)
  | BA_splitlong ba1 ba2 => 
    DO v1 <~ hbuiltin_arg hst ba1;;
    DO v2 <~ hbuiltin_arg hst ba2;;
    RET (BA_splitlong v1 v2)
  | BA_addptr ba1 ba2 => 
    DO v1 <~ hbuiltin_arg hst ba1;;
    DO v2 <~ hbuiltin_arg hst ba2;;
    RET (BA_addptr v1 v2)
  end.

Lemma hbuiltin_arg_correct hst arg:
  WHEN hbuiltin_arg hst arg ~> hargs THEN forall ge sp rs0 m0 (f: reg -> sval)
    (RR: forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (f r) rs0 m0),
    seval_builtin_sval ge sp (builtin_arg_map hsval_proj hargs) rs0 m0 = seval_builtin_sval ge sp (builtin_arg_map f arg) rs0 m0.
Proof.
  induction arg; wlp_simplify.
  + erewrite H; eauto.
  + erewrite H; eauto.
    erewrite H0; eauto.
  + erewrite H; eauto.
    erewrite H0; eauto.
Qed.
Global Opaque hbuiltin_arg.
Local Hint Resolve hbuiltin_arg_correct: wlp.

Fixpoint hbuiltin_args (hst: PTree.t hsval) (args: list (builtin_arg reg)): ?? list (builtin_arg hsval) :=
  match args with
  | nil => RET nil
  | a::l =>
    DO ha <~ hbuiltin_arg hst a;;
    DO hl <~ hbuiltin_args hst l;;
    RET (ha::hl)
    end.

Lemma hbuiltin_args_correct hst args:
  WHEN hbuiltin_args hst args ~> hargs THEN forall ge sp rs0 m0 (f: reg -> sval)
    (RR: forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (f r) rs0 m0),
    bargs_refines ge sp rs0 m0 hargs (List.map (builtin_arg_map f) args).
Proof.
  unfold bargs_refines, seval_builtin_args; induction args; wlp_simplify.
  erewrite H; eauto.
  erewrite H0; eauto.
Qed.
Global Opaque hbuiltin_args.
Local Hint Resolve hbuiltin_args_correct: wlp.

Definition hsum_left (hst: PTree.t hsval) (ros: reg + ident): ?? (hsval + ident) :=
  match ros with
  | inl r => DO hr <~ hsi_sreg_get hst r;; RET (inl hr) 
  | inr s => RET (inr s)
  end.

Lemma hsum_left_correct hst ros:
  WHEN hsum_left hst ros ~> hsi THEN forall ge sp rs0 m0 (f: reg -> sval)
    (RR: forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (f r) rs0 m0),
    sum_refines ge sp rs0 m0 hsi (sum_left_map f ros).
Proof.
  unfold sum_refines; destruct ros; wlp_simplify.
Qed.
Global Opaque hsum_left.
Local Hint Resolve hsum_left_correct: wlp.

Definition hsexec_final (i: instruction) (hst: PTree.t hsval): ?? hsfval :=
  match i with
  | Icall sig ros args res pc =>
    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 hsexec_final_correct (hsl: hsistate_local) i:
  WHEN hsexec_final i hsl ~> hsf THEN forall ge sp rs0 m0 sl
   (OK:  hsok_local ge sp rs0 m0 hsl)
   (REF: hsilocal_refines ge sp rs0 m0 hsl sl),
   hfinal_refines ge sp rs0 m0 hsf (sexec_final i sl).
Proof.
  destruct i; wlp_simplify; try econstructor; simpl; eauto.
Qed.
Global Opaque hsexec_final.
Local Hint Resolve hsexec_final_correct: wlp.

Definition init_hsistate_local (_:unit): ?? hsistate_local
  := DO hm <~ hSinit ();;
     RET {| hsi_smem := hm; hsi_ok_lsval := nil; hsi_sreg := PTree.empty hsval |}.

Lemma init_hsistate_local_correct:
  WHEN init_hsistate_local () ~> hsl THEN forall ge sp rs0 m0,
  hsilocal_refines ge sp rs0 m0 hsl init_sistate_local.
Proof.
  unfold hsilocal_refines; wlp_simplify.
  - unfold hsok_local; simpl; intuition. erewrite H in *; congruence.
  - unfold hsok_local, sok_local; simpl in *; intuition; try congruence.
  - unfold hsi_sreg_eval, hsi_sreg_proj. rewrite PTree.gempty. reflexivity.
  - try_simplify_someHyps.
Qed.
Global Opaque init_hsistate_local.
Local Hint Resolve init_hsistate_local_correct: wlp.

Definition init_hsistate pc: ?? hsistate
  := DO hst <~ init_hsistate_local ();;
     RET {| hsi_pc := pc; hsi_exits := nil; hsi_local := hst |}.

Lemma init_hsistate_correct pc:
  WHEN init_hsistate pc ~> hst THEN
      hsistate_refines_stat hst (init_sistate pc)
   /\ forall ge sp rs0 m0, hsistate_refines_dyn ge sp rs0 m0 hst (init_sistate pc).
Proof.
  unfold hsistate_refines_stat, hsistate_refines_dyn, hsiexits_refines_dyn; wlp_simplify; constructor.
Qed.
Global Opaque init_hsistate.
Local Hint Resolve init_hsistate_correct: wlp.

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.

Lemma hsexec_correct_aux f pc:
  WHEN hsexec f pc ~> hst THEN
  exists st, sexec f pc = Some st /\ hsstate_refines hst st.
Proof.
  unfold hsstate_refines, sexec; wlp_simplify.
  - (* Some *)
   rewrite H; clear H.
   exploit H0; clear H0; eauto.
   intros (st0 & EXECPATH & SREF & DREF).
   rewrite EXECPATH; clear EXECPATH.
   generalize SREF. intros (EQPC & _).
   rewrite <- EQPC, H3; clear H3.
   exploit H4; clear H4; eauto.
   intros (st' & EXECL & SREF' & DREF').
   try_simplify_someHyps.
   eexists; intuition (simpl; eauto).
   constructor.
  - (* None *)
   rewrite H; clear H H4.
   exploit H0; clear H0; eauto.
   intros (st0 & EXECPATH & SREF & DREF).
   rewrite EXECPATH; clear EXECPATH.
   generalize SREF. intros (EQPC & _).
   rewrite <- EQPC, H3; clear H3.
   erewrite hsiexec_inst_None_correct; eauto.
   eexists; intuition (simpl; eauto).
Qed.

Global Opaque hsexec.

End CanonBuilding.

(** Correction of concrete symbolic execution wrt abstract symbolic execution *)
Theorem hsexec_correct
  (hC_hsval : hashinfo hsval -> ?? hsval)
  (hC_list_hsval : hashinfo list_hsval -> ?? list_hsval)
  (hC_hsmem : hashinfo hsmem -> ?? hsmem)
  (f : function) 
  (pc : node):
       WHEN hsexec hC_hsval hC_list_hsval hC_hsmem f pc ~> hst THEN forall
        (hC_hsval_correct: forall hs,
            WHEN hC_hsval hs ~> hs' THEN forall ge sp rs0 m0,
                seval_sval ge sp (hsval_proj (hdata hs)) rs0 m0 =
                seval_sval ge sp (hsval_proj hs') rs0 m0)
        (hC_list_hsval_correct: forall lh,
            WHEN hC_list_hsval lh ~> lh' THEN forall ge sp rs0 m0,
              seval_list_sval ge sp (hsval_list_proj (hdata lh)) rs0 m0 =
              seval_list_sval ge sp (hsval_list_proj lh') rs0 m0)
         (hC_hsmem_correct: forall hm,
            WHEN hC_hsmem hm ~> hm' THEN forall ge sp rs0 m0,
              seval_smem ge sp (hsmem_proj (hdata hm)) rs0 m0 =
              seval_smem ge sp (hsmem_proj hm') rs0 m0),
         exists st : sstate, sexec f pc = Some st /\ hsstate_refines hst st.
Proof.
  wlp_simplify.
  eapply hsexec_correct_aux; eauto.
Qed.

Local Hint Resolve hsexec_correct: wlp.

(** * Intermediate specifications of the simulation test *)

(** ** Specification of the simulation test on [hsistate_local].
       It is motivated by [hsilocal_simu_core_correct theorem] below
*)
Definition hsilocal_simu_core (oalive: option Regset.t) (hst1 hst2: hsistate_local) :=
     List.incl (hsi_ok_lsval hst2) (hsi_ok_lsval hst1)
  /\ (forall r, (match oalive with Some alive => Regset.In r alive | _ => True end) -> PTree.get r hst2 = PTree.get r hst1)
  /\ hsi_smem hst1 = hsi_smem hst2.

Definition seval_sval_partial ge sp rs0 m0 hsv :=
  match seval_hsval ge sp hsv rs0 m0 with
  | Some v => v
  | None => Vundef
  end.

Definition select_first (ox oy: option val) :=
  match ox with
  | Some v => Some v
  | None => oy
  end.

(** If the register was computed by hrs, evaluate the symbolic value from hrs.
    Else, take the value directly from rs0 *)
Definition seval_partial_regset ge sp rs0 m0 hrs :=
  let hrs_eval := PTree.map1 (seval_sval_partial ge sp rs0 m0) hrs in
  (fst rs0, PTree.combine select_first hrs_eval (snd rs0)).

Lemma seval_partial_regset_get ge sp rs0 m0 hrs r:
  (seval_partial_regset ge sp rs0 m0 hrs) # r =
  match (hrs ! r) with Some sv => seval_sval_partial ge sp rs0 m0 sv | None => (rs0 # r) end.
Proof.
  unfold seval_partial_regset. unfold Regmap.get. simpl.
  rewrite PTree.gcombine; [| simpl; reflexivity]. rewrite PTree.gmap1.
  destruct (hrs ! r); simpl; [reflexivity|].
  destruct ((snd rs0) ! r); reflexivity.
Qed.

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

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

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

Theorem hsilocal_simu_core_correct hst1 hst2 of ge1 ge2 sp rs0 m0 rs m st1 st2:
  hsilocal_simu_core of hst1 hst2 ->
  hsilocal_refines ge1 sp rs0 m0 hst1 st1 ->
  hsilocal_refines ge2 sp rs0 m0 hst2 st2 ->
  (forall s, Genv.find_symbol ge1 s = Genv.find_symbol ge2 s) ->
  ssem_local ge1 sp st1 rs0 m0 rs m ->
  match of with
  | None => ssem_local ge2 sp st2 rs0 m0 rs m
  | Some alive => 
      let rs' := seval_partial_regset ge2 sp rs0 m0 (hsi_sreg hst2)
      in ssem_local ge2 sp st2 rs0 m0 rs' m /\ eqlive_reg (fun r => Regset.In r alive) rs rs'
  end.
Proof.
  intros CORE HREF1 HREF2 GFS SEML.
  refine (modusponens _ _ (ssem_local_refines_hok _ _ _ _ _ _ _ _ _ _) _); eauto.
  intro HOK1.
  refine (modusponens _ _ (hsilocal_simu_core_nofail _ _ _ _ _ _ _ _ _ _ _) _); eauto.
  intro HOK2.
  destruct SEML as (PRE & MEMEQ & RSEQ).
  assert (SIPRE: si_pre st2 ge2 sp rs0 m0). { destruct HREF2 as (OKEQ & _ & _). rewrite <- OKEQ in HOK2. apply HOK2. }
  assert (SMEMEVAL: seval_smem ge2 sp (si_smem st2) rs0 m0 = Some m). {
    destruct HREF2 as (_ & MEMEQ2 & _). destruct HREF1 as (_ & MEMEQ1 & _).
    destruct CORE as (_ & _ & MEMEQ3).
    rewrite <- MEMEQ2; auto. rewrite <- MEMEQ3.
    erewrite smem_eval_preserved; [| eapply GFS].
    rewrite MEMEQ1; auto. }
  destruct of as [alive |].
  - constructor.
    + constructor; [assumption | constructor; [assumption|]].
      destruct HREF2 as (B & _ & A & _).
      (** B is used for the auto below. *)
      assert (forall r : positive, hsi_sreg_eval ge2 sp hst2 r rs0 m0 = seval_sval ge2 sp (si_sreg st2 r) rs0 m0) by auto.
      intro r. rewrite <- H. clear H. 
      generalize (A HOK2 r). unfold hsi_sreg_eval.
      rewrite seval_partial_regset_get.
      unfold hsi_sreg_proj.
      destruct (hst2 ! r) eqn:HST2; [| simpl; reflexivity].
      unfold seval_sval_partial. generalize HOK2; rewrite <- B; intros (_ & _ & C) D.
      assert (seval_sval ge2 sp (hsval_proj h) rs0 m0 <> None) by congruence.
      destruct (seval_sval ge2 sp _ rs0 m0); [reflexivity | contradiction].
    + intros r ALIVE. destruct HREF2 as (_ & _ & A & _). destruct HREF1 as (_ & _ & B & _).
      destruct CORE as (_ & C & _). rewrite seval_partial_regset_get.
      assert (OPT: forall (x y: val), Some x = Some y -> x = y) by congruence.
      destruct (hst2 ! r) eqn:HST2; apply OPT; clear OPT.
      ++ unfold seval_sval_partial.
         assert (seval_sval ge2 sp (hsval_proj h) rs0 m0 = hsi_sreg_eval ge2 sp hst2 r rs0 m0). {
           unfold hsi_sreg_eval, hsi_sreg_proj. rewrite HST2. reflexivity. }
         rewrite H. clear H. unfold hsi_sreg_eval, hsi_sreg_proj. rewrite C; [|assumption].
         erewrite seval_preserved; [| eapply GFS].
         unfold hsi_sreg_eval, hsi_sreg_proj in B; rewrite B; [|assumption]. rewrite RSEQ. reflexivity.
      ++ rewrite <- RSEQ. rewrite <- B; [|assumption]. unfold hsi_sreg_eval, hsi_sreg_proj.
         rewrite <- C; [|assumption]. rewrite HST2. reflexivity.
  - constructor; [|constructor].
    + destruct HREF2 as (OKEQ & _ & _). rewrite <- OKEQ in HOK2. apply HOK2.
    + destruct HREF2 as (_ & MEMEQ2 & _). destruct HREF1 as (_ & MEMEQ1 & _).
      destruct CORE as (_ & _ & MEMEQ3).
      rewrite <- MEMEQ2; auto. rewrite <- MEMEQ3.
      erewrite smem_eval_preserved; [| eapply GFS].
      rewrite MEMEQ1; auto.
    + intro r. destruct HREF2 as (_ & _ & A & _). destruct HREF1 as (_ & _ & B & _).
      destruct CORE as (_ & C & _). rewrite <- A; auto. unfold hsi_sreg_eval, hsi_sreg_proj.
      rewrite C; [|auto]. erewrite seval_preserved; [| eapply GFS].
      unfold hsi_sreg_eval, hsi_sreg_proj in B; rewrite B; auto.
Qed.

(** ** Specification of the simulation test on [hsistate_exit].
       It is motivated by [hsiexit_simu_core_correct theorem] below
*)
Definition hsiexit_simu_core dm f (hse1 hse2: hsistate_exit) :=
  (exists path, (fn_path f) ! (hsi_ifso hse1) = Some path
    /\ hsilocal_simu_core (Some path.(input_regs)) (hsi_elocal hse1) (hsi_elocal hse2))
  /\ dm ! (hsi_ifso hse2) = Some (hsi_ifso hse1)
  /\ hsi_cond hse1 = hsi_cond hse2
  /\ hsi_scondargs hse1 = hsi_scondargs hse2.

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

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

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

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

(** ** Specification of the simulation test on [list hsistate_exit].
       It is motivated by [hsiexit_simu_core_correct theorem] below
*)

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

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

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


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


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


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


(** ** Specification of the simulation test on [hsistate].
       It is motivated by [hsistate_simu_core_correct theorem] below
*)

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

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

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

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

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

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


(** ** Specification of the simulation test on [sfval].
       It is motivated by [hfinal_simu_core_correct theorem] below
*)


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

Definition hfinal_simu_core (dm: PTree.t node) (f: RTLpath.function) (pc1 pc2: node) (hf1 hf2: hsfval): Prop :=
  final_simu_core dm f pc1 pc2 (hfinal_proj hf1) (hfinal_proj hf2).

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

Lemma list_proj_refines_eq ge ge' sp rs0 m0 lsv lhsv:
  (forall s, Genv.find_symbol ge s = Genv.find_symbol ge' s) ->
  list_sval_refines ge sp rs0 m0 lhsv lsv ->
  forall lhsv' lsv',
  list_sval_refines ge' sp rs0 m0 lhsv' lsv' ->
  hsval_list_proj lhsv = hsval_list_proj lhsv' ->
  seval_list_sval ge sp lsv rs0 m0 = seval_list_sval ge' sp lsv' rs0 m0.
Proof.
  intros GFS H lhsv' lsv' H' H0.
  erewrite <- H, H0.
  erewrite list_sval_eval_preserved; eauto.
Qed.

Lemma seval_list_builtin_sval_preserved ge ge' sp lsv rs0 m0:
   (forall s : ident, Genv.find_symbol ge' s = Genv.find_symbol ge s) ->
   seval_list_builtin_sval ge sp lsv rs0 m0 =  seval_list_builtin_sval ge' sp lsv rs0 m0.
Admitted. (* TODO *)

Lemma barg_proj_refines_eq ge ge' sp rs0 m0:
  (forall s, Genv.find_symbol ge s = Genv.find_symbol ge' s) ->
  forall lhsv lsv, bargs_refines ge sp rs0 m0 lhsv lsv ->
  forall lhsv' lsv', bargs_refines ge' sp rs0 m0 lhsv' lsv' ->
  List.map (builtin_arg_map hsval_proj) lhsv = List.map (builtin_arg_map hsval_proj) lhsv' ->
  seval_list_builtin_sval ge sp lsv rs0 m0 = seval_list_builtin_sval ge' sp lsv' rs0 m0.
Proof.
  unfold bargs_refines; intros GFS lhsv lsv H lhsv' lsv' H' H0.
  erewrite <- H, H0.
  erewrite seval_list_builtin_sval_preserved; 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, PROJ.
  erewrite <- seval_preserved; eauto.
Qed.

Theorem hfinal_simu_core_correct dm f ctx opc1 opc2 hf1 hf2 f1 f2:
  hfinal_simu_core dm f opc1 opc2 hf1 hf2 ->
  hfinal_refines (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hf1 f1 ->
  hfinal_refines (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hf2 f2 ->
  sfval_simu dm f opc1 opc2 ctx f1 f2.
Proof.
  assert (GFS: forall s : ident, Genv.find_symbol (the_ge1 ctx) s = Genv.find_symbol (the_ge2 ctx) s) by apply ctx.
  intros CORE FREF1 FREF2.
  destruct hf1; inv FREF1.
  (* Snone *)
  - destruct hf2; try contradiction. inv FREF2.
    inv CORE. constructor. assumption.
  (* Scall *)
  - rename H5 into SREF1. rename H6 into LREF1.
    destruct hf2; try contradiction. inv FREF2.
    rename H5 into SREF2. rename H6 into LREF2.
    destruct CORE as (PCEQ & ? & ? & ? & ?). subst.
    rename H0 into SVOSEQ. rename H1 into LSVEQ.
    constructor; [assumption | |].
    + destruct svos.
      * destruct svos0; try discriminate. destruct ros; try contradiction.
        destruct ros0; try contradiction. constructor.
        simpl in SVOSEQ. inv SVOSEQ.
        simpl in SREF1. simpl in SREF2.
        rewrite <- SREF1. rewrite <- SREF2.
        erewrite <- seval_preserved; [| eapply GFS]. congruence.
      * destruct svos0; try discriminate. destruct ros; try contradiction.
        destruct ros0; try contradiction. constructor.
        simpl in SVOSEQ. inv SVOSEQ. congruence.
    + erewrite list_proj_refines_eq; eauto. constructor.
  (* Stailcall *)
  - rename H3 into SREF1. rename H4 into LREF1.
    destruct hf2; try (inv CORE; fail). inv FREF2.
    rename H4 into LREF2. rename H3 into SREF2.
    inv CORE. rename H1 into SVOSEQ. rename H2 into LSVEQ.
    constructor.
    + destruct svos. (** Copy-paste from Scall *)
      * destruct svos0; try discriminate. destruct ros; try contradiction.
        destruct ros0; try contradiction. constructor.
        simpl in SVOSEQ. inv SVOSEQ.
        simpl in SREF1. simpl in SREF2.
        rewrite <- SREF1. rewrite <- SREF2.
        erewrite <- seval_preserved; [| eapply GFS]. congruence.
      * destruct svos0; try discriminate. destruct ros; try contradiction.
        destruct ros0; try contradiction. constructor.
        simpl in SVOSEQ. inv SVOSEQ. congruence.
    + erewrite list_proj_refines_eq; eauto. constructor.
  (* Sbuiltin *)
  - rename H4 into BREF1. destruct hf2; try (inv CORE; fail). inv FREF2.
    rename H4 into BREF2. inv CORE. destruct H0 as (? & ? & ?). subst.
    rename H into PCEQ. rename H1 into ARGSEQ. constructor; [assumption|].
    erewrite barg_proj_refines_eq; eauto. constructor.
  (* Sjumptable *)
  - rename H2 into SREF1. destruct hf2; try contradiction. inv FREF2.
    rename H2 into SREF2. destruct CORE as (A & B). constructor; [assumption|].
    erewrite sval_refines_proj; eauto. constructor.
  (* Sreturn *)
  - rename H0 into SREF1.
    destruct hf2; try discriminate. inv CORE.
    inv FREF2. destruct osv; destruct res; inv SREF1.
    + destruct res0; try discriminate. destruct osv0; inv H1.
      constructor. simpl in H0. inv H0. erewrite sval_refines_proj; eauto.
      constructor.
    + destruct res0; try discriminate. destruct osv0; inv H1. constructor.
Qed.


(** ** Specification of the simulation test on [hsstate].
       It is motivated by [hsstate_simu_core_correct theorem] below
*)

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) st1 st2 (SREF1 & DREF1 & FREF1) (SREF2 & DREF2 & FREF2).
  generalize SCORE. intro SIMU; eapply hsistate_simu_core_correct in SIMU; eauto.
  constructor; auto.
  intros is1 SEM1 CONT1.
  unfold hsistate_simu in SIMU. exploit SIMU; clear SIMU; eauto.
  unfold istate_simu, ssem_internal in *; intros (is2 & SEM2 & SIMU).
  rewrite! CONT1 in *. destruct SIMU as (CONT2 & _).
  rewrite! CONT1, <- CONT2 in *.
  destruct SEM1 as (SEM1 & _ & _).
  destruct SEM2 as (SEM2 & _ & _).
  eapply hfinal_simu_core_correct in FSIMU; eauto.
  - destruct SREF1 as (PC1 & _). destruct SREF2 as (PC2 & _). rewrite <- PC1. rewrite <- PC2.
    eapply FSIMU.
  - eapply FREF1. exploit DREF1. intros (_ & (OK & _) & _). rewrite <- OK. eapply ssem_local_sok; eauto.
  - eapply FREF2. exploit DREF2. intros (_ & (OK & _) & _). rewrite <- OK. eapply ssem_local_sok; eauto.
Qed.

(** * Implementing the simulation test with concrete hash-consed symbolic execution *)

Definition phys_check {A} (x y:A) (msg: pstring): ?? unit :=
  DO b <~ phys_eq x y;;
  assert_b b msg;;
  RET tt.

Definition struct_check {A} (x y: A) (msg: pstring): ?? unit :=
  DO b <~ struct_eq x y;;
  assert_b b msg;;
  RET tt.

Lemma struct_check_correct {A} (a b: A) msg:
  WHEN struct_check a b msg ~> _ THEN
  a = b.
Proof. wlp_simplify. Qed.
Global Opaque struct_check.
Hint Resolve struct_check_correct: wlp.

Definition option_eq_check {A} (o1 o2: option A): ?? unit :=
  match o1, o2 with
  | Some x1, Some x2 => phys_check x1 x2 "option_eq_check: data physically differ"
  | None, None => RET tt
  | _, _ => FAILWITH "option_eq_check: structure differs"
  end.

Lemma option_eq_check_correct A (o1 o2: option A): WHEN option_eq_check o1 o2 ~> _ THEN o1=o2.
Proof.
  wlp_simplify.
Qed.
Global Opaque option_eq_check.
Hint Resolve option_eq_check_correct:wlp.

Import PTree.

Fixpoint PTree_eq_check {A} (d1 d2: PTree.t A): ?? unit :=
  match d1, d2 with
  | Leaf, Leaf => RET tt
  | Node l1 o1 r1, Node l2 o2 r2 =>
      option_eq_check o1 o2;;
      PTree_eq_check l1 l2;;
      PTree_eq_check r1 r2
  | _, _ => FAILWITH "PTree_eq_check: some key is absent"
  end.

Lemma PTree_eq_check_correct A d1: forall (d2: t A),
 WHEN PTree_eq_check d1 d2 ~> _ THEN forall x, PTree.get x d1 = PTree.get x d2.
Proof.
  induction d1 as [|l1 Hl1 o1 r1 Hr1]; destruct d2 as [|l2 o2 r2]; simpl; 
  wlp_simplify. destruct x; simpl; auto.
Qed.
Global Opaque PTree_eq_check.
Local Hint Resolve PTree_eq_check_correct: wlp.

Fixpoint PTree_frame_eq_check {A} (frame: list positive) (d1 d2: PTree.t A): ?? unit :=
  match frame with
  | nil => RET tt
  | k::l => 
    option_eq_check (PTree.get k d1) (PTree.get k d2);;
    PTree_frame_eq_check l d1 d2
  end.

Lemma PTree_frame_eq_check_correct A l (d1 d2: t A):
 WHEN PTree_frame_eq_check l d1 d2 ~> _ THEN forall x, List.In x l -> PTree.get x d1 = PTree.get x d2.
Proof.
  induction l as [|k l]; simpl; wlp_simplify.
  subst; auto.
Qed.
Global Opaque PTree_frame_eq_check.
Local Hint Resolve PTree_frame_eq_check_correct: wlp.

Definition hsilocal_simu_check hst1 hst2 : ?? unit :=
  DEBUG("? last check");;
  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);;
  DEBUG("=> last check: OK").

Lemma hsilocal_simu_check_correct hst1 hst2:
  WHEN hsilocal_simu_check hst1 hst2 ~> _ THEN
  hsilocal_simu_core None hst1 hst2.
Proof.
  unfold hsilocal_simu_core; wlp_simplify. 
Qed.
Hint Resolve hsilocal_simu_check_correct: wlp.
Global Opaque hsilocal_simu_check.

Definition hsilocal_frame_simu_check frame hst1 hst2 : ?? unit :=
  DEBUG("? frame check");;
  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").

Lemma setoid_in {A: Type} (a: A): forall l,
  SetoidList.InA (fun x y => x = y) a l ->
  In a l.
Proof.
  induction l; intros; inv H.
  - constructor. reflexivity.
  - right. auto.
Qed.

Lemma regset_elements_in r rs:
  Regset.In r rs ->
  In r (Regset.elements rs).
Proof.
  intros. exploit Regset.elements_1; eauto. intro SIN.
  apply setoid_in. assumption.
Qed.
Local Hint Resolve regset_elements_in: core.

Lemma hsilocal_frame_simu_check_correct hst1 hst2 alive:
  WHEN hsilocal_frame_simu_check (Regset.elements alive) hst1 hst2 ~> _ THEN
  hsilocal_simu_core (Some alive) hst1 hst2.
Proof.
  unfold hsilocal_simu_core; wlp_simplify. symmetry; eauto.
Qed.
Hint Resolve hsilocal_frame_simu_check_correct: wlp.
Global Opaque hsilocal_frame_simu_check.

Definition revmap_check_single (dm: PTree.t node) (n tn: node) : ?? unit :=
  DO res <~ some_or_fail (dm ! tn) "revmap_check_single: no mapping for tn";;
  struct_check n res "revmap_check_single: n and res are physically different".

Lemma revmap_check_single_correct dm pc1 pc2:
  WHEN revmap_check_single dm pc1 pc2 ~> _ THEN
  dm ! pc2 = Some pc1.
Proof.
  wlp_simplify. congruence.
Qed.
Hint Resolve revmap_check_single_correct: wlp.
Global Opaque revmap_check_single.

Definition hsiexit_simu_check (dm: PTree.t node) (f: RTLpath.function) (hse1 hse2: hsistate_exit): ?? unit :=
  struct_check (hsi_cond hse1) (hsi_cond hse2) "hsiexit_simu_check: conditions do not match";;
  phys_check (hsi_scondargs hse1) (hsi_scondargs hse2) "hsiexit_simu_check: args do not match";;
  revmap_check_single dm (hsi_ifso hse1) (hsi_ifso hse2);;
  DO path <~ some_or_fail ((fn_path f) ! (hsi_ifso hse1)) "hsiexit_simu_check: internal error";;
  hsilocal_frame_simu_check (Regset.elements path.(input_regs)) (hsi_elocal hse1) (hsi_elocal hse2).

Lemma hsiexit_simu_check_correct dm f hse1 hse2:
  WHEN hsiexit_simu_check dm f hse1 hse2 ~> _ THEN
  hsiexit_simu_core dm f hse1 hse2.
Proof.
  unfold hsiexit_simu_core; wlp_simplify.
Qed.
Hint Resolve hsiexit_simu_check_correct: wlp.
Global Opaque hsiexit_simu_check.

Fixpoint hsiexits_simu_check (dm: PTree.t node) (f: RTLpath.function) (lhse1 lhse2: list hsistate_exit) :=
  match lhse1,lhse2 with
  | nil, nil => RET tt
  | hse1 :: lhse1, hse2 :: lhse2 =>
    hsiexit_simu_check dm f hse1 hse2;;
    hsiexits_simu_check dm f lhse1 lhse2
  | _, _ => FAILWITH "siexists_simu_check:  lengths do not match"
  end.

Lemma hsiexits_simu_check_correct dm f: forall le1 le2,
  WHEN hsiexits_simu_check dm f le1 le2 ~> _ THEN
  hsiexits_simu_core dm f le1 le2.
Proof.
  unfold hsiexits_simu_core; induction le1; simpl; destruct le2; wlp_simplify; constructor; eauto.
Qed.
Hint Resolve hsiexits_simu_check_correct: wlp.
Global Opaque hsiexits_simu_check.

Definition hsistate_simu_check (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsistate) :=
  hsiexits_simu_check dm f (hsi_exits hst1) (hsi_exits hst2);;
  hsilocal_simu_check (hsi_local hst1) (hsi_local hst2).

Lemma hsistate_simu_check_correct dm f hst1 hst2:
  WHEN hsistate_simu_check dm f hst1 hst2 ~> _ THEN
  hsistate_simu_core dm f hst1 hst2.
Proof.
  unfold hsistate_simu_core; wlp_simplify.
Qed.
Hint Resolve hsistate_simu_check_correct: wlp.
Global Opaque hsistate_simu_check.


Fixpoint revmap_check_list (dm: PTree.t node) (ln ln': list node): ?? unit :=
  match ln, ln' with
  | nil, nil => RET tt
  | n::ln, n'::ln' => 
      revmap_check_single dm n n';;
      revmap_check_list dm ln ln'
  | _, _ => 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' ~> _ THEN
  ptree_get_list dm lpc' = Some lpc.
Proof.
  induction lpc.
  - destruct lpc'; wlp_simplify.
  - destruct lpc'; wlp_simplify. try_simplify_someHyps.
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"
  | inr id1, inr id2 => phys_check id1 id2 "svos_simu_check: symbol mismatch"
  | _, _ => FAILWITH "svos_simu_check: type mismatch"
  end.

Lemma svos_simu_check_correct svos1 svos2:
  WHEN svos_simu_check svos1 svos2 ~> _ THEN
  svos1 = svos2.
Proof.
  destruct svos1; destruct svos2; wlp_simplify.
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"
  end.

Lemma builtin_arg_simu_check_correct: forall bs1 bs2,
  WHEN builtin_arg_simu_check bs1 bs2 ~> _ THEN
  builtin_arg_map hsval_proj bs1 = builtin_arg_map hsval_proj bs2.
Proof.
  induction bs1.
  all: try (wlp_simplify; subst; reflexivity).
  all: destruct bs2; wlp_simplify; congruence.
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
  | bs1::lbs1, bs2::lbs2 =>
    builtin_arg_simu_check bs1 bs2;;
    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 ~> _ THEN
  List.map (builtin_arg_map hsval_proj) lbs1 = List.map (builtin_arg_map hsval_proj) lbs2.
Proof.
  induction lbs1; destruct lbs2; wlp_simplify. 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) (pc1 pc2: node) (fv1 fv2: hsfval) :=
  match fv1, fv2 with
  | 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";;
      phys_check res1 res2 "sfval_simu_check: Scall res do not match";;
      svos_simu_check svos1 svos2;;
      phys_check lsv1 lsv2 "sfval_simu_check: Scall args do not match"
  | HStailcall sig1 svos1 lsv1, HStailcall sig2 svos2 lsv2 =>
      phys_check sig1 sig2 "sfval_simu_check: Stailcall different signatures";;
      svos_simu_check svos1 svos2;;
      phys_check lsv1 lsv2 "sfval_simu_check: Stailcall args do not match"
  | HSbuiltin ef1 lbs1 br1 pc1, HSbuiltin ef2 lbs2 br2 pc2 =>
      revmap_check_single dm pc1 pc2;;
      phys_check ef1 ef2 "sfval_simu_check: builtin ef do not match";;
      phys_check br1 br2 "sfval_simu_check: builtin br do not match";;
      list_builtin_arg_simu_check lbs1 lbs2
  | HSjumptable sv ln, HSjumptable sv' ln' =>
      revmap_check_list dm ln ln';;
      phys_check sv sv' "sfval_simu_check: Sjumptable sval do not match"
  | HSreturn osv1, HSreturn osv2 =>
      option_eq_check osv1 osv2
  | _, _ => FAILWITH "sfval_simu_check: structure mismatch"
  end.

Lemma sfval_simu_check_correct dm f opc1 opc2 fv1 fv2:
  WHEN sfval_simu_check dm f opc1 opc2 fv1 fv2 ~> _ THEN
  hfinal_simu_core dm f opc1 opc2 fv1 fv2.
Proof.
  unfold hfinal_simu_core; destruct fv1; destruct fv2; wlp_simplify; try congruence.
Qed.
Hint Resolve sfval_simu_check_correct: wlp.
Global Opaque sfval_simu_check.

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

Lemma hsstate_simu_check_correct dm f hst1 hst2:
  WHEN hsstate_simu_check dm f hst1 hst2 ~> _ THEN
  hsstate_simu_core dm f hst1 hst2.
Proof.
  unfold hsstate_simu_core; wlp_simplify.
Qed.
Hint Resolve hsstate_simu_check_correct: wlp.
Global Opaque hsstate_simu_check. 

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 *)
  DO hC_sval <~ hCons hSVAL;;
  DO hC_list_hsval <~ hCons hLSVAL;;
  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.

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 sexec_simu; wlp_simplify.
  exploit H2; clear H2. 1-3: wlp_simplify.
  intros (st2 & SEXEC2 & REF2). try_simplify_someHyps.
  exploit H3; clear H3. 1-3: wlp_simplify.
  intros (st3 & SEXEC3 & REF3). try_simplify_someHyps.
  eexists. split; eauto.
  intros ctx.
  eapply hsstate_simu_core_correct; eauto.
Qed.
Global Opaque simu_check_single.
Global Hint Resolve simu_check_single_correct: wlp.

Fixpoint simu_check_rec (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) lm : ?? unit :=
  match lm with
  | nil => RET tt
  | m :: lm => 
    simu_check_single dm f tf m;;
    simu_check_rec dm f tf lm
  end.

Lemma simu_check_rec_correct dm f tf lm:
  WHEN simu_check_rec dm f tf lm ~> _ THEN
  forall pc1 pc2, In (pc2, pc1) lm -> sexec_simu dm f tf pc1 pc2.
Proof.
  induction lm; wlp_simplify.
  match goal with
  | X: (_,_) = (_,_) |- _ => inversion X; subst
  end.
  subst; eauto.
Qed.
Global Opaque simu_check_rec.
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);;
   DEBUG("simu_check OK!").

Local Hint Resolve PTree.elements_correct: core.
Lemma imp_simu_check_correct dm f tf:
  WHEN imp_simu_check dm f tf ~> _ THEN
  forall pc1 pc2, dm ! pc2 = Some pc1 -> sexec_simu dm f tf pc1 pc2.
Proof.
  wlp_simplify.
Qed.
Global Opaque imp_simu_check.
Global Hint Resolve imp_simu_check_correct: wlp.

Program Definition aux_simu_check (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function): ?? bool :=
   DO r <~ 
     (TRY 
       imp_simu_check dm f tf;; 
       RET true
      CATCH_FAIL s, _ =>
       println ("simu_check_failure:" +; s);;
       RET false
      ENSURE (fun b => b=true -> forall pc1 pc2, dm ! pc2 = Some pc1 -> sexec_simu dm f tf pc1 pc2));;
   RET (`r).
Obligation 1.
  split; wlp_simplify. discriminate.
Qed.

Lemma aux_simu_check_correct dm f tf:
  WHEN aux_simu_check dm f tf ~> b THEN
  b=true -> forall pc1 pc2, dm ! pc2 = Some pc1 -> sexec_simu dm f tf pc1 pc2.
Proof.
  unfold aux_simu_check; wlp_simplify.
  destruct exta; simpl; auto.
Qed.

(* Coerce aux_simu_check into a pure function (this is a little unsafe like all oracles in CompCert). *)

Import UnsafeImpure.

Definition simu_check (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) : res unit := 
  match unsafe_coerce (aux_simu_check dm f tf) with
  | Some true => OK tt
  | _ => Error (msg "simu_check has failed")
  end.

Lemma simu_check_correct dm f tf:
  simu_check dm f tf = OK tt ->
  forall pc1 pc2, dm ! pc2 = Some pc1 ->
  sexec_simu dm f tf pc1 pc2.
Proof.
  unfold simu_check.
  destruct (unsafe_coerce (aux_simu_check dm f tf)) as [[|]|] eqn:Hres; simpl; try discriminate.
  intros; eapply aux_simu_check_correct; eauto.
  eapply unsafe_coerce_not_really_correct; eauto.
Qed.