proof.v 14.2 KB
Newer Older
1 2 3 4 5
From prelude Require Import functions.
From algebra Require Import upred_big_op upred_tactics.
From program_logic Require Import sts saved_prop.
From heap_lang Require Export heap wp_tactics.
From barrier Require Export barrier.
6
From barrier Require Import protocol.
7 8 9 10 11 12
Import uPred.

(** The monoids we need. *)
(* 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
Definition barrierGF : rFunctors := [stsGF sts; agreeRF idCF].
16 17

Instance inGF_barrierG
18
  `{inGF heap_lang Σ (stsGF sts), inGF heap_lang Σ (agreeRF idCF)} : barrierG Σ.
19 20 21 22
Proof. split; apply _. Qed.

(** 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 53
    saved_prop_own i (Next Q)   (Q - R))%I.

Implicit Types I : gset gname.
54 55

(** Setoids *)
56 57 58 59
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).
60
Proof. solve_proper. Qed.
61
Global Instance barrier_inv_ne n l :
62 63
  Proper (dist n ==> eq ==> dist n) (barrier_inv l).
Proof. solve_proper. Qed.
64
Global Instance barrier_ctx_ne n γ l : Proper (dist n ==> dist n) (barrier_ctx γ l).
65
Proof. solve_proper. Qed.
66
Global Instance send_ne n l : Proper (dist n ==> dist n) (send l).
67
Proof. solve_proper. Qed.
68
Global Instance recv_ne n l : Proper (dist n ==> dist n) (recv l).
69
Proof. solve_proper. Qed.
70 71

(** Helper lemmas *)
72
Lemma ress_split i i1 i2 Q R1 R2 P I :
73
  i  I  i1  I  i2  I  i1  i2 
74 75
  (saved_prop_own i2 (Next R2) 
    saved_prop_own i1 (Next R1)  saved_prop_own i (Next Q) 
76 77
    (Q - R1  R2)  ress P I)
   ress P ({[i1]}  ({[i2]}  (I  {[i]}))).
78
Proof.
79
  intros. rewrite /ress !sep_exist_l. apply exist_elim=>Ψ.
80 81 82 83
  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.
84 85 86 87
  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.
88
    rewrite (big_sepS_delete _ I i) //.
89
    sep_split right: [Π★{set _} _]%I.
90 91 92 93
    + 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.
94 95 96
    + 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).
97 98 99 100
  - 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).
101
Qed.
102 103

(** Actual proofs *)
Ralf Jung's avatar
Ralf Jung committed
104
Lemma newbarrier_spec (P : iProp) (Φ : val  iProp) :
105
  heapN  N 
Ralf Jung's avatar
Ralf Jung committed
106
  (heap_ctx heapN   l, recv l P  send l P - Φ (%l))
Ralf Jung's avatar
Ralf Jung committed
107
   #> newbarrier #() {{ Φ }}.
108
Proof.
Ralf Jung's avatar
Ralf Jung committed
109
  intros HN. rewrite /newbarrier. wp_seq.
110 111 112 113
  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. *)
114
  eapply sep_elim_True_r; first by eapply (saved_prop_alloc (F:=idCF) _ (Next P)).
115 116
  rewrite pvs_frame_l. apply pvs_strip_pvs. rewrite sep_exist_l.
  apply exist_elim=>i.
117 118
  trans (pvs   (heap_ctx heapN 
     (barrier_inv l P (State Low {[ i ]}))  saved_prop_own i (Next P))).
119
  - rewrite -pvs_intro. cancel [heap_ctx heapN].
120
    rewrite {1}[saved_prop_own _ _]always_sep_dup. cancel [saved_prop_own i (Next P)].
121
    rewrite /barrier_inv /ress -later_intro. cancel [l  #0]%I.
122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146
    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 γ).
    (* This is even more annoying than usually, since rewrite sometimes unfolds stuff... *)
    rewrite [barrier_ctx _ _ _]lock !assoc
            [(_  locked (barrier_ctx _ _ _))%I]comm !assoc -lock.
    rewrite -always_sep_dup.
    (* TODO: This is cancelling below a pvs. *)
    rewrite [barrier_ctx _ _ _]lock always_and_sep_l -!assoc assoc -lock.
    rewrite -pvs_frame_l. rewrite /barrier_ctx const_equiv // left_id. apply sep_mono_r.
    rewrite [(saved_prop_own _ _  _)%I]comm !assoc. rewrite -pvs_frame_r.
    apply sep_mono_l.
    rewrite -assoc [( _  _)%I]comm assoc -pvs_frame_r.
    eapply sep_elim_True_r; last eapply sep_mono_l.
    { rewrite -later_intro. apply wand_intro_l. by rewrite right_id. }
    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.
147 148
    + intros []; set_solver.
    + set_solver.
149 150 151 152
    + 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
153
  (send l P  P  Φ #())  #> signal (%l) {{ Φ }}.
154 155 156 157 158 159 160 161 162 163
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.
  rewrite !assoc [(_  sts_ownS _ _ _)%I]comm -!assoc. apply sep_mono_r.
  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.
164 165
  eapply wp_store with (v' := #0); eauto with I ndisj. 
  strip_later. cancel [l  #0]%I.
166 167 168 169 170 171 172
  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.
  rewrite !assoc [(_  P)%I]comm !assoc -2!assoc.
  apply sep_mono; last first.
  { apply wand_intro_l. eauto with I. }
  (* Now we come to the core of the proof: Updating from waiting to ress. *)
173 174
  rewrite /ress sep_exist_l. apply exist_mono=>{Φ} Φ.
  rewrite later_wand {1}(later_intro P) !assoc wand_elim_r /= wand_True //.
175 176 177
Qed.

Lemma wait_spec l P (Φ : val  iProp) :
Ralf Jung's avatar
Ralf Jung committed
178
  (recv l P  (P - Φ #()))  #> wait (%l) {{ Φ }}.
179 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.
  apply exist_elim=>i. rewrite -!assoc. apply const_elim_sep_l=>?.
185
  wp_focus (! _)%E.
186 187 188 189 190 191 192 193
  (* I think some evars here are better than repeating *everything* *)
  eapply (sts_fsaS _ (wp_fsa _)) with (N0:=N) (γ0:=γ); simpl;
    eauto with I ndisj.
  rewrite !assoc [(_  sts_ownS _ _ _)%I]comm -!assoc. apply sep_mono_r.
  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.
194
  rewrite -!assoc. apply sep_mono_r. strip_later.
195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218
  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).
    rewrite !assoc.
    do 3 (rewrite -pvs_frame_r; apply sep_mono; last (try apply later_intro; reflexivity)).
    rewrite [(_  heap_ctx _)%I]comm -!assoc.
    rewrite const_equiv // left_id -pvs_frame_l. apply sep_mono_r.
    rewrite comm -pvs_frame_l. apply sep_mono_r.
    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.
219 220 221 222
  rewrite !sep_exist_r. apply exist_mono=>Ψ.
  rewrite !(big_sepS_delete _ I i) // [(_  Π★{set _} _)%I]comm -!assoc.
  rewrite /= !wand_True later_sep.
  ecancel [ Π★{set _} _; Π★{set _} (λ _, saved_prop_own _ _)]%I.
223 224
  apply wand_intro_l. rewrite [(heap_ctx _  _)%I]sep_elim_r.
  rewrite [(sts_own _ _ _  _)%I]sep_elim_r [(sts_ctx _ _ _  _)%I]sep_elim_r.
225
  rewrite [(saved_prop_own _ _  _  _)%I]assoc.
226
  rewrite saved_prop_agree later_equivI /=.
227
  wp_op; [|done]=> _. wp_if. rewrite !assoc.
228
  eapply wand_apply_r; [done..|]. eapply wand_apply_r; [done..|].
229
  apply: (eq_rewrite (Ψ i) Q (λ x, x)%I); by eauto with I.
230 231
Qed.

232 233 234
Lemma recv_split E l P1 P2 :
  nclose N  E  
  recv l (P1  P2)  |={E}=> recv l P1  recv l P2.
235
Proof.
236 237
  rename P1 into R1. rename P2 into R2. intros HN.
  rewrite {1}/recv /barrier_ctx. 
238
  apply exist_elim=>γ. rewrite sep_exist_r.  apply exist_elim=>P. 
239 240
  apply exist_elim=>Q. apply exist_elim=>i. rewrite -!assoc.
  apply const_elim_sep_l=>?. rewrite -pvs_trans'.
241
  (* I think some evars here are better than repeating *everything* *)
242
  eapply pvs_mk_fsa, (sts_fsaS _ pvs_fsa) with (N0:=N) (γ0:=γ); simpl;
243 244 245
    eauto with I ndisj.
  rewrite !assoc [(_  sts_ownS _ _ _)%I]comm -!assoc. apply sep_mono_r.
  apply forall_intro=>-[p I]. apply wand_intro_l. rewrite -!assoc.
246
  apply const_elim_sep_l=>Hs. rewrite /pvs_fsa.
247
  eapply sep_elim_True_l.
248
  { eapply saved_prop_alloc_strong with (x := Next R1) (G := I). }
249 250 251
  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.
252
  { eapply saved_prop_alloc_strong with (x := Next R2) (G := I  {[ i1 ]}). }
253 254 255 256
  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.
257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282
  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).
  do 2 rewrite !(assoc ()%I) [(_  sts_ownS _ _ _)%I]comm.
  rewrite -!assoc. rewrite [(sts_ownS _ _ _  _  _)%I]assoc.
  rewrite -pvs_frame_r. apply sep_mono.
  - 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.
  - rewrite const_equiv // !left_id.
    rewrite {1}[heap_ctx _]always_sep_dup {1}[sts_ctx _ _ _]always_sep_dup.
    rewrite !wand_diag -!later_intro. solve_sep_entails.
283 284
Qed.

285
Lemma recv_weaken l P1 P2 :
286 287 288 289 290 291 292 293 294
  (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.
  rewrite -!assoc. apply sep_mono_r, sep_mono_r, sep_mono_r, sep_mono_r, sep_mono_r.
  rewrite (later_intro (P1 - _)%I) -later_sep. apply later_mono.
  apply wand_intro_l. by rewrite !assoc wand_elim_r wand_elim_r.
Qed.
295 296 297 298

Lemma recv_mono l P1 P2 :
  P1  P2  recv l P1  recv l P2.
Proof.
299
  intros HP%entails_wand. apply wand_entails. rewrite HP. apply recv_weaken.
300 301
Qed.

302
End proof.