Documentation

CatCryptCore.Unary.FailureEvent

Enhanced Failure Event Lemma Variants #

This file provides enhanced variants of the Failure Event Lemma (FEL) from Bridge.lean, tailored to common use patterns in cryptographic security proofs.

Main results #

Direct advantage bounds #

Game hopping chains #

Event-based FEL #

Composition lemmas #

References #

Direct Advantage Bounds #

source
theorem CatCrypt.Unary.advantage_le_prBad (G₀ G₁ : Core.SPComp Bool) (bad : Core.Heap → Prop) (h_agree : ∀ (b : Bool) (h' : Core.Heap), ¬bad h' → (G₀ Core.Heap.empty) (some (b, h')) = (G₁ Core.Heap.empty) (some (b, h'))) (hll₀ : isLossless G₀) :
Crypto.Advantage G₀ G₁ ≤ prEventComp G₀ Core.Heap.empty fun (x : Bool) (h' : Core.Heap) => bad h'

The Failure Event Lemma stated directly as an Advantage bound.

Advantage G₀ G₁ ≤ Pr[G₀ : bad]

when G₀ and G₁ agree on all non-bad outcomes and G₀ is lossless. This wraps failure_event_lemma with the standard Heap.empty initial heap.

source
theorem CatCrypt.Unary.advantage_le_prBad_right (G₀ G₁ : Core.SPComp Bool) (bad : Core.Heap → Prop) (h_agree : ∀ (b : Bool) (h' : Core.Heap), ¬bad h' → (G₀ Core.Heap.empty) (some (b, h')) = (G₁ Core.Heap.empty) (some (b, h'))) (hll₁ : isLossless G₁) :
Crypto.Advantage G₀ G₁ ≤ prEventComp G₁ Core.Heap.empty fun (x : Bool) (h' : Core.Heap) => bad h'

FEL from the right side: Advantage G₀ G₁ ≤ Pr[G₁ : bad].

Symmetric to advantage_le_prBad, but bounds by the bad probability under G₁ (using G₁'s losslessness). Follows from failure_event_lemma applied to (G₁, G₀) and using commutativity of Advantage.

source
theorem CatCrypt.Unary.advantageA_le_prBad {α : Type} (G₀ G₁ : Core.SPComp α) (A : α → Core.SPComp Bool) (bad : Core.Heap → Prop) (h_agree : ∀ (b : Bool) (h' : Core.Heap), ¬bad h' → (G₀.bind A Core.Heap.empty) (some (b, h')) = (G₁.bind A Core.Heap.empty) (some (b, h'))) (hll₀ : isLossless (G₀.bind A)) :
Crypto.AdvantageA G₀ G₁ A ≤ prEventComp (G₀.bind A) Core.Heap.empty fun (x : Bool) (h' : Core.Heap) => bad h'

FEL for AdvantageA with an explicit adversary.

When the composed games G₀.bind A and G₁.bind A agree on non-bad outcomes, the advantage through A is bounded by the bad-event probability.

source
theorem CatCrypt.Unary.advantage_le_prBad_union (G₀ G₁ : Core.SPComp Bool) (bad₀ bad₁ : Core.Heap → Prop) (h_agree : ∀ (b : Bool) (h' : Core.Heap), ¬bad₀ h' → ¬bad₁ h' → (G₀ Core.Heap.empty) (some (b, h')) = (G₁ Core.Heap.empty) (some (b, h'))) (hll₀ : isLossless G₀) :
Crypto.Advantage G₀ G₁ ≤ prEventComp G₀ Core.Heap.empty fun (x : Bool) (h' : Core.Heap) => bad₀ h' ∨ bad₁ h'

FEL with union of bad events: bound by Pr[G₀ : bad₀ ∨ bad₁].

When games agree on outcomes where neither bad₀ nor bad₁ holds, bound the advantage by the probability of either bad event. The union bound then gives Pr[bad₀ ∨ bad₁] ≤ Pr[bad₀] + Pr[bad₁] (use prEvent_union_le from Event.lean for that step).

Game Hopping Chains #

source
theorem CatCrypt.Unary.advantage_le_two_bad (G₀ G₁ G₂ : Core.SPComp Bool) (bad₀₁ bad₁₂ : Core.Heap → Prop) (h_agree₀₁ : ∀ (b : Bool) (h' : Core.Heap), ¬bad₀₁ h' → (G₀ Core.Heap.empty) (some (b, h')) = (G₁ Core.Heap.empty) (some (b, h'))) (h_agree₁₂ : ∀ (b : Bool) (h' : Core.Heap), ¬bad₁₂ h' → (G₁ Core.Heap.empty) (some (b, h')) = (G₂ Core.Heap.empty) (some (b, h'))) (hll₀ : isLossless G₀) (hll₁ : isLossless G₁) :
Crypto.Advantage G₀ G₂ ≤ (prEventComp G₀ Core.Heap.empty fun (x : Bool) (h' : Core.Heap) => bad₀₁ h') + prEventComp G₁ Core.Heap.empty fun (x : Bool) (h' : Core.Heap) => bad₁₂ h'

Two-step game hopping via FEL.

Advantage G₀ G₂ ≤ Pr[G₀:bad₀₁] + Pr[G₁:bad₁₂]

when G₀ ≈ G₁ (up to bad₀₁) and G₁ ≈ G₂ (up to bad₁₂).

source
theorem CatCrypt.Unary.advantage_le_three_bad (G₀ G₁ G₂ G₃ : Core.SPComp Bool) (bad₀₁ bad₁₂ bad₂₃ : Core.Heap → Prop) (h_agree₀₁ : ∀ (b : Bool) (h' : Core.Heap), ¬bad₀₁ h' → (G₀ Core.Heap.empty) (some (b, h')) = (G₁ Core.Heap.empty) (some (b, h'))) (h_agree₁₂ : ∀ (b : Bool) (h' : Core.Heap), ¬bad₁₂ h' → (G₁ Core.Heap.empty) (some (b, h')) = (G₂ Core.Heap.empty) (some (b, h'))) (h_agree₂₃ : ∀ (b : Bool) (h' : Core.Heap), ¬bad₂₃ h' → (G₂ Core.Heap.empty) (some (b, h')) = (G₃ Core.Heap.empty) (some (b, h'))) (hll₀ : isLossless G₀) (hll₁ : isLossless G₁) (hll₂ : isLossless G₂) :
Crypto.Advantage G₀ G₃ ≤ ((prEventComp G₀ Core.Heap.empty fun (x : Bool) (h' : Core.Heap) => bad₀₁ h') + prEventComp G₁ Core.Heap.empty fun (x : Bool) (h' : Core.Heap) => bad₁₂ h') + prEventComp G₂ Core.Heap.empty fun (x : Bool) (h' : Core.Heap) => bad₂₃ h'

Three-step game hopping via FEL.

Advantage G₀ G₃ ≤ Pr[G₀:bad₀₁] + Pr[G₁:bad₁₂] + Pr[G₂:bad₂₃]

A common pattern in cryptographic proofs (e.g., PRF/PRP switching).

Event-Based FEL #

source
theorem CatCrypt.Unary.prEvent_diff_le_prBad (G₀ G₁ : Core.SPComp Bool) (h₀ : Core.Heap) (E : Bool → Core.Heap → Prop) (bad : Core.Heap → Prop) (h_agree : ∀ (b : Bool) (h' : Core.Heap), ¬bad h' → (G₀ h₀) (some (b, h')) = (G₁ h₀) (some (b, h'))) (hll₀ : isLosslessIf (fun (h : Core.Heap) => h = h₀) G₀) :
max (prEventComp G₀ h₀ E - prEventComp G₁ h₀ E) (prEventComp G₁ h₀ E - prEventComp G₀ h₀ E) ≤ prEventComp G₀ h₀ fun (x : Bool) (h' : Core.Heap) => bad h'

FEL for arbitrary events: |Pr[G₀:E] - Pr[G₁:E]| ≤ Pr[G₀:bad].

This generalizes the standard FEL from prTrue (event b=true) to any event E on the output value and heap. When G₀ and G₁ agree on non-bad outcomes, the probabilities of any event E also agree up to the bad probability.

source
theorem CatCrypt.Unary.prEvent_agree_of_no_bad (G₀ G₁ : Core.SPComp Bool) (h₀ : Core.Heap) (E : Bool → Core.Heap → Prop) (h_agree : ∀ (b : Bool) (h' : Core.Heap), (G₀ h₀) (some (b, h')) = (G₁ h₀) (some (b, h'))) :
prEventComp G₀ h₀ E = prEventComp G₁ h₀ E

When games agree on all outcomes, event probabilities agree exactly.

Composition Lemmas #

source
theorem CatCrypt.Unary.agree_trans (G₀ G₁ G₂ : Core.SPComp Bool) (h₀ : Core.Heap) (bad₁ bad₂ : Core.Heap → Prop) (h₁ : ∀ (b : Bool) (h' : Core.Heap), ¬bad₁ h' → (G₀ h₀) (some (b, h')) = (G₁ h₀) (some (b, h'))) (h₂ : ∀ (b : Bool) (h' : Core.Heap), ¬bad₂ h' → (G₁ h₀) (some (b, h')) = (G₂ h₀) (some (b, h'))) (b : Bool) (h' : Core.Heap) :
¬bad₁ h' → ¬bad₂ h' → (G₀ h₀) (some (b, h')) = (G₂ h₀) (some (b, h'))

Transitivity of up-to-bad reasoning: if G₀ ≈ G₁ up to bad₁ and G₁ ≈ G₂ up to bad₂, then G₀ ≈ G₂ when neither bad holds.

source
theorem CatCrypt.Unary.agree_bind_right {α : Type} (c : Core.SPComp α) (G₀ G₁ : α → Core.SPComp Bool) (h₀ : Core.Heap) (bad : Core.Heap → Prop) (h_agree : ∀ (a : α) (h₁ : Core.Heap) (b : Bool) (h' : Core.Heap), ¬bad h' → (G₀ a h₁) (some (b, h')) = (G₁ a h₁) (some (b, h'))) (b : Bool) (h' : Core.Heap) :
¬bad h' → (c.bind G₀ h₀) (some (b, h')) = (c.bind G₁ h₀) (some (b, h'))

If games agree on non-bad outcomes, adding the same prefix preserves agreement.

When c is a shared prefix computation and G₀, G₁ are continuations that agree on non-bad outcomes, then c.bind G₀ and c.bind G₁ also agree on non-bad outcomes.

source
theorem CatCrypt.Unary.agree_bind_left {α : Type} (f₁ f₂ : Core.SPComp α) (k : α → Core.SPComp Bool) (h₀ : Core.Heap) (bad : Core.Heap → Prop) (h_agree : ∀ (a : α) (h₁ : Core.Heap), ¬bad h₁ → (f₁ h₀) (some (a, h₁)) = (f₂ h₀) (some (a, h₁))) (h_bad_bwd : ∀ (a : α) (h₁ : Core.Heap) (b : Bool) (h₂ : Core.Heap), (k a h₁) (some (b, h₂)) ≠ 0 → ¬bad h₂ → ¬bad h₁) (b : Bool) (h' : Core.Heap) :
¬bad h' → (f₁.bind k h₀) (some (b, h')) = (f₂.bind k h₀) (some (b, h'))

Different prefixes with the same continuation: if two prefixes agree on non-bad intermediate states and bad is backward-monotone through the continuation, then the composed computations agree on non-bad outcomes.

Backward monotonicity means: if the output of k a h₁ can reach a non-bad final state h₂, then the intermediate state h₁ was also non-bad.

This is the dual of agree_bind_right, where the CONTINUATION differs and the prefix is shared. Together, these compose into agree_bind_both.

source
theorem CatCrypt.Unary.agree_bind_both {α : Type} (f₁ f₂ : Core.SPComp α) (k₁ k₂ : α → Core.SPComp Bool) (h₀ : Core.Heap) (bad : Core.Heap → Prop) (h_prefix : ∀ (a : α) (h₁ : Core.Heap), ¬bad h₁ → (f₁ h₀) (some (a, h₁)) = (f₂ h₀) (some (a, h₁))) (h_cont : ∀ (a : α) (h₁ : Core.Heap) (b : Bool) (h₂ : Core.Heap), ¬bad h₂ → (k₁ a h₁) (some (b, h₂)) = (k₂ a h₁) (some (b, h₂))) (h_bad_bwd : ∀ (a : α) (h₁ : Core.Heap) (b : Bool) (h₂ : Core.Heap), (k₁ a h₁) (some (b, h₂)) ≠ 0 → ¬bad h₂ → ¬bad h₁) (b : Bool) (h' : Core.Heap) :
¬bad h' → (f₁.bind k₁ h₀) (some (b, h')) = (f₂.bind k₂ h₀) (some (b, h'))

General composition: both prefix and continuation may differ.

If two prefixes agree on non-bad intermediate states, two continuations agree on non-bad final states, and bad is backward-monotone through the first continuation, then the composed computations agree on non-bad outcomes.

This combines the patterns of agree_bind_left and agree_bind_right. It is the key building block for up-to-bad reasoning with oracle composition.

source
theorem CatCrypt.Unary.prBad_le_of_agree (G₀ G₁ : Core.SPComp Bool) (h₀ : Core.Heap) (bad : Core.Heap → Prop) (h_agree : ∀ (b : Bool) (h' : Core.Heap), ¬bad h' → (G₀ h₀) (some (b, h')) = (G₁ h₀) (some (b, h'))) (hll₀ : isLosslessIf (fun (h : Core.Heap) => h = h₀) G₀) :
(prEventComp G₁ h₀ fun (x : Bool) (h' : Core.Heap) => bad h') ≤ prEventComp G₀ h₀ fun (x : Bool) (h' : Core.Heap) => bad h'

FEL variant: if games agree on non-bad outcomes and both sides are lossless, then bad mass is the same in both games.

This is a helper for proofs that need to move between Pr[G₀:bad] and Pr[G₁:bad].

source
theorem CatCrypt.Unary.prBad_eq_of_agree (G₀ G₁ : Core.SPComp Bool) (h₀ : Core.Heap) (bad : Core.Heap → Prop) (h_agree : ∀ (b : Bool) (h' : Core.Heap), ¬bad h' → (G₀ h₀) (some (b, h')) = (G₁ h₀) (some (b, h'))) (hll₀ : isLosslessIf (fun (h : Core.Heap) => h = h₀) G₀) (hll₁ : isLosslessIf (fun (h : Core.Heap) => h = h₀) G₁) :
(prEventComp G₀ h₀ fun (x : Bool) (h' : Core.Heap) => bad h') = prEventComp G₁ h₀ fun (x : Bool) (h' : Core.Heap) => bad h'

When both games are lossless and agree on non-bad outcomes, their bad-event probabilities are equal.

Combines prBad_le_of_agree in both directions.