Require Import Coqlib.
Require Import Maps.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import Stacklayout.
Require Import Globalenvs.
Require Import AsmX.
Require Import Smallstep.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import FlatMemory.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import RealParams.
Require Import PrimSemantics.
Require Import LAsm.
Require Import LoadStoreSem1.
Require Import XOmega.

Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.

Require Import AbstractDataType.

Require Export ObjCPU.
Require Export ObjMM.
Require Export ObjFlatMem.
Require Export ObjMultiprocessor.
Require Export ObjMCSLock.
Require Export ObjSerialDevice.
Require Export ObjKeyboard.
Require Export ObjInterruptController.
Require Export ObjX86.

Require Import ZSet.

Require Import ListLemma2.
Require Import CalMCSLock.
Require Import INVLemmaQSLock.
Require Import QMCSLockOpGenDef.
Require Import QMCSLockOpGenLemma.

Require Import ObjQLock.

Require Import MultiProcessorSemantics.

Section WITHMEM.

  Local Open Scope Z_scope.

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

  Section cal_qslock_status.

    Definition cal_qslock_status (l: MultiLog) (k: LockStatus) (cpu: Z):=
      ∀ self_c other_c b q slow tq
             (Hcal: QS_CalLock l = Some (self_c, other_c, b, q, slow, tq)),
           (k = LockOwn false → CalValidBit l = Some FreeToPull)
        ∧ (k = LockOwn true → CalValidBit l = Some (PullBy cpu)).

    Definition cal_qslock_pool_status (l: MultiLogPool) (k: Lock) (cpu: Z):=
      ∀ i ofs r q
             (Hrange: index2Z i ofs = Some r)
             (Hdef: ZMap.get r l = MultiDef q),
        cal_qslock_status q (ZMap.get r k) cpu.

    Lemma cal_qslock_pool_status_init:
      ∀ l z,
        cal_qslock_pool_status (ZMap.init MultiUndef) l z.
    Proof.
      unfold cal_qslock_pool_status.
      intros. rewrite ZMap.gi in Hdef. inv Hdef.
    Qed.

    Lemma cal_qslock_pool_status_gss´:
      ∀ l k c l´ z
             (HP: cal_qslock_pool_status l k c)
             (Hc: cal_qslock_status l´ (ZMap.get z k) c),
        cal_qslock_pool_status
          (ZMap.set z (MultiDef l´) l) k c.
    Proof.
      intros. unfold cal_qslock_pool_status in *; intros.
      destruct (zeq r z); subst.
      - rewrite ZMap.gss in ×. inv Hdef. trivial.
      - rewrite ZMap.gso in *; eauto.
    Qed.

    Lemma cal_qslock_pool_status_gss:
      ∀ l k c l´ k´ z
             (HP: cal_qslock_pool_status l k c)
             (Hc: cal_qslock_status l´ k´ c),
        cal_qslock_pool_status
          (ZMap.set z (MultiDef l´) l) (ZMap.set z k´ k) c.
    Proof.
      intros.
      unfold cal_qslock_pool_status in *; intros.
      destruct (zeq r z); subst.
      - rewrite ZMap.gss in ×. inv Hdef.
        trivial.
      - rewrite ZMap.gso in *; eauto.
    Qed.

    Lemma real_cal_qslock_pool_status_pb:
      ∀ n l d c
             (Hc: cal_qslock_pool_status l d c),
        cal_qslock_pool_status (CalTicketLock.real_multi_log_pb n l)
                               (CalTicketLock.real_lock_pb n d) c.
    Proof.
      induction n; simpl; intros; trivial.
      eapply cal_qslock_pool_status_gss; eauto.
      unfold cal_qslock_status.
      intros. simpl in Hcal. inv Hcal.
      split; intro HF; inv HF.
    Qed.

    Lemma real_cal_qslock_pool_status:
      ∀ l d c
             (HP: cal_qslock_pool_status l d c),
        cal_qslock_pool_status
          (CalTicketLock.real_multi_log l) (CalTicketLock.real_lock d) c.
    Proof.
      unfold CalTicketLock.real_multi_log.
      unfold CalTicketLock.real_lock.
      eapply real_cal_qslock_pool_status_pb.
    Qed.

    Lemma cal_qslock_status_shared_pull:
      ∀ l c
             (Hc: cal_qslock_status l (LockOwn false) c),
        cal_qslock_status (TEVENT c (TSHARED OPULL) :: l) (LockOwn true) c.
    Proof.
      unfold cal_qslock_status; intros.
      split; intros HF; inv HF.
      Local Transparent QS_CalLock.
      simpl in Hcal. subdestruct; subst.
      inv Hcal. exploit Hc; eauto.
      intros (HF & _). rewrite HF; trivial.
      Local Opaque QS_CalLock.
    Qed.

    Lemma cal_qslock_status_shared:
      ∀ l c m
             (Hc: cal_qslock_status l (LockOwn true) c),
        cal_qslock_status (TEVENT c (TSHARED (OMEME m)) :: l) (LockOwn false) c.
    Proof.
      unfold cal_qslock_status; intros.
      Local Transparent QS_CalLock.
      simpl in Hcal. subdestruct; subst.
      inv Hcal. exploit Hc; eauto.
      intros (_ & HT).
      split; intros HP; inv HP.
      rewrite HT; trivial.
      rewrite zeq_true. trivial.
      Local Opaque QS_CalLock.
    Qed.

    Lemma cal_status_SET_BUSY:
      ∀ l c
             (Hc: cal_qslock_status l (LockOwn false) c),
        cal_qslock_status (TEVENT c (TTICKET SET_BUSY) :: l) LockFalse c.
    Proof.
      Local Transparent QS_CalLock.
      unfold cal_qslock_status.
      simpl; intros.
      subdestruct; inv Hcal.
      exploit Hc; eauto.
      intros (HL & _). specialize (HL refl_equal). rewrite HL.
      split; intros HP; inv HP.
      Local Opaque QS_CalLock.
    Qed.

    Lemma cal_status_CAS_TAIL_true:
      ∀ l c
             (Hc: cal_qslock_status l (LockOwn false) c),
        cal_qslock_status (TEVENT c (TTICKET (CAS_TAIL true)) :: l) LockFalse c.
    Proof.
      Local Transparent QS_CalLock.
      unfold cal_qslock_status.
      simpl; intros.
      subdestruct; inv Hcal.
      exploit Hc; eauto.
      intros (HL & _). specialize (HL refl_equal). rewrite HL.
      split; intros HP; inv HP.
      Local Opaque QS_CalLock.
    Qed.

  End cal_qslock_status.

  Section free_qslock_prop.

    Lemma get_free_qslock_pool_init:
      get_free_qslock_pool (ZMap.init MultiUndef).
    Proof.
      unfold get_free_qslock_pool.
      intros. rewrite ZMap.gi in Hdef. inv Hdef.
    Qed.

    Lemma get_free_qslock_pool_gss:
      ∀ l l´ z
             (HP: get_free_qslock_pool l)
             (Hc: get_free_qslock l´),
        get_free_qslock_pool
          (ZMap.set z (MultiDef l´) l).
    Proof.
      intros. unfold get_free_qslock_pool in *; intros.
      destruct (zeq r z); subst.
      - rewrite ZMap.gss in ×. inv Hdef. trivial.
      - rewrite ZMap.gso in *; eauto.
    Qed.

    Lemma real_get_free_qslock_pool_pb:
      ∀ n l
             (Hc: get_free_qslock_pool l),
        get_free_qslock_pool (CalTicketLock.real_multi_log_pb n l).
    Proof.
      induction n; simpl; intros; trivial.
      eapply get_free_qslock_pool_gss; eauto.
      unfold get_free_qslock.
      intros. trivial.
    Qed.

    Lemma real_get_free_qslock_pool:
      ∀ l
             (HP: get_free_qslock_pool l),
        get_free_qslock_pool
          (CalTicketLock.real_multi_log l).
    Proof.
      unfold CalTicketLock.real_multi_log.
      eapply real_get_free_qslock_pool_pb.
    Qed.

    Lemma get_free_qslock_shared:
      ∀ l c e self_c other_c q slow tq
             (Hcal: QS_CalLock l = Some (self_c, other_c, LHOLD, q, slow, tq)),
        get_free_qslock (TEVENT c (TSHARED e) :: l).
    Proof.
      Local Transparent QS_CalLock.
      unfold get_free_qslock; intros.
      simpl in ×. rewrite Hcal in Hcal0.
      subst.
      subdestruct.
      Local Opaque QS_CalLock.
    Qed.

    Lemma get_free_SET_BUSY:
      ∀ l c
             (Hcal: CalValidBit l = Some FreeToPull),
        get_free_qslock (TEVENT c (TTICKET SET_BUSY) :: l).
    Proof.
      Local Transparent QS_CalLock.
      unfold get_free_qslock.
      simpl; intros.
      rewrite Hcal. trivial.
      Local Opaque QS_CalLock.
    Qed.

    Lemma get_free_CAS_TAIL_true:
      ∀ l c
             (Hcal: CalValidBit l = Some FreeToPull),
        get_free_qslock (TEVENT c (TTICKET (CAS_TAIL true)) :: l).
    Proof.
      Local Transparent QS_CalLock.
      unfold get_free_qslock.
      simpl; intros.
      rewrite Hcal. trivial.
      Local Opaque QS_CalLock.
    Qed.

  End free_qslock_prop.

  Record high_level_invariant (abd: RData) :=
    mkInvariant {
        CPU_ID_range: 0 ≤ (CPU_ID abd) < TOTAL_CPU;
        valid_curid: 0 ≤ ZMap.get (CPU_ID abd) (cid abd) < num_proc;
        valid_qslock_pool_inv: valid_qslock_pool (multi_log abd);
        valid_qslock_pool_status_inv:
          correct_qslock_pool_status (multi_log abd) (lock abd) (CPU_ID abd);
        valid_qs_oracle_pool_inv: valid_qs_oracle_pool (multi_oracle abd);

        cal_qslock_pool_status_inv:
          cal_qslock_pool_status (multi_log abd) (lock abd) (CPU_ID abd);
        get_free_qslock_pool_inv:
          get_free_qslock_pool (multi_log abd);
        get_free_qslock_oracle_pool_inv: get_free_qslock_oracle_pool (multi_oracle abd);

        relate_mcs_qs_oracle_inv: relate_mcs_qs_oracle_pool (multi_oracle abd);
        relate_qs_mcs_log_inv: relate_qs_mcs_log_pool (multi_log abd)
      }.

  Global Instance mqmcslockop_data_ops : CompatDataOps RData :=
    {
      empty_data := init_adt mcs_oracle_init0;
      high_level_invariant := high_level_invariant;
      low_level_invariant := low_level_invariant;
      kernel_mode adt := ikern adt = true ∧ ihost adt = true
    }.

  Section Property_Abstract_Data.

    Lemma correct_qslock_pool_status_init:
      ∀ l z,
        correct_qslock_pool_status (ZMap.init MultiUndef) l z.
    Proof.
      unfold correct_qslock_pool_status.
      intros.
      rewrite ZMap.gi in Hdef.
      inv Hdef.
    Qed.

    Lemma empty_data_high_level_invariant:
      high_level_invariant (init_adt mcs_oracle_init0).
    Proof.
      constructor; trivial; simpl; try congruence; intros.
      - apply current_CPU_ID_range.
      - rewrite ZMap.gi; intuition.
      - apply valid_qslock_pool_init.
      - apply correct_qslock_pool_status_init.
      - apply valid_mcs_oracle11.       - apply cal_qslock_pool_status_init.
      - apply get_free_qslock_pool_init.
      - eapply get_free_qslock_oracle0.

      - apply valid_mcs_oracle12.       -
        constructor; intros.
        rewrite ZMap.gi; constructor.
    Qed.

    Global Instance mqmcslockop_data_prf : CompatData RData.
    Proof.
      constructor.
      - apply low_level_invariant_incr.
      - apply empty_data_low_level_invariant.
      - apply empty_data_high_level_invariant.
    Qed.

  End Property_Abstract_Data.

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

  Section INV.

    Global Instance setPG_inv: PreservesInvariants setPG_spec.
    Proof.
      preserves_invariants_simpl_auto.
    Qed.

    Global Instance fstore_inv: PreservesInvariants fstore´_spec.
    Proof.
      preserves_invariants_simpl_auto.
    Qed.

    Global Instance setCR3_inv: SetCR3Invariants setCR3_spec.
    Proof.
      constructor; intros.
      - functional inversion H; inv H0; constructor; trivial.
      - functional inversion H; inv H0; constructor; auto.
      - functional inversion H; simpl in *; assumption.
    Qed.

    Global Instance trapin_inv: PrimInvariants trapin_spec.
    Proof.
      PrimInvariants_simpl_auto.
    Qed.

    Global Instance trapout_inv: PrimInvariants trapout´_spec.
    Proof.
      PrimInvariants_simpl_auto.
    Qed.

    Global Instance hostin_inv: PrimInvariants hostin_spec.
    Proof.
      PrimInvariants_simpl_auto.
    Qed.

    Global Instance hostout_inv: PrimInvariants hostout´_spec.
    Proof.
      PrimInvariants_simpl_auto.
    Qed.

    Global Instance set_curid_inv: PreservesInvariants set_curid_spec.
    Proof.
      preserves_invariants_simpl_auto; eauto 2.
      - rewrite ZMap.gss. auto.
    Qed.

    Global Instance cli_inv: PreservesInvariants cli_spec.
    Proof.
      econstructor; intros; inv H; functional inversion H1; subst.
      - inv H0; constructor; trivial.
      - inv H0; constructor; auto.
      - simpl in *; assumption.
    Qed.

    Global Instance sti_inv: PreservesInvariants sti_spec.
    Proof.
      econstructor; intros; inv H; functional inversion H1; subst.
      - inv H0; constructor; trivial.
      - inv H0; constructor; auto.
      - simpl in *; assumption.
    Qed.

    Require Import FutureTactic.

    Global Instance serial_in_inv: PreservesInvariants serial_in_spec.
    Proof.
      preserves_invariants_subst low_level_invariant high_level_invariant;
      try eauto using valid_qslock_pool_inv0;
      try eauto using valid_qslock_pool_status_inv0;
      try eauto using valid_qs_oracle_pool_inv0.
    Qed.

    Global Instance serial_out_inv: PreservesInvariants serial_out_spec.
    Proof.
      preserves_invariants_subst low_level_invariant high_level_invariant;
      try eauto using valid_qslock_pool_inv0;
      try eauto using valid_qslock_pool_status_inv0;
      try eauto using valid_qs_oracle_pool_inv0.
    Qed.

    Global Instance serial_hw_intr_inv: PreservesInvariants serial_hw_intr_spec.
    Proof.
      preserves_invariants_nested low_level_invariant high_level_invariant;
      try eauto using valid_qslock_pool_inv0;
      try eauto using valid_qslock_pool_status_inv0;
      try eauto using valid_qs_oracle_pool_inv0.
    Qed.

    Global Instance ic_intr_inv: PreservesInvariants ic_intr_spec.
    Proof.
      preserves_invariants_nested low_level_invariant high_level_invariant;
      try eauto using valid_qslock_pool_inv0;
      try eauto using valid_qslock_pool_status_inv0;
      try eauto using valid_qs_oracle_pool_inv0.
    Qed.

    Global Instance keyboard_in_inv: PreservesInvariants keyboard_in_spec.
    Proof.
      preserves_invariants_subst low_level_invariant high_level_invariant;
      try eauto using valid_qslock_pool_inv0;
      try eauto using valid_qslock_pool_status_inv0;
      try eauto using valid_qs_oracle_pool_inv0.
    Qed.

    Global Instance keyboard_hw_intr_inv: PreservesInvariants keyboard_hw_intr_spec.
    Proof.
      preserves_invariants_nested low_level_invariant high_level_invariant;
      try eauto using valid_qslock_pool_inv0;
      try eauto using valid_qslock_pool_status_inv0;
      try eauto using valid_qs_oracle_pool_inv0.
    Qed.

    Global Instance ioapic_read_inv: PreservesInvariants ioapic_read_spec.
    Proof.
      preserves_invariants_simpl low_level_invariant high_level_invariant;
      try eauto using valid_qslock_pool_inv0;
      try eauto using valid_qslock_pool_status_inv0;
      try eauto using valid_qs_oracle_pool_inv0.
    Qed.

    Global Instance ioapic_write_inv: PreservesInvariants ioapic_write_spec.
    Proof.
      preserves_invariants_simpl low_level_invariant high_level_invariant;
      try eauto using valid_qslock_pool_inv0;
      try eauto using valid_qslock_pool_status_inv0;
      try eauto using valid_qs_oracle_pool_inv0.
    Qed.

    Global Instance lapic_read_inv: PreservesInvariants lapic_read_spec.
    Proof.
      preserves_invariants_simpl low_level_invariant high_level_invariant;
      try eauto using valid_qslock_pool_inv0;
      try eauto using valid_qslock_pool_status_inv0;
      try eauto using valid_qs_oracle_pool_inv0.
    Qed.

    Global Instance lapic_write_inv: PreservesInvariants lapic_write_spec.
    Proof.
      preserves_invariants_simpl low_level_invariant high_level_invariant;
      try eauto using valid_qslock_pool_inv0;
      try eauto using valid_qslock_pool_status_inv0;
      try eauto using valid_qs_oracle_pool_inv0.
    Qed.

    Global Instance iret_inv: PreservesInvariants iret_spec.
    Proof.
      preserves_invariants_direct low_level_invariant high_level_invariant; eauto 2.
    Qed.

    Global Instance local_irq_save_inv: PreservesInvariants local_irq_save_spec.
    Proof.
      preserves_invariants_simpl low_level_invariant high_level_invariant; eauto 2.
    Qed.

    Global Instance local_irq_restore_inv: PreservesInvariants local_irq_restore_spec.
    Proof.
      preserves_invariants_simpl low_level_invariant high_level_invariant; eauto 2.
    Qed.

    Global Instance save_context_inv: SaveContextInvariants save_context_spec.
    Proof.
      constructor; intros.
      -
        inv H0. unfold save_context_spec; simpl. inv H1.
        constructor; simpl; trivial.
        induction (tf d).
        simpl.
        constructor.
        constructor.
        simpl.
        apply inv_reg_wt.
        simpl.
        inv inv_inject_neutral.
        eapply inv_reg_inject_neutral; auto.
        constructor.
        constructor.
        inv tf_INJECT.
        assumption.
        eapply IHt; auto.
        inv tf_INJECT.
        assumption.
      -
        inv H0. unfold save_context_spec; simpl.
        constructor; simpl; trivial.
    Qed.

    Global Instance restore_context_inv: RestoreContextInvariants restore_context_spec.
    Proof.
      constructor; intros.
      -
        inv H0.
        functional inversion H; inv H1;
        constructor; simpl; trivial.
        rewrite H4 in ×.
        clear H4 H.
        generalize dependent _x.
        induction _x0.
        intros.
        simpl in ×.
        constructor.
        intros.
        simpl in ×.
        constructor.
        inv tf_INJECT.
        assumption.
        eapply IH_x0; auto.
        inv tf_INJECT; assumption.
      -
        inv H0.
        functional inversion H; subst;
        constructor; simpl; trivial.
    Qed.

    Global Instance mcs_lock_init_inv: PreservesInvariants ticket_lock_init0_spec.
    Proof.
      preserves_invariants_simpl low_level_invariant high_level_invariant.
      - eapply real_valid_qslock_pool; trivial.
      - eapply real_correct_qslock_pool_status; eauto.
      - assumption.
      - eapply real_cal_qslock_pool_status; eauto.
      - eapply real_get_free_qslock_pool; eauto.
      - assumption.
      - eapply real_relate_qs_mcs_log_pool; eauto.
    Qed.

    Section AUXFORINV.

      Lemma update_abd_log_inv : ∀ abid l LOCK habd,
        high_level_invariant habd →
        valid_qslock l →
        correct_qslock_status l LOCK (CPU_ID habd) →
        cal_qslock_status l LOCK (CPU_ID habd) →
        get_free_qslock l →
        relate_qs_mcs_log l →
        high_level_invariant
          (habd {multi_log : ZMap.set abid (MultiDef l) (multi_log habd)})
          {lock : ZMap.set abid LOCK (lock habd)}.
      Proof.
        inversion 1.
        constructor; auto.
        - unfold valid_qslock_pool.
          intros i ofs r q H_ofs.
          destruct (zeq r abid).
          + subst.
            simpl.
            rewrite ZMap.gss.
            intros.
            replace q with l by congruence.
            assumption.
          + simpl.
            repeat rewrite ZMap.gso by assumption.
            intros.
            eauto using valid_qslock_pool_status_inv0.
        - unfold correct_qslock_pool_status.
          intros.
          simpl.
          destruct (zeq r abid).
          + subst.
            simpl in *; rewrite ZMap.gss in ×.
            inv Hdef; auto.
          + simpl in ×.
            rewrite ZMap.gso by assumption.
            rewrite ZMap.gso in Hdef by assumption.
            econstructor.
            × exploit valid_qslock_pool_status_inv0; eauto.
              intros.
              destruct H5.
              eapply H5; eauto.
            × exploit valid_qslock_pool_status_inv0; eauto.
              intros.
              destruct H5.
              eapply H7; eauto.
        - unfold cal_qslock_pool_status.
          intros.
          unfold cal_qslock_status.
          intros.
          case_eq (zeq r abid).
          + intros; subst; simpl in ×.
            rewrite ZMap.gss.
            rewrite ZMap.gss in Hdef.
            inv Hdef.
            unfold cal_qslock_status in H2.
            eapply H2; eauto.
          + intros.
            simpl in ×.
            repeat rewrite ZMap.gso; auto.
            rewrite ZMap.gso in Hdef; auto.
            exploit cal_qslock_pool_status_inv0; eauto.
        - unfold get_free_qslock_pool.
          intros.
          unfold get_free_qslock.
          intros.
          case_eq (zeq r abid).
          + intros; subst; simpl in ×.
            unfold get_free_qslock in H3.
            rewrite ZMap.gss in Hdef.
            inv Hdef.
            eapply H3; eauto.
          + intros.
            simpl in ×.
            repeat rewrite ZMap.gso; auto.
            rewrite ZMap.gso in Hdef; auto.
            exploit get_free_qslock_pool_inv0; eauto.
        - simpl.
          econstructor.
          intros.
          destruct (zeq z abid).
          + subst; rewrite ZMap.gss.
            econstructor.
            eauto.
          + rewrite ZMap.gso by assumption.
            inversion relate_qs_mcs_log_inv0.
            eauto using Hrelate_qs_mcs_log_type.
      Qed.

      Lemma cpu_not_NULL : ∀ cpu,
          0 ≤ cpu < Constant.TOTAL_CPU →
          cpu ≠ NULL.
      Proof.
        intros; unfold NULL; omega.
      Qed.

      Lemma tail_id_last : ∀ queue,
          tail_id queue = last (map qthread_tid queue) NULL.
      Proof.
        induction queue.
        + reflexivity.
        + simpl.
          destruct queue.
        - reflexivity.
        - rewrite IHqueue.
          reflexivity.
      Qed.

      Lemma wait_lock_kernel_mode : ∀ d d´ bound n ofs,
          wait_qslock_spec bound n ofs d = Some d´ →
          ikern d´ = ikern d ∧ ihost d´ = ihost d.
      Proof.
        intros until ofs.
        intros Hwait.
        unfold wait_qslock_spec in Hwait.
        repeat match goal with | [HCal´ : context[match ?X with | nil ⇒ _ | (_ :: _) ⇒ _ end] |- _] ⇒ destruct X
                          | [HCal´ : context[if ?X then _ else _] |- _] ⇒ destruct X eqn:?
                          | [HCal´ : context[match ?X with | O ⇒ _ | S _ ⇒ _ end] |- _] ⇒ destruct X eqn:?
                          | [HCal´ : context[match QS_CalLock ?X with Some _ ⇒ _ | None ⇒ _ end] |- _] ⇒
                            destruct (QS_CalLock X) as [[[[[[? ?] ?] ?] ?] ?] | ]
                          | [HCal´ : context[match ?X with | Some _ ⇒ _ | None ⇒ _ end] |- _] ⇒ destruct X eqn:?
                          | [HCal´ : context[match ?X with | MultiUndef ⇒ _ | MultiDef _ ⇒ _ end] |- _] ⇒ destruct X eqn:?
               end; try congruence;
        inversion Hwait;
        simpl; split; congruence.
      Qed.

      Lemma pass_lock_kernel_mode : ∀ d d´ i j,
          pass_qslock_spec i j d = Some d´ →
          ikern d´ = ikern d ∧ ihost d´ = ihost d.
      Proof.
        intros until j.
        intros Hwait.
        unfold pass_qslock_spec in Hwait.
        repeat match goal with | [HCal´ : context[match ?X with | nil ⇒ _ | (_ :: _) ⇒ _ end] |- _] ⇒ destruct X
                          | [HCal´ : context[if ?X then _ else _] |- _] ⇒ destruct X eqn:?
                          | [HCal´ : context[match ?X with | O ⇒ _ | S _ ⇒ _ end] |- _] ⇒ destruct X eqn:?
                          | [HCal´ : context[match QS_CalLock ?X with Some _ ⇒ _ | None ⇒ _ end] |- _] ⇒
                            destruct (QS_CalLock X) as [[[[[[? ?] ?] ?] ?] ?] | ]
                          | [HCal´ : context[match ?X with | Some _ ⇒ _ | None ⇒ _ end] |- _] ⇒ destruct X eqn:?
                          | [HCal´ : context[match ?X with | MultiUndef ⇒ _ | MultiDef _ ⇒ _ end] |- _] ⇒ destruct X eqn:?
               end; try congruence; subdestruct;
        inversion Hwait.
        - simpl; split; congruence.
        - simpl; split; congruence.
      Qed.

      Transparent QS_CalLock.

      Lemma wait_lock_preserve_inv:
        ∀ habd habd´ bound n ofs
               (HhighQ: high_level_invariant habd),
          wait_qslock_spec bound n ofs habd = Some habd´
          → high_level_invariant habd´.
      Proof.
        unfold wait_qslock_spec.
        intros until ofs.
        intros HhighQ.

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

        inversion HhighQ.

        inv relate_qs_mcs_log_inv0.
        specialize (Hrelate_qs_mcs_log_type _ _ _ H_abid).

        inv relate_mcs_qs_oracle_inv0.
        specialize (Hrelate_qs_mcs_oracle _ _ _ H_abid).

        specialize (valid_qs_oracle_pool_inv0 _ _ _ H_abid).
        destruct valid_qs_oracle_pool_inv0 as [Hvalid_oracle Hvalid_oracle_queue].


        destruct (ZMap.get abid (multi_log habd)) as [|ll] eqn:H_l;
          intros Hwait_qlock; try congruence.

        specialize (get_free_qslock_pool_inv0 _ _ _ _ H_abid H_l).
        specialize (get_free_qslock_oracle_pool_inv0 _ _ _ H_abid).

        inversion Hrelate_qs_mcs_log_type; subst.

        remember (ZMap.get abid (multi_oracle habd)) as o.
        clear Heqo.

        unfold correct_qslock_pool_status in valid_qslock_pool_status_inv0.
        specialize (valid_qslock_pool_status_inv0 _ _ _ _ H_abid H_l).

        pose (curid := CPU_ID habd).

        destruct (ZMap.get abid (lock habd)) eqn: H_lock; [|congruence].

        inversion Hrelate_qs_mcs_oracle; subst.

        pose (ll1 := o curid ll ++ ll).
        assert (relate_qs_mcs_log ll1) as Hrelate_log1.
        { unfold ll1.
          apply Hrelate_mcs_qs_oracle_res; assumption.
        }
        change (o (CPU_ID habd) ll ++ ll) with ll1.
        change (o (CPU_ID habd) ll ++ ll) with ll1 in Hwait_qlock.

        destruct (Hrelate_qs_mcs_log) as [queue H_CalMCS HCalLock].
        assert (¬ In curid (map qthread_tid queue)) as H_not_In_queue.
        {
          unfold correct_qslock_status in valid_qslock_pool_status_inv0.
          inversion HCalLock as [self_c1 rel_c1 b1 q1 slow1 tq1 Hb1 Hq1 Htq1 Hslow1 HCalLock_inv].
          symmetry in HCalLock_inv.
          specialize (valid_qslock_pool_status_inv0 _ _ _ _ _ _ HCalLock_inv).
          destruct valid_qslock_pool_status_inv0 as [valid_qslock_pool_status_inv0 _].
          specialize (valid_qslock_pool_status_inv0 eq_refl).
          subst.
          exact valid_qslock_pool_status_inv0.
        }

        destruct Hrelate_log1 as [queue1 H_CalMCS1 H_CalLock1].

        assert (¬ In curid (map qthread_tid queue1)) as H_not_In_queue1.
        {
          apply (other_threads_preserve_Not_In _ ll (o curid ll) queue).
          - exact H_CalMCS1.
          - assumption.
          - assumption.
          - intros k e.
            apply Hvalid_oracle.
        }

        assert (get_free_qslock ll1) as Hfree1 by (apply get_free_qslock_oracle_pool_inv0; assumption).

        clearbody ll1.
        clear ll H_l valid_qslock_pool_status_inv0 Hrelate_qs_mcs_log_type get_free_qslock_pool_inv0 queue H_CalMCS HCalLock
              H_not_In_queue.

        destruct (Q_CalMCSLock_completeness _ _ H_CalMCS1) as [[old_tail la] H_CalMCS].

        inversion H_CalLock1 as [self_c1 rel_c1 b1 q1 slow1 tq1 Hb1 Hq1 Hslow1 Htq1 HCalLock1_inv].
        symmetry in HCalLock1_inv.

        rewrite HCalLock1_inv in Hwait_qlock.
        destruct (zeq old_tail CalMCSLock.NULL).
        + assert (queue1 = nil) as Hq1_nil.
          { assert (tailsound := tail_soundness ll1 queue1 H_CalMCS1 _ _ _ H_CalMCS).
            rewrite (Q_CalMCSLock_tail_id_nil ll1 queue1).
            reflexivity.
            auto.
            congruence.
          }
          rewrite Hq1_nil in ×.
          clear Hq1_nil.
          rewrite Hq1 in ×.
          simpl in Hwait_qlock.

          pose (ll2 := (TEVENT curid (TTICKET (SWAP_TAIL (nat_of_Z bound) true))) :: ll1).
          inversion Hwait_qlock.
          change (TEVENT (CPU_ID habd) (TTICKET (SWAP_TAIL (nat_of_Z bound) true)) :: ll1) with ll2.

          assert (QCalLock2 : QS_CalLock ll2 = Some (S (nat_of_Z bound), (S CalPassLockTime),
                                                     LHOLD, curid :: nil, ZSet.empty, nat_of_Z bound :: nil)).
          {
            simpl.
            rewrite HCalLock1_inv.
            rewrite Htq1.
            simpl.
            reflexivity.
          }
          assert (relate_qs_mcs_log ll2) as Hrelate_log2.
          {
            apply RELATE_QS_MCS_LOG with (q:= (QT MCS_INSIDE curid (nat_of_Z bound))::nil).
            × apply Q_CalMCSLock_SWAP_nil.
            - apply (cpu_not_NULL _ CPU_ID_range0).
            - auto.
              × rewrite QCalLock2.
                apply QSTATE_OF_QMCSLOCKSTATE; reflexivity.
          }

          assert (get_free_qslock ll2) as Hfree2.
          {
            specialize (Hfree1 _ _ _ _ _ _ HCalLock1_inv Hb1).
            unfold get_free_qslock.
            intros.
            unfold ll2.
            simpl.
            rewrite Hfree1.
            reflexivity.
          }

          assert (CalValidBit ll2 = Some FreeToPull) as Hfree2´.
          {
            specialize (Hfree1 _ _ _ _ _ _ HCalLock1_inv Hb1).
            unfold ll2.
            simpl.
            rewrite Hfree1.
            reflexivity.
          }
          
          clearbody ll2.
          apply update_abd_log_inv.
          × assumption.
          × unfold valid_qslock.
            inversion Hrelate_log2 as [queue2 HQCal2 HStateOfLockState2].
            inversion HStateOfLockState2 as [selc_c2 rel_c2 b2 q2 slow2 tq2 Hb2 Hqs2 Htq2 HQCal2_inv].
            symmetry in HQCal2_inv.
            repeat eexists; exact QCalLock2.
          × unfold correct_qslock_status.
            intros.
            split; [ intros; congruence| ].
            ∃ nil.
            fold curid.
            repeat split; try congruence.
            simpl; tauto.

            rewrite QCalLock2 in Hcal.
            inv Hcal.
            omega.

          × unfold cal_qslock_status.
            intros.
            split; intros; [exact Hfree2´ | congruence].
          × exact Hfree2.
          × assumption.
        + assert (old_tail = tail_id queue1) as Htail_id by (eapply tail_soundness; eauto).
          destruct (Q_CalMCSLock_tail_id_nonnil queue1) as [q0 [s [bi Hq0]]].
          congruence.

          pose (ll2 := (TEVENT curid (TTICKET (SWAP_TAIL (nat_of_Z bound) false))) :: ll1).

          assert (Q_CalMCSLock ll2 ((queue1 ++ (QT MCS_BEFORE_SET_NEXT curid (nat_of_Z bound)) :: nil))).
          {
            unfold ll2.
            apply Q_CalMCSLock_SWAP_not_nil.
            auto.
            rewrite Hq0; destruct q0; simpl; discriminate.
            apply (cpu_not_NULL _ CPU_ID_range0).
            assumption.
          }

          assert (queue1 ≠ nil) by (rewrite Hq0; destruct q0; discriminate).

          assert (QState_of_QMCSLockState (queue1 ++ QT MCS_BEFORE_SET_NEXT curid (nat_of_Z bound) :: nil) (QS_CalLock ll2)).
          {
            simpl.
            rewrite HCalLock1_inv.

            assert (¬ In curid q1) as H_not_In_q1 by (rewrite Hq1; assumption).
            destruct (in_dec zeq curid q1); [tauto |].

            destruct queue1 as [|[s0 i0 b0] q12]; [congruence|].
            rewrite Hq1.
            simpl.

            assert (curid ≠ i0)
              by (simpl in H_not_In_queue1; intros ?; apply H_not_In_queue1; left; congruence; tauto).
            destruct (zeq curid i0) eqn:Heq_curid; [congruence|].

            rewrite Htq1.
            simpl.

            apply QSTATE_OF_QMCSLOCKSTATE.
            × rewrite Hb1; reflexivity.
            × simpl; rewrite map_app; reflexivity.
            × simpl.
              rewrite Hslow1.
              destruct s0;
                rewrite <- slowset_BEFORE_SET_NEXT; try rewrite ZSet_add_commute; reflexivity.
            × simpl. rewrite map_app. reflexivity.
          }

          assert (relate_qs_mcs_log ll2).
          {
            apply RELATE_QS_MCS_LOG with (q:= (queue1 ++ (QT MCS_BEFORE_SET_NEXT curid (nat_of_Z bound)) :: nil)).
            × apply Q_CalMCSLock_SWAP_not_nil; auto.
              apply (cpu_not_NULL _ CPU_ID_range0).
            × assumption.
          }

          assert (get_free_qslock ll2) as Hfree2 by (apply SWAP_TAIL_false_preserves_get_free_qslock; assumption).

          pose (ll3 := o curid ll2 ++ ll2).
          assert (relate_qs_mcs_log ll3) as Hrelate_log3
                                           by (apply Hrelate_mcs_qs_oracle_res; assumption).

          assert (old_tail = (last q1 NULL)) as Hold_tail.
          {
            rewrite Htail_id.
            rewrite Hq1.
            apply tail_id_last.
          }
          rewrite <- Hold_tail in Hwait_qlock.

          destruct Hrelate_log3 as [queue3 H_QCalMCS3 H_QCal3].
          assert (thread_before_set_next old_tail curid queue3) as Hbefore_set_next.
          {
            apply (other_threads_preserve_BEFORE_SET_NEXT _ _ ll2 (o curid ll2) (queue1 ++ (QT MCS_BEFORE_SET_NEXT curid (nat_of_Z bound)) :: nil)).
            assumption.
            assumption.
            rewrite Hq0.
            rewrite <- app_assoc; simpl.
            unfold thread_before_set_next.
            (replace (tail_id queue1) with old_tail by assumption); eauto 6.
            intros k e; apply Hvalid_oracle.
          }

          assert (get_free_qslock ll3) as Hfree3
            by (apply get_free_qslock_oracle_pool_inv0; assumption).

          pose (ll4 := (TEVENT curid (TTICKET (SET_NEXT old_tail))) :: ll3).

          change ((TEVENT (CPU_ID habd) (TTICKET (SET_NEXT old_tail))
                          :: o (CPU_ID habd) (TEVENT (CPU_ID habd) (TTICKET (SWAP_TAIL (nat_of_Z bound) false)) :: ll1) ++
                          TEVENT (CPU_ID habd) (TTICKET (SWAP_TAIL (nat_of_Z bound) false)) :: ll1)) with ll4.
          change ((TEVENT (CPU_ID habd) (TTICKET (SET_NEXT old_tail))
                          :: o (CPU_ID habd) (TEVENT (CPU_ID habd) (TTICKET (SWAP_TAIL (nat_of_Z bound) false)) :: ll1) ++
                          TEVENT (CPU_ID habd) (TTICKET (SWAP_TAIL (nat_of_Z bound) false)) :: ll1))
          with ll4 in Hwait_qlock.

          assert (get_free_qslock ll4) as Hfree4 by (apply SET_NEXT_preserves_get_free_qslock; assumption).

          destruct queue1 as [| [s0 i0 bi0]] eqn:?; [congruence|].
          rewrite Hq1 in Hwait_qlock.
          simpl in Hwait_qlock.
          change ( match map qthread_tid q with
                   | nil ⇒ i0
                   | _ :: _ ⇒ last (map qthread_tid q) NULL
                   end)
          with (last (map qthread_tid ((QT s0 i0 bi0):: q)) NULL) in Hwait_qlock.

          clear q0 s Hq0.
          destruct Hbefore_set_next as [q0 [s [b_old_tail [b_curid [qpost Hqueue3]]]]].
          pose (queue4 := q0 ++ (QT s old_tail b_old_tail) :: (QT MCS_WAITING_BUSY curid b_curid) :: qpost).
          assert (Q_CalMCSLock ll4 queue4).
          {
            unfold queue4.
            apply Q_CalMCSLock_SET_NEXT with (q := queue3).
            assumption.
            congruence.
          }

          assert (QState_of_QMCSLockState queue4 (QS_CalLock ll4)).
          {
            unfold queue4. unfold ll4.
            simpl.
            inversion H_QCal3 as [self_c3 rel_c3 b3 q3 slow3 tq3 Hb3 Hq3 Hslow3 Htq3 H_QCal3_inv].
            symmetry in H_QCal3_inv.

            rewrite Hq3.
            rewrite Htq3.
            rewrite Hslow3.

            replace (ZSet.mem curid (slowset_of_QMCSLockState queue3)) with true
              by (rewrite Hqueue3; rewrite BEFORE_SET_NEXT_is_slow;
                  [ reflexivity |
                    rewrite <- Hqueue3; eapply Q_CalMCSLock_NoDup; eauto]).

            assert (QState_of_QMCSLockState (q0 ++ QT s old_tail b_old_tail :: QT MCS_WAITING_BUSY curid b_curid :: qpost)
                                            (Some (self_c3, rel_c3, b3, map qthread_tid queue3,
                                                   ZSet.remove curid (slowset_of_QMCSLockState queue3), map qthread_bound queue3))).
            {
              apply QSTATE_OF_QMCSLOCKSTATE.
              + rewrite Hb3, Hqueue3.
                 rewrite QState_of_QMCSLockState_SET_NEXT_head_status.
                 reflexivity.
              + rewrite Hqueue3.
                rewrite QState_of_QMCSLockState_SET_NEXT_queue.
                reflexivity.
              + rewrite Hqueue3.
                rewrite QState_of_QMCSLockState_SET_NEXT_slowset with (l := ll3).
                reflexivity.
                rewrite <- Hqueue3; auto.
              + rewrite Hqueue3.
                rewrite QState_of_QMCSLockState_SET_NEXT_bounds.
                reflexivity.
            }

            rewrite Hqueue3.
            destruct q0.
            + simpl.
              destruct (zeq curid old_tail).
            -
              assert (NoDup (map qthread_tid queue4)) as Hnodup4
                                                        by (eauto using Q_CalMCSLock_NoDup).
              unfold queue4 in Hnodup4.
              simpl in Hnodup4.
              replace old_tail with curid in Hnodup4 by auto.
              inversion Hnodup4.
              simpl in ×.
              tauto.
            - simpl in H4.
              rewrite Hqueue3 in H4.
              exact H4.
              + simpl.
                destruct (zeq curid (qthread_tid q0)).
            -
              assert (NoDup (map qthread_tid queue4)) as Hnodup4
                                                        by (eauto using Q_CalMCSLock_NoDup).
              unfold queue4 in Hnodup4.
              simpl in Hnodup4.
              rewrite map_app in Hnodup4.
              simpl in Hnodup4.
              replace (qthread_tid q0) with curid in Hnodup4 by auto.
              inversion Hnodup4 as [| ? ? Hnodup4´].
              rewrite in_app in Hnodup4´.
              simpl in Hnodup4´.
              tauto.
            - simpl in H4.
              rewrite Hqueue3 in H4.
              exact H4.
          }

          assert (relate_qs_mcs_log ll4) by (apply (RELATE_QS_MCS_LOG ll4 queue4); assumption).

          assert (ZSet.mem curid (slowset_of_QMCSLockState queue4) = false).
          {
            unfold queue4.
            apply slowset_of_QMCSLockState_SET_NEXT_false.
            fold queue4.
            eauto using Q_CalMCSLock_NoDup.
          }

          destruct (QS_CalWaitGet (CalWaitLockTime tq1) (CPU_ID habd) ll4 o) as [hl´|] eqn:H_CalWaitGet;
            [|congruence].

          destruct (wait_lock_CalMCS_AcqWait o Hrelate_qs_mcs_oracle Hvalid_oracle get_free_qslock_oracle_pool_inv0 (CalWaitLockTime tq1) ll4 hl´ queue4 curid b_curid)
            as [H_CalWait_returns [Hrelate_log´ [Hcorrect_status Hfree´]]].
          { assumption. }
          { unfold queue4.
            rewrite in_app.
            right.
            simpl.
            auto.
          }
          { assumption. }
          {assumption. }
          { exact Hfree4. }
          { exact H_CalWaitGet. }

          replace habd´ with
          (habd {multi_log: ZMap.set abid (MultiDef hl´) (multi_log habd)}
                {lock: ZMap.set abid (LockOwn false) (lock habd)}) by congruence.
          apply update_abd_log_inv.
          × assumption.
          × unfold valid_qslock.
            destruct Hrelate_log´ as [queue´ H_QCalMCS´ H_QCal´].
            destruct H_QCal´.
            repeat eexists; reflexivity.
          × exact Hcorrect_status.
          × unfold cal_qslock_status.
            intros.
            split;intros; [exact Hfree´ |congruence].
          × unfold get_free_qslock.
            intros.
            exact Hfree´.
          × assumption.
      Qed.

      Lemma pass_lock_preserve_inv:
        ∀ habd habd´ n ofs
               (HhighQ: high_level_invariant habd),
          pass_qslock_spec n ofs habd = Some habd´
          → high_level_invariant habd´.
      Proof.
        unfold mcs_pass_lock_spec, pass_qslock_spec.
        intros until ofs.
        intros HhighQ.

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

        inversion HhighQ.

        inv relate_qs_mcs_log_inv0.
        specialize (Hrelate_qs_mcs_log_type _ _ _ H_abid).
        inv relate_mcs_qs_oracle_inv0.
        specialize (Hrelate_qs_mcs_oracle _ _ _ H_abid).

        specialize (valid_qs_oracle_pool_inv0 _ _ _ H_abid).
        destruct valid_qs_oracle_pool_inv0 as [Hvalid_oracle _].

        destruct (ZMap.get abid (multi_log habd)) as [|ll] eqn: H_l ;
          intros Hpass_qlock; try congruence.

        specialize (get_free_qslock_pool_inv0 _ _ _ _ H_abid H_l).
        specialize (get_free_qslock_oracle_pool_inv0 _ _ _ H_abid).

        specialize (cal_qslock_pool_status_inv0 _ _ _ _ H_abid H_l).

        inversion Hrelate_qs_mcs_log_type; subst.

        remember (ZMap.get abid (multi_oracle habd)) as o.
        clear Heqo.

        unfold correct_qslock_pool_status in valid_qslock_pool_status_inv0.
        specialize (valid_qslock_pool_status_inv0 _ _ _ _ H_abid H_l).

        assert (CalValidBit ll = Some FreeToPull) as Hvalid.
        {
          unfold cal_qslock_status in cal_qslock_pool_status_inv0.
          destruct (ZMap.get abid (lock habd)); [congruence|].
          destruct b; [congruence|].
          destruct Hrelate_qs_mcs_log as [? ? H0].
          inversion H0 as [self_c rel_c b qs slow tq Hb Hqs Hslow Htq HCal_inv].
          symmetry in HCal_inv.
          destruct (cal_qslock_pool_status_inv0 _ _ _ _ _ _ HCal_inv) as [cal_qslock_pool_status_inv _].
          auto.
        }
        
        pose (curid := CPU_ID habd).

        inversion Hrelate_qs_mcs_oracle; subst.

        pose (ll1 := o curid ll ++ ll).
        change (o (CPU_ID habd) ll ++ ll) with ll1.
        change (o (CPU_ID habd) ll ++ ll) with ll1 in Hpass_qlock.
        assert (Hrelate_log1 : relate_qs_mcs_log ll1 ).
        { unfold ll1. apply Hrelate_mcs_qs_oracle_res; auto. }

        
        destruct Hrelate_qs_mcs_log as [queue H_QCalMCS H_QCal].
        assert (thread_has_lock curid queue) as Hhas_lock.
        {
          assert (Foo := CalLock_thread_has_lock queue).

          inversion H_QCal
            as [self_c rel_c b qs slow tq Hb Hqs Hslow Htq H_QCal_inv].
          symmetry in H_QCal_inv.

          destruct (ZMap.get abid (lock habd)); [congruence|].
          replace (CPU_ID habd) with (CPU_ID habd) in valid_qslock_pool_status_inv0 by congruence.
          unfold correct_qslock_status in valid_qslock_pool_status_inv0.
          specialize (valid_qslock_pool_status_inv0 self_c rel_c b qs tq slow H_QCal_inv).
          destruct valid_qslock_pool_status_inv0 as [_ valid_qslock_pool_status_inv0].
          destruct b0; [try inv Hpass_qlock |].
          assert (eq_refl: LockOwn false = LockOwn false) by reflexivity.
          destruct (valid_qslock_pool_status_inv0 _ eq_refl) as [queue0 [Hvalid1 [Hvalid2 _]]].
          apply Foo with (queue0 := queue0); unfold curid; congruence.
        }

        destruct (ZMap.get abid (lock habd)); [congruence|].

        destruct Hrelate_log1 as [queue1 H_QCalMCS1 H_QCal1].
        assert (thread_has_lock curid queue1) as Hhas_lock1.
        {
          unfold ll1 in H_QCalMCS1.
          apply (other_threads_preserve_thread_has_lock _ ll (o curid ll) queue); auto.
          intros k e.
          apply Hvalid_oracle.
        }

        assert (CalValidBit ll1 = Some FreeToPull) as Hvalid1.
        {
          destruct b; [congruence|].

          inversion H_QCal as [self_c rel_c b qs slow tq Hb Hqs Hslow Htq HQCal_inv].
          symmetry in HQCal_inv.
          inversion Hhas_lock.
          subst.
          simpl in HQCal_inv.

          inversion H_QCal1 as [self_c1 rel_c1 b1 qs1 slow1 tq1 Hb1 Hqs1 Hslow1 Htq1 HQCal_inv1].
          symmetry in HQCal_inv1.
          inversion Hhas_lock1.
          subst.
          simpl in HQCal_inv1.

          unfold ll1.
          apply (other_threads_preserve_FreeToPull _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ HQCal_inv HQCal_inv1); assumption.
        }
                
        clearbody ll1.
        clear ll H_l valid_qslock_pool_status_inv0 get_free_qslock_pool_inv0 cal_qslock_pool_status_inv0 Hrelate_qs_mcs_log_type queue H_QCalMCS H_QCal Hhas_lock Hvalid.

        inversion H_QCal1
          as [self_c1 rel_c1 b1 qs1 slow1 tq1 Hb1 Hqs1 Hslow1 Htq1 H_QCal_inv1].
        symmetry in H_QCal_inv1.

        destruct Hhas_lock1.
        rewrite H_QCal_inv1 in Hpass_qlock.
        rewrite Hqs1 in Hpass_qlock.
        simpl in Hpass_qlock.
        destruct (Q_CalMCSLock_completeness _ _ H_QCalMCS1) as [[old_tail1 la1] H_CalMCS1].

        destruct (zeq old_tail1 (CPU_ID habd)) as [H_old_tail1 | H_old_tail1].
        + rewrite (Q_CalMCSLock_tail_AT_HEAD ll1 MCS_INSIDE (CPU_ID habd) bi q0 H_QCalMCS1 old_tail1
                                             la1 bounds H_CalMCS1) in H_old_tail1.
          subst.
          simpl in ×.
          destruct b; [inv Hpass_qlock|].
          destruct rel_c1 as [|rel_c1´]; [congruence|].
          replace habd´
          with (habd {multi_log: ZMap.set abid
                                          (MultiDef (TEVENT (CPU_ID habd) (TTICKET (CAS_TAIL true)) :: ll1))
                                          (multi_log habd)}
                     {lock: ZMap.set abid LockFalse (lock habd)})
            by congruence.

          pose (ll2 := TEVENT (CPU_ID habd) (TTICKET (CAS_TAIL true)) :: ll1).

          assert (QS_CalLock ll2 = Some (0%nat, 0%nat, LEMPTY, nil, ZSet.empty, nil))
            as H_QCal_inv2.
          {
            simpl.
            rewrite H_QCal_inv1.
            simpl.
            fold curid; destruct (zeq curid curid); [|congruence].
            reflexivity.
          }
          assert (relate_qs_mcs_log ll2) as H_relate2.
          {
            apply RELATE_QS_MCS_LOG with (q:=nil).
            + apply Q_CalMCSLock_CAS_TAIL_true with (bi:=bi).
            - exact H_QCalMCS1.
              + rewrite H_QCal_inv2.
                apply QSTATE_OF_QMCSLOCKSTATE; reflexivity.
          }

          assert (CalValidBit ll2 = Some FreeToPull) as Hvalid2 by (simpl; rewrite Hvalid1; reflexivity).

          fold ll2.
          clearbody ll2.

          apply update_abd_log_inv.
          × assumption.
          × unfold valid_qslock.
            destruct H_relate2 as [queue2 H_CalMCS2 HCalLock2].
            inversion HCalLock2; repeat eexists.
          × unfold correct_qslock_status.
            intros.
            split; intros; [|congruence].
            rewrite H_QCal_inv2 in Hcal.
            replace q with (@nil Z) by congruence.
            simpl; auto.
          × unfold cal_qslock_pool_status.
            unfold cal_qslock_status.
            intros.
            split; intros; inv H.
          × unfold get_free_qslock.
            intros.
            assumption.
          × assumption.
        + assert (q0 ≠ nil).
          {
            pose (Q_CalMCSLock_tail_AT_HEAD ll1 MCS_INSIDE curid bi q0 H_QCalMCS1 old_tail1 la1 bounds H_CalMCS1).
            tauto.
          }
          destruct q0 as [|[s j bj] q00]; [congruence|].
          simpl in Hpass_qlock.

          pose (ll2 := (TEVENT curid (TTICKET (CAS_TAIL false)) :: ll1)).

          assert (Q_CalMCSLock ll2 ((QT MCS_INSIDE curid bi) :: (QT s j bj) :: q00)) as H_QCalMCS2
                                                                                       by (unfold ll2; apply Q_CalMCSLock_CAS_TAIL_false; auto).

          assert (relate_qs_mcs_log ll2) as Hrelate_log2.
          {
            apply RELATE_QS_MCS_LOG with (q := (QT MCS_INSIDE curid bi) :: (QT s j bj) :: q00).
            auto.
            unfold ll2.
            simpl.
            rewrite H_QCal_inv1.
            rewrite Hqs1, Hb1, Htq1.
            simpl.
            rewrite zeq_true.
            destruct b; [ inv Hpass_qlock|].
            destruct rel_c1 as [|rel_c´]; [congruence|].
            apply QSTATE_OF_QMCSLOCKSTATE.
            reflexivity.
            reflexivity.
            rewrite Hslow1; reflexivity.
            reflexivity.
          }

          assert (CalValidBit ll2 = Some FreeToPull) as Hvalid2
            by (simpl; rewrite Hvalid1; reflexivity).

          change (TEVENT (CPU_ID habd) (TTICKET (CAS_TAIL false)) :: ll1) with ll2.
          change (TEVENT (CPU_ID habd) (TTICKET (CAS_TAIL false)) :: ll1) with ll2 in Hpass_qlock.
          clearbody ll2.

          destruct b; [ inv Hpass_qlock|].
          destruct rel_c1 as [|rel_c1´]; [ congruence| ].

          destruct (QS_CalWaitRel CalPassLockLoopTime (CPU_ID habd) j ll2 o) as [ll´|] eqn:H_CalWaitRel;
            [|congruence].

          destruct (pass_lock_CalWaitRel curid j o Hvalid_oracle Hrelate_qs_mcs_oracle CalPassLockLoopTime ll2 ll´ _ H_QCalMCS2 H_CalWaitRel Hrelate_log2) as [H1_ll´ [H2_ll´ [HCal´ [H_correct_status´ Hvalid´]]]].
          { apply THREAD_HAS_LOCK_NEXT. }
          { exact Hvalid2. }

          fold curid.

          inversion H2_ll´ as [q´ H_QCalMCS´ H_QCal´].

          change ((o (CPU_ID habd)
                       (TEVENT (CPU_ID habd) (TTICKET GET_NEXT) :: ll´) ++
                       TEVENT (CPU_ID habd) (TTICKET GET_NEXT) :: ll´))
             with (pass_lock_final1 ll´ (CPU_ID habd) o)
            in Hpass_qlock.
          destruct HCal´ as [[? ?] [? [? [? [? [? HCal´]]]]]] .
          unfold curid in HCal´.
          rewrite HCal´ in Hpass_qlock.
          change (TEVENT (CPU_ID habd) (TTICKET SET_BUSY) :: pass_lock_final1 ll´ (CPU_ID habd) o)
            with (pass_lock_final ll´ (CPU_ID habd) o)
            in Hpass_qlock.

          replace habd´
          with (habd {multi_log: ZMap.set abid
                                           (MultiDef (pass_lock_final ll´ (CPU_ID habd) o))
                                           (multi_log habd)})
                     {lock : ZMap.set abid LockFalse (lock habd)}
            by congruence.


          apply update_abd_log_inv.
          × assumption.
          × unfold valid_qslock.
            fold curid.
            remember (pass_lock_final ll´ curid o) as ll´´.
            inversion H_QCal´.
            repeat eexists.
          × assumption.
          × unfold cal_qslock_pool_status.
            unfold curid in H_correct_status´.
            unfold cal_qslock_status.
            intros.
            split; intros; inv H0.
          × unfold get_free_qslock.
            intros.
            exact Hvalid´.
          × assumption.
      Qed.

    End AUXFORINV.

    Ltac preserves_invariants_simpl_with_hinv_lemma low_level_invariant high_level_invariant inv_lemma
      :=
        constructor; simpl; intros;
        match goal with
        | H:semof _ _ _ _ _
          |- _ ⇒
          inv_generic_sem H;
            match goal with
            | H1:_ = ret _, H0:low_level_invariant _ _
              |- _ ⇒
              inv H0; functional inversion H1; subst; constructor;
              trivial
            | H1:_ = ret _, H0:high_level_invariant _
              |- _ ⇒ intros; eauto using inv_lemma
            | H1:_ = ret _, H0:_ ∧ _
              |- _ ∧ _ ⇒
              functional inversion H1; subst; simpl; try assumption
            | _ ⇒ idtac
            end
        end.

    Global Instance wait_qslock_inv: PreservesInvariants wait_qslock_spec.
    Proof.
      preserves_invariants_simpl_with_hinv_lemma low_level_invariant high_level_invariant wait_lock_preserve_inv.
    Qed.

    Global Instance pass_qslock_inv: PreservesInvariants pass_qslock_spec.
    Proof.
      preserves_invariants_simpl_with_hinv_lemma low_level_invariant high_level_invariant pass_lock_preserve_inv.
    Qed.

    Inductive MCSMatchLock: LockStatus → LockStatus → Prop :=
    | MCSMLFALSE: MCSMatchLock LockFalse LockFalse
    | MCSMLOWN: ∀ a b,
        MCSMatchLock (LockOwn a) (LockOwn b).

    Lemma correct_qslock_status_Match:
      ∀ l k k´ c
             (Hc: correct_qslock_status l k c)
             (Hl: MCSMatchLock k´ k),
        correct_qslock_status l k´ c.
    Proof.
      intros. unfold correct_qslock_status in *; intros.
      exploit Hc; eauto.
      intros (HF & HO).
      split; intros; subst; eauto.
      - inv Hl. eapply HF; eauto.
      - inv Hl. eapply HO; eauto.
    Qed.

    Lemma correct_qslock_pool_status_gss_match:
      ∀ l k c l´ k´ z
             (HP: correct_qslock_pool_status l k c)
             (Hc: correct_qslock_status l´ (ZMap.get z k) c)
             (Hl: MCSMatchLock k´ (ZMap.get z k)),
        correct_qslock_pool_status
          (ZMap.set z (MultiDef l´) l) (ZMap.set z k´ k) c.
    Proof.
      intros. eapply correct_qslock_pool_status_gss; eauto.
      eapply correct_qslock_status_Match; eauto.
    Qed.

    Lemma correct_qslock_status_shared:
      ∀ l d c c´ e
             (Hc: correct_qslock_status l d c),
        correct_qslock_status (TEVENT c´ (TSHARED e) :: l) d c.
    Proof.
      unfold correct_qslock_status; intros.
      Transparent QS_CalLock.
      simpl in Hcal. subdestruct; inv Hcal.
      exploit Hc; eauto.
      Opaque QS_CalLock.
    Qed.

    Lemma QS_CalLock_append:
      ∀ e l p
             (Hcal: QS_CalLock (e :: l) = Some p),
      ∃ self_c other_c b q slow tq,
        QS_CalLock l = Some (self_c, other_c, b, q, slow, tq).
    Proof.
      Local Transparent QS_CalLock.
      simpl; intros. subdestruct; inv Hcal; eauto 20.
      Local Opaque QS_CalLock.
    Qed.

    Global Instance acquire_shared_inv: SAcquireInvariants acquire_shared1_mcs_spec0.
    Proof.
      constructor; unfold acquire_shared1_mcs_spec; intros; subdestruct;
      inv H; inv H0; constructor; auto.
      - eapply valid_qslock_pool_gss´; eauto.
      - simpl. eapply correct_qslock_pool_status_gss_match; eauto.
        + eapply correct_qslock_status_shared; eauto.
        + rewrite Hdestruct3. constructor.
      - simpl. eapply cal_qslock_pool_status_gss; eauto.
        eapply cal_qslock_status_shared_pull; eauto.
        unfold cal_qslock_pool_status in ×.
        rewrite <- Hdestruct3. eauto.
      - simpl. eapply get_free_qslock_pool_gss; eauto.
        eapply QS_CalLock_append in Hdestruct6.
        destruct Hdestruct6 as (self_c & other_c & b & q & slow & tq & Hcal).
        unfold correct_qslock_pool_status in ×.
        exploit valid_qslock_pool_status_inv0; eauto.
        rewrite Hdestruct3. intros (_ & HT).
        exploit HT; eauto.
        intros (_ & _ & ? & _); subst.
        eapply get_free_qslock_shared; eauto.
      - simpl.
        econstructor.
        intros.
        destruct (zeq z z0); subst.
        + rewrite ZMap.gss.
          econstructor.
          simpl.
          generalize Hdestruct6; intros Hcal´.
          eapply QS_CalLock_append in Hdestruct6.
          destruct Hdestruct6 as (self_c & other_c & b & q & slow & tq & Hcal).
          inv relate_qs_mcs_log_inv0.
          eapply Hrelate_qs_mcs_log_type in Hrange; eauto.
          rewrite Hdestruct5 in Hrange.
          inv Hrange.
          inv Hrelate_qs_mcs_log.
          eapply RELATE_QS_MCS_LOG.
          instantiate (1:= q0).
          eapply Q_CalMCSLock_SHARED_MEM; eauto.
          inv H0.
          generalize Hcal´; intro HCal´´.
          Transparent QS_CalLock.
          simpl in Hcal´.
          subdestruct.
          inv Hcal´.
          inv H1.
          inv Hcal.
          rewrite Hdestruct4.
          rewrite zeq_true.
          eapply QSTATE_OF_QMCSLOCKSTATE; eauto.
        + rewrite ZMap.gso; auto.
          inv relate_qs_mcs_log_inv0.
          eapply Hrelate_qs_mcs_log_type in Hrange; eauto.
          Opaque QS_CalLock.
    Qed.

    Global Instance release_shared_inv: ReleaseInvariants release_shared1_mcs_spec0.
    Proof.
      constructor; unfold release_shared1_mcs_spec; intros; subdestruct;
      inv H; inv H0; constructor; auto.
      - simpl; eapply valid_qslock_pool_gss´; eauto.
      - simpl. eapply correct_qslock_pool_status_gss_match; eauto.
        + eapply correct_qslock_status_shared; eauto.
        + rewrite Hdestruct3. constructor.
      - simpl. eapply cal_qslock_pool_status_gss; eauto.
        specialize (valid_qslock_pool_status_inv0 _ _ _ _ Hdestruct2 Hdestruct5).
        eapply cal_qslock_status_shared; eauto.
        unfold cal_qslock_pool_status in ×.
        rewrite <- Hdestruct3.
        eauto.
      - simpl. eapply get_free_qslock_pool_gss; eauto.
        eapply QS_CalLock_append in Hdestruct6.
        destruct Hdestruct6 as (self_c & other_c & b & q & slow & tq & Hcal).
        unfold correct_qslock_pool_status in ×.
        exploit valid_qslock_pool_status_inv0; eauto.
        rewrite Hdestruct3. intros (_ & HT).
        exploit HT; eauto.
        intros (_ & _ & ? & _); subst.
        eapply get_free_qslock_shared; eauto.
      - simpl.
        inv relate_qs_mcs_log_inv0.
        constructor; intros.
        exploit CalMCSLockLemmas.index2Z_in_lock_range; eauto; intros; simpl in ×.
        case_eq (zeq z0 z); intros; subst.
        + rewrite ZMap.gss; auto.
          constructor; intros.
          exploit Hrelate_qs_mcs_log_type; eauto.
          intros.
          inv H1; [ rewrite Hdestruct5 in H3; inv H3 | ].
          symmetry in H3.
          rewrite Hdestruct5 in H3; inv H3.
          rename l0 into l.
          Transparent QS_CalLock.
          simpl in Hdestruct6.
          subdestruct; inv Hdestruct6.
          inv Hrelate_qs_mcs_log.
          eapply RELATE_QS_MCS_LOG.
          econstructor; eauto.
          simpl.
          rewrite Hdestruct4; eauto.
          rewrite zeq_true; auto.
          rewrite Hdestruct4 in H2; eauto.
          inv H2.
          eapply QSTATE_OF_QMCSLOCKSTATE; eauto.
        + rewrite ZMap.gso; auto.
          eauto.
    Qed.

    Global Instance set_curid_init_inv: PreservesInvariants set_curid_init_spec.
    Proof.
      preserves_invariants_simpl_auto; eauto 2.
      case_eq (zeq (CPU_ID d) (Int.unsigned i)); subst.
      - intros.
        rewrite e; rewrite ZMap.gss; omega.
      - intros; rewrite ZMap.gso; auto.
    Qed.

    Global Instance proc_create_postinit_inv:
      PreservesInvariants proc_create_postinit_spec.
    Proof.
      preserves_invariants_simpl low_level_invariant high_level_invariant; eauto 2.
    Qed.

  End INV.

  Definition exec_loadex {F V} := exec_loadex1 (F := F) (V := V).

  Definition exec_storeex {F V} := exec_storeex1 (flatmem_store:= flatmem_store´) (F := F) (V := V).

  Global Instance flatmem_store_inv: FlatmemStoreInvariant (flatmem_store:= flatmem_store´).
  Proof.
    split; inversion 1; intros.
    - functional inversion H0; constructor; auto.
    - functional inversion H1; constructor; auto.
  Qed.

  Global Instance trapinfo_set_inv: TrapinfoSetInvariant.
  Proof.
    split; inversion 1; intros; constructor; auto.
  Qed.


  Lemma page_copy_correct_qslock_pool_status_gss´:
    ∀ l k c l´ z
           (HP: correct_qslock_pool_status l k c)
           (Hc: correct_qslock_status l´ (ZMap.get z k) c),
      correct_qslock_pool_status
        (ZMap.set z (MultiDef l´) l) k c.
  Proof.
    intros.
    unfold correct_qslock_pool_status in *; intros.
    destruct (zeq r z); subst.
    - rewrite ZMap.gss in ×.
      inv Hdef.
      trivial.
    - rewrite ZMap.gso in *; eauto.
  Qed.

  Lemma page_copy_correct_qslock_pool_status_gss_match:
    ∀ l k c l´ z
           (HP: correct_qslock_pool_status l k c)
           (Hc: correct_qslock_status l´ (ZMap.get z k) c),
      correct_qslock_pool_status
        (ZMap.set z (MultiDef l´) l) k c.
  Proof.
    intros. eapply page_copy_correct_qslock_pool_status_gss´; eauto.
  Qed.

  Lemma page_copy_cal_qslock_pool_status_gss:
    ∀ (l : MultiLogPool) (k : Lock) (c : Z) (l´ : MultiLog) (z : ZIndexed.t),
      cal_qslock_pool_status l k c →
      cal_qslock_status l´ (ZMap.get z k) c →
      cal_qslock_pool_status (ZMap.set z (MultiDef l´) l) k c.
  Proof.
    intros.
    unfold cal_qslock_pool_status in *; intros.
    destruct (zeq r z); subst.
    - rewrite ZMap.gss in ×. inv Hdef.
      trivial.
    - rewrite ZMap.gso in *; eauto.
  Qed.

  Global Instance page_copy_inv: PreservesInvariants mcs_page_copy´´_spec.
  Proof.
    preserves_invariants_simpl_auto.
    unfold mcs_page_copy´´_spec in *; subdestruct.
    inv H0; subst.
    - simpl; eapply valid_qslock_pool_gss´; eauto.
    - simpl. eapply page_copy_correct_qslock_pool_status_gss_match; eauto.
      eapply correct_qslock_status_shared; eauto.
    - unfold l´, cpu in *; simpl in ×.
      clear cpu l´.
      simpl. eapply page_copy_cal_qslock_pool_status_gss; eauto.
      rewrite H8.
      assert (HQS_Lock: ∃ _x3, QS_CalLock l = Some _x3).
      { Transparent QS_CalLock.
        simpl in H10.
        subdestruct.
        inv H10.
        esplit; eauto.
        Opaque QS_CalLock. }
      destruct HQS_Lock as (_x3 & HQS_Lock).
      destruct _x3 as (((((? & ?) & ?) & ?) & ?) & ?).
      exploit cal_qslock_pool_status_inv0; eauto.
      intros (_ & ?).
      rewrite H8 in H; exploit H; auto; intros.
      econstructor.
      intros.
      inv H12.
      intros.
      simpl.
      rewrite H11; auto.
    - simpl. eapply get_free_qslock_pool_gss; eauto.
      unfold l´ in ×.
      eapply QS_CalLock_append in H10.
      destruct H10 as (self_c & other_c & b´ & q´ & slow & tq & Hcal).
      unfold correct_qslock_pool_status in ×.
      exploit valid_qslock_pool_status_inv0; eauto.
      intros (_ & HT).
      exploit HT; eauto.
      intros (_ & _ & ? & _); subst.
      eapply get_free_qslock_shared; eauto.
    - simpl.
      unfold l´, cpu in *; subst.
      clear cpu l´.
      inv relate_qs_mcs_log_inv0.
      constructor; intros.
      exploit CalMCSLockLemmas.index2Z_in_lock_range; eauto; intros; simpl in ×.
      case_eq (zeq abid z); intros; subst.
      + rewrite ZMap.gss; auto.
        constructor; intros.
        exploit Hrelate_qs_mcs_log_type; eauto.
        intros.
        inv H12; [ rewrite H7 in H14; inv H14 | ].
        symmetry in H14.
        rewrite H7 in H14; inv H14.
        Transparent QS_CalLock.
        rename l0 into l.
        simpl in H10.
        subdestruct; inv H10.
        inv Hrelate_qs_mcs_log.
        eapply RELATE_QS_MCS_LOG.
        econstructor; eauto.
        simpl.
        rewrite Hdestruct; eauto.
        rewrite zeq_true; auto.
        rewrite Hdestruct in H12; eauto.
        inv H12; subst.
        constructor; eauto.
      + rewrite ZMap.gso; auto.
        eauto.
  Qed.

  Global Instance page_copy_back_inv: PreservesInvariants page_copy_back´_spec.
  Proof.
    preserves_invariants_simpl_auto.
  Qed.

  Definition mqmcslockop_fresh : compatlayer (cdata RData) :=
    ∅.

  Definition mqmcslockop_passthrough : compatlayer (cdata RData) :=
    fload ↦ gensem fload´_spec
          ⊕ fstore ↦ gensem fstore´_spec
          
          ⊕ page_copy ↦ gensem mcs_page_copy´´_spec
          ⊕ page_copy_back ↦ gensem page_copy_back´_spec

          ⊕ vmxinfo_get ↦ gensem vmxinfo_get_spec
          ⊕ set_pg ↦ gensem setPG_spec
          ⊕ set_cr3 ↦ setCR3_compatsem setCR3_spec
          ⊕ get_size ↦ gensem MMSize
          ⊕ is_usable ↦ gensem is_mm_usable_spec
          ⊕ get_mms ↦ gensem get_mm_s_spec
          ⊕ get_mml ↦ gensem get_mm_l_spec
          ⊕ get_CPU_ID ↦ gensem get_CPU_ID_spec
          ⊕ release_shared ↦ primcall_release_lock_compatsem release_shared release_shared1_mcs_spec0
          ⊕ acquire_shared ↦ primcall_acquire_shared_compatsem acquire_shared1_mcs_spec0
          ⊕ get_curid ↦ gensem get_curid_spec
          ⊕ set_curid ↦ gensem set_curid_spec
          ⊕ set_curid_init ↦ gensem set_curid_init_spec

          
          ⊕ ticket_lock_init ↦ gensem ticket_lock_init0_spec
          ⊕ pass_lock ↦ gensem pass_qslock_spec
          ⊕ wait_lock ↦ gensem wait_qslock_spec
          

          ⊕ trap_in ↦ primcall_general_compatsem trapin_spec
          ⊕ trap_out ↦ primcall_general_compatsem trapout´_spec
          ⊕ host_in ↦ primcall_general_compatsem hostin_spec
          ⊕ host_out ↦ primcall_general_compatsem hostout´_spec
          ⊕ proc_create_postinit ↦ gensem proc_create_postinit_spec
          ⊕ trap_get ↦ primcall_trap_info_get_compatsem trap_info_get_spec
          ⊕ trap_set ↦ primcall_trap_info_ret_compatsem trap_info_ret_spec
          ⊕ serial_irq_check ↦ gensem serial_irq_check_spec
          ⊕ iret ↦ gensem iret_spec
          ⊕ cli ↦ gensem cli_spec
          ⊕ sti ↦ gensem sti_spec
          ⊕ serial_irq_current ↦ gensem serial_irq_current_spec
          ⊕ ic_intr ↦ gensem ic_intr_spec
          ⊕ save_context ↦ primcall_save_context_compatsem save_context_spec
          ⊕ restore_context ↦ primcall_restore_context_compatsem restore_context_spec
          ⊕ local_irq_save ↦ gensem local_irq_save_spec
          ⊕ local_irq_restore ↦ gensem local_irq_restore_spec
          ⊕ serial_in ↦ gensem serial_in_spec