Added specs

_CoqProject

@@ -23,6 +23,7 @@ theories/spanning_tree/mon.v
 theories/spanning_tree/spanning.v
 theories/spanning_tree/proof.v
 
+theories/concurrent_stacks/specs.v
 theories/concurrent_stacks/concurrent_stack1.v
 theories/concurrent_stacks/concurrent_stack2.v
 theories/concurrent_stacks/concurrent_stack3.v

theories/concurrent_stacks/concurrent_stack1.v

 From iris.base_logic.lib Require Import invariants.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Import notation proofmode.
+From iris_examples.concurrent_stacks Require Import specs.
 Set Default Proof Using "Type".
 
 Definition new_stack : val := λ: "_", ref NONEV.
@@ -81,16 +82,17 @@ Section stacks.
   Definition is_stack (P : val → iProp Σ) v :=
     inv N (stack_inv P v).
 
-  Theorem mk_stack_spec P :
-    WP new_stack #() {{ s, is_stack P s }}%I.
+  Theorem new_stack_spec P :
+    {{{ True }}} new_stack #() {{{ s, RET s; is_stack P s }}}.
   Proof.
+    iIntros (ϕ) "_ Hpost".
     iApply wp_fupd.
     wp_lam.
     wp_alloc ℓ as "Hl".
     iMod (inv_alloc N ⊤ (stack_inv P #ℓ) with "[Hl]") as "Hinv".
     { iNext; iExists ℓ, NONEV; iFrame;
       by iSplit; last (iApply is_list_unfold; iLeft). }
-    done.
+    by iApply "Hpost".
   Qed.
 
   Theorem push_spec P s v :
@@ -123,7 +125,7 @@ Section stacks.
       iApply ("IH" with "HP HΦ").
   Qed.
 
-  Theorem pop_works P s :
+  Theorem pop_spec P s :
     {{{ is_stack P s }}} pop s {{{ ov, RET ov; ⌜ov = NONEV⌝ ∨ ∃ v, ⌜ov = SOMEV v⌝ ∗ P v }}}.
   Proof.
     iIntros (Φ) "#Hstack HΦ".
@@ -168,3 +170,7 @@ Section stacks.
         iApply ("IH" with "HΦ").
   Qed.
 End stacks.
+
+Program Definition spec {Σ} `{heapG Σ} : concurrent_bag Σ :=
+  {| is_bag := is_stack; new_bag := new_stack; bag_push := push; bag_pop := pop |} .
+Solve Obligations of spec with eauto using pop_spec, push_spec, new_stack_spec.

theories/concurrent_stacks/concurrent_stack2.v

@@ -2,6 +2,7 @@ From iris.heap_lang Require Import notation proofmode.
 From iris.algebra Require Import excl.
 From iris.base_logic.lib Require Import invariants.
 From iris.program_logic Require Export weakestpre.
+From iris_examples.concurrent_stacks Require Import specs.
 Set Default Proof Using "Type".
 
 Definition mk_offer : val :=
@@ -26,7 +27,7 @@ Definition get : val :=
     | SOME "x" => take_offer "x"
     end.
 
-Definition mk_stack : val := λ: "_", (mk_mailbox #(), ref NONEV).
+Definition new_stack : val := λ: "_", (mk_mailbox #(), ref NONEV).
 Definition push : val :=
   rec: "push" "p" "v" :=
     let: "mailbox" := Fst "p" in
@@ -289,9 +290,10 @@ Section stack_works.
   Definition is_stack P v :=
     (∃ mailbox l, ⌜v = (mailbox, #l)%V⌝ ∗ is_mailbox Nmailbox P mailbox ∗ inv N (stack_inv P l))%I.
 
-  Theorem mk_stack_works P :
-    WP mk_stack #() {{ v, is_stack P v }}%I.
+  Theorem new_stack_spec P :
+    {{{ True }}} new_stack #() {{{ v, RET v; is_stack P v }}}.
   Proof.
+    iIntros (ϕ) "_ Hpost".
     rewrite -wp_fupd.
     wp_lam.
     wp_alloc l as "Hl".
@@ -299,10 +301,10 @@ Section stack_works.
     iIntros (mailbox) "#Hmailbox".
     iMod (inv_alloc N _ (stack_inv P l) with "[Hl]") as "#Hinv".
     { by iNext; iExists _; iFrame; rewrite is_list_unfold; iLeft. }
-    wp_pures; iModIntro; iExists _, _; auto.
+    wp_pures; iModIntro; iApply "Hpost"; iExists _, _; auto.
   Qed.
 
-  Theorem push_works P s v :
+  Theorem push_spec P s v :
     {{{ is_stack P s ∗ P v }}} push s v {{{ RET #(); True }}}.
   Proof.
     iIntros (Φ) "[Hstack HP] HΦ". iDestruct "Hstack" as (mailbox l) "(-> & #Hmailbox & #Hinv)".
@@ -340,7 +342,7 @@ Section stack_works.
       by iApply "HΦ".
   Qed.
 
-  Theorem pop_works P s :
+  Theorem pop_spec P s :
     {{{ is_stack P s }}} pop s {{{ ov, RET ov; ⌜ov = NONEV⌝ ∨ ∃ v, ⌜ov = SOMEV v⌝ ∗ P v }}}.
   Proof.
     iIntros (Φ) "Hstack HΦ". iDestruct "Hstack" as (mailbox l) "(-> & #Hmailbox & #Hstack)".
@@ -391,3 +393,7 @@ Section stack_works.
       iApply "HΦ"; iRight; iExists _; auto.
   Qed.
 End stack_works.
+
+Program Definition spec {Σ} `{heapG Σ, channelG Σ} : concurrent_bag Σ :=
+  {| is_bag := is_stack; new_bag := new_stack; bag_push := push; bag_pop := pop |} .
+Solve Obligations of spec with eauto using pop_spec, push_spec, new_stack_spec.

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_examples.concurrent_stacks Require Import specs.
 Set Default Proof Using "Type".
 
 Definition mk_stack : val := λ: "_", ref NONEV.
@@ -83,11 +84,11 @@ Section stack_works.
   Definition stack_inv P l :=
     (∃ v xs, l ↦ v ∗ is_list xs v ∗ P xs)%I.
 
-  Definition is_stack P v :=
+  Definition is_stack_pred P v :=
     (∃ l, ⌜v = #l⌝ ∗ inv N (stack_inv P l))%I.
 
-  Theorem mk_stack_works P :
-    {{{ P [] }}} mk_stack #() {{{ v, RET v; is_stack P v }}}.
+  Theorem mk_stack_spec P :
+    {{{ P [] }}} mk_stack #() {{{ v, RET v; is_stack_pred P v }}}.
   Proof.
     iIntros (Φ) "HP HΦ".
     rewrite -wp_fupd.
@@ -97,8 +98,8 @@ Section stack_works.
     iModIntro; iApply "HΦ"; iExists _; auto.
   Qed.
 
-  Theorem push_works P s v Ψ :
-    {{{ is_stack P s ∗ ∀ xs, P xs ={⊤ ∖ ↑ N}=∗ P (v :: xs) ∗ Ψ #()}}}
+  Theorem push_spec P s v Ψ :
+    {{{ is_stack_pred P s ∗ ∀ xs, P xs ={⊤ ∖ ↑ N}=∗ P (v :: xs) ∗ Ψ #()}}}
       push s v
     {{{ RET #(); Ψ #() }}}.
   Proof.
@@ -130,8 +131,8 @@ Section stack_works.
       iApply ("IH" with "Hupd HΦ").
   Qed.
 
-  Theorem pop_works P s Ψ :
-    {{{ is_stack P s ∗
+  Theorem pop_spec P s Ψ :
+    {{{ is_stack_pred P s ∗
         (∀ v xs, P (v :: xs) ={⊤ ∖ ↑ N}=∗ P xs ∗ Ψ (SOMEV v)) ∗
         (P [] ={⊤ ∖ ↑ N}=∗ P [] ∗ Ψ NONEV) }}}
       pop s
@@ -186,3 +187,7 @@ Section stack_works.
         iApply ("IH" with "Hupdcons Hupdnil HΦ").
   Qed.
 End stack_works.
+
+Program Definition spec {Σ} `{heapG Σ} : concurrent_stack Σ :=
+  {| is_stack := is_stack_pred; new_stack := mk_stack; stack_push := push; stack_pop := pop |} .
+Solve Obligations of spec with eauto using pop_spec, push_spec, mk_stack_spec.

theories/concurrent_stacks/concurrent_stack4.v

 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 specs.
 
 Definition mk_offer : val :=
   λ: "v", ("v", ref #0).
@@ -70,6 +71,16 @@ Section proofs.
      ⊤ ∖ ↑ N ⊆ inner_mask.
   Proof. solve_ndisj. Qed.
 
+  Lemma inner_mask_promote (P Q : iProp Σ) :
+     (P ={⊤ ∖ ↑ N}=∗ Q) -∗ (P ={inner_mask}=∗ Q).
+  Proof.
+    iIntros "Himp P".
+    iMod (fupd_intro_mask' inner_mask (⊤ ∖ ↑ N)) as "H"; first by apply inner_mask_includes.
+    iDestruct ("Himp" with "P") as "HQ".
+    iMod "HQ".
+    by iMod "H".
+  Qed.
+
   Definition revoke_tok γ := own γ (Excl ()).
   Definition can_push P Q v : iProp Σ :=
     (∀ (xs : list val), P xs ={inner_mask}=∗ P (v :: xs) ∗ Q #())%I.
@@ -296,11 +307,11 @@ Section proofs.
   Definition stack_inv P l :=
     (∃ v xs, l ↦ v ∗ is_list xs v ∗ P xs)%I.
 
-  Definition is_stack P v :=
+  Definition is_stack_pred P v :=
     (∃ mailbox l, ⌜v = (mailbox, #l)%V⌝ ∗ is_mailbox P mailbox ∗ inv Nstack (stack_inv P l))%I.
 
   Theorem mk_stack_works (P : list val → iProp Σ) :
-    {{{ P [] }}} mk_stack #() {{{ v, RET v; is_stack P v }}}.
+    {{{ P [] }}} mk_stack #() {{{ v, RET v; is_stack_pred P v }}}.
   Proof.
     iIntros (Φ) "HP HΦ".
     rewrite -wp_fupd.
@@ -313,11 +324,13 @@ Section proofs.
   Qed.
 
   Theorem push_works P s v Ψ :
-    {{{ is_stack P s ∗ ∀ xs, P xs ={inner_mask}=∗ P (v :: xs) ∗ Ψ #()}}}
+    {{{ is_stack_pred P s ∗ ∀ xs, P xs ={⊤ ∖ ↑ N}=∗ P (v :: xs) ∗ Ψ #()}}}
       push s v
     {{{ RET #(); Ψ #() }}}.
   Proof.
     iIntros (Φ) "[Hstack Hupd] HΦ". iDestruct "Hstack" as (mailbox l) "(-> & #Hmailbox & #Hinv)".
+    iAssert (∀ (xs : list val), P xs ={inner_mask}=∗ P (v :: xs) ∗ Ψ #())%I with "[Hupd]" as "Hupd".
+    { iIntros (xs). by iApply inner_mask_promote. }
     iLöb as "IH" forall (v).
     wp_lam. wp_pures.
     wp_apply (put_works with "[Hupd]"); first auto. iIntros (o) "H".
@@ -349,19 +362,22 @@ Section proofs.
         { iExists _, _; iFrame. }
         iModIntro.
         wp_if.
-        iApply ("IH" with "Hupd HΦ").
+        iApply ("IH" with "HΦ Hupd").
     - wp_match. iApply ("HΦ" with "HΨ").
   Qed.
 
   Theorem pop_works P s Ψ :
-    {{{ is_stack P s ∗
-        (∀ v xs, P (v :: xs) ={inner_mask}=∗ P xs ∗ Ψ (SOMEV v)) ∗
-        (P [] ={inner_mask}=∗ P [] ∗ Ψ NONEV) }}}
+    {{{ is_stack_pred P s ∗
+        (∀ v xs, P (v :: xs) ={⊤ ∖ ↑ N}=∗ P xs ∗ Ψ (SOMEV v)) ∗
+        (P [] ={⊤ ∖ ↑ N}=∗ P [] ∗ Ψ NONEV) }}}
       pop s
     {{{ v, RET v; Ψ v }}}.
   Proof.
     iIntros (Φ) "(Hstack & Hupdcons & Hupdnil) HΦ".
     iDestruct "Hstack" as (mailbox l) "(-> & #Hmailbox & #Hinv)".
+    iDestruct (inner_mask_promote with "Hupdnil") as "Hupdnil".
+    iAssert (∀ (v : val) (xs : list val), P (v :: xs) ={inner_mask}=∗ P xs ∗ Ψ (InjRV v))%I with "[Hupdcons]" as "Hupdcons".
+    { iIntros (v xs). by iApply inner_mask_promote. }
     iLöb as "IH".
     wp_lam. wp_proj. wp_let. wp_proj. wp_let.
     wp_apply (get_works _ (λ v, Ψ v) with "[Hupdcons]").
@@ -425,6 +441,10 @@ Section proofs.
           { iNext; iExists _, _; iFrame. }
           iModIntro.
           wp_pures.
-          iApply ("IH" with "Hupdcons Hupdnil HΦ").
+          iApply ("IH" with "HΦ Hupdnil Hupdcons").
   Qed.
 End proofs.
+
+Program Definition spec {Σ} `{heapG Σ, channelG Σ} : concurrent_stack Σ :=
+  {| is_stack := is_stack_pred; new_stack := mk_stack; stack_push := push; stack_pop := pop |} .
+Solve Obligations of spec with eauto using pop_works, push_works, mk_stack_works.

theories/concurrent_stacks/specs.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 bag ("per-elemt spec") *)
+Record concurrent_bag {Σ} `{!heapG Σ} := ConcurrentBag {
+  is_bag (N : namespace) (P : val → iProp Σ) (s : val) : iProp Σ;
+  bag_pers (N : namespace) (P : val → iProp Σ) (s : val) : is_bag N P s -∗ □ is_bag N P s;
+  new_bag : val;
+  bag_push : val;
+  bag_pop : val;
+  mk_bag_spec (N : namespace) (P : val → iProp Σ) :
+    {{{ True }}}
+      new_bag #()
+    {{{ s, RET s; is_bag N P s }}};
+  bag_push_spec (N : namespace) (P : val → iProp Σ) s v :
+    {{{ is_bag N P s ∗ P v }}} bag_push s v {{{ RET #(); True }}};
+  bag_pop_spec (N : namespace) (P : val → iProp Σ) s :
+    {{{ is_bag N P s }}} bag_pop s {{{ ov, RET ov; ⌜ov = NONEV⌝ ∨ ∃ v, ⌜ov = SOMEV v⌝ ∗ P v }}}
+}.
+Arguments concurrent_bag _ {_}.
+
+(** General (HoCAP-style) spec for a concurrent stack *)
+
+Record concurrent_stack {Σ} `{!heapG Σ} := ConcurrentStack {
+  is_stack (N : namespace) (P : list val → iProp Σ) (s : val) : iProp Σ;
+  stack_pers (N : namespace) (P : list val → iProp Σ) (s : val) : is_stack N P s -∗ □ is_stack N P s;
+  new_stack : val;
+  stack_push : val;
+  stack_pop : val;
+  new_stack_spec (N : namespace) (P : list val → iProp Σ) :
+    {{{ P [] }}} new_stack #() {{{ v, RET v; is_stack N P v }}};
+  stack_push_spec (N : namespace) (P : list val → iProp Σ) (Ψ : val → iProp Σ) s v :
+    {{{ is_stack N P s ∗ ∀ xs, P xs ={⊤ ∖ ↑ N}=∗ P (v :: xs) ∗ Ψ #()}}}
+      stack_push s v
+    {{{ RET #(); Ψ #() }}};
+  stack_pop_spec (N : namespace) (P : list val → iProp Σ) Ψ s :
+    {{{ is_stack N P s ∗
+        (∀ v xs, P (v :: xs) ={⊤ ∖ ↑ N}=∗ P xs ∗ Ψ (SOMEV v)) ∗
+        (P [] ={⊤ ∖ ↑ N}=∗ P [] ∗ Ψ NONEV) }}}
+      stack_pop s
+    {{{ v, RET v; Ψ v }}};
+}.
+Arguments concurrent_stack _ {_}.