concurrent stacks: add an interface that both stack3 and stack4 implement

Had to slightly tweak (strengthen) stack3's spec for that

_CoqProject

@@ -27,6 +27,7 @@ theories/concurrent_stacks/concurrent_stack1.v
 theories/concurrent_stacks/concurrent_stack2.v
 theories/concurrent_stacks/concurrent_stack3.v
 theories/concurrent_stacks/concurrent_stack4.v
+theories/concurrent_stacks/spec.v
 
 theories/logrel/prelude/base.v
 theories/logrel/stlc/lang.v

theories/concurrent_stacks/concurrent_stack3.v

@@ -3,6 +3,8 @@ 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.
+
 (** Stack 3: No helping, view-shift spec. *)
 
 Definition mk_stack : val :=
@@ -89,9 +91,9 @@ Section stack_works.
      - The resources for the successful and failing pop must be disjoint.
        Instead, there should be a normal conjunction between them.
      Open question: How does this relate to a logically atomic spec? *)
-  Theorem stack_works P Q Q' Q'' Φ :
-    (∀ (f₁ f₂ : val) ι,
-        (□((∀ v vs, P (v :: vs) ={⊤∖↑ι}=∗ Q v ∗ P vs) -∗ (* pop *)
+  Theorem stack_works ι P Q Q' Q'' Φ :
+    ▷ (∀ (f₁ f₂ : val),
+        (□((∀ v vs, P (v :: vs) ={⊤∖↑ι}=∗ Q v ∗ P vs) ∧ (* pop *)
             (P [] ={⊤∖↑ι}=∗ Q' ∗ P []) -∗
             WP f₁ #() {{ v, (∃ (v' : val), v ≡ SOMEV v' ∗ Q v') ∨ (v ≡ NONEV ∗ Q')}}))
          -∗ (∀ (v : val), (* push *)
@@ -102,14 +104,14 @@ Section stack_works.
     -∗ WP mk_stack #()  {{ Φ }}.
   Proof.
     iIntros "HΦ HP".
-    pose proof (nroot .@ "N") as N.
+    rename ι into N.
     wp_let.
     wp_alloc l as "Hl".
     iMod (inv_alloc N _ (stack_inv P #l) with "[Hl HP]") as "#Istack".
     { iNext; iExists l, (InjLV #()), []; iSplit; iFrame; auto. }
     wp_let.
     iApply "HΦ".
-    - iIntros "!# Hsucc Hfail".
+    - iIntros "!# Hcont".
       iLöb as "IH".
       wp_rec.
       wp_bind (! _)%E.
@@ -122,6 +124,7 @@ Section stack_works.
       * subst.
         iDestruct (is_stack_empty with "Hstack") as "%".
         subst.
+        iDestruct "Hcont" as "[_ Hfail]".
         iMod ("Hfail" with "HP") as "[HQ' HP]".
         iMod ("Hclose" with "[Hl' Hstack HP]").
         { iExists l', (InjLV #()), []; iSplit; iFrame; auto. }
@@ -152,6 +155,7 @@ Section stack_works.
         iDestruct "H" as (ys') "%"; subst.
         iDestruct "Hstack" as (t') "[% Hstack]".
         injection H3; intros; subst.
+        iDestruct "Hcont" as "[Hsucc _]".
         iDestruct ("Hsucc" with "[HP]") as "> [HQ HP]"; auto.
         iMod ("Hclose" with "[Hl'' Hstack HP]").
         { iExists l'', t', ys'; iSplit; iFrame; auto. }
@@ -164,7 +168,7 @@ Section stack_works.
         { iExists l'', v', ys; iSplit; iFrame; auto. }
         iModIntro.
         wp_if.
-        iApply ("IH" with "Hsucc Hfail").
+        iApply ("IH" with "Hcont").
     - iIntros (v) "!# Hpush".
       iLöb as "IH".
       wp_rec.
@@ -199,4 +203,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").
+    iIntros "!>" (f₁ f₂) "Hpop Hpush". iApply "HΦ". iFrame.
+  Qed.
 End stack_works.

theories/concurrent_stacks/concurrent_stack4.v

@@ -2,6 +2,8 @@ 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.
+
 (** Stack 3: Helping, view-shift spec. *)
 
 Definition mk_offer : val :=
@@ -143,7 +145,7 @@ Section stack_works.
 
   (* Whole-stack invariant (P). *)
   Theorem stack_works {channelG0 : channelG Σ} N P Q Q' Q'' Φ :
-    (∀ (f₁ f₂ : val),
+    ▷ (∀ (f₁ f₂ : val),
         (□(((∀ v vs, P (v :: vs) ={⊤ ∖ ↑ N}=∗ Q v ∗ P vs)
             ∧ (P [] ={⊤ ∖ ↑ N}=∗ Q' ∗ P []) -∗
             WP f₁ #() {{ v, (∃ (v' : val), v ≡ SOMEV v' ∗ Q v') ∨ (v ≡ NONEV ∗ Q')}}))
@@ -618,4 +620,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").
+    iIntros "!>" (f₁ f₂) "#[Hpop Hpush]". iApply "HΦ". iFrame "#".
+  Qed.
 End stack_works.

theories/concurrent_stacks/spec.v

+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 stack *)
+
+Record concurrent_stack {Σ} `{!heapG Σ} := ConcurrentStack {
+  mk_stack : val;
+  mk_stack_spec (N : namespace) (P : list val → iProp Σ)
+    (Q : val → iProp Σ) (Q' Q'' : iProp Σ) :
+    {{{ P [] }}}
+      mk_stack #()
+    {{{ (f₁ f₂ : val), RET (f₁, f₂);
+        (□ ( (∀ v vs, P (v :: vs) ={⊤ ∖ ↑ N}=∗ Q v ∗ P vs)
+             ∧ (P [] ={⊤ ∖ ↑ N}=∗ Q' ∗ P []) -∗
+            WP f₁ #() {{ v, (∃ (v' : val), v ≡ SOMEV v' ∗ Q v') ∨ (v ≡ NONEV ∗ Q')}}))
+        ∗ (∀ (v : val),
+             □ ((∀ vs, P vs ={⊤ ∖ ↑ N}=∗ P (v :: vs) ∗ Q'') -∗ WP f₂ v {{ v, Q'' }}))
+    }}}
+}.
+Arguments concurrent_stack _ {_}.