Invariant Tactics

This file provides tactics for working with invariants in relational proofs, including proving invariant preservation and extracting relation hypotheses.

Main tactics

• ssprove_invariant - prove IsInvariant goals using common patterns
• ssprove_invariant_step - discharge per-operation invariant preservation goals
• ssprove_rem_rel - extract hypotheses from remembered/synchronized values
• ssprove_restore - restore invariant after writes

Heap agreement modulo location sets

• heap_agree_except - heaps agree except on a set of locations (useful for proving that operations on private state don't affect the invariant)
• Preservation rules for sample, get, set operations

Implementation Notes

ssprove_invariant

The ssprove_invariant tactic tries the following strategies in order:

1. trueInv_IsInvariant - trivial invariant that always holds
2. heap_agree_IsInvariant - heap agreement on specified locations
3. IsInvariant_inv_conj - conjunction of invariant with semi-invariant
4. andInv_IsInvariant - conjunction of two invariants
5. User-provided assumptions

ssprove_rem_rel

The ssprove_rem_rel tactic extracts information from location couplings:

• rem_lhs l v - the left heap has value v at location l
• rem_rhs l v - the right heap has value v at location l
• syncsAt l - both heaps have the same value at location l

When both rem_lhs l v and syncsAt l hold, we can derive rem_rhs l v.

References

• SSProve: theories/Crypt/package/pkg_user_util.v
• SSProve: theories/Crypt/package/pkg_invariants.v
• EasyCrypt: auto/sp/wp for invariant preservation

Heap Agreement Modulo Locations

These definitions and lemmas support proving that operations on private state don't break an invariant on shared state. This is the key pattern for crypto proofs where packages have disjoint state.

def CatCrypt.Relational.heap_agree_except (L : Finset ℕ) : RPre

Heap equivalence modulo a set of location IDs. Two heaps agree except possibly at locations in L.

This is the "frame" invariant: L represents the "private" locations that may differ, and everything else must be equal.

Equations

• CatCrypt.Relational.heap_agree_except L h₁ h₂ = ∀ (ℓ : CatCrypt.Core.Location), ℓ.id ∉ L → h₁.get ℓ = h₂.get ℓ

Preservation rules for heap_agree_except

theorem CatCrypt.Relational.heap_agree_except_sample (L : Finset ℕ) (α : Type u_1) [Fintype α] [Nonempty α] : rHoare (heap_agree_except L) (Core.SPComp.sample α) (Core.SPComp.sample α) fun (a₁ : α) (h₁ : Core.Heap) (a₂ : α) (h₂ : Core.Heap) => heap_agree_except L h₁ h₂ ∧ a₁ = a₂

Sampling preserves heap_agree_except (sampling doesn't touch the heap).

theorem CatCrypt.Relational.heap_agree_except_get (L : Finset ℕ) (ℓ : Core.Location) (hℓ : ℓ.id ∉ L) : rHoare (heap_agree_except L) (Core.SPComp.get ℓ) (Core.SPComp.get ℓ) fun (a₁ : ℓ.ty) (h₁ : Core.Heap) (a₂ : ℓ.ty) (h₂ : Core.Heap) => heap_agree_except L h₁ h₂ ∧ a₁ = a₂

Getting from a location not in L gives equal values.

theorem CatCrypt.Relational.heap_agree_except_set_in (L : Finset ℕ) (ℓ : Core.Location) (hℓ : ℓ.id ∈ L) (v₁ v₂ : ℓ.ty) : rHoare (heap_agree_except L) (Core.SPComp.set ℓ v₁) (Core.SPComp.set ℓ v₂) fun (x : Unit) (h₁ : Core.Heap) (x_1 : Unit) (h₂ : Core.Heap) => heap_agree_except L h₁ h₂

Setting a location IN L (private state) with arbitrary values preserves the invariant.

theorem CatCrypt.Relational.heap_agree_except_set_same (L : Finset ℕ) (ℓ : Core.Location) (v : ℓ.ty) : rHoare (heap_agree_except L) (Core.SPComp.set ℓ v) (Core.SPComp.set ℓ v) fun (x : Unit) (h₁ : Core.Heap) (x_1 : Unit) (h₂ : Core.Heap) => heap_agree_except L h₁ h₂

Setting the same value on both sides preserves the invariant (for any location).

theorem CatCrypt.Relational.heap_agree_except_get_any (L : Finset ℕ) (ℓ : Core.Location) : rHoare (heap_agree_except L) (Core.SPComp.get ℓ) (Core.SPComp.get ℓ) fun (x : ℓ.ty) (h₁ : Core.Heap) (x_1 : ℓ.ty) (h₂ : Core.Heap) => heap_agree_except L h₁ h₂

Getting from any location preserves the invariant.

theorem CatCrypt.Relational.heap_agree_except_ret {α : Type u_1} (L : Finset ℕ) (a : α) : rHoare (heap_agree_except L) (pure a) (pure a) fun (x : α) (h₁ : Core.Heap) (x_1 : α) (h₂ : Core.Heap) => heap_agree_except L h₁ h₂

Pure/return preserves the invariant.

ssprove_invariant Tactic

def CatCrypt.Tactics.tacticSsprove_invariant : Lean.ParserDescr

ssprove_invariant is a tactic for proving IsInvariant goals.

The tactic attempts to prove that a predicate is a valid invariant by trying:

1. trueInv_IsInvariant - the trivial invariant
2. heap_agree_IsInvariant - heap agreement invariants
3. IsInvariant_inv_conj - conjunction with semi-invariants (recursive)
4. andInv_IsInvariant - conjunction of invariants
5. Type class inference
6. Direct assumptions

Example:

-- Proving that trueInv is an invariant
example : IsInvariant L₀ L₁ trueInv := by ssprove_invariant

-- Proving that heap_agree is an invariant
example : IsInvariant L L (heap_agree L) := by ssprove_invariant

-- Proving conjunction invariants
example [IsInvariant L₀ L₁ inv] [SemiInvariant L₀ L₁ sinv] :
    IsInvariant L₀ L₁ (inv ⋊ sinv) := by ssprove_invariant

Equations

• CatCrypt.Tactics.tacticSsprove_invariant = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_invariant 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_invariant" false)

def CatCrypt.Tactics.tacticSsprove_invariant! : Lean.ParserDescr

ssprove_invariant! is a more aggressive version that uses decide for decidable goals.

Equations

• CatCrypt.Tactics.tacticSsprove_invariant! = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_invariant! 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_invariant!" false)

def CatCrypt.Tactics.tacticSsprove_invariant_step : Lean.ParserDescr

ssprove_invariant_step discharges per-operation invariant preservation goals for heap_agree_except.

This tactic tries all preservation rules for heap_agree_except:

• Sample (always preserves)
• Get (always preserves)
• Set on private location (arbitrary values)
• Set on shared location (same value)
• Sync and ret rules

Example:

-- Given goal: rHoare (heap_agree_except L) (SPComp.sample α) (SPComp.sample α) Ψ
ssprove_invariant_step

Equations

• CatCrypt.Tactics.tacticSsprove_invariant_step = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_invariant_step 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_invariant_step" false)

ssprove_rem_rel Tactic

def CatCrypt.Tactics.tacticSsprove_rem_rel : Lean.ParserDescr

ssprove_rem_rel extracts relation hypotheses from remembered values and syncs.

Given hypotheses about rem_lhs, rem_rhs, and syncsAt, this tactic derives additional hypotheses about the relationship between heap values.

Key derivations:

• From rem_lhs l v and syncsAt l, derive h₀.get l = h₁.get l and h₁.get l = v
• From rem_rhs l v and syncsAt l, derive h₀.get l = h₁.get l and h₀.get l = v
• From rem_lhs l v alone, derive h₀.get l = v
• From rem_rhs l v alone, derive h₁.get l = v
• From syncsAt l alone, derive h₀.get l = h₁.get l

Example:

example (hrem : rem_lhs l v h₀ h₁) (hsync : syncsAt l h₀ h₁) : h₁.get l = v := by
  ssprove_rem_rel

Equations

• CatCrypt.Tactics.tacticSsprove_rem_rel = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_rem_rel 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_rem_rel" false)

def CatCrypt.Tactics.tacticSsprove_rem_rel_intro : Lean.ParserDescr

ssprove_rem_rel_intro introduces and names the extracted relations.

This variant names the derived hypotheses for later use.

Equations

• CatCrypt.Tactics.tacticSsprove_rem_rel_intro = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_rem_rel_intro 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_rem_rel_intro" false)

ssprove_restore Tactic

def CatCrypt.Tactics.tacticSsprove_restore : Lean.ParserDescr

ssprove_restore is a tactic for restoring an invariant after writes.

After a sequence of writes that may have temporarily broken the invariant, this tactic attempts to show that the final state satisfies the invariant.

Common patterns:

1. Writes that "undo" previous changes
2. Writes that establish a synchronized state
3. Combining partial invariants

Example:

-- After setting the same value on both sides, syncsAt is restored
example : syncsAt l (h₀.set l v) (h₁.set l v) := by ssprove_restore

-- After writes that maintain invariant structure
example (hinv : inv h₀ h₁) : inv (h₀.set l v) (h₁.set l v) := by
  ssprove_restore

Equations

• CatCrypt.Tactics.tacticSsprove_restore = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_restore 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_restore" false)

ssprove_invariant_intro Tactic

def CatCrypt.Tactics.tacticSsprove_invariant_intro : Lean.ParserDescr

ssprove_invariant_intro introduces invariant hypotheses into context.

This is useful at the start of a relational proof to set up the invariant assumptions. It introduces the heap pair and the invariant hypothesis.

Example:

theorem example : rHoare inv c₁ c₂ post := by
  ssprove_invariant_intro
  -- Now have: h₀ h₁ : Heap, hinv : inv h₀ h₁

Equations

• CatCrypt.Tactics.tacticSsprove_invariant_intro = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_invariant_intro 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_invariant_intro" false)

def CatCrypt.Tactics.tacticSsprove_invariant_intro_named___ : Lean.ParserDescr

ssprove_invariant_intro_named h₀ h₁ hinv introduces with specific names.

Equations

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

Helper Tactics

def CatCrypt.Tactics.tacticSsprove_split_inv : Lean.ParserDescr

ssprove_split_inv splits a conjunction invariant into its components.

Equations

• CatCrypt.Tactics.tacticSsprove_split_inv = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_split_inv 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_split_inv" false)

def CatCrypt.Tactics.tacticSsprove_extract_sync : Lean.ParserDescr

ssprove_extract_sync l extracts synchronization information for location l.

Equations

• CatCrypt.Tactics.tacticSsprove_extract_sync = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_extract_sync 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_extract_sync" false)

Configuration

structure CatCrypt.Tactics.InvariantConfig : Type

Configuration for invariant tactics

• autoLocality : Bool

  Whether to automatically apply locality

• splitAnd : Bool

  Whether to split conjunction invariants

• maxDepth : ℕ

  Maximum depth for recursive tactics

• unfoldDefs : Bool

  Whether to unfold definitions aggressively

Simp Lemmas for Invariant Reasoning