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

    Definition GetID (e: MultiOracleEvent) :=
      match e with
        | TEVENT cpu (TSHARED e´) ⇒
          match e´ with
            | OTDYIELD _ ⇒ Some (msg_q_id cpu, cpu)
            | OTDSLEEP _ cv _ ⇒ Some (slp_q_id cv 0, cpu)
            | OTDWAKE cv_id ⇒ Some (slp_q_id cv_id 0, cpu)
            | OTDWAKE_DIFF _ cpu´ ⇒ Some (msg_q_id cpu´, cpu)
            | _ ⇒ None
          end
        | _ ⇒ None
      end.

    Context `{multi_oracle_ops: MultiOracleOps}.

    Inductive MultiE2id: MultiOracleEvent → MultiLog → Z → MultiLog → Prop:=
    | MultiE2idSPAWN:
        ∀ cpu l id new_id,
          MultiE2id (TEVENT cpu (TSHARED (OTDSPAWN new_id))) l id nil

    | MultiE2id_DIFF:
        ∀ e nid cpu l id,
          ∀ (Hsome: GetID e = Some (nid, cpu)) (Hneq: nid ≠ id),
            MultiE2id e l id nil

    | MultiE2id_EQ:
        ∀ e t0 q0 nid cpu l curid t q slp cache res (Hsome: GetID e = Some (nid, cpu)),
          ∀ (Hcal: CalTCB_log (e :: l) = Some (t, q, slp, curid, cache, res))
                 (Hcache: ZMap.get nid cache = Some (t0, q0)),
            MultiE2id e l nid
                      (TEVENT cpu (TTICKET REL_LOCK) ::
                              TEVENT cpu (TSHARED (OABTCBE t0 q0)) ::
                              TEVENT cpu (TSHARED OPULL) ::
                              TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) ::nil).

    Inductive MultiLogMap2id: MultiLog → Z → MultiLog → Prop :=
    | BIGMAP_NIL:
        ∀ id,
          MultiLogMap2id nil id nil
    | BIGMAP_CONS:
        ∀ e bl l l´ id
               (Hbig: MultiLogMap2id bl id l)
               (Hrel_e: MultiE2id e bl id l´),
          MultiLogMap2id (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.

    Inductive relate_Thread_Log: MultiLog → Z → MultiLog → Prop :=
    | RELATE_LOG_DEF:
        ∀ bl ml bl0 id
               (Hlogmap: MultiLogMap2id bl id bl0)
               (Heq: ml = remove_cache_event bl0 current_CPU_ID),
          relate_Thread_Log bl id ml.

    Inductive relate_Thread_Log_Type: MultiLogType → Z → MultiLogType → Prop :=
    | RELATE_ORACLE_thread_LOG_Type_UNDEF:
        ∀ id l,
          relate_Thread_Log_Type MultiUndef id l
    | RELATE_ORACLE_thread_LOG_Type:
        ∀ l1 l2 id
               (Hrel_log: relate_Thread_Log l1 id l2),
          relate_Thread_Log_Type (MultiDef l1) id (MultiDef l2).

    Inductive relate_Thread_Log_Pool: MultiLogPool → MultiLogPool → Prop :=
    | RELATE_ORACLE_thread_LOG_Pool:
        ∀ o1 o2
               (Hsame: ∀ i ofs r, i ≠ ID_TCB → index2Z i ofs = Some r →
                                       ZMap.get r o1 = ZMap.get r o2)
               (Hdiff: ∀ i, MSG_Q_START ≤ i < num_chan →
                                 relate_Thread_Log_Type (ZMap.get lock_range o1) i (ZMap.get (i + ID_AT_range) o2)),
          relate_Thread_Log_Pool o1 o2.

    Inductive relate_Thread_Oracle: MultiOracle → Z → MultiOracle → Prop :=
    | RELATE_ORACLE_thread_ORACLE:
        ∀ o1 o2 id
               (Hpre: ∀ i l1 l2
                             (Hrelate_log_pre: relate_Thread_Log l1 id l2),
                        MultiLogMap2id (o1 i l1 ++ l1) id (o2 i l2 ++ l2)),
          relate_Thread_Oracle o1 id o2.

    Inductive relate_Thread_Oracle_Pool: MultiOraclePool → MultiOraclePool → Prop :=
    | RELATE_ORACLE_thread_ORACLE_Pool:
        ∀ o1 o2
               (Hsame: ∀ i ofs r, i ≠ ID_TCB → index2Z i ofs = Some r →
                                       ZMap.get r o1 = ZMap.get r o2)
               (Hdiff: ∀ i, MSG_Q_START ≤ i < num_chan →
                                 relate_Thread_Oracle (ZMap.get lock_range o1) i (ZMap.get (i + ID_AT_range) o2)),
          relate_Thread_Oracle_Pool o1 o2.

  End WITHMEM.

End Refinement.