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 match_TCB: TCB → val → val → val → val→ Prop :=
  | MATCH_TCBUNDEF:
      match_TCB TCBUndef Vzero Vzero Vzero Vzero
  | MATCH_TCBVALID:
      ∀ v1 v2 v3 v4 ts
             (Hzs: ZtoThreadState (Int.unsigned v1) = Some ts),
        match_TCB (TCBValid ts (Int.unsigned v2) (Int.unsigned v3) (Int.unsigned v4))
                  (Vint v1) (Vint v2) (Vint v3) (Vint v4).

  Inductive match_TCBPool: block → TCBPool → mem → Prop :=
  | MATCH_TCBPOOL:
      ∀ tcb m b
             (Hmatch_TCB:
                ∀ ofs
                       (Hofs: 0≤ ofs < num_proc),
                  (∃ v1 v2 v3 v4,
                     Mem.load Mint32 m b (ofs × 16) = Some v1 ∧
                     Mem.valid_access m Mint32 b (ofs × 16) Writable ∧
                     Mem.load Mint32 m b (ofs × 16 + 4) = Some v2 ∧
                     Mem.valid_access m Mint32 b (ofs × 16 + 4) Writable ∧
                     Mem.load Mint32 m b (ofs × 16 + 8) = Some v3 ∧
                     Mem.valid_access m Mint32 b (ofs × 16 + 8) Writable ∧
                     Mem.load Mint32 m b (ofs × 16 + 12) = Some v4 ∧
                     Mem.valid_access m Mint32 b (ofs × 16 + 12) Writable ∧
                     match_TCB (ZMap.get ofs tcb) v1 v2 v3 v4)),
        match_TCBPool b tcb m.

  Inductive match_TDQ: TDQueue → val → val→ Prop :=
  | MATCH_TDQUNDEF:
      match_TDQ TDQUndef Vzero Vzero
  | MATCH_TDQVALID:
      ∀ v1 v2,
        match_TDQ (TDQValid (Int.unsigned v1) (Int.unsigned v2)) (Vint v1) (Vint v2).

  Inductive match_TDQPool: block → TDQueuePool → mem → Prop :=
  | MATCH_TDQPOOL:
      ∀ tdqp m b
             (Hmatch_TDQ:
                ∀ ofs
                       (Hofs: 0≤ ofs < num_chan),
                  (∃ v1 v2,
                     Mem.load Mint32 m b (ofs × 8 + num_proc × 16) = Some v1 ∧
                     Mem.valid_access m Mint32 b (ofs × 8 + num_proc × 16) Writable ∧
                     Mem.load Mint32 m b (ofs × 8 + 4 + num_proc × 16) = Some v2 ∧
                     Mem.valid_access m Mint32 b (ofs × 8 + 4 + num_proc × 16) Writable ∧
                     match_TDQ (ZMap.get ofs tdqp) v1 v2)),
        match_TDQPool b tdqp m.

  Inductive relate_TCB_Event: stencil → SharedMemEvent → SharedMemEvent → Prop :=
  | RELATE_ORACLE_TCB_Event:
      ∀ s l tb tq b,
        find_symbol s TCBPool_LOC = Some b →
        (∀ m m´, Mem.storebytes m b 0 (ByteList l) = Some m´ →
                      match_TCBPool b tb m´
                      ∧ match_TDQPool b tq m´) →
        Z_of_nat (length (ByteList l)) = num_proc × 16 + num_chan × 8 →
        relate_TCB_Event s (OTCBE tb tq) (OMEME l).

  Inductive relate_TCB_MultiEvent: stencil → MultiOracleEventUnit → MultiOracleEventUnit → Prop :=
  | RELATE_ORACLE_TCB_Event_eq:
      ∀ s l tb tq
             (Hrelate_e: relate_TCB_Event s (OTCBE tb tq) (OMEME l)),
        relate_TCB_MultiEvent s (TSHARED (OTCBE tb tq)) (TSHARED (OMEME l))
  | RELATE_ORACLE_TCB_Event_neq:
      ∀ s e,
        relate_TCB_MultiEvent s (TTICKET e) (TTICKET e)
  | RELATE_ORACLE_TCB_Event_pull_neq:
      ∀ s,
        relate_TCB_MultiEvent s (TSHARED OPULL) (TSHARED OPULL).

  Inductive relate_TCB_Log: stencil → MultiLog → MultiLog → Prop :=
  | RELATE_ORACLE_TCB_nil:
      ∀ s,
        relate_TCB_Log s nil nil
  | RELATE_ORACLE_TCB_cons:
      ∀ s l1 l2 a1 a2 i
             (Hrelate_log: relate_TCB_Log s l1 l2)
             (Hrelate_event: relate_TCB_MultiEvent s a1 a2),
        relate_TCB_Log s (TEVENT i a1::l1) (TEVENT i a2::l2).

  Inductive relate_TCB_Log_Type: stencil → MultiLogType → MultiLogType → Prop :=
  | RELATE_ORACLE_TCB_LOG_Type_UNDEF:
      ∀ s,
        relate_TCB_Log_Type s MultiUndef MultiUndef
  | RELATE_ORACLE_TCB_LOG_Type:
      ∀ s l1 l2,
        relate_TCB_Log s l1 l2 →
        relate_TCB_Log_Type s (MultiDef l1) (MultiDef l2).

  Inductive relate_TCB_Log_Pool: stencil → MultiLogPool → MultiLogPool → Prop :=
  | RELATE_ORACLE_TCB_LOG_Pool:
      ∀ s 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_TCB_Log_Type s (ZMap.get (i + ID_AT_range) o1) (ZMap.get (i + ID_AT_range) o2)) →
        relate_TCB_Log_Pool s o1 o2.

  Inductive relate_TCB_Oracle: stencil → MultiOracle → MultiOracle → Prop :=
  | RELATE_ORACLE_TCB_ORACLE:
      ∀ o1 o2 s,
        (∀ i l1 l2
                (Hrelate_log_pre: relate_TCB_Log s l1 l2),
           relate_TCB_Log s (o1 i l1) (o2 i l2)) →
        relate_TCB_Oracle s o1 o2.

  Inductive relate_TCB_Oracle_Pool: stencil → MultiOraclePool → MultiOraclePool → Prop :=
  | RELATE_ORACLE_TCB_ORACLE_Pool:
      ∀ s 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_TCB_Oracle s (ZMap.get (i + ID_AT_range) o1) (ZMap.get (i + ID_AT_range) o2)) →
        relate_TCB_Oracle_Pool s o1 o2.

End Refinement.