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

Section Refinement.

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

  Context `{real_params: RealParams}.

  Section WITHMEM.

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

    Fixpoint relate_log (l: MultiLog): option(MultiLog × list nat) :=
      match l with
        | nil ⇒ Some (nil, nil)
        | (TEVENT i e) :: l´ ⇒
          match relate_log l´ with
            | Some (ll, tq) ⇒
              match e with
                | TTICKET e´ ⇒
                  match e´ with
                    | INC_TICKET p ⇒
                      Some (ll, tq ++ (p::nil))
                    | GET_NOW ⇒
                      Some (ll, tq)
                    | HOLD_LOCK ⇒
                      match tq with
                        | p:: tq´ ⇒
                          Some ((TEVENT i (TTICKET (WAIT_LOCK p))) :: ll, tq)
                        | _ ⇒ None
                      end
                    | INC_NOW ⇒
                      match tq with
                        | _:: tq´ ⇒
                          Some ((TEVENT i (TTICKET REL_LOCK))::ll, tq´)
                        | _ ⇒ None
                      end
                    | _ ⇒ None
                  end
                | TSHARED _ ⇒
                  Some ((TEVENT i e) :: ll, tq)
              end
            | _ ⇒ None
          end
      end.

    Inductive relate_ticket_log_type: MultiLogType → MultiLogType → Prop :=
    | RELATE_TICKET_LOG_TYPE_UNDEF:
        relate_ticket_log_type MultiUndef MultiUndef
    | RELATE_TICKET_LOG_TYPE_DEF:
        ∀ l l´ tq
               (Hrelate_ticket_log: relate_log l = Some (l´, tq)),
          relate_ticket_log_type (MultiDef l´) (MultiDef l).

    Inductive relate_ticket_log_pool: MultiLogPool → MultiLogPool → Prop :=
    | RELATE_TICKET_LOG_POOL:
        ∀ l l´
               (Hrelate_ticket_log_type:
                  ∀ index ofs z
                         (Hrange: index2Z index ofs = Some z),
                    relate_ticket_log_type (ZMap.get z l) (ZMap.get z l´)),
         relate_ticket_log_pool l l´.

    Context `{waittime: WaitTime}.

    Fixpoint CalSumWait (l: list nat) :=
      match l with
        | nil ⇒ O
        | a :: l´ ⇒ (4 + a + CalSumWait l´) % nat
      end.

    Definition rm_head {A: Type} (l: list A) :=
      match l with
        | nil ⇒ nil
        | _ :: l´ ⇒ l´
      end.

    Definition CalStatus (h: head_status) :=
      match h with
        | LEMPTY ⇒ O
        | LHOLD ⇒ 1%nat
        | LGET ⇒ 2%nat
      end.

    Definition decrease_number (self_c other_c: nat) (h: head_status) (tq: list nat) :=
      match h with
        | LEMPTY ⇒ (other_c + (CalSumWait tq) × fairness) % nat
        | _ ⇒ (other_c + (self_c + CalSumWait (rm_head tq) + CalStatus h) × fairness)%nat
      end.

    Definition CalWaitTime (l: list nat) :=
      S (fairness + (CalSumWait l) × fairness).

    Inductive relate_ticket_oracle: MultiOracle → MultiOracle → Prop :=
    | RELATE_ORACLE:
        ∀ o1 o2
               (Hrelate_ticket_oracle_res:
                  ∀ i l1 l2 tq bound
                         (Hrelate_log: relate_log l2 = Some (l1, tq)),
                    let l20 := (TEVENT i (TTICKET (INC_TICKET bound))) :: o2 i l2 ++ l2 in
                    ∀ self_c other_c b q tq0 l2´
                           (HCal: Q_CalLock l20 = Some (self_c, other_c, b, q, tq0))
                           (HWait: Q_CalWait (CalWaitTime tq0) i l20 o2 = Some l2´),
                    ∃ tq´, relate_log l2´ = Some (o1 i l1 ++ l1, tq´)),
          relate_ticket_oracle o1 o2.

    Inductive relate_ticket_oracle_pool: MultiOraclePool → MultiOraclePool → Prop :=
    | RELATE_ORACLE_POOL:
        ∀ o1 o2
               (Hrelate_ticket_oracle:
                  ∀ index ofs z
                         (Hrange: index2Z index ofs = Some z),
                    relate_ticket_oracle (ZMap.get z o1) (ZMap.get z o2)),
          relate_ticket_oracle_pool o1 o2.

  End WITHMEM.

End Refinement.