proof.v 9.01 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 107
  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.
  { iNext. iFrame "Hl". iExists (const P). rewrite !big_sepS_singleton /=.
Robbert Krebbers's avatar
Robbert Krebbers committed
108
    iSplit; [|done]. by iIntros "> ?". }
Robbert Krebbers's avatar
Robbert Krebbers committed
109 110 111 112 113
  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.
114
    + set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
115 116 117 118
    + 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
119
  - iExists γ', P, P, γ. iFrame "Hr". repeat iSplit; auto. by iIntros "> ?".
Robbert Krebbers's avatar
Robbert Krebbers committed
120
  - iExists γ'. by iSplit.
121 122 123
Qed.

Lemma signal_spec l P (Φ : val  iProp) :
124
  (send l P  P  Φ #())  WP signal #l {{ Φ }}.
125
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
126 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".
  iDestruct "Hr" as {Ψ} "[? Hsp]"; iExists Ψ; iFrame "Hsp".
Robbert Krebbers's avatar
Robbert Krebbers committed
135
  iIntros "> _"; by iApply "Hr".
136 137 138
Qed.

Lemma wait_spec l P (Φ : val  iProp) :
139
  (recv l P  (P - Φ #()))  WP wait #l {{ Φ }}.
140
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
141 142
  rename P into R; rewrite /recv /barrier_ctx.
  iIntros "[Hr HΦ]"; iDestruct "Hr" as {γ P Q i} "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
143
  iLöb as "IH". wp_rec. wp_focus (! _)%E.
Robbert Krebbers's avatar
Robbert Krebbers committed
144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162
  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
163
      iExists Ψ; iFrame "Hsp". by iIntros "> _".
Robbert Krebbers's avatar
Robbert Krebbers committed
164 165 166
    + 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".
167 168
Qed.

169
Lemma recv_split E l P1 P2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
170
  nclose N  E  recv l (P1  P2)  |={E}=> recv l P1  recv l P2.
171
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193
  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
194
      by iIntros "> ?".
Robbert Krebbers's avatar
Robbert Krebbers committed
195
    + iExists γ, P, R2, i2. iFrame "Hγ2 Hi2". repeat iSplit; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
196
      by iIntros "> ?".
197 198
Qed.

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

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

Typeclasses Opaque barrier_ctx send recv.