Library compcertx.common.MemimplX

Require compcert.common.Memimpl.
Require MemoryX.

Import Coqlib.
Import Values.
Import Memimpl.
Import MemoryX.

Because we need the additional storebytes_empty property, we have to modify the implementation of storebytes...

Definition is_empty {A: Type} (l: list A):
  {l = nil } + {l ≠ nil }.
Proof.
  destruct l; (left; congruence) || (right; congruence).
Defined.

Definition storebytes m b o l :=
  if is_empty l then Some m else Memimpl.storebytes m b o l.

... and we have to again prove every property of storebytes (fortunately, we can reuse the proofs in Memimpl, we just need to extend them)...

Ltac storebytes_tac thm :=
  simpl; intros;
  match goal with
    | H: storebytes ?m1 _ _ ?l = Some ?m2 |- _ ⇒
      unfold storebytes in H;
        destruct (is_empty l);
        [ | eapply thm; eassumption ];
        subst l;
        replace m2 with m1 in × by congruence;
        clear H;
        try congruence;
        unfold Mem.range_perm, range_perm, Mem.valid_access, valid_access;
        intuition (simpl in *; omega)
  end.

Lemma range_perm_storebytes:
   ∀ (m1 : mem) (b : block) (ofs : Z) (bytes : list memval),
   Mem.range_perm m1 b ofs (ofs + Z.of_nat (length bytes)) Cur Writable →
   ∃ m2 : mem , storebytes m1 b ofs bytes = Some m2.
Proof.
  unfold storebytes. intros.
  destruct (is_empty bytes); eauto using range_perm_storebytes.
Qed.

Lemma encode_val_not_empty chunk v:
  encode_val chunk v ≠ nil.
Proof.
  generalize (encode_val_length chunk v). generalize (encode_val chunk v).
  destruct chunk; destruct l; compute; congruence.
Qed.

Lemma storebytes_store:
   ∀ (m1 : mem) (b : block) (ofs : Z) (chunk : AST.memory_chunk)
     (v : val) (m2 : mem),
   storebytes m1 b ofs (encode_val chunk v) = Some m2 →
   (align_chunk chunk | ofs ) → Mem.store chunk m1 b ofs v = Some m2.
Proof.
  unfold storebytes. intros.
  destruct (is_empty (encode_val chunk v)); eauto using storebytes_store.
  edestruct encode_val_not_empty; eauto.
Qed.

Lemma store_storebytes:
   ∀ (m1 : mem) (b : block) (ofs : Z) (chunk : AST.memory_chunk)
     (v : val) (m2 : mem),
   Mem.store chunk m1 b ofs v = Some m2 →
   storebytes m1 b ofs (encode_val chunk v) = Some m2.
Proof.
  unfold storebytes. intros.
  destruct (is_empty (encode_val chunk v)); eauto using store_storebytes.
  edestruct encode_val_not_empty; eauto.
Qed.

Lemma loadbytes_storebytes_same:
   ∀ (m1 : mem) (b : block) (ofs : Z) (bytes : list memval) (m2 : mem),
   storebytes m1 b ofs bytes = Some m2 →
   Mem.loadbytes m2 b ofs (Z.of_nat (length bytes)) = Some bytes.
Proof.
  unfold storebytes. intros.
  destruct (is_empty bytes); eauto using loadbytes_storebytes_same.
  subst; simpl.
  unfold loadbytes. simpl. destruct (range_perm_dec m2 b ofs (ofs + 0) Cur Readable); try reflexivity.
  destruct n. unfold range_perm. intros; omega.
Qed.

Lemma storebytes_concat: ∀ (m : mem) (b : block) (ofs : Z) (bytes1 : list memval)
         (m1 : mem) (bytes2 : list memval) (m2 : mem),
       storebytes m b ofs bytes1 = Some m1 →
       storebytes m1 b (ofs + Z.of_nat (length bytes1)) bytes2 =
       Some m2 → storebytes m b ofs (bytes1 ++ bytes2) = Some m2.
Proof.
  unfold storebytes at 1.
  intros until m2.
  case_eq (is_empty bytes1).
  {
    intros.
    subst. inv H0.
    simpl in ×.
    replace (ofs + 0) with ofs in × by omega.
    assumption.
  }
  intros.
  unfold storebytes in ×.
  destruct (is_empty bytes2).
  {
    inv H1.
    rewrite <- app_nil_end.
    rewrite H.
    assumption.
  }
  exploit (Memimpl.storebytes_concat m b ofs bytes1 m1 bytes2 m2); eauto.
  intros.
  destruct bytes1; try congruence.

HERE transparently use is_empty

  assumption.
Qed.

Lemma storebytes_split:
   ∀ (m : mem) (b : block) (ofs : Z) (bytes1 bytes2 : list memval)
     (m2 : mem),
   storebytes m b ofs (bytes1 ++ bytes2) = Some m2 →
   ∃ m1 : mem ,
     storebytes m b ofs bytes1 = Some m1 ∧
     storebytes m1 b (ofs + Z.of_nat (length bytes1)) bytes2 = Some m2.
Proof.
  unfold storebytes.
  intros.
  destruct (is_empty (bytes1 ++ bytes2)).
  {
    subst.
    inv H.
    destruct (app_eq_nil _ _ e). subst. simpl. eauto.
  }
  destruct (is_empty bytes1).
  {
    subst; simpl. replace (ofs + 0) with ofs in × by omega.
    simpl in ×.
    destruct (is_empty bytes2); eauto.
    contradiction.
  }
  destruct (is_empty bytes2).
  {
    subst.
    rewrite <- app_nil_end in H. eauto.
  }
  eauto using storebytes_split.
Qed.

Lemma is_empty_list_forall2:
  ∀ (A B: Type) (P: A → B → Prop) l1 l2,
    list_forall2 P l1 l2 →
    (l1 = nil ↔ l2 = nil).
Proof.
  intros.
  inversion H; subst.
   tauto.
   split; discriminate.
Qed.

Lemma storebytes_within_extends:
   ∀ (m1 m2 : mem) (b : block) (ofs : Z) (bytes1 : list memval)
     (m1´ : mem) (bytes2 : list memval),
   Mem.extends m1 m2 →
   storebytes m1 b ofs bytes1 = Some m1´ →
   list_forall2 memval_lessdef bytes1 bytes2 →
   ∃ m2´ : mem ,
     storebytes m2 b ofs bytes2 = Some m2´ ∧ Mem.extends m1´ m2´.
Proof.
  unfold storebytes.
  intros.
  destruct (is_empty bytes1); destruct (is_empty bytes2); eauto using storebytes_within_extends.
  × inv H0. eauto.
  × apply is_empty_list_forall2 in H1. exfalso; tauto.
  × apply is_empty_list_forall2 in H1. exfalso; tauto.
Qed.

Lemma storebytes_mapped_inject:
   ∀ (f : meminj) (m1 : mem) (b1 : block) (ofs : Z)
     (bytes1 : list memval) (n1 m2 : mem) (b2 : block)
     (delta : Z) (bytes2 : list memval),
   Mem.inject f m1 m2 →
   storebytes m1 b1 ofs bytes1 = Some n1 →
   f b1 = Some (b2 , delta) →
   list_forall2 (memval_inject f) bytes1 bytes2 →
   ∃ n2 : mem ,
     storebytes m2 b2 (ofs + delta) bytes2 = Some n2 ∧
     Mem.inject f n1 n2.
Proof.
  unfold storebytes.
  intros.
  destruct (is_empty bytes1); destruct (is_empty bytes2); eauto using storebytes_mapped_inject.
  × inv H0. eauto.
  × apply is_empty_list_forall2 in H2. exfalso; tauto.
  × apply is_empty_list_forall2 in H2. exfalso; tauto.
Qed.

Lemma storebytes_empty_inject:
   ∀ (f : meminj) (m1 : mem) (b1 : block) (ofs1 : Z)
     (m1´ m2 : mem) (b2 : block) (ofs2 : Z) (m2´ : mem),
   Mem.inject f m1 m2 →
   storebytes m1 b1 ofs1 nil = Some m1´ →
   storebytes m2 b2 ofs2 nil = Some m2´ → Mem.inject f m1´ m2´.
Proof.
  unfold storebytes; simpl; congruence.
Qed.

Lemma storebytes_unchanged_on:
   ∀ (P : block → Z → Prop) (m : mem) (b : block)
     (ofs : Z) (bytes : list memval) (m´ : mem),
   storebytes m b ofs bytes = Some m´ →
   (∀ i : Z, ofs ≤ i < ofs + Z.of_nat (length bytes) → ¬ P b i) →
   Mem.unchanged_on P m m´.
Proof.
  unfold storebytes. intros.
  destruct (is_empty bytes); eauto using Mem.storebytes_unchanged_on.
  inv H. eapply Mem.unchanged_on_refl.
Qed.

Additional proof not present in CompCert

Lemma storebytes_empty:
  ∀ m b ofs m´,
    storebytes m b ofs nil = Some m´
    → m´ = m.
Proof.
  unfold storebytes. intros.
  destruct (is_empty nil); congruence.
Qed.

Because we need the additional free_range property, we have to modify the implementation of free...

Definition free (m: mem) (b: block) (lo hi: Z): option mem :=
if zle hi lo then Some m else Memimpl.free m b lo hi.

... and we have to again prove every property of free (fortunately, we can reuse the proofs in Memimpl, we just need to extend them)...

Ltac free_tac thm :=
  simpl;
  intros;
  match goal with
    | H: free ?m1 _ ?lo ?hi = Some ?m2 |- _ ⇒
      unfold free in H;
        destruct (zle hi lo);
        try (eapply thm; eassumption);
        replace m2 with m1 in × by congruence;
        clear H;
        try congruence;
        unfold Mem.range_perm, range_perm, Mem.valid_access, valid_access;
        intuition omega
  end.

Lemma range_perm_free:
  ∀ m1 b lo hi,
  range_perm m1 b lo hi Cur Freeable →
  ∃ m2: mem , free m1 b lo hi = Some m2.
Proof.
  unfold free. intros.
  destruct (zle hi lo); eauto using Memimpl.range_perm_free.
Qed.

Lemma free_parallel_extends:
   ∀ (m1 m2 : mem) (b : block) (lo hi : Z) (m1´ : mem),
   extends m1 m2 →
   free m1 b lo hi = Some m1´ →
   ∃ m2´ : mem , free m2 b lo hi = Some m2´ ∧ extends m1´ m2´.
Proof.
  unfold free. intros until 1.
  destruct (zle hi lo); eauto using free_parallel_extends.
  inversion 1; subst; eauto.
Qed.

Additional proof not present in CompCert

Lemma free_range:
  ∀ m1 m1´ b lo hi,
    free m1 b lo hi = Some m1´ →
    (lo < hi)%Z ∨ m1´ = m1.
Proof.
  unfold free. intros.
  destruct (zle hi lo).
   right; congruence.
  left; omega.
Qed.

Because we need the additional inject_neutral_incr property, we have to modify the implementation of inject_neutral...

Definition inject_neutral (thr: block) (m: mem) :=
Memimpl.inject_neutral thr m ∧ (∀ b, Ple thr b → ∀ o k p, ¬ perm m b o k p ).

... and we have to again prove every property of inject_neutral (fortunately, we can reuse the proofs in Memimpl, we just need to extend them)...

Theorem neutral_inject:
  ∀ m, inject_neutral (nextblock m) m → inject (flat_inj (nextblock m)) m m.
Proof.
  destruct 1; eauto using Memimpl.neutral_inject.
Qed.

Theorem empty_inject_neutral:
  ∀ thr, inject_neutral thr empty.
Proof.
  split; eauto using Memimpl.empty_inject_neutral, perm_empty.
Qed.

Theorem alloc_inject_neutral:
  ∀ thr m lo hi b m´,
  alloc m lo hi = (m´, b ) →
  inject_neutral thr m →
  Plt (nextblock m) thr →
  inject_neutral thr m´.
Proof.
  inversion 2; subst.
  split; eauto using Memimpl.alloc_inject_neutral.
  intros.
  intro. eapply perm_valid_block in H5. unfold valid_block in ×. apply nextblock_alloc in H. rewrite H in H5. xomega.
Qed.

Theorem store_inject_neutral:
  ∀ chunk m b ofs v m´ thr,
  store chunk m b ofs v = Some m´ →
  inject_neutral thr m →
  Plt b thr →
  val_inject (flat_inj thr) v v →
  inject_neutral thr m´.
Proof.
  inversion 2; subst.
  split; eauto using Memimpl.store_inject_neutral.
  intros. intro. eapply H2. eassumption. eauto using perm_store_2.
Qed.

Theorem drop_inject_neutral:
  ∀ m b lo hi p m´ thr,
  drop_perm m b lo hi p = Some m´ →
  inject_neutral thr m →
  Plt b thr →
  inject_neutral thr m´.
Proof.
  inversion 2; subst.
  split; eauto using Memimpl.drop_inject_neutral.
  intros. intro. eapply H2. eassumption. eauto using perm_drop_4.
Qed.

Additional proof not present in CompCert

Theorem inject_neutral_incr:
  ∀ m thr, inject_neutral thr m → ∀ thr´, Ple thr thr´ → inject_neutral thr´ m.
Proof.
  intros ? ? [[] PERM].
  split.
  split.
   unfold flat_inj. intros until p. destruct (plt b1 thr´); try discriminate. injection 1; intros until 2; subst. intro. eapply mi_perm. 2: eassumption. unfold flat_inj. destruct (plt b2 thr). reflexivity. edestruct PERM. 2: eassumption. xomega.
   unfold flat_inj. intros until p. destruct (plt b1 thr´); try discriminate. injection 1; intros until 2; subst. intro. ∃ 0; omega.
   unfold flat_inj. intros until delta. destruct (plt b1 thr´); try discriminate. injection 1; intros until 2; subst. intro.
   intros. eapply memval_inject_incr. eapply mi_memval. 2: assumption. unfold flat_inj. destruct (plt b2 thr). reflexivity. edestruct PERM. 2: eassumption. xomega.
   unfold inject_incr. unfold flat_inj. intros until delta. destruct (plt b thr); try discriminate. injection 1; intros until 2; subst. destruct (plt b´ thr´); try reflexivity. xomega.
   intros. eapply PERM. xomega.
Qed.

Theorem free_inject_neutral´:
  ∀ m b lo hi m´ thr,
  Memimpl.free m b lo hi = Some m´ →
  inject_neutral thr m →
  Plt b thr →
  inject_neutral thr m´.
Proof.
  intros until 1. intros [? PERM]. intros.
  exploit free_left_inj; eauto. intro.
  exploit free_right_inj; eauto.
  intros until p. unfold flat_inj. destruct (plt b´ thr); try discriminate. injection 1; intros until 2; subst. replace (ofs + 0) with ofs by omega. intros. eapply Memimpl.perm_free_2; eauto.
  split.
   assumption.
  intros. intro. eapply PERM. eassumption. eauto using Memimpl.perm_free_3.
Qed.

Theorem storebytes_inject_neutral´:
  ∀ m b o l m´ thr,
  Memimpl.storebytes m b o l = Some m´ →
  list_forall2 (memval_inject (Mem.flat_inj thr)) l l →
  Plt b thr →
  inject_neutral thr m →
  inject_neutral thr m´.
Proof.
  inversion 4; subst.
  unfold Memimpl.inject_neutral in H3.
  generalize H. intro STORE.
  eapply storebytes_mapped_inj in STORE; eauto.
  Focus 3.
   unfold flat_inj. destruct (plt b thr); try reflexivity. contradiction.
  destruct STORE as (m2 & STORE & INJ).
  replace (o + 0) with o in × by omega.
  replace m2 with m´ in × by congruence.
  split; auto.
  intros; intro. eapply Memimpl.perm_storebytes_2 in H6; eauto. eapply H4; eauto.
  unfold meminj_no_overlap.
  unfold flat_inj. intros.
  destruct (plt b1 thr); try discriminate.
  destruct (plt b2 thr); try discriminate.
  left; congruence.
Qed.

Extra properties about drop_perm and extends

Theorem drop_perm_right_extends:
  ∀ m1 m2 b lo hi p m2´,
  extends m1 m2 →
  drop_perm m2 b lo hi p = Some m2´ →
  (∀ ofs k p, perm m1 b ofs k p → lo ≤ ofs < hi → False) →
  extends m1 m2´.
Proof.
  intros. inv H. constructor.
  rewrite (nextblock_drop _ _ _ _ _ _ H0). auto.
  eapply drop_outside_inj; eauto.
  unfold inject_id; intros. inv H. eapply H1; eauto. omega.
Qed.

Theorem drop_perm_parallel_extends:
  ∀ m1 m2 b lo hi p m1´,
  extends m1 m2 →
  drop_perm m1 b lo hi p = Some m1´ →
  ∃ m2´,
     drop_perm m2 b lo hi p = Some m2´
  ∧ extends m1´ m2´.
Proof.
  intros.
  inv H.
  exploit drop_mapped_inj; eauto.
  unfold meminj_no_overlap. unfold inject_id. intros; left; congruence.
  reflexivity.
  replace (lo + 0) with lo by omega.
  replace (hi + 0) with hi by omega.
  destruct 1 as [m2´ [FREE INJ]]. ∃ m2´; split; auto.
  constructor; auto.
  rewrite (nextblock_drop _ _ _ _ _ _ H0).
  rewrite (nextblock_drop _ _ _ _ _ _ FREE). auto.
Qed.

... and we need to repackage instances for the CompCert memory model.

Lemma perm_free_2:
   ∀ (m1 : mem) (bf : block) (lo hi : Z) (m2 : mem),
   free m1 bf lo hi = Some m2 →
   ∀ (ofs : Z) (k : perm_kind) (p : permission),
   lo ≤ ofs < hi → ¬ perm m2 bf ofs k p.
Proof.
  free_tac Memimpl.perm_free_2.
Qed.

Lemma perm_free_3:
  ∀ m1 bf lo hi m2, free m1 bf lo hi = Some m2 →
  ∀ b ofs k p,
  perm m2 b ofs k p → perm m1 b ofs k p.
Proof.
  free_tac Memimpl.perm_free_3.
Qed.

Global Instance memory_model_ops: Mem.MemoryModelOps mem.
Proof.
  constructor.
  exact empty.
  exact alloc.
  exact free.
  exact load.
  exact store.
  exact loadbytes.
  exact storebytes.
  exact drop_perm.
  exact nextblock.
  exact perm.
  exact valid_pointer.
  exact extends.
  exact inject.
  exact inject_neutral.
  exact unchanged_on.
Defined.

Qed does not work here, need transparent definitions for MemoryModel*

Here we expose the additional properties that we need, and most of which are actually already proved in the original CompCert implementation.

Global Instance memory_model_x: Mem.MemoryModelX mem.
Proof.
  constructor.
  typeclasses eauto.
  exact extends_extends_compose.
  exact inject_extends_compose.
  exact inject_compose.
  exact extends_inject_compose.
  apply inject_neutral_incr.
  now free_tac free_inject_neutral´.
  apply drop_perm_right_extends.
  apply drop_perm_parallel_extends.
  now storebytes_tac storebytes_inject_neutral´.
  exact free_range.
  exact storebytes_empty.
Qed.