logic.tex 24.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
\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
\judgment[Machine reduction]{\cfg{\tpool}{\state} \step
Ralf Jung's avatar
Ralf Jung committed
54
  \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
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$.
144
\ralf{$\top$ is not a term in the logic. Neither is any of the operations on masks that we use in the rules for weakestpre.}
145

Ralf Jung's avatar
Ralf Jung committed
146
Some propositions are \emph{timeless}, which intuitively means that step-indexing does not affect them.
147
This is a \emph{meta-level} assertion about propositions, defined as follows:
Ralf Jung's avatar
Ralf Jung committed
148
149
150

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

151

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

\paragraph{Variable conventions.}
Ralf Jung's avatar
Ralf Jung committed
174
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.
175
176
177
178
179


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

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

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

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

Ralf Jung's avatar
Ralf Jung committed
308
\subsection{Proof rules}
Ralf Jung's avatar
Ralf Jung committed
309
\label{sec: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

Ralf Jung's avatar
Ralf Jung committed
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}}
Ralf Jung's avatar
Ralf Jung committed
521
522
\and
{ \mval(\melt) \proves \always \mval(\melt)}
523
524
\end{mathpar}

Ralf Jung's avatar
Ralf Jung committed
525
\paragraph{Laws of primitive view shifts.}
Ralf Jung's avatar
Ralf Jung committed
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
\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
543
{}{\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
544
545
546
547

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

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

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

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

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

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

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

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

\infer[wp-atomic]
{\mask_2 \subseteq \mask_1 \and \physatomic{\expr}}
580
581
{\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
582
583

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

\infer[wp-frame-step]
Ralf Jung's avatar
Ralf Jung committed
587
588
{\toval(\expr) = \bot \and \mask_2 \subseteq \mask_1}
{\wpre\expr[\mask]{\Ret\var.\prop} * \pvs[\mask_1][\mask_2]\later\pvs[\mask_2][\mask_1]\propB \proves \wpre\expr[\mask \uplus \mask_1]{\Ret\var.\propB*\prop}}
Ralf Jung's avatar
Ralf Jung committed
589
590
591

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

Ralf Jung's avatar
Ralf Jung committed
595
596
\paragraph{Lifting of operational semantics.}~
\begin{mathpar}
Ralf Jung's avatar
Ralf Jung committed
597
598
599
600
  \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
601
   \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
602
  { {\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
603
        ~~\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
604
      \end{inbox}} }
Ralf Jung's avatar
Ralf Jung committed
605
606
607
608

  \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
609
610
   \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
611
\end{mathpar}
Ralf Jung's avatar
Ralf Jung committed
612

Ralf Jung's avatar
Ralf Jung committed
613
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).
614
615
616

\subsection{Adequacy}

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

Ralf Jung's avatar
Ralf Jung committed
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
635
     \\&\All\expr'\in\tpool'. \toval(\expr') \neq \bot \lor \red(\expr', \state')
Ralf Jung's avatar
Ralf Jung committed
636
637
638
\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.

639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663

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




664
665
666
667
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "iris"
%%% End: