basics.v 5.09 KB
Newer Older
1
2
3
(** This file includes basic examples that each
encapsulate a feature of the Dependent Separation Protocols.
*)
Robbert Krebbers's avatar
Robbert Krebbers committed
4
From actris.channel Require Import proto_channel proofmode.
5
6
From iris.heap_lang Require Import proofmode notation lib.spin_lock.
From actris.utils Require Import contribution.
Robbert Krebbers's avatar
Robbert Krebbers committed
7

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

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

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

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

33
(** Higher-Order *)
Robbert Krebbers's avatar
Robbert Krebbers committed
34
35
36
37
38
39
40
Definition prog5 : val := λ: <>,
  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" #().

41
(** Locks *)
42
43
44
45
46
47
48
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
49
50
51
Section proofs.
Context `{heapG Σ, proto_chanG Σ}.

52
(** Protocols for their respective programs *)
Robbert Krebbers's avatar
Robbert Krebbers committed
53
54
55
56
57
58
59
Definition prot1 : iProto Σ :=
  (<?> MSG #42; END)%proto.

Definition prot2 : iProto Σ :=
  (<?> l : loc, MSG #l {{ l  #42 }}; END)%proto.

Definition prot3 : iProto Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
60
  (<?> c : val, MSG c {{ c  prot1 }}; END)%proto.
Robbert Krebbers's avatar
Robbert Krebbers committed
61
62
63
64
65
66
67
68
69
70
71

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

Definition prot5 : iProto Σ :=
  (<!> (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.

72
73
74
75
76
77
Fixpoint prot_lock (n : nat) : iProto Σ :=
  match n with
  | 0 => END
  | S n' => <?> MSG #21; prot_lock n'
  end%proto.

78
(** Specs and proofs of their respective programs *)
Robbert Krebbers's avatar
Robbert Krebbers committed
79
80
81
Lemma prog1_spec : {{{ True }}} prog1 #() {{{ RET #42; True }}}.
Proof.
  iIntros (Φ) "_ HΦ". wp_lam.
Robbert Krebbers's avatar
Robbert Krebbers committed
82
  wp_apply (start_chan_proto_spec prot1); iIntros (c) "Hc".
Robbert Krebbers's avatar
Robbert Krebbers committed
83
84
85
86
87
88
89
  - by wp_send with "[]".
  - wp_recv as "_". by iApply "HΦ".
Qed.

Lemma prog2_spec : {{{ True }}} prog2 #() {{{ RET #42; True }}}.
Proof.
  iIntros (Φ) "_ HΦ". wp_lam.
Robbert Krebbers's avatar
Robbert Krebbers committed
90
  wp_apply (start_chan_proto_spec prot2); iIntros (c) "Hc".
Robbert Krebbers's avatar
Robbert Krebbers committed
91
92
93
94
95
96
97
  - wp_alloc l as "Hl". by wp_send with "[$Hl]".
  - wp_recv (l) as "Hl". wp_load. by iApply "HΦ".
Qed.

Lemma prog3_spec : {{{ True }}} prog3 #() {{{ RET #42; True }}}.
Proof.
  iIntros (Φ) "_ HΦ". wp_lam.
Robbert Krebbers's avatar
Robbert Krebbers committed
98
99
  wp_apply (start_chan_proto_spec prot3); iIntros (c) "Hc".
  - wp_apply (new_chan_proto_spec with "[//]").
Robbert Krebbers's avatar
Robbert Krebbers committed
100
101
102
103
104
105
106
107
    iIntros (c2 c2') "Hcc2". iMod ("Hcc2" $! prot1) as "[Hc2 Hc2']".
    wp_send with "[$Hc2]". by wp_send with "[]".
  - wp_recv (c2) as "Hc2". wp_recv as "_". by iApply "HΦ".
Qed.

Lemma prog4_spec : {{{ True }}} prog4 #() {{{ RET #42; True }}}.
Proof.
  iIntros (Φ) "_ HΦ". wp_lam.
Robbert Krebbers's avatar
Robbert Krebbers committed
108
  wp_apply (start_chan_proto_spec prot4); iIntros (c) "Hc".
Robbert Krebbers's avatar
Robbert Krebbers committed
109
110
111
112
113
114
115
  - wp_recv (x) as "_". by wp_send with "[]".
  - wp_send with "[//]". wp_recv as "_". by iApply "HΦ".
Qed.

Lemma prog5_spec : {{{ True }}} prog5 #() {{{ RET #42; True }}}.
Proof.
  iIntros (Φ) "_ HΦ". wp_lam.
Robbert Krebbers's avatar
Robbert Krebbers committed
116
  wp_apply (start_chan_proto_spec prot5); iIntros (c) "Hc".
Robbert Krebbers's avatar
Robbert Krebbers committed
117
118
119
120
121
122
123
124
125
126
  - 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.

127
128
129
130
Lemma prog_lock_spec `{!lockG Σ, contributionG Σ unitUR} :
  {{{ True }}} prog_lock #() {{{ RET #42; True }}}.
Proof.
  iIntros (Φ) "_ HΦ". wp_lam.
Robbert Krebbers's avatar
Robbert Krebbers committed
131
  wp_apply (start_chan_proto_spec (prot_lock 2)); iIntros (c) "Hc".
132
133
134
135
  - iMod (contribution_init) as (γ) "Hs".
    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
136
      c  iProto_dual (prot_lock n))%I
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
      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.
End proofs.