Location Couplings for Relational Reasoning

This file defines location-specific couplings - relations between specific locations across the left and right heaps. These are used as semi-invariants that hold for specific locations.

Main definitions

• syncs - Two locations are synchronized (have equal values)
• rem_lhs / rem_rhs - Remembered values on left/right side
• single_lhs / single_rhs - Predicate about single location
• couple_cross - Relation across left and right locations

Usage

Location couplings are composed with invariants using ⋊ to build more precise relational specifications. The ssprove_sync and ssprove_restore tactics manipulate these couplings.

References

• Larsen and Schürmann, Nominal State-Separating Proofs
• SSProve: theories/Crypt/package/pkg_heap_comp.v

Synchronization

def CatCrypt.Invariant.syncs (l₀ l₁ : Core.Location) (hty : l₀.ty = l₁.ty) : Relational.RPre

Two locations are synchronized: they have equal values

Equations

• CatCrypt.Invariant.syncs l₀ l₁ hty h₀ h₁ = (h₀.get l₀ = cast ⋯ (h₁.get l₁))

def CatCrypt.Invariant.syncsAt (l : Core.Location) : Relational.RPre

Same location synchronized on both sides

Equations

• CatCrypt.Invariant.syncsAt l h₀ h₁ = (h₀.get l = h₁.get l)

theorem CatCrypt.Invariant.syncsAt_def (l : Core.Location) (h₀ h₁ : Core.Heap) : syncsAt l h₀ h₁ ↔ h₀.get l = h₁.get l

Remembered Values

def CatCrypt.Invariant.rem_lhs (l : Core.Location) (v : l.ty) : Relational.RPre

Remembered value on the left: the left heap has value v at location l

Equations

• CatCrypt.Invariant.rem_lhs l v h₀ x✝ = (h₀.get l = v)

def CatCrypt.Invariant.rem_rhs (l : Core.Location) (v : l.ty) : Relational.RPre

Remembered value on the right: the right heap has value v at location l

Equations

• CatCrypt.Invariant.rem_rhs l v x✝ h₁ = (h₁.get l = v)

inductive CatCrypt.Invariant.Side : Type

Remembered value in a specific invariant (left or right)

• left : Side
• right : Side

def CatCrypt.Invariant.rem_inv (s : Side) (l : Core.Location) (v : l.ty) : Relational.RPre

Equations

• CatCrypt.Invariant.rem_inv CatCrypt.Invariant.Side.left l v = CatCrypt.Invariant.rem_lhs l v
• CatCrypt.Invariant.rem_inv CatCrypt.Invariant.Side.right l v = CatCrypt.Invariant.rem_rhs l v

def CatCrypt.Invariant.Side.other : Side → Side

Get the other side

Equations

• CatCrypt.Invariant.Side.left.other = CatCrypt.Invariant.Side.right
• CatCrypt.Invariant.Side.right.other = CatCrypt.Invariant.Side.left

Single-Location Predicates

def CatCrypt.Invariant.single_lhs (l : Core.Location) (P : l.ty → Prop) : Relational.RPre

Predicate about a single location on the left

Equations

• CatCrypt.Invariant.single_lhs l P h₀ x✝ = P (h₀.get l)

def CatCrypt.Invariant.single_rhs (l : Core.Location) (P : l.ty → Prop) : Relational.RPre

Predicate about a single location on the right

Equations

• CatCrypt.Invariant.single_rhs l P x✝ h₁ = P (h₁.get l)

Location Couplings

def CatCrypt.Invariant.couple_lhs (l₀ l₁ : Core.Location) (R : l₀.ty → l₁.ty → Prop) : Relational.RPre

Relation between two locations on the left heap

Equations

• CatCrypt.Invariant.couple_lhs l₀ l₁ R h₀ x✝ = R (h₀.get l₀) (h₀.get l₁)

def CatCrypt.Invariant.couple_rhs (l₀ l₁ : Core.Location) (R : l₀.ty → l₁.ty → Prop) : Relational.RPre

Relation between two locations on the right heap

Equations

• CatCrypt.Invariant.couple_rhs l₀ l₁ R x✝ h₁ = R (h₁.get l₀) (h₁.get l₁)

def CatCrypt.Invariant.couple_cross (l₀ l₁ : Core.Location) (hty : l₀.ty = l₁.ty) (R : l₀.ty → l₁.ty → Prop) : Relational.RPre

Relation between a location on left and a location on right

Equations

• CatCrypt.Invariant.couple_cross l₀ l₁ hty R h₀ h₁ = R (h₀.get l₀) (h₁.get l₁)

def CatCrypt.Invariant.eqCross (l₀ l₁ : Core.Location) (hty : l₀.ty = l₁.ty) : Relational.RPre

Equality coupling across sides (same as syncs)

Equations

• CatCrypt.Invariant.eqCross l₀ l₁ hty = CatCrypt.Invariant.couple_cross l₀ l₁ hty fun (v₀ : l₀.ty) (v₁ : l₁.ty) => v₀ = cast ⋯ v₁

Triple Couplings

def CatCrypt.Invariant.triple_lhs (l₀ l₁ l₂ : Core.Location) (R : l₀.ty → l₁.ty → l₂.ty → Prop) : Relational.RPre

Relation between three locations on the left

Equations

• CatCrypt.Invariant.triple_lhs l₀ l₁ l₂ R h₀ x✝ = R (h₀.get l₀) (h₀.get l₁) (h₀.get l₂)

def CatCrypt.Invariant.triple_rhs (l₀ l₁ l₂ : Core.Location) (R : l₀.ty → l₁.ty → l₂.ty → Prop) : Relational.RPre

Relation between three locations on the right

Equations

• CatCrypt.Invariant.triple_rhs l₀ l₁ l₂ R x✝ h₁ = R (h₁.get l₀) (h₁.get l₁) (h₁.get l₂)

Set Predicates (for writes)

def CatCrypt.Invariant.set_lhs (l : Core.Location) (v : l.ty) (P : Relational.RPre) : Relational.RPre

Setting a value on the left, used in put rules

Equations

• CatCrypt.Invariant.set_lhs l v P h₀ h₁ = P (h₀.set l v) h₁

def CatCrypt.Invariant.set_rhs (l : Core.Location) (v : l.ty) (P : Relational.RPre) : Relational.RPre

Setting a value on the right, used in put rules

Equations

• CatCrypt.Invariant.set_rhs l v P h₀ h₁ = P h₀ (h₁.set l v)

Lemmas

theorem CatCrypt.Invariant.syncsAt_set_both (l : Core.Location) (v : l.ty) (h₀ h₁ : Core.Heap) : syncsAt l (h₀.set l v) (h₁.set l v)

theorem CatCrypt.Invariant.rem_lhs_intro (l : Core.Location) (h₀ h₁ : Core.Heap) : rem_lhs l (h₀.get l) h₀ h₁

theorem CatCrypt.Invariant.rem_rhs_intro (l : Core.Location) (h₀ h₁ : Core.Heap) : rem_rhs l (h₁.get l) h₀ h₁

theorem CatCrypt.Invariant.rem_sync {l : Core.Location} {v : l.ty} {s : Side} {h₀ h₁ : Core.Heap} (hrem : rem_inv s l v h₀ h₁) (hsync : syncsAt l h₀ h₁) : rem_inv s.other l v h₀ h₁

If locations are synced and we remember on one side, we can remember the same on the other

Proof helpers

class CatCrypt.Invariant.ProvenBy (coupling pre : Relational.RPre) : Prop

Mark that a location coupling is proven by the precondition

• holds (h₀ h₁ : Core.Heap) : pre h₀ h₁ → coupling h₀ h₁

instance CatCrypt.Invariant.ProvenBy_left (coupling inv : Relational.RPre) : ProvenBy coupling (coupling ⋊ inv)

If coupling is part of the precondition conjunction, it's proven

instance CatCrypt.Invariant.ProvenBy_right (coupling other inv : Relational.RPre) [ProvenBy coupling inv] : ProvenBy coupling (other ⋊ inv)

theorem CatCrypt.Invariant.coupling_from_pre {coupling pre : Relational.RPre} [ProvenBy coupling pre] {h₀ h₁ : Core.Heap} (hpre : pre h₀ h₁) : coupling h₀ h₁

Helper to extract proven coupling