Module MoreSeparation

From compcert Require Import common.Separation.
From compcert Require Import common.Values.
From compcert Require common.Errors.
From compcert Require Import cfrontend.Ctypes.
From compcert Require Import lib.Maps.
From compcert Require Import lib.Coqlib.
From compcert Require Import lib.Integers.

From Velus Require Import Common.
From Velus Require Import VelusMemory.
From Velus Require Import Common.CompCertLib.

From Coq Require Import List.
From Coq Require Import ZArith.BinInt.

From Coq Require Import Program.Tactics.
From Coq Require Sorting.Permutation.

Open Scope list.
Open Scope sep_scope.
Open Scope Z.

Notation "m -*> m'" := (massert_imp m m') (at level 70, no associativity) : sep_scope.
Notation "m <-*-> m'" := (massert_eqv m m') (at level 70, no associativity) : sep_scope.

Lemma sepconj_eqv:
  forall P P' Q Q',
    P <-*-> P' ->
    Q <-*-> Q' ->
    (P ** Q) <-*-> (P' ** Q').

Lemma pure_imp:
  forall P Q,
    (pure P -*> pure Q) <-> (P -> Q).

Lemma pure_eqv:
  forall P Q,
    (pure P <-*-> pure Q) <-> (P <-> Q).

Lemma disjoint_footprint_sepconj:
  forall P Q R,
    disjoint_footprint R (P ** Q) <-> disjoint_footprint R P /\ disjoint_footprint R Q.


From compcert Require Import common.Memory.
From Coq Require Import Morphisms.

Definition wand_footprint (P Q: massert) (b: block) (ofs: Z) : Prop :=
  ~m_footprint P b ofs /\ m_footprint Q b ofs.

Program Definition sepwand (P Q: massert) : massert := {|
  m_pred := fun m =>
              (forall m', Mem.unchanged_on (wand_footprint P Q) m m' ->
                          m' |= P -> m' |= Q)
              /\ (forall b ofs, wand_footprint P Q b ofs -> Mem.valid_block m b);
  m_footprint := wand_footprint P Q
|}.

Infix "-*" := sepwand (at level 65, right associativity) : sep_scope.

Definition decidable_footprint (P: massert) : Prop :=
  forall b ofs, Decidable.decidable (m_footprint P b ofs).

Instance decidable_footprint_Proper:
  Proper (massert_eqv ==> iff) decidable_footprint.

Lemma decidable_footprint_sepconj:
  forall P Q,
    decidable_footprint P ->
    decidable_footprint Q ->
    decidable_footprint (P ** Q).

Hint Resolve decidable_footprint_sepconj.

Lemma decidable_ident_eq:
  forall (b b': AST.ident), Decidable.decidable (b = b').

Lemma decidable_footprint_range:
  forall {f} b lo hi,
    decidable_footprint (range' f b lo hi).

Hint Resolve decidable_footprint_range.

Lemma decidable_footprint_contains:
  forall {f} chunk b ofs spec,
    decidable_footprint (contains' f chunk b ofs spec).

Hint Resolve decidable_footprint_contains.

Lemma sep_unwand:
  forall P Q,
    decidable_footprint P ->
    (P ** (P -* Q)) -*> Q.

Lemma disjoint_sepwand:
  forall P Q, disjoint_footprint P (P -* Q).

Lemma merge_disjoint:
  forall P Q R m,
    disjoint_footprint P Q ->
    m |= P ** R ->
    m |= Q ** R ->
    m |= P ** Q ** R.

Lemma merge_sepwand:
  forall P Q R m,
    m |= P ** R ->
    m |= (P -* Q) ** R ->
    m |= P ** (P -* Q) ** R.

Lemma sepwand_mp:
  forall m P Q,
    m |= P ->
    m |= P -* Q ->
    m |= Q.

Instance wand_footprint_massert_imp_Proper:
  Proper (massert_imp ==> massert_imp --> eq ==> eq ==> Basics.impl)
         wand_footprint.

Instance wand_footprint_massert_eqv_Proper:
  Proper (massert_eqv ==> massert_eqv ==> eq ==> eq ==> iff) wand_footprint.

Instance sepwand_massert_Proper:
  Proper (massert_eqv ==> massert_eqv ==> massert_eqv) sepwand.

Lemma hide_in_sepwand:
  forall P Q R,
    decidable_footprint Q ->
    P <-*-> (Q ** R) ->
    P <-*-> (Q ** (Q -* P)).

Lemma sepwand_out:
  forall P Q,
    decidable_footprint P ->
    (P ** Q) <-*-> (P ** (P -* (P ** Q))).

Lemma pure_wand_footprint:
  forall (P: Prop) Q b ofs,
    wand_footprint (pure P) Q b ofs <-> m_footprint Q b ofs.

Lemma unchanged_on_imp:
  forall P (Q: block -> Z -> Prop) m m',
    Mem.unchanged_on P m m' ->
    (forall b ofs, Q b ofs -> P b ofs) ->
    Mem.unchanged_on Q m m'.

Lemma pure_sepwand:
  forall (P: Prop) Q,
    P -> (pure P -* Q) <-*-> Q.


Lemma reynolds1:
  forall P1 P2 P3,
    (P1 ** P2) -*> P3 ->
    (forall b ofs, m_footprint P1 b ofs -> wand_footprint P2 P3 b ofs) ->
    P1 -*> (P2 -* P3).

Lemma reynolds2:
  forall P1 P2 P3,
    decidable_footprint P2 ->
    P1 -*> (P2 -* P3) ->
    (P1 ** P2) -*> P3.

Definition footprint_perm' (p: permission) (P: massert) (b: block) (lo hi: Z) : Prop :=
  (forall m, m |= P ->
             (forall i k, m_footprint P b i ->
                          lo <= i < hi ->
                          Mem.perm m b i k p)).

Notation footprint_perm := (footprint_perm' Freeable).
Notation footprint_perm_w := (footprint_perm' Writable).

Lemma footprint_perm_sepconj:
  forall p P Q b lo hi,
    footprint_perm' p P b lo hi ->
    footprint_perm' p Q b lo hi ->
    footprint_perm' p (P ** Q) b lo hi.

Lemma footprint_perm_range:
  forall p b lo hi b' lo' hi',
    footprint_perm' p (range' p b lo hi) b' lo' hi'.

Lemma footprint_perm_contains:
  forall p chunk b ofs spec b' lo hi,
    footprint_perm' p (contains' p chunk b ofs spec) b' lo hi.

Hint Resolve footprint_perm_sepconj
             footprint_perm_range
             footprint_perm_contains.

Lemma range_imp_with_wand:
  forall p P b lo hi,
    (range' p b lo hi) -*> P ->
    decidable_footprint P ->
    footprint_perm' p P b lo hi ->
    (range' p b lo hi) <-*-> (P ** (P -* range' p b lo hi)).

Definition subseteq_footprint (P Q: massert) :=
  (forall b ofs, m_footprint P b ofs -> m_footprint Q b ofs).

Instance subseteq_footprint_footprint_Proper:
  Proper (subseteq_footprint ==> eq ==> eq ==> Basics.impl) m_footprint.

Lemma subseteq_footprint_refl:
  forall P, subseteq_footprint P P.

Lemma subseteq_footprint_trans:
  forall P Q R, subseteq_footprint P Q ->
                subseteq_footprint Q R ->
                subseteq_footprint P R.

Add Parametric Relation: massert subseteq_footprint
    reflexivity proved by subseteq_footprint_refl
    transitivity proved by subseteq_footprint_trans
      as subseteq_footprint_rel.

Instance subseteq_footprint_massert_imp_Proper:
  Proper (massert_imp ==> massert_imp --> Basics.impl) subseteq_footprint.

Instance subseteq_footprint_massert_eqv_Proper:
  Proper (massert_eqv ==> massert_eqv ==> iff) subseteq_footprint.

Lemma subseteq_footprint_sepconj:
  forall P Q R S,
    subseteq_footprint P Q ->
    subseteq_footprint R S ->
    subseteq_footprint (P ** R) (Q ** S).

Lemma unify_distinct_wands:
  forall P Q R S,
    disjoint_footprint R S ->
    subseteq_footprint P R ->
    subseteq_footprint Q S ->
    (P -* R) ** (Q -* S)
    -*> (P ** Q) -* (R ** S).


Program Definition sepemp: massert := pure True.

Lemma sepemp_disjoint:
  forall P, disjoint_footprint P sepemp.

Lemma sepemp_trivial:
  forall m, m |= sepemp.
Hint Resolve sepemp_trivial.

Lemma sepemp_right:
  forall P,
    P <-*-> (P ** sepemp).

Lemma sepemp_left:
  forall P,
    P <-*-> (sepemp ** P).

Lemma wandwand_sepemp:
  forall P, massert_eqv (P -* P) sepemp.

Lemma wand_footprint_sepemp:
  forall P b ofs,
    wand_footprint sepemp P b ofs <-> m_footprint P b ofs.

Lemma sepemp_wand:
  forall P,
    sepemp -* P <-*-> P.

Lemma decidable_footprint_sepemp:
  decidable_footprint sepemp.

Lemma footprint_perm_sepemp:
  forall p b lo hi, footprint_perm' p sepemp b lo hi.

Hint Resolve decidable_footprint_sepemp footprint_perm_sepemp.

Lemma empty_range:
  forall {f} b lo hi,
    hi <= lo ->
    0 <= lo ->
    hi <= Ptrofs.modulus ->
    sepemp <-*-> (range' f b lo hi).

Definition sepfalse := pure False.

Lemma decidable_footprint_sepfalse:
  decidable_footprint sepfalse.

Lemma footprint_perm_sepfalse:
  forall p b lo hi, footprint_perm' p sepfalse b lo hi.

Hint Resolve decidable_footprint_sepfalse footprint_perm_sepfalse.

Section MassertPredEqv.
  Context {A: Type}.

  Definition massert_pred_eqv (P: A -> massert) (Q: A -> massert) : Prop :=
    forall x, massert_eqv (P x) (Q x).

  Lemma massert_pred_eqv_refl:
    forall P, massert_pred_eqv P P.

  Lemma massert_pred_eqv_sym:
    forall P Q, massert_pred_eqv P Q -> massert_pred_eqv Q P.

  Lemma massert_pred_eqv_trans:
    forall P Q R,
      massert_pred_eqv P Q ->
      massert_pred_eqv Q R ->
      massert_pred_eqv P R.

  Lemma massert_pred_eqv_inst:
    forall P Q x,
      massert_pred_eqv P Q ->
      massert_eqv (P x) (Q x).

End MassertPredEqv.

Add Parametric Relation (A: Type) : (A -> massert) massert_pred_eqv
    reflexivity proved by massert_pred_eqv_refl
    symmetry proved by massert_pred_eqv_sym
    transitivity proved by massert_pred_eqv_trans
as massert_pred_eqv_prel.

Section Sepall.
  Context {A: Type}.

  Definition sepall (p: A -> massert): list A -> massert :=
    fold_right (fun x => sepconj (p x)) sepemp.

  Lemma sepall_permutation:
    forall p xs ys,
      Permutation.Permutation xs ys ->
      (sepall p xs) <-*-> (sepall p ys).

  Lemma sepall_app:
    forall p xs ys,
      sepall p (xs ++ ys) <-*-> sepall p xs ** sepall p ys.

  Lemma sepall_cons:
    forall p x xs,
      sepall p (x::xs) <-*-> p x ** sepall p xs.

  Lemma sepall_breakout:
    forall ys ws x xs p,
      ys = ws ++ x :: xs ->
      sepall p ys <-*-> p x ** sepall p (ws ++ xs).

  Lemma sepall_in:
    forall x ys,
      In x ys ->
      exists ws xs,
        ys = ws ++ x :: xs
        /\ (forall p,
              sepall p ys <-*-> p x ** sepall p (ws ++ xs)).

  Lemma sepall_wandout:
    forall p x xs,
      decidable_footprint (p x) ->
      In x xs ->
      (sepall p xs) <-*-> (p x ** (p x -* sepall p xs)).

  Lemma sepall_sepfalse:
    forall m p xs,
      m |= sepall p xs ->
      (forall x, In x xs -> p x <> sepfalse).

  Lemma sepall_weakenp:
    forall P P' xs,
      (forall x, In x xs -> (P x) -*> (P' x)) ->
      (sepall P xs) -*> (sepall P' xs).

  Lemma sepall_swapp:
    forall P P' xs,
      (forall x, In x xs -> P x <-*-> P' x) ->
      sepall P xs <-*-> sepall P' xs.

  Lemma decidable_footprint_sepall:
    forall P xs,
      (forall x, decidable_footprint (P x)) ->
      decidable_footprint (sepall P xs).

  Lemma footprint_perm_sepall:
    forall p P xs b lo hi,
      (forall x b lo hi, footprint_perm' p (P x) b lo hi) ->
      footprint_perm' p (sepall P xs) b lo hi.

  Hint Resolve decidable_footprint_sepall footprint_perm_sepall.

  Lemma sepall_unwand:
  forall xs P Q,
    (forall x, decidable_footprint (P x)) ->
    (sepall P xs ** sepall (fun x => P x -* Q x) xs) -*> sepall Q xs.

  Lemma subseteq_footprint_sepall:
    forall p q xs,
      (forall x, In x xs -> subseteq_footprint (p x) (q x)) ->
      subseteq_footprint (sepall p xs) (sepall q xs).

  Lemma sepall_outwand_cons:
    forall p q x xs,
      (forall x, decidable_footprint (p x)) ->
      (forall x, subseteq_footprint (p x) (q x)) ->
      (p x ** (p x -* q x)) ** sepall p xs ** (sepall p xs -* sepall q xs)
      -*> sepall p (x::xs) ** (sepall p (x::xs) -* sepall q (x::xs)).

End Sepall.

Hint Resolve decidable_footprint_sepall footprint_perm_sepall.

Instance sepall_massert_pred_eqv_permutation_eqv_Proper A:
  Proper (massert_pred_eqv ==> @Permutation.Permutation A ==> massert_eqv)
         sepall.


Section SplitRange.
  Variable env: composite_env.
  Variable id: ident.
  Variable co: composite.

  Hypothesis Henv: Ctypes.composite_env_consistent env.
  Hypothesis Hco: env!id = Some co.
  Hypothesis Hstruct: co_su co = Struct.

  Definition field_range' (p: permission) (flds: list (AST.ident * type))
             (b: block) (lo: Z) (fld: AST.ident * type) : massert :=
    let (id, ty) := fld in
    match field_offset env id flds with
      | Errors.OK ofs => range' p b (lo + ofs) (lo + ofs + sizeof env ty)
      | Errors.Error _ => sepfalse
    end.

  Lemma decidable_footprint_field_range:
    forall p lo b flds,
      decidable_footprint (sepall (field_range' p flds b lo) flds).

  Lemma footprint_perm_field_range:
    forall p flds b pos x b' lo hi,
      footprint_perm' p (field_range' p flds b pos x) b' lo hi.

  Lemma split_range_fields':
    forall p b lo flds,
      NoDupMembers flds ->
      massert_imp (range' p b lo (lo + sizeof_struct env 0 flds))
                  (sepall (field_range' p flds b lo) flds).

  Lemma split_range_fields:
    forall p b lo,
      NoDupMembers (co_members co) ->
      massert_imp (range' p b lo (lo + co_sizeof co))
                  (sepall (field_range' p (co_members co) b lo) (co_members co)).

End SplitRange.

Notation field_range ge := (field_range' ge Freeable).
Notation field_range_w ge := (field_range' ge Writable).


Import Globalenvs.
Import AST.
Import Clight.

Section Galloc.

  Variable p : program .

  Definition grange (idg : ident * globdef fundef type) :=
    let (id, g) := idg in
    match Genv.find_symbol (Genv.globalenv p) id with
    | None => sepfalse
    | Some b =>
      match g with
      | Gfun f => range' Nonempty b 0 1
      | Gvar v =>
        pure (init_data_list_size (gvar_init v) <= Ptrofs.modulus)
             -* range' (Genv.perm_globvar v) b 0
                       (init_data_list_size v.(gvar_init))
      end
    end.

  Lemma init_grange:
    forall m0,
      NoDupMembers p.(prog_defs) ->
      Genv.init_mem p = Some m0 ->
      m0 |= sepall grange p.(prog_defs).

End Galloc.

Lemma sep_swap56:
  forall P Q R S T U V, (P ** Q ** R ** S ** T ** U ** V) <-*-> (P ** Q ** R ** S ** U ** T ** V).

Lemma sep_swap67:
  forall P Q R S T U V W, (P ** Q ** R ** S ** T ** U ** V ** W) <-*-> (P ** Q ** R ** S ** T ** V ** U ** W).

Lemma sep_swap78:
  forall P Q R S T U V W X, (P ** Q ** R ** S ** T ** U ** V ** W ** X) <-*-> (P ** Q ** R ** S ** T ** U ** W ** V ** X).