Invariants for Relational Reasoning

This file defines invariants - predicates on heap pairs that are preserved by package operations. Invariants are central to proving perfect indistinguishability.

Main definitions

• IsInvariant - A class for valid invariants on location pairs
• heapEq - The simplest invariant: heap equality
• trueInv - The trivial invariant that always holds

Usage

When relating two packages up to an invariant, we choose an invariant and prove that all operations preserve it while establishing equal behavior.

References

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

Invariant Class

class CatCrypt.Invariant.IsInvariant (L₀ L₁ : Package.Locations) (inv : Relational.RPre) : Prop

An invariant is a precondition that is well-formed with respect to location sets. It only talks about locations in L₀ (for the left heap) and L₁ (for the right heap).

The key property is that the invariant should be:

1. Preserved by operations that only access the declared locations
2. Restorable after writes to declared locations

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

  The invariant only depends on locations in L₀ for the left heap

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

  The invariant only depends on locations in L₁ for the right heap

Standard Invariants

def CatCrypt.Invariant.heapEq : Relational.RPre

Heap equality invariant: the heaps are equal

Equations

• CatCrypt.Invariant.heapEq = CatCrypt.Relational.eqPre

Note on heapEq and IsInvariant

Heap equality (heapEq) is not a proper invariant for the locality framework.

The IsInvariant class requires that if heaps agree on L₀/L₁, then the invariant is preserved. But heapEq requires complete heap equality, not just equality on specific locations.

For empty location sets, the locality hypothesis ∀ l ∈ ∅, ... is vacuously true, giving us no information about the relationship between h₀ and h₀'. We cannot prove h₀' = h₀ from this.

Design Decision: We intentionally do NOT provide an IsInvariant instance for heapEq with empty location sets. Users should use:

• trueInv for cases where no invariant is needed
• Location-specific invariants like syncsAt for tracking equality at specific locations

In the original CatCrypt/Rocq, the heap-equality case is handled specially, outside the locality framework. For Lean 4, we follow the same pattern: use rHoare_eq (defined in Rules.lean) for the heap equality case directly, bypassing the IsInvariant machinery.

def CatCrypt.Invariant.trueInv : Relational.RPre

True invariant: always holds (used when location sets are empty)

Equations

• CatCrypt.Invariant.trueInv = CatCrypt.Relational.truePre

instance CatCrypt.Invariant.trueInv_IsInvariant (L₀ L₁ : Package.Locations) : IsInvariant L₀ L₁ trueInv

Invariant Combinators

def CatCrypt.Invariant.andInv (inv₁ inv₂ : Relational.RPre) : Relational.RPre

Conjunction of invariants

Equations

• inv₁ ⋊ inv₂ = inv₁ ⋀ inv₂

instance CatCrypt.Invariant.andInv_IsInvariant {L₀ L₁ : Package.Locations} {inv₁ inv₂ : Relational.RPre} [hi₁ : IsInvariant L₀ L₁ inv₁] [hi₂ : IsInvariant L₀ L₁ inv₂] : IsInvariant L₀ L₁ (inv₁ ⋊ inv₂)

Conjunction of invariants is an invariant.

The mathematical proof is straightforward: if hloc : ∀ l ∈ L₀, h₀.get l = h₀'.get l and both inv₁ and inv₂ are invariants for L₀, L₁, then both left_local properties apply with the same hloc.

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.

def CatCrypt.Invariant.«term_⋊_» : Lean.TrailingParserDescr

Equations

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

Invariant Operations

theorem CatCrypt.Invariant.set_preserves_outside {L₀ L₁ : Package.Locations} {inv : Relational.RPre} [hInv : IsInvariant L₀ L₁ inv] (l : Core.Location) (v : l.ty) (h₀ h₁ : Core.Heap) (hinv : inv h₀ h₁) (hl₀ : l ∉ L₀) (hl₁ : l ∉ L₁) : inv (h₀.set l v) (h₁.set l v)

Setting a location on both sides preserves the invariant when the location is outside both L₀ and L₁.

This is because the invariant only depends on locations in L₀/L₁, so writes outside these sets don't affect the invariant.

Mathematical proof:

1. For any l' ∈ L₀, we have l'.id ≠ l.id (since l ∉ L₀ means l.id ∉ L₀.ids)
2. Therefore (h₀.set l v).get l' = h₀.get l' (by get_set_other)
3. Apply left_local with this agreement to get inv (h₀.set l v) h₁
4. Similarly, apply right_local to get inv (h₀.set l v) (h₁.set 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.

Special Invariants for Games

def CatCrypt.Invariant.eqInit : Relational.RPre

Invariant for equal initial state: heaps are equal

Equations

• CatCrypt.Invariant.eqInit = CatCrypt.Relational.eqPre