use a nicer formulation for the strange mask-changing view shift intro

docs/program-logic.tex

@@ -106,40 +106,37 @@ View updates satisfy the following basic proof rules:
 
 \infer[vup-intro-mask]
 {\mask_2 \subseteq \mask_1}
-{(\pvs[\mask_2][\mask_1]\TRUE) \wand \prop \proves \pvs[\mask_1][\mask_2] \prop}
+{\prop \proves \pvs[\mask_1][\mask_2]\pvs[\mask_2][\mask_1] \prop}
 
 \infer[vup-trans]
 {}
 {\pvs[\mask_1][\mask_2] \pvs[\mask_2][\mask_3] \prop \proves \pvs[\mask_1][\mask_3] \prop}
 
+\infer[vup-upd]
+{}{\upd\prop \proves \pvs[\mask] \prop}
+
 \infer[vup-frame]
-{}{\propB * \pvs[\mask_1][\mask_2]\prop \proves \pvs[\mask_1][\mask_2] \propB * \prop}
+{}{\propB * \pvs[\mask_1][\mask_2]\prop \proves \pvs[\mask_1 \uplus \mask_\f][\mask_2 \uplus \mask_\f] \propB * \prop}
 
 \inferH{vup-update}
 {\melt \mupd \meltsB}
 {\ownM\melt \proves \pvs[\mask] \Exists\meltB\in\meltsB. \ownM\meltB}
 
-\infer[vup-upd]
-{}{\upd\prop \proves \pvs[\mask] \prop}
-
 \infer[vup-timeless]
 {\timeless\prop}
 {\later\prop \proves \pvs[\mask] \prop}
-
-\infer[vup-mask-frame]
-{}{\pvs[\mask_1][\mask_2] \prop \proves \pvs[\mask_1 \uplus \mask_\f][\mask_2 \uplus \mask_\f] \prop}
-
-\inferH{vup-allocI}
-{\text{$\mask$ is infinite}}
-{\later\prop \proves \pvs[\mask] \Exists \iname \in \mask. \knowInv\iname\prop}
-
-\inferH{vup-openI}
-{}{\knowInv\iname\prop \proves \pvs[\set\iname][\emptyset] \later\prop}
-
-\inferH{vup-closeI}
-{}{\knowInv\iname\prop \land \later\prop \proves \pvs[\emptyset][\set\iname] \TRUE}
-
+%
+% \inferH{vup-allocI}
+% {\text{$\mask$ is infinite}}
+% {\later\prop \proves \pvs[\mask] \Exists \iname \in \mask. \knowInv\iname\prop}
+%gov
+% \inferH{vup-openI}
+% {}{\knowInv\iname\prop \proves \pvs[\set\iname][\emptyset] \later\prop}
+%
+% \inferH{vup-closeI}
+% {}{\knowInv\iname\prop \land \later\prop \proves \pvs[\emptyset][\set\iname] \TRUE}
 \end{mathpar}
+(There are no rules related to invariants here. Those rules will be discussed later, in \Sref{sec:invariants}.)
 
 We further define the notions of \emph{view shifts} and \emph{linear view shifts}:
 \begin{align*}
@@ -172,17 +169,17 @@ Still, just to give an idea of what view shifts ``are'', here are some proof rul
 \inferH{vs-timeless}
   {\timeless{\prop}}
   {\later \prop \vs \prop}
-\and
-\inferH{vs-allocI}
-  {\infinite(\mask)}
-  {\later{\prop} \vs[\mask] \exists \iname\in\mask.\; \knowInv{\iname}{\prop}}
-\and
-\axiomH{vs-openI}
-  {\knowInv{\iname}{\prop} \proves \TRUE \vs[\{ \iname \} ][\emptyset] \later \prop}
-\and
-\axiomH{vs-closeI}
-  {\knowInv{\iname}{\prop} \proves \later \prop \vs[\emptyset][\{ \iname \} ] \TRUE }
 
+% \inferH{vs-allocI}
+%   {\infinite(\mask)}
+%   {\later{\prop} \vs[\mask] \exists \iname\in\mask.\; \knowInv{\iname}{\prop}}
+% \and
+% \axiomH{vs-openI}
+%   {\knowInv{\iname}{\prop} \proves \TRUE \vs[\{ \iname \} ][\emptyset] \later \prop}
+% \and
+% \axiomH{vs-closeI}
+%   {\knowInv{\iname}{\prop} \proves \later \prop \vs[\emptyset][\{ \iname \} ] \TRUE }
+%
 \inferHB{vs-disj}
   {\prop \vs[\mask_1][\mask_2] \propC \and \propB \vs[\mask_1][\mask_2] \propC}
   {\prop \lor \propB \vs[\mask_1][\mask_2] \propC}
@@ -282,6 +279,9 @@ Still, for a more traditional presentation, we can easily derive the notion of a
 \hoare{\prop}{\expr}{\Ret\val.\propB}[\mask] \eqdef \always{(\prop \Ra \wpre{\expr}[\mask]{\Ret\val.\propB})}
 \]
 
+\subsection{Invariant Namespaces}
+\label{sec:invariants}
+
 \subsection{Lost stuff}
 \ralf{TODO: Right now, this is a dump of all the things that moved out of the base...}
 

program_logic/pviewshifts.v

@@ -47,32 +47,37 @@ Proof. rewrite pvs_eq. solve_proper. Qed.
 Global Instance pvs_proper E1 E2 : Proper ((≡) ==> (≡)) (@pvs Λ Σ _ E1 E2).
 Proof. apply ne_proper, _. Qed.
 
-Lemma pvs_intro' E1 E2 P : E2 ⊆ E1 → ((|={E2,E1}=> True) -★ P) ={E1,E2}=> P.
+Lemma pvs_intro_mask E1 E2 P : E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P.
 Proof.
   intros (E1''&->&?)%subseteq_disjoint_union_L.
-  rewrite pvs_eq /pvs_def ownE_op //; iIntros "H ($ & $ & HE) !==>".
-  iApply except_last_intro. iApply "H".
-  iIntros "[$ $] !==>". by iApply except_last_intro.
+  rewrite pvs_eq /pvs_def ownE_op //. iIntros "H ($ & $ & HE) !==>".
+  iApply except_last_intro. iIntros "[$ $] !==>" . iApply except_last_intro.
+  by iFrame.
 Qed.
+
 Lemma except_last_pvs E1 E2 P : ◇ (|={E1,E2}=> P) ={E1,E2}=> P.
 Proof.
   rewrite pvs_eq. iIntros "H [Hw HE]". iTimeless "H". iApply "H"; by iFrame.
 Qed.
+
 Lemma rvs_pvs E P : (|=r=> P) ={E}=> P.
 Proof.
   rewrite pvs_eq /pvs_def. iIntros "H [$ $]"; iVs "H".
   iVsIntro. by iApply except_last_intro.
 Qed.
+
 Lemma pvs_mono E1 E2 P Q : (P ⊢ Q) → (|={E1,E2}=> P) ={E1,E2}=> Q.
 Proof.
   rewrite pvs_eq /pvs_def. iIntros (HPQ) "HP HwE".
   rewrite -HPQ. by iApply "HP".
 Qed.
+
 Lemma pvs_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P) ={E1,E3}=> P.
 Proof.
   rewrite pvs_eq /pvs_def. iIntros "HP HwE".
   iVs ("HP" with "HwE") as ">(Hw & HE & HP)". iApply "HP"; by iFrame.
 Qed.
+
 Lemma pvs_mask_frame_r' E1 E2 Ef P :
   E1 ⊥ Ef → (|={E1,E2}=> E2 ⊥ Ef → P) ={E1 ∪ Ef,E2 ∪ Ef}=> P.
 Proof.
@@ -81,6 +86,7 @@ Proof.
   iDestruct (ownE_op' with "[HE2 HEf]") as "[? $]"; first by iFrame.
   iVsIntro; iApply except_last_intro. by iApply "HP".
 Qed.
+
 Lemma pvs_frame_r E1 E2 P Q : (|={E1,E2}=> P) ★ Q ={E1,E2}=> P ★ Q.
 Proof. rewrite pvs_eq /pvs_def. by iIntros "[HwP $]". Qed.
 
@@ -103,6 +109,11 @@ 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.