diff --git a/docs/base-logic.tex b/docs/base-logic.tex index a0817ead9e0ec2faba0495828f0ddc5d37d1a343..d03cfa14f8ffd2041af14043ee1d7bcd5560fbe3 100644 --- a/docs/base-logic.tex +++ b/docs/base-logic.tex @@ -26,7 +26,7 @@ Elements of $\SigAx$ are ranged over by $\sigax$. \subsection{Grammar}\label{sec:grammar} \paragraph{Syntax.} -Iris syntax is built up from a signature $\Sig$ and a countably infinite set $\textdom{Var}$ of variables (ranged over by metavariables $x$, $y$, $z$). +Iris syntax is built up from a signature $\Sig$ and a countably infinite set $\Var$ of variables (ranged over by metavariables $\var$, $\varB$, $\varC$). Below, $\melt$ ranges over $\monoid$ and $i$ ranges over $\set{1,2}$. \begin{align*} diff --git a/docs/derived.tex b/docs/derived.tex index 2a74a30f176c90d5e9b3ad6e9d7316c22931f268..2802c54173432c05c8e9e58424a1fee08b5938eb 100644 --- a/docs/derived.tex +++ b/docs/derived.tex @@ -141,7 +141,7 @@ % We write $x \fgmapsto v$ for $\exists q.\; x \fgmapsto[q] v$ and $x \gmapsto v$ for $x \fgmapsto[1] v$. % Note that $x \fgmapsto v$ is duplicable but cannot be boxed (as it depends on resources); \ie we have $x \fgmapsto v \Lra x \fgmapsto v * x \fgmapsto v$ but not $x \fgmapsto v \Ra \always x \fgmapsto v$. -% To implement this interface, allocate an instance $\gname_G$ of $\FHeap(\textdom{Val})$ and define +% To implement this interface, allocate an instance $\gname_G$ of $\FHeap(\Val)$ and define % $% x \fgmapsto[q] v \eqdef % \begin{cases} diff --git a/docs/iris.sty b/docs/iris.sty index 4100a659228bee91365e5a93dbae85c52a94e970..0b4428cdf7ca443f63d42fa042c7bb0c96a1cc47 100644 --- a/docs/iris.sty +++ b/docs/iris.sty @@ -136,6 +136,8 @@ \newcommand{\Val}{\textdom{Val}} \newcommand{\Loc}{\textdom{Loc}} \newcommand{\Expr}{\textdom{Expr}} +\newcommand{\Var}{\textdom{Var}} +\newcommand{\ThreadPool}{\textdom{ThreadPool}} \newcommand{\cofe}{T} \newcommand{\cofeB}{U} diff --git a/docs/language.tex b/docs/language.tex index 709a0c6caf0657a85965fb33de4017169e7a926c..65ae793f43ef9fdf4f31dceb753a4cae460e7ce9 100644 --- a/docs/language.tex +++ b/docs/language.tex @@ -3,12 +3,14 @@ \section{Language} \label{sec:language} -A \emph{language} \Lang consists of a set \textdom{Expr} of \emph{expressions} (metavariable \expr), a set \textdom{Val} of \emph{values} (metavariable \val), and a set \textdom{State} of \emph{states} (metvariable \state) such that +A \emph{language} \Lang consists of a set \Expr{} of \emph{expressions} (metavariable \expr), a set \Val{} of \emph{values} (metavariable \val), and a set \State of \emph{states} (metavariable \state) such that \begin{itemize} -\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} +\item There exist functions \ofval : \Val \to \Expr and \toval : \Expr \pfn \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 (\cup_n \textdom{Expr}^n)$ +\item There exists a \emph{primitive reduction relation} $(-,- \step -,-,-) \subseteq \Expr \times \State \times \Expr \times \State \times (\cup_n \Expr^n)$ A reduction $\expr_1, \state_1 \step \expr_2, \state_2, \overline\expr$ indicates that, when $\expr_1$ reduces to $\expr_2$, the new threads in the list $\overline\expr$ is forked off. We will write $\expr_1, \state_1 \step \expr_2, \state_2$ for $\expr_1, \state_1 \step \expr_2, \state_2, ()$, \ie when no threads are forked off. \\ \item All values are stuck: @@ -26,7 +28,7 @@ A \emph{language} $\Lang$ consists of a set \textdom{Expr} of \emph{expressions} \end{defn} \begin{defn}[Context] - A function $\lctx : \textdom{Expr} \to \textdom{Expr}$ is a \emph{context} if the following conditions are satisfied: + A function $\lctx : \Expr \to \Expr$ is a \emph{context} if the following conditions are satisfied: \begin{enumerate}[itemsep=0pt] \item $\lctx$ does not turn non-values into values:\\ $\All\expr. \toval(\expr) = \bot \Ra \toval(\lctx(\expr)) = \bot$ @@ -43,7 +45,7 @@ For any language $\Lang$, we define the corresponding thread-pool semantics. \paragraph{Machine syntax} $- \tpool \in \textdom{ThreadPool} \eqdef \bigcup_n \textdom{Expr}^n + \tpool \in \ThreadPool \eqdef \bigcup_n \Expr^n$ \judgment[Machine reduction]{\cfg{\tpool}{\state} \step diff --git a/docs/program-logic.tex b/docs/program-logic.tex index 11c2a01d9694bb4bb53c73fa8e5e645a72c14c06..5577652af67bdd45807d65dfaacd7a25fb9ce2c1 100644 --- a/docs/program-logic.tex +++ b/docs/program-logic.tex @@ -14,7 +14,7 @@ To this end, we use tokens that manage which invariants are currently enabled. We assume to have the following four CMRAs available: \begin{align*} - \textmon{State} \eqdef{}& \authm(\exm(\textdom{State})) \\ + \textmon{State} \eqdef{}& \authm(\exm(\State)) \\ \textmon{Inv} \eqdef{}& \authm(\mathbb N \fpfn \agm(\latert \iPreProp)) \\ \textmon{En} \eqdef{}& \pset{\mathbb N} \\ \textmon{Dis} \eqdef{}& \finpset{\mathbb N} @@ -249,10 +249,10 @@ The purpose of the adequacy statement is to show that our notion of weakest prec There are two properties we are looking for: First of all, the postcondition should reflect actual properties of the values the program can terminate with. Second, a proof of a weakest precondition with any postcondition should imply that the program is \emph{safe}, \ie that it does not get stuck. -To express the adequacy statement for functional correctness, we assume we are given some set $V \in \textdom{Val}$ of legal return values. +To express the adequacy statement for functional correctness, we assume we are given some set $V \subseteq \Val$ of legal return values. Furthermore, we assume that the signature $\Sig$ adds a predicate $\pred$ to the logic which reflects $V$ into the logic: $\begin{array}{rMcMl} - \Sem\pred &:& \Sem{\textdom{Val}\,} \nfn \Sem\Prop \\ + \Sem\pred &:& \Sem{\Val\,} \nfn \Sem\Prop \\ \Sem\pred &\eqdef& \Lam \val. \Lam \any. \setComp{n}{v \in V} \end{array}$ The signature can of course state arbitrary additional properties of $\pred$, as long as they are proven sound.