Require Import compcert.lib.Coqlib.
Require Import compcert.lib.Maps.
Require Import compcert.lib.Integers.
Require Import compcert.common.Values.
Require Import compcert.common.Memory.
Require Import compcert.common.Events.
Require Import compcert.common.AST.
Require Import compcert.common.Globalenvs.
Require Import Lia.

Require Import VST.msl.Extensionality.
Require Import VST.sepcomp.mem_lemmas.
Require Import VST.sepcomp.semantics.
Require Import VST.sepcomp.semantics_lemmas.

Require Import Coq.micromega.Lia.

(** * Semantics annotated with Owens-style trace*)
Inductive mem_event :=
  Write : forall (b : block) (ofs : Z) (bytes : list memval), mem_event
| Read : forall (b:block) (ofs n:Z) (bytes: list memval), mem_event
| Alloc: forall (b:block)(lo hi:Z), mem_event
(*| Lock: drf_event
| Unlock: drf_event  -- these events are not generated by core steps*)
| Free: forall (l: list (block * Z * Z)), mem_event.

Fixpoint ev_elim (m:mem) (T: list mem_event) (m':mem):Prop :=
  match T with
   nil => m'=m
 | (Read b ofs n bytes :: R) => Mem.loadbytes m b ofs n = Some bytes /\ ev_elim m R m'
 | (Write b ofs bytes :: R) => exists m'', Mem.storebytes m b ofs bytes = Some m'' /\ ev_elim m'' R m'
 | (Alloc b lo hi :: R) => exists m'', Mem.alloc m lo hi = (m'',b) /\ ev_elim m'' R m'
 | (Free l :: R) => exists m'', Mem.free_list m l = Some m'' /\ ev_elim m'' R m'
  end.

Definition pmax (popt qopt: option permission): option permission :=
  match popt, qopt with
    _, None => popt
  | None, _ => qopt
  | Some p, Some q => if Mem.perm_order_dec p q then Some p else Some q
  end.

Lemma po_pmax_I p q1 q2:
  Mem.perm_order'' p q1 -> Mem.perm_order'' p q2 -> Mem.perm_order'' p (pmax q1 q2).
Proof.
  intros. destruct q1; destruct q2; simpl in *; trivial.
  destruct (Mem.perm_order_dec p0 p1); trivial.
Qed.

Fixpoint cur_perm (l: block * Z) (T: list mem_event): option permission :=
  match T with
      nil => None
    | (mu :: R) =>
          let popt := cur_perm l R in
          match mu, l with
            | (Read b ofs n bytes), (b',ofs') =>
                 pmax (if eq_block b b' && zle ofs ofs' && zlt ofs' (ofs+n)
                       then Some Readable else None) popt
            | (Write b ofs bytes), (b',ofs') =>
                 pmax (if eq_block b b' && zle ofs ofs' && zlt ofs' (ofs+ Zlength bytes)
                       then Some Writable else None) popt
            | (Alloc b lo hi), (b',ofs') =>  (*we don't add a constraint relating lo/hi/ofs*)
                 if eq_block b b' then None else popt
            | (Free l), (b',ofs') =>
                 List.fold_right (fun tr qopt => match tr with (b,lo,hi) =>
                                                   if eq_block b b' && zle lo ofs' && zlt ofs' hi
                                                   then Some Freeable else qopt
                                                end)
                                 popt l
          end
  end.

Lemma po_None popt: Mem.perm_order'' popt None.
Proof. destruct popt; simpl; trivial. Qed.

Lemma ev_perm b ofs: forall T m m', ev_elim m T m' ->
      Mem.perm_order'' ((Mem.mem_access m) !! b ofs Cur) (cur_perm (b,ofs) T).
Proof.
induction T; simpl; intros.
+ subst. apply po_None.
+ destruct a.
  - (*Store*)
     destruct H as [m'' [SB EV]]. specialize (IHT _ _ EV); clear EV.
     rewrite (Mem.storebytes_access _ _ _ _ _ SB) in *.
     eapply po_pmax_I; try eassumption.
     remember (eq_block b0 b && zle ofs0 ofs && zlt ofs (ofs0 + Zlength bytes)) as d.
     destruct d; try solve [apply po_None].
     destruct (eq_block b0 b); simpl in *; try discriminate.
     destruct (zle ofs0 ofs); simpl in *; try discriminate.
     destruct (zlt ofs (ofs0 + Zlength bytes)); simpl in *; try discriminate.
     rewrite Zlength_correct in *.
     apply Mem.storebytes_range_perm in SB.
     exploit (SB ofs); try lia.
     intros; subst; assumption.
  - (*Load*)
     destruct H as [LB EV]. specialize (IHT _ _ EV); clear EV.
     eapply po_pmax_I; try eassumption.
     remember (eq_block b0 b && zle ofs0 ofs && zlt ofs (ofs0 + n)) as d.
     destruct d; try solve [apply po_None].
     destruct (eq_block b0 b); simpl in *; try discriminate.
     destruct (zle ofs0 ofs); simpl in *; try discriminate.
     destruct (zlt ofs (ofs0 + n)); simpl in *; try discriminate.
     apply Mem.loadbytes_range_perm in LB.
     exploit (LB ofs); try lia.
     intros; subst; assumption.
  - (*Alloc*)
     destruct H as [m'' [ALLOC EV]]. specialize (IHT _ _ EV); clear EV.
     destruct (eq_block b0 b); subst; try solve [apply po_None].
     eapply po_trans; try eassumption.
     remember ((Mem.mem_access m'') !! b ofs Cur) as d.
     destruct d; try solve [apply po_None].
     symmetry in Heqd.
     apply (Mem.perm_alloc_4 _ _ _ _ _ ALLOC b ofs Cur p).
     * unfold Mem.perm; rewrite Heqd. destruct p; simpl; constructor.
     * intros N; subst; elim n; trivial.
  - (*Free*)
     destruct H as [m'' [FR EV]]. specialize (IHT _ _ EV); clear EV.
     generalize dependent m.
     induction l; simpl; intros.
     * inv FR. assumption.
     * destruct a as [[bb lo] hi].
       remember (Mem.free m bb lo hi) as p.
       destruct p; inv FR; symmetry in Heqp. specialize (IHl _ H0).
       remember (eq_block bb b && zle lo ofs && zlt ofs hi) as d.
       destruct d.
       { clear - Heqp Heqd. apply Mem.free_range_perm in Heqp.
         destruct (eq_block bb b); simpl in Heqd; inv Heqd.
         exploit (Heqp ofs); clear Heqp; trivial.
         destruct (zle lo ofs); try discriminate.
         destruct (zlt ofs hi); try discriminate. lia. }
       { eapply po_trans; try eassumption. clear - Heqp.
         remember ((Mem.mem_access m0) !! b ofs Cur) as perm2.
         destruct perm2; try solve [apply po_None].
         exploit (Mem.perm_free_3 _ _ _ _ _ Heqp); unfold Mem.perm.
            rewrite <- Heqperm2. apply perm_refl.
         simpl; trivial. }
Qed.

Lemma ev_elim_app: forall T1 m1 m2 (EV1:ev_elim m1 T1 m2) T2 m3  (EV2: ev_elim m2 T2 m3), ev_elim m1 (T1++T2) m3.
Proof.
  induction T1; simpl; intros; subst; trivial.
  destruct a.
+ destruct EV1 as [mm [SB EV]]. specialize (IHT1 _ _ EV _ _ EV2).
  exists mm; split; trivial.
+ destruct EV1 as [LB EV]. specialize (IHT1 _ _ EV _ _ EV2).
  split; trivial.
+ destruct EV1 as [mm [AL EV]]. specialize (IHT1 _ _ EV _ _ EV2).
  exists mm; split; trivial.
+ destruct EV1 as [mm [FL EV]]. specialize (IHT1 _ _ EV _ _ EV2).
  exists mm; split; trivial.
Qed.

Lemma ev_elim_split: forall T1 T2 m1 m3 (EV1:ev_elim m1 (T1++T2) m3),
      exists m2, ev_elim m1 T1 m2 /\ ev_elim m2 T2 m3.
Proof.
  induction T1; simpl; intros.
+ exists m1; split; trivial.
+ destruct a.
  - destruct EV1 as [mm [SB EV]]. destruct (IHT1 _ _ _ EV) as [m2 [EV1 EV2]].
    exists m2; split; trivial. exists mm; split; trivial.
  - destruct EV1 as [LB EV]. destruct (IHT1 _ _ _ EV) as [m2 [EV1 EV2]].
    exists m2; split; trivial. split; trivial.
  - destruct EV1 as [mm [AL EV]]. destruct (IHT1 _ _ _ EV) as [m2 [EV1 EV2]].
    exists m2; split; trivial. exists mm; split; trivial.
  - destruct EV1 as [mm [SB EV]]. destruct (IHT1 _ _ _ EV) as [m2 [EV1 EV2]].
    exists m2; split; trivial. exists mm; split; trivial.
Qed.

(** Similar to effect semantics, event semantics augment memory semantics with suitable effects, in the form
    of a set of memory access traces associated with each internal
    step of the semantics. *)

Record EvSem {C} :=
  { (** [sem] is a memory semantics. *)
    msem :> @MemSem C

    (** The step relation of the new semantics. *)
  ; ev_step: C -> mem -> list mem_event -> C -> mem -> Prop

    (** The next four fields axiomatize [drfstep] and its relation to the
        underlying step relation of [msem]. *)
  ; ev_step_ax1: forall c m T c' m',
       ev_step c m T c' m' ->
            corestep msem c m c' m'
  ; ev_step_ax2: forall c m c' m',
       corestep msem c m c' m' ->
       exists T, ev_step c m T c' m'
(*  ; ev_step_fun: forall c m T' c' m' T'' c'' m'',
       ev_step c m T' c' m' -> ev_step c m T'' c'' m'' -> T'=T'' *)
(*  ; ev_step_elim: forall g c m T c' m',
       ev_step g c m T c' m' -> ev_elim m T m'*)
  ; ev_step_elim: forall c m T c' m' (STEP: ev_step c m T c' m'),
       ev_elim m T m' (*/\
       (forall mm mm', ev_elim mm T mm' -> exists cc', ev_step c mm T cc' mm')*)
  }.

Definition ev_step_fun {C} (sem: @EvSem C) : Prop :=
  forall c m T' c' m' T'' c'' m'',
       ev_step sem c m T' c' m' -> ev_step sem c m T'' c'' m'' -> T'=T''.

Lemma Ev_sem_cur_perm {C} (R: @EvSem C) c m T c' m' b ofs (D: ev_step R c m T c' m'):
      Mem.perm_order'' ((Mem.mem_access m) !! b ofs Cur) (cur_perm (b,ofs) T).
Proof. eapply ev_perm. eapply ev_step_elim; eassumption. Qed.
(*
Arguments EvSem G C.
*)

Require Import List.
Import ListNotations.

Definition in_free_list (b : block) ofs xs :=
  exists x, List.In x xs /\
       let '(b', lo, hi) := x in
       b = b' /\
       (lo <= ofs < hi)%Z.


Fixpoint in_free_list_trace (b : block) ofs es :=
  match es with
  | Free l :: es =>
    in_free_list b ofs l \/ in_free_list_trace b ofs es
  | _ :: es =>
    in_free_list_trace b ofs es
  | nil =>
    False
  end.

(*not needed later - not sure it's useful*)
Lemma EFLT_char es: forall b ofs, in_free_list_trace b ofs es <->
                             exists l lo hi, In (Free l) es /\ In ((b, lo), hi) l /\ lo <= ofs < hi.
Proof. induction es; simpl.
       + split; intros; try contradiction. destruct H as [? [? [? [? ?]]]]. contradiction.
       + intros.
       - destruct a.
         * destruct (IHes b ofs).
           split; intros.
           ++ destruct (H H1) as [? [? [? [? ?]]]]. eexists; eexists; eexists. split. right. apply H2. apply H3.
           ++ destruct H1 as [? [? [? [? ?]]]].
              destruct H1. discriminate. apply H0.  eexists; eexists; eexists. split. eassumption. apply H2.
         * destruct (IHes b ofs).
           split; intros.
           ++ destruct (H H1) as [? [? [? [? ?]]]]. eexists; eexists; eexists. split. right. apply H2. apply H3.
           ++ destruct H1 as [? [? [? [? ?]]]].
              destruct H1. discriminate. apply H0.  eexists; eexists; eexists. split. eassumption. apply H2.
         * destruct (IHes b ofs).
           split; intros.
           ++ destruct (H H1) as [? [? [? [? ?]]]]. eexists; eexists; eexists. split. right. apply H2. apply H3.
           ++ destruct H1 as [? [? [? [? ?]]]].
              destruct H1. discriminate. apply H0.  eexists; eexists; eexists. split. eassumption. apply H2.
         * destruct (IHes b ofs).
           split; intros.
           ++ destruct H1. destruct H1 as [[[? ?] ?] [? [? ?]]]; subst b0. exists l, z, z0. split; eauto.
              destruct (H H1) as [? [? [? [? ?]]]]. eexists; eexists; eexists. split. right. apply H2. apply H3.
           ++ destruct H1 as [? [? [? [? [? ?]]]]].
              destruct H1. inv H1. left. red. exists ((b,x0),x1). split; trivial. split; trivial.
              right. apply H0. exists x, x0 , x1. split; trivial. split; trivial.
Qed.

Lemma freelist_mem_access_1 b ofs p: forall k l m (ACC:(Mem.mem_access m) !! b ofs k = Some p)
                                       m1 (FL: Mem.free_list m1 l = Some m), (Mem.mem_access m1) !! b ofs k = Some p.
Proof. induction l; simpl; intros. inv FL; trivial.
       destruct a as ((?, ?), ?).
       case_eq (Mem.free m1 b0 z z0); intros; rewrite H in FL; try discriminate.
       eapply free_access_inv; eauto.
Qed.

Lemma freelist_access_2' b ofs: forall l  (FL: in_free_list b ofs l)
                                 m m' (FR : Mem.free_list m l = Some m'),
    (forall k, (Mem.mem_access m') !! b ofs k = None) /\ Mem.valid_block m' b.
Proof. intros l FL. destruct FL as [[[? ?] ?] [? [? ?]]]; subst b0.
       induction l; simpl; intros.
       - inv H.
       - destruct H.
         * subst. case_eq (Mem.free m b z z0); intros; rewrite H in FR; try discriminate.
           clear IHl. split.
           ++ intros; case_eq ((Mem.mem_access m') !! b ofs k); trivial; intros.
              exploit freelist_mem_access_1. eassumption. eassumption. intros XX.
              exfalso. apply Mem.free_result in H. subst m0. simpl in XX.
              rewrite PMap.gss in XX. case_eq (zle z ofs && zlt ofs z0); intros; rewrite H in *; try discriminate.
              destruct (zle z ofs); try lia; simpl in *. destruct (zlt ofs z0); try lia. inv H.
           ++ eapply freelist_forward; eauto.
              exploit Mem.free_range_perm. eassumption. eassumption. intros.
              eapply Mem.valid_block_free_1; try eassumption. eapply Mem.perm_valid_block; eauto.
         * destruct a as ((?, ?), ?).
           case_eq (Mem.free m b0 z1 z2); intros; rewrite H0 in FR; try discriminate. eauto.
Qed.

Lemma freelist_access_2 b ofs: forall l  (FL: in_free_list b ofs l)
                                 m m' (FR : Mem.free_list m l = Some m'),
    (Mem.mem_access m') !! b ofs Cur = None /\ Mem.valid_block m' b.
Proof.
  intros; edestruct freelist_access_2'; eauto.
Qed.

Lemma freelist_access_3 b ofs: forall l m (ACC: (Mem.mem_access m) !! b ofs Cur = None)
                                 (VB: Mem.valid_block m b) m' (FL: Mem.free_list m l = Some m'),
    (Mem.mem_access m') !! b ofs Cur = None.
Proof. induction l; simpl; intros.
       + inv FL; trivial.
       + destruct a as [[? ?] ?].
         case_eq (Mem.free m b0 z z0); intros; rewrite H in FL; try discriminate.
         eapply (IHl m0); trivial.
       - destruct (eq_block b0 b); subst. apply Mem.free_result in H. subst. simpl. rewrite PMap.gss, ACC. destruct (zle z ofs && zlt ofs z0); trivial.
         apply Mem.free_result in H. subst. simpl. rewrite PMap.gso; eauto.
       - eapply Mem.valid_block_free_1; eauto.
Qed.

Lemma ev_elim_accessNone b ofs: forall ev m' m'' (EV:ev_elim m'' ev m')
                                  (ACC: (Mem.mem_access m'') !! b ofs Cur = None)
                                  (VB: Mem.valid_block m'' b), (Mem.mem_access m') !! b ofs Cur = None.
Proof.  induction ev; simpl; intros. subst; trivial.
        destruct a.
        - destruct EV as [? [? EV]]. exploit Mem.storebytes_valid_block_1; eauto. intros.
          apply Mem.storebytes_access in H. rewrite <- H in *; clear H.
          apply (IHev _ _ EV ACC H0).
        - destruct EV as [? EV]. eauto.
        - destruct EV as [? [? EV]].
          apply (IHev _ _ EV); clear IHev EV.
          + Transparent Mem.alloc.
            unfold Mem.alloc in H. Opaque Mem.alloc.  inv H. simpl. rewrite PMap.gso; trivial. unfold Mem.valid_block in VB. apply Plt_ne; auto.
          + eapply Mem.valid_block_alloc; eauto.
        - destruct EV as [? [? EV]]. apply (IHev _ _ EV); clear IHev.
          2: eapply freelist_forward; eauto.
          clear EV ev m'.
          eapply freelist_access_3; eassumption.
Qed.

Lemma ev_elim_valid_block: forall ev m m' (EV: ev_elim m ev m') b
                             (VB : Mem.valid_block m b), Mem.valid_block m' b.
Proof. induction ev; simpl; intros; subst; trivial.
       destruct a.
       + destruct EV as [? [? EV]]. exploit Mem.storebytes_valid_block_1. apply H. eassumption. eauto.
       + destruct EV as [? EV]. eauto.
       + destruct EV as [? [? EV]]. exploit Mem.valid_block_alloc. apply H. eassumption. eauto.
       + destruct EV as [? [? EV]]. exploit freelist_forward; eauto. intros [? _]. eauto.
Qed.


(** If (b, ofs) is in the list of freed addresses then the
         permission was Freeable and became None or it was not allocated*)
Lemma ev_elim_free_1 b ofs:
  forall ev m m',
    ev_elim m ev m' ->
    in_free_list_trace b ofs ev ->
    (Mem.perm m b ofs Cur Freeable \/
     ~ Mem.valid_block m b) /\
    (Mem.mem_access m') !! b ofs Cur = None /\
    Mem.valid_block m' b /\
    exists e, List.In e ev /\
         match e with
         | Free _ => True
         | _ => False
         end.
Proof.
  induction ev; simpl; intros; try contradiction.
  destruct a.
  + destruct H as [m'' [ST EV]].
    specialize (Mem.storebytes_access _ _ _ _ _ ST); intros ACCESS.
    destruct (eq_block b0 b); subst.
  - destruct (IHev _ _ EV H0) as [IHa [IHb [IHc [e [E HE]]]]]; clear IHev.
    split. { destruct IHa. left. eapply Mem.perm_storebytes_2; eauto.
             right. intros N. apply H. eapply Mem.storebytes_valid_block_1; eauto. }
           split; trivial.
    split; trivial.
    exists e. split; trivial. right; trivial.
  - destruct (IHev _ _ EV H0) as [IHa [IHb [IHc [e [E HE]]]]]; clear IHev.
    split. { destruct IHa. left. eapply Mem.perm_storebytes_2; eassumption.
             right; intros N. apply H. eapply Mem.storebytes_valid_block_1; eauto. }
           split. trivial.
    split; trivial. exists e. split; trivial. right; trivial.
    + destruct H.
      destruct (IHev _ _ H1 H0) as [IHa [IHb [IHc [e [E HE]]]]]; clear IHev.
      split; trivial.
      split; trivial.
      split; trivial.
      exists e. split; trivial. right; trivial.
    + destruct H as [m'' [ALLOC EV]].
      destruct (IHev _ _ EV H0) as [IHa [IHb [IHc [e [E HE]]]]]; clear IHev.
      destruct (eq_block b0 b); subst.
  - split. right. eapply Mem.fresh_block_alloc. eauto.
    split; trivial.
    split; trivial.
    exists e.
    split; trivial. right; trivial.
  - split. { destruct IHa. left. eapply Mem.perm_alloc_4; eauto.
             right; intros N. apply H. eapply Mem.valid_block_alloc; eauto. }
           split; trivial.
    split; trivial.
    exists e. split; trivial. right; trivial.
    + destruct H as [m'' [FR EV]].
      destruct H0.
  - clear IHev.
    split. { destruct (valid_block_dec m b). 2: right; trivial. left.
             clear EV m'. generalize dependent m''. generalize dependent m.
             destruct H as [[[bb lo] hi] [X [? Y]]]; subst bb.
             induction l; simpl in *; intros. contradiction.
             destruct X; subst.
             + case_eq (Mem.free m b lo hi); intros; rewrite H in FR; try discriminate.
               eapply Mem.free_range_perm; eassumption.
             + destruct a. destruct p.
               case_eq (Mem.free m b0 z0 z); intros; rewrite H0 in FR; try discriminate.
               eapply Mem.perm_free_3. eassumption.
               eapply IHl; try eassumption.
               eapply Mem.valid_block_free_1; eauto. }
           split. { exploit freelist_access_2. eassumption. eassumption.
                    intros [ACC VB].  clear FR m l H.
                    eapply ev_elim_accessNone; eauto. }
                  split. { exploit freelist_access_2; eauto. intros [ACC VB].
                           eapply ev_elim_valid_block; eauto. }
                         exists (Free l). intuition.
  - destruct (IHev _ _ EV H) as [IHa [IHb [IHc [e [E HE]]]]]; clear IHev.
    split. { destruct IHa. left. eapply perm_freelist; eauto.
             right; intros N. apply H0. eapply freelist_forward; eauto. }
           split; trivial.
    split; trivial.
    exists e. split; trivial. right; trivial.
Qed.

Lemma perm_order_pp_refl p: Mem.perm_order'' p p.
Proof. unfold Mem.perm_order''. destruct p; trivial. apply perm_refl. Qed.

Lemma in_free_list_dec b ofs xs: {in_free_list b ofs xs} + {~in_free_list b ofs xs}.
Proof. unfold in_free_list.
       induction xs; simpl. right. intros N. destruct N as [[[? ?] ?] [? _]]. trivial.
       destruct IHxs.
       + left. destruct e as [? [? ?]]. exists x. split; eauto.
       + destruct a as [[? ?] ?].
         destruct (eq_block b0 b); subst.
       - destruct (zle z ofs).
         * destruct (zlt ofs z0). -- left. exists (b, z, z0). split; eauto.
           -- right. intros [[[? ?] ?] [? [? ?]]]. subst b0.
              destruct H. inv H. lia. apply n; clear n.
              exists (b, z1, z2). split; eauto.
         * right. intros [[[? ?] ?] [? [? ?]]]. subst b0.
           destruct H. inv H. lia. apply n; clear n.
           exists (b, z1, z2). split; eauto.
       - right. intros [[[? ?] ?] [? [? ?]]]. subst b1.
         destruct H. inv H. congruence.
         apply n; clear n. exists (b, z1, z2). split; eauto.
Qed.

Lemma in_free_list_trace_dec b ofs: forall es, {in_free_list_trace b ofs es} + {~in_free_list_trace b ofs es}.
Proof.
  induction es; simpl. right; intros N; trivial.
  destruct IHes.
  + destruct a; try solve [left; eauto].
  + destruct a; try solve [right; eauto].
    destruct (in_free_list_dec b ofs l). left; left; trivial.
    right; intros N. destruct N; contradiction.
Qed.

Lemma freelist_access_1 b ofs: forall k l,
    ~ in_free_list b ofs l ->
    forall m m' : mem, Mem.free_list m l = Some m' -> (Mem.mem_access m') !! b ofs k = (Mem.mem_access m) !! b ofs k.
Proof.
  induction l; simpl; intros. inv H0. trivial.
  destruct a as [[? ?] ?].
  remember (Mem.free m b0 z z0) as q; destruct q; try discriminate. symmetry in Heqq.
  assert (~ in_free_list b ofs l). { intros N. elim H. destruct N as [? [? ?]]. exists x. split; eauto. right; trivial. }
                                   rewrite (IHl H1 _ _ H0). clear IHl H0.
  Transparent Mem.free. unfold Mem.free in Heqq. Opaque Mem.free.
  remember (Mem.range_perm_dec m b0 z z0 Cur Freeable).
  destruct s; inv Heqq; clear Heqs. simpl.
  rewrite PMap.gsspec. destruct (peq b b0); subst; trivial.
  destruct (zle z ofs); simpl; trivial.
  destruct (zlt ofs z0); simpl; trivial.
  elim H. unfold in_free_list. exists (b0, z, z0). split; eauto. left; trivial.
Qed.

(** If (b, ofs) is not in the list of freed locations then its permissions
cannot decrease*)
Lemma ev_elim_free_2 b ofs:
  forall ev m m' (EV: ev_elim m ev m')
    (T: ~ in_free_list_trace b ofs ev),
    Mem.perm_order'' ((Mem.mem_access m') !! b ofs Cur)
                     ((Mem.mem_access m) !! b ofs Cur).
Proof.
  induction ev; simpl; intros.
  + subst. apply perm_order_pp_refl.
  + destruct a.
  - destruct EV  as [m'' [ST EV]].
    apply Mem.storebytes_access in ST. rewrite <- ST. apply (IHev _ _ EV T).
  - destruct EV  as [LD EV].
    apply (IHev _ _ EV T).
  - destruct EV  as [m'' [ALLOC EV]].
    eapply po_trans. apply (IHev _ _ EV T). clear IHev.
    unfold Mem.perm_order''. remember ((Mem.mem_access m'') !! b ofs Cur) as q.
    symmetry in Heqq; destruct q.
    * exploit Mem.perm_alloc_inv. eassumption. unfold Mem.perm. rewrite Heqq. simpl. apply perm_refl.
      destruct (eq_block b b0); simpl; intros; subst.
      ++ rewrite Mem.nextblock_noaccess; trivial. intros N.
         eapply Mem.fresh_block_alloc; eassumption.
      ++ Transparent Mem.alloc. unfold Mem.alloc in ALLOC. inv ALLOC. simpl in *. clear EV.
         Opaque Mem.alloc.
         remember ((Mem.mem_access m) !! b ofs Cur) as r. destruct r; trivial. symmetry in Heqr.
         rewrite PMap.gso in Heqq; trivial. rewrite Heqq in Heqr. inv Heqr. apply perm_refl.
    * erewrite alloc_access_inv_None; eauto.
  - destruct EV  as [m'' [FR EV]]. specialize (IHev _ _ EV).
    destruct (in_free_list_dec b ofs l).
    * elim T. left; trivial.
    * destruct (in_free_list_trace_dec b ofs ev).
      elim T. right; trivial.
      eapply po_trans. apply IHev; trivial.
      erewrite freelist_access_1; eauto. apply perm_order_pp_refl.
Qed.

Lemma free_list_cases:
  forall l m m' b ofs
    (Hfree: Mem.free_list m l = Some m'),
    ((Mem.mem_access m) !! b ofs Cur = Some Freeable /\
     (Mem.mem_access m') !! b ofs Cur = None) \/
    ((Mem.mem_access m) !! b ofs Cur =
     (Mem.mem_access m') !! b ofs Cur).
Proof.
  induction l; simpl; intros. inv Hfree. right; trivial.
  destruct a as [[bb lo] hi].
  remember (Mem.free m bb lo hi) as q; symmetry in Heqq. destruct q; inv Hfree.
  specialize (IHl _ _ b ofs H0); clear H0.
  Transparent Mem.free. unfold Mem.free in Heqq. Opaque Mem.free.
  remember (Mem.range_perm_dec m bb lo hi Cur Freeable). destruct s; try discriminate. inv Heqq. clear Heqs.
  simpl in *.
  rewrite PMap.gsspec in *.
  destruct (peq b bb); subst; trivial.
  destruct IHl.
  + destruct H.
    rewrite H0; clear H0.
    destruct (zle lo ofs); try discriminate; simpl in *.
  - destruct (zlt ofs hi); try discriminate; simpl in *. rewrite H. left; split; trivial.
  - rewrite H. left; split; trivial.
    + destruct (zle lo ofs); simpl in *; try solve [right; trivial].
      destruct (zlt ofs hi); simpl in *; try solve [right; trivial].
      rewrite <- H; clear H.
      assert (A: lo <= ofs < hi) by lia.
      specialize (r _ A). unfold Mem.perm, Mem.perm_order' in r.
      remember ((Mem.mem_access m) !! bb ofs Cur) as q. destruct q; try contradiction.
      left; split; trivial. destruct p; simpl in *; trivial; inv r.
Qed.

Lemma ev_elim_mem_fw:
  forall ev m m',
    ev_elim m ev m' -> 
    ((Mem.nextblock m) <= (Mem.nextblock m'))%positive.
Proof.
  induction ev.
  - simpl; intros; subst; reflexivity.
  - intros. simpl in H. destruct a.
    + destruct H as (?&?&?).
      etransitivity.
      * eapply Mem.nextblock_storebytes in H.
        rewrite <- H; reflexivity.
      * eapply IHev; eauto.
    + destruct H as (?&?).
      eapply IHev; eauto.            
    + destruct H as (?&?&?).
      etransitivity.
      * eapply Mem.nextblock_alloc in H.
        instantiate(1:=  Mem.nextblock x); rewrite H.
        lia.
      * eapply IHev; eauto.
    + destruct H as (?&?&?).
      etransitivity.
      * eapply nextblock_freelist in H.
        rewrite <- H; reflexivity.
      * eapply IHev; eauto.        
Qed.
Lemma event_semantics_mem_fw:
  forall C semSem c m ev c' m',
    @ev_step C semSem c m ev c' m' ->
    ((Mem.nextblock m) <= (Mem.nextblock m'))%positive.
Proof.
  intros.
  eapply ev_step_elim in H.
  eapply ev_elim_mem_fw; eassumption.
Qed.
