docs: derived lifting rules

docs/derived.tex

@@ -205,9 +205,64 @@ The following rules can be derived for Hoare triples.
 \end{mathparpagebreakable}
 
 \paragraph{Lifting of operational semantics.}
-We can derive some specialized forms of the lifting axioms for the operational semantics, as well as some forms that involve view shifts and Hoare triples.
+We can derive some specialized forms of the lifting axioms for the operational semantics.
+\begin{mathparpagebreakable}
+  \infer[wp-lift-atomic-step]
+  {\toval(\expr_1) = \bot \and
+   \red(\expr_1, \state_1) \and
+   \All \expr_2, \state_2, \expr_f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_f \Ra \Exists\val_2. \toval(\expr_2) = \val_2 \land \pred(\val_2,\state_2,\expr_f)}
+  {\later\ownPhys{\state_1} * \later\All \val, \state_2, \expr_f. \pred(\val, \state_2, \expr_f) \land \ownPhys{\state_2} \wand \prop * \wpre{\expr_f}[\top]{\Ret\any.\TRUE} \proves \wpre{\expr_1}[\mask_1]{\Ret\val.\prop}}
+
+  \infer[wp-lift-atomic-det-step]
+  {\toval(\expr_1) = \bot \and
+   \red(\expr_1, \state_1) \and
+   \All \expr'_2, \state'_2, \expr_f'. \expr_1,\state_1 \step \expr_2,\state_2,\expr_f \Ra \state_2 = \state_2' \land \toval(\expr_2') = \val_2 \land \expr_f = \expr_f'}
+  {\later\ownPhys{\state_1} * \later(\ownPhys{\state_2} \wand \prop[\val_2/\var] * \wpre{\expr_f}[\top]{\Ret\any.\TRUE}) \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}}
+
+  \infer[wp-lift-pure-det-step]
+  {\toval(\expr_1) = \bot \and
+   \All \state_1. \red(\expr_1, \state_1) \and
+   \All \state_1, \expr_2', \state_2, \expr_f'. \expr_1,\state_1 \step \expr_2,\state_2,\expr_f \Ra \state_1 = \state_2 \land \expr_2 = \expr_2' \land \expr_f = \expr_f'}
+  {\later ( \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \wpre{\expr_f}[\top]{\Ret\any.\TRUE}) \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}}
+\end{mathparpagebreakable}
 
-\ralf{Add these.}
+Furthermore, we derive some forms that directly involve view shifts and Hoare triples.
+\begin{mathparpagebreakable}
+  \infer[ht-lift-step]
+  {\mask_2 \subseteq \mask_1 \and
+   \toval(\expr_1) = \bot \and
+   \red(\expr_1, \state_1) \and
+   \All \expr_2, \state_2, \expr_f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_f \Ra \pred(\expr_2,\state_2,\expr_f) \\\\
+   \prop \vs[\mask_1][\mask_2] \later\ownPhys{\state_1} * \later\prop' \and
+   \All \expr_2, \state_2, \expr_f. \pred(\expr_2, \state_2, \expr_f) * \ownPhys{\state_2} * \prop' \vs[\mask_2][\mask_1] \propB_1 * \propB_2 \\\\
+   \All \expr_2, \state_2, \expr_f. \hoare{\propB_1}{\expr_2}{\Ret\val.\propC}[\mask_1] \and
+   \All \expr_2, \state_2, \expr_f. \hoare{\propB_2}{\expr_f}{\Ret\any. \TRUE}[\top]}
+  { \hoare\prop{\expr_1}{\Ret\val.\propC}[\mask_1] }
+
+  \infer[ht-lift-atomic-step]
+  {\atomic(\expr_1) \and
+   \red(\expr_1, \state_1) \and
+   \All \expr_2, \state_2, \expr_f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_f \Ra \pred(\expr_2,\state_2,\expr_f) \\\\
+   \prop \vs[\mask_1][\mask_2] \later\ownPhys{\state_1} * \later\prop' \and
+   \All \expr_2, \state_2, \expr_f. \hoare{\pred(\expr_2,\state_2,\expr_f) * \prop}{\expr_f}{\Ret\any. \TRUE}[\top]}
+  { \hoare{\later\ownPhys{\state_1} * \later\prop}{\expr_1}{\Ret\val.\Exists \state_2, \expr_f. \ownPhys{\state_2} * \pred(\ofval(\expr_2),\state_2,\expr_f)}[\mask_1] }
+
+  \infer[ht-lift-pure-step]
+  {\toval(\expr_1) = \bot \and
+   \All\state_1. \red(\expr_1, \state_1) \and
+   \All \state_1, \expr_2, \state_2, \expr_f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_f \Ra \state_1 = \state_2 \land \pred(\expr_2,\expr_f) \\\\
+   \All \expr_2, \expr_f. \hoare{\pred(\expr_2,\expr_f) * \prop}{\expr_2}{\Ret\val.\propB}[\mask_1] \and
+   \All \expr_2, \expr_f. \hoare{\pred(\expr_2,\expr_f) * \prop'}{\expr_f}{\Ret\any. \TRUE}[\top]}
+  { \hoare{\later(\prop*\prop')}{\expr_1}{\Ret\val.\propB}[\mask_1] }
+
+  \infer[ht-lift-pure-det-step]
+  {\toval(\expr_1) = \bot \and
+   \All\state_1. \red(\expr_1, \state_1) \and
+   \All \state_1, \expr_2', \state_2, \expr_f'. \expr_1,\state_1 \step \expr_2,\state_2,\expr_f \Ra \state_1 = \state_2 \land \expr_2 = \expr_2' \land \expr_f = \expr_f' \\\\
+   \hoare{\prop}{\expr_2}{\Ret\val.\propB}[\mask_1] \and
+   \hoare{\prop'}{\expr_f}{\Ret\any. \TRUE}[\top]}
+  { \hoare{\later(\prop*\prop')}{\expr_1}{\Ret\val.\propB}[\mask_1] }
+\end{mathparpagebreakable}
 
 \subsection{Global functor and ghost ownership}
 

docs/logic.tex

@@ -7,7 +7,7 @@ A \emph{language} $\Lang$ consists of a set \textdom{Expr} of \emph{expressions}
 \end{mathpar}
 \item There exists a \emph{primitive reduction relation} \[(-,- \step -,-,-) \subseteq \textdom{Expr} \times \textdom{State} \times \textdom{Expr} \times \textdom{State} \times (\textdom{Expr} \uplus \set{\bot})\]
   We will write $\expr_1, \state_1 \step \expr_2, \state_2$ for $\expr_1, \state_1 \step \expr_2, \state_2, \bot$. \\
-  A reduction $\expr_1, \state_1 \step \expr_2, \state_2, \expr'$ indicates that, when $\expr_1$ reduces to $\expr$, a \emph{new thread} $\expr'$ is forked off.
+  A reduction $\expr_1, \state_1 \step \expr_2, \state_2, \expr_f$ indicates that, when $\expr_1$ reduces to $\expr$, a \emph{new thread} $\expr_f$ is forked off.
 \item All values are stuck:
 \[ \expr, \_ \step  \_, \_, \_ \Ra \toval(\expr) = \bot \]
 \item There is a predicate defining \emph{atomic} expressions satisfying
@@ -16,7 +16,7 @@ A \emph{language} $\Lang$ consists of a set \textdom{Expr} of \emph{expressions}
   {\All\expr. \atomic(\expr) \Ra \toval(\expr) = \bot} \and
   {{
     \begin{inbox}
-\All\expr_1, \state_1, \expr_2, \state_2, \expr'. \atomic(\expr_1) \land \expr_1, \state_1 \step \expr_2, \state_2, \expr' \Ra {}\\\qquad\qquad\qquad\quad~~ \Exists \val_2. \toval(\expr_2) = \val_2
+\All\expr_1, \state_1, \expr_2, \state_2, \expr_f. \atomic(\expr_1) \land \expr_1, \state_1 \step \expr_2, \state_2, \expr_f \Ra {}\\\qquad\qquad\qquad\quad~~ \Exists \val_2. \toval(\expr_2) = \val_2
     \end{inbox}
 }}
 \end{mathpar}
@@ -26,7 +26,7 @@ It does not matter whether they fork off an arbitrary expression.
 
 \begin{defn}
   An expression $\expr$ and state $\state$ are \emph{reducible} (written $\red(\expr, \state)$) if
-  \[ \Exists \expr_2, \state_2, \expr'. \expr,\state \step \expr_2,\state_2,\expr' \]
+  \[ \Exists \expr_2, \state_2, \expr_f. \expr,\state \step \expr_2,\state_2,\expr_f \]
 \end{defn}
 
 \begin{defn}[Context]
@@ -35,9 +35,9 @@ It does not matter whether they fork off an arbitrary expression.
   \item $\lctx$ does not turn non-values into values:\\
     $\All\expr. \toval(\expr) = \bot \Ra \toval(\lctx(\expr)) = \bot $
   \item One can perform reductions below $\lctx$:\\
-    $\All \expr_1, \state_1, \expr_2, \state_2, \expr'. \expr_1, \state_1 \step \expr_2,\state_2,\expr' \Ra \lctx(\expr_1), \state_1 \step \lctx(\expr_2),\state_2,\expr' $
+    $\All \expr_1, \state_1, \expr_2, \state_2, \expr_f. \expr_1, \state_1 \step \expr_2,\state_2,\expr_f \Ra \lctx(\expr_1), \state_1 \step \lctx(\expr_2),\state_2,\expr_f $
   \item Reductions stay below $\lctx$ until there is a value in the hole:\\
-    $\All \expr_1', \state_1, \expr_2, \state_2, \expr'. \toval(\expr_1') = \bot \land \lctx(\expr_1'), \state_1 \step \expr_2,\state_2,\expr' \Ra \Exists\expr_2'. \expr_2 = \lctx(\expr_2') \land \expr_1', \state_1 \step \expr_2',\state_2,\expr' $
+    $\All \expr_1', \state_1, \expr_2, \state_2, \expr_f. \toval(\expr_1') = \bot \land \lctx(\expr_1'), \state_1 \step \expr_2,\state_2,\expr_f \Ra \Exists\expr_2'. \expr_2 = \lctx(\expr_2') \land \expr_1', \state_1 \step \expr_2',\state_2,\expr_f $
   \end{enumerate}
 \end{defn}
 
@@ -54,9 +54,9 @@ For any language $\Lang$, we define the corresponding thread-pool semantics.
   \cfg{\tpool'}{\state'}}
 \begin{mathpar}
 \infer
-  {\expr_1, \state_1 \step \expr_2, \state_2, \expr' \and \expr' \neq ()}
+  {\expr_1, \state_1 \step \expr_2, \state_2, \expr_f \and \expr_f \neq \bot}
   {\cfg{\tpool \dplus [\expr_1] \dplus \tpool'}{\state} \step
-     \cfg{\tpool \dplus [\expr_2] \dplus \tpool' \dplus [\expr']}{\state'}}
+     \cfg{\tpool \dplus [\expr_2] \dplus \tpool' \dplus [\expr_f]}{\state'}}
 \and\infer
   {\expr_1, \state_1 \step \expr_2, \state_2}
   {\cfg{\tpool \dplus [\expr_1] \dplus \tpool'}{\state} \step
@@ -170,8 +170,6 @@ We introduce additional metavariables ranging over terms and generally let the c
 \]
 
 \paragraph{Variable conventions.}
-We often abuse notation, using the preceding \emph{term} meta-variables to range over (bound) \emph{variables}.
-We omit type annotations in binders, when the type is clear from context.
 We assume that, if a term occurs multiple times in a rule, its free variables are exactly those binders which are available at every occurrence.
 
 
@@ -596,17 +594,19 @@ This is entirely standard.
   {\mask_2 \subseteq \mask_1 \and
    \toval(\expr_1) = \bot \and
    \red(\expr_1, \state_1) \and
-   \All \expr_2, \state_2, \expr'. \expr_1,\state_1 \step \expr_2,\state_2,\expr' \Ra \pred(\expr_2,\state_2,\expr')}
-  {\pvs[\mask_1][\mask_2] \later\ownPhys{\state_1} * \later\All \expr_2, \state_2, \expr'. \pred(\expr_2, \state_2, \expr') \land \ownPhys{\state_2} \wand \pvs[\mask_2][\mask_1] \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \wpre{\expr'}[\top]{\Ret\var.\TRUE} {}\\\proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}}
+   \All \expr_2, \state_2, \expr_f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_f \Ra \pred(\expr_2,\state_2,\expr_f)}
+  { {\begin{inbox} % for some crazy reason, LaTeX is actually sensitive to the space between the "{ {" here and the "} }" below...
+        ~~\pvs[\mask_1][\mask_2] \later\ownPhys{\state_1} * \later\All \expr_2, \state_2, \expr_f. \pred(\expr_2, \state_2, \expr_f) \land {}\\\qquad\qquad\qquad\qquad\qquad \ownPhys{\state_2} \wand \pvs[\mask_2][\mask_1] \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \wpre{\expr_f}[\top]{\Ret\any.\TRUE} {}\\\proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}
+      \end{inbox}} }
 
   \infer[wp-lift-pure-step]
   {\toval(\expr_1) = \bot \and
    \All \state_1. \red(\expr_1, \state_1) \and
-   \All \state_1, \expr_2, \state_2, \expr'. \expr_1,\state_1 \step \expr_2,\state_2,\expr' \Ra \state_1 = \state_2 \land \pred(\expr_2,\expr')}
-  {\later\All \expr_2, \expr'. \pred(\expr_2, \expr')  \wand \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \wpre{\expr'}[\top]{\Ret\var.\TRUE} \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}}
+   \All \state_1, \expr_2, \state_2, \expr_f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_f \Ra \state_1 = \state_2 \land \pred(\expr_2,\expr_f)}
+  {\later\All \expr_2, \expr_f. \pred(\expr_2, \expr_f)  \Ra \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \wpre{\expr_f}[\top]{\Ret\any.\TRUE} \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}}
 \end{mathpar}
 
-Here we define $\wpre{\expr'}[\mask]{\Ret\var.\prop} \eqdef \TRUE$ if $\expr' = \bot$ (remember that our stepping relation can, but does not have to, define a forked-off expression).
+Here we define $\wpre{\expr_f}[\mask]{\Ret\var.\prop} \eqdef \TRUE$ if $\expr_f = \bot$ (remember that our stepping relation can, but does not have to, define a forked-off expression).
 
 \subsection{Adequacy}
 

program_logic/hoare_lifting.v

@@ -23,19 +23,19 @@ Lemma ht_lift_step E1 E2
   E2 ⊆ E1 → to_val e1 = None →
   reducible e1 σ1 →
   (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
-  ((P ={E1,E2}=> ▷ ownP σ1 ★ ▷ P') ∧ ∀ e2 σ2 ef,
-    (■ φ e2 σ2 ef ★ ownP σ2 ★ P' ={E2,E1}=> Φ1 e2 σ2 ef ★ Φ2 e2 σ2 ef) ∧
-    {{ Φ1 e2 σ2 ef }} e2 @ E1 {{ Ψ }} ∧
-    {{ Φ2 e2 σ2 ef }} ef ?@ ⊤ {{ λ _, True }})
+  ((P ={E1,E2}=> ▷ ownP σ1 ★ ▷ P') ∧
+   (∀ e2 σ2 ef, ■ φ e2 σ2 ef ★ ownP σ2 ★ P' ={E2,E1}=> Φ1 e2 σ2 ef ★ Φ2 e2 σ2 ef) ∧
+   (∀ e2 σ2 ef, {{ Φ1 e2 σ2 ef }} e2 @ E1 {{ Ψ }}) ∧
+   (∀ e2 σ2 ef, {{ Φ2 e2 σ2 ef }} ef ?@ ⊤ {{ λ _, True }}))
   ⊢ {{ P }} e1 @ E1 {{ Ψ }}.
 Proof.
   intros ?? Hsafe Hstep; apply: always_intro. apply impl_intro_l.
   rewrite (assoc _ P) {1}/vs always_elim impl_elim_r pvs_always_r.
   rewrite -(wp_lift_step E1 E2 φ _ e1 σ1) //; apply pvs_mono.
   rewrite always_and_sep_r -assoc; apply sep_mono_r.
-  rewrite (later_intro (∀ _, _)) -later_sep; apply later_mono.
+  rewrite [(_ ∧ _)%I]later_intro -later_sep; apply later_mono.
   apply forall_intro=>e2; apply forall_intro=>σ2; apply forall_intro=>ef.
-  rewrite (forall_elim e2) (forall_elim σ2) (forall_elim ef).
+  do 3 rewrite (forall_elim e2) (forall_elim σ2) (forall_elim ef).
   apply wand_intro_l; rewrite !always_and_sep_l.
   (* Apply the view shift. *)
   rewrite (assoc _ _ P') -(assoc _ _ _ P') assoc.
@@ -62,13 +62,14 @@ Proof.
     (λ e2 σ2 ef, ■ φ e2 σ2 ef ★ P)%I);
     try by (rewrite /φ'; eauto using atomic_not_val, atomic_step).
   apply and_intro; [by rewrite -vs_reflexive; apply const_intro|].
-  apply forall_mono=>e2; apply forall_mono=>σ2; apply forall_mono=>ef.
   apply and_intro; [|apply and_intro; [|done]].
-  - rewrite -vs_impl; apply: always_intro. apply impl_intro_l.
+  - apply forall_mono=>e2; apply forall_mono=>σ2; apply forall_mono=>ef.
+    rewrite -vs_impl; apply: always_intro. apply impl_intro_l.
     rewrite and_elim_l !assoc; apply sep_mono; last done.
     rewrite -!always_and_sep_l -!always_and_sep_r; apply const_elim_l=>-[??].
     by repeat apply and_intro; try apply const_intro.
-  - apply (always_intro _ _), impl_intro_l; rewrite and_elim_l.
+  - apply forall_mono=>e2; apply forall_mono=>σ2; apply forall_mono=>ef.
+    apply (always_intro _ _), impl_intro_l; rewrite and_elim_l.
     rewrite -always_and_sep_r; apply const_elim_r=>-[[v Hv] ?].
     rewrite -(of_to_val e2 v) // -wp_value'; [].
     rewrite -(exist_intro σ2) -(exist_intro ef) (of_to_val e2) //.
@@ -79,16 +80,15 @@ Lemma ht_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) P P' Ψ e
   to_val e1 = None →
   (∀ σ1, reducible e1 σ1) →
   (∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2 ∧ φ e2 ef) →
-  (∀ e2 ef,
-    {{ ■ φ e2 ef ★ P }} e2 @ E {{ Ψ }} ∧
-    {{ ■ φ e2 ef ★ P' }} ef ?@ ⊤ {{ λ _, True }})
+  ((∀ e2 ef, {{ ■ φ e2 ef ★ P }} e2 @ E {{ Ψ }}) ∧
+   (∀ e2 ef, {{ ■ φ e2 ef ★ P' }} ef ?@ ⊤ {{ λ _, True }}))
   ⊢ {{ ▷(P ★ P') }} e1 @ E {{ Ψ }}.
 Proof.
   intros ? Hsafe Hstep; apply: always_intro. apply impl_intro_l.
   rewrite -(wp_lift_pure_step E φ _ e1) //.
-  rewrite (later_intro (∀ _, _)) -later_and; apply later_mono.
+  rewrite [(_ ∧ ∀ _, _)%I]later_intro -later_and; apply later_mono.
   apply forall_intro=>e2; apply forall_intro=>ef; apply impl_intro_l.
-  rewrite (forall_elim e2) (forall_elim ef).
+  do 2 rewrite (forall_elim e2) (forall_elim ef).
   rewrite always_and_sep_l !always_and_sep_r {1}(always_sep_dup (■ _)).
   sep_split left: [■ φ _ _; P; {{ ■ φ _ _ ★ P }} e2 @ E {{ Ψ }}]%I.
   - rewrite assoc {1}/ht -always_wand_impl always_elim wand_elim_r //.
@@ -106,11 +106,13 @@ Lemma ht_lift_pure_det_step
 Proof.
   intros ? Hsafe Hdet.
   rewrite -(ht_lift_pure_step _ (λ e2' ef', e2 = e2' ∧ ef = ef')); eauto.
-  apply forall_intro=>e2'; apply forall_intro=>ef'; apply and_mono.
-  - apply: always_intro. apply impl_intro_l.
+  apply and_mono.
+  - apply forall_intro=>e2'; apply forall_intro=>ef'.
+    apply: always_intro. apply impl_intro_l.
     rewrite -always_and_sep_l -assoc; apply const_elim_l=>-[??]; subst.
     by rewrite /ht always_elim impl_elim_r.
-  - destruct ef' as [e'|]; simpl; [|by apply const_intro].
+  - apply forall_intro=>e2'; apply forall_intro=>ef'.
+    destruct ef' as [e'|]; simpl; [|by apply const_intro].
     apply: always_intro. apply impl_intro_l.
     rewrite -always_and_sep_l -assoc; apply const_elim_l=>-[??]; subst.
     by rewrite /= /ht always_elim impl_elim_r.