Fundamental Lemma of Game Playing + Multi-Query Games

This file provides three layers of game-playing infrastructure:

1. Shoup's Fundamental Lemma (bad-event lemma): if two games are identical until a "bad" event occurs, then their distinguishing advantage is bounded by the probability of the bad event.

2. Multi-query game abstraction: a generic framework for games where an adversary makes q adaptive oracle queries, with a bound Adv_q <= q * Adv_1 via the hybrid argument.

3. Lazy/eager sampling equivalence: the two standard sampling strategies for random oracles produce the same distribution.

Main Results

Fundamental Lemma

• IdenticalUntilBad -- games agree unless bad occurs
• advantage_upto_bad -- Advantage(G0, G1) <= Pr[bad] (Shoup 2004, Lemma 1)
• advantage_upto_bad_A -- adversary-parameterized version
• UpToBad -- bundled: identical-until-bad + bad probability bound
• uptobad_advantage -- extract advantage bound from UpToBad

Multi-Query Games

• MultiQueryGame -- init/query/finalize structure
• MultiQueryGame.run -- execute with q queries
• MultiQueryGame.single_to_multi_bound -- Adv_q <= q * Adv_1

Lazy/Eager Sampling

• lazy_sample -- sample on first query, cache for later
• eager_sample -- sample all values upfront
• lazy_eager_equiv -- they produce the same distribution

Cross-Validation

Property	This file	Reference
Bad-event bound	advantage_upto_bad	Shoup 2004, Lemma 1
Identical-until-bad	IdenticalUntilBad	Bellare-Rogaway 2006, Def. 1
Multi-query hybrid	single_to_multi_bound	Boneh-Shoup, Thm 4.4
Lazy/eager equiv	lazy_eager_equiv	Bellare-Rogaway 2006, Lemma 1

Equivalent formalizations:

• EasyCrypt: upto_bad tactic / Upto theory
• CryptoVerif: find_coll / event declarations
• SSProve (Rocq): rules_RHS / package composition

References

• Shoup, Sequences of Games: A Tool for Taming Complexity in Security Proofs, ePrint 2004/332, Lemma 1.
• Bellare & Rogaway, The Security of Triple Encryption and a Framework for Code-Based Game-Playing Proofs, EUROCRYPT 2006.
• Boneh & Shoup, A Graduate Course in Applied Cryptography, Ch. 4.

Identical-Until-Bad

Two computations are "identical until bad" if they produce the same output distribution conditioned on a bad event not occurring.

This is the core semantic predicate behind Shoup's fundamental lemma and the Bellare-Rogaway code-based game-playing framework.

structure CatCrypt.Crypto.BadEvent.IdenticalUntilBad (G₀ G₁ bad : Core.SPComp Bool) : Prop

Two Bool games are identical until bad if:

1. When bad does NOT happen, they produce the same output
2. The probability of bad is bounded

Formally: G₀ and G₁ are coupled such that they agree whenever a predicate ¬bad holds on the shared randomness.

The inequality G₀(b, h') ≤ G₁(b, h') + bad(true, h') captures that any excess probability mass in G₀ relative to G₁ is accounted for by the bad event. When bad doesn't fire (bad probability = 0), the two games produce identical distributions.

• agree_unless_bad (h : Core.Heap) (b : Bool) (h' : Core.Heap) : (G₀ h) (some (b, h')) ≤ (G₁ h) (some (b, h')) + (bad h) (some (true, h'))

  When bad doesn't happen, the games agree

Fundamental Lemma (Statement)

The full proof of Shoup's lemma requires a coupling argument over the joint distribution of (game output, bad event). We state the key result as an axiom and provide the proof sketch.

Proof sketch (Shoup, Lemma 1): Define events S₀, S₁ (game outputs 1) and F (bad event). Then: |Pr[S₀] - Pr[S₁]| = |Pr[S₀ ∧ ¬F] + Pr[S₀ ∧ F] - Pr[S₁ ∧ ¬F] - Pr[S₁ ∧ F]| = |Pr[S₀ ∧ F] - Pr[S₁ ∧ F]| (since S₀∧¬F = S₁∧¬F) ≤ Pr[F] (since Pr[Sᵢ ∧ F] ≤ Pr[F])

EasyCrypt proves this via the upto_bad tactic.

noncomputable def CatCrypt.Crypto.BadEvent.prFalse (G : Core.SPComp Bool) (h₀ : Core.Heap) : ENNReal

prFalse: probability of returning false (helper for Shoup's lemma).

Equations

• CatCrypt.Crypto.BadEvent.prFalse G h₀ = ∑' (h : CatCrypt.Core.Heap), (G h₀) (some (false, h))

theorem CatCrypt.Crypto.BadEvent.prTrue_prFalse_none_sum (G : Core.SPComp Bool) (h₀ : Core.Heap) : (G h₀) none + prTrue G h₀ + prFalse G h₀ = 1

prTrue + prFalse + none mass = 1 for any SPComp Bool, via PMF total mass.

theorem CatCrypt.Crypto.BadEvent.prTrue_prFalse_eq_one_of_noFail (G : Core.SPComp Bool) (h₀ : Core.Heap) (hnf : SPComp.NoFail G) : prTrue G h₀ + prFalse G h₀ = 1

Under NoFail, prTrue + prFalse = 1.

theorem CatCrypt.Crypto.BadEvent.prFalse_eq_one_sub_prTrue (G : Core.SPComp Bool) (h₀ : Core.Heap) (hnf : SPComp.NoFail G) : prFalse G h₀ = 1 - prTrue G h₀

prFalse equals 1 - prTrue under NoFail.

theorem CatCrypt.Crypto.BadEvent.advantage_upto_bad (G₀ G₁ bad : Core.SPComp Bool) (hnf₀ : SPComp.NoFail G₀) (hnf₁ : SPComp.NoFail G₁) (h : IdenticalUntilBad G₀ G₁ bad) : Advantage G₀ G₁ ≤ prTrue bad Core.Heap.empty

Shoup's Fundamental Lemma: if two games are identical until bad, then their advantage is bounded by the probability of the bad event.

Requires both G₀ and G₁ to be NoFail: without this, the IdenticalUntilBad inequality (one-directional, applied to b = true) only gives prTrue G₀ ≤ prTrue G₁ + prTrue bad. The reverse direction needs the b = false case combined with prTrue + prFalse = 1, which requires NoFail.

theorem CatCrypt.Crypto.BadEvent.advantage_upto_bad_A {α : Type} (G₀ G₁ : Core.SPComp α) (bad : Core.SPComp Bool) (hnf₀ : SPComp.NoFail G₀) (hnf₁ : SPComp.NoFail G₁) (h : ∀ (A : α → Core.SPComp Bool), IdenticalUntilBad (G₀.bind A) (G₁.bind A) bad) (A : α → Core.SPComp Bool) : (∀ (a : α), SPComp.NoFail (A a)) → AdvantageA G₀ G₁ A ≤ prTrue bad Core.Heap.empty

Bad-event lemma with adversary: if two computations are identical until bad for all adversaries, the adversary-parameterized advantage is bounded by the bad-event probability.

Hypotheses: NoFail on G₀, G₁, and (per-input) on the adversary A. These combine via SPComp.bind_noFail to give NoFail on the composed games, which advantage_upto_bad requires.

Proof strategy: For any adversary A, instantiate advantage_upto_bad on the composed games G₀.bind A and G₁.bind A.

UpToBad: Bundled Bad-Event Technique

In practice, a game-hopping step via the bad-event technique requires:

1. A proof that the two games are identical until bad
2. A bound on the probability of the bad event

The UpToBad structure bundles both, making it easy to extract the advantage bound in one step.

structure CatCrypt.Crypto.BadEvent.UpToBad (G₀ G₁ bad : Core.SPComp Bool) (ε_bad : ENNReal) : Prop

Bundled "up to bad" technique: games are identical until bad, and the bad-event probability is bounded by ε_bad. Both games must be NoFail (required by advantage_upto_bad).

• identical : IdenticalUntilBad G₀ G₁ bad

  The games are identical unless bad occurs

• noFail_left : SPComp.NoFail G₀

  G₀ never fails

• noFail_right : SPComp.NoFail G₁

  G₁ never fails

• pr_bad : prTrue bad Core.Heap.empty ≤ ε_bad

  The bad event probability is bounded

theorem CatCrypt.Crypto.BadEvent.uptobad_advantage (G₀ G₁ bad : Core.SPComp Bool) (ε_bad : ENNReal) (h : UpToBad G₀ G₁ bad ε_bad) : Advantage G₀ G₁ ≤ ε_bad

Extract the advantage bound from an UpToBad witness.

structure CatCrypt.Crypto.BadEvent.UpToBadA {α : Type} (G₀ G₁ : Core.SPComp α) (bad : Core.SPComp Bool) (ε_bad : ENNReal) : Prop

Bundled UpToBad with adversary: for adversary-parameterized games.

• identical (A : α → Core.SPComp Bool) : IdenticalUntilBad (G₀.bind A) (G₁.bind A) bad

  The games are identical until bad for all adversaries

• noFail_left : SPComp.NoFail G₀

  G₀ never fails

• noFail_right : SPComp.NoFail G₁

  G₁ never fails

• pr_bad : prTrue bad Core.Heap.empty ≤ ε_bad

  The bad event probability is bounded

theorem CatCrypt.Crypto.BadEvent.uptobadA_advantage {α : Type} (G₀ G₁ : Core.SPComp α) (bad : Core.SPComp Bool) (ε_bad : ENNReal) (h : UpToBadA G₀ G₁ bad ε_bad) (A : α → Core.SPComp Bool) : (∀ (a : α), SPComp.NoFail (A a)) → AdvantageA G₀ G₁ A ≤ ε_bad

Extract the advantage bound from an UpToBadA witness, given a NoFail-preserving adversary.

Lifting to Arbitrary Distinguishers and to sdist

The one-sided gap Pr[G₀ ; D] - Pr[G₁ ; D] of any distinguisher D, failing or not, is at most the gap of the event distinguisher that returns whether the output/heap pair has at least as much mass under G₀ as under G₁. That event distinguisher never fails, so bounds stated for non-failing distinguishers extend to all distinguishers.

theorem CatCrypt.Crypto.BadEvent.exists_noFail_tsub_le {α : Type} (G₀ G₁ : Core.SPComp α) (D : α → Core.SPComp Bool) (h₀ : Core.Heap) : ∃ (A : α → Core.SPComp Bool), (∀ (a : α), SPComp.NoFail (A a)) ∧ prTrue (G₀.bind D) h₀ - prTrue (G₁.bind D) h₀ ≤ prTrue (G₀.bind A) h₀ - prTrue (G₁.bind A) h₀

For any distinguisher D and initial heap h₀ there is a non-failing distinguisher A whose one-sided gap between G₀ and G₁ at h₀ is at least that of D.

theorem CatCrypt.Crypto.BadEvent.advantageA_le_of_noFail_distinguishers {α : Type} {G₀ G₁ : Core.SPComp α} {ε : ENNReal} (h : ∀ (A : α → Core.SPComp Bool), (∀ (a : α), SPComp.NoFail (A a)) → AdvantageA G₀ G₁ A ≤ ε) (D : α → Core.SPComp Bool) : AdvantageA G₀ G₁ D ≤ ε

An advantage bound against every non-failing distinguisher is an advantage bound against every distinguisher.

theorem CatCrypt.Crypto.BadEvent.uptobadA_advantage_all {α : Type} (G₀ G₁ : Core.SPComp α) (bad : Core.SPComp Bool) (ε_bad : ENNReal) (h : UpToBadA G₀ G₁ bad ε_bad) (D : α → Core.SPComp Bool) : AdvantageA G₀ G₁ D ≤ ε_bad

Fundamental lemma against every distinguisher: an UpToBadA witness bounds the advantage of all distinguishers, including failing ones, by the bad-event probability.

theorem CatCrypt.Crypto.BadEvent.sdist_le_of_uptobadA {α β : Type} {f g : α → Core.SPComp β} (bad : α → Core.SPComp Bool) (ε_bad : ENNReal) (hf : ∀ (a : α), (f a).IsPure) (hg : ∀ (a : α), (g a).IsPure) (h : ∀ (a : α), UpToBadA (f a) (g a) (bad a) ε_bad) : sdist f g ≤ ε_bad

Fundamental lemma as a statistical-distance bound: for families of heap-independent games that are identical until a bad event of probability at most ε_bad, sdist f g ≤ ε_bad. IsPure is needed because sdist ranges over all initial heaps while UpToBadA fixes the empty heap.

Corollary: Union Bound for Multiple Bad Events

When a proof involves multiple bad events, the union bound gives:

Pr[bad₁ ∨ bad₂ ∨ ... ∨ bad_n] ≤ Pr[bad₁] + ... + Pr[bad_n]

This composes with the fundamental lemma to give multi-hop bounds.

theorem CatCrypt.Crypto.BadEvent.prTrue_union_bound (bad₁ bad₂ : Core.SPComp Bool) (hp₁ : bad₁.IsPure) (hp₂ : bad₂.IsPure) (hnf₁ : SPComp.NoFail bad₁) (hnf₂ : SPComp.NoFail bad₂) : prTrue (do let b₁ ← bad₁ let b₂ ← bad₂ Core.SPComp.pure (b₁ || b₂)) Core.Heap.empty ≤ prTrue bad₁ Core.Heap.empty + prTrue bad₂ Core.Heap.empty

Union bound for two bad events under IsPure+NoFail: the probability of either bad event firing is at most the sum of their individual probabilities.

Hypotheses: Both bad₁ and bad₂ must be IsPure+NoFail. The bound is false without heap-purity on bad₂ — counter-example: bad₁ writes the heap and returns false, bad₂ reads the heap and returns whether it was written; then chained prTrue = 1 but prTrue bad₁ Heap.empty + prTrue bad₂ Heap.empty = 0.

Proof: Decompose prTrue(bind bad₁ k) via prTrue_isPure_noFail_bind (NomPkgBridge). The first branch (b₁=true) makes the inner expression true || _ = true so the prTrue equals bad₂'s mass = 1 (NoFail). The second branch (b₁=false) reduces to pure b₂, so the prTrue equals prTrue bad₂. Bound: d₁(true)·1 + d₁(false)·prTrue bad₂ ≤ d₁(true) + prTrue bad₂ since d₁(false) ≤ 1.

noncomputable def CatCrypt.Crypto.BadEvent.bad_union (bads : List (Core.SPComp Bool)) : Core.SPComp Bool

Union bound for a finite list of bad events.

Equations

• CatCrypt.Crypto.BadEvent.bad_union [] = CatCrypt.Core.SPComp.pure false
• CatCrypt.Crypto.BadEvent.bad_union [b] = b
• CatCrypt.Crypto.BadEvent.bad_union (b :: bs) = do let b₁ ← b let b₂ ← CatCrypt.Crypto.BadEvent.bad_union bs CatCrypt.Core.SPComp.pure (b₁ || b₂)

theorem CatCrypt.Crypto.BadEvent.prTrue_pure_false_eq_zero (h₀ : Core.Heap) : prTrue (Core.SPComp.pure false) h₀ = 0

The probability of any event in a list firing is bounded by the sum of individual probabilities (finite union bound / Boole's inequality).

Proof strategy: Induction on the list, applying prTrue_union_bound at each step to peel off one event from the disjunction.

theorem CatCrypt.Crypto.BadEvent.bad_union_isPure_noFail (bads : List (Core.SPComp Bool)) : (∀ b ∈ bads, b.IsPure) → (∀ b ∈ bads, SPComp.NoFail b) → (bad_union bads).IsPure ∧ SPComp.NoFail (bad_union bads)

bad_union of IsPure+NoFail events is itself IsPure+NoFail.

theorem CatCrypt.Crypto.BadEvent.prTrue_union_bound_list (bads : List (Core.SPComp Bool)) : (∀ b ∈ bads, b.IsPure) → (∀ b ∈ bads, SPComp.NoFail b) → prTrue (bad_union bads) Core.Heap.empty ≤ List.foldr (fun (b : Core.SPComp Bool) (acc : ENNReal) => prTrue b Core.Heap.empty + acc) 0 bads

Chaining: Bad Event + Hybrid Argument

Combining the fundamental lemma with the hybrid argument gives a powerful pattern: each hybrid step is an "identical until bad" transition, and the total advantage sums the bad-event probabilities.

theorem CatCrypt.Crypto.BadEvent.advantage_hybrid_upto_bad (G : ℕ → Core.SPComp Bool) (n : ℕ) (ε : ENNReal) (bad : ℕ → Core.SPComp Bool) (h_iub : ∀ i < n, UpToBad (G i) (G (i + 1)) (bad i) ε) : Advantage (G 0) (G n) ≤ ↑n * ε

Bad-event hybrid bound: if each of n hybrid steps is identical until bad with bad-event probability at most ε, then the total advantage is at most n * ε.

This is the standard pattern for multi-step game-hopping proofs where each step introduces a collision or failure event.

Multi-Query Game Abstraction

A generic multi-query game models the common pattern in cryptographic security definitions (IND-CPA, PRF, MAC, etc.) where an adversary interacts with an oracle over multiple rounds:

1. Initialize internal state
2. Query the oracle q times, updating state each time
3. Finalize by producing a Boolean decision

The key theorem single_to_multi_bound formalizes the standard reduction: if distinguishing a single query costs advantage ε₁, then distinguishing q queries costs at most q * ε₁.

structure CatCrypt.Crypto.BadEvent.MultiQueryGame (State Input Output : Type) : Type

A multi-query game parameterized by state, input, and output types.

This captures the structure of IND-CPA, PRF, MAC, and other multi-query security definitions. The adversary's strategy is encoded by the sequence of inputs; the game handles the internal oracle computation.

In the PRF setting:

• State = key (or ⊥ for ideal)
• Input = domain element
• Output = range element
• init = key generation (or table init)
• query = evaluate PRF (or sample random)
• finalize = adversary's decision

• init : Core.SPComp State

  Initialize the game state (e.g., key generation)

• query : State → Input → Core.SPComp (State × Output)

  Process one oracle query: takes current state and query input, returns updated state and query output

• finalize : State → Core.SPComp Bool

  Produce the final decision from the accumulated state

noncomputable def CatCrypt.Crypto.BadEvent.MultiQueryGame.run {S I O : Type} (G : MultiQueryGame S I O) (inputs : ℕ → I) (q : ℕ) : Core.SPComp Bool

Execute a multi-query game with a given sequence of inputs.

Processes q queries sequentially, threading state through each query, then finalizes. The result is a SPComp Bool suitable for computing advantage.

The recursion unfolds as:

s₀ ← init
(s₁, o₁) ← query s₀ (inputs 0)
(s₂, o₂) ← query s₁ (inputs 1)
...
(s_q, o_q) ← query s_{q-1} (inputs (q-1))
finalize s_q

Equations

• G.run inputs q = do let s₀ ← G.init let s_final ← CatCrypt.Crypto.BadEvent.MultiQueryGame.run.runQueries G.query s₀ inputs q G.finalize s_final

noncomputable def CatCrypt.Crypto.BadEvent.MultiQueryGame.run.runQueries {S I O : Type} (qry : S → I → Core.SPComp (S × O)) (s : S) (inputs : ℕ → I) : ℕ → Core.SPComp S

Helper: run q queries starting from state s, using inputs at indices 0, 1, ..., q-1.

Equations

• One or more equations did not get rendered due to their size.
• CatCrypt.Crypto.BadEvent.MultiQueryGame.run.runQueries qry s inputs 0 = CatCrypt.Core.SPComp.pure s

noncomputable def CatCrypt.Crypto.BadEvent.MultiQueryGame.runCollect {S I O : Type} (G : MultiQueryGame S I O) (q : ℕ) (inputs : Fin q → I) : Core.SPComp (S × List O)

An alternative, more explicit execution that collects all outputs.

Equations

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

noncomputable def CatCrypt.Crypto.BadEvent.MultiQueryGame.hybridQueries {S I O : Type} (qry_ideal qry_real : S → I → Core.SPComp (S × O)) (s : S) (inputs : ℕ → I) (switch : ℕ) : ℕ → Core.SPComp S

Run queries with the first switch using qry_ideal and the rest using qry_real. Helper for hybrid game construction.

Equations

• One or more equations did not get rendered due to their size.
• CatCrypt.Crypto.BadEvent.MultiQueryGame.hybridQueries qry_ideal qry_real s inputs switch 0 = CatCrypt.Core.SPComp.pure s

noncomputable def CatCrypt.Crypto.BadEvent.MultiQueryGame.hybrid {S I O : Type} (G_real G_ideal : MultiQueryGame S I O) (inputs : ℕ → I) (i q : ℕ) : Core.SPComp Bool

The i-th hybrid game between G_real and G_ideal: first i queries use the ideal oracle, remaining queries use the real oracle.

This is the standard hybrid construction for multi-query reductions:

• hybrid 0 = all-real game
• hybrid q = all-ideal game
• hybrid i and hybrid (i+1) differ in exactly one query

Assumes G_real and G_ideal share the same init and finalize (they differ only in the oracle).

Equations

• G_real.hybrid G_ideal inputs i q = do let s₀ ← G_real.init let s_mid ← CatCrypt.Crypto.BadEvent.MultiQueryGame.hybridQueries G_ideal.query G_real.query s₀ inputs i q G_real.finalize s_mid

theorem CatCrypt.Crypto.BadEvent.MultiQueryGame.single_to_multi_bound {S I O : Type} (G_real G_ideal : MultiQueryGame S I O) (inputs : ℕ → I) (q : ℕ) (ε₁ : ENNReal) (h_single : ∀ i < q, Advantage (G_real.hybrid G_ideal inputs i q) (G_real.hybrid G_ideal inputs (i + 1) q) ≤ ε₁) : Advantage (G_real.hybrid G_ideal inputs 0 q) (G_real.hybrid G_ideal inputs q q) ≤ ↑q * ε₁

Single-to-multi-query reduction: if distinguishing a single query between G_real and G_ideal costs advantage at most ε₁, then distinguishing q queries costs at most q * ε₁.

This formalizes the standard textbook reduction (Boneh-Shoup Thm 4.4): the hybrid argument interpolates between all-real and all-ideal, and each step reduces to the single-query distinguishing problem.

Proof strategy: Construct q+1 hybrid games where hybrid i uses the ideal oracle for the first i queries and the real oracle for the rest. Each adjacent pair of hybrids differs in exactly one query, so the per-step advantage is at most ε₁. Apply advantage_hybrid_uniform to sum the q steps.

Lazy/Eager Sampling Equivalence

A fundamental technique in game-playing proofs: a random oracle can be implemented either by:

• Lazy sampling: sample a random value the first time a query is made, then return the cached value on subsequent queries
• Eager sampling: sample the entire random function upfront, then look up values deterministically

These two strategies produce identical distributions. This equivalence is used pervasively in PRF, ROM, and ideal cipher proofs.

Reference: Bellare & Rogaway 2006, Lemma 1.

noncomputable def CatCrypt.Crypto.BadEvent.lazy_sample {D R : Type} [DecidableEq D] [Fintype R] [Nonempty R] (table : D → Option R) (x : D) : Core.SPComp (R × (D → Option R))

Lazy sampling oracle: maintains a partial function table : D → Option R. On query x:

• If table x = some r, return r (cached)
• If table x = none, sample r ← uniform R, update table, return r

This is the standard "program-on-the-fly" implementation of a random oracle.

Equations

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

noncomputable def CatCrypt.Crypto.BadEvent.eager_sample {D R : Type} [DecidableEq D] (f : D → R) (x : D) : Core.SPComp (R × (D → R))

Eager sampling oracle: given a total function f : D → R (sampled upfront), simply look up the value. No state update needed since everything is precomputed.

The function f is typically obtained by sampling from the uniform distribution over D → R (or equivalently, sampling each f(d) independently).

Equations

• CatCrypt.Crypto.BadEvent.eager_sample f x = CatCrypt.Core.SPComp.pure (f x, f)

noncomputable def CatCrypt.Crypto.BadEvent.lazy_process {D R : Type} [DecidableEq D] [Fintype R] [Nonempty R] : List D → (D → Option R) → Core.SPComp (List R)

Process a list of queries via lazy sampling, threading the table. Each query either returns a cached result or samples fresh.

Equations

• One or more equations did not get rendered due to their size.
• CatCrypt.Crypto.BadEvent.lazy_process [] table = CatCrypt.Core.SPComp.pure []

noncomputable def CatCrypt.Crypto.BadEvent.eager_process {D R : Type} [DecidableEq D] [Fintype R] [Nonempty R] [Fintype D] : List D → Core.SPComp (List R)

Process a list of queries via eager sampling: sample the full function upfront, then look up each query deterministically.

Equations

• CatCrypt.Crypto.BadEvent.eager_process queries = do let f ← CatCrypt.Core.SPComp.sample (D → R) CatCrypt.Core.SPComp.pure (List.map f queries)

Helpers for lazy_eager_equiv

These reduce both lazy and eager sampling to a common sequential_sample intermediate (iid R-uniforms). The lazy half is a straightforward induction; the eager half uses Equiv.piSplitAt + SDistr.uniform_bind_equiv_comp to factor uniform (D → R) into uniform R × uniform ({d // d ≠ x} → R), recursing over the queries.

noncomputable def CatCrypt.Crypto.BadEvent.sequential_sample {R : Type} [Fintype R] [Nonempty R] : ℕ → Core.SPComp (List R)

Sequential iid uniform sampling — n fresh uniforms on R, paired into a list.

Equations

• CatCrypt.Crypto.BadEvent.sequential_sample 0 = CatCrypt.Core.SPComp.pure []
• CatCrypt.Crypto.BadEvent.sequential_sample n.succ = do let r ← CatCrypt.Core.SPComp.sample R let rs ← CatCrypt.Crypto.BadEvent.sequential_sample n CatCrypt.Core.SPComp.pure (r :: rs)

theorem CatCrypt.Crypto.BadEvent.spcomp_sample_bind_const {α β : Type} [Fintype α] [Nonempty α] (c : Core.SPComp β) : ((Core.SPComp.sample α).bind fun (x : α) => c) = c

Binding sample R with a constant continuation reduces to the constant.

theorem CatCrypt.Crypto.BadEvent.lazy_process_eq_sequential {D R : Type} [DecidableEq D] [Fintype R] [Nonempty R] (qs : List D) (T : D → Option R) : qs.Nodup → (∀ q ∈ qs, T q = none) → lazy_process qs T = sequential_sample qs.length

The lazy direction of lazy_eager_equiv: lazy_process with a table that has none at every queried point (and Nodup queries) reduces to a sequential iid R-uniform sampling of queries.length values.

theorem CatCrypt.Crypto.BadEvent.spcomp_sample_bind_equiv_comp {α β γ : Type} [Fintype α] [Fintype β] [Nonempty α] [Nonempty β] (σ : α ≃ β) (k : β → Core.SPComp γ) : ((Core.SPComp.sample α).bind fun (a : α) => k (σ a)) = (Core.SPComp.sample β).bind k

SPComp-level version of SDistr.uniform_bind_equiv_comp.

theorem CatCrypt.Crypto.BadEvent.spcomp_sample_prod {A B γ : Type} [Fintype A] [Fintype B] [Nonempty A] [Nonempty B] (k : A × B → Core.SPComp γ) : (Core.SPComp.sample (A × B)).bind k = (Core.SPComp.sample A).bind fun (a : A) => (Core.SPComp.sample B).bind fun (b : B) => k (a, b)

SPComp-level: sampling a product type equals nested independent samples.

theorem CatCrypt.Crypto.BadEvent.sample_fin_ofFn_eq_sequential {R : Type} [Fintype R] [Nonempty R] (n : ℕ) : ((Core.SPComp.sample (Fin n → R)).bind fun (g : Fin n → R) => Core.SPComp.pure (List.ofFn g)) = sequential_sample n

Sampling uniformly from Fin n → R then taking List.ofFn equals sequential iid sampling of n uniforms.

noncomputable def CatCrypt.Crypto.BadEvent.qsBij {D R : Type} [DecidableEq D] [Fintype D] (qs : List D) (hnodup : qs.Nodup) : (D → R) ≃ (Fin qs.length → R) × ({ d : D // d ∉ qs } → R)

The bijection (D → R) ≃ (Fin qs.length → R) × ({d // d ∉ qs} → R) for Nodup qs. The first component picks out values at qs-indexed positions; the second component holds values at non-qs points.

Equations

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

theorem CatCrypt.Crypto.BadEvent.qsBij_symm_map {D R : Type} [DecidableEq D] [Fintype D] (qs : List D) (hnodup : qs.Nodup) (g : Fin qs.length → R) (h : { d : D // d ∉ qs } → R) : List.map ((qsBij qs hnodup).symm (g, h)) qs = List.ofFn g

Under qsBij.symm (g, h), qs.map reduces to List.ofFn g — the non-qs component h is unused since qs.map only accesses qs-indexed values.

theorem CatCrypt.Crypto.BadEvent.eager_process_eq_sequential {D R : Type} [DecidableEq D] [Fintype D] [Fintype R] [Nonempty R] (qs : List D) (hnodup : qs.Nodup) : eager_process qs = sequential_sample qs.length

Eager direction of lazy_eager_equiv.

theorem CatCrypt.Crypto.BadEvent.lazy_eager_equiv {D R : Type} [DecidableEq D] [Fintype D] [Fintype R] [Nonempty R] (queries : List D) (hnodup : queries.Nodup) (h₀ : Core.Heap) : lazy_process queries (fun (x : D) => none) h₀ = eager_process queries h₀

Lazy/eager sampling equivalence: for any sequence of distinct queries, the lazy and eager sampling strategies produce the same joint distribution over outputs.

Composes lazy_process_eq_sequential (proven) and eager_process_eq_sequential (deferred, see its docstring) via the common sequential_sample intermediate.

This is Bellare-Rogaway 2006, Lemma 1 (also implicit in Shoup 2004).

theorem CatCrypt.Crypto.BadEvent.lazy_sample_fresh_eq_uniform {D R : Type} [DecidableEq D] [Fintype R] [Nonempty R] (x : D) : lazy_sample (fun (x : D) => none) x = do let r ← Core.SPComp.sample R Core.SPComp.pure (r, fun (d : D) => if d = x then some r else (fun (x : D) => none) d)

Single-query lazy/eager equivalence: for a single query x on an empty table, lazy sampling and uniform sampling produce the same distribution.

This is the base case of the full lazy/eager equivalence.

Composition: Bad Event + Lazy/Eager

A common proof pattern combines the bad-event lemma with lazy/eager equivalence:

1. Replace eager sampling with lazy sampling (zero cost, by lazy_eager_equiv)
2. Introduce a bad event (collision, etc.)
3. Bound the game transition by the bad-event probability

This pattern appears in PRF, MAC, and signature security proofs.

theorem CatCrypt.Crypto.BadEvent.lazy_eager_upto_bad (G_lazy G_eager bad : Core.SPComp Bool) (ε : ENNReal) (h_iub : IdenticalUntilBad G_lazy G_eager bad) (hnf_l : SPComp.NoFail G_lazy) (hnf_e : SPComp.NoFail G_eager) (h_bad : prTrue bad Core.Heap.empty ≤ ε) : Advantage G_lazy G_eager ≤ ε

Lazy-to-eager via bad event: if a game using lazy sampling is identical-until-bad to a game using eager sampling (where bad = collision), then the advantage is bounded by the collision probability.

This combines lazy_eager_equiv with advantage_upto_bad. NoFail hypotheses are required by the (now-proven) advantage_upto_bad.