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

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.

(** Tactics *)

Ltac simplify_SOME x := repeat inversion_SOME x; try_simplify_someHyps.

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

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

(** * 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 hv <~ hash r;;
   RET [hc;hv].
Extraction Inline hSinput_hcodes.

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

Lemma hSinput_correct r:
  WHEN hSinput r ~> hv THEN forall ctx,
    sval_refines ctx hv (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 hv <~ hash op;;
   RET [hc;hv;list_sval_get_hid lsv].
Extraction Inline hSop_hcodes.

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

Lemma hSop_fSop_correct op lsv:
  WHEN hSop op lsv ~> hv THEN forall ctx,
    sval_refines ctx hv (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 ~> hv THEN forall ctx lsv2
   (LR: list_sval_refines ctx lsv1 lsv2),
   sval_refines ctx hv (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 hv1 <~ hash trap;;
   DO hv2 <~ hash chunk;;
   DO hv3 <~ hash addr;;
   RET [hc; smem_get_hid sm; hv1; hv2; hv3; 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 hv <~ hSload_hcodes sm trap chunk addr lsv;;
   hC_sval {| hdata := Sload sm trap chunk addr lsv unknown_hid; hcodes := hv |}.

Lemma hSload_correct sm1 trap chunk addr lsv1:
  WHEN hSload sm1 trap chunk addr lsv1 ~> hv THEN forall ctx lsv2 sm2
    (LR: list_sval_refines ctx lsv1 lsv2)
    (MR: smem_refines ctx sm1 sm2),
    sval_refines ctx hv (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 hv <~ hSundef_hcodes;;
   hC_sval {| hdata:=Sundef unknown_hid; hcodes :=hv; |}.

Lemma hSundef_correct:
  WHEN hSundef ~> hv THEN forall ctx,
    sval_refines ctx hv (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() ~> hv THEN forall ctx,
    list_sval_refines ctx hv (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 hv1 <~ hash chunk;;
   DO hv2 <~ hash addr;;
   RET [smem_get_hid sm; hv1; hv2; 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 hv <~ hSstore_hcodes sm chunk addr lsv srce;;
   hC_smem {| hdata := Sstore sm chunk addr lsv srce unknown_hid; hcodes := hv |}.

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 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 hv hl hc => 
      DO b <~ phys_eq hc unknown_hid;;
      if b then (* was not yet really hash-consed *)
        DO hv' <~ fsval_proj hv;;
        DO hl' <~ fsval_list_proj hl;;
        hScons hv' hl' 
      else RET 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.
    rewrite X. simplify_SOME z.
  - intros X; inversion REF.
    erewrite H1; eauto.
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): 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 =>
         DO lsv <~ hlist_args hrs lr;;
         hSop op lsv
        (* TODO gourdinl
       match target_op_simplify op lr hrs with
       | Some fhv => fsval_proj fhv
       | None =>
         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 ~> hv 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 hv (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_SOME z; erewrite H; eauto. }
    wlp_simplify; inv REF. erewrite H0; eauto.
  - (* Rload *)
    destruct trap; wlp_simplify; inv REF.
    + erewrite H0; eauto.
      erewrite H; [|eapply REG_EQ; eauto].
      erewrite MEM_EQ; eauto.
      repeat simplify_SOME z.
      * destruct (Memory.Mem.loadv _ _ _); try congruence.
      * rewrite H1 in OK1; congruence.
    + 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' hrs
      else PTree.set r sv hrs
  | false, Sundef _ =>
      PTree.remove r hrs
  | _, _ => PTree.set r sv 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 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) :=
  (* TODO gourdinl  
  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.
  wlp_simplify; inv REF.
  unfold eval_scondition; erewrite <- H; 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 hris_init: ?? ristate
  := DO hm <~ hSinit ();;
     RET {| ris_smem := hm; ris_input_init := true; ok_rsval := nil; ris_sreg := PTree.empty _ |}.

Lemma ris_init_correct:
  WHEN hris_init ~> hris THEN
  forall ctx, ris_refines ctx hris sis_init.
Proof.
  unfold hris_init, sis_init; wlp_simplify.
  econstructor; simpl in *; eauto.
  + split; destruct 1; econstructor; simpl in *;
    try rewrite H; try congruence; trivial.
  + destruct 1; simpl in *. unfold ris_sreg_get; simpl.
    intros; rewrite PTree.gempty; eauto.
Qed.

Definition hrset_sreg r lr rsv (hrs: ristate): ?? ristate :=
  DO ok_lsv <~
    (if may_trap rsv lr
     then DO hv <~ root_happly rsv lr hrs;;
          XDEBUG hv (fun hv => DO hv_name <~ string_of_hashcode (sval_get_hid hv);; RET ("-- insert undef behavior of hashcode:" +; (CamlStr hv_name))%string);;
          RET (hv::(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.

(* TODO gourdinl move this in BTL_SEtheory? *)
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.
    inversion_SOME v.
    + intro SVAL. inversion_SOME lv; [discriminate|].
      assert (forall r : reg, In r l -> eval_sval ctx (si_sreg st r) = None -> False).
      { intros r INR. eapply ALLR. right. assumption. }
      intro SVALLIST. intro. eapply IHl; eauto.
    + intros. exploit (ALLR a); simpl; eauto.
Qed.

Lemma hrset_sreg_correct r lr rsv hrs:
  WHEN hrset_sreg 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.

Fixpoint hrexec_rec f ib hrs (k: ristate -> ?? rstate): ?? rstate := 
  match ib with
  | BF fin _ => RET (Rfinal (tr_ris f fin hrs) (sexec_final_sfv fin hrs))
  (* basic instructions *)
  | Bnop _ => k hrs
  | Bop op args dst _ =>
      DO next <~ hrset_sreg dst args (Rop op) hrs;;
      k next
  | Bload TRAP chunk addr args dst _ =>
      DO next <~ hrset_sreg dst args (Rload TRAP chunk addr) hrs;;
      k next
  | Bload NOTRAP chunk addr args dst _ => RET Rabort
  | 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 <~ hris_init;;
  hrexec_rec f ib init (fun _ => RET Rabort).

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 ~> ris' THEN
    rst_refines ctx ris' (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 ~> hrs THEN
  rst_refines ctx hrs st.
Proof.
  (*
  induction ib; wlp_simplify.
  - admit.
  - eapply CONT; eauto.
  - try_simplify_someHyps. intros OUT.
    eapply CONT; eauto.
    intuition eauto.
    econstructor; intuition eauto.
    inv REF. inv H2.
    intuition eauto.


  - (* load *) intros; subst; autodestruct; simpl in *; subst; eauto.
  - (* seq *)
    intros; subst.
    eapply IHib1. 3-6: eauto.
    + simpl. eapply sexec_rec_okpreserv; eauto.
    + intros; subst. eapply IHib2; eauto.
  - (* cond *)
    intros rk k CONTh CONT hrs sis lsis sfv st REF EXEC OUT OK. subst.
    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.
    }
    generalize OUT; clear OUT; simpl.
    autodestruct.
    intros COND; generalize COND.
    erewrite <- eval_scondition_refpreserv; eauto.
    econstructor; try_simplify_someHyps.
     Qed.*)
Admitted.

Definition hsexec (f: function) ib: ?? rstate :=
  hrexec f ib.

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 sfval_simu_check (sfv1 sfv2: sfval) := RET tt.

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

Lemma rst_simu_check_correct rst1 rst2:
  WHEN rst_simu_check rst1 rst2 ~> _ THEN
  rst_simu rst1 rst2.
Proof.
  induction rst1, rst2;
  wlp_simplify.
Admitted.
Hint Resolve rst_simu_check_correct: wlp.
Global Opaque rst_simu_check.

Definition simu_check_single (f1 f2: function) (ib1 ib2: iblock): ?? (option (node * node)) :=
  (* creating the hash-consing tables *)
  DO hC_sval <~ hCons hSVAL;;
  DO hC_list_hsval <~ hCons hLSVAL;;
  DO hC_hsmem <~ hCons hSMEM;;
  let hsexec := hsexec hC_sval.(hC) hC_list_hsval.(hC) hC_hsmem.(hC) in
  (* performing the hash-consed executions *)
  DO hst1 <~ hsexec f1 ib1;;
  DO hst2 <~ hsexec f2 ib2;;
  (* comparing the executions *)
  rst_simu_check hst1 hst2.

Lemma simu_check_single_correct (f1 f2: function) (ib1 ib2: iblock):
  WHEN simu_check_single f1 f2 ib1 ib2 ~> _ THEN
  symbolic_simu f1 f2 ib1 ib2.
Proof.
Admitted.
Global Opaque simu_check_single.
Global Hint Resolve simu_check_single_correct: wlp.

Fixpoint simu_check_rec (f1 f2: function) (ibf1 ibf2: iblock_info): ?? unit :=
  DO res <~ simu_check_single f1 f2 ibf1.(entry) ibf2.(entry);;
  let (pc1', pc2') := res in
  simu_check_rec pc1' pc2'.

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 (f tf: function): ?? unit :=
   simu_check_rec f tf ;;
   DEBUG("simu_check OK!").

Local Hint Resolve PTree.elements_correct: core.
Lemma imp_simu_check_correct f tf:
  WHEN imp_simu_check f tf ~> _ THEN
  forall sexec_simu f tf.
Proof.
  wlp_simplify.
Qed.
Global Opaque imp_simu_check.
Global Hint Resolve imp_simu_check_correct: wlp.

Program Definition aux_simu_check (f tf: function): ?? bool :=
   DO r <~ 
     (TRY 
       imp_simu_check f tf;; 
       RET true
      CATCH_FAIL s, _ =>
       println ("simu_check_failure:" +; s);;
       RET false
      ENSURE (sexec_simu f tf));;
   RET (`r).
Obligation 1.
  split; wlp_simplify. discriminate.
Qed.

Lemma aux_simu_check_correct f tf:
  WHEN aux_simu_check f tf ~> b THEN
  sexec_simu f tf.
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 (f tf: function) : res unit := 
  match unsafe_coerce (aux_simu_check f tf) with
  | Some true => OK tt
  | _ => Error (msg "simu_check has failed")
  end.