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.
• Cslib.RandomOracle.eval_zoom_memoize_map, Cslib.RandomOracle.eval_zoom_memoize_bind: component-cache zoomStateT/memoize representation bridges to RandomOracle.answer.
• Cslib.RandomOracle.answer_bind_complete, Cslib.RandomOracle.answer_bind_complete₁, Cslib.RandomOracle.answer_bind_complete₂: continuation-form table completion laws past independent samples.

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') ∈ (ProbOracleComp.runWith (memoize distribution) program 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')) (ProbOracleComp.runWith (memoize distribution) program cache) = ProbOracleComp.runWith (answer distribution) program (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 (OracleComp.sumHandler (fun (n : ℕ) => StateT.lift (ProbComp.unifFin n)) (memoize compute)) program).run cache).eval = ProbOracleComp.runWith (answer fun (q : Query) => (compute q).eval) program (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.eval_zoom_memoize_map {Key Value St T β : Type} [DecidableEq Key] (get : St → List (Key × Value)) (set : St → List (Key × Value) → St) (d : ProbComp Value) (q : Key) (s : St) (g : Value → β) (rep : St → T) (F : (Cache fun (x : Key) => Value) → T) (hrep : ∀ (c : List (Key × Value)), rep (set s c) = F (ofList c)) : PMF.map (fun (z : Value × St) => (g z.1, rep z.2)) (zoomStateT get set (memoize (fun (x : Key) => d) q) s).eval = PMF.map (fun (z : Value × Cache fun (x : Key) => Value) => (g z.1, F z.2)) (answer (fun (x : Key) => d.eval) q (ofList (get s)))

One lazy call on a component cache, with its result and represented state, is RandomOracle.answer on the represented component.

theorem Cslib.RandomOracle.eval_zoom_memoize_bind {Key Value St T β : Type} [DecidableEq Key] (get : St → List (Key × Value)) (set : St → List (Key × Value) → St) (d : ProbComp Value) (q : Key) (s : St) (f : Value → St → ProbComp (β × St)) (rep : St → T) (Φ : (Value × Cache fun (x : Key) => Value) → PMF (β × T)) (hf : ∀ (v : Value) (c : List (Key × Value)), PMF.map (fun (z : β × St) => (z.1, rep z.2)) (f v (set s c)).eval = Φ (v, ofList c)) : PMF.map (fun (z : β × St) => (z.1, rep z.2)) (do let vs ← zoomStateT get set (memoize (fun (x : Key) => d) q) s f vs.1 vs.2).eval = (answer (fun (x : Key) => d.eval) q (ofList (get s))).bind Φ

One lazy call on a component cache followed by a continuation, on represented states.

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 ← ProbOracleComp.runWith (answer distribution) program 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 (OracleComp.sumHandler 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 (OracleComp.sumHandler ProbComp.unifOracle fun (q : Query) => PMF.pure (table q)) program) = PMF.map Prod.fst (ProbOracleComp.runWith (answer distribution) program 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 (OracleComp.sumHandler ProbComp.unifOracle fun (q : Query) => PMF.pure (table q)) program) = PMF.map Prod.fst (ProbOracleComp.runWith (answer fun (q : Query) => Probability.PMF.uniformOfFintype (Response q)) program 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 (OracleComp.sumHandler ProbComp.unifOracle fun (q : Query) => PMF.pure (table q)) program) = PMF.map Prod.fst (ProbOracleComp.runWith (memoize distribution) program [])

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 (OracleComp.sumHandler ProbComp.unifOracle fun (key : Query) => PMF.pure (valueMap (table key))) program) = PMF.map Prod.fst ((OracleComp.interpret (OracleComp.sumHandler (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 (OracleComp.sumHandler (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 (OracleComp.sumHandler 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.

theorem Cslib.RandomOracle.answer_bind_complete {Q V β : Type} [Fintype Q] [Finite V] [DecidableEq Q] (d : Q → PMF V) (c : Cache fun (x : Q) => V) (q : Q) (F : (V × Cache fun (x : Q) => V) → (Q → V) → PMF β) (hF : ∀ (v : V) (c₁ c₂ : Cache fun (x : Q) => V), F (v, c₁) = F (v, c₂)) : ((answer d q c).bind fun (x : V × Cache fun (q : Q) => V) => (complete d x.2).bind (F x)) = (complete d c).bind fun (T : Q → V) => F (T q, c) T

Answering one query and completing its table is completing the table and reading it, followed by any continuation F that ignores the intermediate cache.

theorem Cslib.RandomOracle.answer_bind_complete₁ {Q V α β : Type} [Fintype Q] [Finite V] [DecidableEq Q] (d : Q → PMF V) (c : Cache fun (x : Q) => V) (q : Q) (p : PMF α) (F : (V × Cache fun (x : Q) => V) → α → (Q → V) → PMF β) (hF : ∀ (v : V) (c₁ c₂ : Cache fun (x : Q) => V), F (v, c₁) = F (v, c₂)) : ((answer d q c).bind fun (x : V × Cache fun (q : Q) => V) => p.bind fun (a : α) => (complete d x.2).bind (F x a)) = (complete d c).bind fun (T : Q → V) => p.bind fun (a : α) => F (T q, c) a T

answer_bind_complete past one independent sample p.

theorem Cslib.RandomOracle.answer_bind_complete₂ {Q V α α' β : Type} [Fintype Q] [Finite V] [DecidableEq Q] (d : Q → PMF V) (c : Cache fun (x : Q) => V) (q : Q) (p : PMF α) (p' : PMF α') (F : (V × Cache fun (x : Q) => V) → α → α' → (Q → V) → PMF β) (hF : ∀ (v : V) (c₁ c₂ : Cache fun (x : Q) => V), F (v, c₁) = F (v, c₂)) : ((answer d q c).bind fun (x : V × Cache fun (q : Q) => V) => p.bind fun (a : α) => p'.bind fun (b : α') => (complete d x.2).bind (F x a b)) = (complete d c).bind fun (T : Q → V) => p.bind fun (a : α) => p'.bind fun (b : α') => F (T q, c) a b T

answer_bind_complete past two independent samples p and p'.