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

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_GET_NEXT_ref.

      Transparent CalMCSLock.

      Lemma mcs_GET_NEXT_spec_ref:
        compatsim (crel HDATA LDATA) (gensem mcs_GET_NEXT_spec) mcs_GET_NEXT_spec_low.
      Proof.
        compatsim_simpl (@match_AbData).
        assert (Hkern: kernel_mode d2).
        { inv match_related.
          unfold mcs_GET_NEXT_spec in *; subdestruct;
          repeat (split; congruence); eauto. }
        inv Hlog.
        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_GET_NEXT_spec.
        subrewrite´.
        intros ? HQ.
        subdestruct.
        inv HQ.
        pose proof HMCSLock as HMCSLock´.
        specialize (HMCSLock _ a).
        rewrite multi_log_re in HMCSLock.
        assert (i0_vals: Int.unsigned i0 = 0 ∨ Int.unsigned i0 = 1 ∨ Int.unsigned i0 = 2 ∨ Int.unsigned i0 = 3 ∨
                         Int.unsigned i0 = 4 ∨ Int.unsigned i0 = 5 ∨ Int.unsigned i0 = 6 ∨ Int.unsigned i0 = 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).
        inv Hm; [rewrite Hdestruct3 in H0; inv H0 | ].
        rewrite Hdestruct3 in H0.
        inv H0.
        simpl in Hdestruct4.
        rewrite Hdestruct4 in Hcal.
        inv Hcal.
        destruct i0_vals as [i00 | [i01 | [i02 | [i03 | [i04 | [i05 | [i06 | i07]]]]]]].
        -
          rewrite i00 in *; refine_split.
          + econstructor; eauto.
            × unfold mcs_GET_NEXT_log_spec.
              subrewrite´.
            × rewrite i00; eassumption.
          + rewrite Hnc0 in Hdestruct6.
            inv Hdestruct6.
            rewrite Int.repr_unsigned.
            constructor.
          + split; eauto; pattern2_refinement_simpl; trivial.
            econstructor; simpl; eauto.
            econstructor; eauto; intros.
            destruct (zeq (Int.unsigned i) lock_index); subst.
            { ∃ (Vint (Int.repr la)).
              ∃ (Vint (Int.repr (BooltoZ bs0))), (Vint (Int.repr ne0)).
              ∃ (Vint (Int.repr (BooltoZ bs1))), (Vint (Int.repr ne1)).
              ∃ (Vint (Int.repr (BooltoZ bs2))), (Vint (Int.repr ne2)).
              ∃ (Vint (Int.repr (BooltoZ bs3))), (Vint (Int.repr ne3)).
              ∃ (Vint (Int.repr (BooltoZ bs4))), (Vint (Int.repr ne4)).
              ∃ (Vint (Int.repr (BooltoZ bs5))), (Vint (Int.repr ne5)).
              ∃ (Vint (Int.repr (BooltoZ bs6))), (Vint (Int.repr ne6)).
              ∃ (Vint (Int.repr (BooltoZ bs7))), (Vint (Int.repr ne7)).
              refine_split; eauto.
              rewrite ZMap.gss.
              econstructor; try (simpl; rewrite Hdestruct4; reflexivity); 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_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´).
            ∃ 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´.
            try (simpl; right; destruct (zle (Int.unsigned i) lock_index);
                 [right; unfold next_pos, busy_pos, tail_pos; omega | left; unfold next_pos, busy_pos, tail_pos; omega]).
            refine_split´; trivial.
            rewrite ZMap.gso; auto.
            rewrite <- multi_log_re.
            trivial. }
          + apply inject_incr_refl.
        -
          rewrite i01 in *; refine_split.
          + econstructor; eauto.
            × unfold mcs_GET_NEXT_log_spec.
              subrewrite´.
            × rewrite i01; eassumption.
          + rewrite Hnc1 in Hdestruct6.
            inv Hdestruct6.
            rewrite Int.repr_unsigned.
            constructor.
          + split; eauto; pattern2_refinement_simpl; trivial.
            econstructor; simpl; eauto.
            econstructor; eauto; intros.
            destruct (zeq (Int.unsigned i) lock_index); subst.
            { ∃ (Vint (Int.repr la)).
              ∃ (Vint (Int.repr (BooltoZ bs0))), (Vint (Int.repr ne0)).
              ∃ (Vint (Int.repr (BooltoZ bs1))), (Vint (Int.repr ne1)).
              ∃ (Vint (Int.repr (BooltoZ bs2))), (Vint (Int.repr ne2)).
              ∃ (Vint (Int.repr (BooltoZ bs3))), (Vint (Int.repr ne3)).
              ∃ (Vint (Int.repr (BooltoZ bs4))), (Vint (Int.repr ne4)).
              ∃ (Vint (Int.repr (BooltoZ bs5))), (Vint (Int.repr ne5)).
              ∃ (Vint (Int.repr (BooltoZ bs6))), (Vint (Int.repr ne6)).
              ∃ (Vint (Int.repr (BooltoZ bs7))), (Vint (Int.repr ne7)).
              refine_split; eauto.
              rewrite ZMap.gss.
              econstructor; try (simpl; rewrite Hdestruct4; reflexivity); 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_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´).
            ∃ 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´.
            try (simpl; right; destruct (zle (Int.unsigned i) lock_index);
                 [right; unfold next_pos, busy_pos, tail_pos; omega | left; unfold next_pos, busy_pos, tail_pos; omega]).
            refine_split´; trivial.
            rewrite ZMap.gso; auto.
            rewrite <- multi_log_re.
            trivial. }
          + apply inject_incr_refl.
        -
          rewrite i02 in *; refine_split.
          + econstructor; eauto.
            × unfold mcs_GET_NEXT_log_spec.
              subrewrite´.
            × rewrite i02; eassumption.
          + rewrite Hnc2 in Hdestruct6.
            inv Hdestruct6.
            rewrite Int.repr_unsigned.
            constructor.
          + split; eauto; pattern2_refinement_simpl; trivial.
            econstructor; simpl; eauto.
            econstructor; eauto; intros.
            destruct (zeq (Int.unsigned i) lock_index); subst.
            { ∃ (Vint (Int.repr la)).
              ∃ (Vint (Int.repr (BooltoZ bs0))), (Vint (Int.repr ne0)).
              ∃ (Vint (Int.repr (BooltoZ bs1))), (Vint (Int.repr ne1)).
              ∃ (Vint (Int.repr (BooltoZ bs2))), (Vint (Int.repr ne2)).
              ∃ (Vint (Int.repr (BooltoZ bs3))), (Vint (Int.repr ne3)).
              ∃ (Vint (Int.repr (BooltoZ bs4))), (Vint (Int.repr ne4)).
              ∃ (Vint (Int.repr (BooltoZ bs5))), (Vint (Int.repr ne5)).
              ∃ (Vint (Int.repr (BooltoZ bs6))), (Vint (Int.repr ne6)).
              ∃ (Vint (Int.repr (BooltoZ bs7))), (Vint (Int.repr ne7)).
              refine_split; eauto.
              rewrite ZMap.gss.
              econstructor; try (simpl; rewrite Hdestruct4; reflexivity); 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_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´ & bs_6v´ & 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´).
            ∃ 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´, bs_6v´, ne6_v´, bs7_v´, ne7_v´.
            try (simpl; right; destruct (zle (Int.unsigned i) lock_index);
                 [right; unfold next_pos, busy_pos, tail_pos; omega | left; unfold next_pos, busy_pos, tail_pos; omega]).
            refine_split´; trivial.
            rewrite ZMap.gso; auto.
            rewrite <- multi_log_re.
            trivial. }
          + apply inject_incr_refl.
        -
          rewrite i03 in *; refine_split.
          + econstructor; eauto.
            × unfold mcs_GET_NEXT_log_spec.
              subrewrite´.
            × rewrite i03; eassumption.
          + rewrite Hnc3 in Hdestruct6.
            inv Hdestruct6.
            rewrite Int.repr_unsigned.
            constructor.
          + split; eauto; pattern2_refinement_simpl; trivial.
            econstructor; simpl; eauto.
            econstructor; eauto; intros.
            destruct (zeq (Int.unsigned i) lock_index); subst.
            { ∃ (Vint (Int.repr la)).
              ∃ (Vint (Int.repr (BooltoZ bs0))), (Vint (Int.repr ne0)).
              ∃ (Vint (Int.repr (BooltoZ bs1))), (Vint (Int.repr ne1)).
              ∃ (Vint (Int.repr (BooltoZ bs2))), (Vint (Int.repr ne2)).
              ∃ (Vint (Int.repr (BooltoZ bs3))), (Vint (Int.repr ne3)).
              ∃ (Vint (Int.repr (BooltoZ bs4))), (Vint (Int.repr ne4)).
              ∃ (Vint (Int.repr (BooltoZ bs5))), (Vint (Int.repr ne5)).
              ∃ (Vint (Int.repr (BooltoZ bs6))), (Vint (Int.repr ne6)).
              ∃ (Vint (Int.repr (BooltoZ bs7))), (Vint (Int.repr ne7)).
              refine_split; eauto.
              rewrite ZMap.gss.
              econstructor; try (simpl; rewrite Hdestruct4; reflexivity); 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_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´).
            ∃ 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´.
            try (simpl; right; destruct (zle (Int.unsigned i) lock_index);
                 [right; unfold next_pos, busy_pos, tail_pos; omega | left; unfold next_pos, busy_pos, tail_pos; omega]).
            refine_split´; trivial.
            rewrite ZMap.gso; auto.
            rewrite <- multi_log_re.
            trivial. }
          + apply inject_incr_refl.
        -
            rewrite i04 in *; refine_split.
          + econstructor; eauto.
            × unfold mcs_GET_NEXT_log_spec.
              subrewrite´.
            × rewrite i04; eassumption.
          + rewrite Hnc4 in Hdestruct6.
            inv Hdestruct6.
            rewrite Int.repr_unsigned.
            constructor.
          + split; eauto; pattern2_refinement_simpl; trivial.
            econstructor; simpl; eauto.
            econstructor; eauto; intros.
            destruct (zeq (Int.unsigned i) lock_index); subst.
            { ∃ (Vint (Int.repr la)).
              ∃ (Vint (Int.repr (BooltoZ bs0))), (Vint (Int.repr ne0)).
              ∃ (Vint (Int.repr (BooltoZ bs1))), (Vint (Int.repr ne1)).
              ∃ (Vint (Int.repr (BooltoZ bs2))), (Vint (Int.repr ne2)).
              ∃ (Vint (Int.repr (BooltoZ bs3))), (Vint (Int.repr ne3)).
              ∃ (Vint (Int.repr (BooltoZ bs4))), (Vint (Int.repr ne4)).
              ∃ (Vint (Int.repr (BooltoZ bs5))), (Vint (Int.repr ne5)).
              ∃ (Vint (Int.repr (BooltoZ bs6))), (Vint (Int.repr ne6)).
              ∃ (Vint (Int.repr (BooltoZ bs7))), (Vint (Int.repr ne7)).
              refine_split; eauto.
              rewrite ZMap.gss.
              econstructor; try (simpl; rewrite Hdestruct4; reflexivity); 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_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´).
            ∃ 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´.
            try (simpl; right; destruct (zle (Int.unsigned i) lock_index);
                 [right; unfold next_pos, busy_pos, tail_pos; omega | left; unfold next_pos, busy_pos, tail_pos; omega]).
            refine_split´; trivial.
            rewrite ZMap.gso; auto.
            rewrite <- multi_log_re.
            trivial. }
          + apply inject_incr_refl.
        -
          rewrite i05 in *; refine_split.
          + econstructor; eauto.
            × unfold mcs_GET_NEXT_log_spec.
              subrewrite´.
            × rewrite i05; eassumption.
          + rewrite Hnc5 in Hdestruct6.
            inv Hdestruct6.
            rewrite Int.repr_unsigned.
            constructor.
          + split; eauto; pattern2_refinement_simpl; trivial.
            econstructor; simpl; eauto.
            econstructor; eauto; intros.
            destruct (zeq (Int.unsigned i) lock_index); subst.
            { ∃ (Vint (Int.repr la)).
              ∃ (Vint (Int.repr (BooltoZ bs0))), (Vint (Int.repr ne0)).
              ∃ (Vint (Int.repr (BooltoZ bs1))), (Vint (Int.repr ne1)).
              ∃ (Vint (Int.repr (BooltoZ bs2))), (Vint (Int.repr ne2)).
              ∃ (Vint (Int.repr (BooltoZ bs3))), (Vint (Int.repr ne3)).
              ∃ (Vint (Int.repr (BooltoZ bs4))), (Vint (Int.repr ne4)).
              ∃ (Vint (Int.repr (BooltoZ bs5))), (Vint (Int.repr ne5)).
              ∃ (Vint (Int.repr (BooltoZ bs6))), (Vint (Int.repr ne6)).
              ∃ (Vint (Int.repr (BooltoZ bs7))), (Vint (Int.repr ne7)).
              refine_split; eauto.
              rewrite ZMap.gss.
              econstructor; try (simpl; rewrite Hdestruct4; reflexivity); 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_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´).
            ∃ 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´.
            try (simpl; right; destruct (zle (Int.unsigned i) lock_index);
                 [right; unfold next_pos, busy_pos, tail_pos; omega | left; unfold next_pos, busy_pos, tail_pos; omega]).
            refine_split´; trivial.
            rewrite ZMap.gso; auto.
            rewrite <- multi_log_re.
            trivial. }
          + apply inject_incr_refl.
        -
            rewrite i06 in *; refine_split.
          + econstructor; eauto.
            × unfold mcs_GET_NEXT_log_spec.
              subrewrite´.
            × rewrite i06; eassumption.
          + rewrite Hnc6 in Hdestruct6.
            inv Hdestruct6.
            rewrite Int.repr_unsigned.
            constructor.
          + split; eauto; pattern2_refinement_simpl; trivial.
            econstructor; simpl; eauto.
            econstructor; eauto; intros.
            destruct (zeq (Int.unsigned i) lock_index); subst.
            { ∃ (Vint (Int.repr la)).
              ∃ (Vint (Int.repr (BooltoZ bs0))), (Vint (Int.repr ne0)).
              ∃ (Vint (Int.repr (BooltoZ bs1))), (Vint (Int.repr ne1)).
              ∃ (Vint (Int.repr (BooltoZ bs2))), (Vint (Int.repr ne2)).
              ∃ (Vint (Int.repr (BooltoZ bs3))), (Vint (Int.repr ne3)).
              ∃ (Vint (Int.repr (BooltoZ bs4))), (Vint (Int.repr ne4)).
              ∃ (Vint (Int.repr (BooltoZ bs5))), (Vint (Int.repr ne5)).
              ∃ (Vint (Int.repr (BooltoZ bs6))), (Vint (Int.repr ne6)).
              ∃ (Vint (Int.repr (BooltoZ bs7))), (Vint (Int.repr ne7)).
              refine_split; eauto.
              rewrite ZMap.gss.
              econstructor; try (simpl; rewrite Hdestruct4; reflexivity); 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_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´).
            ∃ 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´.
            try (simpl; right; destruct (zle (Int.unsigned i) lock_index);
                 [right; unfold next_pos, busy_pos, tail_pos; omega | left; unfold next_pos, busy_pos, tail_pos; omega]).
            refine_split´; trivial.
            rewrite ZMap.gso; auto.
            rewrite <- multi_log_re.
            trivial. }
          + apply inject_incr_refl.
        -
            rewrite i07 in *; refine_split.
          + econstructor; eauto.
            × unfold mcs_GET_NEXT_log_spec.
              subrewrite´.
            × rewrite i07; eassumption.
          + rewrite Hnc7 in Hdestruct6.
            inv Hdestruct6.
            rewrite Int.repr_unsigned.
            constructor.
          + split; eauto; pattern2_refinement_simpl; trivial.
            econstructor; simpl; eauto.
            econstructor; eauto; intros.
            destruct (zeq (Int.unsigned i) lock_index); subst.
            { ∃ (Vint (Int.repr la)).
              ∃ (Vint (Int.repr (BooltoZ bs0))), (Vint (Int.repr ne0)).
              ∃ (Vint (Int.repr (BooltoZ bs1))), (Vint (Int.repr ne1)).
              ∃ (Vint (Int.repr (BooltoZ bs2))), (Vint (Int.repr ne2)).
              ∃ (Vint (Int.repr (BooltoZ bs3))), (Vint (Int.repr ne3)).
              ∃ (Vint (Int.repr (BooltoZ bs4))), (Vint (Int.repr ne4)).
              ∃ (Vint (Int.repr (BooltoZ bs5))), (Vint (Int.repr ne5)).
              ∃ (Vint (Int.repr (BooltoZ bs6))), (Vint (Int.repr ne6)).
              ∃ (Vint (Int.repr (BooltoZ bs7))), (Vint (Int.repr ne7)).
              refine_split; eauto.
              rewrite ZMap.gss.
              econstructor; try (simpl; rewrite Hdestruct4; reflexivity); 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_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´).
            ∃ 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´.
            try (simpl; right; destruct (zle (Int.unsigned i) lock_index);
                 [right; unfold next_pos, busy_pos, tail_pos; omega | left; unfold next_pos, busy_pos, tail_pos; omega]).
            refine_split´; trivial.
            rewrite ZMap.gso; auto.
            rewrite <- multi_log_re.
            trivial. }
          + apply inject_incr_refl.
      Qed.

    End mcs_GET_NEXT_ref.

    Section mcs_SET_NEXT_ref.

      Lemma mcs_SET_NEXT_spec_ref:
        compatsim (crel HDATA LDATA) (gensem mcs_SET_NEXT_spec) mcs_SET_NEXT_spec_low.
      Proof.
        compatsim_simpl (@match_AbData).
        assert (Hkern: kernel_mode d2).
        { inv match_related.
          unfold mcs_SET_NEXT_spec in *; subdestruct;
          repeat (split; congruence); eauto. }
        inv Hlog.
        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_SET_NEXT_spec.
        subrewrite´.
        intros ? HQ.
        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: ∃ m´, Mem.store Mint32 m2 b (next_pos (Int.unsigned i) (Int.unsigned i1))
                                                                (Vint (Int.repr (Int.unsigned i0))) = Some m´).
        { eapply Mem.valid_access_store; eauto.
          destruct i1_vals as [i1_v | [i1_v | [i1_v | [i1_v | [i1_v | [i1_v | [i1_v | i1_v]]]]]]];
            rewrite i1_v; assumption. }
        destruct HST as (m´ & HST).
        rewrite Int.repr_unsigned in HST.
        refine_split.
        - econstructor; try eauto.
          unfold mcs_SET_NEXT_log_spec.
          subrewrite´.
        - econstructor.
        - split; eauto; pattern2_refinement_simpl; trivial.
          econstructor; simpl; eauto.
          econstructor; eauto; intros.
          destruct i1_vals as [i1_v | [i1_v | [i1_v | [i1_v | [i1_v | [i1_v | [i1_v | i1_v]]]]]]];
            rewrite i1_v in ×.
          {
            destruct (zeq (Int.unsigned i) lock_index); subst.
            - ∃ la_v.
              ∃ bs0_v, (Vint i0).
              ∃ 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.
              refine_split´; eauto; try (repeat (eapply Mem.store_valid_access_1; eauto));
              try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST); auto;
                   try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                   try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail).
              + unfold next_pos in HST; unfold next_pos; erewrite Mem.load_store_same; eauto; trivial.
              + rewrite ZMap.gss.
                rewrite Hdestruct4 in Hm; inv Hm.
                assert (Hcal´: CalMCSLock (TEVENT (Int.unsigned i0) (TTICKET (SET_NEXT 0)) :: l)
                               = Some (MCSLOCK la (ZMap.set 0 (bs0, (Int.unsigned i0)) np) tq)).
                { Transparent CalMCSLock.
                  simpl.
                  rewrite Hcal; rewrite Hnc0; reflexivity. }
                assert (Hnc0´: ZMap.get 0 (ZMap.set 0 (bs0, Int.unsigned i0) np) = (bs0, Int.unsigned i0)).
                { rewrite ZMap.gss; reflexivity. }
                assert (Hnc1´: ZMap.get 1 (ZMap.set 0 (bs0, Int.unsigned i0) np) = (bs1, ne1)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc2´: ZMap.get 2 (ZMap.set 0 (bs0, Int.unsigned i0) np) = (bs2, ne2)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc3´: ZMap.get 3 (ZMap.set 0 (bs0, Int.unsigned i0) np) = (bs3, ne3)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc4´: ZMap.get 4 (ZMap.set 0 (bs0, Int.unsigned i0) np) = (bs4, ne4)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc5´: ZMap.get 5 (ZMap.set 0 (bs0, Int.unsigned i0) np) = (bs5, ne5)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc6´: ZMap.get 6 (ZMap.set 0 (bs0, Int.unsigned i0) np) = (bs6, ne6)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc7´: ZMap.get 7 (ZMap.set 0 (bs0, Int.unsigned i0) np) = (bs7, ne7)).
                { rewrite ZMap.gso; try assumption; unfold not; intros 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´.
                rewrite Int.repr_unsigned 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_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´ & bs_6v´ & 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´).
              ∃ 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´, bs_6v´, ne6_v´, bs7_v´, ne7_v´.
              rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) 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 i) 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. }
          {
            destruct (zeq (Int.unsigned i) lock_index); subst.
            - ∃ la_v.
              ∃ bs0_v, ne0_v.
              ∃ bs1_v, (Vint i0).
              ∃ bs2_v, ne2_v.
              ∃ bs3_v, ne3_v.
              ∃ bs4_v, ne4_v.
              ∃ bs5_v, ne5_v.
              ∃ bs6_v, ne6_v.
              ∃ bs7_v, ne7_v.
              refine_split´; eauto; try (repeat (eapply Mem.store_valid_access_1; eauto));
              try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST); auto;
                   try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                   try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail).
              + unfold next_pos in HST; unfold next_pos; erewrite Mem.load_store_same; eauto; trivial.
              + rewrite ZMap.gss.
                rewrite Hdestruct4 in Hm; inv Hm.
                assert (Hcal´: CalMCSLock (TEVENT (Int.unsigned i0) (TTICKET (SET_NEXT 1)) :: l)
                               = Some (MCSLOCK la (ZMap.set 1 (bs1, (Int.unsigned i0)) np) tq)).
                { Transparent CalMCSLock.
                  simpl.
                  rewrite Hcal; rewrite Hnc1; reflexivity. }
                assert (Hnc0´: ZMap.get 0 (ZMap.set 1 (bs1, Int.unsigned i0) np) = (bs0, ne0)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc1´: ZMap.get 1 (ZMap.set 1 (bs1, Int.unsigned i0) np) = (bs1, Int.unsigned i0)).
                { rewrite ZMap.gss; reflexivity. }
                assert (Hnc2´: ZMap.get 2 (ZMap.set 1 (bs1, Int.unsigned i0) np) = (bs2, ne2)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc3´: ZMap.get 3 (ZMap.set 1 (bs1, Int.unsigned i0) np) = (bs3, ne3)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc4´: ZMap.get 4 (ZMap.set 1 (bs1, Int.unsigned i0) np) = (bs4, ne4)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc5´: ZMap.get 5 (ZMap.set 1 (bs1, Int.unsigned i0) np) = (bs5, ne5)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc6´: ZMap.get 6 (ZMap.set 1 (bs1, Int.unsigned i0) np) = (bs6, ne6)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc7´: ZMap.get 7 (ZMap.set 1 (bs1, Int.unsigned i0) np) = (bs7, ne7)).
                { rewrite ZMap.gso; try assumption; unfold not; intros 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´.
                rewrite Int.repr_unsigned 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_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´ & bs_6v´ & 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´).
              ∃ 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´, bs_6v´, ne6_v´, bs7_v´, ne7_v´.
              rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) 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 i) 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. }
          {
            destruct (zeq (Int.unsigned i) lock_index); subst.
            - ∃ la_v.
              ∃ bs0_v, ne0_v.
              ∃ bs1_v, ne1_v.
              ∃ bs2_v, (Vint i0).
              ∃ bs3_v, ne3_v.
              ∃ bs4_v, ne4_v.
              ∃ bs5_v, ne5_v.
              ∃ bs6_v, ne6_v.
              ∃ bs7_v, ne7_v.
              refine_split´; eauto; try (repeat (eapply Mem.store_valid_access_1; eauto));
              try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST); auto;
                   try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                   try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail).
              + unfold next_pos in HST; unfold next_pos; erewrite Mem.load_store_same; eauto; trivial.
              + rewrite ZMap.gss.
                rewrite Hdestruct4 in Hm; inv Hm.
                assert (Hcal´: CalMCSLock (TEVENT (Int.unsigned i0) (TTICKET (SET_NEXT 2)) :: l)
                               = Some (MCSLOCK la (ZMap.set 2 (bs2, (Int.unsigned i0)) np) tq)).
                { Transparent CalMCSLock.
                  simpl.
                  rewrite Hcal; rewrite Hnc2; reflexivity. }
                assert (Hnc0´: ZMap.get 0 (ZMap.set 2 (bs2, Int.unsigned i0) np) = (bs0, ne0)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc1´: ZMap.get 1 (ZMap.set 2 (bs2, Int.unsigned i0) np) = (bs1, ne1)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc2´: ZMap.get 2 (ZMap.set 2 (bs2, Int.unsigned i0) np) = (bs2, Int.unsigned i0)).
                { rewrite ZMap.gss; reflexivity. }
                assert (Hnc3´: ZMap.get 3 (ZMap.set 2 (bs2, Int.unsigned i0) np) = (bs3, ne3)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc4´: ZMap.get 4 (ZMap.set 2 (bs2, Int.unsigned i0) np) = (bs4, ne4)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc5´: ZMap.get 5 (ZMap.set 2 (bs2, Int.unsigned i0) np) = (bs5, ne5)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc6´: ZMap.get 6 (ZMap.set 2 (bs2, Int.unsigned i0) np) = (bs6, ne6)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc7´: ZMap.get 7 (ZMap.set 2 (bs2, Int.unsigned i0) np) = (bs7, ne7)).
                { rewrite ZMap.gso; try assumption; unfold not; intros 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´.
                rewrite Int.repr_unsigned 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_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´ & bs_6v´ & 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´).
              ∃ 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´, bs_6v´, ne6_v´, bs7_v´, ne7_v´.
              rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) 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 i) 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. }
          {
            destruct (zeq (Int.unsigned i) lock_index); subst.
            - ∃ la_v.
              ∃ bs0_v, ne0_v.
              ∃ bs1_v, ne1_v.
              ∃ bs2_v, ne2_v.
              ∃ bs3_v, (Vint i0).
              ∃ bs4_v, ne4_v.
              ∃ bs5_v, ne5_v.
              ∃ bs6_v, ne6_v.
              ∃ bs7_v, ne7_v.
              refine_split´; eauto; try (repeat (eapply Mem.store_valid_access_1; eauto));
              try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST); auto;
                   try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                   try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail).
              + unfold next_pos in HST; unfold next_pos; erewrite Mem.load_store_same; eauto; trivial.
              + rewrite ZMap.gss.
                rewrite Hdestruct4 in Hm; inv Hm.
                assert (Hcal´: CalMCSLock (TEVENT (Int.unsigned i0) (TTICKET (SET_NEXT 3)) :: l)
                               = Some (MCSLOCK la (ZMap.set 3 (bs3, (Int.unsigned i0)) np) tq)).
                { Transparent CalMCSLock.
                  simpl.
                  rewrite Hcal; rewrite Hnc3; reflexivity. }
                assert (Hnc0´: ZMap.get 0 (ZMap.set 3 (bs3, Int.unsigned i0) np) = (bs0, ne0)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc1´: ZMap.get 1 (ZMap.set 3 (bs3, Int.unsigned i0) np) = (bs1, ne1)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc2´: ZMap.get 2 (ZMap.set 3 (bs3, Int.unsigned i0) np) = (bs2, ne2)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc3´: ZMap.get 3 (ZMap.set 3 (bs3, Int.unsigned i0) np) = (bs3, Int.unsigned i0)).
                { rewrite ZMap.gss; reflexivity. }
                assert (Hnc4´: ZMap.get 4 (ZMap.set 3 (bs3, Int.unsigned i0) np) = (bs4, ne4)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc5´: ZMap.get 5 (ZMap.set 3 (bs3, Int.unsigned i0) np) = (bs5, ne5)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc6´: ZMap.get 6 (ZMap.set 3 (bs3, Int.unsigned i0) np) = (bs6, ne6)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc7´: ZMap.get 7 (ZMap.set 3 (bs3, Int.unsigned i0) np) = (bs7, ne7)).
                { rewrite ZMap.gso; try assumption; unfold not; intros 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´.
                rewrite Int.repr_unsigned 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_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´ & bs_6v´ & 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´).
              ∃ 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´, bs_6v´, ne6_v´, bs7_v´, ne7_v´.
              rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) 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 i) 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. }
          {
            destruct (zeq (Int.unsigned i) lock_index); subst.
            - ∃ la_v.
              ∃ bs0_v, ne0_v.
              ∃ bs1_v, ne1_v.
              ∃ bs2_v, ne2_v.
              ∃ bs3_v, ne3_v.
              ∃ bs4_v, (Vint i0).
              ∃ bs5_v, ne5_v.
              ∃ bs6_v, ne6_v.
              ∃ bs7_v, ne7_v.
              refine_split´; eauto; try (repeat (eapply Mem.store_valid_access_1; eauto));
              try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST); auto;
                   try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                   try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail).
              + unfold next_pos in HST; unfold next_pos; erewrite Mem.load_store_same; eauto; trivial.
              + rewrite ZMap.gss.
                rewrite Hdestruct4 in Hm; inv Hm.
                assert (Hcal´: CalMCSLock (TEVENT (Int.unsigned i0) (TTICKET (SET_NEXT 4)) :: l)
                               = Some (MCSLOCK la (ZMap.set 4 (bs4, (Int.unsigned i0)) np) tq)).
                { Transparent CalMCSLock.
                  simpl.
                  rewrite Hcal; rewrite Hnc4; reflexivity. }
                assert (Hnc0´: ZMap.get 0 (ZMap.set 4 (bs4, Int.unsigned i0) np) = (bs0, ne0)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc1´: ZMap.get 1 (ZMap.set 4 (bs4, Int.unsigned i0) np) = (bs1, ne1)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc2´: ZMap.get 2 (ZMap.set 4 (bs4, Int.unsigned i0) np) = (bs2, ne2)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc3´: ZMap.get 3 (ZMap.set 4 (bs4, Int.unsigned i0) np) = (bs3, ne3)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc4´: ZMap.get 4 (ZMap.set 4 (bs4, Int.unsigned i0) np) = (bs4, Int.unsigned i0)).
                { rewrite ZMap.gss; reflexivity. }
                assert (Hnc5´: ZMap.get 5 (ZMap.set 4 (bs4, Int.unsigned i0) np) = (bs5, ne5)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc6´: ZMap.get 6 (ZMap.set 4 (bs4, Int.unsigned i0) np) = (bs6, ne6)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc7´: ZMap.get 7 (ZMap.set 4 (bs4, Int.unsigned i0) np) = (bs7, ne7)).
                { rewrite ZMap.gso; try assumption; unfold not; intros 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´.
                rewrite Int.repr_unsigned 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_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´ & bs_6v´ & 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´).
              ∃ 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´, bs_6v´, ne6_v´, bs7_v´, ne7_v´.
              rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) 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 i) 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. }
          {
            destruct (zeq (Int.unsigned i) lock_index); subst.
            - ∃ la_v.
              ∃ bs0_v, ne0_v.
              ∃ bs1_v, ne1_v.
              ∃ bs2_v, ne2_v.
              ∃ bs3_v, ne3_v.
              ∃ bs4_v, ne4_v.
              ∃ bs5_v, (Vint i0).
              ∃ bs6_v, ne6_v.
              ∃ bs7_v, ne7_v.
              refine_split´; eauto; try (repeat (eapply Mem.store_valid_access_1; eauto));
              try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST); auto;
                   try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                   try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail).
              + unfold next_pos in HST; unfold next_pos; erewrite Mem.load_store_same; eauto; trivial.
              + rewrite ZMap.gss.
                rewrite Hdestruct4 in Hm; inv Hm.
                assert (Hcal´: CalMCSLock (TEVENT (Int.unsigned i0) (TTICKET (SET_NEXT 5)) :: l)
                               = Some (MCSLOCK la (ZMap.set 5 (bs5, (Int.unsigned i0)) np) tq)).
                { Transparent CalMCSLock.
                  simpl.
                  rewrite Hcal; rewrite Hnc5; reflexivity. }
                assert (Hnc0´: ZMap.get 0 (ZMap.set 5 (bs5, Int.unsigned i0) np) = (bs0, ne0)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc1´: ZMap.get 1 (ZMap.set 5 (bs5, Int.unsigned i0) np) = (bs1, ne1)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc2´: ZMap.get 2 (ZMap.set 5 (bs5, Int.unsigned i0) np) = (bs2, ne2)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc3´: ZMap.get 3 (ZMap.set 5 (bs5, Int.unsigned i0) np) = (bs3, ne3)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc4´: ZMap.get 4 (ZMap.set 5 (bs5, Int.unsigned i0) np) = (bs4, ne4)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc5´: ZMap.get 5 (ZMap.set 5 (bs5, Int.unsigned i0) np) = (bs5, Int.unsigned i0)).
                { rewrite ZMap.gss; reflexivity. }
                assert (Hnc6´: ZMap.get 6 (ZMap.set 5 (bs5, Int.unsigned i0) np) = (bs6, ne6)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc7´: ZMap.get 7 (ZMap.set 5 (bs5, Int.unsigned i0) np) = (bs7, ne7)).
                { rewrite ZMap.gso; try assumption; unfold not; intros 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´.
                rewrite Int.repr_unsigned 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_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´ & bs_6v´ & 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´).
              ∃ 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´, bs_6v´, ne6_v´, bs7_v´, ne7_v´.
              rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) 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 i) 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. }
          {
            destruct (zeq (Int.unsigned i) lock_index); subst.
            - ∃ 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, (Vint i0).
              ∃ bs7_v, ne7_v.
              refine_split´; eauto; try (repeat (eapply Mem.store_valid_access_1; eauto));
              try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST); auto;
                   try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                   try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail).
              + unfold next_pos in HST; unfold next_pos; erewrite Mem.load_store_same; eauto; trivial.
              + rewrite ZMap.gss.
                rewrite Hdestruct4 in Hm; inv Hm.
                assert (Hcal´: CalMCSLock (TEVENT (Int.unsigned i0) (TTICKET (SET_NEXT 6)) :: l)
                               = Some (MCSLOCK la (ZMap.set 6 (bs6, (Int.unsigned i0)) np) tq)).
                { Transparent CalMCSLock.
                  simpl.
                  rewrite Hcal; rewrite Hnc6; reflexivity. }
                assert (Hnc0´: ZMap.get 0 (ZMap.set 6 (bs6, Int.unsigned i0) np) = (bs0, ne0)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc1´: ZMap.get 1 (ZMap.set 6 (bs6, Int.unsigned i0) np) = (bs1, ne1)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc2´: ZMap.get 2 (ZMap.set 6 (bs6, Int.unsigned i0) np) = (bs2, ne2)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc3´: ZMap.get 3 (ZMap.set 6 (bs6, Int.unsigned i0) np) = (bs3, ne3)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc4´: ZMap.get 4 (ZMap.set 6 (bs6, Int.unsigned i0) np) = (bs4, ne4)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc5´: ZMap.get 5 (ZMap.set 6 (bs6, Int.unsigned i0) np) = (bs5, ne5)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc6´: ZMap.get 6 (ZMap.set 6 (bs6, Int.unsigned i0) np) = (bs6, Int.unsigned i0)).
                { rewrite ZMap.gss; reflexivity. }
                assert (Hnc7´: ZMap.get 7 (ZMap.set 6 (bs6, Int.unsigned i0) np) = (bs7, ne7)).
                { rewrite ZMap.gso; try assumption; unfold not; intros 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´.
                rewrite Int.repr_unsigned 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_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´ & bs_6v´ & 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´).
              ∃ 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´, bs_6v´, ne6_v´, bs7_v´, ne7_v´.
              rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) 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 i) 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. }
          {
            destruct (zeq (Int.unsigned i) lock_index); subst.
            - ∃ 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, (Vint i0).
              refine_split´; eauto; try (repeat (eapply Mem.store_valid_access_1; eauto));
              try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST); auto;
                   try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                   try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail).
              + unfold next_pos in HST; unfold next_pos; erewrite Mem.load_store_same; eauto; trivial.
              + rewrite ZMap.gss.
                rewrite Hdestruct4 in Hm; inv Hm.
                assert (Hcal´: CalMCSLock (TEVENT (Int.unsigned i0) (TTICKET (SET_NEXT 7)) :: l)
                               = Some (MCSLOCK la (ZMap.set 7 (bs7, (Int.unsigned i0)) np) tq)).
                { Transparent CalMCSLock.
                  simpl.
                  rewrite Hcal; rewrite Hnc7; reflexivity. }
                assert (Hnc0´: ZMap.get 0 (ZMap.set 7 (bs7, Int.unsigned i0) np) = (bs0, ne0)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc1´: ZMap.get 1 (ZMap.set 7 (bs7, Int.unsigned i0) np) = (bs1, ne1)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc2´: ZMap.get 2 (ZMap.set 7 (bs7, Int.unsigned i0) np) = (bs2, ne2)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc3´: ZMap.get 3 (ZMap.set 7 (bs7, Int.unsigned i0) np) = (bs3, ne3)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc4´: ZMap.get 4 (ZMap.set 7 (bs7, Int.unsigned i0) np) = (bs4, ne4)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc5´: ZMap.get 5 (ZMap.set 7 (bs7, Int.unsigned i0) np) = (bs5, ne5)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc6´: ZMap.get 6 (ZMap.set 7 (bs7, Int.unsigned i0) np) = (bs6, ne6)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc7´: ZMap.get 7 (ZMap.set 7 (bs7, Int.unsigned i0) np) = (bs7, Int.unsigned i0)).
                { 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´.
                rewrite Int.repr_unsigned 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_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´ & bs_6v´ & 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´).
              ∃ 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´, bs_6v´, ne6_v´, bs7_v´, ne7_v´.
              rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) 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 i) 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. }
        - apply inject_incr_refl.
      Qed.

    End mcs_SET_NEXT_ref.

    Section mcs_GET_BUSY_ref.

      Lemma mcs_GET_BUSY_spec_ref:
        compatsim (crel HDATA LDATA) (gensem mcs_GET_BUSY_spec) mcs_GET_BUSY_spec_low.
      Proof.
        compatsim_simpl (@match_AbData).
        assert (Hkern: kernel_mode d2).
        { inv match_related.
          unfold mcs_GET_BUSY_spec in *; subdestruct;
          repeat (split; congruence); eauto. }
        inv Hlog.
        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_GET_BUSY_spec.
        subrewrite´.
        intros ? HQ.
        subdestruct.
        {
          inv HQ.
          pose proof HMCSLock as HMCSLock´.
          specialize (HMCSLock _ a).
          rewrite multi_log_re in HMCSLock.
          assert (i0_vals: Int.unsigned i0 = 0 ∨ Int.unsigned i0 = 1 ∨ Int.unsigned i0 = 2 ∨ Int.unsigned i0 = 3 ∨
                           Int.unsigned i0 = 4 ∨ Int.unsigned i0 = 5 ∨ Int.unsigned i0 = 6 ∨ Int.unsigned i0 = 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 & bs_6v & 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).
          inv Hm; [rewrite Hdestruct3 in H0; inv H0 | ].
          rewrite Hdestruct3 in H0.
          inv H0.
          rewrite Hdestruct4 in Hcal.
          inv Hcal.
          destruct i0_vals as [i00 | [i01 | [i02 | [i03 | [i04 | [i05 | [i06 | i07]]]]]]].
          - rewrite i00 in *; refine_split.
            + econstructor; eauto.
              × unfold mcs_GET_BUSY_log_spec; subrewrite´.
              × rewrite i00; eassumption.
            + rewrite Hnc0 in Hdestruct6; inv Hdestruct6.
              simpl; rewrite H1; rewrite Int.repr_unsigned; constructor.
            + split; eauto; pattern2_refinement_simpl; trivial; try (rewrite <- H1; auto).
              econstructor; simpl; eauto.
              econstructor; eauto; intros.
              destruct (zeq (Int.unsigned i) lock_index); subst.
              { ∃ (Vint (Int.repr la)).
                ∃ (Vint (Int.repr (BooltoZ bs0))), (Vint (Int.repr ne0)).
                ∃ (Vint (Int.repr (BooltoZ bs1))), (Vint (Int.repr ne1)).
                ∃ (Vint (Int.repr (BooltoZ bs2))), (Vint (Int.repr ne2)).
                ∃ (Vint (Int.repr (BooltoZ bs3))), (Vint (Int.repr ne3)).
                ∃ (Vint (Int.repr (BooltoZ bs4))), (Vint (Int.repr ne4)).
                ∃ (Vint (Int.repr (BooltoZ bs5))), (Vint (Int.repr ne5)).
                ∃ (Vint (Int.repr (BooltoZ bs6))), (Vint (Int.repr ne6)).
                ∃ (Vint (Int.repr (BooltoZ bs7))), (Vint (Int.repr ne7)).
                refine_split; eauto.
                rewrite ZMap.gss.
                Transparent CalMCSLock.
                econstructor; try (simpl; rewrite Hdestruct4; reflexivity); try 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_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´ & bs_6v´ & 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´).
                ∃ 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´, bs_6v´, ne6_v´, bs7_v´, ne7_v´.
                try (simpl; right; destruct (zle (Int.unsigned i) lock_index);
                     [right; unfold next_pos, busy_pos, tail_pos; omega | left; unfold next_pos, busy_pos, tail_pos; omega]).
                refine_split´; trivial.
                rewrite ZMap.gso; auto.
                rewrite <- multi_log_re.
                trivial. }
            + apply inject_incr_refl.
          - rewrite i01 in *; refine_split.
            + econstructor; eauto.
              × unfold mcs_GET_BUSY_log_spec; subrewrite´.
              × rewrite i01; eassumption.
            + rewrite Hnc1 in Hdestruct6; inv Hdestruct6.
              simpl; rewrite H1; rewrite Int.repr_unsigned; constructor.
            + split; eauto; pattern2_refinement_simpl; trivial; try (rewrite <- H1; auto).
              econstructor; simpl; eauto.
              econstructor; eauto; intros.
              destruct (zeq (Int.unsigned i) lock_index); subst.
              { ∃ (Vint (Int.repr la)).
                ∃ (Vint (Int.repr (BooltoZ bs0))), (Vint (Int.repr ne0)).
                ∃ (Vint (Int.repr (BooltoZ bs1))), (Vint (Int.repr ne1)).
                ∃ (Vint (Int.repr (BooltoZ bs2))), (Vint (Int.repr ne2)).
                ∃ (Vint (Int.repr (BooltoZ bs3))), (Vint (Int.repr ne3)).
                ∃ (Vint (Int.repr (BooltoZ bs4))), (Vint (Int.repr ne4)).
                ∃ (Vint (Int.repr (BooltoZ bs5))), (Vint (Int.repr ne5)).
                ∃ (Vint (Int.repr (BooltoZ bs6))), (Vint (Int.repr ne6)).
                ∃ (Vint (Int.repr (BooltoZ bs7))), (Vint (Int.repr ne7)).
                refine_split; eauto.
                rewrite ZMap.gss.
                econstructor; try (simpl; rewrite Hdestruct4; reflexivity); 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_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´ & bs_6v´ & 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´).
                ∃ 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´, bs_6v´, ne6_v´, bs7_v´, ne7_v´.
                try (simpl; right; destruct (zle (Int.unsigned i) lock_index);
                     [right; unfold next_pos, busy_pos, tail_pos; omega | left; unfold next_pos, busy_pos, tail_pos; omega]).
                refine_split´; trivial.
                rewrite ZMap.gso; auto.
                rewrite <- multi_log_re.
                trivial. }
            + apply inject_incr_refl.
          - rewrite i02 in *; refine_split.
            + econstructor; eauto.
              × unfold mcs_GET_BUSY_log_spec; subrewrite´.
              × rewrite i02; eassumption.
            + rewrite Hnc2 in Hdestruct6; inv Hdestruct6.
              simpl; rewrite H1; rewrite Int.repr_unsigned; constructor.
            + split; eauto; pattern2_refinement_simpl; trivial; try (rewrite <- H1; auto).
              econstructor; simpl; eauto.
              econstructor; eauto; intros.
              destruct (zeq (Int.unsigned i) lock_index); subst.
              { ∃ (Vint (Int.repr la)).
                ∃ (Vint (Int.repr (BooltoZ bs0))), (Vint (Int.repr ne0)).
                ∃ (Vint (Int.repr (BooltoZ bs1))), (Vint (Int.repr ne1)).
                ∃ (Vint (Int.repr (BooltoZ bs2))), (Vint (Int.repr ne2)).
                ∃ (Vint (Int.repr (BooltoZ bs3))), (Vint (Int.repr ne3)).
                ∃ (Vint (Int.repr (BooltoZ bs4))), (Vint (Int.repr ne4)).
                ∃ (Vint (Int.repr (BooltoZ bs5))), (Vint (Int.repr ne5)).
                ∃ (Vint (Int.repr (BooltoZ bs6))), (Vint (Int.repr ne6)).
                ∃ (Vint (Int.repr (BooltoZ bs7))), (Vint (Int.repr ne7)).
                refine_split; eauto.
                rewrite ZMap.gss.
                econstructor; try (simpl; rewrite Hdestruct4; reflexivity); 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_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´ & bs_6v´ & 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´).
                ∃ 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´, bs_6v´, ne6_v´, bs7_v´, ne7_v´.
                try (simpl; right; destruct (zle (Int.unsigned i) lock_index);
                     [right; unfold next_pos, busy_pos, tail_pos; omega | left; unfold next_pos, busy_pos, tail_pos; omega]).
                refine_split´; trivial.
                rewrite ZMap.gso; auto.
                rewrite <- multi_log_re.
                trivial. }
            + apply inject_incr_refl.
          - rewrite i03 in *; refine_split.
            + econstructor; eauto.
              × unfold mcs_GET_BUSY_log_spec; subrewrite´.
              × rewrite i03; eassumption.
            + rewrite Hnc3 in Hdestruct6; inv Hdestruct6.
              simpl; rewrite H1; rewrite Int.repr_unsigned; constructor.
            + split; eauto; pattern2_refinement_simpl; trivial; try (rewrite <- H1; auto).
              econstructor; simpl; eauto.
              econstructor; eauto; intros.
              destruct (zeq (Int.unsigned i) lock_index); subst.
              { ∃ (Vint (Int.repr la)).
                ∃ (Vint (Int.repr (BooltoZ bs0))), (Vint (Int.repr ne0)).
                ∃ (Vint (Int.repr (BooltoZ bs1))), (Vint (Int.repr ne1)).
                ∃ (Vint (Int.repr (BooltoZ bs2))), (Vint (Int.repr ne2)).
                ∃ (Vint (Int.repr (BooltoZ bs3))), (Vint (Int.repr ne3)).
                ∃ (Vint (Int.repr (BooltoZ bs4))), (Vint (Int.repr ne4)).
                ∃ (Vint (Int.repr (BooltoZ bs5))), (Vint (Int.repr ne5)).
                ∃ (Vint (Int.repr (BooltoZ bs6))), (Vint (Int.repr ne6)).
                ∃ (Vint (Int.repr (BooltoZ bs7))), (Vint (Int.repr ne7)).
                refine_split; eauto.
                rewrite ZMap.gss.
                econstructor; try (simpl; rewrite Hdestruct4; reflexivity); 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_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´ & bs_6v´ & 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´).
                ∃ 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´, bs_6v´, ne6_v´, bs7_v´, ne7_v´.
                try (simpl; right; destruct (zle (Int.unsigned i) lock_index);
                     [right; unfold next_pos, busy_pos, tail_pos; omega | left; unfold next_pos, busy_pos, tail_pos; omega]).
                refine_split´; trivial.
                rewrite ZMap.gso; auto.
                rewrite <- multi_log_re.
                trivial. }
            + apply inject_incr_refl.
          - rewrite i04 in *; refine_split.
            + econstructor; eauto.
              × unfold mcs_GET_BUSY_log_spec; subrewrite´.
              × rewrite i04; eassumption.
            + rewrite Hnc4 in Hdestruct6; inv Hdestruct6.
              simpl; rewrite H1; rewrite Int.repr_unsigned; constructor.
            + split; eauto; pattern2_refinement_simpl; trivial; try (rewrite <- H1; auto).
              econstructor; simpl; eauto.
              econstructor; eauto; intros.
              destruct (zeq (Int.unsigned i) lock_index); subst.
              { ∃ (Vint (Int.repr la)).
                ∃ (Vint (Int.repr (BooltoZ bs0))), (Vint (Int.repr ne0)).
                ∃ (Vint (Int.repr (BooltoZ bs1))), (Vint (Int.repr ne1)).
                ∃ (Vint (Int.repr (BooltoZ bs2))), (Vint (Int.repr ne2)).
                ∃ (Vint (Int.repr (BooltoZ bs3))), (Vint (Int.repr ne3)).
                ∃ (Vint (Int.repr (BooltoZ bs4))), (Vint (Int.repr ne4)).
                ∃ (Vint (Int.repr (BooltoZ bs5))), (Vint (Int.repr ne5)).
                ∃ (Vint (Int.repr (BooltoZ bs6))), (Vint (Int.repr ne6)).
                ∃ (Vint (Int.repr (BooltoZ bs7))), (Vint (Int.repr ne7)).
                refine_split; eauto.
                rewrite ZMap.gss.
                econstructor; try (simpl; rewrite Hdestruct4; reflexivity); 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_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´ & bs_6v´ & 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´).
                ∃ 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´, bs_6v´, ne6_v´, bs7_v´, ne7_v´.
                try (simpl; right; destruct (zle (Int.unsigned i) lock_index);
                     [right; unfold next_pos, busy_pos, tail_pos; omega | left; unfold next_pos, busy_pos, tail_pos; omega]).
                refine_split´; trivial.
                rewrite ZMap.gso; auto.
                rewrite <- multi_log_re.
                trivial. }
            + apply inject_incr_refl.
          - rewrite i05 in *; refine_split.
            + econstructor; eauto.
              × unfold mcs_GET_BUSY_log_spec; subrewrite´.
              × rewrite i05; eassumption.
            + rewrite Hnc5 in Hdestruct6; inv Hdestruct6.
              simpl; rewrite H1; rewrite Int.repr_unsigned; constructor.
            + split; eauto; pattern2_refinement_simpl; trivial; try (rewrite <- H1; auto).
              econstructor; simpl; eauto.
              econstructor; eauto; intros.
              destruct (zeq (Int.unsigned i) lock_index); subst.
              { ∃ (Vint (Int.repr la)).
                ∃ (Vint (Int.repr (BooltoZ bs0))), (Vint (Int.repr ne0)).
                ∃ (Vint (Int.repr (BooltoZ bs1))), (Vint (Int.repr ne1)).
                ∃ (Vint (Int.repr (BooltoZ bs2))), (Vint (Int.repr ne2)).
                ∃ (Vint (Int.repr (BooltoZ bs3))), (Vint (Int.repr ne3)).
                ∃ (Vint (Int.repr (BooltoZ bs4))), (Vint (Int.repr ne4)).
                ∃ (Vint (Int.repr (BooltoZ bs5))), (Vint (Int.repr ne5)).
                ∃ (Vint (Int.repr (BooltoZ bs6))), (Vint (Int.repr ne6)).
                ∃ (Vint (Int.repr (BooltoZ bs7))), (Vint (Int.repr ne7)).
                refine_split; eauto.
                rewrite ZMap.gss.
                econstructor; try (simpl; rewrite Hdestruct4; reflexivity); 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_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´ & bs_6v´ & 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´).
                ∃ 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´, bs_6v´, ne6_v´, bs7_v´, ne7_v´.
                try (simpl; right; destruct (zle (Int.unsigned i) lock_index);
                     [right; unfold next_pos, busy_pos, tail_pos; omega | left; unfold next_pos, busy_pos, tail_pos; omega]).
                refine_split´; trivial.
                rewrite ZMap.gso; auto.
                rewrite <- multi_log_re.
                trivial. }
            + apply inject_incr_refl.
          - rewrite i06 in *; refine_split.
            + econstructor; eauto.
              × unfold mcs_GET_BUSY_log_spec; subrewrite´.
              × rewrite i06; eassumption.
            + rewrite Hnc6 in Hdestruct6; inv Hdestruct6.
              simpl; rewrite H1; rewrite Int.repr_unsigned; constructor.
            + split; eauto; pattern2_refinement_simpl; trivial; try (rewrite <- H1; auto).
              econstructor; simpl; eauto.
              econstructor; eauto; intros.
              destruct (zeq (Int.unsigned i) lock_index); subst.
              { ∃ (Vint (Int.repr la)).
                ∃ (Vint (Int.repr (BooltoZ bs0))), (Vint (Int.repr ne0)).
                ∃ (Vint (Int.repr (BooltoZ bs1))), (Vint (Int.repr ne1)).
                ∃ (Vint (Int.repr (BooltoZ bs2))), (Vint (Int.repr ne2)).
                ∃ (Vint (Int.repr (BooltoZ bs3))), (Vint (Int.repr ne3)).
                ∃ (Vint (Int.repr (BooltoZ bs4))), (Vint (Int.repr ne4)).
                ∃ (Vint (Int.repr (BooltoZ bs5))), (Vint (Int.repr ne5)).
                ∃ (Vint (Int.repr (BooltoZ bs6))), (Vint (Int.repr ne6)).
                ∃ (Vint (Int.repr (BooltoZ bs7))), (Vint (Int.repr ne7)).
                refine_split; eauto.
                rewrite ZMap.gss.
                econstructor; try (simpl; rewrite Hdestruct4; reflexivity); 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_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´ & bs_6v´ & 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´).
                ∃ 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´, bs_6v´, ne6_v´, bs7_v´, ne7_v´.
                try (simpl; right; destruct (zle (Int.unsigned i) lock_index);
                     [right; unfold next_pos, busy_pos, tail_pos; omega | left; unfold next_pos, busy_pos, tail_pos; omega]).
                refine_split´; trivial.
                rewrite ZMap.gso; auto.
                rewrite <- multi_log_re.
                trivial. }
            + apply inject_incr_refl.
          - rewrite i07 in *; refine_split.
            + econstructor; eauto.
              × unfold mcs_GET_BUSY_log_spec; subrewrite´.
              × rewrite i07; eassumption.
            + rewrite Hnc7 in Hdestruct6; inv Hdestruct6.
              simpl; rewrite H1; rewrite Int.repr_unsigned; constructor.
            + split; eauto; pattern2_refinement_simpl; trivial; try (rewrite <- H1; auto).
              econstructor; simpl; eauto.
              econstructor; eauto; intros.
              destruct (zeq (Int.unsigned i) lock_index); subst.
              { ∃ (Vint (Int.repr la)).
                ∃ (Vint (Int.repr (BooltoZ bs0))), (Vint (Int.repr ne0)).
                ∃ (Vint (Int.repr (BooltoZ bs1))), (Vint (Int.repr ne1)).
                ∃ (Vint (Int.repr (BooltoZ bs2))), (Vint (Int.repr ne2)).
                ∃ (Vint (Int.repr (BooltoZ bs3))), (Vint (Int.repr ne3)).
                ∃ (Vint (Int.repr (BooltoZ bs4))), (Vint (Int.repr ne4)).
                ∃ (Vint (Int.repr (BooltoZ bs5))), (Vint (Int.repr ne5)).
                ∃ (Vint (Int.repr (BooltoZ bs6))), (Vint (Int.repr ne6)).
                ∃ (Vint (Int.repr (BooltoZ bs7))), (Vint (Int.repr ne7)).
                refine_split; eauto.
                rewrite ZMap.gss.
                econstructor; try (simpl; rewrite Hdestruct4; reflexivity); 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_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´ & bs_6v´ & 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´).
                ∃ 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´, bs_6v´, ne6_v´, bs7_v´, ne7_v´.
                try (simpl; right; destruct (zle (Int.unsigned i) lock_index);
                     [right; unfold next_pos, busy_pos, tail_pos; omega | left; unfold next_pos, busy_pos, tail_pos; omega]).
                refine_split´; trivial.
                rewrite ZMap.gso; auto.
                rewrite <- multi_log_re.
                trivial. }
            + apply inject_incr_refl. }
        {
          inv HQ.
          pose proof HMCSLock as HMCSLock´.
          specialize (HMCSLock _ a).
          rewrite multi_log_re in HMCSLock.
          assert (i0_vals: Int.unsigned i0 = 0 ∨ Int.unsigned i0 = 1 ∨ Int.unsigned i0 = 2 ∨ Int.unsigned i0 = 3 ∨
                           Int.unsigned i0 = 4 ∨ Int.unsigned i0 = 5 ∨ Int.unsigned i0 = 6 ∨ Int.unsigned i0 = 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 & bs_6v & 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).
          inv Hm; [rewrite Hdestruct3 in H0; inv H0 | ].
          rewrite Hdestruct3 in H0.
          inv H0.
          rewrite Hdestruct4 in Hcal.
          inv Hcal.
          destruct i0_vals as [i00 | [i01 | [i02 | [i03 | [i04 | [i05 | [i06 | i07]]]]]]].
          - rewrite i00 in *; refine_split.
            + econstructor; eauto.
              × unfold mcs_GET_BUSY_log_spec; subrewrite´.
              × rewrite i00; eassumption.
            + rewrite Hnc0 in Hdestruct6; inv Hdestruct6.
              simpl; rewrite H1; rewrite Int.repr_unsigned; constructor.
            + split; eauto; pattern2_refinement_simpl; trivial; try (rewrite <- H1; auto).
              econstructor; simpl; eauto.
              econstructor; eauto; intros.
              destruct (zeq (Int.unsigned i) lock_index); subst.
              { ∃ (Vint (Int.repr la)).
                ∃ (Vint (Int.repr (BooltoZ bs0))), (Vint (Int.repr ne0)).
                ∃ (Vint (Int.repr (BooltoZ bs1))), (Vint (Int.repr ne1)).
                ∃ (Vint (Int.repr (BooltoZ bs2))), (Vint (Int.repr ne2)).
                ∃ (Vint (Int.repr (BooltoZ bs3))), (Vint (Int.repr ne3)).
                ∃ (Vint (Int.repr (BooltoZ bs4))), (Vint (Int.repr ne4)).
                ∃ (Vint (Int.repr (BooltoZ bs5))), (Vint (Int.repr ne5)).
                ∃ (Vint (Int.repr (BooltoZ bs6))), (Vint (Int.repr ne6)).
                ∃ (Vint (Int.repr (BooltoZ bs7))), (Vint (Int.repr ne7)).
                refine_split; eauto.
                rewrite ZMap.gss.
                econstructor; try (simpl; rewrite Hdestruct4; reflexivity); 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_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´ & bs_6v´ & 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´).
                ∃ 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´, bs_6v´, ne6_v´, bs7_v´, ne7_v´.
                try (simpl; right; destruct (zle (Int.unsigned i) lock_index);
                     [right; unfold next_pos, busy_pos, tail_pos; omega | left; unfold next_pos, busy_pos, tail_pos; omega]).
                refine_split´; trivial.
                rewrite ZMap.gso; auto.
                rewrite <- multi_log_re.
                trivial. }
            + apply inject_incr_refl.
          - rewrite i01 in *; refine_split.
            + econstructor; eauto.
              × unfold mcs_GET_BUSY_log_spec; subrewrite´.
              × rewrite i01; eassumption.
            + rewrite Hnc1 in Hdestruct6; inv Hdestruct6.
              simpl; rewrite H1; rewrite Int.repr_unsigned; constructor.
            + split; eauto; pattern2_refinement_simpl; trivial; try (rewrite <- H1; auto).
              econstructor; simpl; eauto.
              econstructor; eauto; intros.
              destruct (zeq (Int.unsigned i) lock_index); subst.
              { ∃ (Vint (Int.repr la)).
                ∃ (Vint (Int.repr (BooltoZ bs0))), (Vint (Int.repr ne0)).
                ∃ (Vint (Int.repr (BooltoZ bs1))), (Vint (Int.repr ne1)).
                ∃ (Vint (Int.repr (BooltoZ bs2))), (Vint (Int.repr ne2)).
                ∃ (Vint (Int.repr (BooltoZ bs3))), (Vint (Int.repr ne3)).
                ∃ (Vint (Int.repr (BooltoZ bs4))), (Vint (Int.repr ne4)).
                ∃ (Vint (Int.repr (BooltoZ bs5))), (Vint (Int.repr ne5)).
                ∃ (Vint (Int.repr (BooltoZ bs6))), (Vint (Int.repr ne6)).
                ∃ (Vint (Int.repr (BooltoZ bs7))), (Vint (Int.repr ne7)).
                refine_split; eauto.
                rewrite ZMap.gss.
                econstructor; try (simpl; rewrite Hdestruct4; reflexivity); 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_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´ & bs_6v´ & 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´).
                ∃ 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´, bs_6v´, ne6_v´, bs7_v´, ne7_v´.
                try (simpl; right; destruct (zle (Int.unsigned i) lock_index);
                     [right; unfold next_pos, busy_pos, tail_pos; omega | left; unfold next_pos, busy_pos, tail_pos; omega]).
                refine_split´; trivial.
                rewrite ZMap.gso; auto.
                rewrite <- multi_log_re.
                trivial. }
            + apply inject_incr_refl.
          - rewrite i02 in *; refine_split.
            + econstructor; eauto.
              × unfold mcs_GET_BUSY_log_spec; subrewrite´.
              × rewrite i02; eassumption.
            + rewrite Hnc2 in Hdestruct6; inv Hdestruct6.
              simpl; rewrite H1; rewrite Int.repr_unsigned; constructor.
            + split; eauto; pattern2_refinement_simpl; trivial; try (rewrite <- H1; auto).
              econstructor; simpl; eauto.
              econstructor; eauto; intros.
              destruct (zeq (Int.unsigned i) lock_index); subst.
              { ∃ (Vint (Int.repr la)).
                ∃ (Vint (Int.repr (BooltoZ bs0))), (Vint (Int.repr ne0)).
                ∃ (Vint (Int.repr (BooltoZ bs1))), (Vint (Int.repr ne1)).
                ∃ (Vint (Int.repr (BooltoZ bs2))), (Vint (Int.repr ne2)).
                ∃ (Vint (Int.repr (BooltoZ bs3))), (Vint (Int.repr ne3)).
                ∃ (Vint (Int.repr (BooltoZ bs4))), (Vint (Int.repr ne4)).
                ∃ (Vint (Int.repr (BooltoZ bs5))), (Vint (Int.repr ne5)).
                ∃ (Vint (Int.repr (BooltoZ bs6))), (Vint (Int.repr ne6)).
                ∃ (Vint (Int.repr (BooltoZ bs7))), (Vint (Int.repr ne7)).
                refine_split; eauto.
                rewrite ZMap.gss.
                econstructor; try (simpl; rewrite Hdestruct4; reflexivity); 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_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´ & bs_6v´ & 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´).
                ∃ 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´, bs_6v´, ne6_v´, bs7_v´, ne7_v´.
                try (simpl; right; destruct (zle (Int.unsigned i) lock_index);
                     [right; unfold next_pos, busy_pos, tail_pos; omega | left; unfold next_pos, busy_pos, tail_pos; omega]).
                refine_split´; trivial.
                rewrite ZMap.gso; auto.
                rewrite <- multi_log_re.
                trivial. }
            + apply inject_incr_refl.
          - rewrite i03 in *; refine_split.
            + econstructor; eauto.
              × unfold mcs_GET_BUSY_log_spec; subrewrite´.
              × rewrite i03; eassumption.
            + rewrite Hnc3 in Hdestruct6; inv Hdestruct6.
              simpl; rewrite H1; rewrite Int.repr_unsigned; constructor.
            + split; eauto; pattern2_refinement_simpl; trivial; try (rewrite <- H1; auto).
              econstructor; simpl; eauto.
              econstructor; eauto; intros.
              destruct (zeq (Int.unsigned i) lock_index); subst.
              { ∃ (Vint (Int.repr la)).
                ∃ (Vint (Int.repr (BooltoZ bs0))), (Vint (Int.repr ne0)).
                ∃ (Vint (Int.repr (BooltoZ bs1))), (Vint (Int.repr ne1)).
                ∃ (Vint (Int.repr (BooltoZ bs2))), (Vint (Int.repr ne2)).
                ∃ (Vint (Int.repr (BooltoZ bs3))), (Vint (Int.repr ne3)).
                ∃ (Vint (Int.repr (BooltoZ bs4))), (Vint (Int.repr ne4)).
                ∃ (Vint (Int.repr (BooltoZ bs5))), (Vint (Int.repr ne5)).
                ∃ (Vint (Int.repr (BooltoZ bs6))), (Vint (Int.repr ne6)).
                ∃ (Vint (Int.repr (BooltoZ bs7))), (Vint (Int.repr ne7)).
                refine_split; eauto.
                rewrite ZMap.gss.
                econstructor; try (simpl; rewrite Hdestruct4; reflexivity); 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_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´ & bs_6v´ & 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´).
                ∃ 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´, bs_6v´, ne6_v´, bs7_v´, ne7_v´.
                try (simpl; right; destruct (zle (Int.unsigned i) lock_index);
                     [right; unfold next_pos, busy_pos, tail_pos; omega | left; unfold next_pos, busy_pos, tail_pos; omega]).
                refine_split´; trivial.
                rewrite ZMap.gso; auto.
                rewrite <- multi_log_re.
                trivial. }
            + apply inject_incr_refl.
          - rewrite i04 in *; refine_split.
            + econstructor; eauto.
              × unfold mcs_GET_BUSY_log_spec; subrewrite´.
              × rewrite i04; eassumption.
            + rewrite Hnc4 in Hdestruct6; inv Hdestruct6.
              simpl; rewrite H1; rewrite Int.repr_unsigned; constructor.
            + split; eauto; pattern2_refinement_simpl; trivial; try (rewrite <- H1; auto).
              econstructor; simpl; eauto.
              econstructor; eauto; intros.
              destruct (zeq (Int.unsigned i) lock_index); subst.
              { ∃ (Vint (Int.repr la)).
                ∃ (Vint (Int.repr (BooltoZ bs0))), (Vint (Int.repr ne0)).
                ∃ (Vint (Int.repr (BooltoZ bs1))), (Vint (Int.repr ne1)).
                ∃ (Vint (Int.repr (BooltoZ bs2))), (Vint (Int.repr ne2)).
                ∃ (Vint (Int.repr (BooltoZ bs3))), (Vint (Int.repr ne3)).
                ∃ (Vint (Int.repr (BooltoZ bs4))), (Vint (Int.repr ne4)).
                ∃ (Vint (Int.repr (BooltoZ bs5))), (Vint (Int.repr ne5)).
                ∃ (Vint (Int.repr (BooltoZ bs6))), (Vint (Int.repr ne6)).
                ∃ (Vint (Int.repr (BooltoZ bs7))), (Vint (Int.repr ne7)).
                refine_split; eauto.
                rewrite ZMap.gss.
                econstructor; try (simpl; rewrite Hdestruct4; reflexivity); 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_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´ & bs_6v´ & 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´).
                ∃ 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´, bs_6v´, ne6_v´, bs7_v´, ne7_v´.
                try (simpl; right; destruct (zle (Int.unsigned i) lock_index);
                     [right; unfold next_pos, busy_pos, tail_pos; omega | left; unfold next_pos, busy_pos, tail_pos; omega]).
                refine_split´; trivial.
                rewrite ZMap.gso; auto.
                rewrite <- multi_log_re.
                trivial. }
            + apply inject_incr_refl.
          - rewrite i05 in *; refine_split.
            + econstructor; eauto.
              × unfold mcs_GET_BUSY_log_spec; subrewrite´.
              × rewrite i05; eassumption.
            + rewrite Hnc5 in Hdestruct6; inv Hdestruct6.
              simpl; rewrite H1; rewrite Int.repr_unsigned; constructor.
            + split; eauto; pattern2_refinement_simpl; trivial; try (rewrite <- H1; auto).
              econstructor; simpl; eauto.
              econstructor; eauto; intros.
              destruct (zeq (Int.unsigned i) lock_index); subst.
              { ∃ (Vint (Int.repr la)).
                ∃ (Vint (Int.repr (BooltoZ bs0))), (Vint (Int.repr ne0)).
                ∃ (Vint (Int.repr (BooltoZ bs1))), (Vint (Int.repr ne1)).
                ∃ (Vint (Int.repr (BooltoZ bs2))), (Vint (Int.repr ne2)).
                ∃ (Vint (Int.repr (BooltoZ bs3))), (Vint (Int.repr ne3)).
                ∃ (Vint (Int.repr (BooltoZ bs4))), (Vint (Int.repr ne4)).
                ∃ (Vint (Int.repr (BooltoZ bs5))), (Vint (Int.repr ne5)).
                ∃ (Vint (Int.repr (BooltoZ bs6))), (Vint (Int.repr ne6)).
                ∃ (Vint (Int.repr (BooltoZ bs7))), (Vint (Int.repr ne7)).
                refine_split; eauto.
                rewrite ZMap.gss.
                econstructor; try (simpl; rewrite Hdestruct4; reflexivity); 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_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´ & bs_6v´ & 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´).
                ∃ 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´, bs_6v´, ne6_v´, bs7_v´, ne7_v´.
                try (simpl; right; destruct (zle (Int.unsigned i) lock_index);
                     [right; unfold next_pos, busy_pos, tail_pos; omega | left; unfold next_pos, busy_pos, tail_pos; omega]).
                refine_split´; trivial.
                rewrite ZMap.gso; auto.
                rewrite <- multi_log_re.
                trivial. }
            + apply inject_incr_refl.
          - rewrite i06 in *; refine_split.
            + econstructor; eauto.
              × unfold mcs_GET_BUSY_log_spec; subrewrite´.
              × rewrite i06; eassumption.
            + rewrite Hnc6 in Hdestruct6; inv Hdestruct6.
              simpl; rewrite H1; rewrite Int.repr_unsigned; constructor.
            + split; eauto; pattern2_refinement_simpl; trivial; try (rewrite <- H1; auto).
              econstructor; simpl; eauto.
              econstructor; eauto; intros.
              destruct (zeq (Int.unsigned i) lock_index); subst.
              { ∃ (Vint (Int.repr la)).
                ∃ (Vint (Int.repr (BooltoZ bs0))), (Vint (Int.repr ne0)).
                ∃ (Vint (Int.repr (BooltoZ bs1))), (Vint (Int.repr ne1)).
                ∃ (Vint (Int.repr (BooltoZ bs2))), (Vint (Int.repr ne2)).
                ∃ (Vint (Int.repr (BooltoZ bs3))), (Vint (Int.repr ne3)).
                ∃ (Vint (Int.repr (BooltoZ bs4))), (Vint (Int.repr ne4)).
                ∃ (Vint (Int.repr (BooltoZ bs5))), (Vint (Int.repr ne5)).
                ∃ (Vint (Int.repr (BooltoZ bs6))), (Vint (Int.repr ne6)).
                ∃ (Vint (Int.repr (BooltoZ bs7))), (Vint (Int.repr ne7)).
                refine_split; eauto.
                rewrite ZMap.gss.
                econstructor; try (simpl; rewrite Hdestruct4; reflexivity); 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_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´ & bs_6v´ & 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´).
                ∃ 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´, bs_6v´, ne6_v´, bs7_v´, ne7_v´.
                try (simpl; right; destruct (zle (Int.unsigned i) lock_index);
                     [right; unfold next_pos, busy_pos, tail_pos; omega | left; unfold next_pos, busy_pos, tail_pos; omega]).
                refine_split´; trivial.
                rewrite ZMap.gso; auto.
                rewrite <- multi_log_re.
                trivial. }
            + apply inject_incr_refl.
          - rewrite i07 in *; refine_split.
            + econstructor; eauto.
              × unfold mcs_GET_BUSY_log_spec; subrewrite´.
              × rewrite i07; eassumption.
            + rewrite Hnc7 in Hdestruct6; inv Hdestruct6.
              simpl; rewrite H1; rewrite Int.repr_unsigned; constructor.
            + split; eauto; pattern2_refinement_simpl; trivial; try (rewrite <- H1; auto).
              econstructor; simpl; eauto.
              econstructor; eauto; intros.
              destruct (zeq (Int.unsigned i) lock_index); subst.
              { ∃ (Vint (Int.repr la)).
                ∃ (Vint (Int.repr (BooltoZ bs0))), (Vint (Int.repr ne0)).
                ∃ (Vint (Int.repr (BooltoZ bs1))), (Vint (Int.repr ne1)).
                ∃ (Vint (Int.repr (BooltoZ bs2))), (Vint (Int.repr ne2)).
                ∃ (Vint (Int.repr (BooltoZ bs3))), (Vint (Int.repr ne3)).
                ∃ (Vint (Int.repr (BooltoZ bs4))), (Vint (Int.repr ne4)).
                ∃ (Vint (Int.repr (BooltoZ bs5))), (Vint (Int.repr ne5)).
                ∃ (Vint (Int.repr (BooltoZ bs6))), (Vint (Int.repr ne6)).
                ∃ (Vint (Int.repr (BooltoZ bs7))), (Vint (Int.repr ne7)).
                refine_split; eauto.
                rewrite ZMap.gss.
                econstructor; try (simpl; rewrite Hdestruct4; reflexivity); 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_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´ & bs_6v´ & 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´).
                ∃ 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´, bs_6v´, ne6_v´, bs7_v´, ne7_v´.
                try (simpl; right; destruct (zle (Int.unsigned i) lock_index);
                     [right; unfold next_pos, busy_pos, tail_pos; omega | left; unfold next_pos, busy_pos, tail_pos; omega]).
                refine_split´; trivial.
                rewrite ZMap.gso; auto.
                rewrite <- multi_log_re.
                trivial. }
            + apply inject_incr_refl. }
      Qed.

    End mcs_GET_BUSY_ref.

    Section mcs_SET_BUSY_ref.

      Lemma mcs_SET_BUSY_spec_ref:
        compatsim (crel HDATA LDATA) (gensem mcs_SET_BUSY_spec) mcs_SET_BUSY_spec_low.
      Proof.
        compatsim_simpl (@match_AbData).
        assert (Hkern: kernel_mode d2).
        { inv match_related.
          unfold mcs_SET_BUSY_spec in *; subdestruct;
          repeat (split; congruence); eauto. }
        inv Hlog.
        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_SET_BUSY_spec.
        subrewrite´.
        intros ? HQ.
        subdestruct.
        inv HQ.
        pose proof HMCSLock as HMCSLock´.
        specialize (HMCSLock _ a).
        rewrite multi_log_re in HMCSLock.
        rename z into i0_ne.
        assert (i0_ne_vals: i0_ne = 0 ∨ i0_ne = 1 ∨ i0_ne = 2 ∨ i0_ne = 3 ∨
                            i0_ne = 4 ∨ i0_ne = 5 ∨ i0_ne = 6 ∨ i0_ne = 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 (HLoad: Mem.load Mint32 m2 b (next_pos (Int.unsigned i) (Int.unsigned i0)) = Some (Vint (Int.repr i0_ne))).
        { inv Hm.
          - rewrite Hdestruct3 in H0; inversion H0.
          - rewrite Hdestruct3 in H0; inv H0.
            rewrite Hdestruct4 in Hcal; inv Hcal.
            assert (i0_vals: Int.unsigned i0 = 0 ∨ Int.unsigned i0 = 1 ∨ Int.unsigned i0 = 2 ∨ Int.unsigned i0 = 3 ∨
                             Int.unsigned i0 = 4 ∨ Int.unsigned i0 = 5 ∨ Int.unsigned i0 = 6 ∨ Int.unsigned i0 = 7).
            { omega. }
            destruct i0_vals as [i00 | [i01 | [i02 | [i03 | [i04 | [i05 | [i06 | i07]]]]]]].
            + rewrite i00; rewrite i00 in Hdestruct6; rewrite Hnc0 in Hdestruct6; inv Hdestruct6.
              unfold next_pos in HL__ne0; assumption.
            + rewrite i01; rewrite i01 in Hdestruct6; rewrite Hnc1 in Hdestruct6; inv Hdestruct6.
              unfold next_pos in HL__ne1; assumption.
            + rewrite i02; rewrite i02 in Hdestruct6; rewrite Hnc2 in Hdestruct6; inv Hdestruct6.
              unfold next_pos in HL__ne2; assumption.
            + rewrite i03; rewrite i03 in Hdestruct6; rewrite Hnc3 in Hdestruct6; inv Hdestruct6.
              unfold next_pos in HL__ne3; assumption.
            + rewrite i04; rewrite i04 in Hdestruct6; rewrite Hnc4 in Hdestruct6; inv Hdestruct6.
              unfold next_pos in HL__ne4; assumption.
            + rewrite i05; rewrite i05 in Hdestruct6; rewrite Hnc5 in Hdestruct6; inv Hdestruct6.
              unfold next_pos in HL__ne5; assumption.
            + rewrite i06; rewrite i06 in Hdestruct6; rewrite Hnc6 in Hdestruct6; inv Hdestruct6.
              unfold next_pos in HL__ne6; assumption.
            + rewrite i07; rewrite i07 in Hdestruct6; rewrite Hnc7 in Hdestruct6; inv Hdestruct6.
              unfold next_pos in HL__ne7; assumption. }
        assert (HST: ∃ m´, Mem.store Mint32 m2 b (busy_pos (Int.unsigned i) i0_ne) Vzero = Some m´).
        { eapply Mem.valid_access_store; eauto.
          destruct i0_ne_vals as [i0_ne_v | [i0_ne_v | [i0_ne_v | [i0_ne_v |
                                                                   [i0_ne_v | [i0_ne_v | [i0_ne_v | i0_ne_v]]]]]]];
            rewrite i0_ne_v; assumption. }
        destruct HST as (m´ & HST).
        refine_split.
        - eapply mcs_SET_BUSY_spec_low_intro.
          + eauto.
          + eauto.
          + eauto.
          + instantiate (1:= (Int.repr i0_ne)).
            generalize max_unsigned_val; intros muval.
            rewrite Int.unsigned_repr; try omega.
          + unfold mcs_SET_BUSY_log_spec.
            subrewrite´.
          + assumption.
          + generalize max_unsigned_val; intros muval.
            rewrite Int.unsigned_repr; try omega.
            eassumption.
          + eauto.
        - econstructor.
        - split; eauto; pattern2_refinement_simpl; trivial.
          econstructor; simpl; eauto.
          econstructor; eauto; intros.
          destruct i0_ne_vals as [i0_ne_v | [i0_ne_v | [i0_ne_v | [i0_ne_v |
                                                                   [i0_ne_v | [i0_ne_v | [i0_ne_v | i0_ne_v]]]]]]].
          {
            destruct (zeq (Int.unsigned i) lock_index); subst.
            - ∃ la_v.
              ∃ Vzero, 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.
              refine_split´; eauto; try (repeat (eapply Mem.store_valid_access_1; eauto));
              try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST); auto;
                   try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                   try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail).
              + unfold next_pos in HST; unfold next_pos; erewrite Mem.load_store_same; eauto; trivial.
              + rewrite ZMap.gss.
                rewrite Hdestruct3 in Hm; inv Hm.
                rewrite Hcal in Hdestruct4; inv Hdestruct4.
                assert (Hcal´: CalMCSLock (TEVENT (Int.unsigned i0) (TTICKET SET_BUSY) :: l)
                               = Some (MCSLOCK tail (ZMap.set 0 (false, ne0) lock_array) (tl bounds))).
                { Transparent CalMCSLock.
                  simpl.
                  rewrite Hcal; rewrite Hdestruct6; rewrite Hnc0; reflexivity. }
                assert (Hnc0´: ZMap.get 0 (ZMap.set 0 (false, ne0) lock_array) = (false, ne0)).
                { rewrite ZMap.gss; reflexivity. }
                assert (Hnc1´: ZMap.get 1 (ZMap.set 0 (false, ne0) lock_array) = (bs1, ne1)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc2´: ZMap.get 2 (ZMap.set 0 (false, ne0) lock_array) = (bs2, ne2)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc3´: ZMap.get 3 (ZMap.set 0 (false, ne0) lock_array) = (bs3, ne3)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc4´: ZMap.get 4 (ZMap.set 0 (false, ne0) lock_array) = (bs4, ne4)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc5´: ZMap.get 5 (ZMap.set 0 (false, ne0) lock_array) = (bs5, ne5)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc6´: ZMap.get 6 (ZMap.set 0 (false, ne0) lock_array) = (bs6, ne6)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc7´: ZMap.get 7 (ZMap.set 0 (false, ne0) lock_array) = (bs7, ne7)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                unfold Vzero; unfold Int.zero.
                eapply MATCH_MCSLOCK_VALID with (2:= Hnc0´) (3:= Hnc1´) (4:= Hnc2´) (5:= Hnc3´) (6:= Hnc4´)
                                                            (7:= Hnc5´) (8:= Hnc6´) (9:= Hnc7´) in Hcal´.
                simpl 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_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´ & bs_6v´ & 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´).
              ∃ 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´, bs_6v´, ne6_v´, bs7_v´, ne7_v´.
              rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) 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 i) 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. }
          {
            destruct (zeq (Int.unsigned i) lock_index); subst.
            - ∃ la_v.
              ∃ bs0_v, ne0_v.
              ∃ Vzero, 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.
              refine_split´; eauto; try (repeat (eapply Mem.store_valid_access_1; eauto));
              try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST); auto;
                   try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                   try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail).
              + unfold next_pos in HST; unfold next_pos; erewrite Mem.load_store_same; eauto; trivial.
              + rewrite ZMap.gss.
                rewrite Hdestruct3 in Hm; inv Hm.
                rewrite Hcal in Hdestruct4; inv Hdestruct4.
                assert (Hcal´: CalMCSLock (TEVENT (Int.unsigned i0) (TTICKET SET_BUSY) :: l)
                               = Some (MCSLOCK tail (ZMap.set 1 (false, ne1) lock_array) (tl bounds))).
                { Transparent CalMCSLock.
                  simpl.
                  rewrite Hcal; rewrite Hdestruct6; rewrite Hnc1; reflexivity. }
                assert (Hnc0´: ZMap.get 0 (ZMap.set 1 (false, ne1) lock_array) = (bs0, ne0)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc1´: ZMap.get 1 (ZMap.set 1 (false, ne1) lock_array) = (false, ne1)).
                { rewrite ZMap.gss; reflexivity. }
                assert (Hnc2´: ZMap.get 2 (ZMap.set 1 (false, ne1) lock_array) = (bs2, ne2)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc3´: ZMap.get 3 (ZMap.set 1 (false, ne1) lock_array) = (bs3, ne3)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc4´: ZMap.get 4 (ZMap.set 1 (false, ne1) lock_array) = (bs4, ne4)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc5´: ZMap.get 5 (ZMap.set 1 (false, ne1) lock_array) = (bs5, ne5)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc6´: ZMap.get 6 (ZMap.set 1 (false, ne1) lock_array) = (bs6, ne6)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc7´: ZMap.get 7 (ZMap.set 1 (false, ne1) lock_array) = (bs7, ne7)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                unfold Vzero; unfold Int.zero.
                eapply MATCH_MCSLOCK_VALID with (2:= Hnc0´) (3:= Hnc1´) (4:= Hnc2´) (5:= Hnc3´) (6:= Hnc4´)
                                                            (7:= Hnc5´) (8:= Hnc6´) (9:= Hnc7´) in Hcal´.
                simpl 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_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´ & bs_6v´ & 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´).
              ∃ 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´, bs_6v´, ne6_v´, bs7_v´, ne7_v´.
              rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) 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 i) 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. }
          {
            destruct (zeq (Int.unsigned i) lock_index); subst.
            - ∃ la_v.
              ∃ bs0_v, ne0_v.
              ∃ bs1_v, ne1_v.
              ∃ Vzero, ne2_v.
              ∃ bs3_v, ne3_v.
              ∃ bs4_v, ne4_v.
              ∃ bs5_v, ne5_v.
              ∃ bs6_v, ne6_v.
              ∃ bs7_v, ne7_v.
              refine_split´; eauto; try (repeat (eapply Mem.store_valid_access_1; eauto));
              try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST); auto;
                   try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                   try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail).
              + unfold next_pos in HST; unfold next_pos; erewrite Mem.load_store_same; eauto; trivial.
              + rewrite ZMap.gss.
                rewrite Hdestruct3 in Hm; inv Hm.
                rewrite Hcal in Hdestruct4; inv Hdestruct4.
                assert (Hcal´: CalMCSLock (TEVENT (Int.unsigned i0) (TTICKET SET_BUSY) :: l)
                               = Some (MCSLOCK tail (ZMap.set 2 (false, ne2) lock_array) (tl bounds))).
                { Transparent CalMCSLock.
                  simpl.
                  rewrite Hcal; rewrite Hdestruct6; rewrite Hnc2; reflexivity. }
                assert (Hnc0´: ZMap.get 0 (ZMap.set 2 (false, ne2) lock_array) = (bs0, ne0)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc1´: ZMap.get 1 (ZMap.set 2 (false, ne2) lock_array) = (bs1, ne1)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc2´: ZMap.get 2 (ZMap.set 2 (false, ne2) lock_array) = (false, ne2)).
                { rewrite ZMap.gss; reflexivity. }
                assert (Hnc3´: ZMap.get 3 (ZMap.set 2 (false, ne2) lock_array) = (bs3, ne3)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc4´: ZMap.get 4 (ZMap.set 2 (false, ne2) lock_array) = (bs4, ne4)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc5´: ZMap.get 5 (ZMap.set 2 (false, ne2) lock_array) = (bs5, ne5)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc6´: ZMap.get 6 (ZMap.set 2 (false, ne2) lock_array) = (bs6, ne6)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc7´: ZMap.get 7 (ZMap.set 2 (false, ne2) lock_array) = (bs7, ne7)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                unfold Vzero; unfold Int.zero.
                eapply MATCH_MCSLOCK_VALID with (2:= Hnc0´) (3:= Hnc1´) (4:= Hnc2´) (5:= Hnc3´) (6:= Hnc4´)
                                                            (7:= Hnc5´) (8:= Hnc6´) (9:= Hnc7´) in Hcal´.
                simpl 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_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´ & bs_6v´ & 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´).
              ∃ 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´, bs_6v´, ne6_v´, bs7_v´, ne7_v´.
              rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) 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 i) 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. }
          {
            destruct (zeq (Int.unsigned i) lock_index); subst.
            - ∃ la_v.
              ∃ bs0_v, ne0_v.
              ∃ bs1_v, ne1_v.
              ∃ bs2_v, ne2_v.
              ∃ Vzero, ne3_v.
              ∃ bs4_v, ne4_v.
              ∃ bs5_v, ne5_v.
              ∃ bs6_v, ne6_v.
              ∃ bs7_v, ne7_v.
              refine_split´; eauto; try (repeat (eapply Mem.store_valid_access_1; eauto));
              try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST); auto;
                   try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                   try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail).
              + unfold next_pos in HST; unfold next_pos; erewrite Mem.load_store_same; eauto; trivial.
              + rewrite ZMap.gss.
                rewrite Hdestruct3 in Hm; inv Hm.
                rewrite Hcal in Hdestruct4; inv Hdestruct4.
                assert (Hcal´: CalMCSLock (TEVENT (Int.unsigned i0) (TTICKET SET_BUSY) :: l)
                               = Some (MCSLOCK tail (ZMap.set 3 (false, ne3) lock_array) (tl bounds))).
                { simpl; rewrite Hcal; rewrite Hdestruct6; rewrite Hnc3; reflexivity. }
                assert (Hnc0´: ZMap.get 0 (ZMap.set 3 (false, ne3) lock_array) = (bs0, ne0)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc1´: ZMap.get 1 (ZMap.set 3 (false, ne3) lock_array) = (bs1, ne1)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc2´: ZMap.get 2 (ZMap.set 3 (false, ne3) lock_array) = (bs2, ne2)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc3´: ZMap.get 3 (ZMap.set 3 (false, ne3) lock_array) = (false, ne3)).
                { rewrite ZMap.gss; reflexivity. }
                assert (Hnc4´: ZMap.get 4 (ZMap.set 3 (false, ne3) lock_array) = (bs4, ne4)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc5´: ZMap.get 5 (ZMap.set 3 (false, ne3) lock_array) = (bs5, ne5)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc6´: ZMap.get 6 (ZMap.set 3 (false, ne3) lock_array) = (bs6, ne6)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc7´: ZMap.get 7 (ZMap.set 3 (false, ne3) lock_array) = (bs7, ne7)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                unfold Vzero; unfold Int.zero.
                eapply MATCH_MCSLOCK_VALID with (2:= Hnc0´) (3:= Hnc1´) (4:= Hnc2´) (5:= Hnc3´) (6:= Hnc4´)
                                                            (7:= Hnc5´) (8:= Hnc6´) (9:= Hnc7´) in Hcal´.
                simpl 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_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´ & bs_6v´ & 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´).
              ∃ 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´, bs_6v´, ne6_v´, bs7_v´, ne7_v´.
              rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) 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 i) 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. }
          {
            destruct (zeq (Int.unsigned i) lock_index); subst.
            - ∃ la_v.
              ∃ bs0_v, ne0_v.
              ∃ bs1_v, ne1_v.
              ∃ bs2_v, ne2_v.
              ∃ bs3_v, ne3_v.
              ∃ Vzero, ne4_v.
              ∃ bs5_v, ne5_v.
              ∃ bs6_v, ne6_v.
              ∃ bs7_v, ne7_v.
              refine_split´; eauto; try (repeat (eapply Mem.store_valid_access_1; eauto));
              try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST); auto;
                   try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                   try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail).
              + unfold next_pos in HST;unfold next_pos; erewrite Mem.load_store_same; eauto; trivial.
              + rewrite ZMap.gss.
                rewrite Hdestruct3 in Hm; inv Hm.
                rewrite Hcal in Hdestruct4; inv Hdestruct4.
                assert (Hcal´: CalMCSLock (TEVENT (Int.unsigned i0) (TTICKET SET_BUSY) :: l)
                               = Some (MCSLOCK tail (ZMap.set 4 (false, ne4) lock_array) (tl bounds))).
                { simpl; rewrite Hcal; rewrite Hdestruct6; rewrite Hnc4; reflexivity. }
                assert (Hnc0´: ZMap.get 0 (ZMap.set 4 (false, ne4) lock_array) = (bs0, ne0)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc1´: ZMap.get 1 (ZMap.set 4 (false, ne4) lock_array) = (bs1, ne1)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc2´: ZMap.get 2 (ZMap.set 4 (false, ne4) lock_array) = (bs2, ne2)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc3´: ZMap.get 3 (ZMap.set 4 (false, ne4) lock_array) = (bs3, ne3)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc4´: ZMap.get 4 (ZMap.set 4 (false, ne4) lock_array) = (false, ne4)).
                { rewrite ZMap.gss; reflexivity. }
                assert (Hnc5´: ZMap.get 5 (ZMap.set 4 (false, ne4) lock_array) = (bs5, ne5)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc6´: ZMap.get 6 (ZMap.set 4 (false, ne4) lock_array) = (bs6, ne6)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc7´: ZMap.get 7 (ZMap.set 4 (false, ne4) lock_array) = (bs7, ne7)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                unfold Vzero; unfold Int.zero.
                eapply MATCH_MCSLOCK_VALID with (2:= Hnc0´) (3:= Hnc1´) (4:= Hnc2´) (5:= Hnc3´) (6:= Hnc4´)
                                                            (7:= Hnc5´) (8:= Hnc6´) (9:= Hnc7´) in Hcal´.
                simpl 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_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´ & bs_6v´ & 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´).
              ∃ 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´, bs_6v´, ne6_v´, bs7_v´, ne7_v´.
              rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) 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 i) 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. }
          {
            destruct (zeq (Int.unsigned i) lock_index); subst.
            - ∃ la_v.
              ∃ bs0_v, ne0_v.
              ∃ bs1_v, ne1_v.
              ∃ bs2_v, ne2_v.
              ∃ bs3_v, ne3_v.
              ∃ bs4_v, ne4_v.
              ∃ Vzero, ne5_v.
              ∃ bs6_v, ne6_v.
              ∃ bs7_v, ne7_v.
              refine_split´; eauto; try (repeat (eapply Mem.store_valid_access_1; eauto));
              try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST); auto;
                   try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                   try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail).
              + unfold next_pos in HST; unfold next_pos; erewrite Mem.load_store_same; eauto; trivial.
              + rewrite ZMap.gss.
                rewrite Hdestruct3 in Hm; inv Hm.
                rewrite Hcal in Hdestruct4; inv Hdestruct4.
                assert (Hcal´: CalMCSLock (TEVENT (Int.unsigned i0) (TTICKET SET_BUSY) :: l)
                               = Some (MCSLOCK tail (ZMap.set 5 (false, ne5) lock_array) (tl bounds))).
                { Transparent CalMCSLock.
                  simpl.
                  rewrite Hcal; rewrite Hdestruct6; rewrite Hnc5; reflexivity. }
                assert (Hnc0´: ZMap.get 0 (ZMap.set 5 (false, ne5) lock_array) = (bs0, ne0)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc1´: ZMap.get 1 (ZMap.set 5 (false, ne5) lock_array) = (bs1, ne1)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc2´: ZMap.get 2 (ZMap.set 5 (false, ne5) lock_array) = (bs2, ne2)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc3´: ZMap.get 3 (ZMap.set 5 (false, ne5) lock_array) = (bs3, ne3)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc4´: ZMap.get 4 (ZMap.set 5 (false, ne5) lock_array) = (bs4, ne4)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc5´: ZMap.get 5 (ZMap.set 5 (false, ne5) lock_array) = (false, ne5)).
                { rewrite ZMap.gss; reflexivity. }
                assert (Hnc6´: ZMap.get 6 (ZMap.set 5 (false, ne5) lock_array) = (bs6, ne6)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc7´: ZMap.get 7 (ZMap.set 5 (false, ne5) lock_array) = (bs7, ne7)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                unfold Vzero; unfold Int.zero.
                eapply MATCH_MCSLOCK_VALID with (2:= Hnc0´) (3:= Hnc1´) (4:= Hnc2´) (5:= Hnc3´) (6:= Hnc4´)
                                                            (7:= Hnc5´) (8:= Hnc6´) (9:= Hnc7´) in Hcal´.
                simpl 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_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´ & bs_6v´ & 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´).
              ∃ 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´, bs_6v´, ne6_v´, bs7_v´, ne7_v´.
              rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) 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 i) 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. }
          {
            destruct (zeq (Int.unsigned i) lock_index); subst.
            - ∃ 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.
              ∃ Vzero, ne6_v.
              ∃ bs7_v, ne7_v.
              refine_split´; eauto; try (repeat (eapply Mem.store_valid_access_1; eauto));
              try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST); auto;
                   try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                   try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail).
              + unfold next_pos in HST; unfold next_pos; erewrite Mem.load_store_same; eauto; trivial.
              + rewrite ZMap.gss.
                rewrite Hdestruct3 in Hm; inv Hm.
                rewrite Hcal in Hdestruct4; inv Hdestruct4.
                assert (Hcal´: CalMCSLock (TEVENT (Int.unsigned i0) (TTICKET SET_BUSY) :: l)
                               = Some (MCSLOCK tail (ZMap.set 6 (false, ne6) lock_array) (tl bounds))).
                { Transparent CalMCSLock.
                  simpl.
                  rewrite Hcal; rewrite Hdestruct6; rewrite Hnc6; reflexivity. }
                assert (Hnc0´: ZMap.get 0 (ZMap.set 6 (false, ne6) lock_array) = (bs0, ne0)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc1´: ZMap.get 1 (ZMap.set 6 (false, ne6) lock_array) = (bs1, ne1)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc2´: ZMap.get 2 (ZMap.set 6 (false, ne6) lock_array) = (bs2, ne2)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc3´: ZMap.get 3 (ZMap.set 6 (false, ne6) lock_array) = (bs3, ne3)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc4´: ZMap.get 4 (ZMap.set 6 (false, ne6) lock_array) = (bs4, ne4)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc5´: ZMap.get 5 (ZMap.set 6 (false, ne6) lock_array) = (bs5, ne5)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc6´: ZMap.get 6 (ZMap.set 6 (false, ne6) lock_array) = (false, ne6)).
                { rewrite ZMap.gss; reflexivity. }
                assert (Hnc7´: ZMap.get 7 (ZMap.set 6 (false, ne6) lock_array) = (bs7, ne7)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                unfold Vzero; unfold Int.zero.
                eapply MATCH_MCSLOCK_VALID with (2:= Hnc0´) (3:= Hnc1´) (4:= Hnc2´) (5:= Hnc3´) (6:= Hnc4´)
                                                            (7:= Hnc5´) (8:= Hnc6´) (9:= Hnc7´) in Hcal´.
                simpl 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_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´ & bs_6v´ & 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´).
              ∃ 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´, bs_6v´, ne6_v´, bs7_v´, ne7_v´.
              rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) 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 i) 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. }
          {
            destruct (zeq (Int.unsigned i) lock_index); subst.
            - ∃ 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.
              ∃ Vzero, ne7_v.
              refine_split´; eauto; try (repeat (eapply Mem.store_valid_access_1; eauto));
              try (rewrite (Mem.load_store_other _ _ _ _ _ _ HST); auto;
                   try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega);
                   try (right; right; unfold tail_pos, busy_pos, next_pos; simpl; omega); fail).
              + unfold next_pos in HST; unfold next_pos; erewrite Mem.load_store_same; eauto; trivial.
              + rewrite ZMap.gss.
                rewrite Hdestruct3 in Hm; inv Hm.
                rewrite Hcal in Hdestruct4; inv Hdestruct4.
                assert (Hcal´: CalMCSLock (TEVENT (Int.unsigned i0) (TTICKET SET_BUSY) :: l)
                               = Some (MCSLOCK tail (ZMap.set 7 (false, ne7) lock_array) (tl bounds))).
                { simpl; rewrite Hcal; rewrite Hdestruct6; rewrite Hnc7; reflexivity. }
                assert (Hnc0´: ZMap.get 0 (ZMap.set 7 (false, ne7) lock_array) = (bs0, ne0)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc1´: ZMap.get 1 (ZMap.set 7 (false, ne7) lock_array) = (bs1, ne1)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc2´: ZMap.get 2 (ZMap.set 7 (false, ne7) lock_array) = (bs2, ne2)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc3´: ZMap.get 3 (ZMap.set 7 (false, ne7) lock_array) = (bs3, ne3)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc4´: ZMap.get 4 (ZMap.set 7 (false, ne7) lock_array) = (bs4, ne4)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc5´: ZMap.get 5 (ZMap.set 7 (false, ne7) lock_array) = (bs5, ne5)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc6´: ZMap.get 6 (ZMap.set 7 (false, ne7) lock_array) = (bs6, ne6)).
                { rewrite ZMap.gso; try assumption; unfold not; intros contra; inv contra. }
                assert (Hnc7´: ZMap.get 7 (ZMap.set 7 (false, ne7) lock_array) = (false, ne7)).
                { rewrite ZMap.gss; reflexivity. }
                unfold Vzero; unfold Int.zero.
                eapply MATCH_MCSLOCK_VALID with (2:= Hnc0´) (3:= Hnc1´) (4:= Hnc2´) (5:= Hnc3´) (6:= Hnc4´)
                                                            (7:= Hnc5´) (8:= Hnc6´) (9:= Hnc7´) in Hcal´.
                simpl 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_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´ & bs_6v´ & 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´).
              ∃ 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´, bs_6v´, ne6_v´, bs7_v´, ne7_v´.
              rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST) 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 i) 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. }
        - apply inject_incr_refl.
      Qed.

    End mcs_SET_BUSY_ref.

  End WITHMEM.

End Refinement.