Logical Methods in Computer Science
Vol. 8(3:22)2012, pp. 1–31
www.lmcs-online.org

Submitted
Published

Jul. 6, 2011
Sep. 21, 2012

TWO FOR THE PRICE OF ONE: LIFTING SEPARATION LOGIC
ASSERTIONS
JACOB THAMSBORG a , LARS BIRKEDAL, AND HONGSEOK YANG c
a,b

c

IT University of Copenhagen, Rued Langgaards Vej 7, DK-2300 København S, Denmark
e-mail address: {thamsborg, birkedal}@itu.dk
Wolfson Building, Parks Road, Oxford, OX1 3QD, UK
e-mail address: hongseok00@gmail.com
Abstract. Recently, data abstraction has been studied in the context of separation logic,
with noticeable practical successes: the developed logics have enabled clean proofs of tricky
challenging programs, such as subject-observer patterns, and they have become the basis of
efficient verification tools for Java (jStar), C (VeriFast) and Hoare Type Theory (Ynot). In
this paper, we give a new semantic analysis of such logic-based approaches using Reynolds’s
relational parametricity. The core of the analysis is our lifting theorems, which give a sound
and complete condition for when a true implication between assertions in the standard
interpretation entails that the same implication holds in a relational interpretation. Using
these theorems, we provide an algorithm for identifying abstraction-respecting client-side
proofs; the proofs ensure that clients cannot distinguish two appropriately-related module
implementations.

1. Introduction
Data abstraction is one of the key design principles for building computer software, and it
has been the focus of active research from the early days of computer science. Recently,
data abstraction has been studied in the context of separation logic [26, 7, 22, 27, 12],
with noticeable practical successes: the developed logics have enabled clean proofs of tricky
challenging programs, such as the subject-observer pattern, and they have become the basis
of efficient verification tools for Java (jStar [14]), C (VeriFast [18]) and Hoare Type Theory
(Ynot [23]).
In this paper, we give a new semantic analysis of these logic-based approaches using
Reynolds’s relational parametricity. Our techniques can be used to prove representation
independence, i.e., that clients cannot distinguish between related module implementations,
a consequence that we would expect from using data abstraction, but (as we shall see) a
consequence that only holds for certain good clients.
1998 ACM Subject Classification: F.3.1.
Key words and phrases: separation logic, data abstraction, relational interpretation.

l

LOGICAL METHODS
IN COMPUTER SCIENCE

c
DOI:10.2168/LMCS-8(3:22)2012

CC

J. Thamsborg, L. Birkedal, and H. Yang
Creative Commons

2

J. THAMSBORG, L. BIRKEDAL, AND H. YANG

Interface Specification
{1֒→ }init{a} {a}nxt{b} {b}fin{1֒→ }
{a}inc{a}
{b}dec{b}
Two Implementations of a Counter
def

init1 = [1]:=0

def

nxt1 = skip

def

def

fin1 = skip

def

inc1 = [1]:=[1]+1 dec1 = [1]:=[1]−1
def

def

def

init2 = [1]:=0
nxt2 = [1]:=−[1] fin2 = [1]:=−[1]
def
def
inc2 = [1]:=[1]+1 dec2 = [1]:=[1]+1
Client-side Proof Attempts
{1֒→ } init; {a}
inc; {a}
nxt; {b}
dec; {b}
fin {1֒→ }

{1֒→ } init; {a}
inc; {a}
nxt; {b}
[1]:=[1]−1; {???}

Figure 1: Two-stage Counter
Logic-based Data Abstraction. The basic idea of the logic-based approaches is that the
private states of modules are exposed to clients only abstractly using assertion variables [7],
also known as abstract predicates [26]1. For concreteness, we consider a two-stage counter
module and client programs in Figure 1. The module realizes a counter with increment
and decrement operations, called inc and dec. An interesting feature is that the counter
goes through two stages in its lifetime; in the first stage, it can perform only the increment
operation, but in the second, it can only run the decrement. The interface specification in
the figure formalizes this intended behavior of the counter using assertion variables a and b,
where a means that the counter is in the first stage and b that the counter is in the second.
The triple for init says that the initialization can turn the assertion 1֒→ , denoting heaps
with cell 1, to the assertion variable a, which describes an abstract state where we can only
call inc or nxt (since a is the precondition of only those operations). The abstract state a
can be changed to b by calling nxt, says the triple for the nxt operation. In b we are allowed
to run dec but not inc. Finally, fin can turn the abstract state b back to 1֒→ . Note that
by using a and b, the interface specification does not expose the private state of the module
to the client. It reveals only partial information about the private state of the module; here
it is whether the private state is in the first or the second stage. The flexibility afforded by
revealing partial information is very useful in applications; see the examples mentioned in
the references above.
In these logic-based approaches, proof attempts for clients of a module can succeed only
when they are given with respect to the abstract interface specification, without making
any further assumptions on assertion variables. For instance, the proof attempt on the
bottom left of Figure 1 is successful, whereas the bottom right one is not, because the latter
1Abstract predicates do take arguments, though. We conjecture that it is equally expressive to use an

assertion variable for each combination of abstract predicate and concrete arguments.

TWO FOR THE PRICE OF ONE: LIFTING SEPARATION LOGIC ASSERTIONS

3

assumes that the assertion variable b entails the allocatedness of cell 1. This is not so, even
when the entailment holds for an actual definition of b.
Representation Independence. In this paper, we give a condition on client-side proofs that
ensure representation independence: take a client with a standard proof of correctness that
satisfies this condition and two implementations of a module; if we can relate the heap-usage
of the two modules in a way preserved by the module operations, then the client gives the
same result with both modules. To relate the heap-usage, we need to give, for each assertion
variable, a relation on heaps and verify that the module operations respect these relations
— the coupling relations.
As an example, consider the left-hand side client in Figure 1. The proof of the specification
{1֒→ } init; inc; nxt; dec; fin {1֒→ }
satisfies the forthcoming condition on client-side proofs. Also, we have two implementations
of the counter module that the client makes use of; both use cell 1 to represent their private
states, but in different ways — the first stores the current value of the counter, but the
second stores the current value or its negative version, depending on whether it is in the
first stage or the second. Accordingly, we give the two coupling relations:
def

ra = {(h1 , h2 ) | 1∈ dom(h1 )∩ dom(h2 ) ∧ h1 (1)=h2 (1)}
def
rb = {(h1 , h2 ) | 1∈ dom(h1 )∩ dom(h2 ) ∧ h1 (1)=−h2 (1)}
It is easy to see that all module operations preserve these coupling relations. If, say,
(h1 , h2 ) ∈ rb , then we have h1 (1) = n and h2 (1) = −n for some n and so (h1 [1 7→
n − 1], h2 [1 7→ −n + 1]) ∈ rb too; hence the decrement operations of the modules respect
the coupling relation. By Theorem 6.1 we now get that the client specification is valid also
in a binary reading: if we take any two heaps and run the client with one module in the
first and with the other module in the second then we will end up with two heaps holding
the same value in cell 1 — provided that we started out with two such. Indeed, the binary
reading of the assertion 1֒→ is
{(h1 , h2 ) | 1∈ dom(h1 ) ∩ dom(h2 ) ∧ h1 (1) = h2 (1)}
which incidentally coincides with ra .
It is worthwhile to emphasize that this is not a consequence of the standard unary
reading of the specification of the client: due to the existentially quantified content of cell
1, running with the one module could yield different contents of cell 1 than running with
the other module, even if the contents are initially the same. On the other hand, it is the
presence of this quantification that makes the binary reading worthwhile: if our client had
a more exhaustive specification, say
{1֒→0} init; inc; nxt; dec; fin {1֒→0},
then the standard unary reading suffices for representation independence and the binary
reading would provide no news. Often, though, the more exhaustive specification will be
harder to prove, in particular for verification tools.

4

J. THAMSBORG, L. BIRKEDAL, AND H. YANG

Interface Specification
{1֒→ }init{1֒→ ∧ a ∗ b}
{1֒→ }fin{1֒→ }
{1֒→ ∗ a ∨ 1֒→ ∗ b}badfin{1֒→ }
Two Implementations
def

def

def

def

def

def

init1 = skip fin1 = skip badfin1 = [1]:=1
init2 = skip fin2 = skip badfin2 = [1]:=2
Two Client-side Proofs
{1֒→ }
init;
{1֒→ ∧ a ∗ b}
{1֒→ }
fin
{1֒→ }

{1֒→ }
init;
{1֒→ ∧ a ∗ b}
{1֒→ ∗ a ∨ 1֒→ ∗ b}
badfin
{1֒→ }

Figure 2: Good or Bad Client-side Proofs
The Rule of Consequence and Lifting. In earlier work [10] we were able to prove such a
representation independence result for a more restricted form of logical data abstraction,
namely one given by frame rules rather than general assertion variables. Roughly speaking,
frame rules use a restricted form of assertion variables that are not exposed to clients at
all, as can be seen from some models of separation logic in which frame rules are modelled
via quantification over semantic assertions [9]. This means that the rules do not allow the
exposure of even partial information about module internals. (On the other hand, frame
rules implement information hiding, because they completely relieve clients of tracking the
private state of a module, even in an abstracted form.) Our model in [10] exploited this
restricted use of assertion variables, and gave relational meanings to Hoare triple specifications, which led to representation independence.
Removing this restriction and allowing assertion variables in client proofs turned out
to be very challenging. The challenge is the use of the rule of consequence in client-side
proofs; this has implications between assertions (possibly containing assertion variables) as
hypotheses, and such do not always lift, i.e., they may hold in the standard, unary reading
of assertion whilst failing in the binary reading. In this paper, we provide a sound and, in
a certain sense, complete answer to when the lifting can be done.
For instance, consider the example in Figure 2. Our results let us conclude that the
client-side proof on the left is good but the one on the right is bad; hence we expect to
derive representation independence only from the former. The client on the left calls init
and ends with the post-condition (1֒→ ∧ a ∗ b). Since (1֒→ ∧ a ∗ b) =⇒ 1֒→ is true in the
standard interpretation, the rule of consequence can be applied to yield the precondition of
fin, which can be called, ending up with the postcondition (1֒→ ). The key point here is
the implication used in the rule of consequence. Our results imply that this implication can
indeed be lifted to an implication between relational meanings of assertions (1֒→ ∧a∗b) and
1֒→ (Theorem 4.5 in Section 4). They also entail that this lifting implies the representation

TWO FOR THE PRICE OF ONE: LIFTING SEPARATION LOGIC ASSERTIONS

5

independence theorem. The coupling relations
def

ra = {(h1 , h2 ) | 1∈ dom(h1 )}
def
rb = {(h1 , h2 ) | 1∈ dom(h2 )}
are preserved by the modules: the relational meaning of 1֒→ ∗a ∨ 1֒→ ∗b is empty; note that
separating conjunctions binds more tightly than conjunction and disjunction. Hence the
client on the left should give the same result for both modules and, indeed, both init1 ; fin1
and init2 ; fin2 are the same skip command.
The client on the right also first calls init and then uses the rule of consequence. But
this time our results say that a true implication (1֒→ ∧ a ∗ b) =⇒ (1֒→ ∗ a ∨ 1֒→ ∗ b) in
the rule of consequence does not lift to an implication between relational meanings of the
assertions: the pair of heaps ([1 7→ 0], [1 7→ 0]) belong to the left hand side but possibly not
to the right if the pair ([], [1 7→ 0]) is in the interpretation of a and the pair ([1 7→ 0], [])
is in the interpretation of b; see Example 4.9 for details. Because of this failure, the proof
of the client does not ensure representation independence. In fact, the client can indeed
distinguish between the two module implementations — when the client is executed with
the first module implementation, the final heap maps address 1 to 1, but when the client is
executed with the second, the final heap maps address 1 to 2.
Note that we phrase the lifting only in terms of semantically true implications, without
referring to how they are proved. By doing so, we make our results relevant to automatic
tools that use the semantic model of separation logic to prove implications, such as the ones
based on shallow embeddings of the assertion logic [23, 16].
To sum up, the question of whether representation independence holds for a client with
a proof comes down to whether, in the proof, the implications used in the rule of consequence
can be lifted to a relational interpretation. In this paper, we give a sound and, in a certain
sense, complete characterization of when that holds.
It is appropriate to remark already here, that although we extend our assertions with
assertion variables we also restrict them to contain neither ordinary nor separating implication. And, in the end, we consider only a fragment of those. Details are given in Sections 2
and 4; here we just remark that the assertions we do study are not unlike the ones considered in the tools mentioned in the beginning of this introduction, in particular jStar. Also
we use intuitionistic separation logic as we envision a language with garbage collection; this,
too, is in line with the jStar tool.
The rest of the paper is organized as follows:
Sections 2 and 3: give the meanings of assertions, both the standard and relational
meanings. Indeed, we give, for any n ∈ PosInt, the n-ary meaning of assertions as n-ary
relations on the set of heaps. These relations are intuitionistic, i.e., they are upward
closed relations with respect to heap extension.
Section 4: contain the main technical contributions of the paper. We give, for assertions
of a particular form, a sound and, in a certain sense, complete answer to the question of
when we may lift implications between assertions from the standard, unary meaning to
the binary meaning.
Section 5: has the curious spinoff result that an implication between assertions holds
for arbitrary arity if and only if it holds for reasons of parametric polymorphism in a
particular sense.

6

J. THAMSBORG, L. BIRKEDAL, AND H. YANG

Section 6: returns to the main line of development; this is where we show that a clientside proof yields representation independence if it uses the rule of consequence only with
implications that lift.
Section 7: concludes the paper.
Proofs are found in the appendices, the main text only give details for a few examples.
2. Semantic Domain
In the following section we will define the meaning of an assertion to be an n-ary relation on
heaps. To formalize this relational meaning, we need a semantic domain IReln of relations,
which we define and explain in this section.
Let Heap be the set of finite partial functions from positive integers to integers (i.e.,
def
Heap = PosInt →fin Int), ranged over by f, g, h. This is a commonly used set for modelling
heaps in separation logic, and it has a partial commutative monoid structure ([], ·), where
[] is the empty heap and the · operator combines disjoint heaps:

f ∪g
if dom(f ) ∩ dom(g) = ∅
def
def
[] = ∅, f · g =
undefined otherwise

The operator · induces a partial order ⊑ on Heap, modelling heap extension, by f ⊑ g iff
g = f · h for some h.
We also consider the + operator for combining possibly-overlapping but consistent
heaps, and the − operator for subtracting one heap from another:

f ∪g
if ∀l∈ dom(f ) ∩ dom(g). f (l)=g(l)
def
f +g =
undefined otherwise

f (l)
if l ∈ dom(f ) \ dom(g)
def
(f − g)(l) =
undefined otherwise

We call an n-ary relation r ⊆ Heapn upward closed iff (f1 , . . . , fn ) ∈ r∧(∀i. fi ⊑ gi ) =⇒
(g1 , . . . , gn ) ∈ r.
Definition 2.1. IReln is the family of upward closed n-ary relations on heaps.
Note that IRel1 consists of upward closed sets of heaps, which are frequently used to
interpret assertions in separation logic for garbage-collected languages. We call elements of
IRel1 predicates and denote them by p, q.
For every n ≥ 1, domain IReln has a complete lattice structure: join and meet are given
by union and intersection, bottom is the empty relation, and top is Heapn . The domain
also has a semantic separating conjunction connective defined by
def

(f1 , .., fn ) ∈ r ∗ s ⇐⇒ ∃(g1 , .., gn ) ∈ r. ∃(h1 , .., hn ) ∈ s.
(g1 , .., gn ) · (h1 , .., hn ) = (f1 , .., fn ).
Here we use the component-wise extension of · for tuples. Intuitively, a tuple is related by
r ∗ s when it can be split into two disjoint tuples, one related by r and the other by s.
def
The domain IRel1 of predicates is related to IReln for every n, by the map ∆n =
λp.{(f, . . . , f ) | f ∈ p}↑ , where ↑ is the upward closure on relations. Note that each
predicate is turned into an n-ary identity relation on p modulo the upward closure. This
map behaves well with respect to the structures discussed on IRel1 and IReln , as expressed
by the lemma below:

TWO FOR THE PRICE OF ONE: LIFTING SEPARATION LOGIC ASSERTIONS

7

Lemma 2.2. Function ∆n preserves the complete lattice structure and the ∗ operator.
For every n ≥ 1, the domain IReln has further structure: it has standard, semantic
separating implication and upwards-closed implication; as such, it is a complete BI algebra
[8]. Unfortunately, the above lemma fails for both implications. And that lemma is the
pivot of the upcoming results; it is the basic link between the unary and binary (and n-ary)
readings of assertions. This is why we leave out these connectives in our assertions in the
next section; it is a fundamental limitation in our approach.
3. Assertions and Relational Semantics
Let Var and AVar be disjoint sets of normal variables x, y, ... and assertion variables a, b, ...,
respectively. Our assertions ϕ are from separation logic, and they conform to the following
grammar:
E ::= x | 0 | 1 | E + E | . . .
P ::= E ֒→ E | . . .
ϕ ::= P | a | ϕ ∗ ϕ | true | ϕ ∧ ϕ | false | ϕ ∨ ϕ
| ∀x. ϕ | ∃x. ϕ
In the grammar, E is a heap-independent expression, and P is a primitive predicate, which
in the standard interpretation denotes an upward closed set of heaps. For instance, E֒→E ′
means heaps containing cell E with contents E ′ . The dots in the grammar indicate possible
extensions of cases, such as multiplication for E and inductive predicates for P . We will
use the abbreviation E֒→ for ∃y.E֒→y.
An assertion ϕ is given a meaning [[ϕ]]nη,ρ ∈ IReln as an n-ary relation on heaps, where
the arity n is a parameter of the interpretation. Here environment η maps normal variables
in ϕ to integers, and ρ maps assertion variables in ϕ to n-ary relations in IReln . When
ϕ does not contain any assertion variables, we often omit ρ and write [[ϕ]]nη , because the
meaning of ϕ does not depend on ρ. We will make use of unary and binary semantics most
places, but in Section 5 we will explore higher arities as well.
We define the semantics of ϕ, using the complete lattice structure and the ∗ operator
of the domain IReln ; see Figure 3. Note that the relational semantics of primitive predicates
is defined by embedding their standard meanings via ∆n . In fact, this embedding relationship holds for all assertions without assertion variables, because ∆n preserves the semantic
structures of the domains (Lemma 2.2):
Lemma 3.1. For all ϕ and η, ρ, ρ′ , if ∆n (ρ(a)) = ρ′ (a) for every a ∈ AVar, we have that
∆n ([[ϕ]]1η,ρ ) = [[ϕ]]nη,ρ′ .
We write ϕ |=n ψ to mean that [[ϕ]]nη,ρ ⊆ [[ψ]]nη,ρ holds for all environments η, ρ. If
n=1, this reduces to the standard semantics of assertions in separation logic. We will use
the phrase “ϕ =⇒ ψ is n-ary valid” to mean that ϕ |=n ψ holds. In addition, we write
ϕ |=nη ψ for a fixed η to mean that [[ϕ]]nη,ρ ⊆ [[ψ]]nη,ρ holds for all environments ρ; we say that
“ϕ =⇒ ψ is n-ary η-valid” if this is true.
4. Lifting Theorems and Completeness
W V
We call an assertion ϕ simple if it is of the form ( Ii=1 Jj=1 ϕ(i,j) ∗ a(i,j) ), where a(i,j) is a
vector of assertion variables and ϕi,j is an assertion not containing any assertion variables.
We will consider the question of lifting an implication between simple assertions ϕ, ψ to a
binary relational interpretation: when does ϕ |=1 ψ imply that ϕ |=2 ψ?

8

J. THAMSBORG, L. BIRKEDAL, AND H. YANG

def

def

[[P ]]nη,ρ = ∆n (LP Mη ) [[ϕ ∗ ψ]]nη,ρ = [[ϕ]]nη,ρ ∗ [[ψ]]nη,ρ
def

[[a]]nη,ρ = ρ(a)
def

[[true]]nη,ρ = Heapn
def

[[false]]nη,ρ = ∅

def

[[ϕ ∧ ψ]]nη,ρ = [[ϕ]]nη,ρ ∩ [[ψ]]nη,ρ
def

[[ϕ ∨ ψ]]nη,ρ = [[ϕ]]nη,ρ ∪ [[ψ]]nη,ρ
def T
[[∀x.ϕ]]nη,ρ = v∈Int [[ϕ]]nη[x7→v],ρ
def S
[[∃x.ϕ]]nη,ρ = v∈Int [[ϕ]]nη[x7→v],ρ

where LP Mη is the standard semantics of P as an upward closed set of heaps, which
satisfies:
LE֒→F Mη = {f | [[E]]η ∈ dom(f ) ∧ f ([[E]]η ) = [[F ]]η }.
Figure 3: Interpretation of Assertions
The simple assertions are a fragment of the assertions considered in the above section:
simple assertions are not, in general, closed under separating conjunction as the latter does
not distribute over conjunction, nor are quantified simple assertions necessarily simple. The
divide, however, between simple and non-simple assertions is not deep. The forthcoming
completeness result is intimately connected to the form of the assertions, but it is very
possible that the basic ideas from lifting could be applied to a larger fragment. We have not
considered that to any extent, however. It is worth mentioning that all assertions considered
in Section 1 are simple. On the other hand, for assertions ϕ1 , ϕ2 and ϕ3 with no assertion
variables and assertion variables a1 ,a2 and a3 , we do not, in general, have simplicity of an
assertion like


 
(ϕ1 ∗ a1 ) ∧ (ϕ2 ∗ a2 ) ∗ ϕ3 ∗ a3 .
It should be noted, that simple assertions include most of the important aspects of the
fragments of separation logic used by automatic program analysis tools. For instance, if we
ignore so called primed variables (which correspond to existentially-quantified variables), the
W
original SpaceInvader uses separation-logic formulas of the form Ii=1 (Pi,1 ∗ . . . ∗ Pi,ki ) [13],
and its
V most
W recent extension for handling a particular class of graph-like data structures
uses Jj=i Ii=1 (Pi,j,1 ∗ . . . ∗ Pi,j,ki,j ) [19]. Note that in both cases, either formulas are already
simple or they can be easily transformed to equivalent simple formulas. The assertions used
by the jStar tool [15] has neither ordinary implication, separating implication nor ordinary
conjunction and only quite restricted use of quantifiers. Since proofs obtained from such
tools are one target of our results, we argue that the restrictions imposed on assertions are
not unreasonable in terms of usage.
The starting point of our analysis is to realize that it is sufficient to study implications
of the form:
N
M
_
^
ψj ∗ bj,1 ∗ · · · ∗ bj,Nj
(4.1)
ϕi ∗ ai,1 ∗ · · · ∗ ai,Mi =⇒
i=1

j=1

where ϕi ’s and ψj ’s do not contain assertion variables, and no assertion variables occur only
on the right hand side of the implication.

Lemma 4.1. There is an algorithm taking simple assertions ϕ, ψ and returning finitely
many implications {ϕl =⇒ ψ l }l∈L , such that (a) ϕl =⇒ ψ l has the form (4.1) for all l ∈ L,
and (b) for any n ∈ {1, 2}, we have that ϕ |=n ψ holds iff ϕl |=n ψ l holds for all l ∈ L.

TWO FOR THE PRICE OF ONE: LIFTING SEPARATION LOGIC ASSERTIONS

9

The algorithm in the lemma is given in Appendix B.
Thus, in this section, we will focus on lifting implications of the form (4.1). Specifically,
we will give a complete answer to the following question: Given one such implication that is
η-valid in the unary interpretation for some environment η, can we decide if the implication
is η-valid in the binary interpretation merely by inspection of the layout of the assertion
variables? The answer will come in two parts. The first part, in Section 4.3, provides three
lifting theorems, each of which has a criterion on the variable layout that, if met, implies
that η-validity may be lifted regardless of the ϕi ’s and ψj ’s. The second part, in Section 4.4,
is a completeness theorem; it states that if the variables fail the criteria of all three lifting
theorems then there are choices of ϕi ’s and ψj ’s with no variables such that we have unary
but not binary validity.
This approach has pros and cons. Assume that we have an implication of the aforementioned form that is valid in the unary interpretation, and we would like to know if it
is valid in the binary interpretation too. Trying out the layout of the variables against the
criteria of the three lifting theorems is an easily decidable and purely syntactical process
– and if it succeeds then we have binary validity. If it fails, however, we are at a loss; we
know that there are ϕi ’s and ψj ’s with the same variable layout such that lifting fails but
we do not learn anything about our concrete implication. There is, however, an alternate
use of the theory below if the lifting criteria fail; we will elaborate on that in Section 6.
4.1. Notation. We need some notation that will S
accompany us throughout this section.
Consider an implication of the form (4.1). Let V = M
i=1 {ai,1 , . . . , ai,Mi } be the set of all left
hand side assertion variables, these include the right hand side assertion variables too by
assumption. Define Π : {1, . . . , M } → NatV and Ω : {1, . . . , N } → NatV by the following:
def

Π(i)(c) = |{k | ai,k ≡ c}|,

def

Ω(j)(c) = |{k | bj,k ≡ c}|.

These functions give vectors of assertion variable counts for each conjunct and disjunct.
For 1 ≤ i ≤ M and 1 ≤ j ≤ N we write Π(i) ≥ Ω(j) if we have Π(i)(c) ≥ Ω(j)(c) for each
variable c ∈ V , i.e., if conjunct i has the same or a greater number of occurrences of all
variables than disjunct j. We write Π(i)  Ω(j) if this fails, i.e., if there is c ∈ V such that
Π(i)(c) < Ω(j)(c). If a conjunct, say conjunct i, has no variables, i.e., if Π(i)(c) = 0 holds
for all c ∈ V , then we say it is empty; the same goes for the disjuncts.
We shall write − to denote ∃n, m. n֒→m, meaning heaps with at least one cell. On the
semantic side, we write [m] for m ∈ PosInt to denote the heap that stores 0 at location m
and nothing else. For m0 , ..., mn ∈ PosInt different we write [m0 , ..., mn ] for [m0 ] · ... · [mn ].
Finally we introduce a piece of sanity-preserving graphical notation. We depict an
implication of the form (4.1) as a complete bipartite graph with the conjuncts lined up on
the left hand side and the disjuncts on the right hand side. For any 1 ≤ i ≤ M and any
1 ≤ j ≤ N we draw a solid line from conjunct i to disjunct j if Π(i) ≥ Ω(j). We label that
line with all the c ∈ V such that Π(i)(c) > Ω(j)(c) if indeed there are any such. If, on the
other hand, Π(i)  Ω(j) then we draw a dashed line instead and label it with all the c ∈ V
such that Π(i)(c) < Ω(j)(c). Note that the drawing of edges depend solely on the layout of
the variables; the ϕi ’s and ψj ’s have no say in the matter. As an example, the implication
1֒→ ∧ a ∗ b =⇒ 1֒→ ∗ a ∨ 1֒→ ∗ b,

10

J. THAMSBORG, L. BIRKEDAL, AND H. YANG

which we shall look into in Example 4.9, is depicted as follows:
1֒→

a∗b

• ✿❴ ❴a ❴ •

1֒→ ∗ a

•

1֒→ ∗ b

☎
b ✿ ☎☎
✿☎☎
☎☎ ✿
b ☎☎
✿
☎

•

a

With a little experience, it is quite easy to check the conditions of the upcoming lifting
theorems by looking at the corresponding graph; the graphs expose the structure of the
assertions important to the proofs.
4.2. Strategy. We give a brief strategic overview before the onslaught. Consider an implication of the form (4.1). If the layout of the variables satisfy (at least) one of three
upcoming criteria then we know this: unary η-validity holds only if it holds for ‘obvious
reasons’. The latter is captured precisely in the Parametricity Condition but, loosely, it
says that there are 1 ≤ i ≤ M and 1 ≤ j ≤ N such that φi =⇒ ψj is η-valid in the unary
interpretation and such that Π(i) ≥ Ω(j). This is sufficiently parametric in the treatment
of assertion variables that it immediately implies binary η-validity and even n-ary η-validity
for any n.
The three criteria, as given in the next subsection, are rather technical; each is what it
takes for proof idea of the corresponding lifting theorem to go through. They are complete,
however: if the implication fails all three criteria then there are choices of ϕi ’s and ψj ’s
such that unary η-validity holds for ‘non-obvious reasons’; in particular such that binary
η-validity fails. Non-obvious reasons comes down to exploiting the limited arity in different
ways; we elaborate on that in Subsection 4.4.
4.3. Layouts that Lift. The following is a first example of a layout of variables that ensure
that for any choice of ϕi ’s and ψj ’s we get that unary η-validity of the implication yields
binary η-validity. That it holds is a consequence of Theorem 4.5 but we have spelled out a
concrete proof that will serve as a guide to the further development.
Example 4.2 (Shadow-Lift). For any four assertions ϕ1 , ϕ2 , ψ1 , ψ2 with no assertion variables and any appropriate environment η we have that unary η-validity of the following
implication implies binary η-validity:
ϕ1 ∗ a ∗ b

b
• ✽❴ ❴ ❴ •
b

ϕ2 ∗ a ∗ b ∗ b

•

✽ ✝✝✝
✽✝
✝✝ ✽
✝
✝
✽
✝✝
a

•

ψ1 ∗ a ∗ b ∗ b

ψ2 ∗ b ∗ b

Assume that we have unary η-validity. Before we go on to consider the binary case we derive
a simple unary consequence that does not involve assertion variables: For any h ∈ Heap with
subheaps h1 ⊑ h and h2 ⊑ h such that h1 ∈ [[ϕ1 ]]1η and h2 ∈ [[ϕ2 ]]1η we get that h2 ∈ [[ψ1 ]]1η
or that h2 ∈ [[ψ2 ]]1η .
To prove this, let h, h1 and h2 be as assumed. We build ρ : {a, b} → IRel1 by letting
ρ(a) = Heap and letting ρ(b) be the following union of sets of heaps:
{(h − h1 ) · [n, n + 1]}↑ ∪ {(h − h2 ) · [n]}↑ ∪ {[n + 1]}↑

TWO FOR THE PRICE OF ONE: LIFTING SEPARATION LOGIC ASSERTIONS

11

where n = max(dom(h) ∪ {0}) + 1. It is now immediate that h · [n, n + 1] lies in the
interpretation of both conjuncts since
h1 · (h − h1 ) · [n, n + 1] = h · [n, n + 1] = h2 · (h − h2 ) · [n] · [n + 1],
and so by our assumption on the original implication it must lie in the interpretation on
one of the disjuncts too. Suppose that we have
h · [n, n + 1] ∈ [[ψ1 ∗ a ∗ b ∗ b]]1η,ρ = [[ψ1 ]]1η ∗ ρ(b) ∗ ρ(b),
where the equality holds because ρ(a) = Heap is the unit for ∗. We then write h · [n, n + 1] =
g1 · g2 · g3 for g1 ∈ [[ψ]]1η and g2 , g3 ∈ ρ(b). But as g2 and g3 have disjoint domains we must
have (h − h2 ) · [n] ⊑ g2 and [n + 1] ⊑ g3 or the version with g2 and g3 swapped. In any case
we have that
dom(g1 ) = dom(h · [n, n+1]) \ (dom(g2 · g3 ))
⊆ dom(h · [n, n+1]) \ (dom(h−h2 ) ∪ {n, n+1})
= dom(h2 ).
But then we have g1 ⊑ h2 and since g1 ∈ [[ψ1 ]]1η we get h2 ∈ [[ψ1 ]]1η too. If we have
h · [n, n + 1] ∈ [[ψ2 ∗ b ∗ b]]1η,ρ we proceed similarly.
The above short proof is the crux of the example. It implies unary η-validity – this we
knew already – but also the binary η-validity. To see this, we pick an arbitrary environment
ρ : {a, b} → IRel2 , we take arbitrary (h1 , h2 ) ∈ [[ϕ1 ∗ a ∗ b ∧ ϕ2 ∗ a ∗ b ∗ b]]2η,ρ and we aim to
prove that (h1 , h2 ) ∈ [[ψ1 ∗ a ∗ b ∗ b ∨ ψ2 ∗ b ∗ b]]2η,ρ too. We split (h1 , h2 ) according to the
conjuncts. Because of Lemma 3.1 and the upward closedness condition of IRel2 , we can
write
(h1 , h2 ) = (g 1 , g1 ) · (g12 , g22 ) · (g13 , g23 )
for g1 ∈ [[ϕ1 ]]1η , (g12 , g22 ) ∈ ρ(a) and (g13 , g23 ) ∈ ρ(b). Also we can write
(h1 , h2 ) = (f 1 , f 1 ) · (f12 , f22 ) · (f13 , f23 ) · (f14 , f24 )
for f 1 ∈ [[ϕ2 ]]1η , (f12 , f22 ) ∈ ρ(a) and (f13 , f23 ), (f14 , f24 ) ∈ ρ(b). But now g1 + f 1 with subheaps
g1 and f 1 meet the conditions of the unary consequence from above, and so we get f 1 ∈ [[ψ1 ]]1η
or f 1 ∈ [[ψ2 ]]1η and the second splitting of (h1 , h2 ) shows that (h1 , h2 ) lie in the binary
interpretation of the first or second disjunct, respectively. Notice that neither g1 ∈ [[ψ1 ]]1η
nor g 1 ∈ [[ψ2 ]]1η would have worked since the first conjunct has too few variables, i.e.,
Π(1)  Ω(1) and Π(1)  Ω(2)
The simple idea justifies the odd choice of name: we attach to each occurrence of b in the
conjuncts a ‘shadow’ in such a way that any two shadows from different conjuncts overlap.
This means that the two occurrences of b in, say, the first disjunction must correspond to
occurrences of b in the same conjunct; in particular that conjunct must have at least two
occurrences. We attach no shadow to a, instead we remove a by instantiating to Heap; this
is because the second disjunct lacks an occurrence of a and hence we may fail to ‘peel off’
the entire shadow. Had a occurred as the single label of a dashed line, this removal would
have ‘introduced’ a solid line and the approach would fail.
Generalizing the unary consequence that served as the crucial stepping stone in the
above example we arrive at the following condition on our implications:
Definition 4.3 (Parametricity Condition). Assume that we have an implication of the
form (4.1) and an appropriate environment η. We say that the Parametricity Condition is

12

J. THAMSBORG, L. BIRKEDAL, AND H. YANG

satisfied if, for all h, h1 , . . . , hM ∈ Heap with hi ⊑ h and hi ∈ [[ϕi ]]1η for all 1 ≤ i ≤ M , it is
is the case that one (or both) of the following conditions hold:
(1) There are 1 ≤ i ≤ M and 1 ≤ j ≤ N such that hi ∈ [[ψj ]]1η and Π(i) ≥ Ω(j).
(2) There is 1 ≤ j ≤ N such that h ∈ [[ψj ]]1η and the j-th disjunct is empty.
Note that specializing the Parametricity Condition, henceforth just the PC, to an implication of the form treated in the above example yields the stated unary consequence
because no disjuncts are empty. The second option in the PC will be motivated later.
We emphasize that the PC may hold or may fail for any given combination of an
implication and environment η. But if it holds then we have binary η-validity; the proof in
case of the first option of the PC is an easy generalization of the latter half of the above
example:
Proposition 4.4. The PC implies binary η-validity.
We arrive now at the first lifting theorem. It is a generalization of the former half of
Example 4.2; the proof of the theorem has a lot more details to it than the example but
the overall idea is the same. The theorem states a criterion on the layout of the variables
that, if met, means that unary η-validity implies the PC and hence also binary η-validity.
The criterion is, loosely, that we can remove all variables that occur as labels of solid lines
without introducing new solid lines and without emptying any disjuncts:
Theorem 4.5 (Shadow-Lift). Unary η-validity of an implication implies the PC if each
dashed line is labeled with at least one variable which is not a label on a solid line and each
disjunct has an occurrence of a variable that is not a label on a solid line. Spelling it out in
symbols, we require, with L = {(i, j) | 1 ≤ i ≤ M ∧ 1 ≤ j ≤ N }, that

and

∀(i, j) ∈ L. Π(i)  Ω(j) =⇒
∃c ∈ V. Π(i)(c) < Ω(j)(c) ∧

∀(k, l) ∈ L. Π(k) ≥ Ω(l) =⇒ Π(k)(c) = Ω(l)(c)
∀1 ≤ j ≤ N. ∃c ∈ V. Ω(j)(c) > 0 ∧

∀(k, l) ∈ L. Π(k) ≥ Ω(l) =⇒ Π(k)(c) = Ω(l)(c) .

As motivation for the next lifting theorem, we note that the variable layout criterion of
the above theorem fails if one or more disjuncts are empty. Correspondingly, we never touch
upon the second option of the PC. But there are variable layouts with empty disjuncts that
ensure lifting:
Example 4.6 (Balloon-Lift). For any four assertions ϕ1 , ϕ2 , ψ1 , ψ2 with no assertion variables and any appropriate environment η we have that unary η-validity of the following
implication implies binary η-validity:
ϕ1 ∗ a

b
• ✽❴ ❴ ❴ •
a

ϕ2 ∗ a ∗ b

•

✽✽ ✝✝
✽✽ ✝✝
✝✽
✝✝ ✽✽✽
✝
✽
✝✝
a,b

•

ψ1 ∗ a ∗ b

ψ2

Assume unary η-validity. As in Example 4.2 we derive a unary consequence as an intermediate result: For any h ∈ Heap with subheaps h1 ⊑ h and h2 ⊑ h such that h1 ∈ [[ϕ1 ]]1η and
h2 ∈ [[ϕ2 ]]1η we have that either h2 ∈ [[ψ1 ]]1η or h ∈ [[ψ2 ]]1η .

TWO FOR THE PRICE OF ONE: LIFTING SEPARATION LOGIC ASSERTIONS

13

To prove this, let h, h1 and h2 be as assumed. We construct ρ : {a, b} → IRel1 by letting
ρ(a) = Heap and ρ(b) = {h − h2 }↑ . We get that
h ⊒ h1 ∈ [[ϕ1 ]]1η = [[ϕ1 ]]1η ∗ Heap = [[ϕ1 ∗ a]]1η,ρ ,
and
h = h2 · (h − h2 )
∈ [[ϕ2 ]]1η ∗ ρ(b) = [[ϕ2 ]]1η ∗ Heap ∗ ρ(b) = [[ϕ2 ∗ a ∗ b]]1η,ρ .
This means that h must lie in the interpretation of one of the disjuncts. If it is the first, we
inspect the interpretation and get that
h = g1 · g2 · g3
for

g1 ∈ [[ψ1 ]]1η ,

g2 ∈ Heap and g3 ⊒ h−h2 . It means that
dom(g1 ) = dom(h) \ dom(g2 · g3 ) ⊆ dom(h) \ dom(g3 )
⊆ dom(h) \ dom(h − h2 ) = dom(h2 )

which implies that g1 ⊑ h2 and so h2 ∈ [[ψ1 ]]1η . If, on the other hand, h lies in the interpretation of the second disjunct then we are done immediately.
Now we prove the claim of binary η-validity. We pick an arbitrary environment ρ :
{a, b} → IRel2 , we take arbitrary (h1 , h2 ) ∈ [[ϕ1 ∗ a ∧ ϕ2 ∗ a ∗ b]]2η,ρ and we must prove that
(h1 , h2 ) ∈ [[ψ1 ∗ a ∗ b ∨ ψ2 ]]2η,ρ too. We write
(h1 , h2 ) = (g 1 , g1 ) · (g12 , g22 )
for g1 ∈ [[ϕ1 ]]1η and (g12 , g22 ) ∈ ρ(a), and
(h1 , h2 ) = (f 1 , f 1 ) · (f12 , f22 ) · (f13 , f23 )
for f 1 ∈ [[ϕ2 ]]1η , (f12 , f22 ) ∈ ρ(a) and (f13 , f23 ) ∈ ρ(b). But now g 1 + f 1 with subheaps g1 and
f 1 satisfies the above properties and so we get f 1 ∈ [[ψ1 ]]1η or g1 + f 1 ∈ [[ψ2 ]]1η . If f 1 ∈ [[ψ1 ]]1η
holds then the second splitting of (h1 , h2 ) shows that (h1 , h2 ) is in the interpretation of
the first disjunct. If g1 + f 1 ∈ [[ψ2 ]]1η , we are done too, since we may write (h1 , h2 ) =
(g1 + f 1 , g1 + f 1 ) · (e1 , e2 ) for some (e1 , e2 ) ∈ Heap2 and so (h1 , h2 ) lies in the interpretation
[[ψ2 ]]2η = ∆([[ψ2 ]]1η ) of the second conjunct.
Once again, the underlying idea is simple: we attach ‘shadows’ to occurrences of variables, but this time we stay within the the original heap. This is quite inhibitory as we
may have to use the empty heap as shadow. Again we remove a variable (in general a set
of variables) by instantiating to Heap but the remaining variable (in general the remaining
set of variables) must satisfy quite restrictive demands.
Just as we did for Example 4.2 we may generalize the former half of this example
yielding Theorem 4.7 below. The latter half of the example, on the other hand, constitutes
an example of the approach of the proof of Proposition 4.4 in case we run into the second
option of the PC. Note also that specializing the PC to an implication of the form considered
in the example yields the stated unary consequence.
Theorem 4.7 (Balloon-Lift). Unary η-validity of an implication implies the PC if there is
a subset B ⊆ V with the following three properties. First, each conjunct has at most one
occurrence of a variable from B, i.e.,
X
∀1 ≤ i ≤ M.
Π(i)(c) ≤ 1.
c∈B

14

J. THAMSBORG, L. BIRKEDAL, AND H. YANG

Second, each disjunct is empty or has exactly one occurrence of a variable from B, i.e.,
X
X
∀1 ≤ j ≤ N.
Ω(j)(c) = 0 ∨
Ω(j)(c) = 1.
c∈V

c∈B

Third, each dashed line must have a label from B. That is, when L = {(i, j) | 1 ≤ i ≤
M ∧ 1 ≤ j ≤ N },
∀(i, j) ∈ L. Π(i)  Ω(j) =⇒ ∃c ∈ B. Π(i)(c) < Ω(j)(c).
One thing to note about the theorem is that if we have no empty disjuncts, none of the
variables in the subset B ⊆ V can be labels of a solid line. In particular, the conditions of
Theorem 4.5 are met, so the above theorem is really only useful if one or more disjuncts are
empty. A simple but pleasing observation is that this theorem is applicable if all conjuncts
and all disjuncts have at most a single occurrence of any assertion variable; in that case,
we can just choose B = V above.
The final lifting theorem captures the oddities of the special case of just one conjunct:
Theorem 4.8 (Lonely-Lift). Unary η-validity of an implication implies the PC if there is
just one conjunct, i.e., M =1, and all lines are solid, i.e., Π(1) ≥ Ω(j) for all 1 ≤ j ≤ N .
4.4. Completeness. It is now time for examples of implications that do not lift, i.e.,
that are valid in the unary interpretation but not in the binary. The first is based on the
following observation: If h ∈ [[1֒→ ]]1η and h ∈ p∗q for h ∈ Heap and p, q ∈ IRel1 then we have
h ∈ [[1֒→ ]]1η ∗p or h ∈ [[1֒→ ]]1η ∗q. This is because we must have [1 7→ n] ⊑ h for some n ∈ Int
and so writing h = h1 · h2 with h1 ∈ p and h2 ∈ q gives us [1 7→ n] ⊑ h1 or [1 7→ n] ⊑ h2 .
But this line of argument breaks down if we change to binary reading. We have, e.g.,
([1], [1]) ∈ [[1֒→ ]]2η and ([1], [1]) ∈ {([1], [])}↑ ∗ {([], [1])}↑ but both [[1֒→ ]]2η ∗ {([1], [])}↑ and
[[1֒→ ]]2η ∗ {([], [1])}↑ are empty. We can recast this as an implication that cannot be lifted:
Example 4.9 (Fan-Counter). This implication is valid on the unary but not on the binary
level:
1֒→ • ✿❴ ❴a ❴ • 1֒→ ∗ a
✿ ☎☎☎
✿☎☎
☎☎ ✿
☎
b ☎
✿
☎
b

a∗b

•

a

•

1֒→ ∗ b

First we argue that the implication holds on the unary level. Let ρ : {a, b} → IRel1 be an
arbitrary environment of upwards closed sets of heaps to a and b. Let h ∈ Heap be arbitrary
and assume that
h ∈ [[1֒→ ∧ (a ∗ b)]]1η,ρ = [[1֒→ ]]1ρ ∩ (ρ(a) ∗ ρ(b)).
By the above observation we get either h ∈ [[1֒→ ]]1η ∗ ρ(a) or h ∈ [[1֒→ ]]1η ∗ ρ(b) which
matches the right hand side of the implication.
Now we move on to prove that the implication fails on the binary level. Define
an environment ρ : {a, b} → IRel2 by ρ(a) = {([1], [])}↑ and ρ(b) = {([], [1])}↑ . Then,
[[1֒→ ∧ a ∗ b]]2η,ρ = [[1֒→ ]]2η,ρ ∩ (ρ(a) ∗ ρ(b)), which contains the pair ([1], [1]). But, as observed, both disjuncts have empty binary interpretations.

TWO FOR THE PRICE OF ONE: LIFTING SEPARATION LOGIC ASSERTIONS

15

An observation of similar nature is that for p ∈ IRel1 we have either p = Heap or
p ⊆ [[−]]1η = {[m7→n] | m ∈ PosInt, n ∈ Int}↑ because if p 6= Heap then it cannot contain
the empty heap. On the binary level, however, we have Heap2 6= {([1], [])}↑ * [[−]]2η =
{([m7→n], [m7→n]) | m ∈ PosInt, n ∈ Int}↑ . One consequence is this:
Example 4.10 (Bridge-Counter). This implication is valid on the unary but not on the
binary level:
a
− ∗ a ∗ b • ✾❴ ❴ ❴ • − ∗ a ∗ a
✾✾ ✆✆
✾✾ ✆✆
✆✾
✆✆ ✾✾✾
✆
✾
✆✆
•❴ ❴ ❴•
a

a∗a

b

−∗−∗b

First we argue that the implication holds on the unary level. Let ρ : {a, b} → IRel1 be an
arbitrary environment that assigns upwards closed sets of heaps to each of the two variables.
We branch on the value of ρ(a). If ρ(a) 6= Heap then we have ρ(a) ⊆ [[−]]1η which again
means that the first conjunct directly implies the second disjunct. If ρ(a) = Heap holds, we
get that
[[− ∗ a ∗ b]]1η,ρ = [[−]]1η,ρ ∗ Heap ∗ ρ(b) = [[−]]1η,ρ ∗ ρ(b)
⊆ [[−]]1η,ρ = [[−]]1η,ρ ∗ Heap ∗ Heap = [[− ∗ a ∗ a]]1η,ρ
because Heap is the unit for ∗. Hence we get that the first conjunct implies the first disjunct
and we have proved that the implication holds unarily.
Now we prove that the implication fails on the binary level. Define an environment
ρ : {a, b} → IRel2 by ρ(a) = {([1], [])}↑ ∪ {([2], [2])}↑ and ρ(b) = Heap2 . Observe now that
([1, 2], [2]) = ([2], [2]) · ([1], []) · ([], []), which implies that ([1, 2], [2]) ∈ [[− ∗ a ∗ b]]2η,ρ . From
the rewriting ([1, 2], [2]) = ([1], []) · ([2], [2]), we get ([1, 2], [2]) ∈ [[a ∗ a]]2η,ρ too and so this
pair of heaps lies in the interpretation of the left hand side. But it does not belong to
the interpretation of either disjunct. An easy – if somewhat indirect – way of realizing
this is to note that any pair of heaps in either [[−]]2η,ρ or in [[a ∗ a]]2η,ρ must have a second
component with nonempty domain. But then any pair of heaps in the interpretation of
either disjunct must have a second component with a domain of at least two elements. In
particular, neither can contain the pair ([1, 2], [2]).
In principle, the above two observations are all that we need to prove completeness.
Or, phrased differently, assume that we have a layout of variables that fail the criteria of
all three lifting theorems; by applying one of the two observations, we can then build a
concrete implication with that variable layout and with unary but not binary validity.
Having said that, the territory to cover is huge; the full completeness proof is a lengthy
and rather technical journey, the details of which do not provide much insight. We supply
it as a series of lemmas in Appendix D; these include generalizations of Example 4.9 and
Example 4.10 above. If one verifies the lemmas in the order listed and apply them as
sketched then it is feasible, if not exactly easy, to prove the following:
Theorem 4.11 (Completeness). If a variable layout meets none of the criteria in Theorems
4.5, 4.7 and 4.8, then there are choices of ϕi ’s and ψj ’s with no variables such we have unary
but not binary validity.

16

J. THAMSBORG, L. BIRKEDAL, AND H. YANG

4.5. Future Work: Supported Assertions. By now, we have given a complete division
of the possible layouts of variables into those that lift and those that do not. The divide is
technical; without some understanding of the underlying proofs, it is hard to get an intuitive
feel for it.
One way to simplify would be to consider supported assertions. A n-ary relation
r ∈ IReln is supported if, for every f ∈ Heapn , it holds that g1 ⊑ f and g2 ⊑ f and
g1 , g2 ∈ r together implies the existence of g ∈ r with g ⊑ g1 and g ⊑ g2 . In an intuitionistic setting, the supported assertions play the role that the precise assertions do in a
classical, non-intuitionistic setting: they validate reasoning about the resource invariant in
the Hypothetical Frame Rule [25] and about shared resources in concurrent separation logic
[11]. The problems we face here appear reminiscent and a natural question is this: how
about restricting assertion variables to supported assertions?
We have not investigated this in any detail, but initial findings suggest that this would
simplify matters, maybe extensively so. The counter-example given in Example 4.9 still
holds, so it is not the case that everything lifts, but the counter-example of Example 4.10
breaks. The central proof of Theorem 4.5 uses non-supported assertions; on the other hand,
if r ∈ IReln is supported then either r ∗ r is empty or we have r = Heapn so maybe we could
restrict to conjuncts with at most one occurrence of each assertion variable.
Along the same lines, it would be interesting to revisit the challenges in a classical,
non-intuitionistic setting. This, too, is left for future work with the one comment that the
counter-example given in Example 4.9 persists.
5. Higher Arities and Parametricity
We saw in Proposition 4.4 that the PC implies binary η-validity of an implication. It is
easy to show that the PC also implies unary η-validity, either directly or by observing that
binary implies unary. A natural question to ask is whether we can reverse this. Example 4.9
shows that unary validity does not entail the PC, because the latter fails for that concrete
implication. But as binary validity fails too, we could hope that binary validity would
enforce the PC. Unfortunately, this is not the case, as demonstrated by the implication
1֒→ ∧ a ∗ a ∗ b =⇒ 1֒→ ∗ a ∨ 1֒→ ∗ b.
Here the PC is the same as for Example 4.9 and hence still is not true, but we do have
binary validity. We do not, however, have ternary validity but the example could easily be
scaled: having n occurrences of a in the second conjunct means n-ary but not n + 1-ary
validity for any n ≥ 1. In summary, we have seen that for any n ≥ 1 we can have n-ary
validity whilst the PC fails.
What does hold, however, is the following:
Theorem 5.1. For an implication of the form (4.1) and an appropriate environment η we
have that n-ary η- validity implies the PC if n ≥ max{2, M1 , . . . , MM }.
Notice how this fits nicely with the above example: with n occurrences of a we have
n-ary validity but we need (n+1)-ary validity to prove the PC since there is also a single
b. The proof is in Appendix E, and reuses techniques from the proofs of Theorems 4.5 and
4.7.
By an easy generalization of Proposition 4.4 we have the following corollary to the
above theorem:

TWO FOR THE PRICE OF ONE: LIFTING SEPARATION LOGIC ASSERTIONS

17

Corollary 5.2. The PC holds iff we have n-ary η-validity for all n ≥ 1.
This corollary can be read, loosely, as a coincidence between parametric polymorphism
as introduced by Strachey [31] and relational parametricity as proposed by Reynolds [30]:
The PC corresponds to Strachey parametricity in the loose sense that if it holds, then there
is an approach, parametric in the assertion variables, that produce right hand side proofs
of heap membership from the left hand side ones: Take a heap, split it along the conjuncts,
apply the PC to the parts in the interpretations of the ϕ’s and you are done, possibly
after discarding some variables. This involves no branching or other intrinsic operations on
the assertion variables, which we are free to discard by our intuitionistic setup. If, on the
other hand, the implication is η-valid for arbitrary arity, then it is fair to call it relationally
parametric. Note also that the Examples 4.9 and 4.10 branch on assertion variable values.
This result is analogous to the conjecture of coincidence between Strachey parametricity
and n-ary relational parametricity for traditional type-based parametricity [29, Page 2].
Finally we note that as a consequence of the above corollary we have that the lifting
theorems in the previous section really show that unary validity can be lifted to validity
of arbitrary arity. In some sense, they are stronger than required for representation independence, for which binary validity suffices. The authors are unaware of any practical
applications of this fact.
6. Representation Independence
In this section, we relate our lifting theorems to representation independence. We consider separation logic with assertion variables where the rule of consequence is restricted
according to our lifting theorems, and we define a relational semantics of the logic, which
gives a representation independence theorem: all proved clients cannot distinguish between
appropriately related module implementations.
To keep the presentation simple, we omit while-loops and allocation from the language.
Adding the former together with the standard proof rule is straightforward. Allocation,
however, is non-trivial: the notion of having one client using two modules will be hardcoded into our relational reading of the logic, and allocation on part of the client must give
the same address when run with either module. This fails with standard, non-deterministic
allocation; it was resolved earlier, however, by Birkedal and Yang [10] using a combination
of FM sets and continuations and that approach is applicable here too.
We consider commands C given by the grammar:
C ::= k | [E]:=E | let y=[E] in C | C; C | if B C C
Here B is a heap-independent boolean expression, such as x=0. Commands C are from the
loop-free simple imperative language. They can call module operations k, and manipulate
heap cells; command [x]:=E assigns E to the heap cell x, and this assigned value is read
by let y=[x] in C, which also binds y to the read value and runs C under this binding.
Properties of commands C are specified using Hoare triples Γ ⊢ {ϕ}C{ψ}, where the
context Γ is a set of triples for module operations. Figure 4 shows rules for proving these
properties. In the figure, we omit contexts, if the same context Γ is used for all the triples.
The rule of consequence deserves attention. Note that the rule uses semantic implications |=1 in the standard unary interpretation, thus allowing the use of existing theorem
provers for separation logic. The rule does not allow all semantic implications, but only
those that pass our algorithm Chk, so as to ensure that the implications can lift to the

18

J. THAMSBORG, L. BIRKEDAL, AND H. YANG

Chk(ϕ′ , ϕ) ϕ′ |=1 ϕ {ϕ}C{ψ} ψ |=1 ψ ′ Chk(ψ, ψ ′ )
{ϕ′ }C{ψ ′ }
{ϕ}C{ϕ′ }
{ϕ ∗ ψ}C{ϕ′ ∗ ψ}

{ϕ}C{ψ}
x 6∈ FV(C)
{∃x. ϕ}C{∃x. ψ}

Γ, {ϕ}k{ψ} ⊢ {ϕ}k{ψ}

{E֒→ }[E]:=F {E֒→F }

{ϕ ∗ E֒→x}C{ψ}
x 6∈ FV(ψ)
{∃x.ϕ ∗ E֒→x}let x=[E] in C{ψ}
{ϕ}C{ϕ′ } {ϕ′ }C ′ {ψ} {ϕ ∧ B}C{ψ} {ϕ ∧ ¬B}C ′ {ψ}
{ϕ}C; C ′ {ψ}
{ϕ}if B C C ′ {ψ}
Figure 4: Proof Rules
relational level. Our algorithm Chk(ϕ, ψ) performs two checks, and returns true only when
both succeed. The first check is whether ϕ and ψ can be transformed to simple assertions
ϕ′ and ψ ′ , using only the distribution of ∗ over ∃x and ∨ and distributive lattice laws for ∨
and ∧. If this check succeeds and gives ϕ′ and ψ ′ , the algorithm transforms ϕ′ |=1 ψ ′ to a
set of implications of the form (4.1) in Section 4 (Lemma 4.1). Then, for each implication
in the resulting set, it tests if any of the the three criteria for lifting are met and returns
true if that is always the case2.
Commands C are interpreted in a standard way, as functions of the type: [[C]]η,u ∈
Heap → (Heap ∪ {err }). Here err denotes a memory error, and η and u are environments
that provide the meanings of, respectively, free ordinary variables and module operations.
For instance, [[k]]η,u is u(k).
Our semantics of triples, on the other hand, is not standard, and uses the binary
interpretation of assertions: (η, ρ, u) |=2 {ϕ}C{ψ} iff
∀r ∈ IRel2 . ∀f, g ∈ Heap. (f, g) ∈ [[ϕ]]2η,ρ ∗ r =⇒
([[C]]η,u1 (f ), [[C]]η,u2 (g)) ∈ [[ψ]]2η,ρ ∗ r.
The environment ρ provides the meanings of assertion variables, and the 2-dimensional
vector u gives the two meanings for module operations; intuitively, each ui corresponds to
the i-th module implementation. The interpretation means that if two module implementations u are used by the same client C, then these combinations should result in the same
computation, in the sense that they map ϕ-related input heaps to ψ-related outputs. The
satisfaction of triples can be extended to (η, ρ, u) |=2 Γ, by asking that all triples in Γ should
hold wrt. (η, ρ, u). Using these satisfaction relations on triples and contexts, we define the
notion of 2-validity of judgements: Γ ⊢ {ϕ}C{ψ} is 2-valid iff
∀(η, ρ, u). (η, ρ, u) |=2 Γ =⇒ (η, ρ, u) |=2 {ϕ}C{ψ}.
Theorem 6.1. Every derivable Γ ⊢ {ϕ}C{ψ} is 2-valid.
2Recall that the failure of the lifting theorems do not imply that a concrete implication cannot be lifted;

consider, e.g., Example 4.9 and replace 1֒→ with true everywhere. One can sidestep the general lifting
theorems and (try to) verify directly the Parametricity Condition from Definition 4.3 for all environments
η. It is, however, a semantic condition and probably undecidable in general.

TWO FOR THE PRICE OF ONE: LIFTING SEPARATION LOGIC ASSERTIONS

19

It is this theorem that we use to derive the representation independence results mentioned in the introduction. Consider again the example in Figure 1. Since the proof of the
left hand side client C is derivable using the above rules in the context
Γ = {1֒→ }init{a}, {a}inc{a}, {a}nxt{b},
{b}dec{b}, {b}fin{1֒→ },
we get 2-validity of Γ ⊢ {1֒→ }C{1֒→ }. Instantiating, in the definition of 2-validity, ρ with
the given coupling relations and u with the module implementations gives us
(∅, ρ, u) |=2 {1֒→ }C{1֒→ },
since we already know that the different operations respect the coupling relations. Therefore,
when we run the client C with the related module implementations, we find that C maps
[[1֒→ ]]2 -related heaps (i.e, heaps with the same value at cell 1) to [[1֒→ ]]2 -related heaps
again.
7. Conclusion and Discussion
In this paper, we have given a sound and, in a certain sense, complete characterization
of when semantic implications in separation logic with assertion variables can be lifted to
a relational interpretation. This characterization has, then, been used to identify proofs
of clients that respect the abstraction of module internals, specified by means of assertion
variables, and to show representation independence for clients with such proofs. We hope
that our results provide a solid semantic basis for recent logic-based approaches to data
abstraction.
In earlier work, Banerjee and Naumann [2] studied relational parametricity for dynamically allocated heap objects in a Java-like language. Later they extended their results to
cover clients programs that are correct with respect to specifications following the “Boogie methodology” implemented in the Spec# verifier [3, 4]. In both works, Banerjee and
Naumann made use of a non-trivial semantic notion of confinement to describe internal
resources of a module; here instead we use separation logic with assertions variables to
describe which resources are internal to the module.
Data abstraction and information hiding have been studied in logics and specification
languages for pointer programs, other than separation logic. Good example projects are
ESC-Modular-3 [20], ESC-Java [17] and Spec# [5], some of which use concepts analogous to
abstract predicates, called abstract variables [21]. It would be an interesting future direction
to revisit the questions raised in the paper in the context of these logics and specification
languages.
Relational interpretations have also been used to give models of programming languages
with local state, which can validate representation independence results [24, 28, 6, 1]. These
results typically rely on the module allocating the private state, whereas we use the power
of separation logic and allow the ownership transfer of states from client to module. For
instance, in the two-stage counter in the introduction, the ownership of the cell 1 is transferred from the client to the module upon calling init. Even with this ownership transfer,
representation independence is guaranteed, because we consider only those clients having
(good) proofs in separation logic. This contrasts with representation independence results
in local state models, which consider not some but all well-typed clients. The work by
Banerjee and Naumann [2] discussed above also permits ownership transfer.

20

J. THAMSBORG, L. BIRKEDAL, AND H. YANG

Acknowledgement
We would like to thank the anonymous referees for thorough reviews and insightful comments; their work made this work better. We are also grateful to John Wickerson and Peter
O’Hearn for their helpful comments. Yang was supported by EPSRC.
References
[1] A. Ahmed, D. Dreyer, and A. Rossberg. State-dependent representation independence. In POPL, pages
340–353, 2009.
[2] A. Banerjee and D. Naumann. Ownership confinement ensures representation independence for objectoriented programs. JACM, 52(6), 2005.
[3] A. Banerjee and D. A. Naumann. State based ownership, reentrance, and encapsulation. In ECOOP,
pages 387–411, 2005.
[4] M. Barnett, B.-Y. E. Chang, R. DeLine, B. Jacobs, and K. R. M. Leino. Boogie: A modular reusable
verifier for object-oriented programs. In FMCO, pages 364–387, 2005.
[5] M. Barnett, R. DeLine, M. Fähndrich, B. Jacobs, K. R. M. Leino, W. Schulte, and H. Venter. The
spec# programming system: Challenges and directions. In VSTTE, pages 144–152, 2005.
[6] N. Benton and B. Leperchey. Relational reasoning in a nominal semantics for storage. In TLCA, pages
86–101, 2005.
[7] B. Biering, L. Birkedal, and N. Torp-Smith. BI hyperdoctrines and higher-order separation logic. In
ESOP, 2005.
[8] B. Biering, L. Birkedal, and N. Torp-Smith. BI-hyperdoctrines, higher-order separation logic, and abstraction. TOPLAS, 29(5), 2007.
[9] L. Birkedal, N. Torp-Smith, and H. Yang. Semantics of separation-logic typing and higher-order frame
rules. In LICS, pages 260–269, 2005.
[10] L. Birkedal and H. Yang. Relational parametricity and separation logic. In FOSSACS, pages 93–107,
2007.
[11] S. D. Brookes. A semantics for concurrent separation logic. In P. Gardner and N. Yoshida, editors,
CONCUR, volume 3170 of Lecture Notes in Computer Science, pages 16–34. Springer, 2004.
[12] W.-N. Chin, C. David, H. H. Nguyen, and S. Qin. Enhancing modular oo verification with separation
logic. In POPL, 2008.
[13] D. Distefano, P. W. O’Hearn, and H. Yang. A local shape analysis based on separation logic. In TACAS,
pages 287–302, 2006.
[14] D. Distefano and M. Parkinson. jStar: towards practical verification for java. In OOPSLA, pages 213–
226, 2008.
[15] D. Distefano and M. Parkinson J. jstar: Towards practical verification for java. ACM Sigplan Notices,
43(10):213–226, 2008.
[16] R. Dockins, A. Hobor, and A. Appel. A fresh look at separation algebras and share accounting. In
APLAS, pages 161–177, 2009.
[17] C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. Extended static
checking for java. In PLDI, 2002.
[18] B. Jacobs and F. Piessens. The VeriFast program verifier. Technical Report CW-520, Katholieke Universiteit Leuven, 2008.
[19] O. Lee, H. Yang, and R. Petersen. Program analysis for overlaid data structures. In CAV, 2011.
[20] K. R. M. Leino and G. Nelson. An extended static checker for modular-3. In CC, pages 302–305, 1998.
[21] K. R. M. Leino and G. Nelson. Data abstraction and information hiding. ACM Trans. Program. Lang.
Syst., 24(5):491–553, 2002.
[22] A. Nanevski, A. Ahmed, G. Morrisett, and L. Birkedal. Abstract predicates and mutable ADTs in
Hoare type theory. In ESOP, 2007.
[23] A. Nanevski, G. Morrisett, A. Shinnar, P. Govereau, and L. Birkedal. Ynot: dependent types for
imperative programs. In ICFP, pages 229–240, 2008.
[24] P. O’Hearn and R. Tennent. Parametricity and local variables. JACM, 42(3):658–709, May 1995.
[25] P. W. O’Hearn, H. Yang, and J. C. Reynolds. Separation and information hiding. ACM Trans. Program.
Lang. Syst., 31(3), 2009.

TWO FOR THE PRICE OF ONE: LIFTING SEPARATION LOGIC ASSERTIONS

21

[26] M. Parkinson and G. Bierman. Separation logic and abstraction. In POPL, pages 247–258, 2005.
[27] M. Parkinson and G. Bierman. Separation logic, abstraction and inheritance. In POPL, pages 75–86,
2008.
[28] A. Pitts and I. Stark. Observable properties of higher order functions that dynamically create local
names, or: What’s new? In MFCS, pages 122–141, 1993.
[29] G. Plotkin and M. Abadi. A logic for parametric polymorphism. In TLCA, pages 361–375, 1993.
[30] J. C. Reynolds. Types, abstraction, and parametric polymorphism. In Information Processing 83, pages
513–523, 1983.
[31] C. Strachey. Fundamental concepts in programming languages. In Proceedings of the 1967 International
Summer School in Computer Programming, Copenhagen, Denmark., 1967.

Appendix A. Proofs of Lemma 2.2 and Lemma 3.1
Lemma 2.2. Function ∆n preserves the complete lattice structure and the ∗ operator.
Proof. From the definition, it is immediate that ∆n (Heap) = Heapn and ∆n (∅) = ∅, the
former because we have [] ∈ Heap. Now consider a non-empty family {pi }i∈I of predicates
in IRel1 . In order to show the preservation of the complete lattice structure, we need to
prove that
\
\
[
[
∆n ( pi ) =
∆n (pi ) ∧
∆n (pi ) = ∆n ( pi ).
i∈I

i∈I

i∈I

i∈I

The ⊆ direction in both cases is easy; it follows from the monotonicity of ∆n . T
We start with the ⊇ direction for the meet operator. Pick (h1 , . . . , hn ) from i∈I ∆n (pi ).
Then,
∀i ∈ I. (h1 , . . . , hn ) ∈ ∆n (pi ).
By the definition of ∆n , this means that
∀i ∈ I. ∃fi ∈ pi . fi ⊑ h1 ∧ . . . ∧ fi ⊑ hn .

(A.1)

P

Let f = i∈I fi . The sum here is well-defined, because (a) there are only finitely many f ’s
such that f ⊑ hk for all 1 ≤ k ≤ n, and (b) any two such f and g should have the same
value for every location in dom(f ) ∩ dom(g). Since all fi ’s satisfy (A.1), their sum f also
satisfies
f ⊑ h1 ∧ . . . ∧ f ⊑ hn .
T
Furthermore,
T f ∈ i∈ITpi , because pi ’s are upward closed and f is an extension of fi in pi .
Hence, ∆n ( i∈I pi ) ⊆ i∈I ∆n (pi ).
S
Next we prove the ⊇ direction for the join operator. Pick (h1 , . . . , hn ) from ∆n ( i∈I pi ).
Then,
∃i ∈ I. ∃f ∈ pi . f ⊑ h1 ∧ . . . ∧ f ⊑ hn .
Hence, by the definition of ∆n ,
[
(h1 , . . . , hn ) ∈ ∆n (pi ) ⊆
∆n (pi ),
i∈I

as desired.
Finally, it remains to show that ∆n preserves the ∗ operator. Consider predicates
p, q ∈ IRel1 . We need to prove that
∆n (p ∗ q) = ∆n (p) ∗ ∆n (q).

22

J. THAMSBORG, L. BIRKEDAL, AND H. YANG

Choose an arbitrary (h1 , . . . , hn ) from ∆n (p ∗ q). By the definition of ∆n (p ∗ q), it follows
that
∃f ∈ p. ∃g ∈ q. (dom(f ) ∩ dom(g) = ∅) ∧
f ⊑ h1 ∧ . . . ∧ f ⊑ hn ∧ g ⊑ h1 ∧ . . . ∧ g ⊑ hn .
Now, define fi = f and gi = hi − f for i ∈ {1, . . . , n}. Then,
(∀i ∈ {1, . . . , n}. fi · gi = hi )
∧ (f1 , . . . , fn ) ∈ ∆n (p) ∧ (g1 , . . . , gn ) ∈ ∆n (q).
Hence, (h1 , . . . , hn ) ∈ ∆n (p) ∗ ∆n (q). This shows that ∆n (p ∗ q) ⊆ ∆n (p) ∗ ∆n (q). For the
other inclusion, suppose that
(h1 , . . . , hn ) ∈ ∆n (p) ∗ ∆n (q).
Then, by the definition of ∗,
∃(f1 , . . . , fn ) ∈ ∆n (p). ∃(g1 , . . . , gn ) ∈ ∆n (q).
(∀i ∈ {1, . . . , n}. fi · gi = hi ).
Since (f1 , . . . , fn ) ∈ ∆n (p) and (g1 , . . . , gn ) ∈ ∆n (q), there are f ∈ p and g ∈ q such that
f ⊑ f1 ∧ . . . ∧ f ⊑ fn ∧ g ⊑ g1 ∧ . . . ∧ g ⊑ gn .
Furthermore, since f1 and g1 have disjoint domains, their subheaps f and g must have
disjoint domains as well. Consequently, f · g is well defined, and it satisfies
f · g ∈ p ∗ q ∧ (∀i ∈ {1, . . . , n}. f · g ⊑ fi · gi = hi ).
This implies that (h1 , . . . , hn ) ∈ ∆n (p ∗ q), as desired.
Lemma 3.1. For all ϕ and η, ρ, ρ′ , if ∆n (ρ(a)) = ρ′ (a) for every a ∈ AVar, we have that
∆n ([[ϕ]]1η,ρ ) = [[ϕ]]nη,ρ′ .
Proof. We prove by induction on the structure of ϕ. All the inductive cases and the cases
of true and false follow from the preservation result of Lemma 2.2. Thus, it is sufficient to
show the lemma when ϕ ≡ a or ϕ ≡ P . When ϕ ≡ a, the assumption of the lemma implies
that
∆n ([[a]]1η,ρ ) = ∆n (ρ(a)) = ρ′ (a) = [[a]]nη,ρ′ .
When ϕ ≡ P , we note that ∆n ◦ ∆1 = ∆n , and conclude that
∆n ([[P ]]1η,ρ ) = ∆n (∆1 (LP Mη )) = ∆n (LP Mη ) = [[P ]]nη,ρ′ .

TWO FOR THE PRICE OF ONE: LIFTING SEPARATION LOGIC ASSERTIONS

23

Appendix B. Proof of Lemma 4.1
Lemma 4.1. There is an algorithm taking simple assertions ϕ, ψ and returning finitely
many implications {ϕl =⇒ ψ l }l∈L , such that (a) ϕl =⇒ ψ l has the form (4.1) and (b) for
any n ∈ {1, 2}, we have that ϕ |=n ψ holds iff ϕl |=n ψ l holds for all l ∈ L.
Proof. The algorithm first transforms ψ in the conjunctive normal form, using proof rules
in classical logic, which hold in all the n-ary semantics. This gives an implication of the
form:
L
K _
J
I ^
^
_
ψ(k,l) ∗ b(k,l) .
ϕ(i,j) ∗ a(i,j) =⇒
i=1 j=1

k=1 l=1

Then, the algorithm constructs the below set:


L
J

^
_
ϕ(i,j) ∗ a(i,j) =⇒
ψ(k,l) ∗ b(k,l)


j=1

l=1

.
1≤i≤I,1≤k≤K

Finally, it removes, in each implication, all the disjuncts that include assertion variables
not appearing on the LHS of the implication; if all disjuncts are removed, false is the new
RHS. The outcome of this removal becomes the result of the algorithm.
Appendix C. Layouts that Lift
Lemma C.1 (Segregation). For any I, J ≥ 1 there are non-empty, finite segregating subsets SI,J
i,j ⊆ PosInt for all 1 ≤ i ≤ I and 1 ≤ j ≤ J with these properties:
S
S
I,J
I,J
(1) ∀1 ≤ i1 , i2 ≤ I.
1≤j≤J Si1 ,j =
1≤j≤J Si2 ,j .
I,J
(2) ∀1 ≤ i ≤ I. ∀1 ≤ j1 6= j2 ≤ J. SI,J
i,j1 ∩ Si,j2 = ∅.

I,J
(3) ∀1 ≤ i1 6= i2 ≤ I. ∀1 ≤ j1 , j2 ≤ J. SI,J
i1 ,j1 ∩ Si2 ,j2 6= ∅.
S
By 1 we define SI,J = 1≤j≤J SI,J
i,j for any 1 ≤ i ≤ I.

Theorem 4.5 (Shadow-Lift). Unary η-validity of an implication implies the PC if each
dashed line has a label that is not a label on a solid line and each disjunct has an occurrence
of a variable that is not a label on a solid line. Spelling it out in symbols, we require, with
L = {(i, j) | 1 ≤ i ≤ M ∧ 1 ≤ j ≤ N }, that

and

∀(i, j) ∈ L. Π(i)  Ω(j) =⇒
∃c ∈ V. Π(i)(c) < Ω(j)(c) ∧

∀(k, l) ∈ L. Π(k) ≥ Ω(l) =⇒ Π(k)(c) = Ω(l)(c)
∀1 ≤ j ≤ N. ∃c ∈ V. Ω(j)(c) > 0 ∧

∀(k, l) ∈ L. Π(k) ≥ Ω(l) =⇒ Π(k)(c) = Ω(l)(c) .

24

J. THAMSBORG, L. BIRKEDAL, AND H. YANG

Proof. Assume that we have an implication of the form (4.1) in Section 4 and an appropriate
environment η, that the stated criterion on the variable layout holds and that we have unary
η-validity. We must show that the PC holds.
According to Definition 4.3 we assume that we have heaps h, h1 , . . . , hM ∈ Heap with
hi ⊑ h and hi ∈ [[ϕi ]]1η for all 1 ≤ i ≤ M . The core of the proof is the construction of
a particular environment ρ : V → IRel1 . For that purpose we need some notation. For a
subset M ⊆ PosInt we denote by [M ] the heap that has domain M and stores some fixed
value, say 0, at all these locations. Let C ⊆ V be the set of assertion variables that do not
occur as labels on solid edges, i.e., for a c ∈ V we have that c ∈ C iff
∀1 ≤ i ≤ M. ∀1 ≤ j ≤ N.
Π(i) ≥ Ω(j) =⇒ Π(i)(c) = Ω(j)(c).
For each 1 ≤ i ≤ M we let Ki be the set of second indices of all variables in conjunct i that
lie in C, i.e., we set Ki = {1 ≤ k ≤ Mi | ai,k ∈ C}. If non-empty, we let ki = min(Ki ).
We now define ρ(c) = Heap for c ∈ V \ C. For a variable c ∈ C we let ρ(c) be the union
of
n
o↑
[
Y
M,K
(h − hi ) · [SM,K
+
L]
·
[S
+
L]
i,ki
i,k
1 ≤ i ≤ M,
Ki 6= ∅,
ai,ki ≡ c

1 ≤ k ≤ K,
k∈
/ Ki

and

[

[SM,K
i,k + L],

1≤i≤M,Ki 6=∅,k∈Ki \{ki },ai,k ≡c

where we have used K = max{M1 , . . . , MM } and L = max(dom(h) ∪ {0}). For each
1 ≤ i ≤ M we can write h · [SM,K + L] as the following product
Y M,K
Y
hi · (h − hi ) ·
[Si,k + L] ·
[SM,K
i,k + L],
k∈Ki

1≤k≤K,k ∈K
/ i

which implies that we have
a member of [[ϕi ∗ ai,1 ∗ · · · ∗ ai,Mi ]]1η,ρ . In summary,
we have shown that h · [SM,K + L] lies in the unary interpretation of the left hand side in
the environments η and ρ. By assumption, the same must hold for the right hand side and
from this we aim to derive the PC.
We now know that h · [SM,K + L] lies in the interpretation of some disjunct, say disjunct
j. This means that
h·[SM,K +L]

h · [SM,K + L] ∈ [[ψj ∗ bj,1 ∗ · · · ∗ bj,Nj ]]1η,ρ
Y
= [[ψj ]]1η ∗
ρ(bj,k ),
k∈J

where J = {1 ≤ k ≤ Nj | bj,k ∈ C} is the set of second indices of variables of disjunct j
that are in C. By the second assumption of the theorem we know that J 6= ∅. We write
Y
h · [SM,K + L] = g ·
gk
k∈J

[[ψj ]]1η

for g ∈
and gk ∈ ρ(bj,k ) for each k ∈ J. By the properties of segregating sets we get
that there must be a common 1 ≤ i ≤ M such that for all k ∈ J there is lk ∈ Ki with
[SM,K
i,lk + L] ⊑ gk ,

TWO FOR THE PRICE OF ONE: LIFTING SEPARATION LOGIC ASSERTIONS

25

i.e., the gk ’s are all ‘from the same conjunct’. But this implies Π(i)(c) ≥ Ω(j)(c) for all
c ∈ C as the segregating sets are non-empty. But then Π(i)(c) ≥ Ω(j)(c) must hold for
c ∈ V \ C too by the first assumption of the lemma and so Π(i) ≥ Ω(j). Also we must have
Π(i)(c) = Ω(j)(c) for each c ∈ C by definition of C. By construction we have
!
Y
dom
gk ⊇ dom(h − hi ) ∪ (SM,K + L)
k∈J

But then dom(g) ⊆ hi and so we have hi ∈ [[ψj ]]1η too and we have proved the first option
of the PC.

Theorem 4.7 (Balloon-Lift). Unary η-validity of an implication implies the PC if there
is a subset B ⊆ V with the following three properties. First, each conjunct has at most one
occurrence of a variable from B, i.e.,
X
∀1 ≤ i ≤ M.
Π(i)(c) ≤ 1.
c∈B

Second, each disjunct is empty or has exactly one occurrence of a variable from B, i.e.,
X
X
∀1 ≤ j ≤ N.
Ω(j)(c) = 0 ∨
Ω(j)(c) = 1.
c∈V

c∈B

Third, each dashed line must have a label from B. That is, when L = {(i, j) | 1 ≤ i ≤
M ∧ 1 ≤ j ≤ N },
∀(i, j) ∈ L. Π(i)  Ω(j) =⇒ ∃c ∈ B. Π(i)(c) < Ω(j)(c).
Proof. Assume that we have an implication of the form (4.1) in Section 4 and an appropriate
environment η, that the stated criterion on the variable layout holds and that we have unary
η-validity. We must show that the PC holds.
According to Definition 4.3 we assume that we have heaps h, h1 , . . . , hM ∈ Heap with
hi ⊑ h and hi ∈ [[ϕi ]]1η for all 1 ≤ i ≤ M . The core of the proof is the construction of a
particular environment ρ : V → IRel1 . We define ρ(c) = Heap for c ∈ V \ B. For a variable
c ∈ B we let ρ(c) be the following union
[
{h − hi }↑ .
1≤i≤M,1≤k≤Mi ,ai,k ≡c

For each 1 ≤ i ≤ M we can write h = hi ·(h−hi ) and so we have h in [[ϕi ∗ ai,1 ∗ · · · ∗ ai,Mi ]]1η,ρ
by the first of the original assumptions on the set B. In summary, we have shown that h
lies in the unary interpretation of the left hand side in the environments η and ρ. By
assumption, the same must hold for the right hand side and from this we aim to derive the
PC.
We now know that h lies in the interpretation of some disjunct, say disjunct j. If this
disjunct is empty we have proved the second option of the PC. Otherwise we know that
there is exactly one 1 ≤ k ≤ Nj such that bj,k ∈ B. But then we have
h ∈ [[ψj ∗ bj,1 ∗ · · · ∗ bj,Nj ]]1η,ρ = [[ψj ]]1η ∗ ρ(bj,k ).
We write
h = g · gk

26

J. THAMSBORG, L. BIRKEDAL, AND H. YANG

for g ∈ [[ψj ]]1η and gk ∈ ρ(bj,k ). There must be an 1 ≤ i ≤ M such that gk ⊒ h − hi and
such that Π(i)(bj,k ) = Ω(j)(bj,k ) = 1. The first gives hi ∈ [[ψj ]]1η and the second implies
Π(i) ≥ Ω(j) by the third assumption on B. And we have arrived at the first option of the
PC.
Appendix D. Completeness
Lemma D.1 (Fan-Counter). Suppose that the layout of variables is as follows. There are
at least two conjuncts, i.e., M ≥ 2, and one conjunct has the property that each variable
occurring in the conjunct also occurs as a label of a solid line leaving the conjunct and
ending in a non-empty disjunct. In symbols the latter is
∃1 ≤ i ≤ M. ∀c ∈ V. Π(i)(c) > 0 =⇒
∃1 ≤ j ≤ N. Π(i) ≥ Ω(j) ∧ Π(i)(c) > Ω(j)(c) ∧
∃d ∈ V. Ω(j)(d) > 0.
Then there are choices of ϕi ’s and ψj ’s with no variables such that the implication holds on
the unary level but not on the binary level.
In the search for counterexamples we may without loss of generality assume the negation
of the conditions of the above lemma. This means, provided at least two conjuncts, that
for any non-empty set of solid lines leaving one common conjunct and ending in non-empty
disjuncts there is a variable that occurs in the conjunct but is not a label of either of the
lines. If, loosely phrased, we invalidate that variable, then all the solid lines break down,
i.e., become dashed.
Lemma D.2 (X-Counter). Suppose that the layout of variables is as follows. There are
two distinct conjuncts i0 and i1 and two distinct non-empty disjuncts j0 and j1 such that
Π(i0 )  Ω(j0 ) while Π(i0 ) ≥ Ω(j1 ), Π(i1 ) ≥ Ω(j0 ) and Π(i1 ) ≥ Ω(j1 ). Then there are
choices of ϕi ’s and ψj ’s that the implication holds on the unary level but not on the binary
level.
Again we may without loss of generality assume that the negation of this lemma holds
when building counterexamples. Picture the graph of the implication without empty disjuncts and without dashed lines. The negation of the above means that we may arrive at all
vertices in the connected component containing some vertex by paths from that vertex of
length 2 or less. Also all connected components are complete, in particular no two vertices
with a dashed line between them can belong to the same component.
Lemma D.3 (Bridge-Counter). Suppose that the layout of variables is as follows. There
are at least two conjuncts, i.e., M ≥ 2, all disjuncts are non-empty and there is a dashed
line with labels that all occur as labels on solid lines too. In symbols the last demand is
∃1 ≤ i ≤ M. ∃1 ≤ j ≤ N. Π(i)  Ω(j) ∧
∀c ∈ V. Π(i)(c) < Ω(j)(c) =⇒
∃1 ≤ k ≤ M. ∃1 ≤ l ≤ N.
Π(k) ≥ Ω(l) ∧ Π(k)(c) > Ω(l)(c).
Then there are choices of ϕi ’s and ψj ’s with no variables such that the implication holds on
the unary level but not on the binary level.

TWO FOR THE PRICE OF ONE: LIFTING SEPARATION LOGIC ASSERTIONS

27

This lemma deals with the case of a variable layout with at least two conjuncts and no
empty disjuncts but where the first condition of Theorem 4.5 fails.
Lemma D.4 (All-Out-Counter). Suppose that the layout of variables is as follows. There
are at least two conjuncts, i.e., M ≥ 2, at least one non-empty disjunct and for each variable
one of the following two holds: Either the variable occurs as a label on a solid line ending
in a non-empty disjunct. Or it occurs at least twice in a conjunct and we have an empty
disjunct. In symbols the variable condition is
∀c ∈ V. ∃1 ≤ i ≤ M. ∃1 ≤ j ≤ N. Π(i) ≥ Ω(j) ∧

Π(i)(c) > Ω(j)(c) ∧ ∃d ∈ V. Ω(j)(d) > 0 ∨
∃1 ≤ i ≤ M. Π(i)(c) ≥ 2 ∧


∃1 ≤ j ≤ N. ∀d ∈ V. Ω(j)(d) = 0 .

Then there are choices of ϕi ’s and ψj ’s ϕi ’s and ψj ’s with no variables such that the implication holds on the unary level but not on the binary level.
This lemma deals with two cases. The first is the case of a variable layout with at least
two conjuncts and no empty disjuncts but where the second condition of Theorem 4.5 fails
while the first holds. The second is the case of a variable layout with at least two conjuncts,
at least one empty disjunct and no dashed lines for which Theorem 4.7 fails.
Appendix E. Higher Arities and Parametricity
Theorem 5.1. For an implication of the form (4.1) and an appropriate environment η we
have that n-ary η- validity implies the PC if n ≥ max{2, M1 , . . . , MM }.
Proof. Assume that we have an implication of the form (4.1) in Section 4 and an appropriate
environment η, that n ≥ max{2, M1 , . . . , MM } and that we have n-ary η-validity. We must
show that the PC holds.
According to Definition 4.3 we assume that we have heaps h, h1 , . . . , hM ∈ Heap with
hi ⊑ h and hi ∈ [[ϕi ]]1η for all 1 ≤ i ≤ M . The core of the proof is the construction of a
particular environment ρ : V → IReln . For that purpose we need some notation. Define, for
each 1 ≤ k ≤ n, a map γk : Heap → Heapn by letting
n−k

k−1

z }| { z }| { 
γk (h) = [], . . . , [], h, [], . . . , []

for any h ∈ Heap, i.e., it returns the n-tuple that has h as the k-th entry and the empty
heap everywhere else. Similarly, we define δ : Heap → Heapn by setting
n

z }| { 
δ(h) = h, . . . , h

for any h ∈ Heap, i.e., it returns the n-tuple that has h as all entries. For a subset M ⊆ PosInt
we denote by [M ] the heap that has domain M and stores some fixed value, say 0, at all
these locations.
For a variable c ∈ V we now define ρ(c) to be the following union of relations in IReln :
[
↑
{γk (h − hi ) · γ1 ([SM,K
i,k + L])}
1≤i≤M,1≤k≤Mi ,a(i,k) ≡c

28

J. THAMSBORG, L. BIRKEDAL, AND H. YANG

where K = max{M1 , . . . , MM }, L = max(dom(h)). This is well-defined because of our
assumption that n ≥ max{M1 , . . . , MM }. For each 1 ≤ i ≤ M we have that
δ(h) = δ(hi ) · γ1 (h − hi ) · · · · · γn (h − hi )
⊒ δ(hi ) · γ1 (h − hi ) · · · · · γMi (h − hi )
where we use the extension order for heap tuples defined by pointwise extension in all
entries. Also, we have that
[SM,K + L] = [SM,K
+ L] · · · · · [SM,K
i,1
i,K + L]
⊒ [SM,K
+ L] · · · · · [SM,K
i,1
i,Mi + L].
This gives us that δ(h) · γ1 ([SM,K + L]) extends the following n-tuple of heaps:
Y
δ(hi ) ·
γk (h − hi ) · γ1 ([SM,K
i,k + L])
1≤k≤Mi

which again means that δ(h) · γ1 ([SM,K + L]) lies in

[[ϕi ∗ ai,1 ∗ · · · ∗ ai,Mi ]]nη,ρ .
In summary, we have shown that δ(h) · γ1 ([SM,K + L]) lies in the n-ary interpretation of
the left hand side in the environments η and ρ. By assumption, the same must hold for the
right hand side and from this we aim to derive the PC.
There is 1 ≤ j ≤ N such that we have
δ(h) · γ1 ([SM,K + L]) ∈ [[ψj ∗ bj,1 ∗ · · · ∗ bj,Nj ]]nη,ρ .
Consider first the case of a non-empty disjunct, i.e., the case Nj > 0. We split along the
disjunct and get
δ(h) · γ1 ([SM,K + L]) = δ(g) · g1 · · · · · gNj
for g ∈ [[ψj ]]1η and gk ∈ ρ(bj,k ) for all 1 ≤ k ≤ Nj . By the properties of segregating sets
we get that there must be a common 1 ≤ i ≤ M such that for all 1 ≤ k ≤ Nj there is
1 ≤ kk ≤ Mi with
γkk (h − hi ) · γ1 ([SM,K
i,kk + L]) ⊑ gk ,
i.e., the gk ’s are all ‘from the same conjunct’. But this implies Π(i) ≥ Ω(j) as the segregating
sets are non-empty. Also the above equality enforces dom(g) ⊆ dom(h) by the definition of
γ1 . Indeed we must have dom(g) ⊆ dom(hi ) since in particular we have
γ1k (h − hi ) · γ1 ([SM,K
i,1k + L]) ⊑ g1 .
But then g ⊑ hi so we have hi ∈ [[ψj ]]1η too and the first option of the PC holds.
We consider now the case of an empty disjunct, i.e., the case Nj = 0. As above we split
along the disjunct and get
δ(h) · γ1 ([SM,K + L]) = δ(g) · g
for g ∈ [[ψj ]]1η and g ∈ Heapn . Again we must have dom(g) ⊆ dom(h) which implies g ⊑ h
and the second option of the PC holds.

TWO FOR THE PRICE OF ONE: LIFTING SEPARATION LOGIC ASSERTIONS

29

Appendix F. Proof of Theorem 6.1
Theorem 6.1. Every derivable Γ ⊢ {ϕ}C{ψ} is 2-valid.
Proof. We will show that all the rules in Figure 4 are sound. This lets us prove the theorem
by induction on the height of the derivation of a judgment, because using the soundness of
the rules, we can handle all the base and inductive cases.
Let’s start with the rule for the module operation k. Suppose that we have (η, ρ, u) |=2
(Γ, {ϕ}k{ψ}). Then, by the definition of |=2 , we should have (η, ρ, u) |=2 {ϕ}k{ψ} as well.
From this follows the soundness of the rule.
Next, consider four rules: (a) the frame rule for adding − ∗ ϕ to the pre and postconditions, (b) the rule for adding ∃x to the pre and post-conditions, (c) the rule for
sequencing, and (d) the rule for the conditional statement. All these rules are sound,
because of the following four facts:
(η, ρ, u) |=2 {ϕ}C{ϕ′ }
=⇒ (η, ρ, u) |=2 {ϕ ∗ ψ}C{ϕ′ ∗ ψ}
(x 6∈ FV(C)) ∧ (η, ρ, u) |=2 {ϕ}C{ψ}
=⇒ (η, ρ, u) |=2 {∃x.ϕ}C{∃x.ψ}
(η, ρ, u) |=2 {ϕ}C{ϕ′ } ∧ (η, ρ, u) |=2 {ϕ′ }C ′ {ψ}
=⇒ (η, ρ, u) |=2 {ϕ}C; C ′ {ψ}
(η, ρ, u) |=2 {ϕ ∧ B}C{ψ} ∧
(η, ρ, u) |=2 {ϕ ∧ ¬B}C ′ {ψ}
=⇒ (η, ρ, u) |=2 {ϕ}if B C C ′ {ψ}
The first fact is an easy consequence of using the quantification over IRel2 in the semantics
of triples. The second also follows easily from the semantics of triples and the fact that
[[C]]η,ui = [[C]]η[x7→v],ui for all v ∈ Int, as long as one remembers that the ∗ operator distributes
over union. The third and fourth are not different, and they follow from the semantics of
triples and commands. Here we will go through the details of proving the fourth fact.
Consider (η, ρ, u) satisfying the assumption of the fact. Pick r ∈ IRel2 and heaps f, g such
that
(f, g) ∈ [[ϕ]]2η,ρ ∗ r.
Now we do the case analysis on whether [[B]]η is true or not. If it is true, then
(f, g) ∈ [[ϕ ∧ B]]2η,ρ ∗ r
∧ [[if B C C ′ ]]η,u1 (f ) = [[C]]η,u1 (f )
∧ [[if B C C ′ ]]η,u2 (g) = [[C]]η,u2 (g).
Hence, by assumption, we get that
[[if B C C ′ ]]η,u1 (f ), [[if B C C ′ ]]η,u2 (g)
=



[[C]]η,u1 (f ), [[C]]η,u2 (g)



∈ [[ψ]]2η,ρ ∗ r.

If [[B]]η is not true, we reason similarly, but with C ′ instead of C, and get that

[[if B C C ′ ]]η,u1 (f ), [[if B C C ′ ]]η,u2 (g) ∈ [[ψ]]2η,ρ ∗ r.

30

J. THAMSBORG, L. BIRKEDAL, AND H. YANG

We have just shown that in both cases, the outcomes of the conditional statements are
related by [[ψ]]2η,ρ ∗ r, as claimed by the fourth fact.
We move on to the rules for heap update and dereference. They are sound because of
the below two facts:
(η, ρ, u) |=2 {E֒→ }[E]:=F {E֒→F }
x 6∈ FV(ψ) ∧ (η, ρ, u) |=2 {ϕ ∗ E֒→x}C{ψ}
=⇒ (η, ρ, u) |=2 {∃x.ϕ ∗ E֒→x}let x=[E] in C{ψ}
To prove the first, we pick (η, ρ, u), a relation r ∈ IRel2 and heaps f, g such that
(f, g) ∈ [[E ֒→ ]]2η,ρ ∗ r.
Then, there exist heaps h, f1 , g1 such that
(f, g) = (h, h) · (f1 , g1 ) ∧ [[E]]η ∈ dom(h) ∧ (f1 , g1 ) ∈ r.
Thus,
( [[[E]:=F ]]η,u1 (f ), [[[E]:=F ]]η,u2 (g) )
=

h[[[E]]η 7→[[F ]]η ] · f1 , h[[[E]]η 7→[[F ]]η ] · g1



∈ [[E֒→F ]]2η,ρ ∗ r,
as desired by the first fact. For the proof of the second fact, suppose that the assumption
of the second fact holds, and pick r ∈ IRel2 and heaps f, g such that
(f, g) ∈ [[∃x. ϕ ∗ E֒→x]]2η,ρ ∗ r.
Then, there exists an integer v and heaps h, f1 , g1 , f2 , g2 such that
(f, g) = (h, h) · (f1 , g1 ) · (f2 , g2 ) ∧ h ∈ [[E֒→x]]1η[x7→v]
∧ (f1 , g1 ) ∈ [[ϕ]]2η[x7→v],ρ ∧ (f2 , g2 ) ∈ r
Thus, (f, g) ∈ [[ϕ ∗ E֒→x]]2η[x7→v],ρ ∗ r, and f ([[E]]η ) = g([[E]]η ) = v. Using these and the
assumed triple of the second fact, we derive the below:
( [[let x=[E] in C]]η,u1 (f ), [[let x=[E] in C]]η,u2 (g) )

= [[C]]η[x7→v],u1 (f ), [[C]]η[x7→v],u2 (g)
∈ [[ψ]]2η[x7→v],ρ ∗ r

= [[ψ]]2η,ρ ∗ r.
The last equality holds, because x does not appear in ϕ. We have just proved that the
output states of two dereferencing commands are ([[ψ]]2η,ρ ∗ r)-related, as claimed by the
second fact.
Finally, we prove that the rule of consequence is sound. It is sufficient to show that
Chk(ϕ′ , ϕ) ∧ ϕ′ |=1 ϕ ∧
Chk(ψ, ψ ′ ) ∧ ψ |=1 ψ ′ ∧ (η, ρ, u) |=2 {ϕ}C{ψ}
=⇒

(η, ρ, u) |=2 {ϕ′ }C{ψ ′ }.

From the first four conjuncts of the assumption, it follows that
ϕ′ |=2 ϕ

∧

ψ |=2 ψ ′ .

TWO FOR THE PRICE OF ONE: LIFTING SEPARATION LOGIC ASSERTIONS

31

This is due to the correctness of Chk, which holds because all the transformations used in
the first check of Chk are based on semantic equivalences holding in IRel2 and the second
lifting check is sound because of our lifting theorems. In order to prove the conclusion of
the above implication, pick r ∈ IRel2 and heaps f, g such that
(f, g) ∈ [[ϕ′ ]]2η,ρ ∗ r.
Since the ∗ operator is monotone and ϕ′ |=2 ϕ, we get that
(f, g) ∈ [[ϕ]]2η,ρ ∗ r.
This relationship and the assumed triple {ϕ}C{ψ}, then, imply the below:
( [[C]]η,u1 (f ), [[C]]η,u2 (g) ) ∈ [[ψ]]2η,ρ ∗ r.
Again, since ψ |=2 ψ ′ , the monotonicity of the ∗ operator implies that
( [[C]]η,u1 (f ), [[C]]η,u2 (g) ) ∈ [[ψ ′ ]]2η,ρ ∗ r.
Note that this is the conclusion that we are looking for.

This work is licensed under the Creative Commons Attribution-NoDerivs License. To view
a copy of this license, visit http://creativecommons.org/licenses/by-nd/2.0/ or send a
letter to Creative Commons, 171 Second St, Suite 300, San Francisco, CA 94105, USA, or
Eisenacher Strasse 2, 10777 Berlin, Germany

