Updated _CoqProject, updated concurrent_stacks to compile

_CoqProject

@@ -24,10 +24,9 @@ theories/spanning_tree/spanning.v
 theories/spanning_tree/proof.v
 
 theories/concurrent_stacks/concurrent_stack1.v
-#theories/concurrent_stacks/concurrent_stack2.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/concurrent_stacks/concurrent_stack4.v
 
 theories/logrel/prelude/base.v
 theories/logrel/stlc/lang.v

theories/concurrent_stacks/concurrent_stack1.v

@@ -98,12 +98,12 @@ Section stacks.
   Proof.
     iIntros (Φ) "[#Hstack HP] HΦ".
     iLöb as "IH".
-    wp_lam. wp_lam. wp_bind (Load _).
+    wp_lam. wp_let. wp_bind (Load _).
     iInv N as (ℓ v') "(>% & Hl & Hlist)" "Hclose"; subst.
     wp_load.
     iMod ("Hclose" with "[Hl Hlist]") as "_".
     { iNext; iExists _, _; by iFrame. }
-    iModIntro. wp_let. wp_alloc ℓ' as "Hl'". wp_let. wp_bind (CAS _ _ _).
+    iModIntro. wp_let. wp_alloc ℓ' as "Hl'". wp_pures. wp_bind (CAS _ _ _).
     iInv N as (ℓ'' v'') "(>% & >Hl & Hlist)" "Hclose"; simplify_eq.
     destruct (decide (v' = v'')) as [ -> |].
     - iDestruct (is_list_unboxed with "Hlist") as "[>% Hlist]".
@@ -146,7 +146,7 @@ Section stacks.
       iMod ("Hclose" with "[Hl' Hlist]") as "_".
       { iNext; iExists _, _; by iFrame. }
       iModIntro.
-      wp_let. wp_proj. wp_bind (CAS _ _ _).
+      wp_pures. wp_bind (CAS _ _ _).
       iInv N as (ℓ'' v'') "(>% & Hl' & Hlist)" "Hclose". simplify_eq.
       destruct (decide (v'' = InjRV #l)) as [-> |].
       * rewrite is_list_unfold.
@@ -158,8 +158,7 @@ Section stacks.
         iMod ("Hclose" with "[Hl' Hlist]") as "_".
         { iNext; iExists ℓ'', _; by iFrame. }
         iModIntro.
-        wp_if.
-        wp_proj.
+        wp_pures.
         iApply ("HΦ" with "[HP]"); iRight; iExists h; by iFrame.
       * wp_cas_fail.
         iMod ("Hclose" with "[Hl' Hlist]") as "_".

theories/concurrent_stacks/concurrent_stack2.v

@@ -84,7 +84,7 @@ Section side_channel.
     iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
     iMod (inv_alloc N _ (stages γ P l v) with "[Hl HP]") as "#Hinv".
     { iNext; iLeft; iFrame. }
-    iModIntro; iApply "HΦ"; iFrame; iExists _, _; auto.
+    wp_pures; iModIntro; iApply "HΦ"; iFrame; iExists _, _; auto.
   Qed.
 
   (* A partial specification for revoke that will be useful later *)
@@ -94,20 +94,20 @@ Section side_channel.
     {{{ v', RET v'; (∃ v'' : val, ⌜v' = InjRV v''⌝ ∗ P v'') ∨ ⌜v' = InjLV #()⌝ }}}.
   Proof.
     iIntros (Φ) "[Hinv Hγ] HΦ". iDestruct "Hinv" as (v' l) "[-> #Hinv]".
-    wp_let. wp_proj. wp_bind (CAS _ _ _).
+    wp_lam. wp_bind (CAS _ _ _). wp_pures.
     iInv N as "Hstages" "Hclose".
     iDestruct "Hstages" as "[[Hl HP] | [H | [Hl H]]]".
     - wp_cas_suc.
       iMod ("Hclose" with "[Hl Hγ]") as "_".
       { iRight; iRight; iFrame. }
       iModIntro.
-      wp_if. wp_proj.
+      wp_pures.
       by iApply "HΦ"; iLeft; iExists _; iSplit.
     - wp_cas_fail.
       iMod ("Hclose" with "[H]") as "_".
       { iRight; iLeft; auto. }
       iModIntro.
-      wp_if.
+      wp_pures.
       by iApply "HΦ"; iRight.
     - wp_cas_fail.
       iDestruct (own_valid_2 with "H Hγ") as %[].
@@ -127,19 +127,19 @@ Section side_channel.
       iMod ("Hclose" with "[H]") as "_".
       { by iRight; iLeft. }
       iModIntro.
-      wp_if. wp_proj.
+      wp_pures.
       iApply "HΦ"; iLeft; auto.
     - wp_cas_fail.
       iMod ("Hclose" with "[H]") as "_".
       { by iRight; iLeft. }
       iModIntro.
-      wp_if.
+      wp_pures.
       iApply "HΦ"; auto.
     - wp_cas_fail.
       iMod ("Hclose" with "[Hl Hγ]").
       { iRight; iRight; iFrame. }
       iModIntro.
-      wp_if.
+      wp_pures.
       iApply "HΦ"; auto.
   Qed.
 End side_channel.
@@ -181,7 +181,7 @@ Section mailbox.
       iMod ("Hclose" with "[Hnone]") as "_".
       { by iNext; iLeft. }
       iModIntro.
-      wp_let. wp_match.
+      wp_pures.
       iApply "HΦ"; auto.
     - iDestruct "Hsome" as (v' γ) "[Hl #Hoffer]".
       wp_load.
@@ -204,13 +204,13 @@ Section mailbox.
     iIntros (Φ) "[Hmailbox HP] HΦ"; iDestruct "Hmailbox" as (l) "[-> #Hmailbox]".
     wp_lam. wp_let. wp_apply (mk_offer_works with "HP").
     iIntros (offer γ) "[#Hoffer Hrevoke]".
-    wp_let. wp_bind (Store _ _).
+    wp_let. wp_bind (Store _ _). wp_pures.
     iInv N as "[HNone | HSome]" "Hclose".
     - wp_store.
       iMod ("Hclose" with "[HNone]") as "_".
       { by iNext; iRight; iExists _, _; iFrame. }
       iModIntro.
-      wp_let.
+      wp_pures.
       wp_apply (revoke_works with "[Hrevoke]"); first by iFrame.
       iIntros (v') "H"; iDestruct "H" as "[HSome | HNone]".
       * iApply ("HΦ" with "[HSome]"); by iLeft.
@@ -220,7 +220,7 @@ Section mailbox.
       iMod ("Hclose" with "[Hl]") as "_".
       { by iNext; iRight; iExists _, _; iFrame. }
       iModIntro.
-      wp_let.
+      wp_pures.
       wp_apply (revoke_works with "[Hrevoke]"); first by iFrame.
       iIntros (v'') "H"; iDestruct "H" as "[HSome | HNone]".
       * iApply ("HΦ" with "[HSome]"); by iLeft.
@@ -294,13 +294,12 @@ Section stack_works.
   Proof.
     rewrite -wp_fupd.
     wp_lam.
+    wp_alloc l as "Hl".
     wp_apply mk_mailbox_works; first done.
     iIntros (mailbox) "#Hmailbox".
-    wp_alloc l as "Hl".
     iMod (inv_alloc N _ (stack_inv P l) with "[Hl]") as "#Hinv".
     { by iNext; iExists _; iFrame; rewrite is_list_unfold; iLeft. }
-    iModIntro.
-    iExists _, _; auto.
+    wp_pures; iModIntro; iExists _, _; auto.
   Qed.
 
   Theorem push_works P s v :
@@ -319,7 +318,7 @@ Section stack_works.
       iMod ("Hclose" with "[Hl Hlist]") as "_".
       { iNext; iExists _; iFrame. }
       iModIntro.
-      wp_let. wp_alloc l' as "Hl'". wp_let. wp_bind (CAS _ _ _).
+      wp_let. wp_alloc l' as "Hl'". wp_pures. wp_bind (CAS _ _ _).
       iInv N as (list) "(Hl & Hlist)" "Hclose".
       destruct (decide (v'' = list)) as [ -> |].
       * iDestruct (is_list_unboxed with "Hlist") as "[>% Hlist]".
@@ -346,7 +345,7 @@ Section stack_works.
   Proof.
     iIntros (Φ) "Hstack HΦ". iDestruct "Hstack" as (mailbox l) "(-> & #Hmailbox & #Hstack)".
     iLöb as "IH".
-    wp_lam. wp_proj. wp_let. wp_proj. wp_lam.
+    wp_lam. wp_proj. wp_let. wp_proj. wp_pures.
     wp_apply get_works; first done.
     iIntros (ov) "[-> | HSome]".
     - wp_match. wp_bind (Load _).
@@ -367,7 +366,7 @@ Section stack_works.
         iMod ("Hclose" with "[Hl Hlist]") as "_".
         { iNext; iExists _; by iFrame. }
         iModIntro.
-        wp_let. wp_proj. wp_bind (CAS _ _ _).
+        wp_let. wp_proj. wp_bind (CAS _ _ _). wp_pures.
         iInv N as (v'') "[Hl Hlist]" "Hclose".
         destruct (decide (v'' = InjRV #l')) as [-> |].
         + rewrite is_list_unfold.
@@ -379,7 +378,7 @@ Section stack_works.
           iMod ("Hclose" with "[Hl Hlist]") as "_".
           { iNext; iExists _; by iFrame. }
           iModIntro.
-          wp_if. wp_proj.
+          wp_pures.
           iApply ("HΦ" with "[HP]"); iRight; iExists h; by iFrame.
         + wp_cas_fail.
           iMod ("Hclose" with "[Hl Hlist]") as "_".
@@ -388,7 +387,7 @@ Section stack_works.
           wp_if.
           iApply ("IH" with "HΦ").
     - iDestruct "HSome" as (v) "[-> HP]".
-      wp_match.
+      wp_pures.
       iApply "HΦ"; iRight; iExists _; auto.
   Qed.
 End stack_works.

theories/concurrent_stacks/concurrent_stack3.v

@@ -91,7 +91,7 @@ Section stack_works.
   Proof.
     iIntros (Φ) "HP HΦ".
     rewrite -wp_fupd.
-    wp_let. wp_alloc l as "Hl".
+    wp_lam. wp_alloc l as "Hl".
     iMod (inv_alloc N _ (stack_inv P l) with "[Hl HP]") as "#Hinv".
     { by iNext; iExists _, []; iFrame. }
     iModIntro; iApply "HΦ"; iExists _; auto.
@@ -104,14 +104,14 @@ Section stack_works.
   Proof.
     iIntros (Φ) "[Hstack Hupd] HΦ". iDestruct "Hstack" as (l) "[-> #Hinv]".
     iLöb as "IH".
-    wp_lam. wp_lam. wp_bind (Load _).
+    wp_lam. wp_pures. wp_bind (Load _).
     iInv N as (list xs) "(Hl & Hlist & HP)" "Hclose".
     wp_load.
     iMod ("Hclose" with "[Hl Hlist HP]") as "_".
     { iNext; iExists _, _; iFrame. }
     clear xs.
     iModIntro.
-    wp_let. wp_alloc l' as "Hl'". wp_let. wp_bind (CAS _ _ _).
+    wp_let. wp_alloc l' as "Hl'". wp_pures. wp_bind (CAS _ _ _).
     iInv N as (list' xs) "(Hl & Hlist & HP)" "Hclose".
     iDestruct (is_list_unboxed with "Hlist") as "[>% Hlist]".
     destruct (decide (list = list')) as [ -> |].
@@ -163,7 +163,7 @@ Section stack_works.
       iMod ("Hclose" with "[Hlist Hl HP]") as "_".
       { iNext; iExists _, _; iFrame. }
       iModIntro.
-      wp_let. wp_proj. wp_bind (CAS _ _ _).
+      wp_let. wp_proj. wp_bind (CAS _ _ _). wp_pures.
       iInv N as (v' xs'') "(Hl & Hlist & HP)" "Hclose".
       destruct (decide (v' = (SOMEV #l'))) as [ -> |].
       * wp_cas_suc.
@@ -176,8 +176,7 @@ Section stack_works.
         iMod ("Hclose" with "[Hlist Hl HP]") as "_".
         { iNext; iExists _, _; iFrame. }
         iModIntro.
-        wp_if.
-        wp_proj.
+        wp_pures.
         iApply ("HΦ" with "HΨ").
       * wp_cas_fail.
         iMod ("Hclose" with "[Hlist Hl HP]") as "_".

theories/concurrent_stacks/concurrent_stack4.v

@@ -97,7 +97,7 @@ Section proofs.
     iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
     iMod (inv_alloc Nside_channel _ (stages γ P Q l v) with "[Hl HP]") as "#Hinv".
     { iNext; iLeft; iFrame. }
-    iModIntro; iApply "HΦ"; iFrame; iExists _, _; auto.
+    wp_pures; iModIntro; iApply "HΦ"; iFrame; iExists _, _; auto.
   Qed.
 
   Lemma revoke_works γ P Q v :
@@ -106,20 +106,20 @@ Section proofs.
     {{{ v', RET v'; (∃ v'' : val, ⌜v' = InjRV v''⌝ ∗ can_push P Q v'') ∨ (⌜v' = InjLV #()⌝ ∗ (Q #())) }}}.
   Proof.
     iIntros (Φ) "[Hinv Hγ] HΦ". iDestruct "Hinv" as (v' l) "[-> #Hinv]".
-    wp_let. wp_proj. wp_bind (CAS _ _ _).
+    wp_lam. wp_pures. wp_bind (CAS _ _ _).
     iInv Nside_channel as "Hstages" "Hclose".
     iDestruct "Hstages" as "[[Hl HP] | [[Hl HQ] | [[Hl H] | [Hl H]]]]".
     - wp_cas_suc.
       iMod ("Hclose" with "[Hl Hγ]") as "_".
       { iNext; iRight; iRight; iFrame. }
       iModIntro.
-      wp_if. wp_proj.
+      wp_pures.
       by iApply "HΦ"; iLeft; iExists _; iFrame.
     - wp_cas_fail.
       iMod ("Hclose" with "[Hl Hγ]") as "_".
       { iNext; iRight; iRight; iLeft; iFrame. }
       iModIntro.
-      wp_if.
+      wp_pures.
       iApply ("HΦ" with "[HQ]"); iRight; auto.
     - wp_cas_fail.
       iDestruct (own_valid_2 with "H Hγ") as %[].
@@ -147,25 +147,25 @@ Section proofs.
       iMod ("Hclose" with "[Hl HQ]") as "_".
       { iRight; iLeft; iFrame. }
       iApply fupd_intro_mask; first done.
-      wp_if. wp_proj.
+      wp_pures.
       iApply "HΦ"; iLeft; auto.
     - wp_cas_fail.
       iMod ("Hclose" with "[Hl HQ]") as "_".
       { iRight; iLeft; iFrame. }
       iModIntro.
-      wp_if.
+      wp_pures.
       iApply "HΦ"; auto.
     - wp_cas_fail.
       iMod ("Hclose" with "[Hl Hγ]").
       { iRight; iRight; iFrame. }
       iModIntro.
-      wp_if.
+      wp_pures.
       iApply "HΦ"; auto.
     - wp_cas_fail.
       iMod ("Hclose" with "[Hl Hγ]").
       { iRight; iRight; iFrame. }
       iModIntro.
-      wp_if.
+      wp_pures.
       iApply "HΦ"; auto.
   Qed.
 
@@ -200,7 +200,7 @@ Section proofs.
       iMod ("Hclose" with "[Hnone]") as "_".
       { by iLeft. }
       iModIntro.
-      wp_let. wp_match.
+      wp_pures.
       iApply "HΦ"; iRight; by iFrame.
     - iDestruct "Hsome" as (v' γ Q) "[Hl #Hoffer]".
       wp_load.
@@ -218,20 +218,20 @@ Section proofs.
     iIntros (Φ) "[Hmail Hpush] HΦ". iDestruct "Hmail" as (l) "[-> #Hmail]".
     wp_lam. wp_let. wp_apply (mk_offer_works with "Hpush").
     iIntros (o γ) "[#Hoffer Hrev]".
-    wp_let. wp_bind (Store _ _).
+    wp_let. wp_bind (Store _ _). wp_pures.
     iInv Nmailbox as "[Hnone | Hsome]" "Hclose".
     - wp_store.
       iMod ("Hclose" with "[Hnone]") as "_".
       { iNext; iRight; iExists _, _, _; by iFrame. }
       iModIntro.
-      wp_let.
+      wp_pures.
       wp_apply (revoke_works with "[Hrev]"); first auto.
       iIntros (v') "H"; iApply "HΦ"; auto.
     - iDestruct "Hsome" as (? ? ?) "[Hl _]". wp_store.
       iMod ("Hclose" with "[Hl]") as "_".
       { iNext; iRight; iExists _, _, _; by iFrame. }
       iModIntro.
-      wp_let.
+      wp_pures.
       wp_apply (revoke_works with "[Hrev]"); first auto.
       iIntros (v') "H"; iApply "HΦ"; auto.
   Qed.
@@ -304,12 +304,12 @@ Section proofs.
   Proof.
     iIntros (Φ) "HP HΦ".
     rewrite -wp_fupd.
-    wp_let.
-    wp_apply mk_mailbox_works ; first done. iIntros (v) "#Hmailbox".
+    wp_lam.
     wp_alloc l as "Hl".
+    wp_apply mk_mailbox_works ; first done. iIntros (v) "#Hmailbox".
     iMod (inv_alloc Nstack _ (stack_inv P l) with "[Hl HP]") as "#Hinv".
     { by iNext; iExists _, []; iFrame. }
-    iModIntro; iApply "HΦ"; iExists _; auto.
+    wp_pures. iModIntro; iApply "HΦ"; iExists _; auto.
   Qed.
 
   Theorem push_works P s v Ψ :
@@ -319,7 +319,7 @@ Section proofs.
   Proof.
     iIntros (Φ) "[Hstack Hupd] HΦ". iDestruct "Hstack" as (mailbox l) "(-> & #Hmailbox & #Hinv)".
     iLöb as "IH" forall (v).
-    wp_lam. wp_lam. wp_proj. wp_let. wp_proj. wp_let.
+    wp_lam. wp_pures.
     wp_apply (put_works with "[Hupd]"); first auto. iIntros (o) "H".
     iDestruct "H" as "[Hsome | [-> HΨ]]".
     - iDestruct "Hsome" as (v') "[-> Hupd]".
@@ -331,7 +331,7 @@ Section proofs.
       { iNext; iExists _, _; iFrame. }
       clear xs.
       iModIntro.
-      wp_let. wp_alloc l' as "Hl'". wp_let. wp_bind (CAS _ _ _).
+      wp_let. wp_alloc l' as "Hl'". wp_pures. wp_bind (CAS _ _ _).
       iInv Nstack as (list' xs) "(Hl & Hlist & HP)" "Hclose".
       iDestruct (is_list_unboxed with "Hlist") as "[>% Hlist]".
       destruct (decide (list = list')) as [ -> |].
@@ -376,7 +376,7 @@ Section proofs.
       auto. }
     iIntros (ov) "[Hsome | [-> Hupdcons]]".
     - iDestruct "Hsome" as (v) "[-> HΨ]".
-      wp_match.
+      wp_pures.
       iApply ("HΦ" with "HΨ").
     - wp_match. wp_bind (Load _).
       iInv Nstack as (v xs) "(Hl & Hlist & HP)" "Hclose".
@@ -403,7 +403,7 @@ Section proofs.
         iMod ("Hclose" with "[Hlist Hl HP]") as "_".
         { iNext; iExists _, _; iFrame. }
         iModIntro.
-        wp_let. wp_proj. wp_bind (CAS _ _ _).
+        wp_pures. wp_bind (CAS _ _ _).
         iInv Nstack as (v' xs'') "(Hl & Hlist & HP)" "Hclose".
         destruct (decide (v' = (SOMEV #l'))) as [ -> |].
         + wp_cas_suc.
@@ -418,13 +418,13 @@ Section proofs.
           iMod ("Hclose" with "[Hlist Hl HP]") as "_".
           { iNext; iExists _, _; iFrame. }
           iModIntro.
-          wp_if. wp_proj.
+          wp_pures.
           iApply ("HΦ" with "HΨ").
         + wp_cas_fail.
           iMod ("Hclose" with "[Hlist Hl HP]") as "_".
           { iNext; iExists _, _; iFrame. }
           iModIntro.
-          wp_if.
+          wp_pures.
           iApply ("IH" with "Hupdcons Hupdnil HΦ").
   Qed.
 End proofs.