docs: reflect physical state interpretation

CHANGELOG.md

@@ -11,29 +11,28 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 * View shifts are radically simplified to just internalize frame-preserving
   updates.  Weakestpre is defined inside the logic, and invariants and view
   shifts with masks are also coded up inside Iris.  Adequacy of weakestpre is
-  proven in the logic. [#] The old ownership of the entire physical state is
+  proven in the logic. The old ownership of the entire physical state is
   replaced by a user-selected predicate over physical state that is maintained
   by weakestpre.
 * Use OFEs instead of COFEs everywhere.  COFEs are only used for solving the
-  recursive domain equation.  As a consequence, CMRAs no longer need a proof
-  of completeness.
-  (The old `cofeT` is provided by `algebra.deprecated`.)
+  recursive domain equation.  As a consequence, CMRAs no longer need a proof of
+  completeness.  (The old `cofeT` is provided by `algebra.deprecated`.)
 * Implement a new agreement construction.  Unlike the old one, this one
   preserves discreteness.
-* Renaming and moving things around: uPred and the rest of the base logic are
-  in `base_logic`, while `program_logic` is for everything involving the
-  general Iris notion of a language.
+* Renaming and moving things around: uPred and the rest of the base logic are in
+  `base_logic`, while `program_logic` is for everything involving the general
+  Iris notion of a language.
 * Slightly weaker notion of atomicity: an expression is atomic if it reduces in
   one step to something that does not reduce further.
 * Changed notation for embedding Coq assertions into Iris.  The new notation is
   ⌜φ⌝.  Also removed `=` and `⊥` from the Iris scope.  (The old notations are
   provided in `base_logic.deprecated`.)
 * Up-closure of namespaces is now a notation (↑) instead of a coercion.
-* With invariants and the physical state being handled in the logic, there
-  is no longer any reason to demand the CMRA unit to be discrete.
+* With invariants and the physical state being handled in the logic, there is no
+  longer any reason to demand the CMRA unit to be discrete.
 * The language can now fork off multiple threads at once.
-* Local Updates (for the authoritative monoid) are now a 4-way relation
-  with syntax-directed lemmas proving them.
+* Local Updates (for the authoritative monoid) are now a 4-way relation with
+  syntax-directed lemmas proving them.
 
 ## Iris 2.0
 

docs/program-logic.tex

@@ -115,8 +115,7 @@ We assume to have the following four CMRAs available:
   \InvName \eqdef{}& \nat \\
   \textmon{Inv} \eqdef{}& \authm(\InvName \fpfn \agm(\latert \iPreProp)) \\
   \textmon{En} \eqdef{}& \pset{\InvName} \\
-  \textmon{Dis} \eqdef{}& \finpset{\InvName} \\
-  \textmon{State} \eqdef{}& \authm(\maybe{\exm(\State)})
+  \textmon{Dis} \eqdef{}& \finpset{\InvName}
 \end{align*}
 The last two are the tokens used for managing invariants, $\textmon{Inv}$ is the monoid used to manage the invariants themselves.
 Finally, $\textmon{State}$ is used to provide the program with a view of the physical state of the machine.
@@ -253,22 +252,20 @@ Finally, we can define the core piece of the program logic, the assertion that r
 
 \paragraph{Defining weakest precondition.}
 We assume that everything making up the definition of the language, \ie values, expressions, states, the conversion functions, reduction relation and all their properties, are suitably reflected into the logic (\ie they are part of the signature $\Sig$).
+We further assume (as a parameter) a predicate $S : \State \to \iProp$ that interprets the physical state as an Iris assertion.
+This can be instantiated, for example, with ownership of an authoritative RA to tie the physical state to fragments that are used for user-level proofs.
 
 \begin{align*}
   \textdom{wp} \eqdef{}& \MU \textdom{wp}. \Lam \mask, \expr, \pred. \\
         & (\Exists\val. \toval(\expr) = \val \land \pvs[\mask] \prop) \lor {}\\
-        & \Bigl(\toval(\expr) = \bot \land \All \state. \ownGhost{\gname_{\textmon{State}}}{\authfull \state} \vsW[\mask][\emptyset] {}\\
+        & \Bigl(\toval(\expr) = \bot \land \All \state. S(\state) \vsW[\mask][\emptyset] {}\\
         &\qquad \red(\expr, \state) * \later\All \expr', \state', \vec\expr. (\expr, \state \step \expr', \state', \vec\expr) \vsW[\emptyset][\mask] {}\\
-        &\qquad\qquad \ownGhost{\gname_{\textmon{State}}}{\authfull \state'} * \textdom{wp}(\mask, \expr', \pred) * \Sep_{\expr'' \in \vec\expr} \textdom{wp}(\top, \expr'', \Lam \any. \TRUE)\Bigr) \\
+        &\qquad\qquad S(\state') * \textdom{wp}(\mask, \expr', \pred) * \Sep_{\expr'' \in \vec\expr} \textdom{wp}(\top, \expr'', \Lam \any. \TRUE)\Bigr) \\
 %  (* value case *)
   \wpre\expr[\mask]{\Ret\val. \prop} \eqdef{}& \textdom{wp}(\mask, \expr, \Lam\val.\prop)
 \end{align*}
 If we leave away the mask, we assume it to default to $\top$.
 
-This ties the authoritative part of \textmon{State} to the actual physical state of the reduction witnessed by the weakest precondition.
-The fragment will then be available to the user of the logic, as their way of talking about the physical state:
-\[ \ownPhys\state \eqdef \ownGhost{\gname_{\textmon{State}}}{\authfrag \state} \]
-
 \paragraph{Laws of weakest precondition.}
 The following rules can all be derived:
 \begin{mathpar}
@@ -302,41 +299,39 @@ The following rules can all be derived:
 {\wpre\expr[\mask]{\Ret\var. \wpre{\lctx(\ofval(\var))}[\mask]{\Ret\varB.\prop}} \proves \wpre{\lctx(\expr)}[\mask]{\Ret\varB.\prop}}
 \end{mathpar}
 
-We will also want rules that connect weakest preconditions to the operational semantics of the language.
-In order to cover the most general case, those rules end up being more complicated:
+We will also want a rule that connect weakest preconditions to the operational semantics of the language.
 \begin{mathpar}
   \infer[wp-lift-step]
-  {}
+  {\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][\emptyset] \Exists \state_1. \red(\expr_1,\state_1) * \later\ownPhys{\state_1} * {}\\\qquad~~ \later\All \expr_2, \state_2, \vec\expr. \Bigl( (\expr_1, \state_1 \step \expr_2, \state_2, \vec\expr) * \ownPhys{\state_2} \Bigr) \wand \pvs[\emptyset][\mask] \Bigl(\wpre{\expr_2}[\mask]{\Ret\var.\prop} * \Sep_{\expr_\f \in \vec\expr} \wpre{\expr_\f}[\top]{\Ret\any.\TRUE}\Bigr)  {}\\\proves \wpre{\expr_1}[\mask]{\Ret\var.\prop}
+        ~~\All \state_1. S(\state_1) \vsW[\mask][\emptyset] \red(\expr_1,\state_1) * {}\\\qquad~~ \later\All \expr_2, \state_2, \vec\expr.  (\expr_1, \state_1 \step \expr_2, \state_2, \vec\expr)  \vsW[\emptyset][\mask] \Bigl(S(\state_2) * \wpre{\expr_2}[\mask]{\Ret\var.\prop} * \Sep_{\expr_\f \in \vec\expr} \wpre{\expr_\f}[\top]{\Ret\any.\TRUE}\Bigr)  {}\\\proves \wpre{\expr_1}[\mask]{\Ret\var.\prop}
       \end{inbox}} }
-\\\\
-  \infer[wp-lift-pure-step]
-  {\All \state_1. \red(\expr_1, \state_1) \and
-   \All \state_1, \expr_2, \state_2, \vec\expr. \expr_1,\state_1 \step \expr_2,\state_2,\vec\expr \Ra \state_1 = \state_2 }
-  {\later\All \state, \expr_2, \vec\expr. (\expr_1,\state \step \expr_2, \state,\vec\expr)  \Ra \wpre{\expr_2}[\mask]{\Ret\var.\prop} * \Sep_{\expr_\f \in \vec\expr} \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} \proves \wpre{\expr_1}[\mask]{\Ret\var.\prop}}
 \end{mathpar}
 
-We can further derive some slightly simpler rules for special cases:
-We can derive some specialized forms of the lifting axioms for the operational semantics.
-\begin{mathparpagebreakable}
-  \infer[wp-lift-atomic-step]
-  {\atomic(\expr_1) \and
-   \red(\expr_1, \state_1)}
-  { {\begin{inbox}~~\later\ownPhys{\state_1} * \later\All \val_2, \state_2, \vec\expr. (\expr_1,\state_1 \step \ofval(\val),\state_2,\vec\expr)  * \ownPhys{\state_2} \wand \prop[\val_2/\var] * \Sep_{\expr_\f \in \vec\expr} \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
-   \red(\expr_1, \state_1) \and
-   \All \expr'_2, \state'_2, \vec\expr'. \expr_1,\state_1 \step \expr'_2,\state'_2,\vec\expr' \Ra \state_2 = \state_2' \land \toval(\expr_2') = \val_2 \land \vec\expr = \vec\expr'}
-  {\later\ownPhys{\state_1} * \later \Bigl(\ownPhys{\state_2} \wand \prop[\val_2/\var] * \Sep_{\expr_\f \in \vec\expr} \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} \Bigr) \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}}
-
-  \infer[wp-lift-pure-det-step]
-  {\All \state_1. \red(\expr_1, \state_1) \\
-   \All \state_1, \expr_2', \state'_2, \vec\expr'. \expr_1,\state_1 \step \expr'_2,\state'_2,\vec\expr' \Ra \state_1 = \state'_2 \land \expr_2 = \expr_2' \land \vec\expr = \vec\expr'}
-  {\later \Bigl( \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \Sep_{\expr_\f \in \vec\expr} \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} \Bigr) \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}}
-\end{mathparpagebreakable}
+% We can further derive some slightly simpler rules for special cases.
+% \begin{mathparpagebreakable}
+%   \infer[wp-lift-pure-step]
+%   {\All \state_1. \red(\expr_1, \state_1) \and
+%    \All \state_1, \expr_2, \state_2, \vec\expr. \expr_1,\state_1 \step \expr_2,\state_2,\vec\expr \Ra \state_1 = \state_2 }
+%   {\later\All \state, \expr_2, \vec\expr. (\expr_1,\state \step \expr_2, \state,\vec\expr)  \Ra \wpre{\expr_2}[\mask]{\Ret\var.\prop} * \Sep_{\expr_\f \in \vec\expr} \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} \proves \wpre{\expr_1}[\mask]{\Ret\var.\prop}}
+
+%   \infer[wp-lift-atomic-step]
+%   {\atomic(\expr_1) \and
+%    \red(\expr_1, \state_1)}
+%   { {\begin{inbox}~~\later\ownPhys{\state_1} * \later\All \val_2, \state_2, \vec\expr. (\expr_1,\state_1 \step \ofval(\val),\state_2,\vec\expr)  * \ownPhys{\state_2} \wand \prop[\val_2/\var] * \Sep_{\expr_\f \in \vec\expr} \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
+%    \red(\expr_1, \state_1) \and
+%    \All \expr'_2, \state'_2, \vec\expr'. \expr_1,\state_1 \step \expr'_2,\state'_2,\vec\expr' \Ra \state_2 = \state_2' \land \toval(\expr_2') = \val_2 \land \vec\expr = \vec\expr'}
+%   {\later\ownPhys{\state_1} * \later \Bigl(\ownPhys{\state_2} \wand \prop[\val_2/\var] * \Sep_{\expr_\f \in \vec\expr} \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} \Bigr) \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}}
+
+%   \infer[wp-lift-pure-det-step]
+%   {\All \state_1. \red(\expr_1, \state_1) \\
+%    \All \state_1, \expr_2', \state'_2, \vec\expr'. \expr_1,\state_1 \step \expr'_2,\state'_2,\vec\expr' \Ra \state_1 = \state'_2 \land \expr_2 = \expr_2' \land \vec\expr = \vec\expr'}
+%   {\later \Bigl( \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \Sep_{\expr_\f \in \vec\expr} \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} \Bigr) \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}}
+% \end{mathparpagebreakable}
 
 
 \paragraph{Adequacy of weakest precondition.}