proof.v 13.5 KB
Newer Older
1
From prelude Require Import functions.
2 3
From algebra Require Import upred_big_op.
From program_logic Require Import sts saved_prop tactics.
4 5
From heap_lang Require Export heap wp_tactics.
From barrier Require Export barrier.
6
From 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 Σ laterCF;
14
}.
15
(** The Functors we need. *)
16
Definition barrierGF : rFunctors := [stsGF sts; agreeRF laterCF].
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 {Σ : rFunctorG} `{!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 (Next (Ψ 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 52
    saved_prop_own i (Next Q)   (Q - R))%I.

53 54 55 56 57 58 59 60
Global Instance barrier_ctx_always_stable (γ : gname) (l : loc) (P : iProp) :
  AlwaysStable (barrier_ctx γ l P).
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 (Next R2) 
    saved_prop_own i1 (Next R1)  saved_prop_own i (Next Q) 
84 85
    (Q - R1  R2)  ress P I)
   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 93 94 95
  set savedQ := _ i _. set savedΨ := _ i _.
  sep_split left: [savedQ; savedΨ; Q - _;  (_ - Π★{set I} _)]%I.
  - rewrite !assoc saved_prop_agree later_equivI /=. strip_later.
    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))
Ralf Jung's avatar
Ralf Jung committed
115
   #> newbarrier #() {{ Φ }}.
116
Proof.
Ralf Jung's avatar
Ralf Jung committed
117
  intros HN. rewrite /newbarrier. wp_seq.
118 119 120 121
  rewrite -wp_pvs. wp eapply wp_alloc; eauto with I ndisj.
  apply forall_intro=>l. rewrite (forall_elim l). apply wand_intro_l.
  rewrite !assoc. apply pvs_wand_r.
  (* 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:=laterCF) _ (Next P)).
123 124
  rewrite pvs_frame_l. apply pvs_strip_pvs. rewrite sep_exist_l.
  apply exist_elim=>i.
125 126
  trans (pvs   (heap_ctx heapN 
     (barrier_inv l P (State Low {[ i ]}))  saved_prop_own i (Next P))).
127
  - rewrite -pvs_intro. cancel [heap_ctx heapN].
128
    rewrite {1}[saved_prop_own _ _]always_sep_dup. cancel [saved_prop_own i (Next 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) :
Ralf Jung's avatar
Ralf Jung committed
154
  (send l P  P  Φ #())  #> 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) :
Ralf Jung's avatar
Ralf Jung committed
179
  (recv l P  (P - Φ #()))  #> wait (%l) {{ Φ }}.
180 181 182 183 184 185
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.
  apply exist_elim=>i. rewrite -!assoc. 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 204 205
  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.
    rewrite -{2}pvs_wp. apply pvs_wand_r.
    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 220 221 222 223
  rewrite !(big_sepS_delete _ I i) //= !wand_True later_sep.
  ecancel [ Π★{set _} Ψ; Π★{set _} (λ _, saved_prop_own _ _)]%I.
  apply wand_intro_l.  set savedΨ := _ i _. set savedQ := _ i _.
  to_front [savedΨ; savedQ]. rewrite saved_prop_agree later_equivI /=.
  wp_op; [|done]=> _. wp_if. rewrite !assoc. eapply wand_apply_r'; first done.
  eapply wand_apply_r'; first done.
224
  apply: (eq_rewrite (Ψ i) Q (λ x, x)%I); by eauto with I.
225 226
Qed.

227 228 229
Lemma recv_split E l P1 P2 :
  nclose N  E  
  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 235
  apply exist_elim=>Q. apply exist_elim=>i. rewrite -!assoc.
  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 := Next 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 := Next 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 281 282 283 284
  (P1 - P2)  (recv l P1 - recv l P2).
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 290 291

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

295
End proof.