logic.tex 24 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
\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}
Ralf Jung's avatar
Ralf Jung committed
8
9
\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{\bot})\]
  We will write $\expr_1, \state_1 \step \expr_2, \state_2$ for $\expr_1, \state_1 \step \expr_2, \state_2, \bot$. \\
Ralf Jung's avatar
Ralf Jung committed
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
  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
\begin{defn}
  An expression $\expr$ and state $\state$ are \emph{reducible} (written $\red(\expr, \state)$) if
  \[ \Exists \expr_2, \state_2, \expr'. \expr,\state \step \expr_2,\state_2,\expr' \]
\end{defn}

Ralf Jung's avatar
Ralf Jung committed
32
\begin{defn}[Context]
Ralf Jung's avatar
Ralf Jung committed
33
  A function $\lctx : \textdom{Expr} \to \textdom{Expr}$ is a \emph{context} if the following conditions are satisfied:
34
  \begin{enumerate}[itemsep=0pt]
Ralf Jung's avatar
Ralf Jung committed
35
36
37
38
39
40
41
  \item $\lctx$ does not turn non-values into values:\\
    $\All\expr. \toval(\expr) = \bot \Ra \toval(\lctx(\expr)) = \bot $
  \item One can perform reductions below $\lctx$:\\
    $\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' $
  \item Reductions stay below $\lctx$ until there is a value in the hole:\\
    $\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' $
  \end{enumerate}
Ralf Jung's avatar
Ralf Jung committed
42
43
\end{defn}

Ralf Jung's avatar
Ralf Jung committed
44
45
46
\subsection{The concurrent language}

For any language $\Lang$, we define the corresponding thread-pool semantics.
47
48
49

\paragraph{Machine syntax}
\[
Ralf Jung's avatar
Ralf Jung committed
50
	\tpool \in \textdom{ThreadPool} \eqdef \bigcup_n \textdom{Exp}^n
51
52
\]

Ralf Jung's avatar
Ralf Jung committed
53
54
\judgment{Machine reduction} {\cfg{\tpool}{\state} \step
  \cfg{\tpool'}{\state'}}
55
56
\begin{mathpar}
\infer
Ralf Jung's avatar
Ralf Jung committed
57
58
59
60
61
62
63
  {\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'}}
64
65
\end{mathpar}

66
\clearpage
Ralf Jung's avatar
Ralf Jung committed
67
68
69
70
71
\section{The logic}

To instantiate Iris, you need to define the following parameters:
\begin{itemize}
\item A language $\Lang$
Ralf Jung's avatar
Ralf Jung committed
72
\item A locally contractive bifunctor $\iFunc : \COFEs \to \CMRAs$ defining the ghost state, such that for all COFEs $A$, the CMRA $\iFunc(A)$ has a unit
Ralf Jung's avatar
Ralf Jung committed
73
\end{itemize}
74

Ralf Jung's avatar
Ralf Jung committed
75
76
77
\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:
78
\[
79
	\SigType \supseteq \{ \textlog{Val}, \textlog{Expr}, \textlog{State}, \textlog{M}, \textlog{InvName}, \textlog{InvMask}, \Prop \}
80
\]
Ralf Jung's avatar
Ralf Jung committed
81
82
83
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$).
84
85
86
87
88
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
89
90
91
92
93
94

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}
95
96

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

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

141
Note that $\always$ and $\later$ bind more tightly than $*$, $\wand$, $\land$, $\lor$, and $\Ra$.
Ralf Jung's avatar
Ralf Jung committed
142
We will write $\pvs[\term] \prop$ for $\pvs[\term][\term] \prop$.
143
144
If we omit the mask, then it is $\top$ for weakest precondition $\wpre\expr{\Ret\var.\prop}$ and $\emptyset$ for primitive view shifts $\pvs \prop$.

Ralf Jung's avatar
Ralf Jung committed
145
146
147
148
149
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 as follows:

\[ \vctx \proves \timeless{\prop} \eqdef \vctx\mid\later\prop \proves \prop \lor \later\FALSE \]

150

151
\paragraph{Metavariable conventions.}
Ralf Jung's avatar
Ralf Jung committed
152
We introduce additional metavariables ranging over terms and generally let the choice of metavariable indicate the term's type:
153
154
\[
\begin{array}{r|l}
Ralf Jung's avatar
Ralf Jung committed
155
 \text{metavariable} & \text{type} \\\hline
156
  \term, \termB & \text{arbitrary} \\
157
158
159
  \val, \valB & \textlog{Val} \\
  \expr & \textlog{Expr} \\
  \state & \textlog{State} \\
160
161
162
\end{array}
\qquad\qquad
\begin{array}{r|l}
Ralf Jung's avatar
Ralf Jung committed
163
 \text{metavariable} & \text{type} \\\hline
164
165
166
  \iname & \textlog{InvName} \\
  \mask & \textlog{InvMask} \\
  \melt, \meltB & \textlog{M} \\
167
  \prop, \propB, \propC & \Prop \\
Ralf Jung's avatar
Ralf Jung committed
168
  \pred, \predB, \predC & \type\to\Prop \text{ (when $\type$ is clear from context)} \\
169
170
171
172
\end{array}
\]

\paragraph{Variable conventions.}
173
We often abuse notation, using the preceding \emph{term} meta-variables to range over (bound) \emph{variables}.
174
We omit type annotations in binders, when the type is clear from context.
Ralf Jung's avatar
Ralf Jung committed
175
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.
176
177
178
179
180


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

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

Ralf Jung's avatar
Ralf Jung committed
183
184
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$.
185

Ralf Jung's avatar
Ralf Jung committed
186
\judgment{Well-typed terms}{\vctx \proves_\Sig \wtt{\term}{\type}}
187
188
\begin{mathparpagebreakable}
%%% variables and function symbols
Ralf Jung's avatar
Ralf Jung committed
189
	\axiom{x : \type \proves \wtt{x}{\type}}
190
\and
Ralf Jung's avatar
Ralf Jung committed
191
192
	\infer{\vctx \proves \wtt{\term}{\type}}
		{\vctx, x:\type' \proves \wtt{\term}{\type}}
193
\and
Ralf Jung's avatar
Ralf Jung committed
194
195
	\infer{\vctx, x:\type', y:\type' \proves \wtt{\term}{\type}}
		{\vctx, x:\type' \proves \wtt{\term[x/y]}{\type}}
196
\and
Ralf Jung's avatar
Ralf Jung committed
197
198
	\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}}
199
200
201
202
203
204
205
206
207
208
209
\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
210
	\axiom{\vctx \proves \wtt{()}{1}}
211
\and
Ralf Jung's avatar
Ralf Jung committed
212
213
	\infer{\vctx \proves \wtt{\term}{\type_1} \and \vctx \proves \wtt{\termB}{\type_2}}
		{\vctx \proves \wtt{(\term,\termB)}{\type_1 \times \type_2}}
214
\and
Ralf Jung's avatar
Ralf Jung committed
215
216
	\infer{\vctx \proves \wtt{\term}{\type_1 \times \type_2} \and i \in \{1, 2\}}
		{\vctx \proves \wtt{\pi_i\,\term}{\type_i}}
217
218
%%% functions
\and
Ralf Jung's avatar
Ralf Jung committed
219
220
	\infer{\vctx, x:\type \proves \wtt{\term}{\type'}}
		{\vctx \proves \wtt{\Lam x. \term}{\type \to \type'}}
221
222
\and
	\infer
Ralf Jung's avatar
Ralf Jung committed
223
224
	{\vctx \proves \wtt{\term}{\type \to \type'} \and \wtt{\termB}{\type}}
	{\vctx \proves \wtt{\term(\termB)}{\type'}}
225
%%% monoids
226
227
\and
        \infer{}{\vctx \proves \wtt\munit{\textlog{M}}}
228
\and
Ralf Jung's avatar
Ralf Jung committed
229
	\infer{\vctx \proves \wtt\melt{\textlog{M}}}{\vctx \proves \wtt{\mcore\melt}{\textlog{M}}}
230
\and
231
232
	\infer{\vctx \proves \wtt{\melt}{\textlog{M}} \and \vctx \proves \wtt{\meltB}{\textlog{M}}}
		{\vctx \proves \wtt{\melt \mtimes \meltB}{\textlog{M}}}
233
234
235
236
237
238
%%% props and predicates
\\
	\axiom{\vctx \proves \wtt{\FALSE}{\Prop}}
\and
	\axiom{\vctx \proves \wtt{\TRUE}{\Prop}}
\and
Ralf Jung's avatar
Ralf Jung committed
239
240
	\infer{\vctx \proves \wtt{\term}{\type} \and \vctx \proves \wtt{\termB}{\type}}
		{\vctx \proves \wtt{\term =_\type \termB}{\Prop}}
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
\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{
258
259
		\vctx, \var:\type \proves \wtt{\term}{\type} \and
		\text{$\var$ is guarded in $\term$}
260
	}{
261
		\vctx \proves \wtt{\MU \var:\type. \term}{\type}
262
263
	}
\and
Ralf Jung's avatar
Ralf Jung committed
264
265
	\infer{\vctx, x:\type \proves \wtt{\prop}{\Prop}}
		{\vctx \proves \wtt{\Exists x:\type. \prop}{\Prop}}
266
\and
Ralf Jung's avatar
Ralf Jung committed
267
268
	\infer{\vctx, x:\type \proves \wtt{\prop}{\Prop}}
		{\vctx \proves \wtt{\All x:\type. \prop}{\Prop}}
269
270
271
\and
	\infer{
		\vctx \proves \wtt{\prop}{\Prop} \and
272
		\vctx \proves \wtt{\iname}{\textlog{InvName}}
273
274
275
276
	}{
		\vctx \proves \wtt{\knowInv{\iname}{\prop}}{\Prop}
	}
\and
277
	\infer{\vctx \proves \wtt{\melt}{\textlog{M}}}
278
		{\vctx \proves \wtt{\ownGGhost{\melt}}{\Prop}}
Ralf Jung's avatar
Ralf Jung committed
279
280
281
\and
	\infer{\vctx \proves \wtt{\melt}{\textlog{M}}}
		{\vctx \proves \wtt{\mval(\melt)}{\Prop}}
282
\and
283
	\infer{\vctx \proves \wtt{\state}{\textlog{State}}}
284
285
286
287
288
289
290
291
292
293
		{\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
294
295
		\vctx \proves \wtt{\mask}{\textlog{InvMask}} \and
		\vctx \proves \wtt{\mask'}{\textlog{InvMask}}
296
	}{
Ralf Jung's avatar
Ralf Jung committed
297
		\vctx \proves \wtt{\pvs[\mask][\mask'] \prop}{\Prop}
298
299
300
	}
\and
	\infer{
301
302
303
		\vctx \proves \wtt{\expr}{\textlog{Expr}} \and
		\vctx,\var:\textlog{Val} \proves \wtt{\term}{\Prop} \and
		\vctx \proves \wtt{\mask}{\textlog{InvMask}}
304
	}{
305
		\vctx \proves \wtt{\wpre{\expr}[\mask]{\Ret\var.\term}}{\Prop}
306
307
308
	}
\end{mathparpagebreakable}

Ralf Jung's avatar
Ralf Jung committed
309
\subsection{Proof rules}
Ralf Jung's avatar
Ralf Jung committed
310

311
312
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
313
Furthermore, an arbitrary \emph{boxed} assertion context $\always\pfctx$ may be added to every constituent.
Ralf Jung's avatar
Ralf Jung committed
314
Axioms $\vctx \mid \prop \provesIff \propB$ indicate that both $\vctx \mid \prop \proves \propB$ and $\vctx \mid \propB \proves \prop$ can be derived.
315

316
\judgment{}{\vctx \mid \pfctx \proves \prop}
Ralf Jung's avatar
Ralf Jung committed
317
\paragraph{Laws of intuitionistic higher-order logic with equality.}
318
This is entirely standard.
319
320
\begin{mathparpagebreakable}
\infer[Asm]
321
322
323
  {\prop \in \pfctx}
  {\pfctx \proves \prop}
\and
324
\infer[Eq]
325
326
  {\pfctx \proves \prop \\ \pfctx \proves \term =_\type \term'}
  {\pfctx \proves \prop[\term'/\term]}
327
\and
328
329
330
331
332
333
334
335
336
337
338
339
\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
340
\infer[$\wedge$I]
341
342
343
  {\pfctx \proves \prop \\ \pfctx \proves \propB}
  {\pfctx \proves \prop \wedge \propB}
\and
344
\infer[$\wedge$EL]
345
346
347
  {\pfctx \proves \prop \wedge \propB}
  {\pfctx \proves \prop}
\and
348
\infer[$\wedge$ER]
349
350
351
  {\pfctx \proves \prop \wedge \propB}
  {\pfctx \proves \propB}
\and
352
\infer[$\vee$IL]
353
354
355
  {\pfctx \proves \prop }
  {\pfctx \proves \prop \vee \propB}
\and
356
\infer[$\vee$IR]
357
358
359
  {\pfctx \proves \propB}
  {\pfctx \proves \prop \vee \propB}
\and
360
361
362
363
364
365
\infer[$\vee$E]
  {\pfctx \proves \prop \vee \propB \\
   \pfctx, \prop \proves \propC \\
   \pfctx, \propB \proves \propC}
  {\pfctx \proves \propC}
\and
366
\infer[$\Ra$I]
367
368
369
  {\pfctx, \prop \proves \propB}
  {\pfctx \proves \prop \Ra \propB}
\and
370
\infer[$\Ra$E]
371
372
373
  {\pfctx \proves \prop \Ra \propB \\ \pfctx \proves \prop}
  {\pfctx \proves \propB}
\and
374
375
376
\infer[$\forall$I]
  { \vctx,\var : \type\mid\pfctx \proves \prop}
  {\vctx\mid\pfctx \proves \forall \var: \type.\; \prop}
377
\and
378
379
380
381
\infer[$\forall$E]
  {\vctx\mid\pfctx \proves \forall \var :\type.\; \prop \\
   \vctx \proves \wtt\term\type}
  {\vctx\mid\pfctx \proves \prop[\term/\var]}
382
\and
383
384
385
386
\infer[$\exists$I]
  {\vctx\mid\pfctx \proves \prop[\term/\var] \\
   \vctx \proves \wtt\term\type}
  {\vctx\mid\pfctx \proves \exists \var: \type. \prop}
387
\and
388
389
390
391
\infer[$\exists$E]
  {\vctx\mid\pfctx \proves \exists \var: \type.\; \prop \\
   \vctx,\var : \type\mid\pfctx , \prop \proves \propB}
  {\vctx\mid\pfctx \proves \propB}
392
\and
393
394
395
\infer[$\lambda$]
  {}
  {\pfctx \proves (\Lam\var: \type. \prop)(\term) =_{\type\to\type'} \prop[\term/\var]}
396
\and
397
398
399
400
\infer[$\mu$]
  {}
  {\pfctx \proves \mu\var: \type. \prop =_{\type} \prop[\mu\var: \type. \prop/\var]}
\end{mathparpagebreakable}
401

Ralf Jung's avatar
Ralf Jung committed
402
\paragraph{Laws of (affine) bunched implications.}
403
404
\begin{mathpar}
\begin{array}{rMcMl}
Ralf Jung's avatar
Ralf Jung committed
405
406
407
  \TRUE * \prop &\provesIff& \prop \\
  \prop * \propB &\provesIff& \propB * \prop \\
  (\prop * \propB) * \propC &\provesIff& \prop * (\propB * \propC)
408
409
\end{array}
\and
410
\infer[$*$-mono]
411
412
413
  {\prop_1 \proves \propB_1 \and
   \prop_2 \proves \propB_2}
  {\prop_1 * \prop_2 \proves \propB_1 * \propB_2}
414
\and
415
\inferB[$\wand$I-E]
416
417
  {\prop * \propB \proves \propC}
  {\prop \proves \propB \wand \propC}
418
419
\end{mathpar}

Ralf Jung's avatar
Ralf Jung committed
420
\paragraph{Laws for ghosts and physical resources.}
421
422
\begin{mathpar}
\begin{array}{rMcMl}
Ralf Jung's avatar
Ralf Jung committed
423
\ownGGhost{\melt} * \ownGGhost{\meltB} &\provesIff&  \ownGGhost{\melt \mtimes \meltB} \\
Ralf Jung's avatar
Ralf Jung committed
424
\ownGGhost{\melt} &\provesIff& \mval(\melt) \\
Ralf Jung's avatar
Ralf Jung committed
425
\TRUE &\proves&  \ownGGhost{\munit}
426
427
\end{array}
\and
Ralf Jung's avatar
Ralf Jung committed
428
\and
429
\begin{array}{c}
Ralf Jung's avatar
Ralf Jung committed
430
\ownPhys{\state} * \ownPhys{\state'} \proves \FALSE
431
432
433
\end{array}
\end{mathpar}

Ralf Jung's avatar
Ralf Jung committed
434
\paragraph{Laws for the later modality.}
435
\begin{mathpar}
436
\infer[$\later$-mono]
437
438
439
  {\pfctx \proves \prop}
  {\pfctx \proves \later{\prop}}
\and
440
441
442
\infer[L{\"o}b]
  {}
  {(\later\prop\Ra\prop) \proves \prop}
443
\and
444
445
446
447
448
\infer[$\later$-$\exists$]
  {\text{$\type$ is inhabited}}
  {\later{\Exists x:\type.\prop} \proves \Exists x:\type. \later\prop}
\\\\
\begin{array}[c]{rMcMl}
Ralf Jung's avatar
Ralf Jung committed
449
450
  \later{(\prop \wedge \propB)} &\provesIff& \later{\prop} \wedge \later{\propB}  \\
  \later{(\prop \vee \propB)} &\provesIff& \later{\prop} \vee \later{\propB} \\
451
452
\end{array}
\and
453
\begin{array}[c]{rMcMl}
Ralf Jung's avatar
Ralf Jung committed
454
455
456
  \later{\All x.\prop} &\provesIff& \All x. \later\prop \\
  \Exists x. \later\prop &\proves& \later{\Exists x.\prop}  \\
  \later{(\prop * \propB)} &\provesIff& \later\prop * \later\propB
457
458
459
\end{array}
\end{mathpar}

Ralf Jung's avatar
Ralf Jung committed
460
461
462
463
464
465
466
467
468
\begin{mathpar}
\infer
{\text{$\term$ or $\term'$ is a discrete COFE element}}
{\timeless{\term =_\type \term'}}

\infer
{\text{$\melt$ is a discrete COFE element}}
{\timeless{\ownGGhost\melt}}

Ralf Jung's avatar
Ralf Jung committed
469
470
471
472
\infer
{\text{$\melt$ is a discrete COFE element}}
{\timeless{\mval(\melt)}}

Ralf Jung's avatar
Ralf Jung committed
473
\infer{}
Ralf Jung's avatar
Ralf Jung committed
474
{\timeless{\ownPhys\state}}
Ralf Jung's avatar
Ralf Jung committed
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493

\infer
{\vctx \proves \timeless{\propB}}
{\vctx \proves \timeless{\prop \Ra \propB}}

\infer
{\vctx \proves \timeless{\propB}}
{\vctx \proves \timeless{\prop \wand \propB}}

\infer
{\vctx,\var:\type \proves \timeless{\prop}}
{\vctx \proves \timeless{\All\var:\type.\prop}}

\infer
{\vctx,\var:\type \proves \timeless{\prop}}
{\vctx \proves \timeless{\Exists\var:\type.\prop}}
\end{mathpar}


Ralf Jung's avatar
Ralf Jung committed
494
\paragraph{Laws for the always modality.}
495
\begin{mathpar}
496
\infer[$\always$I]
497
498
499
  {\always{\pfctx} \proves \prop}
  {\always{\pfctx} \proves \always{\prop}}
\and
500
\infer[$\always$E]{}
Ralf Jung's avatar
Ralf Jung committed
501
  {\always{\prop} \proves \prop}
502
503
\and
\begin{array}[c]{rMcMl}
Ralf Jung's avatar
Ralf Jung committed
504
505
506
  \always{(\prop * \propB)} &\proves& \always{(\prop \land \propB)} \\
  \always{\prop} * \propB &\proves& \always{\prop} \land \propB \\
  \always{\later\prop} &\provesIff& \later\always{\prop} \\
507
508
\end{array}
\and
509
\begin{array}[c]{rMcMl}
Ralf Jung's avatar
Ralf Jung committed
510
511
512
513
  \always{(\prop \land \propB)} &\provesIff& \always{\prop} \land \always{\propB} \\
  \always{(\prop \lor \propB)} &\provesIff& \always{\prop} \lor \always{\propB} \\
  \always{\All x. \prop} &\provesIff& \All x. \always{\prop} \\
  \always{\Exists x. \prop} &\provesIff& \Exists x. \always{\prop} \\
514
\end{array}
Ralf Jung's avatar
Ralf Jung committed
515
\and
Ralf Jung's avatar
Ralf Jung committed
516
{ \term =_\type \term' \proves \always \term =_\type \term'}
Ralf Jung's avatar
Ralf Jung committed
517
\and
Ralf Jung's avatar
Ralf Jung committed
518
{ \knowInv\iname\prop \proves \always \knowInv\iname\prop}
Ralf Jung's avatar
Ralf Jung committed
519
\and
Ralf Jung's avatar
Ralf Jung committed
520
{ \ownGGhost{\mcore\melt} \proves \always \ownGGhost{\mcore\melt}}
521
522
\end{mathpar}

Ralf Jung's avatar
Ralf Jung committed
523
\paragraph{Laws of primitive view shifts.}
Ralf Jung's avatar
Ralf Jung committed
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[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}

Ralf Jung's avatar
Ralf Jung committed
546
\inferH{pvs-allocI}
Ralf Jung's avatar
Ralf Jung committed
547
548
549
{\text{$\mask$ is infinite}}
{\later\prop \proves \pvs[\mask] \Exists \iname \in \mask. \knowInv\iname\prop}

Ralf Jung's avatar
Ralf Jung committed
550
\inferH{pvs-openI}
Ralf Jung's avatar
Ralf Jung committed
551
552
{}{\knowInv\iname\prop \proves \pvs[\set\iname][\emptyset] \later\prop}

Ralf Jung's avatar
Ralf Jung committed
553
\inferH{pvs-closeI}
Ralf Jung's avatar
Ralf Jung committed
554
555
{}{\knowInv\iname\prop \land \later\prop \proves \pvs[\emptyset][\set\iname] \TRUE}

Ralf Jung's avatar
Ralf Jung committed
556
\inferH{pvs-update}
Ralf Jung's avatar
Ralf Jung committed
557
558
559
{\melt \mupd \meltsB}
{\ownGGhost\melt \proves \pvs[\mask] \Exists\meltB\in\meltsB. \ownGGhost\meltB}
\end{mathpar}
560

Ralf Jung's avatar
Ralf Jung committed
561
\paragraph{Laws of weakest preconditions.}
Ralf Jung's avatar
Ralf Jung committed
562
563
\begin{mathpar}
\infer[wp-value]
564
{}{\prop[\val/\var] \proves \wpre{\val}[\mask]{\Ret\var.\prop}}
Ralf Jung's avatar
Ralf Jung committed
565
566

\infer[wp-mono]
567
{\mask_1 \subseteq \mask_2 \and \var:\textlog{val}\mid\prop \proves \propB}
568
{\wpre\expr[\mask_1]{\Ret\var.\prop} \proves \wpre\expr[\mask_2]{\Ret\var.\propB}}
Ralf Jung's avatar
Ralf Jung committed
569
570

\infer[pvs-wp]
571
{}{\pvs[\mask] \wpre\expr[\mask]{\Ret\var.\prop} \proves \wpre\expr[\mask]{\Ret\var.\prop}}
Ralf Jung's avatar
Ralf Jung committed
572
573

\infer[wp-pvs]
574
{}{\wpre\expr[\mask]{\Ret\var.\pvs[\mask] \prop} \proves \wpre\expr[\mask]{\Ret\var.\prop}}
Ralf Jung's avatar
Ralf Jung committed
575
576
577

\infer[wp-atomic]
{\mask_2 \subseteq \mask_1 \and \physatomic{\expr}}
578
579
{\pvs[\mask_1][\mask_2] \wpre\expr[\mask_2]{\Ret\var. \pvs[\mask_2][\mask_1]\prop}
 \proves \wpre\expr[\mask_1]{\Ret\var.\prop}}
Ralf Jung's avatar
Ralf Jung committed
580
581

\infer[wp-frame]
582
{}{\propB * \wpre\expr[\mask]{\Ret\var.\prop} \proves \wpre\expr[\mask]{\Ret\var.\propB*\prop}}
Ralf Jung's avatar
Ralf Jung committed
583
584
585

\infer[wp-frame-step]
{\toval(\expr) = \bot}
586
{\later\propB * \wpre\expr[\mask]{\Ret\var.\prop} \proves \wpre\expr[\mask]{\Ret\var.\propB*\prop}}
Ralf Jung's avatar
Ralf Jung committed
587
588
589

\infer[wp-bind]
{\text{$\lctx$ is a context}}
590
{\wpre\expr[\mask]{\Ret\var. \wpre{\lctx(\ofval(\var))}[\mask]{\Ret\varB.\prop}} \proves \wpre{\lctx(\expr)}[\mask]{\Ret\varB.\prop}}
Ralf Jung's avatar
Ralf Jung committed
591
\end{mathpar}
592

593
\subsection{Lifting of operational semantics}\label{sec:lifting}
Ralf Jung's avatar
Ralf Jung committed
594
595
596
597
598
599
600

\begin{mathparpagebreakable}
  \infer[wp-lift-step]
  {\mask_2 \subseteq \mask_1 \and
   \toval(\expr_1) = \bot \and
   \red(\expr_1, \state_1) \and
   \All \expr_2, \state_2, \expr'. \expr_1,\state_1 \step \expr_2,\state_2,\expr' \Ra \pred(\expr_2,\state_2,\expr')}
601
  {\pvs[\mask_1][\mask_2] \later\ownPhys{\state_1} * \later\All \expr_2, \state_2, \expr'. \pred(\expr_2, \state_2, \expr') \land \ownPhys{\state_2} \wand \pvs[\mask_2][\mask_1] \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \wpre{\expr'}[\top]{\Ret\var.\TRUE} {}\\\proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}}
Ralf Jung's avatar
Ralf Jung committed
602
603
604
605
606

  \infer[wp-lift-pure-step]
  {\toval(\expr_1) = \bot \and
   \All \state_1. \red(\expr_1, \state_1) \and
   \All \state_1, \expr_2, \state_2, \expr'. \expr_1,\state_1 \step \expr_2,\state_2,\expr' \Ra \state_1 = \state_2 \land \pred(\expr_2,\expr')}
607
  {\later\All \expr_2, \expr'. \pred(\expr_2, \expr')  \wand \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \wpre{\expr'}[\top]{\Ret\var.\TRUE} \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}}
Ralf Jung's avatar
Ralf Jung committed
608
609
\end{mathparpagebreakable}

610
Here we define $\wpre{\expr'}[\mask]{\Ret\var.\prop} \eqdef \TRUE$ if $\expr' = \bot$ (remember that our stepping relation can, but does not have to, define a forked-off expression).
611
612
613

\subsection{Adequacy}

Ralf Jung's avatar
Ralf Jung committed
614
The adequacy statement concerning functional correctness reads as follows:
615
\begin{align*}
Ralf Jung's avatar
Ralf Jung committed
616
 &\All \mask, \expr, \val, \pred, \state, \melt, \state', \tpool'.
Ralf Jung's avatar
Ralf Jung committed
617
 \\&(\All n. \melt \in \mval_n) \Ra
618
 \\&( \ownPhys\state * \ownGGhost\melt \proves \wpre{\expr}[\mask]{x.\; \pred(x)}) \Ra
Ralf Jung's avatar
Ralf Jung committed
619
620
 \\&\cfg{\state}{[\expr]} \step^\ast
     \cfg{\state'}{[\val] \dplus \tpool'} \Ra
621
622
     \\&\pred(\val)
\end{align*}
Ralf Jung's avatar
Ralf Jung committed
623
where $\pred$ is a \emph{meta-level} predicate over values, \ie it can mention neither resources nor invariants.
624

Ralf Jung's avatar
Ralf Jung committed
625
626
627
628
629
630
631
632
633
634
635
Furthermore, the following adequacy statement shows that our weakest preconditions imply that the execution never gets \emph{stuck}: Every expression in the thread pool either is a value, or can reduce further.
\begin{align*}
 &\All \mask, \expr, \state, \melt, \state', \tpool'.
 \\&(\All n. \melt \in \mval_n) \Ra
 \\&( \ownPhys\state * \ownGGhost\melt \proves \wpre{\expr}[\mask]{x.\; \pred(x)}) \Ra
 \\&\cfg{\state}{[\expr]} \step^\ast
     \cfg{\state'}{\tpool'} \Ra
     \\&\All\expr'\in\tpool'. \toval(\expr) \neq \bot \lor \red(\expr, \state')
\end{align*}
Notice that this is stronger than saying that the thread pool can reduce; we actually assert that \emph{every} non-finished thread can take a step.

636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660

% 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.




661
662
663
664
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "iris"
%%% End: