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

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

(** Now we come to the Iris part of the proof. *)
Section proof.
24
Context {Σ : gFunctors} `{!heapG Σ, !barrierG Σ}.
25
Context (heapN N : namespace).
Robbert Krebbers's avatar
Robbert Krebbers committed
26
Implicit Types I : gset gname.
27 28
Local Notation iProp := (iPropG heap_lang Σ).

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

Coercion state_to_val (s : state) : val :=
34
  match s with State Low _ => #0 | State High _ => #1 end.
Robbert Krebbers's avatar
Robbert Krebbers committed
35
Arguments state_to_val !_ / : simpl nomatch.
36

37 38
Definition state_to_prop (s : state) (P : iProp) : iProp :=
  match s with State Low _ => P | State High _ => True%I end.
Robbert Krebbers's avatar
Robbert Krebbers committed
39
Arguments state_to_prop !_ _ / : simpl nomatch.
40

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

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 ]} 
53
    saved_prop_own i Q   (Q - R))%I.
54

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

Typeclasses Opaque barrier_ctx send recv.

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

(** Helper lemmas *)
78
Lemma ress_split i i1 i2 Q R1 R2 P I :
79
  i  I  i1  I  i2  I  i1  i2 
Robbert Krebbers's avatar
Robbert Krebbers committed
80
  (saved_prop_own i Q  saved_prop_own i1 R1  saved_prop_own i2 R2 
81
    (Q - R1  R2)  ress P I)
82
   ress P ({[i1]}  ({[i2]}  (I  {[i]}))).
83
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
84 85 86 87 88 89 90 91 92
  iIntros {????} "(#HQ&#H1&#H2&HQR&H)"; iDestruct "H" as {Ψ} "[HPΨ HΨ]".
  iDestruct (big_sepS_delete _ _ i) "HΨ" as "[#HΨi HΨ]"; first done.
  iExists (<[i1:=R1]> (<[i2:=R2]> Ψ)). iSplitL "HQR HPΨ".
  - iPoseProof (saved_prop_agree i Q (Ψ i)) "#" as "Heq"; first by iSplit.
    iNext. iRewrite "Heq" in "HQR". iIntros "HP". iSpecialize "HPΨ" "HP". 
    iDestruct (big_sepS_delete _ _ i) "HPΨ" as "[HΨ HPΨ]"; first done.
    iDestruct "HQR" "HΨ" as "[HR1 HR2]".
    rewrite !big_sepS_insert''; [|set_solver ..]. by iFrame "HR1 HR2".
  - rewrite !big_sepS_insert'; [|set_solver ..]. by repeat iSplit.
93
Qed.
94 95

(** Actual proofs *)
Ralf Jung's avatar
Ralf Jung committed
96
Lemma newbarrier_spec (P : iProp) (Φ : val  iProp) :
97
  heapN  N 
98
  (heap_ctx heapN   l, recv l P  send l P - Φ #l)
99
   WP newbarrier #() {{ Φ }}.
100
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
101 102 103 104 105 106
  iIntros {HN} "[#? HΦ]".
  rewrite /newbarrier. wp_seq. iApply wp_pvs. wp_alloc l as "Hl".
  iApply "HΦ".
  iPvs (saved_prop_alloc (F:=idCF) _ P) as {γ} "#?".
  iPvs (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}))
    "-" as {γ'} "[#? Hγ']"; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
107 108
  { iNext. rewrite /barrier_inv /=. iFrame "Hl".
    iExists (const P). rewrite !big_sepS_singleton /=.
Robbert Krebbers's avatar
Robbert Krebbers committed
109
    iSplit; [|done]. by iIntros "> ?". }
Robbert Krebbers's avatar
Robbert Krebbers committed
110 111 112 113 114
  iAssert (barrier_ctx γ' l P)%I as "#?".
  { rewrite /barrier_ctx. by repeat iSplit. }
  iPvsAssert (sts_ownS γ' (i_states γ) {[Change γ]}
     sts_ownS γ' low_states {[Send]})%I as "[Hr Hs]" with "-".
  { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
115
    + set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
116 117 118 119
    + iApply sts_own_weaken "Hγ'";
        auto using sts.closed_op, i_states_closed, low_states_closed;
        set_solver. }
  iPvsIntro. rewrite /recv /send. iSplitL "Hr".
Robbert Krebbers's avatar
Robbert Krebbers committed
120
  - iExists γ', P, P, γ. iFrame "Hr". repeat iSplit; auto. by iIntros "> ?".
Robbert Krebbers's avatar
Robbert Krebbers committed
121
  - iExists γ'. by iSplit.
122 123 124
Qed.

Lemma signal_spec l P (Φ : val  iProp) :
125
  (send l P  P  Φ #())  WP signal #l {{ Φ }}.
126
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
127 128 129 130 131 132 133 134 135
  rewrite /signal /send /barrier_ctx.
  iIntros "(Hs&HP&HΦ)"; iDestruct "Hs" as {γ} "[#(%&Hh&Hsts) Hγ]". wp_let.
  iSts γ as [p I]; iDestruct "Hγ" as "[Hl Hr]".
  wp_store. destruct p; [|done].
  iExists (State High I), ( : set token).
  iSplit; [iPureIntro; by eauto using signal_step|].
  iSplitR "HΦ"; [iNext|by iIntros "?"].
  rewrite {2}/barrier_inv /ress /=; iFrame "Hl".
  iDestruct "Hr" as {Ψ} "[? Hsp]"; iExists Ψ; iFrame "Hsp".
Robbert Krebbers's avatar
Robbert Krebbers committed
136
  iIntros "> _"; by iApply "Hr".
137 138 139
Qed.

Lemma wait_spec l P (Φ : val  iProp) :
140
  (recv l P  (P - Φ #()))  WP wait #l {{ Φ }}.
141
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
142 143
  rename P into R; rewrite /recv /barrier_ctx.
  iIntros "[Hr HΦ]"; iDestruct "Hr" as {γ P Q i} "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
144
  iLöb as "IH". wp_rec. wp_focus (! _)%E.
Robbert Krebbers's avatar
Robbert Krebbers committed
145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163
  iSts γ as [p I]; iDestruct "Hγ" as "[Hl Hr]".
  wp_load. destruct p.
  - (* a Low state. The comparison fails, and we recurse. *)
    iExists (State Low I), {[ Change i ]}; iSplit; [done|iSplitL "Hl Hr"].
    { iNext. rewrite {2}/barrier_inv /=. by iFrame "Hl". }
    iIntros "Hγ".
    iPvsAssert (sts_ownS γ (i_states i) {[Change i]})%I as "Hγ" with "[Hγ]".
    { iApply sts_own_weaken "Hγ"; eauto using i_states_closed. }
    wp_op=> ?; simplify_eq; wp_if. iApply "IH" "Hγ [HQR] HΦ". by iNext.
  - (* a High state: the comparison succeeds, and we perform a transition and
    return to the client *)
    iExists (State High (I  {[ i ]})), ( : set token).
    iSplit; [iPureIntro; by eauto using wait_step|].
    iDestruct "Hr" as {Ψ} "[HΨ Hsp]".
    iDestruct (big_sepS_delete _ _ i) "Hsp" as "[#HΨi Hsp]"; first done.
    iAssert ( Ψ i   Π★{set (I  {[i]})} Ψ)%I as "[HΨ HΨ']" with "[HΨ]".
    { iNext. iApply (big_sepS_delete _ _ i); first done. by iApply "HΨ". }
    iSplitL "HΨ' Hl Hsp"; [iNext|].
    + rewrite {2}/barrier_inv /=; iFrame "Hl".
Robbert Krebbers's avatar
Robbert Krebbers committed
164
      iExists Ψ; iFrame "Hsp". by iIntros "> _".
Robbert Krebbers's avatar
Robbert Krebbers committed
165 166 167
    + iPoseProof (saved_prop_agree i Q (Ψ i)) "#" as "Heq"; first by iSplit.
      iIntros "_". wp_op=> ?; simplify_eq/=; wp_if.
      iPvsIntro. iApply "HΦ". iApply "HQR". by iRewrite "Heq".
168 169
Qed.

170
Lemma recv_split E l P1 P2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
171
  nclose N  E  recv l (P1  P2)  |={E}=> recv l P1  recv l P2.
172
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194
  rename P1 into R1; rename P2 into R2. rewrite {1}/recv /barrier_ctx.
  iIntros {?} "Hr"; iDestruct "Hr" as {γ P Q i} "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
  iApply pvs_trans'.
  iSts γ as [p I]; iDestruct "Hγ" as "[Hl Hr]".
  iPvs (saved_prop_alloc_strong _ (R1: %CF iProp) I) as {i1} "[% #Hi1]".
  iPvs (saved_prop_alloc_strong _ (R2: %CF iProp) (I  {[i1]}))
    as {i2} "[Hi2' #Hi2]"; iPure "Hi2'" as Hi2; iPvsIntro.
  rewrite ->not_elem_of_union, elem_of_singleton in Hi2; destruct Hi2.
  iExists (State p ({[i1]}  ({[i2]}  (I  {[i]})))).
  iExists ({[Change i1 ]}  {[ Change i2 ]}).
  iSplit; [by eauto using split_step|iSplitL].
  - iNext. rewrite {2}/barrier_inv /=. iFrame "Hl".
    iApply (ress_split _ _ _ Q R1 R2); eauto. iFrame "Hr HQR". by repeat iSplit.
  - iIntros "Hγ".
    iPvsAssert (sts_ownS γ (i_states i1) {[Change i1]}
       sts_ownS γ (i_states i2) {[Change i2]})%I as "[Hγ1 Hγ2]" with "-".
    { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
      + set_solver.
      + iApply sts_own_weaken "Hγ"; eauto using sts.closed_op, i_states_closed.
        set_solver. }
    iPvsIntro; iSplitL "Hγ1"; rewrite /recv /barrier_ctx.
    + iExists γ, P, R1, i1. iFrame "Hγ1 Hi1". repeat iSplit; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
195
      by iIntros "> ?".
Robbert Krebbers's avatar
Robbert Krebbers committed
196
    + iExists γ, P, R2, i2. iFrame "Hγ2 Hi2". repeat iSplit; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
197
      by iIntros "> ?".
198 199
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
200
Lemma recv_weaken l P1 P2 : (P1 - P2)  (recv l P1 - recv l P2).
201
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
202 203 204
  rewrite /recv.
  iIntros "HP HP1"; iDestruct "HP1" as {γ P Q i} "(#Hctx&Hγ&Hi&HP1)".
  iExists γ, P, Q, i; iFrame "Hctx Hγ Hi".
Robbert Krebbers's avatar
Robbert Krebbers committed
205
  iIntros "> HQ". by iApply "HP"; iApply "HP1".
206
Qed.
207 208

Lemma recv_mono l P1 P2 :
209
  P1  P2  recv l P1  recv l P2.
210
Proof.
211
  intros HP%entails_wand. apply wand_entails. rewrite HP. apply recv_weaken.
212
Qed.
213
End proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
214 215

Typeclasses Opaque barrier_ctx send recv.