derived.tex 23.2 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
We will below abuse notation, using the \emph{term} meta-variables like $\val$ to range over (bound) \emph{variables} of the corresponding type.
Ralf Jung's avatar
Ralf Jung committed
4
5
6
7
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

  \infer{}
Ralf Jung's avatar
Ralf Jung committed
19
  {\prop * \All\var.\propB \proves \All\var. \prop * \propB}
Ralf Jung's avatar
Ralf Jung committed
20
21

  \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 in \Sref{sec:proof-rules}, $t = t'$ as well as $\ownGGhost{\mcore\melt}$, $\mval(\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
\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}
Ralf Jung's avatar
Ralf Jung committed
179
180
  {\hoare{\prop}{\expr}{\Ret\val. \propB}[\mask] \and \toval(\expr) = \bot \and \mask_2 \subseteq \mask_2 \\\\ \propC_1 \vs[\mask_1][\mask_2] \later\propC_2 \and \propC_2 \vs[\mask_2][\mask_1] \propC_3}
  {\hoare{\prop * \propC_1}{\expr}{\Ret\val. \propB * \propC_3}[\mask \uplus \mask_1]}
181
182
183
184
185
186
\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
\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]}
Ralf Jung's avatar
Ralf Jung committed
205
206
207
208
209
210
211
212
213
214
215
216
\and
\inferH{Ht-inv}
  {\hoare{\later\propC*\prop}{\expr}{\Ret\val.\later\propC*\propB}[\mask] \and
   \physatomic{\expr}
  }
  {\knowInv\iname\propC \proves \hoare{\prop}{\expr}{\Ret\val.\propB}[\mask \uplus \set\iname]}
\and
\inferH{Ht-inv-timeless}
  {\hoare{\propC*\prop}{\expr}{\Ret\val.\propC*\propB}[\mask] \and
   \physatomic{\expr} \and \timeless\propC
  }
  {\knowInv\iname\propC \proves \hoare{\prop}{\expr}{\Ret\val.\propB}[\mask \uplus \set\iname]}
217
\end{mathparpagebreakable}
Ralf Jung's avatar
Ralf Jung committed
218

Ralf Jung's avatar
Ralf Jung committed
219
\paragraph{Lifting of operational semantics.}
Ralf Jung's avatar
Ralf Jung committed
220
221
222
We can derive some specialized forms of the lifting axioms for the operational semantics.
\begin{mathparpagebreakable}
  \infer[wp-lift-atomic-step]
223
  {\atomic(\expr_1) \and
Ralf Jung's avatar
Ralf Jung committed
224
225
226
   \red(\expr_1, \state_1)}
  { {\begin{inbox}~~\later\ownPhys{\state_1} * \later\All \val_2, \state_2, \expr_\f. (\expr_1,\state_1 \step \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}
  \end{inbox}} }
Ralf Jung's avatar
Ralf Jung committed
227
228

  \infer[wp-lift-atomic-det-step]
229
  {\atomic(\expr_1) \and
Ralf Jung's avatar
Ralf Jung committed
230
   \red(\expr_1, \state_1) \and
Ralf Jung's avatar
Ralf Jung committed
231
232
   \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
233
234
235
236

  \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
237
238
   \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
239
\end{mathparpagebreakable}
Ralf Jung's avatar
Ralf Jung committed
240

Ralf Jung's avatar
Ralf Jung committed
241
\subsection{Global functor and ghost ownership}
Ralf Jung's avatar
Ralf Jung committed
242

243
244
Hereinafter we assume the global CMRA functor (served up as a parameter to Iris) is obtained from a family of functors $(\iFunc_i)_{i \in I}$ for some finite $I$ by picking
\[ \iFunc(\cofe) \eqdef \prod_{i \in I} \textlog{GhName} \fpfn \iFunc_i(\cofe) \]
245
We don't care so much about what concretely $\textlog{GhName}$ is, as long as it is countable and infinite.
246
With $M_i \eqdef \iFunc_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]]}$.
Ralf Jung's avatar
Ralf Jung committed
247
248
249
250
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}
Ralf Jung's avatar
Ralf Jung committed
251
  \inferH{ghost-alloc-strong}{\text{$G$ infinite}}
Ralf Jung's avatar
Ralf Jung committed
252
253
254
  {  \TRUE \vs \Exists\gname\in G. \ownGhost\gname{\melt : M_i}
  }
  \and
Ralf Jung's avatar
Ralf Jung committed
255
  \axiomH{ghost-alloc}{
Ralf Jung's avatar
Ralf Jung committed
256
257
258
    \TRUE \vs \Exists\gname. \ownGhost\gname{\melt : M_i}
  }
  \and
Ralf Jung's avatar
Ralf Jung committed
259
  \inferH{ghost-update}
Ralf Jung's avatar
Ralf Jung committed
260
261
262
    {\melt \mupd_{M_i} B}
    {\ownGhost\gname{\melt : M_i} \vs \Exists \meltB\in B. \ownGhost\gname{\meltB : M_i}}
  \and
Ralf Jung's avatar
Ralf Jung committed
263
  \axiomH{ghost-op}
Ralf Jung's avatar
Ralf Jung committed
264
265
    {\ownGhost\gname{\melt : M_i} * \ownGhost\gname{\meltB : M_i} \Lra \ownGhost\gname{\melt\mtimes\meltB : M_i}}

Ralf Jung's avatar
Ralf Jung committed
266
  \axiomH{ghost-valid}
Ralf Jung's avatar
Ralf Jung committed
267
268
    {\ownGhost\gname{\melt : M_i} \Ra \mval_{M_i}(\melt)}

Ralf Jung's avatar
Ralf Jung committed
269
  \inferH{ghost-timeless}
Ralf Jung's avatar
Ralf Jung committed
270
271
272
    {\text{$\melt$ is a discrete COFE element}}
    {\timeless{\ownGhost\gname{\melt : M_i}}}
\end{mathparpagebreakable}
273

Ralf Jung's avatar
Ralf Jung committed
274
\subsection{Invariant identifier namespaces}
275

Ralf Jung's avatar
Ralf Jung committed
276
Let $\namesp \in \textlog{InvNamesp} \eqdef \textlog{list}(\textlog{InvName})$ be the type of \emph{namespaces} for invariant names.
277
278
279
280
281
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
282
We have that $\namesp_1 \sqsubseteq \namesp_2 \Ra \namecl{\namesp_2} \subseteq \namecl{\namesp_1}$.
283

Ralf Jung's avatar
Ralf Jung committed
284
285
Similarly, we define $\namesp_1 \disj \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.
We have that $\namesp_1 \disj \namesp_2 \Ra \namecl{\namesp_2} \disj \namecl{\namesp_1}$, and furthermore $\iname_1 \neq \iname_2 \Ra \namesp.\iname_1 \disj \namesp.\iname_2$.
286

287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
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
313

314
% TODO: These need syncing with Coq
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
% \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}
344

345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
% 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$.
361
 
362
363
%  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]\]
364

365
366
367
%  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]\]
368
 
369
370
%  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]\]
371
 
372
%  This holds by our premise.
Ralf Jung's avatar
Ralf Jung committed
373
% \end{proof}
374

375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
% % \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
415
%   {\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}}}
416
417
%  \and
%  \axiomH{AuthClose}
Ralf Jung's avatar
Ralf Jung committed
418
%   {\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}} }
419
420
421
422
423
% \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
424
%   {\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]
425
426
427
428
%    \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
429
%   {\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)}
430
431
432
433
434
435
436
437
%   {\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
438
% FIXME use the finmap provided by the global ghost ownership, instead of adding our own
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
% 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]$.
466

Ralf Jung's avatar
Ralf Jung committed
467
468
469
470
471

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