Library mcertikos.conlib.conmclib.Concurrent_Linking_Lib

Require Import Coqlib.
Require Import Maps.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Events.
Require Import Conventions.
Require Import AuxLemma.
Require Import GlobIdent.
Require Import CommonTactic.


Section ZSET.

  Definition ZSet := Z → bool.

  Definition subset (A B: ZSet) :=
    ∀ i (HA: A i = true), B i = true.

  Definition disjoint_set (A B: ZSet) :=
    ∀ i, (A i = true → B i = false)
              ∧ (B i = true → A i = false).

  Class ZSet_operation :=
    {
      union_set: ZSet → ZSet → ZSet;
      join_set: ZSet → ZSet → ZSet;
      s_set: Z → ZSet;

      union_left:
        ∀ s1 s2 e
               (Hleft: s1 e = true),
          (union_set s1 s2) e = true;

      union_right:
        ∀ s1 s2 e
               (Hright: s2 e = true),
          (union_set s1 s2) e = true;
      
      union_false:
        ∀ s1 s2 e
               (Hleft: s1 e = false)
               (Hright: s2 e = false),
          (union_set s1 s2) e = false;

      
      join_set_commutativity:
        ∀ A B, join_set A B = join_set B A;

      join_set_imply:
        ∀ A B i
               (Hjoin: join_set A B i = true),
          A i = true ∧ B i = true;
      
      join_set_rely:
        ∀ A B i
               (HA: A i = true)
               (HB: B i = true),
          join_set A B i = true;
      
      s_set_in:
        ∀ i,
          (s_set i) i = true;

      s_set_not_in:
        ∀ i j
               (Hneq: i ≠ j),
          (s_set i) j = false
                          
    }.

  Context `{zset_op: ZSet_operation}.

  Lemma join_set_not_in:
    ∀ A B i,
      join_set A B i = false →
      A i = false ∨ B i = false.
  Proof.
    intros. destruct (A i) eqn: HA; eauto.
    destruct (B i) eqn: HB; eauto.
    erewrite join_set_rely in H; eauto.
  Qed.

  Lemma join_set_not_in_rely:
    ∀ A B i,
      A i = false ∨ B i = false →
      join_set A B i = false.
  Proof.
    intros.
    destruct (join_set A B i) eqn: HJ; trivial.
    eapply join_set_imply in HJ.
    destruct HJ as (HA & HB).
    rewrite HA, HB in H.
    inv H; eauto.
  Qed.

  Lemma union_subset_left:
    ∀ s1 s2,
      subset s1 (union_set s1 s2).
  Proof.
    unfold subset. intros. eapply union_left. trivial.
  Qed.

  Lemma union_subset_right:
    ∀ s1 s2,
      subset s2 (union_set s1 s2).
  Proof.
    unfold subset. intros. eapply union_right. trivial.
  Qed.

  Lemma union_false´:
    ∀ s1 s2 e
           (Hfalse: (union_set s1 s2) e = false),
      s1 e = false
      ∧ s2 e = false.
  Proof.
    intros. destruct (s1 e) eqn:Hs1.
    - eapply (union_left _ s2) in Hs1. congruence.
    - destruct (s2 e) eqn:Hs2.
      + eapply (union_right s1) in Hs2. congruence.
      + eauto.
  Qed.

  Lemma s_set_in_imply:
    ∀ i j,
      (s_set i) j = true → i = j.
  Proof.
    intros. destruct (zeq i j); trivial.
    rewrite s_set_not_in in H; eauto. congruence.
  Qed.

  Lemma s_set_not_in_imply:
    ∀ i j,
      (s_set i) j = false → i ≠ j.
  Proof.
    intros. destruct (zeq i j); trivial. subst.
    rewrite s_set_in in H; eauto. congruence.
  Qed.

End ZSET.


Section PARTIAL_MAP.

  Class PartialMap :=
    {
      pMap: Type → ZSet → Type;
      pget {A:Type} {B: ZSet} : Z → (pMap A B) → option A;
      pset {A:Type} {B: ZSet} : Z → A → (pMap A B) → (pMap A B);

      pinit {A:Type} {B: ZSet} : A → (pMap A B);

      pget_none:
        ∀ {A:Type} {B: ZSet} (m: pMap A B) i,
          B i = false → pget i m = None;

      pget_some:
        ∀ {A:Type} {B: ZSet} (m: pMap A B) i,
          B i = true → ∃ b, pget i m = Some b;

      pgss:
        ∀ {A:Type} {B: ZSet} (m: pMap A B) i b,
          B i = true → pget i (pset i b m) = Some b;

      pgso:
        ∀ {A:Type} {B: ZSet} (m: pMap A B) i j b,
          i ≠ j → pget i (pset j b m) = pget i m;

      pinit_gi:
        ∀ {A: Type} {B: ZSet} i a,
          B i = true → pget i (pinit (A := A) (B := B) a) = Some a
    }.

  Context `{pmap: PartialMap}.

  Lemma pget_some_domain:
    ∀ {A:Type} {B: ZSet} (m: pMap A B) i b,
      pget i m = Some b → B i = true.
  Proof.
    intros. destruct (B i) eqn: Hn; trivial.
    eapply (pget_none m) in Hn. congruence.
  Qed.

  Lemma pget_none_domain:
    ∀ {A:Type} {B: ZSet} (m: pMap A B) i,
      pget i m = None → B i = false.
  Proof.
    intros. destruct (B i) eqn: Hn; trivial.
    eapply (pget_some m) in Hn.
    destruct Hn as (b & Heq).
    congruence.
  Qed.

End PARTIAL_MAP.


Section MACHINE_DEF.

  Require Import AuxStateDataType.

  Inductive OtherEvent :=
  
  | OINC_TICKET (n: nat)
  | OINC_NOW
  | OGET_NOW
  | OINIT
  | OHOLD_LOCK
  | OPAGE_COPY (b: PageBuffer)
  .

  Function OtherEvent_2_ident (e: OtherEvent) :=
    match e with
      | OINC_TICKET _ ⇒ atomic_FAI
      | OINC_NOW ⇒ log_incr
      | OGET_NOW ⇒ log_get
      | OINIT ⇒ log_init
      | OHOLD_LOCK ⇒ log_hold
      | OPAGE_COPY _ ⇒ page_copy
    end.

  Function cpu_set (i: Z) : bool :=
    if zle_lt 0 i 8 then true else false.

  Function private_id eid :=
    if peq eid acquire_shared then False
    else if peq eid release_shared then False
         else if peq eid atomic_FAI then False
              else if peq eid log_get then False
                   else if peq eid log_incr then False
                        else if peq eid log_hold then False
                             else if peq eid log_init then False
                                  else if peq eid page_copy then False
                                       else True.

  Function atomic_id eid :=
     if peq eid log_get then True
         else if peq eid log_incr then True
              else if peq eid log_hold then True
                   else if peq eid log_init then True
                        else if peq eid page_copy then True
                             else False.

  Lemma ef_or:
    ∀ ef,
      match ef with
      | EF_external _ _ ⇒ False
      | _ ⇒ True
      end ∨
      match ef with
      | EF_external _ _ ⇒ True
      | _ ⇒ False
      end.
  Proof.
    destruct ef; eauto.
  Qed.

  Lemma private_id_dec (eid: ident) :
    {private_id eid } + {¬ private_id eid }.
  Proof.
    unfold private_id.
    repeat match goal with
           | |- context [peq ?a ?b] ⇒
             destruct (peq a b); eauto
           end.
  Qed.

End MACHINE_DEF.

Section LIST_LEMMAS.

  Lemma list_append_neq0:
    ∀ {A: Type} l (a: A),
      l = a :: l → False.
  Proof.
    induction l; intros.
    - inv H.
    - inversion H. eauto.
  Qed.

  Lemma list_append_neq:
    ∀ {A: Type} l l´ (a: A),
      l = l´ ++ a :: l → False.
  Proof.
    induction l; intros.
    - destruct l´; inv H.
    - destruct l´; inversion H.
      + eapply list_append_neq0 in H2; eauto.
      + specialize (IHl (l´ ++ a0 :: nil) a1). eapply IHl.
        rewrite <- app_assoc.
        rewrite <- app_comm_cons.
        rewrite app_nil_l. assumption.
  Qed.

  Lemma list_append_e_eq:
    ∀ {A : Type} l0 l (e e0: A),
      l0 ++ e :: l = e0 :: l →
      l0 = nil ∧ e = e0.
  Proof.
    induction l0; intros.
    - inv H. eauto.
    - inversion H.
      symmetry in H2.
      apply list_append_neq in H2. inv H2.
  Qed.

  Lemma list_eq_bidirection:
    ∀ {A:Type} (l0 l1 l l´: list A),
      l = l0 ++ l´ →
      l´ = l1 ++ l →
      l = l´.
  Proof.
    induction l0; intros; trivial.
    destruct l1.
    + rewrite H0. trivial.
    + destruct l; inversion H; clear H.
      exploit IHl0; try eapply H3.
      {
        rewrite H0.
        instantiate (1:= (a0 :: l1) ++ (a1:: nil)).
        rewrite <- app_assoc.
        trivial.
      }
      {
        clear H2 H3. intros Heq.
        rewrite Heq in H0.
        eapply list_append_neq in H0. inv H0.
      }
  Qed.

  Lemma list_append_neq´:
    ∀ {A: Type} (l l´: list A),
      l = l´ ++ l → l´ = nil.
  Proof.
    destruct l; intros.
    - rewrite app_nil_r in H. congruence.
    - destruct l´; trivial.
      inversion H. clear H.
      eapply list_append_neq in H2. inv H2.
  Qed.

  Lemma list_append_e_or´:
    ∀ {A : Type} l l1 l2 (e: A),
      e :: l = l2 ++ l1 ++ l →
      (l1 = nil ∧ l2 = e::nil) ∨ (l1 = e::nil ∧ l2 = nil).
  Proof.
    intros. destruct l2.
    - right. destruct l1.
      + symmetry in H.
        eapply list_append_neq0 in H. inv H.
      + inversion H. clear H.
        eapply list_append_neq´ in H2. subst. eauto.
    - left. inversion H. clear H.
      rewrite app_assoc in H2.
      eapply list_append_neq´ in H2.
      eapply app_eq_nil in H2.
      destruct H2 as (? & ?); subst.
      eauto.
  Qed.

  Lemma regmap_None_Some:
    ∀ {A:Type} i i´ (rs rs´: A),
      ZMap.get i´ (ZMap.set i (Some rs) (ZMap.init None)) = Some rs´
      → i´ = i ∧ rs´ = rs.
  Proof.
    intros. destruct (zeq i i´); subst.
    - rewrite ZMap.gss in H. inv H. eauto.
    - rewrite ZMap.gso in H; eauto.
      rewrite ZMap.gi in H. inv H.
  Qed.

  Lemma ZMap_gss_eq:
    ∀ {A:Type} i (d d´: A) a a´,
      ZMap.set i d a = ZMap.set i d´ a´ →
      d´ = d.
  Proof.
    intros.
    assert (Heq: ZMap.get i (ZMap.set i d a) = ZMap.get i (ZMap.set i d´ a´)).
    {
      rewrite H. trivial.
    }
    repeat rewrite ZMap.gss in Heq; subst.
    trivial.
  Qed.

  Lemma ZMap_gss_forall:
    ∀ {A:Type} (a a´: ZMap.t A) b0 i0,
      (∀ i,
         ZMap.get i (ZMap.set i0 b0 a) = ZMap.get i a´) →
      ∀ (b: A),
        (∀ i,
           ZMap.get i (ZMap.set i0 b a) =
           ZMap.get i (ZMap.set i0 b a´)).
  Proof.
    intros. destruct (zeq i i0); subst.
    - repeat rewrite ZMap.gss. trivial.
    - repeat rewrite ZMap.gso; auto.
      rewrite <- H. rewrite ZMap.gso; auto.
  Qed.

  Lemma Eapp_E0_inv´: ∀ t1 t2, E0 = t1 ** t2 → t1 = E0 ∧ t2 = E0.
  Proof.
    intros. eapply Eapp_E0_inv. auto.
  Qed.

  Lemma list_append_rewrite:
    ∀ {A: Type} l (a b: A),
      a :: b :: l = (a:: nil) ++ (b :: l).
  Proof.
    intros.
    rewrite <- app_comm_cons. trivial.
  Qed.

  Lemma list_append_event:
    ∀ {A: Type} l l0 l1 (e e1: A),
      l0 ++ e :: l = l1 ++ e1 :: l →
      e = e1.
  Proof.
    induction l0; intros.
    - destruct l1.
      + inv H. trivial.
      + symmetry in H.
        eapply list_append_e_eq in H.
        destruct H as (HF & _). inv HF.
    - destruct l1.
      + eapply list_append_e_eq in H.
        destruct H as (HF & _). inv HF.
      + inv H. eauto.
  Qed.

  Lemma set_init_eq:
    ∀ {A: Type} (a a´: A) i rsm,
      ZMap.set i a rsm = ZMap.set i a´ rsm
      → a = a´.
  Proof.
    intros.
    assert (Heq: ZMap.get i (ZMap.set i a rsm) = ZMap.get i (ZMap.set i a´ rsm)).
    {
      rewrite H. reflexivity.
    }
    repeat rewrite ZMap.gss in Heq.
    assumption.
  Qed.

  Lemma regmap_None_None:
    ∀ {A:Type} i i´ (rs: A),
      ZMap.get i´ (ZMap.set i (Some rs) (ZMap.init None)) = None
      → i´ ≠ i.
  Proof.
    intros. destruct (zeq i i´); subst.
    - rewrite ZMap.gss in H. inv H.
    - auto.
  Qed.

  Lemma list_append_list:
    ∀ {A: Type} l l0 l1 (e e1: A),
      l0 ++ e :: l = l1 ++ e1 :: l →
      e = e1.
  Proof.
    induction l0; intros.
    - destruct l1.
      + inv H; trivial.
      + symmetry in H.
        eapply list_append_e_eq in H.
        destruct H as (HF & _). inv HF.
    - destruct l1.
      + eapply list_append_e_eq in H.
        destruct H as (HF & _). inv HF.
      + inv H. eauto.
  Qed.

End LIST_LEMMAS.