docs: lifting axioms

docs/derived.tex

@@ -87,7 +87,7 @@ The convention for omitted masks is similar to the base logic:
 An omitted $\mask$ is $\top$ for Hoare triples and $\emptyset$ for view shifts.
 
 
-\paragraph{View shifts.}~
+\paragraph{View shifts.}
 The following rules can be derived for view shifts.
 
 \begin{mathparpagebreakable}
@@ -199,6 +199,11 @@ The following rules can be derived for Hoare triples.
   {\hoare{\FALSE}{\expr}{\Ret \val. \prop}[\mask]}
 \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.
+
+\ralf{Add these.}
+
 \subsection{Global Functor and ghost ownership}
 \ralf{Describe this.}
 

docs/iris.sty

@@ -300,6 +300,7 @@
 \newcommand{\toval}{\mathit{val}}
 \newcommand{\ofval}{\mathit{expr}}
 \newcommand{\atomic}{\mathit{atomic}}
+\newcommand{\red}{\mathit{red}}
 \newcommand{\Lang}{\Lambda}
 
 \newcommand{\tpool}{T}

docs/logic.tex

@@ -5,8 +5,8 @@ A \emph{language} $\Lang$ consists of a set \textdom{Expr} of \emph{expressions}
 \item There exist functions $\ofval : \textdom{Val} \to \textdom{Expr}$ and $\toval : \textdom{Expr} \pfn \textdom{val}$ (notice the latter is partial), such that
 \begin{mathpar} {\All \expr, \val. \toval(\expr) = \val \Ra \ofval(\val) = \expr} \and {\All\val. \toval(\ofval(\val)) = \val} 
 \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{()})\]
-  We will write $\expr_1, \state_1 \step \expr_2, \state_2$ for $\expr_1, \state_1 \step \expr_2, \state_2, ()$. \\
+\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.
 \item All values are stuck:
 \[ \expr, \_ \step  \_, \_, \_ \Ra \toval(\expr) = \bot \]
@@ -24,6 +24,11 @@ In other words, atomic expression \emph{reduce in one step to a value}.
 It does not matter whether they fork off an arbitrary expression.
 \end{itemize}
 
+\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' \]
+\end{defn}
+
 \begin{defn}[Context]
   A function $\lctx : \textdom{Expr} \to \textdom{Expr}$ is a \emph{context} if the following conditions are satisfied:
   \begin{enumerate}[itemsep=0pt]
@@ -579,7 +584,23 @@ This is entirely standard.
 \end{mathpar}
 
 \subsection{Lifting of operational semantics}\label{sec:lifting}
-~\\\ralf{Add this.}
+
+\begin{mathparpagebreakable}
+  \infer[wp-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'. \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}{\Ret\var.\prop}[\mask_1] * \wpre{\expr'}{\Ret\var.\TRUE}[\top] {}\\\proves \wpre{\expr_1}{\Ret\var.\prop}[\mask_1]}
+
+  \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}{\Ret\var.\prop}[\mask_1] * \wpre{\expr'}{\Ret\var.\TRUE}[\top] \proves \wpre{\expr_1}{\Ret\var.\prop}[\mask_1]}
+\end{mathparpagebreakable}
+
+Here we define $\wpre{\expr'}{\Ret\var.\prop}[\mask] \eqdef \TRUE$ if $\expr' = \bot$ (remember that our stepping relation can, but does not have to, define a forked-off expression).
 
 % The following lemmas help in proving axioms for a particular language.
 % The first applies to expressions with side-effects, and the second to side-effect-free expressions.

program_logic/hoare_lifting.v

@@ -20,14 +20,14 @@ Implicit Types Ψ : val Λ → iProp Λ Σ.
 
 Lemma ht_lift_step E1 E2
     (φ : expr Λ → state Λ → option (expr Λ) → Prop) P P' Φ1 Φ2 Ψ e1 σ1 :
-  E1 ⊆ E2 → to_val e1 = None →
+  E2 ⊆ E1 → to_val e1 = None →
   reducible e1 σ1 →
   (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
-  ((P ={E2,E1}=> ▷ ownP σ1 ★ ▷ P') ∧ ∀ e2 σ2 ef,
-    (■ φ e2 σ2 ef ★ ownP σ2 ★ P' ={E1,E2}=> Φ1 e2 σ2 ef ★ Φ2 e2 σ2 ef) ∧
-    {{ Φ1 e2 σ2 ef }} e2 @ E2 {{ Ψ }} ∧
+  ((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 {{ Ψ }}.
+  ⊑ {{ 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.
@@ -42,7 +42,7 @@ Proof.
   rewrite {1}/vs -always_wand_impl always_elim wand_elim_r.
   rewrite pvs_frame_r; apply pvs_mono.
   (* Now we're almost done. *)
-  sep_split left: [Φ1 _ _ _; {{ Φ1 _ _ _ }} e2 @ E2 {{ Ψ }}]%I.
+  sep_split left: [Φ1 _ _ _; {{ Φ1 _ _ _ }} e2 @ E1 {{ Ψ }}]%I.
   - rewrite {1}/ht -always_wand_impl always_elim wand_elim_r //.
   - destruct ef as [e'|]; simpl; [|by apply const_intro].
     rewrite {1}/ht -always_wand_impl always_elim wand_elim_r //.

program_logic/lifting.v

@@ -19,18 +19,18 @@ Notation wp_fork ef := (default True ef (flip (wp ⊤) (λ _, ■ True)))%I.
 
 Lemma wp_lift_step E1 E2
     (φ : expr Λ → state Λ → option (expr Λ) → Prop) Φ e1 σ1 :
-  E1 ⊆ E2 → to_val e1 = None →
+  E2 ⊆ E1 → to_val e1 = None →
   reducible e1 σ1 →
   (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
-  (|={E2,E1}=> ▷ ownP σ1 ★ ▷ ∀ e2 σ2 ef,
-    (■ φ e2 σ2 ef ∧ ownP σ2) -★ |={E1,E2}=> #> e2 @ E2 {{ Φ }} ★ wp_fork ef)
-  ⊑ #> e1 @ E2 {{ Φ }}.
+  (|={E1,E2}=> ▷ ownP σ1 ★ ▷ ∀ e2 σ2 ef,
+    (■ φ e2 σ2 ef ∧ ownP σ2) -★ |={E2,E1}=> #> e2 @ E1 {{ Φ }} ★ wp_fork ef)
+  ⊑ #> e1 @ E1 {{ Φ }}.
 Proof.
   intros ? He Hsafe Hstep. rewrite pvs_eq wp_eq.
   uPred.unseal; split=> n r ? Hvs; constructor; auto.
   intros rf k Ef σ1' ???; destruct (Hvs rf (S k) Ef σ1')
     as (r'&(r1&r2&?&?&Hwp)&Hws); auto; clear Hvs; cofe_subst r'.
-  destruct (wsat_update_pst k (E1 ∪ Ef) σ1 σ1' r1 (r2 ⋅ rf)) as [-> Hws'].
+  destruct (wsat_update_pst k (E2 ∪ Ef) σ1 σ1' r1 (r2 ⋅ rf)) as [-> Hws'].
   { apply equiv_dist. rewrite -(ownP_spec k); auto. }
   { by rewrite assoc. }
   constructor; [done|intros e2 σ2 ef ?; specialize (Hws' σ2)].