concurrent stacks: also unify concurrent bag (per-element) specs for stacks 1 and 2

theories/concurrent_stacks/concurrent_stack1.v

@@ -5,6 +5,9 @@ From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang.
 From iris.algebra Require Import agree list.
 From iris.heap_lang Require Import assert proofmode notation.
+
+From iris_examples.concurrent_stacks Require Import spec.
+
 Set Default Proof Using "Type".
 
 (** Stack 1: No helping, bag spec. *)
@@ -14,10 +17,10 @@ Definition mk_stack : val :=
   let: "r" := ref NONEV in
   (rec: "pop" "n" :=
      match: !"r" with
-       NONE => #-1
+       NONE => NONE
      | SOME "hd" =>
        if: CAS "r" (SOME "hd") (Snd !"hd")
-       then Fst !"hd"
+       then SOME (Fst !"hd")
        else "pop" "n"
      end,
     rec: "push" "n" :=
@@ -81,8 +84,8 @@ Section stacks.
 
   (* Per-element invariant (i.e., bag spec). *)
   Theorem stack_works P Φ :
-    (∀ (f₁ f₂ : val),
-            (∀ (v : val), □ WP f₁ #() {{ v, P v  ∨ v ≡ #-1 }})
+    ▷ (∀ (f₁ f₂ : val),
+            (□ WP f₁ #() {{ v, (∃ v', v ≡ SOMEV v' ∗ P v')  ∨  v ≡ NONEV }})
          -∗ (∀ (v : val), □ (P v -∗ WP f₂ v {{ v, True }}))
          -∗ Φ (f₁, f₂)%V)%I
     -∗ WP mk_stack #()  {{ Φ }}.
@@ -98,7 +101,7 @@ Section stacks.
     wp_let.
     iModIntro.
     iApply "HΦ".
-    - iIntros (v) "!#".
+    - iIntros "!#".
       iLöb as "IH".
       wp_rec.
       wp_bind (! #l)%E.
@@ -129,7 +132,7 @@ Section stacks.
           wp_if.
           wp_load.
           wp_proj.
-          iLeft; auto.
+          eauto.
         * simpl in Hne. wp_cas_fail.
           iMod ("Hclose" with "[Hl'' Hstack]").
           { iExists v''; iFrame; auto. }
@@ -172,3 +175,10 @@ Section stacks.
         done.
   Qed.
 End stacks.
+
+Program Definition is_concurrent_bag `{!heapG Σ} : concurrent_bag Σ :=
+  {| spec.mk_bag := mk_stack |}.
+Next Obligation.
+  iIntros (??? P Φ) "_ HΦ". iApply stack_works.
+  iNext. iIntros (f₁ f₂) "Hpop Hpush". iApply "HΦ". iFrame.
+Qed.

theories/concurrent_stacks/concurrent_stack2.v

@@ -3,6 +3,9 @@ stricter CAS requirements yet. *)
 From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang proofmode notation.
 From iris.algebra Require Import excl.
+
+From iris_examples.concurrent_stacks Require Import spec.
+
 Set Default Proof Using "Type".
 
 (** Stack 2: With helping, bag spec. *)
@@ -268,7 +271,7 @@ Section stack_works.
 
   (* Per-element invariant (i.e., bag spec). *)
   Theorem stack_works {channelG0 : channelG Σ} P Φ :
-    (∀ (f₁ f₂ : val),
+    ▷ (∀ (f₁ f₂ : val),
             (□ WP f₁ #() {{ v, (∃ (v' : val), v ≡ SOMEV v' ∗ P v')  ∨ v ≡ NONEV }})
          -∗ (∀ (v : val), □ (P v -∗ WP f₂ v {{ v, True }}))
          -∗ Φ (f₁, f₂)%V)%I
@@ -405,3 +408,10 @@ Section stack_works.
         done.
   Qed.
 End stack_works.
+
+Program Definition is_concurrent_bag `{!heapG Σ, !channelG Σ} : concurrent_bag Σ :=
+  {| spec.mk_bag := mk_stack |}.
+Next Obligation.
+  iIntros (???? P Φ) "_ HΦ". iApply stack_works.
+  iNext. iIntros (f₁ f₂) "Hpop Hpush". iApply "HΦ". iFrame.
+Qed.

theories/concurrent_stacks/concurrent_stack3.v

 From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang proofmode notation.
 From iris.algebra Require Import excl.
-Set Default Proof Using "Type".
 
 From iris_examples.concurrent_stacks Require Import spec.
 
+Set Default Proof Using "Type".
+
 (** Stack 3: No helping, view-shift spec. *)
 
 Definition mk_stack : val :=
@@ -213,11 +214,11 @@ Section stack_works.
         wp_if.
         iApply ("IH" with "Hpush").
   Qed.
-
-  Program Definition is_concurrent_stack : concurrent_stack Σ :=
-    {| spec.mk_stack := mk_stack |}.
-  Next Obligation.
-    iIntros (????? Φ) "HP HΦ". iApply (stack_works with "[HΦ] HP").
-    iNext. iIntros (f₁ f₂) "Hpop Hpush". iApply "HΦ". iFrame.
-  Qed.
 End stack_works.
+
+Program Definition is_concurrent_stack `{!heapG Σ} : concurrent_stack Σ :=
+  {| spec.mk_stack := mk_stack |}.
+Next Obligation.
+  iIntros (??????? Φ) "HP HΦ". iApply (stack_works with "[HΦ] HP").
+  iNext. iIntros (f₁ f₂) "Hpop Hpush". iApply "HΦ". iFrame.
+Qed.

theories/concurrent_stacks/concurrent_stack4.v

@@ -6,6 +6,8 @@ From iris.algebra Require Import excl.
 
 From iris_examples.concurrent_stacks Require Import spec.
 
+Set Default Proof Using "Type".
+
 (** Stack 3: Helping, view-shift spec. *)
 
 Definition mk_offer : val :=
@@ -620,11 +622,11 @@ Section stack_works.
         wp_cas_fail.
         by iDestruct (own_valid_2 with "Hγ Hγ'") as %?.
   Qed.
-
-  Program Definition is_concurrent_stack `{!channelG Σ} : concurrent_stack Σ :=
-    {| spec.mk_stack := mk_stack |}.
-  Next Obligation.
-    iIntros (?????? Φ) "HP HΦ". iApply (stack_works with "[HΦ] HP").
-    iNext. iIntros (f₁ f₂) "#[Hpop Hpush]". iApply "HΦ". iFrame "#".
-  Qed.
 End stack_works.
+
+Program Definition is_concurrent_stack `{!heapG Σ, !channelG Σ} : concurrent_stack Σ :=
+  {| spec.mk_stack := mk_stack |}.
+Next Obligation.
+  iIntros (???????? Φ) "HP HΦ". iApply (stack_works with "[HΦ] HP").
+  iNext. iIntros (f₁ f₂) "#[Hpop Hpush]". iApply "HΦ". iFrame "#".
+Qed.

theories/concurrent_stacks/spec.v

@@ -2,6 +2,19 @@ From stdpp Require Import namespaces.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export proofmode notation.
 
+(** General (HoCAP-style) spec for a concurrent bag ("per-elemt spec") *)
+Record concurrent_bag {Σ} `{!heapG Σ} := ConcurrentBag {
+  mk_bag : val;
+  mk_bag_spec (N : namespace) (P : val → iProp Σ) :
+    {{{ True }}}
+      mk_bag #()
+    {{{ (f₁ f₂ : val), RET (f₁, f₂);
+        (□ WP f₁ #() {{ v, (∃ (v' : val), v ≡ SOMEV v' ∗ P v')  ∨  v ≡ NONEV }})
+        ∗ (∀ (v : val), □ (P v -∗ WP f₂ v {{ v, True }}))
+    }}}
+}.
+Arguments concurrent_bag _ {_}.
+
 (** General (HoCAP-style) spec for a concurrent stack *)
 
 Record concurrent_stack {Σ} `{!heapG Σ} := ConcurrentStack {