proof.v 13.6 KB
Newer Older
1 2 3 4
From iris.prelude Require Import functions.
From iris.algebra Require Import upred_big_op.
From iris.program_logic Require Import sts saved_prop tactics.
From iris.heap_lang Require Export heap wp_tactics.
Ralf Jung's avatar
Ralf Jung committed
5 6
From iris.heap_lang.lib.barrier Require Export barrier.
From iris.heap_lang.lib.barrier Require Import protocol.
7 8
Import uPred.

9
(** The CMRAs we need. *)
10 11 12
(* Not bundling heapG, as it may be shared with other users. *)
Class barrierG Σ := BarrierG {
  barrier_stsG :> stsG heap_lang Σ sts;
13
  barrier_savedPropG :> savedPropG heap_lang Σ idCF;
14
}.
15
(** The Functors we need. *)
16
Definition barrierGF : gFunctorList := [stsGF sts; savedPropGF idCF].
17 18 19
(* Show and register that they match. *)
Instance inGF_barrierG `{H : inGFs heap_lang Σ barrierGF} : barrierG Σ.
Proof. destruct H as (?&?&?). split; apply _. Qed.
20 21 22

(** Now we come to the Iris part of the proof. *)
Section proof.
23
Context {Σ : gFunctors} `{!heapG Σ, !barrierG Σ}.
24 25 26
Context (heapN N : namespace).
Local Notation iProp := (iPropG heap_lang Σ).

27
Definition ress (P : iProp) (I : gset gname) : iProp :=
28
  ( Ψ : gname  iProp,
29
     (P - Π★{set I} Ψ)  Π★{set I} (λ i, saved_prop_own i (Ψ i)))%I.
30 31

Coercion state_to_val (s : state) : val :=
32
  match s with State Low _ => #0 | State High _ => #1 end.
33 34
Arguments state_to_val !_ /.

35 36 37 38
Definition state_to_prop (s : state) (P : iProp) : iProp :=
  match s with State Low _ => P | State High _ => True%I end.
Arguments state_to_val !_ /.

39
Definition barrier_inv (l : loc) (P : iProp) (s : state) : iProp :=
40
  (l  s  ress (state_to_prop s P) (state_I s))%I.
41 42 43 44 45 46 47 48 49 50

Definition barrier_ctx (γ : gname) (l : loc) (P : iProp) : iProp :=
  ( (heapN  N)  heap_ctx heapN  sts_ctx γ N (barrier_inv l P))%I.

Definition send (l : loc) (P : iProp) : iProp :=
  ( γ, barrier_ctx γ l P  sts_ownS γ low_states {[ Send ]})%I.

Definition recv (l : loc) (R : iProp) : iProp :=
  ( γ P Q i,
    barrier_ctx γ l P  sts_ownS γ (i_states i) {[ Change i ]} 
51
    saved_prop_own i Q   (Q - R))%I.
52

53
Global Instance barrier_ctx_persistent (γ : gname) (l : loc) (P : iProp) :
54
  PersistentP (barrier_ctx γ l P).
55 56 57 58 59 60
Proof. apply _. Qed.

(* TODO: Figure out if this has a "Global" or "Local" effect.
   We want it to be Global. *)
Typeclasses Opaque barrier_ctx send recv.

61
Implicit Types I : gset gname.
62 63

(** Setoids *)
64 65 66 67
Global Instance ress_ne n : Proper (dist n ==> (=) ==> dist n) ress.
Proof. solve_proper. Qed.
Global Instance state_to_prop_ne n s :
  Proper (dist n ==> dist n) (state_to_prop s).
68
Proof. solve_proper. Qed.
69
Global Instance barrier_inv_ne n l :
70 71
  Proper (dist n ==> eq ==> dist n) (barrier_inv l).
Proof. solve_proper. Qed.
72
Global Instance barrier_ctx_ne n γ l : Proper (dist n ==> dist n) (barrier_ctx γ l).
73
Proof. solve_proper. Qed. 
74
Global Instance send_ne n l : Proper (dist n ==> dist n) (send l).
75
Proof. solve_proper. Qed.
76
Global Instance recv_ne n l : Proper (dist n ==> dist n) (recv l).
77
Proof. solve_proper. Qed.
78 79

(** Helper lemmas *)
80
Lemma ress_split i i1 i2 Q R1 R2 P I :
81
  i  I  i1  I  i2  I  i1  i2 
82 83
  (saved_prop_own i2 R2 
    saved_prop_own i1 R1  saved_prop_own i Q 
84
    (Q - R1  R2)  ress P I)
85
   ress P ({[i1]}  ({[i2]}  (I  {[i]}))).
86
Proof.
87
  intros. rewrite /ress !sep_exist_l. apply exist_elim=>Ψ.
88 89 90 91
  rewrite -(exist_intro (<[i1:=R1]> (<[i2:=R2]> Ψ))).
  rewrite [(Π★{set _} (λ _, saved_prop_own _ _))%I](big_sepS_delete _ I i) //.
  do 4 (rewrite big_sepS_insert; last set_solver).
  rewrite !fn_lookup_insert fn_lookup_insert_ne // !fn_lookup_insert.
92
  set savedQ := _ i Q. set savedΨ := _ i (Ψ _).
93
  sep_split left: [savedQ; savedΨ; Q - _;  (_ - Π★{set I} _)]%I.
94
  - rewrite !assoc saved_prop_agree /=. strip_later.
95
    apply wand_intro_l. to_front [P; P - _]%I. rewrite wand_elim_r.
96
    rewrite (big_sepS_delete _ I i) //.
97
    sep_split right: [Π★{set _} _]%I.
98 99 100 101
    + rewrite !assoc.
      eapply wand_apply_r'; first done.
      apply: (eq_rewrite (Ψ i) Q (λ x, x)%I); last by eauto with I.
      rewrite eq_sym. eauto with I.
102 103 104
    + apply big_sepS_mono; [done|] => j.
      rewrite elem_of_difference not_elem_of_singleton=> -[??].
      by do 2 (rewrite fn_lookup_insert_ne; last naive_solver).
105 106 107 108
  - rewrite !assoc [(saved_prop_own i2 _  _)%I]comm; apply sep_mono_r.
    apply big_sepS_mono; [done|]=> j.
    rewrite elem_of_difference not_elem_of_singleton=> -[??].
    by do 2 (rewrite fn_lookup_insert_ne; last naive_solver).
109
Qed.
110 111

(** Actual proofs *)
Ralf Jung's avatar
Ralf Jung committed
112
Lemma newbarrier_spec (P : iProp) (Φ : val  iProp) :
113
  heapN  N 
Ralf Jung's avatar
Ralf Jung committed
114
  (heap_ctx heapN   l, recv l P  send l P - Φ (%l))
115
   WP newbarrier #() {{ Φ }}.
116
Proof.
Ralf Jung's avatar
Ralf Jung committed
117
  intros HN. rewrite /newbarrier. wp_seq.
118 119
  rewrite -wp_pvs. wp eapply wp_alloc; eauto with I ndisj.
  apply forall_intro=>l. rewrite (forall_elim l). apply wand_intro_l.
120
  rewrite !assoc. rewrite- pvs_wand_r; apply sep_mono_l.
121
  (* The core of this proof: Allocating the STS and the saved prop. *)
122
  eapply sep_elim_True_r; first by eapply (saved_prop_alloc (F:=idCF) _ P).
123 124
  rewrite pvs_frame_l. apply pvs_strip_pvs. rewrite sep_exist_l.
  apply exist_elim=>i.
125
  trans (pvs   (heap_ctx heapN 
126
     (barrier_inv l P (State Low {[ i ]}))  saved_prop_own i P)).
127
  - rewrite -pvs_intro. cancel [heap_ctx heapN].
128
    rewrite {1}[saved_prop_own _ _]always_sep_dup. cancel [saved_prop_own i P].
129
    rewrite /barrier_inv /ress -later_intro. cancel [l  #0]%I.
130 131 132 133 134 135 136 137
    rewrite -(exist_intro (const P)) /=. rewrite -[saved_prop_own _ _](left_id True%I ()%I).
    by rewrite !big_sepS_singleton /= wand_diag -later_intro.
  - rewrite (sts_alloc (barrier_inv l P)  N); last by eauto.
    rewrite !pvs_frame_r !pvs_frame_l. 
    rewrite pvs_trans'. apply pvs_strip_pvs. rewrite sep_exist_r sep_exist_l.
    apply exist_elim=>γ.
    rewrite /recv /send. rewrite -(exist_intro γ) -(exist_intro P).
    rewrite -(exist_intro P) -(exist_intro i) -(exist_intro γ).
138 139 140 141 142
    rewrite always_and_sep_l wand_diag later_True right_id.
    rewrite [heap_ctx _]always_sep_dup [sts_ctx _ _ _]always_sep_dup.
    rewrite /barrier_ctx const_equiv // left_id.
    ecancel_pvs [saved_prop_own i _; heap_ctx _; heap_ctx _;
                 sts_ctx _ _ _; sts_ctx _ _ _].
143 144 145 146 147
    rewrite (sts_own_weaken  _ _ (i_states i  low_states) _ 
                            ({[ Change i ]}  {[ Send ]})).
    + apply pvs_mono.
      rewrite -sts_ownS_op; eauto using i_states_closed, low_states_closed.
      set_solver.
148 149
    + intros []; set_solver.
    + set_solver.
150 151 152 153
    + auto using sts.closed_op, i_states_closed, low_states_closed.
Qed.

Lemma signal_spec l P (Φ : val  iProp) :
154
  (send l P  P  Φ #())  WP signal (%l) {{ Φ }}.
155 156 157 158 159 160
Proof.
  rewrite /signal /send /barrier_ctx. rewrite sep_exist_r.
  apply exist_elim=>γ. rewrite -!assoc. apply const_elim_sep_l=>?. wp_let.
  (* I think some evars here are better than repeating *everything* *)
  eapply (sts_fsaS _ (wp_fsa _)) with (N0:=N) (γ0:=γ); simpl;
    eauto with I ndisj.
161
  ecancel [sts_ownS γ _ _]. 
162 163 164
  apply forall_intro=>-[p I]. apply wand_intro_l. rewrite -!assoc.
  apply const_elim_sep_l=>Hs. destruct p; last done.
  rewrite {1}/barrier_inv =>/={Hs}. rewrite later_sep.
165 166
  eapply wp_store with (v' := #0); eauto with I ndisj. 
  strip_later. cancel [l  #0]%I.
167 168 169
  apply wand_intro_l. rewrite -(exist_intro (State High I)).
  rewrite -(exist_intro ). rewrite const_equiv /=; last by eauto using signal_step.
  rewrite left_id -later_intro {2}/barrier_inv -!assoc. apply sep_mono_r.
170
  sep_split right: [Φ _]; last first.
171 172
  { apply wand_intro_l. eauto with I. }
  (* Now we come to the core of the proof: Updating from waiting to ress. *)
173 174 175
  rewrite /ress sep_exist_r. apply exist_mono=>{Φ} Φ.
  ecancel [Π★{set I} (λ _, saved_prop_own _ _)]%I. strip_later.
  rewrite wand_True. eapply wand_apply_l'; eauto with I.
176 177 178
Qed.

Lemma wait_spec l P (Φ : val  iProp) :
179
  (recv l P  (P - Φ #()))  WP wait (%l) {{ Φ }}.
180 181 182 183 184
Proof.
  rename P into R. wp_rec.
  rewrite {1}/recv /barrier_ctx. rewrite !sep_exist_r.
  apply exist_elim=>γ. rewrite !sep_exist_r. apply exist_elim=>P.
  rewrite !sep_exist_r. apply exist_elim=>Q. rewrite !sep_exist_r.
185
  apply exist_elim=>i. rewrite -!(assoc ()%I). apply const_elim_sep_l=>?.
186
  wp_focus (! _)%E.
187 188 189
  (* I think some evars here are better than repeating *everything* *)
  eapply (sts_fsaS _ (wp_fsa _)) with (N0:=N) (γ0:=γ); simpl;
    eauto with I ndisj.
190
  ecancel [sts_ownS γ _ _].
191 192 193 194
  apply forall_intro=>-[p I]. apply wand_intro_l. rewrite -!assoc.
  apply const_elim_sep_l=>Hs.
  rewrite {1}/barrier_inv =>/=. rewrite later_sep.
  eapply wp_load; eauto with I ndisj.
195
  ecancel [ l {_} _]%I. strip_later.
196 197 198 199 200 201 202 203
  apply wand_intro_l. destruct p.
  { (* a Low state. The comparison fails, and we recurse. *)
    rewrite -(exist_intro (State Low I)) -(exist_intro {[ Change i ]}).
    rewrite [( sts.steps _ _ )%I]const_equiv /=; last by apply rtc_refl.
    rewrite left_id -[( barrier_inv _ _ _)%I]later_intro {3}/barrier_inv.
    rewrite -!assoc. apply sep_mono_r, sep_mono_r, wand_intro_l.
    wp_op; first done. intros _. wp_if. rewrite !assoc.
    rewrite -always_wand_impl always_elim.
204
    rewrite -{2}pvs_wp. rewrite -pvs_wand_r; apply sep_mono_l.
205
    rewrite -(exist_intro γ) -(exist_intro P) -(exist_intro Q) -(exist_intro i).
206 207
    rewrite const_equiv // left_id -later_intro.
    ecancel_pvs [heap_ctx _; saved_prop_own _ _; Q - _; R - _; sts_ctx _ _ _]%I.
208 209 210 211 212 213 214 215 216
    apply sts_own_weaken; eauto using i_states_closed. }
  (* a High state: the comparison succeeds, and we perform a transition and
     return to the client *)
  rewrite [(_   (_  _ ))%I]sep_elim_l.
  rewrite -(exist_intro (State High (I  {[ i ]}))) -(exist_intro ).
  change (i  I) in Hs.
  rewrite const_equiv /=; last by eauto using wait_step.
  rewrite left_id -[( barrier_inv _ _ _)%I]later_intro {2}/barrier_inv.
  rewrite -!assoc. apply sep_mono_r. rewrite /ress.
217
  rewrite !sep_exist_r. apply exist_mono=>Ψ.
218 219
  rewrite !(big_sepS_delete _ I i) //= !wand_True later_sep.
  ecancel [ Π★{set _} Ψ; Π★{set _} (λ _, saved_prop_own _ _)]%I.
220 221
  apply wand_intro_l.  set savedΨ := _ i (Ψ _). set savedQ := _ i Q.
  to_front [savedΨ; savedQ]. rewrite saved_prop_agree /=.
222
  wp_op; [|done]=> _. wp_if. rewrite -pvs_intro. rewrite !assoc. eapply wand_apply_r'; first done.
223
  eapply wand_apply_r'; first done.
224
  apply: (eq_rewrite (Ψ i) Q (λ x, x)%I); by eauto with I.
225 226
Qed.

227 228
Lemma recv_split E l P1 P2 :
  nclose N  E  
229
  recv l (P1  P2)  |={E}=> recv l P1  recv l P2.
230
Proof.
231 232
  rename P1 into R1. rename P2 into R2. intros HN.
  rewrite {1}/recv /barrier_ctx. 
233
  apply exist_elim=>γ. rewrite sep_exist_r.  apply exist_elim=>P. 
234
  apply exist_elim=>Q. apply exist_elim=>i. rewrite -!(assoc ()%I).
235
  apply const_elim_sep_l=>?. rewrite -pvs_trans'.
236
  (* I think some evars here are better than repeating *everything* *)
237
  eapply pvs_mk_fsa, (sts_fsaS _ pvs_fsa) with (N0:=N) (γ0:=γ); simpl;
238
    eauto with I ndisj.
239
  ecancel [sts_ownS γ _ _].
240
  apply forall_intro=>-[p I]. apply wand_intro_l. rewrite -!assoc.
241
  apply const_elim_sep_l=>Hs. rewrite /pvs_fsa.
242
  eapply sep_elim_True_l.
243
  { eapply saved_prop_alloc_strong with (x := R1) (G := I). }
244 245 246
  rewrite pvs_frame_r. apply pvs_strip_pvs. rewrite sep_exist_r.
  apply exist_elim=>i1. rewrite always_and_sep_l. rewrite -assoc.
  apply const_elim_sep_l=>Hi1. eapply sep_elim_True_l.
247
  { eapply saved_prop_alloc_strong with (x := R2) (G := I  {[ i1 ]}). }
248 249 250 251
  rewrite pvs_frame_r. apply pvs_mono. rewrite sep_exist_r.
  apply exist_elim=>i2. rewrite always_and_sep_l. rewrite -assoc.
  apply const_elim_sep_l=>Hi2.
  rewrite ->not_elem_of_union, elem_of_singleton in Hi2.
252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267
  destruct Hi2 as [Hi2 Hi12]. change (i  I) in Hs.
  (* Update to new state. *)
  rewrite -(exist_intro (State p ({[i1]}  ({[i2]}  (I  {[i]}))))).
  rewrite -(exist_intro ({[Change i1 ]}  {[ Change i2 ]})).
  rewrite [( sts.steps _ _)%I]const_equiv; last by eauto using split_step.
  rewrite left_id {1 3}/barrier_inv.
  (* FIXME ssreflect rewrite fails if there are evars around. Also, this is very slow because we don't have a proof mode. *)
  rewrite -(ress_split _ _ _ Q R1 R2); [|done..].
  rewrite {1}[saved_prop_own i1 _]always_sep_dup.
  rewrite {1}[saved_prop_own i2 _]always_sep_dup !later_sep.
  rewrite -![( saved_prop_own _ _)%I]later_intro.
  ecancel [ l  _; saved_prop_own i1 _; saved_prop_own i2 _ ;
            ress _ _ ;  (Q - _) ; saved_prop_own i _]%I. 
  apply wand_intro_l. rewrite !assoc. rewrite /recv.
  rewrite -(exist_intro γ) -(exist_intro P) -(exist_intro R1) -(exist_intro i1).
  rewrite -(exist_intro γ) -(exist_intro P) -(exist_intro R2) -(exist_intro i2).
268 269 270 271 272 273 274 275 276
  rewrite [heap_ctx _]always_sep_dup [sts_ctx _ _ _]always_sep_dup.
  rewrite /barrier_ctx const_equiv // left_id.
  ecancel_pvs [saved_prop_own i1 _; saved_prop_own i2 _; heap_ctx _; heap_ctx _;
               sts_ctx _ _ _; sts_ctx _ _ _].
  rewrite !wand_diag later_True !right_id.
  rewrite -sts_ownS_op; eauto using i_states_closed.
  - apply sts_own_weaken;
      eauto using sts.closed_op, i_states_closed. set_solver.
  - set_solver.
277 278
Qed.

279
Lemma recv_weaken l P1 P2 :
280
  (P1 - P2)  (recv l P1 - recv l P2).
281 282 283 284
Proof.
  apply wand_intro_l. rewrite /recv. rewrite sep_exist_r. apply exist_mono=>γ.
  rewrite sep_exist_r. apply exist_mono=>P. rewrite sep_exist_r.
  apply exist_mono=>Q. rewrite sep_exist_r. apply exist_mono=>i.
285 286
  ecancel [barrier_ctx _ _ _; sts_ownS _ _ _; saved_prop_own _ _].
  strip_later. apply wand_intro_l. by rewrite !assoc wand_elim_r wand_elim_r.
287
Qed.
288 289

Lemma recv_mono l P1 P2 :
290
  P1  P2  recv l P1  recv l P2.
291
Proof.
292
  intros HP%entails_wand. apply wand_entails. rewrite HP. apply recv_weaken.
293 294
Qed.

295
End proof.