Module Emem

Require Import Coqlib.
Require Import Ast Events Mem Pointers Integers Values.

Record mod4 (i: int) : Prop :=
  { I: Z
  ; _: Int.unsigned i = 4 * I
  ; _: 0 <= I < Int.modulus / 4
  }.

Definition wf_ptr (p:pointer) : Prop :=
  match p with
    | Ptr b i => mod4 i
  end.

Lemma wf_ptr_aligned (p: pointer) : wf_ptr p -> pointer_chunk_aligned p Mint32.
Proof.
destruct p as (P & pi). intros [I J K]. simpl. exists I. omega. Qed.

Definition wf_val (v:val) : Prop :=
  match v with
    | Vint _ => True
    | Vptr p => wf_ptr p
    | Vfloat _
    | Vundef => False
  end.

Definition wf_rmw (rmw: rmw_instr) : Prop :=
  match rmw with
    | rmw_ADD v | rmw_SET v => False
    | rmw_CAS v v' => wf_val v /\ wf_val v'
  end.

Lemma wf_rmw_instr_sem (v: val) (rmw: rmw_instr) :
  wf_val v -> wf_rmw rmw ->
  wf_val (rmw_instr_semantics rmw v).
Proof.
  destruct rmw as [| i j |]; simpl; try now intuition.
  intros V (I & J).
  destruct (Val.eq_dec i Vundef). subst. inv I. simpl.
  destruct (Val.eq_dec v Vundef). subst. inv V. simpl.
  case (Val.eq_dec i v); trivial.
Qed.

Lemma p_dec p1 p2 : wf_ptr p1 -> wf_ptr p2 ->
  { p1 = p2 } +
  { p1 <> p2 /\ ranges_disjoint (p1, Int.repr 4) (p2, Int.repr 4) }.
Proof.
    intros Hi Hj.
    destruct p1 as [b1 i1]; destruct p2 as [b2 i2]; simpl in *.
    destruct (Z_eq_dec b1 b2).
    destruct (Int.eq_dec i1 i2).
      subst. left. reflexivity.
    right. intuition.
    inv H; intuition.
    unfold ranges_disjoint.
    right.
    destruct Hi as [I HI K]. simpl in K.
    destruct Hj as [J HJ L]. simpl in L.
    simpl.
    repeat rewrite Zmod_small; intuition.
    assert(Int.unsigned i1<>Int.unsigned i2).
      intro; elim n; apply Int.unsigned_eq; auto.
    omega.
    reflexivity.
    right; split.
    congruence.
    left; auto.
  Qed.

Definition wf_range (r: arange) : Prop :=
  wf_ptr (fst r) /\ mod4 (snd r).

Remark wf_range_of_ptr {p: pointer} : wf_ptr p -> wf_range (range_of_chunk p Mint32).
Proof.
intros H. split. exact H. simpl. exists 1. reflexivity. intuition. reflexivity.
Qed.

Lemma wf_range_ptr_inside {r: arange} {p: pointer} :
  wf_range r -> wf_ptr p ->
  { range_inside (range_of_chunk p Mint32) r } + { ranges_disjoint r (range_of_chunk p Mint32) }.
Proof.
  destruct r as ((Blk & i) & sz). destruct p as (p & pi).
  intros (B & Sz). simpl in *.
  intros P.
  unfold range_of_chunk, size_chunk.
  case (ranges_disjoint_dec (Ptr Blk i, sz) (Ptr p pi, Int.repr 4)).
  intuition.
  intros K.
  left.
  destruct (ranges_overlapD K) as (<- & X & Y).
  split. reflexivity.
  destruct B as [I Hi Hi']. destruct Sz as [S Hs Hs']. rewrite Hi in *. rewrite Hs in *.
  destruct P as [P Hp Hp']. rewrite Hp in *.
  change (Int.unsigned (Int.repr 4)) with 4 in *.
  right.
  omega.
Qed.

Lemma load_store_new : forall m p v m',
  wf_ptr p -> wf_val v ->
  store_ptr Mint32 m p v = Some m' ->
  load_ptr Mint32 m' p = Some v.
Proof.
  intros.
  exploit @Mem.load_store_similar; eauto.
  destruct v; simpl in *; intuition.
Qed.

Lemma load_store_old : forall m p v m' p',
  wf_ptr p -> wf_val v -> wf_ptr p' ->
  store_ptr Mint32 m p v = Some m' ->
  p <> p' ->
  load_ptr Mint32 m' p' = load_ptr Mint32 m p'.
Proof.
  intros.
  exploit @Mem.load_store_other; eauto.
  destruct (p_dec _ _ H H1); intuition.
Qed.

Lemma store_store_ex :
  forall m p1 v1 m1 p2 v2 m2,
    wf_ptr p1 -> wf_val v1 ->
    wf_ptr p2 -> wf_val v2 ->
    store_ptr Mint32 m p1 v1 = Some m1 ->
    store_ptr Mint32 m1 p2 v2 = Some m2 ->
      store_ptr Mint32 m p2 v2 <> None.
Proof.
  intros m p1 v1 m1 p2 v2 m2 Hp1 Hv1 Hp2 Hv2 Hm1 Hm2.
  intros H.
  elim (store_chunk_allocated_noneD H).
      destruct (store_chunk_allocated_someD Hm2) as ((r & s & A & B) & ?).
      split. 2: assumption. exists r. exists s. split. assumption.
      erewrite (store_preserves_allocated_ranges Hm1). assumption.
Qed.

Record mem_ext (m m' : mem) : Prop :=
{ eq_load: forall p, wf_ptr p -> load_ptr Mint32 m p = load_ptr Mint32 m' p
; eq_alloc: forall r k, range_allocated r k m <-> range_allocated r k m'
; eq_restr: forall b, mrestr m b = mrestr m' b
}.
Implicit Arguments eq_load [m m' p].
Implicit Arguments eq_alloc [m m'].
Implicit Arguments eq_restr [m m'].

Notation "m == m'" := (mem_ext m m') (at level 70).

Lemma mem_eq_refl : forall m, m == m.
Proof.
constructor; intros; reflexivity. Qed.
Lemma mem_eq_sym : forall m m', m == m' -> m' == m.
Proof.
intros m m' EQ. constructor. intros p Hp; symmetry; apply (EQ.(eq_load) Hp).
  intros r k; symmetry; apply (EQ.(eq_alloc) r k).
  intros b; symmetry; apply (EQ.(eq_restr) b).
Qed.
Lemma mem_eq_trans: forall m m' m'', m == m' -> m' == m'' -> m == m''.
Proof.
  intros m m' m'' E F.
  constructor. intros p Hp. transitivity (load_ptr Mint32 m' p); intuition.
  intros r k. transitivity (range_allocated r k m'). apply (E.(eq_alloc) r k). apply F.(eq_alloc).
  intros b. transitivity (mrestr m' b). apply E.(eq_restr). apply F.(eq_restr).
Qed.

Lemma store_same :
  forall m m' p v m'',
    wf_ptr p ->
    wf_val v ->
    load_ptr Mint32 m p = Some v ->
    store_ptr Mint32 m' p v = Some m'' ->
    m == m' ->
    m' == m''.
Proof.
  intros m m' p v m'' Hp Hv HL HS EQ.
  constructor. intros p' Hp'.
  destruct (p_dec p p'); trivial.
  subst. rewrite (EQ.(eq_load) Hp') in HL. rewrite HL. symmetry. eapply load_store_new; eassumption.
  eapply load_store_other; intuition eauto.
  intros r k. eapply store_preserves_allocated_ranges. eassumption.
  intros b. erewrite <- restr_of_store; eauto.
Qed.

Lemma store_ext :
  forall m p v m1 m',
    m == m' ->
    wf_ptr p -> wf_val v ->
    store_ptr Mint32 m p v = Some m1 ->
    exists m1',
      store_ptr Mint32 m' p v = Some m1' /\ m1' == m1.
Proof.
  intros m p v m1 m' EQ Hp Hv Hm1.
  case_eq (store_ptr Mint32 m' p v).
    intros m1' Hm1'.
    exists m1'. split. reflexivity.
    constructor.
      intros q Hq.
      case (p_dec p q Hp Hq).
        intros <-.
        repeat (erewrite load_store_new; eauto).
      intros (NE & _).
      rewrite (load_store_old m p v m1 q); auto.
      rewrite (load_store_old m' p v m1' q); auto.
      symmetry.
      apply EQ.(eq_load); auto.
    intros r k.
    transitivity (range_allocated r k m'). symmetry.
      eapply store_preserves_allocated_ranges. eassumption.
    transitivity (range_allocated r k m). symmetry.
      apply EQ.(eq_alloc); auto.
      eapply store_preserves_allocated_ranges. eassumption.
    intros b. erewrite (restr_of_store Hm1); eauto. rewrite (restr_of_store Hm1').
    symmetry.
    apply EQ.(eq_restr).
  intros K. apply False_ind.
  elim (store_chunk_allocated_noneD K).
  destruct (store_chunk_allocated_someD Hm1) as ((x & y & A & B) & C).
  split. exists x; exists y. split. exact A.
    apply EQ.(eq_alloc). exact B.
  exact C.
Qed.

Lemma alloc_ext :
  forall m r k m1 m',
    m == m' ->
    wf_range r ->
    alloc_ptr r k m = Some m1 ->
    exists m1',
      alloc_ptr r k m' = Some m1' /\ m1' == m1.
Proof.
  intros m r k m1 m' EQ Hr Hm1.
  case_eq (alloc_ptr r k m').
    intros m1' Hm1'.
    exists m1'. split. reflexivity.
    constructor.
      intros p Hp.
      pose proof (wf_ptr_aligned _ Hp).
      destruct (wf_range_ptr_inside Hr Hp).
        rewrite (load_alloc_inside Hm1); auto.
        rewrite (load_alloc_inside Hm1'); auto.
      apply ranges_disjoint_comm in r0.
      rewrite (load_alloc_other Hm1); auto.
      rewrite (load_alloc_other Hm1'); auto.
      symmetry; apply eq_load with (1:=EQ).
      assumption.
    intros r' k'.
    rewrite (alloc_preserves_allocated_iff Hm1).
    rewrite (alloc_preserves_allocated_iff Hm1').
    pose proof (EQ.(eq_alloc) r' k').
    intuition.
    intros b.
    rewrite (restr_of_alloc Hm1).
    rewrite (restr_of_alloc Hm1').
    symmetry; apply EQ.(eq_restr).
  intros K.
    destruct (alloc_someD Hm1) as (A & B & C & D).
    destruct (alloc_noneD K) as [| [H|(r' & k' & H & H')]]. contradiction.
    elim H. destruct r as ((a & b) & c). simpl. rewrite <- EQ.(eq_restr). exact C.
  elim (D r' k' H).
  apply EQ.(eq_alloc).
  exact H'.
Qed.

Lemma free_ext :
  forall m r k n m1 m',
    m == m' ->
    wf_range (r,n) ->
    range_allocated (r,n) k m ->
    free_ptr r k m = Some m1 ->
    exists m1',
      free_ptr r k m' = Some m1' /\ m1' == m1.
Proof.
  intros m r k n m1 m' EQ Hr RA Hm1.
  case_eq (free_ptr r k m').
    intros m1' Hm1'.
    exists m1'. split. reflexivity.
    constructor.
      intros p Hp.
      destruct (ranges_disjoint_dec (range_of_chunk p Mint32) (r, n)) as [Y|Y].
        rewrite (load_free_other Hm1 RA Y).
        erewrite (load_free_other Hm1'). 2: apply EQ.(eq_alloc); apply RA. 2: exact Y.
        symmetry. apply EQ.(eq_load). assumption.
      rewrite (load_free_overlap Hm1 RA Y).
      eapply load_free_overlap; try eassumption.
      apply EQ.(eq_alloc). assumption.
    intros r' k'.
    split.
    intros H; assert (H' := free_preserves_allocated_back Hm1' _ _ H);
      apply EQ.(eq_alloc) in H'; destruct (free_preserves_allocated Hm1 _ _ H') as [Y|(Y&->)].
      assumption. destruct r'. unfold fst in *. subst.
      elim (free_not_allocated Hm1' _ _ H).
    intros H; assert (H' := free_preserves_allocated_back Hm1 _ _ H);
      rewrite EQ.(eq_alloc) in H'; destruct (free_preserves_allocated Hm1' _ _ H') as [Y|(Y&->)].
      assumption. destruct r'. unfold fst in *. subst.
      elim (free_not_allocated Hm1 _ _ H).
    intros b.
    rewrite (restr_of_free Hm1).
    rewrite (restr_of_free Hm1').
    symmetry; apply EQ.(eq_restr).
  intros K.
    destruct (free_someD Hm1) as (n' & Hn').
    rewrite EQ.(eq_alloc) in Hn'.
    elim (free_noneD K n' Hn').
Qed.

Lemma store_comm :
  forall m p1 v1 m1 p2 v2 m2,
    p1 <> p2 ->
    wf_ptr p1 -> wf_val v1 ->
    wf_ptr p2 -> wf_val v2 ->
    store_ptr Mint32 m p1 v1 = Some m1 ->
    store_ptr Mint32 m1 p2 v2 = Some m2 ->
    forall m0, m0 == m ->
    forall m3, store_ptr Mint32 m0 p2 v2 = Some m3 ->
               exists m2', store_ptr Mint32 m3 p1 v1 = Some m2' /\ m2' == m2.
Proof.

  intros m p1 v1 m1 p2 v2 m2 NEQ Hp1 Hv1 Hp2 Hv2 Hm1 Hm2 m0 EQ m3 Hm3.
  case_eq (store_ptr Mint32 m3 p1 v1).
    intros m' Hm'.
    exists m'; split. reflexivity.
    constructor.
    intros p Hp.
    case (Ptr.eq_dec p2 p). intros ->.
      rewrite load_store_old with (4:=Hm'); auto.
      rewrite load_store_new with (3:=Hm3); auto.
      rewrite load_store_new with (3:=Hm2); auto.
    intros.
    rewrite load_store_old with (4:=Hm2); auto.
    case (p_dec _ _ Hp1 Hp).
      intros ->.
      rewrite load_store_new with (3:=Hm1); auto.
      rewrite load_store_new with (3:=Hm'); auto.
    intros (? & _).
    rewrite load_store_old with (4:=Hm1); auto.
    rewrite load_store_old with (4:=Hm'); auto.
    rewrite load_store_old with (4:=Hm3); auto.
    eapply eq_load; eauto.
    intros r k.
    transitivity (range_allocated r k m3).
      symmetry.
      eapply (store_preserves_allocated_ranges Hm').
    transitivity (range_allocated r k m0).
      symmetry.
      eapply (store_preserves_allocated_ranges Hm3).
    transitivity (range_allocated r k m1).
    transitivity (range_allocated r k m).
      eapply eq_alloc; eauto.
      eapply (store_preserves_allocated_ranges Hm1).
      eapply (store_preserves_allocated_ranges Hm2).
    intros b.
    rewrite (restr_of_store Hm2).
    rewrite (restr_of_store Hm1).
    rewrite (restr_of_store Hm').
    rewrite (restr_of_store Hm3).
    apply EQ.(eq_restr).
  intros H.
  pose proof (store_chunk_allocated_someD Hm1) as ((u & u' & U & U') & V).
  elim (store_chunk_allocated_noneD H). split. 2: assumption.
  exists u. exists u'. split. trivial.
  apply (store_preserves_allocated_ranges Hm3).
  rewrite eq_alloc with (1:=EQ).
  assumption.
Qed.

  Lemma store_alloc :
    forall m p v m' r k m'',
      wf_ptr p -> wf_val v -> wf_range r ->
      store_ptr Mint32 m p v = Some m' ->
      alloc_ptr r k m' = Some m'' ->
      forall x, x == m ->
      (exists n, alloc_ptr r k x = Some n)
        /\
      (forall n, alloc_ptr r k x = Some n ->
         exists n', store_ptr Mint32 n p v = Some n' /\ n' == m'').
Proof.
    intros m p v m' r k m'' Hp Hv Hr HS HA x EQ.
    destruct (alloc_someD HA) as (Hr'' & V & R & HA').
    pose proof (store_preserves_allocated_ranges HS) as Hr'.
    case_eq (alloc_ptr r k x).
    Focus 2.
  intros K.
    destruct (alloc_noneD K) as [| [H|(r' & k' & H & H')]]. contradiction.
    elim H. destruct r as ((a & b) & c). simpl. rewrite EQ.(eq_restr).
    rewrite <- (restr_of_store HS). exact R.
    elim (HA' r' k' H). apply Hr'.
    apply EQ.(eq_alloc).
    exact H'.

    intros x' Hx'.
    split. exists x'. reflexivity.
    intros ? H; inv H.
    case_eq (store_ptr Mint32 n p v).
    Focus 2.
    intros K. apply False_ind.
    pose proof (store_chunk_allocated_someD HS) as ((u & u' & U & U') & K').
    elim (store_chunk_allocated_noneD K). split. 2: assumption.
    exists u. exists u'. split. assumption.
    apply (alloc_preserves_allocated Hx'). rewrite EQ.(eq_alloc).
    assumption.
  intros n' Hn'.
  exists n'. split. reflexivity.
  constructor.
  3: intros b; rewrite (restr_of_store Hn'), (restr_of_alloc Hx'), (restr_of_alloc HA), (restr_of_store HS);
    apply EQ.(eq_restr).
  intros q Hq.
  destruct (p_dec q p Hq Hp) as [->|(Hpq & _)].
    rewrite (load_store_new _ _ _ _ Hp Hv Hn').
    rewrite (load_alloc_other HA).
    rewrite (load_store_new _ _ _ _ Hp Hv HS).
    reflexivity.
    destruct (wf_range_ptr_inside Hr Hp) as [H|H]. 2: apply ranges_disjoint_comm; exact H.
    destruct (store_chunk_allocated_someD HS) as ((u & u' & A & B) & C).
    elim (HA' u u').
      2: apply (store_preserves_allocated_ranges HS); assumption.
      eapply overlap_inside_overlap. 2: eapply H.
      apply ranges_overlap_comm.
      eapply overlap_inside_overlap. 2: eapply A.
      apply ranges_overlap_refl. vauto.
  rewrite (load_store_old _ _ _ _ _ Hp Hv Hq Hn'). 2: intuition.
  pose proof (wf_ptr_aligned _ Hq).
  destruct (wf_range_ptr_inside Hr Hq) as [K|K].
    rewrite (load_alloc_inside HA); auto.
    rewrite (load_alloc_inside Hx'); auto.
  apply ranges_disjoint_comm in K.
  rewrite (load_alloc_other HA); auto.
  rewrite (load_alloc_other Hx'); auto.
  rewrite (load_store_old _ _ _ _ _ Hp Hv Hq HS); intuition.
  intros ar ak.
  transitivity (range_allocated ar ak n).
  symmetry.
  exact (store_preserves_allocated_ranges Hn' ar ak).
  destruct (alloc_someD Hx') as (Hrx & _ & Rx & HAx).
  rewrite (alloc_preserves_allocated_iff Hx').
  rewrite (alloc_preserves_allocated_iff HA).
  specialize HAx with ar ak.
  specialize HA' with ar ak.
  specialize Hr' with ar ak.
  pose proof (EQ.(eq_alloc) ar ak).
  intuition (subst; intuition).
  Qed.

  Lemma store_free :
    forall m p v m' r rx k m'',
      wf_ptr p -> wf_val v -> wf_range (r, rx) ->
      store_ptr Mint32 m p v = Some m' ->
      range_allocated (r, rx) k m' ->
      ranges_disjoint (range_of_chunk p Mint32) (r, rx) ->
      free_ptr r k m' = Some m'' ->
      forall x, x == m ->
      (exists n, free_ptr r k x = Some n)
        /\
      (forall n, free_ptr r k x = Some n ->
         exists n', store_ptr Mint32 n p v = Some n' /\ n' == m'').
Proof.
    intros m p v m' r rx k m'' Hp Hv Hr Hs Ha Hd Hf x EQ.
    destruct (free_someD Hf) as (q & Hq).
    pose proof (store_preserves_allocated_ranges Hs) as Hr'.
    case_eq (free_ptr r k x).
    2: intros H; eelim (free_noneD H); erewrite eq_alloc with (1:=EQ); apply Hr'; eassumption.
    intros n' Hn.
    split. exists n'; trivial.
    intros n K; inv K.
    pose proof (store_chunk_allocated_someD Hs) as ((u & u' & U & U') & V).
    case_eq (store_ptr Mint32 n p v).
    Focus 2. intros H; elim (store_chunk_allocated_noneD H). split. 2: assumption.
      exists u. exists u'. split. assumption.
      rewrite <- eq_alloc with (1:=EQ) in U'.
      destruct (free_preserves_allocated Hn u u' U') as [A|(A&B)]. exact A.
      subst. destruct u as ((blk & ofs) & usz). unfold fst in *.
      destruct (alloc_ranges_same Ha Hq). subst.
      apply Hr' in Hq.
      rewrite eq_alloc with (1:=EQ) in U'.
      destruct (alloc_ranges_same U' Hq). subst. clear U'.
      unfold range_of_chunk in *.
      assert (Int.unsigned (Int.repr 4) = 4) as H4.
        apply Int.unsigned_repr. intuition. discriminate.
      destruct p as (pb & pi). simpl in Hd, U. inv U. inv H2. rewrite H4 in *.
      inv Hd. congruence.
      rewrite H4 in *.
      destruct Hr as ((Ofs & B) & (Q & F)).
      unfold snd in *. rewrite F in *. rewrite B in *.
      simpl in V. destruct V as (V & HV). rewrite HV in *.
      apply False_ind. intuition.

    intros n' Hn'.
    exists n'. split. reflexivity.
    constructor.
    intros l Hl.
    destruct (p_dec l p) as [<-|(X&_)]; auto.
      rewrite load_store_new with (3:=Hn'); auto.
      rewrite (load_free_other Hf Ha); auto.
      rewrite load_store_new with (3:=Hs); auto.
    rewrite load_store_old with (4:=Hn'); auto.
    destruct (ranges_disjoint_dec (range_of_chunk l Mint32) (r, rx)) as [Y|Y].
      rewrite (load_free_other Hf Ha Y).
      erewrite (load_free_other Hn). 2: erewrite eq_alloc with (1:=EQ); rewrite Hr'; apply Ha. 2: exact Y.
      rewrite load_store_old with (4:=Hs); auto.
      apply eq_load; auto.
    rewrite (load_free_overlap Hf Ha Y).
    eapply load_free_overlap; try eassumption.
    rewrite eq_alloc with (1:=EQ).
    rewrite Hr'.
    assumption.
    intros ar ak.
     specialize Hr' with ar ak.
     pose proof (store_preserves_allocated_ranges Hn' ar ak).
     pose proof (free_preserves_allocated Hf ar ak).
     pose proof (free_preserves_allocated_back Hf ar ak).
     pose proof (free_preserves_allocated Hn ar ak).
     pose proof (free_preserves_allocated_back Hn ar ak).
     pose proof (store_preserves_allocated_ranges Hs ar ak).
     pose proof (EQ.(eq_alloc) ar ak).
     destruct ar as (ar, ari).
     pose proof (free_not_allocated Hf ari ak).
     pose proof (free_not_allocated Hn ari ak).
     unfold fst in *.
     intuition (subst; intuition).
   intros b.
   pose proof (EQ.(eq_restr) b).
   pose proof (restr_of_store Hs).
   pose proof (restr_of_store Hn').
   pose proof (restr_of_free Hf).
   pose proof (restr_of_free Hn).
   congruence.
  Qed.

Axiom emem_is_eq : forall m m', m == m' -> m = m'.
This is axiom is safe because we always access memory on well aligned pointer. It could be remove if we lift every definitions that deal with memory with == instead of =

Generated by coq2html