Fix the pvs_intro', bring back the redundant always, and others fixes

IRIS_VERSION

-a0fc612e5c81bbff25f63938b50f448ecc056c68
+a90ab674afeee9f4525a4bf233b2a7e48530eaf2

atomic.v

-From iris.program_logic Require Export hoare weakestpre pviewshifts ownership.
+From iris.program_logic Require Export hoare weakestpre pviewshifts.
 From iris.prelude Require Export coPset.
 Import uPred.
 

atomic_incr.v

+From iris.program_logic Require Export weakestpre wsat.
 From iris.heap_lang Require Export lang proofmode notation.
 From iris_atomic Require Import atomic.
+From iris.proofmode Require Import tactics.
+From iris.prelude Require Import coPset.
 
 Section incr.
   Context `{!heapG Σ} (N : namespace).
@@ -82,12 +85,8 @@ Section user.
       (* open the invariant *)
       iInv N as (x') ">Hl'" "Hclose".
       (* mask magic *)
-      iApply pvs_intro'.
-      { apply ndisj_subseteq_difference; auto. }
-      iIntros "Hvs".
-      iExists x'.
-      iFrame "Hl'".
-      iSplit.
+      iVs (pvs_intro_mask' (⊤ ∖ nclose N) heapN) as "Hvs"; first set_solver.
+      iVsIntro. iExists x'. iFrame "Hl'". iSplit.
       + (* provide a way to rollback *)
         iIntros "Hl'".
         iVs "Hvs". iVs ("Hclose" with "[Hl']"); eauto.
@@ -95,11 +94,10 @@ Section user.
         iIntros (v) "[Heq Hl']".
         iVs "Hvs". iVs ("Hclose" with "[Hl']"); eauto.
     - iDestruct "Hincr" as "#HIncr".
-      iSplitL; [|iSplitL]; try (iApply wp_wand_r;iSplitL; [by iApply "HIncr"|auto]).
+      iSplitL; [|iSplitL];
+        try (iApply wp_wand_r; iSplitL; [by iApply "HIncr"|auto]).
       iIntros (v1 v2) "_ !>".
-      wp_seq.
-      iInv N as (x') ">Hl" "Hclose".
-      wp_load.
-      iApply "Hclose". eauto.
+      wp_seq. iInv N as (x') ">Hl" "Hclose".
+      wp_load. iApply "Hclose". eauto.
   Qed.
 End user.

atomic_sync.v

@@ -26,7 +26,7 @@ Section atomic_sync.
                                  (fun g v => ∃ g':A, gHalf γ g' ★ β x g g' v)
                                  Ei Eo
                                 (f x) (P x) (fun _ => Q x))%I.
-       
+
   Definition sync (mk_syncer: val) : val :=
     λ: "f_seq" "l",
        let: "s" := mk_syncer #() in
@@ -37,9 +37,14 @@ Section atomic_sync.
          {{ True }} f l {{ f', ■ (∀ (x: val) (Φ: val → iProp Σ) (g: A),
                                heapN ⊥ N →
                                heap_ctx ★ ϕ l g ★ □ α x ★
-                               (∀ (v: val) (g': A), ϕ l g' -★ β x g g' v -★ |={E}=> Φ v)
+                               (∀ (v: val) (g': A),
+                                  ϕ l g' -★ β x g g' v ={E}=★ Φ v)
                                ⊢ WP f' x @ E {{ Φ }} )}}.
-  
+  (* XXX (zgzehen): The linear VS in the above post-condition is for the final step
+     of computation. The client side of such triple will have to prove that the
+     specific post-condition he wants can be lvs'd from whatever threaded together
+     by magic wands. The library side ... *)
+
   Lemma atomic_spec (mk_syncer f_seq l: val) (ϕ: val → A → iProp Σ) α β Ei:
       ∀ (g0: A),
         heapN ⊥ N → seq_spec f_seq ϕ α β ⊤ →
@@ -66,11 +71,11 @@ Section atomic_sync.
     rewrite /atomic_triple'.
     iIntros (P Q) "#Hvss".
     rewrite /synced.
-    iSpecialize ("Hsynced" $! P Q x). 
+    iSpecialize ("Hsynced" $! P Q x).
     iIntros "!# HP". iApply wp_wand_r. iSplitL "HP".
     - iApply ("Hsynced" with "[]")=>//.
       iAlways. iIntros "[HR HP]". iDestruct "HR" as (g) "[Hϕ Hg1]".
-      (* we should view shift at this point *) 
+      (* we should view shift at this point *)
       iDestruct ("Hvss" with "HP") as "Hvss'". iApply pvs_wp.
       iVs "Hvss'". iDestruct "Hvss'" as (?) "[[Hg2 #Hα] [Hvs1 _]]".
       iVs ("Hvs1" with "[Hg2]") as "HP"; first by iFrame.

flat.v

@@ -405,7 +405,7 @@ Section proof.
     iFrame "Hh Hm". iIntros (γ s) "#Hss".
     wp_let. iVsIntro. iApply "HΦ". rewrite /synced.
     iAlways.
-    iIntros (f). wp_let. iVsIntro.
+    iIntros (f). wp_let. iVsIntro. iAlways.
     iIntros (P Q x) "#Hf".
     iIntros "!# Hp". wp_let.
     wp_bind (install _ _ _).

peritem.v

@@ -140,12 +140,9 @@ Lemma new_stack_spec' Φ RI:
       iDestruct (extract_is_list with "[Hxs]") as "==>[Hxs Hxs']"; first by iFrame.
       iDestruct (dup_is_list with "[Hxs']") as "[Hxs'1 Hxs'2]"; first by iFrame.
       (* mask magic *)
-      iApply pvs_intro'.
-      { apply ndisj_subseteq_difference; auto. }
-      iIntros "Hvs".
-      iExists (xs, hd).
-      iFrame "Hs Hxs'1".
-      iSplit.
+      iVs (pvs_intro_mask' (⊤ ∖ nclose N) heapN) as "Hvs"; first set_solver.
+      iVsIntro. iExists (xs, hd).
+      iFrame "Hs Hxs'1". iSplit.
       + (* provide a way to rollback *)
         iIntros "[Hs Hl']".
         iVs "Hvs". iVs ("Hclose" with "[-Rx]"); last done.

simple_sync.v

@@ -28,7 +28,7 @@ Section syncer.
     iSplitR "HR HΦ"; first done.
     iFrame "HR".
     iIntros (lk γ) "#Hl". wp_let. iApply "HΦ". iIntros "!#".
-    iIntros (f). wp_let. iVsIntro.
+    iIntros (f). wp_let. iVsIntro. iAlways.
     iIntros (P Q x) "#Hf !# HP".
     wp_let. wp_bind (acquire _).
     iApply acquire_spec. iSplit; first done.

sync.v

@@ -4,15 +4,15 @@ From iris.heap_lang Require Import proofmode notation.
 
 Section sync.
   Context `{!heapG Σ} (N : namespace).
-  
+
   Definition synced R (f' f: val) :=
-    (∀ P Q (x: val), ({{ R ★ P x }} f x {{ v, R ★ Q x v }}) → ({{ P x }} f' x {{ v, Q x v }}))%I.
+    (□ ∀ P Q (x: val), ({{ R ★ P x }} f x {{ v, R ★ Q x v }}) → ({{ P x }} f' x {{ v, Q x v }}))%I.
 
   Definition is_syncer (R: iProp Σ) (s: val) :=
-    (∀ (f : val), WP s f {{ f', synced R f' f }})%I.
+    (□ ∀ (f : val), WP s f {{ f', synced R f' f }})%I.
 
   Definition mk_syncer_spec (mk_syncer: val) :=
     ∀ (R: iProp Σ) (Φ: val -> iProp Σ),
       heapN ⊥ N →
-      heap_ctx ★ R ★ (∀ s, □ (is_syncer R s) -★ Φ s) ⊢ WP mk_syncer #() {{ Φ }}.
+      heap_ctx ★ R ★ (∀ s, is_syncer R s -★ Φ s) ⊢ WP mk_syncer #() {{ Φ }}.
 End sync.