Small changes to specs, strengthen CAP spec

theories/concurrent_stacks/concurrent_stack1.v

@@ -171,6 +171,6 @@ Section stacks.
   Qed.
 End stacks.
 
-Program Definition spec {Σ} `{heapG Σ} : concurrent_bag Σ :=
-  {| is_bag := is_stack; new_bag := new_stack; bag_push := push; bag_pop := pop |} .
+Program Definition spec {Σ} N `{heapG Σ} : concurrent_bag Σ :=
+  {| is_bag := is_stack N; 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

@@ -394,6 +394,6 @@ Section stack_works.
   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 |} .
+Program Definition spec {Σ} N `{heapG Σ, channelG Σ} : concurrent_bag Σ :=
+  {| is_bag := is_stack N; 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

@@ -133,12 +133,12 @@ Section stack_works.
 
   Theorem pop_spec P s Ψ :
     {{{ is_stack_pred P s ∗
-        (∀ v xs, P (v :: xs) ={⊤ ∖ ↑ N}=∗ P xs ∗ Ψ (SOMEV v)) ∗
+        (∀ 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Φ".
+    iIntros (Φ) "(Hstack & Hupd) HΦ".
     iDestruct "Hstack" as (l) "[-> #Hinv]".
     iLöb as "IH".
     wp_lam. wp_bind (Load _).
@@ -147,6 +147,7 @@ Section stack_works.
     iDestruct (is_list_disj with "Hlist") as "[Hlist H]".
     iDestruct "H" as "[-> | HSome]".
     - iDestruct (is_list_empty with "Hlist") as %->.
+      iDestruct "Hupd" as "[_ Hupdnil]".
       iMod ("Hupdnil" with "HP") as "[HP HΨ]".
       iMod ("Hclose" with "[Hlist Hl HP]") as "_".
       { iNext; iExists _, _; iFrame. }
@@ -170,6 +171,7 @@ Section stack_works.
       * wp_cas_suc.
         iDestruct (is_list_cons with "[Hl'] Hlist") as (ys) "%"; first by iExists _.
         simplify_eq.
+        iDestruct "Hupd" as "[Hupdcons _]".
         iMod ("Hupdcons" with "HP") as "[HP HΨ]".
         iDestruct "Hlist" as (l'' t') "(% & Hl'' & Hlist)"; simplify_eq.
         iDestruct "Hl''" as (q') "Hl''".
@@ -184,7 +186,7 @@ Section stack_works.
         { iNext; iExists _, _; iFrame. }
         iModIntro.
         wp_if.
-        iApply ("IH" with "Hupdcons Hupdnil HΦ").
+        iApply ("IH" with "Hupd HΦ").
   Qed.
 End stack_works.
 

theories/concurrent_stacks/concurrent_stack4.v

@@ -138,13 +138,13 @@ Section proofs.
       iDestruct (own_valid_2 with "H Hγ") as %[].
   Qed.
 
-  Lemma take_works γ P Q o Ψ :
+  Lemma take_works γ P Q Q' o Ψ :
     let do_pop : iProp Σ :=
         (∀ v xs, P (v :: xs) ={inner_mask}=∗ P xs ∗ Ψ (SOMEV v))%I in
-    {{{ is_offer γ P Q o ∗ access_inv P ∗ do_pop }}}
+    {{{ is_offer γ P Q o ∗ access_inv P ∗ (do_pop ∧ Q') }}}
       take_offer o
     {{{ v', RET v';
-        (∃ v'' : val, ⌜v' = InjRV v''⌝ ∗ Ψ v') ∨ (⌜v' = InjLV #()⌝ ∗ do_pop) }}}.
+        (∃ v'' : val, ⌜v' = InjRV v''⌝ ∗ Ψ v') ∨ (⌜v' = InjLV #()⌝ ∗ (do_pop ∧ Q')) }}}.
   Proof.
     simpl; iIntros (Φ) "[H [Hopener Hupd]] HΦ"; iDestruct "H" as (v l) "[-> #Hinv]".
     wp_lam. wp_proj. wp_bind (CAS _ _ _).
@@ -197,12 +197,12 @@ Section proofs.
     iApply "HΦ"; iExists _; auto.
   Qed.
 
-  Lemma get_works P Ψ mailbox :
+  Lemma get_works Q P Ψ mailbox :
     let do_pop : iProp Σ :=
         (∀ v xs, P (v :: xs) ={inner_mask}=∗ P xs ∗ Ψ (SOMEV v))%I in
-    {{{ is_mailbox P mailbox ∗ access_inv P ∗ do_pop }}}
+    {{{ is_mailbox P mailbox ∗ access_inv P ∗ (do_pop ∧ Q) }}}
       get mailbox
-    {{{ ov, RET ov; (∃ v, ⌜ov = SOMEV v⌝ ∗ Ψ ov) ∨ (⌜ov = NONEV⌝ ∗ do_pop) }}}.
+    {{{ ov, RET ov; (∃ v, ⌜ov = SOMEV v⌝ ∗ Ψ ov) ∨ (⌜ov = NONEV⌝ ∗ (do_pop ∧ Q)) }}}.
   Proof.
     simpl; iIntros (Φ) "[Hmail [Hopener Hpush]] HΦ". iDestruct "Hmail" as (l) "[-> #Hmail]".
     wp_lam. wp_bind (Load _).
@@ -213,7 +213,7 @@ Section proofs.
       iModIntro.
       wp_pures.
       iApply "HΦ"; iRight; by iFrame.
-    - iDestruct "Hsome" as (v' γ Q) "[Hl #Hoffer]".
+    - iDestruct "Hsome" as (v' γ Q') "[Hl #Hoffer]".
       wp_load.
       iMod ("Hclose" with "[Hl Hoffer]") as "_".
       { iNext; iRight; iExists _, _, _; by iFrame. }
@@ -368,19 +368,19 @@ Section proofs.
 
   Theorem pop_works P s Ψ :
     {{{ is_stack_pred P s ∗
-        (∀ v xs, P (v :: xs) ={⊤ ∖ ↑ N}=∗ P xs ∗ Ψ (SOMEV v)) ∗
+        (∀ 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Φ".
+    iIntros (Φ) "(Hstack & Hupd) 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. }
+    iDestruct (bi.and_mono_r with "Hupd") as "Hupd"; first apply inner_mask_promote.
+    iDestruct (bi.and_mono_l _ _ (∀ (v : val) (xs : list val), _)%I with "Hupd") as "Hupd".
+    { iIntros "Hupdcons". iIntros (v xs). iSpecialize ("Hupdcons" $! v xs). iApply (inner_mask_promote with "Hupdcons"). }
     iLöb as "IH".
     wp_lam. wp_proj. wp_let. wp_proj. wp_let.
-    wp_apply (get_works _ (λ v, Ψ v) with "[Hupdcons]").
+    wp_apply (get_works _ _ (λ v, Ψ v) with "[Hupd]").
     { iSplitR; first done.
       iFrame.
       iInv Nstack as (v xs) "(Hl & Hlist & HP)" "Hclose".
@@ -390,7 +390,7 @@ Section proofs.
       iMod ("Hclose" with "[HP Hl Hlist]") as "_".
       { iNext; iExists _, _; iFrame. }
       auto. }
-    iIntros (ov) "[Hsome | [-> Hupdcons]]".
+    iIntros (ov) "[Hsome | [-> Hupd]]".
     - iDestruct "Hsome" as (v) "[-> HΨ]".
       wp_pures.
       iApply ("HΦ" with "HΨ").
@@ -401,7 +401,7 @@ Section proofs.
       iDestruct "H" as "[-> | HSome]".
       * iDestruct (is_list_empty with "Hlist") as %->.
         iMod (fupd_intro_mask' (⊤ ∖ ↑Nstack) inner_mask) as "Hupd'"; first solve_ndisj.
-        iMod ("Hupdnil" with "HP") as "[HP HΨ]".
+        iMod ("Hupd" with "HP") as "[HP HΨ]".
         iMod "Hupd'" as "_".
         iMod ("Hclose" with "[Hlist Hl HP]") as "_".
         { iNext; iExists _, _; iFrame. }
@@ -426,6 +426,7 @@ Section proofs.
           iDestruct (is_list_cons with "[Hl'] Hlist") as (ys) "%"; first by iExists _.
           simplify_eq.
           iMod (fupd_intro_mask' (⊤ ∖ ↑Nstack) inner_mask) as "Hupd'"; first solve_ndisj.
+          iDestruct "Hupd" as "[Hupdcons _]".
           iMod ("Hupdcons" with "HP") as "[HP HΨ]".
           iMod "Hupd'" as "_".
           iDestruct "Hlist" as (l'' t') "(% & Hl'' & Hlist)"; simplify_eq.
@@ -441,7 +442,7 @@ Section proofs.
           { iNext; iExists _, _; iFrame. }
           iModIntro.
           wp_pures.
-          iApply ("IH" with "HΦ Hupdnil Hupdcons").
+          iApply ("IH" with "HΦ Hupd").
   Qed.
 End proofs.
 

theories/concurrent_stacks/specs.v

@@ -4,27 +4,27 @@ 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;
+  is_bag (P : val → iProp Σ) (s : val) : iProp Σ;
+  bag_pers (P : val → iProp Σ) (s : val) : Persistent (is_bag P s);
   new_bag : val;
   bag_push : val;
   bag_pop : val;
-  mk_bag_spec (N : namespace) (P : val → iProp Σ) :
+  mk_bag_spec (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 }}}
+    {{{ s, RET s; is_bag P s }}};
+  bag_push_spec (P : val → iProp Σ) s v :
+    {{{ is_bag P s ∗ P v }}} bag_push s v {{{ RET #(); True }}};
+  bag_pop_spec (P : val → iProp Σ) s :
+    {{{ is_bag 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 *)
+(** General (CAP-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;
+  stack_pers (N : namespace) (P : list val → iProp Σ) (s : val) : Persistent (is_stack N P s);
   new_stack : val;
   stack_push : val;
   stack_pop : val;
@@ -36,7 +36,7 @@ Record concurrent_stack {Σ} `{!heapG Σ} := ConcurrentStack {
     {{{ 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)) ∗
+        (∀ v xs, P (v :: xs) ={⊤ ∖ ↑ N}=∗ P xs ∗ Ψ (SOMEV v)) ∧
         (P [] ={⊤ ∖ ↑ N}=∗ P [] ∗ Ψ NONEV) }}}
       stack_pop s
     {{{ v, RET v; Ψ v }}};