diff --git a/CslibFrontier.lean b/CslibFrontier.lean index fa53ceba7d..f684e99fac 100644 --- a/CslibFrontier.lean +++ b/CslibFrontier.lean @@ -6082,6 +6082,8 @@ public import CslibFrontier.Languages.Probabilistic.QueryCount.Support public import CslibFrontier.Languages.Probabilistic.RandomOracle public import CslibFrontier.Languages.Probabilistic.RandomOracle.Probabilistic public import CslibFrontier.Languages.Probabilistic.RandomOracle.Programming +public import CslibFrontier.Languages.Probabilistic.RandomOracle.Represented +public import CslibFrontier.Languages.Probabilistic.RandomOracle.Sum public import CslibFrontier.Languages.Probabilistic.RandomPermutation public import CslibFrontier.Languages.Probabilistic.RandomPermutation.ExtPermsCard public import CslibFrontier.Languages.Probabilistic.Rational diff --git a/CslibFrontier/Crypto/Computational/Encryption/KEM.lean b/CslibFrontier/Crypto/Computational/Encryption/KEM.lean index 7698528052..a4c927c524 100644 --- a/CslibFrontier/Crypto/Computational/Encryption/KEM.lean +++ b/CslibFrontier/Crypto/Computational/Encryption/KEM.lean @@ -7,7 +7,7 @@ Authors: Samuel Schlesinger module -- upstream: candidate -public import Cslib.Init +public import CslibFrontier.Init /-! # Key encapsulation challenges diff --git a/CslibFrontier/Crypto/Protocols/KEM/FujisakiOkamoto/Bot.lean b/CslibFrontier/Crypto/Protocols/KEM/FujisakiOkamoto/Bot.lean index 69e8775bee..dba14d0cf1 100644 --- a/CslibFrontier/Crypto/Protocols/KEM/FujisakiOkamoto/Bot.lean +++ b/CslibFrontier/Crypto/Protocols/KEM/FujisakiOkamoto/Bot.lean @@ -13,7 +13,6 @@ import CslibFrontier.Crypto.Game.CloseTo.UntilBad import CslibFrontier.Crypto.Game.Hybrid import CslibFrontier.Crypto.Protocols.KEM.FujisakiOkamoto.NotBot.Challenge import CslibFrontier.Crypto.Protocols.KEM.FujisakiOkamoto.NotBot.Correctness -import CslibFrontier.Crypto.Protocols.KEM.FujisakiOkamoto.NotBot.Lazy import CslibFrontier.Crypto.Protocols.KEM.FujisakiOkamoto.NotBot.Pushforward import CslibFrontier.Languages.Probabilistic.Norm import CslibFrontier.Languages.Probabilistic.RandomOracle.Probabilistic @@ -548,6 +547,59 @@ def cachedCoupledBotGame (S : Scheme PK SK M R CT K) (A : ROAdversary PK M R CT (b : Bool) : ProbComp Bool := S.coupledFilterGame (cachedCoupledBotCheck S.pke) A b +/-- The three partial tables `(G, Hraw, Hq)` of the coupled game. -/ +private abbrev Tables (M R CT K : Type) : Type := + RandomOracle.Cache (fun _ : M => R) × RandomOracle.Cache (fun _ : Bool × M × CT => K) × + RandomOracle.Cache (fun _ : CT => K) + +/-- The represented tables of a `SimState`. -/ +private def tablesOf (st : SimState M R CT K) : Tables M R CT K := + (RandomOracle.ofList st.gCache, RandomOracle.ofList st.hCache, RandomOracle.ofList st.hqCache) + +/-- `coupledHashH` on represented tables, answered with `RandomOracle.answer`. -/ +private noncomputable def answerHashH (S : Scheme PK SK M R CT K) (pk : PK) (sk : SK) + (x : Bool × M × CT) : StateT (Tables M R CT K) PMF K := fun (tG, tH, tQ) => + match x with + | (false, m, c) => + (RandomOracle.answer (fun _ => ProbComp.eval S.pke.sampleCoins) m tG).bind fun y => + if S.pke.encDet pk m y.1 = c ∧ S.pke.dec sk c = some m then + (RandomOracle.answer (fun _ => ProbComp.eval S.sampleKey) c tQ).map + fun z => (z.1, (y.2, tH, z.2)) + else + (RandomOracle.answer (fun _ => ProbComp.eval S.sampleKey) (false, m, c) tH).map + fun z => (z.1, (y.2, z.2, tQ)) + | (true, m, c) => + (RandomOracle.answer (fun _ => ProbComp.eval S.sampleKey) (true, m, c) tH).map + fun z => (z.1, (tG, z.2, tQ)) + +/-- Mapping `SimState` to its represented tables turns `coupledHashH` into `answerHashH`. -/ +private theorem coupledHashH_map_tablesOf (S : Scheme PK SK M R CT K) (pk : PK) (sk : SK) + (x : Bool × M × CT) (st : SimState M R CT K) : + (ProbComp.eval (S.coupledHashH pk sk x st)).map (fun z => (z.1, tablesOf z.2)) = + S.answerHashH pk sk x (tablesOf st) := by + rcases x with ⟨_ | _, m, c⟩ + · change (ProbComp.eval (simHashG S.pke.sampleCoins m st >>= fun vs => + (if S.pke.encDet pk m vs.1 = c ∧ S.pke.dec sk c = some m then + simHashHq S.sampleKey c else simHashHRaw S.sampleKey (false, m, c)) vs.2)).map _ = _ + dsimp only [answerHashH, simHashG] + refine eval_zoom_memoize_bind (fun st : SimState M R CT K => st.gCache) + (fun st g => { st with gCache := g }) S.pke.sampleCoins m st + (fun r st' => (if S.pke.encDet pk m r = c ∧ S.pke.dec sk c = some m then + simHashHq S.sampleKey c else simHashHRaw S.sampleKey (false, m, c)) st') + tablesOf _ (fun r gC => ?_) + by_cases h : S.pke.encDet pk m r = c ∧ S.pke.dec sk c = some m + · simp only [h, and_self, ↓reduceIte] + exact eval_zoom_memoize_map SimState.hqCache (fun st q => { st with hqCache := q }) + S.sampleKey c _ (fun k => k) tablesOf + (fun q => (RandomOracle.ofList gC, RandomOracle.ofList st.hCache, q)) (fun _ => rfl) + · simp only [h, ↓reduceIte] + exact eval_zoom_memoize_map (fun st : SimState M R CT K => st.hCache) + (fun st h => { st with hCache := h }) S.sampleKey (false, m, c) _ (fun k => k) tablesOf + (fun h => (RandomOracle.ofList gC, h, RandomOracle.ofList st.hqCache)) (fun _ => rfl) + · exact eval_zoom_memoize_map (fun st : SimState M R CT K => st.hCache) + (fun st h => { st with hCache := h }) S.sampleKey (true, m, c) st (fun k => k) tablesOf + (fun h => (RandomOracle.ofList st.gCache, h, RandomOracle.ofList st.hqCache)) (fun _ => rfl) + /-- `coupledFilterHandler (cachedCoupledBotCheck S.pke pk sk)` on represented tables `(tG, tH, tQ)`. -/ private noncomputable def answerCachedBotHandler (S : Scheme PK SK M R CT K) (pk : PK) (sk : SK) @@ -616,6 +668,18 @@ section CompleteBot variable [Fintype M] [Finite R] [Fintype CT] [Finite K] +/-- Full tables `(G, Hraw, Hq)` of the eager coupled game. -/ +private abbrev FullTables (M R CT K : Type) : Type := + (M → R) × (Bool × M × CT → K) × (CT → K) + +/-- Complete the three represented tables independently. -/ +private noncomputable def completeTables (S : Scheme PK SK M R CT K) : + Tables M R CT K → PMF (FullTables M R CT K) + | (tG, tH, tQ) => + (RandomOracle.complete (fun _ => ProbComp.eval S.pke.sampleCoins) tG).bind fun G => + (RandomOracle.complete (fun _ => ProbComp.eval S.sampleKey) tH).bind fun H => + (RandomOracle.complete (fun _ => ProbComp.eval S.sampleKey) tQ).map fun Q => (G, H, Q) + private noncomputable def eagerCoupledBotStateHandler (S : Scheme PK SK M R CT K) (pk : PK) (sk : SK) (cStar : CT) (q : ROQuery M CT) : StateT (FullTables M R CT K) PMF (ROResp R K q) := diff --git a/CslibFrontier/Crypto/Protocols/KEM/FujisakiOkamoto/NotBot/Correctness.lean b/CslibFrontier/Crypto/Protocols/KEM/FujisakiOkamoto/NotBot/Correctness.lean index 9dac2f2d4e..f13a934800 100644 --- a/CslibFrontier/Crypto/Protocols/KEM/FujisakiOkamoto/NotBot/Correctness.lean +++ b/CslibFrontier/Crypto/Protocols/KEM/FujisakiOkamoto/NotBot/Correctness.lean @@ -398,11 +398,6 @@ theorem advantage_coupledFilterGame_simFilterGame_le [Fintype M] [Nonempty M] (Game.advantage (ProbComp.eval (S.coupledFilterGame d₁ A b)) (ProbComp.eval (S.simFilterGame d₂ A b)) : ℝ) ≤ ((qG + qH + 1 : ℕ) : ℝ) * δ := by - have hcost (ch : KEM.Challenge PK CT K) : - OracleComp.IsCostBounded ROQuery.ghCost (A ch) (qG + qH) := by - have ⟨hG, hH⟩ := hq ch - convert OracleComp.IsCostBounded.add hG hH using 1 - funext q; cases q <;> rfl set E : ℝ≥0∞ := S.pke.keyGen.expect fun x => ENNReal.ofReal (S.pke.keyPairMaxFailProb x.1 x.2) with hE have hclose : CloseTo (ProbComp.eval (S.coupledFilterGame d₁ A b)) @@ -456,7 +451,7 @@ theorem advantage_coupledFilterGame_simFilterGame_le [Fintype M] [Nonempty M] exact hr refine (CloseTo.bind_right_tsum _ (err := fun _ => ((qG + qH : ℕ) : ℝ≥0∞) * p) fun kRand _ => ?_).mono (le_of_eq (hconst _ _)) - exact closeTo_run_coupled_sim S pk sk _ (d₁ pk sk) (d₂ pk) (hd pk sk) _ (hcost _) hgood _ + exact closeTo_run_coupled_sim S pk sk _ (d₁ pk sk) (d₂ pk) (hd pk sk) _ (hq.ghCost _) hgood _ · rw [ite_eq_right_of_eq_false _ _ (eq_false hr)] exact fun e => (Probability.PMF.toOuterMeasure_le_one _ e).trans (le_self_add.trans le_add_self) diff --git a/CslibFrontier/Crypto/Protocols/KEM/FujisakiOkamoto/NotBot/Lazy.lean b/CslibFrontier/Crypto/Protocols/KEM/FujisakiOkamoto/NotBot/Lazy.lean index 44c44d3166..3cae809be7 100644 --- a/CslibFrontier/Crypto/Protocols/KEM/FujisakiOkamoto/NotBot/Lazy.lean +++ b/CslibFrontier/Crypto/Protocols/KEM/FujisakiOkamoto/NotBot/Lazy.lean @@ -10,7 +10,7 @@ module public import CslibFrontier.Crypto.Protocols.KEM.FujisakiOkamoto.NotBot.Hybrids import CslibFrontier.Languages.Probabilistic.Norm import CslibFrontier.Languages.Probabilistic.RandomOracle.Probabilistic -import CslibFrontier.Languages.Probabilistic.Simulation +import CslibFrontier.Languages.Probabilistic.RandomOracle.Represented import CslibFrontier.Tactic.PMFSwap /-! @@ -23,11 +23,11 @@ that it has the same output distribution as the eager coupled game `Scheme.eager step in the IND-CCA proof for `FO-notbot` of [HofheinzHoevelmannsKiltz2017] (IACR ePrint 2017/604, full version dated 2 November 2021, §3.1 and §3.2.2). -The proof follows the eager/lazy argument of -`CslibFrontier.Crypto.Protocols.KEM.FujisakiOkamoto.Security`: the list caches are mapped to -`RandomOracle.Cache` tables with `RandomOracle.ofList`, and the three tables are then completed -at once with `RandomOracle.complete`; each oracle call commutes with completion by -`RandomOracle.answer_complete`. +The three lazy tables are one lazy random oracle on the joined interface `CoupledSpec`, and every +query of the coupled game is the oracle program `coupledProgram` over it. So +`RandomOracle.eval_run_interpret_eq_complete_bind` replaces the three caches by complete tables in +one step, and `RandomOracle.bind_complete_sum` splits the completed table into `G`, `Hraw` and +`Hq`. ## Main results @@ -47,8 +47,7 @@ namespace Cslib.Crypto.Protocols.FujisakiOkamoto open Probability open Probability.PMF -open RandomOracle (eval_zoom_memoize_map eval_zoom_memoize_bind - answer_bind_complete answer_bind_complete₁ answer_bind_complete₂) +open scoped Cslib variable {PK SK M R CT K : Type} @@ -56,197 +55,156 @@ namespace Scheme variable [DecidableEq M] [DecidableEq CT] -/-- The three partial tables `(G, Hraw, Hq)` of the coupled game. -/ -abbrev Tables (M R CT K : Type) : Type := - RandomOracle.Cache (fun _ : M => R) × RandomOracle.Cache (fun _ : Bool × M × CT => K) × - RandomOracle.Cache (fun _ : CT => K) - -/-- The represented tables of a `SimState`. -/ -@[expose] def tablesOf (st : SimState M R CT K) : Tables M R CT K := - (RandomOracle.ofList st.gCache, RandomOracle.ofList st.hCache, RandomOracle.ofList st.hqCache) - -/-- `coupledHashH` on represented tables, answered with `RandomOracle.answer`. -/ -@[expose] noncomputable def answerHashH (S : Scheme PK SK M R CT K) (pk : PK) (sk : SK) - (x : Bool × M × CT) : StateT (Tables M R CT K) PMF K := fun (tG, tH, tQ) => - match x with - | (false, m, c) => - (RandomOracle.answer (fun _ => ProbComp.eval S.pke.sampleCoins) m tG).bind fun y => - if S.pke.encDet pk m y.1 = c ∧ S.pke.dec sk c = some m then - (RandomOracle.answer (fun _ => ProbComp.eval S.sampleKey) c tQ).map - fun z => (z.1, (y.2, tH, z.2)) - else - (RandomOracle.answer (fun _ => ProbComp.eval S.sampleKey) (false, m, c) tH).map - fun z => (z.1, (y.2, z.2, tQ)) - | (true, m, c) => - (RandomOracle.answer (fun _ => ProbComp.eval S.sampleKey) (true, m, c) tH).map - fun z => (z.1, (tG, z.2, tQ)) - -/-- `coupledHandler` on represented tables, answered with `RandomOracle.answer`. -/ -private noncomputable def answerHandler (S : Scheme PK SK M R CT K) (pk : PK) (sk : SK) - (cStar : CT) (q : ROQuery M CT) : StateT (Tables M R CT K) PMF (ROResp R K q) := - ROQuery.dispatch - (fun m t => (RandomOracle.answer (fun _ => ProbComp.eval S.pke.sampleCoins) m t.1).map - fun z => (z.1, (z.2, t.2.1, t.2.2))) - (S.answerHashH pk sk) - (fun c t => (RandomOracle.answer (fun _ => ProbComp.eval S.sampleKey) c t.2.2).map - fun z => (some z.1, (t.1, t.2.1, z.2))) - cStar q - -/-- Mapping `SimState` to its represented tables turns `coupledHashH` into `answerHashH`. -/ -theorem coupledHashH_map_tablesOf (S : Scheme PK SK M R CT K) (pk : PK) (sk : SK) - (x : Bool × M × CT) (st : SimState M R CT K) : - (ProbComp.eval (S.coupledHashH pk sk x st)).map (fun z => (z.1, tablesOf z.2)) = - S.answerHashH pk sk x (tablesOf st) := by - rcases x with ⟨_ | _, m, c⟩ - · change (ProbComp.eval (simHashG S.pke.sampleCoins m st >>= fun vs => - (if S.pke.encDet pk m vs.1 = c ∧ S.pke.dec sk c = some m then - simHashHq S.sampleKey c else simHashHRaw S.sampleKey (false, m, c)) vs.2)).map _ = _ - dsimp only [answerHashH, simHashG] - refine eval_zoom_memoize_bind (fun st : SimState M R CT K => st.gCache) - (fun st g => { st with gCache := g }) S.pke.sampleCoins m st - (fun r st' => (if S.pke.encDet pk m r = c ∧ S.pke.dec sk c = some m then - simHashHq S.sampleKey c else simHashHRaw S.sampleKey (false, m, c)) st') - tablesOf _ (fun r gC => ?_) - by_cases h : S.pke.encDet pk m r = c ∧ S.pke.dec sk c = some m - · simp only [h, and_self, ↓reduceIte] - exact eval_zoom_memoize_map SimState.hqCache (fun st q => { st with hqCache := q }) - S.sampleKey c _ (fun k => k) tablesOf - (fun q => (RandomOracle.ofList gC, RandomOracle.ofList st.hCache, q)) (fun _ => rfl) - · simp only [h, ↓reduceIte] - exact eval_zoom_memoize_map (fun st : SimState M R CT K => st.hCache) - (fun st h => { st with hCache := h }) S.sampleKey (false, m, c) _ (fun k => k) tablesOf - (fun h => (RandomOracle.ofList gC, h, RandomOracle.ofList st.hqCache)) (fun _ => rfl) - · exact eval_zoom_memoize_map (fun st : SimState M R CT K => st.hCache) - (fun st h => { st with hCache := h }) S.sampleKey (true, m, c) st (fun k => k) tablesOf - (fun h => (RandomOracle.ofList st.gCache, h, RandomOracle.ofList st.hqCache)) (fun _ => rfl) - -/-- Mapping `SimState` to its represented tables turns `coupledHandler` into `answerHandler`. -/ -private theorem coupledHandler_map_tablesOf (S : Scheme PK SK M R CT K) (pk : PK) (sk : SK) - (cStar : CT) (q : ROQuery M CT) (st : SimState M R CT K) : - (ProbComp.eval (S.coupledHandler pk sk cStar q st)).map (fun z => (z.1, tablesOf z.2)) = - S.answerHandler pk sk cStar q (tablesOf st) := by +/-- The random oracles `G : M → R`, `Hraw : Bool × M × CT → K` and `Hq : CT → K` of the coupled +game as one interface. -/ +private abbrev CoupledSpec (M R CT K : Type) := + ((fun _ : M => R) ⊕ₒ (fun _ : Bool × M × CT => K)) ⊕ₒ (fun _ : CT => K) + +/-- Each query of the coupled game as a program over its random oracles: `G` is forwarded, `H` +runs the coupled key derivation `coupledH`, and decapsulation reads `Hq`. -/ +private def coupledProgram (S : Scheme PK SK M R CT K) (pk : PK) (sk : SK) (cStar : CT) : + (q : ROQuery M CT) → OracleComp (CoupledSpec M R CT K) (ROResp R K q) := + ROQuery.dispatch (fun m => OracleComp.query (spec := CoupledSpec M R CT K) (.inl (.inl m))) + (fun + | (false, m, c) => do + let r : R ← OracleComp.query (spec := CoupledSpec M R CT K) (.inl (.inl m)) + if S.pke.encDet pk m r = c ∧ S.pke.dec sk c = some m then + OracleComp.query (spec := CoupledSpec M R CT K) (.inr c) + else + OracleComp.query (spec := CoupledSpec M R CT K) (.inl (.inr (false, m, c))) + | (true, m, c) => OracleComp.query (spec := CoupledSpec M R CT K) (.inl (.inr (true, m, c)))) + (fun c => do + let k ← OracleComp.query (spec := CoupledSpec M R CT K) (.inr c) + return some k) + cStar + +/-- The lazy oracles of the coupled game on the caches of `SimState`. -/ +private abbrev lazyOracle (S : Scheme PK SK M R CT K) : + (q : (M ⊕ (Bool × M × CT)) ⊕ CT) → + StateT (SimState M R CT K) ProbComp (CoupledSpec M R CT K q) := + OracleComp.sumHandler + (OracleComp.sumHandler (simHashG S.pke.sampleCoins) (simHashHRaw S.sampleKey)) + (simHashHq S.sampleKey) + +/-- The sampling distributions of the coupled game's random oracles. -/ +private noncomputable abbrev coupledDistribution (S : Scheme PK SK M R CT K) : + (q : (M ⊕ (Bool × M × CT)) ⊕ CT) → PMF (CoupledSpec M R CT K q) := + OracleComp.sumHandler + (OracleComp.sumHandler (fun _ => ProbComp.eval S.pke.sampleCoins) + (fun _ => ProbComp.eval S.sampleKey)) + (fun _ => ProbComp.eval S.sampleKey) + +/-- The coupled game's oracles answered from complete tables `G`, `Hraw` and `Hq`. -/ +private noncomputable abbrev tableOracle (G : M → R) (Hraw : Bool × M × CT → K) (Hq : CT → K) : + (q : (M ⊕ (Bool × M × CT)) ⊕ CT) → PMF (CoupledSpec M R CT K q) := + OracleComp.sumHandler + (OracleComp.sumHandler (fun m => PMF.pure (G m)) (fun x => PMF.pure (Hraw x))) + (fun c => PMF.pure (Hq c)) + +/-- The joined cache represented by the three list caches of a `SimState`. -/ +private abbrev coupledCache (st : SimState M R CT K) : RandomOracle.Cache (CoupledSpec M R CT K) := + RandomOracle.Cache.sum + (RandomOracle.Cache.sum (RandomOracle.ofList st.gCache) (RandomOracle.ofList st.hCache)) + (RandomOracle.ofList st.hqCache) + +/-- Each lazy oracle call, read on the joined cache, is a lazy call of the joined oracle. -/ +private theorem eval_lazyOracle_map_coupledCache (S : Scheme PK SK M R CT K) + (q : (M ⊕ (Bool × M × CT)) ⊕ CT) (st : SimState M R CT K) : + (ProbComp.eval (S.lazyOracle q st)).map (fun z => (z.1, coupledCache z.2)) = + RandomOracle.answer S.coupledDistribution q (coupledCache st) := by + rcases q with (m | x) | c + · rw [coupledCache, RandomOracle.answer_sum_inl, RandomOracle.answer_sum_inl, PMF.map_comp] + exact RandomOracle.eval_zoom_memoize_map (fun st : SimState M R CT K => st.gCache) + (fun st g => { st with gCache := g }) S.pke.sampleCoins m st (fun r => r) coupledCache + (fun g => RandomOracle.Cache.sum + (RandomOracle.Cache.sum g (RandomOracle.ofList st.hCache)) + (RandomOracle.ofList st.hqCache)) (fun _ => rfl) + · rw [coupledCache, RandomOracle.answer_sum_inl, RandomOracle.answer_sum_inr, PMF.map_comp] + exact RandomOracle.eval_zoom_memoize_map (fun st : SimState M R CT K => st.hCache) + (fun st h => { st with hCache := h }) S.sampleKey x st (fun k => k) coupledCache + (fun h => RandomOracle.Cache.sum + (RandomOracle.Cache.sum (RandomOracle.ofList st.gCache) h) + (RandomOracle.ofList st.hqCache)) (fun _ => rfl) + · rw [coupledCache, RandomOracle.answer_sum_inr] + exact RandomOracle.eval_zoom_memoize_map SimState.hqCache + (fun st q => { st with hqCache := q }) S.sampleKey c st (fun k => k) coupledCache + (fun q => RandomOracle.Cache.sum + (RandomOracle.Cache.sum (RandomOracle.ofList st.gCache) (RandomOracle.ofList st.hCache)) + q) (fun _ => rfl) + +/-- `coupledHandler` interprets `coupledProgram` with the lazy oracles on `SimState`. -/ +private theorem coupledHandler_eq_interpret (S : Scheme PK SK M R CT K) (pk : PK) (sk : SK) + (cStar : CT) (q : ROQuery M CT) : + S.coupledHandler pk sk cStar q = + OracleComp.interpret S.lazyOracle (S.coupledProgram pk sk cStar q) := by cases q with - | G m => - exact eval_zoom_memoize_map (fun st : SimState M R CT K => st.gCache) - (fun st g => { st with gCache := g }) S.pke.sampleCoins m st (fun r => r) tablesOf - (fun g => (g, RandomOracle.ofList st.hCache, RandomOracle.ofList st.hqCache)) - (fun _ => rfl) - | H x => exact S.coupledHashH_map_tablesOf pk sk x st + | G m => exact (OracleComp.interpret_query S.lazyOracle (.inl (.inl m))).symm + | H x => + rcases x with ⟨_ | _, m, c⟩ + · simp only [coupledHandler, coupledFilterHandler, simFilterDispatch, coupledHashH, + coupledProgram, ROQuery.dispatch, OracleComp.interpret_bind, OracleComp.interpret_query] + refine congrArg (simHashG S.pke.sampleCoins m >>= ·) (funext fun r => ?_) + split_ifs <;> exact (OracleComp.interpret_query _ _).symm + · exact (OracleComp.interpret_query S.lazyOracle (.inl (.inr (true, m, c)))).symm | decaps c => by_cases hc : c = cStar - · simp only [coupledHandler, coupledFilterHandler, simFilterDispatch, answerHandler, hc, - ↓reduceIte, ROQuery.dispatch] - exact PMF.pure_map _ _ - · simp only [coupledHandler, coupledFilterHandler, simFilterDispatch, answerHandler, hc, - ↓reduceIte, Bool.cond_true, ROQuery.dispatch, filterDecaps] - change (ProbComp.eval (simHashHq S.sampleKey c st >>= fun vs => - pure (some vs.1, vs.2))).map _ = _ - refine Eq.trans ?_ (eval_zoom_memoize_map SimState.hqCache - (fun st q => { st with hqCache := q }) S.sampleKey c st some tablesOf - (fun q => (RandomOracle.ofList st.gCache, RandomOracle.ofList st.hCache, q)) - (fun _ => rfl)) - rw [ProbComp.eval_bind, PMF.map_bind] - simp only [ProbComp.eval_pure, PMF.pure_map] + · simp [coupledHandler, coupledFilterHandler, simFilterDispatch, coupledProgram, hc] + · simp only [coupledHandler, coupledFilterHandler, simFilterDispatch, coupledProgram, + ROQuery.dispatch, hc, ↓reduceIte, OracleComp.interpret_bind, OracleComp.interpret_query, + OracleComp.interpret_pure] rfl -section Complete - -variable [Fintype M] [Finite R] [Fintype CT] [Finite K] - -/-- Full tables `(G, Hraw, Hq)` of the eager coupled game. -/ -abbrev FullTables (M R CT K : Type) : Type := - (M → R) × (Bool × M × CT → K) × (CT → K) - -/-- Complete the three represented tables independently. -/ -@[expose] noncomputable def completeTables (S : Scheme PK SK M R CT K) : - Tables M R CT K → PMF (FullTables M R CT K) - | (tG, tH, tQ) => - (RandomOracle.complete (fun _ => ProbComp.eval S.pke.sampleCoins) tG).bind fun G => - (RandomOracle.complete (fun _ => ProbComp.eval S.sampleKey) tH).bind fun H => - (RandomOracle.complete (fun _ => ProbComp.eval S.sampleKey) tQ).map fun Q => (G, H, Q) - -/-- `eagerCoupledHandler` reading its tables from the state. -/ -private noncomputable def eagerStateHandler (S : Scheme PK SK M R CT K) (pk : PK) (sk : SK) - (cStar : CT) (q : ROQuery M CT) : StateT (FullTables M R CT K) PMF (ROResp R K q) := - fun T => (S.eagerCoupledHandler T.1 T.2.2 T.2.1 pk sk cStar q).map (·, T) - -/-- Single-step simulation from `answerHandler` to `eagerStateHandler` via -`RandomOracle.answer_complete`. -/ -private theorem answerHandler_sim (S : Scheme PK SK M R CT K) (pk : PK) (sk : SK) (cStar : CT) - (q : ROQuery M CT) (t : Tables M R CT K) : - (S.answerHandler pk sk cStar q t).bind (fun x => (S.completeTables x.2).map (x.1, ·)) = - (S.completeTables t).bind (S.eagerStateHandler pk sk cStar q) := by - rcases t with ⟨tG, tH, tQ⟩ +/-- `eagerCoupledHandler` interprets `coupledProgram` with the complete tables. -/ +private theorem eagerCoupledHandler_eq_interpret (S : Scheme PK SK M R CT K) (G : M → R) + (Hq : CT → K) (Hraw : Bool × M × CT → K) (pk : PK) (sk : SK) (cStar : CT) + (q : ROQuery M CT) : + S.eagerCoupledHandler G Hq Hraw pk sk cStar q = + OracleComp.interpret (tableOracle G Hraw Hq) (S.coupledProgram pk sk cStar q) := by cases q with - | G m => - simp only [answerHandler, completeTables, eagerStateHandler, eagerCoupledHandler, pmf_norm, - ROQuery.dispatch] - rw [answer_bind_complete] - · rfl - · intros; rfl + | G m => exact (OracleComp.interpret_query (tableOracle G Hraw Hq) (.inl (.inl m))).symm | H x => rcases x with ⟨_ | _, m, c⟩ - · simp only [answerHandler, answerHashH, completeTables, eagerStateHandler, - eagerCoupledHandler, coupledH, pmf_norm, ROQuery.dispatch] - refine Eq.trans ?_ (answer_bind_complete _ tG m - (fun x G => (RandomOracle.complete (fun _ => ProbComp.eval S.sampleKey) tH).bind fun H => - (RandomOracle.complete (fun _ => ProbComp.eval S.sampleKey) tQ).bind fun Q => - PMF.pure (if S.pke.encDet pk m x.1 = c ∧ S.pke.dec sk c = some m then Q c - else H (false, m, c), G, H, Q)) (fun _ _ _ => rfl)) - congr 1 with y : 1 - by_cases h : S.pke.encDet pk m y.1 = c ∧ S.pke.dec sk c = some m - · simp only [h, and_self, ↓reduceIte, pmf_norm, PMF.map] - rw [answer_bind_complete₂] - · pmf_swap - · intros; rfl - · simp only [h, ↓reduceIte, pmf_norm, PMF.map] - rw [answer_bind_complete₁] - · pmf_swap - · intros; rfl - · simp only [answerHandler, answerHashH, completeTables, eagerStateHandler, - eagerCoupledHandler, coupledH, pmf_norm, PMF.map, ROQuery.dispatch] - rw [answer_bind_complete₁] - · pmf_swap - · intros; rfl + · simp only [eagerCoupledHandler, coupledH, coupledProgram, ROQuery.dispatch, + OracleComp.interpret_bind, OracleComp.interpret_query, Function.comp_apply, + PMF.monad_bind_eq_bind, PMF.pure_bind] + split_ifs <;> exact (OracleComp.interpret_query _ _).symm + · exact (OracleComp.interpret_query (tableOracle G Hraw Hq) (.inl (.inr (true, m, c)))).symm | decaps c => by_cases hc : c = cStar - · simp only [answerHandler, completeTables, eagerStateHandler, eagerCoupledHandler, hc, - ↓reduceIte, pure, StateT.pure, pmf_norm, PMF.map, ROQuery.dispatch] - · simp only [answerHandler, completeTables, eagerStateHandler, eagerCoupledHandler, hc, - ↓reduceIte, pmf_norm, PMF.map, ROQuery.dispatch] - rw [answer_bind_complete₂] - · pmf_swap - · intros; rfl + · simp [eagerCoupledHandler, coupledProgram, hc] + · simp only [eagerCoupledHandler, coupledProgram, ROQuery.dispatch, hc, ↓reduceIte, + OracleComp.interpret_bind, OracleComp.interpret_query, OracleComp.interpret_pure, + PMF.monad_bind_eq_bind, PMF.pure_bind] + rfl -/-- Running `prog` under `coupledHandler` from `st` has the output distribution of completing the -represented tables of `st` and interpreting `prog` under `eagerCoupledHandler`. -/ -private theorem eval_run_coupledHandler_eq_eager (S : Scheme PK SK M R CT K) (pk : PK) (sk : SK) - (cStar : CT) {α : Type} (prog : OracleComp (ROResp (M := M) (CT := CT) R K) α) - (st : SimState M R CT K) : +/-- Running a program under `coupledHandler` has the law of completing the three caches into +tables `G`, `Hraw` and `Hq` and running it under `eagerCoupledHandler`. -/ +private theorem eval_run_coupledHandler_eq_eager [Fintype M] [Finite R] [Fintype CT] [Finite K] + (S : Scheme PK SK M R CT K) (pk : PK) (sk : SK) (cStar : CT) {α : Type} + (prog : OracleComp (ROResp (M := M) (CT := CT) R K) α) (st : SimState M R CT K) : (ProbComp.eval ((OracleComp.interpret (S.coupledHandler pk sk cStar) prog).run st)).map Prod.fst = - (S.completeTables (tablesOf st)).bind fun T => - OracleComp.interpret (S.eagerCoupledHandler T.1 T.2.2 T.2.1 pk sk cStar) prog := by - rw [OracleComp.map_run_interpret ProbComp.isMonadHom_eval] - have hmap := congrArg (PMF.map Prod.fst) - (OracleComp.run_interpret_map_state - (fun q s => ProbComp.eval (S.coupledHandler pk sk cStar q s)) - (S.answerHandler pk sk cStar) tablesOf - (fun q s => S.coupledHandler_map_tablesOf pk sk cStar q s) prog st) - simp only [PMF.map_comp, Function.comp_def] at hmap - rw [hmap, OracleComp.run_interpret_simulation_fst _ (S.eagerStateHandler pk sk cStar) _ - (fun q t => S.answerHandler_sim pk sk cStar q t)] + (RandomOracle.complete (fun _ => ProbComp.eval S.pke.sampleCoins) + (RandomOracle.ofList st.gCache)).bind fun G => + (RandomOracle.complete (fun _ => ProbComp.eval S.sampleKey) + (RandomOracle.ofList st.hCache)).bind fun Hraw => + (RandomOracle.complete (fun _ => ProbComp.eval S.sampleKey) + (RandomOracle.ofList st.hqCache)).bind fun Hq => + OracleComp.interpret (S.eagerCoupledHandler G Hq Hraw pk sk cStar) prog := by + have himpl : S.coupledHandler pk sk cStar = fun q => + OracleComp.interpret S.lazyOracle (S.coupledProgram pk sk cStar q) := + funext (S.coupledHandler_eq_interpret pk sk cStar) + have heager (G : M → R) (Hq : CT → K) (Hraw : Bool × M × CT → K) : + S.eagerCoupledHandler G Hq Hraw pk sk cStar = fun q => + OracleComp.interpret (tableOracle G Hraw Hq) (S.coupledProgram pk sk cStar q) := + funext (S.eagerCoupledHandler_eq_interpret G Hq Hraw pk sk cStar) + simp only [heager, himpl, ← OracleComp.interpret_interpret] + rw [RandomOracle.eval_run_interpret_eq_complete_bind S.coupledDistribution S.lazyOracle + coupledCache S.eval_lazyOracle_map_coupledCache, + ← RandomOracle.bind_complete_sum, ← RandomOracle.bind_complete_sum] congr 1 with T : 1 - have hro := congrArg (PMF.map Prod.fst) - (OracleComp.run_interpret_readOnly - (fun q T' => S.eagerCoupledHandler T'.1 T'.2.2 T'.2.1 pk sk cStar q) prog T) - change ((OracleComp.interpret (S.eagerStateHandler pk sk cStar) prog).run T).map Prod.fst = - ((OracleComp.interpret (fun q => S.eagerCoupledHandler T.1 T.2.2 T.2.1 pk sk cStar q) - prog).map (fun a => (a, T))).map Prod.fst at hro - rw [PMF.map_comp] at hro - exact hro.trans (PMF.map_id _) - -end Complete + congr 1 with q : 1 + rcases q with (m | x) | c <;> rfl /-- **Lazy/eager equivalence of the coupled game**: the lazy coupled game `S.coupledGame A b` has the output distribution of the eager coupled game `S.eagerCoupledGame A b`. -/ @@ -290,8 +248,7 @@ theorem eval_coupledGame_eq_eagerCoupledGame [Fintype M] [Finite R] [Fintype CT] rw [PMF.bind_comm] simp only [← hP] simp only [eval_run_coupledHandler_eq_eager] - simp only [completeTables, tablesOf, - RandomOracle.complete_ofList_singleton, RandomOracle.ofList_nil, + simp only [RandomOracle.complete_ofList_singleton, RandomOracle.ofList_nil, RandomOracle.complete_empty, OracleComp.interpret_bind, OracleComp.interpret_query, eagerCoupledHandler, pmf_norm, ROQuery.dispatch] pmf_swap diff --git a/CslibFrontier/Crypto/Protocols/KEM/FujisakiOkamoto/NotBot/Pushforward.lean b/CslibFrontier/Crypto/Protocols/KEM/FujisakiOkamoto/NotBot/Pushforward.lean index 94c5561f01..215356cf2c 100644 --- a/CslibFrontier/Crypto/Protocols/KEM/FujisakiOkamoto/NotBot/Pushforward.lean +++ b/CslibFrontier/Crypto/Protocols/KEM/FujisakiOkamoto/NotBot/Pushforward.lean @@ -8,7 +8,6 @@ module -- upstream: candidate public import CslibFrontier.Crypto.Protocols.KEM.FujisakiOkamoto.NotBot.Hybrids -import CslibFrontier.Probability.PMF.Map import CslibFrontier.Probability.Product.Split import CslibFrontier.Tactic.PMFSwap @@ -54,23 +53,6 @@ open scoped ENNReal NNReal variable {PK SK M R CT K : Type} -/-- An independent product over a sum of index types is the product of the two independent -products over the summands. -/ -private theorem bind_pi_sum {I J γ β : Type} [Fintype I] [Fintype J] [Finite γ] (μ : PMF γ) - (F : (I → γ) → (J → γ) → PMF β) : - (pi fun _ : I ⊕ J => μ).bind (fun f => F (fun i => f (Sum.inl i)) fun j => f (Sum.inr j)) = - (pi fun _ : I => μ).bind fun a => (pi fun _ : J => μ).bind fun b => F a b := by - have hsplit : - (pi fun _ : I ⊕ J => μ).map (Equiv.sumArrowEquivProdArrow I J γ) = - (pi fun _ : I => μ).bind fun a => (pi fun _ : J => μ).map (a, ·) := by - ext ⟨a, b⟩ - rw [map_equiv_apply, bind_map_prodMk_apply, pi_apply, pi_apply, pi_apply, - Fintype.prod_sum_type] - rfl - have h := congrArg (fun p => p.bind fun ab => F ab.1 ab.2) hsplit - simp only [PMF.bind_bind, PMF.map, PMF.pure_bind, Function.comp_def] at h - exact h - namespace Scheme variable [DecidableEq M] [DecidableEq CT] @@ -118,13 +100,13 @@ private theorem bind_pi_reindex [Fintype M] [Fintype CT] [Finite K] (pi fun _ : CT ⊕ ((Bool × M × CT) ⊕ CT) => μ).bind fun f => F (S.coupledH G (fun c => f (.inl c)) (fun x => f (.inr (.inl x))) pk sk) (S.coupledFb G (fun c => f (.inl c)) (fun c => f (.inr (.inr c))) pk sk) := by - refine Eq.symm ((bind_pi_sum μ fun (Hq : CT → K) (g : (Bool × M × CT) ⊕ CT → K) => + refine Eq.symm ((bind_pi_sum (fun _ => μ) fun (Hq : CT → K) (g : (Bool × M × CT) ⊕ CT → K) => F (S.coupledH G Hq (fun x => g (Sum.inl x)) pk sk) (S.coupledFb G Hq (fun c => g (Sum.inr c)) pk sk)).trans ?_) congr 1 with Hq : 1 - exact bind_pi_sum μ fun Hraw Hfb' => + exact bind_pi_sum (fun _ => μ) fun Hraw Hfb' => F (S.coupledH G Hq Hraw pk sk) (S.coupledFb G Hq Hfb' pk sk) - rw [hR, ← bind_pi_sum μ F, + rw [hR, ← bind_pi_sum (fun _ => μ) F, ← pi_map_comp_injective (fun _ : CT ⊕ ((Bool × M × CT) ⊕ CT) => μ) (S.readIndex_injective G pk sk), PMF.bind_map] diff --git a/CslibFrontier/Crypto/Protocols/KEM/FujisakiOkamoto/Security.lean b/CslibFrontier/Crypto/Protocols/KEM/FujisakiOkamoto/Security.lean index 7291eb7212..cb29a66004 100644 --- a/CslibFrontier/Crypto/Protocols/KEM/FujisakiOkamoto/Security.lean +++ b/CslibFrontier/Crypto/Protocols/KEM/FujisakiOkamoto/Security.lean @@ -10,6 +10,8 @@ module public import CslibFrontier.Crypto.Computational.Encryption.KEM public import CslibFrontier.Crypto.Protocols.KEM.FujisakiOkamoto public import CslibFrontier.Languages.Probabilistic.RandomOracle +import CslibFrontier.Languages.Probabilistic.RandomOracle.Probabilistic +import CslibFrontier.Languages.Probabilistic.RandomOracle.Represented import CslibFrontier.Languages.Probabilistic.Simulation import CslibFrontier.Probability.PMF.Union import CslibFrontier.Tactic.PMFSwap @@ -64,8 +66,9 @@ On top of those definitions, this module formalizes: 1. **Executable lazy and eager ROM IND-CCA games for `FO-notbot`** (`Scheme.roIndCcaGame`, `Scheme.indCcaRomAdvantage`, `Scheme.eagerIndCcaGame`) over the oracle interface `ROQuery M CT` (`G`, `H`, and punctured decapsulation rejecting `c = cStar` with `none`), - together with exact eager/lazy equivalence (`Scheme.eval_roIndCcaGame_eq_h1`, - `Scheme.eval_roIndCcaGame_eq_eagerIndCcaGame`, `Scheme.indCcaRomAdvantage_eq_eager`). + together with exact eager/lazy equivalence (`Scheme.eval_roIndCcaGame_eq_eagerIndCcaGame`, + `Scheme.indCcaRomAdvantage_eq_eager`), obtained from the generic represented-cache law + `RandomOracle.eval_run_interpret_eq_complete_bind`. 2. **Keyless ROM simulator and IND-CPA reduction** (`Scheme.simHandler`, `Scheme.romCpaReduction`, `Scheme.simHitProb`). Neither is a verbatim construction from [HofheinzHoevelmannsKiltz2017]; both are adapted to domain-separated `FO-notbot`. `simHandler` is @@ -215,6 +218,12 @@ def ROQueryBounds (A : ROAdversary PK M R CT K) (qG qH : ℕ) : Prop := OracleComp.IsCostBounded ROQuery.gCost (A ch) qG ∧ OracleComp.IsCostBounded ROQuery.hCost (A ch) qH +/-- Bounds `(qG, qH)` on `G` and `H` queries bound their combined count by `qG + qH`. -/ +theorem ROQueryBounds.ghCost {A : ROAdversary PK M R CT K} {qG qH : ℕ} (hq : ROQueryBounds A qG qH) + (ch : KEM.Challenge PK CT K) : OracleComp.IsCostBounded ROQuery.ghCost (A ch) (qG + qH) := by + convert OracleComp.IsCostBounded.add (hq ch).1 (hq ch).2 using 1 + funext q; cases q <;> rfl + /-- An `ROAdversary` satisfies full query bounds `(qG, qH, qD)` if on every challenge `ch` its execution makes at most `qG` queries to `G`, `qH` queries to `H`, and `qD` queries to `decaps`. -/ def ROFullQueryBounds (A : ROAdversary PK M R CT K) (qG qH qD : ℕ) : Prop := @@ -423,370 +432,127 @@ def romCpaReduction (S : Scheme PK SK M R CT K) (A : ROAdversary PK M R CT K) (m0 m1 : M) : PK → CT → ProbComp Bool := S.romFilterCpaReduction (fun _ _ _ => true) A m0 m1 -/-! ### Section 2: Connecting `memoize` to `RandomOracle.answer` and Eager/Lazy Equivalence -/ - -/-- Hybrid 1 handler: `G : M → R` is a complete table while `H : Bool × M × CT → K` is answered -lazily via `RandomOracle.answer`. Decapsulation queries `c ≠ cStar` run `decapsNotBotM` against -these oracles. -/ -noncomputable def h1Handler (S : Scheme PK SK M R CT K) - (G : M → R) (dk : ImplicitSK PK SK M) (cStar : CT) - (q : ROQuery M CT) : - StateT (RandomOracle.Cache (fun _ : Bool × M × CT => K)) PMF (ROResp R K q) := - let H := RandomOracle.answer (fun _ : Bool × M × CT => ProbComp.eval S.sampleKey) - ROQuery.dispatch (pure ∘ G) H (fun c => some <$> S.decapsNotBotM (pure ∘ G) H dk c) cStar q - -/-- A decapsulation query `c ≠ cStar` to `h1Handler`: the `T` check runs on the table `G`, and -only the key derivation touches the `H` table. -/ -private theorem h1Handler_decaps (S : Scheme PK SK M R CT K) (G : M → R) - (dk : ImplicitSK PK SK M) {cStar c : CT} (hc : c ≠ cStar) - (tH : RandomOracle.Cache (fun _ : Bool × M × CT => K)) : - S.h1Handler G dk cStar (.decaps c) tH = - match decT S.pke G dk.pk dk.sk c with - | some m' => - (RandomOracle.answer (fun _ => ProbComp.eval S.sampleKey) (false, m', c) tH).map - (fun (k, tH') => (some k, tH')) - | none => - (RandomOracle.answer (fun _ => ProbComp.eval S.sampleKey) (true, dk.fallback, c) tH).map - (fun (k, tH') => (some k, tH')) := by - simp only [h1Handler, ROQuery.dispatch, hc, ↓reduceIte, decapsNotBotM, decTM_pure, pure_bind] - cases decT S.pke G dk.pk dk.sk c <;> rfl - -/-- Intermediate handler answering `G` and `H` via `RandomOracle.answer` on a pair of -`RandomOracle.Cache` tables `(tG, tH)`. Decapsulation queries `c ≠ cStar` run `decapsNotBotM` -against these table oracles. -/ -noncomputable def roAnswerHandler (S : Scheme PK SK M R CT K) - (dk : ImplicitSK PK SK M) (cStar : CT) (q : ROQuery M CT) : - StateT (RandomOracle.Cache (fun _ : M => R) × - RandomOracle.Cache (fun _ : Bool × M × CT => K)) PMF (ROResp R K q) := - let G : M → StateT (RandomOracle.Cache (fun _ : M => R) × - RandomOracle.Cache (fun _ : Bool × M × CT => K)) PMF R := fun m (tG, tH) => - (RandomOracle.answer (fun _ => ProbComp.eval S.pke.sampleCoins) m tG).map - (fun (r, tG') => (r, (tG', tH))) - let H : Bool × M × CT → StateT (RandomOracle.Cache (fun _ : M => R) × - RandomOracle.Cache (fun _ : Bool × M × CT => K)) PMF K := fun x (tG, tH) => - (RandomOracle.answer (fun _ => ProbComp.eval S.sampleKey) x tH).map - (fun (k, tH') => (k, (tG, tH'))) - ROQuery.dispatch G H (fun c => some <$> S.decapsNotBotM G H dk c) cStar q - -/-- A decapsulation query `c ≠ cStar` to `roAnswerHandler` as explicit table operations. -/ -private theorem roAnswerHandler_decaps (S : Scheme PK SK M R CT K) (dk : ImplicitSK PK SK M) - {cStar c : CT} (hc : c ≠ cStar) (tG : RandomOracle.Cache (fun _ : M => R)) - (tH : RandomOracle.Cache (fun _ : Bool × M × CT => K)) : - S.roAnswerHandler dk cStar (.decaps c) (tG, tH) = - match S.pke.dec dk.sk c with - | none => - (RandomOracle.answer (fun _ => ProbComp.eval S.sampleKey) (true, dk.fallback, c) tH).map - (fun (k, tH') => (some k, (tG, tH'))) - | some m' => - (RandomOracle.answer (fun _ => ProbComp.eval S.pke.sampleCoins) m' tG).bind fun (r', tG') => - if S.pke.encDet dk.pk m' r' = c then - (RandomOracle.answer (fun _ => ProbComp.eval S.sampleKey) (false, m', c) tH).map - (fun (k, tH') => (some k, (tG', tH'))) - else - (RandomOracle.answer (fun _ => ProbComp.eval S.sampleKey) (true, dk.fallback, c) tH).map - (fun (k, tH') => (some k, (tG', tH'))) := by - simp only [roAnswerHandler, ROQuery.dispatch, hc, ↓reduceIte, decapsNotBotM_eq] +/-! ### Section 2: Eager/Lazy Equivalence + +The lazy oracles `G` and `H` of `roHandler` are one lazy random oracle on the joined interface +`ROSpec`, kept in `ROCache` and read through `RandomOracle.ofList`. Every query of the game is the +oracle program `roProgram` over that interface, so +`RandomOracle.eval_run_interpret_eq_complete_bind` replaces both caches by complete tables in one +step, and `RandomOracle.bind_complete_sum` splits the completed table into `G` and `H`. -/ + +/-- The random oracles `G : M → R` and `H : Bool × M × CT → K` as one interface. -/ +private abbrev ROSpec (M R CT K : Type) := (fun _ : M => R) ⊕ₒ (fun _ : Bool × M × CT => K) + +/-- Each query of the ROM IND-CCA game as a program over the random oracles: `G` and `H` are +forwarded, and decapsulation runs `decapsNotBotM` against them. -/ +private def roProgram (S : Scheme PK SK M R CT K) (dk : ImplicitSK PK SK M) (cStar : CT) : + (q : ROQuery M CT) → OracleComp (ROSpec M R CT K) (ROResp R K q) := + ROQuery.dispatch (fun m => OracleComp.query (spec := ROSpec M R CT K) (Sum.inl m)) + (fun x => OracleComp.query (spec := ROSpec M R CT K) (Sum.inr x)) + (fun c => some <$> S.decapsNotBotM + (fun m => OracleComp.query (spec := ROSpec M R CT K) (Sum.inl m)) + (fun x => OracleComp.query (spec := ROSpec M R CT K) (Sum.inr x)) dk c) cStar + +omit [DecidableEq M] in +/-- Interpreting `decapsNotBotM` against oracle calls runs it against the interpreted calls. -/ +private theorem interpret_decapsNotBotM {ι : Type} {spec : OracleSpec ι} {n : Type → Type} + [Monad n] [LawfulMonad n] (oracle : (q : ι) → n (spec q)) (S : Scheme PK SK M R CT K) + (G : M → OracleComp spec R) (H : Bool × M × CT → OracleComp spec K) + (dk : ImplicitSK PK SK M) (c : CT) : + OracleComp.interpret oracle (S.decapsNotBotM G H dk c) = + S.decapsNotBotM (fun m => OracleComp.interpret oracle (G m)) + (fun x => OracleComp.interpret oracle (H x)) dk c := by + rw [decapsNotBotM_eq, decapsNotBotM_eq] cases S.pke.dec dk.sk c with - | none => - dsimp only - simp only [Functor.map, StateT.map, Probability.PMF.monad_bind_eq_bind, - Probability.PMF.monad_pure_eq_pure, PMF.bind_map] - rfl + | none => rfl | some m' => - dsimp only - simp only [Functor.map, StateT.map, bind, StateT.bind, Probability.PMF.monad_pure_eq_pure, - PMF.bind_map, PMF.bind_bind] - congr 1 with a : 1 - dsimp only [Function.comp_apply] - split_ifs <;> rw [PMF.bind_map] <;> rfl - -/-- Evaluating `(some <$> roHashH sampleKey x) st` and mapping `ROCache` via -`RandomOracle.ofList`. -/ -private theorem eval_roHashH_some_map_ofList (sampleKey : ProbComp K) (x : Bool × M × CT) - (st : ROCache M R CT K) : - (ProbComp.eval ((some <$> roHashH sampleKey x) st)).map - (fun (res, st') => - (res, (RandomOracle.ofList st'.gCache, RandomOracle.ofList st'.hCache))) = - (RandomOracle.answer (fun _ => ProbComp.eval sampleKey) x - (RandomOracle.ofList st.hCache)).map - (fun (k, tH') => (some k, (RandomOracle.ofList st.gCache, tH'))) := by - dsimp only [roHashH] - change (ProbComp.eval - (RandomOracle.zoomStateT ROCache.hCache (fun st c => { st with hCache := c }) - (memoize (fun _ => sampleKey) x) st >>= fun a => pure (some a.fst, a.snd))).map _ = _ - simp only [ProbComp.eval_bind, RandomOracle.eval_zoomStateT_memoize, ProbComp.eval_pure, - PMF.map_bind, PMF.bind_map, PMF.pure_map, Function.comp_def] - have h := congrArg (PMF.map (fun (k, tH') => (some k, (RandomOracle.ofList st.gCache, tH')))) - (RandomOracle.memoize_map_ofList (fun _ => ProbComp.eval sampleKey) x st.hCache) - simpa only [PMF.map_comp, Function.comp_def, PMF.map, PMF.bind_bind, PMF.pure_bind] using h - -/-- Mapping `ROCache` via `RandomOracle.ofList` turns `S.roHandler` into `S.roAnswerHandler`. -/ -theorem roHandler_map_ofList (S : Scheme PK SK M R CT K) (dk : ImplicitSK PK SK M) (cStar : CT) - (q : ROQuery M CT) (st : ROCache M R CT K) : - (ProbComp.eval (S.roHandler dk cStar q st)).map - (fun (res, st') => - (res, (RandomOracle.ofList st'.gCache, RandomOracle.ofList st'.hCache))) = - S.roAnswerHandler dk cStar q - (RandomOracle.ofList st.gCache, RandomOracle.ofList st.hCache) := by - let dG : M → PMF R := fun _ => ProbComp.eval S.pke.sampleCoins - let dH : Bool × M × CT → PMF K := fun _ => ProbComp.eval S.sampleKey + simp only [OracleComp.interpret_bind] + congr 1 with r' + split_ifs <;> rfl + +/-- `roHandler` interprets `roProgram` with the lazy oracles `roHashG` and `roHashH`. -/ +private theorem roHandler_eq_interpret (S : Scheme PK SK M R CT K) (dk : ImplicitSK PK SK M) + (cStar : CT) (q : ROQuery M CT) : + S.roHandler dk cStar q = OracleComp.interpret + (OracleComp.sumHandler (roHashG S.pke.sampleCoins) (roHashH S.sampleKey)) + (S.roProgram dk cStar q) := by cases q with - | G m => - dsimp only [roHandler, roHashG, roAnswerHandler, ROQuery.dispatch] - rw [RandomOracle.eval_zoomStateT_memoize] - have h := congrArg (PMF.map (fun (r, tG') => (r, (tG', RandomOracle.ofList st.hCache)))) - (RandomOracle.memoize_map_ofList dG m st.gCache) - simpa only [PMF.map_comp, Function.comp_def, dG] using h - | H x => - dsimp only [roHandler, roHashH, roAnswerHandler, ROQuery.dispatch] - rw [RandomOracle.eval_zoomStateT_memoize] - have h := congrArg (PMF.map (fun (k, tH') => (k, (RandomOracle.ofList st.gCache, tH')))) - (RandomOracle.memoize_map_ofList dH x st.hCache) - simpa only [PMF.map_comp, Function.comp_def, dH] using h + | G m => exact (OracleComp.interpret_query _ _).symm + | H x => exact (OracleComp.interpret_query _ _).symm | decaps c => by_cases hc : c = cStar - · dsimp only [roHandler, roAnswerHandler, ROQuery.dispatch] - simp only [hc, ↓reduceIte] - exact PMF.pure_map _ _ - · rw [roAnswerHandler_decaps S dk hc] - dsimp only [roHandler, ROQuery.dispatch] - simp only [hc, ↓reduceIte, decapsNotBotM_eq] - cases hdec : S.pke.dec dk.sk c with - | none => exact eval_roHashH_some_map_ofList S.sampleKey (true, dk.fallback, c) st - | some m' => - dsimp only - rw [map_bind] - change (ProbComp.eval (roHashG S.pke.sampleCoins m' st >>= fun a => - (some <$> if S.pke.encDet dk.pk m' a.fst = c then roHashH S.sampleKey (false, m', c) - else roHashH S.sampleKey (true, dk.fallback, c)) a.snd)).map _ = _ - dsimp only [roHashG] - simp only [ProbComp.eval_bind, RandomOracle.eval_zoomStateT_memoize, PMF.map_bind, - PMF.bind_map, Function.comp_def] - rw [← RandomOracle.memoize_map_ofList dG m' st.gCache, PMF.bind_map] - congr 1; funext ⟨r', gC'⟩ - dsimp only [Function.comp_def] - by_cases henc : S.pke.encDet dk.pk m' r' = c <;> - simp only [henc, ↓reduceIte] <;> - exact eval_roHashH_some_map_ofList S.sampleKey _ { st with gCache := gC' } - -/-- Single-step simulation from `S.roAnswerHandler` to `S.h1Handler` via -`RandomOracle.answer_complete`. -/ -theorem roAnswerHandler_sim_h1 [Fintype M] [Finite R] - (S : Scheme PK SK M R CT K) (dk : ImplicitSK PK SK M) (cStar : CT) - (q : ROQuery M CT) - (st : RandomOracle.Cache (fun _ : M => R) × RandomOracle.Cache (fun _ : Bool × M × CT => K)) : - (do - let (res, st') ← S.roAnswerHandler dk cStar q st - let G ← RandomOracle.complete (fun _ : M => ProbComp.eval S.pke.sampleCoins) st'.fst - PMF.pure (res, (G, st'.snd))) = - (do - let G ← RandomOracle.complete (fun _ : M => ProbComp.eval S.pke.sampleCoins) st.fst - let (res, tH') ← S.h1Handler G dk cStar q st.snd - PMF.pure (res, (G, tH'))) := by - rcases st with ⟨tG, tH⟩ - let dG : M → PMF R := fun _ => ProbComp.eval S.pke.sampleCoins - let dH : Bool × M × CT → PMF K := fun _ => ProbComp.eval S.sampleKey - simp only [Probability.PMF.monad_bind_eq_bind] + · simp [roHandler, roProgram, hc] + · simp only [roHandler, roProgram, ROQuery.dispatch, hc, ↓reduceIte, + OracleComp.interpret_map, interpret_decapsNotBotM, OracleComp.interpret_query] + +omit [DecidableEq M] in +/-- `eagerHandler` interprets `roProgram` with the complete tables `G` and `H`. -/ +private theorem eagerHandler_eq_interpret (S : Scheme PK SK M R CT K) (G : M → R) + (H : Bool × M × CT → K) (dk : ImplicitSK PK SK M) (cStar : CT) (q : ROQuery M CT) : + S.eagerHandler G H dk cStar q = OracleComp.interpret + (OracleComp.sumHandler (fun m => PMF.pure (G m)) (fun x => PMF.pure (H x))) + (S.roProgram dk cStar q) := by cases q with - | G m => - dsimp only [roAnswerHandler, h1Handler, ROQuery.dispatch, Function.comp_apply, pure, - StateT.pure] - have hc := congrArg (PMF.map (fun (r, G) => (r, (G, tH)))) - (RandomOracle.answer_complete dG tG m) - simpa only [Probability.PMF.monad_bind_eq_bind, PMF.bind_map, PMF.map_bind, PMF.map_comp, - Function.comp_def, PMF.bind_bind, PMF.pure_bind, PMF.map, dG] using hc - | H x => - dsimp only [roAnswerHandler, h1Handler, ROQuery.dispatch] - rw [PMF.bind_map, PMF.bind_comm] - rfl + | G m => exact (OracleComp.interpret_query _ _).symm + | H x => exact (OracleComp.interpret_query _ _).symm | decaps c => by_cases hc : c = cStar - · dsimp only [roAnswerHandler, h1Handler, ROQuery.dispatch] - simp [hc, pure, StateT.pure] - · rw [roAnswerHandler_decaps S dk hc] - simp only [h1Handler_decaps S _ dk hc] - cases hdec : S.pke.dec dk.sk c with - | none => - simp only [decT_eq, hdec, Function.comp_def, PMF.map, PMF.bind_bind, PMF.pure_bind] - exact PMF.bind_comm _ _ _ - | some m' => - simp only [decT_eq, encT, hdec, PMF.bind_bind] - trans (((RandomOracle.answer dG m' tG).bind (fun (r', tG') => - (RandomOracle.complete dG tG').map (fun G => (r', G)))).bind (fun (r', G) => - if S.pke.encDet dk.pk m' r' = c then - (RandomOracle.answer dH (false, m', c) tH).bind - fun (k, tH') => PMF.pure (some k, (G, tH')) - else - (RandomOracle.answer dH (true, dk.fallback, c) tH).bind - fun (k, tH') => PMF.pure (some k, (G, tH')))) - · simp only [PMF.bind_bind] - congr 1; funext ⟨r', tG'⟩ - by_cases henc : S.pke.encDet dk.pk m' r' = c <;> - simp only [henc, ↓reduceIte, PMF.bind_map, Function.comp_def] <;> - exact PMF.bind_comm _ _ _ - · have hG := RandomOracle.answer_complete dG tG m' - simp only [Probability.PMF.monad_bind_eq_bind] at hG - rw [hG, PMF.bind_map] - congr 1 with G : 1 - dsimp only [Function.comp_def] - by_cases henc : S.pke.encDet dk.pk m' (G m') = c <;> - simp [henc, dH, PMF.map] - -/-- Running `A` under `S.roHandler` from `st` has the same output distribution as completing -`st.gCache` via `RandomOracle.complete` and running `A` under `S.h1Handler`. -/ -theorem eval_run_roHandler_eq_h1 [Fintype M] [Finite R] - (S : Scheme PK SK M R CT K) (dk : ImplicitSK PK SK M) (cStar : CT) - (prog : OracleComp (ROResp (M := M) (CT := CT) R K) Bool) (st : ROCache M R CT K) : + · simp [eagerHandler, roProgram, hc] + · simp only [eagerHandler, roProgram, ROQuery.dispatch, hc, ↓reduceIte, + OracleComp.interpret_map, interpret_decapsNotBotM, OracleComp.interpret_query] + change PMF.pure _ = some <$> S.decapsNotBotM (m := PMF) (pure ∘ G) (pure ∘ H) dk c + rw [decapsNotBotM_pure, map_pure] + rfl + +/-- The joined cache represented by the two list caches of an `ROCache`. -/ +private abbrev roTables (st : ROCache M R CT K) : RandomOracle.Cache (ROSpec M R CT K) := + RandomOracle.Cache.sum (RandomOracle.ofList st.gCache) (RandomOracle.ofList st.hCache) + +/-- Each lazy oracle call, read on the joined cache, is a lazy call of the joined oracle. -/ +private theorem eval_roHash_map_roTables (S : Scheme PK SK M R CT K) + (q : M ⊕ (Bool × M × CT)) (st : ROCache M R CT K) : + (ProbComp.eval (OracleComp.sumHandler (roHashG S.pke.sampleCoins) (roHashH S.sampleKey) q + st)).map (fun z => (z.1, roTables z.2)) = + RandomOracle.answer (OracleComp.sumHandler (fun _ => ProbComp.eval S.pke.sampleCoins) + (fun _ => ProbComp.eval S.sampleKey)) q (roTables st) := by + rcases q with m | x + · rw [roTables, RandomOracle.answer_sum_inl] + exact RandomOracle.eval_zoom_memoize_map ROCache.gCache (fun st c => { st with gCache := c }) + S.pke.sampleCoins m st (fun r => r) roTables + (fun c => RandomOracle.Cache.sum c (RandomOracle.ofList st.hCache)) (fun _ => rfl) + · rw [roTables, RandomOracle.answer_sum_inr] + exact RandomOracle.eval_zoom_memoize_map ROCache.hCache (fun st c => { st with hCache := c }) + S.sampleKey x st (fun k => k) roTables + (fun c => RandomOracle.Cache.sum (RandomOracle.ofList st.gCache) c) (fun _ => rfl) + +/-- Running a program under `roHandler` has the law of completing both caches into tables `G` and +`H` and running it under `eagerHandler`. -/ +private theorem eval_run_roHandler_eq_eager [Fintype M] [Finite R] [Fintype CT] [Finite K] + (S : Scheme PK SK M R CT K) (dk : ImplicitSK PK SK M) (cStar : CT) {α : Type} + (prog : OracleComp (ROResp (M := M) (CT := CT) R K) α) (st : ROCache M R CT K) : (ProbComp.eval ((OracleComp.interpret (S.roHandler dk cStar) prog).run st)).map Prod.fst = - (RandomOracle.complete (fun _ : M => ProbComp.eval S.pke.sampleCoins) - (RandomOracle.ofList st.gCache)).bind (fun G => - ((OracleComp.interpret (S.h1Handler G dk cStar) prog).run - (RandomOracle.ofList st.hCache)).map Prod.fst) := by - rw [OracleComp.map_run_interpret ProbComp.isMonadHom_eval] - have hmap := congrArg (PMF.map Prod.fst) - (OracleComp.run_interpret_map_state - (fun q s => ProbComp.eval (S.roHandler dk cStar q s)) - (S.roAnswerHandler dk cStar) - (fun s => (RandomOracle.ofList s.gCache, RandomOracle.ofList s.hCache)) - (fun q s => S.roHandler_map_ofList dk cStar q s) prog st) - simp only [PMF.map_comp, Function.comp_def] at hmap - rw [hmap] - let sim : (RandomOracle.Cache (fun _ : M => R) × - RandomOracle.Cache (fun _ : Bool × M × CT => K)) → - PMF ((M → R) × RandomOracle.Cache (fun _ : Bool × M × CT => K)) := - fun (tG, tH) => (RandomOracle.complete (fun _ : M => ProbComp.eval S.pke.sampleCoins) tG).map - (fun G => (G, tH)) - let h₂ : (q : ROQuery M CT) → - StateT ((M → R) × RandomOracle.Cache (fun _ : Bool × M × CT => K)) PMF (ROResp R K q) := - fun q (G, tH) => (S.h1Handler G dk cStar q tH).map (fun (res, tH') => (res, (G, tH'))) - have hsim := OracleComp.run_interpret_simulation_fst - (S.roAnswerHandler dk cStar) h₂ sim - (fun q s => by - simpa only [sim, h₂, Probability.PMF.monad_bind_eq_bind, PMF.bind_map, PMF.map_bind, - Function.comp_def, PMF.map, PMF.bind_bind, PMF.pure_bind] using - S.roAnswerHandler_sim_h1 dk cStar q s) - prog (RandomOracle.ofList st.gCache, RandomOracle.ofList st.hCache) - simp only [sim, PMF.bind_map, Function.comp_def] at hsim - rw [hsim] - congr 1 with G : 1 - have hproj := congrArg (PMF.map Prod.fst) - (OracleComp.run_interpret_map_state - (S.h1Handler G dk cStar) h₂ (fun tH => (G, tH)) - (fun q tH => rfl) prog (RandomOracle.ofList st.hCache)) - simpa only [PMF.map_comp, Function.comp_def] using hproj.symm - -/-- Evaluating `S.roIndCcaGame A b` equals sampling `G` eagerly from `pi` and running `A` -against `S.h1Handler`. -/ -theorem eval_roIndCcaGame_eq_h1 [Fintype M] [Finite R] - (S : Scheme PK SK M R CT K) (A : ROAdversary PK M R CT K) (b : Bool) : - ProbComp.eval (S.roIndCcaGame A b) = - (ProbComp.eval S.keyGenNotBot).bind (fun (pk, dk) => - (ProbComp.eval S.sampleMsg).bind (fun mStar => - (pi (α := fun _ : M => R) (fun _ => ProbComp.eval S.pke.sampleCoins)).bind (fun G => - let cStar := S.pke.encDet pk mStar (G mStar) - (ProbComp.eval S.sampleKey).bind (fun kReal => - (ProbComp.eval S.sampleKey).bind (fun kRand => - let kStar := if b then kRand else kReal - let tH₀ := RandomOracle.ofList [((false, mStar, cStar), kReal)] - ((OracleComp.interpret (S.h1Handler G dk cStar) (A ⟨pk, cStar, kStar⟩)).run tH₀).map - Prod.fst))))) := by - dsimp only [roIndCcaGame] - simp only [ProbComp.eval_bind, ProbComp.eval_pure] - congr 1; funext ⟨pk, dk⟩ - congr 1 with mStar : 1 - let dG : M → PMF R := fun _ => ProbComp.eval S.pke.sampleCoins - have hstep (rStar : R) (kReal kRand : K) : - (ProbComp.eval ((OracleComp.interpret (S.roHandler dk (S.pke.encDet pk mStar rStar)) - (A ⟨pk, S.pke.encDet pk mStar rStar, if b then kRand else kReal⟩)).run - { gCache := [(mStar, rStar)], - hCache := [((false, mStar, S.pke.encDet pk mStar rStar), kReal)] })).bind - (fun x => PMF.pure x.fst) = - (pi (Function.update dG mStar (PMF.pure rStar))).bind (fun G => - ((OracleComp.interpret (S.h1Handler G dk (S.pke.encDet pk mStar rStar)) - (A ⟨pk, S.pke.encDet pk mStar rStar, if b then kRand else kReal⟩)).run - (RandomOracle.ofList [((false, mStar, S.pke.encDet pk mStar rStar), kReal)])).map - Prod.fst) := by - change (ProbComp.eval _).map Prod.fst = _ - rw [eval_run_roHandler_eq_h1, RandomOracle.complete_ofList_singleton] - simp only [hstep] - rw [← bind_pi_update dG mStar (fun rStar G => - let cStar := S.pke.encDet pk mStar rStar - (ProbComp.eval S.sampleKey).bind fun kReal => - (ProbComp.eval S.sampleKey).bind fun kRand => - ((OracleComp.interpret (S.h1Handler G dk cStar) - (A ⟨pk, cStar, if b then kRand else kReal⟩)).run - (RandomOracle.ofList [((false, mStar, cStar), kReal)])).map Prod.fst)] - congr 1 with rStar : 1 - pmf_swap - -/-- Single-step simulation from `S.h1Handler` to `S.eagerHandler` via -`RandomOracle.answer_complete`. -/ -theorem h1Handler_sim_eager [Fintype M] [Fintype CT] [Finite K] - (S : Scheme PK SK M R CT K) (G : M → R) (dk : ImplicitSK PK SK M) (cStar : CT) - (q : ROQuery M CT) (tH : RandomOracle.Cache (fun _ : Bool × M × CT => K)) : - (do - let (res, tH') ← S.h1Handler G dk cStar q tH - let H ← RandomOracle.complete (fun _ : Bool × M × CT => ProbComp.eval S.sampleKey) tH' - PMF.pure (res, H)) = - (do - let H ← RandomOracle.complete (fun _ : Bool × M × CT => ProbComp.eval S.sampleKey) tH - let res ← S.eagerHandler G H dk cStar q - PMF.pure (res, H)) := by - let dH : Bool × M × CT → PMF K := fun _ => ProbComp.eval S.sampleKey - simp only [Probability.PMF.monad_bind_eq_bind] - cases q with - | G m => - simp [h1Handler, eagerHandler, pure, StateT.pure] - | H x => - dsimp only [h1Handler, eagerHandler, ROQuery.dispatch] - simpa only [Probability.PMF.monad_bind_eq_bind, PMF.pure_bind, PMF.map, Function.comp_def, dH] - using RandomOracle.answer_complete dH tH x - | decaps c => - by_cases hc : c = cStar - · dsimp only [h1Handler, eagerHandler, ROQuery.dispatch] - simp [hc, pure, StateT.pure] - · rw [h1Handler_decaps S G dk hc] - dsimp only [eagerHandler, decapsNotBot_eq, ROQuery.dispatch] - simp only [hc, ↓reduceIte] - cases hdec : decT S.pke G dk.pk dk.sk c with - | none => - have hH := congrArg (PMF.map (fun (k, H) => (some k, H))) - (RandomOracle.answer_complete dH tH (true, dk.fallback, c)) - simpa only [Probability.PMF.monad_bind_eq_bind, PMF.bind_map, PMF.map_bind, PMF.map_comp, - Function.comp_def, PMF.bind_bind, PMF.pure_bind, PMF.map, dH] using hH - | some m' => - have hH := congrArg (PMF.map (fun (k, H) => (some k, H))) - (RandomOracle.answer_complete dH tH (false, m', c)) - simpa only [Probability.PMF.monad_bind_eq_bind, PMF.bind_map, PMF.map_bind, PMF.map_comp, - Function.comp_def, PMF.bind_bind, PMF.pure_bind, PMF.map, dH] using hH - -/-- Running `prog` under `S.h1Handler G dk cStar` from `tH` has the same output distribution as -completing `tH` via `RandomOracle.complete` and interpreting `prog` under `S.eagerHandler`. -/ -theorem eval_run_h1Handler_eq_eager [Fintype M] [Fintype CT] [Finite K] - (S : Scheme PK SK M R CT K) (G : M → R) (dk : ImplicitSK PK SK M) (cStar : CT) - (prog : OracleComp (ROResp (M := M) (CT := CT) R K) Bool) - (tH : RandomOracle.Cache (fun _ : Bool × M × CT => K)) : - ((OracleComp.interpret (S.h1Handler G dk cStar) prog).run tH).map Prod.fst = - (RandomOracle.complete (fun _ : Bool × M × CT => ProbComp.eval S.sampleKey) tH).bind (fun H => - OracleComp.interpret (S.eagerHandler G H dk cStar) prog) := by - let h₂ : (q : ROQuery M CT) → StateT (Bool × M × CT → K) PMF (ROResp R K q) := - fun q H => (S.eagerHandler G H dk cStar q).map (fun res => (res, H)) - have hsim := OracleComp.run_interpret_simulation_fst - (S.h1Handler G dk cStar) h₂ - (RandomOracle.complete (fun _ : Bool × M × CT => ProbComp.eval S.sampleKey)) - (fun q s => by - simpa only [h₂, Probability.PMF.monad_bind_eq_bind, PMF.map, Function.comp_def] using - S.h1Handler_sim_eager G dk cStar q s) - prog tH - rw [hsim] - congr 1 with H : 1 - have hro := congrArg (PMF.map Prod.fst) - (OracleComp.run_interpret_readOnly (fun q H' => S.eagerHandler G H' dk cStar q) prog H) - change ((OracleComp.interpret h₂ prog).run H).map Prod.fst = - ((OracleComp.interpret (fun q => S.eagerHandler G H dk cStar q) prog).map - (fun a => (a, H))).map Prod.fst at hro - rw [PMF.map_comp] at hro - exact hro.trans (PMF.map_id _) + (RandomOracle.complete (fun _ => ProbComp.eval S.pke.sampleCoins) + (RandomOracle.ofList st.gCache)).bind fun G => + (RandomOracle.complete (fun _ => ProbComp.eval S.sampleKey) + (RandomOracle.ofList st.hCache)).bind fun H => + OracleComp.interpret (S.eagerHandler G H dk cStar) prog := by + have himpl : S.roHandler dk cStar = fun q => OracleComp.interpret + (OracleComp.sumHandler (roHashG S.pke.sampleCoins) (roHashH S.sampleKey)) + (S.roProgram dk cStar q) := funext (S.roHandler_eq_interpret dk cStar) + have heager (G : M → R) (H : Bool × M × CT → K) : S.eagerHandler G H dk cStar = fun q => + OracleComp.interpret + (OracleComp.sumHandler (fun m => PMF.pure (G m)) (fun x => PMF.pure (H x))) + (S.roProgram dk cStar q) := funext (S.eagerHandler_eq_interpret G H dk cStar) + simp only [heager, himpl, ← OracleComp.interpret_interpret] + rw [RandomOracle.eval_run_interpret_eq_complete_bind + (OracleComp.sumHandler (fun _ => ProbComp.eval S.pke.sampleCoins) + (fun _ => ProbComp.eval S.sampleKey)) + (OracleComp.sumHandler (roHashG S.pke.sampleCoins) (roHashH S.sampleKey)) roTables + S.eval_roHash_map_roTables, + ← RandomOracle.bind_complete_sum] + congr 1 with T : 1 + congr 1 with q : 1 + rcases q with m | x <;> rfl /-- **Eager/lazy equivalence for the `FO-notbot` ROM IND-CCA game**: evaluating the executable lazy-cached game `S.roIndCcaGame A b` yields the exact same output distribution as the eager @@ -794,26 +560,41 @@ random-oracle game `S.eagerIndCcaGame A b`. -/ theorem eval_roIndCcaGame_eq_eagerIndCcaGame [Fintype M] [Finite R] [Fintype CT] [Finite K] (S : Scheme PK SK M R CT K) (A : ROAdversary PK M R CT K) (b : Bool) : ProbComp.eval (S.roIndCcaGame A b) = S.eagerIndCcaGame A b := by - rw [eval_roIndCcaGame_eq_h1] + let dG : M → PMF R := fun _ => ProbComp.eval S.pke.sampleCoins + let dH : Bool × M × CT → PMF K := fun _ => ProbComp.eval S.sampleKey + dsimp only [roIndCcaGame] simp only [eagerIndCcaGame, encapsNotBot, encapsBot, encT, Probability.PMF.monad_bind_eq_bind, ProbComp.eval_bind, ProbComp.eval_pure, PMF.bind_bind, PMF.pure_bind] congr 1; funext ⟨pk, dk⟩ - let dH : Bool × M × CT → PMF K := fun _ => ProbComp.eval S.sampleKey - pmf_swap with G mStar - set cStar := S.pke.encDet pk mStar (G mStar) - have hstep (kReal kRand : K) : - ((OracleComp.interpret (S.h1Handler G dk cStar) - (A ⟨pk, cStar, if b then kRand else kReal⟩)).run - (RandomOracle.ofList [((false, mStar, cStar), kReal)])).map Prod.fst = - (pi (Function.update dH (false, mStar, cStar) (PMF.pure kReal))).bind (fun H => - OracleComp.interpret (S.eagerHandler G H dk cStar) - (A ⟨pk, cStar, if b then kRand else kReal⟩)) := by - rw [eval_run_h1Handler_eq_eager, RandomOracle.complete_ofList_singleton] + have hstep (mStar : M) (rStar : R) (kReal kRand : K) : + (ProbComp.eval ((OracleComp.interpret (S.roHandler dk (S.pke.encDet pk mStar rStar)) + (A ⟨pk, S.pke.encDet pk mStar rStar, if b then kRand else kReal⟩)).run + { gCache := [(mStar, rStar)], + hCache := [((false, mStar, S.pke.encDet pk mStar rStar), kReal)] })).bind + (fun x => PMF.pure x.fst) = + (pi (Function.update dG mStar (PMF.pure rStar))).bind fun G => + (pi (Function.update dH (false, mStar, S.pke.encDet pk mStar rStar) + (PMF.pure kReal))).bind fun H => + OracleComp.interpret (S.eagerHandler G H dk (S.pke.encDet pk mStar rStar)) + (A ⟨pk, S.pke.encDet pk mStar rStar, if b then kRand else kReal⟩) := by + change (ProbComp.eval _).map Prod.fst = _ + rw [eval_run_roHandler_eq_eager, RandomOracle.complete_ofList_singleton, + RandomOracle.complete_ofList_singleton] simp only [hstep] - refine Eq.trans ?_ (bind_pi_update dH (false, mStar, cStar) (fun kReal H => + pmf_hoist (ProbComp.eval S.sampleMsg) + congr 1 with mStar : 1 + rw [← bind_pi_update dG mStar fun rStar G => + (pi dH).bind fun H => (ProbComp.eval S.sampleKey).bind fun kRand => + OracleComp.interpret (S.eagerHandler G H dk (S.pke.encDet pk mStar rStar)) + (A ⟨pk, S.pke.encDet pk mStar rStar, + if b then kRand else H (false, mStar, S.pke.encDet pk mStar rStar)⟩)] + congr 1 with rStar : 1 + pmf_hoist (pi (Function.update dG mStar (PMF.pure rStar))) + congr 1 with G : 1 + rw [← bind_pi_update dH (false, mStar, S.pke.encDet pk mStar rStar) fun kReal H => (ProbComp.eval S.sampleKey).bind fun kRand => - OracleComp.interpret (S.eagerHandler G H dk cStar) - (A ⟨pk, cStar, if b then kRand else kReal⟩))) + OracleComp.interpret (S.eagerHandler G H dk (S.pke.encDet pk mStar rStar)) + (A ⟨pk, S.pke.encDet pk mStar rStar, if b then kRand else kReal⟩)] congr 1 with kReal : 1 exact PMF.bind_comm _ _ _ @@ -1035,11 +816,7 @@ theorem sum_simFilterHitProb_le [Fintype M] (S : Scheme PK SK M R CT K) obtain ⟨keys, -, rStar, -, kStar, -, hrun⟩ := hx set pk := keys.fst set cStar := S.pke.encDet pk m₀ rStar - have hcost : OracleComp.IsCostBounded ROQuery.ghCost (A ⟨pk, cStar, kStar⟩) (qG + qH) := by - have ⟨hG, hH⟩ := hq ⟨pk, cStar, kStar⟩ - convert OracleComp.IsCostBounded.add hG hH using 1 - funext q; cases q <;> rfl - have hlen := hcost.measure_le + have hlen := (hq.ghCost ⟨pk, cStar, kStar⟩).measure_le (fun q st => ProbComp.eval (S.simFilterHandler (d pk) pk cStar q st)) (fun st : SimState M R CT K => st.gCache.length) (S.simFilterHandler_gCache_length_le (d pk) pk cStar) diff --git a/CslibFrontier/Languages/Probabilistic/RandomOracle/Represented.lean b/CslibFrontier/Languages/Probabilistic/RandomOracle/Represented.lean new file mode 100644 index 0000000000..f4bfd25fde --- /dev/null +++ b/CslibFrontier/Languages/Probabilistic/RandomOracle/Represented.lean @@ -0,0 +1,109 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import CslibFrontier.Languages.Probabilistic.RandomOracle.Sum +import CslibFrontier.Languages.Probabilistic.Semantics +import CslibFrontier.Languages.Probabilistic.Simulation +import CslibFrontier.Probability.Product.Split + +/-! +# Lazy random oracles behind a represented state + +A game usually keeps its random-oracle tables in its own state: association lists, several caches +in a record, or caches for several oracles at once. When each call of such a handler, read through +a map `rep` from the game state to a `RandomOracle.Cache`, is a lazy `RandomOracle.answer`, the +game has the law of completing the represented cache once and answering every call from the +completed table (`eval_run_interpret_eq_complete_bind`). The per-call hypothesis is the only +game-specific step of an eager/lazy argument. + +Several oracles are one oracle on the sum of their interfaces. `RandomOracle.Cache.sum`, re-exported +here, joins their caches, so that one represented state serves them all, and `bind_complete_sum` +splits the completed table back into one table per oracle. + +## Main results + +* `Cslib.RandomOracle.run_interpret_eq_complete_bind`, + `Cslib.RandomOracle.eval_run_interpret_eq_complete_bind`: a handler that is a lazy random oracle + on a represented cache has the law of the completed table. +* `Cslib.RandomOracle.bind_complete_sum`: completing a joined cache completes each side + independently. +-/ + +public section + +namespace Cslib.RandomOracle + +open Probability +open scoped Cslib + +section Represented + +variable {Query State α : Type} {Response : Query → Type} [DecidableEq Query] [Fintype Query] + [∀ q, Finite (Response q)] + +/-- A stateful handler that, read through `rep`, answers every call as the lazy random oracle +`answer distribution` has the result law of completing the represented initial cache and answering +every call from the completed table. -/ +theorem run_interpret_eq_complete_bind (distribution : (q : Query) → PMF (Response q)) + (impl : (q : Query) → StateT State PMF (Response q)) (rep : State → Cache Response) + (step : ∀ q s, (impl q s).map (fun z => (z.1, rep z.2)) = answer distribution q (rep s)) + (program : OracleComp Response α) (s : State) : + ((OracleComp.interpret impl program).run s).map Prod.fst = + (complete distribution (rep s)).bind fun table => + OracleComp.interpret (fun q => PMF.pure (table q)) program := by + have hrep := congrArg (PMF.map Prod.fst) + (OracleComp.run_interpret_map_state impl (answer distribution) rep step program s) + have hcomplete := congrArg (PMF.map Prod.fst) + (run_interpret_answer_complete distribution program (rep s)) + simp only [PMF.monad_bind_eq_bind, PMF.map_bind, PMF.map_comp, Function.comp_def] at hcomplete + change ((OracleComp.interpret (answer distribution) program).run (rep s)).bind + (fun a => (complete distribution a.2).map (Function.const _ a.1)) = + (complete distribution (rep s)).bind (fun table => + (OracleComp.interpret (fun q => PMF.pure (table q)) program).map id) at hcomplete + simp only [PMF.map_const, PMF.map_id] at hcomplete + simp only [PMF.map_comp, Function.comp_def] at hrep + rw [hrep, ← hcomplete] + rfl + +/-- A closed stateful handler that, read through `rep`, answers every call as the lazy random +oracle `answer distribution` has the result law of completing the represented initial cache and +answering every call from the completed table. -/ +theorem eval_run_interpret_eq_complete_bind (distribution : (q : Query) → PMF (Response q)) + (impl : (q : Query) → StateT State ProbComp (Response q)) (rep : State → Cache Response) + (step : ∀ q s, + (ProbComp.eval (impl q s)).map (fun z => (z.1, rep z.2)) = answer distribution q (rep s)) + (program : OracleComp Response α) (s : State) : + (ProbComp.eval ((OracleComp.interpret impl program).run s)).map Prod.fst = + (complete distribution (rep s)).bind fun table => + OracleComp.interpret (fun q => PMF.pure (table q)) program := by + rw [OracleComp.map_run_interpret ProbComp.isMonadHom_eval] + exact run_interpret_eq_complete_bind distribution _ rep step program s + +end Represented + +section Sum + +universe u + +variable {ι₁ ι₂ : Type u} {spec₁ : OracleSpec.{u, u} ι₁} {spec₂ : OracleSpec.{u, u} ι₂} + +/-- Completing a joined cache completes its two sides independently. -/ +theorem bind_complete_sum [Fintype ι₁] [Fintype ι₂] [∀ q, Finite (spec₁ q)] + [∀ q, Finite (spec₂ q)] {γ : Type u} (d₁ : (q : ι₁) → PMF (spec₁ q)) + (d₂ : (q : ι₂) → PMF (spec₂ q)) (c₁ : Cache spec₁) (c₂ : Cache spec₂) + (F : ((q : ι₁) → spec₁ q) → ((q : ι₂) → spec₂ q) → PMF γ) : + (complete (OracleComp.sumHandler d₁ d₂) (Cache.sum c₁ c₂)).bind + (fun table => F (fun q => table (.inl q)) fun q => table (.inr q)) = + (complete d₁ c₁).bind fun t₁ => (complete d₂ c₂).bind fun t₂ => F t₁ t₂ := + PMF.bind_pi_sum (β := spec₁ ⊕ₒ spec₂) + (fun q => (Cache.sum c₁ c₂ q).elim (OracleComp.sumHandler d₁ d₂ q) PMF.pure) F + +end Sum + +end Cslib.RandomOracle diff --git a/CslibFrontier/Languages/Probabilistic/RandomOracle/Sum.lean b/CslibFrontier/Languages/Probabilistic/RandomOracle/Sum.lean new file mode 100644 index 0000000000..e7d69f336a --- /dev/null +++ b/CslibFrontier/Languages/Probabilistic/RandomOracle/Sum.lean @@ -0,0 +1,115 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import CslibFrontier.Languages.Probabilistic.RandomOracle +public import CslibFrontier.Languages.Probabilistic.Sum + +/-! +# Random-oracle caches on a sum of interfaces + +Several independent lazy random oracles are one lazy random oracle on the sum of their interfaces, +answered by `OracleComp.sumHandler`. `RandomOracle.Cache.sum` joins one cache per side into a cache +of the joined interface, and a lazy call on one side of a joined cache is a lazy call on that side's +cache (`answer_sum_inl`, `answer_sum_inr`). A game that keeps one cache per oracle can therefore be +read as one represented lazy oracle. + +## Main definitions + +* `Cslib.RandomOracle.Cache.sum`: the cache of `spec₁ ⊕ₒ spec₂` built from one cache for each side. + +## Main results + +* `Cslib.RandomOracle.answer_sum_inl`, `Cslib.RandomOracle.answer_sum_inr`: a lazy call on one side + of a joined cache is a lazy call on that side's cache. +* `Cslib.RandomOracle.Cache.update_sum_inl`, `Cslib.RandomOracle.Cache.update_sum_inr`: recording + an answer in a joined cache records it on its side. +-/ + +public section + +namespace Cslib.RandomOracle + +open scoped Cslib + +universe u + +variable {ι₁ ι₂ : Type u} {spec₁ : OracleSpec.{u, u} ι₁} {spec₂ : OracleSpec.{u, u} ι₂} + +/-- The cache of the joined interface `spec₁ ⊕ₒ spec₂`: left queries read `c₁`, right queries read +`c₂`. -/ +@[expose] def Cache.sum (c₁ : Cache spec₁) (c₂ : Cache spec₂) : Cache (spec₁ ⊕ₒ spec₂) + | .inl q => c₁ q + | .inr q => c₂ q + +@[simp] theorem Cache.sum_inl (c₁ : Cache spec₁) (c₂ : Cache spec₂) (q : ι₁) : + Cache.sum c₁ c₂ (.inl q) = c₁ q := rfl + +@[simp] theorem Cache.sum_inr (c₁ : Cache spec₁) (c₂ : Cache spec₂) (q : ι₂) : + Cache.sum c₁ c₂ (.inr q) = c₂ q := rfl + +/-- The responses of a joined interface are finite when both sides' responses are. -/ +instance [∀ q, Finite (spec₁ q)] [∀ q, Finite (spec₂ q)] : ∀ q, Finite ((spec₁ ⊕ₒ spec₂) q) + | .inl q => inferInstanceAs (Finite (spec₁ q)) + | .inr q => inferInstanceAs (Finite (spec₂ q)) + +variable [DecidableEq ι₁] [DecidableEq ι₂] + +/-- Recording a left answer in a joined cache records it in the left cache. -/ +theorem Cache.update_sum_inl (c₁ : Cache spec₁) (c₂ : Cache spec₂) (q : ι₁) (v : spec₁ q) : + Function.update (Cache.sum c₁ c₂) (.inl q) (some v) = + Cache.sum (Function.update c₁ q (some v)) c₂ := by + funext q' + rcases q' with q' | q' + · by_cases h : q' = q + · subst h; simp + · simp [Function.update_of_ne h, Function.update_of_ne (Sum.inl_injective.ne h)] + · simp + +/-- Recording a right answer in a joined cache records it in the right cache. -/ +theorem Cache.update_sum_inr (c₁ : Cache spec₁) (c₂ : Cache spec₂) (q : ι₂) (v : spec₂ q) : + Function.update (Cache.sum c₁ c₂) (.inr q) (some v) = + Cache.sum c₁ (Function.update c₂ q (some v)) := by + funext q' + rcases q' with q' | q' + · simp + · by_cases h : q' = q + · subst h; simp + · simp [Function.update_of_ne h, Function.update_of_ne (Sum.inr_injective.ne h)] + +/-- A lazy call on the left side of a joined cache is a lazy call on the left cache. -/ +theorem answer_sum_inl (d₁ : (q : ι₁) → PMF (spec₁ q)) (d₂ : (q : ι₂) → PMF (spec₂ q)) + (c₁ : Cache spec₁) (c₂ : Cache spec₂) (q : ι₁) : + answer (OracleComp.sumHandler d₁ d₂) (.inl q) (Cache.sum c₁ c₂) = + (answer d₁ q c₁).map fun z => (z.1, Cache.sum z.2 c₂) := by + cases h : c₁ q with + | none => + rw [answer_of_none d₁ c₁ q h, + answer_of_none (OracleComp.sumHandler d₁ d₂) (Cache.sum c₁ c₂) (.inl q) h, PMF.map_comp] + exact congrArg (PMF.map · (d₁ q)) + (funext fun v => Prod.ext rfl (Cache.update_sum_inl c₁ c₂ q v)) + | some v => + rw [answer_of_some d₁ c₁ q v h, + answer_of_some (OracleComp.sumHandler d₁ d₂) (Cache.sum c₁ c₂) (.inl q) v h, PMF.pure_map] + +/-- A lazy call on the right side of a joined cache is a lazy call on the right cache. -/ +theorem answer_sum_inr (d₁ : (q : ι₁) → PMF (spec₁ q)) (d₂ : (q : ι₂) → PMF (spec₂ q)) + (c₁ : Cache spec₁) (c₂ : Cache spec₂) (q : ι₂) : + answer (OracleComp.sumHandler d₁ d₂) (.inr q) (Cache.sum c₁ c₂) = + (answer d₂ q c₂).map fun z => (z.1, Cache.sum c₁ z.2) := by + cases h : c₂ q with + | none => + rw [answer_of_none d₂ c₂ q h, + answer_of_none (OracleComp.sumHandler d₁ d₂) (Cache.sum c₁ c₂) (.inr q) h, PMF.map_comp] + exact congrArg (PMF.map · (d₂ q)) + (funext fun v => Prod.ext rfl (Cache.update_sum_inr c₁ c₂ q v)) + | some v => + rw [answer_of_some d₂ c₂ q v h, + answer_of_some (OracleComp.sumHandler d₁ d₂) (Cache.sum c₁ c₂) (.inr q) v h, PMF.pure_map] + +end Cslib.RandomOracle diff --git a/CslibFrontier/Probability/Product/Split.lean b/CslibFrontier/Probability/Product/Split.lean index ac56023c61..9813cc31a1 100644 --- a/CslibFrontier/Probability/Product/Split.lean +++ b/CslibFrontier/Probability/Product/Split.lean @@ -20,6 +20,7 @@ Split the coordinates of an independent product by a predicate `P`, along Mathli `Equiv.piEquivPiSubtypeProd`. The coordinates satisfying `P` and the remaining coordinates form two independent products. In particular, the restriction of an independent product to some of its coordinates, or its composition with an injection of index types, is again an independent product. +An independent product over a sum of index types splits the same way into its two summands. Conditioning a uniform tuple on the value of one coordinate splits that coordinate off: it becomes constant, and the other coordinates stay uniform. @@ -30,6 +31,8 @@ constant, and the other coordinates stay uniform. * `Cslib.Probability.PMF.pi_map_restrict`, `Cslib.Probability.PMF.pi_map_comp_injective`: restricting an independent product, or reading it along an injection, gives the independent product of the selected factors. +* `Cslib.Probability.PMF.pi_map_sumPiEquivProdPi`, `Cslib.Probability.PMF.bind_pi_sum`: an + independent product over `ι ⊕ κ` is a pair of independent products over `ι` and `κ`. * `Cslib.Probability.PMF.filter_uniformOfFintype_eval_eq`: conditioning a uniform tuple on one coordinate sets that coordinate. * `Cslib.Probability.PMF.uniformOfFintype_map_comp_dep`: a uniform dependent function read @@ -85,6 +88,32 @@ theorem pi_map_comp_injective {κ : Type*} [Fintype κ] (p : ∀ i, PMF (α i)) (pi p).map (fun a k => a (e k)) = pi fun k => p (e k) := pi_map_comp_subtypeEquiv (· ∈ Set.range e) p (Equiv.ofInjective e he) +section Sum + +variable {ι κ : Type*} [Fintype ι] [Fintype κ] {β : ι ⊕ κ → Type*} [∀ i, Finite (β i)] + +/-- An independent product over `ι ⊕ κ` splits, along Mathlib's `Equiv.sumPiEquivProdPi`, into +independent products over `ι` and over `κ`. -/ +theorem pi_map_sumPiEquivProdPi (p : ∀ i, PMF (β i)) : + (pi p).map (Equiv.sumPiEquivProdPi β) = + (pi fun i => p (.inl i)).bind fun a => (pi fun j => p (.inr j)).map (a, ·) := by + ext ⟨a, b⟩ + rw [map_equiv_apply, bind_map_prodMk_apply, pi_apply, pi_apply, pi_apply, + Fintype.prod_sum_type] + rfl + +/-- An experiment reading the two halves of an independent product over `ι ⊕ κ` samples each half +independently. -/ +theorem bind_pi_sum {γ : Type*} (p : ∀ i, PMF (β i)) + (F : (∀ i, β (.inl i)) → (∀ j, β (.inr j)) → PMF γ) : + (pi p).bind (fun f => F (fun i => f (.inl i)) fun j => f (.inr j)) = + (pi fun i => p (.inl i)).bind fun a => (pi fun j => p (.inr j)).bind fun b => F a b := by + have h := congrArg (fun q => q.bind fun ab => F ab.1 ab.2) (pi_map_sumPiEquivProdPi p) + simp only [PMF.bind_bind, PMF.map, PMF.pure_bind, Function.comp_def] at h + exact h + +end Sum + /-- Conditioning a uniform tuple on the value `c` of its coordinate `j` sets that coordinate to `c` and keeps the other coordinates uniform. -/ theorem filter_uniformOfFintype_eval_eq [DecidableEq ι] {γ : Type*} [Fintype γ] [Nonempty γ] diff --git a/manual/workflows/probabilistic-workflows.md b/manual/workflows/probabilistic-workflows.md index 85a5026926..5820000fc0 100644 --- a/manual/workflows/probabilistic-workflows.md +++ b/manual/workflows/probabilistic-workflows.md @@ -1505,6 +1505,41 @@ child-table equations remain local mathematical obligations. These eager tables prove distributional equalities; the executable reductions retain their existing separate runtime and query-bound certificates. +## Replace a game's own caches by complete tables + +Use this route when a game keeps its random-oracle caches in its own state, such as association +lists in a record or several caches for several oracles, rather than running a program through +`memoize`. Import +[RandomOracle/Represented.lean](../../CslibFrontier/Languages/Probabilistic/RandomOracle/Represented.lean). + +1. Join the oracles into one interface with `⊕ₒ` and write each game query as an oracle program + over it. Write the lazy handler and the complete-table handler as `interpret` of the same + program, so the game logic is stated once. +2. Choose `rep : State → RandomOracle.Cache spec`, the cache that the state represents. Build it + from one cache per oracle with `RandomOracle.Cache.sum` from + [RandomOracle/Sum.lean](../../CslibFrontier/Languages/Probabilistic/RandomOracle/Sum.lean), + which `Represented.lean` re-exports, and read list caches with `RandomOracle.ofList`. +3. Prove the per-call step: each lazy handler call, with its next state mapped by `rep`, is + `RandomOracle.answer` on the represented cache. On a joined cache, `answer_sum_inl` and + `answer_sum_inr` reduce this to one side, and `RandomOracle.eval_zoom_memoize_map` proves it for + a `zoomStateT`/`memoize` cache. +4. Apply `RandomOracle.eval_run_interpret_eq_complete_bind`, or `run_interpret_eq_complete_bind` + for a handler that already returns `PMF`. The run's result law becomes completing `rep s` once + and answering every call from the table. `RandomOracle.bind_complete_sum` then splits the + completed table into one independent table per oracle. + +This proves an exact equality, so step 3 fails when a handler also inspects its caches directly, +for example a decapsulation filter that checks whether a message was already queried. Such a hop +needs an approximate simulation instead, as in `closeTo_cachedCoupledBotGame_eagerCoupledBotGame` +in [FujisakiOkamoto/Bot.lean](../../CslibFrontier/Crypto/Protocols/KEM/FujisakiOkamoto/Bot.lean). + +The checked clients are `Scheme.eval_roIndCcaGame_eq_eagerIndCcaGame` in +[FujisakiOkamoto/Security.lean](../../CslibFrontier/Crypto/Protocols/KEM/FujisakiOkamoto/Security.lean), +with two caches for `G` and `H`, and `Scheme.eval_coupledGame_eq_eagerCoupledGame` in +[NotBot/Lazy.lean](../../CslibFrontier/Crypto/Protocols/KEM/FujisakiOkamoto/NotBot/Lazy.lean), +with three caches and a key-derivation query that calls two oracles. Check them with +`scripts/build.sh --wfail --iofail CslibFrontier.Crypto.Protocols.KEM.FujisakiOkamoto.NotBot.Lazy`. + ## Certify an adaptive oracle client For native oracle efficiency, start with `WordOracleComp Operation α`: finite operation names and word payloads/replies.