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 LogReplay.
Require Import RealParams.

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}.
  Context `{real_params: RealParams}.

  Inductive relate_ATH_MultiEvent: MultiOracleEvent → MultiLog → MultiLog → Prop :=
  | RELATE_ORACLE_ATH_Event_eq:
      ∀ l a i r
             (Hrelate_e: CalAT_log_real (TEVENT i (TSHARED (OPALLOCE r)) :: l) = Some a),
        relate_ATH_MultiEvent (TEVENT i (TSHARED (OPALLOCE r))) l
                              (TEVENT i (TTICKET REL_LOCK) :: TEVENT i (TSHARED (OATE a)) ::
                                      TEVENT i (TSHARED OPULL) ::
                                      TEVENT i (TTICKET (WAIT_LOCK local_lock_bound)) :: nil).

  Inductive relate_ATH_Log: MultiLog → MultiLog → Prop :=
  | RELATE_ORACLE_ATH_nil:
        relate_ATH_Log nil nil
  | RELATE_ORACLE_ATH_cons:
      ∀ l1 l2 a1 a2
             (Hrelate_log: relate_ATH_Log l1 l2)
             (Hrelate_event: relate_ATH_MultiEvent a1 l1 a2),
        relate_ATH_Log (a1::l1) (a2++l2).

  Inductive relate_ATH_Log_Type: MultiLogType → MultiLogType → Prop :=
  | RELATE_ORACLE_ATH_LOG_Type_UNDEF:
        relate_ATH_Log_Type MultiUndef MultiUndef
  | RELATE_ORACLE_ATH_LOG_Type:
      ∀ l1 l2
             (Hrelate_type: relate_ATH_Log l1 l2),
        relate_ATH_Log_Type (MultiDef l1) (MultiDef l2).

  Inductive relate_ATH_Log_Pool: MultiLogPool → MultiLogPool → Prop :=
  | RELATE_ORACLE_ATH_LOG_Pool:
      ∀ o1 o2
             (Hre_neq: ∀ i ofs r, i ≠ ID_AT → index2Z i ofs = Some r →
                                       ZMap.get r o1 = ZMap.get r o2)
             (Hrel_eq: relate_ATH_Log_Type (ZMap.get ID_AT o1) (ZMap.get ID_AT o2)),
        relate_ATH_Log_Pool o1 o2.

  Inductive relate_ATH_Oracle: MultiOracle → MultiOracle → Prop :=
  | RELATE_ORACLE_ATH_ORACLE:
      ∀ o1 o2
             (Hrel_o_log: ∀ i l1 l2
                                 (Hrelate_log_pre: relate_ATH_Log l1 l2),
                            relate_ATH_Log ((o1 i l1) ++ l1) ((o2 i l2) ++ l2)),
        relate_ATH_Oracle o1 o2.

  Inductive relate_ATH_Oracle_Pool: MultiOraclePool → MultiOraclePool → Prop :=
  | RELATE_ORACLE_ATH_ORACLE_Pool:
      ∀ o1 o2
        (Hrel_o_neq: ∀ i ofs r, i ≠ ID_AT → index2Z i ofs = Some r →
                                     ZMap.get r o1 = ZMap.get r o2)
        (Hrel_o_eq: relate_ATH_Oracle (ZMap.get ID_AT o1) (ZMap.get ID_AT o2)),
        relate_ATH_Oracle_Pool o1 o2.

End Refinement.