Chapter 6.1 — The Cubical Heap

Mutation as a path in the world category — Deppy's alternative to separation logic.

From Separating Conjunction to World-Paths

Most modern verifiers reason about heap mutation using separation logic: the heap factors as P ★ Q, mutation transfers ownership through the frame rule, and aliasing is forbidden by construction. Deppy takes a different route. The heap is a World, and mutation is a path in the category of worlds: every mutation increments a global epoch, and a proof established at epoch n only travels to epoch m via an explicit TransportProof.

The two approaches achieve similar soundness through different math, and both have honest tradeoffs. Pulse buys a clean frame rule at the cost of forbidding most aliasing; Deppy embraces aliasing as a first-class DuckPath in the world category and pays for it with an epoch counter and per-cell mutation log. The next chapter compares the two systems in detail; this chapter introduces the cubical machinery.

The World Type

A World records the entire heap as Deppy understands it during PSDL compilation. It carries an epoch counter, a name-to-cell table (so different Python names can point at the same cell — aliasing), and the cells themselves with per-cell invariants and mutation histories.

from deppy.proofs.psdl_heap import World

w = World()
cid = w.alloc('list')
w.bind('xs', cid)
w.alias('ys', 'xs')
print(sorted(w.aliases_of('xs')))   # ['xs', 'ys']
print(w.epoch)                       # 0

affected = w.mutate('xs')
print(w.epoch)                       # 1
print(sorted(affected))               # ['xs', 'ys']  ← alias group

needed, ms = w.transport_required(
    'ys', from_epoch=0, to_epoch=w.epoch
)
print(needed, ms)                    # True [1]

The output above is exactly what Deppy produces today — copy the snippet, run it under PYTHONPATH=/path/to/deppy python3, and the printed lines match.

What PSDL Emits for Mutation

Inside the PSDL compiler, every Python statement is mapped to a kernel ProofTerm. Mutating method calls (list.append, dict.__setitem__, attribute assignment, += on mutable types, …) emit an EffectWitness tagged with the cell name and the new epoch:

from deppy.proofs.psdl import compile_psdl

src = """
def append_then_read(xs):
    ys = xs
    xs.append(1)
    return ys
"""
res = compile_psdl(src, foundations={})
print(res.term_repr)
print(res.final_epoch, res.effect_sequence)

The compiler reports:

Cut(_psdl_step_3,
    Cut(ys, AxiomInvocation(xs), Refl),
    Cut(_psdl_step_4,
        EffectWitness(mutate:xs.append@epoch1, Refl),
        Refl))
1 [(4, 'mutate', 'xs.append')]

Three things to notice:

• The alias ys = xs becomes Cut(ys, AxiomInvocation(xs), Refl) — at the cell level this is a DuckPath: ys and xs are observationally interchangeable and the kernel records the equation.
• The mutating call becomes EffectWitness("mutate:xs.append@epoch1", Refl). The label names both the method and the new epoch.
• res.effect_sequence is the world path: the ordered list of effects from start to end of the block. Two composable blocks chain via the kernel's PathComp.

Reads After Mutation Require Transport

Suppose you proved an invariant about ys before the xs.append line — say, len(ys) == 3. After the mutation the proof was established at epoch 0 but you want to use it at epoch 1, with one intervening mutation on the shared cell. The kernel rejects the unmodified proof and demands a TransportProof along the mutation path:

# Pseudocode of what the kernel checks:
inv_at_0 = w.invariants_at('ys', epoch=0)   # [len(ys) == 3]
# ... w.mutate('xs') runs ...
inv_at_1 = w.invariants_at('ys', epoch=1)   # []  ← invariant is gone
needed, ms = w.transport_required('ys', from_epoch=0, to_epoch=1)
# needed == True; ms == [1] — transport must bridge the mutation at epoch 1

In HoTT terms, the invariant lives in the fibre over the world's type, and TransportProof is the operation that pushes a fibred fact along a world-path. Reading at the new epoch demands either a fresh proof at that epoch, or transport of an old proof along the path that produced the new epoch.

Aliasing Is a DuckPath at the Cell Level

Separation logic outlaws aliasing by construction: pts_to(x, _) ★ pts_to(y, _) implies x ≠ y. This is sound but restrictive — most Python idioms (list append, dictionary update, object reference passing) involve aliases.

Deppy instead represents an alias as a DuckPath: a kernel-level path saying that ys and xs address the same cell. The aliases_of(name) method returns the equivalence class. When any member of the class is mutated, the epoch increments for the entire class — invariants on every aliased name drop simultaneously, exactly as Python semantics require.

Quick Comparison to Pulse

Pulse (Microsoft Research's concurrent separation-logic verifier built on F^★) takes the opposite design choice. Both systems achieve similar soundness for memory-safe code; the next chapter expands this table.

Pulse's frame rule is an arrow you draw around a Hoare triple; Deppy's PathComp is an arrow you compose through a sequence of effects. Pulse forbids what it cannot prove disjoint; Deppy admits everything but forces transport when a proof is reused across mutations.

Cells & Per-Cell Invariants

Each HeapCell carries a type_tag, a list of CellInvariants, and a mutated_at log of epochs. The kernel uses the log to decide whether transport is needed:

from deppy.proofs.psdl_heap import World

w = World()
w.alloc('list'); w.bind('xs', 0)
w.add_invariant('xs', 'len(xs) >= 1')
print(w.invariants_at('xs', epoch=0))   # [the invariant]

w.mutate('xs')                          # epoch → 1
print(w.invariants_at('xs', epoch=1))   # []  ← invariant dropped

The EffectSequence

The compile result exposes a flat list of effects in source order:

res = compile_psdl("""
def f(a):
    a.append(1)
    a.extend([2, 3])
""", foundations={})
print(res.final_epoch)
print(res.effect_sequence)

Yields:

2
[(3, 'mutate', 'a.append'), (4, 'mutate', 'a.extend')]

Each tuple is (line_no, kind, target). The kernel chains these via PathComp to form the block's world-path. When one PSDL block calls another, the callee's path appends to the caller's; composition is associative because PathComp is.

What's Next

The next chapter, Separation Logic (vs Pulse), walks through the points-to and frame-rule machinery the older parts of Part 6 still use, and contrasts each separation-logic primitive with its cubical counterpart. The remaining Part 6 chapters apply the heap to references, arrays, threading, and async.