Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

docs/program-logic.tex

@@ -96,7 +96,7 @@ The following assertion states that an invariant with name $\iname$ exists and m
 Next, we define \emph{view updates}, which are essentially the same as the resource updates of the base logic ($\Sref{sec:base-logic}$), except that they also have access to world satisfaction and can enable and disable invariants:
 \[ \pvs[\mask_1][\mask_2] \prop \eqdef W * \ownGhost{\gname_{\textmon{En}}}{\mask_1} \wand \upd\diamond (W * \ownGhost{\gname_{\textmon{En}}}{\mask_2} * \prop) \]
 Here, $\mask_1$ and $\mask_2$ are the \emph{masks} of the view update, defining which invariants have to be (at least!) available before and after the update.
-We use $\top$ as symbol for the largest possible mask, $\mathbb N$.
+We use $\top$ as symbol for the largest possible mask, $\mathbb N$, and $\bot$ for the smallest possible mask $\emptyset$.
 We will write $\pvs[\mask] \prop$ for $\pvs[\mask][\mask]\prop$.
 %
 View updates satisfy the following basic proof rules:

program_logic/lifting.v

@@ -35,8 +35,8 @@ Lemma wp_lift_pure_step E Φ e1 :
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
   iIntros (He Hsafe Hstep) "H". rewrite wp_unfold /wp_pre; iRight; iSplit; auto.
-  iIntros (σ1) "Hσ". iApply pvs_intro'; [set_solver|iIntros "Hclose"].
-  iSplit; [done|]; iNext; iIntros (e2 σ2 efs ?).
+  iIntros (σ1) "Hσ". iVs (pvs_intro_mask' E ∅) as "Hclose"; first set_solver.
+  iVsIntro. iSplit; [done|]; iNext; iIntros (e2 σ2 efs ?).
   destruct (Hstep σ1 e2 σ2 efs); auto; subst.
   iVs "Hclose"; iVsIntro. iFrame "Hσ". iApply "H"; auto.
 Qed.
@@ -51,7 +51,7 @@ Lemma wp_lift_atomic_step {E Φ} e1 σ1 :
 Proof.
   iIntros (Hatomic ?) "[Hσ H]".
   iApply (wp_lift_step E _ e1); eauto using reducible_not_val.
-  iApply pvs_intro'; [set_solver|iIntros "Hclose"].
+  iVs (pvs_intro_mask' E ∅) as "Hclose"; first set_solver. iVsIntro.
   iExists σ1. iFrame "Hσ"; iSplit; eauto.
   iNext; iIntros (e2 σ2 efs) "[% Hσ]".
   edestruct (Hatomic σ1 e2 σ2 efs) as [v2 <-%of_to_val]; eauto.

program_logic/pviewshifts.v

@@ -99,6 +99,8 @@ Proof. intros P Q; apply pvs_mono. Qed.
 
 Lemma pvs_intro E P : P ={E}=> P.
 Proof. iIntros "HP". by iApply rvs_pvs. Qed.
+Lemma pvs_intro_mask' E1 E2 : E2 ⊆ E1 → True ⊢ |={E1,E2}=> |={E2,E1}=> True.
+Proof. exact: pvs_intro_mask. Qed.
 Lemma pvs_except_last E1 E2 P : (|={E1,E2}=> ◇ P) ={E1,E2}=> P.
 Proof. by rewrite {1}(pvs_intro E2 P) except_last_pvs pvs_trans. Qed.
 
@@ -109,11 +111,6 @@ Proof. by rewrite pvs_frame_l wand_elim_l. Qed.
 Lemma pvs_wand_r E1 E2 P Q : (|={E1,E2}=> P) ★ (P -★ Q) ={E1,E2}=> Q.
 Proof. by rewrite pvs_frame_r wand_elim_r. Qed.
 
-Lemma pvs_intro' E1 E2 P : E2 ⊆ E1 → ((|={E2,E1}=> True) -★ P) ={E1,E2}=> P.
-Proof.
-  iIntros (?) "Hw". iApply pvs_wand_l. iFrame. by iApply pvs_intro_mask.
-Qed.
-
 Lemma pvs_trans_frame E1 E2 E3 P Q :
   ((Q ={E2,E3}=★ True) ★ |={E1,E2}=> (Q ★ P)) ={E1,E3}=> P.
 Proof.

program_logic/weakestpre.v

@@ -96,7 +96,7 @@ Proof.
   { iDestruct "Hv" as (v) "[% Hv]". iExists v; iSplit; first done.
     iApply ("HΦ" with "==>[-]"). by iApply (pvs_mask_mono E1 _). }
   iSplit; [done|]; iIntros (σ1) "Hσ".
-  iApply (pvs_trans _ E1); iApply pvs_intro'; auto. iIntros "Hclose".
+  iVs (pvs_intro_mask' E2 E1) as "Hclose"; first done.
   iVs ("H" $! σ1 with "Hσ") as "[$ H]".
   iVsIntro. iNext. iIntros (e2 σ2 efs Hstep).
   iVs ("H" $! _ σ2 efs with "[#]") as "($ & H & $)"; auto.

tests/atomic.v

@@ -125,18 +125,15 @@ Section user.
       (* open the invariant *)
       iInv N as (x') ">Hl'" "Hclose".
       (* mask magic *)
-      iApply pvs_intro'.
+      iVs (pvs_intro_mask' _ heapN) as "Hclose'".
       { apply ndisj_subseteq_difference; auto. }
-      iIntros "Hvs".
-      iExists x'.
-      iFrame "Hl'".
-      iSplit.
+      iVsIntro. iExists x'. iFrame "Hl'". iSplit.
       + (* provide a way to rollback *)
         iIntros "Hl'".
-        iVs "Hvs". iVs ("Hclose" with "[Hl']"); eauto.
+        iVs "Hclose'". iVs ("Hclose" with "[Hl']"); eauto.
       + (* provide a way to commit *)
         iIntros (v) "[Heq Hl']".
-        iVs "Hvs". iVs ("Hclose" with "[Hl']"); eauto.
+        iVs "Hclose'". iVs ("Hclose" with "[Hl']"); eauto.
     - iDestruct "Hincr" as "#HIncr".
       iSplitL; [|iSplitL]; try (iApply wp_wand_r;iSplitL; [by iApply "HIncr"|auto]).
       iIntros (v1 v2) "_ !>".