Require Import ALInitGenDef.
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_AT_log:
      ∀ l l´ s p
             (Hcal: H_CalLock l = Some p)
             (Hrel: relate_AT_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.
    Qed.

    Lemma relate_AT_Log_cons:
      ∀ l1 l1´ l2 l2´ s
             (Hrel1: relate_AT_Log s l1 l2)
             (Hrel2: relate_AT_Log s l1´ l2´),
        relate_AT_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_AT_Log_oracle_cons:
      ∀ c o1 o2 l1 l2 s
             (Hrel1: relate_AT_Log s l1 l2)
             (Hrel2: relate_AT_Oracle_Pool s o1 o2),
        relate_AT_Log s (ZMap.get 0 o1 c l1 ++ l1) (ZMap.get 0 o2 c l2 ++ l2).
    Proof.
      intros. eapply relate_AT_Log_cons; eauto.
      inv Hrel2. inv H0. eauto.
    Qed.

    Lemma relate_AT_Log_GetSharedAT:
      ∀ l1 l2 s
             (Hrel1: relate_AT_Log s l1 l2),
        (∀ a, GetSharedAT l1 = Some a →
                   ∃ m, GetSharedMemEvent l2 = Some m
                             ∧ relate_AT_Event s (OATE a) (OMEME m))
        ∧ (GetSharedAT 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.
        + 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.
    Qed.

    Lemma relate_AT_Log_GetSharedAT_Some:
      ∀ l1 l2 s a
             (Hget: GetSharedAT l1 = Some a)
             (Hrel1: relate_AT_Log s l1 l2),
      ∃ m, GetSharedMemEvent l2 = Some m
                ∧ relate_AT_Event s (OATE a) (OMEME m).
    Proof.
      intros. exploit relate_AT_Log_GetSharedAT; eauto.
      intros (HP & _). exploit HP; eauto.
    Qed.

    Lemma relate_AT_Log_GetSharedAT_None:
      ∀ l1 l2 s
             (Hget: GetSharedAT l1 = None)
             (Hrel1: relate_AT_Log s l1 l2),
        GetSharedMemEvent l2 = None.
    Proof.
      intros. exploit relate_AT_Log_GetSharedAT; eauto.
      intros (_ & HP). exploit HP; eauto.
    Qed.

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

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

    Local Opaque H_CalLock.

    Lemma index2Z_neq:
      ∀ i ofs r
             (Hneq: i ≠ 0)
             (Hin: index2Z i ofs = Some r),
        r ≠ 0.
    Proof.
      intros. functional inversion Hin.
      functional inversion H0.
      - omega.
      - subst. functional inversion H1; subst.
        unfold ID_AT_range in ×. omega.
      - subst. functional inversion H1; subst.
        unfold lock_TCB_range, ID_AT_range, ID_TCB_range. omega.
    Qed.

  End WITHMEM.

End Refinement.