Location-Based Frame Rule

This file provides a location-based frame rule for pRHL, the CatCrypt analogue of separation logic's frame rule and Bluebell's P * Q (separating conjunction = independence). The key idea: assertions on disjoint heap regions plus computations with bounded footprints enable compositional reasoning.

Main definitions

• DependsOn P L — assertion P only examines locations in L
• PreservesOutside c L — computation c only modifies locations in L
• r_frame_local — the frame rule: disjoint footprints preserve the frame
• r_frame_of_preservesNothing — any frame survives computations that write nothing
• r_frame_agreeOff — agreeOff L survives computations that write only inside L

Design notes

RPre = Heap → Heap → Prop is deterministic (no probabilistic separation needed). The right analogue of Bluebell's probabilistic separation is location-based separation: assertions on disjoint heap regions + computations with bounded footprints.

The three frame rules

The three rules cover three shapes of frame footprint, and none of them is an instance of another.

• r_frame_local frames an assertion with a finite footprint L_f (DependsOn Frame L_f) across computations writing only inside a L_c disjoint from it.
• r_frame_of_preservesNothing frames an arbitrary assertion, at the price of asking both computations to write nothing at all.
• r_frame_agreeOff frames the specific assertion agreeOff L, whose footprint is co-finite, across computations writing only inside L. DependsOn (agreeOff L) L_f fails for every finite L_f, so r_frame_local does not reach it; the computations write, so r_frame_of_preservesNothing does not either.

At L = ∅ the last two rules meet without either containing the other: agreeOff ∅ is whole-heap equality (agreeOff_empty_iff), one assertion, while r_frame_of_preservesNothing at the same footprint frames every assertion.

References

• Bluebell (POPL 2025) — P * Q separating conjunction for independence
• O'Hearn, Reynolds, Yang — Separation logic

Assertion locality

def CatCrypt.Relational.DependsOn (P : RPre) (L : Core.LocSet) : Prop

DependsOn P L means P only examines locations in L: heap pairs agreeing on L cannot be distinguished by P.

Equations

• CatCrypt.Relational.DependsOn P L = ∀ (h₁ h₁' h₂ h₂' : CatCrypt.Core.Heap), h₁.agreeOn h₁' L → h₂.agreeOn h₂' L → P h₁ h₂ → P h₁' h₂'

DependsOn instances

theorem CatCrypt.Relational.dependsOn_truePre : DependsOn truePre ∅

theorem CatCrypt.Relational.dependsOn_leftHas (l : Core.Location) (v : l.ty) : DependsOn (leftHas l v) {l.id}

theorem CatCrypt.Relational.dependsOn_rightHas (l : Core.Location) (v : l.ty) : DependsOn (rightHas l v) {l.id}

theorem CatCrypt.Relational.dependsOn_andPre {P Q : RPre} {L₁ L₂ : Core.LocSet} (hP : DependsOn P L₁) (hQ : DependsOn Q L₂) : DependsOn (P ⋀ Q) (L₁ ∪ L₂)

theorem CatCrypt.Relational.dependsOn_mono {P : RPre} {L L' : Core.LocSet} (h : DependsOn P L) (hsub : L ⊆ L') : DependsOn P L'

Computation footprint

def CatCrypt.Relational.PreservesOutside {α : Type} (c : Core.SPComp α) (L : Core.LocSet) : Prop

PreservesOutside c L means c does not modify locations outside L: for every output in c's support, non-L locations are unchanged.

Equations

• CatCrypt.Relational.PreservesOutside c L = ∀ (h : CatCrypt.Core.Heap) (a : α) (h' : CatCrypt.Core.Heap), (c h) (some (a, h')) ≠ 0 → ∀ id ∉ L, Finmap.lookup id h'.data = Finmap.lookup id h.data

PreservesOutside instances

theorem CatCrypt.Relational.preservesOutside_pure {α : Type} (a : α) : PreservesOutside (Core.SPComp.pure a) ∅

theorem CatCrypt.Relational.preservesOutside_sample (α : Type) [Fintype α] [Nonempty α] : PreservesOutside (Core.SPComp.sample α) ∅

theorem CatCrypt.Relational.preservesOutside_get (l : Core.Location) : PreservesOutside (Core.SPComp.get l) ∅

theorem CatCrypt.Relational.preservesOutside_set (l : Core.Location) (v : l.ty) : PreservesOutside (Core.SPComp.set l v) {l.id}

theorem CatCrypt.Relational.preservesOutside_bind {α β : Type} {c : Core.SPComp α} {f : α → Core.SPComp β} {L₁ L₂ : Core.LocSet} (hc : PreservesOutside c L₁) (hf : ∀ (a : α), PreservesOutside (f a) L₂) : PreservesOutside (c >>= f) (L₁ ∪ L₂)

The frame rule

theorem CatCrypt.Relational.r_frame_local {α β : Type} {Φ Frame : RPre} {Ψ : RPost α β} {c₁ : Core.SPComp α} {c₂ : Core.SPComp β} {L_c L_f : Core.LocSet} (hLocal₁ : PreservesOutside c₁ L_c) (hLocal₂ : PreservesOutside c₂ L_c) (hFrame : DependsOn Frame L_f) (hDisjoint : Disjoint L_c L_f) (hInner : rHoare Φ c₁ c₂ Ψ) : rHoare (Φ ⋀ Frame) c₁ c₂ fun (a : α) (h₁ : Core.Heap) (b : β) (h₂ : Core.Heap) => Ψ a h₁ b h₂ ∧ Frame h₁ h₂

Location-based frame rule: if computations only modify locations in L_c, and the frame assertion only depends on locations in L_f, and these sets are disjoint, then the frame is preserved.

This is the CatCrypt analogue of separation logic's frame rule.

theorem CatCrypt.Relational.heap_eq_of_preservesOutside_empty {α : Type} {c : Core.SPComp α} (h : PreservesOutside c ∅) {h₀ : Core.Heap} {a : α} {h' : Core.Heap} (hsupp : (c h₀) (some (a, h')) ≠ 0) : h' = h₀

A computation that modifies nothing leaves its heap alone.

theorem CatCrypt.Relational.r_frame_of_preservesNothing {α β : Type} {Φ : RPre} {Ψ : RPost α β} {c₁ : Core.SPComp α} {c₂ : Core.SPComp β} (hc₁ : PreservesOutside c₁ ∅) (hc₂ : PreservesOutside c₂ ∅) (hInner : rHoare truePre c₁ c₂ Ψ) : rHoare Φ c₁ c₂ fun (a : α) (h₁ : Core.Heap) (b : β) (h₂ : Core.Heap) => Ψ a h₁ b h₂ ∧ Φ h₁ h₂

Frame rule for computations that modify no location: the precondition carries through to the postcondition, whatever it is.

r_frame_local asks the frame to depend on a LocSet, which is a Finset, so it cannot frame an assertion with no finite footprint — eqPre, whole-heap equality, is one such. Nothing is needed of the assertion here, because the two computations leave their heaps as they found them, so the assertion holds of the final pair exactly when it held of the initial pair.

theorem CatCrypt.Relational.r_frame_agreeOff {α β : Type} {Φ : RPre} {Ψ : RPost α β} {c₁ : Core.SPComp α} {c₂ : Core.SPComp β} {L : Core.LocSet} (hc₁ : PreservesOutside c₁ L) (hc₂ : PreservesOutside c₂ L) (hInner : rHoare Φ c₁ c₂ Ψ) : rHoare (Φ ⋀ agreeOff L) c₁ c₂ fun (a : α) (h₁ : Core.Heap) (b : β) (h₂ : Core.Heap) => Ψ a h₁ b h₂ ∧ agreeOff L h₁ h₂

Frame rule for agreement outside a write-set: if both computations write only inside L and the two initial heaps agree outside L, the two final heaps agree outside L.

The frame agreeOff L constrains every location outside a finite set, so it has no finite footprint and DependsOn (agreeOff L) L_f fails for every L_f; the computations write inside L, so r_frame_of_preservesNothing does not apply. What replaces the disjointness hypothesis is that the frame's footprint is the complement of the write-set: each side's final heap agrees with its own initial heap outside L, and the initial heaps agree with each other there.