Module RTLpathSE_impl

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.

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
  | HSop op1 lsv1 _, HSop op2 lsv2 _ =>
     DO b1 <~ phys_eq lsv1 lsv2;;
     if b1
     then struct_eq op1 op2
     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.


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
    else RET hsv
  | HSop op hl hc =>
    DO b <~ phys_eq hc unknown_hid;;
    if b
    then
      DO hl' <~ fsval_list_proj hl;;
      hSop op hl'
    else RET hsv
  | HSload hm t chk addr hl _ => RET hsv
  end
with fsval_list_proj hsl: ?? list_hsval :=
  match hsl with
  | HSnil hc =>
    DO b <~ phys_eq hc unknown_hid;;
    if b
    then hSnil()
    else RET hsl
  | HScons hv hl hc =>
    DO b <~ phys_eq hc unknown_hid;;
    if b
    then
      DO hv' <~ fsval_proj hv;;
      DO hl' <~ fsval_list_proj hl;;
      hScons hv' hl'
    else RET hsl
  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.

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


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


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.