Semi-Invariants for Relational Reasoning

This file defines semi-invariants - partial invariants that conclude about specific locations rather than whole heaps. Semi-invariants can be combined with proper invariants using ⋊ conjunction.

Main definitions

• SemiInvariant - A predicate that is location-local
• IsInvariant_inv_conj - Combining invariants with semi-invariants

Usage

Semi-invariants are used for:

1. Tracking remembered values (rem_lhs, rem_rhs)
2. Location synchronization (syncsAt)
3. Location-specific couplings (couple_cross)

References

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

Semi-Invariant Class

class CatCrypt.Invariant.SemiInvariant (L₀ L₁ : Package.Locations) (sinv : Relational.RPre) : Prop

A semi-invariant is a predicate that depends only on specific locations. Unlike a full invariant, it doesn't need to be preserved by arbitrary writes, but it is local to the locations it mentions.

• left_reads (h₀ h₀' h₁ : Core.Heap) : (∀ l ∈ L₀, h₀.get l = h₀'.get l) → sinv h₀ h₁ → sinv h₀' h₁

  The semi-invariant only reads from locations in L₀ on the left

• right_reads (h₀ h₁ h₁' : Core.Heap) : (∀ l ∈ L₁, h₁.get l = h₁'.get l) → sinv h₀ h₁ → sinv h₀ h₁'

  The semi-invariant only reads from locations in L₁ on the right

Basic Semi-Invariant Instances

instance CatCrypt.Invariant.truePre_SemiInvariant (L₀ L₁ : Package.Locations) : SemiInvariant L₀ L₁ Relational.truePre

True is always a semi-invariant

theorem CatCrypt.Invariant.syncsAt_SemiInvariant (l : Core.Location) (L₀ L₁ : Package.Locations) (hl₀ : l ∈ L₀) (hl₁ : l ∈ L₁) : SemiInvariant L₀ L₁ (syncsAt l)

Synchronization at a location is a semi-invariant if both sides have the location.

Mathematical argument:

• hsync : h₀.get l = h₁.get l
• hloc : ∀ l' ∈ L₀, h₀.get l' = h₀'.get l'
• Since l ∈ L₀, we have h₀.get l = h₀'.get l (by hloc)
• Therefore h₀'.get l = h₀.get l = h₁.get l

Note: Earlier versions of this codebase had universe polymorphism issues here. These were resolved by fixing Location.ty to Type (Type 0) in Core/Location.lean.

theorem CatCrypt.Invariant.rem_lhs_SemiInvariant (l : Core.Location) (v : l.ty) (L₀ L₁ : Package.Locations) (hl : l ∈ L₀) : SemiInvariant L₀ L₁ (rem_lhs l v)

Remembered value on left is a semi-invariant.

Mathematical argument:

• hrem : h₀.get l = v
• hloc : ∀ l' ∈ L₀, h₀.get l' = h₀'.get l'
• Since l ∈ L₀, we have h₀.get l = h₀'.get l
• Therefore h₀'.get l = h₀.get l = v

Note: Earlier versions of this codebase had universe polymorphism issues here. These were resolved by fixing Location.ty to Type (Type 0) in Core/Location.lean.

theorem CatCrypt.Invariant.rem_rhs_SemiInvariant (l : Core.Location) (v : l.ty) (L₀ L₁ : Package.Locations) (hl : l ∈ L₁) : SemiInvariant L₀ L₁ (rem_rhs l v)

Remembered value on right is a semi-invariant.

Mathematical argument:

• hrem : h₁.get l = v
• hloc : ∀ l' ∈ L₁, h₁.get l' = h₁'.get l'
• Since l ∈ L₁, we have h₁.get l = h₁'.get l
• Therefore h₁'.get l = h₁.get l = v

Note: Earlier versions of this codebase had universe polymorphism issues here. These were resolved by fixing Location.ty to Type (Type 0) in Core/Location.lean.

Combining Invariants with Semi-Invariants

theorem CatCrypt.Invariant.IsInvariant_inv_conj {L₀ L₁ : Package.Locations} {inv sinv : Relational.RPre} [hInv : IsInvariant L₀ L₁ inv] [hSInv : SemiInvariant L₀ L₁ sinv] : IsInvariant L₀ L₁ (inv ⋊ sinv)

An invariant combined with a semi-invariant is still an invariant.

Mathematical argument:

• Both inv and sinv only depend on locations in L₀ (for left heap)
• If heaps agree on L₀, both inv and sinv transfer to the new heap
• Therefore their conjunction transfers as well

Note: Earlier versions of this codebase had universe polymorphism issues here. These were resolved by fixing Location.ty to Type (Type 0) in Core/Location.lean.

Additional Location Couplings

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

Predicate about a single location on the left heap

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 heap

Equations

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

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

Cross-heap coupling: relate values at locations across heaps. Unlike couple_cross in Coupling.lean, this version doesn't require type equality.

Equations

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

@[reducible, inline, deprecated CatCrypt.Invariant.syncsAt (since := "2026-02-13")]

abbrev CatCrypt.Invariant.syncs' (l : Core.Location) : Relational.RPre

Synchronized location: same value on both sides. Deprecated alias for syncsAt.

Equations

• CatCrypt.Invariant.syncs' l = CatCrypt.Invariant.syncsAt l

Semi-Invariant Instances for Additional Couplings

theorem CatCrypt.Invariant.single_lhs'_SemiInvariant (l : Core.Location) (P : l.ty → Prop) (L₀ L₁ : Package.Locations) (hl : l ∈ L₀) : SemiInvariant L₀ L₁ (single_lhs' l P)

single_lhs' is a semi-invariant for L₀ containing l

theorem CatCrypt.Invariant.single_rhs'_SemiInvariant (l : Core.Location) (P : l.ty → Prop) (L₀ L₁ : Package.Locations) (hl : l ∈ L₁) : SemiInvariant L₀ L₁ (single_rhs' l P)

single_rhs' is a semi-invariant for L₁ containing l

theorem CatCrypt.Invariant.couple_cross'_SemiInvariant (l₀ l₁ : Core.Location) (R : l₀.ty → l₁.ty → Prop) (L₀ L₁ : Package.Locations) (hl₀ : l₀ ∈ L₀) (hl₁ : l₁ ∈ L₁) : SemiInvariant L₀ L₁ (couple_cross' l₀ l₁ R)

couple_cross' is a semi-invariant when both locations are in respective sets

Heap Agreement Invariants

def CatCrypt.Invariant.heap_ignore (L : Package.Locations) : Relational.RPre

Heap ignore: heaps are equal except on specified locations. This is useful when protocols use private state that differs between the left and right executions.

Important Design Note: This definition talks about locations OUTSIDE L (requiring equality for l ∉ L), which is fundamentally incompatible with the IsInvariant L₀ L₁ framework:

• IsInvariant requires that if heaps agree on L₀/L₁, the invariant transfers
• heap_ignore L reads from ALL locations outside L
• When l ∉ L and l ∉ L₀, we have no information about h₀'.get l

For this reason, heap_ignore cannot be made into a sound IsInvariant instance. Use heap_agree (below) instead, which uses a positive formulation that works correctly with the IsInvariant framework.

Equations

• CatCrypt.Invariant.heap_ignore L h₀ h₁ = ∀ l ∉ L, h₀.get l = h₁.get l

Positive Agreement Invariant

def CatCrypt.Invariant.heap_agree (L : Package.Locations) : Relational.RPre

Heaps agree on a specific set of locations (positive formulation)

Equations

• CatCrypt.Invariant.heap_agree L h₀ h₁ = ∀ l ∈ L, h₀.get l = h₁.get l

instance CatCrypt.Invariant.heap_agree_IsInvariant (L : Package.Locations) : IsInvariant L L (heap_agree L)

heap_agree L is an invariant for (L, L)

Get/Put Preservation

theorem CatCrypt.Invariant.get_preserves_semi {L₀ L₁ : Package.Locations} {sinv : Relational.RPre} [SemiInvariant L₀ L₁ sinv] (l : Core.Location) (h₀ h₁ : Core.Heap) (hsinv : sinv h₀ h₁) : sinv h₀ h₁

Getting a value preserves semi-invariants

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

Putting a value on both sides preserves syncsAt if values are equal

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

Putting a value on left updates rem_lhs

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

Putting a value on right updates rem_rhs

Restoring Invariants After Writes

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

After writing equal values to both sides, sync is restored

theorem CatCrypt.Invariant.restore_rem_from_sync {l : Core.Location} {v : l.ty} {h₀ h₁ : Core.Heap} (hsync : syncsAt l h₀ h₁) (hrem_l : rem_lhs l v h₀ h₁) : rem_rhs l v h₀ h₁

Writing on one side and syncing restores remembered values