Add bag and tweak lock

_CoqProject

@@ -20,6 +20,7 @@ theories/lecture_notes/coq_intro_example_2.v
 theories/lecture_notes/lists.v
 theories/lecture_notes/lists_guarded.v
 theories/lecture_notes/lock.v
+theories/lecture_notes/bag.v
 theories/lecture_notes/lock_unary_spec.v
 theories/lecture_notes/modular_incr.v
 theories/lecture_notes/recursion_through_the_store.v

theories/lecture_notes/bag.v

+(* This file contains Example 7.38 of the Iris Lecture Notes. We implement a
+   concurrent course grained bag based on the lock in `lock.v`.
+*)
+
+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Export lang.
+From iris.heap_lang Require Import proofmode notation.
+From iris.algebra Require Import auth.
+Import uPred.
+
+From iris_examples.lecture_notes Require Import lock.
+
+Definition newbag : val :=
+  λ: <>, let: "ℓ" := ref NONE in
+         let: "v" := newlock #() in ("ℓ", "v").
+
+Definition insert : val :=
+  λ: "x", λ: "e", let: "ℓ" := Fst "x" in
+                  let: "lock" := Snd "x" in
+                  acquire "lock" ;; 
+                  "ℓ" <- SOME ("e", !"ℓ") ;;
+                  release "lock".
+
+Definition remove : val :=
+  λ: "x", let: "ℓ" := Fst "x" in
+          let: "lock" := Snd "x" in
+          acquire "lock" ;; 
+          let: "r" := !"ℓ" in 
+          let: "res" := match: "r" with
+                          NONE => NONE
+                        | SOME "p" => "ℓ" <- Snd "p" ;; SOME (Fst "p")
+                        end
+          in release "lock" ;; "res".
+
+Section spec.
+  Context `{!heapG Σ, lockG Σ}.
+  Local Notation iProp := (iProp Σ).
+
+  Fixpoint isBag (Ψ : val → iProp) (v : val) : iProp :=
+    match v with
+    | NONEV => ⌜True⌝%I
+    | SOMEV (x, r) => (Ψ x ∗ isBag Ψ r)%I
+    | _ => ⌜False⌝%I
+    end.
+
+  Definition is_bag (v : val) (Ψ : val → iProp) :=
+    (∃ (ℓ : loc) (v₂ : val) γ, ⌜v = PairV (#ℓ) v₂⌝ ∗ is_lock γ v₂ (∃ u, ℓ ↦ u ∗ isBag Ψ u))%I.
+
+  Global Instance bag_persistent v Ψ: Persistent (is_bag v Ψ).
+  Proof. apply _. Qed.
+
+  Lemma newbag_triple_spec Ψ:
+    {{{ True }}} newbag #() {{{ b, RET b; is_bag b Ψ}}}.
+  Proof.
+    iIntros (ϕ) "_ Hcont".
+    wp_lam ; wp_alloc ℓ as "Hℓ"; wp_let.
+    wp_apply ((newlock_spec (∃ u, ℓ ↦ u ∗ isBag Ψ u))%I with "[Hℓ]").
+    { iExists NONEV. auto. }
+    iIntros (v). iDestruct 1 as (γ) "IL".
+    wp_pures. iApply "Hcont".
+    iExists ℓ, v, γ. iFrame. done.
+  Qed.
+
+  Lemma bag_insert_triple_spec v Ψ e: 
+    {{{ is_bag v Ψ ∗ Ψ e }}} insert v e {{{ RET #(); True }}}.
+  Proof.
+    iIntros (ϕ) "[Hb Hψ] Hcont".
+    iDestruct "Hb" as (ℓ u γ) "[% #IL]" ; subst.
+    wp_lam. wp_pures.
+    wp_apply (acquire_spec with "IL"); first done.
+    iIntros (v) "[P HLocked]".
+    iDestruct "P" as (b) "[Hp Hb]".
+    wp_load. wp_store.
+    iApply (release_spec with "[$IL $HLocked Hp Hψ Hb]"); first done.
+    { iExists _. iFrame "Hp". iFrame. }
+    done.
+  Qed.
+
+  Lemma bag_remove_triple_spec v Ψ:
+    {{{ is_bag v Ψ }}} remove v {{{ u, RET u; ⌜u = NONEV⌝ ∨ ∃ x, ⌜u = SOMEV x⌝ ∗ Ψ x}}}.
+  Proof.
+    iIntros (ϕ) "Hb Hcont".
+    iDestruct "Hb" as (ℓ u γ) "[% #IL]"; subst.
+    wp_lam. wp_pures.
+    wp_apply (acquire_spec with "IL"); first done.
+    iIntros (v) "[P HLocked]". iDestruct "P" as (b) "[Hp Hb]".
+    wp_load.
+    destruct b; try (iDestruct "Hb" as "%"; contradiction).
+    - wp_apply (release_spec with "[$IL $HLocked Hp Hb]"); first done.
+      { iExists _. iFrame. }
+      iIntros. wp_pures. iApply "Hcont". iLeft. done.
+    - destruct b; try (iDestruct "Hb" as "%"; contradiction).
+      simpl. iDestruct "Hb" as "[Hψ Hb]".
+      wp_store.
+      wp_apply (release_spec with "[$IL $HLocked Hp Hb]"); first done.
+      { iExists _. iFrame. }
+      iIntros (_).
+      wp_pures.
+      iApply "Hcont".
+      iRight. iExists _. by iFrame.
+  Qed.
+
+End spec.

theories/lecture_notes/lock.v

-(* This file contains the specification of the lock module implemented as a simple spin lock and discussed in 
-   section 7.6 in the invariants and ghost state chapter of the Iris Lecture Notes.
+(* This file contains the specification of the lock module implemented as a
+   simple spin lock and discussed in section 7.6 in the invariants and ghost
+   state chapter of the Iris Lecture Notes.
 *)
 
 (* Contains definitions of the weakest precondition assertion, and its basic rules. *)
@@ -10,9 +11,9 @@ From iris.program_logic Require Export weakestpre.
    the lang file contains the actual language syntax. *)
 From iris.heap_lang Require Export notation lang.
 
-(* Files related to the interactive proof mode. The first import includes the 
-   general tactics of the proof mode. The second provides some more specialized 
-   tactics particular to the instantiation of Iris to a particular programming 
+(* Files related to the interactive proof mode. The first import includes the
+   general tactics of the proof mode. The second provides some more specialized
+   tactics particular to the instantiation of Iris to a particular programming
    language. *)
 From iris.proofmode Require Export tactics.
 From iris.heap_lang Require Import proofmode.
@@ -23,40 +24,39 @@ From iris.base_logic.lib Require Export invariants.
 (* The exclusive resource algebra. *)
 From iris.algebra Require Import excl.
 
-Section lock_model. 
+Class lockG Σ := lock_G :> inG Σ (exclR unitR).
+
+Section lock_model.
 (* In order to do the proof we need to assume certain things about the
    instantiation of Iris. The particular, even the heap is handled in an
    analogous way as other ghost state. This line states that we assume the Iris
    instantiation has sufficient structure to manipulate the heap, e.g., it
    allows us to use the points-to predicate, and that the ghost state includes
    the exclusive resource algebra over the singleton set (represented using the
-   unitR type). *)  
+   unitR type). *)
+
+  Context `{heapG Σ, lockG Σ}.
 
-  Context `{heapG Σ}.
-  Context `{inG Σ (exclR unitR)}.
- 
   (* We use a ghost name with a token to model whether the lock is locked or not.
      The the token is just exclusive ownerwhip of unit value. *)
   Definition locked γ := own γ (Excl ()).
 
   (* The name of a lock. *)
-  Definition lockN (l : loc) := nroot .@ "lock" .@ l.
+  Definition lockN (l : val) := nroot .@ "lock" .@ l.
 
   (* The lock invariant *)
-  Definition is_lock γ l P :=
-    inv (lockN l) ((l ↦ (#false) ∗ P ∗ locked γ) ∨
-                                l ↦ (#true))%I.
+  Definition is_lock γ (v : val) P :=
+    (∃ (ℓ : loc), ⌜v = #ℓ⌝ ∧ inv (lockN v) (ℓ ↦ #false ∗ P ∗ locked γ ∨ ℓ ↦ #true))%I.
 
   (* The is_lock predicate is persistent *)
   Global Instance is_lock_persistent γ l Φ : Persistent (is_lock γ l Φ).
   Proof. apply _. Qed.
-  
+
 End lock_model.
 
 Section lock_code.
 
-  (* Here is the standard spin lock code *)
-  
+  (* The standard spin lock code *)
   Definition newlock : val := λ: <>, ref #false.
   Definition acquire : val :=
     rec: "acquire" "l" :=
@@ -66,11 +66,10 @@ Section lock_code.
 End lock_code.
 
 Section lock_spec.
-  Context `{heapG Σ}.
-  Context `{inG Σ (exclR unitR)}.
+  Context `{heapG Σ, lockG Σ}.
 
-  Lemma wp_newlock_t P:
-    {{{ P }}} newlock #() {{{v, RET v; ∃ (l: loc) γ, ⌜v = #l⌝ ∧ is_lock γ l P }}}.
+  Lemma newlock_spec P :
+    {{{ P }}} newlock #() {{{ l, RET l; ∃ γ, is_lock γ l P }}}.
   Proof.
     iIntros (φ) "Hi Hcont".
     rewrite -wp_fupd /newlock.
@@ -82,21 +81,21 @@ Section lock_spec.
       as "Hinv"; last eauto.
     { iNext; iLeft; iFrame. }
     iApply "Hcont".
-    iExists l, γ.
-    iModIntro. iSplit; first done.
+    iExists γ. iModIntro. iExists l. iSplit; first done.
     iFrame.
   Qed.
 
-  Lemma wp_acquire_t E γ l P :
+  Lemma acquire_spec E γ l P :
     nclose (lockN l) ⊆ E →
-    {{{ is_lock γ l P }}} acquire (#l) @ E {{{v, RET #v; P ∗ locked γ}}}.
+    {{{ is_lock γ l P }}} acquire l @ E {{{ v, RET #v; P ∗ locked γ }}}.
   Proof.
     iIntros (HE φ) "#Hi Hcont"; rewrite /acquire.
+    iDestruct "Hi" as (ℓ ->) "Hinv".
     iLöb as "IH".
     wp_rec.
     wp_bind (CmpXchg _ _ _).
-    iInv (lockN l) as "[(Hl & HP & Ht)|Hl]" "Hcl".
-    - wp_cmpxchg_suc. 
+    iInv (lockN #ℓ) as "[(Hl & HP & Ht)|Hl]" "Hcl".
+    - wp_cmpxchg_suc.
       iMod ("Hcl" with "[Hl]") as "_"; first by iRight.
       iModIntro.
       wp_proj.
@@ -108,17 +107,18 @@ Section lock_spec.
       iModIntro.
       wp_proj.
       wp_if.
-      iApply ("IH" with "[$Hcont]").
+      iApply ("IH" with "Hcont").
   Qed.
 
-  Lemma wp_release_t E γ l P :
+  Lemma release_spec E γ l P :
     nclose (lockN l) ⊆ E →
-    {{{ is_lock γ l P ∗ locked γ ∗ P }}} release (#l) @ E {{{RET #(); True}}}.
+    {{{ is_lock γ l P ∗ locked γ ∗ P }}} release l @ E {{{ RET #(); True}}}.
   Proof.
     iIntros (HE φ) "(#Hi & Hld & HP) Hcont"; rewrite /release.
+    iDestruct "Hi" as (ℓ ->) "Hinv".
     wp_lam.
-    iInv (lockN l) as "[(Hl & HQ & >Ht)|Hl]" "Hcl".
-    - iDestruct (own_valid_2 with "Hld Ht") as %Hv. done. 
+    iInv (lockN #ℓ) as "[(Hl & HQ & >Ht)|Hl]" "Hcl".
+    - iDestruct (own_valid_2 with "Hld Ht") as %Hv. done.
     - wp_store.
       iMod ("Hcl" with "[-Hcont]") as "_"; first by iNext; iLeft; iFrame.
       iApply "Hcont".