Lazy sampling of random functions

RandomOracle.answer samples a response on the first occurrence of a query and reuses it on later calls. It supports arbitrary query domains, dependent response types, and a separate distribution for each query. A cache may also contain answers fixed in advance.

On finite domains and finite response types, run_interpret_answer_complete proves the stronger form of eager/lazy equivalence: completing the cache after an adaptive program has the same joint law as completing it before the program. interpret_eq_lazy discards the final table, and uniform_interpret_eq_lazy specializes to a uniformly random function.

memoize supplies an ordinary association-list implementation. run_interpret_memoize relates its complete executions to the mathematical cache, including on infinite query domains. Its closed efficiency certificate is in Computability.Probabilistic.Memoize. memoize_cache_bounds derives cache cardinality and entry provenance from the program's query bounds; a computational certificate must also account for the encoded sizes of keys and replies.

Main definitions

• RandomOracle.Cache, .answer, .complete: partial tables, consistent replies and completion.
• RandomOracle.ofList: represent a list cache by its first occurrence at each key.

Main results

• RandomOracle.run_interpret_answer_complete: eager/lazy equivalence of the result and table.
• RandomOracle.uniform_interpret_eq_lazy: replace a uniformly sampled function by a lazy oracle.
• RandomOracle.run_interpret_memoize: association-list implementation with joint state semantics.
• RandomOracle.memoize_cache_bounds: query bounds control cache growth and entry provenance.

References

• O. Goldreich, S. Goldwasser, S. Micali, How to Construct Random Functions, Section 3.3, uses consistent lazy sampling in the adaptive hybrid argument.

Adapted from Languages/Probabilistic/RandomOracle.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using OracleComp.interpret and generic monad morphisms.

@[reducible, inline]

abbrev Cslib.RandomOracle.Cache {Query : Type u} (Response : Query → Type u) : Type u

Previously assigned responses, indexed by their typed queries.

noncomputable def Cslib.RandomOracle.answer {Query : Type u} {Response : Query → Type u} [DecidableEq Query] (distribution : (q : Query) → PMF (Response q)) (q : Query) : StateT (Cache Response) PMF (Response q)

Return a cached answer, or sample and store one fresh answer.

theorem Cslib.RandomOracle.answer_of_some {Query : Type u} {Response : Query → Type u} [DecidableEq Query] (distribution : (q : Query) → PMF (Response q)) (cache : Cache Response) (q : Query) (value : Response q) (h : cache q = some value) : answer distribution q cache = PMF.pure (value, cache)

A cache hit does not change the cache or draw fresh randomness.

theorem Cslib.RandomOracle.answer_of_none {Query : Type u} {Response : Query → Type u} [DecidableEq Query] (distribution : (q : Query) → PMF (Response q)) (cache : Cache Response) (q : Query) (h : cache q = none) : answer distribution q cache = PMF.map (fun (value : Response q) => (value, Function.update cache q (some value))) (distribution q)

A previously unseen query draws exactly one response from its designated distribution.

theorem Cslib.RandomOracle.mem_support_memoize_iff {Query Value : Type u} [BEq Query] (distribution : Query → PMF Value) (key : Query) (cache : List (Query × Value)) (result : Value × List (Query × Value)) : result ∈ (memoize distribution key cache).support ↔ List.lookup key cache = some result.1 ∧ result.2 = cache ∨ List.lookup key cache = none ∧ result.1 ∈ (distribution key).support ∧ result.2 = (key, result.1) :: cache

A supported memoized call either returns the first cached value unchanged, or samples and prepends exactly one new entry. Initial cached values need not belong to the sampling support.

theorem Cslib.RandomOracle.memoize_invariant {Query Value : Type u} [BEq Query] [LawfulBEq Query] (distribution : Query → PMF Value) (property : Query → Value → Prop) (key : Query) (cache : List (Query × Value)) (hcache : ∀ entry ∈ cache, property entry.1 entry.2) (hsample : ∀ value ∈ (distribution key).support, property key value) (result : Value × List (Query × Value)) (hresult : result ∈ (memoize distribution key cache).support) : property key result.1 ∧ ∀ entry ∈ result.2, property entry.1 entry.2

A memoized sampler preserves any property of its key-value entries and returns a value with that property at the requested key. Cache keys need not be unique.

theorem Cslib.RandomOracle.memoize_cache_bounds {Query α Value : Type u} [BEq Query] (distribution : Query → PMF Value) (program : OracleComp (fun (x : Query) => Value) α) (size : Query → ℕ) (calls maxSize : ℕ) (hcalls : program.IsQueryBounded calls) (hsize : OracleComp.QueriesSatisfy (fun (x : Query) => size x ≤ maxSize) program) (cache cache' : List (Query × Value)) (result : α) (h : (result, cache') ∈ ((OracleComp.interpret (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

Query bounds control the number and provenance of all new cache entries. The sampler's own support bound can then bound stored replies, without assuming that each call grows by a constant.

def Cslib.RandomOracle.ofList {Query Value : Type u} [BEq Query] (cache : List (Query × Value)) : Cache fun (x : Query) => Value

Interpret a finite association list as a partial function. The first occurrence of a key determines its value, so arbitrary initial lists are supported without a uniqueness invariant.

@[simp]

theorem Cslib.RandomOracle.ofList_nil {Query Value : Type u} [BEq Query] : ofList [] = fun (x : Query) => none

The empty list represents the empty cache.

theorem Cslib.RandomOracle.ofList_cons {Query Value : Type u} [BEq Query] [LawfulBEq Query] [DecidableEq Query] (cache : List (Query × Value)) (q : Query) (value : Value) : ofList ((q, value) :: cache) = Function.update (ofList cache) q (some value)

Prepending a cache entry updates exactly its key in the represented partial function.

theorem Cslib.RandomOracle.run_interpret_memoize {Query α Value : Type u} [BEq Query] [LawfulBEq Query] [DecidableEq Query] (distribution : Query → PMF Value) (program : OracleComp (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 (memoize distribution) program).run cache) = (OracleComp.interpret (answer distribution) program).run (ofList cache)

The ordinary list-based memoizer implements the mathematical random oracle, preserving the result and represented final cache for every adaptive program, even on an infinite query domain.

noncomputable def Cslib.RandomOracle.complete {Query : Type u} {Response : Query → Type u} [Fintype Query] [∀ (q : Query), Finite (Response q)] (distribution : (q : Query) → PMF (Response q)) (cache : Cache Response) : PMF ((q : Query) → Response q)

Independently fill all missing entries while retaining the previously assigned answers.

@[simp]

theorem Cslib.RandomOracle.complete_empty {Query : Type u} {Response : Query → Type u} [Fintype Query] [∀ (q : Query), Finite (Response q)] (distribution : (q : Query) → PMF (Response q)) : (complete distribution fun (x : Query) => none) = Probability.PMF.pi distribution

Completing the empty cache samples all coordinates independently.

theorem Cslib.RandomOracle.complete_agrees {Query : Type u} {Response : Query → Type u} [Fintype Query] [∀ (q : Query), Finite (Response q)] (distribution : (q : Query) → PMF (Response q)) (cache : Cache Response) (table : (q : Query) → Response q) (htable : table ∈ (complete distribution cache).support) (q : Query) (value : Response q) (h : cache q = some value) : table q = value

A completion agrees with every answer already in the cache.

theorem Cslib.RandomOracle.complete_update {Query : Type u} {Response : Query → Type u} [Fintype Query] [∀ (q : Query), Finite (Response q)] [DecidableEq Query] (distribution : (q : Query) → PMF (Response q)) (cache : Cache Response) (q : Query) (value : Response q) : complete distribution (Function.update cache q (some value)) = Probability.PMF.pi (Function.update (fun (q : Query) => (cache q).elim (distribution q) PMF.pure) q (PMF.pure value))

Fixing one cache entry fixes the corresponding coordinate of its completion.

theorem Cslib.RandomOracle.answer_complete {Query : Type u} {Response : Query → Type u} [Fintype Query] [∀ (q : Query), Finite (Response q)] [DecidableEq Query] (distribution : (q : Query) → PMF (Response q)) (cache : Cache Response) (q : Query) : (do let __x ← answer distribution q cache match __x with | (value, cache') => PMF.map (fun (x : (q : Query) → Response q) => (value, x)) (complete distribution cache')) = PMF.map (fun (table : (q : Query) → Response q) => (table q, table)) (complete distribution cache)

Answering one query and completing the cache gives the same joint answer and table as completing first and reading the table.

theorem Cslib.RandomOracle.run_interpret_answer_complete {Query : Type u} {Response : Query → Type u} {α : Type u} [Fintype Query] [∀ (q : Query), Finite (Response q)] [DecidableEq Query] (distribution : (q : Query) → PMF (Response q)) (program : OracleComp Response α) (cache : Cache Response) : (do let __x ← (OracleComp.interpret (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 (fun (q : Query) => PMF.pure (table q)) program)

Eager/lazy equivalence including the final complete table, for every adaptive program and every initial cache. Later continuations can inspect both the result and that table.

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

Lazy evaluation from an empty cache agrees with sampling the entire independent function in advance, even for adaptive programs with repeated queries.

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

A uniformly sampled function can be replaced by a consistent lazy uniform oracle.

theorem Cslib.RandomOracle.interpret_eq_memoize {Query α Value : Type u} [Fintype Query] [Finite Value] [BEq Query] [LawfulBEq Query] (distribution : Query → PMF Value) (program : OracleComp (fun (x : Query) => Value) α) : (do let table ← Probability.PMF.pi distribution OracleComp.interpret (fun (q : Query) => PMF.pure (table q)) program) = PMF.map Prod.fst ((OracleComp.interpret (memoize distribution) program).run [])

An ordinary list-based cache implements eager independent function sampling.

theorem Cslib.RandomOracle.interpret_eq_memoize_map {Query α Value : Type u} [Fintype Query] [Finite Value] [BEq Query] [LawfulBEq Query] {Key' Value' : Type u} [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 : OracleComp (fun (x : Query) => Value') α) : (do let table ← Probability.PMF.pi distribution OracleComp.interpret (fun (key : Query) => PMF.pure (valueMap (table key))) program) = PMF.map Prod.fst ((OracleComp.interpret (fun (key : Query) => memoize sample' (keyMap key)) program).run [])

Implement a finite random function using arbitrary injective key representations and mapped values. The client sees the represented values; it need not know the finite sampling type.

theorem Cslib.RandomOracle.eval_run_interpret_memoize {Key Value Result : Type} [BEq Key] [LawfulBEq Key] [DecidableEq Key] (sample : Key → ProbComp Value) (program : OracleComp (fun (x : Key) => Value) Result) (cache : List (Key × Value)) : PMF.map (fun (x : Result × List (Key × Value)) => match x with | (result, cache') => (result, ofList cache')) ((OracleComp.interpret (memoize sample) program).run cache).eval = (OracleComp.interpret (answer fun (q : Key) => (sample q).eval) program).run (ofList cache)

Evaluate memoized closed samplers while retaining the represented final cache.

theorem Cslib.RandomOracle.eval_run_interpret_memoize_eq_eager {Key Value Result : Type} [BEq Key] [LawfulBEq Key] [Fintype Key] [Finite Value] (sample : Key → ProbComp Value) (program : OracleComp (fun (x : Key) => Value) Result) : (Prod.fst <$> (OracleComp.interpret (memoize sample) program).run []).eval = do let table ← Probability.PMF.pi fun (q : Key) => (sample q).eval OracleComp.interpret (fun (q : Key) => PMF.pure (table q)) program

Memoized closed samplers implement the eager independent random-function experiment.