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

    Ltac load_store_other_tac H :=
      rewrite (Mem.load_store_other _ _ _ _ _ _ H); auto;
      try (right; left; unfold tail_pos, busy_pos, next_pos; simpl; omega).

    Section mcs_log_ref.

      Lemma mcs_log_spec_ref:
        compatsim (crel HDATA LDATA) (gensem mcs_log_spec) mcs_log_spec_low.
      Proof.
        compatsim_simpl (@match_AbData).
        intros Hargs0 Hasm_inv Hesp HRA Hle.
        inv Hlog.
        assert (HFB: ι b0 = Some (b0, 0)).
        { eapply stencil_find_symbol_inject´; eauto. }
        pose proof match_related as Hre.
        simpl; inv match_related.
        revert H1.
        assert (Hcpuid_range: 0 ≤ (CPU_ID d1) ≤ Int.max_unsigned).
        { generalize max_unsigned_val; intros.
          rewrite H; inv Hhigh´; omega. }
        assert (Hcpuid_eq: Int.unsigned (Int.repr ((CPU_ID d1))) = (CPU_ID d1)).
        { rewrite Int.unsigned_repr; trivial. }
        revert Hcpuid_eq.
        unfold mcs_log_spec.
        subrewrite´.
        intros ? HQ.
        set (rs2´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
                                     :: RA :: nil)
                                 (undef_regs (List.map preg_of destroyed_at_call) rs2))).
        ∃ ι, (rs2´#PC <- (rs2#RA)).
        subdestruct.
        inv HQ.
        destruct m.
        remember (ZMap.get 0 lock_array) as node0; symmetry in Heqnode0;
        destruct node0 as (bs_0, ne_0); rename Heqnode0 into Hna0´.
        remember (ZMap.get 1 lock_array) as node1; symmetry in Heqnode1;
        destruct node1 as (bs_1, ne_1); rename Heqnode1 into Hna1´.
        remember (ZMap.get 2 lock_array) as node2; symmetry in Heqnode2;
        destruct node2 as (bs_2, ne_2); rename Heqnode2 into Hna2´.
        remember (ZMap.get 3 lock_array) as node3; symmetry in Heqnode3;
        destruct node3 as (bs_3, ne_3); rename Heqnode3 into Hna3´.
        remember (ZMap.get 4 lock_array) as node4; symmetry in Heqnode4;
        destruct node4 as (bs_4, ne_4); rename Heqnode4 into Hna4´.
        remember (ZMap.get 5 lock_array) as node5; symmetry in Heqnode5;
        destruct node5 as (bs_5, ne_5); rename Heqnode5 into Hna5´.
        remember (ZMap.get 6 lock_array) as node6; symmetry in Heqnode6;
        destruct node6 as (bs_6, ne_6); rename Heqnode6 into Hna6´.
        remember (ZMap.get 7 lock_array) as node7; symmetry in Heqnode7;
        destruct node7 as (bs_7, ne_7); rename Heqnode7 into Hna7´.

        pose proof HMCSLock as HMCSLock´.
        specialize (HMCSLock _ a).
        rewrite multi_log_re in HMCSLock.
        destruct HMCSLock as (_ & _ & _ & _ & _ & _ & _ & _ & _ &
                                _ & _ & _ & _ & _ & _ & _ & _ &
                                _ & _ & _ & _ & _ & _ & _ & _ & _ &
                                _ & _ & _ & _ & _ & _ & _ & _ &
                                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 & _).
        assert (HST__la: ∃ m_la, Mem.store Mint32 m2 b0 (tail_pos (Int.unsigned i))
                                                (Vint (Int.repr tail)) = Some m_la).
        { eapply Mem.valid_access_store; eauto. }
        destruct HST__la as (m_la & HST__la).
        assert (HST__bs0: ∃ m_bs0, Mem.store Mint32 m_la b0 (busy_pos (Int.unsigned i) 0)
                                                  (Vint (Int.repr (BooltoZ bs_0))) = Some m_bs0).
        { eapply Mem.valid_access_store; eauto.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
        destruct HST__bs0 as (m_bs0 & HST__bs0).
        assert (HST__ne0: ∃ m_ne0, Mem.store Mint32 m_bs0 b0 (next_pos (Int.unsigned i) 0) (Vint (Int.repr ne_0)) = Some m_ne0).
        { eapply Mem.valid_access_store; eauto.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
        destruct HST__ne0 as (m_ne0 & HST__ne0).
        assert (HST__bs1: ∃ m_bs1, Mem.store Mint32 m_ne0 b0 (busy_pos (Int.unsigned i) 1)
                                                  (Vint (Int.repr (BooltoZ bs_1))) = Some m_bs1).
        { eapply Mem.valid_access_store; eauto.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
        destruct HST__bs1 as (m_bs1 & HST__bs1).
        assert (HST__ne1: ∃ m_ne1, Mem.store Mint32 m_bs1 b0 (next_pos (Int.unsigned i) 1) (Vint (Int.repr ne_1)) = Some m_ne1).
        { eapply Mem.valid_access_store; eauto.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs1); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
        destruct HST__ne1 as (m_ne1 & HST__ne1).
        assert (HST__bs2: ∃ m_bs2, Mem.store Mint32 m_ne1 b0 (busy_pos (Int.unsigned i) 2)
                                                (Vint (Int.repr (BooltoZ bs_2))) = Some m_bs2).
        { eapply Mem.valid_access_store; eauto.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne1); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs1); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
        destruct HST__bs2 as (m_bs2 & HST__bs2).
        assert (HST__ne2: ∃ m_ne2, Mem.store Mint32 m_bs2 b0 (next_pos (Int.unsigned i) 2) (Vint (Int.repr ne_2)) = Some m_ne2).
        { eapply Mem.valid_access_store; eauto.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs2); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne1); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs1); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
        destruct HST__ne2 as (m_ne2 & HST__ne2).
        assert (HST__bs3: ∃ m_bs3, Mem.store Mint32 m_ne2 b0 (busy_pos (Int.unsigned i) 3)
                                                  (Vint (Int.repr (BooltoZ bs_3))) = Some m_bs3).
        { eapply Mem.valid_access_store; eauto.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne2); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs2); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne1); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs1); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
        destruct HST__bs3 as (m_bs3 & HST__bs3).
        assert (HST__ne3: ∃ m_ne3, Mem.store Mint32 m_bs3 b0 (next_pos (Int.unsigned i) 3) (Vint (Int.repr ne_3)) = Some m_ne3).
        { eapply Mem.valid_access_store; eauto.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs3); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne2); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs2); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne1); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs1); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
        destruct HST__ne3 as (m_ne3 & HST__ne3).
        assert (HST__bs4: ∃ m_bs4, Mem.store Mint32 m_ne3 b0 (busy_pos (Int.unsigned i) 4)
                                                  (Vint (Int.repr (BooltoZ bs_4))) = Some m_bs4).
        { eapply Mem.valid_access_store; eauto.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne3); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs3); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne2); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs2); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne1); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs1); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
        destruct HST__bs4 as (m_bs4 & HST__bs4).
        assert (HST__ne4: ∃ m_ne4, Mem.store Mint32 m_bs4 b0 (next_pos (Int.unsigned i) 4) (Vint (Int.repr ne_4)) = Some m_ne4).
        { eapply Mem.valid_access_store; eauto.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs4); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne3); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs3); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne2); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs2); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne1); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs1); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
        destruct HST__ne4 as (m_ne4 & HST__ne4).
        assert (HST__bs5: ∃ m_bs5, Mem.store Mint32 m_ne4 b0 (busy_pos (Int.unsigned i) 5)
                                                  (Vint (Int.repr (BooltoZ bs_5))) = Some m_bs5).
        { eapply Mem.valid_access_store; eauto.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne4); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs4); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne3); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs3); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne2); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs2); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne1); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs1); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
        destruct HST__bs5 as (m_bs5 & HST__bs5).
        assert (HST__ne5: ∃ m_ne5, Mem.store Mint32 m_bs5 b0 (next_pos (Int.unsigned i) 5) (Vint (Int.repr ne_5)) = Some m_ne5).
        { eapply Mem.valid_access_store; eauto.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs5); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne4); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs4); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne3); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs3); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne2); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs2); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne1); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs1); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
        destruct HST__ne5 as (m_ne5 & HST__ne5).
        assert (HST__bs6: ∃ m_bs6, Mem.store Mint32 m_ne5 b0 (busy_pos (Int.unsigned i) 6)
                                                  (Vint (Int.repr (BooltoZ bs_6))) = Some m_bs6).
        { eapply Mem.valid_access_store; eauto.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne5); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs5); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne4); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs4); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne3); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs3); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne2); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs2); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne1); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs1); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
        destruct HST__bs6 as (m_bs6 & HST__bs6).
        assert (HST__ne6: ∃ m_ne6, Mem.store Mint32 m_bs6 b0 (next_pos (Int.unsigned i) 6) (Vint (Int.repr ne_6)) = Some m_ne6).
        { eapply Mem.valid_access_store; eauto.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs6); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne5); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs5); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne4); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs4); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne3); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs3); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne2); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs2); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne1); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs1); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
        destruct HST__ne6 as (m_ne6 & HST__ne6).
        assert (HST__bs7: ∃ m_bs7, Mem.store Mint32 m_ne6 b0 (busy_pos (Int.unsigned i) 7)
                                                  (Vint (Int.repr (BooltoZ bs_7))) = Some m_bs7).
        { eapply Mem.valid_access_store; eauto.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne6); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs6); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne5); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs5); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne4); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs4); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne3); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs3); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne2); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs2); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne1); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs1); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
        destruct HST__bs7 as (m_bs7 & HST__bs7).
        assert (HST__ne7: ∃ m_ne7, Mem.store Mint32 m_bs7 b0 (next_pos (Int.unsigned i) 7) (Vint (Int.repr ne_7)) = Some m_ne7).
        { eapply Mem.valid_access_store; eauto.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs7); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne6); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs6); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne5); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs5); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne4); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs4); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne3); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs3); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne2); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs2); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne1); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs1); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__ne0); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__bs0); trivial.
          apply (Mem.store_valid_access_1 _ _ _ _ _ _ HST__la); trivial. }
        destruct HST__ne7 as (m_ne7 & HST__ne7).
        refine_split´; repeat val_inject_inv; eauto.
        - econstructor; eauto; simpl; lift_trivial.
          × unfold atomic_mcs_log_spec.
            simpl; subrewrite´.
          × eapply (extcall_args_without_data (D:= HDATAOps) d2).
            inv Hargs.
            inv H2.
            inv Hargs0.
            inv H3.
            inv H7.
            inv H6.
            inv H1.
            constructor; eauto.
            econstructor; eauto.
            econstructor; eauto.
            econstructor; eauto.
        - split; eauto; pattern2_refinement_simpl;
          econstructor; eauto. simpl.
          econstructor; eauto; intros.
          destruct (zeq (Int.unsigned i) lock_index); subst.
          { ∃ (Vint (Int.repr tail)).
            ∃ (Vint (Int.repr (BooltoZ bs_0))), (Vint (Int.repr ne_0)).
            ∃ (Vint (Int.repr (BooltoZ bs_1))), (Vint (Int.repr ne_1)).
            ∃ (Vint (Int.repr (BooltoZ bs_2))), (Vint (Int.repr ne_2)).
            ∃ (Vint (Int.repr (BooltoZ bs_3))), (Vint (Int.repr ne_3)).
            ∃ (Vint (Int.repr (BooltoZ bs_4))), (Vint (Int.repr ne_4)).
            ∃ (Vint (Int.repr (BooltoZ bs_5))), (Vint (Int.repr ne_5)).
            ∃ (Vint (Int.repr (BooltoZ bs_6))), (Vint (Int.repr ne_6)).
            ∃ (Vint (Int.repr (BooltoZ bs_7))), (Vint (Int.repr ne_7)).
            refine_split´; eauto; try (repeat (eapply Mem.store_valid_access_1; eauto)).
            - load_store_other_tac HST__ne7; load_store_other_tac HST__bs7; load_store_other_tac HST__ne6; load_store_other_tac HST__bs6;
              load_store_other_tac HST__ne5; load_store_other_tac HST__bs5; load_store_other_tac HST__ne4; load_store_other_tac HST__bs4;
              load_store_other_tac HST__ne3; load_store_other_tac HST__bs3; load_store_other_tac HST__ne2; load_store_other_tac HST__bs2;
              load_store_other_tac HST__ne1; load_store_other_tac HST__bs1; load_store_other_tac HST__ne0; load_store_other_tac HST__bs0.
              erewrite Mem.load_store_same; eauto; trivial.
            - load_store_other_tac HST__ne7; load_store_other_tac HST__bs7; load_store_other_tac HST__ne6; load_store_other_tac HST__bs6;
              load_store_other_tac HST__ne5; load_store_other_tac HST__bs5; load_store_other_tac HST__ne4; load_store_other_tac HST__bs4;
              load_store_other_tac HST__ne3; load_store_other_tac HST__bs3; load_store_other_tac HST__ne2; load_store_other_tac HST__bs2;
              load_store_other_tac HST__ne1; load_store_other_tac HST__bs1.
              rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne0); auto;
              try (right; right; unfold busy_pos, busy_pos, next_pos; simpl; omega).
              erewrite Mem.load_store_same; eauto; trivial.
            - load_store_other_tac HST__ne7; load_store_other_tac HST__bs7; load_store_other_tac HST__ne6; load_store_other_tac HST__bs6;
              load_store_other_tac HST__ne5; load_store_other_tac HST__bs5; load_store_other_tac HST__ne4; load_store_other_tac HST__bs4;
              load_store_other_tac HST__ne3; load_store_other_tac HST__bs3; load_store_other_tac HST__ne2; load_store_other_tac HST__bs2;
              load_store_other_tac HST__ne1; load_store_other_tac HST__bs1.
              erewrite Mem.load_store_same; eauto; trivial.
            - load_store_other_tac HST__ne7; load_store_other_tac HST__bs7; load_store_other_tac HST__ne6; load_store_other_tac HST__bs6;
              load_store_other_tac HST__ne5; load_store_other_tac HST__bs5; load_store_other_tac HST__ne4; load_store_other_tac HST__bs4;
              load_store_other_tac HST__ne3; load_store_other_tac HST__bs3; load_store_other_tac HST__ne2; load_store_other_tac HST__bs2.
              rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne1); auto;
              try (right; right; unfold busy_pos, busy_pos, next_pos; simpl; omega).
              erewrite Mem.load_store_same; eauto; trivial.
            - load_store_other_tac HST__ne7; load_store_other_tac HST__bs7; load_store_other_tac HST__ne6; load_store_other_tac HST__bs6;
              load_store_other_tac HST__ne5; load_store_other_tac HST__bs5; load_store_other_tac HST__ne4; load_store_other_tac HST__bs4;
              load_store_other_tac HST__ne3; load_store_other_tac HST__bs3; load_store_other_tac HST__ne2; load_store_other_tac HST__bs2;
              erewrite Mem.load_store_same; eauto; trivial.
            - load_store_other_tac HST__ne7; load_store_other_tac HST__bs7; load_store_other_tac HST__ne6; load_store_other_tac HST__bs6;
              load_store_other_tac HST__ne5; load_store_other_tac HST__bs5; load_store_other_tac HST__ne4; load_store_other_tac HST__bs4;
              load_store_other_tac HST__ne3; load_store_other_tac HST__bs3.
              rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne2); auto;
              try (right; right; unfold busy_pos, busy_pos, next_pos; simpl; omega).
              erewrite Mem.load_store_same; eauto; trivial.
            - load_store_other_tac HST__ne7; load_store_other_tac HST__bs7; load_store_other_tac HST__ne6; load_store_other_tac HST__bs6;
              load_store_other_tac HST__ne5; load_store_other_tac HST__bs5; load_store_other_tac HST__ne4; load_store_other_tac HST__bs4;
              load_store_other_tac HST__ne3; load_store_other_tac HST__bs3;
              erewrite Mem.load_store_same; eauto; trivial.
            - load_store_other_tac HST__ne7; load_store_other_tac HST__bs7; load_store_other_tac HST__ne6; load_store_other_tac HST__bs6;
              load_store_other_tac HST__ne5; load_store_other_tac HST__bs5; load_store_other_tac HST__ne4; load_store_other_tac HST__bs4;
              rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne3); auto;
              try (right; right; unfold busy_pos, busy_pos, next_pos; simpl; omega).
              erewrite Mem.load_store_same; eauto; trivial.
            - load_store_other_tac HST__ne7; load_store_other_tac HST__bs7; load_store_other_tac HST__ne6; load_store_other_tac HST__bs6;
              load_store_other_tac HST__ne5; load_store_other_tac HST__bs5; load_store_other_tac HST__ne4; load_store_other_tac HST__bs4;
              erewrite Mem.load_store_same; eauto; trivial.
            - load_store_other_tac HST__ne7; load_store_other_tac HST__bs7; load_store_other_tac HST__ne6; load_store_other_tac HST__bs6;
              load_store_other_tac HST__ne5; load_store_other_tac HST__bs5.
              rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne4); auto;
              try (right; right; unfold busy_pos, busy_pos, next_pos; simpl; omega).
              erewrite Mem.load_store_same; eauto; trivial.
            - load_store_other_tac HST__ne7; load_store_other_tac HST__bs7; load_store_other_tac HST__ne6; load_store_other_tac HST__bs6;
              load_store_other_tac HST__ne5; load_store_other_tac HST__bs5;
              erewrite Mem.load_store_same; eauto; trivial.
            - load_store_other_tac HST__ne7; load_store_other_tac HST__bs7; load_store_other_tac HST__ne6; load_store_other_tac HST__bs6.
              rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne5); auto;
              try (right; right; unfold busy_pos, busy_pos, next_pos; simpl; omega).
              erewrite Mem.load_store_same; eauto; trivial.
            - load_store_other_tac HST__ne7; load_store_other_tac HST__bs7; load_store_other_tac HST__ne6; load_store_other_tac HST__bs6;
              erewrite Mem.load_store_same; eauto; trivial.
            - load_store_other_tac HST__ne7; load_store_other_tac HST__bs7.
              rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne6); auto;
              try (right; right; unfold busy_pos, busy_pos, next_pos; simpl; omega).
              erewrite Mem.load_store_same; eauto; trivial.
            - load_store_other_tac HST__ne7; load_store_other_tac HST__bs7;
              erewrite Mem.load_store_same; eauto; trivial.
            - rewrite (Mem.load_store_other _ _ _ _ _ _ HST__ne7); auto;
              try (right; right; unfold busy_pos, busy_pos, next_pos; simpl; omega).
              erewrite Mem.load_store_same; eauto; trivial.
            - erewrite Mem.load_store_same; eauto; trivial.
            -
              rewrite ZMap.gss.
              econstructor; try eauto. }
          {
            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.
            mcslock_destruct´ HMCSLock´.
            ∃ 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´.
            rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__la)
              in HL__la´, HL__bs0´, HL__ne0´, HL__bs1´, HL__ne1´, HL__bs2´, HL__ne2´, HL__bs3´, HL__ne3´, HL__bs4´, HL__ne4´,
                 HL__bs5´, HL__ne5´, HL__bs6´, HL__ne6´, HL__bs7´, HL__ne7´;
              try (simpl; right; destruct (zle (Int.unsigned 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]).

            rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs0)
              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]).

            rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne0)
              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]).

            rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs1)
              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]).

            rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne1)
              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]).

            rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs2)
              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]).

            rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne2)
              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]).

            rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs3)
              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]).

            rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne3)
              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]).

            rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs4)
              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]).

            rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne4)
              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]).

            rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs5)
              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]).

            rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne5)
              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]).

            rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs6)
              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]).

            rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne6)
              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]).

            rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__bs7)
              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]).

            rewrite <- (Mem.load_store_other _ _ _ _ _ _ HST__ne7)
              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. }
        - intros.
          inv Hasm_inv.
          inv inv_inject_neutral.
          subst rs2´.
          destruct r; simpl;
          repeat simpl_Pregmap; eauto;
          (elim H; eauto 20).
      Qed.

    End mcs_log_ref.

  End WITHMEM.

End Refinement.