The GGM reduction to one generator challenge

The expansion game consumes at most one fresh draw per adversary call. Pre-sampling a sufficient list exposes it as a test of independent samples, so the shared sequence hybrid supplies a single challenge reduction. Cached replies ignore the extra draw, preserving repeated-query consistency.

Main definitions

• Cslib.Crypto.GGM.sampleGame: a saved-list version of the expansion game.
• Cslib.Crypto.GGM.levelTest: insert one challenge at a sampled query coordinate.
• Cslib.Crypto.GGM.reduction: sample a level to obtain one uniform generator distinguisher.

Main results

• Cslib.Crypto.GGM.isPPT_reduction: strict PPT for the complete single-challenge reduction.
• Cslib.Crypto.GGM.reduction_advantage: exact loss, including at zero width and query budget.

References

• O. Goldreich, S. Goldwasser, S. Micali, How to Construct Random Functions, Section 3.3, the simulation used in the proof of Theorem 3.

Adapted from Crypto/Computational/GGM/Reduction.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, reusing the shared stateful interpreter and game API.

def Cslib.Crypto.GGM.sampleGame (generator : List Bool → List Bool) (adversary : OracleDistinguisher) (n depth : ℕ) (values : List (List Bool)) : ProbComp Bool

Run the expansion game using a saved list, consuming one entry at each adversary call. Truncation and the empty fallback make the test total on every challenge list.

theorem Cslib.Crypto.GGM.sampleGame_replicate (generator : List Bool → List Bool) (sample : ProbComp (List Bool)) (adversary : OracleDistinguisher) (n depth count : ℕ) (hqueries : ProbOracleComp.IsQueryBounded (adversary n []) count) : (OracleComp.replicate count sample >>= sampleGame generator adversary n depth).eval = (expansionGame generator sample adversary n depth).eval

A list with one independent expansion per possible query gives exactly the online game.

theorem Cslib.Crypto.GGM.isPPTOn_sampleGame {Caller : Type} {input : Caller ↪ List Bool} {generator : List Bool → List Bool} (hgenerator : Turing.MultiTapeTM.ComputableTidilyInPolyTime generator Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) {width depth : Caller → ℕ} {values : Caller → List (List Bool)} (hwidth : Turing.MultiTapeTM.ComputableTidilyInPolyTime width input Turing.MultiTapeTM.encUnary) (hdepth : Turing.MultiTapeTM.ComputableTidilyInPolyTime depth input Turing.MultiTapeTM.encUnary) (hvalues : Turing.MultiTapeTM.ComputableTidilyInPolyTime values input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) {adversary : OracleDistinguisher} (hadversary : Probability.IsOraclePPT Turing.MultiTapeTM.encBool adversary) : Probability.IsPPTOn input Turing.MultiTapeTM.encBool fun (a : Caller) => sampleGame generator adversary (width a) (depth a) (values a)

The saved-sample game is uniformly PPT, including arbitrary and short challenge lists. The shared interpreter accounts for list consumption, cache lookup and tree evaluation.

noncomputable def Cslib.Crypto.GGM.levelTest (generator : List Bool → List Bool) (adversary : OracleDistinguisher) (n depth count : ℕ) (challenge : List Bool) : ProbComp Bool

Insert one challenge among simulated uniform and generated expansions at a chosen level.

theorem Cslib.Crypto.GGM.isPPTOn_levelTest {Caller : Type} {input : Caller ↪ List Bool} {generator : List Bool → List Bool} (hgenerator : Turing.MultiTapeTM.ComputableTidilyInPolyTime generator Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) {width depth count : Caller → ℕ} {challenge : Caller → List Bool} (hwidth : Turing.MultiTapeTM.ComputableTidilyInPolyTime width input Turing.MultiTapeTM.encUnary) (hdepth : Turing.MultiTapeTM.ComputableTidilyInPolyTime depth input Turing.MultiTapeTM.encUnary) (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) (hchallenge : Turing.MultiTapeTM.ComputableTidilyInPolyTime challenge input Turing.MultiTapeTM.encBits) {adversary : OracleDistinguisher} (hadversary : Probability.IsOraclePPT Turing.MultiTapeTM.encBool adversary) : Probability.IsPPTOn input Turing.MultiTapeTM.encBool fun (a : Caller) => levelTest generator adversary (width a) (depth a) (count a) (challenge a)

The single-challenge reduction is PPT whenever its level and query budget are efficiently computed. No semantic query-bound hypothesis is needed for this efficiency certificate.

theorem Cslib.Crypto.GGM.levelTest_gap (generator : List Bool → List Bool) (adversary : OracleDistinguisher) (n depth count : ℕ) (hdepth : depth < n) (hqueries : ProbOracleComp.IsQueryBounded (adversary n []) count) : ↑(Game.succProbability (hybridGame generator adversary n depth).eval) - ↑(Game.succProbability (hybridGame generator adversary n (depth + 1)).eval) = ↑(Probability.dyadicSize count) * (↑(Game.succProbability (generator <$> BitString.sampleList n >>= levelTest generator adversary n depth count).eval) - ↑(Game.succProbability (BitString.sampleList (2 * n) >>= levelTest generator adversary n depth count).eval))

The single-challenge test captures the signed gap of adjacent GGM levels. Its loss is the dyadic sampling range for the query budget, including padding coordinates.

noncomputable def Cslib.Crypto.GGM.reduction (generator : List Bool → List Bool) (adversary : OracleDistinguisher) (count : ℕ → ℕ) : Distinguisher

Choose a level uniformly and run its single-challenge reduction. Both random choices use dyadic ranges, and unused indices reject. The query budget is a fixed function of the parameter.

theorem Cslib.Crypto.GGM.isPPT_reduction {generator : List Bool → List Bool} (hgenerator : Turing.MultiTapeTM.ComputableTidilyInPolyTime generator Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) {adversary : OracleDistinguisher} (hadversary : Probability.IsOraclePPT Turing.MultiTapeTM.encBool adversary) {count : ℕ → ℕ} (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) : Probability.IsPPT Turing.MultiTapeTM.encBool (reduction generator adversary count)

Efficient generation and an efficient query budget give one uniform PPT reduction.

theorem Cslib.Crypto.GGM.reduction_gap (generator : List Bool → List Bool) (adversary : OracleDistinguisher) (count : ℕ → ℕ) (n : ℕ) (hqueries : ProbOracleComp.IsQueryBounded (adversary n []) (count n)) : ↑(Game.succProbability (prfRealGame (eval generator) adversary n).eval) - ↑(Game.succProbability (prfIdealGame adversary n).eval) = ↑(Probability.dyadicSize n) * ↑(Probability.dyadicSize (count n)) * (↑(Game.succProbability (generator <$> BitString.sampleList n >>= reduction generator adversary count n).eval) - ↑(Game.succProbability (BitString.sampleList (2 * n) >>= reduction generator adversary count n).eval))

The GGM reduction preserves the full real/ideal signed gap up to the product of the two dyadic sampling ranges. This statement is exact, including the zero-width game.

theorem Cslib.Crypto.GGM.reduction_advantage (generator : List Bool → List Bool) (adversary : OracleDistinguisher) (count : ℕ → ℕ) (n : ℕ) (hqueries : ProbOracleComp.IsQueryBounded (adversary n []) (count n)) : Game.advantage (prfRealGame (eval generator) adversary n).eval (prfIdealGame adversary n).eval = ↑(Probability.dyadicSize n) * ↑(Probability.dyadicSize (count n)) * Game.advantage (generator <$> BitString.sampleList n >>= reduction generator adversary count n).eval (BitString.sampleList (2 * n) >>= reduction generator adversary count n).eval

The real/ideal PRF advantage is the reduction's generator advantage times the two sampling ranges. The loss is polynomial whenever the query budget is polynomial.