Relational Separating Conjunction

A separating conjunction on relational assertions RPre = Heap → Heap → Prop, and the frame rule it supports.

Main definitions

• HeapDisj, heapUnion (⊎), HeapSplit — the partial commutative monoid of heaps
• sepPre (∗) — separating conjunction of relational preconditions
• sepPost (∗ᵖ) — separating conjunction of a relational postcondition with a frame
• emp — the assertion holding only of the pair of empty heaps
• Frameable c D — the separation-logic locality of c on heaps satisfying D
• r_frame_sep — the frame rule
• not_frameable_get — reading is not local at a heap that does not own the location

Design

sepPre P Q splits both heaps of the pair, and splits them independently: (P ∗ Q) h₁ h₂ asserts that h₁ = a₁ ⊎ b₁ and h₂ = a₂ ⊎ b₂ for some splits with P a₁ a₂ and Q b₁ b₂. The two splits are unrelated to each other; in particular the domains a₁ and a₂ need not coincide.

The alternative — a lockstep split, additionally demanding a₁.data.keys = a₂.data.keys — is a strictly stronger assertion. As a precondition that is harmless, but the frame rule needs the same connective in the postcondition, where the extra conjunct becomes an obligation: the two runs must end with equal domains on the non-frame part. rHoare couples the two runs through a relation on (value, heap) pairs and delivers exactly that relation, so a lockstep postcondition would have to be established from Ψ, which in general does not mention domains. Independent splits keep the frame rule free of that obligation, and the frame parts b₁, b₂ are still related by the frame assertion, so no information about the frame is lost.

The locality side condition

rHoare is a global triple: it quantifies over whole heaps, and SPComp has no fault state, so a computation cannot be prevented from reading or writing outside a region by typing alone. The frame rule therefore cannot be side-condition-free; the side condition is Frameable c D, the semantic locality of separation logic:

• Frameable.frame — running c on h ⊎ hf is running it on h and re-attaching hf;
• Frameable.confined — c allocates no location outside the domain it was given.

Both are relative to a domain predicate D, because SPComp.get l and SPComp.set l v are local only on heaps that already contain l — that hypothesis is exactly what the points-to assertion l ↦ _ supplies in a small-footprint semantics. The frame rule requires D to follow from the precondition.

Unlike DependsOn, Frameable constrains the computation, not the assertion, so the frame assertion is arbitrary: eqPre and agreeOff, which have no finite footprint and so are outside the reach of r_frame_local, are framable here.

Relation to the location-based frame rules of CatCryptCore.Relational.Frame

r_frame_sep does not subsume r_frame_local, r_frame_of_preservesNothing or r_frame_agreeOff, and none of them subsumes it. Two independent obstructions separate ∗ from the location-based family.

The hypothesis on the computations. All three location-based rules ask only for PreservesOutside, a condition on writes. Frameable is a condition on writes and on reads: the frame property fails as soon as a computation can observe a location outside the heap it was given. not_frameable_get is the witness — SPComp.get l satisfies PreservesOutside (SPComp.get l) ∅, the strongest hypothesis any of the three rules can demand, and is not Frameable (SPComp.get l) (fun _ => True). So the three rules apply to computations for which r_frame_sep has no side condition to offer, at any choice of frame assertion.

The reading of the assertions. (P ∗ R) h₁ h₂ says P and R hold of parts of h₁ and h₂; (P ⋀ R) h₁ h₂ says both hold of the wholes. Neither implies the other, and a whole-heap precondition determines no split, so a location-based conclusion cannot be re-derived by instantiating ∗ even where Frameable does hold.

In the other direction, r_frame_set_sync_eqPre frames whole-heap equality of the untouched region across computations that write. r_frame_local cannot state that frame (no finite footprint), r_frame_of_preservesNothing forbids the writes, and r_frame_agreeOff frames only agreeOff L, not an arbitrary assertion on the untouched region. agreeOff_of_sepPost_eqPre is the one-way reading of a ∗ᵖ conclusion back as a whole-heap agreeOff assertion.

The four rules therefore cover four points:

• r_frame_local — finite-footprint frame, writes confined away from it, reads free.
• r_frame_of_preservesNothing — arbitrary frame, no writes, reads free.
• r_frame_agreeOff — co-finite frame of the fixed shape agreeOff L, writes inside L, reads free.
• r_frame_sep — arbitrary frame, writes free, reads confined to the owned region.

References

• Bluebell (POPL 2025) — P * Q separating conjunction for independence
• O'Hearn, Reynolds, Yang — Separation logic; locality = safety monotonicity + the frame property

Heap splitting

def CatCrypt.Relational.HeapDisj (h₁ h₂ : Core.Heap) : Prop

Two heaps have no location in common.

Equations

• CatCrypt.Relational.HeapDisj h₁ h₂ = h₁.data.Disjoint h₂.data

def CatCrypt.Relational.heapUnion (h₁ h₂ : Core.Heap) : Core.Heap

Union of two heaps. Left-biased on the overlap, so it is the disjoint union exactly when the arguments are HeapDisj.

Equations

• CatCrypt.Relational.heapUnion h₁ h₂ = { data := h₁.data ∪ h₂.data }

def CatCrypt.Relational.«term_⊎_» : Lean.TrailingParserDescr

Union of two heaps. Left-biased on the overlap, so it is the disjoint union exactly when the arguments are HeapDisj.

Equations

• One or more equations did not get rendered due to their size.

def CatCrypt.Relational.HeapSplit (h h₁ h₂ : Core.Heap) : Prop

HeapSplit h h₁ h₂ : h is the disjoint union of h₁ and h₂.

Equations

• CatCrypt.Relational.HeapSplit h h₁ h₂ = (CatCrypt.Relational.HeapDisj h₁ h₂ ∧ h = CatCrypt.Relational.heapUnion h₁ h₂)

Algebra of disjointness and union

theorem CatCrypt.Relational.heapUnion_data (h₁ h₂ : Core.Heap) : (heapUnion h₁ h₂).data = h₁.data ∪ h₂.data

theorem CatCrypt.Relational.HeapDisj.symm {h₁ h₂ : Core.Heap} (h : HeapDisj h₁ h₂) : HeapDisj h₂ h₁

theorem CatCrypt.Relational.heapDisj_empty_left (h : Core.Heap) : HeapDisj Core.Heap.empty h

theorem CatCrypt.Relational.heapDisj_empty_right (h : Core.Heap) : HeapDisj h Core.Heap.empty

theorem CatCrypt.Relational.heapDisj_union_left {h₁ h₂ h₃ : Core.Heap} : HeapDisj (heapUnion h₁ h₂) h₃ ↔ HeapDisj h₁ h₃ ∧ HeapDisj h₂ h₃

theorem CatCrypt.Relational.heapDisj_union_right {h₁ h₂ h₃ : Core.Heap} : HeapDisj h₁ (heapUnion h₂ h₃) ↔ HeapDisj h₁ h₂ ∧ HeapDisj h₁ h₃

@[simp]

theorem CatCrypt.Relational.heapUnion_empty (h : Core.Heap) : heapUnion h Core.Heap.empty = h

@[simp]

theorem CatCrypt.Relational.empty_heapUnion (h : Core.Heap) : heapUnion Core.Heap.empty h = h

theorem CatCrypt.Relational.heapUnion_assoc (h₁ h₂ h₃ : Core.Heap) : heapUnion (heapUnion h₁ h₂) h₃ = heapUnion h₁ (heapUnion h₂ h₃)

theorem CatCrypt.Relational.heapUnion_comm {h₁ h₂ : Core.Heap} (h : HeapDisj h₁ h₂) : heapUnion h₁ h₂ = heapUnion h₂ h₁

theorem CatCrypt.Relational.lookup_heapUnion_left {h₁ h₂ : Core.Heap} {id : ℕ} (h : id ∈ h₁.data) : Finmap.lookup id (heapUnion h₁ h₂).data = Finmap.lookup id h₁.data

theorem CatCrypt.Relational.lookup_heapUnion_right {h₁ h₂ : Core.Heap} {id : ℕ} (h : id ∉ h₁.data) : Finmap.lookup id (heapUnion h₁ h₂).data = Finmap.lookup id h₂.data

theorem CatCrypt.Relational.mem_heapUnion {h₁ h₂ : Core.Heap} {id : ℕ} : id ∈ (heapUnion h₁ h₂).data ↔ id ∈ h₁.data ∨ id ∈ h₂.data

The domain of a union is the union of the domains.

Algebra of splits

theorem CatCrypt.Relational.HeapSplit.disj {h h₁ h₂ : Core.Heap} (s : HeapSplit h h₁ h₂) : HeapDisj h₁ h₂

theorem CatCrypt.Relational.HeapSplit.eq {h h₁ h₂ : Core.Heap} (s : HeapSplit h h₁ h₂) : h = heapUnion h₁ h₂

theorem CatCrypt.Relational.HeapSplit.comm {h h₁ h₂ : Core.Heap} (s : HeapSplit h h₁ h₂) : HeapSplit h h₂ h₁

Splitting is symmetric.

theorem CatCrypt.Relational.HeapSplit.empty_right (h : Core.Heap) : HeapSplit h h Core.Heap.empty

The empty heap is a unit for splitting.

theorem CatCrypt.Relational.HeapSplit.empty_left (h : Core.Heap) : HeapSplit h Core.Heap.empty h

theorem CatCrypt.Relational.HeapSplit.assocL {h h₁ h₂ h₃ k : Core.Heap} (s : HeapSplit h h₁ k) (t : HeapSplit k h₂ h₃) : HeapSplit h (heapUnion h₁ h₂) h₃ ∧ HeapSplit (heapUnion h₁ h₂) h₁ h₂

A split whose right part splits again regroups to the left.

theorem CatCrypt.Relational.HeapSplit.assocR {h h₁ h₂ h₃ k : Core.Heap} (s : HeapSplit h k h₃) (t : HeapSplit k h₁ h₂) : HeapSplit h h₁ (heapUnion h₂ h₃) ∧ HeapSplit (heapUnion h₂ h₃) h₂ h₃

A split whose left part splits again regroups to the right.

Separating conjunction

def CatCrypt.Relational.sepPre (P Q : RPre) : RPre

Separating conjunction of relational preconditions: each of the two heaps splits, and P relates the two left parts while Q relates the two right parts. The splits on the two sides are independent.

Equations

• One or more equations did not get rendered due to their size.

def CatCrypt.Relational.«term_∗_» : Lean.TrailingParserDescr

Separating conjunction of relational preconditions: each of the two heaps splits, and P relates the two left parts while Q relates the two right parts. The splits on the two sides are independent.

Equations

• One or more equations did not get rendered due to their size.

def CatCrypt.Relational.sepPost {α : Type u_1} {β : Type u_2} (Ψ : RPost α β) (R : RPre) : RPost α β

Separating conjunction of a relational postcondition with a frame assertion: the postcondition constrains the parts the computations ran on, the frame the parts they did not.

Equations

• One or more equations did not get rendered due to their size.

def CatCrypt.Relational.«term_∗ᵖ_» : Lean.TrailingParserDescr

Separating conjunction of a relational postcondition with a frame assertion: the postcondition constrains the parts the computations ran on, the frame the parts they did not.

Equations

• One or more equations did not get rendered due to their size.

def CatCrypt.Relational.emp : RPre

The assertion of the pair of empty heaps: the unit of ∗.

Equations

• CatCrypt.Relational.emp h₁ h₂ = (h₁ = CatCrypt.Core.Heap.empty ∧ h₂ = CatCrypt.Core.Heap.empty)

Algebra of ∗

theorem CatCrypt.Relational.sepPre_of_split {P Q : RPre} {h₁ h₂ a₁ b₁ a₂ b₂ : Core.Heap} (s₁ : HeapSplit h₁ a₁ b₁) (s₂ : HeapSplit h₂ a₂ b₂) (hP : P a₁ a₂) (hQ : Q b₁ b₂) : sepPre P Q h₁ h₂

Introduction rule for ∗: exhibit the two splits.

theorem CatCrypt.Relational.sepPre_comm (P Q : RPre) (h₁ h₂ : Core.Heap) : sepPre P Q h₁ h₂ ↔ sepPre Q P h₁ h₂

theorem CatCrypt.Relational.sepPre_assoc (P Q S : RPre) (h₁ h₂ : Core.Heap) : sepPre (sepPre P Q) S h₁ h₂ ↔ sepPre P (sepPre Q S) h₁ h₂

theorem CatCrypt.Relational.sepPre_mono {P P' Q Q' : RPre} (hP : ∀ (k₁ k₂ : Core.Heap), P k₁ k₂ → P' k₁ k₂) (hQ : ∀ (k₁ k₂ : Core.Heap), Q k₁ k₂ → Q' k₁ k₂) {h₁ h₂ : Core.Heap} (h : sepPre P Q h₁ h₂) : sepPre P' Q' h₁ h₂

theorem CatCrypt.Relational.sepPre_emp (P : RPre) (h₁ h₂ : Core.Heap) : sepPre P emp h₁ h₂ ↔ P h₁ h₂

theorem CatCrypt.Relational.emp_sepPre (P : RPre) (h₁ h₂ : Core.Heap) : sepPre emp P h₁ h₂ ↔ P h₁ h₂

theorem CatCrypt.Relational.sepPost_mono {α : Type u_1} {β : Type u_2} {Ψ Ψ' : RPost α β} {R R' : RPre} (hΨ : ∀ (a : α) (k₁ : Core.Heap) (b : β) (k₂ : Core.Heap), Ψ a k₁ b k₂ → Ψ' a k₁ b k₂) (hR : ∀ (k₁ k₂ : Core.Heap), R k₁ k₂ → R' k₁ k₂) {a : α} {b : β} {h₁ h₂ : Core.Heap} (h : sepPost Ψ R a h₁ b h₂) : sepPost Ψ' R' a h₁ b h₂

Locality of computations

structure CatCrypt.Relational.Frameable {α : Type u_1} (c : Core.SPComp α) (D : Core.Heap → Prop) : Prop

Separation-logic locality of c, relative to the heaps satisfying D.

frame is the frame property: extending the heap by a disjoint hf extends every outcome by the same hf, with the same probabilities. confined says c allocates no location it was not given, which is what keeps the extension disjoint.

• frame (h hf : Core.Heap) : D h → HeapDisj h hf → c (heapUnion h hf) = (c h).bind fun (p : α × Core.Heap) => Prob.SDistr.pure (p.1, heapUnion p.2 hf)

  Running on an extended heap is running on the small heap and re-attaching.

• confined (h : Core.Heap) (a : α) (h' : Core.Heap) : D h → (c h) (some (a, h')) ≠ 0 → ∀ id ∈ h'.data, id ∈ h.data

  Outcomes stay inside the domain of the initial heap.

theorem CatCrypt.Relational.Frameable.disj_of_support {α : Type u_1} {c : Core.SPComp α} {D : Core.Heap → Prop} (hc : Frameable c D) {h hf h' : Core.Heap} {a : α} (hD : D h) (hdisj : HeapDisj h hf) (hsupp : (c h) (some (a, h')) ≠ 0) : HeapDisj h' hf

Confinement turns disjointness of the initial heap from a frame into disjointness of every outcome from that frame.

Support extraction

theorem CatCrypt.Relational.exists_of_bind_ne_zero {β : Type u_2} {γ : Type u_3} {d : Prob.SDistr γ} {g : γ → Prob.SDistr β} {x : β} (hne : (d.bind g) (some x) ≠ 0) : ∃ (y : γ), d (some y) ≠ 0 ∧ (g y) (some x) ≠ 0

A nonzero outcome of a bind comes from a nonzero outcome of each stage.

theorem CatCrypt.Relational.heap_eq_of_liftSDistr_support {γ : Type u_3} {d : Prob.SDistr γ} {h h' : Core.Heap} {a : γ} (hne : (d.bind fun (x : γ) => Prob.SDistr.pure (x, h)) (some (a, h')) ≠ 0) : h' = h

A heap-independent computation leaves the heap alone on its support.

Frameable instances

theorem CatCrypt.Relational.frameable_of_isPure {α : Type u_1} {c : Core.SPComp α} (hc : c.IsPure) : Frameable c fun (x : Core.Heap) => True

Every heap-independent computation is local, with no constraint on the heap.

theorem CatCrypt.Relational.frameable_pure {α : Type u_1} (a : α) : Frameable (Core.SPComp.pure a) fun (x : Core.Heap) => True

theorem CatCrypt.Relational.frameable_sample (α : Type) [Fintype α] [Nonempty α] : Frameable (Core.SPComp.sample α) fun (x : Core.Heap) => True

theorem CatCrypt.Relational.frameable_fail {α : Type u_1} : Frameable Core.SPComp.fail fun (x : Core.Heap) => True

def CatCrypt.Relational.Owns (l : Core.Location) : Core.Heap → Prop

The heaps that own location l: the domain predicate of get l and set l v.

Equations

• CatCrypt.Relational.Owns l h = (l.id ∈ h.data)

theorem CatCrypt.Relational.frameable_get (l : Core.Location) : Frameable (Core.SPComp.get l) (Owns l)

Reading a location is local on the heaps that own it. Ownership is needed: on a heap without l the read would see the frame's value instead of default.

theorem CatCrypt.Relational.not_frameable_get (l : Core.Location) (v : l.ty) (hv : v ≠ default) : ¬Frameable (Core.SPComp.get l) fun (x : Core.Heap) => True

Reading a location is not local at an arbitrary heap. SPComp.get l writes nothing, so PreservesOutside (SPComp.get l) ∅ holds, yet the frame property fails on a heap that does not own l together with a frame that does: the read sees the frame's value. The witness needs a location type with a non-default element.

theorem CatCrypt.Relational.frameable_set (l : Core.Location) (v : l.ty) : Frameable (Core.SPComp.set l v) (Owns l)

Writing a location is local on the heaps that own it. Ownership is needed for confinement: writing to an unowned location allocates it, and could collide with the frame.

theorem CatCrypt.Relational.Frameable.bind {α : Type u_1} {β : Type u_2} {c : Core.SPComp α} {f : α → Core.SPComp β} {D D' : Core.Heap → Prop} (hc : Frameable c D) (hf : ∀ (a : α), Frameable (f a) D') (hstep : ∀ (h : Core.Heap) (a : α) (h' : Core.Heap), D h → (c h) (some (a, h')) ≠ 0 → D' h') : Frameable (c.bind f) D

Locality composes through bind, provided the first stage lands in the domain predicate of the second.

The frame rule

theorem CatCrypt.Relational.r_frame_sep {α : Type u_1} {β : Type u_2} {Φ : RPre} {Ψ : RPost α β} {R : RPre} {c₁ : Core.SPComp α} {c₂ : Core.SPComp β} {D₁ D₂ : Core.Heap → Prop} (hL₁ : Frameable c₁ D₁) (hL₂ : Frameable c₂ D₂) (hD₁ : ∀ (k₁ k₂ : Core.Heap), Φ k₁ k₂ → D₁ k₁) (hD₂ : ∀ (k₁ k₂ : Core.Heap), Φ k₁ k₂ → D₂ k₂) (hInner : rHoare Φ c₁ c₂ Ψ) : rHoare (sepPre Φ R) c₁ c₂ (sepPost Ψ R)

The frame rule for the relational separating conjunction.

The frame assertion R is arbitrary — no footprint condition. What is required is that the two computations are local (Frameable) on the heaps their precondition describes, which is the semantic content of separation logic's "the triple only talks about the heap it owns".

Framing assertions with no finite footprint

theorem CatCrypt.Relational.r_frame_sep_eqPre {α : Type u_1} {β : Type u_2} {Φ : RPre} {Ψ : RPost α β} {c₁ : Core.SPComp α} {c₂ : Core.SPComp β} {D₁ D₂ : Core.Heap → Prop} (hL₁ : Frameable c₁ D₁) (hL₂ : Frameable c₂ D₂) (hD₁ : ∀ (k₁ k₂ : Core.Heap), Φ k₁ k₂ → D₁ k₁) (hD₂ : ∀ (k₁ k₂ : Core.Heap), Φ k₁ k₂ → D₂ k₂) (hInner : rHoare Φ c₁ c₂ Ψ) : rHoare (sepPre Φ eqPre) c₁ c₂ (sepPost Ψ eqPre)

Whole-heap equality is framable. r_frame_local cannot frame it: DependsOn requires a LocSet, which is finite, and eqPre constrains every location.

theorem CatCrypt.Relational.r_frame_sep_agreeOff {α : Type u_1} {β : Type u_2} {Φ : RPre} {Ψ : RPost α β} {L : Core.LocSet} {c₁ : Core.SPComp α} {c₂ : Core.SPComp β} {D₁ D₂ : Core.Heap → Prop} (hL₁ : Frameable c₁ D₁) (hL₂ : Frameable c₂ D₂) (hD₁ : ∀ (k₁ k₂ : Core.Heap), Φ k₁ k₂ → D₁ k₁) (hD₂ : ∀ (k₁ k₂ : Core.Heap), Φ k₁ k₂ → D₂ k₂) (hInner : rHoare Φ c₁ c₂ Ψ) : rHoare (sepPre Φ (agreeOff L)) c₁ c₂ (sepPost Ψ (agreeOff L))

Agreement outside a finite set is framable. Its footprint is co-finite, so it too is out of reach of r_frame_local.

A worked instance

theorem CatCrypt.Relational.rHoare_set_sync_owned (l : Core.Location) (v : l.ty) : rHoare (fun (h₁ h₂ : Core.Heap) => h₁ = h₂ ∧ Owns l h₁) (Core.SPComp.set l v) (Core.SPComp.set l v) fun (x : Unit) (h₁ : Core.Heap) (x_1 : Unit) (h₂ : Core.Heap) => h₁ = h₂

Writing the same value to the same owned location on both sides keeps the two heaps equal. The precondition carries the ownership of l that frameable_set needs.

theorem CatCrypt.Relational.r_frame_set_sync (l : Core.Location) (v : l.ty) (R : RPre) : rHoare (sepPre (fun (h₁ h₂ : Core.Heap) => h₁ = h₂ ∧ Owns l h₁) R) (Core.SPComp.set l v) (Core.SPComp.set l v) (sepPost (fun (x : Unit) (h₁ : Core.Heap) (x_1 : Unit) (h₂ : Core.Heap) => h₁ = h₂) R)

The synchronised write, framed by an arbitrary assertion on the rest of the heap.

theorem CatCrypt.Relational.r_frame_set_sync_eqPre (l : Core.Location) (v : l.ty) : rHoare (sepPre (fun (h₁ h₂ : Core.Heap) => h₁ = h₂ ∧ Owns l h₁) eqPre) (Core.SPComp.set l v) (Core.SPComp.set l v) (sepPost (fun (x : Unit) (h₁ : Core.Heap) (x_1 : Unit) (h₂ : Core.Heap) => h₁ = h₂) eqPre)

The synchronised write framed by whole-heap equality of the untouched region: the frame assertion here has no finite footprint, so r_frame_local does not apply to it.

theorem CatCrypt.Relational.agreeOff_of_sepPost_eqPre {α : Type u_1} {β : Type u_2} {Ψ : RPost α β} {a : α} {b : β} {h₁ h₂ : Core.Heap} (h : sepPost Ψ eqPre a h₁ b h₂) : ∃ (L : Core.LocSet), agreeOff L h₁ h₂

Framing whole-heap equality yields agreement outside the region the computations ran on: the untouched parts are literally the same heap, so the final heaps can differ only inside the two owned domains, which are finite.