ipm_paper.v 9.34 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 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27
From iris.program_logic Require Export hoare.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".

(** The proofs from Section 3.1 *)
Section demo.
  Context {M : ucmraT}.
  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 *)
28
  Check "sep_exist".
29 30 31 32 33
  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Ψ".
34 35
    iExists x. Show.
    iSplitL "HΨ". Show. iAssumption. Show. iAssumption.
36 37 38
  Qed.

  (* The short version in IPM, as in the paper *)
39
  Check "sep_exist_short".
40 41
  Lemma sep_exist_short A (P R: iProp) (Ψ: A  iProp) :
    P  ( a, Ψ a)  R   a, Ψ a  P.
42
  Proof. iIntros "[HP [HΨ HR]]". Show. iFrame "HP". iAssumption. Qed.
43 44 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 80 81 82 83 84

  (* 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 :
    {{ is_list hd xs  is_list acc ys }} rev hd acc {{ w, is_list w (reverse xs ++ ys) }}.
  Proof.
    iIntros "!# [Hxs Hys]".
    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
85
      wp_match. wp_load. wp_load. wp_store.
86 87 88 89 90 91
      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 :
92
    {{ is_list hd xs }} rev hd NONEV {{ w, is_list w (reverse xs) }}.
93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109
  Proof.
    iIntros "!# Hxs". rewrite -(right_id_L [] (++) (reverse xs)).
    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. *)
110
Lemma wp_inv_open `{!irisG Λ Σ} N E P e Φ :
111
  nclose N  E  Atomic WeaklyAtomic e 
112 113 114 115 116 117 118 119 120 121 122 123
  inv N P  ( P - WP e @ E  N {{ v,  P  Φ v }})  WP e @ E {{ Φ }}.
Proof.
  iIntros (??) "[#Hinv Hwp]".
  iMod (inv_open E N P with "Hinv") as "[HP Hclose]"=>//.
  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
124
    if: CAS "l" "n" (#1 + "n") then #() else "incr" "l".
125 126 127 128 129 130 131 132 133 134
Definition read : val := λ: "l", !"l".

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

Section M.
  Arguments cmra_op _ !_ !_/.
  Arguments op _ _ !_ !_/.
  Arguments core _ _ !_/.

135
  Canonical Structure M_O : ofeT := leibnizO M.
136 137 138 139 140 141 142 143 144 145

  Instance M_valid : Valid M := λ x, x  Bot.
  Instance M_op : Op M := λ x y,
    match x, y with
    | Auth n, Frag j | Frag j, Auth n => if decide (j  n)%nat then Auth n else Bot
    | Frag i, Frag j => Frag (max i j)
    | _, _ => Bot
    end.
  Instance M_pcore : PCore M := λ x,
    Some match x with Auth j | Frag j => Frag j | _ => Bot end.
Robbert Krebbers's avatar
Robbert Krebbers committed
146
  Instance M_unit : Unit M := Frag 0.
147 148 149 150 151 152 153 154 155 156 157 158 159 160

  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.
  Canonical Structure M_R : cmraT := discreteR M M_ra_mixin.
161

162
  Global Instance M_discrete : CmraDiscrete M_R.
163 164
  Proof. apply discrete_cmra_discrete. Qed.

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

172
  Global Instance frag_core_id n : CoreId (Frag n).
173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200
  Proof. by constructor. Qed.
  Lemma auth_frag_valid j n :  (Auth n  Frag j)  (j  n)%nat.
  Proof. simpl. case_decide. done. by intros []. Qed.
  Lemma auth_frag_op (j n : nat) : (j  n)%nat  Auth n = Auth n  Frag j.
  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)].
Instance subG_counterΣ {Σ} : subG counterΣ Σ  counterG Σ.
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. *)
201
  Global Instance C_persistent l n : Persistent (C l n).
202 203 204 205 206
  Proof. apply _. Qed.

  Lemma newcounter_spec :
    {{ True }} newcounter #() {{ v,  l, v = #l  C l 0 }}.
  Proof.
207
    iIntros "!# _ /=". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224
    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 "#?".
    { iIntros "!>". iExists 0%nat. by iFrame. }
    iModIntro. rewrite /C; eauto 10.
  Qed.

  Lemma incr_spec l n :
    {{ C l n }} incr #l {{ v, v = #()  C l (S n) }}.
  Proof.
    iIntros "!# Hl /=". iLöb as "IH". wp_rec.
    iDestruct "Hl" as (N γ) "[#Hinv Hγf]".
    wp_bind (! _)%E. iApply wp_inv_open; last iFrame "Hinv"; auto.
    iDestruct 1 as (c) "[Hl Hγ]".
    wp_load. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
    wp_let. wp_op.
225
    wp_bind (CmpXchg _ _ _). iApply wp_inv_open; last iFrame "Hinv"; auto.
226 227 228 229 230 231
    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]".
232
      wp_cmpxchg_suc. iSplitL "Hl Hγ".
233
      { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
234
      wp_pures. rewrite {3}/C; eauto 10.
235
    - wp_cmpxchg_fail; first (intros [=]; abstract omega).
236
      iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
237
      wp_pures. iApply ("IH" with "[Hγf]"). rewrite {3}/C; eauto 10.
238 239
  Qed.

240
  Check "read_spec".
241 242 243 244
  Lemma read_spec l n :
    {{ C l n }} read #l {{ v,  m : nat, v = #m  n  m  C l m }}.
  Proof.
    iIntros "!# Hl /=". iDestruct "Hl" as (N γ) "[#Hinv Hγf]".
245
    rewrite /read /=. wp_lam. Show. iApply wp_inv_open; last iFrame "Hinv"; auto.
246
    iDestruct 1 as (c) "[Hl Hγ]". wp_load. Show.
247 248 249 250 251 252 253
    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']".
    iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
    rewrite /C; eauto 10 with omega.
  Qed.
End counter_proof.