Require Import Coqlib Maps Integers Values Memdata.
Require Import Blockset Memory Injections InjRels.

Import Mem.

Memory Closures

Local Notation "a # b" := (PMap.get b a) (at level 1).

Inductive reach' (m: mem) (B: Bset.t) : list (block * ptrofs) -> block -> Prop :=
| reach_nil: forall b, Bset.belongsto B b -> reach' m B nil b
| reach_cons: forall b L b' z ofs q n,
    reach' m B L b' ->
    perm m b' z Max Readable ->
    ZMap.get z (mem_contents m)!!b' = Fragment (Vptr b ofs) q n->
    reach' m B ((b',ofs)::L) b.

Inductive reachable : mem -> Bset.t -> block -> Prop :=
  Reachable : forall m bs b L,
    reach' m bs L b -> reachable m bs b.

Record reach_closed (m: mem) (B: Bset.t) : Prop :=
  {
    reachable_closure: forall b, reachable m B b -> Bset.belongsto B b;
    no_undef: forall b z,
        Bset.belongsto B b ->
        perm m b z Max Readable ->
        (~ ZMap.get z (mem_contents m) !! b = Undef);
    no_vundef: forall b z q n,
        Bset.belongsto B b ->
        perm m b z Max Readable ->
        (~ ZMap.get z (mem_contents m) !! b = Fragment Vundef q n);
  }.

Lemma reach_closed_belongsto:
  forall m B b,
    reach_closed m B ->
    reachable m B b ->
    Bset.belongsto B b.

Lemma bset_eq_reach'_local:
  forall bs1 bs2,
    (forall b, bs1 b <-> bs2 b) ->
    forall m L b, reach' m bs1 L b <-> reach' m bs2 L b.

Lemma bset_eq_reachable_local:
  forall bs1 bs2 m,
    (forall b, bs1 b <-> bs2 b) ->
    (forall b, reachable m bs1 b <-> reachable m bs2 b).


Lemma bset_eq_reach_closed_local:
  forall bs1 bs2 m,
    (forall b, bs1 b <-> bs2 b) ->
    reach_closed m bs1 <-> reach_closed m bs2.

Lemma sep_inject_rc_inject:
  forall mu j m m',
    Bset.inject (inj mu) (SharedSrc mu) (SharedTgt mu) ->
    inject_incr (Bset.inj_to_meminj (inj mu)) j ->
    sep_inject (Bset.inj_to_meminj (inj mu)) j ->
    inject j m m' ->
    reach_closed m (SharedSrc mu) ->
    inject (Bset.inj_to_meminj (inj mu)) m m'.

Lemma sep_inject_rely_inject:
  forall mu j m1 m1' m2 m2',
    Bset.inject (inj mu) (SharedSrc mu) (SharedTgt mu) ->
    inject_incr (Bset.inj_to_meminj (inj mu)) j ->
    sep_inject (Bset.inj_to_meminj (inj mu)) j ->
    inject j m1 m1' ->
    unchanged_on (fun b _ => ~ SharedSrc mu b) m1 m2 ->
    reach_closed m2 (SharedSrc mu) ->
    unchanged_on (fun b _ => ~ SharedTgt mu b) m1' m2' ->
    reach_closed m2' (SharedTgt mu) ->
    inject (Bset.inj_to_meminj (inj mu)) m2 m2' ->
    inject j m2 m2'.
    
    
Lemma unchanged_on_reach_closed:
  forall m B m',
    reach_closed m B ->
    Mem.unchanged_on (fun b _ => B b) m m' ->
    (forall b, Bset.belongsto B b -> Mem.valid_block m b) ->
    reach_closed m' B.

Lemma unchanged_on_reach_closed_inverse:
  forall m B m',
    reach_closed m' B ->
    Mem.unchanged_on (fun b _ => B b) m m' ->
    (forall b, Bset.belongsto B b -> Mem.valid_block m b) ->
    reach_closed m B.

Record unmapped_closed (mu: Mu) (m m': mem) : Prop :=
  {
    unmapped_closure:
      forall b' z b0 ofs0 q n,
        Bset.belongsto (SharedTgt mu) b' ->
        (forall b, (inj mu) b = Some b' -> ~ perm m b z Max Readable) ->
        perm m' b' z Max Readable ->
        ZMap.get z (mem_contents m') !! b' = Fragment (Vptr b0 ofs0) q n ->
        Bset.belongsto (SharedTgt mu) b0;
    unmapped_no_undef:
      forall b' z,
        Bset.belongsto (SharedTgt mu) b' ->
        (forall b, (inj mu) b = Some b' -> ~ perm m b z Max Readable) ->
        perm m' b' z Max Readable ->
        ZMap.get z (mem_contents m') !! b' <> Undef;
    unmapped_no_vundef:
      forall b' z q n,
        Bset.belongsto (SharedTgt mu) b' ->
        (forall b, (inj mu) b = Some b' -> ~ perm m b z Max Readable) ->
        perm m' b' z Max Readable ->
        ZMap.get z (mem_contents m') !! b' <> Fragment Vundef q n;
  }.

Lemma reach_closed_unmapped_closed:
  forall mu m m',
    reach_closed m' (SharedTgt mu) ->
    unmapped_closed mu m m'.

Lemma inject_shared_src_valid:
  forall mu j m m',
    Bset.inject (inj mu) (SharedSrc mu) (SharedTgt mu) ->
    inject_incr (Bset.inj_to_meminj (inj mu)) j ->
    inject j m m' ->
    (forall b, Bset.belongsto (SharedSrc mu) b -> Mem.valid_block m b).
  
Lemma inject_shared_tgt_valid:
  forall mu j m m',
    Bset.inject (inj mu) (SharedSrc mu) (SharedTgt mu) ->
    inject_incr (Bset.inj_to_meminj (inj mu)) j ->
    inject j m m' ->
    (forall b, Bset.belongsto (SharedTgt mu) b -> Mem.valid_block m' b).


Lemma unmapped_closed_reach_closed_preserved_by_extends:
  forall mu m m',
    inject_incr (Bset.inj_to_meminj (inj mu)) inject_id ->
    Bset.inject (inj mu) (SharedSrc mu) (SharedTgt mu) ->
    (forall b, Bset.belongsto (SharedSrc mu) b -> valid_block m b) ->
    (forall b, Bset.belongsto (SharedTgt mu) b -> valid_block m' b) ->
    extends m m' ->
    unmapped_closed mu m m' ->
    reach_closed m (SharedSrc mu) ->
    reach_closed m' (SharedTgt mu).


Lemma unmapped_closed_reach_closed_preserved_by_injection:
  forall mu m m',
    Bset.inject (inj mu) (SharedSrc mu) (SharedTgt mu) ->
    (forall b, Bset.belongsto (SharedSrc mu) b -> valid_block m b) ->
    (forall b, Bset.belongsto (SharedTgt mu) b -> valid_block m' b) ->
    inject (Bset.inj_to_meminj (inj mu)) m m' ->
    unmapped_closed mu m m' ->
    reach_closed m (SharedSrc mu) ->
    reach_closed m' (SharedTgt mu).

Lemma unmapped_closed_reach_closed_preserved_by_injection':
  forall mu m m',
    Bset.inject (inj mu) (SharedSrc mu) (SharedTgt mu) ->
    inject (Bset.inj_to_meminj (inj mu)) m m' ->
    unmapped_closed mu m m' ->
    reach_closed m (SharedSrc mu) ->
    reach_closed m' (SharedTgt mu).

Lemma unmapped_closed_reach_closed_preserved_by_injection'':
  forall mu j m m',
    Bset.inject (inj mu) (SharedSrc mu) (SharedTgt mu) ->
    inject_incr (Bset.inj_to_meminj (inj mu)) j ->
    sep_inject (Bset.inj_to_meminj (inj mu)) j ->
    inject j m m' ->
    unmapped_closed mu m m' ->
    reach_closed m (SharedSrc mu) ->
    reach_closed m' (SharedTgt mu).

Lemma unchanged_on_unmapped_closed_preserved:
  forall mu m1 m1' m2 m2',
    Bset.inject (inj mu) (SharedSrc mu) (SharedTgt mu) ->
    (forall b, Bset.belongsto (SharedSrc mu) b -> valid_block m1 b) ->
    (forall b, Bset.belongsto (SharedTgt mu) b -> valid_block m1' b) ->
    unmapped_closed mu m1 m1' ->
    unchanged_on (fun b _ => SharedSrc mu b) m1 m2 ->
    unchanged_on (fun b _ => SharedTgt mu b) m1' m2' ->
    unmapped_closed mu m2 m2'.
  
Lemma unchanged_on_reach_closed_preserved:
  forall mu m1 m1' m2 m2',
    (forall b, Bset.belongsto (SharedSrc mu) b -> valid_block m1 b) ->
    (forall b, Bset.belongsto (SharedTgt mu) b -> valid_block m1' b) ->
    (reach_closed m1 (SharedSrc mu) -> reach_closed m1' (SharedTgt mu)) ->
    unchanged_on (fun b _ => SharedSrc mu b) m1 m2 ->
    unchanged_on (fun b _ => SharedTgt mu b) m1' m2' ->
    (reach_closed m2 (SharedSrc mu) -> reach_closed m2' (SharedTgt mu)).

Lemma store_val_inject_unmapped_closed_preserved:
  forall mu m1 m1' chunk j b ofs v m2 b' delta v' m2',
    Bset.inject (inj mu) (SharedSrc mu) (SharedTgt mu) ->
    (forall b, Bset.belongsto (SharedSrc mu) b -> valid_block m1 b) ->
    (forall b, Bset.belongsto (SharedTgt mu) b -> valid_block m1' b) ->
    inject_incr (Bset.inj_to_meminj (inj mu)) j ->
    sep_inject (Bset.inj_to_meminj (inj mu)) j ->
    unmapped_closed mu m1 m1' ->
    store chunk m1 b ofs v = Some m2 ->
    j b = Some (b', delta) ->
    store chunk m1' b' (ofs + delta) v' = Some m2' ->
    unmapped_closed mu m2 m2'.

Lemma free_inject_unmapped_closed_preserved:
  forall mu m1 m1' j b lo hi m2 b' delta lo' hi' m2',
    Bset.inject (Injections.inj mu) (Injections.SharedSrc mu) (Injections.SharedTgt mu) ->
    (forall b0 : block, Bset.belongsto (Injections.SharedSrc mu) b0 -> Mem.valid_block m1 b0) ->
    (forall b0 : block, Bset.belongsto (Injections.SharedTgt mu) b0 -> Mem.valid_block m1' b0) ->
    inject_incr (Bset.inj_to_meminj (Injections.inj mu)) j ->
    sep_inject (Bset.inj_to_meminj (Injections.inj mu)) j ->
    unmapped_closed mu m1 m1' ->
    Mem.free m1 b lo hi = Some m2 ->
    j b = Some (b', delta) ->
    lo' <= (lo + delta) ->
    (hi + delta) <= hi' ->
    Mem.free m1' b' lo' hi' = Some m2' ->
    unmapped_closed mu m2 m2'.