Require Import Coqlib AST RTL BTL Errors.
Require Import Maps Registers OptionMonad.
Require Import BTL_Invariants BTL_SEtheory.
Require Import BTL_SEsimuref BTL_SEsimplify BTL_SEimpl_prelude.
Require Import BTL_SEimpl_SE BTL_SEimpl_SI.
Import Notations SvalNotations.
Import HConsing.
Local Open Scope impure.

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.

Lemma phys_check_correct {A} (a b: A) msg:
  WHEN phys_check a b msg ~> _ THEN
  a = b.

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.
Global Opaque struct_check.
Local 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.
Global Opaque option_eq_check.
Local Hint Resolve option_eq_check_correct:wlp.

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

Lemma option_incl_check_correct A (o1 o2: option A): WHEN option_incl_check o1 o2 ~> _ THEN
  o1=o2 \/ o1 = None.
Global Opaque option_incl_check.
Local Hint Resolve option_incl_check_correct:wlp.


Import PTree.

Definition PTree_incl_check {A} (m1 m2: PTree.t A): ?? unit :=
  PTree.tree_rec2
    RET tt
    (fun t => RET tt)
    (fun t => FAILWITH "PTree_incl_check")
    (fun l1 o1 r1 l2 o2 r2 olrec orrec =>
      DO lrec <~ olrec;;
      DO rrec <~ orrec;;
      DO oc <~ option_incl_check o1 o2;;
      RET tt)
    m1 m2.

Lemma PTree_incl_check_correct A: forall (m1 m2: PTree.t A),
 WHEN PTree_incl_check m1 m2 ~> _ THEN forall x,
 m1!x = m2!x \/ m1!x = None.
Local Hint Resolve PTree_incl_check_correct: wlp.

Definition hrs_simu_check (hrs1 hrs2: ristate) : ?? unit :=
  struct_check (ris_input_init hrs1) None
    "hrs_simu_check : hrs1.(ris_input_init) isn't None";;
  PTree_incl_check (ris_sreg hrs1) (ris_sreg hrs2);;
  DEBUG("hrs_simu_check=>OK").

Lemma hrs_simu_check_spec ctx hrs1 hrs2 sis1 sis2
  (RR1 : ris_refines_ok ctx hrs1 sis1)
  (RR2 : ris_refines_ok ctx hrs2 sis2)
  (MEM : smem_equiv ctx (sis_smem sis1) (sis_smem sis2)):
  WHEN hrs_simu_check hrs1 hrs2 ~> _ THEN
  sistate_simu ctx sis1 sis2.
Global Opaque hrs_simu_check.


Fixpoint check_list [A] (check : A -> ?? unit) (l : list A) : ?? unit :=
  match l with
  | nil => RET ()
  | x :: xs => check x;; check_list check xs
  end.

Lemma check_list_spec A check l:
  WHEN @check_list A check l ~> _ THEN
  Forall (fun x => check x ~~> ()) l.
Global Opaque check_list.


Definition hrs_check_match_si HCF HC RRULES (m : se_mode) (gm : node -> csasv)
    (hrs0 : ristate) (rfv : rfval) (hrs1 : ristate) : ?? unit :=
  DO csis <~ si_rfv gm rfv;;
  let m' := se_mode_set_ok_check m in
  check_list (fun csi =>
    DO hrsI <~ @tr_hrs_single HCF HC RRULES m' hrs0 csi;;
    let hrsI := ris_input_init_set hrsI None in
    hrs_simu_check hrsI hrs1
  ) csis.

Lemma hrs_check_match_si_spec HCF HC RRULES m ctx gm hrs0 sis0 rfv sfv hrs1 sis1
  (RR0 : ris_refines_ok ctx hrs0 sis0)
  (RR1 : ris_refines_ok ctx hrs1 sis1)
  (RFV : rfv_refines ctx rfv sfv)
  (MEM : smem_equiv ctx (sis_smem sis0) (sis_smem sis1)):
  WHEN hrs_check_match_si HCF HC RRULES m gm hrs0 rfv hrs1 ~> _ THEN
  match_tr_si_sfv ctx gm sis0 sfv sis1.
Global Opaque hrs_check_match_si.


Definition svos_simu_check (svos1 svos2: sval + qualident) :=
  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.
Global Opaque svos_simu_check.
Local 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.
Global Opaque builtin_arg_simu_check.
Local 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.
Global Opaque list_builtin_arg_simu_check.
Local Hint Resolve list_builtin_arg_simu_check_correct: wlp.

Definition sfval_simu_check (sfv1 sfv2: rfval): ?? 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.
Local Hint Resolve sfval_simu_check_correct: wlp.
Global Opaque sfval_simu_check.


Fixpoint rst_simu_check (check : ristate -> rfval -> ristate -> rfval -> meminv_annot_t -> ?? unit)
  (rst1 rst2: rstate) {struct rst1} : ?? unit :=
  match rst1, rst2 with
  | Sfinal hrs1 sfv1 _, Sfinal hrs2 sfv2 meminv_annot =>
      check hrs1 sfv1 hrs2 sfv2 meminv_annot
  | Scond cond1 lsv1 rsL1 rsR1, Scond 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 check rsL1 rsL2;;
      rst_simu_check check rsR1 rsR2
  | _, _ => FAILWITH "rst_simu_check: simu_check failed"
  end.

Lemma rst_simu_check_spec ctx check rst1 rst2 ris1 rfv1
  (GET : get_routcome ctx rst1 = sout ris1 rfv1)
  (ROK : ris_ok ctx ris1):
  WHEN rst_simu_check check rst1 rst2 ~> _ THEN
  let (ris2, rfv2) := get_routcome ctx rst2 in
  exists an,
  check ris1 rfv1 ris2 rfv2 an ~~> ().

Global Opaque rst_simu_check.

Definition HashConsing_Fcts (_ : unit) :=
  DO hC_sval <~ hCons hSVAL;;
  DO hC_list_sval <~ hCons hLSVAL;;
  DO hC_smem <~ hCons hSMEM;;
  DO hC_okclause <~ hCons hOKCL;;
  RET (Build_HashConsingFcts hC_sval.(hC) hC_list_sval.(hC) hC_smem.(hC) hC_okclause.(hC)).

Lemma HashConsing_Instance_correct u:
  WHEN HashConsing_Fcts u~> HCF THEN
  HashConsingHyps HCF.
Global Opaque HashConsing_Fcts.

Program Definition HashConsing (u : unit): ?? { HCF : HashConsingFcts | HashConsingHyps HCF } :=
  DO HCF <~ mk_annot (HashConsing_Fcts u);;
  RET (exist _ (`HCF) _).
Global Opaque HashConsing.

Definition simu_check_single (RRULES: rrules_set) (f1 f2: function)
  (ibf1 ibf2: iblock_info) (gm: gluemap) pc: ?? unit :=
  DO HCF_HC <~ HashConsing tt;;
  let (HCF, HC) := HCF_HC in
  let se_mode := {| se_ok_check := false;
                    se_ok_equiv := true |} in
  let se_mode_trg := se_mode_set_ok_equiv false se_mode in
  let hrs_ini_states := @hrs_ini_states HCF HC RRULES in
  let hrexec := @hrexec HCF HC RRULES in
  let hrs_check_match_si := hrs_check_match_si HCF HC RRULES se_mode in
  let hrs_imem_subst_isol := @hrs_imem_subst_isol HCF HC RRULES in
  DO ini12 <~ hrs_ini_states se_mode (gm pc);;
  let (ini1, ini2) := ini12 in
  DO ends1 <~ hrexec se_mode ibf1.(entry) ini1;;
  DO ends2 <~ hrexec se_mode_trg ibf2.(entry) ini2;;
  rst_simu_check (fun end1 fin1 end2 fin2 mannot =>
    sfval_simu_check fin1 fin2;;
    assert_okset_incl (ris_pre end2) (ris_pre end1);;
    let endE := rset_smem (ris_smem end2) end1 in
    hrs_check_match_si (fun pc => history (gm pc)) endE fin1 endE;;
    hrs_check_match_si (fun pc => glue (gm pc)) endE fin1 end2;;
    DO ims <~ meminv_rfv (fun pc => meminv (gm pc)) fin1;;
    check_list (fun im =>
      DO mI <~ hrs_imem_subst_isol se_mode_trg end2 mannot im;;
      let (mI, mIok) := mI in
      assert_okset_incl mIok (ris_pre end1);;
      phys_check (ris_smem end1) mI "simu_check_single: memory invariant"
    ) ims
  ) ends1 ends2.

Lemma simu_check_single_correct (RRULES: rrules_set) (f1 f2: function) (ibf1 ibf2: iblock_info)
  (gm: gluemap) pc:
  WHEN simu_check_single RRULES f1 f2 ibf1 ibf2 gm pc ~> _ THEN
  match_sexec_si_all_ctx gm ibf1.(entry) ibf2.(entry) pc.
Global Opaque simu_check_single.
Local Hint Resolve simu_check_single_correct: wlp.

Coerce simu_check_single into a pure function.

Definition aux_simu_check (RRULES: rrules_set) (f1 f2: function) (ibf1 ibf2: iblock_info)
  (gm: gluemap) (pc: node): ?? unit :=
   XDEBUG pc (fun pc => DO name_pc <~ string_of_Z (Zpos pc);; RET ("simu_check_single?:BTL block n°" +; name_pc)%string);;
   simu_check_single RRULES f1 f2 ibf1 ibf2 gm pc;;
   DEBUG("simu_check_single=>OK").

Lemma aux_simu_check_correct (RRULES: rrules_set) (f1 f2: function) (ibf1 ibf2: iblock_info)
  (gm: gluemap) (pc: node):
  WHEN aux_simu_check RRULES f1 f2 ibf1 ibf2 gm pc ~> _ THEN
    match_sexec_si_all_ctx gm ibf1.(entry) ibf2.(entry) pc.

Definition simu_check (RRULES: rrules_set) (f1 f2: function) (ibf1 ibf2: iblock_info)
  (gm: gluemap) (pc: node): res unit :=
  if has_returned (aux_simu_check RRULES f1 f2 ibf1 ibf2 gm pc)
  then OK tt
  else Error (msg "unexpected value of has_returned")
  .

Lemma simu_check_correct RRULES f1 f2 ibf1 ibf2 gm pc:
  simu_check RRULES f1 f2 ibf1 ibf2 gm pc = OK tt ->
  match_sexec_si_all_ctx gm ibf1.(entry) ibf2.(entry) pc.