Library mcertikos.mcslock.HMCSLockOpGen


This file provide the contextual refinement proof between MALInit layer and MALOp layer
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 LAsmModuleSemAux.
Require Import TacticsForTesting.
Require Import ListLemma2.

Require Import AbstractDataType.
Require Import DeviceStateDataType.

Require Import ZSet.
Require Import HMCSLockOpGenDef.
Require Import CalMCSLock.
Require Import CalMCSLockLemmas.
Require Import INVLemmaQSLock.
Require Import StarvationFreedomMCSLockPassLock.
Require Import StarvationFreedomMCSLockWaitLock.

Require Export MQMCSLockOp.
Require Export MHMCSLockOp.

Require Import ObjQLock.

Notation of the refinement relation

Section Refinement.

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

  Context `{real_params: RealParams}.
  Context `{mcs_oracle_prop: MCSOracleProp}.

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

  Notation HDATAOps := (cdata (cdata_ops := mhticketlockop_data_ops) HDATA).
  Notation LDATAOps := (cdata (cdata_ops := mqmcslockop_data_ops) LDATA).

  Section WITHMEM.

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

Definition the refinement relation: relate_RData + match_RData

    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;

          CPU_ID_re: CPU_ID hadt = CPU_ID ladt;
          cid_re: cid hadt = cid ladt;
          mcs_oracle_re: relate_mcs_oracle_pool (multi_oracle hadt) (multi_oracle ladt);
          mcs_log_re: relate_mcs_log_pool (multi_log hadt) (multi_log ladt);
          lock_re: lock hadt = lock 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
      }.

Properties of relations

    Section Rel_Property.

Prove that after taking one step, the refinement relation still holds
      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.

Proofs the one-step forward simulations for the low level specifications

    Section OneStep_Forward_Relation.

      Lemma update_abd_log : ∀ abid f habd labd hl ll tq LOCK,
        relate_RData f habd labd →
        relate_mcs_log ll = Some (hl,tq) →
        relate_RData f
                     (habd {multi_log : ZMap.set abid (MultiDef hl) (multi_log habd)})
                     {lock : ZMap.set abid LOCK (lock habd)}
                     (labd {multi_log : ZMap.set abid (MultiDef ll) (multi_log labd)})
                     {lock : ZMap.set abid LOCK (lock labd)}.
          intros.
          inv H; econstructor; simpl; try auto.
          econstructor.
          - intros.
            inv mcs_log_re0.
            eapply Hrelate_mcs_log_type in Hrange.
            case_eq (zeq z abid); intros; subst.
            + repeat rewrite ZMap.gss.
              econstructor; eauto.
            + repeat rewrite ZMap.gso; eauto.
          - rewrite lock_re0; reflexivity.
      Qed.

      Section FRESH_PRIM.

        Lemma relate_log_shared:
          ∀ l1 l0 tq
                 (Hre: relate_mcs_log l1 = Some (l0, tq)),
            GetSharedMemEvent l0 = GetSharedMemEvent l1.
        Proof.
          induction l1; simpl; intros.
          - inv Hre. trivial.
          - subdestruct; inv Hre; simpl; eauto.
            destruct e0; eauto.
        Qed.

        Lemma relate_log_buffer:
          ∀ l1 l0 tq
                 (Hre: relate_mcs_log l1 = Some (l0, tq)),
            GetSharedBuffer l0 = GetSharedBuffer l1.
        Proof.
          induction l1; simpl; intros.
          - inv Hre. trivial.
          - subdestruct; inv Hre; simpl; eauto.
            destruct e0; eauto.
        Qed.

        Lemma relate_mcs_log_shared:
          ∀ curid l l´ e
                 (Hlog: relate_mcs_log_type (MultiDef l) (MultiDef l´)),
            relate_mcs_log_type (MultiDef (TEVENT curid (TSHARED e) :: l))
                                (MultiDef (TEVENT curid (TSHARED e) :: l´)).
        Proof.
          intros.
          inv Hlog.
          econstructor.
         simpl.
         rewrite Hrelate_mcs_log.
         reflexivity.
        Qed.

        Lemma acquire_shared_exist:
          ∀ habd habd´ labd (Hhigh: MQMCSLockOp.high_level_invariant labd) n ofs i l f,
            acquire_shared_spec0 n ofs habd = Some (habd´, i, l)
            → relate_RData f habd labd
            → ∃ labd´, acquire_shared1_mcs_spec0 n ofs labd = Some (labd´, i, l) ∧ relate_RData f habd´ labd´
                             ∧ Shared2ID0 n = Some i.
        Proof.
          unfold acquire_shared_spec, acquire_shared1_mcs_spec. intros until f.
          intros HP HR; pose proof HR as HR´; inv HR; revert HP; simpl; subrewrite.
          d8 subdestruct_one. inv HQ.
          inv mcs_log_re0.
          specialize (Hrelate_mcs_log_type _ _ _ Hdestruct1).
          rewrite Hdestruct5 in Hrelate_mcs_log_type.
          inv Hrelate_mcs_log_type.
          exploit relate_log_shared; eauto.
          intros Heq. rewrite <- Heq. clear Heq.
          inv Hhigh.
          exploit valid_qslock_pool_inv; eauto.
          unfold valid_qslock.
          intros (self_c & other_c & b & q & slow & tq0 & Hcal).
          assert (Hs: ∃ x, QS_CalLock (TEVENT (CPU_ID labd) (TSHARED OPULL) :: l) = Some x).
          {
            destruct p0. destruct p.
            eapply QS_CalLock_TSHARED_exists; eauto.
          }
          destruct Hs as (x & ->).
          exploit cal_qslock_pool_status_inv; eauto.
          rewrite Hdestruct3. intros (Hvalid &_).
          rewrite Hvalid; trivial.

          refine_split; eauto.
          inv HR´; constructor; eauto. simpl.

          constructor.
          intros.
          case_eq (zeq z z0); intros; subst.
          - repeat rewrite ZMap.gss.
            assert (relate_mcs_log_type (MultiDef l0) (MultiDef l)).
            { inv mcs_log_re0.
              eapply Hrelate_mcs_log_type in Hrange.
              rewrite Hdestruct5, <- H in Hrange.
              auto. }
            exploit relate_mcs_log_shared; eauto.
          - repeat rewrite ZMap.gso; eauto.
            inv mcs_log_re0.
            eapply Hrelate_mcs_log_type in Hrange; eauto.
        Qed.

        Lemma acquire_shared_sim:
          ∀ id,
            sim (crel RData RData)
                (id ↦ primcall_acquire_shared_compatsem acquire_shared_spec0)
                (id ↦ primcall_acquire_shared_compatsem acquire_shared1_mcs_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
                 (Hhigh: MQMCSLockOp.high_level_invariant labd),
            release_shared_spec0 n ofs e habd = Some habd´
            → relate_RData f habd labd
            → ∃ labd´, release_shared1_mcs_spec0 n ofs e labd = Some labd´ ∧ relate_RData f habd´ labd´.
        Proof.
          unfold release_shared_spec, release_shared1_mcs_spec. intros until f. intro.
          intros HP HR; pose proof HR as HR´; inv HR; revert HP; simpl; subrewrite.
          subdestruct. inv HQ.
          inv mcs_log_re0.
          specialize (Hrelate_mcs_log_type _ _ _ Hdestruct2).
          rewrite Hdestruct5 in Hrelate_mcs_log_type.
          inv Hrelate_mcs_log_type.
          exploit MQMCSLockOp.valid_qslock_pool_inv; eauto.
          unfold valid_qslock.
          intros (self_c & other_c & b & q & slow & tq0 & Hcal).
          repeat destruct p0.
          assert (Hs: ∃ x, QS_CalLock (TEVENT (CPU_ID labd) (TSHARED (OMEME e)) :: l0) = Some x).
          {
            eapply QS_CalLock_TSHARED_exists; eauto.
          }
          destruct Hs as (x & ->).
          exploit cal_qslock_pool_status_inv; eauto.
          rewrite Hdestruct3. intros (_ & Hvalid).
          rewrite Hvalid; trivial. rewrite zeq_true.
          refine_split; eauto.
          inv HR´; constructor; eauto. simpl.

          constructor.
          intros.
          case_eq (zeq z z0); intros; subst.
          - repeat rewrite ZMap.gss.
            assert (relate_mcs_log_type (MultiDef l) (MultiDef l0)).
            { inv mcs_log_re0.
              eapply Hrelate_mcs_log_type in Hrange.
              rewrite Hdestruct5, <- H in Hrange.
              auto. }
            exploit relate_mcs_log_shared; eauto.
          - repeat rewrite ZMap.gso; eauto.
            inv mcs_log_re0.
            eapply Hrelate_mcs_log_type in Hrange; eauto.
        Qed.

        Lemma release_shared_sim:
          ∀ id,
            sim (crel RData RData)
                (id ↦ primcall_release_lock_compatsem id release_shared_spec0)
                (id ↦ primcall_release_lock_compatsem id release_shared1_mcs_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_back_exist:
          ∀ s habd habd´ labd (Hhigh: MQMCSLockOp.high_level_invariant labd)
                 index i to f,
            page_copy_back´_spec index i to habd = Some habd´
            → relate_AbData s f habd labd
            → ∃ labd´, page_copy_back´_spec index i to labd = Some labd´
                             ∧ relate_AbData s f habd´ labd´.
        Proof.
          unfold page_copy_back´_spec.
          intros until f.
          intros HP HR; pose proof HR as HR´; inv HR; revert HP; simpl; subrewrite.
          subdestruct. inv HQ.
          inv mcs_log_re0.
          specialize (Hrelate_mcs_log_type _ _ _ Hdestruct4).
          rewrite Hdestruct5 in Hrelate_mcs_log_type.
          inv Hrelate_mcs_log_type.
          exploit relate_log_buffer; eauto.
          intros Heq. rewrite <- Heq. clear Heq.
          rewrite Hdestruct6.
          exploit page_copy_back_aux_exists; eauto.
          intros (lh´ & HCopy´ & Hinj).
          rewrite HCopy´.
          refine_split; eauto.
          inv HR´; constructor; eauto.
        Qed.

        Lemma page_copy_back_sim:
          ∀ id,
            sim (crel RData RData) (id ↦ gensem page_copy_back´_spec)
                (id ↦ gensem page_copy_back´_spec).
        Proof.
          intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
          exploit page_copy_back_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 page_copy_exist:
          ∀ s habd habd´ labd (Hhigh: MQMCSLockOp.high_level_invariant labd)
                 index i from f,
            page_copy´_spec index i from habd = Some habd´
            → relate_AbData s f habd labd
            → ∃ labd´, mcs_page_copy´´_spec index i from labd = Some labd´
                             ∧ relate_AbData s f habd´ labd´.
        Proof.
          unfold mcs_page_copy´´_spec, page_copy´_spec.
          intros until f.
          intros HP HR; pose proof HR as HR´; inv HR; revert HP; simpl; subrewrite.
          d11 subdestruct_one. inv HQ.
          inv mcs_log_re0.
          specialize (Hrelate_mcs_log_type _ _ _ Hdestruct4).
          rewrite Hdestruct5 in Hrelate_mcs_log_type.
          inv Hrelate_mcs_log_type.
          exploit relate_log_buffer; eauto.
          intros Heq.           exploit page_copy_aux_exists; eauto.
          intros HCopy´.
          rewrite HCopy´.
          inv Hhigh.
          exploit valid_qslock_pool_inv; eauto.
          unfold valid_qslock.
          intros (self_c & other_c & b & q & slow & tq0 & Hcal).
          assert (Hs: ∃ x, QS_CalLock (TEVENT (CPU_ID labd) (TSHARED (OBUFFERE l0))
                                                   :: l1) = Some x).
          { destruct p.
            destruct p.
            eapply QS_CalLock_TSHARED_exists; eauto.
          }
          destruct Hs as (x & ->).
          refine_split; eauto.
          inv HR´; constructor; eauto. simpl.

          constructor.
          intros.
          case_eq (zeq z z0); intros; subst.
          - repeat rewrite ZMap.gss.
            assert (relate_mcs_log_type (MultiDef l) (MultiDef l1)).
            { inv mcs_log_re0.
              eapply Hrelate_mcs_log_type in Hrange.
              rewrite Hdestruct5, <- H in Hrange.
              auto. }
            exploit relate_mcs_log_shared; eauto.
          - repeat rewrite ZMap.gso; eauto.
            inv mcs_log_re0.
            eapply Hrelate_mcs_log_type in Hrange; eauto.
        Qed.

        Lemma page_copy_sim:
          ∀ id,
            sim (crel RData RData) (id ↦ gensem page_copy´_spec)
                (id ↦ gensem mcs_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_init0_spec n labd = Some labd´ ∧ relate_RData f habd´ labd´.
        Proof.
          unfold ticket_lock_init0_spec; intros until f; exist_simpl.
          eauto using real_relate_mcs_log_pool.
        Qed.

        Lemma ticket_lock_init_sim:
          ∀ id,
            sim (crel RData RData) (id ↦ gensem ticket_lock_init0_spec)
                (id ↦ gensem ticket_lock_init0_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 same_len_implies_sub_lst_len_same:
          ∀ {A : Type} (l11 l12 l21 l22 : list A),
            length (l11 ++ l12) = length (l21++l22) →
            length l11 = length l21 →
            length l12 = length l22.
        Proof.
          induction l11 as [ | e1]; intros; simpl.
          - destruct l21; simpl; try (inv H0; fail).
            simpl in H; assumption.
          - destruct l21; simpl in *; try (inv H0; fail).
            inv H0; inv H.
            eapply IHl11; eauto.
        Qed.

        Lemma not_nil_has_pre_and_post_lst:
          ∀ {A : Type} (l : list A),
            l ≠ nil →
            ∃ ev (l_hd l_tl : list A),
              l = l_hd++ev::l_tl.
        Proof.
          clear real_params real_params_ops.
          clear Hmwd Hmem memory_model_ops.
          clear mem Hstencil stencil_ops stencil mcs_oracle_prop.
          clear big_ops mcs_oracle_ops.           clear oracle_ops1.
          intros; induction l as [ | ev]; intros.
          - elim H; auto.
          - destruct l; try (∃ ev, nil, nil; eauto; fail).
            assert (a::l ≠ nil).
            { unfold not; intros; inv H0. }
            eapply IHl in H0.
            destruct H0 as (ev0 & l_hd0 & l_tl0 & H0).
            eexists ev0, (ev::l_hd0), l_tl0; eauto; simpl.
            f_equal; auto.
        Qed.

        Lemma QS_CalWaitGet_last_event_is_GET_BUSY_false:
          ∀ bounds i ll to ll´,
            QS_CalWaitGet bounds i ll to = Some ll´ →
            ∃ ll_tl,
              ll´ = (TEVENT i (TTICKET (GET_BUSY false)))::ll_tl.
        Proof.
          Transparent QS_CalWaitGet.
          induction bounds; intros; simpl.
          - simpl in H; inv H.
          - simpl in H; subdestruct.
            + inv H; eauto.
            + eapply IHbounds; eauto.
        Qed.

        Lemma QS_CalWaitGet_prev_has_qs:
          ∀ bounds i ll to ll´ ll_tl,
            QS_CalWaitGet bounds i ll to = Some ll´ →
            ll´ = (TEVENT i (TTICKET (GET_BUSY false)))::ll_tl →
            ∃ self_c rel_c b q slow tq q´,
              QS_CalLock ll_tl = Some (self_c, rel_c, b, q, slow, tq) ∧ q = i::q´.
        Proof.
          Transparent QS_CalWaitGet.
          induction bounds; intros; simpl.
          - simpl in H; inv H.
          - simpl in H.
            subdestruct; subst.
            × inv H.
              destruct p3.
              ∃ n, n0, h, (i::l1), t, l, l1; eauto.
            × eapply IHbounds; eauto.
        Qed.

        Lemma valid_log_keeps_loc_info:
          ∀ ll self_c rel_c b q_hd curid q_tl slow tq_hd bound tq_tl id ev self_c´ rel_c´ b´ q´ slow´ tq´,
            QS_CalLock ll = Some (self_c, rel_c, b, q_hd ++ curid::q_tl, slow, tq_hd ++ bound::tq_tl) →
            ¬ In curid q_hd →
            length q_hd = length tq_hd →
            ZSet.mem curid slow = false →
            curid ≠ id →
            QS_CalLock ((TEVENT id ev)::ll) = Some (self_c´, rel_c´, b´, q´, slow´, tq´) →
            ∃ q´_hd q´_tl tq´_hd tq´_tl,
              q´ = q´_hd++curid::q´_tl ∧ tq´ = tq´_hd++bound::tq´_tl ∧
              ZSet.mem curid slow´ = false ∧
              ¬ In curid q´_hd ∧
              length q´_hd = length tq´_hd.
        Proof.
          clear real_params real_params_ops.
          clear Hmwd Hmem memory_model_ops.
          clear mem Hstencil stencil_ops stencil mcs_oracle_prop.
          clear big_ops mcs_oracle_ops.           clear oracle_ops1.
          intros.
          Transparent QS_CalLock.
          simpl in ×.
          rewrite H in H4.
          remember (q_hd ++ curid::q_tl) as q_prev.
          remember (tq_hd ++ bound::tq_tl) as tq_prev.
          destruct q_prev; destruct tq_prev; try (inv H4; fail).
          - destruct q_hd; simpl in Heqq_prev; inv Heqq_prev.
          - case_eq (zeq id z); intros; subst; [ rewrite zeq_true in H4; try omega | rewrite zeq_false in H4; try omega].
            + destruct b; simpl in ×.
              × destruct ev; try (inv H4; fail).
                destruct e; try (inv H4; fail).
                { remember (ZSet.mem z slow) as b.
                  destruct b; inv H4.
                  destruct q_hd; destruct tq_hd.
                  - simpl in Heqq_prev; inv Heqq_prev.
                    elim H3; auto.
                  - simpl in Heqq_prev; inv Heqq_prev.
                    elim H3; auto.
                  - simpl in Heqq_prev.
                    simpl in Heqtq_prev.
                    simpl in H1; inv H1.
                  - ∃ (z0::q_hd), q_tl, (n0::tq_hd), tq_tl.
                    simpl in Heqq_prev; simpl in Heqtq_prev; inv Heqq_prev; inv Heqtq_prev.
                    split; [simpl; tauto | ].
                    split; [simpl; tauto | ].
                    split; eauto using ZSet_remove_preserves_not_in. }
                { destruct busy; inv H4.
                  destruct q_hd; destruct tq_hd.
                  - simpl in Heqq_prev; inv Heqq_prev.
                    elim H3; auto.
                  - simpl in Heqq_prev; inv Heqq_prev.
                    elim H3; auto.
                  - simpl in Heqq_prev.
                    simpl in H1; inv H1.
                  - ∃ (z0::q_hd), q_tl, (n0::tq_hd), tq_tl.
                    simpl in Heqq_prev; simpl in Heqtq_prev; inv Heqq_prev; inv Heqtq_prev.
                    split; [simpl; tauto | ].
                    split; [simpl; tauto | eauto]. }
              × destruct ev; simpl in *; try (inv H4; fail).
                destruct e; simpl in *; try (inv H4; fail).
                remember (ZSet.mem z slow) as b.
                destruct b; inv H4.
                destruct q_hd; destruct tq_hd.
                { simpl in Heqq_prev; inv Heqq_prev.
                  elim H3; auto. }
                { simpl in Heqq_prev; inv Heqq_prev.
                  elim H3; auto. }
                { simpl in Heqq_prev.
                  simpl in Heqtq_prev.
                  simpl in H1; inv H1. }
                { ∃ (z0::q_hd), q_tl, (n0::tq_hd), tq_tl.
                  simpl in Heqq_prev; simpl in Heqtq_prev; inv Heqq_prev; inv Heqtq_prev.
                  split; [simpl; tauto | ].
                  split; [simpl; tauto | ].
                  split; eauto using ZSet_remove_preserves_not_in. }
              × destruct ev; simpl in H4; try (inv H4; fail).
                { destruct e; simpl in H4; try (inv H4; fail).
                  - destruct success.
                    + destruct q_prev; inv H4.
                      destruct q_hd; simpl in Heqq_prev; inv Heqq_prev; [elim H3; auto | ].
                      destruct q_hd; simpl in H7; inv H7.
                    + destruct rel_c; try inv H4.
                      destruct q_hd; destruct tq_hd.
                      { simpl in Heqq_prev; inv Heqq_prev.
                        elim H3; auto. }
                      { simpl in Heqq_prev; inv Heqq_prev.
                        elim H3; auto. }
                      { simpl in Heqq_prev.
                        simpl in Heqtq_prev.
                        simpl in H1; inv H1. }
                      { ∃ (z0::q_hd), q_tl, (n0::tq_hd), tq_tl.
                        simpl in Heqq_prev; simpl in Heqtq_prev; inv Heqq_prev; inv Heqtq_prev.
                        split; [simpl; tauto | ].
                        split; [simpl; tauto | ].
                        split; auto. }
                  - destruct rel_c; try inv H4.
                    destruct q_hd; destruct tq_hd.
                    { simpl in Heqq_prev; inv Heqq_prev.
                      elim H3; auto. }
                    { simpl in Heqq_prev; inv Heqq_prev.
                      elim H3; auto. }
                    { simpl in Heqq_prev.
                      simpl in Heqtq_prev.
                      simpl in H1; inv H1. }
                    { ∃ (z0::q_hd), q_tl, (n0::tq_hd), tq_tl.
                      simpl in Heqq_prev; simpl in Heqtq_prev; inv Heqq_prev; inv Heqtq_prev.
                      split; [simpl; tauto | ].
                      split; [simpl; tauto | ].
                      split; auto. }
                  - remember (ZSet.mem z slow) as b.
                    destruct b; inv H4.
                    destruct q_hd; destruct tq_hd.
                    { simpl in Heqq_prev; inv Heqq_prev.
                      elim H3; auto. }
                    { simpl in Heqq_prev; inv Heqq_prev.
                      elim H3; auto. }
                    { simpl in Heqq_prev.
                      simpl in Heqtq_prev.
                      simpl in H1; inv H1. }
                    { ∃ (z0::q_hd), q_tl, (n0::tq_hd), tq_tl.
                      simpl in Heqq_prev; simpl in Heqtq_prev; inv Heqq_prev; inv Heqtq_prev.
                      split; [simpl; tauto | ].
                      split; [simpl; tauto | ].
                      split; eauto using ZSet_remove_preserves_not_in. }
                  - destruct rel_c; try inv H4.
                    remember (negb (ZSet.mem z slow)) as b.
                    destruct b; inv H7.
                    destruct q_hd; destruct tq_hd.
                    { simpl in Heqq_prev; inv Heqq_prev.
                      elim H3; auto. }
                    { simpl in Heqq_prev; inv Heqq_prev.
                      elim H3; auto. }
                    { simpl in Heqq_prev.
                      simpl in Heqtq_prev.
                      simpl in H1; inv H1. }
                    { ∃ q_hd, q_tl, tq_hd, tq_tl.
                      simpl in Heqq_prev; simpl in Heqtq_prev; inv Heqq_prev; inv Heqtq_prev.
                      split; [simpl; tauto | ].
                      split; [simpl; tauto | ].
                      split; auto.
                      simpl in H1; inv H1.
                      split; auto.
                      unfold not; intros contras; elim H0; simpl; tauto. } }
                { destruct self_c; inv H4.
                  destruct q_hd; destruct tq_hd.
                  { simpl in Heqq_prev; inv Heqq_prev.
                    elim H3; auto. }
                  { simpl in Heqq_prev; inv Heqq_prev.
                    elim H3; auto. }
                  { simpl in Heqq_prev.
                    simpl in Heqtq_prev.
                    simpl in H1; inv H1. }
                  { ∃ (z0::q_hd), q_tl, (n0::tq_hd), tq_tl.
                    simpl in Heqq_prev; simpl in Heqtq_prev; inv Heqq_prev; inv Heqtq_prev.
                    split; [simpl; tauto | ].
                    split; [simpl; tauto | ].
                    split; auto. } }
            + destruct ev; simpl in *; try (inv H4; fail).
              destruct e; simpl in *; try (inv H4; fail).
              × destruct is_null; try (inv H4; fail).
                remember (zeq z id) as z_id.
                destruct (zeq z id); try inv H4; [elim n0; auto | ].
                remember (in_dec zeq id q_prev) as in_dec_prop.
                destruct in_dec_prop; inv H7.
                destruct q_hd; destruct tq_hd.
                { simpl in Heqq_prev; inv Heqq_prev.
                  simpl in Heqtq_prev; inv Heqtq_prev.
                  ∃ nil, (q_tl++id::nil), nil, (tq_tl++n1::nil).
                  split; auto; split; auto; split; auto.
                  rewrite ZSet_gso; eauto. }
                { simpl in Heqq_prev; inv Heqq_prev.
                  simpl in H1; inv H1. }
                { simpl in Heqq_prev.
                  simpl in Heqtq_prev.
                  simpl in H1; inv H1. }
                { simpl in ×.
                  inv Heqq_prev; inv Heqtq_prev.
                  ∃ (z0::q_hd), (q_tl++id::nil), (n4::tq_hd), (tq_tl++n1::nil).
                  split; simpl; [rewrite app_assoc_reverse; simpl; auto | ].
                  split; simpl; [rewrite app_assoc_reverse; simpl; auto | ].
                  split; auto.
                  rewrite ZSet_gso; eauto. }
              × remember (ZSet.mem id slow) as b´´.
                destruct b´´; inv H4.
                destruct q_hd; destruct tq_hd.
                { simpl in Heqq_prev; inv Heqq_prev.
                  simpl in Heqtq_prev; inv Heqtq_prev.
                  ∃ nil, q_tl, nil, tq_tl.
                  split; auto; split; auto; split; auto.
                  eauto using ZSet_remove_preserves_not_in. }
                { simpl in Heqq_prev; inv Heqq_prev.
                  simpl in H1; inv H1. }
                { simpl in Heqq_prev.
                  simpl in Heqtq_prev.
                  simpl in H1; inv H1. }
                { simpl in ×.
                  inv Heqq_prev; inv Heqtq_prev.
                  ∃ (z0::q_hd), q_tl, (n1::tq_hd), tq_tl.
                  split; simpl; auto.
                  split; simpl; auto.
                  split; auto.
                  eauto using ZSet_remove_preserves_not_in. }
              × destruct busy; try inv H4.
                remember (ZSet.mem id slow) as b´´.
                destruct b´´; try inv H7.
                destruct q_hd; destruct tq_hd.
                { simpl in Heqq_prev; inv Heqq_prev.
                  simpl in Heqtq_prev; inv Heqtq_prev.
                  ∃ nil, q_tl, nil, tq_tl.
                  split; auto; split; auto; split; auto. }
                { simpl in Heqq_prev; inv Heqq_prev.
                  simpl in H1; inv H1. }
                { simpl in Heqq_prev.
                  simpl in Heqtq_prev.
                  simpl in H1; inv H1. }
                { simpl in ×.
                  inv Heqq_prev; inv Heqtq_prev.
                  ∃ (z0::q_hd), q_tl, (n1::tq_hd), tq_tl.
                  split; simpl; auto. }
                Opaque QS_CalLock.
        Qed.

        Lemma valid_log_keeps_loc_info´:
          ∀ ll´ ll self_c rel_c b q_hd curid q_tl slow tq_hd bound tq_tl self_c´ rel_c´ b´ q´ slow´ tq´,
            QS_CalLock ll = Some (self_c, rel_c, b, q_hd ++ curid::q_tl, slow, tq_hd ++ bound::tq_tl) →
            ¬ In curid q_hd →
            length q_hd = length tq_hd →
            ZSet.mem curid slow = false →
            (∀ i0 e, In (TEVENT i0 e) ll´ → i0 ≠ curid) →
            QS_CalLock (ll´ ++ ll) = Some (self_c´, rel_c´, b´, q´, slow´, tq´) →
            ∃ q´_hd q´_tl tq´_hd tq´_tl,
              q´ = q´_hd++curid::q´_tl ∧ tq´ = tq´_hd++bound::tq´_tl ∧
              ZSet.mem curid slow´ = false ∧
              ¬ In curid q´_hd ∧
              length q´_hd = length tq´_hd.
        Proof.
          clear real_params real_params_ops.
          clear Hmwd Hmem memory_model_ops.
          clear mem Hstencil stencil_ops stencil mcs_oracle_prop.
          clear big_ops mcs_oracle_ops.           clear oracle_ops1.
          induction ll´ as [ | ev´]; simpl; intros; auto.
          - rewrite H in H4; inv H4; repeat (eexists; auto).
          - assert (new_event: ∃ i0 e, ev´ = TEVENT i0 e).
            { Transparent QS_CalLock.
              simpl in H4.
              remember ev´ as ev´´.
              destruct ev´.
              ∃ i, e; eauto.
              Opaque QS_CalLock. }
            destruct new_event as (id_n´ & ev_n´ & new_event); subst.
            assert (not_in_prop: ∀ i0 e, In (TEVENT i0 e) ll´ → i0 ≠ curid).
            { intros; eapply H3; eauto. }
            assert (not_eq_prop: curid ≠ id_n´).
            { assert (id_n´ ≠ curid) by (eapply H3; left; eauto).
              auto. }
            destruct QS_CalLock_pre_exist with (1:= H4) as (mcs´, H_Cal_ll_ll´).
            destruct mcs´ as (((((self_c_tmp & rel_c_tmp) & b_tmp) & q_tmp) & slow_tmp) & tq_tmp).
            destruct (IHll´ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H H0 H1 H2 not_in_prop H_Cal_ll_ll´) as
                (q_tmp_hd & q_tmp_tl & tq_tmp_hd & tq_tmp_tl & H_Cal_ll_ll´_prop1
                          & H_Cal_ll_ll´_prop2 & H_Cal_ll_ll´_prop3 & H_Cal_ll_ll´_prop4 & H_Cal_ll_ll´_prop5).
            subst.
            eapply valid_log_keeps_loc_info; eauto.
        Qed.

        Lemma valid_log_and_GET_BUSY_keeps_loc_info:
          ∀ ll self_c rel_c b q_hd curid q_tl slow tq_hd bound tq_tl self_c´ rel_c´ b´ q´ slow´ tq´,
            QS_CalLock ll = Some (self_c, rel_c, b, q_hd ++ curid::q_tl, slow, tq_hd ++ bound::tq_tl) →
            ¬ In curid q_hd →
            length q_hd = length tq_hd →
            ZSet.mem curid slow = false →
            QS_CalLock ((TEVENT curid (TTICKET (GET_BUSY true)))::ll) = Some (self_c´, rel_c´, b´, q´, slow´, tq´) →
            ∃ q´_hd q´_tl tq´_hd tq´_tl,
              q´ = q´_hd++curid::q´_tl ∧ tq´ = tq´_hd++bound::tq´_tl ∧
              ZSet.mem curid slow´ = false ∧
              ¬ In curid q´_hd ∧
              length q´_hd = length tq´_hd.
        Proof.
          clear real_params real_params_ops.
          clear Hmwd Hmem memory_model_ops.
          clear mem Hstencil stencil_ops stencil mcs_oracle_prop.
          clear big_ops mcs_oracle_ops.           clear oracle_ops1.
          intros.
          Transparent QS_CalLock.
          simpl in H3.
          rewrite H in H3.
          remember (q_hd ++ curid::q_tl) as q_prev.
          remember (tq_hd ++ bound::tq_tl) as tq_prev.
          destruct q_prev.
          - destruct tq_prev; inv H3.
          - destruct tq_prev; try (inv H3; fail).
            remember (zeq curid z) as s.
            destruct s; [destruct b; inv H3 | ].
            remember (ZSet.mem curid slow) as b´´.
            destruct b´´; inv H3.
            destruct q_hd; destruct tq_hd.
            { simpl in Heqq_prev; inv Heqq_prev.
              simpl in Heqtq_prev; inv Heqtq_prev.
              ∃ nil, q_tl, nil, tq_tl; eauto. }
            { simpl in Heqq_prev; inv Heqq_prev.
              simpl in H1; inv H1. }
            { simpl in Heqq_prev.
              simpl in Heqtq_prev.
              simpl in H1; inv H1. }
            { ∃ (z::q_hd), q_tl, (n::tq_hd), tq_tl.
              simpl in Heqq_prev; simpl in Heqtq_prev; inv Heqq_prev; inv Heqtq_prev.
              split; [simpl; tauto | ].
              split; [simpl; tauto | ].
              split; eauto. }
        Qed.

        Lemma QS_CalWaitGet_prev_has_mcs:
          ∀ bounds i ll to ll´,
            QS_CalWaitGet bounds i ll to = Some ll´ →
            ∃ mcs, QS_CalLock ll = Some mcs.
        Proof.
          clear real_params real_params_ops.
          clear Hmwd Hmem memory_model_ops.
          clear mem Hstencil stencil_ops stencil mcs_oracle_prop.
          clear big_ops mcs_oracle_ops.           clear oracle_ops1.
          destruct bounds; intros.
          - Transparent QS_CalWaitGet.
            simpl in H; inv H.
          - simpl in H.
            subdestruct.
            + subst.
              inv H.
              eapply QS_CalLock_app_exist; eauto.
            + subst.
              eapply QS_CalLock_app_exist; eauto.
              Opaque QS_CalWaitGet.
        Qed.

        Lemma valid_log_and_QS_CalWaitGet_keeps_loc_info:
          ∀ bounds to ll ll´ ll´_tl self_c rel_c b q_hd curid q_tl slow tq_hd bound tq_tl self_c´ rel_c´ b´ q´ slow´ tq´,
            QS_CalLock ll = Some (self_c, rel_c, b, q_hd ++ curid::q_tl, slow, tq_hd ++ bound::tq_tl) →
            ¬ In curid q_hd →
            length q_hd = length tq_hd →
            ZSet.mem curid slow = false →
            QS_CalWaitGet bounds curid ll to = Some ll´ →
            ll´ = (TEVENT curid (TTICKET (GET_BUSY false)))::ll´_tl →
            valid_multi_oracle_domain to →
            QS_CalLock ll´_tl = Some (self_c´, rel_c´, b´, q´, slow´, tq´) →
            ∃ q´_hd q´_tl tq´_hd tq´_tl,
              q´ = q´_hd++curid::q´_tl ∧ tq´ = tq´_hd++bound::tq´_tl ∧
              ZSet.mem curid slow´ = false ∧
              ¬ In curid q´_hd ∧
              length q´_hd = length tq´_hd.
        Proof.
          clear real_params real_params_ops.
          clear Hmwd Hmem memory_model_ops.
          clear mem Hstencil stencil_ops stencil mcs_oracle_prop.
          clear big_ops mcs_oracle_ops.           clear oracle_ops1.
          induction bounds; intros; simpl.
          Transparent QS_CalWaitGet.
          - simpl in H3; inv H3.
          - simpl in H3; subdestruct; subst.
            + inv H3.
              unfold valid_multi_oracle_domain in H5.
              assert ( ∀ (i i0 : Z) (e : MultiOracleEventUnit) (l0 : MultiLog),
                         In (TEVENT i0 e) (to i l0) → i0 ≠ i).
              { intros; exploit H5; eauto; tauto. }
              eauto using valid_log_keeps_loc_info´.
            + assert (∃ mcs´, QS_CalLock (TEVENT curid (TTICKET (GET_BUSY true)) :: to curid ll ++ ll) = Some mcs´).
              { eauto using QS_CalWaitGet_prev_has_mcs. }
              destruct H4 as (mcs´ & H4).
              destruct mcs´ as (((((self_c_p´ & rel_c_p´) & b_p´) & q_p´) & slow_p´) & tq_p´).
              destruct p3.
              assert (∀ i0 e, In (TEVENT i0 e) (to curid ll) → i0 ≠ curid).
              { unfold valid_multi_oracle_domain in H5.
                intros; eapply H5; eauto. }
              generalize (valid_log_keeps_loc_info´ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
                                                    H H0 H1 H2 H7 Hdestruct); intros.
              destruct H8 as (q´_hd & q´_tl & tq´_hd & tq´_tl & H8a & H8b & H8c & H8d & H8e); subst.
              rewrite H8a in Hdestruct.
              generalize (valid_log_and_GET_BUSY_keeps_loc_info _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
                                                                Hdestruct H8d H8e H8c H4).
              intros.
              destruct H8 as (q´´_hd & q´´_tl & tq´´_hd & tq´´_tl & H9a & H9b & H9c & H9d & H9e); subst.
              eapply IHbounds; eauto.
        Qed.


        Lemma mcs_wait_lock_exist:
          ∀ habd habd´ labd bound n ofs f
                 (Hhigh: MQMCSLockOp.high_level_invariant labd),
            wait_hlock_spec bound n ofs habd = Some habd´
            → relate_RData f habd labd
            → ∃ labd´, wait_qslock_spec bound n ofs labd = Some labd´ ∧ relate_RData f habd´ labd´.
        Proof.
          Opaque QS_CalWaitRel CalWaitLockTime.

          unfold wait_hlock_spec, wait_qslock_spec; intros until f; intro.
          intros HP HR; pose proof HR as HR´; inv HR; revert HP; simpl.
          subrewrite´.

          destruct (ikern labd); [|intros; congruence].
          destruct (ihost labd); [|intros; congruence].
          destruct (index2Z n ofs) as [abid|] eqn: H_abid; [|intros; congruence].

          inv mcs_log_re0.
          specialize (Hrelate_mcs_log_type _ _ _ H_abid).
          inv mcs_oracle_re0; specialize (Hrelate_mcs_oracle _ _ _ H_abid).

          inversion Hhigh.
          specialize (valid_qs_oracle_pool_inv _ _ _ H_abid).
          destruct valid_qs_oracle_pool_inv as [Hvalid_oracle_domain Hvalid_qs_oracle].

          destruct (ZMap.get abid (multi_log labd)) as [|ll] eqn:H_ll;
            destruct (ZMap.get abid (multi_log habd)) as [|hl] eqn:H_hl;
            inversion Hrelate_mcs_log_type; intros Hpass_hlock; try congruence.
          rename tq into rtq.

          unfold correct_qslock_pool_status in valid_qslock_pool_status_inv.
          specialize (valid_qslock_pool_status_inv _ _ _ _ H_abid H_ll).
          pose (curid := CPU_ID labd).

          inversion Hrelate_mcs_oracle; subst.

          unfold correct_qslock_status in valid_qslock_pool_status_inv.
          destruct (ZMap.get abid (lock labd)); [|congruence].

          pose (ll1 := (ZMap.get abid (multi_oracle labd)) (CPU_ID labd) ll ++ ll).
          fold ll1.

          specialize (valid_qslock_pool_inv _ _ _ _ H_abid H_ll).

          unfold valid_qslock in valid_qslock_pool_inv.
          destruct valid_qslock_pool_inv as [self_c [rel_c [b [q [slow [tq HCal]]]]]].

          destruct (valid_qslock_pool_status_inv self_c rel_c b q tq slow HCal) as [Hvalid_qslock_status _].
          specialize (Hvalid_qslock_status eq_refl).

          assert (Hrtq := QS_CalLock_relate_mcs_log_eq _ _ _ _ _ _ _ rtq tq Hrelate_mcs_log HCal).
          subst rtq.

          unfold valid_qs_oracle in Hvalid_qs_oracle.
          generalize (wait_lock_extend_other_threads _ _ _ _ _ _ _ _ _ _ HCal Hrelate_mcs_log Hvalid_qslock_status
                                                     Hvalid_qs_oracle Hvalid_oracle_domain); intros wait_lock_extend.
          destruct wait_lock_extend as (hl_tmp1 & self_c1 & rel_c1 & b1 & q1 & slow1 & tq1 & HCal_ll1 &
                                        HnotIn1 & Hrelate_tmp1).
          generalize HCal; intro HCal_tmp_ll1.
          eapply Hvalid_qs_oracle with (i := (CPU_ID labd)) in HCal_tmp_ll1.
          destruct HCal_tmp_ll1 as (self_tmp_c1 & rel_tmp_c1 & tmp_b1 & tmp_q1 & tmp_slow1 & tmp_tq1 & HCal_tmp_ll1
                                    & HCal_ll1_bound).
          rewrite HCal_ll1 in HCal_tmp_ll1; symmetry in HCal_tmp_ll1; inv HCal_tmp_ll1.
          fold ll1 in HCal_ll1, HCal_ll1_bound.
          rewrite HCal_ll1.

          assert (Hlength_tq1: length tq1 = length q1%nat ).
          { rewrite <- (QS_CalLock_q_length_same _ _ _ _ _ _ _ HCal_ll1).
            simpl; auto. }

          destruct q1 as [|j1 tail]; [ destruct Hrelate_mcs_oracle_res as (Hrelate_mcs_oracle_res, _) |
                                       destruct Hrelate_mcs_oracle_res as (_, Hrelate_mcs_oracle_res)].
          -
            eexists; split; [reflexivity | ].
            subdestruct.
            inv Hpass_hlock.
            pose (hl1 := (ZMap.get abid (multi_oracle habd) (CPU_ID labd) hl ++ hl)).
            fold hl1.
            assert (H_tmp: habd {multi_log
                                   : ZMap.set abid
                                            (MultiDef (TEVENT (CPU_ID labd) (TTICKET (WAIT_LOCK (Z.to_nat bound)))
                                                              :: hl1)) (multi_log habd)}
                                {lock : ZMap.set abid (LockOwn false) (lock labd)} =
                           habd {multi_log
                                 : ZMap.set abid
                                            (MultiDef (TEVENT (CPU_ID labd) (TTICKET (WAIT_LOCK (Z.to_nat bound)))
                                                              :: hl1)) (multi_log habd)}
                                {lock : ZMap.set abid (LockOwn false) (lock habd)}) by (rewrite lock_re0; eauto);
              rewrite H_tmp; clear H_tmp.
            assert (tq1 = nil).
            { eapply QS_CalLock_q_tq_length_same_nil in HCal_ll1; destruct HCal_ll1.
              eapply H0; trivial. }
            subst.
            assert (∃ self_c2 rel_c2 slow2,
                      QS_CalLock (TEVENT (CPU_ID labd) (TTICKET (SWAP_TAIL (nat_of_Z bound) true)) :: ll1) =
                      Some (self_c2, rel_c2, LHOLD, CPU_ID labd :: nil, slow2, nat_of_Z bound::nil)) as HCal_res.
            { Transparent QS_CalLock.
              simpl.
              rewrite HCal_ll1.
              repeat eexists; auto. }
            destruct HCal_res as (self_c2 & rel_c2 & slow2 & HCal_res).
            destruct Hrelate_mcs_oracle_res with (1:= Hrelate_mcs_log) (2:= HCal_res)
              as (tq´, Hrelate_res).
            assert (tq´ = nil).
            { unfold ll1 in HCal_ll1.
              eapply QS_CalLock_relate_mcs_log_eq in HCal_ll1; eauto. }
            subst.
            assert (Hrelate_mcs_log_res: relate_mcs_log
                                           (TEVENT (CPU_ID labd)
                                                   (TTICKET (SWAP_TAIL (nat_of_Z bound) true)) :: ll1) =
                                         Some ((TEVENT (CPU_ID labd)
                                                       (TTICKET (WAIT_LOCK (nat_of_Z bound))) :: hl1),
                                               nat_of_Z bound :: nil)).
            { simpl; unfold ll1; unfold hl1.
              rewrite Hrelate_res.
              reflexivity. }
            eapply update_abd_log; eauto.

          -
            subdestruct; inv Hpass_hlock.
            clear curid.
            pose (ll2 := TEVENT (CPU_ID labd) (TTICKET (SWAP_TAIL (nat_of_Z bound) false)) :: ll1).
            pose (slow2 := ZSet.add (CPU_ID labd) slow1).
            fold ll2.

            assert (HCal_ll2: QS_CalLock ll2
                              = Some (self_c1, rel_c1, b1, (j1 :: tail) ++ (CPU_ID labd)::nil ,
                                      slow2, tq1 ++ (nat_of_Z bound) :: nil)).
            { unfold ll2, slow2; simpl.
              rewrite HCal_ll1.
              assert (length tq1 ≠ 0%nat ) as Hlength_tq1´.
              { rewrite <- (QS_CalLock_q_length_same _ _ _ _ _ _ _ HCal_ll1).
                simpl; auto. }
              destruct tq1 as [|tq1_head tq1_tail]; [simpl in Hlength_tq1´; congruence|].
              destruct (zeq (CPU_ID labd) j1); [subst; contradict HnotIn1; simpl; auto|].
              destruct (in_dec zeq (CPU_ID labd) (j1 :: tail)); [tauto | ].
              reflexivity. }
          
            assert (Hslow2 : ZSet.mem (CPU_ID labd) slow2 = true)
              by (unfold slow2; apply ZSet_gss).

            assert (Hrelate_tmp2: relate_mcs_log ll2 = Some (hl_tmp1, tq1 ++ (nat_of_Z bound) :: nil)).
            { simpl; unfold ll1; rewrite Hrelate_tmp1; reflexivity. }

            pose (ll3 := (ZMap.get abid (multi_oracle labd)) (CPU_ID labd) ll2 ++ ll2).
            fold ll3.

            unfold valid_qs_oracle in Hvalid_qs_oracle.
            destruct (Hvalid_qs_oracle (CPU_ID labd) _ _ _ _ _ _ _ HCal_ll2)
              as [self_c3 [rel_c3 [b3 [q3 [slow3 [tq3 [HCal_ll3 Hfairness3]]]]]]].
            fold ll3 in HCal_ll3, Hfairness3.

            destruct (QS_CalLock_relate_mcs_log_exists _ _ _ _ _ _ _ HCal_ll3) as [hl_tmp3 Hrelate_tmp3].

            destruct (MCS_CalLock_progress _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ HCal_ll2 HCal_ll3 Hlength_tq1)
              as [q´_3 [q´´_3 [q1_3 [tq´_3 [tq´´_3 [tq1_3 [H_q3 [H_tq3 [? [H_tq1 [Hlen3 Hdecrease3]]]]]]]]]]];
              [ intros i0 e; apply Hvalid_oracle_domain | exact Hfairness3 | assumption | ].

            assert (Hslow3 : ZSet.mem (CPU_ID labd) slow3 = true).
            { assert (∀ i0 e, In (TEVENT i0 e) ((ZMap.get abid (multi_oracle labd)) (CPU_ID labd) ll2) →
                                   i0 ≠ (CPU_ID labd)) as Hdomain.
              { intros.
                unfold valid_multi_oracle_domain in Hvalid_oracle_domain.
                apply (Hvalid_oracle_domain _ _ e ll2); auto. }
              rewrite (QS_CalLock_oracle_Mem ((ZMap.get abid (multi_oracle labd)) (CPU_ID labd) ll2)
                                             _ _ _ _ _ _ _ _ _ _ _ _ _ _ HCal_ll2 Hdomain HCal_ll3).
              exact Hslow2. }
            
            pose (ll4 := (TEVENT (CPU_ID labd)
                                  (TTICKET
                                     (SET_NEXT
                                        match tail with
                                        | nil ⇒ j1
                                        | _ :: _ ⇒ last tail NULL
                                        end)) :: ll3)).
            pose (slow4 := ZSet.remove (CPU_ID labd) slow3).
            fold ll4.

            assert (HCal_ll4 : QS_CalLock ll4 = Some (self_c3, rel_c3, b3, q3, slow4, tq3)).
            { unfold ll4; simpl.
              rewrite HCal_ll3.
              assert (q3≠nil) by (rewrite H_q3; destruct q´´_3; simpl; congruence).
              assert (tq3 ≠ nil).
              { eapply QS_CalLock_q_tq_length_same_not_nil in HCal_ll3;
                destruct HCal_ll3 as (_ & HCal_ll3); apply HCal_ll3; auto. }
              destruct q3 as [|i0 q3]; [congruence|].
              destruct tq3 as [|? ?]; [congruence|].
              destruct (zeq (CPU_ID labd) i0).
              + rewrite Hslow3.
                destruct b3;
                reflexivity.
              + rewrite Hslow3.
                reflexivity. }
            
            rewrite H_q3, H_tq3 in HCal_ll4.
            destruct (CalWaitGet_exist´ (CalWaitLockTime tq1) _ _ _ _ _ _ _ _ _ (ZMap.get abid (multi_oracle labd)) _ _ HCal_ll4)
              as [l´ HCal´].
            { congruence. }
            { apply le_lt_trans with (decrease_number self_c3 rel_c3 b3 (CPU_ID labd) q´´_3 slow3 tq´´_3 ll3 + WaitConstant)%nat;
              [apply decrease_number_remove_slow | ].
              fold ll3 in Hdecrease3.
              apply le_lt_trans with (decrease_number self_c1 rel_c1 b1 (CPU_ID labd) (j1 :: tail) slow2 tq1 ll2 +
                                      WaitConstant)%nat; [ apply plus_le_compat_r; apply Hdecrease3 | ].
              assert (Htq1_nonnil : tq1 ≠ nil)
                by (destruct tq1; simpl in Hlength_tq1; congruence).
              apply (decrease_number_upper_bound _ _ _ (CPU_ID labd) _ slow2 _ (CPU_ID labd :: nil) slow2
                                                 (nat_of_Z bound :: nil) _ HCal_ll2 Htq1_nonnil).
              congruence. }
            { split; auto. }
            { assert (HnotIn´: ¬In (CPU_ID labd) (q´_3 ++ q´´_3))
                by (replace (q´_3 ++ q´´_3) with (j1::tail) by congruence; assumption).
              rewrite in_app in HnotIn´.
              tauto. }
            { unfold slow4; eapply ZSet_mem_remove. }
            rewrite HCal´.
            eexists; split; [reflexivity | ].

            destruct QS_CalWaitGet_last_event_is_GET_BUSY_false with (1:= HCal´) as
                (ll_tl´, res_l).
            assert (Hrelate_res_prev: ∃ tq´ : list nat,
                       relate_mcs_log ll_tl´ = Some (ZMap.get abid (multi_oracle habd) (CPU_ID labd) hl ++ hl,
                                                     tq´)).
            { unfold ll4 in HCal´.
              unfold ll3 in HCal´.
              unfold ll2 in HCal´.
              unfold ll1 in HCal´.
              unfold ll2 in HCal_ll2.
              unfold ll1 in HCal_ll2.
              unfold ll4 in HCal_ll4.
              unfold ll3 in HCal_ll4.
              unfold ll2 in HCal_ll4.
              unfold ll1 in HCal_ll4.
              set (prev_id :=
                     match tail with
                       | nil ⇒ j1
                       | _ :: _ ⇒ last tail NULL
                     end).
              fold prev_id in HCal´.
              destruct Hrelate_mcs_oracle_res with (1:= Hrelate_mcs_log) (2:= HCal_ll2) (3:= HCal_ll4) (4 := HCal´) (5:= res_l)
                as (tq´, H_tmp).
              ∃ tq´; auto. }
            subst.
            destruct Hrelate_res_prev as (tq_res_prev´, Hrelate_res_prev).

            remember (TEVENT (CPU_ID labd) (TTICKET (GET_BUSY false)) :: ll_tl´) as ll_tl_prop.
            assert (pre_not_in: ¬ In (CPU_ID labd) q´´_3).
            { rewrite H in HnotIn1.
              intro contra.
              elim HnotIn1.
              eapply in_or_app.
              right; auto. }
            symmetry in Hlen3.
            assert (pre_slow_false: ZSet.mem (CPU_ID labd) slow4 = false).
            { unfold slow4.
              eauto using ZSet_mem_remove. }

            generalize (QS_CalWaitGet_prev_has_qs _ _ _ _ _ _ HCal´ Heqll_tl_prop); intros HCal_ll_tl´.
            destruct HCal_ll_tl´ as (self_c_ll_tl´ & rel_c_ll_tl´ & b_ll_tl´ & q_ll_tl´´ & slow_ll_tl´ & tq_ll_tl´ & q_ll_tl´ & HCal_ll_tl´
                                                   & H_tmp).
            rewrite H_tmp in HCal_ll_tl´.
            clear H_tmp q_ll_tl´´.

            generalize (valid_log_and_QS_CalWaitGet_keeps_loc_info _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
                                                                   HCal_ll4 pre_not_in Hlen3 pre_slow_false HCal´ Heqll_tl_prop
                                                                   Hvalid_oracle_domain HCal_ll_tl´); intros post_cond.
            destruct post_cond as (q_ll_tl´_hd & q_ll_tl´´_tl & tq_ll_tl´_hd & tq_ll_tl´_tl & post_cond1 & post_cond2
                                                & post_cond3 & post_cond4 & post_cond5).
            assert (q_ll_tl´_hd = nil).
            { destruct q_ll_tl´_hd; [ reflexivity | ].
              inv post_cond1.
              elim post_cond4; simpl; tauto. }
            assert (tq_ll_tl´_hd = nil).
            { destruct tq_ll_tl´_hd; [ reflexivity | ].
              subst.
              simpl in post_cond5; inv post_cond5. }
            subst; simpl in HCal_ll_tl´.
            assert (nat_of_Z bound::tq_ll_tl´_tl = tq_res_prev´).
            { symmetry; eauto using QS_CalLock_relate_mcs_log_eq. }
            subst.
            assert (Hrelate_res:
                      relate_mcs_log (TEVENT (CPU_ID labd) (TTICKET (GET_BUSY false)) :: ll_tl´) =
                      Some ((TEVENT (CPU_ID labd) (TTICKET (WAIT_LOCK (Z.to_nat bound)))
                                    :: ZMap.get abid (multi_oracle habd) (CPU_ID labd) hl ++ hl), nat_of_Z bound::tq_ll_tl´_tl)).
            { simpl; rewrite Hrelate_res_prev; reflexivity. }

            pose (hl1 := ZMap.get abid (multi_oracle habd) (CPU_ID labd) hl ++ hl).
            fold hl1.
            fold hl1 in Hrelate_res.
            assert (H_tmp: habd {multi_log
                                   : ZMap.set abid
                                            (MultiDef (TEVENT (CPU_ID labd) (TTICKET (WAIT_LOCK (Z.to_nat bound)))
                                                              :: hl1)) (multi_log habd)}
                                {lock : ZMap.set abid (LockOwn false) (lock labd)} =
                           habd {multi_log
                                 : ZMap.set abid
                                            (MultiDef (TEVENT (CPU_ID labd) (TTICKET (WAIT_LOCK (Z.to_nat bound)))
                                                              :: hl1)) (multi_log habd)}
                                {lock : ZMap.set abid (LockOwn false) (lock habd)}) by (rewrite lock_re0; eauto);
              rewrite H_tmp; clear H_tmp.
            eapply update_abd_log; eauto.
        Qed.

        Lemma mcs_wait_lock_sim:
          ∀ id,
            sim (crel RData RData) (id ↦ gensem wait_hlock_spec)
                (id ↦ gensem wait_qslock_spec).
        Proof.
          intros.
          layer_sim_simpl.
          compatsim_simpl (@match_AbData); intros.
          exploit mcs_wait_lock_exist; eauto 1.
          intros [labd´ [HP HM]].
          match_external_states_simpl.
        Qed.

        Lemma mcs_pass_lock_exist:
          ∀ habd habd´ labd id ofs f
                 (Hhigh: MQMCSLockOp.high_level_invariant labd),
            pass_hlock_spec id ofs habd = Some habd´
            → relate_RData f habd labd
            → ∃ labd´, pass_qslock_spec id ofs labd = Some labd´ ∧ relate_RData f habd´ labd´.
        Proof.
          unfold pass_hlock_spec, pass_qslock_spec; intros until f. intro.
          intros HP HR; pose proof HR as HR´; inv HR; revert HP; simpl.
          subrewrite´.

          destruct (ikern labd); [|intros; congruence].
          destruct (ihost labd); [|intros; congruence].
          destruct (index2Z id ofs) as [abid|] eqn: H_abid; [|intros; congruence].

          inv mcs_log_re0.
          specialize (Hrelate_mcs_log_type _ _ _ H_abid).

          inversion Hhigh.
          specialize (valid_qs_oracle_pool_inv _ _ _ H_abid).
          destruct valid_qs_oracle_pool_inv as [Hvalid_oracle_domain Hvalid_qs_oracle].

          destruct (ZMap.get abid (multi_log labd)) as [|ll] eqn:H_ll;
            destruct (ZMap.get abid (multi_log habd)) as [|hl] eqn:H_hl;
            inversion Hrelate_mcs_log_type; intros Hpass_hlock; try congruence.
          rename tq into rtq.

          remember (ZMap.get abid (multi_oracle habd)) as ho.
          remember (ZMap.get abid (multi_oracle labd)) as lo.
          clear Heqho Heqlo.

          unfold correct_qslock_pool_status in valid_qslock_pool_status_inv.
          specialize (valid_qslock_pool_status_inv _ _ _ _ H_abid H_ll).
          pose (curid := CPU_ID labd).

          unfold correct_qslock_status in valid_qslock_pool_status_inv.
          destruct (ZMap.get abid (lock labd)); [congruence|].

          pose (ll1 := lo (CPU_ID labd) ll ++ ll).
          fold ll1.

          specialize (valid_qslock_pool_inv _ _ _ _ H_abid H_ll).

          unfold valid_qslock in valid_qslock_pool_inv.
          destruct b; [inv Hpass_hlock|].

          destruct valid_qslock_pool_inv as [self_c [rel_c [b [q [slow [tq HCal]]]]]].

          destruct (valid_qslock_pool_status_inv self_c rel_c b q tq slow HCal) as [_ Hvalid_qslock_status].
          assert (eq_refl: LockOwn false = LockOwn false) by reflexivity.
          destruct (Hvalid_qslock_status _ eq_refl) as [q0 [Hq [Hb [HnotIn Hfuel]]]].
          rewrite Hq in ×.
          rewrite Hb in ×.
          idtac.
          assert (Hrtq := QS_CalLock_relate_mcs_log_eq _ _ _ _ _ _ _ rtq tq Hrelate_mcs_log HCal).
          subst rtq.

          destruct (pass_lock_extend_other_threads _ _ _ _ _ _ _ _ _ HCal Hrelate_mcs_log HnotIn
                                                   Hvalid_qs_oracle Hvalid_oracle_domain)
            as [q1 [slow1 [tq1 [HCal1 [HnotIn1 Hrelate1]]]]].

          fold ll1 in HCal1, Hrelate1.
          clearbody ll1.
          subst.
          clear ll tq H_ll H_hl HCal Hrelate_mcs_log_type Hrelate_mcs_log valid_qslock_pool_status_inv.

          assert (habd´ = (habd {multi_log : ZMap.set abid
                                                      (MultiDef (TEVENT (CPU_ID labd) (TTICKET REL_LOCK) :: hl)) (multi_log habd)}
                                {lock : ZMap.set abid LockFalse (lock labd)})) as H_habd´.
          {
            destruct (H_CalLock (TEVENT (CPU_ID labd) (TTICKET REL_LOCK) :: hl)); congruence.
          }

          rewrite HCal1.

          destruct q1 as [| j tail].
          +
            eexists.
            assert (Hfuel´ : (0 < rel_c)%nat).
            { Transparent CalPassLockTime.
              unfold CalPassLockTime, CalPassLockLoopTime in Hfuel.
              omega.
            }
            clear Hfuel. rename Hfuel´ into Hfuel.
            destruct rel_c as [|rel_c´]; [omega|].

            split; [reflexivity|].
            rewrite H_habd´.
            pattern (lock labd) at 1; rewrite <- lock_re0.
            apply update_abd_log with (@nil nat).
            assumption.
            {
              simpl.
              rewrite Hrelate1.
              reflexivity.
            }
          +
            unfold CalPassLockTime.
            assert (Hij : (CPU_ID labd) ≠ j).
            {
              simpl in HnotIn1.
              auto.
            }

            assert (Hfuel´ : (S (S fairness) < rel_c)%nat).
            {
              unfold CalPassLockTime, CalPassLockLoopTime in Hfuel.
              omega.
            }
            clear Hfuel. rename Hfuel´ into Hfuel.

            pose (ll2 := (TEVENT (CPU_ID labd) (TTICKET (CAS_TAIL false)) :: ll1)).
            fold ll2.

            assert (Hrelate2 : relate_mcs_log ll2 = Some (hl, tq1)).
            {
              unfold ll2.
              simpl.
              rewrite Hrelate1.
              reflexivity.
            }

            destruct rel_c as [|rel_c´] ; [omega|].
            assert (HCal2: QS_CalLock ll2 = Some (self_c, rel_c´, LHOLD, CPU_ID labd :: j :: tail, slow1, tq1)).
            {
              unfold ll2.
              Transparent QS_CalLock.
              simpl.
              rewrite HCal1.
              assert (Hlen_tq1 : (length tq1 ≠ 0)%nat). {
                rewrite <- (QS_CalLock_q_length_same _ _ _ _ _ _ _ HCal1).
                simpl.
                congruence.
              }
              destruct tq1 as [|? ?] ; [ simpl in Hlen_tq1; congruence | ].
              rewrite zeq_true.
              reflexivity.
            }

            assert (Hfuel´ : (S fairness < rel_c´)%nat)
              by omega.

            destruct (CalWaitRel_exist _ _ _ _ _ _ _ _ _ _ _ Hvalid_qs_oracle Hvalid_oracle_domain Hij HCal2 Hrelate2 Hfuel´)
              as [ll3 [rtq3 [HCalWait3 [HCal3 Hrelate3]]]].

            unfold CalPassLockLoopTime.
            rewrite HCalWait3.
            change (lo (CPU_ID labd) (TEVENT (CPU_ID labd) (TTICKET GET_NEXT) :: ll3) ++
                       TEVENT (CPU_ID labd) (TTICKET GET_NEXT) :: ll3)
            with (pass_lock_final1 ll3 (CPU_ID labd) lo).
            destruct HCal3 as [[? ?] [? [? [? [? [? HCal3]]]]]].
            rewrite HCal3.

            destruct (H_CalLock (TEVENT (CPU_ID labd) (TTICKET REL_LOCK) :: hl)); try congruence.
            eexists; split; [reflexivity|].
            replace habd´
            with (habd {multi_log : ZMap.set abid (MultiDef (TEVENT (CPU_ID labd) (TTICKET REL_LOCK) :: hl))
                                             (multi_log habd)}
                       {lock : ZMap.set abid LockFalse (lock labd)} )
              by congruence.

            pattern (lock labd) at 1; rewrite <- lock_re0.
            apply update_abd_log with rtq3; try assumption.

            Opaque QS_CalLock.
        Qed.

        Lemma mcs_pass_lock_sim:
          ∀ id,
            sim (crel RData RData) (id ↦ gensem pass_hlock_spec)
                (id ↦ gensem pass_qslock_spec).
        Proof.
          intros.
          layer_sim_simpl.
          compatsim_simpl (@match_AbData); intros.
          exploit mcs_pass_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) mhticketlockop mqmcslockop.
        Proof.
          unfold mhticketlockop.
          unfold mhticketlockop_fresh.
          unfold mqmcslockop.
          unfold mqmcslockop_fresh.
          eapply oplus_sim_monotonic; [eapply lower_bound | ].
          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 mcs_pass_lock_sim.
          - apply mcs_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.