Lazy random functions with independent private randomness

The eager/lazy completion law also holds for clients interleaving external queries with fresh private finite-uniform samples. Only external replies are cached. The joint law retains the client's result and the completed table, including when a private sample or an earlier reply determines a later query.

Main results

• Cslib.RandomOracle.run_interpret_answer_complete_prob: the full joint completion law.
• Cslib.RandomOracle.interpret_prob_eq_lazy: the marginal eager/lazy equivalence.
• Cslib.RandomOracle.uniform_interpret_prob_eq_lazy: specialization to a uniform random function.
• Cslib.RandomOracle.run_interpret_memoize_prob: the list cache implements the partial table.
• Cslib.RandomOracle.memoize_cache_bounds_prob: external budgets control the list cache.
• Cslib.RandomOracle.eval_run_interpret_memoize_prob: closed samplers realize the list cache.
• Cslib.RandomOracle.interpret_prob_eq_memoize_map: injective representations preserve the game.

References

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

Extends the crypto-branch lazy-sampling proof at 5ff69ca93402e7c947208dc56396d6d86203ccd8 to the disjoint-sum interface of ProbOracleComp, reusing the general state simulation rule.

theorem Cslib.RandomOracle.memoize_cache_bounds_prob {Query Value α : Type} [BEq Query] (distribution : Query → PMF Value) (program : ProbOracleComp (fun (x : Query) => Value) α) (size : Query → ℕ) (calls maxSize : ℕ) (hcalls : program.IsQueryBounded calls) (hsize : ProbOracleComp.QueriesSatisfy (fun (x : Query) => size x ≤ maxSize) program) (cache cache' : List (Query × Value)) (result : α) (h : (result, cache') ∈ ((OracleComp.interpret (ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) (memoize distribution)) program).run cache).support) : cache'.length ≤ cache.length + calls ∧ ∀ entry ∈ cache', entry ∈ cache ∨ size entry.1 ≤ maxSize ∧ entry.2 ∈ (distribution entry.1).support

External query budgets control cache growth and new-entry provenance for randomized clients. Preassigned entries are retained regardless of the sampling distribution's support.

theorem Cslib.RandomOracle.run_interpret_memoize_prob {Query Value α : Type} [BEq Query] [LawfulBEq Query] [DecidableEq Query] (distribution : Query → PMF Value) (program : ProbOracleComp (fun (x : Query) => Value) α) (cache : List (Query × Value)) : PMF.map (fun (x : α × List (Query × Value)) => match x with | (result, cache') => (result, ofList cache')) ((OracleComp.interpret (ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) (memoize distribution)) program).run cache) = (OracleComp.interpret (ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) (answer distribution)) program).run (ofList cache)

List memoization implements the mathematical random oracle for clients with private samples, retaining the result and represented final cache even over infinite query domains.

theorem Cslib.RandomOracle.eval_run_interpret_memoize_prob {Query Value α : Type} [BEq Query] [LawfulBEq Query] [DecidableEq Query] (compute : Query → ProbComp Value) (program : ProbOracleComp (fun (x : Query) => Value) α) (cache : List (Query × Value)) : PMF.map (fun (x : α × List (Query × Value)) => match x with | (result, cache') => (result, ofList cache')) ((OracleComp.interpret (ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (ProbComp.unifFin n)) (memoize compute)) program).run cache).eval = (OracleComp.interpret (ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) (answer fun (q : Query) => (compute q).eval)) program).run (ofList cache)

Closed samplers and the client's private randomness implement the same joint result/cache law as the mathematical lazy oracle. Only external requests are memoized.

theorem Cslib.RandomOracle.run_interpret_answer_complete_prob {Query α : Type} {Response : Query → Type} [Fintype Query] [∀ (q : Query), Finite (Response q)] [DecidableEq Query] (distribution : (q : Query) → PMF (Response q)) (program : ProbOracleComp Response α) (cache : Cache Response) : (do let __x ← (OracleComp.interpret (ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) (answer distribution)) program).run cache match __x with | (result, cache') => PMF.map (fun (x : (q : Query) → Response q) => (result, x)) (complete distribution cache')) = do let table ← complete distribution cache PMF.map (fun (x : α) => (x, table)) (OracleComp.interpret (ProbOracleComp.handler ProbComp.unifOracle fun (q : Query) => PMF.pure (table q)) program)

Complete the cache before or after a client with fresh private randomness: the joint result and complete-table distributions agree, even for arbitrary preassigned cache entries.

theorem Cslib.RandomOracle.interpret_prob_eq_lazy {Query α : Type} {Response : Query → Type} [Fintype Query] [∀ (q : Query), Finite (Response q)] [DecidableEq Query] (distribution : (q : Query) → PMF (Response q)) (program : ProbOracleComp Response α) : (do let table ← Probability.PMF.pi distribution OracleComp.interpret (ProbOracleComp.handler ProbComp.unifOracle fun (q : Query) => PMF.pure (table q)) program) = PMF.map Prod.fst ((OracleComp.interpret (ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) (answer distribution)) program).run fun (x : Query) => none)

Lazy sampling from an empty cache implements the eager table experiment for randomized, adaptive clients, with private randomness independent of the table.

theorem Cslib.RandomOracle.uniform_interpret_prob_eq_lazy {Query α : Type} {Response : Query → Type} [Fintype Query] [∀ (q : Query), Finite (Response q)] [DecidableEq Query] [(q : Query) → Fintype (Response q)] [∀ (q : Query), Nonempty (Response q)] (program : ProbOracleComp Response α) : (do let table ← Probability.PMF.uniformOfFintype ((q : Query) → Response q) OracleComp.interpret (ProbOracleComp.handler ProbComp.unifOracle fun (q : Query) => PMF.pure (table q)) program) = PMF.map Prod.fst ((OracleComp.interpret (ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) (answer fun (q : Query) => Probability.PMF.uniformOfFintype (Response q))) program).run fun (x : Query) => none)

A uniform random function can be implemented by consistent lazy uniform replies even when the client uses private randomness between its adaptive queries.

theorem Cslib.RandomOracle.interpret_prob_eq_memoize {Query α : Type} [Fintype Query] {Value : Type} [Finite Value] [BEq Query] [LawfulBEq Query] (distribution : Query → PMF Value) (program : ProbOracleComp (fun (x : Query) => Value) α) : (do let table ← Probability.PMF.pi distribution OracleComp.interpret (ProbOracleComp.handler ProbComp.unifOracle fun (q : Query) => PMF.pure (table q)) program) = PMF.map Prod.fst ((OracleComp.interpret (ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) (memoize distribution)) program).run [])

A list cache implements eager independent sampling for clients with private randomness.

theorem Cslib.RandomOracle.interpret_prob_eq_memoize_map {Query α : Type} [Fintype Query] {Value Key' Value' : Type} [Finite Value] [BEq Query] [LawfulBEq Query] [BEq Key'] [LawfulBEq Key'] (keyMap : Query ↪ Key') (valueMap : Value → Value') (distribution : Query → PMF Value) (sample' : Key' → PMF Value') (hsample : ∀ (key : Query), sample' (keyMap key) = PMF.map valueMap (distribution key)) (program : ProbOracleComp (fun (x : Query) => Value') α) : (do let table ← Probability.PMF.pi distribution OracleComp.interpret (ProbOracleComp.handler ProbComp.unifOracle fun (key : Query) => PMF.pure (valueMap (table key))) program) = PMF.map Prod.fst ((OracleComp.interpret (ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) fun (key : Query) => memoize sample' (keyMap key)) program).run [])

Injective keys and mapped values implement the same finite random function, including independent private samples and adaptive external queries in the client.

theorem Cslib.RandomOracle.eval_run_interpret_memoize_prob_eq_eager {Key Value Result : Type} [Fintype Key] [Finite Value] [BEq Key] [LawfulBEq Key] (compute : Key → ProbComp Value) (program : ProbOracleComp (fun (x : Key) => Value) Result) : (Prod.fst <$> (OracleComp.interpret (ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (ProbComp.unifFin n)) (memoize compute)) program).run []).eval = do let table ← Probability.PMF.pi fun (q : Key) => (compute q).eval OracleComp.interpret (ProbOracleComp.handler ProbComp.unifOracle fun (q : Key) => PMF.pure (table q)) program

Executable closed samplers with a list cache implement the eager independent-table experiment, including the adversary's private samples and adaptive external calls.