coq_intro_example_2.v 28.7 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31
(* In this file we explain how to do prove the counter specifications from
   Section 7.7 of the notes. This involves construction and manipulation of
   resource algebras, the explanation of which is the focus of this file. We
   assume the reader has experimented with coq-intro-example-1.v example, and
   thus we do not explain the features we have explained therein already. *)

From iris.program_logic Require Export weakestpre.
From iris.base_logic.lib Require Export invariants.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode.
From iris.heap_lang Require Import notation lang.

From iris.heap_lang.lib Require Import par.

(* The counter module definition. *)
Definition read : val := λ: "c", !"c".
Definition incr : val := rec: "incr" "c" := let: "n" := !"c" in
                                            let: "m" := #1 + "n" in
                                            if: CAS "c" "n" "m" then #() else "incr" "c".

Definition newCounter : val := λ: <>, ref #0.

Section monotone_counter.
  (* For the first example we will only give the weaker specification, as we did
     in the notes. In this specification we only know the lower bound on the
     counter value, since the isCounter predicate is freely duplicable.

     Before we start with the actual verification we will define the resource
     algebra we shall be using. The Iris library contains all the ingredients
     needed to compose this particular resource algebra from simpler components,
     however to illustrate how to define our own we will define it from scratch.
32

33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61
     In the subsequent section we show how to obtain an equivalent resource
     algebra from the building blocks provided by the Iris Coq library. 
  *)

  (* The carrier of our resource algebra is the set ℕ_{⊥,⊤} × ℕ. NBT (Natural
     numbers with Top and Bottom) is the first component of this product. *)
  Inductive NBT :=
    Bot : NBT (* Bottom *)
  | Top : NBT (* Top *)
  | NBT_incl : nat  NBT. (* Inclusion of natural numbers into our new type. *)

  (* The carrier of our RA. *)
  Definition mcounterRAT : Type := NBT * nat.

  (* The notion of a resource algebra as used in Iris is more general than the one
     currently described. It is called a cmra (standing roughly for complete
     metric resource algebra). For most verification purposes it is not
     important what that is. It is a step-indexed generalization of the resource
     algebra we have described in Section 7. The main difference is that the
     carrier is not simply a set, but comes equipped with a set of equivalence
     relations indexed by natural numbers (the "step-indices").

     The notion we have defined in Section 7 is that of a "discrete" CMRA. There
     is special support in the library for such CMRAs, and that is why in the
     remainder of this file we will often use, e.g., special lemmas for discrete
     CMRAs. 
   *)

  (* 
62
     To tell Coq we wish to use such a discrete CMRA we use the constructor leibnizO.
63 64 65 66
     This takes a Coq type and makes it an instance of an OFE (a step-indexed generalization of sets).
     This is not the place do describe Canonical Structures.
     A very good introduction is available at https://hal.inria.fr/hal-00816703v1/document 
  *)
67
  Canonical Structure mcounterRAC := leibnizO mcounterRAT.
68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 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 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317

  (* To make the type mcounterRAT into an RA we need an operation. This is
     defined in the standard way, except we use the typeclass Op so we can reuse
     a lot of the notation mechanism (we can write x ⋅ y for the operation), and
     some other infrastucture and generic lemmas. *)
  Instance mcounterRAop : Op mcounterRAT :=
    λ p p,
    let (x, n) := p in 
    let (y, m) := p in
    match x with
      Bot => (y, max n m)
    | _ => match y with
             Bot => (x, max n m)
           | _ => (Top, max n m)
           end
    end.

  (* The set of valid elements. Valid A is simply abbreviation for A → Prop,
     i.e., for the set of subsets of A. Importantly Valid is a typeclass, and
     thus we make our definition an instance of it. This will enable the Coq
     typeclass search and various interactive proof mode tactics automatically
     deal with many boring use cases. *)
  Instance mcounterRAValid : Valid mcounterRAT :=
    λ x, match x with
           (Bot, _) => True
         | (NBT_incl x, m) => x  m
         | _ => False
         end.

  (* The core of the RA. PCore stands for "partial core", and is an abbreviation
     for a partial function, which in Coq is encoded as a function from A →
     option A. Again, PCore is a typeclass for better automation support, and
     thus our definition is an instance. *)
  Instance mcounterRACore : PCore mcounterRAT :=
    λ x, let (_, n) := x in Some (Bot, n).

  (* We can then package these definitions up into an RA structure, used by the
     Iris library. *)

  (* We need these auxiliary lemmas in the proof below. 
     We need the type  annotation to guide the type inference. *)
  Lemma mcounterRA_op_second (x y : NBT) n m:  z, ((x, n) : mcounterRAT)  (y, m) = (z, max n m).
  Proof.
    destruct x as [], y as []; eexists; unfold op, mcounterRAop; simpl; auto.
  Qed.
  
  Lemma mcounterRA_included_aux x y (n m : nat): ((x, n) : mcounterRAT)  (y, m)  (n  m)%nat.
  Proof.
    intros [[z k] [=H]].
    revert H.
    destruct (mcounterRA_op_second x z n k) as [? ->].
    inversion 1; subst; auto with arith.
  Qed.

  Lemma mcounterRA_included_frag (n m : nat): ((Bot, n) : mcounterRAT)  (Bot, m)  (n  m)%nat.
  Proof.
    split.
    - apply mcounterRA_included_aux.
    - intros H%Max.max_r; exists (Bot, m); unfold op, mcounterRAop; rewrite H; auto.
  Qed.

  Lemma mcounterRA_valid x (n : nat):  ((NBT_incl x, n) : mcounterRAT)  (n  x)%nat.
  Proof.
    split; auto.
  Qed.

  (* An RAMixin is a structure which combines all the parts of an RA into one
     Coq structure, together with all the properties that the operations and
     functions satisfy. *)
  Definition mcounterRA_mixin : RAMixin mcounterRAT.
  Proof.
    split; try apply _; try done.
    unfold valid, op, mcounterRAop, mcounterRAValid. intros ? ? cx -> ?; exists cx. done.
    (* The operation is associative. *)
    - unfold op, mcounterRAop. intros [[]] [[]] [[]]; rewrite !Nat.max_assoc; reflexivity.
    (* The operation is commutative. *)
    - unfold op, mcounterRAop. intros [[]] [[]]; rewrite Nat.max_comm; reflexivity.
    (* Core axioms. *)
    - unfold pcore, mcounterRACore, op, mcounterRAop; intros [[]] [[]] [=->]; rewrite Max.max_idempotent; auto.
    - unfold pcore, mcounterRACore, op, mcounterRAop; intros [[]] [[]] [=->]; auto.
    - unfold pcore, mcounterRACore, op, mcounterRAop. 
      intros [x n] [y m] cx Hleq%mcounterRA_included_aux [=<-].
      exists (Bot, m); split; first auto.
      by apply mcounterRA_included_frag.
    - (* Validity axiom: validity is down-closed with respect to the extension order. *)
      intros [[]].
      + reflexivity.
      + unfold op, mcounterRAop; intros [[]] [].
      + unfold op, mcounterRAop; intros [[]].
        * rewrite !mcounterRA_valid. eauto with arith.
        * intros [].
        * intros [].
  Qed.

  (* We finally wrap the type and the above mixin and make the structure
  available for typeclass search. The discreteR is a wrapper for when our CMRA is
  "discrete" as described above. *)
  Canonical Structure mcounterRA := discreteR mcounterRAT mcounterRA_mixin.

  (* Some tactics and lemmas only apply for discrete CMRAs (what we called RAs).
     To be able to use these we need to register our CMRA as a discrete one, to
     make this information available to typeclass search. *) 
  Instance mcounterRA_cmra_discrete : CmraDiscrete mcounterRA.
  Proof. apply discrete_cmra_discrete. Qed.

  (* A total CMRA (or RA) is the one where the core operation is a total
     function, i.e., the core of every element is defined. Some properties and
     lemmas only apply for such CMRAs, and so we register the fact that our CMRA
     is of this form.
   *)
  Instance mcounterRA_cmra_total : CmraTotal mcounterRA.
  Proof. intros [[]]; eauto. Qed.

  (* We define some abbreviation. We only define it as notation in this section
     since the same notation is already defined for the general authoritative RA
     construction in the Iris Coq library. 
   *)
  Local Notation "◯ n" := ((Bot, n%nat) : mcounterRA) (at level 20).
  Local Notation "● m" := ((NBT_incl m%nat, 0%nat) : mcounterRA) (at level 20).

  (* We now prove the three properties we claim were required from the resource
     algebra in Section 7.7. 
   *)
  (* CoreId x states that the core of x is x, which is one of the properties we claimed for the
     fragments. CoreId is a typeclass. *)
  Instance mcounterRA_frag_core (n : nat): CoreId ( n).
  Proof.
    rewrite /CoreId; reflexivity.
  Qed.

  Lemma mcounterRA_valid_auth_frag m n:  ( m   n)  (n  m)%nat.
  Proof.
    apply mcounterRA_valid.
  Qed.

  Lemma mcounterRA_update m n: (( m   n) : mcounterRA) ~~> ( (1 + m)   (1 + n)).
  Proof.
    (* Use the specialized definition of update, since our RA is a nice one. *)
    apply cmra_discrete_update.
    intros [[] k].
    - rewrite /op /cmra_op !mcounterRA_valid; lia.
    - intros [].
    - intros [].
  Qed.

  (* We now need to tell Coq to use our RA as one of the RA's in the instantiation of Iris. *)
  (* This is achieved via the subG constructor. All of this is boilerplate, so
     the proofs are trivial, with the tactics provided by the library. *)
  Class mcounterG Σ := MCounterG { mcounter_inG :> inG Σ mcounterRA }.
  Definition mcounterΣ : gFunctors := #[GFunctor mcounterRA].
  
  Instance subG_mcounterΣ {Σ} : subG mcounterΣ Σ  mcounterG Σ.
  Proof. solve_inG. Qed.

  (* We can now verify the programs. *)
  (* We start off as in the previous example, with some boilerplate code. *)
  Context `{!heapG Σ, !mcounterG Σ} (N : namespace).
  Notation iProp := (iProp Σ).

  (* The counter invariant as defined in the notes. The only difference is that
     we are using the namespace N for the invariant, instead of existentially
     quantifying the invariant name. *)
  Definition counter_inv ( : loc) (γ : gname) : iProp := ( (m : nat),   #m  own γ ( m))%I.

  (* the isCounter predicate as in the notes. *)
  Definition isCounter ( : loc) (n : nat) : iProp :=
    ( γ, own γ ( n)  inv N (counter_inv  γ))%I.

  (* isCounter is a persistent predicate. This is needed so we can share it among threads. *)
  (* We first need an auxiliary lemma, which tells Coq that ownership of fragments is persistent.
     This follows from the persistently-core axiom of the logic.
     Instead of proving this as a lemma we make it an instance of the Persistent class.
     This way Coq will be able to infer automatically whenever it needs the fact
     that ownership of fragments is persistent.
   *)
  Instance ownFrac_persistent γ n: Persistent (own γ ( n)).
  Proof.
   apply own_core_persistent, _.
  Qed.

  (* Now the proof of the main counter predicate is simple: Coq's typeclass
     search can automatically deduce that isCounter is persistent. It knows the
     closure properties of persistent propositions, e.g., existential
     quantification over a persistent predicate is persistent, and it knows that
     invariants are persistent. The final part it needs is that own γ (◯ n) is
     persistent, and we have just taught it that in the preceding lemma. *)
  Instance isCounter_persistent  n: Persistent (isCounter  n).
  Proof.
    apply _.
  Qed.

  (* We can now perform the main proofs. They are not very different from the
     proofs we have done previously. *) 
  Lemma newCounter_spec: {{{ True }}} newCounter #() {{{ v, RET #v; isCounter v 0 }}}.
  Proof.
    iIntros (Φ) "_ HCont".
    rewrite /newCounter -wp_fupd. (* See comment below for why we used wp_fupd. *)
    wp_lam.
    (* We allocate ghost state using the rule/lemma own_alloc. Since the
       conclusion of the rule is under a modality we wrap the application of
       this lemma with the call to the iMod tactic, which takes care of the
       bookkeeping, using the primitive rules of the modality. 
       In this case the tactic knows that |==> WP ... implies WP ... and thus removes it from the goal.
     *)
    iMod (own_alloc ( 0   0)) as (γ) "[HAuth HFrac]".
    - apply mcounterRA_valid_auth_frag; auto. (* NOTE: We use the validity property of the RA we have constructed. *)
    - wp_alloc  as "Hpt".
      (* We now allocate an invariant. For this it is crucial we have used the
         wp_fupd lemma above to have the Φ under a modality. Otherwise we would
         have been stuck here, since allocating an invariant is only possible
         under the fancy update modality. *)
      iMod (inv_alloc N _ (counter_inv  γ) with "[Hpt HAuth]") as "HInv".
      + iExists 0%nat; iFrame.
      + iApply ("HCont" with "[HFrac HInv]").
        iExists γ; iFrame.
  Qed.
  
  (* The read method specification. *)
  Lemma read_spec  n: {{{ isCounter  n }}} read # {{{ m, RET #m; n  m%nat }}}.
  Proof.
    iIntros (Φ) "HCounter HCont".
    iDestruct "HCounter" as (γ) "[HOwnFrag HInv]".
    rewrite /read.
    wp_lam.
    iInv N as (m) ">[Hpt HOwnAuth]" "HClose".
    wp_load.
    (* NOTE: We use the validity property of the RA we have constructed. From the fact that we own 
             ◯ n and ● m to conclude that n ≤ m. *)
    iDestruct (@own_valid_2 _ _ _ γ with "HOwnAuth HOwnFrag") as %H%mcounterRA_valid_auth_frag. 
    iMod ("HClose" with "[Hpt HOwnAuth]") as "_".
    { iNext; iExists m; iFrame. }
    iModIntro.
    iApply "HCont"; done.
  Qed.

  (* The read method specification. *)
  Lemma incr_spec  n: {{{ isCounter  n }}} incr # {{{ RET #(); isCounter  (1 + n)%nat }}}.
  Proof.
    iIntros (Φ) "HCounter HCont".
    iDestruct "HCounter" as (γ) "[HOwnFrag #HInv]".
    iLöb as "IH".
    rewrite /incr.
    wp_lam.
    wp_bind (! _)%E.
    iInv N as (m) ">[Hpt HOwnAuth]" "HClose".
    wp_load.
    iDestruct (@own_valid_2 _ _ _ γ with "HOwnAuth HOwnFrag") as %H%mcounterRA_valid_auth_frag.
    iMod ("HClose" with "[Hpt HOwnAuth]") as "_".
    { iNext; iExists m; iFrame. }
    iModIntro.
318
    wp_let; wp_op; wp_let.
319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334
    wp_bind (CAS _ _ _)%E.
    iInv N as (k) ">[Hpt HOwnAuth]" "HClose".
    destruct (decide (k = m)); subst.
    + wp_cas_suc.
      (* If the CAS succeeds we need to update our ghost state. This is achieved using the own_update rule/lemma.
         The arguments are the ghost name and the ghost resources x from which and to which we are updating.
         Finally we need to give up own γ x to get ownership of the new resources.
         We do this using the "with ..." syntax.
         Again, the conclusion of the update rule is under the update modality,
         and thus we wrap the application of the lemma with the iMod tactic. *)
      iMod (own_update γ (( m   n) : mcounterRA) ( (1 + m)   (1 + n)) with "[HOwnFrag HOwnAuth]") as "[HOwnAuth HOwnFrag]".
      { apply mcounterRA_update. } (* We need the final property of the RA we proved above: the frame preserving update from (● m ⋅ ◯ n) to (● (1 + m) ⋅ ◯ (1 + n)). *)
      { rewrite own_op; iFrame. }
      iMod ("HClose" with "[Hpt HOwnAuth]") as "_".
      { iNext; iExists (1 + m)%nat.
        rewrite Nat2Z.inj_succ Z.add_1_l; iFrame. }
335
      iModIntro; wp_if; iApply ("HCont" with "[HInv HOwnFrag]").
336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379
      iExists γ; iFrame "#"; iFrame.
    + wp_cas_fail; first intros ?; simplify_eq.
      iMod ("HClose" with "[Hpt HOwnAuth]") as "_".
      - iExists k; iFrame.
      - iModIntro; wp_if.
        iApply ("IH" with "HOwnFrag HCont"); iFrame.
  Qed.
End monotone_counter.

(* In the preceding section we spent a lot of time defining our own resource
   algebra and proving it satisfies all the needed properties. The same patterns
   appear often in proof development, and thus the iris Coq library provides
   several building blocks for constructing resource algebras.

   In the following section we repeat the above specification, but with a
   resource algebra constructed using these building blocks. We will see that
   this will save us quite a bit of work.

   As we stated in an exercise in the counter modules section of the lecture
   notes, the resource algebra we constructed above is nothing but Auth(N_max).
   Auth and N_max are both part of the iris Coq library. They are called authR
   and mnatUR (standing for authoritative Resource algebra and max nat Unital
   Resource algebra). *)

(* Auth is defined in iris.algebra.auth. *)
From iris.algebra Require Import auth.

(* The following section is a generic update property of the authoritative construction.
   In the Iris Coq library there are several update lemmas, using the concept of local updates
   (notation x ~l~> y, and the definition is called local_update).
   
   The two updates in the following section are the same as stated in the exercise in the notes.
*)
Section auth_update.
  Context {U : ucmraT}.

  Lemma auth_update_add (x y z : U):  (x  z)   x   y ~~>  (x  z)   (y  z).
  Proof.
    intros ?.
    (* auth_update is the generic update rule for the auth RA. It reduces a
       frame preserving update to that of a local update. *)
    apply auth_update.
    intros ? mz ? Heq.
    split.
380
    - apply cmra_valid_validN; auto.
381
    - simpl in *.
382
      rewrite Heq.
383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425
      destruct mz; simpl; auto.
      rewrite -assoc (comm _ _ z) assoc //.
  Qed.

  Lemma auth_update_add' (x y z w : U):  (x  z)  w  z   x   y ~~>  (x  z)   (y  w).
  Proof.
    (* The proof of this lemma uses the previous lemma, together with the fact
       that ~~> is transitive, and the fact that we always have the frame
       preserving update from a ⋅ b to a. This is proved in cmra_update_op_l in
       the Coq library.
    *)
    intros Hv [? He].
    etransitivity.
    apply (auth_update_add x y z Hv).
    rewrite {2}He assoc auth_frag_op assoc.
    apply cmra_update_op_l.
  Qed.
End auth_update.

Section monotone_counter'.
  (* We tell Coq that our Iris instantiation has the following resource
     algebras. Note that the only diffference from above is that we use authR
     mnatUR in place of the resource algebra mcounterRA we constructed above. *)
  Class mcounterG' Σ := MCounterG' { mcounter_inG' :> inG Σ (authR mnatUR)}.
  Definition mcounterΣ' : gFunctors := #[GFunctor (authR mnatUR)].

  Instance subG_mcounterΣ' {Σ} : subG mcounterΣ' Σ  mcounterG' Σ.
  Proof. solve_inG. Qed.

  (* We now prove the same three properties we claim were required from the resource
     algebra in Section 7.7.  *)
  Instance mcounterRA_frag_core' (n : mnatUR): CoreId ( n).
  Proof.
    apply _.
    (* CoreID is a typeclass, so typeclass search can automatically deduce what
       we want. Concretely, the proof follows by lemmas auth_frag_core_id and
       mnat_core_id proved in the Iris Coq library. *)
  Qed.

  Lemma mcounterRA_valid_auth_frag' (m n : mnatUR):  ( m   n)  (n  m)%nat.
  Proof.
    (* Use a simplified definition of validity for when the underlying CMRA is discrete, i.e., an RA.
       The general definition also involves the use of step-indices, which is not needed in our case. *)
426
    rewrite auth_both_valid.
427
    split.
428
    - intros [? _]; by apply mnat_included.
429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462
    - intros ?%mnat_included; done.
  Qed.

  Lemma mcounterRA_update' (m n : mnatUR):  m   n ~~>  (S m : mnatUR)   (S n : mnatUR).
  Proof.
    replace (S m) with (m  (S m)); last auto with arith.
    replace (S n) with (n  (S n)); last auto with arith.
    apply cmra_update_valid0; intros ?%cmra_discrete_valid%mcounterRA_valid_auth_frag'.
    apply auth_update_add'; first reflexivity.
    exists (S m); symmetry; apply max_r; auto with arith.
  Qed.

  (* We can now verify the programs. *)
  (* We start off as in the previous example, with some boilerplate code. *)
  Context `{!heapG Σ, !mcounterG' Σ} (N : namespace).
  Notation iProp := (iProp Σ).

  (* The rest of this section is exactly the same as the preceding one. We use
     the properties of the RA we have proved above. *)
  Definition counter_inv' ( : loc) (γ : gname) : iProp := ( (m : mnatUR),   #m  own γ ( m))%I.

  Definition isCounter' ( : loc) (n : mnatUR) : iProp :=
    ( γ, own γ ( n)  inv N (counter_inv'  γ))%I.

  Global Instance isCounter_persistent'  n: Persistent (isCounter'  n).
  Proof.
    apply _.
  Qed.

  Lemma newCounter_spec': {{{ True }}} newCounter #() {{{ v, RET #v; isCounter' v 0%nat }}}.
  Proof.
    iIntros (Φ) "_ HCont".
    rewrite /newCounter -wp_fupd.
    wp_lam.
463
    iMod (own_alloc ( (0%nat : mnatUR)   (0%nat : mnatUR))) as (γ) "[HAuth HFrac]".
464 465 466 467 468 469 470
    - apply mcounterRA_valid_auth_frag'; auto.
    - wp_alloc  as "Hpt".
      iMod (inv_alloc N _ (counter_inv'  γ) with "[Hpt HAuth]") as "HInv".
      + iExists 0%nat; iFrame.
      + iApply ("HCont" with "[HFrac HInv]").
        iExists γ; iFrame.
  Qed.
471

472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502
  (* The read method specification. *)
  Lemma read_spec'  n: {{{ isCounter'  n }}} read # {{{ m, RET #m; n  m%nat }}}.
  Proof.
    iIntros (Φ) "HCounter HCont".
    iDestruct "HCounter" as (γ) "[HOwnFrag HInv]".
    rewrite /read.
    wp_lam.
    iInv N as (m) ">[Hpt HOwnAuth]" "HClose".
    wp_load.
    iDestruct (@own_valid_2 _ _ _ γ with "HOwnAuth HOwnFrag") as %H%mcounterRA_valid_auth_frag'.
    iMod ("HClose" with "[Hpt HOwnAuth]") as "_".
    { iNext; iExists m; iFrame. }
    iModIntro.
    iApply "HCont"; done.
  Qed.

  (* The read method specification. *)
  Lemma incr_spec'  n: {{{ isCounter'  n }}} incr # {{{ RET #(); isCounter'  (1 + n)%nat }}}.
  Proof.
    iIntros (Φ) "HCounter HCont".
    iDestruct "HCounter" as (γ) "[HOwnFrag #HInv]".
    iLöb as "IH".
    rewrite /incr.
    wp_lam.
    wp_bind (! _)%E.
    iInv N as (m) ">[Hpt HOwnAuth]" "HClose".
    wp_load.
    iDestruct (@own_valid_2 _ _ _ γ with "HOwnAuth HOwnFrag") as %H%mcounterRA_valid_auth_frag'.
    iMod ("HClose" with "[Hpt HOwnAuth]") as "_".
    { iNext; iExists m; iFrame. }
    iModIntro.
503
    wp_let; wp_op; wp_let.
504 505 506 507
    wp_bind (CAS _ _ _)%E.
    iInv N as (k) ">[Hpt HOwnAuth]" "HClose".
    destruct (decide (k = m)); subst.
    + wp_cas_suc.
508
      iMod (own_update γ (( m   n)) ( (S m : mnatUR)  ( (S n : mnatUR))) with "[HOwnFrag HOwnAuth]") as "[HOwnAuth HOwnFrag]".
509 510 511 512 513
      { apply mcounterRA_update'. }
      { rewrite own_op; iFrame. }
      iMod ("HClose" with "[Hpt HOwnAuth]") as "_".
      { iNext; iExists (1 + m)%nat.
        rewrite Nat2Z.inj_succ Z.add_1_l; iFrame. }
514
      iModIntro; wp_if; iApply ("HCont" with "[HInv HOwnFrag]").
515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549
      iExists γ; iFrame "#"; iFrame.
    + wp_cas_fail; first intros ?; simplify_eq.
      iMod ("HClose" with "[Hpt HOwnAuth]") as "_".
      - iExists k; iFrame.
      - iModIntro; wp_if.
        iApply ("IH" with "HOwnFrag HCont"); iFrame.
  Qed.
End monotone_counter'.

(* Counter with contributions. *)
(* As a final example in this example file we give the more precise specification to the counter. *) 
(* As explained in the lecture notes we need a different resource algebra: the
   authoritative resource algebra on the product of the RA of fractions and the
   RA of natural numbers, with an added unit.

   The combination of the RA of fractions and the authoritative RA in this way
   is fairly common, and so the Iris Coq library provides frac_authR (CM)RA. *)

From iris.algebra Require Import frac_auth.

Section ccounter.
  (* We start as we did before, telling Coq what we assume from the Iris instantiation. *)
  (* Note that now we use natR as the underlying resource algebra. This is the
     RA of natural numbers with addition as the operation. *)
  Class ccounterG Σ := CCounterG { ccounter_inG :> inG Σ (frac_authR natR) }.
  Definition ccounterΣ : gFunctors := #[GFunctor (frac_authR natR)].

  Instance subG_ccounterΣ {Σ} : subG ccounterΣ Σ  ccounterG Σ.
  Proof. solve_inG. Qed.


  (* The first thing we are going to prove are the properties of the resource
     algebra, specialized to our use case. These are listed in the exercise in
     the relevant section of the lecture notes. *)
  (* We are using some new notation. The frac_auth library defines the notation
550 551 552
     ◯F{q} n to mean ◯ (q, n) as we used in the lecture notes. Further, ●F m
     means ● (1, m) and ◯F n means ◯ (1, n). *)
  Lemma ccounterRA_valid (m n : natR) (q : frac):  (F m  F{q} n)  (n  m)%nat.
553 554 555 556 557 558
  Proof.
    intros ?.
    (* This property follows directly from the generic properties of the relevant RAs. *)
    by apply nat_included, (frac_auth_included_total q).
  Qed.

559
  Lemma ccounterRA_valid_full (m n : natR):  (F m  F n)  (n = m)%nat.
560 561
  Proof.
    by intros ?%frac_auth_agree.
562
  Qed.
563

564
  Lemma ccounterRA_update (m n : natR) (q : frac): (F m  F{q} n) ~~> (F (S m)  F{q} (S n)).
565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582
  Proof.
    apply frac_auth_update, (nat_local_update _ _ (S _) (S _)).
    lia.
  Qed.

  (* We have all the properties of the RAs needed and thus we can proceed with
     the proof, which proceeds largely as before, modulo the changes in
     invariants.

     There is one important difference in the definition of is_ccounter. The
     ghost name γ is not hidden. This is because now is_ccounter is not
     persistent, and to share it we have the is_ccounter_op lemma, which would
     not hold if we were to existentially quantify γ as we did in the previous
     examples.
  *)
  Context `{!heapG Σ, !ccounterG Σ} (N : namespace).

  Definition ccounter_inv (γ : gname) (l : loc) : iProp Σ :=
583
    ( n, own γ (F n)  l  #n)%I.
584 585

  Definition is_ccounter (γ : gname) (l : loc) (q : frac) (n : natR) : iProp Σ :=
586
    (own γ (F{q} n)  inv N (ccounter_inv γ l))%I.
587 588 589 590

  (** The main proofs. *)

  (* As explained in the notes the is_ccounter predicate for this specificatin is not persistent.
591
     However it is still shareable in the following restricted way.
592 593 594 595
   *)
  Lemma is_ccounter_op γ  q1 q2 (n1 n2 : nat) :
    is_ccounter γ  (q1 + q2) (n1 + n2)%nat ⊣⊢ is_ccounter γ  q1 n1  is_ccounter γ  q2 n2.
  Proof.
Ralf Jung's avatar
Ralf Jung committed
596
    apply bi.equiv_spec; split; rewrite /is_ccounter frac_auth_frag_op own_op.
597 598 599 600 601 602 603
    - iIntros "[? #?]".
      iFrame "#"; iFrame.
    - iIntros "[[? #?] [? _]]".
      iFrame "#"; iFrame.
  Qed.

  Lemma newcounter_contrib_spec (R : iProp Σ) :
604
    {{{ True }}}
605 606 607
        newCounter #()
    {{{ γ , RET #; is_ccounter γ  1 0%nat }}}.
  Proof.
608
    iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newCounter /=. wp_lam. wp_alloc  as "Hpt".
609
    iMod (own_alloc (F O%nat  F 0%nat)) as (γ) "[Hγ Hγ']"; first by apply auth_both_valid.
610 611 612 613 614 615 616
    iMod (inv_alloc N _ (ccounter_inv γ ) with "[Hpt Hγ]").
    { iNext. iExists 0%nat. by iFrame. }
    iModIntro. iApply "HΦ". rewrite /is_ccounter; eauto.
  Qed.

  Lemma incr_contrib_spec γ  q n :
    {{{ is_ccounter γ  q n  }}}
617
        incr #
618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636
    {{{ RET #(); is_ccounter γ  q (S n) }}}.
  Proof.
    iIntros (Φ) "[Hown #Hinv] HΦ". iLöb as "IH". wp_rec.
    wp_bind (! _)%E. iInv N as (c) ">[Hγ Hpt]" "Hclose".
    wp_load. iMod ("Hclose" with "[Hpt Hγ]") as "_"; [iNext; iExists c; by iFrame|].
    iModIntro. wp_let. wp_op. wp_let.
    wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hpt]" "Hclose".
    destruct (decide (c' = c)) as [->|].
    - iMod (own_update_2 with "Hγ Hown") as "[Hγ Hown]".
      { apply ccounterRA_update. } (* We use the update lemma for our RA. *)
      wp_cas_suc. iMod ("Hclose" with "[Hpt Hγ]") as "_".
      { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
      iModIntro. wp_if. iApply "HΦ". by iFrame "Hinv".
    - wp_cas_fail; first (by intros [= ?%Nat2Z.inj]).
      iMod ("Hclose" with "[Hpt Hγ]") as "_"; [iNext; iExists c'; by iFrame|].
      iModIntro. wp_if. by iApply ("IH" with "[Hown] [HΦ]"); auto.
  Qed.

  Lemma read_contrib_spec γ  q n :
637
    {{{ is_ccounter γ  q n }}}
638 639 640 641
        read #
    {{{ c, RET #c; n  c%nat  is_ccounter γ  q n }}}.
  Proof.
    iIntros (Φ) "[Hown #Hinv] HΦ".
642
    rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hpt]" "Hclose". wp_load.
643 644 645 646 647 648 649 650 651 652
    iDestruct (own_valid_2 with "Hγ Hown") as % ?%ccounterRA_valid. (* We use the validity property of our RA. *)
    iMod ("Hclose" with "[Hpt Hγ]") as "_"; [iNext; iExists c; by iFrame|].
    iApply ("HΦ" with "[-]"); rewrite /is_ccounter; eauto.
  Qed.

  Lemma read_contrib_spec_1 γ  n :
    {{{ is_ccounter γ  1 n }}} read #
    {{{ m, RET #m; m = n  is_ccounter γ  1 m }}}.
  Proof.
    iIntros (Φ) "[Hown #Hinv] HΦ".
653
    rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hpt]" "Hclose". wp_load.
654 655 656 657
    iDestruct (own_valid_2 with "Hγ Hown") as % <-%ccounterRA_valid_full. (* We use the validity property of our RA. *)
    iMod ("Hclose" with "[Hpt Hγ]") as "_"; [iNext; iExists n; by iFrame|].
    iApply "HΦ"; iModIntro. iFrame "Hown #"; done.
  Qed.
658
End ccounter.