model.tex 12 KB
Newer Older
1
\section{Model and semantics}
Ralf Jung's avatar
Ralf Jung committed
2
\label{sec:model}
3
4
5

The semantics closely follows the ideas laid out in~\cite{catlogic}.

6
\subsection{Generic model of base logic}
Ralf Jung's avatar
Ralf Jung committed
7
\label{sec:upred-logic}
8

9
The base logic including equality, later, always, and a notion of ownership is defined on $\UPred(\monoid)$ for any CMRA $\monoid$.
10

Ralf Jung's avatar
Ralf Jung committed
11
\typedsection{Interpretation of base assertions}{\Sem{\vctx \proves \term : \Prop} : \Sem{\vctx} \nfn \UPred(\monoid)}
12
13
Remember that $\UPred(\monoid)$ is isomorphic to $\monoid \monra \SProp$.
We are thus going to define the assertions as mapping CMRA elements to sets of step-indices.
14

15
We introduce an additional logical connective $\ownM\melt$, which will later be used to encode all of $\knowInv\iname\prop$, $\ownGGhost\melt$ and $\ownPhys\state$.
16
17

\begin{align*}
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
	\Sem{\vctx \proves t =_\type u : \Prop}_\gamma &\eqdef
	\Lam \any. \setComp{n}{\Sem{\vctx \proves t : \type}_\gamma \nequiv{n} \Sem{\vctx \proves u : \type}_\gamma} \\
	\Sem{\vctx \proves \FALSE : \Prop}_\gamma &\eqdef \Lam \any. \emptyset \\
	\Sem{\vctx \proves \TRUE : \Prop}_\gamma &\eqdef \Lam \any. \mathbb{N} \\
	\Sem{\vctx \proves \prop \land \propB : \Prop}_\gamma &\eqdef
	\Lam \melt. \Sem{\vctx \proves \prop : \Prop}_\gamma(\melt) \cap \Sem{\vctx \proves \propB : \Prop}_\gamma(\melt) \\
	\Sem{\vctx \proves \prop \lor \propB : \Prop}_\gamma &\eqdef
	\Lam \melt. \Sem{\vctx \proves \prop : \Prop}_\gamma(\melt) \cup \Sem{\vctx \proves \propB : \Prop}_\gamma(\melt) \\
	\Sem{\vctx \proves \prop \Ra \propB : \Prop}_\gamma &\eqdef
	\Lam \melt. \setComp{n}{\begin{aligned}
            \All m, \meltB.& m \leq n \land \melt \mincl \meltB \land \meltB \in \mval_m \Ra {} \\
            & m \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\melt) \Ra {}\\& m \in \Sem{\vctx \proves \propB : \Prop}_\gamma(\melt)\end{aligned}}\\
	\Sem{\vctx \proves \All x : \type. \prop : \Prop}_\gamma &\eqdef
	\Lam \melt. \setComp{n}{ \All v \in \Sem{\type}. n \in \Sem{\vctx, x : \type \proves \prop : \Prop}_{\gamma[x \mapsto v]}(\melt) } \\
	\Sem{\vctx \proves \Exists x : \type. \prop : \Prop}_\gamma &\eqdef
        \Lam \melt. \setComp{n}{ \Exists v \in \Sem{\type}. n \in \Sem{\vctx, x : \type \proves \prop : \Prop}_{\gamma[x \mapsto v]}(\melt) } \\
  ~\\
	\Sem{\vctx \proves \always{\prop} : \Prop}_\gamma &\eqdef \Lam\melt. \Sem{\vctx \proves \prop : \Prop}_\gamma(\mcore\melt) \\
	\Sem{\vctx \proves \later{\prop} : \Prop}_\gamma &\eqdef \Lam\melt. \setComp{n}{n = 0 \lor n-1 \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\melt)}\\
	\Sem{\vctx \proves \prop * \propB : \Prop}_\gamma &\eqdef \Lam\melt. \setComp{n}{\begin{aligned}\Exists \meltB_1, \meltB_2. &\melt \nequiv{n} \meltB_1 \mtimes \meltB_2 \land {}\\& n \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\meltB_1) \land n \in \Sem{\vctx \proves \propB : \Prop}_\gamma(\meltB_2)\end{aligned}}
\\
	\Sem{\vctx \proves \prop \wand \propB : \Prop}_\gamma &\eqdef
	\Lam \melt. \setComp{n}{\begin{aligned}
            \All m, \meltB.& m \leq n \land  \melt\mtimes\meltB \in \mval_m \Ra {} \\
            & m \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\meltB) \Ra {}\\& m \in \Sem{\vctx \proves \propB : \Prop}_\gamma(\melt\mtimes\meltB)\end{aligned}} \\
        \Sem{\vctx \proves \ownM{\melt} : \Prop}_\gamma &\eqdef \Lam\meltB. \setComp{n}{\melt \mincl[n] \meltB}  \\
        \Sem{\vctx \proves \mval(\melt) : \Prop}_\gamma &\eqdef \Lam\any. \setComp{n}{\melt \in \mval_n} \\
45
46
\end{align*}

Ralf Jung's avatar
Ralf Jung committed
47
For every definition, we have to show all the side-conditions: The maps have to be non-expansive and monotone.
48
49


Ralf Jung's avatar
Ralf Jung committed
50
\subsection{Iris model}
51

Ralf Jung's avatar
Ralf Jung committed
52
53
54
55
56
57
58
59
60
61
62
63
\paragraph{Semantic domain of assertions.}
The first complicated task in building a model of full Iris is defining the semantic model of $\Prop$.
We start by defining the functor that assembles the CMRAs we need to the global resource CMRA:
\begin{align*}
  \textdom{ResF}(\cofe) \eqdef{}& \record{\wld: \agm(\latert \cofe), \pres: \exm(\textdom{State}), \ghostRes: F(\cofe)}
\end{align*}
where $F$ is the user-chosen bifunctor from $\COFEs$ to $\CMRAs$.
$\textdom{ResF}(\cofe)$ is a CMRA by lifting the individual CMRAs pointwise.
Furthermore, if $F$ is locally contractive, then so is $\textdom{ResF}(-)$.

Now we can write down the recursive domain equation:
\[ \iPreProp \cong \UPred(\textdom{ResF}(\iPreProp)) \]
64
$\iPreProp$ is a COFE, which exists by America and Rutten's theorem~\cite{America-Rutten:JCSS89,birkedal:metric-space}.
Ralf Jung's avatar
Ralf Jung committed
65
66
67
68
69
70
71
72
We do not need to consider how the object is constructed. 
We only need the isomorphism, given by
\begin{align*}
  \Res &\eqdef \textdom{ResF}(\iPreProp) \\
  \iProp &\eqdef \UPred(\Res) \\
	\wIso &: \iProp \nfn \iPreProp \\
	\wIso^{-1} &: \iPreProp \nfn \iProp
\end{align*}
73

Ralf Jung's avatar
Ralf Jung committed
74
75
We then pick $\iProp$ as the interpretation of $\Prop$:
\[ \Sem{\Prop} \eqdef \iProp \]
76
77


Ralf Jung's avatar
Ralf Jung committed
78
79
\paragraph{Interpretation of assertions.}
$\iProp$ is a $\UPred$, and hence the definitions from \Sref{sec:upred-logic} apply.
Ralf Jung's avatar
Ralf Jung committed
80
We only have to define the missing connectives, the most interesting bits being primitive view shifts and weakest preconditions.
81

Ralf Jung's avatar
Ralf Jung committed
82
83
84
85
86
87
88
89
90
91
92
93
\typedsection{World satisfaction}{\wsat{-}{-}{-} : 
	\Delta\textdom{State} \times
	\Delta\pset{\mathbb{N}} \times
	\textdom{Res} \nfn \SProp }
\begin{align*}
  \wsatpre(n, \mask, \state, \rss, \rs) & \eqdef \begin{inbox}[t]
    \rs \in \mval_{n+1} \land \rs.\pres = \exinj(\sigma) \land 
    \dom(\rss) \subseteq \mask \cap \dom( \rs.\wld) \land {}\\
    \All\iname \in \mask, \prop. \rs.\wld(\iname) \nequiv{n+1} \aginj(\latertinj(\wIso(\prop))) \Ra n \in \prop(\rss(\iname))
  \end{inbox}\\
	\wsat{\state}{\mask}{\rs} &\eqdef \set{0}\cup\setComp{n+1}{\Exists \rss : \mathbb{N} \fpfn \textdom{Res}. \wsatpre(n, \mask, \state, \rss, \rs \mtimes \prod_\iname \rss(\iname))}
\end{align*}
94

Ralf Jung's avatar
Ralf Jung committed
95
\typedsection{Primitive view-shift}{\mathit{pvs}_{-}^{-}(-) : \Delta(\pset{\mathbb{N}}) \times \Delta(\pset{\mathbb{N}}) \times \iProp \nfn \iProp}
Ralf Jung's avatar
Ralf Jung committed
96
97
\begin{align*}
	\mathit{pvs}_{\mask_1}^{\mask_2}(\prop) &= \Lam \rs. \setComp{n}{\begin{aligned}
Ralf Jung's avatar
Ralf Jung committed
98
            \All \rs_\f, m, \mask_\f, \state.& 0 < m \leq n \land (\mask_1 \cup \mask_2) \sep \mask_\f \land k \in \wsat\state{\mask_1 \cup \mask_\f}{\rs \mtimes \rs_\f} \Ra {}\\&
Ralf Jung's avatar
Ralf Jung committed
99
100
101
            \Exists \rsB. k \in \prop(\rsB) \land k \in \wsat\state{\mask_2 \cup \mask_\f}{\rsB \mtimes \rs_\f}
          \end{aligned}}
\end{align*}
102

Ralf Jung's avatar
Ralf Jung committed
103
\typedsection{Weakest precondition}{\mathit{wp}_{-}(-, -) : \Delta(\pset{\mathbb{N}}) \times \Delta(\textdom{Exp}) \times (\Delta(\textdom{Val}) \nfn \iProp) \nfn \iProp}
104

Ralf Jung's avatar
Ralf Jung committed
105
106
107
$\textdom{wp}$ is defined as the fixed-point of a contractive function.
\begin{align*}
  \textdom{pre-wp}(\textdom{wp})(\mask, \expr, \pred) &\eqdef \Lam\rs. \setComp{n}{\begin{aligned}
Ralf Jung's avatar
Ralf Jung committed
108
        \All &\rs_\f, m, \mask_\f, \state. 0 \leq m < n \land \mask \sep \mask_\f \land m+1 \in \wsat\state{\mask \cup \mask_\f}{\rs \mtimes \rs_\f} \Ra {}\\
Ralf Jung's avatar
Ralf Jung committed
109
110
111
112
113
114
115
        &(\All\val. \toval(\expr) = \val \Ra \Exists \rsB. m+1 \in \prop(\rs') \land m+1 \in \wsat\state{\mask \cup \mask_\f}{\rs' \mtimes \rs_\f}) \land {}\\
        &(\toval(\expr) = \bot \land 0 < m \Ra \red(\expr, \state) \land \All \expr_2, \state_2, \expr_\f. \expr,\state \step \expr_2,\state_2,\expr_\f \Ra {}\\
        &\qquad \Exists \rsB_1, \rsB_2. m \in \wsat\state{\mask \cup \mask_\f}{\rs' \mtimes \rs_\f} \land  m \in \textdom{wp}(\mask, \expr_2, \pred)(\rsB_1) \land {}&\\
        &\qquad\qquad (\expr_\f = \bot \lor m \in \textdom{wp}(\top, \expr_\f, \Lam\any.\Lam\any.\mathbb{N})(\rsB_2))
    \end{aligned}} \\
  \textdom{wp}_\mask(\expr, \pred) &\eqdef \mathit{fix}(\textdom{pre-wp})(\mask, \expr, \pred)
\end{align*}
116
117


Ralf Jung's avatar
Ralf Jung committed
118
\typedsection{Interpretation of program logic assertions}{\Sem{\vctx \proves \term : \Prop} : \Sem{\vctx} \nfn \iProp}
119

Ralf Jung's avatar
Ralf Jung committed
120
121
122
123
124
125
126
127
128
\begin{align*}
	\Sem{\vctx \proves \knowInv{\iname}{\prop} : \Prop}_\gamma &\eqdef \ownM{[\iname \mapsto \aginj(\latertinj(\wIso(\prop)))], \munit, \munit} \\
	\Sem{\vctx \proves \ownGGhost{\melt} : \Prop}_\gamma &\eqdef \ownM{\munit, \munit, \melt} \\
	\Sem{\vctx \proves \ownPhys{\state} : \Prop}_\gamma &\eqdef \ownM{\munit, \exinj(\state), \munit} \\
	\Sem{\vctx \proves \pvs[\mask_1][\mask_2] \prop : \Prop}_\gamma &\eqdef
	\textdom{pvs}^{\Sem{\vctx \proves \mask_2 : \textlog{InvMask}}_\gamma}_{\Sem{\vctx \proves \mask_1 : \textlog{InvMask}}_\gamma}(\Sem{\vctx \proves \prop : \Prop}_\gamma) \\
	\Sem{\vctx \proves \wpre{\expr}[\mask]{\Ret\var.\prop} : \Prop}_\gamma &\eqdef
	\textdom{wp}_{\Sem{\vctx \proves \mask : \textlog{InvMask}}_\gamma}(\Sem{\vctx \proves \expr : \textlog{Expr}}_\gamma, \Lam\val. \Sem{\vctx \proves \prop : \Prop}_{\gamma[\var\mapsto\val]})
\end{align*}
129

Ralf Jung's avatar
Ralf Jung committed
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
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
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
\paragraph{Remaining semantic domains, and interpretation of non-assertion terms.}

The remaining domains are interpreted as follows:
\[
\begin{array}[t]{@{}l@{\ }c@{\ }l@{}}
\Sem{\textlog{InvName}} &\eqdef& \Delta \mathbb{N}  \\
\Sem{\textlog{InvMask}} &\eqdef& \Delta \pset{\mathbb{N}} \\
\Sem{\textlog{M}} &\eqdef& F(\iProp)
\end{array}
\qquad\qquad
\begin{array}[t]{@{}l@{\ }c@{\ }l@{}}
\Sem{\textlog{Val}} &\eqdef& \Delta \textdom{Val} \\
\Sem{\textlog{Expr}} &\eqdef& \Delta \textdom{Expr} \\
\Sem{\textlog{State}} &\eqdef& \Delta \textdom{State} \\
\end{array}
\qquad\qquad
\begin{array}[t]{@{}l@{\ }c@{\ }l@{}}
\Sem{1} &\eqdef& \Delta \{ () \} \\
\Sem{\type \times \type'} &\eqdef& \Sem{\type} \times \Sem{\type} \\
\Sem{\type \to \type'} &\eqdef& \Sem{\type} \nfn \Sem{\type} \\
\end{array}
\]

The balance of our signature $\Sig$ is interpreted as follows.
For each base type $\type$ not covered by the preceding table, we pick an object $X_\type$ in $\cal U$ and define
\[
\Sem{\type} \eqdef X_\type
\]
For each function symbol $\sigfn : \type_1, \dots, \type_n \to \type_{n+1} \in \SigFn$, we pick a function $\Sem{\sigfn} : \Sem{\type_1} \times \dots \times \Sem{\type_n} \nfn \Sem{\type_{n+1}}$.

\typedsection{Interpretation of non-propositional terms}{\Sem{\vctx \proves \term : \type} : \Sem{\vctx} \nfn \Sem{\type}}
\begin{align*}
	\Sem{\vctx \proves x : \type}_\gamma &\eqdef \gamma(x) \\
	\Sem{\vctx \proves \sigfn(\term_1, \dots, \term_n) : \type_{n+1}}_\gamma &\eqdef \Sem{\sigfn}(\Sem{\vctx \proves \term_1 : \type_1}_\gamma, \dots, \Sem{\vctx \proves \term_n : \type_n}_\gamma) \\
	\Sem{\vctx \proves \Lam \var:\type. \term : \type \to \type'}_\gamma &\eqdef
	\Lam \termB : \Sem{\type}. \Sem{\vctx, \var : \type \proves \term : \type}_{\gamma[\var \mapsto \termB]} \\
	\Sem{\vctx \proves \term(\termB) : \type'}_\gamma &\eqdef
	\Sem{\vctx \proves \term : \type \to \type'}_\gamma(\Sem{\vctx \proves \termB : \type}_\gamma) \\
	\Sem{\vctx \proves \MU \var:\type. \term : \type}_\gamma &\eqdef
	\mathit{fix}(\Lam \termB : \Sem{\type}. \Sem{\vctx, x : \type \proves \term : \type}_{\gamma[x \mapsto \termB]}) \\
  ~\\
	\Sem{\vctx \proves () : 1}_\gamma &\eqdef () \\
	\Sem{\vctx \proves (\term_1, \term_2) : \type_1 \times \type_2}_\gamma &\eqdef (\Sem{\vctx \proves \term_1 : \type_1}_\gamma, \Sem{\vctx \proves \term_2 : \type_2}_\gamma) \\
	\Sem{\vctx \proves \pi_i(\term) : \type_i}_\gamma &\eqdef \pi_i(\Sem{\vctx \proves \term : \type_1 \times \type_2}_\gamma) \\
  ~\\
	\Sem{\vctx \proves \munit : \textlog{M}}_\gamma &\eqdef \munit \\
	\Sem{\vctx \proves \mcore\melt : \textlog{M}}_\gamma &\eqdef \mcore{\Sem{\vctx \proves \melt : \textlog{M}}_\gamma} \\
	\Sem{\vctx \proves \melt \mtimes \meltB : \textlog{M}}_\gamma &\eqdef
	\Sem{\vctx \proves \melt : \textlog{M}}_\gamma \mtimes \Sem{\vctx \proves \meltB : \textlog{M}}_\gamma
\end{align*}
%

An environment $\vctx$ is interpreted as the set of
finite partial functions $\rho$, with $\dom(\rho) = \dom(\vctx)$ and
$\rho(x)\in\Sem{\vctx(x)}$.

\paragraph{Logical entailment.}
We can now define \emph{semantic} logical entailment.

\typedsection{Interpretation of entailment}{\Sem{\vctx \mid \pfctx \proves \prop} : 2}

\[
\Sem{\vctx \mid \pfctx \proves \propB} \eqdef
\begin{aligned}[t]
\MoveEqLeft
\forall n \in \mathbb{N}.\;
\forall \rs \in \textdom{Res}.\; 
\forall \gamma \in \Sem{\vctx},\;
\\&
\bigl(\All \propB \in \pfctx. n \in \Sem{\vctx \proves \propB : \Prop}_\gamma(\rs)\bigr)
\Ra n \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\rs)
\end{aligned}
\]

The soundness statement of the logic reads
\[ \vctx \mid \pfctx \proves \prop \Ra \Sem{\vctx \mid \pfctx \proves \prop} \]
206
207
208
209
210

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