Library mcertikos.mcslock.MCSLockIntroGenFresh2


This file provide the contextual refinement proof between MBoot layer and MALInit layer

Require Import MCSLockIntroGenDef.
Require Import MCSLockIntroGenSpec.
Require Import Conventions.
Require Import XOmega.
Require Import LAsmModuleSemAux.
Require Import AuxLemma.

Definition of the refinement relation

Section Refinement.

  Section WITHMEM.

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

    Ltac pattern2_refinement_simpl:=
      pattern2_refinement_simpl´ (@relate_AbData).

    Section mcs_SWAP_TAIL_ref.

      Lemma mcs_SWAP_TAIL_spec_ref:
        compatsim (crel HDATA LDATA) (gensem mcs_SWAP_TAIL_spec) mcs_SWAP_TAIL_spec_low.
      Proof.
        compatsim_simpl (@match_AbData).
        intros Hargs0 Hasm_inv Hesp HRA Hle.
        inv Hlog.
        assert (HFB: ι b0 = Some (b0, 0)).
        { eapply stencil_find_symbol_inject´; eauto. }
        pose proof match_related as Hre.
        simpl; inv match_related.
        revert H1.
        assert (Hcpuid_range: 0 (CPU_ID d1) Int.max_unsigned).
        { generalize max_unsigned_val; intros.
          rewrite H; inv Hhigh´; omega. }
        assert (Hcpuid_eq: Int.unsigned (Int.repr ((CPU_ID d1))) = (CPU_ID d1)).
        { rewrite Int.unsigned_repr; trivial. }
        revert Hcpuid_eq.
        unfold mcs_SWAP_TAIL_spec.
        subrewrite´.
        intros ? HQ.
        set (rs2´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
                                     :: RA :: nil)
                                 (undef_regs (List.map preg_of destroyed_at_call) rs2))).
         ι, (rs2´#PC <- (rs2#RA) #EAX <- (Vint z)).
        subdestruct.
        {
          inv HQ.

          pose proof HMCSLock as HMCSLock´.
          specialize (HMCSLock _ a).
          rewrite multi_log_re in HMCSLock.
          assert (i1_vals: Int.unsigned i1 = 0 Int.unsigned i1 = 1 Int.unsigned i1 = 2 Int.unsigned i1 = 3
                           Int.unsigned i1 = 4 Int.unsigned i1 = 5 Int.unsigned i1 = 6 Int.unsigned i1 = 7).
          { omega. }
          destruct HMCSLock as (la_v & bs0_v & ne0_v & bs1_v & ne1_v & bs2_v & ne2_v & bs3_v & ne3_v &
                                bs4_v & ne4_v & bs5_v & ne5_v & bs6_v & ne6_v & bs7_v & ne7_v &
                                HL__la & HL__bs0 & HL__ne0 & HL__bs1 & HL__ne1 & HL__bs2 & HL__ne2 & HL__bs3 & HL__ne3 &
                                HL__bs4 & HL__ne4 & HL__bs5 & HL__ne5 & HL__bs6 & HL__ne6 & HL__bs7 & HL__ne7 &
                                HV__la & HV__bs0 & HV__ne0 & HV__bs1 & HV__ne1 & HV__bs2 & HV__ne2 & HV__bs3 & HV__ne3 &
                                HV__bs4 & HV__ne4 & HV__bs5 & HV__ne5 & HV__bs6 & HV__ne6 & HV__bs7 & HV__ne7 & Hm).
          assert (HST__la: m_la, Mem.store Mint32 m2 b0 (tail_pos (Int.unsigned i0)) (Vint i1) = Some m_la).
          { eapply Mem.valid_access_store; eauto. }
          destruct HST__la as (m_la & HST__la).
          assert (HST__ne: m_ne, Mem.store Mint32 m_la b0
                                                (next_pos (Int.unsigned i0) (Int.unsigned i1)) (Vint (Int.repr NULL))
                                      = Some m_ne).
          { eapply Mem.valid_access_store; eauto.
            apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial.
            destruct i1_vals as [i1_v | [i1_v | [i1_v | [i1_v | [i1_v | [i1_v | [i1_v | i1_v]]]]]]]; rewrite i1_v; trivial. }
          destruct HST__ne as (m_ne & HST__ne).
          assert (HST__bs: m_bs, Mem.store Mint32 m_ne b0
                                                (busy_pos (Int.unsigned i0) (Int.unsigned i1)) (Vint (Int.repr 1))
                                      = Some m_bs).
          { eapply Mem.valid_access_store; eauto.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial.
          destruct i1_vals as [i1_v | [i1_v | [i1_v | [i1_v | [i1_v | [i1_v | [i1_v | i1_v]]]]]]]; rewrite i1_v; trivial. }
          destruct HST__bs as (m_bs & HST__bs).
          refine_split´; repeat val_inject_inv; eauto.
          - econstructor; eauto; simpl; lift_trivial.
            × unfold atomic_mcs_SWAP_spec.
              simpl; subrewrite´.
            × eapply (extcall_args_without_data (D:= HDATAOps) d2).
              inv Hargs.
              instantiate (1:= i).
              inv H4.
              inv H3.
              inv H2.
              inv Hargs0.
              inv H5.
              inv H8.
              inv H9.
              constructor; eauto.
              econstructor; eauto.
              econstructor; eauto.
              econstructor; eauto.
          - split; eauto; pattern2_refinement_simpl;
            econstructor; eauto.
            simpl.
            econstructor; eauto; intros.
            destruct i1_vals as [i00 | [i01 | [i02 | [i03 | [i04 | [i05 | [i06 | i07]]]]]]].
            +
              rewrite i00 in ×.
              destruct (zeq (Int.unsigned i0) lock_index); subst.
              { (Vint (Int.repr 0)).
                 (Vint (Int.repr (BooltoZ true))), (Vint (Int.repr NULL)).
                 bs1_v, ne1_v.
                 bs2_v, ne2_v.
                 bs3_v, ne3_v.
                 bs4_v, ne4_v.
                 bs5_v, ne5_v.
                 bs6_v, ne6_v.
                 bs7_v, ne7_v.
                assert (i0_v: i1 = Int.repr 0).
                { rewrite <- i00; rewrite Int.repr_unsigned; reflexivity. }
                refine_split´; eauto; try (repeat (eapply Mem.store_valid_access_1; eauto));
                try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                rewrite (Mem.load_store_other _ _ _ _ _ _ HST__la); auto;
                try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail).
                - rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  erewrite Mem.load_store_same; eauto; trivial.
                  rewrite i0_v; simpl; reflexivity.
                - erewrite Mem.load_store_same; eauto; trivial.
                - rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                  try (right; left; unfold next_pos, tail_pos, busy_pos, next_pos; simpl; omega).
                  erewrite Mem.load_store_same; eauto; trivial.
                - inv Hm.
                  + rewrite Hdestruct3 in H0.
                    inv H0.
                  + rewrite ZMap.gss.
                    rewrite Hdestruct3 in H0.
                    inv H0.
                    rewrite Hcal in Hdestruct4; inv Hdestruct4.
                    assert (Hcal´: CalMCSLock (TEVENT 0 (TTICKET (SWAP_TAIL (nat_of_Z (Int.unsigned i)) true)) :: l)
                                   = Some (MCSLOCK 0 (ZMap.set 0 (true, NULL) lock_array)
                                                   (bounds ++ nat_of_Z (Int.unsigned i) :: nil))).
                    { Transparent CalMCSLock.
                      simpl.
                      rewrite Hcal; unfold CalMCSLock.NULL; reflexivity. }
                    assert (Hnc0´: ZMap.get 0 (ZMap.set 0 (true, TOTAL_CPU) lock_array) = (true, TOTAL_CPU)).
                    { rewrite ZMap.gss; reflexivity. }
                    assert (Hnc1´: ZMap.get 1 (ZMap.set 0 (true, TOTAL_CPU) lock_array) = (bs1, ne1)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc2´: ZMap.get 2 (ZMap.set 0 (true, TOTAL_CPU) lock_array) = (bs2, ne2)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc3´: ZMap.get 3 (ZMap.set 0 (true, TOTAL_CPU) lock_array) = (bs3, ne3)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc4´: ZMap.get 4 (ZMap.set 0 (true, TOTAL_CPU) lock_array) = (bs4, ne4)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc5´: ZMap.get 5 (ZMap.set 0 (true, TOTAL_CPU) lock_array) = (bs5, ne5)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc6´: ZMap.get 6 (ZMap.set 0 (true, TOTAL_CPU) lock_array) = (bs6, ne6)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc7´: ZMap.get 7 (ZMap.set 0 (true, TOTAL_CPU) lock_array) = (bs7, ne7)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    eapply MATCH_MCSLOCK_VALID with (2:= Hnc0´) (3:= Hnc1´) (4:= Hnc2´) (5:= Hnc3´) (6:= Hnc4´)
                                                                (7:= Hnc5´) (8:= Hnc6´) (9:= Hnc7´) in Hcal´; assumption. }
              { specialize (HMCSLock´ _ Hvalid).
                clear HV__la HV__bs0 HV__ne0 HV__bs1 HV__ne1 HV__bs2 HV__ne2 HV__bs3 HV__ne3 HV__bs4 HV__ne4
                      HV__bs5 HV__ne5 HV__bs6 HV__ne6 HV__bs7 HV__ne7.
                destruct HMCSLock´ as (la´ & bs0´ & ne0´ & bs1´ & ne1´ & bs2´ & ne2´ & bs3´ & ne3´ &
                                       bs4´ & ne4´ & bs5´ & ne5´ & bs6´ & ne6´ & bs7´ & ne7´ &
                                       HL__la´ & HL__bs0´ & HL__ne0´ & HL__bs1´ & HL__ne1´ & HL__bs2´ & HL__ne2´ & HL__bs3´ & HL__ne3´ &
                                       HL__bs4´ & HL__ne4´ & HL__bs5´ & HL__ne5´ & HL__bs6´ & HL__ne6´ & HL__bs7´ & HL__ne7´ &
                                       HV__la´ & HV__bs0´ & HV__ne0´ & HV__bs1´ & HV__ne1´ & HV__bs2´ & HV__ne2´ & HV__bs3´ & HV__ne3´ &
                                       HV__bs4´ & HV__ne4´ & HV__bs5´ & HV__ne5´ & HV__bs6´ & HV__ne6´ & HV__bs7´ & HV__ne7´ & HM´).
                 la´, bs0´, ne0´, bs1´, ne1´, bs2´, ne2´, bs3´, ne3´, bs4´, ne4´, bs5´, ne5´, bs6´, ne6´, bs7´, ne7´.
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__la) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                refine_split´; trivial; try (repeat (eapply Mem.store_valid_access_1; eauto)).
                rewrite ZMap.gso; auto.
                rewrite <- multi_log_re; trivial. }
            +
              rewrite i01 in ×.
              destruct (zeq (Int.unsigned i0) lock_index); subst.
              { (Vint (Int.repr 1)).
                 bs0_v, ne0_v.
                 (Vint (Int.repr (BooltoZ true))), (Vint (Int.repr NULL)).
                 bs2_v, ne2_v.
                 bs3_v, ne3_v.
                 bs4_v, ne4_v.
                 bs5_v, ne5_v.
                 bs6_v, ne6_v.
                 bs7_v, ne7_v.
                assert (i0_v: i1 = Int.repr 1).
                { rewrite <- i01; rewrite Int.repr_unsigned; reflexivity. }
                refine_split´; eauto; try (repeat (eapply Mem.store_valid_access_1; eauto));
                try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__la); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail);
                try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                     try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                     try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__la); auto;
                   try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail).
                - rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  erewrite Mem.load_store_same; eauto; trivial.
                  rewrite i0_v; simpl; reflexivity.
                - erewrite Mem.load_store_same; eauto; trivial.
                - rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  erewrite Mem.load_store_same; eauto; trivial.
                - inv Hm.
                  + rewrite Hdestruct3 in H0.
                    inv H0.
                  + rewrite ZMap.gss.
                    rewrite Hdestruct3 in H0.
                    inv H0.
                    rewrite Hcal in Hdestruct4; inv Hdestruct4.
                    assert (Hcal´: CalMCSLock (TEVENT 1 (TTICKET (SWAP_TAIL (nat_of_Z (Int.unsigned i)) true)) :: l)
                                   = Some (MCSLOCK 1 (ZMap.set 1 (true, NULL) lock_array)
                                                   (bounds ++ nat_of_Z (Int.unsigned i) :: nil))).
                    { Transparent CalMCSLock.
                      simpl.
                      rewrite Hcal; unfold CalMCSLock.NULL; reflexivity. }
                    assert (Hnc0´: ZMap.get 0 (ZMap.set 1 (true, TOTAL_CPU) lock_array) = (bs0, ne0)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc1´: ZMap.get 1 (ZMap.set 1 (true, TOTAL_CPU) lock_array) = (true, TOTAL_CPU)).
                    { rewrite ZMap.gss; reflexivity. }
                    assert (Hnc2´: ZMap.get 2 (ZMap.set 1 (true, TOTAL_CPU) lock_array) = (bs2, ne2)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc3´: ZMap.get 3 (ZMap.set 1 (true, TOTAL_CPU) lock_array) = (bs3, ne3)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc4´: ZMap.get 4 (ZMap.set 1 (true, TOTAL_CPU) lock_array) = (bs4, ne4)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc5´: ZMap.get 5 (ZMap.set 1 (true, TOTAL_CPU) lock_array) = (bs5, ne5)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc6´: ZMap.get 6 (ZMap.set 1 (true, TOTAL_CPU) lock_array) = (bs6, ne6)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc7´: ZMap.get 7 (ZMap.set 1 (true, TOTAL_CPU) lock_array) = (bs7, ne7)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    eapply MATCH_MCSLOCK_VALID with (2:= Hnc0´) (3:= Hnc1´) (4:= Hnc2´) (5:= Hnc3´) (6:= Hnc4´)
                                                                (7:= Hnc5´) (8:= Hnc6´) (9:= Hnc7´) in Hcal´; assumption. }
              { specialize (HMCSLock´ _ Hvalid).
                clear HV__la HV__bs0 HV__ne0 HV__bs1 HV__ne1 HV__bs2 HV__ne2 HV__bs3 HV__ne3 HV__bs4 HV__ne4
                      HV__bs5 HV__ne5 HV__bs6 HV__ne6 HV__bs7 HV__ne7.
                destruct HMCSLock´ as (la´ & bs0´ & ne0´ & bs1´ & ne1´ & bs2´ & ne2´ & bs3´ & ne3´ &
                                       bs4´ & ne4´ & bs5´ & ne5´ & bs6´ & ne6´ & bs7´ & ne7´ &
                                       HL__la´ & HL__bs0´ & HL__ne0´ & HL__bs1´ & HL__ne1´ & HL__bs2´ & HL__ne2´ & HL__bs3´ & HL__ne3´ &
                                       HL__bs4´ & HL__ne4´ & HL__bs5´ & HL__ne5´ & HL__bs6´ & HL__ne6´ & HL__bs7´ & HL__ne7´ &
                                       HV__la´ & HV__bs0´ & HV__ne0´ & HV__bs1´ & HV__ne1´ & HV__bs2´ & HV__ne2´ & HV__bs3´ & HV__ne3´ &
                                       HV__bs4´ & HV__ne4´ & HV__bs5´ & HV__ne5´ & HV__bs6´ & HV__ne6´ & HV__bs7´ & HV__ne7´ & HM´).
                 la´, bs0´, ne0´, bs1´, ne1´, bs2´, ne2´, bs3´, ne3´, bs4´, ne4´, bs5´, ne5´, bs6´, ne6´, bs7´, ne7´.
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__la) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                refine_split´; trivial; try (repeat (eapply Mem.store_valid_access_1; eauto)).
                rewrite ZMap.gso; auto.
                rewrite <- multi_log_re; trivial. }
            +
              rewrite i02 in ×.
              destruct (zeq (Int.unsigned i0) lock_index); subst.
              { (Vint (Int.repr 2)).
                 bs0_v, ne0_v.
                 bs1_v, ne1_v.
                 (Vint (Int.repr (BooltoZ true))), (Vint (Int.repr NULL)).
                 bs3_v, ne3_v.
                 bs4_v, ne4_v.
                 bs5_v, ne5_v.
                 bs6_v, ne6_v.
                 bs7_v, ne7_v.
                assert (i0_v: i1 = Int.repr 2).
                { rewrite <- i02; rewrite Int.repr_unsigned; reflexivity. }
                refine_split´; eauto; try (repeat (eapply Mem.store_valid_access_1; eauto));
                try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__la); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail);
                try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                     try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                     try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__la); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail).
                - rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  erewrite Mem.load_store_same; eauto; trivial.
                  rewrite i0_v; simpl; reflexivity.
                - erewrite Mem.load_store_same; eauto; trivial.
                - rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  erewrite Mem.load_store_same; eauto; trivial.
                - inv Hm.
                  + rewrite Hdestruct3 in H0.
                    inv H0.
                  + rewrite ZMap.gss.
                    rewrite Hdestruct3 in H0.
                    inv H0.
                    rewrite Hcal in Hdestruct4; inv Hdestruct4.
                    assert (Hcal´: CalMCSLock (TEVENT 2 (TTICKET (SWAP_TAIL (nat_of_Z (Int.unsigned i)) true)) :: l)
                                   = Some (MCSLOCK 2 (ZMap.set 2 (true, NULL) lock_array)
                                                   (bounds ++ nat_of_Z (Int.unsigned i) :: nil))).
                    { Transparent CalMCSLock.
                      simpl.
                      rewrite Hcal; unfold CalMCSLock.NULL; reflexivity. }
                    assert (Hnc0´: ZMap.get 0 (ZMap.set 2 (true, TOTAL_CPU) lock_array) = (bs0, ne0)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc1´: ZMap.get 1 (ZMap.set 2 (true, TOTAL_CPU) lock_array) = (bs1, ne1)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc2´: ZMap.get 2 (ZMap.set 2 (true, TOTAL_CPU) lock_array) = (true, TOTAL_CPU)).
                    { rewrite ZMap.gss; reflexivity. }
                    assert (Hnc3´: ZMap.get 3 (ZMap.set 2 (true, TOTAL_CPU) lock_array) = (bs3, ne3)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc4´: ZMap.get 4 (ZMap.set 2 (true, TOTAL_CPU) lock_array) = (bs4, ne4)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc5´: ZMap.get 5 (ZMap.set 2 (true, TOTAL_CPU) lock_array) = (bs5, ne5)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc6´: ZMap.get 6 (ZMap.set 2 (true, TOTAL_CPU) lock_array) = (bs6, ne6)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc7´: ZMap.get 7 (ZMap.set 2 (true, TOTAL_CPU) lock_array) = (bs7, ne7)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    eapply MATCH_MCSLOCK_VALID with (2:= Hnc0´) (3:= Hnc1´) (4:= Hnc2´) (5:= Hnc3´) (6:= Hnc4´)
                                                                (7:= Hnc5´) (8:= Hnc6´) (9:= Hnc7´) in Hcal´; assumption. }
              { specialize (HMCSLock´ _ Hvalid).
                clear HV__la HV__bs0 HV__ne0 HV__bs1 HV__ne1 HV__bs2 HV__ne2 HV__bs3 HV__ne3 HV__bs4 HV__ne4
                      HV__bs5 HV__ne5 HV__bs6 HV__ne6 HV__bs7 HV__ne7.
                destruct HMCSLock´ as (la´ & bs0´ & ne0´ & bs1´ & ne1´ & bs2´ & ne2´ & bs3´ & ne3´ &
                                       bs4´ & ne4´ & bs5´ & ne5´ & bs6´ & ne6´ & bs7´ & ne7´ &
                                       HL__la´ & HL__bs0´ & HL__ne0´ & HL__bs1´ & HL__ne1´ & HL__bs2´ & HL__ne2´ & HL__bs3´ & HL__ne3´ &
                                       HL__bs4´ & HL__ne4´ & HL__bs5´ & HL__ne5´ & HL__bs6´ & HL__ne6´ & HL__bs7´ & HL__ne7´ &
                                       HV__la´ & HV__bs0´ & HV__ne0´ & HV__bs1´ & HV__ne1´ & HV__bs2´ & HV__ne2´ & HV__bs3´ & HV__ne3´ &
                                       HV__bs4´ & HV__ne4´ & HV__bs5´ & HV__ne5´ & HV__bs6´ & HV__ne6´ & HV__bs7´ & HV__ne7´ & HM´).
                 la´, bs0´, ne0´, bs1´, ne1´, bs2´, ne2´, bs3´, ne3´, bs4´, ne4´, bs5´, ne5´, bs6´, ne6´, bs7´, ne7´.
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__la) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                refine_split´; trivial; try (repeat (eapply Mem.store_valid_access_1; eauto)).
                rewrite ZMap.gso; auto.
                rewrite <- multi_log_re; trivial. }
            +
              rewrite i03 in ×.
              destruct (zeq (Int.unsigned i0) lock_index); subst.
              { (Vint (Int.repr 3)).
                 bs0_v, ne0_v.
                 bs1_v, ne1_v.
                 bs2_v, ne2_v.
                 (Vint (Int.repr (BooltoZ true))), (Vint (Int.repr NULL)).
                 bs4_v, ne4_v.
                 bs5_v, ne5_v.
                 bs6_v, ne6_v.
                 bs7_v, ne7_v.
                assert (i0_v: i1 = Int.repr 3).
                { rewrite <- i03; rewrite Int.repr_unsigned; reflexivity. }
                refine_split´; eauto; try (repeat (eapply Mem.store_valid_access_1; eauto));
                try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__la); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail);
                try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                     try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                     try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__la); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail).
                - rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  erewrite Mem.load_store_same; eauto; trivial.
                  rewrite i0_v; simpl; reflexivity.
                - erewrite Mem.load_store_same; eauto; trivial.
                - rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  erewrite Mem.load_store_same; eauto; trivial.
                - inv Hm.
                  + rewrite Hdestruct3 in H0.
                    inv H0.
                  + rewrite ZMap.gss.
                    rewrite Hdestruct3 in H0.
                    inv H0.
                    rewrite Hcal in Hdestruct4; inv Hdestruct4.
                    assert (Hcal´: CalMCSLock (TEVENT 3 (TTICKET (SWAP_TAIL (nat_of_Z (Int.unsigned i)) true)) :: l)
                                   = Some (MCSLOCK 3 (ZMap.set 3 (true, NULL) lock_array)
                                                   (bounds ++ nat_of_Z (Int.unsigned i) :: nil))).
                    { Transparent CalMCSLock.
                      simpl.
                      rewrite Hcal; unfold CalMCSLock.NULL; reflexivity. }
                    assert (Hnc0´: ZMap.get 0 (ZMap.set 3 (true, TOTAL_CPU) lock_array) = (bs0, ne0)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc1´: ZMap.get 1 (ZMap.set 3 (true, TOTAL_CPU) lock_array) = (bs1, ne1)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc2´: ZMap.get 2 (ZMap.set 3 (true, TOTAL_CPU) lock_array) = (bs2, ne2)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc3´: ZMap.get 3 (ZMap.set 3 (true, TOTAL_CPU) lock_array) = (true, TOTAL_CPU)).
                    { rewrite ZMap.gss; reflexivity. }
                    assert (Hnc4´: ZMap.get 4 (ZMap.set 3 (true, TOTAL_CPU) lock_array) = (bs4, ne4)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc5´: ZMap.get 5 (ZMap.set 3 (true, TOTAL_CPU) lock_array) = (bs5, ne5)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc6´: ZMap.get 6 (ZMap.set 3 (true, TOTAL_CPU) lock_array) = (bs6, ne6)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc7´: ZMap.get 7 (ZMap.set 3 (true, TOTAL_CPU) lock_array) = (bs7, ne7)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    eapply MATCH_MCSLOCK_VALID with (2:= Hnc0´) (3:= Hnc1´) (4:= Hnc2´) (5:= Hnc3´) (6:= Hnc4´)
                                                                (7:= Hnc5´) (8:= Hnc6´) (9:= Hnc7´) in Hcal´; assumption. }
              { specialize (HMCSLock´ _ Hvalid).
                clear HV__la HV__bs0 HV__ne0 HV__bs1 HV__ne1 HV__bs2 HV__ne2 HV__bs3 HV__ne3 HV__bs4 HV__ne4
                      HV__bs5 HV__ne5 HV__bs6 HV__ne6 HV__bs7 HV__ne7.
                destruct HMCSLock´ as (la´ & bs0´ & ne0´ & bs1´ & ne1´ & bs2´ & ne2´ & bs3´ & ne3´ &
                                       bs4´ & ne4´ & bs5´ & ne5´ & bs6´ & ne6´ & bs7´ & ne7´ &
                                       HL__la´ & HL__bs0´ & HL__ne0´ & HL__bs1´ & HL__ne1´ & HL__bs2´ & HL__ne2´ & HL__bs3´ & HL__ne3´ &
                                       HL__bs4´ & HL__ne4´ & HL__bs5´ & HL__ne5´ & HL__bs6´ & HL__ne6´ & HL__bs7´ & HL__ne7´ &
                                       HV__la´ & HV__bs0´ & HV__ne0´ & HV__bs1´ & HV__ne1´ & HV__bs2´ & HV__ne2´ & HV__bs3´ & HV__ne3´ &
                                       HV__bs4´ & HV__ne4´ & HV__bs5´ & HV__ne5´ & HV__bs6´ & HV__ne6´ & HV__bs7´ & HV__ne7´ & HM´).
                 la´, bs0´, ne0´, bs1´, ne1´, bs2´, ne2´, bs3´, ne3´, bs4´, ne4´, bs5´, ne5´, bs6´, ne6´, bs7´, ne7´.
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__la) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                refine_split´; trivial; try (repeat (eapply Mem.store_valid_access_1; eauto)).
                rewrite ZMap.gso; auto.
                rewrite <- multi_log_re; trivial. }
            +
              rewrite i04 in ×.
              destruct (zeq (Int.unsigned i0) lock_index); subst.
              { (Vint (Int.repr 4)).
                 bs0_v, ne0_v.
                 bs1_v, ne1_v.
                 bs2_v, ne2_v.
                 bs3_v, ne3_v.
                 (Vint (Int.repr (BooltoZ true))), (Vint (Int.repr NULL)).
                 bs5_v, ne5_v.
                 bs6_v, ne6_v.
                 bs7_v, ne7_v.
                assert (i0_v: i1 = Int.repr 4).
                { rewrite <- i04; rewrite Int.repr_unsigned; reflexivity. }
                refine_split´; eauto; try (repeat (eapply Mem.store_valid_access_1; eauto));
                try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__la); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail);
                try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                     try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                     try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__la); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail).
                - rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  erewrite Mem.load_store_same; eauto; trivial.
                  rewrite i0_v; simpl; reflexivity.
                - erewrite Mem.load_store_same; eauto; trivial.
                - rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  erewrite Mem.load_store_same; eauto; trivial.
                - inv Hm.
                  + rewrite Hdestruct3 in H0.
                    inv H0.
                  + rewrite ZMap.gss.
                    rewrite Hdestruct3 in H0.
                    inv H0.
                    rewrite Hcal in Hdestruct4; inv Hdestruct4.
                    assert (Hcal´: CalMCSLock (TEVENT 4 (TTICKET (SWAP_TAIL (nat_of_Z (Int.unsigned i)) true)) :: l)
                                   = Some (MCSLOCK 4 (ZMap.set 4 (true, NULL) lock_array)
                                                   (bounds ++ nat_of_Z (Int.unsigned i) :: nil))).
                    { Transparent CalMCSLock.
                      simpl.
                      rewrite Hcal; unfold CalMCSLock.NULL; reflexivity. }
                    assert (Hnc0´: ZMap.get 0 (ZMap.set 4 (true, TOTAL_CPU) lock_array) = (bs0, ne0)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc1´: ZMap.get 1 (ZMap.set 4 (true, TOTAL_CPU) lock_array) = (bs1, ne1)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc2´: ZMap.get 2 (ZMap.set 4 (true, TOTAL_CPU) lock_array) = (bs2, ne2)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc3´: ZMap.get 3 (ZMap.set 4 (true, TOTAL_CPU) lock_array) = (bs3, ne3)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc4´: ZMap.get 4 (ZMap.set 4 (true, TOTAL_CPU) lock_array) = (true, TOTAL_CPU)).
                    { rewrite ZMap.gss; reflexivity. }
                    assert (Hnc5´: ZMap.get 5 (ZMap.set 4 (true, TOTAL_CPU) lock_array) = (bs5, ne5)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc6´: ZMap.get 6 (ZMap.set 4 (true, TOTAL_CPU) lock_array) = (bs6, ne6)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc7´: ZMap.get 7 (ZMap.set 4 (true, TOTAL_CPU) lock_array) = (bs7, ne7)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    eapply MATCH_MCSLOCK_VALID with (2:= Hnc0´) (3:= Hnc1´) (4:= Hnc2´) (5:= Hnc3´) (6:= Hnc4´)
                                                                (7:= Hnc5´) (8:= Hnc6´) (9:= Hnc7´) in Hcal´; assumption. }
              { specialize (HMCSLock´ _ Hvalid).
                clear HV__la HV__bs0 HV__ne0 HV__bs1 HV__ne1 HV__bs2 HV__ne2 HV__bs3 HV__ne3 HV__bs4 HV__ne4
                      HV__bs5 HV__ne5 HV__bs6 HV__ne6 HV__bs7 HV__ne7.
                destruct HMCSLock´ as (la´ & bs0´ & ne0´ & bs1´ & ne1´ & bs2´ & ne2´ & bs3´ & ne3´ &
                                       bs4´ & ne4´ & bs5´ & ne5´ & bs6´ & ne6´ & bs7´ & ne7´ &
                                       HL__la´ & HL__bs0´ & HL__ne0´ & HL__bs1´ & HL__ne1´ & HL__bs2´ & HL__ne2´ & HL__bs3´ & HL__ne3´ &
                                       HL__bs4´ & HL__ne4´ & HL__bs5´ & HL__ne5´ & HL__bs6´ & HL__ne6´ & HL__bs7´ & HL__ne7´ &
                                       HV__la´ & HV__bs0´ & HV__ne0´ & HV__bs1´ & HV__ne1´ & HV__bs2´ & HV__ne2´ & HV__bs3´ & HV__ne3´ &
                                       HV__bs4´ & HV__ne4´ & HV__bs5´ & HV__ne5´ & HV__bs6´ & HV__ne6´ & HV__bs7´ & HV__ne7´ & HM´).
                 la´, bs0´, ne0´, bs1´, ne1´, bs2´, ne2´, bs3´, ne3´, bs4´, ne4´, bs5´, ne5´, bs6´, ne6´, bs7´, ne7´.
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__la) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                refine_split´; trivial; try (repeat (eapply Mem.store_valid_access_1; eauto)).
                rewrite ZMap.gso; auto.
                rewrite <- multi_log_re; trivial. }
            +
              rewrite i05 in ×.
              destruct (zeq (Int.unsigned i0) lock_index); subst.
              { (Vint (Int.repr 5)).
                 bs0_v, ne0_v.
                 bs1_v, ne1_v.
                 bs2_v, ne2_v.
                 bs3_v, ne3_v.
                 bs4_v, ne4_v.
                 (Vint (Int.repr (BooltoZ true))), (Vint (Int.repr NULL)).
                 bs6_v, ne6_v.
                 bs7_v, ne7_v.
                assert (i0_v: i1 = Int.repr 5).
                { rewrite <- i05; rewrite Int.repr_unsigned; reflexivity. }
                refine_split´; eauto; try (repeat (eapply Mem.store_valid_access_1; eauto));
                try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__la); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail);
                try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                     try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                     try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__la); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail).
                - rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  erewrite Mem.load_store_same; eauto; trivial.
                  rewrite i0_v; simpl; reflexivity.
                - erewrite Mem.load_store_same; eauto; trivial.
                - rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  erewrite Mem.load_store_same; eauto; trivial.
                - inv Hm.
                  + rewrite Hdestruct3 in H0.
                    inv H0.
                  + rewrite ZMap.gss.
                    rewrite Hdestruct3 in H0.
                    inv H0.
                    rewrite Hcal in Hdestruct4; inv Hdestruct4.
                    assert (Hcal´: CalMCSLock (TEVENT 5 (TTICKET (SWAP_TAIL (nat_of_Z (Int.unsigned i)) true)) :: l)
                                   = Some (MCSLOCK 5 (ZMap.set 5 (true, NULL) lock_array)
                                                   (bounds ++ nat_of_Z (Int.unsigned i) :: nil))).
                    { Transparent CalMCSLock.
                      simpl.
                      rewrite Hcal; unfold CalMCSLock.NULL; reflexivity. }
                    assert (Hnc0´: ZMap.get 0 (ZMap.set 5 (true, TOTAL_CPU) lock_array) = (bs0, ne0)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc1´: ZMap.get 1 (ZMap.set 5 (true, TOTAL_CPU) lock_array) = (bs1, ne1)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc2´: ZMap.get 2 (ZMap.set 5 (true, TOTAL_CPU) lock_array) = (bs2, ne2)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc3´: ZMap.get 3 (ZMap.set 5 (true, TOTAL_CPU) lock_array) = (bs3, ne3)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc4´: ZMap.get 4 (ZMap.set 5 (true, TOTAL_CPU) lock_array) = (bs4, ne4)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc5´: ZMap.get 5 (ZMap.set 5 (true, TOTAL_CPU) lock_array) = (true, TOTAL_CPU)).
                    { rewrite ZMap.gss; reflexivity. }
                    assert (Hnc6´: ZMap.get 6 (ZMap.set 5 (true, TOTAL_CPU) lock_array) = (bs6, ne6)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc7´: ZMap.get 7 (ZMap.set 5 (true, TOTAL_CPU) lock_array) = (bs7, ne7)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    eapply MATCH_MCSLOCK_VALID with (2:= Hnc0´) (3:= Hnc1´) (4:= Hnc2´) (5:= Hnc3´) (6:= Hnc4´)
                                                                (7:= Hnc5´) (8:= Hnc6´) (9:= Hnc7´) in Hcal´; assumption. }
              { specialize (HMCSLock´ _ Hvalid).
                clear HV__la HV__bs0 HV__ne0 HV__bs1 HV__ne1 HV__bs2 HV__ne2 HV__bs3 HV__ne3 HV__bs4 HV__ne4
                      HV__bs5 HV__ne5 HV__bs6 HV__ne6 HV__bs7 HV__ne7.
                destruct HMCSLock´ as (la´ & bs0´ & ne0´ & bs1´ & ne1´ & bs2´ & ne2´ & bs3´ & ne3´ &
                                       bs4´ & ne4´ & bs5´ & ne5´ & bs6´ & ne6´ & bs7´ & ne7´ &
                                       HL__la´ & HL__bs0´ & HL__ne0´ & HL__bs1´ & HL__ne1´ & HL__bs2´ & HL__ne2´ & HL__bs3´ & HL__ne3´ &
                                       HL__bs4´ & HL__ne4´ & HL__bs5´ & HL__ne5´ & HL__bs6´ & HL__ne6´ & HL__bs7´ & HL__ne7´ &
                                       HV__la´ & HV__bs0´ & HV__ne0´ & HV__bs1´ & HV__ne1´ & HV__bs2´ & HV__ne2´ & HV__bs3´ & HV__ne3´ &
                                       HV__bs4´ & HV__ne4´ & HV__bs5´ & HV__ne5´ & HV__bs6´ & HV__ne6´ & HV__bs7´ & HV__ne7´ & HM´).
                 la´, bs0´, ne0´, bs1´, ne1´, bs2´, ne2´, bs3´, ne3´, bs4´, ne4´, bs5´, ne5´, bs6´, ne6´, bs7´, ne7´.
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__la) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                refine_split´; trivial; try (repeat (eapply Mem.store_valid_access_1; eauto)).
                rewrite ZMap.gso; auto.
                rewrite <- multi_log_re; trivial. }
            +
              rewrite i06 in ×.
              destruct (zeq (Int.unsigned i0) lock_index); subst.
              { (Vint (Int.repr 6)).
                 bs0_v, ne0_v.
                 bs1_v, ne1_v.
                 bs2_v, ne2_v.
                 bs3_v, ne3_v.
                 bs4_v, ne4_v.
                 bs5_v, ne5_v.
                 (Vint (Int.repr (BooltoZ true))), (Vint (Int.repr NULL)).
                 bs7_v, ne7_v.
                assert (i0_v: i1 = Int.repr 6).
                { rewrite <- i06; rewrite Int.repr_unsigned; reflexivity. }
                refine_split´; eauto; try (repeat (eapply Mem.store_valid_access_1; eauto));
                try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__la); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail);
                try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                     try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                     try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__la); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail).
                - rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  erewrite Mem.load_store_same; eauto; trivial.
                  rewrite i0_v; simpl; reflexivity.
                - erewrite Mem.load_store_same; eauto; trivial.
                - rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  erewrite Mem.load_store_same; eauto; trivial.
                - inv Hm.
                  + rewrite Hdestruct3 in H0.
                    inv H0.
                  + rewrite ZMap.gss.
                    rewrite Hdestruct3 in H0.
                    inv H0.
                    rewrite Hcal in Hdestruct4; inv Hdestruct4.
                    assert (Hcal´: CalMCSLock (TEVENT 6 (TTICKET (SWAP_TAIL (nat_of_Z (Int.unsigned i)) true)) :: l)
                                   = Some (MCSLOCK 6 (ZMap.set 6 (true, NULL) lock_array)
                                                   (bounds ++ nat_of_Z (Int.unsigned i) :: nil))).
                    { Transparent CalMCSLock.
                      simpl.
                      rewrite Hcal; unfold CalMCSLock.NULL; reflexivity. }
                    assert (Hnc0´: ZMap.get 0 (ZMap.set 6 (true, TOTAL_CPU) lock_array) = (bs0, ne0)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc1´: ZMap.get 1 (ZMap.set 6 (true, TOTAL_CPU) lock_array) = (bs1, ne1)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc2´: ZMap.get 2 (ZMap.set 6 (true, TOTAL_CPU) lock_array) = (bs2, ne2)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc3´: ZMap.get 3 (ZMap.set 6 (true, TOTAL_CPU) lock_array) = (bs3, ne3)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc4´: ZMap.get 4 (ZMap.set 6 (true, TOTAL_CPU) lock_array) = (bs4, ne4)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc5´: ZMap.get 5 (ZMap.set 6 (true, TOTAL_CPU) lock_array) = (bs5, ne5)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc6´: ZMap.get 6 (ZMap.set 6 (true, TOTAL_CPU) lock_array) = (true, TOTAL_CPU)).
                    { rewrite ZMap.gss; reflexivity. }
                    assert (Hnc7´: ZMap.get 7 (ZMap.set 6 (true, TOTAL_CPU) lock_array) = (bs7, ne7)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    eapply MATCH_MCSLOCK_VALID with (2:= Hnc0´) (3:= Hnc1´) (4:= Hnc2´) (5:= Hnc3´) (6:= Hnc4´)
                                                                (7:= Hnc5´) (8:= Hnc6´) (9:= Hnc7´) in Hcal´; assumption. }
              { specialize (HMCSLock´ _ Hvalid).
                clear HV__la HV__bs0 HV__ne0 HV__bs1 HV__ne1 HV__bs2 HV__ne2 HV__bs3 HV__ne3 HV__bs4 HV__ne4
                      HV__bs5 HV__ne5 HV__bs6 HV__ne6 HV__bs7 HV__ne7.
                destruct HMCSLock´ as (la´ & bs0´ & ne0´ & bs1´ & ne1´ & bs2´ & ne2´ & bs3´ & ne3´ &
                                       bs4´ & ne4´ & bs5´ & ne5´ & bs6´ & ne6´ & bs7´ & ne7´ &
                                       HL__la´ & HL__bs0´ & HL__ne0´ & HL__bs1´ & HL__ne1´ & HL__bs2´ & HL__ne2´ & HL__bs3´ & HL__ne3´ &
                                       HL__bs4´ & HL__ne4´ & HL__bs5´ & HL__ne5´ & HL__bs6´ & HL__ne6´ & HL__bs7´ & HL__ne7´ &
                                       HV__la´ & HV__bs0´ & HV__ne0´ & HV__bs1´ & HV__ne1´ & HV__bs2´ & HV__ne2´ & HV__bs3´ & HV__ne3´ &
                                       HV__bs4´ & HV__ne4´ & HV__bs5´ & HV__ne5´ & HV__bs6´ & HV__ne6´ & HV__bs7´ & HV__ne7´ & HM´).
                 la´, bs0´, ne0´, bs1´, ne1´, bs2´, ne2´, bs3´, ne3´, bs4´, ne4´, bs5´, ne5´, bs6´, ne6´, bs7´, ne7´.
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__la) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                refine_split´; trivial; try (repeat (eapply Mem.store_valid_access_1; eauto)).
                rewrite ZMap.gso; auto.
                rewrite <- multi_log_re; trivial. }
            +
              rewrite i07 in ×.
              destruct (zeq (Int.unsigned i0) lock_index); subst.
              { (Vint (Int.repr 7)).
                 bs0_v, ne0_v.
                 bs1_v, ne1_v.
                 bs2_v, ne2_v.
                 bs3_v, ne3_v.
                 bs4_v, ne4_v.
                 bs5_v, ne5_v.
                 bs6_v, ne6_v.
                 (Vint (Int.repr (BooltoZ true))), (Vint (Int.repr NULL)).
                assert (i0_v: i1 = Int.repr 7).
                { rewrite <- i07; rewrite Int.repr_unsigned; reflexivity. }
                refine_split´; eauto; try (repeat (eapply Mem.store_valid_access_1; eauto));
                try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                     try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                     try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__la); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail).
                - rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  erewrite Mem.load_store_same; eauto; trivial.
                  rewrite i0_v; simpl; reflexivity.
                - erewrite Mem.load_store_same; eauto; trivial.
                - rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  erewrite Mem.load_store_same; eauto; trivial.
                - inv Hm.
                  + rewrite Hdestruct3 in H0.
                    inv H0.
                  + rewrite ZMap.gss.
                    rewrite Hdestruct3 in H0.
                    inv H0.
                    rewrite Hcal in Hdestruct4; inv Hdestruct4.
                    assert (Hcal´: CalMCSLock (TEVENT 7 (TTICKET (SWAP_TAIL (nat_of_Z (Int.unsigned i)) true)) :: l)
                                   = Some (MCSLOCK 7 (ZMap.set 7 (true, NULL) lock_array)
                                                   (bounds ++ nat_of_Z (Int.unsigned i) :: nil))).
                    { Transparent CalMCSLock.
                      simpl.
                      rewrite Hcal; unfold CalMCSLock.NULL; reflexivity. }
                    assert (Hnc0´: ZMap.get 0 (ZMap.set 7 (true, TOTAL_CPU) lock_array) = (bs0, ne0)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc1´: ZMap.get 1 (ZMap.set 7 (true, TOTAL_CPU) lock_array) = (bs1, ne1)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc2´: ZMap.get 2 (ZMap.set 7 (true, TOTAL_CPU) lock_array) = (bs2, ne2)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc3´: ZMap.get 3 (ZMap.set 7 (true, TOTAL_CPU) lock_array) = (bs3, ne3)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc4´: ZMap.get 4 (ZMap.set 7 (true, TOTAL_CPU) lock_array) = (bs4, ne4)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc5´: ZMap.get 5 (ZMap.set 7 (true, TOTAL_CPU) lock_array) = (bs5, ne5)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc6´: ZMap.get 6 (ZMap.set 7 (true, TOTAL_CPU) lock_array) = (bs6, ne6)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc7´: ZMap.get 7 (ZMap.set 7 (true, TOTAL_CPU) lock_array) = (true, TOTAL_CPU)).
                    { rewrite ZMap.gss; reflexivity. }
                    eapply MATCH_MCSLOCK_VALID with (2:= Hnc0´) (3:= Hnc1´) (4:= Hnc2´) (5:= Hnc3´) (6:= Hnc4´)
                                                                (7:= Hnc5´) (8:= Hnc6´) (9:= Hnc7´) in Hcal´; assumption. }
              { specialize (HMCSLock´ _ Hvalid).
                clear HV__la HV__bs0 HV__ne0 HV__bs1 HV__ne1 HV__bs2 HV__ne2 HV__bs3 HV__ne3 HV__bs4 HV__ne4
                      HV__bs5 HV__ne5 HV__bs6 HV__ne6 HV__bs7 HV__ne7.
                destruct HMCSLock´ as (la´ & bs0´ & ne0´ & bs1´ & ne1´ & bs2´ & ne2´ & bs3´ & ne3´ &
                                       bs4´ & ne4´ & bs5´ & ne5´ & bs6´ & ne6´ & bs7´ & ne7´ &
                                       HL__la´ & HL__bs0´ & HL__ne0´ & HL__bs1´ & HL__ne1´ & HL__bs2´ & HL__ne2´ & HL__bs3´ & HL__ne3´ &
                                       HL__bs4´ & HL__ne4´ & HL__bs5´ & HL__ne5´ & HL__bs6´ & HL__ne6´ & HL__bs7´ & HL__ne7´ &
                                       HV__la´ & HV__bs0´ & HV__ne0´ & HV__bs1´ & HV__ne1´ & HV__bs2´ & HV__ne2´ & HV__bs3´ & HV__ne3´ &
                                       HV__bs4´ & HV__ne4´ & HV__bs5´ & HV__ne5´ & HV__bs6´ & HV__ne6´ & HV__bs7´ & HV__ne7´ & HM´).
                 la´, bs0´, ne0´, bs1´, ne1´, bs2´, ne2´, bs3´, ne3´, bs4´, ne4´, bs5´, ne5´, bs6´, ne6´, bs7´, ne7´.
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__la) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
              rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
              rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                      HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                      HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
              refine_split´; trivial; try (repeat (eapply Mem.store_valid_access_1; eauto)).
              rewrite ZMap.gso; auto.
              rewrite <- multi_log_re; trivial. }
        - repeat simpl_Pregmap; eauto.
        - intros. inv Hasm_inv.
          inv inv_inject_neutral. subst rs2´.
          destruct r; simpl;
          repeat simpl_Pregmap; eauto;
          (elim H; eauto 20). }

        {
          inv HQ.
          pose proof HMCSLock as HMCSLock´.
          specialize (HMCSLock _ a).
          rewrite multi_log_re in HMCSLock.
          assert (i1_vals: Int.unsigned i1 = 0 Int.unsigned i1 = 1 Int.unsigned i1 = 2 Int.unsigned i1 = 3
                           Int.unsigned i1 = 4 Int.unsigned i1 = 5 Int.unsigned i1 = 6 Int.unsigned i1 = 7).
          { omega. }
          destruct HMCSLock as (la_v & bs0_v & ne0_v & bs1_v & ne1_v & bs2_v & ne2_v & bs3_v & ne3_v &
                                bs4_v & ne4_v & bs5_v & ne5_v & bs6_v & ne6_v & bs7_v & ne7_v &
                                HL__la & HL__bs0 & HL__ne0 & HL__bs1 & HL__ne1 & HL__bs2 & HL__ne2 & HL__bs3 & HL__ne3 &
                                HL__bs4 & HL__ne4 & HL__bs5 & HL__ne5 & HL__bs6 & HL__ne6 & HL__bs7 & HL__ne7 &
                                HV__la & HV__bs0 & HV__ne0 & HV__bs1 & HV__ne1 & HV__bs2 & HV__ne2 & HV__bs3 & HV__ne3 &
                                HV__bs4 & HV__ne4 & HV__bs5 & HV__ne5 & HV__bs6 & HV__ne6 & HV__bs7 & HV__ne7 & Hm).
          assert (HST__la: m_la, Mem.store Mint32 m2 b0 (tail_pos (Int.unsigned i0)) (Vint i1) = Some m_la).
          { eapply Mem.valid_access_store; eauto. }
          destruct HST__la as (m_la & HST__la).
          assert (HST__ne: m_ne, Mem.store Mint32 m_la b0
                                                (next_pos (Int.unsigned i0) (Int.unsigned i1)) (Vint (Int.repr NULL))
                                      = Some m_ne).
          { eapply Mem.valid_access_store; eauto.
            apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial.
            destruct i1_vals as [i1_v | [i1_v | [i1_v | [i1_v | [i1_v | [i1_v | [i1_v | i1_v]]]]]]]; rewrite i1_v; trivial. }
          destruct HST__ne as (m_ne & HST__ne).
          assert (HST__bs: m_bs, Mem.store Mint32 m_ne b0
                                                (busy_pos (Int.unsigned i0) (Int.unsigned i1)) (Vint (Int.repr 1))
                                      = Some m_bs).
          { eapply Mem.valid_access_store; eauto.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial.
          destruct i1_vals as [i1_v | [i1_v | [i1_v | [i1_v | [i1_v | [i1_v | [i1_v | i1_v]]]]]]]; rewrite i1_v; trivial. }
          destruct HST__bs as (m_bs & HST__bs).
          refine_split´; repeat val_inject_inv; eauto.
          - econstructor; eauto; simpl; lift_trivial.
            × unfold atomic_mcs_SWAP_spec.
              simpl; subrewrite´.
            × eapply (extcall_args_without_data (D:= HDATAOps) d2).
              inv Hargs.
              instantiate (1:= i).
              inv H3.
              inv H2.
              inv H1.
              inv Hargs0.
              inv H4.
              inv H7.
              inv H8.
              constructor; eauto.
              econstructor; eauto.
              econstructor; eauto.
              econstructor; eauto.
          - split; eauto; pattern2_refinement_simpl;
            econstructor; eauto.
            simpl.
            econstructor; eauto; intros.
            destruct i1_vals as [i00 | [i01 | [i02 | [i03 | [i04 | [i05 | [i06 | i07]]]]]]].
            +
              rewrite i00 in ×.
              destruct (zeq (Int.unsigned i0) lock_index); subst.
              { (Vint (Int.repr 0)).
                 (Vint (Int.repr (BooltoZ true))), (Vint (Int.repr NULL)).
                 bs1_v, ne1_v.
                 bs2_v, ne2_v.
                 bs3_v, ne3_v.
                 bs4_v, ne4_v.
                 bs5_v, ne5_v.
                 bs6_v, ne6_v.
                 bs7_v, ne7_v.
                assert (i0_v: i1 = Int.repr 0).
                { rewrite <- i00; rewrite Int.repr_unsigned; reflexivity. }
                refine_split´; eauto; try (repeat (eapply Mem.store_valid_access_1; eauto));
                try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                rewrite (Mem.load_store_other _ _ _ _ _ _ HST__la); auto;
                try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail).
                - rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  erewrite Mem.load_store_same; eauto; trivial.
                  rewrite i0_v; simpl; reflexivity.
                - erewrite Mem.load_store_same; eauto; trivial.
                - rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  erewrite Mem.load_store_same; eauto; trivial.
                - inv Hm.
                  + rewrite Hdestruct3 in H0.
                    inv H0.
                  + rewrite ZMap.gss.
                    rewrite Hdestruct3 in H0.
                    inv H0.
                    rewrite Hcal in Hdestruct4; inv Hdestruct4.
                    assert (Hcal´: CalMCSLock (TEVENT 0 (TTICKET (SWAP_TAIL (nat_of_Z (Int.unsigned i)) false)) :: l)
                                   = Some (MCSLOCK 0 (ZMap.set 0 (true, NULL) lock_array)
                                                   (bounds ++ nat_of_Z (Int.unsigned i) :: nil))).
                    { Transparent CalMCSLock.
                      simpl.
                      rewrite Hcal; unfold CalMCSLock.NULL; reflexivity. }
                    assert (Hnc0´: ZMap.get 0 (ZMap.set 0 (true, TOTAL_CPU) lock_array) = (true, TOTAL_CPU)).
                    { rewrite ZMap.gss; reflexivity. }
                    assert (Hnc1´: ZMap.get 1 (ZMap.set 0 (true, TOTAL_CPU) lock_array) = (bs1, ne1)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc2´: ZMap.get 2 (ZMap.set 0 (true, TOTAL_CPU) lock_array) = (bs2, ne2)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc3´: ZMap.get 3 (ZMap.set 0 (true, TOTAL_CPU) lock_array) = (bs3, ne3)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc4´: ZMap.get 4 (ZMap.set 0 (true, TOTAL_CPU) lock_array) = (bs4, ne4)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc5´: ZMap.get 5 (ZMap.set 0 (true, TOTAL_CPU) lock_array) = (bs5, ne5)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc6´: ZMap.get 6 (ZMap.set 0 (true, TOTAL_CPU) lock_array) = (bs6, ne6)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc7´: ZMap.get 7 (ZMap.set 0 (true, TOTAL_CPU) lock_array) = (bs7, ne7)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    eapply MATCH_MCSLOCK_VALID with (2:= Hnc0´) (3:= Hnc1´) (4:= Hnc2´) (5:= Hnc3´) (6:= Hnc4´)
                                                                (7:= Hnc5´) (8:= Hnc6´) (9:= Hnc7´) in Hcal´; assumption. }
              { specialize (HMCSLock´ _ Hvalid).
                clear HV__la HV__bs0 HV__ne0 HV__bs1 HV__ne1 HV__bs2 HV__ne2 HV__bs3 HV__ne3 HV__bs4 HV__ne4
                      HV__bs5 HV__ne5 HV__bs6 HV__ne6 HV__bs7 HV__ne7.
                destruct HMCSLock´ as (la´ & bs0´ & ne0´ & bs1´ & ne1´ & bs2´ & ne2´ & bs3´ & ne3´ &
                                       bs4´ & ne4´ & bs5´ & ne5´ & bs6´ & ne6´ & bs7´ & ne7´ &
                                       HL__la´ & HL__bs0´ & HL__ne0´ & HL__bs1´ & HL__ne1´ & HL__bs2´ & HL__ne2´ & HL__bs3´ & HL__ne3´ &
                                       HL__bs4´ & HL__ne4´ & HL__bs5´ & HL__ne5´ & HL__bs6´ & HL__ne6´ & HL__bs7´ & HL__ne7´ &
                                       HV__la´ & HV__bs0´ & HV__ne0´ & HV__bs1´ & HV__ne1´ & HV__bs2´ & HV__ne2´ & HV__bs3´ & HV__ne3´ &
                                       HV__bs4´ & HV__ne4´ & HV__bs5´ & HV__ne5´ & HV__bs6´ & HV__ne6´ & HV__bs7´ & HV__ne7´ & HM´).
                 la´, bs0´, ne0´, bs1´, ne1´, bs2´, ne2´, bs3´, ne3´, bs4´, ne4´, bs5´, ne5´, bs6´, ne6´, bs7´, ne7´.
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__la) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                refine_split´; trivial; try (repeat (eapply Mem.store_valid_access_1; eauto)).
                rewrite ZMap.gso; auto.
                rewrite <- multi_log_re; trivial. }
            +
              rewrite i01 in ×.
              destruct (zeq (Int.unsigned i0) lock_index); subst.
              { (Vint (Int.repr 1)).
                 bs0_v, ne0_v.
                 (Vint (Int.repr (BooltoZ true))), (Vint (Int.repr NULL)).
                 bs2_v, ne2_v.
                 bs3_v, ne3_v.
                 bs4_v, ne4_v.
                 bs5_v, ne5_v.
                 bs6_v, ne6_v.
                 bs7_v, ne7_v.
                assert (i0_v: i1 = Int.repr 1).
                { rewrite <- i01; rewrite Int.repr_unsigned; reflexivity. }
                refine_split´; eauto; try (repeat (eapply Mem.store_valid_access_1; eauto));
                try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__la); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail);
                try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                     try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                     try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__la); auto;
                   try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail).
                - rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  erewrite Mem.load_store_same; eauto; trivial.
                  rewrite i0_v; simpl; reflexivity.
                - erewrite Mem.load_store_same; eauto; trivial.
                - rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  erewrite Mem.load_store_same; eauto; trivial.
                - inv Hm.
                  + rewrite Hdestruct3 in H0.
                    inv H0.
                  + rewrite ZMap.gss.
                    rewrite Hdestruct3 in H0.
                    inv H0.
                    rewrite Hcal in Hdestruct4; inv Hdestruct4.
                    assert (Hcal´: CalMCSLock (TEVENT 1 (TTICKET (SWAP_TAIL (nat_of_Z (Int.unsigned i)) false)) :: l)
                                   = Some (MCSLOCK 1 (ZMap.set 1 (true, NULL) lock_array)
                                                   (bounds ++ nat_of_Z (Int.unsigned i) :: nil))).
                    { Transparent CalMCSLock.
                      simpl.
                      rewrite Hcal; unfold CalMCSLock.NULL; reflexivity. }
                    assert (Hnc0´: ZMap.get 0 (ZMap.set 1 (true, TOTAL_CPU) lock_array) = (bs0, ne0)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc1´: ZMap.get 1 (ZMap.set 1 (true, TOTAL_CPU) lock_array) = (true, TOTAL_CPU)).
                    { rewrite ZMap.gss; reflexivity. }
                    assert (Hnc2´: ZMap.get 2 (ZMap.set 1 (true, TOTAL_CPU) lock_array) = (bs2, ne2)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc3´: ZMap.get 3 (ZMap.set 1 (true, TOTAL_CPU) lock_array) = (bs3, ne3)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc4´: ZMap.get 4 (ZMap.set 1 (true, TOTAL_CPU) lock_array) = (bs4, ne4)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc5´: ZMap.get 5 (ZMap.set 1 (true, TOTAL_CPU) lock_array) = (bs5, ne5)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc6´: ZMap.get 6 (ZMap.set 1 (true, TOTAL_CPU) lock_array) = (bs6, ne6)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc7´: ZMap.get 7 (ZMap.set 1 (true, TOTAL_CPU) lock_array) = (bs7, ne7)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    eapply MATCH_MCSLOCK_VALID with (2:= Hnc0´) (3:= Hnc1´) (4:= Hnc2´) (5:= Hnc3´) (6:= Hnc4´)
                                                                (7:= Hnc5´) (8:= Hnc6´) (9:= Hnc7´) in Hcal´; assumption. }
              { specialize (HMCSLock´ _ Hvalid).
                clear HV__la HV__bs0 HV__ne0 HV__bs1 HV__ne1 HV__bs2 HV__ne2 HV__bs3 HV__ne3 HV__bs4 HV__ne4
                      HV__bs5 HV__ne5 HV__bs6 HV__ne6 HV__bs7 HV__ne7.
                destruct HMCSLock´ as (la´ & bs0´ & ne0´ & bs1´ & ne1´ & bs2´ & ne2´ & bs3´ & ne3´ &
                                       bs4´ & ne4´ & bs5´ & ne5´ & bs6´ & ne6´ & bs7´ & ne7´ &
                                       HL__la´ & HL__bs0´ & HL__ne0´ & HL__bs1´ & HL__ne1´ & HL__bs2´ & HL__ne2´ & HL__bs3´ & HL__ne3´ &
                                       HL__bs4´ & HL__ne4´ & HL__bs5´ & HL__ne5´ & HL__bs6´ & HL__ne6´ & HL__bs7´ & HL__ne7´ &
                                       HV__la´ & HV__bs0´ & HV__ne0´ & HV__bs1´ & HV__ne1´ & HV__bs2´ & HV__ne2´ & HV__bs3´ & HV__ne3´ &
                                       HV__bs4´ & HV__ne4´ & HV__bs5´ & HV__ne5´ & HV__bs6´ & HV__ne6´ & HV__bs7´ & HV__ne7´ & HM´).
                 la´, bs0´, ne0´, bs1´, ne1´, bs2´, ne2´, bs3´, ne3´, bs4´, ne4´, bs5´, ne5´, bs6´, ne6´, bs7´, ne7´.
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__la) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                refine_split´; trivial; try (repeat (eapply Mem.store_valid_access_1; eauto)).
                rewrite ZMap.gso; auto.
                rewrite <- multi_log_re; trivial. }
            +
              rewrite i02 in ×.
              destruct (zeq (Int.unsigned i0) lock_index); subst.
              { (Vint (Int.repr 2)).
                 bs0_v, ne0_v.
                 bs1_v, ne1_v.
                 (Vint (Int.repr (BooltoZ true))), (Vint (Int.repr NULL)).
                 bs3_v, ne3_v.
                 bs4_v, ne4_v.
                 bs5_v, ne5_v.
                 bs6_v, ne6_v.
                 bs7_v, ne7_v.
                assert (i0_v: i1 = Int.repr 2).
                { rewrite <- i02; rewrite Int.repr_unsigned; reflexivity. }
                refine_split´; eauto; try (repeat (eapply Mem.store_valid_access_1; eauto));
                try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__la); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail);
                try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                     try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                     try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__la); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail).
                - rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  erewrite Mem.load_store_same; eauto; trivial.
                  rewrite i0_v; simpl; reflexivity.
                - erewrite Mem.load_store_same; eauto; trivial.
                - rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  erewrite Mem.load_store_same; eauto; trivial.
                - inv Hm.
                  + rewrite Hdestruct3 in H0.
                    inv H0.
                  + rewrite ZMap.gss.
                    rewrite Hdestruct3 in H0.
                    inv H0.
                    rewrite Hcal in Hdestruct4; inv Hdestruct4.
                    assert (Hcal´: CalMCSLock (TEVENT 2 (TTICKET (SWAP_TAIL (nat_of_Z (Int.unsigned i)) false)) :: l)
                                   = Some (MCSLOCK 2 (ZMap.set 2 (true, NULL) lock_array)
                                                   (bounds ++ nat_of_Z (Int.unsigned i) :: nil))).
                    { Transparent CalMCSLock.
                      simpl.
                      rewrite Hcal; unfold CalMCSLock.NULL; reflexivity. }
                    assert (Hnc0´: ZMap.get 0 (ZMap.set 2 (true, TOTAL_CPU) lock_array) = (bs0, ne0)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc1´: ZMap.get 1 (ZMap.set 2 (true, TOTAL_CPU) lock_array) = (bs1, ne1)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc2´: ZMap.get 2 (ZMap.set 2 (true, TOTAL_CPU) lock_array) = (true, TOTAL_CPU)).
                    { rewrite ZMap.gss; reflexivity. }
                    assert (Hnc3´: ZMap.get 3 (ZMap.set 2 (true, TOTAL_CPU) lock_array) = (bs3, ne3)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc4´: ZMap.get 4 (ZMap.set 2 (true, TOTAL_CPU) lock_array) = (bs4, ne4)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc5´: ZMap.get 5 (ZMap.set 2 (true, TOTAL_CPU) lock_array) = (bs5, ne5)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc6´: ZMap.get 6 (ZMap.set 2 (true, TOTAL_CPU) lock_array) = (bs6, ne6)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc7´: ZMap.get 7 (ZMap.set 2 (true, TOTAL_CPU) lock_array) = (bs7, ne7)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    eapply MATCH_MCSLOCK_VALID with (2:= Hnc0´) (3:= Hnc1´) (4:= Hnc2´) (5:= Hnc3´) (6:= Hnc4´)
                                                                (7:= Hnc5´) (8:= Hnc6´) (9:= Hnc7´) in Hcal´; assumption. }
              { specialize (HMCSLock´ _ Hvalid).
                clear HV__la HV__bs0 HV__ne0 HV__bs1 HV__ne1 HV__bs2 HV__ne2 HV__bs3 HV__ne3 HV__bs4 HV__ne4
                      HV__bs5 HV__ne5 HV__bs6 HV__ne6 HV__bs7 HV__ne7.
                destruct HMCSLock´ as (la´ & bs0´ & ne0´ & bs1´ & ne1´ & bs2´ & ne2´ & bs3´ & ne3´ &
                                       bs4´ & ne4´ & bs5´ & ne5´ & bs6´ & ne6´ & bs7´ & ne7´ &
                                       HL__la´ & HL__bs0´ & HL__ne0´ & HL__bs1´ & HL__ne1´ & HL__bs2´ & HL__ne2´ & HL__bs3´ & HL__ne3´ &
                                       HL__bs4´ & HL__ne4´ & HL__bs5´ & HL__ne5´ & HL__bs6´ & HL__ne6´ & HL__bs7´ & HL__ne7´ &
                                       HV__la´ & HV__bs0´ & HV__ne0´ & HV__bs1´ & HV__ne1´ & HV__bs2´ & HV__ne2´ & HV__bs3´ & HV__ne3´ &
                                       HV__bs4´ & HV__ne4´ & HV__bs5´ & HV__ne5´ & HV__bs6´ & HV__ne6´ & HV__bs7´ & HV__ne7´ & HM´).
                 la´, bs0´, ne0´, bs1´, ne1´, bs2´, ne2´, bs3´, ne3´, bs4´, ne4´, bs5´, ne5´, bs6´, ne6´, bs7´, ne7´.
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__la) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                refine_split´; trivial; try (repeat (eapply Mem.store_valid_access_1; eauto)).
                rewrite ZMap.gso; auto.
                rewrite <- multi_log_re; trivial. }
            +
              rewrite i03 in ×.
              destruct (zeq (Int.unsigned i0) lock_index); subst.
              { (Vint (Int.repr 3)).
                 bs0_v, ne0_v.
                 bs1_v, ne1_v.
                 bs2_v, ne2_v.
                 (Vint (Int.repr (BooltoZ true))), (Vint (Int.repr NULL)).
                 bs4_v, ne4_v.
                 bs5_v, ne5_v.
                 bs6_v, ne6_v.
                 bs7_v, ne7_v.
                assert (i0_v: i1 = Int.repr 3).
                { rewrite <- i03; rewrite Int.repr_unsigned; reflexivity. }
                refine_split´; eauto; try (repeat (eapply Mem.store_valid_access_1; eauto));
                try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__la); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail);
                try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                     try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                     try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__la); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail).
                - rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  erewrite Mem.load_store_same; eauto; trivial.
                  rewrite i0_v; simpl; reflexivity.
                - erewrite Mem.load_store_same; eauto; trivial.
                - rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  erewrite Mem.load_store_same; eauto; trivial.
                - inv Hm.
                  + rewrite Hdestruct3 in H0.
                    inv H0.
                  + rewrite ZMap.gss.
                    rewrite Hdestruct3 in H0.
                    inv H0.
                    rewrite Hcal in Hdestruct4; inv Hdestruct4.
                    assert (Hcal´: CalMCSLock (TEVENT 3 (TTICKET (SWAP_TAIL (nat_of_Z (Int.unsigned i)) false)) :: l)
                                   = Some (MCSLOCK 3 (ZMap.set 3 (true, NULL) lock_array)
                                                   (bounds ++ nat_of_Z (Int.unsigned i) :: nil))).
                    { Transparent CalMCSLock.
                      simpl.
                      rewrite Hcal; unfold CalMCSLock.NULL; reflexivity. }
                    assert (Hnc0´: ZMap.get 0 (ZMap.set 3 (true, TOTAL_CPU) lock_array) = (bs0, ne0)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc1´: ZMap.get 1 (ZMap.set 3 (true, TOTAL_CPU) lock_array) = (bs1, ne1)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc2´: ZMap.get 2 (ZMap.set 3 (true, TOTAL_CPU) lock_array) = (bs2, ne2)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc3´: ZMap.get 3 (ZMap.set 3 (true, TOTAL_CPU) lock_array) = (true, TOTAL_CPU)).
                    { rewrite ZMap.gss; reflexivity. }
                    assert (Hnc4´: ZMap.get 4 (ZMap.set 3 (true, TOTAL_CPU) lock_array) = (bs4, ne4)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc5´: ZMap.get 5 (ZMap.set 3 (true, TOTAL_CPU) lock_array) = (bs5, ne5)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc6´: ZMap.get 6 (ZMap.set 3 (true, TOTAL_CPU) lock_array) = (bs6, ne6)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc7´: ZMap.get 7 (ZMap.set 3 (true, TOTAL_CPU) lock_array) = (bs7, ne7)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    eapply MATCH_MCSLOCK_VALID with (2:= Hnc0´) (3:= Hnc1´) (4:= Hnc2´) (5:= Hnc3´) (6:= Hnc4´)
                                                                (7:= Hnc5´) (8:= Hnc6´) (9:= Hnc7´) in Hcal´; assumption. }
              { specialize (HMCSLock´ _ Hvalid).
                clear HV__la HV__bs0 HV__ne0 HV__bs1 HV__ne1 HV__bs2 HV__ne2 HV__bs3 HV__ne3 HV__bs4 HV__ne4
                      HV__bs5 HV__ne5 HV__bs6 HV__ne6 HV__bs7 HV__ne7.
                destruct HMCSLock´ as (la´ & bs0´ & ne0´ & bs1´ & ne1´ & bs2´ & ne2´ & bs3´ & ne3´ &
                                       bs4´ & ne4´ & bs5´ & ne5´ & bs6´ & ne6´ & bs7´ & ne7´ &
                                       HL__la´ & HL__bs0´ & HL__ne0´ & HL__bs1´ & HL__ne1´ & HL__bs2´ & HL__ne2´ & HL__bs3´ & HL__ne3´ &
                                       HL__bs4´ & HL__ne4´ & HL__bs5´ & HL__ne5´ & HL__bs6´ & HL__ne6´ & HL__bs7´ & HL__ne7´ &
                                       HV__la´ & HV__bs0´ & HV__ne0´ & HV__bs1´ & HV__ne1´ & HV__bs2´ & HV__ne2´ & HV__bs3´ & HV__ne3´ &
                                       HV__bs4´ & HV__ne4´ & HV__bs5´ & HV__ne5´ & HV__bs6´ & HV__ne6´ & HV__bs7´ & HV__ne7´ & HM´).
                 la´, bs0´, ne0´, bs1´, ne1´, bs2´, ne2´, bs3´, ne3´, bs4´, ne4´, bs5´, ne5´, bs6´, ne6´, bs7´, ne7´.
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__la) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                refine_split´; trivial; try (repeat (eapply Mem.store_valid_access_1; eauto)).
                rewrite ZMap.gso; auto.
                rewrite <- multi_log_re; trivial. }
            +
              rewrite i04 in ×.
              destruct (zeq (Int.unsigned i0) lock_index); subst.
              { (Vint (Int.repr 4)).
                 bs0_v, ne0_v.
                 bs1_v, ne1_v.
                 bs2_v, ne2_v.
                 bs3_v, ne3_v.
                 (Vint (Int.repr (BooltoZ true))), (Vint (Int.repr NULL)).
                 bs5_v, ne5_v.
                 bs6_v, ne6_v.
                 bs7_v, ne7_v.
                assert (i0_v: i1 = Int.repr 4).
                { rewrite <- i04; rewrite Int.repr_unsigned; reflexivity. }
                refine_split´; eauto; try (repeat (eapply Mem.store_valid_access_1; eauto));
                try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__la); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail);
                try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                     try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                     try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__la); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail).
                - rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  erewrite Mem.load_store_same; eauto; trivial.
                  rewrite i0_v; simpl; reflexivity.
                - erewrite Mem.load_store_same; eauto; trivial.
                - rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  erewrite Mem.load_store_same; eauto; trivial.
                - inv Hm.
                  + rewrite Hdestruct3 in H0.
                    inv H0.
                  + rewrite ZMap.gss.
                    rewrite Hdestruct3 in H0.
                    inv H0.
                    rewrite Hcal in Hdestruct4; inv Hdestruct4.
                    assert (Hcal´: CalMCSLock (TEVENT 4 (TTICKET (SWAP_TAIL (nat_of_Z (Int.unsigned i)) false)) :: l)
                                   = Some (MCSLOCK 4 (ZMap.set 4 (true, NULL) lock_array)
                                                   (bounds ++ nat_of_Z (Int.unsigned i) :: nil))).
                    { Transparent CalMCSLock.
                      simpl.
                      rewrite Hcal; unfold CalMCSLock.NULL; reflexivity. }
                    assert (Hnc0´: ZMap.get 0 (ZMap.set 4 (true, TOTAL_CPU) lock_array) = (bs0, ne0)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc1´: ZMap.get 1 (ZMap.set 4 (true, TOTAL_CPU) lock_array) = (bs1, ne1)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc2´: ZMap.get 2 (ZMap.set 4 (true, TOTAL_CPU) lock_array) = (bs2, ne2)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc3´: ZMap.get 3 (ZMap.set 4 (true, TOTAL_CPU) lock_array) = (bs3, ne3)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc4´: ZMap.get 4 (ZMap.set 4 (true, TOTAL_CPU) lock_array) = (true, TOTAL_CPU)).
                    { rewrite ZMap.gss; reflexivity. }
                    assert (Hnc5´: ZMap.get 5 (ZMap.set 4 (true, TOTAL_CPU) lock_array) = (bs5, ne5)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc6´: ZMap.get 6 (ZMap.set 4 (true, TOTAL_CPU) lock_array) = (bs6, ne6)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc7´: ZMap.get 7 (ZMap.set 4 (true, TOTAL_CPU) lock_array) = (bs7, ne7)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    eapply MATCH_MCSLOCK_VALID with (2:= Hnc0´) (3:= Hnc1´) (4:= Hnc2´) (5:= Hnc3´) (6:= Hnc4´)
                                                                (7:= Hnc5´) (8:= Hnc6´) (9:= Hnc7´) in Hcal´; assumption. }
              { specialize (HMCSLock´ _ Hvalid).
                clear HV__la HV__bs0 HV__ne0 HV__bs1 HV__ne1 HV__bs2 HV__ne2 HV__bs3 HV__ne3 HV__bs4 HV__ne4
                      HV__bs5 HV__ne5 HV__bs6 HV__ne6 HV__bs7 HV__ne7.
                destruct HMCSLock´ as (la´ & bs0´ & ne0´ & bs1´ & ne1´ & bs2´ & ne2´ & bs3´ & ne3´ &
                                       bs4´ & ne4´ & bs5´ & ne5´ & bs6´ & ne6´ & bs7´ & ne7´ &
                                       HL__la´ & HL__bs0´ & HL__ne0´ & HL__bs1´ & HL__ne1´ & HL__bs2´ & HL__ne2´ & HL__bs3´ & HL__ne3´ &
                                       HL__bs4´ & HL__ne4´ & HL__bs5´ & HL__ne5´ & HL__bs6´ & HL__ne6´ & HL__bs7´ & HL__ne7´ &
                                       HV__la´ & HV__bs0´ & HV__ne0´ & HV__bs1´ & HV__ne1´ & HV__bs2´ & HV__ne2´ & HV__bs3´ & HV__ne3´ &
                                       HV__bs4´ & HV__ne4´ & HV__bs5´ & HV__ne5´ & HV__bs6´ & HV__ne6´ & HV__bs7´ & HV__ne7´ & HM´).
                 la´, bs0´, ne0´, bs1´, ne1´, bs2´, ne2´, bs3´, ne3´, bs4´, ne4´, bs5´, ne5´, bs6´, ne6´, bs7´, ne7´.
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__la) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                refine_split´; trivial; try (repeat (eapply Mem.store_valid_access_1; eauto)).
                rewrite ZMap.gso; auto.
                rewrite <- multi_log_re; trivial. }
            +
              rewrite i05 in ×.
              destruct (zeq (Int.unsigned i0) lock_index); subst.
              { (Vint (Int.repr 5)).
                 bs0_v, ne0_v.
                 bs1_v, ne1_v.
                 bs2_v, ne2_v.
                 bs3_v, ne3_v.
                 bs4_v, ne4_v.
                 (Vint (Int.repr (BooltoZ true))), (Vint (Int.repr NULL)).
                 bs6_v, ne6_v.
                 bs7_v, ne7_v.
                assert (i0_v: i1 = Int.repr 5).
                { rewrite <- i05; rewrite Int.repr_unsigned; reflexivity. }
                refine_split´; eauto; try (repeat (eapply Mem.store_valid_access_1; eauto));
                try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__la); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail);
                try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                     try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                     try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__la); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail).
                - rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  erewrite Mem.load_store_same; eauto; trivial.
                  rewrite i0_v; simpl; reflexivity.
                - erewrite Mem.load_store_same; eauto; trivial.
                - rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  erewrite Mem.load_store_same; eauto; trivial.
                - inv Hm.
                  + rewrite Hdestruct3 in H0.
                    inv H0.
                  + rewrite ZMap.gss.
                    rewrite Hdestruct3 in H0.
                    inv H0.
                    rewrite Hcal in Hdestruct4; inv Hdestruct4.
                    assert (Hcal´: CalMCSLock (TEVENT 5 (TTICKET (SWAP_TAIL (nat_of_Z (Int.unsigned i)) false)) :: l)
                                   = Some (MCSLOCK 5 (ZMap.set 5 (true, NULL) lock_array)
                                                   (bounds ++ nat_of_Z (Int.unsigned i) :: nil))).
                    { Transparent CalMCSLock.
                      simpl.
                      rewrite Hcal; unfold CalMCSLock.NULL; reflexivity. }
                    assert (Hnc0´: ZMap.get 0 (ZMap.set 5 (true, TOTAL_CPU) lock_array) = (bs0, ne0)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc1´: ZMap.get 1 (ZMap.set 5 (true, TOTAL_CPU) lock_array) = (bs1, ne1)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc2´: ZMap.get 2 (ZMap.set 5 (true, TOTAL_CPU) lock_array) = (bs2, ne2)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc3´: ZMap.get 3 (ZMap.set 5 (true, TOTAL_CPU) lock_array) = (bs3, ne3)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc4´: ZMap.get 4 (ZMap.set 5 (true, TOTAL_CPU) lock_array) = (bs4, ne4)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc5´: ZMap.get 5 (ZMap.set 5 (true, TOTAL_CPU) lock_array) = (true, TOTAL_CPU)).
                    { rewrite ZMap.gss; reflexivity. }
                    assert (Hnc6´: ZMap.get 6 (ZMap.set 5 (true, TOTAL_CPU) lock_array) = (bs6, ne6)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc7´: ZMap.get 7 (ZMap.set 5 (true, TOTAL_CPU) lock_array) = (bs7, ne7)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    eapply MATCH_MCSLOCK_VALID with (2:= Hnc0´) (3:= Hnc1´) (4:= Hnc2´) (5:= Hnc3´) (6:= Hnc4´)
                                                                (7:= Hnc5´) (8:= Hnc6´) (9:= Hnc7´) in Hcal´; assumption. }
              { specialize (HMCSLock´ _ Hvalid).
                clear HV__la HV__bs0 HV__ne0 HV__bs1 HV__ne1 HV__bs2 HV__ne2 HV__bs3 HV__ne3 HV__bs4 HV__ne4
                      HV__bs5 HV__ne5 HV__bs6 HV__ne6 HV__bs7 HV__ne7.
                destruct HMCSLock´ as (la´ & bs0´ & ne0´ & bs1´ & ne1´ & bs2´ & ne2´ & bs3´ & ne3´ &
                                       bs4´ & ne4´ & bs5´ & ne5´ & bs6´ & ne6´ & bs7´ & ne7´ &
                                       HL__la´ & HL__bs0´ & HL__ne0´ & HL__bs1´ & HL__ne1´ & HL__bs2´ & HL__ne2´ & HL__bs3´ & HL__ne3´ &
                                       HL__bs4´ & HL__ne4´ & HL__bs5´ & HL__ne5´ & HL__bs6´ & HL__ne6´ & HL__bs7´ & HL__ne7´ &
                                       HV__la´ & HV__bs0´ & HV__ne0´ & HV__bs1´ & HV__ne1´ & HV__bs2´ & HV__ne2´ & HV__bs3´ & HV__ne3´ &
                                       HV__bs4´ & HV__ne4´ & HV__bs5´ & HV__ne5´ & HV__bs6´ & HV__ne6´ & HV__bs7´ & HV__ne7´ & HM´).
                 la´, bs0´, ne0´, bs1´, ne1´, bs2´, ne2´, bs3´, ne3´, bs4´, ne4´, bs5´, ne5´, bs6´, ne6´, bs7´, ne7´.
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__la) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                refine_split´; trivial; try (repeat (eapply Mem.store_valid_access_1; eauto)).
                rewrite ZMap.gso; auto.
                rewrite <- multi_log_re; trivial. }
            +
              rewrite i06 in ×.
              destruct (zeq (Int.unsigned i0) lock_index); subst.
              { (Vint (Int.repr 6)).
                 bs0_v, ne0_v.
                 bs1_v, ne1_v.
                 bs2_v, ne2_v.
                 bs3_v, ne3_v.
                 bs4_v, ne4_v.
                 bs5_v, ne5_v.
                 (Vint (Int.repr (BooltoZ true))), (Vint (Int.repr NULL)).
                 bs7_v, ne7_v.
                assert (i0_v: i1 = Int.repr 6).
                { rewrite <- i06; rewrite Int.repr_unsigned; reflexivity. }
                refine_split´; eauto; try (repeat (eapply Mem.store_valid_access_1; eauto));
                try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__la); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail);
                try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                     try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                     try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__la); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail).
                - rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  erewrite Mem.load_store_same; eauto; trivial.
                  rewrite i0_v; simpl; reflexivity.
                - erewrite Mem.load_store_same; eauto; trivial.
                - rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  erewrite Mem.load_store_same; eauto; trivial.
                - inv Hm.
                  + rewrite Hdestruct3 in H0.
                    inv H0.
                  + rewrite ZMap.gss.
                    rewrite Hdestruct3 in H0.
                    inv H0.
                    rewrite Hcal in Hdestruct4; inv Hdestruct4.
                    assert (Hcal´: CalMCSLock (TEVENT 6 (TTICKET (SWAP_TAIL (nat_of_Z (Int.unsigned i)) false)) :: l)
                                   = Some (MCSLOCK 6 (ZMap.set 6 (true, NULL) lock_array)
                                                   (bounds ++ nat_of_Z (Int.unsigned i) :: nil))).
                    { Transparent CalMCSLock.
                      simpl.
                      rewrite Hcal; unfold CalMCSLock.NULL; reflexivity. }
                    assert (Hnc0´: ZMap.get 0 (ZMap.set 6 (true, TOTAL_CPU) lock_array) = (bs0, ne0)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc1´: ZMap.get 1 (ZMap.set 6 (true, TOTAL_CPU) lock_array) = (bs1, ne1)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc2´: ZMap.get 2 (ZMap.set 6 (true, TOTAL_CPU) lock_array) = (bs2, ne2)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc3´: ZMap.get 3 (ZMap.set 6 (true, TOTAL_CPU) lock_array) = (bs3, ne3)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc4´: ZMap.get 4 (ZMap.set 6 (true, TOTAL_CPU) lock_array) = (bs4, ne4)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc5´: ZMap.get 5 (ZMap.set 6 (true, TOTAL_CPU) lock_array) = (bs5, ne5)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc6´: ZMap.get 6 (ZMap.set 6 (true, TOTAL_CPU) lock_array) = (true, TOTAL_CPU)).
                    { rewrite ZMap.gss; reflexivity. }
                    assert (Hnc7´: ZMap.get 7 (ZMap.set 6 (true, TOTAL_CPU) lock_array) = (bs7, ne7)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    eapply MATCH_MCSLOCK_VALID with (2:= Hnc0´) (3:= Hnc1´) (4:= Hnc2´) (5:= Hnc3´) (6:= Hnc4´)
                                                                (7:= Hnc5´) (8:= Hnc6´) (9:= Hnc7´) in Hcal´; assumption. }
              { specialize (HMCSLock´ _ Hvalid).
                clear HV__la HV__bs0 HV__ne0 HV__bs1 HV__ne1 HV__bs2 HV__ne2 HV__bs3 HV__ne3 HV__bs4 HV__ne4
                      HV__bs5 HV__ne5 HV__bs6 HV__ne6 HV__bs7 HV__ne7.
                destruct HMCSLock´ as (la´ & bs0´ & ne0´ & bs1´ & ne1´ & bs2´ & ne2´ & bs3´ & ne3´ &
                                       bs4´ & ne4´ & bs5´ & ne5´ & bs6´ & ne6´ & bs7´ & ne7´ &
                                       HL__la´ & HL__bs0´ & HL__ne0´ & HL__bs1´ & HL__ne1´ & HL__bs2´ & HL__ne2´ & HL__bs3´ & HL__ne3´ &
                                       HL__bs4´ & HL__ne4´ & HL__bs5´ & HL__ne5´ & HL__bs6´ & HL__ne6´ & HL__bs7´ & HL__ne7´ &
                                       HV__la´ & HV__bs0´ & HV__ne0´ & HV__bs1´ & HV__ne1´ & HV__bs2´ & HV__ne2´ & HV__bs3´ & HV__ne3´ &
                                       HV__bs4´ & HV__ne4´ & HV__bs5´ & HV__ne5´ & HV__bs6´ & HV__ne6´ & HV__bs7´ & HV__ne7´ & HM´).
                 la´, bs0´, ne0´, bs1´, ne1´, bs2´, ne2´, bs3´, ne3´, bs4´, ne4´, bs5´, ne5´, bs6´, ne6´, bs7´, ne7´.
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__la) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                  try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
                refine_split´; trivial; try (repeat (eapply Mem.store_valid_access_1; eauto)).
                rewrite ZMap.gso; auto.
                rewrite <- multi_log_re; trivial. }
            +
              rewrite i07 in ×.
              destruct (zeq (Int.unsigned i0) lock_index); subst.
              { (Vint (Int.repr 7)).
                 bs0_v, ne0_v.
                 bs1_v, ne1_v.
                 bs2_v, ne2_v.
                 bs3_v, ne3_v.
                 bs4_v, ne4_v.
                 bs5_v, ne5_v.
                 bs6_v, ne6_v.
                 (Vint (Int.repr (BooltoZ true))), (Vint (Int.repr NULL)).
                assert (i0_v: i1 = Int.repr 7).
                { rewrite <- i07; rewrite Int.repr_unsigned; reflexivity. }
                refine_split´; eauto; try (repeat (eapply Mem.store_valid_access_1; eauto));
                try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                     try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                     try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                     rewrite (Mem.load_store_other _ _ _ _ _ _ HST__la); auto;
                     try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail).
                - rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  erewrite Mem.load_store_same; eauto; trivial.
                  rewrite i0_v; simpl; reflexivity.
                - erewrite Mem.load_store_same; eauto; trivial.
                - rewrite (Mem.load_store_other _ _ _ _ _ _ HST__bs); auto;
                  try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).
                  erewrite Mem.load_store_same; eauto; trivial.
                - inv Hm.
                  + rewrite Hdestruct3 in H0.
                    inv H0.
                  + rewrite ZMap.gss.
                    rewrite Hdestruct3 in H0.
                    inv H0.
                    rewrite Hcal in Hdestruct4; inv Hdestruct4.
                    assert (Hcal´: CalMCSLock (TEVENT 7 (TTICKET (SWAP_TAIL (nat_of_Z (Int.unsigned i)) false)) :: l)
                                   = Some (MCSLOCK 7 (ZMap.set 7 (true, NULL) lock_array)
                                                   (bounds ++ nat_of_Z (Int.unsigned i) :: nil))).
                    { Transparent CalMCSLock.
                      simpl.
                      rewrite Hcal; unfold CalMCSLock.NULL; reflexivity. }
                    assert (Hnc0´: ZMap.get 0 (ZMap.set 7 (true, TOTAL_CPU) lock_array) = (bs0, ne0)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc1´: ZMap.get 1 (ZMap.set 7 (true, TOTAL_CPU) lock_array) = (bs1, ne1)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc2´: ZMap.get 2 (ZMap.set 7 (true, TOTAL_CPU) lock_array) = (bs2, ne2)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc3´: ZMap.get 3 (ZMap.set 7 (true, TOTAL_CPU) lock_array) = (bs3, ne3)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc4´: ZMap.get 4 (ZMap.set 7 (true, TOTAL_CPU) lock_array) = (bs4, ne4)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc5´: ZMap.get 5 (ZMap.set 7 (true, TOTAL_CPU) lock_array) = (bs5, ne5)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc6´: ZMap.get 6 (ZMap.set 7 (true, TOTAL_CPU) lock_array) = (bs6, ne6)).
                    { rewrite ZMap.gso; try assumption; try (unfold not; intro contra; inv contra). }
                    assert (Hnc7´: ZMap.get 7 (ZMap.set 7 (true, TOTAL_CPU) lock_array) = (true, TOTAL_CPU)).
                    { rewrite ZMap.gss; reflexivity. }
                    eapply MATCH_MCSLOCK_VALID with (2:= Hnc0´) (3:= Hnc1´) (4:= Hnc2´) (5:= Hnc3´) (6:= Hnc4´)
                                                                (7:= Hnc5´) (8:= Hnc6´) (9:= Hnc7´) in Hcal´; assumption. }
              { specialize (HMCSLock´ _ Hvalid).
                clear HV__la HV__bs0 HV__ne0 HV__bs1 HV__ne1 HV__bs2 HV__ne2 HV__bs3 HV__ne3 HV__bs4 HV__ne4
                      HV__bs5 HV__ne5 HV__bs6 HV__ne6 HV__bs7 HV__ne7.
                destruct HMCSLock´ as (la´ & bs0´ & ne0´ & bs1´ & ne1´ & bs2´ & ne2´ & bs3´ & ne3´ &
                                       bs4´ & ne4´ & bs5´ & ne5´ & bs6´ & ne6´ & bs7´ & ne7´ &
                                       HL__la´ & HL__bs0´ & HL__ne0´ & HL__bs1´ & HL__ne1´ & HL__bs2´ & HL__ne2´ & HL__bs3´ & HL__ne3´ &
                                       HL__bs4´ & HL__ne4´ & HL__bs5´ & HL__ne5´ & HL__bs6´ & HL__ne6´ & HL__bs7´ & HL__ne7´ &
                                       HV__la´ & HV__bs0´ & HV__ne0´ & HV__bs1´ & HV__ne1´ & HV__bs2´ & HV__ne2´ & HV__bs3´ & HV__ne3´ &
                                       HV__bs4´ & HV__ne4´ & HV__bs5´ & HV__ne5´ & HV__bs6´ & HV__ne6´ & HV__bs7´ & HV__ne7´ & HM´).
                 la´, bs0´, ne0´, bs1´, ne1´, bs2´, ne2´, bs3´, ne3´, bs4´, ne4´, bs5´, ne5´, bs6´, ne6´, bs7´, ne7´.
                rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__la) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
              rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                        HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                        HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
              rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs) in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´,
                                                                      HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                                                                      HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
                try (simpl; right; destruct (zle (Int.unsigned i0) lock_index);
                     [ right; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega |
                       left; unfold tail_pos, next_pos, busy_pos, mcs_node_st_size, mcs_lock_st_size; omega]).
              refine_split´; trivial; try (repeat (eapply Mem.store_valid_access_1; eauto)).
              rewrite ZMap.gso; auto.
              rewrite <- multi_log_re; trivial. }
        - repeat simpl_Pregmap; eauto.
        - intros. inv Hasm_inv.
          inv inv_inject_neutral. subst rs2´.
          destruct r; simpl;
          repeat simpl_Pregmap; eauto;
          (elim H; eauto 20). }
      Qed.

    End mcs_SWAP_TAIL_ref.

  End WITHMEM.

End Refinement.