Library mcertikos.objects.LogReplay

Require Import Coqlib.
Require Import Maps.
Require Import AuxStateDataType.
Require Import FlatMemory.
Require Import Values.
Require Import Memory.
Require Import AuxLemma.
Require Import Constant.
Require Import GlobIdent.
Require Import GlobalOracle.

Section Cal_TICKET_LOCK.

  Inductive SharedPieceStatus :=
  | FreeToPull
  | PullBy (i: Z).

  Fixpoint CalValidBit (l: MultiLog):=
    match l with
      | nil ⇒ Some FreeToPull
      | (TEVENT c e) :: l´ ⇒
        match CalValidBit l´ with
          | Some FreeToPull ⇒
            match e with
              | TSHARED OPULL ⇒
                Some (PullBy c)
              | TSHARED (OMEME _) ⇒
                None
              | _ ⇒ Some FreeToPull
            end
          | Some (PullBy i) ⇒
            match e with
              | TSHARED (OMEME _) ⇒
                if zeq i c then
                  Some FreeToPull
                else None
              | TSHARED OPULL ⇒
                None
              | _ ⇒ Some (PullBy i)
            end
          | _ ⇒ None
        end
    end.

  Fixpoint CalTicketLock (l: MultiLog):=
    match l with
      | nil ⇒ Some (0, 0, nil)
      | (TEVENT _ e) :: l´ ⇒
        match CalTicketLock l´ with
          | Some (t´, n´, q) ⇒
            match e with
              | TTICKET e´ ⇒
                match e´ with
                  | INC_TICKET p ⇒ Some (t´ + 1, n´, q ++ (p::nil))
                  | INC_NOW ⇒
                    match q with
                      | _ :: q´ ⇒
                        Some (t´, n´ + 1, q´)
                      | _ ⇒ Some (t´, n´ + 1, nil)
                    end
                  | GET_NOW ⇒ Some (t´, n´, q)
                  | HOLD_LOCK ⇒ Some (t´, n´, q)
                  
                  | _ ⇒ None
                end
              | _ ⇒ Some (t´, n´, q)
            end
          | _ ⇒ None
        end
    end.

  Global Opaque CalTicketLock.

  Fixpoint CalTicketWait (n: nat) (i t: Z) (l: MultiLog) (to: MultiOracle):=
    match n with
      | O ⇒ None
      | S n´ ⇒
        let l´ := (TEVENT i (TTICKET GET_NOW)) :: (to i l) ++ l in
        match CalTicketLock l´ with
          | Some (_, n0, _) ⇒
            if zeq t n0 then Some l´
            else
              CalTicketWait n´ i t l´ to
          | _ ⇒ None
        end
    end.

  Global Opaque CalTicketWait.

  Require Import Integers.
  Fixpoint CalTicketLockWraparound (l: MultiLog):=
    match l with
      | nil ⇒ Some (0, 0, nil)
      | (TEVENT _ e) :: l´ ⇒
        match CalTicketLockWraparound l´ with
          | Some (t´, n´, q) ⇒
            match e with
              | TTICKET e´ ⇒
                match e´ with
                  | INC_TICKET p ⇒ Some (Int.unsigned (Int.repr (t´ + 1)), Int.unsigned (Int.repr n´), q ++ (p::nil))
                  | INC_NOW ⇒
                    match q with
                      | _ :: q´ ⇒
                        Some (Int.unsigned (Int.repr t´), Int.unsigned (Int.repr (n´ + 1)), q´)
                      | _ ⇒ Some (Int.unsigned (Int.repr t´), Int.unsigned (Int.repr (n´ + 1)), nil)
                    end
                  | GET_NOW ⇒ Some (Int.unsigned (Int.repr t´), Int.unsigned (Int.repr n´), q)
                  | HOLD_LOCK ⇒ Some (Int.unsigned (Int.repr t´), Int.unsigned (Int.repr n´), q)
                  | _ ⇒ None
                end
              | _ ⇒ Some (Int.unsigned (Int.repr t´), Int.unsigned (Int.repr n´), q)
            end
          | _ ⇒ None
        end
    end.

  Fixpoint CalTicketWaitWraparound (n: nat) (i t: Z) (l: MultiLog) (to: MultiOracle):=
    match n with
      | O ⇒ None
      | S n´ ⇒
        let l´ := (TEVENT i (TTICKET GET_NOW)) :: (to i l) ++ l in
        match CalTicketLockWraparound l´ with
          | Some (_, n0, _) ⇒
            if zeq t n0 then Some l´
            else
              CalTicketWaitWraparound n´ i t l´ to
          | _ ⇒ None
        end
    end.

  Context `{waittime: WaitTime}.

  Fixpoint Q_CalTicketLock (l: MultiLog) :=
    match l with
      | nil ⇒ Some (0, O, fairness, LEMPTY, nil, nil)
      | (TEVENT i e) :: l´ ⇒
        match Q_CalTicketLock l´ with
          | Some (n, self_c, other_c, b, q, tq) ⇒
            match q, tq with
              | nil, nil ⇒
                match e with
                  | TTICKET (INC_TICKET p) ⇒
                    Some (n, self_c, other_c, LEMPTY, i :: nil, p :: nil)
                  | _ ⇒ None
                end
              | i0 :: q´, p0:: tq´ ⇒
                if zeq i i0 then
                  match b with
                    | LEMPTY ⇒
                      match e with
                        | TTICKET (GET_NOW) ⇒
                          Some (n, p0, fairness, LGET, q, tq)
                        | _ ⇒ None
                      end
                    | LGET ⇒
                      match e with
                        | TTICKET (HOLD_LOCK) ⇒
                          Some (n, self_c, fairness, LHOLD, q, tq)
                        | _ ⇒ None
                      end
                    | LHOLD ⇒
                      match e with
                        | TTICKET (INC_NOW) ⇒
                          Some (n + 1, O, fairness, LEMPTY, q´, tq´)
                        | TSHARED _ ⇒
                          match self_c with
                            | O ⇒ None
                            | S self_c´ ⇒
                              Some (n, self_c´, fairness, LHOLD, q, tq)
                          end
                        | _ ⇒ None
                      end
                  end
                else
                  match other_c with
                    | O ⇒ None
                    | S other_c´ ⇒
                      match e with
                        | TTICKET e´ ⇒
                          match e´ with
                            | INC_TICKET p ⇒
                              if in_dec zeq i q´ then None
                              else Some (n, self_c, other_c´, b, q ++ (i::nil), tq++(p::nil))
                            | GET_NOW ⇒
                              Some (n, self_c, other_c´, b, q, tq)
                            | _ ⇒ None
                          end
                        | _ ⇒ None
                      end
                  end
              | _, _ ⇒ None
            end
          | _ ⇒ None
        end
    end.


  Global Opaque Q_CalTicketLock.

  Fixpoint Q_CalTicketWait (n: nat) (i: Z) (l: MultiLog) (to: MultiOracle):=
    match n with
      | O ⇒ None
      | S n´ ⇒
        let l´ := (TEVENT i (TTICKET GET_NOW)) :: (to i l) ++ l in
        match Q_CalTicketLock l´ with
          | Some (n0, self_c, other_c, b, q, tq) ⇒
            match q with
              | e0 :: q´ ⇒
                if (zeq e0 i) then Some l´
                else Q_CalTicketWait n´ i l´ to
              | _ ⇒ None
            end
          | _ ⇒ None
        end
    end.

  Global Opaque Q_CalTicketWait.

  Fixpoint Q_CalLock (l: MultiLog) :=
    match l with
      | nil ⇒ Some (O, fairness, LEMPTY, nil, nil)
      | (TEVENT i e) :: l´ ⇒
        match Q_CalLock l´ with
          | Some (self_c, other_c, b, q, tq) ⇒
            match q, tq with
              | nil, nil ⇒
                match e with
                  | TTICKET (INC_TICKET p) ⇒
                    Some (self_c, other_c, LEMPTY, i :: nil, p :: nil)
                  | _ ⇒ None
                end
              | i0 :: q´, p0:: tq´ ⇒
                if zeq i i0 then
                  match b with
                    | LEMPTY ⇒
                      match e with
                        | TTICKET (GET_NOW) ⇒
                          Some (p0, fairness, LGET, q, tq)
                        | _ ⇒ None
                      end
                    | LGET ⇒
                      match e with
                        | TTICKET (HOLD_LOCK) ⇒
                          Some (self_c, fairness, LHOLD, q, tq)
                        | _ ⇒ None
                      end
                    | LHOLD ⇒
                      match e with
                        | TTICKET (INC_NOW) ⇒
                          Some (O, fairness, LEMPTY, q´, tq´)
                        | TSHARED _ ⇒
                          match self_c with
                            | O ⇒ None
                            | S self_c´ ⇒
                              Some (self_c´, fairness, LHOLD, q, tq)
                          end
                        | _ ⇒ None
                      end
                  end
                else
                  match other_c with
                    | O ⇒ None
                    | S other_c´ ⇒
                      match e with
                        | TTICKET e´ ⇒
                          match e´ with
                            | INC_TICKET p ⇒
                              if in_dec zeq i q´ then None
                              else Some (self_c, other_c´, b, q ++ (i::nil), tq++(p::nil))
                            | GET_NOW ⇒
                              Some (self_c, other_c´, b, q, tq)
                            | _ ⇒ None
                          end
                        | _ ⇒ None
                      end
                  end
              | _, _ ⇒ None
            end
          | _ ⇒ None
        end
    end.

  Global Opaque Q_CalLock.

  Fixpoint Q_CalWait (n: nat) (i: Z) (l: MultiLog) (to: MultiOracle):=
    match n with
      | O ⇒ None
      | S n´ ⇒
        let l´ := (TEVENT i (TTICKET GET_NOW)) :: (to i l) ++ l in
        match Q_CalLock l´ with
          | Some (self_c, other_c, b, q, tq) ⇒
            match q with
              | e0 :: q´ ⇒
                if (zeq e0 i) then Some l´
                else Q_CalWait n´ i l´ to
              | _ ⇒ None
            end
          | _ ⇒ None
        end
    end.

  Global Opaque Q_CalWait.

  Fixpoint H_CalLock (l: MultiLog) :=
    match l with
      | nil ⇒ Some (O, LEMPTY, None)
      | (TEVENT i e) :: l´ ⇒
        match H_CalLock l´ with
          | Some (self_c, LHOLD, Some i0) ⇒
            if zeq i i0 then
              match e with
                | TTICKET REL_LOCK ⇒
                  Some (O, LEMPTY, None)
                | TSHARED _ ⇒
                  match self_c with
                    | O ⇒ None
                    | S self_c´ ⇒
                      Some (self_c´, LHOLD, Some i0)
                  end
                | _ ⇒ None
              end
            else None
          | Some (_, LEMPTY, None) ⇒
            match e with
              | TTICKET (WAIT_LOCK n) ⇒
                Some (n, LHOLD, Some i)
              | _ ⇒ None
            end
          | _ ⇒ None
        end
    end.

  Global Opaque H_CalLock.

End Cal_TICKET_LOCK.


Section CAL_AT.

  Require Import RealParams.
  Context `{real_params: RealParams}.

  Fixpoint CalAT_log (l: MultiLog) (a: ATable) :=
    match l with
      | nil ⇒ Some a
      | (TEVENT _ e) :: l´ ⇒
        match CalAT_log l´ a with
          | Some a´ ⇒
            match e with
              | TSHARED (OPALLOCE i) ⇒
                if zeq i 0 then Some a´
                else
                  match ZMap.get i a´ with
                    | ATValid false ATNorm ⇒
                      Some (ZMap.set i (ATValid true ATNorm) a´)
                    | _ ⇒ None
                  end
              | _ ⇒ None
            end
          | _ ⇒ None
        end
    end.

  Definition CalAT_log_real (l: MultiLog) :=
    CalAT_log l (real_AT (ZMap.init ATUndef)).

End CAL_AT.

Section CAL_TCB.

  Require Import CalRealProcModule.

  Inductive TCB_RES :=
  | TCB_NORES
  | TCB_RID (run_id: Z)
  | TCB_YIELD (run_id: Z) (msg: option Z)
  | TCBWAKE_F
  | TCBWAKE_T (wk_id: Z)
  | TCBWAKE (wk_id cpu_id: Z).

  Context`{oracle_ops: MultiOracleOps}.

  Fixpoint CalTCB_split_log (l: MultiLog) (t: AbTCBPool) (q: AbQueuePool) (slp: Z) (cid: Z)
           (cache: ZMap.t (option (prod AbTCBPool AbQueuePool))):=
    match l with
      | nil ⇒ Some (t, q, slp, cid, cache, TCB_NORES)
      | (TEVENT cpu e) :: l´ ⇒
        let rdyq := rdy_q_id cpu in
        match CalTCB_split_log l´ t q slp cid cache with
          | Some (t´, q´, slp´, cid´, cache´, res´) ⇒
            match e with
              | TSHARED (OTDSPAWN new_id) ⇒
                match (ZMap.get rdyq q´, ZMap.get new_id t´) with
                  | (AbQValid l, AbTCBValid _ _ (-1)) ⇒
                    let (rt, rq) := if zeq cpu current_CPU_ID then
                                      (ZMap.set new_id (AbTCBValid READY cpu rdyq) t´,
                                       ZMap.set rdyq (AbQValid (l++ (new_id :: nil))) q´)
                                    else (t´, q´) in
                    Some (rt, rq, slp´, cid´, cache´, TCB_NORES)
                  | _ ⇒ None
                end
              | TSHARED (OTDSLEEP _ cv _ ) ⇒
                let slpq := slp_q_id cv 0 in
                let (nt, nq) := match ZMap.get slpq cache´ with
                                  | Some (t0, q0) ⇒ (t0, q0)
                                  | _ ⇒ (t´, q´)
                                end in
                match (ZMap.get slpq nq, ZMap.get rdyq nq) with
                  | (AbQValid l0, AbQValid (nextt :: l)) ⇒
                    match (ZMap.get cid´ nt, ZMap.get nextt nt) with
                      | (AbTCBValid RUN cpu_t b, AbTCBValid READY cpu_t´ q_id) ⇒
                        if zeq cpu_t cpu then
                          if zeq b (-1) then
                            if zeq cpu_t´ cpu then
                              if zeq q_id rdyq then
                                if zeq nextt cid´ then None
                                else
                                  let n := slp´ + 1 in
                                  if zlt_lt 0 n num_proc then
                                    let cache_t := ZMap.set cid´ (AbTCBValid RUN cpu slpq) nt in
                                    let cache_q := ZMap.set slpq (AbQValid (l0 ++ (cid´::nil))) nq in
                                    let (rt, rq) :=
                                        if zeq cpu current_CPU_ID then
                                          (ZMap.set nextt (AbTCBValid RUN cpu (-1))
                                                    (ZMap.set cid´ (AbTCBValid SLEEP cpu slpq) nt),
                                           ZMap.set rdyq (AbQValid l)
                                                    (ZMap.set slpq (AbQValid (l0 ++ (cid´::nil))) nq))
                                        else (t´, q´) in
                                    let (rslp, rcid) := if zeq cpu current_CPU_ID then (n, nextt) else (slp´, cid´) in
                                    Some (rt, rq, rslp, rcid,
                                          ZMap.set slpq (Some (cache_t, cache_q)) cache´,
                                          TCB_RID nextt)
                                  else None
                              else None
                            else None
                          else None
                        else None
                      | _ ⇒ None
                    end
                  | _ ⇒ None
                end
              | TSHARED (OTDWAKE cv_id) ⇒
                let n := slp_q_id cv_id 0 in
                let (nt, nq) := match ZMap.get n cache´ with
                                  | Some (t0, q0) ⇒ (t0, q0)
                                  | _ ⇒ (t´, q´)
                                end in
                match (ZMap.get n nq) with
                  | AbQValid ll ⇒
                    match ll with
                      | nil ⇒
                        let (rt, rq) := if zeq cpu current_CPU_ID then (nt, nq) else (t´, q´) in
                        Some (rt, rq, slp´, cid´, ZMap.set n (Some (nt, nq)) cache´, TCBWAKE_F)
                      | la :: l ⇒
                        if zle_lt 0 la num_proc then
                          match (ZMap.get la nt) with
                            | AbTCBValid tds cpu´ _ ⇒
                              if zeq cpu cpu´ then
                                match ZMap.get rdyq nq with
                                  | AbQValid l0 ⇒
                                    let cache_t := (ZMap.set la (AbTCBValid tds cpu (-1)) nt): AbTCBPool in
                                    let cache_q := (ZMap.set n (AbQValid l) nq): AbQueuePool in
                                    let (rt, rq) :=
                                        (if zeq cpu current_CPU_ID then
                                          (ZMap.set la (AbTCBValid READY cpu rdyq) nt,
                                           ZMap.set rdyq (AbQValid (l0 ++ (la :: nil)))
                                                    (ZMap.set n (AbQValid l) nq))
                                        else (t´, q´)) : (prod AbTCBPool AbQueuePool) in
                                    Some (rt, rq, slp´, cid´,
                                          ZMap.set n (Some (cache_t, cache_q)) cache´,
                                          TCBWAKE_T la)
                                  | _ ⇒ None
                                end
                              else
                                if zle_lt 0 cpu´ 8 then
                                  let cache_t := ZMap.set la (AbTCBValid tds cpu´ (-1)) nt in
                                  let cache_q := ZMap.set n (AbQValid l) nq in
                                  let (rt, rq) := if zeq cpu current_CPU_ID then (cache_t, cache_q) else (t´, q´) in
                                  Some (rt, rq, slp´, cid´,
                                        ZMap.set n (Some (cache_t, cache_q)) cache´, TCBWAKE la cpu´)
                                else None
                            | _ ⇒ None
                          end
                        else None
                    end
                  | _ ⇒ None
                end
              | TSHARED (OTDWAKE_DIFF la cpu´) ⇒
                let msgq := msg_q_id cpu´ in
                let (nt, nq) := match ZMap.get msgq cache´ with
                                  | Some (t0, q0) ⇒ (t0, q0)
                                  | _ ⇒ (t´, q´)
                                end in
                match ZMap.get msgq nq, ZMap.get la nt with
                  | AbQValid l0, AbTCBValid tds0 cpu0 b ⇒
                    if zeq cpu0 cpu´ then
                      if zeq b (-1) then
                        let cache_t := ZMap.set la (AbTCBValid tds0 cpu´ msgq) nt in
                        let cache_q := ZMap.set msgq (AbQValid (l0 ++ (la :: nil))) nq in
                        let (rt, rq) :=
                            if zeq cpu current_CPU_ID then
                              (ZMap.set la (AbTCBValid tds0 cpu´ msgq) nt, cache_q)
                            else (t´, q´) in
                        Some (rt, rq, slp´, cid´, ZMap.set msgq (Some (cache_t, cache_q)) cache´, TCB_NORES)
                      else None
                    else None
                  | _,_ ⇒ None
                end
              | TSHARED (OTDYIELD _) ⇒
                let msgq := msg_q_id cpu in
                let (nt, nq) := match ZMap.get msgq cache´ with
                                  | Some (t0, q0) ⇒ (t0, q0)
                                  | _ ⇒ (t´, q´)
                                end in
                match (ZMap.get msgq nq) with
                  | AbQValid ll ⇒
                    match ll with
                      | nil ⇒
                        match ZMap.get rdyq nq, ZMap.get cid´ nt with
                          | AbQValid (la0 :: l0), AbTCBValid RUN cpu_t q_id ⇒
                            if zeq cpu_t cpu then
                              if zeq q_id (-1) then
                                match ZMap.get la0 nt with
                                  | AbTCBValid _ cpu_t´ _ ⇒
                                    if zeq cpu_t´ cpu then
                                      let (rt, rq) :=
                                          if zeq cpu current_CPU_ID then
                                            (ZMap.set la0 (AbTCBValid RUN cpu (-1))
                                                      (ZMap.set cid´ (AbTCBValid READY cpu rdyq) nt),
                                             ZMap.set rdyq (AbQValid (l0 ++ (cid´::nil))) nq)
                                          else (t´, q´) in
                                      let rcid := if zeq cpu current_CPU_ID then la0 else cid´ in
                                      Some (rt, rq, slp´, rcid, ZMap.set msgq (Some (nt, nq)) cache´,
                                            TCB_YIELD la0 None)
                                    else None
                                  | _ ⇒ None
                                end
                              else None
                            else None
                          | _,_ ⇒ None
                        end
                      | la :: l ⇒
                        if zle_lt 0 la num_proc then
                          if zeq la cid´ then None
                          else
                            match ZMap.get rdyq nq, ZMap.get la nt, ZMap.get cid´ nt with
                              | AbQValid l0, AbTCBValid tds cpu_la _, AbTCBValid RUN cpu_t q_id ⇒
                                if zeq cpu_t cpu then
                                  if zeq q_id (-1) then
                                    match (l0 ++ (la :: nil)) with
                                      | nil ⇒ None
                                      | la0 :: l1 ⇒
                                        match ZMap.get la0 nt with
                                          | AbTCBValid _ cpu_t´ _ ⇒
                                            if zeq cpu_t´ cpu then
                                              let n := slp´ - 1 in
                                              if zle_lt 0 n (num_proc - 1) then
                                                let cache_t := ZMap.set la (AbTCBValid tds cpu_la (-1)) nt in
                                                let cache_q := ZMap.set msgq (AbQValid l) nq in
                                                let (rt, rq) :=
                                                    if zeq cpu current_CPU_ID then
                                                      (ZMap.set
                                                         la0 (AbTCBValid RUN cpu (-1))
                                                         (ZMap.set
                                                            cid´ (AbTCBValid READY cpu rdyq)
                                                            (ZMap.set la (AbTCBValid READY cpu rdyq) nt)),
                                                       ZMap.set rdyq (AbQValid (l1 ++ (cid´ :: nil)))
                                                                (ZMap.set msgq (AbQValid l) nq))
                                                    else (t´, q´) in
                                                let (rslp, rcid) :=
                                                    if zeq cpu current_CPU_ID then (n, la0) else (slp´, cid´) in
                                                Some (rt, rq, rslp, rcid,
                                                      ZMap.set msgq (Some (cache_t, cache_q)) cache´,
                                                      TCB_YIELD la0 (Some la))
                                              else None
                                            else None
                                          | _ ⇒ None
                                        end
                                    end
                                  else None
                                else None
                              | _, _,_ ⇒ None
                            end
                        else None
                    end
                  | _ ⇒ None
                end
              | _ ⇒ Some (t´, q´, slp´, cid´, cache´, res´)
            end
          | _ ⇒ None
        end
    end.

    Definition CalTCB_log (l: MultiLog) :=
      CalTCB_split_log l (ZMap.set 0 (AbTCBValid RUN current_CPU_ID (-1)) (real_abtcb (ZMap.init AbTCBUndef)))
                       (real_abq (ZMap.init AbQUndef)) 0 (current_CPU_ID + 1) (ZMap.init None).

    Definition CalTCB_log_real (l: MultiLog) :=
      match CalTCB_log l with
        | Some (_,_,_,_,_, r) ⇒ Some r
        | _ ⇒ None
      end.


End CAL_TCB.

Section Def_Invariant.

  Context `{waittime: WaitTime}.

  Definition valid_multi_oracle_domain (o: MultiOracle):=
    ∀ i i0 e l
           (Hin: In (TEVENT i0 e) (o i l)),
      i0 ≠ i ∧ 0 ≤ i0 < TOTAL_CPU.

  Definition valid_qlock (l: MultiLog) :=
    ∃ self_c other_c b q tq, Q_CalLock l = Some (self_c, other_c, b, q, tq).

  Definition valid_qlock_pool (l: MultiLogPool):=
    ∀ i ofs r q
           (Hrange: index2Z i ofs = Some r)
           (Hdef: ZMap.get r l = MultiDef q),
      valid_qlock q.


  Definition not_head (i: Z) (l: list Z) :=
    match l with
      | nil ⇒ True
      | i0 :: _ ⇒
        if zeq i i0 then False
        else True
    end.

  Definition valid_multi_oracle_queue(o: MultiOracle):=
    ∀ i l
           (Hin´: ∀ i1 e1, In (TEVENT i1 e1) l → 0 ≤ i1 < TOTAL_CPU)
           (Hin: valid_qlock l)
           (Hlast: match l with
                     | TEVENT c0 e0 :: l´ ⇒ c0 = i
                     | _ ⇒ True
                   end),
    ∃ self_c other_c b q tq,
      Q_CalLock ((o i l) ++ l) = Some (self_c, other_c, b, q, tq)
      ∧ (other_c ≠ O).

  Definition valid_multi_oracle_pool (o: MultiOraclePool):=
    ∀ i ofs r
           (Hrange: index2Z i ofs = Some r),
      valid_multi_oracle_domain (ZMap.get r o)
      ∧ valid_multi_oracle_queue (ZMap.get r o).

  Definition get_free_qlock (l: MultiLog) :=
    ∀ k self_c other_c q tq l´
           (Hincr: ∃ prefix, prefix ++ l´ = l)
           (Hcal: Q_CalLock l´ = Some (self_c, other_c, k, q, tq))
           (Hk: k = LGET ∨ k = LEMPTY),
      CalValidBit l´ = Some FreeToPull.

  Definition get_free_qlock_pool (l: MultiLogPool) :=
    ∀ i ofs r q
           (Hrange: index2Z i ofs = Some r)
           (Hdef: ZMap.get r l = MultiDef q),
      get_free_qlock q.

  Definition get_free_qlock_oracle (o: MultiOracle):=
    ∀ i l
           (Hget: get_free_qlock l)
           (Hfrom: ∀ i1 e1, In (TEVENT i1 e1) l → i1 ≠ i → ∃ l0, In (TEVENT i1 e1) (o i l0)),
      get_free_qlock ((o i l) ++ l).

  Definition get_free_qlock_oracle_pool (o: MultiOraclePool) :=
    ∀ i ofs r
           (Hrange: index2Z i ofs = Some r),
      get_free_qlock_oracle (ZMap.get r o).

  Definition valid_hlock (l: MultiLog) :=
    ∃ self_c b q, H_CalLock l = Some (self_c, b, q).

  Definition valid_hlock_pool (l: MultiLogPool):=
    ∀ i ofs r q
           (Hrange: index2Z i ofs = Some r)
           (Hdef: ZMap.get r l = MultiDef q),
      valid_hlock q.

  Definition valid_multi_oracle_hqueue(o: MultiOracle):=
    ∀ i l
           (Hin: valid_hlock l),
    ∃ self_c b q,
      H_CalLock ((o i l) ++ l) = Some (self_c, b, q).

  Definition valid_multi_oracle_pool_H (o: MultiOraclePool):=
    ∀ i ofs r
           (Hrange: index2Z i ofs = Some r),
      valid_multi_oracle_domain (ZMap.get r o)
      ∧ valid_multi_oracle_hqueue (ZMap.get r o).

  Function index_range1 (i: Z) :=
    match i with
      
      | ID_TCB ⇒ Some ID_TCB_range
      
      | ID_SC ⇒ Some ID_SC_range
      | _ ⇒ None
    end.

  Function index2Z1 (index ofs: Z) :=
    match index_range1 index, index_incrange index with
      | Some r, Some base ⇒
        if zle_lt 0 ofs r then
          Some (base + ofs)
        else
          None
      | _, _ ⇒ None
    end.

  Definition valid_hlock_pool1 (l: MultiLogPool):=
    ∀ i ofs r q
           (Hrange: index2Z1 i ofs = Some r)
           (Hdef: ZMap.get r l = MultiDef q),
      valid_hlock q.

  Definition valid_multi_oracle_pool_H1 (o: MultiOraclePool):=
    ∀ i ofs r
           (Hrange: index2Z1 i ofs = Some r),
      valid_multi_oracle_domain (ZMap.get r o)
      ∧ valid_multi_oracle_hqueue (ZMap.get r o).

  Function index_range2 (i: Z) :=
    match i with
      
      | ID_SC ⇒ Some ID_SC_range
      | _ ⇒ None
    end.

  Function index2Z2 (index ofs: Z) :=
    match index_range2 index, index_incrange index with
      | Some r, Some base ⇒
        if zle_lt 0 ofs r then
          Some (base + ofs)
        else
          None
      | _, _ ⇒ None
    end.

  Definition valid_hlock_pool2 (l: MultiLogPool):=
    ∀ i ofs r q
           (Hrange: index2Z2 i ofs = Some r)
           (Hdef: ZMap.get r l = MultiDef q),
      valid_hlock q.

  Definition valid_multi_oracle_pool_H2 (o: MultiOraclePool):=
    ∀ i ofs r
           (Hrange: index2Z2 i ofs = Some r),
      valid_multi_oracle_domain (ZMap.get r o)
      ∧ valid_multi_oracle_hqueue (ZMap.get r o).

  Context `{real_params: RealParams}.

  Definition valid_AT_log_H l :=
    ∃ a, CalAT_log_real l = Some a.

  Definition valid_AT_log_pool_H l :=
    ∀ q (Hdef: ZMap.get lock_AT_start l = MultiDef q),
      valid_AT_log_H q.

  Definition valid_AT_oracle_H (o: MultiOracle) :=
    ∀ q i (Hvalid: valid_AT_log_H q),
      valid_AT_log_H ((o i q) ++ q).

  Definition valid_AT_oracle_pool_H (o: MultiOraclePool) :=
    valid_AT_oracle_H (ZMap.get lock_AT_start o).

  Section WITH_OPS.

    Context`{oracle_ops: MultiOracleOps}.

    Definition valid_TCB_log l :=
      ∃ res, CalTCB_log_real l = Some (res).

    Definition valid_TCB_log_type l :=
      ∀ q (Hdef: ZMap.get lock_range l = MultiDef q),
        valid_TCB_log q.

    Definition valid_TCB_oracle (o: MultiOracle) :=
      ∀ q i (Hvalid: valid_TCB_log q),
        valid_TCB_log ((o i q) ++ q).

    Definition valid_TCB_pool_oracle (o: MultiOraclePool) :=
      valid_TCB_oracle (ZMap.get lock_range o).

  End WITH_OPS.

  Fixpoint GetSharedMemEvent (l: MultiLog):=
    match l with
      | nil ⇒ None
      | TEVENT _ e :: l´ ⇒
        let l0 := GetSharedMemEvent l´ in
        match e with
          | TSHARED (OMEME e´) ⇒ Some e´
          | _ ⇒ l0
        end
    end.

  Fixpoint GetSharedAT (l: MultiLog):=
    match l with
      | nil ⇒ None
      | TEVENT _ e :: l´ ⇒
        let l0 := GetSharedAT l´ in
        match e with
          | TSHARED (OATE e´) ⇒ Some e´
          | _ ⇒ l0
        end
    end.



  Fixpoint GetSharedSC (l: MultiLog):=
    match l with
      | nil ⇒ None
      | TEVENT _ e :: l´ ⇒
        let l0 := GetSharedSC l´ in
        match e with
          | TSHARED (OSCE s´) ⇒ Some s´
          | TSHARED (OTDSLEEP _ _ s´) ⇒ Some s´
          | _ ⇒ l0
        end
    end.


  Fixpoint GetSharedTCB (l: MultiLog):=
    match l with
      | nil ⇒ None
      | TEVENT _ e :: l´ ⇒
        let l0 := GetSharedTCB l´ in
        match e with
          | TSHARED (OTCBE e1 e2) ⇒ Some (e1, e2)
          | _ ⇒ l0
        end
    end.

  Fixpoint GetSharedABTCB (l: MultiLog):=
    match l with
      | nil ⇒ None
      | TEVENT _ e :: l´ ⇒
        let l0 := GetSharedABTCB l´ in
        match e with
          | TSHARED (OABTCBE e1 e2) ⇒ Some (e1, e2)
          | _ ⇒ l0
        end
    end.

  Fixpoint GetSharedBuffer (l: MultiLog):=
    match l with
      | nil ⇒ None
      | TEVENT _ e :: l´ ⇒
        let l0 := GetSharedBuffer l´ in
        match e with
          | TSHARED (OBUFFERE e) ⇒ Some e
          | _ ⇒ l0
        end
    end.

End Def_Invariant.