Require Import Coqlib.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Smallstep.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import Constant.
Require Import GlobIdent.
Require Import AbstractDataType.
Require Import GlobalOracle.

Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compat.CompatLayers.
Require Import AuxStateDataType.
Require Import RealParams.
Require Import LogReplay.

Section Refinement.

  Local Open Scope string_scope.
  Local Open Scope error_monad_scope.
  Local Open Scope Z_scope.

  Context `{real_params: RealParams}.

  Section WITHMEM.

    Context `{Hstencil: Stencil}.
    Context `{Hmem: Mem.MemoryModelX}.
    Context `{Hmwd: UseMemWithData mem}.

    Function BigE2E (e: BigSharedMemEvent) :=
      match e with
        | BTDSPAWN curid new_id q ofs b_uc uc_ofs´ ⇒
          Some (TSHARED (OTDSPAWN new_id))
        | BTDYIELD cur_id ⇒
          Some (TSHARED (OTDYIELD cur_id))
        | BTDWAKE _ cv_id ⇒
          Some (TSHARED (OTDWAKE cv_id))
        | BTDWAKE_DIFF _ cv_id wk_id cpu´ ⇒
          Some (TSHARED (OTDWAKE_DIFF wk_id cpu´))
        | _ ⇒ None
      end.

    Function BigE2id (e: BigOracleEvent) (id: Z) :=
      match e with
        | TBEVENT cid e0 ⇒
          if zeq id lock_AT_start then
            match e0 with
              | TBSHARED (BPALLOCE _ b) ⇒
                TEVENT cid (TSHARED (OPALLOCE b)) :: nil
              | _ ⇒ nil
            end
          else
            if zeq id lock_range then
              match e0 with
                | TBSHARED (BTDSLEEP slp_id cv s) ⇒
                  TEVENT cid (TSHARED (OTDSLEEP slp_id cv s)) :: nil
                | TBSHARED e1 ⇒
                  match BigE2E e1 with
                    | Some e2 ⇒ TEVENT cid e2 :: nil
                    | _ ⇒ nil
                  end
                | _ ⇒ nil
              end
            else
              match e0 with
                | TBLOCK lock_id e1 ⇒
                  if zeq id lock_id then
                    match e1 with
                      | BWAIT_LOCK _ n ⇒
                        TEVENT cid (TSHARED OPULL) :: TEVENT cid (TTICKET (WAIT_LOCK (n))) :: nil
                      | BGET_LOCK _ ⇒
                        TEVENT cid (TTICKET GET_LOCK) :: nil
                      | BREL_LOCK _ s ⇒
                        TEVENT cid (TTICKET REL_LOCK) :: TEVENT cid (TSHARED (OSCE s)) :: nil
                    end
                  else nil
                | TBSHARED (BTDSLEEP slp_id cv s) ⇒
                  let n := slp_q_id cv 0 in
                  let sc_id := n + lock_TCB_range in
                  if zeq id sc_id then
                    TEVENT cid (TTICKET REL_LOCK) ::
                           TEVENT cid (TSHARED (OSCE s)) :: nil
                  else nil
                | TBSHARED (BBUFFERE _ cv b) ⇒
                  let n := slp_q_id cv 0 in
                  let sc_id := n + lock_TCB_range in
                  if zeq id sc_id then
                    TEVENT cid (TSHARED (OBUFFERE b)) :: nil
                  else nil
                | _ ⇒ nil
              end
      end.

    Inductive BigLogMap2id: BigLog → Z → MultiLog → Prop :=
    | BIGMAP_NIL:
        ∀ id,
          BigLogMap2id nil id nil
    | BIGMAP_CONS:
        ∀ id e bl l l´
               (Hbig: BigLogMap2id bl id l)
               (Hrel_e: BigE2id e id = l´),
          BigLogMap2id (e::bl) id (l´ ++ l).

    Fixpoint remove_cache_event (l: MultiLog) (cid: Z) :=
      match l with
        | nil ⇒ nil
        | TEVENT scid e :: l´ ⇒
          if zeq scid cid then l
          else remove_cache_event l´ cid
      end.

    Context `{multi_oracle_ops: MultiOracleOps}.

    Inductive relate_big_small_log: BigLog → Z → MultiLog → Prop :=
    | RELATE_BIG_SMALL_LOG_DEF:
        ∀ bl ml abid bl0
               (Hlogmap: BigLogMap2id bl abid bl0)
               (Heq: ml = remove_cache_event bl0 current_CPU_ID),
          relate_big_small_log bl abid ml.

    Inductive relate_big_small_log_pool: BigLogType → MultiLogPool → Prop :=
    | RELATE_BIG_SMALL_LOG_POOL_UNDEF:
        ∀ ml,
          relate_big_small_log_pool BigUndef ml
    | RELATE_BIG_SMALL_LOG_POOL_DEF:
        ∀ bl ml
               (Hrel_log: ∀ abid
                                 (Habid: abid = ID_AT ∨ abid = lock_range ∨
                                         (∃ ofs, index2Z ID_SC ofs = Some abid)),
                          ∃ l, ZMap.get abid ml = MultiDef l
                                    ∧ relate_big_small_log bl abid l),
          relate_big_small_log_pool (BigDef bl) ml.

    Inductive relate_big_small_oracle: BigOracle → MultiOraclePool → Prop :=
    | RELATE_BIG_SMALL_ORACLE:
        ∀ bo o
               (Hrel: ∀ abid bl l
                             (Habid: abid = ID_AT ∨ abid = lock_range ∨
                                     (∃ ofs, index2Z ID_SC ofs = Some abid))
                             (Hrel_log: relate_big_small_log bl abid l),
                        BigLogMap2id (bo current_CPU_ID bl ++ bl) abid
                                     ((ZMap.get abid o) current_CPU_ID l ++ l)),
          relate_big_small_oracle bo o.

  End WITHMEM.

End Refinement.