Library mcertikos.conlib.conmtlib.AlgebraicMem

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

Initial memories are related to themselves by mem_disjoint_union whenever the program they are constructed from does not contain any global variables. Below we define that criterion and show that it is decidable.

Section NOGLOBVAR.
  Context {F V : Type}.

  Definition globdef_not_var (d : option (globdef F V)) :=
    match d with
      | Some (Gvar v) ⇒ False
      | _ ⇒ True
    end.

  Program Instance globdef_not_var_dec d : Decision (globdef_not_var d) :=
    match d with
      | Some (Gvar v) ⇒ right _
      | _ ⇒ left _
    end.
  Next Obligation.
    destruct d as [[|]|]; simpl; eauto.
    elim (H v eq_refl).
  Qed.

  Definition noglobvar (p: program F V) :=
    Forall (fun d ⇒ globdef_not_var (snd d)) (prog_defs p).

  Global Instance noglobvar_dec p : Decision (noglobvar p) := _.
End NOGLOBVAR.

With this we can define the interface of mem_disjoint_union.

Section WITHMEM.

  Class AlgebraicMemory `{Hmem: Mem.MemoryModelX} :=
    {
      mem_disjoint_union : mem → mem → mem → Prop;

      mem_lift_nextblock : mem → nat → mem;

      mem_disjoint_union_nextblock_max:
        ∀ m m´ m0,
          mem_disjoint_union m m0 m´ →
          Mem.nextblock m´ = Pos.max (Mem.nextblock m) (Mem.nextblock m0);

      mem_disjoint_union_nextblock:
        ∀ m m´ m0,
          mem_disjoint_union m m0 m´ →
          (Mem.nextblock m ≤ Mem.nextblock m´)%positive;
      
      mem_disjoint_union_commutativity:
        ∀ m m0 m´,
          mem_disjoint_union m m0 m´ →
          mem_disjoint_union m0 m m´;
      
      mem_lift_nextblock_target_eq :
        ∀ n m m´,
          mem_lift_nextblock m n = m´ →
          Pos.to_nat (Mem.nextblock m´) = (Pos.to_nat (Mem.nextblock m) + n) % nat;

      mem_lift_nextblock_source_eq :
        ∀ m m´,
          mem_lift_nextblock m 0 = m´ →
          m´ = m;

      mem_lift_nextblock_extends:
        ∀ nb m m´ m0 m0´,
          mem_lift_nextblock m nb = m´ →
          Mem.extends m m0 →
          mem_lift_nextblock m0 nb = m0´ →
          Mem.extends m´ m0´;

      mem_lift_nextblock_unchanged_on:
        ∀ nb m m´ P,
          mem_lift_nextblock m nb = m´ →
          Mem.unchanged_on P m m´;

      
      mem_lift_nextblock_inject:
        ∀ nb m m´ m0 m0´ f,
          mem_lift_nextblock m nb = m´ →
          Mem.inject f m m0 →
          mem_lift_nextblock m0 nb = m0´ →
          Mem.inject f m´ m0´;
      
      mem_lift_nextblock_perm:
        ∀ nb m b ofs P p,
          Mem.perm (mem_lift_nextblock m nb) b ofs P p →
          Mem.perm m b ofs P p;
      
      mem_lift_nextblock_inject_neutral:
        ∀ nb m,
          Mem.inject_neutral (Mem.nextblock m) m →
          Mem.inject_neutral (Mem.nextblock (mem_lift_nextblock m nb))
                             (mem_lift_nextblock m nb);

      mem_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 (mem_lift_nextblock m1 n) (mem_lift_nextblock m2 n);

      mem_disjoint_union_lift_nextblock_right:
        ∀ m m0 m´ nb,
          mem_disjoint_union m m0 m´ →
          (Mem.nextblock m ≤ Mem.nextblock m0) % positive →
          mem_disjoint_union m (mem_lift_nextblock m0 nb) (mem_lift_nextblock m´ nb);

      mem_disjoint_union_lift_nextblock_right´:
        ∀ m m0 m´ nb nb´,
          mem_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 →
          mem_disjoint_union m (mem_lift_nextblock m0 nb) (mem_lift_nextblock m´ nb´);

      init_mem_disjoint_union {F V}:
        ∀ (p: program F V) m,
          noglobvar p →
          Genv.init_mem p = Some m →
          mem_disjoint_union m m m;

      mem_alloc_disjoint_union:
        ∀ m m´ m0 gm i sz b,
          Mem.alloc m i sz = (m´, b) →
          (Mem.nextblock m0 ≤ Mem.nextblock m)%positive →
          mem_disjoint_union m m0 gm →
          ∃ gm´,
            Mem.alloc gm i sz = (gm´, b)
            ∧ mem_disjoint_union m´ m0 gm´
            ∧ (Mem.nextblock m0 ≤ Mem.nextblock m´)%positive;

      mem_free_disjoint_union:
        ∀ m m´ m0 gm i sz b,
          Mem.free m b i sz = Some m´ →
          mem_disjoint_union m m0 gm →
          ∃ gm´,
            Mem.free gm b i sz = Some gm´
            ∧ mem_disjoint_union m´ m0 gm´;

      mem_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´ →
          mem_disjoint_union m m0 gm →
          ∃ gm´,
            Mem.store chunk gm b ofs v´ = Some gm´
            ∧ mem_disjoint_union m´ m0 gm´;

      mem_load_disjoint_union:
        ∀ m m0 gm chunk b ofs v,
          Mem.load chunk m b ofs = Some v →
          mem_disjoint_union m m0 gm →
          ∃ v´,
            Mem.load chunk gm b ofs = Some v´
            ∧ Val.lessdef v v´;

      mem_valid_pointer_disjoint_union:
        ∀ m m0 gm b ofs,
          Mem.valid_pointer m b ofs = true →
          mem_disjoint_union m m0 gm →
          Mem.valid_pointer gm b ofs = true;

      mem_storebytes_disjoint_union:
        ∀ m m´ m0 gm b ofs bytes bytes´,
          Mem.storebytes m b ofs bytes = Some m´ →
          mem_disjoint_union m m0 gm →
          list_forall2 (memval_lessdef) bytes bytes´ →
          ∃ gm´,
            Mem.storebytes gm b ofs bytes´ = Some gm´
            ∧ mem_disjoint_union m´ m0 gm´;
      
      mem_loadbytes_disjoint_union:
        ∀ m m0 gm b ofs sz bytes,
          Mem.loadbytes m b ofs sz = Some bytes →
          mem_disjoint_union m m0 gm →
          ∃ bytes´,
            Mem.loadbytes gm b ofs sz = Some bytes´
            ∧ list_forall2 (memval_lessdef) bytes bytes´

    }.

  Section WITHALGEMEM.

    Context `{Hmem: Mem.MemoryModelX}.
    Context `{agmem: !AlgebraicMemory}.

    Lemma mem_lift_nextblock_valid_access:
      ∀ m nb chunk b o p,
        Mem.valid_access (mem_lift_nextblock m nb) chunk b o p →
        Mem.valid_access m chunk b o p.
    Proof.
      unfold Mem.valid_access; intros.
      destruct H as (Hvalid & Ha).
      split; trivial.
      unfold Mem.range_perm in ×.
      intros.
      eapply mem_lift_nextblock_perm; eauto.
    Qed.

    Lemma mem_lift_nextblock_load:
      ∀ m nb b o chunk,
        Mem.load chunk (mem_lift_nextblock m nb) b o = Mem.load chunk m b o.
    Proof.
      intros.
      specialize (mem_lift_nextblock_unchanged_on
                    nb m _
                    (fun b: block ⇒ fun z: Z ⇒ True)
                    refl_equal).
      intros.
      destruct (Mem.load chunk m b o) eqn: Hload.
      - eapply Mem.load_unchanged_on; eauto.
        intros. simpl. trivial.
      - destruct (Mem.load chunk (mem_lift_nextblock m nb) b o) eqn: Hload´; trivial.
        eapply Mem.load_valid_access in Hload´.
        eapply mem_lift_nextblock_valid_access in Hload´.
        eapply Mem.valid_access_load in Hload´.
        rewrite Hload in Hload´.
        destruct Hload´ as (v´ & HF). inv HF.
    Qed.

    Lemma mem_lift_nextblock_source_target_le :
      ∀ m m´ n,
        mem_lift_nextblock m n = m´ →
        (Mem.nextblock m ≤ Mem.nextblock m´) % positive.
    Proof.
      intros.
      eapply mem_lift_nextblock_target_eq in H. xomega.
    Qed.

    Lemma lift_nextblock_le:
      ∀ m0 n,
        (Mem.nextblock m0 ≤ n)%positive →
        Mem.nextblock
          (mem_lift_nextblock m0 (Pos.to_nat (n) - Pos.to_nat (Mem.nextblock m0))) = n.
    Proof.
      intros.
      exploit (mem_lift_nextblock_target_eq (Pos.to_nat n - Pos.to_nat (Mem.nextblock m0)) m0); eauto.
      intros Heq.
      rewrite le_plus_minus_r in Heq.
      eapply Pos2Nat.inj; eauto.
      eapply Pos2Nat.inj_le; eauto.
    Qed.

    Lemma mem_disjoint_union_lift_nextblock_left:
      ∀ m m0 m´ nb,
        mem_disjoint_union m m0 m´ →
        (Mem.nextblock m0 ≤ Mem.nextblock m) % positive →
        mem_disjoint_union (mem_lift_nextblock m nb) m0
                           (mem_lift_nextblock m´ nb).
    Proof.
      intros. apply mem_disjoint_union_commutativity.
      apply mem_disjoint_union_lift_nextblock_right; auto.
      apply mem_disjoint_union_commutativity.
      trivial.
    Qed.

    Lemma mem_disjoint_union_lift_nextblock_left´:
      ∀ m m0 m´ nb nb´,
        mem_disjoint_union m0 m m´ →
        (Mem.nextblock m0 ≤ Mem.nextblock m) % positive →
        nb´ = (nb - (Pos.to_nat (Mem.nextblock m) - Pos.to_nat(Mem.nextblock m0))) % nat →
        mem_disjoint_union (mem_lift_nextblock m0 nb) m (mem_lift_nextblock m´ nb´).
    Proof.
      intros. apply mem_disjoint_union_commutativity.
      apply mem_disjoint_union_lift_nextblock_right´; auto.
      apply mem_disjoint_union_commutativity.
      trivial.
    Qed.

    Lemma mem_disjoint_union_nextblock_eq:
        ∀ m m´ m0,
          mem_disjoint_union m m0 m´ →
          (Mem.nextblock m0 ≤ Mem.nextblock m) % positive →
          Mem.nextblock m´ = Mem.nextblock m.
    Proof.
      intros. erewrite mem_disjoint_union_nextblock_max; eauto.
      rewrite Pos.max_l; trivial.
    Qed.

  End WITHALGEMEM.

End WITHMEM.