Library mcertikos.conlib.conmtlib.AlgebraicMemImpl

Require Import Coqlib.
Require Import Integers.
Require Import MemoryX.
Require Import Values.
Require Import Events.
Require Import AST.
Require Import Globalenvs.
Require Import AlgebraicMem.

Section IMPLEMENT.

  Context `{Hmem: Mem.MemoryModelX}.

  Fixpoint lift_nextblock m (n: nat) {struct n}: mem :=
    match n with
      | O ⇒ m
      | S n´ ⇒ lift_nextblock (fst (Mem.alloc m 0 0)) n´
    end.

  Definition catch_up m gm :=
    Mem.extends (lift_nextblock m (Pos.to_nat (Mem.nextblock gm) - Pos.to_nat (Mem.nextblock m))) gm.

The situation with permissions is somewhat subtle. The basic idea is that no permission should be present on both memory states, so that operations in one can't interefere with the other. However, for the initial memory to be related, we need to allow both to carry a Nonempty permission, which is what we get for the blocks corresponding to function definitions. Yet in order to prove mem_free_disjoint_union, we need to know that the untouched memory state has no permission whatsoever for the range being freed (cf. Mem.free_right_extends).
To state a constraint on the permissions of the two memory states which ensures these situations are both supported, we use the following permission compatibility relation: two Nonempty permissions are compatible, but Freeable is not compatible with any other permission.

  Inductive perm_compatible: permission → permission → Prop :=
    | perm_compatible_nonempty: perm_compatible Nonempty Nonempty.

  Inductive disjoint_union: mem → mem → mem → Prop :=
  | disjoint_union_intro:
      ∀ m1 m2 gm
             (Hext1: catch_up m1 gm)
             (Hext2: catch_up m2 gm)
             (Hnext: Mem.nextblock gm = Pos.max (Mem.nextblock m1) (Mem.nextblock m2))
             (HpermF: ∀ b o k p1 p2,
                        Mem.perm m1 b o k p1 →
                        Mem.perm m2 b o k p2 →
                        perm_compatible p1 p2),
        disjoint_union m1 m2 gm.

  Lemma disjoint_union_nextblock_max:
    ∀ m m´ m0,
      disjoint_union m m0 m´ →
      Mem.nextblock m´ = Pos.max (Mem.nextblock m) (Mem.nextblock m0).
  Proof.
    destruct 1. trivial.
  Qed.

  Lemma disjoint_union_nextblock:
    ∀ m m´ m0,
      disjoint_union m m0 m´ →
      (Mem.nextblock m ≤ Mem.nextblock m´)%positive.
  Proof.
    destruct 1. rewrite Hnext.
    xomega.
  Qed.

  Lemma perm_compatible_comm p1 p2:
    perm_compatible p1 p2 →
    perm_compatible p2 p1.
  Proof.
    destruct 1; constructor.
  Qed.

  Lemma disjoint_union_commutativity:
    ∀ m m0 m´,
      disjoint_union m m0 m´ →
      disjoint_union m0 m m´.
  Proof.
    destruct 1. constructor; eauto.
    - rewrite Hnext. eapply Pos.max_comm.
    - eauto using perm_compatible_comm.
  Qed.

  Lemma lift_nextblock_target_eq:
    ∀ n m m´,
      lift_nextblock m n = m´ →
      Pos.to_nat (Mem.nextblock m´) = (Pos.to_nat (Mem.nextblock m) + n) % nat.
  Proof.
    induction n.
    - simpl; intros; subst. omega.
    - simpl; intros.
      destruct (Mem.alloc m 0 0) eqn: Halloc.
      simpl in H.
      eapply Mem.nextblock_alloc in Halloc.
      exploit IHn; eauto. rewrite Halloc.
      intros Hn. rewrite Hn. xomega.
  Qed.

  Lemma lift_nextblock_target_eq´ :
    ∀ n m,
      Pos.to_nat (Mem.nextblock (lift_nextblock m n)) = (Pos.to_nat (Mem.nextblock m) + n) % nat.
  Proof.
    intros n m.
    apply lift_nextblock_target_eq.
    reflexivity.
  Qed.

  Lemma lift_nextblock_source_eq:
    ∀ m m´,
      lift_nextblock m 0 = m´ →
      m´ = m.
  Proof.
    simpl; intros.
    subst. reflexivity.
  Qed.

  Lemma lift_nextblock_extends:
    ∀ nb m m´ m0 m0´,
      lift_nextblock m nb = m´ →
      Mem.extends m m0 →
      lift_nextblock m0 nb = m0´ →
      Mem.extends m´ m0´.
  Proof.
    induction nb; simpl; intros.
    - subst. assumption.
    - destruct (Mem.alloc m 0 0) eqn: Halloc.
      exploit Mem.alloc_extends; eauto; try reflexivity.
      intros (m1´ & Halloc´ & Hext).
      rewrite Halloc´ in H1. simpl in ×.
      eapply IHnb; eauto.
  Qed.

  Lemma lift_nextblock_unchanged_on:
    ∀ nb m m´ P,
      lift_nextblock m nb = m´ →
      Mem.unchanged_on P m m´.
  Proof.
    induction nb; simpl; intros.
    - subst. eapply Mem.unchanged_on_refl.
    - destruct (Mem.alloc m 0 0) eqn: Halloc.
      simpl in H.
      eapply Mem.unchanged_on_trans.
      + eapply Mem.alloc_unchanged_on; eauto.
      + eapply IHnb; eauto.
  Qed.

  Require Import CommonTactic.
  Require Import FunctionalExtensionality.

  Lemma inject_incr_eq:
    ∀ f f´ b,
      inject_incr f f´ →
      f´ b = None →
      (∀ b0, b0 ≠ b → f´ b0 = f b0) →
      f´ = f.
  Proof.
    intros. eapply functional_extensionality.
    intros. destruct (peq x b); subst.
    - specialize (H b).
      rewrite H0. destruct (f b).
      + destruct p. specialize (H _ _ refl_equal).
        congruence.
      + trivial.
    - eapply H1; auto.
  Qed.

  Lemma lift_nextblock_left_unmapped_inject:
    ∀ nb m m´ m0 f,
      lift_nextblock m nb = m´ →
      Mem.inject f m m0 →
      Mem.inject f m´ m0.
  Proof.
    induction nb; simpl; intros.
    - subst. assumption.
    - destruct (Mem.alloc m 0 0) eqn: Halloc.
      exploit Mem.alloc_left_unmapped_inject; eauto.
      intros (f´ & Hinject & Hincr & Hf0 & Hfb).
      simpl in ×.
      exploit (IHnb m1 m´ m0 f); eauto.
      exploit inject_incr_eq; eauto.
      intros Heq. subst. assumption.
  Qed.

  Lemma lift_nextblock_right_inject:
    ∀ nb m m´ m0 f,
      lift_nextblock m nb = m´ →
      Mem.inject f m0 m →
      Mem.inject f m0 m´.
  Proof.
    induction nb; simpl; intros.
    - subst. assumption.
    - destruct (Mem.alloc m 0 0) eqn: Halloc.
      exploit Mem.alloc_right_inject; eauto.
  Qed.

  Lemma lift_nextblock_inject:
    ∀ nb m m´ m0 m0´ f,
      lift_nextblock m nb = m´ →
      Mem.inject f m m0 →
      lift_nextblock m0 nb = m0´ →
      Mem.inject f m´ m0´.
  Proof.
    intros.
    eapply lift_nextblock_left_unmapped_inject in H; eauto.
    eapply lift_nextblock_right_inject; eauto.
  Qed.

  Lemma lift_nextblock_perm:
    ∀ nb m b ofs P p,
      Mem.perm (lift_nextblock m nb) b ofs P p →
      Mem.perm m b ofs P p.
  Proof.
    induction nb; simpl; intros.
    - assumption.
    - destruct (Mem.alloc m 0 0) eqn: Halloc.
      simpl in H. exploit IHnb; eauto.
      intros Hperm.
      eapply Mem.perm_alloc_4; eauto.
      red; intros; subst.
      exploit Mem.perm_alloc_3; eauto.
      intros. omega.
  Qed.

  Lemma lift_nextblock_perm´:
    ∀ nb m b ofs P p,
      Mem.perm m b ofs P p →
      Mem.perm (lift_nextblock m nb) b ofs P p.
  Proof.
    induction nb; simpl; intros.
    - assumption.
    - destruct (Mem.alloc m 0 0) eqn: Halloc.
      simpl. eapply IHnb; eauto.
      eapply Mem.perm_alloc_1; eauto.
  Qed.

  Lemma lift_nextblock_inject_neutral:
    ∀ nb m,
      Mem.inject_neutral (Mem.nextblock m) m →
      Mem.inject_neutral (Mem.nextblock (lift_nextblock m nb))
                         (lift_nextblock m nb).
  Proof.
    induction nb; simpl; intros.
    - assumption.
    - destruct (Mem.alloc m 0 0) eqn: Halloc. simpl.
      eapply IHnb; eauto.
      exploit Mem.nextblock_alloc; eauto.
      intros Hnb. rewrite Hnb.
      eapply Mem.alloc_inject_neutral; eauto.
      + eapply Mem.inject_neutral_incr; eauto.
        xomega.
      + xomega.
  Qed.

  Lemma lift_nextblock_generic (P: mem → mem → Prop) m1 m2 n:
    P m1 m2 →
    (∀ m1´ m2´ m1´´ m2´´ b1 b2,
       (Mem.nextblock m1 ≤ Mem.nextblock m1´)%positive →
       (Mem.nextblock m2 ≤ Mem.nextblock m2´)%positive →
       Mem.alloc m1´ 0 0 = (m1´´, b1) →
       Mem.alloc m2´ 0 0 = (m2´´, b2) →
       P m1´ m2´ → P m1´´ m2´´) →
    P (lift_nextblock m1 n) (lift_nextblock m2 n).
  Proof.
    intros Hm H.
    revert Hm.
    generalize (Pos.le_refl (Mem.nextblock m1))
               (Pos.le_refl (Mem.nextblock m2)).
    generalize m1 at 2 3 4, m2 at 2 3 4.
    induction n.
    - eauto.
    - simpl.
      intros m1´ m2´ Hm1´ Hm2´ HmP.
      destruct (Mem.alloc m1´ _ _) as [m1´´ b1] eqn:Halloc1; simpl.
      destruct (Mem.alloc m2´ _ _) as [m2´´ b2] eqn:Halloc2; simpl.
      eapply IHn; eauto;
      etransitivity; eauto.
      + erewrite (Mem.nextblock_alloc m1´ 0 0 m1´´); eauto; xomega.
      + erewrite (Mem.nextblock_alloc m2´ 0 0 m2´´); eauto; xomega.
  Qed.

  Lemma lift_nextblock_add:
    ∀ nb1 nb2 nb m,
      (nb = nb1 + nb2) % nat →
      lift_nextblock (lift_nextblock m nb1) nb2 = lift_nextblock m nb.
  Proof.
    induction nb1; simpl; intros.
    - subst; reflexivity.
    - subst. simpl. destruct (Mem.alloc m 0 0) eqn: Halloc. simpl.
      eapply IHnb1; eauto.
  Qed.

  Lemma lift_nextblock_add´ :
    ∀ nb1 nb2 m,
      lift_nextblock m (nb1 + nb2) = lift_nextblock (lift_nextblock m nb1) nb2.
  Proof.
    intros.
    symmetry.
    eapply lift_nextblock_add; eauto.
  Qed.

  Lemma catch_up_lift_nextblock_right:
    ∀ m gm nb,
      (Mem.nextblock m ≤ Mem.nextblock gm)%positive →
      catch_up m gm →
      catch_up m (lift_nextblock gm nb).
  Proof.
    unfold catch_up.
    intros m gm nb H H0.
    rewrite (lift_nextblock_target_eq _ gm _ (eq_refl _)).
    generalize H. intro H_.
    apply Pos2Nat.inj_le in H_.
    replace (Pos.to_nat (Mem.nextblock gm) + nb - Pos.to_nat (Mem.nextblock m))%nat
    with (Pos.to_nat (Mem.nextblock gm) - Pos.to_nat (Mem.nextblock m) + nb)%nat
      by omega.
    rewrite <- (lift_nextblock_add _ nb _ m (eq_refl _)).
    eapply lift_nextblock_extends; eauto.
  Qed.

  Lemma catch_up_lift_nextblock:
    ∀ m gm nb,
      catch_up m gm →
      catch_up (lift_nextblock m nb) (lift_nextblock gm nb).
  Proof.
    unfold catch_up.
    intros m gm nb H.
    rewrite (lift_nextblock_target_eq _ gm _ (eq_refl _)).
    rewrite (lift_nextblock_target_eq _ m _ (eq_refl _)).
    replace (Pos.to_nat (Mem.nextblock gm) + nb - (Pos.to_nat (Mem.nextblock m) + nb))%nat
    with (Pos.to_nat (Mem.nextblock gm) - Pos.to_nat (Mem.nextblock m))%nat
      by omega.
    erewrite lift_nextblock_add by eauto.
    rewrite plus_comm.
    rewrite <- (lift_nextblock_add _ nb _ m (eq_refl _)).
    eapply lift_nextblock_extends; eauto.
  Qed.

  Lemma disjoint_union_lift_nextblock_right:
    ∀ m m0 m´ nb,
      disjoint_union m m0 m´ →
      (Mem.nextblock m ≤ Mem.nextblock m0) % positive →
      disjoint_union m (lift_nextblock m0 nb) (lift_nextblock m´ nb).
  Proof.
    destruct 1; intros. constructor.
    - apply catch_up_lift_nextblock_right; auto.
      rewrite Hnext. apply Pos.le_max_l.
    - apply catch_up_lift_nextblock; auto.
    - pose proof (lift_nextblock_target_eq nb gm _ refl_equal) as Hnb.
      pose proof (lift_nextblock_target_eq nb m2 _ refl_equal) as Hnb´.
      rewrite Pos.max_r in Hnext; try assumption.
      rewrite Hnext in ×.
      rewrite Pos.max_r.
      + eapply Pos2Nat.inj. congruence.
      + xomega.
    - intros. eapply lift_nextblock_perm in H1. eauto.
  Qed.

  Lemma nat_sub_aux:
    ∀ a b c,
      (c ≤ b) % nat →
      (a + (b - c) = a + b - c) % nat.
  Proof.
    intros. omega.
  Qed.

  Lemma extends_catch_up m1 m2:
    Mem.extends m1 m2 →
    catch_up m1 m2.
  Proof.
    intros H.
    unfold catch_up.
    erewrite <- Mem.mext_next; eauto.
    replace (Pos.to_nat (Mem.nextblock m1) - Pos.to_nat (Mem.nextblock m1))%nat
            with O by omega.
    assumption.
  Qed.

  Lemma catch_up_lift_nextblock_left m gm nb:
    (Mem.nextblock m ≤ Mem.nextblock gm)%positive →
    (nb ≤ Pos.to_nat (Mem.nextblock gm) - Pos.to_nat (Mem.nextblock m))%nat →
    catch_up m gm →
    catch_up (lift_nextblock m nb) gm.
  Proof.
    intros H H0.
    unfold catch_up.
    intros H1.
    erewrite lift_nextblock_add by eauto.
    rewrite lift_nextblock_target_eq´ .
    replace (nb + (Pos.to_nat (Mem.nextblock gm) - (Pos.to_nat (Mem.nextblock m) + nb)))%nat
    with (Pos.to_nat (Mem.nextblock gm) - Pos.to_nat (Mem.nextblock m))%nat ;
      auto.
    omega.
  Qed.

  Lemma disjoint_union_lift_nextblock_right´:
    ∀ m m0 m´ nb nb´,
      disjoint_union m m0 m´ →
      (Mem.nextblock m0 ≤ Mem.nextblock m) % positive →
      nb´ = (nb - (Pos.to_nat (Mem.nextblock m) - Pos.to_nat(Mem.nextblock m0))) % nat →
      disjoint_union m (lift_nextblock m0 nb) (lift_nextblock m´ nb´).
  Proof.
    destruct 1; intros. constructor.
    - apply catch_up_lift_nextblock_right; auto.
      rewrite Hnext. apply Pos.le_max_l.
    - generalize H. intro H_.
      apply Pos2Nat.inj_le in H_.
      rewrite Pos.max_l in Hnext by xomega.
      destruct (le_lt_dec nb (Pos.to_nat (Mem.nextblock m1) - Pos.to_nat (Mem.nextblock m2))%nat).
      + assert (nb´ = O) by omega.
        clear H0.
        subst.
        simpl.
        eapply catch_up_lift_nextblock_left; eauto; congruence.
      + assert (nb = Pos.to_nat (Mem.nextblock m1) - Pos.to_nat (Mem.nextblock m2) + nb´)%nat
               by omega.
        rewrite H1 ; clear H1.
        erewrite <- (lift_nextblock_add _ nb´); eauto.
        apply catch_up_lift_nextblock.
        apply catch_up_lift_nextblock_left; auto.
        × congruence.
        × rewrite Hnext. xomega.
    - pose proof (lift_nextblock_target_eq nb´ gm _ refl_equal) as Hnb.
      pose proof (lift_nextblock_target_eq nb m2 _ refl_equal) as Hnb´.
      rewrite Pos.max_l in Hnext; [| xomega].
      rewrite Hnext in ×.
      destruct (le_lt_dec nb (Pos.to_nat (Mem.nextblock m1) - Pos.to_nat(Mem.nextblock m2))).
      + assert (Heq: nb´ = 0 % nat).
        { subst. omega. }
        rewrite Heq.
        rewrite Pos.max_l.
        × rewrite (lift_nextblock_source_eq gm _ refl_equal).
          assumption.
        × xomega.
      + rewrite Pos.max_r.
        × eapply Pos2Nat.inj. rewrite Hnb, Hnb´.
          subst nb´.
          rewrite nat_sub_aux; xomega.
        × xomega.
    - intros. eapply lift_nextblock_perm in H2. eauto.
  Qed.

  Lemma lift_nextblock_source_eq´:
    ∀ m a b,
      a = b →
      lift_nextblock m (a - b) = m.
  Proof.
    intros. rewrite <- H.
    replace ((a - a) % nat) with O by omega.
    eapply lift_nextblock_source_eq.
    trivial.
  Qed.

  Lemma catch_up_extends m1 m2:
    catch_up m1 m2 →
    Mem.nextblock m1 = Mem.nextblock m2 →
    Mem.extends m1 m2.
  Proof.
    intros H H0.
    unfold catch_up in H.
    rewrite H0 in H.
    replace (Pos.to_nat (Mem.nextblock m2) - Pos.to_nat (Mem.nextblock m2))%nat with O in H by omega.
    assumption.
  Qed.

  Lemma catch_up_alloc_right m gm lo hi gm´ b:
    (Mem.nextblock m ≤ Mem.nextblock gm)%positive →
    catch_up m gm →
    Mem.alloc gm lo hi = (gm´, b) →
    catch_up m gm´.
  Proof.
    intros H H0 H1.
    exploit Mem.nextblock_alloc; eauto. intros.
    unfold catch_up.
    rewrite H2.
    rewrite Pos2Nat.inj_succ.
    generalize H. intro H_.
    apply Pos2Nat.inj_le in H_.
    replace (S (Pos.to_nat (Mem.nextblock gm)) - Pos.to_nat (Mem.nextblock m))%nat
    with ((Pos.to_nat (Mem.nextblock gm) - Pos.to_nat (Mem.nextblock m)) + 1)%nat
      by omega.
    erewrite <- lift_nextblock_add by reflexivity.
    simpl.
    destruct (Mem.alloc (lift_nextblock m _) 0 0) as [m´ ?] eqn:ALLOC.
    simpl.
    unfold catch_up in H0.
    exploit (Mem.alloc_empty_extends _ _ _ _ _ _ lo hi H0 ALLOC); auto with zarith.
    destruct 1 as (? & ALLOC´ & EXT).
    congruence.
  Qed.

  Lemma catch_up_alloc m gm lo hi m´ b:
    (Mem.nextblock m = Mem.nextblock gm)%positive →
    catch_up m gm →
    Mem.alloc m lo hi = (m´, b) →
    ∃ gm´ ,
      Mem.alloc gm lo hi = (gm´, b) ∧
      catch_up m´ gm´.
  Proof.
    intros H H0 H1.
    exploit catch_up_extends; eauto.
    intros H2.
    exploit Mem.alloc_extends; eauto with zarith.
    destruct 1 as (? & ? & ?); eauto using extends_catch_up.
  Qed.

  Lemma alloc_disjoint_union:
    ∀ m m´ m0 gm i sz b,
      Mem.alloc m i sz = (m´, b) →
      (Mem.nextblock m0 ≤ Mem.nextblock m)%positive →
      disjoint_union m m0 gm →
      ∃ gm´,
        Mem.alloc gm i sz = (gm´, b)
        ∧ disjoint_union m´ m0 gm´
        ∧ (Mem.nextblock m0 ≤ Mem.nextblock m´)%positive.
  Proof.
    intros m1 m´ m2 gm i sz b H H0 DISJ.
    inversion DISJ; subst.
    rewrite Pos.max_l in Hnext; trivial.
    generalize Hnext. intro Hnext_. symmetry in Hnext_.
    exploit catch_up_alloc; eauto.
    destruct 1 as (gm´ & Halloc & Hext1´).
    generalize H0. intro H0_. rewrite Hnext_ in H0_.
    exploit catch_up_alloc_right; eauto.
    intros.
    assert (Hle: (Mem.nextblock m2 ≤ Mem.nextblock m´)%positive).
    {
      eapply Mem.nextblock_alloc in H.
      rewrite H. xomega.
    }
    refine_split´; eauto.
    constructor; eauto.
    - eapply Mem.nextblock_alloc in Halloc.
      rewrite Pos.max_l; trivial.
      eapply Mem.nextblock_alloc in H.
      rewrite Halloc, H, Hnext. trivial.
    - intros.
      generalize H. intro H_.
      eapply Mem.perm_alloc_inv in H; eauto.
      destruct (eq_block b0 b); subst; eauto.
      apply Mem.perm_valid_block in H3.
      edestruct Mem.fresh_block_alloc; eauto.
      unfold Mem.valid_block in × . xomega.
  Qed.

  Require Import MemoryExtra.

  Lemma lift_nextblock_free nb:
    ∀ m b lo hi m1,
      Mem.free m b lo hi = Some m1 →
      ∃ m2,
        Mem.free (lift_nextblock m nb) b lo hi = Some m2 ∧
        Mem.extends (lift_nextblock m1 nb) m2.
  Proof.
    induction nb.
    {
      simpl.
      intros m b lo hi m1 H.
      eauto using Mem.extends_refl.
    }
    intros m b lo hi m0 H.
    replace (S nb) with (nb + 1)%nat by omega.
    repeat rewrite lift_nextblock_add´ .
    apply IHnb in H; clear IHnb.
    destruct H as (m1 & Hm1 & EXT).
    destruct (Mem.alloc m1 0 0) as [m2 b2] eqn:ALLOC1.
    simpl.
    destruct (Mem.alloc (lift_nextblock m nb) 0 0) as [m1´ b1´ ] eqn:ALLOC1´.
    simpl.
    assert (b1´ = b2).
    {
      apply Mem.alloc_result in ALLOC1´.
      apply Mem.alloc_result in ALLOC1.
      apply Mem.nextblock_free in Hm1.
      congruence.
    }
    subst.
    exploit Mem.free_alloc_reverse_extends; eauto.
    destruct 1 as (m2´ & FREE2´ & EXT2´).
    esplit.
    split; eauto.
    eapply Mem.extends_extends_compose; [ | eassumption ] .
    destruct (Mem.alloc (lift_nextblock m0 nb) 0 0) as [m0´ ? ] eqn:ALLOC0´ .
    simpl.
    exploit Mem.alloc_extends.
    + eapply EXT.
    + eassumption.
    + apply Z.le_refl.
    + apply Z.le_refl.
    + destruct 1 as (? & ? & ?).
      congruence.
  Qed.

  Lemma catch_up_free m gm lo hi m´ b:
    catch_up m gm →
    Mem.free m b lo hi = Some m´ →
    ∃ gm´ ,
      Mem.free gm b lo hi = Some gm´ ∧
      catch_up m´ gm´.
  Proof.
    intros H H0.
    generalize H0. intro H0_.
    apply lift_nextblock_free with (nb := (Pos.to_nat (Mem.nextblock gm) - Pos.to_nat (Mem.nextblock m))%nat) in H0.
    destruct H0 as (m2 & FREE & EXT).
    unfold catch_up in H.
    revert EXT.
    exploit Mem.free_parallel_extends; eauto.
    destruct 1 as (m2´ & FREE´ & EXT´).
    intros EXT.
    esplit.
    split; eauto.
    unfold catch_up.
    eapply Mem.extends_extends_compose; eauto.
    erewrite Mem.nextblock_free; eauto.
    erewrite (Mem.nextblock_free _ _ _ _ m´); eauto.
  Qed.

  Lemma free_disjoint_union:
    ∀ m m´ m0 gm i sz b,
      Mem.free m b i sz = Some m´ →
      disjoint_union m m0 gm →
      ∃ gm´,
        Mem.free gm b i sz = Some gm´
        ∧ disjoint_union m´ m0 gm´.
  Proof.
    intros m m´ m0 gm i sz b H DISJ.
    inversion DISJ; subst.
    exploit catch_up_free; try eexact Hext1; eauto.
    intros (gm´ & Hfree & Hcatch).
    refine_split´; eauto.
    constructor; auto.
    - unfold catch_up in × |- × .
      erewrite Mem.nextblock_free by eassumption.
      eapply Mem.free_right_extends; eauto.
      intros ofs k p H0 H1.
      apply lift_nextblock_perm in H0.
      eapply Mem.free_range_perm in H.
      specialize (H _ H1).
      eapply (Mem.perm_cur _ _ _ k) in H.
      specialize (HpermF _ _ _ _ _ H H0).
      inversion HpermF.
    - eapply Mem.nextblock_free in H; eauto.
      eapply Mem.nextblock_free in Hfree; eauto.
      rewrite Hfree, H, Hnext. trivial.
    - intros. eapply Mem.perm_free_3 in H0; eauto.
  Qed.

  Lemma lift_nextblock_storebytes_aux nb b o v:
    ∀ m m1,
      Mem.storebytes m b o v = Some m1 →
      ∃ m2,
        Mem.storebytes (lift_nextblock m nb) b o v = Some m2 ∧
        Mem.extends (lift_nextblock m1 nb) m2.
  Proof.
    induction nb.
    {
      simpl.
      intros m m1 H.
      eauto using Mem.extends_refl.
    }
    intros m m0 H.
    replace (S nb) with (nb + 1)%nat by omega.
    repeat rewrite lift_nextblock_add´ .
    apply IHnb in H; clear IHnb.
    destruct H as (m1 & Hm1 & EXT).
    destruct (Mem.alloc m1 0 0) as [m2 b2] eqn:ALLOC1.
    simpl.
    destruct (Mem.alloc (lift_nextblock m nb) 0 0) as [m1´ b1´ ] eqn:ALLOC1´.
    simpl.
    assert (b1´ = b2).
    {
      apply Mem.alloc_result in ALLOC1´.
      apply Mem.alloc_result in ALLOC1.
      apply Mem.nextblock_storebytes in Hm1.
      congruence.
    }
    subst.
    exploit Mem.storebytes_alloc_reverse_extends; eauto.
    destruct 1 as (m2´ & FREE2´ & EXT2´).
    esplit.
    split; eauto.
    eapply Mem.extends_extends_compose; [ | eassumption ] .
    destruct (Mem.alloc (lift_nextblock m0 nb) 0 0) as [m0´ ? ] eqn:ALLOC0´ .
    simpl.
    exploit Mem.alloc_extends.
    + eapply EXT.
    + eassumption.
    + apply Z.le_refl.
    + apply Z.le_refl.
    + destruct 1 as (? & ? & ?).
      congruence.
  Qed.

  Lemma Val_lessdef_inject_id:
    ∀ v v´,
      Val.lessdef v v´ ↔
      val_inject inject_id v v´.
  Proof.
    split; intros.
    - destruct v; inv H; econstructor; try reflexivity.
      rewrite Int.add_zero. trivial.
    - destruct v; inv H; try constructor.
      inv H2. rewrite Int.add_zero.
      constructor.
  Qed.

  Lemma load_disjoint_union:
    ∀ m m0 gm chunk b ofs v,
      Mem.load chunk m b ofs = Some v →
      disjoint_union m m0 gm →
      ∃ v´,
        Mem.load chunk gm b ofs = Some v´
        ∧ Val.lessdef v v´.
  Proof.
    destruct 2.
    eapply Mem.load_extends.
    + eexact Hext1.
    + eapply Mem.load_unchanged_on with (P := fun _ _ ⇒ True); eauto.
      eapply lift_nextblock_unchanged_on; eauto.
  Qed.

  Lemma loadbytes_disjoint_union:
    ∀ m m0 gm b ofs sz bytes,
      Mem.loadbytes m b ofs sz = Some bytes →
      disjoint_union m m0 gm →
      ∃ bytes´,
        Mem.loadbytes gm b ofs sz = Some bytes´
        ∧ list_forall2 (memval_lessdef) bytes bytes´.
  Proof.
    destruct 2.
    eapply Mem.loadbytes_extends.
    + eexact Hext1.
    + eapply Mem.loadbytes_unchanged_on with (P := fun _ _ ⇒ True); eauto.
      eapply lift_nextblock_unchanged_on; eauto.
  Qed.

  Lemma memval_lessdef_list_length:
    ∀ bytes bytes´,
      list_forall2 memval_lessdef bytes bytes´ →
      length (bytes) = length (bytes´).
  Proof.
    induction 1.
    - trivial.
    - simpl. rewrite IHlist_forall2.
      trivial.
  Qed.

  Lemma lift_nextblock_storebytes nb b o v:
    ∀ m m1,
      Mem.storebytes m b o v = Some m1 →
      ∀ v´,
        list_forall2 memval_lessdef v v´ →
      ∃ m2,
        Mem.storebytes (lift_nextblock m nb) b o v´ = Some m2 ∧
        Mem.extends (lift_nextblock m1 nb) m2.
  Proof.
    intros m m1 H v´ H0.
    exploit (lift_nextblock_storebytes_aux nb); eauto.
    destruct 1 as (m2 & Hm2 & EXT).
    clear H.
    revert EXT.
    exploit Mem.storebytes_within_extends; eauto.
    { eapply Mem.extends_refl. }
    destruct 1 as (m2´ & Hm2´ & EXT´).
    intros.
    esplit.
    split; eauto.
    eapply Mem.extends_extends_compose; eauto.
  Qed.

  Lemma catch_up_storebytes m gm o v m´ b v´:
    catch_up m gm →
    Mem.storebytes m b o v = Some m´ →
    list_forall2 memval_lessdef v v´ →
    ∃ gm´ ,
      Mem.storebytes gm b o v´ = Some gm´ ∧
      catch_up m´ gm´.
  Proof.
    intros H H0 H1.
    generalize H0. intro H0_.
    eapply lift_nextblock_storebytes with (nb := (Pos.to_nat (Mem.nextblock gm) - Pos.to_nat (Mem.nextblock m))%nat) in H0; eauto.
    destruct H0 as (m2 & FREE & EXT).
    unfold catch_up in H.
    revert EXT.
    exploit Mem.storebytes_within_extends; eauto.
    { instantiate (1 := v´).
      clear.
      induction v´; constructor; simpl; auto.
      destruct a; econstructor.
      + reflexivity.
      + rewrite Int.add_zero. reflexivity.
    }
    destruct 1 as (m2´ & FREE´ & EXT´).
    intros EXT.
    esplit.
    split; eauto.
    unfold catch_up.
    eapply Mem.extends_extends_compose; eauto.
    erewrite Mem.nextblock_storebytes; eauto.
    erewrite (Mem.nextblock_storebytes _ _ _ _ m´); eauto.
  Qed.

  Lemma storebytes_disjoint_union:
    ∀ m m´ m0 gm b ofs bytes bytes´,
      Mem.storebytes m b ofs bytes = Some m´ →
      disjoint_union m m0 gm →
      list_forall2 (memval_lessdef) bytes bytes´ →
      ∃ gm´,
        Mem.storebytes gm b ofs bytes´ = Some gm´
        ∧ disjoint_union m´ m0 gm´.
  Proof.
    intros m1 m´ m2 gm b ofs bytes bytes´ H DISJ H0.
    inversion DISJ; subst.
    exploit catch_up_storebytes; try eexact Hext1; eauto.
    intros (gm´ & Hstore & Hinject).
    refine_split´; eauto.
    constructor; eauto.
    - eapply Mem.storebytes_outside_extends; eauto.
      {
        erewrite Mem.nextblock_storebytes by eassumption.
        assumption.
      }
      intros ofs´ H1 H2.
      eapply Mem.storebytes_range_perm in H.
      assert (Hp´: Mem.perm m1 b ofs´ Cur Readable).
      {
        eapply Mem.perm_implies with Writable.
        eapply H.
        erewrite memval_lessdef_list_length; eauto.
        constructor.
      }
      apply lift_nextblock_perm in H1.
      specialize (HpermF _ _ _ _ _ Hp´ H1).
      inversion HpermF.
    - eapply Mem.nextblock_storebytes in H; eauto.
      eapply Mem.nextblock_storebytes in Hstore; eauto.
      rewrite Hstore, H, Hnext. trivial.
    - intros. eapply Mem.perm_storebytes_2 in H1; eauto.
  Qed.

  Lemma store_disjoint_union:
    ∀ m m´ m0 gm chunk b ofs v v´,
      Mem.store chunk m b ofs v = Some m´ →
      Val.lessdef v v´ →
      disjoint_union m m0 gm →
      ∃ gm´,
        Mem.store chunk gm b ofs v´ = Some gm´
        ∧ disjoint_union m´ m0 gm´.
  Proof.
    intros m m´ m0 gm chunk b ofs v v´ H H0 H1.
    generalize H. intro H_.
    apply Mem.store_storebytes in H.
    apply Mem.store_valid_access_3 in H_.
    destruct H_ as [_ ALIGN].
    exploit storebytes_disjoint_union; eauto.
    { eapply encode_val_inject.
      eapply Val_lessdef_inject_id.
      eassumption.
    }
    destruct 1 as (gm´ & Hgm´ & DISJ´).
    esplit.
    split; eauto using Mem.storebytes_store.
  Qed.

  Lemma valid_pointer_disjoint_union:
    ∀ m m0 gm b ofs,
      Mem.valid_pointer m b ofs = true →
      disjoint_union m m0 gm →
      Mem.valid_pointer gm b ofs = true.
  Proof.
    intros m m0 gm b ofs H H0.
    destruct H0.
    clear Hext2.
    apply Mem.valid_pointer_nonempty_perm.
    eapply Mem.perm_extends; eauto.
    apply lift_nextblock_perm´ .
    apply Mem.valid_pointer_nonempty_perm.
    assumption.
  Qed.

Initial memory

Below we show that the initial memory of a program with no global variables is related to itself.

  Lemma mem_empty_disjoint_union:
    disjoint_union Mem.empty Mem.empty Mem.empty.
  Proof.
    constructor.
    - apply extends_catch_up.
      apply Mem.extends_refl.
    - apply extends_catch_up.
      apply Mem.extends_refl.
    - rewrite Mem.nextblock_empty.
      reflexivity.
    - intros.
      eelim Mem.perm_empty; eauto.
  Qed.

  Section INIT_MEM.
    Context {F V : Type}.

    Definition self_compatible m :=
      ∀ b ofs k p1 p2,
        Mem.perm m b ofs k p1 →
        Mem.perm m b ofs k p2 →
        perm_compatible p1 p2.

    Lemma alloc_gfun_self_compatible (ge: Genv.t F V) m i f m´:
      Genv.alloc_global ge m (i, Some (Gfun f)) = Some m´ →
      self_compatible m →
      self_compatible m´.
    Proof.
      intros Hm´ Hp.
      simpl in Hm´.
      destruct (Mem.alloc _ _ _) as [ma b´] eqn:Hma.
      destruct (Mem.drop_perm _ _ _ _ _) as [mb|] eqn:Hmb; [|discriminate].
      inversion Hm´; clear Hm´; subst.
      intros b ofs k p1 p2 Hp1 Hp2.
      destruct (Decision.decide (b = b´)) as [Hb´|Hb´]; subst.
      -
        destruct (Decision.decide (0 ≤ ofs < 1)) as [Hofs | Hofs].
        + eapply Mem.perm_drop_2 in Hp1; eauto.
          eapply Mem.perm_drop_2 in Hp2; eauto.
          inversion Hp1; inversion Hp2; constructor.
        + eapply Mem.perm_drop_4 in Hmb; eauto.
          eapply Mem.perm_alloc_3 in Hmb; eauto.
          contradiction.
      -
        eapply Hp.
        + eapply Mem.perm_alloc_4; eauto.
          eapply Mem.perm_drop_4; eauto.
        + eapply Mem.perm_alloc_4; eauto.
          eapply Mem.perm_drop_4; eauto.
    Qed.

    Lemma alloc_none_self_compatible (ge: Genv.t F V) m i m´:
      Genv.alloc_global ge m (i, None) = Some m´ →
      self_compatible m →
      self_compatible m´.
    Proof.
      intros Hm´ Hp.
      simpl in Hm´.
      destruct (Mem.alloc _ _ _) as [ma b´] eqn:Hma.
      inversion Hm´; clear Hm´; subst.
      intros b ofs k p1 p2 Hp1 Hp2.
      destruct (Decision.decide (b = b´)) as [Hb´|Hb´]; subst.
      -
        eapply Mem.perm_alloc_3 in Hma; eauto.
        omega.
      -
        eapply Hp.
        + eapply Mem.perm_alloc_4; eauto.
        + eapply Mem.perm_alloc_4; eauto.
    Qed.

    Lemma noglobvar_self_compatible (p : AST.program F V) m:
      noglobvar p →
      Genv.init_mem p = Some m →
      self_compatible m.
    Proof.
      unfold noglobvar.
      unfold Genv.init_mem.
      intros Hp.
      assert (Hempty: self_compatible Mem.empty).
      {
        intros b ofs k p1 p2 Hp1 Hp2.
        eelim Mem.perm_empty; eauto.
      }
      revert Hempty.
      generalize Mem.empty as m0.
      induction Hp; intros m0 Hm0 Hm.
      - inversion Hm; subst.
        assumption.
      - simpl in Hm.
        destruct (Genv.alloc_global _ _ _) as [m0´|] eqn:Hm0´; try discriminate.
        eapply (IHHp m0´); eauto.
        destruct x as [i [[f|v]|]].
        + eapply alloc_gfun_self_compatible; eauto.
        + contradiction.
        + eapply alloc_none_self_compatible; eauto.
    Qed.

    Lemma init_mem_disjoint_union (p : AST.program F V) m:
      noglobvar p →
      Genv.init_mem p = Some m →
      disjoint_union m m m.
    Proof.
      intros Hp Hm.
      constructor.
      - eapply extends_catch_up.
        eapply Mem.extends_refl.
      - eapply extends_catch_up.
        eapply Mem.extends_refl.
      - rewrite Pos.max_id.
        reflexivity.
      - intros.
        eapply noglobvar_self_compatible; eauto.
    Qed.
  End INIT_MEM.

End IMPLEMENT.

Section INSTANCE.

  Context `{Hmem: Mem.MemoryModelX}.

  Instance algebraicmem : AlgebraicMemory :=
    {
      mem_disjoint_union := disjoint_union;
      mem_lift_nextblock := lift_nextblock
    }.
  Proof.
    - exact disjoint_union_nextblock_max.
    - exact disjoint_union_nextblock.
    - exact disjoint_union_commutativity.
    - exact lift_nextblock_target_eq.
    - exact lift_nextblock_source_eq.
    - exact lift_nextblock_extends.
    - exact lift_nextblock_unchanged_on.
    - exact lift_nextblock_inject.
    - exact lift_nextblock_perm.
    - exact lift_nextblock_inject_neutral.
    - exact lift_nextblock_generic.
    - exact disjoint_union_lift_nextblock_right.
    - exact disjoint_union_lift_nextblock_right´.
    - exact (fun _ _ ⇒ init_mem_disjoint_union).
    - exact alloc_disjoint_union.
    - exact free_disjoint_union.
    - exact store_disjoint_union.
    - exact load_disjoint_union.
    - exact valid_pointer_disjoint_union.
    - exact storebytes_disjoint_union.
    - exact loadbytes_disjoint_union.
  Qed.

End INSTANCE.