Require Import Coqlib Maps Floats.
Require Import Classes.RelationClasses.
Require Import AST Integers Values Events Memory Globalenvs Smallstep.
Require Import Op Registers.
Require Import OptionMonad BTL BTL_SEtheory.
Require Import ValueDomain.
Require Import IntPromotionCommon.
Import ListNotations.
Import SvalNotations.
Import HConsing.

Local Open Scope option_monad_scope.
Local Open Scope lazy_bool_scope.

Local Hint Resolve OK_PRE OK_SMEM OK_SREG: core.
Local Hint Constructors sis_ok: core.

Inductive rrules_set: Type :=
  RRexpansions | RRlct (sr abs: bool) | RRschedule (rel abs : bool) | RRpromotion |
  RRstoreMotion (alias_load alias_store : bool) | RRnone.


Record se_mode := {
  se_ok_check: bool;
  se_ok_equiv: bool;
}.

Definition se_mode_set_ok_check (m : se_mode) : se_mode :=
  {| se_ok_check := true;
     se_ok_equiv := se_ok_equiv m |}.

Definition se_mode_set_ok_equiv (eqv : bool) (m : se_mode) : se_mode :=
  {| se_ok_check := se_ok_check m;
     se_ok_equiv := eqv |}.



Module OKset.

  Definition t : Type := list okclause.

  Program Definition pred (s : t) : okpred :=
    fun ctx => Forall (eval_okclause ctx) s.

  Definition eval (ctx : iblock_common_context) (s : t) : Prop :=
    proj1_sig (pred s) ctx.

  Lemma fold_eval s ctx:
    proj1_sig (pred s) ctx <-> eval ctx s.


  Definition empty : t := nil.

  Lemma eval_empty ctx:
    eval ctx empty.

  Definition singleton (c : okclause) : t := c :: nil.

  Lemma eval_singleton ctx c:
    eval ctx (singleton c) <-> eval_okclause ctx c.
  
  Definition sfalse : t := singleton fOKfalse.

  Lemma eval_sfalse ctx:
    ~eval ctx sfalse.

  Definition of_list (cs : list okclause) : t := cs.

  Lemma eval_of_list ctx cs:
    eval ctx (of_list cs) <-> Forall (eval_okclause ctx) cs.

  Definition union (s0 s1 : t) : t := s0 ++ s1.

  Lemma eval_union ctx s0 s1:
    eval ctx (union s0 s1) <-> eval ctx s0 /\ eval ctx s1.

  Global Opaque t pred.
End OKset.


Definition sval_get_hid (sv: sval): hashcode :=
  match sv with
  | Sinput _ _ hid | Sop _ _ hid | Sfoldr _ _ _ hid
  | Sload _ _ _ _ _ hid | SmayUndef _ _ hid
      => hid
  end.

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

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

Definition okclause_get_hid (okc : okclause) : hashcode :=
  match okc with
  | OKfalse hid | OKalive _ hid
  | OKpromotableOp _ _ _ hid | OKpromotableCond _ _ _ hid
  | OKaddrMatch _ _ _ hid | OKvalidAccess _ _ _ _ hid => hid
  end.

Definition sval_set_hid (sv: sval) (hid: hashcode): sval :=
  match sv with
  | Sinput trg r _ => Sinput trg r hid
  | Sop o lsv _ => Sop o lsv hid
  | Sfoldr op lsv sv0 _ => Sfoldr op lsv sv0 hid
  | Sload sm trap chunk addr lsv _ => Sload sm trap chunk addr lsv hid
  | SmayUndef cond sv _ => SmayUndef cond sv 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 sinfo srce _ => Sstore sm chunk addr lsv sinfo srce hid
  end.

Definition okclause_set_hid (okc : okclause) (hid : hashcode) : okclause :=
  match okc with
  | OKfalse _ => OKfalse hid
  | OKalive sv _ => OKalive sv hid
  | OKpromotableOp op prom args _ => OKpromotableOp op prom args hid
  | OKpromotableCond cond prom args _ => OKpromotableCond cond prom args hid
  | OKaddrMatch addr args aa _ => OKaddrMatch addr args aa hid
  | OKvalidAccess perm chk addr args _ => OKvalidAccess perm chk addr args hid
  end.

Lemma sval_set_hid_correct ctx x y:
  sval_set_hid x unknown_hid = sval_set_hid y unknown_hid ->
  sval_equiv ctx x y.
Global 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_equiv ctx x y.
Global 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_equiv ctx x y.
Global Hint Resolve smem_set_hid_correct: core.

Lemma okclause_set_hid_correct ctx x y:
  okclause_set_hid x unknown_hid = okclause_set_hid y unknown_hid ->
  eval_okclauseb ctx x = eval_okclauseb ctx y.
Global Hint Resolve okclause_set_hid_correct: core.

refined (symbolic) internal state and abstract operators over states

Record ristate :=
  {
    ris_smem:> smem;
    ris_input_init: option bool;
    ris_sreg: PTree.t sval;
    ris_pre: OKset.t;
  }.

Definition ris_sreg_get (ris: ristate) r: option sval :=
   match ris.(ris_sreg)!r with
   | None => SOME trg <- ris_input_init ris IN Some (fSinput trg r)
   | Some sv => Some sv
   end.

Coercion ris_sreg_get: ristate >-> Funclass.

Definition ris_sreg_set (ris: ristate) (sreg: PTree.t sval): ristate :=
  {| ris_smem := ris.(ris_smem);
     ris_input_init := ris.(ris_input_init);
     ris_pre := ris.(ris_pre);
     ris_sreg := sreg |}.

Definition ris_input_init_set (ris: ristate) (ini : option bool): ristate :=
  {| ris_smem := ris.(ris_smem);
     ris_input_init := ini;
     ris_pre := ris.(ris_pre);
     ris_sreg := ris.(ris_sreg) |}.

Definition ris_pre_set (ris: ristate) pre: ristate :=
  {| ris_smem := ris.(ris_smem);
     ris_input_init := ris.(ris_input_init);
     ris_pre := pre;
     ris_sreg := ris.(ris_sreg) |}.

Definition ris_sreg_pre_set (ris: ristate) sreg pre: ristate :=
  {| ris_smem := ris.(ris_smem);
     ris_input_init := ris.(ris_input_init);
     ris_pre := pre;
     ris_sreg := sreg |}.

Definition rset_smem rm (ris:ristate): ristate :=
  {| ris_smem := rm;
     ris_input_init := ris.(ris_input_init);
     ris_pre := ris.(ris_pre);
     ris_sreg := ris.(ris_sreg) |}.

Definition ris_ok ctx (ris: ristate) := OKset.eval ctx (ris_pre ris).

Lemma ris_ok_set_sreg ctx ris sreg:
  ris_ok ctx ris <-> ris_ok ctx (ris_sreg_set ris sreg).

Lemma ris_sreg_set_access (ris: ristate) (sreg: PTree.t sval) r rsval:
  ris_sreg_pre_set ris sreg rsval r = ris_sreg_set ris sreg r.

Lemma ris_ok_set_input_init ctx ris ini:
  ris_ok ctx ris <-> ris_ok ctx (ris_input_init_set ris ini).

Definition ris_empty := {|
  ris_smem := fSinit;
  ris_input_init := Some false;
  ris_pre := OKset.empty;
  ris_sreg := PTree.empty _
|}.

Definition ris_error := {|
  ris_smem := fSinit;
  ris_input_init := Some true;
  ris_pre := OKset.sfalse;
  ris_sreg := PTree.empty _
|}.

Lemma ris_error_not_ok ctx:
  ~ris_ok ctx ris_error.


Definition red_PTree_set (r: reg) (sv: sval) (ris: ristate): PTree.t sval :=
  match ris_input_init ris, sv with
  | Some ini, Sinput trg r' _ =>
      if bool_dec ini trg && Pos.eq_dec r r'
      then PTree.remove r ris.(ris_sreg)
      else PTree.set r sv ris.(ris_sreg)
  | _, _ => PTree.set r sv ris.(ris_sreg)
  end.

Lemma red_PTree_set_spec r sv ris ctx r0:
  optsv_simu ctx (ris_sreg_set ris (red_PTree_set r sv ris) r0)
                 (if Pos.eq_dec r r0 then Some sv else ris r0).
Global Opaque red_PTree_set.

refinement of (symbolic) internal states

Record ris_refines_ok ctx (ris: ristate) (sis: sistate): Prop := {
  SHY: `sis.(sis_hyp) ctx;
  ROK: ris_ok ctx ris;
  SOK: sis_ok ctx sis;
  MEM_EQ: eval_smem ctx ris.(ris_smem) = eval_smem ctx sis.(sis_smem);
  REG_EQ: forall r, optsv_simu ctx (ris r) (sis r);
}.

Inductive ok_equivp (shy : Prop) (sok : Prop) (rok : Prop) : bool -> Prop :=
  | OKequivpImp (IMP: rok -> shy /\ sok): ok_equivp shy sok rok false
  | OKequivpEqv (SHY : shy) (EQV: rok <-> sok): ok_equivp shy sok rok true.

Lemma ok_equivp_intro_eqv [shy sok rok : Prop] (SHY : shy) (EQV: sok <-> rok) b:
  ok_equivp shy sok rok b.

Lemma ok_equivp_elim_imp [shy sok rok b] (EQP: ok_equivp shy sok rok b):
  rok -> shy /\ sok.

Lemma ok_equivp_elim_eqv [shy sok rok b] (EQP : ok_equivp shy sok rok b):
  b = true -> shy /\ (sok <-> rok).

Lemma ok_equivp_morph [shy0 shy1 sok0 sok1 rok0 rok1 b]
  (EQP : ok_equivp shy0 sok0 rok0 b)
  (HEQ : shy0 <-> shy1)
  (SEQ : sok0 <-> sok1)
  (REQ : rok0 <-> rok1):
  ok_equivp shy1 sok1 rok1 b.

Lemma ok_equivp_and [shy sok rok b] (P : Prop)
  (EQP : ok_equivp shy sok rok b):
  ok_equivp shy (sok /\ P) (rok /\ P) b.


Record ris_refines (m : se_mode) ctx (ris: ristate) (sis: sistate): Prop := {
  OK_EQUIV: ok_equivp (`sis.(sis_hyp) ctx) (sis_ok ctx sis) (ris_ok ctx ris) m.(se_ok_equiv);
  REF: ris_ok ctx ris -> ris_refines_ok ctx ris sis
}.

Lemma wref [ctx ris sis]:
  ris_refines_ok ctx ris sis ->
  forall m, ris_refines m ctx ris sis.

Lemma ok_ref [m ctx ris sis]:
  ris_ok ctx ris -> ris_refines m ctx ris sis ->
  ris_refines_ok ctx ris sis.

Lemma ok_ref_si [ctx ris sis]:
  sis_ok ctx sis ->
  forall m, m.(se_ok_equiv) = true ->
  ris_refines m ctx ris sis ->
  ris_refines_ok ctx ris sis.

Record ris_refines_ok_introT ctx ris sis : Prop := {
  RI_MEM_EQ: smem_equiv ctx (ris_smem ris) (sis_smem sis);
  RI_REG_EQ: forall (r : reg), optsv_simu ctx (ris r) (sis r)
}.

Lemma ris_refines_intro m ctx ris sis
  (OK_EQUIV: ok_equivp (`sis.(sis_hyp) ctx) (sis_ok ctx sis) (ris_ok ctx ris) m.(se_ok_equiv))
  (REF: ris_ok ctx ris -> sis_ok ctx sis -> ris_refines_ok_introT ctx ris sis):
  ris_refines m ctx ris sis.

Lemma ris_refines_intro_not_ok m ctx ris sis:
  ~ris_ok ctx ris ->
  (m.(se_ok_equiv) = true -> `sis.(sis_hyp) ctx /\ ~sis_ok ctx sis) ->
  ris_refines m ctx ris sis.

Lemma ris_refines_case [m ctx ris sis]:
  ris_refines m ctx ris sis ->
  ris_refines_ok ctx ris sis \/
  (~ris_ok ctx ris /\ (m.(se_ok_equiv) = true -> `sis.(sis_hyp) ctx /\ ~sis_ok ctx sis)).

Lemma ris_refines_step [m ctx hrs0 hrs1 sis0 sis1]
  (H : ris_refines m ctx hrs0 sis0)
  (R : ris_ok ctx hrs1 -> ris_ok ctx hrs0)
  (S : sis_rel sis0 sis1)
  (P : forall (RR : ris_refines_ok ctx hrs0 sis0), ris_refines m ctx hrs1 sis1):
  ris_refines m ctx hrs1 sis1.

Global Hint Resolve wref: core.

Lemma ris_refines_ok_morph [ctx ri si0 si1]:
  sistate_eq ctx si0 si1 ->
  ris_refines_ok ctx ri si0 <-> ris_refines_ok ctx ri si1.

Lemma ris_refines_morph [m ctx ri si0 si1]:
  sistate_eq ctx si0 si1 ->
  ris_refines m ctx ri si0 ->
  ris_refines m ctx ri si1.

Lemma ris_refines_change_mode m m' ctx ris sis:
  ris_refines m ctx ris sis ->
  implb m'.(se_ok_equiv) m.(se_ok_equiv) = true ->
  ris_refines m' ctx ris sis.

Lemma ris_ok_empty ctx:
  ris_ok ctx ris_empty.

Lemma ris_refines_ok_empty ctx:
  ris_refines_ok ctx ris_empty sis_empty.
Global Hint Resolve ris_ok_empty ris_refines_ok_empty: sempty.

Local Hint Resolve ROK SOK MEM_EQ REG_EQ: core.
Local Hint Constructors ris_refines: core.

Lemma ris_refines_reg_some [ctx ris sis r sv]
  (RR: ris_refines_ok ctx ris sis)
  (RG: ris r = Some sv):
  exists sv', sis r = Some sv' /\ sval_equiv ctx sv sv'.

Lemma ris_refines_reg_some_si [ctx ris sis r sv]
  (RR: ris_refines_ok ctx ris sis)
  (RG: sis r = Some sv):
  exists sv', ris r = Some sv' /\ sval_equiv ctx sv' sv.

Lemma ris_refines_ok_rmem [ctx ris sis]
  (RR : ris_refines_ok ctx ris sis):
  alive (eval_smem ctx (ris_smem ris)).

refinement of (symbolic) final states

Inductive rfval :=
  | Sgoto (pc: exit)
  | Sreturn (or : option sval)
  | Scall (sig:signature) (svos: sval + qualident) (lsv:list_sval) (res:reg) (pc:exit)
  | Stailcall (sig : signature) (svos : sval + qualident) (lsv : list_sval)
  | Sbuiltin (ef:external_function) (sargs: list (builtin_arg sval)) (res: builtin_res reg) (pc:exit)
  | Sjumptable (sv: sval) (tbl: list exit).

Definition sfval_of_rsval (rfv : rfval) : sfval :=
  match rfv with
  | Sgoto pc => Bgoto pc
  | Sreturn or => Breturn or
  | Scall sig svos lsv res pc => Bcall sig svos (list_of_lsv lsv) res pc
  | Stailcall sig svos lsv => Btailcall sig svos (list_of_lsv lsv)
  | Sbuiltin ef sargs res pc => Bbuiltin ef sargs res pc
  | Sjumptable sv tbl => Bjumptable sv tbl
  end.

Definition rfv_refines (ctx : iblock_common_context) (rfv : rfval) (sfv : sfval) : Prop :=
  sfv_simu ctx (sfval_of_rsval rfv) sfv.

Inductive rstate :=
  | Sfinal (sis: ristate) (rfv: rfval) (annot : meminv_annot_t)
  | Scond (cond: condition) (args: list_sval) (ifso ifnot: rstate)
 .

Definition routcome := poutcome ristate rfval.

Definition error_routcome : routcome := sout ris_error (Sreturn None).
Definition error_rstate : rstate := Sfinal ris_error (Sreturn None) None.

Fixpoint get_routcome ctx (rs : rstate): routcome :=
  match rs with
  | Sfinal sis sfv _ => sout sis sfv
  | Scond cond args ifso ifnot =>
      match eval_scondition ctx cond args with
      | Some b => get_routcome ctx (if b then ifso else ifnot)
      | None => error_routcome
      end
  end.


Inductive rout_refines (ctx : iblock_common_context) (P : ristate -> sistate -> Prop)
  : routcome -> soutcome -> Prop :=
  rout_refines_intro (ris : ristate) (rfv : rfval) (sis : sistate) (sfv : sfval)
      (RST_RR : P ris sis)
      (RST_RFV : ris_ok ctx ris -> rfv_refines ctx rfv sfv)
  : rout_refines ctx P (sout ris rfv) (sout sis sfv).

Lemma elim_rout_refines ctx P ris rfv sis sfv:
  rout_refines ctx P (sout ris rfv) (sout sis sfv) ->
  P ris sis /\ (ris_ok ctx ris -> sfv_simu ctx (sfval_of_rsval rfv) sfv).

Definition rst_refines_ok ctx (rs : rstate) (ss : sstate) :=
  rout_refines ctx (ris_refines_ok ctx) (get_routcome ctx rs) (get_soutcome ctx ss).

Definition rst_refines (m : se_mode) ctx (rs : rstate) (ss : sstate) :=
  rout_refines ctx (ris_refines m ctx) (get_routcome ctx rs) (get_soutcome ctx ss).

Lemma ris_refines_step_rst [m : se_mode] [ctx : iblock_common_context]
          [hrs0 : ristate] [rst1 : rstate] [sis0 : sistate] [ss1 : sstate]
  (H : ris_refines m ctx hrs0 sis0)
  (R : ris_ok ctx (get_routcome ctx rst1).(_sis) -> ris_ok ctx hrs0)
  (S : sis_rel sis0 (get_soutcome ctx ss1).(_sis))
  (P : ris_refines_ok ctx hrs0 sis0 -> rst_refines m ctx rst1 ss1):
  rst_refines m ctx rst1 ss1.

Lemma rout_refines_error m ctx sis
  (HY : `sis.(sis_hyp) ctx):
  rout_refines ctx (ris_refines m ctx) error_routcome (error_soutcome sis).

Lemma wrst_ref ctx rs ss:
  rst_refines_ok ctx rs ss ->
  forall m, rst_refines m ctx rs ss.

Simulation relation on symbolic final values

Definition rfv_simu (rfv1 rfv2: rfval): Prop := rfv1 = rfv2.

Lemma rfv_simu_correct rfv1 rfv2 ctx sfv1 sfv2:
  rfv_simu rfv1 rfv2 ->
  rfv_refines ctx rfv1 sfv1 ->
  rfv_refines ctx rfv2 sfv2 ->
  sfv_simu ctx sfv1 sfv2.

Relation between the implementation states for common operations

Record ris_rel (m : se_mode) (ris0 ris1 : ristate) := {
  RRL_INPUT: ris0.(ris_input_init) = ris1.(ris_input_init);
  RRL_OK: forall ctx, ris_ok ctx ris1 -> ris_ok ctx ris0;
  RRL_OK_SI: m.(se_ok_check) = true ->
             forall ctx, ris_ok ctx ris0 -> ris_ok ctx ris1;
}.

Global Instance ris_rel_PreOrder {m : se_mode}: PreOrder (ris_rel m).