derived.tex 25 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
\section{Derived proof rules and other constructions}
2

Ralf Jung's avatar
Ralf Jung committed
3
4
5
6
7
We will below abuse notation, using the \emph{term} meta-variables like $\val$ to range over (bound) \emph{variables} of the corresponding type..
We omit type annotations in binders and equality, when the type is clear from context.
We assume that the signature $\Sig$ embeds all the meta-level concepts we use, and their properties, into the logic.
(The Coq formalization is a \emph{shallow embedding} of the logic, so we have direct access to all meta-level notions within the logic anyways.)

8
9
\subsection{Base logic}

Ralf Jung's avatar
Ralf Jung committed
10
11
12
13
14
15
We collect here some important and frequently used derived proof rules.
\begin{mathparpagebreakable}
  \infer{}
  {\prop \Ra \propB \proves \prop \wand \propB}

  \infer{}
Ralf Jung's avatar
Ralf Jung committed
16
  {\prop * \Exists\var.\propB \provesIff \Exists\var. \prop * \propB}
Ralf Jung's avatar
Ralf Jung committed
17
18
19
20
21

  \infer{}
  {\prop * \Exists\var.\propB \proves \Exists\var. \prop * \propB}

  \infer{}
Ralf Jung's avatar
Ralf Jung committed
22
  {\always(\prop*\propB) \provesIff \always\prop * \always\propB}
Ralf Jung's avatar
Ralf Jung committed
23
24
25
26
27
28
29
30

  \infer{}
  {\always(\prop \Ra \propB) \proves \always\prop \Ra \always\propB}

  \infer{}
  {\always(\prop \wand \propB) \proves \always\prop \wand \always\propB}

  \infer{}
Ralf Jung's avatar
Ralf Jung committed
31
  {\always(\prop \wand \propB) \provesIff \always(\prop \Ra \propB)}
Ralf Jung's avatar
Ralf Jung committed
32
33
34
35
36
37
38
39
40
41
42

  \infer{}
  {\later(\prop \Ra \propB) \proves \later\prop \Ra \later\propB}

  \infer{}
  {\later(\prop \wand \propB) \proves \later\prop \wand \later\propB}

  \infer
  {\pfctx, \later\prop \proves \prop}
  {\pfctx \proves \prop}
\end{mathparpagebreakable}
43

44
45
46
47
48
49
\paragraph{Persistent assertions.}
\begin{defn}
  An assertion $\prop$ is \emph{persistent} if $\prop \proves \always\prop$.
\end{defn}

Of course, $\always\prop$ is persistent for any $\prop$.
Ralf Jung's avatar
Ralf Jung committed
50
Furthermore, by the proof rules given above, $t = t'$ as well as $\ownGGhost{\mcore\melt}$ and $\knowInv\iname\prop$ are persistent.
51
52
53
54
Persistence is preserved by conjunction, disjunction, separating conjunction as well as universal and existential quantification.

In our proofs, we will implicitly add and remove $\always$ from persistent assertions as necessary, and generally treat them like normal, non-linear assumptions.

Ralf Jung's avatar
Ralf Jung committed
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
\paragraph{Timeless assertions.}

We can show that the following additional closure properties hold for timeless assertions:

\begin{mathparpagebreakable}
  \infer
  {\vctx \proves \timeless{\prop} \and \vctx \proves \timeless{\propB}}
  {\vctx \proves \timeless{\prop \land \propB}}

  \infer
  {\vctx \proves \timeless{\prop} \and \vctx \proves \timeless{\propB}}
  {\vctx \proves \timeless{\prop \lor \propB}}

  \infer
  {\vctx \proves \timeless{\prop} \and \vctx \proves \timeless{\propB}}
  {\vctx \proves \timeless{\prop * \propB}}

  \infer
  {\vctx \proves \timeless{\prop}}
  {\vctx \proves \timeless{\always\prop}}
\end{mathparpagebreakable}


78
79
\subsection{Program logic}

Ralf Jung's avatar
Ralf Jung committed
80
Hoare triples and view shifts are syntactic sugar for weakest (liberal) preconditions and primitive view shifts, respectively:
81
\[
82
\hoare{\prop}{\expr}{\Ret\val.\propB}[\mask] \eqdef \always{(\prop \Ra \wpre{\expr}[\mask]{\lambda\Ret\val.\propB})}
83
84
85
86
87
88
\qquad\qquad
\begin{aligned}
\prop \vs[\mask_1][\mask_2] \propB &\eqdef \always{(\prop \Ra \pvs[\mask_1][\mask_2] {\propB})} \\
\prop \vsE[\mask_1][\mask_2] \propB &\eqdef \prop \vs[\mask_1][\mask_2] \propB \land \propB \vs[\mask2][\mask_1] \prop
\end{aligned}
\]
Ralf Jung's avatar
Ralf Jung committed
89
We write just one mask for a view shift when $\mask_1 = \mask_2$.
90
91
Clearly, all of these assertions are persistent.
The convention for omitted masks is similar to the base logic:
Ralf Jung's avatar
Ralf Jung committed
92
93
94
An omitted $\mask$ is $\top$ for Hoare triples and $\emptyset$ for view shifts.


Ralf Jung's avatar
Ralf Jung committed
95
\paragraph{View shifts.}
96
The following rules can be derived for view shifts.
Ralf Jung's avatar
Ralf Jung committed
97

98
99
\begin{mathparpagebreakable}
\inferH{vs-update}
Ralf Jung's avatar
Ralf Jung committed
100
101
102
  {\melt \mupd \meltsB}
  {\ownGGhost{\melt} \vs \exists \meltB \in \meltsB.\; \ownGGhost{\meltB}}
\and
103
\inferH{vs-trans}
Ralf Jung's avatar
Ralf Jung committed
104
105
106
  {\prop \vs[\mask_1][\mask_2] \propB \and \propB \vs[\mask_2][\mask_3] \propC \and \mask_2 \subseteq \mask_1 \cup \mask_3}
  {\prop \vs[\mask_1][\mask_3] \propC}
\and
107
\inferH{vs-imp}
Ralf Jung's avatar
Ralf Jung committed
108
109
110
  {\always{(\prop \Ra \propB)}}
  {\prop \vs[\emptyset] \propB}
\and
111
\inferH{vs-mask-frame}
Ralf Jung's avatar
Ralf Jung committed
112
  {\prop \vs[\mask_1][\mask_2] \propB}
113
  {\prop \vs[\mask_1 \uplus \mask'][\mask_2 \uplus \mask'] \propB}
Ralf Jung's avatar
Ralf Jung committed
114
\and
115
116
117
118
119
\inferH{vs-frame}
  {\prop \vs[\mask_1][\mask_2] \propB}
  {\prop * \propC \vs[\mask_1][\mask_2] \propB * \propC}
\and
\inferH{vs-timeless}
Ralf Jung's avatar
Ralf Jung committed
120
121
122
  {\timeless{\prop}}
  {\later \prop \vs \prop}
\and
123
124
125
126
127
\inferH{vs-allocI}
  {\infinite(\mask)}
  {\later{\prop} \vs[\mask] \exists \iname\in\mask.\; \knowInv{\iname}{\prop}}
\and
\axiomH{vs-openI}
Ralf Jung's avatar
Ralf Jung committed
128
129
  {\knowInv{\iname}{\prop} \proves \TRUE \vs[\{ \iname \} ][\emptyset] \later \prop}
\and
130
\axiomH{vs-closeI}
Ralf Jung's avatar
Ralf Jung committed
131
132
  {\knowInv{\iname}{\prop} \proves \later \prop \vs[\emptyset][\{ \iname \} ] \TRUE }

133
\inferHB{vs-disj}
Ralf Jung's avatar
Ralf Jung committed
134
135
136
  {\prop \vs[\mask_1][\mask_2] \propC \and \propB \vs[\mask_1][\mask_2] \propC}
  {\prop \lor \propB \vs[\mask_1][\mask_2] \propC}
\and
137
\inferHB{vs-exist}
Ralf Jung's avatar
Ralf Jung committed
138
139
140
  {\All \var. (\prop \vs[\mask_1][\mask_2] \propB)}
  {(\Exists \var. \prop) \vs[\mask_1][\mask_2] \propB}
\and
141
\inferHB{vs-box}
Ralf Jung's avatar
Ralf Jung committed
142
  {\always\propB \proves \prop \vs[\mask_1][\mask_2] \propC}
Ralf Jung's avatar
Ralf Jung committed
143
144
  {\prop \land \always{\propB} \vs[\mask_1][\mask_2] \propC}
 \and
145
\inferH{vs-false}
Ralf Jung's avatar
Ralf Jung committed
146
147
  {}
  {\FALSE \vs[\mask_1][\mask_2] \prop }
148
\end{mathparpagebreakable}
Ralf Jung's avatar
Ralf Jung committed
149
150


151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
\paragraph{Hoare triples.}
The following rules can be derived for Hoare triples.

\begin{mathparpagebreakable}
\inferH{Ht-ret}
  {}
  {\hoare{\TRUE}{\valB}{\Ret\val. \val = \valB}[\mask]}
\and
\inferH{Ht-bind}
  {\text{$\lctx$ is a context} \and \hoare{\prop}{\expr}{\Ret\val. \propB}[\mask] \\
   \All \val. \hoare{\propB}{\lctx(\val)}{\Ret\valB.\propC}[\mask]}
  {\hoare{\prop}{\lctx(\expr)}{\Ret\valB.\propC}[\mask]}
\and
\inferH{Ht-csq}
  {\prop \vs \prop' \\
    \hoare{\prop'}{\expr}{\Ret\val.\propB'}[\mask] \\   
   \All \val. \propB' \vs \propB}
  {\hoare{\prop}{\expr}{\Ret\val.\propB}[\mask]}
\and
\inferH{Ht-mask-weaken}
  {\hoare{\prop}{\expr}{\Ret\val. \propB}[\mask]}
  {\hoare{\prop}{\expr}{\Ret\val. \propB}[\mask \uplus \mask']}
\\\\
\inferH{Ht-frame}
  {\hoare{\prop}{\expr}{\Ret\val. \propB}[\mask]}
  {\hoare{\prop * \propC}{\expr}{\Ret\val. \propB * \propC}[\mask]}
\and
\inferH{Ht-frame-step}
  {\hoare{\prop}{\expr}{\Ret\val. \propB}[\mask] \and \toval(\expr) = \bot}
  {\hoare{\prop * \later\propC}{\expr}{\Ret\val. \propB * \propC}[\mask]}
\and
\inferH{Ht-atomic}
  {\prop \vs[\mask \uplus \mask'][\mask] \prop' \\
    \hoare{\prop'}{\expr}{\Ret\val.\propB'}[\mask] \\   
   \All\val. \propB' \vs[\mask][\mask \uplus \mask'] \propB \\
   \physatomic{\expr}
Ralf Jung's avatar
Ralf Jung committed
187
  }
188
  {\hoare{\prop}{\expr}{\Ret\val.\propB}[\mask \uplus \mask']}
Ralf Jung's avatar
Ralf Jung committed
189
\and
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
\inferHB{Ht-disj}
  {\hoare{\prop}{\expr}{\Ret\val.\propC}[\mask] \and \hoare{\propB}{\expr}{\Ret\val.\propC}[\mask]}
  {\hoare{\prop \lor \propB}{\expr}{\Ret\val.\propC}[\mask]}
\and
\inferHB{Ht-exist}
  {\All \var. \hoare{\prop}{\expr}{\Ret\val.\propB}[\mask]}
  {\hoare{\Exists \var. \prop}{\expr}{\Ret\val.\propB}[\mask]}
\and
\inferHB{Ht-box}
  {\always\propB \proves \hoare{\prop}{\expr}{\Ret\val.\propC}[\mask]}
  {\hoare{\prop \land \always{\propB}}{\expr}{\Ret\val.\propC}[\mask]}
\and
\inferH{Ht-false}
  {}
  {\hoare{\FALSE}{\expr}{\Ret \val. \prop}[\mask]}
\end{mathparpagebreakable}
Ralf Jung's avatar
Ralf Jung committed
206

Ralf Jung's avatar
Ralf Jung committed
207
\paragraph{Lifting of operational semantics.}
Ralf Jung's avatar
Ralf Jung committed
208
209
210
We can derive some specialized forms of the lifting axioms for the operational semantics.
\begin{mathparpagebreakable}
  \infer[wp-lift-atomic-step]
211
  {\atomic(\expr_1) \and
Ralf Jung's avatar
Ralf Jung committed
212
   \red(\expr_1, \state_1) \and
Ralf Jung's avatar
Ralf Jung committed
213
214
   \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)}
  {\later\ownPhys{\state_1} * \later\All \val_2, \state_2, \expr_\f. \pred(\ofval(\val), \state_2, \expr_\f) \land \ownPhys{\state_2} \wand \prop[\val_2/\var] * \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}}
Ralf Jung's avatar
Ralf Jung committed
215
216

  \infer[wp-lift-atomic-det-step]
217
  {\atomic(\expr_1) \and
Ralf Jung's avatar
Ralf Jung committed
218
   \red(\expr_1, \state_1) \and
Ralf Jung's avatar
Ralf Jung committed
219
220
   \All \expr'_2, \state'_2, \expr_\f'. \expr_1,\state_1 \step \expr_2,\state_2,\expr_\f \Ra \state_2 = \state_2' \land \toval(\expr_2') = \val_2 \land \expr_\f = \expr_\f'}
  {\later\ownPhys{\state_1} * \later(\ownPhys{\state_2} \wand \prop[\val_2/\var] * \wpre{\expr_\f}[\top]{\Ret\any.\TRUE}) \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}}
Ralf Jung's avatar
Ralf Jung committed
221
222
223
224

  \infer[wp-lift-pure-det-step]
  {\toval(\expr_1) = \bot \and
   \All \state_1. \red(\expr_1, \state_1) \and
Ralf Jung's avatar
Ralf Jung committed
225
226
   \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 \expr_2 = \expr_2' \land \expr_\f = \expr_\f'}
  {\later ( \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
227
\end{mathparpagebreakable}
Ralf Jung's avatar
Ralf Jung committed
228

Ralf Jung's avatar
Ralf Jung committed
229
230
231
232
233
234
Furthermore, we derive some forms that directly involve view shifts and Hoare triples.
\begin{mathparpagebreakable}
  \infer[ht-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
235
   \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
236
   \prop \vs[\mask_1][\mask_2] \later\ownPhys{\state_1} * \later\prop' \and
Ralf Jung's avatar
Ralf Jung committed
237
238
239
   \All \expr_2, \state_2, \expr_\f. \pred(\expr_2, \state_2, \expr_\f) * \ownPhys{\state_2} * \prop' \vs[\mask_2][\mask_1] \propB_1 * \propB_2 \\\\
   \All \expr_2, \state_2, \expr_\f. \hoare{\propB_1}{\expr_2}{\Ret\val.\propC}[\mask_1] \and
   \All \expr_2, \state_2, \expr_\f. \hoare{\propB_2}{\expr_\f}{\Ret\any. \TRUE}[\top]}
Ralf Jung's avatar
Ralf Jung committed
240
241
242
243
244
  { \hoare\prop{\expr_1}{\Ret\val.\propC}[\mask_1] }

  \infer[ht-lift-atomic-step]
  {\atomic(\expr_1) \and
   \red(\expr_1, \state_1) \and
Ralf Jung's avatar
Ralf Jung committed
245
   \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
246
   \prop \vs[\mask_1][\mask_2] \later\ownPhys{\state_1} * \later\prop' \and
Ralf Jung's avatar
Ralf Jung committed
247
248
   \All \expr_2, \state_2, \expr_\f. \hoare{\pred(\expr_2,\state_2,\expr_\f) * \prop}{\expr_\f}{\Ret\any. \TRUE}[\top]}
  { \hoare{\later\ownPhys{\state_1} * \later\prop}{\expr_1}{\Ret\val.\Exists \state_2, \expr_\f. \ownPhys{\state_2} * \pred(\ofval(\expr_2),\state_2,\expr_\f)}[\mask_1] }
Ralf Jung's avatar
Ralf Jung committed
249
250
251
252

  \infer[ht-lift-pure-step]
  {\toval(\expr_1) = \bot \and
   \All\state_1. \red(\expr_1, \state_1) \and
Ralf Jung's avatar
Ralf Jung committed
253
254
255
   \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) \\\\
   \All \expr_2, \expr_\f. \hoare{\pred(\expr_2,\expr_\f) * \prop}{\expr_2}{\Ret\val.\propB}[\mask_1] \and
   \All \expr_2, \expr_\f. \hoare{\pred(\expr_2,\expr_\f) * \prop'}{\expr_\f}{\Ret\any. \TRUE}[\top]}
Ralf Jung's avatar
Ralf Jung committed
256
257
258
259
260
  { \hoare{\later(\prop*\prop')}{\expr_1}{\Ret\val.\propB}[\mask_1] }

  \infer[ht-lift-pure-det-step]
  {\toval(\expr_1) = \bot \and
   \All\state_1. \red(\expr_1, \state_1) \and
Ralf Jung's avatar
Ralf Jung committed
261
   \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 \expr_2 = \expr_2' \land \expr_\f = \expr_\f' \\\\
Ralf Jung's avatar
Ralf Jung committed
262
   \hoare{\prop}{\expr_2}{\Ret\val.\propB}[\mask_1] \and
Ralf Jung's avatar
Ralf Jung committed
263
   \hoare{\prop'}{\expr_\f}{\Ret\any. \TRUE}[\top]}
Ralf Jung's avatar
Ralf Jung committed
264
265
  { \hoare{\later(\prop*\prop')}{\expr_1}{\Ret\val.\propB}[\mask_1] }
\end{mathparpagebreakable}
Ralf Jung's avatar
Ralf Jung committed
266

Ralf Jung's avatar
Ralf Jung committed
267
\subsection{Global functor and ghost ownership}
Ralf Jung's avatar
Ralf Jung committed
268
269

Hereinafter we assume the global CMRA functor (served up as a parameter to Iris) is obtained from a family of functors $(F_i)_{i \in I}$ for some finite $I$ by picking
270
271
\[ F(\cofe) \eqdef \prod_{i \in I} \textlog{GhName} \fpfn F_i(\cofe) \]
We don't care so much about what concretely $\textlog{GhName}$ is, as long as it is countable and infinite.
Ralf Jung's avatar
Ralf Jung committed
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
With $M_i \eqdef F_i(\iProp)$, we write $\ownGhost{\gname}{\melt : M_i}$ (or just $\ownGhost{\gname}{\melt}$ if $M_i$ is clear from the context) for $\ownGGhost{[i \mapsto [\gname \mapsto \melt]]}$.
In other words, $\ownGhost{\gname}{\melt : M_i}$ asserts that in the current state of monoid $M_i$, the ``ghost location'' $\gname$ is allocated and we own piece $\melt$.

From~\ruleref{pvs-update}, \ruleref{vs-update} and the frame-preserving updates in~\Sref{sec:prodm} and~\Sref{sec:fpfnm}, we have the following derived rules.
\begin{mathparpagebreakable}
  \inferH{NewGhostStrong}{\text{$G$ infinite}}
  {  \TRUE \vs \Exists\gname\in G. \ownGhost\gname{\melt : M_i}
  }
  \and
  \axiomH{NewGhost}{
    \TRUE \vs \Exists\gname. \ownGhost\gname{\melt : M_i}
  }
  \and
  \inferH{GhostUpd}
    {\melt \mupd_{M_i} B}
    {\ownGhost\gname{\melt : M_i} \vs \Exists \meltB\in B. \ownGhost\gname{\meltB : M_i}}
  \and
  \axiomH{GhostEq}
    {\ownGhost\gname{\melt : M_i} * \ownGhost\gname{\meltB : M_i} \Lra \ownGhost\gname{\melt\mtimes\meltB : M_i}}

  \axiomH{GhostVal}
    {\ownGhost\gname{\melt : M_i} \Ra \mval_{M_i}(\melt)}

  \inferH{GhostTimeless}
    {\text{$\melt$ is a discrete COFE element}}
    {\timeless{\ownGhost\gname{\melt : M_i}}}
\end{mathparpagebreakable}
299

Ralf Jung's avatar
Ralf Jung committed
300
\subsection{Invariant identifier namespaces}
301
302
303
304
305
306
307

Let $\namesp \ni \textlog{InvNamesp} \eqdef \textlog{list}(\textlog{InvName})$ be the type of \emph{namespaces} for invariant names.
Notice that there is an injection $\textlog{namesp\_inj}: \textlog{InvNamesp} \ra \textlog{InvName}$.
Whenever needed (in particular, for masks at view shifts and Hoare triples), we coerce $\namesp$ to its suffix-closure: \[\namecl\namesp \eqdef \setComp{\iname}{\Exists \namesp'. \iname = \textlog{namesp\_inj}(\namesp' \dplus \namesp)}\]
We use the notation $\namesp.\iname$ for the namespace $[\iname] \dplus \namesp$.

We define the inclusion relation on namespaces as $\namesp_1 \sqsubseteq \namesp_2 \Lra \Exists \namesp_3. \namesp_2 = \namesp_3 \dplus \namesp_1$, \ie $\namesp_1$ is a suffix of $\namesp_2$.
Ralf Jung's avatar
Ralf Jung committed
308
We have that $\namesp_1 \sqsubseteq \namesp_2 \Ra \namecl{\namesp_2} \subseteq \namecl{\namesp_1}$.
309
310

Similarly, we define $\namesp_1 \sep \namesp_2 \eqdef   \Exists \namesp_1', \namesp_2'. \namesp_1' \sqsubseteq \namesp_1 \land \namesp_2' \sqsubseteq \namesp_2 \land |\namesp_1'| = |\namesp_2'| \land \namesp_1' \neq \namesp_2'$, \ie there exists a distinguishing suffix.
Ralf Jung's avatar
Ralf Jung committed
311
We have that $\namesp_1 \sep \namesp_2 \Ra \namecl{\namesp_2} \sep \namecl{\namesp_1}$, and furthermore $\iname_1 \neq \iname_2 \Ra \namesp.\iname_1 \sep \namesp.\iname_2$.
312

313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
We will overload the usual Iris notation for invariant assertions in the following:
\[ \knowInv\namesp\prop \eqdef \Exists \iname \in \namecl\namesp. \knowInv\iname{\prop} \]
We can now derive the following rules for this derived form of the invariant assertion:
\begin{mathpar}
  \axiom{\knowInv\namesp\prop \proves \always\knowInv\namesp\prop}

  \axiom{\later\prop \proves \pvs[\namesp] \knowInv\namesp\prop}

  \infer{\physatomic{\expr} \and \namesp \subseteq \mask \and
    \pfctx \proves \knowInv\namesp\prop \and
    \pfctx \proves \later\prop \wand \wpre\expr[\mask \setminus \namesp]{\Ret\val.\later\prop * \propB}}
  {\pfctx \proves \wpre\expr[\mask]{\Ret\val.\propB}}

  \infer{\namesp \subseteq \mask \and
    \pfctx \proves \knowInv\namesp\prop \and
    \pfctx \proves \later\prop \wand \pvs[\mask \setminus \namesp]{\later\prop * \propB}}
  {\pfctx \proves \pvs[\mask]{\propB}}

  \infer{\physatomic{\expr} \and \namesp \subseteq \mask \and
    \hoare{\later\prop*\propB}\expr{\Ret\val.\later\prop*\propC}[\mask \setminus \namesp]}
  {\knowInv\namesp\prop \proves \hoare\propB\expr{\Ret\val.\propC}[\mask]}

  \infer{\namesp \subseteq \mask \and
    \later\prop*\propB \vs[\mask \setminus \namesp] \later\prop*\propC}
  {\knowInv\namesp\prop \proves \propB \vs[\mask] \propC}
\end{mathpar}
Ralf Jung's avatar
Ralf Jung committed
339

340
% TODO: These need syncing with Coq
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
% \subsection{STSs with interpretation}\label{sec:stsinterp}

% Building on \Sref{sec:stsmon}, after constructing the monoid $\STSMon{\STSS}$ for a particular STS, we can use an invariant to tie an interpretation, $\pred : \STSS \to \Prop$, to the STS's current state, recovering CaReSL-style reasoning~\cite{caresl}.

% An STS invariant asserts authoritative ownership of an STS's current state and that state's interpretation:
% \begin{align*}
%   \STSInv(\STSS, \pred, \gname) \eqdef{}& \Exists s \in \STSS. \ownGhost{\gname}{(s, \STSS, \emptyset):\STSMon{\STSS}} * \pred(s) \\
%   \STS(\STSS, \pred, \gname, \iname) \eqdef{}& \knowInv{\iname}{\STSInv(\STSS, \pred, \gname)}
% \end{align*}

% We can specialize \ruleref{NewInv}, \ruleref{InvOpen}, and \ruleref{InvClose} to STS invariants:
% \begin{mathpar}
%  \inferH{NewSts}
%   {\infinite(\mask)}
%   {\later\pred(s) \vs[\mask] \Exists \iname \in \mask, \gname.   \STS(\STSS, \pred, \gname, \iname) * \ownGhost{\gname}{(s, \STST \setminus \STSL(s)) : \STSMon{\STSS}}}
%  \and
%  \axiomH{StsOpen}
%   {  \STS(\STSS, \pred, \gname, \iname) \vdash \ownGhost{\gname}{(s_0, T) : \STSMon{\STSS}} \vsE[\{\iname\}][\emptyset] \Exists s\in \upclose(\{s_0\}, T). \later\pred(s) * \ownGhost{\gname}{(s, \upclose(\{s_0\}, T), T):\STSMon{\STSS}}}
%  \and
%  \axiomH{StsClose}
%   {  \STS(\STSS, \pred, \gname, \iname), (s, T) \ststrans (s', T')  \proves \later\pred(s') * \ownGhost{\gname}{(s, S, T):\STSMon{\STSS}} \vs[\emptyset][\{\iname\}] \ownGhost{\gname}{(s', T') : \STSMon{\STSS}} }
% \end{mathpar}
% \begin{proof}
% \ruleref{NewSts} uses \ruleref{NewGhost} to allocate $\ownGhost{\gname}{(s, \upclose(s, T), T) : \STSMon{\STSS}}$ where $T \eqdef \STST \setminus \STSL(s)$, and \ruleref{NewInv}.

% \ruleref{StsOpen} just uses \ruleref{InvOpen} and \ruleref{InvClose} on $\iname$, and the monoid equality $(s, \upclose(\{s_0\}, T), T) = (s, \STSS, \emptyset) \mtimes (\munit, \upclose(\{s_0\}, T), T)$.

% \ruleref{StsClose} applies \ruleref{StsStep} and \ruleref{InvClose}.
% \end{proof}
370

371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
% Using these view shifts, we can prove STS variants of the invariant rules \ruleref{Inv} and \ruleref{VSInv}~(compare the former to CaReSL's island update rule~\cite{caresl}):
% \begin{mathpar}
%  \inferH{Sts}
%   {\All s \in \upclose(\{s_0\}, T). \hoare{\later\pred(s) * P}{\expr}{\Ret \val. \Exists s', T'. (s, T) \ststrans (s', T') * \later\pred(s') * Q}[\mask]
%    \and \physatomic{\expr}}
%   {  \STS(\STSS, \pred, \gname, \iname) \vdash \hoare{\ownGhost{\gname}{(s_0, T):\STSMon{\STSS}} * P}{\expr}{\Ret \val. \Exists s', T'. \ownGhost{\gname}{(s', T'):\STSMon{\STSS}} * Q}[\mask \uplus \{\iname\}]}
%  \and
%  \inferH{VSSts}
%   {\forall s \in \upclose(\{s_0\}, T).\; \later\pred(s) * P \vs[\mask_1][\mask_2] \exists s', T'.\; (s, T) \ststrans (s', T') * \later\pred(s') * Q}
%   {  \STS(\STSS, \pred, \gname, \iname) \vdash \ownGhost{\gname}{(s_0, T):\STSMon{\STSS}} * P \vs[\mask_1 \uplus \{\iname\}][\mask_2 \uplus \{\iname\}] \Exists s', T'. \ownGhost{\gname}{(s', T'):\STSMon{\STSS}} * Q}
% \end{mathpar}

% \begin{proof}[Proof of \ruleref{Sts}]\label{pf:sts}
%  We have to show
%  \[\hoare{\ownGhost{\gname}{(s_0, T):\STSMon{\STSS}} * P}{\expr}{\Ret \val. \Exists s', T'. \ownGhost{\gname}{(s', T'):\STSMon{\STSS}} * Q}[\mask \uplus \{\iname\}]\]
%  where $\val$, $s'$, $T'$ are free in $Q$.
387
 
388
389
%  First, by \ruleref{ACsq} with \ruleref{StsOpen} and \ruleref{StsClose} (after moving $(s, T) \ststrans (s', T')$ into the view shift using \ruleref{VSBoxOut}), it suffices to show
%  \[\hoareV{\Exists s\in \upclose(\{s_0\}, T). \later\pred(s) * \ownGhost{\gname}{(s, \upclose(\{s_0\}, T), T)} * P}{\expr}{\Ret \val. \Exists s, T, S, s', T'. (s, T) \ststrans (s', T') * \later\pred(s') * \ownGhost{\gname}{(s, S, T):\STSMon{\STSS}} * Q(\val, s', T')}[\mask]\]
390

391
392
393
%  Now, use \ruleref{Exist} to move the $s$ from the precondition into the context and use \ruleref{Csq} to (i)~fix the $s$ and $T$ in the postcondition to be the same as in the precondition, and (ii)~fix $S \eqdef \upclose(\{s_0\}, T)$.
%  It remains to show:
%  \[\hoareV{s\in \upclose(\{s_0\}, T) * \later\pred(s) * \ownGhost{\gname}{(s, \upclose(\{s_0\}, T), T)} * P}{\expr}{\Ret \val. \Exists s', T'. (s, T) \ststrans (s', T') * \later\pred(s') * \ownGhost{\gname}{(s, \upclose(\{s_0\}, T), T)} * Q(\val, s', T')}[\mask]\]
394
 
395
396
%  Finally, use \ruleref{BoxOut} to move $s\in \upclose(\{s_0\}, T)$ into the context, and \ruleref{Frame} on $\ownGhost{\gname}{(s, \upclose(\{s_0\}, T), T)}$:
%  \[s\in \upclose(\{s_0\}, T) \vdash \hoare{\later\pred(s) * P}{\expr}{\Ret \val. \Exists s', T'. (s, T) \ststrans (s', T') * \later\pred(s') * Q(\val, s', T')}[\mask]\]
397
 
398
%  This holds by our premise.
Ralf Jung's avatar
Ralf Jung committed
399
% \end{proof}
400

401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
% % \begin{proof}[Proof of \ruleref{VSSts}]
% % This is similar to above, so we only give the proof in short notation:

% % \hproof{%
% % 	Context: $\knowInv\iname{\STSInv(\STSS, \pred, \gname)}$ \\
% % 	\pline[\mask_1 \uplus \{\iname\}]{
% % 		\ownGhost\gname{(s_0, T)} * P
% % 	} \\
% % 	\pline[\mask_1]{%
% % 		\Exists s. \later\pred(s) * \ownGhost\gname{(s, S, T)} * P
% % 	} \qquad by \ruleref{StsOpen} \\
% % 	Context: $s \in S \eqdef \upclose(\{s_0\}, T)$ \\
% % 	\pline[\mask_2]{%
% % 		 \Exists s', T'. \later\pred(s') * Q(s', T') * \ownGhost\gname{(s, S, T)}
% % 	} \qquad by premiss \\
% % 	Context: $(s, T) \ststrans (s', T')$ \\
% % 	\pline[\mask_2 \uplus \{\iname\}]{
% % 		\ownGhost\gname{(s', T')} * Q(s', T')
% % 	} \qquad by \ruleref{StsClose}
% % }
% % \end{proof}

% \subsection{Authoritative monoids with interpretation}\label{sec:authinterp}

% Building on \Sref{sec:auth}, after constructing the monoid $\auth{M}$ for a cancellative monoid $M$, we can tie an interpretation, $\pred : \mcarp{M} \to \Prop$, to the authoritative element of $M$, recovering reasoning that is close to the sharing rule in~\cite{krishnaswami+:icfp12}.

% Let $\pred_\bot$ be the extension of $\pred$ to $\mcar{M}$ with $\pred_\bot(\mzero) = \FALSE$.
% Now define
% \begin{align*}
%   \AuthInv(M, \pred, \gname) \eqdef{}& \exists \melt \in \mcar{M}.\; \ownGhost{\gname}{\authfull \melt:\auth{M}} * \pred_\bot(\melt) \\
%   \Auth(M, \pred, \gname, \iname) \eqdef{}& M~\textlog{cancellative} \land \knowInv{\iname}{\AuthInv(M, \pred, \gname)}
% \end{align*}

% The frame-preserving updates for $\auth{M}$ gives rise to the following view shifts:
% \begin{mathpar}
%  \inferH{NewAuth}
%   {\infinite(\mask) \and M~\textlog{cancellative}}
%   {\later\pred_\bot(a) \vs[\mask] \exists \iname \in \mask, \gname.\; \Auth(M, \pred, \gname, \iname) * \ownGhost{\gname}{\authfrag a : \auth{M}}}
%  \and
%  \axiomH{AuthOpen}
Ralf Jung's avatar
Ralf Jung committed
441
%   {\Auth(M, \pred, \gname, \iname) \vdash \ownGhost{\gname}{\authfrag \melt : \auth{M}} \vsE[\{\iname\}][\emptyset] \exists \melt_\f.\; \later\pred_\bot(\melt \mtimes \melt_\f) * \ownGhost{\gname}{\authfull \melt \mtimes \melt_\f, \authfrag a:\auth{M}}}
442
443
%  \and
%  \axiomH{AuthClose}
Ralf Jung's avatar
Ralf Jung committed
444
%   {\Auth(M, \pred, \gname, \iname) \vdash \later\pred_\bot(\meltB \mtimes \melt_\f) * \ownGhost{\gname}{\authfull a \mtimes \melt_\f, \authfrag a:\auth{M}} \vs[\emptyset][\{\iname\}] \ownGhost{\gname}{\authfrag \meltB : \auth{M}} }
445
446
447
448
449
% \end{mathpar}

% These view shifts in turn can be used to prove variants of the invariant rules:
% \begin{mathpar}
%  \inferH{Auth}
Ralf Jung's avatar
Ralf Jung committed
450
%   {\forall \melt_\f.\; \hoare{\later\pred_\bot(a \mtimes \melt_\f) * P}{\expr}{\Ret\val. \exists \meltB.\; \later\pred_\bot(\meltB\mtimes \melt_\f) * Q}[\mask]
451
452
453
454
%    \and \physatomic{\expr}}
%   {\Auth(M, \pred, \gname, \iname) \vdash \hoare{\ownGhost{\gname}{\authfrag a:\auth{M}} * P}{\expr}{\Ret\val. \exists \meltB.\; \ownGhost{\gname}{\authfrag \meltB:\auth{M}} * Q}[\mask \uplus \{\iname\}]}
%  \and
%  \inferH{VSAuth}
Ralf Jung's avatar
Ralf Jung committed
455
%   {\forall \melt_\f.\; \later\pred_\bot(a \mtimes \melt_\f) * P \vs[\mask_1][\mask_2] \exists \meltB.\; \later\pred_\bot(\meltB \mtimes \melt_\f) * Q(\meltB)}
456
457
458
459
460
461
462
463
%   {\Auth(M, \pred, \gname, \iname) \vdash
%    \ownGhost{\gname}{\authfrag a:\auth{M}} * P \vs[\mask_1 \uplus \{\iname\}][\mask_2 \uplus \{\iname\}]
%    \exists \meltB.\; \ownGhost{\gname}{\authfrag \meltB:\auth{M}} * Q(\meltB)}
% \end{mathpar}


% \subsection{Ghost heap}
% \label{sec:ghostheap}%
Ralf Jung's avatar
Ralf Jung committed
464
% FIXME use the finmap provided by the global ghost ownership, instead of adding our own
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
% We define a simple ghost heap with fractional permissions.
% Some modules require a few ghost names per module instance to properly manage ghost state, but would like to expose to clients a single logical name (avoiding clutter).
% In such cases we use these ghost heaps.

% We seek to implement the following interface:
% \newcommand{\GRefspecmaps}{\textsf{GMapsTo}}%
% \begin{align*}
%  \exists& {\fgmapsto[]} : \textsort{Val} \times \mathbb{Q}_{>} \times \textsort{Val} \ra \textsort{Prop}.\;\\
%   & \All x, q, v. x \fgmapsto[q] v \Ra x \fgmapsto[q] v \land q \in (0, 1] \\
%   &\forall x, q_1, q_2, v, w.\; x \fgmapsto[q_1] v * x \fgmapsto[q_2] w \Leftrightarrow x \fgmapsto[q_1 + q_2] v * v = w\\
%   & \forall v.\; \TRUE \vs[\emptyset] \exists x.\; x \fgmapsto[1] v \\
%   & \forall x, v, w.\; x \fgmapsto[1] v \vs[\emptyset] x \fgmapsto[1] w
% \end{align*}
% We write $x \fgmapsto v$ for $\exists q.\; x \fgmapsto[q] v$ and $x \gmapsto v$ for $x \fgmapsto[1] v$.
% Note that $x \fgmapsto v$ is duplicable but cannot be boxed (as it depends on resources); \ie we have $x \fgmapsto v \Lra x \fgmapsto v * x \fgmapsto v$ but not $x \fgmapsto v \Ra \always x \fgmapsto v$.

% To implement this interface, allocate an instance $\gname_G$ of $\FHeap(\textdom{Val})$ and define
% \[
% 	x \fgmapsto[q] v \eqdef
% 	  \begin{cases}
%     	\ownGhost{\gname_G}{x \mapsto (q, v)} & \text{if $q \in (0, 1]$} \\
%     	\FALSE & \text{otherwise}
%     \end{cases}
% \]
% The view shifts in the specification follow immediately from \ruleref{GhostUpd} and the frame-preserving updates in~\Sref{sec:fheapm}.
% The first implication is immediate from the definition.
% The second implication follows by case distinction on $q_1 + q_2 \in (0, 1]$.
492

Ralf Jung's avatar
Ralf Jung committed
493
494
495
496
497

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "iris"
%%% End: