diff --git a/docs/iris/derived.tex b/docs/iris/derived.tex index 10b2cffd51d9dc9647798aed21a46f6f8ec5b358..857f881c7a34a7113552d421b0ab6b87b6d1dcea 100644 --- a/docs/iris/derived.tex +++ b/docs/iris/derived.tex @@ -93,27 +93,27 @@ Using these view shifts, we can prove STS variants of the invariant rules \ruler This holds by our premise. \end{proof} -\begin{proof}[Proof of \ruleref{VSSts}] -This is similar to above, so we only give the proof in short notation: - -\hproof{% - Context: $\knowInv\iname{\STSInv(\STSS, \pred, \gname)}$ \\ - \pline[\mask_1 \uplus \{\iname\}]{ - \ownGhost\gname{(s_0, T)} * P - } \\ - \pline[\mask_1]{% - \Exists s. \later\pred(s) * \ownGhost\gname{(s, S, T)} * P - } \qquad by \ruleref{StsOpen} \\ - Context: $s \in S \eqdef \upclose(\{s_0\}, T)$ \\ - \pline[\mask_2]{% - \Exists s', T'. \later\pred(s') * Q(s', T') * \ownGhost\gname{(s, S, T)} - } \qquad by premiss \\ - Context: $(s, T) \ststrans (s', T')$ \\ - \pline[\mask_2 \uplus \{\iname\}]{ - \ownGhost\gname{(s', T')} * Q(s', T') - } \qquad by \ruleref{StsClose} -} -\end{proof} +% \begin{proof}[Proof of \ruleref{VSSts}] +% This is similar to above, so we only give the proof in short notation: + +% \hproof{% +% Context: $\knowInv\iname{\STSInv(\STSS, \pred, \gname)}$ \\ +% \pline[\mask_1 \uplus \{\iname\}]{ +% \ownGhost\gname{(s_0, T)} * P +% } \\ +% \pline[\mask_1]{% +% \Exists s. \later\pred(s) * \ownGhost\gname{(s, S, T)} * P +% } \qquad by \ruleref{StsOpen} \\ +% Context: $s \in S \eqdef \upclose(\{s_0\}, T)$ \\ +% \pline[\mask_2]{% +% \Exists s', T'. \later\pred(s') * Q(s', T') * \ownGhost\gname{(s, S, T)} +% } \qquad by premiss \\ +% Context: $(s, T) \ststrans (s', T')$ \\ +% \pline[\mask_2 \uplus \{\iname\}]{ +% \ownGhost\gname{(s', T')} * Q(s', T') +% } \qquad by \ruleref{StsClose} +% } +% \end{proof} \subsection{Authoritative monoids with interpretation}\label{sec:authinterp} @@ -185,3 +185,8 @@ The view shifts in the specification follow immediately from \ruleref{GhostUpd} The first implication is immediate from the definition. The second implication follows by case distinction on $q_1 + q_2 \in (0, 1]$. + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "iris" +%%% End: diff --git a/docs/iris/logic.tex b/docs/iris/logic.tex index b4cfb69b564421aeccfe501829f01ed04896af24..2283fc838793d6425847411b6ea3c72cb75a7356 100644 --- a/docs/iris/logic.tex +++ b/docs/iris/logic.tex @@ -106,7 +106,7 @@ Let $\mcarp{M} \eqdef |\monoid| \setminus \{\mzero\}$. \paragraph{Signatures.} We use a signature to account syntactically for the logic's parameters. -A \emph{signature} $\SigNat = (\SigType, \SigFn)$ comprises a set +A \emph{signature} $\Sig = (\SigType, \SigFn)$ comprises a set $\SigType \supseteq \{ \textsort{Val}, \textsort{Exp}, \textsort{Ectx}, \textsort{State}, \textsort{Monoid}, \textsort{InvName}, \textsort{InvMask}, \Prop \}$ @@ -120,7 +120,7 @@ to express that $\sigfn$ is a function symbol with the indicated arity. \dave{Say something not-too-shabby about adequacy: We don't spell out what it means.} \paragraph{Syntax.} -Iris syntax is built up from a signature $\SigNat$ and a countably infinite set $\textdom{Var}$ of variables (ranged over by metavariables $x$, $y$, $z$, and $\pvar$): +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$): \newcommand{\unitterm}{()}% \newcommand{\unitsort}{1}% \unit is bold. \begin{align*} @@ -145,9 +145,9 @@ Iris syntax is built up from a signature $\SigNat$ and a countably infinite set \prop * \prop \mid \prop \wand \prop \mid \\& - \MU \pvar. \pred \mid - \Exists x:\sort. \prop \mid - \All x:\sort. \prop \mid + \MU \var. \pred \mid + \Exists \var:\sort. \prop \mid + \All \var:\sort. \prop \mid \\& \knowInv{\term}{\prop} \mid \ownGGhost{\term} \mid @@ -164,7 +164,7 @@ Iris syntax is built up from a signature $\SigNat$ and a countably infinite set \sort \times \sort \mid \sort \to \sort \end{align*} -Recursive predicates must be \emph{guarded}: in $\MU \pvar. \pred$, the variable $\pvar$ can only appear under the later $\later$ modality. +Recursive predicates must be \emph{guarded}: in $\MU \var. \pred$, the variable $\var$ can only appear under the later $\later$ modality. \paragraph{Metavariable conventions.} We introduce additional metavariables ranging over terms and generally let the choice of metavariable indicate the term's sort: @@ -196,13 +196,13 @@ We omit type annotations in binders, when the type is clear from context. \subsection{Types}\label{sec:types} Iris terms are simply-typed. -The judgment $\vctx \proves_\SigNat \wtt{\term}{\sort}$ expresses that, in signature $\SigNat$ and variable context $\vctx$, the term $\term$ has sort $\sort$. +The judgment $\vctx \proves_\Sig \wtt{\term}{\sort}$ expresses that, in signature $\Sig$ and variable context $\vctx$, the term $\term$ has sort $\sort$. In giving the rules for this judgment, we omit the signature (which does not change). A variable context, $\vctx = x_1:\sort_1, \dots, x_n:\sort_n$, declares a list of variables and their sorts. In writing $\vctx, x:\sort$, we presuppose that $x$ is not already declared in $\vctx$. -\judgment{Well-typed terms}{\vctx \proves_\SigNat \wtt{\term}{\sort}} +\judgment{Well-typed terms}{\vctx \proves_\Sig \wtt{\term}{\sort}} \begin{mathparpagebreakable} %%% variables and function symbols \axiom{x : \sort \proves \wtt{x}{\sort}} @@ -274,10 +274,10 @@ In writing $\vctx, x:\sort$, we presuppose that $x$ is not already declared in ${\vctx \proves \wtt{\prop \wand \propB}{\Prop}} \and \infer{ - \vctx, \pvar:\sort\to\Prop \proves \wtt{\pred}{\sort\to\Prop} \and - \text{$\pvar$is guarded in$\pred$} + \vctx, \var:\sort\to\Prop \proves \wtt{\pred}{\sort\to\Prop} \and + \text{$\var$is guarded in$\pred$} }{ - \vctx \proves \wtt{\MU \pvar. \pred}{\sort\to\Prop} + \vctx \proves \wtt{\MU \var. \pred}{\sort\to\Prop} } \and \infer{\vctx, x:\sort \proves \wtt{\prop}{\Prop}} @@ -410,31 +410,31 @@ Soundness follows from the theorem that${\cal U}(\any, \textdom{Prop}) {\pfctx \proves \exists X: \sort. \prop} \and \infer[$\forall_2$I] - {\pfctx, \pvar: \Pred(\sort) \proves \prop} - {\pfctx \proves \forall \pvar\in \Pred(\sort).\; \prop} + {\pfctx, \var: \Pred(\sort) \proves \prop} + {\pfctx \proves \forall \var\in \Pred(\sort).\; \prop} \and \infer[$\forall_2$E] - {\pfctx \proves \forall \pvar. \prop \\ + {\pfctx \proves \forall \var. \prop \\ \pfctx \proves \propB: \Prop} - {\pfctx \proves \prop[\propB/\pvar]} + {\pfctx \proves \prop[\propB/\var]} \and \infer[$\exists_2$E] - {\pfctx \proves \exists \pvar \in \Pred(\sort).\prop \\ - \pfctx, \pvar : \Pred(\sort), \prop \proves \propB} + {\pfctx \proves \exists \var \in \Pred(\sort).\prop \\ + \pfctx, \var : \Pred(\sort), \prop \proves \propB} {\pfctx \proves \propB} \and \infer[$\exists_2$I] - {\pfctx \proves \prop[\propB/\pvar] \\ + {\pfctx \proves \prop[\propB/\var] \\ \pfctx \proves \propB: \Prop} - {\pfctx \proves \exists \pvar. \prop} + {\pfctx \proves \exists \var. \prop} \and \inferB[Elem] {\pfctx \proves \term \in (X \in \sort). \prop} {\pfctx \proves \prop[\term/X]} \and \inferB[Elem-$\mu$] - {\pfctx \proves \term \in (\mu\pvar \in \Pred(\sort). \pred)} - {\pfctx \proves \term \in \pred[\mu\pvar \in \Pred(\sort). \pred/\pvar]} + {\pfctx \proves \term \in (\mu\var \in \Pred(\sort). \pred)} + {\pfctx \proves \term \in \pred[\mu\var \in \Pred(\sort). \pred/\var]} \end{mathpar} \subsection{Axioms from the logic of (affine) bunched implications} diff --git a/docs/iris/model.tex b/docs/iris/model.tex index ab298e7d1e6ab42deaba57e3766a58fa88ab06c5..0135b58ab14e9567dd3aacbd81a3e06d7a963472 100644 --- a/docs/iris/model.tex +++ b/docs/iris/model.tex @@ -149,36 +149,36 @@ For a set $X$, write $\Delta X$ for the discrete c.o.f.e.\ with $x \nequiv{n} x'$ iff $n = 0$ or $x = x'$ $\begin{array}[t]{@{}l@{\ }c@{\ }l@{}} -\semSort{\textsort{Unit}} &\eqdef& \Delta \{ \star \} \\ -\semSort{\textsort{InvName}} &\eqdef& \Delta \mathbb{N} \\ -\semSort{\textsort{InvMask}} &\eqdef& \Delta \pset{\mathbb{N}} \\ -\semSort{\textsort{Monoid}} &\eqdef& \Delta |\monoid| +\Sem{\textsort{Unit}} &\eqdef& \Delta \{ \star \} \\ +\Sem{\textsort{InvName}} &\eqdef& \Delta \mathbb{N} \\ +\Sem{\textsort{InvMask}} &\eqdef& \Delta \pset{\mathbb{N}} \\ +\Sem{\textsort{Monoid}} &\eqdef& \Delta |\monoid| \end{array} \qquad\qquad \begin{array}[t]{@{}l@{\ }c@{\ }l@{}} -\semSort{\textsort{Val}} &\eqdef& \Delta \textdom{Val} \\ -\semSort{\textsort{Exp}} &\eqdef& \Delta \textdom{Exp} \\ -\semSort{\textsort{Ectx}} &\eqdef& \Delta \textdom{Ectx} \\ -\semSort{\textsort{State}} &\eqdef& \Delta \textdom{State} \\ +\Sem{\textsort{Val}} &\eqdef& \Delta \textdom{Val} \\ +\Sem{\textsort{Exp}} &\eqdef& \Delta \textdom{Exp} \\ +\Sem{\textsort{Ectx}} &\eqdef& \Delta \textdom{Ectx} \\ +\Sem{\textsort{State}} &\eqdef& \Delta \textdom{State} \\ \end{array} \qquad\qquad \begin{array}[t]{@{}l@{\ }c@{\ }l@{}} -\semSort{\sort \times \sort'} &\eqdef& \semSort{\sort} \times \semSort{\sort} \\ -\semSort{\sort \to \sort'} &\eqdef& \semSort{\sort} \to \semSort{\sort} \\ -\semSort{\Prop} &\eqdef& \textdom{Prop} \\ +\Sem{\sort \times \sort'} &\eqdef& \Sem{\sort} \times \Sem{\sort} \\ +\Sem{\sort \to \sort'} &\eqdef& \Sem{\sort} \to \Sem{\sort} \\ +\Sem{\Prop} &\eqdef& \textdom{Prop} \\ \end{array}$ -The balance of our signature $\SigNat$ is interpreted as follows. +The balance of our signature $\Sig$ is interpreted as follows. For each base type $\type$ not covered by the preceding table, we pick an object $X_\type$ in $\cal U$ and define $-\semSort{\type} \eqdef X_\type +\Sem{\type} \eqdef X_\type$ -For each function symbol $\sigfn : \type_1, \dots, \type_n \to \type_{n+1} \in \SigFn$, we pick an arrow $\Sem{\sigfn} : \semSort{\type_1} \times \dots \times \semSort{\type_n} \to \semSort{\type_{n+1}}$ in $\cal U$. +For each function symbol $\sigfn : \type_1, \dots, \type_n \to \type_{n+1} \in \SigFn$, we pick an arrow $\Sem{\sigfn} : \Sem{\type_1} \times \dots \times \Sem{\type_n} \to \Sem{\type_{n+1}}$ in $\cal U$. An environment $\vctx$ is interpreted as the set of maps $\rho$, with $\dom(\rho) = \dom(\vctx)$ and -$\rho(x)\in\semSort{\vctx(x)}$, +$\rho(x)\in\Sem{\vctx(x)}$, and $\rho\nequiv{n} \rho' \iff n=0 \lor \bigl(\dom(\rho)=\dom(\rho') \land \All x\in\dom(\rho). \rho(x) \nequiv{n} \rho'(x)\bigr)$. @@ -420,89 +420,89 @@ $\rho\nequiv{n} \rho' \iff n=0 \lor \bigl(\dom(\rho)=\dom(\rho') \land $\mathit{wp}_\mask(\val, q) = \mathit{vs}_{\mask}^{\mask}(q \: \val)$ \end{lem} -\typedsection{Interpretation of terms}{\Sem{\vctx \proves \term : \sort} : \Sem{\vctx} \to \semSort{\sort} \in {\cal U}} +\typedsection{Interpretation of terms}{\Sem{\vctx \proves \term : \sort} : \Sem{\vctx} \to \Sem{\sort} \in {\cal U}} -%A term$\vctx \proves \term : \sort$is interpreted as a non-expansive map from$\Sem{\vctx}$to$\semSort{\sort}$. +%A term$\vctx \proves \term : \sort$is interpreted as a non-expansive map from$\Sem{\vctx}$to$\Sem{\sort}. \begin{align*} - \semTerm{\vctx \proves x : \sort}_\gamma &= \gamma(x) \\ - \semTerm{\vctx \proves \sigfn(\term_1, \dots, \term_n) : \type_{n+1}}_\gamma &= \Sem{\sigfn}(\semTerm{\vctx \proves \term_1 : \type_1}_\gamma, \dots, \semTerm{\vctx \proves \term_n : \type_n}_\gamma) \ \WHEN \sigfn : \type_1, \dots, \type_n \to \type_{n+1} \in \SigFn \\ - \semTerm{\vctx \proves \Lam x. \term : \sort \to \sort'}_\gamma &= - \Lam v : \semSort{\sort}. \semTerm{\vctx, x : \sort \proves \term : \sort'}_{\gamma[x \mapsto v]} \\ - \semTerm{\vctx \proves \term~\termB : \sort'}_\gamma &= - \semTerm{\vctx \proves \term : \sort \to \sort'}_\gamma(\semTerm{\vctx \proves \termB : \sort}_\gamma) \\ - \semTerm{\vctx \proves \unitterm : \unitsort}_\gamma &= \star \\ - \semTerm{\vctx \proves (\term_1, \term_2) : \sort_1 \times \sort_2}_\gamma &= (\semTerm{\vctx \proves \term_1 : \sort_1}_\gamma, \semTerm{\vctx \proves \term_2 : \sort_2}_\gamma) \\ - \semTerm{\vctx \proves \pi_i~\term : \sort_1}_\gamma &= \pi_i(\semTerm{\vctx \proves \term : \sort_1 \times \sort_2}_\gamma) + \Sem{\vctx \proves x : \sort}_\gamma &= \gamma(x) \\ + \Sem{\vctx \proves \sigfn(\term_1, \dots, \term_n) : \type_{n+1}}_\gamma &= \Sem{\sigfn}(\Sem{\vctx \proves \term_1 : \type_1}_\gamma, \dots, \Sem{\vctx \proves \term_n : \type_n}_\gamma) \ \WHEN \sigfn : \type_1, \dots, \type_n \to \type_{n+1} \in \SigFn \\ + \Sem{\vctx \proves \Lam x. \term : \sort \to \sort'}_\gamma &= + \Lam v : \Sem{\sort}. \Sem{\vctx, x : \sort \proves \term : \sort'}_{\gamma[x \mapsto v]} \\ + \Sem{\vctx \proves \term~\termB : \sort'}_\gamma &= + \Sem{\vctx \proves \term : \sort \to \sort'}_\gamma(\Sem{\vctx \proves \termB : \sort}_\gamma) \\ + \Sem{\vctx \proves \unitterm : \unitsort}_\gamma &= \star \\ + \Sem{\vctx \proves (\term_1, \term_2) : \sort_1 \times \sort_2}_\gamma &= (\Sem{\vctx \proves \term_1 : \sort_1}_\gamma, \Sem{\vctx \proves \term_2 : \sort_2}_\gamma) \\ + \Sem{\vctx \proves \pi_i~\term : \sort_1}_\gamma &= \pi_i(\Sem{\vctx \proves \term : \sort_1 \times \sort_2}_\gamma) \end{align*} % \begin{align*} - \semTerm{\vctx \proves \mzero : \textsort{Monoid}}_\gamma &= \mzero \\ - \semTerm{\vctx \proves \munit : \textsort{Monoid}}_\gamma &= \munit \\ - \semTerm{\vctx \proves \melt \mtimes \meltB : \textsort{Monoid}}_\gamma &= - \semTerm{\vctx \proves \melt : \textsort{Monoid}}_\gamma \mtimes \semTerm{\vctx \proves \meltB : \textsort{Monoid}}_\gamma + \Sem{\vctx \proves \mzero : \textsort{Monoid}}_\gamma &= \mzero \\ + \Sem{\vctx \proves \munit : \textsort{Monoid}}_\gamma &= \munit \\ + \Sem{\vctx \proves \melt \mtimes \meltB : \textsort{Monoid}}_\gamma &= + \Sem{\vctx \proves \melt : \textsort{Monoid}}_\gamma \mtimes \Sem{\vctx \proves \meltB : \textsort{Monoid}}_\gamma \end{align*} % \begin{align*} - \semTerm{\vctx \proves t =_\sort u : \Prop}_\gamma &= - \Lam W. \{\, (n, r) \mid \semTerm{\vctx \proves t : \sort}_\gamma \nequiv{n+1} \semTerm{\vctx \proves u : \sort}_\gamma \,\} \\ - \semTerm{\vctx \proves \FALSE : \Prop}_\gamma &= \Lam W. \emptyset \\ - \semTerm{\vctx \proves \TRUE : \Prop}_\gamma &= \Lam W. \mathbb{N} \times \textdom{Res} \\ - \semTerm{\vctx \proves P \land Q : \Prop}_\gamma &= - \Lam W. \semTerm{\vctx \proves P : \Prop}_\gamma(W) \cap \semTerm{\vctx \proves Q : \Prop}_\gamma(W) \\ - \semTerm{\vctx \proves P \lor Q : \Prop}_\gamma &= - \Lam W. \semTerm{\vctx \proves P : \Prop}_\gamma(W) \cup \semTerm{\vctx \proves Q : \Prop}_\gamma(W) \\ - \semTerm{\vctx \proves P \Ra Q : \Prop}_\gamma &= + \Sem{\vctx \proves t =_\sort u : \Prop}_\gamma &= + \Lam W. \{\, (n, r) \mid \Sem{\vctx \proves t : \sort}_\gamma \nequiv{n+1} \Sem{\vctx \proves u : \sort}_\gamma \,\} \\ + \Sem{\vctx \proves \FALSE : \Prop}_\gamma &= \Lam W. \emptyset \\ + \Sem{\vctx \proves \TRUE : \Prop}_\gamma &= \Lam W. \mathbb{N} \times \textdom{Res} \\ + \Sem{\vctx \proves P \land Q : \Prop}_\gamma &= + \Lam W. \Sem{\vctx \proves P : \Prop}_\gamma(W) \cap \Sem{\vctx \proves Q : \Prop}_\gamma(W) \\ + \Sem{\vctx \proves P \lor Q : \Prop}_\gamma &= + \Lam W. \Sem{\vctx \proves P : \Prop}_\gamma(W) \cup \Sem{\vctx \proves Q : \Prop}_\gamma(W) \\ + \Sem{\vctx \proves P \Ra Q : \Prop}_\gamma &= \Lam W. \begin{aligned}[t] \{\, (n, r) &\mid \All n' \leq n. \All W' \geq W. \All r' \geq r. \\ &\qquad - (n', r') \in \semTerm{\vctx \proves P : \Prop}_\gamma(W')~ \\ + (n', r') \in \Sem{\vctx \proves P : \Prop}_\gamma(W')~ \\ &\qquad - \implies (n', r') \in \semTerm{\vctx \proves Q : \Prop}_\gamma(W') \,\} + \implies (n', r') \in \Sem{\vctx \proves Q : \Prop}_\gamma(W') \,\} \end{aligned} \\ - \semTerm{\vctx \proves \All x : \sort. P : \Prop}_\gamma &= - \Lam W. \{\, (n, r) \mid \All v \in \semSort{\sort}. (n, r) \in \semTerm{\vctx, x : \sort \proves P : \Prop}_{\gamma[x \mapsto v]}(W) \,\} \\ - \semTerm{\vctx \proves \Exists x : \sort. P : \Prop}_\gamma &= - \Lam W. \{\, (n, r) \mid \Exists v \in \semSort{\sort}. (n, r) \in \semTerm{\vctx, x : \sort \proves P : \Prop}_{\gamma[x \mapsto v]}(W) \,\} + \Sem{\vctx \proves \All x : \sort. P : \Prop}_\gamma &= + \Lam W. \{\, (n, r) \mid \All v \in \Sem{\sort}. (n, r) \in \Sem{\vctx, x : \sort \proves P : \Prop}_{\gamma[x \mapsto v]}(W) \,\} \\ + \Sem{\vctx \proves \Exists x : \sort. P : \Prop}_\gamma &= + \Lam W. \{\, (n, r) \mid \Exists v \in \Sem{\sort}. (n, r) \in \Sem{\vctx, x : \sort \proves P : \Prop}_{\gamma[x \mapsto v]}(W) \,\} \end{align*} % \begin{align*} - \semTerm{\vctx \proves \always{\prop} : \Prop}_\gamma &= \always{\semTerm{\vctx \proves \prop : \Prop}_\gamma} \\ - \semTerm{\vctx \proves \later{\prop} : \Prop}_\gamma &= \later \semTerm{\vctx \proves \prop : \Prop}_\gamma\\ - \semTerm{\vctx \proves \MU x. \pred : \sort \to \Prop}_\gamma &= - \mathit{fix}(\Lam v : \semSort{\sort \to \Prop}. \semTerm{\vctx, x : \sort \to \Prop \proves \pred : \sort \to \Prop}_{\gamma[x \mapsto v]}) \\ - \semTerm{\vctx \proves \prop * \propB : \Prop}_\gamma &= + \Sem{\vctx \proves \always{\prop} : \Prop}_\gamma &= \always{\Sem{\vctx \proves \prop : \Prop}_\gamma} \\ + \Sem{\vctx \proves \later{\prop} : \Prop}_\gamma &= \later \Sem{\vctx \proves \prop : \Prop}_\gamma\\ + \Sem{\vctx \proves \MU x. \pred : \sort \to \Prop}_\gamma &= + \mathit{fix}(\Lam v : \Sem{\sort \to \Prop}. \Sem{\vctx, x : \sort \to \Prop \proves \pred : \sort \to \Prop}_{\gamma[x \mapsto v]}) \\ + \Sem{\vctx \proves \prop * \propB : \Prop}_\gamma &= \begin{aligned}[t] \Lam W. \{\, (n, r) &\mid \Exists r_1, r_2. r = r_1 \bullet r_2 \land{} \\ &\qquad - (n, r_1) \in \semTerm{\vctx \proves \prop : \Prop}_\gamma \land{} \\ + (n, r_1) \in \Sem{\vctx \proves \prop : \Prop}_\gamma \land{} \\ &\qquad - (n, r_2) \in \semTerm{\vctx \proves \propB : \Prop}_\gamma \,\} + (n, r_2) \in \Sem{\vctx \proves \propB : \Prop}_\gamma \,\} \end{aligned} \\ - \semTerm{\vctx \proves \prop \wand \propB : \Prop}_\gamma &= + \Sem{\vctx \proves \prop \wand \propB : \Prop}_\gamma &= \begin{aligned}[t] \Lam W. \{\, (n, r) &\mid \All n' \leq n. \All W' \geq W. \All r'. \\ &\qquad - (n', r') \in \semTerm{\vctx \proves \prop : \Prop}_\gamma(W') \land r \sep r' \\ + (n', r') \in \Sem{\vctx \proves \prop : \Prop}_\gamma(W') \land r \sep r' \\ &\qquad - \implies (n', r \bullet r') \in \semTerm{\vctx \proves \propB : \Prop}_\gamma(W') + \implies (n', r \bullet r') \in \Sem{\vctx \proves \propB : \Prop}_\gamma(W') \} \end{aligned} \\ - \semTerm{\vctx \proves \knowInv{\iname}{\prop} : \Prop}_\gamma &= - inv(\semTerm{\vctx \proves \iname : \textsort{InvName}}_\gamma, \semTerm{\vctx \proves \prop : \Prop}_\gamma) \\ - \semTerm{\vctx \proves \ownGGhost{\melt} : \Prop}_\gamma &= - \Lam W. \{\, (n, \rs) \mid \rs.\ghostRes \geq \semTerm{\vctx \proves \melt : \textsort{Monoid}}_\gamma \,\} \\ - \semTerm{\vctx \proves \ownPhys{\state} : \Prop}_\gamma &= - \Lam W. \{\, (n, \rs) \mid \rs.\pres = \semTerm{\vctx \proves \state : \textsort{State}}_\gamma \,\} + \Sem{\vctx \proves \knowInv{\iname}{\prop} : \Prop}_\gamma &= + inv(\Sem{\vctx \proves \iname : \textsort{InvName}}_\gamma, \Sem{\vctx \proves \prop : \Prop}_\gamma) \\ + \Sem{\vctx \proves \ownGGhost{\melt} : \Prop}_\gamma &= + \Lam W. \{\, (n, \rs) \mid \rs.\ghostRes \geq \Sem{\vctx \proves \melt : \textsort{Monoid}}_\gamma \,\} \\ + \Sem{\vctx \proves \ownPhys{\state} : \Prop}_\gamma &= + \Lam W. \{\, (n, \rs) \mid \rs.\pres = \Sem{\vctx \proves \state : \textsort{State}}_\gamma \,\} \end{align*} % \begin{align*} - \semTerm{\vctx \proves \pvsA{\prop}{\mask_1}{\mask_2} : \Prop}_\gamma &= - \textdom{vs}^{\semTerm{\vctx \proves \mask_2 : \textsort{InvMask}}_\gamma}_{\semTerm{\vctx \proves \mask_1 : \textsort{InvMask}}_\gamma}(\semTerm{\vctx \proves \prop : \Prop}_\gamma) \\ - \semTerm{\vctx \proves \dynA{\expr}{\pred}{\mask} : \Prop}_\gamma &= - \textdom{wp}_{\semTerm{\vctx \proves \mask : \textsort{InvMask}}_\gamma}(\semTerm{\vctx \proves \expr : \textsort{Exp}}_\gamma, \semTerm{\vctx \proves \pred : \textsort{Val} \to \Prop}_\gamma) \\ - \semTerm{\vctx \proves \wtt{\timeless{\prop}}{\Prop}}_\gamma &= - \textdom{timeless}(\semTerm{\vctx \proves \prop : \Prop}_\gamma) + \Sem{\vctx \proves \pvsA{\prop}{\mask_1}{\mask_2} : \Prop}_\gamma &= + \textdom{vs}^{\Sem{\vctx \proves \mask_2 : \textsort{InvMask}}_\gamma}_{\Sem{\vctx \proves \mask_1 : \textsort{InvMask}}_\gamma}(\Sem{\vctx \proves \prop : \Prop}_\gamma) \\ + \Sem{\vctx \proves \dynA{\expr}{\pred}{\mask} : \Prop}_\gamma &= + \textdom{wp}_{\Sem{\vctx \proves \mask : \textsort{InvMask}}_\gamma}(\Sem{\vctx \proves \expr : \textsort{Exp}}_\gamma, \Sem{\vctx \proves \pred : \textsort{Val} \to \Prop}_\gamma) \\ + \Sem{\vctx \proves \wtt{\timeless{\prop}}{\Prop}}_\gamma &= + \textdom{timeless}(\Sem{\vctx \proves \prop : \Prop}_\gamma) \end{align*} \typedsection{Interpretation of entailment}{\Sem{\vctx \mid \pfctx \proves \prop} : 2 \in \mathit{Sets}} @@ -514,10 +514,10 @@\rho\nequiv{n} \rho' \iff n=0 \lor \bigl(\dom(\rho)=\dom(\rho') \land \forall n \in \mathbb{N}.\; \forall W \in \textdom{World}.\; \forall \rs \in \textdom{Res}.\; -\forall \gamma \in \semSort{\vctx},\; +\forall \gamma \in \Sem{\vctx},\; \\& -\bigl(\All \propB \in \pfctx. (n, \rs) \in \semTerm{\vctx \proves \propB : \Prop}_\gamma(W)\bigr) -\implies (n, \rs) \in \semTerm{\vctx \proves \prop : \Prop}_\gamma(W) +\bigl(\All \propB \in \pfctx. (n, \rs) \in \Sem{\vctx \proves \propB : \Prop}_\gamma(W)\bigr) +\implies (n, \rs) \in \Sem{\vctx \proves \prop : \Prop}_\gamma(W) \end{aligned} \] diff --git a/docs/setup.tex b/docs/setup.tex index b8e184fcc46bf33ef941974569d80733eb04e912..5ba0f0f2009666a8079fc745dde7f71f51c5715b 100644 --- a/docs/setup.tex +++ b/docs/setup.tex @@ -1,5 +1,5 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% PACKAGES +%% PACKAGES %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \usepackage{mathtools} %\usepackage{amsmath} @@ -32,7 +32,7 @@ \usepackage{hyperref} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% SETUP +%% SETUP %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \extrarowheight=\jot % else, arrays are scrunched compared to, say, aligned @@ -85,7 +85,7 @@ \newtheorem{exercise}{Exercise} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% FONTS & FORMATTING +%% FONTS & FORMATTING %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \SetSymbolFont{stmry}{bold}{U}{stmry}{m}{n} % this fixes warnings when \boldsymbol is used with stmaryrd included @@ -97,7 +97,7 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% GENERIC MACROS +%% GENERIC MACROS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \newcommand*{\Sref}[1]{\hyperref[#1]{\S\ref*{#1}}} \newcommand*{\secref}[1]{\hyperref[#1]{Section~\ref*{#1}}} @@ -112,18 +112,31 @@ \newcommand{\changes}{{\bf\color{red}{Changes}}} \newcommand{\TODO}{\vskip 4pt {\color{red}\bf TODO}} -%\newcommand{\bigast}{\scalebox{3}{\raisebox{-0.3ex}{$\ast$}}} -%\newcommand{\bigtimes}{\scalebox{2.5}{\raisebox{-0.3ex}{$\times$}}} -\DeclareMathOperator*{\Sep}{\scalerel*{\ast}{\sum}} -\newcommand{\bigast}{\Sep} -\newcommand*{\sep}[1][]{\mathrel{\#_{#1}}} % bad name; it's a different "sep" +\newcommand{\ie}{\emph{i.e.,} } +\newcommand{\eg}{\emph{e.g.,} } +\newcommand{\etal}{\emph{et~al.}} +\newcommand{\wrt}{w.r.t.~} -\newcommand{\ALT}{\ |\ } +\newcommand{\aaron}[1]{{\color{red}\textbf{AT: #1}}} +\newcommand{\derek}[1]{{\color{red}\textbf{DD: #1}}} +\newcommand{\lars}[1]{{\color{red}\textbf{LB: #1}}} +\newcommand{\kasper}[1]{{\color{red}\textbf{KS: #1}}} +\newcommand{\ralf}[1]{{\color{red}\textbf{RJ: #1}}} +\newcommand{\dave}[1]{{\color{red}\textbf{PDS: #1}}} +\newcommand{\hush}[1]{} +\newcommand{\relaxguys}{% + \let\aaron\hush% + \let\derek\hush% + \let\lars\hush% + \let\kasper\hush% + \let\ralf\hush% + \let\dave\hush% +} -\newenvironment{pf} - {\resetpfcounter\begin{proof}} - {\end{proof}} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% MATH SYMBOLS & NOTATION & IDENTIFIERS +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % superscript to the left \def\presuper#1#2% @@ -132,226 +145,196 @@ \kern-\scriptspace% #2} +\DeclareMathOperator*{\Sep}{\scalerel*{\ast}{\sum}} +\newcommand{\bigast}{\Sep} + +\newcommand*{\sep}[1][]{\mathrel{\#_{#1}}} % bad name; it's a different "sep" + +\newcommand{\ALT}{\ |\ } + \newcommand{\upclose}{\mathord{\uparrow}} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% LANGUAGE-LEVEL SYNTAX AND SEMANTICS -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\def\All #1.{\forall #1.\;}% +\def\Exists #1.{\exists #1.\;}% +\def\Ret #1.{#1.\;}% -\newcommand{\cfg}[2]{{#1};{#2}} -\newcommand{\fork}[1]{\textlang{fork}\;{#1}} +\newcommand{\any}{{\rule[-.2ex]{1ex}{.4pt}}}% +\newcommand{\unitval}{()}% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% METAVARIABLES -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\newcommand{\aexpr}{a} -\newcommand{\expr}{e} -\newcommand{\type}{\tau} -\newcommand{\htype}{\sigma} -\newcommand{\ctype}{\sigma} -\newcommand{\heap}{h} -\newcommand{\tyvar}{\alpha} -\newcommand{\tyvarB}{\beta} -\newcommand{\val}{v} -\newcommand{\valB}{w} -\newcommand{\hval}{u} -\newcommand{\tls}{L} -\newcommand{\tlsVar}{L} +\newcommand{\judgment}[2]{\paragraph{#1}\hspace{\stretch{1}}\fbox{$#2$}} -\newcommand{\cenv}{\Omega} -\newcommand{\tenv}{\Gamma} -\newcommand{\tvenv}{\Delta} +\newcommand{\pfn}{\rightharpoonup} +\newcommand{\fpfn}{\stackrel{\textrm{fin}}{\rightharpoonup}} +\newcommand{\ra}{\rightarrow} +\newcommand{\Ra}{\Rightarrow} +\newcommand{\Lra}{\Leftrightarrow} +\newcommand{\monra}{\stackrel{\textrm{mon}}{\rightarrow}} -%\newcommand{\vctx}{\mathcal{X}} -\newcommand{\pvar}{p} -\newcommand{\pvarB}{q} -%\newcommand{\pvarC}{r} +\newcommand{\eqdef}{\triangleq} -\newcommand{\ectx}{K} -\newcommand{\tpool}{T} +\newcommand{\restr}[2]{\lfloor #1 \rfloor_{#2}} +\newcommand{\pset}[1]{\wp(#1)} % Powerset +\newcommand{\psetdown}[1]{\wp^\downarrow(#1)} -% \newcommand{\progexpr}{p} -% \newcommand{\progctx}{D} +\newcommand{\dom}{\textrm{dom}} +%\newcommand{\rng}{\textrm{rng}} +%\newcommand{\cod}{\textrm{cod}} -\newcommand{\subst}{\gamma} -%\newcommand{\island}{I} -\newcommand{\sisland}{\iota} -%\newcommand{\islands}{\omega} -%\newcommand{\islands}{\mathbf{\island}} +\newcommand{\IF}{\mathrel{\text{if}}} +\newcommand{\WHEN}{\textrm{when }} -\newcommand{\predinterp}{\PRED} -\newcommand{\propinterp}{\mathcal{P}} -\newcommand{\PROP}{\mathcal{P}} -\newcommand{\PROPB}{\mathcal{Q}} -\newcommand{\interp}{\textrm{interp}} -\newcommand{\interps}{\textrm{interpAll}} +\newcommand{\SET}[2]{ +\left\{% +#1% +\;\middle|\;% +#2% +\right\} +} +\newcommand{\SETB}[1]{ +\left\{% +#1% +\right\} +} +\newcommand{\SETC}[2]{#1 & #2} -\newcommand{\restype}{\theta} -\newcommand{\restypes}{\boldsymbol{\theta}} +\newenvironment{inbox}[1][]{ + \begin{array}[#1]{@{}l@{}} +}{ + \end{array} +} +\newcommand{\tabubox}[2][]{% + \begin{tabu}{@{#1}X[1,l,m]@{}}% + #2 % + \end{tabu}% +} -%\newcommand{\aprop}{{\color{red}A}} -\newcommand{\prop}{P} -\newcommand{\propB}{Q} -\newcommand{\propC}{R} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% CMRA (RESOURCE ALGEBRA) SYMBOLS & NOTATION & IDENTIFIERS +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\newcommand{\monoid}{M} -\newcommand{\pred}{\varphi} -\newcommand{\predB}{\psi} -\newcommand{\predC}{\zeta} +\newcommand{\melt}{a} +\newcommand{\meltB}{b} +\newcommand{\meltC}{c} +\newcommand{\melts}{A} +\newcommand{\meltsB}{B} + +\newcommand{\mcar}[1]{|#1|} +\newcommand{\mcarp}[1]{\mcar{#1}^{+}} +\newcommand{\mzero}{\bot} +\newcommand{\munit}{\mathord{\varepsilon}} +\newcommand{\mtimes}{\mathbin{\cdot}} -% \newcommand{\Prop}{\mathbb{B}} -% \newcommand{\Pred}{\mathbb{P}} +\newcommand{\mupd}{\rightsquigarrow} + + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% MODEL-SPECIFIC SYMBOLS & NOTATION & IDENTIFIERS +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\newcommand{\wIso}{\xi} \newcommand{\rs}{r} \newcommand{\rsB}{s} -%\newcommand{\propSet}{\mathcal{P}} -%\newcommand{\apropSet}{\mathcal{A}} -%\newcommand{\pfctx}{\mathcal{C}} -\newcommand{\vctx}{\Gamma} -\newcommand{\pfctx}{\Theta} +\newcommand{\pres}{\pi} +\newcommand{\ghostRes}{g} -\newcommand{\assert}{\varphi} -\newcommand{\assertB}{\psi} +%% Various pieces of syntax +\newcommand{\fullSat}[4]{#1 \models_{#2} #3; #4} -\newcommand{\PRED}{\Phi} +\newcommand{\wtt}[2]{#1 : #2} % well-typed term -%% \newcommand{\pname}{\pi} -%% \newcommand{\prot}{\pi} -%% \newcommand{\prots}{\boldsymbol{\pi}} -%% \newcommand{\protSet}{\mathcal{N}} +\newcommand{\nequiv}[1]{\ensuremath{\mathrel{\stackrel{#1}{=}}}} +\newcommand{\notnequiv}[1]{\ensuremath{\mathrel{\stackrel{#1}{\neq}}}} +\newcommand{\nequivset}[2]{\ensuremath{\mathrel{\stackrel{#1}{=}_{#2}}}} +\newcommand{\nequivB}[1]{\ensuremath{\mathrel{\stackrel{#1}{\equiv}}}} +\newcommand{\latert}{\mathord{\blacktriangleright}} -\newcommand{\iname}{\iota} -\newcommand{\inameB}{\iota'} -\newcommand{\inv}{I} -\newcommand{\invs}{\mathcal{I}} -\newcommand{\mask}{\mathcal{E}} +\newcommand{\Sem}[1]{\llbracket #1 \rrbracket} -\newcommand{\state}{\varsigma} -\newcommand{\prescar}{\Pi} -\newcommand{\pres}{\pi} +\newcommand{\sembox}[1]{\hfill \normalfont \mbox{\fbox{$$#1$$}}} +\newcommand{\typedsection}[2]{\subsubsection*{\rm\em #1 \sembox{#2}}} -\newcommand{\var}{x} -\newcommand{\varB}{y} -\newcommand{\varC}{z} -%\newcommand{\VAL}{d} -\newcommand{\ectxVar}{\kappa} -\newcommand{\term}{t} -\newcommand{\termB}{u} -\newcommand{\termVal}{V} +%% Some commonly used identifiers +\newcommand{\UPred}{\textdom{UPred}} +\newcommand{\SPred}{\textdom{SPred}} -\newcommand{\sort}{\sigma} +\newcommand{\PropDom}{\textdom{Prop}} +\newcommand{\PredDom}{\textdom{Pred}} -\newcommand{\SigNat}{\Sigma} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% LOGIC SYMBOLS & NOTATION & IDENTIFIERS +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\newcommand{\Sig}{\Sigma} \newcommand{\SigType}{\mathcal{T}} \newcommand{\SigFn}{\mathcal{F}} \newcommand{\sigfn}{F} -\newcommand{\tmap}{B} -\newcommand{\ttokSet}{I} - -\newcommand{\monoid}{M} +\newcommand{\type}{\tau} -%\newcommand{\mvar}{a} -%\newcommand{\mvarB}{b} -\newcommand{\melt}{a} -\newcommand{\meltB}{b} -\newcommand{\meltC}{c} -\newcommand{\melts}{A} -\newcommand{\meltsB}{B} -\newcommand{\ghostRes}{g} +\newcommand{\var}{x} +\newcommand{\varB}{y} +\newcommand{\varC}{z} -\newcommand{\gname}{\gamma} +\newcommand{\term}{t} +\newcommand{\termB}{u} +\newcommand{\termVal}{V} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% IDENTIFIERS -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\newcommand{\sort}{\sigma} +\newcommand{\vctx}{\Gamma} +\newcommand{\pfctx}{\Theta} -\newcommand{\Prop}{\textlog{Prop}} -\newcommand{\Pred}{\textlog{Pred}} +\newcommand{\prop}{P} +\newcommand{\propB}{Q} +\newcommand{\propC}{R} -\newcommand{\PropDom}{\textdom{Prop}} -\newcommand{\PredDom}{\textdom{Pred}} +\newcommand{\pred}{\varphi} +\newcommand{\predB}{\psi} +\newcommand{\predC}{\zeta} +\newcommand{\gname}{\gamma} +\newcommand{\iname}{\iota} +\newcommand{\inameB}{\iota'} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% SYMBOLS, NOTATION -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\newcommand{\mask}{\mathcal{E}} -\def\All #1.{\forall #1.\;}% -\def\Exists #1.{\exists #1.\;}% -\def\Absp #1.{({#1}).\;} -\def\Ret #1.{#1.\;}% -\def\Lam #1.{\lambda #1.\;}% +%% various pieces of Syntax \def\MU #1.{\mu #1.\;}% -\newcommand{\any}{{\rule[-.2ex]{1ex}{.4pt}}}% -\newcommand{\unitval}{()}% +\def\Lam #1.{\lambda #1.\;}% +\newcommand{\proves}{\vdash} +\newcommand{\provesalways}{\vdash_{\!\!\boxempty}} -\newcommand{\fullSat}[4]{#1 \models_{#2} #3; #4} -\newcommand{\fullNSat}[6]{#2 \models_{#3}^{#1} #4; #5; #6} +\newcommand{\wand}{\;{{\mbox{---}}\!\!{*}}\;} -\newcommand{\erasestate}[1]{|#1|_\state} -\newcommand{\eraseexp}[1]{|#1|_\expr} +\newcommand{\fmapsto}[1][-]{\stackrel{#1}{\mapsto}} +\newcommand{\gmapsto}{\hookrightarrow}% +\newcommand{\fgmapsto}[1][-]{\stackrel{#1}{\gmapsto}}% -\newcommand{\mcar}[1]{|#1|} -\newcommand{\mcarp}[1]{\mcar{#1}^{+}} -\newcommand{\mzero}{\bot} -\newcommand{\munit}{\mathord{\varepsilon}} -\newcommand{\mtimes}{\mathbin{\cdot}} +\newcommand{\dyn}[2]{\textlog{wp}({#1}, {#2})} +\newcommand{\adyn}[2]{{#1}\;\llparenthesis{#2}\rrparenthesis} +\newcommand{\dynpred}[2]{\textdom{wp}({#1}, {#2})} +\newcommand{\dynA}[3]{\textlog{wp}_{#3}({#1}, {#2})} +\newcommand{\pvs}[1]{\textlog{vs}({#1})} +\newcommand{\pvsA}[3]{\textlog{vs}_{#2}^{#3}({#1})} -\newcommand{\gtimes}{\bullet} - - - -\newcommand{\protAt}[3]{\mbox{$- \begin{array}{|@{}l@{}|@{}l@{}|} - \firsthline \;#1 : #2\;\; & \;#3\;\; \\ - \lasthline - \end{array}$}} -\newcommand{\protAtB}[2]{\mbox{$- \begin{array}{|@{}l@{}|} - \firsthline \;#1 : #2\;\; \\ - \lasthline - \end{array}$}} - -% PDS: The baseline of the boxed contents of -% \oldKnowInv and \oldOwnGGhost and \oldOwnGhost isn't right: -% It can be lower than the surrounding formula. -%\newcommand{\oldKnowInv}[2]{\mbox{$-% \begin{array}{|@{\;}c@{\;}|} -% \firsthline #2 \\ -% \lasthline -% \end{array}$}{}^{\,#1}} - -%% \newcommand{\ownGhost}[2]{{\dbox{$#1 : #2$}}} -%% \newcommand{\ownGhostB}[3]{\dbox{$#1 : #2$}{}_{#3}} - -% \newcommand{\ownGhost}[3]{\mbox{$-% \begin{array}{:@{}l@{}:@{}l@{}:} -% \firsthdashline \;#1 : #2\;\; & \;#3\;\; \\ -% \lasthdashline -% \end{array}$}} -%\newcommand{\oldOwnGhost}[2]{\mbox{$-% \begin{array}{:@{\;}c@{\;}:} -% \firsthdashline #2 \\ -% \lasthdashline -% \end{array}$}{}^{\,#1}} -%\newcommand{\oldOwnGGhost}[1]{\mbox{$-% \begin{array}{:@{\;}c@{\;}:} -% \firsthdashline #1 \\ -% \lasthdashline -% \end{array}$}} +\newcommand{\later}{\mathord{\triangleright}} +\newcommand{\always}{\Box{}} +%% Invariants and Ghost ownership % PDS: Was 0pt inner, 2pt outer. % \boxedassert [tikzoptions] contents [name] \tikzstyle{boxedassert_border} = [sharp corners,line width=0.2pt] @@ -368,22 +351,7 @@ \newcommand{\ownPhys}[1]{\lfloor#1\rfloor} -\newcommand{\supported}[1]{\left[ #1 \right]} - - -%\newcommand*{\know}[2]{\knowInv{#1}{#2}}% -%\newcommand*{\own}[2]{\ownGhost{#1}{#2}}% - -%\newcommand{\varset}{\mathcal{X}} - -\newcommand{\simpl}{\textsc{i}} -\newcommand{\sspec}{\textsc{s}} -\newcommand{\IMSP}{\simpl\sspec} - -\newcommand{\pointsto}{\hookrightarrow} -\newcommand{\wand}{\;{{\mbox{---}}\!\!{*}}\;} -%\newcommand{\gm}{\Rrightarrow} - +%% View Shifts \NewDocumentCommand \vsGen {O{} m O{}}% {\mathrel{% \ifthenelse{\equal{#3}{}}{% @@ -399,143 +367,7 @@ \NewDocumentCommand \vsE {O{} O{}} % {\vsGen[#1]{\Lleftarrow\!\!\!\Rrightarrow}[#2]} -\newcommand{\mupd}{\rightsquigarrow} - -\newcommand{\heapmaps}[1]{\hookrightarrow_{#1}} -\newcommand{\codemaps}[1]{\Mapsto_{#1}} - -\newcommand{\implmaps}{\heapmaps{\IM}} -\newcommand{\implmapscode}{\codemaps{\IM}} - -\newcommand{\specmaps}{\heapmaps{\SP}} -\newcommand{\specmapscode}{\codemaps{\SP}} - -\newcommand{\IM}{\simpl} -\newcommand{\SP}{\sspec} - -%\newcommand{\tRole}[1]{\texttok{Tid}(#1)} -\newcommand{\bij}[2]{{#1} \bowtie {#2}} - -\newcommand{\iassert}[3]{\fbox{$#1$}{}^{#2}_{#3}} - -%\newcommand{\mown}[2]{\textsf{own}(#1, #2)} -\newcommand{\mown}[3]{\fbox{$#1$}^{#2}_{#3}} -\newcommand{\minterp}[2]{\textsf{interp}(#1) = #2} -\newcommand{\mdisable}[2]{\delta_{#1}(#2)} - -\newcommand{\TRUE}{\textlog{True}} -\newcommand{\FALSE}{\textlog{False}} -\newcommand{\emp}{\textsf{emp}} - -\newcommand{\const}{\textlog{Inv}} - -\newcommand{\infinite}{\textlog{infinite}} - -\newcommand{\tokPure}{\textlog{TokPure}} -\newcommand{\timeless}[1]{\textlog{timeless}(#1)} - -\newcommand{\physatomic}[1]{\text{$#1$ phys.\ atomic}} - -\newcommand{\unlimRely}[1]{\cdot \geqRely {#1}} - -\newcommand{\fmapsto}[1][-]{\stackrel{#1}{\mapsto}} -\newcommand{\gmapsto}{\hookrightarrow}% -\newcommand{\fgmapsto}[1][-]{\stackrel{#1}{\gmapsto}}% - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% JUDGMENTS -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -\newcommand{\wfte}[1]{{#1}\;\mbox{tyenv}} -\newcommand{\wtt}[2]{#1 : #2} -\newcommand{\wt}[3]{#1 \proves #2 : #3} -\newcommand{\wtd}[4]{#1; #2 \proves #3 : #4} - -\newcommand{\judgment}[2]{\paragraph{#1}\hspace{\stretch{1}}\fbox{$#2$}} -\newcommand{\judgmentB}[2]{\paragraph{#1}\hspace{\stretch{1}}{$#2$}} -\newcommand{\judgmentC}[2]{{\normalsize\textbf{\emph{#1}}}\hspace{\stretch{1}}{\fbox{$#2$}}} -\newcommand{\judgmentD}[2]{{\normalsize\textbf{\emph{#1}}}\quad{\fbox{$#2$}}} - -\newcommand{\isAtomic}[2]{\cfg{#1}{#2}\ \textrm{atomic}} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% MATH SYMBOLS & NOTATION -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -\newcommand{\pfn}{\rightharpoonup} -\newcommand{\fpfn}{\stackrel{\textrm{fin}}{\rightharpoonup}} -\newcommand{\ra}{\rightarrow} -\newcommand{\Ra}{\Rightarrow} -\newcommand{\Lra}{\Leftrightarrow} -\newcommand{\monra}{\stackrel{\textrm{mon}}{\rightarrow}} -%\newcommand{\res}{\upharpoonright} -\newcommand{\step}{\ra} -%\newcommand{\monora}{\stackrel{\textrm{mono}}{\longrightarrow}} -\newcommand{\monora}{\Rightarrow} - -\newcommand{\restr}[2]{\lfloor #1 \rfloor_{#2}} -% LB -\newcommand{\nequiv}[1]{\ensuremath{\mathrel{\stackrel{#1}{=}}}} -\newcommand{\notnequiv}[1]{\ensuremath{\mathrel{\stackrel{#1}{\neq}}}} -\newcommand{\nequivset}[2]{\ensuremath{\mathrel{\stackrel{#1}{=}_{#2}}}} -\newcommand{\nequivB}[1]{\ensuremath{\mathrel{\stackrel{#1}{\equiv}}}} -\newcommand{\UPred}{\textdom{UPred}} -\newcommand{\SPred}{\textdom{SPred}} -\newcommand{\latert}{\mathord{\blacktriangleright}} - -%\newcommand{\emp}{1} -% \newcommand{\lget}{\textrm{get}} -% \newcommand{\lput}{\textrm{put}} -% \newcommand{\trans}{\textrm{trans}} - -\newcommand{\lift}[1]{\lfloor {#1} \rfloor} - -\newcommand{\Sem}[1]{\llbracket #1 \rrbracket} - -\newcommand{\semSort}[1]{\Sem{#1}} -\newcommand{\semTerm}[1]{\Sem{#1}} -\newcommand{\semVCtx}[1]{\Sem{#1}} -\newcommand{\semProtSet}[1]{\Sem{#1}} -\newcommand{\semAProp}[1]{\Sem{#1}} - -%\newcommand{\semProp}[3]{#1 \models^{#2} #3} -\newcommand{\semProp}[3]{#1 \in \llbracket #3 \rrbracket^{#2}} -\newcommand{\semPropB}[2]{\llbracket #2 \rrbracket^{#1}} -\newcommand{\semPred}[2]{\llbracket{#1}\rrbracket^{#2}} - -\newcommand{\Interp}[1]{\mathcal{I}\llbracket #1 \rrbracket} -\newcommand{\Val}[1]{\llbracket #1 \rrbracket} -\newcommand{\ValB}{\mathbb{V}} -\newcommand{\LiftVal}[1]{\widehat{\mathcal{V}}\llbracket #1 \rrbracket} -\newcommand{\Exp}[1]{\mathcal{E}\llbracket #1 \rrbracket} -\newcommand{\LiftExp}[1]{\widehat{\mathcal{E}}\llbracket #1 \rrbracket} - -\newcommand{\expPred}[3]{(#1, #2) \downarrow #3} -\newcommand{\expPredPure}[3]{(#1, #2) \downarrow^{\textrm{pure}} #3} - -\newcommand{\Store}[1]{\mathcal{H}\llbracket #1 \rrbracket} -\newcommand{\Heap}[1]{\mathcal{H}\llbracket #1 \rrbracket} -\newcommand{\Env}[1]{\mathcal{G}\llbracket #1 \rrbracket} -\newcommand{\TEnv}[1]{\mathcal{D}\llbracket #1 \rrbracket} -\newcommand{\Ctx}[1]{\mathcal{K}\llbracket #1 \rrbracket} -% \newcommand{\Thread}[1]{\mathcal{T}\llbracket #1 \rrbracket} -% \newcommand{\ThreadRel}[3]{\mathcal{T}(#1,#2,#3)} -% \newcommand{\TRel}[4]{\mathcal{T}(#1,#2,#3,#4)} -% \newcommand{\TRelD}[1]{\mathcal{T}\llbracket{#1}\rrbracket} -\newcommand{\HVal}[1]{\mathcal{H}\llbracket #1 \rrbracket} -\newcommand{\Obs}[1]{\mathcal{O}(#1)} - -\newcommand{\dyn}[2]{\textlog{wp}({#1}, {#2})} -\newcommand{\adyn}[2]{{#1}\;\llparenthesis{#2}\rrparenthesis} -\newcommand{\dynpred}[2]{\textdom{wp}({#1}, {#2})} -\newcommand{\dynA}[3]{\textlog{wp}_{#3}({#1}, {#2})} -\newcommand{\pvs}[1]{\textlog{vs}({#1})} -\newcommand{\pvsA}[3]{\textlog{vs}_{#2}^{#3}({#1})} - - -% \hoaresizebox pre post -% \hoarescalebox char sizebox +%% Hoare Triples \newcommand*{\hoaresizebox}[1]{% \hbox{$\mathsurround=0pt{#1}\mathstrut$}} \newcommand*{\hoarescalebox}[2]{% @@ -576,253 +408,38 @@ \end{aligned}}% } -\newcommand{\ttrip}[4]{ - \semPropB{#1}{\rho}{\safe(#2, #3, #4)} -} -%% \newcommand{\ttrip}[4]{ -%% #1 \models^\rho -%% {#2}@{#3}\; -%% \big\{ #4 \big\} -%% } -\newcommand{\halfttrip}[3]{ - {#1}@{#2}\; - \big\{ #3 \big\} -} - -\newcommand{\rewriteSpec}{\ra_\SP} - -%\newcommand{\dyn}[2]{{#1}\;\{{#2}\}} - -\newcommand{\safe}{\textsf{safe}} - -\newcommand{\mthread}{m} -\newcommand{\absent}{\textsf{none}} - -\newcommand{\PROG}[1]{\textrm{prog}\llbracket #1 \rrbracket} -\newcommand{\PRES}[1]{\textrm{pres}\llbracket #1 \rrbracket} - -\newcommand{\pset}[1]{\wp(#1)} -\newcommand{\pmset}[1]{\wp_{m}(#1)} -\newcommand{\psetup}[1]{\wp^\uparrow(#1)} -\newcommand{\psetdown}[1]{\wp^\downarrow(#1)} -\newcommand{\fpset}[1]{\wp_{\textrm{fin}}(#1)} -\newcommand{\mset}[1]{\mathrm{bag}(#1)} -%\newcommand{\bag}[1]{\Lbag #1 \Rbag} -\newcommand{\eqdef}{\triangleq} - -\newcommand{\extendseq}{\sqsupseteq} -\newcommand{\extends}{\sqsupset} -\newcommand{\beforeeq}{\sqsubseteq} -\newcommand{\extby}{\sqsubseteq} -%\newcommand{\ntime}{\triangleright} -\newcommand{\later}{\mathord{\triangleright}} -%\newcommand{\always}[1]{\Box{#1}} -\newcommand{\always}{\Box{}} -\newcommand{\dup}[1]{\textrm{dup}({#1})} -\newcommand{\restrict}[2]{\lfloor #1 \rfloor_{#2}} - -\newcommand{\extendseqCtx}{\stackrel{\textrm{ctx}}{\sqsupseteq}} -\newcommand{\extbyCtx}{\stackrel{\textrm{ctx}}{\sqsubseteq}} - -\newcommand{\leqWT}{\sqsubseteq} -\newcommand{\geqWT}{\sqsubseteq} -\newcommand{\lubWT}{\sqcup} - -\newcommand{\leqRes}{\leq} -\newcommand{\geqRes}{\geq} - -\newcommand{\geqIS}{\sqsupseteq} - -\newcommand{\proves}{\vdash} -\newcommand{\provesalways}{\vdash_{\!\!\boxempty}} -\newcommand{\refines}{\leq} -\newcommand{\pbrk}{\mbox{\phantom{.}}} - -\newcommand{\hasHVal}[3]{#1 \Ra \textrm{hval}(#2, #3)} - - -\newcommand{\dom}{\textrm{dom}} -\newcommand{\rng}{\textrm{rng}} -\newcommand{\cod}{\textrm{cod}} - - -\newcommand{\IF}{\mathrel{\text{if}}} -\newcommand{\WHEN}{\textrm{when }} - -\newcommand{\ie}{\emph{i.e.,} } -\newcommand{\eg}{\emph{e.g.,} } -\newcommand{\etal}{\emph{et~al.}} -\newcommand{\wrt}{w.r.t.~} -\newcommand{\deadfootnote}[1]{} - -\newcommand{\idisl}[2]{{#1} \mapsto {#2}} - -%\newcommand{\region}[4] - -\newcommand{\SET}[2]{ -\left\{% -#1% -\;\middle|\;% -#2% -\right\} -} -\newcommand{\SETB}[1]{ -\left\{% -#1% -\right\} -} -\newcommand{\SETC}[2]{#1 & #2} - -\newcommand{\SPACER}{\;\;\;} - -\newcommand{\wIso}{\xi} -\newcommand{\sembox}[1]{\hfill \normalfont \mbox{\fbox{$$#1$$}}} -\newcommand{\typedsection}[2]{\subsubsection*{\rm\em #1 \sembox{#2}}} +%% Some commonly used identifiers +\newcommand{\timeless}[1]{\textlog{timeless}(#1)} +\newcommand{\physatomic}[1]{\textlog{$#1$ phys.\ atomic}} +\newcommand{\infinite}{\textlog{infinite}} -% what are we calling the manuscript? -\newcommand{\book}{book} +\newcommand{\Prop}{\textlog{Prop}} +\newcommand{\Pred}{\textlog{Pred}} -\newcommand{\aaron}[1]{{\color{red}\textbf{AT: #1}}} -\newcommand{\derek}[1]{{\color{red}\textbf{DD: #1}}} -\newcommand{\lars}[1]{{\color{red}\textbf{LB: #1}}} -\newcommand{\kasper}[1]{{\color{red}\textbf{KS: #1}}} -\newcommand{\ralf}[1]{{\color{red}\textbf{RJ: #1}}} -\newcommand{\dave}[1]{{\color{red}\textbf{PDS: #1}}} -\newcommand{\hush}[1]{} -\newcommand{\relaxguys}{% - \let\aaron\hush% - \let\derek\hush% - \let\lars\hush% - \let\kasper\hush% - \let\ralf\hush% - \let\dave\hush% -} +\newcommand{\TRUE}{\textlog{True}} +\newcommand{\FALSE}{\textlog{False}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% ATOMIC SHIFTS - -\newcommand{\funnyforall}{\boldsymbol\forall} -\newcommand{\funnyexists}{\boldsymbol\exists} - -\newcommand{\aspre}{P} -\newcommand{\asfrom}{\alpha} -\newcommand{\asto}{\beta} -\newcommand{\aspost}{Q} -%\newcommand{\asprop}{\aspost} -%\newcommand{\aspred}{\aspost} -\newcommand{\asframe}{R} -\newcommand{\asfmask}{\mask_{\asframe}} -\newcommand\nomask{\,\!}% to avoid \as defaults. It ain't empty, but it looks empty. - -% we need 10 arguments, so use some magic to get that... -\newcommand\ascore[1]{% - \def\tempflags{#1}% - \ascoreContinued% -} -\newcommand{\ascoreContinued}[9]{ - {\stretchleftright[450]{\langle}{ % - \IfSubStr{\tempflags}{l}{ \begin{inbox} }{} % - #2 - \IfSubStr{\tempflags}{b}{\vsE}{\vs} % - \IfSubStr{\tempflags}{a}{ #1.\;}{} % - #3 % - \IfSubStr{\tempflags}{x}{ \mid #4}{} % - \IfSubStr{\tempflags}{f}{ % - \mid % - \IfSubStr{\tempflags}{l}{ \\ }{} % - \IfSubStr{\tempflags}{e}{ #5.\;}{} % - #6 \vs #7 % - }{} % - \IfSubStr{\tempflags}{l}{ \end{inbox} }{} % - }{\rangle}}_{#9}^{#8} % -} -\NewDocumentCommand \as {d() m m o d() m m O{\top} O{}} - { \ascore{ % - \IfNoValueF{#1}{a} % universal quantifier - b % arrow back to start - \IfNoValueF{#4}{x} % explicit R and E - f % add forwards shift to final state - \IfNoValueF{#5}{e} % existential quantifier - }{#1}{#2}{#3}{#4}{#5}{#6}{#7}{#8}{#9} % - } -\NewDocumentCommand \asl {d() m m o d() m m O{\top} O{}} - { \ascore{ % - l % use multiple lines - \IfNoValueF{#1}{a} % universal quantifier - b % arrow back to start - \IfNoValueF{#4}{x} % explicit R and E - f % add forwards shift to final state - \IfNoValueF{#5}{e} % existential quantifier - }{#1}{#2}{#3}{#4}{#5}{#6}{#7}{#8}{#9} % - } -% \NewDocumentCommand \am {d() m m o m} -% { \ascore{ % -% \IfNoValueF{#1}{a} % universal quantifier -% b % arrow back to start -% \IfNoValueF{#4}{x} % explicit R and E -% }{#1}{#2}{#3}{#4}{#5}{}{}{} % -% } - -%%% Atomic triples - -\NewDocumentCommand \ahoare {m m m O{} O{}}{ - \triple\langle\rangle{#1}{#2}{#3}% - _{#5}^{#4}% -} - -\NewDocumentCommand \ahoareV {O{c} m m m O{} O{}}{ - {\begin{aligned}[#1] - &\anglebracket{#2} \\ - &\quad{#3} \\ - &{\anglebracket{#4}}_{#6}^{#5} - \end{aligned}}% -} - -\NewDocumentCommand \ahoareHV {O{c} m m m O{} O{}}{ - {\begin{aligned}[#1] - &\anglebracket{#2}\;\;\; {#3} \\ - &{\anglebracket{#4}}_{#6}^{#5} - \end{aligned}}% -} - +% LANGUAGE-LEVEL SYNTAX AND SEMANTICS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% hoare proof typesetting - -\newenvironment{inbox}[1][]{ - \begin{array}[#1]{@{}l@{}} -}{ - \end{array} -} - -\newcommand{\tabubox}[2][]{% - \begin{tabu}{@{#1}X[1,l,m]@{}}% - #2 % - \end{tabu}% -} -\newcommand{\hproofnospace}[1]{\noindent\parbox{\linewidth}{#1}} % -\newcommand{\hproof}[1]{\vspace{0.5em}\hproofnospace{#1}\vspace{0.5em}} % -\newcommand\psub[2]{% - \begin{tabu}{ m{0.9em} | X[1,l,m] }% - \begin{sideways}#1\end{sideways} &% - \tabubox{#2}% - \end{tabu}% -}% +\newcommand{\expr}{e} +\newcommand{\val}{v} +\newcommand{\valB}{w} +\newcommand{\state}{\sigma} +\newcommand{\step}{\ra} -\newcommand\pind[1]{\tabubox[\hspace{1em}]{#1}} -\newcommand{\pline}[2][\empty]{\ensuremath{\left\{{#2\mathstrut}\right\}_{#1}}} -\newcommand{\pmline}[2][\empty]{\ensuremath{\left\{\begin{inbox}#2\end{inbox}\right\}_{#1}}} -\newcommand{\aline}[2][\empty]{\ensuremath{{\stretchleftright[450]{\langle}{#2\mathstrut}{\rangle}}_{#1}}} -\newcommand{\amline}[2][\empty]{\ensuremath{{\stretchleftright[450]{\langle}{\begin{inbox}#2\end{inbox}}{\rangle}}_{#1}}} -\definecolor{code_color}{rgb}{0, 0, 0.6} -\newcommand{\cdline}[1]{\ensuremath{\color{code_color}#1}} +\newcommand{\ectx}{K} +\newcommand{\tpool}{T} -\definecolor{interp_p_backgr}{rgb}{0.8, 0.8, 1.0} -\definecolor{interp_q_backgr}{rgb}{0.8, 1.0, 0.8} +\newcommand{\cfg}[2]{{#1};{#2}} +\newcommand{\fork}[1]{\textlang{fork}\;{#1}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% Monoid and other constructions +% DERIVED CONSTRUCTIONS +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% Commonly used identifiers \newcommand{\FHeap}{\textsc{FHeap}} \newcommand{\AFHeap}{\textsc{AFHeap}} @@ -835,9 +452,6 @@ \newcommand{\exm}[1]{\ensuremath{\textsc{Ex}(#1)}} \newcommand{\agm}[1]{\ensuremath{\textsc{Ag}(#1)}} -%\newcommand{\dispm}[1]{\ensuremath{\textsc{Disp}(#1)}} -%\newcommand{\disposed}{\mathord{\dagger}} - \newcommand{\STSMon}[1]{\textsc{Sts}_{#1}} \newcommand{\STSInv}{\textsf{STSInv}}