Library mcertikos.mcslock.CalMCSLockLemmas

Require Import List.
Require Import CommonTactic.
Require Import Coqlib.

Require Import CommonTactic.
Require Import GlobalOracle.
Require Import CalMCSLock.

Require Import Maps.
Require Import ZSet.
Require Import ListLemma2.

Section WITHWAITTIME.

  Context `{waittime: WaitTime}.

  Lemma index2Z_in_lock_range:
    ∀ i ofs abid, index2Z i ofs = Some abid → 0 ≤ abid < lock_range.
  Proof.
    intros i ofs z Hdestruct1.
    assert (lock_id_val: i = ID_AT ∨ i = ID_TCB ∨ i = ID_SC).
    { unfold index2Z in Hdestruct1.
      unfold index_range in ×.
      destruct i; try tauto; try (inversion Hdestruct1; fail).
      destruct p; try tauto; try (inversion Hdestruct1; fail).
      destruct p; try tauto; try (inversion Hdestruct1). }
    Opaque Z.add Z.mul Z.sub Z.div.
    destruct lock_id_val as [lock_id_val | [lock_id_val | lock_id_val]]; subst.
    - unfold index2Z in Hdestruct1; simpl.
      unfold index_range in Hdestruct1.
      subdestruct; inv Hdestruct1; unfold ID_AT_range in *; auto.
      unfold lock_range.
      simpl; unfold ID_AT_range, ID_TCB_range, ID_SC_range; omega.
    - unfold index2Z in Hdestruct1; simpl.
      unfold index_range in Hdestruct1; simpl.
      unfold index_incrange in Hdestruct1; simpl.
      subdestruct; simpl; unfold ID_TCB_range in *; unfold lock_range; simpl; subst.
      inv Hdestruct1; unfold ID_AT_range in *; try omega.
      unfold ID_TCB_range, ID_SC_range; omega.
    - unfold index2Z in Hdestruct1; simpl.
      unfold index_range in Hdestruct1.
      unfold index_incrange in Hdestruct1.
      subdestruct.
      unfold lock_TCB_range in ×.
      unfold lock_range; unfold ID_AT_range, ID_SC_range, ID_TCB_range in *; inv Hdestruct1.
      omega.
  Qed.

  Lemma QS_CalLock_q_length_same : ∀ ll self_c rel_c b q slow tq,
                                     QS_CalLock ll = Some (self_c, rel_c, b, q, slow, tq) → length q = length tq.
  Proof.
    Transparent QS_CalLock.
    induction ll; simpl; intros.
    - inv H; simpl.
      trivial.
    - subdestruct; inv H;
      exploit IHll; eauto;
      intros;
      repeat rewrite app_comm_cons;
      repeat rewrite app_length;
      rewrite H; simpl; trivial.
  Qed.


  Lemma QS_CalLock_inv : ∀ e l self_c rel_c b q slow tq,
                           QS_CalLock (e::l) = Some (self_c, rel_c, b, q, slow, tq) →
                           ∃ self_c´ rel_c´ b´ q´ slow´ tq´,
                             QS_CalLock l = Some (self_c´, rel_c´, b´, q´, slow´, tq´).
  Proof.
    Transparent QS_CalLock.
    simpl; intros.
    destruct e; destruct (QS_CalLock l) as [[[[[[? ?] ?] ?] ?] ?] |] ;
    try congruence; eauto.
    simpl in H.
    Opaque QS_CalLock.
    subdestruct; (repeat (eexists); reflexivity).
  Qed.
  Lemma QS_CalLock_inv_app : ∀ l´ l self_c rel_c b q slow tq,
                               QS_CalLock (l´ ++ l) = Some (self_c, rel_c, b, q, slow, tq) →
                               ∃ self_c´ rel_c´ b´ q´ slow´ tq´,
                                 QS_CalLock l = Some (self_c´, rel_c´, b´, q´, slow´, tq´).
  Proof.
    Opaque QS_CalLock.
    induction l´.
    + simpl; intros; eauto 7.
    + simpl.
      intros until tq.
      intros HCal.
      destruct (QS_CalLock_inv _ _ _ _ _ _ _ _ HCal)
        as [self_c1 [rel_c1 [ b1 [q1 [ slow1 [tq1 H]]]]]].
      exact (IHl´ _ _ _ _ _ _ _ H).
  Qed.


  Lemma QS_CalLock_NoDup_onestep:
    ∀ e l self_c rel_c b q slow tq self_c´ rel_c´ b´ q´ slow´ tq´
           (HCal: QS_CalLock l = Some (self_c, rel_c, b, q, slow, tq))
           (Hndup: NoDup q)
           (HCal´: QS_CalLock (e :: l) = Some (self_c´, rel_c´, b´, q´, slow´, tq´)),
      NoDup q´.
  Proof.
    Transparent QS_CalLock.
    intros until tq´.
    intros HCal Hndup HCal´.
    simpl in HCal´.
    rewrite HCal in HCal´. clear HCal.
    destruct e as [j e].
    destruct e as [e | e ]; destruct e eqn:?; try congruence;
    repeat match goal with
             | [ HCal´ : context [match QS_CalLock ?lis with
                                    | Some _ ⇒ _ | None ⇒ _ end] |- _]
               ⇒ destruct (QS_CalLock lis) as [[[[[[? ?] ?] ?] ?] ?] |] eqn:?
             | [HCal´ : context[match ?X with | nil ⇒ _ | (_ :: _) ⇒ _ end] |- _] ⇒ destruct X eqn:?
             | [HCal´ : context[if ?X then _ else _] |- _] ⇒ destruct X
             | [HCal´ : context[match ?X with | O ⇒ _ | S _ ⇒ _ end] |- _] ⇒ destruct X eqn:?
             | [HCal´ : context[match ?X with | Some _ ⇒ _ | None ⇒ _ end] |- _ ] ⇒ destruct X eqn:?
             | [HCal´ : context[match ?X with | MCSLOCK _ _ _ ⇒ _ end] |- _ ] ⇒ destruct X as [? ? ?] eqn:?
             | [HCal´ : context[match ?X with | LEMPTY ⇒ _ | LGET ⇒ _ | LHOLD ⇒ _ end] |- _ ] ⇒ destruct X
             | [ HCal´ : context[ZMap.get ?X ?Y] |- _]
               ⇒ destruct (ZMap.get X Y)
           end; try congruence.
    + replace q´ with (j::nil) by congruence.
      apply NoDup_singleton.
    + replace q´ with ((z :: l0) ++ j :: nil) by congruence.
      clear HCal´.
      rewrite NoDup_app.
      split; [|split].
    - assumption.
    - apply NoDup_singleton.
    - intros x.
      simpl.
      intros [H1 H2].
      destruct H2; [ subst | tauto].
      intuition.
      + replace q´ with (@nil Z) by congruence.
        constructor.
      + subst.
        replace q´ with l0 by congruence.
        inversion Hndup.
        assumption.
  Qed.

  Lemma QS_CalLock_NoDup:
    ∀ l self_c rel_c b q slow tq
           (HCal: QS_CalLock l = Some (self_c, rel_c, b, q, slow, tq)),
      NoDup q.
  Proof.
    induction l as [|e l].
    × simpl.
      intros.
      replace q with (@nil Z) by congruence; constructor.
    × Opaque QS_CalLock.
      intros until tq.
      intros HCal.
      destruct (QS_CalLock_inv _ _ _ _ _ _ _ _ HCal) as [self_c0 [rel_c0 [b0 [q0 [slow0 [tq0 HCal0]]]]]].
      specialize (IHl _ _ _ _ _ _ HCal0).
      eapply QS_CalLock_NoDup_onestep; eauto.
  Qed.

End WITHWAITTIME.