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.

Ltac wlp_intro vname hname := apply wlp_unfold; intros vname hname.
Ltac wlp_bind vname hname := apply wlp_bind; intros vname hname.
Ltac wlp_ret vname := let H := fresh "H" vname in wlp_intro vname H; apply mayRet_ret in H; subst.

Tactic Notation "wlp_intro" ident(v) ident(h) := wlp_intro v h.
Tactic Notation "wlp_intro" ident(v) := let H := fresh "H" v in wlp_intro v H.
Tactic Notation "wlp_bind" ident(v) ident(h) := wlp_bind v h.
Tactic Notation "wlp_bind" ident(v) := let H := fresh "H" v in wlp_bind v H.

Ltac wlp_absurd := match goal with
  | [ H : FAILWITH ?msg |- _ ] => eapply (_FAILWITH_correct _ _ (fun _ => False)) in H; inv H
  | [ H : DO r <~ fail ?msg;; RET ?expr ~~> ?exta |- _ ] => eapply (_FAILWITH_correct _ _ (fun _ => False)) in H; inv H
end.

Ltac wlp_hbind var := match goal with
  | [ H : DO _ <~ ?expr;; _ ~~> _ |- _ ] => 
      let Hvar := fresh "H" var in (apply mayRet_bind in H; destruct H as (var & Hvar & H))
  end.

Ltac wlp_hret := match goal with
  | [ H : RET _ ~~> _ |- _ ] => apply mayRet_ret in H; subst; clear H
  end.

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

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.

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.

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 _ => RET () (* NB no log *) |}.
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 }.

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.

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

Variable hC_hsval: hashinfo hsval -> ?? hsval.

(** FIXME - maybe it's not what we want ? *)
Hypothesis hC_hsval_correct: forall hs rhsv,
  hC_hsval hs ~~> rhsv ->
  (hsval_proj (hdata hs)) = (hsval_proj rhsv).
Local Hint Resolve hC_hsval_correct: wlp.

Variable hC_list_hsval: hashinfo list_hsval -> ?? list_hsval.

Hypothesis hC_list_hsval_correct: forall hs rhsv,
  hC_list_hsval hs ~~> rhsv ->
  (hsval_list_proj (hdata hs)) = (hsval_list_proj rhsv).
Local Hint Resolve hC_list_hsval_correct: wlp.

Variable hC_hsmem: hashinfo hsmem -> ?? hsmem.

Hypothesis hC_hsmem_correct: forall hs rhsv,
  hC_hsmem hs ~~> rhsv ->
  (hsmem_proj (hdata hs)) = (hsmem_proj rhsv).
Local Hint Resolve hC_hsmem_correct: wlp.

(* 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; |}.

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

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

Definition hSnil (_: unit): ?? list_hsval :=
   hC_list_hsval {| hdata := HSnil unknown_hid; hcodes := nil |}.

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

Definition hSinit (_: unit): ?? hsmem :=
   hC_hsmem {| hdata := HSinit unknown_hid; hcodes := nil |}.

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


Definition hsi_sreg_get (hst: PTree.t hsval) r: ?? hsval :=
   match PTree.get r hst with 
   | None => hSinput r
   | Some sv => RET sv
   end.

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.

(** ** Assignment of memory *)
Definition hslocal_store (hst: hsistate_local) chunk addr args src: ?? hsistate_local :=
   let pt := hst.(hsi_sreg) in
   DO hargs <~ hlist_args pt args;;
   DO hsrc <~ hsi_sreg_get pt src;;
   DO hm <~ hSstore hst chunk addr hargs hsrc;;
   RET {| hsi_smem := hm;
         hsi_ok_lsval := hsi_ok_lsval hst;
         hsi_sreg:= hsi_sreg hst
       |}.

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

(** ** 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) (hst: hsistate_local) : ?? hsval :=
  DO lhsv <~ hlist_args hst lr;;
  match rsv with
  | Rop op => hSop op lhsv hst
  | Rload trap chunk addr => hSload hst trap chunk addr lhsv
  end.

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.

(** 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 hsi <~ hSinit ();;
       DO lhsv <~ hlist_args hst lr;;
       hSop op lhsv hsi (** magically remove the dependency on sm ! *)
     end
  | Rload _ chunk addr => 
       DO lhsv <~ hlist_args hst lr;;
       hSload hst NOTRAP chunk addr lhsv
  end.

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.

Definition hslocal_set_sreg (hst: hsistate_local) (r: reg) (rsv: root_sval) (lr: list reg): ?? hsistate_local :=
  DO ok_lhsv <~
   (if may_trap rsv lr
    then DO hv <~ root_apply rsv lr hst;; RET (hv::(hsi_ok_lsval hst))
    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) |}.

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

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 =>
    DO i <~ some_or_fail ((fn_code f)!(hst.(hsi_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.

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.

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.

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.


(** * The simulation test of 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.

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

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

Lemma struct_check_correct {A} (a b: A) msg:
  WHEN struct_check a b msg ~> tt 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. congruence.
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.

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.

(** hsilocal_simu_check and properties *)

Definition seval_hsval ge sp hsv rs0 m0 := seval_sval ge sp (hsval_proj hsv) rs0 m0.
Definition seval_hsmem ge sp hsm rs0 m0 := seval_smem ge sp (hsmem_proj hsm) rs0 m0.

Definition hsi_sreg_eval ge sp (hst: PTree.t hsval) r rs0 m0: option val :=
   match PTree.get r hst with
   | None => Some (Regmap.get r rs0)
   | Some hsv => seval_hsval ge sp hsv rs0 m0
   end.

Lemma hsi_sreg_eval_correct ge sp hst r rs0 m0:
  WHEN hsi_sreg_get hst r ~> hv THEN
  hsi_sreg_eval ge sp hst r rs0 m0 = seval_hsval ge sp hv rs0 m0.
Proof.
  wlp_simplify.
  - unfold hsi_sreg_eval. rewrite H. reflexivity.
  - unfold hsi_sreg_eval. rewrite H. eapply hC_hsval_correct in Hexta1.
    simpl in Hexta1. unfold seval_hsval. rewrite <- Hexta1. simpl. reflexivity.
Qed.
Hint Resolve hsi_sreg_eval_correct: wlp.

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

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

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

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

Definition hsilocal_simu_core (oalive: option Regset.t) (hst1 hst2: hsistate_local) :=
     incl (hsi_ok_lsval hst2) (hsi_ok_lsval hst1)
  /\ (forall r, (match oalive with Some alive => Regset.In r alive | _ => True end) -> (* hsi_sreg_get hst2 r = hsi_sreg_get hst1 r *)
              PTree.get r hst2 = PTree.get r hst1)
  /\ hsi_smem hst1 = hsi_smem hst2.

Lemma hseval_preserved ge ge' rs0 m0 sp hsv:
  (forall s, Genv.find_symbol ge' s = Genv.find_symbol ge s) ->
  seval_hsval ge sp hsv rs0 m0 = seval_hsval ge' sp hsv rs0 m0.
Proof.
  intros. unfold seval_hsval. erewrite seval_preserved; eauto.
Qed.

Lemma hsmem_eval_preserved ge ge' rs0 m0 sp hsm:
  (forall s, Genv.find_symbol ge' s = Genv.find_symbol ge s) ->
  seval_hsmem ge sp hsm rs0 m0 = seval_hsmem ge' sp hsm rs0 m0.
Proof.
  intros. unfold seval_hsmem. erewrite smem_eval_preserved; eauto.
Qed.

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

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

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

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

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

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

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

Definition hsilocal_simu_check hst1 hst2 : ?? unit :=
  phys_check (hsi_smem hst2) (hsi_smem hst1) "hsilocal_simu_check: hsi_smem sets aren't equiv";;
  Sets.assert_list_incl mk_hash_params (hsi_ok_lsval hst2) (hsi_ok_lsval hst1);;
  PTree_eq_check (hsi_sreg hst1) (hsi_sreg hst2).

Theorem hsilocal_simu_check_correct hst1 hst2:
  WHEN hsilocal_simu_check hst1 hst2 ~> tt THEN
  hsilocal_simu_core None hst1 hst2.
Proof.
  wlp_simplify. constructor; [|constructor]; [assumption | | congruence].
  intros. unfold hsi_sreg_get. rewrite (PTree_eq_check_correct _ hst1 hst2); [|eassumption].
  reflexivity.
Qed.
Hint Resolve hsilocal_simu_check_correct: wlp.
Global Opaque hsilocal_simu_check.

Definition hsilocal_frame_simu_check frame hst1 hst2 : ?? unit :=
  phys_check (hsi_smem hst2) (hsi_smem hst1) "hsilocal_frame_simu_check: hsi_smem sets aren't equiv";;
  Sets.assert_list_incl mk_hash_params (hsi_ok_lsval hst2) (hsi_ok_lsval hst1);;
  PTree_frame_eq_check frame (hsi_sreg hst1) (hsi_sreg hst2).

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

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

Local Hint Resolve PTree_frame_eq_check_correct: wlp.
Local Hint Resolve regset_elements_in: core.

Theorem hsilocal_frame_simu_check_correct hst1 hst2 alive:
  WHEN hsilocal_frame_simu_check (Regset.elements alive) hst1 hst2 ~> tt THEN
  hsilocal_simu_core (Some alive) hst1 hst2.
Proof.
  wlp_simplify. constructor; [|constructor]; [assumption | | congruence].
  intros. symmetry. eauto.
(*   rewrite (PTree_frame_eq_check_correct _ (Regset.elements alive) hst1 hst2); [reflexivity | eassumption | ].
  apply regset_elements_in. assumption. *)
Qed.
Hint Resolve hsilocal_frame_simu_check_correct: wlp.
Global Opaque hsilocal_frame_simu_check.

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

Remark hsinit_seval_hsmem ge sp rs0 m0:
  WHEN hSinit () ~> init THEN
  seval_hsmem ge sp init rs0 m0 = Some m0.
Proof.
  wlp_simplify. unfold hSinit in Hexta. apply hC_hsmem_correct in Hexta. simpl in Hexta.
  unfold seval_hsmem. rewrite <- Hexta. simpl. reflexivity.
Qed.

Remark init_hsistate_local_correct ge sp rs0 m0:
  WHEN init_hsistate_local () ~> hsl THEN
  hsilocal_refines ge sp rs0 m0 hsl init_sistate_local.
Proof.
  wlp_simplify.
  constructor; constructor; simpl.
  - intro. destruct H as (_ & SMEM & SVAL). unfold hsok_local. simpl. contradiction.
  - intro. constructor; [simpl; auto|]. constructor; simpl; discriminate.
  - unfold hsok_local. simpl. intros; simpl. apply hsinit_seval_hsmem. assumption.
  - constructor.
    + intros. simpl. unfold hsi_sreg_eval. rewrite PTree.gempty. reflexivity.
    + intros r sv. rewrite PTree.gempty. discriminate.
Qed.

(** Simulation of exits *)

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

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

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

Definition hseval_condition ge sp cond hcondargs hmem rs0 m0 :=
  seval_condition ge sp cond (hsval_list_proj hcondargs) (hsmem_proj hmem) rs0 m0.

Lemma hseval_condition_preserved ge ge' sp cond args mem rs0 m0:
  (forall s : ident, Genv.find_symbol ge' s = Genv.find_symbol ge s) ->
  hseval_condition ge sp cond args mem rs0 m0 = hseval_condition ge' sp cond args mem rs0 m0.
Proof.
  intros. unfold hseval_condition. erewrite seval_condition_preserved; [|eapply H].
  reflexivity.
Qed.

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

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

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

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

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

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

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

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

Theorem hsiexit_simu_check_correct dm f hse1 hse2:
  WHEN hsiexit_simu_check dm f hse1 hse2 ~> tt THEN
  hsiexit_simu_core dm f hse1 hse2.
Proof.
  wlp_simplify. constructor; [| constructor; [| constructor]]. 2-4: assumption.
  exists a. constructor. 1-2: assumption.
Qed.
Hint Resolve hsiexit_simu_check_correct: wlp.
Global Opaque hsiexit_simu_check.

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

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

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

Definition hsiexits_refines_stat lhse lse :=
  list_forall2 hsiexit_refines_stat lhse lse.

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

Fixpoint hsiexits_simu_check (dm: PTree.t node) (f: RTLpath.function) (lhse1 lhse2: list hsistate_exit) :=
  match lhse1,lhse2 with
  | nil, nil => RET tt
  | 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.

Theorem hsiexits_simu_check_correct dm f: forall le1 le2,
  WHEN hsiexits_simu_check dm f le1 le2 ~> tt THEN
  hsiexits_simu_core dm f le1 le2.
Proof.
  induction le1; simpl.
  - destruct le2; wlp_simplify. constructor.
  - destruct le2; wlp_simplify. constructor; [assumption|].
    eapply IHle1. eassumption.
Qed.
Hint Resolve hsiexits_simu_check_correct: wlp.
Global Opaque hsiexits_simu_check.

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

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

Inductive nested_sok ge sp rs0 m0: sistate_local -> list sistate_exit -> Prop :=
    nsok_nil st: nested_sok ge sp rs0 m0 st nil
  | nsok_cons st se lse:
     (sok_local ge sp rs0 m0 st -> sok_local ge sp rs0 m0 (si_elocal se)) ->
     nested_sok ge sp rs0 m0 (si_elocal se) lse ->
     nested_sok ge sp rs0 m0 st (se::lse).

Lemma nested_sok_prop ge sp st sle rs0 m0:
  nested_sok ge sp rs0 m0 st sle ->
  sok_local ge sp rs0 m0 st ->
  forall se, In se sle -> sok_local ge sp rs0 m0 (si_elocal se).
Proof.
  induction 1; simpl; intuition (subst; eauto).
Qed.

Lemma nested_sok_elocal ge sp rs0 m0 st2 exits:
  nested_sok ge sp rs0 m0 st2 exits ->
  forall st1, (sok_local ge sp rs0 m0 st1 -> sok_local ge sp rs0 m0 st2) ->
  nested_sok ge sp rs0 m0 st1 exits.
Proof.
  induction 1; [intros; constructor|].
  intros. constructor; auto.
Qed.

Lemma nested_sok_tail ge sp rs0 m0 st lx exits:
  is_tail lx exits ->
  nested_sok ge sp rs0 m0 st exits ->
  nested_sok ge sp rs0 m0 st lx.
Proof.
  induction 1; [auto|].
  intros. inv H0. eapply IHis_tail. eapply nested_sok_elocal; eauto.
Qed.

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

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

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

Remark init_hsistate_correct_stat pc:
  WHEN init_hsistate pc ~> hst THEN
  hsistate_refines_stat hst (init_sistate pc).
Proof.
  wlp_simplify.
  constructor; constructor; simpl; auto.
Qed.
Hint Resolve init_hsistate_correct_stat: wlp.

Remark init_hsistate_correct_dyn ge sp rs0 m0 pc:
  WHEN init_hsistate pc ~> hst THEN
  hsistate_refines_dyn ge sp rs0 m0 hst (init_sistate pc).
Proof.
  unfold init_hsistate. wlp_bind hst.
  wlp_simplify.
  constructor; simpl; auto; [|constructor].
  - apply list_forall2_nil.
  - apply init_hsistate_local_correct. assumption.
  - constructor.
Qed.

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

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

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

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

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

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

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

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

Theorem hsistate_simu_check_correct dm f hst1 hst2:
  WHEN hsistate_simu_check dm f hst1 hst2 ~> tt THEN
  hsistate_simu_core dm f hst1 hst2.
Proof.
  wlp_simplify.
  constructor; [|constructor]. 1-3: assumption.
Qed.
Hint Resolve hsistate_simu_check_correct: wlp.
Global Opaque hsistate_simu_check.

Definition hsi_proj (hsi: hsval + ident) := match hsi with
  | inl hv => inl (hsval_proj hv)
  | inr id => inr id
  end.

Fixpoint barg_proj (bhv: builtin_arg hsval) := match bhv with
  | BA hv => BA (hsval_proj hv)
  | BA_splitlong ba1 ba2 => BA_splitlong (barg_proj ba1) (barg_proj ba2)
  | BA_addptr ba1 ba2 => BA_addptr (barg_proj ba1) (barg_proj ba2)
  | BA_int i => BA_int i
  | BA_long i => BA_long i
  | BA_float f => BA_float f
  | BA_single f32 => BA_single f32
  | BA_loadstack m p => BA_loadstack m p
  | BA_addrstack p => BA_addrstack p
  | BA_loadglobal c i p => BA_loadglobal c i p
  | BA_addrglobal i p => BA_addrglobal i p
  end.

Fixpoint barg_list_proj lbh := match lbh with
  | [] => []
  | bh::lbh => (barg_proj bh) :: (barg_list_proj lbh)
  end.

Definition option_hsval_proj oh := match oh with None => None | Some h => Some (hsval_proj h) end.

Definition hfinal_proj hfv := match hfv with
  | HSnone => Snone
  | HScall s hvi hlv r pc => Scall s (hsi_proj hvi) (hsval_list_proj hlv) r pc
  | HStailcall s hvi hlv => Stailcall s (hsi_proj hvi) (hsval_list_proj hlv)
  | HSbuiltin ef lbh br pc => Sbuiltin ef (barg_list_proj lbh) br pc
  | HSjumptable hv ln => Sjumptable (hsval_proj hv) ln
  | HSreturn oh => Sreturn (option_hsval_proj oh)
  end.

Section HFINAL_REFINES.

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

Definition sval_refines (hv: hsval) (sv: sval) := seval_hsval ge sp hv rs0 m0 = seval_sval ge sp sv rs0 m0.

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

Inductive list_refines: list_hsval -> list_sval -> Prop :=
  | hsnil_ref: forall h, list_refines (HSnil h) Snil
  | hscons_ref: forall lhv lsv hv sv h,
      list_refines lhv lsv ->
      sval_refines hv sv ->
      list_refines (HScons hv lhv h) (Scons sv lsv).

Inductive barg_refines: builtin_arg hsval -> builtin_arg sval -> Prop :=
  | hba_ref: forall hsv sv, sval_refines hsv sv -> barg_refines (BA hsv) (BA sv)
  | hba_splitlong: forall bha1 bha2 ba1 ba2,
      barg_refines bha1 ba1 -> barg_refines bha2 ba2 ->
      barg_refines (BA_splitlong bha1 bha2) (BA_splitlong ba1 ba2)
  | hba_addptr: forall bha1 bha2 ba1 ba2,
      barg_refines bha1 ba1 -> barg_refines bha2 ba2 ->
      barg_refines (BA_addptr bha1 bha2) (BA_addptr ba1 ba2)
  | hba_int: forall i, barg_refines (BA_int i) (BA_int i)
  | hba_long: forall l, barg_refines (BA_long l) (BA_long l)
  | hba_float: forall f, barg_refines (BA_float f) (BA_float f)
  | hba_single: forall s, barg_refines (BA_single s) (BA_single s)
  | hba_loadstack: forall chk ptr, barg_refines (BA_loadstack chk ptr) (BA_loadstack chk ptr)
  | hba_addrstack: forall ptr, barg_refines (BA_addrstack ptr) (BA_addrstack ptr)
  | hba_loadglobal: forall chk id ptr, barg_refines (BA_loadglobal chk id ptr) (BA_loadglobal chk id ptr)
  | hba_addrglobal: forall id ptr, barg_refines (BA_addrglobal id ptr) (BA_addrglobal id ptr).

Definition option_refines ohsv osv :=
  match ohsv, osv with
  | Some hsv, Some sv => sval_refines hsv sv
  | None, None => True
  | _, _ => False
  end.

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

Remark hfinal_refines_snone: hfinal_refines HSnone Snone.
Proof. constructor. Qed.

End HFINAL_REFINES.

Lemma list_proj_refines_eq ge ge' sp rs0 m0: forall lsv lhsv,
  (forall s, Genv.find_symbol ge s = Genv.find_symbol ge' s) ->
  list_refines ge sp rs0 m0 lhsv lsv ->
  forall lhsv' lsv',
  list_refines ge' sp rs0 m0 lhsv' lsv' ->
  hsval_list_proj lhsv = hsval_list_proj lhsv' ->
  seval_list_sval ge sp lsv rs0 m0 = seval_list_sval ge' sp lsv' rs0 m0.
Proof.
  induction 2; rename H into GFS.
  - simpl. intros. destruct lhsv'; try discriminate. clear H0.
    inv H. simpl. reflexivity.
  - simpl. intros. destruct lhsv'; try discriminate.
    simpl in H2. inv H2. destruct lsv'; [inv H|].
    inv H. simpl.
    assert (SVALEQ: seval_sval ge sp sv rs0 m0 = seval_sval ge' sp sv0 rs0 m0). {
      rewrite <- H10. rewrite <- H1. unfold seval_hsval. erewrite <- seval_preserved; [| eapply GFS]. congruence.
    } rewrite SVALEQ.
    erewrite IHlist_refines; eauto.
Qed.

Lemma sval_refines_proj ge ge' sp rs m hsv sv hsv' sv':
  (forall s, Genv.find_symbol ge s = Genv.find_symbol ge' s) ->
  sval_refines ge sp rs m hsv sv ->
  sval_refines ge' sp rs m hsv' sv' ->
  hsval_proj hsv = hsval_proj hsv' ->
  seval_sval ge sp sv rs m = seval_sval ge' sp sv' rs m.
Proof.
  intros GFS REF REF' PROJ.
  rewrite <- REF. rewrite <- REF'. unfold seval_hsval.
  erewrite <- seval_preserved; [| eapply GFS].
  congruence.
Qed.

Lemma barg_proj_refines_eq_single ge ge' sp rs0 m0:
  (forall s, Genv.find_symbol ge s = Genv.find_symbol ge' s) ->
  forall hsv sv, barg_refines ge sp rs0 m0 hsv sv ->
  forall hsv' sv', barg_refines ge' sp rs0 m0 hsv' sv' ->
  barg_proj hsv = barg_proj hsv' ->
  seval_builtin_sval ge sp sv rs0 m0 = seval_builtin_sval ge' sp sv' rs0 m0.
Proof.
  intro GFS. induction 1.
  all: try (simpl; intros hsv' sv' BREF' BPROJ';
    destruct hsv'; simpl in BPROJ'; try discriminate;
    inv BPROJ'; inv BREF'; simpl; try reflexivity;
    erewrite sval_refines_proj; eauto).
(* BA_splitlong *)
  - simpl. intros hsv' sv' BREF' BPROJ'.
    destruct hsv'; simpl in BPROJ'; try discriminate.
    inv BPROJ'. inv BREF'. simpl.
    erewrite IHbarg_refines2; eauto.
    erewrite IHbarg_refines1. 2: eapply H5.
    all: eauto.
(* BA_addptr *)
  - simpl. intros hsv' sv' BREF' BPROJ'.
    destruct hsv'; simpl in BPROJ'; try discriminate.
    inv BPROJ'. inv BREF'. simpl.
    erewrite IHbarg_refines2; eauto.
    erewrite IHbarg_refines1. 2: eapply H5.
    all: eauto.
Qed.

Lemma barg_proj_refines_eq ge ge' sp rs0 m0: forall lsv lhsv,
  (forall s, Genv.find_symbol ge s = Genv.find_symbol ge' s) ->
  list_forall2 (barg_refines ge sp rs0 m0) lhsv lsv ->
  forall lhsv' lsv',
  list_forall2 (barg_refines ge' sp rs0 m0) lhsv' lsv' ->
  barg_list_proj lhsv = barg_list_proj lhsv' ->
  seval_list_builtin_sval ge sp lsv rs0 m0 = seval_list_builtin_sval ge' sp lsv' rs0 m0.
Proof.
  induction 2; rename H into GFS.
  - simpl. intros. destruct lhsv'; try discriminate. clear H0.
    inv H. simpl. reflexivity.
  - simpl. intros. destruct lhsv'; try discriminate.
    simpl in H2. inv H2. destruct lsv'; [inv H|].
    inv H. simpl.
    erewrite barg_proj_refines_eq_single; eauto.
    erewrite IHlist_forall2; eauto.
Qed.

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

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

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

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

Definition hsexec_final (i: instruction) (hst: PTree.t hsval): ?? hsfval := 
  match i with
  | Icall sig ros args res pc => 
    DO svos <~ hsum_left hst ros;;
    DO sargs <~ hlist_args hst args;;
    RET (HScall sig svos sargs res pc)
  | Itailcall sig ros args =>
    DO svos <~ hsum_left hst ros;;
    DO sargs <~ hlist_args hst args;;
    RET (HStailcall sig svos sargs)
  | Ibuiltin ef args res pc =>
    DO sargs <~ hbuiltin_args hst args;;
    RET (HSbuiltin ef sargs res pc)
  | Ijumptable reg tbl =>
    DO sv <~ hsi_sreg_get hst reg;;
    RET (HSjumptable sv tbl)
  | Ireturn or => 
    match or with
    | Some r => DO hr <~ hsi_sreg_get hst r;; RET (HSreturn (Some hr))
    | None => RET (HSreturn None)
    end
  | _ => RET (HSnone)
  end.

Lemma sval_refines_local_get ge sp rs0 m0 hsl sl r:
  hsok_local ge sp rs0 m0 hsl ->
  hsilocal_refines ge sp rs0 m0 hsl sl ->
  WHEN hsi_sreg_get hsl r ~> hsv THEN
  sval_refines ge sp rs0 m0 hsv (si_sreg sl r).
Proof.
  intros HOK HREF. wlp_intro hsv. unfold sval_refines.
  erewrite <- hsi_sreg_eval_correct; eauto.
  destruct HREF as (_ & _ & A & _). rewrite <- A; [| assumption].
  reflexivity.
Qed.

Lemma hsum_left_correct ge sp rs0 m0 hsl sl ros:
  hsok_local ge sp rs0 m0 hsl ->
  hsilocal_refines ge sp rs0 m0 hsl sl ->
  WHEN hsum_left hsl ros ~> svos THEN
  sum_refines ge sp rs0 m0 svos (sum_left_map (si_sreg sl) ros).
Proof.
  intros HOK HREF. destruct ros; [| wlp_simplify].
  wlp_bind hr. wlp_simplify. unfold sval_refines.
  rewrite sval_refines_local_get; eauto.
Qed.

Lemma hSnil_correct:
  WHEN hSnil () ~> shv THEN hsval_list_proj shv = Snil.
Proof.
  wlp_simplify. unfold hSnil in Hexta. apply hC_list_hsval_correct in Hexta.
  simpl in *. symmetry. assumption.
Qed.
Global Opaque hSnil.
Hint Resolve hSnil_correct: wlp.

Lemma hScons_correct: forall lhsv hsv,
  WHEN hScons hsv lhsv ~> lhsv' THEN
  hsval_list_proj lhsv' = Scons (hsval_proj hsv) (hsval_list_proj lhsv).
Proof.
  destruct lhsv; wlp_simplify.
  - unfold hScons in Hexta. apply hC_list_hsval_correct in Hexta.
    simpl in *. congruence.
  - unfold hScons in Hexta. apply hC_list_hsval_correct in Hexta. simpl in *. congruence.
Qed.
Global Opaque hScons.
Hint Resolve hScons_correct: wlp.

Lemma hsi_sreg_get_refines ge sp rs0 m0 hsl sl r:
  hsok_local ge sp rs0 m0 hsl ->
  hsilocal_refines ge sp rs0 m0 hsl sl ->
  WHEN hsi_sreg_get hsl r ~> hsv THEN
  sval_refines ge sp rs0 m0 hsv (si_sreg sl r).
Proof.
  intros HOK HREF. wlp_intro hsv. destruct HREF as (_ & _ & A & _).
  unfold sval_refines. erewrite <- hsi_sreg_eval_correct by eassumption.
  rewrite A by assumption. reflexivity.
Qed.

Lemma hsval_list_proj_correct ge sp rs m lsv: forall lhsv,
  list_refines ge sp rs m lhsv lsv ->
  forall lhsv', hsval_list_proj lhsv' = hsval_list_proj lhsv ->
  list_refines ge sp rs m lhsv' lsv.
Proof.
  induction 1.
  - intro. simpl. intros. destruct lhsv'; try discriminate. constructor.
  - intros. simpl in H1. destruct lhsv'; try discriminate.
    simpl in H1. inv H1. apply IHlist_refines in H4.
    constructor; [assumption|].
    unfold sval_refines. unfold seval_hsval. rewrite H3. assumption.
Qed.
Hint Resolve hsval_list_proj_correct: wlp.

Lemma hsval_proj_correct ge sp rs0 m0 hsl sl hsv r:
  hsok_local ge sp rs0 m0 hsl ->
  hsilocal_refines ge sp rs0 m0 hsl sl ->
  WHEN hsi_sreg_get hsl r ~> hsv' THEN
  hsval_proj hsv = hsval_proj hsv' ->
  sval_refines ge sp rs0 m0 hsv (si_sreg sl r).
Proof.
  intros HOK HREF. wlp_intro hsv'. intros PROJ.
  unfold sval_refines. unfold seval_hsval.
  rewrite PROJ. enough (seval_sval ge sp (hsval_proj hsv') rs0 m0 = seval_hsval ge sp hsv' rs0 m0) as ->; [|reflexivity].
  erewrite hsi_sreg_get_refines; eauto.
Qed.
Hint Resolve hsval_proj_correct: wlp.

Lemma hlist_args_correct ge sp rs0 m0 hsl sl:
  hsok_local ge sp rs0 m0 hsl ->
  hsilocal_refines ge sp rs0 m0 hsl sl ->
  forall lr, WHEN hlist_args hsl lr ~> shv THEN
  list_refines ge sp rs0 m0 shv (list_sval_inj (List.map (si_sreg sl) lr)).
Proof.
  intros HOK HREF. induction lr.
  - simpl. wlp_simplify. destruct exta; try discriminate. constructor.
  - simpl. wlp_bind v. wlp_bind lhsv. wlp_simplify.
    apply IHlr in Hlhsv. clear IHlr.
    destruct exta; try discriminate. simpl in H. inv H. constructor.
    + eapply hsval_list_proj_correct; eauto.
    + eapply hsval_proj_correct; eauto.
Qed.
Global Opaque hlist_args.
Hint Resolve hlist_args_correct: wlp.

Lemma hbuiltin_arg_correct ge sp rs0 m0 hsl sl:
  hsok_local ge sp rs0 m0 hsl ->
  hsilocal_refines ge sp rs0 m0 hsl sl ->
  forall br,
  WHEN hbuiltin_arg hsl br ~> bhsv THEN
  barg_refines ge sp rs0 m0 bhsv (builtin_arg_map (si_sreg sl) br).
Proof.
  intros HOK HREF.
  induction br.
  all: try (wlp_simplify; constructor; auto; fail).
  (* BA *)
  - simpl. wlp_bind hsv. wlp_simplify. constructor. eapply hsi_sreg_get_refines; eauto.
Qed.

Lemma hbuiltin_args_correct ge sp rs0 m0 hsl sl:
  hsok_local ge sp rs0 m0 hsl ->
  hsilocal_refines ge sp rs0 m0 hsl sl ->
  forall lbr,
  WHEN hbuiltin_args hsl lbr ~> lbhsv THEN
  list_forall2 (barg_refines ge sp rs0 m0) lbhsv (List.map (builtin_arg_map (si_sreg sl)) lbr).
Proof.
  intros HOK HREF.
  induction lbr; [wlp_simplify; constructor|].
  simpl. wlp_bind ha. wlp_bind hl. wlp_simplify.
  constructor; [|auto]. eapply hbuiltin_arg_correct; eauto.
Qed.

Lemma hsexec_final_correct ge sp rs0 m0 hsl sl i:
  hsok_local ge sp rs0 m0 hsl ->
  hsilocal_refines ge sp rs0 m0 hsl sl ->
  WHEN hsexec_final i hsl ~> hsf THEN
  hfinal_refines ge sp rs0 m0 hsf (sexec_final i sl).
Proof.
  intro HOK.
  destruct i; simpl; intros HLREF; try (wlp_simplify; apply hfinal_refines_snone).
  (* Scall *)
  - wlp_bind svos. wlp_bind sargs. wlp_simplify. constructor.
    + eapply hsum_left_correct; eauto.
    + eapply hlist_args_correct; eauto.
  (* Stailcall *)
  - wlp_bind svos. wlp_bind sargs. wlp_simplify. constructor.
    + eapply hsum_left_correct; eauto.
    + eapply hlist_args_correct; eauto.
  (* Sbuiltin *)
  - wlp_simplify. constructor. eapply hbuiltin_args_correct; eauto.
  (* Sjumptable *)
  - wlp_bind sv. wlp_simplify. constructor. eapply hsi_sreg_get_refines; eauto.
  (* Sreturn *)
  - destruct o.
    -- wlp_bind sv. wlp_simplify. constructor. simpl.
       eapply hsi_sreg_get_refines; eauto.
    -- wlp_simplify. repeat constructor.
Qed.

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' ~> tt THEN
  ptree_get_list dm lpc' = Some lpc.
Proof.
  induction lpc.
  - destruct lpc'; wlp_simplify.
  - destruct lpc'; wlp_simplify. rewrite H. rewrite H0. reflexivity.
Qed.
Global Opaque revmap_check_list.
Hint Resolve revmap_check_list_correct: wlp.

Definition svos_simu_check (svos1 svos2: hsval + ident) :=
  match svos1, svos2 with
  | inl sv1, inl sv2 => phys_check sv1 sv2 "svos_simu_check: sval mismatch"
  | 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 ~> tt THEN
  svos1 = svos2.
Proof.
  destruct svos1; destruct svos2; wlp_simplify; try wlp_absurd.
  all: congruence.
Qed.
Global Opaque svos_simu_check.
Hint Resolve svos_simu_check_correct: wlp.

Fixpoint builtin_arg_simu_check (bs bs': builtin_arg hsval) :=
  match bs with
  | BA sv =>
    match bs' with
    | BA sv' => phys_check sv sv' "builtin_arg_simu_check: sval mismatch"
    | _ => FAILWITH "builtin_arg_simu_check: BA mismatch"
    end
  | BA_splitlong lo hi =>
    match bs' with
    | BA_splitlong lo' hi' =>
        builtin_arg_simu_check lo lo';;
        builtin_arg_simu_check hi hi'
    | _ => FAILWITH "builtin_arg_simu_check: BA_splitlong mismatch"
    end
  | BA_addptr b1 b2 =>
    match bs' with
    | BA_addptr b1' b2' =>
        builtin_arg_simu_check b1 b1';;
        builtin_arg_simu_check b2 b2'
    | _ => FAILWITH "builtin_arg_simu_check: BA_addptr mismatch"
    end
  | bs => struct_check bs bs' "builtin_arg_simu_check: basic mismatch"
  end.

Lemma builtin_arg_simu_check_correct: forall bs1 bs2,
  WHEN builtin_arg_simu_check bs1 bs2 ~> tt THEN
  barg_proj bs1 = barg_proj bs2.
Proof.
  induction bs1.
  all: try (intros; simpl; wlp_simplify; subst; reflexivity).
  (* BA *)
  - destruct bs2; wlp_simplify; try wlp_absurd. congruence.
  (* BA_splitlong *)
  - destruct bs2; try (wlp_simplify; wlp_absurd). simpl.
    wlp_bind b1. wlp_intro b2.
    rewrite IHbs1_1 by eassumption. rewrite IHbs1_2 by eassumption.
    reflexivity.
  (* BA_addptr *)
  - destruct bs2; try (wlp_simplify; wlp_absurd). simpl.
    wlp_bind b1. wlp_intro b2.
    rewrite IHbs1_1 by eassumption. rewrite IHbs1_2 by eassumption.
    reflexivity.
Qed.
Global Opaque builtin_arg_simu_check.
Hint Resolve builtin_arg_simu_check_correct: wlp.

Fixpoint list_builtin_arg_simu_check lbs1 lbs2 :=
  match lbs1, lbs2 with
  | nil, nil => RET tt
  | 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 ~> tt THEN
  barg_list_proj lbs1 = barg_list_proj lbs2.
Proof.
  induction lbs1.
  - wlp_simplify. destruct lbs2; [simpl; reflexivity|].
    simpl in Hexta. wlp_absurd.
  - destruct lbs2; wlp_simplify; try wlp_absurd.
    congruence.
Qed.
Global Opaque list_builtin_arg_simu_check.
Hint Resolve list_builtin_arg_simu_check_correct: wlp.

Definition sfval_simu_check (dm: PTree.t node) (f: RTLpath.function) (opc1 opc2: node) (fv1 fv2: hsfval) :=
  match fv1, fv2 with
  | HSnone, HSnone => revmap_check_single dm opc1 opc2
  | 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.


Theorem sfval_simu_check_correct dm f opc1 opc2 fv1 fv2:
  WHEN sfval_simu_check dm f opc1 opc2 fv1 fv2 ~> tt THEN
  hfinal_simu_core dm f opc1 opc2 fv1 fv2.
Proof.
  destruct fv1; destruct fv2; try (wlp_simplify; simpl in Hexta; wlp_absurd).
  (* HScall *)
  - simpl. wlp_bind u1 REVMAP. wlp_bind u2 SIG. wlp_bind u3 RES.
    wlp_bind u4 SVOS. wlp_intro u5 LSV.
    apply phys_check_correct in SIG. apply phys_check_correct in RES.
    apply revmap_check_single_correct in REVMAP. apply phys_check_correct in LSV.
    apply svos_simu_check_correct in SVOS. subst. repeat (constructor; auto).
  (* HStailcall *)
  - simpl. wlp_bind u1 SIG. wlp_bind u2 SVOS. wlp_intro u3 LSV.
    apply phys_check_correct in SIG. apply phys_check_correct in LSV.
    apply svos_simu_check_correct in SVOS. subst. repeat (constructor; auto).
  (* HSbuiltin *)
  - simpl. wlp_bind u1 RMAP. wlp_bind u2 EF. wlp_bind u3 RES.
    wlp_intro u4 SARGS.
    apply phys_check_correct in EF. apply phys_check_correct in RES.
    apply list_builtin_arg_simu_check_correct in SARGS. apply revmap_check_single_correct in RMAP.
    subst. repeat (constructor; auto).
  (* HSjumptable *)
  - simpl. wlp_simplify. subst. constructor; auto.
  (* HSreturn *)
  - wlp_simplify. subst. reflexivity.
Qed.
Hint Resolve sfval_simu_check_correct: wlp.
Global Opaque hfinal_simu_core.

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

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

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

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

Definition hsstate_simu_check (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsstate) :=
  hsistate_simu_check dm f (hinternal hst1) (hinternal hst2);;
  sfval_simu_check dm f (hsi_pc hst1) (hsi_pc hst2) (hfinal hst1) (hfinal hst2).

Theorem hsstate_simu_check_correct dm f hst1 hst2:
  WHEN hsstate_simu_check dm f hst1 hst2 ~> tt THEN
  hsstate_simu_core dm f hst1 hst2.
Proof.
  wlp_simplify. constructor. 1-2: assumption.
Qed.
Hint Resolve hsstate_simu_check_correct: wlp.
Global Opaque hsstate_simu_core. 

Definition seval_list_hsval ge sp lhsv rs m := seval_list_sval ge sp (hsval_list_proj lhsv) rs m.

Definition hok_args ge sp rs0 m0 hst lr :=
  WHEN hlist_args (hsi_sreg hst) lr ~> lhsv THEN
  hsok_local ge sp rs0 m0 hst -> 
  (seval_list_hsval ge sp lhsv rs0 m0 <> None).

Lemma hsist_set_local_correct_dyn ge sp rs0 m0 hst st pc hnxt nxt:
  hsistate_refines_dyn ge sp rs0 m0 hst st ->
  hsilocal_refines ge sp rs0 m0 hnxt nxt ->
  (sok_local ge sp rs0 m0 nxt -> sok_local ge sp rs0 m0 (si_local st)) ->
  hsistate_refines_dyn ge sp rs0 m0 (hsist_set_local hst pc hnxt) (sist_set_local st pc nxt).
Proof.
  unfold hsistate_refines_dyn; simpl.
  intros (EREF & LREF & NESTED) LREFN SOK; intuition.
  destruct NESTED as [|st0 se lse TOP NEST]; econstructor; simpl; auto.
Qed.

(* Completely lost on that one *)
(* Lemma hsok_local_set_sreg ge sp rs0 m0 hst r (rsv:root_sval) lr:
  WHEN hslocal_set_sreg hst r rsv lr ~> hst' THEN
  hok_args ge sp rs0 m0 hst lr ->
  hsok_local ge sp rs0 m0 hst'
  <-> (hsok_local ge sp rs0 m0 hst /\ (WHEN root_apply rsv lr hst ~> hsv THEN seval_hsval ge sp hsv rs0 m0 <> None)).
Proof.
  unfold hslocal_set_sreg. wlp_bind lhsvok. wlp_bind hsv. wlp_ret hst'.
  intros HOK.
  destruct may_trap eqn: MAYTRAP.
  - wlp_hbind hv. wlp_hret. constructor.
    + unfold hsok_local. simpl. intro. constructor.
      * intros. apply H. right. assumption.
      * wlp_intro hsv'. apply H.


  unfold hok_args, hsok_local. simpl.

  unfold hslocal_set_sreg, ok_args, hsok_local; simpl.
  destruct may_trap eqn: MAYTRAP; simpl; intuition (subst; eauto).
  eapply may_trap_correct; eauto.
Qed. *)

Lemma seval_list_sval_proj ge sp rs0 m0: forall lhsv lsv,
  list_refines ge sp rs0 m0 lhsv lsv ->
  seval_list_sval ge sp (hsval_list_proj lhsv) rs0 m0 = seval_list_sval ge sp lsv rs0 m0.
Proof.
  induction lhsv.
  - destruct lsv; simpl; intros H; [reflexivity | inv H].
  - destruct lsv; [intro H; inv H|].
    intros. inv H. simpl. erewrite IHlhsv; eauto.
    rewrite H6. reflexivity.
Qed.

Lemma hSop_correct ge sp rs0 m0 op lhsv lsv hst st:
  WHEN hSop op lhsv (hsi_smem hst) ~> hsv THEN
  hsok_local ge sp rs0 m0 hst ->
  list_refines ge sp rs0 m0 lhsv lsv ->
  hsilocal_refines ge sp rs0 m0 hst st ->
  seval_hsval ge sp hsv rs0 m0 = seval_sval ge sp (Sop op lsv (si_smem st)) rs0 m0.
Proof.
  wlp_simplify. apply hC_hsval_correct in Hexta1. simpl in *. unfold seval_hsval.
  rewrite <- Hexta1. simpl. clear Hexta1.
  erewrite seval_list_sval_proj; eauto. clear H0.
  destruct H1 as (A & B & C & D). rewrite <- B; eauto.
Qed.

(** Version of hSop_correct with weaker hypothesis *)
Lemma hSop_correct_mem ge sp rs0 m0 op lhsv lsv hsm sm:
  WHEN hSop op lhsv hsm ~> hsv THEN
  seval_hsmem ge sp hsm rs0 m0 = seval_smem ge sp sm rs0 m0 ->
  list_refines ge sp rs0 m0 lhsv lsv ->
  seval_hsval ge sp hsv rs0 m0 = seval_sval ge sp (Sop op lsv sm) rs0 m0.
Proof.
  wlp_simplify. apply hC_hsval_correct in Hexta1. simpl in *. unfold seval_hsval.
  rewrite <- Hexta1. simpl. clear Hexta1.
  erewrite seval_list_sval_proj; eauto. clear H0.
  rewrite <- H. eauto.
Qed.

Lemma hSload_correct ge sp rs0 m0 lhsv lsv hst st trap addr chunk:
  WHEN hSload (hsi_smem hst) trap chunk addr lhsv ~> hsv THEN
  hsok_local ge sp rs0 m0 hst ->
  list_refines ge sp rs0 m0 lhsv lsv ->
  hsilocal_refines ge sp rs0 m0 hst st ->
  seval_hsval ge sp hsv rs0 m0 = seval_sval ge sp (Sload (si_smem st) trap chunk addr lsv) rs0 m0.
Proof.
  wlp_simplify. apply hC_hsval_correct in Hexta3. simpl in *. unfold seval_hsval.
  rewrite <- Hexta3. simpl. clear Hexta3.
  erewrite seval_list_sval_proj; eauto. clear H0.
  destruct H1 as (A & B & C & D). rewrite <- B; eauto.
Qed.

Lemma hsinit_sinit ge sp rs0 m0:
  WHEN hSinit () ~> init THEN
  seval_hsmem ge sp init rs0 m0 = seval_smem ge sp Sinit rs0 m0.
Proof.
  wlp_intro init. eapply hsinit_seval_hsmem in Hinit; eauto.
Qed.

Lemma simplify_correct (rsv: root_sval) lr (ge: RTL.genv) (sp: val) rs0 m0 v hst st:
  WHEN root_apply rsv lr hst ~> hsv THEN
  hsok_local ge sp rs0 m0 hst ->
  hsilocal_refines ge sp rs0 m0 hst st ->
  seval_hsval ge sp hsv rs0 m0 = Some v ->
  WHEN simplify rsv lr hst ~> hsv' THEN
  seval_hsval ge sp hsv' rs0 m0 = Some v.
Proof.
  wlp_bind lhsv. wlp_intro hsv. intros HOK HREF HEVAL.
  eapply hlist_args_correct in Hlhsv; eauto.
  destruct rsv; simpl.
  (* Rop *)
  - exploit hSop_correct; eauto. intros EVALMOV. clear Hlhsv. clear Hhsv.
    destruct (is_move_operation _ _) eqn:IMOVE.
    + apply is_move_operation_correct in IMOVE. inv IMOVE.
      rewrite <- HEVAL. rewrite EVALMOV. wlp_intro hsv'.
      simpl. destruct HREF as (A & B & C & D). rewrite <- C; eauto.
      rewrite hsi_sreg_eval_correct; eauto.
      destruct (seval_hsval ge sp hsv' rs0 m0); [|reflexivity].
      apply A in HOK. destruct HOK as (_ & MOK & _).
      destruct (seval_smem _ _ _ _ _); [reflexivity|contradiction].
    + clear IMOVE. wlp_bind hsm. wlp_bind lhsv'. wlp_intro hsv'.
      eapply hlist_args_correct in Hlhsv'; eauto.
      rewrite hSop_correct_mem; eauto; [|eapply hsinit_sinit; eauto].
      clear Hlhsv'. clear Hhsv'. rewrite <- HEVAL. rewrite EVALMOV.
      admit. (** Voir avec Sylvain - je ne sais plus où on en est sur les dépendances mémoires avec les op *)
  (* Rload *)
  - exploit hSload_correct; eauto. intros EVALLOAD.
    wlp_bind lhsv'. wlp_intro hsv'. eapply hlist_args_correct in Hlhsv'; eauto.
    rewrite hSload_correct; eauto. rewrite EVALLOAD in HEVAL.
    destruct trap; simpl; auto. simpl in HEVAL.
    destruct (seval_list_sval _ _ _ _) as [args|] eqn: Hargs; try congruence.
    destruct (eval_addressing _ _ _ _) as [a|] eqn: Ha; try congruence.
    destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
    rewrite HEVAL. reflexivity.
Admitted.

Lemma hsok_local_set_sreg ge sp rs0 m0 hst r (rsv:root_sval) lr:
  hok_args ge sp rs0 m0 hst lr ->
  WHEN hslocal_set_sreg hst r rsv lr ~> hst' THEN
  hsok_local ge sp rs0 m0 hst'
  <-> (hsok_local ge sp rs0 m0 hst /\ 
    (WHEN root_apply rsv lr hst ~> hsv' THEN seval_hsval ge sp hsv' rs0 m0 <> None)).
Proof.
(*   unfold hslocal_set_sreg, ok_args, hsok_local; simpl.
  destruct may_trap eqn: MAYTRAP; simpl; intuition (subst; eauto).
  eapply may_trap_correct; eauto. *)
Admitted.

Lemma slocal_set_sreg_preserves_sok ge sp rs m st r sv:
  sok_local ge sp rs m st <-> sok_local ge sp rs m (slocal_set_sreg st r sv).
Proof.
Admitted.

Lemma root_apply_none ge sp rsv rs m hst lr:
  hsok_local ge sp rs m hst ->
  WHEN root_apply rsv lr hst ~> hsv THEN
  seval_hsval ge sp hsv rs m <> None.
Proof.
Admitted.

Lemma hslocal_set_sreg_preserves_smem ge sp hst rs0 m0 r rsv lr:
  WHEN hslocal_set_sreg hst r rsv lr ~> hst' THEN
  seval_hsmem ge sp hst' rs0 m0 = seval_hsmem ge sp hst rs0 m0.
Proof.
Admitted.

Lemma hslocal_set_sreg_preserves_hsok ge sp rs m hst r rsv lr:
  WHEN hslocal_set_sreg hst r rsv lr ~> hst' THEN
  hsok_local ge sp rs m hst <-> hsok_local ge sp rs m hst'.
Proof.
Admitted.

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

(** TODO - express some lemma about root_apply_correct and simplify_correct
  * Figure out how to prove this stuff *)
Lemma hslocal_set_sreg_correct ge sp rs0 m0 hst st r (rsv:root_sval) lr sv':
  hsilocal_refines ge sp rs0 m0 hst st ->
  hok_args ge sp rs0 m0 hst lr ->
  ( hsok_local ge sp rs0 m0 hst ->
    WHEN root_apply rsv lr hst ~> hsv THEN
    seval_sval ge sp sv' rs0 m0 = seval_hsval ge sp hsv rs0 m0) ->
  WHEN hslocal_set_sreg hst r rsv lr ~> hst' THEN
  hsilocal_refines ge sp rs0 m0 hst' (slocal_set_sreg st r sv').
Proof.
  intros HREF HOK REVAL. wlp_intro hst'.
  unfold hsilocal_refines. split; [|split; [|split]].
  + symmetry. eapply iff_trans. eapply hsok_local_set_sreg; eauto.
    constructor.
    * intros (HOKL & REVAL'). apply slocal_set_sreg_preserves_sok.
      destruct HREF as (A & _). apply A in HOKL. assumption.
    * intros SOKL. rewrite <- slocal_set_sreg_preserves_sok in SOKL.
      destruct HREF as (A & _). apply A in SOKL.
      split; [assumption|].
      eapply root_apply_none; eauto.
  + intros HOKL. simpl. rewrite hslocal_set_sreg_preserves_smem; eauto.
    destruct HREF as (_ & A & _). rewrite A; auto.
    eapply hslocal_set_sreg_preserves_hsok; eauto.
  + intros HOKL. simpl. intro r0. unfold hslocal_set_sreg in Hhst'.
    wlp_hbind ok_lhsv. wlp_hbind hsv'. wlp_hret. simpl.
    rewrite red_PTree_set_correct. unfold hsi_sreg_eval.
    destruct (Pos.eq_dec r r0).
    * subst. rewrite PTree.gss. (* Something about simplify_correct ? *) admit.
    * admit.
  + admit.

(*   intros (ROK & RMEM & RVAL) OKA RSV.
  unfold hsilocal_refines; simpl. rewrite! hsok_local_set_sreg; eauto. split.
  + rewrite <- ROK in RSV; rewrite sok_local_set_sreg; eauto.
    intuition congruence.
  + split; try tauto.
    intros (HOKL & RSV2) r0.
    rewrite red_PTree_set_correct.
    rewrite hsi_sreg_eval_correct. unfold hsi_sreg_get.
    destruct (Pos.eq_dec r r0).
    * subst. rewrite PTree.gss, RSV; auto.
      destruct (seval_sval ge sp (rsv lsv (hsi_smem hst))) eqn: RSV3; simpl; try congruence.
      eapply simplify_correct; eauto.
    * intros; rewrite PTree.gso; auto.
      rewrite <- RVAL, hsi_sreg_eval_correct; auto. *)
Admitted.




Lemma seval_list_hsval_refines ge sp rs0 m0 hst st lr:
  hsok_local ge sp rs0 m0 hst ->
  hsilocal_refines ge sp rs0 m0 hst st ->
  WHEN hlist_args hst lr ~> lhsv THEN
  seval_list_hsval ge sp lhsv rs0 m0 = seval_list_sval ge sp (list_sval_inj (List.map (si_sreg st) lr)) rs0 m0.
Proof.
  intros OKL HLREF. wlp_simplify.
  destruct lr.
  - simpl in *. inv H. reflexivity.
  - inv H. simpl. unfold seval_list_hsval. simpl. rewrite H4. erewrite seval_list_sval_proj; eauto.
Qed.

Lemma seval_list_sval_none ge sp (srs: reg -> sval) rs0 m0: forall lr,
  (forall r, seval_sval ge sp (srs r) rs0 m0 <> None) ->
  seval_list_sval ge sp (list_sval_inj (List.map srs lr)) rs0 m0 <> None.
Proof.
  induction lr.
  - simpl. discriminate.
  - intro SR. simpl. destruct (seval_sval _ _ _ _ _) eqn:V.
    2: { apply SR in V. inv V. }
    destruct (seval_list_sval _ _ _ _ _) eqn:LV.
    2: { apply IHlr in SR. assumption. }
    discriminate.
Qed.

Lemma refines_okargs ge sp rs0 m0 hst st lr: 
  hsistate_refines_dyn ge sp rs0 m0 hst st ->
  hok_args ge sp rs0 m0 (hsi_local hst) lr.
Proof.
  unfold hok_args.
  intros (_ & HLREF & _). wlp_intro lhsv LHSV. intros OK.
  exploit hlist_args_correct; eauto. intro LREF.
  erewrite seval_list_hsval_refines; eauto.
  destruct HLREF as (OKEQ & _ & _).
  rewrite <- OKEQ in OK.
  destruct OK as (_ & _ & OK).
  apply seval_list_sval_none. assumption.
Qed.

(* Local Hint Resolve refines_okargs: core. *)
Lemma hsiexec_inst_correct_dyn ge sp rs0 m0 i hst st hst' st':
  WHEN hsiexec_inst i hst ~> ohst' THEN
  ohst' = Some hst' ->
  siexec_inst i st = Some st' ->
  hsistate_refines_dyn ge sp rs0 m0 hst st -> hsistate_refines_dyn ge sp rs0 m0 hst' st'.
Proof.
  destruct i.
  (* Inop *)
  - wlp_simplify. inv H. inv H0. auto.
  (* Iop *)
  - simpl. wlp_bind next NEXT. wlp_simplify. inv H. inv H0.
    eapply hsist_set_local_correct_dyn; eauto.
    + destruct H1 as (A & B & C).
      eapply hslocal_set_sreg_correct; eauto.
      { eapply refines_okargs. repeat (econstructor; eauto). }
      simpl. intro HOK. unfold root_apply. wlp_bind lhsv LHSV. wlp_intro hsv HSV.
      eapply hlist_args_correct in LHSV; eauto.
      erewrite hSop_correct; eauto. simpl. reflexivity.
    + unfold sok_local; simpl; intros (PRE & MEM & REG).
      intuition.
      generalize (REG r0); clear REG.
      destruct (Pos.eq_dec r r0); simpl; intuition (subst; eauto).
  (* Iload *)
  - simpl.  wlp_bind next NEXT. wlp_simplify. inv H. inv H0.
    eapply hsist_set_local_correct_dyn; eauto.
    + destruct H1 as (A & B & C).
      eapply hslocal_set_sreg_correct; eauto.
      { eapply refines_okargs. repeat (econstructor; eauto). }
      simpl. intro HOK. unfold root_apply. wlp_bind lhsv LHSV. wlp_intro hsv HSV.
      eapply hlist_args_correct in LHSV; eauto.
      erewrite hSload_correct; eauto. simpl. reflexivity.
    + unfold sok_local; simpl; intros (PRE & MEM & REG).
      intuition.
      generalize (REG r0); clear REG.
      destruct (Pos.eq_dec r r0); simpl; intuition (subst; eauto).
  (* Istore *)
  - simpl. wlp_bind next NEXT. wlp_simplify. inv H. inv H0.
    eapply hsist_set_local_correct_dyn; eauto.
    + admit. (** TODO - port hslocal_set_smem_correct *)
    + unfold sok_local; simpl; intuition.
  (* Icall *)
  - admit.
  (* Itailcall *)
  - admit.
  (* Ibuiltin *)
  - admit.
  (* Icond *)
  - admit.
  (* Ijumptable *)
  - admit.
  (* Ireturn *)
  - admit.
Admitted.


(* PROOF from RTLpathSE_impl.v
  destruct i; simpl; intros STEP1 STEP2; inversion_clear STEP1;
    inversion_clear STEP2; discriminate || (intro REF; eauto).
  - (* Iop *)
    eapply hsist_set_local_correct_dyn; eauto.
    + eapply hslocal_set_sreg_correct; eauto.
      simpl; intros.
      erewrite seval_list_sval_refines; eauto.
      erewrite seval_smem_refines; eauto.
    + unfold sok_local; simpl; intros (PRE & MEM & REG).
      intuition.
      generalize (REG r0); clear REG.
      destruct (Pos.eq_dec r r0); simpl; intuition (subst; eauto).
  - (* Iload *)
    eapply hsist_set_local_correct_dyn; eauto.
    + eapply hslocal_set_sreg_correct; eauto.
      simpl; intros.
      erewrite seval_list_sval_refines; eauto.
      erewrite seval_smem_refines; eauto.
    + unfold sok_local; simpl; intros (PRE & MEM & REG).
      intuition.
      generalize (REG r0); clear REG.
      destruct (Pos.eq_dec r r0); simpl; intuition (subst; eauto).
  - (* Istore *)
    eapply hsist_set_local_correct_dyn; eauto.
    + eapply hslocal_set_mem_correct; eauto.
      * simpl. simplify_SOME x.
      * intros. simpl.
        erewrite seval_list_sval_refines; eauto.
        erewrite seval_smem_refines; eauto.
        erewrite seval_sval_refines; eauto.
    + unfold sok_local; simpl; intuition.
  - (* Icond *)
    destruct REF as (EXREF & LREF & NEST).
    split.
    + constructor; simpl; auto.
      constructor; simpl; auto.
      intros; erewrite seval_condition_refines; eauto.
      unfold seval_condition.
      erewrite seval_list_sval_refines; eauto.
    + split; simpl; auto.
      destruct NEST as [|st0 se lse TOP NEST];
      econstructor; simpl; auto; constructor; auto.
Qed.  *)

Definition hsexec (f: function) (pc:node): ?? hsstate :=
  DO path <~ some_or_fail ((fn_path f)!pc) "hsexec.internal_error.1";;
  DO hinit <~ init_hsistate pc;;
  DO hst <~ hsiexec_path path.(psize) f hinit;;
  DO i <~ some_or_fail ((fn_code f)!(hst.(hsi_pc))) "hsexec.internal_error.2";;
  DO ohst <~ hsiexec_inst i hst;;
  match ohst with
  | Some hst' => RET {| hinternal := hst'; hfinal := HSnone |}
  | None => DO hsvf <~ hsexec_final i hst.(hsi_local);;
            RET {| hinternal := hst; hfinal := hsvf |}
  end.

(**
 * init_hsistate_correct_stat : OK
 * init_hsistate_correct_dyn : OK
 * hsexec_final_correct : OK
 * hsiexec_inst_correct_dyn : TODO
 * hsiexec_path_correct_dyn : TODO
 * hfinal_refines_snone : OK
 *)

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

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

End CanonBuilding.

Definition simu_check_single (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) (m: node * node): ?? unit :=
  let (pc2, pc1) := m in
  (* creating the hash-consing tables *)
  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 *)
  DO hst1 <~ hsexec f pc1;;
  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 simu_check_single.
  wlp_bind hC_sval HSVAL. wlp_bind hC_list_hsval HLSVAL.
  wlp_bind hC_hsmem HSMEM. wlp_bind hst1 HSEXEC1. wlp_bind hst2 HSEXEC2.
  wlp_intro u HSIMU.
  unfold sexec_simu. intros st1 SEXEC. explore.
  assert (TODO1: forall hs rhsv, hC hC_sval hs ~~> rhsv -> hsval_proj (hdata hs) = hsval_proj rhsv)
    by admit.
  assert (TODO2: forall hs rhsv, hC hC_list_hsval hs ~~> rhsv -> hsval_list_proj (hdata hs) = hsval_list_proj rhsv)
    by admit.
  assert (TODO3: forall hs rhsv, hC hC_hsmem hs ~~> rhsv -> hsmem_proj (hdata hs) = hsmem_proj rhsv)
    by admit.
  exploit hsexec_correct; eauto.
  intros (st2 & SEXEC2 & REF2).
  exploit hsexec_correct. 4: eapply HSEXEC1. all: eauto.
  intros (st0 & SEXEC1 & REF1).
  rewrite SEXEC1 in SEXEC. inv SEXEC.
  eexists. split; eauto.
  intros ctx. eapply hsstate_simu_check_correct in HSIMU; eauto.
  eapply hsstate_simu_core_correct; eauto.
Admitted.
Global Opaque simu_check_single.
Global Hint Resolve simu_check_single_correct: wlp.

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);;
   println("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.