(** 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.
Require Import RTLpathSE_theory RTLpathLivegenproof.
Require Import Axioms RTLpathSE_simu_specs.
Require Import RTLpathSE_simplify.

Local Open Scope error_monad_scope.
Local Open Scope option_monad_scope.

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

Local Open Scope impure.
Local Open Scope hse.

Import ListNotations.
Local Open Scope list_scope.

Definition XDEBUG {A} (x:A) (k: A -> ?? pstring): ?? unit := RET tt. (* TO REMOVE DEBUG INFO *)
(*Definition XDEBUG {A} (x:A) (k: A -> ?? pstring): ?? unit := DO s <~ k x;; println ("DEBUG simu_check:" +; s). (* TO INSERT DEBUG INFO *)*)

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

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

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 _ => HSop o lhsv 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.


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

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

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

(** 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 _, HSop op2 lsv2 _  =>
     DO b1 <~ phys_eq lsv1 lsv2;;
     if b1
     then struct_eq op1 op2 (* NB: really need a struct_eq here ? *)
     else RET false
  | HSload sm1 trap1 chk1 addr1 lsv1 _, HSload sm2 trap2 chk2 addr2 lsv2 _ =>
     DO b1 <~ phys_eq lsv1 lsv2;;
     DO b2 <~ phys_eq sm1 sm2;;
     DO b3 <~ struct_eq trap1 trap2;;
     DO b4 <~ struct_eq chk1 chk2;;
     if b1 && b2 && b3 && b4
     then struct_eq addr1 addr2
     else RET false
  | _,_ => RET false
  end.


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

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

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

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

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

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


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

Program Definition mk_hash_params: Dict.hash_params hsval :=
 {|
    Dict.test_eq := phys_eq;
    Dict.hashing := fun (ht: hsval) => RET (hsval_get_hid ht);
    Dict.log := fun hv =>
         DO hv_name <~ string_of_hashcode (hsval_get_hid hv);;
         println ("unexpected undef behavior of hashcode:" +; (CamlStr hv_name)) |}.
Obligation 1.
  wlp_simplify.
Qed.

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

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

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

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

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

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

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

Variable hC_hsval: hashinfo hsval -> ?? hsval.

Hypothesis hC_hsval_correct: forall hs,
  WHEN hC_hsval hs ~> hs' THEN forall ge sp rs0 m0,
    seval_hsval ge sp (hdata hs) rs0 m0 = seval_hsval ge sp hs' rs0 m0.

Variable hC_list_hsval: hashinfo list_hsval -> ?? list_hsval.
Hypothesis hC_list_hsval_correct: forall lh,
  WHEN hC_list_hsval lh ~> lh' THEN forall ge sp rs0 m0,
    seval_list_hsval ge sp (hdata lh) rs0 m0 = seval_list_hsval ge sp lh' rs0 m0.

Variable hC_hsmem: hashinfo hsmem -> ?? hsmem.
Hypothesis hC_hsmem_correct: forall hm,
  WHEN hC_hsmem hm ~> hm' THEN forall ge sp rs0 m0,
    seval_hsmem ge sp (hdata hm) rs0 m0 = seval_hsmem ge sp hm' rs0 m0.

(* First, we wrap constructors for hashed values !*)

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

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

Definition hSinput (r:reg): ?? hsval :=
   DO hv <~ hSinput_hcodes r;;
   hC_hsval {| hdata:=HSinput r unknown_hid; hcodes :=hv; |}.

Lemma hSinput_correct r:
  WHEN hSinput r ~> hv THEN forall ge sp rs0 m0,
    sval_refines ge sp rs0 m0 hv (Sinput r).
Proof.
  wlp_simplify.
Qed.
Global Opaque hSinput.
Local Hint Resolve hSinput_correct: wlp.

Definition hSop_hcodes (op:operation) (lhsv: list_hsval) :=
   DO hc <~ hash op_hcode;;
   DO hv <~ hash op;;
   RET [hc;hv;list_hsval_get_hid lhsv].
Extraction Inline hSop_hcodes.

Definition hSop (op:operation) (lhsv: list_hsval): ?? hsval :=
   DO hv <~ hSop_hcodes op lhsv;;
   hC_hsval {| hdata:=HSop op lhsv unknown_hid; hcodes :=hv |}.

Lemma hSop_fSop_correct op lhsv:
  WHEN hSop op lhsv ~> hv THEN forall ge sp rs0 m0,
    seval_hsval ge sp hv rs0 m0 = seval_hsval ge sp (fSop op lhsv) rs0 m0.
Proof.
  wlp_simplify.
Qed.
Global Opaque hSop.
Local Hint Resolve hSop_fSop_correct: wlp_raw.

Lemma hSop_correct op lhsv:
  WHEN hSop op lhsv ~> hv THEN forall ge sp rs0 m0 lsv sm m
   (MEM: seval_smem ge sp sm rs0 m0 = Some m)
   (MVALID: forall b ofs, Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs)
   (LR: list_sval_refines ge sp rs0 m0 lhsv lsv),
   sval_refines ge sp rs0 m0 hv (Sop op lsv sm).
Proof.
  generalize fSop_correct; simpl.
  intros X.
  wlp_xsimplify ltac:(intuition eauto with wlp wlp_raw).
  erewrite H, X; eauto.
Qed.
Local Hint Resolve hSop_correct: wlp.

Definition hSload_hcodes (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval):=
   DO hc <~ hash load_hcode;;
   DO hv1 <~ hash trap;;
   DO hv2 <~ hash chunk;;
   DO hv3 <~ hash addr;;
   RET [hc; hsmem_get_hid hsm; hv1; hv2; hv3; list_hsval_get_hid lhsv].
Extraction Inline hSload_hcodes.

Definition hSload (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval): ?? hsval :=
   DO hv <~ hSload_hcodes hsm trap chunk addr lhsv;;
   hC_hsval {| hdata := HSload hsm trap chunk addr lhsv unknown_hid; hcodes := hv |}.

Lemma hSload_correct hsm trap chunk addr lhsv:
  WHEN hSload hsm trap chunk addr lhsv ~> hv THEN forall ge sp rs0 m0 lsv sm
    (LR: list_sval_refines ge sp rs0 m0 lhsv lsv)
    (MR: smem_refines ge sp rs0 m0 hsm sm),
    sval_refines ge sp rs0 m0 hv (Sload sm trap chunk addr lsv).
Proof.
  wlp_simplify.
  rewrite <- LR, <- MR.
  auto.
Qed.
Global Opaque hSload.
Local Hint Resolve hSload_correct: wlp.

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

Lemma hSnil_correct:
  WHEN hSnil() ~> hv THEN forall ge sp rs0 m0,
    list_sval_refines ge sp rs0 m0 hv Snil.
Proof.
  wlp_simplify.
Qed.
Global Opaque hSnil.
Local Hint Resolve hSnil_correct: wlp.

Definition hScons (hsv: hsval) (lhsv: list_hsval): ?? list_hsval :=
   hC_list_hsval {| hdata := HScons hsv lhsv unknown_hid; hcodes := [hsval_get_hid hsv; list_hsval_get_hid lhsv] |}.

Lemma hScons_correct hsv lhsv:
  WHEN hScons hsv lhsv ~> lhsv' THEN forall ge sp rs0 m0 sv lsv
    (VR: sval_refines ge sp rs0 m0 hsv sv)
    (LR: list_sval_refines ge sp rs0 m0 lhsv lsv),
    list_sval_refines ge sp rs0 m0 lhsv' (Scons sv lsv).
Proof.
  wlp_simplify.
  rewrite <- VR, <- LR.
  auto.
Qed.
Global Opaque hScons.
Local Hint Resolve hScons_correct: wlp.

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

Lemma hSinit_correct:
  WHEN hSinit() ~> hm THEN forall ge sp rs0 m0,
    smem_refines ge sp rs0 m0 hm Sinit.
Proof.
  wlp_simplify.
Qed.
Global Opaque hSinit.
Local Hint Resolve hSinit_correct: wlp.

Definition hSstore_hcodes (hsm: hsmem) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval) (srce: hsval):=
   DO hv1 <~ hash chunk;;
   DO hv2 <~ hash addr;;
   RET [hsmem_get_hid hsm; hv1; hv2; list_hsval_get_hid lhsv; hsval_get_hid srce].
Extraction Inline hSstore_hcodes.

Definition hSstore (hsm: hsmem) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval) (srce: hsval): ?? hsmem :=
   DO hv <~ hSstore_hcodes hsm chunk addr lhsv srce;;
   hC_hsmem {| hdata := HSstore hsm chunk addr lhsv srce unknown_hid; hcodes := hv |}.

Lemma hSstore_correct hsm chunk addr lhsv hsv:
  WHEN hSstore hsm chunk addr lhsv hsv ~> hsm' THEN forall ge sp rs0 m0 lsv sm sv
    (LR: list_sval_refines ge sp rs0 m0 lhsv lsv)
    (MR: smem_refines ge sp rs0 m0 hsm sm)
    (VR: sval_refines ge sp rs0 m0 hsv sv),
    smem_refines ge sp rs0 m0 hsm' (Sstore sm chunk addr lsv sv).
Proof.
  wlp_simplify.
  rewrite <- LR, <- MR, <- VR.
  auto.
Qed.
Global Opaque hSstore.
Local Hint Resolve hSstore_correct: wlp.

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

Lemma hsi_sreg_get_correct hst r:
  WHEN hsi_sreg_get hst r ~> hsv THEN forall ge sp rs0 m0 (f: reg -> sval)
    (RR: forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (f r) rs0 m0),
    sval_refines ge sp rs0 m0 hsv (f r).
Proof.
  unfold hsi_sreg_eval, hsi_sreg_proj; wlp_simplify; rewrite <- RR; try_simplify_someHyps.
Qed.
Global Opaque hsi_sreg_get.
Local Hint Resolve hsi_sreg_get_correct: wlp.

Fixpoint hlist_args (hst: PTree.t hsval) (l: list reg): ?? list_hsval :=
  match l with
  | nil => hSnil()
  | r::l =>
    DO v <~ hsi_sreg_get hst r;;
    DO lhsv <~ hlist_args hst l;;
    hScons v lhsv
  end.

Lemma hlist_args_correct hst l:
  WHEN hlist_args hst l ~> lhsv THEN forall ge sp rs0 m0 (f: reg -> sval)
    (RR: forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (f r) rs0 m0),
    list_sval_refines ge sp rs0 m0 lhsv (list_sval_inj (List.map f l)).
Proof.
  induction l; wlp_simplify.
Qed.
Global Opaque hlist_args.
Local Hint Resolve hlist_args_correct: wlp.

(** Convert a "fake" hash-consed term into a "real" hash-consed term *)

Fixpoint fsval_proj hsv: ?? hsval :=
  match hsv with
  | HSinput r hc => 
    DO b <~ phys_eq hc unknown_hid;;
    if b 
    then hSinput r (* was not yet really hash-consed *)
    else RET hsv (* already hash-consed *)
  | HSop op hl hc => 
    DO b <~ phys_eq hc unknown_hid;;
    if b 
    then (* was not yet really hash-consed *) 
      DO hl' <~ fsval_list_proj hl;;
      hSop op hl'
    else RET hsv (* already hash-consed *)
  | HSload hm t chk addr hl _ => RET hsv (* FIXME ? *)
  end
with fsval_list_proj hsl: ?? list_hsval :=
  match hsl with
  | HSnil hc => 
    DO b <~ phys_eq hc unknown_hid;;
    if b 
    then hSnil() (* was not yet really hash-consed *)
    else RET hsl (* already hash-consed *)
  | HScons hv hl hc => 
    DO b <~ phys_eq hc unknown_hid;;
    if b 
    then (* was not yet really hash-consed *)
      DO hv' <~ fsval_proj hv;;
      DO hl' <~ fsval_list_proj hl;;
      hScons hv' hl' 
    else RET hsl (* already hash-consed *)
  end.

Lemma fsval_proj_correct hsv:
  WHEN fsval_proj hsv ~> hsv' THEN forall ge sp rs0 m0,
  seval_hsval ge sp hsv rs0 m0 = seval_hsval ge sp hsv' rs0 m0.
Proof.
 induction hsv using hsval_mut 
 with (P0 := fun lhsv => 
       WHEN fsval_list_proj lhsv ~> lhsv' THEN forall ge sp rs0 m0,
         seval_list_hsval ge sp lhsv rs0 m0 = seval_list_hsval ge sp lhsv' rs0 m0)
       (P1 := fun sm => True); try (wlp_simplify; tauto).
 - wlp_xsimplify ltac:(intuition eauto with wlp_raw wlp).
   rewrite H, H0; auto.
 - wlp_simplify; erewrite H0, H1; eauto.
Qed.
Global Opaque fsval_proj.
Local Hint Resolve fsval_proj_correct: wlp.

Lemma fsval_list_proj_correct lhsv:
  WHEN fsval_list_proj lhsv ~> lhsv' THEN forall ge sp rs0 m0,
  seval_list_hsval ge sp lhsv rs0 m0 = seval_list_hsval ge sp lhsv' rs0 m0.
Proof.
  induction lhsv; wlp_simplify.
  erewrite H0, H1; eauto.
Qed.
Global Opaque fsval_list_proj.
Local Hint Resolve fsval_list_proj_correct: wlp.


(** ** Assignment of memory *)
Definition hslocal_set_smem (hst:hsistate_local) hm :=
  {| hsi_smem := hm;
     hsi_ok_lsval := hsi_ok_lsval hst;
     hsi_sreg:= hsi_sreg hst
  |}.

Lemma sok_local_set_mem ge sp rs0 m0 st sm:
  sok_local ge sp rs0 m0 (slocal_set_smem st sm)
  <-> (sok_local ge sp rs0 m0 st /\ seval_smem ge sp sm rs0 m0 <> None).
Proof.
  unfold slocal_set_smem, sok_local; simpl; intuition (subst; eauto).
Qed.

Lemma hsok_local_set_mem ge sp rs0 m0 hst hsm:
  (seval_hsmem ge sp (hsi_smem hst) rs0 m0 = None -> seval_hsmem ge sp hsm rs0 m0 = None) ->
  hsok_local ge sp rs0 m0 (hslocal_set_smem hst hsm)
  <-> (hsok_local ge sp rs0 m0 hst /\ seval_hsmem ge sp hsm rs0 m0 <> None).
Proof.
  unfold hslocal_set_smem, hsok_local; simpl; intuition.
Qed.

Lemma hslocal_set_mem_correct ge sp rs0 m0 hst st hsm sm:
  (seval_hsmem ge sp (hsi_smem hst) rs0 m0 = None -> seval_hsmem ge sp hsm rs0 m0 = None) ->
  (forall m b ofs, seval_smem ge sp sm rs0 m0 = Some m -> Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs) ->
  hsilocal_refines ge sp rs0 m0 hst st ->
  (hsok_local ge sp rs0 m0 hst -> smem_refines ge sp rs0 m0 hsm sm) ->
  hsilocal_refines ge sp rs0 m0 (hslocal_set_smem hst hsm) (slocal_set_smem st sm).
Proof.
  intros PRESERV SMVALID (OKEQ & SMEMEQ' & REGEQ & MVALID) SMEMEQ.
  split; rewrite! hsok_local_set_mem; simpl; eauto; try tauto.
  rewrite sok_local_set_mem.
  intuition congruence.
Qed.

Definition hslocal_store (hst: hsistate_local) chunk addr args src: ?? hsistate_local :=
   let pt := hst.(hsi_sreg) in
   DO hargs <~ hlist_args pt args;;
   DO hsrc <~ hsi_sreg_get pt src;;
   DO hm <~ hSstore hst chunk addr hargs hsrc;;
   RET (hslocal_set_smem hst hm).

Lemma hslocal_store_correct hst chunk addr args src:
  WHEN hslocal_store hst chunk addr args src ~> hst' THEN forall ge sp rs0 m0 st
    (REF: hsilocal_refines ge sp rs0 m0 hst st),
    hsilocal_refines ge sp rs0 m0 hst' (slocal_store st chunk addr args src).
Proof.
  wlp_simplify.
  eapply hslocal_set_mem_correct; simpl; eauto.
  + intros X; erewrite H1; eauto.
    rewrite X. simplify_SOME z.
  + unfold hsilocal_refines in *; 
    simplify_SOME z; intuition. 
    erewrite <- Mem.storev_preserv_valid; [| eauto].
    eauto.
  + unfold hsilocal_refines in *; intuition eauto.
Qed.
Global Opaque hslocal_store.
Local Hint Resolve hslocal_store_correct: wlp.

(** ** Assignment of local state *)

Definition hsist_set_local (hst: hsistate) (pc: node) (hnxt: hsistate_local): hsistate :=
   {| hsi_pc := pc; hsi_exits := hst.(hsi_exits); hsi_local:= hnxt |}.

Lemma hsist_set_local_correct_stat hst st pc hnxt nxt:
  hsistate_refines_stat hst st ->
  hsistate_refines_stat (hsist_set_local hst pc hnxt) (sist_set_local st pc nxt).
Proof.
  unfold hsistate_refines_stat; simpl; intuition.
Qed.

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

(** ** Assignment of registers *)

(** locally new symbolic values during symbolic execution *)
Inductive root_sval: Type :=
| Rop (op: operation)
| Rload (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing)
.

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

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

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

Local Open Scope lazy_bool_scope.

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

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

Lemma seval_list_sval_length ge sp rs0 m0 (f: reg -> sval) (l:list reg):
  forall l', seval_list_sval ge sp (list_sval_inj (List.map f l)) rs0 m0 = Some l' ->
  Datatypes.length l = Datatypes.length l'.
Proof.
  induction l.
  - simpl. intros. inv H. reflexivity.
  - simpl. intros. destruct (seval_sval _ _ _ _ _); [|discriminate].
    destruct (seval_list_sval _ _ _ _ _) eqn:SLS; [|discriminate]. inv H. simpl.
    erewrite IHl; eauto.
Qed.

Lemma may_trap_correct (ge: RTL.genv) (sp:val) (rsv: root_sval) (rs0: regset) (m0: mem) (lr: list reg) st:
  may_trap rsv lr = false -> 
  seval_list_sval ge sp (list_sval_inj (List.map (si_sreg st) lr)) rs0 m0 <> None ->
  seval_smem ge sp (si_smem st) rs0 m0 <> None ->
  seval_sval ge sp (rsv lr st) rs0 m0 <> None.
Proof.
  destruct rsv; simpl; try congruence.
  - rewrite lazy_orb_negb_false. intros (TRAP1 & TRAP2) OK1 OK2.
    explore; try congruence.
    eapply is_trapping_op_sound; eauto.
    erewrite <- seval_list_sval_length; eauto.
    apply Nat.eqb_eq in TRAP2.
    assumption.
  - intros X OK1 OK2.
    explore; try congruence.
Qed.

(** simplify a symbolic value before assignment to a register *)
Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hsval :=
  match rsv with
  | Rop op =>
     match is_move_operation op lr with
     | Some arg => hsi_sreg_get hst arg (* optimization of Omove *)
     | None =>
       match target_op_simplify op lr hst with
       | Some fhv => fsval_proj fhv
       | None =>
         DO lhsv <~ hlist_args hst lr;;
         hSop op lhsv
       end
     end
  | Rload _ chunk addr => 
       DO lhsv <~ hlist_args hst lr;;
       hSload hst NOTRAP chunk addr lhsv
  end.

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

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

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

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

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

Definition hslocal_set_sreg (hst: hsistate_local) (r: reg) (rsv: root_sval) (lr: list reg): ?? hsistate_local :=
  DO ok_lhsv <~
   (if may_trap rsv lr
    then DO hv <~ root_happly rsv lr hst;;
         XDEBUG hv (fun hv => DO hv_name <~ string_of_hashcode (hsval_get_hid hv);; RET ("-- insert undef behavior of hashcode:" +; (CamlStr hv_name))%string);;
         RET (hv::(hsi_ok_lsval hst))
    else RET (hsi_ok_lsval hst));;
  DO simp <~ simplify rsv lr hst;;
  RET {| hsi_smem := hst;
         hsi_ok_lsval := ok_lhsv;
         hsi_sreg := red_PTree_set r simp (hsi_sreg hst) |}.

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

(** ** Execution of one instruction *)

(* TODO gourdinl
 * This is just useful for debugging fake values hashcode projection *)
Fixpoint check_no_uhid lhsv :=
  match lhsv with
  | HSnil hc =>
      DO b <~ phys_eq hc unknown_hid;;
      assert_b (negb b) "fail no uhid";;
      RET tt
  | HScons hsv lhsv' hc =>
      DO b <~ phys_eq hc unknown_hid;;
      assert_b (negb b) "fail no uhid";;
      check_no_uhid lhsv'
  end.

Definition cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list reg): ?? (condition * list_hsval) :=
    match target_cbranch_expanse prev cond args with
    | Some (cond', vargs) => 
      DO vargs' <~ fsval_list_proj vargs;;
      RET (cond', vargs')
    | None =>
      DO vargs <~ hlist_args prev args ;;
      RET (cond, vargs)
    end.

Lemma cbranch_expanse_correct hst c l:
 WHEN cbranch_expanse hst c l ~> r THEN forall ge sp rs0 m0 st
  (LREF : hsilocal_refines ge sp rs0 m0 hst st)
  (OK: hsok_local ge sp rs0 m0 hst),
  seval_condition ge sp (fst r) (hsval_list_proj (snd r)) (si_smem st) rs0 m0 =
  seval_condition ge sp c (list_sval_inj (map (si_sreg st) l)) (si_smem st) rs0 m0.
Proof.
  unfold cbranch_expanse.
  destruct (target_cbranch_expanse _ _ _) eqn: TARGET; wlp_simplify;
  unfold seval_condition; erewrite <- H; eauto.
  destruct p as [c' l']; simpl.
  exploit target_cbranch_expanse_correct; eauto.
Qed.
Local Hint Resolve cbranch_expanse_correct: wlp.
Global Opaque cbranch_expanse.

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 res <~ cbranch_expanse prev cond args;;
      let (cond, vargs) := res in
      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
  end.

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

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

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

Local Hint Resolve hsist_set_local_correct_stat: core.

Lemma hsiexec_cond_noexp (hst: hsistate): forall l c0 n n0,
  WHEN DO res <~
       (DO vargs <~ hlist_args (hsi_local hst) l;; RET ((c0, vargs)));;
       (let (cond, vargs) := res in
        RET (Some
               {|
               hsi_pc := n0;
               hsi_exits := {|
                            hsi_cond := cond;
                            hsi_scondargs := vargs;
                            hsi_elocal := hsi_local hst;
                            hsi_ifso := n |} :: hsi_exits hst;
               hsi_local := hsi_local hst |})) ~> o0
  THEN (forall (hst' : hsistate) (st : sistate),
        o0 = Some hst' ->
        exists st' : sistate,
          Some
            {|
            si_pc := n0;
            si_exits := {|
                        si_cond := c0;
                        si_scondargs := list_sval_inj
                                          (map (si_sreg (si_local st)) l);
                        si_elocal := si_local st;
                        si_ifso := n |} :: si_exits st;
            si_local := si_local st |} = Some st' /\
          (hsistate_refines_stat hst st -> hsistate_refines_stat hst' st') /\
          (forall (ge : RTL.genv) (sp : val) (rs0 : regset) (m0 : mem),
           hsistate_refines_dyn ge sp rs0 m0 hst st ->
           hsistate_refines_dyn ge sp rs0 m0 hst' st')).
Proof.
  intros.
  wlp_simplify; try_simplify_someHyps; eexists; intuition eauto.
  - unfold hsistate_refines_stat, hsiexits_refines_stat in *; simpl; intuition.
    constructor; simpl; eauto.
    constructor.
  - destruct H0 as (EXREF & LREF & NEST).
    split.
    + constructor; simpl; auto.
      constructor; simpl; auto.
      intros; erewrite seval_condition_refines; eauto.
    + split; simpl; auto.
      destruct NEST as [|st0 se lse TOP NEST];
      econstructor; simpl; auto; constructor; auto.
Qed.

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


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

Fixpoint hsiexec_path (path:nat) (f: function) (hst: hsistate): ?? hsistate :=
  match path with
  | O => RET hst
  | S p =>
    let pc := hst.(hsi_pc) in
    XDEBUG pc (fun pc => DO name_pc <~ string_of_Z (Zpos pc);; RET ("- sym exec node: " +; name_pc)%string);;
    DO i <~ some_or_fail ((fn_code f)!pc) "hsiexec_path.internal_error.1";;
    DO ohst1 <~ hsiexec_inst i hst;;
    DO hst1 <~ some_or_fail ohst1 "hsiexec_path.internal_error.2";;
    hsiexec_path p f hst1
  end.

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

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

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

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

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

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

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

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

Lemma hsexec_final_correct (hsl: hsistate_local) i:
  WHEN hsexec_final i hsl ~> hsf THEN forall ge sp rs0 m0 sl
   (OK:  hsok_local ge sp rs0 m0 hsl)
   (REF: hsilocal_refines ge sp rs0 m0 hsl sl),
   hfinal_refines ge sp rs0 m0 hsf (sexec_final i sl).
Proof.
  destruct i; wlp_simplify; try econstructor; simpl; eauto.
Qed.
Global Opaque hsexec_final.
Local Hint Resolve hsexec_final_correct: wlp.

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

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

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

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

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

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

Global Opaque hsexec.

End CanonBuilding.

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

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

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

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

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

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

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

Import PTree.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


Fixpoint revmap_check_list (dm: PTree.t node) (ln ln': list node): ?? unit :=
  match ln, ln' with
  | nil, nil => RET tt
  | n::ln, n'::ln' => 
      revmap_check_single dm n n';;
      revmap_check_list dm ln ln'
  | _, _ => FAILWITH "revmap_check_list: lists have different lengths"
  end.

Lemma revmap_check_list_correct dm: forall lpc lpc',
  WHEN revmap_check_list dm lpc lpc' ~> _ THEN
  ptree_get_list dm lpc' = Some lpc.
Proof.
  induction lpc.
  - destruct lpc'; wlp_simplify.
  - destruct lpc'; wlp_simplify. try_simplify_someHyps.
Qed.
Global Opaque revmap_check_list.
Hint Resolve revmap_check_list_correct: wlp.


Definition svos_simu_check (svos1 svos2: hsval + ident) :=
  match svos1, svos2 with
  | inl sv1, inl sv2 => phys_check sv1 sv2 "svos_simu_check: sval mismatch"
  | inr id1, inr id2 => phys_check id1 id2 "svos_simu_check: symbol mismatch"
  | _, _ => FAILWITH "svos_simu_check: type mismatch"
  end.

Lemma svos_simu_check_correct svos1 svos2:
  WHEN svos_simu_check svos1 svos2 ~> _ THEN
  svos1 = svos2.
Proof.
  destruct svos1; destruct svos2; wlp_simplify.
Qed.
Global Opaque svos_simu_check.
Hint Resolve svos_simu_check_correct: wlp.


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

Lemma builtin_arg_simu_check_correct: forall bs1 bs2,
  WHEN builtin_arg_simu_check bs1 bs2 ~> _ THEN
  builtin_arg_map hsval_proj bs1 = builtin_arg_map hsval_proj bs2.
Proof.
  induction bs1.
  all: try (wlp_simplify; subst; reflexivity).
  all: destruct bs2; wlp_simplify; congruence.
Qed.
Global Opaque builtin_arg_simu_check.
Hint Resolve builtin_arg_simu_check_correct: wlp.

Fixpoint list_builtin_arg_simu_check lbs1 lbs2 :=
  match lbs1, lbs2 with
  | nil, nil => RET tt
  | bs1::lbs1, bs2::lbs2 =>
    builtin_arg_simu_check bs1 bs2;;
    list_builtin_arg_simu_check lbs1 lbs2
  | _, _ => FAILWITH "list_builtin_arg_simu_check: length mismatch"
  end.

Lemma list_builtin_arg_simu_check_correct: forall lbs1 lbs2,
  WHEN list_builtin_arg_simu_check lbs1 lbs2 ~> _ THEN
  List.map (builtin_arg_map hsval_proj) lbs1 = List.map (builtin_arg_map hsval_proj) lbs2.
Proof.
  induction lbs1; destruct lbs2; wlp_simplify. congruence.
Qed.
Global Opaque list_builtin_arg_simu_check.
Hint Resolve list_builtin_arg_simu_check_correct: wlp.

Definition sfval_simu_check (dm: PTree.t node) (f: RTLpath.function) (pc1 pc2: node) (fv1 fv2: hsfval) :=
  match fv1, fv2 with
  | HSnone, HSnone => revmap_check_single dm pc1 pc2
  | HScall sig1 svos1 lsv1 res1 pc1, HScall sig2 svos2 lsv2 res2 pc2 =>
      revmap_check_single dm pc1 pc2;;
      phys_check sig1 sig2 "sfval_simu_check: Scall different signatures";;
      phys_check res1 res2 "sfval_simu_check: Scall res do not match";;
      svos_simu_check svos1 svos2;;
      phys_check lsv1 lsv2 "sfval_simu_check: Scall args do not match"
  | HStailcall sig1 svos1 lsv1, HStailcall sig2 svos2 lsv2 =>
      phys_check sig1 sig2 "sfval_simu_check: Stailcall different signatures";;
      svos_simu_check svos1 svos2;;
      phys_check lsv1 lsv2 "sfval_simu_check: Stailcall args do not match"
  | HSbuiltin ef1 lbs1 br1 pc1, HSbuiltin ef2 lbs2 br2 pc2 =>
      revmap_check_single dm pc1 pc2;;
      phys_check ef1 ef2 "sfval_simu_check: builtin ef do not match";;
      phys_check br1 br2 "sfval_simu_check: builtin br do not match";;
      list_builtin_arg_simu_check lbs1 lbs2
  | HSjumptable sv ln, HSjumptable sv' ln' =>
      revmap_check_list dm ln ln';;
      phys_check sv sv' "sfval_simu_check: Sjumptable sval do not match"
  | HSreturn osv1, HSreturn osv2 =>
      option_eq_check osv1 osv2
  | _, _ => FAILWITH "sfval_simu_check: structure mismatch"
  end.

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

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

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

Definition simu_check_single (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) (m: node * node): ?? unit :=
  let (pc2, pc1) := m in
  (* creating the hash-consing tables *)
  DO hC_sval <~ hCons hSVAL;;
  DO hC_list_hsval <~ hCons hLSVAL;;
  DO hC_hsmem <~ hCons hSMEM;;
  let hsexec := hsexec hC_sval.(hC) hC_list_hsval.(hC) hC_hsmem.(hC) in
  (* performing the hash-consed executions *)
  XDEBUG pc1 (fun pc => DO name_pc <~ string_of_Z (Zpos pc);; RET ("entry-point of input superblock: " +; name_pc)%string);;
  DO hst1 <~ hsexec f pc1;;
  XDEBUG pc2 (fun pc => DO name_pc <~ string_of_Z (Zpos pc);; RET ("entry-point of output superblock: " +; name_pc)%string);;
  DO hst2 <~ hsexec tf pc2;;
  DO path <~ some_or_fail ((fn_path f)!pc1) "simu_check_single.internal_error.1";;
  let outframe := path.(pre_output_regs) in
  (* comparing the executions *)
  hsstate_simu_check dm f outframe hst1 hst2.

Lemma simu_check_single_correct dm tf f pc1 pc2:
  WHEN simu_check_single dm f tf (pc2, pc1) ~> _ THEN
  sexec_simu dm f tf pc1 pc2.
Proof.
  unfold sexec_simu; wlp_simplify.
  exploit H2; clear H2. 1-3: wlp_simplify.
  intros (st2 & SEXEC2 & REF2). try_simplify_someHyps.
  exploit H3; clear H3. 1-3: wlp_simplify.
  intros (st3 & SEXEC3 & REF3). try_simplify_someHyps.
  eexists. eexists. split; eauto. split; eauto.
  intros ctx.
  eapply hsstate_simu_spec_correct; eauto.
Qed.
Global Opaque simu_check_single.
Global Hint Resolve simu_check_single_correct: wlp.

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

Lemma simu_check_rec_correct dm f tf lm:
  WHEN simu_check_rec dm f tf lm ~> _ THEN
  forall pc1 pc2, In (pc2, pc1) lm -> sexec_simu dm f tf pc1 pc2.
Proof.
  induction lm; wlp_simplify.
  match goal with
  | X: (_,_) = (_,_) |- _ => inversion X; subst
  end.
  subst; eauto.
Qed.
Global Opaque simu_check_rec.
Global Hint Resolve simu_check_rec_correct: wlp.

Definition imp_simu_check (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function): ?? unit :=
   simu_check_rec dm f tf (PTree.elements dm);;
   DEBUG("simu_check OK!").

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

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

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

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

Import UnsafeImpure.

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

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