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.

Section Refinement.

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

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

  Inductive abqueue_match_next_prev_rec:
    (list Z) → Z → Z → Z → Z → TCBPool → Prop :=
  | abqueue_match_nil:
      ∀ tcb starting,
        abqueue_match_next_prev_rec nil num_proc starting starting num_proc tcb
  | abqueue_match_cons:
      ∀ starting ending tcb tl t l next
             (Hvalid: ∃ st parent,
                        ZMap.get t tcb = TCBValid st parent starting next)
             (Hmatch_ind: abqueue_match_next_prev_rec l next tl t ending tcb),
        abqueue_match_next_prev_rec (t :: l) t tl starting ending tcb.

  Definition abqueue_match_dllist (abq: AbQueuePool) (tcb: TCBPool) (tdq: TDQueuePool): Prop :=
    ∀ qi l
           (Hqi_range: 0≤ qi < num_chan)
           (Hq_valid: ZMap.get qi abq = AbQValid l),
    ∃ hd tl,
      ZMap.get qi tdq = TDQValid hd tl
      ∧ abqueue_match_next_prev_rec l hd tl num_proc num_proc tcb.

  Definition abtcbpool_tcbpool (abtcb: AbTCBPool) (tcb: TCBPool) : Prop :=
    ∀ i tds inq parent
           (Hi_range: 0 ≤ i < num_proc)
           (Ht_valid: ZMap.get i abtcb = AbTCBValid tds parent inq),
    ∃ pv, ∃ nx,
                 ZMap.get i tcb = TCBValid tds parent pv nx.

  Inductive AbQ_RealQ: AbTCBPool → AbQueuePool → TCBPool → TDQueuePool → Prop:=
  | AbQ_RealQ_con :
      ∀ abtcb abq tcb tdq
             (Hq_match: abqueue_match_dllist abq tcb tdq)
             (Ht_match: abtcbpool_tcbpool abtcb tcb),
        AbQ_RealQ abtcb abq tcb tdq.

  Inductive relate_ABTCB_Event: SharedMemEvent → SharedMemEvent → Prop :=
  | RELATE_ORACLE_ABTCB_Event:
      ∀ ta qa t q
             (Hrelate_event: AbQ_RealQ ta qa t q),
        relate_ABTCB_Event (OABTCBE ta qa) (OTCBE t q).

  Inductive relate_ABTCB_MultiEvent: MultiOracleEventUnit → MultiOracleEventUnit → Prop :=
  | RELATE_ORACLE_ABTCB_Event_eq:
      ∀ ta qa t q
             (Hrelate_e: relate_ABTCB_Event (OABTCBE ta qa) (OTCBE t q)),
        relate_ABTCB_MultiEvent (TSHARED (OABTCBE ta qa)) (TSHARED (OTCBE t q))
  | RELATE_ORACLE_ABTCB_Event_neq:
      ∀ e,
        relate_ABTCB_MultiEvent (TTICKET e) (TTICKET e)
  | RELATE_ORACLE_ABTCB_Event_pull_neq:
      relate_ABTCB_MultiEvent (TSHARED OPULL) (TSHARED OPULL).

  Inductive relate_ABTCB_Log: MultiLog → MultiLog → Prop :=
  | RELATE_ORACLE_ABTCB_nil:
      relate_ABTCB_Log nil nil
  | RELATE_ORACLE_ABTCB_cons:
      ∀ l1 l2 a1 a2 i
             (Hrelate_log: relate_ABTCB_Log l1 l2)
             (Hrelate_event: relate_ABTCB_MultiEvent a1 a2),
        relate_ABTCB_Log (TEVENT i a1::l1) (TEVENT i a2::l2).

  Inductive relate_ABTCB_Log_Type: MultiLogType → MultiLogType → Prop :=
  | RELATE_ORACLE_ABTCB_LOG_Type_UNDEF:
      relate_ABTCB_Log_Type MultiUndef MultiUndef
  | RELATE_ORACLE_ABTCB_LOG_Type:
      ∀ l1 l2,
        relate_ABTCB_Log l1 l2 →
        relate_ABTCB_Log_Type (MultiDef l1) (MultiDef l2).

  Inductive relate_ABTCB_Log_Pool: MultiLogPool → MultiLogPool → Prop :=
  | RELATE_ORACLE_ABTCB_LOG_Pool:
      ∀ o1 o2,
        (∀ i ofs r, i ≠ ID_TCB → index2Z i ofs = Some r →
                         ZMap.get r o1 = ZMap.get r o2) →
        (∀ i, 0 ≤ i < num_chan →
                   relate_ABTCB_Log_Type (ZMap.get (i + ID_AT_range) o1) (ZMap.get (i + ID_AT_range) o2)) →
        relate_ABTCB_Log_Pool o1 o2.

  Inductive relate_ABTCB_Oracle: MultiOracle → MultiOracle → Prop :=
  | RELATE_ORACLE_ABTCB_ORACLE:
      ∀ o1 o2,
        (∀ i l1 l2
                (Hrelate_log_pre: relate_ABTCB_Log l1 l2),
           relate_ABTCB_Log (o1 i l1 ++ l1) (o2 i l2 ++ l2)) →
        relate_ABTCB_Oracle o1 o2.

  Inductive relate_ABTCB_Oracle_Pool: MultiOraclePool → MultiOraclePool → Prop :=
  | RELATE_ORACLE_ABTCB_ORACLE_Pool:
      ∀ o1 o2,
        (∀ i ofs r, i ≠ ID_TCB → index2Z i ofs = Some r →
                         ZMap.get r o1 = ZMap.get r o2) →
        (∀ i, 0 ≤ i < num_chan →
                   relate_ABTCB_Oracle (ZMap.get (i + ID_AT_range) o1) (ZMap.get (i + ID_AT_range) o2)) →
        relate_ABTCB_Oracle_Pool o1 o2.

End Refinement.