Require Import Coqlib.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Asm.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import FlatMemory.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import RealParams.
Require Import LoadStoreSem1.
Require Import AsmImplLemma.
Require Import LAsm.
Require Import RefinementTactic.
Require Import PrimSemantics.

Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import compcert.cfrontend.Ctypes.
Require Import LayerCalculusLemma.

Require Import AbstractDataType.
Require Import LAsmModuleSemAux.
Require Import TacticsForTesting.
Require Import DeviceStateDataType.
Require Export MQTicketLockOp.
Require Export MTicketLockOp.
Require Import ListLemma2.

Section Refinement.

  Local Open Scope string_scope.
  Local Open Scope error_monad_scope.
  Local Open Scope Z_scope.

  Context `{real_params: RealParams}.
  Context `{multi_oracle_prop: MultiOracleProp}.

  Notation HDATA := RData.
  Notation LDATA := RData.

  Notation HDATAOps := (cdata (cdata_ops := mqticketlockop_data_ops) HDATA).
  Notation LDATAOps := (cdata (cdata_ops := mcurid_data_ops) LDATA).

  Section WITHMEM.

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

    Record relate_RData (f:meminj) (hadt: HDATA) (ladt: LDATA) :=
      mkrelate_RData {
          flatmem_re: FlatMem.flatmem_inj (HP hadt) (HP ladt);
          MM_re: MM hadt = MM ladt;
          MMSize_re: MMSize hadt = MMSize ladt;
          vmxinfo_re: vmxinfo hadt = vmxinfo ladt;
          CR3_re: CR3 hadt = CR3 ladt;
          ikern_re: ikern hadt = ikern ladt;
          pg_re: pg hadt = pg ladt;
          ihost_re: ihost hadt = ihost ladt;
          ti_fst_re: (fst (ti hadt)) = (fst (ti ladt));
          ti_snd_re: val_inject f (snd (ti hadt)) (snd (ti ladt));
          init_re: init hadt = init ladt;
          
          buffer_re: buffer hadt = buffer ladt;

          CPU_ID_re: CPU_ID hadt = CPU_ID ladt;
          cid_re: cid hadt = cid ladt;
          multi_oracle_re: multi_oracle hadt = multi_oracle ladt;
          multi_log_re: multi_log hadt = multi_log ladt;
          com1_re: com1 ladt = com1 hadt;
          ioapic_re: ioapic ladt = ioapic hadt;
          lapic_re: lapic ladt = lapic hadt;
          intr_flag_re: intr_flag ladt = intr_flag hadt;
          saved_intr_flags_re: saved_intr_flags ladt = saved_intr_flags hadt;
          curr_intr_num_re: curr_intr_num ladt = curr_intr_num hadt;
          in_intr_re: in_intr hadt = in_intr ladt;
          tf_re: tfs_inj f (tf hadt) (tf ladt)
        }.

    Inductive match_RData: stencil → HDATA → mem → meminj → Prop :=
    | MATCH_RDATA: ∀ habd m f s, match_RData s habd m f.

    Local Hint Resolve MATCH_RDATA.

    Global Instance rel_ops: CompatRelOps HDATAOps LDATAOps :=
      {
        relate_AbData s f d1 d2 := relate_RData f d1 d2;
        match_AbData s d1 m f := match_RData s d1 m f;
        new_glbl := nil
      }.

    Section Rel_Property.

      Lemma relate_incr:
        ∀ abd abd´ f f´,
          relate_RData f abd abd´
          → inject_incr f f´
          → relate_RData f´ abd abd´.
      Proof.
        inversion 1; subst; intros; inv H; constructor; eauto.
        eapply tfs_inj_incr; eauto.
      Qed.

      Global Instance rel_prf: CompatRel HDATAOps LDATAOps.
      Proof.
        constructor; intros; simpl; trivial.
        eapply relate_incr; eauto.
      Qed.

    End Rel_Property.

    Section OneStep_Forward_Relation.

      Section FRESH_PRIM.

        Lemma acquire_shared_exist:
          ∀ habd habd´ labd n ofs i l f,
            acquire_shared1_spec0 n ofs habd = Some (habd´, i, l)
            → relate_RData f habd labd
            → ∃ labd´, acquire_shared0_spec0 n ofs labd = Some (labd´, i, l) ∧ relate_RData f habd´ labd´
                             ∧ Shared2ID0 n = Some i.
        Proof.
          unfold acquire_shared0_spec, acquire_shared1_spec. intros until f.
          intros HP HR; pose proof HR as HR´; inv HR; revert HP; simpl; subrewrite.
          subdestruct;
          inv HQ; refine_split; eauto.
          destruct (GetSharedMemEvent l0); trivial.
          inv HR´; constructor; eauto.
        Qed.

        Lemma acquire_shared_sim:
          ∀ id,
            sim (crel RData RData)
                (id ↦ primcall_acquire_shared_compatsem acquire_shared1_spec0)
                (id ↦ primcall_acquire_shared_compatsem acquire_shared0_spec0).
        Proof.
          intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
          inv match_extcall_states.
          exploit acquire_shared_exist; eauto 1; intros (labd´ & HP & HM & Hs).
          eapply (extcall_args_with_data (D:= HDATAOps) d1) in H10.
          destruct l; subst.
          {
            exploit Mem.storebytes_mapped_inject; eauto.
            { eapply stencil_find_symbol_inject´; eauto. }
            { eapply list_forall2_bytelist_inject; eauto. }
            intros (m2´ & Hst & Hinj).
            exploit (extcall_args_inject (D1:= HDATAOps) (D2:= HDATAOps) d1 d2); eauto.
            intros (varg´ & Hargs & Hlist).
            eapply extcall_args_without_data in Hargs.
            refine_split;
              match goal with
                | |- inject_incr ?f ?f ⇒ apply inject_incr_refl
                | _ ⇒ (econstructor; eauto ; try congruence)
              end;
              match goal with
                | |- _ PC = Vptr _ _ ⇒ eapply reg_symbol_inject; eassumption
                | |- _ → val_inject _ _ _ ⇒ val_inject_simpl
                | _ ⇒ idtac
              end.
            simpl; eauto.
            econstructor; eauto ; try congruence.
            -
              constructor.
            -
              erewrite Mem.nextblock_storebytes; eauto.
              eapply Mem.nextblock_storebytes in Hst; eauto.
              rewrite Hst. assumption.
            -
              intros. red; intros. inv H.
            -
              subst rs´.
              val_inject_simpl.
          }
          {
            exploit (extcall_args_inject (D1:= HDATAOps) (D2:= HDATAOps) d1 d2); eauto.
            intros (varg´ & Hargs & Hlist).
            eapply extcall_args_without_data in Hargs.
            refine_split;
              match goal with
                | |- inject_incr ?f ?f ⇒ apply inject_incr_refl
                | _ ⇒ (econstructor; eauto ; try congruence)
              end;
              match goal with
                | |- _ PC = Vptr _ _ ⇒ eapply reg_symbol_inject; eassumption
                | |- _ → val_inject _ _ _ ⇒ val_inject_simpl
                | _ ⇒ idtac
              end.
            simpl; eauto.
            econstructor; eauto ; try congruence.
            -
              constructor.
            -
              subst rs´.
              val_inject_simpl.
          }
        Qed.

        Lemma release_shared_exist:
          ∀ habd habd´ labd n ofs e f,
            release_shared1_spec0 n ofs e habd = Some habd´
            → relate_RData f habd labd
            → ∃ labd´, release_shared0_spec0 n ofs e labd = Some labd´ ∧ relate_RData f habd´ labd´.
        Proof.
          unfold release_shared0_spec, release_shared1_spec. intros until f.
          intros HP HR; pose proof HR as HR´; inv HR; revert HP; simpl; subrewrite.
          subdestruct. inv HQ.
          refine_split; eauto.
          inv HR´; constructor; eauto.
        Qed.

        Lemma release_shared_sim:
          ∀ id,
            sim (crel RData RData)
                (id ↦ primcall_release_lock_compatsem id release_shared1_spec0)
                (id ↦ primcall_release_lock_compatsem id release_shared0_spec0).
        Proof.
          intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
          inv match_extcall_states.
          exploit release_shared_exist; eauto 1; intros (labd´ & HP & HM).
          eapply (extcall_args_with_data (D:= HDATAOps) d1) in H11.
          exploit (extcall_args_inject (D1:= HDATAOps) (D2:= HDATAOps) d1 d2); eauto.
          intros (varg´ & Hargs & Hlist).
          eapply extcall_args_without_data in Hargs.
          refine_split;
            match goal with
              | |- inject_incr ?f ?f ⇒ apply inject_incr_refl
              | _ ⇒ (econstructor; try eapply H7; eauto ; try congruence)
            end;
            match goal with
              | |- _ PC = Vptr _ _ ⇒ eapply reg_symbol_inject; eassumption
              | |- _ → val_inject _ _ _ ⇒ val_inject_simpl
              | _ ⇒ idtac
            end.
          - exploit Mem.loadbytes_inject; eauto.
            { eapply stencil_find_symbol_inject´; eauto. }
            intros (bytes2 & HLD & Hlist).
            eapply list_forall2_bytelist_inject_eq in Hlist. subst.
            change (0 + 0) with 0 in HLD. trivial.
          - econstructor; eauto ; try congruence.
            constructor.
          -
            subst rs´.
            val_inject_simpl.
        Qed.

        Lemma page_copy_exist:
          ∀ s habd habd´ labd index i from f,
            page_copy´´_spec index i from habd = Some habd´
            → relate_AbData s f habd labd
            → ∃ labd´, page_copy´´´_spec index i from labd = Some labd´
                             ∧ relate_AbData s f habd´ labd´.
        Proof.
          unfold page_copy´´_spec, page_copy´´´_spec.
          intros until f.
          intros HP HR; pose proof HR as HR´; inv HR; revert HP; simpl; subrewrite.
          subdestruct;
            inv HQ; refine_split; eauto.
          - exploit page_copy_aux_exists; eauto.
            intros HCopy´.
            rewrite HCopy´. trivial.
          - inv HR´; constructor; eauto.
        Qed.

        Lemma page_copy_sim:
          ∀ id,
            sim (crel RData RData) (id ↦ gensem page_copy´´_spec)
                (id ↦ gensem page_copy´´´_spec).
        Proof.
          intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
          exploit page_copy_exist; eauto 1. intros [labd´ [HP HM]].
          refine_split;
            match goal with
              | |- inject_incr ?f ?f ⇒ apply inject_incr_refl
              | _ ⇒ (econstructor; eauto ; try congruence)
            end;
            match goal with
              | |- _ PC = Vptr _ _ ⇒ eapply reg_symbol_inject; eassumption
              | |- _ → val_inject _ _ _ ⇒ val_inject_simpl
              | _ ⇒ idtac
            end.
          - repeat econstructor; eauto ; try congruence.
          - constructor.
        Qed.

        Lemma ticket_lock_init_exist:
          ∀ habd habd´ labd n f,
            ticket_lock_init0_spec n habd = Some habd´
            → relate_RData f habd labd
            → ∃ labd´, ticket_lock_init_spec n labd = Some labd´ ∧ relate_RData f habd´ labd´.
        Proof.
          unfold ticket_lock_init_spec, ticket_lock_init0_spec; intros until f; exist_simpl.
        Qed.

        Lemma ticket_lock_init_sim:
          ∀ id,
            sim (crel RData RData) (id ↦ gensem ticket_lock_init0_spec)
                (id ↦ gensem ticket_lock_init_spec).
        Proof.
          intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
          exploit ticket_lock_init_exist; eauto 1. intros [labd´ [HP HM]].
          match_external_states_simpl.
        Qed.

        Lemma pass_lock_exist:
          ∀ habd habd´ labd n ofs f,
            pass_qlock_spec n ofs habd = Some habd´
            → relate_RData f habd labd
            → ∃ labd´, pass_lock_spec n ofs labd = Some labd´ ∧ relate_RData f habd´ labd´.
        Proof.
          unfold pass_lock_spec, pass_qlock_spec; intros until f.
          intros HP HR; pose proof HR as HR´; inv HR; revert HP; simpl.
          subrewrite´.
          intros HQ; subdestruct; inv HQ.
          refine_split´; simpl; trivial.
          constructor; simpl; inv HR´; trivial.
        Qed.

        Lemma pass_lock_sim:
          ∀ id,
            sim (crel RData RData) (id ↦ gensem pass_qlock_spec)
                (id ↦ gensem pass_lock_spec).
        Proof.
          intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
          exploit pass_lock_exist; eauto 1. intros [labd´ [HP HM]].
          match_external_states_simpl.
        Qed.

        Section CALLOCK_LEMMA.

          Local Transparent Q_CalTicketLock Q_CalLock Q_CalTicketWait Q_CalWait CalTicketLock CalTicketWait.

          Lemma Q_CalLock_imply_ticket:
            ∀ l self_c other_c b q tq
                   (Hqcal_lock: Q_CalLock l = Some (self_c, other_c, b, q, tq)),
            ∃ n, Q_CalTicketLock l = Some (n, self_c, other_c, b, q, tq).
          Proof.
            induction l; intros.
            - inv Hqcal_lock. simpl. eauto.
            - simpl in ×. destruct a; contra_inv.
              destruct (Q_CalLock l) eqn: Hlock; contra_inv.
              repeat destruct p.
              exploit IHl; eauto.
              intros (n1 & ->).
              subdestruct; inv Hqcal_lock; eauto.
          Qed.

          Lemma Q_CalWait_imply_ticket:
            ∀ wait_time curid l o l0
                   (Hqcal_wait: Q_CalWait wait_time curid l o = Some l0),
              Q_CalTicketWait wait_time curid l o = Some l0.
          Proof.
            induction wait_time; intros.
            - inv Hqcal_wait.
            - simpl in ×.
              destruct (Q_CalLock (o curid l ++ l)) eqn: Hlock; contra_inv.
              repeat (destruct p).
              eapply Q_CalLock_imply_ticket in Hlock.
              destruct Hlock as (n1 & ->).
              subdestruct; eauto.
          Qed.

          Lemma CalTicketLock_Q_imply:
            ∀ l n self_c other_c b q tq
                   (Hqlock: Q_CalTicketLock l = Some (n, self_c, other_c, b, q, tq)),
              CalTicketLock l = Some (n + Z.of_nat (length q), n, tq).
          Proof.
            induction l; intros.
            - inv Hqlock. simpl. trivial.
            - simpl in ×.
              destruct a; contra_inv.
              destruct (Q_CalTicketLock l) eqn: Hqlock1; contra_inv.
              repeat (destruct p).
              exploit IHl; eauto.
              intros Heq; rewrite Heq; clear Heq.
              destruct l1; contra_inv.
              + simpl. destruct l0; contra_inv.
                destruct e; contra_inv.
                destruct e; contra_inv. inv Hqlock.
                simpl. replace (n + 0 + 1) with (n + 1) by omega. trivial.
              + destruct l0; contra_inv.
                destruct (zeq i z0); subst.
                × destruct h.
                  {
                    destruct e; contra_inv.
                    destruct e; contra_inv.
                    inv Hqlock. trivial.
                  }
                  {
                    destruct e; contra_inv.
                    destruct e; contra_inv.
                    inv Hqlock. trivial.
                  }
                  {
                    destruct e; contra_inv.
                    - destruct e; contra_inv.
                      inv Hqlock.
                      Local Opaque Z.of_nat.
                      simpl. rewrite Nat2Z.inj_succ.
                      replace (z + Z.succ (Z.of_nat (length q))) with (z + 1 + Z.of_nat (length q)) by omega.
                      trivial.
                    - destruct n1; contra_inv.
                      inv Hqlock. trivial.
                  }
                × destruct n0; contra_inv.
                  destruct e; contra_inv.
                  destruct e; contra_inv.
                  {
                    destruct (in_dec zeq i l1); contra_inv.
                    inv Hqlock.
                    repeat rewrite app_comm_cons.
                    rewrite app_length. simpl.
                    replace ((length l1 + 1)%nat) with (S (length l1)).
                    repeat rewrite Nat2Z.inj_succ.
                    replace (n + Z.succ (Z.of_nat (length l1)) + 1)
                    with (n + Z.succ (Z.succ (Z.of_nat (length l1)))).
                    trivial.
                    omega.
                    replace ((length l1 + 1)%nat) with ((1 + length l1)%nat).
                    trivial. omega.
                  }
                  {
                    inv Hqlock. trivial.
                  }
          Qed.

          Lemma Q_CalTicketLock_in_head´:
            ∀ l´ l n n´ b b´ q q0 q1 curid self_c self_c´ other_c other_c´ tq tq´
                   (Hqlock : Q_CalTicketLock l = Some (n, self_c, other_c, b, q ++ curid :: q0, tq))
                   (HnotIn: ¬ In curid q)
                   (Hin: ∀ i0 e, In (TEVENT i0 e) l´ → i0 ≠ curid)
                   (Hqlock1 : Q_CalTicketLock (l´ ++ l) = Some (n´, self_c´, other_c´, b´, q1, tq´)),
              In curid q1.
          Proof.
            induction l´; intros.
            - simpl in Hqlock1. rewrite Hqlock in Hqlock1. inv Hqlock1.
              eapply list_In_middle.
            - rewrite <- app_comm_cons in Hqlock1.
              destruct a. simpl in Hqlock1.
              destruct (Q_CalTicketLock (l´ ++ l)) eqn: Hqlock2; contra_inv.
              assert (Hin_append:
                        ∀ i0 e,
                          In (TEVENT i0 e) l´ → i0 ≠ curid).
              { eapply list_valid_In_append; eauto. }
              subdestruct; inv Hqlock1; try (exploit IHl´; eauto 1; fail).
              + exploit IHl´; try eassumption.
                intros. inv H.
              + exploit IHl´; try eassumption.
                specialize (Hin z0 (TTICKET INC_NOW)).
                intros HF. eapply in_inv in HF.
                destruct HF as [HF´|HF´]; trivial.
                subst. elim Hin. left. trivial. trivial.
              + exploit IHl´; try eassumption.
                rewrite app_comm_cons.
                intros. eapply in_or_app. eauto.
          Qed.

          Lemma Q_CalTicketLock_neq_head´:
            ∀ l´ l n n´ b b´ q q0 q1 curid head self_c self_c´ other_c other_c´ tq tq´
                   (Hqlock : Q_CalTicketLock l = Some (n, self_c, other_c, b, q ++ curid :: q0, tq))
                   (HnotIn: ¬ In curid q)
                   (Hin: ∀ i0 e, In (TEVENT i0 e) l´ → i0 ≠ curid)
                   (Hqlock1 : Q_CalTicketLock (l´ ++ l) = Some (n´, self_c´, other_c´, b´, head :: q1, tq´))
                   (Hnot_head: head ≠ curid),
            ∃ q2 q3, q1 = q2 ++ curid :: q3
                          ∧ n´ + Z.of_nat (length (head :: q2)) = n + Z.of_nat (length q)
                          ∧ ¬ In curid q2.
          Proof.
            induction l´; intros.
            - simpl in Hqlock1. rewrite Hqlock in Hqlock1. inv Hqlock1.
              destruct q.
              { inv H4. elim Hnot_head. trivial. }
              rewrite <- list_append_trans in H4. inv H4.
              refine_split´; trivial.
              eapply list_not_in_append_re; eauto.
            - rewrite <- app_comm_cons in Hqlock1.
              destruct a. simpl in Hqlock1.
              destruct (Q_CalTicketLock (l´ ++ l)) eqn: Hqlock2; contra_inv.
              assert (Hin_append:
                        ∀ i0 e,
                          In (TEVENT i0 e) l´ → i0 ≠ curid).
              { eapply list_valid_In_append; eauto. }
              subdestruct; inv Hqlock1.
              + exploit Q_CalTicketLock_in_head´; try eapply Hqlock2; eauto.
                intros HF. inv HF.
              + exploit IHl´; try eassumption.
                intros (q2 & q3 & Heq & Heq´ & HnotIn1). subst.
                refine_split´; trivial.
              + exploit IHl´; try eassumption.
                intros (q2 & q3 & Heq & Heq´ & HnotIn1). subst.
                refine_split´; trivial.
              + exploit IHl´; try eassumption.
                {
                  specialize (Hin z0 (TTICKET INC_NOW)).
                  eapply Hin.
                  left; trivial.
                }
                intros (q2 & q3 & Heq & Heq´ & HnotIn1). subst.
                destruct q2; inv Heq.
                {
                  elim Hnot_head. trivial.
                }
                refine_split´; trivial.
                {
                  rewrite <- Heq´.
                  simpl. xomega.
                }
                eapply list_not_in_append_re; eauto.

              + exploit IHl´; try eassumption.
                intros (q2 & q3 & Heq & Heq´ & HnotIn1). subst.
                refine_split´; trivial.
              + exploit IHl´; try eassumption.
                intros (q2 & q3 & Heq & Heq´ & HnotIn1). subst.
                refine_split´; trivial.
              + exploit Q_CalTicketLock_in_head´; try eapply Hqlock2; eauto.
                intros HF.
                exploit IHl´; try eassumption.
                intros (q2 & q3 & Heq & Heq´ & HnotIn1). subst.
                rewrite <- app_assoc.
                rewrite <- app_comm_cons.
                refine_split´; trivial.
              + exploit IHl´; try eassumption.
                intros (q2 & q3 & Heq & Heq´ & HnotIn1). subst.
                refine_split´; trivial.
          Qed.

          Lemma Q_CalTicketLock_eq_head´:
            ∀ l´ l n n´ b b´ q q0 q1 curid self_c self_c´ other_c other_c´ tq tq´
                   (Hqlock : Q_CalTicketLock l = Some (n, self_c, other_c, b, q ++ curid :: q0, tq))
                   (HnotIn: ¬ In curid q)
                   (Hin: ∀ i0 e, In (TEVENT i0 e) l´ → i0 ≠ curid)
                   (Hqlock1 : Q_CalTicketLock (l´ ++ l) = Some (n´, self_c´, other_c´, b´, curid :: q1, tq´)),
              n´ = n + Z.of_nat (length q).
          Proof.
            induction l´; intros.
            - simpl in Hqlock1. rewrite Hqlock in Hqlock1. inv Hqlock1.
              eapply list_prefix_nil in HnotIn; eauto. subst. simpl.
              Local Transparent Z.of_nat. xomega.
            - rewrite <- app_comm_cons in Hqlock1.
              destruct a. simpl in Hqlock1.
              destruct (Q_CalTicketLock (l´ ++ l)) eqn: Hqlock2; contra_inv.
              assert (Hin_append:
                        ∀ i0 e,
                          In (TEVENT i0 e) l´ → i0 ≠ curid).
              { eapply list_valid_In_append; eauto. }
              subdestruct; inv Hqlock1; try (exploit IHl´; eauto 1; fail).
              + exploit Q_CalTicketLock_in_head´; try eapply Hqlock2; eauto.
                intros HF. inv HF.
              + exploit Q_CalTicketLock_neq_head´; try eapply Hqlock2; eauto.
                {
                  specialize (Hin z0 (TTICKET INC_NOW)).
                  eapply Hin.
                  left; trivial.
                }
                intros (q2 & q3 & Heq & Heq´ & Hin´).
                eapply list_prefix_nil in Hin´; eauto. subst. simpl in Heq´. trivial.
          Qed.

          Lemma Q_CalTicketLock_eq_head:
            ∀ l n n´ b b´ q q0 q1 curid self_c self_c´ other_c other_c´ tq tq´ o
                   (Hqlock : Q_CalTicketLock l = Some (n, self_c, other_c, b, q ++ curid :: q0, tq))
                   (HnotIn: ¬ In curid q)
                   (Horacle_domain : valid_multi_oracle_domain o)
                   (Hqlock1 : Q_CalTicketLock (o curid l ++ l) = Some (n´, self_c´, other_c´, b´, curid :: q1, tq´)),
              n´ = n + Z.of_nat (length q).
          Proof.
            intros. eapply Q_CalTicketLock_eq_head´; eauto.
            intros. eapply Horacle_domain; eauto.
          Qed.

          Lemma Q_CalTicketLock_neq_head:
            ∀ l n n´ b b´ q q0 q1 curid head self_c self_c´ other_c other_c´ tq tq´ o
                   (Hqlock : Q_CalTicketLock l = Some (n, self_c, other_c, b, q ++ curid :: q0, tq))
                   (HnotIn: ¬ In curid q)
                   (Horacle_domain : valid_multi_oracle_domain o)
                   (Hqlock1 : Q_CalTicketLock (o curid l ++ l) = Some (n´, self_c´, other_c´, b´, head :: q1, tq´))
                   (Hnot_head: head ≠ curid),
            n´ < n + Z.of_nat (length q)
            ∧ (∃ q2 q3, q1 = q2 ++ curid :: q3
                          ∧ n´ + Z.of_nat (length (head :: q2)) = n + Z.of_nat (length q)
                          ∧ ¬ In curid q2).
          Proof.
            intros. exploit Q_CalTicketLock_neq_head´; eauto.
            {
              intros. eapply Horacle_domain; eauto.
            }
            intros (q2 & q3 & Heq & Hn´ & HnotIn1).
            refine_split´; eauto.
            rewrite <- Hn´. simpl. xomega.
          Qed.

          Lemma CalTicketWait_Q_imply:
            ∀ wait_time curid l o l0 n self_c other_c b q q0 tq t
                   (Hqlock: Q_CalTicketLock l = Some (n, self_c, other_c, b, q ++ curid :: q0, tq))
                   (Hwait: Q_CalTicketWait wait_time curid l o = Some l0)
                   (HnotIn: ¬ In curid q)
                   (Ht: t = n + Z.of_nat (length (q)))
                   (Horacle_domain : valid_multi_oracle_domain o),
              CalTicketWait wait_time curid t l o = Some l0.
          Proof.
            induction wait_time; intros; simpl in *; try (inv Hwait; fail).
            destruct (Q_CalTicketLock (o curid l ++ l)) eqn: Hqlock1; contra_inv.
            repeat (destruct p).
            exploit CalTicketLock_Q_imply; eauto.
            intros Heq; rewrite Heq; clear Heq.
            destruct l2; contra_inv; destruct l1; contra_inv.
            destruct (zeq curid z0); subst.
            + destruct h; contra_inv.
              rewrite zeq_true in Hwait. inv Hwait.
              exploit Q_CalTicketLock_eq_head; eauto.
              intros; subst.
              rewrite zeq_true. trivial.
            + subdestruct.
              × inv Hwait. exploit Q_CalTicketLock_eq_head; eauto.
                intros; subst.
                rewrite zeq_true. trivial.
              × exploit Q_CalTicketLock_neq_head; eauto.
                intros (Hlt & (q2 & q3 & Heq & Hz & HnotIn1)). subst.
                eapply list_not_in_append in HnotIn1; eauto.
                rewrite zeq_false.
                exploit IHwait_time; try eapply Hwait; eauto.
                {
                  simpl. rewrite Hqlock1.
                  rewrite zeq_false; auto.
                }
                rewrite <- Hz. trivial.
                omega.
          Qed.

          Lemma CalTicketWait_Q_imply´:
            ∀ wait_time curid l l´ o l0 n self_c other_c b q tq t bound
                   (Hl: l = TEVENT curid (TTICKET (INC_TICKET bound)) :: l´)
                   (Hqlock: Q_CalTicketLock l = Some (n, self_c, other_c, b, q, tq))
                   (Hwait: Q_CalTicketWait wait_time curid l o = Some l0)
                   (Ht: t = n + Z.of_nat (length (q)) - 1)
                   (Horacle_domain : valid_multi_oracle_domain o),
              CalTicketWait wait_time curid t l o = Some l0.
          Proof.
            intros. subst.
            assert (Hq: ∃ q0, q = q0 ++ (curid::nil) ∧ ¬ In curid q0).
            {
              simpl in Hqlock. subdestruct; inv Hqlock.
              - ∃ nil.
                split; trivial.
                intros HF; inv HF.
              - ∃ (z0 :: l3).
                split; trivial.
                intros HF; inv HF; try congruence.
            }
            destruct Hq as (q0 & Hq & HnotIn); subst.
            eapply CalTicketWait_Q_imply; eauto.
            rewrite app_length. simpl.
            replace ((length q0 + 1)%nat) with (S (length q0)) by omega.
            repeat rewrite Nat2Z.inj_succ.
            omega.
          Qed.

        End CALLOCK_LEMMA.

        Lemma l_len_cons:
          ∀ {A:Type} (z: A) l,
            Z.of_nat (length (z :: l)) = Z.of_nat (length l) + 1.
        Proof.
          Local Opaque Z.of_nat.
          simpl; intros.
          rewrite Nat2Z.inj_succ. omega.
        Qed.

        Local Transparent Z.of_nat.

        Lemma q_unique:
          ∀ n q (Hrange: ∀ i, In i q → 0 ≤ i < Z.of_nat n)
                 (Hcount: ∀ i, In i q → count_occ zeq q i = 1%nat),
            Z.of_nat (length q) < Z.of_nat n + 1.
        Proof.
          induction n; intros.
          - destruct q.
            + simpl; omega.
            + exploit (Hrange z); eauto.
              left; trivial. simpl; intros. omega.
          - destruct (in_dec zeq (Z.of_nat (n)) q).
            + eapply in_split in i.
              destruct i as (l1 & l2 & Heq); subst.
              assert (Hlen: Z.of_nat (length (l1 ++ l2)) < Z.of_nat n + 1).
              {
                assert (Hnot: ¬ In (Z.of_nat n) (l1 ++ l2)).
                {
                  intro HF.
                  exploit (Hcount (Z.of_nat n)).
                  - eapply in_or_app. right.
                    left. trivial.
                  - rewrite count_occ_append.
                    rewrite count_occ_cons_eq; trivial.
                    intros.
                    eapply in_app_or in HF.
                    destruct HF.
                    {
                      eapply (count_occ_In zeq) in H0.
                      omega.
                    }
                    {
                      eapply (count_occ_In zeq) in H0.
                      omega.
                    }
                }
                eapply IHn; eauto.
                - intros. destruct (zeq i (Z.of_nat n)); subst.
                  + congruence.
                  + exploit (Hrange i).
                    × eapply in_app_or in H. destruct H.
                      {
                        eapply in_or_app. left. trivial.
                      }
                      {
                        eapply in_or_app. right. right. trivial.
                      }
                    × rewrite Nat2Z.inj_succ.
                      intros. omega.
                - intros. rewrite count_occ_append.
                  destruct (zeq i (Z.of_nat n)); subst. congruence.
                  exploit (Hcount i); eauto.
                  + eapply in_app_or in H. destruct H.
                    × eapply in_or_app. left. trivial.
                    × eapply in_or_app. right. right. trivial.
                  + rewrite count_occ_append.
                    rewrite count_occ_cons_neq; auto.
              }
              rewrite Nat2Z.inj_succ.
              rewrite app_length in ×.
              rewrite Nat2Z.inj_add in ×.
              rewrite l_len_cons. omega.
            + exploit IHn; eauto.
              × intros. exploit Hrange; eauto.
                rewrite Nat2Z.inj_succ.
                intros.
                destruct (zeq i (Z.of_nat n)); subst.
                {
                  elim n0; trivial.
                }
                {
                  omega.
                }
              × intros.
                rewrite Nat2Z.inj_succ.
                omega.
        Qed.

        Lemma wait_lock_exist:
          ∀ habd habd´ labd bound n ofs f
                 (Hhigh: MQTicketLockOp.high_level_invariant habd),
            wait_qlock_spec bound n ofs habd = Some habd´
            → relate_RData f habd labd
            → ∃ labd´, wait_lock_spec bound n ofs labd = Some labd´ ∧ relate_RData f habd´ labd´.
        Proof.
          unfold wait_lock_spec, wait_qlock_spec; intros until f. intro.
          intros HP HR; pose proof HR as HR´; inv HR; revert HP; simpl.
          subrewrite´.
          intros HQ; subdestruct; inv HQ.
          assert (Hlt: Z.of_nat (length l1) < TOTAL_CPU + 1).
          {
            inv Hhigh.
            assert (Hlen: qlock_length (TEVENT (CPU_ID labd) (TTICKET (INC_TICKET (Z.to_nat bound)))
                                               :: ZMap.get z (multi_oracle labd) (CPU_ID labd) l ++ l)).
            {
              rewrite <- CPU_ID_re0, <- multi_oracle_re0.
              eapply qlock_length_cons; eauto.
              eapply qlock_length_append; eauto.
              - eapply qlock_pool_length_inv; eauto.
                subrewrite´; trivial.
              - intros. eapply valid_multi_oracle_pool_inv; eauto.
            }
            unfold qlock_length in Hlen.
            specialize (Hlen _ _ _ _ _ Hdestruct4).
            pose proof (Q_CalLock_unique _ _ _ _ _ _ Hdestruct4).
            specialize (q_unique (8%nat)). simpl.
            intros HF. eapply HF; eauto.
          }
          eapply Q_CalLock_imply_ticket in Hdestruct4.
          destruct Hdestruct4 as (n2 & HCalTL).
          eapply Q_CalWait_imply_ticket in Hdestruct9.
          exploit CalTicketWait_Q_imply´; eauto.
          {
            rewrite <- multi_oracle_re0.
            eapply valid_multi_oracle_pool_inv; eauto.
          }
          intros Heq.
          eapply CalTicketLock_Q_imply in HCalTL. rewrite HCalTL.
          rewrite zlt_true.
          rewrite Heq; clear Heq.
          refine_split´; trivial.
          constructor; simpl; inv HR´; trivial.
          omega.
        Qed.

        Lemma wait_lock_sim:
          ∀ id,
            sim (crel RData RData) (id ↦ gensem wait_qlock_spec)
                (id ↦ gensem wait_lock_spec).
        Proof.
          intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
          exploit wait_lock_exist; eauto 1. intros [labd´ [HP HM]].
          match_external_states_simpl.
        Qed.

      End FRESH_PRIM.

      Section PASSTHROUGH_RPIM.

        Global Instance: (LoadStoreProp (hflatmem_store:= flatmem_store´) (lflatmem_store:= flatmem_store´)).
        Proof.
          accessor_prop_tac.
          - eapply flatmem_store´_exists; eauto.
        Qed.

        Lemma passthrough_correct:
          sim (crel HDATA LDATA) mqticketlockop mticketlockop.
        Proof.
          unfold mqticketlockop.
          unfold mqticketlockop_fresh.
          rewrite id_left.
          sim_oplus.
          - apply fload´_sim.
          - apply fstore´_sim.
          - apply page_copy_sim.
          - apply page_copy_back´_sim.

          - apply vmxinfo_get_sim.
          - apply setPG_sim.
          - apply setCR3_sim.
          - apply get_size_sim.
          - apply is_mm_usable_sim.
          - apply get_mm_s_sim.
          - apply get_mm_l_sim.
          - apply get_CPU_ID_sim.
          - apply release_shared_sim.
          - apply acquire_shared_sim.
          - apply get_curid_sim.
          - apply set_curid_sim.
          - apply set_curid_init_sim.
          - apply ticket_lock_init_sim.
          - apply pass_lock_sim.
          - apply wait_lock_sim.
          - apply trapin_sim.
          - apply trapout´_sim.
          - apply hostin_sim.
          - apply hostout´_sim.
          - apply proc_create_postinit_sim.
          - apply trap_info_get_sim.
          - apply trap_info_ret_sim.
          - apply serial_irq_check_sim.
          - apply iret_sim.
          - apply cli_sim.
          - apply sti_sim.
          - apply serial_irq_current_sim.
          - apply ic_intr_sim.
          - apply save_context_sim.
          - apply restore_context_sim.
          - apply local_irq_save_sim.
          - apply local_irq_restore_sim.
          - apply serial_in_sim.
          - apply serial_out_sim.
          - apply serial_hw_intr_sim.
          - apply ioapic_read_sim.
          - apply ioapic_write_sim.
          - apply lapic_read_sim.
          - apply lapic_write_sim.
          - layer_sim_simpl.
            + eapply load_correct1.
            + eapply store_correct1.
        Qed.

      End PASSTHROUGH_RPIM.

    End OneStep_Forward_Relation.

  End WITHMEM.

End Refinement.