Commit cfa6acb0 by Robbert Krebbers

### Define macro for singleton map and use it.

parent 095de633
 ... @@ -55,7 +55,7 @@ Frame-preserving updates on the $M_i$ lift to the product: ... @@ -55,7 +55,7 @@ Frame-preserving updates on the $M_i$ lift to the product: \begin{mathpar} \begin{mathpar} \inferH{prod-update} \inferH{prod-update} {\melt \mupd_{M_i} \meltsB} {\melt \mupd_{M_i} \meltsB} {f[i \mapsto \melt] \mupd \setComp{ f[i \mapsto \meltB]}{\meltB \in \meltsB}} {\mapinsert i \melt f \mupd \setComp{ \mapinsert i \meltB f}{\meltB \in \meltsB}} \end{mathpar} \end{mathpar} \subsection{Sum} \subsection{Sum} ... @@ -96,15 +96,15 @@ We obtain the following frame-preserving updates: ... @@ -96,15 +96,15 @@ We obtain the following frame-preserving updates: \begin{mathpar} \begin{mathpar} \inferH{fpfn-alloc-strong} \inferH{fpfn-alloc-strong} {\text{$G$ infinite} \and \melt \in \mval} {\text{$G$ infinite} \and \melt \in \mval} {\emptyset \mupd \setComp{[\gname \mapsto \melt]}{\gname \in G}} {\emptyset \mupd \setComp{\mapsingleton \gname \melt}{\gname \in G}} \inferH{fpfn-alloc} \inferH{fpfn-alloc} {\melt \in \mval} {\melt \in \mval} {\emptyset \mupd \setComp{[\gname \mapsto \melt]}{\gname \in K}} {\emptyset \mupd \setComp{\mapsingleton \gname \melt}{\gname \in K}} \inferH{fpfn-update} \inferH{fpfn-update} {\melt \mupd_\monoid \meltsB} {\melt \mupd_\monoid \meltsB} {f[i \mapsto \melt] \mupd \setComp{ f[i \mapsto \meltB]}{\meltB \in \meltsB}} {\mapinsert i \melt f] \mupd \setComp{ \mapinsert i \meltB f}{\meltB \in \meltsB}} \end{mathpar} \end{mathpar} Above, $\mval$ refers to the validity of $\monoid$. Above, $\mval$ refers to the validity of $\monoid$. ... ...
 ... @@ -197,7 +197,7 @@ This is best demonstrated by giving some proof rules. ... @@ -197,7 +197,7 @@ This is best demonstrated by giving some proof rules. So let us first define the notion of ghost ownership that we use in this logic. So let us first define the notion of ghost ownership that we use in this logic. Assuming that the family of functors contains the functor $\Sigma_i$ at index $i$, and furthermore assuming that $\monoid_i = \Sigma_i(\iPreProp, \iPreProp)$, given some $\melt \in \monoid_i$ we define: Assuming that the family of functors contains the functor $\Sigma_i$ at index $i$, and furthermore assuming that $\monoid_i = \Sigma_i(\iPreProp, \iPreProp)$, given some $\melt \in \monoid_i$ we define: $\ownGhost\gname{\melt:\monoid_i} \eqdef \ownM{(\ldots, \emptyset, i:\set{\gname \mapsto \melt}, \emptyset, \ldots)}$ $\ownGhost\gname{\melt:\monoid_i} \eqdef \ownM{(\ldots, \emptyset, i:\mapsingleton \gname \melt, \emptyset, \ldots)}$ This is ownership of the pair (element of the product over all the functors) that has the empty finite partial function in all components \emph{except for} the component corresponding to index $i$, where we own the element $\melt$ at index $\gname$ in the finite partial function. This is ownership of the pair (element of the product over all the functors) that has the empty finite partial function in all components \emph{except for} the component corresponding to index $i$, where we own the element $\melt$ at index $\gname$ in the finite partial function. We can show the following properties for this form of ownership: We can show the following properties for this form of ownership: ... ...
 ... @@ -85,6 +85,8 @@ ... @@ -85,6 +85,8 @@ \newcommand{\subst}[3]{{#1}[{#3} / {#2}]} \newcommand{\subst}[3]{{#1}[{#3} / {#2}]} \newcommand{\mapinsert}[3]{#3[#1:=#2]} \newcommand{\mapinsert}[3]{#3[#1:=#2]} \newcommand{\mapsingleton}[2]{[#1:=#2]} \newcommand{\mapsingletonComp}[3]{\left[ #1 := #2 \spac\middle|\spac #3 \right]} \newcommand{\nil}{\epsilon} \newcommand{\nil}{\epsilon} ... ...
 ... @@ -42,10 +42,10 @@ We are thus going to define the assertions as mapping CMRA elements to sets of s ... @@ -42,10 +42,10 @@ We are thus going to define the assertions as mapping CMRA elements to sets of s \Lam \melt. \setComp{n}{\begin{aligned} \Lam \melt. \setComp{n}{\begin{aligned} \All m, \meltB.& m \leq n \land \melt \mincl \meltB \land \meltB \in \mval_m \Ra {} \\ \All m, \meltB.& m \leq n \land \melt \mincl \meltB \land \meltB \in \mval_m \Ra {} \\ & m \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\meltB) \Ra {}\\& m \in \Sem{\vctx \proves \propB : \Prop}_\gamma(\meltB)\end{aligned}}\\ & m \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\meltB) \Ra {}\\& m \in \Sem{\vctx \proves \propB : \Prop}_\gamma(\meltB)\end{aligned}}\\ \Sem{\vctx \proves \All x : \type. \prop : \Prop}_\gamma &\eqdef \Sem{\vctx \proves \All \var : \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) } \\ \Lam \melt. \setComp{n}{ \All v \in \Sem{\type}. n \in \Sem{\vctx, \var : \type \proves \prop : \Prop}_{\mapinsert \var v \gamma}(\melt) } \\ \Sem{\vctx \proves \Exists x : \type. \prop : \Prop}_\gamma &\eqdef \Sem{\vctx \proves \Exists \var : \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) } \\ \Lam \melt. \setComp{n}{ \Exists v \in \Sem{\type}. n \in \Sem{\vctx, \var : \type \proves \prop : \Prop}_{\mapinsert \var v \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 * \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}} \\ \\ ... @@ -72,11 +72,11 @@ For every definition, we have to show all the side-conditions: The maps have to ... @@ -72,11 +72,11 @@ For every definition, we have to show all the side-conditions: The maps have to \Sem{\vctx \proves x : \type}_\gamma &\eqdef \gamma(x) \\ \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 \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 \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]} \\ \Lam \termB : \Sem{\type}. \Sem{\vctx, \var : \type \proves \term : \type}_{\mapinsert \var \termB \gamma]} \\ \Sem{\vctx \proves \term(\termB) : \type'}_\gamma &\eqdef \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 \term : \type \to \type'}_\gamma(\Sem{\vctx \proves \termB : \type}_\gamma) \\ \Sem{\vctx \proves \MU \var:\type. \term : \type}_\gamma &\eqdef \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]}) \\ \mathit{fix}(\Lam \termB : \Sem{\type}. \Sem{\vctx, x : \type \proves \term : \type}_{\mapinsert \var \termB \gamma}) \\ ~\\ ~\\ \Sem{\vctx \proves () : 1}_\gamma &\eqdef () \\ \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 (\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) \\ ... ...
 ... @@ -85,12 +85,20 @@ Furthermore, we assume that instances named $\gname_{\textmon{State}}$, $\gname_ ... @@ -85,12 +85,20 @@ Furthermore, we assume that instances named$\gname_{\textmon{State}}$,$\gname_ \paragraph{World Satisfaction.} \paragraph{World Satisfaction.} We can now define the assertion $W$ (\emph{world satisfaction}) which ensures that the enabled invariants are actually maintained: We can now define the assertion $W$ (\emph{world satisfaction}) which ensures that the enabled invariants are actually maintained: \begin{align*} \begin{align*} W \eqdef{}& \Exists I : \mathbb N \fpfn \Prop. \ownGhost{\gname_{\textmon{Inv}}}{\authfull \setComp{\iname \mapsto \aginj(\latertinj(\wIso(I(\iname))))}{\iname \in \dom(I)}} * \Sep_{\iname \in \dom(I)} \left( \later I(\iname) * \ownGhost{\gname_{\textmon{Dis}}}{\set{\iname}} \lor \ownGhost{\gname_{\textmon{En}}}{\set{\iname}} \right) W \eqdef{}& \Exists I : \mathbb N \fpfn \Prop. \begin{array}{@{} l} \ownGhost{\gname_{\textmon{Inv}}}{\authfull \mapsingletonComp {\iname} {\aginj(\latertinj(\wIso(I(\iname))))} {\iname \in \dom(I)}} * \\ \Sep_{\iname \in \dom(I)} \left( \later I(\iname) * \ownGhost{\gname_{\textmon{Dis}}}{\set{\iname}} \lor \ownGhost{\gname_{\textmon{En}}}{\set{\iname}} \right) \end{array} \end{align*} \end{align*} \paragraph{Invariants.} \paragraph{Invariants.} The following assertion states that an invariant with name $\iname$ exists and maintains assertion $\prop$: The following assertion states that an invariant with name $\iname$ exists and maintains assertion $\prop$: $\knowInv\iname\prop \eqdef \ownGhost{\gname_{\textmon{Inv}}}{\authfrag\set{\iname \mapsto \aginj(\latertinj(\wIso(\prop)))}}$ $\knowInv\iname\prop \eqdef \ownGhost{\gname_{\textmon{Inv}}} {\authfrag \mapsingleton \iname {\aginj(\latertinj(\wIso(\prop)))}}$ \paragraph{View Updates and View Shifts.} \paragraph{View Updates and View Shifts.} Next, we define \emph{view updates}, which are essentially the same as the resource updates of the base logic ($\Sref{sec:base-logic}$), except that they also have access to world satisfaction and can enable and disable invariants: Next, we define \emph{view updates}, which are essentially the same as the resource updates of the base logic ($\Sref{sec:base-logic}$), except that they also have access to world satisfaction and can enable and disable invariants: ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!