docs: complete invariant namespaces

docs/derived.tex

@@ -244,8 +244,6 @@ Let $\namesp \ni \textlog{InvNamesp} \eqdef \textlog{list}(\textlog{InvName})$ b
 Notice that there is an injection $\textlog{namesp\_inj}: \textlog{InvNamesp} \ra \textlog{InvName}$.
 Whenever needed (in particular, for masks at view shifts and Hoare triples), we coerce $\namesp$ to its suffix-closure: \[\namecl\namesp \eqdef \setComp{\iname}{\Exists \namesp'. \iname = \textlog{namesp\_inj}(\namesp' \dplus \namesp)}\]
 We use the notation $\namesp.\iname$ for the namespace $[\iname] \dplus \namesp$.
-We will overload the usual Iris notation for invariant assertions in the following:
-\[ \knowInv\namesp\prop \eqdef \Exists \iname \in \namecl\namesp. \knowInv\iname{\prop} \]
 
 We define the inclusion relation on namespaces as $\namesp_1 \sqsubseteq \namesp_2 \Lra \Exists \namesp_3. \namesp_2 = \namesp_3 \dplus \namesp_1$, \ie $\namesp_1$ is a suffix of $\namesp_2$.
 We have that $\namesp_1 \sqsubseteq \namesp_2 \Ra \namecl\namesp_2 \subseteq \namecl\namesp_1$.
@@ -253,7 +251,32 @@ We have that $\namesp_1 \sqsubseteq \namesp_2 \Ra \namecl\namesp_2 \subseteq \na
 Similarly, we define $\namesp_1 \sep \namesp_2 \eqdef   \Exists \namesp_1', \namesp_2'. \namesp_1' \sqsubseteq \namesp_1 \land \namesp_2' \sqsubseteq \namesp_2 \land |\namesp_1'| = |\namesp_2'| \land \namesp_1' \neq \namesp_2'$, \ie there exists a distinguishing suffix.
 We have that $\namesp_1 \sep \namesp_2 \Ra \namecl\namesp_2 \sep \namecl\namesp_1$, and furthermore $\iname_1 \neq \iname_2 \Ra \namesp.\iname_1 \sep \namesp.\iname_2$.
 
-\ralf{Give derived rules for invariants.}
+We will overload the usual Iris notation for invariant assertions in the following:
+\[ \knowInv\namesp\prop \eqdef \Exists \iname \in \namecl\namesp. \knowInv\iname{\prop} \]
+We can now derive the following rules for this derived form of the invariant assertion:
+\begin{mathpar}
+  \axiom{\knowInv\namesp\prop \proves \always\knowInv\namesp\prop}
+
+  \axiom{\later\prop \proves \pvs[\namesp] \knowInv\namesp\prop}
+
+  \infer{\physatomic{\expr} \and \namesp \subseteq \mask \and
+    \pfctx \proves \knowInv\namesp\prop \and
+    \pfctx \proves \later\prop \wand \wpre\expr[\mask \setminus \namesp]{\Ret\val.\later\prop * \propB}}
+  {\pfctx \proves \wpre\expr[\mask]{\Ret\val.\propB}}
+
+  \infer{\namesp \subseteq \mask \and
+    \pfctx \proves \knowInv\namesp\prop \and
+    \pfctx \proves \later\prop \wand \pvs[\mask \setminus \namesp]{\later\prop * \propB}}
+  {\pfctx \proves \pvs[\mask]{\propB}}
+
+  \infer{\physatomic{\expr} \and \namesp \subseteq \mask \and
+    \hoare{\later\prop*\propB}\expr{\Ret\val.\later\prop*\propC}[\mask \setminus \namesp]}
+  {\knowInv\namesp\prop \proves \hoare\propB\expr{\Ret\val.\propC}[\mask]}
+
+  \infer{\namesp \subseteq \mask \and
+    \later\prop*\propB \vs[\mask \setminus \namesp] \later\prop*\propC}
+  {\knowInv\namesp\prop \proves \propB \vs[\mask] \propC}
+\end{mathpar}
 
 % \subsection{STSs with interpretation}\label{sec:stsinterp}
 

program_logic/hoare.v

@@ -113,4 +113,19 @@ Proof.
   rewrite (comm _ _ (▷ R)%I); setoid_rewrite (comm _ _ R).
   apply ht_frame_step_l.
 Qed.
+
+Lemma ht_inv N E P Φ R e :
+  atomic e → nclose N ⊆ E →
+  (inv N R ★ {{ ▷ R ★ P }} e @ E ∖ nclose N {{ λ v, ▷ R ★ Φ v }})
+    ⊢ {{ P }} e @ E {{ Φ }}.
+Proof.
+  intros; apply: always_intro. apply impl_intro_l.
+  rewrite always_and_sep_r assoc [(P ★ _)%I]comm -assoc.
+  eapply wp_inv; [by eauto with I..|].
+  rewrite sep_elim_r. apply wand_intro_l.
+  (* Oh wow, this is annyoing... *)
+  rewrite assoc -always_and_sep_r'.
+  by rewrite /ht always_elim impl_elim_r.
+Qed.
+
 End hoare.

program_logic/invariants.v

@@ -54,14 +54,14 @@ Qed.
 
 (* Derive the concrete forms for pvs and wp, because they are useful. *)
 
-Lemma pvs_open_close E N P Q R :
+Lemma pvs_inv E N P Q R :
   nclose N ⊆ E →
   R ⊢ inv N P →
   R ⊢ (▷ P -★ |={E ∖ nclose N}=> (▷ P ★ Q)) →
   R ⊢ (|={E}=> Q).
 Proof. intros. by apply: (inv_fsa pvs_fsa). Qed.
 
-Lemma wp_open_close E e N P Φ R :
+Lemma wp_inv E e N P Φ R :
   atomic e → nclose N ⊆ E →
   R ⊢ inv N P →
   R ⊢ (▷ P -★ WP e @ E ∖ nclose N {{ λ v, ▷ P ★ Φ v }}) →

program_logic/viewshifts.v

@@ -87,13 +87,13 @@ Qed.
 Lemma vs_mask_frame' E Ef P Q : Ef ∩ E = ∅ → (P ={E}=> Q) ⊢ (P ={E ∪ Ef}=> Q).
 Proof. intros; apply vs_mask_frame; set_solver. Qed.
 
-Lemma vs_open_close N E P Q R :
+Lemma vs_inv N E P Q R :
   nclose N ⊆ E →
   (inv N R ★ (▷ R ★ P ={E ∖ nclose N}=> ▷ R ★ Q)) ⊢ (P ={E}=> Q).
 Proof.
   intros; apply: always_intro. apply impl_intro_l.
   rewrite always_and_sep_r assoc [(P ★ _)%I]comm -assoc.
-  eapply pvs_open_close; [by eauto with I..|].
+  eapply pvs_inv; [by eauto with I..|].
   rewrite sep_elim_r. apply wand_intro_l.
   (* Oh wow, this is annyoing... *)
   rewrite assoc -always_and_sep_r'.