ipm_paper.v 9.44 KB
Newer Older
1
2
3
4
5
(** This file contains the examples from the paper:

Interactive Proofs in Higher-Order Concurrent Separation Logic
Robbert Krebbers, Amin Timany and Lars Birkedal
POPL 2017 *)
6
From iris.proofmode Require Import tactics.
7
From iris.base_logic Require Import base_logic.
8
From iris.deprecated.program_logic Require Import hoare.
9
10
11
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".

12
13
Unset Mangle Names.

14
15
(** The proofs from Section 3.1 *)
Section demo.
16
  Context {M : ucmra}.
17
18
19
20
21
22
23
24
25
26
27
28
29
  Notation iProp := (uPred M).

  (* The version in Coq *)
  Lemma and_exist A (P R: Prop) (Ψ: A  Prop) :
    P  ( a, Ψ a)  R   a, P  Ψ a.
  Proof.
    intros [HP [HΨ HR]].
    destruct HΨ as [x HΨ].
    exists x.
    split. assumption. assumption.
  Qed.

  (* The version in IPM *)
30
  Check "sep_exist".
31
32
33
34
35
  Lemma sep_exist A (P R: iProp) (Ψ: A  iProp) :
    P  ( a, Ψ a)  R   a, Ψ a  P.
  Proof.
    iIntros "[HP [HΨ HR]]".
    iDestruct "HΨ" as (x) "HΨ".
36
37
    iExists x. Show.
    iSplitL "HΨ". Show. iAssumption. Show. iAssumption.
38
39
40
  Qed.

  (* The short version in IPM, as in the paper *)
41
  Check "sep_exist_short".
42
43
  Lemma sep_exist_short A (P R: iProp) (Ψ: A  iProp) :
    P  ( a, Ψ a)  R   a, Ψ a  P.
44
  Proof. iIntros "[HP [HΨ HR]]". Show. iFrame "HP". iAssumption. Qed.
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79

  (* An even shorter version in IPM, using the frame introduction pattern `$` *)
  Lemma sep_exist_shorter A (P R: iProp) (Ψ: A  iProp) :
    P  ( a, Ψ a)  R   a, Ψ a  P.
  Proof. by iIntros "[$ [??]]". Qed.
End demo.

(** The proofs from Section 3.2 *)
(** In the Iris development we often write specifications directly using weakest
preconditions, in sort of `CPS` style, so that they can be applied easier when
proving client code. A version of [list_reverse] in that style can be found in
the file [theories/tests/list_reverse.v]. *)
Section list_reverse.
  Context `{!heapG Σ}.
  Notation iProp := (iProp Σ).
  Implicit Types l : loc.

  Fixpoint is_list (hd : val) (xs : list val) : iProp :=
    match xs with
    | [] => hd = NONEV
    | x :: xs =>  l hd', hd = SOMEV #l  l  (x,hd')  is_list hd' xs
    end%I.

  Definition rev : val :=
    rec: "rev" "hd" "acc" :=
      match: "hd" with
        NONE => "acc"
      | SOME "l" =>
         let: "tmp1" := Fst !"l" in
         let: "tmp2" := Snd !"l" in
         "l" <- ("tmp1", "acc");;
         "rev" "tmp2" "hd"
      end.

  Lemma rev_acc_ht hd acc xs ys :
Gregory Malecha's avatar
Gregory Malecha committed
80
     {{ is_list hd xs  is_list acc ys }} rev hd acc {{ w, is_list w (reverse xs ++ ys) }}.
81
  Proof.
82
    iIntros "!> [Hxs Hys]".
83
84
85
86
    iLöb as "IH" forall (hd acc xs ys). wp_rec; wp_let.
    destruct xs as [|x xs]; iSimplifyEq.
    - (* nil *) by wp_match.
    - (* cons *) iDestruct "Hxs" as (l hd') "(% & Hx & Hxs)"; iSimplifyEq.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
87
      wp_match. wp_load. wp_load. wp_store.
88
89
90
91
92
93
      rewrite reverse_cons -assoc.
      iApply ("IH" $! hd' (InjRV #l) xs (x :: ys) with "Hxs [Hx Hys]").
      iExists l, acc; by iFrame.
  Qed.

  Lemma rev_ht hd xs :
Gregory Malecha's avatar
Gregory Malecha committed
94
     {{ is_list hd xs }} rev hd NONEV {{ w, is_list w (reverse xs) }}.
95
  Proof.
96
    iIntros "!> Hxs". rewrite -(right_id_L [] (++) (reverse xs)).
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
    iApply (rev_acc_ht hd NONEV with "[Hxs]"); simpl; by iFrame.
  Qed.
End list_reverse.

(** The proofs from Section 5 *)
(** This part contains a formalization of the monotone counter, but with an
explicit contruction of the monoid, as we have also done in the proof mode
paper. This should simplify explaining and understanding what is happening.
A version that uses the authoritative monoid and natural number monoid
under max can be found in [theories/heap_lang/lib/counter.v]. *)

(** The invariant rule in the paper is in fact derived from mask changing
update modalities (which we did not cover in the paper). Normally we use these
mask changing update modalities directly in our proofs, but in this file we use
the first prove the rule as a lemma, and then use that. *)
112
Lemma wp_inv_open `{!irisG Λ Σ} N E P e Φ :
Ralf Jung's avatar
Ralf Jung committed
113
  nclose N  E  Atomic WeaklyAtomic e 
114
115
116
  inv N P  ( P - WP e @ E  N {{ v,  P  Φ v }})  WP e @ E {{ Φ }}.
Proof.
  iIntros (??) "[#Hinv Hwp]".
Ralf Jung's avatar
Ralf Jung committed
117
  iMod (inv_acc E N P with "Hinv") as "[HP Hclose]"=>//.
118
119
120
121
122
123
124
125
  iApply wp_wand_r; iSplitL "HP Hwp"; [by iApply "Hwp"|].
  iIntros (v) "[HP $]". by iApply "Hclose".
Qed.

Definition newcounter : val := λ: <>, ref #0.
Definition incr : val :=
  rec: "incr" "l" :=
    let: "n" := !"l" in
126
    if: CAS "l" "n" (#1 + "n") then #() else "incr" "l".
127
128
129
130
131
132
Definition read : val := λ: "l", !"l".

(** The CMRA we need. *)
Inductive M := Auth : nat  M | Frag : nat  M | Bot.

Section M.
Ralf Jung's avatar
Ralf Jung committed
133
134
135
  Local Arguments cmra_op _ !_ !_/.
  Local Arguments op _ _ !_ !_/.
  Local Arguments core _ _ !_/.
136

137
  Canonical Structure M_O : ofe := leibnizO M.
138

139
140
  Local Instance M_valid : Valid M := λ x, x  Bot.
  Local Instance M_op : Op M := λ x y,
141
    match x, y with
142
    | Auth n, Frag j | Frag j, Auth n => if decide (j  n) then Auth n else Bot
143
144
145
    | Frag i, Frag j => Frag (max i j)
    | _, _ => Bot
    end.
146
  Local Instance M_pcore : PCore M := λ x,
147
    Some match x with Auth j | Frag j => Frag j | _ => Bot end.
148
  Local Instance M_unit : Unit M := Frag 0.
149
150
151
152
153
154
155
156
157
158
159
160
161

  Definition M_ra_mixin : RAMixin M.
  Proof.
    apply ra_total_mixin; try solve_proper || eauto.
    - intros [n1|i1|] [n2|i2|] [n3|i3|];
        repeat (simpl; case_decide); f_equal/=; lia.
    - intros [n1|i1|] [n2|i2|]; repeat (simpl; case_decide); f_equal/=; lia.
    - intros [n|i|]; repeat (simpl; case_decide); f_equal/=; lia.
    - by intros [n|i|].
    - intros [n1|i1|] y [[n2|i2|] ?]; exists (core y); simplify_eq/=;
        repeat (simpl; case_decide); f_equal/=; lia.
    - intros [n1|i1|] [n2|i2|]; simpl; by try case_decide.
  Qed.
162
  Canonical Structure M_R : cmra := discreteR M M_ra_mixin.
163

164
  Global Instance M_discrete : CmraDiscrete M_R.
165
166
  Proof. apply discrete_cmra_discrete. Qed.

167
  Definition M_ucmra_mixin : UcmraMixin M.
168
169
170
171
  Proof.
    split; try (done || apply _).
    intros [?|?|]; simpl; try case_decide; f_equal/=; lia.
  Qed.
172
  Canonical Structure M_UR : ucmra := Ucmra M M_ucmra_mixin.
173

174
  Global Instance frag_core_id n : CoreId (Frag n).
175
  Proof. by constructor. Qed.
176
  Lemma auth_frag_valid j n :  (Auth n  Frag j)  j  n.
177
  Proof. simpl. case_decide. done. by intros []. Qed.
178
  Lemma auth_frag_op (j n : nat) : j  n  Auth n = Auth n  Frag j.
179
180
181
182
183
184
185
186
187
188
  Proof. intros. by rewrite /= decide_True. Qed.

  Lemma M_update n : Auth n ~~> Auth (S n).
  Proof.
    apply cmra_discrete_update=>-[m|j|] /= ?; repeat case_decide; done || lia.
  Qed.
End M.

Class counterG Σ := CounterG { counter_tokG :> inG Σ M_UR }.
Definition counterΣ : gFunctors := #[GFunctor (constRF M_UR)].
189
Global Instance subG_counterΣ {Σ} : subG counterΣ Σ  counterG Σ.
190
191
192
193
194
195
196
197
198
199
200
201
202
Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.

Section counter_proof.
  Context `{!heapG Σ, !counterG Σ}.
  Implicit Types l : loc.

  Definition I (γ : gname) (l : loc) : iProp Σ :=
    ( c : nat, l  #c  own γ (Auth c))%I.

  Definition C (l : loc) (n : nat) : iProp Σ :=
    ( N γ, inv N (I γ l)  own γ (Frag n))%I.

  (** The main proofs. *)
203
  Global Instance C_persistent l n : Persistent (C l n).
204
205
206
  Proof. apply _. Qed.

  Lemma newcounter_spec :
Gregory Malecha's avatar
Gregory Malecha committed
207
     {{ True }} newcounter #() {{ v,  l, v = #l  C l 0 }}.
208
  Proof.
209
    iIntros "!> _ /=". rewrite /newcounter /=. wp_lam. wp_alloc l as "Hl".
210
211
212
213
    iMod (own_alloc (Auth 0)) as (γ) "Hγ"; first done.
    rewrite (auth_frag_op 0 0) //; iDestruct "Hγ" as "[Hγ Hγf]".
    set (N:= nroot .@ "counter").
    iMod (inv_alloc N _ (I γ l) with "[Hl Hγ]") as "#?".
214
    { iIntros "!>". iExists 0. by iFrame. }
215
216
217
218
    iModIntro. rewrite /C; eauto 10.
  Qed.

  Lemma incr_spec l n :
Gregory Malecha's avatar
Gregory Malecha committed
219
     {{ C l n }} incr #l {{ v, v = #()  C l (S n) }}.
220
  Proof.
221
    iIntros "!> Hl /=". iLöb as "IH". wp_rec.
222
223
224
    iDestruct "Hl" as (N γ) "[#Hinv Hγf]".
    wp_bind (! _)%E. iApply wp_inv_open; last iFrame "Hinv"; auto.
    iDestruct 1 as (c) "[Hl Hγ]".
225
    wp_load. iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
226
    wp_let. wp_op.
Ralf Jung's avatar
Ralf Jung committed
227
    wp_bind (CmpXchg _ _ _). iApply wp_inv_open; last iFrame "Hinv"; auto.
228
229
230
231
232
233
    iDestruct 1 as (c') ">[Hl Hγ]".
    destruct (decide (c' = c)) as [->|].
    - iCombine "Hγ" "Hγf" as "Hγ".
      iDestruct (own_valid with "Hγ") as %?%auth_frag_valid; rewrite -auth_frag_op //.
      iMod (own_update with "Hγ") as "Hγ"; first apply M_update.
      rewrite (auth_frag_op (S n) (S c)); last lia; iDestruct "Hγ" as "[Hγ Hγf]".
234
      wp_cmpxchg_suc. iModIntro. iSplitL "Hl Hγ".
235
      { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
236
      wp_pures. rewrite {3}/C; eauto 10.
237
    - wp_cmpxchg_fail; first (intros [=]; abstract lia).
238
      iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
239
      wp_pures. iApply ("IH" with "[Hγf]"). rewrite {3}/C; eauto 10.
240
241
  Qed.

242
  Check "read_spec".
243
  Lemma read_spec l n :
Gregory Malecha's avatar
Gregory Malecha committed
244
     {{ C l n }} read #l {{ v,  m : nat, v = #m  n  m  C l m }}.
245
  Proof.
246
    iIntros "!> Hl /=". iDestruct "Hl" as (N γ) "[#Hinv Hγf]".
247
    rewrite /read /=. wp_lam. Show. iApply wp_inv_open; last iFrame "Hinv"; auto.
248
    iDestruct 1 as (c) "[Hl Hγ]". wp_load. Show.
249
250
251
    iDestruct (own_valid γ (Frag n  Auth c) with "[-]") as % ?%auth_frag_valid.
    { iApply own_op. by iFrame. }
    rewrite (auth_frag_op c c); last lia; iDestruct "Hγ" as "[Hγ Hγf']".
252
    iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
253
    rewrite /C; eauto 10 with lia.
254
255
  Qed.
End counter_proof.