proof.v 9.17 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
  iIntros {????} "(#HQ&#H1&#H2&HQR&H)"; iDestruct "H" as {Ψ} "[HPΨ HΨ]".
85
  iDestruct (big_sepS_delete _ _ i with "HΨ") as "[#HΨi HΨ]"; first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
86
  iExists (<[i1:=R1]> (<[i2:=R2]> Ψ)). iSplitL "HQR HPΨ".
87
  - iPoseProof (saved_prop_agree i Q (Ψ i) with "[#]") as "Heq"; first by iSplit.
88 89 90
    iNext. iRewrite "Heq" in "HQR". iIntros "HP". iSpecialize ("HPΨ" with "HP").
    iDestruct (big_sepS_delete _ _ i with "HPΨ") as "[HΨ HPΨ]"; first done.
    iDestruct ("HQR" with "HΨ") as "[HR1 HR2]".
91 92
    rewrite !big_sepS_insert''; [|abstract set_solver ..]. by iFrame "HR1 HR2".
  - rewrite !big_sepS_insert'; [|abstract 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
  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 {γ} "#?".
105
  iPvs (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]")
106
    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
  iAssert (barrier_ctx γ' l P)%I as "#?".
  { rewrite /barrier_ctx. by repeat iSplit. }
  iPvsAssert (sts_ownS γ' (i_states γ) {[Change γ]}
113
     sts_ownS γ' low_states {[Send]})%I with "[-]" as "[Hr Hs]".
Robbert Krebbers's avatar
Robbert Krebbers committed
114
  { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
115
    + set_solver.
116
    + iApply (sts_own_weaken with "Hγ'");
Robbert Krebbers's avatar
Robbert Krebbers committed
117
        auto using sts.closed_op, i_states_closed, low_states_closed;
118
        abstract set_solver. }
Robbert Krebbers's avatar
Robbert Krebbers committed
119
  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
  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".
135
  iDestruct "Hr" as {Ψ} "[Hr 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
  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γ".
151
    iPvsAssert (sts_ownS γ (i_states i) {[Change i]})%I with "[Hγ]" as "Hγ".
152 153
    { iApply (sts_own_weaken with "Hγ"); eauto using i_states_closed. }
    wp_op=> ?; simplify_eq; wp_if. iApply ("IH" with "Hγ [HQR] HΦ"). by iNext.
Robbert Krebbers's avatar
Robbert Krebbers committed
154 155 156 157 158
  - (* 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]".
159
    iDestruct (big_sepS_delete _ _ i with "Hsp") as "[#HΨi Hsp]"; first done.
160
    iAssert ( Ψ i   Π★{set (I  {[i]})} Ψ)%I with "[HΨ]" as "[HΨ HΨ']".
Robbert Krebbers's avatar
Robbert Krebbers committed
161 162 163
    { 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 "> _".
165
    + iPoseProof (saved_prop_agree i Q (Ψ i) with "[#]") as "Heq"; first by iSplit.
Robbert Krebbers's avatar
Robbert Krebbers committed
166 167
      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
  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]}))
179
    as {i2} "[Hi2' #Hi2]"; iDestruct "Hi2'" as %Hi2; iPvsIntro.
Robbert Krebbers's avatar
Robbert Krebbers committed
180 181 182 183 184 185 186 187
  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]}
188
       sts_ownS γ (i_states i2) {[Change i2]})%I with "[-]" as "[Hγ1 Hγ2]".
Robbert Krebbers's avatar
Robbert Krebbers committed
189 190
    { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
      + set_solver.
191 192
      + iApply (sts_own_weaken with "Hγ");
          eauto using sts.closed_op, i_states_closed.
193
        abstract set_solver. }
Robbert Krebbers's avatar
Robbert Krebbers committed
194 195
    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
196
      by iIntros "> ?".
Robbert Krebbers's avatar
Robbert Krebbers committed
197
    + iExists γ, P, R2, i2. iFrame "Hγ2 Hi2". repeat iSplit; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
198
      by iIntros "> ?".
199 200
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
201
Lemma recv_weaken l P1 P2 : (P1 - P2)  (recv l P1 - recv l P2).
202
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
203 204 205
  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
206
  iIntros "> HQ". by iApply "HP"; iApply "HP1".
207
Qed.
208

209
Lemma recv_mono l P1 P2 : 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.