model.tex 12 KB
Newer Older
1
\section{Model and semantics}
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: