From 4243295d81443cb6331e820b5090f5717f2ce154 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 19 Apr 2016 22:18:54 -0400 Subject: [PATCH] Start of SeparationLogic chapter: assertion logic --- frap_book.tex | 87 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 87 insertions(+) diff --git a/frap_book.tex b/frap_book.tex index 0f0654b..be5405f 100644 --- a/frap_book.tex +++ b/frap_book.tex @@ -3173,6 +3173,93 @@ Another notation uses $0^n$ to refer informally to a sequence of $n$ zeroes to w Similarly, the conclusion of the $\mt{Free}$ rule unmaps a whole size-$n$ region, starting at $a$. We could also have chosen to enforce in this rule that the region starts out as mapped into $h$. +\section{Assertion Logic} + +Separation logic is based on two big ideas. +The first one has to do with the \emph{assertion logic}\index{assertion logic}, which we use to write invariants; while the second one has to do with the \emph{program logic}\index{program logic}, which we use to prove that programs satisfy specifications. +The assertion logic is based on predicates over \emph{partial memories}\emph{partial memories}, or finite maps from addresses to stored values. +Because they are finite, they omit infinitely many addresses, and it is crucial that we are able to describe heaps that intentionally leave addresses out of their domains. +Informally, a predicate \emph{claims ownership}\index{ownership} of addresses in the domains of matching heaps. + +\newcommand{\emp}[0]{\mt{emp}} +\newcommand{\lift}[1]{[#1]} +\newcommand{\ptsto}[2]{#1 \mapsto #2} + +We can describe the connectives of separation logic in terms of the sets of partial heaps that they accept. +\begin{eqnarray*} + \emp &=& \{\mempty\} \\ + \ptsto{p}{v} &=& \{\mupd{\mempty}{p}{v}\} \\ + \lift{\phi} &=& \{h \mid \phi \land h = \mempty\} \\ + \exists x. \; P(x) &=& \{h \mid \exists x. \; h \in P(x)\} \\ + P * Q &=& \{h_1 \uplus h_2 \mid h_1 \in P \land h_2 \in Q\} +\end{eqnarray*} + +The formula $\emp$ accepts only the empty heap, while formula $\ptsto{p}{v}$ accepts only the heap whose only address is $p$, mapped to value $v$. +We overload the $\mapsto$ operator in that second line above, to denote ``points-to'' on the lefthand side of the equality and finite-map overriding on the righthand side. +Notation $\lift{\phi}$ is \emph{lifting}\index{lifting pure propositions} a \emph{pure} (i.e., regular old mathematical) proposition $\phi$ into an assertion, enforcing both that the heap is empty and that $\phi$ is true. +We also adapt the normal existential quantifier to this setting. + +The essential definition is the last one, of the \emph{separating conjunction}\index{separating conjunction} $*$. +We use the notation $h_1 \uplus h_2$ for \emph{disjoint union} of heaps $h_1$ and $h_2$, implicitly enforcing $\dom{h_1} \cap \dom{h_2} = \emptyset$. +The intuition of separating conjunction is that we \emph{partition} the overall heap into two subheaps, each of which matches one of the respective conjuncts $P$ and $Q$. +This connective implicitly enforces \emph{lack of aliasing}, leading to separation logic's famous conciseness of specifications that combine data structures. + +We can also define natural comparison operators between assertions, overloading the usual notations for equivalence and implication of propositions. +\begin{eqnarray*} + P \Leftrightarrow Q &=& \forall h. \; h \in P \Leftrightarrow h \in Q \\ + P \Rightarrow Q &=& \forall h. \; h \in P \Rightarrow h \in Q +\end{eqnarray*} + +The core connectives satisfy a number of handy algebraic laws. +Here is a sampling. + +$$\infer{P * \lift{\phi} \Rightarrow Q}{ + \phi \rightarrow (P \Rightarrow Q) +} +\quad \infer{P \Rightarrow Q * \lift{\phi}}{ + \phi + & P \Rightarrow Q +} +\quad \infer{P \Leftrightarrow \lift{\phi} * P}{ + \phi +}$$ + +$$\infer{P * Q \Leftrightarrow Q * P}{} +\quad \infer{P * (Q * R) \Leftrightarrow (P * Q) * R}{} +\quad \infer{P_1 * Q_1 \Rightarrow P_2 * Q_2}{ + P_1 \Rightarrow P_2 + & Q_1 \Rightarrow Q_2 +}$$ + +$$\infer{(P * \exists x. \; Q(x)) \Leftrightarrow \exists x. \; P * Q(x)}{} +\quad \infer{(\exists x. \; P(x)) \Rightarrow Q}{ + \forall x. \; P(x) \Rightarrow Q +} +\quad \infer{P \Rightarrow \exists x. \; Q(x)}{ + P \Rightarrow Q(v) +}$$ + +This set of algebraic laws has a very special consequence: it supports automated proof of implications by \emph{cancellation}\index{cancellation}, where we repeatedly ``cross out'' matching subformulas on the two sides of the arrow. +Consider this example formula that we might want to prove. +$$(\exists q. \; \ptsto{p}{q} * \exists r. \; \ptsto{q}{r} * \ptsto{r}{0}) \Rightarrow (\exists a. \; \exists b. \; \exists c. \; \ptsto{r}{c} * \ptsto{p}{a} * \ptsto{a}{b})$$ + +First, the laws above allow us to bubble all quantifiers to the fronts of formulas. +$$(\exists q, r. \; \ptsto{p}{q} * \ptsto{q}{r} * \ptsto{r}{0}) \Rightarrow (\exists a, b, c. \; \ptsto{b}{c} * \ptsto{p}{a} * \ptsto{a}{b})$$ + +Next, all $\exists$ to the left can be replaced with fresh free variables, while all $\exists$ to the right can be replaced with fresh \emph{unification variables}\index{unification variables}, whose values, in terms of the free-variable values, we can deduce in the course of the proof. +$$\ptsto{p}{q} * \ptsto{q}{r} * \ptsto{r}{0} \Rightarrow \; \ptsto{?b}{?c} \; * \; \ptsto{p}{?a} \; * \; \ptsto{?a}{?b}$$ + +Next, we find matching subformulas to \emph{cancel}. +We start by matching $\ptsto{p}{q}$ with $\ptsto{p}{?a}$, learning that $?a = q$ and reducing to this formula. +This crucial step relies on the three key properties of $*$, given in the second row of rules above: commutativity, associativity, and cancellativity\index{cancellativity}. +$$\ptsto{q}{r} * \ptsto{r}{0} \Rightarrow \; \ptsto{?b}{?c} \; * \; \ptsto{q}{?b}$$ + +We run another cancellation step of $\ptsto{q}{r}$ against $\ptsto{q}{?b}$, learning $?q = r$. +$$\ptsto{r}{0} \Rightarrow \; \ptsto{r}{?c}$$ + +Now we can finish the proof by reflexivity of $\Rightarrow$, learning $?c = 0$. + + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%