invariants.v 5.09 KB
Newer Older
1 2 3 4
From algebra Require Export base.
From prelude Require Export countable co_pset.
From program_logic Require Import ownership.
From program_logic Require Export pviewshifts weakestpre.
Ralf Jung's avatar
Ralf Jung committed
5 6 7 8 9 10
Import uPred.

Local Hint Extern 100 (@eq coPset _ _) => solve_elem_of.
Local Hint Extern 100 (@subseteq coPset _ _) => solve_elem_of.
Local Hint Extern 100 (_  _) => solve_elem_of.
Local Hint Extern 99 ({[ _ ]}  _) => apply elem_of_subseteq_singleton.
Robbert Krebbers's avatar
Robbert Krebbers committed
11

12

Robbert Krebbers's avatar
Robbert Krebbers committed
13 14
Definition namespace := list positive.
Definition nnil : namespace := nil.
15 16
Definition ndot `{Countable A} (N : namespace) (x : A) : namespace :=
  encode x :: N.
Ralf Jung's avatar
Ralf Jung committed
17
Coercion nclose (N : namespace) : coPset := coPset_suffixes (encode N).
Robbert Krebbers's avatar
Robbert Krebbers committed
18

19
Instance ndot_inj `{Countable A} : Inj2 (=) (=) (=) (@ndot A _ _).
20
Proof. by intros N1 x1 N2 x2 ?; simplify_equality. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
21 22
Lemma nclose_nnil : nclose nnil = coPset_all.
Proof. by apply (sig_eq_pi _). Qed.
23
Lemma encode_nclose N : encode N  nclose N.
Robbert Krebbers's avatar
Robbert Krebbers committed
24
Proof. by apply elem_coPset_suffixes; exists xH; rewrite (left_id_L _ _). Qed.
25
Lemma nclose_subseteq `{Countable A} N x : nclose (ndot N x)  nclose N.
Robbert Krebbers's avatar
Robbert Krebbers committed
26 27
Proof.
  intros p; rewrite /nclose !elem_coPset_suffixes; intros [q ->].
28
  destruct (list_encode_suffix N (ndot N x)) as [q' ?]; [by exists [encode x]|].
29
  by exists (q ++ q')%positive; rewrite <-(assoc_L _); f_equal.
Robbert Krebbers's avatar
Robbert Krebbers committed
30
Qed.
31
Lemma ndot_nclose `{Countable A} N x : encode (ndot N x)  nclose N.
Robbert Krebbers's avatar
Robbert Krebbers committed
32
Proof. apply nclose_subseteq with x, encode_nclose. Qed.
33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62

Definition ndisj (N1 N2 : namespace) :=
   N1' N2', N1' `suffix_of` N1  N2' `suffix_of` N2 
             length N1' = length N2'  N1'  N2'.

Global Instance ndisj_comm : Comm iff ndisj.
Proof. intros N1 N2. rewrite /ndisj; naive_solver. Qed.

Lemma ndot_ne_disj `{Countable A} N (x y : A) :
  x  y  ndisj (ndot N x) (ndot N y).
Proof.
  intros Hxy. exists (ndot N x), (ndot N y). split_ands; try done; [].
  by apply not_inj2_2.
Qed.

Lemma ndot_preserve_disj_l `{Countable A} N1 N2 (x : A) :
  ndisj N1 N2  ndisj (ndot N1 x) N2.
Proof.
  intros (N1' & N2' & Hpr1 & Hpr2 & Hl & Hne). exists N1', N2'.
  split_ands; try done; []. by apply suffix_of_cons_r.
Qed.

Lemma ndot_preserve_disj_r `{Countable A} N1 N2 (x : A) :
  ndisj N1 N2  ndisj N1 (ndot N2 x).
Proof.
  rewrite ![ndisj N1 _]comm. apply ndot_preserve_disj_l.
Qed.

Lemma ndisj_disjoint N1 N2 :
  ndisj N1 N2  nclose N1  nclose N2 = .
Robbert Krebbers's avatar
Robbert Krebbers committed
63
Proof.
64 65
  intros (N1' & N2' & [N1'' Hpr1] & [N2'' Hpr2] & Hl & Hne). subst N1 N2.
  apply elem_of_equiv_empty_L=> p; unfold nclose.
Robbert Krebbers's avatar
Robbert Krebbers committed
66
  rewrite elem_of_intersection !elem_coPset_suffixes; intros [[q ->] [q' Hq]].
67 68
  rewrite !list_encode_app !assoc in Hq.
  apply Hne. eapply list_encode_suffix_eq; done.
69 70
Qed.

Ralf Jung's avatar
Ralf Jung committed
71 72
Local Hint Resolve nclose_subseteq ndot_nclose.

73 74
(** Derived forms and lemmas about them. *)
Definition inv {Λ Σ} (N : namespace) (P : iProp Λ Σ) : iProp Λ Σ :=
75 76 77
  ( i,  (i  nclose N)  ownI i P)%I.
Instance: Params (@inv) 3.
Typeclasses Opaque inv.
Ralf Jung's avatar
Ralf Jung committed
78 79 80 81 82 83 84 85

Section inv.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types i : positive.
Implicit Types N : namespace.
Implicit Types P Q R : iProp Λ Σ.

Global Instance inv_contractive N : Contractive (@inv Λ Σ N).
86
Proof. intros n ???. apply exists_ne=>i. by apply and_ne, ownI_contractive. Qed.
Ralf Jung's avatar
Ralf Jung committed
87

88 89
Global Instance inv_always_stable N P : AlwaysStable (inv N P).
Proof. rewrite /inv; apply _. Qed.
Ralf Jung's avatar
Ralf Jung committed
90 91 92 93

Lemma always_inv N P : ( inv N P)%I  inv N P.
Proof. by rewrite always_always. Qed.

94
(** Invariants can be opened around any frame-shifting assertion. *)
95 96 97
Lemma inv_fsa {A} (fsa : FSA Λ Σ A) `{!FrameShiftAssertion fsaV fsa}
    E N P (Q : A  iProp Λ Σ) R :
  fsaV 
Ralf Jung's avatar
Ralf Jung committed
98
  nclose N  E 
99
  R  inv N P 
100 101
  R  ( P - fsa (E  nclose N) (λ a,  P  Q a)) 
  R  fsa E Q.
Ralf Jung's avatar
Ralf Jung committed
102
Proof.
103 104
  intros ? HN Hinv Hinner.
  rewrite -[R](idemp ()%I) {1}Hinv Hinner =>{Hinv Hinner R}.
105
  rewrite always_and_sep_l /inv sep_exist_r. apply exist_elim=>i.
106
  rewrite always_and_sep_l -assoc. apply const_elim_sep_l=>HiN.
107
  rewrite -(fsa_open_close E (E  {[encode i]})) //; last by solve_elem_of+.
Ralf Jung's avatar
Ralf Jung committed
108
  (* Add this to the local context, so that solve_elem_of finds it. *)
109
  assert ({[encode i]}  nclose N) by eauto.
110
  rewrite (always_sep_dup (ownI _ _)).
Ralf Jung's avatar
Ralf Jung committed
111
  rewrite {1}pvs_openI !pvs_frame_r.
112
  apply pvs_mask_frame_mono; [solve_elem_of..|].
113
  rewrite (comm _ (_)%I) -assoc wand_elim_r fsa_frame_l.
114
  apply fsa_mask_frame_mono; [solve_elem_of..|]. intros a.
115
  rewrite assoc -always_and_sep_l pvs_closeI pvs_frame_r left_id.
Ralf Jung's avatar
Ralf Jung committed
116 117 118
  apply pvs_mask_frame'; solve_elem_of.
Qed.

119 120
(* Derive the concrete forms for pvs and wp, because they are useful. *)

121
Lemma pvs_open_close E N P Q R :
122
  nclose N  E 
123 124 125
  R  inv N P 
  R  (P - pvs (E  nclose N) (E  nclose N) (P  Q)) 
  R  pvs E E Q.
Ralf Jung's avatar
Ralf Jung committed
126
Proof. intros. by apply: (inv_fsa pvs_fsa). Qed.
127

128
Lemma wp_open_close E e N P (Q : val Λ  iProp Λ Σ) R :
Ralf Jung's avatar
Ralf Jung committed
129
  atomic e  nclose N  E 
130 131 132
  R  inv N P 
  R  (P - wp (E  nclose N) e (λ v, P  Q v)) 
  R  wp E e Q.
Ralf Jung's avatar
Ralf Jung committed
133
Proof. intros. by apply: (inv_fsa (wp_fsa e)). Qed.
Ralf Jung's avatar
Ralf Jung committed
134

135
Lemma inv_alloc N P :  P  pvs N N (inv N P).
136
Proof. by rewrite /inv (pvs_allocI N); last apply coPset_suffixes_infinite. Qed.
Ralf Jung's avatar
Ralf Jung committed
137 138

End inv.