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
  A reduction $\expr_1, \state_1 \step \expr_2, \state_2, \expr_\f$ indicates that, when $\expr_1$ reduces to $\expr$, a \emph{new thread} $\expr_\f$ is forked off.
Ralf Jung's avatar
Ralf Jung committed
11
12
13
14
15
16
17
18
\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}
Ralf Jung's avatar
Ralf Jung committed
19
\All\expr_1, \state_1, \expr_2, \state_2, \expr_\f. \atomic(\expr_1) \land \expr_1, \state_1 \step \expr_2, \state_2, \expr_\f \Ra {}\\\qquad\qquad\qquad\quad~~ \Exists \val_2. \toval(\expr_2) = \val_2
Ralf Jung's avatar
Ralf Jung committed
20
21
22
23
24
    \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
\begin{defn}
  An expression $\expr$ and state $\state$ are \emph{reducible} (written $\red(\expr, \state)$) if
Ralf Jung's avatar
Ralf Jung committed
29
  \[ \Exists \expr_2, \state_2, \expr_\f. \expr,\state \step \expr_2,\state_2,\expr_\f \]
Ralf Jung's avatar
Ralf Jung committed
30
31
\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
  \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$:\\
Ralf Jung's avatar
Ralf Jung committed
38
    $\All \expr_1, \state_1, \expr_2, \state_2, \expr_\f. \expr_1, \state_1 \step \expr_2,\state_2,\expr_\f \Ra \lctx(\expr_1), \state_1 \step \lctx(\expr_2),\state_2,\expr_\f $
Ralf Jung's avatar
Ralf Jung committed
39
  \item Reductions stay below $\lctx$ until there is a value in the hole:\\
Ralf Jung's avatar
Ralf Jung committed
40
    $\All \expr_1', \state_1, \expr_2, \state_2, \expr_\f. \toval(\expr_1') = \bot \land \lctx(\expr_1'), \state_1 \step \expr_2,\state_2,\expr_\f \Ra \Exists\expr_2'. \expr_2 = \lctx(\expr_2') \land \expr_1', \state_1 \step \expr_2',\state_2,\expr_\f $
Ralf Jung's avatar
Ralf Jung committed
41
  \end{enumerate}
Ralf Jung's avatar
Ralf Jung committed
42
43
\end{defn}

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

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
  {\expr_1, \state_1 \step \expr_2, \state_2, \expr_\f \and \expr_\f \neq \bot}
Ralf Jung's avatar
Ralf Jung committed
58
  {\cfg{\tpool \dplus [\expr_1] \dplus \tpool'}{\state} \step
Ralf Jung's avatar
Ralf Jung committed
59
     \cfg{\tpool \dplus [\expr_2] \dplus \tpool' \dplus [\expr_\f]}{\state'}}
Ralf Jung's avatar
Ralf Jung committed
60
61
62
63
\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
\section{Logic}
Ralf Jung's avatar
Ralf Jung committed
68
69
70
71

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
\\&
Ralf Jung's avatar
Ralf Jung committed
127
    \MU \var:\type. \term  \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. \term$, 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.}
Ralf Jung's avatar
Ralf Jung committed
173
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.
174
175
176
177
178


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

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

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

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

Ralf Jung's avatar
Ralf Jung committed
307
\subsection{Proof rules}
Ralf Jung's avatar
Ralf Jung committed
308

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

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

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

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

Ralf Jung's avatar
Ralf Jung committed
432
\paragraph{Laws for the later modality.}
433
\begin{mathpar}
434
\infer[$\later$-mono]
435
436
437
  {\pfctx \proves \prop}
  {\pfctx \proves \later{\prop}}
\and
438
439
440
\infer[L{\"o}b]
  {}
  {(\later\prop\Ra\prop) \proves \prop}
441
\and
442
443
444
445
446
\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
447
448
  \later{(\prop \wedge \propB)} &\provesIff& \later{\prop} \wedge \later{\propB}  \\
  \later{(\prop \vee \propB)} &\provesIff& \later{\prop} \vee \later{\propB} \\
449
450
\end{array}
\and
451
\begin{array}[c]{rMcMl}
Ralf Jung's avatar
Ralf Jung committed
452
453
454
  \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
455
456
457
\end{array}
\end{mathpar}

Ralf Jung's avatar
Ralf Jung committed
458
459
460
461
462
463
464
465
466
\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
467
468
469
470
\infer
{\text{$\melt$ is a discrete COFE element}}
{\timeless{\mval(\melt)}}

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

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

Ralf Jung's avatar
Ralf Jung committed
521
\paragraph{Laws of primitive view shifts.}
Ralf Jung's avatar
Ralf Jung committed
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
\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]
Ralf Jung's avatar
Ralf Jung committed
539
{}{\pvs[\mask_1][\mask_2] \prop \proves \pvs[\mask_1 \uplus \mask_\f][\mask_2 \uplus \mask_\f] \prop}
Ralf Jung's avatar
Ralf Jung committed
540
541
542
543

\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
544
\inferH{pvs-allocI}
Ralf Jung's avatar
Ralf Jung committed
545
546
547
{\text{$\mask$ is infinite}}
{\later\prop \proves \pvs[\mask] \Exists \iname \in \mask. \knowInv\iname\prop}

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

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

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

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

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

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

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

\infer[wp-atomic]
{\mask_2 \subseteq \mask_1 \and \physatomic{\expr}}
576
577
{\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
578
579

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

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

\infer[wp-bind]
{\text{$\lctx$ is a context}}
588
{\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
589
\end{mathpar}
590

Ralf Jung's avatar
Ralf Jung committed
591
592
\paragraph{Lifting of operational semantics.}~
\begin{mathpar}
Ralf Jung's avatar
Ralf Jung committed
593
594
595
596
  \infer[wp-lift-step]
  {\mask_2 \subseteq \mask_1 \and
   \toval(\expr_1) = \bot \and
   \red(\expr_1, \state_1) \and
Ralf Jung's avatar
Ralf Jung committed
597
   \All \expr_2, \state_2, \expr_\f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_\f \Ra \pred(\expr_2,\state_2,\expr_\f)}
Ralf Jung's avatar
Ralf Jung committed
598
  { {\begin{inbox} % for some crazy reason, LaTeX is actually sensitive to the space between the "{ {" here and the "} }" below...
Ralf Jung's avatar
Ralf Jung committed
599
        ~~\pvs[\mask_1][\mask_2] \later\ownPhys{\state_1} * \later\All \expr_2, \state_2, \expr_\f. \pred(\expr_2, \state_2, \expr_\f) \land {}\\\qquad\qquad\qquad\qquad\qquad \ownPhys{\state_2} \wand \pvs[\mask_2][\mask_1] \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} {}\\\proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}
Ralf Jung's avatar
Ralf Jung committed
600
      \end{inbox}} }
Ralf Jung's avatar
Ralf Jung committed
601
602
603
604

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

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

\subsection{Adequacy}

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

Ralf Jung's avatar
Ralf Jung committed
624
625
626
627
628
629
630
631
632
633
634
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.

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

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




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