Require Import Coqlib AST Maps.
Require Import Op Registers.
Require Import RTL BTL Errors.
Require Import BTL_SEsimuref BTL_SEtheory OptionMonad.
Require Import BTL_SEsimplify.

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

Local Open Scope option_monad_scope.
Local Open Scope impure.

Import ListNotations.
Local Open Scope list_scope.

(** Notations to make lemmas more readable *)
Notation "'sval_refines' ctx sv1 sv2" := (eval_sval ctx sv1 = eval_sval ctx sv2)
  (only parsing, at level 0, ctx at next level, sv1 at next level, sv2 at next level): hse.

Local Open Scope hse.

Notation "'list_sval_refines' ctx lsv1 lsv2" := (eval_list_sval ctx lsv1 = eval_list_sval ctx lsv2)
  (only parsing, at level 0, ctx at next level, lsv1 at next level, lsv2 at next level): hse.

Notation "'smem_refines' ctx sm1 sm2" := (eval_smem ctx sm1 = eval_smem ctx sm2)
  (only parsing, at level 0, ctx at next level, sm1 at next level, sm2 at next level): hse.

(** Debug printer *)
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 sval_get_hid (sv: sval): hashcode :=
  match sv with
  | Sundef hid => hid
  | Sinput _ hid => hid
  | Sop _ _ hid => hid
  | Sload _ _ _ _ _ hid => hid
  end.

Definition list_sval_get_hid (lsv: list_sval): hashcode :=
  match lsv with
  | Snil hid => hid
  | Scons _ _ hid => hid
  end.

Definition smem_get_hid (sm: smem): hashcode :=
  match sm with
  | Sinit hid => hid
  | Sstore _ _ _ _ _ hid => hid
  end.

Definition sval_set_hid (sv: sval) (hid: hashcode): sval :=
  match sv with
  | Sundef _ => Sundef hid
  | Sinput r _ => Sinput r hid
  | Sop o lsv _ => Sop o lsv hid
  | Sload sm trap chunk addr lsv _ => Sload sm trap chunk addr lsv hid
  end.

Definition list_sval_set_hid (lsv: list_sval) (hid: hashcode): list_sval :=
  match lsv with
  | Snil _ => Snil hid
  | Scons sv lsv _ => Scons sv lsv hid
  end.

Definition smem_set_hid (sm: smem) (hid: hashcode): smem :=
  match sm with
  | Sinit _ => Sinit hid
  | Sstore sm chunk addr lsv srce _ => Sstore sm chunk addr lsv srce hid
  end.

Lemma sval_set_hid_correct ctx x y:
  sval_set_hid x unknown_hid = sval_set_hid y unknown_hid ->
  sval_refines ctx x y.
Proof.
  destruct x, y; intro H; inversion H; subst; simpl; auto.
Qed.
Local Hint Resolve sval_set_hid_correct: core.

Lemma list_sval_set_hid_correct ctx x y:
  list_sval_set_hid x unknown_hid = list_sval_set_hid y unknown_hid ->
  list_sval_refines ctx x y.
Proof.
  destruct x, y; intro H; inversion H; subst; simpl; auto.
Qed.
Local Hint Resolve list_sval_set_hid_correct: core.

Lemma smem_set_hid_correct ctx x y:
  smem_set_hid x unknown_hid = smem_set_hid y unknown_hid ->
  smem_refines ctx x y.
Proof.
  destruct x, y; intro H; inversion H; subst; simpl; auto.
Qed.
Local Hint Resolve smem_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 sval_hash_eq (sv1 sv2: sval): ?? bool :=
  match sv1, sv2 with
  | Sinput r1 _, Sinput r2 _ => struct_eq r1 r2 (* NB: really need a struct_eq here ? *)
  | Sop op1 lsv1 _, Sop 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
  | Sload sm1 trap1 chk1 addr1 lsv1 _, Sload 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 sval_hash_eq_correct x y:
  WHEN sval_hash_eq x y ~> b THEN 
   b = true -> sval_set_hid x unknown_hid = sval_set_hid y unknown_hid.
Proof.
  destruct x, y; wlp_simplify; try (rewrite !and_true_split in *); intuition; subst; try congruence.
Qed.
Global Opaque sval_hash_eq.
Local Hint Resolve sval_hash_eq_correct: wlp.

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

Lemma list_sval_hash_eq_correct x y:
  WHEN list_sval_hash_eq x y ~> b THEN 
   b = true -> list_sval_set_hid x unknown_hid = list_sval_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_sval_hash_eq.
Local Hint Resolve list_sval_hash_eq_correct: wlp.

Definition smem_hash_eq (sm1 sm2: smem): ?? bool :=
  match sm1, sm2 with
  | Sinit _, Sinit _ => RET true
  | Sstore sm1 chk1 addr1 lsv1 sv1 _, Sstore 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 smem_hash_eq_correct x y:
  WHEN smem_hash_eq x y ~> b THEN 
   b = true -> smem_set_hid x unknown_hid = smem_set_hid y unknown_hid.
Proof.
  destruct x, y; wlp_simplify; try (rewrite !and_true_split in *); intuition; subst; try congruence.
Qed.
Global Opaque smem_hash_eq.
Local Hint Resolve smem_hash_eq_correct: wlp.

Definition hSVAL: hashP sval := {| hash_eq := sval_hash_eq; get_hid:=sval_get_hid; set_hid:=sval_set_hid |}. 
Definition hLSVAL: hashP list_sval := {| hash_eq := list_sval_hash_eq; get_hid:= list_sval_get_hid; set_hid:= list_sval_set_hid |}.
Definition hSMEM: hashP smem := {| hash_eq := smem_hash_eq; get_hid:= smem_get_hid; set_hid:= smem_set_hid |}.

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

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

Variable hC_sval: hashinfo sval -> ?? sval.

Hypothesis hC_sval_correct: forall s,
  WHEN hC_sval s ~> s' THEN forall ctx,
    sval_refines ctx (hdata s) s'.

Variable hC_list_sval: hashinfo list_sval -> ?? list_sval.
Hypothesis hC_list_sval_correct: forall lh,
  WHEN hC_list_sval lh ~> lh' THEN forall ctx,
    list_sval_refines ctx (hdata lh) lh'.

Variable hC_smem: hashinfo smem -> ?? smem.
Hypothesis hC_smem_correct: forall hm,
  WHEN hC_smem hm ~> hm' THEN forall ctx,
    smem_refines ctx (hdata hm) hm'.

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

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

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

Definition hSinput (r:reg): ?? sval :=
   DO sv <~ hSinput_hcodes r;;
   hC_sval {| hdata:=Sinput r unknown_hid; hcodes :=sv; |}.

Lemma hSinput_correct r:
  WHEN hSinput r ~> sv THEN forall ctx,
    sval_refines ctx sv (Sinput r unknown_hid).
Proof.
  wlp_simplify.
Qed.
Global Opaque hSinput.
Local Hint Resolve hSinput_correct: wlp.

Definition hSop_hcodes (op:operation) (lsv: list_sval) :=
   DO hc <~ hash op_hcode;;
   DO sv <~ hash op;;
   RET [hc;sv;list_sval_get_hid lsv].
Extraction Inline hSop_hcodes.

Definition hSop (op:operation) (lsv: list_sval): ?? sval :=
   DO sv <~ hSop_hcodes op lsv;;
   hC_sval {| hdata:=Sop op lsv unknown_hid; hcodes :=sv |}.

Lemma hSop_fSop_correct op lsv:
  WHEN hSop op lsv ~> sv THEN forall ctx,
    sval_refines ctx sv (fSop op lsv).
Proof.
  wlp_simplify.
Qed.
Global Opaque hSop.
Local Hint Resolve hSop_fSop_correct: wlp_raw.

Lemma hSop_correct op lsv1:
  WHEN hSop op lsv1 ~> sv THEN forall ctx lsv2
   (LR: list_sval_refines ctx lsv1 lsv2),
   sval_refines ctx sv (Sop op lsv2 unknown_hid).
Proof.
  wlp_xsimplify ltac:(intuition eauto with wlp wlp_raw).
  rewrite <- LR. erewrite H; eauto.
Qed.
Local Hint Resolve hSop_correct: wlp.

Definition hSload_hcodes (sm: smem) (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (lsv: list_sval):=
   DO hc <~ hash load_hcode;;
   DO sv1 <~ hash trap;;
   DO sv2 <~ hash chunk;;
   DO sv3 <~ hash addr;;
   RET [hc; smem_get_hid sm; sv1; sv2; sv3; list_sval_get_hid lsv].
Extraction Inline hSload_hcodes.

Definition hSload (sm: smem) (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (lsv: list_sval): ?? sval :=
   DO sv <~ hSload_hcodes sm trap chunk addr lsv;;
   hC_sval {| hdata := Sload sm trap chunk addr lsv unknown_hid; hcodes := sv |}.

Lemma hSload_correct sm1 trap chunk addr lsv1:
  WHEN hSload sm1 trap chunk addr lsv1 ~> sv THEN forall ctx lsv2 sm2
    (LR: list_sval_refines ctx lsv1 lsv2)
    (MR: smem_refines ctx sm1 sm2),
    sval_refines ctx sv (Sload sm2 trap chunk addr lsv2 unknown_hid).
Proof.
  wlp_simplify.
  rewrite <- LR, <- MR.
  auto.
Qed.
Global Opaque hSload.
Local Hint Resolve hSload_correct: wlp.

Definition hSundef_hcodes :=
   DO hc <~ hash undef_code;;
   RET [hc].
Extraction Inline hSundef_hcodes.

Definition hSundef : ?? sval :=
   DO sv <~ hSundef_hcodes;;
   hC_sval {| hdata:=Sundef unknown_hid; hcodes :=sv; |}.

Lemma hSundef_correct:
  WHEN hSundef ~> sv THEN forall ctx,
    sval_refines ctx sv (Sundef unknown_hid).
Proof.
  wlp_simplify.
Qed.
Global Opaque hSundef.
Local Hint Resolve hSundef_correct: wlp.

Definition hSnil (_: unit): ?? list_sval :=
   hC_list_sval {| hdata := Snil unknown_hid; hcodes := nil |}.

Lemma hSnil_correct:
  WHEN hSnil() ~> sv THEN forall ctx,
    list_sval_refines ctx sv (Snil unknown_hid).
Proof.
  wlp_simplify.
Qed.
Global Opaque hSnil.
Local Hint Resolve hSnil_correct: wlp.

Definition hScons (sv: sval) (lsv: list_sval): ?? list_sval :=
   hC_list_sval {| hdata := Scons sv lsv unknown_hid; hcodes := [sval_get_hid sv; list_sval_get_hid lsv] |}.

Lemma hScons_correct sv1 lsv1:
  WHEN hScons sv1 lsv1 ~> lsv1' THEN forall ctx sv2 lsv2
    (VR: sval_refines ctx sv1 sv2)
    (LR: list_sval_refines ctx lsv1 lsv2),
    list_sval_refines ctx lsv1' (Scons sv2 lsv2 unknown_hid).
Proof.
  wlp_simplify.
  rewrite <- VR, <- LR.
  auto.
Qed.
Global Opaque hScons.
Local Hint Resolve hScons_correct: wlp.

Definition hSinit (_: unit): ?? smem :=
   hC_smem {| hdata := Sinit unknown_hid; hcodes := nil |}.

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

Definition hSstore_hcodes (sm: smem) (chunk: memory_chunk) (addr: addressing) (lsv: list_sval) (srce: sval):=
   DO sv1 <~ hash chunk;;
   DO sv2 <~ hash addr;;
   RET [smem_get_hid sm; sv1; sv2; list_sval_get_hid lsv; sval_get_hid srce].
Extraction Inline hSstore_hcodes.

Definition hSstore (sm: smem) (chunk: memory_chunk) (addr: addressing) (lsv: list_sval) (srce: sval): ?? smem :=
   DO sv <~ hSstore_hcodes sm chunk addr lsv srce;;
   hC_smem {| hdata := Sstore sm chunk addr lsv srce unknown_hid; hcodes := sv |}.

Lemma hSstore_correct sm1 chunk addr lsv1 sv1:
  WHEN hSstore sm1 chunk addr lsv1 sv1 ~> sm1' THEN forall ctx lsv2 sm2 sv2
    (LR: list_sval_refines ctx lsv1 lsv2)
    (MR: smem_refines ctx sm1 sm2)
    (VR: sval_refines ctx sv1 sv2),
    smem_refines ctx sm1' (Sstore sm2 chunk addr lsv2 sv2 unknown_hid).
Proof.
  wlp_simplify.
  rewrite <- LR, <- MR, <- VR.
  auto.
Qed.
Global Opaque hSstore.
Local Hint Resolve hSstore_correct: wlp.

Definition hrs_sreg_get (hrs: ristate) r: ?? sval :=
   match PTree.get r (ris_sreg hrs) with
   | None => if ris_input_init hrs then hSinput r else hSundef
   | Some sv => RET sv
   end.

Lemma hrs_sreg_get_correct hrs r:
  WHEN hrs_sreg_get hrs r ~> sv THEN forall ctx (f: reg -> sval)
  (RR: forall r, sval_refines ctx (hrs r) (f r)),
  sval_refines ctx sv (f r).
Proof.
  unfold ris_sreg_get; wlp_simplify; rewrite <- RR; rewrite H; auto;
  rewrite H0, H1; simpl; auto.
Qed.
Global Opaque hrs_sreg_get.
Local Hint Resolve hrs_sreg_get_correct: wlp.

Fixpoint hlist_args (hrs: ristate) (l: list reg): ?? list_sval :=
  match l with
  | nil => hSnil()
  | r::l =>
    DO v <~ hrs_sreg_get hrs r;;
    DO lsv <~ hlist_args hrs l;;
    hScons v lsv
  end.

Lemma hlist_args_correct hrs l:
  WHEN hlist_args hrs l ~> lsv THEN forall ctx (f: reg -> sval)
    (RR: forall r, sval_refines ctx (hrs r) (f r)),
    list_sval_refines ctx lsv (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 sv: ?? sval :=
  match sv with
  | Sundef hc =>
      DO b <~ phys_eq hc unknown_hid;;
      if b then hSundef else RET sv
  | Sinput r hc => 
      DO b <~ phys_eq hc unknown_hid;;
      if b then hSinput r (* was not yet really hash-consed *)
      else RET sv (* already hash-consed *)
  | Sop 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 sv (* already hash-consed *)
  | Sload hm t chk addr hl _ => RET sv (* FIXME TODO gourdinl ? *)
  end
with fsval_list_proj sl: ?? list_sval :=
  match sl with
  | Snil hc => 
      DO b <~ phys_eq hc unknown_hid;;
      if b then hSnil() (* was not yet really hash-consed *)
      else RET sl (* already hash-consed *)
  | Scons sv hl hc => 
      DO b <~ phys_eq hc unknown_hid;;
      if b then (* was not yet really hash-consed *)
        DO sv' <~ fsval_proj sv;;
        DO hl' <~ fsval_list_proj hl;;
        hScons sv' hl' 
      else RET sl (* already hash-consed *)
  end.

Lemma fsval_proj_correct sv:
  WHEN fsval_proj sv ~> sv' THEN forall ctx,
  sval_refines ctx sv sv'.
Proof.
 induction sv using sval_mut 
 with (P0 := fun lsv => 
       WHEN fsval_list_proj lsv ~> lsv' THEN forall ctx,
         eval_list_sval ctx lsv = eval_list_sval ctx lsv')
       (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 lsv:
  WHEN fsval_list_proj lsv ~> lsv' THEN forall ctx,
  list_sval_refines ctx lsv lsv'.
Proof.
  induction lsv; wlp_simplify.
  erewrite H0, H1; eauto.
Qed.
Global Opaque fsval_list_proj.
Local Hint Resolve fsval_list_proj_correct: wlp.

(** ** Assignment of memory *)

Definition hrexec_store chunk addr args src hrs: ?? ristate :=
  DO hargs <~ hlist_args hrs args;;
  DO hsrc <~ hrs_sreg_get hrs src;;
  DO hm <~ hSstore hrs chunk addr hargs hsrc;;
  RET (rset_smem hm hrs).

Lemma hrexec_store_correct chunk addr args src hrs:
  WHEN hrexec_store chunk addr args src hrs ~> hrs' THEN forall ctx sis
  (REF: ris_refines ctx hrs sis),
  ris_refines ctx hrs' (sexec_store chunk addr args src sis).
Proof.
  wlp_simplify.
  eapply rset_mem_correct; simpl; eauto.
  - intros X; erewrite H1; eauto.
    simplify_option.
  - intros X; inversion REF.
    erewrite H1; eauto.
Qed.
Local Hint Resolve hrexec_store_correct: wlp.

(** ** 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): sval :=
  let lsv := list_sval_inj (List.map (si_sreg st) lr) in
  let sm := si_smem st in
  match rsv with
  | Rop op => fSop op lsv
  | Rload trap chunk addr => fSload sm trap chunk addr lsv
  end.
Coercion root_apply: root_sval >-> Funclass.

Definition root_happly (rsv: root_sval) (lr: list reg) (hrs: ristate): ?? sval :=
  DO lsv <~ hlist_args hrs lr;;
  match rsv with
  | Rop op => hSop op lsv
  | Rload trap chunk addr => hSload hrs trap chunk addr lsv
  end.

Lemma root_happly_correct (rsv: root_sval) lr hrs:
  WHEN root_happly rsv lr hrs ~> sv THEN forall ctx sis
  (REF: ris_refines ctx hrs sis)
  (OK: ris_ok ctx hrs),
  sval_refines ctx sv (rsv lr sis).
Proof.
  unfold root_apply, root_happly; destruct rsv; wlp_simplify; inv REF;
  erewrite H0, H; eauto.
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. repeat autodestruct; simpl; intuition (try congruence).
Qed.

Lemma eval_list_sval_length ctx (f: reg -> sval) (l:list reg):
  forall l', eval_list_sval ctx (list_sval_inj (List.map f l)) = Some l' ->
  Datatypes.length l = Datatypes.length l'.
Proof.
  induction l.
  - simpl. intros. inv H. reflexivity.
  - simpl. intros. destruct (eval_sval _ _); [|discriminate].
    destruct (eval_list_sval _ _) eqn:SLS; [|discriminate]. inv H. simpl.
    erewrite IHl; eauto.
Qed.

Lemma may_trap_correct ctx (rsv: root_sval) (lr: list reg) st:
  may_trap rsv lr = false -> 
  eval_list_sval ctx (list_sval_inj (List.map (si_sreg st) lr)) <> None ->
  eval_smem ctx (si_smem st) <> None ->
  eval_sval ctx (rsv lr st) <> None.
Proof.
  destruct rsv; simpl; try congruence.
  - rewrite lazy_orb_negb_false. intros (TRAP1 & LEN) OK1 OK2.
    autodestruct; try congruence. intros.
    eapply is_trapping_op_sound; eauto.
    erewrite <- eval_list_sval_length; eauto.
    apply Nat.eqb_eq in LEN.
    assumption.
  - intros X OK1 OK2.
    repeat autodestruct; try congruence.
Qed.

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

Lemma simplify_correct rsv lr hrs:
  WHEN simplify rsv lr hrs ~> sv THEN forall ctx sis
    (REF: ris_refines ctx hrs sis)
    (OK0: ris_ok ctx hrs)
    (OK1: eval_sval ctx (rsv lr sis) <> None),
    sval_refines ctx sv (rsv lr sis).
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 *. inv REF.
      simplify_option. erewrite H; eauto. }
    destruct (target_op_simplify _ _ _) eqn: Htarget_op_simp; wlp_simplify.
    { destruct (eval_list_sval _ _) eqn: OKlist; try congruence.
      rewrite <- H; exploit target_op_simplify_correct; eauto. }
    inv REF; clear Htarget_op_simp.
    intuition eauto.
  - (* Rload *)
    destruct trap; wlp_simplify; inv REF.
    + erewrite H0; eauto.
      erewrite H; [|eapply REG_EQ; eauto].
      erewrite MEM_EQ; eauto.
      simplify_option.
    + erewrite H0; eauto.
Qed.
Global Opaque simplify.
Local Hint Resolve simplify_correct: wlp.

Definition red_PTree_set (r: reg) (sv: sval) (hrs: ristate): PTree.t sval :=
  match (ris_input_init hrs), sv with
  | true, Sinput r' _ =>
      if Pos.eq_dec r r' 
      then PTree.remove r' (ris_sreg hrs)
      else PTree.set r sv (ris_sreg hrs)
  | false, Sundef _ =>
      PTree.remove r (ris_sreg hrs)
  | _, _ => PTree.set r sv (ris_sreg hrs)
  end.

Lemma red_PTree_set_correct (r r0:reg) sv (hrs: ristate) ctx:
  sval_refines ctx ((ris_sreg_set hrs (red_PTree_set r sv hrs)) r0) ((ris_sreg_set hrs (PTree.set r sv (ris_sreg hrs))) r0).
Proof.
  unfold red_PTree_set, ris_sreg_set, ris_sreg_get; simpl.
  destruct (ris_input_init hrs) eqn:Hinit, sv; simpl; auto.
  1: destruct (Pos.eq_dec r r1); auto; subst;
     rename r1 into r.
  all: destruct (Pos.eq_dec r r0); 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) ctx hrs sis sv1 sv2:
 ris_refines ctx hrs sis ->
 sval_refines ctx sv1 sv2 ->
 ris_ok ctx hrs ->
 sval_refines ctx (ris_sreg_set hrs (red_PTree_set r sv1 hrs) r0) (if Pos.eq_dec r r0 then sv2 else si_sreg sis r0).
Proof.
  intros REF SREF OK; rewrite red_PTree_set_correct.
  unfold ris_sreg_set, ris_sreg_get.
  destruct (Pos.eq_dec r r0).
  - subst; simpl. rewrite PTree.gss; simpl; auto.
  - inv REF; simpl. rewrite PTree.gso; simpl; eauto.
Qed.

Definition cbranch_expanse (prev: ristate) (cond: condition) (args: list reg): ?? (condition * list_sval) :=
  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 hrs c l:
 WHEN cbranch_expanse hrs c l ~> r THEN forall ctx sis
  (REF : ris_refines ctx hrs sis)
  (OK: ris_ok ctx hrs),
  eval_scondition ctx (fst r) (snd r) =
  eval_scondition ctx c (list_sval_inj (map (si_sreg sis) l)).
Proof.
  unfold cbranch_expanse.
  destruct (target_cbranch_expanse _ _ _) eqn: TARGET; wlp_simplify;
  unfold eval_scondition; try erewrite <- H; inversion REF; 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 some_or_fail {A} (o: option A) (msg: pstring): ?? A :=
  match o with
  | Some x => RET x
  | None => FAILWITH msg
  end.

Definition hrs_init: ?? ristate
  := DO hm <~ hSinit ();;
     RET {| ris_smem := hm; ris_input_init := true; ok_rsval := nil; ris_sreg := PTree.empty _ |}.

Lemma hrs_init_correct:
  WHEN hrs_init ~> hrs THEN
  forall ctx, ris_refines ctx hrs sis_init.
Proof.
  unfold hrs_init, sis_init; wlp_simplify.
  econstructor; simpl in *; eauto.
  split; destruct 1; econstructor; simpl in *;
    try rewrite H; try congruence; trivial.
Qed.
Local Hint Resolve hrs_init_correct: wlp.
Global Opaque hrs_init.

Definition hrs_sreg_set r lr rsv (hrs: ristate): ?? ristate :=
  DO ok_lsv <~
    (if may_trap rsv lr
     then DO sv <~ root_happly rsv lr hrs;;
          XDEBUG sv (fun sv => DO sv_name <~ string_of_hashcode (sval_get_hid sv);; RET ("-- insert undef behavior of hashcode:" +; (CamlStr sv_name))%string);;
          RET (sv::(ok_rsval hrs))
     else RET (ok_rsval hrs));;
  DO simp <~ simplify rsv lr hrs;;
  RET {| ris_smem := hrs.(ris_smem);
         ris_input_init := hrs.(ris_input_init);
         ok_rsval := ok_lsv;
         ris_sreg:= red_PTree_set r simp hrs |}.

Lemma ok_hrset_sreg (rsv:root_sval) ctx (st: sistate) r lr:
  si_ok ctx (set_sreg r (rsv lr st) st)
  <-> (si_ok ctx st /\ eval_sval ctx (rsv lr st) <> None).
Proof.
  unfold set_sreg; simpl; split.
  - intros. destruct H as [[OK_SV OK_PRE] OK_SMEM OK_SREG]; simpl in *.
    repeat (split; try tauto).
    + intros r0; generalize (OK_SREG r0); clear OK_SREG; destruct (Pos.eq_dec r r0); try congruence.
    + generalize (OK_SREG r); clear OK_SREG; destruct (Pos.eq_dec r r); try congruence.
  - intros (OK & SEVAL). inv OK.
    repeat (split; try tauto; eauto).
    intros r0; destruct (Pos.eq_dec r r0) eqn:Heq; simpl;
    rewrite Heq; eauto.
Qed.

Lemma eval_list_sval_inj_not_none ctx st: forall l,
  (forall r, List.In r l -> eval_sval ctx (si_sreg st r) = None -> False) ->
  eval_list_sval ctx (list_sval_inj (map (si_sreg st) l)) = None -> False.
Proof.
  induction l.
  - intuition discriminate.
  - intros ALLR. simpl.
    simplify_option.
Qed.

Lemma hrs_sreg_set_correct r lr rsv hrs:
  WHEN hrs_sreg_set r lr rsv hrs ~> hrs' THEN forall ctx sis
  (REF: ris_refines ctx hrs sis),
  ris_refines ctx hrs' (set_sreg r (rsv lr sis) sis).
Proof.
  wlp_simplify; inversion REF.
  - (* may_trap -> true *)
    assert (X: si_ok ctx (set_sreg r (rsv lr sis) sis) <->
               ris_ok ctx {| ris_smem := hrs;
                             ris_input_init := ris_input_init hrs;
                             ok_rsval := exta :: ok_rsval hrs;
                             ris_sreg := red_PTree_set r exta0 hrs |}).
    {
      rewrite ok_hrset_sreg, OK_EQUIV.
      split.
      + intros (ROK & SEVAL); inv ROK.
        assert (ROK: ris_ok ctx hrs) by (econstructor; eauto).
        econstructor; eauto; simpl.
        intuition (subst; eauto).
        erewrite H0 in *; eauto.
      + intros (OK_RMEM & OK_RREG); simpl in *.
        assert (ROK: ris_ok ctx hrs) by (econstructor; eauto).
        erewrite <- H0 in *; eauto. }
    split; auto; rewrite <- X, ok_hrset_sreg.
    + intuition eauto.
    + intros (SOK & SEVAL) r0.
      rewrite ris_sreg_set_access.
      erewrite red_PTree_set_refines; intuition eauto.
  - (* may_trap -> false *)
    assert (X: si_ok ctx (set_sreg r (rsv lr sis) sis) <->
               ris_ok ctx {| ris_smem := hrs;
                             ris_input_init := ris_input_init hrs;
                             ok_rsval := ok_rsval hrs;
                             ris_sreg := red_PTree_set r exta hrs |}).
    {
      rewrite ok_hrset_sreg, OK_EQUIV.
      split.
      + intros (ROK & SEVAL); inv ROK.
        econstructor; eauto.
      + intros (OK_RMEM & OK_RREG).
        assert (ROK: ris_ok ctx hrs) by (econstructor; eauto).
        split; auto.
        intros SNONE; exploit may_trap_correct; eauto.
        * intros LNONE; eapply eval_list_sval_inj_not_none; eauto.
          assert (SOK: si_ok ctx sis) by intuition.
          inv SOK. intuition eauto.
        * rewrite <- MEM_EQ; auto. }
    split; auto; rewrite <- X, ok_hrset_sreg.
    + intuition eauto.
    + intros (SOK & SEVAL) r0.
      rewrite ris_sreg_set_access.
      erewrite red_PTree_set_refines; intuition eauto.
Qed.

Lemma hrs_ok_op_okpreserv ctx op args dest hrs:
  WHEN hrs_sreg_set dest args (Rop op) hrs ~> rst THEN
  ris_ok ctx rst -> ris_ok ctx hrs.
Proof.
  wlp_simplify; inv H2 || inv H1;
  simpl in *; econstructor; eauto.
Qed.

Lemma hrs_ok_load_okpreserv ctx chunk addr args dest hrs trap:
  WHEN hrs_sreg_set dest args (Rload trap chunk addr) hrs ~> rst THEN
  ris_ok ctx rst -> ris_ok ctx hrs.
Proof.
  wlp_simplify; inv H2 || inv H1;
  simpl in *; econstructor; eauto.
Qed.

Lemma hrs_ok_store_okpreserv ctx chunk addr args src hrs:
  WHEN hrexec_store chunk addr args src hrs ~> rst THEN
  ris_ok ctx rst -> ris_ok ctx hrs.
Proof.
  unfold hrexec_store; wlp_simplify.
  generalize H2. erewrite ok_rset_mem; intuition.
  specialize H1 with (sm2 := hrs).
  erewrite H1; eauto. rewrite H3. repeat autodestruct.
Qed.

Global Opaque hrs_sreg_set hrexec_store.
Local Hint Resolve hrs_sreg_set_correct: wlp.

(* transfer *)

Lemma ok_hrset_red_sreg ctx r rsv hrs:
  ris_ok ctx (ris_sreg_set hrs (red_PTree_set r rsv hrs))
  <-> (ris_ok ctx hrs).
Proof.
   split; destruct 1; econstructor; simpl in *; eauto.
Qed.

Fixpoint transfer_hrs (inputs: list reg) (hrs: ristate): ?? ristate :=
  match inputs with
  | nil => RET {| ris_smem := hrs.(ris_smem);
                  ris_input_init := false;
                  ok_rsval := hrs.(ok_rsval);
                  ris_sreg:= PTree.empty _
               |}
  | r::l =>
      DO hrs' <~ transfer_hrs l hrs;;
      DO sv <~ hrs_sreg_get hrs r;;
      RET (ris_sreg_set hrs' (red_PTree_set r sv hrs'))
  end.

Lemma ok_transfer_hrs ctx inputs hrs:
  WHEN transfer_hrs inputs hrs ~> hrs' THEN
  ris_ok ctx hrs'
  <-> (ris_ok ctx hrs).
Proof.
  induction inputs as [|r l]; simpl; wlp_simplify;
  try (inv H; econstructor; eauto; fail).
  + apply H0; rewrite <- ok_hrset_red_sreg; eauto.
  + rewrite ok_hrset_red_sreg; auto.
Qed.
Local Hint Resolve ok_transfer_hrs: wlp.

Lemma transfer_hrs_correct ctx inputs hrs sis:
  WHEN transfer_hrs inputs hrs ~> hrs' THEN
  ris_refines ctx hrs sis ->
  ris_refines ctx hrs' (transfer_sis inputs sis).
Proof.
  unfold transfer_hrs;
  induction inputs as [|r l]; wlp_simplify.
  inversion H.
  + constructor.
    * erewrite ok_transfer_sis; split; intros X.
      - constructor; simpl; rewrite OK_EQUIV in X; inv X; assumption.
      - rewrite OK_EQUIV; constructor; inv X; assumption.
    * intros X; inv X; simpl; apply MEM_EQ; constructor; auto.
    * simpl. unfold ris_sreg_get. auto.
  + constructor.
    * erewrite ok_hrset_red_sreg; eauto.
      inv H2. rewrite <- OK_EQUIV.
      erewrite !ok_transfer_sis; reflexivity.
    * intros X; inversion X; simpl in *.
      rewrite ok_hrset_red_sreg in X.
      inv H2; rewrite MEM_EQ; auto.
    * simpl; intros X r0. inversion H2.
      rewrite ok_hrset_red_sreg in X.
      erewrite red_PTree_set_refines; eauto.
      destruct (Pos.eq_dec); auto.
      inv H1. rewrite ok_transfer_sis in OK_EQUIV.
      rewrite <- OK_EQUIV, OK_EQUIV0 in X.
      erewrite H0; eauto.
Qed.

Definition tr_hrs := poly_tr (fun f tbl or => transfer_hrs (Regset.elements (pre_inputs f tbl or))).

Local Hint Resolve transfer_hrs_correct ok_transfer_hrs: core.
Local Opaque transfer_hrs.

Lemma ok_tr_hrs ctx fi hrs:
  WHEN tr_hrs (cf ctx) fi hrs ~> hrs' THEN
  ris_ok ctx hrs'
  <-> (ris_ok ctx hrs).
Proof.
   destruct fi; simpl; eauto.
Qed.

Lemma tr_hrs_correct ctx fi hrs sis:
  WHEN tr_hrs (cf ctx) fi hrs ~> hrs' THEN
  ris_refines ctx hrs sis ->
  ris_refines ctx hrs' (tr_sis (cf ctx) fi sis).
Proof.
  unfold tr_hrs, poly_tr; destruct fi; wlp_simplify;
  exploit transfer_hrs_correct; eauto.
  Unshelve. all: auto.
Qed.

Fixpoint hbuiltin_arg (hrs: ristate) (arg : builtin_arg reg): ?? builtin_arg sval := 
  match arg with
  | BA r => 
         DO v <~ hrs_sreg_get hrs 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 hrs ba1;;
    DO v2 <~ hbuiltin_arg hrs ba2;;
    RET (BA_splitlong v1 v2)
  | BA_addptr ba1 ba2 => 
    DO v1 <~ hbuiltin_arg hrs ba1;;
    DO v2 <~ hbuiltin_arg hrs ba2;;
    RET (BA_addptr v1 v2)
  end.

Lemma hbuiltin_arg_correct hrs arg:
  WHEN hbuiltin_arg hrs arg ~> hargs THEN forall ctx (f: reg -> sval)
    (RR: forall r, sval_refines ctx (hrs r) (f r)),
    eval_builtin_sval ctx hargs = eval_builtin_sval ctx (builtin_arg_map f arg).
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 hrs (args: list (builtin_arg reg)): ?? list (builtin_arg sval) :=
  match args with
  | nil => RET nil
  | a::l =>
    DO ha <~ hbuiltin_arg hrs a;;
    DO hl <~ hbuiltin_args hrs l;;
    RET (ha::hl)
    end.

Lemma hbuiltin_args_correct hrs args:
  WHEN hbuiltin_args hrs args ~> hargs THEN forall ctx (f: reg -> sval)
    (RR: forall r, sval_refines ctx (hrs r) (f r)),
    bargs_refines ctx hargs (List.map (builtin_arg_map f) args).
Proof.
  unfold bargs_refines; 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 hrs (ros: reg + ident): ?? (sval + ident) :=
  match ros with
  | inl r => DO hr <~ hrs_sreg_get hrs r;; RET (inl hr) 
  | inr s => RET (inr s)
  end.

Lemma hsum_left_correct hrs ros:
  WHEN hsum_left hrs ros ~> hsi THEN forall ctx (f: reg -> sval)
    (RR: forall r, sval_refines ctx (hrs r) (f r)),
    rsvident_refines ctx hsi (sum_left_map f ros).
Proof.
  destruct ros; wlp_simplify;
  econstructor; eauto.
Qed.
Global Opaque hsum_left.
Local Hint Resolve hsum_left_correct: wlp.

(** * Symbolic execution of final step *)
Definition hrexec_final_sfv (i: final) hrs: ?? sfval := 
  match i with
  | Bgoto pc => RET (Sgoto pc)
  | Bcall sig ros args res pc => 
      DO svos <~ hsum_left hrs ros;;
      DO sargs <~ hlist_args hrs args;;
      RET (Scall sig svos sargs res pc)
  | Btailcall sig ros args =>
      DO svos <~ hsum_left hrs ros;;
      DO sargs <~ hlist_args hrs args;;
      RET (Stailcall sig svos sargs)
  | Bbuiltin ef args res pc =>
      DO sargs <~ hbuiltin_args hrs args;;
      RET (Sbuiltin ef sargs res pc)
  | Breturn or => 
      match or with
      | Some r => DO hr <~ hrs_sreg_get hrs r;; RET (Sreturn (Some hr))
      | None => RET (Sreturn None)
      end
  | Bjumptable reg tbl =>
      DO sv <~ hrs_sreg_get hrs reg;;
      RET (Sjumptable sv tbl)
  end.

Lemma hrexec_final_sfv_correct ctx fi hrs sis:
  WHEN hrexec_final_sfv fi hrs ~> hrs' THEN forall
  (REF: ris_refines ctx hrs sis)
  (OK: ris_ok ctx hrs),
  rfv_refines ctx hrs' (sexec_final_sfv fi sis).
Proof.
  destruct fi; simpl; wlp_simplify; repeat econstructor;
  try inversion REF; try erewrite H; eauto.
Qed.

Fixpoint hrexec_rec f ib hrs (k: ristate -> ?? rstate): ?? rstate := 
  match ib with
  | BF fin _ =>
      DO sfv <~ hrexec_final_sfv fin hrs;;
      DO hrs' <~ tr_hrs f fin hrs;;
      RET (Rfinal hrs' sfv)
  (* basic instructions *)
  | Bnop _ => k hrs
  | Bop op args dst _ =>
      DO next <~ hrs_sreg_set dst args (Rop op) hrs;;
      k next
  | Bload trap chunk addr args dst _ =>
      DO next <~ hrs_sreg_set dst args (Rload trap chunk addr) hrs;;
      k next
  | Bstore chunk addr args src _ =>
      DO next <~ hrexec_store chunk addr args src hrs;;
      k next
 (* composed instructions *)
  | Bseq ib1 ib2 =>
      hrexec_rec f ib1 hrs (fun hrs2 => hrexec_rec f ib2 hrs2 k)
  | Bcond cond args ifso ifnot _ =>
      DO res <~ cbranch_expanse hrs cond args;;
      let (cond, vargs) := res in
      DO ifso <~ hrexec_rec f ifso hrs k;;
      DO ifnot <~ hrexec_rec f ifnot hrs k;;
      RET (Rcond cond vargs ifso ifnot)
  end
  .

Definition hrexec f ib :=
  DO init <~ hrs_init;;
  hrexec_rec f ib init (fun _ => RET Rabort).

Local Hint Resolve exec_final_refpreserv ok_tr_hrs: core.
Local Hint Constructors rst_refines: core.

Lemma hrexec_rec_correct1 ctx ib: 
  forall rk k
  (CONTh: forall sis lsis sfv, get_soutcome ctx (k sis) = Some (sout lsis sfv) ->  si_ok ctx lsis -> si_ok ctx sis)
  (CONT: forall hrs sis lsis sfv st,
    ris_refines ctx hrs sis ->
    k sis = st ->
    get_soutcome ctx (k sis) = Some (sout lsis sfv) ->
    si_ok ctx lsis ->
    WHEN rk hrs ~> rst THEN
    rst_refines ctx rst (k sis))
  hrs sis lsis sfv st
  (REF: ris_refines ctx hrs sis)
  (EXEC: sexec_rec (cf ctx) ib sis k = st)
  (SOUT: get_soutcome ctx st = Some (sout lsis sfv))
  (OK: si_ok ctx lsis),
  WHEN hrexec_rec (cf ctx) ib hrs rk ~> rst THEN
  rst_refines ctx rst st.
Proof.
  induction ib; try (wlp_simplify; try (eapply CONT; eauto); fail).
  - (* BF *)
    wlp_simplify; exploit tr_hrs_correct; eauto.
    intros; constructor; auto.
    intros X; apply H0 in X.
    exploit hrexec_final_sfv_correct; eauto.
  - (* Bseq *)
    wlp_simplify.
    eapply IHib1. 3-7: eauto.
    + simpl. eapply sexec_rec_okpreserv; eauto.
    + intros; eapply IHib2; eauto.
  - (* Bcond *)
    simpl; intros; wlp_simplify.
    assert (rOK: ris_ok ctx hrs). {
      erewrite <- OK_EQUIV. 2: eauto.
      eapply sexec_rec_okpreserv with (ib:=(Bcond cond args ib1 ib2 iinfo)); simpl; eauto.
    }
    exploit (Refcond ctx (fst exta) cond (snd exta) (list_sval_inj (map sis args)) exta0 exta1
              (sexec_rec (cf ctx) ib1 sis k) (sexec_rec (cf ctx) ib2 sis k));
    exploit H; eauto; intros SEVAL; auto.
    all:
      simpl in SOUT; generalize SOUT; clear SOUT;
      simplify_option.
    + intros; eapply IHib1; eauto.
    + intros; eapply IHib2; eauto.
Qed.

Lemma hrexec_correct1 ctx ib sis sfv:
  get_soutcome ctx (sexec (cf ctx) ib) = Some (sout sis sfv) ->
  (si_ok ctx sis) ->
  WHEN hrexec (cf ctx) ib ~> rst THEN
  rst_refines ctx rst (sexec (cf ctx) ib).
Proof.
  unfold sexec; intros; wlp_simplify.
  eapply hrexec_rec_correct1; eauto; simpl; congruence.
Qed.

Lemma hrexec_rec_okpreserv ctx ib: 
  forall k
  (CONT: forall hrs lhrs rfv,
    WHEN k hrs ~> rst THEN
    get_routcome ctx rst = Some (rout lhrs rfv) ->
    ris_ok ctx lhrs ->
    ris_ok ctx hrs)
  hrs lhrs rfv,
  WHEN hrexec_rec (cf ctx) ib hrs k ~> rst THEN
  get_routcome ctx rst = Some (rout lhrs rfv) ->
  ris_ok ctx lhrs ->
  ris_ok ctx hrs.
Proof.
  induction ib; simpl; try (wlp_simplify; try_simplify_someHyps; fail).
  - (* Bop *)
    wlp_simplify; exploit hrs_ok_op_okpreserv; eauto.
  - (* Bload *)
    destruct trap; wlp_simplify; try_simplify_someHyps;
    exploit hrs_ok_load_okpreserv; eauto.
  - (* Bstore *)
    wlp_simplify; exploit hrs_ok_store_okpreserv; eauto.
  - (* Bcond *)
    wlp_simplify; generalize H2; clear H2; simplify_option.
Qed.
Local Hint Resolve hrexec_rec_okpreserv: wlp.

Lemma hrexec_rec_correct2 ctx ib: 
  forall rk k
  (CONTh: forall hrs lhrs rfv,
    WHEN rk hrs ~> rst THEN
    get_routcome ctx rst = Some (rout lhrs rfv) ->
    ris_ok ctx lhrs ->
    ris_ok ctx hrs)
  (CONT: forall hrs sis lhrs rfv,
    ris_refines ctx hrs sis ->
    WHEN rk hrs ~> rst THEN
    get_routcome ctx rst = Some (rout lhrs rfv) ->
    ris_ok ctx lhrs ->
    rst_refines ctx rst (k sis))
  hrs sis lhrs rfv
  (REF: ris_refines ctx hrs sis),
  WHEN hrexec_rec (cf ctx) ib hrs rk ~> rst THEN
  get_routcome ctx rst = Some (rout lhrs rfv) ->
  ris_ok ctx lhrs ->
  rst_refines ctx rst (sexec_rec (cf ctx) ib sis k).
Proof.
  induction ib; try (wlp_simplify; fail).
  - (* BF *)
    wlp_simplify; exploit tr_hrs_correct; eauto.
    intros; constructor; auto.
    intros X; apply H0 in X.
    exploit hrexec_final_sfv_correct; eauto.
  - (* Bnop *) wlp_simplify; eapply CONT; eauto.
  - (* Bseq *)
    wlp_simplify.
    eapply IHib1. 3-6: eauto.
    + simpl; eapply hrexec_rec_okpreserv; eauto.
    + intros; eapply IHib2; eauto.
  - (* Bcond *)
    simpl; intros; wlp_simplify.
    assert (rOK: ris_ok ctx hrs). {
      simpl in H2; generalize H2; simplify_option.
    }
    exploit (Refcond ctx (fst exta) cond (snd exta) (list_sval_inj (map sis args)) exta0 exta1
              (sexec_rec (cf ctx) ib1 sis k) (sexec_rec (cf ctx) ib2 sis k));
    exploit H; eauto; intros SEVAL; auto.
    all:
      simpl in H2; generalize H2; clear H2;
      simplify_option.
    + intros; eapply IHib1; eauto.
    + intros; eapply IHib2; eauto.
    Unshelve. all: auto.
Qed.

Lemma hrexec_correct2 ctx ib hrs rfv:
  WHEN hrexec (cf ctx) ib ~> rst THEN
  get_routcome ctx rst = Some (rout hrs rfv) ->
  (ris_ok ctx hrs) ->
  rst_refines ctx rst (sexec (cf ctx) ib).
Proof.
  unfold hrexec; intros; wlp_simplify.
  eapply hrexec_rec_correct2; eauto; simpl;
  wlp_simplify; congruence.
Qed.

Global Opaque hrexec.

End CanonBuilding.

(** * 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.tree' A): ?? unit :=
  DO phy <~ phys_eq d1 d2;;
  if phy
  then
    RET tt
  else
    match d1, d2 with
    | Node001 r1, Node001 r2 => PTree_eq_check' r1 r2
    | Node010 x1, Node010 x2 =>
        phys_check x1 x2 "PTree_eq_check': data physically differ"
    | Node011 x1 r1, Node011 x2 r2 =>
        phys_check x1 x2 "PTree_eq_check': data physically differ" ;;
        PTree_eq_check' r1 r2
    | Node100 l1, Node100 l2 => PTree_eq_check' l1 l2
    | Node101 l1 r1, Node101 l2 r2 =>
        PTree_eq_check' l1 l2 ;;
        PTree_eq_check' r1 r2
    | Node110 l1 x1, Node110 l2 x2 =>
        phys_check x1 x2 "PTree_eq_check': data physically differ" ;;
        PTree_eq_check' l1 l2
    | Node111 l1 x1 r1, Node111 l2 x2 r2  =>
        phys_check x1 x2 "PTree_eq_check': data physically differ" ;;
        PTree_eq_check' l1 l2 ;;
        PTree_eq_check' r1 r2
    | _, _ => FAILWITH "PTree_eq_check': different shapes"
    end.

Lemma PTree_eq_check'_correct A : forall (d1 d2: PTree.tree' A),
    WHEN PTree_eq_check' d1 d2 ~> _ THEN d1 = d2.
Proof.
  induction d1; destruct d2; cbn; wlp_simplify; try congruence.
Qed.
                                    
Definition PTree_eq_check {A} (d1 d2: PTree.t A): ?? unit :=
  match d1, d2 with
  | Empty, Empty => RET tt
  | Nodes m1, Nodes m2 => PTree_eq_check' m1 m2
  | _, _ => FAILWITH "PTree_eq_check: empty vs nonempty"
  end.

Lemma PTree_eq_check_correct' A : forall (d1 d2: PTree.tree A),
    WHEN PTree_eq_check d1 d2 ~> _ THEN d1 = d2.
Proof.
  Local Hint Resolve PTree_eq_check'_correct: wlp.
  destruct d1 as [ | m1]; destruct d2 as [ | m2]; cbn; wlp_simplify.
  congruence.
Qed.                                    

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.
  Local Hint Resolve PTree_eq_check_correct': wlp.
  intros.
  wlp_simplify.
  congruence.
Qed.
Global Opaque PTree_eq_check.
Local Hint Resolve PTree_eq_check_correct: wlp.

Definition hrs_simu_check (hrs1 hrs2: ristate) : ?? unit :=
  DEBUG("? hrs_simu_check");;
  phys_check (ris_smem hrs1) (ris_smem hrs2) "hrs_simu_check: ris_smem sets aren't equiv";;
  phys_check (ris_input_init hrs1) (ris_input_init hrs2) "hrs_simu_check: ris_input_init bools aren't equiv";;
  PTree_eq_check (ris_sreg hrs1) (ris_sreg hrs2);;
  Sets.assert_list_incl mk_hash_params (ok_rsval hrs2) (ok_rsval hrs1);;
  DEBUG("=> hrs_simu_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 hrs_simu_check_correct hrs1 hrs2:
  WHEN hrs_simu_check hrs1 hrs2 ~> _ THEN
  ris_simu hrs1 hrs2.
Proof.
  wlp_simplify; constructor; auto.
  unfold ris_sreg_get; intros r; rewrite H, H1; reflexivity.
Qed.
Hint Resolve hrs_simu_check_correct: wlp.
Global Opaque hrs_simu_check.

Definition svos_simu_check (svos1 svos2: sval + 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 sval) :=
  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
  bs1 = 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
  lbs1 = 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 (sfv1 sfv2: sfval): ?? unit :=
  match sfv1, sfv2 with
  | Sgoto e1, Sgoto e2 =>
      phys_check e1 e2 "sfval_simu_check: Sgoto successors do not match"
  | Scall sig1 svos1 lsv1 res1 e1, Scall sig2 svos2 lsv2 res2 e2 =>
      phys_check e1 e2 "sfval_simu_check: Scall successors do not match";;
      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"
  | Stailcall sig1 svos1 lsv1, Stailcall 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"
  | Sbuiltin ef1 lbs1 br1 e1, Sbuiltin ef2 lbs2 br2 e2 =>
      phys_check e1 e2 "sfval_simu_check: Sbuiltin successors do not match";;
      phys_check ef1 ef2 "sfval_simu_check: Sbuiltin ef do not match";;
      phys_check br1 br2 "sfval_simu_check: Sbuiltin br do not match";;
      list_builtin_arg_simu_check lbs1 lbs2
  | Sjumptable sv1 le1, Sjumptable sv2 le2 =>
      phys_check le1 le2 "sfval_simu_check: Sjumptable successors do not match";;
      phys_check sv1 sv2 "sfval_simu_check: Sjumptable sval do not match"
  | Sreturn osv1, Sreturn osv2 =>
      option_eq_check osv1 osv2
  | _, _ => FAILWITH "sfval_simu_check: structure mismatch"
  end.

Lemma sfval_simu_check_correct sfv1 sfv2:
  WHEN sfval_simu_check sfv1 sfv2 ~> _ THEN
  rfv_simu sfv1 sfv2.
Proof.
  destruct sfv1; destruct sfv2; simpl; wlp_simplify; try congruence.
Qed.
Hint Resolve sfval_simu_check_correct: wlp.
Global Opaque sfval_simu_check.

Fixpoint rst_simu_check (rst1 rst2: rstate) {struct rst1} :=
  match rst1, rst2 with
  | Rfinal hrs1 sfv1, Rfinal hrs2 sfv2 =>
      hrs_simu_check hrs1 hrs2;;
      sfval_simu_check sfv1 sfv2
  | Rcond cond1 lsv1 rsL1 rsR1, Rcond cond2 lsv2 rsL2 rsR2 =>
      struct_check cond1 cond2 "rst_simu_check: conditions do not match";;
      phys_check lsv1 lsv2 "rst_simu_check: args do not match";;
      rst_simu_check rsL1 rsL2;;
      rst_simu_check rsR1 rsR2
  | _, _ => FAILWITH "rst_simu_check: simu_check failed"
  end.

Lemma rst_simu_check_correct rst1: forall rst2,
  WHEN rst_simu_check rst1 rst2 ~> _ THEN
  rst_simu rst1 rst2.
Proof.
  induction rst1; destruct rst2;
  wlp_simplify; constructor; auto.
Qed.
Hint Resolve rst_simu_check_correct: wlp.
Global Opaque rst_simu_check.

Definition simu_check_single (f1 f2: function) (ibf1 ibf2: iblock_info): ?? unit :=
  (* creating the hash-consing tables *)
  DO hC_sval <~ hCons hSVAL;;
  DO hC_list_hsval <~ hCons hLSVAL;;
  DO hC_hsmem <~ hCons hSMEM;;
  let hrexec := hrexec hC_sval.(hC) hC_list_hsval.(hC) hC_hsmem.(hC) in
  (* performing the hash-consed executions *)
  DO hst1 <~ hrexec f1 ibf1.(entry);;
  DO hst2 <~ hrexec f2 ibf2.(entry);;
  (* comparing the executions *)
  rst_simu_check hst1 hst2.

Lemma simu_check_single_correct (f1 f2: function) (ibf1 ibf2: iblock_info):
  WHEN simu_check_single f1 f2 ibf1 ibf2 ~> _ THEN
  symbolic_simu f1 f2 ibf1.(entry) ibf2.(entry).
Proof.
  unfold symbolic_simu; wlp_simplify.
  eapply rst_simu_correct; eauto.
  + intros; eapply hrexec_correct1; eauto; wlp_simplify.
  + intros; eapply hrexec_correct2; eauto; wlp_simplify.
Qed.
Global Opaque simu_check_single.
Global Hint Resolve simu_check_single_correct: wlp.

Program Definition aux_simu_check (f1 f2: function) (ibf1 ibf2: iblock_info): ?? bool :=
   DO r <~ 
     (TRY 
       simu_check_single f1 f2 ibf1 ibf2;; 
       RET true
      CATCH_FAIL s, _ =>
       println ("simu_check_failure:" +; s);;
       RET false
       ENSURE (fun b => b=true -> symbolic_simu f1 f2 ibf1.(entry) ibf2.(entry)));;
   RET (`r).
Obligation 1.
  split; wlp_simplify. discriminate.
Qed.

Lemma aux_simu_check_correct (f1 f2: function) (ibf1 ibf2: iblock_info):
  WHEN aux_simu_check f1 f2 ibf1 ibf2 ~> b THEN
  b=true -> symbolic_simu f1 f2 ibf1.(entry) ibf2.(entry).
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 (f1 f2: function) (ibf1 ibf2: iblock_info): res unit := 
  match unsafe_coerce (aux_simu_check f1 f2 ibf1 ibf2) with
  | Some true => OK tt
  | _ => Error (msg "simu_check has failed")
  end.

Lemma simu_check_correct f1 f2 ibf1 ibf2:
  simu_check f1 f2 ibf1 ibf2 = OK tt ->
  symbolic_simu f1 f2 ibf1.(entry) ibf2.(entry).
Proof.
  unfold simu_check.
  destruct (unsafe_coerce (aux_simu_check f1 f2 ibf1 ibf2)) as [[|]|] eqn:Hres; simpl; try discriminate.
  intros; eapply aux_simu_check_correct; eauto.
  eapply unsafe_coerce_not_really_correct; eauto.
Qed.