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_Chan: SyncChannel → val → val → val → val → Prop :=
  | MATCH_CHANUNDEF:
      match_Chan SyncChanUndef Vzero Vzero Vzero Vzero
  | MATCH_CHANVALID:
      ∀ v1 v2 v3 v4,
        match_Chan (SyncChanValid v1 v2 v3 v4) (Vint v1) (Vint v2) (Vint v3) (Vint v4).

  Inductive match_ChanPool: stencil → SyncChanPool → mem → Prop :=
  | MATCH_CHANPOOL:
      ∀ chp m b s,
        (∀ ofs,
           0≤ ofs < num_chan →
           (∃ 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_Chan (ZMap.get ofs chp) v1 v2 v3 v4))
        → find_symbol s SYNCCHPOOL_LOC = Some b
        → match_ChanPool s chp m.

  Inductive relate_SC_Event: stencil → SharedMemEvent → SharedMemEvent → Prop :=
  | RELATE_ORACLE_SC_Event:
      ∀ s l sc b,
        find_symbol s SYNCCHPOOL_LOC = Some b →
        (∀ m m´, Mem.storebytes m b 0 (ByteList l) = Some m´ →
                      match_ChanPool s sc m´) →
        Z_of_nat (length (ByteList l)) = num_chan × 16 →
        relate_SC_Event s (OSCE sc) (OMEME l).

  Inductive relate_SC_MultiEvent: stencil → MultiOracleEventUnit → MultiOracleEventUnit → Prop :=
  | RELATE_ORACLE_SC_Event_eq:
      ∀ s l sc
             (Hrelate_e: relate_SC_Event s (OSCE sc) (OMEME l)),
        relate_SC_MultiEvent s (TSHARED (OSCE sc)) (TSHARED (OMEME l))
  | RELATE_ORACLE_SC_Event_neq:
      ∀ s e,
        relate_SC_MultiEvent s (TTICKET e) (TTICKET e)
  | RELATE_ORACLE_SC_Event_pull_neq:
      ∀ s,
        relate_SC_MultiEvent s (TSHARED OPULL) (TSHARED OPULL)
  | RELATE_ORACLE_SC_Event_buffer_neq:
      ∀ s b,
        relate_SC_MultiEvent s (TSHARED (OBUFFERE b)) (TSHARED (OBUFFERE b)).

  Inductive relate_SC_Log: stencil → MultiLog → MultiLog → Prop :=
  | RELATE_ORACLE_SC_nil:
      ∀ s,
        relate_SC_Log s nil nil
  | RELATE_ORACLE_SC_cons:
      ∀ s l1 l2 a1 a2 i
             (Hrelate_log: relate_SC_Log s l1 l2)
             (Hrelate_event: relate_SC_MultiEvent s a1 a2),
        relate_SC_Log s (TEVENT i a1::l1) (TEVENT i a2::l2).

  Inductive relate_SC_Log_Type: stencil → MultiLogType → MultiLogType → Prop :=
  | RELATE_ORACLE_SC_LOG_Type_UNDEF:
      ∀ s,
        relate_SC_Log_Type s MultiUndef MultiUndef
  | RELATE_ORACLE_SC_LOG_Type:
      ∀ s l1 l2,
        relate_SC_Log s l1 l2 →
        relate_SC_Log_Type s (MultiDef l1) (MultiDef l2).

  Inductive relate_SC_Log_Pool: stencil → MultiLogPool → MultiLogPool → Prop :=
  | RELATE_ORACLE_SC_LOG_Pool:
      ∀ s o1 o2,
        (∀ i ofs r, i ≠ ID_SC → index2Z i ofs = Some r →
                         ZMap.get r o1 = ZMap.get r o2) →
        (∀ i, 0 ≤ i < num_chan →
                   relate_SC_Log_Type s (ZMap.get (i + lock_TCB_range) o1) (ZMap.get (i + lock_TCB_range) o2)) →
        relate_SC_Log_Pool s o1 o2.

  Inductive relate_SC_Oracle: stencil → MultiOracle → MultiOracle → Prop :=
  | RELATE_ORACLE_SC_ORACLE:
      ∀ o1 o2 s,
        (∀ i l1 l2
                (Hrelate_log_pre: relate_SC_Log s l1 l2),
           relate_SC_Log s (o1 i l1) (o2 i l2)) →
        relate_SC_Oracle s o1 o2.

  Inductive relate_SC_Oracle_Pool: stencil → MultiOraclePool → MultiOraclePool → Prop :=
  | RELATE_ORACLE_SC_ORACLE_Pool:
      ∀ s o1 o2,
        (∀ i ofs r, i ≠ ID_SC → index2Z i ofs = Some r →
                         ZMap.get r o1 = ZMap.get r o2) →
        (∀ i, 0 ≤ i < num_chan →
                   relate_SC_Oracle s (ZMap.get (i + lock_TCB_range) o1) (ZMap.get (i + lock_TCB_range) o2)) →
        relate_SC_Oracle_Pool s o1 o2.

End Refinement.