model.tex 12 KB
 Ralf Jung committed Jan 31, 2016 1 2 3 4 \section{Model and semantics} The semantics closely follows the ideas laid out in~\cite{catlogic}.  Ralf Jung committed Mar 12, 2016 5 \subsection{Generic model of base logic}  Ralf Jung committed Mar 12, 2016 6 \label{sec:upred-logic}  Ralf Jung committed Jan 31, 2016 7   Ralf Jung committed Mar 12, 2016 8 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 9   Ralf Jung committed Mar 12, 2016 10 \typedsection{Interpretation of base assertions}{\Sem{\vctx \proves \term : \Prop} : \Sem{\vctx} \nfn \UPred(\monoid)}  Ralf Jung committed Mar 12, 2016 11 12 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 13   Ralf Jung committed Mar 12, 2016 14 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 15 16  \begin{align*}  Ralf Jung committed Mar 12, 2016 17 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  \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 44 45 \end{align*}  Ralf Jung committed Mar 12, 2016 46 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 47 48   Ralf Jung committed Mar 12, 2016 49 \subsection{Iris model}  Ralf Jung committed Mar 12, 2016 50   Ralf Jung committed Mar 12, 2016 51 52 53 54 55 56 57 58 59 60 61 62 \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))$  Ralf Jung committed Mar 15, 2016 63 $\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 64 65 66 67 68 69 70 71 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*}  Ralf Jung committed Mar 12, 2016 72   Ralf Jung committed Mar 12, 2016 73 74 We then pick $\iProp$ as the interpretation of $\Prop$: $\Sem{\Prop} \eqdef \iProp$  Ralf Jung committed Mar 12, 2016 75 76   Ralf Jung committed Mar 12, 2016 77 78 \paragraph{Interpretation of assertions.} $\iProp$ is a $\UPred$, and hence the definitions from \Sref{sec:upred-logic} apply.  Ralf Jung committed Mar 12, 2016 79 We only have to define the missing connectives, the most interesting bits being primitive view shifts and weakest preconditions.  Ralf Jung committed Jan 31, 2016 80   Ralf Jung committed Mar 12, 2016 81 82 83 84 85 86 87 88 89 90 91 92 \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*}  Ralf Jung committed Jan 31, 2016 93   Ralf Jung committed Mar 12, 2016 94 \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 95 96 \begin{align*} \mathit{pvs}_{\mask_1}^{\mask_2}(\prop) &= \Lam \rs. \setComp{n}{\begin{aligned}  Ralf Jung committed Mar 12, 2016 97  \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 committed Mar 12, 2016 98 99 100  \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 101   Ralf Jung committed Mar 12, 2016 102 \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 103   Ralf Jung committed Mar 12, 2016 104 105 106 $\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 12, 2016 107  \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 committed Mar 12, 2016 108 109 110 111 112 113 114  &(\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*}  Ralf Jung committed Mar 12, 2016 115 116   Ralf Jung committed Mar 12, 2016 117 \typedsection{Interpretation of program logic assertions}{\Sem{\vctx \proves \term : \Prop} : \Sem{\vctx} \nfn \iProp}  Ralf Jung committed Jan 31, 2016 118   Ralf Jung committed Mar 12, 2016 119 120 121 122 123 124 125 126 127 \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*}  Ralf Jung committed Mar 12, 2016 128   Ralf Jung committed Mar 12, 2016 129 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 \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}$  Ralf Jung committed Jan 31, 2016 205 206 207 208 209  %%% Local Variables: %%% mode: latex %%% TeX-master: "iris" %%% End: