Chapter 6.3 — Mutable References

Aliasing as DuckPath in cubical, vs ownership transfer in Pulse.

Python Variables Are References

In Python, every variable is a reference — a name bound to an object on the heap. Assignment (y = x) copies the reference, not the object. This is the fundamental source of aliasing in Python:

class Box:
    def __init__(self, value):
        self.value = value

a = Box(10)
b = a            # b is an ALIAS for a — same object
b.value = 99
print(a.value)   # 99 — a was mutated through b!

In the classical separation-logic view: if two variables a and b are separated (pts_to(a, _) ** pts_to(b, _)), they cannot be aliases. If they might alias, we must model this explicitly. In the cubical view: aliases are DuckPaths; mutation through either of two aliases bumps the epoch on the shared cell, so any proof about either name is correctly invalidated.

Cubical view, in code

from deppy.proofs.psdl_heap import World

w = World()
cid = w.alloc('Box')
w.bind('a', cid); w.alias('b', 'a')
print(sorted(w.aliases_of('a')))   # ['a', 'b']

affected = w.mutate('b', line=3)
print(sorted(affected))               # ['a', 'b']  ← both invalidated
print(w.epoch)                       # 1

Aliasing vs. Non-Aliasing

# x ≠ y guaranteed
@requires(
    pts_to(x, 'a') **
    pts_to(y, 'b')
)
def safe(x, y):
    x.value = 0
    # y.value is still b

# x might equal y!
@requires(
    pts_to(x, 'a') and
    pts_to(y, 'b')
)
def unsafe(x, y):
    x.value = 0
    # y.value might be 0!

Ownership Tracking

Deppy tracks which references each function owns. Ownership is passed through function calls: when you call a function, you transfer ownership of the references mentioned in its precondition. When it returns, you get back ownership of the references in its postcondition.

@requires(pts_to(x, 'v'))
@ensures(lambda _: pts_to(x, 'v * 2'))
def double_ref(x: Ref[int]):
    x.value *= 2

# Caller perspective:
# pre:  pts_to(r, 5) ** pts_to(s, 7)
double_ref(r)   # transfers ownership of r, keeps s
# mid:  pts_to(r, 10) ** pts_to(s, 7)   ← r doubled, s unchanged
double_ref(s)   # transfers ownership of s, keeps r
# post: pts_to(r, 10) ** pts_to(s, 14)  ← both doubled independently

Swap with Detailed Proof

The swap function exchanges the values of two references. Here we annotate each intermediate state:

@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]):
    # State: pts_to(x, a) ** pts_to(y, b)
    tmp = x.value
    # State: pts_to(x, a) ** pts_to(y, b) ∧ tmp = a
    x.value = y.value
    # State: pts_to(x, b) ** pts_to(y, b) ∧ tmp = a
    y.value = tmp
    # State: pts_to(x, b) ** pts_to(y, a)  ✓

The key insight is that ** guarantees x ≠ y, so writing to x does not affect the value at y. Without separation logic, we would need to add an explicit x is not y precondition — which is exactly what ** gives us for free.

Linked Data Structures

Heap-allocated data structures like linked lists are where separation logic truly shines. Consider a simple linked list node:

from __future__ import annotations
from typing import Optional

class Node:
    def __init__(self, val: int, nxt: Optional[Node] = None):
        self.val = val
        self.nxt = nxt

A linked list is a chain of nodes on the heap. We define a recursive separation-logic predicate that describes the entire list:

from deppy.separation import SLProp, attr_to, emp

def is_list(head: Optional[Node], vals: list[int]) -> SLProp:
    """head points to a linked list containing vals."""
    if head is None:
        return emp if vals == [] else False
    if not vals:
        return False
    return (
        attr_to(head, 'val', vals[0]) **
        attr_to(head, 'nxt', head.nxt) **
        is_list(head.nxt, vals[1:])
    )

Each node occupies a disjoint region of the heap (enforced by **), which prevents cycles by construction.

Example: Prepend to a Linked List

@requires(is_list(head, 'xs'))
@ensures(lambda result: is_list(result, '[v] + xs'))
def prepend(head: Optional[Node], v: int) -> Node:
    """Prepend v to the front of the list."""
    return Node(v, head)

Example: Length of a Linked List

@requires(is_list(head, 'xs'))
@ensures(lambda result: is_list(head, 'xs') and result == len('xs'))
def list_length(head: Optional[Node]) -> int:
    """Return the length without modifying the list."""
    count = 0
    current = head
    while current is not None:
        count += 1
        current = current.nxt
    return count

Existential Quantification

Often we don't care about the exact value stored at a reference — we just need to know something is there. Deppy uses exists for this:

from deppy.separation import exists

# "x points to some integer, we don't care what"
prop = exists('v', pts_to(x, 'v'))

@requires(exists('v', pts_to(x, 'v')))
@ensures(lambda _: pts_to(x, 0))
def reset(x: Ref[int]):
    """Set reference to zero, regardless of current value."""
    x.value = 0

The existential hides the initial value — the function doesn't need to know it. This is useful for initialisation functions and cleanup code.

Ghost Variables

Ghost variables exist only in specifications — they have no runtime representation. Deppy uses them to track logical properties that aren't stored explicitly in the program:

from deppy.ghost import ghost_var, ghost_update

class Counter:
    def __init__(self):
        self.count = 0
        self._total_ops = ghost_var(0)  # specification-only

    @requires(
        attr_to(self, 'count', 'n') **
        ghost_pts_to(self._total_ops, 't')
    )
    @ensures(lambda _:
        attr_to(self, 'count', 'n + 1') **
        ghost_pts_to(self._total_ops, 't + 1')
    )
    def increment(self):
        self.count += 1
        ghost_update(self._total_ops, lambda t: t + 1)

Fractional Permissions

Full ownership (pts_to(x, v)) grants both read and write access. But what if multiple functions need to read the same reference concurrently? Deppy supports fractional permissions: a permission p where 0 < p ≤ 1.0.

from deppy.separation import pts_to_frac

# Full permission — can read and write
full = pts_to_frac(x, 'v', perm=1.0)

# Half permission — can only read
half = pts_to_frac(x, 'v', perm=0.5)

# Two halves combine to full permission:
# pts_to_frac(x, v, 0.5) ** pts_to_frac(x, v, 0.5)
#   ≡ pts_to_frac(x, v, 1.0)
#   ≡ pts_to(x, v)

Splitting and Joining Permissions

# Split: one full permission → two half permissions
@requires(pts_to(x, 'v'))
@ensures(lambda _:
    pts_to_frac(x, 'v', perm=0.5) **
    pts_to_frac(x, 'v', perm=0.5))
def share(x: Ref[int]):
    """Split ownership for concurrent readers."""
    pass  # ghost operation — no runtime effect

# Join: two half permissions → one full permission
@requires(
    pts_to_frac(x, 'v', perm=0.5) **
    pts_to_frac(x, 'v', perm=0.5))
@ensures(lambda _: pts_to(x, 'v'))
def recombine(x: Ref[int]):
    """Recombine shared permissions for exclusive access."""
    pass  # ghost operation

Multiple Readers, Single Writer

Fractional permissions naturally encode the readers–writer pattern: any number of readers can hold fractional permissions simultaneously, but a writer needs the full permission (which means all readers must give up their shares first).

# Multiple readers — each gets a fraction
@requires(pts_to_frac(data, 'v', perm=0.25))
@ensures(lambda result:
    pts_to_frac(data, 'v', perm=0.25) and result == 'v')
def read_data(data: Ref[str]) -> str:
    """Read-only access with fractional permission."""
    return data.value

# Writer — needs full permission
@requires(pts_to(data, 'old'))  # perm=1.0 implied
@ensures(lambda _: pts_to(data, 'new_val'))
def write_data(data: Ref[str], new_val: str):
    """Write requires exclusive ownership."""
    data.value = new_val

Comparison with Pulse References

fn swap (x y: ref int)
  requires
    pts_to x 'a' **
    pts_to y 'b'
  ensures
    pts_to x 'b' **
    pts_to y 'a'
{
  let vx = !x;
  let vy = !y;
  x := vy;
  y := vx;
}

@requires(
    pts_to(x, 'a') **
    pts_to(y, 'b'))
@ensures(lambda _:
    pts_to(x, 'b') **
    pts_to(y, 'a'))
def swap(x, y):
    vx = x.value
    vy = y.value
    x.value = vy
    y.value = vx

The specifications are nearly identical — separation logic is the same regardless of the host language. The main differences are syntactic:

• Pulse uses ! for read and := for write; Deppy uses .value.
• Pulse requires explicit type annotations on all bindings; Deppy infers types from Python's runtime.
• Deppy specifications are Python decorators — they can be introspected, composed, and tested like any other Python object.

Example: Binary Tree Ownership

class TreeNode:
    def __init__(self, val, left=None, right=None):
        self.val = val
        self.left = left
        self.right = right

def is_bst(node: Optional[TreeNode],
         lo: int, hi: int) -> SLProp:
    """node is a BST with all values in (lo, hi)."""
    if node is None:
        return emp
    return (
        attr_to(node, 'val', node.val) **
        attr_to(node, 'left', node.left) **
        attr_to(node, 'right', node.right) **
        pure(lo < node.val < hi) **
        is_bst(node.left, lo, node.val) **
        is_bst(node.right, node.val, hi)
    )

@requires(is_bst(root, 'lo', 'hi'))
@ensures(lambda result:
    is_bst(root, 'lo', 'hi') and
    result == '(target in tree_values(root))')
def search(root: Optional[TreeNode], target: int) -> bool:
    """Search in BST — verified to not modify the tree."""
    if root is None:
        return False
    if target == root.val:
        return True
    elif target < root.val:
        return search(root.left, target)
    else:
        return search(root.right, target)