logic.tex 23.3 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
\section{Language}
2

Ralf Jung's avatar
Ralf Jung committed
3
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
4
\begin{itemize}
Ralf Jung's avatar
Ralf Jung committed
5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24
\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} 
\end{mathpar}
\item There exists a \emph{primitive reduction relation} \[(-,- \step -,-,-) \subseteq \textdom{Expr} \times \textdom{State} \times \textdom{Expr} \times \textdom{State} \times (\textdom{Expr} \uplus \set{()})\]
  We will write $\expr_1, \state_1 \step \expr_2, \state_2$ for $\expr_1, \state_1 \step \expr_2, \state_2, ()$. \\
  A reduction $\expr_1, \state_1 \step \expr_2, \state_2, \expr'$ indicates that, when $\expr_1$ reduces to $\expr$, a \emph{new thread} $\expr'$ is forked off.
\item All values are stuck:
\[ \expr, \_ \step  \_, \_, \_ \Ra \toval(\expr) = \bot \]
\item There is a predicate defining \emph{atomic} expressions satisfying
\let\oldcr\cr
\begin{mathpar}
  {\All\expr. \atomic(\expr) \Ra \toval(\expr) = \bot} \and
  {{
    \begin{inbox}
\All\expr_1, \state_1, \expr_2, \state_2, \expr'. \atomic(\expr_1) \land \expr_1, \state_1 \step \expr_2, \state_2, \expr' \Ra {}\\\qquad\qquad\qquad\quad~~ \Exists \val_2. \toval(\expr_2) = \val_2
    \end{inbox}
}}
\end{mathpar}
In other words, atomic expression \emph{reduce in one step to a value}.
It does not matter whether they fork off an arbitrary expression.
25 26
\end{itemize}

Ralf Jung's avatar
Ralf Jung committed
27 28 29 30 31 32 33 34 35
\begin{defn}[Context]
  A function $\lctx : \textdom{Expr} \to \textdom{Expr}$ is a \emph{context} if the following conditions are satisfied
  \begin{align*}
  \All\expr.& \toval(\expr) = \bot \Ra \toval(\lctx(\expr)) = \bot \tagH{lang-ctx-not-val}\\
  \All \expr_1, \state_1, \expr_2, \state_2, \expr'.& \expr_1, \state_1 \step \expr_2,\state_2,\expr' \Ra \lctx(\expr_1), \state_1 \step \lctx(\expr_2),\state_2,\expr' \tagH{lang-ctx-step}\\
  \All \expr_1', \state_1, \expr_2, \state_2, \expr'.& \toval(\expr_1') = \bot \land \lctx(\expr_1'), \state_1 \step \expr_2,\state_2,\expr' \Ra \Exists\expr_2'. \expr_2 = \lctx(\expr_2') \land \expr_1', \state_1 \step \expr_2',\state_2,\expr' \tagH{lang-ctx-step-inv}
  \end{align*}
\end{defn}

Ralf Jung's avatar
Ralf Jung committed
36 37 38
\subsection{The concurrent language}

For any language $\Lang$, we define the corresponding thread-pool semantics.
39 40 41

\paragraph{Machine syntax}
\[
Ralf Jung's avatar
Ralf Jung committed
42
	\tpool \in \textdom{ThreadPool} \eqdef \bigcup_n \textdom{Exp}^n
43 44
\]

Ralf Jung's avatar
Ralf Jung committed
45 46
\judgment{Machine reduction} {\cfg{\tpool}{\state} \step
  \cfg{\tpool'}{\state'}}
47 48
\begin{mathpar}
\infer
Ralf Jung's avatar
Ralf Jung committed
49 50 51 52 53 54 55
  {\expr_1, \state_1 \step \expr_2, \state_2, \expr' \and \expr' \neq ()}
  {\cfg{\tpool \dplus [\expr_1] \dplus \tpool'}{\state} \step
     \cfg{\tpool \dplus [\expr_2] \dplus \tpool' \dplus [\expr']}{\state'}}
\and\infer
  {\expr_1, \state_1 \step \expr_2, \state_2}
  {\cfg{\tpool \dplus [\expr_1] \dplus \tpool'}{\state} \step
     \cfg{\tpool \dplus [\expr_2] \dplus \tpool'}{\state'}}
56 57
\end{mathpar}

58
\clearpage
Ralf Jung's avatar
Ralf Jung committed
59 60 61 62 63 64 65
\section{The logic}

To instantiate Iris, you need to define the following parameters:
\begin{itemize}
\item A language $\Lang$
\item A locally contractive functor $\iFunc : \COFEs \to \CMRAs$ defining the ghost state
\end{itemize}
66

Ralf Jung's avatar
Ralf Jung committed
67 68 69
\noindent
As usual for higher-order logics, you can furthermore pick a \emph{signature} $\Sig = (\SigType, \SigFn, \SigAx)$ to add more types, symbols and axioms to the language.
You have to make sure that $\SigType$ includes the base types:
70
\[
Ralf Jung's avatar
Ralf Jung committed
71
	\SigType \supseteq \{ \textsort{Val}, \textsort{Expr}, \textsort{State}, \textsort{M}, \textsort{InvName}, \textsort{InvMask}, \Prop \}
72
\]
Ralf Jung's avatar
Ralf Jung committed
73 74 75
Elements of $\SigType$ are ranged over by $\sigtype$.

Each function symbol in $\SigFn$ has an associated \emph{arity} comprising a natural number $n$ and an ordered list of $n+1$ types $\type$ (the grammar of $\type$ is defined below, and depends only on $\SigType$).
76 77 78 79 80
We write
\[
	\sigfn : \type_1, \dots, \type_n \to \type_{n+1} \in \SigFn
\]
to express that $\sigfn$ is a function symbol with the indicated arity.
Ralf Jung's avatar
Ralf Jung committed
81 82 83 84 85 86

Furthermore, $\SigAx$ is a set of \emph{axioms}, that is, terms $\term$ of type $\Prop$.
Again, the grammar of terms and their typing rules are defined below, and depends only on $\SigType$ and $\SigFn$, not on $\SigAx$.
Elements of $\SigAx$ are ranged over by $\sigax$.

\subsection{Grammar}\label{sec:grammar}
87 88

\paragraph{Syntax.}
Ralf Jung's avatar
Ralf Jung committed
89
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$):
90

91
\begin{align*}
Ralf Jung's avatar
Ralf Jung committed
92 93 94 95 96 97
  \type ::={}&
      \sigtype \mid
      \unitsort \mid
      \type \times \type \mid
      \type \to \type
\\[0.4em]
98
  \term, \prop, \pred ::={}&
99
      \var \mid
100
      \sigfn(\term_1, \dots, \term_n) \mid
101
      \unitval \mid
102 103
      (\term, \term) \mid
      \pi_i\; \term \mid
104
      \Lam \var:\type.\term \mid
Ralf Jung's avatar
Ralf Jung committed
105
      \term(\term)  \mid
106 107 108 109 110
      \munit \mid
      \term \mtimes \term \mid
\\&
    \FALSE \mid
    \TRUE \mid
Ralf Jung's avatar
Ralf Jung committed
111
    \term =_\type \term \mid
112 113 114 115 116 117
    \prop \Ra \prop \mid
    \prop \land \prop \mid
    \prop \lor \prop \mid
    \prop * \prop \mid
    \prop \wand \prop \mid
\\&
118
    \MU \var:\type. \pred  \mid
Ralf Jung's avatar
Ralf Jung committed
119 120
    \Exists \var:\type. \prop \mid
    \All \var:\type. \prop \mid
121 122 123 124 125 126
\\&
    \knowInv{\term}{\prop} \mid
    \ownGGhost{\term} \mid
    \ownPhys{\term} \mid
    \always\prop \mid
    {\later\prop} \mid
Ralf Jung's avatar
Ralf Jung committed
127
    \pvs[\term][\term] \prop\mid
Ralf Jung's avatar
Ralf Jung committed
128
    \wpre{\term}{\Ret\var.\term}[\term]
129
\end{align*}
Ralf Jung's avatar
Ralf Jung committed
130
Recursive predicates must be \emph{guarded}: in $\MU \var. \pred$, the variable $\var$ can only appear under the later $\later$ modality.
131

132
Note that $\always$ and $\later$ bind more tightly than $*$, $\wand$, $\land$, $\lor$, and $\Ra$.
Ralf Jung's avatar
Ralf Jung committed
133
We will write $\pvs[\term] \prop$ for $\pvs[\term][\term] \prop$.
134

135
\paragraph{Metavariable conventions.}
Ralf Jung's avatar
Ralf Jung committed
136
We introduce additional metavariables ranging over terms and generally let the choice of metavariable indicate the term's type:
137 138
\[
\begin{array}{r|l}
Ralf Jung's avatar
Ralf Jung committed
139
 \text{metavariable} & \text{type} \\\hline
140 141
  \term, \termB & \text{arbitrary} \\
  \val, \valB & \textsort{Val} \\
Ralf Jung's avatar
Ralf Jung committed
142
  \expr & \textsort{Expr} \\
143 144 145 146
  \state & \textsort{State} \\
\end{array}
\qquad\qquad
\begin{array}{r|l}
Ralf Jung's avatar
Ralf Jung committed
147
 \text{metavariable} & \text{type} \\\hline
148 149
  \iname & \textsort{InvName} \\
  \mask & \textsort{InvMask} \\
Ralf Jung's avatar
Ralf Jung committed
150
  \melt, \meltB & \textsort{M} \\
151
  \prop, \propB, \propC & \Prop \\
Ralf Jung's avatar
Ralf Jung committed
152
  \pred, \predB, \predC & \type\to\Prop \text{ (when $\type$ is clear from context)} \\
153 154 155 156
\end{array}
\]

\paragraph{Variable conventions.}
157
We often abuse notation, using the preceding \emph{term} meta-variables to range over (bound) \emph{variables}.
158
We omit type annotations in binders, when the type is clear from context.
Ralf Jung's avatar
Ralf Jung committed
159
We assume that, if a term occurs multiple times in a rule, its free variables are exactly those binders which are available at every occurrence.
160 161 162 163 164


\subsection{Types}\label{sec:types}

Iris terms are simply-typed.
Ralf Jung's avatar
Ralf Jung committed
165
The judgment $\vctx \proves \wtt{\term}{\type}$ expresses that, in variable context $\vctx$, the term $\term$ has type $\type$.
166

Ralf Jung's avatar
Ralf Jung committed
167 168
A variable context, $\vctx = x_1:\type_1, \dots, x_n:\type_n$, declares a list of variables and their types.
In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $\vctx$.
169

Ralf Jung's avatar
Ralf Jung committed
170
\judgment{Well-typed terms}{\vctx \proves_\Sig \wtt{\term}{\type}}
171 172
\begin{mathparpagebreakable}
%%% variables and function symbols
Ralf Jung's avatar
Ralf Jung committed
173
	\axiom{x : \type \proves \wtt{x}{\type}}
174
\and
Ralf Jung's avatar
Ralf Jung committed
175 176
	\infer{\vctx \proves \wtt{\term}{\type}}
		{\vctx, x:\type' \proves \wtt{\term}{\type}}
177
\and
Ralf Jung's avatar
Ralf Jung committed
178 179
	\infer{\vctx, x:\type', y:\type' \proves \wtt{\term}{\type}}
		{\vctx, x:\type' \proves \wtt{\term[x/y]}{\type}}
180
\and
Ralf Jung's avatar
Ralf Jung committed
181 182
	\infer{\vctx_1, x:\type', y:\type'', \vctx_2 \proves \wtt{\term}{\type}}
		{\vctx_1, x:\type'', y:\type', \vctx_2 \proves \wtt{\term[y/x,x/y]}{\type}}
183 184 185 186 187 188 189 190 191 192 193
\and
	\infer{
		\vctx \proves \wtt{\term_1}{\type_1} \and
		\cdots \and
		\vctx \proves \wtt{\term_n}{\type_n} \and
		\sigfn : \type_1, \dots, \type_n \to \type_{n+1} \in \SigFn
	}{
		\vctx \proves \wtt {\sigfn(\term_1, \dots, \term_n)} {\type_{n+1}}
	}
%%% products
\and
194
	\axiom{\vctx \proves \wtt{\unitval}{\unitsort}}
195
\and
Ralf Jung's avatar
Ralf Jung committed
196 197
	\infer{\vctx \proves \wtt{\term}{\type_1} \and \vctx \proves \wtt{\termB}{\type_2}}
		{\vctx \proves \wtt{(\term,\termB)}{\type_1 \times \type_2}}
198
\and
Ralf Jung's avatar
Ralf Jung committed
199 200
	\infer{\vctx \proves \wtt{\term}{\type_1 \times \type_2} \and i \in \{1, 2\}}
		{\vctx \proves \wtt{\pi_i\,\term}{\type_i}}
201 202
%%% functions
\and
Ralf Jung's avatar
Ralf Jung committed
203 204
	\infer{\vctx, x:\type \proves \wtt{\term}{\type'}}
		{\vctx \proves \wtt{\Lam x. \term}{\type \to \type'}}
205 206
\and
	\infer
Ralf Jung's avatar
Ralf Jung committed
207 208
	{\vctx \proves \wtt{\term}{\type \to \type'} \and \wtt{\termB}{\type}}
	{\vctx \proves \wtt{\term(\termB)}{\type'}}
209 210
%%% monoids
\and
211
	\infer{}{\vctx \proves \wtt{\munit}{\textsort{M} \to \textsort{M}}}
212
\and
Ralf Jung's avatar
Ralf Jung committed
213 214
	\infer{\vctx \proves \wtt{\melt}{\textsort{M}} \and \vctx \proves \wtt{\meltB}{\textsort{M}}}
		{\vctx \proves \wtt{\melt \mtimes \meltB}{\textsort{M}}}
215 216 217 218 219 220
%%% props and predicates
\\
	\axiom{\vctx \proves \wtt{\FALSE}{\Prop}}
\and
	\axiom{\vctx \proves \wtt{\TRUE}{\Prop}}
\and
Ralf Jung's avatar
Ralf Jung committed
221 222
	\infer{\vctx \proves \wtt{\term}{\type} \and \vctx \proves \wtt{\termB}{\type}}
		{\vctx \proves \wtt{\term =_\type \termB}{\Prop}}
223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239
\and
	\infer{\vctx \proves \wtt{\prop}{\Prop} \and \vctx \proves \wtt{\propB}{\Prop}}
		{\vctx \proves \wtt{\prop \Ra \propB}{\Prop}}
\and
	\infer{\vctx \proves \wtt{\prop}{\Prop} \and \vctx \proves \wtt{\propB}{\Prop}}
		{\vctx \proves \wtt{\prop \land \propB}{\Prop}}
\and
	\infer{\vctx \proves \wtt{\prop}{\Prop} \and \vctx \proves \wtt{\propB}{\Prop}}
		{\vctx \proves \wtt{\prop \lor \propB}{\Prop}}
\and
	\infer{\vctx \proves \wtt{\prop}{\Prop} \and \vctx \proves \wtt{\propB}{\Prop}}
		{\vctx \proves \wtt{\prop * \propB}{\Prop}}
\and
	\infer{\vctx \proves \wtt{\prop}{\Prop} \and \vctx \proves \wtt{\propB}{\Prop}}
		{\vctx \proves \wtt{\prop \wand \propB}{\Prop}}
\and
	\infer{
240 241
		\vctx, \var:\type \proves \wtt{\term}{\type} \and
		\text{$\var$ is guarded in $\term$}
242
	}{
243
		\vctx \proves \wtt{\MU \var:\type. \term}{\type}
244 245
	}
\and
Ralf Jung's avatar
Ralf Jung committed
246 247
	\infer{\vctx, x:\type \proves \wtt{\prop}{\Prop}}
		{\vctx \proves \wtt{\Exists x:\type. \prop}{\Prop}}
248
\and
Ralf Jung's avatar
Ralf Jung committed
249 250
	\infer{\vctx, x:\type \proves \wtt{\prop}{\Prop}}
		{\vctx \proves \wtt{\All x:\type. \prop}{\Prop}}
251 252 253 254 255 256 257 258
\and
	\infer{
		\vctx \proves \wtt{\prop}{\Prop} \and
		\vctx \proves \wtt{\iname}{\textsort{InvName}}
	}{
		\vctx \proves \wtt{\knowInv{\iname}{\prop}}{\Prop}
	}
\and
Ralf Jung's avatar
Ralf Jung committed
259
	\infer{\vctx \proves \wtt{\melt}{\textsort{M}}}
260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275
		{\vctx \proves \wtt{\ownGGhost{\melt}}{\Prop}}
\and
	\infer{\vctx \proves \wtt{\state}{\textsort{State}}}
		{\vctx \proves \wtt{\ownPhys{\state}}{\Prop}}
\and
	\infer{\vctx \proves \wtt{\prop}{\Prop}}
		{\vctx \proves \wtt{\always\prop}{\Prop}}
\and
	\infer{\vctx \proves \wtt{\prop}{\Prop}}
		{\vctx \proves \wtt{\later\prop}{\Prop}}
\and
	\infer{
		\vctx \proves \wtt{\prop}{\Prop} \and
		\vctx \proves \wtt{\mask}{\textsort{InvMask}} \and
		\vctx \proves \wtt{\mask'}{\textsort{InvMask}}
	}{
Ralf Jung's avatar
Ralf Jung committed
276
		\vctx \proves \wtt{\pvs[\mask][\mask'] \prop}{\Prop}
277 278 279
	}
\and
	\infer{
Ralf Jung's avatar
Ralf Jung committed
280 281
		\vctx \proves \wtt{\expr}{\textsort{Expr}} \and
		\vctx,\var:\textsort{Val} \proves \wtt{\term}{\Prop} \and
282 283
		\vctx \proves \wtt{\mask}{\textsort{InvMask}}
	}{
Ralf Jung's avatar
Ralf Jung committed
284
		\vctx \proves \wtt{\wpre{\expr}{\Ret\var.\term}[\mask]}{\Prop}
285 286 287
	}
\end{mathparpagebreakable}

Ralf Jung's avatar
Ralf Jung committed
288
\subsection{Timeless propositions}
Ralf Jung's avatar
Ralf Jung committed
289 290 291

Some propositions are \emph{timeless}, which intuitively means that step-indexing does not affect them.
This is a \emph{meta-level} assertions about propositions, defined by the following judgment.
292

Ralf Jung's avatar
Ralf Jung committed
293
\judgment{Timeless Propositions}{\timeless{P}}
294

Ralf Jung's avatar
Ralf Jung committed
295 296
\ralf{Define a judgment that defines them.}

Ralf Jung's avatar
Ralf Jung committed
297
\subsection{Proof rules}
Ralf Jung's avatar
Ralf Jung committed
298

299 300
The judgment $\vctx \mid \pfctx \proves \prop$ says that with free variables $\vctx$, proposition $\prop$ holds whenever all assumptions $\pfctx$ hold.
We implicitly assume that an arbitrary variable context, $\vctx$, is added to every constituent of the rules.
Ralf Jung's avatar
Ralf Jung committed
301
Furthermore, an arbitrary \emph{boxed} assertion context $\always\pfctx$ may be added to every constituent.
302 303 304
Axioms $\prop \Ra \propB$ stand for judgments $\vctx \mid \cdot \proves \prop \Ra \propB$ with no assumptions.
(Bi-implications are analogous.)

305
\judgment{}{\vctx \mid \pfctx \proves \prop}
Ralf Jung's avatar
Ralf Jung committed
306
\paragraph{Laws of intuitionistic higher-order logic.}
307
This is entirely standard.
308 309
\begin{mathparpagebreakable}
\infer[Asm]
310 311 312
  {\prop \in \pfctx}
  {\pfctx \proves \prop}
\and
313
\infer[Eq]
314 315
  {\pfctx \proves \prop \\ \pfctx \proves \term =_\type \term'}
  {\pfctx \proves \prop[\term'/\term]}
316
\and
317 318 319 320 321 322 323 324 325 326 327 328
\infer[Refl]
  {}
  {\pfctx \proves \term =_\type \term}
\and
\infer[$\bot$E]
  {\pfctx \proves \FALSE}
  {\pfctx \proves \prop}
\and
\infer[$\top$I]
  {}
  {\pfctx \proves \TRUE}
\and
329
\infer[$\wedge$I]
330 331 332
  {\pfctx \proves \prop \\ \pfctx \proves \propB}
  {\pfctx \proves \prop \wedge \propB}
\and
333
\infer[$\wedge$EL]
334 335 336
  {\pfctx \proves \prop \wedge \propB}
  {\pfctx \proves \prop}
\and
337
\infer[$\wedge$ER]
338 339 340
  {\pfctx \proves \prop \wedge \propB}
  {\pfctx \proves \propB}
\and
341
\infer[$\vee$IL]
342 343 344
  {\pfctx \proves \prop }
  {\pfctx \proves \prop \vee \propB}
\and
345
\infer[$\vee$IR]
346 347 348
  {\pfctx \proves \propB}
  {\pfctx \proves \prop \vee \propB}
\and
349 350 351 352 353 354
\infer[$\vee$E]
  {\pfctx \proves \prop \vee \propB \\
   \pfctx, \prop \proves \propC \\
   \pfctx, \propB \proves \propC}
  {\pfctx \proves \propC}
\and
355
\infer[$\Ra$I]
356 357 358
  {\pfctx, \prop \proves \propB}
  {\pfctx \proves \prop \Ra \propB}
\and
359
\infer[$\Ra$E]
360 361 362
  {\pfctx \proves \prop \Ra \propB \\ \pfctx \proves \prop}
  {\pfctx \proves \propB}
\and
363 364 365
\infer[$\forall$I]
  { \vctx,\var : \type\mid\pfctx \proves \prop}
  {\vctx\mid\pfctx \proves \forall \var: \type.\; \prop}
366
\and
367 368 369 370
\infer[$\forall$E]
  {\vctx\mid\pfctx \proves \forall \var :\type.\; \prop \\
   \vctx \proves \wtt\term\type}
  {\vctx\mid\pfctx \proves \prop[\term/\var]}
371
\and
372 373 374 375
\infer[$\exists$I]
  {\vctx\mid\pfctx \proves \prop[\term/\var] \\
   \vctx \proves \wtt\term\type}
  {\vctx\mid\pfctx \proves \exists \var: \type. \prop}
376
\and
377 378 379 380
\infer[$\exists$E]
  {\vctx\mid\pfctx \proves \exists \var: \type.\; \prop \\
   \vctx,\var : \type\mid\pfctx , \prop \proves \propB}
  {\vctx\mid\pfctx \proves \propB}
381
\and
382 383 384
\infer[$\lambda$]
  {}
  {\pfctx \proves (\Lam\var: \type. \prop)(\term) =_{\type\to\type'} \prop[\term/\var]}
385
\and
386 387 388 389
\infer[$\mu$]
  {}
  {\pfctx \proves \mu\var: \type. \prop =_{\type} \prop[\mu\var: \type. \prop/\var]}
\end{mathparpagebreakable}
390

Ralf Jung's avatar
Ralf Jung committed
391
\paragraph{Laws of (affine) bunched implications.}
392 393
\begin{mathpar}
\begin{array}{rMcMl}
394
  \TRUE * \prop &\Lra& \prop \\
395
  \prop * \propB &\Lra& \propB * \prop \\
396
  (\prop * \propB) * \propC &\Lra& \prop * (\propB * \propC)
397 398
\end{array}
\and
399
\infer[$*$-mono]
400 401 402
  {\prop_1 \proves \propB_1 \and
   \prop_2 \proves \propB_2}
  {\prop_1 * \prop_2 \proves \propB_1 * \propB_2}
403
\and
404
\inferB[$\wand$I-E]
405 406
  {\prop * \propB \proves \propC}
  {\prop \proves \propB \wand \propC}
407 408
\end{mathpar}

Ralf Jung's avatar
Ralf Jung committed
409
\paragraph{Laws for ghosts and physical resources.}
410 411 412
\begin{mathpar}
\begin{array}{rMcMl}
\ownGGhost{\melt} * \ownGGhost{\meltB} &\Lra&  \ownGGhost{\melt \mtimes \meltB} \\
413 414
%\TRUE &\Ra&  \ownGGhost{\munit}\\
\ownGGhost{\melt} &\Ra& \melt \in \mval % * \ownGGhost{\melt}
415 416 417
\end{array}
\and
\begin{array}{c}
418
\ownPhys{\state} * \ownPhys{\state'} \Ra \FALSE
419 420 421
\end{array}
\end{mathpar}

Ralf Jung's avatar
Ralf Jung committed
422
\paragraph{Laws for the later modality.}
423
\begin{mathpar}
424
\infer[$\later$-mono]
425 426 427
  {\pfctx \proves \prop}
  {\pfctx \proves \later{\prop}}
\and
428 429 430
\infer[L{\"o}b]
  {}
  {(\later\prop\Ra\prop) \proves \prop}
431
\and
432 433 434 435 436
\infer[$\later$-$\exists$]
  {\text{$\type$ is inhabited}}
  {\later{\Exists x:\type.\prop} \proves \Exists x:\type. \later\prop}
\\\\
\begin{array}[c]{rMcMl}
437 438 439 440
  \later{(\prop \wedge \propB)} &\Lra& \later{\prop} \wedge \later{\propB}  \\
  \later{(\prop \vee \propB)} &\Lra& \later{\prop} \vee \later{\propB} \\
\end{array}
\and
441
\begin{array}[c]{rMcMl}
442
  \later{\All x.\prop} &\Lra& \All x. \later\prop \\
443
  \Exists x. \later\prop &\Ra& \later{\Exists x.\prop}  \\
444 445 446 447
  \later{(\prop * \propB)} &\Lra& \later\prop * \later\propB
\end{array}
\end{mathpar}

Ralf Jung's avatar
Ralf Jung committed
448
\paragraph{Laws for the always modality.}
449
\begin{mathpar}
450
\infer[$\always$I]
451 452 453
  {\always{\pfctx} \proves \prop}
  {\always{\pfctx} \proves \always{\prop}}
\and
454 455 456 457 458 459 460
\infer[$\always$E]{}
  {\always{\prop} \Ra \prop}
\and
\begin{array}[c]{rMcMl}
  \always{(\prop * \propB)} &\Ra& \always{(\prop \land \propB)} \\
  \always{\prop} * \propB &\Ra& \always{\prop} \land \propB \\
  \always{\later\prop} &\Lra& \later\always{\prop} \\
461 462
\end{array}
\and
463
\begin{array}[c]{rMcMl}
464 465 466 467 468
  \always{(\prop \land \propB)} &\Lra& \always{\prop} \land \always{\propB} \\
  \always{(\prop \lor \propB)} &\Lra& \always{\prop} \lor \always{\propB} \\
  \always{\All x. \prop} &\Lra& \All x. \always{\prop} \\
  \always{\Exists x. \prop} &\Lra& \Exists x. \always{\prop} \\
\end{array}
Ralf Jung's avatar
Ralf Jung committed
469 470 471 472 473 474
\and
{ \term =_\type \term' \Ra \always \term =_\type \term'}
\and
{ \knowInv\iname\prop \Ra \always \knowInv\iname\prop}
\and
{ \ownGGhost{\munit(\melt)} \Ra \always \ownGGhost{\munit(\melt)}}
475 476
\end{mathpar}

Ralf Jung's avatar
Ralf Jung committed
477
\paragraph{Laws of primitive view shifts.}
Ralf Jung's avatar
Ralf Jung committed
478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513
\begin{mathpar}
\infer[pvs-intro]
{}{\prop \proves \pvs[\mask] \prop}

\infer[pvs-mono]
{\prop \proves \propB}
{\pvs[\mask_1][\mask_2] \prop \proves \pvs[\mask_1][\mask_2] \propB}

\infer[pvs-timeless]
{\timeless\prop}
{\later\prop \proves \pvs[\mask] \prop}

\infer[pvs-trans]
{\mask_2 \subseteq \mask_1 \cup \mask_3}
{\pvs[\mask_1][\mask_2] \pvs[\mask_2][\mask_3] \prop \proves \pvs[\mask_1][\mask_3] \prop}

\infer[pvs-mask-frame]
{}{\pvs[\mask_1][\mask_2] \prop \proves \pvs[\mask_1 \uplus \mask_f][\mask_2 \uplus \mask_f] \prop}

\infer[pvs-frame]
{}{\propB * \pvs[\mask_1][\mask_2]\prop \proves \pvs[\mask_1][\mask_2] \propB * \prop}

\infer[pvs-allocI]
{\text{$\mask$ is infinite}}
{\later\prop \proves \pvs[\mask] \Exists \iname \in \mask. \knowInv\iname\prop}

\infer[pvs-openI]
{}{\knowInv\iname\prop \proves \pvs[\set\iname][\emptyset] \later\prop}

\infer[pvs-closeI]
{}{\knowInv\iname\prop \land \later\prop \proves \pvs[\emptyset][\set\iname] \TRUE}

\infer[pvs-update]
{\melt \mupd \meltsB}
{\ownGGhost\melt \proves \pvs[\mask] \Exists\meltB\in\meltsB. \ownGGhost\meltB}
\end{mathpar}
514

Ralf Jung's avatar
Ralf Jung committed
515
\paragraph{Laws of weakest preconditions.}
Ralf Jung's avatar
Ralf Jung committed
516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545
\begin{mathpar}
\infer[wp-value]
{}{\prop[\val/\var] \proves \wpre{\val}{\Ret\var.\prop}[\mask]}

\infer[wp-mono]
{\mask_1 \subseteq \mask_2 \and \var:\textsort{val}\mid\prop \proves \propB}
{\wpre\expr{\Ret\var.\prop}[\mask_1] \proves \wpre\expr{\Ret\var.\propB}[\mask_2]}

\infer[pvs-wp]
{}{\pvs[\mask] \wpre\expr{\Ret\var.\prop}[\mask] \proves \wpre\expr{\Ret\var.\prop}[\mask]}

\infer[wp-pvs]
{}{\wpre\expr{\Ret\var.\pvs[\mask] \prop}[\mask] \proves \wpre\expr{\Ret\var.\prop}[\mask]}

\infer[wp-atomic]
{\mask_2 \subseteq \mask_1 \and \physatomic{\expr}}
{\pvs[\mask_1][\mask_2] \wpre\expr{\Ret\var. \pvs[\mask_2][\mask_1]\prop}[\mask_2]
 \proves \wpre\expr{\Ret\var.\prop}[\mask_1]}

\infer[wp-frame]
{}{\propB * \wpre\expr{\Ret\var.\prop}[\mask] \proves \wpre\expr{\Ret\var.\propB*\prop}[\mask]}

\infer[wp-frame-step]
{\toval(\expr) = \bot}
{\later\propB * \wpre\expr{\Ret\var.\prop}[\mask] \proves \wpre\expr{\Ret\var.\propB*\prop}[\mask]}

\infer[wp-bind]
{\text{$\lctx$ is a context}}
{\wpre\expr{\Ret\var. \wpre{\lctx(\ofval(\var))}{\Ret\varB.\prop}[\mask]}[\mask] \proves \wpre{\lctx(\expr)}{\Ret\varB.\prop}[\mask]}
\end{mathpar}
546

547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586
\subsection{Lifting of operational semantics}\label{sec:lifting}
~\\\ralf{Add this.}

% The following lemmas help in proving axioms for a particular language.
% The first applies to expressions with side-effects, and the second to side-effect-free expressions.
% \dave{Update the others, and the example, wrt the new treatment of $\predB$.}
% \begin{align*}
%  &\All \expr, \state, \pred, \prop, \propB, \mask. \\
%  &\textlog{reducible}(e) \implies \\
%  &(\All \expr', \state'. \cfg{\state}{\expr} \step \cfg{\state'}{\expr'} \implies \pred(\expr', \state')) \implies \\
%  &{} \proves \bigl( (\All \expr', \state'. \pred (\expr', \state') \Ra \hoare{\prop}{\expr'}{\Ret\val. \propB}[\mask]) \Ra \hoare{ \later \prop * \ownPhys{\state} }{\expr}{\Ret\val. \propB}[\mask] \bigr) \\
%  \quad\\
%  &\All \expr, \pred, \prop, \propB, \mask. \\
%  &\textlog{reducible}(e) \implies \\
%  &(\All \state, \expr_2, \state_2. \cfg{\state}{\expr} \step \cfg{\state_2}{\expr_2} \implies \state_2 = \state \land \pred(\expr_2)) \implies \\
%  &{} \proves \bigl( (\All \expr'. \pred(\expr') \Ra \hoare{\prop}{\expr'}{\Ret\val. \propB}[\mask]) \Ra \hoare{\later\prop}{\expr}{\Ret\val. \propB}[\mask] \bigr)
% \end{align*}
% Note that $\pred$ is a meta-logic predicate---it does not depend on any world or resources being owned.

% The following specializations cover all cases of a heap-manipulating lambda calculus like $F_{\mu!}$.
% \begin{align*}
%  &\All \expr, \expr', \prop, \propB, \mask. \\
%  &\textlog{reducible}(e) \implies \\
%  &(\All \state, \expr_2, \state_2. \cfg{\state}{\expr} \step \cfg{\state_2}{\expr_2} \implies \state_2 = \state \land \expr_2 = \expr') \implies \\
%  &{} \proves (\hoare{\prop}{\expr'}{\Ret\val. \propB}[\mask] \Ra \hoare{\later\prop}{\expr}{\Ret\val. \propB}[\mask] ) \\
%  \quad \\
%  &\All \expr, \state, \pred, \mask. \\
%  &\textlog{atomic}(e) \implies \\
%  &\bigl(\All \expr_2, \state_2. \cfg{\state}{\expr} \step \cfg{\state_2}{\expr_2} \implies \pred(\expr_2, \state_2)\bigr) \implies \\
%  &{} \proves (\hoare{ \ownPhys{\state} }{\expr}{\Ret\val. \Exists\state'. \ownPhys{\state'} \land \pred(\val, \state') }[\mask] )
% \end{align*}
% The first is restricted to deterministic pure reductions, like $\beta$-reduction.
% The second is suited to proving triples for (possibly non-deterministic) atomic expressions; for example, with $\expr \eqdef \;!\ell$ (dereferencing $\ell$) and $\state \eqdef h \mtimes \ell \mapsto \valB$ and $\pred(\val, \state') \eqdef \state' = (h \mtimes \ell \mapsto \valB) \land \val = \valB$, one obtains the axiom $\All h, \ell, \valB. \hoare{\ownPhys{h \mtimes \ell \mapsto \valB}}{!\ell}{\Ret\val. \val = \valB \land \ownPhys{h \mtimes \ell \mapsto \valB} }$.
% %Axioms for CAS-like operations can be obtained by first deriving rules for the two possible cases, and then using the disjunction rule.


\subsection{Adequacy}

The adequacy statement reads as follows:
\begin{align*}
Ralf Jung's avatar
Ralf Jung committed
587
 &\All \mask, \expr, \val, \pred, \state, \melt, \state', \tpool'.
Ralf Jung's avatar
Ralf Jung committed
588 589 590 591
 \\&(\All n. \melt \in \mval_n) \Ra
 \\&( \ownPhys\state * \ownGGhost\melt \proves \wpre{\expr}{x.\; \pred(x)}[\mask]) \Ra
 \\&\cfg{\state}{[\expr]} \step^\ast
     \cfg{\state'}{[\val] \dplus \tpool'} \Ra
592 593
     \\&\pred(\val)
\end{align*}
Ralf Jung's avatar
Ralf Jung committed
594
where $\pred$ is a \emph{meta-level} predicate over values, \ie it can mention neither resources nor invariants.
595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620


% RJ: If we want this section back, we should port it to primitive view shifts and prove it in Coq.
% \subsection{Unsound rules}

% Some rule suggestions (or rather, wishes) keep coming up, which are unsound. We collect them here.
% \begin{mathpar}
% 	\infer
% 	{P \vs Q}
% 	{\later P \vs \later Q}
% 	\and
% 	\infer
% 	{\later(P \vs Q)}
% 	{\later P \vs \later Q}
% \end{mathpar}

% Of course, the second rule implies the first, so let's focus on that.
% Since implications work under $\later$, from $\later P$ we can get $\later \pvs{Q}$.
% If we now try to prove $\pvs{\later Q}$, we will be unable to establish world satisfaction in the new world:
% We have no choice but to use $\later \pvs{Q}$ at one step index below what we are operating on (because we have it under a $\later$).
% We can easily get world satisfaction for that lower step-index (by downwards-closedness of step-indexed predicates).
% We can, however, not make much use of the world satisfaction that we get out, becaase it is one step-index too low.




621 622 623 624
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "iris"
%%% End: