From 93f602ed4c8849223b2388453348cf76de332435 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 27 Jul 2016 18:05:00 +0200
Subject: [PATCH] docs: update lifting lemmas
---
CHANGELOG.md | 2 +-
docs/derived.tex | 44 +++-----------------------------------------
docs/logic.tex | 10 ++++------
3 files changed, 8 insertions(+), 48 deletions(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 13fa9bd61..cfd5f40d6 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -14,7 +14,7 @@ This version accompanies the final ICFP paper.
about values and closed expressions.
* [program_logic/language] The language does not define its own "atomic"
predicate. Instead, atomicity is defined as reducing in one step to a value.
-* [# program_logic/lifting] Lifting lemmas no longer round-trip through a
+* [program_logic/lifting] Lifting lemmas no longer round-trip through a
user-chosen predicate to define the configurations we can reduce to; they
directly relate to the operational semantics. This is equivalent and
much simpler to read.
diff --git a/docs/derived.tex b/docs/derived.tex
index 89d0f082e..34471d080 100644
--- a/docs/derived.tex
+++ b/docs/derived.tex
@@ -221,9 +221,9 @@ We can derive some specialized forms of the lifting axioms for the operational s
\begin{mathparpagebreakable}
\infer[wp-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)}
- {\later\ownPhys{\state_1} * \later\All \val_2, \state_2, \expr_\f. \pred(\ofval(\val), \state_2, \expr_\f) \land \ownPhys{\state_2} \wand \prop[\val_2/\var] * \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}}
+ \red(\expr_1, \state_1)}
+ { {\begin{inbox}~~\later\ownPhys{\state_1} * \later\All \val_2, \state_2, \expr_\f. (\expr_1,\state_1 \step \ofval(\val),\state_2,\expr_\f) \land \ownPhys{\state_2} \wand \prop[\val_2/\var] * \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} {}\\ \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}
+ \end{inbox}} }
\infer[wp-lift-atomic-det-step]
{\atomic(\expr_1) \and
@@ -238,44 +238,6 @@ We can derive some specialized forms of the lifting axioms for the operational s
{\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}
-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}
Hereinafter we assume the global CMRA functor (served up as a parameter to Iris) is obtained from a family of functors $(\iFunc_i)_{i \in I}$ for some finite $I$ by picking
diff --git a/docs/logic.tex b/docs/logic.tex
index d36424c5c..95b5adf17 100644
--- a/docs/logic.tex
+++ b/docs/logic.tex
@@ -593,18 +593,16 @@ A type $\type$ being \emph{inhabited} means that $ \proves \wtt{\term}{\type}$ i
\begin{mathpar}
\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_\f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_\f \Ra \pred(\expr_2,\state_2,\expr_\f)}
+ \toval(\expr_1) = \bot}
{ {\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}
+ ~~\pvs[\mask_1][\mask_2] \Exists \state_1. \red(\expr_1,\state_1) \land \later\ownPhys{\state_1} * \later\All \expr_2, \state_2, \expr_\f. (\expr_1, \state_1 \step \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_\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}}
+ \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 }
+ {\later\All \state, \expr_2, \expr_\f. (\expr_1,\state \step \expr_2, \state,\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_\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).
--
GitLab