ipm_paper.v 9.34 KB
 Robbert Krebbers committed Jun 01, 2018 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 *) `````` Robbert Krebbers committed Jan 17, 2017 6 ``````From iris.proofmode Require Import tactics. `````` Jacques-Henri Jourdan committed Sep 13, 2019 7 ``````From iris.base_logic Require Import base_logic. `````` Robbert Krebbers committed Jan 17, 2017 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 *) `````` Ralf Jung committed Jul 04, 2018 28 `````` Check "sep_exist". `````` Robbert Krebbers committed Jan 17, 2017 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Ψ". `````` Ralf Jung committed Jun 01, 2018 34 35 `````` iExists x. Show. iSplitL "HΨ". Show. iAssumption. Show. iAssumption. `````` Robbert Krebbers committed Jan 17, 2017 36 37 38 `````` Qed. (* The short version in IPM, as in the paper *) `````` Ralf Jung committed Jul 04, 2018 39 `````` Check "sep_exist_short". `````` Robbert Krebbers committed Jan 17, 2017 40 41 `````` Lemma sep_exist_short A (P R: iProp) (Ψ: A → iProp) : P ∗ (∃ a, Ψ a) ∗ R ⊢ ∃ a, Ψ a ∗ P. `````` Ralf Jung committed Jun 01, 2018 42 `````` Proof. iIntros "[HP [HΨ HR]]". Show. iFrame "HP". iAssumption. Qed. `````` Robbert Krebbers committed Jan 17, 2017 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 committed Oct 29, 2018 85 `````` wp_match. wp_load. wp_load. wp_store. `````` Robbert Krebbers committed Jan 17, 2017 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 : `````` Jacques-Henri Jourdan committed Oct 29, 2018 92 `````` {{ is_list hd xs }} rev hd NONEV {{ w, is_list w (reverse xs) }}. `````` Robbert Krebbers committed Jan 17, 2017 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. *) `````` Ralf Jung committed Mar 05, 2019 110 ``````Lemma wp_inv_open `{!irisG Λ Σ} N E P e Φ : `````` Ralf Jung committed Dec 07, 2017 111 `````` nclose N ⊆ E → Atomic WeaklyAtomic e → `````` Robbert Krebbers committed Jan 17, 2017 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 `````` Ralf Jung committed Jun 24, 2019 124 `````` if: CAS "l" "n" (#1 + "n") then #() else "incr" "l". `````` Robbert Krebbers committed Jan 17, 2017 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 _ _ !_/. `````` Robbert Krebbers committed Jun 16, 2019 135 `````` Canonical Structure M_O : ofeT := leibnizO M. `````` Robbert Krebbers committed Jan 17, 2017 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 committed Sep 17, 2017 146 `````` Instance M_unit : Unit M := Frag 0. `````` Robbert Krebbers committed Jan 17, 2017 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. `````` Robbert Krebbers committed Feb 09, 2017 161 `````` `````` Robbert Krebbers committed Oct 25, 2017 162 `````` Global Instance M_discrete : CmraDiscrete M_R. `````` Robbert Krebbers committed Feb 09, 2017 163 164 `````` Proof. apply discrete_cmra_discrete. Qed. `````` Robbert Krebbers committed Oct 25, 2017 165 `````` Definition M_ucmra_mixin : UcmraMixin M. `````` Robbert Krebbers committed Jan 17, 2017 166 167 168 169 `````` Proof. split; try (done || apply _). intros [?|?|]; simpl; try case_decide; f_equal/=; lia. Qed. `````` Robbert Krebbers committed Oct 25, 2017 170 `````` Canonical Structure M_UR : ucmraT := UcmraT M M_ucmra_mixin. `````` Robbert Krebbers committed Jan 17, 2017 171 `````` `````` Robbert Krebbers committed Oct 25, 2017 172 `````` Global Instance frag_core_id n : CoreId (Frag n). `````` Robbert Krebbers committed Jan 17, 2017 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. *) `````` Robbert Krebbers committed Oct 25, 2017 201 `````` Global Instance C_persistent l n : Persistent (C l n). `````` Robbert Krebbers committed Jan 17, 2017 202 203 204 205 206 `````` Proof. apply _. Qed. Lemma newcounter_spec : {{ True }} newcounter #() {{ v, ∃ l, ⌜v = #l⌝ ∧ C l 0 }}. Proof. `````` Jacques-Henri Jourdan committed Oct 29, 2018 207 `````` iIntros "!# _ /=". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl". `````` Robbert Krebbers committed Jan 17, 2017 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. `````` Ralf Jung committed Jun 24, 2019 225 `````` wp_bind (CmpXchg _ _ _). iApply wp_inv_open; last iFrame "Hinv"; auto. `````` Robbert Krebbers committed Jan 17, 2017 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]". `````` Ralf Jung committed Jun 24, 2019 232 `````` wp_cmpxchg_suc. iSplitL "Hl Hγ". `````` Robbert Krebbers committed Jan 17, 2017 233 `````` { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. } `````` Ralf Jung committed Jun 24, 2019 234 `````` wp_pures. rewrite {3}/C; eauto 10. `````` Ralf Jung committed Jun 24, 2019 235 `````` - wp_cmpxchg_fail; first (intros [=]; abstract omega). `````` Robbert Krebbers committed Jan 17, 2017 236 `````` iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|]. `````` Ralf Jung committed Jun 24, 2019 237 `````` wp_pures. iApply ("IH" with "[Hγf]"). rewrite {3}/C; eauto 10. `````` Robbert Krebbers committed Jan 17, 2017 238 239 `````` Qed. `````` Ralf Jung committed Jul 04, 2018 240 `````` Check "read_spec". `````` Robbert Krebbers committed Jan 17, 2017 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]". `````` Jacques-Henri Jourdan committed Oct 29, 2018 245 `````` rewrite /read /=. wp_lam. Show. iApply wp_inv_open; last iFrame "Hinv"; auto. `````` Ralf Jung committed Jun 01, 2018 246 `````` iDestruct 1 as (c) "[Hl Hγ]". wp_load. Show. `````` Robbert Krebbers committed Jan 17, 2017 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.``````