basics.v 11 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2
(** This file includes basic examples that each describe a unique feature of 
dependent separation protocols. *)
3 4
From actris.channel Require Import proofmode.
From iris.heap_lang Require Import lib.spin_lock.
5
From actris.utils Require Import contribution.
Robbert Krebbers's avatar
Robbert Krebbers committed
6

7
(** Basic *)
8
Definition prog : val := λ: <>,
Robbert Krebbers's avatar
Robbert Krebbers committed
9 10 11
  let: "c" := start_chan (λ: "c'", send "c'" #42) in
  recv "c".

Robbert Krebbers's avatar
Robbert Krebbers committed
12
(** Tranfering References *)
13
Definition prog_ref : val := λ: <>,
Robbert Krebbers's avatar
Robbert Krebbers committed
14 15 16
  let: "c" := start_chan (λ: "c'", send "c'" (ref #42)) in
  ! (recv "c").

Robbert Krebbers's avatar
Robbert Krebbers committed
17
(** Delegation, i.e. transfering channels *)
18
Definition prog_del : val := λ: <>,
Robbert Krebbers's avatar
Robbert Krebbers committed
19 20 21 22 23 24
  let: "c1" := start_chan (λ: "c1'",
    let: "cc2" := new_chan #() in
    send "c1'" (Fst "cc2");;
    send (Snd "cc2") #42) in
  recv (recv "c1").

Robbert Krebbers's avatar
Robbert Krebbers committed
25
(** Dependent protocols *)
26
Definition prog_dep : val := λ: <>,
Robbert Krebbers's avatar
Robbert Krebbers committed
27 28 29 30 31
  let: "c" := start_chan (λ: "c'",
    let: "x" := recv "c'" in send "c'" ("x" + #2)) in
  send "c" #40;;
  recv "c".

32
Definition prog_dep_ref : val := λ: <>,
Robbert Krebbers's avatar
Robbert Krebbers committed
33 34 35 36
  let: "c" := start_chan (λ: "c'",
    let: "l" := recv "c'" in "l" <- !"l" + #2;; send "c'" #()) in
  let: "l" := ref #40 in send "c" "l";; recv "c";; !"l".

37
Definition prog_dep_del : val := λ: <>,
Robbert Krebbers's avatar
Robbert Krebbers committed
38 39 40 41 42 43
  let: "c1" := start_chan (λ: "c1'",
    let: "cc2" := new_chan #() in
    send "c1'" (Fst "cc2");;
    let: "x" := recv (Snd "cc2") in send (Snd "cc2") ("x" + #2)) in
  let: "c2'" := recv "c1" in send "c2'" #40;; recv "c2'".

Robbert Krebbers's avatar
Robbert Krebbers committed
44 45 46 47 48 49 50 51
Definition prog_dep_del_2 : val := λ: <>,
  let: "c1" := start_chan (λ: "c1'",
    send (recv "c1'") #40;;
    send "c1'" #()) in
  let: "c2" := start_chan (λ: "c2'",
    let: "x" := recv "c2'" in send "c2'" ("x" + #2)) in
  send "c1" "c2";; recv "c1";; recv "c2".

52 53
Definition prog_dep_del_3 : val := λ: <>,
  let: "c1" := start_chan (λ: "c1'",
54 55
    let: "c" := recv "c1'" in let: "y" := recv "c1'" in
    send "c" "y";; send "c1'" #()) in
56 57
  let: "c2" := start_chan (λ: "c2'",
    let: "x" := recv "c2'" in send "c2'" ("x" + #2)) in
58
  send "c1" "c2";; send "c1" #40;; recv "c1";; recv "c2".
59

Robbert Krebbers's avatar
Robbert Krebbers committed
60 61 62 63 64 65 66 67 68 69 70 71 72
(** Loops *)
Definition prog_loop : val := λ: <>,
  let: "c" := start_chan (λ: "c'",
    let: "go" :=
      rec: "go" <> :=
        let: "x" := recv "c'" in send "c'" ("x" + #2);; "go" #() in
    "go" #()) in
  send "c" #18;;
  let: "x1" := recv "c" in
  send "c" #20;;
  let: "x2" := recv "c" in
  "x1" + "x2".

Robbert Krebbers's avatar
Robbert Krebbers committed
73
(** Transfering higher-order functions *)
74
Definition prog_fun : val := λ: <>,
Robbert Krebbers's avatar
Robbert Krebbers committed
75 76 77 78 79 80
  let: "c" := start_chan (λ: "c'",
    let: "f" := recv "c'" in send "c'" (λ: <>, "f" #() + #2)) in
  let: "r" := ref #40 in
  send "c" (λ: <>, !"r");;
  recv "c" #().

Robbert Krebbers's avatar
Robbert Krebbers committed
81
(** Lock protected channel endpoints *)
82 83 84 85 86 87 88
Definition prog_lock : val := λ: <>,
  let: "c" := start_chan (λ: "c'",
    let: "l" := newlock #() in
    Fork (acquire "l";; send "c'" #21;; release "l");;
    acquire "l";; send "c'" #21;; release "l") in
  recv "c" + recv "c".

Robbert Krebbers's avatar
Robbert Krebbers committed
89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106
(** Swapping of sends *)
Definition prog_swap : val := λ: <>,
  let: "c" := start_chan (λ: "c'",
    send "c'" #20;;
    let: "y" := recv "c'" in
    send "c'" "y") in
  send "c" #22;;
  recv "c" + recv "c".

Definition prog_swap_twice : val := λ: <>,
  let: "c" := start_chan (λ: "c'",
    send "c'" #20;;
    let: "y1" := recv "c'" in
    let: "y2" := recv "c'" in
    send "c'" ("y1" + "y2")) in
  send "c" #11;; send "c" #11;;
  recv "c" + recv "c".

Robbert Krebbers's avatar
Robbert Krebbers committed
107
Section proofs.
108
Context `{heapG Σ, chanG Σ}.
Robbert Krebbers's avatar
Robbert Krebbers committed
109

Robbert Krebbers's avatar
Robbert Krebbers committed
110
(** Protocols for the respective programs *)
111
Definition prot : iProto Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
112 113
  (<?> MSG #42; END)%proto.

114
Definition prot_ref : iProto Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
115 116
  (<?> l : loc, MSG #l {{ l  #42 }}; END)%proto.

117 118
Definition prot_del : iProto Σ :=
  (<?> c : val, MSG c {{ c  prot }}; END)%proto.
Robbert Krebbers's avatar
Robbert Krebbers committed
119

120
Definition prot_dep : iProto Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
121 122
  (<!> x : Z, MSG #x; <?> MSG #(x + 2); END)%proto.

123
Definition prot_dep_ref : iProto Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
124 125 126 127
  (<!> (l : loc) (x : Z), MSG #l {{ l  #x }};
   <?> MSG #() {{ l  #(x + 2) }};
   END)%proto.

128 129
Definition prot_dep_del : iProto Σ :=
  (<?> c : val, MSG c {{ c  prot_dep }}; END)%proto.
Robbert Krebbers's avatar
Robbert Krebbers committed
130

Robbert Krebbers's avatar
Robbert Krebbers committed
131 132 133 134 135
Definition prot_dep_del_2 : iProto Σ :=
  (<!> c : val, MSG c {{ c  prot_dep }};
   <?> MSG #() {{ c  <?> MSG #42; END }};
   END)%proto.

136
Definition prot_dep_del_3 : iProto Σ :=
137 138
  (<!> c : val, MSG c {{ c  prot_dep }};
   <!> y : Z, MSG #y; <?> MSG #() {{ c  <?> MSG #(y + 2); END }};
139 140
   END)%proto.

Robbert Krebbers's avatar
Robbert Krebbers committed
141 142 143 144 145 146 147 148 149
Definition prot_loop_aux (rec : iProto Σ) : iProto Σ :=
  (<!> x : Z, MSG #x; <?> MSG #(x + 2); rec)%proto.
Instance prot_loop_contractive : Contractive prot_loop_aux.
Proof. solve_proto_contractive. Qed.
Definition prot_loop : iProto Σ := fixpoint prot_loop_aux.
Global Instance prot_loop_unfold :
  ProtoUnfold prot_loop (prot_loop_aux prot_loop).
Proof. apply proto_unfold_eq, (fixpoint_unfold _). Qed.

150
Definition prot_fun : iProto Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
151 152 153 154 155 156
  (<!> (P : iProp Σ) (Φ : Z  iProp Σ) (vf : val),
     MSG vf {{ {{{ P }}} vf #() {{{ x, RET #x; Φ x }}} }};
   <?> (vg : val),
     MSG vg {{ {{{ P }}} vg #() {{{ x, RET #(x + 2); Φ x }}} }};
   END)%proto.

157 158 159 160 161 162
Fixpoint prot_lock (n : nat) : iProto Σ :=
  match n with
  | 0 => END
  | S n' => <?> MSG #21; prot_lock n'
  end%proto.

Robbert Krebbers's avatar
Robbert Krebbers committed
163 164 165 166 167 168 169 170 171 172 173
Definition prot_swap : iProto Σ :=
  (<!> x : Z, MSG #x;
   <?> MSG #20;
   <?> MSG #x; END)%proto.

Definition prot_swap_twice : iProto Σ :=
  (<!> x : Z, MSG #x;
   <!> y : Z, MSG #y;
   <?> MSG #20;
   <?> MSG #(x+y); END)%proto.

Robbert Krebbers's avatar
Robbert Krebbers committed
174
(** Specs and proofs of the respective programs *)
175
Lemma prog_spec : {{{ True }}} prog #() {{{ RET #42; True }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
176 177
Proof.
  iIntros (Φ) "_ HΦ". wp_lam.
178
  wp_apply (start_chan_spec prot); iIntros (c) "Hc".
Robbert Krebbers's avatar
Robbert Krebbers committed
179 180 181 182
  - by wp_send with "[]".
  - wp_recv as "_". by iApply "HΦ".
Qed.

183
Lemma prog_ref_spec : {{{ True }}} prog_ref #() {{{ RET #42; True }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
184 185
Proof.
  iIntros (Φ) "_ HΦ". wp_lam.
186
  wp_apply (start_chan_spec prot_ref); iIntros (c) "Hc".
Robbert Krebbers's avatar
Robbert Krebbers committed
187 188 189 190
  - wp_alloc l as "Hl". by wp_send with "[$Hl]".
  - wp_recv (l) as "Hl". wp_load. by iApply "HΦ".
Qed.

191
Lemma prog_del_spec : {{{ True }}} prog_del #() {{{ RET #42; True }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
192 193
Proof.
  iIntros (Φ) "_ HΦ". wp_lam.
194 195 196
  wp_apply (start_chan_spec prot_del); iIntros (c) "Hc".
  - wp_apply (new_chan_spec prot with "[//]").
    iIntros (c2 c2') "[Hc2 Hc2']". wp_send with "[$Hc2]". by wp_send with "[]".
Robbert Krebbers's avatar
Robbert Krebbers committed
197 198 199
  - wp_recv (c2) as "Hc2". wp_recv as "_". by iApply "HΦ".
Qed.

200
Lemma prog_dep_spec : {{{ True }}} prog_dep #() {{{ RET #42; True }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
201 202
Proof.
  iIntros (Φ) "_ HΦ". wp_lam.
203
  wp_apply (start_chan_spec prot_dep); iIntros (c) "Hc".
Robbert Krebbers's avatar
Robbert Krebbers committed
204 205 206 207
  - wp_recv (x) as "_". by wp_send with "[]".
  - wp_send with "[//]". wp_recv as "_". by iApply "HΦ".
Qed.

208
Lemma prog2_ref_spec : {{{ True }}} prog_dep_ref #() {{{ RET #42; True }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
209 210
Proof.
  iIntros (Φ) "_ HΦ". wp_lam.
211
  wp_apply (start_chan_spec prot_dep_ref); iIntros (c) "Hc".
Robbert Krebbers's avatar
Robbert Krebbers committed
212 213 214 215 216
  - wp_recv (l x) as "Hl". wp_load. wp_store. by wp_send with "[Hl]".
  - wp_alloc l as "Hl". wp_send with "[$Hl]". wp_recv as "Hl". wp_load.
    by iApply "HΦ".
Qed.

217
Lemma prog_dep_del_spec : {{{ True }}} prog_dep_del #() {{{ RET #42; True }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
218 219
Proof.
  iIntros (Φ) "_ HΦ". wp_lam.
220 221
  wp_apply (start_chan_spec prot_dep_del); iIntros (c) "Hc".
  - wp_apply (new_chan_spec prot_dep with "[//]"); iIntros (c2 c2') "[Hc2 Hc2']".
Robbert Krebbers's avatar
Robbert Krebbers committed
222 223 224 225 226
    wp_send with "[$Hc2]". wp_recv (x) as "_". by wp_send with "[]".
  - wp_recv (c2) as "Hc2". wp_send with "[//]". wp_recv as "_".
    by iApply "HΦ".
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
227 228 229
Lemma prog_dep_del_2_spec : {{{ True }}} prog_dep_del_2 #() {{{ RET #42; True }}}.
Proof.
  iIntros (Φ) "_ HΦ". wp_lam.
230
  wp_apply (start_chan_spec prot_dep_del_2); iIntros (c) "Hc".
Robbert Krebbers's avatar
Robbert Krebbers committed
231
  { wp_recv (c2) as "Hc2". wp_send with "[//]". by wp_send with "[$Hc2]". }
232
  wp_apply (start_chan_spec prot_dep); iIntros (c2) "Hc2".
Robbert Krebbers's avatar
Robbert Krebbers committed
233 234 235 236
  { wp_recv (x) as "_". by wp_send with "[//]". }
  wp_send with "[$Hc2]". wp_recv as "Hc2". wp_recv as "_". by iApply "HΦ".
Qed.

237 238 239
Lemma prog_dep_del_3_spec : {{{ True }}} prog_dep_del_3 #() {{{ RET #42; True }}}.
Proof.
  iIntros (Φ) "_ HΦ". wp_lam.
240
  wp_apply (start_chan_spec prot_dep_del_3); iIntros (c) "Hc".
241 242
  { wp_recv (c2) as "Hc2". wp_recv (y) as "_".
    wp_send with "[//]". by wp_send with "[$Hc2]". }
243
  wp_apply (start_chan_spec prot_dep); iIntros (c2) "Hc2".
244
  { wp_recv (x) as "_". by wp_send with "[//]". }
245 246
  wp_send with "[$Hc2]". wp_send with "[//]".
  wp_recv as "Hc2". wp_recv as "_". by iApply "HΦ".
247 248
Qed.

Robbert Krebbers's avatar
Fix.  
Robbert Krebbers committed
249
Lemma prog_loop_spec : {{{ True }}} prog_loop #() {{{ RET #42; True }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
250 251
Proof.
  iIntros (Φ) "_ HΦ". wp_lam.
252
  wp_apply (start_chan_spec prot_loop); iIntros (c) "Hc".
Robbert Krebbers's avatar
Robbert Krebbers committed
253 254 255 256 257 258 259 260 261
  - iAssert ( Ψ, WP (rec: "go" <> := let: "x" := recv c in
      send c ("x" + #2) ;; "go" #())%V #() {{ Ψ }})%I with "[Hc]" as "H".
    { iIntros (Ψ). iLöb as "IH". wp_recv (x) as "_". wp_send with "[//]".
      wp_seq. by iApply "IH". }
    wp_lam. wp_closure. wp_let. iApply "H".
  - wp_send with "[//]". wp_recv as "_". wp_send with "[//]". wp_recv as "_".
    wp_pures. by iApply "HΦ".
Qed.

262
Lemma prog_fun_spec : {{{ True }}} prog_fun #() {{{ RET #42; True }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
263 264
Proof.
  iIntros (Φ) "_ HΦ". wp_lam.
265
  wp_apply (start_chan_spec prot_fun); iIntros (c) "Hc".
Robbert Krebbers's avatar
Robbert Krebbers committed
266 267 268 269 270 271 272 273 274 275
  - wp_recv (P Ψ vf) as "#Hf". wp_send with "[]"; last done.
    iIntros "!>" (Ψ') "HP HΨ'". wp_apply ("Hf" with "HP"); iIntros (x) "HΨ".
    wp_pures. by iApply "HΨ'".
  - wp_alloc l as "Hl".
    wp_send ((l  #40)%I (λ w,  w = 40%Z   l  #40)%I) with "[]".
    { iIntros "!>" (Ψ') "Hl HΨ'". wp_load. iApply "HΨ'"; auto. }
    wp_recv (vg) as "#Hg". wp_apply ("Hg" with "Hl"); iIntros (x) "[-> Hl]".
    by iApply "HΦ".
Qed.

276 277 278 279
Lemma prog_lock_spec `{!lockG Σ, contributionG Σ unitUR} :
  {{{ True }}} prog_lock #() {{{ RET #42; True }}}.
Proof.
  iIntros (Φ) "_ HΦ". wp_lam.
280 281
  wp_apply (start_chan_spec (prot_lock 2)); iIntros (c) "Hc".
  - iMod contribution_init as (γ) "Hs".
282 283 284
    iMod (alloc_client with "Hs") as "[Hs Hcl1]".
    iMod (alloc_client with "Hs") as "[Hs Hcl2]".
    wp_apply (newlock_spec nroot ( n, server γ n ε 
Robbert Krebbers's avatar
Robbert Krebbers committed
285
      c  iProto_dual (prot_lock n))%I
286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301
      with "[Hc Hs]"); first by eauto with iFrame.
    iIntros (lk γlk) "#Hlk".
    iAssert ( (client γ ε -
      WP acquire lk;; send c #21;; release lk {{ _, True }}))%I as "#Hhelp".
    { iIntros "!> Hcl".
      wp_apply (acquire_spec with "[$]"); iIntros "[Hl H]".
      iDestruct "H" as (n) "[Hs Hc]".
      iDestruct (server_agree with "Hs Hcl") as %[? _].
      destruct n as [|n]=> //=. wp_send with "[//]".
      iMod (dealloc_client with "Hs Hcl") as "Hs /=".
      wp_apply (release_spec with "[$Hlk $Hl Hc Hs]"); eauto with iFrame. }
    wp_apply (wp_fork with "[Hcl1]").
    { iNext. by iApply "Hhelp". }
    by wp_apply "Hhelp".
  - wp_recv as "_". wp_recv as "_". wp_pures. by iApply "HΦ".
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320

Lemma prog_swap_spec : {{{ True }}} prog_swap #() {{{ RET #42; True }}}.
Proof.
  iIntros (Φ) "_ HΦ". wp_lam.
  wp_apply (start_chan_spec prot_swap); iIntros (c) "Hc".
  - wp_send with "[//]". wp_recv (x) as "_". by wp_send with "[//]".
  - wp_send with "[//]". wp_recv as "_". wp_recv as "_".
    wp_pures. by iApply "HΦ".
Qed.

Lemma prog_swap_twice_spec : {{{ True }}} prog_swap_twice #() {{{ RET #42; True }}}.
Proof.
  iIntros (Φ) "_ HΦ". wp_lam.
  wp_apply (start_chan_spec prot_swap_twice); iIntros (c) "Hc".
  - wp_send with "[//]". wp_recv (x1) as "_". wp_recv (x2) as "_".
    by wp_send with "[//]".
  - wp_send with "[//]". wp_send with "[//]". wp_recv as "_". wp_recv as "_".
    wp_pures. by iApply "HΦ".
Qed.
321
End proofs.