logic.tex 24.4 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_2$, a \emph{new thread} $\expr_\f$ is forked off.
Ralf Jung's avatar
Ralf Jung committed
11
12
\item All values are stuck:
\[ \expr, \_ \step  \_, \_, \_ \Ra \toval(\expr) = \bot \]
13
14
\end{itemize}

Ralf Jung's avatar
Ralf Jung committed
15
16
\begin{defn}
  An expression $\expr$ and state $\state$ are \emph{reducible} (written $\red(\expr, \state)$) if
Ralf Jung's avatar
Ralf Jung committed
17
  \[ \Exists \expr_2, \state_2, \expr_\f. \expr,\state \step \expr_2,\state_2,\expr_\f \]
Ralf Jung's avatar
Ralf Jung committed
18
19
\end{defn}

20
21
22
23
24
\begin{defn}
  An expression $\expr$ is said to be \emph{atomic} if it reduces in one step to a value:
  \[ \All\state_1, \expr_2, \state_2, \expr_\f. \expr, \state_1 \step \expr_2, \state_2, \expr_\f \Ra \Exists \val_2. \toval(\expr_2) = \val_2 \]
\end{defn}

Ralf Jung's avatar
Ralf Jung committed
25
\begin{defn}[Context]
Ralf Jung's avatar
Ralf Jung committed
26
  A function $\lctx : \textdom{Expr} \to \textdom{Expr}$ is a \emph{context} if the following conditions are satisfied:
27
  \begin{enumerate}[itemsep=0pt]
Ralf Jung's avatar
Ralf Jung committed
28
29
30
  \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
31
    $\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
32
  \item Reductions stay below $\lctx$ until there is a value in the hole:\\
Ralf Jung's avatar
Ralf Jung committed
33
    $\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
34
  \end{enumerate}
Ralf Jung's avatar
Ralf Jung committed
35
36
\end{defn}

Ralf Jung's avatar
Ralf Jung committed
37
\subsection{Concurrent language}
Ralf Jung's avatar
Ralf Jung committed
38
39

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

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

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

59
\clearpage
Ralf Jung's avatar
Ralf Jung committed
60
\section{Logic}
61
\label{sec:logic}
Ralf Jung's avatar
Ralf Jung committed
62
63
64

To instantiate Iris, you need to define the following parameters:
\begin{itemize}
65
66
\item A language $\Lang$, and
\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. (By \lemref{lem:cmra-unit-total-core}, this means that the core of $\iFunc(A)$ is a total function.)
Ralf Jung's avatar
Ralf Jung committed
67
\end{itemize}
68

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

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}
89
90

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

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

135
Note that $\always$ and $\later$ bind more tightly than $*$, $\wand$, $\land$, $\lor$, and $\Ra$.
Ralf Jung's avatar
Ralf Jung committed
136
We will write $\pvs[\term] \prop$ for $\pvs[\term][\term] \prop$.
137
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
138
%FIXME $\top$ is not a term in the logic. Neither is any of the operations on masks that we use in the rules for weakestpre.
139

Ralf Jung's avatar
Ralf Jung committed
140
Some propositions are \emph{timeless}, which intuitively means that step-indexing does not affect them.
141
This is a \emph{meta-level} assertion about propositions, defined as follows:
Ralf Jung's avatar
Ralf Jung committed
142
143
144

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

145

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

\paragraph{Variable conventions.}
Ralf Jung's avatar
Ralf Jung committed
168
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.
169
170
171
172
173


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

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

Ralf Jung's avatar
Ralf Jung committed
176
177
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$.
178

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

Ralf Jung's avatar
Ralf Jung committed
302
\subsection{Proof rules}
Ralf Jung's avatar
Ralf Jung committed
303
\label{sec:proof-rules}
Ralf Jung's avatar
Ralf Jung committed
304

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

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

397

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

\infer[wp-frame-step]
Ralf Jung's avatar
Ralf Jung committed
584
585
{\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
586
587
588

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

Ralf Jung's avatar
Ralf Jung committed
592
593
\paragraph{Lifting of operational semantics.}~
\begin{mathpar}
Ralf Jung's avatar
Ralf Jung committed
594
595
  \infer[wp-lift-step]
  {\mask_2 \subseteq \mask_1 \and
Ralf Jung's avatar
Ralf Jung committed
596
   \toval(\expr_1) = \bot}
Ralf Jung's avatar
Ralf Jung committed
597
  { {\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
598
        ~~\pvs[\mask_1][\mask_2] \Exists \state_1. \red(\expr_1,\state_1) \land \later\ownPhys{\state_1} * {}\\\qquad\qquad\qquad \later\All \expr_2, \state_2, \expr_\f. \left( (\expr_1, \state_1 \step \expr_2, \state_2, \expr_\f) \land \ownPhys{\state_2} \right) \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
599
      \end{inbox}} }
Ralf Jung's avatar
Ralf Jung committed
600
\\\\
Ralf Jung's avatar
Ralf Jung committed
601
602
603
  \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
604
605
   \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 }
  {\later\All \state, \expr_2, \expr_\f. (\expr_1,\state \step \expr_2, \state,\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
606
\end{mathpar}
Ralf Jung's avatar
Ralf Jung committed
607
Notice that primitive view shifts cover everything to their right, \ie $\pvs \prop * \propB \eqdef \pvs (\prop * \propB)$.
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
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
631
     \\&\All\expr'\in\tpool'. \toval(\expr') \neq \bot \lor \red(\expr', \state')
Ralf Jung's avatar
Ralf Jung committed
632
633
634
\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: