model.tex 12 KB
 Ralf Jung committed Jan 31, 2016 1 \section{Model and semantics}  Ralf Jung committed Mar 15, 2016 2 \label{sec:model}  Ralf Jung committed Jan 31, 2016 3 4 5  The semantics closely follows the ideas laid out in~\cite{catlogic}.  Ralf Jung committed Mar 12, 2016 6 \subsection{Generic model of base logic}  Ralf Jung committed Mar 12, 2016 7 \label{sec:upred-logic}  Ralf Jung committed Jan 31, 2016 8   Ralf Jung committed Mar 12, 2016 9 The base logic including equality, later, always, and a notion of ownership is defined on $\UPred(\monoid)$ for any CMRA $\monoid$.  Ralf Jung committed Jan 31, 2016 10   Ralf Jung committed Mar 12, 2016 11 \typedsection{Interpretation of base assertions}{\Sem{\vctx \proves \term : \Prop} : \Sem{\vctx} \nfn \UPred(\monoid)}  Ralf Jung committed Mar 12, 2016 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.  Ralf Jung committed Jan 31, 2016 14   Ralf Jung committed Mar 12, 2016 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$.  Ralf Jung committed Jan 31, 2016 16 17  \begin{align*}  Ralf Jung committed Mar 12, 2016 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} \\  Ralf Jung committed Jan 31, 2016 45 46 \end{align*}  Ralf Jung committed Mar 12, 2016 47 For every definition, we have to show all the side-conditions: The maps have to be non-expansive and monotone.  Ralf Jung committed Mar 12, 2016 48 49   Ralf Jung committed Mar 12, 2016 50 \subsection{Iris model}  Ralf Jung committed Mar 12, 2016 51   Ralf Jung committed Mar 12, 2016 52 53 54 55 \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*}  Ralf Jung committed Mar 23, 2016 56  \textdom{ResF}(\cofe^\op, \cofe) \eqdef{}& \record{\wld: \agm(\latert \cofe), \pres: \exm(\textdom{State}), \ghostRes: \iFunc(\cofe^\op, \cofe)}  Ralf Jung committed Mar 12, 2016 57 \end{align*}  Ralf Jung committed Mar 23, 2016 58 59 60 Remember that $\iFunc$ is the user-chosen bifunctor from $\COFEs$ to $\CMRAs$. $\textdom{ResF}(\cofe^\op, \cofe)$ is a CMRA by lifting the individual CMRAs pointwise. Furthermore, if $F$ is locally contractive, then so is $\textdom{ResF}$.  Ralf Jung committed Mar 12, 2016 61 62  Now we can write down the recursive domain equation:  Ralf Jung committed Mar 23, 2016 63 $\iPreProp \cong \UPred(\textdom{ResF}(\iPreProp, \iPreProp))$  Ralf Jung committed Mar 15, 2016 64 $\iPreProp$ is a COFE, which exists by America and Rutten's theorem~\cite{America-Rutten:JCSS89,birkedal:metric-space}.  Ralf Jung committed Mar 12, 2016 65 66 67 We do not need to consider how the object is constructed. We only need the isomorphism, given by \begin{align*}  Ralf Jung committed Mar 23, 2016 68  \Res &\eqdef \textdom{ResF}(\iPreProp, \iPreProp) \\  Ralf Jung committed Mar 12, 2016 69 70 71 72  \iProp &\eqdef \UPred(\Res) \\ \wIso &: \iProp \nfn \iPreProp \\ \wIso^{-1} &: \iPreProp \nfn \iProp \end{align*}  Ralf Jung committed Mar 12, 2016 73   Ralf Jung committed Mar 12, 2016 74 75 We then pick $\iProp$ as the interpretation of $\Prop$: $\Sem{\Prop} \eqdef \iProp$  Ralf Jung committed Mar 12, 2016 76 77   Ralf Jung committed Mar 12, 2016 78 79 \paragraph{Interpretation of assertions.} $\iProp$ is a $\UPred$, and hence the definitions from \Sref{sec:upred-logic} apply.  Ralf Jung committed Mar 23, 2016 80 We only have to define the interpretation of the missing connectives, the most interesting bits being primitive view shifts and weakest preconditions.  Ralf Jung committed Jan 31, 2016 81   Ralf Jung committed Mar 12, 2016 82 83 84 85 86 87 88 89 \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 {}\\  Ralf Jung committed Mar 23, 2016 90  \All\iname \in \mask, \prop. (\rs.\wld)(\iname) \nequiv{n+1} \aginj(\latertinj(\wIso(\prop))) \Ra n \in \prop(\rss(\iname))  Ralf Jung committed Mar 12, 2016 91 92 93  \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*}  Ralf Jung committed Jan 31, 2016 94   Ralf Jung committed Mar 12, 2016 95 \typedsection{Primitive view-shift}{\mathit{pvs}_{-}^{-}(-) : \Delta(\pset{\mathbb{N}}) \times \Delta(\pset{\mathbb{N}}) \times \iProp \nfn \iProp}  Ralf Jung committed Mar 12, 2016 96 97 \begin{align*} \mathit{pvs}_{\mask_1}^{\mask_2}(\prop) &= \Lam \rs. \setComp{n}{\begin{aligned}  Ralf Jung committed Mar 22, 2016 98  \All \rs_\f, m, \mask_\f, \state.& 0 < m \leq n \land (\mask_1 \cup \mask_2) \disj \mask_\f \land k \in \wsat\state{\mask_1 \cup \mask_\f}{\rs \mtimes \rs_\f} \Ra {}\\&  Ralf Jung committed Mar 12, 2016 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*}  Ralf Jung committed Mar 12, 2016 102   Ralf Jung committed Mar 12, 2016 103 \typedsection{Weakest precondition}{\mathit{wp}_{-}(-, -) : \Delta(\pset{\mathbb{N}}) \times \Delta(\textdom{Exp}) \times (\Delta(\textdom{Val}) \nfn \iProp) \nfn \iProp}  Ralf Jung committed Mar 12, 2016 104   Ralf Jung committed Mar 12, 2016 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 committed Mar 22, 2016 108  \All &\rs_\f, m, \mask_\f, \state. 0 \leq m < n \land \mask \disj \mask_\f \land m+1 \in \wsat\state{\mask \cup \mask_\f}{\rs \mtimes \rs_\f} \Ra {}\\  Ralf Jung committed Mar 23, 2016 109  &(\All\val. \toval(\expr) = \val \Ra \Exists \rsB. m+1 \in \pred(\rsB) \land m+1 \in \wsat\state{\mask \cup \mask_\f}{\rsB \mtimes \rs_\f}) \land {}\\  Ralf Jung committed Mar 12, 2016 110  &(\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 {}\\  Ralf Jung committed Mar 23, 2016 111  &\qquad \Exists \rsB_1, \rsB_2. m \in \wsat\state{\mask \cup \mask_\f}{\rsB \mtimes \rs_\f} \land m \in \textdom{wp}(\mask, \expr_2, \pred)(\rsB_1) \land {}&\\  Ralf Jung committed Mar 12, 2016 112 113 114 115  &\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*}  Ralf Jung committed Mar 12, 2016 116 117   Ralf Jung committed Mar 12, 2016 118 \typedsection{Interpretation of program logic assertions}{\Sem{\vctx \proves \term : \Prop} : \Sem{\vctx} \nfn \iProp}  Ralf Jung committed Jan 31, 2016 119   Ralf Jung committed Mar 23, 2016 120 $\knowInv\iname\prop$, $\ownGGhost\melt$ and $\ownPhys\state$ are just syntactic sugar for forms of $\ownM{-}$.  Ralf Jung committed Mar 12, 2016 121 \begin{align*}  Ralf Jung committed Mar 23, 2016 122 123 124 125  \knowInv{\iname}{\prop} &\eqdef \ownM{[\iname \mapsto \aginj(\latertinj(\wIso(\prop)))], \munit, \munit} \\ \ownGGhost{\melt} &\eqdef \ownM{\munit, \munit, \melt} \\ \ownPhys{\state} &\eqdef \ownM{\munit, \exinj(\state), \munit} \\ ~\\  Ralf Jung committed Mar 12, 2016 126 127 128 129 130  \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*}  Ralf Jung committed Mar 12, 2016 131   Ralf Jung committed Mar 12, 2016 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 \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}$  Ralf Jung committed Mar 23, 2016 154 For the remaining base types $\type$ defined by the signature $\Sig$, we pick an object $X_\type$ in $\cal U$ and define  Ralf Jung committed Mar 12, 2016 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 $\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}$  Ralf Jung committed Jan 31, 2016 206 207 208 209 210  %%% Local Variables: %%% mode: latex %%% TeX-master: "iris" %%% End: