diff --git a/docs/base-logic.tex b/docs/base-logic.tex index 93c0f58facf2107c768409563a5f75f017d237ce..6a4639c725135b63e0223ed5f03c5089c4a3d852 100644 --- a/docs/base-logic.tex +++ b/docs/base-logic.tex @@ -63,12 +63,13 @@ Below, $\melt$ ranges over $\monoid$ and $i$ ranges over $\set{1,2}$. %\\& \ownM{\term} \mid \mval(\term) \mid \always\prop \mid + \plainly\prop \mid {\later\prop} \mid \upd \prop \end{align*} Recursive predicates must be \emph{guarded}: in $\MU \var. \term$, the variable $\var$ can only appear under the later $\later$ modality. -Note that the modalities $\upd$, $\always$ and $\later$ bind more tightly than $*$, $\wand$, $\land$, $\lor$, and $\Ra$. +Note that the modalities $\upd$, $\always$, $\plainly$ and $\later$ bind more tightly than $*$, $\wand$, $\land$, $\lor$, and $\Ra$. \paragraph{Variable conventions.} @@ -175,6 +176,9 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in \$ \and \infer{\vctx \proves \wtt{\prop}{\Prop}} {\vctx \proves \wtt{\always\prop}{\Prop}} +\and + \infer{\vctx \proves \wtt{\prop}{\Prop}} + {\vctx \proves \wtt{\plainly\prop}{\Prop}} \and \infer{\vctx \proves \wtt{\prop}{\Prop}} {\vctx \proves \wtt{\later\prop}{\Prop}} diff --git a/docs/iris.sty b/docs/iris.sty index aefb06027655b6d93f6be21c6fd354bcb02ab0b4..9ba0f619ee6025bb86dd090ac8e161017be62f73 100644 --- a/docs/iris.sty +++ b/docs/iris.sty @@ -260,6 +260,7 @@ \newcommand{\later}{\mathop{{\triangleright}}} \newcommand*{\lateropt}[1]{\mathop{{\later}^{#1}}} \newcommand{\always}{\mathop{\Box}} +\newcommand{\plainly}{\mathop{\blacksquare}} %% Invariants and Ghost ownership % PDS: Was 0pt inner, 2pt outer. diff --git a/docs/model.tex b/docs/model.tex index 4ea588ae82bffaf573ab6ea9777a34843d9a98fd..af3ed1e4fd53c6eb62d3d2e139e68589bc12669b 100644 --- a/docs/model.tex +++ b/docs/model.tex @@ -54,10 +54,11 @@ We are thus going to define the assertions as mapping CMRA elements to sets of s \Lam \melt. \setComp{n}{\begin{aligned} \All m, \meltB.& m \leq n \land \melt\mtimes\meltB \in \mval_m \Ra {} \\ & m \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\meltB) \Ra {}\\& m \in \Sem{\vctx \proves \propB : \Prop}_\gamma(\melt\mtimes\meltB)\end{aligned}} \\ - \Sem{\vctx \proves \always{\prop} : \Prop}_\gamma &\eqdef \Lam\melt. \Sem{\vctx \proves \prop : \Prop}_\gamma(\mcore\melt) \\ - \Sem{\vctx \proves \later{\prop} : \Prop}_\gamma &\eqdef \Lam\melt. \setComp{n}{n = 0 \lor n-1 \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\melt)}\\ \Sem{\vctx \proves \ownM{\term} : \Prop}_\gamma &\eqdef \Lam\meltB. \setComp{n}{\Sem{\vctx \proves \term : \textlog{M}}_\gamma \mincl[n] \meltB} \\ \Sem{\vctx \proves \mval(\term) : \Prop}_\gamma &\eqdef \Lam\any. \setComp{n}{\Sem{\vctx \proves \term : \textlog{M}}_\gamma \in \mval_n} \\ + \Sem{\vctx \proves \always{\prop} : \Prop}_\gamma &\eqdef \Lam\melt. \Sem{\vctx \proves \prop : \Prop}_\gamma(\mcore\melt) \\ + \Sem{\vctx \proves \plainly{\prop} : \Prop}_\gamma &\eqdef \Lam\melt. \Sem{\vctx \proves \prop : \Prop}_\gamma(\munit) \\ + \Sem{\vctx \proves \later{\prop} : \Prop}_\gamma &\eqdef \Lam\melt. \setComp{n}{n = 0 \lor n-1 \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\melt)}\\ \Sem{\vctx \proves \upd\prop : \Prop}_\gamma &\eqdef \Lam\melt. \setComp{n}{\begin{aligned} \All m, \melt'. & m \leq n \land (\melt \mtimes \melt') \in \mval_m \Ra {}\\& \Exists \meltB. (\meltB \mtimes \melt') \in \mval_m \land m \in \Sem{\vctx \proves \prop :\Prop}_\gamma(\meltB) \end{aligned}