Library mcertikos.ticketlog.TicketLockIntroGenAsm


This file provide the contextual refinement proof between MPTInit layer and MPTBit layer
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 MCurID.
Require Import TicketLockIntroGenSpec.
Require Import TicketLockIntroGenAsmSource.
Require Import TicketLockIntroGenAsmData.

Require Import LAsmModuleSemSpec.
Require Import LRegSet.
Require Import AbstractDataType.

Section ASM_VERIFICATION.

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

  Context `{real_params: RealParams}.
  Context `{oracle_prop: MultiOracleProp}.

    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 get_now_spec:
           ge (s: stencil) (rs rs´: regset) b m m0 labd labd´ i ofs pos n t sig
                 (HHIGH: high_level_invariant labd)
                 (Hpos: index2Z (Int.unsigned i) (Int.unsigned ofs) = Some pos)
                 (ikern: ikern labd = true)
                 (ihost: ihost labd = true),
            find_symbol s get_now = Some
            make_globalenv s (get_now get_now_function) mcurid = ret ge
            rs PC = Vptr Int.zero
            log_get_spec (Int.unsigned i) (Int.unsigned ofs) labd = Some (labd´, (t, n))
            find_symbol s TICKET_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 i ::Vint ofs ::nil) →
            Mem.store Mint32 m b (pos × 8) (Vint (Int.repr t)) = Some m0
            Mem.store Mint32 m0 b (pos × 8 + 4) (Vint (Int.repr n)) = Some
            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
            
             m´´ r_,
              lasm_step (get_now get_now_function) (mcurid (Hmwd:= Hmwd) (Hmem:= Hmem)) get_now s rs
                        (m, labd) r_ (m´´, labd´)
               inject_incr (Mem.flat_inj (Mem.nextblock ))
               Memtype.Mem.inject m´´
               (Mem.nextblock Mem.nextblock m´´)%positive
               ( l,
                    Val.lessdef (Pregmap.get l (rs´ # PC <- (rs RA)) # EAX <- (Vint (Int.repr n)))
                                (Pregmap.get l r_)).
      Proof.
        intros.
        inv H8.
        rename H9 into HLOW.
        inv H5.
        inv H10.
        inv H12.
        inv H9.
        simpl in H11.
        simpl in H12.

        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 = Mem.nextblock m).
        {
          rewrite (Mem.nextblock_store _ _ _ _ _ _ H7); trivial.
          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 Hlog_get; eauto.
        intros [[b_log_get [Hlog_get_symbol Hlog_get_fun] prim_log_get]].

        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 i) 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 ofs) HVofs) as [mofs HSTofs].

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

        assert (HV4: Mem.valid_access mofs Mint32 b (pos × 8) 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 t)) HV4) as [m5 HST4].
        assert (HV5: Mem.valid_access m5 Mint32 b (pos × 8 + 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.valid_access_alloc_other; eauto.
          eapply Mem.store_valid_access_2; eauto.
          eapply Mem.store_valid_access_3; eauto.
        }
        eapply Mem.valid_access_implies with (p2:= Writable) in HV5; [|constructor].
        destruct (Mem.valid_access_store _ _ _ _ (Vint (Int.repr n)) HV5) as [m6 HST5].

        assert(Hnextblock6: Mem.nextblock m6 = Mem.nextblock m1).
        {
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST5); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST4); 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 Hget_now; eauto 2. intros Hfunct.

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

        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 H11.
        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;
        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_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 H12.
        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 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_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 HSTofs.
        reflexivity.

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

        econstructor; eauto.
        eapply (LAsm.exec_step_prim_call _ b_log_get); eauto 1; trivial.
        econstructor.
        refine_split´; eauto 1.
        econstructor; eauto 1. simpl.
        econstructor; 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.

        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, H8; clearAll; intros.
          rewrite H8 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_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_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.
        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 mofs).
        {
          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 t)) 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 HST4 in store; inv store.
        exploit (Mem.store_mapped_inject _ _ _ _ _ _ _ _ b 0 (Vint (Int.repr n)) 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 HST5 in store2; inv store2.
        apply inject2.

        generalize (Mem.nextblock_free _ _ _ _ _ HFree); intro.
        rewrite H5, Hnextblock6.
        generalize (Mem.nextblock_alloc _ _ _ _ _ HALC); intro.
        rewrite Hnextblock.
        rewrite H8.
        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 get_now_code_correct:
      asm_spec_le (get_now get_now_spec_low)
                  ( get_now get_now_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 get_now_function)).
      {
        assert (Hmodule:
          get_module_function get_now (get_now get_now_function)
            = OK (Some get_now_function)) by reflexivity.
        assert (HInternal:
          make_internal get_now_function
            = OK (AST.Internal get_now_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 _ _ _ _ _ _ Hstore1); trivial.
        rewrite (Mem.nextblock_store _ _ _ _ _ _ Hstore0); trivial.
      }

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

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

      split; [ reflexivity |].
       , (m0´, ), r_.
      repeat split; try assumption.
      exact (PowersetMonad.powerset_fmap_intro m0´ Hinject).
    Qed.

    Lemma incr_ticket_spec:
       ge (s: stencil) (rs rs´: regset) b m m0 labd labd´ i ofs pos n t sig bound
             (HHIGH: high_level_invariant labd)
             (Hpos: index2Z (Int.unsigned i) (Int.unsigned ofs) = Some pos)
             (ikern: ikern labd = true)
             (ihost: ihost labd = true),
        find_symbol s incr_ticket = Some
        make_globalenv s (incr_ticket incr_ticket_function) mcurid = ret ge
        rs PC = Vptr Int.zero
        atomic_FAI_spec (Int.unsigned bound) (Int.unsigned i) (Int.unsigned ofs) labd = Some (labd´, (t, n))
        find_symbol s TICKET_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 i ::Vint ofs ::nil) →
        Mem.store Mint32 m b (pos × 8) (Vint (Int.repr (Int.unsigned (Int.repr (t + 1))))) = Some m0
        Mem.store Mint32 m0 b (pos × 8 + 4) (Vint (Int.repr n)) = Some
        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
        
         m´´ r_,
          lasm_step (incr_ticket incr_ticket_function) (mcurid (Hmwd:= Hmwd) (Hmem:= Hmem)) incr_ticket s rs
                    (m, labd) r_ (m´´, labd´)
           inject_incr (Mem.flat_inj (Mem.nextblock ))
           Memtype.Mem.inject m´´
           (Mem.nextblock Mem.nextblock m´´)%positive
           ( l,
                Val.lessdef (Pregmap.get l (rs´ # PC <- (rs RA)) # EAX <- (Vint (Int.repr t)))
                            (Pregmap.get l r_)).
    Proof.
      intros. inv H8.
      rename H9 into HLOW.
      inv H5.
      inv H10.
      inv H12.
      inv H9.
      inv H13.
      inv H9.
      simpl in H11.
      simpl in H12.
      simpl in H13.

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

      assert(Hnextblock: Mem.nextblock = Mem.nextblock m).
      {
        rewrite (Mem.nextblock_store _ _ _ _ _ _ H7); trivial.
        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_FAI; eauto.
      intros [[b_atomic_FAI [Hatomic_FAI_symbol Hatomic_FAI_fun] prim_atomic_FAI]].

      specialize (Mem.valid_access_alloc_same _ _ _ _ _ HALC). intros.
      assert (HV1: Mem.valid_access m1 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 [m2 HST1].

      assert (HV2: Mem.valid_access m2 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 [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 bound) 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 (HVi: 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 HVi; [|constructor].
      destruct (Mem.valid_access_store _ _ _ _ (Vint i) HVi) as [mi HSTi].

      assert(Hnextblocki: Mem.nextblock mi= Mem.nextblock m1).
      {
        rewrite (Mem.nextblock_store _ _ _ _ _ _ HSTi); trivial.
      }

      assert (HVofs: Mem.valid_access mi 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 ofs) HVofs) as [mofs HSTofs].

      assert(Hnextblockofs: Mem.nextblock mofs = Mem.nextblock m1).
      {
        rewrite (Mem.nextblock_store _ _ _ _ _ _ HSTofs); trivial.
      }
      
      assert (HV4: Mem.valid_access mofs Mint32 b (pos × 8) 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 (Int.repr (t + 1))) HV4) as [m5 HST4].
      assert (HV5: Mem.valid_access m5 Mint32 b (pos × 8 + 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.valid_access_alloc_other; eauto.
        eapply Mem.store_valid_access_2; eauto.
        eapply Mem.store_valid_access_3; eauto.
      }
      eapply Mem.valid_access_implies with (p2:= Writable) in HV5; [|constructor].
      destruct (Mem.valid_access_store _ _ _ _ (Vint (Int.repr n)) HV5) as [m6 HST5].

      assert(Hnextblock6: Mem.nextblock m6 = Mem.nextblock m1).
      {
        rewrite (Mem.nextblock_store _ _ _ _ _ _ HST5); trivial.
        rewrite (Mem.nextblock_store _ _ _ _ _ _ HST4); trivial.
      }
      
      assert (HV6: Mem.range_perm m6 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 _ _ _ _ HV6) as [m7 HFree].

      exploit Hincr_ticket; eauto 2. intros Hfunct.

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

      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 H11.
      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;
      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_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 H12.
      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 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_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 HSTi.
      reflexivity.

      one_step_forward´.
      accessors_simpl.
      unfold Mem.loadv in H13.
      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 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_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 HSTofs.
      reflexivity.

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

      econstructor; eauto.
      eapply (LAsm.exec_step_prim_call _ b_atomic_FAI); eauto 1; trivial.
      econstructor.
      refine_split´; eauto 1.
      econstructor; eauto 1. simpl.
      econstructor; 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_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))) 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 8))) with 8.
      erewrite Mem.load_store_same; eauto.
      reflexivity.
      Lregset_simpl_tac.
      change (Int.add
                (Int.add
                   (Int.add (Int.add (Int.repr 4) 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, H8; clearAll; intros.
        rewrite H8 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_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_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.
      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 mofs).
      {
        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 (t + 1))) H5 H6); eauto.
      unfold Mem.flat_inj.
      destruct (plt b (Mem.nextblock m)).
      reflexivity.
      xomega.
      rewrite Int.repr_unsigned.
      econstructor.
      intros[n2 [store inject]].
      rewrite Z.add_0_r in store.
      rewrite HST4 in store; inv store.
      exploit (Mem.store_mapped_inject _ _ _ _ _ _ _ _ b 0 (Vint (Int.repr n)) 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 HST5 in store2; inv store2.
      apply inject2.

      generalize (Mem.nextblock_free _ _ _ _ _ HFree); intro.
      rewrite H5, Hnextblock6.
      generalize (Mem.nextblock_alloc _ _ _ _ _ HALC); intro.
      rewrite Hnextblock.
      rewrite H8.
      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 incr_ticket_code_correct:
      asm_spec_le (incr_ticket incr_ticket_spec_low)
                  ( incr_ticket incr_ticket_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 incr_ticket_function)).
      {
        assert (Hmodule:
          get_module_function incr_ticket (incr_ticket incr_ticket_function)
            = OK (Some incr_ticket_function)) by reflexivity.
        assert (HInternal:
          make_internal incr_ticket_function
            = OK (AST.Internal incr_ticket_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 _ _ _ _ _ _ Hstore1); trivial.
        rewrite (Mem.nextblock_store _ _ _ _ _ _ Hstore0); trivial.
      }

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

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

      split; [ reflexivity |].
       , (m0´, ), r_.
      repeat split; try assumption.
      exact (PowersetMonad.powerset_fmap_intro m0´ Hinject).
    Qed.

  End WITHMEM.

End ASM_VERIFICATION.