Module SeparationC

Require Import Setoid Program.Basics.
Require Import CoqlibC Decidableplus.
Require Import AST Integers Values MemoryC Events Globalenvs.
newly added *
Require Import AxiomsC.
Require Export Separation.
Require Import JunkBlock.

Local Open Scope sep_scope.


Ltac sep_split := econs; [|split]; swap 2 3.

Global Program Instance disjoint_footprint_sym: Symmetric disjoint_footprint.
Next Obligation.
ii. eapply H; eauto. Qed.


Lemma separation_private
      m_src m_tgt F P
      (MATCH: m_tgt |= P ** minjection F m_src)
  :
     P.(m_footprint) <2= loc_out_of_reach F m_src.
Proof.
  inv MATCH. des; ss.
  ii. unfold disjoint_footprint in *. ss.
  eapply H1; eauto.
Qed.

Lemma disjoint_footprint_drop_empty
      P Q0 Q1
      (EMPTY: Q0.(m_footprint) <2= bot2)
      (DISJ: disjoint_footprint P Q1)
  :
    <<DISJ: disjoint_footprint P (Q0 ** Q1)>>.
Proof.
  ii. ss. unfold disjoint_footprint in *. des; eauto.
  eapply EMPTY; eauto.
Qed.


Lemma disjoint_footprint_mconj
      P Q0 Q1
  :
    <<DISJ: disjoint_footprint P (mconj Q0 Q1)>>
    <-> <<DISJ0: disjoint_footprint P Q0>> /\ <<DISJ1: disjoint_footprint P Q1>>.
Proof.
  split; ii; ss; unfold disjoint_footprint in *; des; eauto.
  esplits; ii; ss; eauto.
Qed.

Lemma disjoint_footprint_sepconj
      P Q0 Q1
  :
    (<<DISJ0: disjoint_footprint P Q0>>) /\ (<<DISJ1: disjoint_footprint P Q1>>)
    <-> (<<DISJ: disjoint_footprint P (Q0 ** Q1)>>).
Proof.
  unfold disjoint_footprint in *.
  split; esplits; ii; ss; des; eauto.
Qed.


Lemma massert_eq
      pred0 footprint0 INVAR0 VALID0
      pred1 footprint1 INVAR1 VALID1
      (EQ0: pred0 = pred1)
      (EQ1: footprint0 = footprint1)
  :
    Build_massert pred0 footprint0 INVAR0 VALID0 = Build_massert pred1 footprint1 INVAR1 VALID1.
Proof.
  clarify.
  f_equal.
  apply Axioms.proof_irr.
  apply Axioms.proof_irr.
Qed.

Lemma mconj_sym
      P Q
  :
    <<EQ: (mconj P Q) = (mconj Q P)>>.
Proof.
  apply massert_eq; ss.
  - apply Axioms.functional_extensionality. ii; ss.
    apply prop_ext.
    split; i; des; split; ss.
  - apply Axioms.functional_extensionality. ii; ss.
    apply Axioms.functional_extensionality. ii; ss.
    apply prop_ext.
    split; i; des; eauto.
Qed.

Lemma sepconj_sym
      P Q
  :
    <<EQ: (sepconj P Q) = (sepconj Q P)>>.
Proof.
  apply massert_eq; ss.
  - apply Axioms.functional_extensionality. ii; ss.
    apply prop_ext.
    split; i; des; esplits; ss.
    + sym; ss.
    + sym; ss.
  - apply Axioms.functional_extensionality. ii; ss.
    apply Axioms.functional_extensionality. ii; ss.
    apply prop_ext.
    split; i; des; eauto.
Qed.

Local Transparent sepconj.

Lemma sep_drop_tail3
      P Q R
  :
    massert_imp (P ** Q ** R) (P ** Q).
Proof.
  unfold massert_imp. ss. split; ii; eauto.
  - des; esplits; eauto. apply disjoint_footprint_sepconj in H1. des; ss.
  - ss. des; eauto.
Qed.

Lemma sepconj_isolated_mutation0
      m0 m1 P Q
      (SEP: m0 |= P ** Q)
      (UNCH: Mem.unchanged_on (fun blk ofs => ~ P.(m_footprint) blk ofs /\ Mem.valid_block m0 blk) m0 m1)
  :
    <<SEP: m1 |= Q>>.
Proof.
  destruct SEP as (A & B & C).
  eapply m_invar; eauto.
  eapply Mem.unchanged_on_implies; eauto. ii. ss. esplits; eauto.
Qed.

Lemma sepconj_isolated_mutation1
      m0 m1 P Q
      (SEP: m0 |= P ** Q)
      (UNCH: Mem.unchanged_on (~2 P.(m_footprint)) m0 m1)
  :
    <<SEP: m1 |= Q>>.
Proof.
  eapply sepconj_isolated_mutation0; eauto.
  eapply Mem.unchanged_on_implies; eauto. ii. des; ss.
Qed.

Lemma sepconj_isolated_mutation_strong
      m0 m1 P0 P1 Q
      (SEP: m0 |= P0)
      (UNCH: Mem.unchanged_on Q m0 m1)
      (IMP: massert_imp P0 P1)
      (FOOT: P1.(m_footprint) <2= Q)
  :
    <<SEP: m1 |= P1>>.
Proof.
  hnf in IMP. des.
  eapply m_invar; eauto.
  eapply Mem.unchanged_on_implies; eauto.
Qed.

Lemma sepconj_isolated_mutation_stronger
      m0 m1 P0 P1 CTX CHNG
      (SEP: m0 |= P0 ** CTX)
      (UNCH: Mem.unchanged_on (~2 CHNG) m0 m1)
      (IMP: massert_imp P0 P1)
      (ISOL0: CHNG <2= P0.(m_footprint))
      (ISOL1: P1.(m_footprint) <2= ~2 CHNG)
  :
    <<SEP: m1 |= P1 ** CTX>>.
Proof.
  destruct SEP as (A & B & C).
  hnf in IMP. des.
  sep_split; eauto.
  - eapply m_invar; eauto.
    eapply Mem.unchanged_on_implies; eauto.
    ii. eapply ISOL1; eauto.
  - ii. eapply C; eauto.
  - eapply m_invar; eauto.
    eapply Mem.unchanged_on_implies; eauto.
    ii. apply ISOL0 in H1. eauto.
Qed.

Lemma globalenv_inject_incr_strong
      j j' m_src m_tgt0 m_tgt1 F V (ge: Genv.t F V)
      (INCR: inject_incr j j')
      (INJ: inject_separated j j' m_src m_tgt0)
      (SEP: m_tgt0 |= globalenv_inject ge j)
      (MLE: (m_tgt0.(Mem.nextblock) <= m_tgt1.(Mem.nextblock))%positive)
  :
    <<SEP: m_tgt1 |= globalenv_inject ge j'>>.
Proof.
  assert(m_tgt0 |= globalenv_inject ge j').
  { ss. des. esplits; eauto. inv SEP0. econs; eauto. ii. eapply IMAGE; eauto.
    rr in INJ. destruct (j b1) eqn:T.
    - destruct p; ss. exploit INCR; eauto. i; clarify.
    - exploit INJ; eauto. i; des. exfalso.
      eapply H2. r. eapply Plt_Ple_trans; eauto.
  }
  eapply m_invar; eauto.
  ss.
Qed.

Lemma disjoint_footprint_sep
      A WALL B
      (DISJ0: A.(m_footprint) <2= WALL)
      (DISJ1: B.(m_footprint) <2= ~2 WALL)
  :
    <<DISJ: disjoint_footprint A B>>.
Proof.
  ii. apply DISJ0 in H. apply DISJ1 in H0. ss.
Qed.

Program Definition freed_range (b: block) (lo hi: Z): massert := {|
  m_pred := fun m =>
              <<RANGE: 0 <= lo /\ hi <= Ptrofs.modulus>> /\ <<VALID: lo < hi -> m.(Mem.valid_block) b>>
  ;
  m_footprint := brange b lo hi
  ;
|}.
Next Obligation.
des. esplits; eauto. i. eapply Mem.valid_block_unchanged_on; eauto. Qed.
Next Obligation.
hnf in H0. des; clarify. eapply H1. lia. Qed.

Hint Unfold freed_range.

Lemma add_pure_r
      m P
  :
    <<SEP: m |= P>> <-> <<SEP: m |= P ** pure True>>.
Proof.
split; ii. - sep_split; ss. - destruct H. ss. Qed.

Lemma range_split0
      b lo mid hi
      (RANEG: lo <= mid <= hi)
  :
    massert_imp (range b lo hi) (range b lo mid ** range b mid hi).
Proof.
  econs; ii.
  - apply add_pure_r. apply add_pure_r in H. r. rewrite sep_assoc. eapply range_split; eauto.
  - ss. des; esplits; eauto; try lia.
Qed.

Lemma range_freed_range
      sp lo hi
  :
    massert_imp (range sp lo hi) (freed_range sp lo hi).
Proof.
  econs; ii; ss.
  des; esplits; eauto. i. specialize (H1 lo).
  exploit H1; eauto with mem lia.
Unshelve.
  all: econs.
Qed.

Lemma add_pure_r_eq
      P
  :
    P = P ** pure True.
Proof.
  destruct P; ss. unfold sepconj. ss.
  eapply massert_eq.
  - apply functional_extensionality. ii; ss.
    apply prop_ext. split; ii; des; esplits; ss.
  - repeat (apply functional_extensionality; ii; ss).
    apply prop_ext. split; ii; des; ss; eauto.
Qed.

Lemma mconj_distr
      m P Q CTX
  :
    <<SEP: m |= (mconj P Q) ** CTX>> <-> <<SEP: m |= P ** CTX>> /\ <<SEP: m |= Q ** CTX>>.
Proof.
  split; ii.
  - destruct H as (A & B & C). ss. des. sym in C. apply disjoint_footprint_mconj in C. des.
    esplits; eauto.
    + sym; ss.
    + sym; ss.
  - des. destruct SEP. destruct SEP0. des.
    sep_split; ss.
    sym. apply disjoint_footprint_mconj. esplits; eauto.
    + sym; ss.
    + sym; ss.
Qed.

Lemma range_nonnil_valid_block
      m b lo hi
      (SEP: m |= range b lo hi)
      (RANGE: lo < hi)
  :
    <<VALID: m.(Mem.valid_block) b>>.
Proof.
  ss. des. specialize (SEP1 lo). exploit SEP1; eauto. { lia. } i. eapply Mem.perm_valid_block; eauto.
Unshelve.
  all: econs.
Qed.

Lemma sepconj_isolated_mutation_strongest
      m0 m1 P P0 P1 CTX CHNG
      (SEP: m0 |= P ** CTX)
      (UNCH: Mem.unchanged_on (~2 CHNG) m0 m1)
      (IMP: massert_imp P P1)
      (PRED: m1 |= P0)
      (ISOL: CHNG <2= P.(m_footprint))
      (ISOL0: P0.(m_footprint) <2= CHNG)
      (ISOL1: P1.(m_footprint) <2= ~2 CHNG)
      (DISJ: disjoint_footprint P0 P1)
  :
    <<SEP: m1 |= P0 ** P1 ** CTX>>.
Proof.
  destruct SEP as (A & B & C).
  hnf in IMP. des.
  sep_split; eauto.
  { apply disjoint_footprint_sepconj. split; ss. ii. eapply C; eauto. }
  sep_split.
  - eapply m_invar; eauto.
    eapply Mem.unchanged_on_implies; eauto.
    ii. eapply ISOL1; eauto.
  - ii. eapply C; eauto.
  - eapply m_invar; eauto.
    eapply Mem.unchanged_on_implies; eauto.
    ii. apply ISOL in H1. eauto.
Qed.

Lemma sepconj_isolated_mutation_revisited
      m0 m1 P0 P1 CTX CHNG
      (SEP: m0 |= P0 ** CTX)
      (UNCH: Mem.unchanged_on (~2 CHNG) m0 m1)
      (ISOL: CHNG <2= P0.(m_footprint))
      (PRED: m1 |= P1)
      (FOOT: P1.(m_footprint) <2= P0.(m_footprint))
  :
    <<SEP: m1 |= P1 ** CTX>>.
Proof.
  destruct SEP as (A & B & C).
  sep_split; eauto.
  { ii. et. }
  eapply m_invar; et.
  eapply Mem.unchanged_on_implies; eauto.
  ii. eapply ISOL in H1. rr in C. et.
Qed.

Lemma mconj_footprint_le
      A0 B0 A1 B1
      (LEA: A0.(m_footprint) <2= A1.(m_footprint))
      (LEB: B0.(m_footprint) <2= B1.(m_footprint))
  :
    (mconj A0 B0).(m_footprint) <2= (mconj A1 B1).(m_footprint).
Proof.
  ss. ii. des; et.
Qed.

Lemma sepconj_footprint_le
      A0 B0 A1 B1
      (LEA: A0.(m_footprint) <2= A1.(m_footprint))
      (LEB: B0.(m_footprint) <2= B1.(m_footprint))
  :
    (sepconj A0 B0).(m_footprint) <2= (sepconj A1 B1).(m_footprint).
Proof.
Local Transparent sepconj.
  ss. ii. des; et.
Local Opaque sepconj.
Qed.

Local Transparent sepconj.
Lemma m_footprint_sepconj_le
      P0 Q0 P1 Q1
      (LEP: P0.(m_footprint) <2= P1.(m_footprint))
      (LEQ: Q0.(m_footprint) <2= Q1.(m_footprint))
  :
    <<LE: (P0 ** Q0).(m_footprint) <2= (P1 ** Q1).(m_footprint)>>.
Proof.
ii; ss. des; ss; eauto. Qed.

Lemma sep_assoc_footprint
      P Q R
  :
    ((P ** Q) ** R).(m_footprint) =
    (P ** Q ** R).(m_footprint).
Proof.
  ss.
  apply func_ext2. ii; ss. apply prop_ext.
  split; ii; ss; des; et.
Qed.

Lemma unfree_freed_range
      sp m0 m1 lo mid hi
      (SEP: m0 |= freed_range sp lo mid ** range sp mid hi)
      (UNFREE: Mem_unfree m0 sp lo mid = Some m1):
    <<SEP: m1 |= range sp lo hi>>.
Proof.
  ss. des. esplits; et. ii.
  hexploit Mem_unfree_unchanged_on; et. intro UNCH; des.
  destruct (classic (i < mid)).
  - eapply Mem_unfree_perm; et.
  - eapply Mem.perm_unchanged_on; et.
    + u. ii. des. xomega.
    + eapply SEP3; et. xomega.
Qed.

Local Opaque sepconj.

Lemma assign_junk_blocks_rule
      P m_src0
      (PRED: m_src0 |= P)
      n
  :
    (assign_junk_blocks m_src0 n) |= P.
Proof.
  destruct P; ss.
  eapply m_invar; eauto.
  eapply Mem.unchanged_on_implies.
  { eapply assign_junk_blocks_unchanged_on; eauto. }
  ss.
Qed.