Triangle Inequality Tactic

This file provides the ssprove_triangle tactic for game-hopping proofs.

Main definitions

• advantage_sum - Recursive sum of pairwise advantages for a chain of games
• Advantage_triangle_chain - Triangle inequality for chains of games
• ssprove_triangle - Tactic to introduce a triangle inequality bound

Usage

The tactic ssprove_triangle G₀ [G₁, G₂, G₃] G₄ produces:

ineq : Advantage G₀ G₄ ≤
       Advantage G₀ G₁ + Advantage G₁ G₂ +
       Advantage G₂ G₃ + Advantage G₃ G₄

This is essential for game-hopping proofs where we transition through a sequence of hybrid games.

References

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

Advantage Sum

noncomputable def CatCrypt.Crypto.advantage_sum (G₀ : Core.SPComp Bool) (gs : List (Core.SPComp Bool)) (Gn : Core.SPComp Bool) : ENNReal

Recursive sum of pairwise advantages for a chain of games.

advantage_sum G₀ [G₁, G₂] G₃ = Advantage G₀ G₁ + Advantage G₁ G₂ + Advantage G₂ G₃

The base case advantage_sum G₀ [] G₁ = Advantage G₀ G₁.

Equations

• CatCrypt.Crypto.advantage_sum G₀ [] Gn = CatCrypt.Crypto.Advantage G₀ Gn
• CatCrypt.Crypto.advantage_sum G₀ (G₁ :: rest) Gn = CatCrypt.Crypto.Advantage G₀ G₁ + CatCrypt.Crypto.advantage_sum G₁ rest Gn

theorem CatCrypt.Crypto.Advantage_triangle_chain (G₀ : Core.SPComp Bool) (gs : List (Core.SPComp Bool)) (Gn : Core.SPComp Bool) : Advantage G₀ Gn ≤ advantage_sum G₀ gs Gn

Triangle inequality for chains of games.

For any sequence of games G₀, G₁, ..., Gₙ: Advantage G₀ Gₙ ≤ Advantage G₀ G₁ + Advantage G₁ G₂ + ... + Advantage Gₙ₋₁ Gₙ

AdvantageA Sum

noncomputable def CatCrypt.Crypto.advantageA_sum {α : Type} (G₀ : Core.SPComp α) (gs : List (Core.SPComp α)) (Gn : Core.SPComp α) (A : α → Core.SPComp Bool) : ENNReal

Recursive sum of pairwise advantages with explicit adversary.

Equations

• CatCrypt.Crypto.advantageA_sum G₀ [] Gn A = CatCrypt.Crypto.AdvantageA G₀ Gn A
• CatCrypt.Crypto.advantageA_sum G₀ (G₁ :: rest) Gn A = CatCrypt.Crypto.AdvantageA G₀ G₁ A + CatCrypt.Crypto.advantageA_sum G₁ rest Gn A

theorem CatCrypt.Crypto.advantageA_triangle {α : Type} (G₀ G₁ G₂ : Core.SPComp α) (A : α → Core.SPComp Bool) : AdvantageA G₀ G₂ A ≤ AdvantageA G₀ G₁ A + AdvantageA G₁ G₂ A

Triangle inequality for AdvantageA.

theorem CatCrypt.Crypto.AdvantageA_triangle_chain {α : Type} (G₀ : Core.SPComp α) (gs : List (Core.SPComp α)) (Gn : Core.SPComp α) (A : α → Core.SPComp Bool) : AdvantageA G₀ Gn A ≤ advantageA_sum G₀ gs Gn A

Triangle inequality for chains with explicit adversary.

Convenience Lemmas for Simplification

@[simp]

theorem CatCrypt.Crypto.advantage_sum_nil (G₀ Gn : Core.SPComp Bool) : advantage_sum G₀ [] Gn = Advantage G₀ Gn

Simplification lemma: expand advantage_sum for the empty list case

@[simp]

theorem CatCrypt.Crypto.advantage_sum_cons (G₀ G₁ : Core.SPComp Bool) (rest : List (Core.SPComp Bool)) (Gn : Core.SPComp Bool) : advantage_sum G₀ (G₁ :: rest) Gn = Advantage G₀ G₁ + advantage_sum G₁ rest Gn

Simplification lemma: expand advantage_sum for the cons case

@[simp]

theorem CatCrypt.Crypto.advantageA_sum_nil {α : Type} (G₀ Gn : Core.SPComp α) (A : α → Core.SPComp Bool) : advantageA_sum G₀ [] Gn A = AdvantageA G₀ Gn A

Simplification lemma: expand advantageA_sum for the empty list case

@[simp]

theorem CatCrypt.Crypto.advantageA_sum_cons {α : Type} (G₀ G₁ : Core.SPComp α) (rest : List (Core.SPComp α)) (Gn : Core.SPComp α) (A : α → Core.SPComp Bool) : advantageA_sum G₀ (G₁ :: rest) Gn A = AdvantageA G₀ G₁ A + advantageA_sum G₁ rest Gn A

Simplification lemma: expand advantageA_sum for the cons case

Triangle Tactic Implementation

The ssprove_triangle tactic automates the application of triangle inequality for game-hopping proofs.

Syntax

ssprove_triangle G₀ [G₁, G₂, G₃] G₄

This introduces a hypothesis ineq with type:

Advantage G₀ G₄ ≤ Advantage G₀ G₁ + Advantage G₁ G₂ + Advantage G₂ G₃ + Advantage G₃ G₄

After introduction, use simp only [advantage_sum_nil, advantage_sum_cons] at ineq to expand the sum into individual advantage terms.

Variants

• ssprove_triangle_A - For games with explicit adversary AdvantageA

def CatCrypt.Tactics.tacticSsprove_triangle___ : Lean.ParserDescr

ssprove_triangle G₀ gs Gₙ introduces a hypothesis ineq : Advantage G₀ Gₙ ≤ advantage_sum G₀ gs Gₙ

Where gs is a list of intermediate games.

After introducing the hypothesis, use: simp only [advantage_sum_nil, advantage_sum_cons] at ineq to expand the sum into individual pairwise advantages.

This is the main tactic for game-hopping proofs where we need to bound the advantage through a sequence of hybrid games.

Equations

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

def CatCrypt.Tactics.tacticSsprove_triangle_A____ : Lean.ParserDescr

ssprove_triangle_A G₀ gs Gₙ A for AdvantageA.

Produces: ineq : AdvantageA G₀ Gₙ A ≤ advantageA_sum G₀ gs Gₙ A

Equations

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

def CatCrypt.Tactics.tacticSsprove_triangle_simpl : Lean.ParserDescr

ssprove_triangle_simpl simplifies advantage_sum expressions.

After ssprove_triangle, the bound is in terms of advantage_sum. This tactic expands it into explicit pairwise advantages.

Usage: ssprove_triangle_simpl or ssprove_triangle_simpl at h

Equations

• CatCrypt.Tactics.tacticSsprove_triangle_simpl = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_triangle_simpl 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_triangle_simpl" false)

def CatCrypt.Tactics.tacticSsprove_triangle_simplAt_ : Lean.ParserDescr

ssprove_triangle_simpl at h simplifies advantage_sum in hypothesis h.

Equations

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

def CatCrypt.Tactics.«tacticAdv_game_hop[_,,]» : Lean.ParserDescr

adv_game_hop [G₁, …, Gₙ₋₁] — the n-ary shallow game-hopping tactic. On a goal AdvantageA G₀ Gₙ A ≤ ε₁ + … + εₙ, insert the intermediate games and reduce to one per-hop subgoal AdvantageA Gᵢ Gᵢ₊₁ A ≤ εᵢ₊₁ each. Each hop is then typically a reduction, discharged by ShallowModule.advantageA_absorb down to a component advantage. The advantage-level analog of game_hop (which is sdist-level and stays in the dev UC layer).

Equations

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