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

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.

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.