An executable finite-list oracle for the PRF ideal game

Valid queries are memoized as ordinary words. Malformed queries receive the empty word and retain the cache. Injective key representations and the shared eager/lazy theorem identify this program with the ideal PRF game for every randomized adaptive adversary.

Main definitions

• Cslib.Crypto.cachedRandomFunctionOracle: a list cache with fair-bit sampling on misses.

Main results

• Cslib.Crypto.prfIdealGame_eq_cached: exact equality of the eager and cached experiments.
• Cslib.Crypto.isPPT_prfIdealGame: a strict PPT realization for every oracle-PPT adversary.

References

• O. Goldreich, S. Goldwasser, S. Micali, How to Construct Random Functions.

Adapts Crypto/Computational/PseudorandomFunction/RandomOracle.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8 to the shared typed interpreter.

noncomputable def Cslib.Crypto.cachedRandomFunctionOracle (n : ℕ) (query : List Bool) : StateT (List (List Bool × List Bool)) ProbComp (List Bool)

Memoize sampled words on valid queries, rejecting malformed words without altering the cache.

theorem Cslib.Crypto.isPPTOn_cachedRandomFunctionOracle {α : Type} {input : α ↪ List Bool} {parameter : α → ℕ} {query : α → List Bool} {cache : α → List (List Bool × List Bool)} (hparameter : Turing.MultiTapeTM.ComputableTidilyInPolyTime parameter input Turing.MultiTapeTM.encUnary) (hquery : Turing.MultiTapeTM.ComputableTidilyInPolyTime query input Turing.MultiTapeTM.encBits) (hcache : Turing.MultiTapeTM.ComputableTidilyInPolyTime cache input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits))) : Probability.IsPPTOn input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits))) fun (a : α) => cachedRandomFunctionOracle (parameter a) (query a) (cache a)

Each cached call charges the parameter, query and complete input and output cache.

theorem Cslib.Crypto.prfIdealGame_eq_cached (adversary : OracleDistinguisher) (n : ℕ) : (prfIdealGame adversary n).eval = (Prod.fst <$> (OracleComp.interpret (ProbOracleComp.handler (fun (k : ℕ) => StateT.lift (ProbComp.unifFin k)) fun (request : Unit × List Bool) => cachedRandomFunctionOracle n request.2) (adversary n [])).run []).eval

An executable list cache realizes the ideal experiment, preserving repeated-query consistency and independent private randomness under arbitrary adaptive interaction.

theorem Cslib.Crypto.isPPT_prfIdealGame {adversary : OracleDistinguisher} (hadversary : Probability.IsOraclePPT Turing.MultiTapeTM.encBool adversary) : Probability.IsPPT Turing.MultiTapeTM.encBool fun (n : ℕ) (x : List Bool) => prfIdealGame adversary n

The ideal experiment has a strict PPT realization through its lazy cache. This does not construct the exponentially large eager table; the entire adaptive interaction is certified.