Require Import CVIntroGenDef.
Require Import XOmega.
Require Export ByteListProp.

Section Refinement.

  Section WITHMEM.

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

    Lemma H_CalLock_relate_SC_log:
      ∀ l l´ s p
             (Hcal: H_CalLock l = Some p)
             (Hrel: relate_SC_Log s l l´),
        H_CalLock l´ = Some p.
    Proof.
      induction l; intros; simpl.
      - inv Hrel. eauto.
      - inv Hrel. inv Hrelate_event.
        + Local Transparent H_CalLock.
          simpl in ×.
          subdestruct. inv Hcal.
          exploit IHl; eauto.
          intros Hcal´. rewrite Hcal´.
          rewrite zeq_true. trivial.
        + simpl in ×.
          subdestruct; inv Hcal.
          × exploit IHl; eauto.
            intros Hcal´. rewrite Hcal´.
            rewrite zeq_true. trivial.
          × exploit IHl; eauto.
            intros Hcal´. rewrite Hcal´. trivial.
        + simpl in ×.
          subdestruct; inv Hcal.
          × exploit IHl; eauto.
            intros Hcal´. rewrite Hcal´.
            rewrite zeq_true. trivial.
        + simpl in ×.
          subdestruct; inv Hcal.
          × exploit IHl; eauto.
            intros Hcal´. rewrite Hcal´.
            rewrite zeq_true. trivial.
    Qed.

    Lemma relate_SC_Log_cons:
      ∀ l1 l1´ l2 l2´ s
             (Hrel1: relate_SC_Log s l1 l2)
             (Hrel2: relate_SC_Log s l1´ l2´),
        relate_SC_Log s (l1 ++ l1´) (l2 ++ l2´).
    Proof.
      induction l1; simpl; intros.
      - inv Hrel1. eapply Hrel2.
      - inv Hrel1. exploit IHl1; eauto.
        intros Hrel3. simpl.
        econstructor; eauto.
    Qed.

    Lemma relate_SC_Log_oracle_cons:
      ∀ c o1 o2 l1 l2 s i
             (Hrel1: relate_SC_Log s l1 l2)
             (Hrel2: relate_SC_Oracle_Pool s o1 o2)
             (Hrange: 0 ≤ i < num_chan),
        relate_SC_Log s (ZMap.get (i + lock_TCB_range) o1 c l1 ++ l1) (ZMap.get (i + lock_TCB_range) o2 c l2 ++ l2).
    Proof.
      intros. eapply relate_SC_Log_cons; eauto.
      inv Hrel2. specialize (H0 _ Hrange).
      inv H0. eauto.
    Qed.

    Lemma relate_SC_Log_GetSharedSC:
      ∀ l1 l2 s
             (Hrel1: relate_SC_Log s l1 l2),
        (∀ e, GetSharedSC l1 = Some e →
                       ∃ m, GetSharedMemEvent l2 = Some m
                                 ∧ relate_SC_Event s (OSCE e) (OMEME m))
        ∧ (GetSharedSC l1 = None → GetSharedMemEvent l2 = None).
    Proof.
      induction l1; simpl; intros.
      - split; intros; try congruence. inv Hrel1. trivial.
      - split; intros.
        + inv Hrel1. inv Hrelate_event.
          × inv H. simpl.
            refine_split´; trivial.
          × simpl. exploit IHl1; eauto.
            intros (HP & _). eapply HP; eauto.
          × simpl. exploit IHl1; eauto.
            intros (HP & _). eapply HP; eauto.
          × simpl. exploit IHl1; eauto.
            intros (HP & _). eapply HP; eauto.

        + inv Hrel1. inv Hrelate_event; try congruence.
          × simpl. exploit IHl1; eauto.
            intros (_ & HP). eapply HP; eauto.
          × simpl. exploit IHl1; eauto.
            intros (_ & HP). eapply HP; eauto.
          × simpl. exploit IHl1; eauto.
            intros (_ & HP). eapply HP; eauto.
    Qed.

    Lemma relate_SC_Log_GetSharedSC_Some:
      ∀ l1 l2 s e
             (Hget: GetSharedSC l1 = Some e)
             (Hrel1: relate_SC_Log s l1 l2),
      ∃ m, GetSharedMemEvent l2 = Some m
                ∧ relate_SC_Event s (OSCE e) (OMEME m).
    Proof.
      intros. exploit relate_SC_Log_GetSharedSC; eauto.
      intros (HP & _). exploit HP; eauto.
    Qed.

    Lemma relate_SC_Log_GetSharedSC_None:
      ∀ l1 l2 s
             (Hget: GetSharedSC l1 = None)
             (Hrel1: relate_SC_Log s l1 l2),
        GetSharedMemEvent l2 = None.
    Proof.
      intros. exploit relate_SC_Log_GetSharedSC; eauto.
      intros (_ & HP). exploit HP; eauto.
    Qed.

    Lemma relate_SC_Log_ticket:
      ∀ l1 l2 s c e
             (Hrel1: relate_SC_Log s l1 l2),
        relate_SC_Log s (TEVENT c (TTICKET e) :: l1) (TEVENT c (TTICKET e) :: l2).
    Proof.
      intros. econstructor; trivial. econstructor.
    Qed.

    Lemma relate_SC_Log_pull:
      ∀ l1 l2 s c
             (Hrel1: relate_SC_Log s l1 l2),
        relate_SC_Log s (TEVENT c (TSHARED OPULL) :: l1) (TEVENT c (TSHARED OPULL) :: l2).
    Proof.
      intros. econstructor; trivial. econstructor.
    Qed.

    Local Opaque H_CalLock.

    Lemma index2Z_eq:
      ∀ i (Hrange: 0 ≤ i < num_chan),
        index2Z ID_SC i = Some (i + lock_TCB_range).
    Proof.
      intros. unfold index2Z.
      Local Opaque Z.add. simpl.
      unfold ID_SC_range. rewrite zle_lt_true; trivial.
      f_equal. omega.
      Local Transparent Z.add.
    Qed.

    Lemma index2Z_neq:
      ∀ i ofs r k
             (Hneq: i ≠ ID_SC)
             (Hrange: 0 ≤ k < num_chan)
             (Hin: index2Z i ofs = Some r),
        r ≠ k + lock_TCB_range.
    Proof.
      intros. functional inversion Hin.
      functional inversion H0.
      - subst. functional inversion H1; subst.
        unfold lock_TCB_range in ×.
        simpl in ×.
        unfold ID_AT_range in ×.
        omega.
      - unfold lock_TCB_range, ID_AT_range, ID_TCB_range in ×.
        subst.
        simpl in ×.
        inv H1.
        unfold ID_AT_range in ×.
        omega.
      - subst. functional inversion H1; subst.
        unfold lock_TCB_range, ID_AT_range, ID_TCB_range, ID_SC_range in ×.
        omega.
    Qed.

    Lemma neq_add:
      ∀ a b c,
        a ≠ b →
        a + c ≠ b + c.
    Proof.
      intros. omega.
    Qed.

  End WITHMEM.

End Refinement.