Chapter 6.2 — Separation Logic (vs Pulse)

The classical points-to + frame-rule machinery, side-by-side with the cubical heap and Pulse.

Two Heap Models, One Verifier

Deppy ships with two complementary heap models. The cubical heap from Chapter 6.1 is the native one — every compile_psdl call uses it implicitly. This chapter describes the older separation-logic primitives that remain available in deppy.separation, and contrasts them with both the cubical heap and the Pulse verifier (Microsoft Research).

Both systems achieve memory-safety soundness, but they slice the problem differently. Pulse forbids aliasing and gets a clean frame rule; Deppy's cubical model embraces aliasing as a first-class DuckPath and pays for it with an epoch counter and transport requirement.

From Hoare Logic to Separation Logic

Classical Hoare logic uses triples {P} C {Q} where P and Q are predicates over all program state. This works for simple programs, but falls apart when functions manipulate only part of the heap — every specification must describe the entire memory to be precise.

Separation logic (Reynolds, 2002; O'Hearn, 2001) solves this with a single new idea: propositions can assert ownership of disjoint regions of memory. A function that owns references x and y cannot accidentally corrupt reference z belonging to someone else, because z lives in a separate part of the heap that the function cannot even name.

SLProp: Propositions About the Heap

An SLProp describes a set of heaps — those heaps that satisfy the proposition. The fundamental building blocks are:

emp — The Empty Heap

emp is satisfied only by the empty heap: no references, no objects, nothing allocated.

from deppy.separation import emp, SLProp

# emp describes a heap with zero allocated references
assert isinstance(emp, SLProp)

pts_to(ref, value) — Points-To

The assertion pts_to(x, v) states that reference x exists on the heap and currently holds value v. Crucially, pts_to also asserts exclusive ownership of that reference — no other part of the program may read or write x unless ownership is explicitly shared.

from deppy.separation import pts_to
from deppy.heap import Ref

# "x points to the integer 42"
x: Ref[int] = Ref(42)
prop: SLProp = pts_to(x, 42)

The value argument can be a logical variable (a string name) to represent an unknown value:

# "x points to some unknown integer v"
prop = pts_to(x, 'v')  # v is universally quantified

★ — Separating Conjunction

The central operator. P ★ Q asserts that the heap can be split into two disjoint sub-heaps, one satisfying P and the other satisfying Q. In Python we write this as P ** Q:

# x and y point to DIFFERENT heap locations
spec = pts_to(x, 'a') ** pts_to(y, 'b')

# This implies x is not y (non-aliasing!)

Properties of ★:

• Commutative: P ** Q ≡ Q ** P
• Associative: (P ** Q) ** R ≡ P ** (Q ** R)
• Unit: P ** emp ≡ P

The Frame Rule

The frame rule is the crown jewel of separation logic. It says: if a function is proved correct for a small piece of the heap, it remains correct when run in a bigger heap — the "frame" (the unmentioned part) is automatically preserved.

In Deppy, the frame rule is applied automatically. When you call a function with a separation-logic spec, Deppy infers the frame from the calling context:

@requires(pts_to(x, 'i'))
@ensures(lambda _: pts_to(x, 'i + 1'))
def incr(x: Ref[int]):
    """Increment a mutable integer reference."""
    x.value += 1

# Calling context: we own both x and y
# pre:  pts_to(x, 10) ** pts_to(y, 20)
incr(x)
# post: pts_to(x, 11) ** pts_to(y, 20)  ← frame preserved y!

Ownership & Access Control

Ownership in separation logic is implicit: if your precondition mentions pts_to(x, v), you own x. If it doesn't, you can't access it. Attempting to read or write a reference you don't own is a proof failure, not a runtime error.

@requires(pts_to(x, 'v'))
def bad_read(x: Ref[int], y: Ref[int]) -> int:
    return y.value  # ✗ ERROR: no ownership of y!

@requires(pts_to(x, 'v') ** pts_to(y, 'w'))
def good_read(x: Ref[int], y: Ref[int]) -> int:
    return y.value  # ✓ OK — y is owned

Example: Incrementing a Reference

Let's walk through the complete verification of incr:

from deppy.separation import pts_to
from deppy.heap import Ref, requires, ensures

@requires(pts_to(x, 'i'))
@ensures(lambda _: pts_to(x, 'i + 1'))
def incr(x: Ref[int]):
    x.value += 1

Python-Specific: Object Attribute Mutation

In Python, heap mutation often takes the form of setting attributes on objects rather than dereferencing raw pointers. Deppy generalises pts_to with an attr_to assertion for attribute access:

from deppy.separation import attr_to

class Point:
    def __init__(self, x: float, y: float):
        self.x = x
        self.y = y

@requires(attr_to(p, 'x', 'px') ** attr_to(p, 'y', 'py'))
@ensures(lambda _: attr_to(p, 'x', 'px + dx') ** attr_to(p, 'y', 'py + dy'))
def translate(p: Point, dx: float, dy: float):
    """Translate a point by (dx, dy)."""
    p.x += dx
    p.y += dy

Here attr_to(p, 'x', 'px') means "the x attribute of object p holds value px." The separating conjunction between the two attr_to assertions guarantees that the x and y attributes are stored in disjoint slots (which they are, since Python stores them in the object's __dict__).

Example: Swapping Two References

Swapping is the canonical separation-logic example. We need to own both references, and the postcondition reflects the exchange:

@requires(pts_to(x, 'a') ** pts_to(y, 'b'))
@ensures(lambda _: pts_to(x, 'b') ** pts_to(y, 'a'))
def swap(x: Ref[int], y: Ref[int]):
    """Swap the values stored in two mutable references."""
    tmp = x.value      # read x → a
    x.value = y.value  # read y → b, write x ← b
    y.value = tmp      # write y ← a

Example: Rotate Three Values

@requires(pts_to(a, 'x') ** pts_to(b, 'y') ** pts_to(c, 'z'))
@ensures(lambda _: pts_to(a, 'z') ** pts_to(b, 'x') ** pts_to(c, 'y'))
def rotate3(a: Ref[int], b: Ref[int], c: Ref[int]):
    """Rotate values: a←c, b←a, c←b."""
    tmp = a.value
    a.value = c.value
    c.value = b.value
    b.value = tmp

Notice how the three-way ** guarantees that a, b, and c are all distinct references. Without this, the rotation proof would be unsound — if a and c were the same reference, the first write would destroy the value we need to read later.

Example: Dictionary Mutation

Python dictionaries are heap-allocated mutable maps. Deppy treats dictionary entries as individual heap cells:

from deppy.separation import dict_entry

@requires(dict_entry(d, 'name', 'old_name'))
@ensures(lambda _: dict_entry(d, 'name', 'new_name'))
def rename(d: dict, new_name: str):
    """Update the 'name' key without touching other keys."""
    d['name'] = new_name

The frame rule ensures that other dictionary entries (e.g., d['age']) are unaffected by this operation — they live in a separate region of the conceptual heap.

The Magic Wand (—★)

The magic wand P —★ Q (also called "separating implication") asserts: "given a heap satisfying P, I can produce a heap satisfying Q." It is the adjoint of ★:

# If I have (P —★ Q) ** P, I can derive Q
# This is the "modus ponens" of separation logic

from deppy.separation import wand

# "If you give me ownership of x, I'll give back x incremented"
promise: SLProp = wand(pts_to(x, 'v'), pts_to(x, 'v + 1'))

Summary of Rules

Z3 Encoding

Under the hood, Deppy encodes separation-logic obligations as Z3 constraints. The heap is modelled as a partial map from abstract addresses to values, and the separating conjunction is encoded using disjointness constraints on the domains of two sub-maps:

# Simplified Z3 encoding (internal)
from z3 import *

Addr = DeclareSort('Addr')
Heap = ArraySort(Addr, IntSort())

def disjoint(dom1, dom2):
    """No address belongs to both domains."""
    a = Const('a', Addr)
    return ForAll([a], Not(And(dom1(a), dom2(a))))

def sep_conj(p, q, heap):
    """P ** Q holds for heap iff heap splits into disjoint parts."""
    h1, h2 = Consts('h1 h2', Heap)
    return Exists([h1, h2],
        And(disjoint(dom(h1), dom(h2)),
            union(h1, h2) == heap,
            p(h1), q(h2)))

def copy(x: Ref[int], y: Ref[int]):
    y.value = x.value

@requires(pts_to(x, 'v'))
@ensures(lambda _: pts_to(x, 'v') ** pts_to(x, 'v'))