Library mcertikos.mcslock.MCSLockIntroGenAsm

Require Import Coqlib.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Locations.
Require Import AuxStateDataType.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Op.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import FlatMemory.
Require Import RefinementTactic.
Require Import AuxLemma.
Require Import RealParams.
Require Import Constant.
Require Import AsmImplLemma.
Require Import AsmImplTactic.
Require Import GlobIdent.
Require Import CommonTactic.

Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compcertx.MakeProgram.
Require Import LAsmModuleSem.
Require Import LAsm.
Require Import liblayers.compat.CompatGenSem.
Require Import PrimSemantics.
Require Import Conventions.

Require Import LAsmModuleSemSpec.
Require Import LRegSet.

Require Import AbstractDataType.
Require Import CalMCSLock.

Require Import MCSMCurID.
Require Import MCSLockIntroGenSpec.
Require Import MCSLockIntroGenAsmSource.
Require Import MCSLockIntroGenAsmData.

Section ASM_VERIFICATION.

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

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

  Notation LDATA := RData.
  Notation LDATAOps := (cdata (cdata_ops := mcurid_data_ops) LDATA).

  Section WITHMEM.

    Context `{Hstencil: Stencil}.
    Context `{Hmem: Mem.MemoryModelX}.
    Context `{Hmwd: UseMemWithData mem}.
    Context `{make_program_ops: !MakeProgramOps function Ctypes.type fundef unit}.
    Context `{make_program_prf: !MakeProgram function Ctypes.type fundef unit}.

    Ltac accessors_simpl:=
      match goal with
      | |- exec_storeex _ _ _ _ _ _ _ = _ ⇒
        unfold exec_storeex, LoadStoreSem1.exec_storeex1;
          simpl; Lregset_simpl_tac;
          match goal with
          | |- context [Asm.exec_store _ _ _ _ _ _ _] ⇒
            unfold Asm.exec_store; simpl;
            Lregset_simpl_tac; lift_trivial
          end
      | |- exec_loadex _ _ _ _ _ _ = _ ⇒
        unfold exec_loadex, LoadStoreSem1.exec_loadex1;
          simpl; Lregset_simpl_tac;
          match goal with
          | |- context[Asm.exec_load _ _ _ _ _ _] ⇒
            unfold Asm.exec_load; simpl;
            Lregset_simpl_tac; lift_trivial
          end
      end.

    Ltac clearAll := repeat match goal with
                            | [H: _ |- _] ⇒ clear H
                            end.


    Lemma mcs_log_spec:
      ∀ ge (s: stencil) (rs rs´: regset) b b´ m m_la m0_bs m0_ne m1_bs m1_ne m2_bs m2_ne m3_bs m3_ne
             m4_bs m4_ne m5_bs m5_ne m6_bs m6_ne m7_bs m´ labd labd´ lock_index cpuid
             la bs0 bs1 bs2 bs3 bs4 bs5 bs6 bs7 ne0 ne1 ne2 ne3 ne4 ne5 ne6 ne7 sig
             (HHIGH: high_level_invariant labd)
             (ikern: ikern labd = true)
             (ihost: ihost labd = true)
             (index_range: 0 ≤ (Int.unsigned lock_index) < lock_range)
             (cpuid_range: 0 ≤ (Int.unsigned cpuid) < TOTAL_CPU),
        find_symbol s mcs_log = Some b´ →
        make_globalenv s (mcs_log ↦ mcs_log_function) mcurid = ret ge →
        rs PC = Vptr b´ Int.zero →
        atomic_mcs_log_spec (Int.unsigned lock_index) (Int.unsigned cpuid) labd
        = Some (labd´, la, (bs0, bs1, bs2, bs3, bs4, bs5, bs6, bs7), (ne0, ne1, ne2, ne3, ne4, ne5, ne6, ne7)) →
        find_symbol s MCS_LOCK_LOC = Some b →
        sig = AST.mksignature (AST.Tint::AST.Tint::nil) None AST.cc_default →
        Asm.extcall_arguments rs m sig (Vint lock_index ::Vint cpuid ::nil) →
        Mem.store Mint32 m b (tail_pos (Int.unsigned lock_index)) (Vint (Int.repr la)) = Some m_la →
        Mem.store Mint32 m_la b (busy_pos (Int.unsigned lock_index) 0) (Vint (Int.repr bs0)) = Some m0_bs →
        Mem.store Mint32 m0_bs b (next_pos (Int.unsigned lock_index) 0) (Vint (Int.repr ne0)) = Some m0_ne →
        Mem.store Mint32 m0_ne b (busy_pos (Int.unsigned lock_index) 1) (Vint (Int.repr bs1)) = Some m1_bs →
        Mem.store Mint32 m1_bs b (next_pos (Int.unsigned lock_index) 1) (Vint (Int.repr ne1)) = Some m1_ne →
        Mem.store Mint32 m1_ne b (busy_pos (Int.unsigned lock_index) 2) (Vint (Int.repr bs2)) = Some m2_bs →
        Mem.store Mint32 m2_bs b (next_pos (Int.unsigned lock_index) 2) (Vint (Int.repr ne2)) = Some m2_ne →
        Mem.store Mint32 m2_ne b (busy_pos (Int.unsigned lock_index) 3) (Vint (Int.repr bs3)) = Some m3_bs →
        Mem.store Mint32 m3_bs b (next_pos (Int.unsigned lock_index) 3) (Vint (Int.repr ne3)) = Some m3_ne →
        Mem.store Mint32 m3_ne b (busy_pos (Int.unsigned lock_index) 4) (Vint (Int.repr bs4)) = Some m4_bs →
        Mem.store Mint32 m4_bs b (next_pos (Int.unsigned lock_index) 4) (Vint (Int.repr ne4)) = Some m4_ne →
        Mem.store Mint32 m4_ne b (busy_pos (Int.unsigned lock_index) 5) (Vint (Int.repr bs5)) = Some m5_bs →
        Mem.store Mint32 m5_bs b (next_pos (Int.unsigned lock_index) 5) (Vint (Int.repr ne5)) = Some m5_ne →
        Mem.store Mint32 m5_ne b (busy_pos (Int.unsigned lock_index) 6) (Vint (Int.repr bs6)) = Some m6_bs →
        Mem.store Mint32 m6_bs b (next_pos (Int.unsigned lock_index) 6) (Vint (Int.repr ne6)) = Some m6_ne →
        Mem.store Mint32 m6_ne b (busy_pos (Int.unsigned lock_index) 7) (Vint (Int.repr bs7)) = Some m7_bs →
        Mem.store Mint32 m7_bs b (next_pos (Int.unsigned lock_index) 7) (Vint (Int.repr ne7)) = Some m´ →
        asm_invariant (mem := mwd LDATAOps) s rs (m, labd) →
        low_level_invariant (Mem.nextblock m) labd →
        let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
                                   :: RA :: nil)
                               (undef_regs (List.map preg_of destroyed_at_call) rs)) in
        ∃ f´ m´´ r_,
          lasm_step (mcs_log ↦ mcs_log_function) (mcurid (Hmwd:= Hmwd) (Hmem:= Hmem)) mcs_log s rs
                    (m, labd) r_ (m´´, labd´)
          ∧ inject_incr (Mem.flat_inj (Mem.nextblock m´)) f´
          ∧ Memtype.Mem.inject f´ m´ m´´
          ∧ (Mem.nextblock m´ ≤ Mem.nextblock m´´)%positive
          ∧ (∀ l,
                 Val.lessdef (Pregmap.get l (rs´ # PC <- (rs RA)))
                             (Pregmap.get l r_)).
      Proof.
        intros.
        inv H23.
        rename H24 into HLOW; subst.
        inv H5.
        inv H25.
        inv H27.
        inv H24.
        simpl in H26.
        simpl in H27.

        caseEq(Mem.alloc m 0 16).
        intros m_init b0 HALC.
        exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
        intros Hstencil_matches.

        assert(Hnextblock: Mem.nextblock m´ = Mem.nextblock m).
        {
          rewrite (Mem.nextblock_store _ _ _ _ _ _ H22); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ H21); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ H20); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ H19); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ H18); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ H17); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ H16); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ H15); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ H14); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ H13); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ H12); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ H11); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ H10); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ H9); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ H8); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ H7); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ H6); trivial.
        }

        assert (Hblock: Ple (Genv.genv_next ge) b0 ∧ Plt b0 (Mem.nextblock m_init)).
        {
          erewrite Mem.nextblock_alloc; eauto.
          apply Mem.alloc_result in HALC.
          rewrite HALC.
          inv inv_inject_neutral.
          inv Hstencil_matches.
          rewrite stencil_matches_genv_next.
          lift_unfold.
          split; xomega.
        }


        exploit Hatomic_mcs_log; eauto.
        intros [[b_atomic_mcs_log [Hatomic_mcs_log_symbol Hatomic_mcs_log_fun] prim_atomic_mcs_log]].


        specialize (Mem.valid_access_alloc_same _ _ _ _ _ HALC). intros.


        assert (HFRAME1: Mem.valid_access m_init Mint32 b0 8 Freeable).
        {
          eapply H4; auto; simpl; try omega.
          unfold Z.divide.
          ∃ 2; omega.
        }
        eapply Mem.valid_access_implies with (p2:= Writable) in HFRAME1; [|constructor].
        destruct (Mem.valid_access_store _ _ _ _ (rs ESP) HFRAME1) as [m_frame1 HST_FRAME1].

        assert (HFRAME2: Mem.valid_access m_frame1 Mint32 b0 12 Freeable).
        {
          eapply Mem.store_valid_access_1; eauto.
          eapply H4; auto; simpl; try omega.
          unfold Z.divide.
          ∃ 3; omega.
        }
        eapply Mem.valid_access_implies with (p2:= Writable) in HFRAME2; [|constructor].
        destruct (Mem.valid_access_store _ _ _ _ (rs RA) HFRAME2) as [m_frame2 HST_FRAME2].

        assert (HFRAME3: Mem.valid_access m_frame2 Mint32 b0 0 Freeable).
        {
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply H4; auto; simpl; try omega.
          apply Zdivide_0.
        }
        eapply Mem.valid_access_implies with (p2:= Writable) in HFRAME3; [|constructor].
        destruct (Mem.valid_access_store _ _ _ _ (Vint lock_index) HFRAME3) as [m_frame3 HST_FRAME3].

        assert(Hnextblock_m_frame3: Mem.nextblock m_frame3 = Mem.nextblock m_init).
        {
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST_FRAME3); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST_FRAME2); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST_FRAME1); trivial.
        }

        assert (HFRAME4: Mem.valid_access m_frame3 Mint32 b0 4 Freeable).
        {
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply H4; auto; simpl; try omega.
          ∃ 1.
          omega.
        }
        eapply Mem.valid_access_implies with (p2:= Writable) in HFRAME4; [|constructor].
        destruct (Mem.valid_access_store _ _ _ _ (Vint cpuid) HFRAME4) as [m_frame4 HST_FRAME4].

        assert(Hnextblock_m_frame4: Mem.nextblock m_frame4 = Mem.nextblock m_init).
        {
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST_FRAME4); trivial.
        }

        
        
        assert (HTAIL: Mem.valid_access m_frame4 Mint32 b (tail_pos (Int.unsigned lock_index)) Writable).
        {
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.valid_access_alloc_other; eauto.
          eapply Mem.store_valid_access_3; eauto.
        }
        destruct (Mem.valid_access_store _ _ _ _ (Vint (Int.repr la)) HTAIL) as [m_tail HST_TAIL].


        assert (HBUSY0: Mem.valid_access m_tail Mint32 b (busy_pos (Int.unsigned lock_index) 0) Writable).
        {
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.valid_access_alloc_other; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_3; eauto.
        }
        destruct (Mem.valid_access_store _ _ _ _ (Vint (Int.repr bs0)) HBUSY0) as [m_busy0 HST_BUSY0].

        assert (HNEXT0: Mem.valid_access m_busy0 Mint32 b (next_pos (Int.unsigned lock_index) 0) Writable).
        {
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.valid_access_alloc_other; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_3; eauto.
        }
        destruct (Mem.valid_access_store _ _ _ _ (Vint (Int.repr ne0)) HNEXT0) as [m_next0 HST_NEXT0].


        assert (HBUSY1: Mem.valid_access m_next0 Mint32 b (busy_pos (Int.unsigned lock_index) 1) Writable).
        {
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.valid_access_alloc_other; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_3; eauto.
        }
        destruct (Mem.valid_access_store _ _ _ _ (Vint (Int.repr bs1)) HBUSY1) as [m_busy1 HST_BUSY1].

        assert (HNEXT1: Mem.valid_access m_busy1 Mint32 b (next_pos (Int.unsigned lock_index) 1) Writable).
        {
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.valid_access_alloc_other; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_3; eauto.
        }
        destruct (Mem.valid_access_store _ _ _ _ (Vint (Int.repr ne1)) HNEXT1) as [m_next1 HST_NEXT1].


        assert (HBUSY2: Mem.valid_access m_next1 Mint32 b (busy_pos (Int.unsigned lock_index) 2) Writable).
        {
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.valid_access_alloc_other; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_3; eauto.
        }
        destruct (Mem.valid_access_store _ _ _ _ (Vint (Int.repr bs2)) HBUSY2) as [m_busy2 HST_BUSY2].

        assert (HNEXT2: Mem.valid_access m_busy2 Mint32 b (next_pos (Int.unsigned lock_index) 2) Writable).
        {
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.valid_access_alloc_other; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_3; eauto.
        }
        destruct (Mem.valid_access_store _ _ _ _ (Vint (Int.repr ne2)) HNEXT2) as [m_next2 HST_NEXT2].


        assert (HBUSY3: Mem.valid_access m_next2 Mint32 b (busy_pos (Int.unsigned lock_index) 3) Writable).
        {
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.valid_access_alloc_other; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_3; eauto.
        }
        destruct (Mem.valid_access_store _ _ _ _ (Vint (Int.repr bs3)) HBUSY3) as [m_busy3 HST_BUSY3].

        assert (HNEXT3: Mem.valid_access m_busy3 Mint32 b (next_pos (Int.unsigned lock_index) 3) Writable).
        {
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.valid_access_alloc_other; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_3; eauto.
        }
        destruct (Mem.valid_access_store _ _ _ _ (Vint (Int.repr ne3)) HNEXT3) as [m_next3 HST_NEXT3].


        assert (HBUSY4: Mem.valid_access m_next3 Mint32 b (busy_pos (Int.unsigned lock_index) 4) Writable).
        {
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.valid_access_alloc_other; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_3; eauto.
        }
        destruct (Mem.valid_access_store _ _ _ _ (Vint (Int.repr bs4)) HBUSY4) as [m_busy4 HST_BUSY4].

        assert (HNEXT4: Mem.valid_access m_busy4 Mint32 b (next_pos (Int.unsigned lock_index) 4) Writable).
        {
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.valid_access_alloc_other; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_3; eauto.
        }
        destruct (Mem.valid_access_store _ _ _ _ (Vint (Int.repr ne4)) HNEXT4) as [m_next4 HST_NEXT4].


        assert (HBUSY5: Mem.valid_access m_next4 Mint32 b (busy_pos (Int.unsigned lock_index) 5) Writable).
        {
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.valid_access_alloc_other; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_3; eauto.
        }
        destruct (Mem.valid_access_store _ _ _ _ (Vint (Int.repr bs5)) HBUSY5) as [m_busy5 HST_BUSY5].

        assert (HNEXT5: Mem.valid_access m_busy5 Mint32 b (next_pos (Int.unsigned lock_index) 5) Writable).
        {
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.valid_access_alloc_other; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_3; eauto.
        }
        destruct (Mem.valid_access_store _ _ _ _ (Vint (Int.repr ne5)) HNEXT5) as [m_next5 HST_NEXT5].


        assert (HBUSY6: Mem.valid_access m_next5 Mint32 b (busy_pos (Int.unsigned lock_index) 6) Writable).
        {
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.valid_access_alloc_other; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_3; eauto.
        }
        destruct (Mem.valid_access_store _ _ _ _ (Vint (Int.repr bs6)) HBUSY6) as [m_busy6 HST_BUSY6].

        assert (HNEXT6: Mem.valid_access m_busy6 Mint32 b (next_pos (Int.unsigned lock_index) 6) Writable).
        {
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.valid_access_alloc_other; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_3; eauto.
        }
        destruct (Mem.valid_access_store _ _ _ _ (Vint (Int.repr ne6)) HNEXT6) as [m_next6 HST_NEXT6].


        assert (HBUSY7: Mem.valid_access m_next6 Mint32 b (busy_pos (Int.unsigned lock_index) 7) Writable).
        {
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.valid_access_alloc_other; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_3; eauto.
        }
        destruct (Mem.valid_access_store _ _ _ _ (Vint (Int.repr bs7)) HBUSY7) as [m_busy7 HST_BUSY7].

        assert (HNEXT7: Mem.valid_access m_busy7 Mint32 b (next_pos (Int.unsigned lock_index) 7) Writable).
        {
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.valid_access_alloc_other; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_3; eauto.
        }
        destruct (Mem.valid_access_store _ _ _ _ (Vint (Int.repr ne7)) HNEXT7) as [m_next7 HST_NEXT7].

        assert (Hnextblock_m_next7: Mem.nextblock m_next7 = Mem.nextblock m_init).
        {
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST_NEXT7); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST_BUSY7); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST_NEXT6); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST_BUSY6); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST_NEXT5); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST_BUSY5); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST_NEXT4); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST_BUSY4); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST_NEXT3); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST_BUSY3); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST_NEXT2); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST_BUSY2); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST_NEXT1); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST_BUSY1); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST_NEXT0); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST_BUSY0); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST_TAIL); trivial.
        }

        assert (HFREE: Mem.range_perm m_next7 b0 0 16 Cur Freeable).
        {
          unfold Mem.range_perm.
          intros.
          repeat (eapply Mem.perm_store_1; [eassumption|]).
          eapply Mem.perm_alloc_2; eauto.
        }

        destruct (Mem.range_perm_free _ _ _ _ HFREE) as [m_free HST_FREE].

        exploit Hmcs_log; eauto 2.
        intros Hfunct.

        rewrite (Lregset_rewrite rs).
        refine_split´; try eassumption.
        rewrite H1.
        econstructor; eauto; subst.


        one_step_forward´.
        Lregset_simpl_tac.
        lift_trivial.
        change (Int.unsigned (Int.add Int.zero (Int.repr 8))) with 8.
        change (Int.unsigned (Int.add Int.zero (Int.repr 12))) with 12.
        unfold set; simpl.
        rewrite HALC. simpl.
        rewrite HST_FRAME1.
        simpl.
        rewrite HST_FRAME2.
        reflexivity.

        Lregset_simpl_tac´ 1.

        one_step_forward´.
        accessors_simpl.
        unfold Mem.loadv in H26.
        Lregset_simpl_tac.

        change (Int.add Int.zero (Int.repr 0)) with (Int.repr 0).
        case_eq (Val.add (rs ESP) (Vint (Int.repr 0))); intros;
        rewrite H5 in H26; try discriminate H26.
        rewrite ikern, ihost.
        unfold Asm.exec_load.
        unfold Mem.loadv.
        unfold eval_addrmode; simpl.
        Lregset_simpl_tac.
        unfold lift; simpl.
        assert (Plt b1 (Mem.nextblock m)).
        {
          eapply Mem.load_valid_access in H26.
          eapply Mem.valid_access_implies with (p2:= Nonempty) in H26; [|constructor].
          exploit Mem.valid_access_valid_block; eauto.
        }
        exploit Mem.alloc_result; eauto.
        intro nbm1.
        assert (b1 ≠ b0).
        {
          intro.
          subst.
          xomega.
        }
        erewrite Mem.load_store_other; eauto.
        erewrite Mem.load_store_other; eauto.
        erewrite Mem.load_alloc_other; eauto.
        Lregset_simpl_tac.

        one_step_forward´.
        accessors_simpl.
        change (Int.unsigned (Int.add Int.zero (Int.add Int.zero Int.zero))) with 0.
        unfold set; simpl.
        rewrite ikern, ihost.
        rewrite HST_FRAME3.
        reflexivity.

        one_step_forward´.
        accessors_simpl.
        unfold Mem.loadv in H27.
        Lregset_simpl_tac.
        change (Int.add Int.zero (Int.repr 4)) with (Int.repr 4).
        case_eq (Val.add (rs ESP) (Vint (Int.repr 4))); intros;
        try rewrite H5 in H27; try discriminate H27.
        rewrite ikern, ihost.
        unfold Asm.exec_load.
        unfold Mem.loadv.
        unfold eval_addrmode; simpl.
        Lregset_simpl_tac.
        unfold lift; simpl.
        assert (Plt b1 (Mem.nextblock m)).
        {
          eapply Mem.load_valid_access in H27.
          eapply Mem.valid_access_implies with (p2:= Nonempty) in H27; [|constructor].
          exploit Mem.valid_access_valid_block; eauto.
        }
        exploit Mem.alloc_result; eauto.
        intro nbm1.
        assert (b1 ≠ b0).
        {
          intro.
          subst.
          xomega.
        }
        erewrite Mem.load_store_other; eauto.
        erewrite Mem.load_store_other; eauto.
        erewrite Mem.load_store_other; eauto.
        erewrite Mem.load_alloc_other; eauto.
        Lregset_simpl_tac.

        one_step_forward´.
        accessors_simpl.
        change (Int.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 4)))) with 4.
        unfold set; simpl.
        rewrite ikern, ihost.
        rewrite HST_FRAME4.
        reflexivity.


        one_step_forward´.
        unfold symbol_offset.
        unfold fundef.
        rewrite Hatomic_mcs_log_symbol.
        Lregset_simpl_tac.


        econstructor; eauto.
        eapply (LAsm.exec_step_prim_call _ b_atomic_mcs_log); eauto 1; trivial.
        econstructor.
        refine_split´; eauto 1.
        econstructor; eauto 1.
        simpl.
        econstructor.
        instantiate (20:= lock_index).
        instantiate (19:= cpuid).
        instantiate (18:= labd´).

        eauto.

        eauto.

        unfold tail_pos.
        unfold tail_pos in HST_TAIL.
        eassumption.

        unfold busy_pos.
        unfold busy_pos in HST_BUSY0.
        eassumption.

        unfold next_pos.
        unfold next_pos in HST_NEXT0.
        eassumption.

        unfold busy_pos.
        unfold busy_pos in HST_BUSY1.
        eassumption.

        unfold next_pos.
        unfold next_pos in HST_NEXT1.
        eassumption.

        unfold busy_pos.
        unfold busy_pos in HST_BUSY2.
        eassumption.

        unfold next_pos.
        unfold next_pos in HST_NEXT2.
        eassumption.

        unfold busy_pos.
        unfold busy_pos in HST_BUSY3.
        eassumption.

        unfold next_pos.
        unfold next_pos in HST_NEXT3.
        eassumption.

        unfold busy_pos.
        unfold busy_pos in HST_BUSY4.
        eassumption.

        unfold next_pos.
        unfold next_pos in HST_NEXT4.
        eassumption.

        unfold busy_pos.
        unfold busy_pos in HST_BUSY5.
        eassumption.

        unfold next_pos.
        unfold next_pos in HST_NEXT5.
        eassumption.

        unfold busy_pos.
        unfold busy_pos in HST_BUSY6.
        eassumption.

        unfold next_pos.
        unfold next_pos in HST_NEXT6.
        eassumption.

        unfold busy_pos.
        unfold busy_pos in HST_BUSY7.
        eassumption.

        unfold next_pos.
        unfold next_pos in HST_NEXT7.
        eassumption.

        eauto.

        repeat econstructor; eauto.

        simpl.
        change (Int.unsigned (Int.add Int.zero (Int.repr 0))) with 0.
        erewrite Mem.load_store_other; eauto.
        erewrite Mem.load_store_same; eauto.
        reflexivity.
        right.
        left.
        simpl.
        omega.
        Lregset_simpl_tac.
        change (Int.unsigned (Int.add Int.zero (Int.repr 4))) with 4.
        erewrite Mem.load_store_same; eauto.
        reflexivity.
        Lregset_simpl_tac.

        one_step_forward´.
        Lregset_simpl_tac.
        lift_trivial.
        unfold set; simpl.
        change (Int.unsigned (Int.add Int.zero (Int.repr 12))) with 12.
        change (Int.unsigned (Int.add Int.zero (Int.repr 8))) with 8.
        assert (Plt b (Mem.nextblock m)).
        {
          eapply Mem.store_valid_access_3 in H6.
          eapply Mem.valid_access_implies with (p2:= Nonempty) in H6; [|constructor].
          exploit Mem.valid_access_valid_block; eauto.
        }
        exploit Mem.alloc_result; eauto.
        intro nbm1.
        assert (b0 ≠ b).
        {
          intro.
          subst.
          generalize H5, H23; clearAll; intros.
          rewrite H23 in H5.
          xomega.
        }
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_same; eauto.
        erewrite register_type_load_result.

        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_same; eauto.
        erewrite register_type_load_result.

        rewrite HST_FREE.
        reflexivity.
        apply inv_reg_wt.
        right; left; omega.
        right; right; omega.
        right; right; omega.
        apply inv_reg_wt.
        right; right; omega.
        right; right; omega.

        Lregset_simpl_tac´ 7.

        one_step_forward´.
        Lregset_simpl_tac.

        eapply star_refl.
        simpl.
        reflexivity.
        reflexivity.

        assert (HFB: ∀ b delta, Mem.flat_inj (Mem.nextblock m) b ≠ Some (b0, delta)).
        {
          intros. unfold Mem.flat_inj.
          red; intros.
          destruct (plt b1 (Mem.nextblock m)).
          inv H5.
          rewrite (Mem.alloc_result _ _ _ _ _ HALC) in p.
          xomega.
          inv H5.
        }
        rewrite <- Hnextblock in HFB.
        eapply Mem.free_right_inject; eauto; [|intros; specialize (HFB b1 delta); apply HFB; trivial].

        rewrite Hnextblock.

        assert (bplt: Plt b (Mem.nextblock m)).
        {
          inv inv_inject_neutral.
          eapply genv_symb_range in H3.
          generalize inv_mem_valid, H3; clearAll.
          lift_simpl.
          unfold lift; simpl.
          intros.
          xomega.
        }
        assert (Mem.inject (Mem.flat_inj (Mem.nextblock m)) m m_frame4).
        {
          rewrite Hnextblock in HFB.
          repeat (eapply Mem.store_outside_inject; [ | | eassumption]
                ; [|intros b1 delta; intros; specialize (HFB b1 delta); apply HFB; trivial]).
          eapply Mem.alloc_right_inject; eauto.
          inv inv_inject_neutral.
          apply Mem.neutral_inject; trivial.
        }

        

        exploit (Mem.store_mapped_inject _ _ _ _ _ _ _ _ b 0 (Vint (Int.repr la)) H5 H6); eauto.
        unfold Mem.flat_inj.
        destruct (plt b (Mem.nextblock m)).
        reflexivity.
        xomega.
        intros [n_tl [store_tl inject_tl]].
        rewrite Z.add_0_r in store_tl.
        rewrite HST_TAIL in store_tl; inv store_tl.

        exploit (Mem.store_mapped_inject _ _ _ _ _ _ _ _ b 0 (Vint (Int.repr bs0)) inject_tl H7); eauto.
        unfold Mem.flat_inj.
        destruct (plt b (Mem.nextblock m)).
        reflexivity.
        xomega.
        intros [n_bs0 [store_bs0 inject_bs0]].
        rewrite Z.add_0_r in store_bs0.
        rewrite HST_BUSY0 in store_bs0; inv store_bs0.

        exploit (Mem.store_mapped_inject _ _ _ _ _ _ _ _ b 0 (Vint (Int.repr ne0)) inject_bs0 H8); eauto.
        unfold Mem.flat_inj.
        destruct (plt b (Mem.nextblock m)).
        reflexivity.
        xomega.
        intros [n_ne0 [store_ne0 inject_ne0]].
        rewrite Z.add_0_r in store_ne0.
        rewrite HST_NEXT0 in store_ne0; inv store_ne0.

        exploit (Mem.store_mapped_inject _ _ _ _ _ _ _ _ b 0 (Vint (Int.repr bs1)) inject_ne0 H9); eauto.
        unfold Mem.flat_inj.
        destruct (plt b (Mem.nextblock m)).
        reflexivity.
        xomega.
        intros [n_bs1 [store_bs1 inject_bs1]].
        rewrite Z.add_0_r in store_bs1.
        rewrite HST_BUSY1 in store_bs1; inv store_bs1.

        exploit (Mem.store_mapped_inject _ _ _ _ _ _ _ _ b 0 (Vint (Int.repr ne1)) inject_bs1 H10); eauto.
        unfold Mem.flat_inj.
        destruct (plt b (Mem.nextblock m)).
        reflexivity.
        xomega.
        intros [n_ne1 [store_ne1 inject_ne1]].
        rewrite Z.add_0_r in store_ne1.
        rewrite HST_NEXT1 in store_ne1; inv store_ne1.

        exploit (Mem.store_mapped_inject _ _ _ _ _ _ _ _ b 0 (Vint (Int.repr bs2)) inject_ne1 H11); eauto.
        unfold Mem.flat_inj.
        destruct (plt b (Mem.nextblock m)).
        reflexivity.
        xomega.
        intros [n_bs2 [store_bs2 inject_bs2]].
        rewrite Z.add_0_r in store_bs2.
        rewrite HST_BUSY2 in store_bs2; inv store_bs2.

        exploit (Mem.store_mapped_inject _ _ _ _ _ _ _ _ b 0 (Vint (Int.repr ne2)) inject_bs2 H12); eauto.
        unfold Mem.flat_inj.
        destruct (plt b (Mem.nextblock m)).
        reflexivity.
        xomega.
        intros [n_ne2 [store_ne2 inject_ne2]].
        rewrite Z.add_0_r in store_ne2.
        rewrite HST_NEXT2 in store_ne2; inv store_ne2.

        exploit (Mem.store_mapped_inject _ _ _ _ _ _ _ _ b 0 (Vint (Int.repr bs3)) inject_ne2 H13); eauto.
        unfold Mem.flat_inj.
        destruct (plt b (Mem.nextblock m)).
        reflexivity.
        xomega.
        intros [n_bs3 [store_bs3 inject_bs3]].
        rewrite Z.add_0_r in store_bs3.
        rewrite HST_BUSY3 in store_bs3; inv store_bs3.

        exploit (Mem.store_mapped_inject _ _ _ _ _ _ _ _ b 0 (Vint (Int.repr ne3)) inject_bs3 H14); eauto.
        unfold Mem.flat_inj.
        destruct (plt b (Mem.nextblock m)).
        reflexivity.
        xomega.
        intros [n_ne3 [store_ne3 inject_ne3]].
        rewrite Z.add_0_r in store_ne3.
        rewrite HST_NEXT3 in store_ne3; inv store_ne3.

        exploit (Mem.store_mapped_inject _ _ _ _ _ _ _ _ b 0 (Vint (Int.repr bs4)) inject_ne3 H15); eauto.
        unfold Mem.flat_inj.
        destruct (plt b (Mem.nextblock m)).
        reflexivity.
        xomega.
        intros [n_bs4 [store_bs4 inject_bs4]].
        rewrite Z.add_0_r in store_bs4.
        rewrite HST_BUSY4 in store_bs4; inv store_bs4.

        exploit (Mem.store_mapped_inject _ _ _ _ _ _ _ _ b 0 (Vint (Int.repr ne4)) inject_bs4 H16); eauto.
        unfold Mem.flat_inj.
        destruct (plt b (Mem.nextblock m)).
        reflexivity.
        xomega.
        intros [n_ne4 [store_ne4 inject_ne4]].
        rewrite Z.add_0_r in store_ne4.
        rewrite HST_NEXT4 in store_ne4; inv store_ne4.

        exploit (Mem.store_mapped_inject _ _ _ _ _ _ _ _ b 0 (Vint (Int.repr bs5)) inject_ne4 H17); eauto.
        unfold Mem.flat_inj.
        destruct (plt b (Mem.nextblock m)).
        reflexivity.
        xomega.
        intros [n_bs5 [store_bs5 inject_bs5]].
        rewrite Z.add_0_r in store_bs5.
        rewrite HST_BUSY5 in store_bs5; inv store_bs5.

        exploit (Mem.store_mapped_inject _ _ _ _ _ _ _ _ b 0 (Vint (Int.repr ne5)) inject_bs5 H18); eauto.
        unfold Mem.flat_inj.
        destruct (plt b (Mem.nextblock m)).
        reflexivity.
        xomega.
        intros [n_ne5 [store_ne5 inject_ne5]].
        rewrite Z.add_0_r in store_ne5.
        rewrite HST_NEXT5 in store_ne5; inv store_ne5.

        exploit (Mem.store_mapped_inject _ _ _ _ _ _ _ _ b 0 (Vint (Int.repr bs6)) inject_ne5 H19); eauto.
        unfold Mem.flat_inj.
        destruct (plt b (Mem.nextblock m)).
        reflexivity.
        xomega.
        intros [n_bs6 [store_bs6 inject_bs6]].
        rewrite Z.add_0_r in store_bs6.
        rewrite HST_BUSY6 in store_bs6; inv store_bs6.

        exploit (Mem.store_mapped_inject _ _ _ _ _ _ _ _ b 0 (Vint (Int.repr ne6)) inject_bs6 H20); eauto.
        unfold Mem.flat_inj.
        destruct (plt b (Mem.nextblock m)).
        reflexivity.
        xomega.
        intros [n_ne6 [store_ne6 inject_ne6]].
        rewrite Z.add_0_r in store_ne6.
        rewrite HST_NEXT6 in store_ne6; inv store_ne6.

        exploit (Mem.store_mapped_inject _ _ _ _ _ _ _ _ b 0 (Vint (Int.repr bs7)) inject_ne6 H21); eauto.
        unfold Mem.flat_inj.
        destruct (plt b (Mem.nextblock m)).
        reflexivity.
        xomega.
        intros [n_bs7 [store_bs7 inject_bs7]].
        rewrite Z.add_0_r in store_bs7.
        rewrite HST_BUSY7 in store_bs7; inv store_bs7.

        exploit (Mem.store_mapped_inject _ _ _ _ _ _ _ _ b 0 (Vint (Int.repr ne7)) inject_bs7 H22); eauto.
        unfold Mem.flat_inj.
        destruct (plt b (Mem.nextblock m)).
        reflexivity.
        xomega.
        intros [n_ne7 [store_ne7 inject_ne7]].
        rewrite Z.add_0_r in store_ne7.
        rewrite HST_NEXT7 in store_ne7; inv store_ne7.

        apply inject_ne7.


        generalize (Mem.nextblock_free _ _ _ _ _ HST_FREE); intro.
        rewrite H5, Hnextblock_m_next7.
        generalize (Mem.nextblock_alloc _ _ _ _ _ HALC); intro.
        rewrite Hnextblock.
        rewrite H23.
        xomega.

        unfold Lregset_fold; simpl.
        intros reg.
        repeat (rewrite Pregmap.gsspec).
        simpl_destruct_reg.
        exploit reg_false; try eassumption.
        intros HF; inv HF.
    Qed.

    Lemma mcs_log_code_correct:
      asm_spec_le (mcs_log ↦ mcs_log_spec_low)
                  (〚mcs_log ↦ mcs_log_function 〛 mcurid).
    Proof.
      eapply asm_sem_intro; try solve [ reflexivity | eexists; reflexivity ].
      intros. inv H.
      eapply make_program_make_globalenv in H0.
      exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
      intros Hstencil_matches.
      assert(Hfun: Genv.find_funct_ptr (Genv.globalenv p) b0 =
                   Some (Internal mcs_log_function)).
      {
        assert (Hmodule:
          get_module_function mcs_log ( mcs_log ↦ mcs_log_function)
            = OK (Some mcs_log_function)) by reflexivity.
        assert (HInternal:
          make_internal mcs_log_function
            = OK (AST.Internal mcs_log_function)) by reflexivity.
        eapply make_globalenv_get_module_function in H0; eauto.
        destruct H0 as [?[Hsymbol´ ?]].
        inv Hstencil_matches.
        rewrite stencil_matches_symbols in Hsymbol´.
        rewrite Hsymbol0 in Hsymbol´. inv Hsymbol´.
        assumption.
      }
      assert(Hnextblock: Mem.nextblock m´0 = Mem.nextblock m0).
      {
        rewrite (Mem.nextblock_store _ _ _ _ _ _ Hstore_next7); trivial.
        rewrite (Mem.nextblock_store _ _ _ _ _ _ Hstore_busy7); trivial.
        rewrite (Mem.nextblock_store _ _ _ _ _ _ Hstore_next6); trivial.
        rewrite (Mem.nextblock_store _ _ _ _ _ _ Hstore_busy6); trivial.
        rewrite (Mem.nextblock_store _ _ _ _ _ _ Hstore_next5); trivial.
        rewrite (Mem.nextblock_store _ _ _ _ _ _ Hstore_busy5); trivial.
        rewrite (Mem.nextblock_store _ _ _ _ _ _ Hstore_next4); trivial.
        rewrite (Mem.nextblock_store _ _ _ _ _ _ Hstore_busy4); trivial.
        rewrite (Mem.nextblock_store _ _ _ _ _ _ Hstore_next3); trivial.
        rewrite (Mem.nextblock_store _ _ _ _ _ _ Hstore_busy3); trivial.
        rewrite (Mem.nextblock_store _ _ _ _ _ _ Hstore_next2); trivial.
        rewrite (Mem.nextblock_store _ _ _ _ _ _ Hstore_busy2); trivial.
        rewrite (Mem.nextblock_store _ _ _ _ _ _ Hstore_next1); trivial.
        rewrite (Mem.nextblock_store _ _ _ _ _ _ Hstore_busy1); trivial.
        rewrite (Mem.nextblock_store _ _ _ _ _ _ Hstore_next0); trivial.
        rewrite (Mem.nextblock_store _ _ _ _ _ _ Hstore_busy0); trivial.
        rewrite (Mem.nextblock_store _ _ _ _ _ _ Hstore_la); trivial.
      }

      lift_trivial.
      unfold lift; simpl.
      rewrite <- Hnextblock.
      generalize Hspec; intro tmp.
      unfold atomic_mcs_log_spec in tmp.
      subdestruct.

      exploit mcs_log_spec; eauto 2.
      intros big_spec.
      eapply big_spec in Hhigh; try eassumption; try reflexivity.
      revert Hhigh.
      intros (f´ & m0´ & r_ & Hstep & Hincr & Hinject & Hnb & Hlessdef).
      split; [ reflexivity |].
      ∃ f´, (m0´, d´), r_.
      repeat split; try assumption.
      exact (PowersetMonad.powerset_fmap_intro m0´ Hinject).
    Qed.


    Lemma mcs_CAS_TAIL_spec:
      ∀ ge (s: stencil) (rs rs´: regset) b b´ m m´ labd labd´ lock_index cpuid new_tail succeed sig
             (HHIGH: high_level_invariant labd)
             (ikern: ikern labd = true)
             (ihost: ihost labd = true)
             (index_range: 0 ≤ (Int.unsigned lock_index) < lock_range)
             (cpuid_range: 0 ≤ (Int.unsigned cpuid) < TOTAL_CPU),
        find_symbol s mcs_CAS_TAIL = Some b´ →
        make_globalenv s (mcs_CAS_TAIL ↦ mcs_CAS_TAIL_function) mcurid = ret ge →
        rs PC = Vptr b´ Int.zero →
        atomic_mcs_CAS_spec (Int.unsigned lock_index) (Int.unsigned cpuid) labd = Some (labd´, (new_tail, succeed)) →
        find_symbol s MCS_LOCK_LOC = Some b →
        sig = AST.mksignature (AST.Tint::AST.Tint::nil) (Some AST.Tint) AST.cc_default →
        Asm.extcall_arguments rs m sig (Vint lock_index ::Vint cpuid ::nil) →
        Mem.store Mint32 m b (tail_pos (Int.unsigned lock_index)) (Vint (Int.repr new_tail)) = Some m´ →
        asm_invariant (mem := mwd LDATAOps) s rs (m, labd) →
        low_level_invariant (Mem.nextblock m) labd →
        let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
                                   :: RA :: nil)
                               (undef_regs (List.map preg_of destroyed_at_call) rs)) in
        
        ∃ f´ m´´ r_,
          lasm_step (mcs_CAS_TAIL ↦ mcs_CAS_TAIL_function) (mcurid (Hmwd:= Hmwd) (Hmem:= Hmem)) mcs_CAS_TAIL s rs
                    (m, labd) r_ (m´´, labd´)
          ∧ inject_incr (Mem.flat_inj (Mem.nextblock m´)) f´
          ∧ Memtype.Mem.inject f´ m´ m´´
          ∧ (Mem.nextblock m´ ≤ Mem.nextblock m´´)%positive
          ∧ (∀ l,
                 Val.lessdef (Pregmap.get l (rs´ # PC <- (rs RA)) # EAX <- (Vint (Int.repr succeed)))
                             (Pregmap.get l r_)).
    Proof.
      intros.
      inv H7.
      rename H8 into HLOW.
      inv H5.
      inv H9.
      inv H11.
      inv H8.
      simpl in H10.
      simpl in H11.

      caseEq(Mem.alloc m 0 16).
      intros m1 b0 HALC.
      exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
      intros Hstencil_matches.

      assert(Hnextblock: Mem.nextblock m´ = Mem.nextblock m).
      {
        rewrite (Mem.nextblock_store _ _ _ _ _ _ H6); trivial.
      }

      assert (Hblock: Ple (Genv.genv_next ge) b0 ∧ Plt b0 (Mem.nextblock m1)).
      {
        erewrite Mem.nextblock_alloc; eauto.
        apply Mem.alloc_result in HALC.
        rewrite HALC.
        inv inv_inject_neutral.
        inv Hstencil_matches.
        rewrite stencil_matches_genv_next.
        lift_unfold.
        split; xomega.
      }

      exploit Hatomic_mcs_CAS; eauto.
      intros [[b_atomic_mcs_CAS [Hatomic_mcs_CAS_symbol Hatomic_mcs_CAS_fun] prim_atomic_mcs_CAS]].

      specialize (Mem.valid_access_alloc_same _ _ _ _ _ HALC). intros.
      assert (HV1: Mem.valid_access m1 Mint32 b0 8 Freeable).
      {
        eapply H4; auto; simpl; try omega. unfold Z.divide.
        ∃ 2; omega.
      }
      eapply Mem.valid_access_implies with (p2:= Writable) in HV1; [|constructor].
      destruct (Mem.valid_access_store _ _ _ _ (rs ESP) HV1) as [m2 HST1].

      assert (HV2: Mem.valid_access m2 Mint32 b0 12 Freeable).
      {
        eapply Mem.store_valid_access_1; eauto.
        eapply H4; auto; simpl; try omega.
        unfold Z.divide. ∃ 3; omega.
      }
      eapply Mem.valid_access_implies with (p2:= Writable) in HV2; [|constructor].
      destruct (Mem.valid_access_store _ _ _ _ (rs RA) HV2) as [m3 HST2].

      assert (HV3: Mem.valid_access m3 Mint32 b0 0 Freeable).
      {
        eapply Mem.store_valid_access_1; eauto.
        eapply Mem.store_valid_access_1; eauto.
        eapply H4; auto; simpl; try omega. apply Zdivide_0.
      }
      eapply Mem.valid_access_implies with (p2:= Writable) in HV3; [|constructor].
      destruct (Mem.valid_access_store _ _ _ _ (Vint lock_index) HV3) as [m4 HST3].

      assert(Hnextblock4: Mem.nextblock m4 = Mem.nextblock m1).
      {
        rewrite (Mem.nextblock_store _ _ _ _ _ _ HST3); trivial.
        rewrite (Mem.nextblock_store _ _ _ _ _ _ HST2); trivial.
        rewrite (Mem.nextblock_store _ _ _ _ _ _ HST1); trivial.
      }

      assert (HVofs: Mem.valid_access m4 Mint32 b0 4 Freeable).
      {
        eapply Mem.store_valid_access_1; eauto.
        eapply Mem.store_valid_access_1; eauto.
        eapply Mem.store_valid_access_1; eauto.
        eapply H4; auto; simpl; try omega. ∃ 1.
        omega.
      }
      eapply Mem.valid_access_implies with (p2:= Writable) in HVofs; [|constructor].
      destruct (Mem.valid_access_store _ _ _ _ (Vint cpuid) HVofs) as [m5 HST4].

      assert(Hnextblockofs: Mem.nextblock m5 = Mem.nextblock m1).
      {
        rewrite (Mem.nextblock_store _ _ _ _ _ _ HST4); trivial.
      }

      assert (HV4: Mem.valid_access m5 Mint32 b (tail_pos (Int.unsigned lock_index)) Writable).
      {
        eapply Mem.store_valid_access_1; eauto.
        eapply Mem.store_valid_access_1; eauto.
        eapply Mem.store_valid_access_1; eauto.
        eapply Mem.store_valid_access_1; eauto.
        eapply Mem.valid_access_alloc_other; eauto.
        eapply Mem.store_valid_access_3; eauto.
      }
      destruct (Mem.valid_access_store _ _ _ _ (Vint (Int.repr new_tail)) HV4) as [m6 HST5].

      assert(Hnextblock6: Mem.nextblock m6 = Mem.nextblock m1).
      {
        rewrite (Mem.nextblock_store _ _ _ _ _ _ HST5); trivial.
      }

      assert (HV6: Mem.range_perm m6 b0 0 16 Cur Freeable).
      {
        unfold Mem.range_perm. intros.
        repeat (eapply Mem.perm_store_1; [eassumption|]).
        eapply Mem.perm_alloc_2; eauto.
      }

      destruct (Mem.range_perm_free _ _ _ _ HV6) as [m7 HFree].

      exploit Hmcs_CAS_TAIL; eauto 2. intros Hfunct.

      rewrite (Lregset_rewrite rs).
      refine_split´; try eassumption.
      rewrite H1.
      econstructor; eauto; subst.

      one_step_forward´.
      Lregset_simpl_tac.
      lift_trivial.
      change (Int.unsigned (Int.add Int.zero (Int.repr 8))) with 8.
      change (Int.unsigned (Int.add Int.zero (Int.repr 12))) with 12.
      unfold set; simpl.
      rewrite HALC. simpl.
      rewrite HST1. simpl. rewrite HST2.
      reflexivity.

      Lregset_simpl_tac´ 1.

      one_step_forward´.
      accessors_simpl.
      unfold Mem.loadv in H10.
      Lregset_simpl_tac.
      change (Int.add Int.zero (Int.repr 0)) with (Int.repr 0).
      case_eq (Val.add (rs ESP) (Vint (Int.repr 0))); intros;
      rewrite H5 in H10; try discriminate H10.
      rewrite ikern, ihost.
      unfold Asm.exec_load.
      unfold Mem.loadv.
      unfold eval_addrmode; simpl.
      Lregset_simpl_tac.
      unfold lift; simpl.
      assert (Plt b1 (Mem.nextblock m)).
      {
        eapply Mem.load_valid_access in H10.
        eapply Mem.valid_access_implies with (p2:= Nonempty) in H10; [|constructor].
        exploit Mem.valid_access_valid_block; eauto.
      }
      exploit Mem.alloc_result; eauto.
      intro nbm1.
      assert (b1 ≠ b0).
      {
        intro.
        subst.
        xomega.
      }
      erewrite Mem.load_store_other; eauto.
      erewrite Mem.load_store_other; eauto.
      erewrite Mem.load_alloc_other; eauto.
      Lregset_simpl_tac.

      one_step_forward´.
      accessors_simpl.
      change (Int.unsigned (Int.add Int.zero (Int.add Int.zero Int.zero))) with 0.
      unfold set; simpl.
      rewrite ikern, ihost.
      rewrite HST3.
      reflexivity.

      one_step_forward´.
      accessors_simpl.
      unfold Mem.loadv in H11.
      Lregset_simpl_tac.
      change (Int.add Int.zero (Int.repr 4)) with (Int.repr 4).
      case_eq (Val.add (rs ESP) (Vint (Int.repr 4))); intros;
      try rewrite H5 in H11; try discriminate H11.
      rewrite ikern, ihost.
      unfold Asm.exec_load.
      unfold Mem.loadv.
      unfold eval_addrmode; simpl.
      Lregset_simpl_tac.
      unfold lift; simpl.
      assert (Plt b1 (Mem.nextblock m)).
      {
        eapply Mem.load_valid_access in H11.
        eapply Mem.valid_access_implies with (p2:= Nonempty) in H11; [|constructor].
        exploit Mem.valid_access_valid_block; eauto.
      }
      exploit Mem.alloc_result; eauto.
      intro nbm1.
      assert (b1 ≠ b0).
      {
        intro.
        subst.
        xomega.
      }
      erewrite Mem.load_store_other; eauto.
      erewrite Mem.load_store_other; eauto.
      erewrite Mem.load_store_other; eauto.
      erewrite Mem.load_alloc_other; eauto.
      Lregset_simpl_tac.

      one_step_forward´.
      accessors_simpl.
      change (Int.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 4)))) with 4.
      unfold set; simpl.
      rewrite ikern, ihost.
      rewrite HST4.
      reflexivity.


      one_step_forward´.
      unfold symbol_offset. unfold fundef.
      rewrite Hatomic_mcs_CAS_symbol.
      Lregset_simpl_tac.

      econstructor; eauto.
      eapply (LAsm.exec_step_prim_call _ b_atomic_mcs_CAS); eauto 1; trivial.
      econstructor.
      refine_split´; eauto 1.
      econstructor; eauto 1.
      simpl.
      econstructor; eauto.
      instantiate (3 := cpuid).
      instantiate (1 := Int.repr succeed).
      rewrite Int.unsigned_repr.
      rewrite H2.
      reflexivity.
      assert (succeed = 1 ∨ succeed = 0).
      { functional inversion H2; tauto. }
      generalize max_unsigned_val; intros muval.
      destruct H5; subst; omega.

      repeat econstructor; eauto.
      simpl.
      change (Int.unsigned (Int.add Int.zero (Int.repr 0))) with 0.
      erewrite Mem.load_store_other; eauto.
      erewrite Mem.load_store_same; eauto.
      reflexivity.
      right. left. simpl. omega.
      Lregset_simpl_tac.
      change (Int.unsigned (Int.add Int.zero (Int.repr 4))) with 4.
      erewrite Mem.load_store_same; eauto.
      reflexivity.
      Lregset_simpl_tac.

      one_step_forward´.
      Lregset_simpl_tac.
      lift_trivial.
      unfold set; simpl.
      change (Int.unsigned (Int.add Int.zero (Int.repr 12))) with 12.
      change (Int.unsigned (Int.add Int.zero (Int.repr 8))) with 8.
      assert (Plt b (Mem.nextblock m)).
      {
        eapply Mem.store_valid_access_3 in H6.
        eapply Mem.valid_access_implies with (p2:= Nonempty) in H6; [|constructor].
        exploit Mem.valid_access_valid_block; eauto.
      }
      exploit Mem.alloc_result; eauto.
      intro nbm1.
      assert (b0 ≠ b).
      {
        intro.
        subst.
        generalize H5, H7; clearAll; intros.
        rewrite H7 in H5.
        xomega.
      }
      erewrite Mem.load_store_other; eauto; simpl.
      erewrite Mem.load_store_other; eauto; simpl.
      erewrite Mem.load_store_other; eauto; simpl.
      erewrite Mem.load_store_same; eauto.
      erewrite register_type_load_result.

      erewrite Mem.load_store_other; eauto; simpl.
      erewrite Mem.load_store_other; eauto; simpl.
      erewrite Mem.load_store_other; eauto; simpl.
      erewrite Mem.load_store_other; eauto; simpl.
      erewrite Mem.load_store_same; eauto.
      erewrite register_type_load_result.

      rewrite HFree. reflexivity.
      apply inv_reg_wt.
      right. left. omega.
      right. right. omega.
      right. right. omega.
      apply inv_reg_wt.
      right. right. omega.
      right. right. omega.

      Lregset_simpl_tac´ 7.

      one_step_forward´.
      Lregset_simpl_tac.

      eapply star_refl.
      simpl.
      reflexivity.
      reflexivity.

      assert (HFB: ∀ b delta, Mem.flat_inj (Mem.nextblock m) b ≠ Some (b0, delta)).
      {
        intros. unfold Mem.flat_inj.
        red; intros.
        destruct (plt b1 (Mem.nextblock m)). inv H5.
        rewrite (Mem.alloc_result _ _ _ _ _ HALC) in p.
        xomega.
        inv H5.
      }
      rewrite <- Hnextblock in HFB.
      eapply Mem.free_right_inject; eauto; [|intros; specialize (HFB b1 delta); apply HFB; trivial].

      rewrite Hnextblock.

      assert (bplt: Plt b (Mem.nextblock m)).
      {
        inv inv_inject_neutral.
        eapply genv_symb_range in H3.
        generalize inv_mem_valid, H3; clearAll.
        lift_simpl.
        unfold lift; simpl.
        intros.
        xomega.
      }
      assert (Mem.inject (Mem.flat_inj (Mem.nextblock m)) m m5).
      {
        rewrite Hnextblock in HFB.
        repeat (eapply Mem.store_outside_inject; [ | | eassumption]
                ; [|intros b1 delta; intros; specialize (HFB b1 delta); apply HFB; trivial]).
        eapply Mem.alloc_right_inject; eauto.
        inv inv_inject_neutral.
        apply Mem.neutral_inject; trivial.
      }
      exploit (Mem.store_mapped_inject _ _ _ _ _ _ _ _ b 0 (Vint (Int.repr new_tail)) H5 H6); eauto.
      unfold Mem.flat_inj.
      destruct (plt b (Mem.nextblock m)).
      reflexivity.
      xomega.
      intros[n2 [store inject]].
      rewrite Z.add_0_r in store.
      rewrite HST5 in store; inv store.
      apply inject.

      generalize (Mem.nextblock_free _ _ _ _ _ HFree); intro.
      rewrite H5, Hnextblock6.
      generalize (Mem.nextblock_alloc _ _ _ _ _ HALC); intro.
      rewrite Hnextblock.
      rewrite H7.
      xomega.

      unfold Lregset_fold; simpl.
      intros reg.
      repeat (rewrite Pregmap.gsspec).
      simpl_destruct_reg.
      exploit reg_false; try eassumption.
      intros HF; inv HF.
    Qed.

    Lemma mcs_CAS_TAIL_code_correct:
      asm_spec_le (mcs_CAS_TAIL ↦ mcs_CAS_TAIL_spec_low)
                  (〚mcs_CAS_TAIL ↦ mcs_CAS_TAIL_function 〛 mcurid).
    Proof.
      eapply asm_sem_intro; try solve [ reflexivity | eexists; reflexivity ].
      intros. inv H.
      eapply make_program_make_globalenv in H0.
      exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
      intros Hstencil_matches.
      assert(Hfun: Genv.find_funct_ptr (Genv.globalenv p) b0 =
                   Some (Internal mcs_CAS_TAIL_function)).
      {
        assert (Hmodule:
                  get_module_function mcs_CAS_TAIL ( mcs_CAS_TAIL ↦ mcs_CAS_TAIL_function)
                  = OK (Some mcs_CAS_TAIL_function)) by reflexivity.
        assert (HInternal:
                  make_internal mcs_CAS_TAIL_function
                  = OK (AST.Internal mcs_CAS_TAIL_function)) by reflexivity.
        eapply make_globalenv_get_module_function in H0; eauto.
        destruct H0 as [?[Hsymbol´ ?]].
        inv Hstencil_matches.
        rewrite stencil_matches_symbols in Hsymbol´.
        rewrite Hsymbol0 in Hsymbol´. inv Hsymbol´.
        assumption.
      }

      assert(Hnextblock: Mem.nextblock m´0 = Mem.nextblock m0).
      {
        rewrite (Mem.nextblock_store _ _ _ _ _ _ Hstore); trivial.
      }

      lift_trivial.
      unfold lift; simpl.
      rewrite <- Hnextblock.
      generalize Hspec; intro tmp.
      unfold atomic_mcs_CAS_spec in tmp.
      subdestruct; subst.

      -
        exploit mcs_CAS_TAIL_spec; eauto 2.
        intros (f´ & m0´ & r_ & Hstep & Hincr & Hinject & Hnb & Hlessdef).

        rewrite Int.repr_unsigned in Hlessdef.
        split; [ reflexivity |].
        ∃ f´, (m0´, d´), r_.
        repeat split; try assumption.
        exact (PowersetMonad.powerset_fmap_intro m0´ Hinject).

      -
        exploit mcs_CAS_TAIL_spec; eauto 2.
        intros (f´ & m0´ & r_ & Hstep & Hincr & Hinject & Hnb & Hlessdef).

        rewrite Int.repr_unsigned in Hlessdef.
        split; [ reflexivity |].
        ∃ f´, (m0´, d´), r_.
        repeat split; try assumption.
        exact (PowersetMonad.powerset_fmap_intro m0´ Hinject).
    Qed.

    Lemma mcs_SWAP_TAIL_spec:
      ∀ ge (s: stencil) (rs rs´: regset) b b´ m m0 m1 m´ labd labd´ bound lock_index cpuid prev_tail sig
             (HHIGH: high_level_invariant labd)
             (ikern: ikern labd = true)
             (ihost: ihost labd = true)
             (index_range: 0 ≤ (Int.unsigned lock_index) < lock_range)
             (curid_range: 0 ≤ (Int.unsigned cpuid) < TOTAL_CPU),
        find_symbol s mcs_SWAP_TAIL = Some b´ →
        make_globalenv s (mcs_SWAP_TAIL ↦ mcs_SWAP_TAIL_function) mcurid = ret ge →
        rs PC = Vptr b´ Int.zero →
        atomic_mcs_SWAP_spec (Int.unsigned bound) (Int.unsigned lock_index) (Int.unsigned cpuid) labd = Some (labd´, prev_tail) →
        find_symbol s MCS_LOCK_LOC = Some b →
        sig = AST.mksignature (AST.Tint::AST.Tint::AST.Tint::nil) (Some AST.Tint) AST.cc_default →
        Asm.extcall_arguments rs m sig (Vint bound :: Vint lock_index :: Vint cpuid ::nil) →
        Mem.store Mint32 m b (tail_pos (Int.unsigned lock_index)) (Vint cpuid) = Some m0 →
        Mem.store Mint32 m0 b (next_pos (Int.unsigned lock_index) (Int.unsigned cpuid)) (Vint (Int.repr NULL)) = Some m1 →
        Mem.store Mint32 m1 b (busy_pos (Int.unsigned lock_index) (Int.unsigned cpuid)) (Vint Int.one) = Some m´ →
        asm_invariant (mem := mwd LDATAOps) s rs (m, labd) →
        low_level_invariant (Mem.nextblock m) labd →
        let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
                                   :: RA :: nil)
                               (undef_regs (List.map preg_of destroyed_at_call) rs)) in
        ∃ f´ m´´ r_,
          lasm_step (mcs_SWAP_TAIL ↦ mcs_SWAP_TAIL_function) (mcurid (Hmwd:= Hmwd) (Hmem:= Hmem)) mcs_SWAP_TAIL s rs
                    (m, labd) r_ (m´´, labd´)
          ∧ inject_incr (Mem.flat_inj (Mem.nextblock m´)) f´
          ∧ Memtype.Mem.inject f´ m´ m´´
          ∧ (Mem.nextblock m´ ≤ Mem.nextblock m´´)%positive
          ∧ (∀ l,
                 Val.lessdef (Pregmap.get l (rs´ # PC <- (rs RA)) # EAX <- (Vint (Int.repr prev_tail)))
                             (Pregmap.get l r_)).
    Proof.
        intros.
        inv H9.
        rename H10 into HLOW.
        inv H5.
        inv H11.
        inv H13.
        inv H10.
        inv H14.
        inv H10.
        simpl in H12.
        simpl in H13.
        simpl in H14.

        caseEq(Mem.alloc m 0 20).
        intros m2 b0 HALC.
        exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
        intros Hstencil_matches.

        assert(Hnextblock: Mem.nextblock m´ = Mem.nextblock m).
        {
          rewrite (Mem.nextblock_store _ _ _ _ _ _ H8); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ H7); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ H6); trivial.
        }

        assert (Hblock: Ple (Genv.genv_next ge) b0 ∧ Plt b0 (Mem.nextblock m2)).
        {
          erewrite Mem.nextblock_alloc; eauto.
          apply Mem.alloc_result in HALC.
          rewrite HALC.
          inv inv_inject_neutral.
          inv Hstencil_matches.
          rewrite stencil_matches_genv_next.
          lift_unfold.
          split; xomega.
        }

        exploit Hatomic_mcs_SWAP; eauto.
        intros [[b_atomic_mcs_SWAP [Hatomic_mcs_SWAP_symbol Hatomic_mcs_SWAP_fun] prim_atomic_mcs_SWAP]].

        specialize (Mem.valid_access_alloc_same _ _ _ _ _ HALC). intros.
        assert (HV1: Mem.valid_access m2 Mint32 b0 12 Freeable).
        {
          eapply H4; auto; simpl; try omega. unfold Z.divide.
          ∃ 3; omega.
        }
        eapply Mem.valid_access_implies with (p2:= Writable) in HV1; [|constructor].
        destruct (Mem.valid_access_store _ _ _ _ (rs ESP) HV1) as [m3 HST1].

        assert (HV2: Mem.valid_access m3 Mint32 b0 16 Freeable).
        {
          eapply Mem.store_valid_access_1; eauto.
          eapply H4; auto; simpl; try omega.
          unfold Z.divide. ∃ 4; omega.
        }
        eapply Mem.valid_access_implies with (p2:= Writable) in HV2; [|constructor].
        destruct (Mem.valid_access_store _ _ _ _ (rs RA) HV2) as [m4 HST2].

        assert (HV3: Mem.valid_access m4 Mint32 b0 0 Freeable).
        {
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply H4; auto; simpl; try omega. apply Zdivide_0.
        }
        eapply Mem.valid_access_implies with (p2:= Writable) in HV3; [|constructor].
        destruct (Mem.valid_access_store _ _ _ _ (Vint bound) HV3) as [m5 HST3].

        assert(Hnextblock4: Mem.nextblock m5 = Mem.nextblock m2).
        {
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST3); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST2); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST1); trivial.
        }

        assert (HV4: Mem.valid_access m5 Mint32 b0 4 Freeable).
        {
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply H4; auto; simpl; try omega. ∃ 1.
          omega.
        }
        eapply Mem.valid_access_implies with (p2:= Writable) in HV4; [|constructor].
        destruct (Mem.valid_access_store _ _ _ _ (Vint lock_index) HV4) as [m6 HST4].

        assert(Hnextblock5: Mem.nextblock m6 = Mem.nextblock m2).
        {
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST4); trivial.
        }

        assert (HVofs: Mem.valid_access m6 Mint32 b0 8 Freeable).
        {
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply H4; auto; simpl; try omega. ∃ 2.
          omega.
        }
        eapply Mem.valid_access_implies with (p2:= Writable) in HVofs; [|constructor].
        destruct (Mem.valid_access_store _ _ _ _ (Vint cpuid) HVofs) as [m7 HST5].

        assert(Hnextblockofs: Mem.nextblock m7 = Mem.nextblock m2).
        {
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST5); trivial.
        }

        assert (HV5: Mem.valid_access m7 Mint32 b (tail_pos (Int.unsigned lock_index)) Writable).
        {
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.valid_access_alloc_other; eauto.
          eapply Mem.store_valid_access_3; eauto.
        }
        destruct (Mem.valid_access_store _ _ _ _ (Vint cpuid) HV5) as [m8 HST6].

        assert (HV6: Mem.valid_access m8 Mint32 b (next_pos (Int.unsigned lock_index) (Int.unsigned cpuid)) Writable).
        {
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.valid_access_alloc_other; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_3; eauto.
        }
        destruct (Mem.valid_access_store _ _ _ _ (Vint (Int.repr TOTAL_CPU)) HV6) as [m9 HST7].

        assert (HV7: Mem.valid_access m9 Mint32 b (busy_pos (Int.unsigned lock_index) (Int.unsigned cpuid)) Writable).
        {
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.valid_access_alloc_other; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_3; eauto.
        }
        destruct (Mem.valid_access_store _ _ _ _ (Vint Int.one) HV7) as [m10 HST8].

        assert(Hnextblock7: Mem.nextblock m10 = Mem.nextblock m2).
        {
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST8); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST7); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST6); trivial.
        }

        assert (HV8: Mem.range_perm m10 b0 0 20 Cur Freeable).
        {
          unfold Mem.range_perm. intros.
          repeat (eapply Mem.perm_store_1; [eassumption|]).
          eapply Mem.perm_alloc_2; eauto.
        }

        destruct (Mem.range_perm_free _ _ _ _ HV8) as [m11 HFree].

        exploit Hmcs_SWAP_TAIL; eauto 2. intros Hfunct.

        rewrite (Lregset_rewrite rs).
        refine_split´; try eassumption.
        rewrite H1.
        econstructor; eauto; subst.

        one_step_forward´.
        Lregset_simpl_tac.
        lift_trivial.
        change (Int.unsigned (Int.add Int.zero (Int.repr 12))) with 12.
        change (Int.unsigned (Int.add Int.zero (Int.repr 16))) with 16.
        unfold set; simpl.
        rewrite HALC. simpl.
        rewrite HST1.
        simpl.
        rewrite HST2.
        reflexivity.

        Lregset_simpl_tac´ 1.

        one_step_forward´.
        accessors_simpl.
        unfold Mem.loadv in H12.
        Lregset_simpl_tac.

        change (Int.add Int.zero (Int.repr 0)) with (Int.repr 0).
        case_eq (Val.add (rs ESP) (Vint (Int.repr 0))); intros;
        rewrite H5 in H12; try discriminate H12.
        rewrite ikern, ihost.
        unfold Asm.exec_load.
        unfold Mem.loadv.
        unfold eval_addrmode; simpl.
        Lregset_simpl_tac.
        unfold lift; simpl.
        assert (Plt b1 (Mem.nextblock m)).
        {
          eapply Mem.load_valid_access in H12.
          eapply Mem.valid_access_implies with (p2:= Nonempty) in H12; [|constructor].
          exploit Mem.valid_access_valid_block; eauto.
        }
        exploit Mem.alloc_result; eauto.
        intro nbm1.
        assert (b1 ≠ b0).
        {
          intro.
          subst.
          xomega.
        }
        erewrite Mem.load_store_other; eauto.
        erewrite Mem.load_store_other; eauto.
        erewrite Mem.load_alloc_other; eauto.
        Lregset_simpl_tac.

        one_step_forward´.
        accessors_simpl.
        change (Int.unsigned (Int.add Int.zero (Int.add Int.zero Int.zero))) with 0.
        unfold set; simpl.
        rewrite ikern, ihost.
        rewrite HST3.
        reflexivity.

        one_step_forward´.
        accessors_simpl.
        unfold Mem.loadv in H13.
        Lregset_simpl_tac.
        change (Int.add Int.zero (Int.repr 4)) with (Int.repr 4).
        case_eq (Val.add (rs ESP) (Vint (Int.repr 4))); intros;
        try rewrite H5 in H13; try discriminate H13.
        rewrite ikern, ihost.
        unfold Asm.exec_load.
        unfold Mem.loadv.
        unfold eval_addrmode; simpl.
        Lregset_simpl_tac.
        unfold lift; simpl.
        assert (Plt b1 (Mem.nextblock m)).
        {
          eapply Mem.load_valid_access in H13.
          eapply Mem.valid_access_implies with (p2:= Nonempty) in H13; [|constructor].
          exploit Mem.valid_access_valid_block; eauto.
        }
        exploit Mem.alloc_result; eauto.
        intro nbm1.
        assert (b1 ≠ b0).
        {
          intro.
          subst.
          xomega.
        }
        erewrite Mem.load_store_other; eauto.
        erewrite Mem.load_store_other; eauto.
        erewrite Mem.load_store_other; eauto.
        erewrite Mem.load_alloc_other; eauto.
        Lregset_simpl_tac.

        one_step_forward´.
        accessors_simpl.
        change (Int.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 4)))) with 4.
        unfold set; simpl.
        rewrite ikern, ihost.
        rewrite HST4.
        reflexivity.

        one_step_forward´.
        accessors_simpl.
        unfold Mem.loadv in H14.
        Lregset_simpl_tac.
        change (Int.add Int.zero (Int.repr 8)) with (Int.repr 8).
        case_eq (Val.add (rs ESP) (Vint (Int.repr 8))); intros;
        try rewrite H5 in H14; try discriminate H14.
        rewrite ikern, ihost.
        unfold Asm.exec_load.
        unfold Mem.loadv.
        unfold eval_addrmode; simpl.
        Lregset_simpl_tac.
        unfold lift; simpl.
        assert (Plt b1 (Mem.nextblock m)).
        {
          eapply Mem.load_valid_access in H14.
          eapply Mem.valid_access_implies with (p2:= Nonempty) in H14; [|constructor].
          exploit Mem.valid_access_valid_block; eauto.
        }
        exploit Mem.alloc_result; eauto.
        intro nbm1.
        assert (b1 ≠ b0).
        {
          intro.
          subst.
          xomega.
        }
        erewrite Mem.load_store_other; eauto.
        erewrite Mem.load_store_other; eauto.
        erewrite Mem.load_store_other; eauto.
        erewrite Mem.load_store_other; eauto.
        erewrite Mem.load_alloc_other; eauto.
        Lregset_simpl_tac.

        one_step_forward´.
        accessors_simpl.
        change (Int.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 8)))) with 8.
        unfold set; simpl.
        rewrite ikern, ihost.
        rewrite HST5.
        reflexivity.


        one_step_forward´.
        unfold symbol_offset. unfold fundef.
        rewrite Hatomic_mcs_SWAP_symbol.
        Lregset_simpl_tac.

        econstructor; eauto.
        eapply (LAsm.exec_step_prim_call _ b_atomic_mcs_SWAP); eauto 1; trivial.
        econstructor.
        refine_split´; eauto 1.
        econstructor; eauto 1.
        simpl.
        econstructor.
        instantiate (5:= bound).
        instantiate (4:= lock_index).
        instantiate (3:= cpuid).
        instantiate (2:= labd´).
        instantiate (1:= Int.repr prev_tail).
        rewrite Int.unsigned_repr.
        eauto.
        assert (0 ≤ prev_tail ≤ TOTAL_CPU).
        { functional inversion H2; assumption. }
        rewrite max_unsigned_val; omega.
        eauto.
        unfold tail_pos.
        unfold tail_pos in HST6.
        Opaque Z.mul.
        simpl. exact HST6.
        unfold next_pos.
        unfold next_pos in HST7.
        simpl. exact HST7.
        unfold busy_pos.
        unfold next_pos in HST8.
        simpl. exact HST8.
        eauto.

        repeat econstructor; eauto.

        simpl.
        change (Int.unsigned (Int.add Int.zero (Int.repr (4 × 0)))) with 0.
        erewrite Mem.load_store_other; eauto.
        erewrite Mem.load_store_other; eauto.
        erewrite Mem.load_store_same; eauto.
        reflexivity.
        right. left. simpl. omega.
        right. left. simpl. omega.
        Lregset_simpl_tac.

        change (Int.unsigned (Int.add Int.zero (Int.repr (4 × 1)))) with 4.
        erewrite Mem.load_store_other; eauto.
        erewrite Mem.load_store_same; eauto.
        reflexivity.
        right. left. simpl. omega.
        Lregset_simpl_tac.

        change (Int.unsigned (Int.add Int.zero (Int.repr (4 × 2)))) with 8.
        erewrite Mem.load_store_same; eauto.
        reflexivity.
        Lregset_simpl_tac.

        change (Int.add
                  (Int.add
                     (Int.add
                        (Int.add
                           (Int.add
                              (Int.add (Int.add (Int.repr 1) Int.one)
                                       Int.one) Int.one) Int.one) Int.one)
                     Int.one) Int.one) with (Int.repr 8).

        one_step_forward´.
        Lregset_simpl_tac.
        lift_trivial.
        unfold set; simpl.
        change (Int.unsigned (Int.add Int.zero (Int.repr 16))) with 16.
        change (Int.unsigned (Int.add Int.zero (Int.repr 12))) with 12.
        assert (Plt b (Mem.nextblock m)).
        {
          eapply Mem.store_valid_access_3 in H6.
          eapply Mem.valid_access_implies with (p2:= Nonempty) in H6; [|constructor].
          exploit Mem.valid_access_valid_block; eauto.
        }
        exploit Mem.alloc_result; eauto.
        intro nbm1.
        assert (b0 ≠ b).
        {
          intro.
          subst.
          generalize H5, H9; clearAll; intros.
          rewrite H9 in H5.
          xomega.
        }
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_same; eauto.
        erewrite register_type_load_result.

        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_same; eauto.
        erewrite register_type_load_result.

        rewrite HFree. reflexivity.
        apply inv_reg_wt.
        right. left. omega.
        right. right. omega.
        right. right. omega.
        right. right. omega.
        apply inv_reg_wt.
        right. right. omega.
        right. right. omega.
        right. right. omega.

        Lregset_simpl_tac´ 9.

        one_step_forward´.
        Lregset_simpl_tac.

        eapply star_refl.
        simpl.
        reflexivity.
        reflexivity.

        assert (HFB: ∀ b delta, Mem.flat_inj (Mem.nextblock m) b ≠ Some (b0, delta)).
        {
          intros. unfold Mem.flat_inj.
          red; intros.
          destruct (plt b1 (Mem.nextblock m)). inv H5.
          rewrite (Mem.alloc_result _ _ _ _ _ HALC) in p.
          xomega.
          inv H5.
        }
        rewrite <- Hnextblock in HFB.
        eapply Mem.free_right_inject; eauto; [|intros; specialize (HFB b1 delta); apply HFB; trivial].

        rewrite Hnextblock.

        assert (bplt: Plt b (Mem.nextblock m)).
        {
          inv inv_inject_neutral.
          eapply genv_symb_range in H3.
          generalize inv_mem_valid, H3; clearAll.
          lift_simpl.
          unfold lift; simpl.
          intros.
          xomega.
        }
        assert (Mem.inject (Mem.flat_inj (Mem.nextblock m)) m m7).
        {
          rewrite Hnextblock in HFB.
          repeat (eapply Mem.store_outside_inject; [ | | eassumption]
                ; [|intros b1 delta; intros; specialize (HFB b1 delta); apply HFB; trivial]).
          eapply Mem.alloc_right_inject; eauto.
          inv inv_inject_neutral.
          apply Mem.neutral_inject; trivial.
        }
        exploit (Mem.store_mapped_inject _ _ _ _ _ _ _ _ b 0 (Vint cpuid) H5 H6); eauto.
        unfold Mem.flat_inj.
        destruct (plt b (Mem.nextblock m)).
        reflexivity.
        xomega.
        intros[n2 [store inject]].
        rewrite Z.add_0_r in store.
        rewrite HST6 in store; inv store.

        exploit (Mem.store_mapped_inject _ _ _ _ _ _ _ _ b 0 (Vint (Int.repr TOTAL_CPU)) inject H7); eauto.
        unfold Mem.flat_inj.
        destruct (plt b (Mem.nextblock m)).
        reflexivity.
        xomega.
        intros[n3 [store2 inject2]].
        rewrite Z.add_0_r in store2.
        rewrite HST7 in store2; inv store2.

        exploit (Mem.store_mapped_inject _ _ _ _ _ _ _ _ b 0 (Vint Int.one) inject2 H8); eauto.
        unfold Mem.flat_inj.
        destruct (plt b (Mem.nextblock m)).
        reflexivity.
        xomega.
        intros[n4 [store3 inject3]].
        rewrite Z.add_0_r in store3.
        rewrite HST8 in store3; inv store3.
        apply inject3.

        generalize (Mem.nextblock_free _ _ _ _ _ HFree); intro.
        rewrite H5, Hnextblock7.
        generalize (Mem.nextblock_alloc _ _ _ _ _ HALC); intro.
        rewrite Hnextblock.
        rewrite H9.
        xomega.

        unfold Lregset_fold; simpl.
        intros reg.
        repeat (rewrite Pregmap.gsspec).
        simpl_destruct_reg.
        exploit reg_false; try eassumption.
        intros HF; inv HF.
    Qed.

    Lemma mcs_SWAP_TAIL_code_correct:
      asm_spec_le (mcs_SWAP_TAIL ↦ mcs_SWAP_TAIL_spec_low)
                  (〚mcs_SWAP_TAIL ↦ mcs_SWAP_TAIL_function 〛 mcurid).
    Proof.
      eapply asm_sem_intro; try solve [ reflexivity | eexists; reflexivity ].
      intros. inv H.
      eapply make_program_make_globalenv in H0.
      exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
      intros Hstencil_matches.
      assert(Hfun: Genv.find_funct_ptr (Genv.globalenv p) b0 =
                     Some (Internal mcs_SWAP_TAIL_function)).
      {
        assert (Hmodule:
          get_module_function mcs_SWAP_TAIL ( mcs_SWAP_TAIL ↦ mcs_SWAP_TAIL_function)
            = OK (Some mcs_SWAP_TAIL_function)) by reflexivity.
        assert (HInternal:
          make_internal mcs_SWAP_TAIL_function
            = OK (AST.Internal mcs_SWAP_TAIL_function)) by reflexivity.
        eapply make_globalenv_get_module_function in H0; eauto.
        destruct H0 as [?[Hsymbol´ ?]].
        inv Hstencil_matches.
        rewrite stencil_matches_symbols in Hsymbol´.
        rewrite Hsymbol0 in Hsymbol´. inv Hsymbol´.
        assumption.
      }
      assert(Hnextblock: Mem.nextblock m´0 = Mem.nextblock m0).
      {
        rewrite (Mem.nextblock_store _ _ _ _ _ _ Hstore_busy); trivial.
        rewrite (Mem.nextblock_store _ _ _ _ _ _ Hstore_next); trivial.
        rewrite (Mem.nextblock_store _ _ _ _ _ _ Hstore_la); trivial.
      }

      lift_trivial.
      unfold lift; simpl.
      rewrite <- Hnextblock.
      generalize Hspec; intro tmp.
      unfold atomic_mcs_SWAP_spec in tmp.
      subdestruct.
      -
        exploit mcs_SWAP_TAIL_spec; eauto 2.
        intros (f´ & m0´ & r_ & Hstep & Hincr & Hinject & Hnb & Hlessdef).

        rewrite Int.repr_unsigned in Hlessdef.
        split; [ reflexivity |].
        ∃ f´, (m0´, d´), r_.
        repeat split; try assumption.
        exact (PowersetMonad.powerset_fmap_intro m0´ Hinject).
      -
        exploit mcs_SWAP_TAIL_spec; eauto 2.
        intros (f´ & m0´ & r_ & Hstep & Hincr & Hinject & Hnb & Hlessdef).

        rewrite Int.repr_unsigned in Hlessdef.
        split; [ reflexivity |].
        ∃ f´, (m0´, d´), r_.
        repeat split; try assumption.
        exact (PowersetMonad.powerset_fmap_intro m0´ Hinject).
    Qed.

  End WITHMEM.

End ASM_VERIFICATION.