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_AT_info: ATInfo → val → val → Prop :=
  | MATCH_ATINFO_UNDEF: match_AT_info ATUndef Vzero Vzero
  | MATCH_ATINFO_VALID: ∀ u z t b,
                          ZtoATType (Int.unsigned z) = Some t →
                          ZtoBool u = Some b →
                          match_AT_info (ATValid b t)
                                        (Vint (Int.repr u)) (Vint z).

  Inductive match_AT: stencil → ATable → mem → Prop :=
  | MATCH_AT: ∀ AT m b s,
                (∀ ofs, 0≤ ofs < maxpage →
                             (∃ v1 v2,
                                Mem.load Mint32 m b (ofs × 8) = Some v1 ∧
                                Mem.load Mint32 m b (ofs × 8 + 4) = Some v2 ∧
                                Mem.valid_access m Mint32 b (ofs × 8) Writable ∧
                                Mem.valid_access m Mint32 b (ofs × 8 + 4) Writable ∧
                                match_AT_info (ZMap.get ofs AT) v2 v1))
                → find_symbol s AT_LOC = Some b
                → match_AT s AT m.

  Inductive relate_AT_Event: stencil → SharedMemEvent → SharedMemEvent → Prop :=
  | RELATE_ORACLE_AT_Event:
      ∀ s l a b,
        find_symbol s AT_LOC = Some b →
        (∀ m m´, Mem.storebytes m b 0 (ByteList l) = Some m´ →
                      match_AT s a m´) →
        Z_of_nat (length (ByteList l)) = maxpage × 8 →
        relate_AT_Event s (OATE a) (OMEME l).

  Inductive relate_AT_MultiEvent: stencil → MultiOracleEventUnit → MultiOracleEventUnit → Prop :=
  | RELATE_ORACLE_AT_Event_eq:
      ∀ s l a
        (Hrelate_e: relate_AT_Event s (OATE a) (OMEME l)),
        relate_AT_MultiEvent s (TSHARED (OATE a)) (TSHARED (OMEME l))
  | RELATE_ORACLE_AT_Event_neq:
      ∀ s e,
        relate_AT_MultiEvent s (TTICKET e) (TTICKET e)
  | RELATE_ORACLE_AT_Event_pull_neq:
      ∀ s,
        relate_AT_MultiEvent s (TSHARED OPULL) (TSHARED OPULL).

  Inductive relate_AT_Log: stencil → MultiLog → MultiLog → Prop :=
  | RELATE_ORACLE_AT_nil:
      ∀ s,
        relate_AT_Log s nil nil
  | RELATE_ORACLE_AT_cons:
      ∀ s l1 l2 a1 a2 i
             (Hrelate_log: relate_AT_Log s l1 l2)
             (Hrelate_event: relate_AT_MultiEvent s a1 a2),
        relate_AT_Log s (TEVENT i a1::l1) (TEVENT i a2::l2).

  Inductive relate_AT_Log_Type: stencil → MultiLogType → MultiLogType → Prop :=
  | RELATE_ORACLE_AT_LOG_Type_UNDEF:
      ∀ s,
        relate_AT_Log_Type s MultiUndef MultiUndef
  | RELATE_ORACLE_AT_LOG_Type:
      ∀ s l1 l2,
        relate_AT_Log s l1 l2 →
        relate_AT_Log_Type s (MultiDef l1) (MultiDef l2).

  Inductive relate_AT_Log_Pool: stencil → MultiLogPool → MultiLogPool → Prop :=
  | RELATE_ORACLE_AT_LOG_Pool:
      ∀ s o1 o2,
        (∀ i ofs r, i ≠ ID_AT → index2Z i ofs = Some r →
                         ZMap.get r o1 = ZMap.get r o2) →
        relate_AT_Log_Type s (ZMap.get ID_AT o1) (ZMap.get ID_AT o2) →
        relate_AT_Log_Pool s o1 o2.

  Inductive relate_AT_Oracle: stencil → MultiOracle → MultiOracle → Prop :=
  | RELATE_ORACLE_AT_ORACLE:
      ∀ o1 o2 s,
        (∀ i l1 l2
                (Hrelate_log_pre: relate_AT_Log s l1 l2),
           relate_AT_Log s (o1 i l1) (o2 i l2)) →
        relate_AT_Oracle s o1 o2.

  Inductive relate_AT_Oracle_Pool: stencil → MultiOraclePool → MultiOraclePool → Prop :=
  | RELATE_ORACLE_AT_ORACLE_Pool:
      ∀ s o1 o2,
        (∀ i ofs r, i ≠ ID_AT → index2Z i ofs = Some r →
                         ZMap.get r o1 = ZMap.get r o2) →
        relate_AT_Oracle s (ZMap.get ID_AT o1) (ZMap.get ID_AT o2) →
        relate_AT_Oracle_Pool s o1 o2.

End Refinement.